From 250c28a74e064ff2ac5c0e30fae10b904feb7d7c Mon Sep 17 00:00:00 2001 From: Johannes Theiner Date: Mon, 27 Apr 2020 17:42:44 +0200 Subject: [PATCH] Anfang A2b_v2 --- mCRL2/TrafiicLights/TrafficLights v2_spec.lps | Bin 0 -> 20563 bytes mCRL2/TrafiicLights/v2/v2.mcrl2proj | 4 ++ mCRL2/TrafiicLights/v2/v2_spec.lps | Bin 0 -> 1491 bytes mCRL2/TrafiicLights/v2/v2_spec.mcrl2 | 55 ++++++++++++++++++ mCRL2/VendingMachine/VendingMachine_spec.lps | Bin 1804 -> 1804 bytes mCRL2/VendingMachine/VendingMachine_spec.lts | Bin 12919 -> 12919 bytes .../VendingMachine/VendingMachine_spec.mcrl2 | 11 ++-- 7 files changed, 66 insertions(+), 4 deletions(-) create mode 100644 mCRL2/TrafiicLights/TrafficLights v2_spec.lps create mode 100644 mCRL2/TrafiicLights/v2/v2.mcrl2proj create mode 100644 mCRL2/TrafiicLights/v2/v2_spec.lps create mode 100644 mCRL2/TrafiicLights/v2/v2_spec.mcrl2 diff --git a/mCRL2/TrafiicLights/TrafficLights v2_spec.lps b/mCRL2/TrafiicLights/TrafficLights v2_spec.lps new file mode 100644 index 0000000000000000000000000000000000000000..4470614cf0c414f92860516373b6021a8c9d8bdd GIT binary patch literal 20563 zcmY(p30zWH|340RRW6dj1q;mz@T%YnYGp+QhzN?}R#|DGXlYrgQK3^kfM}>#EN+=H zrkG31*fNb-&7hH4+2qpnI88NbHDk?2jWg3U%k#U=^ZkAQ|DV2I=Wx#XoX_X|SA}yrLYrB5&^=6xt@H9gZ_Cfyr&xMQo##HE2$9GhXeTrP$7rqVVpqR9ESh$Mi_yvbHn7E z?HDIC8jW*_+MB<3e-R4pRFspA;4RL{&)<6xk+Y*HCkIi$IeO3j-OCVpIT73b>B9fp zh5ff<|F>h!b=ZI86y(Sez94o^jg8 zZr`3Km*nlpMWz7$-o5#VP3KmkiuUf?m$zpJqEghdZO9tZvXMdJ-hKZag#EV*N13n4v*l2$CQ);v_Tz9F1s) zMjZFQOq|h(0{`$pxF{nKE;)$i|GVr;L1ZxhmjaNePdc zyd^yY13Ed0=Un5QgTz@8qVqqQhL9oQ_s_?uy}NfKL9j1(F4EoPxjFJ(|2GZX<^K~t z>-WqB6Oxtke-b3+pKNeNnEYQzZZY|Lvk=Gs&)5mAM8I?9h>|V{6_WiJ26{b`Zt?r` z703jdfd=Pu_akw>J#SA=_O_y&OeA7~Z4e$}bb;yhY`tSnPyC zanLB-NEm@ig|O951T}=F>i``!JeWHy8&-)-PQKg$LV!w8iKY)>+nt#FD`+SUpr1zL zC_rEf;k1g6Bje>R01!7x@KQBQ^T$Z^y6R?!c58d}K>{*X0D?MIPF~L;vZr(a0 zJI}CDQ92e5OP|H?u+A7au8J|ih-Ep`=X13xfZFQ9#jyRTEbe9%oe;dsSu8}ga%Ttz zFpU}8?=*dtqs8S-tK z8)aFC$uE?c2{`$mwRVXIGP3(_{%0*)LMAIQ58+4utmWuE$nSvXWn0n3)0p8?&yPhu zuQIWcHxLLsveua#%|pXRE_YM*#z|r{A^5Hs2VZ33%5irG(3#0YNxnu&A}eVF!7bLv zuL!D4{#4W5quP|(O%`XT)Xb8<&|)52M_S|PrZX+)yQu-)SRHuUupr!}8~NLLOjBN? z>YHIwY2{cEE>AO!*(7UFU70}d3X?`jt~}TUz^Z5gf_84td+ zEW+cm71N)ywfw~H+EXoU?bHQTezOtx@_*RxoZ*S~KCqd)FOxM; zZ|Tf!S+FvY*st9wdN*(t>~&>O9cRAY`L^q3%f)ug85d_7vuC z7e=7wh>P{i}O!c9_ehGy#LTI=^_-rhPr0@oUB@!zc=79%05q5WXG@lv7!F9!AN%tIt7F ztyEX!mPP5-Vx$DJ3#{f`Q_$$Abbp_SfS#|Ij9jl=*Lx3 zEP$g6^_ftBA}Hio6i`K_<3*a{B9*i)428wHM|EZx?r)+(>8c?%1Wv`Gx9U4lR03R# zPRz%c#fdBGVxod7CXbgjN;rECc~Asd2vy&Gn$nZLArMqli}Ip%;k!4PBQz9 ze_5LIs<26%N={x`7L8wTLem&-r39HJeUdQqKo#JGiA`MU0{3&6wvbVSDrhm~E(-0# zz($c|mW)YK?l5-&qE{lNoYv0?v;~aTsDdznriF=*(-bSX(QPYHY3?3Ty_*tmBA|Dw zUa*&dQ%UIU`WmOnnL!qMag=sT;vL~B3r3mKBEB-2o75JJ zdIx|$+|3l7_U-qoQeg?&L4o{KvurjvwFzCK*P{$GgFP59oGYZ%Xx~n&nuXg@A~Li< zHO%$|r=roD^=DBA0(=ggmQ_T$*N9o>If16iM30?%>}3D42EnLwmrvm#!|1yPhK$rvM%1jF9DP68Kgn~`oF$t;F^qKiLp%Dw2wU9AH zUF@#ki=vtp0I_058qxsPY$v#@(X<)74}oRzV0kd^QWv8!aU*0QoXNQ+qbD_SSGfYm zTO##>0p$i;S{tkyUd3)jX(S^?VIH~xQJ@SLHiWlvO_!-j7VdTzp!(DyeI=@AW>ACz z*Kx&^TJ78CDvK}&l?L&Sidr%otGRF#+M2bTG;j=a)iV_>ql(KhL-z0e>(hav@J@`) zX3)DDb&*nBuUmHZ2X@*8J^D?)c_t`$baMMjV6v(kD#C=?R0n~hKgVeB-Yx9PC!#8MgJpmXuu>lLAHY& zBV^f7;_VoUJ@Y24UVYzqpL&_f*bOXBn<`b{;o_yRzw zEL_iTRVKEqzscmr0-&F5Bc)dG_9eHfyhv5!wfku9napw|a#o|CWGy2N)M7sO3~)^v z)nidmhRVWrsd)KV?T`P$sgnwSfWDp;Pa60bbIfz6Ya&(rE9RYjvwyu8;2r+Zy~Sqm zc70QES&EBro5;>}jS)srv0`@&VDIy<-wb>o9^ur|V)S+ab+c03W!ywgt}9pV7l|X0 zW-J*q#GcPb+)FY10&hPmn-e$^oM~=}T1**I(R?F85|Ls_r$9aTM`#+1u)xdDkIiAQ zn3?r0QAh|(21)o?#R?h!<~nXU9(1-T8*1#1PTSRTo@!Vj&q8TUlXOW!R&kL`a+77- zjs-nz*$o=I!)og)Pf`tIp`aP-ZQTh!*wk6qZV=kdxB4yWig8>PgFcuiA^C! zTGAt-k^4P98jZj~Iqg@-VH7Y=)yra>fD@BU34gk{Xfi5lt?d{dbh8yT)Y={Gw!ZQx z)f0srhX!gVeI*Ig#Rn$iqu91RIB=0|XG5voan9CVo}zk!g$}AdX8TvXysh@Ye~a#o zgqNaUXN8gmj$`h6hPb>L)puf`6m3m-`n*Y%v59f2ZgMYTrt_Rc1liLj0Wl_ z{Us8pxPTyuVo`ZmaH(xigBEtQP&>;Lxf(q5FVzh;L;P}tN5oI6fk+soexJoM5430o zJZY}rX!Q&RiqmSt`R)XjF`YrHBNS+W#wj%3QL06J?dHf9VElzF89}_2G&!sT_!^<( zBbQVz9Wj+w8QzK}Od1Xa_nQf#X3D6F=ld?MbUD?Cz!+%qECh5c@!y2W2Rb-P!^K{6 z;d5IRaz8X+AW(3*MYL`nA_aYWj za<8#N#4jK5ApEpCI}*mKf6d~U2hM8jp1!VkM)kb_6rESN!q|9vT0Q zx+W5)sDI1~Fb{NVhCG8^x<;$t0nkRRA$;?^#1`XqhPrNKrv_-A0`R|1llsJ>58lIWQ=f_~rx@_d`L`)@+h4(onP8#UJX!FSCX37W`?JJ0NTG8?`0)uYw zJnY=b5|0v84`za+G(26e3)l8qA*Z1LGr?zAnq0guQR2js?Z<%&s5=_eR>$dDuXFp4RpQ(sT!COFlKvxUaGSI1NAFW@n{iOK;9ujXF(WoZYw+J@)`n)v z0D{>L{!F}V$%ugd6WQn9p_rkyid0E;h-#T%Y{(! z%YXA0&c0MDB4JqFpS9LJa9;D^RiNvu(P}FIZPR`@zF|J1(4UOI>w1oq0v}Gf&i+z5 zixi2fudVs09YVGNB~BuJCYeADXoR|R?>E?75cdl9j$c8sCJkA^N6bCEX38Tj8ir&4 zS|KY%V9@JdeE?7x;tIlN(h2HK4PSKiJ~u#MDiDFG71ZNQghR^ z*^Z8uuJ=i{ay(ST?YY3X^YUvRY4*7q9|4oqQ(0{Dz^9tqul!v-N2_Z9h$}cgp5V?> z88M6_bp?eQpn>Q#`*W!tDH2sbS<^8H=0ud3P5N5W3k+zYb?4u&xA`IN6&xHtk7kV+ zrh`8<7l@lFUm#9^;|?#MG$SzRCtn=|8d%~xgs-K&@J&8X)b~Ehc3L4{h5}3mdQf~= zaRDp-FncluIUcFmY313D7FqZE6x(Smw3FL;A?VJ_p?;6qZ`BeO9HAb~T4^3IYVN%X zbv-evj{u+uZTS-~Kx!ls#NpXX?2knQ@GPS?et%?+6NtX~mOn8U6iQx_{T|nE!VKfA8%^FX`i<}2#aFGs5tC}^|b=s0iwoC1usb=bp5Wj3N`9Z}!2 zV0_hYRzB)mVfYB8*gN}2;i`1~{*|6PwV1deVjaAab2ZKX*$J#qGv#Y8&F2OF9?9E6 zKI`#Qtd=;Skq&v((N=Q$CVZYXV|_{iRpRQP*dpcno-H^02r+n&+LDl_fARKPS$#=9 z?Q@0P38mE~t_b24DN}kBF`;q$Yz_Ab3l6GSak_QE zx5DKttmt?0-Z(+<9LCa;651X-gpU4hjO|unGvWNVp3tpsrr2#XA2L3W^u$8;_V_5) zzIXtWz#wm+7IUsf`fP31t=4EYiIHbTZ2En93T>v0*=Y2djcWo7+YlJ7D_=d-ykm)S z7CaDJ7v9vwG3rWo(>_(m1D%aYk3^~Rj~Mq7lIkvU;aGKT)>8Ap8O@1TiZTRIz6-Qf z5I+9O_2)Lv2`qe9y*}$-=6lyPuU_Fx-*H9jox1I)jk9?dtSCtG)-H=QOR3);{Cg7CG4&ItI20|aZRHcdUBtL@7I9K0=E-?;a1=^#D zE6+yblqrscHQ@$=77S^LOKT**{b}-S$wn&88(PDCbOFzt+SX5*{gFQ~Gnjw|m(oXH zamuub;@_d;@h^gC8ZN_HvW=EWfp`L+@!wtD+7?A(;n!71tvL5NjFL61#Da3rul3X` zeyLU_`j|LBfy@cfXH8Pgubn^E5v3t$H&<)r5+aWpF@G0Cw~#T={CF~l#uw!hAJL;Z zeE?%g9YZMubR*$sC6&rlEO!kjkv}W?#X~IW+sVzy~P&oJ51sCR&fVNceik~$z_#+x5v_5+krnM)E%b?%l zYy4;!KBJ>A{S@09N)oIYf9YJ+Mp0tn$5q#?0d7PZ?P2^=c48W0s@C(bVm0;x(J#b< z38~9N^m&LvUO_*aI`a`2qyCC7qOvIP>B`mZ-HV9*J`ud9YZ4>-*!3z+LhiyxzPC7i z+R#15PVZ%?HsNV_Vx$)IZQ)LQNPhbb;auN_mO?KmklTL&&76|Z7Abz< zLo*Gt(W_Njm@B>oeG>nWM&t7s?R{HMffPtA2p<0hh-+K)4hz4pI%)O78WFon zp0Y*+WgxBf^edqTmWir~D-t5uA$l2sYToQTPbZd!jJhqdHd2ge+GY1ekjdiF3ayBb zVAC*hxzKVSUrw)`v8OIKO9&hriO5fgRVL}UPdOvxK6VRNBh6i~9B$|I*+b78b8!Md zJ;KS4j#aMLNi)Jm$Yr2Ui(sO$=IytH^L^`EnBI^-_s)fR%&7$0V#Rm-v6;bsG)QiJ z{Azibl`C$C{vCfgn5KzhobJmwmFEp@5-c14!8NXpqQ%04RcEZL+>Jb1M0^H&M1i=s zwfj{n6H(}K(0S8L2?Ar(SMl$tF*1CtGO)dGiLsxq;AN~C!S}Hn zxEjff$8tD_(+7u!7-w7rK-tKue8F91swg2Nd<0((2DV5hPSm`8VL02jvBlF1TEYGD zf*W&6O!HLy#J@N*IO+yMtz)m&mgbD=vjAwHpnd$X%TSA9Gc%-qW;q`)je?5*@GeHc z8>*_TE{p4h%X9>BGijj&znYHW&vf=BW`2o>HVUH0OWlV?jD0~NCW?Co<#Q^}U*UEV zDzaplpoQ^xS2~6_vvfKAB_|MOgw#>o`G9$ZmLGq&xKPB+;IO>);KG)yiK8`+R>Nnj z1ewJOxj+q^NLs5H8hA^E11f)R7cMlYeN$taSFx_^L9f;)uh^w8NA)HY6r{a6E_WSj zF}+}ZUQb!e2aeO+74Q1rvf$s{E?NDS)(e-5P~sbyIyd7k!^mcQUe`e60|u5)enLR8Vu;tghDARH5@g#aG^vg*!;MwKOkdbQd2uxJ%)nz3cAMkIWrK9%!K*| zW)x6Aic|dAAIpM|RGF;{yfzA1Ly-)Pad=--p{4(|cl%flFGIuWHNJkLrt1 z(7&P!$Ijq8RR$NIW6fzfh#}bdipHA(kua}9e)^H~M&Ys{l*osCJMJuQ4o3N^!?N{w zh;eIlY!Rk&(k%2l)-bU?gYtlirs?N@MeMeC6nVtN<_EO$<0ym!{_8ncU(k;=O|0hw z$5^cIdELsCp-qc@d%CMZjx1@yoci`fqG{DG*~bbwT@8GgBv4%G-^qYobUqzd+!9a0 z5nC7g^la9H#MXjW&E;Q=R#&=11-CNCt~s4)qtu{aP<=ZqBW1wIXT5r=ewZjGVG`^m z9ramdr^Y^T>f{>zT$(F>k>YNFQKx@(O;Y5`BSCKr<)vYR+yibNm(dw}nmt2{t5q58k437cyqg=&>n~gJr9w-pVLcMx^G(sfy zS@?&jY2_(RH08s`*;Dtuq1;l0FT%ND(E-}W97d|& zuMNF%LhVUb$oFwOixr*ge_$3I=wsjDA_qX#$<-ahq%7o@zkXY3QycWqt~DA-f? zv||r?4#wsm{0rR6!39|x^RB5Bx#COYYjIC}&g-*BP=;?@pX!>WxLRyR$B#rr!C~wN zq*a#m?uDyG93O;p1LarRehxF$??8hxMhJY!Vtya{y7*vc>JJRZo<8t-I6hffrTLyO`u*i0m* zS{|nnqP(DdyUVz(5<#Trz#dh%p~I z_wyLh)uYwhQBbVCaXhhV4hG{SKL z5sqBl%p;H#a$i-#h5q=nJKBf9H8SahG2-oyBPTXz63hyDjtWrstoUBisN9&FdXAwJ zSAssWZ4+e?Z>L5oHWw1ic*xK8p9=wbQ&Fd~E}Lk6Ecm_}H61a2uY(_*XN`#;)o(yS z3v9MRm%OQzQ~b*peNHprb87CiWc=PIeCNCuF%qiiD<`#mQ%BjJvbST5V-1t$D?n+* zC27bS@a5?wS47t|g7~q=z1UXwEDUet*yjC&eRwFL?BZB%X@kwE@U1&3NPkLsDnnEA zQ-VWuR}qX^o_Vv;!z|Isg>j;+5IIIN(YRSo_*o&JrvgfQBD|%I%A}d~!AxDT4)m9$ zMXD~p{cfak^FG4QI4H#CD5T|0Z9J8IxsLV?3x295Ow-5jeaIK*ofQU;Rxd|EOKd}h zVBVDUl;H9ep9NI-hB|RNdHi0_0GRi^Fo-4k!|9Ygr=u*hY08GYm7@7~j-cLv91j7hEHL@i{Ov zSnmYlCrcuaUUr;e-DngVKR~{Hsy#S;BP3WYtXEo*>;5Bi@9}vc+7x7b?n2El|D8mkK=!pH{ zxOdg+Hm~adOsec^U%8+V@lkaA%Arf;AbI+3UPyFPfw%)oi7)d0QNJBgD1>pk?!`(3 zMxk@WZ?wCC zDBqnAfA|8ZDqu7T`il3Z3FB7}-RonksL0js#&lSy-0YJ#^4WKKzvOkiheMBCQT% z{GkKgr?2NF#XMn&4-%gzRIYuFiRt~sOOiNWA!kKt8yu^eL?y}%6LHnc88LnAUaE$# zBqjK*;q-pb9IPk%*tIo|!lY0<6mFjx535j4nk|9C+M2+pltBWIdL6riwAGUS zE3qx%uE#WAtfYKSyTM_8A1pN21P%a|4rWtaNwFd_wt59)V>P&Ja$n@JSx09R{tJN0bBK~Z9#(>+Zj8=~&j#EC~l4@4xZ+b9t+L{;5Jv>@Xbcf`2(Riiqk2X&_ z7G9wan)V;RcVWPu=PNjrDBkO|$^M|DOs>_9$Lij3jnAAf>9$Ej{BgwgTH+hE|MmGh zpieF21cHw=V9}5Id>z%W7T8zuwKSx|ZOXcS-Wwi#2>&hNh{Yp;bW_s3Xo@d*=kYoG z7w2kIV0mroirc^m$Lgl&_sW#Wn0c!@zwTpqQ~A8eD_-$QpOGQ4y=Q!9^*fm{fmvRk zx)-TRh4_f~Eq~7p=4wE2dM0lk?@y6fN{W)~oIj-zD!aW>690wx$euXfSoKHSqE;+C zzlvu4c;Orj@w{c7pOt~6X zhvt1tKwHQmq*BT2r3mMD3qOaQIDP4XF0~KW4QiVm>zV{E%G6%ryw#ny683reKwRWy zFKHroR?gu8nm3GyXDwpH3N;Iiq-Jf~=<(dst7Qew6z*PU&w+9qIDQ&`{a)LK&@(ASdI`MadFd8AK*6P z(CyWDg!7-cg%Hn@ah~8L^`ek4@$bAt=%t*%^w9Ulh}<<4yMgA@B>g2UcSHnora$XS z5o)NSg~Y!S8Y4&;QST?OB_py~c`^?ue-rxf%a(oy{7L1J_WLeawa@jaU)JWbB;cCq zpSs+lOGov00O)}B>y!mmfXbiS(*Otjsx zqy7W!hbbG50xHwrE>$|h1Ke-8we9EJ5zc?QEre*6^d*GD(#_r^jr84;5PB4c!3ixf zUd~=a88gu6=?TAt=MIU$u<1{_wg~wQ(MIBpgvVhdO>FPSuMa50;nS8= z4ET8E*7hHqv8U*V_`j^nWh8*%)8BTvMn{cScLC5+`-2qsN-Y8-prl5TN(YX=Aw7KF zdMXnBPt_7@^St>&wpA%YX?*Q7JL+S!$5Rs2N87x@g5X`1OWK=B^MzsA1kpCa8tE!O zNE7?+)7R0XEIqWs{#!~&g?7aJX<%QiB4`ceOXCz36SIHS%tQ&himDL-o*}fGoB&R6 zpIMO)13GL#dR%#Nkuq-o@|g)C$Ra3ukK-N4-Ph}k(Vhl~Ks`~o*7N19sd*3oXd%uF zHtDsbix%Lv1gz^M1$(JPpDfG}mC%;xbB3sfBYu4ivwUB`{AT^bj#eT8-ljX>v4&8g z_WN_we%~2E3Hy^d1g6)!Msx;<>bo%cnN}b(qp5wCS-Kyf1&bdZZ$pG|G|0Oj`?@|9 z(vf#RJep(Qvx&&NANtn^M|DleyB{6NM>H{Q6dV@*sv_a^UqA(#_9S_K=nO0bL#9bx z|KZV*%D!;1$c4E?pUXg*^nR-v@X5Y_J~QcIOO}xWKgS;Ha3WWzsSRoSVM=xh+t6|j zm~Q8VJ=E+tO9AnO{N5(Lqt#(}oy%g($}_n@9X2FgEG*uyOxzztA&Wq7!lB+uy`$Tq zdaYzJ^pKKTR=CXb<^8E64|TF6qm*H01XmvDFf^U70e5y)-lwhC7 z&G^l9qy+DI*pM}fl;Da3r*FC+7lxBjVn6Z^apj94O*HH1&O@vj9h6u0RWk9YVA3$` z_qah{vWD^`5$&s4|1py?i@<<_yM}JJvc!{hyT!saBn?+<-no-SnU#ZFz=&n0iw27i zDw94Arr<>&L@4U5&^yjMN_Up9C^{&cT3Z*#zW0*Ba{Hu#=C`>)a$pUmKXJ;J@3xUpXvz57BRJO2A8|}4%6Q84jIQ?q z?myVN4ic$?=Fi9en^b5?M=uB#`}q?!Jgw(>+H(#A18;7WB=~8~*ueC-!D0oF_;FCf zp%Qjui-xCE?<{7$GeL2;eokf{wR4SI{Tok6*7|81-=sh6mcN-9e60fM(8{idx2L%x zL*0Gx>2*YmL|eCWH~U>9MD`6&ex>qnqwGY%xuWeIn@%40Zyem-4RX@)BFa&f0IB1GZ?6XInE68i!TI_i^nzvBIXWEm^XBmhA|W^cK~(T(lg znRo$if|99ig+V7?4igCvr!w!%3<@=%({z6q{iZ2VycC)jzrfpw9FZ+M(|TSsK|AbD zDYuUMw=MGWhCAclTjS7DA@UNvNN4^CS&kxb5Qge z%EQqqAG-SrBGW?dhkl8#3$y5Ra*=b6`MN$R#}}x5Ge7lrIg&+IN{N9lScgR|&(A zj-crS{4ds}trCOFp>Mie`p2lE0`oG-a(6Q(PTSR;bU`sIU&sZTDoCl%vtA)E;=HUU z7mE7fR?!y`6MYiU11j&@esg@ZIs*lXwewQ$AGNj^C86EM{55o-F>_7oz06mUa5(OD z`z7TG zCxBi9m0f!V!bhtQ&s*icY0%FDl!+%ayX^;d)KdgkQ{=~Yw0WLJ!QQ+p)2`tIdU{h=;q8lw;z-R8_G3Hh z0l~_Y=f|^U#zNPxbWIO%*s6WGL{g3TQLnjO^7(4BCf*@B9cxY8F~ z1L$(C;?D=Tp-QN|-t~?ehTIMkoGlqi1YcQ z9B6{}z)2}5)eGA^>rgO1j&A(~GY3QLv8}j#=_Q0XgQpja;=(dGhYbCnV(Q@Q10}w zOaz;_}lBGI26(nU<3ziG=$KjoLvAjY(fd1>%&ftXzLdz{66t3Gd{$INs-T2b^M1lAqu zcrZUyxZE2hdRJd8+PWkeBekEro8@?`gV4TPlk1Px*i0b(ZPWEbHz@W3#5kK?`YL~q z1tUyS=9$}fsiN$f;<&AAQ!sIG>D>|sZdRUT)7DIVP*XkWL4|jKPfqVeb@uy5Zg?4} zbe4e511p$c*#k%Qw=s|h)$xY7X-Z(+Rnt6;5O?#4(^;49bdnpu zXrcB|%F?47+ZLV2!K-)|rb{jjT&163N^QGF^(z12`t8I%=XURnjqH%a9qr+`Fe6c1%4kZY5$K?S3fn3pR?{=Gx7{IsS#v*Tj<|$0+U0+444Ef z&@kl7iGNgFXqDu!fM(?J#;{X)^sJ*z)Oj}%T-6ArP%pm;-Sl$QNUWJ8{xUOoyA*^> zH$p z2?g&{sDc%3o)#?p4bO8r^U^&t{RT6U?j;fhm4@4Wc9i)EN>W+`5i-*z=N%Qo2O+~% z3ad?*cZz<|{Q8L<&ynp8(!VT#AK5!)RUavi_EcljQ9p+ z(7~gJMYXR5%p#C&`hkgs8>u3RIZwia$N90@XJV7Fr)T9``hli93u;~v<6(F~T!giy zGPfVTC~jW{q{M?BrfO!c-^o$^PXP1*^~oFjms8P3mzr4;LhQ~fp5AonUI+abCdIFj zD)uh@*}iW_S%Tno3M)RsW?Ts@toY_ZNP6YNcA0vwFzgUkWHojr^kc@5n)GpO0(OB8 z@`Srn3b>bTraR2!dQCJ^z}_VJ72!jP!4~pWLYK5Z?3q669o57MNjC6v+JTCxu$lo< zFa>^qt7#{k$Wzmlg7!#lU{R% z&$XV9T@NmAf}-J~l+Nf++9*f7;q7tR){&EYg%N)eMCqnG@u!xLX<}cTj?DnC=%5vF zSjtTNB5OW}7E|D7yxM8frGb{#3(RzQl}vOAbcn4eaHz9)sC&X#3 zSkq6!2n|8ZF@qAK@0cd~MQ3bcMTj2S3-eR7Vuj7{dk|!z2i~CE#qxZWBHswX##nIC zfSQ>_@1u&J5kM)?V_d^?d{!x_I6o^_Qjwyyj(mrdffTLSckQCa8Kh{%+*&30_gv9> z#tfq&un1acA$&b0J4(@Fy2_lcr!Q&+s_)Dv|4w)s3I7<^Yh~0Su=oV=5mKQfDR>MM z<2X~9T(L(F{Y#skQWK|`G+=_JO|7eua}zu2^A`Mw^wg431{KC9IX%iy^d1Uo6_{{{bfu7ussfnvW#84o$_meFPo0WJHrjB^O-BFe38Ot@J-Q0hNKR zwORAq03CyNJ^t6?edL(vRraOvAS+R>Jo>%kG~-HTe8rJjxsV3v?gW#+g8rhygR!~o z6ZJD{T3A%{TKi}5Ak*}k>F)E#sJ=l3Ndym5yklltj9CG#HPh=_fs;fJ^0&mlkQbV( z7}nkoe-bXwLWwY@r1-*hb1+&fw^aPChp1L^$`k4Ah}k)mZk$FPrrgq@X*k?o$jOp% zi)56%L4{#r$==WCuAIQiKzi*oDhtpve6LH~iwkOm(W~vKVK6drms0EPIK{YJDXrkm z%0p;K)nbyrhDwpD6)S3gS3^On7C(BOz2!bqwWgV9AJ@_9UKND0+EXw>yvpPpK(B#V zazMuDoMI=z`FQN*GBD&6)HqAck-5HTKv*XnoKQHEQt zpXg3Kz=c&}+qEW7nr|icClW&Pl0cM#Fk2Ht_IyS=%3864n(*yJW=p?^77 z%r{I)D>!V7kbDit7f&@n1=fiahUY8@(*R?j&Lqgz9wWMtXH7l?*ikiN%{F@WQw0fS;jrjEyT*W2%yYO6B4Z7- z5zbAyDA03_SA+Rx6TAaxz7s%xV)mIC9E+`(57jV>X)&YvY!#F$V5Gd|>sySiA$&tJ zSq?N4!^i`MHsn40N<%xjcBycgDMG9?(h`_nYxR4qR8w&f-;^AY1619ilgEs0NNtKG zwAWO7s%dYzWgP3wdv>`26Gi?M7cCw&L1|V;N?KN%>Oor5kS>g#?rHZT1Mz~ZbGplb*r;tUuyR`y5O~p+qX#M!A}B|YBpZ$(#F!w5cvPfXw4%^RT|_W|2b9)|LBQ)RAu94p zKkxDv?9BXTcIKJqySpyPpLZfCLT$}30_Q@CTFoltEW*G(6HpLy7f0gxJF4wlz6t4+ z8FQ>Xc8jufW#Z{o)nysOrZ#0pt)kj9Y!AITbaC^)A@UtG%%1c!dI6GA1|$UiC~e_z z??@&bJ~z>r1^D5W;3Rw^3GxPTro0s7szVC_;>rHy$hWv-*s_!QW5}F=|04k_k$kT! zg+~b>xBNEAMN!{N62yLT6c`3^Ywg{T`-Fp95vB-8R9=~PU`&rj9n{r`-3eem>%|l) zx35JNfpiek2#{V#)(p5Vc!@`ai+Y?`S#^mcPk$hb2N z<3HP^PebA=fZ(97rPo3S|CTTvjx}|97T}*!jLD(#pU8qNR0iIc$W4bd3Ph9jaK>%j zg+a1XeIYV#;F~M4b&k2Z7 z3Urv>RJjdogwL?ODvThhbaxnoypkwq^>GNJ42Wso01rWfcO>WBewF077T|j+^G>;= z74@&5V>tH|`c$Obzz#pK1nw@h$E;Hkn7uLP-0LB z@RaTIZj9;Ss4(44@d5=*WsOel&h1mEY>|)KUlO1J;X%#knYx0YC(^BZ&@jcW8ZI*# zHeD*eO!5_{u&JR&&`3>kXg;A+$dXm)a}g6X0ngP*lS5qomZXBeHt4q(;2%+_;Q6&@ zEY>O#*I6cW^4Ii;(q!h+8p5v%{l-+Rs6Ag-Ev_^Nr=elev68r6!uh@V&N|f+^#<=i zP|UX74x4=`HV(c``s@Pyy*6XwKzu$~H+2uUl^2cNCR?Fm$`qVW-dBbGF(vvR?-33B z1IiLvd$z79l7qSgRg*BneZ^#_n0$&QFoZMVIUskM>$IX!A>bHvQp$o{ir`Stx4{(R zV^2h}bU*PpD2`sXfh?>@VS6|o%WN{dYGKm-B~EUW64Q(VytYk3JijKz{JtWw%Hkcj z)TKux7(-cM=gAt=xKxxC-m07B-A7sB%J0Fx+PGc^I;Y#yGG~c;HBuEEgYQAV&~>zN zoUAi7L3>vli+tWR1#ng*RhhqwD8+PQ{KxEi?7#GNwsD;lSD5gzk~ZQo?xp-}dRRBr z()0n&A~JKaH1Qu*dPfe=F&6DzN{{wCNGAWn*l>6xKnzTPCG5*;+i%h1K&2O`s)}O~ zx}a_k%S;W9sH#HJ)qB%JE}9>X2x9h#_^92F+!7@f-wLqB?M&TZbO#=+3VlL6&=hyp zK9k+;V`;NQy&NfIk6HDAPke7Q>_~(w)(NmpZM%*IUHT!G9@_0?X`{idj$|*MPSj7Q zpUX+6c+>;o$_Ml7yPt<@O?97nuV?#z3o73nxp%QTQU5l*JBQ`?-oW2@7OQBd>H4By z6To$$bwuFIzFsghu-jXYW>FLf4{i=yaAtW-x;(v$}`#;f*77ApOt*0=>CfO zV}(r*ChAX(qxlxV@RNN&JE2w;K*tvnzV~%xy4s1Ig3$t+lMro8{Wkh2lA0{mb2qv7 zh_dns;`dH=GN*%rlDc+t-ScQ4G=QAdV1<0VnEWb)L631=qLz=U*mS!>;`hGJOp0Bt zlUD(LY?ei$`!jrF4iDgPs(%qc{oPI|%;E#L#`da^oqoA9ru|O?KVn7ZZGySzo2bm3 zqu@Z(Q&eWoxM$3}6`2)Cj`E{c)KdhQX?DTWtT#$&n(G_!`3-z*CDluCH}WVQ9Iv=Z zbb_C;J(nCvjiU0F_!nFQ$Cz*-Xq*v~yhN>jhzX(tg`|(Zzua(nBR%gXz&51QKks?> zLsT9#?h%vRk28B1w^%o+e>JP_jBmSD55y@K=C^e}kJYXgypR4L3TyP?Y*(qVFp`9{X(!1y?VAkvJba`w}e==tPg>Xz>m2<@5~kk zk6r4FZ9iTQ6gGbgUkuo$w%ua{MsxlHPLwc=Ne!Gh&#~>O!y^sIcV|(v(!`G=ex?+P z_-2|NKGqA|u9x+%wJ0WiqjOK&ZwCIp{a7K@L-2dlNf4A&bP$;$?_PURP#k0It05fy zzyRXfxdHE>e6ol^Q2F%P=1l}2qfhPxKUUrcj|lzPUj0CABlm90 zkwt&_G1*1_Dr6adryix?_QpAnNd`~~j)wfzdP(dLJ#lJfbl1me-(y}{w~wWJfperzhq4vLgn zan{)viZZ!I@D75D!X|JUTbfZQC>tT0gB{QUi7jFDI>dh|ccMc}R5@*m9av4v%Ye~y z%~#ly^M?iXqhtbjyF8cFFZV_->7(VYbYuwUH)V&+pN-Ip%k1(ic zpfBU^%0ni;b$=|M)nWp@Z_(HpqXvF58mbJYU~sgR0y>9|64RQzi;3}UxetAA2xl`g zhA@=FTG6L!z*^G|=R#-HwhJqyR5bA=%wU0y0dhaOydNc{bcjjw5K2l}khnXn3Pt-} z7NtW@Tv>e9GG4n6=a3jE_wHgWQKdf#0~W8)p!8gHsMnOkoIQ>EB|Q{wZM@yflBRi# zKtD1w+drUzjDSUClNx<=YzYviJUzcVfBJW=uV6qsLjV(4*QYQGebuU8kXZH5PUxEO zznapSx|G0dxFfjnj`;2BXJwVcrahH>@NxZZHvO^thsMEMEzFzT_x{E9lN@W$F5(ik z_9r20v4xhD&XEBT8Y=ucAkkk^=qeIV057qp=jnp}k-FLbi9Q@@qzwr>=jtDFO~MX8 z*}O&GC1|XmSzc@z)n%)U!!1Eg#+=LsN0y}%d+0pm8!vQpZW*cqIUfzq}t*H z_bmf0NnjXXqlDKDXZNKb^lHOa;7>1w8>WH=l6 z(P?1){2IZ(+AnAO)A~^K=5OQ+)uk2mW)*kKrfd|wX`@BXb~K{s4GTUQmZG*jx&}PW z`2sxE&~0o#5n@fxd(@Bf94SKhEtmF(d?#KNv1J`vx^IkNiJL*fw3)^V%l(>>hfnaJ zEOeO|exkeBUKKpY%=;N_(pP19@6xu=9x@MJ4#b%O&med8Wvytr2-pYqzz2g9izK~{ zhB_wm1y+IE(ELgJ1myxaw?J3LZMNqrbn^rs;U?|MK{rnwBfPoSE1RcexGo|Q-8{J% zq&HSA>_-a)UjCJzeh8{6On9 z+n+rExdGRqgqE+hRSP2NA@DGKJ>Z!dzj+O);3R?XO1oM1`p`MAydC{GFKHcg^z31D zxg@?3@uzd4C_Papo^#C;AMsqq-}{9{9O2IGG#o + v2_spec.mcrl2 + + diff --git a/mCRL2/TrafiicLights/v2/v2_spec.lps b/mCRL2/TrafiicLights/v2/v2_spec.lps new file mode 100644 index 0000000000000000000000000000000000000000..431f53fc43778bdabb53ef41c47342fed38071be GIT binary patch literal 1491 zcmY*XZ%h+s7{B-K+PiD7*ut@aI4saA)UmZFAQM;%1)==$5Or=c*|j~S$h zskJy{F2fBIadRm}6K7^%i$*`pgc&8oYzqP!LnL!kwrq)sS@eU+mh8QvOmoRS`91%B zzvp>g3YPEBPKt zJGnDhlgXhcsZ5xNRoh> z0E031Y(jI?^@ec*?uG%`fH6MvJa3RH(EtvB8Cbw8AO}~vwUKn50K5i@Z~?F?x4kIgB-iwb$ehq%79TEu)mh z+yThEvU7|844!Rg%21|^_QK~Thy0P091LJ+nVo5d?3~QXVt`ka_DD|;7Y^#JFa}Fr zuLO1|8I+?{RVhAi#1Cy3Cn#{!IxjD%9OQDhin};LySVA4Zt#s#@N*!*@{&I_lNKvC zLcd0>okIt}8juePKs9iC%u!?#u_2#D@dR?`a{j;xw8aZN#zUSReVxtH;ygq+t z^O1wp?W0V+|ClQl^xvMiIOZhtzMe6R_}UWejNfR$#|lZypVMh4d^d+!XIl=XE7(lB zM($82Zn!4c3577?1-7=I9p9D&8=7$8e)3SPe($5jfzQ`j57+!4{lpYiO#PU=_h55# z$>hN=PL2C=4R!ssmF&_VIkTU}hJH0q59^*z-A$NJU*5gZ8e==o`|@Z{{E&mp>|dB4 zHDBA!ZaiaZ>%CZb&6Q@RN8EQi1P4Vo_5WK&7TXtM$)Rg~+h&)DP;cUF&{duJ_-XC! zj*z2*c6&d}BeA7fTY`;u@0l~lTpdZDo%F=76ptKF+xvb2Nj$mncfuKu zzdPrQNsHr-0@CX}wSnDRo^vC9HN&#Cb-ui1>hPE|Zu87a(SH`l&lyQy-NSPB`%5{0 z4PLbz+tM_@_WacEqZ9E5yXGDZ&i~SzzA4v}e{<=#%CB1UE0+8vd&v74-?68MtrOo! JN2Lo=^grmX%Q^r6 literal 0 HcmV?d00001 diff --git a/mCRL2/TrafiicLights/v2/v2_spec.mcrl2 b/mCRL2/TrafiicLights/v2/v2_spec.mcrl2 new file mode 100644 index 0000000..5d06f0d --- /dev/null +++ b/mCRL2/TrafiicLights/v2/v2_spec.mcrl2 @@ -0,0 +1,55 @@ +%----------------------------------------------------------------------- + +sort + CardinalDirection = struct north | east | south | west; + +map + otherDirection : CardinalDirection -> CardinalDirection; + +eqn + otherDirection(north) = south; + otherDirection(south) = north; + otherDirection(east) = west; + otherDirection(west) = east; + +%----------------------------------------------------------------------- + +sort + Colour = struct red | green | yellow; + +map + nextColour: Colour -> Colour; + +eqn + nextColour(red) = green; + nextColour(green) = yellow; + nextColour(yellow) = red; + + +%------------------------------------------------------------------------ + +act + show : CardinalDirection # Colour; + crossingUnsafe : Colour # Colour # Colour # Colour; + safe : Bool; + emptyAct; + +%------------------------------------------------------------------------ + +proc + TrafficLight(direction : CardinalDirection) = TF(direction, red); + + TF(direction : CardinalDirection, colour : Colour) = + show(direction, colour) . TF(direction, nextColour(colour)) + ; + + Monitor = + emptyAct + ; + + + + +init + TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || Monitor +; \ No newline at end of file diff --git a/mCRL2/VendingMachine/VendingMachine_spec.lps b/mCRL2/VendingMachine/VendingMachine_spec.lps index 4ef8f622a303dd39d014fe4aa7b712da14350af2..deea8103d4809d1bf5fb5e13deaca3a76ac2b944 100644 GIT binary patch delta 157 zcmV;O0Al})4vY@4LID9^vqJ$m0RdjKd;)v{5@j-9R!sl_1#mH6R!sl_0z5sl3ItjK z1d%FgP?Kl{=3U-YG?a$w{F?>kCgJrf`_?SR8pCDFHbVY7(+CG^Auz zZGi(_MP#QSt(?IZ$+#TEI32Ylnzcb@aHT#6B_5?~tYp2AQNvNvloe4nredRGMp;GH L)Jk})lduL{&BBNtQ LSw+^=lduL{;FCK% diff --git a/mCRL2/VendingMachine/VendingMachine_spec.lts b/mCRL2/VendingMachine/VendingMachine_spec.lts index 2d52125f1f94d3c8d14a6d12b9ce1227d5b9a0c7..a61f92d99b2430d39fd35ebcf996c90a190f7e21 100644 GIT binary patch delta 8847 zcmX|`2~?6<|HlCpMbr$pG%Z9_a0>y=Jr-LO$CS`qCvnAf%q_D8a$m9xOfeh(Xll4* zZkdXEYMN9=+EmuO)>u&p8~vpYLzE_j#WC-0M018U1H;=da3e zWzj3;<9zIU*ndB8ZL$EU5o%EeP)MdW5HQIa5OB9lcJ)(!-se_C%INS#dr zAXIXpbmhZqXbJGNl)x{{KzT+7NOV+o91Tcql4xCp9*AUAK$UQ6QV|ctkVR&nfkH^9 z^f$&r(Fnj)_HWgc0I6kE3SAi5jG9OTruG(5Ir3X;rajaJ?i5qF(Yhcq8e}0lmvlE; zYfV1{rZV>oN&=*oPKg>&Xl7Ux4M=Te5nh$0Me9U}~Y!O3#yN0JL>QJ*xCQNcxN&FyOmJ_H48~#TaFr-)Nfp(ycLk}dTKgk$`&tI0;zlhwNthinzd39NRu8KWEW^6TL|Y z1PrruJV^jFZ5;kr5(x3w)rW7;$D ziF0n5Z9iHM6Ph}{(auPet4`-@$8BLIL6AyP>klrMygq;onrb&7E*fdh@Jsy?}= zw*(79YTL>*PwOGrTNR!H;LK16)EE@du=yHCNYN5zFhC->3!~xHlK|j1%snn!7DEx` z+~Jgi+5mJXCv%?E6qIESq@%ZD-lXYk5g)wJ2ouTCHjWyF-dFq&K#7`a_>kv?SWsnQ zf_5;^paC$(2@}0}0sz<)k)4JCUkPg^1qN(5IM5SFC5E9(Ya=uZQ~~ZrK5N+WHHy*(;y4@Etcp+TD8_;Y z7J6kdPa|jmjBVJra%choSQN2(A7|JPLZ+N8B?>Phv*o=Rh07%05au3Ly$I^FfISv33VKwBx zGaCT>MvGH-EHn;6CATY6cMc!9YFNkGy^xL&mPz%^i3Wbn&^mVwP^i=naVkKbDcQU|ucD99TFptYT)Qg%!LK-&$2j%;=y=ugUxXtrhI z-qBj^p7>pk_|6KD09TBpJy-_X5YYqU1F3v`v3v|jBOUb7#6$rAAD4STz%U;j4?@z( zx#eZ@#vY(u%$yU}WXP(`>|gJ+^Nk>Pgyl{~hYjdIp@H-*bIxflCBn3oC2goaNcv(X zYYYG%Mxf6L*93sz`-ZE{9s>9;9vzjcB*^3=!X-FG7Z=&1Di z%yo}BhBGLxa|0g0Nqqcbr zRFDyK@z*s40H`Jlkiziqzk35rn3zIrbbA0n>Pexa{g*6r0A?18z2$fpGlB8bdLW%2x$2DQ)kL= z8-YSxcWmYDmFU}s)pK4K(sv0(RDD{D1#bkm(T?GBZ!xvMrg^E}p2EC_Yly9m!+YM| zcFP*|uV4X4(%$rN3@D5aL+wxpWE0H)X$CgDqL5G9|HTI)NyDhN2DI9hZ=CZWZHA_! zBuE?bbBh3J$_U-;_oZTe2|)B=>^%XH(fW#C=w?8}c(9hKyg~qQQX2EDiUt&UCYEj1 z*aAiP@B&91t{K@Ly-NZtL(PmJ=^+{bBaJ!x`JV*Yn=jsY?u^pi zy&we12U z!<0<3Mz)=X+9)w=+|0D0HmFk<`eXSX5>TV6b~?2^oCW}~xs2<7z=b{05UbHruv;F? zR4)$h9@NvHRs#vJ7gQ_DfLl^dXvB)2^vt6&Q~z*@kkN3=nNaj%eLo#_lLHc!OvyuA zOQjId0-Saj`T;=YD>_f&_!2;>YWRrUqci|&o2=<7Cq#-oR1+{@GoJA(n2kT#<}(>u zmbxH<;C|}IcoP7?#{x)HG1MOce=dp9o#D`K85Xy}E7R@SN(6n36zMk$9Tu=A8rqt_ zRyX>NH3RCA%;a4YwG|K)g^V^?VgcwVt?;d~XaKa}Z6_Dn1pu_SWBv(hPHXwvDL>Er zBTC#VTOI2O*tvLmy!C3i85SfNDk~of$)N!-Qcd*8=oJ9q_^1d^ylw#ibIO!{CT|>% z+JDp6y=xMN*F=;>*GG2I3D>(BlM6pYU)llH8n%5u>v9=0EL;jC9>ZtlGS8EOdavy;3~E! z(_vxn?PZVwUv0bUby0rsl%#Lm4E+#i^5!=IOP#mO-aCoV3J9t^5o{ zmSg*0+r5W?Hf#U%7T4&K?DRBs?-A#ViCXW_$_kSw>~~Otm(;a?b%AyyJ$Ys{<=LZI zkEe6JiecH=q{?IQae{A2|9P=3R1>qvXQ2vX3(VV?jdH61;?f^J_nFsU*Tl+x_=$4c z@n7{3Ay-Cegx=7TKL%Pm{*!!BnEcf>ld$whRtNq1>ou$41P6+(%R+2S$TjJc>E1;D zg1p4QOU`jndke*tJ(eeJCjo+!R`VgBN%|=WlFK%O@vWT@&>m5rdPljm44%G|aUjz<_l?CW z+FbG7LdZIlU@fhcuCCE{9!T;VN~wPw@AQ;)J*{i-EH64LdA9&0Sr{blarqr8Ft%3k z%QIskvWg>aeeJW8vGZO{O8*a+DNjlNqDSP^kBA7Lm?uoa(a5jK%|gvjt_KNQUuXS8 z+j(!TZ}hSQ#eJ7=EH`K5;*;r5C!7oN-sGfv#wk9%%>0h{`gY$}=6&(naoJ^u$K^YH zSfk;q?IZ~3$*#2d2mq*} zw7&XL8UR%l-DI=x1pw5xz6lw1`H_9?Sr+ zOJpZ3$y<`xJ|(TuoZql(J;ZK$W%i!TMxBP>p1^Ij|KH2#RuA&kxW5=%`Zz z64?UiVAIl=vvQmQ5tz0UJ0QPVo7bi$my8GMh{uQ8u|0XtL9CPrD5J3Z#}OLPn&{pb znguM>yUN&AaXwc~t;NdFr(%L*FRt&G#!;B|e&gK2hWfgNF_4ee*v&Lyq16kMJB4~0 zt^_IH$}nq|#<73|?~yt?vXZ+?+pBIy=my(%Otg_h-ACCm9nDnUT$udTc$G|SKWv-Y9pw`8>Qw}o z0AjlL+MOod_{6@sMD|Z6HGE-Hhs>pg6}EnfAw0UUI)GnaN+x^#()GAe^iyK5mu21E zM9iURXCeL>FInn+iIh&Onp|ETvG7uQ;TBxVo$l|^m^*zq*7@w#NIBYrJSF!13Pyq< z;!DZ%G^Wl=E@{w;cq5tW?I*C33OF-9{;-&%0A_kQdE`)jee~(&XC|`2kKQEvN)e3`6%;&1^qWL^?n^U>DsiX=Y6M(0zLP z1Yl63T11UY8%Bk^6fISc&eEgl-um{I%!-y??>cA1Z63wh%=w)3JbI?~cyXCK`O9WI z{sm~Z$oP-A)mi4s-ej_DrsUD$&U0J)2Cw3F#8JPG{kG2BF<;*8U1C< z+WPQZ3S-!{?twu6x>AqY>6E>`x`|=F6qoKv6xYsb=w~v zg79lb!?4Ry)Es!q#9RhqxKHuA!pXhmUj4c%vmR0NLdH-cSv%%yMF(C{Lrk`ZXm97& zgi^6Cr5GMyVL@IfhvM4YEsf30B>LU% z!!qi{YcB_w4v(Ia3*)YbG+7wmZuj<4DGJpU!&AD6q|6fpHn%UG);P9iGvZb75bY*X zy&gD#FjVSI+n)kG2_utGezcX3iDG7W;{b_Jk(Bml#Xq!DIcOAAk{kMcEmV#sW7IKBGoSsEqUs> zGzg2Wmgq!nPF5iU+q#D6ryqDcK;l;`1fX20;Bmc9f^B4H`uBjbS)l($8-N$hAt|V#+ah4)eRKJ*q@+iOh*+q8(zG1+J~Z2yLC(K_Fyte zo*7Hv*7U(?H%M>EBZV;!9o#i;b|D5`XhBgS7ET7@(B9!ruB zp84?D%)#W%^$>om>)j|SC*Ao>DB&eqz1v?ta)ozEyjnxwOG(~5bcVZ>>}))DJ+RyP zYFG^i#oK=Z6tJ(o-%f z$z2zE)o;e<^Yl6v-}qU(pHWCwo0W<51$o^>UYnRRpz7CkjI7nMzTRl!E5+|~>6>WN z&g7fqv9YT%3W2_`?m;VD5~q%6cJ{n=+xo-n^?t`Y^_2@QFdCt`8KdYMft!RBI`v*U#k4(@?By_<)d>b?l%tcg^PHxXR;UpCNQlOO2C3 z^7WifyPGM|5#b#-6KOK{QiWjMnja5eGg|dvC@m$~^s9C~9wu!{>?(v);t-V#6>jAWE3(}dIVk$g zl!4-Gg{#GsVm{Z2TyXTwlFw)*YriV|`{T-|s-^oeRMBbNc8pb?_Kr_&j119uvCh}< zdW(JYqG6ngDSbx&>%n?cujLigi5>IeMqZkVN97i8w%i%9ouy$(3>5u^BVz(oCBd(Q z^WR$L&Er1}P57Rx7ws}LFlyBp8&3AJ+R;6lJ=oKb70+d0kF4y@}D|9cj6nV?Z}->cT|Up(VYF z{*tae1@qqV$36SoCteY$^|<2!T+t%lVKaSgvr))7cjEFoTGM*pxk{dBtGS7xeVoeI^U>ekqEd2Cu)57(#ESgQO>k1z+^60j&Gp<&#_gKE=#-XgEnjBmmY4?@ zr7~N%o{H8Rq6%}jZx7&oa7(b~FA}A~MR7!aLe&B*0p=hPWm>&-KN6YP|3~=E0sYp4{_d@kXQ+T3(sK*%Qwyvr zsXnVzCx#x&$UHOF*fg!_JDtHc5!=EtAV7IvP)n%i_~l$Yo-^Fwcds6!Yvq5>DUnp7 zrf2g?=n&*t@bP>G%gBlvq2RhTJ=K|R)vV}X*Oln(N6zde{@^)#i5YEMd9{J_fZL6^ zb?BZ;LZ|4C1?HeMuWz2d{u{Jf9PW2zbBFss=-Id*e>P!mO`uTA7_i3{Ltt>4##*3qidoX=-ZmF(S9 z_$rLZp8Tc#Muvs%K&00qcTi8A-DUGidOweu&!}qO?;>@Y825gF4|g->Vw>LR*p+LM zB<%8%gTX~xXvEmbH{b60xTR@mfbzq=vni7|FXtxNu3U{gaIfAG^YKuZ^BYpF`cZvaAP zad^SS^A~-;wu{^eIKE$c!P@ySA7r-kL>8;VT*=7zS*ZC=ol`wpspZ0@66|7;Q^;)i zWM||hx~2!F`_N%GBgtL$U_$mejrVc+HdSsug;dJKOYb^!W~|{eiuqlg`ZkUCEyC)O z&MD6c7X&W)+Ve06I$fU}_`$<)SyE!SBfH`>&u_Oz<#C@qay0@D$?`Ba3lzO1*y9p% zg|>}Xp9fOLy)cSHA6&Q0HM{u@S?ij1xDrLr?_q zd}SHYTKVF4VsFpN>Rd02c2N$|GJs=v&e?ok*ixr4(=HTyEld|i@9|2)Ur4$^w#9c~ zk{!4;7~vt5hgdquWbDRQ;`YT#ci}Ls%@!25?dJ}g?-SOPZ<-McSG?qpidHyY-uSA7 z8=`e05!b3Fl?YFJh22%=(7a;t@1hu1J0{yO`yIJ@I?uyPc3$Wd(XGC1YXSPt50;RE zms?8?@0hH#;RWn=s>Jx}%dHxWStxv2poni}#rHem8B`_ouFCdkkbBQsvW&L-TbQp1 zV|q48FJVf(x)+NU=p`}uFOdx|G@T6^0=!H^Bo9jN*)@vW-zVhTn=7pTgYnn!c+dKZH7n7ez5%TIS1y@qOHMy@>;}Hjg_8il5o8 zoJ-;yt#594=>5ealw;IoWB#}BN}XmzG5S^gDha9GW}RHRf|tU>)0hGI8LR`b5M zP#$2XrjK9!_D{7Iywm(o#iwjJ7fi&7Q-brYEUk8j=QP$Ley`rPEw8pnFy&t77FGVH zp<)}QzvljX$LBV7#^HLt&fnoJ7Oo_<(b9ht7ivv{MAbH~{MEdBcAuq+ob>TmqT^xl zW=`{;yhn)CnjghE_(S>^yzjKTWA2vT#{a5kBIX5&p8xJOu&DCf|HJOap(zYlvGo7ZkU z!e;j<(lfbh)lULmJM>GdZqO(HG{|A4NOuTjr6(+}yBW-yOpOR#%h4-+&quv}d{pp} zb(r7Su{!aE*e@aPKkWbXjHo!pMx*wrUv|?^dPvs0Y&UjdS)S#eM%#!1Q>H@I9@Hk? z(&zKDd5c9N9Xs=HF9dbyxpY=^SJ}w-a7J{?FAPm5s<*SiNzKXsl=fKu=7y>9n0h4K zRF3kw8hLTH=uv+2-maABORE#2*WbomL_P@b@{ex&H80WPVSjh#hx%*hli0x)e~})~ z^x4|fo(K|=cAW7(WjsBDq&ecAEREYG6&t~xl>W}kJ$l+t1D3q|OCSCCv=sTjKQ-h& zu7@Y>GyLD+GIUCA!RdKTe#g}A-U-}8Kl^`QH_%@~l||7+YNP=5bN7+^ACQff?%Rpt zNKUpTV#kruD#xG1Xym~M>di~zsRYauA6 zm_8CJM;&#JA^#iHfQ7n3*`12zfCO7e%0W0h+adK#EQla-ji641=riW)n(%#ZKw8%S zwu%rSMv2D+gfdx3AOj3l(OLl{D3jYB4Wl@x7knL^eH5C45Wm#?I$CaW8Z^jqwiJZ` zF*0RhKq%V9qhx@g+GsUE0#kX49~@4xP2ML05kw9;93tVHY9>HK1QsG$%6(NK2x64? zLQ_yOt4U-K40RH8$y4^iVPkvR_kJCDraTm65hK*fuOpT6ewb1cf;dLe4wZUMhv6Lr-Ef0V2oZ+!}8} z>nTN*gD8S}!>4o>Dpt-rCU7Z$L4fjf0RjQp$dYVQC5jAJ@QdS}l2>ysE z02ra?a}YrI{68cpNQ+hIgn}FdbP{0w3z$d{M2@CAURPEx*N1A1+YT$=_BuG|aJEMV5Ti5l;p}H1Jyigsxj<^8iXL z2oAPvML$TXiTha~0n6TyEL20+0jDDE`pou&jA}OH-|+VRL0pb!L+hiI^7eKYVL^$t zN{LFT7J{WO_2PjDc0b-BN)a%O8BI={Mgx%%b|ymMk+AAXfQZpJ&nxDIKv3EAp<{>C zfGA8(W<05_Ejihjg0e)vJb_6gJp7G#Q80%hIw9m%ulXN<3XzEO!K(#W(B-PYaKxpO zfe_`;3G`SV5D89Tt*p(3WuF@IKj;NwaB2V(BG=YNXcwwEq@I)h&~TKTSNw&qk5X${ zM!**>T~=FsGBgw$O9*(t0V80{kI*m}RTMi8f-?1b(9MMPu^;Ba9R3X>#`;KoO$wj{ zl|yPeglxhBgPGFXb;}uAp((a}3kk*_A8?!~_@r#bMZoxdG3>9`3|~9ZUI?|g?qo#$ z5>5vFM1Az_3^EUh#JQzN0TM7?WB-vypMb#0%1ap1QEqXCkvoV{rsT+?o&Vz;{nc{ z(a<_5p0wi|r8q1|p-dw#=$>VGJES1^#jzM~g64hVZK@TsC4(yobAtNeGGn&Qkx)M( zzeWujTOWFV1)$*$J6k}q)co90fEe{QWJx9uNGP1Iw95E;OdauBlXEY~mL;_gBh_kM zaeJ%@9O>|hhby2Mu8^0-tt=Y_rlb`O0ES9WNZTu=7b9)Y%9)M~{fw)bb$ORj#7|jUhAs%^Ec)+s+9>Gf!bFsN z{8v0+u<40fJK4OfhcT|7*RB2M(D{1l#=TGu=ZiWC$|;%=z$ zfM^;*Un3Zr`}6CUAPC!#Z-I!=?EVl!aWsvdaTN&S*_Zx`f{a2a)#qp;7j>d_ufg3l zb}3RYOVD9x^I3<#zNr)<@Xdo&P%Sf)!pI;3k*OyRUV0MoRUQSpA);*R`EXmWoG$ zc%V;h_u?oZv<6jSS34BOoBiDk!Z5NCneo~8f3p1yh6zhYc73P;DS4W=CsrNW4wBa} z815bpGTI7jr`{A7VuV0Z$4Bq;0IKP*Rw*WcVR);So4L>n8a|&*D?uuQ44ktzuv1wF z2y(Q;$=J9-?kd-7j}U}p<-G!@kC1^V>AkdLKIH*P)#V?p_W%qFgo`F8`hmccvnglC zC-NXO9x}|e^LBMpN!oG>GC!D!Xq3kpmwAIn zF$`v;GmI&P#=xnY?jCB;7**aaG8lo7L~}ibfKe!i5`E@`e}69~YtI|)cM9TH~Y zxT?7(5SjWH5;PqT1Tm^>>reyDN9DB&1C-0LAf>=2x9S$Q!PzNxEQAPy79stKO=OfM zck|N7YsNGvg2UhL8Lumch7~N0G?_!~hVX8#MH(4oFxs;}EL`OQ2{mDTStOol`7EB( zqP;&_(>ky|+7+<-P7$Z|dYK6p6v1~)9tqAM15r{yd8T&rfUr|lrKg{N{o)6@i9V5_ zf4{(!^(k-Zq)(s@9zV1yuzTP(WgQ-WqnJ9m@SSE;ZQEf&Mm2hnwd_PV)tE-5zNK$A z^sNdW3lcQ3Tv?@sZx2$*pj~O#?9RkbJRqqssmJ5vfMJ1}qEjgmK;X&m$bZDy*A73w zTL?uEJ|44`YCsUYjDZ^@ED%FEhwpcKk%3@Pmd6I)@PLHEq)#TZxKDw>R9pHA=YFK6 zXw>xguVcGTI?nlUUbJ2Jxj1*|hy7$wq@c&JMy&9FXkr^7LWky4Kn%7KBpN^=AQ6A0 z9M_Zuf_OGR_{>}L4KVmem+^v_7hU-V+-ZjxC1hcOpC-drdU5Ips8vCi;8p^?z2Wn1 z)a3JDZ!o7<^4uC4gB-tOH!)?s0u9x>e5Ula!@eCZ7ZX%>qGY88?o~b_=kym2 z_z}*t1NbxNF=g^MHR%)G_h_? z^g#G-yE{&!obcdlJn3|I2zuy>MMcaS`oAcbhXvd|`q`8o+YFoL9z~J+lwB3gSAqjU>fQtI#TEzg7W4|~|cwY|(Cga*t zPzw0PC7a4gp$(slIwtvj* zb$t&QMzof4%T7i^CSeeCbUJraZS880Ny207f3Y1Mi_ECc=1+d0$#~FEa&k#kd}U>~ z-FO|{G#Rq3-K*Y_>keK+dk#lOWeg8Kx%uIAdj5|uGu|`gr61QnS`l8}>6N2Bs@cpM zxbFD4Z1>@q-v0I*Pp`AXzUy61aQ%v=F&^~y>L)Wj`0)bN< z-N^IdKvZ*SlvG?C$+?WNpqv#|8p~~@ACV{oA!Y} z3qcVAsnlFFKn8+@cYkx>An)Jv2ZOolz0`}o12Qn;9=_upJxC;0qBuhB2wCc1^UrYO z75l$Ed??{^{e1qk@=5IJ!)@{8&0gt3wwqx~i%i-8jfH%*)nA{)1l@3%d`Fg42n4}< z*jm{~24bih8IZu@f%6Z;C?{ArO@Rz7RF}{8>RpE{JXTaVhaL0RsHF@xU^{YMynJHh zI)5A{gFGCr8AW#0PM|jvv7MDUk`w|#cheW@RU2p7)f!0}W9(>l`^TaS8Y=h`%HAd( zAtOejahNyXWaO&A5c#*#y=j!&)xCseK@$g%P@Slv$^r=ZkaHy43H#}*@r zjboaq1<@cLv)JLxH0hv=g@+;|Ipj+d4C;wWT~=N|pht^hLb4kbJ?j<=tvR#(qtf<( zEyFspSy)A#@}&@)F4Q4{GV0K>oy(dc#mKZuGWz!Rw`5ANsJo{E{ru}@n@5a^v%Wug zrJt?iW)+rrkUpzd$;G`hc|oA9?Mv(&m@Zm=u)9LPxBt4a&36umqqonQ``q?9ORse^ z6uq}k8=$O5z1kX@jf3~NU6ST?-jEqmARgOyP+dRN?}?67GTr_HY!QZuJ6=9_b^KS8 zn#X-N$z5IcrA6WESM2Lm7yPsj%IF)kbDv;4ou3@@i#;xx3myG6rM7SQ=8E{eN7+o& z`hfnWX4ACYPID!R#|+Q#7oQBM5IQ7V*|ei+&;f_FWc1(NfG!I$26xPTN(L*V@`Ky< zl>KM!AXk?cLi{I1tuyEgh7;TMnP@x~^L_z8cyE0%-Q}kVu2`>YPjz@?Ggz>2}$hH{M;AxfSiOSHAseg7OZJ29hpv=kr*S5|K0- zi3y4t*>59K@hlJP(i_5FNpQ%Z9J~86HD{<-xyb+)XgtLez{AIu2tb55B3nB+`Jkel>cK0 zyNhAg*%JLxg}}PgyFqQL*<9~qI4*jSs$#@TO$fEHt8`i9nGj6{hIJ=i?V}8yY1I3k zEF`~rJxtDDLb+$liy!u3WK}+#`1Tm|=_tu3a3d{JIrST-V{*=c*JrmdR@iO+$@eYV_cDG#(G8szFVcB8tf zd#f9kWy|bwor-$vma%9D;=@tX_`sx*!bhT_J?hswNy8@lqPny8w$ECgD)SiOzj1mx z5Vw*v$D@rd2Kf$TcXuIo%Y4TowaYEXE`+L_U3%%PAJ#xhcFL3&t;FY9QAQU6n}@Qm zc38Q|9O1H-dgTU^QWI7Dp3Da7{n9HHJ7!YiIDf4`7qxYddh6pTw8a%(Ujb+9w7v4p zsDftQi{quf_Q*PYooI$G$#(7|2G6PO%_dLSzUmw_ZNGnA&eg@P zqwt;g=c)*Cmup{S)ArdX&h?+=a+XXS4Q9nltuE&h9N5a=wTIw!N|ZX8c2!of!lN&O zDCAp7>Vw%u%SkRW`r?P3ayH?4kthw9y8Xj@uXR>rMQ6qtf1Xnv_kI&(C@ER%aI@3C zcfh#8rY?HT>xk-qW)+6R`qAoHnf7?2Cr)=qX_COO5&6{40Z-N651be@eVu&dIQ*O@7V@j%C86M5pGUj`H-#hFg%dxzd##npv>2xO?vhuBty<)AslOy$_| ztAArD`N4tAA*CB_^{!e;Jr}wyZiVN?2DD3OnQb0trS&iVxk{id%v~Bk(^kXo+rjL} zB<*a8-fHwX+-SN#qgUFd_K|CNnPv21z#dOq*cv7mEFRq&RuOkTbJvgKY)PD+wy=|v zdY`t1FB=v}$9e}+2)T({-_zhrpHKJ8ba&W0$bZL<7pX3Dx|xP&Cql4pVFe^|S|$UZ z^Xl~vW5}hTzXwq_T56rOlWvg2*0(sN;bHB!637D{ty11r8;Stm)O#^Zm03=FEs^h7 z3bNgi&=V}&c`u=xjP*F&rHa*rtKpu7V(QM3jpr49wOaWppD7?2krfZg^TKqQdG9O) znMNiWW9905gN@8enBC}Ul!>KUoi|g^VWe$tnJdJWc2bXG>gTl!0*qXWY`c{<6eq09 zFH8motE3`1=cgGFB3HrhMpVU6eYiqYG5S-hz}1+dzVZnrW67+-iLzv~t3}_UMS@b} zU1-Z(HJcA@)YPi_LXAJe>dojv!H}_`(bzQR&qMV_4Cb2RX`A_)#+nmI&+|HT7SRQ< zi=k{zU<>{-CZP|>3xl2qp9yC@r{%pjoe&$Pc8q&ha2B;)+0RI~g@P6n5;|0k zV$$?l!=Oh2TQ5DQ=ocU>*fiO7AlYAbtNIk;>sc(LdXB zkC++-v?~bt(l`8<2WAM-D!NvpQEXLAwb>OLRhSL$GWgmlO0KEqIS_E z%)LXkDY{J^=!hPauv;oA>hQ^*r^jV^NgBpC2oCkeSpgKm15-!!u~+JP!4)2s%q^6P z<^GCFra&KOsJn7kL4`Ois1(H@|E!Gs=C-eW&S^#`?l-o;A7^MRam)FI{tl-VZ#ZV% z^jV`=pt^E}l~aWCK9fvq;dn_~a|Pu%_w5hhO;Aga*U~lGC)0(&hOq4wpW+Mx+j3=X z*sTo*4%X*rw1)Y+wAhX*Js^nq518S3@l^|qc$lM5aMEJk z&lCe}L=_K2$@v!N9eiK-I#ab6dbpDq1EUj7-)Qu=3Rq_50f%Jw2eyQGja{RfnzDx) zm{JZ})58D0bF8>XL5sM-cVv3yzpG4T=vg>~OF8aMzi8ZSS1E62T`JNDE|}g&_|9vl zaU#;{{PhO*eNHF(_L2Lp@j}5}Gh?H%cnx}}om~R6N2!URbH2MKIFD6T>K9D3qR!B7 znqFfI)XjB_R>~A`#F~m8(cb*kN?+e4UlZzaMl&u6qh24_WUtZNDxjMi2ZZX^?{7kB zsP?GL=dq@W_W2ZSgc4Yjzcx&ynrZe$_&lKWYbmihh#R7xb7^_hs;l3+N}R{X=nqZ9 z;te?1rk5Jl0##cftE}jd_Zb~BA$s!V_B|gnHwrlk$W}94GX< zBONXq;yR^tyfgnJ^P4>PDg#Ca%yEUUg2(Lney4NTjQ`{xZ8@*Z)+DR@9@eL6onRfe ze{MUV&}Zdb`5`bY|6=7uzduC+54X7DTow_78-L^ZjL zzg&cUAnzPJ6E-Q1xJ*&;M0XxJ?yk3TPbmn0szOB+lSiy__bu?XA77_m!qG6g&+Kvc zH0oQG-?Z?ni^Nl2S;303QS*(ULvJXok9(ef+M9rQlHSJJT}=U+VpkgxP{GR8~R&2j+Vx1SkdkaLIK5M z`>_^)Sv^!_8^UZYI&L$0o>&v$?R*~Xhap-t7%&t~OV|Rgg#|bHv{zsipI)`#*)T_+ zF=v?V@;Ae+@uNz1h%TdxeL5e=FHnl2Og~37{HEff-4Nho6uk1V=)QGh%{5VickFp7 z{h+U7g99VZ+!CXAKOUFL4`@}1twjIn6F;@L)m4e$RnO1p89S}k5IAEJ!W=HCu!yX^ zT64r}x|&3PNK~+CXru?3C$I&!mPBqlswNwK*XQO^{@fA8L#Ber@pbdO0e)NuCq--g zzzlIo*jM<>YONxXonGJEut@)G780u0LBxIGU+Yl`Y({7MJe(=GN>dDPtc#d9Xq_iw zCG}9+G^n8j&qdL|KAJc4eDVG?iA@Ba;cey?uiX)ei{Sq#KrQmoZ+-4gDdxZOSM+ME zj?WRSZSQ96d-a?Ug84FYpoC(1zV1~`*rc%fHe-uuy;@G!GXIOMeOv)oERZQKRCf3f zs>o^-zRW#rCfmnKPOHDZ{hw+rrY^RR3bU=)7YqUurg)XD3{{ciDw*-Xbf4Bvoedo! zy3D8I5%LRJF}hK-N&Uy>QyVMw1c$5fC9K8FS*$Qp{10KF&X6gnCc1H7=H9pdB$8&N z)o%#0LgP$aY(LP42@bUv12asIU@p+_iagNwitm{ISIe*_Hc+to-ly*oa@GH>cjMqD z^)2>Or}T#toKw|<0dZJ~c+lsmb$3k|^Dyo^%_To;3w(#PLw~B5&uHIa+Os;~)3kJk zPk(#5v2$%=hH$E0ntoi7vsOMB_}sW(CIXZQWuivvHvSRfQpR$=Voy@oU z8k<)q9%D~+NmEWzUR6H{cRZUPP|Ip509Fy4a2Z~Rd--y?qF`OFay9rQhy{jWW zKThSpV;tu;w!g^vOppjk-yZk><*cCa7*VRXOn#l;X^vyAOc zTbmh;U8*)<*Wxmn_k7M;`(7BViD}xW*~~ahw3nKc95BDm7Svmt8B1`azl*!fe~(Ak zdQLs&?+_^ZUXQpqb7m^9d0)q|$jdKs1kbnEd?fcUtiwODZIhN@wkYX5`Hs_5naBz< z`y^hP?zJM;on{JbZO+nj3?8eI;2oItr^pn2tRC!1@%z}E^irlWEXn(GFEwkieD^;? znwST&C_SO>{{@wxj^*Wxg$aMBSy(lzV{T@j`zVq0E)oOpzyu1m0ZKI~a^F5A=`BlL z1u?eHR`+V0hDWNL9#z=O9eSwLy!=LR)L4e`GT%N4SuW sum c : Coin.accept(c).VM(credit + value(c)) - + (credit > 0) -> returnChange(credit).ReturnChange(credit); + + + (credit > 0) -> returnChange(credit).ReturnChange(credit) + + sum p : Product.( (credit >= price(p)) -> offer(p).serve(p).VM(credit - price(p)) - ) + ); ReturnChange(credit : Int) = @@ -80,8 +81,10 @@ proc ((credit - value(c)) > 0) -> ReturnChange(credit - value(c)) <> VM(credit - value(c)) )); + + % ----------------------------------------------------------------------------------------------------------------------- init - VendingMachine + VM(0) ;