From 5339a53824f6eb6d535f0e96bdf45df477871b1f Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 13 Aug 2013 13:35:57 +0200 Subject: [PATCH] model-checker : create mc directory in smpi examples and add new example for liveness verification of MPI programs --- examples/smpi/CMakeLists.txt | 26 ++++-- examples/smpi/mc/bugged1 | Bin 0 -> 66599 bytes examples/smpi/{mc_bugged1.c => mc/bugged1.c} | 6 +- examples/smpi/mc/bugged1_liveness | Bin 0 -> 67709 bytes examples/smpi/mc/bugged1_liveness.c | 89 +++++++++++++++++++ examples/smpi/mc/bugged2 | Bin 0 -> 66567 bytes examples/smpi/{mc_bugged2.c => mc/bugged2.c} | 0 examples/smpi/mc/hostfile_bugged1 | 3 + examples/smpi/mc/hostfile_bugged1_liveness | 3 + examples/smpi/mc/hostfile_bugged2 | 36 ++++++++ examples/smpi/mc/promela_bugged1_liveness | 11 +++ 11 files changed, 164 insertions(+), 10 deletions(-) create mode 100755 examples/smpi/mc/bugged1 rename examples/smpi/{mc_bugged1.c => mc/bugged1.c} (94%) create mode 100755 examples/smpi/mc/bugged1_liveness create mode 100644 examples/smpi/mc/bugged1_liveness.c create mode 100755 examples/smpi/mc/bugged2 rename examples/smpi/{mc_bugged2.c => mc/bugged2.c} (100%) create mode 100644 examples/smpi/mc/hostfile_bugged1 create mode 100644 examples/smpi/mc/hostfile_bugged1_liveness create mode 100644 examples/smpi/mc/hostfile_bugged2 create mode 100644 examples/smpi/mc/promela_bugged1_liveness diff --git a/examples/smpi/CMakeLists.txt b/examples/smpi/CMakeLists.txt index 669d3e3e60..154b3d585b 100644 --- a/examples/smpi/CMakeLists.txt +++ b/examples/smpi/CMakeLists.txt @@ -10,22 +10,29 @@ if(enable_smpi) set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}") include_directories("${CMAKE_HOME_DIRECTORY}/include/smpi") + file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/mc/") add_executable(bcbench bcbench.c) add_executable(mvmul mvmul.c) add_executable(smpi_traced tracing/smpi_traced.c) add_executable(smpi_traced_simple tracing/smpi_traced_simple.c) - add_executable(mc_bugged1 mc_bugged1.c) - add_executable(mc_bugged2 mc_bugged2.c) add_executable(smpi_replay replay/replay.c) - + + if(HAVE_MC) + add_executable(mc/bugged1 mc/bugged1.c) + add_executable(mc/bugged2 mc/bugged2.c) + add_executable(mc/bugged1_liveness mc/bugged1_liveness.c) + + target_link_libraries(mc/bugged1 simgrid) + target_link_libraries(mc/bugged2 simgrid) + target_link_libraries(mc/bugged1_liveness simgrid) + endif() + target_link_libraries(bcbench simgrid) target_link_libraries(mvmul simgrid) target_link_libraries(smpi_traced simgrid) target_link_libraries(smpi_traced_simple simgrid) - target_link_libraries(mc_bugged1 simgrid) - target_link_libraries(mc_bugged2 simgrid) target_link_libraries(smpi_replay simgrid) endif() @@ -43,18 +50,23 @@ set(xml_files ) set(examples_src ${examples_src} - ${CMAKE_CURRENT_SOURCE_DIR}/mc_bugged2.c - ${CMAKE_CURRENT_SOURCE_DIR}/mc_bugged1.c ${CMAKE_CURRENT_SOURCE_DIR}/mvmul.c ${CMAKE_CURRENT_SOURCE_DIR}/bcbench.c ${CMAKE_CURRENT_SOURCE_DIR}/replay/replay.c ${CMAKE_CURRENT_SOURCE_DIR}/tracing/smpi_traced.c ${CMAKE_CURRENT_SOURCE_DIR}/tracing/smpi_traced_simple.c + ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged2.c + ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1.c + ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1_liveness.c PARENT_SCOPE ) set(bin_files ${bin_files} ${CMAKE_CURRENT_SOURCE_DIR}/hostfile + ${CMAKE_CURRENT_SOURCE_DIR}/mc/promela_bugged1_liveness + ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1_liveness + ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1 + ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged2 PARENT_SCOPE ) set(txt_files diff --git a/examples/smpi/mc/bugged1 b/examples/smpi/mc/bugged1 new file mode 100755 index 0000000000000000000000000000000000000000..fa4c2ec8ace12a8fad3b91bea2870c61440f2999 GIT binary patch literal 66599 zcmeFad3+qjnKwQ?(n#`c0uBZnXv+s9Taq=S8{=a%8cBn7p&9w$NFz%lTUZy;$Onc1 zaUeL{NgyF)Ap}UswJ$lAO|r>C0t-1d*Cvp>*<_a`BntsH$C50&IsE&6pQ`Ha8I6p0 z_ubF${o@^5)m_!q)pb1e)N|ES*CaaIf|eC9zhGcXfU)n)-zG^a3s3os)La7rTN3yl>l#=pQCu%mH~PAi6~eDZU(I{09^YH8-&?Npo9m>mzqy+Bv2FZY zsh_V5ZbOXmZM+0pCG@V+7f9>wsaUy3ySaVBE?_G$QIm+^V5 z;a|S~{;!1Iv+2`tg zpVH-<{HFY`BLABJbq4R68hr-or=X^Gf8s&-;%yC@cO*m^aphLy}EqP2mU@O=}Q8y=ya8e z5cp+!WNh!$$PkfAZFQt3;5d87CdQrV?7&pkaRSZ-2b{jl-jV5SW-2~9Fg=}_4minl zmot=^(#h$r_~^uVCOxocG^3sseA3mMbduvE*#K`+neidHX&V_I7#+DXBayz$-~qXb zPmGN@(@dTon;gO2*v#laHZ$am4UCLCUY4nW@%<{+)79nd?CI-lm1wd%&9;rPRSmow z+&eWexsTC$MrXzkj*Ls28@(vetE14Xqz;WLOpE+eS>8sNcQU(gDl;JO)=0_f8<|6B z+2l-iIxsmkGM*hqKk~D>A6e~ylNlPw4&cF_>1maYBy_{ZeG_Aujbj5-BNO8r_l{&Y z>LDTaH^mH2&p5*)<0I(b9=tn*UYMEA4B;`$G^MFeGB2`b1MQv3mbeqGj-t`>Q}7T3 zo-~kQAOQdZ49$P$ntva|qoq3g%$Xxt0)l~mWOn>+eA8ueC9WneHa`Q;Tu=P?+RR`7 zI>UD!*5wd~>!O()c*K|PuleVE>3+K7abLQB{rIXco!>CO@A%TqoaeJ2`qH@un%{H2 zbgqHs_o6S|zn1;Vm+oIgUiYPQZ8g7+qpy^`_qqj@Q4f%nlr1`*ws& z&e?`L#`iJ9OV1t0Z|#+gv+G{^j>M-JXP3S7xWq4KoI~`|BNE@kIMLQiAC&k-jI%3W zx?SRZjI#@0x>n*BFwU-fX;R`XjI+yLx=iBdF+Pv+UWrE;CrRPFxuX@wTrynP#>UjFgM2HMT_oh%Y123~v~(VG&lT>toz>#sxn zu|DSc5)z+I{DB!>?&`Ry{%V$c)3O_+_{3`+w{)S?7OqJi`*rMdttjgA&)|i>W)<0l zZ%dJ{9ee7raTF#U^5VrvJDT`|#k#y`ZA$#%nul*nFw2c@mL_C*Io5I0q9y8U%hlIj zNgn%J>~rf;_UBn2_bdPY2dOxUc%NIuZ;|%mB+8MGe(ebtWd8MuVg9O@obz@Tf@+Sg z`C;d=p*7ES+*0-4pdIMEW$lf;ApOP8W7##o>O6MUn%6syU9twy_exV|#m{2L{+K-W zyN)mau_$@$2QQ}ZrH<=g&9036J;%TE*ne~$`(5j?U&fA~_T!GDPgotzFHilVlIjPhX2$L8zL9Bra%ut#+?aiEB)iYf92ywRjvlt7OdiZ|$+p8)_4EXZ7P?Q~{3YX`cJbzpDCp2`enMh;|#?BS`2F?;RM`~Xr8ID2M>hwaT0M*&&f z*x3o2E3jRI8E&m8+7w2$h)jllfBbkWt~D5gQCuGcaNLaRXK{THSF;vaSM~+0Lrbj{ z3rovx2i&Z|Gt%hG@&4nu1{N=ETfF>&B?}IgT^rbX=BD+vYs#6-JS_i<=zgKCVvCpF z5R5M>DH^s=l$1Y&=S%TD|9Zjlufks$(vRU9xbWuC4JFRvZEZ(OZwua9bW1T4|L^%d zvS6E3=5~EGHRBZHFaP=zmF%Yfb6)&+dGU}gz?8EhFTO4>9?6T7Cg5+0x&&^}@r62W z=u@*68v2twr2K#x`6F-19~Tn-%vxBcpL4wVGtbR1T^8Ji)Ii|3e>y(FYq)3|FRl#Y zvJw^N0>bdTn5;Ouuj7xm0Cy`QcxcZIcv} z{;-alc68|c^YqnxAK)qNxl!lGf+2DJxxlYmlcWZHZPV8s z`Z}zy2lVv@eZ5OxKdi5h>g!Ybn*W{lc>Fv&+?v@lGB9q}RX0{gtLiJ%O(5?Xo>tZJ z8E!-#qsFXEip=NB^1t&8GVA=-E&#K2S5qJ`0VpspwlCV2^G>j=^ezB(&?+1IFfPH; z3$DbaxU>V1AGAtd1w|DMh8})5$m8M=*n>c@Ec9J)zj*Iy3~F&1B?!p)8Zs7_9YrL> zl;W~Urk54pa33$B`!0mM>y#t7zwaaR_>%}rd&8(<+0x+suOT*XcM6X`bTQvs9hmot zT3jDcvEq3HI}v+O#meT5UxL^}Dz-3C@*yw@!4H21FP3~`2Dh)zmzpg_So#~(!z#T1 zePWedim>SQbLHWi`S8JNCjSM(qJQ5a$yEqT{s|Q+`h5>>=ihP`WM@S|D~MMY9C{Gx zMRJcCF8KMqh!*Q;*@AyZ4-|!Tbm@X0-GXR|b+t5S`GVi~B3i1W_JVnDMzqXQO$aae z0vc2_Pe&^k{2fqy(R>}PSul`Bbb+-J6$-9yS}?K$(S=s6M7J$?A&KZBow*}W@>ACS z4~tOY;xe`YBee!Yve2qN1+85y84E#!^(nlv=upWs6@0CN!~2mW;Ufql>pC@Z=PZc<_#Gfu*;j@ZcjK zK-999E~-N0_s3PF4SiR9V=J0qfu%deTD$nv1x1TjEI!40leM(u?iS$2;F`dK1zV7c z>grp}lj0>vO`Zx+To>S_aM%k&>f(1;qkY(N?H%rrejQgop z(PDWT;?o8CX()LrpDwJnwk}j9p1Ux4D(kbYI59OunUH!got@dkJXl-hmV$8|8^Sxd2MlKq zPfDpMNN(}AE*CvxzV5U;gA?P!BdjATb8v9qz?8a$pk-i+$ta3Kmk9`1#t=nuXo-WF zI|{*=N^l#S9T{U4QDJ?DGW8wb%Zz3Q`3j!9_e>wzJDo8_jZ6~-H6-CfvGW*JeiSNA=L#Y z-p_!2Q<+g&XJXpX;zRYm8{s&hX+y~ByJZK=WGBW3vJ>o8l&8d)atm}DG%HZiV(X={ z-Fxr5zwBt)(WCe6zW`#G38$^wW;C#?CGEuHeaUn(9_tJbR#sP6SJ;x++0%}=&GukoJCJuyOpRm@ zJA(*E0ArQ5D|4F6u!}x>`t^gjvb*Sv#q7gro>saTPo2> zrCTMlO(?)b4x~H!dUoQ22P$mG+}j5#rIrSCb5e=EWUP}Jk!n}T zXHrggPhX<9GZs(S4R!clYa$+rHaUsjRI;@w*(#{nJc#L_)o$+)vK-Vy6_(oSbj ze7n=umq^&rK+A6QaZg`sqR&RhxDjE@yJEYXWOrK+dau)t)UapxDW@%#;`jI%Rc)%P zYiO*it7)ultZA;Vk2FN;`#XU@uFSB<@D7^Pt^)N&b2M68+Ze5>ZD^{mYiz7mzmfo3rsjp)~1!PzJPF)%ra z$)A~Wre`N*1EZOSy6nWh@SzGDfA09D;yw6EZ(mP5kxJQSRC7|%G(B*-UDeHR^h-2E z>gq7AV*~pEO9#SZ1D98hjf_{=SRtXoH~@WuJh0`7%}4CO-iA5_jS#jEj%EhNXC@u$ zG>l#(>L_ zl{Zu>5ijpZ^rezAx5|Z4D-WcSUG06zR)L<*ct;|>9n-ag-39fu164&|tZz3pPEKn} zrvQ7T#!2kz#kXr~nvkrPNMDVmmkta7eL#E#z18^4prfM#yt)o-S-ZpGXsAQB2|y>Y z0LHc>vCFREL?fujd%Ai%6T8r#vjCrUO2jz@lNwtz*SEGIbvy%|l;gA|I}>b(%xkB& zwbw~>w9hX~)d0 zLFmBtPD~vpP!JX4?HxL^v}ZUwb(rHi3>hI{RDmZjNRz=;8dH(N35;W|r$+Vw_wEhE zfin`$jxM|A5FteR1kJ*dkPZ)FqB7WMJ5G07E0B2#lZ2lqu2k5U!^jkjWZX%`W8H1x z;R&pbS!ZPEP$g(6UV*=zfh`HXCB>Gt7o|%!+Ec9XKxvetTI!9nEQvyzioF=r?D#?tW)Vo2%JRI)v+ zs6P(F&crT223Cvylu6ZK)t%VcP26{=PGC#cwVClf6Ej#OhB$57Vmo^JoR(B8?mYk* zpBNbjZ~{_Lx|a-C0kC)v(Q>uucEom|y}P^PGLvI{2`ARw>ZEqYdYuSR04H^#ug~d= zb#J#D@lL$A-?=E!*W;kRnJf`(<=`Zgs##2%p$UA`0M=M$45@ZlKdrRSy`<*cN?X5F zvB^HT5A)3q*RUpnayxo}8a0*U5;S-?jp9Ka4uJ}E(JqqPI@1QTR7V=?>zeCo>uZ{# z(P&d+eNAI?W2UOMsVxAIQz(R!MMdJ_0&6=ugwRQ%;bikWPHz}9ZMuTBsH zzLey;7KqYX}jj&)(^(|yVAc1<@4BI3G|?Cu1`iLdaJJ#B5AuQFp%OzOgZP>!6w zzUK9JWA$#uQy<6?;%3IFa0fxlQ63r?8k))-#Np{Zqx%QPvpK0)W5B}YqvUo+U=`RN zQ${ML5e9}$Ew)^rcCoKI6VhA6t!Xl5 zCo8J9V0j1YX0Nlk_HizNF6pkYS8cWdx-O;Z0S%K7i-!x*oa_foSyZC0HQCmNUgbb0 zc40tvx5jqU=FE<3*{pAQZ7Q(3?o7669BnWMy5CDAyzh*Ghd^~~lLKETtsVnr?{2k8 z9;8V3!UROK4}#r^j?H9H6trDv%5+u)rbjcGNfM>X;6%qztc#~mP7|jobZKB72nGH8 zqNaZH7ZPQA(c72kOI+xYog51F#IesmA3R2dy#Z}iNhlj=(6P5{#+ZRpt?;shNtxo4 z8gg2CdcYu{2A#=t8X%&m4LcI8C3n-;ne6g_Tq@~y3m+$1lYNPJI!q#?5-P&%L?!f# z1DO3xq0$g~J;49;7$+|X%TyO9m>piNvY{SnnZ1I$Tb+1kUwEhz=#a2>U}A&>1Br(e z8NU=p3{NiB)PxO6;!=CvX8Wy7=!&JbGezc0+#bKed()MI7ka2V#m&}g9jHBSe?&!vjIub`n`M7|{)7+GL)kAC2hp)Y`N zJF6o2JjqG50;L36Nw()C2))O`!!9dLPTJ6RE*m{EK0J}fLM!qt-jVFYf|f|9ldUAw zK)CXUmXqHg4N3%u=fobweY(e_Rc$?eX)Jxfl3bykWII`6wvebr@qqFeYU5f^$gp<|_M6^*87RerTLzC(Sc7vkP zbGZ5jkm+nhPk&lJ4$E(av|r52!W(3MVy61`!z(S}Q7hdgsM zj5LKEVFaDYRJy{}Hv$yNlnf0738*ajFH{szrJxrRtTx)%(3mqssGX8kRDlFgxn(s6 z_E8c5bO6>sa-GA2`xH(`LV@LnAL2W+Db%(U;3Y2T-CYj*eaoTHB)*=kh5)3dIobq) zLrr5-BwEj2&r~&%2{Ifqcw%qSv}NiDiLCf0pv`EcuCcDEwxO<(Go~*g(j2?BM~ihF z;d5ZqFb|zLWBZHmyAg+&SlC; zpj?lcM^j~;?uezF3;UA*j&5P`2pWgN1C@JZtsSVax7gu56&3bYJB$bvmWbe8zfd3m zLN#S5AmM?P;KdmjJvac#vZ8#AGzPdhCpm{U5po!|nj^y_gRm1(1PV(}CqWb`QcKo$ z84H&abfs3p3v!a8j}z^QzJly;JGm>60%WuG9a>~ovZ$Vqm@*xpxrv+j!_0JfTnPSR z{UCGmSzPiDBZICiu^@vB0mZ<~C{`Db2GvB`W_z8a`T1Z1gipSNen-PxUQN%S!ZI`| zt95rbgmxGc0M{N3T$o%UYl$?7tcBA2sp*+L9P>)3Eu?Z_8IIUt9jn@sJ>Y=WhrJA7 zz>QTA7EEkYZf>#$zU&h9@-w>09vQ}H`#&MM&IkF1Z&y|2Jdzi3QY7<+&7_d|+hkvj ze;)7R8XAdNsUKQ})W8}P-wyGOi!M@{@)0bD?BL*l<4BeG7Gfps2v=b(hV_w@0Rd2V zPr9cYg2%qtPFqQ0@QPg%C2mxtJ?1Lz{WPf`hq=J3*lozz56Oq!k#@n{FYr(-M^Bs6 z+e26eMxnWT#DCKlT>VCQbnT@Wx0F>lR=Plce*2tbu5pkmG6vC zKwC3$kOlRjHt5njjps1s4o6gTODxt>uN zx&pE(yf=c;I-n%N`WCeSEay@NZK;;d?Q^f~B!^mJ@$Dc7!QN}gMmcPb1HsbJ$nY>) zwT~0f5M*2mlA5?#lYfcR(vksU!8tj!5LglujvC zpR8wGa8^kofZlzBHmDc}k6PwZ;w>at04Ts0HVjhAi5ct*slYA-5RHwsP4!K=6kZje!s#Y2}Lu~}PCb{ushrPn>h~@&TmSj!ElZozhvMq^4gF;1g8X!vvF3@4k z`HG=LZBtz z16@E62zk^xFAeGqqTUmh79m&_&ckvAubXdV##tOIrqp$Kh}Q|e5zHD#^U1D^QD(-MHO0fLKngr%876X++fGqN00xnufN z%`t!FG1m$=yI@BbeE*2*jsJfC|EEUaYUyZu6_5i*wg4;V2bc=`s;jVQh{UL1A642) zmT0gdmc%l=6Eocj1UC`ar@2Q*% zJab7nEMBP;kO)|)%aLmnnY2r7C~FgJZHPM~(+;*pU|&NR zvuk>MdrD8~pOrtK^T-V&t7;UcaS8E~GPLgOqy)}oZpC&~E6<*65hz<{A zruIxsXYwR)J{ATrt3sxmV=2FjmI zNm!*+pdd1J$`*=msdVhroSM#tMetp@&Sb8zHwg*l%SWXz6gIti{#5>mh9b_KOaXHn-Ih}HCZs)LjjktXI#5?@Y-hleVMhcGH&vt<@Zs?B6ur{nXk zRShIWfO#V#Gh)UFW!aoPu3QuiplOYfi>k-M+|UAn9m!Uaf|`P5BRO;1iwe0YLq0N2 z8lEGlN8BA}^#qKZlO@&89JUPKY-u~yPr%mh1DW`-R4>%3Y07!Ycjfjt?9L3mj%q2o z9b22ZWt)H8nyjc%!Jk-@P>Mn#q{PJ*kk&7vT>?YY?uhLz)@yy$1h!IqkQnXLst<^Y z_>+Y~tm{&+w9_UY1~+R6z{=_NI5`A?f)gvy6?jlCbOM`#C>8=jI0~oOw65Snr4XPj zR^S5E*lWeSU!Da(#KZPoyPQ}{(wI(h;f%^B`nwYl&36JCxem}|D49xh$G{!7hCx$y zD?OgF!US~A%CsYF(qJv5@>f(s&!^wOr>Sg(P6q1cR-<4AmJ9o&XCm7+)*kDyEHw^O zcM0lx%N7Z#Lv}mb=;ma$VK&2p4WIz?D|NvarDwFXN11p!Sc!-%xa3 zKR$7AoVM0L!FElhUEZc8WKi0G>>i=j{unkSW`@curJaV~Cl-N?SvSZZ+6KfaukT8v zkP3}oJJ=%FBcRdz9#IMf0j?y*J4K5C9aej1PYbP5*-4&tWA2FOB3Mv+7&MGH zFY04CL|vS#LJXvzvbz)5?nDVAqZ^7CdG#aAllGOHO@6HrRL~l2$6zXcrgpq&{ zP;1S`#B|&l7#{-PMJsZTT-@WCpc=_OK$F&}x=V~J3DvJ8xk2If^mWMqXp>;pN!=2> z1yP8UM~iKsn-q*D50JGzkrqP~DuD5X14l$4k~=V|Q851~MixC=FMiVOw$504Dheh) ztr!y^0aj8zB>_sZb5hWGTA7ruMN)BjKh@u2?8Hz_jWKpOV$=f^;lmI0q)+CI!Z5XnnYRaCB%BHgivIvZ>qFl7B3+y-xJMdw1{EwKg1iv$cxE3`;frf7 zl_Ft72fNjBkeRuX!kw7@kmPmu1LM~m;^zDS8LSwQTEm1CJV$=KGda z)RmJDW>X|<5i77@G1+vh@Du7IjLw^uWb0M8X6h` z*wxVm1sGD>Y~MXT)b3aDxu*R@cB0}_6H<&WnAzLwpeSac#q>@G8f}1cRB|%*fs!fc z1uIv0?upM_vn@>`P}e#=3Ds!s=hCu#)4mgGcy7#)EfYdQ3cCqU2*PzjnBUnZXq)0{ zT4w;2i&VgXNse~U6?`b+b(I?zI=u>nj!S|8Zo6qkCD_sxG%C!i|XnIoBwwFjt65}QZPin^L+k}jHaF*bpy96%|~s#Ij*uDq6+P z!2>1wQ<7W7Hxp7>2*kFoBub%5rjYTK*F51K3X=}<{>%R3(4E`Q$p>IG|73VGu8rX6$UJA$z66i@OjoLmr+lFe4bJ3o-lk`JmE|a z3}@6@v*&Wq)Q6xKK3R^x5@>`nfvpVX-IL|_VbbEhLUF+y(gTy{|Kx{6G@yl(nv-)y zmA1@JurltF;_@=W;ke0M_X-)5Vh+KQOYPmlg1|)-7{H(Cp#gV62LxuaN+KewvtHl4 z6(55F%3o*kk(ja=XucKTM_XEhAu$m(Nok;!nq^E_Sny#34JN%`WWcKUHF@AiB1&gx z%k=U;^J)3)au~f;+N-JZ^O^q|)@|;!)}uXpW68d7N3ycBr^4>+skA$i(DZ^Uk;MX5 zelUZFu)K??w!roP;V=cRD`1n%)xQRYEMO;LTzhicq_9nUqqpT43==kaL}3NnBy&dW zEwHU@x4WmY)5(raLhXlrP=e|VDR1`qp`N51M6?5w3lIx5Yb6EbZ4ChI5Xt*&EHoD@ zmI#mt@-<)}6+Pc>ve%0VEOUuXnAl?r?X2=>vkNlVcoW|fQ*E`X(}Dpt!ZsYjEDMJ5 zEM7yJvYl0lPE3(=H z1$G{y27sV8S?+7!p(rj*=fj`}@CD5W_cToo4DP2Q!rf%zOSi+MXt_f%XJ4$cBrxl{ zUfb(MY5|heFgW!!4XA*yLux#L#qyDb*7)b+2`?Ee9PI$?@|f5LK(9twi*h~Xp$tu- zaW$10KHG|)BBY!N4v9J7l(M5hA%u{FCg#G@v9zq;%D7qUdz5K7+bz2Q&~jo|y;sX6 zp(ylMQfZME0;aehMK~N|_YaOtyi8JHAP>l6$@j1^jrR83OM>A6it9|YK|4ePT^|{2 zOw0U)uuu%(HwABM@xY0+TY3eG#bIO$8*NYOhmBOEUd50SfSzkhS&7Z)kb+f0n-9^k zrY{}7GCQlS^V*VmlbhQVo?EhNF3b#eVmEjqrR`C$-+lj}&mcv%ny_D5uv0)bAA&zY zl+H4#g_Ug$+>qi+hVeB-dcgj~Y1|Gr1y#U73_J@1q(BS?D_Vx<+3O(+^f6AtH|G_H zuV@>?l+z3LCIzEHZR|LT%}3oS=p)jtXrveL70TWTxucEEq!xXL4dPtQ9euuJ>{1 zIqW*uH1qb%xbg7{>Du^UW>lDebxTiin(TKAM(0X4X9@xwZ0eKcOr-!FBDe3OXo1mm z=Wr`KVXj4+HNBHl_BLx{D?ObQQ$yGXt=9%(j(SZPvcMpq0JGvUAK)?sLTM zr%`;C_o3+lsJe46KM#QyC>F>00iAOxduLLt!#;> zkVNh0bhRk05Dm6LL)eDhJgF`Kt=iOr1vlLZu`WevFc{ZMD%V{sPr!Y$he)t_N>*h` z=(W%k#D`+XL1luHlUbchtlMF4>0^b3sdI!OZb`I*!WV^rSou-2FY`zXTt(Wk6UA!! zgGL{Pbv&$*wgLkDDf1r}RZ+7eGy=CA=Mbbm^WVXV$-{+=e-)XQzjvk0;a+X@juOeD z71+zdIPitY6}*&gu34U$9){G5xb#g=uN~pa$uScXhk6W-%pq!;DBn1MU1B2>d1iq| zgyHF;M7adV9I`2tMmXNa^~?b*O%M=>6gP7Ka7}S;=0G({Cm_pLNHptYqnjc*Eya0{ zxVN1eFPS)MW%fPPsv(ns%`j>fFBf+ech8JT32H^hGtM*hbygL3m^><;+lfR~eq^Nx z9Q2=vQXsUQ*qg;c4T9t9~4_K!$CMn12HTKShV^($v3z+l1oIy zk`q%I(qfezfX!yYGAYpq12sr5gy3+EjtmFnGdY?I;DiL$6ebBMHRZ6N?1W{UN2urS zwB%Z3%z^TpFc7G)C)YR4u>OkOC9s5_5~Ij4Om%TC9VUhmk}OkGYe%%2L^V6&nFW*4GmXZy)eWGwIoCjhZkUU|;G z%;;oh$|${onpC-p?xj`OfsyGE`jw|$oNT+$)?s7tB%&T+D(`PngoP_Ka=97+RgN$q z3?h}>(h=K{eS`2;VHhB)H4GIoLM|PdV08yxn>#HumvnUnlSpOK2aPat?t(`~4(v83 zx7x(%?W5$vf_e(0BaCgpX-i!6w4?C?BBha>(y2wT;3a*uUj-*8{H>%{)VwD{^p*=QAC`8p# zx(%+H!w;uK{g9wic+2R8{fT}R^KD`PF^wJk_Uvs7>H+$F)N`;yeXye9Wuw4sDxU1S zt5p(pk}K$ODR&l8P@}?OH3AdQjE?4ies+@EUP)U3xIGtAe#8k60i9uP8LAu^$LRwK z^(pJBX~oMb^9icJ!>c7DC|TsBC`xU0SJ`NaRv^=PIhnwV%+3VyF3a`fS8V7;Lu3=8 zyNYOXZ+B`(3SNVR-V=WyehLpF4zuKFCb$n073v~tNiL!bw7(hfR?0A;RkjB!lOL#< zw5uX8K_U+^JD?+KGhaiUUpuB%{(9Po<(7admM9QYibXWA@0x=YvRhOunTTdZ1X(YO z6%=ASQ3=taC}|@p7wv*UT|{dSQuWw)cY09*hdh{af=<4|7zgf zO@k;;G_GCX?b&#BU`Tsk57aY)`!q5HIi#_+VZGEY2OEwL$)Vbp@7bgViUMo3kAwm` zPE2>W3yU&I@d)Rj%s%?N;mr-6${?$$34js;GKcQzKqbslJ>EViU66Q7Pa3KQ+lU~m zBA~)ago=Jg83Ke43`|uHk7P#02a`4zSQo}SaQss(59|u4J&Yy6I(eX{UJ6quPHh&5 zd!u}{1yYnx6yO08!iv-veQwuvixD;!M0fk`bjZYhCQvgt?&dSVKYgdhy6}9Fr`2(+_Rph;A2CWrBq@o{GdGt zQtD<_hNw&@(SFH}HF3M)X~gs{wtV4kF1N?2-qjT&G3Gd9aP~>x8dPziMMg=0)nW%+ zOo~E5&C&Ig^$VdUf@vC=pl7v_Nuh3~#i={@fgr`$8v4`!o(U24!SHP3vbJEhwfi`9 zpigKGDL9xkKZ${%nHV3R0nGr4d0-4i+p}pVodaW_^N@Bi<{B;l14nCjkltv39M!rf zwppnsku+P-o<9~wL27H^5y<^+Ejto}U{t_!sfmgik9;|9a>T`;@;#$`+tG?f*)bWp zFVL+>eYLkcB2@8sB|a6DrHLYEFscwpDr!b-k^`+tNKvpcFO^C{p)cU8^eW++%JTHS zjGY{toPhr-?1{8nu_>uTy2lP5hKI3%y>Ky7QOl|f%0mKNKQ{~)=PQ7Fo3|41YMnHToLJpLp zi9wNXtECvvcc|4syO3nV^bXWWHC(ARG{XqCuBicz`05*Lnj-a?4SENvV_c$ma*kXZ zr2xG_Be4k0+zDYC@&uynkqHDSx#SKB=W58z=>pORtF1+a~79R?W476G+o0qd5# znJ8QZ?||qrA{pbx?WE1tA*m6AInPf6XSb(X1?mTdF^PlD2n6{I>=76Ys>9wqBrd=Q z%_V1}Y~nuzj+=61Zxs=B_5kE&&|V-D#8b#G@-_7__c@7fW^fI8w3n%J$!D*<0w#wv zPMi{ZM7aD#gjR@BD5P`_WQR(@?d{A|o8>8K?Sz<|TiS-~Wk z;RADK;ki99Q;=L-QIz{flS;Fu!qtI*3x>uoMuHGj=#e9c8 zu99uLp%%t|%Ydx8vlQw=fy~}mFTmM`1%lff{4)AnwHWoF@I42lY{)=&8;BOY8zKqw z+T2p@YO>EFuAp}n$$PcW_X{`W`Y8rTs7A8kbpUHE+NZB?OmMvG{|28|V~8_QfPh_L zztJU(-=Ga$4BzN5$JL!GxJ|7gcr+KQrKm^U`8kB8`!%jo1q|pQctLN%gbv@^uS{`; z&{33VAu=qV*Mu4|)(7bW3}#)elQPxER*BYDz=X0hfN)9^zxb3V`1d>!B%0}nOwkOj ziF8c3YRW*AOH}=&P17>i_X9ncEAi6Q8Avp>qywn24EA^Rx-vY!nFWCw&#A_ey(rAY^xK0D;f8++o+LarGWYyhA!WIi9GlNIz+?xhqRTz8@VrAAS)kK99| zJCw*CYbbS$%4MGRnWrCveC&sVLX3kN24Vj(mEoeK9Tu3Ka0@E!)jl}`23>H7wHp(? zK^@!*+@U70QfOJHkozL;EC^?+rW(yi&DpQH9azKTL?JgB+^0N^lUrm87DFW2N`L}; z@!bWX&=8Oc*yo&Fn500FaMkESvTO5AtP$sSm6O`fQNU}Vsj$yT#I!{`;^Y~M90X#? z6tEOg>BdxKs|^oi5JI?yA`m~iSb?he$? zq%6=s7*aYq_>(ujUr8GOe7H9 zq%6q8aK@BtH-Xk^lQmXamkoMACAzusF+S%vjm`n?i`2ekk>KJfrn;Ot0(lsSWGx(X z94#KhcG10JV`Dz&mW}E`NujHybJL2)(1d$&T8J11jqK0h6he@0xu3?+9Pt`Emp#a= zP9ifq+sNcxsB;A}4nbbfKkPq!YUKN@j^OIl8Gzj;DD> z1`O@7ck`kI?fx+()~jotDUCkZYm0~CCIxu1LHEB3$?|dz9J_P}*d-1dOm|%SUq_sF^%vBuc@iZtUG>{I zyS4zz*^J*T9%Df3nY@=}XKyY=j%nkY#vUB|O_FkCYa)*Ei`JCD6)l2aD{s~H(T_Xf zny|~Sq4iUD%61m?E<9$(Fn#HN00^15YWNVf$iiUr8Ml$sH9@7#=lGt;8AL+w)3o}1 zJ_lMaXo*6OlIn2THuOAkS*#zL3TWiIl~#=VGrQrrxWZn2NRGCeqD1dM>kJbHEdMEI zm|lKpYv*)^33f-Dd~%uDup!3-<{UmTtK4_;jeC?N-{3o;=Rp7GxVBImqr;$Grlu=} zCGmN{FmxZI7XJ;g7Uh5i#aeJ$ zaL``URB5k0cml~5rCfu9+#Tx^aOGPlLIjKHNU^=UB0~;N2V*d8?&;p$MK4ya&oOWF zpqMC#d|04Bv0cUkw^o*VxIuUuW1{7w0n{D`bIMkl;uB>)540c*STFb``Uw(lM$ink zkMOf6h{uO=jI;S%Z+y1Op}fym+RD>B##`2bS$p|qwS`4G*0^TYE6uyF;X`Lm2 z727$GVvr_!$3DU6j*d{V#hUMOWz`xaw1&D}+1&xBP-@b8eiO|^5*Pf8%m!qV9&S1gYL)Umk_ctBZ7egK!DO0G=NbzYJvcC?a1>Daht_zd&%gkff-^@+z$ zw8-j}i$ml}$a#7WdK8WE4(q}E5Yv8cqm~|me@H;&1rU_T=1L{|fGBfDISV#UDh&$< z_fM3qiJcMsfO2rPhJi+m5J+GU_0a^PROjbC5elhDHTvo$r4*92$R}=qOiU{?#MXHh zslf7bHF4q@RMD3nz8ywV@2tei4MCu?d| zhgd|d=R$@m2N!DBRHVADCK7FKs%xmLjn*|q8f$RWTr^WvS1*2mOu-bg=Nov!j@n=k zbEuFgkaqYS3AsL%+*2dS51rt+2%FE{!y@#7B|aGnod{uM60K%KF7Sf88<+Q@z$5#> zf%ADN8k`s#gT)?%mlIQHjG)0hcOT%o@|>@0w;DO@7}l`7jQXS)?BGxim|Yg77Ag9A%tVgTH0 zC^s5&!=9&2QHWFoWu~X$fMsk9z%@F|4TG-C0l*A)Kt~B5pb^55^{A6wX-k0|$_@Z~ z+L&7;8NCUJ>tQ`Pi~RtUX^w>JQ~?7~B1++K61(D^zy~|Tlt+{rJhqeSHPLyHyYhJk z08U%)sj);Lm7l}id?SSwQs3D)h!kWUHFU100Ms(xXNOAcQ+5|9x$*(B?Ji7;VKoBdQBOg~QmCz}8Q_D6zDFhs2Nz){7 zTWh|jKBNzL!3xPb&>&9v*ubf(aCv7yQ``$-*O7MbqkvS#15m0gEO5|F19pL<9?QZSU4aPQZ=zYwv4NWFq+PA}H@%Nu)F-9+ zpimAT*`4Z&#rvQRC5CaOManBK-iA)aXZ2~+GCEzs2t`$IwAtFjljaVFdFE6mKNmA= zE14FyxdJ#>zoO)Q6pdC89&<%;mGI9(&|$xc4-Vs02ec0rGWqjG45{^g8QKlm0=z<0 zrUfS!7CMs08Gi2O~ z%Uq-BDoXJrQ77Dr2I5^AGU|gCq?KZv;z_X~#GVatBB0Bq((zSep04!gikHs85G2H9 zqp)ZGo4aoqO9~Bv!FMVBW z*NIG;D*CXS22MmdiJ;SM^#U>?QN-7nHW(_}B!N40?UQ&f5A@mKepk&n%@chg3nK*a za;`Q?(9q?=8M5dkdQ#;{aru5!k(TF0)o3kTG^RE@C{MB=G;kdG8%W#4jAFK7=Lw~4 z1>XT4_sisJX``V<0)Br0=)J=96_y6{fZn+R#6qm8T}@&k>2|W=?n<7fU13f;7d{S; z;Q6&1f5P|qC=_8c=(d`&a(Ph@p7P=(N*@=QL#yjkloXW9xvE4htfP1i)pf;7YFZn* zM&_ZSZmHPJrEKYic?R%3+YPhiC4H-otKBRa)wv!%2Z*wl*R8u!TU>x+dU6c`a?_0h zPIi3(SPC34RlplUu5SaC!P`JqxEL-fN(ef~l81Fop9oET9tTV`a)1@z;1yQcamH&g zLl;iSO2Qo{_q33WGYbHbPTuY(Er@e>^&b zldZ@pqO48151HhQX2wwqco(k;)6D`}W{$^&nKE>vGRe55xsP%Grhd?@sxJVt31 zm4pj(WDesCqiqqBuR^|Wf!I8cxO1>Q5Y-NV1)Ds~!!P|E;!jq@FRWe69&I{`b=`B! zUT5cY5=#*D7I|v0MH`W8Pmd)+rOT7MK*lMX7yUYV#&eiWKep&JoWEzxnDQ)M z6(+`)Y|`T}@#j}%f%MKYL5ey1ZlGcdR61L6;@Np}<{da&Qa2OBLj#A^IX{9-bCc09 z*>Q*dj^(;f1ChkK7)$Kl3TM=qNNiv@kc6)+~}9PNhmN(%w9 z&&wtqFrmFVg=-UCaOC#Co@;=x*<6v3pPuy72@f>XRSq=N;xCH72>xm+2kM*g*Mz@D z{59aO9)HMJk9_sWSC4%4$XADab;wtTe09iIhkSL&SBHFc$XADab;wtXe6`3|i+r`n zSBreL$XAPewa8bCe6`3IMZPHVMUgLxd{N|!B3~5wqR1CTz9{lVkS~IK5#);?Uj+Fg z$QMDr2=YacFM@o?hFr*mJggeNf&%cYvRiFN>=sbOkw-Me0)0Dqq}>4spO&$?UM z#8^zkn=TnFZ?)ifX6*)<7Fq!ZJ3=_;ffl-A?L7VGP+P1ePVNF!bF44cm4e|Tj<1#Z z*lX_9Bn0EribE;5K~xF)l&rJ1y0#%2fp6rx+DHUvT;k~MhG+w1opM0C52@seda)qD z#9Z%8QYE>T=5^K0bu|t34R!TRb&+UYLw#Lcq>-n1N9%ajQM(qJraSt(w=1di@H7l^ z^A3+DTRB9h@7mX2n2}25`@a&qgeuj3c|3&?r<_nAzWdc-1oEOjCqSP@z@&=V#}W8* zQWRC-JOVKirr9mNiu2~lePM@7c%4)LB$8WG{lUD02}F7CoweC0>$W%wJ~5YD*hR4L zOSG_>DyTe!)l-h{5L`Q!BUxmzII3-9#`%)kAT%_R@d*_)&n*(=J~%}8POL;L(N^Ko zT{azQxlEDjjC}8t`fPaLmK#~Be0zG0NJnAyg3FeCnamkPc0Pw3CK(P6blt@m7#2q~ z&&{nJAYVvD->I=mu8s%Bg^>ui!XQE6ib0FGybUtMf>Oesq2W;wftX7qOnCOU_@&6x zveBu9*0K>sWa@F+%s#}11EkJl;~jbj9|A2Q#3CoGoGsuXhlAoU)VB@K^&hHEvSC#1 z#G@A`@h+iUDG{@~d$xte)ZUgnJ)p3|z%uS>@@BQb79h$}6SBDg+e@P)bC+Nt3&9!04rgdA#ESQ(uU%nad5XNL9{Mk^GfvgbJ?dRi_JWwNK2g;z5;Eug9w zI~rj#2fYX{l>bBNpsi#K(X7Q{G+#4gsZ_jho~N~$U402fm~sxaCR+O2-#{QTl!4>P zS+k2ruah<~UF1JfnI(55;I|)efzv@LNJm9|r+9eQp)DXY3a1`m9<16Wi+LPUr#%6FW+l5ju3EO7@e7If!aOwkGI1*IN6+C(XBs6SS3+$mbsV+u$T9sSgH*lxKuc@4dkV8xLCK1DS znk}R_@MH(4`5fu!DOEjj;z-75E=P`hrkpu~##WoIHOeqz6I!n0lrA{x&P6106e2$4 zc|nK?DbJ)-7dtiz;s%E~Vgr-d2-xI>1Y_xRoF2mmcmd~vD-n!`KGj%LB&yb%InBcj zvd;0tCXO9sHvvF7qPAAGiKa*CF^uMiikSiubCFoM(CCRP=b)r<*j}D9hP+p>RH2o5 z{4tH%=^RAOc)%(5i8t8-1~{EeW&q`Dc$0Gq?uY1GPL>^S&U$RHD+6&qr0iYkOH8Pr z!{a!Q46gKYr6Ryf1q33<<;g<`j;RhDHl#+voLL}i3UaB#Sh^K!b#PI(tu=bQ=| z!Ljhh$sr6H^`TxnWepM(ucYvH{!{ zfvZ6tKZ1+f=DwZMlW%OWrbS}PkWB<*V)erPzT{qV>pzsiWTaNLuy+~%W4)@0-xjKb zD>+NKIRGpR<2K_qztU{-!GGk}v8HmO{_5DvOI(U$@*T9v>N>I758I=aGb#JB*7 zh?+;fDY`-&!f4U7*qe(d7g4Y1Jq2EZ$m|HE_~UxbDJT!RJdN63{XnRL7O)B*CBKldW;RGO3e>04+q7 z8gE7l;>|pat7euKNMi1*Z;_Z1Rj>%?2#v~pFM-o=@#ysw&(CecPqFe8Vv(@$?K5kx z6JSv=rwNz>D+bEMu>GI%OUunhGwx0!ZYerBFSHvru(C#ut}uH+o=%@SsgFC8Gq=$K zCE);>=sQ#%#kKZo^D~YZxGr<9w0lrAH1%f6yn!P$n1kl}3RZ4U%tjMkigzARH;__A z!Ka=&Un2~c3v~|@^1poKL~~UiO{O*yt#S)8?%OK-+f-!}5tm+V(4x1g&VEVBLvqyT zu=v8B))Cm4UYQvJMx{eXHW`+H`aorMByhNp>kQ0u(>-p*AY?cKZ>(;*>RzzmqQY}8 ztFc6|Gb+XZ9F`XQjVgx>5&Y#A6A>*<4;-Gld`3Pi1|ZVw-<$@aJV;3vRdJUxXGy+o z19^UZ{96YwPlW1I_Q+uA?mH@N3|X z14?4xZg(~!1e4(6b)(#HW*@gMD>0Qi+7*G%M~L)X!ISPz+FuBfhWHx;eiT<$s1gjt zi6v;ts@&L#w{uC;-owB(!^gEcAZY`}!j+u!APv|#c_~or`J_QUNxFe~ZD)q#hbj+y zGeoB%(LSsePfFc!lm-0ffQAy8f}Cz(d~l=Wybq)9o(gSpW{R3me-a&hKvX0T1e|AR z2~ax3dZcDEJoRU?eT=cM7Ui}Alc-!I>Kb+@ySR)2ak$Wy`(2^VzEi_gLIi+Go ztTnO2o8%s2;(DtxCn3m5&j3{TC^FU|F1KgMK(+8nO(_NdU7>^rg%&2+4rvw{vyv;K z0xG~a)&MHPGsh)@&0``tQ?QdGu^ro#90w<$XZF*flJe$6nn1PR9RKN~UloT8%za1^ zDu8%b1pqaH&<#WhTx_{%nH!_E4gXFc_N4e_!Db*FkfY>9xOL@4B0N$6>f4@&O%=3c z#DKG}Nc5WHEIFQHx2DcU4Qnyh$j~8D^4Ro;tx-8ZN*MLax|AK60~-S0tEBqnUBI!D za$}<*cU8r^dMV+8Ud`Pj1EUS!?kRPyhe&8*hPcgNwu zPc$=P7Ol1NI;Va5(7)U^v z*Ys0C2krGN>k*{oS&slP(zN>rf67A_L03}ZDmsw(zL8N1LzRi6cU&g4_mO&>3DV2s zVTMMg?DCDcQ3o&eckfKlvp%Gx6pCX@H0#DS)Ajx!jMI8-huPg4+l>>CxmOgHKEij? zHX+$dMU~zM!naAc;{5R$_<(|DTc}tS6Ip`nO9Z{51dy^ox=FKbPiBcAiJxS{nkOc4 zH#y#P@G$O#zUSR#jRwQM62NVQLJ9YSm>-&JdBlDB@3`}FsQ6UV@Q5N{|GiDJSu?@t| zii_vUJsAS@v>ZyN&LR^l2YH6Zh-W)FcMOgjNj$8YmT8hxmJJcVD17U* zi3thWQ{QL-PZV0pP-jTn6{U!2DEzYMiy@8{^2o^QJ>e2xG1d;Y?_NB|=>-}r{^-aw zB#&GRpn8V(fP#JEF|0iFgp%w=NVg*_F4@L4$bY&r617>q>&8Va@sL}Yb4_RWlX4TD z8Aq1@+j_u(jvO7BhBLQmWmZ+Grey(XBXZ{KF7V2LaC&ccpEk?Fg3mGEo4a2fb%d5e zBoqBS0~g2N2@d2uaYZ|YI$f5-MRu&r-s_=uteDO1g?6dvt?f`Id4($Z=`eO%L(hal zRV(8ppv961*clu86}w-HEmYB_Xl-2s=0|lxeLBKCtQm!aSx8vA0v9&VPC3$|&x=pj1Cp->lmVb0p6kYGKEXAp+c4B#^z74Y9 zc5a{WEr&TLGGTa>)~K&fhzE)Rn`Dk*g1R)gQ8|HH!_;!M1nmy*ooloN<=SZK>$J-{NLDb%#&RU?l+b?*=tX**BJ5+-zH;?#xOL1JVodEHv-mH!-$1;(Y2AL zrf6LwP7;sS*U~tqKGJC@9>7VwgKU04JIBb3QyQuwc9<~~u2oq$)e3ryPLWUM`wT(F zJl+VeXcH{pANbKOho{}?E6R~fr4&~ncQH8CT1NRm>!_ zXvg_KcRb;LiOiDLqHc3gS+f^F-=fH#EU>Q(%pi8_?)OQsWr(Q-n?sXFf*{9P0}o7q zVTwT^;GpdD$rlO3gb0`-M5Nf0@Qk1(07g-!bxCQPhwx!Tken`zNnpGx5%MePPDaki z1~9l!WK!TvFY`=DH?e=S!62J`z5?goKCJp$B1dmmr=UlGurVaj{=~(Pc#c#7U(Sh3 zb31T0r;sM-Gp<-_)he`>1OA2fiuZK(cXdN3t)*^Y4aCKJo{#w4WX(j(68uSvHS%Gb z4LKFiKTBVOfrDk{zSv7!YVI%B4}*aNOU?a$H|=1VDbHMs13})F{uK%+3Rp$+LZKCR zPUC)MN$KkOxIPgqExlqvAW&TT4unN71j|al$eVu-&MUPRG5r*VMQ<;fUsSAM&j`&y8)(!8BmjM!0Yap?oNDK2@!a^|tnu_Z{}z9e+^ zZFl0vURrt&6P7G2{S>anp{1#_5Iyab((f`_`b!BPTZ**$HN9p@{-o) z&gat!$@4VBqJ=9<18?TdqO(HtACjK_l*E@7hZer@b`-O?sPvIDa9#VR(#LTvE?T#+ zxOCx}yjyy9X#NukJX=&$a`q=LWYXeuLY3D-(};LtP0Ivz&b4~FFj)g zt{9SyxE2?E$XXqG^ZWSS;?g0e6qkOG8FsA+Enl<=H)pR6Ei2>A3f)%pz>4D1FEVfG z-%2>Vk|n)qT~XP};-Y!0ic7DOgk|TJK7*U0Rr*_@b^q%KqU*z@FU#`{6{TxAj zQCzhAywVl;Y;n;Un@S^cbLRP>vVAu(X~pKyg1?hDS8fT--}(U4&fXfDU!3LLIom=D zzq^fhcC2(oxN!N^3t=AP+WQ`!=kgzEV_YFPR_Pa@EkO{sH{Cy)^m)B zrDv?=rD%cla&d8>I1mU~!S^ui0?r6ozi45&=LUw~U&XLr^4xO^@8_ZDkahcJhIe){ z9DbPL(?twx0GJ``t|Y@#B;{NHV#vB=1;e{9Ww`KMhSj$*yj{{idnfOI^iGD~>Sy>H zKpnn5!|)xzXd&x@5W{b#8777p{sPlGWW9n;4OvUy%JBCWF}&{*hJO#d6|&wVrJZ*r z?_2vA{)@c(k5bx-Ql>OdF#L>s>n$JV{nj|c2=IN#`ndGW*X3K^x{oPm1E4}yoxJ-z zFkQ%c@-V|GDY@b(?=J)92w4x`%JA3H>ireG|2d#1WMw7&Iv}Bt^?oV&c_5dNb!g=5fV7bHvb5_vQmfMd79nd8ocpG3ADLNFEu%vYUC|Ea75c>X3ET2*WRoGkmI=VZ}!n zPMpi|ThjkuyO#I2O3K$h#`}e(3}28@_>GkI(d(GfDs}tE(|G@)qAHG$0Q<-YYTOh2%L;a3Dc&yw^iNzb0e^lwW))UM|J z2PI|uL%hFk9>ZmCVrWe=yt|j-yD^tT)<;({e4q5{ym#{c-=rTN5%~WPnHP5yGyPE+ zweL$E`hcPVAyV5$ft;09Oj#i?Fn%NNk1k-iN=C3s+J4PWru?n+&;9b1{mow$v0=+vDyk8q)*dx&RHG!^m*Dz)A0fx~5hC`C) zDQWfJNX>sOwR%eW{~a0TxlkbXBI&)aE@sNdgA9KYU>Frhe&HDJcglEuU!ZYN#^{MM zrk`HHa7yaDDZ=~XQfA*?-rv5R;ngxLyJf7;i!x>89SnaWb^Be4_aBw?*k;~e+QM)= z%y8gphG%?$;orQQ;qoDdMh<$r(=CZ2*(!z zzDp)P|6zoaUs;0iiWK^yWNH{|M#=Oy0QV)?pWcITW(d7ga^U!_2oJWfoI}@PJW3A# zcs=U&)>}9dZ?o=w0GFGsZ@dYYzqB4ZAD7QrcM(#)Wj)IY^{n+S;=3PO7j)zDW9!Fv z;PRaH0XF^x>j>%*deQnaJL(l{hIM<@VpBu^VwJWc_DhS+5B z@tOw_)+{7~yr7sMygkVZ_Z~bG;f0ZX2-82Y5%ynkAHqw2z)HU5>(?QidhdRO)2Fav z*-P3G&it0(c_2+tI=Gqbzxr%e;jLK=K);qi^|4@-ANpSKL+s1vgSS1TJF)outB??y##4dzKL)Sj$Nv=kXU^;6!9*`E*A|`4 z8FpP!(I_rQi*Dx}dwWp|F?nhJM)t*mS2@`iZeddvJ$eel#pe;)mONR5aOpSMHK*KJ ziSSK}0pOui+Y<;+`$H|lW!o_Rp*P?00K(J10#qR7+9YH{tG@CMNgt4p?4Sk+j)rHU34XI zl2mK(&)$vnq4Uo{nEB1M2!|IFGw*$RA;Nt##3~0K-G%VrlG_j-`WUmNe6 z^{mr%OV*ypwyxV0LfCxv7&>v&Zq_EglJ|*Q*urE_lg=G_bSvWX1q2ow5O~9}xbT}O zrDWh^hY?;^DwnsFUbIG+x$IS>hwP8AZ&uyMI+m{?j#>TADuipch7qoPC&P8$WFMb9 zv>xGkpJ4xOnOcBw>rdGFZC_r6Fm^VPPD=}WqV*xRHPL!E!nQxL=i1{ev*WHtgvm>I zzx@|=2)lkpbkIHi0fas0q!9LgmZOv!B^33qun_L5>p{5tV#3KqS6q+q;-mElFM0A3 zgqOuJN&)F2naF-Uz`f#{7$HMdw%Fjxhaw zmT}R?E=D*KVVy7E!5Z!VT@2yq=Q#_;7O`F9zqknD#B(SrG}+CZhaUX^!o#0nIaeNj z55glYgr=)LJ%;e=M@JF9bIQ2M3w?+69*)wD)+Ge(W7hka_)cprhxcY{i1ob1x`)GahqW+{%X_T{D{*7|=xIXf_lv%MKQ7M~U3w)h zKP~#F#kjmsbP1pRtmvzpfIlxf z!zw)!mv>ozju%Sqx88FbE-wqt58W6Hup^HJf5e`DXYlSJTy6@!!0CB&@KgNIEy0hc zak({k6KDEu!FTX-dvGVm=#JnW1k-l~N7%LR4qkmHF7F8rF?MJ0P8N1oa08lI@<6cZ z9$bDHyan^2;8GL1x9FoKy3xzNe=1%*^Uu(;GAHBPI1SqVH=wH|^+Wcwv;ACz`=7+n zm0WYyTXa5=!G+q^_Um%ay8B_gSAOqCgqzAgig5F0g38t_CUuTCpU!Esa^;MUuYI@} z@%8+2Xv6!^4)6Q3zZ{x^Uwhy8L($9UA%0%hR)m{o(4{5k|B*z)mXaG0Zao9-3vGLi z-P!qI1mT6xuSU2lf&8IMKXNa^w~VkuopaE-&}Ah@b*%=zh5CkuHrFHE_glXCpf!Ct zE)Q9c+lQ9gTdf?$uUr50FN334|-RY(jX}=iZ0#>}#(tzm(L?itlrKEw&ojvs?geZ@C)lc z@J@v1hWT#zf%6bn#Jdo#zn>$&VTO&W{1U%j^*npBdO7oN>^Xq2=8NpE$PK3;tc$YA z^3(jPHwpRh}L!JN1I(PjQ za8{^$$=wKhyB|P!;j>K$`!L`btn)Yw>Ax98*x$Mn;m(chv0cBZM!5UuBM2|rvl-zf zt68^8Klw3)Z#l&8IztN)UiKdw5DtWhLia4^93KpwhH&V7)++Pdtq6zT!`kjGW_?C( zVab;-AZYEM$5xMya(x*4A-^@giM=|xW);FK{=66A)X#1}IDJ<)!t5e~<;)}z%E2FS z-W~c)6~e)=yc;$F0i(eafNvnvR^)+iRd+|rs=7(_kd+UZ9ae3bQ`4zbQtMwJu_$p?48%9t-VWhszV8U!IT4Q=!9cxO^k@>FpRjbbu1{hsp=< zQSs0@O9{I6H*e$I6hdWV4*|Gl8$lv+C%;#_={kh<%?wA|I4Bb4TDtSPI<`OPB7X8Yz(!t{0;uIj z$$W?SgX9j!_@PGtpYm#QrgMD018|wIe+F<>+tmZ`yS8^4V4dD}Bw(w)gC@dl`k-vU z9zBn0epTn>6NmM78GxgDDk*hLkEE_VsfR;v$0vHo3c%-jO=rMaeKz&>MZJW)=zIMp z_3u@E`CPy?eI511b=^aT_*IYZ30TzR=YfF7n|w`WKGozMn3D|cXm_Cq)OG`AT^#@H zVpYo*Hbq%`_@*v^ef*_rz(Jlyc0SBcYy}+QF=Vc{`EYb3?q~aNGSmo&OQS)Tlu8bt zJk$f4G8m2}R2-E?E|xPMJu2eqXUJ8j2KYdy4IBYFeQ5>gPA#0wut%%*0^Zclx&a?( z;ZcAuHBT+zyml{5LYK8S@&H$~sT~1J^p1A}Ht8200PNPM&=@iPs7>gaPV7&P`p8ex44IcQugv=I3^UZO7UyoP9Z;Xfm*O6F9gLBlezMx6V=7T2h(m_*#$AFH$kOn%Y zx&SooYA?{SMVc(jyT1}~-?!1AGpEIY&T@?h%^3)e(5in-D&naTq|f9EvdR6Sz#$3UkpX#qODE*`XSB012*=Q@Bs#&-<>JkD#Vj3>A+60m{?U@8+egr}2! zJznVq8n>G4IyAKlXkv59pHfl-I(8k^Ghqv9>s`|gboO+zR(b#CpbJ)!&WkvsS#vQL zySOEM@@T}C^5rXKJ@Hc?grkW)rLm`TOt}Ut8GA}c_9GZg_MIgLa`{4(@&-S-4setY zYzO$5XQD`2gf0S(GJ%Yg8#LrQV&HPFhpqd|C0jS~KXyk0=(Hj8U zcn$gNcD~~dz)Sq)5rA60pN7OPK6eaYH@{o}c!l@z0`~Huy#V`oI?3(l=eh$9@M@aW zFw>&pc;c9}9`JX5F&pqYA3`>GgZG7z@a(L(GvEmSOMAfEJen;1F26zo@9`*FQr_q5 zX#kz%<-GxQJZKZ(BYw68;8XrF>G>Hir%C*C-jt?`FZl35fU`W1vRvTaiGYhdj$HK{ zp8gErM}CW(_$m*g_WioXPgC+o$X@w619@kD%mM68%B=C%O2}1(6QxS^+ z&ub4-Y^~Oh(spS-Q`&AViTYuW_AQOc1KMj8 zJE+CLbfP1hU89+5@Hga33qra|Zj1Hgd07K!pynN>QcIHhfR-+&_LU`X2Cd{P?*pvm z$03DY+=b~v6xrf8GIL=vHL2p;)u2!C*^>ZI@-L{htNDjB0nhTcsQ5KJmz-!Vzup0` zj<5WyET(OGKQJPdKRcXa97q4r-PrB>Ku1(0S)k+cdqJHOw}Qs>r&jcI1c3HhM!wj4 z#&S^CD4H?*444cWJ0udc-!G)q-DzZB<_=Y%4%<_S6MCqHC>N+zk ztJqhrV)Vgebq#x|%ltxAX2=#~W*1{D{C@)G3dZpVA2EXFmS_NmnkevIz{X@fty%DU&PGvLo~NYA0p*3Nn3(lo?Oj=Kc#<$=0=RM49R#~#4tlh z#0(&UDrY2OzudZ2sN}orZjs(y7r=51Xdo}y35C8zLbn>=fkVdQLOfYQ^5-L7B7f5QcprP?1VsQ)QHB zFYgxkq<^eEpOjCq@hL9_g)~2?Ya_*=DN^2Eu08Lae&j2p{AX%l$-?dOo&CtuFQ_P7 zG@zc^<>?oQb{=I;zy_2;FIwD8!JhXXDQ|D5S1#PEYE8npRPqW_q`Wm3V?P};I2pDC zC8yXE{m4%^Zsh2Ldm3}F%eO?L@*Q)&$1WSO44Z&0D%xY~A|aUbt08|z4m?r=cS-f* zNv$6=zcyBX3O8!{%2v3&exsJgsZQEy?goiEW^1)iGAHWLMD2g9{3h7XxXmnatz+k- z_ABN@9W#>JhgkVdv9EBOS>jrURn)%0oTy{S@3R*mIv&(u6?%}=}ehCyd?GO#7- zEYij?qB@K6!|&*a@ASiu_QUVgfKTH}L%;vGncI>^^FtH%BP|n_KrP~p*uMw(RF1Q` z+me5%djXw)~&f2r?(*A1PmkWMFf7l?)*<&kbhsfX1uV{L0tX=-v`%h6$ z7^?_zB-q4a;8zZBnj|zS;8z=X_YTABU^6m4<8t|Q#5{yWV zAO35ioQ47?{P0f;e#80doS*y}6mG1&&B1R>&%3~HiA}Pa_td^T-cSB<;Di3ty55;&_{veBI zhy0XtOy-ZZ`RxaO%J~?4@}DENd4~3RVXTpLDjQ#2_spWBsPT>T;!>7fT#7>$X3lhF zH$BYjEB4L8u@1gs90lXSncj2ow5Ji42gkSIMg77od~eQ+Z-%kET6Zp z&^ifUI~XP2mG{Ut(0lW^HaV@) zF&0N}OZ6$NLY+J*6KC;=cT#a|UhW(Zj!c3jC~M;x#R)8C zONcLV(uWm|&qd`Hl;w-#U`Z3Qe!T(6xW;SDzU*>wAzo0&gT*`%!|S-nj)#w?(vx!W UT|+9IP8tOf4=AZ*Ci;r~4=z&kQUCw| literal 0 HcmV?d00001 diff --git a/examples/smpi/mc_bugged1.c b/examples/smpi/mc/bugged1.c similarity index 94% rename from examples/smpi/mc_bugged1.c rename to examples/smpi/mc/bugged1.c index 699d293b7e..68dd966cc9 100644 --- a/examples/smpi/mc_bugged1.c +++ b/examples/smpi/mc/bugged1.c @@ -40,9 +40,9 @@ int main(int argc, char **argv) } printf("recv_buff = %d\n", recv_buff); -#ifdef HAVE_MC - MC_assert(recv_buff == size - 1); -#endif + //#ifdef HAVE_MC + //MC_assert(recv_buff == size - 1); + //#endif }else{ MPI_Send(&rank, 1, MPI_INT, 0, 42, MPI_COMM_WORLD); diff --git a/examples/smpi/mc/bugged1_liveness b/examples/smpi/mc/bugged1_liveness new file mode 100755 index 0000000000000000000000000000000000000000..d64379358210d677b95be413f20fc875fd9bbc27 GIT binary patch literal 67709 zcmeFad3;>ec|SaNMkC1!UI4QixER}vY)RIPR%2`|jYiU7ZD>Yb0^~B1MwYNPG$SvV z#letZ3R#lU+d4*bJN85 zP*cOEiIJL#@u|6kH3wUoYML5qbJMjksXwd1zU%BAl%h?4oP!v@eLDWwWqiKxBOi2D zHQs#jGk^KPbG~`tGyVO!UoK_0U5LMB_&XPW{4K#B>&i0tV_lZw?^OITKg(Q&zccZ7 z3jX+=)9}ZiEuj~juW!w;v97D}$2r2fpM^jE&QKS3x}Ask1^8QxzY6><$KN9S`G05o zBl@28W4Y`HzIV@xBb9;Z>5D4E?KQV2>@Fn9bGC(b=66jUSRU(U>TKh_)bB@M`T4Sa zH^1|SPu=y4WnHINUi^*gcCSA3uY-Y)?)cslfBU_++^}y^{A*X`ui29S@gIK_PdxXN zrKf-Qy@wC%3B-o}^{4;(Pv3j*DVMyRU0m|_FjCi)cybUO$2u4P_9LNGI>*Q^&W!j) z3#8{3D1T~!^qUt*pG5hk>fgM;cT)?bKej+QA6p>(2+~XS!@n+&|5>U3^1$zxZ$}RA zcc*UGgBre?CnqF*Y2ew#+f9;OKaX$?R?kE?G_b2Xr|Ro!^x6f~21vc%i8L7m|rfy2lyG&g$fJ zPkdr}Dx1y>O=Q)xl23a2lTLDKJRj(ZJL7w&rf0Lf%gp7cCo_3`aVmSjnVFrQna+*p z$ET+<6He~X57|+5Aa1yoqVaMX?< zsUs6=b3p#tJa41SJCh%q&1U4?Iw@IwBYO~ypP9?&0yDGYQ~6PJH9xDnn$-?C*^x{> zg9k&ooJvO$TE1y)dNR9dGBb;g*|c{&ze$f8H!M@kaBj{S9iJKx40D9~@cIZkVlI~* zK@Jvc3RGWZcI3_nW&@qw$+ox?tBs-M@-y=<2*_^k%^bs2!XD`V$0vnx#zv4)Z`*;n zbH=fq1OpYiura-kxbK;@$5PBX;(q1dZ_GMky4fe0{dQdr_a4^E{O<9k`|E$dFWu~s zeCI)5I_qS9ANHm58|L?@FWszpK6}iUjt0BGCw%GL+s*G8U-~H~5!YvZ>BJSx?;E~! z?$PG=yf0m&X7Z@(=uawN2%%@Xj()E4sX*XF<69QlffMWQL%95c?YLunjCo&t{seyO z?qHl<`Qoz@zlCvj;fqg5{CdXObuT_D@ma<>gfBiQ@oO39Fuiz>#D^GXm%eyJ;;&)3a@j(-28 z{&e!`CkR2io_>-5uvx zU{?+Ik*=dJFY7w?g9E{*&_qVPwdk>sDdq;Nvf?MD33K;KZ|6zjzq0ytp61J@>GPq z@gKX6%{}pS;`dUUy9S@=x+{UCuXP=J`i0aVPn|*p8Mr#@ELKG#TH=kJg8O{Wj_tYPdcs%^k3Omqs*Wj=9SN?!h zd<75wL_K&(KR6v_;KA|4OSe6-{I-vykRMz3bRBP;V7B9{<|KFGCtY{-pjVf!O&tpSB=Tpz2#Luvj{OF$}ay;?Xqc2-?S026b_ksM<$D^!a2hxB1=<&o)@Ff4?$J>|| zLmED?1SKEu`3b(UQhnnkDH{a_++x4}`x7V7YqBUfmma@{1^hy#GUtm|Z~##GW1oNg zW;~Ozdf`!I=sJGNBjwVBkMnX@0>%GB>tihHQ+(6?Mh=-#0IPob)8V_2nR%WLzX^Bz zp{m!Yg2q)rCHjK-+ydVx1%CCmC+1drDt^zVKrmHss*9s1-CyqHQ8 z2ozTOGsvt8Uw+#kFd9#Xzskvq-_zkQ>AM%dj|c7&`_)sU{M9bM;8w}kb!=koH@c6F ztbM-guA03;JJ5aCy4}1W{e|vh`L!=~AG=}g%U#E=T8sJhla}tPAG99(L-N>fyPo_* zD0%GbFPzKz-uBb{>gd06y>uV@&+cQtZ9n$&))S|HtLx}fR@deq&;F?E_*HAM^e5J? z=srHO_N;E)+1GZW+2XNZ;9qnYuE z?1+6KwoUA_@sypJ;9h^o=0;n~gz=GyY^~i1yd!UqPflh>#xwbeL$z!$p3Y_`vY8w* z3}kcDbF;%)dusZCdMB`M#LndQ?~iGa_n(t zvCa)`Aq`xPzsP@{II$boGR%M@xURtUL0nhk`UI{Y#(+GJ>tndSj4OYnU-+}G9|%|n zS6JsRt*E>QGjJ`^NTWUT%83)tGQ+YJ9m~$TeEE_Cl}7@XowH>_{n|B5W}bHZ-GJec z{jGJ`iZ=%1r<8Z1ApLv<*Rhj4=Zr|>x#0BXeWdZn`h5U@Phi!mkzuN;-=}eX4C%+1 zaK)YBHn_Tx+qSZi9fTqKceFXXE5}T!4(WWWpJhES6(CU8{Pu@oX>h;5UCfG0kgTXge=1kLjgy73VzT?;HBLOj5*8(}QCO?z1G9;$P@nxe$TiZwA{Z ze`ZW=-Ci>vE99x-eem|tMcXCCq>t&iX-Ahl^>`QN`l^j;ZTkAKz7~J4GakRh zjR=FRgA>&7ov8?haB4MVKRn9QIvg~IM@Dje`3c$`ky&m@u zd`KSu8N!OH2x?flBKXj+5nI#_=1K51gGWN6`bJ zu#T=+@}avCEw^rz=A5S@J{rGk~EccFl^9VCGwAshn4>Sf4=b zY|fJ4z1vqDy$7*#)U%1e%6-R>{3zymz_M1B*C6t{6DsoU8_)^2x1$p*>r{Ms5#O;E zg$%dqR3I2`qG16Atd-WfWv49(EjxGFO6yc>Mfp400FHxe151`{Ln>OPZ?PoHmLoNJ z8fN|a059cd1VYO$S+YgaDo#V>QY@s()2t;+m}()*qEp-~Edc9_PqRYH!-8X_LV0i=PnW_+@D-hN7 zV|1k#y=*CKda9TGvZc%s=qCgS`~Vx6W&Lj1DF{V;!#-V*XOcabnVgx(<~EUWv}tm9 zVeZQK)bPaINLDhwdai>*`M{>R-0UX(T0vx!;v8wg!rrO5O+(}01o`vN&yqXzYB^Al zDg%t5O?!uj=a&IE?Nw+YHj-Q8SIJ=bPJzJC+}^#}ktldc`?FKoT&{MQ$P#$f zhL{K2zuZzbqhlj@2ltrs`9m{ODhiTYysgVc7n!d+ozC#|)aW?th{_xo9?Q(CTX4-X zvrI-&gbD&1mG?kHH>Vb@&xno(WKGHyn z&9NJCJCm86G|4krsTES)$;A6PP>d=wD(g(=9L)|^@4FF>1DZC1tiD@zfMJQNLKItC zUIus$n(Yxg@Q%H8JN8C@bf9w2-UlA~!4E5YDsQd4HFWATq3i5m<7r3thL*lJw7>S~ z1Hp}_9UgpOf9Ukxp=rBvYp~|DqYpfY9KfWk@_acWlK8hs3v^$O+C9}Dst;441K*Xjh(MhG-C9}=3#qtcKy9WAp zMTV>QSJ{raxA#{|;Z=ctBqdtgownA2fn;L9NhJo7t=-IsRJ%q#lX80d1`_?4CxCxE*Z@V7a#qcBGQ8vs zb7Nz)DcU&L4XAK^mOX}d(4>jwzShf*w&4D zwzsBRBYe5a&K`uoW=i^As>DYeIvH6ro;`i-2{eo8XvCoI3a&8+@Y~7E%wS1pXPw;q zqg} z=c}F3nJOFExv4;qw0Aa(t!auWgQtnj}DC_~Cbn0W$kB*si@xI>FV2_%pSW9synd)<*bxjRTXi}^Wzs+2e z!+@6i#z&kyx&h)JOkd9I(FtHVv$OV#6Y}z}~%qIABJ? z+1X>)9pns=K0&iEQ0d4B7Ak{Hw&V16v;&x@ut@lM!b$~wIgCufNXDI1ytTI@GCGYN zFYkLv!O3d5A2{b6aJwb&kNURJyOfKhX~0>o@@B09^!Vjt%Ma-eTxY zc-!K{Bg0kpFtQ^SZ8G_DW7D(X%?gw!Snf^$E@M>v#i^&=W(EUX*G5}5H`hlSHaFHc zHpl9t%}tGUvFyf%&GoTvfscZPIeW8tCzFdvq?(sU zb%b4u{xR#z%=(_z9SO8oEjpbTDT-r8UfwrQZO=u8P81-3i#jnd;0(0( z?y#HjPP~86d0k?l&p~~&c>>t#;Tf>w^H??`)A**DSd-aFq}mbvwA#M-s=AA-ZT(W! z7W=>$)|(xvV@(9)cJ%=?YAnY^Xz(zH;(_yx0Jn3&E|NRC(+0BCMw=TOHaFBa*0sc9 zv6kk>y5`Nz*_!&6jsT{d0wG*1DiV*B*xS(|oSj4(UTc2G>5pKg<*K;eaxR?j>y0Py zr6l()Z+UZr0V)(v_YFj#kuY6iS)+|0DCUOq)3X>om5bxl+6`2w6+oYRjarI$ZthQt z-*}s#jegYIA;*+&^|tn4=+gtq-cF4-2_WLWlI-mU#)+@+lYJc>T(7cXQB3NJL12zt zzP{!S_G0&L$5Y>w3u)(c|ia*%4HlTR=nr z?Mzk8Hf--8$n5nt_dc!#;3d6P_Jvz*OkEe#^d=3H5Q|4j;hgLTELl`ypgq~qfnMc6 zCU#>$_O!R|p)#W#*UVtw_S#Znciolj&@kFS4s^el$oamj6*L5@W1AfKI&t+@K=$5t zo9ID`crO%nH2EOVo#5Ck28BV}rIt*0RUkK!&CU=hRcb*xhGJbfg>qWBOzlVwhzG9q zL4HwVzr`DgQjX~#NDL&d@X$^Ug?i%HmtG1QqsrchwyGqQ4KV1~+qPoNfT>n_St7(t z@ku>%+WPuHAfN`_$#fc1L}43tG*(aQW}rLS<4tm@q}wfgoM=xDB;x4^k&J4nPUWYo zA*jq?^)tnm6jUmco8;mJVwvjU0<$9*scfi6T2`;X?sg~MJrEhG1~}wg+dn-{gn`II ziiBSZBZeneYHY#=CULdBeye>G6M9-xJD4JCN+C~eKsH_Esi7WNCnry9?;a=BH#h(S zuBNfEQ6?)kW~_ZX($t8ZmBV3(1B0Uh_t!KXCVnAS(kH))_-Pq6)>2$K4h#C-A{?KyL8^l2g;P9N#gRoEcn6#>+Zy=4W4^Wajw3F;4 zNz4|q9*PbuK?3q&9FPK_ez@ALHn7D`#O--i7x+_DcMf0S$H52iKCdd@-LJ;iGgbCBJ2F&NWnX4T5P?J$5xnbXBFK1iWJs2Rm8Fm! zh3kOiHn@~f(~5=TWF`(|zFFfUD}}TP zmLQ|#(v&X$OQ=dNcl3UuGciz-knSX%2Bd-nyS_tP&7K(3D;tZc3)nlM9Di8jvWiJ9 zV54$j_B&iHmM`msU`;>>xYIJX_yil?q0?Ytz ztTq$W7Q3Z5p=ibkdH_Hj-vO43yJS-uTMtcjY3LVFKVI|l}n)vX;5qFv>5*gg?gYsdwPu&USXHuwT zklKkI&(I8g9Zr8Arxyt@j&rVP0QHsa4 zQ9PSny?vO1peJPQNlS{j+mQ$-dm4OG5OWh*@H9v=5aAa|%!Vo<2uWu4VZpjY<_Pq& zfD%>bW`}W!>T9fenz*{-aQT9x3|1qMufsNoP6yerUN%4-8?V~H4s{VAJpoNgYw?PV zlh6ZWKCtkj%%?v=)Zd}p@Fe+TUjCRbzZzK-KMt5BSrn;Eb`YOo>qMQ+w^1SQg)L;{ z@aZ_-tK+A~?Mrn@TkMS+5hnoj-nKW8lw{jXeTg=XUyavQlT>VaMnz*1Wx0H1i+!U& z&E9lZ1RF~cQ7Ye=nuZW%`T*gYjVu9_J(X|q(`y}M5(-vH?msX(QHJNsxF>?Op(?VT z_c14`o+)zBo%4EmVd&;FmoQ~PD=D0{6c$OCk35CDc1NnMd&k22E@4JnYkUV#JCN#n zlA|29%mI^VWPEfK4IJab^yt|GnOSJ~D|!~PR6s;j*q;G2593lQ8~a!j?pXfa*o)d( zHh2Pn$B~28hpOy@_C*)jhXP0feGAAV9KsaVQ8D=B++f;CNldoTP`;?6xdortwa_3X z8}Azgafm_F%pXXfoHT0&T0+c$np%&kl{h=-P;|U~-6v3dK4Ba(|rEU|b|#tghh$x^j<5O?`8fFo`Kw zb5R-?>PTKR&nKYSEYmI7(+^4y0#6DWaHoknB^u;n63$pV@QjnQ@CZ}qbMVrT(8PiM z^$zyi*@;{hv*AWGoRc7XP*89HotkaL#fLL3OUvcf$-5k}J>-A-3vALXi0Y z*v~g4i$mnN!f4h=vX&WmJRwhX0O|#hGTs%DW{ymARENi8i>JiL^r>27{>o#mm2P&) zjxPEBVbvS|^Zx%Yjlhl44De1KUKL9n- zTf&!iu@t3oVvGG~&dC5b-=B?OG3E9;Sbm}^grcA;g!&8Kq^TJqO{iL59F=cit4WYU zm>%D}S$b2THAr$7TGw+p`g_uTQHn=cA*Uj&KvpRRrXnQ`pQ0hQxnXltb8K_tpxXMd zRT8xWq^&zh88v}7#CUD5!am%eogJFaWs4999~Fct{2Jc`b(772-Guw<;knt|^lWu@ViKeUsh)^RsX{@d8WpdUZ>e-x+|K6m z5n+v2uQ!>i>@9*%`SMXL43W<0Y&IKl^HmGen7QylC%>U;eS}}e=4tAtzXI#)8B@5e z5DDt3xmBMYy0)4LQt3zp(W}Yqlww zykciz#$c{1(K<H6swVicTe zGX?4^NJym;)RIbfX@nhLB#iPtNyQgeHm`@Y31}esg=DY_hhG@1G7o`tPUTVOg859i zLR7koXcoaGR#OsRPDe&Zsz*mKDxl+KjY+D_WLu}>^RC_vbU(2o4C~7<7Ng{Lb8Wet zP&9zbH-;0c9t+7t9R+qITSatg78;Et{cSHQxT6gD_!JR(j-VcKcbwG|kcUp5C_Ho6 zGJNy-@f1*ji{d^Iu+W<7hu}3$&Mv9B!XAfannB)CErrCxM4hJh{G)xjLQMs_0yjk| z3d9gC7i~f6$B6t1^hu{9I=9%o^;NbB(XUHE*G?;W7|5(g7~7=Vqa+7plus@~SHn-n z(n+)mV%P>agHbryoed?oDFyyys{+ce#bEiIQ_lVA2DG15-i7 z1s##OseQ1OoT3gkK(t*~ZLjIjEINpNfTNF7t$#8*1uqb5s->R{mw^p~mRc_mBWf4K z$-(bQq>u`kVJCUDt=(uezekWm_Jhj`atY5;!gDSQ4w4c?Q5w`68J)~~A~s6cxI#(y znPGDBvzcLR?98af*wnLVvnSdjFbd**K^{;qWk;X@Bj@$50qDhm$-xdM$|O6TC%`En z(d(dbTGy}{q2hvS}c=7;QI}>S9WuXWePdIP{B*HHQMH>UB0L93r zXzR^Un%&Xe+L?-hBal{941fqLDW8%6CD{cj=sYb%DwZCpxV)blY%`i>sHTQEI~`FA z0*LWJA;lbw6@nmuA8dwxJ)tTYzxb}!f!^1|DkFOmg1@4<&xW)^s5+2r8-%8H8}|kf zA7(90WDZTw0j3ov5c(Fu9t@R|wW|3lBI@Yo&0tWeK?bZYn10fSg;WZ^O4Q9}05fg@ zkXVsIN7Z5axtlPMt^QdkD0BDKNE5-Q`+RJAdLNXK^HoUXW?5c2*}%7hWjPRZ06>IbgaD})6%WVRKMfx^&|yQ9BWs2yMz+9?d}fPH zk+?1gprS7Y+2oq7!)wU59jU_ruG!kIB7oj_ltDz2>u_U)1EV8EmJ7uNNTZ~pibX_` z7c3x8TSO{+W!=?MBvkL9?z#rJXCW_f7uGy@eZ7MK^K}R593Vj2ZQ75j2>}Rf1Z$(D zkdD11Famu)ncGW{K>}HH)WF@Gn-U>{*jiA)ArJscfbxK=kBH7|$0Z2zus!YGY$R4E zK`dGXNO}ugi_v_0DeB4<2W>0jx`>t7rI>8GRR|4CC=LaME9hhq2#H9XO63%Z8%U-# z%DIxLkFQk!Ynqyx0$^nKKH+4|V#bjIKohAsiY$AR;*o6m>P2*)x$)XtW@3 z+CYN39w0UqCyjlem<@WDD&*693^rHWOXCGJqsq->huI0f&xw3h)IuSRr#**QS_ob# z6soNWRmcsxI|Npfp-m+X%AIMt0zLxzh5W+4bQg>`M7vw_LlkqnrjS2UL;T1fWSF(R zRJ{@a=`tb}uvPr15|Gpgd`mr&l_6Y1%`+33qo79Y0thDFEdjaJY@4gPN3qV_SUYxU2Uyo-+)OJa8)#X z%sx@7J!})A`BG8A4T^0W@ui|w>>NB$tU<-uRirfMDGLEx7p5xEivu@Z0ZOKj7M9mM z<{t`^4)XZSn)h5-KC)$opx_;mE)|tt(dY%L-N*l;UuAYYrJ1Amy>=pof^rCNT~8R* z@$G~CG=$<9D8Am@j9EoHlLKku^m-xbC^(4VYz)JI4eb;TqT5QvMAT0?XLqJa0XW^Q zZ9q_=#nO@7ZLa||&pT^m)KkEi=hRjwG@#~KIJwMdR_!!H*8+_`2wC)NWdc+Kh+vPZ zx{RT``&wB5&}(sDAqQarhJwlSfAd4aEpXQ;6pMT-)Ry%LWm9)Uamg1UYTRV*dZn~b zv4)_|r3}8X9dHXp`Tj(q;N>&!c8(dC%_}Aeb~$vbwvk%I@x~w!4xLDT5G^tpcin(47Y}y@!yygiV1El`^lZ zpvcUPY=6%Lr1?QzW$yPf>x45WUrjS@&^ zkaJ`EhiVWl5M~avIDiRI)s^UtXD)!LK^X2++t75WC^vuy$kzZ@RP<82#oi!lvCJiU zU!tQuUz39*Gv37aM15Or*;I-^jbNI?DanGNP>Z6Gru1o5A|xJE>;_^+0i0sNxoW^A zHcmy3mQa!ebv^{!x2ck9l0JghC@#dbey&g_hP%Ds#1Q$JPr;1p`a67bdAG_keB5`j zmqGf?u_gv)?8Y=?7CPOv0#Nc_P%0$7U|^-zXI-trzfDNv&z5?Kf;l0`ZH2_FUA%CO-Xc_E+c1t3q z)lp#CzHiv4k0RzL?3XrJ4~Rh`hz~^R`iw$YF?FDkiZ2-o*YQ^~p7$o(kAc07?qmc@O z(?C?XzI#Y=Fe- z-Gb4%lFgX~O9qC1vYn|EfI|-r*Oqlg&|N@`?1I`Cb>Fmgr`S7dr7gXj6wSi94^*xL zxEkf0&|`ri#Xo%7#9*f3>tBoQtvSQ4W z$*ljS>=Y1&;(B;=5VNvE{Hm&>_Y5x$<^;+YsE~S91vyWN!Tdtk9IKoIv^A5fQ3)02a^^H6~Gi5 zZn_(cTJp)rGEm9@+;_1(0rrVqkwEj5?8@Z1Yc?p54@GSQi3BDmtGW;uw|*)sr{?ln6(`OX=ly<|*)@(O$$wefs+C zC^uCOr)WboV%%hTQ7lEy#(o%;jZYUT3>xNzC%6(x6#RHFvrI$J&OHm~Kp;K_}cudxm+O&NSwH(M~U^9$N#mhw_=x zCrpclCY)f$8u{dmRjUzu%`WK7c{qHbVJ5dJqaRe{vw@QeCcK6Ex}uQ@0OCi|$SRCb zc3g;}iI#*U%kHN|AzCJ)nw|8P1ANa{gS(tn6ICq*_o?Hb{MEMP`~SoL4|)KjT?);e?^Z)$xPTj60EAXW>6u-U&P6?i1`?V#;B+Kl7CN9;FpS%w zg}xugsLFXp(WXdSZ6qzQDSBcHB^*(<(%31D*`Ic#13W+Cv`>#i%3|t5jx`lC5oamH zItmF@#gP_$?dVB0wNXMTgqM765ZoMoc%c~t@04s?Mz0u5462yVPC^;{+Xc#JLKLV6 z==TZF9}k7U3c(j!g!u?QDSKC%Bw{3&2jn94ETW_&g~MuiDW1k1H3j{YCaq+NTZp{H zc%1SBPM9HdN5raZd8P^UYijUI#k721FB?(glBo*n5y+LI9?jf$ zbw5g}II5jYn6kp1Y?RFkg0Nkvgvd`6Ba)bl_Sm2Oj>L3ovT6;)ELZ?dMQ#y*hA*<(1mWdSScWG{-NH3MaLu8nj- zDrTxOK_1EGp*G1yP83pgJk@rR@npJt4}civ7N!TuebTUu0n{K$w*y9l6!?IM2|JRa z3_&PIgFZ<5h1U1%6;WORexrPtp%>I~Fr5Q^kkAMa)KC$4kp|y}JX3}cHrybRinXsD z+Jciq|q@U>g=?O%$j&F;NlkC@p}<{>*Ik=y-NQ{5EM_f%Or*17|_C^1!Zw)WfI| ztd|FR{iU#e;uK~9!#9#wTc(ThqXJ++Y*^v@qKy1n+yazVN!Id31<)zi`1U)z)WI2iOOAOk?=Y=N_(?)K^%-=$ij|;q~r zn_`=lbP`GP8S%wqVdSH>W-bBe@725|v1dUAJU5)EnDOFQ;95uA5-NW+${!w8Xp|C@ z;R^%Y3RhTr$Rj`%6Fc#qpwvthPJ>Ye!&0F%Vp0=mPlA;KyS-E@33q-qWOk$VqUj4+Q%Ss>FoL#$;K9x6j1 za8SIffSO11sh;Fn3PWRnPW&jHauhP;JyS-){v1?*Bqm3~3MxD?vfH)KSX2CZ&efnWp5TQF} zI1d0fyBfZTt6}KlrPOS5)s1SYN(d5t64fo8!9Y~zA}oV$Gm@y3OT61Snu#T`Ytj5Mj#YARhFaLMorD}p@)k%e=TAn{5!kawYSi6`fTW8 zcu9vYuI^M(Dp7j~9xX&*DeO^qegR_XevP|S3H>>6U(lP-pu_j}DLq_4bQC693cD>P zI3Z?i9RLdg+On=xN-5{VgtfgLb3$eXzT!FK@p1n>M+J$^bY7-#hW13dRY+?xLX;a- z{iH+VGO!d9-CE7|(%2bLG_|E;Qezt&?CE!Thki8-PHH@-EK9a;t(%;3;@ml9b2R&k zhp@W@h9>O6B@#92j@EAKfuaM2&w@=#Ni^s-5yCkUbvRVKb$Z~@tB-C{xvVrt#h@to zsM#S=g5qG>u#PhuxF%Gf>Q5cWV){iVt65K`m#4N1u`nf#YSGeKM0X^CJV*}89+i7N z?O#tn2HH3XXNKs1)%`;3V+q3rN+%RAyWv7q+N=F{1`L?s&}ug++HM_G3S6fqutR7@ zr=a=5>nu6H3c!ohoc&tZfpt6}7EF`jG3Aw+!H8???(Q_TEuCX@|r9+N_aRl74|8Qn6`-XogxL20{|%55*j2b-KdaUX2ZuA zm=CT333!h#G~gadO$$iS#OYe`gAG1?758%+H*&9%cLZGN)!^YhvLCo?Dh{y6V=&90 zz6EZzjM9YRibJVmETR=5=rCLBUHG*tpjR?N4is@gqdI}8_5>Dz-={)-3banEva!;- zY~TSZ(anvI@j1U~1P<_&q%4$$eT%19;&SQ;cwj(|HABpCG)oMIqkBd7#(d5#8`Xn^ zLRU-Yrgo3P1^42-5K$N!-@M3k-Y(-@k=USk*16PedZBx2_)pWKL&Ot%}1Ro88P zX70Fz;22?rM|)ZWvYldqwI!g-GBaC^{foG(F`Gmh%qG!IdeY2;nYhxrxVL4pWq#Eg?`urWFE~zA8L3)i9P^q-SZlx1o}($-P{ zwh_KaGEG~*SD3_?SQ{juU?a#+w4h%Dr9+9z#MydXtMa?g-*pqwGJi1wSS z%%+6AP)=V@Ms*W7xz^C7wshf2=-Mk@CC=~Yr5rh)=6M>>uZNZ9>k?G=$CB8fu0<*~ z9x?-UG4$5lEc?W#IikO;@I99^Onn-q;1V%zNm6hEtJ5I=z?_FKUw*k}+qH1`NL5FC z0JCQho{IbloSnO$&ycO1K%bHZ*;xTpcz{VyEBZ$5IO6%&S6>Coy-DkB zoPx>%ENP6w-B1hDQJ*3*O#99BAgJrq2EB?OIv1+KEk-RHj$D|GRHddZ-i%w+#1m88 z|L#ndmkZ{xOSFMZ;;=!b$JGmV#3|TdNuip@NfMP-zwWcE2%vn>__g6N22`CXdRc6E z3o&sl8{aba=CNN@seq>@Y#2XFO)*;0BDlNqc3mIdXcUx6Vs%QV7I-eaYqw(g(h~sy zGJ(VBL5h%tu;w!woYP4`waw@Fp70lhGw&0#`u#%(+AnX5fq#+IHJYiYuAS4tJ z$Mq_anDXo?2&IdY0*Mh(FL`=!gGvA@UO9!ziRf6(w)}pW4hnIY!Rpa5=&=mBF?gZy z=Z09;pIxF}en!>4Gyf$JJX$G~8_vd!1v%usf)pva#(k$)$4Bw<4dfHd4irFvy9;Fu z9RU_Io2wS0#OL)QCkM?r(Fo_+JWbfaIP=67PwrbCk6dZtn@oYx#}0lrA#Ok zOop1QVBm3RDQk=5lPM_E;s9te2Qh(m5$7&A@c|%5qJ zCS6a-9R%d}OMky|q3*j&f z9xKbm6y3)t?SH`EB15nwe+&K!4%lm3s_k_LPQv0MyK8uuHnKiWS6iYJWRr*)eU1;w zzX!FU{Plw&PQOpkf$r&mM4sz8kUE!AJsowU9RgcPNI0KR$s(J{V*?)fam0vsDf-7wF6$XKT}& zJ;qx$hIwZEvi(AJ9UESI3W}fHX~~5JebYXV6Dyi@z|Fu`^v;Ze3Lc%X!qA%Ua;w#% zB(#QoE@mL`CZ*P{aZ%;1C-L7e8@&H`Elp{<8qK8jMg5h?fp)@gjs|iQaQc%Fh{bFZ zsFV;N)IP5@Z%$BIR?gMkn_MD^dlPL zo$q5b|7k)k{Q~cin1`2xPa>w3iuEBDH!?Gg3rj=E!5+ zI(?dfYtZa*P>4(_{*HP{$%JGh@^KxYr>SKbq6$3^V_;~oKH1df4(^EB)&(0?9xZ^{0~?FhHq=F9 zn_C*18tP*WEz#yWoK6?Z)-*JVV<1y7dF;hXo^YsUV1_w|NaRO5eV&C}Crj=@6C{gH za>9ho=kECu`iv7FD}`Q#FfxgDV~z`G;M(HyUgUSAA~)MZoU$mygX9XFR$8|9|q3V=RqOS&BEvJ$v94Y0$l4h(PqYuOfc4p6Y z0)6T$9TVErMFX8sN&;^O_k=iV3nBX|WkZKynBF?)K>uqch9a|M^H|mZ{9TJ^TW=6W zgoFl0e&T>L+xtO=EVM);jz{qm5p{5x;pM8UGx-`|E>xJWFsI2EYnY$UpVQ<64O3hk zKWjcN*{+0enKyDN5KQ_?oe1I#YZ@$7lS`J31oa?lxB!7#{z2r#DtD=S^=Sm zfK#MShNT7uawzQqSjsWC@Im?$u*1@N=R)lycE`H`6n2U_j|euvMidd7Pz2m7e9i#? z*fw~gEMZO+=Wq>lq_9#VJR8TC0HdRn&UIGc6^c~9&c1TugO%X(wj0Hn8X&g`5PQkV zz&SVc4hXmC5nA_B^@qOEU0l&{%M}3($d7?2SmCAUNo8_bq=TaOK)+FT0ikJ_HGbI> zcN!U9j3bt|!tjeU9MthathnBM6h~ZbN`i>sO>}}_1uowKPOqeC61c53-%}sb8f}Cs zX6}feAQ&5IKRs#|i75`Iky4z%nKMnW?Z!u4;RNc^QfCeV=}`2#OcA9*BS-^yGx$0V zF~tcMN)`*;x@ZRJ`QeiTQfx~E`nBc6q#J@DYbrnLr|~sYpr`_vOJbK$s&aUyPcXYmC#s z8OE6mrdKna_TZDbgBqPVcgas`%rgutW}CTE5yhnwE+*$xAp@-%&Qv%f*d5|9!}z}e zs!}X()hI3zjBolNLab35OwoSS8#8yEti z>RQR&9R`S^lnyKo&QvDL5ahL}Ls}L6VmyY+3Z}9tO7XZ!C$%L54z5OBpUWWdR}@P; zPBa+N^QV{q5;O{^5_mO` z^$4ag4yMb@K-Ej6RrdI1@cC`@N88w?ILhycJ{Z6e;w z1AS<>-w`v;>qKA3<_7k;oScmk^n7w>7P9ChdP3z{aK(O5kyhjd)yNuL=%j2ElqXoA z1UM|=RXAg!^e|ry^Q4@ylJ5Wn`}t?})Tq#OyWhGWy;mBq!G?hz&{B5*7D7!>Lv+Ca z0MzT`BfZr;@wm#IXD(zH9>H^KFaCr~D^{wbQ)+U!Vs0cAPGj7)l8M>1BL z5()}7N`24;bSI3kL^QQP9|JlUI;jPO^HRx7D`n_Si&a{|@|;V*tk<8ckXtZA&?%G# zMd{Ji^|~>Ci(Sy0E9auOzYEix4J=fH$6g`aR?z0s_sQMh<|&mG{W^Na^L$N*v*6Y%!Xno;NBzG1GsU)QAl$^;Xt2-1<=XG zM>Si$<$~So^NdNqN@%Z6;U)#X3(ymP|LaAE0hmwX2p;NjEuBcFsi8X4RFA(H{-XG+ ztIjlT#$OBmn(^0!zefBaUnBB0B3~o&H6mXF@--k|1M)Q>UjyJ@VBfUkv$T$QMJt81luCFNSkwTpVN1Fgu)NiVlbCrt5i(Q3D&WA7gP0KDLr-fb&-6Li(b^U#nE`~k zb)dB;1${-Z`(-`$n|rkgLDaP4kVG1HdaBZJ=UQ9e6pO-%aYKDHisLD9%63z%2|P+U zi`@rQ3R$#<{1^YdireWbh&R-3Zm4T&Y-(t1X^6%eni?A#qRl+8JJ!Gxj5;;5Gu<`V zyF+o4M|04lEjlM!XoB3_(0^GP3Nx<%k~GxIe==$4rS!jZ*siH55PB{k2Hm)z7?ia1 z2z}CPzk?A*s@2g1)i7DARu=qt3XM`ZKtYZcP-i8`i~1M?eOLmMs^*`T;Lk}8SBc{i zL?4w~4Hm3IGFiYpOq3bZ&xZ6nKY!HVaxJeu_^{n`@n$A~H$_n`&RP zB?XsI#VU|ng4e*^mK3k>N0hVuh_<^JA2~>EG3bs!q&W{4(V2irLi0)Z6%LSE->W?D zUEbA@lIVpplQXhjWe_zop7n8CG&4e2=mXeIy|Xyck?2l7_l`Y7T44{U{w{X5slEL8 zOpIiYhvOz=$ZQx}inuGe-^-Ut(1O|M^Fm^h;nhLcU6h}pX+?G9!rB332(s-vDOU*+ z@W8lq5*A+sNId*cXhxrB5X9|6N*Ed$od6mQAVk!T=c9`=jv`?qJ$YzhBB!CiEXtYY zpXtM`Or3MbJM<1d1hiYwZ9+OZUBQE@2gE>W6!9vJfv4DajBtPOK~E(hU(;9 zVR?$rDNo!fEChgO%KTlQcid)S@Plqb^=m?CoT}H5CMKqmw+}Qz26Y zs}|%uW|FeHl4a{=hFBZwIbpbQ%}o6rt~=!X}|Dj?C& z`ap)z&>TYQhZ`hG$*w`WYSC@aKtdt&Ts7^9w!zLB`}h~laVRq9@U8vAb*FN+?Z)t75I|UHZ<^} zwAP|J;zRIkMWt$fxy#SuroqBdq-$`XI7-U&T={?2Hk-+wB(%I`s`G`DAnl$`h9+fb zaPA&j!;zr$vE*?I${%E8e>KEop1!FsRR&Vp(XRXszlzr=eof^xI4@eN&0q{2YK&yD z@9gBlULYMkr79wBEJ;i*0)X#_lmomLklpxo1R1W+HQOcI zjKFjys&KW>%mmk7m5b-MN_IgcI}HbtHFBeXv*KQ|Ke)ju-xlBtDc=@+*hYOOp3zri zX~dl!uGl-%oF{(huQioQoyBV&$uvoc>U1G1sIV`vg2V`^k*Ds#yCTm}!NqO!z%J>! zS68{yd_$#*C)`6(LZAt=Z2blGAIW0%QRF*<1?_K`(sl4Z*4vo)qoKUIn#+=yEXX;= zZN`b6<_ZgnL=I##I5}dA%GD1Js+$vakqM$DEF7V35S;8|R|0?-7a6A&{zP{QQDK#o zTJESOvul`evXdkRHJ_lw>d+{shb}L`f)u=&W&!g(S1EAz>P*a@HV5RlY1%M*l4hOG zkXK<4z+jxgHly|$0Pv?|rxANNNc{yLuWr_lpACo#%iM#n7z zfZLjedKs?fp)6(%p0vY5fleUpdGMe(vM{Fjnh7f2AGpyI!Qy!OMCH+d=1-wIF0U#H z-UB|_9@krmI_?OgP1wdY3qThw3FwO0u4-jyt}E8A`WCSt5u^$#%Gsnm4s&uD4h4EW z#S?!!@KbCG%~2-Hz-WwZZZJEoo-e3x2@sDmF>L?0T^2B0nV006hGL8!vou$K3IK#^a7z9P~^UAn{DWSli)&pBinK2 zA001yEM;2SZ-UREiS%j7gZN&va}zX4c}N2+7jIjr5|r5$4NLX_c^KllUDC9_Gjs+V zcB`YDHe!@qc>z!3fU1_4LMLe+E5|24FsnhUx8b0q>Oyt69mU@;9Na0 zMua^eM>QCS;wZW3!>GF_{+*edrQp|}q;MzoKqmU!LV{(Na;0=xa{bq2%o-S@hfxJo z-G8_U@dKC);dq?+)Tfv3Sq>@!xX9PC1}qvQ_q^_)y#=~x=n_HXlpG$h_QXyPNO+Wp z>wwD~{s5ve-X;1mlSXOACGQLxs5Wk?Dd~RTC5l^6YGYG80^KhL6JXzL8k?TXZko)1 zdpNae?|6QbRu0&dJt($2xlI&*ZJHe31b)cg>_`;HHo&JbR4HqRxtL%fpV$HOE62fs z@7aBH5T(3RaV@LHn*&aL$g84<0rn5Ni{6!uKz<@f2bVW@Y8qqH;9Hv_?82^)6hAZI z>EpZ~#T~+}%N-I{k($FkvqRX1P%9I2f*nPS*&N8};o3ZBOPS-qQ@w~V;ywLjK0!L@ z+T%b6#V4vzho0!iVoilt+zeu_11zPW0DlIW^USMid`}!c1Vz3iO4-UTG720{Koe%O zbS{LTM7>J!qEwT#F+VWdIJKco#v<6ue&$*i2ZHEid_}n|6K(jqL5dk6jGw0rgR~-L z7=X4ktqwp*@{C7dkYs;~%p*QFK0!XE(z^6c=Y%psw6VQC(9g4LM#g9DHJfmw4t*Nz z-Ibu*fBI4)AW%n)aCdZFPbf2OnBeSbZ{33fm}#&IX9PkaQ`I8bPjQ>JJz>j;q2jRg zIXIw#pkDA*6%#UFj3a@WDBhrKg>KS(RhoI+cETI6mGd|lu3;6vEo13xdTm`xLkxBo z&9E|PY{b!|^)NiZd8C`W1#6s#{3vZ`hO+g+KUD7^9Ezf3ZW+)``d>WM$CE^hdHicU z%V(>7lT@zYG#@Mn_Z%OCXM-4F=NT||a{qfuR|l+RIka4zmtL)pBd?Z&m__6clGtP2 z6v*H7D{!Qvl3|+2%Q?XcqFHghP;37wMz(bPF;qN^d# z&=_&6Cug3)dxSi9k2R;;8oamfyD82-bYk*JSDaIK9+u@JeHc3LjKkC>QH$2eC7(AJwA=*Wpojy7LPORQQg z%My%021G4j={H+upU5wet zdcfE*io!VOm+yibr!}o0&jrP_5 z48DcWY*_;-Kt{|wg~j=e4C`y5XhS9L`e;i_tf3jllE)hBsld}1?Kb!f=1IJZGXf^WW@g#5+$ug-4?*1=5KGlEst}#q!K87 zU+?pAqGgCFep*0;=3=(O@WG_!feg?AF(3r=k$owt9wCPi0m*}i6#H6SE-2=y5m;%N zPTJ=Ae{eh^rxs%o7{^VV`PDoDO3vQKWN@FzqQG%t=9wU7qN8U6k1;mHGS5Bt4UITl z6K7u`e*5DFmRyK+?RQ2E6n{8H*Nn4 zbHCJ0J5Z@_-HUm4iZ743U*V;#F!yJ=Y5P~0`?K7%`Q@8uXZ!M)`_*3B3UmLiph^q| z_M1=YT!BDYKps~76B-)|SRpGMKKHM4xL;jf(YP4br-Bs~N73rCigzFkeLq-P@g?5; zdvH<3X=qhh#YGH5w}uvn%5+j_(UOYYOf4&`cof&rnxz#_NUpV~gwMXV4JoV5+q;$_ zcGOx{@mIJhD}Ty5V-X9zc{!4IEDxW5%G+>buc-JlCM;iC@f5CQ;T0F0hv?}mE565Q zg@tyNRs1u;P~)i;jVl>TNO=BfNPEaStzsNEWfk`_`la&I%gRE*RTYmhwmcZFyzd}x z7B8*%Dl>(aoKf))rz7FqGb_G{Ygu^p!BIrdJFCK4#pf5C9X|8%KBQc5PUuY2j+OFg z&AAozys3yI3{{_5v4^p6jTBIOR(bnJF6GlVNS<#p3@u$mpOW~B zvhdP3-il(Dg(^Oa@eQpzwc=lJEeow*T2^uXIlNnOet7XC2|PO`RDS;bS1@VW1>x$+ zD3WT?$T~Z`_*yn@`Gw)dOIfF-YbrLLiz|kt71y%R`>cz?XY}#AWfl9GQdaSCX4t(p zeAYKE!Oi*W!mGZ*n{#zr(F5m}ReXtgEB;NwgP3Y%p;Om~Dp!|<7F}3YaknI_y13%s zaTB^we=EGc>oB4lA{Bp-=NqdknmLZG8!C?Sx^82*qW0Y^_5nt>R)^2|&H1=-C(F}F zF01&tgj?{Wtm0}ue`I0=OKIOZ#QRMH z4F6f)eVdf_FY@k1(@eizzV(5JdA}~s@Pz=ws<$$1ly5aX$onU5W%y%x_j`bSVQZh1 zKPV-C@fN1^0+xiWIcej!q}6MynDPnCr?Ay3>91f*3R__*`7nkeY%RW0o=VQw0WPDQ zdl>G(+zVS@lXkrcn{L>8QO4z!81K8KT_@fvd8D?NEarXtM;YF;p5bE-Lo34Y4Oxc2 zZDQC4&=|J%NMAj;h4-1;8Qv-*_?*B9 z#PIi0haXS#{?>kmugB`fXiA^|o3!X_SY2W3JJJuo{V?ypvX)_28N>erxPbnVI-I|n z_kSm~{ie*ERW(d`LF$}5#`{Z_FgzwB_}2IF{@Ps(KPdfkT)y&USzn7PnEqBNXHaHi zpM3q-GfaQBp5du7C(pZ<_bX*ST$&R#PEAE^H*hff3B>HzmQhn zD>dKq0MqZigyFR^b3VO__p2^qc=IxbL$cBz3Gn`l2N?c^^iP|N*KwJRb<*DJEBW+U z>Hn*)<9$_>;Q?6%jeB{&e+R?8(*I!@>xj(r_S>2MjMVKrDc-+b(wA=KeWZRFNG)7f`0{QF*pE2I@oGGmX(SY%|4 zd|gHaQxbW;DfiV<|4}KwR_^~%>Ndy~6j*^7C2)4tr}2&Q%sCjX@}Vcu!t&uJj70g! z0ko<-`^{Q}qxWN-ly7SQ&<+Fc8OUiS9&Zqf@&==)%ThTk^`~UIH2oKZ%)|4M?sYH0_xeci0 zO@}!Ww^-#Lz~xTsBUY<~D9>)UH^`L%Tf)2aM7)?t3= zx7O`^{lVZt_S*-7@8FX7aBz@4`qAJE9J0rQH@{E!=2>swiG*|i@f?J!->_Y$em;0F zyX8y47S8uC2X7z6vQbv+pTMcak<0# zAs6X!tBTEdoAp_=E&LbO!>s>bTc2Ew%crcXCUN;2>oD37{<76{FD~D(THb}rcdXA} zj>~tgc7Eqa)^GXjx7IU*xEu+daU7Rp!9W_9dxP&~!`>PE!U!%81Q)Y8e-Zp*4KAMu zzL7BHGr<;)>f^x^Y{plDhuN3k4L%3hDYLumxx+{ZZ$~vG{)gZYKmNzy7r3rZ1nc^7 zITCvJ{kXg#^dIb_qoJ$0#%>LDPUx2wFJ@mXdFFP6OMib4!c*R}65%qNvu*ju>kzJZ zlwGs(?rMamzH&9f(`pFfPJf{u;i~@#B0S@j_ai*>${TgLHc{K~g&#}m_}^Nu5RQG? zs$GoB-&whL;_?~m02}(a^+mKP{Dk#mcJq_gD^s|9);hp(dCJQ1@;U2nPT#+`?jpSV zymbd-Pg^gr51+9<%h*3y(=77~);Vm^m#vr4JLNyNmRy0$-Jw54MZ$j)`s^i$y(5$b zOp-nuK9`exr1AoU+53(l9R0;L2>0H^=`uDPL%9E;-3SkS3+p(1aEv2*=)uhhufLyb z=b|ZfNo_8a>;GLXN_V1zyFMN>GcFhO5+%9^7Fn4V` zDi&VXz_D8Y5WDE&*KrghZ(^5JopmR|4gbXa8^3lw!s|hI%TUvDP@Ea~ee6dV{Wo8Pz>R4QH z9Ho?Jt~iA74Ha^^rDD}uUFNF$kRG;Q&%U|v80)xZ9bwExM{5wSJu8B6-7v%Tf6Gz3 z`05P^FBxY4ZL3;>@Umyv`t5gJh_H1L`>ZX(o@hUXZB2ZOJ=F0i!!GA$j!@H~c5bimf^W=4>-G=bW=|+TC zee5cP*KEKjNsq4C$=<%G@d(1T4{;^0`yRvfJt2e_fAJ#-BfsY;SKY;0Zn$DK!i}Gt zL|FaDWe972&->b^(Cgt%fA>*@b-&w&upx-$z;BeVc^g}Hv4!tTyt$eSr6tE!bYFWb z!t`gj)?WA4D-n+WoXh{(pWlpd-;=EfCuTUeCqIYR!&A?_4&n6Mc|Wt1tvh%f`{7V8 z%enqPxQ-708E4ZC53^o3{^N~7Aa~i(W`Vwc$yR4tGa__dj!ajJ9^|3Ns-fO)=5cYs|)jM%{(At>A zHte;WGf5H24J?RYCL9}k^i1^+s<^%`9MAvAL?E?)@Uv;>#0hGOr- z<-4J>>v8#B=zb3M_d}=g*$+ZDhjIB~=qo{7{ynt%a*PJsamClzCr%YRXzaZQ5FP^H z#<1M`7KDdwrXR63u&eH}&gBHV+xi9P)|;)Z9E|&{9Qs{~I_s01PiK#Em7Mb+d*{4Q z?#5hNH+3iO*FS}}Nxnxcn_cjy*4sE2K4J~9=N~GAI&>iX#j=|movre%2a&M&tt@ou zXO<#73f44ZouU&!CmayKMDSh19x9=fU&m*53;bg1(%_j zy-y6E7TsL~vbEo0ebB>{B*$L(GbJ^sMUHE2s>Z#oboweBL z%lF-ap)0@nXDCzh30E%Mv0_k{bKbW(~xUP4vK>qO6%O61a`XD>hd3im;Yd(C7u2tqS)Hgg*)rfHH zdwlZ)*7UWwe9(%#373bhKcWjT&uYeS`AcgHK&s51#kX+AExT(u!qcv1)>S81i8GUH z5uWvTixIB=H&i-&-uuo&b=Q2I6^adV+HdL-SNB)! zuIS`SgbiP1lN%pkb(^kgL)iR%me%sN|F^U&fsU$3*H!nX144wbM7D%%>`D_5kew!B z39GUxo6}h#frNxCY=W{0BFHE+BCE245HR4#q6i4+pg0KQGB}{3GlPtb9vsxk^T7DN zuWnV+eUqH$Iq#m6@4NL^{k8n{*U}AL#pZYa9HYq7qnL*3`BF__uN21izQbDe`R+wv z-!GDYzUv$f{YEmML<@t!lT@-D*#8aIbHFqjU|_>I;GnXVz~pglfrDEv01j!u`V8Is zJK(VHtn=`+IlvLSXp@HyZ3B+n!kUkQ{m@xkHv`8U%>j<>@Cfjc_*~$)8(!e}53_+2 z+V=)dx{Gyt^wu8WZw5RA^fwCwrrf$0n0kz(AZ-oCn}u=!8AdKMg~Im=$m~y;14# zIbA5>I9;M+8q2%?vjxB|mx(zm*(rH7SmWXu+!)MG+^zE(Jp)eS8GoHkoN${4nmCM& znDohdU}_6?Rpu@>WM<_3zy)&H8qj7rF&R`MYtmESkbb(uSvlr$&?j;_o#}6~BPW&b zWE0lvmW4|SU`*@9iJVq!W+3*-uvli{A zL(uAIPhgvV=yfFx`}ac#H%z4EBmUePcuyhx+S6<#2U64m8m-HF&4Giyz;qTm8(En@>)jrXSFCn-%+j&DVx9?tDLB z%-IRR*u<5<_`%zNEo)B&w%UlkQ29lT?1pem!4#(WhSh3yj_KOoW(n=Pioz!GdOUXJ;Q27ZtM$;TFued{2-^{=sZjSo|xBu4~z|G z{&9Vt08ZNWu-0!F#|#^DRM3v0%}3LdTYLyxD7*f{^CZSm=&2gdL0d`gZN{ab+off| z^|C<+&^FnV{<2f1nJF@&#Ucor%;QjKvk9H4RJ&ZH(dV=)2Ci}bMdbzOA4)dMt6>ms zk;j-~tNbtxv`s#_60}3sk}K)6yJgBa7gTvj}8Uxm*?rG z2W9;X(5v!+`#^t?KI*+DH?{#Cma+7$BXR&5j&B@8IJvwo-%AI*DWhqF<1!LP!gpuw z<3T57EbM?;xCSl#j@(a$Kgy3;?E7*l2he$$*B*317Gs9?T$F3sqEF-s*7H+Ymuuc- zd5d0rMTYeNeJM}W23?a6js|@#W14`j%fGA!eJ{VI6W@}TI1l|KcT;#r#?z<&E6eDr zPg*q}11+`I(F9Lh&r)HvHI<$HJL~vD&sz*AtMv}2wr$p_XF%JnHzt5~ zTG_2ZCDz-F+h@JSxcyc%`=QiY$y^Rws~I|C*)W~z$XZ`;rs}znzBKPT>ZGJ$S@gWL zcs6m`^USrdGu@-8i0vzWWh?M0Ir~A-TDi3)Xt!L4>B3QdjaAIMN=KUQ1O3@W-Hu}J@bq{$7TD`y=F>Zoj@ox(U0}aUj7@wCE%79cU=IB=B7p-M)C3O9 z2?wTcMOmTQ=cnO)`k)!W{LRd5#*9V4SrMFHW}of@TqO5XZI%4tWzh5TmCc}y@)B38 z?b7Bj*)8Mxf)2}wMxax2-g?j(`4-*iZFvOqkm{IbJ?N_~)VkTSV#Vx2Y1{^ur}$d>b#1r?)sMqV7JGg1NJDJ1nfQKAt%?s8MN}}aX8)>xV9?3WsAq5*!m?- z)Z;r%1f4A;mXhJ)71StX#&@+%v(Rd%&Nd*lc7;u2ZPiXD_$^FgQNE{>Wrax(4w zt~?(OIwz0Bfc_-AaI9aH?{TnRk~2}bXIV(=`k<#g-c-;g&l|9os?yytm?=FCH^%`Z zzD$Nxcnjy`7Nw?viwYdhGH>|LxS0j{!i)c9p6TtEIJiBoRMa6{JLBcuf*I|zGlZ9+ ztkl9R;l&R+ke|av1x^euyDY>{(t-kh#1&-bq*6h@<>wR$^($oIEy5*8!i!tsvk{la z1JQ&xGs{1@06*~cXJtUwgd7dr1z(Ul$I&qFQ`3=*zc0znPDjys$PnOFr8qgJ6&4CF zFA>1cwULyk1VK4<`jkw_oggm-HSeiuX$6@xO^7#1n|IjDyyoPgFh@5xHN601;s5(! zmJkwu@DAs(e3~7?Knr@9Ht@mRBx>N#=to*UgoKFHf*2L5060j{(-EOS{a%(&#rM+s zoI(R1w?3T=(@%N%DV7f*AyTyd1r@^Fpc!LdJtm+22>tZSFL|c^3ARtgCt%d@+3ipz zeJvIk+5&4;dHI*L{w1y7SToy5+nMs!9tUBJF2N+G{F|XZgoL=ME8M_DD5;Z&epQ4a zD}D*6f5=@vCFlR};gjf4dHqdxhB0A^{|4wMYyD)cAEWi%_19v7Rf$8ty#85QKTGSg zfB3lVZ`!{Eae?}!TEEnkuN{v1cjM1(zg3ViiOK&$EgwQcT&Sf;)N!aBSyte)9DzXn zt6Kl6);IoRbTBun$1wI3LHeb&eJZ}RwjwdiRiM#xVuirc5~P2-u1`hX#>&S>o52YH zUD=7vkg@)zKWm2j5Q3d_L8U5G0mgntvKudf`bV_>5v||LB-HFK|By?+OzW3v{lB~P z-Q}M|Jo`uw6LGa(3PJ*`sJy?OP(}Zn@cVe7sf_-0t$+Pj>R*B`+i&!5YWNKsK`TEC47Re(FcUl7ImCsZU+Z$`hH zOU|@>4A;bqd3RzQOu!C{k2_y?+D6srr)d5D{kLKZOlk! z9}+CDfqjK9P^8{%SjFrc0wZl$$Lt4!<+X%a=Y!?7g;~FY> zFzaZbl8u?(tdGI+aIAN}K#_X4MLl8Gv%pAO)E8!*3YIr0Uw?w-4TV`(g5?pytQW!Z zdxTjBg5`}cucrix)VmFDH1l>~q%E2VGam=bn+h|}2Ftmdul(2|va%2oTSQeOZ(faD zPb#ihTg12|PS6&y)yU&2$vLhp>;$gp{gX++`5{Dn&t)R$VT+`wZ2z{9GanJ=3rgQd z%M)Dkky@Vbl23tLil(BmUe8!RJ~QzrMP+~31Ubun)|Jo8Dt%?YItzJK?YgY{UW6guK2fEP$U^@;V|# z@3+kwvO~+=^G``N`5b~gCLmw)`gS$)Ppir2Mm6#~N?v*1vr*xy+7$;m?GvN@*6i0? zLLO%-7r`pz^w$E&<4mRjyh_RIh>x^CFGiTpHgJ9T zdA{zK<&Idqs?zH~03B250|ff@t7_8Ugq-#X*Y+{~QwDiB<{7u2hhY6@`bd{OLm_AS zHd=0KP+QC0`P7G;{k7ROzco_wD%QvJ)SMju6rP!_&YBYG1w}Y=V)A4jrsN-zgu9P% zjJMw}GBOJ?r{Iu_OkAy)>&J29IB`i-A@bue8yswqmxen6GjNY_f19-Jij4V|`Y`A^nyvdFOh>W8_baRMmnhwmpR`+S3NFIkemled!>=ilNu zk+gJwdSS7$3GT<@@n8ZK%ASHF?OBP69%B=R%=C}ay_1BqKnl?{`Nc(r!MSG6&Mpd; z=-i#sR2ewNG<$k*qVz&l*}-Tve#$#$I8OaC-3}Ac55}b8@FMjyU!0SdJzbv@%%oK( zR7cjBHu0DI>IPI^j_F(%mYrLiqfWYIW!M$v)}W +#include +#include + +#define GRANT_TAG 0 +#define REQUEST_TAG 1 +#define RELEASE_TAG 2 + +int r, cs; + +static int predR(){ + return r; +} + +static int predCS(){ + return cs; +} + + +int main(int argc, char **argv){ + + //int i; + int err, size, rank; + int recv_buff; + MPI_Status status; + int CS_used = 0; + + /* Initialize MPI */ + err = MPI_Init(&argc, &argv); + if(err != MPI_SUCCESS){ + printf("MPI initialization failed !\n"); + exit(1); + } + + MC_automaton_new_propositional_symbol("r", &predR); + MC_automaton_new_propositional_symbol("cs", &predCS); + + MC_ignore(&(status.count), sizeof(status.count)); + + /* Get number of processes */ + err = MPI_Comm_size(MPI_COMM_WORLD, &size); + /* Get id of this process */ + err = MPI_Comm_rank(MPI_COMM_WORLD, &rank); + + if(rank == 0){ /* Coordinator */ + //for(i=0; iQbyszDbsbMV^<4GTwTZ6wpk)QjFBsSwVC?Dn+ayVafxuJ0mZ(l^3RDEP1=a;t z2g;BV!rwM|!mGM7*T;3y=31fimEc;+`=Cw;Zc{hmzqy+Bv2FZYp`Wh^ zZbOXmZM+29B=oM*7f9=UJ~t%yx*dTf+f+_{jp+Bx)x38R-jnv}=dX4#_1ri*vZtYL z@q(8{!edwy6M1u zyQ}wpY^(FZ5C8P)efR$7NqBY+{`fmtT>|rQENmZ^(`r~2-B%X$)CSg*73$1Xe#fBc#DE>h9F(BE%o;0fEf7=LV=`LPZxkIz`& zyOv&85mw-&imu-se z`Ilclvi&EIcb-yl-uJ)ull#7V#jX{XUwiLWpT7OKix-~q+pbaeU9`?=13ny`NitlILCL>bELmzj&g3BBmGlzq+dHn z`WI0DrG&I)mm!Dudj_{B0SaxMZs6v6$^YA9H3j*{b^6kR^e-aaE>ixNbonN~DgP41~WbUQ=YDV?0@ zj*m`^XEOtPMziW!(I?%#Nhdizk_+%AogE*NoA#0MfzgpGvl8jc4jz!3_{7+lGtK1b zvB?qKjm?Y>A{T&Yr%mHi;%v8MbYVt!m)i;NGc$$$gC0 zGdeSVaAaKC+~`G#ULA#AC3R?2VOr#$%JDYJypy?oQ`rG|w?;}<-^d<9%O+=X(}BsU zk@4Ix`jMa2{m5zuob1p*ZU7JVOi!zHB%vEN?wc6PZX6q!8krd1xOXJCQ4a~RzbR&L zdd3+Z86QFa_Tb$i^uo+^b_kDIrYTK*l6jFe7wG6pw#J=UbqtM`pMr-V@T7qZ0|@{S zU}*j`*TVZ2JX)%=&zv=aB_J4hmf7*U<>brcN?c7`Y<>owxt{p(wVA*Eb%yUetji$| z*F`fq@Tf1{U-M7-(*1PDCOr+w*W&hy!Ked$~S&F@FPbgqHs_ku6o zzn1;Rm+oIgUh$=KZ8g8n8(yk-;ZKNl-tfhWCrxS~aIF4y6?Wj*+8YrrId>cG7~jVX zFaGElervB}oL%?g(-NOzoL%Wt?61;$;#)pYeH&_ewm*I7x~Zw;>+=W%B4hzqa$}bDcN*^f$ek zuQs+Pabq4Q$hIu=0`ae1I{&V{M>$cpD>I7y^>c^WeT!V^U`lZk{NV0zSB*&xk zhAq2Fks-I-t-?wDk1YjNiu}i(zVyW-c;&?d2=2OzMWBtnN3Z^;&Z9Grci!HQzXa~T z-FfuOFHHUQ*s-IDKi_cmp98s59=i^B`-P22dW=K+LOt%#HNPse19`jsB_3LZS8 z9=xO<>`)JG?f%VYcJ%l6AARZ%KR^1^6R(_G`GuoTTaQ~$AN^|O7tq)N?FMI{jTf1L6-kVEqx)(V+Z>_(S-@WzJVflRGmCoC{(Wwj9B#-{KtEcm zUi$N~W51X{X-|giz#Of(ec@8n`J>2y?te+@x*j!jtNAvRF~_Uc7t{w|bU%0mnP2!l z0%^-vp7aAN?tk~>Fn`rc&b<+zU^k4e`EJ+Ip*271yuIr5pdIMCeQgCVNPnU0Xl~7K zx{hA8=9SK)m#hKwztq%K`FzXKza)?TzVnH{lq8RS=Y?(H7rx^QQA-I`ky?z;7=H8q%3 zO{}NPH;ryAy*^;2wz-mwaETtsVSTcP2S!G-Lo22FfvK5sJGXCS+Mb-6zydpF9~{Z; zv$KZ=26Ll_?b`JzJ{ZiBXs`p}wL_KmA$xO`y>@86iXApFkOMg++qnswOSZq znp{LEA9fkt-&+W{*V9h z*s;fP4J=;TzW9s_mn=9~ab4hovo@`-U9*bG%+rRyA$&tpiKl9vl=VifdNDT!3E`2FC5W>c;9=Rehzp2^2iT)2doN!%cuVM2%U66j{iZ z6@KTN$gJ~Q2>`Qo`)dP%O8^Dt#U~bR%X=qSQGNq}I%ri4K7>oKeC?IEl$O^6@`F~{ z_d!twgQ08Q1oF5v1oj{htOz{Fe(2 zB{Xmm1wo!zyn?pIBuVA}o33Jb8E; zA0DV?^6L?n{O49lu0mM$ASzPwryktSzw&Iz&Psw-5U(y6e-F}24HaZN3_hkTAFjlg3t9LTCSt^g5P7JmQ+}(3E>4-p+P0{bTqQyVW8rY z`8ry&V08x31=b2wD7d<5!G;}(F0^VTx^2OuNkkXv%$y&qbf zotkoEqf4H}AeelYE%`ohqKRFyWMKlalQ`bNySD|F=1_F-(Z4~|vX(vzXb=ABn2M}K z&z0WNh6Y$*=uWcME?%~vWbyLFCs`+3OUvHg3d|T>6IifdD^gKeeT!LAx&*1oWdOu= z0ba^Z3zRHAf59e6D_@4lW=xEVW!8cPOtp|@-Xb?k(|nBjGOJ{I59OuiI93QotxRiJXl%fmSS-o8^Sxd2Mp&9PfDpMNN(}AE*Cvx zzV385gA?P!BdjATb8v9qz?8a$m}Ov!$ta2wzJDoK}jZ6#>u2-|(Vv6gVS2 zqPl9&3>Y&7rZN&tJvg8tcVAYjkF+ahvNP;P+)fTmjhW=htkeprE->+a2F#PnjLJF_ z(~cG%s`uRp#{o?nLRQ}`J76X^F*cB!V6UP)CB&3lpxdBXe@YfxFIMc{d;bF!H{jpz z?%(}DaP6{S{j!R^3~mgzE(=zj`kLKXeJzW^*HnL3m(!N$N@NmFd&*`su&XuW#N&O* zOfufm6&{RKS65fslGxSLfw;{EU?w{dZ%#~&?VOFUsW)S>XUL_8X6auU7iWLHm$UrAKe z*0y!A0%<4H*Pn{p(S`t~eQSSvI{6yADcT$hAU(lKI{gqG*T$s&cz0$TGjlvU1THv- zhoCW?mP}7~GVbh*ceeC78KOC;=ApmjGow5P8v(PyI<+=xh|yIXcS$y9p} zx~j{L*03A+DW|<9&F}Fss@han*U(s3SJPPASkqizA8m-%_jdt1T$$ypz&mJChYHji z&9PW*ZDXvawxOxMuCcMcsisj6W^aFM7wXy8l4%L^T(nN!iOqt{JGYhrN!$dHpmH$Z6s@FipqkAldVnzApx z6cKcGvKw=$E!n|WqXlD?-kr`Qx(kL%CF12BiN17F=GH1czKfYnqU(7C>K(rI!v209Q<-mmG}g zprfM#yt)o-S%<^nXsAQB2|y>Y0LHd6vCFREL?fujd%AnO61&i!vjCrUO2jz@lNwtz z*SEDJbvz4wljF1}yAo`O%xkB&t=CDU+LA5ITU!^6sn-Ehgj?OBrg}lAK%7X)B>Gb5 z=y*#e(b3blJ3Kf(Fy>9hX~)d0LFl*kPD~vpP!R9p?HxL^v}ZUsb(rHi4EY;iRDmZj zNRz=;8dH&e35;W|r$_bx(e4ezfin`$j&8f=5FteR1kD2e&x9e73p3bgJ5H*-4VXKP zNy5()S1RnwVPpzMGVY|~EvfeK@B~)AoHH_XC;|$JSKx1FAP0hD&rB}sIN>nhO=WUy z+)obun^!9<0~5o;AW9~N!^At0?nHNMqK`%HnHd?)LDyxT+bV;ta|Cv# zGd;b%i8df##{n`2>LNmOY$zo67GiJW+a@O-9;~znksYyUgULU=Z(=H^u{_aoR|0q$ zqv|hCtpQyIf`P89qfO0?wb8of`r7)&SZ%bip}r=T-B8zD8|xDMDAbs{|4XnO_F#yIZy=&|Wp^bYi$54v4(4r!Qj9 zN={z~Vhb%hjUW*|G!e-JOcdOm68* zI4!9*C%v2z zqFp4ncV!G_sg5?**EQGG*4H$}VzH*i`kKb(#%xt>Q+og)r%(tdi;Bdt72%(ci z!-?j1oZc{I+H@u7+q8@4ds6WPzLey;A#3)KtWCbAMd=##;n!^rK!5Ii`Fo)zXcj&-5iz9hz*q z=>Ea+TwW^H7%*ssD7nKCSOvDnl#z;Qgn?mGi!IluUF@r_g!C41YdfgY43|{FH^jJx zN|OHMr@(Ha$JGb3L#Q;DfUqFi$;zs&Sl+>y+3ReseVhxROH!5g$}KiP*QGQ)pkWeX z@o+Jkll_1xi%RshCEMH4s~pJ0E)2--wwB$rC$r;P?&@1!n~JQiJCp4iM;pw6?)MT2 z?>k$-FrYfN$$_tvR&N1jPqo=357MN2VcwxeRAG0bV>1~P1#K6bGF_E{>CtRO8 zCebkz>*6Vt)5K|NhpWIm5DNPFMNRz{E+opXqPH*6m$=9yJ2@2UiDPfx3?8G>-hj5M zB$N#_=-6AgV9Y?NR(e^&q)hQi4LPknJzx+}gRW#I0}xTvh8>O7lDp~aN_KldE|qk< zg^v?$$-YE96DE-nf$}Xk5rOV*0JEPdRL4QZ2Kb*I4fv=m#Dd`XUIot161mlblp5P+FjsWP4tM(0eRA?DEZIn+ zPFgPzu|`c;Bzw>eO{y2z4T?t3J4$UIj?- zizqp2!U(#O=}e`qZv-fkX&D*_5>Q$4U#KXcNg7}z)M`v zySp6r`<6qYNqjw74FO0^bF2vhhnmKwXsn*So~>#m6J$7K@WkGtY0K0R5?S$0K%22> zU1MESZ9`onXG~v0q&aq5j~44V!sozVU>q!oGnhMs1uZwYFAVH}b{O>S6;c`4mzx;P zMjMPQK{&}cga}2DE*X=2oXeCGK)D_>kEY5x-Pw|MF6vJLI8wsm5i|~k2O@i9tsSVe zx7y)7m6i4db{G*TBN4&7exX1BglgJQK*9qn!HY96dT;=8V@3HIX$)|2UUD97BIGda zFh_<*24RDt2o#o{NrEU+q?WAhG8Qf;=t`}G7vv;GA168zeMQ;d4sur@1;}RWJG98G zWHCJ-F=aYIa}zi5hneZ}xRCO-^n=VTWO2zqj10Ph!=el>1QY`^qgY)$8dMW$TkLg` z=I4V65I*@5`W+2(c{M$Qip$WXthU`L2<x!2 z4mgffiEklR(vENy*5X(t!32`f?w(XnrY8l#V_(ZoTS;Q@id_>UZd9Z_<|^*}G^rnl zxxlN~ZAj1$$%oyMcEQ{)@K7vAPrK9GLs%!NMY_=^uq9oUC#@xs!WEai3i>Tp=K^$J zPme&eJvA|rLn)rnM~QrPrg|_Jz>WxNm&zB2)Wc!Ux(p<(-~~ss5Q&iEAip3Ao%NN% zPm)XR>GkobL)qyZD5}Wx)F3WVeT_vXNa{Nd@dyOckW_+pJ7R-p1ssAYvDbrZ!K(x@ zT?9B+AaAm2ydvY+!1R9Rg9I?jeEJjQ92{yLkCQ*<<&XLDtHDI^BS4XoMRD4cCh-|o zUewuq8x`_i*hD!HpN`-?04r}c>ykFv8#W+LeCxe!uO}zUwwd~p>KwTgud61h*u4LeQQ5d=+vMIbbg3&slB*OX@wE!&VQwHtn)~@Yyuk9p< zT3h1VK@Nhw*N}~J*c=CfrJ<4GVYF%=C!ogz9~_v1Il1D26$U~r{TTpm7>r`s*s+?~ z$29MPWTuT}LymyeAbcotm?nR#SKEgJNCHm`3?ov-G$v0W@+Lqq?YL|yTWGjt)Y05R zw(RZ&Aom;Z=?6oJkYX<&9L<;F%>7k5N*Yv7~0B3PlO5C1^JN5O==pCX$ zwi_5nR5C<2q6vui_wgYH)Lm8G1=f3~tq0l}N-lt;kaZZ7~_vt1KC zx;CO07~4bYh8mmz1wBr>KQ78GR@aF9Top&SsJ)IN`8Uzsd8ATX;?<;e#DBAebr~pQ;-DE*{k?W}bUF(P<7zaVK#)Bo)H!fP z)mD<}g99^r_i<$rnnGvhQsj*BG0+7BfsjY7^U|Q+AnHACX;Fez@jNV7@Vfa%cAUkr zVoF_yhj^Xf8zpU|ZUlCW+)KEzKpV8&svkM=XX8!3h>+3@QQ3-2SyR?pJ>ZFdJS_nj z8z8uNXIPp!G=Y8sJ0r_6l{=i+Y(ZN9>w;8Izo&98^2{aSuz01@Kq64j*8~n?37?oeFffX)rkRUGCt;w0 zsCguBLb2FgXiuStKiR@IC-Il*?iFGp22>d%rAnkRoB1r1Gs(Im@^4YsbR~A6snFkQ zY^9_~oY{R^js&`!KYTzLEGQnyp6|CRhpG-0}e(%kc#CiG!=lAg_6UI7+#S- z63Wywx>+t~ZCL7oUwYCB(ZKTiEJ!P1ZQkeE9-tC44tZ5~4HFy)+(uqaB+)L7p$tmw zKzH03nRc+zVB|nHj5#&E*TF0lBOw$8DLNLWg(+N$*IN~8st05mIgIZ62bK$>HjZlNg! z@KsN5It(pE8}ApvD)8Y`jm> zn8nq%>mh9by+@fLg{&gA7a^;N=|NqN=TPT7h}Bejx|8%2Q6=U}5?{`Qhle7=Ll_k> z*D{MF)n>A-)A4!NmIiVmz`PNR8R24-5^T;MR~m{2(4fXhL)BwpX=r!Aj%2GyH%-A> zk^H#rMTJO|As-nh<<1e*Bkqo~dII*%$&prP4qJwAwv3%hCtz#$flU0CbT5>t8A^A_ zZRPhktj!FSj%q1t9h;T837dc1Y^-Qd!Jk-(P>Mn#q`$@7k2Wu&Qvw^*;fOsgR%v~e zg+L@lY1q$c!wrLb^$24ghK!X^ziKq`M_1ll|O20l#{Dl{!nBDWc}DX>`BCleEiwXxw?hh?X6m>NmY z%v-lgNX@X@(MIDYvk9{mc4-)D7*(kYz9>DTWjFy5?>ks&hzz(ny6K zuLH~utPId-evc@F?7b^raXG|d3T=WlJ6S1*sL@G^;-d+ku}cNYn}8$ zdsj_sZ^HR`VT4PkGDpGNIKi%JIjKNS%jX-udVz~p1;X^7) z78lFMD8MFI+x(_Hl`@?1oh^N-6VeA$8VFrp!Bk*F+Mp-xOSbmI7`m0H9()8BFB*@J z4ji7C0XbHfKxA5giZE14eX77$w8+usW(bzlAOrR0L8J6x{&X;lwKulxa135tp-#+I z;f`vChrNXtWK{1I%!#?KYI2B()m?t~O-$^E$#AX`iCiWqnifKf$Te&TD9FjNk>vmp z8t4t0qJgfM2Bo1yZvcJ}*FcR3AaVV(EKqrg-MHJpN0jI*-AT@3O%}GV; zd1a_y)zHuoz&?#`Xt|KuZu{=>p$@+u&$ZttvJ*X?nvh~y!OY%<21OtXX{NU`&@uyz zq7sI&50nT&uV48Ra!*Dk+6_e>3B^E#>hvV^pZTB5$ZAd_PUzaX`$G0b2*rq(NifO< zFTn?%pl!;eX@UV%Et$YCt&>{>keyrflakRA)5nsg$avVcRPD_wzg3C0^v`@*r8PV=Rrg6oy+ zHS9}8tJpbspyYc>JgeAbLMjV^Y!+KfV8;fLxI&doA)hO+c@jJnCLQDni?skbzkFmH z*aL%X)up0+5DQ$8(LMYx_E2W|Q-EiB@i8c11auZ3i7AVLW@7<kci77$n9NY>X0INqLBc=;H87h1EkM&$ z5;&fDKR|;x+-E1Dc~-F|fP9ay0l}!~X1mE=FJ`RFC3an6Q!S*i%A-vu$WG%;d{4}+ z)uK%+1k?yyX$X=m7zVI-4Qa~$RV6}gK|^eiX4Il7@tSM4TV&}}tZEUXM)d6->{S~t zZr12A!^UVJrtN8kRWY*ZIRQhIU_R3_n%8gl>BQYC%kWXzhP4bTY>qW)Ftg7~V`kyu zU8{Yi#0A?zJ`5Y8)cmZeRus4ixmmNR7W!NQ2YOs7cf?#qYKO)CLa0tilklrj2X0lY zbt|FtrnG6Mn4OuF#Q{wPAXoqhYO~|Mjvb1i(quf0asXe@V{l*6hkSXEu!Ct zZj6!@<(kRE2wG&r#Zo5lY)gC!jPm9$YcK*8Z}A5bOt{bY@9Ss%%Z*rV?K=45%T%19B%$ak1rCoxS%+EMcWCconCM+X&44-gT+y7AWEg7UC6Ydk&1%TNL27OtL)j5*->tv z5PV!|uSMNb$V>b{)QUDK-oeHithoriw~;y3E=NEGUU5W9>odU92tI0-lNhkRhXcR^ z4~|W`o5i9Ln&5Fkh3-nvk>+{%C&=5qm~lJC{XGb;YD2D z0!)NJD2@FJ^Jz13FexHa$+Hr{V(T#)VkL>kVm9HLlt_%i81rN->whUb4uYYu9v&aW ztgH~fs_N)H!;5(~F^Y}yJ~TZ5#dTf|F>X+dC?N(LpfcS5RHslex>fXEBJ7~5_V^kR zfS}tZ*GPx0m2K^mfv7#1uFj+llD~H7``WQ1C*2L8RU1>V;AXlY#HFMRM&Ei#<+_XI z3Aj)80SPuw%c@Lyyq1ZA_)y$7h)7U!GOP1xaXaiSeXOwXYz|ut6W(s*b(bfsJUWRD zFGl-gifK`+$T@c6i<&f{O-FHM4=byUd;prty2r(0lwk<@z#YYTw5rd#cW`3za539n zMZpzrO=)+y6&oF=gt4AB0;ohJ3SLTz%b90|hemr5m-OlBwWC~AIh*qw=|zU&1o;`q73!(v$-)0X01my8lvJd&r8w^qx2{w5C38wG+P;TcM`SXv8AjjY<>IE{)XbQapcZ>P;}le1XH{{B zd8Oj{ok%R^$7722LH~&m1>)L?{aI2H2f|6(e_^%2 zde+}XmcqS}Tp}EnoS5a16RYfic{USN-k5z?x(=V0)Yx!Zu4zr#jFwt#80GASQw^WIG;ol3kXS;)lch1 zw1Px6JLydaxDSs&zMNHns-}Yb)bRs<#Fl*jfB64F4`7r$@#!qe)u^?Lk-4+oU?>U~ zc!Lvw*s7pBXJ2-7GCO6o-#|^OTtyPo{OiET^ax$TgCW3fbnrmh3~UUJLewKn<^4^H z=5Ut`cSQkE<;e-cpkK*I9kCtR76@k)hBu-@!w?uFWZ;nrmVjWxxsgIMP*+zni3BKJ z%m|O?u7%|Bz=?BmD;=n}O_B=>>M1;s@Vo)1J%MeUeR>9CGdkQX9e~3nZt3gQCbil{!t?bv+MohE>RKY!hxKiAsfqmC5q?m!CTFFEx zE7Hk&S*)N6+lfku{zM5PNx5hb3+f{J;_>Xk8Zpd|XeDLX=g>u&FVuMYSLO5tl!3~O zZU$#HDCAlvHnqNrA*i-RSyfeK9~_vr_u=%7f?dr{s;Vv%aB*h~(MatlV66!uUB7+!5$qLPGc6fH^r-o9hg`M&kj@eaKCRLcXq5^4@(Ij~M1=n0p`go#so z1(Mz&;npX9G1@WpocME30$w;ig z*&S-h_bqUE%Oz6;2uZe)p22QkB6pz8t~L?mkohuvAlx|tX0dLM4PkClX|1q=b_Yl? zoLLWIGMz-*CEL)%mxiYS(_7ODrM>w)9w&HrcMC}{#~FivPCCqR?e09$Km10DhC$8I z^%VXKc_xx-8kL}DwNXj2Zl%GgJNJPW#g-cS(*K#s5cR)sSK~6YV6nANICP*-iVd+i zSTjFifuWfgAD;oG06KYK3^v)bDJ7i)W1#bpVln0!E&u~FYafr^Xn+XS$|$y3sUwjz zTk>8w7DgdzYiSaQ{FD|Z$;K2^!1I%diWxV1dA@JNZ=iB0qa4=JYDU>D89^}6t%!lO z3p*lIabqQp5|m|$B4RMAkWeZbM)t-8+LDl+V7Fa5orD5kz*i|+!ZndqnSEJ1IW{=~ zr&QSJXt!afQKxi|9X<@VVFP>NH>7eE`;lu8XN)L?i|+9?J*)^%83MtB;{F8eJDN|6 zByU?TOa$mNBoX3Em z7GphB3A$4m5wo=FVIq{?$`8G)bx_Bt? zsHwd?aH>;=i9KJLcu!lxmbtI?a0(v4!=64RxuDlx8{Ik#FpwPpYDWUrEqAX_xC$=+ z&|_v5ArW%IR_l<@h=H8ve1Wsu)3q97Fhv3vvaLs8AgE4f^N_f#K2T+HHpYO8BsR88wa@Z@8tZt)BTqcRt984R6~L~G8$Ip2X=a)vU?@PRqA@R%FeEl4h| zD9Wd!Nu?Q6@#;V!3dQQ&_44S}oz5( zWJo1QswWNseg=FbDNJo(Ly^3r)yL#qv_oF{<5j4btM_qGG2bDnpKRX^Jux;>24u~h zrC}EeWcF@(0nT!-QV3 zr4KR(7|6P6C}o7o5$rC5 zp*eYog|y|gi$rO3i#myb1&ftZWzfGNv~r^3aA{M^p2KLEGM^}=t1BD z0d|FoO65CGJI~XPL2~xPQz6Dq4V?%IF#X}Hqytu(UGNVoeWaap1`LWJSZIGHdZ#)# z9QZ{|V0F<_QDG58Fj^EgRZTT&l5yl%7y4bhaAKM`x3rwlo{u8#3r&T6mL{ex;u@#G+TNfGfR`_7O&$z|?+=dNY=j0thb$TXwG!wPG z=pPIzJ)UxaJ^6&0I<-ykb7d?nj0hbTAp64FYJ%RdwULJ36az*mLzG*Qjx=@_h;C9= z=3#hc$~V41>$Ke)E3L~04WSa<-1r!u^P5IH0Y64+tFp*?@f7GmjuwIB41~27qdATi zq+ti?UNO`$pL5Gb^`Oqs)zZ0X3S{WWy*Ly^tcynWXK~aY$i4heV`z?ejh)M=WL77U z0iJECay3da-EOE|UANhpxmpwZV}unA?wJ_KQj7`Knt(;k< zh#fI}Y~&oCbQWs@RO=Wty-4qX%Pr-@PWDv!wDiC$bg~|x;AslRQ-h;QPXa{k9>yRY zFO;L&S%B*Jm^|Zki9Qp-81Y52czUx;E_ax4s!1Yb5dK3pA}c8$Xw2(-6c!I zJ!SxxEUq_F4lFr@kI_zX)rKo!O_WF1<8kanPVTnoV&s5GG<5BioD+w0q^NX`XLwi! zjPbGE^ECn*lI1_Lc=YQ$ZH^V9K>0v1j?(eyB=>&6DXiXS>xY__!x zH(a+c8L7&qTU-@4DZrCGz5iWEmY4J3*rip#VsY4D|Kl1FJL0{ozo-VzlR}C8tKU%C zwHi=fXZ)t~7z5hb6uc~(f%B<&OdH=c_TboW*OVuZ6A_MI9H)e|Xb~J-d8@9E<}}t! zMJYmMfD0NKuCrS(ed&?_2${HQ_z?BY!j$tFcb?N*LB!^Bd{1N(BGvclWc|*c18o4>l~KBpJc za&(*%4HLR%86!t*^%f4w<$?k?h;*c&--#7}ryy7D9J$mk3x$cPQX}S}A@d2?Fz+Ne zo_A`4F?wIG{;M=GvbtJ<%n0UZE}T06{ULOtxEKei;vULP z;8<4%+FQD~X$??pJhBq{Fd6ggG>QqlT!e=H_oQAfVdy?aY5xOJ7-fe=MPcxBaL``U z6tUMHJdQMslCi--?x6Jv#aa^`;H*R=>2pX(QNOz)Lv~J2W3Z3zN$u{YJ1f`un76@D zj2T3xEKs0WHRFm~t5rSRAiRw+=JL@1>cAIs+*XDn7iEJFv>;4dFZd<84iaug&ZOY;>{8Y!C1!ZtuGs*#`_G=MBbguH8k z(^0Ij^g7BF%cB5wZ0?gDP?nN8z;~#UMN`~ekR-|=tr$^yIj$K#6TSignptUmBDLc! zvU=s>5V=xy9;1UEMPs~Ed(8d-Znc&kf}==4_RG1jlOzGDUxI@@`)QDN7D)rF_@l3DzLnK z?VY#?74{Hz1fpbscNdp(&}`cgZQ~AN>EhU>SjEr|3Nn@Duk;7{N{*YN-!-+WLoA}! zb0I^O6AaMwAj6{7bv4mgb5mVIU2UwcDcV?rGv{L2s=9h{4P*+YV7|~46i(9&_AsXl ziPC9@&$p24X30H1g8a~N&W*77+&wiypIqXTq0p}oMkdi_Hthm0xI1=vFG@eM4;(n3 z)1twNu`$^8LEt$tg~kXPEN}?|uB*TcyLP>i$BtnQE6AvijKMY#<%!u9oZ&mJWqt8; zi#eAboMpfY&d+U)eksu!rYq zQGx5#p@3=7n8?ov5SYCmbj`vy)Z?5JKf_Q1ZyH{%ni`X@4*Q7m^X2C>`C@gm^Z9d{ zd`-o&c^M@eHVMs<&15v$ihotLgY7Z-inYRP?eMV4hh9+z0`9q9;z7=HcBibtia5E0 zB8c)a*TWrrUMd3yU};0+(Lfy5LhXu{q?#!^J&nO18v_`Q4s(B^E1dw?gK^MNLK3Kn zFr-52s8?EQAcwLtz!o~@7MVwH0?GhwkS?4}VpqHicwmQ^{fGjD=XO#RC;Aa`RX(o) zz-8+_m6r&j3UjzSccidlsy-XXj)I({HqZ59;1!BgzcIfwQ8tk9^b;7+rZ5Q#WGOJz zmvbETK?>>=kQC(^ILe030^zzm%niXb9-{wpmxMI(cEtu`84%y2zUf|!t5mx*3#?f5 zg6QAJoyTq(k&Rz_#brlm5{xh=y`uOFY$VhPL9BS5TwJYCLZ9GGEz|U*5AdNSO_RWF zt@)n%khY2A%4ncU{0w1#lJ@hX;7d9m0H#bYaI8!Nwu9rNu6hG?X{s@2gS0EIU4Ta! z;Rpo*i$8oF=ak~O3#H8k$z1?j8ghJ^L@ItsSD#o;fa4yh!p3vMz~?Tf5AuYs7gPXH zCR-Wic%~0J$p=ODl6#b{48QI-Q90)sN6mGJuC@q(28ajfQZ}N`Me~8295b>z-Q5!J zgPxSg!4(N9AGmlM$`+pysL|KxbOjKUN4?s%Y!AhmJ6PBAc^?gf9+@5Oh{tvPedj z%b#$v=61IKIycK)H`rE$%4(B&cZ9G$D~nnjo2fQHLrd7Cj%ZaJk8vU{lbe>TD8&;u z9d~CMD0F4vsE<{UR*Kb%C#r^|dN#y~6fU0>$5)NDx>BqwhB*%%klL0l#hx{A{tjdC zH?#|uV|$brBk=j+U9wz z^v(jaLGhA$5>Gk_Fos}Yds1EWsiQpeig%)PKekhcr)Q|KB99hPx4DrVeBQ(8InUR~ ztRs*Jfq7QMLTACsd^`CIYFoj}z+-|;T*#1dNZr6Btja{WrLSx4IuSfmcOQ1sz-}ma z5_GYxUO+}9ii{f5217+-C9r_5;S%rVfj;)z@1hxJccL$3735JU`utoCT`rsRGQYQjZhYX5`sAPcGjCyl>~NKNc3W?Ot7SEN?-9pG`l;H{R%8=CL; zdk#SF6(^0bG@u9cMiw9zVomT+bnk$LB<1A7sR+-`u9Wk&AxaQt4UgdQHHAN6?tJ8k z@Dg-aO@X+)C4S@M!JRfp4Vk&NmT51%JQ+4bwzUFjw+#GyR-76SR{M$0CfzyK^oj*}|l zHzD5(g393SCo5hI7ZoMxoMXwux~9*6rqYfBCTcf(7A>j$A9DD#Ud|^==*D?iNx13c z78mkrW&t45DcB69rETv1e`LU9^N!xui`afI%Gi0i~1J>j?P;Jo20pq8D`oDSh$%7(= za2_a4x_>XXndNci>J*=1dF^4IEa-`v_LePe#LJJF+UD zgsC6zV+Cs29UhvQf}=|w>QLxB+T%_o=BftOkqyvP_=7od~^<X5Gv`Rb6b4*BYkuMYX@kgpc`YLTxN`D&4`7WrzC zuNL`gk*^l{YLPF7d@jjEr8X(11Qc=75e=_EH32oi11OEYAqMBORBOAKlZi0X zrHAFMR-DSL{Up;KE8t+y2q_`phwhdR9{O{ry`?oyHUs2yOJ7TO8m5srwN~b1uen!~ z5FAh&PNm?+Q6<(>lFi!c+J;yZ&XenEqfs1fi4(UQVhxaN%DL=5q>?Y##mWF9biH>; zmE_u@*Ht&y)il&M)YUiDMPqdh^>ua8MjqZBtK$(z9a==1>FiH!S2F0~X_)L5oEc62 za)@5vwfDa;BN65NKZ1Qk5w(vVPhsXMM-+(jesvmwyr>Tf(8m!lsdDyt1pb^9Clxu6 zK+K3~n2WFCn0c~c*aH(@Clvs#y8f65h8dN0utzUSA`~QCPj`vL#<8mjOm(1I;*3k|WLl(1)Lcofti<`O9s9{DZ)DhhOJbatV2 zYJ?G)dYm@1&#vJBsbko9hu*=5KvW3T$O$Wl3wX%kptunAZPY99waKX3t4GI8;&noK zUm|9A_i_ubsr~eMT0h~7fo0r7~oww=a+{z;<=d#;UP6{_ig|MpHc zSE+x*=K~>3NYa_1-GxyK#ii_P&VioR3q@J%>0ROa4DJi4%Ec~6*u+8a z!3(AKP!(t^7(*{>i5Sh(%;+fif7Fyp0Q49 zz;u!S>|~bQnSd*QKmv{dB@Ky+`i|=cb0LShwSwq};1r?-0V((RNQ?l*6trIkq+wRz zOUlO1;EUq6dSbh%$VJ6$X%Uz!q#;IU;V9BI(N}^IwL7~fgKgmuZ?N;Av`fOaSwNjH z9EbMwOcOLk&du5GnJp}gs<)!25h$05;R6vUiaaL6m+Inhr%k!$eHF(_{F=&XNH?@p zZyYfkr`cADGfsAJV$YF|o>CPNPmkn@=JNK)XUgLvsA{zlTO$c0F`+d(j^l!}?tIiC zXCC51oZA>Nsk?q*l8vyi@#!)&Q2gdLLUcdq1O8VjVE|B$s_j zhhswT93ICJWbn6_FAxD9Ffa7=gNd?7Uw=G+2VMUYFKy2_OUn3vNT|qy%BmwMUJ2k`QNMwA?T5G!+*PuRG1-SujMa19fP3E*nR)`P z@&*BEhw=u&hpn{o;n8#jTXne5!+Ci}hG64g47B}DF&{1Fkw8sa?1%FO9Qj>?2_?ID z>H{!%fj>f?NP>&o=DwZMldo=&rln!ZP)%fFV%5Suz~oo*>pzsmWTY;%xStvSW4)@0 z2Nx=GBb=o){s)u7xXrlDxb5#Dn2jII4&bzfO)6I}rA zF)lzNo#rWTimnjXFj^`t_T=KzMKmjV&w!U8;yOYp{=^~)5FrADV%P)C<)6@pMgBWuuV>uQE{%*;@XbV^K zP;i6BcG|_DAUiO;976FVVfMmn{3q@gNH>sPBRu&0OGE=&YJ=*y5}YJBa(uEau2&{? z_z<9ls8Zw2Xi>abfN|B#(y~a*ef2F8Q=*3y%9hZmeEbqP4d0GlPxGMMcKj6cPO%jU z3rNb0^;L770E>b-O~4dcF;FIk?f;eYT5cwqad#4N%g~9rs@<@Gl{F%Ch1rX8ar&T1 zeZrX>u8kHbnFh#2-|6uvuB}&_mvO|vXPE<}-4mgqQZQ5IRa~OM+%w;yuyTcBHj?O4 zyfcAPKuVQGpL&{njWArk(>+kg|MHRJ%~gF`nc66{(k;k1a;x-jU6oBjTza(`ir%_9 z`z0j-$9snqcx+%-q)o?MM2X8uc$7cQOJq`i1hk5 zr@(65dW|Z zCWF`5e!ub0Yy%D7NppG^g>1_ue!@4Q$be9=Pi^?>h7sN zCugRp^z%j%_j zo8uJMT;Ri4qYq8Dd(Lgp-aLaXbcv9AN(YTtTVjWY3Ox43^>bwoRgi<90nYGlWXwlg zp3o4BYI&BLYW7Tt7>X@lO0b~&#jN*=^ni}=)m4OwJk4{aVDo%Q&L`~WNNmSuCC9;m z=-K_WEKq)+NI9tXn{z>ZRIcKqfkF={at8ClRSiIWAk+mB2bW}SUFP;^ZOOkA=szhQ zU9cqxN9ic35^i0ol8BfT82dKqVQU5L8UYrd)PyuP=U{R?#js5sni|%^u92Zbr1!D) z4_j37K$(#2mxw7tGY3WnzE{Z`$h&}cCH=;BL+-7LclS~b27Q~mQwCNYzCBdxh!Xvn z`(|vs;%1PIG@x+u3h-y(Mw?l!kMEAdx#yhtxkni(3IvR7@yjXI*KKeaPKC;gD6Qdo|S(X1O+ zR@ZNYuva*?vSoK$%WfQn%pIdJ1rqL@#tX?_DzNl!5WY?776+5hzXgoH9#LNh~JY);wW~yVVKbma+6Ty}G8UE{6RNjj;Bwug4*ywb%fF zlSP}mgyNh>W%8 z_tYH_a<#vUbQuLrCI>pXR| zhwBu9jwlP0_Y6#9Gg2|6&Vd(@@^f@i9LEh@&x(s1%spAc__Um8rVcU_g9v$s#)z9d zIkXHO9pt%t=D6$#)JZ(pn$~QRQ&tj@+b9(5w2RpZ`C8v-VW}v#x}nYx(<>4aGgBCC zQ7z-}aiOb>kl&L^@fBkjVf*gI4V_-IK`D%mOhaVJ(-ev-?3`n*2=Jsh*F3_skyeS{HBcES0zEI0*QQnXd+>@6v>4`uca4z&-(Y;G^M_e5`P zhqB2lRLNI|vD+GYC={w%87G0Q9Zrcy9Wm9Z#TKeqQ>?bG0n?y9*3?wr+!T$$LtPWM zP>FS)&od}iM1eVuYrg*s*(l(bJta~m;wFS+9T2#Gjt z%_vGZET>wl1Zf~p(xjt7?*z6YlW_2FLjE7@H|FWDMfV#^o$R&8*=r1Wh;Ngz##TU) zfILOv`8NXAR>Q1?CeyXirlwe3BMu*r)z{KoraszbXdS>wypv*pfOd|N9jCNZMeHzR zC|s+$a5NV599<&6Ec6+Iig{cSUeQKbke9*Z_Nr+Z`dqOJ$y8c#p>cPEhO268aK<)q z482F?s|@8l&)G*~fOcShS7&G-AA$w6N3pqwz(CrERYgd4y4w{+fX)#(-mb-~xIxdi zZBcEWf?kcv=M!%Uwf0n)m0|zV2eW{nW)ZG76KMV#AEH(GfyJ-h2OnK&7 z8VK^X{O?gfNx&+Z7YZ%^#5C?#l$EcZkL#1c^71Pd1OlbyuSZz&(_lsUXL<9p;Jk8c z5z|j%SaM^@{E||gR5EWtc{@`}OUv)WwPe-8@()R_HH$)L_O>Erg?T%%7_l3y#pMs; zrnKxyt7{$$9b1Cr?Mp)EWZ!}tdujPQn6PAF`A2Xq4K3YvHlnATRQ}J5mj7D9$Ce_k z{^au2Co!#7!iCF__JFmld?#*7%dchh>t&~umX^#vwfrH*mIOl;-#&z!`3uXxz)U3z zPAmVrQ;@Ly^ztv`S{hn$>oB5cpHcp6MoZ2;Gj#erJxDqCtdi4BJC4btRm;m)p2`nJ z5tc+wFYjP1R3!yepHbF!_hvqwkUU>zSh8?MdEhkOEIKQYFdwkH(C1A0I$ zd@rAthQ3wua0JP}EvYGgo;lAn#r%i79kN-*=?qIwa(jMRw4`Dk+8+ze+kOjPT2vdF z|GrhYSyC5T@cla8)R&YrgwA-m5BJL(%Qs5_ZtMCO4V6!C;N>&c)i<&DrRz#Vo2-2W zUuwdzU&ypmnnUv^IiVJtYLu3oaen!7e73aY%uVG{xjAcdsAB7_Oj^DrwBSB@bH&!s z{M3U?JLiJX{53h=ox3fx@O9gGXSbA(%d4weL-SUb;R6fMwB_;8sqX`*l$_aC{s}xT zImh(NKQOlH^zvuqr45PlKkz10^~bldw6jhxFJFTU>vZ;#^=FiyjfB$jOBt4&V`kCK zjB;|ehk~b~(Ipifp^Dn0Oe{ZhEiWYtq?b!e1EqmL$olS^7@iND5whOV%CP-rhEJ?y z*eZFhxSjVet!CJ=h2cOK!%H4!`0)~k3jmlQYfqBlUxN()axcRq;5%epd?~|UuVYwx zC&Q~H{S9y7{iAPScvnBePXOvd))!_N=77;cR%3|aof(Fkh8TVa(>r8+51ksaesML! z&%K7>z$FZy0^SN)JEXKzujG9hz$Ik;RNnn3DXpTMDH|skJ|N%9JjDA2afasr--oR0 z-^}pu?|uWAE@a(*nBhJtdC?8L$6h~#*WAJIW76vCO5T4K&=ayQ zl=N{Rp^)`@Dfx3iE+Om3QvdCe^DbcFkhN2KDGEpnSs#>keNJli2N{=VV@zKy?RwLF zysv%>!^!y!U;bN$_eyX7qr>|JVTNzcGWdo0xL>>m`&C{8y>%lG~W_ z{S?DxBMcuMXZW^ihUdPIVc&TS?~?j|@H*aKAt{f2fcO6?WAvDe!c$V(?bkE?JgM71 zox=Nnl9bz}CQrSaDW_h<@Mi*J|I*C+2I+yL(gR-?2-B--fvyvhI;Sze9TU*`rMP zrS!u?0{=f;!<1`E8QvzNc8}EI0-$J&@&<;>1#*5B;r(x=&V9G=esTfBvtzRJP z)a_Gg-XD?lf8Wge#jOl4l9D%H&HGdThT%KjBu|GJUMndFWxo7G(uZYS9+G!iKU%l(I>{_m6WAC>z@rEagi73Bm@I|*4i zey6@W83>dOteZr*=WA$T+2ANfqHHLIR+VKxT8(h{`=!>$c&2L9I{RHMiS?<|)Ae`wy z@01;Q<_?4hOD{%vXuJa9;rlt4u5maLud_b*ATGCApE?k8B(^nx|Tj(W-3&$|86VpBuEvc4Hd?AI2X zANq||P6&G03ZlEp{=*vJhkkE0@%48FuV=r#Cs;+`dpP*`6}UVS+(ux2EV%C7x;M`l z-+_eX4a*U(*t<=qeku56cFWg;;f1ZKx!r#tAxIMxO_YR$f@S^kfAAx~(F5HfA=AP>i9#~IMI#|p0U%h};xMlzY5W4oNTM*u8t!EeB zWR)@RE!OlPE^n~H?D|`+&1}X!)+=aR=p)t-`0^*M@2yZm_dCt0$-}$+wYea*9Fgg11?8{-$~iD)yRjrWs$ZJFjD4}-pE=nVp2DUqdhjHK zi^~XYOYW&bxb#VO%}Ki=2v2^R2yNN21j19kUW@S5D)!N7?|Km7>F)$8kjmI3WJ4?8 zf(a<`zqgKXo_^LEnvcuptdC%}gg$Q#vZ0SzN6@CwxIAHn2)pAp7*&QW! zp(3F-l{|btVs9_m44fp@8k~L;(uXR~MVS5ebqI$`iJA9)d?CVp9WjIl4(&pC@Ogl2 z=+JfSqQf^gBfRpO%?OXITZHhc2UyFiGjBwA?VsPJOFy%_3-NQ_`VNHWevlAlKO053 z@;QR-s%B2N)#n5eu33+Yh1TB2v0C>XcF}ob9L4bGSbF73&d>D&%)j9e=OBzM<1DQD z+?fcgzakUp#~ikr$aaL$V;tq!Gc2w4-yMW?4-wDS|KSpZ4Zq^xHGYigP0Khc%^UAW zc>Y~G5pH^jy}!Af!+F8{({)SM{(_*mE*wJGe99O)aZ^8Q6F-^viKA>`a%Gdw9ol;V z;`0Rr78?+F)v>tfD=4LG;HJX}uP>L&>&myR(Pf_c6w*WXo7p!j-@-bsI*B-D^(9pZ z*Q^R7Tsy{a-TfT3^Ufmxp8t0C-&SV!j4l}X6L>}gvn~&Z~tr^!tVb=9GANMZxHtUxDR3P2RKUURzgufMI51BfgXgr zqlA;!^xuT=;{JMsm)y+0zpMtMB#^hNioL!1;B^Ss{NxD2wQH|Jxb6l{r}K{dEyD2d za)g!BtmXQt6$m%Hg(DuRTY|9aTY=gY}0fF1J}1u%5SD zV;r8lt?#zt@>Xka1edp2|F#*Iw_7s=!+Wjo6I$M3O|Wu*WBrMJ@J{RbQe5t{o~^~@ ze(PQi{=2NLSzI2l>~37%ZM~B{{-E{u*W>aY>lTjjd#$geaCykOjHSHKx`>syI~d~& z9}1qqLHO5Tf@Ab-@B?qf}j$tO4g|E**mVdQ5e!3zTlm@fJZLEhQV z4%+v32N51Vj7Om>-+wp4BYT*BomIlFy4|{nFW+HZ%#Yq_UCY6EvsDfZAaHrcI|)x` zzJ4Xbvu6+pJC&cDuD=0GB(g zK9+Q+6=5NFSz%u8wq9mmztMURUMPFOy8KRD6wVLb5?sQLJQ{qOJ^zN_okO_X8hnV; z^S0n^*Wq$|a4dt%9l=XE)9(!K=H;$n702lA;OJGjyfL_mUHhhB`YpJ;IoQD1TY|T; zuzP|l(af?3gNxsR%XfoEF&~O9HKF@T?kUraKJ|%Zc=fCa^sLOu_!>63{ljm0KMp)0%gS>PHo9ud>HSon%szR(;4qaxMe*-<$}GFI>%|H zoHi@w&*=Etx0E8jo?i}axE$^9zCZiRp{d3AlK1^kZ09`0&;Kiisch4JbZObsg7@ zzn4RJ#_#4MTyYA+v!6U0)m?Rr6^cD}7Q(F`Arz$F{1C!jYfzQYWjD7YyuAJfgjY?! z7UAR8FIn^x)@kp;Crn#pQ?A zO)UN2tba8#=G0D%XlVJ834|+teLljo?|2)+b1uFXq5X$Zge%|A3a|R*EeKavbAqk; zGN3B7Hpefln|cGn^S;M-!x@H^ONe>a-@%dJ(8xwbKE|(CeVjd6{VT%O#(kW8HFvPP zqSGfKtUHZOuD^!OY-nvo*!WeJ*7RMbH~;=lgy%nd7Q#)>R3O~k&Zk?-SlZUtaV#(R zhd9D*-(vk+YFJL|wtErAFL@8bwlA`tiRJ8o_El^}hjkmm&OMa~lY6g2c;OE>AlzO8 zxDR!`$U1l51Dq8~J{d7xO~tm590DM>qeIIMeAP=;qn!0eFT^9Tea`Sw+W1_csKW6IR|<`iDAP-d=it0+)MBx3e+tD1H24T>hrCnnV1~($wj= z+*f)#JMw|jZjSFKL)UOBekSZMP)T%HWQYcnoi3MJZc`Nz;T+cA3R z043-Tt#W`X1%aLWgDzyS9|W*zLS^F$JPXyF#-WMs=l5#Qy&hrx*$hWF6G$e0$r{ge zk}x>*@9)!PVQU`ZyMM+ezUCQr(8YgdBQ80GKsm65LzP{@h8zgiBD~Ie57GI%td>q( z9pE)z<%*>fH%e!#r0>0x5Hvq0`xKjki)GF@*Y}L<^ ziR$%7X$jn;C*%S4>p6P?FX?ZQgiLTS*YpCa=%0ET8REKreIQ_YtKB0254HM`bUxB*{bXs3 zTbj$ju>1h?-W-4FX4S~&wuY|#d=>f7LH^24z{|XZ?ED&kvmS7S+sItUcux!@e$S@v zFq#pRG@?Bi6DGlpWLv}F##n251YPo>c*%D{+<^sGj5)!9GggWmJE6wo;?^6!1x zRf7H67Rq@;+u#IzpxGh-f6}rV0T;ABn*rZx2WjeD)-oaiEA{Vbn0M$6cLSc+(`k+! z(jP;0wpaC@K-=qj#umUEdIlNuExmIV;Dlb#1<<6gfX9fI^%=1MjDFj0104{GQ5W3y z?@d9vTNPQpdvkx#9={{s4I4%iDf}feTGAzIWkxt^37T*XWr8M7p@CVPPy)K7nwHn4 zH)=uG@MY+}P~2PmW{QX)FN;*aoNT?ulIw=u;{=U36-0Rl$w>BXvq7UKt^wvZuXHlQVrQ?Q7$*srHPm zI%wu+6F?^%m;^d;%Y4vDZ^wa7z8A}-s55^{4btvr>SaNE5@_M&DWFCDqGX9%f5=37 zd?m?c#nSS1SA8nz%vZ;Q-aTg@=&TFNL1&k>2c1)w3|bmX4s>5r80dq1*)YIE{Audb z!+cseU>$G9q9NK4+LziF`(!j|QXbiLbX*_Mv|dy`vzXSO$+c9^v>Iw{esw?4xzos6 zi|p+{@1HUibU8msidJxOid)H}sPn71>rq)xa_?Wk(Zre3IMdl?o`aQ)Go>wWRyE?5 zlO-nd)TPjJnD5#OILiCo0{DdIK&5DVkM|dYk#f2OG&PP|m-ex;?M40~s6p$zP*#}#Q{0p|f_X7K9>y3~WoIzK}PQ$;XRdg#aB}duGmlD+T z%*nD)_ktB*+!8}mVZcfZrVvf~oQz(bRtdVv_!pI@jDINE&UqNW$m<6H4)JPQ)L!PD&~ZF*Or^!;6@E4k@H$T<8yx0WvjA`KtQf!%z7BT4D*P>Z z>^uA$5_p%lqb=nmzZcUA$J5MsKojr11Mm?))gJIi{wB5a44+Di_~-l#d2utpG6L`= zzeb~Zk@uSp_=*oASN)m~hEHRpKO!f-$`7Xie&CFl|KSt+0Dk5l(h#iHCfo;jNLxlG zSgTc#zy|H;M!-gm(EvQ94W-m(tvkupX+H%4c4{Xc0qoK?%m&nJ<^2JT+P^99IqiMQ zdtQsBaoDe&dJu3(dxlakYaL)ZF_6KRXr;RCE%K%NuRyopwqHn|m)n-QIBy$iEe{kd%+_l%$3|htGQ`Uew5^2R8e4SdE5K9YE;(2P-&{VQcQWf!&hfV?=HjsvB_(`lC zwvnGkfsTqNJ-3e~M;)`i6KKjM%1zBePi$$kNyFIHy+PB*w*ehj7Xq4B4VMfmZkmVq zg6RuE%T7{%7rsEFy?FXo(5k(oL09neB=#8JwHNRtPumW7h99QgY8U@2Ef)>E%^1KT zzP2aeD1U`k+hcq;xzXGF%^GRZF#AX_`iOnA@68=EjJVMcQeBSw9tTaBPZmpDNrN@C zf_j}is|V=tO|_sSKcqQ)`{*f#R`Uw#`+FRYw+VhA{GxBc0}$+gfEMamadScMe~lDw z;-5_hZ07wN0o!?KD?lAD(E$7SY4YMmew-S1fbUxhILaTOS#yl1lbzq=XBPub@H2M6 z2fRHNM9f(h3^>i968_gJz6+qnmXZT_*0uxI5>4uG7uD76crh_c|2mYV7+mVtwJ|15Tlqq~>#X&bm=EoQ3GY6%La>|RC1MfyapMez~ zBM0AdEXQSkUI`cSJnoVl5|FX7k_sl?4`z-EeDsGo3h){&@=EDiGUjj>xe7dZ_10CC z4_TEmB=DJZPfoQVq2hD%P>f#Hm|vWSs!O2|#35=iH0G9|k1VS=?4_b5rKrr1ou8BE!Cd&i1C|NK@dx)Xg65QH0A`w3 zpt9zG#fi1XpOWvbIgw(lw`ABw>L!7Qc!eQIndL`mPLV%K%F`NZ4pw>cGORx>^=E5N zq!`PV^2bC9i-SZ=ei4+Ou}J-J<3_1!{{Y=7@(1VwSdjrf@{-Lkw;498milX@e65sk zl8UL1WII)VDB=|8yg@}({n!&h{;#sgUzYNhr9A!91_hGu zfIrD*N*+6_u&dJlV_PRUjQxny1%-|Vv`}iRIbgr?k`D=XitLbJqtp=tT4;!jDSQHH zYND#YNy;}#`DdgbCK)#TID-~t$fE^vfw)-m2DBQBt?HL zLnH(evy~KI+Zy#MJ)i%@1K}-}C0fyVQPW%FtOC zruHcl8`j6956L#OL|kXxnA%s&nL6vv)PCX3@4?hQ;LY!ebv@h65^)`;8MSVkGj)as zVqN`}@5R(Q>s_8s^S(i6axt)E=?uTk{REvw_~Ft#i44HE2jE8q;79xLXht#=;^|mEdKn3;QRXFH-hi$R~kCP;a67w=_vVaEdCZI zI^NaC|KlXzI$y>JJ-+@=`;6U>Khyrv8Fp6fp|b>qT=0Fpgt2+x%cG4^P|{_Bk9DJi zQ*hL>{kY;={Av^Ub}4Iy-2wQ&7kbPkjrfTG{Ii1ZyI%bzKzR)f_SfHb;M;wxW&OeL zj6*NR1ivF|mj0|>idznT7tF6Oq@CAD+1dblwglks z0iVX*F8xi7`)|Py!F*T#pqln-06oWL`2>sKeh@&#jn& zrCMCn#PU29xJIF%z>$X+dncq#GhW+tv3$43U5JYt+#cNj;=%>r3-F-F56gu+Tkwv4 zX)eA(mygeemb-E)s~8>>m6f=0L8v1cUrL2$KZRWM$jW#Cg)1d1Jk`v2WQDJC;y-HR zY9R3dOQghYcV0#D_^HsHpD0>A4xc_q7q7{?WFP32dBlxxk-Knp9K9hdzIsa~W=u|N zDV<+l>MF`vkY7Sq2h&Y-Ew#{{I3|W+E!WstxQ%#x8l#6|(t<7TS>v|WNn^#^q|8dnWq9f6P%VcpGMsA)fue?(99-mO6TeQHwIU>~X35#6Qr1jHqe?>V= zUshRB?ybvRRb1iCkvfe!gl632S-ilz5H)u^I*M0LXH3R@SZYjR6&mCjIk$ezyj4P})&7HSMM8v!4 lc&0c{r0^y#isQMXN&C2BeC?2w(Fcs) */ +T0_init : /* init */ + if + :: (1) -> goto T0_init + :: (!cs && r) -> goto accept_S2 + fi; +accept_S2 : /* 1 */ + if + :: (!cs) -> goto accept_S2 + fi; +} -- 2.20.1