From 3d33cd4f63cc8bafd756f8f39a73be264105b92b Mon Sep 17 00:00:00 2001 From: Johannes Theiner Date: Sun, 10 May 2020 09:23:44 +0200 Subject: [PATCH] fast funktionierende Version A2b4 --- mCRL2/TrafficLights/v4/v4_spec.lps | Bin 0 -> 2247 bytes mCRL2/TrafficLights/v4/v4_spec.lts | Bin 0 -> 25171 bytes mCRL2/TrafficLights/v4/v4_spec.mcrl2 | 4 ++-- 3 files changed, 2 insertions(+), 2 deletions(-) create mode 100644 mCRL2/TrafficLights/v4/v4_spec.lps create mode 100644 mCRL2/TrafficLights/v4/v4_spec.lts diff --git a/mCRL2/TrafficLights/v4/v4_spec.lps b/mCRL2/TrafficLights/v4/v4_spec.lps new file mode 100644 index 0000000000000000000000000000000000000000..f9c31e45d4d0760dc355111bf28572fdc0abd74e GIT binary patch literal 2247 zcmZ8geN}13KH2ocrGA z_rA~j{GQ+Mxk&d9yYMFQ4$@<_J4uJZ?x8HS-Q`38+wAhtl~%yzB7)T1vK>3?Sx$)9 z5Fpr29dy%gwL0uxx(opb0us!$$7i8;xSU>$!$H{`u5e8vzyOX@q?bkj%j@znnRo}q zgp%z{YO4hvkLS5OWvG8rz~Td9-G;nvI+>;d#drw}ft8B^3V0kQY@qg`C;%XVy~E{j z`8)`~Jd_m{*zchzhV)yM!{O>c05_iOrY!IdsES&}VgtFP|(=#$R%26K1x7bMMe#&IuZ-Z(JRwCAt#zB3wWPHU z=HgWRV${A50cdtMe3X_#j#>*W@=SWn0ti-~nviL5LZ;S$jOX@n0(y{#stNdK!}j6# zfC|6{ID<7l2Mqxr0K7!4501w^yOXlEdMFawiZ{d;meykMwL?1lNQW1iE_^0SrPEHM zX&{fK$%8f7TFXiTR_TN~!?gH{)sibwd=(hrm*TOv`{E=pfT8LfB6Uye*=$q$?TQ$AQRGJ^5jk?g zj}Ie@H!?#5$e_P41jffF5gv|g6aCuM8rJ9&b-0 zYhaR-N{HKfaH^*2=abZ^#su^>vE}=6ctijfjHOJHdHJ~?i$2;Oge4w7qbzD9pBhxPiUQKSFZ`tOKEtp(Chu5Q8jpsJYN@`c$fnqSsr`snPK zi7sjPUEB0U$oP}#r2r8fGxkM&!vmMNSMf{S3uN|QyMSn zG~@d8bLmsFr;U@E-{-Y7$V!8`wL?eMpI!c5{rEt}-e0GvOtz)B_jJ9dED7Bgq$!Sf z_nUH5?Wc;>cdm3_ms}5|=&lEng`?X>e>WZdB-l@%{Y#PUZ^STL!A;G+Kl5r?DBSNz zR9SK#k9@wCEc}D=kK6Q*V&~E-W~#@w3}!vK{kZ$2;XfD7Oxb=${9-zi8}7KZ9GvHM zpP1o%cxJ}-U*cEO;R{!2)y?^EY#oxxyFK#4z-}8K`^3LLVXp0ZUD=A; z)g{OtP6@JmbI)thc-+ z5N~6PoNP||^zN+nRb(OcezJ}muuen_mQ&mENQMcD%yIB|JCRCKMn=j{s%%K+pXYrudZZCkakdcW zuj?C^m9R5CF3oReR^s-Yox9U9kXppC*vU4yHK703`kDa*B6F-I& zuaB*<+n35e_3h5`flC@R@nncJfRlA7=C zwB38MFc3B?F=6QnJF*fJKMuV&F)eNP=NO3asW~HY`%*EH@Nu#T5MXt8XJqWo-kFp5 zKYJy9tmb58?fx8AgNP7B-k1@buwi#_dO~6@tgB1WH!y@Pfpj55$PAzD6e|c@+B>DaQJ|9|T8k-Gf<)a~Pw=^D#({`k`^mbcW4 z%TE4y;CRmVrB@5ArpB~iwc5cECSu9kljG8NB!=zWk-YSzYk(*L4Yfh|KL@CT7W@w) ze0rfRi7^n_D=sH7Ygg>f^rhEap^+N0ou3%Dbe`DY^rb8g1bAforx3d#ZV4_$pMGMI z?MwUp@4;hnO9yYVboL%L>3ep??oNu$&RKG2$EL-_C#Ge`#-%4LU1ev^&bTy?!9tMJ z(mzC8>$YUzy=`+si^45Xit7Pm7! z_J6V;U-`I_kxxb^*vnfDN#C82h`>czSgMc5$A6c`_S+M`G=5TCTK3WlM;qC*^fFA^ znVy&soAqhW8oTzSRKH3ni})UK#3r6SCF1imZA#)%v;I59#{CD6!7ypBIcB399^ z(!~&w#5Y73!#0p=h z%4FTn2dQ|T(^%&(2c|XAHk=yThKDwQHpr3b(7|G(zzVnTFQQls){wYAS`~)|JV(ll zyDsQRCTj4J9dHRK!y+`_Gt&|kh>|tPy%%A0gq1J?D4g%s>01ca*y#-Bj|4{%h^T6~ z=-VWXfOQ4kLN#1JT{ZI0-riFo)xT7eqKK+s4cTFf~uq0-QL9C_-x4mtu3 zmPMk)p69tD9oD9Hj0gZ7wW8%+r@VnUNbk0m4`Pr)m=r~iIXV>v57&KF_!r15U6Olt zJV=9FS7JB^5Dpi&dWYcGECvV(ps;S5tHZ^K1*j6{ zNRWZ($%J%Is{iw6u))k?gD<2jlnmuXOBimLKVin!zXoaxRO-7~0aA(}!SG*>Uk zPvHJn)qvQS20`R^w<*giwYYVj7UMY9(_u2IqU#jp-7P2_??0wHhN>L7ls{%kn8Bm* zzMhy*4;U%+y&1&NBcC6oqAINdi!~lJ*-hrtHa%2D(J0zFneVI9eYCo2Srt#oo*)vr zRY_b_1zEInZjMmx$oKB)EUStw)~=;VdRR%1v8YOCMF5(_r9CXmm-HT%FhVHZB%kq5 z^I!z;Wu;&hD+EMdl7F9V!Z&sOSM4#*TC~@#btO&LI?y z!IHh4`+#GSDCB!akSY236Fff7n|*v2THl@l7ML{F$;nkR5QOO!<=ihR?Cd+t<7rWT zn72WvVU`UxZAVZgKKz{ThU6CrXpz$@PMy|7r_<-oxO%sq1{t^=W}eK^mx0Jd!%r|) zl%Jt&9OwB^A}+8|wGDo-{BvKbN-bQyOd zTVNDYtlS8M)}o{VOf6D*mu6nd1I6T-zm1lk)PQiWb#XK%tHjI#?FuA;Dh%E)XzwRw=nWls8Pp8FC3(U@mN%YO{pL13)9?cy~3 z1_W65Xy$&ebQy>o48Tu}o*(Z&#gibw|B|dUe&s3t6hUUID884~(G6G~Xf54+Ed|u6 zzmkCk#)YGS+l7GOgH6SNst&!hzVB^!cO9MyORc~FEf%iy6O9LplY3SWo5Y`5Ab}pG zZ~#wil_XfAYJ7MYSEDG$rXqj5dRfJ}?dYjXi)N|~sx7Mw{gAuC`N^FtiSx@UD++do zqS-2rw~~L7WANdXh=yN|Tg8WwdQ_zc-ClQ3S7yNa+mdeR_jLldz^H$|GzC>SdQ<)h zH^IjrlUvXb6kX1DCE|MK7Ze?$Whp4dZH(uN?{@tbbbVRHqIi!I zG~@T5x4`g&mf?Tsbj^z2CTmd@5tHeCU+VrR>%s&@21Gkn41XT&m+#*9dvH1Ef|}JS zKRvf9nmv5nk_n1%16zG_5~|1*XKqSRl^!Z-$q|A zt5#CB-LuM{t@y_3I#8))yyxUR{;;-U?BO8>K*qyFj|URoZ!FK(W-@@n%!hZxgw5c3 zejineKOv}@Cq43x0?pRQT2U2F<;BgRjv0kk4c4G4@|9Okclqv*n4aYtsLBCD4-DTp zo7?%D-2_l!E{de)SMbEy!nWffpX3;Lfs5qS=Ga#JIZ?N)x<>T5A5MG3x__Oztb*xZ zY!39z?cZ%DMOBiOlwY4%l~aziwxTMWD$ln^P-PU_cfA@_5%I6w?(yAcnD^y4ROM+n zyhRu^?bn@tY8I%V_lR`Y6kdJyz{%s~m`@L!>OH4t@`Fz3o%{8uYUNd;=K~%OVnxpz zEvqo})NLE5i+XpTYDHB7hV=9s8v>>7vP@RM?Qsc5KKU?mv(WmIsuCi5e4J;&++q@h zDufhz==R`(qOP=LiKBGYdK~%*z^tGYpE}+$i1fMy;X(*2ZWMtP`RZ6vQLy{HaoH%# z^a3ISbca5D`{#azZ9VDF&0M4hyfNs89D+d}qb03Ad;B#Ba4IF&b#Y8BwB&O2@TlX@ z~67dJCa)OOQA6tkc1E4uO+1mxS)&J<%W@uvvdmnPL5QkQ^~Ll8f|ZATUe)H1Il zE|o!Up?_6ZUmIN)?Q|Y+Sagr|B47vH_GR+OG__x0yjA=u0X3&c-)vu3AwAk5l4be+ zSh*Sj4GmhM7hW|EoLUp({B|#M-ew04@GwLAHou#{Om??7FubIDYV^=4Y_z3S%A`ya z&YiFzDD?iR>Jd;+9zL~J=tL`KrJM|;w(ZJMp&P=_2zt*n%yFf?KUkIU>rd`bf_nH> z3U~762dB`c#)1Mn=Pge60Ecq-FjJE}32p1szMrn`QZ%NCLE@sC)HT~&gI{t+Bnv@) zyy=Dj9-|jJ|E{Xo&O6qLmdKJDq|yKnGi%$!9Tp4v+Bcg8NT(|F(G8dr`AuE%h}<{Q zzDh4tenN_FKu_(ItDyVs8>YOTq}C?P8b|;hb?&6{%;xuMQsE7}I=}qH4mRKrG|v%q z$W249PgSA{9A>9Sw6fit#k>=NPN8ESHxBA?iP6`OyY#f*4HJI?kRVc8XG$PUNV}6z zB|iK4ik{-2GYQ)%b-be_38t|irfK-8Eh_(p^( zupCcB@RH67eSM@DyVGY&_j7P{?DP@Vjn63NZF|!P#X0?~yNk+ z?8yXJ;-6petu+hM4pk2A4+4k?d%Q>c+_q-#1Q63KLKnWw8&!Jy+cswoW}0=ca_<49 zm<@5##2q&1@q1iHi!toV)@k%oxPjHNG{8A^Tjvq5ytFcOLQ$js+;dyzDL}BzhghL! zvX8ax+%uM`(Q9{JApVqq_BlyUtifa0wS6;uP>O$km0SO?0dqt8Z6i9pVM`->QwFb) z8Ty+w4OGR{Cj@_ajjPec*h>|ELeM^4skJr*$1duc{;w(ksrPEoxiS0A(PdR@qnF?n zZHQHI)MHuIl#rQy%~zw(Zf^pra@3Vxac~wZ8&1q}0(_|#tLQgce=I>2dRSwZ=s(;; znH4c#!wKQ31HP3?*4{SIib04{|J}|7%F;`-Qp~3Zgz?D)D-6f*;+V;e!SAK03WsZS z-~5NWDT{QONCPzvx(RWcu5rS8m~SOJrNyyU2icNupHV;(epSyk%*)ZZQSke*p+?7T z3%qV7=_@C+RYxmGoN9U?{eqzvotgA%8ih}>nutX{TZU$9B&{M?leT>bG_u{DK zX)v4DNk~i6`~g|eK$nhg!dD{3Y+C}6=C1Q!RlV;s_yhCCMM-Qa zDAMQLTO%dNSj;~-J~V)YrU^004&sjP8~9xDCj<$$N%xA%Ny>v>y0f4NAKu4#R*=lR z@vwBuvWk0eZ8brb%F4D_O#@X+s`La)PDk(cVt4T;1PRQg=Xqt2@{p&_vWnNoea3yO zcB8pr+p^04o^uUBa+sMN=eDdOCu~TwDM;(OQ5=P;7R;p{8BJv6{?)p)KIF+D!|le) zxBklt&OPsAMA;WCrEb!)!Z6`8u0#IIzMFmxK!HK%K?vs4gL1F*_dfwNJ;~$96ndeV@`nGM7?f`alx|KwsgYITt=EdG z+>dg0v`icJGNrugx`uk6HL{TqiRfzs!=Q#yb< z_`g0vtC1b`ZKDJ^-{=|iTiyt4eHTy3`V_hGIBv(lH&@q%?MDuV+(;F5p;qnj#{Ys`)r&GYwT}=U?m%wQlC|Pd&bj zPUD75JHgzV&UqmD16i z5>#PWMQU7KgM8&{J28iV?id`a?Js})I~U1l3m{OgL@qU^7(V82XD+Lz2bEz7L0?OQ z!^)Rc6{Iq|8qNofEqer2(J`#yr{ROe?$S{Upu$dL6qL<@Ce-*;2C9O&aL@WgGb4Uk zS^=suA&{z9)n>+VZIuhC>H~pQ^rt_JcdQ;ASXLo&ipSSfDt8A92axtmL1)-wo`_G} zTDh#!Amy_Ty&6Dlv&K=C+>G`1w^#_j&U{2BQ_SvV&_K6Pi<-C5CcmJ+>@hEc|LS5J zs$lLX9bHpRv+%w8nn7osyUaz8S>LyKjp2=Ho_zKl#e}-`>(%HKq?W<%gOA6J_?hp^ z$fPP-1PuIm-VA4$^wx`YH-A0Gf2|QSAMmB$<|?-116NSfc&(^HtpJ8ziY4) zox+DuUhgi*(B%%7BM4}G%VsrH$Ey6DO_&fM7;$_Jx?*nk|5}$CmfZe}W!FI}Mhx(V zJigQHNm6-<7azHe42S%Sa$ATsSGHllzqhU(%}8GB%CUU@2jk3*z<4m z&rSpG@qKv{Q!vow>mL%N#cF>ZxBxf~f5p|Dxk#6{Chk@Nq@zt0gek@+lm}|R0|bM3 zgoweC60STO6jJUZcn@Oy^D<80b(#-rq}Uf#8lF7iq0=tLDXjEASAi-Av)Y9Cj$bBv zDg`_)zdGdbG~kB$AyT`@3}dc8lWxH(eIi5^##a-a%-SWxa;v&PO08c=>swH-T}bIH z6E++0b(zPDLke6Y^8i=NyoUtHKiIJrru-pmAA?gqfMciWiovNJ*xKCavoq3uZQ)A5 zp#?sFX1@Et^=9vIWYo7PMOzFKV-Bp&1AhCh-E`Y!RQZtW7b?K>D78^Z9W$@HH70|Y z{J7{N(|{Y6U$10^Tb$w)r&L+7#(#}OH$War^fW&un^gGr1`=zNHyqCe_4wJWUgFgI zXnu=lIX0wrP2@$u;f3?ulKEs!mgJ|{p%ZMwQ!#);xn6Sa8yADxpqSSDi7xFa2f#5G zWB3+-m1&0*tqVttks=dAF-XL$V@(&X$0d5{Bul~+g__wa!1Ii2GvZniWuJztnGb&; zpm7>-6Vmkt#%WMC9sc#?33lC7SwY=a~bOUMySxTbo`xShS zO*#I0smmQN;K7HV=cqNwwOOhkg#J(5O;XzP6xj8`m9?Usav7~av)K?@vyeo~VL zQ(`}vf#<3>?H7Z@TOEb?kM)qgMCJF`^b-MNs_9+L!^j;R*e9Pm;xV8bOF*z2CJ>1=e~;1z#U%#g_NK>G>SZZou%+k>7CwC3@AI;s#$pNqG<1B9PW>08ij{*wO)DkI1btDKNJ-+gL7po+I_#aZOuu&e8w zk%TF~gbmaaY?36Rt=a{0w%UpxjfV4kJztpq35qbymlfN#=c!Gm zHt)C#5S;l}Z+2zS7XF!6XGH)Jzn`yrMt^JXp4u(`t8(}Rjt4CbaTeUpZdouO^#0V z+XIg075d(f9K)r48}jp2%{7Ue>j8(`E#xm14rVUf>XK(ly8BLt0uBjy6Q4~T$~URH z-@h=#xqHW23=(pB>I0LXuW7E`9__BH*p(Wu0z5|Qvg`Ej{D9uxj`8G)zCG0c|B6>j>LYtlWLo&5BJFjS>uJS_Y+A^)VZ^QAM|Hn)V}2Q*x?$|rg4RZtJN`zvm#$4GnjN}d@3L^^KJ&o*bd0A0eTcI!_0uX0OS8vqErD3sp{6l(NrZg_&K@Y9jq z&gRX`iKOkvtD-9(=2W7kuUMSJRb#HHKV<%VZIx%7JF39CyDGwLzlM8u7R}8@_PQJy z0`-`SCKD%XzAKKdoyf^la2q$oi9zC$W@?Syl>ce=F3%D`AlV-I`fo_Yp5V$^bPDbK zJ6%rAjHC&h?oJV?A`W^M-PsfV0%;uMhyk)?y!gdq3fbkg+fxk?Oml?dz%!w4PiDb1 zs?un3>s$K0ht0%Qa+AjWhTESnf>PYT7GIOq407sm>+i<_(!=g@NjNWCB|mT|7C})( zPq^}FL7&oXE6;5rfOSv?I0d?2dL@(dfMaszkr<%lwW&kGQQWWYN$2+gf^FWW(D=~> z+Y{F`Tku)Wnr+^ILxR;4C8qmjATr0^mkecczU7*v|0V_~$04zj)~_l0D?{W zN3PLNQSaf@&lddI>Gsn$z#)OpgxZ7iBc9@GnK=OA!~aH%etYKl;-78z(2eOM=Ia#S zHd`qc|6_}Qs+fYDua3^mYW4s4lR2u|mpSp*--k*)k0A@os^_-8b1SNJUR?5hgsKd` zF<;aEg}bkO@!;BJRb@_0_1rI7-FLiq{hw;zweKoD5Bk080SG^5%b7d+f$-v|i2KW` z<;;eziHo0NZzw@$BLZDoAdZxbY1q3s$Khbnns&=79_=>ZM zyYq6i7$oE-FAl7E_-vcgnZHs1f!$xoUDjzLAlhM`6Y$M%=v3;Q^v=omL7EdL$I6Kp z3Pb-8fFeAvAKCfUy{Z>)c2DsDGW+ExpVNQ2KTu45t&gg*kLBz;_~e)Le&IiLpa>eX znwbCYc;SU38(*U;b&rF-r#^hpdeQs!?Pb-Bx7*pj-+n8f#1t>9Y8Ru$`m?`v3$Ra6 z)jsk>ig?rh3kP@_ng8LOg0jRQaS8uoisqs6_H0vg->(pg@1csAg2j~1l`|`PBe7=N zC*-s+8K`&Q?5p!5Eo|hr=YOz!QOEN{r!bUVV$0RtcgTgvzh;Xe4f+gFPacoyihwVM zPB2B;#rul4YSaRb4?l}2@~L_+o)9ci1#SlG)q>Amqo}3*Yp|HrwgOeaS^0f}!sfLT z*Ck&c+}9XFrUC`zt{SrA#9&{XV0a9F>2g}F9B{0Sw!BXEjJU|Jq@W6oCLd*Z!A0AN zkj@MlsA5+BRTinCisjf1aK!-Gu6=RE-D%)U_p@pwKrqcK75dZ9@Qd*UI;e`&dbx+k zm8_X4Fa4SZsyxR2st(u4_?c^GktYV|nfi-jy2sF$jvXbh0l~WeF4vb_!!B~m^+o_9 zwSLtZ&Yg3ZAhmx^1IR7)uY93K#&?Ka%T_T!_l~`I=dy0_pLMHCvH-z0i&LMBpEX^~ zyI?f^pxLRZ5oUuuTX}9bN3DL7=5yNM^_fdl(?&15Wd*y?*|s=$JSAb_nVLq}Wh3+q zi1`Cuhlb3e*le6H4Tx;C)k=`6Op)rk?xGkVTej(QuE$WJHzUA(A+@da0s=T)S0ks| zXxgH$-fAZxP&1A_G0ex6H2Iaa0i^CB849W%vot+LaT@e>Wd`yAhZjdu+D7CEh&=T* z1dT@1Ey_byc7R~!T-f}_Ul){=b4yW`+D*rSpzse&(@~PskgtbbpmbR^muk&;RH%_~ z!gM08r}p@mJzFZ+NdsBK10~Xss*H@m;Be{+)3Ox$@|m~}Ijss<%uS&u&my2SOsCTC zfY~oIoz=(9U^b;EoCdfXo@`MwPjR zD@#EUdAzz`XZskRJzE(=1BiG%pgFi~7z9`uW2nsOgRyCsjng$NH~VYxfWwQ_lq(G{ zCn}>V^idVW?Me`XY`5Oh_lCh^LnJ%?WdIEX4*mg^+e%y72TC*N!~i{WHNCxIl@16D zTaJ6$T^04D`kk9Z0LrefOg==(yxnUs8x9CY;>m9H%A$dYcrBnd@Sum$VEL;cF+i8R zO{-(E%}jeYYaZsY^$11`x~~XAL?6#ge;~2B^n~O;ObP zA`sx`8dMd;9B0!RT^qC%_jJ1#)0PYJ*d(*mqTzM~M0&-Q84cB(u0BIO3qT-8H})XK zj|L)-v8xT-Aes9RDR^28P>{N5i=F*{)xWq{Thq3t6t|5dAfH`R$?Iv%&s6G4Ie=g` zq_eqfKK5#9h5m`NTUtfrUM>~Wz~~k+-p9w=d=C&TvP{7Vj)_5(FdT-+>lQ!& zA*VX^B78uAnG0vb^MNW5;h}HxzzP;eY|KTMh>ME2b2kVu_lgdGSY=tPx9---ivVGh zq^a+E+Nfb)Ye~^d5cA9WXC@e#?DrS4RiKIj*&I6*)IuM6^?W0$YM>sz>}{u3v*!Dg zUI4)&cFMcOHiNKONb+CRX!kT*vX`A#@+GP=$DBMUxz3>uyfXfLSw%Vg$ZB;-#M+xl z4*|m3grx4RynqkeO{~cPNaL_w?~JpfKKtUyJ;i z3n}M1+Q?y>^s9Y$DxY@$iIyVf?5%DwDi9IKCoAf2-30-JSsci`w-&9V`5YemVyy^7 zIE=H0>PZ@!5|^ZUnB5YCNQZE9hhB9j2s9dvduFp8x3il!Y=e_(8o!SM95)a)nC+2c ze7H(OPaSd^$RB^2;_gTy-VC%N7N|NOi{^4EW|er2r-kK312iO)m*YbIlSx#|_8H@h z*Qeeap&Q`7@PN2Te*!YcV!te` z)-gvg01R#JPR#B$Wv8WYRRKiOOgeDnRs#ss2Ra5i_d0_B!_Yi@XQQVGM7aEJ&nr*D z(3GSvb@RnhF^KXEZl-EiFJFRluQ&0Js~`g{tYvq66{P|ZQ9G&b*exRvs1Ljx?8IAv z07J(fu1C&^K%|MuW)JIYfB=$JrED%35Q8XB_hu-8hh9pf$)hWdgxIp}TfRm>o}lrx zxRNyo0tn-XbQMzxTb^e0%K%#X3b)r7mDiHmV0lywkPfLR8z(3z?%PrAm_@ny+8oPm zJj&%5`8tnK^~ooL6w9sZ7A~Xuj3)-`ezsnoqYJJdoQXqb^OEq8dY{C)p)iZRi^!LbGsLxd%i~$+JyEmtYKFY zL$sb&S2LHDG_OInHN*CB3B3zdt%Uz@9Ill-N->s}psGCeo4#y5_g!aP==`#39b3aL zSo>*y9jhH6ECQ?8C+M^-f4TJiS4CbIP$wHmeLm5IsuD)*zx0e07x&9<$Wc{|NV#bI z6>M;{hPkZbaEERuqW9~Vw~Q?pwk&<4c}-{>Z6@V;8VR=F<`%;P-D>&8-6yXza+En9 zn-PF~)C{WjGi2<6i6+FF3H(=(~bugl5yyL`4TtHl1j-&~i3 zDSPnY%PPpAUMxqHgSYR}yegX3>ftJ!1LMYTr|cvZh=Isc&3?TFzreq%mGv4B%v_Yx z#Xp#6P|~0n0SGIbRsEpPpl+F`^wR*++F#+#6-dHUPlYs#0SZ&I-($xw^zS>)QUU@w zMkyx~gEbABn&qepqQwtI)G_S0$VuHaP-W^8>dFyFGE>@_wJYp}*5MMsNiu6?t6~CG z3H+3Tsb~a5%%b}8lG8yTz=ul*_*2XGXL8b(>z?OnAf@jg>akHs2Lar^GnHX7ECx}+ zE&D`lY~hI>S<1MEvi1NM0o;dJFRfNAof&U9c~wQZQ5pV*ldlf%T?&JeXE5v!`{h6B zlm#(hC3St;a*JktL74){QiZ!xv0GjzoumQPO8gCIin=EpKE-*k$$N zJ;*@sQ+3Urj`bL z4+6~BS{<2;+tVP@n3?LcGJS~FHSbdn|FT64BEy4`4F$V0K%lmMen@A%9J{48_=E}| zeZN!}?hn&W%+hEVh#pS%D|A&_Br^<@ei0F3P{J&_Q(B%Zvl-A^Uj+z8?!0AiXKT@6 zcV8EGfZ+C3sf469N?M#@a6xa6<=ot7%A##VoK#ZLg7CSNTc0hrvbGd#J|lkN80dC) zxph|x;pqjv4vyCkB7jK8dpm6pJ8CI$6C$RkP;Q)el};9Y;VF`RZZsq8#2Asa;iXmQ`wLpE*qy{Mt9*Ik~JdR^GMc ztM?sVnaI1~yZvQ@{ezA#tM(suEzfBOCD1rIrE9}AgS1HFhcbZFxvP{zYu|5HMm^(; z0W!z+RhYfZcsd~3Rt^XzhyCCt`MaUR9%VTUfM5|h)oJy$6=_NOKhppr7Od(S{Pz7` zWy6nK#Q?1n_tluZ%rqDj{e*ssV(!TwRGNM_xW%dPGxr-QPU(%H5))IL7O?8U#Ocl} z-|ll&8hxIFDjYWS6|R_M=k#6o6 ze&`?k~%ocxkfH)^xF>u^_`SU8q;=$yO^Mh+WD;IeOQ+YAVpH~h>FH^`5r;qe< z_DKSj?Lj9=pVbldT2>FXSXTMmsHH|=*Rl)B#y6$#!oOab5W*U#feWeoZtL>@;(dgY zadvyjXT_SoPXmsXrK?&leeihjcukk;Td%4&3xLC-A5*Iz{Y!b7wf64Jwm#(VT)?4y zsmhUK%YR^S@cpb&@3&j&Ll$46pD&nuM;^58R)|5hvGcbsg@0y%0BiG~6vHj`D)Ojyn*$g$Z5m=FC0r)Z-eAIR|4@=u8#Y1 z>%^r_uG*ZolAv1te*+Eyf94yRw)m)Mg^Q>y$MC^hUb+}WhTnX#j-(}8nL0giAI<9( zzRWXXXMNdUsJ6jDxiF3XZWqH&{PU>Uid&b5RKCmanP+ProFnAT{JjR!ZvHN1`bkV_ z?N+lkF}Ay~mVsntNYGy{V%&E8Sw%5w85kJwrJ`4Pw(`MUM&7f(*W$ICF)u_d<*-?r ziw^>_T3OiMk`f6atMks;0A{_(q$+=KC_0C+w!tVz3`%gb>dsh=X4SkXuBON=Ok)kF zu&a3aYoJh#PL^ZmPg+_fS}SOv9`fL*28J4p*3RW7qY7hZb#HBr=IIwQ-9b=<$!<2w zfxR1i`||gUdGNZgM80yIn z*btQ^Vf>`M^c7??v{l_BZjgIC2VPt1vK`1U#?Jel)T%@a^A@+4pVaK5W`3UR46Dw9 zTiu3yoy}5QRRP(trCP;3X=|leSo)i2fj*=L9^=ITCcAnvm!{6K>c?Rif~;wp4WX(T zhmqYLDx7|1xwbP8Hyh}tE#}S5tHwQz&7w?j1;@J~+J=NI5uKt{Rf$(y|0_oBN{d*N4OE?Ke|8?CBZ;~`l$x6nO^MwaY=3ps4<>E_LH z&U^YwT+q6FMAC)JbQDa`s?1@yNLMA}Aq9)in5ok-MUNpb^6l}rto(f>eZLI1^bB#I z+AYUCit1i5ezw8b$$i`xYm-AH%MwQM;V$sfU`+7_I(eAqF_s}ys(UyJDabQ({A{Tn z$wQg{>SGnd1tRdX|2>r6&~!d5p|Th`51$T!@zAmMW&h z`#l^Xu4q(_VR+&mBY0e4b0-WrhEXtxxjI)&fDs7-VW@ccdAsN+BqCuDOoqh-2Inc# z#YiwrvGXGbnLkrgludZvAvyvvNC+1a?+=1S_?{`pP;m!NM8k|?!Z7tsPl=^Ehzvgs zu|;^7$uJ9FjWbj<^VauDXDj@MIrDAUND&v ztm?ywK0;=yyUldu60Dud2%%lZEzmH(b2LuOS+zl2f*8p!EVDZ^-ORy}Y1D{_0m}lF zA?*|{2y&;6s5=%kJt7LIGC6+Q1{1SB7B^3nZN@Y=eIVxO%MRdZ<}{LyehtsUr@+Vn zv9jsp`r?-UZh7>2UeQ&uXfvj^X@+={B07qnW+43aK}Gc>)mCv)(`{m!p-O?1(2%X` zql*3{(6)*jnqCpjs4^uK?n)zT=gOz#vN(}2H?@sUh%Ly| zpU$ujf{XCD$&oOf68s2(cv@0xkw%sn{<6u!og1bvvb}nl8&$l(wBQp;wahjh;1)e6 zm-1jbMbcJ8hZxim!mAEmjYSAqV(^Qg#f{snFS5RRo|{+n*mfY7q(l9M-(tb-(buuK z+RKeEe#=yCI}lyeOK9KB4I$x9VT4?ou8z&sOWc6sNjr!_4AS2o-ooNG>59v6ZG^6l z@gprZq*8wO;q|rvl@}iqe4h*}bYS={ia}6j+X?}`p0OchsE|nOi zMfY^W?H3|-CchB13_II!be4>NAh_rol6wG5(I2-6=ot(xZnn)Q5`zq_BI8yKp3zg4 z;d6-9XB``7M1h5J`|E|bs|9$Ybn*C(MtLULfTlDms3MCeSZ^mZQEMQE9T$4m~dPp&GOAV8-}>u);{at;64r0d<9tQTba z*JaB%3*g zu-dBI)G`fTJc2ukM7#;{dsSY!rPT^|#Hn1v57|FIS@r|9p=h{P-7h|ZYLpLsKDARX z$;v5}P#H@*Jil1>hh9UaUy!w<@J)bUaRoI@RWX0FtU{mBn7?CcGo{`>oD6SNC~fTp ztp@m&g2(Hl%CE@nb%n6DBFnlXpfw5qyYTVGr~`iX#7AdGYPxonr}>I9S|;vNJ>~e_ z0_ys^mzH+=sDp8+E0EY`a7hrpE`H1)*?Ql(*6=H0Mkcl_jZ~T+I%Ta_Wj*6kV5kV8 zHwO;h!hbKUUGHA+Paz&X%c#%%itM8A9Ug8u`%G_oY5Rnu9qo;oP}!n^w=mpuc9Y(8 zxnBu!#hLa)nNaz|fLY4YQSjcZ_uF6baASd$o)K+dUu(pb0LClR(o(~pHicWyes91l z9X?6??QDDftKjmB0kb&#=K`0Yx8Gi|v~W)I@82`e`YcVCGiR-H9E zTxJ$3@QZ(k4-|xj4)==;?A4ipE6apSSMCmd^VLzF}9y^=k8M6 zv1Z4@l~TV(D00eFuhFU{fxAlKMpuRo?#CY%rmatC!dDaB&fKjZT}d3I?uzL0miAB+ zX!rZ$1FhfM5@LE|hL471ZE4+N@c59mE)*s{lJZX(T=%%&U)N#OCm2I&grcX^DgJc3 z^l}nuPqFQ&F6^q%vMm?z^{CW_ws$lnx;K1yG$I$Bih=#dH8$?g{x{z`J?Q0J-s-eKV_(=PdgP71PhU}lpAFs(zeF@ z_^C~Lb=JXT*k5smE{}rcc(UN(dcmdQYJ$P(bM>bJ$(DwV_}D~q zC$2B;yCq>NR_`>^jum2ph@~mNm-SWmG+5&uB;l?bhyM<~&!;RM2Cb=oc6*z-UGUOj z7#`U4%5H)$?XflaZZ^A3-$oSaiqH=QF}bSB6jksU2_nx=oR6vUIyOM26E9w{5OQF3r775Fc7ugS$ky&@n7&%p+e7h7<5dgz;fvC-4HI z=b7Q!Mi)X9bx%Z@2fLZFNSp7cgd`?A7{yG*&?j#!gpMDPzYl(16V~r1wx&f+ap*Tk zlD4!`D2rApozl+|x>wz%klGD;1;K0B9+HMKJb@T}hJL6qll++4%MW%`;t$;v!>t@H zY@i6XHt>a$@VA804fcJwo5ZHGbm?XdLX^I1c(9A|u1=?Aic-2cVcbR(H6^6K9(9ay ztd`FQ>(|PP^L>RbH7vV<+(9+PPV2}G+?e7w!ifzX-{F5D&Yx{Nv^jd@&Zc}RrZ#_@ zP(y0!usOX#6@paBuLiHLO*@c4x1QS~jG#XqNs4i-mp=_YUA+W@mJU!DO79y@;;KsI zcY=>dUVfWUYfK^O7z!gtSxS#Ok&XP4^z+0?2Z>M^NI!Z#IhIx~9}E7c=H=N0n*LIu zflxR~%fi=*=<;u+q9+U+QMhm;y=8PH#<4*DD0rxvcOKd+%&Q5s^f0-xG*GkrL$KZ< zvxXY&?idM_DJZbIWp;G!zw&5JS#T4|y1jL{aPb zc0O4ibvhQz9zOT+TBd5NFskjz=<4vS5UrwO0B=YCMruB~JA&!t;vxXIy1;dI&+w{<^?T5r?^1l*hNk6ytAj5fz zC)U4h%KB9zIS<7MNz#K3=TnIo-fQ)0BRm`SQs~>R@Kv_r&kLEsUeYH~#H=%d#=Xwh zkA@6PV2Yo7ZzUq(@E!tr$i;)juL)VF1vPu~$T8anark>e`TC2;68(tEvw}l=y~=|0 z6T?sWytXi;Szhnv`#x@6jcl%qY`b=Sc&oUE`D^e->DKoA0HJ41tmV5Mqfu;x>P5TW z&;R1_&vv>r(h9>9n@%~uURmE+RIE*$I6GPM&iTeyp|1xpG9^1twlls$*y! zxzmy~9m!j|KPF1gx-{a0%QW<@!*?=C&J>Adh;kx_`jqY%RVQp~U{SY+RE=oVqG7kFN!`FX<6Y9wvNehj~ld$29PJdr}>b-W{zR_I^hJ@+Oh z3rd&vK$z{wsV-i3<12$Jg6Ga8Oyqm(^79j)Q9Bjyh=dsG75;NulF!nZ<-HT>`pHb( zHvKJa7g-C@3r)=b1mnWzF6-~3AwvDYwn2tQh^UHX)Ry8-?Zs~TTynjNd&o~`NEuS+i-t^q2d@{ULf)6SiJiBWb`O^j20Jt)SAxqQ8WanRoyvcwNUTZc*b(|Z)-=9;P{LDIUXZAW zIX-G1(QtYoLl{>R)!LN>ixflFU0dQG<2izWjq%5xOqUjPR90WXum%k9LSt5Wvw-{Y zd4$hY9=ejwObdc9hR@1mb`mN+!gyVIROEXasgE60w{*jzx%8*fK|ZBk#n3T)x5?Ng z#77^teSMi7RjXW;yXgrx;T3B^Ksb1Pc$Biq{j%=vy5JhR%qh<@mQ`aN95Ne$_Ys`j zAQdm&Ipm!VJ8Ydt7)6$DrXC4ThDy&-y@(gjh8?rkC${PD4R5pv>C;)TeBI6F*HJrK zOi9%Sdxec2A&-TY^w;0AQ)&erE!46~>fVUPRUwZBxwO~)?0~w-Q@S6I@%*MnR!CEL zX}Nz6@!{E6effBorb4FBBHeP!LMnu{GX#+Ih6EjI6BVIRIw)b%e)$S~ zq~Nn4(&?oe>yD0>OW&g_%{AC8yvJa6=`7Hd-zqZ%0=Zv!;>H9?`>F8hg6oe);`uyT$QNk=Q15MinQB=gcVCAfN0}(-i zFJDo-x4fX;ByHMsDM~6?GXyW>OcYSOi<;BfMH?+;me*RP<(!n7YsPfHbglj9-_P?t z@B5z5InU=k=RD7Qq7x$)3!9;_jy`k~JC8vwmnm!#(}?;gBM_OPRI-5SB(;u3*ld)d5lkD3)&ld2WQtOqJQ@IWuGBv5OTg`aXr3 zIozIci<`!DcD)xa_glQ)EFg_vBHtPLgWe;`PZb9Vy&E|g0}%V2U8djUJH8{cmb@a8 zT{2|0`FuYE2`RI{glF3~-)9Nz7=yY~U~~tZDJLwxS8mW9^-+alsC2&5s=CDpIk-5~ z^fu_;74oZ*0LH!2EB@jG=>-T=LQQ9BeYGQ z)Inj7jj&4>ICHz{bQBs`9BFEbG^rrJ909;i=@3QiTCQl9<9L?XINLFR%z;dTH>r{) zrVmuskyF)ssQEZ?_#>92V#uKw5lr7alo}G=S@Dy3v8?r-u-B?YW*!V~9!@<2u$!lk zLjrw;o zjXmkWz(}JgrSCQ8+ELzVMDNSqww6|Jf46Lz8*__`bkRjw>(Z%9>Slyzr?T_AqG4byeJ>hCU_)^+& zD)N$G7~?j%OEQs$2m})9_u%WpvBff*(A2f53j*J!Vt5yW;BGZP#kM}$BVgbvI*g*# zk?_SdUcl{Yfezy^Sy+@0Am9MKr8l+S4(lLqV5KJUOF=s6?f@R+P!eN6#5O6uie8x^ z7%?Zvcl)Qu4EMFwe}Czdk#iOkEP}liM7VBWe^YQ0H|1K!BIw65q$JVuE(`8r-cHx6 ztWO{)3~0MNfXBvGDLw|sMGzdbi)<$%Tro^(J6c1HxQMc#hpTNRc=$oP`Wpfc{=IY^ zBm}{AoN@-LxSWlu?-mg7D~hs60t-IM*%7cL6uibvPby@#dcx_1Ft{Y8AYh3nc!uej z+$x&LM&tm?jZ`<1jG9s-c#kof+!}O`L>K^;?R$*tJ+M3Fo~)J62{I5GoYajw>QI8O zXJ88z-K>>0wJozGEa@t~8Qle`H^TZxLJu zza5I>ZKO&oPAX!XIuz4TuVewikL*k4~yJP+vQ|`n@KDvM&?k8vU4s{p-e6py7 z!w9%t1e?JyrYj16%EQ*h=)Zg{r`!j9ufjGks)>r5$Mhh`CyF*Xnm7+L1PwLZP4@5k z0=*Q;4;QIZUc|bU!~VdKr&cSaM1(gWu8YhXHo|7eTEbPEkR@=L8h#^D2OaO2tY{;S znjoaK#KUY$alDOx=P0pvy0w_ir;El?Igut}*zXwj3`{yiM%V$p4fJFFa4bdkD(Ywv z?pIRaJGuLvNuqnCS3iH$bxW9~e#V zxvVIo@u{Nnv@-!q`LL%L#iXKWA_s967*m`efAC=~>>rHzq+-xL8nG8}ZloI5AH;ql zj|!EnsXM_#q1U_h2gbK^%TFYw-GL7=v|dlP#@W`q-qD!e3F&+cBuexT=c-?d1ol77 zqlLB)?z`n^q`pDA0pQr zQU^jvdvEoA^I;_o%aiY>d2fCw4@d}WMnLPQvG+)zZy{`4DV?g|=buI-Fz!enXAQ?= zhZ~E6xv_j-CV_IfFw+9%2O1!;D0xtr>J2{+B!pfr*6N_!+6CpG5=T4X+W~}^x24zw zX>i>!IwRRGK5jFb`F4e`*E8K)CG=6VUeB~p;N!NgWBy-i%;fgbW<`)&VsvPz2)!42 z-i0juJ~t&7{+=Pmdv86uVEwMwk)1iAD2v%-GuM}|>Sau~uC$!;8gyrAEdkHEKZ1C! z8jr^05br!w($%hHZ6xDNM}H76Oruh~4A7lae=gF7+`qbb*YHc{(XyDFS1*XeUqSv9 zYsoIsOr%YMJMU|aPF5K)kY{dKH58?V03r38?z{sUSYst+;Gsoc)liz2z`!at4;*D_ z1PWH1_er&@NK9^*X3Q1GIXjle>`r5a=unUcVllP-;^JJ%HCM;Vm|P7DafA+94{SU- zJ_yM$yynzgH5YR)!u$vb9vYy|tm;AN=Pu2{x%j0B_z?ia4}?^fB6F@cM`hSZ+UKKKbq~!Fh=@DWdqD-uV(bGsqTd` zcidY#MAbS2|Hv`}c>6VMnQ^q)J^mwcFXb~4`U;|b8T8sh?DeQ@2#cjgQ(f=)D!EcnzlP% zgqfcNdtJ6>!{N5GKc?ocE1inz{h`x8FFp6$@~4|1XZuotjUVdX#rDTezg)Ja&wtPT zSLr$#+c3n|?grwN>H|mdn!WN{RM?EVMf_>lw}Oq&pez^fEC1qGeBkYjOzhURnN>mH zTrtbp`}=?0^%lB>XWDP=pU$$29$Y!K-q;q+>?cg$T0TXeFX3vG|4sP!rXSU^fNk+R z0%c+-UvO=`u@e_7C~or^-6_*xvLU?bnRk$(uF{*_zjldADIf z>NBFlr2GoR)8dy-=c;$uV!t-O&)jg_x)4NZILr zvs#*=Jq64s@9>48{N75q|5F-zEmTXH+Rp)#w8Y&D7|jtm^2z8hzg(Of?5EoE7rHCK zKUi~9UN^I=%c!g;v>NVz%7b32 zf;SP`ZBwU@7wlee*KC*1&+IZ*H;8wTtS@b>ok}z{plk9KCX=JaY8z1j*}4z0MhbG? zRTHqy%Ew}F_#WE}HR0`cpA1@YjPg>}n1=#!Dy#GCABws6IEx;`SKh>HX;TgePL2eDm_SzjAuKRMpb+iKi!*lEk|gzSaEJIR1E757Q@PuW9=sv82~8L<8iRi0LX_MwxALW%8LJPA8bT6k_NYU~0af+(Gl|D07msUUW=Wcn#(OiPa5Pl}kmz!86X~jxqN*VcORMk#sTkt*aH;L_ z0SUKMs7RqbrsBl=)_xh!S3Ti0d#)6`$xY0doK6zwn4QxsH#R-Eki^dvd6FjbO2-Ue zIVFi3s8)Y}AgEXD89Gt0XDv9*C8@l@+EN04$QV07bUH9(-P$XOEe%XciHVHD{ku;d zw^O3}n{&a&kzR{R&GO9(avYg}K5zk;{W#1%AW@4K9Esf|-7n_6m=l){dr z^*puQh}$Vr{l+=#;a)8bPDD+uavE~X%rpeqL5-saS}ndvNxud*1<0!)QMm3xqxBuj zzu7nPAkC5W#Ba76y(ynE$0Qe5uk7+14WmS%tL>71fIm2N*!@^V2EVrKFP}PRvoT@! z6U*d62rp9Sb?#2bpkeMO%@eNG pzK!!q^ifwu-qjC7d#4lqWiCyshO7pDbRYO7f?s>wLK#M({U2_CUd{jj literal 0 HcmV?d00001 diff --git a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 index ba4aab3..e6a6eab 100644 --- a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 +++ b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 @@ -49,8 +49,8 @@ proc TL(direction : CardinalDirection, colour : Colour) = show(direction, colour). (colour == red) - -> ChangeLight(direction, colour) - <> changeDirection(nextDirection(direction)) . ChangeLight(direction, colour) + -> (changeDirection(nextDirection(direction)) . changeDirection(direction) . ChangeLight(direction, colour)) + <> ChangeLight(direction, colour) ; ChangeLight(direction : CardinalDirection, colour : Colour) =