From 2eb837fb7fd1c5790db77f9a79de9d556754fbdf Mon Sep 17 00:00:00 2001 From: compudj Date: Wed, 15 Oct 2008 16:20:33 +0000 Subject: [PATCH] update verif git-svn-id: http://ltt.polymtl.ca/svn@3111 04897980-b3bd-0310-b5e0-8ef037075253 --- trunk/verif/examples/buffer.spin | 41 ++- trunk/verif/examples/buffer.spin.trail | 203 ++++++------- trunk/verif/examples/pan | Bin 102109 -> 108893 bytes trunk/verif/examples/pan.b | 76 +++-- trunk/verif/examples/pan.c | 31 +- trunk/verif/examples/pan.h | 97 +++--- trunk/verif/examples/pan.m | 400 +++++++++++-------------- trunk/verif/examples/pan.t | 233 +++++++------- trunk/verif/examples/run | 5 +- trunk/verif/examples/run3 | 5 +- 10 files changed, 499 insertions(+), 592 deletions(-) diff --git a/trunk/verif/examples/buffer.spin b/trunk/verif/examples/buffer.spin index 41965dc3..b04b1bb0 100644 --- a/trunk/verif/examples/buffer.spin +++ b/trunk/verif/examples/buffer.spin @@ -1,8 +1,8 @@ -// LTTng ltt-tracer.c atomic lockless buffering scheme Promela model v1 +// LTTng ltt-tracer.c atomic lockless buffering scheme Promela model v2 // Created for the Spin validator. // Mathieu Desnoyers -// June 2008 +// October 2008 // TODO : create test cases that will generate an overflow on the offset and // counter type. Counter types smaller than a byte should be used. @@ -20,7 +20,7 @@ #define NUMPROCS 4 // NUMPROCS 3 : does not cause event loss because buffers are big enough. -//#define NUMPROCS 3 +// #define NUMPROCS 3 // e.g. 3 events, 1 switch, read 1 subbuffer #define NUMSWITCH 1 @@ -34,7 +34,6 @@ byte commit_count[NR_SUBBUFS]; // Reader counters byte read_off = 0; -byte retrieve_count[NR_SUBBUFS]; byte events_lost = 0; byte refcount = 0; @@ -80,8 +79,11 @@ cmpxchg_loop: tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size; commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit; if - :: tmp_commit % SUBBUF_SIZE == 0 -> deliver = 1 - :: else -> skip + :: (((prev_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS) + SUBBUF_SIZE - + tmp_commit + -> deliver = 1 + :: else + -> skip fi; refcount = refcount - 1; } @@ -139,8 +141,11 @@ cmpxchg_loop: tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size; commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit; if - :: tmp_commit % SUBBUF_SIZE == 0 -> deliver = 1; - :: else -> skip + :: (((prev_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS) + SUBBUF_SIZE - + tmp_commit + -> deliver = 1 + :: else + -> skip fi; } atomic { @@ -163,15 +168,13 @@ end: proctype reader() { byte i, j; - byte tmp_retrieve; - byte lwrite_off, lcommit_count; do :: (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) > 0 && (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) < HALF_UCHAR - && commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE] - - retrieve_count[(read_off % BUFSIZE) / SUBBUF_SIZE] - == SUBBUF_SIZE -> + && (commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE] + - SUBBUF_SIZE - (((read_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS) + == 0) -> atomic { i = 0; do @@ -184,10 +187,6 @@ proctype reader() } // reading from buffer... - // Since there is only one reader per buffer at any given time, - // we don't care about retrieve_count vs read_off ordering : - // combined use of retrieve_count and read_off are made atomic by a - // mutex. atomic { i = 0; do @@ -196,9 +195,6 @@ proctype reader() i++ :: i >= SUBBUF_SIZE -> break od; - tmp_retrieve = retrieve_count[(read_off % BUFSIZE) / SUBBUF_SIZE] - + SUBBUF_SIZE; - retrieve_count[(read_off % BUFSIZE) / SUBBUF_SIZE] = tmp_retrieve; read_off = read_off + SUBBUF_SIZE; } :: read_off >= (NUMPROCS - events_lost) -> break; @@ -231,7 +227,6 @@ init { do :: i < NR_SUBBUFS -> commit_count[i] = 0; - retrieve_count[i] = 0; i++ :: i >= NR_SUBBUFS -> break od; @@ -272,8 +267,8 @@ init { commit_sum = commit_sum + commit_count[j]; // The commit count of a particular subbuffer must always be higher // or equal to the retrieve_count of this subbuffer. - assert(commit_count[j] - retrieve_count[j] >= 0 && - commit_count[j] - retrieve_count[j] < HALF_UCHAR); + // assert(commit_count[j] - retrieve_count[j] >= 0 && + // commit_count[j] - retrieve_count[j] < HALF_UCHAR); j++ :: j >= NR_SUBBUFS -> break od; diff --git a/trunk/verif/examples/buffer.spin.trail b/trunk/verif/examples/buffer.spin.trail index 93bb3331..bc2446c0 100644 --- a/trunk/verif/examples/buffer.spin.trail +++ b/trunk/verif/examples/buffer.spin.trail @@ -1,102 +1,103 @@ -4:-4:-4 -1:0:120 -2:0:121 -3:0:121 -4:0:125 -5:0:131 -6:0:131 -7:0:131 -8:0:131 -9:0:134 -10:0:139 -11:0:140 -12:0:142 -13:0:144 -14:0:142 -15:0:144 -16:0:142 -17:0:144 -18:0:146 -19:0:152 -20:0:154 -21:0:156 -22:0:160 -23:6:0 -24:6:6 -25:6:7 -26:6:13 -27:6:14 -28:6:18 -29:6:20 -30:6:28 -31:6:29 -32:5:30 -33:5:35 -34:5:36 -35:5:42 -36:5:43 -37:5:47 -38:5:51 -39:5:55 -40:5:57 -41:5:58 -42:5:61 -43:5:70 -44:5:71 -45:5:75 -46:5:77 -47:5:79 -48:4:30 -49:4:35 -50:4:36 -51:4:42 -52:4:43 -53:4:47 -54:4:51 -55:4:55 -56:4:57 -57:4:58 -58:4:61 -59:4:68 -60:4:75 -61:4:77 -62:4:79 -63:3:30 -64:3:33 -65:3:76 -66:3:77 -67:3:79 -68:2:111 -69:2:113 -70:2:117 -71:3:0 -72:3:3 -73:3:28 -74:3:29 -75:2:119 -76:1:80 -77:1:81 -78:1:82 -79:1:82 -80:1:86 -81:1:90 -82:1:92 -83:1:93 -84:1:93 -85:1:96 -86:1:80 -87:1:81 -88:1:82 -89:1:82 -90:1:86 -91:1:90 -92:1:92 -93:1:93 -94:1:93 -95:1:96 -96:1:105 -97:1:110 -98:0:162 -99:0:165 -100:0:165 -101:0:169 +1:0:118 +2:0:119 +3:0:119 +4:0:122 +5:0:128 +6:0:128 +7:0:128 +8:0:128 +9:0:131 +10:0:136 +11:0:137 +12:0:139 +13:0:141 +14:0:139 +15:0:141 +16:0:139 +17:0:141 +18:0:139 +19:0:141 +20:0:143 +21:0:149 +22:0:151 +23:0:153 +24:0:157 +25:7:0 +26:7:3 +27:7:28 +28:7:29 +29:6:30 +30:6:35 +31:6:36 +32:6:42 +33:6:43 +34:6:47 +35:6:51 +36:6:55 +37:6:57 +38:6:58 +39:6:61 +40:6:68 +41:6:75 +42:6:77 +43:6:79 +44:5:30 +45:5:35 +46:5:36 +47:5:42 +48:5:43 +49:5:47 +50:5:51 +51:5:55 +52:5:57 +53:5:58 +54:5:61 +55:5:70 +56:5:71 +57:5:75 +58:5:77 +59:5:79 +60:4:30 +61:4:35 +62:4:36 +63:4:42 +64:4:43 +65:4:47 +66:4:51 +67:4:55 +68:4:57 +69:4:58 +70:4:61 +71:4:68 +72:4:75 +73:4:77 +74:4:79 +75:3:30 +76:3:35 +77:3:36 +78:3:42 +79:3:43 +80:3:47 +81:3:51 +82:3:55 +83:3:57 +84:3:58 +85:3:61 +86:3:70 +87:3:71 +88:3:75 +89:3:77 +90:3:79 +91:2:109 +92:2:111 +93:2:115 +94:3:0 +95:3:3 +96:3:28 +97:3:29 +98:2:117 +99:0:159 +100:0:162 +101:0:162 +102:0:165 diff --git a/trunk/verif/examples/pan b/trunk/verif/examples/pan index a0356c1856af44062658f30290864cb0d7741232..c6cf6e59a21d2725bdfe70da538248ea6d9755b0 100755 GIT binary patch literal 108893 zcmeFad0-Sp7C$~Y8p07L9MOOX0R;gC0YO0y6L54q(0HH`QHb0sf{*~N27&?2I7abW z@n*dibq~BSiIPb`lX$Gg6<0hrA}&1yHH)lf73KT+yw}~+J&=Iz_xt)C(wE}P^7Zxg@wEY$fqyn% zmX)%PRhF22OaU+dlJGB?iA4V3FEI;0_)E;fkI&abeq%?wb{<(@>@Uko>hZ?QmD4`@ ze3?>CDs}Zu({kUmJfYjiCoIM0%u}*0NA)Pz-;(QZ$=S!X7My*w?W1k{*Tb@}M`9Lo z%xCf7%aq^PQG5Yf&R6*}m|lOb0#IcW+CU!dhwX^c}p&t@$@$Xpt>ueFJ*U|Ww zfqy;muNVIPn!olgX8O^#&nBnZ3G2xCb^kFYZC`b<3XZ}t6aVa3J_70P_{YD)^dR9+ zJLqF+KPD2=5=o=K1{`%;k5RkBHUuc%zeZ$jAF$*xtN4aE`fiKn{n$<4EmWV6c%3j3*3Zckian0JVbQDN=)S2_XV05|?bJp2c?ZvISPUjF>K!Vbk|Ss?jy=gnLsL})#ADh;-*pO-fm_FTVc`g|aqan70JCrlkS z_(Uf)Y%qflBPRc|kD9Z8ldMuZe<(*{a{Nt{@jFekzAkg;V#rVObwiwyR?vNJJJxx$ z6?b)c+P)mKtxy+9yM1{+;23HD+3`R+$9DVAv~b#jU_nb!lZ#Gk?Z0Lh-E$7QQuQGY z>#+Y)Ty#0VSOsY=I%Vv?3>V#wU6y6K=x~Jd*WX3A$7mJ~anX5>xBo`E==R)zWmzt| z`&=7z(d|A={u~#ba}WD3*G0G6l4a9ebbD?>`WzSC-Jch@==S-X{7YSQdk#Z-k&AAR z(WIBS==R)*^wlmp=LPoP8W){&8T)Uoi_UqL{kP6Vx91itTkoQCPG$dMepsRn=X1E7rn_vKiWlacG2xQqZCh%#eZKH ze~OFV&qWUw?@BQrM9(q@q8pj%hbQ=g#jmAo-Zx^?MZJCd`o4x=f3Ga0n4d$*Xv04I z^{rr@T{T)S`RAEu7mZd){u$=kHKXe#{}}TeBBE<0{{ZvsqS4iozl(Wx&1jM2Z)Kic zGP*$WH!;ty7@a2h-!acF7|oIVLgv}^qFIu^ig|Xq=n%uMm&n^*NAo)b**%hMGB>&@u$g>MXb0oi;d4_&8OY%FJ zXUIo~NPZjh4E1QHI9f0H z=b2~dMyn+M4D$@x=z7UN#ymqcx)%ANU!NIz?}}h(Td;V0Q_e+a)>aku$@T?nt5?gR zHviTvpLqln*|T~zV>B2xdSB4n7hF}9pSZ7HLUgtJZ&EPy)rDj%8k=${v?@5eECWl_ zU^qPy+2EiwW~!T$f~C3pf}=iO)Yspu2)g)!rQ;KVA>*@L1bf%lg)5x?E^=U6xUI%` z1<3?fci9`8XU&>5*xzd<#e9>3#bbAzhl)^de)lqxs9Rbj6BV5q+WbcLzAxEt-q^f) zHFbMqGk-&cdk;N9bNYu0xA-?0J&Vx`H&lfJCj3x+Ewl>-n!?6tn1)KzR}`ARKmq?F zRl-ys?T&t95tp@(Ja=@q&z!T$=PNGUVl0^u4r~dAlV4wZOtx=dLv3I?`&8q}NU(D> z4z?+MkzjXi>|s;7*p&8>*9e&oNa)k<$=<%=hPE`nZ+Id#{Nah-zR;%PZEeel9opRg z{m{q3>D48x8*1`=jUB@A6_DU%|*!*Ai$|8EN*VQ?DWW17%r`C?)-7zz6y?al^nDpDR8G2 zyoZ8H4t$Yg9ok0FA_<_GXJg0-2ezy3?>z1(xS7eY@hT3pLdH;3TN~I#iN<4t;ndG2 zu{8Y=l&UjA?*|8L4u-bEyaaj#ylmGs{+Cz!N-(!xGdi%Vum+NktKh?8MP-1_egiZbp;}eP-nu_a;lJN;Ga)lH7?(;YA3nkVV^B1wthmEFHs1z*^ z|3+Vi16q`IYDhkW8d80$6Md}aJq#Z$>BBhBN@}S_DNSy*)M&M|jW1kinpgd_Z(sCt zgz&))OF9I@iry}wS#xO?;ky!k`60n49s+!-Z*7A3?ScQ*Z&a=b9WuHN{p;YiCme!u zMQ;zG?OPA3TB{BIzcpzKmPoL)ZOKk4O_6X|jE)$67hSRiAg3oCl0VkdAFB`QkCrO? zzZBxnHglK?G+`vUbvDONGZd%~2RMP~k25;Y$rWiBNn|LBa0D^?{0Abn#tDz~mIW`y zf&NHhOn&%=-afO(8Voze-_P&utKhkbQB=am<+}u&f&j|U6c<#G} zTuL&}u*J>E!hNHV7sqqY6!O$~?sGwap8ve3x36JV9+RIUnW@Q-kQ_2osQ*B6{R~OI zPXk*UwYVe?#iCt`7SGq>Ia(Z=fnw1$`aAJRt`?uK#T7W!tLATN@pa@EUCWg)hXm1X zof4*!Ao|>=go{ZK4Q^J#L=vRV0wtVAg7{~K60W`r1gYghC0t2@)G}TPmy#g03{^r7 z2~ta@63!q&YVj*!90}vt_`h5)rhYXYgjpnft%OfW7(>FRN_d|HE{n{!l<+1A3rVO@ zLNy7TW0_AYp$vptqu;dNa&@ED$V7^k)EeE9q6xJ|SEQ(Wt#KGqqa>Ar6tzWIqyhq` z_MSMkBiB}Q!!(zmxuZ1q6I-dcs-5Qkqq&iq`&M(Dk^-e#b3-(D14fH8L)F=3?40G( z@KeFXXeHYqf`2}9V}q!&X}QJ7u3J70owkBXR?;G!GTx(%_up?ZvSXK5p&wUtCnF7x za3X46t&GiASd8rU<v8s~((B>MijNc+~MMn+_<uXPPcYTX_UIwye=O(1aIR)>t;35|Mm#L*peaqB(roLjzWa<;9P=(JN1>MbG ze!x%JYScS~w8#<(pII2CBAF!oMG2E&TG+S{`UIypoA)bm2+S~l-UqI`cJJF~jy=+c zWfzC`;EG)h5Dtc3%Ebyc7`m4`2fJKQe6JizlkbHn zhE<_n(lg5!9H0!P0h?*xHvfR7|Mm}9@P&WCocH_#rd9g~f_|$m}Utt-?et5fhm_WD~>2oo7juTxQ$%f5F(NzJb$L9RoFFCDcBa z4hz-tLGi9MtgOREl4{UCa#TM=*!5rU+gDt;H?g2yZD22aer5C3LIcEq3>Y_meYb5I`^c0#`Ng1NQmbho+uP) z@Z;PNW+SzOB(yRc4G3d(jOmSkgKtb>eg`YLvZ~;#7&T_aOpptDCuO14zd#Q5arWN)u!fCR&jpfnl15J&;i<}G{bm!rcolu09 zhL>iTM`4!@9LYlD8JLS)su9vPkhq0^jSNM{H|> z+dYA1wJQq?e?Q0eHNkMl*NbLjvnMj?d#I64HLi5j=m|BfKG1lj6Dr}=K1g_xMr|q> z>o5evt5YnFu&>(eSlqCjl_g+H{tMZ@xdqntEvh@tS5%j6e)59 ziy-LLg7$QM-M3t|i%Dt4(q{fhsRM8-0JI5LSx_+%1Pi0X@>H|A5MiVK{sWfCXpP6P z-RR%Y6nV^nYuZ75jQ7wI*z~);1C}1uNb_%2ZQy&1BY9}Z|E+=Y0qAO=LR9(xyn!-M z$!}_)fBx%#Y@kN~pbfO$f@-;e-ov)atm44;2@HP!hV;aFY@ff6s`uX(!pLJDiJ6o( zL*wXQ(*{lcNa6S9MoPQTpSZ?Czwrf)ig2^j+gI!wf=MDG;jd3fB;*Hz;jxb+UHLp> z#XOUyaLc;5(8Ms&2G@Gf^NLX(dC`fbC%%H^h!&qY48YMZ09cD52n6e-jo|8<)!X;% z(b<%~cQk4$-Piyhm{H(|jb7tr>{xjmWT48fQ!#F)wg)j-dN0|?jgUSwR8{$gQ|n<= zO$$`lhoOd}YyQyUz}|$gu|6BS!p$=Zx)BN(;ex%9_Z*C!+aba;)twd?Dytk!ONOZ7 z*7&&cVbLtm#FK5y^+ zMWNK{aq&7-e(qSeixO@R-Qcd-_R#HUnU+0N_od~b`Lsq`O+9p&x?4Szzg#VacTxwn zrc|9mPNC_E#8H?zd)GQ~#@YuD;Rc?1&@)2Zk zW=!zkelvmrGs}ehtgsQ*dh&ZSI+`5jx3^)yGOj}541`3qKS$Nh$D&t!i2@DyC|NYt z5!tVdj77GeO4S-YP(R~7Y@7ldoKjbA0v2MZE!9lz3u0?AG=Mg`o3IQOI)3u6%3v6{ zTV<*G(T>|@smzYsyT`E3=k{wKZ^wFxRU9C0$68fK9~aQn0MNX;yJBwvnca%-`@*Go z!E}$(n-$p#r88oov`vNz_ZZ-+BDDoQ@AcGlF(*RHhXhOQ__!UIvG^!L&J`c!kd%^?G!EW?(z7q$T&V(taHh^<7hO?(}x<%`3jq-vV8hIfaIau7hub_S8 zJO<7)zySF&k`W6f8^MOta}u^SIavy98MUc!K)7H_WR6qq84$rzBNB2bBS4A%6_Vh` zEb1Hk1o2Hvv#9hJ&P9FhDMD3j2Aal#*qO>zqI1)u*c#!SW3YI_ylB*>{4OK}!>;LL z!KcY3I!@Z7*}h-$@Iz^#|K0I39kgUV6qkr zPsG%x3aQYh>TMmv333UjU41Aa+8gSS2~${JE_F?jFqsT@UDa?y9?M5<^51a*T8|tt zM{s5zn^V>MBL&|?);sk-_qn#phYsaYP$Espny(|}5w2oW|I&sL;exCxZZ`aP>=1H# zr-{G4g@yta4HC@YF`Uz14hxQn9Npgz-6Yj0uGQ+ISE){*W3BOAlf-UA*jRZAN2>g` zHAcHzdLuw1f%wp}uk8JZYXey5OqYW(1qaMRjp907ZZYVwV7Rc!d=`6FSb&@oHr~bf zxTJVgbhd$bX%hR-mTF zK29*Ypo*-;gRa34{SChS_ArB+0%eUU!P-FCGGIxg2K$F6)zidSm^Pgg4wOaG2G~uV zfr`vecRBsAafA#HQX#J^yVqFGilHf7xW&BXYgccLrlyF=q%Tvo6PolldeNcp_`wiG^3L6to zmKa^NPIAX;ZsjB5sS)QO8#&LZZxZUW{gmO_85j$?W0-Uyj$O+?V{(68hD*ytCONRb zd;~K*;Z-H!Ri)uoP!+k{;r%;!qkB1g8n>LJnty{_*|ZILhzay&|H?0|R`zi-egn##BRnQP0Ez!^OdNum z4#`AMi`Pku*I5IKdl(6ZC)Gt(JEp()p_twj&dO}{92+dfo@(htoLvjIVisAEf^E{u zKR7Ux(GbPWN&b~h-(y&M7~7pXXTlblwOQMEx-~vwYc+m+!U)*x32e-ec470z+3=FP zsT#W%2lgajz}k2@2P}*=dzL?IO~|m@W=+yo?8-#f!+JCu2QdG5VsGD=go4gUeuE^= zPi3;J@&ifF)2I&X|tSuu(!zyu=#3yh%!=SzqSecwFOPqJlE`jHUZuviZ>DS zJftuNJgU2B6Ojwm7dIuKvLWam#!yT|jgvtw4Pve=%hNMMO|ry|G~AeH%{%)+g~mQu zSA8%9H7lFUf?Yg`(p>3x6A??8nD8j5guAec3wQbap%-bLH7A!v?%8hZ{44Jf>t(S3 zGd>(9ZW$Xk?m-GSZmp_XMzzm{8eyXdv{u!g{|`&;o-M0=Hh9p$vO*50(>|~EH$Xp2 z`|C3+X;tJ;PHYYS08@m`$eLa0p{`o~hEskR$`LQx{*fXGo6mw23>n*Tt;w0YX9Y`f zo#0L>;WR3}2BlOgIG}!a&_A$hx4%=MPOr^f1}=-1HnDEE|BAX<{{GcuXbu|}!}&b@ z6~T+M{FhYC@(&I)FDcmVPYX0hwo)yOpqS5W0S0L(H=apP@GZUoSz`f=2OwB|18vrG zz#2BbK?!DK$Ac^NEa6HsE|6m`Q~(gfsw0_>)ZvhFtV_cZ^xr4+M#Zuo*@+|^@Cn2b z%C9Yz+>-&`r?!VI(VOveunuYDLjc2m8<}<|V&C&D_$%&I*!A^>`}1Tv7MrV7$(AZl zANiQ8rVj!PwCHD{71!YoqBhuHmoxVsMBuJVtr^H3PSIz|6g~aE!6LPq2XNv-Elx-! ziD9D>wn3NfFa=#4$m!RBNB8S_Ckn3bmg4G5$oQFLaW$_!)@{r|P-v zi+E8f3m28P&I%Q5sR=Yv(~i*8Wep+|c5e-5^$!JJEG~R8dr4|I@FH)^3?9du*&+e7 ziTUDXK3`4X6<>6BUnUxpqT7%F+Thb%Uc{J?-%i-xve{lywjB!{Lm~9v3CNY^pdT8` zR6Yr<5E_q3zcCL4-f$+B6sq*oDs5feKHCx*ldxDTyF$5&l`BcFdfzK`#!7kv;4P=X`%*6_q#+)JSUOM80e>ed%L*se}t15)cE5=-^h&w~W##E~WF;X%< z34})!D+O5Mq05euX1GPkhE_4ak{Xk+L_IV{xmL(#r0tW*GaaAIadhIs%ZMVYwn3k; zF@BK5BrfF{@1lgQgJf5&vW-^RMsw{om*LUR19lb9M)*Xnyusxs$M$_U`&z~K|Pc!Te&(a*M(A}?XBanduBz@ zDJ<|t(90n09}UTjpijp_kP%dKw>N@{Tb5ZTGBqMXU$2`lHKwX!6 zrHT?kM_DCK1Wi#a$J^cdh_?euK1{3FfhuUvm?SHLe#GbtMNVba+H+sCShVMcjULB2 zQSvm3oIYHxl3!gbN_PRicFD)zKNj!&@`(@?sO70|jvB1rZ>kL%pE@etr zm7kDJNC}Vu9@W5^VJU><WxKDbYrUR9=UTE{!%9EV?MDdh~6 z<5|Bn@<^-5Y2+me;#fIcv8O4yyJ9C=QcfeME7xSH(+>O-^I*CTo!Kmqz?WfS6SA&h z;>ZC`0IWlaHB5Ys%QlcXQmg!@=6Y%F-?FjDq1XxJYu%V=t}9|lkE`slkQJv+>m_Y+ zn+Ng{LTZ2>?ShhFqH_%Ek~plcij}40OjU0iuxOuiR{Kv+sj<6q^;WLqts2qrX&1Pn zAPE_Xf*;SfqTsJ8{>jzikvs$i<+y{U zie0C%EfP3l9I#K=;YqJn=3=rEF03+NK3VEspmiUomfkd)v0=ycWmkYj<9aR&VsX6_ zS$HIw=JIs>G4eH8$sBTeDd6!6IMk7I;`c8q%UPw!J|ePhDEsAHspUl5KWlr4j&Cb@ zkV0Oo^2yHRW`%M+rCfuRs|;}?Ks5%0AF$opJ2;OY3Jy1DxmUobq*MQrCz_?H0rkUd zJ)L&r{;S=uI5`5Kav`U~_Yp{rDJwvxF3g#6E_f_P55r771WR;}&! zvBhGy+pwdYc8j3M>D2Fb5&Xt!qO`S?O0{q>ynK5)tFjhJ+mI=)N-QxxLPFGAt>S-D zaW0Y|^NPsSA@#hZ>dV-h2h@+MF4U7n9;8J4d=;Ok;#~Q}#^Z`fuJQN;TcVdroTw5U zkKvEYhth6)l6cZZFiHFRX)K6MtzJhKesd;?FR?g;M?4J!ik6J$wC1C!B4Q1WNe+P1 zm_-U=&?{`r1p-oy)GR5H-J#2rDG7r}Nwy)j&cxIGV7gxMt&OD<9Wb6tZjud2>r8^@ zx|SUcfiw@xR4>c2W$IDCf?qU*j*vCSM@Yg}QFDC%urc&VCjcr@RFh?B6TH(&)Y^81 zm~9OVTQtWLr0D*%GHq0{wIj1cYRG{%jhfSX`$lfErUJ#vT!(E=OP7hNi};a#C!n)*@}SWOL$hC?H}h2B9CT~T861Qjm* z&*j2vb=V!6v-(yi2ghmg+f}};jkgT>nyj`&dRAq*@E4tn(!`thcpxhWJD!-}f|B*^ zuo%|VIIQ7{6;yI(4fR9;$Z3nZe*i2;fsvaQY7n$nfg@CayEgWz7u;_sH`<^cxmPqt zlUhE{{bL}EvCne{JpE=KhtuyqY+eI$?G$k;M=s>v97LP#c6vO=X{YB{;2OrkJJ_RI z=Ao!I+N~Pf1zWrY+!o#jcE{lm*dLu-pF!O_==hh;HT83C>( ziwx&8tP&Z{*+yZ-a^hneUJ(LvzLKrscCbiEn;xwIXwya7rYEVu4ad`+(y@J39kiOA zDfbAcGkpavD=<524czsTz}$fs2cY7gCW~!7w2}J8P@h2(ev=rNz`WnW(*Cc~8&%qR zwrz=sh}zevbSxB?tH5n4U_B_e;W!#$$HX1yIx+Du3%oJWT@kHt?Wnod+ws``Y)9{= zt;EDTfRDvQmF8N<`s7$*#ZK{?FBJ`~J+Q9_+WI;%aa9aeVq!8)l9Gh=vnD$3Jl9cAw*1~j)^1u{8R(zx z#LG)4vEpT0u9#%)k8RN$w}qhDF9Y^7_XfpuwoI;Om7&d6C%jxsWxPM=vSvX)ZMN0C zT7%j$Raj1)vT1RKD$`Guxz3|ZZi-dqPLQ>Y4`C(sGcP{byCd$=AWD_`i3oYMtvJKJfq2UrlBsc>Hw<~aWCfPBoqKZE&@ zjZL$Rwf$SA!ZH8uxLB&T{M*Sym? z)i8F@r9SB7bg3&*Vr^N~Ix@~Eaaycu$~_#D8z^$J=Xl8^sjI(Qw8D#$g1OC8*)$S0 z*BB2VNxP3$8SZgP@HOMPLy$Yhk-t##e=d?5xV;Oe9h!4wUsa}hC0l!iKlY_(WPj$f zQ?z=yZc>j7M>eAt38}hJ#qU&cYaj5Hm^imPslABbMR612++Gy%aVpODX`w&xp=w58 zM7GoZhz4=CXnKHABs!`@hDumVg0rMTdvH8D=(OZe7Q{N*^T;A#WXprW@feF`Nw6DR zZF>E-@x{RQkEc@vPIQumg#GD;)s*rB;$YD;m zISwUOw^{ATIQ~tw>b1JtteD()V6MrMZj*6=)Mah|oaIGfx9Mk@guODOJJJ$&osfWK zpPVnk+WYrYf9$6267uT=j^H6txS(9nd=rX<)LCW4k}rXJxym-G*6kI?}LhT zB6qTI+PiIGxn!TM=)8<9n)Otifl79+2)9*o7bRPJDFLf8=yD8n(Ow4~ zH-gSlvcyOQ8H7)B#C!*>98(IAUsp0$63G3~o2uK>xBAnZR{op?u~wd{=*|N9JZj<0 z4YIXVI^03$1{d+N7EaXmxhq+PCEO<%(CKK^&{}j%auo5LyWRoW?&Alo@(W%8JJ8&q zDhp!GQ-!SU4V;6zb#S8YDU?_ndL0}YrxTW_oHlFN_@ccdcdf`7wCL`0r7mk> z^Lj74WC&=CkzhifFW8()aDbmOy-knXV$ z#sjm12lMBNqKAcf0x|Ve*2Th-b5R=`>}PDs3E1-rR;l9L-2(J_%~|R`=7HYQ(}6An zh;}&W`7AP`=VKOh<76PsQdzE!V&}NcnaBMgO}IcrdVVt8Xcuel{9pClNQdZe8Bdy2Cj78XN-=^b_}u{r0mNR{*=# z*qVaoRR>N4!E^f>u2&i(Re3&RUBVYeq~Fq=CL-y6X1zK7F`b6S{-_zxM&ric2J;Qv zWy%XnFhj0@@e!d0>k**_x#zs#y;@@;RN)^A&0xr=JPPUr_TbSR+|=&)CQEL|O#G8| z+if`gWH~h)@OI3%pKbAWOy>^EARdKSJVdgQe0a4?rZBsok()4$AKTb>T`qIV{(&-m zj<*N#ac?HiKfGHrnOLJiNqrs^yNc??{mI1h4~up*`gkK}b)>{WTnR+;_qg_`R+4)K zD#pFElW~ar#bLZm)k>W%YNZ)h%Q3e)@`l4Q(qhT5Sc*^`ZbE$zRo3IUDe{@an#yXQ z{DrsJj(yJP?K8)~tEvLtw1H z59kTWIE>nK<3b=z0tvTDcd9YYLMkEB1k21hPs=^lSyGnYKGJzGh}R6G&(l&z!%BL0 z(N5-bd1tP1ENB3(LRe$C;dazZOctBC$jL{Q(olbNOdEz}`hzUN^)`zE5u6bWjnDAE zY~&>&1n?lAf7Me6An+^z4*_H(Na20IrCJa{9N=w=Rd?t4%y%(UhV?sV6&LPIl6iRm=}$Cp*LvJi!o0G-#2)W`yEt7p8vuw%4EBEzfxN2XI9xDl-VH$k4`FsK%k5r z;z*P%>WDj{j}MduLxHMB-lS|8f|WKAd{guWX)si=JXl5p@mCZaid-1~K; zRG>M3l=(5<5P_0rj1c*t;=av9-f5m79XI%X1Mk1)eb2@?Hi>_5^64)8*Jnr6Me5Ck)$H6o7qSqK3wNf2=qfn+}x(vNh&(N!{ zJh5IM0xf)NiW?YjD}N6^Lg+&{3FCEZLU1xpHW;p7&T50Moj(GV7tww!8R3coB=O#W zop_XCt2yi?p7`>|fMsTkWinY_Mj+#*9XNiE;~vy~^$~QUF#`wfOquXr<8iZ!=j}`o zcKWOIGZ})?$0_s4Hgm&2!3>aoO7ErgHpLCM;5KmaHvRiBcGFw&@AWFY5QqKzd$}UU z{QK(RqV7vLKwZ@I3u=P?Pms>32rSggPj^`q3~k&;OkdcAA_sMH^q+XwGypHO#OZWI zVkYJl@NVH&b1m-0ED4xJe3`<^r@)LbYqKv?hL!>bY&S}Vjm|iTihPoiDh@y_TFupy z$*}P)f<@+&c%FgDaQbHqAKQfVcagKz-z*Hqt7H(v|0}4t(4Uowr#kQ?n=ynHbFM5z zeF@3|o~cDOiv>&#Lw2@+26mK;$4-0trJ9SDjK|_R{cPl@!}yNKjAN0+&iFKBPf$*? zWPCeR-y1nz41+(u|Jm{fAM-)XGT`x$L4J1#{m5|w{aIq3qjw4ej*e^4l8@|?h96J@ zv~@OGmKSX(J>?E(3@NGK{gNr8;fdR0Bj-Osi%$5joOLdf{Xp+IEqW}Pvz4HZ}Vw{T%02DG(ta~Df=CVhdln%L85dl@nm!SabVy^ zQtY!tKhm<^PT4IeleS!szdNf|q7h2Iki3n!n23Hwyu^{& z2p-GI?{rsqv{Uv63(u*|va%aE&}HJRl(pSBbYHP@rlSiK=NqzlM*?)3=+S8#X7kY- zwBF4u5i18EW$82(WtjE+(2q4%l`gQ~tVdfWs9e~Q`*$Z>4kE9`iL{|enu^p}jK*KU z6#c24wEP4I=V>?2jd3`YRJl$?(j1Y+5b*>AOx;bI7?f+3+6@zwyxlOL4F}?4MXYpW zjzP+D!elM$Y*CD6Y_~-NN-T8*zDu(OV0{f(+zv~j)}2*kvLjOEh(y2FUFLC4*%K&p zTf_l3(o(%6PsuyWtL)Xn*Bw@N2nIgI&647qVc%i?rJ{UlaNVY}AVQ$AgiJ z>bC7rr=t5TAdCfn)3S7@>;{y%9mUJNJ5f)L)Wf-T6dc-L;;v|Obg*wIOU9Km={d() zc+U7>^_(t3w;i$$v-@ba>Jnm!xcJ+{>==ml)v|d`+50Fvke=&~rgqdb8@vbAa|%Wf z(X-gXi`VmNq1$@;sOSB%k}$qtiRgI-QdV#mYS{>jVswK#(K#SWbDTX0;**u-F-JUw zDahLc6Svz|I;A^PwbYKyk0oy_G=C@%Qxq}Bk=XzqQOJny(v9QcPT2!?S#q>q%QBp@ zWma9bCcLnIl|@7SMz9ZcF)k63t-`J$P+^rq{f#B!lM|5=71~DUYT0v6*%2ZiGq|lz zo@8GZEylfb)UpCx$nAgm*d1pNVGxk^+uYH16RLNO(9a6p)-{W|euS|d_`Mx{ZUK*_ z>qadzoU*H9Wq;7JC=tcR^8|Z;J8D6X*-@^!*6rAW-Yj5DRkS8r5qMI zK_AO=lbjk`xF~D+jMqg>ew{_?y2Gjq&7I=ZXI&glqHSX3+!&Xfr8%5^MVgeJZIv=S z87`wG4?X2tc|FIUxky@i{u!m}nM2UC3VmMm+<_g?SO>A%*V6McN0Vxc%N}x{lf3P* z)2Ycnbp!Xl7#{2{F(NpVsfrk%8EGZ2PJQt{2BZBVy$Q}N*Gv1 z7wm*a^OV@lCho(&T=X0eWo$TM0OZCg%gscTx^}g5OsA?+-yEm(omi=(=UGnadaIOj zyo9w@^0uBMsOLLa+M?v<7>+oE+npfqBU#j#8DnrN`obwa!z#5EJX!K~MQ ze|BWLASHb+DSD=sC0G<=8+Hw&!)4LUHI=ax1qhm!FJ!obJB-0bg64T_MYa?){TwxJ zv$&`_$K4wxZwE~$s{V{D!i_6qcpbrQWJ5~`oE;;J>lR_a2l+LU#dQN?4B|T0@|08B z(JHmuXm4AJqki;lpLyqT*fbghfv-T8Kzgf3Zy&$6V!Urt%1LP_A+)QXv}PHK;4f$2 zN;U%?cN5dF*2)CP?I2n^X2nc8+fCdtL;1CCA?!#9(xq-Flw#HCE-_CD>{!yV zsBlNp;#2{{fQ!$N$lB~A))lITL@TRaEO+&dS6i{2y%ig1hvRKYar+#T@K$H&esLR@ zhq1iQ&jm5tO@v)c=Isq z@#PN#+n3nmbQ%?xCHyNN)Nb>py8w%5|H_-#bv77xV*3(%t4Cr@)s*RD!CVxWIT#3$ zSv5t)7kz`)D9xc&>%fLBH2>|{TC~88%+@~>OqaQdygV`-rkoBU%1*V)iW|P?%6x-y znCzf>t&c9*DGTjss154P4jbmTRIlK2vxBHsa1o$-P#2AtPE6u{!(`Nf07blfh-BoX z!C32Ftj~Xa0|cDJ7+qg788%)NZah30GM+}V@jA>Wq?-KMDE&Q1aHd}4;l{%SAU-W1 z5~7bN$b12jDrX=W39`yB^|`7Wgj=dypxoKQEmfYxWY{5&LtPzYsvHFkf*lhUg2E_l63ZLzDJ|CN`ae zt6_3!q7yDTj1DvxVt;%)LQeL_x2xR&Gd!^=JZTR%9Ik<$;lk~v4{wKngmZ-@^^C9K zN_`DS-QrQ$-APXcg}Xe49*w@j(f=cCQ*Xuo_GbKhGg1OPxkJQ!XEoj`as+ppx1d!b z&$57um@lD#WV{CyR{W40aXDwJBQ%$l98ISA7Sj@&$v4!l z@HDH!i%=Bl=a2_k6;1-#uJCt>`J!?*Sx<3T6D@>ONX~J{jd!@hW;JY+{rMn1uVN<} ztPfaK()0TCd7C@&j?|^Vh}=&g7MPC#2-i&-rLVS+tVMxY30kC*sTZ00h^c3oYG!IJ zQ@w}T0C~tF6lX&}TuAH~8Hp0}Mi3j@M{<~6K>l2&W-)cMBYCV!4z?v9B+q!2e39vs zkj60d?aoYJc*J{9F;eCT@4Ov)k7z(qq`@J603t4#Ed$kT2V>2r@p2HoBG?{SY{^Y1 zW20@uQ7?^5spqAUqOdU^HQ>}!T-5`9EWz2L#J4n+7cBxMd{NBmMm$Xb`g_=|n^c0^ zk%H~?H8X(0WevX4rPIXKzz!7c_Fo!6suQo2q?;ySL-l+wbwWKZ5F`f;HW=zaU4?6W zOVe1#q&48bcPaWpV?R{0MypwK;A-Tf38+cWP+w<21D-!{eP_sh9<6sHfwE**HZg+V)0s4W$l4gnYb=&jI&`!*{~R( zZP@jIU2ns#Cv2I(u29L{QRqG+PjHyrh8 zJX{f|iah01_7IrRUta~mtlAHH3glBmJH$=K({h{wZ%NH`;B+lN2gDwe26zzmPzLVV~em8L?* z@$u3@N4nfC4Q5EwtOwLA0Y&Q%HllCgJUNC%%k3g7TpTNFzyezA%KcKOmJ78OV*+G} z_8`&ZEHPBkQbVA~T?T6%p`Mn|FKSBaESsgyVfiU!pKU&}n6hoAoetAKz=Y?@!GK9g zd(89USj<5DcqUv@1%{b_CmKK^DElGj45A ztL0Y8V~oO}fwyM`Uc*3AZ6+bp#0R3mp0yk&!Sd@*ek58fb6>uc&KFGJk^o6;k7%~R%BE?SS7RE21BAhA1_irVq z{r>+J(nz!;>3?e>d^h9=ObL!gQ-qAqze5u7&Ckk)j3&t$?`e4hDF3j^+3l5Qi&7~3 zv?j^-6q3&UMQL~?TXU#jPq+a09~3s5>##Hl8#gp$;yv-FEm5qy6oquq$)9FY(*kG;_vv4WZ(>;^N*{G(R!&HL6naS!{fpCcbKtXy?oq!iIW(oI@cy8l#vWAWGcnBF~V2+IDIqvhD>{B1(sDG#s?-t}|e~b};0Otm9 zM!6ObvWr=#2`Glw75Xc&?U9Z13trAT%74o%SUbxNlgY0KPvW)u8sl;_PD1n}6x0|O zO8Rd|*BVh^a}gRnLMEm$;L@du<~eXD?D#Cx7k!kF#=GD~jUl53iD+2R5{Xu8ylMj# z2=yCgWi!6kSYa2vpr<>R^0?cVTLt*G*4Pizdi%^|Y^X+01cKW}s!|Q-gsN);pMFv7 z9~TaM`a`t($D~kQb#t%K`vW$IF5iyNCs#KZNrCO5HwSDAP1=tAxa}pzXzKnYOsg?2 zffl$u`9e{Q)9@POG^T5eEFoZh5$ir(-}C0!H=vXx9I61`K(z0T@| z0?Z#m#_gY=&iUY|H6BOx;@xSIEwZxl#%*6gKPRF#tAwX~cxKEX|H^)`sz?R?#i!z~ z<9U1VMW%q65^WPJPhmNobr0}%TX(gstLDT`)>_6n$0CA0fI_v#7pP1$tHE!)J{O5T zSJ93?3U{r=ZGK$Djt@m*wxc&f)gVI9^^K#KtNQYzXPD+;c#H8;xgP)#G75nhJqzH) zg?keHw`aw)aM?c4ONH%xA6m@z_M+S{+mwqqD%Bbvf1K$%1|`u(G@841)s*j=esBL0 zfWQ6`blQL-v->mlmc&)g*y3M~Dd_M!5C`zM&s>9rd^CgVzqFQ7E;5$g~( z(otP;bHZ}m%r*8STmdxOu9Rt5_R_ zCv(}csJ#?e`V~yz`6A!3_MuYy*oCa-QBa}z8PFGgfaY5OhO;L%KcBKEf2!NPp}@`r-h)D79uMUWg7E>wC+|=b4l-R({a~{WpWYei8dXt{jumTk-oFgs<*R4{~PIlx9PnddIRYdHocESPZZ2)Lmxu=tv0={L(d_7p-qq3wUqS9HhqA@zn1jzHvKqz9G}3q9VEF;}LfLUb`o}iC zr$a9zeG};6^x+?%cOZHzKLky}+x*BDh&ir_0(aWMO{ zukDb{;vyE$W@;T%mm_8Jvw)VaviV`_T1H(PMAtIawX6kQ8>rVC(2M(^$aFGZMFyD7 z&Z;X@8mbsqVewc9Mg3<#ieFj^3~(Ba84P{ z4uvMpOk+?JrYWmlMD#G=Dt-ZL<+R`B!7SjyIitgd|2>`+_vIfJHjJu0IN zlQt0GMZ$Zlu)h@w$b&xx$DrO1AY`qS-eeNb`(Ss`I_s@Q5~h&{6aKVt`YTX6Y_!8K z9(gp(XEEvLbvi)`3zA$NEmEZO1xc=so~}qGf|P$1s_9XWYA_GD0u@{bGQPur6@?LS zP!PE2x#`16z}dRmJe3zc-g8<9O~3WsOsoiof&&|RBi=+V(&V_U3zpT5y~62jMdwMV z4r_2sN6tnHZZgbv_;y{bu@qAK@aHsW4j#Fv5UJ(K9m%w4`-!}4%96_ zDUR3?#2b5ih{5oX$Z-z#`-|Yej@DOBi<{dnemY!G7a8W1zkqU8Ix9m~g!!l1Hkem& zC&eCYWAuZ9D!I_)bRHdL@ZG^rsNnz$9$n(@u(z3{Irzt;rA!}X&%XFK)1v5>Vi zOB>uOe0&rV1B|Fvu#n4k$aQ@^Yk3|(Sm=B?mXF#T*BXO7Ddb@FbHtP6u?K&o88gN( zROOeZCu4j}2<&Z4=BFb0Z9{O64s7?|b`=5`i)q}YfnUtELp8_Y3m`Kc3);d0#{tvK zZy&&N4vdA{eg2Xj49U{MwH57QTIKbSF*De-AenbSE?8Qy78loXuaen7I<~{b6S!!A zv0&`mG6un94Dkh>!C29bIK{+SPyTRf-r>D5uwbP1Ou9>xaW@9XYyQj12dg+IRz34W?2JPBW95yj1c)M9j?DgTH_ zDYY619^Ng`8Amhu3ltW^q#)kQ^*0PPqtL9kA47kF<=X|e-?+V#0v_(e$qpLU9`l0X zqe_vFWWr+egJxDe0jEG?sW9atIrgP)y)mQKBFb}5Cm6=Z;KRlROoqm1AbCcNx)K7j zLgVo`_+Y3b!+T#O8VkUdDQsD3c=96=aZ?Y{B(P%-Yth9>CrGhWJC4;(h*kS9Y>`;i ze!`?yTOXsQI@P|cEsAewA_3HAg-P}d*Ge+|emNK)XHe5b42|_jfs=bi7{XF2<+;cA z;XAC1Qer!vc__!DJeKC%)Cq5WpB7saSa8c7S})1$W-OjF-?%ubvgUN4|)r1+Pj$ zRx)-7d6RHMjV;0FW5k8iaUrVf>qY46z$vxZwKZywz+;MdhiYIKZ^27%dV{A7e*2p@ zD(Nk1#q)Nd+wRis;rqbP9mw~AG{Hi$+;by~AQB82*D;CbgM`6$UsvSdK1R>^EXTHK z627x{`F!!w_t+kdxq3(ptFL19#9IS=AR=C4M2!Dl{O}F-U!?^1eIdEO0``OQ zBhYsm4fAk#LcWvqXcZd@vz}e1VTVVt>EXlzx5^JvykOUjCftI}bMM#NMm!$z7g*b$K^AQBO$vfPS@v*(E? zwqvU{77;yTSX~s0&z&M7R_vB3-x3@!_LLacB7vHo66vf&G{9bD@6#;aNQJL)?Hy2$ zah$h%rSGd@Bl84k1-pHY+I!;{5Ss?ESUYWDJ3X*Rv^(7{2^pi2bk0?o_(<4_!d?3i zq08Dwwo_sbBs4hjSX;w}JkBEXhj}T`2VbG_(!x0@mU}7GI53jNQM=c7sGsc8O-skD z0uguo2-Uidfmt5AFwXDO9zt!jFO-u)qFkUxF8Kqe#J*yK(?up%2AF6_(D4~OVUiI2 ziH1CiO1x#Fb{v09ZLMPx&X!!-BwC{Q#u9ztXtmv?6-#1+V1EpPp#ogaZlaB74nEh0 zXLvC?Db3-_VplY=?eR8~{0wZ`lPP*U_Dy*r9E>BUg5a70E^NUKK=OPQ;NXVWPu$~U z+{;|Yeiy|oe44NdHT@MGG=$!ad6HeUMqhb^4lUD=l^r<^!F+;`n&@<(;1Zl)2O%FB z0#(d{f3u|~WP(YaM+xU<;vQiHTyT1`nX82y4S&KuCdO&Aw^DEqN5t&R?k8bPRjnww*`aSJ($U?Hl56Y|Mu`mU8YLGAol#=9pbOO-7X!d5aZxmz zaS_iKGIHcWHe=H+D=x~BXc5&F7rt2%7o8xku#WQXxY#XS(rCm1aWM_paLs4P*>TaX zy5+cVojt8pR^wpnbZ@-PUZolmB582^3MW=FmEpXV-J**S^~w!SVo)mCKB@_R7%hTS;#v^RTV zxxhIe-rliGdqGS&p246jK3k-x&b@z!|2P)He7PVzYSY4blC$>EIwDit(2Q%vD)7Dt za7mM1holPXG@y({cz=aMc5QFnV-b0dDs0kmAZ-Sg*?uCRGxWvfiy)d1r;gaGTevvh zijUoaxD|yBTt6=GG6};#W1Tm>VpYuOd#k~e@ZXT^WD&a|6?6Y?>w$t1CZ+QqU$teiNxc*tZ zd*OgB+3@Obbk84utKhZ2RdB>_72NyEZ?tjqZxy`t5CrvW*Tq$Bd83s~cdfU1F+B-W zz-CV3agyEBcFA=1QZ(coyCKaQA2u{)k0kJaC5`)oy8_&N7}qUyNcdqZhk(Wf_DGHg zn$n-I@Ol!9F+2g|9Ux3BN#(AJ1}v)gj1FwMvBrjw;m6k8x+$x;xy@qJT_fEhG`f18vYV*ro zRt;DOM3b$)C##VL+)RS`O+l0S!c{h6-<=P)dGAfJ^eYI3jFw%WrC=L(?%k%Xz;=c&movY z>#3x1ssMz!UMuKD@Q-DGimNOr#O8vX;(^BDxEz&wSGio#GoE?G=Un<(2Ac9?8WaV047OQ?##y0k}f)x)Lv5-@Kqw7)P54Iy-N#$BK>AdoX?b80& zN(IJj9!hgFBRt!gpGX-WpgoUtJ_-RlN^w?$TTkPQP~@0GU)Lrd1FA2(d>uMKb{UJx z`BT9kc@;_o=K9RVK_6TJOt~BSkWq;3LKz|`^l%f_tV5vTpWk$8n48if@LxqeT;K8W z1*EhBc`YXWqSwr z2IBtvG_kzKsQ;_t&iCL3Tf}W@5qBAJ?^j%O$DSU*oE8DKJGOyvIe%OZSWdv81NgTZ zm*s0pP}m}7e26J zUC$3pX{WqcaS=kFyyjMPPK$sC>6C^8c&i6+fg8}%Dbun!qNhNma{lOTZRCg)Aq70(KKX$ok5qH+Dfvd-+NNPImy!%`TJItVUsrnDIR^hItDy{SM|m9?UhZ zVfGO{+kvH=Kl-e+7|#A?zLI4dp5?(@i^3N594eR`f6Dn&(E~qfdk86Wc9vk)80SB$ zVf57|w+q&R#|@2aERuBWAjvh;U{)ikW0tM%ogPdR9Bxb+=*(W?$Bvk~cY)0;JJrS< z>%nYj4YTF3<4$7EurYt#*ug70>PSK9DJcKj*wNh!`PMiZ>w+|b)$Ybw5B3%vslx{c zxN`nfWZ*~D4I^dF7i^rH0O_QXk=sUo*nB>q{ojST@@N5$o(G7Dq^%W zYrRx3JA$R0Kdvw>Mb@kuEA3um{AHc0JI(`L7YB`OOx=TwPcs!7>h6rVT~Hr~=?POE zqEf+9&Yy~Y_)+iPft1~w zO|3!4k6AJ3y9s@nLcM0MB~m{Be2W9%8n2FmLlV5v*khHL1Ip|F@N14kO^6BcR}eUD6Ss+8)o&#cp+;}p|LJV zW5Pza(Y$56MMqvIvE&D0Ie#kpIN0|hWnLxN7zCz0sj+0f>V{5Yn7m%xVoYzW1L@b@9&^d6<}&JDA%l+pfHEa#6th{9%!Jc=K4wqPTsW?Dm5pfOw8-~*%UdSc!kj9>u-A2!8&FKG1<8Y>5 z&L3ASJ%+4#q+lbKdal)2y59r6APyQLu~Tt%xfIX ze{XQRpePR06H8+Rvny0A=T8MXxKG{~7kLsXGea?Jj6RR53x4l`E@=%q5K|Xyz6yBL z3e%?uz41hGL5)%Sh(eF{K(B2LI)3PjK|f9CD-{|&b;nC?PpoSVGe^`-hkQAIT%LG_ zn1|WwcC*yI%>%tY4jLk{U|19L1nKd?@B%up4gw=Rm{oC@f5Oz%*^8?b%)LKkO**bN%NBHQ)^9i^KUKD;I_BrEyVaS3@DbS*AcLd4cNN9@hE6Y zH%b+TG4CmGtVg|+7MtTWY4;-lSI(b`BnNmNQs!&{#+dcagVy=)dAHeVZd~xk;^|=X zKgC7d+~WcCY!-V)7M=WMppJ6>xHh5ZBWubB**W<;)>3qg2RGBLs0VjTtTWN6F5Csg zoppj0k4EEjZp%lu2pB(@v;&Nu_7@Q_-2r^S1L)b*JwVs&2H|r4xVmNm0bd(zYj`FB zOLNmAO{8yp)9#u>wIW>U;?<$8C_I4jpkhltKK#3bs>)x5l$q<)_1SvyhJ{&=!WJ>( zV;8&@=3HVX+n6o&0P<&-$D>FOU{OR+Dls?k^nh090tbd? z|HW;ur?Y$dkS_9%1Y9|P^hpeIM9#;L*~eDT_@f6fr$u|?!%+H=0A5PK_l~pdH7@o5 zdisz@!}#a{ie-8(0gG(FmSRwwAs!_*SPIH1g5q*ut1)diFK?N^8DkH?mGj5dCKu4++XWco<&xj)z~0e=>lrV>9~;=$2rfzG{Bey&%$g@D zE@JzYKe-k4oFK{R%slE^2mES)-PTum06nL058y%8^7lA^-8_ITkLXd+@F-ML&Yy}7 z_|Z1H7%6jt0@fHq?p0S-KkK$UtHmh)K4v+C!G(JXaT~F!*SXaK4`6PKfbpjup3!yO znM}Y39Kc>~z%^wkY!NelrUhQh_*uj}-NtOa=ftC=dQp6W;_5j@;WKU@&S_D-_@SqZ z13ZQ5{qb1ahsV1C*Q`ZhiCjhj|Di zcs$BsUX*e{ak=p~3_zW{kh9_;jW5@^jLu!qq8D`l>It}V{1osutH633q9) z343stx^clD8!vpPwYn63sjuDQr?>&v6cNL9dBKBukRc<_!Ti@BUB zKNact(NSX>Qf8`yd6x%sH45E&dQM}#W46nP5yQ+QW;r&8b;KCw!CcoGX8fSR<)7*~ zgP1cN%$-lUZC~FS=0MRi6D;NY(HE>B;fu_~kJ-t={JjUW3WY7&etOLI-r%d?P^^R7 zY^2PMN87fK_h8l?7!y>?t7gP7#h)?EImDdnV1DzY+x7+&9zah}ff?`580OU|H`5)= z2RxW&9OeO*0DZtx&L7uF_ZnhWgQ)F(Ix$OgQzG2)Gb<|XCBR^<3pbs~;{5>1)Be^b znwhL9*RJT-jrPRWkP?*6g5nycj60qX_gd{1UC5JNH z$D^cpQQpiXirbH8c+|^k(T@)u$lgStM=&bkg@gip(Dg(-3L8R=6qMrx#iiaMoQ>ik z+jt?jVkGriJn1oagJia7@mjI?7{GCm^i`bT0HY~<=5hh%k}TN+=$W?CLC&2BAH`gl z;05eMz`+jS3x9BH7;I6)_*n;6QaZl%Bj9I>j(ew*K2AZro`tMtO3;nY~H3 zNum$%&lkZe%4hz7n9?Y}(G9rY?9J0U@jWLtg&jo9#}%{22$iU=z1`5cEw3%&J5X%4 zJ&?F(JG$0C>^8pTDe>WAJkJ2-{BhlMa~uJG>@LRF7!9|mqD$Slticrfcw*kW77`!xg1+MP}!=GhKr{X;JM*HpEJ8NY%7uZ1}RDf0*Ha2`TO zk4Ne3MR`t8Tpj%odQv=OY#JrH4aZhW}+HhW9(d| z?Ox=8UIQL?8zCE;xr~hUC(Vz5pn8*6&}o1FFD7b@c?A$c@{C( z*_gj>zTU%&a;2cSx|8wGHEydLz}})KbztK7R?Z*SJw~IDHQU%48etD+2Hf5vX8gd^ z2T0mFS;TxE%VPE9$sWwK)-dDyKY%REQ;B(njoG><<54g%aHC`hip!I~VPMMiLcZRW z#=0Pl@%OnK#{_$ej?{sPQ-yN=xEkjaWX-vPjkEle721P#{N4@S1Rgguvax|_ZL9~8 z9zQT0rqDPc-R;3_CdO~vrr{Qow)?3bOkZp5u7e2sVmW^*7^E6YW05jvDJJfLD^eG1 zzt`=8l-8iDV=e%juY!|ig&s%f4mPx5L5DohnXN&`k0mkaY(lTc2~j;U!h_krHOzWZ zm(zuE{ zKs^N2l=DZ`Wv!7j@ng1gFmLx@23y07pOy2}ukJmam@i?`r=fp}2Q#NNOkLU1ndSU( zx%G_y)86~XM^#+?PWAzpw8fpMmVT_sp3yXU?3NIWza(8RF^JJon@`tkr7$pRYJou=!}Lvyaeq#Cot1 z_vmKo=0Xir7n-^BjG#h0%rw6;L&E6MB#fpj9%SkXswvI;3X-sqdDGI!fvwI`w;zq? z8s<3(>37qQgJ&)AEVg-mJ%eY*(RhA?c}^yt^rK&|!-eXekDt_&!%f9kW$@hU;yJ*= z>J+5kO+Su~X#w$UF+9)s;7&_*)8Lc}K4cbEe*>IeP|f~G&RucfAj%y|%!Zf@{<-R> zdeT+IT%I20uKr7G(T=s4Iu)#T(~si`G452Vm6>Aj&$~ez{d;$q;$~k+-I=x}V&c#z z^Bk>t!j|r_nT^gm+#h3A_U9*<3SVe5%f7tk?v+U%t-=CarPdo}N3RGs7wUQ)T&6J> zM?3r%hKnJYEdPia&TQHZTTDGzPSs^}ynDGGE(ELH^rIh^@HjyWE~%}|6m@%kyRO?2 zHqTNgPtc|Z2;Ke&wVQt2bvsk@MBP4pyAd$^;^b+U*&YEIv*T$_K5kPV7Mi+E*vu9> zCCezSdp>X?Sm>D**kA*Bo7s6bv+S#!?(v1pLs#)&Vz$I)_S-H~Om9}n^uR*%yWRBj z1WU&CK-HWo(9HJae|MFxhg%HKqkmnPy;m7YY<~cmkHhzIbHQjVC1oxvn2W=h^HaA; ziMMrtG;5*VjRds9w+L6Mla5b1Hy3mrPAUU2ct=vLh=kTTO1JsMZ3D-6GXZpa*!$t9n;IF$G=wBu7VSw4y}E~9J6pKyz* zmj^-WRA5Gd_3UaUNOseYW7Iqux2bEGFN`sNrLLEKn+)5XF1EN$*UK?xR(YB&>SeRd zZ?B7AhM2lF)AGb_`f-R!hLrjth}nDsQ7z^~o9(Wnv30j=s$^Z=Sfj)IU$cdnZ*DZj z?l~GiJ@(O3$8P#@h)MO88fL`&aYT!Go6UBgi!E-`+B}9E@*}ttx^J9r^Gmt-i8hIC z)ov{&UF)y^zkn;<*N(+iDrob2Z-XiJAw)QhXn-jNEgJ5oABUTC2JstZ^Shh)ZCP5X z``{7xm}$kA3BRGIw5BV=H5Q@CTdLZ9e%gKVQYM7eLJvO=nUFcM60$W-#Ag=03J8a& zBZ$lO%*D|(^WXil5slw6aq8eW#VaDlMeY^LyuXR`0Lv zoWHkw8d9VVev?#0d*-G(pV{yh9Wve5)LFb?U9n1@L^s%H7!g0Ct(7POn?Zs0?ao`xM+(3l16vQpo$F|)uiTq(SVSKg;ek8x zbMv~xpW@~w>|@zSc5!eWFz=z8V+^1=xB{3rFn%%yLx4JXH88IX5e#C~!OMVo4jyun z_#j3doC?e?I75tqpP>$(0}M4k#(-8G9NArg#*x~MLL*rLP|k`Yfjg75dtl*e6sV6j zoLdh1BfYf!WeQuUe{!%2mmVqr-AthylAUhOqZ<;NZcf9FZ#kesj+ax8mvN4tAVcK% ziLD|w6|?y<9T1U(u6l{;z-Ra&o^O+C$&{;m4?KfQ zv+3mnjK;2c+Fs_&%EiGAspZ%$5zPc;9K8NSDrtgp#9pCC4s1dKU~&>GXg9iyWVA=z zuQ?@Z^pHwmr!_4Zwo*TwWP`>L2`6GR-5J$=I9nol2+HVunwi)J3S6I!({_1?x5}e) z=8EoE2pPzVuqj-1ui5MD=Jz*4s?K$fbtZRqE_nopW9-1;7~9b9w|3=swqkGDzPzG4 zI=QHiVb4x;P{vLuodz^)?^8r|y^oZ15SurT@~*d_Euyt|xWl$=`<(aae{hQXnK&11 z2THK3E4i<0-D9bx80S&!U9#7fKGZ1r+YR82^fRh=uD$QTL-2Pcv*+_0erb^e>cF3n zIda~!?znQ+2Tmn$@C*)e;eEX}wL>-7zwUXyAeJ>mui?tBXV0h zKyE^jSys?b0e$K5(vwKoEsyr>%hW~DrW+t9w&L4`Q)WJ8DYa+^-r$>2Kg9~ETlE8q zgyT8n!9imAdzDrl)#A?;B^-Ll7m8T3z$^buD>}_cuHrGlYX*vY9Z$bvUf# zpW*Qix(=HIO8f&nkNO2Hj!rka4HuMahA|XvIu!~?8${9VgVAPiz6OY~KkcTsa8ycH z{;MIfTAWqc-)f(;t@gcPnO1w-jr~=3Tvq#SjHmqsby@Alm^g~n9yl4@3asI@HKF1>}MWSv*N4d+F$C=MIkm3jb!5n;tfdJa6Ko553S`s*r7 zK@vF5Wz-$VM?WpK_A}E$ARz6m=&(;)QQ4&Jqa`|rv}ngYs%TTK%c6VPhKriXhS6#F zx8Z%Z4WBzS(}wr7_b+!^v9xIioPt#kg#E0>n2q{3-@voL|$#t#0FY zp>=JVI4z;~-?0ZO_x5H(?V?RvF@W0y%fHv3AOZr^!{FnSzvtjYn;T`9uG(~#XE4XK zX|S@B=*LFgxB9r0)T66sl|MNf3@8YY^4meJf?&zxS z$mz+WAAO`W5c}B=>Zu7-cWCeZ7(6z1Rc|C7_|ZIoNZC9#YG8U3)Ic)Qan$&bO1e%x3&7W zLD1?Y_U%EsT|i16nGetWPr5eQ&pYrAY|gZT=lYpAnqSdI8fY>tA4Z)j+V~a5ldqdm z-Dxr6$kzxw6njQ*4nT&31#}g{RVGhZ3QZEa=5Owf*pg4QCI2F>pdhsEg`>5iqNBSv z*@Oj%J}`>xQF?-+J0_tK=@h)1t@f~sHo<|hlj@%Hu;0r`!EFoyd?mY$VReh$JT35kV) zexDwWZbdHLU$@negRF$pOg`i9se8{swO<46z~vm){VhQamu2kwVy8YSM2>kQ^kO(;XIzhW&EZTyMW z@sO3rrQ=-(zRdJI7nxDLFG+{y!3c1+B(0{UI<#&VONLYQ!G`zS3OSTR3US*goj&@6 zP4g0Hx?dyB{F$yGK3=;#c|hZdL-}Tc-8E`9Ry}pb$C&)l`jHlzRz6cdhq6%}IOFgT zIeLh3SZMN9%!zZ>S7(;!JzLr@P>GgcpY?s+`SVOST1bMQg4@&ty9isb){?HhqT5^0 zI=b?|bDf?&oIY?ZRj_D9n+`(>GWC~wJ$MaT#+8xdEb-Y?E}U0}lXKP&m20eI^e^qN z(;}|DSN5<+kFsSZUWnU_I_S)AL!L&4<&fbQ;p3E{6vP!sEZOURicVbH#|Ia=_5QL$ zl5IG9cNr;)7fQBbJlBSwe57mL&N-MC&g*=7UgzGagP&+ zo38vjuHm{SKOu5Fd0@$l7j*W)F#5W1{@J?sQ@6r*g{AdLWA4MK--l@hSdKkjmSvP) zFXdvj0?QA{6gX2S`&&I^yO{5_Rp+&rvW@DnruBkR-%6-YtD{*f^0pPnsYvpXo$90W zt$N3zS=`tUJ994Z=aLf)Jsz=KJpVZ(Q(~zo8X=_ z!62HRohH;cD)CVFmu<3DAnU#k)s=b@SD0WxV!LwT?%uDH8SkC^!v}9cYW5Ew+>9&T z)TP_h49uJt2QEKfz4JChzH=?S9GhHsLzG_z`L5dy`K}Cd-4pgB@43T}_Yiqn+QAsQ zFG%0g3MommcdMb_EA)8MQ~d%L=Y@YmTvzq|orA{JcFljVwySz4+V?J=Ceo49UqkdR zs7j^0fBoF9a++23lE15~UKeKO(B#PO>E{~yV$dHPI}l;fQ+=sfh$Yh)C?03cd`p)? zKM{y^f8UnkiN3THms9R^JTuSS`QgFjG)hlrUq~Y`yB`cg==@pt4{UZTz|MYZv{M_! zcY)In)YK8K$D`w`$jpCcoOf96wKxW}Z3|Ki$2!O`Wpo$dRgDy+Mk` zkA5Oa?`d{h6#dyoidGce(}-x;yL##i6kP#aY9B{;AZGV+ipJWBdJ4-us(UAHQ@c63 zH$c(&c>*K5dg@||wkY~;L~8-})+dx ze=433fQlR{rb5fz)A4gng(I%l9nK-DPq1E&gWmt7L5cv*09>FV>F z$j#0F^S6*u?+~nYCQ7>I9|EQq7@7eO;oa{$pDlg0^S69jFdhAO5C^!y``E+h0HS5& zKT6bewo@gHbmS%|itN+&fZ_9kd#{zgB70_ zoXG%vbAByFAxTYVeibgYpchfrbdWKfaZCs8q2Sx`WPp!${VFb~TcC4;@`tCB=h7w4 z(Y)89^Zuelm4ELd;F$1jpdms{(d=hB^KT_|SN>kYRUUz{tQy+gOR9TzJr-RX;sM=S?0Yo>E~k?y$nyzXg{g z^9E#2_w9vvD0xIzt%o8!B-MO=vP;@mFX7ZDc)Wduds#`Fw-UyvgbpPd^m+$7W;iep zNNT85$(Yc^I5w@ckwet8=psP_gs`ocZ}zKLW9U*KL4EtKRlWvF}quA zihNCxW{14jUz;J#HZnS-9i$I4Md@Z_#vArVB9j2~N@%J3HaoLzACov}@%)UCG`OU% z`&)MO8bo*R#BFNV+9OAHK}*@yWZj)rO%#=>Cc^Yr)35D}70cCMO`q5lZ~U1RsnsNT zJJduNQ|f`##PLowITMJQMqXiRZ6#;sQq#G1^ddxSHGSpAfz(7MUi3AbQ+=3>ZfN&3 zq)at|^r+`+qR-2)NjI0}#Kk%W7cWlb?1Ax)BBP7ubl++Vea}Y_`X1uZa|47%)u!tf zt@eFcAK){#N%r@(>^mvNe3xH-4`RZ6~qlRM6` zwB3GrgT6 zxTf}`y#;a&W)7xT5cqNVf!q4W7A9vDbyvTy&u0GPDju#bekOS;A(46I=SV`YZS1E8 zL}!og2SgV8JFE8{tW0M`PRBM>)?o574xZF~28nz&L`L3};^0Ww02bJNynMsrU==`& zPHkM=~Ca&)WqYd zODX$XGz}rT7uqS8e`p*Wj8l`ZpmV0NEJsd8>M=A192>~j58^s)!`)G0xCBX&=!GPy z=}`ANo98e@7&oMZJ0$716u)|g|_yNY$-ePmlG+1_Pm`wGy<*5+e2 z{kM-r&)M#=>0`&DXKn7c>1Q2_p0)XrO@HFC=!axl!&?WBQQm?~Yj_m&2VOzrq}nQm zIqK&B&113Q+DfZo#j)sFZD}>kI2JvtEv<$Vjz!OEOIPFX-gEXYXnjY8_Wx+toO3bSbU5@UX>mZL{Ja}MO)aIoMAoZUQ%NPdK*1z5G+x|Ncod@w1( zJgZcWqN$@&4augaV5~eI4TY6Qsrc$pBG3|ysYJ{l0Eh+sjR1kxpg#;aJroWlrmN}U zsBb!vgj!W160zF+;Wbt?76}C7@nBpv_#64o@>u@HM#3u<^@pch!B{L3n{M?_VtG7P zAQ_7V!wHs3De!E!LUF4^vx-}#o;h`MtL81LENLtostRMlK%^}iY7JVDxW!6G(rgzY zo!@xts_NN`7c8p3hBJ=0`CD7ZTj}(mEDtEd#?V&QX-wTEC5=OszabJ!gu=~A^%Z-W zf6hn^hYCDN;8=kr0*9Td>Ha!O!({^hak9Q2C-9k*gx}(rKO7GwLXohwcuh1o-BKK? zD*cH_TPQHYnp4^6izkB78CGp&Yb4-ronc*8+1wgw@VBb^NHP`(dg>GYM9`}BHw0Vb zU=XcD9W=*KIWw$aWiZ@0!}3@91A$;PF++1#sxFd1UU5p;hFY-Ng0W^4*jnw6TgiB^ zvD{h^Ze3#~T7p(nC>A%>q%02cL>tls+k=5*BG_n!!dB29XkjKnD;`{#42A~$f$&zO$%-Ts(PYBoQ8xyBfkbhNRg!U)mc+{}WwnOFL91kP zqq0glU#nzNV;OEj;Z^?DP$RL@0+p$AY(q!-=|fda+giXM4o4DD4k$|~n|MiMc}ZNi z5)cZKP=RQ&q|v9Fk7*KUb3x0GKggt|Z-Q~h!JjQT)@DUwR@*8I#tS`D)mf2nQ0&~9 zHz%gFoZ(Cg^^2<(Ew&cSwPs&EySDlg3Yu#*wa4+gts-Aj*eD82avM9O7Erhd4Q>^L zY_$9dtqO=L(z*B~V7F8b(Im>A$<1O#MUr8YzBLp_ahj}XBpwe@-KR5;lQAV)U^=4q z>8dc{gMi>qorWIK9W{MtyAKE36Ao6^lDg`p)w7o@u9{U_4eg;1h_?FI z=oY~C*cO2tt)Ue`SbD$@+eGVW3qd9{gaB1oV1+IeHIXFW4T9In%KPiqY z>XG6TG#RLvjek|MvtAp6s7A1x+Du(lU?>kjO_A7Yf2`4JgVjQrrKP2-W1&RQ7intp z(5OZiWtUV|l%0F-fKf9`CrzC?VNzLH8COL{dJH{np@c78D&UvFws5 zWoy@#qRwDHzE+r9B_yC6O7%eOLjkTWEj0pO5GpH~Qg$5?i9ux2MPtELRFM93|32Nz zDZVZ6VS%p*ES{m`C(YDwaHWQe1ST%g_pb@ey;R@F1@04gwO8XkRT{1l_=Z5=ERFw# zzz=5Y`+{l>OXh0$dx1rl>HDa_M+Ckh@ZlOAe?Z^^m+SkJuh8&IwHiJp@E-za&e!;` zz|uN>-!1TMfmbik_~8pRyjq}Vk-mRG;M)SL7HjZ0-r_&JNIg|>!Z=F~Ck=(bQ8!+V^^pI~DUz4si9LoJjB z!)raaRNPEsR*UWNBW~m72iqdCHMqUFd~#Evq9EfRd3*7oKL)3vk$9$EHKp&hC}5I591+p!&KGFPF-`6l3+xqm zSm5TUPItdRlWw=%KQD01N=;|-pDOoP3fwMmm%y5srf(G3A+R{E@w)`hN@Vgi{2vy4 zkHFUj{y|`UGBe$iuKRs*|AD~Ot2F&50tZWdj~3|1%mgkxM*UTxNGryaMoW2YkH;U2 zVFZEe7Hn5Kz(noQXFSX(LY_})Ni&keI}g$vWFQhZw#`q|DYO(#?DT6&D-Ev;gbF+d zrqkIw$TT-SBY<$)uWhzyK!MX8kNca0GNiWn<1H43*rwJH{1FW5TrLbS@kr|`E`}~| zJvrf51!Hki(bV#ZiLLS`fp;(OML2Oa@5pYUtb~Tvt7uM=`fF%^l&3v`*7Nrm8^=?NP3r9uxSifW~} zJdYupJ-;+VvI{J7;#=VVh+hMH0AGI~kwl$k$l%~q3RPVjWG)Uz5su25&ApEI|f^aMA))YFFQaMMRHzl~X?JUR4ZA{U^-a00UZ zesXYo!<4lt=5MAcfuAhhNtcKupw~c}qP>vc9`~=dB2n%mJtgp>Ilzb3?cKB33N?qh8(iHI#DqOWlOE4Jn$?qY(U0E5 zua3l4aAn2)O~C}O6Gf>jh9f~T4K*%+X>$HpGn0E35zBP`Azh$(Ryc^-_sm&TT{XLg z77RE8jQ2?@4Kbwf;%#1rtMAb8P1pU!U77L!aNYl0?mu$j4L>)%!Pnic`93HxCGh?& z8vjFqhQ7~r|0R)kkw8QDufo@*+=m1fNqNq3m8)9r7YlsD74Odf3@O*80^RYy5&RHW z`JQ#%mq?j4~Ha{ zF305-7FsaqK!za3F7z6tSxhRzU=JaZVH!7#zf$OFtK+p_?e>#e;oV@I)|#xGSh0e8 z;zCc@!a5Q}iPOR?@k@ryK+Brd8Y=W$2_8YL17Sj=>x)KPy;O;sr-aB*&uk!cp=Tw@ zi*Xifaly7IIxHFlcqIqYJC_1EgF;V?=&|BWWtSCDU1M1O#^MMqfm@zc<2~W=o`rSe zJJQRCQwchs9{Di z7nbWP)Bfrg&a1P?Fv$$U$+iZv+CtANi;xWw*eg6>N*DISrzQzp7G{i(L@D&Fu5%2_ zu&PO4s>6I6YDHRCPvG!W3O(%>25w#wCD)7>skqZ=7t7WqA~`6Zp@n*gj$0nA+9I0Wf?xT--Ox5-aPqowT-A%B0lMObTY&gf#~N~;h_;6(Q}{- zS`C;GCw0W!DM-CcUo#t|+)I+53-1jE0^QjC9B!G;_)?&T;lrn)XJ&3fcHBzPgJEdU zeVX<=EuN6*^-L}^>DaXdLf-IDRbJX0NkqyN{aRT5*3T+vDnTp70D2%PAq+nt;d>8U zcGDlibg3chb$J>TupCVFhF{%PqMz_gna=-lHE}xsmpayC8QCRU0gXju94fxbN8JWA zEo(UL`=~2^rMZ_S;}&QXj%0Jp-{3>-W8Ijapa?n{wj+{Q$j1bb1`GIljqrhk>Xh$! zsk+qfAJOoBfhz<~68P7Lb$pM&TLtcv^xFj9F0eyjLST!)WdauptXjNa{=C^LWK~)f zYR&?zFNbDgv6yB?v@{&R(~ZQnq3bxBh)P3P{UxePDv3*bRP>gapsh#x#p}X8CxhP6L!-$>xqVsdHl2 zP7gFF%mWx$BVEq{O$EqI}9Ws&n z5&ohuG^fmZ?Vql~D0iYZ8V?+CO!tCulLo*|&cv~6Bnv#_;Y`yj81Uwl z{eF;st%Teb_)l2fQ{;rlgRSrd$Op66h9s$_+CuGc66lGteuIYnZp@+M+O4EiG(;m> zF&jJ)Z}gNjUWW-FB`m>Q5_17ncwR~TJZmNv6zBqeka3NfFUVkOyrs7-s-?a)ZSr#^Ta zf&)Dtq}A$(UgMov62F8^Ouwgq6;VY#J5>(!U&eDQHhCyqt866^b|WlGmv2^?;i zF#1b+x})E#Fm<}pN0dj&w-k>I(6Pd)#o~xbrE#c%>~bI-Ud~&UnQkSaFr!%!#`|N| zN?5GNLS>^RE6nez=hx1gPjfun=tnqG%Sz4GZwX>~29I0<0lZ{JW`>qd#)d_1{oyoDc~iIB3`_<=H^5(Q(F$w0AsF5wh`2CU3n%y^uM zm0>RvnI54vUN_SLb2hUS$~%5m6;sZ%H2mqA8djgJ;h(;sAv!ed>Wh-?6b=?t5qJc+0DyytJWadUH55fDBxMsksh!Pa3|pJ0rvtvHv{Pbe^!O`1xo#O4$=dD zdoI!g-g6n!1MUXg3V7Q*qzAnI3Zw^Ift}Y50e)vb(ibZAb{*0KUbg`00Ux{)=>boz zM|!|l0e1p6EJk|3eODnp;5$o^9)0P|tC1e?H-HNPZ@mWT0l$JzY_3 z|DQ+?c+ta1kDcr;eFW(N4*@O&Z1^7118)32(i8qEqz62!2k8NqJ&p8$ea|5MFr`*L zi}ZjK_aHssD}Yfz-}6WhSpFi?1HK8k7qH;xNDnySC8QsYO0`3Le4A={}1CYYW8mOEb7O9-} z;+(u;LkhO$C^Z&%`de1)RWJ!`k36FImfYFH`C8&;0yZEXDjzU@8PF?^62BJliKE1C zNBp{@#6OAnTaFUHAMtl0z8N-Y%U`_#EmW87FyN=Bde!gHX6$&1L>Nnd(8J4Tc-0>W zF;Mvt|JWD2Y7pQ+@ymeUb*5L%$dZ07;y*_G?dW&x^bYy9BmSndz3Q1P>7PV=)j3}E zCo0hZ^6f|bg!8;=c9!xTMtp3%S52V`93cHz$o0TfuUeTU|CxwC^+K=WPY?!3Pg|s) zI?bz2&60jC;>!{LMwa;Ph#z*bS51eU1IhO!;^*Q$$ZOAa#9y{y(CyF%)!%-^-?!Y$ z^*B)a!-)Th->crqlK)un`A&mZZO9To6Y=K;yy~hf@yigu7V#TN0R!k~E#lRUUbQnz z`t69{iTEX1;-5r({#vh^ltn-L5r5G-ubM@Tc7Xg3BYw>WuOjsg6h9VY(YFv^2{=&v zOyKw5>QxJ~q+f>k@teJBl{4O9-)j;7ZNyJ-#?v(d)!%l+zl?YfAqJ5DNyLAS_&c-2 z???QWPOo}5OZ;KPCvHRk=G2cvzOiUGH*AG`(9=Nq&qVw~U-hbovgm&q;un40tNxxP z|Fwvpe;4dCOZ;}khYdg|rAMvN%?NvEh;twPK^ly6Av@G#sp_lsY zURC9ccj#v(;=gu}SFOn+|1!i6zt^j-Ks&Sb=SaU6@k@7jRm91kcp-58BmVjOyy{6p z3{?M!-|+3D)IZ`+{0{6dOa6xuzxhABYDAX!u^2b*`fm32JrnWoBmSN&@-0Jr=YwAL z{Vefo5r5G`UNsc;Fi`onBfjeUUUg2E^iLwb5%F(l(cgZ=*X;DFzt%YTJM@2;`2W?b z9>~IfEPSzd5nqsn|4hVx_&2ZmL6-E(5WnN^UVK^O$e*qesD9TX{=~yxb#@m1+YvwI zA70g33}RFNHR#J~*-} zt9{Qz{8=YfsUD~OaB7`?8RFkOxk}wfI3vF!el6m^JgQ1<$r8UE@kOUpsb4zfbJX9H zh=1eMD)qxG>Gvc4E2FE_dCv5X{0}33*O=__V~1jHb6S;}n}t6eaaMAAm5OAEUxxUv z9VLD(;`7Et*L9b+ivz;hj3brgE}-r%RnJ%$_(H3HEEb1?aTengk2K)UkQ9i;HLry zkI?y@BJf;+7Ydv!@G61mAz9>A0&fv`m%s-EJ}z*Nz+VY`N8qOd2Ny~H0?!qAp}@HU zuM*fKkcIdsexhRU*^|7b-d2Ca-1S}j`-3{be+Sk3>I3yB{CiIw;=hm7pVcSoFX~hE znd-y8kJaD!@38uZ`dl5M4Fq!ju5$7BrW%|xB&Q%}XwC^a#W^GKuQ2Bn{yQyaP|jFm zfFclWALtB5ULu=@KNEj3uIamnejx{x_@n>kf`l>G8CMR9G@n=1YwC6NEA@)nhrgHA zZ_-h?GWi>%Q$A{QCZ75O?gJ8~+|tKgQpqs#`sc6`5z% zbNJVz_VC|R>IM9JME#8ah=JiR%#<_#GaT_>z%~01IiwJyk#vEziVPPgyk4zPA^2WV ztk0}eVHH+N;j^w$H>$O2om#JM!oM5T&G<{GThwONscutU_;)KjPx`w< zeMSA7`l|XGX3}@5O=_FETWwe0Q1?2sb6p>;e3L+H;_)g7`z@~IT-8)${%_1+fa0@t zuwA%0%v6=?5MEeXVbpj@S{R7>%%PF<^( zIpi~3o%KU?V&tc~u?&$D+V(=iO923M!Lar(w95m2zB1zoZRbeAj3YgAkAxg(vq)!H z-jsRojH7GX1!|yhli)WCyi?#^0%^;23jZOH#%H>J*uJMbjLYmir=iB~t@`ke&6|fP zullbuo*opa8(w_tglCG5JbUQUU)QFl9jN(1?mcfmx^2y?r#$|fo5uaesPhjz@zbuc zyFcz&dPk_|*N^=0isv5tuQR__zVhZ-cU=A2!QYL1=e93TzWUMDD}VKiTh8*`dGEXX z`d*KGy>9!;@xT00+ch2KOQs*5{PHE%|0=xt%s)*1-Ks^Oed(%U|8ZL7dB6X`IqVAO zKq&g7GMuCZRK3sp`6@@{;U85DQD7}x1ATYdY6~Cg2#*!{ z&NI0T{{8Wi*eNHMPr@4|V1Wyh{-}}1k^jG*o(qkiTKwgr&EqKpqqfVqWc(H5ZyA5Y z?Qd}+$Inb$=km-_^E*MtXXAhQ#g5FqBPm~=#p&siWQyR=H*W#7}toib3aO z8cIRViMY<8l>}OCGSV9e6vnWEYYF5InLuFB5Xw5YfE}>hoWa*|T>dP8yg~W&o@#DE zeh7Di3Wgw>GR!9><&4=xzlC`%Qi8!>#69{%FjH6Hw;)HFgqqM2X$wy9Cu70Z$&)5D zvgu4{ZVfdAJd?^Vn$VC8wKjSZu^?#L8ZVrJuNE2t69Vz%gaAI9DzE=1(x;gsxq`u1 zRrS`S@`=;RD^yO0mW>Knkn=o#X+8G;M7Hq%gR;SmC>e3m33($_e(*xfN;$$bV#6`&Yi4nRgkMK1@T zijKbyG8+a}tppkiD42Uw9Y2(Q&(uPW^joF|mWdKfIs-MgG(V%hVo7h5*OVo_Dvz&e z!#84piI|2h<_aYb#-gemF9in6t7gsfB>c^)yg8gKr;is@dE=Te5^I=<=@|LmCF912 zIP^t+N+4I!)`TkOm)*(}*hNQ`<9nSD;v$XygkO~hTYUKDwJqptX+&Ccr^@N;=QuLd z;Q9a}!4uz)1dw3_Z17XgyfvQ&yr)=BucF}V6OaZQlFdFpHjcpO>*h9^Y~b&2%zY@_ z6fxKS2E0DM%G}Wlc;*@^GMB>6RLK7!JRRw&B^W>Guhw^%D}sq&Mpnvw&?RWmNAPE2~U zJ~K_y*9f7>-(7xsChkmc)_Xc6y;&ck^uzGyPJbhCBp1m?!SqLcM2ukctnbqGZtm%s zsx!Umhl+=5ishzYlEB!XS!cW1l|Cx{VzfvnNS#F7)4`-Om|Jn-%-{5%OV82iFt}#~ zlfOZ3!39woF^#v?BI#=`Fq9e^{Tb}nap6qA6FWmv*jcCZr+2xW!JYqi5a~?+;FUW4 zgIDVGuTkT01b6=5LmW{`Gf}j0BZuWWy<1=I^pCmH7fbr$<4pf!S9(j*TawB;tt{APWxRMPLz#jx$uq&MYy(Ut!TvOfBPUney5Amd=}4g7CliPGe6)>rpRdavZK zQ>WXHN&jnCdMn^(QY)YnZZr*77+3-g_&qL&m&w1UMW?^NMW=tT(NJn=W!|c{aIYyd zBTV`~WTN}g9?X({Ye;k5>Pm0)ZqR?rlHR&rr!O&t0^PC>1;ULZ(rQWntSi!Wt4_(1 zzMxf8MvjsHxGd>cOZxe)3|+UXLef{b@_DXJQ}Q!uN1RD-AUzW{*A6n(5!Tpa>3<{= z8QXEDFOKN+^IXhbx16`Di()oA)@aIYXKSwG0P68)?B0wEG|UW?|1^G>jpwp54rnd| zm(|3%A+49FT(29A{Bq&n41~{9-U0E0;ExPMpRbI+p&TI(y^ZlB9BAY_L>d1e6JMar zxSxqHRAxNS#1FNf%VgqDu*cs_{4iz4)lB?wWyZ@){0RFwRVKbjnei6gQOfl9nfOzb>Blqir`pfIGV!C8>31{n zW0dJnGx4W6Z|&W3plo;s@^J_ndV z>LYtTX$YuY4uq!#i(EYUH}g(Ie@+(qa^Q1R|N5QD`2O{KIph1+FD+J4zCGg4;g&-i zesk0qwNJ)5Di4LV_#=F;;7vbs8}P)ZqS%Y8bjT+ET_7R(3taa39mbDT?blVMnc#~0 z=N!C!?6%LJ08jZ^u6cAeJ--V2f%H#LgQ#4^*ZXmm?myoU{Ad^cUBO!}{D*=s6}-{g zr-CnY;gKold%g>=$J;UL0vG;dp&#$UTY~qv@aGG@+=Zuips2hPT=G{P{!Pf}h*h4_@(Hk|r!8Zwhs|z0z{AL%PhIf*4n+s3FCgIy%_?X~3T==Bm zce?O53jRSC{#L>7aN)lu_!bxb-vz(ig}>L}ML!Ul!^48#CG>(;KO%f?|NismM3CFR zz31){qW1?WP`jl-=PMBYI}Kjk;r&Ve1y1nvzAy!T zXBcpd;MWGcgx2pe1D*r?NYqzp$j^9V4-z`K=AawIR*1vgBA!#&KF$y-XQqBE_{dZq3;?f$aG$H3jJ1B zdFkDK;{Tuv{}slMR{NSW^|MXrdnI4v&)o++ticX{ma88LeV4WO=n+24UFDrB_(9Si z8hI)iKU$gRuPw|C^C96+-w9B7hkun?AbeU}{1*Xl35^r@v*44!JL~;+Dc7ycf3%|G z04ba)%;>u_(i?sEK!Lw~0Q@G?k5QvtdfOpYR?Zwj8ir=V~Z|3crwr$hKyg8z`| z`}^B}5&9iMZ|t8=#dGR;u;hC(41n72+b;Rf0^Uhaeg=gLUHHAi=W-Vw&#gFI=fXcD z^lO2qe0NH|rvKc)^uzhRePWO!^qU1w-+NHtZ$1FODtL9Hm(coK62Q9!Pw&T4Xy;!% z?+2dp?G^pN+2Zh!;8QL=Jj#3|F~B#VM+(myKI{E_Z{&Z8>4)=oLli;lq!eBe`f0B6 z{zmBOJ248TKY2^&Q!f4=2t9pwLSZ5QD)oubcewa}#`w{yUHn_za`=bPA9C@}!@AK( zjHeyaUX1+=1D@L5w>Ee=J%1B}D|!w|c=`^2!ae+p=K#V-x%%OAg`VEqr|`DauSf9o zJ~oB(1b-3pNzWgR{Bwn#zTcoQP3Y^G9`d{V`Fh5W!3Sl2rZ?rfPWaGwDir?Czu3>4 z@p1!DBA4yL$Lr#AGvm>J%KIu_q3>iq!}&W6Lft9&uN(S+mM0}0v{|C8{iqZm0zg1;F2tr{=QNPRB&v95NPkHuNCEBbzsLbE(qp${+#Pv5mr;BQ+1 zM*&ZAVh=UO)4SpnzQFh~YKN;`j5BzVr&tWjBYdK+_A&{0XMcE+X0NUgK6K6{2Py9& z!5?y!i@pgW`RThh3jA#wU^CN?R@io!@y5=hhW}SJ-pH8{{3kB{^i2`)Y5Fbf|#@R@>Xr*9d&tGowVFLf+TWzKvt#*lhn)3cl=;^y&3b^Hv2m2zu z72lnypAo=QebIMP6!=>yz>|c2w9w~pEWRfb{9c!wX9^$s9*F{flLT1Gct-J$@hfHu zJ$+w9!K~-bW&WepURSvmy7)XP0yPqS?r4SmG?|b2S;>6HC^{LGgVg&CE)BOI-^suD)}8Tk17PGo$b3-V?Yg|i9zGI2^qm)lf*c0wGoddPdXw+x zLQmg~QaG1?VMk!d<#O>KCiu;+@)ilc-Gx7q@fg44y+~vKV}WrkofU;23Vylp@w)h|5PXm1Yx=PS^O3{= zzn9C+OpkF>%6p37x4P)RE%kCgAOw}Yxo!boA9?p&gp{xo#1Food zr|!!24jCzKDvHyYK={qnA zz5I)D6L=a=mrJ`V7X0}_Pv3P?_&)zCHI?b%U%BR$(}kYClcQjsi&Y7pzHg=QB>yUP zh45J}`Z4QuO9lVFtG;}O{t-WOI3j%LSQaWTeSb+I#=lCnGG1-~&XUUxp{MV)DXijO zd>?E0yV}tfga4k+*R<2S1i!@nDO!P?4 z^qnXL(_RXIr~Yu4Oa3CEr|&u`{4$4u8qM^h)edP#MxSRhy{4hxZPKA!D17MqN(#oV zDg{s9y;7j(oD}8)Pwk@R7k-V9-z$Wk_Sv9-Vsco_c)0=S6Fx1#Q@Q$F`k~_zNDuTq zErsnu-!AkmEEX}FIC2TcD)mL-vt0Oe2;Rqh zp?!$R z9?W+TreFOl(~A%Q#(qY?VW9F>o#W+5-ctrwV}K_++`4@H~d@SK(+OJ>eX+IDOW}RWB&@U8v zBY(Tl)BXY!c#i?V4#qQze>&vy--ORnm;7H7yw_!i-(>t~wNv~DQ{D%Jey__up8%fp zPy0Fq4RFL&Y1E8z6bGQF#ex505V zZmX}kEfU7(A=sXg-m}MXa5&pJpnN_$5!hEduYR%5hr2l$cbCt0L^VcydXGRKzt!yX zC);UrT7BSE`Gpl1PE!e+uGKce5&i_a5i%nRn4#VnLEnHT&Hv4 zSExA`-k}hODm5jDCm%4Rs(ieMJa2u9k6myQ84kU{X0{4Ple8w|bVcWv`mXn{^3#^K zu{A#4p;Cn-dN0g4uCOa3_UEMYSHS{14wg@ueDPH5G3<|GA9f%1yyUZj%co48I90{z zP@(dRDyCGZ>nEz~C#&lxsq3exD<-NdCaF3fy^)Ts8EMl^A5Hsv5)ZhiG)A0Nz0)j^er_rP%`n~%2U z%|Ph7^v$`tu8KBbr}xOEesP2VHfN28al~i~-ZiK4B%{2YGw*h)0z?;BVXOf=E5kzK zs=glkyW&;)Ca?Fh+Ih2P`zGO&uBi(9`M1$w#>(Edo^$rmIU@Asfo!xoSz#ZSFbLE+XCI7?R99+WheqC>?#@GF z?327o1g3(SY${X$TS*5qxwYUBMFm5`wvB-nwYnt~Xn|~@R@IKZCc%}>mQF~3Ikkal zg_`egZ-_LmQIutC7#Si9E}*KdgjL)LrwD&L}DGY+K)#%9w7!+1p>XE4VzW#GJn zjgv?YRt#!{kEMca+H#=;AC)@}#bQ%Z7;ea=6<95uzJYiu5RMs$lL;-1;+1}>f;Od9 zW!C~pLSKYr3Il2!_^J=sLDEQ}HQBp-Z_cnjX6+N3zl~XYv zDvMhYWgM3+x2^_H6zh_zLs~7DrT(Vf9%{OYLLrXaS)Mdli8`vlq3cyz~7!`cz zaT-+uo2xd3+Ia_C-Sg2Xr<*Snu+nUEu5d69cDqh+JD{q-|8#MwtJAxNgG5Er%`_1U z_+1Ut=WC2dU|Zov*fMpC0W?*$YM?SQj)nuWPc}!Ly$rQ_*bB4e*d{&+W70}zcgUr} zA(x>{acg+g2}IYx=CKQLD+V(%)hPPvdf#FUNY}KexqjQ~CsWr8>P#l2M(TQ0I7a;| zj=D-$;8e9l51LSk*-_fA-HFQYYExBj`G03f*)i8lkoZQ9hHm{XaYWx zA%Ty!0^+$~FL)f7L?;QXz<|ijQ`#(bu(FYJy4CWjSFlj*woKlFFNSUn7QG@Ag-&S~ zc`BQ`Cq-ScRkk2T;fz$Bfs}z$xND%ww$4Js``G%h+Q z82ufbA2fsjoy$%GPGeJC&2EX1LD)NvlP;+5t6(c|OD)?`@ zQ$Vik!^|!*SGi^(WA8aWAIP-oJ3dx z*G>{gNOJQfW0!<{NT_OxWAlI4_<;|hVY-=GqXUdq1<9`qIE;Lfs;R24@zpI-Np0+_ zcqmz@?NgiaB$#CzPCbLiz$Z{-@=cI2#3!l6^B2siMnBeylckN>NTp6z%|X!^o$5?Z z70#~9WYfQz1KI&(zrh#eF9lg`Y=ZN7$ku&%8%C+7fw~_ag>}aKOBTSLx@pb>6ldvD zs2{GgP9~d+Bj09Y%Jk`E&=>GWaqe_b)fzPD;r|WbG@x~og3u46=uI?+z)Tu(WL9SR zSH^wZ;?P`aUwcd(qPl8kFQ}_u44Fb<#R@^0Taj4+enb;|{gzBN)CG!j3gyd?BATSG If;x)-4F&{O+yDRo literal 102109 zcmeFaeSB2awLU&cX2O626EP@i)KP+h_%2ltv=JG_7i!vy;#CyOOR)t-Ndzl_;3PHE zAxf*Zxz$^V@!o4&Y^|k8ducl$O=3%XQ>DGw3mUIf&p4?~ZK|nF<@Y>m?|tT+GcQS$ z&+o4j8tmZoKm^fImO}O7K^XY~>sLLH-?uF#niFYziY@ke7cA*BANt$NauB zl`e5_27(Rv>jlBiPy2)}(~AMt0{9lB@vjSE{*f=z;NK(=nFQMWiy+KDllJL9)+|Oa z>z~Pg_VU|5clPqdXD+|}j@mV6t-AB9^Hg4t7T&M;)I7;cKA0znzlr!e9e)$_dpVx` z7gi6U%~!%s)^U6=KmQ$#zvJVCJ`nw4h(e-bp4$&@2W3~=2)Zwdj zc%=?Uv;Z!KQ4qdGr&GoZZ`I)obofpkenp3!@{1tuU7h}UBryNyb+{c*hVRp1RyBs- z(qY5TS9Ewjo=hL32|TCa8P9(|*5QQ`^7+21!^Womig@P#rB0_@7=A{FEe-!4I()fK zkLmFDb@(bBK2L|w(P7#Y@qM7f({=byI!ya#`uB8ri4MQ1!#8UBf7fAy@2fg|r%vCY z!?im6f)0O2hwsthhjciq!>lW$|C$aP{M9;a#d((apxVkuBy51?wVU~^}(eqqAR(;ck7kc zB6jiZcidXLYRO{X(xuC5S1t3cs=0g7%6olF*4$p>Teb4;+wZ7Z>RWa9ZFd0R&Xr5< zVEP@4R;=Xn?nTS)_N`oU_uY5it)h`{)$O0Z>}VX!)J1miX?`bXVNAeEFS=m}AjxH7LlUntN9+x%G3ms>sEl z>|45O(QS7u^(|d}_w6-He7DuydAopvv85VG&Fw3etddA@ee10(zZS-d+ipjB?p?L$ zPGGp=nk#2rcI$a(oom0HZ@Hb z$|o4z&LM^~@RlN9;^BcqhYmHqR1>fsB!UAFqqT2Bk#GJ@FTQZ-6DxuF(8L=2 zGS8ujYw)&=uc>ZiJ2Y`E!%RzcNthZ~Mir)#5~e1Wp`^alvl6C8mPHueEMaP9*(8QH zNq7^(=P+C^;YS#r#_&oBw=i7A@Inbc&hQ+Dt0hbgE~{p^O2X9SviS_3BVlTE*+PaR z5~gOCu|TOZ2|vs5N``$B-pcSAhI>Cm#Ki3k*E8HL;T;S&G2A6#TEMbR3@0T_OIX&z z@Us%8MJ(IQ@Ma0qGL}8f@Fod&G5jpU^%CC8@OFk*N_Zc`Nro3nct69P3|C8-7PPF3 z;VKE!l9ugb_#6q-qLy_t9FZ_BYnjDxnS^^8?q%2~;Xa1@8Secj%iqs1`wOXV2@fzF zWVlPhw7_L$3@0T_OI$Xd;b$dGi(JO8Kx(suX_?E|bxdtS7<7E+{^^$Z>#>8q)z^Jy zSsDEOvIu@Yef_dg!9dWu8cg+Va{Yr%$9jVG7e57`;HwFxD`H81+a#bp^inGyiL%C* zYSZljrWd{V!X^dZ`UtwQjmes^l&udhBRl++j62k&U>3Xpz`Q@Po=M?tf%6cLeRY4Rw7V0&)0TNdY*RdJFDHN3IKj){)PkIMrYA`C@g!!0OqF zXmDqDaiYE-(TBP_qP;=nPEW@R`*`VdOw4I`VT+hP(Zq~1F~nL)tRKXEzShN)OM|iQ z5|peWF}F{G@m;b1E7{K6le(HV_|7X0rbi{BeeLyp_2DhNOx&*%2UmTD2r^mJ4 z4AC`LA4){~5!LQ1imm7`O3dpQpy|6-zm_v=8#zeKQ>2&18^%^mq_jk6v1HMc6kh8Z zC9Z$T2op)M{t@fupfJ-|n7_k4bn35GY5`4E_w z_&7?6$Sy{{{|_nAJA6N>2_>4_OM!zQO0*@uYdb|rWnEJlq=--?U)*15jX}oTkZm+q zWwW~g(Ns($3_tJ*WHp9Z_B|S6?(Feh;cc^uV%@#5&Op;FNGB&ZyAs6{4~6>=#f#em zRU=A+MXg)M!6uVMu%Og0QSN;CY~=pIk&pImF7}baRVh^O+!))dO7hTZukz4l2WpAAx_2N3B?$6|5W45w+MD!h5zcUMKd%>Uu&<>|q0$fKzoO z_QvXZC8so_iD<7gu`gEF=V#77dP<1inb;qz>zADUie|qvaUfPVAUOwA&H+j62=qrv zgAs_nBQSusg|NPkfbV3yp{8{N{CIl`wYnn^#9Kt(LU^N3ggnrl_gSCc;PbU@hI>TB z`HZ-p5l^Xz2qU75cv?kZq~f!tGGdF0n8An%jCfW>utl`SGJ-zWP$^*N4Ns9PDc?pwtGl@TK3t<{yTX?vNNu5mMPg^B^kR;rk&7?g{;!oSbVo4Id%9+%~ zB>uGRQM81^zpqD9kAf9xTa4&c5fLA_`5#8~sR-eroe}*iLMZ=;5d$hh=sm>kv_sKr5I7JBG|vO_Az2SBLZjmN`ogMt|M>`-dK)~ zz*M|N$azO#Cf>+$N1zICH*YJI+if`fjB=x?B?-lCZ|9!ldsdtd|S)n5Q{IImhXRUcy3d(X@ zyVk-gW}?pt(q)YJ0VC$1(K(YOa zXppVo`+q)kXgdfRph>OE-jO1noD2FzK*Q-1K27h>7kGa|pd&hf2w(bi(Ae1>Ku>-e z7*-=0j9(H}{4ki)%-AM5$z7I$-@A(>uCgCjt$cLCm;RVx+-z0Q+jj>f}G8Bo`mT zY}7qRFeYlH#>1YrCqaY;z=aE14f9b^>sE{BiW^X<7bwd8PHA zNK1VQazats!2@LG0u|X$ab&&@`9Sba!Pyg!_NM)@XfHDLhPU}<*41Fp$hU@Mt!2lV zBFqyyy+WtA2yHCcPyGx(XlN7uU#z55MfW|Vkp_*%WVrEP1wf+qy>sYL`~?Rzz;+{U z`U|!9WU-30rycM$#E!T}5LW~oy$n2nK(oKZE$U}9N9Dg@o-Djt1U<-_J~|fdW1mrT zPj)$%l$8fE?=>?2Au<{OjG-O!rb?H=c*xlbK*7Y&lktTcZ^6`tf@`n;In)e+W%L<^ zq^;QQ%9~_HBGxk=`o(+!%zF~5AIv*ZmWYNB!&e_i?RUXQSJFtg|4HyBs>YM#a?G-z z2ByzM4WKqh)s6w+Dgr(P!1R$SKK!#Jp||wFz)?le@9|OX%mTH)fGpBpZA3cQOjMl# zlIS`4YU8>hPHIhl7=RluYU5J{`isJikHGu2w$MZ&2cTI)%Hu$}^*Ri$A={>VU_thD zK$k>M-?g4~4l46mcX5bJ*roC42jQRNFULSwTugXdRZ*-vjQN*@zi|z;9RB&d4-%s_ z@lgD_${s}8cMM=m$ z{JgJ4m+X5)Is-`4V>1TCY>mm<&A{r&s&i~-j*%i#2-?t0lsB>=b>|={Q3d7l3+DT6 zT3o-VbPrsI9}Og;6Yq@*0Ov3qOK9hNp#?lHjnla5eHlq@sm8Q$y0i88GOjvFHayBF1gw zI6ew*due)Ccw-w}f|W!wtc0DOIYdd*(5XUt|0l6Nk`w*f=Zx-8#4uEXayXFFE^5+9ztbcLs2^t80pg=0XoH%x}V^Crn4<5}5kzbX`zxEq#&!Vp<+M?TH^ z7x9{!V&sVOd8Bu=OL`}OnQS(0$gnYF>0Op#!O}?G(mM~aw)DON!8)Wj7@PO}F~7_x z&*7^2>&TlBjJDp!epIX9`bK^YT0)^W^&?ZN!OY?FK$cyWR)vPXs&++o zIi5o%U5=Vh4a4?6_`m#|pXDHVBYQ*Z&mF2QwE=Bv3fw*X3tbt!4NPJg&7+^i)8cEd8TK8l~hw7MMxn7`%<}<}%uiy@#)UlA z9|%9R(HlEtT}T(V8bge}#GFdeLxk-vmzT6j+(ce(1z&D0b)=3FqR^ZSHV$EYjB#!2 zLTS)zMzja&F}K40VlLZJGsxq*(b;X~53DE<>%^>ofEh>`)Y!;BgYFeZA(!YO!&p_z1**R*ykJMf}kg>CIun!sS{}Pd4SBoF@ z0s#!4yIDnY@qvnMD)j~;{R;9s%xEvoXs?*jyuI2_#R>O0z@>hN`q8>lGt4gVcGhnh zn1&l(^7`k&D$hg2JIYb0!(Mrw*`Hs@54#n|y2rw3^|q0>JCHq>3`MrN<`tww(~!%U z>tQd^|Nd`*5@|gyu;L5$QIGqSJ8=4%#JqhD3)sO@HUXu$^@>96U~`mhR9Ulh972>< z3+#Zk_}4&!6+jyH0icTYmxLRZy$_Fa5VJh7-LuUUR=J)NO@ERy9dr^0U6mlb<`|jD zKo17HZhF$kv3G7e8Muf3_0Q=(k(syM&@%}&31iPo@c`)ez~;=N+Oc?j2CryGMr@cn zP|pg+;V4URHUeb-ombd=sd=qYsymK}HOz%_Lr6a@qq(u~pMU}EtUt*7iAMS9)_PSd zp4f$&*v3G-E7n^CY8R-%gaE{>B1pdsm@q68Opqfv;Gh;Yx*OdIt7#upe46y{vjI7N zGk~`Ouyr|R#sCHln9-~tS%fsxZIACl`A9{L$V>?~3y739-0%cIP)3YrGjf_`cy3It z8+Ivn{m&3f@vi_B%4g*(%Qpa_%X052EC)*nA?%~|{t~6Y`=9xK3EtCOFftH-W9-w2 zg?;OJN@mzqNWf-VfX?eLepV!O4l>gi(R2-v@%Pyr_VR z)6oL~3tHS?Yk(&a_%9%#J0>*~6vTl*Kj2>72^_EfMI)X=*k1rv7h`-!pbJ1?602c& zX=62&HIX*~LrL3>c=}E3zBhJxIo9W4#aS2y{t~Az( zohsM})h7)UHk|1_bg12Z(|3g*s%5Wv9QT{a4lF=n?GFt~Q*mpx)Tr8{!7^p8ppXr; zxIVZ>C0}S}nWBB@Y53CPvH8ujp{w~)blowm7%0N-JWi>gR=#3(qMfJd)J)DQc+Ju6 zf%`EzhnZJ<6I+Zsudsuln;h$9tAKS2m%aWCp22$YbiJ%~J%(%5n4-tn>0o>GuRhs) z<&YRSf`dy`RmP(`Vs$$%T^&ly+mY};n%pY;0sWOLsMyHo=*p5Pm@oB<(|kT)DoOna zFK%X0qMDF_`!@sEOgL^qP*RmF&D9a%1o|wYPn}gELGG9m+&5$e!9>NmQ z6?8)N%`z>TjF${A_cO@dE}2c){f0*}Q&rJC-#`}U z8I2T+q_EIqL=WvX%_`A~e-35a!ZNOK+h~%Z7b?w!eq1~o@??K+}f#D29Tky zjJkHDV5D7W$|FccS3?8J$BUzYMQTtx`;JWZkgLok8RL8+ z12fvNsf<&KfBNn2;t$n0{n|J`6&2%b8lEwj+-1n!UeC-%3}XzB+BmCoi87xt*n(-B zV9Pb^7EHz%zDyV~hHMv*rE@W{xf!hGz-rpQcV6P?1+z`jB!uEioe403KOqA@PQjNT z-TIja{-3AV%pPq@Ke!QaSBX%0K9l_zX15LBVFcgIz>Ig0fFFNYD{fYW4xn~D$w9{F~ z3;%rX!T8+W5XDBZ<}SQFr0rU^vo|K!Ov;}c>tDAX`&T%8mmM{oc%tvmQG{ud6Vcrq zQ?OO8M>ixfuah%9+dgTtafU53Y4?kP!TRq-`7F}!Y!&>bC}$cRS=Ps{r`?K_8u(8b zas22+n~$@ILwf+fvyak}fjQgIaWn%H^787S9e+WiURmnwF`zVq^k61KP`U@x>@RJ) ztW+zH``VQ9_6!fbWLIYiBPy1<``1#~c`PvI@-S5p*O=G%Zbf)T_UMOA5Y@d5LaHF$EXX+@r6B*fNEhVZ~|^5HfPorlKKLmp}(xeU7)VTT){#0Y|36YI@P#V0C1`IG_=xwq)Ws zF7Otn>Q;AQ8UQZ&xIwd(`_=8jup#NP@EsU9WK+WTr25nezT!bl3vphk02J&p{Lm8w zL*t~85Cy+Li+Am`PAcm9ZNJ&2Xqp+WL)arfsP-?@-EQuqWBN~p$>sE7{l%F<@|y8l z7W`IK%fhKPW6(JV$x}0Vs4^SY*#I4rfuX*_KVNXrC7Lcf7sP}q4Uv?mMr!fM=mFw+ zX_|m;k<;ifflII#!VOEs@GU&3|gHA^yc;e0O2Ag9chsZwyhv#HCr1CLz z|9JSiaYld|FJYIs*sF|nS+%nKy=W@m;8|rJWh%}pe44Eh%COcRLpTP{*AvF$?~OHh z{5{6Via^j17@Hv=BfJcO%t-Zb_)c8slR=x%%5sV->MJb)#EiLl_b%wmFX01nm)NOidPL z#^V9XOxxEBF2f$CmpkGUq6YdVeD%~;RI-&lOk6ht zSEdgYXu6-gYp(6_wGmjz;r%&t%H{;+e3DO{=LDnaG>%a43f?i3Sa(A{g&sC#ti#tJ z=&BE{3``n+bY+asQ2E%(*mK@6l!3WhduTYAGHyB2Rt9G^?3|r=`x=yo=0?6HpWHQl zXPrI!b2f5GtvxA|o!|O+J0m~5-rX5_A0L!RzPIqw%FpOjXT(vdWmI|ZynHs`>fnP% z_D-5+`86)PF*kN;Ppmm@XQy^9nQC5wwz%oifUtH=hBda~#t{L5=_gT}(r=IT``4XZ z7+@Wa0f;8ysC=mpaHNR0Z4tJz#}WZ0rJc;7q$DktdbMYRpUfo7U`8n; zGWq!>vChgVI^pW6F}84Q9FFNI$!#xmWM^NJ$u2E{7TyS>&XQ@n?zUC;$qevOV&oyWd2*L+jb~pJlhqg?o07>z>^dWYAJzv+1ogvp?h3gX-CRJRYyh@JMY)-|pjK zECxo?yHggxX=5o%R;6`VK&B-c0hiGoX3I!>DN9Qs^k>+?{M% zXV|uQnDl%cFq(d%(zARFI#^B5r{@Vq`rH<%B`LGe1@-&@fivQhm5CFsb&D_4Vbtc9 z&j4iBS`|fRd~+7XHIvBRgQK<#vjesdtIFYRo46!ukVrd)nMK6~r;42wNA(>Itho1K zjl@4M1f6TJABX*8fi0uW(x&@a5UC7rW21sDf-Oi#d$M+JJ_Q{{;odiSxWbjb;71qk zC?R;bgu7!>KH)Zxu!VbC#?w?$bg}LteDGsC!7mUpQ#qvL<-2AO*?TGn=INC!a$Uq} zi_#0(fh{9+Cpfc$ulW93dVE|*5JPw!`-r`9zs|&+PMn@B-^(Otrub!rNcC2^xj}bb zIpM}gA$3nCA1CBhx$~?nS&qfQOEUR5N$l<5zI3&_gL^cWL>Rl*6TqU}^I4uiV1RAVXeVzC{JI1N4CHCU=kjMbM) zH`y-*oEWeR=yEXF%yi7ywPTF$uu+lS%~$4=o#x(SqnMa4 zcr2lgEi*qYbrh#=1!elnZ=v)dkthVaECS>_lIdkN@V8tq$2kDL$*}@v`O0=^5LA}cE1!wIlR7u4A{scC4`EudOx7zRY$=}JKkcp`LTnzzR z`c};iyV_p&{#R_>!O9R8&Xb_&OJBqyq|X$oqk5=D)enf#CMwX7yw?Ulg5cq8(Z9x{ z$wV|6+g*LrE&9{`X`*|4hNt&tV$&dxtl-yNoj<}Jz>16TA!uF5w+3Ifn-d6UL__#O zKDwW*q<(-OWXiFfQ@*h22=I(TE^i4T*B-=vV|V;;zA1_?!lQ?FdXE|CM-1FOj~VDm zPX;CV;vM^~xexkCY(2#?7z)})5@~$L)g#|=$tef5zg5(c0v3DK7eCnc7sbaZ`#l?P zlh4RD-@+SjAN#I%<86)&wP$4Z-5#U_|6>dG-Fo)ezQcrOBtXogz@7C2V8+he(@KK} z0&`sZb3dV@qy1*bF81Rpz-j=#`ggq*x1T640!r(Vh<&)pctu$D;sVZmUvT0!z>cx` zvUm2X-NMtE+A9ooVx#GSzi?VKSa^i zW4%p|Gvx7sOJSm;T6tm%Ple#I5?;G0+7+M26I%oqcCjwT$LJPatT8^cblBC}i|BWu zRo8ysK&<;Ae7}_#C%cXx$49i&cdcEFtXp7$*mipq&by;ALg+WM6dS=aQhz9^=#Tm< z*D?B1totaDykcRy^9kJcEY+&Hx?7$xE5eDSSZ5iirS8Be!odd;aqLTcR(bgOKnqw{ zijO11jd!9&0x53jRSpzZd$nftY0#g(Yu!w96rD5Nxif2?jwW>oSE4+P2}GAJi?-~_(4&cu0Opf_4x z5>-K$jPAyYN9sj%gGtjTWwd;?Qq+>#)AK9#K)|P{zy$cFvXApxM(PfQ`fXqBdR5z$ z)o@e2**L%O_pGR|)cqcU{QXw$%HI3RioLJZb-uFV_lam{V%{EX$Zp+@qf4eo`)a0H zRrp>T`;*%k(>foBn&%YB`7SSan|=QZwQ&gnYxYFj3MmcPpSCV;!-sW^k`KDt7;+e^ zm~r<2%(y-J2Gs1Z*w4TMz;5r-8Tfp%VKzff9YNd^wD!Ucr_$8e`oi*K$ujjxRuj+V z6$~)9)Zb`EKaalYt?zK{;+L~qhaPw9@JF-`f86P99eNNWtpkrjiFMQP8yZQfAh2oy z!p~Qg!Xee1+d2p8#rUX=PwYy16U~FEFKc(P<*k|8dX0wR6Qz0+O2lWS(RcCe^-8oe z0*R(4Esd>svq)em!{&d&UwR?CUlWH#*@*yIt76>`;Hw2)0m2P%b8gMNjtB$nsPDg& zVrQxm>*ejXincg1*)=rW@MtCzK9+b=)j@+p25rzf{RbyI@8|ai?h@b=3oLt-rmJ1X zfi*3H;=`wDIzHC@PY-f*BHIPZ={%+QbgQMd;T$pc;~I{aWk^*uh3d_ebB)%xSGy`G8n{j+P1Dd!zvR+6g^&pIf#T6$V zWRD1=!9sNeW}o6Y@|i6AWpO^#4wkpkG#1fzQ28m6{*lsUp;QM>#%@H~3fx zO=w&64NS?~fj>6Q()LQKvqCySYVE8t8|+}ytdSyN1g2Q_p2=u}$t5$<=sZ-x~o{r?|@T5i|&2UhPKK_j! zdy+JWQ5g`tdQoDu!@E?MZeI^mK3OJVs4if4sLfJpOC19%$sk5mMR(;WS9c}+;7Mi^ z1V6uz?l(-0Xo|jJ-h)liKbm*WiNIIBsTmBRJ72IpAk*;BW%RQK$4D5a7{#P`bZe|` z>nHi$(pG%8v=^NroMY~c+SkmL+Koy9c|DLtyr>K44+Xw1+SeEJd4GRW4YLQ zhF#ciVG!iupX_ki1ZJqts7k_A>8GG&NCbz+GUJk*8T01(F7uqrJX*jqX_h)^cvzMY zOL}A$%SKe5lH}FIbL^S6W#eJdH!|AA+<}GTH$S=>CCv|pqwC24u2k)whLH%)B z(RAlL6KL4P0m*|za$YWCC8^`Hqm4c>VfQA8sJUc&ft{0W=z8j{lP*``**f_R zw4yFirJTTbHH3hAPSTdCG$@VIjl#(JA z*WTM)5)v!GsI=C_fO5!cpO;$>y1)UCc(Q7kxFIOKn(SWcVi&&tW3$^n+9@x^R4#VO zSHMWh>C3mD3%+MhZlJ6cm6VOWRA zWYbKJ`uh&6)N5R2aBB+PuvBMuw82bcksRnqp=V%MD)+9HTqYx`g~`l9Lq4=hbv0R> znavAXoR~X$Om_6)>e=A@eslml;u>b{I>tp%*DiZGKf{VHVy-s8HU*~@ zzl$w2sW(uEKOTE)(E56rP`x0xNwGHNY(u_4K5haZ#$Kf$Pjc13W0iSPoJJHp5ZR!R z728y)GluJIDb6#SO8d#vS$@uaxEa+QN^cujK)fY}tW&%X(UQ6CB~^Gr4N>Whjh!wB&> zL6CErSdEc$4YoMau9?D-JC1bY5|WH?D$upyLXb1M$BsLAQS^<~q58TvO70mg`QbOC z2b(bR5(~h{xhMaynZs-xb+8y-O*Jjpi+Si$zkDT z=o#r5jQkTC`6iFLpMce-Penm|H4*pl8q;8$lHoiM=AJlm^h~F{#bcbQf14dJUNfZm zmAvd=HZC*q#`7l0S-6qwSB8{r0O7{JIAo-v$-&8zr(thaA}l1__)|n@B!-c-p7X)Z z%Z65FkwJORxs(%FSi?qXe5bsswTM!RzI1y%&NCU=HL?>QeVWM)qnivR)?V40l9_i> z6LD$*UFJZXJ!(#Hs@0ZMGtLXO8L%tDN15Z}9EtMfw)R+oY*bluk@j>Ujz@LLA=dq8 z2P#_);f6G%DTZ~7VcD*z;fCK()as0vaKi=$v?bXvHFvnwMBV+Xfm74mS_5XzyG)C} z2`Y6ASu^6}6uX;wyjGu~lt9}Y+y~B;CF)tU=a37mkCQi+HkoCe%hl?+>-BDbOJ~ykh z?{Q`HU5RT=|(d}_;ny2_t_=j#t^Zd2N>io40 zJ>$`%=DKjWkyGg)`vaxtwdnE4txW9s?0uf6Yx}VJ#nJki&0GZw@%22sUd+u(_nfNI zo2!pvMn(|?dAYcG)5b%G+N1x#IZQT`BXu;8WU$|KY-W{Q7OZg>K@d9|>L3Cxor(ws zq-@dgY96qh^MHvcPf(LJS_|y*)UroL8 zA{OOCdI8_J9X56^N{~KU!>Z-@35>rD@oME!Lr-Vy)e`F^6)~jrd0h%kH8UJX^e5&_ zU&Hhd5+uV(Xier@j6Eo^L9qOaDN(KeOU2}qks94fAQAv)@ja>D zujKny^}dYnPpkK@^1TA@w&m6ECW@yS-H7NkSO1d?tyUR!@jVSrOzk_%R9V=^j#rQ> zw!a@QiRca*AP{sj(>7!hbnh`VNue9@6TCl;6wp^5PUu%KI$-F3f}!_GQ!UdrL5#FD zd>l{g)0jM;$@?G(O>!Y4FJq+HiP0X%-i%rt2Zk&dS^2Dah%hQwb|-g6VxjgY6#HkY zUps>*%mrV4@xX$lczaxB6H6|1ryf|)nHbHr=&Xh4Wxt0lBX5_WZLThB-3Z3R-{0j% zAh-53V-wz{T&dV-v0xvsCaIlpAe!7C?c5*j+8^DwKiYjDz+EV&CIwPcVI(TsDNzd+<7AEyI ziSTyweVKsa)I8TF7>h~22H1gU@BStIU<7DK{}&>+OC+cohKth|b3;%xnTepSl@U0h zfDZ&#iU{}DCUsppk*OLX|<=Abl6( z$`B`83l2oPOyOWs#u+scrsn}&z%CR}3NH|NTt`yk$x4^{YW>?Wu!UvaEv}1 zw>Dr+eN5!W%3>}2y6wv7oIcO|vytCA5vTYgLV#vufF_|;z+NXbLpv?rZ=0Bh7KD4+ z^i{6vKAxIO)iIx;5<**Ca+2{`am{#)(n@NA_${hAI(-~YTW&`~8nueNZwl*~M_&4w zljU?jY;)^@v-t(;4tnZ14L6By9J=zUr@$gwt%R?L*G&z`tV9v^Fz^-g3q?E{ux~Qc z`gV3!oXeM9iR_t7sGgmj$DPZUKFQxZnee?kJI9~Pmma}nXD`c@eRQtuAf&V7y5AC< zlNiF0_9fv5KEsA}Zhw3(oWs82nq%=R;@DSIGd_*OksVAsi=s={D_FtZSYfkI*g>(z zN%?w&5fo^Il*|S$a|2hnfq@F8w}FEIZjE4_aRN5%ScljgVC+4jtsk#CzPGJU#qYFA zm^2`vzP28D_O|unshdaSmfj4l2HlDu!;MQVjrE_jy1Z2~jGOH%4W8U3w9=y_PTtLq zxpG+HeKgfy-_KS7T8Fh^nx6RXz)D2hRNkqkZU{>suZ?k6D`T50imeA4(EEY{`imrQ zELp;HZuiA@mz$$>g93|QY`{Xhqs9d^XpMt=HH8<$_`0Jz0^}L6hg$j4MscN2aWyAg zhh~}pKu!Xq_o&K-!kR^p33h>^6mQWc5U2`?U=5wsV_QYeMnDWmjAAYb?A$6;M%k8m z5{l#svtpwKjq=#=L%ShK6-pMjvH6pLZhUK4``aOAT@-d>UhXD~fiVy?DO!KUuAhzo z4Fie3^yF5)Dvpx4FOVEbp~g}=Oyfo*K7~;8oDX$-3-K}*7hwOil^NUolomP4z_j@o zN3v}MfgyZ@96kjOUwok%w@=}s^FwzH@Rqnw$9f|1xxKCRK+v`qz^V1%J~6L1F$>2O zVKxnHU>_H5=89RD!j+(Do*sVSD8kI`N%)&r{!CWf1J!79*;`JXkEC|#)fc5slXvc` zEJ_`Zcig>dz-~wDomkMDxXe%~rntVg0mtE1gOyYddh~MXAjQDT2UCAQOncy2BIpRz z8$7!umR+f$)ONgg1lE|OZ%c5Y3BC{ZT;;+p86QTNV_R8lQhyE$M5$HC#k;OAbuspL zOsT|oVhif)vG65ux$mcTeozwc+}VFp{N>3n#23(4qPJ9nUB$n|*;ey##%#3jNjlxs zDZ(L-XvSwp!hR}jM-`c<0m!30@O>#qFWwbXXoxwy!6LdGolF5kng2#*J^+qv&ik=; zlln2UQIBlDneAkEwr82G8rf10QTSP99EYSf4)RmnrP>kTned|0g%Vt*gV|c!zaANR zIhqkK>L+A7^UQF=Lr8rcF0@J;uZ|(^2DoSwXOIOPyCEd)AqCoy({!))Pd(UGvu)Di?@NL znzNPQ`0lDZm=|%@oj!`=YEq}Ax3O7NZoU8bb(3*b5(#|;l$EMENh8HF;;uCIR@{u`pVkct6Z#B zy7Ny$^JUGnxzMbh=mx4L&@m1op^gBj(E#O3pQOc#=?IBLA$)1vSV#cawJ>{qiOgU~ z&3ouxRK+)O5xHZ8&3g8~aN%vdHCB#E=f+6}tSK?N1kQL6v6bWvpLp@bc1Lc!X+iUC z1M152@$~mn<59`x|D3%~Y0~ccl5~+wi-1jLPU+nYK zEYj2x#Eu&$p{)e@og3sBH%N*g&$&T7?Ost5Ae5hj(8+Er;!!{YL1wx^s@zz%5ad`l2+k3866z($d-u2s?J3bY zF976aH;BiVEhNaZZV*rF^$0cV2Ei^tXNk&o1EkUo;_-@e z2vP(PY06OXrGfuEVzux28?IGw)KriD)-wApH;7mA1bLz$NH0Ow0tDS+agY%(gmI0! ztC)V3mpfqMg?97L?LQ%wA3j8jdRoY3RRNnBvyAxP}m`BE?72Lg(9m!L((bP(P+cM*>U zTOUU=J0lugbv*?b?b(0{(M?6ZRaj<`7mU5)qYoZJ$ACX9CP&q6-Hc(@OxKw+Wn_d; z0d8Y@D3SRa^yT4AM*zQCrvE4VCVL8raF@(_EM_%6hR8onW@BCaocw}V$@s(rV!TxO0MN?xE*ikwc`^22(IBKJ4DIe1U_gL zwO|EAaYrfPs4k4RMfQs{#Q6dt6@>ItX9ylzA2t02mS^EzbU2U=Fkv@BAHaO+d5L*_ z@vfp|Q5U!?iH5MIIU`!W{-UgC)T#2d6THzrO<)xX99qfQc71m?u93Q@EfM8{A369E z0bT`wDuT=()Zj)vmWL&5*}7Lu6&3ELNKmqV-y zBi98QNoo~<@Gh%2-?$U+YPL=YV&{&&68TG*S;F+4t0qE)dd;#-Ux22GKTN#G6R*;7 zdOfn1L@_taxsWd?hWwb9L$nzY^W(Tk&Xg8A=Q#pj62<4P*d*3Pe$W*}COm+PE2pwF z``AAZ9V)^%zqro|7rcW8AhFsS-Uw%kQiL%7hpF+{+eK664KS--^LmDCFNO%Tr&(rw z;}ObQiJ<8M7zz!FlA_7&1bB1wS?c7^cVM+wz4qaiI2i;G#7KZoAy$7kp86f~EANvm zni1`*J)TIhNnVit3P^RHDG6Bqzat`u39{v8Zl7E}Q9gX;5S z2yU{(`&B&dk71tptdJe%H^)okvx;RIklvTef$3XRdKEwFDTbv8y6L-CU9RFC_+RWN z-C^Q4*xRHyk(ve zf)PC~k!AILm&&kE0G&4ku`+&u@m-F1;nQ>vP-%%cF%O?I!>A~srSXQb{9@h_=Wn{- zcU~q2)8BFbqgAM~CKFB;QDPOV>`#xATdlBl2R4K#Y$wFp3aVMZmi_A2a^-9jX(>KX zr8@;CfmL0`m%zF4Vpgn3vkrabizulLY7{OIuL8 z(BP5?tn^7fRase;MQa$^W6#9K`>hLz^@DoW&8_u;Sqvk#m z0nH8a=rXK`wijZOGdl@N?>;FjLFvB!h}^m#M1y@!4R+o>Bn@iDC@1o6GY%OJm;lWW z4sUW7dqB@{G$LSo=qhlq)FZt$*`KSqp7Ej*&P7FOTC({gr1B@+*LZ3eddy zPM6RAPtAnri|0{6I+dH8{EreYU5Wghxv{>`N52Z6Evqmv;u{%(^`C(_mxj;cWRwvC4MuBQxs1HM15{|tbc%2TM{mN48$rc0E`o4PNGq3e7bkB5uK7Bg; zf)SD_oHUK-zH`@R53P(h)Z(5=)4t$_+JW^QNK-~)+9CTY+|R%}+otU(pmb<6jjlaX z!Jd(wR!DtVU}*EO7)AR`_Ud)rK(*wqfhY8?;+j#`S?GSk6lGZCW@i%eaC2-^^aH%{ zte2+fKU%pR8@pKHLUnSi^IUU+1oy{2NkC<@x);s52qz>b=Dhnkv?eX^C~^{v^z7T7 zM$r1t=edXz{XnCN{zLF|1eiz(b_C3rSnXY=H=b2)8gTe*?3x2ltz2lAHUslE(|6r{ z8{pJ*&bWjeUxa`%0GZbrXysx(UH3S?02ty^3;0AdB|6Z?CyD98kQa87;5fJ4h7lt# zB4*&3KT(Vv6gYT-Tsxw@3r9#tOLEQ&VXmP6q@C6Y7#jDNfMd=^gdcnw^Afr>N!3FQ ztOVQ8>h(62#b72Jlh|D{j12K%p6ouD+=XpDYH0lb;7vdC@W=;);DPYtN!A_Cl6_Ie z^nDl#n?{#cB##I`aEoY*8^;p$E78?B)cyZ-cergegw0NRm!8_9$L)I9;nB}7Ew1qG z8?hSmve@qd9c6yKCsx^m*7x3K!-VZ~z3GK!lIwKSlV%4%P1o?4 zyG*_9#e7O1{-pk5PG#+HOjdXe!&rpV@-AOQOC({f}bjxlc z)g9f?^9bE!bRYdpNA#e2>?b1hsyIq!#}=OImVeMwb(`-FrsJzN2uOlpV%;e^FZwt0 z_MD)Dt`T9dO*Y#WzW@AV%%++rVpg*#xf4MvH zD6{e_i-t_HI*A2MZj;I1lrw+R%iYtX4K=sx4x)Wv8Wse~(9-ELMmMS#@Y)o8I0uzS z43$T6QhDU%?orW)6LU8<6&byTAN*fec`~1!B`x`Gl!j{xn@L1N1C!oq8codaxu77k zqopC5!i}*#+qup#1+#c;lwkF9dnFM&@3=ElsSoH>b%7QpM0?SPjmGM5?%OeiMFRWi zX%1mr=E1_YzIS9-6HL>>5a>5x05EMlY7I~MmZrtaGSu|A5#ZxF1^77BJg;S>7^NIk z?J|>v2J_||n4cm-8qiZDkpa*K^wi7U6QY|je|x;^)E-^}!ajg6b(~o5(|Glz#^7C> zaLtv5=(8D|w$*Jl#o3y(I9o~dS+1Z&zn{iHmU2;{`nvB!YL9{#Vnu3R>?;l3?cNlK zafd1Fj+}+vLAu*f*eUM9R_HAn;f7LG3)Mk_;V-|BRu+OFvec3I#XBja0(fWTzIV3v zB7yf<;qkc>%oBbCn~#09<8%0wu6S`8Q+4|iQM~adx;H(CCBkm9+6s+qJ0>n@M|(NX zfFuH8H~e^1NOkxV-rGpn58X7UL0NO~K51+a&bXTlv#GzYGZ+09j*^5HFEf z`2U2jxrL}OzaPPa&kC}K=Xi35XZf>e^6}(kJHsLU4C<#};Qf`Y2wRn(!6ZUS0$urj zfJQXPkWp%qE|kChG{4H{D5Lre2ix=gg$O*ad8QK~&-xi8(+C>^YY?LE!wA4;ucBM3qHd7{*khP>tT`+{oB zhrARFI;1SfM>&u?)ks-J0M86rc9PTrK|hG;A^r5q`d%bk-@cXtX%9?DVKbVO0yi5+ z03j6glXZmQ^3Fj-E^zvLnJa{X6Lnc3)cc2ly600~8!Rt``rTom{%RI#E^bG(0J20r zpiu{ufI|8ikzc|&Q(gy zqA;ltg)u{;uz?ir779+Ko>2(3aV*-zL;C3z&;3MwOcv@ng;3{nEFQ_niF(I1UVE8c z2z9=S3RF&|HWBr0f_hLFo)0CP2e4waC@9Ae<>7EF_%0|5`46tnAa|WLRzB590g%LGJC+KM4eE5e)s(PyEbm<9)#kK9sE1SgAI?HO z(}~(!H_y^s>vl4vpZ2Hk0`IT1S}9o9hHopO%ICxIepAjVng1~R0dLG#Ii z=Ketnr0sHLDAT-#vd~FEi_&&hw|eTPPS0s5mkI?Z^NXFRy@s+{qt@+0NI$(+zKP7g z8CA?*7L=BvESuPj92 z%O1%auNZMtc$gGAW-IYzQQ+w$%s?KqI&}G*BQpTrl;P_LT1$k2Lp&|@3Mzs}PVC0T zj8W+!{q#!c8%VZBWMSW|az*gSi9Mf}@yP!PWVgP38KvXo{c(jgf=5p5Lv%FXLU!wF z!TymQ&B=-dBWyw0KMM>W4o5RF2lB@p$el82P_Pj^a?0c(ZI8OA71Gb(1O;yj(1M_K zA!(pvG|OZ0ElmnIf`<^%&yVD8Ub@t)RyK%*4E`Is2xST`q@P}s#OH=St46T52WESV zK!4;Uf*`|o5r*S*!dXRNL*vBm^*c}NBIvGvNI!#DBQ;rWSB&L!6U(me@B5_Cc#| zK9o}wD@Nvm@?xUYRo5w$ErYPVLyLT@f(z+qaH^ZelL%U`T%z=PjaRSaz$qI98MaN+ z_o91zt9?-3B?Y;C{TYc*YiU>~Bx|1Por zi(ntrYVx5xOR-|CMo^9*%ERIC&&z@QJ2NxLo%-B9h)l+5ed^EcLi*`7$$zIzE+-8* z{A;}?xx+&QL6=EJhG8_X&+w`>ISBS^hJihng?;xR*uOUn>=U!FcY3gU4Su`EUasIm z`Wd`Ph5huCaFgH0!|FgJ#eYM}J;T|uM*&ChpxCpzfIB@!C{l323)RyY>30ycK9`Tk zJ_Q`XBPWr34&OuM8DzKqiB`bfSKF_!M)1gqeUC1J9(RZI(<`U%A-na2U~do1_sXeT zA&=l8MD)}4oaMh9y63zos|c3D8qruQwqUg2^vf4%?E0(KkbZjo@(+;T+CR+}Q1g85 zDW1gG>pLB5H#pFqw?KdVM)Dq_{-O{Z)ZOK4Bm=+!R*WSH%JD?$ZX|{0g456W8UPQ0 z8uI)+Ov|<+LG79}_g1xht{SMEysskan+5ft;>d?mS1= zA^o&J-Ip@@EAJ%FPhUWBv9We<4E-+`3c7U>)ULG^ufR=5ob?MV zg!D5wLWPZV?n2N?e?l?;w3m6;5{s8YwWq=w$L67MHz~x0f|L1zs}%X%*+|Vi9(2sL zM158kYS#*4K1Xn@LKV_auOnDZ)Gwpwqiwu-J~ximGj{H7hau>5DHX>d$2e#(2Ms)Y2tl2L4A(1s(P(GpYs)- zGtT!WqJB(J=asdVW!|-YP1;mZK{3k?llwgdc1?8*fWF%eC zs*M`+A@}$}LB7F(+-cPXU3vIds%NA12MMhgcJKJk0u7+P{Wpg9$Z_Y4KFUmsg>aKWE4`&)En1#Av19ZFQ`UF*q zkbVY_P+?;**CS{>gW)DczRWA~NTCXJk4G-1_4H7ekgP02|5V|l?Nb0ELZ zf!t};(+Ua1c)=4D!jOIjJ+fXvfgDEysFHVjtK>{41wc}iwyUc5R7stl(+h4t-D@aS zg-{R2RV~OuJ==-e+gut~b&@JgNI!#~{^dd>Tg8I9J#dd#E^`V|X!Xd&xT>QSMN>m> zBZbYFz^3H0C|p;FLOze>p|F?~E)fb&vzcEA^%l*1L@^uEPp^2E5cM0A6!WXS;3ZfpDg?gSt%q8^b`^sG0i;T$O6jbzN*X@Rb8qF3PgOdR-~JflzUv%X3KgS(M@C_RHgL3s&L zYB%z+s-$OtCCFb#Lu!ya1#(6qAJwhRgw{(l(NBAxT$>5{C%83?1Yjo1y=GEy@~z)v zyv!FIf99*8o?#cd=Ggx& z6r9W#921TDwdxbQ24B;FiYb0 ziHkpqiNS!9mzuN8hCn94`*Ed3#=x%&AZ^h^Ipw0>orBLpFy+O zAy^yG% z!Mvgib<0)-6~TkhSz988*b%=9*{y2@`$ul|%`AwPwxAq<(VFV%G{TkOH80P`5z?1Z zo%$I(MTL#4olc$~BLQc>vt^@#ir|q`BKcY&5B4f#w=T}Y-lVWb@W_chpL@~phWAe* zY`un6?vLRP^+dS~VYobGVBP;fHunyB!i9*)mC(u=yKUNIWcShMP;aa+2khx9Y3 z?cK=!V&u1eI8KSC(Ic9chCzt@z#|>wx%2?T5V?dzK9!Hira_40^I;w$my$@ToF#Fn zpyiQ4u|DjbgA_cO+?3s^fRYguN5NBB0Q_GMRcyL z8f@AUtOSc?>Ze@<$>*=U5>M+d80NU`{wb9!B2YQn?tG&e-MukNxSZG@&cgomAlS`} zgBEv4KW*OG@xVOE6~z7t!QLL&=oSC&L5K{o`|&9f=_(tN-RDE8y@HX7psXWGZTC*S zZXbm0t2|a?oTk>Vp>Z|YK33RvV&5?c_RnhU=P9_5eg-|*uOasT!d!~mYLbIsze{6h zZVg}qbdir~TAc{g`XRp}x9^wy_qk!&3rBMLo%Cv$+}TE^Y? zEqmggv-SliJMw87c*vX4!YJZ>SkXF62XY9?Dx!264;dcPlsyNJ6uo|WcaM;N>;Fbm zIPHN`dd!qP(HESr-{`SQ;sF`2>;-*H(2G@Ot&Zq?b_Z%W>i|>Scni+N=4(VWeWO3} zZ@mo9{4p9maaI|V5R~;qc{m!q5n#|^Z-RV+1Gz2bg0tycwDvAg*h2bge;}&;E$7*+ zUmT%~W1`DATr=tbBU82#O|{qYU@yOMEEV)N+Xd&m-}4xqafN2|A$0te0X(fSZoCCo zh)mO|`3xDnXoE%A8t+Kr-G=(8ogj_5;6!@9Mw41|D6y1yZ*k*|AU%S3!euq}rn%%e z9O)tbv@eC!>Z7e#rGmFTaJox<1!s+h=OYx~f9* z7-Ho{1B3ma5dIJt&WDn=3|5T45R`31c{nOJoO~AY%N@w=T2gS<+|0{QQ`kcKX>VfF z)`9xrvv@BLJ^z_5>nJ#{oo`Z}_$V1X*rroZR$S2AY!{qzHkFW5DKu*R^zPW8#aQRM z@fMsc&sPblI)^6Fmf-t8R7FSSF1Q|KCgC|-Kz{Yp=2wfEI<+M_R}!sL1pP;zEW?;73*~>qi5i=>_2-%i_6{q}$asdr7Sd1ei3#+n)?LI7vzzLY zM>WJ4K{A=C&`-Nf8P1q^tf05qF1Q?#ucB-ErlOM%>nG6Z$M7AP(QwLHP=1~$4~Or- zd{`FpQ4Zv`G+YzoUL~4w@Jxj*q@Ui70p=Wh))sURsKg6gN_0(*1B^`BN*vAzc&?zg z*)BM5ZF~o(r&t&D)5|vIlzrCUP-e0{!^L*N8TWiHgyjM`VUBXJE zh(qH2>duD;+<0A+r}?&GaYCBn&`(|~s;-V0QG0mU~zUcp>S6xoBKF+_O>Q964$WO%Sa-4J;W zlK>ku&2wz`RCQV&xP^a9n96c}84yaUwd&yyG$yAgYMZ8ZR%ne<30-@%*DMfppL}rs!JvH zx;ePX!^Cd8u6QhBo31MwEBA}l4FuNxid5A7Y=14r9Zxv$6Gu2NCpRb^NRKA~e{mq= zcyptX1yG5P2n>D!Qz`HG#XE|Ky!Ju1;b&;7YGR%&Ta@B!*^~z6mieq01vNNb#kwM9gmVlX=I&08)JE3lXy&eK3jP zh$1}^F|1+|!?8>HDE7->_SS7EDl)RpWYiLj)rCf`#woucImUb@0C|)=uD#$zX6eiD zdM0^i-~tB7HUl_VJ9s8JW}t$l1(XmwmBjjRu{a_@%Rvmc(e*OMef{Oz0s~c6mGXwU z(|{Q7LB6A)Jt8n1U~6uz!2Nb|!MVA&;4xjGg^f~NxxN_$~925>S!U@%uxg`@9vn-aYsd2Yp_`yac16*aY2Ckk5 z+(K)MDah463UWVf3HKYSONw?$OM~;Qaf5wyKNQDTC}Iz_!b=KqWbPh3f=DGUWTRC6 zijfu)+)vIb3Gstu$Ep({tN*BrsqbE|M4 z;SQcRyn~q&(H%T4nFk>6N#7#0E1=e^bKwJD6{aZK3=qV@>vFEHDytI)q;QxrwBjt# z<1CiCl1Nca{a)CRyPfi)k`tEqDTJ3&bP(1RJg*+g!~w)-n1bykF}f&96*8uxZ~Qdu zSKx6dbmLhJ)VzaBPy37W7}**c+1L+1JX}WhAcj~j7ClC`3+_rAS!&l{rp1G;|8+1R z(ObCTt|7pQF=pFBm&^3R4X5To<%FYVC-CM&m_(jh$=e0?$ob#EUlJXU3-@4@c??L5 z?z@<`AqdTtWw|AX3+_s@{X%AimukqM{w3NnTfG!w?aR4z=R_x>ZdidH z0WwmNKcph{ofA#>+6Y;wQxWQjcEf4}IJzellh-}y*tNvErQlZxjI_e(8*$|aq?c(n zXX0u@+@}z$>nU9~3cn-6jmHRu-o!kD%_?T2e4@#A9s6fpayupNoP*ErM!ms>WN7&6 zdW+Vzx-=7R#BIulVs+hc&*w`0Vxy3%z^m>Rr2a{6JuH1&PTVI;Md5~hZUAYxd)UD7 zCXh3Q`EIoHfbyj$CFWVe-Rx?%-`%yiSVSVW%`R4Lcu&o!7%oi14Gw{IFUjwHiMaY|2O_#zp}G=taUGeo|M~Ln zPDFPzFMd>BMD*yqyH#HScbsUkg&+Jo>XAoue?Sy2A}C#VIS4N8s6tl{HcOnmXSanS zK!0H~Yu6S1A0qcb9krcNQxS#am-zlP-qX>+tS)_wh)!Eg4H{YPlf-D>;BU>WL6ID% zkZ`E+KKW)x--)MtFbvB0S1N1K{ljqMLOYDk9&f%TPTKz!Cc(D$Pap<&rc0-pH_mt^ z)=iO&!}Sjk&%1mdsoqPv@Lq@a)G^X=6H|Q^W@SwE=d?uJE|RGh;fDWYoWp!);BJ$K zuL)po!jHfA;UU8v`lp@8fGWFAohRVMfr)m$pc5C*pvysXmo5i5oDL0$tb5z~Y6|CtM@cjmsc*snjqL6h^K|lb6E1oty+y)PxM8apOF`-GNvWobJ>ePA z{k38 zT{o72LGvKxJwZxTiK`FSja08P@!>4xfecS;zpw8>M>7G*yi|vaMK*Ki0=NeCG(}NZ zz7a(P`FFK4Cp)0~dEco^uzzrn+#;g`H0oz@DhIP!Lon>CVc4OS~N8JJ*x zrJ}h4K^U$toz*uJxS9dEBh8wmiSZDKY!~|ckpT6MiKcnq? zP{DaomE*pl9Cgd3go}*Ka#WLS(fvM4bV;hsU4-sGHx*|Dngg%Wv_~uV0kxi4OQVN{ z87Psp?fW3 z*IpV3fJPjhi3x;x^-l)I&rtzY19-pbjGjlBp8y6p7eMURt38AdWpsquB4#n2O!R>E zU4TsN0qvWH7pTN`Bf7$>%kuVLq`~&@N29L5T=iOkbpgs_z4C72v3A7XYslME!pt{UO>l>f4oyd*;6<+^b2| z+d=XclAPoqIg2Je4<(#EOJ-irk~wu;RVX8*P94IeYH5pHf~`2ejc8uiRB?@LVBL13 z;(xp?>c&)o&-ydoTQ~nnweqt7t__i`e_1!SapD=;te!H_$S%xD$O&YT9*~%MAM6~k z5d({Z8W6UZYGhlXzj7gxtuh0vU_!~1f`zrqB2q-*U5I4s;FlEMdIb}@S;L}L6IgN& z9-cz9wOzw@TZ-R>>KWt&J^7X8ZtzRkjeyl6&z_bE741ECf@wVQ+_WCAVNG#WN zqhnLDt_Pc08KFBBgz0auZ&on<7?t)H5#}KUBNORz>u-DgCIvG9m;r(L8Y9{R5A&h! zSC=t-`6^guPdOOCu%Yb{v^K`sXufb|8gICU&qcRnLtX!e0L6`f{>s~_;`8o-ocxvd z^8Hl2%jL@IQsWBT)TZuQ#?Y>0JEbwHt7!u-=T483a`4rsuMkJ86!O(zm8P!<_Qs3h z%r)K!r^l)LbF1MSX!-2muYfhr8<5=7cddTSnWal&0Vh{#^6GkBAk37i zE4%eA+`K4N;3f0YwlAa5txb@Jx~4lm&yr!JH9gw1suZ&X@p(Oz7$GFb#fM-U_fRmK zD2!uk(Jaozf`eR^O}dT?xV^W52Q7NNoRI8kG|fWA?FYkJHCT=b`f5pPD@nE2aNHmC ztr>}B9d?Y#xkXe0V^jMDlMN*e z2mz+=3O6K?hQhte68zg+5Y4<`>}`mEqawM)Ju_l0dkHZ262?Vw-De%)7TnH`oGc_t zgb}_?wWXOBl?i459qrh8ByqHm2%)JFS;?ifW-xRG0se+1A@Dq(@1MXVmfTV35l0f$ zJzE@%b&7-GT;f$JWD+w2h9xvT-90m%^mKQ6$)e~BvMP(Hd{5*dA`ca1Q}8JwK2`-3eTXQ& zCn73JSVcwQ3Cj2TSJmylGYQf6KEFFTx%Xdn>eP1X)N*fCd)qf6q3gtX%9}>Vz#8M^ zlB)^aiLakM{HogR11V(HK*Osvz1@~wuuOunu0SuIcPO+S;c!O+mh!3R=GoNkrFG-6m)lAhs}aa^Z>2Q8 zrKG-6)DZP41$k~?4G|_>lCjGKHZhEaY(CC)hB`yq?_-3)SVzk_>V|ea@f1TP*-wie28CsY+v^hWIRp?;ov(U6C%W}f zeD=a8?6N6he&^Ko$BqlbspSTZ-2yTH{FfSc@jKgErFaB^>Zuz7=ZWVV@Pz$40@d@W z^R5eg)eGzs^CecG@A)NA-Fib{RXiKu!ACuP!{=i8tg%tKVFFR1t#-Uok4iH~rTt&U ze3*^O4j{&S;E}L2>84{7&eyV4_%*=fAN#KXeBe73_&2|(+o1VvBl?a@X#dBY9b+ii(*NGqc_4<1+t{!eKzT*hlYw&wc>fN!L$FuHT!2IUy=l9yN=y5FZH}qcM z;B;r?UU=|i zqC`GlzQjIr&TsTl!W-57X8iPxhc7&PyWn#%Txu_!eP4{FHfQy;unv$ZDEZ2D^h1KDzCrIag}gfW#ZxoUbSTQ=2lD$T8&O=Y;H^Vw8^``lb1 zSDkC-7D~yvV#(!AwO9;>Q-y6osa#BFE0t`;^rtcw1&JV)$;jQ9QmQaF$d=2+^4wtO zAVDG#q-*7JwooNq$lDs^DnXkQQwiD=i+h$XSh2RdEz>d1w3f5!;&3UK&jzG+C}?;x z^=!m5H8^R>qQ2E@drz?uR)$mg{M4Wk7S7JJ2}Ojw-965wXI@)ooJsW;%hgMESa4vmpu(&&utW>k5V}q65`C>YiKQ>s_J(w@{r}Cz^SSzQqiQa0enhjQ_`m^~8 zflJ+#<6xNrJ~qg9XA7BQgH(4aoz9l3nnatPVwE^53N%b92E*C%APEn)q$)wJlFf7m zs|)#UL3Jn_4CKlc6|)KKRjCfcpWT{G*Q(h}kShe)RC>q?$Oe_{rdqa;&Z;^pL&Yun z0MmzSM{FRy2@OhA{ZO(vU=j&( z6ch)7Vy#-LRTByGzH~BO%w$b#t2s@PDk3yTDi^?82~q>qY&mGlXNW9Ys*E#jGxM3b ztpF7T!MOj>Q6bo6e$G*61+%~Yn+6a%+)!VmVZC|i@X|U+zMJt!g)8(WtQ9GOJ+92_UnJtlF zr90G1X?W{e8q;PHnF&%=R}>`Gr*4#-DtfGZ_>v^=Bc%nZ+ks-O5Qfj^Dr9FMC>1M} zob;j*c}0p=9YU>qvClQF)g%c-zKlT%#QE(wc^Iq=&|lR%N9(x(un=RJ?AhQgZox zb}*F>D!EKHk;O`;t2WW;WOi$*91UYN&zE-BPO29i+EzI4ytp@kJ);^=_lz3aE9Vc}+RCrPzqS z)rUqRDqOE`uWxCrKDI~NZcEG+{+2Q(#yXC3m61=CFf2heH;i-V%t4Grx=7Phb$RW! zVvgyYgP$x@Wtw9N?R0AMV6+}HS*i_Dvj=6e(&KDLGEgjUNtH9fFj}fIY;WIE&Q-Hm zje&%ECp~n`>z>|m_~E&Qa`jm%6CG z%^8tADqTKor8Zm_*GP24Ga`Ys&6+Z!W8SQeGtX=%LFi&KkLq@lvkv9kb<{};=G6A~ zFym8l9c{BZ){AK;o>DoxS%ou_XZ}}W@s-et(EFh;L#KQ-#zIdl-UAKZ7K?uqdI9SF zdMti3bm;A|_+!uk--yM_(66DTcOc`NvH0ijjKv?gD;EFg-Ld$C&|&w);-^FZ3|(_? zEdFEY6W@x(UxjAhAB!LIU@U&acVhA9pu@f!i~l>c;-Of42znSA_+BjjS*Z3OvG~uS zw>%t+um3?T9{iB>J{pU6{3sUhhE9VngC2rnKPFAkn4geV=)=%e(34R2f5qbO_-QPD z26R32GidDN$VYVI=XW@{ePddJfA~(WYC=V zaIQd?S+RCIo5^DJ7OO*37`mlitMPz2R#acz?pEqhZyO{iqrI%gr@LYq?K+&&FdL0=%+Y?ay*rdO z#d9HZ*L*Je2%D4UMwukejf(~Y84?C`l}c(bi+LVORfYmg^*}yHpGN0k^Mp~U6!V*H z7L4iD!0x1MxuRm3-8rN4D0R!n1gj{EuIba~m~k3mjWh2_l?!yGbAw)|u^Iwk;Y#@| zg<)E!1Zz?hE#2tqG82hlZ8lR&tEkPmr8R~;u3IQE*9cV}d#_EQt+q1^()m6P%$1 zW1RkN)vO-?GhVSRS%Xfm%K=s(H;(r~@+4*)`DCM(Hu$tuWS06@nQX)lW6*(^h|2D$G=Td%_}iP9Lyk zWP&MnkguH9)92a)>8mGN8MI4QdFPl6HqY)nb+6+eImk3pwhkvemju+3dh` zMFGQHu9eh?{8%bm$-P&DR^`!Ukyw?<&Q2ye8O<7e2a?E#6S0g*tO}HY#4;vK8p5JV z41^Pl7p~}I`p~yzoLQD-W^aui?L=d~N@`0`ELnS)Xk!#+7=O7op6Cm5g9U5ywhU#N z_~kTEPOQ-EP#tQNw`ND!N?$<5s!v08H3zUmQd=(#xuKjb#qvg5k(JaywrbZDN;1uK zvP$>3Fo$95OO*#Ldtz;vBp+yZd z;mp(i2@~c&C9R02(-!86ppYd@V)5D~3l=Tc#MdSq$u*Uv5;~MCRGF`8g5&#go@kNT zfT=_-ol_H)ZswRBX(2*IsMf;-Pl9_FEM3xfGI0;bTjJTh_|VDUANTjCTb=s{xL@m^ z#TUBkdH%ST_@|(sL09bA68{1u_hkPJG*-%b>47--dQTuRvpo_oI=x zzr^#t#5Ds7<$a&$zj%C`kM}_0I|4e*$9pw*Dc(tTO1|2v9uxd>mRWKub;ybZDjYG} zcAVqp8Le1$uaxMS`tkM--;JvyuzJ>-=*Q55n8`7(tI{Hzl~v7Y(oK0)J|*Fhgj{(GE^v~$gj#qDO0>F0y~AK!A}kP zYZPD!)3`Oq_=Lp`aygJq$45zENz_@s8VOpOrMH53u*=R2O5X8VyIl* z(y1qqXxF#GE;%tTP>*c8V6EHvHf{Tu9HTUy$6;3uD2eEDlZ~J?Q5HX|r7Aguq!?=}_EB0DDjZ@7x1}f2m7_^rr}r=))pA5- zw3YEAnbySCfR5fSvuUVi*A%QV+v+vhh$zQn(L5vBOwL_8(6(=GuS0j$HpHowBv4K1!8q zDw~sP=9ID@Lyg9zQU04k?3WYWYJV_TPW310BUw|7yab?))IDk}>@u;FMPfXaVZ56) zM^0&p|M|$4_;;WypbgMmXdLuk9WC)&@V^4O6gm$&6DmVP(CN^EzSXN%EHb&En_qie zyqYz@+;J=hsuyW21m@OT?@^0^-c>={bF9rN?7VITb~V(0lg|`LH&G zynKkGO?$cKtWvhzj=P2a?V4~oJ7Cu)6=(QtqgF7hcQ%+8H^)XjBa{=qyt9IpR{3~V z9Sr5iNB<8?s2yg5Eh%4mEO1)b-oC*WDshbP371>pn=+!nH>}q@u#uiop8ud_S(n=O z4X*AsjHtUA)1&e4a&>m+Mde23IvPv29g%#z`4Vo2QIkzjVPUnpm0e#wI%pCqLFE*E@8~bBo=72WKOdS{)xz%8f;2R*=2qoz}y5$<)!^?NTPaqd9rdD9=bc zXb6ZbL#yt0$AeDIkmPw`JfRZv$@1R_H$7yXMI6;(nI^Zu?;6yI#r{UxA|)`z<%Wj% zw|S8nje;=lb%cw{J%{odkttV+$O^ySOn5EmGU1{S z)Emzec_lK-z7g5Uy`d65S}kB0UNUD*yR~s)6qCB^DF{=T9xiQ74-N8SqF6F@U()4c zvFcz`rYf$tixG7eir<|+jN%~zuMb|fFD{z!NPXBjTwNb#z^lq~Z9qjisx^dRqq^V< zIkai+rBQpm4kDb$YY106ZlE@&P_DJJzK~BTSJ1GFKm}Crga&IUGZ=fVP(#&mIS=vo%-Ge2mc0K^14;|5wSC|0v z(msz>-^r&|;1dvY#sw{LQ5!TJ>V{5$-UEexdhYF8vL=`@awucnx_031VfNjh%nJ<{uBibrQ1jjL})dOR$aG=J@Q;r7cK8>ln zT5eNMe>n7;tMMvhCKsV3Gs7m@frM?7yOd(X8e0sx0_&PNlFlG9I6{s72u6l{|535} zWEU?OEQWb!O)AC9gJQ{waPtA5l9{YhwO3ino|)+&PYu_=oT|6@_*YBz%M0Fco0Vpn zDVeNEnZ;&-(fjW3Z+$(oZsz-~ryA;n5WIv7zboPc6kcK5w_5g*X(wwS_K`$~-|cAq zOhNo-K3OWuF03()Fk4S8SJwMi2~r&H zvC~^3-p1QkXzStKorm^fWZj9uIvm6Fkpqy!VA% zR@hkJTc%(WnwkixXj(6_7KQ7tDPF&%(|pt<6`}?6e6orYc@4AYN-FJB*8jB<|_s`J`aRBoCS zjY_@QNKs*LKho9ri6b2wUAc2NW>=Ahb1y~v&g)y^uYQ3~zprbF|C;BS+%baodf)yx zE&IiL&pG~zPwM*m@y@kpzPnFfp!@c7I_=$qmvBK-PRb6AC z{L?LQ?EsvPzqY~YplKbex$^v2T+g$(@5lW>NXOyEAvV_*Up_AuCuv2c=_T%0fqDEN zUzhVyYZ&Mr^7IJwOX&Ad^M{BVIuz=H7D8*Gey9w65c(K&4Ri~15A+E1OX&Ad^M?r! z9SU_p3!$}8KU9W32z?B?2D$~h2YLkhCG>l!`9i`&VfsejFO8%<>h~~p62&_||HAyr zJY{}ueq)~I@0aEoOV63-%?sv5{+=~2S^Ay%y?NRE(frB0VqWF%59ZI7UN?U+e>Esb zlWBU*G(%6Cu}yn4#hb=8?b$S;X`iNj`D<-Dz|uiYu_m1%6kghw8$K(o^3wZdxgX2@ zxX|;>?oA58fBF|bIQ6VMM!f61PTV8rhvrf9Bl83E81%6D$xgBCDt)bR$z8fEJ+=`m zl3iY3FxQ(K%}wTJ^Ck0T{%$b0LSHoBFyA!)ZtgU9@pp&0$I^Y~Tjq9iKY!Pn2QBSV zWW;e-={p2}xd+@QMR<4l*kse~%PLZWzR-3VW`twfWK6#qGC8w>zd@5X1E$DdiN6A0 zwU$lQ)XZkH#cbuTV%`f4n}0HAnGc$?%{lySH|JS8-+YL_5A%0{xyXFLTw*RYA2S!5 z%SOaE66`AfU9iYqJB~Fk-|c0y?9|5>0_-~#hf^+V^+rpZV~#;%yUjdvyqVA6v1Xw; z+AQI3DSwO2a>X?P*tcG!AX+`Z=@%`YrS)NXPNC+(;k8wWqyfzuAEx zYFrO5Xgs^8-(GUT1$$5`Uwg;hv2@S)ea@eD&xAMbed+keR_>Vd%m{vmOtGd#JU9It|D6LZrY9EhNRJoatXuOQ7RB~BN+`C6R)CtD z#_A)!=H?cqaZId5?<1PyEqBNPj&grIUyGxAD35hk`$o~QKcL?1nF@=9bVi;bu?fsTL z$L#&~z4vX}uW28~n$45Vo_o&2iBk8ER2HYD$dxjlWyb71ch6(@T=ACU_iCmeAA7i2 zp(<+H*X%R)#Ia-IZ;!Xd-=e|m&Mt@H+H7nsHNCd?c$r<)O_rm{uC1`kN7o0TW^6vr zquKtaCB z3iGK@(;Cy-G-=YLX4~(yG^>$~*}v|>2A*=2seOfyxLEm+?mH(vjcRWBBCjd!edKMz|iHm6r0~qm&~xU28SeU?V+BY-8@DqQ44KN#6;nLUgH5(Ordd1EivOAmVR2 zE8B+oPKSH7?CwM16ES4VCDX}*XSQ>}!WD^XYS45J7HXY(S!_Bp+X@7B_iEYs`0oNn zfFyo&PU3eDrF_+N+U35^DtlN=Cm%ND@G53f)s*SX4kh`Da5!r^^_6Ia2;6N$8bJu* z{d$@RiUj1pPAkoY>}SojQ?p~<&cmARuMH+sd~nX^z9B5t`t5fKAfd?29X{!%O!ofFLH7ql`v$AG_^AQQSc|V6zIHqUp2I8bCuZXy z6Cgg#X_v#d7?PVV@rh*VIrg+DKFxVA;z6c;G@s@(nlFe?bK%=~xEj*j7_nBC=EUl1 z#z5lJ+<6^>G-nR4@KJpMYG>osocAgO_2CxAtMFC^cg>Uathw^b@XhBr8ZVHsJKtYG z;?rDv7KNm_b|_DImBN>xkWX{-mGEiKEuPM$hi?dwbL7>HkpIv;jb{>3&9GlsMJ;; zfbX^r&%`Zk+#lyTl z@LdMqWp5Jim*7*`DPFB%Tn^vE-i=$mKEBSg@*%z<)>?+%vvWR_Mjd+>@@Y*b51-N; zUg8nm4~2XIbBthJlj#eU1-}5&^*u=Cpm?`){zG+rlX>U_fWHENe}uc_g_rm~5^)G0 ze+onREZ%ss$*c(j3H#?~xkvfd!Pgey3;q5)itqjKeLnPz_>ILa;%p|TnwaM{uFy|* zCw!Lg$KmUUIE0UZ=L_4!9sNz_I}LGGhIprVzR>G}bdznrArAAaH8PcPcs&5$F=1pl zhL5^OnwPnD1M*mCI}G==km`0HNNqeS@2Rtz%zvwa`zw?e;^}S^l!}4mP zM_-2jnsD}I#v4sTuEnlMADig0^4!~f`82VDTmf&7@Q;pP{mKQA_%8y7>#2(WlM3(a zw~6}wJUE)3TjlS^dd;L~bbcSiKfILR{{URcVP(>ErT0Vl z-}B%bBlu6?n<5w?=H>_<2mVq79{~Px1P9<-BKQdKtr4uBak>jE)mHlE2>-Q_{vPms z5qvUu#~Tg*)4;DrFy_^~9Ko19&Jb$wXTi@$@DTW=2;K;eb6jp%e)=VeSOmWxOpjRi z|1kKeNO<)rPe$-%!lYm2ru=<|`(A|SX7Tkrs2`Nnrsf08-QZAPP4m9ykx}^9;IKV6 zHScd;1c&W4Kp+1beB{)Y_@T(#4}Ez9{NF!gkEq9b33B0IWAX2jLHSPr-~I&qU1^HK zZv#JxzAOLxlHMc0Z@sQ1{s^X2{?oy_W+>z;S*VPDGYCh%0`$+9UuUlV^s{vF_bXn&#nhrl|8al8Su~NS?QSs{$?b9M}l=2VVJ*Z;4`mki9cn- zk2iC``H24_@DT^L#P9Xxs{@;VdPGZnwN3AM(+9pflD^Zxy8aVVdJ1427a7L4S^TW+ z4&kTr`vCau=+_gLf4sQ>d~HPDh2ZcCc(`H|z6q?OI49vJd0zwn;a28N?TUZAxd*KN z(8WK&JP3X?qMzRfUrBvB|B2=?@Yb;{aoKT&{{{HuYx&OB6MKA%--fO@E!Pv`jr6d z`ZlEUo$qmzkFVF`diw$EWMer?{w5xlNAOn9zs}41u*bJ}d7lSA`?i+&lh%K{xdB}I z3;Usce!d1i`}J7-O7H*gKK$2x_#c2T_*_f;c<=u>_(}4kL7vj{BzS8iJGmE|in zl~Z|d!BA2DDewvZ+7h4O%X1@m-6z@8@55KY51|ialkgMF+2HRS)DmCg`7Z>Y7D@l5 zV4Yta>dO`2?Qd<=-!CqjTH+gh{C9%&j%KU(zaJd-7yFQ( zN5Kap&!z7`^Pl4XbW8lxKKxVSkN7_eemiFl7@z*%gXbgPg`a3%2j5lC52>V_=2QOD zef)Y^ud_AjRBioF0PFe#r1mgL{(FqI@06q;M}mJ6kv9W;5Bk!!hb#YMz~3al>X%d> z3&3Yk9_pV|UnhX)NAzWl{E@GAEBPmb*VN@tG^c}g9S12rTfjPuG)(UYgd_4U03Sko zdbi~tZ$1w0i^#iD{2b92#&vuUyk?<41x|Tw=e!xB0 z*CQ<+Z;k|CM*X_*6HS-rzuEII245R#->bm45q}upI?vzb`E%eG4r_^j&+AtKtn-tB zw!Sul&xoY&z2Jp2TjDpZb@@9Ry#9Q!Pv6Dht0U?A1bDI^zwg^T(Oe7GDX3w2-U!w; z8B%`l1V4R!OI$Mr;Kf|r4-V8k(H z`rRA7U|lsIe-=Fd%2>U8H-TUN9OEnNKi<3#Tq1oEp!}Q zamG(W-v27_H-eVF7K3$t(fZR?!LL!iP9Irs0C#?p_s%~20C=VU`AyaLM(}MBd!l`&S4Z-D9(Yb9 z{TG3CXlfga-h;ir(xd!$g72q2B)q(1!DnU*i@562@XgTF<7 zNv_Rb3cMA2cC%0a5I7SFUjQGB{c+=m@umjWH!%xs_=)EI;O+2l_wvpKn@IUw49?f< zbE5gU{Euw3ug`$>a|Ci$`~4yhOFqZhQxur;dkgsTNO|fPfgi8SJJ8$*j@pm!f^~)S z`NxI38twHr;OF;m*oPP7&$lh%c;-*wUtn)EZ&UnD7~=hpZj|Q)unwU&UOy%Zqt9Xc zItZL+e((<8zS_Wdp>GcmjpR)Q>*|A4fAhflHKB0)vK)Np*p~Pv>p$MC^ZbAI{6pa5 zBJmZ$=Y5D@aA2ub^0$EJNBp;eUybPZcJO=YpAl#FYaVYt0lpOb>C!*Z=*L-aZ)=IW z^o=*ygPY;U%vkwf1>Xh#MPSv}-QaQYmiWW;`-=bD;BdWoKi=Ry1kOb2??>QkSP!}1 z%X<<$6!Cu+yf~8nKZ5nkuwnUzUk&I@t=`b``kD9roR&2(z+*D0Q$>?2SM>HJlc2>T z&~mYCd-+MLqXr1G|;-J4(vMYjW@!V}-)vm-+%JtBhd%sXezo<5TuVW|>3e3R^U zuqQcm&N^!5OjFU(G@VD!JZiexFvDz^X*P734YSO>edB|sHn98;a`y5835(#YSizchGSs64whnshiF$yP4%5*ctxjqKX z%_w1aGUk#?GqZ5wws)1`FSlA;Qe1Eu897F_s}fh0PO z=OmA$%BVttvyH`|+d8!Yq+Fm}>7jBoVQhS_NcGl~_z1#R%`l>=g+}ctTp?ZB77fS= zw))m3>ST8`L>-XFA(rl-7_*48;3##fgEU6Dd~LeOhf}!`DpXDq#LtN87fO3>(> zREyg8sI!I4Kw;Q~C&!>zB`iad(+^F7uRbUluVgbD8JuM*N&DH$(jmjaUNp)ACq{5M zF8kN?L5b9uQ(~g2&bRHqVt96ScLEt0h*&#q*>@rq-pCUCfRjokFjC4wfOTNO`jrLs`BYg zF0cZK$CQ#bg98KD#i3{hy~@pYyY?t~f66r*oK!5KO3pBA)~;T-#5RH?8;%U;c@;^P zJ)j}kFZ0omI+Ied(e;#*HaQiuPzKhOla4U4q9tY^&7R$CBj^m%SE;UsgId&P-n!|S zj!f;H!klbM_WB}Ub7G%Chcm8#*)tXvWfi^=_2`aaky?&c@Khlw181u2qZ!EA#zTv0 zq=;>|9A@pTsVu8&&jTZk;0!}~ZPI_*6KgmJh7FWe+a#z0Z6*bpV!i!RpOqr2Rmf0J zvYBZGQ@b72{A7*Qkw{yuDmt0AB;CC|88S;#b%md4IEpbBEf#uYjt|B{70NPdGTZgqnr%*WJuTS|Hy_qL zXP8vdr`_rIOdU5(SF4`KEXeUyzj}$`;$R^+fHBoMZ36=w+&)56rkjDCEm8eE53km< z%)rihrkME`&5GxqZs@Mq#5|BOoKZn<#D7$Yz9>xcS(@)jT)T}1r_CgllPcfArTs98 zjl-PMqwVDz>3405_RU-t+V2!>G<18!5?al6J`GBeW$YmezcE*$2DIgvTC{39L@#GJ zpwkKS31=jgrN?w*iCkCkfgh`rZ3cW+A4CZ4vRb~id57^^y7hAG5&MCBwPipN0D!0*??a7m7 zpu(>25rYVwo5KOhiZi0jT`GaXsL{pp1-;9YJ!?(P>G@{covd*x?6jI-xnZ`t>U?!- zu+nAvR;^yV1cSwC+?lYheT~gDgPhW!;fCwr({9*jd;MhAei^B;)QIx4MPpTDmFr5> zF(!xUWo%FC#M%EfeUX5LUTws04% k?&<9#nf#iAEesk|9_eX1VeFJ2T2g%8`uh@7n^lYbzq*-V`~Uy| diff --git a/trunk/verif/examples/pan.b b/trunk/verif/examples/pan.b index 8816afb3..1ae73245 100644 --- a/trunk/verif/examples/pan.b +++ b/trunk/verif/examples/pan.b @@ -10,16 +10,15 @@ ; goto R999; - case 4: /* STATE 5 */ + case 4: /* STATE 4 */ ; - ((P4 *)this)->i = trpt->bup.ovals[2]; - now.retrieve_count[ Index(((P4 *)this)->i, 2) ] = trpt->bup.ovals[1]; + ((P4 *)this)->i = trpt->bup.ovals[1]; now.commit_count[ Index(((P4 *)this)->i, 2) ] = trpt->bup.ovals[0]; ; - ungrab_ints(trpt->bup.ovals, 3); + ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 5: /* STATE 11 */ + case 5: /* STATE 10 */ ; ((P4 *)this)->i = trpt->bup.ovals[1]; /* 0 */ ((P4 *)this)->i = trpt->bup.ovals[0]; @@ -28,13 +27,13 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 6: /* STATE 11 */ + case 6: /* STATE 10 */ ; ((P4 *)this)->i = trpt->bup.oval; ; goto R999; - case 7: /* STATE 14 */ + case 7: /* STATE 13 */ ; ((P4 *)this)->i = trpt->bup.ovals[1]; now.buffer_use[ Index(((P4 *)this)->i, 4) ] = trpt->bup.ovals[0]; @@ -42,21 +41,21 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 8: /* STATE 15 */ + case 8: /* STATE 14 */ ; /* 0 */ ((P4 *)this)->i = trpt->bup.oval; ; ; goto R999; - case 9: /* STATE 20 */ + case 9: /* STATE 19 */ ; ; delproc(0, now._nr_pr-1); ; goto R999; - case 10: /* STATE 22 */ + case 10: /* STATE 21 */ ; ((P4 *)this)->i = trpt->bup.oval; ; @@ -64,13 +63,13 @@ ; goto R999; - case 11: /* STATE 24 */ + case 11: /* STATE 23 */ ; now.refcount = trpt->bup.oval; ; goto R999; - case 12: /* STATE 26 */ + case 12: /* STATE 25 */ ; ((P4 *)this)->i = trpt->bup.oval; ; @@ -78,7 +77,7 @@ ; goto R999; - case 13: /* STATE 32 */ + case 13: /* STATE 31 */ ; ((P4 *)this)->i = trpt->bup.ovals[1]; /* 0 */ ((P4 *)this)->i = trpt->bup.ovals[0]; @@ -87,19 +86,19 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 14: /* STATE 32 */ + case 14: /* STATE 31 */ ; ((P4 *)this)->i = trpt->bup.oval; ; goto R999; - case 15: /* STATE 34 */ + case 15: /* STATE 33 */ ; now.refcount = trpt->bup.oval; ; goto R999; - case 16: /* STATE 36 */ + case 16: /* STATE 35 */ ; ((P4 *)this)->i = trpt->bup.oval; ; @@ -107,14 +106,14 @@ ; goto R999; - case 17: /* STATE 37 */ + case 17: /* STATE 36 */ ; /* 0 */ ((P4 *)this)->i = trpt->bup.oval; ; ; goto R999; - case 18: /* STATE 45 */ + case 18: /* STATE 44 */ ; ((P4 *)this)->commit_sum = trpt->bup.ovals[1]; ((P4 *)this)->j = trpt->bup.ovals[0]; @@ -122,7 +121,7 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 19: /* STATE 49 */ + case 19: /* STATE 47 */ ; ((P4 *)this)->j = trpt->bup.ovals[1]; ((P4 *)this)->commit_sum = trpt->bup.ovals[0]; @@ -130,7 +129,7 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 20: /* STATE 50 */ + case 20: /* STATE 48 */ ; /* 0 */ ((P4 *)this)->j = trpt->bup.oval; ; @@ -138,10 +137,10 @@ goto R999; ; - case 21: /* STATE 55 */ + case 21: /* STATE 53 */ goto R999; - case 22: /* STATE 58 */ + case 22: /* STATE 56 */ ; p_restor(II); ; @@ -203,29 +202,22 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 31: /* STATE 24 */ + case 31: /* STATE 17 */ ; - now.read_off = trpt->bup.ovals[3]; - now.retrieve_count[ Index(((now.read_off%4)/(4/2)), 2) ] = trpt->bup.ovals[2]; - ((P2 *)this)->tmp_retrieve = trpt->bup.ovals[1]; - /* 0 */ ((P2 *)this)->i = trpt->bup.ovals[0]; + /* 0 */ ((P2 *)this)->i = trpt->bup.oval; ; ; - ungrab_ints(trpt->bup.ovals, 4); goto R999; - case 32: /* STATE 24 */ + case 32: /* STATE 22 */ ; - now.read_off = trpt->bup.ovals[2]; - now.retrieve_count[ Index(((now.read_off%4)/(4/2)), 2) ] = trpt->bup.ovals[1]; - ((P2 *)this)->tmp_retrieve = trpt->bup.ovals[0]; + now.read_off = trpt->bup.oval; ; - ungrab_ints(trpt->bup.ovals, 3); goto R999; ; ; - case 34: /* STATE 31 */ + case 34: /* STATE 29 */ ; p_restor(II); ; @@ -323,11 +315,12 @@ case 47: /* STATE 40 */ ; - deliver = trpt->bup.ovals[1]; - /* 0 */ ((P1 *)this)->tmp_commit = trpt->bup.ovals[0]; + deliver = trpt->bup.ovals[2]; + /* 1 */ ((P1 *)this)->tmp_commit = trpt->bup.ovals[1]; + /* 0 */ ((P1 *)this)->prev_off = trpt->bup.ovals[0]; ; ; - ungrab_ints(trpt->bup.ovals, 2); + ungrab_ints(trpt->bup.ovals, 3); goto R999; ; @@ -409,12 +402,13 @@ case 60: /* STATE 27 */ ; - now.refcount = trpt->bup.ovals[2]; - deliver = trpt->bup.ovals[1]; - /* 0 */ ((P0 *)this)->tmp_commit = trpt->bup.ovals[0]; + now.refcount = trpt->bup.ovals[3]; + deliver = trpt->bup.ovals[2]; + /* 1 */ ((P0 *)this)->tmp_commit = trpt->bup.ovals[1]; + /* 0 */ ((P0 *)this)->prev_off = trpt->bup.ovals[0]; ; ; - ungrab_ints(trpt->bup.ovals, 3); + ungrab_ints(trpt->bup.ovals, 4); goto R999; case 61: /* STATE 27 */ diff --git a/trunk/verif/examples/pan.c b/trunk/verif/examples/pan.c index 928afc4e..2c12633e 100644 --- a/trunk/verif/examples/pan.c +++ b/trunk/verif/examples/pan.c @@ -478,7 +478,7 @@ addproc(int n) break; case 4: /* :init: */ ((P4 *)pptr(h))->_t = 4; - ((P4 *)pptr(h))->_p = 42; reached4[42]=1; + ((P4 *)pptr(h))->_p = 41; reached4[41]=1; /* params: */ /* locals: */ ((P4 *)pptr(h))->i = 0; @@ -508,20 +508,14 @@ addproc(int n) break; case 2: /* reader */ ((P2 *)pptr(h))->_t = 2; - ((P2 *)pptr(h))->_p = 28; reached2[28]=1; + ((P2 *)pptr(h))->_p = 26; reached2[26]=1; /* params: */ /* locals: */ ((P2 *)pptr(h))->i = 0; ((P2 *)pptr(h))->j = 0; - ((P2 *)pptr(h))->tmp_retrieve = 0; - ((P2 *)pptr(h))->lwrite_off = 0; - ((P2 *)pptr(h))->lcommit_count = 0; #ifdef VAR_RANGES logval("reader:i", ((P2 *)pptr(h))->i); logval("reader:j", ((P2 *)pptr(h))->j); - logval("reader:tmp_retrieve", ((P2 *)pptr(h))->tmp_retrieve); - logval("reader:lwrite_off", ((P2 *)pptr(h))->lwrite_off); - logval("reader:lcommit_count", ((P2 *)pptr(h))->lcommit_count); #endif #ifdef HAS_CODE locinit2(h); @@ -9835,12 +9829,6 @@ iniglobals(void) } } now.read_off = 0; - { int l_in; - for (l_in = 0; l_in < 2; l_in++) - { - now.retrieve_count[l_in] = 0; - } - } now.events_lost = 0; now.refcount = 0; #ifdef VAR_RANGES @@ -9858,12 +9846,6 @@ iniglobals(void) } } logval("read_off", now.read_off); - { int l_in; - for (l_in = 0; l_in < 2; l_in++) - { - logval("retrieve_count[l_in]", now.retrieve_count[l_in]); - } - } logval("events_lost", now.events_lost); logval("refcount", now.refcount); #endif @@ -11464,12 +11446,6 @@ c_globals(void) } } printf(" byte read_off: %d\n", now.read_off); - { int l_in; - for (l_in = 0; l_in < 2; l_in++) - { - printf(" byte retrieve_count[%d]: %d\n", l_in, now.retrieve_count[l_in]); - } - } printf(" byte events_lost: %d\n", now.events_lost); printf(" byte refcount: %d\n", now.refcount); { int l_in; @@ -11497,9 +11473,6 @@ c_locals(int pid, int tp) printf("local vars proc %d (reader):\n", pid); printf(" byte i: %d\n", ((P2 *)pptr(pid))->i); printf(" byte j: %d\n", ((P2 *)pptr(pid))->j); - printf(" byte tmp_retrieve: %d\n", ((P2 *)pptr(pid))->tmp_retrieve); - printf(" byte lwrite_off: %d\n", ((P2 *)pptr(pid))->lwrite_off); - printf(" byte lcommit_count: %d\n", ((P2 *)pptr(pid))->lcommit_count); break; case 1: printf("local vars proc %d (tracer):\n", pid); diff --git a/trunk/verif/examples/pan.h b/trunk/verif/examples/pan.h index 0dcc8a8b..e4ec3cd1 100644 --- a/trunk/verif/examples/pan.h +++ b/trunk/verif/examples/pan.h @@ -23,6 +23,9 @@ char *trailfilename; #ifndef uint #define uint unsigned int #endif +#ifndef HASH32 +#define HASH64 +#endif #define DELTA 500 #ifdef MA #if NCORE>1 && !defined(SEP_STATE) @@ -53,38 +56,38 @@ typedef struct S_F_MAP { char *fnm; int from; int upto; } S_F_MAP; -#define nstates4 59 /* :init: */ -#define endstate4 58 +#define nstates4 57 /* :init: */ +#define endstate4 56 short src_ln4 [] = { - 0, 225, 227, 228, 229, 230, 231, 231, - 226, 233, 226, 233, 235, 236, 237, 238, - 238, 234, 240, 234, 240, 241, 242, 244, - 245, 246, 247, 248, 248, 243, 250, 243, - 250, 252, 253, 254, 255, 256, 256, 251, - 258, 251, 224, 262, 263, 264, 266, 267, - 271, 272, 273, 273, 265, 278, 265, 278, - 282, 260, 284, 0, }; + 0, 226, 228, 229, 230, 231, 231, 227, + 233, 227, 233, 235, 236, 237, 238, 238, + 234, 240, 234, 240, 241, 242, 244, 245, + 246, 247, 248, 248, 243, 250, 243, 250, + 252, 253, 254, 255, 256, 256, 251, 258, + 251, 225, 262, 263, 264, 266, 267, 272, + 273, 273, 265, 278, 265, 278, 282, 260, + 284, 0, }; S_F_MAP src_file4 [] = { { "-", 0, 0 }, - { "buffer.spin", 1, 58 }, - { "-", 59, 60 } + { "buffer.spin", 1, 56 }, + { "-", 57, 58 } }; uchar reached4 [] = { - 0, 1, 1, 0, 0, 0, 1, 1, - 0, 1, 1, 0, 1, 0, 0, 1, - 1, 0, 1, 1, 0, 0, 0, 1, - 0, 0, 0, 1, 1, 0, 1, 1, - 0, 1, 0, 0, 0, 1, 1, 0, - 1, 1, 0, 1, 0, 0, 1, 0, + 0, 1, 1, 0, 0, 1, 1, 0, + 1, 1, 0, 1, 0, 0, 1, 1, + 0, 1, 1, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, - 0, 0, 0, 0, }; + 1, 0, 0, 0, 1, 1, 0, 1, + 1, 0, 1, 0, 0, 1, 0, 0, + 1, 1, 0, 1, 1, 0, 0, 0, + 0, 0, }; uchar *loopstate4; #define nstates3 10 /* cleaner */ #define endstate3 9 short src_ln3 [] = { - 0, 210, 211, 212, 213, 209, 215, 209, - 208, 216, 0, }; + 0, 211, 212, 213, 214, 210, 216, 210, + 209, 217, 0, }; S_F_MAP src_file3 [] = { { "-", 0, 0 }, { "buffer.spin", 1, 9 }, @@ -95,37 +98,35 @@ uchar reached3 [] = { 0, 0, 0, }; uchar *loopstate3; -#define nstates2 32 /* reader */ -#define endstate2 31 +#define nstates2 30 /* reader */ +#define endstate2 29 short src_ln2 [] = { - 0, 169, 171, 173, 174, 175, 176, 177, - 177, 172, 179, 172, 170, 187, 189, 190, - 191, 192, 192, 188, 194, 188, 194, 196, - 197, 186, 199, 199, 164, 201, 164, 201, - 0, }; + 0, 177, 179, 181, 182, 183, 184, 185, + 185, 180, 187, 180, 178, 191, 193, 194, + 195, 196, 196, 192, 198, 192, 198, 190, + 200, 200, 172, 202, 172, 202, 0, }; S_F_MAP src_file2 [] = { { "-", 0, 0 }, - { "buffer.spin", 1, 31 }, - { "-", 32, 33 } + { "buffer.spin", 1, 29 }, + { "-", 30, 31 } }; uchar reached2 [] = { 0, 1, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 0, - 0, 0, 1, 1, 0, 1, 1, 0, - 0, }; + 1, 1, 0, 1, 1, 0, 0, }; uchar *loopstate2; #define nstates1 51 /* tracer */ #define endstate1 50 short src_ln1 [] = { - 0, 99, 100, 98, 104, 105, 106, 106, - 103, 108, 102, 111, 111, 112, 112, 110, - 114, 114, 116, 117, 118, 119, 120, 120, - 115, 122, 115, 109, 127, 129, 130, 131, - 132, 132, 128, 134, 128, 134, 135, 137, - 137, 138, 138, 136, 140, 126, 142, 144, - 146, 141, 148, 0, }; + 0, 106, 107, 105, 111, 112, 113, 113, + 110, 115, 109, 118, 118, 119, 119, 117, + 121, 121, 123, 124, 125, 126, 127, 127, + 122, 129, 122, 116, 134, 136, 137, 138, + 139, 139, 135, 141, 135, 141, 142, 145, + 146, 147, 148, 143, 150, 133, 152, 154, + 156, 151, 158, 0, }; S_F_MAP src_file1 [] = { { "-", 0, 0 }, { "buffer.spin", 1, 50 }, @@ -144,10 +145,10 @@ uchar *loopstate1; #define nstates0 31 /* switcher */ #define endstate0 30 short src_ln0 [] = { - 0, 56, 57, 58, 61, 62, 63, 64, - 64, 59, 66, 55, 69, 69, 70, 70, - 68, 72, 67, 75, 76, 78, 78, 79, - 79, 77, 81, 81, 74, 84, 85, 0, }; + 0, 60, 61, 62, 65, 66, 67, 68, + 68, 63, 70, 59, 73, 73, 74, 74, + 72, 76, 71, 79, 80, 83, 84, 85, + 86, 81, 88, 88, 78, 91, 92, 0, }; S_F_MAP src_file0 [] = { { "-", 0, 0 }, { "buffer.spin", 1, 30 }, @@ -224,11 +225,8 @@ typedef struct P2 { /* reader */ unsigned _p : 7; /* state */ uchar i; uchar j; - uchar tmp_retrieve; - uchar lwrite_off; - uchar lcommit_count; } P2; -#define Air2 (sizeof(P2) - Offsetof(P2, lcommit_count) - 1*sizeof(uchar)) +#define Air2 (sizeof(P2) - Offsetof(P2, j) - 1*sizeof(uchar)) #define Ptracer ((P1 *)this) typedef struct P1 { /* tracer */ unsigned _pid : 8; /* 0..255 */ @@ -453,7 +451,6 @@ typedef struct State { uchar write_off; uchar commit_count[2]; uchar read_off; - uchar retrieve_count[2]; uchar events_lost; uchar refcount; uchar sv[VECTORSZ]; @@ -473,9 +470,9 @@ uchar *loopstate5; /* np_ */ #define endstate5 2 /* np_ */ #define start5 0 /* np_ */ -#define start4 42 +#define start4 41 #define start3 8 -#define start2 28 +#define start2 26 #define start1 3 #define start0 11 #ifdef NP diff --git a/trunk/verif/examples/pan.m b/trunk/verif/examples/pan.m index 5d40303e..357708ae 100644 --- a/trunk/verif/examples/pan.m +++ b/trunk/verif/examples/pan.m @@ -15,7 +15,7 @@ _m = 3; goto P999; /* PROC :init: */ - case 3: /* STATE 1 - line 225 "buffer.spin" - [i = 0] (0:0:1 - 1) */ + case 3: /* STATE 1 - line 226 "buffer.spin" - [i = 0] (0:0:1 - 1) */ IfNotBlocked reached[4][1] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); @@ -25,43 +25,35 @@ #endif ; _m = 3; goto P999; /* 0 */ - case 4: /* STATE 2 - line 227 "buffer.spin" - [((i<2))] (8:0:3 - 1) */ + case 4: /* STATE 2 - line 228 "buffer.spin" - [((i<2))] (7:0:2 - 1) */ IfNotBlocked reached[4][2] = 1; if (!((((int)((P4 *)this)->i)<2))) continue; - /* merge: commit_count[i] = 0(8, 3, 8) */ + /* merge: commit_count[i] = 0(7, 3, 7) */ reached[4][3] = 1; - (trpt+1)->bup.ovals = grab_ints(3); + (trpt+1)->bup.ovals = grab_ints(2); (trpt+1)->bup.ovals[0] = ((int)now.commit_count[ Index(((int)((P4 *)this)->i), 2) ]); now.commit_count[ Index(((P4 *)this)->i, 2) ] = 0; #ifdef VAR_RANGES logval("commit_count[:init::i]", ((int)now.commit_count[ Index(((int)((P4 *)this)->i), 2) ])); #endif ; - /* merge: retrieve_count[i] = 0(8, 4, 8) */ + /* merge: i = (i+1)(7, 4, 7) */ reached[4][4] = 1; - (trpt+1)->bup.ovals[1] = ((int)now.retrieve_count[ Index(((int)((P4 *)this)->i), 2) ]); - now.retrieve_count[ Index(((P4 *)this)->i, 2) ] = 0; -#ifdef VAR_RANGES - logval("retrieve_count[:init::i]", ((int)now.retrieve_count[ Index(((int)((P4 *)this)->i), 2) ])); -#endif - ; - /* merge: i = (i+1)(8, 5, 8) */ - reached[4][5] = 1; - (trpt+1)->bup.ovals[2] = ((int)((P4 *)this)->i); + (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i); ((P4 *)this)->i = (((int)((P4 *)this)->i)+1); #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 9, 8) */ - reached[4][9] = 1; + /* merge: .(goto)(0, 8, 7) */ + reached[4][8] = 1; ; - _m = 3; goto P999; /* 4 */ - case 5: /* STATE 6 - line 231 "buffer.spin" - [((i>=2))] (17:0:2 - 1) */ + _m = 3; goto P999; /* 3 */ + case 5: /* STATE 5 - line 231 "buffer.spin" - [((i>=2))] (16:0:2 - 1) */ IfNotBlocked - reached[4][6] = 1; + reached[4][5] = 1; if (!((((int)((P4 *)this)->i)>=2))) continue; /* dead 1: i */ (trpt+1)->bup.ovals = grab_ints(2); @@ -70,41 +62,41 @@ if (!readtrail) #endif ((P4 *)this)->i = 0; - /* merge: goto :b6(17, 7, 17) */ - reached[4][7] = 1; + /* merge: goto :b6(16, 6, 16) */ + reached[4][6] = 1; ; - /* merge: i = 0(17, 11, 17) */ - reached[4][11] = 1; + /* merge: i = 0(16, 10, 16) */ + reached[4][10] = 1; (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i); ((P4 *)this)->i = 0; #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 18, 17) */ - reached[4][18] = 1; + /* merge: .(goto)(0, 17, 16) */ + reached[4][17] = 1; ; _m = 3; goto P999; /* 3 */ - case 6: /* STATE 11 - line 233 "buffer.spin" - [i = 0] (0:17:1 - 3) */ + case 6: /* STATE 10 - line 233 "buffer.spin" - [i = 0] (0:16:1 - 3) */ IfNotBlocked - reached[4][11] = 1; + reached[4][10] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); ((P4 *)this)->i = 0; #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 18, 17) */ - reached[4][18] = 1; + /* merge: .(goto)(0, 17, 16) */ + reached[4][17] = 1; ; _m = 3; goto P999; /* 1 */ - case 7: /* STATE 12 - line 235 "buffer.spin" - [((i<4))] (17:0:2 - 1) */ + case 7: /* STATE 11 - line 235 "buffer.spin" - [((i<4))] (16:0:2 - 1) */ IfNotBlocked - reached[4][12] = 1; + reached[4][11] = 1; if (!((((int)((P4 *)this)->i)<4))) continue; - /* merge: buffer_use[i] = 0(17, 13, 17) */ - reached[4][13] = 1; + /* merge: buffer_use[i] = 0(16, 12, 16) */ + reached[4][12] = 1; (trpt+1)->bup.ovals = grab_ints(2); (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((int)((P4 *)this)->i), 4) ]); now.buffer_use[ Index(((P4 *)this)->i, 4) ] = 0; @@ -112,21 +104,21 @@ logval("buffer_use[:init::i]", ((int)now.buffer_use[ Index(((int)((P4 *)this)->i), 4) ])); #endif ; - /* merge: i = (i+1)(17, 14, 17) */ - reached[4][14] = 1; + /* merge: i = (i+1)(16, 13, 16) */ + reached[4][13] = 1; (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i); ((P4 *)this)->i = (((int)((P4 *)this)->i)+1); #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 18, 17) */ - reached[4][18] = 1; + /* merge: .(goto)(0, 17, 16) */ + reached[4][17] = 1; ; _m = 3; goto P999; /* 3 */ - case 8: /* STATE 15 - line 238 "buffer.spin" - [((i>=4))] (0:0:1 - 1) */ + case 8: /* STATE 14 - line 238 "buffer.spin" - [((i>=4))] (0:0:1 - 1) */ IfNotBlocked - reached[4][15] = 1; + reached[4][14] = 1; if (!((((int)((P4 *)this)->i)>=4))) continue; /* dead 1: i */ (trpt+1)->bup.oval = ((P4 *)this)->i; @@ -135,36 +127,36 @@ #endif ((P4 *)this)->i = 0; _m = 3; goto P999; /* 0 */ - case 9: /* STATE 20 - line 240 "buffer.spin" - [(run reader())] (0:0:0 - 3) */ + case 9: /* STATE 19 - line 240 "buffer.spin" - [(run reader())] (0:0:0 - 3) */ IfNotBlocked - reached[4][20] = 1; + reached[4][19] = 1; if (!(addproc(2))) continue; _m = 3; goto P999; /* 0 */ - case 10: /* STATE 21 - line 241 "buffer.spin" - [(run cleaner())] (29:0:1 - 1) */ + case 10: /* STATE 20 - line 241 "buffer.spin" - [(run cleaner())] (28:0:1 - 1) */ IfNotBlocked - reached[4][21] = 1; + reached[4][20] = 1; if (!(addproc(3))) continue; - /* merge: i = 0(0, 22, 29) */ - reached[4][22] = 1; + /* merge: i = 0(0, 21, 28) */ + reached[4][21] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); ((P4 *)this)->i = 0; #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 30, 29) */ - reached[4][30] = 1; + /* merge: .(goto)(0, 29, 28) */ + reached[4][29] = 1; ; _m = 3; goto P999; /* 2 */ - case 11: /* STATE 23 - line 244 "buffer.spin" - [((i<4))] (25:0:1 - 1) */ + case 11: /* STATE 22 - line 244 "buffer.spin" - [((i<4))] (24:0:1 - 1) */ IfNotBlocked - reached[4][23] = 1; + reached[4][22] = 1; if (!((((int)((P4 *)this)->i)<4))) continue; - /* merge: refcount = (refcount+1)(0, 24, 25) */ - reached[4][24] = 1; + /* merge: refcount = (refcount+1)(0, 23, 24) */ + reached[4][23] = 1; (trpt+1)->bup.oval = ((int)now.refcount); now.refcount = (((int)now.refcount)+1); #ifdef VAR_RANGES @@ -172,26 +164,26 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 12: /* STATE 25 - line 246 "buffer.spin" - [(run tracer())] (29:0:1 - 1) */ + case 12: /* STATE 24 - line 246 "buffer.spin" - [(run tracer())] (28:0:1 - 1) */ IfNotBlocked - reached[4][25] = 1; + reached[4][24] = 1; if (!(addproc(1))) continue; - /* merge: i = (i+1)(0, 26, 29) */ - reached[4][26] = 1; + /* merge: i = (i+1)(0, 25, 28) */ + reached[4][25] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); ((P4 *)this)->i = (((int)((P4 *)this)->i)+1); #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 30, 29) */ - reached[4][30] = 1; + /* merge: .(goto)(0, 29, 28) */ + reached[4][29] = 1; ; _m = 3; goto P999; /* 2 */ - case 13: /* STATE 27 - line 248 "buffer.spin" - [((i>=4))] (39:0:2 - 1) */ + case 13: /* STATE 26 - line 248 "buffer.spin" - [((i>=4))] (38:0:2 - 1) */ IfNotBlocked - reached[4][27] = 1; + reached[4][26] = 1; if (!((((int)((P4 *)this)->i)>=4))) continue; /* dead 1: i */ (trpt+1)->bup.ovals = grab_ints(2); @@ -200,41 +192,41 @@ if (!readtrail) #endif ((P4 *)this)->i = 0; - /* merge: goto :b8(39, 28, 39) */ - reached[4][28] = 1; + /* merge: goto :b8(38, 27, 38) */ + reached[4][27] = 1; ; - /* merge: i = 0(39, 32, 39) */ - reached[4][32] = 1; + /* merge: i = 0(38, 31, 38) */ + reached[4][31] = 1; (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i); ((P4 *)this)->i = 0; #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 40, 39) */ - reached[4][40] = 1; + /* merge: .(goto)(0, 39, 38) */ + reached[4][39] = 1; ; _m = 3; goto P999; /* 3 */ - case 14: /* STATE 32 - line 250 "buffer.spin" - [i = 0] (0:39:1 - 3) */ + case 14: /* STATE 31 - line 250 "buffer.spin" - [i = 0] (0:38:1 - 3) */ IfNotBlocked - reached[4][32] = 1; + reached[4][31] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); ((P4 *)this)->i = 0; #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 40, 39) */ - reached[4][40] = 1; + /* merge: .(goto)(0, 39, 38) */ + reached[4][39] = 1; ; _m = 3; goto P999; /* 1 */ - case 15: /* STATE 33 - line 252 "buffer.spin" - [((i<1))] (35:0:1 - 1) */ + case 15: /* STATE 32 - line 252 "buffer.spin" - [((i<1))] (34:0:1 - 1) */ IfNotBlocked - reached[4][33] = 1; + reached[4][32] = 1; if (!((((int)((P4 *)this)->i)<1))) continue; - /* merge: refcount = (refcount+1)(0, 34, 35) */ - reached[4][34] = 1; + /* merge: refcount = (refcount+1)(0, 33, 34) */ + reached[4][33] = 1; (trpt+1)->bup.oval = ((int)now.refcount); now.refcount = (((int)now.refcount)+1); #ifdef VAR_RANGES @@ -242,26 +234,26 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 16: /* STATE 35 - line 254 "buffer.spin" - [(run switcher())] (39:0:1 - 1) */ + case 16: /* STATE 34 - line 254 "buffer.spin" - [(run switcher())] (38:0:1 - 1) */ IfNotBlocked - reached[4][35] = 1; + reached[4][34] = 1; if (!(addproc(0))) continue; - /* merge: i = (i+1)(0, 36, 39) */ - reached[4][36] = 1; + /* merge: i = (i+1)(0, 35, 38) */ + reached[4][35] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); ((P4 *)this)->i = (((int)((P4 *)this)->i)+1); #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 40, 39) */ - reached[4][40] = 1; + /* merge: .(goto)(0, 39, 38) */ + reached[4][39] = 1; ; _m = 3; goto P999; /* 2 */ - case 17: /* STATE 37 - line 256 "buffer.spin" - [((i>=1))] (41:0:1 - 1) */ + case 17: /* STATE 36 - line 256 "buffer.spin" - [((i>=1))] (40:0:1 - 1) */ IfNotBlocked - reached[4][37] = 1; + reached[4][36] = 1; if (!((((int)((P4 *)this)->i)>=1))) continue; /* dead 1: i */ (trpt+1)->bup.oval = ((P4 *)this)->i; @@ -269,16 +261,16 @@ if (!readtrail) #endif ((P4 *)this)->i = 0; - /* merge: goto :b9(0, 38, 41) */ - reached[4][38] = 1; + /* merge: goto :b9(0, 37, 40) */ + reached[4][37] = 1; ; _m = 3; goto P999; /* 1 */ - case 18: /* STATE 43 - line 262 "buffer.spin" - [assert((((write_off-read_off)>=0)&&((write_off-read_off)<(255/2))))] (0:52:2 - 1) */ + case 18: /* STATE 42 - line 262 "buffer.spin" - [assert((((write_off-read_off)>=0)&&((write_off-read_off)<(255/2))))] (0:50:2 - 1) */ IfNotBlocked - reached[4][43] = 1; + reached[4][42] = 1; assert((((((int)now.write_off)-((int)now.read_off))>=0)&&((((int)now.write_off)-((int)now.read_off))<(255/2))), "(((write_off-read_off)>=0)&&((write_off-read_off)<(255/2)))", II, tt, t); - /* merge: j = 0(52, 44, 52) */ - reached[4][44] = 1; + /* merge: j = 0(50, 43, 50) */ + reached[4][43] = 1; (trpt+1)->bup.ovals = grab_ints(2); (trpt+1)->bup.ovals[0] = ((int)((P4 *)this)->j); ((P4 *)this)->j = 0; @@ -286,25 +278,25 @@ logval(":init::j", ((int)((P4 *)this)->j)); #endif ; - /* merge: commit_sum = 0(52, 45, 52) */ - reached[4][45] = 1; + /* merge: commit_sum = 0(50, 44, 50) */ + reached[4][44] = 1; (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->commit_sum); ((P4 *)this)->commit_sum = 0; #ifdef VAR_RANGES logval(":init::commit_sum", ((int)((P4 *)this)->commit_sum)); #endif ; - /* merge: .(goto)(0, 53, 52) */ - reached[4][53] = 1; + /* merge: .(goto)(0, 51, 50) */ + reached[4][51] = 1; ; _m = 3; goto P999; /* 3 */ - case 19: /* STATE 46 - line 266 "buffer.spin" - [((j<2))] (52:0:2 - 1) */ + case 19: /* STATE 45 - line 266 "buffer.spin" - [((j<2))] (50:0:2 - 1) */ IfNotBlocked - reached[4][46] = 1; + reached[4][45] = 1; if (!((((int)((P4 *)this)->j)<2))) continue; - /* merge: commit_sum = (commit_sum+commit_count[j])(52, 47, 52) */ - reached[4][47] = 1; + /* merge: commit_sum = (commit_sum+commit_count[j])(50, 46, 50) */ + reached[4][46] = 1; (trpt+1)->bup.ovals = grab_ints(2); (trpt+1)->bup.ovals[0] = ((int)((P4 *)this)->commit_sum); ((P4 *)this)->commit_sum = (((int)((P4 *)this)->commit_sum)+((int)now.commit_count[ Index(((int)((P4 *)this)->j), 2) ])); @@ -312,24 +304,21 @@ logval(":init::commit_sum", ((int)((P4 *)this)->commit_sum)); #endif ; - /* merge: assert((((commit_count[j]-retrieve_count[j])>=0)&&((commit_count[j]-retrieve_count[j])<(255/2))))(52, 48, 52) */ - reached[4][48] = 1; - assert((((((int)now.commit_count[ Index(((int)((P4 *)this)->j), 2) ])-((int)now.retrieve_count[ Index(((int)((P4 *)this)->j), 2) ]))>=0)&&((((int)now.commit_count[ Index(((int)((P4 *)this)->j), 2) ])-((int)now.retrieve_count[ Index(((int)((P4 *)this)->j), 2) ]))<(255/2))), "(((commit_count[j]-retrieve_count[j])>=0)&&((commit_count[j]-retrieve_count[j])<(255/2)))", II, tt, t); - /* merge: j = (j+1)(52, 49, 52) */ - reached[4][49] = 1; + /* merge: j = (j+1)(50, 47, 50) */ + reached[4][47] = 1; (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->j); ((P4 *)this)->j = (((int)((P4 *)this)->j)+1); #ifdef VAR_RANGES logval(":init::j", ((int)((P4 *)this)->j)); #endif ; - /* merge: .(goto)(0, 53, 52) */ - reached[4][53] = 1; + /* merge: .(goto)(0, 51, 50) */ + reached[4][51] = 1; ; - _m = 3; goto P999; /* 4 */ - case 20: /* STATE 50 - line 273 "buffer.spin" - [((j>=2))] (58:0:1 - 1) */ + _m = 3; goto P999; /* 3 */ + case 20: /* STATE 48 - line 273 "buffer.spin" - [((j>=2))] (56:0:1 - 1) */ IfNotBlocked - reached[4][50] = 1; + reached[4][48] = 1; if (!((((int)((P4 *)this)->j)>=2))) continue; /* dead 1: j */ (trpt+1)->bup.oval = ((P4 *)this)->j; @@ -337,32 +326,32 @@ if (!readtrail) #endif ((P4 *)this)->j = 0; - /* merge: goto :b10(58, 51, 58) */ - reached[4][51] = 1; + /* merge: goto :b10(56, 49, 56) */ + reached[4][49] = 1; ; - /* merge: assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))(58, 55, 58) */ - reached[4][55] = 1; + /* merge: assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))(56, 53, 56) */ + reached[4][53] = 1; assert((((((int)now.write_off)-((int)((P4 *)this)->commit_sum))>=0)&&((((int)now.write_off)-((int)((P4 *)this)->commit_sum))<(255/2))), "(((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2)))", II, tt, t); - /* merge: assert((((4+1)>4)||(events_lost==0)))(58, 56, 58) */ - reached[4][56] = 1; + /* merge: assert((((4+1)>4)||(events_lost==0)))(56, 54, 56) */ + reached[4][54] = 1; assert((((4+1)>4)||(((int)now.events_lost)==0)), "(((4+1)>4)||(events_lost==0))", II, tt, t); _m = 3; goto P999; /* 3 */ - case 21: /* STATE 55 - line 278 "buffer.spin" - [assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))] (0:58:0 - 3) */ + case 21: /* STATE 53 - line 278 "buffer.spin" - [assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))] (0:56:0 - 3) */ IfNotBlocked - reached[4][55] = 1; + reached[4][53] = 1; assert((((((int)now.write_off)-((int)((P4 *)this)->commit_sum))>=0)&&((((int)now.write_off)-((int)((P4 *)this)->commit_sum))<(255/2))), "(((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2)))", II, tt, t); - /* merge: assert((((4+1)>4)||(events_lost==0)))(58, 56, 58) */ - reached[4][56] = 1; + /* merge: assert((((4+1)>4)||(events_lost==0)))(56, 54, 56) */ + reached[4][54] = 1; assert((((4+1)>4)||(((int)now.events_lost)==0)), "(((4+1)>4)||(events_lost==0))", II, tt, t); _m = 3; goto P999; /* 1 */ - case 22: /* STATE 58 - line 284 "buffer.spin" - [-end-] (0:0:0 - 1) */ + case 22: /* STATE 56 - line 284 "buffer.spin" - [-end-] (0:0:0 - 1) */ IfNotBlocked - reached[4][58] = 1; + reached[4][56] = 1; if (!delproc(1, II)) continue; _m = 3; goto P999; /* 0 */ /* PROC cleaner */ - case 23: /* STATE 1 - line 210 "buffer.spin" - [((refcount==0))] (3:0:1 - 1) */ + case 23: /* STATE 1 - line 211 "buffer.spin" - [((refcount==0))] (3:0:1 - 1) */ IfNotBlocked reached[3][1] = 1; if (!((((int)now.refcount)==0))) @@ -376,7 +365,7 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 24: /* STATE 3 - line 212 "buffer.spin" - [(run switcher())] (7:0:0 - 1) */ + case 24: /* STATE 3 - line 213 "buffer.spin" - [(run switcher())] (7:0:0 - 1) */ IfNotBlocked reached[3][3] = 1; if (!(addproc(0))) @@ -385,20 +374,20 @@ reached[3][4] = 1; ; _m = 3; goto P999; /* 1 */ - case 25: /* STATE 9 - line 216 "buffer.spin" - [-end-] (0:0:0 - 1) */ + case 25: /* STATE 9 - line 217 "buffer.spin" - [-end-] (0:0:0 - 1) */ IfNotBlocked reached[3][9] = 1; if (!delproc(1, II)) continue; _m = 3; goto P999; /* 0 */ /* PROC reader */ - case 26: /* STATE 1 - line 169 "buffer.spin" - [((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&((commit_count[((read_off%4)/(4/2))]-retrieve_count[((read_off%4)/(4/2))])==(4/2))))] (0:0:0 - 1) */ + case 26: /* STATE 1 - line 177 "buffer.spin" - [((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&(((commit_count[((read_off%4)/(4/2))]-(4/2))-(((read_off/4)*4)/2))==0)))] (0:0:0 - 1) */ IfNotBlocked reached[2][1] = 1; - if (!((((((((int)now.write_off)/(4/2))-(((int)now.read_off)/(4/2)))>0)&&(((((int)now.write_off)/(4/2))-(((int)now.read_off)/(4/2)))<(255/2)))&&((((int)now.commit_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])-((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]))==(4/2))))) + if (!((((((((int)now.write_off)/(4/2))-(((int)now.read_off)/(4/2)))>0)&&(((((int)now.write_off)/(4/2))-(((int)now.read_off)/(4/2)))<(255/2)))&&(((((int)now.commit_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])-(4/2))-(((((int)now.read_off)/4)*4)/2))==0)))) continue; _m = 3; goto P999; /* 0 */ - case 27: /* STATE 2 - line 171 "buffer.spin" - [i = 0] (0:0:1 - 1) */ + case 27: /* STATE 2 - line 179 "buffer.spin" - [i = 0] (0:0:1 - 1) */ IfNotBlocked reached[2][2] = 1; (trpt+1)->bup.oval = ((int)((P2 *)this)->i); @@ -408,7 +397,7 @@ #endif ; _m = 3; goto P999; /* 0 */ - case 28: /* STATE 3 - line 173 "buffer.spin" - [((i<(4/2)))] (9:0:2 - 1) */ + case 28: /* STATE 3 - line 181 "buffer.spin" - [((i<(4/2)))] (9:0:2 - 1) */ IfNotBlocked reached[2][3] = 1; if (!((((int)((P2 *)this)->i)<(4/2)))) @@ -437,7 +426,7 @@ reached[2][10] = 1; ; _m = 3; goto P999; /* 4 */ - case 29: /* STATE 7 - line 177 "buffer.spin" - [((i>=(4/2)))] (11:0:1 - 1) */ + case 29: /* STATE 7 - line 185 "buffer.spin" - [((i>=(4/2)))] (11:0:1 - 1) */ IfNotBlocked reached[2][7] = 1; if (!((((int)((P2 *)this)->i)>=(4/2)))) @@ -451,8 +440,8 @@ reached[2][8] = 1; ; _m = 3; goto P999; /* 1 */ -/* STATE 13 - line 187 "buffer.spin" - [i = 0] (0:0 - 1) same as 27 (0:0 - 1) */ - case 30: /* STATE 14 - line 189 "buffer.spin" - [((i<(4/2)))] (19:0:2 - 1) */ +/* STATE 13 - line 191 "buffer.spin" - [i = 0] (0:0 - 1) same as 27 (0:0 - 1) */ + case 30: /* STATE 14 - line 193 "buffer.spin" - [((i<(4/2)))] (19:0:2 - 1) */ IfNotBlocked reached[2][14] = 1; if (!((((int)((P2 *)this)->i)<(4/2)))) @@ -478,92 +467,41 @@ reached[2][20] = 1; ; _m = 3; goto P999; /* 3 */ - case 31: /* STATE 17 - line 192 "buffer.spin" - [((i>=(4/2)))] (28:0:4 - 1) */ + case 31: /* STATE 17 - line 196 "buffer.spin" - [((i>=(4/2)))] (0:0:1 - 1) */ IfNotBlocked reached[2][17] = 1; if (!((((int)((P2 *)this)->i)>=(4/2)))) continue; - /* dead 1: i */ (trpt+1)->bup.ovals = grab_ints(4); - (trpt+1)->bup.ovals[0] = ((P2 *)this)->i; + /* dead 1: i */ (trpt+1)->bup.oval = ((P2 *)this)->i; #ifdef HAS_CODE if (!readtrail) #endif ((P2 *)this)->i = 0; - /* merge: goto :b4(28, 18, 28) */ - reached[2][18] = 1; - ; - /* merge: tmp_retrieve = (retrieve_count[((read_off%4)/(4/2))]+(4/2))(28, 22, 28) */ - reached[2][22] = 1; - (trpt+1)->bup.ovals[1] = ((int)((P2 *)this)->tmp_retrieve); - ((P2 *)this)->tmp_retrieve = (((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])+(4/2)); -#ifdef VAR_RANGES - logval("reader:tmp_retrieve", ((int)((P2 *)this)->tmp_retrieve)); -#endif - ; - /* merge: retrieve_count[((read_off%4)/(4/2))] = tmp_retrieve(28, 23, 28) */ - reached[2][23] = 1; - (trpt+1)->bup.ovals[2] = ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]); - now.retrieve_count[ Index(((now.read_off%4)/(4/2)), 2) ] = ((int)((P2 *)this)->tmp_retrieve); -#ifdef VAR_RANGES - logval("retrieve_count[((read_off%4)/(4/2))]", ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])); -#endif - ; - /* merge: read_off = (read_off+(4/2))(28, 24, 28) */ - reached[2][24] = 1; - (trpt+1)->bup.ovals[3] = ((int)now.read_off); - now.read_off = (((int)now.read_off)+(4/2)); -#ifdef VAR_RANGES - logval("read_off", ((int)now.read_off)); -#endif - ; - /* merge: .(goto)(0, 29, 28) */ - reached[2][29] = 1; - ; - _m = 3; goto P999; /* 5 */ - case 32: /* STATE 22 - line 194 "buffer.spin" - [tmp_retrieve = (retrieve_count[((read_off%4)/(4/2))]+(4/2))] (0:28:3 - 3) */ + _m = 3; goto P999; /* 0 */ + case 32: /* STATE 22 - line 198 "buffer.spin" - [read_off = (read_off+(4/2))] (0:0:1 - 1) */ IfNotBlocked reached[2][22] = 1; - (trpt+1)->bup.ovals = grab_ints(3); - (trpt+1)->bup.ovals[0] = ((int)((P2 *)this)->tmp_retrieve); - ((P2 *)this)->tmp_retrieve = (((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])+(4/2)); -#ifdef VAR_RANGES - logval("reader:tmp_retrieve", ((int)((P2 *)this)->tmp_retrieve)); -#endif - ; - /* merge: retrieve_count[((read_off%4)/(4/2))] = tmp_retrieve(28, 23, 28) */ - reached[2][23] = 1; - (trpt+1)->bup.ovals[1] = ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]); - now.retrieve_count[ Index(((now.read_off%4)/(4/2)), 2) ] = ((int)((P2 *)this)->tmp_retrieve); -#ifdef VAR_RANGES - logval("retrieve_count[((read_off%4)/(4/2))]", ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])); -#endif - ; - /* merge: read_off = (read_off+(4/2))(28, 24, 28) */ - reached[2][24] = 1; - (trpt+1)->bup.ovals[2] = ((int)now.read_off); + (trpt+1)->bup.oval = ((int)now.read_off); now.read_off = (((int)now.read_off)+(4/2)); #ifdef VAR_RANGES logval("read_off", ((int)now.read_off)); #endif ; - /* merge: .(goto)(0, 29, 28) */ - reached[2][29] = 1; - ; - _m = 3; goto P999; /* 3 */ - case 33: /* STATE 26 - line 199 "buffer.spin" - [((read_off>=(4-events_lost)))] (0:0:0 - 1) */ + _m = 3; goto P999; /* 0 */ + case 33: /* STATE 24 - line 200 "buffer.spin" - [((read_off>=(4-events_lost)))] (0:0:0 - 1) */ IfNotBlocked - reached[2][26] = 1; + reached[2][24] = 1; if (!((((int)now.read_off)>=(4-((int)now.events_lost))))) continue; _m = 3; goto P999; /* 0 */ - case 34: /* STATE 31 - line 201 "buffer.spin" - [-end-] (0:0:0 - 3) */ + case 34: /* STATE 29 - line 202 "buffer.spin" - [-end-] (0:0:0 - 3) */ IfNotBlocked - reached[2][31] = 1; + reached[2][29] = 1; if (!delproc(1, II)) continue; _m = 3; goto P999; /* 0 */ /* PROC tracer */ - case 35: /* STATE 1 - line 99 "buffer.spin" - [prev_off = write_off] (0:10:2 - 1) */ + case 35: /* STATE 1 - line 106 "buffer.spin" - [prev_off = write_off] (0:10:2 - 1) */ IfNotBlocked reached[1][1] = 1; (trpt+1)->bup.ovals = grab_ints(2); @@ -582,7 +520,7 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 36: /* STATE 4 - line 104 "buffer.spin" - [((((new_off-read_off)>4)&&((new_off-read_off)<(255/2))))] (0:0:1 - 1) */ + case 36: /* STATE 4 - line 111 "buffer.spin" - [((((new_off-read_off)>4)&&((new_off-read_off)<(255/2))))] (0:0:1 - 1) */ IfNotBlocked reached[1][4] = 1; if (!((((((int)((P1 *)this)->new_off)-((int)now.read_off))>4)&&((((int)((P1 *)this)->new_off)-((int)now.read_off))<(255/2))))) @@ -593,7 +531,7 @@ #endif ((P1 *)this)->new_off = 0; _m = 3; goto P999; /* 0 */ - case 37: /* STATE 7 - line 106 "buffer.spin" - [(1)] (27:0:0 - 1) */ + case 37: /* STATE 7 - line 113 "buffer.spin" - [(1)] (27:0:0 - 1) */ IfNotBlocked reached[1][7] = 1; if (!(1)) @@ -602,7 +540,7 @@ reached[1][9] = 1; ; _m = 3; goto P999; /* 1 */ - case 38: /* STATE 11 - line 111 "buffer.spin" - [((prev_off!=write_off))] (3:0:1 - 1) */ + case 38: /* STATE 11 - line 118 "buffer.spin" - [((prev_off!=write_off))] (3:0:1 - 1) */ IfNotBlocked reached[1][11] = 1; if (!((((int)((P1 *)this)->prev_off)!=((int)now.write_off)))) @@ -616,7 +554,7 @@ reached[1][12] = 1; ; _m = 3; goto P999; /* 1 */ - case 39: /* STATE 14 - line 112 "buffer.spin" - [write_off = new_off] (0:24:2 - 1) */ + case 39: /* STATE 14 - line 119 "buffer.spin" - [write_off = new_off] (0:24:2 - 1) */ IfNotBlocked reached[1][14] = 1; (trpt+1)->bup.ovals = grab_ints(2); @@ -641,7 +579,7 @@ reached[1][25] = 1; ; _m = 3; goto P999; /* 3 */ - case 40: /* STATE 17 - line 114 "buffer.spin" - [i = 0] (0:24:1 - 2) */ + case 40: /* STATE 17 - line 121 "buffer.spin" - [i = 0] (0:24:1 - 2) */ IfNotBlocked reached[1][17] = 1; (trpt+1)->bup.oval = ((int)((P1 *)this)->i); @@ -654,7 +592,7 @@ reached[1][25] = 1; ; _m = 3; goto P999; /* 1 */ - case 41: /* STATE 18 - line 116 "buffer.spin" - [((ii)<((int)((P1 *)this)->size)))) @@ -683,7 +621,7 @@ reached[1][25] = 1; ; _m = 3; goto P999; /* 4 */ - case 42: /* STATE 22 - line 120 "buffer.spin" - [((i>=size))] (26:0:1 - 1) */ + case 42: /* STATE 22 - line 127 "buffer.spin" - [((i>=size))] (26:0:1 - 1) */ IfNotBlocked reached[1][22] = 1; if (!((((int)((P1 *)this)->i)>=((int)((P1 *)this)->size)))) @@ -697,7 +635,7 @@ reached[1][23] = 1; ; _m = 3; goto P999; /* 1 */ - case 43: /* STATE 28 - line 127 "buffer.spin" - [i = 0] (0:0:1 - 1) */ + case 43: /* STATE 28 - line 134 "buffer.spin" - [i = 0] (0:0:1 - 1) */ IfNotBlocked reached[1][28] = 1; (trpt+1)->bup.oval = ((int)((P1 *)this)->i); @@ -707,7 +645,7 @@ #endif ; _m = 3; goto P999; /* 0 */ - case 44: /* STATE 29 - line 129 "buffer.spin" - [((ii)<((int)((P1 *)this)->size)))) @@ -733,7 +671,7 @@ reached[1][35] = 1; ; _m = 3; goto P999; /* 3 */ - case 45: /* STATE 32 - line 132 "buffer.spin" - [((i>=size))] (43:0:3 - 1) */ + case 45: /* STATE 32 - line 139 "buffer.spin" - [((i>=size))] (43:0:3 - 1) */ IfNotBlocked reached[1][32] = 1; if (!((((int)((P1 *)this)->i)>=((int)((P1 *)this)->size)))) @@ -764,7 +702,7 @@ #endif ; _m = 3; goto P999; /* 3 */ - case 46: /* STATE 37 - line 134 "buffer.spin" - [tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)] (0:43:2 - 3) */ + case 46: /* STATE 37 - line 141 "buffer.spin" - [tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)] (0:43:2 - 3) */ IfNotBlocked reached[1][37] = 1; (trpt+1)->bup.ovals = grab_ints(2); @@ -783,20 +721,25 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 47: /* STATE 39 - line 137 "buffer.spin" - [(((tmp_commit%(4/2))==0))] (49:0:2 - 1) */ + case 47: /* STATE 39 - line 145 "buffer.spin" - [((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))] (49:0:3 - 1) */ IfNotBlocked reached[1][39] = 1; - if (!(((((int)((P1 *)this)->tmp_commit)%(4/2))==0))) + if (!((((((((int)((P1 *)this)->prev_off)/4)*4)/2)+(4/2))-((int)((P1 *)this)->tmp_commit)))) continue; - /* dead 1: tmp_commit */ (trpt+1)->bup.ovals = grab_ints(2); - (trpt+1)->bup.ovals[0] = ((P1 *)this)->tmp_commit; + /* dead 1: prev_off */ (trpt+1)->bup.ovals = grab_ints(3); + (trpt+1)->bup.ovals[0] = ((P1 *)this)->prev_off; +#ifdef HAS_CODE + if (!readtrail) +#endif + ((P1 *)this)->prev_off = 0; + /* dead 1: tmp_commit */ (trpt+1)->bup.ovals[1] = ((P1 *)this)->tmp_commit; #ifdef HAS_CODE if (!readtrail) #endif ((P1 *)this)->tmp_commit = 0; /* merge: deliver = 1(49, 40, 49) */ reached[1][40] = 1; - (trpt+1)->bup.ovals[1] = ((int)deliver); + (trpt+1)->bup.ovals[2] = ((int)deliver); deliver = 1; #ifdef VAR_RANGES logval("deliver", ((int)deliver)); @@ -806,12 +749,12 @@ reached[1][44] = 1; ; _m = 3; goto P999; /* 2 */ - case 48: /* STATE 44 - line 140 "buffer.spin" - [.(goto)] (0:49:0 - 2) */ + case 48: /* STATE 44 - line 150 "buffer.spin" - [.(goto)] (0:49:0 - 2) */ IfNotBlocked reached[1][44] = 1; ; _m = 3; goto P999; /* 0 */ - case 49: /* STATE 42 - line 138 "buffer.spin" - [(1)] (49:0:0 - 1) */ + case 49: /* STATE 42 - line 148 "buffer.spin" - [(1)] (49:0:0 - 1) */ IfNotBlocked reached[1][42] = 1; if (!(1)) @@ -820,7 +763,7 @@ reached[1][44] = 1; ; _m = 3; goto P999; /* 1 */ - case 50: /* STATE 47 - line 144 "buffer.spin" - [events_lost = (events_lost+1)] (0:0:1 - 2) */ + case 50: /* STATE 47 - line 154 "buffer.spin" - [events_lost = (events_lost+1)] (0:0:1 - 2) */ IfNotBlocked reached[1][47] = 1; (trpt+1)->bup.oval = ((int)now.events_lost); @@ -830,7 +773,7 @@ #endif ; _m = 3; goto P999; /* 0 */ - case 51: /* STATE 48 - line 146 "buffer.spin" - [refcount = (refcount-1)] (0:0:1 - 2) */ + case 51: /* STATE 48 - line 156 "buffer.spin" - [refcount = (refcount-1)] (0:0:1 - 2) */ IfNotBlocked reached[1][48] = 1; (trpt+1)->bup.oval = ((int)now.refcount); @@ -840,14 +783,14 @@ #endif ; _m = 3; goto P999; /* 0 */ - case 52: /* STATE 50 - line 148 "buffer.spin" - [-end-] (0:0:0 - 1) */ + case 52: /* STATE 50 - line 158 "buffer.spin" - [-end-] (0:0:0 - 1) */ IfNotBlocked reached[1][50] = 1; if (!delproc(1, II)) continue; _m = 3; goto P999; /* 0 */ /* PROC switcher */ - case 53: /* STATE 1 - line 56 "buffer.spin" - [prev_off = write_off] (0:9:3 - 1) */ + case 53: /* STATE 1 - line 60 "buffer.spin" - [prev_off = write_off] (0:9:3 - 1) */ IfNotBlocked reached[0][1] = 1; (trpt+1)->bup.ovals = grab_ints(3); @@ -874,7 +817,7 @@ #endif ; _m = 3; goto P999; /* 2 */ - case 54: /* STATE 4 - line 61 "buffer.spin" - [(((((new_off-read_off)>4)&&((new_off-read_off)<(255/2)))||(size==(4/2))))] (29:0:3 - 1) */ + case 54: /* STATE 4 - line 65 "buffer.spin" - [(((((new_off-read_off)>4)&&((new_off-read_off)<(255/2)))||(size==(4/2))))] (29:0:3 - 1) */ IfNotBlocked reached[0][4] = 1; if (!(((((((int)((P0 *)this)->new_off)-((int)now.read_off))>4)&&((((int)((P0 *)this)->new_off)-((int)now.read_off))<(255/2)))||(((int)((P0 *)this)->size)==(4/2))))) @@ -902,7 +845,7 @@ reached[0][6] = 1; ; _m = 3; goto P999; /* 2 */ - case 55: /* STATE 8 - line 64 "buffer.spin" - [(1)] (18:0:0 - 1) */ + case 55: /* STATE 8 - line 68 "buffer.spin" - [(1)] (18:0:0 - 1) */ IfNotBlocked reached[0][8] = 1; if (!(1)) @@ -911,7 +854,7 @@ reached[0][10] = 1; ; _m = 3; goto P999; /* 1 */ - case 56: /* STATE 12 - line 69 "buffer.spin" - [((prev_off!=write_off))] (11:0:1 - 1) */ + case 56: /* STATE 12 - line 73 "buffer.spin" - [((prev_off!=write_off))] (11:0:1 - 1) */ IfNotBlocked reached[0][12] = 1; if (!((((int)((P0 *)this)->prev_off)!=((int)now.write_off)))) @@ -925,12 +868,12 @@ reached[0][13] = 1; ; _m = 3; goto P999; /* 1 */ - case 57: /* STATE 17 - line 72 "buffer.spin" - [.(goto)] (0:28:0 - 1) */ + case 57: /* STATE 17 - line 76 "buffer.spin" - [.(goto)] (0:28:0 - 1) */ IfNotBlocked reached[0][17] = 1; ; _m = 3; goto P999; /* 0 */ - case 58: /* STATE 15 - line 70 "buffer.spin" - [write_off = new_off] (0:28:1 - 1) */ + case 58: /* STATE 15 - line 74 "buffer.spin" - [write_off = new_off] (0:28:1 - 1) */ IfNotBlocked reached[0][15] = 1; (trpt+1)->bup.oval = ((int)now.write_off); @@ -943,7 +886,7 @@ reached[0][17] = 1; ; _m = 3; goto P999; /* 1 */ - case 59: /* STATE 19 - line 75 "buffer.spin" - [tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)] (0:25:2 - 1) */ + case 59: /* STATE 19 - line 79 "buffer.spin" - [tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)] (0:25:2 - 1) */ IfNotBlocked reached[0][19] = 1; (trpt+1)->bup.ovals = grab_ints(2); @@ -962,20 +905,25 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 60: /* STATE 21 - line 78 "buffer.spin" - [(((tmp_commit%(4/2))==0))] (29:0:3 - 1) */ + case 60: /* STATE 21 - line 83 "buffer.spin" - [((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))] (29:0:4 - 1) */ IfNotBlocked reached[0][21] = 1; - if (!(((((int)((P0 *)this)->tmp_commit)%(4/2))==0))) + if (!((((((((int)((P0 *)this)->prev_off)/4)*4)/2)+(4/2))-((int)((P0 *)this)->tmp_commit)))) continue; - /* dead 1: tmp_commit */ (trpt+1)->bup.ovals = grab_ints(3); - (trpt+1)->bup.ovals[0] = ((P0 *)this)->tmp_commit; + /* dead 1: prev_off */ (trpt+1)->bup.ovals = grab_ints(4); + (trpt+1)->bup.ovals[0] = ((P0 *)this)->prev_off; +#ifdef HAS_CODE + if (!readtrail) +#endif + ((P0 *)this)->prev_off = 0; + /* dead 1: tmp_commit */ (trpt+1)->bup.ovals[1] = ((P0 *)this)->tmp_commit; #ifdef HAS_CODE if (!readtrail) #endif ((P0 *)this)->tmp_commit = 0; /* merge: deliver = 1(29, 22, 29) */ reached[0][22] = 1; - (trpt+1)->bup.ovals[1] = ((int)deliver); + (trpt+1)->bup.ovals[2] = ((int)deliver); deliver = 1; #ifdef VAR_RANGES logval("deliver", ((int)deliver)); @@ -986,14 +934,14 @@ ; /* merge: refcount = (refcount-1)(29, 27, 29) */ reached[0][27] = 1; - (trpt+1)->bup.ovals[2] = ((int)now.refcount); + (trpt+1)->bup.ovals[3] = ((int)now.refcount); now.refcount = (((int)now.refcount)-1); #ifdef VAR_RANGES logval("refcount", ((int)now.refcount)); #endif ; _m = 3; goto P999; /* 3 */ - case 61: /* STATE 26 - line 81 "buffer.spin" - [.(goto)] (0:29:1 - 2) */ + case 61: /* STATE 26 - line 88 "buffer.spin" - [.(goto)] (0:29:1 - 2) */ IfNotBlocked reached[0][26] = 1; ; @@ -1006,7 +954,7 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 62: /* STATE 24 - line 79 "buffer.spin" - [(1)] (29:0:1 - 1) */ + case 62: /* STATE 24 - line 86 "buffer.spin" - [(1)] (29:0:1 - 1) */ IfNotBlocked reached[0][24] = 1; if (!(1)) @@ -1023,7 +971,7 @@ #endif ; _m = 3; goto P999; /* 2 */ - case 63: /* STATE 30 - line 85 "buffer.spin" - [-end-] (0:0:0 - 1) */ + case 63: /* STATE 30 - line 92 "buffer.spin" - [-end-] (0:0:0 - 1) */ IfNotBlocked reached[0][30] = 1; if (!delproc(1, II)) continue; diff --git a/trunk/verif/examples/pan.t b/trunk/verif/examples/pan.t index 4dc0dfa0..217eaf43 100644 --- a/trunk/verif/examples/pan.t +++ b/trunk/verif/examples/pan.t @@ -26,123 +26,121 @@ settable(void) /* proctype 4: :init: */ - trans[4] = (Trans **) emalloc(59*sizeof(Trans *)); - - T = trans[ 4][42] = settr(161,2,0,0,0,"ATOMIC", 1, 2, 0); - T->nxt = settr(161,2,1,0,0,"ATOMIC", 1, 2, 0); - trans[4][1] = settr(120,2,8,3,3,"i = 0", 1, 2, 0); - trans[4][9] = settr(128,2,8,1,0,".(goto)", 1, 2, 0); - T = trans[4][8] = settr(127,2,0,0,0,"DO", 1, 2, 0); - T = T->nxt = settr(127,2,2,0,0,"DO", 1, 2, 0); - T->nxt = settr(127,2,6,0,0,"DO", 1, 2, 0); - trans[4][2] = settr(121,2,8,4,4,"((i<2))", 1, 2, 0); /* m: 3 -> 8,0 */ + trans[4] = (Trans **) emalloc(57*sizeof(Trans *)); + + T = trans[ 4][41] = settr(158,2,0,0,0,"ATOMIC", 1, 2, 0); + T->nxt = settr(158,2,1,0,0,"ATOMIC", 1, 2, 0); + trans[4][1] = settr(118,2,7,3,3,"i = 0", 1, 2, 0); + trans[4][8] = settr(125,2,7,1,0,".(goto)", 1, 2, 0); + T = trans[4][7] = settr(124,2,0,0,0,"DO", 1, 2, 0); + T = T->nxt = settr(124,2,2,0,0,"DO", 1, 2, 0); + T->nxt = settr(124,2,5,0,0,"DO", 1, 2, 0); + trans[4][2] = settr(119,2,7,4,4,"((i<2))", 1, 2, 0); /* m: 3 -> 7,0 */ reached4[3] = 1; trans[4][3] = settr(0,0,0,0,0,"commit_count[i] = 0",0,0,0); - trans[4][4] = settr(0,0,0,0,0,"retrieve_count[i] = 0",0,0,0); - trans[4][5] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); - trans[4][6] = settr(125,2,17,5,5,"((i>=2))", 1, 2, 0); /* m: 11 -> 17,0 */ - reached4[11] = 1; - trans[4][7] = settr(126,2,11,1,0,"goto :b6", 1, 2, 0); /* m: 11 -> 0,17 */ - reached4[11] = 1; - trans[4][10] = settr(129,2,11,1,0,"break", 1, 2, 0); - trans[4][11] = settr(130,2,17,6,6,"i = 0", 1, 2, 0); - trans[4][18] = settr(137,2,17,1,0,".(goto)", 1, 2, 0); - T = trans[4][17] = settr(136,2,0,0,0,"DO", 1, 2, 0); - T = T->nxt = settr(136,2,12,0,0,"DO", 1, 2, 0); - T->nxt = settr(136,2,15,0,0,"DO", 1, 2, 0); - trans[4][12] = settr(131,2,17,7,7,"((i<4))", 1, 2, 0); /* m: 13 -> 17,0 */ - reached4[13] = 1; - trans[4][13] = settr(0,0,0,0,0,"buffer_use[i] = 0",0,0,0); - trans[4][14] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); - trans[4][15] = settr(134,2,20,8,8,"((i>=4))", 1, 2, 0); - trans[4][16] = settr(135,2,20,1,0,"goto :b7", 1, 2, 0); - trans[4][19] = settr(138,2,20,1,0,"break", 1, 2, 0); - trans[4][20] = settr(139,2,21,9,9,"(run reader())", 1, 2, 0); - trans[4][21] = settr(140,2,29,10,10,"(run cleaner())", 1, 2, 0); /* m: 22 -> 29,0 */ - reached4[22] = 1; - trans[4][22] = settr(0,0,0,0,0,"i = 0",0,0,0); - trans[4][30] = settr(149,2,29,1,0,".(goto)", 1, 2, 0); - T = trans[4][29] = settr(148,2,0,0,0,"DO", 1, 2, 0); - T = T->nxt = settr(148,2,23,0,0,"DO", 1, 2, 0); - T->nxt = settr(148,2,27,0,0,"DO", 1, 2, 0); - trans[4][23] = settr(142,2,25,11,11,"((i<4))", 1, 2, 0); /* m: 24 -> 25,0 */ - reached4[24] = 1; - trans[4][24] = settr(0,0,0,0,0,"refcount = (refcount+1)",0,0,0); - trans[4][25] = settr(144,2,29,12,12,"(run tracer())", 1, 2, 0); /* m: 26 -> 29,0 */ - reached4[26] = 1; - trans[4][26] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); - trans[4][27] = settr(146,2,39,13,13,"((i>=4))", 1, 2, 0); /* m: 32 -> 39,0 */ - reached4[32] = 1; - trans[4][28] = settr(147,2,32,1,0,"goto :b8", 1, 2, 0); /* m: 32 -> 0,39 */ - reached4[32] = 1; - trans[4][31] = settr(150,2,32,1,0,"break", 1, 2, 0); - trans[4][32] = settr(151,2,39,14,14,"i = 0", 1, 2, 0); - trans[4][40] = settr(159,2,39,1,0,".(goto)", 1, 2, 0); - T = trans[4][39] = settr(158,2,0,0,0,"DO", 1, 2, 0); - T = T->nxt = settr(158,2,33,0,0,"DO", 1, 2, 0); - T->nxt = settr(158,2,37,0,0,"DO", 1, 2, 0); - trans[4][33] = settr(152,2,35,15,15,"((i<1))", 1, 2, 0); /* m: 34 -> 35,0 */ - reached4[34] = 1; - trans[4][34] = settr(0,0,0,0,0,"refcount = (refcount+1)",0,0,0); - trans[4][35] = settr(154,2,39,16,16,"(run switcher())", 1, 2, 0); /* m: 36 -> 39,0 */ - reached4[36] = 1; - trans[4][36] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); - trans[4][37] = settr(156,2,41,17,17,"((i>=1))", 1, 2, 0); /* m: 38 -> 41,0 */ - reached4[38] = 1; - trans[4][38] = settr(157,2,41,1,0,"goto :b9", 1, 2, 0); - trans[4][41] = settr(160,0,57,1,0,"break", 1, 2, 0); - T = trans[ 4][57] = settr(176,2,0,0,0,"ATOMIC", 1, 2, 0); - T->nxt = settr(176,2,43,0,0,"ATOMIC", 1, 2, 0); - trans[4][43] = settr(162,2,52,18,18,"assert((((write_off-read_off)>=0)&&((write_off-read_off)<(255/2))))", 1, 2, 0); /* m: 44 -> 0,52 */ - reached4[44] = 1; - trans[4][44] = settr(0,0,0,0,0,"j = 0",0,0,0); - trans[4][45] = settr(0,0,0,0,0,"commit_sum = 0",0,0,0); - trans[4][53] = settr(172,2,52,1,0,".(goto)", 1, 2, 0); - T = trans[4][52] = settr(171,2,0,0,0,"DO", 1, 2, 0); - T = T->nxt = settr(171,2,46,0,0,"DO", 1, 2, 0); - T->nxt = settr(171,2,50,0,0,"DO", 1, 2, 0); - trans[4][46] = settr(165,2,52,19,19,"((j<2))", 1, 2, 0); /* m: 47 -> 52,0 */ - reached4[47] = 1; - trans[4][47] = settr(0,0,0,0,0,"commit_sum = (commit_sum+commit_count[j])",0,0,0); - trans[4][48] = settr(0,0,0,0,0,"assert((((commit_count[j]-retrieve_count[j])>=0)&&((commit_count[j]-retrieve_count[j])<(255/2))))",0,0,0); - trans[4][49] = settr(0,0,0,0,0,"j = (j+1)",0,0,0); - trans[4][50] = settr(169,4,58,20,20,"((j>=2))", 1, 2, 0); /* m: 55 -> 58,0 */ - reached4[55] = 1; - trans[4][51] = settr(170,2,55,1,0,"goto :b10", 1, 2, 0); /* m: 55 -> 0,58 */ - reached4[55] = 1; - trans[4][54] = settr(173,2,55,1,0,"break", 1, 2, 0); - trans[4][55] = settr(174,4,58,21,21,"assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))", 1, 2, 0); /* m: 56 -> 0,58 */ - reached4[56] = 1; - trans[4][56] = settr(0,0,0,0,0,"assert((((4+1)>4)||(events_lost==0)))",0,0,0); - trans[4][58] = settr(177,0,0,22,22,"-end-", 0, 3500, 0); + trans[4][4] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); + trans[4][5] = settr(122,2,16,5,5,"((i>=2))", 1, 2, 0); /* m: 10 -> 16,0 */ + reached4[10] = 1; + trans[4][6] = settr(123,2,10,1,0,"goto :b6", 1, 2, 0); /* m: 10 -> 0,16 */ + reached4[10] = 1; + trans[4][9] = settr(126,2,10,1,0,"break", 1, 2, 0); + trans[4][10] = settr(127,2,16,6,6,"i = 0", 1, 2, 0); + trans[4][17] = settr(134,2,16,1,0,".(goto)", 1, 2, 0); + T = trans[4][16] = settr(133,2,0,0,0,"DO", 1, 2, 0); + T = T->nxt = settr(133,2,11,0,0,"DO", 1, 2, 0); + T->nxt = settr(133,2,14,0,0,"DO", 1, 2, 0); + trans[4][11] = settr(128,2,16,7,7,"((i<4))", 1, 2, 0); /* m: 12 -> 16,0 */ + reached4[12] = 1; + trans[4][12] = settr(0,0,0,0,0,"buffer_use[i] = 0",0,0,0); + trans[4][13] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); + trans[4][14] = settr(131,2,19,8,8,"((i>=4))", 1, 2, 0); + trans[4][15] = settr(132,2,19,1,0,"goto :b7", 1, 2, 0); + trans[4][18] = settr(135,2,19,1,0,"break", 1, 2, 0); + trans[4][19] = settr(136,2,20,9,9,"(run reader())", 1, 2, 0); + trans[4][20] = settr(137,2,28,10,10,"(run cleaner())", 1, 2, 0); /* m: 21 -> 28,0 */ + reached4[21] = 1; + trans[4][21] = settr(0,0,0,0,0,"i = 0",0,0,0); + trans[4][29] = settr(146,2,28,1,0,".(goto)", 1, 2, 0); + T = trans[4][28] = settr(145,2,0,0,0,"DO", 1, 2, 0); + T = T->nxt = settr(145,2,22,0,0,"DO", 1, 2, 0); + T->nxt = settr(145,2,26,0,0,"DO", 1, 2, 0); + trans[4][22] = settr(139,2,24,11,11,"((i<4))", 1, 2, 0); /* m: 23 -> 24,0 */ + reached4[23] = 1; + trans[4][23] = settr(0,0,0,0,0,"refcount = (refcount+1)",0,0,0); + trans[4][24] = settr(141,2,28,12,12,"(run tracer())", 1, 2, 0); /* m: 25 -> 28,0 */ + reached4[25] = 1; + trans[4][25] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); + trans[4][26] = settr(143,2,38,13,13,"((i>=4))", 1, 2, 0); /* m: 31 -> 38,0 */ + reached4[31] = 1; + trans[4][27] = settr(144,2,31,1,0,"goto :b8", 1, 2, 0); /* m: 31 -> 0,38 */ + reached4[31] = 1; + trans[4][30] = settr(147,2,31,1,0,"break", 1, 2, 0); + trans[4][31] = settr(148,2,38,14,14,"i = 0", 1, 2, 0); + trans[4][39] = settr(156,2,38,1,0,".(goto)", 1, 2, 0); + T = trans[4][38] = settr(155,2,0,0,0,"DO", 1, 2, 0); + T = T->nxt = settr(155,2,32,0,0,"DO", 1, 2, 0); + T->nxt = settr(155,2,36,0,0,"DO", 1, 2, 0); + trans[4][32] = settr(149,2,34,15,15,"((i<1))", 1, 2, 0); /* m: 33 -> 34,0 */ + reached4[33] = 1; + trans[4][33] = settr(0,0,0,0,0,"refcount = (refcount+1)",0,0,0); + trans[4][34] = settr(151,2,38,16,16,"(run switcher())", 1, 2, 0); /* m: 35 -> 38,0 */ + reached4[35] = 1; + trans[4][35] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); + trans[4][36] = settr(153,2,40,17,17,"((i>=1))", 1, 2, 0); /* m: 37 -> 40,0 */ + reached4[37] = 1; + trans[4][37] = settr(154,2,40,1,0,"goto :b9", 1, 2, 0); + trans[4][40] = settr(157,0,55,1,0,"break", 1, 2, 0); + T = trans[ 4][55] = settr(172,2,0,0,0,"ATOMIC", 1, 2, 0); + T->nxt = settr(172,2,42,0,0,"ATOMIC", 1, 2, 0); + trans[4][42] = settr(159,2,50,18,18,"assert((((write_off-read_off)>=0)&&((write_off-read_off)<(255/2))))", 1, 2, 0); /* m: 43 -> 0,50 */ + reached4[43] = 1; + trans[4][43] = settr(0,0,0,0,0,"j = 0",0,0,0); + trans[4][44] = settr(0,0,0,0,0,"commit_sum = 0",0,0,0); + trans[4][51] = settr(168,2,50,1,0,".(goto)", 1, 2, 0); + T = trans[4][50] = settr(167,2,0,0,0,"DO", 1, 2, 0); + T = T->nxt = settr(167,2,45,0,0,"DO", 1, 2, 0); + T->nxt = settr(167,2,48,0,0,"DO", 1, 2, 0); + trans[4][45] = settr(162,2,50,19,19,"((j<2))", 1, 2, 0); /* m: 46 -> 50,0 */ + reached4[46] = 1; + trans[4][46] = settr(0,0,0,0,0,"commit_sum = (commit_sum+commit_count[j])",0,0,0); + trans[4][47] = settr(0,0,0,0,0,"j = (j+1)",0,0,0); + trans[4][48] = settr(165,4,56,20,20,"((j>=2))", 1, 2, 0); /* m: 53 -> 56,0 */ + reached4[53] = 1; + trans[4][49] = settr(166,2,53,1,0,"goto :b10", 1, 2, 0); /* m: 53 -> 0,56 */ + reached4[53] = 1; + trans[4][52] = settr(169,2,53,1,0,"break", 1, 2, 0); + trans[4][53] = settr(170,4,56,21,21,"assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))", 1, 2, 0); /* m: 54 -> 0,56 */ + reached4[54] = 1; + trans[4][54] = settr(0,0,0,0,0,"assert((((4+1)>4)||(events_lost==0)))",0,0,0); + trans[4][56] = settr(173,0,0,22,22,"-end-", 0, 3500, 0); /* proctype 3: cleaner */ trans[3] = (Trans **) emalloc(10*sizeof(Trans *)); - T = trans[ 3][8] = settr(118,2,0,0,0,"ATOMIC", 1, 2, 0); - T->nxt = settr(118,2,5,0,0,"ATOMIC", 1, 2, 0); - trans[3][6] = settr(116,2,5,1,0,".(goto)", 1, 2, 0); - T = trans[3][5] = settr(115,2,0,0,0,"DO", 1, 2, 0); - T->nxt = settr(115,2,1,0,0,"DO", 1, 2, 0); - trans[3][1] = settr(111,2,3,23,23,"((refcount==0))", 1, 2, 0); /* m: 2 -> 3,0 */ + T = trans[ 3][8] = settr(116,2,0,0,0,"ATOMIC", 1, 2, 0); + T->nxt = settr(116,2,5,0,0,"ATOMIC", 1, 2, 0); + trans[3][6] = settr(114,2,5,1,0,".(goto)", 1, 2, 0); + T = trans[3][5] = settr(113,2,0,0,0,"DO", 1, 2, 0); + T->nxt = settr(113,2,1,0,0,"DO", 1, 2, 0); + trans[3][1] = settr(109,2,3,23,23,"((refcount==0))", 1, 2, 0); /* m: 2 -> 3,0 */ reached3[2] = 1; trans[3][2] = settr(0,0,0,0,0,"refcount = (refcount+1)",0,0,0); - trans[3][3] = settr(113,2,7,24,24,"(run switcher())", 1, 2, 0); /* m: 4 -> 7,0 */ + trans[3][3] = settr(111,2,7,24,24,"(run switcher())", 1, 2, 0); /* m: 4 -> 7,0 */ reached3[4] = 1; - trans[3][4] = settr(114,2,7,1,0,"goto :b5", 1, 2, 0); - trans[3][7] = settr(117,0,9,1,0,"break", 1, 2, 0); - trans[3][9] = settr(119,0,0,25,25,"-end-", 0, 3500, 0); + trans[3][4] = settr(112,2,7,1,0,"goto :b5", 1, 2, 0); + trans[3][7] = settr(115,0,9,1,0,"break", 1, 2, 0); + trans[3][9] = settr(117,0,0,25,25,"-end-", 0, 3500, 0); /* proctype 2: reader */ - trans[2] = (Trans **) emalloc(32*sizeof(Trans *)); + trans[2] = (Trans **) emalloc(30*sizeof(Trans *)); - trans[2][29] = settr(108,0,28,1,0,".(goto)", 0, 2, 0); - T = trans[2][28] = settr(107,0,0,0,0,"DO", 0, 2, 0); - T = T->nxt = settr(107,0,1,0,0,"DO", 0, 2, 0); - T->nxt = settr(107,0,26,0,0,"DO", 0, 2, 0); - trans[2][1] = settr(80,0,12,26,0,"((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&((commit_count[((read_off%4)/(4/2))]-retrieve_count[((read_off%4)/(4/2))])==(4/2))))", 1, 2, 0); + trans[2][27] = settr(106,0,26,1,0,".(goto)", 0, 2, 0); + T = trans[2][26] = settr(105,0,0,0,0,"DO", 0, 2, 0); + T = T->nxt = settr(105,0,1,0,0,"DO", 0, 2, 0); + T->nxt = settr(105,0,24,0,0,"DO", 0, 2, 0); + trans[2][1] = settr(80,0,12,26,0,"((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&(((commit_count[((read_off%4)/(4/2))]-(4/2))-(((read_off/4)*4)/2))==0)))", 1, 2, 0); T = trans[ 2][12] = settr(91,2,0,0,0,"ATOMIC", 1, 2, 0); T->nxt = settr(91,2,2,0,0,"ATOMIC", 1, 2, 0); trans[2][2] = settr(81,2,9,27,27,"i = 0", 1, 2, 0); @@ -158,9 +156,9 @@ settable(void) trans[2][7] = settr(86,2,11,29,29,"((i>=(4/2)))", 1, 2, 0); /* m: 8 -> 11,0 */ reached2[8] = 1; trans[2][8] = settr(87,2,11,1,0,"goto :b3", 1, 2, 0); - trans[2][11] = settr(90,0,25,1,0,"break", 1, 2, 0); - T = trans[ 2][25] = settr(104,2,0,0,0,"ATOMIC", 1, 2, 0); - T->nxt = settr(104,2,13,0,0,"ATOMIC", 1, 2, 0); + trans[2][11] = settr(90,0,23,1,0,"break", 1, 2, 0); + T = trans[ 2][23] = settr(102,2,0,0,0,"ATOMIC", 1, 2, 0); + T->nxt = settr(102,2,13,0,0,"ATOMIC", 1, 2, 0); trans[2][13] = /* c */ settr(92,2,19,27,27,"i = 0", 1, 2, 0); trans[2][20] = settr(99,2,19,1,0,".(goto)", 1, 2, 0); T = trans[2][19] = settr(98,2,0,0,0,"DO", 1, 2, 0); @@ -170,19 +168,14 @@ settable(void) reached2[15] = 1; trans[2][15] = settr(0,0,0,0,0,"buffer_use[((read_off+i)%4)] = 0",0,0,0); trans[2][16] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); - trans[2][17] = settr(96,0,28,31,31,"((i>=(4/2)))", 1, 2, 0); /* m: 22 -> 28,0 */ - reached2[22] = 1; - trans[2][18] = settr(97,2,22,1,0,"goto :b4", 1, 2, 0); /* m: 22 -> 0,28 */ - reached2[22] = 1; + trans[2][17] = settr(96,2,21,31,31,"((i>=(4/2)))", 1, 2, 0); + trans[2][18] = settr(97,2,21,1,0,"goto :b4", 1, 2, 0); trans[2][21] = settr(100,2,22,1,0,"break", 1, 2, 0); - trans[2][22] = settr(101,0,28,32,32,"tmp_retrieve = (retrieve_count[((read_off%4)/(4/2))]+(4/2))", 1, 2, 0); /* m: 23 -> 0,28 */ - reached2[23] = 1; - trans[2][23] = settr(0,0,0,0,0,"retrieve_count[((read_off%4)/(4/2))] = tmp_retrieve",0,0,0); - trans[2][24] = settr(0,0,0,0,0,"read_off = (read_off+(4/2))",0,0,0); - trans[2][26] = settr(105,0,31,33,0,"((read_off>=(4-events_lost)))", 1, 2, 0); - trans[2][27] = settr(106,0,31,1,0,"goto :b2", 0, 2, 0); - trans[2][30] = settr(109,0,31,1,0,"break", 0, 2, 0); - trans[2][31] = settr(110,0,0,34,34,"-end-", 0, 3500, 0); + trans[2][22] = settr(101,0,26,32,32,"read_off = (read_off+(4/2))", 1, 2, 0); + trans[2][24] = settr(103,0,29,33,0,"((read_off>=(4-events_lost)))", 1, 2, 0); + trans[2][25] = settr(104,0,29,1,0,"goto :b2", 0, 2, 0); + trans[2][28] = settr(107,0,29,1,0,"break", 0, 2, 0); + trans[2][29] = settr(108,0,0,34,34,"-end-", 0, 3500, 0); /* proctype 1: tracer */ @@ -253,7 +246,7 @@ settable(void) T = trans[1][43] = settr(72,2,0,0,0,"IF", 1, 2, 0); T = T->nxt = settr(72,2,39,0,0,"IF", 1, 2, 0); T->nxt = settr(72,2,41,0,0,"IF", 1, 2, 0); - trans[1][39] = settr(68,4,49,47,47,"(((tmp_commit%(4/2))==0))", 1, 2, 0); /* m: 40 -> 49,0 */ + trans[1][39] = settr(68,4,49,47,47,"((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))", 1, 2, 0); /* m: 40 -> 49,0 */ reached1[40] = 1; trans[1][40] = settr(0,0,0,0,0,"deliver = 1",0,0,0); trans[1][44] = settr(73,0,49,48,48,".(goto)", 1, 2, 0); @@ -308,7 +301,7 @@ settable(void) T = trans[0][25] = settr(24,2,0,0,0,"IF", 1, 2, 0); T = T->nxt = settr(24,2,21,0,0,"IF", 1, 2, 0); T->nxt = settr(24,2,23,0,0,"IF", 1, 2, 0); - trans[0][21] = settr(20,4,29,60,60,"(((tmp_commit%(4/2))==0))", 1, 2, 0); /* m: 22 -> 29,0 */ + trans[0][21] = settr(20,4,29,60,60,"((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))", 1, 2, 0); /* m: 22 -> 29,0 */ reached0[22] = 1; trans[0][22] = settr(0,0,0,0,0,"deliver = 1",0,0,0); trans[0][26] = settr(25,4,29,61,61,".(goto)", 1, 2, 0); /* m: 27 -> 0,29 */ diff --git a/trunk/verif/examples/run b/trunk/verif/examples/run index 5a47e644..8a2cf840 100755 --- a/trunk/verif/examples/run +++ b/trunk/verif/examples/run @@ -1,5 +1,8 @@ #!/bin/bash +#avail. mem +MEM=15360 + ../Spin/Src5.1.6/spin -a buffer.spin -cc -DSAFETY -o pan pan.c +cc -DMEMLIM=${MEM} -DSAFETY -o pan pan.c ./pan diff --git a/trunk/verif/examples/run3 b/trunk/verif/examples/run3 index 69ac0915..2dcc2cc6 100755 --- a/trunk/verif/examples/run3 +++ b/trunk/verif/examples/run3 @@ -1,5 +1,8 @@ #!/bin/bash +#avail. mem +MEM=15360 + ../Spin/Src5.1.6/spin -a buffer.spin -cc -o pan pan.c +cc -DMEMLIM=${MEM} -o pan pan.c ./pan -- 2.34.1