From dbe8fcbf68d1451be932268260155a7f3027c81a Mon Sep 17 00:00:00 2001 From: Johannes Theiner Date: Sun, 17 May 2020 11:28:29 +0200 Subject: [PATCH] Verbesserungen nach Testatversuch --- go/TrafficLights/TrafficLight.go | 88 +++++++++++++++------------ mCRL2/TrafficLights/v2/v2_spec.lps | Bin 1564 -> 1751 bytes mCRL2/TrafficLights/v2/v2_spec.lts | Bin 8425 -> 8625 bytes mCRL2/TrafficLights/v2/v2_spec.mcrl2 | 30 ++++++++- mCRL2/TrafficLights/v3/v3_spec.lps | Bin 2125 -> 1673 bytes mCRL2/TrafficLights/v3/v3_spec.lts | Bin 5244 -> 4866 bytes mCRL2/TrafficLights/v3/v3_spec.mcrl2 | 43 +++++++++---- mCRL2/TrafficLights/v4/v4_spec.lps | Bin 3396 -> 2850 bytes mCRL2/TrafficLights/v4/v4_spec.lts | Bin 3153 -> 2708 bytes mCRL2/TrafficLights/v4/v4_spec.mcrl2 | 17 +++--- 10 files changed, 118 insertions(+), 60 deletions(-) diff --git a/go/TrafficLights/TrafficLight.go b/go/TrafficLights/TrafficLight.go index cd7cf5e..d0fb958 100644 --- a/go/TrafficLights/TrafficLight.go +++ b/go/TrafficLights/TrafficLight.go @@ -1,5 +1,11 @@ package main +import ( + "fmt" +) + +var debuggingAllowed = true + type CardinalDirection string const ( @@ -13,28 +19,12 @@ var Directions = []CardinalDirection{ north, south, east, west, } -func nextDirection(currentDirection CardinalDirection) CardinalDirection { - switch currentDirection { - case north: - return east - case south: - return west - case east: - return south - case west: - return north - default: - return north - //TODO: dont return this here, return nil instead - } -} - type Colour string const ( - red = Colour("Red") - green = Colour("Green") - yellow = Colour("Yellow") + red = Colour("\u001B[31m Red \u001B[0m") + green = Colour("\u001B[33m Green \u001B[0m") + yellow = Colour("\u001B[32m Yellow \u001B[0m") ) var Colours = []Colour{ @@ -55,35 +45,53 @@ func nextColour(currentColour Colour) Colour { } func main() { - var directionChannel = make(chan CardinalDirection) - var colourChannel = make(chan Colour) - var waitChannel = make(chan string) + var quitChannel = make(chan string) - for _, direction := range Directions { - go TrafficLight(direction, directionChannel, colourChannel, waitChannel) - } + var northColour = make(chan Colour, 2) + var southColour = make(chan Colour, 2) + var eastColour = make(chan Colour, 2) + var westColour = make(chan Colour, 2) - directionChannel <- north - directionChannel <- south + var northDirection = make(chan string, 4) + var southDirection = make(chan string, 4) + var eastDirection = make(chan string, 4) + var westDirection = make(chan string, 4) + go TrafficLight(north, northColour, southColour, northDirection, eastDirection, southDirection) + go TrafficLight(south, southColour, northColour, southDirection, westDirection, northDirection) + go TrafficLight(east, eastColour, westColour, eastDirection, southDirection, westDirection) + go TrafficLight(west, westColour, eastColour, westDirection, northDirection, eastDirection) + + <-quitChannel } -func TrafficLight(direction CardinalDirection, directionChannel chan CardinalDirection, colourChannel chan Colour, waitChannel chan string) { - var colour Colour +func TrafficLight(direction CardinalDirection, currentColour <-chan Colour, oppositeColour chan<- Colour, currentDirection <-chan string, nextDirection chan<- string, oppositeDirection chan<- string) { + var colour = red + + if direction != north && direction != south { + nextDirection <- "go" + } + for { - switch msg := <-waitChannel; { - case msg == "proceed": - directionChannel <- nextDirection(direction) + show(direction, colour) + oppositeColour <- nextColour(colour) + select { + case msg := <-currentColour: + if msg == nextColour(colour) { + colour = msg + } } - switch msg := <-directionChannel; { - case msg == direction: - } - colourChannel <- nextColour(colour) - switch msg := <-colourChannel; { - case msg == nextColour(colour): - - } + } +} + +func show(direction CardinalDirection, colour Colour) { + fmt.Println(string(direction), " : ", string(colour)) +} + +func debug(message string) { + if debuggingAllowed { + fmt.Println("Debug:", message) } } diff --git a/mCRL2/TrafficLights/v2/v2_spec.lps b/mCRL2/TrafficLights/v2/v2_spec.lps index 39315feb515a78c2aef6d0de6a29344f0b137388..18a5d01bac3ae1769727491c695031bf28a5efe9 100644 GIT binary patch delta 1089 zcmbQkbDfusp?iHZOT7@8Ig@;pO8W5XvOXD41VRkYAixl8R&k7sy2C{G9yKA_hj5c;CbV21cIb{M@9> zyhM;4#SDyWrFq4PX{kVI7N`9DoXPc!qV*gui6x1S1qC@w3e4gP$}Hl_3hL}2G1tO8 z7G5T1PDXJi1$Aa|Wp&1E21WspOju$O!mR?lN-C;qW)_xK);4y|!Ay+8jAcNZic1np zN`Y2#rXc(Xw~ASbQJh6t9B8bviMTqGni>NmQ%wz!$OMK2M{s^oiCb`L36$v!bUG6w zqc$TWhXYX5HLo;x@@qyVaXCgkmg0>3at20L$K(>v6eboH10!RT$tp}sMQv>v7?~ZC z4S@~;$^kvk#L8$m`7e_PyE3b~vVwTvWFKa84RvJ^pUk|}#G-(r{N&W);^5NU+{C;T zHa13PCUtQpryxdUCSZj5PF~Hd$g0dJ&Zs>3BD0f}FE>yZNK0@*YBDP$qduc4qd8*; zV_5iPT^6Mlb3E8rs;R_zoNw)e#hA@nI0s zh$%Xx#Ob4zz^q{FJX>pOQ?t-Q7l$39CssTO2vf3So#5eF(=pG4Ra?x9qZUpVM+wb)3caN;Rb#YT~?981ZI zD^{JKc+E8AhL_Rf(9nsCyZSs=E;|r7XV$DWUuA>CeVZ2RnwCazgk%_nutn|n4SxAT zc6p(@L&A2iXr7RY46CbQ${V&kkoH|X<3LZvQ-gi;9t$gIBquY~S4@oBYTSCzn|-Em zYjSgwTZ+=uE{powcmX zoug~hJC$9hC96FhlWk)1R!@!*4Ozk`_FiS3psMd3=aMk3Zz4c5cbJDP-g!EcLx%Y# zr;QTV?;Z1Attowbkd^0+!O5!?M+5G?hz{FpvTbQ~YHrZiTen)@=~chhZ|CLY{+4>D UG|$31r|IwJ&)-g;zirI`0B|T?UjP6A delta 871 zcmcc4JBNpjp?iHZOW;H{Wi~luTPGKviTbg8X*{fq+~P_K>he|&!tN7iN3#hqaxyUr zPy8#z#+P4`ky-qG3B!_$vRn2{?lwW7p1 zKPSJmh=Gx-I591Cavq~xJ-csWL2yB8G9x1+Cre3DX(|IFi&K7n4g({HOJYf)V?jX< zlLWK4yb_DJlDq{wNX)e`kA<6wnUhhRQJzU$i7}gjQ2-7Y>4D2W=TeI7NCp7nZzxaYHAo5*??Lz^YfTk8Pz9;GJCKq zv05m}i+fF8!feiDp)~m}vlI_dv9&j&5)&sgquXR=7DZMipcj-TYqB^=xpDhs<^>ex zCxhI^%E+k7sLiO$=*#FIFu9dQtv;B6Nlbx3XC?ObF==GRsjZ%0HG`l79(D#x{0vVxME z{kn|OrwW-y8Xs)5aFac@yLj2%tnC$M^?nb&G`SQDc`sUXIBD4evzJYW7)?*CzM!0D z<&x=Z*EvB%cq{LW2?B<98)Jodmo66F^z`%vPL?F*N&5xbrlc}$a^i6-v@nxYnrPSO zv}B@7Bu8{9tH4C>zM`ZUsmxhLnw*zr9#xB2=39AC_m0RpcWn!elLnb$6{nUcJEn`z z6!MvBD$Hu`5inI~(_@vTj>{vbs!f<`Iwv&MtK{kwfxBCES6m4-JhxiQT`gyo%7a!LU`epHabkq8Vx#j-TqXcohAQ(4OSY!w zW~oZT0T2K{i-eM5wW5Sukgr0TniJI8X61Zo6FT3T zsxa9<^%WF{BldJJLW4MaS0ddx*dtVcjTIx1Sc~~7pllEUV$J8v)yfP68U&FRM9_>| zkXxWG20&!7GTpSw#$u&%e)g@(+}wiACR!vf1VAv_^dkX4?0h%7xVT_5f&gNXAd!yw z6kn)RfFOv)%uk;H6-cXm<(87a9S1J9Fe+VK5S5><+=8Gu*pVF^7gLtP8};<^_6cKg zxKYtD2qI`*P*_-?$|_O*t=(ciZedtd>Zh?R6$N=|rc<9kZ>rvLTq|F;ej2il`t?My z0{UVVpPpfAVvOk;{SOEHy$Jk!!88>rMyjYFKdYo*{?W%3n8wFL`}m7SsWRtp0Gh2Z z-C_g^6%?{!C5XkUl*)z2056vC>B`_0#RV!=R{q8$_$lB*DiC^DvNF{9id1!>X{o-cHAxu%A{O{dzbDpBT{_7wp}&hISFj{ukffB=YM0kwdcvDvNC z9l*8$T~zQ&oV5#U!qpFR4rDrGFj2dkwLryg08Dhi5UMRXs9zh`&n3hhn1-7U%NI6MR(X;WbKX$j3C=yCdi@<8+Ksq<2!LK?wJ`WVf&qXibr&9qEZ@Ao+z)fU?oN)* zoqJg0m8U&&t?{RciS1>Ok6;1&<2J#J7>DeJICFCtPG${^^uZZiac z*te&XA!y#Bg*llg1kk(qq%sJ)OJOY|7iJ<~XTXhU8BC!nZrd?suyIo)45DAlreFwG ztg;ic;KFxH8HBjMKVL}NJ=Fnm=w}BDA)CurYNfWlO{#GX|T5 z&VTF_$3(p$!A_LB^@6a}Itq@Aw}cb@m%$AC4+7i(9AZHts35KN4~LIB{uNrW2^y$Nx!@hcjICwvpX8g`?MpV3Nf zIq%{YqT{uY(L8=3`o7gp*euG0G{8pzGcmu9&Osca=i$N=!EI1b-ec>Q3ygm@adgZUB{ehIa`as=4Y++C@ZL>lQJBf)fpAZH!kt#np z+MLOP#cNL>fc`q#4z?BVh%WBTglMxXS_pub7mPvc&0yoo7)S%Q=fMoOaB~~Pp%t|6 z%$bo{utQW>IDLAJxrYF*?IJd*U?-wAslh%Q4%jA-QWq~o$WPm^VFvlbEo`;ANBLrn zc(W5shztMlgdpk-3j&Bgk|BWJSP)PK!KFOt6G&yi3}5vQZbU0ipIx;p6E@fhRj;O% z9;?K_Ak1(|u&@)+qwHgKQ72&`rUWxP6UiEqX<&j^gkNwfW=#KD${;@8&j=&I=0$fP z&aA$|9CH(^{6r4kFX=6BW8ke-0cADAf_LK zQPkyV0pvlG(2EmCU>b{IUlqfGS%Y|CntxihE*N6Y!AN{nr@JEqKE2R6p%iQWRqgYn z3!$Y&!mc}T1bBx98}5@~u*_HD#kn$-Hh9k$zc%K|3#~djw7U!vLrM?9h}Yp$32_L+ zvStXO_anM!f(|dqC=T%f&AQ?RJ5Z0k7sB7#%)tR%TCBg9F-c`phm7?9OgnmYbsMY% zyocg|;%{Ll+OKUPiaEO6q6^9OyJ%>aK{oWT#fLCaz*iWkG-qC#gN1}#2{MA&)5|!L zE2Z}{`}7Q=(!1^9k>T6K%r z*)_s|yjKusmIF6|`I!)dc9r}C_A{TrVAC1c#qs+W+=x!QrpJFYkMWzExyHqxUBwIh z8CDQl^R*e*&WoZL`ffZ!e%QkqC|1S9&&W_#C2#3cGzbu4hxq3(V$2F0| zFZJ(kg%9nVg}u=a9AF2+s15_W+_(>%3|8ad5c>@55ItG~J5aw@q{z?0^wQvn@07B4 zCpJ-5MSUlmedn}EOz(L}UI^2_dujcVHS~}?X_aR^6#s9yi$A=y1A^cmj-C)gU&Q_Z z%ke1T$Vu2>R(INmO?T&vSR1Vd*?7Ugi0zb7qZ1md ztRY|4!+-ceHsqn1cWbZ0Ep$M3Fhc53`h=!Q zpV6&HU?pHy6t@lzLoqZ-=q{8oE~W2u9eT*3KaM05kwA)DPaH|7oB_qT;>2Xw3;IPU zY5#>ou$Fwu`Ug;f=&d`gY_h#8Nzof=$`6UU_!L+H@6wE$C4mELR2g*QDFq&kb9x>TLdPfCf+P<_17Cre4n z<=3w<=AC1VF6@3W{TQqub0Xx(*KkPeIzCY?fB9t)CHyW?-KTU85@&I2!w8U!(7){Aegp?>!+M<9 z+@TPjO$e-@)0}p@c5M>a1kXBwu0uqYjYXgG|ENvY_n%{?oOV)&u#vMXU@!Q3=38P9 zyda%+&8&)WjqN!CAP=QWAv0-@^(>N8@d*bBsq0Lb*s{7t8 z+0w;kzo?u!@vkjIDdOpvKvF)h$*Xr-Fm>V*Z^%{nB4nXE?S!xDW0vkk@QV{esv%%t z;#*ij^qvsox=6fGuR#W;bF?h4UPUyn=qJ$fkVews#cVv}dn*1oi= zI8vAAkTN>08}=fX%`k%>qxFjYGScJVv0Wm?fyq%xP8R^Z=wL*~bwf&h&KM~w;;|I5{I)J7V|_iWaFxBv>pdxF){nUgmA4J!?mHiobQ^#DL*2V` z3>et>t8SdnZr{vHUo1E7V~@%1q%Z9qHxuepSm_ti82=U?OuFCtRnPb~`eWC~Q~g@2 z8}x(9=u`I%>J{trnKgbw7y;MKGj`KLl*t#qusgYCX6xI5faolm`_Y3nW z*)7-gDL=2QQxCP=?i#X2y#N9G%pwNS=ciEep^e9<^9Hi}4s8=UTU5&Kz8RcO&dQg-L+Yn~sCZ+bc@FtDVIds<{ zH`g?)G!9*h8wb1IQe7t*-$FqcH>79EW@c}r)*B@Q?{8^bs@Ql7!tZRXaVVoAas z50AHDh+?Tq>*4m|>-U(L7`vr;PM={sNCIuOrYe8)&s-m;9B3bjUi?T+8F zB=B9|*}rK?EWdn1E%6|J!n^Siva>3MFkQUZtfMqOc8 zO6L!-UmMW8rP4wk`%Q5~Ii;N-VBgz_Mo|uWve`t7hyW>F@#q3dKToZVZR`T|g zykJyHB=Ld@MMfP)A|Qj5XkbcK=ZD9uxWJ2^ z!3U-ESdqD2{w}UmN->)2R6aFyNk%_HugD|NrMuV&!;Er*NoNir66B0 zDSej^t(PZJrFahx+AuMr71Jd#s42OTC6?lOs26?4GAf-eKp+)LfGU-;5UA-%%u(xB z3lOlfvZABP0#`Z)KSX$-3J_)PXqM$l$5iZ>i>c)Vz(Izc40VmM+Y{$#=9rA=j;VZx znrH|2?W+e464MyYEL#r7&Pi+4(pKG?oaoqMrz_=8J0oN^x-@>R4?sFGBo1LR$OcmHc{*io`Xu*tU5l*qv%oq~S^5>dF4w^tMf20{% zhbDZ6dZP&xqX{0UyP6UaIlhd7+%F!@2;VtdNl)r za;+C?R@0tXp4_$=K@esBXaq!6U>o^qayRjNW)YqST$v*xHuC>PGs^5z5Y6Jb9}HVA z0rw_&*jtO=|HGE*Aj5&HT4XggZb)}F)!j1Rrp(Q)Y``+JJr1jPG_)Ne_;oybPe5e$ z_B+!Ibj!eF=#NYMZwP_f!^lGao0nJh#$+8PII~mxV)70@aAq&<9mqLc=*%wY8^~Op z`I#F*hez;f?~R)31T?|x{ftJq9!+q5KdSMLMc3|eWNR_TXG<<$iz1vtJ#)BxOIXub z!}SctlP^qlF|$~NN6p!oZ-W$)n#pyz@KuUUhbPxz!~LejhbH+J;lWe+M<)F+;ek^d zYOL*WKZZ`RYr!4fX0j7gzD$RBTiL~_OAH6BwM;XWA9##q7toxK+YmmLRll2w-QYj9 z_Q-Cg#fFe6WkWzW&N;p8dwdz+dCPa2$HKb=`VI8`C9f~td1`~MyTVeKv-QN#jlKVI zMsP@>n|u4H(>$|Ogooz+*mP5OS$|FP>yM7oa;!k`y6m{L35$t)tvw$4&5^>6jz>!b zRS z_EuW&&krZcRy$i@^Zkj1NzT+(GfWZ1U(|al$0F0)mP4292y=;8U-nROe(tFSVQicG zt1oqL?4=p*l`XovMCm5?J7;y3Bx$~T+iBe!Yw1q+xn`GaJE`3LNgKkSZAF+sr$rxh z`;Nq0%h|7SduHn<;^4k;dr&7xba{KAb)*i6_jEo?LA8sEMvfou#AHf}IvZCvVKVte zzcoI(UVS=_S#g%!f6FWRBI+!q|ElMceMw02>Z10>E9JO3PSG#Nuk5Y%lNL2K79XkX zh$$L7UR;hNCl=joeA9%R;}v~qwD@NKOdO-)bFx>*1=i*A&naHr=Yd0U-1K04a`RLK zvo6%yo0ax?oGXE{<;;~1V3Xb7llqaX$yA?KoIFo-`mlpP1S9bVKjmyz>km zJDu+OF!P|8CrN5~rpH>T729 zGyR4O64>5V%;4eFxXA(wX5jFy_{m)uX6P_$c+vv*IAB=zXtDtNc*Sts18ZvaW9G16 z1eCX$B^MzsJNA8_=XmO~$?V=0IgU1N*4}+93LIN$@xtC4nT-^0Ym2@c*^RSafrKCM z1io+bebF!nmFAxOt7tjfSnHkqOmtOfoOVh6C{jfkM(D}f!MD*B9Jl0&K^!ZBCZy&=#Ru>~JxMb&982>d=xkabpx| zyWYR*IP(xDGupquv8&0#Ey4d>-Iec~T~<);G!4@$C=T(S-h zJSq8^>vB#rFjkT)m~*~F@vw~W|MR%G5pyDLdBhR&+M7Q$9~(uMMEM&VeYeyJR5EA}5fo_`KA9_MFNEM9x*pWP=7iluA6{U_^CL<{-p z<)0?@jv`}({)3GtPht~S`(HeMvaPa~$kFJ_~Csn#vO}8y2-2#!;YmPt>oa_6}QOOI~|h0 zF26;&-tG`w6A|Wk{iZ`<9WQLj^;2X_UBtM<^(zkA4#T+9^&5-3YXgv+l|$qUEt>=N zSev%}Eq^feDiY>u%c3BCAaNfiJrc9brle@LJa3P`ZAsRwL9zM>p=9f9YxbjP`%dNT zv@-2WVyAkxHvRdRq|UtA&TLLwk5%PdcN+7Hn?GvC5?vl2D1E4DPIQqREPZ<5Rcu-#m;<+1S()_XN# z5>O1+@|o(NnYg6o?6At8!*S|>$>saA{c$2c>%~>sA-Ft7R#ow%~Aq&HdQ^eWhvJRtiam3e0 zN1EM~OC!E&?5w4oCL3=bORnRcrWl*o2G>Q<9F1-3YMQSgg(3Om@|GuG<9vzb-7UeL z`#}=#XiIn3e#bgYTg#Sf`z3Xl%9i(E?{^_#I$BVj(ecD5H7(^`(O9CPxrO(2^k$p- z<_v*FXmm{1ZbbB(fM{taxK_3=u~>RJJTj`FUhQqYf#07gS?Y0lNo0SngyI~P&-cog z%(`7<_))D7`}mqYZn@~n=dF=} z_L58Gcg8FZ^$V(svfpzw&DSZml?@q}cx^vg#19FoinD){XlgW+q_)XDbE8jgE&g&v z$g+4}tJG@$E`nmuHJe|P3|ALVx`*70_f>C*x_p_WsNPTMNXfoYGga){N3)~#UiitE zd8(-}J}u?^^+QwJeELG{Xm>9>1(_KiR0&g!Ur`us4Z=&)yz%2$y+EA3M;3NCugHoIPHgJC(MJoelHxhkzTp=ShX?z1tT&zyWjU%%1_t7 zxu)8;zlmYnVENU%&>x;`9ZVTocQg9N8nf_%mp3O*zwlwx2AAnqG4bCP4zEsGeZvn| z`0ERwaGG)16t(N%?!t$UQVw7D$8Gt=-p8NTziha$ODtC<;p*ED&(%GxU4K^4of&a2 dKB`doq1WeXr?hjVVap}@^JgoJ_adWY{|^p%C}jWu 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@{_>; diff --git a/mCRL2/TrafficLights/v2/v2_spec.mcrl2 b/mCRL2/TrafficLights/v2/v2_spec.mcrl2 index 5d8cb08..6858fdb 100644 --- a/mCRL2/TrafficLights/v2/v2_spec.mcrl2 +++ b/mCRL2/TrafficLights/v2/v2_spec.mcrl2 @@ -3,6 +3,22 @@ sort CardinalDirection = struct north | east | south | west; +map + nextDirection: CardinalDirection -> CardinalDirection; + oppositeDirection : CardinalDirection -> CardinalDirection; + +eqn + + nextDirection(north) = east; + nextDirection(east) = south; + nextDirection(south) = west; + nextDirection(west) = north; + + oppositeDirection(north) = south; + oppositeDirection(south) = north; + oppositeDirection(east) = west; + oppositeDirection(west) = east; + %----------------------------------------------------------------------- @@ -40,7 +56,19 @@ sort map combinations: Map; +%------------------------------------------------------------------------ +map + unsafe : Map # CardinalDirection -> Bool; + +var + status: Map; + direction: CardinalDirection; + +eqn + unsafe(status, direction) = ((status(direction) in {green, yellow} || status(oppositeDirection(direction)) in {green, yellow}) + && (status(nextDirection(direction)) in {green, yellow} + || status(oppositeDirection(nextDirection(direction))) in {green, yellow})); %------------------------------------------------------------------------ @@ -60,7 +88,7 @@ proc ; Monitor(status : Map) = - ((status(north) in {green, yellow} || status(south) in {green, yellow}) && (status(east) in {green, yellow} || status(west) in {green, yellow})) %ist aktueller Zustand unsicher ? + (unsafe(status, north)) %ist aktueller Zustand unsicher ? -> crossingUnsafe(status(north), status(east), status(south), status(west)) . delta %unsicherer Zustand, deadlock <>%wenn aktueller Zustand sicher: diff --git a/mCRL2/TrafficLights/v3/v3_spec.lps b/mCRL2/TrafficLights/v3/v3_spec.lps index 7165696640fbcce083b3aed46e2319c1320fcc59..caafb14c483c6cb23ef970574619d2e4293ac7ec 100644 GIT binary patch delta 1153 zcmYjOYfMvT7(U-Qr#ITlDMebkg1xO$E~S7tK$*P(ZAB;)6rD~^Z=ncn*Pg1GE}&ed zLYno0V`kY9a6&-_lPxm*0S?E~#iY@(EL*l9j!9UyEQ`th?sPF3f8KoG_rCA*Jm2#? z!mhFlp@C0(&?b%!_t{-;yhHEuIc$W>q9CzgGPg? zG&*}%YRIb0eS<{-OrDfmATBwiI|3t&l;oO)@C9rHfB}P+yf!+VFeS8jh?WKz2;de( zvVowP?RK0ecJMLly+(VT$LO{@&ci}M20v5qig3?MDn)LdvhsC(mBDnl0p=M#xbJ`ZRF*{cs(f!*dBuT)ntB*;!CBG}KY0`w$^#_R1s zDS!v0uryiZHF5~R7cY{#$J(C<6PzYrqT|Evjxv1*JjZZiX7MCc>g&Pzrq^VuyPT@0C@z zavHf-tXH=D1cEa}ko*HW7PDgF6}8?{)RQf`ls~LB%Hn33!5~A|W0hW(Lk-c&A+e@n zi?4?0(UCho76!=_UFPaVDj!NIZ{Of!YHxIE0@na(bO!H1p+4dXSgiT1OTpY0iHxIy!Vg!45=}v03pzV|B{S8$ z86U@HOnoIwCz-!C{hgDC?|~CC*-gFr20W&Ac1c3|I?Vc*QFm}!oC{madPhEb6B+{M zXe2ISegjn9CRM_qn$XR$Ir|mX+?D(KmU+Wn&Lf@j(#Yh#zorxZP`rk5vR~hn_-^RN ziO&w0rXw&rvpLj0u{Cx-rYKrUG*@L@3z}l%D?P`Xn_8ITC3EJD#OIkkaRDLe>Rf2u zdVGDsyxEp@cI@Mtz}u)My7c3P7q#z-ufAY!XjkbA%CB1QVSkKW4+`dVmZOUHyshVB z!Ps%t$lBWBjA=>cpfHL?^Cc5EA4q;Uw(CfRDg9K{vR}NiYRh8V`$N;=Cu>Cy8<>N) zf+?eo8OFxY(=ViAlD%?A;kasU7T delta 1622 zcmYjPeM}Q)7{B-KXiF(lzN9kF6)dHNa`p-+pw0p7Ybk9;S-zQ_ zqDT;kftc_BwY8}s1pzp%(5)J3&Bz(!`#ahdVsqBf_BS0l5U{FKMmrI}VH9(0RtJir zZzTZ`w7XGbDz<5?Cb}7oi;dp+wlFqslPF$-Cd!go9QInXl~vX6>I^3Hfd(`jaIJJR zl&H5g*%82X7|is)7hG3lXhiy20Dl9PlcIwyLZsG=V$G!Vd4bp^zz8XY6BH@Mm5w)U z<*s(fR+LB}g{oRKI7%1@PqnflAXblAypL z1n`+irNRE+Xu^$hMM~;|v>84k zO2cm7{4yW{YE$r&ViZYW6hWdbOi~L>LR;W?Xmcu4v+CQz_|h0)e9a7_8P<})Ksp0k z5dub-L>h*%77FS>ghCMI2C<|t2|M~^1D6VD^&1U%21zDdrxggTO40F`Z^-4-vm(D90cv6F zsHaC!g6%n_RLbYHvdJYiJI4L$wsfL37D4!0{)wx&2f3^A`o_c(vzhrO7WjbMf49_pX!orp=n#lcP*P zHFRagsF{mf(5k~!dac*%^H06V=^5#`Cb${8CGCvRKOC9c+TQE(4P?gnjp2}Yo*p5yQ9r}jx1^sO^6{K zoFErl;wMN*`$x&-*N;?|-@7y_UmI7UP}s*ln+mV+jfv}ql|?JLqVf0=?b33&deQ3| z84@jNmmaLNKk<%y9uMjA{Xb%-fv75HZ^`|MrSAFE&JCl#M5M?RLi6_~U7`IsKNB@y zqY)K361;Sv)h8AlQ7#)K1%=0+Hr$*R=NEHB3qP==-cacO+Z=n9mX?#vaPVv4-9n9xG z9=P1TPf8}po)2!^)<4S45}!TY>${a9-~HHQjEkyZm7L*;US4Q8D9+tK^i7!e6)%K+ zcRpBneDA$m)zA6`Nx!Cv{?yex5tQfFj#Zj#J1Qz`C#w$Eddt7gjED=J^hD%l{@A9z`Y4-SQ9|n00IG|A|SFjo$Mh&EaC=e3n2s(mIRW}g4KDFkc1_u zh^TDS0YPQ66#<2+Ehs30v>*Xd^dCX(0M=I2F81&I&wn8|Gv0*cocDdt@}2Jl!1z@m zew!Ujs7RB_gjsBQOD2t&)5Cjo;x%(Yv2e(Ql&R4xN4&p~S{IqRyzAR0g54n(?DK4&VYv0EX>gONu!4^7` z#fKa~J9$oyTq#wF-w7rxC$qGQPhM%tRwU0(MQ6S|Z6(@ro=hoB7o!tm%H>%AXoHHd zUJyJwBb0&JLY0t_lamEGtX=NlmM1|rtI<(w<^mK{6@ zI)YB%dteY^?j?EWR&>YyV+X(Mgud&90pM!$nUZ7WGO0?A?gm~dS>6RJh6vqf2#4Do z5eXuQQY^OI2$p!q%I*-i2vuT5cCu84u6C|9T@)`CqW6L0%g_Vj;^gSC@Mg%0E;57L zgeZl2E8jS}Xd?jnpr=ljrzbD>B33462~)*c%4DG|4b3Z6NrhQv1_y#s=nElbi&etp zH1x`nC1PQkSb}iIVej&`Rh+t)b_k>zpo?iPMr5E2p&0&dX9slZ7k) z1E7_q^0G$fh8Blx!Eg|9T{%e>8t_hGWr0#9&PH42fV}0VV}q!GEdWv>0f5kf=`O?* zQR7X(B`Pkho?T)Cg#e}HJ_8<*ead_az|jJbB#p|68=&&=bavdGl<)B*@AB*Re2>cd z?QpaQ7*1#$@7s6+0F>pBqeEl85CBR9gz=#uI>bDIm;6Xc0UA#>7N;<65W$fKJ!~H# zh%nev;hnUfC^_o-JzlyL59@BaXnSxZ*PcY_Zf;rIXa%p&Soi4!1O!tY=`385yQa=5 z0j_{A02Kqdx1e?Q(@rV&eO1LSI8)^8E<7Q^pSEB7_-}SQuG0e24zAYes@QB;LO5)l z>hI~9Lmg}qC`XHT;l~Fm$^QUa2^AHu?bp;3@u8e5ztna88|=75c5x7Ile-4cO}oOo zG;wMm99VfEE4A4GXXDHU0PHQXZ@NDa!Ycj=bd2v^mFqzLj$7H$@0*!B@w{*vQ)#eo zD`LIbLY`~17-oY{FIW{c2P!G+t7>0>aT=s%8Wa1Cm+#2WD* zSKq*RLO?LaL(DrE1_y+ssR8q29L}-uoFS?iLxywJrNc_rEzE~UURRkJz*&tM#+cXa zK#WHOB^F*?Dk$ap_L)Vnz{v2%G(@AoqAB#jc*Mx}E;Yu`qm4rrPTh)eMB*@~gm_zb z9`gyr5pFc0jRLGZxHHCAErv4~hrDWI310VU&e6>*{QCNY*#dwVMJl63A)Lf~{IGH! z%K@lG7QJ$j9@Dwt!|!yPH|ucqf=(B&=!?}B|7=Wf4T~RKZIELzgb?}#H71S@VQAVW z5-=^ql42TUB2hOyu~#@WF(WZc0mqRYGy8AHM_7E_aC{{D2TTvgN2LZ-d~MkHzy0T|#}=J^<8S5&z-DBwk06P5O(T@L-V+(?d+R#v(?^X&w!W*Slj{!f7stcADcG;K}2) zcn)Gb?u@_Zpl7q^Eq3OOn-=Vx-;JBh)*FNBQ&=o~;}$cM`S@ZBb5`rhe8PcQzC&1k z?H8DaSm<4ZXkRgFv`d;|?b2i>F3wPcaR@G+N5IA3YlcG35&sM}N&gMomHr#KC;2m4 zV>~EeR9JKe`D2TR(xc6}ap#&3rL!}yi9My)NL?A%?7ZQtaThbU#B-1>+YL2ao)w#Q zfF9oROjG;l2aE3{ee|p-^|$+cw(%t;+sLSGpTammhqO-?mA2nwSDiOm^lW0_q`@Wd9&0#|rltk@^NgeZ z<1V8C9KmSYx#H2*3Aflb`t7Y@Iaq(ru3I;=X|bUe-{5vQjLAQ|nc-h{`GQ%4YoL@} zV!7FN`?}a(=G52@by93^dl}!1u=#IjmtEiZvx?vNsRL9241Qi076TNP=5=eM^DeV$ zyFLrTYH6fhpR#MZ^7PT&c^HOks@;^QzP+i(VR%!oj<%`yUajf(!rP`lc#EdD8k*_t z*xp^WXZX8n=)=2eCaZQzE{s%WzVWNfFbOK9cZW{kbpcLzJ3l9@yGf3e?kY!DcFa>3 z5B}5N;;@=J!P8&7s-FE~@ij5xUs=`SU-YeMGrv`(-PevZ&4_O|*;@FbnkHLPLenbk z-gRrz6TR1zoAW@-Ved8K1n+R|$Y9i~#KEX^|A8YGjx#iHSihHjlp*Eh>xVg?|C+!l zFa+p7=Pl@ulCVDXN%|vPn*J!K4IgX4GzfkhD+wQ~YsP=Xn0dPm!*Pv?Z(|LuZ$IKp z|9;1!CGX82Ro~D5p1WA^{bMX=Q9{9YY-8`J?tbt0ti>MRrsf_WZdCJD zrRMOWmow9b3BTzgM(gx?OPqRodcEUJ!UncWBKzWlL@tY#$f34X^XSs*z!WTZp?`It z&vf+$)(quK3#M+Ne93)4IbR47FBG@dEs#B~BL!|HPh$ ze@>5D`neCwrHxqniLA*2-H;xrXY#bv;ZX8$lY@A^19fL1aj}e%zV}wb{7?E2WSFUx5JO1+PxC&EG+;K+j zu?u>aV;9+9AM5b!Io8RzLQ1&QOG;wakP;15q{PW9v%hPrXa9F8Y4)wAYWA&ZuTWyB z7G^MNgc;*KLg~bn`gwhC{UST5exb0Z{`vkZRQiPiDw9p1GSoCGi;>w+)gk>}zX|$1 zw9)-uyyx^jwIBUDQ$W8yHAKI`Y17neq?*&bMNNagS<^7l2B zPCPA%eOd3I$p*VV*Y6T@eM)9SJyY0L+k<@u;$d~EFWXeyPjY5Y*KSXvLqqjb^u@bn ze1|zXdmP5CgNmz;r+XObE>sfxX>D#+jJ4iytpB`bQct<+(=-+{mv3tuT8>;l5WDUe zjd_C=Lz<#4J}leq5S-}^w5-Zl-QGGNjPiN473u5pc{(m&gxl->to5V#LgiIE^49B` z-KaWW#|eG|iHyHnE4B56Qoh)6C{Q==meTCAb8KXmWQSj@srIDxP3tvbXHUivgQijz z@3u!fEM|%mVWOv2T{Xe`V1%CNNW%Y6)4MGO7<&Be&8~?NMZR@3{{Q}R_M1JG)Zl@D zrN4&~)X9d+HoKit|LQ)G)8r2aUAP+_xO8n(>FHu4Zq<5b^7|9)W~+frI8V0QZ>ca$ zkg`+vVR(8=JfZx`&9Xgy?9 zs~nvwBhMZ>TyWN;o%8MZIqZRCr~cEBAFi+n7ca`ZI$F-%N9b=ac zSPS$g!<>JPzMUVo-TSEi+yvxG>nOhTNBTCMbAb15qc-?h~8Ba%G2~ zbp~B`^&bDTJ6*!#L26`MVE8> zCj&{5yRY9Q40LjbO$kD>z2xm)<95%A!<06u1TS#I7xMh4k~&nUnkV;;M0-`_z1PMO z>Qi?&Zpu1OEuoh_PAU|Bvf;3HX>iZlv3+_~!)DmmdtXfbS0{bO*^k>wa-4>n{%2j? zv)m8P{?tQ1{Jb?aof^HSZgzqB;*;Ql4tM@c%=iSHJ)O 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~ diff --git a/mCRL2/TrafficLights/v3/v3_spec.mcrl2 b/mCRL2/TrafficLights/v3/v3_spec.mcrl2 index 3804c8d..160c592 100644 --- a/mCRL2/TrafficLights/v3/v3_spec.mcrl2 +++ b/mCRL2/TrafficLights/v3/v3_spec.mcrl2 @@ -3,6 +3,22 @@ sort CardinalDirection = struct north | east | south | west; +map + nextDirection: CardinalDirection -> CardinalDirection; + oppositeDirection : CardinalDirection -> CardinalDirection; + +eqn + + nextDirection(north) = east; + nextDirection(east) = south; + nextDirection(south) = west; + nextDirection(west) = north; + + oppositeDirection(north) = south; + oppositeDirection(south) = north; + oppositeDirection(east) = west; + oppositeDirection(west) = east; + %----------------------------------------------------------------------- sort @@ -38,7 +54,20 @@ sort map combinations: Map; +%------------------------------------------------------------------------ +map + unsafe : Map # CardinalDirection # Colour -> Bool; + +var + status: Map; + direction: CardinalDirection; + colour: Colour; + +eqn + unsafe(status, direction, colour) = (colour in {green, yellow} || status(oppositeDirection(direction)) in {green, yellow}) + && (status(nextDirection(direction)) in {green, yellow} + || status(oppositeDirection(nextDirection(direction))) in {green, yellow}); %------------------------------------------------------------------------ @@ -59,17 +88,9 @@ proc Monitor(status : Map) = sum direction : CardinalDirection.( sum c : Colour . - (c == green) -> - (direction == north || direction == south) -> - ((status(east) == red && status(west) == red) -> % sind die anderen Ampeln rot ? - seeColour(direction, c) . Monitor(status= status[direction -> c])) % dann darf fortgefahren werden - <> - ((status(north) == red && status(south) == red) -> - seeColour(direction, c) . Monitor(status= status[direction -> c])) - <> %soll nicht grün gezeigt werden kann einfach fortgefahren werden, es wurde ja bereits überprüft - seeColour(direction, c) . - Monitor(status= status[direction -> c]) - + (unsafe(status, direction, c)) + -> delta + <> seeColour(direction, c) . Monitor(status= status[direction -> c]) ); diff --git a/mCRL2/TrafficLights/v4/v4_spec.lps b/mCRL2/TrafficLights/v4/v4_spec.lps index a184cb05c9499dcf2af4c271d29915fa8ab84456..4884bf00d4e0891f79ebed7ae8f6dfae47281c23 100644 GIT binary patch delta 2220 zcmaJNrwIg* zueJ#Rrxd#w6+;SI5qhY{wi=P65FJ+AuAX+s&9b3$n?=`Yx9;pR*LLIV^pE@g-uJoB z{k_lcdG2hSF9r+ropqwE?l1=C<(>7~7I#MdI>#L%h6uvU#G>TdR}AiveRfidVZTjc zvKVwWleq-|@fBu^O=Pi{_dyXL9t4ToT4nljv#dpL*bl|8kD>gbauV+-eh1YikoG6=}|dQB3uV2ibV) zp;zPRU;)}{H17jIj7Vpb>7lT&jhlWV6p4#H&!7W#;+7_}77vQ@AKq5dBpB9Ls&{1Kx4yL%8n$kwbMVSYzMJYHv5!-H5X z0ECK)kQs$K$zCl|8#GN;1CotU_unR=szDe7Gu4db)ohZ%1QGyZ5nGVI1VV#Fo=G$t zCVd}^ti@!5l0YUVS41C@ih-}DTgCL~uBjNlf6S5(94U25Z{vX712_v!ViHO)$ zrK{;;K(G*$fHKew?y>M3z$E|=FxY^^f#OXux{m<8UV`62>k(5o3k#0}lo?1*;Q?U1 z1A}+9g`wN&axq%M5aD9mG4-)?IxK;b+R>B1XzjU=6FPCf5I1ba4~aEHbIQ(jl(Y`U z;fS#gJH3w!%t-*$h$F(=A3)&%+@N=A421@yO7Gy?sBnP2#FW61s9G=I-w|*Ugz&U~ zX3U8ds_$H_>%jrgESoNJ;phMWIQ;(V1iC}s*##;oXkZ>)ZfnPak(B7tFZJyi2Sq5L zk4PA@2rfqy)7u;pNoVaTg1whPWx*mh471s6zt?~3_@3F?4!WC59T3joWBNN)^&D;VMBi&BPJ4HOTZUo9b(aXcxp*hR(GbBo z@6Ii8L~0vF;n~6|2T$tA4DTX*E+7JR>85r~1Qd2#dF_U(YH*HLQ`jZ0TTr$7$64=W z_fQoA?`uA;Si1;SXkWk4b%LT~bexR0cM+SY%~$Iszy54d99BvsbSLs=>M~4M>J@dn z+w;y{1q1MJ7~`yXAT1~F(adgqv^LMj+Q6mHC~jVteep?nS>G{qqRrI`cV!YggJ*`* z(b`v{0Y)?D?Yj{9r2y_bnryr56BaN4K23)cwie3j0gt?3EMvbNuCC-Jhp&uP=Uz zrC?PBfVZ*Cnui}|UdL2~5j zbFKWKyoa?hh1Q&S5qHtvHnc6;>{4E@pa*dahX82>?*m~vZRNM?2*_k|LDc2Q@KA<} z(4~E*YxCUygDBxFSEV?4^)zmg*DDzK$dJguV11{yi%$!K#`(&x!11v=+x-)=zReW< z^yf><%})IN{4}6kP_^)J{}_C;?bSdatJ*(Np(lM|xEGYzZz|+Nfal@z_4EU>q_Ol{ zl|I?=&{4i=C3Ix!XpCH49lyTm+cD8ROX|em&Q7Hzgo4k3VZ+3sy!@P;y{ZMb{8{wF zBee7;noY4hu=k^%E!=elQ*Wq3(>(XXyKj`V$m3euoj7X|iM2!E+7Wp8e)NT`aAxSQ z(t(HH{IbN}atwugQdE7l;P^?tQ2QZ^1aDQ6_qjBq;f&P&EKnS}O}})0=m`^Da4x`C zYdo^H(rZBI0z~!J508GoY;JSn2u7lr&83sWfQ~i%9)_ zQl0I|`L73gZ%t19v9L0!b{Zw!fnA7>N!n>En?&%Q$?5fla^~>FVa3O(zNEU5oblLP zdFjQarRm1}zw0U+>Brutg>qvi@=N|yQ@-cf)5MDLuWMC@2bC1=F7UzdQ5Ks&h70ng`BEANqCT(q?pnymS*g`XTHSq-$aB1BQMDdjjMa^z@ zubQR3ZO**A*0vtSY}3lhY-M-rrfa*q&0DV9UY`5h`#kq&J$HB8AHQ=x-}C!?&-tFu zIfEgW!+l|G@706$<_;toNvf!_*y}qIRM@&?48ji}(x|VOn%?R-x=)KYRaTlT2CJTD zFzdBegUJX3&~lU6$~Bu!``~y04FG;SDup_UNodsRYv7wVg@lD~jCf@;8SaZjVFNbc z1B3L%drOR!W^2vw>`r(nfHmrCtpCsF*#m6!^O2e?FaXS86(xBZfP_t901+h8C#+FpAtDmo@MElL__mE{N$l%GcQ zp&5Su;I%9m0IyA2HxLzGvwqaSIC^%#HQ|xKtDvRCv=0U#xLT`F2lw^e{sxDep2726 zh1c4AblPMX0NIomHuZ(w`ogBYuxzMhotDXX>7WYhCn){8gG#MCD8ageGWcbcn>0Js zW_hJv3jhEbVPO_2#LzgjrgBrY`31%n8_X7~+^RNPixf8KC(@Dx{eUuKer7@W1Aa*p zLjk0P^;;TL_}4TjfV3q4mIgKTYZ??lSW=3lELa8vQj4VPa?xlo0EmRZ_U%yP9PKZ4 z_c;I%ku(a?Kz|!aG|=djw~>&T(5Asb;C0UqkWNByw7hB!48X3B3Q|C*6B-Rxcrrjk zKzt&_a|qmOGtdZPgHf+GOU)*&-eQqgS5&BtI^FFT=wXaWs zyvK;(*{c1ZH?2QteP{>(cn#nKI{|wGU~jZHF*q<449)@hFi-#sbN08ARX{KYGh+9@ z-0#G@eXS&5qdh3Hc@l=GgQ4+mI|kp(^@VeB6lNVB6p-p_aB;9A|44rYp6n=Ag0rMv z-P)X#G!^&_H3w{&3ZAwRy-i@YszEk|>5T-V=)PjP_UL+|NE@WVvtM%*JV5`)3SQlpULp%J>0NbssuCTxmD*F3~^t~eBB zSu`{V!9cjIEGrSsgJ9>scbd5LA&KKQkB!dYa=Aj`cYF`1?#RSkCHvcg+PQP0J^t|# zuJ?kK%vli^f@cpAmY7#Xxe)C8bMU>wW#>q)|Gf;g%tj#yAGW3;D@s0*t&-rAK*&L3yCqi~{& z1V)#Ynj2TLYlXAc5}mj#7w35OooAdk*rBLg%{*bOt1l{VE-n9CT;;*!_tXVOiMRUR zIp@<88&QmBpAo8-TihTxq?tT<-s6G0CJ}U7d>x!$ro#RW_R*BwI}{`tc?ShHU=5TN zf_r8v|0f0uXeAz$r(=oR4Ggd8`W)9E>ABN>j!(+{p-L2t06VAPekgM42)-7mn=x8LT z3KWj@tObU&A&ni|{Cj2i1R-udx1>zhn57*PD8AQCv+%)Ifpvo-+O>e*6m**E#1OJ@ znMY-}5DXo;FtXEt=@!_;hZJ$H(O04)B)j?;1G^kzc2+W~6q`yYz-2cD)FT*=Qe)!_ zA}g1yW1AB~V%*Nv28!$11-yPJ5FJex#?0>i!wqq-TSw3@mvLIUQIMPb& z&cP)@4XTk7$pAP1RM0jkcsNL|)g7iBGRu@w|AUYAC z5cIIHXSYh2;LePvK) zg{1A$LevJ&A*yToVpSH4H*x%k=JP&ocI)8}N^h(FA&=sU|AYSgMDsrSc*-9$Do695 zZxMZ@TFG5%3=*3=RgZFzG)pdo1`?C9F?Btxe z>rU0>VOq-kb?Win!Iq)56C(~MGyVHb^`rF2GRR2=}Ur^RUjcv#%nS zJL?sXPtB?z(VEnme+gig^s%Jj$L_G>A+eaN^t!MMLw(-;1}=*? z-hV`MzYkzF9)7F%uIgCekc}%IMpK8IcR*^jOy?vWjffw+q-Nh-xDXL7UB2k+H$~ig zK5e*#m;Cfpw5EUi@BcIC>j&q%7+sC9emdt#NJ)o4Z<*NHmq7hSmVLj+HWA}orrp3M)hJK% zB9C2PDKwwCoOVF+!O?dwjXxZ|a4V-Ph>*AG56K4u-6uCUbyiobwFx6Gg(h~st4Gwl4QX%TaZBceE!=dYvOr}v`wt>QoY0d4;;6AROv diff --git a/mCRL2/TrafficLights/v4/v4_spec.lts b/mCRL2/TrafficLights/v4/v4_spec.lts index a3fd64c1af98078e553c6ceb11b7bf4573a62c21..b8da6f91e20512050869203ec3a7dbdaafe59a3c 100644 GIT binary patch delta 1916 zcma)&YfxHe8pqFjIN$-i91#`NvOpz4BH`ktF|igDsSsQd4@QZJ;;oo^TQtpWw}25= zg2`%-Ox)PSD-o48X?NYkNi%8EI>bcVZX0*H+jP5`wyWuEn>se#$cU@3gmh1I8xJ3;Uho$c}Z!1x;f^46qycKf~N~{T_tt@zW$*@MB?66#j)`T&73&RUroC{Yw;d$Yk%EkBIRr@hwhr$ZAWo(N z7R=&DsLY+_!e6u^i7;tX;ctam0`DgvG54vbQnv`xMBCEE+a*$&JR>tJ`h>Q~>}t$RL1j=9TU3&17sNEnoq`W_h21e`Vu>oiQDyOl!4*8E1=Kt|+92e7(@e_<2&y4BF%lrw>3AS>%SHT7^rgi8H< zkw&}Qdx%sAMBcxUa;cQff7$pf+{;BoTpiE>D%R4_X|Ar{czd;_!Cc>9MF7|Zs2gSU z9zY~XSsSK}g7;KV6s>Lb4GOr3#Hz$$R;Bm%NLHkPvT<5dTPqw13cZgJE?N#MHq+H! z4q0G}l|t}a5G{@er!Y{53}x^bsNx#74Z5Del8!J!MW-2C(eu)7)XZ4X-5!xo>f~1z z^kdz-&FDn8$c*wA?6Q7{G-Styd#6Y!#5Z*PaXb=3oFc0BlJo{GM^j26lT5?1$?mD+ zG<)sx=mURb68WUg80xb_mu)mm*@r10gm%JdWngi ztp>}yDK)P0gNcR3v-`i%bYsJz4@qAi{WhoY98D&=bo#W1p2PD6cBU<|tkc=@gOb7= z?@MKk^ZUnH7qhjaX;zVFIeqj+t9JWi;V5g3mbN6}o7Sx2ujqd0fMV!re_#9TAn&HB z#bcv2xzl<6*}1_hupat;!SwJBp=Jd^Fy(Ko-gTd`K$@octL9_lN1?0~<}8_hgNOha zA)M(epAl3?gh|vqHX$KW0&bqt5>p!x9`8RT!BdGzzUID+z{oxV46|<&?g%C!F;A{x zVFZifU&?Rm9mD`zJ0r1&8G)UePs0eHSFKmV2<4{@^=Ze)?BUji$lcR5VFr`o9fD_$ zRuK5Z)u8~}Pe_z0SL2+cq9)t|>T9zr#AKJ9(3-ydEg_+%s}Bhk&OUYc%iwh(F;TA8 zSRu&vea9On#3zGHdl(~sxIvz43pXs0uvWK|J(VBsAZ$zE0)a@{iO+9@8PJ-Cm4ia; ziyjrXtEP%D07=S#onXx^toD+ls+V6bj#k=k>-2mtTi5M`xAT~*ZvFfy&g+S%Hd8E> z6jy=+xa>-Q*FE(B6NSq3G|(8xe6Ob>-sJ6d;`Ph#XcuV*fFkvt{|pm#sHZa@^{CLS zBNK&u?BU&!Niz3M+*D=Qmf%`$eo>k>c`GVz>Q2dtcep{Lsn)IaWN9;J%zW6S;J*Ajr5Gz}fqv&&6s#U0Uhf@jC8mdp?K>zex>7{^x=zz4U>* zoK50fz_gFDhb#Sb=?tlkxB>(2H?6Vo^6vwrV<^ZcIw|3A<7 z&il@M-MDY@NLbt1M#TOuBoRRn<`s0&C0_sXa6toj3OTDdSB#R&x(1J;ur-Gc)u<}e zaswU+rQ`8_{sDnOJKiUP+mNmvo?cjQA3=U$kwgk^2Ry3f$JA*RN_m;OqNW;VC|cc#iQ1m7?aTqfIGOvt{76ZQQ-t z`*=BgLms>gh%_w1ccWakPRVg}#fG2YVT4>D7eHYS%GDB)%yC{Kg)bfLl!6krbYjnBcEh0n{9R&lIVJM$qSZEg0^-v}eu_n&cWd?(< z7!%-sS1_x(Omi$*QIASC6)P>5%E~8B!7fyX&*r~V;(czbJB6%IOJSJ;^pf)pK#{MtR!CV zId5*O+fb2GLU^SicXr|^a~mr;57^Ym)vM1qR3CGNC8#Mi-IvclZn5hmT`Zh24WFH~ zjmm#*O!6-k%D&+Y`_PrMyGQMV^BhXSOHG(#^>y*pWGo{?_52h{p(G@mv z98K46l$W;9t+v(EckOG9-i7Sc?mv9d+s7i$&H{RkW%f zaCtRM4Rb!)B?#{DAb`!E3n6hs1f6R;l*-woxC)M225z!Rllp27N-)t%4+ulAL$FfP z!EmCdJ0wN@4hzkMYlAPE+ZI9~1LJ)#1qyqRA&op9+v!B`5+tFB_hk^yaCd3qV)m^v zoIN6F$Q4QhUWA7ip;YRXTU`)h+&(4~Cs#4f7C;Pf5RhYoDx8-0C4|ZK5UdLJL+IH$ z5-@5mKL;6%13j7(5GOox5X1o^p*IBsYVz;L?#1*(VQ{0v`*7f9Ua+@^D7zz%v7H*)9@55by^RNhBL1jr|cL+8v(}0-H zJWxXJy)@0M{0qH@{5mdEhdh7N7RKx)4IJ6KD2N9*1)g2#|6~lu%r%j?K==afhWIo= zJN)L0n}vStZfPpdPi}gSIV-HopmArbrfDtW&+_YzhS*~UHFG|7ew&|jH)?m}^tw=q z-kX2h_juum@8+Mfd|h_1dd;3^zc(}TB}c68ErJ}Jza&UqaX2f_#ZLFBT)NsVr{;8b zUA&hEP7x;s{;S%vRC~%q=nal#!Y!tNxV~&08w(q>(KsCXdT_6;vVXDF*nDD?Ff}x; zn7J2IKwj6FyDI~bU!E#Dsi#>w^8BC7*ld<^n??F{s9oHc-z+yP0u+61>uIv&g!vKa zklCvJ;qg!$(d>S+qqKz-{|7-8?bIXo! zVRUD}n?3cxR_%|UPdc_0BAglYM>b4RL$yCrHNwOF_~t$RWD8E@|Myc0e+wrbMGLloLi4p2}XH1A9NzP^6h>gc_! zSoNLlf@hiIxjPfqYUvm4%^Y0O{wEb@4h(>AjIOvkncv+r+znQ_G2IYabT>M@O(W*q zH1D2RYrQ}7_{uIy2(72^bfKScq{=P1fYfu>P;3;s{u}Tu@=9#~9(jh7djZ_FF#L3y z{)&I9{bjAorq}LUqom?K_9xm%9993-Q(k%(|Vh_(NkU=L)vx+Q@myE^YJc zrH+WQ_rCM^V|M}xJ$S8-_#IBJzaR8ude7yzR|}=FN&on4Eci9=PDl2BpO@{&ZzT|6 F{{t~03|RmG diff --git a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 index 59c2fbe..0257d0e 100644 --- a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 +++ b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 @@ -40,12 +40,13 @@ act %------------------------------------------------------------------------ proc - TrafficLight(direction : CardinalDirection) = TL(direction, red, true); + TrafficLight(direction : CardinalDirection) = + (direction == north || direction == south) + -> TL(direction, red) + <> changeDirection(direction) . TL(direction, red) + ; - TL(direction : CardinalDirection, colour : Colour, firstStart : Bool) = - (firstStart) %beim ersten Start nur das Licht umschalten - -> changeDirection(direction) . TL(direction, colour, false) - <> %ansonsten + TL(direction : CardinalDirection, colour : Colour) = show(direction, colour) . %aktuellen Zustand zeigen (colour == red) %wenn rot -> wait . ChangeDirection(direction) %Richtungswechsel, wenn wieder zurück @@ -61,7 +62,7 @@ proc ChangeLight(direction : CardinalDirection, colour : Colour) = changeLight(nextColour(colour)) %zur nächsten Farbe wechseln, wenn beide Richtungen dies autorisieren - . TL(direction, nextColour(colour), false) %fortfahren + . TL(direction, nextColour(colour)) %fortfahren ; System = @@ -83,8 +84,8 @@ proc }, - TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || changeDirection(north) || changeDirection(south) - %starten der Prozesse und auslösen des ersten Richtungswechsels + TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) + %starten der Prozesse ))); init