From c681fcc2ee950ae43db503d4b5388d5e178e57bb Mon Sep 17 00:00:00 2001 From: Johannes Theiner Date: Sun, 10 May 2020 10:19:29 +0200 Subject: [PATCH] A2b4 fast perfekt --- mCRL2/TrafficLights/v4/v4_spec.lps | Bin 2247 -> 3156 bytes mCRL2/TrafficLights/v4/v4_spec.lts | Bin 25171 -> 3439 bytes mCRL2/TrafficLights/v4/v4_spec.mcrl2 | 22 +++++++++++++++------- 3 files changed, 15 insertions(+), 7 deletions(-) diff --git a/mCRL2/TrafficLights/v4/v4_spec.lps b/mCRL2/TrafficLights/v4/v4_spec.lps index f9c31e45d4d0760dc355111bf28572fdc0abd74e..13c7fda4968958a3590a22479b2064b7b823ac33 100644 GIT binary patch delta 2659 zcmYjQX;@QN8ouY|W(6_9V8as3Mj(Kauqa?*2n0w1Vn_l78!>?dO^rzmp@6m%NWzk! zPFO`teIN>gP{j^*w08Q);u6I^R)tb)J3?u-wVlT<_D9V~)`b|5wY(72pTO?3==4~!v_{DlgurMAinFo1~nyK-GMjOm!s7cn4F{?Xj4=QAb^pXYMwiZ&y^o2+hj680KY|JR+x2F001I_ zQq)0!AktVhLbKTbhXNWx3cUo4Rp6c%lj70VUMlG0bo%D25*Wi;=#)V^L<&mN6Yiwi|J1Xk1F$_BuNi5OtO>jeDg z+_BXfLk+rLI9=-V1Dr1Hxq;^Rhl0|B_0@mjh#-IlxIhimINioSYBu?eKy7bh_eN8O@++Rrdw@Df!ZmbBK0wms2F@28GR~PZg(q#$dD(7Cr)JmY2(7c2R)7! zC^^=lnoV*vCGn z-As@W0WanFVWQ{(xwG^4Qj;*|M3McDD2>!&x7$0rmfN|68P;fz z5UX79yH0rOk^~1hH+lI)~Q@$H}x3^;-HdhlEo|S4485vno;HEFeczF{NPKo;6 zYllj8%S?7`>|Vvii2iGw>^!+_`S9y$4c%hrfpOPyNJoxFlJ$7(U2Q9JcTYQ3Sy_N6 zcURJKsWSelku!tIA8*aJJ@%e<@-Nd#diTBH8`R15@39y2>0J}2-;dM0{6pUKZ{MAB z5(IH1nzT1KW+gs;Z+oApQ^6lS8LLU06HPztJnM|Pz$TTO#gAZEE>J7VeZHpr0l0f@ zR@3yk3FIMkNIkHmB8@3uK`?gQWba;*xbnfciWb=e9RH@?x8>=X@|n=n%XNVV(^|yl zk#{JISY#Qyj&!m*JNu`BtpeGTCTz}w!6!l!p0HDh)PkwBrfk;Or%u=JE34;v-iQ~< z5e|!-#T+=oub^KN7m8`iW+%Z)wETJ^;VSNQM>;8YR#e7No+Wgj z@GKPX>ds?!^xgD^q_s<#x3!yojFm#Aq>xv z4I_DUt(?83zzG-CclF}#kSIslt{dnNW8>aDARKee2{=hha}sly?+){*>dKG+o8wt@ zk79IdUAgbRB*5<6q&DU4*S~!m+X&o%~V6bz96rSL@@N%n9B&CN~ zLZgEvbE7=ExO=Ej_9?6RIyF~5Vod5BF4D;6KPto+*YnX;K}Kk?b-iNnTRP$HwZ8P- z){2&uZ+z=JSYHlCI!At8J9g`7q*E_a($BrWE;>?T7)_vye;yL^&wkdot=<@Q&7BS} zF}m`>ZmBu&2gAEHw?CkGm2Jv@@!GcvWrpa8_p;M+y~VXHkB9D*RqP8XX&xERDA&+p zg08$pt-a=c`z!8F8=vQsPANAN7Z#1Z(@&2wf`%_r>j<&^JzQ-PZ%%qei6?%tXgoIk zG%?|quUn~_`SeqTE8@G4ay7AQoR1?miI?^julcPYr+IWnzB5*GQXa=s^hXyiy?-*` zmiWwP+f79LOJ~QHE*n&Tuxb#HRhU9snQanG)~?5p9!I9F?!Q?l(&8%HvSJc CwvcTA delta 1860 zcmY*X4N#ir9eb9t0MI(g2#iCvTsEE31YH)TBg{-f8bKIspu* zJU{YPg=;6E0zf-tt1&fLYr0L?YcQA1N@a6kGARKnDJ?6n__kcBQtROqK<~z0bAE$S zQX)TKwOD)X5FpnZY{q^L}|5JAV5(WoCbx>W`R=yil9<%9yw7tc(NN& z(f|RVfD2ICv(j^jCryb20e}IRU>C?h99`B^5FjdyxD7Cgw40ZimCYacD}2O6tFl-- zTMYJR-2|dT)ZV0l06}YYK!B0J#&7>85=C?K_ZAcuy;v*~msHl&)@kY+4(V{_#wTi? z^pYH6{1ibT>1lD`BSMCY%~6+oDBAW0Si*ZBOWtY9Jsyo zuVvMAo1Jh5$Ro<~aHxSfq}(OVLpA1Z%wX5rtwzk@(D$4;VdyrI(qJlqAj5&brNswO z380FEJ=00To@patWlu$tu=3|Y>GPoEX+XrDI!shy7N-HHE^n~57%Yirr{jYM!oaAb`hc?PGcmeIPD7a;VFU{|2jt@Oin27&pd)VHCsPr| zAFJV1mg~Z<-UfbePQHI}C`qn;BLGF^gSmmQb|x=VDZT2ab^7@^fuH1XptUnxMlcc% zT}!j7M%yt@3o9qgV`lN%R>PiIwXXS*<8q44ku3U@_oU8lrrfx*7gd*V!Xo4)f^7>t{~Io z`aViEv^d2-ng6!(*E0u4)SZ!G{ZWooR=-IL8F|@iKG!xYcb*z^hd>ftnu)yZB&=cc zoAf;%Z?b9$_CA*0T+}VNsaH+#@s+-MHnQXLb}>_)xfJtuXo_6&GlOHpz2m-WMfE06 z>pMF*NGZ38N=DotNqy!&E%nCt_rg+yFL~%m%h^PJJd|RSm}#7fT}Tou{P%(0(^~|= zKf^JuQ^bA`o$dVK!k~PrV?`mEWsRMEb?FmcBgH>a$-eJDOrB9u_WHgu5Y$?KukN9I zHD{;rN_fEK>A6d4UamizRad~D%pPsJo&WCS1&kn%2mZ3VUOAOZd}VqGh2Gwk)g1DTryDWt~0Oi$3$If4aQoK|?d@!BEdwbeb}UOj9Ne zf}`SFoa0Ai>GORBeTw48o^^_R)kxf2&E~ z(qGEiDo`&>gvi?ZM4wKZ}py~2jkv(itleqT2m z%{=-mwnWpl_4?tyH^pVXd&wE1bHO1^uB7uqsr1gZ;0@Ld4_k4=lS-f1H}Tu$kn2P5 zkaOhE#a(|x$4DYdn&95bk^MgZkY%UDD10>j=`KUz@5O)Er+gT@oKd|}H&Z^G^Z53o z;DGAilb4pdevZDs91!|X-P-oXsloFr4F;7Wqhd~-iqDfyyg3{SzH^RD~+jBbe0F7v)}pnd%^X! z(}kYYh0LLy)1Ccqa&2wzo&4wf&N=`2 z&;Q?Z{t2}AjaIalosBt6W-DgNF*|Uh%WShkFimH3xC%@#oel-DmPD*AT}QP7O&tUW zW#aXASEIpVcDmL;Fa*I&oy*Z+bY)xE!+jvKv*Casw%VwhRKLf7)&Awe{c|s5kOEaUW-s*7-rJ4 zZ5CUD1A-|I+yqwG=)iFz@kZQYv26nig|(qR2`q_A4L*_R7ZO6yeUa_B5kz9piOh9= zLSftNcAL}e!e2NH2H`DtIBeSxCd`20z+!uWNo^~zn(*z2KoA@nwm5w0pQ4Ze8o6^_ znZCRlLqgyMR(!kbg-A?-|C)Gqk^$rg#ze3Sjm_yNQokT_&a&Ao5FAj1*~#=6C^#=1 zZA&_u@|0x_~3gklkvGR*N?!qL&9WwCMb3CmZk zlq5=%l2cMwrKM-AUh`*}JS#g#k(-xaP*?-Q2oAFPbsZ`TL=_8QG4UdeAUUKFL`NEd z6SAG4xR0h1x)fqaCJe-Y`<&AWT^cd0A`FBJ4y=^ML@*DG#1S+mN+39p+{*JE`%)kX z3d1~@4@bf;QJsl~wJHc^7=0z+!wYK74ksuU%;EBJno|lSh|2uc2`semcV0k2b0+=K z4P^CuH=v+7lmF-jcKUlaprATa3>vUqsx#G~0nt%sov#$-M$k(LjixM87i&ro1|`r~ zhgmn`D)YuV7icLzGm&(WpT1BwEYjfx72Vf`ATT(wOw5Hl>J4TqXvkGGnNf>lplm1w zR$xT^geo)oC`F9{C15^Dkr`k7$P|<)9Z*jdV$eGVTdl$A0->D-3s!?$oCeHl0*jbk zX3XNZfJW4Um%*yXU6{cHD$P)bVN0PD2gIz814MK@%*JHGmGRHCu6$!QtC- zP}+(p@OqGP6}*8+8kfkRY6y{` z3JA@ILfiX0qN-uOj5*XCbgjRg-4)=9fEPD&BX@hDKm_7MM?x{Vk!Tu+-V(Zx!OC&d zLt2m#>bH}u58OhHYC7VukQ;O?v=Ei#yv5+kqwEU%dyXW{bMjzft~9cR9n5(Zxfv8h!cuv7ec~Kb&=?_ zMq98ej`LrnV2eC1dphei$?CHBX-FDL3tu=J~^RbAxXQrZVSES~qg6H`=uUwKF z%Bvn8iOpPA|`9N;E6#xixL8_TtO4yLDD<43End^Dm{S7v_q zU6tmW2?e{zT@ZDadN9Xver3+VwQC=|wlzJyt40|cvqd=`e&vHiQEyjJRLAt=(o*hB zU)|Z`4R`Xg1a+6%ldmsl;A4Hk_j8h?JL8Aet?$ts+YxuX>8T8QQGL2ut!#q+0i8i7GSWRgGt@`_(!9D*j9gK-x7+=YB z+lNVyD6bzNf%~b=ei$V1OGuvhg@l9(QZnPDViLyo`vKgRm+$pMnq=g$g2Scw8AN~J zuI`gro{_Xh`9p_!&6XKIg|p*7Vwhf@mXX#0Qifm7sUzVbQU-L-UnC(Dl!ov5?x?ok zkKmH*Gs^h$+Gamp@;v3zRDs5?LTdaHqMey`kg#4xf?53|5-!+zeu?zf=F_BMsh0#9 z`=3UT@OkVI`SEL{>iNkaU)_mm_Uq8+duhrz#qz7*BczSKxytQVLDA1PcVQO;za?p> z^mxIe-gqxblP3o^zS@16WI=nSYY%U#I6_i%IRBGoKMu?ybt$76BYp_a%lv>g7V(I* zu1;-R^1Aor^H2Nur3X!LyeM$Dc@yM|m#rG~MoQX4fG_ zR>tA@o%cnOSFLBbMHl4%IW-a$cnd1o(d>@#vQU=g(v)UMNQZ_tL7(g0-XQzANQs_> zM%u%T6$PWre0*|v#n||=NlDl8K)7i9ZpTMlDrV=4$9@){$UhO$PV0}NpQs*-q4CSJ zdlHjNg4+@$>v^y?KEZ*-?|z_bqr%)^FpbqcedMUJ zJMC}+tcHor2OE>u@~BWH8&zQWa$>5vw^6F; zy`CsZ0snP!POYDNQmElg1@R6S_u!#bI-w*Bf2XjNPgSey@6oPw#zpMjyYG#uFFX3< zz>l|MA;%FCXrJ=Z1DXOzF{x%`>z!O_A6P0%58mG-LUT2ilj%boTsMT1WZ_g~G? z&F+h?RbU5q5=CpBR@hhNd3HTjH7Y#nk|*Cz zy7th;GZ$*ltFB5#t*jzpScT`x{Z!Rd)eXtOLs!V@3T@zDt|o~b>cJ;P3460X>Q>1) zcQ2S8y7;GawegM*FXFANoPkZ{p1xZb5~enNFgEwl6@0o(`&Gq<=S61<2k)sZi+6ZA zD!KUP7!RyJzYsnFF(R@JBq=DI+o|CIrn9?_abuXebJY^UysQ4f1X)fpEZuR zgie}T?zj9nu?`EHbRGDYeBsnOOfYHLb6?SU14(WBDe0p7sC#r$+IBtga_iCV(aGet zhw&E**Y89z#+g-?o#Rwxo0ak9woUEhB4t}Gqi>P*Z{s}rEce2(j|D&0v3H9fzkMlm zzH}>lWZ9FqU+2%?-pcM03!2_pGGE%s?q3$#beubXyOZ54e&v_Z#q*^r*zevr{LAT( K`P(bl(EkB3&kkJx literal 25171 zcmZ6S2Ut^Q`?zyX63AeNut5U^2nh;=At2yM*h38=K}3asfCz{zTeP$dQpXYrudZZCkakdcW zuj?C^m9R5CF3oReR^s-Yox9U9kXppC*vU4yHK703`kDa*B6F-I& zuaB*<+n35e_3h5`flC@R@nncJfRlA7=C zwB38MFc3B?F=6QnJF*fJKMuV&F)eNP=NO3asW~HY`%*EH@Nu#T5MXt8XJqWo-kFp5 zKYJy9tmb58?fx8AgNP7B-k1@buwi#_dO~6@tgB1WH!y@Pfpj55$PAzD6e|c@+B>DaQJ|9|T8k-Gf<)a~Pw=^D#({`k`^mbcW4 z%TE4y;CRmVrB@5ArpB~iwc5cECSu9kljG8NB!=zWk-YSzYk(*L4Yfh|KL@CT7W@w) ze0rfRi7^n_D=sH7Ygg>f^rhEap^+N0ou3%Dbe`DY^rb8g1bAforx3d#ZV4_$pMGMI z?MwUp@4;hnO9yYVboL%L>3ep??oNu$&RKG2$EL-_C#Ge`#-%4LU1ev^&bTy?!9tMJ z(mzC8>$YUzy=`+si^45Xit7Pm7! z_J6V;U-`I_kxxb^*vnfDN#C82h`>czSgMc5$A6c`_S+M`G=5TCTK3WlM;qC*^fFA^ znVy&soAqhW8oTzSRKH3ni})UK#3r6SCF1imZA#)%v;I59#{CD6!7ypBIcB399^ z(!~&w#5Y73!#0p=h z%4FTn2dQ|T(^%&(2c|XAHk=yThKDwQHpr3b(7|G(zzVnTFQQls){wYAS`~)|JV(ll zyDsQRCTj4J9dHRK!y+`_Gt&|kh>|tPy%%A0gq1J?D4g%s>01ca*y#-Bj|4{%h^T6~ z=-VWXfOQ4kLN#1JT{ZI0-riFo)xT7eqKK+s4cTFf~uq0-QL9C_-x4mtu3 zmPMk)p69tD9oD9Hj0gZ7wW8%+r@VnUNbk0m4`Pr)m=r~iIXV>v57&KF_!r15U6Olt zJV=9FS7JB^5Dpi&dWYcGECvV(ps;S5tHZ^K1*j6{ zNRWZ($%J%Is{iw6u))k?gD<2jlnmuXOBimLKVin!zXoaxRO-7~0aA(}!SG*>Uk zPvHJn)qvQS20`R^w<*giwYYVj7UMY9(_u2IqU#jp-7P2_??0wHhN>L7ls{%kn8Bm* zzMhy*4;U%+y&1&NBcC6oqAINdi!~lJ*-hrtHa%2D(J0zFneVI9eYCo2Srt#oo*)vr zRY_b_1zEInZjMmx$oKB)EUStw)~=;VdRR%1v8YOCMF5(_r9CXmm-HT%FhVHZB%kq5 z^I!z;Wu;&hD+EMdl7F9V!Z&sOSM4#*TC~@#btO&LI?y z!IHh4`+#GSDCB!akSY236Fff7n|*v2THl@l7ML{F$;nkR5QOO!<=ihR?Cd+t<7rWT zn72WvVU`UxZAVZgKKz{ThU6CrXpz$@PMy|7r_<-oxO%sq1{t^=W}eK^mx0Jd!%r|) zl%Jt&9OwB^A}+8|wGDo-{BvKbN-bQyOd zTVNDYtlS8M)}o{VOf6D*mu6nd1I6T-zm1lk)PQiWb#XK%tHjI#?FuA;Dh%E)XzwRw=nWls8Pp8FC3(U@mN%YO{pL13)9?cy~3 z1_W65Xy$&ebQy>o48Tu}o*(Z&#gibw|B|dUe&s3t6hUUID884~(G6G~Xf54+Ed|u6 zzmkCk#)YGS+l7GOgH6SNst&!hzVB^!cO9MyORc~FEf%iy6O9LplY3SWo5Y`5Ab}pG zZ~#wil_XfAYJ7MYSEDG$rXqj5dRfJ}?dYjXi)N|~sx7Mw{gAuC`N^FtiSx@UD++do zqS-2rw~~L7WANdXh=yN|Tg8WwdQ_zc-ClQ3S7yNa+mdeR_jLldz^H$|GzC>SdQ<)h zH^IjrlUvXb6kX1DCE|MK7Ze?$Whp4dZH(uN?{@tbbbVRHqIi!I zG~@T5x4`g&mf?Tsbj^z2CTmd@5tHeCU+VrR>%s&@21Gkn41XT&m+#*9dvH1Ef|}JS zKRvf9nmv5nk_n1%16zG_5~|1*XKqSRl^!Z-$q|A zt5#CB-LuM{t@y_3I#8))yyxUR{;;-U?BO8>K*qyFj|URoZ!FK(W-@@n%!hZxgw5c3 zejineKOv}@Cq43x0?pRQT2U2F<;BgRjv0kk4c4G4@|9Okclqv*n4aYtsLBCD4-DTp zo7?%D-2_l!E{de)SMbEy!nWffpX3;Lfs5qS=Ga#JIZ?N)x<>T5A5MG3x__Oztb*xZ zY!39z?cZ%DMOBiOlwY4%l~aziwxTMWD$ln^P-PU_cfA@_5%I6w?(yAcnD^y4ROM+n zyhRu^?bn@tY8I%V_lR`Y6kdJyz{%s~m`@L!>OH4t@`Fz3o%{8uYUNd;=K~%OVnxpz zEvqo})NLE5i+XpTYDHB7hV=9s8v>>7vP@RM?Qsc5KKU?mv(WmIsuCi5e4J;&++q@h zDufhz==R`(qOP=LiKBGYdK~%*z^tGYpE}+$i1fMy;X(*2ZWMtP`RZ6vQLy{HaoH%# z^a3ISbca5D`{#azZ9VDF&0M4hyfNs89D+d}qb03Ad;B#Ba4IF&b#Y8BwB&O2@TlX@ z~67dJCa)OOQA6tkc1E4uO+1mxS)&J<%W@uvvdmnPL5QkQ^~Ll8f|ZATUe)H1Il zE|o!Up?_6ZUmIN)?Q|Y+Sagr|B47vH_GR+OG__x0yjA=u0X3&c-)vu3AwAk5l4be+ zSh*Sj4GmhM7hW|EoLUp({B|#M-ew04@GwLAHou#{Om??7FubIDYV^=4Y_z3S%A`ya z&YiFzDD?iR>Jd;+9zL~J=tL`KrJM|;w(ZJMp&P=_2zt*n%yFf?KUkIU>rd`bf_nH> z3U~762dB`c#)1Mn=Pge60Ecq-FjJE}32p1szMrn`QZ%NCLE@sC)HT~&gI{t+Bnv@) zyy=Dj9-|jJ|E{Xo&O6qLmdKJDq|yKnGi%$!9Tp4v+Bcg8NT(|F(G8dr`AuE%h}<{Q zzDh4tenN_FKu_(ItDyVs8>YOTq}C?P8b|;hb?&6{%;xuMQsE7}I=}qH4mRKrG|v%q z$W249PgSA{9A>9Sw6fit#k>=NPN8ESHxBA?iP6`OyY#f*4HJI?kRVc8XG$PUNV}6z zB|iK4ik{-2GYQ)%b-be_38t|irfK-8Eh_(p^( zupCcB@RH67eSM@DyVGY&_j7P{?DP@Vjn63NZF|!P#X0?~yNk+ z?8yXJ;-6petu+hM4pk2A4+4k?d%Q>c+_q-#1Q63KLKnWw8&!Jy+cswoW}0=ca_<49 zm<@5##2q&1@q1iHi!toV)@k%oxPjHNG{8A^Tjvq5ytFcOLQ$js+;dyzDL}BzhghL! zvX8ax+%uM`(Q9{JApVqq_BlyUtifa0wS6;uP>O$km0SO?0dqt8Z6i9pVM`->QwFb) z8Ty+w4OGR{Cj@_ajjPec*h>|ELeM^4skJr*$1duc{;w(ksrPEoxiS0A(PdR@qnF?n zZHQHI)MHuIl#rQy%~zw(Zf^pra@3Vxac~wZ8&1q}0(_|#tLQgce=I>2dRSwZ=s(;; znH4c#!wKQ31HP3?*4{SIib04{|J}|7%F;`-Qp~3Zgz?D)D-6f*;+V;e!SAK03WsZS z-~5NWDT{QONCPzvx(RWcu5rS8m~SOJrNyyU2icNupHV;(epSyk%*)ZZQSke*p+?7T z3%qV7=_@C+RYxmGoN9U?{eqzvotgA%8ih}>nutX{TZU$9B&{M?leT>bG_u{DK zX)v4DNk~i6`~g|eK$nhg!dD{3Y+C}6=C1Q!RlV;s_yhCCMM-Qa zDAMQLTO%dNSj;~-J~V)YrU^004&sjP8~9xDCj<$$N%xA%Ny>v>y0f4NAKu4#R*=lR z@vwBuvWk0eZ8brb%F4D_O#@X+s`La)PDk(cVt4T;1PRQg=Xqt2@{p&_vWnNoea3yO zcB8pr+p^04o^uUBa+sMN=eDdOCu~TwDM;(OQ5=P;7R;p{8BJv6{?)p)KIF+D!|le) zxBklt&OPsAMA;WCrEb!)!Z6`8u0#IIzMFmxK!HK%K?vs4gL1F*_dfwNJ;~$96ndeV@`nGM7?f`alx|KwsgYITt=EdG z+>dg0v`icJGNrugx`uk6HL{TqiRfzs!=Q#yb< z_`g0vtC1b`ZKDJ^-{=|iTiyt4eHTy3`V_hGIBv(lH&@q%?MDuV+(;F5p;qnj#{Ys`)r&GYwT}=U?m%wQlC|Pd&bj zPUD75JHgzV&UqmD16i z5>#PWMQU7KgM8&{J28iV?id`a?Js})I~U1l3m{OgL@qU^7(V82XD+Lz2bEz7L0?OQ z!^)Rc6{Iq|8qNofEqer2(J`#yr{ROe?$S{Upu$dL6qL<@Ce-*;2C9O&aL@WgGb4Uk zS^=suA&{z9)n>+VZIuhC>H~pQ^rt_JcdQ;ASXLo&ipSSfDt8A92axtmL1)-wo`_G} zTDh#!Amy_Ty&6Dlv&K=C+>G`1w^#_j&U{2BQ_SvV&_K6Pi<-C5CcmJ+>@hEc|LS5J zs$lLX9bHpRv+%w8nn7osyUaz8S>LyKjp2=Ho_zKl#e}-`>(%HKq?W<%gOA6J_?hp^ z$fPP-1PuIm-VA4$^wx`YH-A0Gf2|QSAMmB$<|?-116NSfc&(^HtpJ8ziY4) zox+DuUhgi*(B%%7BM4}G%VsrH$Ey6DO_&fM7;$_Jx?*nk|5}$CmfZe}W!FI}Mhx(V zJigQHNm6-<7azHe42S%Sa$ATsSGHllzqhU(%}8GB%CUU@2jk3*z<4m z&rSpG@qKv{Q!vow>mL%N#cF>ZxBxf~f5p|Dxk#6{Chk@Nq@zt0gek@+lm}|R0|bM3 zgoweC60STO6jJUZcn@Oy^D<80b(#-rq}Uf#8lF7iq0=tLDXjEASAi-Av)Y9Cj$bBv zDg`_)zdGdbG~kB$AyT`@3}dc8lWxH(eIi5^##a-a%-SWxa;v&PO08c=>swH-T}bIH z6E++0b(zPDLke6Y^8i=NyoUtHKiIJrru-pmAA?gqfMciWiovNJ*xKCavoq3uZQ)A5 zp#?sFX1@Et^=9vIWYo7PMOzFKV-Bp&1AhCh-E`Y!RQZtW7b?K>D78^Z9W$@HH70|Y z{J7{N(|{Y6U$10^Tb$w)r&L+7#(#}OH$War^fW&un^gGr1`=zNHyqCe_4wJWUgFgI zXnu=lIX0wrP2@$u;f3?ulKEs!mgJ|{p%ZMwQ!#);xn6Sa8yADxpqSSDi7xFa2f#5G zWB3+-m1&0*tqVttks=dAF-XL$V@(&X$0d5{Bul~+g__wa!1Ii2GvZniWuJztnGb&; zpm7>-6Vmkt#%WMC9sc#?33lC7SwY=a~bOUMySxTbo`xShS zO*#I0smmQN;K7HV=cqNwwOOhkg#J(5O;XzP6xj8`m9?Usav7~av)K?@vyeo~VL zQ(`}vf#<3>?H7Z@TOEb?kM)qgMCJF`^b-MNs_9+L!^j;R*e9Pm;xV8bOF*z2CJ>1=e~;1z#U%#g_NK>G>SZZou%+k>7CwC3@AI;s#$pNqG<1B9PW>08ij{*wO)DkI1btDKNJ-+gL7po+I_#aZOuu&e8w zk%TF~gbmaaY?36Rt=a{0w%UpxjfV4kJztpq35qbymlfN#=c!Gm zHt)C#5S;l}Z+2zS7XF!6XGH)Jzn`yrMt^JXp4u(`t8(}Rjt4CbaTeUpZdouO^#0V z+XIg075d(f9K)r48}jp2%{7Ue>j8(`E#xm14rVUf>XK(ly8BLt0uBjy6Q4~T$~URH z-@h=#xqHW23=(pB>I0LXuW7E`9__BH*p(Wu0z5|Qvg`Ej{D9uxj`8G)zCG0c|B6>j>LYtlWLo&5BJFjS>uJS_Y+A^)VZ^QAM|Hn)V}2Q*x?$|rg4RZtJN`zvm#$4GnjN}d@3L^^KJ&o*bd0A0eTcI!_0uX0OS8vqErD3sp{6l(NrZg_&K@Y9jq z&gRX`iKOkvtD-9(=2W7kuUMSJRb#HHKV<%VZIx%7JF39CyDGwLzlM8u7R}8@_PQJy z0`-`SCKD%XzAKKdoyf^la2q$oi9zC$W@?Syl>ce=F3%D`AlV-I`fo_Yp5V$^bPDbK zJ6%rAjHC&h?oJV?A`W^M-PsfV0%;uMhyk)?y!gdq3fbkg+fxk?Oml?dz%!w4PiDb1 zs?un3>s$K0ht0%Qa+AjWhTESnf>PYT7GIOq407sm>+i<_(!=g@NjNWCB|mT|7C})( zPq^}FL7&oXE6;5rfOSv?I0d?2dL@(dfMaszkr<%lwW&kGQQWWYN$2+gf^FWW(D=~> z+Y{F`Tku)Wnr+^ILxR;4C8qmjATr0^mkecczU7*v|0V_~$04zj)~_l0D?{W zN3PLNQSaf@&lddI>Gsn$z#)OpgxZ7iBc9@GnK=OA!~aH%etYKl;-78z(2eOM=Ia#S zHd`qc|6_}Qs+fYDua3^mYW4s4lR2u|mpSp*--k*)k0A@os^_-8b1SNJUR?5hgsKd` zF<;aEg}bkO@!;BJRb@_0_1rI7-FLiq{hw;zweKoD5Bk080SG^5%b7d+f$-v|i2KW` z<;;eziHo0NZzw@$BLZDoAdZxbY1q3s$Khbnns&=79_=>ZM zyYq6i7$oE-FAl7E_-vcgnZHs1f!$xoUDjzLAlhM`6Y$M%=v3;Q^v=omL7EdL$I6Kp z3Pb-8fFeAvAKCfUy{Z>)c2DsDGW+ExpVNQ2KTu45t&gg*kLBz;_~e)Le&IiLpa>eX znwbCYc;SU38(*U;b&rF-r#^hpdeQs!?Pb-Bx7*pj-+n8f#1t>9Y8Ru$`m?`v3$Ra6 z)jsk>ig?rh3kP@_ng8LOg0jRQaS8uoisqs6_H0vg->(pg@1csAg2j~1l`|`PBe7=N zC*-s+8K`&Q?5p!5Eo|hr=YOz!QOEN{r!bUVV$0RtcgTgvzh;Xe4f+gFPacoyihwVM zPB2B;#rul4YSaRb4?l}2@~L_+o)9ci1#SlG)q>Amqo}3*Yp|HrwgOeaS^0f}!sfLT z*Ck&c+}9XFrUC`zt{SrA#9&{XV0a9F>2g}F9B{0Sw!BXEjJU|Jq@W6oCLd*Z!A0AN zkj@MlsA5+BRTinCisjf1aK!-Gu6=RE-D%)U_p@pwKrqcK75dZ9@Qd*UI;e`&dbx+k zm8_X4Fa4SZsyxR2st(u4_?c^GktYV|nfi-jy2sF$jvXbh0l~WeF4vb_!!B~m^+o_9 zwSLtZ&Yg3ZAhmx^1IR7)uY93K#&?Ka%T_T!_l~`I=dy0_pLMHCvH-z0i&LMBpEX^~ zyI?f^pxLRZ5oUuuTX}9bN3DL7=5yNM^_fdl(?&15Wd*y?*|s=$JSAb_nVLq}Wh3+q zi1`Cuhlb3e*le6H4Tx;C)k=`6Op)rk?xGkVTej(QuE$WJHzUA(A+@da0s=T)S0ks| zXxgH$-fAZxP&1A_G0ex6H2Iaa0i^CB849W%vot+LaT@e>Wd`yAhZjdu+D7CEh&=T* z1dT@1Ey_byc7R~!T-f}_Ul){=b4yW`+D*rSpzse&(@~PskgtbbpmbR^muk&;RH%_~ z!gM08r}p@mJzFZ+NdsBK10~Xss*H@m;Be{+)3Ox$@|m~}Ijss<%uS&u&my2SOsCTC zfY~oIoz=(9U^b;EoCdfXo@`MwPjR zD@#EUdAzz`XZskRJzE(=1BiG%pgFi~7z9`uW2nsOgRyCsjng$NH~VYxfWwQ_lq(G{ zCn}>V^idVW?Me`XY`5Oh_lCh^LnJ%?WdIEX4*mg^+e%y72TC*N!~i{WHNCxIl@16D zTaJ6$T^04D`kk9Z0LrefOg==(yxnUs8x9CY;>m9H%A$dYcrBnd@Sum$VEL;cF+i8R zO{-(E%}jeYYaZsY^$11`x~~XAL?6#ge;~2B^n~O;ObP zA`sx`8dMd;9B0!RT^qC%_jJ1#)0PYJ*d(*mqTzM~M0&-Q84cB(u0BIO3qT-8H})XK zj|L)-v8xT-Aes9RDR^28P>{N5i=F*{)xWq{Thq3t6t|5dAfH`R$?Iv%&s6G4Ie=g` zq_eqfKK5#9h5m`NTUtfrUM>~Wz~~k+-p9w=d=C&TvP{7Vj)_5(FdT-+>lQ!& zA*VX^B78uAnG0vb^MNW5;h}HxzzP;eY|KTMh>ME2b2kVu_lgdGSY=tPx9---ivVGh zq^a+E+Nfb)Ye~^d5cA9WXC@e#?DrS4RiKIj*&I6*)IuM6^?W0$YM>sz>}{u3v*!Dg zUI4)&cFMcOHiNKONb+CRX!kT*vX`A#@+GP=$DBMUxz3>uyfXfLSw%Vg$ZB;-#M+xl z4*|m3grx4RynqkeO{~cPNaL_w?~JpfKKtUyJ;i z3n}M1+Q?y>^s9Y$DxY@$iIyVf?5%DwDi9IKCoAf2-30-JSsci`w-&9V`5YemVyy^7 zIE=H0>PZ@!5|^ZUnB5YCNQZE9hhB9j2s9dvduFp8x3il!Y=e_(8o!SM95)a)nC+2c ze7H(OPaSd^$RB^2;_gTy-VC%N7N|NOi{^4EW|er2r-kK312iO)m*YbIlSx#|_8H@h z*Qeeap&Q`7@PN2Te*!YcV!te` z)-gvg01R#JPR#B$Wv8WYRRKiOOgeDnRs#ss2Ra5i_d0_B!_Yi@XQQVGM7aEJ&nr*D z(3GSvb@RnhF^KXEZl-EiFJFRluQ&0Js~`g{tYvq66{P|ZQ9G&b*exRvs1Ljx?8IAv z07J(fu1C&^K%|MuW)JIYfB=$JrED%35Q8XB_hu-8hh9pf$)hWdgxIp}TfRm>o}lrx zxRNyo0tn-XbQMzxTb^e0%K%#X3b)r7mDiHmV0lywkPfLR8z(3z?%PrAm_@ny+8oPm zJj&%5`8tnK^~ooL6w9sZ7A~Xuj3)-`ezsnoqYJJdoQXqb^OEq8dY{C)p)iZRi^!LbGsLxd%i~$+JyEmtYKFY zL$sb&S2LHDG_OInHN*CB3B3zdt%Uz@9Ill-N->s}psGCeo4#y5_g!aP==`#39b3aL zSo>*y9jhH6ECQ?8C+M^-f4TJiS4CbIP$wHmeLm5IsuD)*zx0e07x&9<$Wc{|NV#bI z6>M;{hPkZbaEERuqW9~Vw~Q?pwk&<4c}-{>Z6@V;8VR=F<`%;P-D>&8-6yXza+En9 zn-PF~)C{WjGi2<6i6+FF3H(=(~bugl5yyL`4TtHl1j-&~i3 zDSPnY%PPpAUMxqHgSYR}yegX3>ftJ!1LMYTr|cvZh=Isc&3?TFzreq%mGv4B%v_Yx z#Xp#6P|~0n0SGIbRsEpPpl+F`^wR*++F#+#6-dHUPlYs#0SZ&I-($xw^zS>)QUU@w zMkyx~gEbABn&qepqQwtI)G_S0$VuHaP-W^8>dFyFGE>@_wJYp}*5MMsNiu6?t6~CG z3H+3Tsb~a5%%b}8lG8yTz=ul*_*2XGXL8b(>z?OnAf@jg>akHs2Lar^GnHX7ECx}+ zE&D`lY~hI>S<1MEvi1NM0o;dJFRfNAof&U9c~wQZQ5pV*ldlf%T?&JeXE5v!`{h6B zlm#(hC3St;a*JktL74){QiZ!xv0GjzoumQPO8gCIin=EpKE-*k$$N zJ;*@sQ+3Urj`bL z4+6~BS{<2;+tVP@n3?LcGJS~FHSbdn|FT64BEy4`4F$V0K%lmMen@A%9J{48_=E}| zeZN!}?hn&W%+hEVh#pS%D|A&_Br^<@ei0F3P{J&_Q(B%Zvl-A^Uj+z8?!0AiXKT@6 zcV8EGfZ+C3sf469N?M#@a6xa6<=ot7%A##VoK#ZLg7CSNTc0hrvbGd#J|lkN80dC) zxph|x;pqjv4vyCkB7jK8dpm6pJ8CI$6C$RkP;Q)el};9Y;VF`RZZsq8#2Asa;iXmQ`wLpE*qy{Mt9*Ik~JdR^GMc ztM?sVnaI1~yZvQ@{ezA#tM(suEzfBOCD1rIrE9}AgS1HFhcbZFxvP{zYu|5HMm^(; z0W!z+RhYfZcsd~3Rt^XzhyCCt`MaUR9%VTUfM5|h)oJy$6=_NOKhppr7Od(S{Pz7` zWy6nK#Q?1n_tluZ%rqDj{e*ssV(!TwRGNM_xW%dPGxr-QPU(%H5))IL7O?8U#Ocl} z-|ll&8hxIFDjYWS6|R_M=k#6o6 ze&`?k~%ocxkfH)^xF>u^_`SU8q;=$yO^Mh+WD;IeOQ+YAVpH~h>FH^`5r;qe< z_DKSj?Lj9=pVbldT2>FXSXTMmsHH|=*Rl)B#y6$#!oOab5W*U#feWeoZtL>@;(dgY zadvyjXT_SoPXmsXrK?&leeihjcukk;Td%4&3xLC-A5*Iz{Y!b7wf64Jwm#(VT)?4y zsmhUK%YR^S@cpb&@3&j&Ll$46pD&nuM;^58R)|5hvGcbsg@0y%0BiG~6vHj`D)Ojyn*$g$Z5m=FC0r)Z-eAIR|4@=u8#Y1 z>%^r_uG*ZolAv1te*+Eyf94yRw)m)Mg^Q>y$MC^hUb+}WhTnX#j-(}8nL0giAI<9( zzRWXXXMNdUsJ6jDxiF3XZWqH&{PU>Uid&b5RKCmanP+ProFnAT{JjR!ZvHN1`bkV_ z?N+lkF}Ay~mVsntNYGy{V%&E8Sw%5w85kJwrJ`4Pw(`MUM&7f(*W$ICF)u_d<*-?r ziw^>_T3OiMk`f6atMks;0A{_(q$+=KC_0C+w!tVz3`%gb>dsh=X4SkXuBON=Ok)kF zu&a3aYoJh#PL^ZmPg+_fS}SOv9`fL*28J4p*3RW7qY7hZb#HBr=IIwQ-9b=<$!<2w zfxR1i`||gUdGNZgM80yIn z*btQ^Vf>`M^c7??v{l_BZjgIC2VPt1vK`1U#?Jel)T%@a^A@+4pVaK5W`3UR46Dw9 zTiu3yoy}5QRRP(trCP;3X=|leSo)i2fj*=L9^=ITCcAnvm!{6K>c?Rif~;wp4WX(T zhmqYLDx7|1xwbP8Hyh}tE#}S5tHwQz&7w?j1;@J~+J=NI5uKt{Rf$(y|0_oBN{d*N4OE?Ke|8?CBZ;~`l$x6nO^MwaY=3ps4<>E_LH z&U^YwT+q6FMAC)JbQDa`s?1@yNLMA}Aq9)in5ok-MUNpb^6l}rto(f>eZLI1^bB#I z+AYUCit1i5ezw8b$$i`xYm-AH%MwQM;V$sfU`+7_I(eAqF_s}ys(UyJDabQ({A{Tn z$wQg{>SGnd1tRdX|2>r6&~!d5p|Th`51$T!@zAmMW&h z`#l^Xu4q(_VR+&mBY0e4b0-WrhEXtxxjI)&fDs7-VW@ccdAsN+BqCuDOoqh-2Inc# z#YiwrvGXGbnLkrgludZvAvyvvNC+1a?+=1S_?{`pP;m!NM8k|?!Z7tsPl=^Ehzvgs zu|;^7$uJ9FjWbj<^VauDXDj@MIrDAUND&v ztm?ywK0;=yyUldu60Dud2%%lZEzmH(b2LuOS+zl2f*8p!EVDZ^-ORy}Y1D{_0m}lF zA?*|{2y&;6s5=%kJt7LIGC6+Q1{1SB7B^3nZN@Y=eIVxO%MRdZ<}{LyehtsUr@+Vn zv9jsp`r?-UZh7>2UeQ&uXfvj^X@+={B07qnW+43aK}Gc>)mCv)(`{m!p-O?1(2%X` zql*3{(6)*jnqCpjs4^uK?n)zT=gOz#vN(}2H?@sUh%Ly| zpU$ujf{XCD$&oOf68s2(cv@0xkw%sn{<6u!og1bvvb}nl8&$l(wBQp;wahjh;1)e6 zm-1jbMbcJ8hZxim!mAEmjYSAqV(^Qg#f{snFS5RRo|{+n*mfY7q(l9M-(tb-(buuK z+RKeEe#=yCI}lyeOK9KB4I$x9VT4?ou8z&sOWc6sNjr!_4AS2o-ooNG>59v6ZG^6l z@gprZq*8wO;q|rvl@}iqe4h*}bYS={ia}6j+X?}`p0OchsE|nOi zMfY^W?H3|-CchB13_II!be4>NAh_rol6wG5(I2-6=ot(xZnn)Q5`zq_BI8yKp3zg4 z;d6-9XB``7M1h5J`|E|bs|9$Ybn*C(MtLULfTlDms3MCeSZ^mZQEMQE9T$4m~dPp&GOAV8-}>u);{at;64r0d<9tQTba z*JaB%3*g zu-dBI)G`fTJc2ukM7#;{dsSY!rPT^|#Hn1v57|FIS@r|9p=h{P-7h|ZYLpLsKDARX z$;v5}P#H@*Jil1>hh9UaUy!w<@J)bUaRoI@RWX0FtU{mBn7?CcGo{`>oD6SNC~fTp ztp@m&g2(Hl%CE@nb%n6DBFnlXpfw5qyYTVGr~`iX#7AdGYPxonr}>I9S|;vNJ>~e_ z0_ys^mzH+=sDp8+E0EY`a7hrpE`H1)*?Ql(*6=H0Mkcl_jZ~T+I%Ta_Wj*6kV5kV8 zHwO;h!hbKUUGHA+Paz&X%c#%%itM8A9Ug8u`%G_oY5Rnu9qo;oP}!n^w=mpuc9Y(8 zxnBu!#hLa)nNaz|fLY4YQSjcZ_uF6baASd$o)K+dUu(pb0LClR(o(~pHicWyes91l z9X?6??QDDftKjmB0kb&#=K`0Yx8Gi|v~W)I@82`e`YcVCGiR-H9E zTxJ$3@QZ(k4-|xj4)==;?A4ipE6apSSMCmd^VLzF}9y^=k8M6 zv1Z4@l~TV(D00eFuhFU{fxAlKMpuRo?#CY%rmatC!dDaB&fKjZT}d3I?uzL0miAB+ zX!rZ$1FhfM5@LE|hL471ZE4+N@c59mE)*s{lJZX(T=%%&U)N#OCm2I&grcX^DgJc3 z^l}nuPqFQ&F6^q%vMm?z^{CW_ws$lnx;K1yG$I$Bih=#dH8$?g{x{z`J?Q0J-s-eKV_(=PdgP71PhU}lpAFs(zeF@ z_^C~Lb=JXT*k5smE{}rcc(UN(dcmdQYJ$P(bM>bJ$(DwV_}D~q zC$2B;yCq>NR_`>^jum2ph@~mNm-SWmG+5&uB;l?bhyM<~&!;RM2Cb=oc6*z-UGUOj z7#`U4%5H)$?XflaZZ^A3-$oSaiqH=QF}bSB6jksU2_nx=oR6vUIyOM26E9w{5OQF3r775Fc7ugS$ky&@n7&%p+e7h7<5dgz;fvC-4HI z=b7Q!Mi)X9bx%Z@2fLZFNSp7cgd`?A7{yG*&?j#!gpMDPzYl(16V~r1wx&f+ap*Tk zlD4!`D2rApozl+|x>wz%klGD;1;K0B9+HMKJb@T}hJL6qll++4%MW%`;t$;v!>t@H zY@i6XHt>a$@VA804fcJwo5ZHGbm?XdLX^I1c(9A|u1=?Aic-2cVcbR(H6^6K9(9ay ztd`FQ>(|PP^L>RbH7vV<+(9+PPV2}G+?e7w!ifzX-{F5D&Yx{Nv^jd@&Zc}RrZ#_@ zP(y0!usOX#6@paBuLiHLO*@c4x1QS~jG#XqNs4i-mp=_YUA+W@mJU!DO79y@;;KsI zcY=>dUVfWUYfK^O7z!gtSxS#Ok&XP4^z+0?2Z>M^NI!Z#IhIx~9}E7c=H=N0n*LIu zflxR~%fi=*=<;u+q9+U+QMhm;y=8PH#<4*DD0rxvcOKd+%&Q5s^f0-xG*GkrL$KZ< zvxXY&?idM_DJZbIWp;G!zw&5JS#T4|y1jL{aPb zc0O4ibvhQz9zOT+TBd5NFskjz=<4vS5UrwO0B=YCMruB~JA&!t;vxXIy1;dI&+w{<^?T5r?^1l*hNk6ytAj5fz zC)U4h%KB9zIS<7MNz#K3=TnIo-fQ)0BRm`SQs~>R@Kv_r&kLEsUeYH~#H=%d#=Xwh zkA@6PV2Yo7ZzUq(@E!tr$i;)juL)VF1vPu~$T8anark>e`TC2;68(tEvw}l=y~=|0 z6T?sWytXi;Szhnv`#x@6jcl%qY`b=Sc&oUE`D^e->DKoA0HJ41tmV5Mqfu;x>P5TW z&;R1_&vv>r(h9>9n@%~uURmE+RIE*$I6GPM&iTeyp|1xpG9^1twlls$*y! zxzmy~9m!j|KPF1gx-{a0%QW<@!*?=C&J>Adh;kx_`jqY%RVQp~U{SY+RE=oVqG7kFN!`FX<6Y9wvNehj~ld$29PJdr}>b-W{zR_I^hJ@+Oh z3rd&vK$z{wsV-i3<12$Jg6Ga8Oyqm(^79j)Q9Bjyh=dsG75;NulF!nZ<-HT>`pHb( zHvKJa7g-C@3r)=b1mnWzF6-~3AwvDYwn2tQh^UHX)Ry8-?Zs~TTynjNd&o~`NEuS+i-t^q2d@{ULf)6SiJiBWb`O^j20Jt)SAxqQ8WanRoyvcwNUTZc*b(|Z)-=9;P{LDIUXZAW zIX-G1(QtYoLl{>R)!LN>ixflFU0dQG<2izWjq%5xOqUjPR90WXum%k9LSt5Wvw-{Y zd4$hY9=ejwObdc9hR@1mb`mN+!gyVIROEXasgE60w{*jzx%8*fK|ZBk#n3T)x5?Ng z#77^teSMi7RjXW;yXgrx;T3B^Ksb1Pc$Biq{j%=vy5JhR%qh<@mQ`aN95Ne$_Ys`j zAQdm&Ipm!VJ8Ydt7)6$DrXC4ThDy&-y@(gjh8?rkC${PD4R5pv>C;)TeBI6F*HJrK zOi9%Sdxec2A&-TY^w;0AQ)&erE!46~>fVUPRUwZBxwO~)?0~w-Q@S6I@%*MnR!CEL zX}Nz6@!{E6effBorb4FBBHeP!LMnu{GX#+Ih6EjI6BVIRIw)b%e)$S~ zq~Nn4(&?oe>yD0>OW&g_%{AC8yvJa6=`7Hd-zqZ%0=Zv!;>H9?`>F8hg6oe);`uyT$QNk=Q15MinQB=gcVCAfN0}(-i zFJDo-x4fX;ByHMsDM~6?GXyW>OcYSOi<;BfMH?+;me*RP<(!n7YsPfHbglj9-_P?t z@B5z5InU=k=RD7Qq7x$)3!9;_jy`k~JC8vwmnm!#(}?;gBM_OPRI-5SB(;u3*ld)d5lkD3)&ld2WQtOqJQ@IWuGBv5OTg`aXr3 zIozIci<`!DcD)xa_glQ)EFg_vBHtPLgWe;`PZb9Vy&E|g0}%V2U8djUJH8{cmb@a8 zT{2|0`FuYE2`RI{glF3~-)9Nz7=yY~U~~tZDJLwxS8mW9^-+alsC2&5s=CDpIk-5~ z^fu_;74oZ*0LH!2EB@jG=>-T=LQQ9BeYGQ z)Inj7jj&4>ICHz{bQBs`9BFEbG^rrJ909;i=@3QiTCQl9<9L?XINLFR%z;dTH>r{) zrVmuskyF)ssQEZ?_#>92V#uKw5lr7alo}G=S@Dy3v8?r-u-B?YW*!V~9!@<2u$!lk zLjrw;o zjXmkWz(}JgrSCQ8+ELzVMDNSqww6|Jf46Lz8*__`bkRjw>(Z%9>Slyzr?T_AqG4byeJ>hCU_)^+& zD)N$G7~?j%OEQs$2m})9_u%WpvBff*(A2f53j*J!Vt5yW;BGZP#kM}$BVgbvI*g*# zk?_SdUcl{Yfezy^Sy+@0Am9MKr8l+S4(lLqV5KJUOF=s6?f@R+P!eN6#5O6uie8x^ z7%?Zvcl)Qu4EMFwe}Czdk#iOkEP}liM7VBWe^YQ0H|1K!BIw65q$JVuE(`8r-cHx6 ztWO{)3~0MNfXBvGDLw|sMGzdbi)<$%Tro^(J6c1HxQMc#hpTNRc=$oP`Wpfc{=IY^ zBm}{AoN@-LxSWlu?-mg7D~hs60t-IM*%7cL6uibvPby@#dcx_1Ft{Y8AYh3nc!uej z+$x&LM&tm?jZ`<1jG9s-c#kof+!}O`L>K^;?R$*tJ+M3Fo~)J62{I5GoYajw>QI8O zXJ88z-K>>0wJozGEa@t~8Qle`H^TZxLJu zza5I>ZKO&oPAX!XIuz4TuVewikL*k4~yJP+vQ|`n@KDvM&?k8vU4s{p-e6py7 z!w9%t1e?JyrYj16%EQ*h=)Zg{r`!j9ufjGks)>r5$Mhh`CyF*Xnm7+L1PwLZP4@5k z0=*Q;4;QIZUc|bU!~VdKr&cSaM1(gWu8YhXHo|7eTEbPEkR@=L8h#^D2OaO2tY{;S znjoaK#KUY$alDOx=P0pvy0w_ir;El?Igut}*zXwj3`{yiM%V$p4fJFFa4bdkD(Ywv z?pIRaJGuLvNuqnCS3iH$bxW9~e#V zxvVIo@u{Nnv@-!q`LL%L#iXKWA_s967*m`efAC=~>>rHzq+-xL8nG8}ZloI5AH;ql zj|!EnsXM_#q1U_h2gbK^%TFYw-GL7=v|dlP#@W`q-qD!e3F&+cBuexT=c-?d1ol77 zqlLB)?z`n^q`pDA0pQr zQU^jvdvEoA^I;_o%aiY>d2fCw4@d}WMnLPQvG+)zZy{`4DV?g|=buI-Fz!enXAQ?= zhZ~E6xv_j-CV_IfFw+9%2O1!;D0xtr>J2{+B!pfr*6N_!+6CpG5=T4X+W~}^x24zw zX>i>!IwRRGK5jFb`F4e`*E8K)CG=6VUeB~p;N!NgWBy-i%;fgbW<`)&VsvPz2)!42 z-i0juJ~t&7{+=Pmdv86uVEwMwk)1iAD2v%-GuM}|>Sau~uC$!;8gyrAEdkHEKZ1C! z8jr^05br!w($%hHZ6xDNM}H76Oruh~4A7lae=gF7+`qbb*YHc{(XyDFS1*XeUqSv9 zYsoIsOr%YMJMU|aPF5K)kY{dKH58?V03r38?z{sUSYst+;Gsoc)liz2z`!at4;*D_ z1PWH1_er&@NK9^*X3Q1GIXjle>`r5a=unUcVllP-;^JJ%HCM;Vm|P7DafA+94{SU- zJ_yM$yynzgH5YR)!u$vb9vYy|tm;AN=Pu2{x%j0B_z?ia4}?^fB6F@cM`hSZ+UKKKbq~!Fh=@DWdqD-uV(bGsqTd` zcidY#MAbS2|Hv`}c>6VMnQ^q)J^mwcFXb~4`U;|b8T8sh?DeQ@2#cjgQ(f=)D!EcnzlP% zgqfcNdtJ6>!{N5GKc?ocE1inz{h`x8FFp6$@~4|1XZuotjUVdX#rDTezg)Ja&wtPT zSLr$#+c3n|?grwN>H|mdn!WN{RM?EVMf_>lw}Oq&pez^fEC1qGeBkYjOzhURnN>mH zTrtbp`}=?0^%lB>XWDP=pU$$29$Y!K-q;q+>?cg$T0TXeFX3vG|4sP!rXSU^fNk+R z0%c+-UvO=`u@e_7C~or^-6_*xvLU?bnRk$(uF{*_zjldADIf z>NBFlr2GoR)8dy-=c;$uV!t-O&)jg_x)4NZILr zvs#*=Jq64s@9>48{N75q|5F-zEmTXH+Rp)#w8Y&D7|jtm^2z8hzg(Of?5EoE7rHCK zKUi~9UN^I=%c!g;v>NVz%7b32 zf;SP`ZBwU@7wlee*KC*1&+IZ*H;8wTtS@b>ok}z{plk9KCX=JaY8z1j*}4z0MhbG? zRTHqy%Ew}F_#WE}HR0`cpA1@YjPg>}n1=#!Dy#GCABws6IEx;`SKh>HX;TgePL2eDm_SzjAuKRMpb+iKi!*lEk|gzSaEJIR1E757Q@PuW9=sv82~8L<8iRi0LX_MwxALW%8LJPA8bT6k_NYU~0af+(Gl|D07msUUW=Wcn#(OiPa5Pl}kmz!86X~jxqN*VcORMk#sTkt*aH;L_ z0SUKMs7RqbrsBl=)_xh!S3Ti0d#)6`$xY0doK6zwn4QxsH#R-Eki^dvd6FjbO2-Ue zIVFi3s8)Y}AgEXD89Gt0XDv9*C8@l@+EN04$QV07bUH9(-P$XOEe%XciHVHD{ku;d zw^O3}n{&a&kzR{R&GO9(avYg}K5zk;{W#1%AW@4K9Esf|-7n_6m=l){dr z^*puQh}$Vr{l+=#;a)8bPDD+uavE~X%rpeqL5-saS}ndvNxud*1<0!)QMm3xqxBuj zzu7nPAkC5W#Ba76y(ynE$0Qe5uk7+14WmS%tL>71fIm2N*!@^V2EVrKFP}PRvoT@! z6U*d62rp9Sb?#2bpkeMO%@eNG pzK!!q^ifwu-qjC7d#4lqWiCyshO7pDbRYO7f?s>wLK#M({U2_CUd{jj diff --git a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 index e6a6eab..f961434 100644 --- a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 +++ b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 @@ -44,17 +44,25 @@ act %------------------------------------------------------------------------ proc - TrafficLight(direction : CardinalDirection) = TL(direction, red); + TrafficLight(direction : CardinalDirection) = TL(direction, red, true); - TL(direction : CardinalDirection, colour : Colour) = - show(direction, colour). - (colour == red) - -> (changeDirection(nextDirection(direction)) . changeDirection(direction) . ChangeLight(direction, colour)) - <> ChangeLight(direction, colour) + 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) + + ; + + ChangeDirection(direction : CardinalDirection) = + changeDirection(nextDirection(direction)) . changeDirection(direction) ; ChangeLight(direction : CardinalDirection, colour : Colour) = - changeLight(nextColour(colour)) . TL(direction, nextColour(colour)) + changeLight(nextColour(colour)) . TL(direction, nextColour(colour), false) ; System =