From ba8cc850c7d6c412b957c0c23bd15e702cd4f680 Mon Sep 17 00:00:00 2001 From: Johannes Theiner Date: Sun, 10 May 2020 11:51:33 +0200 Subject: [PATCH] nearly there --- mCRL2/TrafficLights/v4/v4_spec.lps | Bin 3156 -> 3229 bytes mCRL2/TrafficLights/v4/v4_spec.lts | Bin 3439 -> 3763 bytes mCRL2/TrafficLights/v4/v4_spec.mcrl2 | 25 ++++++++++++++----------- 3 files changed, 14 insertions(+), 11 deletions(-) diff --git a/mCRL2/TrafficLights/v4/v4_spec.lps b/mCRL2/TrafficLights/v4/v4_spec.lps index 13c7fda4968958a3590a22479b2064b7b823ac33..cfc93b3f954dd0dfd00e6d81e2b0226aa6a9333f 100644 GIT binary patch delta 1767 zcmXxee^}B79>8(F0t!eD5GFdjsi1uQ#er!Fc1?b$KuMtFG|dTO^H)ZM=CTuF_!Dyq z=Fspi2o+6Dm$qE%S&H_AK67Ncvt4%TnYrr9y0*Jpw|maVd+v|V>+^n|&p)39Vwb-c z#BlXfnD*0FPcp2qw5+-{TINGV!@U7w7-fG!F-ShyYWW(SCzIzFl^j2D>adBn$?{sWNqr-}}V)6%7fGd|4BI+C4pH20&ARqFDJPtH`Gtp)&(0tN&?@MLNk zTd6FC2LVKnFd{Te@&CCd^#A~73MOKtchf2?ysw72AhQcs@z#eXyuZ ztU8gOt}Muh1He9j2S@-7pgpJ6nHJ%04LuP80RRT*zSNRPW6QJ$bwOGt+wiC*@pcHu zcG#LiVZdS#L|7(Is0JU`f_KdjX#0FGSX2*4dsY6e@xe>N)C1QWOTmX2ofO zx(HF)EG$RaMA%@zn=C7EEd)@0Od z2->%qJtNFTN0FMY60#UBA$vOqKEpp?%nBvjY59_{G@M(Rk*7oYB-0UFTd!Z|h+j-3 zVN-R2kSp+Zo@(UtdVQ0lZ(8(Rb+U!8Z?apbY0p)!Oa`y_HRdF|gx>EMkj38PPd>9* z_4H{ds;Kc7+${c0^!13%6q3X}bYsxE@6`d$+qK<#1e1y)%A0Xu8!77K>=Mu9JKSf# zB8!lQK*%)st5f)S;IE}H_(ooKcb3`#Q;ogC%V@5(0qw^6}dH23qQHN?=4AhE6 zL6Z9ZiUP_9Eco9E?;~2&0E(#h+fw$Zu_RWTGYPl($x*-ginkf*hh^lQo2P^bjls`t?(dQ4 z#_1E7zJ6C-uXE-JX0yy83GB9cQey=uDR@1o%f~K{3|&ae3R3@wFlqRTevUoOH+m64 z9;oFJiwd=Z?{LDrK)SWV7H=80nsud1>j5_`P88>lKJvJ{U8Wvx)Ogd3+$&MMG*hTm z8MxW&v{TGKa96JM0Cn$04sj?d|L7KnU)?91diqoslG29@VPPFqj`)GR#)aQ63Q=x4 z#IAUwAkA*ql#?YQi}i~F?+f7B#w6K;G+T2_4X;!2u4ydH@cif7m)9*LDG7PDTDgH{ zu|GpH=Lq-%cy4wF?=ZpFGYIO#PQHuoR;xZ4%O!wV@RRpj`d2;a1*O9 zHfy5|9O&wx9P^)RWORbAM~#g7pyN8W-8B`bp*S)(F7H7v#z>JR`i-7T>Z9J7-Sr=X zqjA05dvvp!oOWH-L65mPx+m4D8hqzm;pvRcYom$l8!j@YH{aakWbLo%fAhN(Yrr_J zF16Y~f7r#O6yazrteMKAkFo0aubjIPc0zI)Z25i1?K=q+A4 z^VK9>8hE}UVpBp$m=R1l@EezvH0>(u?XLSvxi@+21^3#}J$Sm&ZsBx@9aq6lYyxzuFmFKi~SbipUf=icj4-imL4cK1y#toCWBLSxaw`Ds>({>PlX zX{%?#@m?j_4cBM(Vr4(Eo|fILO4koP5wOH)iL~m*LM%V^9~Hf-(ZERO7Hg!Et#AGg z4L)|Qc7BF(S5_dPgBPbB-of@lQy2JEHQdnovmbC*Jzt_3=5PM|;B4xot+OI_SwS6d z+uikB=bLKG@vS3HR>QBCX`;oy$b%`>BOy)k^OTb*Dt(iiBA^ER^L*@!Ls--e!@j?! zVAqe%%9#hSgq&h|%(HQHQaZ=m#`*z+7<}U46842BmEy90Mnu1bZTza+T|GgE{1*kSBLrk0_VGbh<1q%TfCL}&#W+)?Vk)6B?TwPvY zWoKz?Z*zQ;WdUpfV3X1TECMt%k^&q$PESx#Qd3k_R##YAT3cgoaB*^Vc6WGs0RaMK zF#rJwL}7GcL2z(v1snkw0wx#(CSVu?CSVu?CSbE#0s#RbGynkuWMee|0Rv=XH~;|y zWMer10R&`YF){!F1Y~0|Gn149;0jlL!SI3}6@n zVtD~30to{FY?CkrLjzy|V3T$QV;XD=OlfXVa&Kc(aAji!0RcP#L;+0!djWlZll2AA ze_((B00IJHQK3N~fLwyZ0GR|q0CI*edO-sKi3*8Ug&dKHA&@}8BElk5p+_uYjARfn z2#Bzi=}=Trl%SYl4n!cqK|w`CgrL@fO9%W++c1?Pok2q2K;W&s`^9$rg|9oQ(MDX>W-RbaBn zj#g#jAtNd(aZ|e-oX8|XMp97Xmv%XMldT6Ie;7p+P%x^fuc0*2PeSXWu7ohf9SUiR z+7inYv@NzH*hd|cu&%l*VLb6h!u#yCga|P!3K&Y35-8*>EOCpNM3Pf5si!JoGR#E6 z=aR96D7hmFS#U_`0s>MoU{hJi$$>|p0+bd&fx@-01m^&bV4&e#3aeCC1OtKww3cxS ze@J5BtXvo#l>vjj6x>E>AyUH`uHttLjX8!$aHy>j*aZaQ1s@8hWGvVG9(56$p6dY!in`aEo0~e+nlgNec~Q1r*HQD~G#A(5EPq7^xdN+Hl) zP^>#kgbYq-k{M8J8p+cknq0=EF$F`A*ovtGWfqA=vKKL!%OUWX zH8K$)kjZp~K(sr`C?6h1*BknE~aTWLh1bKzEw$e227bY6z!>B%jTBIBVR zgsA!!tI+ixglR-n9kse2Cmu;`sV^N!^rc8JwE>5#^dmtcAnU9#1{p|Vv@oYZO;-={ zccon5z)C)fD2R6onurNBe{PgUQi7(KX8TrC3c!}qVcHzHOd(uhiem~vV0Y1&gNZ{F z;wh@hM{_BsDtU%!%qv!5+Eo$mm8g8OP+$tF=mErm?2sU_OgvGwz&Eifa6w|S$>mfbNp`58cAEEGrcZL~M zOYIqQR;=?80VDPC6mG_zBa7RW#Ac2nNI2HSX@_!Hh*ZQ`GshYjk0kD05z1(Ytm9P? nmz~I>DvA(U5!O(EMQ=D1N>vF;D`1k}ut9IwCpYX7oAwESAHb`r diff --git a/mCRL2/TrafficLights/v4/v4_spec.lts b/mCRL2/TrafficLights/v4/v4_spec.lts index 42ebf1cc92fba2bd5be51b96588d84c43a348153..ee795b23d444294d6e759132041651b7f22e1072 100644 GIT binary patch delta 1982 zcmXxh4OEi%9tZG;Hx)%LBqo}A5fKs4o0Lw?bwLr47hh0(L2J1youTHMN!dN!fo3VP zoC<38a_0-61T{3X<#MymT&b<8$xUfBZyQ@?d%3Oc*t&P;YR^A7oagiVeZSB7pNHqC zpo<}`ClJv?EomqO->`uCgj9x*ZG4ftc6)HE-Y!#ek=olAE$Dqn%~mb+@Hxx~QE67k#CD8$Bl@u+^1R7ZF>1{#+wza}Q z)O+;*3{!(l^?BTaj2!zj=-|izj0=lb0rwMNAo_MJgZm&F7v6d3E2R@Kq0We*;985R z1dLM@7>G?lvi&fTW{@GpHr~X#HS0h8dtiyB_wN9tgCn8s=j@eWx1RgQN7}* z=@YceJ|JP@`o20@?fuJE5ckc@e9;*BS3eNPm)QS%@+rp~#8BgmMnai@Lv%hULFR;U zKx_g4(llQK7~$=gv6-c3ap4(7vLv4X5rzT48Ju1Kl=lEkhg-8@A_`deUYUu$@n38_ zKg22TalLx|YPbVI<*3zGU=FwP1b}KIahkS0Ov)7JN z{bYG_(ty8(Y_Gwci=B7a(lWav{6p|2$&!M|*|U0l!fDyUtQquBb0|SdF{b$5D`4fnBB4ddy@k=J|9g!^z~A522|0SMWj{xV!nYoLy3uKs2ZdAA!c znVh3YH>1LI^^VBu8?=YQ(QxdWT4ugGQyB4|yctiO#ZjOXSSIKmo*C*)m#3}UM1sGk~YRo&cp>4 z@_WY9V)it(!AAEQ_F_uh{}j5HlBI;++>XQB3}y%4{UF1AB}UPO=8-lhW*MGSvpU>$ z^pCwu_wj@#P{XUeInfebH)1>I(Ruhw|)m4r}H8+{4r&-=2`{2B2BqX1(R4a4J z#RfiOmy#%SI#p64FRn9fTYer|uFMfRJHm)XH8S-+u`!~sNEs`PQ>(JO7OuU{!_kHp zEkQ1AGy6i6MQ2w9@&>WYBb4Dajro+TRe!5Ds`J=+)~N}3VWv`-c}dOUb@GZjBIvUt zXn}GnYvhMw;av=N=jLvaEW}61wHhs#La3fcXFoV(lCQj{y=XX9DB zCdH{Yb`c8Ze!W`wgOwc+D3BfHPQ3Puk0=LoM564@@;#a*_47?7bS7%b#TbFyc=P&J z+}zf-z=JYBvWuh3nSI8qy&c!|&8W#ys7%a|8fbIukSKnDF09kNEl%3MJ@qxoe1hA` zCI#-!y~v*0#^-RA&xO$kf+q;ict^gBKem4C3NKeroxSv#neYbf_rkpS&xUTz?et&C z$(`ZMUgWQ(nb`IGOq-0(?Ul%S$k16s#zcvz$O){<&<({U` zuiubrc1tUZMY9I$L8F{?xl$E>@Ag3HJ>-vi?8vZn{C(xj!7z1_+$*GupqdLcYKpYN*PX|5Sy2 zvEA#ILHUO(;5P=*8aa)!L&44mL>--ly6P1ye?T0HWFGC~2Rp*4(gM#iass11JS8iy zF;9k0TqjcUuf`fAITbz zOw)!8EX`U0AMI*|nl-LXV}^~cThl{bE!y2SYo=-1+1h(O_mA)Qecw6v-gAyU;4lBS zRw%}*Ww}B3=$&piv1w4jmj{-27)dYxu24pYDJSf`@G_Vp4gw51A5iE37EBntCP8{i=B&sF)I^wLex7I5A*7agdW11vO=a^IuyoNg3!-Yv9)9mUyQpoI^lK34wE3WygI3}dbF zg8)KZbO4aHz%{TgIb6niI-t~RYYr%$a9fXwqyG#JWZh?{et5zq7;;xGE*%A8N z$~&p5vm8`n0_vQlKRP4kYD2NHjVq)j*p84YnfQ@Lrf~u<+&2Y7@8y#zFrqm>$S{QE z>r^_=wssaXzJt=ROroAE@5iJMG5+Ws4Dyv=WnjKQBY+X1lsMy1g9{NVdToDp`Tbu~{5_k-tPwyv&eY zODiPQ@aj_(IcP)&Ia955_%Tixe-3UhToO~Opr|a(+ToQa!glk_&K%v-7j1|+v216? z%7-}a>1Tv9Ct?m_5s(}-oFz?Vd|6s#JVE0dr=zH`P*hSv`sgK1cRGPv{>2OY9Z}K zxq>PF?P#N_;!*v0y5$YKbt*~dJQbYJJH!whNb#}WFqWl>)A}ub!Vh6gJyRqQV&G4x zEcGz~u`}1OIUUEfDu~^3M$AI=?NvFph%K;lr)VTKDxK(`Z5UsUj zuOFtONtHayMtVdG^S+MD@L3!xT$SVck_D8?d&4p{D#=`&W$2tAikK<>)wZ%K_w5r4 zUS;32lls|~C0^-{8ix;;L4IJve*RV;Pp~YWw&N6PRGK+F$Dn;YIxv&k9(GtT#+$a2 zg1D9syw^CgF^nNRx%0`$L1&VsKEw6VcS)F8V8jJhE(CdCAkDjycs|SYBTIqF?w!FS zj@N_q)@S=O%9vxaI>KaO-E!Ugi9=HVN%`sD7~5wKN%51VP0K9pU09svL-eq!TVtu{(l`_Q6Yk*5V`uCJJj3GFha*vna7uS!GIGQ6KonM##IEHn1VusE? z#J@j=ZX~bY7$LYs)#$;HjT_f+u7zrJ8yR1FGr%R%qD>)$+6x%hf)=eLpZ#Rr;Sxon QZ{6+q)aU0~h(tsF1CxgzegFUf diff --git a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 index f961434..3794ae5 100644 --- a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 +++ b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 @@ -47,27 +47,30 @@ proc TrafficLight(direction : CardinalDirection) = TL(direction, red, true); TL(direction : CardinalDirection, colour : Colour, firstStart : Bool) = - (firstStart) - -> changeDirection(direction) . ChangeLight(direction, colour) - <> - show(direction, colour) . - (colour == red) - -> ChangeDirection(direction) . ChangeLight(direction, colour) - <> ChangeLight(direction, colour) + (firstStart) %beim ersten Start nur das Licht umschalten + -> changeDirection(direction) . TL(direction, colour, false) + <> %ansonsten + show(direction, colour) . %aktuellen Zustand zeigen + (colour == red) %wenn rot + -> ChangeDirection(direction) %Richtungswechsel, wenn wieder zurück + . ChangeLight(direction, colour) % -> zur nächsten Farbe wechseln. + <> ChangeLight(direction, colour) %ansonsten zum nächsten Zustand wechseln. ; ChangeDirection(direction : CardinalDirection) = - changeDirection(nextDirection(direction)) . changeDirection(direction) + changeDirection(nextDirection(direction)) %nächste Richtung freigeben + . changeDirection(direction) % -> warten bis eigene Richtung wieder freigegeben. ; ChangeLight(direction : CardinalDirection, colour : Colour) = - changeLight(nextColour(colour)) . TL(direction, nextColour(colour), false) + changeLight(nextColour(colour)) %zur nächsten Farbe wechseln, wenn beide Richtungen dies autorisieren + . TL(direction, nextColour(colour), false) %fortfahren ; System = allow({ - show, + show, %changeLight, changedLight, %changeDirection, @@ -77,10 +80,10 @@ proc comm({ changeDirection | changeDirection -> changedDirection, changeLight | changeLight -> changedLight - }, TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || changeDirection(north) || changeDirection(south) + %starten der Prozesse und auslösen des ersten Richtungswechsels )); init