From 469070763467a8df0dde8f30cd95ea94ab37a370 Mon Sep 17 00:00:00 2001 From: Johannes Theiner Date: Mon, 4 May 2020 14:46:22 +0200 Subject: [PATCH] A2b3: working version --- .../TrafiicLights/TrafficLights v2_spec_1.lts | Bin 18352 -> 0 bytes mCRL2/TrafiicLights/v3/v3.mcrl2proj | 4 + mCRL2/TrafiicLights/v3/v3_spec.lps | Bin 0 -> 2125 bytes mCRL2/TrafiicLights/v3/v3_spec.lts | Bin 0 -> 5244 bytes mCRL2/TrafiicLights/v3/v3_spec.mcrl2 | 103 ++++++++++++++++++ 5 files changed, 107 insertions(+) delete mode 100644 mCRL2/TrafiicLights/TrafficLights v2_spec_1.lts create mode 100644 mCRL2/TrafiicLights/v3/v3.mcrl2proj create mode 100644 mCRL2/TrafiicLights/v3/v3_spec.lps create mode 100644 mCRL2/TrafiicLights/v3/v3_spec.lts create mode 100644 mCRL2/TrafiicLights/v3/v3_spec.mcrl2 diff --git a/mCRL2/TrafiicLights/TrafficLights v2_spec_1.lts b/mCRL2/TrafiicLights/TrafficLights v2_spec_1.lts deleted file mode 100644 index 3d85ce2cbf33fbad8fb6d86928d6b5f198a09ef1..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 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=k0kPHnZc4M + v3_spec.mcrl2 + + diff --git a/mCRL2/TrafiicLights/v3/v3_spec.lps b/mCRL2/TrafiicLights/v3/v3_spec.lps new file mode 100644 index 0000000000000000000000000000000000000000..7165696640fbcce083b3aed46e2319c1320fcc59 GIT binary patch literal 2125 zcmY*ZYfu~472dnMdM(08fQ^zOS70Ga7&ck~4kosdv0D=IbR}y2K)GS1z7(t*)l{$Yz!NyG`00TJAvr!2F zil`8igYgkwHVb#k(H;&)WJ3jUH<~!ERe-!AV=47q`%A9`QA|U~IC8mRDve4ud-wpV z1OOw7fU;Q#2{91?n8^F#6$eG0m(j=hP)Hbo?oM_X0iYfJ`VpX!qZ>t07(q7z4F*b! z6wXL2Tmv!j4o`NWa*JJF)Y-d-c@6-eQOneNa|Tu*NJG51UalwtvcP(I$SWHqA4XC1 zC))tX+dJ&?cL}bDpC3ib%bwl*Q&U;_7ITFat*ok6s#Uo<_3t0}nTPcU4u;VpKt%Xa zSjrqTBFYB%CkF1x64G))*atf%_X=K)HP?6`2PmoB;>ayBqb5NJL3l9iF?bCQ%gsZa z3@fpX!^0uefEjHRZlp*XPDj@%v}D<+=l~mv@-V%ch7P%0KM2K2fDs1TNYqHG>HIeUe@9}WKl1R=b;#t&+%{=f1S7oPBl0X98@wmGF8>;)kZ5!5tdK!6E%BI*m+|Z?UT{;9rh; z$7bIxyiX)XdXOz@{C1@d(M=>wg!`>T6GJoBR#W+3tL#)7*EsaJt7l^|J~VmWR6aqN z)TvqT{KtKiUSeGM!1yf{Sw1)AZ`^d#F>o`_+@z!3X}7t?qg(sfZeO`-&Ug{vG?gtR zrybqcORv+k{hGUKdDW>ZO?-dbwsfQnL3D22vG?&Lf*q?>wk}&0vBMfIQlRY|Y@)|d z>td#D^1@=PJ5j;EuHSD@vB=%YyZ`K(LbR8jRpYJ1xBVcqi7_!(5vyy^N=?uubKS|~ zCbwIs)1{r##hc!QYx)K;b9zb0KwdW>*59OB{!my7nL7cE0`bm#pR^Tmp8_v%`o^ImHH zta;VF`uY9wZ&LHWsetO*Xa6o+0p|V92f9C7TAjLHd;FP&zZch3IZS~+`8^%tLtO(J z_>e~!az20c;E}Y&FhZ}f*7lBHd>g*8VrlCl^c}wp*5l5?uYyPJl?9%w41BqH$Dg-Z zLxyCyy~>DPL93^(oHjnZ+V)`L4SM=gQQ4jAf7DzVcN@9CO+6yO|565(w}WYVboEZJ zbL`ET>Wf#txNZCBnsv?ks{-{oT?6-BW7qGOcW$k$GAFC|kjCbd8t?B`@M{ctS^L}C z**4m@+sLg|4`(;OaB6{Qw7hZpWct<)``)jUTzSbpW%n7a`MY!BS1qrc{j@Ok zy|zGg_jp-x&H@e2e`7-^9Lt-}3&$zEs~I8j8#H%gN%F UhQFNL@cD%erv{{p*Uz>7A8o~ONB{r; literal 0 HcmV?d00001 diff --git a/mCRL2/TrafiicLights/v3/v3_spec.lts b/mCRL2/TrafiicLights/v3/v3_spec.lts new file mode 100644 index 0000000000000000000000000000000000000000..dbb6758d1d697f14980500a64eb91b8c10420297 GIT binary patch literal 5244 zcmYjT30xD`_MVv}kc6Pa5(FU@Vpt*u0tAEz8VJaQ9RdhJ2q6h35)w#)1{WS6SWvO- zil7AvuAo81g{n^xD=xGysMXf~OVz&A(*Lhk+gJNq-a`V8Jzt~N;mBmj#+GP5Z$8y!0f+OQ(+0lZ;)GD z$4E=GSc*o>hHA7cpc?Ib0%+$%^9Tw|3lJ8PRU8iJN34;If(L30z^G7)FjE|W_^5F`;T-3jL$+Hgnu__}hL%3yFh7JacPL8s;${;iiI-+^dkqv-$SU1)Un=QfO;6cz8bOU`sge09k z9dTw7dhy@eXr8|ubj`mUbg_9ly+mK36DMobO1(yl9*s_6xt)Y)Df*N_I9zIa21p|5 zPz!QupJJvydobZEjkh`^K1fhiJ{LcQ4; z$CIKB`k*H$))b2^wa9g1m83|n(upN%8JbtAS4vcK3=RZ^=$8bS%JmYl3_U`zLN1ZX zwdf8AKoa_0L)B{~Y8@J*QH%fjDF8rfnM$Hmi~q)29&&t5;cP}BR3NtDsWmb=52`*2 z(F*Z2W?>P9S6rc%iYv;{mHvJ+@s=ZJ7J)R7HlJ64K0C!qwOl6F&UQ{Itx)NeV#(~U z6=ZL@ctJMkUZMp-6fg}WEu8I6g$Des7+s}KFE2&g$OpxiMv94^00jULprIFN1aRyN zBs!@Yp9L&A0E9TzI5Otpi$Q8(a>FV-<63WG<`Urljlg0eB%|U1xPb=~{QP(^F`jg1 zN0|QHg)Q~MlY)tLtwyS!LmxHMlU_%FA%>G{hJ;F?2h_zj)5jNtYp1CmK`jt#TX2q) z(CS&|nbvUFf%0f3D%?a?1=|~iYdp8R^ioNM= zCBksu-EAYq-bK6fgy9TfTT}MJHT0#yb?JUPsZ2qK><9j~sfJG|a)+>mPdqzTW!)Wo z8LaCYKNzfTl09s@IM2I$x4tB-y~nNWGtSMjuZLs%%3k-pm}=`Ua1H2Mv~We2+RbZE z!tN#8n0!)1=(ic?IYEi;jgL<_j@;_oo_RZk^_yy3`O`H)Y(FtTw>#A7nAgJd3u{9X zIC%9`QC5BS&<{C{lg+I?%n?oY7b!D!9n<;8Hop0t{Ur8{^38VhEjNd|XMI@+7n$VzWIAk1 z*(OW{dtyePe$D`+%Gf*%`(`JG<;O0^AmlP;q)%ZSEml#DVL|8}w0yu)RoTD)3auL17Z@L;WDKV(6(omBCo4zA4iS`8BEw#l z?2dDoHo8)A1I&_QI{k1}7JJIdt;kX+3k)#FjA<7cM1`1;q)tLY1CqGCnBSGM1&5h1 zMKNcA^R^(Q^;;M>!lYX;PEX2~GL$aDD64;?ScoWngzQP{8mkm8Fh(kE6ztHAB{a-M zO8w?6kXyp;5|yYT7H%rVIH+sgCe_;|@hr@TyAtA&o(W7(j#tHLS0`Jw5y7k3Z!=aa zp1NYZW2(J1E}|$Exqx6eJ(V37ld9Nk)j^q6-(bSGn==)mk-QOW+}kz0+BgrMd8-18 zRc(g(WthEmvuGe`vtpW3)`95}zP`*H#6ezIjz?U zj9K^`bCbbv&5FGUH%w&Z7)*{oVX>|TbFyNMOP1dnHXm7|=p)MBVp>>u2h)_vOw;TF zM3`2<4uT7~Lxt<$`)L^Gxel4;trPtMtkO^aW1FaHWgiqI?&JRWK_eWbX+(mpy1+&* zEp_k)mRtYJ{K1K)4THwyWd~fERv%#WE!ggoymmX%=ewPKKfY(!T0@_0k11r+g}ay! z4K2T5`Z4dqOul<iQP^5bb84Nz zNsm|MFFwvr=O0%HaVKl6eEyb`wNX(gO}PA%<|WqNX-D5-Jd$2|)O?>c45ud#SK;i3 z6(JRSzqZEKgzh!H%GzsgqmJ&k>TBeqrmNng=E}GMm_QgnUR4f=7Do&yj^vK$U%8El zq{#++*k-OL9o%KjdA0oDgdpgk**m@SR}9lHcIcdtN;-|tygJRNqPtwA zU>Bpjs!P$hqTc0MK|NBwsGdzw*DII-XF9EU%2Upm1oO_Ab?bM1XT?}yyC&MQcbSg3 z96xBy-Bx_u@7y=RPvpyCb7&r+#~SDE zPN?lJA(*%N`*r3e`c25~{ESqcpV>add(f(p3%!kBI(eHnNvXH37$qzM6(wsX#DRqALl;vy+O?DnFwI??}tsvKK2_>7hW|2p2shrM9 zIcFl&oAbmzjx+ipfzljWNqM(5g7RcjE@gC|n?3f%0bqNj{lq4wz41Q+7WM`KkWv!M z^kF$`CO(MXT$)aQXX`*W?UT@FE_%`GtTlcZO`F&U(q^t#Mg3;Q;#WjXTr7w(U0)Ps zzN^MzZw)~28-SZQl!7xk&BK`=t@m^}6y{mAHrtcUckxsRi@ESxA1?H-Rb2K08?M5C zBk1D91rfdo6!k9z75CRU!u%zURSOavMZ3w4iV$rW+#eidtac1jEGx2ec|^BE zgfVvP`;Z;??B1+EOmp9)v>e^ysSfVhet6I~S}WgM8r z<{*Ejao8g;hg(qy!(N^+(!zt;5&%}*5v1gvbH)R)v2mUbdz~9e$+@SUAx|gHxkH0r zlWGAHg1;70d^iKHfm@ubGlgeL>m=xl*#W`Ftt|d6jdb}l@K?g)oi#h`e@-MzCW(6- zK(CaDVdq*;KjxuOIy)9mi2QCU7Y1(nE$-FDwEoeh+vwB4^Y(Ol{zG>VMFcW|6Fy&k zxuYnD9!%dweD3jx@saOWcM`ufI6Bgs?X=QKMvEVxPWOj*U75@fXmyjaUaFS|zk8&+Rb z-k#c|9y@+u9WT8tdY!DHA3p=jeiG&KmX2{hSGSj~YMWNRI3I~OLQ{Koi2ZNE-bIea=OO|xa4h1((8o-{;j`qJ-nyL){k6{f zcjO%PYnVW`j|T|$oKC1-6T4yFx|2z5!>abnN64*eR)&%4<(PVHG`-fiR8V*NrXmI3 z7~c7qPrBUa)B1n@k_fl4NLxmYZ|j|7)8PxoZ;Cp2etq1!SKQ7QS&eDOeeT^mHoU}P z{P(=96yKOH_S_N;jq?(nx-?maesWO>Yi}=nr)SJ{|E+8z!<_FFp?(nCPdc!HHQMWN zXW!W2?pp;%2z%n3-fE@_PubB6hql!ms%cLXIMpjTO)-?gB5r)Iu|4)~UNSpyjJV&w z^58n6x5t9I8+k0d*l2&a$2Z}DvZkC`_c(9JHE@jmv48Rr!nnwZT6+4<5mJnHX#F;- z7m}RS_i*gj#qEY&0%B^`@S`zf0BP?CwP3`@42u-+0&EtE}Z=6hU_E)88MvN~#o$0Nc{PcaPxpB}v1?WJ#g=vDsxnPOLd+-D(SgOfya*Y)D3dm9To!oT`b$6MUG z{QBX+mheBGyv`1AyzZJ;RZJ*Cp6yU9y?t@JhqAPOC$$mx5$mvNEFf^W_q>_$dgN#FlNA~Ifxx^q#-V3a?}Ut3BQK9W_RjdFgHiuu$;g9Ik6083Q4wXe~ literal 0 HcmV?d00001 diff --git a/mCRL2/TrafiicLights/v3/v3_spec.mcrl2 b/mCRL2/TrafiicLights/v3/v3_spec.mcrl2 new file mode 100644 index 0000000..0ee5f1b --- /dev/null +++ b/mCRL2/TrafiicLights/v3/v3_spec.mcrl2 @@ -0,0 +1,103 @@ +%----------------------------------------------------------------------- + +sort + CardinalDirection = struct north | east | south | west; + +map + otherDirections : CardinalDirection -> Set(CardinalDirection); + +eqn + otherDirections(north) = {east, west}; + otherDirections(south) = {east, west}; + otherDirections(east) = {north, south}; + otherDirections(west) = {north, south}; + +%----------------------------------------------------------------------- + +sort + Colour = struct red | green | yellow; + +map + nextColour: Colour -> Colour; + safeColour: Colour -> Colour; + +eqn + nextColour(red) = green; + nextColour(green) = yellow; + nextColour(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; + +%------------------------------------------------------------------------ + +proc + TrafficLight(direction : CardinalDirection) = TL(direction, red); + + TL(direction : CardinalDirection, colour : Colour) = + show(direction, colour) . TL(direction, nextColour(colour)) + ; + + Monitor(status : Map) = + sum direction : CardinalDirection.( + sum c : Colour . + (c == green) -> + (direction == north || direction == south) -> + ((status(east) == red && status(west) == red) -> + seeColour(direction, c) . Monitor(status= status[direction -> c])) + <> + ((status(north) == red && status(south) == red) -> + seeColour(direction, c) . Monitor(status= status[direction -> c])) + <> + seeColour(direction, c) . + Monitor(status= status[direction -> c]) + + ); + + System = + allow({ + colourSeen + }, + comm({ + show | seeColour -> colourSeen + + }, + + TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || Monitor(_Map(red)) + )); + + + + + +init + System +; \ No newline at end of file