From e16a069d091dd130464a64b20234f0621fb26414 Mon Sep 17 00:00:00 2001 From: Johannes Theiner Date: Sun, 10 May 2020 12:43:31 +0200 Subject: [PATCH] A2b4 fertig --- mCRL2/TrafficLights/v4/v4_spec.lps | Bin 3229 -> 3396 bytes mCRL2/TrafficLights/v4/v4_spec.lts | Bin 3763 -> 3153 bytes mCRL2/TrafficLights/v4/v4_spec.mcrl2 | 20 +++++++++++++------- 3 files changed, 13 insertions(+), 7 deletions(-) diff --git a/mCRL2/TrafficLights/v4/v4_spec.lps b/mCRL2/TrafficLights/v4/v4_spec.lps index cfc93b3f954dd0dfd00e6d81e2b0226aa6a9333f..a184cb05c9499dcf2af4c271d29915fa8ab84456 100644 GIT binary patch delta 1757 zcmV<31|s>L8N?a~0E@4K1b~Q<2O|Y-adUu!kuG5jGztX^0T?DEK5B1vk)6B@WoBn+ zZg6sRczl3`lVt&H0cn%c0W1PMJdy$wO-4sZNlHshO-@fxQBqS>RaaP9T3cLQUSD8g zVq;`%cX@hyet&>~fPsL60RaMKF#rJwL}7GcL2z(v1t0+!0wx#(CTSQ0CTSQ0CTWve z0*?s?2R%PPK|(`BlkoyY4+M8%X>D& zV{`!p0to|?mjo~cGyx_BX_L$ZJ1S`=6ijJuWnpqqa&Kd0b8}O5ZEaz0WCkAs0|^3Y z7y@g6f&nH12?GIjlQ0EC18D(ilXeAT9d!##X>L$*Z(~z%Wn%>a0XzXk0agKkgaLqt zfQPg71-$`(g`)sv5GMsRX$J%}WQPURZHoldVoL>7YiOv=!mx@csbN)7Lc(dHxrNt7 zGYDadrWDf@OeK~p7+Y*oFpfB=VO?=R!g=Dph4;lh2oOrT6fl%@BvC79SmHqNi6<`M zQ%p_5Ws<9f&p8(eQDV*%vXq=9RmwP8>kx2_G_PTQTW(Imb=a+i@1+|EF!I(Eap8%O z1O%jFz^1d4lLCyu1t=_m0!3?J4d(#7!BfJd6Hcgp2n2);X(Qqkkj24T_%JgH0|$C5 z_>9s*rG_&=B<>j+a}1E-QCSl(3JH$PmJlf9RE7(nL1L&83JH`ULy&?Y4idqFgvtYg zXR{4|j0zPM5F+F_St*2Cf?|kBR3M~7L9pO~Gk}no9M52ai$zRWy8{+#(G#GV;ub9k zClK-M1TTz|2^M*vWKM{Z6Aa@87R?P@iW-)Gg(4K@^85KD&+g9R|;HYzMzA#mAr zvL7uLDUgNigd>ddxe;Zg5(y_FNhyJM!i8pt5kj)X2|0o{1u<;Js=!+(OoEw;7?n+b z5H3+@Ya)d$X0#}BHFUtU;pK2BM7~2L@)ZKu$f8je9FwUel>$avLe&K`lrc=9N~I1| zNR~4wlqyaXl2j=rZA(-X#Zbjcg(y@xRU(+mqfu8`TB2>T2+7`)MfQ7ORq9R{W1TS3 zLa{}cZqjzboa>H?Es7vx%%VCu#9mYqnTpdoIy*9m$qutVC_>SK}`J#+@*+jD6}S3L=d9BNt#r zISNS7B*U~VFjF|fbjBO1Fug>JBO!>#6zVA>LXnQtw82bM3DlTwgu?YwB#g#05aX4m zD!|Hel+|&>rzSPd%_O6kqKTw`@TI7Ng)uBYbE`#!5ldjO!!BLs5~ncLS%sjYGMg+z z+M~*Kl+|Q%d6LkkHHYe~AjM&Z^$ur|RO+e8V978khhawB4l!t)Gf*0x)j2HLE(I~{DA!@eSrvwVTYZXo(jyO3 zj-;HzdTBv3M6{rpV%nSmGlrLTX4hby5~M*)rwJsdh)*cAHHpJbGMgMMvc6$C(9*da zCs5(K2MfU%XR|n`i9|H-sV8EfJ({(_OqU5TxM{h<%z7;hj#m`$NG6<(B+{xzSCO6BJb)o-~aTkftApl67tHi%A^5 z8ClDx!}LB7Zt%hv22Wp!drT)z4x6Zv&k9BqzzFkygjxJD-eO>I&FBd)YKrOE({+%! z=19VrK^|-fiy%f@)KnRHa!#%H5hEka85L>9y(6nTlcavFB51hLq-~dS)QM80UDq0v zkEZTIk?Q1#ZsSamkKM|WDTWY4klyve?9$ delta 1586 zcmV-22F>}z8l4#j0E@4K1b~B)2O|V%Y;Jy$FJTTR3WojrRagm(73}9hm zV`*z`Z*zBmfRkhaYyo7G(E%(vI5;IIDJm;0EiNxGF)}kWH8wXmIXXo~M@UIZOH55p zPf$`*R8>}2SXo+ITwPvYXL59Pc6oYxe14NY0vQQp7y~9`7y~9`lVAdm2nGf{KR`i3 zLzDOdMF|LHZE$pXL1T22OaoVwzXR7QYXKMrCLD&V{`!w0SS}A1TY0G0VV}xllBBVDP$%TOlfXqVRBG%Z)0V1b5nI~ZDDR? z1{nea2?Aso0%m;yCISfq0dSLB1w#X50c4Y*1!Ej=3ruNlP;zf$Q*dQt1pxs(0Ym{& z0e=C2fq;UuAqKqxe~F_2We_I>G-(F~)MSSQ)NP9eRANg6RBK|GMHEpms;I1CG|@=H z>!P8AFvSB3X^Q$1%M|o2wkqgH98u7&xUHc)@k>Jc;xmK@IVTDjVvZ6hlpHK^%h*Jd z6R@eIt6?(EM#ATqwS*|8D+*b1mJ+JOEG=~_m`0nEFs-)+e~y44B_kFEHJqH76h;6k zL1YL5D_a0=a0=!ME)*c^wM6hh1R!fkcMzn8E(*iJff!I2JJCzTW|9>wF`C{daLCh` zWQPih)g6FPP9RZ;s&-{0KRN~T6(0zYbO8z&gctB|rgRZUP#hDO6f!Ekm?)SoK!V9o zBIF$?LPH@0e?l4siv^L~1cc!Q5{jVaYG8}7aI;egl?O!-u_!@EhmB>yBy^UDz4ZX1 zazv1rdl)E|Xlh#GiW-(HcuufUEI}M>rJ4j427)ID+Q@|l#1kRPJHSXrEFQW<=qncy zF<^nxBqBz3^!^-Cn=x(S{e;uWw1}8L03REbzAe|1RVk;%o zQduB$=?IfZWU4}>QWGuJ2qUb9L>OskfJx61N?;u@p_!sMoUoyof^6928n~Rp3PPU_ zVl`k5lcqx~xs1wU2S8BR%4mRci$h!FE^|4aL*T2X0f!qau0kYo87+{g7l(O5h%m&R z2_&f!e&tq*}{ zcUI`Lv_RzM$s-V_W0;J?IzEM}^gTzR8o3gOO@50o+?_cjX%a3v5tt`LFttI4s0<@c zeMv6os*IZ&OvY5pfVNQaYu3zNuO1Z&+lw%Z8 z5bhN<5RzowC`_dXPcY4ntmYMoEv&<}IdPamw8Ipp6oTOIps^PUhAG5TRg#Y8Q%-ct z4ANLuqQkW6CJu%x6?LWh9H$vcIfZu;e}HC*N^p{ZVhJZ=5Nk?s42c?9Ihfsov`Uc* z*5x&6m>mwna4F&y$}J6Tu-y!XTMNjqm{v4YuA2)`*m}CcFjO6lb}Hym6+6mF#HbYJ zqi`;O;X3;b)7W0SL_yTh;;zvJQ<9{dLYYotHw@@b6RdFEBZcbZSRKtyD#NOEe^isC zNYv;?;GG4+bTbJxQ-rSPNjgvrQB-@l)HFy<_jadpv>hwM@H(-0L4=Oa3@GKv;hK*M(0FzT1Ff6H z+{O{715MOOdxb+K(tJNd;Rf#vbTOE}+u3|g!lIgXG~Hw;xs)@VFT?bH5N+_oI*I+G zE>6|oVj(1cu_BB((j;+5a)gY~BuOV4_>DB~PZ0{Zi#+2;5#(LVVmV6@6ixqB`0T2(9M=$x5jyMQjpV_6RNe1m^vMGk(D^02$?iO#lD@ diff --git a/mCRL2/TrafficLights/v4/v4_spec.lts b/mCRL2/TrafficLights/v4/v4_spec.lts index ee795b23d444294d6e759132041651b7f22e1072..a3fd64c1af98078e553c6ceb11b7bf4573a62c21 100644 GIT binary patch delta 2079 zcmXw$3s72D9>(vzAQA8ZDi(}M5s`@aHZf{l2T@VM7)9_|6%Y)X=4IVvw3z`BE#jjZ z72g)FkAknL(H*r-SB+`Km?kwkNo=~CO*9X)O?9{1*-2+QtIO>I|`Mz(?IWyY+G62L!N=oG==kklrmqq~r&FiR0 ztPMzpJjoC_r$EIV)y5V%?0QH_do52_9v8= zk71v`Ad|Bp)hLQA&N*1kW9UFfdkBRE8JOsT(xMCJA-m?E&@^Q(n166YVW0|_2e1Im z8;Dh*0;g!&c0gyqnN*Y-jtiIlfe|3iK(e4f09pXB&K`hw636yp0u8+?PS7NHK)dV_ z=)a4E6-|OM#8+eS2(&zBva5;yni?bRqV73)v4QBPq3H=`4OKG)eisXXI7pz@ncS6B zbVanVQVj?UCrkl83%3A;a62~41;mXEeTq}TsjY!e@6(Id#@r(?6+EG*$`EAoD`xsM zEv96CY|@zHZP-sAl8XDOfNi6p!hyX203aBYYUD%%vv@m5Mzck=1bwpRQQ<@)WxH(E zMcZk`ahkZ~s_+7r0veg9BuX*{IB?wnwwkcTu}h63Igv0^{$b1aHO_vVYf0fLZ8J`M z9j-6CL_*!AH#U+OQ`?KFPZOB|D|cV}8tXWx>^$U#f@G>?(FwLP0#i@%3krK)3^+HI6Cd-M1$AB@A=!No+{Fy2?Y zU6@znYcj9&JhrS>I%Orsw0wD^t%FOSoCLM-G6$IoeGU`; zK~b%JuG?XaSxmjiL7ZKOUu6I{-}2czN=@gpI35OG+lMkcxP?c+zN9%Y%Y>GJ_RCT*2(J6#-6{M1UZnFjE*lsHY+!P||9P zI1iBy<@8-e(2u$g|Nnn|(H}ONG*p=;HB9ID6GC|!Dhxjqk8tpJPCWZK)_df8yr+K* z|J2-En%h`^mA%pL&EeYO%>rSN$&8o!3>|i8{7cN(v>_U2AjH6@atAnuMk-`9p{k^K zAZT$)vmj;@s^%}%7lkehxF7l~I_DSdDow|17w_9$nP8Ku=7lrs5yf;J4NyC@YH2m< zWdk|s?2(Z7Vk?ek+Ep`f^QMi6WO}VMQ11=(b7$AES5K2}p;CzGl+5DXuof@k@q}jd zc*5CSdfV;sl;R(KTj_hp6Ev8c56nKCHqWlhr{;twKwhRp6aGK({lQaJo_r*%^|{Cc7G8Dv2U-FD<&1lx}13buOO2+ahPC zwlpnmrbA=2Q6XhTeVu8ER*rbD@!%0$a3*bIK|eI)(`{z)c)lARZRX<6Ii0?`VURl3 zH>{Z049=u)7+Z?nFkiQ4U(>SS`gF>R39}h4G{e$wy)EL(jB2@2;il-Q-H4S%gia4g z`-~>_uRX((Zxt4CPdb-B@;ahHyu+j3)NKe0%g3e%wdHS>U7x!5d8tq2QvTM~{~A8( zCkkqGdl#khFsXn4e02X=UZRO^3Z`O=>8<{qDZ122u8!)Y!=!x5KiU-(nCCCTwz_eN zvrHcWk0GjQJIp24v&i4fcMqrsgdK^nxHEV!Y)HVPi7eN;7}$E2(``XVN2hFMa5E{S z^wE1t;j4thTC;kxTtx#P;UY3UTOT*)=tZ{w23@ip!|Hy)^zzbfK__SXUyl3k z3fk-5mf7q$My?Nf=5!=}q7EQ2wcorH#nYc(t!T~ D^`pIT delta 2671 zcmXxi4OEi%9tZG;hX({i2Z)M>UEW0AEVXo4t_zBYyeOe4qLrp}@+C*6z3jH}lBQ@m z6|`(^^9_ZhhGuT7JQq8&Qro6Zx3aCZmUp$Wt8U+qR=c)i0MBM4B9K#YMR!q1B^rC*aLYT3#)XG^}H!B4HR)idilU&4x zh#AIo1*b(qS0gF)Uw@lXjZMsY~+#t17_|O^Ah{**Z>Qw-t0IvKU?4L>(K0I z{_sIG**2%&-AGr@r;{CTlMCXc5#(aeC~Z=BpXyXx)!jE7JTu)Y9|#fDjHcw2U5nM& zx{{Nt`6H&{%RhJ~ArkeNZ+*&>Cq?S-C)0^4YbIkD)g`Gpzh2Unn|p6)e{yo$P6d~< zS8<7Yc_u!(vklK^o_(OzhRmJXJ=|OOX+|n#_jtp`saULG^iu$FC9`3$s%U0Eg)Deg+}i}gY;W@eVMUwz zfAAYj3;ebfjJfzXxPzy_;GDa88K!adSpU2beVgyXj{z*vUn>CJQl;|w33Nq|P!A3c z6v5*(%?|`AQe*TJbi$blR1AxK{vr4nyu`BmH^XGZuLL%p@l?UPTV@yg0mjI`5 z0wz`n0~}bWg&BL$4z2?g$VY9k6W}{y_~|Z@-vQF0X*aw^M!vJ_`Dq7Lywv^K@ZKu8hWi}u ztaX0a{=6<7N~$w`8?{V;7e=!mQ03TN5xkop{Nzpc@VaO4SgRLY9Is6J#_XR1(g$u2 zC-tv=4~~PD@dx)+E`1Hhz!yXLjag^6+=OG-#l&BW{RRggX>r$_xu$?>CxQa!4_*lk z=+GCr+#u`qzE0{BX2_2G?Y>2W#&L^o1P^_e3$nc<3u^W;*@m7degKvDdiDIhN# zp?P8bXa%d80a#7JolOjz^?DCw`%18KYM!PFL(*+lZ%oZK);-xc6T8#Q%Uj8kMgN$R zj}H<_h~hOTk_8UQ z+MTYui>UJ5q0N}0iD_j!=X!$g93T9K^Q2HP!>Bh6voWI>o^s_a*~+aH6`?n$^Uwyn z(<@oIlezN#I{gVqOb$!Vw*Sh=?p(1{D4^ED`;!H2p@($jm?qpsGl!ibhK`wdHMrst+Up*IWy$g(Y65|!)!BE zjd7cs1{iPfadMAqK|U6hN4RxRv!qqnC7f*rqHJlYTtyTocBOB~%Z0Rtt@5Q#IR^k86+EuL+?nC)l>mJry7P$duUh_4t5SXGqRe z*;(^~D6S;jM(;&HLSk& zp*W|7F?ZnuCt(NcH(l<+2O~G;w}d|2nlqa)cV6-=!#S1Z8I~`%xu+!I)76g7EhCoW7y8Y2m$!+la z7VOxld*XG&?0$OPCaqH|i@N>V$K$B~35ex&IRR_Gbe_t|9l5!8piy_Rzv(enDqt-v z4`zj&SeNWvija0LvG+#}ac`29Ua|9M)#;dW%Ycv3qBq&=x6e_3kr6xDwh3?IV**p2 zP5xaSaEm{26e`K=__7-O9d)3-I& %ansonsten show(direction, colour) . %aktuellen Zustand zeigen (colour == red) %wenn rot - -> ChangeDirection(direction) %Richtungswechsel, wenn wieder zurück + -> wait . ChangeDirection(direction) %Richtungswechsel, wenn wieder zurück . ChangeLight(direction, colour) % -> zur nächsten Farbe wechseln. <> ChangeLight(direction, colour) %ansonsten zum nächsten Zustand wechseln. @@ -69,22 +70,27 @@ proc ; System = + hide({%unnötige Informationen verstecken + proceed, + changedDirection, + changedLight + }, allow({ show, - %changeLight, changedLight, - %changeDirection, changedDirection, - emptyAct + proceed }, comm({ changeDirection | changeDirection -> changedDirection, - changeLight | changeLight -> changedLight + changeLight | changeLight -> changedLight, + wait | wait -> proceed }, + TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || changeDirection(north) || changeDirection(south) %starten der Prozesse und auslösen des ersten Richtungswechsels - )); + ))); init System