From cf0f988c9c6aa48c4c259dbea6332989f9912a50 Mon Sep 17 00:00:00 2001 From: Johannes Theiner Date: Sat, 25 Apr 2020 10:57:28 +0200 Subject: [PATCH] A2a fertig --- mCRL2/VendingMachine/.DS_Store | Bin 0 -> 6148 bytes mCRL2/VendingMachine/VendingMachine_spec.lps | Bin 0 -> 1804 bytes mCRL2/VendingMachine/VendingMachine_spec.lts | Bin 0 -> 12919 bytes .../VendingMachine/VendingMachine_spec.mcrl2 | 19 +++++++++--------- 4 files changed, 10 insertions(+), 9 deletions(-) create mode 100644 mCRL2/VendingMachine/.DS_Store create mode 100644 mCRL2/VendingMachine/VendingMachine_spec.lps create mode 100644 mCRL2/VendingMachine/VendingMachine_spec.lts diff --git a/mCRL2/VendingMachine/.DS_Store b/mCRL2/VendingMachine/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..5008ddfcf53c02e82d7eee2e57c38e5672ef89f6 GIT binary patch literal 6148 zcmeH~Jr2S!425mzP>H1@V-^m;4Wg<&0T*E43hX&L&p$$qDprKhvt+--jT7}7np#A3 zem<@ulZcFPQ@L2!n>{z**++&mCkOWA81W14cNZlEfg7;MkzE(HCqgga^y>{tEnwC%0;vJ&^%eQ zLs35+`xjp>T0wihi0xodiYRTRwxj;S(OL#=JJxEa?M!FXKOJZKp6RsHKRvrqJO0@7?LGIN^PTUW zbFnu+93c0QRep~TLo%md2r@22(^zbB+UoQ=j%Y9DFceeDcL#z8+r6HiU^#{`49T5A zA;bl%{JtI{IvSTn(a~`$l<|l_B-w7zLk!to5P@O|EFr;vv4iAx9X#&Lv@BFZlKT|kT>BFM8)G3R%?c^>FEwhMq_ z0|74}EhP!?90bW}u}o)VK~VcyZwO8hj1RIzi{~l?!T&lQhvY!8Ex@?y{fy7WAHa24 zN$OWp@m1Ok*_x;x#0bki z9~lRit3n#2!3}y0;RT{8216M1U@5R7;sp?c8^u2p7{#;b=haC3;(|md0VSdolqX|3 zjt_|36&y4lr>K0rp`Z}SWda`z2{0Cvc*g=@4=?NoEisXes=cglkEj;np6AD1(0Zjv z+QbU~-=s=aywOy$X>(~=`KuL`Rn@lbjXQR>?`EMrgo`tP2p3l%*+R({NfwlV-zeFQ zaD{LZHbj6O#TKu>14y1TQ$2?EraIUTM1YeZniF`JCn){nWo4kj%vFav0Nt#&2Z|@m zBK?cD5V>Moj2ebiF&d)`lzIFx4O$1?To3bV<{}4Us^K9Bo{o@2fFlBDj7c^~$O^woV5OrSPRoqM-LLM3FQMjuA0HLGh7W zq5=`bOT|0k3nB^mNJ5G$ima=7Zx9|CZLaq>MP5zpOC`dSlp}fkOFl`r=yxccwojHo zmMhtz2@LDkR*sSMU}dd(_tNNg<&&}Zht#_p?xp=~Qad1M9HPn*fz~X)D^w2~t zre7)wXD==+&kr`Mv3*Nv;pW9Zm(LG1AH;-Qtqtp+o2cuz6KTULb{y5^51NuOC3Chu z*-VFLw+__O;qb^=pGKQt9i1J}7c5^)U!~B>a|dQ8^|^Bw(s!w}DV@h=kLfo(4WC5e zEXUr|_nR9LFntmuzH{N@9xsjP{ z9V=Adkae}hbRslNFEl1*oJ+Jdx|Xx3QwvDn-2I99=bOfE;>_Ju%It2Rx>LR*yXd58 zAK&+ROi2QHVmb8#Q-ayviXC}R_D5FysiNxU)Yx-f8@~9}^-sT2`|o4>jNPft89t<~ zSQ+P*jg8y%sph^ftD>hr4g?oweyXMKoX*Va(kZHRiaMRbqEj(|)WR zn&OT+d#8jdOYDsOPCj#F>aZz6dv&xp-jI^g5zhOx|BbvcS4mmJ4}-IG=9aBlmBVw6 zdv7~ha{9MT>q|!To9CF~&VJh?t2fTN-ui8G>%pANW0{|2ugzFr{jjEH@aWk5M-#s{ zYrCfA&pc9ncQx&nN%MI8@3iqlN%@yg{AF;DewEyJv*GLG$qmNy8Pi-%i{;@rst5Xq zIl|Kivx$ct6?bhFO9Or9Q}9cVtKuHD;g^0J*VNv#)7d4b8?N7<;7^{Nyd6s0xjLso qqkJlSZz#HS#o2x9ov|Bbt)}`5^S_jg=(u;y+i%SrAAQSf!Ttm7X!v0O literal 0 HcmV?d00001 diff --git a/mCRL2/VendingMachine/VendingMachine_spec.lts b/mCRL2/VendingMachine/VendingMachine_spec.lts new file mode 100644 index 0000000000000000000000000000000000000000..2d52125f1f94d3c8d14a6d12b9ce1227d5b9a0c7 GIT binary patch literal 12919 zcmYkC2UrtX+puTSC;^1f5!lcZn)E6-2{i;U#Gq6mH0fOyLEV6WRE5xO8xSy{A|POp zA{`V|%pxMFuOjQK0xs(6>aM%rA9u$8`|!Fl_x+snJm;Co$s_@R(yPZYUKp3;*dzeN z?M+V0phbdWVt}-w`VU%;=uqnj0F>Gpm6(!oI5Z(PJ;NCQ0RWWTn~`=XBEuy)DIF~# zfx?N2OUP`Kl>^Zr1`}#-Cd$EtTEGYEe-Cbl(vks?u=87q&|45zqPs-7Bn`Kop4Ar15Ha3Rgw5MkCK*_{38kn zN{SZPlR}I1Nv0)5MrENiG!#@+x1%(P+BjV?J#l>r1Cq=(vaF$;k;6_GS2vUrh)Igd z5>>&bq{T*vYKrYM)2 zRe&P?J)#-O=>P~?i)ww#a7#_X$cQeiGN=J+pv=tx5M}Z0!CLfyHa8PJVnvVNjwlOJ z4$9^m*@+(TNcQ(`{$2l@U_g)n%7bd4F*e;ibl+|Ol>Ih!A3N=T&l`(1H8Zzx2SH5A zzcVlq{~jbF(xM_`GyY{9J0c<~ChHnw)4BrYu~<4~GtJ7K>)F=?V> zdQ@7b=t4-r11>S_q=O>G?__60r6q>OCW&@cE(ZriFr(O_3x$CXXeh$`|6DcnF;E$$ zp^Q>?(oZ^+7@8a%nw}xbPY+FChesu(hq99*MU`SRV%Z7s2pR69 z42_9mM@FTI&fi4zL`#CsiWzC_q;yeEa#HC3ZgBuqOi5tJCWZc=(Qo?}bKKzHiuNdo zf`gKhBcmWx?pL%j)k*YZQbp~4doG{|*F)i=V>CM`E2_=XU{?Gd9hto5n5=EWw0x92mr!iy! zSpet+Ts;9f5};ZEptLLGXyQP-0I>819NPhu)-y8z$AR?hr1C+3DXMrFLHsjDWwH}M z5yTaEc_@M*SY`#$sp&Q6L3cAioWW~`#+X-9B+N!YFHV6ePVGSiC!iR>Sy_=uX1$jZ zP{t}iI`6sH=!v0#FvW;5bQ2k4CLZsNO3;NY^Ud&Gm0+MUq&4aaith$4D#}VwSg2qt zVp%Lj0rfb8=oM@3$u3L}BFa5ygLIdYASt83TfkLiakb?m%q;fPg$V_0C6-2_(8Oi; z%~VU_I0a}L&lI|)B2i&8g=&_f5nX|8uYiAl#L*QnfII~l007Ik1Ev(Ak|ODf>Rc6{ zL;4n3V#st9jtI}f0@*O2nwOO4VZ_J)83@sew((#TCx9_9;pG|05R9@`0Fpz{4?Dnt zgG7HE4<^#?Q74!HXiE=*5jqEGZNUi2T5w<*wmN|Oux9!%tu zavCrJkgGEUqstF~R*^afmKzoxJurb_u2sefRea&-WG0R2A+#yf0E$AsDv)>gbD9*HUfe%SeYOT6XArwodY9L z(}oBWS>~NIOaOF*1;I$wGgyEL1Sw`I9(-6(d4w>8cw2Q07&TBtgfNu* zGCVk_B;}5DfJd(;LU1tHhJe!z`z6!Z%k8STKUX z=&la;@9mtZ2!_L`o79@`?MUVyo0R0iaU}^Kgz!giM?r8fSd8%3GedP)06+W)OyrMk zibxDfarup5hzQTB7NLPh7pq|uqr|*~3A7#XAi;>uC0zBXMcPmX^AAi&*3g}9#6s|} zEQyf)JCg$oDTDOKYdx63dE8!@0Lq4$7ZMCB6C%N(#|IT)#E!-~HcuhTNk&z`Q55w$ zt!x&VER~;BWnYMhG(JQhkK_XSgd5(qDaeRA`A~ox!q8$m2S(~EA~E3v67FA#Mp8la zbIXniWLZ?6@Z!;m?-v{A>T?3%!5K<&bMr9aHGGaiFb1n|9f}MODviKO%IH4~69DBy znWll^ILo`%RIW;K_ssfZSJt zg*xOCfK;q`zdo|8OfDS>qb|g;kmd1``R+Z%L^#(}x>UMM5yjjtbmhPiq9@5JN&;qp z5e+5G5MV*`x)YG_&5*hY7*Qj!&KC`eV8Q2l4JGZDg++W~BKvVeL+PRZbR)ugno=ft z@mJ%sE|+Fjks`V8zuyf8_KrXbx8X2o)7gTQL*Z7h`0ho@VNunAtA#{(l7l$iS}y~F z#TZA3_ln`bBG4l}*kVN;L6mZp)C3OzxmiQL`&?lGseTNE9NL?aB>1JF*fs!xDFV%Pzx)MW0hB?bLgoXo%EMkTpR*wP#h zEWsdGa+Uu5HDFCroS1t98I?9z-K>+n7Q4%o%oYx(Ek1)MgW~x|YRX4okyMO^0l*)Q zkLSRgfg*fZ{C?K{(oM(=^2w$oT+v{Qu5mjv%G@lzZF_4k9x{KkF&T{8(ov@%z zoNjfy7Y2(4e$9KfV+0l@e7x#@4Gt{9+qo8Y56xi#f=H1mbD7Z0i-wKi%8^ccC!ON( zv>WL^hh=1(X&r$liHn!UUYF*;qM$Jb13>uY?K*<5#M%%dx9(g-uru1lEBi7msOMjA zR2F6zAw&JvI=HB`c6ar=YpgPC)ht%g!%3}!wTLisDD-S&SkR5egXg#W zVL^>I*z5d;>?k}ZyL(^NDiI!%UW>eBSmTs9wJ;Yzb;wm)Pb; zF4wf1_SGfpx?a&-Hj)Sp;J|sZwo4;05#*`jKXf2rlK$VVa2SBJAo>??M0jO4fB3x~ z7BLq$XQCX^4VKe17`8JE9#Ixw%i1a_QsTjiPaV0>fl*e4xk}N286cUoO&v!*SAg@m zE~Qv0cm!mx4QNWKz=9p=veDLV!d-UV#e*XlF<1YYPzV-DwRLmGQw}T{s@#Z1Czt_$ zkUueg0~RnPmvVA!9Jx7y+Cv)0&D|UvW!NP>nW$NXm<_%2M!ph?vKCFxHIQ^7j_fi1 zeRDHjQj6Sr;1P7A9P%6k{R-tVa1b@#Xkky7hXtQ^yE&pjfe4#;wdb^Iv60-#bPJ}A zx)O`;Zf_h5mAhHN!+@5`uu>UP2BdE8bdp8N$Z)11cn(Ss?aYG_kGD#>9D>A6<+ii$ zCxmg}AqVDoQ?yju3Aech7n!1f?i(5koxfT+?C`tI&j^ZHW4t;!S*mqEq=M_xlyjJL z;@402C=$~wI2Yi&AKYHThXtfW+3iqez#^01-g!)$2MZqC9F}(&g2hyvPQf0%COj_D z0tW!1CK*dWK5YVwqA?i*1$YGA_(nkRBEf#+j)Lc6-0PQoCUS37F_~a z>E=unUx~oS`Wm-Dc%#kpH{a4{;5i`pZr9kE3Zz!y^34_lBwGXQ`N=R7f=85;XOAsh z=D-rH!~D8roYwZGb57CaLqvW1z{`+dgke@Fgj3*_?~lC0)M$#*LT6Ylp1oXzVwauF}rV?LX!T!IQ+* z=%%P=99R^H%?J^K3n*|5coo1Oz@rf9{76Yvz`%lfK0o-}O<@Z*@T2`$;lVf83e;z; z4oYH+;(Zk8X2P?R$B;~MRkC9#@=gxUU!tZ|f4}nVKEZ2KqzZQIj`{ec=`*CJ+JzHk zx2-(3*`JM<(Zpkf>N{&`e7nPMte}(+38b6s=PS3I$7j2RLnls!SLehY>!Sz4Y|Zc3jIhH3uW*DjJwf1*kC6>JagdvUbCf16 zNoOWeI#o9fhoUXNe@{Z2ILt+}1AFTqPxZu`7o3aV7eUt-UY`1Rm>f{vho)Xr*_`i> zwqE{XF?aBKdrR)Evvc&r-@i?XtIaA&UPSs(KoLw7k#|bql_Njk|9=7Pd-uVVJ)yT%tr5RI_KiBl?3YBwAiMEV ztlc=h^LT;Sy`PQc{k#Bo)<6G-PJJ(RcHzmFv*11JP00!-J2fem{D+;M{ul z2fCQ>en-DB`a4k{i00$ORHKV{?*+a~pV=IYm zF<&zssrUcf%3N#X)UdE&2}3fblM_^&K@t z1Sb4ga>GqX=v)8KaPvjWzny55Fx(9;cSh4#v^kcsq*XL4Xsl8QI9nS>b#R^_r>`(7dz7Q-)^BaZsY zH&6zfh+W6+U1 zk@Z+DZ1yVg23X4|clc|Hgw? z0;dF}QnO{LO7^F=ha2OaEhhYHQL!Z!vRD`S|MECD3=K!Lth|B>m-#&JB5z-)q3Dcu zZo0XJ=np7_m=dgU^QZ!Tfj>x6TI#Z6=yZ8?^7cnYvZ3?ibZT0SDl^~D->FR^KE;tr zn01Unmb@jTTC)|=YKv);#C51%}9q^Q)%;)`4@F80078?wuqM?&|&O!3MC+sf^IH?C^$NVYl< zE!tu`=R{lVaD$@;|AS@b0Oe)W#;2j#Sg_aeyfDA}I(kUlILTw5-1cCf$0|a>Ovf9z zLqI7uwPNn_*bANdNBvXKwQH7T#bGZmS~kio_$co~Z&&YlOzgIMoa7UeDwqo%d6C}G zKRorU^Mh0Qt*Dm++t0V^X4=}!l_n%p z^5xe7pW|jmHs@p__g!&7Om?_P+Jl|TEhyQL%U&4li68}W zx@k8__9L3a(CYgD@t}>j!%)F8erK*&=VHGSM*8=(JxRz@BPkXiX_$fQo*6>kGys3G zwyJF8E)S+WbkQcveZ1kSW4Ufshbt~J?QZn5Et7MZ}xbf@aJZ=wXWy^s3M>VzCP z8`Xqsl()tAP~GdARxst3dfgIgFO6adR>q4Xx^e!AH;W$fi+9Og>9!cw@rdd<;@&Z9 zlvVC@le=Z}bRhOw;vC0iWGTRVAh+il))t-2wCKRC#4H3$pIlzI+aA(nkz$i0#(x%< zZ$cSa@NXT;z1(FY`nxW3xeqsxn2{ju^LW-@?Ma`o(>jL|%l_*ba!Q}>QKvtSARRvA z^cS)}9krC2iYjbXJv&zBZHYazT_u{XYGF3_QHjKE=*xx1%{ID+3!|2;ousC(Q*YRF z`Jy*m`%`CPUgAmJ_vdQKu@@TNI?g%2OluC9p z%xg_zcoA;`DA07G++c3;N}@e_d*@;|Zbw*tBwpVBjOVcXmF~(T(K)f&U*=@S+_nNV z1f^?Tj^@hu_G&lnI1|0*8Y=UjS@GeJ8w9x{IhG`?$2NCITm=3hH^nl#2b^Vo+nYA1 zu@b+Q<#=**J>|!c%fe@GbJEFU{?9G75zYgIn5yH9vY_M^rHrq-JQOOngNr(vjYDdN+xbZ7VTo!evC zp9D5f+gK@yeNQiit!NYqNBaiS$;T5u{pbQNe>r*s-P2`hC6>&JUC8-#2~P$$-wadH zD+zA}VqMDtX4~R>19_VF;(H*X(}7C>l-MT(IHEfp2xbmIC~)JGwZ*ao1fe4R0U9Ci zA%QjfN;el!2Rym8Ittq#g`nbyK?>5-PQ}%&j8S88U>@aN-KO&F@nKLhs*FJ7Yy))3 z^vYuC=}u*R)~KO4FoW`{Zc&+eoaMd|Y^%u@e3V|&_ijkX)DzJ>2{q}xfFA%)i@FPP*y5T_FDhUTaHB|5&bHyH1B&HK^#uI` zqk7`N8p^Huno9GN68#sWwwj%c1`kY+;c=jpL-f9u=PnDr!ki)RGruKxm-qR$K#vWm zay--OA_!+rMH-Y1gOPD&ck9nKmk37NcEWPK!N@q?%+VkQsOrHH*z=*+i)ogid z14K^cuO?GYwwgq`>Q9(eBC1HjnK>A7E%nzkUEWWMqF>yRj3CLLb_Hl4(J-{kCut|6 z&|*{~a=#cSM3s^M-thQ{ewlz8B?~HGD%vRK1%fS;rQxKB52@>Cx~vS#nyG$@qZM-Q zfm-^dj2^-aUdKrGj2j~oQ(0HErwK6SR4N+lldfwrd{tfZ3yqHRh-KZ>2&Kk(m$yXBNrWL0r`~#&ku~Wp_}nhd5m>ZH zpdhg=f<;U7#NtNabxpqk0xE2_T2BH{A<}NwRLQzgs`)emUA@H41oZD9VG(e6>GpydLzS5=tq{QaM==E>`q#B*y zW^`P3$M2V@8MTc?@_&Xj>U;4fB>yJQi+(wukgMGu;2o4S8I-!Z(j~6*`*rG(n$a1h zKle9k(HUzJM|aHEH`k|OovT&6n8x;~ALvpBWR`mFk1g)jv#(eFP|3P=WQ!Aru%&n5Wr0l?YZgHEpA#u($ zy{Y*{W95{Zc1G{m(F!mVliPOG+)40hY})Iwu6?j9MW^Mh zyn3%Vu~B$R!p9FI3%x#=Uq?irmC#`phKr^Cw$kPNIQ!FvKYr72>-4WFzL-ySS@g68 zQr>{q5rckx1&T(?FkxrAB(YC;Q{n)G%OdEvlugOJcp#CuW9!_nDKxB2HHP+nK{szZ z9i{(8pFla(LLq!Dl^~uLJ}dsm4^!b6>*+eu)Pz!$lnV@$vm*h#Jnx0J`o_mO_oG_a z1Zsykk1O0NZVb$4_{O@rb~cZZh&|ofS-xxq<Up{v@S^C&G3R35PIzP*J9dQ|TD52g`i*YLsRdR#88JTLrHwo*YZy70 z!n$U!+khppvezV9`^WGXf)5%?MG9)Zm5zqb?uttr&s5d$4`TnUiQIkL+cNJcy<6{B zmg?w%7JGsuXWNYKrq`pB=a#D9P8wtq^RsK$ybT48c~89F>nX-*jGDH5kuRx|d3KSR zSFGoDBE_YR?J8_PE-+o-Hy!r%jY6H1=rtuZumCp-@y&s`;J1?pGj$xh3=J2Wn+`ER zKTK7dhk5CMY{>NB+nrmbOkuJ0ezC29wgA`VD=wdP7Y3U`{3u@);(UFz_`sieZVT7y zYo3&vZqR-VAEdNJxlUa=j@iL#Z`!-BF;Bid#Mi#fY*g|Ana_Q|2+NPFU7*JS*1W1i zhA*9d438Il44Lj%YTxhc)c)+bgx?N+>VsS;|S6pj`Yr*@P47!@3RhW>yv*n5WREKm$2lITfd|=^>2RYgG zR`YnIN%hqx)_rz2;dbbKhdACN$taS_87r3ec+;3F9cOR{P&T7wSAWnLIF)2t%@3zO z7>$$n3N|;7XY@+8kX5RC>I3tcwPikm#wOHTUQ@bPSW1n$EiVX*9BF^uqx8eYPo`TG zynM}_;+~a@>lxQq_VV2eR%^Vym%VkUsq|L8L?yXK{}xO6zIO5XGUlV=0XNqT!vqtB zj__miU=HTzwovl{!PcrT{iUu(@b*T}7QDPnuk?IAbF$cjR`@EI%$#`9G@hZa&>v2F zK)InP$?P(I#sB5FOFp&s@*W3)-PowtqHai>I-A(CE^k^TW5#2a7w>mFp#qVkC)V4K zm+e@)6rOnB*H)%Z;*06h&ly0-C{ZnR?!eofYgf7Finr~@EP32YnwY*qO)y!z8opP^ zwjsO^?XrK>c}DUu$&UMxu{(cftvWp$uztpsCMoUuQPVEumhZ$Lm-06B*95B`i;bCz zY0Om1*JcCa{U&xbzx#(2oUJ+Q^C#bQ%!htg|8GV4E&kR8ZfWuVK-jMYt(LqA%@+%v z_Qrw=>6G+>jhbL@+=BgBCcQ%st*`z(NY7S2w^SyjoV!v?d?02Qcq?S0GyDQY+L_QD znz~c%**(bsQdXrj|6smx?N0APZ_BZlUgz~(lvJNv>fMuXY?s<<aGu))Ak9fNqleBSkXFVO3g4|KPP=asCN!N`0J+vPu zdcrUGYRD-H_rB9n0e+`?Tk-v0JSo0FDCv7kK9d5(anp`V;VL$ z6WBJ5WI1M_1gXKSx|D2$IqU83BVt^FZ;STi zfeq##n#zJtg!f*J`g?;_EA92>xoy2tGncvbw1r!Rk?ynv-P7UY7ACqKghXpf1A!YV z;atzZ;X-xOt=9I87VOd{(B-G|Y z%zZDPtS*%>a;=;La0MTa#wSC4BZzq08{Vk^}QfJ~i0qPy~Q(E0$ zY!<|5FHYStQEgoB=Vn(;@KG{0Y*MF7=$5h+eKYl3xsxU3qWk;q;#A$@F!ZDZM))ow zG*kPpu7i&cJHPlvvWu+SV3Kmw)xVbORlDHaH0O28fUf_8ufEz|S{{o?e*8MYza6{rCBxkUw@qSj;g25E$_hB=MwJHrj`rl zLM8U=Rz;4zG{_&|#&)sO70348GG6BO7dy(=jrj_|)@92+mc|l}@6~;g*#i;tsMt#TxukJSeldJ+RFCbpYWKhTq~zF(@jt@-UEZ;q zd)ANNH~q{PW@k3OsyY%Jt7C8WyVo$;s^P4Ewr;4>X|KC{C&ImwJG%c>)Toc~uUh>; z>wkz{^?m2oJh(}HNBrC^JeJ1JsvGo+B?>wRX-`di>O&X@^pX{peM}8WUBa&IlYLxz z$2Q&G)d5<|@(HfjyQ9tBYvZ@bS&hQOsqD3iLI2m}`!7s3ygp3{A( zsNw&5scp56c4!2*NKkDNPW`jt@kjW729&u5r6C3ngEenOOeS%+_il@XPqe(OXx z+1L;V%9Zb`XS0j-DAJk)&hR*IA!7wP_0Y$%6Ov)SsF=-sF8D3wRcLQhlGCtSU+}mOAq!C9CD3B98ucVJ9=b^tizv`kG|F zNiD8e={ALu)%jb;ABdF%r20obUu`;}p-c!qplX%HubkdJsjT3>N7K+ab^aZ8vXX1i zA#OFe%D+{$oUi7Sni1KyHYROk*J_dRj*Y848>FhA%{xx_F)FLu$x3+9vbwkQh3*c; zAM9RzZeGp5MW1vxbvUMF*JY9RarAthI;%l1hjEW~($xF(VEw@s4~16x0b@&{PU&8Q zt1Q*m?8(?F+mfQk87R-x?8wd4rt2ESYIWZR+bsUMX;)n_rD*z7fu6sgcbXuk#MdAuN$hU znf2QBMEKaPx`(*MkS^cIOPen7`b&cDL+{zWH3`fB{m-4tGkqq;XO1!wqs}PS?in^T zeRscDfAZI=A4-ajWUTsjxkdhWwdrRKOhrOKfc0m7-84;aU2)%@V}>U0?$aD5A5`rs zDf*fr+}E``^0(Edn;KGixt*YCg)ORQ8Bj|gszA&5UlM@Volp`wi*$z%L{EbC(iPWi zo=KdM!trdWmzN=>gcKFd3jSIm>QPyRG$*;hzBf<(k*o#SrS$SCHhnu$4R~DgAtvu| z8AA$4borQ0j2n){DMwi{NI^|CarQxQ@N);3Iu&i#{PGJ zl|R2SgM#IZlQ>a-vrSBfC2P$_to{+y)XwM6s)eci6iA;7q@2Y)K~MVsmV`Zr@^kI&RORh1!bHA?*I2FX=(< zs+SLP!v2oexpGZr(RRdkc&KXeLE*ZJtm=OPX4jKuRF4O(_q!z8QMwwz@{fa+eUI07l} zTH-AH`PzMjrjZa1g&$40nAlU^XHB$m9%f`NdaS5csQ%#J=9sLbQ9dKRt%DWP<9l~X z0VlTDp0q-G7~zFJy8d8WA}gn>20Z`qbY0&Y%cW(`!|Y9umE9T}5m3ZX(#6fb@=w-0 zo2NG!G7mleQk_>#_Ky`yzJM-&C2iYb<+X(p4fXJm@S((u8olKwt;1{%4A1*4PEV_Ls_yWAZIB!xU%n)* z+>x=jC-v5pIu5^hBX-4Z;e`+S@cI*}&EV|RI`Hhr^R=08E$vn~i`l<SA<)5VuI;7}55|dLXocv;8)CxxUf`U$6 zAD7&u9!{;ut^ZhAllk02ummk+znU8GJQo~J40lR67}B%5!&=rxbJ#3t(cqzKk?J=8 z2HRx$?d22FVjbQ=J+wPh1RQ#?HE~6E@dXWiZ2cFRO=eDNb?(oH8tO7%TMCw;hc`B+ M2fWWcjvzw+4+^azSO5S3 literal 0 HcmV?d00001 diff --git a/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 b/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 index 7bfedb3..6b7cdef 100644 --- a/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 +++ b/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 @@ -18,7 +18,7 @@ sort map value: Coin -> Int; % the value of a coin as an integer - next: Coin -> Coin; + next: Coin -> Int; eqn value(_5c) = 5; @@ -27,10 +27,11 @@ eqn value(_50c) = 50; value(Euro) = 100; - next(Euro) = _50c; - next(_50c) = _20c; - next(_20c) = _10c; - next(_10c) = _5c; + next(Euro) = 10000; + next(_50c) = 100; + next(_20c) = 50; + next(_10c) = 20; + next(_5c) = 10; % ----------------------------------------------------------------------------------------------------------------------- @@ -68,15 +69,15 @@ proc VM(credit : Int) = (credit < 200) -> sum c : Coin.accept(c).VM(credit + value(c)) - + sum p : Product.( - (credit > 0) -> returnChange(credit).ReturnChange(credit + price(p)) - ) + (credit > 0) -> returnChange(credit).ReturnChange(credit); + + sum p : Product.( + (credit >= price(p)) -> offer(p).serve(p).VM(credit - price(p)) + ) ReturnChange(credit : Int) = sum c : Coin.((credit >= value(c) && credit < next(c)) -> return(c).( - ((credit - value(c)) >0) -> ReturnChange(credit - value(c)) <> VM(credit - value(c)) + ((credit - value(c)) > 0) -> ReturnChange(credit - value(c)) <> VM(credit - value(c)) )); % -----------------------------------------------------------------------------------------------------------------------