From 6c55a8400b4737632f063515e70ac89722326f68 Mon Sep 17 00:00:00 2001 From: Jake Ginesin Date: Thu, 12 Mar 2026 02:40:33 -0400 Subject: [PATCH] tcp --- ._n_i_p_s_ | 21 +++ .../model_generate.cpython-313.pyc | Bin 17683 -> 17683 bytes src/model_generate.py | 1 - tests/abp/abp.pml | 59 +++++++ tests/paper.yaml | 154 ++++++++++++++++ tests/tcp/pan | Bin 0 -> 114744 bytes tests/tcp/props/phi1.pml | 4 + tests/tcp/props/phi2.pml | 5 + tests/tcp/props/phi3.pml | 22 +++ tests/tcp/props/phi4.pml | 11 ++ tests/tcp/props/phi5.pml | 13 ++ tests/tcp/props/phi6.pml | 9 + tests/tcp/tcp-phi1.pml | 149 ++++++++++++++++ tests/tcp/tcp-phi2.pml | 149 ++++++++++++++++ tests/tcp/tcp-phi2.pml.trail | 55 ++++++ tests/tcp/tcp-phi3.pml | 167 ++++++++++++++++++ tests/tcp/tcp-phi4.pml | 156 ++++++++++++++++ tests/tcp/tcp-phi4.pml.trail | 43 +++++ tests/tcp/tcp-phi5.pml | 158 +++++++++++++++++ tests/tcp/tcp-phi6.pml | 154 ++++++++++++++++ tests/tcp/tcp.pml | 144 +++++++++++++++ 21 files changed, 1473 insertions(+), 1 deletion(-) create mode 100644 ._n_i_p_s_ create mode 100644 tests/abp/abp.pml create mode 100644 tests/paper.yaml create mode 100755 tests/tcp/pan create mode 100644 tests/tcp/props/phi1.pml create mode 100644 tests/tcp/props/phi2.pml create mode 100644 tests/tcp/props/phi3.pml create mode 100644 tests/tcp/props/phi4.pml create mode 100644 tests/tcp/props/phi5.pml create mode 100644 tests/tcp/props/phi6.pml create mode 100644 tests/tcp/tcp-phi1.pml create mode 100644 tests/tcp/tcp-phi2.pml create mode 100644 tests/tcp/tcp-phi2.pml.trail create mode 100644 tests/tcp/tcp-phi3.pml create mode 100644 tests/tcp/tcp-phi4.pml create mode 100644 tests/tcp/tcp-phi4.pml.trail create mode 100644 tests/tcp/tcp-phi5.pml create mode 100644 tests/tcp/tcp-phi6.pml create mode 100644 tests/tcp/tcp.pml diff --git a/._n_i_p_s_ b/._n_i_p_s_ new file mode 100644 index 0000000..ea80a74 --- /dev/null +++ b/._n_i_p_s_ @@ -0,0 +1,21 @@ +ltl phi3 { + !(eventually (((always (state[0] == 2)) || + (always (state[0] == 3)) || + (always (state[0] == 4)) || + (always (state[0] == 5)) || + (always (state[0] == 6)) || + (always (state[0] == 7)) || + (always (state[0] == 8)) || + (always (state[0] == 9)) || + (always (state[0] == 10))) + && + ((always (state[1] == 2)) || + (always (state[1] == 3)) || + (always (state[1] == 4)) || + (always (state[1] == 5)) || + (always (state[1] == 6)) || + (always (state[1] == 7)) || + (always (state[1] == 8)) || + (always (state[1] == 9)) || + (always (state[1] == 10))))) +} diff --git a/src/__pycache__/model_generate.cpython-313.pyc b/src/__pycache__/model_generate.cpython-313.pyc index 58b0958ca01941c415c8efb67cd4ab8556d595c0..7ed32cee091116c66de5b9222b6d959b3ee2ebc8 100644 GIT binary patch delta 72 zcmbQ-#W=Z(k@qt%FBbz4uvu=(wBN|PL7h=<^FDP`ZuWRa28QB|%#%OzNKQT{<+VB1 c_z64Xyv9CP^gF2)9=6&j>-0TUA3=G8^nJ0hbk(_)^%4>71 c@e_8&`J0`r_1G9sZ!UEF!NeFeIm=}w057~3-~a#s diff --git a/src/model_generate.py b/src/model_generate.py index 4729af0..b8cf2ff 100644 --- a/src/model_generate.py +++ b/src/model_generate.py @@ -283,7 +283,6 @@ def gen_replay_unbounded(chan : str, chan_type : List[str], mem : int, index : i # return ret_string - def gen_reorder(chan : str, chan_type : List[str], mem : int, index : int) -> str: ret_string = "" diff --git a/tests/abp/abp.pml b/tests/abp/abp.pml new file mode 100644 index 0000000..02f6562 --- /dev/null +++ b/tests/abp/abp.pml @@ -0,0 +1,59 @@ +mtype = { DATA0, DATA1, ACK0, ACK1 } + +chan AtoB = [1] of { mtype } +chan BtoA = [1] of { mtype } + +mtype ackA, ackB; +byte seqA = 0; +byte seqB = 0; + +mtype packetA, packetB; + +active proctype A() +{ + do + :: + if + :: seqA == 0 -> packetA = DATA0 + :: else -> packetA = DATA1 + fi; + AtoB!packetA; + do + :: BtoA?ackA -> + if + :: (seqA == 0 && ackA == ACK0) || (seqA == 1 && ackA == ACK1) -> + seqA = 1 - seqA; + break + :: else -> skip; + fi + :: + AtoB!packetA + od + od +} + +active proctype B() +{ + do + :: AtoB?packetB -> + if + :: (seqB == 0 && packetB == DATA0) || (seqB == 1 && packetB == DATA1) -> + if + :: seqB == 0 -> ackB = ACK0 + :: else -> ackB = ACK1 + fi; + BtoA!ackB; + seqB = 1 - seqB; + :: else -> + if + :: seqB == 0 -> ackB = ACK1 + :: else -> ackB = ACK0 + fi; + BtoA!ackB; + fi + od +} + +ltl liveness { + always ((packetA != packetB) implies eventually (packetA == packetB)) +} diff --git a/tests/paper.yaml b/tests/paper.yaml new file mode 100644 index 0000000..e37883d --- /dev/null +++ b/tests/paper.yaml @@ -0,0 +1,154 @@ +unidirectional-drop-abp: + - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol + +bidirectional-drop-abp: + - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol + +tcp-phi1-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping A's outbound messages alone is insufficient to create a half-open state; B cannot reach Established without receiving from A + +tcp-phi1-drop-BtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping B's outbound messages prevents B from progressing; A times out back to Closed, no half-open + +tcp-phi1-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping on both directions prevents any handshake progress; neither side reaches Established + +tcp-phi1-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replaying A's SYN can drive B into Established via a forged handshake while A returns to Closed, creating a half-open state + +tcp-phi1-replay-BtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replaying B's SYN+ACK can cause A to believe handshake completed; if A then closes, B may remain Established + +tcp-phi1-replay-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replaying on both channels gives the attacker maximum ability to manufacture a half-open state + +tcp-phi1-reorder-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: property violation + - explanation: reordering A's messages (e.g., delivering ACK before SYN) can desynchronize the handshake, leading to half-open + +tcp-phi1-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: property violation + - explanation: reordering on both channels maximizes desynchronization potential for half-open + +tcp-phi2-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping A's SYN prevents the handshake from completing, violating the liveness property that A should eventually reach Established + +tcp-phi2-drop-BtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=drop --chan=BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping B's SYN+ACK response prevents A from ever completing the handshake + +tcp-phi2-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping on both channels trivially prevents connection establishment + +tcp-phi2-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying A's messages does not prevent establishment; extra SYNs are handled by B's wildcard receives + +tcp-phi2-reorder-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: acceptance cycle + - explanation: reordering A's handshake messages can prevent B from following the correct SYN/ACK sequence, stalling establishment + +tcp-phi3-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping A's messages can cause B to stall indefinitely in SynReceived or similar waiting states + +tcp-phi3-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping on both channels can strand both sides in intermediate states with no timeout recovery + +tcp-phi3-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: replaying stale messages can trap B in a loop re-processing old handshake messages + +tcp-phi3-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: acceptance cycle + - explanation: reordering on both channels can desynchronize both sides into permanently mismatched states + +tcp-phi4-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: during simultaneous open, dropping A's SYN prevents B from advancing, breaking the simultaneous open guarantee + +tcp-phi4-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping both sides' SYNs trivially prevents simultaneous open from resolving + +tcp-phi4-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying SYN messages during simultaneous open should not prevent eventual establishment; the protocol handles duplicate SYNs + +tcp-phi4-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: acceptance cycle + - explanation: reordering handshake messages during simultaneous open can prevent the SYN+ACK exchange from completing correctly + +tcp-phi5-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: if A's ACK is dropped, B remains stuck in SynReceived with no timeout to recover + +tcp-phi5-drop-BtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping B's SYN+ACK means A never sends ACK, leaving the initiator-side SynReceived unresolved + +tcp-phi5-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying A's messages provides additional ACKs that can help resolve SynReceived + +tcp-phi5-reorder-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: acceptance cycle + - explanation: reordering can deliver A's SYN after the ACK, confusing B's state machine and trapping it in SynReceived + +tcp-phi6-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping A's messages while in Closing does not cause A to transition to an unexpected state; A remains in Closing or eventually times out + +tcp-phi6-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replaying a FIN while in Closing could cause a transition to TimeWait instead of the expected Closing or Closed + +tcp-phi6-replay-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replaying on both channels maximizes the chance of injecting an unexpected ACK that transitions Closing to TimeWait, violating the next-state constraint + +tcp-phi6-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: property violation + - explanation: reordering close-sequence messages can cause ACK delivery at unexpected times, violating the strict Closing transition property diff --git a/tests/tcp/pan b/tests/tcp/pan new file mode 100755 index 0000000000000000000000000000000000000000..7f43cf263f13847cb8ce3081baea76e0eb9e619d GIT binary patch literal 114744 zcmcG%3wRVo7B<|I%s_y|4vts*9_JBw{)jNB{)`C?X03r}m`PMtbcb-KE`dif~Foe?IJ5cow1w+j?n7n{jQ{3r;;>w{@Bg><2-kSX*Nt`j;T zl^K75beY;!;G7zPNc;llC>|6daVFe+Eq;DPCPEa>q?3@xj=^&vcRE|NIDX31Li`*% zk*5rt1;NVViAu7b)Z$N0oXY5dvsGk4VeJZj4&X>U!U>az1D!c8a6YM#1Lr{bsBH9C ztCg=dA`>ABXW|&(9z0W8`sE#QPN(bE+d1Rb+wF`VIBy`u;TJduaQ6Yn8%($g^`oh`8sSi(^I(XLf zTOWV?vEoHThfXV=`{zb^Q*;_rX?1?-%3cY^`YS-UpY z_Z5ctu7+#6BpV@}kcnT3zrgQmTy)1@H~jU{h>19BCdMd)qr9m+EI+z1#YPZ~^p(=* z*=sURyGc#${t7`Qy@&rE1ff0pZ5_}lZF}ke*a3ZN2lQPX(BJBS{!IsT>N4AtCtzoQ zh5WJ*YA=0J2lTf)p#Rtb{gw{st`6u&JD`v0fKCR`p8OwyZUrX%Hy4EV(!bUL{XZSh z$u`^LGqeMGO9%8J9nkOYfF9LBdHo%vujqhI{Y!iDQy;Y?wnb3wuU$AuZivz)@h`3q*v zbruSfbMBoyzsOl2EL<>k?sTDW-uxMJDdF6LN9WUdLBY%g!u%Nv7R*~9ES&Z5+^KVT zEcgJnkPZbiry|a|z&US@@aT+37tR28=K}nv5N9)eUXfFnJbBi_c?B66lM5FXOr2ZE zV!@`cV9vaSGlWN{&Y3e0VnD{Jl(xY6`1~1@r%mR>>5xDuT)beGa|TNSp`5cGow1Mw zAnD}ERNBc4ol_S$CqFuM)?8sxp;p3$k1s5khwSchLs{c@OoHE7@v z;s5_oH{1vvI&1E%CuR+qI&;qBGaoB1Uc4x6!J@gTL#7TIGOJ+fg2x6tTu?Az*uYx{ zrebu&AUSIqit+HH^X6*Bm`t@Bq5X^0uL6|NGo>{DW*Q5NrSZVb#)N<$(R0=;3~?4A z7VU;;FZ}V(7%t30Z!O%5#YYPLwQy1ISr`f;kUrHwzurKXTt7rfZp$0@B??km ztuw;kEV(vDH3D67Cud3 zY8u`W7Cug4Y7*Z0EPRN<)D*l^Sa>gmsR?-VSa>Ie$@IOMEWDM%Wb)or7Otl-nY!1? z!qpTe6Zgil@P8>xrtKA2_#Fz9NqbLTqVoTP!d42mu<*+iCKL8Hv+(m2Ce!uSvhXt$ zCX@B9Lpbfn9C^niNj@aG4xh{$m(x_+e1%<*n(C&oQ&ViDUGT?Wd2gcdvv_T`AdIh! zg-0XV*ik;>>{SU)%tT`*Dn#_Ruyhj}3fZ}aXyc_7Cp3UmcR5m$PfB&_9g?Y0+Hu(# zuXE@YX7%G_is4KZ8@IP&iP$wv+@xR`QXFKG`mx zw!02R+T~OBx?dtjm2FvekKJSUJ3QGd&650!SYbESwM2;(-A&D=lVZhVk#$EAx-Y`C zyY6T=`E*)+T}!Oon6_JT)tTj!b!stB;b6T@pUw6E_sh&bt@lYpIvs^35mT&43g$A*rmua_H@qnrB zP!z|+iWQ3^>W=nEgB0@ax)a?@yM6x@D>{>$i%pQz)Ch@Mx~0)c?QUxHm9bd4vF>PB zBJNO4jo!J?RJP~N&SmGa#hgZaU29}+K`j8S*Vd_hJaL^|hdQS;d-9?j1zU5dOs>{W zi$~?SYE4o>qhxAzUFf`csJzpk^py%bXhaQrGELe^^5pT$k*3B7L>NOzB34*dqJrG! zGV2UjN_EdAqnB4bKJ4!~uGR?g>0hBDDe|r;De{3>hbJ!9A#af)MMuhx99+mdq&n|S zjlu{2;PMtT(k%mB>WI$ct7S+pu+9ApH5~`&w zuwPqXT3cW@18@fMjbQUQMEFmFhR0l{uDeV+AE6L!so#&M% zrJbgXQ47e30lR5H%8v4m)=(%jc)?r^5UNF#ezW9`vAmA)3kedzW=QjF1QL;XObuPh zmal8*6rZ{R4FO8?zKsrv&i}#rOauQ1bDFs^QOIZ&|6VIr)Hb;85X2YQRa0jg@z%5v9H*LKtS-DSIrvRsEQ%RP~zIhcZa>RpYA zr$I-)6DBq^jRFRy?~Z?mrRoYk)r`-fEj5Ayq>h0 zo!?Db%g!Gqtz+j6NwqjPWhX_^;Ei*1D$bIpG^vHoU>+-ZvXiWIl^}V>B}GZ{Wyx(D zet)8%j{3##XPTE*Y$VbCUyA6m-H$AVqL|PO<;(w{WOv(EjECUQw)*|P3i|{0`|acH zxWFEsB%eqzl)^_bAG>Ffv$v{rbf!e{wW2#bacpvyr}@Y zHlhFBgdWc@9kq$nGUcQ53ONI=@pY_))4m0`?#80ec2IfBO9#8T}Yb7|R$s z&>wiRyZ*|{E%Kg=*r*Rd04h{0LNlGdQ4-6RXa$jV?~CnUK^%|Gk+ixpX>5lh9=Lud%4;IJ2G zXi0L_o5YHU5lfxs(%Pa^NKrNuF>D+fY2rrf?sJ!f_D-4`12uCkZ$PTt0)I~3v2OOp zl?N72C6&%eO7Ny2LhBC-Snuq%w7dkk+uSO-Z$2rN{aAFb)`pdyC>pD2H69{Lt_G9S zDpuT4fj6r!)#z|*?mX?v9 zsY7}V<~rCp8}80Ns2aUu1Iyq{18XlUe!wh)P-1&(44g2rl;#;Fcb^!9YG}?BHmD|` zP@me7ib`XaJo%`Y{SvHq`5C{z#Fm4!aOm7IGjZXun`FymT$F7QpL>%riAiG#bcPyIh4X3pT?;k*PxGnW$WRS97sFZg@8t-@{sTs)B zaZLRN$Q*eiDPt1+qY|4$*%!sQEf3?uBl*j=ET4(t<1vk4Sg|iaB737bX&}aqD@KKt z{ZT3%m0c$1f|or_FZ(>?tVjr|MM&p8OKr$)>C(R7&m)QN&(Mb*Hwd~u98~N&UYBAS z-LYu;`0$h#;k}iJG}ul#fNstQ0EYITE1(@3aw+Dt7;7o0PZX3qjI68!P`?Bm4_#`v4tThbv!h4TAWm;6zhn80O7JtfN+BIYl5D_ypK=7@L&1K&fb%Nlj6B<+zmEb!wR=()6z0ZjgvsfBOM6u#aS4-zAas}Yxxrh7=ODm7Q67-*8nvF;b!~qb+3UjJyvsBP5W$akk zm;53S8?(FnO*Bq|?2cJOsWY}NJ_N|S8bmU|ag14p7>DQPp@{e=A`0c``MCw>9B^nO zUdm{e#F6!~ z#Y};MhCNr#f`<_r^xjP~U?9WaVazte*`pqWlZc&mNXi!l5|AaO#D&yf# zJw*{{5&!)U>Jtu?zwF0s@!po~@_$f->moYQ-QY$St9r4E2(fetyNE2xU`)h{r>Jvw zwY0i6N0zf|&_@X?))EVU=T_VlKM!}+1i^QGj3Q;4Ob*$Wi5xwn&^9+F82lA(E8Ls* zeXl&lEN0VNiGo+f7-X+uQ!)GKQmojB@*mG49Yyfz2BntT7As5cgoAQY zkND+B^h7klq`U~;Jn<3Gxcwja6<4tdfr!r$;T}?0iO%5zJ@tA@{RI>3W)kdq^f0jF zvShR!R`8Owq>t86<#cv!j^fHG`A0oPH(K7$gi;tntavENT)w6ObUhqZzGh<}?0zUI zT3)jmL2o^B3*`*8N9bxFFSuEi_9wlUe4Z+^P^0CpkyHUqmcEk`h1Ju+=ZW_Cm^$JU z72wnNZt(Hi0ESz#;)evZR(RdfZ@^~D{9-9R7^^8sN5}C;Xo&`ut{B`X749<7aKFbL zm$C=CQy=>wpz}vABBkerBwBR9ZeElhbzR?$RNlQ{`U(C7Zz~Suy~Tkn$^G})6NPHn zqEK@I2#n#pIt!6Cv)pS@&n{adoQ~;YX%5)S`<2XuK;{1A^ZT1DZ%{0;ZL&NAcET-S zxo@ajy!Z95L$Z8oAmphwI zCet7;lLaP2K1nt*;UhB3a}iJym*u ztiE6zY&R? ze^W<0slXvRnong$4VQh3KF6R72}}dJxE>YHb#eOkj&-pJoZ9H3JBZ$WOx^uI2DqJe zayv=j9`X}hR&MJ{RS=piPa!$gw>zfzF6R1{CPEwB>^n00(~vr}e5{fw-6EYvn zc{O)Ks*X(lIV5e{u2Vn_6s9}7P3zw{qTRyWOIiJRftB~4?I*dJl6b*og`Zru#eLZ= zp5;ZP7T24L3(=o6rj*l+TS|l7l7`g3}`^`hrEt)pR05@2NVEK$WFQ7eSz5!yoS|hY%|^Qg#hI$zw?3 z`yS5n`LFAKx;EpC_)2YJQ_WCn_H_Rw@0p{_dDQC_Yt2Wi82i=nFpv&(#Wece&^zd-&35QWi6<^QyJKz#gcVZS)xzevWQ&WZaIB&^S(po~WUPdnC-)sH27UBq zS+QV!X&mKvIRiN^zXE)7IqE3La2XG+4FhFOut` z)tMmvbKk;K?!kXsyKyS+j}Bo1>CX_G}7=3DWj znM4skoTL4MpJqex@DYv(n>?~_ux^?v_-@RWk7ME?nW_~QBdD=p9eIWdBz4~gZkJUbx->bP|MD)PmC7$d|kyjq@VLH`-gB&WcY#P;!Yoj&b<~LN6 zEHx5Dh3~iq9J$0N4p9xptOTJt36gMUuo%hI4^bH2m;VJDS<8hNlzK1t*u8kwG}awg5hq_0M%$G4oU z61lTRrU@rbPVNozNliegL?h=D`5TRVolY(xa=k{TN2#32TSWf1Mo!nsn~D5_M$Xd7 zQCEY!6lB=@P|TR*Aq-EGE4u6;SIP}~@)AmZkH#fMC%;AHVH)`+oxF$0R*f7iPt-La zchShfdbmhRIjv<$kE(fj#8i;K)yVyIaw;*|sF8zKkWb|IG&0RyaV8~1{W5^7SCQaEY0D%rD2fE<}l?+bBx@G9y1~xtft5z2tj090|#ts^p+FyoK!A zhrC_Cb{1EzMPl3l3L*5 zMb`5^+###gh!MQE`cWB>zlLVu4JGIfF}+!cRNsRu07tyK2i>@d*?5-Ps7%m{bL3y~6foM3r?r>?#N%^%AXQM0r|l(EF++qw z;wC&)b{68WWR$DbygU=Jl6&x`wTM>c>jI2}0KU-}96ni@ND~WA;u1)wzKK}6vG^~_ zpHt8npewKF_&CCMRh|Js-TW=4f=N}bB}vhyWrcW17M<;xc{#_mDdH2d5*C?TaM>44 z54bRJ=Va`2-XVWuFBx%-P~?N1UCP7=3kNt~cYqOR7K*;0CvLH#G9o`4lZ5mzO}+b) z-*4LFt3;JVyN;XW-6?whMP<{%tE@&XDLE*=i!l89KV*6@ucT$$!j3XL^ktl zc#W9X5i8=SL$cDH&TI%Yh07aNQbi>ZiiYy%Iy*gMa6=u9=Q^96y#mj5N~&2J=W*8R z8kkK5j#Opz3@Hk%OMWpeS_IcEn)4os=S1t+oa52X?h;~wH87Zcg(aM&Mp!bUli-|y zr*UR_o@Bp_=Sd@_jML6rk#7XZfR{7)!7zCAHV!wTZkb4M^2kJ7wzBj@+?1SDY1LQ2 z^UL;3;wxD8+v_eyj>7!Vs(X+cP91-A8-;t@1-B#$qdW!v(VjWSptlQERIE=jpTfhh zD&mZ1Smjsc_QfAE(lxay+puKLco1v~E&E8=3a z<x-O&3?GDAr=ln@$lSTB$ zq^q)X;;QwaLZOKRF>QPgS`k(#kSNv!e38^x9@5rIaU!0Zh*x+87<*BqV%lEzHkvjXZu&$Xc#~SIU=PyMk zaZA^U=h2`oh^xCCQFdTau9E?Y{YIEE3JhSO*`bRb%(kVamO#Ft=d|+dw5T>9SZ`n7H*5a7B0FIo_42f_DE6aA=pi@ zwid1q2FTXJ{X%Quw)m5_y@l$hStR3HIILnMirv&`!pRsSdcjUS%PNK+7g!Eg61|v9kp4KY26pr!i58|7A_o!wQ%7;tcBBon;}880o9yS*V3ac z+x(63<`AlCTdnWeaf zCQIZx@6Yf}=zIZZKCJm8mMvyeQY-xD&>b$DT}d-yEBwcCS~jr~vtbDAw;+&Li6a6# zvC?Q+)(Zbdtf6+MtngQ2t+exo75;Z)aPH3@v|G~1J?ZYjZ9P4(r4FQ_5-_2mlAPIw zNgViXY+M$*SI=@dZ+tN^p1{j&OJucVb|lXm?#Q z72TNQ+8B|W@w0P#u6)c67cWWO0@>{HCbYk0-?>`5IKTcBR^s=)huAx^<)ct_9P>z!tGER%0!%$G!PI1+D zI6DdsI4CE}I}6zz)1J|;5zUweszqFg<`Qz{ZMpKs9C^Fk%Ul9 z+gyhdN-o3}EzN2)cQ@Hf#3+|-EIb>*`H0I_$S$Uh6qUI9aBH#I8n}sC)l6QzYipdn zyca~cAs~YLnr5tja^5TzWMLBbnoVoBpa5g7xw1D`Zox_~%qqcES5v7Gx+h>&(ziul z+DmTu2{mVYRD4GBXyr2wOlC!p_P<@$OOjR3SoHkk;!P#i@8Nr5SZXf%nb$hz40np9 zUf7MkzAh?9-X_VrhU%(Al#zwdoCMg*(L4I>sLDcmN&4qAF z%07c8m5Dg0BFIv~*-@f0t_XJvk#c>Z>rhnnt-#r<77eir4sq1hoPsamNwaz{88Jwx z{`>8St$Y->W{9oVV!0EF*egJ?f{wKGF%Qcm5z&jJv4^3H-2*xSI0Z#p`1^ z^6;(3V+5-6$su(v$zR!djgPS^^K|q+AjI{fNRL;&Wi1;0R+RGr+!b^MyWS%nD*Co$NmtX{qAwAtSjpsG`5e$Ml_u~~TX3CIurH?o%OcF1xRv0p zaDYajo~C332&uURhjCAPgc}(Mw;Gg>eoRS73>f-0V&6=(be&d3v<*a?qSM|WTGbiW z`y7H?p*@SE!0#x)?Xl(hd8`j=MIUq$ebC!TN&VDoIN$9tr}G>6MVbC6qBpVVDHKhsG5AUqdhJNb zL{NPb(Nrrm_@%Q+EWZ3}!)JKJNE6@6PThQxL37#uLgf@o$7A4D&XYOp*h=IZ8M!Q% z$UO#uTn(~v3$A!q=0gzL_{f?_6A-u?E#XUfI_r}vcj;*rg5IMC*CAM9yE294docnT z%%BV&q*O2Ksh&a5WxJcFI*e2<4ypN!3a}jq>Y|hnbO6Ke(SxIj-A{V(HkRqyWR~gc zl<6hJsfV{vG2;J*Y}`ZsiCATwZk$noxQ8r4loEeypxkE|z!r_9>UtzlQ}HZ>cTEyS z6%3h(C_MCvNdXX#@M3;JnBHx0)n6l)XCUXmGQ9fJ;)9#90MCJ`F4)x#Nam`Ilss{p zP@Mw#igkw~sSheo^?ooO3&XK znMmC+!4up7S!hvsiY#PN<5h@ohMsDjFOv_d_C#IJb{yn6^ncz!5I`9VdU87)OpzT)04my zu~-rfnooRs01H3Z$A?(3!=uYdo0NW3y)5@QO|&^EIM`W6uyZV4P(Z?y05lS{0$`;? zm*YSa8W%k$QtsC6nh>9+>1gi`N^lzq z`PV=Ks%=}*Inw>}NaEW9bF@%ciR~BA^7}~aJ%d<^dywMN^|-gphfJ*4|J)av!hBs?=1 zYAbW7{dAwh49vEUgV6ZM4l(8)>jz|uj@-kU^Hv7clcj9LBQz+)@+`38%2QAmcw64r zsEZi&yhhFA{4ELn!FGzSkQHFdE8*Bi>JrtYL`;r$aoKL53ulbWb^&sr3;&EN1Bw&W zF<+uqF#zzzIjJZSmIh}$!y)X~8c=_N`l*JBhsbD1P>%A59=R5g zzSlsuECMs7Trc@bM5wpol^hx}Dbw93D6Kmpy*qXM6peW$$h68}Ek!@4N87dNQ!qHP zoGOa`ryhMBW%3172d{GIb%}y{5QM-G8m0Uf3Dp`*II8d96&reftgfR3SkPj{@L&9J zpv|Et$+t{oB6PQm$9Y17QbS;xtyI>bQ0ij3+Cx{5;>tbbR%E9{B|%B7*49vTI)dsw zbTx&pvT>!RB4^B=Q6v2xO?Yo0OV-SNE4Ar)T1EL97(qlVH|Xq)l3d@n;;BTGl+kC@ z;6!1;V97lo8y9#5rVmnC(&;*-PYRvnz06slWo~w4iF+YZ0WG~;aZy-pLQ}&*60`7X znN7Vl5szg_V^|N5>wq|x0|<~7zF_C>mL{ArvQ^Saw$$OoR(o*A{1q;?SYb@oY^B3MZ;uS?XooHC`$#q0C|$4JvXmb4?%o+ zlt6AUix?gNWYjPDGEgYklZ5*VURhH6%ywEz$eQNugY-?7w+10A{M?p*5G(02 zYZtUU1%@=7mBYS)nhK;yFCk$@>`})NmI@;GnFGArQpm9mxrLA!4GVTa_AZoMj_-}! zkm=RzG~nmu5NQXQUj#&COGY#^aSvE65&wy?Tc>TBHyi%M36gtrl&dYudL2uqYn zi(;nWQd}SZ+LfqkIS=nxS?*zx@hbr=lw(1#F+wq(g~l%cv4%a0Dn`zl!ud_dST+=m zB0w|)0!9tN zDTJjD$Y!BhlyO=-=t}m;%d#&8>xo3R;??0Ea3fOWxRzSc!AC)AC@29GD9DORkD*Aq zZ;Rr9DH#6!Jv8=ts z?2SVjQ5kHPRy49|{6L}GL%c3wQFv7Je7y4DW+2NeAknK6?0wysMIdHuTh@!_&;$ zDMQvL(JP7#3cb~-ny~&cM;>KGvIxXG+%qvDX8Qsox_T7e1ER>-j+Fz-6gD#1W%&rP zChtdRrk;CDcmjD4v8)5m*g_RGt+=N9~mTiZJ%_WmH=e`C>#xj5TBAQpIg$|hR9@MqRo2Xq2O;x;mn+sMx= zNuEsDh{ek;K7_7E>IsnB|{R#bJ<_A}xPHB+Lm9ll$ZYRWjf)98Cli zmGqG6-m-yJ_ZTjhIbBM@+;g9PNS>W>W+`l{!R|U?vZw4H?Qx{SrsDIElHTCpHnq9v z2gvgC)67`91I2sT(7SI|8Eiuge)VTq0k@>}Y>Z`=R0$pux1_S(u%uUb6j{>WSQIrq zvZUFFHF;No$5_t;bPxA;n3k&vCg_(knwHz-9e4!ew4`kHj6uiNrx>v`d+UkDqQRKi z6iUGZ5z9$bsPGk#keAutS6Y!nBQ=m!rd*A2ut!qv@GUo zUq!ZjUTuMXs9SW$|LZ0uPd>>b-`woAgU2Z9>d4*4gmqSe9g|sja-Ua*_W`%Nj+*3? zxM`tRqYg&wYDsL$Xmw7eOz&rzS{D0>B1=S#acG|LJj_Y zLdktTokZP0%(_x6G{o(!aIOxoISnV+!H7zngk3FVSy(7^10{D`-n@}zG7OoBuhxqd zJF$Ym+l`Vx86|+d?^RNe!Ui&U40r__Hx~lld|{18PWD{~tvyCe+?MN#xz>DF5XK$A z;EmZnU&AesCq}z$USuRVvmoIWkPyNZw9@3hR^{E zCqjiF3Am>XZKLGuyJMcb!r)W&rq_~X%e9Na976zmvZLZ2hx_RvjU&n~W0{Iw{@N~o zo-J?6mA5PD$VL4c@2|SPzh2(!+8PBdX9{BW-aZJ7t6Nu(VrT@@V+x?N0pe#zQQR#c;9UN>?*+?MV6 zfeK-XrolL_9kgX|Xx{X+lvmg?LVv~l(X33McRvtP?sg^bs-u?^`X!E*fL;@V zo=FdINpam+_GBehbTBBcgc#h<8RVhAdVm;USvMbfZFrd(7K;JHay#dYdo!)Uz$Cge zw)70SiVl3j8yAAI00-3%4^Tr3Iyz_)eHoe>8Cwro9W;HKaaZd&nrgHDex?)Tt)Wq* zn;4p&Kv&VBI@ko9gm!T>jr^tUphq$^ji_v)W;Kb=>!XO!qd1yu;m#0rm`14@tLR|R z=ptfZ<_usCeJsR)G`a=_RDC~@PB1c9ejHDQLK6$>^FbyR)ov9X4EjU}YiHSOKCCv@ z1;9ad&SYSE+)zb_YSIcX64|S|fP+b$3&X(ebbUcEU8zGjnCx>X11B4+qT`;ADpzf# zSt9C*N2UK3Dp>stRnJhr+g}E&ouQu9^ZL#HlG1YBFx34F#rn$!#%Z+@w6r3oSRk}v zA=vt;_fxOpV6wE{A>hul(L`1-FinEnmz^=D&4gA{-|34aIPr^UK@G!=*wZy{E zp@ds8H6kuG0}f)q-?c}YZ7`sI#ST3G!}#4J6xGO3%pPgq5Y|hOJhib}?gV`M9UpROsz_bsct}G7z zG^`cS)C8{|l0kilgXaT0(FoQx{RP9*-i}ptsHOwQQ$f^g7~WNaYq02TWWjyPaHk_^ z&QuolJLZwP$~k`Ty$1Pb(kd*f?5~1FAUiRP3M7pB7tUfeXYrDe1sCB!5YIdp>a}NnT~Mv`6R zcT@e}V^Bf+Zg~(-SL$Clem=?u{7Y@|;SC!gE&rPd{~*JoVY_A$i{I!G5<-Di2BdNA zH^&-lDC#)dtmb$7k(5x>M-275dEFF>TE zu3B6}wIhryc-6E9O$%v^UQizd)yvF%B-NfI76#RZ1Fu3nw+RN^#DHyz8;+vqx(3v9 z+*_p~ZMCDl;$CFplGRqxp}Mz@r>a%&Wq8+ST!Tffk%h4*BCD;ULv=b1Jb#j36*;~c z*TBbw;F%vEIVAKhAc!YP)Gto5mavE8x7}?h!tb>NsyOvIj&J37PY9lM!@MV@s;#0! zbt(>A{;P4N-plbVxTf-l;Ftyw$Hy4)y2bG-NI;S*I#gee0~g_1T&bTk z_t+)y#=Ld(@2Vh(rz`bYj!)v8lh)86@h0Ghj~!Y-6$E*(HUd z_R*3cnh|hY_U9PNs;i4PP_nKnI#ge$7jXrz? z4c0g*Q+=7^lR17(TYUKN6&yZpAp9RVK9l3~jrg!4kd0T-q54J~coC9`MK8`m;w<8g zEZQ$ZPz37c)vteGD#+vbukJFapgkvmdPsv4K*Fdma2ENT#q&lMT!fCD02(vYaU4H| z1?!dnRcCEMi1Rl@N*?=+~O z{jM*Frz>r58rM3l{B7~!4G|zM|G|VG$MUCk{}!<@j8x&kv{2yH4EVe4{?<^`k>h&1 zKRU`#R^8%wH%VP$6&(!imK3kP!SJqfUR>JOEa>+BPP--f)fpVWn&S(McwGeEZmmdO zMTctA6R)vBxKgjufuwEXWN{2`Uf55p;=4H|yS;xa;kZ!_TUI*_-8q80|S`)z0S_E40Kq1gCzdzMkd z%$*p>G)x0Q6&^E}_Umj`1Gb0@u<_-n%RAjaG7{fPne2o#W8|j^l z1q~!sbf_MI1Fz)a#9}FDv4^vG(#XO%KGHx^MThEpbUf)#wQ+n4$KMu$XGORttO!9o zNupjl%8H$ z_8^|F)M}2O!ts?1|39{~(S(13;i;YF6N}&I*|T-Q8PLvvzuV643Pp7bWcSQY~1c$bwc=}$%$Mmr~OrHT&KlXX0mS{={v z$s9j61kddJkuW?EDDXujQ` z1#TzBVIlHD^uP!(P?#7yl|6!K&zEIR!hGLE8 zwGl>L83res;i;lS^}{-tw5}E~u&bDtb!rHnS^SG(<`%@0@Y-H6t`d$sWo*ngX`2uy_VJD*^6ktWo&9KV|5|K1iKZf?OAGmh|6IQ}h; zpA?3Nx&4!=U?9>~(V_Yw9Ju`B32){2bsXO}4Bw8q1@UyH?G@uvwek;dQ~r+4Z35xf z9w4hBb88_MzhQ0<=z=rg!wmSlKKma+QE3dt%x#cSR=v7;A5FJ2RdlG%*YTuy_0)dW z!Bz6&{*+-Xu3>hD{QD|8RL|4#B)|Fr$JcWFe?sugT-JqIY!FY9sE={{W{#g{#Op=i z9VFc%RMDZD)WvK3L1HnGvuNflZZ@)Lzk>|cI4M&-v5%=>56AzIZd3s)Lb$~Shnb0l zf1l$|a{Rktcv!5$R6zG9RdlGHjsur}65;1^d@IM#3B$Kzu|YgtsRKDaIg&7DxA%RdlGP;_`w|B^Dbvi&)O0 z+Q_1Piwo8mDMMv@^T7M$_$S)p!!0h@&CekG2%di`#}5y~!{R<4LQ}eQZ(Bu&>Nz-Y z`3njE>t3dUbdJ9;#GnE$fB56hAfB$&4IDpHD}P&j#}@Yp;g>Kx^^sGE#cx>LOkHpW z%woXbwYb@#s2GM~7I%eF)-a133RD#x4AWSocy-%1OkJ70xStJfqppspu}FT^!|@Ww zyN!5V1a5IO2T(mH_p`5eFb)=(9|;=W-PM|ap&bTFuJF5#cy_+pMP55uF6>sW;(i8`9&OSJNb;gSC_ zmOtI0SJ9z*0S;V$^9kRTQJFPF6$89khcisagl6owW~Fu=rHYEXWT27eNab| zzfhMl?xd|EtiEkhA6tcYVn!v&SxN3u$#Pb*d(_Qx*3Gmt5SDI2IKy(y6+g^`^6au7 zuWP4b55B>)`C9_L#hpwafXb8#ny@uYBwGaUvR(b7RfrTkB!fz978p*ku_o9Y9| z8EZRJP0Q}fE%+&??ntD4Llh!Dr5bY3E^DaKy{YUa@MOHdO)qdcuVNny+AE*Pmi_9L zHPDo{bHp)h9Duz%qB7OH@pYK%%ULTYHvT6KyX``nK1Q!o3Mtpo@2wd{*q=7a=~k2}!inq)8Mw)suM{1{Oi} zYt<@gPEu4htRda|8Zi&nfLKc39YDEyqg>d9AT>~b-#TP3USH$&cmD=M{rPIOs>JSc z1!GAk`>{$M*krt2)l7T698h=uO3K6TC3oUo=qzhvwnZ?x7g|v**n8{(eVXdoYHSN2 zAN4_TbCM*sn*=Pv3VFI>@iJZwb$F6~gsiAb%QBt6StZlJ>sk4*k#C)NmzvgJ;q_T; z26$JYY@Vk{SCK2`~w4`cr_sD~-gm<{7Cne*PIpz=v&#T9)^g@fJ6QFeZ z0+i&Ck9aKzVDCh6RXJqMF|?VULj!H5pBpdPUJF|o?J*x=#Xx1GBlrIfFxU^2jW^Zs z8G{?Czl8NDm268JdMBU}mC0;HEPWmf&P8JV`+s=_Q^m&S$k;?-dXm+L@6~LI$jSJ@ zIV?v$L0=b9*R3b{IxXvhU2(*+Vu0-8dTh~A>-@6twk*D)Ud#p$;^V8$buUM&z$W1K zbDfb1y*`lRnHQ1kdAO7BUDA#f_7#gwG^rrijHi?MTnnyHm?La;I%{jx81R)j$&Cw$ zUz!Fk=LE33%#yM;EtX!*sYNHe$A}lU@tG$#sxHVY*Rjrqc523}OpqQsH7m}nP8r*a zeiSR5k=Uo_T+#QgR?D*cEC2n@J2%?T|A_CI)wN!mQtvU3G1X?vKczIutBQ2Js5RCaShlLWg1_v6dMsN=waYg&i7aaIeGc9FzAS9Y>O`f?PD;R5 zI)kSuef8QMCDR_FCzPQ&r@1)&35pMJ!nBM{@{`Qj~|41 zWd(w&x{}%rwn}j?Oi(`16Ld!cFTJVVF8eb8Df9KjhbhRoy^JewHDFrrHyKrh;lt#} zn2rw^mU>VGmu<;WD;0M&+Bl3bpLS+*$FVI}u>I?GP}<`xU+ltC&31&ff>a1nc;k#` z?}TXftTj&OAE}cl84&@@y~GA1E+3-s2@_-}6-bEfDmcCD3%#U4DH~l53oV52$?KM;M>u52A?x; zW{NL0iqF?&rf)CWFq&RA{DAh4!N!43d)6ic*lfDCNg!6U`Bg?O){;c#0h%9-WNmG<#I^aP7d`W0{{6$H$%%bm< z1Bh1rWr*pjY^CcnxK@6mD=)4%4{QHGZx|0A(92-uSDkGHNZhGNq>dw*_QZqMQauk~ zchGU&BO3800rdp5R}}37gTVzp4BjOf3`VKsR9uVx*=5T;OjTb-4a8;3^Ai+u zo7wvWA%?Zvm`z_@+WWyM*lN-22kTL{AxgQ2ay#Y16`8zx)1M%(n~WNR+fL`8Z0v7K z#ylO#*vkgAv2rbJIc2k0QwuG*cA+7R!HB-IXg9tSw4C;OGmXkPB(5U&EL%Qer#=7P zHSomu0h_%8x!!e;b(SvG8<2&37o}7uJx}7jNPh(Q zma$kZ>azWGkOkhwz>e=3@IVG)jCy-r&$BOb(pKKq@Sfpd528j1qvg1$9BlfU zoAJ5xcJi?B&gg(){b>+FBp;)lSLe!m95Niey}oinV=J1S&TbBQWUB8Ih~%qq;P3(V z!Dz9P2JXXRQJ1aDK^DkHp#4IpJO!)kj;aaqGUI5aDfTr=3LOX8t-@~Bv~_3G`vE1L zKn@-@=BqO167;X|i4&tf=`IAj`(is9WO6SuF}kw26$!esZUcAYt;q65@BA|`HZV$e z**c@hrsbt!&U7B%OMo2dhv*<>V`uYx?~-3gF<%}a#guIjm`j-Lj%NK0-@+==@(FgX z(9r0^QoT38g7EGyFyzFqdOysDqVx`DZ;5V0%~;ZDu%Td?y(3uFjA0U#p1nZgOy%PA zVV0WAV;;DuRa!LL-Wq(6)T~GA&^M^hMJ*a{ei1<* zirFrm-z|CW$56W;Zk_tCbH>;_(a93+Z5 zg|j*lT^0onBj62h!Ar_w#rO6Vzg~ve*sS3UnE2z*U_#t=37-;N zMFS}=R^_mZNU?MpyD*DowB)F;$ubb@g-mo|!Lwo$K6-+C7b<@<7SGWKB9|kXSg|YQ z`;edSveNe<@hbm2NM-koi=i7{xmnDv6DzO{MEt*z0B_CrHr3O{@)>pPTak?*HfEdf zt;plp(V!maIkZ48V>A0!WHE!76Zp3x$50I3j{*_jiOkO}IP1Wk-I12zM3*hM;#6YE z#nFUK4|0fD5a0DX)L2G6J_Fe-$6xvu0ULd^RvBUCh*ToeNz%cPRQo{m0#L;YOryj<0Fl_I7|TGyhm-i+7-|O_ z!k}9yw`60jAD?D}rz7C@b2}psBr*sB`z#~K>lrygPi^L@*D`Vh$W4}uShh#MCd*m< z>b4sKv?1Engofar9rTGFZ2I`QXEOZAqPvx1rgC>*yzraA$~0vtRT7ND^7kD~w{iK} z=P|{KXJ`uzvEo!ovB@m1?8hvw*yK;Tlpbpb-7*70Wb9d7OVbPS=WoS^1|ydWC2%RR zt!w$5)Chb^0-oSG2uxSYVwJa8?lH*S+XAZ6%)*!YAl!^F{OfX-XDEY@!x?-|fLDVI zHc;t*BPshhXe>j zN+vu$88D1eV0YC~V#VRnviS&Y(^4o8$fgV`*ax;e#iq=1TPhKhMOQm`_(u4ih~+$5A;vS)rVQWGMC_Y!ewQciCduQ7rCl?6Lq;?OI;MZ%lI!Nf@rrCsfGW`R*j{y<-0p4DOqz~|7LzbSn z&J~rp<{Z;Dhdkg{ESt;W%EdQMugq~Tid9>S;YEnb6%G@;s+hefy)=8ZX=DQnP|v#$JZl73~m%F{;0VN_{MGz?Hjx3&McKI zeUxcb*6wTvrI*F1L(uoRd?viATy#e7<&ovZ&v|>v z*Mwoa$&(YMzJR#`%v*Qmx7|n{?6cq! zmVG}xavmZ{FPu@wddbugwl)Hf*W(gNV6K;nULEO$vQnRb!~UCk+3gJ1%NboS)reDC zm|pHhHolhv{Rr*Xk;6vVT)7cF{BT9MfvhS8sZf_uYph>R#pLyu4telbROb%)X10OV zxrT_Me&-sn8Dd^`B{Y;={rtz-Fs-c3nn z*;QXj+0iJzXN%S}FoIBT9ryr_d?|p)V~BDc@g_&a<(E|R!DoW@X=@BV<*{~wf33zO zzEF!jpM3X(2JZ+BriKO+Lq^Ab7AA`@QHs+^n^?eFI6SK2OfX##O z_37jY_{U=D%M8Ih50}@}$i5wo6gwKTWATaYC5UBHRR9;^dlcIMjN-tlK_EukEq0(i zkNGpp|4W+B&e*nexMwN6A=;NcJ)#B`=TA9-bojvH6&TUdBXelXfFOe;86S`MC9`~R z3Vl(;kx^fC9G}A&*_a&_LB6qAdY*cof3os#kAt^E6Z@<%*Mt{l8)7uqt)0UB2eBO# z=7k`z{la7z3ghr(r$+`$UF*EvT+5S3Ebb$* zuU?83-?;BeMhn>k6JwU_J%<%S$~GoD?a#!C2SF@!*%BMAf*&o&W6tz$2Z=?3-i6W2 zJ^=}B_oHNtofVl~v2D}{(^a*umPqewh{4q^*T9C;ZII)eHolTW=^XZM}{FZHEtxhm}f@(9=q_p7PQi&cdRy4bZL_lEWEpTGu zsZY+MZ;tnY@RUEcO?(E!zB*(+ZlBZ8C|tIy0tIY^gC{sK4Q*M>^6pAv|IEZzyJAua z^O#rFo^K}AJUxgh?Wc|Hij!&-XCbmPi1Wi-66YCYrHMoSg!(3g^gSJ@nR#IA7t0cP zCWqi*leQt3h`TIzd{G8G_`I1-mYKMqA6L=ov|!y1;2aKs1Q>lcurU*!tJ|{edg3rF zz~ROa4(kjYd<{&7zi|$e7>7taf`~ZCfLlVG#>e76ds8&d-8#kn15X$R0deVS;>) zz8;CrCj|tV*k1CtS@I@x86~G5m!a;KpfY}~V=}xC68JsLWH6J#M1!GNQ5>nJwbFie zOnKN@y{r@|UAApot-N#ioGyy~0Km6+VoZQ4(tmKD8}%@~gNx^+TC`etit&p;D*9T) zV4m~eSafD2och^yR{rs3Zvu~7!Q%2FYxZZ@1;tu5RcqniIetISC_mMXsi0%L;qL?) z^NB2>`Y{6DNoenZ+V2MLXk(uaWCdP?ezq~QD^t4ri9oe$+MZ3%yQtbVZOi=v+WrZB zZJWxujV0H#O-kU}9?NrzW;u0()jwfYr{SG!^7HAboT$VU*IG&Ye*sr~YRk+-&DbH9 zC2;5pMlUw2Po6VYMd>dCXjW!DycEg}4Dz*vtcmibi3maMfk$Cl6}m2T7Rzb@MDi3Z zKU`i(5@0jcyvy1o0NvuXd^J@t;UkELpmu-!zhP^5{~Wn_=2M0G@I)2$ZRYjO@_7gH zp?`;m#0HLabWud#kx;a>>MR%oB%x_0s{COP1k+=S6x4~|n}SfFnx+#;EV~jU?=Ns- zz~l+WB+pzU3=c7bL$lj8gU>+L&ES0myl@3|Gca@h6*n_Y%)=6y#>{A{oJckEtgbCG z_&*_u%l2K9R;X|3f*JgAJl<{3;LrTP#QjW*R*OzBegT8e;#t1SqM5-zUK23*8+hDm z7T4C`TW7Uf(t{xDCEbWXh{5*;cWCnSn^;N9(7!ci#_*EfkB19}ru{aOxNN849D%?ZQiXkhu`(D%^PG8vFt!eUN8a&pixk+RuF&D5;Idy~*O*mh=iL zDa$CNX`i2IDCu4VSV>_Uh8Wbkc0o|IuHMKLNp9m=1zQ)rFb;Y@F1=ap zgNH;xZIu2M(M^^IdjwinpJ%ScJplX@jK$3E!QHSZQGJi#Su@?18v)@>WOE=XwNKU_ z)s;x)vaNzU!*uMS3)Vzl(bB4SLaBx(5(hERM8u!L^|=6@njMIV8+uK2)mO0M;-WM8~* zJ)g`(TZfLUF*AYJekZ*9ZRlICflT0P1J{tgbpwa?XLR(f*YaTrtXa?WH$*pCCd3A6 z-|{QQ{PwE7B8X#s>vYa{8%xgi{;sZu1i#(4-V4*hKHg%$aGncf7BrlDkdMnYz5(_^ zPWd>xV1`qmrB!3_?zh2kzP*7NPH*IndfkRlpqiqHB$ic!6zE&~YT}0XtxwNrx5t?W zvTiqH5MX^P)O_`0bk5)Q4)~VdTb}uqBXLuqHM_ zK9}vYI;|$Q(gmxDZ{Q!0iKs3$q$cizAZWs?D_KosArz>IWkeFoQb7vT#0!i`+a~;L zLAyQT5s>wo*o;8PDA$+sZ|=`DA)}{j%x?p|3 znHNfP>wQB2dx?cw8-uYg^J}l%kzcuDh|MKTp+43T1Cb zXVsW#<*lnP#4z-8gOMqcjOSSeN4YQiF^$-`^k#J!A6_(VlzxopCd~ z?Li!CT}wFMBUaK1>*scU3<-X_bv@jhT2~k3##`6F7&^p1o<27 zjX2pD;PieD-u&rA#&?32AF_~0g5R!*eF;<(%aI$ei9UhMOpu4WD&Ijqm+gCa8UKg8 zFM*4)isJoPMi~?aw=|dhR7gn1+yitB1QZMr1y?jg7?xy{nGsx4Y(OO>O>HqNHJ3Kq z&D7Fy1+B~_HOopZ%Nc1g%{`s>Klk2mm|?Nrd%yR7zxR8i!@1wN=bn4+x#ymH?)~Pw zAM1&qD8YK-FE;(71*?8`>4|Iz0zdc0N3183ai#Rc^Mulr#Q>%B#3sh1zMpHI(%_79 z2WvP-Pn^Yti=P|7`CB0&n!gqL8Q&qS>w>cSNIK{XFP$?QQj#pJX`cHOd8hMmU?`aL?GZTboQO+mGu2z|vDmK?? zV`~=UY6N{ygi@GIOwPu2x_IzKyy#!|i{7t+)bi}PK{$k|-FfF!uL2k!vWs!;9lPz)zosjSv;+M^!a2S8}V2BJ&}W;hQk zE%^2a7sGkI12ddo-(iNc5?6}h948d)A1K9xU&Itb>Zv=Ij-Jq$o{__Y@{F?9~dm7>lvLTSn#0ZJK%s~D5|>hu^-<8UREyt27G zwQd5hyd|qVl=|1h`ZM?ZD8`l@13+Td%|pDxR63UuY}rwXTg5cra`iU>Iq#|GzlE^q zCy{M!cbaKjnT~&L$J#rRWwYtHBV=K*y6tnG*O%qhpN?0Jh1s%-T((F`fp(Z}CN7jM zr-AUBRpA4<**^Q7ivxN6EoQa{uvzNjK!$M<-e-6OP;YU+jn*-<4McXe>Q}pRk4Uvp z5N;z1Cwq;k)uQ=U6HVElZCSI&i~69TXp-RG4&*!ZbA@USYU38)Ua73s;=hG_X5Co? z7p!~EP=Z&s_;SF=JL-l8A%Wd0r!B!tZSw;%9}NcLcsfZ zqw0l#UB6*AcMA@eOwzjkl#9(3@+wcWY-V$ByrJ0KSe|ELdG&3sJ6h2|2iC0w{0)E|wX=D(W-qSh&bDh(qwHevfs=_;p&2?Jm z&0J-3L0{MOs;D@*%19L9hI5Wh?JldhHJ~!?q`u*t8cnV;4@z=%mAimbc4wMlM_>Z76V88NqA11xHjB9>qH|;iQWL z$$(7g%!T0U;y{}4qWKID2a?Sv9I$2%*k$mR8n|N53p6O-W# ztHPtX1L?^p8PXOxkoh1n>pn+l!Wwmu5^T~sg(#zT(yHA-I(LjYkZmH{ns%JES(&tY z^D19r+021tLKZ%0wc&YlSzdhy^6SV39mrvz9WDJ37s{ly04}a7d>FU6@4t4jxy$RA z&9&lH)jE)6Etp1bW4d52|0;L+LK~$9WLK+t-*njAF+o_@<`!d)6pn{Qy?@63pg8l@|Pr{&4a=ANVnwyYw2f zxplZwZ0<)w;qeHd6r20ohY!iRQSYSq274kJXh%;3;zEgf|A7yy3XkPIF&Y9nx$-Pj ziy>Gps$$Ym)awN~fS=Cr82!`uM5OeDO+!8L`gNrzI-SB&1oRPtzHW!yrsCwvi&2CR z;rkTQT6LZP74Cl`o?z-cO$nyXi_L{WtT^hT&Z!UsLwN04rp_c>De7E8C{0-eP>L(x zz?jq@!agI&m9K-6TwVFqI46Cc!i9?~@5w7T>&x`C65gyTJicL9Ua1EoCs)1+3n}i( zTSBCIuKaOEE?hZ9iQJXXKut>PK3KzAm&Pma$SNPn9mwzS?zMAnSvW|{x^hG;Or?t` z!5qj7*cq*LAS@U~RX9}bD+r5z64}A;bxnnkk*>*1E4bN0uU529s5&)nQdQ1 zj31y>Cok}Jb7r;|Uu99o&a{%(_m9W|$pxqy)2r9!d*N zeCc8b>%5sA{PZ%jgXeIi*ufD(Y091gN|_CQ#Xe|5b`T%a;IMiGXonfJ$AwD-Qo#9l z1%H^qX}F=P@bTP%Y~nK(X^SEdyP6zG3?d@ds9}^~4rDBoM_D%4Mj$DlqhjoTh-~Y* zFIbxu2l5{HA-f&RW)9?+Rf+>y&h!4krY2fi??+ha!y26TMgZ+-X)jzT4#bl+Ya+L~ zi4enS-YY<*5aU^1Rc!>~$3>XQ@NggoKH&&$l>X&KHuv5o#pXJl#nJ?PVg-F&)AJx@ zk^?D05$-@9P)KVH=Lb}R-?$xCRlLL7IVqo5T^Cf0DlW?UN z&I^Rnl*Iz2IFNT3llt>so1x@D-iEh!bs%@5o%DGY7cLHD0I$G`5sr4Rg@>yOPifeJ zJoh*lIXRHc|HxwAYY&m?IgkuSE*uEt7Y<}Dujvt1(-hvBl?PoM$hwuR6ZRnnahVMw zdC^S_kIvkPNyN#4_#?Yo_0u0pXR6GCux>Bv_#8+^z{1HIOqXbUlBf^K2$JC54&)>( z1@kIu6Y-ByS*;zMfP9F5*2>%tPE&%%KZqEZ9jrLuVh2+p2*p1yGCN4Zm0|}=2!;3u zD8+$nU`*=UflpL}!|Gb3lNo%A3niR<2i~kId@An=4+!KmtnNp(P)C@kib+G^B%Rm* zd{?C%9r=VP;Y0KCOUSNPjsIQgiB9FW7@x~WZz{uTuUiAd zO2f#-u!46J!>T*4=`6faRd^Qf%mGy{!zvCkL6}@{bs1K_;SLAzV;CO8Y9yc4z?yaD zA!JvpDr%I@R0Rvdy1n>oZ8%np_dTB~lqiybtBAh3hss2$yO2UC|~2O)&glwAZ$8CLN^+`6l@ zE#VCgtJOd|%-|_pD8p(jd}3Aj6TBxj?QJW~@^4v&*1Y(=gO3v04jj zpH^5u7rl2wdCH`w8y;=xh{`luhTypzPtyY>v(yrM6R#$APmPN4tv#4yFRK8ryvOs` zaTNiHkgYP$E%Xi^P4*0erD?Xbc?kZCk%nH>ELcMAPosCtcY|0M&YnYJDwncH zt;^f^fkm~d3PA&O$Tb`z(m=~*}nz}>o zHruZ-4M*bvP0y0y$J{U)eqTzXA$f1fEjQB$2c>E$qYU?{`K1;&N5LI+;M!!>=eUY- ztl4CdSyyDBSGf{iay-q6cdyg4htcKxD)Z^U1Uz5K+CK3IYCCmNF_^?uwjP3}x$|e1 z@uajdxde|wYb-5m8>=Z@19eh^dr^aDQG-ViX-gbzg6HD>h)>$r>=8qHuy7Dmi}Uo_ zx!3fe7I#(hYI?(=xsmn~iP;0hObcelkHm9wtFiKSJRnC!FA%%m9qfLlO7YlYZB<7d zdDTt=&0FFs(Ay5GwT{Q(yfj;ewj9*N*fxfq()?$T+Su(=vYH5XFhGp~BF?r_Mrpy7DrXuRy$BHFqCmVFTD_WNZ6lC zIFw5`nn|cBn+P96teaY=ikS&3O8$g{EnYBeYMss*?%)guIPepA-J5LP9HjyVgON=ld0B6{4xv13yivw!Z_VRjTdEs~yOd%(UxaOczSNdIvL5h3XC_ zX#~9<*6VwCn|}bFxA|unBPdQQ6cQKV1D?B|=k8E)e`4iLFWENnjP**!t2|?oZ8USwft6MVy*(kY%KjZDiTT%}kb>LCET-WKH1pt*Lns z*asABJC1#}#?R81d92NsgvW9^ScLg+OgPR*MzzC8JAkMQt~djSk9tK=my=!+vA8Ok zqF#cebvcH6sA>WNC(Ytn*vu}`4MkeQ@u#3I(elguz3}*+HLAko36}u5o8x@oC*mo3QF&w9jM9Aaq%SD+KIYlMVVZ?U5ujHj z24lS6z<94xEkrGDmIU}~>lghH=7eAXBFNbIG=)&5O`!s~?`&%Jz&1}n?zuQAt4%6z zKp2FApH*Mm<7sSS{^_4Z32L+lYA8X-MhA=JGBqTAL$a&pfF-;=N;Ethw?09~MnY77 z_vq5|#ulP<8KYvF2`(I*(-kn?Uig(S^0qC)5Rduhr#0t>RWAVZIx zLF4IoIlQ-(A-or6MB$uVuZ-x>JDSCBHD???BMzF|!hvrd-Sea@IrT{%J%%`-j01-kl@x(n{#yCS?fjOfH7hqzClfViVEPFXqI zT_0>*V6Y(Wn-N0Qe>jz@9k1%j#Au;v&*0;#mSwV(q3Nl53HgSA%Q2eZQ!$~P20?44 zzNqjDRuYggiRvv+@UvB*25QALV#kQt;D-g2#Pr@L{O94ZE7#5DHp~xs>AzJMkye3{oyVx-lyRFSI9xiFNjCM2s)O1mj zKTcxx*@snBNvikVs72Y~QRUM^G+T~gX8*r`J(*FYP zb%&SY^oAQO-{-;tR(%W27Iut<`9jl*Wn_H2FT%wf!=c%C!cQU$9n@AbMd2h@_i)XY zYjpZu<)Be9p@%i49}pXjr3K|_wtPr2tNGVDJo;VbJnoZ>U!cXFTqJj!31zQ&xNFL2 zBE2@`C`R=(jLE7YYEMEl-egwEQ@B~}T_Q89{uD5}{7*iXZOONA_`xDJoIdA1HK~TG8ga3n)-I9A|L) z97Zx~(G%$K!jO`wLvB_i%4Nsq2I0`60LW80=mZxh-pzcjsru%kc(+{_Axpfw`P>cl z=ZnU=n{|JKDb6~$!R)=wJYrowv0c=nspx2cvu^%r}IHKzgzMDviVv6<5u9-cX2-Nz{B(t}}_+wqUH_1l{J=4?o5nGoBn>bgy!i z9+bA>%2hI54Prd{KT16QaI;Xetiv#NZQXdrgU%T}DZ`t}6YsIa`yaHAEo@JrLvWmB zbN<}<6aU%VDN!--Y3c6}l=)X$XnwYL<#Lepyt6ZCN0rJ|4K+L57^Ac}PhJyG}AjU9u zJK*x`Xr~Ul7l~aUBVJmcxQ;5P5%KNYqHcqz>LL)>eHEn})7-;U*1|};{|l)nk*)w~ z19o}#c3d_ zRgv`tYU0|F4^S=dDy1J3rC(vCRsSO4PoTCHg0uk*os6oZq2Y|>hlnleXsC`rmBh4@ zBG7Yx@a8mUrH%DV*D<7#RQk+KYWpxj+?am-iF7ka8<4(TUFjEtj_KD^2sE43@$+%s zoW|7j{}+KCrm_}t z)3ht->O8yE73c-V(vEnePM6hDI=zJ5_5>q7CWsqT$a_TkXv6id8&XFhZ5hjX|5`u2 zgxz-WI&1&G)c-J%T0q)R`|H;KLc?^oBkIVRPjoajefloAr{bz)_)$Mw9wp}ZH}jaG zra+`@Bd!tWA9F`Spsl&UE|8jGk>JBECT?ieqi8;F=`pXp{*$j~B0Tj+$e!3Km&@7n= zhleeKcFMLO-uHv%Xer){F8$r~uvzyG5t=%otm(kDy$Dy2K$9g;9+foZ>%hu(5SP{t zkFk~BcaUeh86sna6f;oO9YyC>Q5Q8IzjAjvr-A`FHSU>qXIO zn=c8j+48$%MPdH=n)wS)hf0Y*?XOlOoT62eX3KbV17vy>%_u2`OpE$cgDTo=A}I#8 zA>lPkDAzU)f6xeHlWWmOJ@HzG5l7u^v*Gku`74mh{6#71u~iTq>-Uq?yfX+v=y1p9 zcGm=P2<`(Q0~s}2|0VH2-5XWW^3xr#^dL_0MpGz%naIBki75Xfpv|2s9&!|`*iWv~ z_)xpq=)`feE)uygzBf_pHC3-a$wtfC;UcCYnpSH@&ytvSCDcQ$kVk9u61{qfv$@$k zNPg8-Y~P@$geKJNW#ht&S~C!Ts9w`z+cOwnEaOkGFFmbU6o@>$Cd3bi&TC2!Ao|z} zrNG?hkVwXkIQMBSn3f;FUM>CKg{a&8>$BI7bQ|JTKE%uRJWB8*AaSa75h&4DzTXqb z@;)vfuU#o3@U8Aw_o<1{F^r$wE5P^oIwU|{Hj zWM9x=$A(I6I!)wRe&TSznEAhXVck*X=@0C$t|ytZ6TClA2~E4 zc63a+Uq*Gf7Z&`**brikwqETD?(_E%uf23wXo=476sk8q#Lv-+U{u>kob51wX(#=` zL9`eNS9+r)9VYs(lm|gsa~yBT!Lf7gEH7d)w~g+7(YqLSYnJT^Icjvj!YVJXGT&&b zS!hOP`7WFzcce8A(s>Q^T-Jz(M2(i$9XKs;H5V;!I}jZS@vY?p2cj7v4p_GJQ`p=J z0^$=(pZ*HMMu?4;G6%&eLOf@o=WKY*)r2VJosRQ~akFYJc9KH(6t%>%Y{?;k)>O9w~6Tb<}us>@9RuZm79=3>Jo(yd%ofdpbhywD!Kb3l8q|aNWKjqdid~Y)*bNHZGsoM)M(pxnv`=IC9BoYE@&w1k zRc;`kfV)vRt{>Y>cxfPiH--fpbNx>skg+`EkTo84;1KeW1!yFM8i!JIQ0hX{t5d{5$d5fu&%G zxpFnp;8XK$M8#%*(e66!Xv*6$mYNY!QOc?6HAGWd13tVl(H+ooSAJ;DTvEL???L3j zJz~f21iJi*U#ZJAm3vT_N5MXs(`6}6WATp|QOQL@*`dyzjh?QV>C)5bs1U0GeIE5R z4!M2U&Q#B86rCM`JYyU75>uk^0fp%B8mC4@lviVO**cYk)NJ`iV@Vo=P{Fy!Z??xI zarmxFNBlxKH*mDl=0J&V#V<0Vfk&9Hh6SI11ur8b#GZD7X3P6xN0_!dv136~h2;mR zA_b*F_s;o>_w{p_J^9=jgI7V^g?e_b$;0SYqb@{xJ+ZkRPdv>xF-W3(zAL7U|07UK zWq})BKw>F!n8PrXU<~kn77OF?@%^w`)jA^1ax2%qgoIgl7#y%}SVlEvz~j?)>|)Yu zIbK+_OH*2cj1pZYQJK63YJbnitqPU(rInz-=$VBEj6_~3C>MYdPVF#FyGpAZEAqQF;-`(VN)F-3Y=eRSS?{hqwQWxU%eWIEr$}S`%x18k(vZ zfsNox$i|+v>c~;-S=*+uZq%OUNbRQ#NmDpB-`#4~;Y+MmhxOD5bhh(d&k*YrxE{Q#rX7*RmRH%9V(3_wL8I2~z}dFplHMn1bx8R$(0CP5 zpyh3c+K&+Bk5C0(e2V)V!LT;G`t+nRKDHtRKdxy?T00*Vn(S}-(X!o9>Lp?nmO|PMg^AFx$oSQ1SzMaPd?AZ;%$*iMw+f8h}AA)fU&$tO!Qt{3x zynregcKho&+(-zuY8KNPC%W8*7b@JrkUf(lOY!hS#j%x}n9~!Tq1i%H(#mb{Qk9+u zA}SVhk7$Ey{|oOtgYGV&Z}BS=74;v442|?RwshS2xaBEHz?g6_?d*2egwBu%x2XNh zy0Ijcv1yg+<6TIIPC{?6365y!uI+FLH5`7V*zuZ!kZ-8ZRJ*^zqBBPAhTq8GO`Gfo zTk|&1%@j@93N#D95kN_%>&I~kU6&KuHVS`m9uQ&$$<$q`Gwn!4>*q>Rao_3|)}YbU zH(2zg6a5)n(EGpedfJN^tZ67{X`)k1@B21v+yqPb#8qfdWXTe}zc&v*9&yaOWVD!k zKR}+bTlvYD^4)QGvoy#wrN@v%$Cfk4Jk!r~j>b)W@4OFDEVcpck#NsXGWXoUA;CmQ zK<~c8I(1jX)|Nf-#wJblu8PM3>&!>E4H9T+_mCoZHx#q}g)I||dM15|?(i8Iy-=EW z2PO--@Efadpytn?fVN%zxV6bOF=mV1%I7ePT7j~m)pNeI^+IX9(K*;KhxPL7)dZRbC6zu8gJ?5&`MNmXeAAqc#pJajCrdUIHPT^gMpKJ`Hv;q znRV|MQq#)}|B!8b$}j$a9A@2X{9*!fN_0Lu8QB0C*iIG^qlrFJ#~ds(90Iokxvdz}4f>-Lp@?OmBkNAf z+P2WXU1y6Q*lmSoBkeB2lWC*+PrgYjNlfxCBngCJIEAaEJBzYF<36lcaXdQ z65DkI5>DgnHl}(fr5c?CiL21%>Pe|~U(j@> z5GVz~GX<}mF}t)LM=?&7$6AAXNCiw?4jqW71+792q0D_ONQ=R2uM@?B&(*V?jl`LM( zt~w4?(Fe)hnCa;ghvy`4dnT@2wdx?8Al#%UM#@^iy|C;7p<#zsdwRw4^!w6W(-s$v7aq)NZOl*xDMw;?pdwJ6GpMfAd59 zMt=**xF^E=xqI}Y1pHt@wF(tg@nhhZQc`j=>oQ1MQ!A1TW2qTM!+@`J2-S7P1<`N!YMQfrXohqFgm(%ND?xq%YI&&{`z&NL%bMqHGu^6(cW zJfPZeI20r$B-1e&BYEcpu<0y$3rWA@Fb@MtTa)4-ak=U*kXo7$B9bGlglI;HJ{)m| z5b%T8UFV3CgkU`UI3m}KT-qa8fHi(5n>NV z(2ELqk9@!p89=}a7rsxnT1e-8m9nIYlJi;8o04-`(%r3E6@pqx@M={bq^NhRRl!J+ zsMV?mks=w*y1s}-JlHSZVNBg|VZPByvtSGI%2n-fiT4tgy@M+-|Moc5uBLkKzDLRF zZWyRPL;Vq3$?CRAX{lnHm1^dTr`2=mO|d@O?}>^Ga$7H$B8xnBl2jI&RoSZ;K{awO z;{}3kONojIc9O&v8iv+H@G|Q*Op|HGGy`MSEussf%w9wt*DtqQ5M;otnRsG{yI>A3?=d9~=HGqsfWwVvD!!!0X86w`0ryMlZDkd$4rd zgU(V7|3s!<9MHgC`+=D2N7$Vp^No3$1uvr-yh~W~%xE<>0xI$AvdYN2BPxyi{9>#3 zLzkEgO_HSqbA|O2QU#@$sCZed^6t%y>XLatqk8jxuh`H(OkXfE=eiYARg7`ptHU4|)_pX0JxHC@nGtI|Zu8jps=Xm*alucD-DQ3-DNy`!g!)PUD{ zE<>SMiepPcw3^Z#PzrSV3v`ONn8j8m;b(IOP{dR|>As!zkJw~sy#w*eRf$t*s{6?{ z8U$w5_lUFI%&K1q5Oxs5o>VTixU5n=OPAHEHYiCSoHs!Tq^N{9Bgs)p+=htNs*Qrc z7EFDE_xWtcT!J@HLY3AGHM`x{vRW1B#AYwbVR|>=m#o)}QPxq-@Pc~H&TDA2k9i<_5$cqW4De>8>v_=c6D%A=qRHb@aDchD|=O~w6tTLaTsBC)=;zp{m zc=Z6wi6mr&t`*6#0lP-n>u8H&+q*c(LWry{$Vlv+&{Cad#z0%R@lmc?joF@PULu+b zpCh>3PHPcf+Z1B+8)&UtzPwKSOpJhFi&V`!^byTZbHZa8;5x#8SEwO}PI#fvmjh%DM)tXBOE zE+iM#d6+{e9DMgsDf51J{N6o%B0_`@acy0TmE6uX_v4mrOR(Y9JP%&hgmW~_6G;UY zq-Iq(u?5eXxpf-h#Tqdh94U7SV*gqJYDQr~&YUXKP%OYGB8tIPs`bDyUVSt>kL~P+ ziqY2z$mjKMMEyWK3WW72?vqj}ax66-_=C|LS2@*-&DAGKr4>*3@fq^~u4s#_a)@P6 zXwe2No^UtXuMLzl1{*fEEsWU5whgw>9qr<7?M1SMHfRDW{0dptDX0)V7ypJVEp8bu z+1Lg^wd#*CvLraXP8=R`aM(p0zJ|!Q4|xp>DZh^+{}SbYMEShDE|aRc36Wr#$*#Nt zwV++dn(q@%S?wHb`cg0F@T>sJ>gLEAPo+ljEN{wc@5qXyQUj31hwv_}RZ;6NTR~Ji z9!jWu3lN!gQ&VLqu}p`S*e3GkY$f6V2gj{MeBOicd4;mNII_-C)^b)^L1U5cwcJD=m*TO&?tNM*A6I^n zy?NdqVQ>9CJ=ho%T4TbVfXmI;r5QaH`YU@SxFqZtP%sY(+$8cilH}ehoIyKAAbld* zaQK(F4i(owi|g+NJR#txk8t|e1pH0FQ~`eyP!{m+08amdfc_!;I!3@q0W|^+7SK(= zTY}FO0e!=G`DOyT58~H%LOHxOki$R4wN=1#0&W)c3S1?wR|~jNz;^^ZB%ngCKm|W( z1+OnaK-+SD{f2;31w0_~cMDk4$n~sMy!8v*{CbFh-U3c} zmE-3LxJ*EcfNNIs{NObl<_Y+|fSzkPe!PIo1nlq{$FCM}={kPxv!25jHgGt9BZt#o z=kU`vIQ&h(>^J%KmA5#2aubJ{?{GNkT@Fvb$D#fM4o7~-;p&e#{Btvh^2Z#$B4GDV z_;t}%4*wSL$8G#N>r)O#f5zc!J2>pTlfySH94_C*VW&MD=I-V2qJYQu@oWDo4%Z6U z;{d;IbC5&*=N$edV9uBP`m;kEhJMB2-oqTWI?CZv0lkm$Yn_0}0`5M+@oxw?{3O5L zEnvtu{Q5ls2cP2CTYlv5?K)7wC!FQ^j|-S1;4A@`3%E(Z?E?NJp!YdmzJq{~0u~53 zU%+JoDst=)*S`qZ@+Z#cQ2`SKOcn4M0Y4S+O98J7sPOIjbGSsG;Q|&3_?m#93wT;U zuk)P#egUHd%n@*%c&Bd+Ir@$yvyKCR~0D+N^ej1uxG*B^@Ob#?Gc{(psP(Y}WS zTq3XmnvDA5l9W2!O|MTk$c3qSnR>al%+#5(!Zs~GFFmCwwYHphL26!@tj|d;Fo3%;8#l57diKqf z4SFIqcsuwLSz)RX*`Yl{kZ(lV@GvI>6=Rb+BU3h_c0;x?J3miO2iuuo*FRG>fspay z)fE=z7lz5k{Cqh#H4oAi=BMcm2E9SnYUMOjVWB=xX&4BK1vgN z2Iv%;9=WN;v@A~BARTAxOeSTe8nR?`O-4?3n$Zv@dLytH!re(=}di4(B7Nyok$Z~dO z9`q)sqU#HdfkDtqeoiWxPOaUkwNqtkuOT~KUnplA<9AH8jwKiJ@73)o6ZO9_OWH4fQ!3?NRXe<(4tSskbPt(iV>|lAS z3A!%8FfY!A+93xtk&$XJ>OrZrXSj^PIs=xYm-Wz>oL@*io}VG-fj#WZl!yLx;%MQM|@yv%X1Cis=-TDFyLZMh)?_SfGCe+$I86yEA z8;qn1)N9H^H`Dm!7Q`!7Ye#_x6hy9)+nWqa*B9&4Ow8$_AS%qxga4)yYVCAt*K|`h z3|*gFV4NwZWx+#|A=bAFqAw)+)O4mJ&Q@5O4BrUrPfbskwKIaXdBNI*_+V{ju$G>8 zrgF?4$wlR*!i_h^1r-yGP&~@T*QbovqBF%XBO|B&jBJ!6sMh)8%}Vu>idt z=pw4K-NGCb8mN*xVJ&1az)9g(O&lTE!LVqOkmH5ekSDWId3wmXhBP_Tl&#ExOh1XR zThfgYRTN-i3PZo;%%m|`2=4(O58;`^$S{yq7x9|ZM=R7IRR1pupupe{3Mq zP;O)dlCkqFRF{^OpAS-PK}umh`K9<^N*Cx0X~GYN(aXr;!+;5()+V|78$M5w`H+=p zSsQZm(`)(4XgPNmVU*3OU#IhD0q%cLjsWCNhi2vY_h zm!l}2`7-9WX*l+IJRTmDO<)+@YHhI$PtGQ)4-X}l&9+9*mH97i(nR0XR^K^m!eK}Gy%HHH044huwc#U zjxneVzwW^@nn|97W+#Wr9DMks6p)TK=dmCJF;1$Slb>I}avXGOLD(0AKG0Yw2lP!3 zf_JOMLKpOrih&6V7ot`4+NIZB*pQxVVUf#AvyjoSC1W9?U`n%q_VEG`GX6kbh*o#py>xU=e_> z=!U^+L@e>Jfre{g-4aY>;vW+UQWhT(PqdD)tc^=>$>bOko0OOokwkJ}5rxpSFf|QE z>q;o(U~w_T%brDJotX1(MT@Cpd-jw$VPKa)`p?E~a<9ocU9X^^IddGC-oW$=qL1J! zV&X3Uxtu5{%fpi7WXC`iqZc7B=H}p>)T#O$UDp6ZSH}Q$teN0{XgwyDP5N|%+O%Rq z*RW5aK7)GElt+tBtSYi+!IYVqv0wwyWnMZopolNkuI*9_;qK8p%taCz3^UiUz9YH} zeG%%qCzY5k?O0l7XDU88S7ec~ z>fh+5XP9zwK>2TUSZC|AXVh8%_wWJfVR9tNN=sx4{4rhw#f-;&nA{~0|Jk?B*dR1V zIS-D;cKE&{@GEV|RuWGw`yq-nCnhm{k?o2M^k zVY#xuGbTQIe01cPq=+GL(PWG~uIA<7mSs7Y<{4T9QsA44aRc4uW}|L2JuQXY>NIW_ zGzl44K~_$tI5;~e2Qz;Tg7$R1R*x+Q>~~Puo0fuj6$?+Yr`mGdRA660yixM(fb`&i z^e5%y0K;VHG(wkZ#CAy9Ksid6o$2({Glu^vg6AEL>3hW;VN*!YeLts4TwND=G;u$##j&zNo45ai1*(Yl1_ z(IdtrMMrr{%GeO)x(67#)5a6uVS=cNczm@cc*3jSi)UTAorVi{;A9v=V5L83>BJWM zm=j7VBt-ezC3-!eLd0$0o6_LL{+d9b{;tLu%=j{G$BAX)K5|q-N-` zoq+L5F$(tSSf7e=LY{)2`8^>K+zp#%$X2MyP$HQY(;~G}u|tk=nhl9H(>O*hqjQ#r zB25UKN4tR9sL|08kuhYrOhC+wCfb+doEBgXs_Ti} z<0clH(P{OL8mNH=eGcndlvV~Pc_3~kYOM@I=1~A`oXCXO*k#Qpvk;hxc zMCc>M4rR0sF45Sb7y^-ETnYO+m+HqV9vUlzMIvQfL~K$D7tDcY)v+As!u`3llo=a8 zj9)l7^l_#fz%%0_5|dI$J}0>!;aN$sBckh75aLW2>U_~#=}6XgZD4P7T3$g)kc19M zkbAS)kR|)nCi}7^vo8^91S?ys!E)_1&I5Gv;kXAx4vu1UJ_>2~#}TC{yRuSlb}>9J z-3#aUwAs{xyMGjy3J(+{F$Pj{K)N;{eKJ-!R3rfRk>FM&H48-t!G}_UW-(ZIL6(e& z6lzZ=yI0qNSSw&}hdX0z=_Cg ziq$QN#?(%AVYE?&Ne0uWXcw)s^f?(?+JKhyIR<^htXS7d@G=PS^RVTZ4L#6A(w&NQ zmzj1A63iqb&ULcX_QB*5rtJgI*E@{;M?{g6PDpZDtl!w2DAPth#nmj(q22V_&cpJ_ zq&Khtj3s#l#*)%>wzEXB8N2Q#aSBXZv~t5Q5oj9mb}7q>IANx1X$whd_;h7vRw8NT zT5J#@>MBZ|NoHU)72I(#q3QC@`0%Gx?k}udMK~*Toj>$j8=@-nA?hVi;_PW7MT%uK*+g>0Km*Djy5hxZ$U1V@C_kEP}B0T+Losy z0wSr&=q0|(!#A+SeF(OfS759SPZ6PrxtMBa3P5+WTf(d!-t}Da6jL5;gr=uRBNH%7 zj806Fm|vA5hKwAY#0{M3h{7VNS?6;_MS!^j|#t2hC;<&_U3R4eo zT*AYKsr%Pn68kW9KL>)<8m8{+KtPl*bsxtii5I5sEvcEQ($t7wq`+Fk)YuY)XkluR zMH6NtSu}Gtl7&)3>SxiPF=-iuB~)AP)^5B-q%& zLPhLuvKujj=!4mKbdo%Bs2n*VGA?>BeQ5Qj?37V!)uZuKBrIYvH-Li>0C*QNwwsfY zZ_1+r#uR2O>_<_l*hnC^%eS*w+l12k(C>~6K}zFr4nbmMm^^nFGc%qZ&C=v=$;FUw z3X`1GBUng^TGE5m$xsQLEwvciXU-W6;hj|5xFpP`V4Rq5DooRB6Pae?=uQLe85HQC zN%q@}fwEqQ0X0xg)$vGqpp>7HA!RGKt1;(^+u%s?o8y##7sLgn_-#gs?chj`yWG++ z@e>&4ENQ)ENG)>gMg?GN))9UOYBPdpB-8Ek91y|>vF#tR5u(L;lcS@f#zaOtwu{(? zDeVE|z$ZztO(~3~?J$Wp8>BDL@ZcX#bpz_F+A+FLilvmbzgfad|}p;tRj zyDb2`|Hr%bMSw2@t_N&>=C1t!U^w7ez$Cm1DY&U5^|qlMfGL1EfR%tHfUg6-2pD?t zu6;A$SimEIMKyQrzX5Irq?18U0CoiI{@Y!92;d~ZIKUSHivbV+j`jm?`|Ga#IN-!9 zckQxTl2-kV`T$i|At&JDfbRot1KbBV_8RmKxaKDGj{UYZx1e{xmUkd8;B$cZNttvS za1r3LyWkIK1GEBugU3cfn&GzucxZeI;2k{O@;+cD9vu1`FcA+TMKwo#fRg~X<8jjh zzy)|l;2_&nfo!1aK?0k*^$R{b=RL~nZxZVNdh?DizU zH%Hp-YXG+bZU)RA1v%PbFAvYdhXdXOoCH{b=eA!2yal)!u+=!b{Vd=gINn0OUy^!E zz`>t@krVCqEWqSsyL|=VX~5%vO(xmxmjK@aY}X$BpJKO<2b{GWbbybpu-kV520aJ9 zfHBX5ZwEYgv=a3L4&7w8zX4bccm%M+J7^c+OhB)WIOGTCVfzD~eh>Np4E(@u&jIxN z5XamC7JUpk0MBhf`#MR|hMjma5AZDu6%kr!@zX+pN)& zTd|*8hvrSambx|dBRp72rw-k<_YgD$8m5;df8-JU_%ARP-I4J18|vF`xTaZ=SBdm! z`+*Pj_3sL-{SYgf4uhU3Nq#=w8~?I=Ih(dlNX~O&@|s@ZA6$%%6P-cOKtWz`=Cchj2IWT@Ds`db%Yq^d)Cc;6*%*}704@wuYK2%m+ei=VsQOF^1R`HHKfELzJ5#G zhxoR8#$$-DTcpW-^ z*S?bKacRTj&P`x#2t<8hC+^xi6D>Z}mO;Qp1DDS*lGF>3Y-J5_9fW*~NiPdLB79}D z=P=(jp6;J``^rF}IwlF}xD>Pt;p;J!U`)P#W1tDr(aXS>18)}iT&4x|39h#y?-KF~ zC=blc?oqzs?o+)Ly%XQ>K{E(*Mn4A)Y!d0efgcY%9g6d>I!y2w<=%)E$qvFXFUsHF zwf{i#RILt&`M&R!;jBc`R}N^8p1W)Bi8Or(R{~s(6OQDjclN4&68ebYHb?r{1bkEA zmmw{U^gCD25mdgK0S=xn1x+w*voz^{#!b;C;_=li)Gmt&u(_`{{?i?t@q$;=k~k;t}Z9&>#dK(kI0= z-4Q=Lfi#!bJ&W||k4uVmOvsxc@|=83g5qLG@B2Wv5p>B!hY#US0rxv_uP_W^9l+m! zn}L{QIO%4B(C=azn+r(4W>u7LFOMiUU$4DYUw-ujbgf$8x!B_wcaMqCMj*&AZWRwQ ziBqw#sOWCNChS>qGo%eF5f#Y^A$cy++Wj1s$DtB0c8oS4nnWrytyZ_6>>l z4WH=S%Y9)z<-21RqIyw09N&H57mZl)iF@$#Xj#7x=LjyO3yNc>T}NDtv^4x*b#d@s zx}ZKC4}MK=+_h&AKk_-LzFuS(1;CF1-VM43KAgrtDR4s&vwn#*;oN6(Cq#VKAn!8r zXg$LCOy_*I0-u2Rww1sWpD%$M3EXppV{<|dV-$!>EAkE?kJ*w--?%3^`)L|?tr2r4 zB4(Z~_&ANbLZu_AzCobd2s#!|p^YiRcT#=hk@qq3J|`Y^{GR)sTE|DUrBokcb2{qD z)o$D|f!D?oL`&;~Aa}dH80k8+3C^@3$o?L*CeXe}d?7u{rHXQ`nPeO;PJJ4L&k@q zWG_d+>pdJA(+z2|m&f5u2~X>x?Z9Js!SFO`MNt~-p!b2#qx8Sk9qvA+p{oDJ_=^Fb zli;(SI?2Vprc?0MYlv^i5Z~}(r*uIh>BeZB@$;O@I^+L)I-1F2^pz+7FR^kIPj)I^ z^dHiVwb~i~U-*`f~o4x*DTt41aIg{(C<*#^?WZz5j*(f1zni{(JY)z5T%dyY)Kz zgd*43(Ag}VC)QjgB%@d{90BN4L3X~*a+&wtS15E8Pi2AbI_Sny0CMj*1KT7X?wcA} z%}@-z8NA#=aA-5q6yp&81Hk?Bh}}-FB>orvQNAT^BN|~Z(K@{~0;beZyIn2fv4+>- z9z`N@bY6n9HEj~gKQz#8UkF|z-YcUuEybh-$a@ZX%kCAE&UbTNZlWB;+nZ3fW{{ol zH?jC0p*!})DC9bTyumo6>3+f2d7r_fg_|SbruO{}+8%@L_S1s4k@kJmSo`|5!AX*j z+8ui)qn+aZ1ms;nUOVFLY7ZYe$LA#T9MFCp{_nIT^BbVGU?02$Y3kpGWp)gNYI~?81_NhOrc9utyOM+yFH#{Cp4(vXez6VFm6>FQCrlMLXXkaj|iaNf_sjMK;yj8uxy_#l0NbSE2sBXT1d;{To~RQv0TW*Qm92es6^C z4&3BQq`W!E3wsS~PfuKsUa~!zUV7p3MdU5sXtxi8zDb6L$2;~ykxic{e7{7QH*haW zPl#H%qaF7KV(8vL4BZ{1Nb>VgCQir=&$VYifdkWUBO0Alp~R z^+17W&T?U=zTqr|+nnrk+&6+jbOrldnw-iYZvU|lOq+e!y$+;qi2RNMujG?S(C4gs zIR4`Pk+{twd-7{+<+6|L#jj~QjXp6VAKM-5Lx*b8hs=mRWOwwzbl~!#A;vyaxV%c= zPZ1fIGTDcQ1byIA*vIM}&Y*%{B(9ZqOkufn51N0J`f)HKyKNLA=MV5bF z9WF}#Uj~nJJ=CprhUo7F0zNO`Mgg}7SS8>|0e=0iPFeqkvlktP=2~fWHcOO~598qJ9A%6mWomLj@cwV1|G*1Y98C^8#)Zu&%!D zbzM^0liflg8alDn`9tXR_RkB;6ecx3+NyO2l}Uc=tV5_nUbE$Q3CFo zDy}(})lEryPXK+~*k9cLQp$;I{De_S)rD^ONa8LjqBOp2{691y5q0%tS<1v_23UP{2fQTR6! z_ohZlW2Eu;H&IHKCP|a=Z>*Gp?-VIbN|*FfCjMpNU#j#3zSE>!{L8~XJfVc|bi9cI z53t}jOEb{6Vti*xv+-{Z{>_r+;yX{8kAF|$Ux`$TZ<(|}S|pXbwAb}Q(T{?4)*ty^ zC7=8*_kD|{O6eJCiL{g#QF>7^9EFj9N_hpnOxP`vlkZmY$!|AjL>?0T^Ta=Qyl=xD zwUUp;FF*L_;RpsxUQOljB!}T89Ip9>Lpr^iKJd5fBYn*A*C#FB$8X`o zdo)Fp+PuDP@8#mA$NK!3-0R6bJ#K&0VMFzc-S4DizC3^FlSO}Bez)nv%e>zGME`a2 z?0uttU;D?zRlScN{LH>2H#D==o!7ePQ@uK`EPZ@`a_quY9=(E=Z`krxns)Tv_nKXs zXX(7^#+bIdjFt)e&kp-1dw}KZu?wS1ueYArcAtOH2iLtT2Xy`MXSa@nV+R+#H^F~K za*Lp&3*K9osMhVt-7<2=N6(M?;e-44-d=DjV9k}+)1KMj^t-M?tmt=mN}7$?_BD{5~4h?x`!CXQ`Tf|Kl^glYdw`;Yvzc|3jy< zM%okn#udJQ`t*Rb7}EpqnOC-bIP$`UBfFDp{_e7S&jX7>KfcneFw+g z-&Q>;cV+A9K69;;KfSZrn3FUrPo}YU6C``^uzq*+gBeyetG1sh!-l?`}FD(@x9xyLoL@n_F*^o3!kli zV|M2Uvd+9)b)nmduRC{py~EhsL&C3)${f}HM6%bR6GMkwnB1&wg{^F*|MizgBzNof ztS$7)u9Q)iZbW>LAN2I7)k~*7cTyGn#Xpa$|1!3Db8pooO^?rC>$ZEas%rk(`)ghZ z?Vvk!W&ivAlTZEf*NzW5F6q9c`QF&4MpbS}UH!_lXW!Wy^lDMricP2Aj6D~u_Kyp= z-7i@#Z~yjzvVh^!9{bj#+qMO3mu$#=D)ya6!j2tm*DPz^j{NmEgM(olhp$)kDBbK+ zY(78DbU0)FBcBZ3(Dw5PO^2HkzRkS7Ow)Ig_vuI7hQ8OY$-ur>{g=M(w&wZe-+b2Q zgU-FfDh57Vd}i|SS9-5%*Vp{it8dzZzPR3f_{o;`g4ch4!M)Gx8(I(Ak>BRX^Us}b z1i@O{(nEBAb} z$(^z%J$j72vO9TY#f7MI*{h8YjJuS(F7v)W4u5iA#NwalrLVaDO8Kwz%e&;xT-xNX zzU|A7n*Z_tTU9XBf5Ll<-)Z&TFYRx(oDuuy(QAGx``;Ivd8CAQ@*J2Qy-_cJH2t^L znhrbmu4}vO^5k;?niqO3KCV6d^jE85f||JbCbyrk>qs9<`T%X;kd%EL#>_jh|JiSM ztp4tW)o<c6K>Rh@IH>fYN`b^OcL)IM|CagRSSX3pLrxvML;zr1!qaOabgmS+qoxj$#vNj0mI z->dwx^X--sPAV;1z2u1q@d#x>`@Iq|a-KRIw^!Q($) z{mJN}6Cb(iw)sV$tbg@~mumlg{&T-6U$}JKaf2T`@cuJ3AMCmC?q2_~@$t%xzRxW` zwcnP3AKkp@%7L41e)Lf9K!en$OluyJYh9jc?hBp@MO{UOD5^+28pa z-d^|i4ZVMT@xSgKb=%s9o(+vT_s@G;Jjc~-y6AAqdtcu=;NxHaP;%(vVXv(}b!6kr zNhxb*KI|^EQ{PH%oAqMxfgP)@Lk|^Yu3BETDbhCnlC3}A+wb|5oQKN;zgT)`Z^?n{ z#-8gQ-us)n1K)pq;mJ$O?pd%T`Qszw_unyhz~2WQxUFu)n&FwrJGWl<{1Y#a_~Vmv zZj7w|!(DriG##)H-Cyxm=?~u|`gi^A;)chc+kNSI-;67oKKkyAaicHlHSFW?8sEEz z-|h9!z~bLtv~p|0qCqRa9`wWwCwOkWui~{Kb4MlDwEb#t!1uck5}uAMy7nJ?-y1w} z=iE15$rw8Eety>I-EZJm#-|JUfZj}M%G!&zh6-)VfS zPsS4$-ZbREmf>R$G>u=rt!nL#Z-!*vJK>76A1Hlxll^@0pVFTBAuwm>st5BABqpDf z{OmVZKlsL}&0D`e(>G(pCr@2>Br)-^x63!|zw)E|Mm|@1)At*j9)55}-w|UfKRbNo zAIn!g^QYy1`_0@9Wv3VCH5UE;Uf=N}AKkrea>7e{SN-WvI-+kBj=he)-?yWC- zJ^G&K3{PS0t}t-N!KE34O|vj?RuxekNcK&pl_AVzPhsS#!=Aoi#4EC^uil023I9e_A*dQT-07-vqbF z`@xuavaT4t|0du`5;IY{u-E{7w@XlW;ikTC-n*sX%Di`*_vYBN6xQiGyV9R8?_uUW zdXK!fo47OmDFCEC{AgtA^RCp3=;@uF9a`#FCvbJHIghwa zMv)WNP!QanM*3b>lC_GWuB4lgGI=sid)$Zmf~U2LIDR(|ca=4jXntHyLF;`mb^n{f z9%}{|x{pve)B2dgKT$Z#I+4ouGljELXjy<;xhRsKLeJ4|7e|Uy5~=739Py?ExH=pu zOL?5gdU2#8WdSix;>g038scWT<^iipnM-87T?-MZPkEEd)z?J@4yRl}+&mnKrkqRp z3~*K9PDhG|B7trq&~BDKJdzuho`L;o~v^<4s^I=n@A~l7uqw>2(~jOeh5Rq_eIBnq<+(dJm<1 z9)UDIksQ+w(CHAJz(=L^r4y0y3F)?hJef*WpEREmSdSo_bZ!Uelr;)vNLsKAVauWw z8cF9-QjhfnUsxK-zq35%H{=fN-((E~WJ?K-g>9 z;FeTNJj<+&6b?{$mh~y6t)p;-^#FzIDLmgIw_Qn%6kcczBfObZRE26>i&*jw+|EyG zr7ByUu&AVH60%WNkdn1g*s?CiIcW*8@K_s&<`N1YXDuLhmr^*>YQZ^a<&~h!vYLth za?(yVvLQhxSwG@DAdiSFVwz;>Fj+_fO@vRHHH_hrIC~-hsODNHM5z)6(e3gnOho!* z#gRyuNF~sW!K8|6zF&`XdZg>#aX(RIECQ0aG6Pm|L8yeuCj<2)UDb(;MgFIfuAwq1 zYa>ywA)~Og+^!`Ok4h!6?L=@O8KUa%O&)!a(q4{8@|d*@C3@8oJ%YQjm61*dos<<&U9~}CT~r|$-R++$~qJL-1ku9w=A1T z?`M^uP9uONS=WFlqc4aO$Hg2YXx7$Y z;{5zDdSSP&LMrzQG#}Nn)`7;o{U(GxRyiemWiP^+)?bN!*S82~S#3n~7Yb)vcTn2D z4#P`-zV!jozfO3uRZTQ+k`%mFKGD2I;T0;KI+Zj!q4-qXB#X-9xd_2?%&jyssx*%B zsfun;+tH_hPJIC`1E?QQvWP0lB8ntyB*M(@CImPq&F-l5t%mT`ctUE(X?)@vyXh{U z$iE>npj#+4XH0mKbqCIDoK$yHxsMGbFQ`pjD(OwFB^jNfy!kKz3`hdb&mIX%c4=J2&@lf;;h4U>QiT+OEVv7f&PbloQ zcpUl%h081+hCZWkh4n2dZ9lb_g;q8x^9u@BSv)p;Nt&x4!o$e{Dsr}K$W9{qie}E{ zyHqNP$Bi)e-RL=PX3^0PIs*vizMV!Mxu0YWVOtmpUVLw|xtFev{|9(ktEm+ne>2R` zx`Kj3+fdPz%tfF}aqpAol>yW|c=1ny^1<{i7qvAy$SS&@NN9Obf{HN3U~u;$PHW}5 zDO_pjBGOy~T<(6y_dBT{4KvD>=0d0sAs&43PZ*@!{Z8w1dY>8TsOyQUPoFb!4{cF` zC|R%mKw%+tA*$qb@axlu61fnyQoA_t$~1}gnvqV?-ohVI{9=*e>Q2|UI~~O3a?MC5 zZv9568R>aQ*grjn)-%v`@?cGn)(Zqsz$m_?(+x^@TslfYE5HU419VEJUg%pAxx6#d zO^GwJK|2(A4Cb2jGWd}05*3r4#&%U~@?c^;G!{sp&uc8;bCTl33z5em^k|r%A0k~p z_Dj{Dd65)QE?(t+RdM94uIEisUslROi+C{ZgnLSp|?w-6G7|)0^L!UUv?$v~F0_K!jsiftT8yV_6RxA|07I?zS+tBl&`^gc zS_>FAgb+lVrS-Y+^FT)x{uA(Rya&O?l-VfFkBzvxb!OgU+>>3i+9u^CB+y6wlmzoS z~X>b4Pwg4c14KqQ+uEtVyjx1_x4r>m+j(85pt{QtpwS|SaTd7>U z(t-m0vYM6C9L4@tlh}(v12)xcrk$H6K_fZi$6{}8{MFS|XXTU^X5~P|lVG(-niHs) zQHpag1dz6h&!J`Y0qp$?5G2JDa~guY=Sfb0wr{M>!G_*BFc;K|wt>w-HL<`Rn~Weo z>^LTzP+;;S5XFW}A#B7Kh&DxXc%}FxGAV4@icQsO{Ui%4ANRLMZQd9JacmzD^7AHn zxYb6x9g%r*+hFlvV;>QsBn&kwoA(J1b!&$94x&ZoS@bq(+idDKKs(^q`XkX3k&S)z zkPq#* #}9L5%4QLVi$7PM1aOqpf>S!H84E;0^m?Ll{IPzhYAqB_H_O4fvIz0rvs z3~_7ku0L*JhmHD%0I`5@(E}n7sfRt<*kh`u31%V{sg8yg`!(mq*v`{#=S`Bi%usnF zBt|V5MF?PLa_n4XlfYOU$N}3VV$TFE7bAPnzyl8W*Z877=EEDnYXg@|S#lBL#DY9EhSJn>GhQh|3f!Tx)r42r+eJE08+IXiS?-LolGN ziV97IM_ZgeW7ah3NMqTCSn25WQ72XctB*QgEe_HM2?sW(E03L2M1mw4ppZ~CE=Ki6 zIbtbV>Z~^ug7vPorL`Ype$p;rP$WX^LsEw=!KEW7IiOK-HYggloI#K`r@$5aH&m13 z1_YrNkuj{9bwk_L;s&gI{8*6$cY<9V7%N;$v#a4!QkaZJ!@inv3Pw&sfaYWMrnPTs zjFL;KyDXTtjzALXQjPMphDcgsws8$y8*q2wv?4^$O(7q3(4p!@=$>GG=x+Qut+h}x z#=4`22pP+Iyg>s{_hEipG>94Z%-CcGJTopCI&*cVH|cEoj%U)nC(p$u-T&l@4_PXl z;5~}ejZwX`N8H^tFDEt;{W_bK=#7Oq?8cLXnU@oL(~U<8Gk+%@PgXt6dvW7KkeM$N zPoJX9yqkEuH`YCQV<8T^F&oIpKlY{@zcg2gJmc|HWu7hL@qS(3UE}fo%DkV%;~sVR zsQDRqlfXBqr>2y|l5*Is1}HOsD)y#ZrFYGnipMcasfT$xZp?N%X!~MGh5sNty!C`< zD6g+4JX2u@?;iNzdB2Cl&2Lvn-*7848!Y~wn`f`aV-$1KCJ;RwZnNow6=0VHvib?@gmfHT#6v!o-}Vah|rCKn|XES=5G;jVK!Qs z$kQb^o@V@L{q6%!{LMT)Ay;28{n2*P2Ml{Ee;RPg_uz6Lv!MFZLG#85|I~qx5PV-q z)AIyL(2o-QDZve&Qw3Kt@512Y1h*XcX@Ywk_+-HkJIXUv@J>g*6@qVf;J*}npMy`W z;13BsUV-?C3clHaUoQ9t2miH#Z*kDyXXt}I%@}by$a8m3dZF*xF7yL^e_5glW6nL% zj{-ej?2qaP=!>K_i_nW@ELQu1>eV@q1I6>&EguiLO zd4g|t@EI@ojUqS0|1{x0XPlS$@*WBZl?wjBB#r-*?_v)t!9Tf0dp|2LkF&@dhL!&SHQE5Od0|~EXJXLL-?PUb-`+VFY{Ht!(ayI(COYnLJzESWM zg5%MHkIjsuJk^>{RKw~qp*Q2B;s281BlFVGIQbX=f-KA;c8;?<4E^1jKRSIr{v!D0 z4t>1|yeB!({vSQzy`WH%^NNka-=q1b8~ibiXK7f`4>mpV$zwcKHJN4X*O!EW$0EivRldXCLcporg}(J_I>~q@K8BIpHap6{RQPlXZuGTM_%mPdzSM$=AWSsHfg;Wx!odsrVY}3M2%{*;H%|1q?hntfQCcm?{Kv1 zM}&WsJntF)j|-n!Cush>zmLM+b4;J9IvPx}lW|R>jSKkVsbH{oazd-1Z2)_P^#*KXXK)*fN z`Eb#@nI~%OEnD!+r**zYZn?}SRsC&<=Fj^;A#eH#mg;rSPa5YnFTm-yKf+&|rSUPq z=$OL%Gw>Lt`5XPt5c-)byiCXIDG{10_+hb!NBFK%*YUV>^m_{ZphEd>xmNSxb(2U_ z#rbBcEslO>kQiZtMn0DbpGTH!KI@Su9ajkcnCQ#k z*9reJM?1ZZ>2=!J^BJ)7p7i+eG3d7n|Exd8>v22d=*Ma`4zuCoRpyhb=E^v0^zxSQ z$re6_{vDzJUiAC2@Yyf)H#+3}mC!ef{e*=6UqZi6=#4!8Ex1?m%@X=v_*zfxu}W}L z&VGW|JLEZ3aClQ>4yOF01P?pplMlQnIZtCeRlRzOm-)<-^3d9m-pGyiT%vISj)Ryp z?Q2QLTH*7%8D5V6na@hyCVVyspUVZmQ|Qm!ujwxpd^6(`iMc$>d@@w0qh0(-@a>L% z_+`d3Ri;B z+|q!PUc7H;{=5bhylDT@p6nr0_~bkI3>7{rZ`6E@ozu_3l$}{ zCkgJAe6vtSI;I1s^3NaRfd7jrk}YTzc4fZ9r5M&fS#Tc zoX^R_fcIo?1&pVv*<#P;J?J#S)4%X?`FOoALT3S|eqfhloUJ?t|2pAgPtkn7U~ZV5 z$9ytXSnSZ$cd5{?IYZM=7y1=Kzroa31aXzn-=CrB`%49iaG&I}`PF#&+#-BB1vh#* z{TSom9m4;O3eBJQw?dgV89qBT|K3v02Y_cuIQByOkCEKMj{fRDg#QgiUM628iM9*A zTfQ5Z=bYCVkL9ex9}@qB3{@ul4aEV%Nneis^T%WG>6fDAwoB>-GCtB7@BU6}?C=EO zWY729;bl6SK1fHl@M(7Fw@~PRl6u{%$<;)r&rn+&LvB|yo}u=MelvysI^nZQ+HaQN8wK|XZtU|h!K>uEQ?1ZH&-}sl z_4soBS#ZmN?-bl4I9{Lmp#7(N>Sw+X`WmShxLDq=vH$VF$*#VZae1)V z)nuXf3V&m_Qv|=l!KX~{phNHTh5w!M-5@CCJYVRmg#QY`3n3p5SkcDhOUDEYpm?<)16&>!+@g!j5c-cJZ_ zeWh{UD*||@@Yx{kD;pRcI|M)Mum{>Vo$Tg#RwF2V*}+fRlbbf(v_8QaLkPT92>lA7H~rY<27gQI(a7N{!Ogl{^IiQ~ z!Jl==;b!2Z_l?);eEUoJHwwN??9=qaj~o7P$LIUB(2sas^Wi;kz-t^56907~=Lw?6 zPUe%Lo|5)r%KstrkwU~=wjBe1hxufxJ011<;28AepMc79t@M-qBo7qXVes@?P@`(z5`fa-WnWD#Kf`?Ag_#~lU#r!kWVaNB? zwM;KWF_%qDpQ#$9oWfo`DEJnVlIb|f%nFDY0`_5@mJ@98OQv+I#rFlRU<~ugM~ii zkk3e_kI7Ji6Nnzq`Of~oRQRV!z0C9E65;Qa@|b?OT<{i0zUK+P(9s`O3IDHT+`nEF z84!HunYvzuQqE@K^LvN<+XcVE!T%D*GgQ5dzowikg?@#D&(*-Gz4u-Y<9@*t<@b@X8di@AK4G_)kE`M=*{##$5ghM3Gd+vizc+xjq|rQ6c$cw zs1Fneo0=9cs$W`H-Cox*t|mVRliPE6iR*tq)m@WeR$O&0yt(Iw;Qp-@Axy=?1kYyp zwu28+n*E4*eA*?OU4u!$5!=_+0UwFYVfG%FJ0ZVlLeE5)&Kqp7*|#$0^hH~js6ZNxT;#*X}j-=G0LVe{q!*gs*lqFtuf3lw7aojw_fj7Ebqk zVU)}^&bo5P7Ec_fXg)FKp5~4lJF!^(f2#&lE}_ObKsYomPScVV8U{eTFJEzwxcKp@c7OlmcRhlAP zan5`-*AA%=rawpOu@Hnz2lJ*Et8iPCrp$W1XU&>1rPRh`{oHXnx!=YdVKo~w)I)w% z*Ve!;0jbiewmBSKg30<=xDml*V$3g%s!F?rnUZr~RTGGid0?6~T!Gs2&c(FQ)}TMU zBtDm5WxcP4jfEW-lIK=XHHYJ=;E0-L!>S18=AtGu3*m5$r_+kRL-NQWncKvm2upE6CAl~k75bLJ`Ii#-%3W3dLTs2MY-BQQ7cgrYF59HP)= zjKW*8AM@Kuh4l_grAg#u!trG!kI8Bdl4+?e3Sk2O!iDH%cxegANLy!32yVeufZZye zUs6%2+8ZJ|&pEA?q;I$_r&SA>uZ}Ysa<^|k?%&uBQLLlOB`yJNzb_0YthL;WwT03C z{LMAA0E7k^ZpSU!nCnPZ(4SV3Hl5P)Iq=mP38McaFU%?&h7;FXf1`HbO?H9q!clRU zmmO(r2&#!Rner zL0vG6Nb_fxPo0Kt5(1%hdC(O)W@EO;OR$M(_%V-@+YbuPMK zzq;t!wMHYziQVl+F*XGnI@I|=HJ=1Nom?cB*z>UZ56wtFy+mLkt!PcYKy7r1I=@~` z_u(ESNR2;&jsoV3g+IX%wSE<70>@bE2 zNEWXIxmlo{?gnV_l?nu)j{11I2tT}-4jw~}?&ucRH~8yy!|ig)Tv-Vnkb1}|=n`3q zg*u@}hlWsUg%9%%}dqNC@JDTVXhtrbQ%S5~3z5#K5aZV~Qh$h8MN{@XOt( ztzVaf6v~-!>A0W5=sX`!Yb-b{m8!89`!I}mK)B#UR@I_P>#^>N9yF^X5wUeJs^bQX zu9zJfLxku^+k$WtUJX&BrTN2cFn8|W+akU?@y!j3XbVMsusx%Q)-G44su{~5<|bJxs>vzYR}3sC_%Dr!7cb0j!ZbK$NrH7-z6@lvZ`dTSc&TvF>20rc{i8mPI_3Uq30* z6Rmlg-2@AS$sKbI~p9>&`5!zRZ7vC8Zgu^^0oU^fL8>?C%5hS zvrFaSSU=tCCfI;C8LSCH_eLupG1zG5<`^@eQuLBduv&jDjb?s4MxwGf&-QgxhiaD4 z2&MZ-j9=QBI+AglCAY^mm6%q3p|8Me2W(PXYdx+ZjJfsH3a5~$M6}u*xf?}?&SR?d z-Gz9XV!2BkEj-$azxXP)n0~T4)B+Q2;WewapPqK?YU;$g$&2v#VRJ8tZY_#uItME* zseVR|D3u#o(u|7Yir$*9^(F*8)wYIJE*_+7b4#Yo$icXwaAPV zi=*Ey>8Rqf))57r^=|=2>8H?59A^F8rzX9~kK{iH|IYNk0!A{S^3h?|*_Gk@6df7* z(sdTKbj8~dicN3U<5fxe3R5vj;c;9qb)+}H_ihow6Mm8ej&ufH?MQFdWxn1|Yg*K3 z$XQlh5d_vqdQ(iZ4sf5O&&-dd?v|fHZ*rtJ>je*=sq-h_ + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* safety: half-open prevention */ +ltl phi1 { + always ( leftClosed implies !rightEstablished ) +} diff --git a/tests/tcp/tcp-phi2.pml b/tests/tcp/tcp-phi2.pml new file mode 100644 index 0000000..d423edc --- /dev/null +++ b/tests/tcp/tcp-phi2.pml @@ -0,0 +1,149 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: verifying connection establishment */ +ltl phi2 { + ( (always ( eventually ( state[0] == 1 && state[1] == 2 ) ) ) + implies ( eventually ( state[0] == 4 ) ) ) diff --git a/tests/tcp/tcp-phi2.pml.trail b/tests/tcp/tcp-phi2.pml.trail new file mode 100644 index 0000000..319ff39 --- /dev/null +++ b/tests/tcp/tcp-phi2.pml.trail @@ -0,0 +1,55 @@ +-2:2:-2 +-4:-4:-4 +1:0:121 +2:1:114 +3:0:121 +4:1:115 +5:0:121 +6:1:116 +7:0:121 +8:1:117 +9:0:121 +10:3:0 +11:0:121 +12:3:1 +13:0:121 +14:3:2 +15:0:121 +16:3:9 +17:0:121 +18:2:0 +19:0:121 +20:2:1 +21:0:121 +22:2:2 +23:0:121 +24:2:9 +25:0:121 +26:3:17 +27:0:121 +28:3:1 +29:0:121 +30:3:3 +31:0:121 +32:3:22 +33:0:119 +34:2:17 +35:0:126 +36:2:1 +37:0:121 +38:2:3 +39:0:121 +40:2:22 +41:0:121 +42:2:42 +43:0:121 +44:2:1 +-1:-1:-1 +45:0:121 +46:2:2 +47:0:121 +48:2:9 +49:0:119 +50:2:17 +51:0:126 +52:2:1 diff --git a/tests/tcp/tcp-phi3.pml b/tests/tcp/tcp-phi3.pml new file mode 100644 index 0000000..b1e9e80 --- /dev/null +++ b/tests/tcp/tcp-phi3.pml @@ -0,0 +1,167 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: no infinite stalls/deadlocks */ +ltl phi3 { + !(eventually (((always (state[0] == SynSentState)) || + (always (state[0] == SynRecState)) || + (always (state[0] == EstState)) || + (always (state[0] == FinW1State)) || + (always (state[0] == CloseWaitState)) || + (always (state[0] == FinW2State)) || + (always (state[0] == ClosingState)) || + (always (state[0] == LastAckState)) || + (always (state[0] == TimeWaitState))) + && + ((always (state[1] == SynSentState)) || + (always (state[1] == SynRecState)) || + (always (state[1] == EstState)) || + (always (state[1] == FinW1State)) || + (always (state[1] == CloseWaitState)) || + (always (state[1] == FinW2State)) || + (always (state[1] == ClosingState)) || + (always (state[1] == LastAckState)) || + (always (state[1] == TimeWaitState))))) +} diff --git a/tests/tcp/tcp-phi4.pml b/tests/tcp/tcp-phi4.pml new file mode 100644 index 0000000..3ca2932 --- /dev/null +++ b/tests/tcp/tcp-phi4.pml @@ -0,0 +1,156 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: simultanous open */ +ltl phi4 { + always ( + (state[0] == SynSentState && + state[1] == SynSentState) + + implies + + ((eventually state[0] == EstState) && + (eventually state[1] == EstState))) +} diff --git a/tests/tcp/tcp-phi4.pml.trail b/tests/tcp/tcp-phi4.pml.trail new file mode 100644 index 0000000..08508a0 --- /dev/null +++ b/tests/tcp/tcp-phi4.pml.trail @@ -0,0 +1,43 @@ +-2:2:-2 +-4:-4:-4 +1:0:122 +2:1:114 +3:0:122 +4:1:115 +5:0:122 +6:1:116 +7:0:122 +8:1:117 +9:0:122 +10:3:0 +11:0:122 +12:3:1 +13:0:122 +14:3:2 +15:0:122 +16:3:9 +17:0:122 +18:2:0 +19:0:122 +20:2:1 +21:0:122 +22:2:2 +23:0:122 +24:2:9 +25:0:122 +26:3:17 +27:0:122 +28:3:1 +29:0:122 +30:3:3 +31:0:122 +32:3:22 +33:0:122 +34:2:17 +35:0:122 +36:2:1 +37:0:122 +38:2:3 +39:0:122 +40:2:22 +41:0:119 diff --git a/tests/tcp/tcp-phi5.pml b/tests/tcp/tcp-phi5.pml new file mode 100644 index 0000000..e675b63 --- /dev/null +++ b/tests/tcp/tcp-phi5.pml @@ -0,0 +1,158 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: SYN_RECEIVED resolution*/ +ltl phi5 { + always ( + (state[0] == SynRecState) + implies ( + eventually ( + (state[0] == EstState || + state[0] == FinW1State || + state[0] == ClosedState) + ) + ) + ) +} diff --git a/tests/tcp/tcp-phi6.pml b/tests/tcp/tcp-phi6.pml new file mode 100644 index 0000000..fc14aeb --- /dev/null +++ b/tests/tcp/tcp-phi6.pml @@ -0,0 +1,154 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* safety: strict closing transitions */ +ltl phi6 { + always ( + (state[0] == ClosingState) + implies + (next (state[0] == ClosingState || + state[0] == ClosedState)) + ) +} diff --git a/tests/tcp/tcp.pml b/tests/tcp/tcp.pml new file mode 100644 index 0000000..be7125b --- /dev/null +++ b/tests/tcp/tcp.pml @@ -0,0 +1,144 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +}