From d29a82f412c1941139404e85665522f4d65fefec Mon Sep 17 00:00:00 2001 From: Johannes Theiner Date: Thu, 30 Apr 2020 14:40:28 +0200 Subject: [PATCH] A2b2: fertig --- .../TrafiicLights/TrafficLights v2_spec_1.lts | Bin 0 -> 18352 bytes mCRL2/TrafiicLights/TrafficLights v3_spec.lps | Bin 0 -> 5665 bytes mCRL2/TrafiicLights/TrafficLights v4_spec.lps | Bin 0 -> 1598 bytes mCRL2/TrafiicLights/v2/v2_spec.lps | Bin 1491 -> 1564 bytes mCRL2/TrafiicLights/v2/v2_spec.lts | Bin 0 -> 8425 bytes mCRL2/TrafiicLights/v2/v2_spec.mcrl2 | 67 +++++++++++++++--- mCRL2/VendingMachine/VendingMachine_spec.lps | Bin 1804 -> 1802 bytes mCRL2/VendingMachine/VendingMachine_spec.lts | Bin 12919 -> 12917 bytes .../VendingMachine/VendingMachine_spec.mcrl2 | 17 +++-- 9 files changed, 68 insertions(+), 16 deletions(-) create mode 100644 mCRL2/TrafiicLights/TrafficLights v2_spec_1.lts create mode 100644 mCRL2/TrafiicLights/TrafficLights v3_spec.lps create mode 100644 mCRL2/TrafiicLights/TrafficLights v4_spec.lps create mode 100644 mCRL2/TrafiicLights/v2/v2_spec.lts diff --git a/mCRL2/TrafiicLights/TrafficLights v2_spec_1.lts b/mCRL2/TrafiicLights/TrafficLights v2_spec_1.lts new file mode 100644 index 0000000000000000000000000000000000000000..3d85ce2cbf33fbad8fb6d86928d6b5f198a09ef1 GIT binary patch literal 18352 zcmYkD2UrtX*T-ijw9ups9VA5vMQRiwSW*ZbLLi}c5+D$25W!fIu&9WlA&L#Mibg=J zxa(ThUCJuPg1XqE>q^m8G+5SMx4rv*-zYPFUwoeA{_pRc|2g;0+);x9ttXlcs;yZC zwE|IPfjB}`D=exLRaF9@QA$;9U5o%UF#*i2+=yufMTV8gOep}GFBMi)*EQyeMUuMZ z00;n}X-Zw~%Az_}Riy-HZVnk4n^;)Rv$nB??LZu8U?41z)B&KOq-y2Ibc0pGkJ4u8 z$Nan^BkeA@~KX> zun6(Rn|xeI%ACNNR8?13Nknx*0K|U`V${}Ft%58;JP4X`s$&F+RWX$UVFTpm=IG)& z-|L4Kh?SXK@>fd-Yr24vw@l7eC(uePALSX2}*Dk(*#4473_ zVq{}K5>{=ML?WszK~}|DoQE*vJqQs=RgyUoJoiBbK;wjhYP3zf0kVlmizX2Tbp?#- zYB7WdogrsW=%sQVVMTZzUccUOv8o zLBZ6;A)#Tk@TJR^ub?xStO#~wRCG*iTzop36e4keN?jA2WoXB7zYwWEL?)-VrzC9f8O@Vr7QzJ9c?K zwf#{TfS^6-04@NN!3JdO1j53V$fY)96d`8~GBe?)XJlq&=j1|o94_YLB6@n%J(!lH8QI9L{;_YlAG;~j;Z&!SHUCFRqpFk4zs zC#OGP3lvh=pC#gd$ zBzfY3LZMiaS5PTH%tUpf0`VL{4rdVy?Y zhb5rsV~k6As6sxbWUEE+Z@6x3Gt^O!6sWT`tJN} zFMxRxz{i5IiZMHY2rTZ!Ipaf<0R_PI2~7ny071Q>TtH6$y4Uq(KmiZ314l1L=)Gl( z{S9A>eK!YM0TGU-CZyjC6jr7N_HuxG@_^T%x7BKc1pw2Oa0S>Bv&oU*M<-eNm7BJ2 zfm(3;ne^D<9sOXz7i`%k(!xO=*CyZ7Q5NTD&9Vc0NrM|m05^i|m<}A-yul>XGqAhE zPV>O5jU+Z8Y%&96oi(GbOPRx4wt+DVvSd4wJq9yH@C4a>Q?*?O-4BY1Z}&dX5u81I zbQ>^$FA0u5ydk}hYFfJ#daxi_OWNyHq>1;v^4831XZeE7rNS0v;QoVye#`{%$Fz|2 z;qEWN(8)B}x9`B>q<5pPHJ7xG$*EQZg|`XJwKKpk*bEtVu-8Fe-G=94h!GuZV$$%y zN!iIhfmi#L!(NWuR4eg+j?kWSCy?S*3m$^1IsBb)5_ z1`+tf+wG}FN03)pTeF2X^lJYhxp^Ryet5S(A#S0qmERd4^SbKRxZml!U-^il&B8iX zI}6W5b~O8WgH^!+toSq6@7y}3AuP1#zYulkGM(YNLx$bjix$C;!gH9%x5!=VGwH|A zfr7VZr`tlG&h)0-NusE)csV=~J~gqbtu-_c%YfLfhNrawYs|e)@R{Fr%T6^4-^iOC zUi2m{O0qvey7)G*yGdxeVKa2&S=x6-aJt|?^lf_9w|oB>9NyfLZRQ$HGzXYw28)27 zYG>LvBF5)Kk-w&S#@2?3EOZhG;_+n=qF&!To4G*(KML~ zogx2(!^!5xIJqr4$@&S9&kX^Hj!oizf)uj3SsY_}ZUC+wH~w~RXedKF0S7U->9OHfeWXz8 zSOIYRHPpuAVH6p)0l0DKB>Q0`GYJ!h51DdqD@qz4(=iX=)=qRX>@f?vZHJ1C$8`BE zOgKHJlW#vmiRjko(z&6bA`qMOzB7VO0<1tkG&1JS2yp5KD)4tMGf!fo=FTATR02wZ ze!lcM7v%mt0t{LIJlHf;@bj?z0P*%9%0Q^v2~A+!9sz4+Pyyb)JV~D$18=d(b+?BV z??hF~)TA{;iSwEdlY^b8FY>$8rx)ZDgl0l_geU}YPPfs?HFt`D-I!QW_D>3X{W^)NU+fd-}rp#$;bVypmEu<&sSVKV-4F~i#YaXv{|H(rP` zX!rqk#TVTdUS}ch{+wulUCR7hHfD6RgyA_fl5oqO z{skuJw`>&6VJHFaS$*~>SfA=Zm|T%+&#=x*wIV6qa~1TQt{*bZH$Lu`10DGi3dMb+9DOf#9J-Bhu3BnF}!CkY*$I$UsR+ zb_bdZ0-6u#Bqdt~9l}IZcE_Zq9wo-v+sTJ8A?3ECxyDn%GiXFOf5+!$xLJG^5ahz& zE)Oc_ZzrGf&DoAIdQDu83Vdgl(=mmYt5H#tzJav}6G7<;+1KY$!sRuW=A+}UIOxDSSw^oZNNxh( z5tBDe;Tg#aIUda1Sh|0X11q;z}-4_O*XT zxc)@afX7-Znb726p#W{NkF{Ug#uqnnTJ6Pr& zn@mNSk1Q2Z)1v5+5(LgWgO_*9%X zlOHJWgZRO+nKe0!PzLVHM-y*+gC;IbTM|DvL|V*FLt1oALs}H4AuTSCxPbTT3n zDPoX`!+AGk0`k7lOh`79o@<=Be~ts5>k_G)-NPGT=OxnDZR9a@bjmB|?oQJ8Mn;qU@|^{uQ;enqX+$RfjR$ zjI;|e4evrsv$_yd7gaT8%6wdlnw6_0;7^$FRn@Z|51=GYB?(-L3A5dQ{5CglFtAm! z<2@<>Ml*HCALQng9UthIYxl}Bj<Y)2<7tDeOXOdZ^x`3}F5z8I5AA-h=BWi)5(o=0wW+HFa{B-(94yyU$Dk1-a6H4?L99-%1`&BpIAQ7AA`v%^&0v;ieS z`!*U9=EeYX6rJSml0%KwyA&pW73|u;{EN6tMlfW2`Nak_5M)K6f#7cBskd%7^3+?t z8+q#G?na(^^Sdm*LNU}>*=1_-mw%Tf^RL7%6M~_o3Xd}6($%YwRfMRJRivtrRoL&d zL>cZ^Veu|gERZ#P9<}q_WokmEp(1jZC6j~+qg|$Q@0 zmzmv|aPAx=Vt+UW%i1rMcT3SQpS^=DkJ!BOzs!~i8dXV z=?4lsh7|`$%C<#wDF&|!n0q#(0>qJ_J*~jOHGA5a2bb>IgjCtN1!YDrl&)Qyus~2L z?%GD+F6?S!a^t%;%em&NZFkTnAncE5V4Z3kaaxZ~FH*HlPho=4g1JH*q$4)H8;i}}ocT!S`2apRE2zePoqTO#8}Oc=XGlgF2$L~1pL<#KO?Tiqnz z$g;X3^K-GfsyJ3|8u3pi-&5Xn4P zd}9Zif(u5Ue_#%L4LJQ9I_(BuQ4CI(SZ7%y%HkwpO}R%74Y0^tay6BqmxP1c{c`hv^6Et-BQmLY(%)ggH~l z>>BExYS+WvYHxQCx3$>r@MMCgU3XJLq+7S$;2g)9ji7->j#l<&t6i-@CC$}=z|C~E zXL6lgZRFfC8*2wN8rn=nqkWvMac;5BHux@6XM0vxt+Q=VPOv+Yoa~My+qfgih3-f) z$!a@eGqzHul?vCo19gC`I_R;OSYy?$h=WnG)UjhGwiOlG@OD;?E4+*FSPXYCmo0=< zLCfOZyajU@VE%6I7C^M9bMv3JSmfp-+sd=`N0~8qD{SkF+bXd2pG;U_>(i7F;o|d| z-7s(oAm3NJAe>g9BKG9lV&xGBNJZpgm1 z+I9$%2ilI{}dxFew{VycNu@$e0 zkUZ}-87FstO;9kZUXz*_0h2_WgfofUF!LroneSIkA~(pAnFTsu71~Og{=@=w2+1Av z{Wy7vzE{DZ=#MlpqNe&$W}Go({PGwo07k3yWk0Sp{N-_aT-M7Yia3{F`cP)@prHKq zQOq&4tO)h?o$19UaTRehCkV4O&d8c)0*|Pk7aj zdxfP~yy}%XV`Am2{$Q5~G;HzHN^~Az9bPB#oA}3#EZeRr6>bfYm;Y@y|I}^_NH(a*&EVymBCydz+y3{k>;Rjq`5WINOMbH zm1B(Yunu+4epP1n=qpsXzABZ`Fd=?brU+kzl7&xa(OhHWf_VK5Dv+;y&GoOq$vXXO z*5o4n3z9W&>NUy?zEHw1Ut)nciQwfM!utg;Uo+oFynHEtZ!l>MO*Ty0f|H?>_N>YD zNh^}IzO}M46F`CM}*g}An5~C&|klhuf_!M`UP2P{+>mdDRN;F@f52pi9U@h zOC#B?ElZuWT~?Mvw#_L{qHEoX(@5Hi;#7v#uQ<6$n^1)0S`;C6*`+4S_|jXn+t@_ie_Skdnmdxpomd{ zn1B_C$+`-}WOI%z$;t zvh+)WM}4W9=@C-8SMHH2P-BcfZ7=weWLqpyPuhA4c9U%*#d}d^oTM@m?}JpU#p-Dl zO}v|sl3Cb^vE&rz!Y_#_Wre$&QhW+`6R5FeyD^p$XIl0p;aY8(dg@wm*zYwkzJ5m+wkWsVm<_Oj%UEy(xuPzMVjYOORYa36i^@1j&skL2?bMlsMyts$GPQ zp;aBsjp#k+DkLQbcVmpMr5yZ{ zq>VbLW@wEM?rqXa`@h^h*R*k&cX-b}Q~(TWRu5w0(u0_k_aG*|C%Q0Z-xs$(1ItPh zneESlM3Viv3=wsIW|JtTHy34)-Hh$=xAuKS2i`&F$Orx)o?{(&+jI_h;8$7W+P-&? z;j+G8%?xw;KG2)p`hHb3S7_eh`u#M&nwBSM-pb1@H1Db9E05x#bBmA8Bc9_QHEB9$ zchpqYDC{<&J9%`QK^g3B6M3Uyx2gQE#v>-IOJPUm5j--ESTa4Fj+n|lM2Ai2ue=Y> zBfW|_Y$A8TA2y@9)byUDYlC{fA!)h2XBb-R-hn1d{{G$W%Yn9yt_D=r2_mf14z2lI`viBZCRNwn!lPKiSZOAb7 z(2r(@_J{7#n~M+qsA%>)dK;>VJUR~67#+Pg@ox3e9~JLt-M4X0ncd^S9_Q|R%spk@ zzM^ybTc-ZW3V|oGO=d?RMT)M3#~z@ z6RH(qS%hk0n2Se_7kXB4{pB8+rscjK>GJY8k1T4rnO_FV0QxJ5Umocd)h}J{lH!*| zb+IMqerEfM$eE`5$mCqcJ{CDEFbn6Ki7`gjTHj2wtYyCGvPU_->7++)6yzUke0o9l zP89*^s6c*z`4g7W$v*E$fE99NqBN)E)d{nEcSYY3J?tEdp#kC+j;#=zaaE_ zK)T@JTZ40A`$~X4hQ9U8J&nE+>Ygx4HGN+OrPg$x6Q!Q9PehRfW_brx^IBpEZ|Q72 z;XTBzA$(x4g9vZQZ0>>wsJXF`&U)dKXly@p1q&YmVZ?Jn zJs)7T!0=j6q>o@vq>p4zqz@baC!5f1qq7VBA3G(f6U^ zc`4-q##k4;D2Qh?1@SbYAfD9$PfXAS+3^Dj;iy1#xuh4l8~L`#+Ps>&sCA;{I{JzJg#}bv;yJ9B@69Xv`U=eP$cy zAtGwk@N#Cu+t2C3fC09cgYbjT0^0iTyLqD^Bj4vae(#wcv_+`X1 zYiz|^?2?$djD-WOqqKT}f$(vXs(JVXM2#2t9?MNbX=dzJ#;?A6FoTR&M*W#eN71t6Ocm1wKlkX;s za<~+WQ4X21ax`(GXYpt>sfT})lk8`AlSA|q-b`fqdEAVZ9b;eLmUP$fdMk9d@p>EM zZrJrr&DDUA-#Hg67Er14pwH4CTTy2}w1YO-k)^IPkK#Q#} zw}OicF1N836EAO;ea*NOR*fB_jo>9@AJ<(%_Hp?oWFK>HEJqo@ikg1|S##wLWX=9J zkToZc(6Bsvq2;xup94qguhC4%A=j2O$*I?9a+TlNOPH^NOR6NTcBrUH@6X=`P|&p^epz~CW4*mU<~+s?I4Hzd+=c5ghldT ztir-(H0&hWFrXf!Skp97(Gh|FW`Ez2hYk%TnEpR zO2k*b{mdK|Ub%pCh`;jP#4htI=M}r^emIMnK+hKa@ICPv?}xKZ&)^@<66^%mzYj$3 z5Jt~}>xgH>b;Q%)I^x+dd;w#uzR=nFBC(Ug5Bw zaUNsIek&N?6aDfS-?9AM8Ruoks$#xH8Dw`XApR!zIVb)a?)kj8>w@mCcNOPE^R z#WdzsleG@aD~h!x%&YRXlvpjaI4brUxY#&$jI~%AdsX&zc%&AZ&5FDR&bmZiX__sM zycX!@8zsVBjEgEWS!)(ms#q(DDwD6Ja!Oga6iyYP$(B>9Xe#2A$(zXZ7pxH${iO*R zM}N&Eucg0~lb1!mV5H?lzcfp8i+&-yUlIK(_`YAl&1AoXgquV^i-a+j-^zrmvSW)` zNH2UA(u*An=|#vwdhv+Ug1@ulZjygDj2oMp-9}}{5qCb;dkmw^P6B%9%2L{6z=KwPN zCw8r4_$YQQkMUwY&W-T}AJ32RXFaZr@eN$&&pw-k-f`gXiR|ymzgx1uo3N;7pI2Cf zBz(UeyCED>6ObFpJ^{IriW86<$&+>AGusu(LN2-y3%Tg4S;$4F#a+Z$>ekGtbErVB zmNVx&R3JZDE8|=MXMH$ln`UD<7XsZ(>8mjY-mj&vC*KdIucI$Xrb~mD*hH`S%$5{J zuO}}dMK{R4VMaHQzJa3ppxHH1{ow4ew}yV0;r8yPo__QtUeV zDy!HA(yIK(hR+3-5F(Mq&?Aw>0FlUI*0-&nK)0Ov?}|1l_-|fYL({+RZ4Crmm0XH3 z#y0_S#FHaOJm<*~&s8mJF-Dg!X<1K{r?oUR5gl4q%NZrjjTmFBqBO53uZn7Jko{rY z+(7z6x^*4OjJbb=ZE{I*|x4$R29kJaQ`67U*Y~>$zRCk;p8t!^VYV^fb*8MyfmAa)AB;L z&8_7HXGdSwvt*?O7{H-q(r|q`Bl%E!EY|IBf zy+ClD$HvuW^Vl03WZMikHjuV8Zd->kfUzxX+j{c0jBO1vj?=aV5=SKa`!nNs%lpkq)Bc;?iPMRj=TA>tZgwQt)^BjaNkTTb6W*t8 zn9qD~zrk7lzPJ_1^=w6QBU_PNqgEt$^+rbqhqlq#jFY)>KK-WiMn}@kvTcrxn?BoI za5rPO&7TM`-R4LNsNIBonHszahigsVWJHg%*#s%#3R^*Fn$&7coMyHfO;1Cu0Ks-m zn~ZUDX2;WwnUMucv~VT z-oRU!iZ_C7qudhR#Y`84&bPvii5!Ebj5zfX-7r3{B-FS#ZTV*`Kc(ufM8uu#A zctYmlU_2e{QUV6yBouH7;e8Ys!hCNG2Fu?|ae<81a2yranuQCY$GPBw6>;TIHKWQG zT1BpkgX$;Vm_fCQHxjU#;Z6ltk=;|kdis~Ppd|RqBGcR88?xzr@*9@vEtxycbUfI7 zE&dkc)iV4z?o|%{mdwQsKOXE-VR4J$?q_kI?4Dq8kN%~F#dz?SD=kklzFchi4f#vH zH_yZJJ~@wVc}w=h(DD}PNhAIgAPvKxhNKzzlX9sO{v=r{vc%(z zy)EYvHpW<5GB@HaO^6$7@Oa$2ApAT+9~W=Zgtx|6$J z{+%@A$#TfY>`5-7niaAO%umwjm4eVK?&IVQ_u*_nRIpkw8 zN2qdDyDbY7!}HL3Ly~pjszJK`j`;VgohwVF|)=9 zpgS!!!a*6?Mu5E0)d-URB{rAQ6Be3pB;1HM-$3s&H&@7V>I?zq*NY5|Nh^7VK+{Ut z5Jx>G0OYu@7XTYc6%l}}smTD4kys6ubh=rnB@1Xxx1`I>94+Yt-%=1@^?8BDM8jy% zh*e_(0>nMl0G%!m1fq!YB!J#Tv;vrNM!o?+ClU;d$x1rn#Q+Qdf>pVb(s3Y_+8r*x z*wJn4DT{c1G9%6@$d#b88nCAp(ij6$S@z}ZD6bH9HGcQaO|wSYNif9;@0zcJ38bPR z@=+JcA;T@g1(GHKPo~`RwC$}}odgH9D~BwUv5*lpnMNFt((@uSqZWj)OYtvmM(a0d zr@+qr{V zl`)VhHI`;QASL8RW<-%f*aG~On_l`z?UX#j$<8%e2Pcuq!3X|Vb|d|-Rzx>)K1E|P8P1EIyjI-4mxu;N3*jQkK>=@Y`<7qYeiN(HVe9tWLtB+`5Jb(S1r12^^EPBfd4{mX__sGp^_R8N z@?0l3*K{3RO&*~h?02CYH#{q>lN1T~gS*UMx9P>|26$3+dt|GU1G!RH(`p8!6FD35 zqWnYHYw#y;zL>qNonWLo;anSZunB1-u;_#f<$&RCp}AyQz$2*4C)@rbR!6`E?LmVH z%4mf-HIjxOkXq$#NFODJunY0GZaV5cwNs2tCtKGD9UM(&1sC=1qx2c}3gacV0zP4< z`AplCSS^4LsDg$Ql<^9fT1<->kZ#Z3kUi=h!mh<{zqxzXQ#;8>b~1An=wL4rE2!w` zK8nV0lW?I#CE)E>nm=p%RjlU0#P(A|3CdW70X3E8Js?fWGs+zG2w|7uCvK+e4{N6x z*-kF5JRMw0ZlV?)*+)5McoO+PJ1GMG{tolmwwGdc9XzBuHIkrAR5()WX`%t?tsJA= zQNIxOYW)724`vT*Cx&=V#;$cb*pbu}IDLE{<)Gnqp{rzEz{_tppKkkGtd55n?KOip zlrahuY9h^PKpL29lrc&UVHe{EZ-(lNwNpdsP7bc|Iyjw-3!d)VN9i}*FU*!u1^oOS z=C9g*5v#?pTvaoCLz$qkqE^x}2BasmjdDhPL)i6r+0C=F#oEcCB&T_Hd9`6NcYw)<`4*{=}}|-n6|ItJlE)RlOUzq2wss$Jfys2c&Ov z{>~c>2w|_of6w`I_8090F>MCuT%&^xNdE@fp4dm(-~6QplDrr2tW>{EB>q>dX2R>* z@q>QKXy&|e2F-9lYLfeRI)!kCU4VbWG0@v1{rtVM@#d ze5;+my-1uCs|(@pRQO>(Wjxbiynx0YkZ#KUJDcKlhFydIlJmu^y>^nAGGo$NsDl@f z)&|)g&7vG?-lic*S_QoA%HN(Qz7wmH;pOcuLw?FwrtvtJ<}o0R&Rd;HS#X9e!oT4} z=sUF2#GDz&&SV`dAYY`~9?7B{ZT?16D2WsBw|D%ePn;2}YvG?&EhB!)M5fDl4NW*8 zy^^y!m$L8-yAgka^TTY1cH#hk#-OuS2g9U`fvV$Kl@U?m@8<2YCuFjy4&aj2}o16vuRPEG(j2XByRtNLQ%Ys#XS(GEqJ(^^R zuYjMlXPFLO zL|PW4I+jH_+`Lf}Ea?~UZf*bVm&D)2>P&ckyLRZ9GLDHG&!8&iOow{~7jL{5PDZv-h+U1*tPo=V~2nPI?@eaw3azpn0FhRPsu|3slujCjKi{ zN5Ylu-h&m&=wXX-HqBx{>X>^zy@z;)U4*~Sf%PHUse;TIo6blb98b;(PU(F_>1*!S z#7bNQ{J@=cGl|n;buoNg%Z$O%!N6YN-IKwW- zKj-lDXSCA=*)z_asXACp?xLm~c|AcvOQ<9CKF#rJUT%%0IsO!8)oI_q_?E2%4R{P-iv!Df}lS@KB0t8TBGPW(r# zPJ|QNMT4`-m|^^Q0?lne8k$SX=pmnBm*7V^i}dx{smb&i`_4oioK1EM9`AcZ>2E%$ z$&`c(_|-e=UL`&kt1IC)m1uZYnJ{cUUO~$lke(=|5YKc_9f4l3eH;He=>UHo3)y&AOk~2Ji zd@XJ5fb`Fthj~2#XV~lU7dXGoe$Y->r-{JMbvhU#%?46WJfiGpcWI0y{|I;{s;?%- z{zt54!1e7;gKo-blI1vyh8vI?nxFVCqoA_$rZuW-f&7U z`Xv<+Ewh%|N$V65 zzOz6FlSmao)T7~)L+q^@Psv6BZSz^UySgI&rPlIeIH&2~V#AU89kgjCNKv|QsX)F*1Elo=ws&KMn>O!f;t-4{+d z!q#X~B@_WaddF8U$DZodBDh19G2Eq0AlZzU(^3Ychq5zsN_^_sbuF!&qqB+HNhMcg z(J9iw!6d(+)5pRohuO`V5J``KcV+umzl{B+S7*TX?Yf~ZWgH0_&!SNWq=LM?StXwJ zY;ntbj#xjYomS?G+&VLKa4q=;^>lwYX|19A$hrJYGVJ8<6hE-kbg0yPjR!qT+PU`fDe-$s)5( zp$_&TB?L*1UZ7~$EgFBxE&;Dsx#-#0uX;5f_G~{ll%tI8HW*K%`3^{VdCr;7J?hzI zEz_KA{c-IyH(TV=$=AVU{FUbNt%G)+p%bN?4@44627cDH~5fIO#(vSOE8q>P#^J}xgl?@c8yL@{g%3#U@?K^= zr_{46TmI#&(ZAMC-_GlE@66G`tI5Ap-}hgjoM3;aStnT~;J?^)=grt_y?QPDx9YEv z$4XAOd&+v6bU^xB&da>#0rl*4Ef+cenSHID2ukY%ve)WhBhv4IW+yIC_FqzKK*=8h zo}=o{g#Ul_Y8Je@-EeT3GP-bH3jMtCfYdzqWx5051G}K*F$dDm*G>gx^;u=JbZ{hj zWw2SVl+t_YxP~E_C*V8oyz|0;Qm-z8&#MfFmnq{59a8eoM-51~WWUUI@cO{6Y3br9 zX6I`sgHrlTvWs-ECuwDn*-7codVO^n}?PuV+)N_lFm~G zr15!WnGOp+uthDi9Hw5aoes+BbIeZB!NugSsb)u{l%to-S>QqJ_oE@iw zQ^|{iTl=JxBbN?qxRL+?KYhoYm;TT6>T-CmiamT$nNVn(QhGjZKzcO0EXTp;1AAr5 zR!;Y9u6FVix6eGgTnC4c76-K+lTr>}+Mo%NoDlFHY`^o1|L=Nr7VO-9Y3QOdt`L`! zetyY-RGfDt%fa&lyQ1ZHPNDv1?ewYKKG*Cl9b8YoOKt6!QjT9buc?t#3HT3o@m~AS z>eW*CrRvhiMJ1=uEv4c7ssX7!=SZG|{|ENkmajQevp;JmYEt{4Y^e^mB;5^+J0YbU zxU^S;m%I`1LRGv;|9|!BD7dWMV{ol9ddeat;{3b;scY_$^j*Xc?4p*t92@;|?Nm)> zpG|g@4o)QVgX4Ptq4ZrkqKT2X3;3Zsc{BdgdUXkWMCCEORvABKmm)aN8IX2nAIaY3 z{edlM*~w|2U9O$1N$xYvF44jMBz{ob(SInKOPe*`k}n0kvr67G|Mz-z8tl`q8Ct81 zoia?}oevn0X6N~2?(+D+E^m3pN!EX-ovz95bIwlF!Ik8l)VL%6P>x+1(1;{?0{+KyoPq(wEsVPH3yDu7Y_cbjG4lx#GiK`kS@*j$=F5yz%FUI#0l1~ z(@woh@3YV5=-^zkUGTNOe<=Nzx-}V+6#{<44&E#O=X!M&yjdk2{#ThWWt}2EpEn@= zHrpp>m+uGms+MNX!0bBhWc~`S`Q9iJ%TK?kH>i?^qewXJxKRZtcuOmOBUhDsda^ljr znnuZb0sl{ezsx3%?vUTLS$1aB!^QQa?fNdJr7!f4>m4z(~XWs>f5LA+s1CMvLj}-#U2lx@O(nMv^2GOe%O(-UtD|M@Xh9v{iAkiR(sdH*!eCO z{&Vukl3PKdw9eBNr^h9dU8vxTno|Kl}*i z2hV_TK{rpU41EzXecZMKsjOb9{o$CZu;zBlwM>d%n$@1AZ`xzhJQqCMuWI`?krqN+ z)OhP~`*#U3*Vq(4LFdYBX8!wAEDxqyrT!v1;q^*y!O@gp$?X<=*Vwb{ow13DG+o%M zFTS|JV z*5d|m-_!Z}zKE~+YWm1{+gH&EiFGq|$H!^4w`N8&7I;#^>sIq-9)}?*51!|K8T)ui z&oU&%_027(w4UFl4=3BQx{O%9zYTTP9bx86PTmnR+No_P$5!7aF45g72tIk!X*9mX zZRz$s`qv?Qc*6K+eN^>8bV7aIp6kb{#kIHhjHVv)3=faD=k0kPHnZc4MrW1UIHYTSZ+eJzz;Tri-<@P z1QgU7A>0%dDfL&kwF#hH#0r9|wU-5@t*Grr7hB5O?my9P_uprp=lkZI?_Az46v#4_io9F^v=ZkPD0xy4K>%BVt9yz>ip@neasafAmgVFt zi+5!!3YD<{2ml~ntSs1hi`nuOJpu%kWqm(3#;S+L4(BVQ_d0gtwv5KsalQxJibdfFOvsV&`S& z?JEF4Oo2>_!Y!6%XXkx@=Gk2!lcD&r@wxkQ!q9xO&|Pn~khfd#+bzhlA#W1o%QDe` zIK%>9{8qpqdHMNyg$kt%0C5&0RzX4D2aqj@13{aO`8;WI9xqoaD}r2{SGlZS<3^#< z=#aG)vclfZ&)-t`_Vf(M350WHMQE*r!t^ZJ=7RLBEJdb3v0IL+;JCcJY_ye@6Lvvf zVWA>-H(CliY!`ZluEB4&5L741D|{=20-&`pJ^v4gI2i343J>9=E7Mu|`Pq;)=nOhr zTg3RixiAH7Am|Kx`i6#MoC6rvnfnR~WVseJ7K_yMg8vjjqpkJ!2@DDj30wD0L}b+Z z=$P0IOjaD56Q7XCf++YmG0-SQVQ3T?TKk{JR%A2><3AR~7K>uE zAy6@D1{I_2f{NCmi|maq!lHY}vV>a}%R!OlO@_K*ii0g(Ee=L~&^5?n5NR>6*vn8; zREgT6>)ZFYE@)VrKRWyG{=Wfd5nvE>1XqF{pb#sSW$Z)m5zER%M+dS&Hf|Dc-je!m z8id1Oc$Vg4Whjvf(8}J75Nd|<>&+`WFDD1R=0drJ!#0_6S?2ryCb(VZ9|YNwYoQA| zZkcbWFMh*wYc$BeA=xBm=VhQ*`-hAHi_k)tnP{a}s1-WaD1$}lAPM(nD^UfA^4Xrb z4<&MzB3CBeRUk`8ISFrivtgN;oP8N6;;i)SLNw`$KWW3uRVbl+^qvBo5oU5;YI?SX zhqfGao(mKi``+XM(Sc=<1!&mx0#QL;rmV0~ye}swJy&W~o(^JAS7_&MGz1O<%CH<+ zwlW>f@L%Q-I+7rc_+Pp=nJs#m4XU@qwN#37CmGxdZUg0@Vox6x2m$~tP@@MpDqz9` zVjNOIJ}P{-$|_^howFJE$p8>5ftD-4791M@Tw%bS?G8o5>Hs#OoCeoWxu4pOX(uGZ z<+Pd*Lr^77&p8VtdS*Y2Ga}k?(S>pnmo^++=QPW?4AYunA4yy_Of|40ht9xUg5Wwl zHY>OQ57}j?kW>K22l?tOAE46e6Cjf%CaYK=r!AuokvQF}O93%9+seOaOYl)uRcK0T zojM^qH-C)d=p+?5EMia(iRc8Ch&q5k*K5ggJjbmZ2e@NrM?t3sf<*NRNGMl4=}Azv zF`p2$zHLob*lJ=4%pyi%=hpg!HrsMlO$w;4nm`#v}EwBx4XrYVQ&Yo@O!=X{nlVh}2rye1B zp>L&$*32VMj&S7{g{n)q)P8Pfwbzb#D_8t2+H>3pVP%K4U;nMuUTy7e*dKJcFd-!X zOHN6K8$>oC4W)ScX`i;EZqU~qr=df1MtARss;_62v5i+d&bTz|@3Y0sXxP+H+q<-K zt78!{p6b_$l{IgTOo~*a8{c+g3TkF095gn+qyFmmPq|%#%*(~^W?m>R%5?&+ z_{{0Sbf20lQYejIbvPm$Oygg`MP#Vb+N%xvxf8w*ay`~t>5QCXz7A5kX8v!F7H>&sYaRWF6Q7P9xd6t@$j{z&!X3QR!7l90x$*hm|Rb6kP zx~!mV2a%IWgVIh1SD=BaT?%qLN!=)zTmgY()|nTQXa@5_i^K(j+;J&Xj6g+dk4My!f^uPq9)e+|H~`RRA8pwr*gObSQJ*YzyOAaFf+eT| z^kD^?Cu5?F{Vm9v6%;-IIW>rbF?toZp;ks!BDhT~!Mt6?wdC&_jMyR_6MGebcC5YTzL-ek$(C*h7}{R(__3r&T)s7A(hG)*;k72?;@_c= z-Fkr&?xpR6Eqir@>m}3IE%}qd9y-lykXdr>a`c^Zfw*qE=k=SwY%yX>=HEHDiGwoXl0FV z^uF8Mxu*qSi4scj_Q~D8H@8|-RSo)yrA9YLQDWUoJ2vRZ+G_5OiPZnEGuh<`g$F=! z4Ua=AM0(z)lQPjBTijW@I~A-sAsq3AekO=8<8XRq#dNjJrK8LzQ?IlD%{x3)z6K9( z@wvGJZFIFE?T%g^JQRiSTuatp?x@&xGCBbfCF|F+ST%Acj>rf9+V^eCk|ldXE-9Z?$SjVm_~) zmzwv7mH7cksi5v#yFqX@E8ZLt6EWN4T)IXL?XNieD8DGhL<(J6Zws%1j}6W)K2r}% zk=(GdYzTSCtuw7KfooYE=Avky*)z^@tE-^^^{q$dk`GK!XeGrZwjP9k46No>%mGIY z=G%l)CkLh5E=tAVb^Kg2bxGp>gmxV`*aZ=XqT_JwPiG0NyAPyX76G}IWIKkqgZBLN zCTiu>D>K*gNyzn}gH;e=D2jzJ6DPNn677>K1F8jTqUyB%=~A1UBOA(; z)O5yygz@rYdNS41nGm`N9f32k?+l9;=i-b~C(p1lJb)|V+77{O;D%bTQPN0V>lArC zl{j%m4`>Yk5(b^6JJelV$Z|}8copx>br)?uLz$k4 zYK?6I;NSe0;}51#)zZ%eeNPD_LDxd+nncK3{nf0zq~MJGbgx%y>=6LQ1S|_HC-tq8 zpO?0|k-LS9U*Xz8Thp2s12GYk=N9%`3n{58h@~rwH9pbvLhcwM*4QFhyu}erd%2(K z)C*-aW3qiA*k>@ffi z4!9;@T>=hC?+a_f354FW3wu}IrX;G=@wy$cv@`>ai6&-Qdw0`#A{T3XI}&_5w}PAB5a`vO}-y2Heo#Vf+`( zI#&tx0sTPe!LD%PsTk_j_9qA-u7BDfT}43t%2!UP=gO_dlbdwgr(RVuX@_vr{l1m( z2`kM|zPWSov0?sQC*-mXrG9QLy>N(Mj3e3&oh5P)^0jqoN|w9C7;Ps@B-< zL-2ckQLH$#>V)*5fUz@z@SM0|_0V(|-mXzpI`wLp;JFo?uC=d%|6;ZAhS}UR_?w}T z;)MK+KYeg+;a258g^b_j%Or%@dr={y+<LJwK<|=R||# zx}4Z{*vQS#eofHeqx~MT<82b}X_*z$69V}eD)D){LP(~m+1i}QGga-+MpYa8Ul|61 zT9JC2)AhuK`<2gxa-w{>mP&9vugHODkcaMkjGkj;lkORm+<`I~fD7jjd~t{bLj2UG zDVoG9BK80|v1%vb{QCCz_9xvyeE)ZbMY$G75)6EMga`(YHy@j7%Xg1(KVX~Kb%5x< zq3uTdLN_4nzhSUVYrxfW2TX?@%Dqj8&5xpe&1V#BH-8G739ZrkM`R9b;|hK?)D_j> zk~fA;X&hM2rX({dCIY#j$Rzqxl9O$@9C`m{A(X@ypN$nHo7A*5~-2jFlERV43rfDI6Ob>_90!lr|F!zKiU^DDBg4Mf_&BYA4^O2 z5|Qc4cH3gBRB(KNOR{NHRXaZ7Zw=c?b;wUiGq-9}HHKN%y77{x zy?mzUReSLTZw_1>@KkuiTlLZGk4rK)$6?{jSM{ly-dWa)@oUHSjx#;3t`h$g84v&B z_mpismpHu_&>Bt&iX4Lo(GH)J+NUdPqZ-X;r(S)H{+(EhKXT;2_JMnn278RU*>9Ha zxsmC~GxsY}H9e15nDK|r<~{keqQC?GiCx~rPh#fowLdG;a$o+{P#RT(e8iu*b5P6* zHU0C&(`avQN6#+sJmp;z^q%&U^|N72?xybzudR+FJCO}FQwujaw}neW`SJmT_;pXu zhqyNND&4vbkJq(7f%Tl1Hw{o$D{iOl2KCfj0_TVTJ}+NpF&v`L^e~&+pm(+FB1i*9 z&ZcF9I((pvP>K6#=iD2(f=%GtwL34_(V{-M!uW^ z5TZMKL=^_eMSCxbpqx!Gr@T(qB=-lL70{j~PSpUq`Fq039aPfH*`EBvZO}WqEwM!9 zWU_hh>s$@K-|uXk`?JL98sN};lYkRLCw|)2!#&ukwpVX_v{>?i4lCACw#BNM@SQ*( zzQ+Rf)ckisP8oqv+S?=7bV5G5rWl7;?F)1u?&V!W#(^4S4}bFnGhB043;K@pn`*2? z)L(JpOTYxYF2E<5zB=*lD4>$w5Dr(6Nu@3yBAJ7q*47?7WF?_3`TZU=(iKm1+(0SoCTrOM!x(B zo%H&=cXoM}`ooHgkNk>KQe4Dek{-r>#)Cif=O@zARHx^A1oKHj4vQV$+goxdDQ6&x zwqyNKKlCqY-tf|KploF$?sq}sw{ahX)bWO6W2sZGq5#idN#b99M&XbB_{@&2dKKZs z()(^FXSj`~;}w=YOh|e0)AKu zREJ0yq8~b(8z?W%xyf|%%QT}poovPs{D3pdf+Nd@d(*@vZlCrXpw3Ut?|;wl?f)-w zV%~pQ7z&Xh9@f&WCy`nAQ_Ir)13SwyZ72>%03_Rj zm7W@=GT@=xQJE}7orWd~6GVheAvfn16r!mB576zfo2Z%!u4s`sY)8Y^Wenqoo(_tm z?7^TP6#*4ciFmkaUjP@uek!mUs3a?sr}QNP4{!jIff8uIOL)k;RKxCuw?TzMtviRH#T?v|N3Hfph8V5RFx;H4*NN1 z021JZlWbwQ%~oH4_B69J1ykd-OFsge+YxSo$7-egA(%JenOSAP$Dul4Li1FFt%hl! z{QQ2U4)||keJx?W3<}^nP0A`LOR-LtanqqtU3l+aSWvhQV33Kf+Xxj%3~Ug>C_F_9 zbbu5%Xg^0mw-=~Tjs&Fqh1pUHe!f8h=e!5MAOQetz*>+Etl*WBnFxj;2Bc>gC=lsY zXYZB>aSAzWBx)UCXg+Zd(g~CJr_s~BTP~Sgl+L_edp*D5n`=PV7eVq5 z5{K|ISFSg*V|*P+~naq^RUg$P0zeg)WQYNp19;I%C1oI4}PD8{8qRA&d% zvG)q>ijxs1*9(YgfanMB521M3giM-#z*bcdpNeZyV~%Ei-r%(q6&};2p0p9%VIaHt z4$$3+k%?DaX3c=pH7OSlO3!2~(z7))Gp;j0JRps!EmiotHS=ccrpQ<0@pzXEw{Dxg zKOe8qmzowI60UOqysveHA9Sv%C@UAprY+9b=&Z6rtL^4u3i@L#+PR}Ua#2tq`~F+7 z`OTQ(@o2qeC)$5|Ce7-YnwZEK>B{!(FQ0W<;_FdS@l@=$nXW&F4jvLy4f6xLZ`H+y zyKhf!usXCS#ztIs=4US7u8Y1MitL;FNYGTOlBULoC6`70M=SJ;>L;%L6r_Q>g<7^D zJ$Z!A`nT)Y7$xtDat^cQq9WC+KXOW1bF?vg@vbA`>k{?FK{>j6KoNeR6IEW%5cH@A zfA2gtx?OTFuu-kw>^T0%Ix+Kw`hrYtnz3>{Bc?5DPvhR63u6sM?#-q80!+pvY*NFV*;}b;hVt3(a zwPeVbETN^*b1B94*Uf^H2VzyT(~a@g)SNF}{zc{0@egWl5TE7mNUj)O!0!@!7P>;` zcS+J{mD+gYTG{E3jXHVJobZ>5ON#Yp^Ahi+OB#(t_owYi*2lq-iP}e9Kdf$QoBC%q eBbt!)VV``V<-xxvY+2+(nWl8>g&cFcV)8%G@#<;- literal 0 HcmV?d00001 diff --git a/mCRL2/TrafiicLights/v2/v2_spec.lps b/mCRL2/TrafiicLights/v2/v2_spec.lps index 431f53fc43778bdabb53ef41c47342fed38071be..39315feb515a78c2aef6d0de6a29344f0b137388 100644 GIT binary patch delta 1270 zcmYk4{ZCU@7{||Z?=AFIOIs))+H$Rx3L+qdj!kWA3q>dvDr{sUaC>`;)zVw;y`3yE zsk~?gW`?&eVEjQ*k?EE>HrhC(O9;8b9vWWh0a_;lobDrn> z{XFMq)g|>lbpFF(sx{{@BZQ-ICgzC>94kfnID)JoFG!7HP^pkwo1@#Y|A5=mJWQ|bvN_Z2&R0@hx2FQgXuu$T0{uBb4 zi^ZG>in5m2_JBema+`9L?1so7$6=sbSb-PCXuP*Qo{@|o8($12I2Hgy2(t)O4KY51 zB|J+i{=eRRtQp(f{H{v97*)R*)MRkjyZwATD)E>N8Q?|SSdN8o-3VM zQ`Mw9RjdqG6xnNiuST;8wEu{zD7(AdB*IPariyq+K7h7TvVDN!L5x#hI&eQu*$yhR1_fjxFnkw1yJ}ZEbEi+hvQ4 zATBUR*xvKrZhg>1d4{Y=r<g~-XTwCAQd zBDLsN*Y`VW3h0T07u?q-Je~5_lQQi@(*+^)Mq%`#U{m}w`;GOrdH-8Wdw(~qG?Y3@ z9#%y229~ewboCl%b!od^R_hC-b&F3d*IhR{)7J5{{Zc!3MEYe~yMAZy!diRf%B?*O q*4WLW-xe`{Bil;uAh{q delta 1150 zcmYjPZA?>F7{2G;TYB5xvKB55EQ7YR2t{VgM}Z02mV!{eE(0CYD(jcCOX(y-rsToRX4~ z_BzZ@!o&q3p+O%zqdWI9}N3Y_ElYWOqN;``dwG2Z+JJ&A@gEMw<2@d_bTXYC;badfe>x2N<`#`^8`cAh2FdG`hVm z8$&Xb!{zt4b$4~yyv`&!*W)DnD}kC@4$9!FDlSEX!`yA>>S>$D&xICQK}@}6B5uI0 zdN&*%0GU7ua=;;AFiL_@0#ZSr1<@#Ue@;0t4owCN2S8k#fCMO1h_e`3CtsAabwMOO z$cF0j2B5}PbR?Kxm%b^^*_Z)Hzs!ya(3`&E?&2MAK6a^YZe7=WcxH&TL0$ylw`hxEWRRc z_1(yu*Ck8v3Bv=cMEcdv%A>o<6VMu(~xBxWW99 z0z}o)9C@t`;`li)AQ-vAKCv!0Vv!y?xT9$oxO&g-OW;Hq7 zFEd{%AWxOame@O~(j(35Wlam`r?srgxJn2A+M1maVV0VmGV<0<+3!Plq~U`N>)F>9 yewm81kB_ZA8Cw6*mr{~tRIY6QT=_+_vSQm_bOL*n`VDz`R386|9;UC;!G8dy;dZ+K diff --git a/mCRL2/TrafiicLights/v2/v2_spec.lts b/mCRL2/TrafiicLights/v2/v2_spec.lts new file mode 100644 index 0000000000000000000000000000000000000000..77fc0b9d5f82b8e21deac0c10316c6c67b462aec GIT binary patch literal 8425 zcmYk92Ut`08phAbAd5gC3lIfD*dRlKi8El34FM9SUJ@Y+$Ow>tdbJ`%B`n!9YNVj3 zr6mHPj#^|?5m8h?mQ|5D+H$Mb+TN?QH+YWsHatA%_r34?U*9<=JOCwM6{7r&wurNn zQZmG8yp(K7qAVpd0|50RGqYs@Ngy5%=#z|$S2=mI)}k|XS~39YZ;+%*WqT9SQgURQ z01yB`e55Q}o+#UrnURCUU=Vs3EYZLaM1m-kM4Tf7Ky*%~e0d})PqJJZZ&)6hkf@7) z9G98B2~p5tfCdS4hUMyY9-GOyt-c5(4!^t!Xlf7v;xNl)gk&cI4T4BK8Pwa7nU*Qf z20&!CBuTf(u55{9dFy*6X=#~xIypov1wb%J_ZtO(xaHB_+1Z(S2m**hfMo2)*`<<1 z5Cn19<-JEj1=1i>mMqEsTQ>+{(txDU%z%s}$sPoaLNhTnTd@*>(OW*|8ZS17>$3$x z2Jsn^J-Qx1d&1|4cS=4LsDzJO(ND}w-=S;ta*J~S5Tg^}C2=TSBP6;8`DA9M0U(wq zmWjQk(lmr2f^LDNGb}L6if>j1ilFNYNCzztbOyK^07=VwlsNnU+autttZnV=9UPr` zx6}?8^lT1SudDGzXcu#E;uf5CrRP=Kt8^?}g{z3ol)f!%7Ir%t(=C zF5dxurtUxnIWn4f*!gb z94TEQ6DK6;nw*d<5hqEqbv?5Iak`)NR9Ut-BS$wTGb7>uF9ZNmrD@`njD)|r%TGJ1 zfb?-j55&ezdfbf6BncOBC;>s=jHX*`_FkvY-6_vVOpr@;OX&{&zXt&2yu5F3-5sav zPR5h((4BCnI4wt)G33g1&*RRN3`tT#_Q$s9r_0l1DGB0_?=Zq)`AK2u>3Xl*A;KP9 z4dTo`9yd)l;BULj*_$Jir0dSL0o=5FGCwyGpa%f{KmZr00rZB{%pzL=*A8ec!3%sN zhIijqkx>L9&4)y)2EFq^8VW#HBw1P?A{jAF6gZw~sp(^Hgts24igXwZ6mo$?OU?~T zA9X9h_V~jAZwdJ1*Qih6`x}4?$Hy)9JhWqBTnpQ=I2`F+=Gz%b*#RC7LT81Nl7(*k z8Y4v67IZ)W$wW97F$w~v0yN1eq(+OEGCHwU*iN8g0b8N0aO`*FHWVolKQacfF*_>} zCyL&hfIbMRop&q6$-9bT?X4YW*!VDN7FaU^KZ26H=>r47p`Mj>% z95-dfLf;>xzACFGyTU{Nf>T_32te-{7}(ARk0CTS&xZg(R6{^5w90@8P~U(6Jmm<3 ziLKsa2x*jj2n-NvSSft+B}4$%=pIC%y}SNn2yv)<2uzJFA)pk5he8DMiy#2THoyvY zBla>z(N2xe1H|eqgn(Z{v_;~9qWUL{vp{5)=s6& zK?H8TT`Pic)iKxv^VJYhmrSBytx*aA*mwa3i=jplgwz7)3K-Kq#7yTy1vm}20(2cJ zEQJGlln=2Sn1PG)aMEyADT0uODer@beqav`BB0{m@NjVLqjC`>5&(W5MAQR+WIdrj zswV})0`0)RIqr5hqC}8SYS;=Jl>NT8kOuPHAOHs8#|6a9`G_D5;R}1l5sx9FUupdg zBCu@?Hj`Gv%KAxx2ttDp*ju&jF+|iW)FTjq;S?rJD~9NQOmIbzK=gx+mAuCg(KoRE0};sTgw39ESXnb0t%i_*@#R89-Pk?tPM(dX z$HM|`W6$fm)_45WkdHbU4jYsW`j;RL)EB|vj_kV*)Xx#6rQNWyvG0*d?ZdKlPzi+a zVLkXA3@dL9s3A0;hOPkOfe0enL+3b%z~SFqZr)Wxh1m#n1@x|qAfh}>GlR87_@04_ zT1Wwj*S=RnNG+}3Wrsf7=3qA1wU4MK#XHEtSoPjwwNgjqIfbdWR5%u_$o3M6(1Od2z5(d*d<7x=0 z<#np1CAa`$9qtTN)~J@)NKZJ48)L#I0bRcmF;%F54fiqY=Gv7=PQj<7(I6X6;*Qm= z+=7R5ya5_aR&$#zAvBAlm^0o$3@khW@2!Om0)9QQ6F^ASPS~&=aB5s_96Xck75tN|c3TlA} z)UVwzc!nyx6(}H@4}Ob`8V!UUVB|3zx%nR$ocmiWAtcQTZaGd7_4|8`HTjT44|aO> zo9E3daKe1%vKlg|A(|K>Wfo&H8KRMPF=s9G$AfqKKpqg{jhbxzG^C$i`V#^&z>c3j zy@%{;YB)fxnkY4!Hfx6?Cf9nw$x^f9+wF&Y`ykB}{?-K07uAqLDT~_=5il!)0Gw%p z0XuNH4?=431O4?MR=N#*UN@n?PPIh3e;#%S;3RR~^fk--pEr&Z*BwU!BVDj#FsoHV zqv>z=%|Qfi+?NW|=CGbV2&soB-o9VjZV}dNIQjNH=Y0d5aOFzi1c5sKR&T1(kef$Z zE5mT~J|))r?}ZcO8LIq<3K|IPe?s40TR177k}lb8FKix{PqVvp|5ALK%3n7L#%B+|O=(qNlsk^s34d{)z(QP9b)qgDYf;l zBXPcYu!FI$r#_6i@4kJsNl1Mty=b)k5vZlgIzz0YLyl3XGByE>PC%|*DARwv$^ZHa z)3OX-(#kdp*B?atXX)&A0T1oUcv_7a$ zuob2&x+PHpCq3aoY;Rj_OwhVmKT1zqjZkA2n?TjJJ`g}zV5HK~Pgv01Dx22e{i0D1 znDSTWJ+|+KH%wSTwV9OeHr}3xh_ZR`dN*TB3hbB0;%8TBI{E5ABAiii-s3)7IVGsk1!MfeL81d70(f}KfQuidu~t7(o26g%iVK_^U&^ulg0Sn`Drxfgmqos#itzk`bxJk;YDNVnH81R z<+&Hh>@p|S^G~CTWf$)(ogt{6p2*|eVI$WRyoVivnVh|PN=PnvdL)z?vY5;m*wMtIk1RIkHDqSVIY<7&$s03Z z2PD>;);&k(HfBo89P0ie%NpOuMB`3=`|yG3dnwZWrvTjG~r;TdT3lhAmloLOTCN=x}nSg zIBtkgP><%_;7+gHpg`8kZ*Wz|%vA)V$>Bcf@6IaZN!f6ps!+d}sEG~`#~6Cn5z8h5 z#L{DwI&y8De?{j*rV>MX>t87?L@CKf=}K(pF?K~+5le~X95bn?F051XJ2m#TM8#WW zc-B*FE&0gr*Z}=7H^ouPZ`gn=GD%Tg_YOB48)m6GdFw51IO`6esy^BKs=f2hW_(#$ z?W?m=R||Y~MeggD#HX&S$|^lyzu>qUuBxu;l{Utb*W!+v|0Zoo#H*=2+9qsaJ7_Ah8ef;qkN zmWIGFA1(i_@|N%yQ}ai7TII$V3kULOWq0L9sW*;1JV__**Q{{ITqjXU2ePgiVTOlk zr0h;_D~yYZLds^J0x=F_^^b3A#GCXxl+?!~S-4gDUDb6@nu+17O*<4dPnxq{8kly~ zM2lu)0=$T4%xgun(ncDwt0_vXuNk%_J-S&VCQ2vtNcYR5Pc6m1TxT(=tUdLC!!onD zub5N|IvX9)enf#0yVPI$kT=1?qf zx3pYMY%`NUEbHcKvX)Q;a&3M7ROc+4c$74eKP?rS5UY>U4oNjj_H^Q5!67O8IF?Q> ztOwbeST}OnQ7Xuha!BNp7BnEgQ)7uGmel}#mkD|gJ1yCrIPGf*yn%!S~ zYO;S11$1)+Pnj(6e-V3Ny#c*C;KE9C=Cx!S;FP*8pLui_?o}whFWKHfgtvOwA3*_m zmic0H#E!tnZFnO?7t)q9iUli#h+f#MsBuAv$c0}i#_bRyYT>tvQdB&l*?he%#j%d-qesPl@B`>MkcmNNfp-s5mYU#@>W zZ!D_#keZ1RDBnh+`s^_>rG7lB&k_@?3=Tt^w3{OS(%w)F76l^?_S|S1^7k!1)amqo zzw&23YO2Caacsb7=@jp_)u38$JK~Yn{`lb6UjQTOpm%NLJ;$hhDf{uC&9xjP&nt+| zpy7-l*cib()Ous}`&4B=AEl@;Rg_zk4|MP}j!d4XKIJMpAv4^=KOhT9MB94PXFNlz z@@<&;bIe?muEi$iFqWjQUW~IHP9~{8U!1WSW|P!~i|d#Up7biLm<*26zv<--ITRF; zzxj&S=2B2Z{pMRajmJpiHn8FX zH=WFNp+3Ai_>+wUtLxhOZgzcAni9Ad+8O$t~4CO{?&!UXHsz< z4zF5JXEJb(4$>=!?NV^-?6FM>yL6nFBT&lU!fOCczFrjD429G94U13ghHzwl`=Sxk zCW4ABTCB9O;Zg#zN!8#0ZRI)ULI=Xkc;zK#%^8FlW#wsR_m?})3W%q`*&ShlQBK~U z&CCbi^s=huen(!s%KYLK;y={IQ_P>$^QA_M8m6js-kG*|mN|C{@tyJFMdp<=i2qO) z+n5Dk&i`9L6dTM&1Urs7i*sl0g*xUl1*Bo~zTK6%*rEU6h4 zpEk@mS8*`{DQG&9+?5_{C(JQESBrN$Ydd=((xM4Gs7$^n8(ihhjzgu=`nc zVFc2%Nzde)^u2a0PvcZ>Mm5)(-0>~5uA{(*+M#aMo*SPt+tSa{Qcg^`1^P_%P#P!v zx10r!1P^!yYUisiT~-Prv{hC6P7vglp2HR5qNtgO%t&v?lDf%=1pbpuT;2B(2g9En z#Mj-8;NE|N$JR|pi0(bfB+w=z_+z^72HL|2|8Y>4KZtReS(-x4Kg!k z8ttF?G0d#hCVa!}kN!>Ojz-&N%mSO9Ie3z0ZAo#~&4~f`eNa1Gnj-_&cn{UsH0K0# z1r9AZGzSIb1PqQ_HSZ4iHR!O<>gMHzc zy|hX8Z}+WEeaT7%+IiI(FI{$XTYSkWFRfD^Uz$KtyuH4!_Nv4t|HJEQl~#pkhI;*3 zm3x+u&S&{1CYx^F-Ed-J>h59x@1{Jw@17NuY#sLy-#@Fb+&brxbys7pK625m^sfKR z){u3{3^{j{RMwsJ>*<1B0^(ii%y<5mrd&_C&3+ersl&CBKVutssli#SJ6-4{5;I&h zb2{WwtF@dvU`)J}botBqe^Q92liqhAd`U!Y()BY1h61Ad!MJCE`}Wv`Z;pQ!y03*1 zo)AY1*k`;t+#;S9v@hTBZT=nGQ%78WiWvT7YwJ0ipR$J&w!HjW|I9t){^qU8XF8nh z4j7P(^q`BT;1v-r2EpiJpa)#E5^=g&hm?yCVF^!fzJt ziQh2CiLZrmn}Tf38Clf$O<}fPjz*HWtHGy}t%6D8r;Uy<&*u#bMp5tV&xZ|OIyN@b%a^gC?y{=eg?Id#0???N%IPo1y#})5voTLuH zS@Z=)O-92s+RJnWQUOc!;}u)$`XeWf;eL**Yl&o?!0xv6I$JDOM$839U3juOFydZdZl{sAf5c2+sP<57 zP}OAMKf11MPt_YI#slGc6B&518)=~Gk~!b`+zhQ>YIBq$W8CX_vdy-DEsgeZcATd7 z@3A{-Dr3xb+-2DMD6;w1P3Xq>9n8?fMb9mHakW=%c~gRNJjz!YZ%he0eB-GlFP?hQ zg*O;j9#|voyWo@>rMyvQ{)2sqPjB0cCgt605k;L&JHwSP3e6?gb(h25cFzzw(NCLBnhVED z(t4@9h8X2gOsJzzj-bW)!i=CQOKiu=VxLtGMHF?9?2QU&D^&?w=iBUv2*!X*?OwaO zZ0Um?F83ZrMM#p)P<=V=4g=eP8E!ML`oXIp0mLQ{W~-k*1ln3}wI zKyrro8DrXIbfc};rL6G#P1Qz8b(5#6n~|LJFGoX)x`X~1Gu%!rv>*np$x|~R3mmQDpU&!3Oi@JiH;!blCeFptaR1Jdr2E59kE&Q-mq>eq_cyNJ uI}~)=%*VGOe&?T|st?c3KPS2~#$A5pp1uuAC##%&rnLC|3v{9{BmciD@{_>; literal 0 HcmV?d00001 diff --git a/mCRL2/TrafiicLights/v2/v2_spec.mcrl2 b/mCRL2/TrafiicLights/v2/v2_spec.mcrl2 index 5d06f0d..8855810 100644 --- a/mCRL2/TrafiicLights/v2/v2_spec.mcrl2 +++ b/mCRL2/TrafiicLights/v2/v2_spec.mcrl2 @@ -19,37 +19,86 @@ sort map nextColour: Colour -> Colour; + safeColour: Colour -> Colour; eqn nextColour(red) = green; nextColour(green) = yellow; nextColour(yellow) = red; + safeColour(green) = red; + safeColour(red) = green; + safeColour(yellow) = red; + +%------------------------------------------------------------------------ + +sort + Map = K -> V; + +map + _Map: V -> Map; + +var + k: K; + v: V; + +eqn + _Map(v)(k) = v; + +sort + K = CardinalDirection; + V = Colour; + +map + combinations: Map; + + %------------------------------------------------------------------------ act show : CardinalDirection # Colour; + seeColour : CardinalDirection # Colour; + colourSeen : CardinalDirection # Colour; crossingUnsafe : Colour # Colour # Colour # Colour; - safe : Bool; - emptyAct; %------------------------------------------------------------------------ proc - TrafficLight(direction : CardinalDirection) = TF(direction, red); + TrafficLight(direction : CardinalDirection) = TL(direction, red); - TF(direction : CardinalDirection, colour : Colour) = - show(direction, colour) . TF(direction, nextColour(colour)) + TL(direction : CardinalDirection, colour : Colour) = + show(direction, colour) . TL(direction, nextColour(colour)) ; - Monitor = - emptyAct - ; + Monitor(status : Map) = + ((status(north) in {green, yellow} || status(south) in {green, yellow}) && (status(east) in {green, yellow} || status(west) in {green, yellow})) + -> crossingUnsafe(status(north), status(east), status(south), status(west)) . delta + + <> + sum direction : CardinalDirection.( + sum c : Colour . + seeColour(direction, c) . + Monitor(status= status[direction -> c]) + ); + + System = + allow({ + colourSeen, + crossingUnsafe + }, + comm({ + show | seeColour -> colourSeen + + }, + + TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || Monitor(_Map(red)) + )); + init - TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || Monitor + System ; \ No newline at end of file diff --git a/mCRL2/VendingMachine/VendingMachine_spec.lps b/mCRL2/VendingMachine/VendingMachine_spec.lps index deea8103d4809d1bf5fb5e13deaca3a76ac2b944..d73c6aa688e2869a73c135c8399a1b80f8c8c56f 100644 GIT binary patch delta 15 WcmeC->*CvRf{}^Ybn_WT2UY+mv;?aF delta 17 YcmeC;>*3pQf{}&Q(7<5xDMklY05IwW2><{9 diff --git a/mCRL2/VendingMachine/VendingMachine_spec.lts b/mCRL2/VendingMachine/VendingMachine_spec.lts index a61f92d99b2430d39fd35ebcf996c90a190f7e21..b335078b16bc1cc701e66c0976010bad5fa6d3ce 100644 GIT binary patch delta 15 XcmeyK@-=0{VMZoq)6K^jHy8i_J?RF% delta 17 ZcmeyG@;zn4VMZ2KLj!}&M;SL5002oD2OIzZ diff --git a/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 b/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 index 3027a87..0488106 100644 --- a/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 +++ b/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 @@ -18,7 +18,7 @@ sort map value: Coin -> Int; % the value of a coin as an integer - next: Coin -> Int; + next: Coin -> Int; %nächst größerer Betrag eqn value(_5c) = 5; @@ -27,7 +27,7 @@ eqn value(_50c) = 50; value(Euro) = 100; - next(Euro) = 10000; + next(Euro) = 500; next(_50c) = 100; next(_20c) = 50; next(_10c) = 20; @@ -67,18 +67,21 @@ act proc VM(credit : Int) = - (credit < 200) -> sum c : Coin.accept(c).VM(credit + value(c)) + (credit < 200) -> sum c : Coin.accept(c).VM(credit + value(c)) %Coins akzeptieren, solange credit < 2€ - + (credit > 0) -> returnChange(credit).ReturnChange(credit) + + (credit > 0) -> returnChange(credit).ReturnChange(credit)%Geld zurückgeben wenn credit > 0 + sum p : Product.( - (credit >= price(p)) -> offer(p).serve(p).VM(credit - price(p)) + (credit >= price(p)) -> offer(p).serve(p).VM(credit - price(p))%Produkt anbieten, wenn genug credit ); ReturnChange(credit : Int) = - sum c : Coin.((credit >= value(c) && credit < next(c)) -> return(c).( - ((credit - value(c)) > 0) -> ReturnChange(credit - value(c)) <> VM(credit - value(c)) + sum c : Coin.((credit >= value(c) && credit < next(c)) -> %größt möglichen Coin ermitteln + return(c).( %diesen zurückgeben + ((credit - value(c)) > 0) %wenn noch Geld übrig + -> ReturnChange(credit - value(c)) %dieses zurückgeben + <> VM(credit - value(c)) % oder nur abziehen ));