From 1cdea8875e3485a33214e17bdb781cd73b978413 Mon Sep 17 00:00:00 2001 From: sp Date: Tue, 27 May 2025 14:15:09 +0200 Subject: [PATCH] added examples for first lecture --- msg_delivery_in_class.dot | 11 +++++++++++ msg_delivery_in_class.dot.pdf | Bin 0 -> 7100 bytes msg_delivery_in_class.prism | 14 ++++++++++++++ robot_1D_in_class.dot | 30 ++++++++++++++++++++++++++++++ robot_1D_in_class.dot.pdf | Bin 0 -> 13695 bytes robot_1D_in_class.prism | 29 +++++++++++++++++++++++++++++ 6 files changed, 84 insertions(+) create mode 100644 msg_delivery_in_class.dot create mode 100644 msg_delivery_in_class.dot.pdf create mode 100644 msg_delivery_in_class.prism create mode 100644 robot_1D_in_class.dot create mode 100644 robot_1D_in_class.dot.pdf create mode 100644 robot_1D_in_class.prism diff --git a/msg_delivery_in_class.dot b/msg_delivery_in_class.dot new file mode 100644 index 0000000..307e256 --- /dev/null +++ b/msg_delivery_in_class.dot @@ -0,0 +1,11 @@ +digraph model { + 0 [ label = "0[s=0]: {init}" ]; + 1 [ label = "1[s=1]: {}" ]; + 2 [ label = "2[s=3]: {delivered}" ]; + 3 [ label = "3[s=2]: {}" ]; + 0 -> 1 [ label= "1" ]; + 1 -> 2 [ label= "0.9" ]; + 1 -> 3 [ label= "0.1" ]; + 2 -> 2 [ label= "1" ]; + 3 -> 1 [ label= "1" ]; +} diff --git a/msg_delivery_in_class.dot.pdf b/msg_delivery_in_class.dot.pdf new file mode 100644 index 0000000000000000000000000000000000000000..6bbd2d47d1671914f6b3139dbacdba72dfddab38 GIT binary patch literal 7100 zcma)>2|QHa+rV2SMkGphW8ay}D`y%f5w>T^O>HER}3UNC_dyk}a~7 zElY&#?+n$i-@pI+e%^cM-aF58o_o%7o^#Ig`P}be*Hu*J2Ma&|>@~}kdjJt22#B(A z0!T>#1vL>!dyE4Rf>Y@OfIy(2vZD(I;emU)z%U3!1RQ0H0LaJy&=?N{%oX61m1?XN zLoZ7He92^fIKaWoXtz9AkdP8IOYVp4V$?h@37xq1^%~iWqmK_C$l47(QMhSlXHjIF zs{YVY8nP4B9K9CLzPt0{U^&0%`N3eb57R+A>dt<1x?k9&y|?!&JnHbGO5f3!r$gkD zd+!fkA_u70lILDA*GyY%vVld^B(kIt#F|}Fsk%1XNY4?MaI81$HhIifr1;7dC~Mo* zx}3Pa=QB&gNV7%!=4L^Vr$>rHY$Dn+z8RYWfofc_;x@d*@vY?i_VmlkoG!~cOyeKP z+e=BkSqG=a#N25u?@)FM`N`_j1ooK(X05MHiVaTnTjdpZbe&5xu@JzHDHTVGzj9wyA-sxmkII?Vy-67PZkd}(O3#*=RgX9nJ}(Tur>}tI zDlgP+5#Ye+*x3?&Q{N$s1Db^ZJ#U*0J-T3N4LJp<2?c9{Qw+bFkhBJL{rSe!P?RhQ8BNZZh0nd$d74~-^cQz@`?))TEX@mm30 z4QPt8e#Gra-|%(DT)mq~%KH~+^E`|~S_4PaRUStQNEj%DjgqGrE-3J4NOZoJeFvf^ z-0Zs0wwPBzG!t24qVa&7MJe`u9SX z#Q3El&u5WSg)*7mF$q##%yO5PSg`rm-(Mu`a|)TrOkwu?>}A;d<5aWP{XlQoQ^WGW z3;+UY`*X$O{^8d;eu3kkxFs$w48fP* z3UWX&P!JBo-Er9fS8#F{R7N2&e^}e`gZM!}=&x*oGs69THYW7DF`%HKuNwj=s0*`4 z0NH`y3nVn=V z6%UlB+aJE1v~jHc)fod^%N{T!+6~_p-1nDS4T$mZMEsHza8`;4FGn~+Uqv3T{Ml7~ z1RCY(0Y{*L_^|2!(KAt;{2vKb?6+J0EurEAdy;vs`)Do;i8)ILcCkSB+*4&_Ox$iGF z9hRoYdAs8!*ITi#U;RVl_1fLrdfi3s#=%SHH5*6JC>6}s-uKCmvbBq4O-3aTv=0`u ztg;`3>&iz(W5|IMZCz9~{^?JT2$=1ZqjaDDxCce)yy#a5H+3e?lU%Y$aV&$hYt-0e7F&H7 z|0p0}W4$eg$P5%o&P_RXrHiTp3FB`(HO4=@RXcv;LzPF|5B}P^ORcNGGo>a4<@cBr ztBKi+9zPORlu{sVRJLXt2ts~xV#%fx6HQo62=Hj(+*_ofK}LXI=9Kk?zlsTJwxExc zkWi6s)IhV|4wjjx)aq`(IEFD>XYM|DlV;NlQk%X~?A`YnQ#YE6 zH1WPqS}&|_vp5;Cr^LC!V(|Ehv7Q4v?**2tT*28ygap9sSK-vRHV=MWucx~!sC;yv zOuvDaB0KKx9Vo>Olcf%Ox0KXG_t~=up4RT~spj1ajLbb2PPOUwSbj?;jr{mT%Lz)& zo85!hQTQZnIm0T%!rzh5yOOtJz>etI8{vrSbQxev+C?TY@6+4-q;IxtG&31)ofpyY zm*i@Q*|6^^Q%|61ZgmPhYyi&O7sbA(E#jFcz8ThJt^Cf)^#Rnx;z7mWJttJnLy3Yn z&3#Y$8v5$M@B-Pz=$i#i4$1>T9q10f4sWiR1X-<4%bb8$zOOvl7NYi4*Ar7H-%?gm zs&S5UCg~Ki4JBkoN1R)z2KsAFg_o1}6hu%~auabry>TeD*n90EyRUVm4hlT7HB#=YWYB@_lO$92FJrs-c4JGEy1Jh? ziNMP;s`X9E;1RvH)z^aUIW9$h^3YG3)*>GDxfYqfu{EnUp6%j2L#8lF)=PT1EAyJ* zC}&Osxlx`JGcT6PDNyNAa;XNo`0HiLcNtZ}rNK`%1f>VZr4j1h8wPjPyPhGVrPkhM z*I@#hFmvsOQMLT8G5S+8Dzp!t4d`5SQSTkDw>qdUQ?DD*+%Nr{lh<>7mavUfdCz=K zrn3r~80^sVn1G>{UR+j<_8B>2Q*K1uyKB_$hcZVF@pPq{_HEZU%I+i=CMM6fvvsQ{ zNoOhbQTZ*~PS{CdqI_|MOmt4i~$~#zHt(gM4?LA!8K&J%fBpu!$^uUjt(Q2NpL`l} z@yv&P1)};-(O-u1!g&0uy|mh2TavDS`_d4&z2c36LIJaz%k6;`#dlt3c2YZs`kxbe zET@LXM%gaA3!OFN1?*+jbP^|NqGP3q*iy=wl1SzPnc|sDSMLr4vdPIzS38L%M~4EE z)z&-I7)qw6iN`;wyU|opR9(nR+2oeyjxSDkq7Qs!k*g#dM=|BhLB*yYC&?sx_@k@Z zTv{Y=f7h{-lr z?@jm5R)E!$)+Z+pinCATY*S)1NUKw+DQ%Sro?t4QgX*m~zmsQL z+-Y~-G75dwWS$UGE9zJ)x>PGlxv^ax8Bm>t6rTMY8Lbl5gVqJ2uo`iKlfN`%`f~HdDirt5wWsRFv743{G=!EK-q1 zb3~8!IQo2WC|2ZI+SVjOQG4pXH_K1&()#?xL*wa_@wUYAK(iUamkz8Px^XX>#2Vr!3y8~fe4ng0U zu-*(SLu)H9>soHUl4Sg5N7uh7bqDH~-S8Gp_d$8FYSFs10y>68YHq{}UuxzmzD-pU zJsjb3kk)wSx!9pGHDkiW02E}JwHlRE>%)Z>vQjqIZSn|no949wRu^OgDFkw9#=K;j zMYn7YwiqrV7wRu=y8~9E>N;)(d$MR|*&gj1z@LTV4{$mn~v zAS)7dg+nxbhGyEy*-?Q=_oC=6w!W;Qw#vNI)%xSt4w8_JY(+w^6{JJYOLf1LUSN!G zU;5@NR4h>}QSz)DVkkLP=+-)~pz*|V|FF*Bpf=v(q9yilyh^r=b>QH$_dsz|aUf;} zT~}kuWa_mG*{oT)(eSLndzoshH&cy2=pgouQ^{`qGxKchy}-wn8HA>Likxqv{*{F7r&m$KXc?_H)m+_PWeW7d1`a#Qnm% zZ;NV%CuK%gTMnmr4`j2e$qz1l)Y$Gjo9?HwflZ&xN5O(xd%IJ=?-;+b-%B*)$Uj8L zHmvk=o+depmYGS-Tu>)XaF^94%pX}h>Q7bFD!fuLsxt9_JFgit9 zYhTL7k#3aSY@T-TT? z>F5s6$Upb+mX{Ed-v_zVA9;%t&EJ!4=qa$jd8W!9aM6TWdp)UxhA3s$rzoAgo|(b` z`Cz@NrsXbnLpIZr`vn~<+GYqc(Uh1dZsc;oihKqRCkMSUZ8=)d@eItw3Oj43if)b3 zAPUUw2h#FfEUy^XP~Fy(Dd4+1ucuO9&|5Na;Fwo2+Z@%NyYZ#q+|1R$qvziby^{;K zNrRY2cPPHo>^6oYoM;*Msx?+G)~T+>zX?+HxbQkt{$ zrnJsC_T_X=MzzoZmU_cKRJiRLCgj{{DFtSghfprBJ)pUhF_n5Zdp{M__%*x`!dD5g{8sexS~;MXt+hXrf8UXlzP7~x_QQzao@Qhi%xC%= zQILE@JL{UMNTMuN@Wdd;1YNL-{fpDYTXQd(v=;nx0L|mP->iyXSQ2l2)t>b`^N6l} zSv&kAU@U^tTO4L`K88cy5Y|l8@-}jPNBaun$keBJ0_%1!-pQ$8h5$poSeHF0p< zIUt2g^pPvauvgM1A8JmzJ$Elqcr`800(Qf6DU-mWj(*0%Xt?U>EtEK+g~afe$g}=v zQWxXlmr+Yor(70Oc8W2>1EL=KG_Y(TmzE+?#ZP(uJ|JSosMZ6!`6xx7NWc=7y-DWW zinGq_c0``^rIj1@Gusl@*`!0tu(%6lT8|bP1+6@3R?NiHCTAj2;d!K-HAM<#0PnI# z`E74Z?!U8%po-u}MK+|Rt~X>_n{kVXn)y5-=wT@DJfj70e#K5F`11WNxPK{tRKv;V zCD>u!T4V97zZxl@o@v0TMK|4#h$uzt$0RF;utY!&$%an_fMnwn*%c?l`T(l&A+kXp zKCUpHD@dcMG`QOnzy=HG1F>iX>}?!Wri1}mE%(_FL2H-}vm-!ufY#{p-2$j9&qiC# z1$#(#lWY1b15&iS*Qz+uWwfUI89=TNGIWxyAK1(q^yE^@^?enKzd;wFpVp;e|1yPw zGe?L-odfF=O{snvIzo_qd)Z%~^zzlt#$hrgA9J@BoHES#B`Nyd4!=XQ0g13`z}hU%2jahB$S8JUG*$WU<>J5 zn62b+lb|18ASh|2Cwnv_wg*n=YpeoL1Qt44E9}>DvDsMV1B?x=wFt{v`FPSF!;Eid zwuHkqm#t%indQC^aLgoMEf`Iz<+=L9d;=;ceg!tcI>R>!v`2Vrb8;M=WFc7)Y_Tg=_;us>3 znjSkzsk$iNuCAkO%dmn?DRo!Exge`}PW2)I>pRPmCL3JZA2sGa0@_rvwBmVV-;PCf z`Nt8$TApm=Cs}8kp-T2elgaW`I}d8h#XJMEBJ_3ri`x-#bYJf+OMMDE6+A6%9{V;2 zwjHpz^Pu_GS{UW-74^PaYj;hrhZ2no#CaW^dvA-q>yUdXTO~h6&xCf*-PRC#(#Gx( zrne^yFiPXU@9uK$=H61eSBlpD{a_wEJzK40CmK@da|7lmU+m zxlc-6VD>n2BlO!;{sb-Yi$cYL{K6topb!`Y0fNCG@t=rE4Fhv=gv%lAT@XOf@oREu zI37`n3yB?zcn9$^zYvb7;ayaKxv3%??HzCw3s=pt$^e6KH3o{EypI=De+l?5;@A*E z2#Ci=f8r!OKKnZyC)Ih{V2;t5Ar4sKLv^f`hoKS2Antz+jiUz|qu>DZ_!R(6*iRWO zbmIEI1CI0m_o7fj;`RU>k@i4A6Gx;R67Bd)aon_tqb8a1(tTBMnDee1!1)Q~x)<^u)8yKNuqT zPduvYfwJ|4hKgCiU*fby{CKAGeS zxJ??2BMPaAXSiI75<(y$2nZr13KkL(hKTZlgg8MU?mrv-2LS(KvI;QVv`5(=JAT}S zpG5W_j_c!rumgaAU=aZ5_W^`LAi@x!9q^|PDk6@H5dHunf9b$r2reuChYlq2mmLTM z#?k8kv=hQjiht{%ASllLf9t@)qPQXZw+~A|!=wJRpM8$C<`|tXo5GZci z{D%%I_J*JO297ro_*midgFXs{8}t);jF;7rcDS)Uo);$s80LXFjxJPG NSOmb%uB4+3_#cy->s0^% literal 0 HcmV?d00001 diff --git a/msg_delivery_in_class.prism b/msg_delivery_in_class.prism new file mode 100644 index 0000000..dcb21a9 --- /dev/null +++ b/msg_delivery_in_class.prism @@ -0,0 +1,14 @@ +dtmc + +const double deliverySuccess = 0.9; + +label "delivered" = s=3; + +module msg_delivery + s : [0..3] init 0; + + [] s=0 -> (s'=1); + [] s=1 -> deliverySuccess : (s'=3) + 1-deliverySuccess: (s'=2); + [] s=2 -> (s'=1); + [] s=3 -> (s'=0); +endmodule diff --git a/robot_1D_in_class.dot b/robot_1D_in_class.dot new file mode 100644 index 0000000..7c3f986 --- /dev/null +++ b/robot_1D_in_class.dot @@ -0,0 +1,30 @@ +digraph model { + 0 [ label = "0[position=0]: {init, lava}" ]; + 1 [ label = "1[position=1]: {cliff, init}" ]; + 2 [ label = "2[position=2]: {cliff, init}" ]; + 3 [ label = "3[position=3]: {init}" ]; + 4 [ label = "4[position=4]: {init}" ]; + 5 [ label = "5[position=5]: {init}" ]; + 6 [ label = "6[position=6]: {init}" ]; + 7 [ label = "7[position=7]: {cliff, init}" ]; + 8 [ label = "8[position=8]: {init}" ]; + 9 [ label = "9[position=9]: {init}" ]; + 10 [ label = "10[position=10]: {goal, init}" ]; + 0 -> 0 [ label= "1" ]; + 1 -> 0 [ label= "1" ]; + 2 -> 1 [ label= "1" ]; + 3 -> 2 [ label= "0.5" ]; + 3 -> 4 [ label= "0.5" ]; + 4 -> 3 [ label= "0.5" ]; + 4 -> 5 [ label= "0.5" ]; + 5 -> 4 [ label= "0.5" ]; + 5 -> 6 [ label= "0.5" ]; + 6 -> 5 [ label= "0.5" ]; + 6 -> 7 [ label= "0.5" ]; + 7 -> 8 [ label= "1" ]; + 8 -> 7 [ label= "0.5" ]; + 8 -> 9 [ label= "0.5" ]; + 9 -> 8 [ label= "0.5" ]; + 9 -> 10 [ label= "0.5" ]; + 10 -> 10 [ label= "1" ]; +} diff --git a/robot_1D_in_class.dot.pdf b/robot_1D_in_class.dot.pdf new file mode 100644 index 0000000000000000000000000000000000000000..b65fded99330a94895cfbb93353b548a72a6a009 GIT binary patch literal 13695 zcmd73WmsIx5-uDPh~Sdofx#VS2DcF0-JQV)cbDJ}f#49_f)gwROK|sK!6gvfUA}?r z?6c*Z?>^7{b!TABbak)p>Z)FAz143Gg`AKG1Bj6ok)nFL^b(N;00da;n<4V>0GOnV ztV|qC0jw~Q0wMqaU=o2^I2hT%J}n>)MnXmg)`muiuU;YAJJ=aPED>E&`!#wa2|FD5!;s`tF_ zm8aA(qSe2}Of96-ef7@jJ^X2P@!jxfF8v1B>|*lcv{?##i*(x5+RP_yJvU$sI!vbm z9iCRw8QVIcx;AZ2fEe0)w;Hr_VmaHVjOz^ti$*OsKnm(4KW^j z9v9p4EsF%7`#R~o&j$BtWrEO%kI(JScK5fBokw@e203dv>4yW=JzgsWy=cgLk;(YA zn|`=ofzbY|q+wsZ@LRI$uWBnKQmsX^Lm*j`UWEP~n`&ryNbhK(MHVM1RA-aJ*+f0{ zh~A*1pQTqAikbrTBCSUi3x&u$?FKi$#xC}KaA?ua(B6S(jji>7oYY>PM-gK9tS<@f zV;gBTf(wn5rH(HpBjeYFYVr;EQw4C|6RiZ_5aE#}o*xNI35iMWpG3LmHxO|vxX@J) zoo~RrcJ7ThV=jL2R#;;3mP$;04lc34^ku}zR;R~1aP`81J z`3oh+KItQ=Aeuf+Kms5~;6i|3TMUW$!P~Q79+CQ3-+6{3Dc&@JoG_ocy&gh*40842 z(Nww&>-}JQO1li&CqgS^weN$+*j$C>x=kzmBhLW}gb4dCCgr&^! zZ9V6+4t5C*Irp%b9a4!7Bx)K{vG51m8E6PZ_z?k2lp9R6PHIkLC@eHq;z>2sbhfSv zFP}{bS5jfOjczRGPtv&Tc@DWab=!(Y=Or$aOLFD`>A%_HK>1WX% z+R4@BzownK!=A=DW;@1n{+!7*S0c< z1$mI%2I#mUu>fIZy!Zm}JE;2hMM7^)FQ>;MEXG9e74xTAQx5_agJm0G+RMbA#aB~8 z_Cg~K&2Hwhc8;UpY-pC5qo)^+IpSadF_86&G&AoZ@k%`Pydm? z&NnxMI|jVDH1j$(^SZ9LHV2OQx}IRT{Bgawa%M|lkufpjjymXyOz&&2Y)3sAasLXIg z`JAuMN7*d^e8)D7hdj1r(^8<>SiIt=XDoqls02q*gUD_fR4R{((j+JKW3;N z+a0Srk}A0@MDgxGKeWf`!~%f7rpcBUdKxt^VB zdE7u-KI-*NvrH3?h)cssl2m2$1w$;#tbk*_*=BIQ701c-i~uWN=V%%ifJxSXQf>5U zwtI=+jCW6mU|}*k8lnY1yEgo+M>i27H)4gvHG*S`L`O-+$w8s1FJJc~&CGSbtE6Y* zpT&=b>6#7Non1$^(Jr4QOhd7@Vm8uzOTLb?^=ziK!F{@N&v*7!GfXxa5U!OMXIHUU zR}8l#J|40z%Q~P))*nkV#X)`Kgw9j1g6otG*JDtW6hh7Ib`mPEW|l45Yy4Pi0BFIE zZ~FNg$v5qgCK*Wt{d9}0sfRyhiU3Sd=1=rmYIrj zr2zv!Kci&Y50?c*0?)FB_A@U95=K2UH)V_cceWhrhO{377oVVf1f8BwGMhqW2m?Cn z-ZX!uTYiPcL~fYt_lVabJOv)hTD)c%k;QzPzC!rTp# zw6p5yl1dD5cq7$0e-0fB(_oBjk))UNMoby^J1awH*#l3+?7*Dz7!Ng*?p>WtK(oXF z{}e-MT-YZS#%PaVHYe*j0j-!&hWHt^AZ{M~hj~271;K`Uuivae=1c{6K2SvJ%I^VV zXF0rRzm)0hF{8H+(p-teF%y01N!fm!3=Hd{qu!D*b)?$2=byEk8;5={#Hf<_AaD@< z-Kw4Vt-rp<>}edPxuqXvIcXOB16GN*3a=H!m=r>HaPc*qhfPx2EU?>%Q?^OrX(Z_0 zY#`{ZEK_c{Hg%S#k zp%J8t>M840hhV!l1x#;c zX&n5W$2@o|_PZiY4WJ>SxFhVtTIHJr!>spRbwW&x z02Bbwy*_dfJ0n>4px@^*NgEkLAp+Je08N+(2w-Jr2Cy-60JQI03&K=^HMa-c;oV>0 zR@Bbg(dIAe{Tkz5`g?wgu#xQ`R`xb`V;Q*q7K;NM>>Q1Lmjq$0gp8b^21W{^0(Zhc zX0KpmZ|!JjU}O)tv!udbX2t<4-&y!Cn49xYwf-CCzBAP?a1H`+fPgH21L3pkt}f4& zYnp3iW;Yt^-6Zq5a}pf5q)#SEUc>8G1b4;ozeYACe~l@C36IPzf^JClEJfS~J?p?m zDBueKOPEA|#wZm*No3eI80k=-$eMEbwN62U;)?0)$GhPNT3g~M*&2*Q*>DS!bp1!ppBX=S# zon|YuGy2&>p-9|*66Qad(ko$%Lp9c0&2d9>g2LE}nlisfL}G=}jMa-xuU^4#fEP0F zx92Xr+EQ2fETa8-=2IHaN4=9!;VUxw6!gK@S0_wvpA3gb;#$zocq7qI0E=QDv<4GC z`iYeUx{#CIqGHTtYN&MWlUHtgbXp4W%-c4R^;)5*3Bs9Y#8UApqfZ=GYn6d?FMC@B zz&jNmPQkjJrI?RwqcaStC`2;b*yh!qBl(VIV$lbxRTO1QP8Bs432yZv3R|c|BT?F@ z4F8Y-s6-oz#x~E?G)6?Y$6ctN^A#MIX)DE+MdrTysl*i_6Q8n*vzoB-qpm9Yl@QK| zNS)Li&2CKZTV{#m)n=QhXQ(Tr@*nq=AF2vtnZliZ(KoeSl>{%0BR# z`MP9A+|n*@fx6kNfv{Ga6OCSH|TFf0@*1R*Di)-5b?PBmGjgy9UU7b4BxPP)BAw!Og zsFahT%|J$uo-aD;5BOA97H)leE;(9phH9tm>Ug zERXH|qGmqXg%hwhA2;%Odi{*rZPv0aaEZV2a<09aE7s>M%@P=<*~ljRsd^M0dQrfP z=vcEI`if@%!c8vp9~!AF_1S)^Gp<$`q59Mt0&X0hS0QT|UKc~MZ@Pgq!XZe(r( zKbL7`TAhEd@V2sUw##k29<+zn(2oXRnXAVSe)wFl(TLo+e`RPVj~`+tgS>)=qC^n*ooJiN{sTKZ>7GWAMKM;DEV=njdA^mi@y#;B46^V0Ru(svP zweQ?Yc++GHqN5Is4YKsH z46yVc^&br)_eoJdwK}pqvPQO$n#3(W{dT$e==j<3SHUL18$lnzXFGZ7NI0i-@RcEy{TZBok4;4NwFdMaNAwJeHWnDd zeN$H+n6U6PoGor7s42cVJBF4GFs!jNX@B(ik*AG9&~&Y*^S#`>H{rzqF86iKQB|j; z^GgZIbE~-+8by)$cQI+|mF0`MRRz+KoqWPu;Egfyop`N`$`ZRRtcapMczDHRkVS2d zdZm6_>4}(Z{ZdWROAMAHw93edI=SZ#0+sd}UpL9~YF`{<`3d8jy#zZ1YEy7a<+A*K8hf`EE zme9(_yn`l=f3P)s$09y0b&Bu&{_>5ct|=O+>s083hVm|6jHL*KYE{eaN0REg)cH_G z#j=R)_o`}cG#=D4<)Qt9?ofh&6v{bn^R3aVJUns}k9mvr zFPAKgGm4JB3+umx5Wl5V8`*-4ZhIt)K7Gf+*c;|6O!=8>y4|V0k~zrP=`$&Bp?DTT zTHjI0KI`Q|d`4qoMx$Dm??9x4isK=!$=KHtdEM41Xpmgj)SwC*F&FjWlTek?*~y&X z^W&bNx!bdj@2jhXuJ&smbbHcXd3+X=oH8lbZQpX~?&Fp64{~M5uHdnSD%;NcTRx9h zU<8+Hs?cs(e;&`-vVGE%g$GI@Q?YxEXxq-!7>T`k{8?Pdnq1j9qO0)e&}a1EVMX#6 z{UJNHip{INnwqr50^a9v8wWf@M%(tUZ``#GcrSGFP*HYrbl2F=`!k-l0WAe8ZKtn8 zYxbjzrmv}qQ)r0^;tM=-)E*rVWgc1eAZa19%kd==6gGzu*y9a6t=Wx7Ew=($r{cfi_B-4%Qj2uZxK5q^w zHGa~Cp{FaaCB%(FZiaZ*pU^5ZHH2Ltf8o=KaNXN^szap4gr5oJ3hhcp`BPkL7Gb5- zdPYwY0_ee=|VFh0;eHJfVyy_QFwR3g^iY7n#4BK5~V<%o7T$W^M}z zN!;_}Qgch;o#&TAMl^(JyIs|^FU^#7)cZc1p-n?*`{m1#Ltcu!FO=tkM|qgIWZFQt zdvO?7O(rs?^2(dnTB`qO$uVj$N$2qRiZ_8;wb}3{#;r$tT3bbq%)8pVk{zAri4$1A59o{tcjfIDALh^( z!_Z=$MdT${hX}S8F7-qF7c&C;h(wJKXJ3~s`0}@NJpvsWydRLgVo^-^u$En#)hF-S zn$f4cMs3_}ClLB`6tKEFKiX6Boav0Op{^<0JJ5feVuJ_Bd(-GGc9*1;wcM*R@>aDUhKf`2-rA2s zu4(1PEQsYfS_7H4hWX>@n!z+Z$}tG^4FT%#VI5i3pBRWFQ;ptG%q_8M1P5FMM;XUR z(NZ@>>=eJr!Zd*&o6Nt}5T1qls_1+ISq|0w^vUQF|}OJl&0-!;bJ%`dfR#*_NaQMJZ-F zh3hjKaay1A_$;MnRUBfe@pl;j7x-*JSqrT~{D4{V#zB3z3yVBv_FkgKsjTwFgZ|Cg1flCG5;pdwri4#fYi}5FeWjV36A9!joZ0(C4)MEIKMhj&JLC z#-=zwp2J1Akjc(4s0buivhFOQ7YcFb6H)n?^LC(sS=}`{#J8ZrY+IyWoFxofzDna= zM0cKtZWAA$-eu4v?ga{40VR`9iVtz;b{W*7_(PGkhf!ZxoUX##GOaoi-P~-`braDY zT??(#p{Y>=J}&o@Y-e5XHG`cE|9#WC1kg8iapIhmpBQDQK{0mcXoY-qAP=4nTA~;- z*Df8^mx=h{vTB0WNL&wHGT zRZ9#48{qQ+@teWqQ~t`+?L6x3!z`HNukm|FL>~<{m1FtIv_|>LG$OuqqnBTQI*ZKm zlb<5#>sDSvL#p^{4`*WS!6rs$)e3}$=z%-O>!UP(nK~`zpof$W{u5X}qcqr1Wv1HF z$QywFF#-v#*WxhOvFUq(V}>z>3*|2(G|OhU&u}6TO67vi@NFKKzZXr(0?3-k)ZF)>RD$++5HX^(;&0$1Kqxcgu)N^u#cDq5p39OA00^BI1xw) zfrd2xPRI2!-k4Xm`IvC0n$HUnyv8Cg|SLO(Tj37OsJ|#3)g+3)!apnPR zO%c`4EC*^5*;LIfit4`^&eCNdI>1(aOgQI=GgRHU9aY+9|M zO-S6C%9a00Na5^xe3s;JeqvAzy)9u~uS3H5D+RqY(Vo8EGb4+-a)Ek*T7l*kmIr11 z50pQKWH4T2RcY$f#prNKDMB~kG-|bULh$6;BhXLPg@p%kg(sqpr%DL+Kgvmv6L~+I zq_d>croi5dT}MB8N9aa?;oG+!j$;Ax^-bJ1tu-x@PiYt9_i;mDUiKL4Jpa;pnK-z4 zcz)INh6$46nPZSMIu^y_ci}ZAZ{=%RYLR_SD-zf8b66DHgXC0UB935;G(DbA)L+X` zqjq5ndhTE;C}?RZNOn5rzdv?1Yh)J3-aXhww?d<{TOA{Tzl4P@8W=82j=HZZ+izgV4i+1!*Cdt{_OTsFNC zYBEeRJL|Alyd?PI;DmYic7J5e+pR24h>RBj3lvYnlMrRigi+BcH4ZS7&8_^2ctJhe z-q`QCBYR+SZhhK}E4IF^>~%>d?SRP8vcJ(}%N@BkM|e9C71QA*lb&x9&-rI$%TW7Ry?`UJqkj@|U?pCly$G&Sf#Dcb*Oc+*A-##vb?RXKu zEB?4is~R#)?W934a1&#5=#EhaV_eb3#>dgY(_O33@8} zAUI=oaXcAm#Yb_KNVttG(RM3`tTWeoRq2$YG;;8{RS!5<)*-k-jRazxy8aZ!@gQ1n zc_I!g*0lLfCeBXYFBFFmH{3z_0gj+cVoI{Na|$^Qgeo$b#HDX3<>=@7=K#yB%ODag zmT!jmk)?qa7dhy%p<=93tuGHM$^utLW%r&tB)xmM3|bJBt8# zx6@x;XLZa=QL?9~TxhzvQ{gO>fU}cOOatH6B%vWRU#R-&=H^Q$YAslM?GAuE>*v&2 z9$)5R>nWbMSZy`iOL57|2f3H8b|3T-4}3(vCD?~5*PnZc^c3Hm9?M$KFnSeUlgaZ$ zDXJE1vLG2ANt$0B%erHSq@NtmyEX7ggx7UZ?nN8_AZtCFk5PCPsbuSD$b(GMs+Jgz zBa_iz*Y%RagwHuuYXNwu&p53r&OS~ydHT4i7BU;;h}4`MyF}Dlew}r3jlEN!shV_& zo2EGJ{7UC7d~`Thd73C?J|yE5DI6nEfBTD~j9z14xvvNGvHmPpiAMNSkS7(FR?#it zqF9UDi_AI%{t66|$7{*XfIdUWHi^)d0G>xs#$?`=wP>7g!f3S8NP&bTx%-RoC6uEw zM5}5W^IX0rvexfTE=3H{jmpT@;vSl$4N%`oYyYV!eHSw1k^q}Ld>!U5G>;lCLj4-? zeN+jDFnx5pZ4?3%jLveAJB>KTJ#e_kQTm;~%Hu^UwMv2;OapOH38s)xIV}9w$o9hY zT?UYzknL?Tw{NNArO^cDZ}xBfL}w`(s?0+tOnh)D>_YqK#PZ~$C-~}0Jo=i4DD64K zIy-3_g`aG|oJBCZjeViz@e`Kf)y;l6rhQp|y}@O5izwuJ=c%b3^sQ;Ae*IQ?QGi5D z=i2Smg(vywo2t^MY+pFpKltODof_&%J$qA^G>0b36SsO0yW#u zEi`+rXEF6Pksw8F*8HDq{Phkg>Ar6T^fNS;C@?j5BNFVbqqOh2U>8UEI3DjM!i{6& zR91tFKRlnpXXnwdG>#Iv;oO|p|TD+2lHvpq4dV1>h)fgJ3OHO zDlFL`N732}rq?ml4>M9T^cBWzF2^U*c-u)-_y)mMP90(xN2*l1N*69ivcKwL=*r&5 z#NGa*SB|ahZQOg`kJVQVBj_orPY=nPSl}r*KI9ODhCxcPeslpf1GCieip2ue@%A#1 z1He2$xSg`VByb<@BLwgaRqK(WO&PLc7$o%3PRN&)boI#<#tg^Z(Icb$vIlWvn}KVk@Jb}I8mzAPjzr>I5Vtz5SMVY*QLh}C(~po| zG?0JFiLDE63WK+|MsS7gW!O3i=C?shuCAVNBXt7+b89!)fTS{RaBo9B5DPqh@bj~N zybc=l18O`QoI-Sn(vuts55$->1?28Wm1+lKxWWD?eZIh^7BKlNDv2UJ(hC9op$^P^ z0rUg}OZ3e?24ClUF86@xFFed$%ZM5?F7z=23F)|^Y!$6*}* z)t?|y|10^v2p;koTu}zGG1#{(NHp z&F33ti7OF~N`mKzEu@;X^sTDkh;4`#W6~ac0Lr8^^YR+fhPp_qUCAZX7a_F|+xy0SHzhzsOUy(0} z%86Rf{QP2EIaU-xB)$gNC!`IHKq9)iji5s?<5 z6EZS`s5mMb*+Gr}Y#;)$gj%=)sDIS~?kj12)mlJIU`z`5&!z&us2&D(HckKoGYcC4 z3<9zOKp-IJAC!-{1H=Mqz;9(@VFUo)pT=)*a7P(&f;sMscM9H>8Nke}_X0tPjhGSC z#1zIV!MeE@DLNQgssK2Coqtyl`(3!3B5ai!fdO}P&R^-BJBI7`%Kk+v-L?JIouj_P zJ(Z;dBarUu?xg|{d!u`~tXbQ3WZ2&3AA7v2um+F5vH~@6#l3z5JuoWzA z3uZkVF9oK!GK?Nu+|`E01NQ$ zw!+GG$Nc?z-^~F=M8b~uv<~n(QryOKHTz4jeiOLvUGfTul{;#;zte&)VvaL5H9-1 zWr{>k7t8%puG(s) z=4@sYxdnA@%T^^oSWsijzTkAO<(1xx6RmGZMj1XMZ)-k2e^d2Ufsv)c)L{(VzJ%eZ zANI4P@K`l&TxC2qZd|q`mAW{Mmc44sKp^Uy6SkPJmL|$ue=I z0lA<>>@?{a!SAmz5cp6}ZellwVSRG(`aS9Cq+Fi;DIE5)1#E6l-y$m15B`DPqS?8Pa>^u#IUDkX)UoKP&kw$yu@4H95 zyoibKQqaDo%8*v6RlvX<5t&=x>4-_=wbt!oI+H$JI_^B#y;0Z}cRhc@T0hxklKh;w z+@ounEK9Q($G!c*rgPgs)pcl9u0I2@BJGJ_^jHt4jBJQXE6e9I&O`r6=b&Y>@F#5> zRkyDKN9`WBUZ`Yd2UN!&MZ!h5Nzs6K*hcGLp;xvEgAzxeYHgfWA!ot4(Nj1fl1m2L z>b5fVG+9e;C#k0x5LvlrS2RAin|)4-=L=r_*+-+vKD(kxgg!g7Mq$jyZamRbO|kx3 z$b1>q(GneL^0TNzFKYb9DwfrjYioepDf75~7y9#G$vpFZ{k!J-7t z-k9R?@~QrV5A1TURoh56NhR})D@58APIiRExD9BYza$OK?JG~T3~JNgCL18-S@I1a zcaT2{ zPQH>t3oGa$r5A76Pm;}sNXnY(nu=rr3**a%JlY$-oEj0j4sKK)9SDoUVdpFf2BIXUyCN^;#3)s^Vjg7w0whveRDlWG~fb$Tf#(F|U48xEcvLEsY&^hiK8X zt~yywSWTZw z+?R7mglxRj$$v#1PK>>%gxkp6=RJWlt|-vJ?8{>m~wtQ{7~7>mRu|5jGKY zGNZP&KtgGFX3d925nO1Kg=G;i`ddohPgV6syq}uH=ybxVnW}IMOQ@OajPJ*ShT)`8 z>0?<>EBQwt5YO?1>RVl7K~jK3byohEgZ_%TJ%X}%Ln zTkyzVK-GlX5hat3lAFwH!$LHlhRmyYHKY0z1Jyv9QH8EpVO>pK`XwS=QH4OJHpG>= z39Ee>u{U`rZ_hHo8f7sBu>?ZDzfb|tAnMPHrzYy}SmHD$BeK<#$3>!=GKCN#`6ic+?))A5g|6Una-?P0$fhQP3)RgP+KX=He_1DYZKfXtYwC z0g~yMBIhd);s(DOGFsR@FlvaU@i2OPHQ;ejn_Wd7B%vwa@?FACPQOQ-?X2N^#XP8X zQh3h8g{fCxMrBLDRtkGc-ms?yQ>w4SUm=|7>Clb89BY~Gx=$LJFVE2!N)lb$9(oW(l&%n z(;p-Mbz$8bB(`1c#%+t3k%wsCV{CW2MZeW#Sd%g)v2!$h;#iW0dvl`~L}=>Udg|yB z9>|)@Js^fRP`LReGhuB`%8i}bw{-7=b5>Bpd-zLx56fqZ3YR}Hxk5e#Pj(};I??BCGze4{Xf&^m{b9pKp2*1 z0|Ei;FeIz3{gRmB8lsE7bWv&hd8?0bu&AHiOuGXTPEB*p(s)y2-p7!e4ISP_ALz5r~jtjw$cW56#N2+YX}3q9^$0INS_KrlNP z7VZ2)#&#Fq{9OhFf?(GDy9~_A4)ep`Wt^<+F!lc?1A*B&VP^iD3<&0Afi0iE%Q!gh zZomJOG5oE-`g>R{yMIM9RwEV+uf&YDni|i?)-Ll slipToRight: (position'=position+1) + 1-slipToRight: (position'=position-1); +[] isOnRightCliff -> (position'=position+1); +[] isOnLeftCliff -> (position'=position-1); +[] isOnGoal | isOnLava -> true; + +endmodule