From e41bd51c77fe6c84ec48f66eb8a0d6fe95657791 Mon Sep 17 00:00:00 2001 From: Johannes Theiner Date: Sat, 25 Apr 2020 20:43:47 +0200 Subject: [PATCH] A2b_v1 fertig --- mCRL2/TrafiicLights/v1/v1.mcrl2proj | 4 ++++ mCRL2/TrafiicLights/v1/v1_spec.lps | Bin 0 -> 1103 bytes mCRL2/TrafiicLights/v1/v1_spec.lts | Bin 0 -> 11593 bytes mCRL2/TrafiicLights/v1/v1_spec.mcrl2 | 32 +++++++++++++++++++++++++++ 4 files changed, 36 insertions(+) create mode 100644 mCRL2/TrafiicLights/v1/v1.mcrl2proj create mode 100644 mCRL2/TrafiicLights/v1/v1_spec.lps create mode 100644 mCRL2/TrafiicLights/v1/v1_spec.lts create mode 100644 mCRL2/TrafiicLights/v1/v1_spec.mcrl2 diff --git a/mCRL2/TrafiicLights/v1/v1.mcrl2proj b/mCRL2/TrafiicLights/v1/v1.mcrl2proj new file mode 100644 index 0000000..e9162bd --- /dev/null +++ b/mCRL2/TrafiicLights/v1/v1.mcrl2proj @@ -0,0 +1,4 @@ + + v1_spec.mcrl2 + + diff --git a/mCRL2/TrafiicLights/v1/v1_spec.lps b/mCRL2/TrafiicLights/v1/v1_spec.lps new file mode 100644 index 0000000000000000000000000000000000000000..f00fa5580357ec4718a487961a012fcb8fb44ef8 GIT binary patch literal 1103 zcmY*XO>7%g5PtJ^z23E*AKTl;Ar0708d8@4c9N!`siA$0eCj=oCrJMCD*|6C) z>vfafEGI=lH52aqC;1rCS`Ax;Q!LPBEJPD86by#40Q zH#6TikG%iI692M4tyl%kQ1pyuG1b;ggMct$T6V4gqDXvgy@#KBe$ZuLWR`&M7@IHJ z7pHZtWFIF$2zVxJtE}2-(VtSot zTE}VL7i%i$e z1p;E7Tx2RHOQJK?L<4XhgDv8i4YuT@r7X)_pe~RAyr+w~!nm0;3T%-!HwX5k2pa2q z;YHLlM1$ZSQ;NHVBpwH6DCmS~>ew)&*h;Ec)TsnACr3hVCvfr|gXho%8A2d?cO#Dq z)F}?&0b0Qi``{_QH0w<7N~!2O3O#_j@&6ISJFJ^CQ;M~VIZ3VSn4ZiMXmzUN-T(6o zLO9yh{p=vxwU?K`P3?h!$H5VF4_o2lDG#04cdV@27=RX#T9RdShpaY(UXW$4NeaTOtLe}_oa*A}ciC25bSh8=0 zJ9mvhBwW4Y4}{5kS>~@^CAC-|Un3)nH$-`<3j)~>dso*}9kT=X!@}hloAhVNxU!QB zwUYk8j6WUNs@+=NZm*7H?uItDHb!gWS3AGO?&!1pVqEaJdS0a`9(sq)eVw3Dd6=&T zk1k0U?!8+~(fomLE>(Z+u54V`46c1P^3nI<&9k2`ug9aY#QpZy=YARVO|Go|)jaq> zekI)&y&J8(X@4BtS^jhFyDMuyU0+^}M0*ok`-Zg5esOZe_eWFT1K+7yTlC+a%8%A3 z!JC(QKOMWW{qv2?<;dLOAAav#(6)!fsg=L~>3Z$*p(p-DDW4fAX|6++78`G5$vnHElHLJ6xnd$yb^JaF?&xhyxyuaUb z-uGPO=n;16_rFHuUDtJ5*axWvZ!grwwGe~})Ql?mS#75!uaPm>`y z6!qK_l$2M%;SdBxZ!f4aRn=9)pl#LVWm{YLRdsp!lSy04O{S`2FbMT?v!(pdR&f;S z$;_lrVOzAhynbt{PrIX@l+miItB%1DP!t61D6(+NgjHN~S$RGD`R8Nfw-%B@dij+n zYl35;=L7}|$caL1&AohUP4ucN)7JJFhFSy7Vllyy5Dt#RKlg;0N6m0~Szgnm-4FjW8FbdboMyLJ;Zwif@lvW%^L|2N3` zd&t?ES&i|@oQ_T=Uj(*(R#0 z*=l=gA*qL+nnJ^qBS<~;^ZPdHq4d97>^A7>+V-03j_9f?bTzeG`87I|;jMC0jm}^$ z+uBlPZKc8VbY!di7h7LZ=p*H|23^_K0(Hi6Ls@zC)-Fig+Wk?`YjL&J26N3;PnB8s zf2SD?inEvum1f=FjXpVt5KVvhIq?_pUy`>|%~fUPRJa3+ zpBEW(q|Q`ZsWbe1e#0AKTc;S5w0&#uY;6l310_RIgr6sF+Uoeb?bKLnYRivo&G2=I z{A7;VXd=uHi-JXwV6hFb8$OiB1>5U}-)Pu=nd*meqEJc%gA2o?b#nYK6YRvRW ziALoR`%@Ps63Z*bvKTwj1A}m|pI=+oPs3A%M?QVux}a*4WW2_lHblzM#V9vx+Ps8| z!L;Xts@LjHdS8XXOU<}5_40$LOUMB!P;{Vzb1G(3D&t#AhK(4$$>!K+w*@V4J%DlzK3crxHT_Bk=S>4~ELn z15$V}Esudlu{>zbKLH@CJs7u#4~XYMPkagVro@9;jPL-_J!sN3ph;Q}#_mi3#P^{4 zUI)5f=E3yI0Vo+B3_0uFXXHWq{TvU*GISI;A`co?D+ECGgjfCmG((pXrc#Si7V!sw z6Ddv!uBDT^%#RZ7@m72z;9&DGZR#Lm4U|#%sRKm6 zEOl^zzI6@#{9>dIS^@?D%G3c^vH}1n)xgjJ-7QMhkADSVl$vVrQ*~Di<6Gy=&#%0q zEBcg|0VEe+G3Z6?D~3hA=87R@3E1$$D|*j600Po01`(&=iot^c4!z`xfnpL|F%014 zR}2;s^NJouR*g@3o{mFhyFsCdJ3bNle*nnh@ySRr01It=k{C?{R60KCZc7Fr9G}$l zo=s3OKI!ZN1DmYz3E8g!;ML=kvN`}t-uOgl5&%UqJ~?xj0f;_6NhUm-xORMUpeqWD z@W&_Ie%bg0Ow9rg<4SnwzkrTbURkXD9{_EfE8*H-0pN+Qgo#w@m9Sf{V}|wUBIe@y zv#Uj2%nYxe1ci6m%*B{g00a#)9McY;W^_{u zY(^Nb#5Q9p0`+YI+e~e*+!i$b2pl!jHp9`YY(Y1JYnz!siET6M@ig1az3ZTWP->fr zxh=E>aTy9*u#d#D1<6jeZN^{Ev(4aG659+cLT~Q5_adn8)i%3pqxsG5ozK=7FKh0> zGZ@W1ZmP1`?TT=k-RnG2bI;DtLCbAwvpeRl4%x$J6(M_+&SGQ_nZri9TZS}9H?FG? z>4u@D$XsxiLEZa7pQQjv(RKjXEJ5Z*@&rhVk0(dw`qWHhuKt1r462a1&SWlcLiy=jECX&$3a{N~x_3Li(E_y&Ml`Z%igLcwE{4_)#&%7+p>j?#C_AEVZH zF(0G;^6V<>QawgFGq{hVVjhSeMEoyYxbQIwCsaH}!A4n|J%9NRka|JA z>4x70u#30ZQyVSW>>2N-Z@N=PwVOS9Du2_x-X`1Zfr~-a1IA{LR;b+UiMh+!?D4=w zn>~~Ob+c!HqpNr02u1a7n7-JGL_95r-uqY3hhke1l!(TPY#A-IBIv!q-jrIAzS;sS zVj{W3id^gw0bgK61fG3}*UPQQ%^{{0(HBrz5okZxiXbAyR)pU~vm!0wXZJCsRs;-V z0{ud3R5Barh{B4ZpjlQFzDI3Eoq6^HsFr7q@>wKSlnX<*MlE)0tx;z_11&>*Yt*Ju zW<@E(3~ST`LTN=2DI6=Rg(k8_S>RMF3YMqy&Ajy-s2?rz&5ZXH`+_ZcwlDbBabPEF zd^0JSLf^~;S?UWeG75Y%f4Tt10wul~Pgvla=_AQ~!Fm(Z7o^Zsz8Sxg>kC?(V&4qR zL-QH_^berEr_`q(?-u&>c!t8KkNpDJ7?w|;lBf3RT^^p#ut=5o46%O(V_~{a?}2N5 zdZm-^Gtg-=pMgSW`1CDVN}s{P;rR40k!U2f{%JY%u?F;Us3R$o-vJ=$a#JOl0E|Vs zDYJhBfG^HXoqY{}lAW89(FuT}$xY38c281Yn45}LQNfTjH`P8L3!or3Rg_BrP?DQE zGqMwaAUBn4%>f|KO&xgj?Cyt|n`%Ms1tY556uX~$ARK-AnIS%~*merQJncZZ4GSQ* z^uQwTuK-4b2g1B^09M6;#j8O8k5~u7S6={tR38YVsk{SWyIyi2EJD){gl9zB17R|m ze;_chMUapcN_dV@_Uj9$eOyW>v5~qkF`+^3XdMZW!MG^p|?uL9etLTPI z%Wjj@& z@+%`O)n%net-4GW@l^hnT8Zki1x;7^y^plYx*Ja;pf_qjmXWWl{c;b0dYQ6L0%s`e zz8nD#MX9Wv@pF{58FZ1dE+ary)^6tNTy>ksB3GR#-w4WzU3G{@Y*#Ijt8vv0jO78l z&{bzSDFGmL)!I!3oy$L71O~jMGqU~JO=m#Rxh&zxJD0bsz%ZTJ89|s-oskSYw{tmz zB<@^J$)|NjJSR&#mqjXJ=dx!^(YZ`XVs$PLjHo-8E%Ut2h+Qdhwb;G`8M$;(!GSSIZ_^nPvIo^MDgo(d= zbzX(PoYKw3`#qy#{ACf9hQI8|E5%=?Bn$DE2Sf_|Ws9DL_j|2syukG|0^0jqkcH>r z`Mo6oloGt4_YnXJ9nYV=tHldu34A<1qf3V8ll=@lUpAt|3uIOfo*#N7!V6|HIiP`x z7mzPz0MM-n25Q~_P_)8#bBkB__6+t)-0fcg_pW9I7k>l*p>QQGejY%VbOkrdDOib{ zC6%n;GK_+ixKM_CC2l>Fxq^$is9K4Oso}1~&8WmHapZa0O58wh=?V^q6|Ugy^@=;j zjsg%g!n#x0@jL*l`i@c258x5+j**usxl_rzNWWveTBE&FS9Ds{#DXZ3aL^jMfn)F%&sy#CO=i<16OjE3HS9f#HSU+_eQs<#+Cb$lId6Nc>%D-|`eoM_ML0i%83}oMO^4X^2f) z4s~fr%R4oNq)1Grl(fuGEFdi_vr9Qpr3#l2X4ZA*uS>=p+@nS4&d*)qIlD zT`MCgy@`ypv_F3cB8Qb}X&ob+w6w!-ZD27d`=z8rcMOE|W1qy_Be&pnadsnV|7hq6zBZI_dKp^utDG)2JOY4OXsNxgI?H|fhR6?f-M z2A8`t0C-tPRvvoZK zu4>%~3AwH7f2k3-t~;@`){U5brL7x?Tw&`v5vge17|3U}uH)G1)^&S;cdGo`ToCy{ za;khmNIz8`e^+~|d^?*2 zalNG3XFPjye_If3V98*W99Z%v# zlN2M8=(KP4(W6Pn+1hB*)l7bLTD4Ucoi>`sh$hu1E2Bvv5hps$b3qiHM%hJ;P8*2U zJtVowMGr~di^UIDFK|I*4g2BhZLH?u+T6avhpVhy>BH4(WWmGLtNA4lS1Z_phpT_# z$sevd)y#)$F&9)1*AQs#!&M?m{BUicoAz)Ox2yEws`sRDt?|N95V=pW)*xiF)*9zB z)oYF4#+YcvTBE01xzjajCzLRpx0-DRTED+;VmIZ$j*K*5p3=bwLwk+6bwCarqJ-`?$tzQ4qD6C#5 zgca2rMg*&ReTJg0-XPI<)f*XbN%h8=I(qfSX0En+U3rXOy)h9dt6nEQVpOlU>{nKA zSn@g5>vp=RI<)IDhzwAxL)*hTZ|DnBk@tF&sn{Dr(AeIPNU8B&&u|ucLw`Cc^@cph z3cR7d`4aE-`Xqt(I%U7y8}eJ3-s_fZl{aM1;(C{NHG;^n*c;gnr+Fg;XQ_8NKofc+ z2)e?%Ov++;moqqO?{e%ho;Tvjmv|$}Y`S-uzF+HIri}5uk(ObZciEz1cq4Yaa)9yK z*B}zf8DQG#L<7vOlhgr5G*?GvRL2#Onck#gGV|&&HklDXX~@jYNFkZgH!3AF(3=Hh z2C=q;%fJaRdA0gcDS7qqej$17 zYQBQJb|%6iuWh2$SX!lxmv+Y;2i)QVA8ZDl+dwSTj_CCF4w!J>NaJHR-kpBtne9}@?uhlgoF+ErC)kQUn` z3{pMaiXc_VUmbzqBr@$QEja(ILc3E z1V`y=WpK=FgXoEU0wY}Kz5k1isL#G`ssv3L}n!4{7aSsL-EUsxy}b^ZTO##oEdr_U97Znnorz~kM|?b$)aTmGm5w;`#8Tf1f+qDXQc9&G z9GXx%GQmY8X%N;{n%j?~34iKMQ28dd7jD|L>}dSQ{HlTuaeaQO*rhs&L%akyZ;g^uR0D?p@L z>S#U@U*Kpq?J99J(NO|Nvo9idG);^$9Zl=IRgR{i46dWe$r3x7aYCA-30+_6Xd(^? z9Zmj#!qJ4QVmX>%J!(7Z-Dkh+#`Ek^CwLM&YUggc9d#z6wMY5Td^^h3BeSE{FEH$= zS6NCs%Gt%SNAasf_Na*=svSi%>d>f`a1k1Xdr*u53wXhJWD6|MKmV?}vFW~^9SrHU2f2;5k4eLx&5ri5v+B0s4#R)o7P zj1|Ec3T)p`&u*MCENtIso*LVC&cnm@#qO41`%*5@v3;&yEwuOgva62=CE8kcap1Z!^Pt=wVfO4+YK*6I-0(FcEi`7AC@|rHk7Z zpROBf@Cz5=7KCCEK44-k!dElYi|`p1ZxJpMN*3W{8hvrwDp$J*UyS1~!u3hAMK~JE zScDT3m5Xpco3jXa?-wn??N!vpZWKbN@3v5i^xZ~UvHnvdi>>dT>C)&wB~=ybyUBE^ zzI!FEK;OOis6_uMXTL!I=|rMj-%YGx>bqND^ZIW07+2qIe;_uPZkT8WQxmP!U>Z;g z4M&=U3WEtz#WI*g1hv6L&f;x7Qcsc?O!fQe29w^ZH5{pD^9@HRu#myzzsN9{+`~$P z$$pz-SSZU78E$2efXF(KT_uL9qX?hlhu!TJf&O~X?EgZX` zX90~Y=~*Dw33?X%C*?g0IM|h*1$$WKUjKl_b#G*KiQOAhRW$d8aj4Y2K4TQRH%MWH zdn5FKi-RmvK`0jPwKAC&n4rjPS-9n}N`a%`Q z9m*nz+}E1|RCfpw))7M@QW5cb=yowNl*eWhuWMm9iPv!#3yIh3PfCf`DaQ(kA^&^{ zF@)0yh#|XEPMms=#w1QP(N)ALV-}Y<9jFo$rw|Wl#A(v)QsNXDFCc?2b zY0j{kI8BFLB~DZJNr+P|8ai>xJ)$K}+3)g+CqCxNh$kP$F^DG~CMk(0qOly}iRwfV z@uZhcC7!I_uk)W=-7NB-SgbAfpU@|>{U^|BjsFBOzR-Wdzf0;r;l>pBPk3Rs0=}2y z1c8xAlDabXE_G0xm`} zHQ=hp=;$szxrp9bzpI$uN!iV&yZmh$y36e;q`SNtDZObgwt(JrJF$e`ymdcAZ;D3B z=}pyjOnS5Tq>A2D0h^>Z4XMTSCTBd2-n?}`LvKQ(g!Cq2L_u%zkFw}ZxZP@cllK^p zZplfM&@H!X=yb~^*aF>hw~kM@ROia*mcz#wbW6oPCEfCBJcn*^@i2jIO*oYRwzH7u(Tr6lr|9G;b5q(VUkVfAvYDlA8pf-?NdUY_8 zTT}!ic{7WlvLCA0Q2D|G4OBjLyAUc5gr!g!0$u=>lbj_`dFZYHDmw_f4wY;7F`;t4 zMg^7Ak8z=LO1>B>YsscTWw^{zsLak0LR2zEGo z>mg%BrWS%7+|7p|?FAVG@p~B%MDI~T5T%;~!CDw12!@NMLNKpt$C)WC97eRmKaJCO z$8JM3pjW;^%(S4&U|%sQsZDUI;LHLx0HI$FmPWP1n(&7BQ>(m|riP15#6AX{$UPH? zeQOVj6ck4dq8iXfUz5+y*%6Y^PjHeEcVFAHCk6f9aGc#`Z-oe_CU_hMb(o3Umy(R; zowvbLYNK+R%l`-^RWS;nLcRqdtLkp(nm-`l5xo!y^sUG4?jiz82o=!O;8T zR!>W!dT^&U3;P%%FB85mlx*ZCUyda}d8Bqx>xZyGG{?v2Z7JF@E=jIoyvq2~YnW6I zHZU01(lxsSgFiK1Xk@GoF=O`)C6DuxC$VopFQAg!<2auLQAbgyJi%ySEX8bhB+<_3Cq2B0idhb;+`B#oWV;squc?||Eo<3)k%SeEsLSHkMnLvOv0Ssi1ny-(dyFFwQgqX#kiYB0kPgnt%i{DizhdvV8* z(B%<*)%-@vl*A|q+`?8=;$9Ayw$@~IVJv@OJZdZ2K@q)0zw#=h`_=UH3P<3hIK1;> zA?CRq9|)Bm%2@N>lykE?g@Ny|iX_}C2370ZFLYrBM#neaFWR9Lzs36FImWqH2Qv*b zi&#DkYtCAXyW>7yHuc(f=$LQ1;D628&6hWSx&60A5Us1B!W_7@4bw{$oJ37Z=S zzH>7wmbWK7pMzu_*7dl*TjWD+9r=w}X842DPOrFfJYgdnx%Y5!&+nx(yo%-H z_>D|tuUTUF7wG`2!m~G_Za=cZOgEgBt_mw675F-Gb9^PTbAP96`+eb_)YCX+MQAo& z)z7q@FWM7#+NpdibTv*jQf`|T_GEW`tSk$C|B`AX)%Iag&-14pN`2^?*!kg{w|>x9 z$!^Eb_rGSV6Bv?Ce|+O@*`MR)M~>LC`QiN2@|7d92QSU{=iB6h@V3*A8xoB1i^i$XIz!ezs6g~5^M?l^p{T0QOwSzIO~|yRw+o|fBN4jhn@fZl69=m zmc}1^v1|5*$@!nSM@uRF`C>^gNmra^w?IRAGwqqlh(3w@1Rwc#sJHC;0tf%8UGs^m_ z*qA{_uexKSH6bCVtg=eh-s8Bf=ontZC#09%F)P}?c65|>Y^){R$u3K%qPAaf%!xZT zD)DzR%R5cI%3(%g<$*HQVO4vF;~ja&awnnk&9Zqjv)$%+p`>H_cw#>#l6$zMy~`n# zb}Y{m`tu?q=7RP%$LpGo;m*XgHzHQEru}1wxwvC^o{)Ah^2l7={+?r(u4AJ!aWXf8 ztYWrzJ4!{0jd{Xkex$jop#1~KL8W42B$0a{!mKK8cRJpcDW>BI+&3dv4$H(%4oIt5 zW+t{$aH(d#*yW%}6vIqHYaZ@%vqaqD*rQf#FcYKRz?E0=#de25q1Z?zL>-JRPFe%y7l zTznS0R-)Kg#vdg+v#Z47uduCB#l|NIgIUhuD!KS~*h!7z+$H>AhO^GB5nsgi7c0*F zIUzmAxnV9A{}y{kr`Q8rguPPRgVLL^0=i?KC+0GBmqTqS#ymIbb2R@kT6quF4 zVeE)(ZsYj`@qXuYl`{A__K|k(Tq9mgmc3@y21l^XlDUoPg!U}?dGqg-bqqp#p6rNu z#?XpQRm|Q0F%k2I?7lf+ z9}&X&vJ!JB{1G-=K6n4yM8g5uE%R)+16x-zckdFx@TM%^eA8gVJ};fS_vgeON@&dd z?}jd{Kr?smAfYEObkcln>&fG5#dG)L6ZgCk`m1@~@G6`GUL)aheyG5F1M>kkUzT$ZlSn%d`lI;=u@iezn{z*oKzlRv z3-i3V3A;^_b6=j=NXh!G`KH)~El}s&uOl?(WgRll1Y5AbP~_bIFcEqqYstJ2v||sI z=A7>&KnJt1=F;>AELNOzem?Q1+$@J#oc_;CQdQ2z65*%(ENPWE{hyXHiSHiB z`pzs*|IJcONzR6p@a~&gndbTS_m_4^bMC1UzorabG~a4Jy;P{lxtB}$I&Y}Pe6#)3 z(ksO|_pONs-x&IDb4cu1dRv!s?+W4I!J!@IS@Exz5=EEpFD3qvJ9Nq%O#gIAqr7xq zO86mvsL*r^^Wo9~*(Fb5V(EdQYi7paCrkgJy|i3ND1CG2mA4s#%}dWoE=68R{ESlj zyDG+D=Mr0eX`_(vSzhhiRrJBurG1J^=Yxs6-l+XgvtqD)=~tzf&ZQG}9jr|>mku^A zy(GT0@pj^a+}hJsrGuX>6{{|tUn4xouhp1UgC8yJmtWdAooGH#d((Ui)3J1{o$ zv3aij_YaQ`b}#9a??m1we4D?{uHqd1 lVChZSJNF6`g$LIE)f^ghF8!nSoqMkkgm13zGfy0a{eMh?1RMYW literal 0 HcmV?d00001 diff --git a/mCRL2/TrafiicLights/v1/v1_spec.mcrl2 b/mCRL2/TrafiicLights/v1/v1_spec.mcrl2 new file mode 100644 index 0000000..cf47e47 --- /dev/null +++ b/mCRL2/TrafiicLights/v1/v1_spec.mcrl2 @@ -0,0 +1,32 @@ + +sort + CardinalDirection = struct north | east | south | west; + + +sort + Colour = struct red | green | yellow; + +map + nextColour: Colour -> Colour; + +eqn + nextColour(red) = green; + nextColour(green) = yellow; + nextColour(yellow) = red; + +act + show : CardinalDirection # Colour; + +proc + TrafficLight(direction : CardinalDirection) = TF(direction, red); + + TF(direction : CardinalDirection, colour : Colour) = + show(direction, colour). + TF(direction, nextColour(colour)) + ; + + + +init + TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) +; \ No newline at end of file