From eccbe4095ffea56f2e95bd3806eaa81c183cc603 Mon Sep 17 00:00:00 2001 From: Jake Ginesin Date: Sun, 3 May 2026 00:17:08 -0400 Subject: [PATCH] initial commit --- README.md | 59 +---- TUTORIAL.md | 101 ++++++++ .../model_generate.cpython-313.pyc | Bin 17683 -> 17690 bytes src/__pycache__/utility.cpython-313.pyc | Bin 7113 -> 7562 bytes src/main-old.py | 146 ------------ src/main.py | 3 +- tests/abp.yaml | 9 + tests/paper-attempt1.yaml | 216 ------------------ tests/paper.yaml | 109 --------- tests/{paper-attempt2.yaml => tcp.yaml} | 0 tests/tcp/README.md | 2 + tests/tcp/attempt1/tcp-phi1.pml | 143 ------------ tests/tcp/attempt1/tcp-phi2.pml | 143 ------------ tests/tcp/attempt1/tcp-phi2.pml.trail | 43 ---- tests/tcp/attempt1/tcp-phi3.pml | 161 ------------- tests/tcp/attempt1/tcp-phi3.pml.trail | 62 ----- tests/tcp/attempt1/tcp-phi4.pml | 150 ------------ tests/tcp/attempt1/tcp-phi4.pml.trail | 157 ------------- tests/tcp/attempt1/tcp-phi5.pml | 152 ------------ tests/tcp/attempt1/tcp-phi5.pml.trail | 64 ------ tests/tcp/attempt1/tcp-phi6.pml | 148 ------------ tests/tcp/attempt1/tcp-phi6.pml.trail | 88 ------- tests/tcp/attempt1/tcp.pml | 138 ----------- tests/tcp/no-network/tcp-phi1.pml | 149 ------------ tests/tcp/no-network/tcp-phi2.pml | 149 ------------ tests/tcp/no-network/tcp-phi2.pml.trail | 55 ----- tests/tcp/no-network/tcp-phi3.pml | 167 -------------- tests/tcp/no-network/tcp-phi4.pml | 156 ------------- tests/tcp/no-network/tcp-phi4.pml.trail | 43 ---- tests/tcp/no-network/tcp-phi5.pml | 158 ------------- tests/tcp/no-network/tcp-phi6.pml | 154 ------------- tests/tcp/no-network/tcp.pml | 144 ------------ tests/tcp/pan | Bin 110664 -> 0 bytes tests/tcp/tcp-phi4.pml.trail | 192 ---------------- tests/tcp/tcp-phi6.pml.trail | 102 --------- 35 files changed, 125 insertions(+), 3438 deletions(-) create mode 100644 TUTORIAL.md delete mode 100644 src/main-old.py create mode 100644 tests/abp.yaml delete mode 100644 tests/paper-attempt1.yaml delete mode 100644 tests/paper.yaml rename tests/{paper-attempt2.yaml => tcp.yaml} (100%) create mode 100644 tests/tcp/README.md delete mode 100644 tests/tcp/attempt1/tcp-phi1.pml delete mode 100644 tests/tcp/attempt1/tcp-phi2.pml delete mode 100644 tests/tcp/attempt1/tcp-phi2.pml.trail delete mode 100644 tests/tcp/attempt1/tcp-phi3.pml delete mode 100644 tests/tcp/attempt1/tcp-phi3.pml.trail delete mode 100644 tests/tcp/attempt1/tcp-phi4.pml delete mode 100644 tests/tcp/attempt1/tcp-phi4.pml.trail delete mode 100644 tests/tcp/attempt1/tcp-phi5.pml delete mode 100644 tests/tcp/attempt1/tcp-phi5.pml.trail delete mode 100644 tests/tcp/attempt1/tcp-phi6.pml delete mode 100644 tests/tcp/attempt1/tcp-phi6.pml.trail delete mode 100644 tests/tcp/attempt1/tcp.pml delete mode 100644 tests/tcp/no-network/tcp-phi1.pml delete mode 100644 tests/tcp/no-network/tcp-phi2.pml delete mode 100644 tests/tcp/no-network/tcp-phi2.pml.trail delete mode 100644 tests/tcp/no-network/tcp-phi3.pml delete mode 100644 tests/tcp/no-network/tcp-phi4.pml delete mode 100644 tests/tcp/no-network/tcp-phi4.pml.trail delete mode 100644 tests/tcp/no-network/tcp-phi5.pml delete mode 100644 tests/tcp/no-network/tcp-phi6.pml delete mode 100644 tests/tcp/no-network/tcp.pml delete mode 100755 tests/tcp/pan delete mode 100644 tests/tcp/tcp-phi4.pml.trail delete mode 100644 tests/tcp/tcp-phi6.pml.trail diff --git a/README.md b/README.md index 35b08b9..35b00e3 100644 --- a/README.md +++ b/README.md @@ -1,50 +1,15 @@ -# Korg, reborn +# Automated Channel Fault Analysis with Tofu -# TODO: -- [x] nix flake here -- [x] fix weird spin errors(?) - - jake note: pinned specific working SPIN version using Nix -- [x] add attackers that only do specifically n queries - - limitation: you cannot choose only *n* queries for the dropping attacker; trace violations can happen at any time -- [x] add attackers to do <= n queries -- [x] add attackers that can do attacks with an unbounded number of messages -- [x] add a test suite -- [x] make the impl more robust; do more SWE -- [x] add no self-deadlock experiments - - I envision this would be: providing an eventually-style LTL query, sending messages onto an open channel, and asserting that the gadget doesn't somehow deadlock with itself -- [ ] support queries over multiple properties -- [ ] add raft, TCP, SCTP, ABP experiments from old Korg impl to the test suite -- [ ] add labels on trace logging to gadgets -- [ ] modify the paper? spin workshop? +## Installation and Tests +- Install nix +- Run `nix develop` +- Execute the test harnesses with `test_harness.py`: -# Notes -- Sound and complete attack discovery for replay, dropping, and reordering attacks on channels - - possible because of the finite-state modeling spin does. Indeed, we can model no-limit attackers within the finite-state model, giving guarantees of decidability and complexity. -- Limiting the number of messages a drop/replay/reorder attacker can reason about has the ability to significantly reduce the searchspace, especially when dealing with larger models. Although KORG is always decidable, sound, and complete, using the unbounded attacker is inadvisable in practice because spin must reason about *all* such permutations of possible drop, replay, and reorder sequences, thereby increasing the search space factorially. -- One explicit limitation of the replay attacker is not being able to transition back to listening for packets after replaying -- Maybe change the title to: Korg: Automated analysis of channel faults -- The inclusion of the pass on chan functionality is required to ensure liveness properties are not trivially violated by an attacker gadget that loops with itself. Thus the pass on chan functionality is the best possible "wait" we could think up. We also include no deadlock tests. +``` +$ test_harness tests/tcp.yaml # TCP tests +$ test_harness tests/abp.yaml # ABP tests +$ test_harness tests/tests.yaml # general correctness tests +``` +Each test comes with a description - check out the respective YAML files -# Gadget Structures - -Drop: -- drop msg off chan -- pass on chan - -Replay: -:CONSUME: -- consume msg; may go to CONSUME or REPLAY -- pass on chan -:REPLAY: -- replay msg -- pass on chan -- pass on chan, then go to REPLAY - -Reorder: -:INIT: -- pass msg on chan -- go to CONSUME -:CONSUME: -- consume n messages on chan, then go to REPLAY -:REPLAY: -- replay msg +A full tutorial is available in [TUTORIAL.MD](TUTORIAL.MD) diff --git a/TUTORIAL.md b/TUTORIAL.md new file mode 100644 index 0000000..8afad2d --- /dev/null +++ b/TUTORIAL.md @@ -0,0 +1,101 @@ +# Tutorial + +Tofu synthesizes attacker gadgets (drop / replay / reorder) on top of an existing Promela model, then hands the combined model to Spin. If the LTL property breaks, the attacker found an attack. + +## Setup + +``` +$ nix develop +``` + +The flake pins `nixpkgs` and a specific `spin` revision (see `flake.lock`), so the toolchain is reproducible across machines. + +## CLI + +``` +python src/main.py \ + --model=.pml \ + --attacker={drop,replay,reorder} \ + --chan=[,...] \ + --mem= \ + --output=.pml \ + [--eval] [--cleanup] [--nocheck] +``` + +- `--mem` bounds the attacker's memory (number of messages it can buffer / drop). Use `unbounded` to remove the bound. +- `--chan` accepts a comma-separated list. Multi-channel arrays use `name:i` or `name:a-b`. +- `--eval` runs Spin on the output. `--cleanup` removes Spin artifacts (`pan*`, `*.trail`, `_spin_nvr.tmp`) and the output `.pml` after evaluation. + +## Writing a Model + +A model has three parts: a channel, a consumer that walks a state machine on that channel, and an LTL property. + +Save as `tests/example/tut.pml`: + +```promela +// INTENDED BEHAVIOR: violation under replay, mem=1 +chan c = [8] of { byte }; +byte q = 1; + +init { + c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC1; + od +PROC1: + do + :: c ? 5 -> goto PROC2; + od +PROC2: + q = 0; +} + +ltl proc { + always !(q == 0); +} +``` + +The honest channel only carries one `5`, so `consume` should stall at `PROC1`. A replay attacker with `mem=1` can re-emit the consumed `5`, advancing the consumer to `PROC2` and falsifying the property. + +## Running the Tool + +``` +$ python src/main.py --model=tests/example/tut.pml \ + --attacker=replay --chan=c \ + --output=temp.pml --mem=1 --eval --cleanup +``` + +Outputs to look for in Spin's report: + +| Spin output | Meaning | +|------------------------|------------------------------------------------------------------| +| `assertion violated` | LTL safety property violated (attack found) | +| `acceptance cycle` | LTL liveness violated (attacker stalls progress) | +| neither | No violation; attacker (at this `--mem`) cannot break the model | + +For the model above, expect a property violation. Drop `--mem` to `0` or switch to `--attacker=drop` and the violation disappears — the attacker no longer has the budget. + +## Test Harness + +Each `tests/*.yaml` entry pins a command and its intended outcome: + +```yaml +my-test: + - command: python src/main.py --model=tests/example/tut.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replay attacker can re-emit the consumed 5 +``` + +Run the suite: + +``` +$ python test_harness.py tests/tests.yaml +$ python test_harness.py tests/tcp.yaml +$ python test_harness.py tests/abp.yaml +``` + +The harness diffs Spin's verdict against `intended` and prints a pass/fail summary. diff --git a/src/__pycache__/model_generate.cpython-313.pyc b/src/__pycache__/model_generate.cpython-313.pyc index 7ed32cee091116c66de5b9222b6d959b3ee2ebc8..7cdfc4b02bfb15cbe2d0c2a970ff17cfd6d1d8a1 100644 GIT binary patch delta 51 zcmbQ-#W<^rk^3_*FBbz4q&02c$UTvV(RuP*9vQ*n#I)4p{M-WF#G;bSw8Z3+&4+mc FEC7~U5ZV9$ delta 44 ycmbQ$#W=Z(k^3_*FBbz4uvu=}$UTvV(Pr{o9vQC0qT-yyJl(w1^3A7s0xSR(T@6?O diff --git a/src/__pycache__/utility.cpython-313.pyc b/src/__pycache__/utility.cpython-313.pyc index 83e6ed044ec424bdaf6dbc7f885772f6a2e337cb..b800d061b0ab975f98c855f26e884f3d9d0ab558 100644 GIT binary patch delta 987 zcmX?U-et}AnU|M~0SMBXHfN?vY~*8PVzikoz$7DBoS2rHoS$2un^;tmnUFg(sAd7X59pN13pqt6Z(t4Qa%c4QU;ui`*LyNAn=Kp2_LoeP1K0w& zS<{R1OABr>XXcemUc=TT$O4pWV7S3A*x+$PRJ_6O&SZOb6{Q>e!kslUGj0frPq&(A zH6wAl?L^xZEbF;ea&0hN&%2U$C&%Pub_W#!5dx}iNXboJ%5KHiY z2b;-n*%g#Npu_<%9+;u=V8XzV2l5f)dM6K|FR` z5BOy-@~hqyka#wEB2O0Mt;v6QWtouAUz;@fy);#{WXYDgi*9e9~dqG-bD39 delta 710 zcmeCOK55SPnU|M~0SM~n{L6SIzLAfSiP3bj0Fw+?Vo`BUVxDeZYWZecCT1pyTZ{}0 zQyB~x@)&`bDU?B&!Q%k~LmugW1VUMYI43iT z3QvB`%E@C2Gy()7RG@vY=KFww!S~VRXKc1? zOh98^GEUZH59DUf%qzLYnqHJ&S}?hly-Dx@P^y992ESl~#|=^O2EW^rB{)-<3jeJOfXX@ ziz&!{Ajo4y@+vDfubLt}G&zb(m#G8d)m2;q0vZrA7!rek;lzee#{%a70}a7Z=l0=b z@_o#}Ajc5RKDmxth0Pb}KHuMy*KlVtI&2o>nZzh<3N*4f0vOD&01y^!@IeU$*~w~r zij4Or2l8bx-kiLLPhR>mkHSYbPqu8fScCqI+1Ntb05 znPL2a0Z1)0S#0(N#Q0z*$EY;J`2z!xS{Sl8Y-PymunQ_CUqJj14vbuk!Hf%-KQMsk i6)a!C^amMzMsG%t9uU32 None: - msg=( - "Usage: \n" - " python main.py [arguments] \n\n" - "Arguments: \n" - " --model=path/to/model.pml Promela model to generate attackers on\n" - " --attacker=[replay,drop,reorder] \n" - " --chan=[chan1, chan2:int, ...] Channels to synthesize attackers on. When specifying over ranges of\n" - " channels, you can give ranges or a list of values\n" - " --nocheck Don't check channel validity\n" - # " --nchan=[nat, nat, ...] If the channel is a set of channels, how many attackers to synthesize?\n" - " --mem=[num] Size of memory. Defaults to '3' \n" - " --mem=unbounded Use the unbounded memory gadget version (not recommended)\n" - " --output=path/to/file.pml Output file name\n" - " --eval Evaluate the outputted file with Spin\n" - " --cleanup Clean up the extra files spin creates, including Korg's \n" - ) - print(msg) - - # assert "syntax error" not in stdout, "there seems to be a syntax error in the model" - # assert "processes created" in stdout, "the spin model creates no processes ... check to see if it compiles" - -def main() -> None: - args = sys.argv[1:] - if len(args) == 0 or args[0] in ["help", "--help", "-h", "-help"]: - show_help() - sys.exit() - - mem = 3 # default - - for arg in args: - if arg.startswith("--model="): - model_path = arg.split("=", 1)[1] - elif arg.startswith("--attacker="): - attacker = arg.split("=", 1)[1] - elif arg.startswith("--mem="): - mem_read = arg.split("=", 1)[1] - elif arg.startswith("--chan="): - chans = arg.split("=", 1)[1] - elif arg.startswith("--output="): - out_file = arg.split("=", 1)[1] - - if "--eval" in args and not "--output" in args: - out_file = "korg-promela-out.pml" - - if not model_path or not attacker or not mem or not chans or not out_file: - print("error: all arguments are required. \n") - show_help() - sys.exit(1) - - unbounded = mem_read == "unbounded" - if not unbounded : mem = int(mem_read) - - ensure_compile(model_path) - model = fileRead(model_path) - - channels = parse_channels(fileReadLines(model_path)) - mchannels, mchannel_len = parse_mchannels(fileReadLines(model_path)) - model_with_attacker = str; - assert mem >= 0, "memory value must be positive" - - chans_togen = set() - - # first, process the input - mc = chans.split(",") - for chan in mc: - if ":" in chan: - name, num_extr = chan[:chan.index(":")], chan[chan.index(":")+1:] - if "-" in num_extr: - a, b = list(map(lambda a: int(a), num_extr.split("-"))) - assert a < b - assert a >= 0 - assert b < mchannel_len[name] - for i in range(a,b+1): - chan_name = str(name) + "[" + str(i) + "]" - chans_togen.add(chan_name) - channels[chan_name] = mchannels[name] - else: - a = int(num_extr) - assert a >= 0 - assert a < mchannel_len[name] - chan_name = str(name) + "[" + str(a) + "]" - chans_togen.add(chan_name) - channels[chan_name] = mchannels[name] - - else : chans_togen.add(chan) - - print(chans_togen) - - for i in range(len(chans_togen)): - chan = list(chans_togen)[i] - - if not "--nocheck" : assert chan in channels, "can't find "+str(chan)+" in model" - - match attacker: - case "replay": - if unbounded : attacker_gadget = gen_replay_unbounded(chan, channels[chan], i) - else : attacker_gadget = gen_replay(chan, channels[chan], mem, i) - case "drop": - if unbounded : attacker_gadget = gen_drop_unbounded(chan, channels[chan], i) - else : attacker_gadget = gen_drop(chan, channels[chan], mem, i) - case "reorder": - if unbounded : attacker_gadget = gen_reorder_unbounded(chan, channels[chan], i) - else : attacker_gadget = gen_reorder(chan, channels[chan], mem, i) - case _: - print("error: inputted an invalid attacker model. \n") - sys.exit(1) - - if model.rindex("};") >= model.rindex("}"): - model = model[:model.rindex("};")+2] + "\n\n" + attacker_gadget + "\n" + model[model.rindex("};")+2:] - else: - model = model[:model.rindex("}")+1] + "\n\n" + attacker_gadget + "\n" + model[model.rindex("}")+1:] - - # Write the modified model to the output file - with open(out_file, 'w') as file: - file.write(model) - - if "--eval" in args: - print() - print("generated Promela file with attacker model gadget... now running SPIN on "+str(out_file) + "!\n") - eval_model(out_file) - - if "--cleanup" in args: - print("\nCleaning up Spin files...") - cleanup_spin_files() - try: - os.remove(out_file) - print(f"Removed: {out_file}") - except OSError: - pass - - -if __name__== "__main__": - main() diff --git a/src/main.py b/src/main.py index a7b1b79..fce6774 100644 --- a/src/main.py +++ b/src/main.py @@ -1,6 +1,5 @@ # ============================================================================== -# Author : Jake Ginesin -# Authored : 14 June 2024 +# Author : [redacted] # Purpose : synthesize attacker gadgets for attackers that can drop, # replay, and reorder messages on a channel # ============================================================================== diff --git a/tests/abp.yaml b/tests/abp.yaml new file mode 100644 index 0000000..1ad576d --- /dev/null +++ b/tests/abp.yaml @@ -0,0 +1,9 @@ +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 diff --git a/tests/paper-attempt1.yaml b/tests/paper-attempt1.yaml deleted file mode 100644 index 3bc8ec1..0000000 --- a/tests/paper-attempt1.yaml +++ /dev/null @@ -1,216 +0,0 @@ -# --- PHI 1: HALF-OPEN PREVENTION --- - -tcp-phi1-drop-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: property violation - - explanation: Dropping A's FIN allows A to eventually time out to Closed while B remains stranded in Established. - -tcp-phi1-drop-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=0 - - intended: no violation - - explanation: Attacker has 0 memory budget; normal teardown prevents half-open states. - -tcp-phi1-replay-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: property violation - - explanation: Replaying a stale SYN from A forces B into an Established state while A is completely Closed. - -tcp-phi1-replay-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=BtoA --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: Replaying B's final teardown ACK is idempotent and harmlessly dropped by A, maintaining state sync. - -tcp-phi1-reorder-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoB --output=temp.pml --eval --cleanup --mem=2 - - intended: property violation - - explanation: Reordering A's SYN and FIN segments desynchronizes B's state machine, triggering a half-open state. - -tcp-phi1-reorder-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: Reorder attacker requires at least mem=2 to swap messages; mem=1 is insufficient. - - -# --- PHI 3: NO DEADLOCKS --- - -tcp-phi3-drop-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=BtoA --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: Dropping B's SYN-ACK stalls A in SynSent and B in SynRec indefinitely without timeout recovery. - -tcp-phi3-drop-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=0 - - intended: no violation - - explanation: Zero memory prevents dropping, allowing standard timers and handshakes to resolve without deadlocks. - -tcp-phi3-replay-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: Replaying FIN messages traps the receiver in an infinite loop of CloseWait/LastAck processing. - -tcp-phi3-replay-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=replay --chan=BtoA --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: Replaying an ACK during the Established state is cleanly ignored and does not halt liveness progress. - -tcp-phi3-reorder-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=reorder --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=2 - - intended: acceptance cycle - - explanation: Swapping handshake messages (ACK before SYN) deadlocks both endpoints in intermediate waiting states. - -tcp-phi3-reorder-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=reorder --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: Attacker lacks the mem=2 budget required to execute a reorder attack. - - -# --- PHI 5: SYN_RECEIVED RESOLUTION --- - -tcp-phi5-drop-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: Dropping the final ACK of the 3-way handshake prevents B from ever resolving SynRec to Established. - -tcp-phi5-drop-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=0 - - intended: no violation - - explanation: Without drop capabilities, the ACK arrives normally, resolving the SynRec state. - -tcp-phi5-replay-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: Replaying a SYN forces B to repeatedly trigger simultaneous open logic, preventing resolution. - -tcp-phi5-replay-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: Replaying the final ACK simply provides redundant resolution signals, which satisfies the property. - -tcp-phi5-reorder-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=reorder --chan=AtoB --output=temp.pml --eval --cleanup --mem=2 - - intended: acceptance cycle - - explanation: Delivering A's final ACK before B has fully entered SynRec confuses the state machine, stalling resolution. - -tcp-phi5-reorder-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=reorder --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: Insufficient memory to reorder packets; handshakes process chronologically. - - -# --- PHI 6: STRICT CLOSING TRANSITIONS --- - -tcp-phi6-drop-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: property violation - - explanation: Dropping the ACK to the FIN causes a timeout that bypasses the strict Closing-to-Closed state sequence. - -tcp-phi6-drop-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=0 - - intended: no violation - - explanation: Normal termination proceeds; Closing transitions accurately based on protocol rules. - -tcp-phi6-replay-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: property violation - - explanation: Replaying a FIN while in Closing forces an invalid transition to TimeWait instead of Closed. - -tcp-phi6-replay-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=0 - - intended: no violation - - explanation: 0 memory prevents injection of unexpected packets during the tear-down phase. - -tcp-phi6-reorder-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=reorder --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=2 - - intended: property violation - - explanation: Swapping FINs during a simultaneous close alters the ACK delivery timing, violating the strict sequence. - -tcp-phi6-reorder-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=reorder --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: Mem=1 prevents the reordering of the close-sequence messages. - -# --- PHI 7: SIMULTANEOUS CLOSE RESOLUTION --- - -tcp-phi7-drop-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi7.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: Dropping a FIN during a simultaneous close prevents one side from transitioning out of FinW1State. - -tcp-phi7-drop-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi7.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=0 - - intended: no violation - - explanation: Zero memory prevents message dropping; both endpoints successfully reach ClosedState. - -tcp-phi7-replay-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi7.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: Replaying stale FINs traps the endpoint in a continuous processing loop, halting progress to ClosedState. - -tcp-phi7-replay-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi7.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=0 - - intended: no violation - - explanation: Without replay capabilities, the simultaneous close resolves chronologically. - -tcp-phi7-reorder-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi7.pml --attacker=reorder --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=2 - - intended: acceptance cycle - - explanation: Swapping FIN and ACK segments out of order desynchronizes the simultaneous close, causing a deadlock. - -tcp-phi7-reorder-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi7.pml --attacker=reorder --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: Mem=1 is insufficient to execute a reorder attack. - - -# --- PHI 8: ACTIVE CLOSE EVENTUALLY TERMINATES --- - -tcp-phi8-drop-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi8.pml --attacker=drop --chan=BtoA --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: Dropping the responder's ACK leaves the active closer permanently stranded in FinW1State. - -tcp-phi8-drop-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi8.pml --attacker=drop --chan=BtoA --output=temp.pml --eval --cleanup --mem=0 - - intended: no violation - - explanation: Normal teardown ensures the active closer receives its ACK and FIN. - -tcp-phi8-replay-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi8.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: acceptance cycle - - explanation: Replaying application data or FINs delays the final transition, breaking the eventual termination guarantee. - -tcp-phi8-replay-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi8.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=0 - - intended: no violation - - explanation: Normal sequence guarantees the active closer reaches ClosedState. - -tcp-phi8-reorder-violate: - - command: python src/main.py --model=tests/tcp/tcp-phi8.pml --attacker=reorder --chan=BtoA --output=temp.pml --eval --cleanup --mem=2 - - intended: acceptance cycle - - explanation: Delivering the responder's FIN before the ACK confuses the state machine logic in FinW1State, stalling termination. - -tcp-phi8-reorder-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi8.pml --attacker=reorder --chan=BtoA --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: Insufficient memory to alter the close sequence. - - -# --- PHI 9: HANDSHAKE CANNOT BE BYPASSED --- -# Note: This is a strict safety property guaranteed by the structure of the Promela model. -# The LISTEN state explicitly routes only to SYN_RECEIVED upon reading a SYN. -# No channel attacker (drop, replay, reorder) can force a direct jump to ESTABLISHED. - -tcp-phi9-drop-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi9.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: Dropping messages halts progress but cannot force an illegal structural transition from Listen directly to Established. - -tcp-phi9-replay-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi9.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: The model's Listen state only branches on SYN (transitioning to SynRec). Replaying ACKs or FINs results in skipped messages, not illegal state jumps. - -tcp-phi9-reorder-pass: - - command: python src/main.py --model=tests/tcp/tcp-phi9.pml --attacker=reorder --chan=AtoB --output=temp.pml --eval --cleanup --mem=2 - - intended: no violation - - explanation: Regardless of message order, the Promela model restricts ListenState exits exclusively to SynRecState. This safety property is structurally immune to channel manipulation. diff --git a/tests/paper.yaml b/tests/paper.yaml deleted file mode 100644 index 061fb04..0000000 --- a/tests/paper.yaml +++ /dev/null @@ -1,109 +0,0 @@ -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-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-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/paper-attempt2.yaml b/tests/tcp.yaml similarity index 100% rename from tests/paper-attempt2.yaml rename to tests/tcp.yaml diff --git a/tests/tcp/README.md b/tests/tcp/README.md new file mode 100644 index 0000000..580a47f --- /dev/null +++ b/tests/tcp/README.md @@ -0,0 +1,2 @@ +Note: +- we do not expect properties 2, 4, and 6 to hold under this model. diff --git a/tests/tcp/attempt1/tcp-phi1.pml b/tests/tcp/attempt1/tcp-phi1.pml deleted file mode 100644 index a95ba99..0000000 --- a/tests/tcp/attempt1/tcp-phi1.pml +++ /dev/null @@ -1,143 +0,0 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoB = [2] of { mtype }; -chan BtoA = [2] 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 -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(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 1); -} - -/* safety: half-open prevention */ -ltl phi1 { - always ( leftClosed implies !rightEstablished ) -} diff --git a/tests/tcp/attempt1/tcp-phi2.pml b/tests/tcp/attempt1/tcp-phi2.pml deleted file mode 100644 index 620854f..0000000 --- a/tests/tcp/attempt1/tcp-phi2.pml +++ /dev/null @@ -1,143 +0,0 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoB = [2] of { mtype }; -chan BtoA = [2] 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 -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(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 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/attempt1/tcp-phi2.pml.trail b/tests/tcp/attempt1/tcp-phi2.pml.trail deleted file mode 100644 index 745e3e2..0000000 --- a/tests/tcp/attempt1/tcp-phi2.pml.trail +++ /dev/null @@ -1,43 +0,0 @@ --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 --1:-1:-1 -29:0:121 -30:3:3 -31:0:121 -32:3:22 -33:0:119 -34:2:15 -35:0:126 -36:2:16 -37:0:119 -38:3:42 -39:0:126 -40:3:1 diff --git a/tests/tcp/attempt1/tcp-phi3.pml b/tests/tcp/attempt1/tcp-phi3.pml deleted file mode 100644 index 45f6418..0000000 --- a/tests/tcp/attempt1/tcp-phi3.pml +++ /dev/null @@ -1,161 +0,0 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoB = [2] of { mtype }; -chan BtoA = [2] 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 -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(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 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/attempt1/tcp-phi3.pml.trail b/tests/tcp/attempt1/tcp-phi3.pml.trail deleted file mode 100644 index bb2a009..0000000 --- a/tests/tcp/attempt1/tcp-phi3.pml.trail +++ /dev/null @@ -1,62 +0,0 @@ --2:3:-2 --4:-4:-4 -1:0:289 -2:2:122 -3:0:289 -4:2:123 -5:0:289 -6:2:124 -7:0:289 -8:2:125 -9:0:289 -10:4:0 -11:0:289 -12:4:1 -13:0:289 -14:4:2 -15:0:289 -16:4:9 -17:0:289 -18:3:0 -19:0:289 -20:3:1 -21:0:289 -22:3:2 -23:0:289 -24:3:9 -25:0:289 -26:4:17 -27:0:289 -28:4:1 -29:0:289 -30:4:3 -31:0:289 -32:4:22 -33:0:289 -34:1:116 -35:0:289 -36:1:117 -37:0:289 -38:3:10 -39:0:289 -40:3:11 -41:3:12 -42:0:289 -43:3:47 -44:0:249 -45:1:114 -46:0:599 -47:1:115 -48:0:599 -49:4:40 -50:0:599 -51:4:41 -52:0:599 -53:1:114 -54:0:599 -55:1:115 -56:0:599 -57:4:31 --1:-1:-1 -58:0:599 -59:0:599 diff --git a/tests/tcp/attempt1/tcp-phi4.pml b/tests/tcp/attempt1/tcp-phi4.pml deleted file mode 100644 index b34fa36..0000000 --- a/tests/tcp/attempt1/tcp-phi4.pml +++ /dev/null @@ -1,150 +0,0 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoB = [2] of { mtype }; -chan BtoA = [2] 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 -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(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 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/attempt1/tcp-phi4.pml.trail b/tests/tcp/attempt1/tcp-phi4.pml.trail deleted file mode 100644 index cf64d44..0000000 --- a/tests/tcp/attempt1/tcp-phi4.pml.trail +++ /dev/null @@ -1,157 +0,0 @@ --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:10 -35:0:122 -36:2:11 -37:2:12 -38:0:122 -39:3:23 -40:0:122 -41:3:24 -42:0:122 -43:3:25 -44:0:122 -45:3:55 -46:0:122 -47:3:56 -48:0:122 -49:3:66 -50:0:122 -51:2:47 -52:0:122 -53:2:48 -54:0:122 -55:2:55 -56:0:122 -57:2:56 -58:0:122 -59:3:67 -60:0:122 -61:3:68 -62:0:122 -63:3:94 -64:0:122 -65:2:66 -66:0:122 -67:2:67 -68:0:122 -69:2:68 -70:0:122 -71:3:95 -72:0:122 -73:3:110 -74:0:122 -75:3:1 -76:0:122 -77:3:2 -78:0:122 -79:2:94 -80:0:122 -81:2:95 -82:0:122 -83:2:110 -84:0:122 -85:2:1 -86:0:122 -87:2:3 -88:0:122 -89:3:9 -90:0:122 -91:3:10 -92:0:122 -93:3:11 -94:3:12 -95:0:122 -96:3:47 -97:0:122 -98:2:22 -99:0:122 -100:2:23 -101:0:122 -102:2:24 -103:0:122 -104:2:25 -105:0:122 -106:3:48 -107:0:122 -108:3:55 -109:0:122 -110:3:56 -111:0:122 -112:2:55 -113:0:122 -114:2:56 -115:0:122 -116:2:66 -117:0:122 -118:3:66 -119:0:122 -120:3:67 -121:0:122 -122:3:68 -123:0:122 -124:2:67 -125:0:122 -126:2:68 -127:0:122 -128:2:94 -129:0:122 -130:3:94 -131:0:122 -132:3:95 -133:0:122 -134:3:110 -135:0:122 -136:3:1 -137:0:122 -138:3:3 -139:0:122 -140:3:22 -141:0:122 -142:2:95 -143:0:122 -144:2:110 -145:0:122 -146:2:1 -147:0:122 -148:2:3 -149:0:122 -150:3:23 -151:0:122 -152:3:27 -153:0:122 -154:2:22 -155:0:119 diff --git a/tests/tcp/attempt1/tcp-phi5.pml b/tests/tcp/attempt1/tcp-phi5.pml deleted file mode 100644 index 3b65921..0000000 --- a/tests/tcp/attempt1/tcp-phi5.pml +++ /dev/null @@ -1,152 +0,0 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoB = [2] of { mtype }; -chan BtoA = [2] 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 -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(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 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/attempt1/tcp-phi5.pml.trail b/tests/tcp/attempt1/tcp-phi5.pml.trail deleted file mode 100644 index ad988b0..0000000 --- a/tests/tcp/attempt1/tcp-phi5.pml.trail +++ /dev/null @@ -1,64 +0,0 @@ --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:121 -34:2:10 -35:0:121 -36:2:11 -37:2:12 -38:0:121 -39:3:23 -40:0:121 -41:3:24 -42:0:121 -43:3:25 -44:0:121 -45:3:55 -46:0:121 -47:3:56 -48:0:121 -49:3:66 -50:0:121 -51:2:47 -52:0:119 -53:2:50 -54:0:126 -55:2:51 -56:0:126 -57:2:50 -58:0:126 -59:2:51 --1:-1:-1 -60:0:126 -61:0:126 diff --git a/tests/tcp/attempt1/tcp-phi6.pml b/tests/tcp/attempt1/tcp-phi6.pml deleted file mode 100644 index d0cf9a0..0000000 --- a/tests/tcp/attempt1/tcp-phi6.pml +++ /dev/null @@ -1,148 +0,0 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoB = [2] of { mtype }; -chan BtoA = [2] 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 -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(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 1); -} - -/* safety: strict closing transitions */ -ltl phi6 { - always ( - (state[0] == ClosingState) - implies - (next (state[0] == ClosingState || - state[0] == ClosedState)) - ) -} diff --git a/tests/tcp/attempt1/tcp-phi6.pml.trail b/tests/tcp/attempt1/tcp-phi6.pml.trail deleted file mode 100644 index 1840bcf..0000000 --- a/tests/tcp/attempt1/tcp-phi6.pml.trail +++ /dev/null @@ -1,88 +0,0 @@ --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:121 -34:2:10 -35:0:121 -36:2:11 -37:2:12 -38:0:121 -39:3:23 -40:0:121 -41:3:24 -42:0:121 -43:3:25 -44:0:121 -45:3:55 -46:0:121 -47:3:56 -48:0:121 -49:3:66 -50:0:121 -51:2:47 -52:0:121 -53:2:48 -54:0:121 -55:2:55 -56:0:121 -57:2:56 -58:0:121 -59:3:67 -60:0:121 -61:3:68 -62:0:121 -63:3:94 -64:0:121 -65:2:66 -66:0:121 -67:2:67 -68:0:121 -69:2:68 -70:0:121 -71:3:95 -72:0:121 -73:3:110 -74:0:121 -75:3:1 -76:0:121 -77:3:2 -78:0:121 -79:3:9 -80:0:121 -81:2:94 -82:0:121 -83:2:95 -84:0:119 -85:2:110 -86:0:126 diff --git a/tests/tcp/attempt1/tcp.pml b/tests/tcp/attempt1/tcp.pml deleted file mode 100644 index 1792fbe..0000000 --- a/tests/tcp/attempt1/tcp.pml +++ /dev/null @@ -1,138 +0,0 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoB = [2] of { mtype }; -chan BtoA = [2] 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 -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(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 1); -} diff --git a/tests/tcp/no-network/tcp-phi1.pml b/tests/tcp/no-network/tcp-phi1.pml deleted file mode 100644 index 243cfd0..0000000 --- a/tests/tcp/no-network/tcp-phi1.pml +++ /dev/null @@ -1,149 +0,0 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] 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: half-open prevention */ -ltl phi1 { - always ( leftClosed implies !rightEstablished ) -} diff --git a/tests/tcp/no-network/tcp-phi2.pml b/tests/tcp/no-network/tcp-phi2.pml deleted file mode 100644 index 960a173..0000000 --- a/tests/tcp/no-network/tcp-phi2.pml +++ /dev/null @@ -1,149 +0,0 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] 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/no-network/tcp-phi2.pml.trail b/tests/tcp/no-network/tcp-phi2.pml.trail deleted file mode 100644 index 319ff39..0000000 --- a/tests/tcp/no-network/tcp-phi2.pml.trail +++ /dev/null @@ -1,55 +0,0 @@ --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/no-network/tcp-phi3.pml b/tests/tcp/no-network/tcp-phi3.pml deleted file mode 100644 index 35a9049..0000000 --- a/tests/tcp/no-network/tcp-phi3.pml +++ /dev/null @@ -1,167 +0,0 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] 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/no-network/tcp-phi4.pml b/tests/tcp/no-network/tcp-phi4.pml deleted file mode 100644 index 68c2d48..0000000 --- a/tests/tcp/no-network/tcp-phi4.pml +++ /dev/null @@ -1,156 +0,0 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] 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/no-network/tcp-phi4.pml.trail b/tests/tcp/no-network/tcp-phi4.pml.trail deleted file mode 100644 index 08508a0..0000000 --- a/tests/tcp/no-network/tcp-phi4.pml.trail +++ /dev/null @@ -1,43 +0,0 @@ --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/no-network/tcp-phi5.pml b/tests/tcp/no-network/tcp-phi5.pml deleted file mode 100644 index 417ac59..0000000 --- a/tests/tcp/no-network/tcp-phi5.pml +++ /dev/null @@ -1,158 +0,0 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] 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/no-network/tcp-phi6.pml b/tests/tcp/no-network/tcp-phi6.pml deleted file mode 100644 index 2cf306a..0000000 --- a/tests/tcp/no-network/tcp-phi6.pml +++ /dev/null @@ -1,154 +0,0 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] 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/no-network/tcp.pml b/tests/tcp/no-network/tcp.pml deleted file mode 100644 index 4e39675..0000000 --- a/tests/tcp/no-network/tcp.pml +++ /dev/null @@ -1,144 +0,0 @@ -// models: phi1, phi2, phi3, phi5 -// does not model: phi4, phi7 -// not yet implemented: phi6 -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } - -chan AtoN = [2] of { mtype }; -chan NtoA = [2] of { mtype }; -chan BtoN = [2] of { mtype }; -chan NtoB = [2] 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); -} diff --git a/tests/tcp/pan b/tests/tcp/pan deleted file mode 100755 index 79a5e06ef9bd3a520a1ae7b89515240cd4a41ed6..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 110664 zcmcG%3w#ts);8Xg%#Z*H9gs*+kOYGgi->p&AlgF|BOq5{{?9qp)6+AP?7rXs`+WoH z?mAV^sdG-9x^#7Q^~yZw4KWsr6#T_V*GUw5JIT%@ag?OWzlPG-rSVb^$u39=|BYju3_IbdsjUI6mIu97$g{X4013%cz%-%hhOj<#N7%U%PFG&>oG}B zaa%CIF6@$|%O5=J>PltF*16Kq|C)`FAZVA73+9!MT;f`|c<#v3dzRc+ntAWtbH>cO z=c*c%fR1d`0Inee)ywbf;dT+=;vgdJ5y%> z=$GQ}0zDn&MLY-L?;@R+qMw7O{Q4g7^(_ay&WcSG5Z$Rjber*?YO50ibr@Ele>4Lti3;KpG=%05%rzW#Ad4hfh zSlBNIq0Z8mbU}Z;3;K^;&_{MbcXvVmt_%8YUC_w^I+Oo>&{Khl{4D^Xv-B@@L4T_Y zI{9X2e8zP_Z|j0SwhQ`AUC`sZ&^ORU`l>GI)V_2kKeZ8^(RX%1U)}{hvkUsax}ZM} zdT%L3nmuz4t|W=t7W#dJKcbgK&?Rbvsi_?&6&1}dSyC)5aV;)f^pG^Sbe>CEvS{(V z1+F4#R{kxs7L~XPr6r5!EVxH1TDWNL0!p}`@PS2iUR+qbSXwl9@#2Mxr6u$3T`*_9 zhy@?Ome8TFcn;!Ri(L!nOApL_V98u?cP++$3JEs%EG%(Jvu4d(vam2KYgW;c!Z{0y zI2LS*3g<6eGFN(F&iwfcAqHfeLum_L4=tKI>+V^Ccn>6yik2;&=bFn&Ae3v~19O*f z0Fus{McU3<;+nJAHS2*n^A<=;i*yZ_JhY^6A+o#CnLjaS*60ye8CRpm7?)QYSEEOa zmHz*Cb=R1o9VDx7B5|pId;zIvGWS&EPinKy@iFtuO4yL zh)nd3=p^Ue4K?n4VBrE?jagK>G5Wt)<0?oAKT}HUe@tWJSn3a~+$RLb5f{vxhc3=0 zC86FB?U|>ZMR#G9F4DvOI6hVyqK8W^nuo41MjDAQ{W@-$!)JiFpW*-xr%ZI}ql3So z|56`m?i+*tOLXd=g1?k0f5i5~2?iEcO1 zNw?rnG0{n;;BShF9;}-bS74&k7$W$aZK9j|{bCcH+R)%{k%=B015sS5iB4mc;IGU? zH;*wYP4u7-5N553PGgJUZ=H#5Zui!k=)o}-VK$iPG;Rw1-Zs(AW0`6bJvhcAOudP2 z9;a_L}H4ZVLX|Omy=gNHfucV=KaRnCQW=C(%!t=rp!8ez%7F zHq{`a-8RwFO!OoZoyMQRUy6x-X^@C>s)-&Pt5Wn(6Mcv&eWriX!)NRWQ`6{Q%i*IG zrmEpDW;e<^?>63wqwe){FeH%V|GbtX-MKz%Z(a*EcwFg)1>3_pj=6sUOfdP z8YP>L>LFLZYH(r~O`Pc?VxW!F&1@>-a~;v9E31y^0Hxu4tfF=(4chgJrCHf=-j!@{ z=o#W51@UFsqnuEtq~CN!J*2IG!p*ippjc)$G5=#Y*`=Zp@}P1O1X-zvX11#i^{B&r zAl9M&>}WV0lUK2I#mx?{BjEJruCXfWX}QW_X=sa=t9n~nEgf>zgRu?YA#`huWlzI* zJ=LS58XMY@)aFrp6nBGF?P$oW>csCycY^t9}0e?_i}BRQ8@Ag84n61DXlMJKJdrMbO=W7Xz{?|Kk% zhh}N^FMy?Ty*I>FoXC~)n;i|OVkZ~Y18{0kgEr9Hx10MwTt=&RO1!ghTR!RJKGkhm zUcS5Dq7*hOmQ(ICam&W3I|J#Tu7e*mqlCS7i+)nPQ^e&&OLGh&%poL^t8BiT(j*9C#|e`=;}Y`yHCZ)kNpZ0DX}-kE3tPZIlX<8oa$C3R(59W$j61cLuv3| z=^V9H$!JwFw&be~in>K`;0qk>|I z23{Hs92E`hX#(zm1PS>pq%&g+DbTRLk1}eDlO-f2IIjzpQQPv}TCC!3NnzdBSWzZQ z;R(e%<|qgjR}UhW#F06iumKp6PCqN^QHXk_GHQpC(E&3k>Ncg}KzC&nY_eU+Xr_3z zS!p;DufRb8L3{>CKf`#JMWFgAqZ%2tM^Rf*>1@g z4oxjQ<_n&biW9EB)PwpKouTII@>h`$b)R~&=~KCTRnIEwFX&`D-aubkCBgaKr>^M_+*xU!bA(;Ig^5Sk$;P#Q+RCCkqPFyMF^{%VsjNJ4oa)vW~wwy67eUY5;LV6i6a>lFa zYx(?U`g%UUpZ+$VKTNO3xg|F}o;q)w6EbmDyyfX_bO!Sz#haU+N>?e0cUpS9qMlbg z*$>~4CTV%60|BeI;kex~ z-7$?F0VZ7z4J!h!RP=kWdw`4K=s&3OIf-$XW>K;OaImF)6%X0My=my3GaWM=GaYw1 zW;NBN&YmMNqDDf2D(cB&%HQ}BXT{@6Pw`O-ZS{#jz~O_fr2Lj<%Ej?73i#>hR1f$w z0d{Xj`@0z}o>lRzYsJt|srW)Je*!5K^=qg4y_R?~5U8jx`OK;Qj9{*+LCTXm6z{D8 zP!#nW68au+A&U; z#0;Hi54^cOeieGlqU9ns+6)LlN+mH@Z8C!Sg+GC1Pi56+(zC8Zc0k&nw8fNCZNlhP zE?*4|nqwuWx6s0cn459Rp|&XNplMIVMlkX+IM@+IZP5yT2?XS-9Lt19K#e$JV05C<5$LKElyY-t9W8C^r=c5_I8?7 zP2N<#)io1s*{jz;cG;JttZH1pZI0wnPsvq_E$;8)vd+6kDen3hxoRuC1%1#IC9A_V zgwrzl@t2TZhq?F1K&gK@kczaiD&7JV%-0IMcjd7_pe%be(qcg8NnDQ$ufw9+p2J1OR{3{-VP=W- zS+L7)m4K9T4{SDn0B4=MFf?5gE`G280TFY6(ag02fUf=Hzd{-6aw+DhoMgN7y)?%MYs3Kp{dQ|R>?#%}+CGAec zBch%n>X8j1z?70C&qfCBYzs+H(hF&}Lhxc|*mdAtLdytDi@GLi0Bg2%IbX;p{#eEB~$+ zE*y1qvyY}?$KTSV4RLaLUn0s?yWMSZH8d2!5YIE#iCR{fa3Sc&;hKLzQXsAdQLeIP zTDB;KtxDF8C6^#>5{S*Yy#p5NCqeckmQw1hZOaY-V$~sv1p~*#yAb2_4jYGvvvB1i zHDS@@!V^vmXk(Kn5=u?J7AK7Prs0I9r_y#4U1Tr64kmEP7y$ApEl&R3Vpy|CP0l1# zp)DWrN>-~PPi$0e6DUyFROJ3p+H&h0*kz;`ITRja`Lg$71g2zs21%cU5Y5&s3z*8j zXU0+Ltj0$_hj{NJjT6IfPx5`7CdQ(y%6=Zi0H#jlHP;|_XYBBCh|8CKkD}ddq2?Bv z)WL$1HsmMNdD%A|^?zU6zEwPn+4SJrmYCW+C#C71N_&$trEfD;@zd$9s#o|=6Q;?%K z4|Q`>ifOzed_|0=+YkEgV~?@@F-`Jo=z|<}JQed5UCLFPp#Q`%WTO}{-Qb%-b&FN( zb0iR`h3iOl-Ei=g84;&{L`y^yOuk3KTO>XNn(+T`e#O;#Bk{+G@Ql6Tbu4M0YgX{*eizFhZ`Hk#4PA z_X_AnIKFb-tHH2mMtXv}ZbLBGT=p6+C4Uui4$lQe5MvaXK<<&t^TA&I+Sh6n z^uhK(pvAU>Vu@{wjdat9k!P$-gBEU`XCjqn;PVJm`*j>C9o3Xb{haPVlIp0>QoJ9s z^dkE&AROBuNY)-=amB#X#WLL`WU|41XnZmrnTXz*^UOj}Q8&YUa(Ony{s47PYR3H< z`pU5o(v#Se-a$y%i;Gd~n?XFtF>l~?Kocq15_6jl%nj?AA$dJIaa9Y%UQMiNB=VpJLW^zt2vH9_iLW9G!{G8XSVOpdS5E&O zqz>1wob(|5&Z2&s^qWDM@LiZ|5_E%0-;Mk{iQ`#}&Rx0^yrML`G?>AkxB+>etDx_c zQNLr6ktm&WxY0F9uE4O zDY+CmJlZ+(AA~Fbb5YE9AXQf`??%$-dOZ--pfbJrmTgF%&a=v)tbRPh`u;SmQ+-n@ zi62~61!(xT>=M4+v+YM}d84(o2<>@K+@IAeHtOclpxe&Bh?%nR)PL(bbv4GgO_Y2103Q|eB$)7^$%W8ViH5dd>Cjp_k)vOr6(52r%hS(-K;1?l zd1EPrShb0=YZ6K3B1!u}44hAX*6`DytYh*E^=U12mq28V?xobdcN#YmJuv3Nz}q(Z z1O{S{Q5Q%z0|S^kbjMM7Mr)Bgw9%LHD+VfP+$3!tc+)+FADa3mfn_x{@Y-!UxfW#N zcL3A(@?)z7KikKk9+eAh?-R&Qycjf42faq*IR>w8I(ezi>sj!6_^y%}lS_bf*z@*U;&sHOol?>rr6f&Yna$uIvTA7J<45WDFlK;FIl3XrXwm zxIF;m0!2-^lRWcE?$X+my$Rz+?a1|7$5otg$oX5;?K^&QCE8E4SX_tPCoQ8o+P^;5 z#7TJ$LOthDk8?x8^0xP&nHa@=Hr16Pzw*_RpFLy#r|tbYxK}!W$)sl?X#3ZE<8PYt zOZ8;0&Op2SKL;@?v8GSQ558@^3O|}vl<~tkAs_{4W)u%1F%aR2B*%xd|2ao$zam#X zj7f-UDi(N*q*=kpUx6zJ=I|V=&Q;u&sGGILI5iwf9JSf~iKWH%c4Zn( zNJt-$q@HWR?Y!2GCQZ$;LK~|y>tKoBot>y6Rmq!*deG@z(pNp=xmG)iMD+0BIg#vG ziC-Q5{ZJ}_QjAq_n|L>sjC)gRaLC_OOS07Mg{T-ievEvD#0L&g2_}93LTx%E5re__ zb9PDlE0hs!xffSde%p!mEtbTZp_og9*+gUGXVawyBxSdbN+Jl0@hC-Nwre2GCWCGtfedy;=hhge43)z=O5U!M?FN@EMBW`mPO^ghFOWq|e+5_JlTgmW)6T+1^cP7Frb&}L z*7`}FVW%*GEtgNV;O6cl3+G;u*7fJ)(UDh5!l# zXrF}6;iqNjq|q%CmtZ>WPl%-(i+7=aeqnQv?khL&@r3W;TMUBs;TM<|CR4eWrzcoe z6ybqcLaw*?e7<{g4BsGfp3U)z2Me69z~n?eMd6W$0ls04^{F zz=*R-CI6vY;n4KdhUI z`R&uUK}*?(!O@a*tQVBU78}5^z^;O z5qm_$TNL53r(h8DDlYHj(Fx7nJ_j!P^w|O4VzF*ZpHV6C@M^ZYU-5NIEybp-*`Q~^+ z(tNYiGuDdh$+B;OHQ(}yQyu=}Gnk+i_QN#Zh54SPNm}=PJg3*oY4Kx9`Xi)3?(@MF z7EUOTt5%7**0|98@kCK2X>xn)^OQbg52U-51hI~y$z#~>N}a(Ka@AAJ;6NOvl>6vY z%5?LV#_8iNc@^KvPdmf3Dc9yFIb66Ye-<`g1k;3WHs z@vK3VNGq4fO>UMyfzxn_SVZza1zC&RM-)~3f#L z^U5u*euz&Za#<~>aUJF!q=^eCc%xshT&pHqRh*EY+z2WR`ac(=3fzod0jqDwmK^VY43UcW zzV33>ZSj>CDC=OXzT#dOE1+P>CS-xg=@KFfTM?U(#1nj2{8YG8vFyUyIK}$_{w7;Q zDy)fPE@N~qTppO}n1^^vWvmxV6$*Do^ZCDKpvxGofPzQh!^sxj;$CVaj4S6Kb{{&G zvDtktZkbEf0_mGmj@u;_!xg`O8Z66K?N4IShT^@`qMsCRj<_rk3jn8zkiHI35V5`l zd1YuKJDPIf=H)Id@Y>ss4r^cgcDicyo#v+Fi4~ZA*hb4b(1N@AqNh)iO0d##Oh0>N zCM`N_Kd5+>xOOZWZRMqg69d%Nmvmr?qMOL0Nnh;Qa6YEu#EP4}H(;5kbB#4$Jp~Kn zx#RwLoFz-6We3hvVreBNQKrOL8XFGu9JQ@se-f?KtGB8<8cz4LY@3YUZ!@@HW~$S5 zp4LyvbFetGwc(TvYdOJ1tn)l$tn=hJtn-BPsJ5+@m_CuKZWJp{Wy>~T8jvYgea18# z=rgKy)E4kK)6>#O>pV@#8X?er2uO1Ewrrzyp0Z_!x~<_r4r(XH96S=V>hUJPj*}rJlE7sizf7KKo%^Q9jBM4HgzSI%#Pl zEi%lf<*-o14#J|8rFGYK_pUbGf-IP8HvI=PXo0@QE5#h)_Fz(vCcCR zh;^QkK&N-^^62!siy&??6A(0 zQNcx>SmenNv};)6iuJ2_9^dmZn*386{Kqk3pz|4=MYk4+S+R_#SXTv3paorVUp39} zt_mE+X~oQH%0f#Y=Yi51Z|B)sMJeQ8lAM z6N~>aHRkl*8{_mY>&D=A+2KBCDY+uwy(wmL)^XSN$?EqG+_I!=TOpf6-HiIT;!F3b z?yk@N1uqG-{~fW{=c-4vVF+PySiJ0;+AXWm)ki7(v`EdJ+AX(o{sn!Ib^Dug)zm(@ zS%*swwZBB&j>r0GTQim%6yBH$XTx1bLgo$e2^hy%KTT~B^e`fgO(-$i*360VV^Dv$ zQd+v%^4yV%k-5^8byW6#3jwb53 zBVXJ-QTFw{6}QR-n3WKd0`Go8cct!aeI1qkAcAMME`n!3E7tb8hAD+PcqlPob6X7* zn3_6S^-osYu!<40q`39e=;ac{b0=2ZeNnR8QFi%HC^_>oh+|D+RI46yVsbWytpCM| zeu}Djr=sPbmTW0YJt*#lT1$?LQpX(lPPyCll4gV?0aJeGa&w&}$!2H!iUjVOUb}5iIGOiGy|($V%Zad9rU>32vEU)y5+C zf%w{MfpgT<^>av0Id5Bj;ckqkx!lVpjFxJDKM1ka(~~&1QI8daP{f|V6hsY0Dh&OV zmJ*U{Ff<#C>qKPkp1SK1+R&|}Pm#MVwQf3cW2TtD=y2Rt%yS*n3-r29HuKe`Xk+)Bu#LXF|)}x-^l(!q!M!B0Rhc5oa^Sg zRNm;izZ*>N`a!Omc4Z$Dc%gx~p7Pu!%Hx%7xL%9LVpQg{!pdAxKXr%_zb)0b%s^X! zmN({+9s6%cEt#|--gSrX??&_iVkrBbG6*|B@HHF3Mg(c93S)Y#=bp#UH+a0?p5uGb zNc947+3Kq`2p%F-%XL_-I`*3s802vf=y?dudKG?zyMi8IchQ6yC0~>+?_pU`vKx`U zRC2lct$^9E!zItmL&UiHxwB9ABiJ{=SbE{Ay$wvx->J*u8GseSU$_RL z0dit?DjuvbF=Yj(5vKNMKWr4<_E1;nsBXJ$j#QI6b&kaMB6V&^@3VuZ_5A^zMYVkz zq8H)7Hyd@-3HpX2sL|>YNA-G&rqxAa6&Ae$=PRS=J&2}Kq0VnSPs)m=jcr@-$ebSJ z`1Tp@;{?r}{R`?F*1Q{L(_?$Cz9(naCIQ1^H``eOKd3G-WctutsJtzHi6f zXqi5BVoVa=Vx&Dt(A$mRZUoD+mt4sCo{d2U4^Re=QmU7YRR2KGo&8sl>RY68XD_Be z-7ZpK4-V8s`DzRR8WfaY{5+Y&Z~0ZBS*JKm}-F>KPy~ z?e0nZG$GA+Xd7f%kLTZQU^^t`GkP}O`=0bvdY(L(Md^(xR0y;QYbLuxMr4+$6eh>e zrTkVStstq~WnuBQQbt(lY4fvC&8bMx%n4dWg5cWOf^A^ffGnJ}RCY#U*5#~o1H{EcXYkU4Cphhkr9L4zXZ|NAY)U z_FYNE%ejx&McV?!!Opgh&q;Xs1_?U=XeR1T+y?rRx&=Y80M!kkIyjXWQR!(vZ9)h5 z6nOgfQ>9u@!57fN_)Ng&=jv- znPa(ZcOrJD|6;@n-(HI;7nl(*%fO5%3HdR4yyD+M335nCUoZiccJ@=d$@WhpN&8lm zu#LjL^@hQABC-D%VkxeK;2Ql(=BM`Wqs&tMIxRb(v(h z(SQf-zTCi<>&*Ky^8(wiNwD8@M)X`gIuXptbCQwF_ctT@2Fm2$Fdasff0ENA%?2w6 zyU=)FEfQ)6>XGIRygo+jA++5t zzDA#-r&Yl(fe}Q+@|ieSyy8B13QyVMm8^lUW2$EH7{xPu11|7-*FdDQy+GF)1HE)o z_witXmTk^Ombe!p6VOuPRcEEO7Rg5kMb5!%li5xHw4-D()mDJ(pg6W11jq_k@wvC{ zN}SQN4WN^18-f$BUJ?WI7lhbyRrV7wLu~dD8@P6-ygjzVi9mQKRM2{KZ6J-NRNHwx zLqgQQDT=zuiux6!c%ZBl?gITAiuMj$t93)^sCg0%gE`{QK|ogH^4&qD;7^J>`wd_u z*M;c+f2Kqp+n+%2Sl4ptYcr5<`$3wK_t@q^IPanub?j_h_)_D8Mb_Pia!kC5h&*Gl z>wArsd($#O)%GoU(~EfGgq5BNlofs++a<(GInUh)8ZYFeIO-QlUE=&WV(`1!{b5peNOIoSzRE&59xF_ z@eDscmiW(1qS5O#c>Sh_5SD#8F$&(aUH!BW;@_OePK&%Y@n!P=AX$-`1OeY;LMfi) zCs%@4N6%8Ue;^;-yy6yPE_Xb61X#_00$gU_0f07%qjJE&b}vUwK|T{P3POIKd9)>s;p6As1g&~b49yWNaU#(v{2jBN<4MGFbDOn;R=$ScaAIwtdJa#L z-$f!6-p4r63#ji?NfhqE+e>}$77{w3(WHSV@hY6;jRS5i%9?S*dHKobkc?|G8qt$* zSJYfES;I_R0~wikN+M+PX`Cj?8^>Hxl;v`qU%7p9;jg%ny|$Oz#hJ&5A5!$)j^63$?q$e{1TMJhjmFXeDm-|^u7C6a&) z7qRWYCEwNeJ;cx5)hQ`Ox%Al9wviJRbi?JF%(65ozwlFpt^=n@@R-t|$NaOF3XTMi zMbn1dWgi~o4_p9L+3+8JKAvn1$rIS;roQPc=E* zM=XwvuP1q(ne>qTYow%ik%Ui)MG8HT9L{n%PSvmkd5rm9n+t=tb`e+4!V82aZRH-7 zJ!!j(491>xEDoOZ4-rM4^d3i1)gw>Zi&%^QN${BJy@T%9`ogu`EpWkrlGU;@Tit;N zE-qWfHt%gH!+}RItfaYGZvvLQCbm&11CKv!U*n2Bo?b^eT}_P$t#B?pqmAL5o7#_r zJEgXLKTRJuyR(bp)6ieVHQRdA#A&X2!bgwww7@PhW%A$qlOncW)V}Exr3-TLjvzp} z>Myw&=kWgbd$`Yta@h z!xas{R>20;!~eX6!o6(|BCM!0$Z0QbugXhOn68Y-Ic{yZ*WlvODZBFomJ8yp2Q8j^fV ztN%enAyap=1xc60%YUfnxfZJMw-ZVocokSfzUIYPCX1U_=|lrw*t>>c`(xPOcC}UH zV42(HB9j3klh;rSLSpK({t6?L)GG8lt*w;40d=Bg9u+LF?|M1>3tg2cIHNmuF8m3 z#x$&j_t*}BsCY2QfkyX9_r=_Y$$MIL=-}?AhAdr6kHWa}`@Dqa2Nh~gCeVL1(3?_% z=o85X8maY}Lb~$Nwh;Od9G;Xjl#JRHiZT{?GKzLXU@h`8{}YO8i3#->qgc{&Hw5+6 z^Rzf>PKP8VU@h(OCD1gk(G-EEuFV&ThLz+C4L#XPA+$9tso+8lH>9*uWSgjN92%&#Z=sp5H z8)%i$#qh1J%NY>e<}`%YcJqJ~-kMkNpHQ?#g(xXT{h3i*&dHH^qMXNu^rh^?+%?s8 zA1!LrW*d1>D> zP}xBLfzVe9^dg{N4nr5yqj3^`Itx#JT|)<9bzDe38WC!TG4_Q8O3^pWAqIE>M6`kj z@g_PVsM;xlGwyoz#tDYKliAXfbzb`{9wji_)x`Gqf-RwY80b)yFJ?47n5dzHscCZ) zdb&VUrTus!*`yeGhn%--M|zCV{TNNo8`iW%qPUS_M`F}|nko{_X#wY15SC{NOH9tk z3&Cs2n}i#dQ=YE~G&K|#b%K6^(X;}gh7Pr4H{k;ngq|zV)KGlsU?0%)jwnT{Z#8r< zmEsy=kZuS+@OffDrAV)HYXkAJy`rM$x4D@y#toq|e1)Z=hNFfKrcyu%Z+-BPl0D#t zAUISAZ!?$@^20`xL}VK6X$D92FOev+zc2)&W{6QNiY}~wiA06^7e-ws1f`zvf9zyF zXc-dpy^x^XL6F0VEGek@dAlL*AZAB{Bm3YGm@1R@rT|mUmxh6D_o0sXIA@xNs-Z*e zg*b?uNo{SR0F%$qrXLYvw?v2?0+aUIXaOddc|8J*oIhnSS^%kr4&rqyTu46hJnfeg z?CaFE%#Q$f(z9Fuh!C5uv}y*s*W()aVbS=mM;?6$U&?rRhI<{cFqKp!kehm>k$eoi zo`F=a!<-`$)f)gIE~B~&U8#u5t}|J=_za4lO6dUGidy9wI@E?*SSoC7D-S4h?7-X2 zcriwc^h_Z1%!!xw1cRv-l$sTdL{Xa{L}t|OjEYh;5=A9zLZu2pNzv!BO^OOZ53`n} zTMZp*LtQsnSvx3(qSS}|HVkZXWSY6Ep@XRxCCRnF2=Eku2S$TWa?VsLHFT&Qje`)I zWYB0ACfKI{;I;`-Vh0$EbdneYhrrZgX~P6~Ho&h$gCi?%$dSne+E3WH2wqr*Yv2o` z@xA*QLrbc#wNyAla;nbSTa3@4p8K+BaAe0F%ACqgTP(nf0QO&NQoERzwvk(27|NXd zm~Ssd<~)NqS_of>D6sg8nT06u)DWJVJvs8Pp>Eqw$f= z0zi8HBM5&KJ3R4ByStQF{D)SEUneEBkAXD|jH;ZG*$ofR&dn$u8lTBB=^D`rk!fq_ zPgrxW_}HM-6$KIMMgmj9f!nal6x#{1n~W5R zx;Py545Olq6p6|RN8QCJHqxi#O-3@eVB|bCbg1obfT@JEGzPotaSaRoAq>xrm}rN{ znl*GVwL_$`wx7ql?kxg8Jq*v|_^z8Gl0zs8AOXK26~F;+pi2#z*EK!qb(upGS)B@go1}(fCLY2T0F<2;pC1 zJay}t5grx^q{R+Ga0V7LFv?dVQR(5R(TrkWd3~J8RuL77infLhwSx^j`Kor5Ha=3_ zZMcTHip(s8yG8mc66#W?;Yxd#@uY52gu0Qyf#JZ17#O8)Bq}u=mBT1jw|1;aU31kS zH>{yU?Ii}7Y^`+@x@x$Ft`CRdO;v;3sD=);*W(~ch=kXgv8oJ;cHkQLYr^ncHExLL zYeIOEM0-r&PYL{)F;Vh&?V40-+6@AqB3zU9-G~?~M|RXyLPGvQgzqNslE6P4jgRcB zLscV{@XfR?PIc?g)UGk(JL|5=zf9frrNqK5SfmOOPF@wILf73jIlh)7@IwWDV>CXp zyAHK3mlHl#;OzpxEE*qaLh3by35OEC=`fo>5%{a4@sTDBg<`(!Vy8fe0`gdkR za$A!LhY<_AU{Nesyl-Y9YC+c~q|R8A1b&ggyQ1-tCJc==GYMbsXA@Kk{Fn$lMm%@) zqv0aem>N3NPQXE!a1`Oo1b(f+A0K5hfsjA47KHG0rP&2u)Af(WN4A&%>G@wvc!}}U zVzm(qQ)eCtyeb^ng6)R>7n8o%grlBf6t`IMW?3T|Xlfv8=ukV}z?0#%TN&?OC)C}X z8D*}>784*{-Kz=ToAIP>eT2G^z%k*#z2A4LZX{}4IO=6avAX@EWfgrlHAXdbFg37b zYi%xr-Rp&}pO1{vwd)3!gx7`${04#lV>G^N*CMNHhrVOi-Xie7iN;5^4rF2B+G7d- zn!vv;@cpClk*!0>waJXyT!F9F^&er|E+Z($JGuT zViW8Y_}ioLk*!0hkIN?f%L3ma@E1nl(K_72twS2p*3hAL5)Q(I*Af11fj=eidxo1# z(0S_+!qb&DSl|nAql!NI*=T%ZB?m~)KcDaiz9s#sx=bM!|DkoThXY?{VAOafGP{Z4 zs3nZz>T-CPSyvv9Jjk}9zQ2YJwUZ4nSzQ~)U^nf91YO?4Vch}INR>46OmxEZmCs@#Cm=NJ|GYe5%kj z`QJhKHH?SLR@4&2);-NzM5Ht z2_9K%0MZ4YPWbKLkm4lx+Yy3C0&fWi{(*t0-H_d+ZY1iqaMY||cH#5ek*I0ms0>E2 zk=9>sGLmS9MAfDtd<`9Hrx;+ewf4i;T(qUaLbJp0rm9Ut_!>IY-fQ4VW$jIYFBACG zFg!Oc??qJY5S}E_<_mnKz_(o%C4Xeq4!I_kwKh!Ps|9|2G+qq6u0YxvI@I2YgQyy} z68?v;SpT)U{?YjQ2>C;JDm;yMnZkn%UH@o&WYa=^CGww2`1vCL^}7B;qV$h!T0;7h z8)(A>euJ)mG(NIv3CaH(!vF9k>))#DAAv{H(#rbN1XT?kYVW~8$p2fyzbWv0b^Rmo zoir^WJY8w?1%7BOccX3Tq<>fqjcg$R((^AQ{4mB-4NWB$rn(jhoDmK@_5~@6vcLhU`qyW51~mz!DqxBh<);g>L;`v0T|!6U2tOe13kUcne z)(Cuuz@Hr)mH$@}l`MoONwgaU{*=If5RH#)BtlMhH{s(1K1Dd$BhmQCN=k+n^3NiC z%jc{=eU2Mry=$ZKk(D%*|7^mq5%_q4Kbsb%e`F;MHIj1)f1|)>3j7BVcvR9K*nTwQ zQbUK@g*XWLiwGYl@Z)v;Bk-M6(h#1mw3fZBf0?d7Hh2X2rEdE<1olp4fpONBJNsA){kF2Eg zjEouh2L}GvN_u}dY8Ind-93X$>Izv!PewCIHFT&gGr(juZ7_q~iqQ4hXnfa|jD*(? z?BPP5BJj6I<0C6s$VtfR+RFmJNZ>Dw#z$5%GL&%A`v`xxz!wPoo=c+ikE~>&{K<^k zV1b{l>mQAetYo2^j75Y$@G0wGsp}tsM2u)wd^^^d?q{=ST->7p7s)IN%X zkl#i41G`!O4Z8jj_)Z#$5T35Imj%8<*PrqK%SK{3;qPWVH4+-J_z#W5QbTYCW-w5U ze+QVX7STx1JXH-HY9BH1R0NuT7c2g@5PYVY#eZug9wz+jjHgCoZ-n5Hjl?n|V+Jl_ z;D2o-9tuZY!zfnwor_KCni~n4Q>&qaX_Abrrk&f#x>gHaAB@I#J%vufYyT4XdVwDm zjgM?3LQXIDO5>mcC>~LCi|}>{G$So&#}`;;^+QR`gd*rGQwvI zJa4z}vAq+9H!b!=(x^pwMAOc-vi?b&|G)JmdVo>v%-^PvF$zK}_h8Mg^OOlaQlR6Z z!%)0gr@x}8o)ha=FJ*n2Xk(QkHP(}ts^+935L2Y)#Ncej*;?HP^2i&f1Jv@3-z*wQSPU*~dX z`*x*DvGS8;fKWtm6W*~Xj%u=|)`Xn#mO`dw#jTSIf68w-6zljf9ufbdUcyPc-J(Qk zLk{e|GIWw>0KItZ>dzl=+@~JNRRh{x8=;H7l zQ4BjH)nnt5DXG{Rxq~;9>brxsN&Z%GKb$GKzCv`#A_v}#QQUZ&Jw7)JYRcvBK^h2h z?m{YNygiP03-N~pPEWdJa>ciV-5vJw6xSFy8+XF%Ol1T>dawz+-Dp=JLx7 zmfsgn6?@R?<@aaU!YIG?di@eRqZUpjn>;SCL-AH{EA3JCjkfbw(iOXI-GDtja#EXf zZIZ>aBo)PiJu}bH=R$YChwW_C@7iIw`RNMpf&`C9g*-j*8VWngwg4%oQhLDRcsO4`f)h;M;Gc@Y#}C4$;?T(u{# z+1hPZneL6OD+v)0Fl+`L%R1rG31^xRXItDSWy_9BGE?V;$CY7Hx z6s%i8U#UF-OSnp6YCZuS-x=}kGUES?cwY?}U>dG?i!aZT6rbNn@F>WB+F_(q_Ol4S z!ALxXg3PTO!D<21TfbQWv@GsT7H8Hy_^5Qb7b>{3Q$I;1b=RVf!wCy$M^R5--YN{+ z@DGO39s&cn=H{|DcxV1pkcvQxteg!=(Z%F?iW-Ts2{FLjLTu3EiY^MDl0$|{p@P^R zlFRR>Z;+A&m0UDQ1=T1syuIAwq|T^4St-0Nl{Oh9|8{1z$>m#ZR20dRk>?~&U%Y17 z7n>aIbbZ5}TnRE+oFYC85C=ZT{$iJ(YnGpGu#ewf^5GW$5+`;?uz#??`YS1GYStwvwTp4}`-zSD+fPb`Q13R{ew_+wnxp&MB_h}yIAUJzOF zy3%L+2K5j2{+j`4Pe;WQul%ECmVD{!hiL77is|8tq3c<=_FYa_({UwuDDgoat3ZQY z#`wkx3)25&`<0i#SB zRNRZU(w+VDHY)lGsvz#{<03E=^LXy;!jIS~{&bQRc2D3>4?sy31nMQZ1z(N;x=VC6 zo0DK>2fupb_yCuZe-ljyvNgIJVsCr|?sx%w(3ecg7E{nlE*WOhiDXjP%;LJy+&z3{ zuvtX7b8r{f)rHjENk@T-3vtGq%We^{|qA7b?PS=+SqU z?7{aMSJED(mb|P3@{=??%T*6KXs_BgO+4|<=2rg*VRvK1`hp=(%Cg0J6t){*2%aW>-2y|1!OXospfyIwAg7LQo=68?H}=z z!$y3I8$+S%CZl`La`FR*JZX~JH$ESml~2z4*mWI^u(12V@Pj?6bwi}+qg@wIR`)tp z4D|N3R}vaqsO@z1bgC0G+dqIv?Nv@3-f?IDxrLR!^*Aa0cM-@%pmU}FPztZ>jiLz~ zW%fmS^lr0R1Rk98=!b6=@WldDZDX)G>Ti@(Y>#@Vy~dnNXnZvixtQ!pcOlr7em>ud zob3@ll*O$`XehhujSzS9t;ot||Dt1}`5y1i{#!HN)m&K~F_@kr_Q0Wm^b9&Ex%k3N zfq(gFGE6BTXoxh|e8`zn&HO zh!a;_jUsH{L@)CNl3(hcCTaQqK=yawBLLI&&j2V|#cKKh%R@45K^4<295xe1S-<~b zDs8rbEeh81-irs~@UgJE!>Ap`hk|OLocZP#5%j^n?aIkLiuZPOwO?acr(LiVsVeGA z|EQ?nDb>TrT*Lnr)tX*Jn?&@8_~sw8_((aqOTm7*gx^)dc)4;qRKmVWFK;3{J-Hht z<@k`M8hBKguYQ-`(t;F$_R+N%JxO)PAu8d2Pk7oG`3k=ZIt>)jK#fzRoCfe+W6M+Q#yq-e|k z4lVi0sh$SW_;8`O0Cw2tR8Np7@gz#tUhH@QIepzPLUVS=MNQ;S+Dt@guc67Jz!U`h zG{OlM7w-zYN3I(99F`8sRqe)Sxi15cK=OLbrqlM&a`|;=8F3XOSKNxLq88g4tUR*N z#a(#z90QACYKPPv4o38iZab36RlCAI(fv|wDt)3Gd(gxomBZUN0k^kmtDM^)S7H02 zUkC4u1JM)9W{ui@A*W2J^OpyDj>d9#9Iq;D>smHd-E(o|8Ih+ zZbiAX&4%K6bV7MOYI)a>s3U`8=tvY zu-v&~i1>by{-G+~w+M4PvhO8>-C`hko9Qu|DH;Q+_=|(wZbzI?0rNoemDV(4-yq)W zt}uW(uOjvR>nW>hatv(D!|JU6=YLnH%EjN zoi&Kl)tM37l{%D_P$$@2(Y7i1?68y7W;pCMzC~=36!1V+@$00`bI{H1cB*4OB@;ST zY?p>&InfkTa_NaCY;$i^M@+=PP)oP^E`(5l?BOJ;m+V5?dO7sdPXcW5Puhlz6EmCYHA`TSX})kSQZbS z5K}U;j6V?+BR^A*ZMWJp!-HvIo_xbX7;q$uezrdh2wik{ZVDL-8-sE6-p<0v6<;Hf zPh)|;v!IGkWc&xfiz?n*$d-UA{*o$2@FD9gn@; z@U8lo7_{YLmPoGR&mr06s*~6Z%X?#>ausoNWF3F>y2*u`aCaS31G5HlGxj4*z?+bT z&7ANZFUx5M2Kd<63-hebj23LLwfyoJdu1s;Vnla*TS~r1E7F`hI)?I<%lD8rQ(1)+ zXyeBXEgB`;CmGa&$ZIl?gTFrxT}b*IC+|{HyDlj<@`}L|0g^XQ$m{S<$ofB%)ipww zbCCou3opn=A3#Cg&svO5Nz->?+iSR~KBlsxA2^H7!PBF`-&6f))xiLYz`b&4*0PHf z{0j?|i}kNX zj5}MyP(^ZKkJiurMHd5+_Q<8!6VGnJx8NTcip~qJ>9yMZa|9#*yX^gv@m;DSe3(k! zxCO%Y+K#T=moQ1**yraBe^hDVS5p4c$)1p347c}Fm1rwNO}szaI%#OB2I|(yLY;@?E4>^MEa>FOr%T} zsaHs(m5A34gWA3tx%cPXEwtOrUob`MN#205n>wYq#r8Zd=qK#5x*uEia2g4Vis`W} zA^+C<{Sj;#j-i&zJcivG$Jh8Qx?K%*s6%m`9Y4s06O(b@5XpLQGK&S%qTfNcS1yJr zO0fYyoCRNC=Dk(4OYv|^S?B3nu>ma?5-r92D=dX8S7*tOyD52#m6Ma6!jM@a!#}19 z%K$wNXt}C1R@;4=_N=R>wAd@XLPkpLjaHp1Jmz+~D9Hf8rUPn7p;~fVevGM&KY{xK z8t?gcC$sWjq6ed|Mb)i`zx!stj=mGISm}6QARusdOc3E~=7KyOWZXD$LTx+(?N1}O zpD^HWw#NlcQwg3?rio`=L#Da2chEGy=`8u@xEVA|LrMtKTq2}i!5PM*%pbODe>i2f zN%`5nG;FPor9m^Rcp5zwZj@|jU%pF1rjv?cN~^F8=_)MqE4U!V$4Fc`(Z*XaxwFqz zrJ{Ez-vE~G>{BA}JOa@973Mm{TK8(W;jWrTd~D?++Ey24z6&WbXui|MC=0s(@hgJm z1~k>p_U_PXqHRK~s|TChe;e%Li>T&_HpzeH0v7PM z%&iC6C{}ynq}fIlpCO4mdk_Js;l6|}*l#{b5soIT6Y?7ga{|I|UJ%@0<%H3GGX_d^ z;x_|9HWZf-V87Xj+k|F&Pa)!IxTeXq$FPXY|EY`k2wkva3Wh@GCCMH~jh^O(G z97SO1Ld2);g@}v`E1QQwHbk6>0E^g{MZ`oq_O0nfwy}3d2k3uRWN`ww1I_je+3`IO zM>GZ(mVu$EF_;IuXbkQ}-x^gxzF$en^~QjzsPOn3Gw6`V_k16AmdmSplY?{b`A;%=#+&DZgALn{cwnr1#=f3idPWDhz%%NRIOG{WzeD1c zzW|o*>>otncL=~V&oS3%&$#>^_KZ>y9pM>0C^G07KNbc(V}fA$0@}}J`@jg#7{r<1 z$eCAUaLU9!(8KTyr-(Y)OSjPxTtL8^ncF48GuC3}Gi0NRkC4QjeE|WCRp$ z0)vGJS1{LTXRDpV&el^zM>yO6P-M{A$`BCE(7zK{tC46go9$zSvl+GWT|~OG_x*z; zsd!DKd@Vk*R_gJzeLvUA(e9D9A|1@<*YspbM31-vM* zkr*>Y71&#xTrV&hPKW|K-jh|E#yQ!A=Rb=*S3(6=u>(om+5JgD^86IKV9#&C@FL{- z)E9{^_Dp-w^Pd&m|I7)aJ%7Y(cs}F8y4Zdo8>Mh&mhSoQpkZycPZU121(ho#V)+Q< z(_(8sZTQqM&XEUm{o}gysgY0=4Ol=n`&8!Np`Tp-1(w;kv#%6^?FgWV_8?(rU0V@k zMD#`x9pO{?6dClXVF(DHdPK1N0*zj?JxAPqmOX641jro3R8xcQ&MtqGWU07Cq`jpZ zdzI1Y8}TC%&t7$zNcb2t%@w7&1>2;AOjQw!B<}2+h%uGsB)Z_zJk8^l=yq(_;b3WQ z!4nFo*~$r{OLO*Jowj57AcyovfP1)uXbhX}lRJ0qSb9Wb8WP=($yVXo(~x(RYwyNW z3}Z-y1rEAv_ZQ+m#5vJM_qYjI`-9mS?`_-wEdt7#t0_A(c@3X1^Yi-K#-f6=@j8NYf+0$e)AEMp#LMr z-2c&q=>Psd_TB`nspI<}z6k^p1Ol$Ov|g)JP@>?D8U+D`iinC^Q87Y5Dw`xxv@Y0y zLJ^l*?cQozyDxTesjcFUOKt69TfeqdTdhHAwY6@wn)h>N=7s=jzrW}A{@>^MzfZ4{ zGxyAyGiT16Idf+2h6tq23)DqMf1XwBW(DW|BqMBWHz8=-?dCtA>)M~H%zyB0`=Ule zL@a(>KDZkbZrtnC1En2!bsey@s~;JOd=>K9Xu0OaT0McWOufA+7U4>lyD1*RUMn}n z0|+P@nPLJX7hV?i2vc0fYx)gdX}Kf>^62yPM+k$PuQv^HtU9N zVvxJttirO3+s#VEIF0NkkdX_!!Kf8>GY%6qG`tC3Zy$nu=E4qRT)EjzPmok=F8<-N zn+Wh1c5^RPdV9O+<)Hp<;R)h8yXpN3^;HQy$Y3{y^OLV|0uhe0=%lgT%$PuYG@tP7 z26mG~nTp*+;Dp;vF=u%aZf{={eFNToD5tZ^E7p@FrQgmEbSza{*O)d;5GGTwtFWAg;5|)h|Jl{OZ5mxPqVbQ6Nye+`J4eO7Xo z=iztu6&K^=_PyehSHD*#gE2SJRD?i{dgVB-YPbR)#C5z^YCA%49Z?bk3zuO$Z4t$D zb$oYMpRlVId!8hWeNPl!2inctbnQhBYB>0b?KjjOr|UzB6~QMEKUC(aB5&H7RK3=g zE@+-X$Kk_4+u@fOY2-Qm;+4dezGK{?`%^OA$ly67zLH;_FK_WIg&>;u*KsSTyF15q zaR=9SNa=nboI%+NJbF>l4tJ&=w|3B1oiG25Zc`r#izwM)!^f}rZCW*4NM8;#O!8{Y zNK`>bVtH@~>SRrHU0{v!A>rex3U=4Qf+vxx>@@+x`o~wYt9ANK>~f-h(-GVeVt1(c z)kP3^iO;zr=xB}0sa^1h$iCQC`1TIs{=Y~YQGWEv8W-|Kfvl~m+QW4A9(sh!`mO6C z>Lqr$Ij($fY~^gaN1{p9bSC2Z(=zVjy#n6HpOEo28hjT@U)3tU@_l~c^id9WvMZHq z(OTS!TgH$?rr-1!UHdKmOJyBV{1+A!D?kBKYp2rV3uUw^a`(d4@##nOn-W{9E0b~G z%a>(Hv5W<0iBOAA4eg8dQcJi3Yl5m`%QEg&*N*>hio2EU>?(;5J&jY5JT)Xw2^_0( zRr1*zvgwAln}#+W=w-$C$LUMr19jGpAEOOY^fqdEtp$3Cxz2R1vtLxvMr#KA zCcYJZny&HUf=)0TQY`LwetcK-qQ7sUr2hFGxa!^ENX-Bc4pdv?i|5_bRAZe;z{6@L z;Ax#1Z@+;%jyr-xzbW>fW{_YteQOT&zm#d8H`&WmzoZssibty^dpSED-Et)gj}vT~ z@8!tAD_L+e;~T7hYrX{y$0stp?WvkQE)>1J1&Pr!OIf=EmV;?J|FNp_+7n~{>dOMDChTAwk-i6=B@V2*Vdb>~yIcjaqeZ1NM zyjoVDhc!b~`|~a4MZZBjLGza*ftBK)*W{J_3?-vmK2#`1a}nO-xqEr;8YQWbb3y z)(?5sKxFwTS#Po|+uGXufxU`=0L}AsJjAgpYXhpjWn=g9H8FPGZtCH#vcZR`V0*74 zq{3Lr#B(lMx>wLkMT%KXwsS&%*0OYE}a1mwt$?xnko&q%pC*i$)h4XV8hY zN!72c>Zec2>@!o3O`*?AP0;jsj?M!$T>!ys0P&6gBH)Uq2kKQ>n*;YMc4$yRI90Ih zem!-Jp&97nD<%iwa;L3{ep8%pS!^eQS|CowR^)nOctB!bJcKr%?Zs2FA44it^3ivI@XNkBxJ-~@ir`nAkt7Hiu zwwevIf=DleD1LxuJw#f7TQW7zB7vD=K9)O}rF5@(TD|Ni|1KM%D>hC?C@H}c2DT$- z{mcm>)O`OKK)w4q8_pcfkJ7^lkh7OMuH=d}P?S$a`RMJ?D{=8hbyuQvxV+yTb0CDA z0=7arXV7DPnlBl`X9>Oq2SjGtXnU4IRaci`7U zUrOJHup6&F#l-xO+O1g%V%+reDo*G-W{D7pz6tzcDxC*v2I9On3__(}lBFv{eAG6t zD?`3iTLCIv;SzW94-og%-%jU8 zFhi-PFUf;D_{h)oC7)1D`l>+6({Fm8vH7Jjn_ibWo0bwD{;X)RA8Q#1 zrmmTf;#WKnU{P0I8S(}E3O$^;Z-~y5&?Vb|CM)}P0>KHIg^10+02AlIpxClPOlR{tHHj*l>kIz$ zvDfy<%o}xUPDZNQ&my(9Ay~SHLZEZeD{oe z%8;l$@%{w&Rn`1~MzU4kcd_L)c!tB5-#_$o8Z`W5#n|w2ehX2}LC~?lED)Duqsyyn zKDvFuHyRdP2|BFHPNJ(I8!gKz0E%Y5X)B4#rcTFjcBNPI*?A0cdR9pDDZ+`eWKGQ| zs%LCCC5I|9RN}%Z$E0CpW0_dC)PHoVmzVQVB%0<{ixJ zch$o%F2liEMGyNC^pGA#)X6YJ;ax6xM^Ij4q3&xal#a>J<)38O4Ytt3P?rp`LWTo> zx%99dN!C7%km2pRyca3iSe#Xp8t7;)=y2a6qKCVxq!$-w^EpK&8xggTO8VDT*&RtH z&MaJPBn!Ov_A=-j%5VjfLbayVKgqBGY@w2#E*T<(44Y71jDj~Q*|^!yrZ#A{9du0A zgSfm(vKHRHV0y!X4}h*(GvoVz(3dBdbxDn)uTso*q%R+;hr1CcIoHOrUVN~DtlxsJ z_<=71YEB~&U3|+!zqmcPU{=IuWlMI%>Eo`}_yduN$7}Q@6L6bPwEb6AO$-utW5#ls z_GVddz7OF9mJNpAZ(yZhKd-X?yu56(PORMc(t&s^$QPl{sKuDi>W4nt5vtr}PwT{& zD8ZteUc0V%;q?S%S13+iKu^}EB8l#^IuKLD>tr4l)GUR+jVu4Pri37t5~bUbfRMq7 z5Hhahw5^TZ_$=ZdgoE!P$FUptq2a-j(wA`pZu>A1$79yQimNNA^vj4JEkJw+YOS5| zsDi$9Iehz--JaH2czQu!k|XkO+V`u<;&e6i)L)!_)9Je4(Ejrk`ytOd#h{iQXQ^4q z-%$vx-!uW*L;$2l$>O3fBz+lqTu{A1vJB9?NpdWw+?v+-!SccCbtUc#Pdq$6;tO?+ z5yY(gPsp?%DnUgx!x^2YHKycv(O^8>AAl#?^d;W`%c5($@gdTHwH@y0?Tgs6d_OjV z=>HCc5BON})gv8;Xv>FaYhFQ#;`tD%{8^-GH(rUuTB&pc(s(Y<2jW4nZ8Vbcb}r@C zczouTp43^rvo@4NgcC=8p}6mh01D|mNAi&FSrn&`?s3491NxHZp-9R3GaXK{Q`F?Ih4 zwzm1$xC3ZNc{^17H;UBg!;a z5q_bCp8;&A7`lor0WTO?4>~H4S+2>pGw{Ikxar#)1G(&;om8q?(+e0nkci^n8@mmeCNh60wCyb6S56G;J z(qc8Y1-lDds1C=Q1HpaK9^%D5f?RAgk@Bov`0e1)jOrsI<(HJne^-$gcf5`TEp6ZI z{zuA%psf8G@AbeVR6$h(5tp;CQ_>UUJN1w4>i30JeTh|0OWg>pbgf3LD6P%P_f^q- zEL_mPV!%XSb)%(%r~!i2UuA2h;Eoc}xvJeRqCJE-#(N9TwqTDv^{OmI?wTD`eyeII zB;m~058%A;eyI2-(Qz9WLD~AM=Gbw6n)(l4635dQ)(P0Cj^9Sg;7|KV*8WxFT}-AD zlk~lanmyD!%+sOksvdL^3T=p6hxI7z1Qvm(C(%i#T?Hk|X4e_+EoR;0iN~_GyhIx%I!J_W^WymC4`T62c(lgp zD!wz4Xf!`9Y*6+D1~>2r-S96H&y5Ed&-Xc=@gzKWw!TNvP%h`WtYKO9F?BqLpx`Su z(31&OJzWKR@q%L&0{x~9>xp8Bi=rtg@bIVmv)bBnLre8l2cd;M z3z&Ao;u9;^li_1;Jhl@pY4IX1{=9kBm#8C{>KNmaH4}B<%fML=qcDV;gi`ZR>a6z` zX|zd-G!8|EHITix4cSIKAr=tX&vqfU;%!#P&ht$&qZgfVVpnDJWk(i!6B-vD@qxeqlvf>#yDE7YrE0fhv@}InShd21PX`{;UlRl~Qc;^?;~$8` zFa^zkh~@u@X5+hN4H&|ypDslfj@o0<6(4rGQ)`;?){LXZL|2q>y4y5IUvde&c$1R) zKm!eVqEQQ|FC4aLirMzk-qlgqz$i!+Uuoq7YdiB)F^sC9(mRlm>uy5Jt(|sKI0Zp8&~lOYgqKo z3uFRknF(BVWI$4wfDe_nuWhKp{~m6}fxfXT0Cn#5$eIy8>@)y#*z0KRE?% z!3T9Agy;r!y-GY0oSdalwb_-DugP=V^c5KvF3Xe zshqAVH++SJ-KfPc0@%l>CLee$+6<~B?c&n{^pJBgGK!7s5D`c=?EnLfDVxU8eLE;H zsOF*p<;W`m$bDYwvyFy%2o(3AP4+*LI+NJg{h_V){!1LC)LEv6 za|jaYHy^;z`n@XIB~_9l)eRT_0YFt1fx_{752}fAALua~tAiaCW8F7f{jTjrpH+D7 zWG^U$u=mAR3=gUp6H;O6RMq@mrGL(WjdBV9N5`kvnO^(3O$m16_C+#=!_QS4sM@)p zuX0eTfKswAQkh6qXnrk1FdVs8U$O*^fyI?Aq(*Iuk#DPt82PrENW}Ix-UF4`DQxS8 z$tJ1(>oI9J+E;>cex&Dqf z4?&X`(e3b38fqCNjg0AJZR*;RZ3;9nw%_6_9u9K!p?HJdu4gw|Ni?hXKF#q%NQhpe zcag0fg)2OCWfGE=&Bm<-a4|*k8gl9g@vrhQMio_U>#Wq7ex#!L>SEMt{|oD$L=}4=v1A<4*WiTS z!h@GYp2Ij^gekwOyUR{?g|i_QCgDh|Fnnym9TB)S!Ga5su9=#J_>smZkZ0{!{!M)O z&O~@^km*Z~p;$cL>cBkroB-P?8d7&~-xN)g`;KwB?^u@@10V*yh6;<%9no9<(&ObR z`nVkx!$TU)TiBirshR-uHGhH-8(M(kaL~AI^wr zj`Ugx{`B;GJ6!YJN&ybL7&bsN6&cq1qstE@lpmpYWig^lYSPrN%f5*10+?2uFBVUtJ5ot*T)@cWEfR1xa2->fZb2T)P#OniQuIw!LT8U z5{qYv*S=xG4Nza|m+3IwU>{{trx2#t?Jz&7hAxYejW?>WYJ#h-UQ`!dzrcDGuTIu{ zhiHZlB=;gbpd+zD^W!OabG-ZKYq&=^P)|tWOIaAdtFT#y%Var;6@CF2cbGntePYYM zwV%a>#~qag;JZ)7WU39oEm>%bFFY6COL5T}8CBx6)gt0;jyUyE77Lzge2vogFuz6_ zC|Rqb?FZFyWyyHEqvjJ>|31870m=6$DdAlUStPKn83~8MN)CSwqr$WJm<;I(`Y)ic z8#^;Py`wuufTP6^)b>3=yB(^lh^)@hx*d(*f_)@9klctJXgaFcL+$pn*Vz4Z@uAlj z?W8wz@2v4CKfqdeDgI56PeI85kmJoob6C>xvW+~$qB*kUyM@%IAEB|~q+FAaUzB+3 zlq^NT%OLqWk|8N9`3jQ7JoyrmjyS-M>yifDTT*Oj%d0AjVRYV^QFRS zBFC#azM@9q7|rp2R5ALFM-;}P9RCx?k0E+HRT#+eqd!p?OB|6v2qxo&=}Z$*gkUoM z$Ps-B!FU|zh|ds>@OFN}5qk;2c)ZCGpAdrac$yy!3to?JD14P>3Q#qp zF#lI=aCxZ5I^(p6qT_fOQ`@qqyj00`X$G3tm3NF zkl0cC0fv4q)<;$0l<^9`Gwj`;(1DOna;)ZvP0vGf>BefC4EyJ(bf^yI9*gT5jrUur zncGPtd}mgV`W)TQ;pcgpnP`u;S~CmGNGCPfaOuhov+z1{`Hh6~KhZfIK!6&24x_s? zV|K|BI`;t(Jn_DVlZjGq4?g>b!-V2Rl zVzgoV8xw}3m=r=O=C$xXN9FZ+nbpNrK%;v5UTs3;Z?;2>%)M@flvQkWqOEx4+obk% zN89VLqy(%Pw8ir!gTAyzE8)J@RYB2GO=nn2RTOUGaF~NJ-He4a)tXIKeo-y4{HGcR zM$JCW2*S|mF?KpoIX#HeYE7Y_uhwLUl%o|I60hGr7WZ;US7MV@xcAHxHfO(qmq0#- zLJ1V#7WXsY21+OeI{ghgwb!Z=DpPRpj|CL*mGjkGeW1GS_=BH>c;y=F44UnJsu>Le zyXFT3;VQf47XpMG$gtlkrv{wv)2yP?YE2)Mq@!B%8X=IP5<3^C zrTZb7V9=ek{Vy75YdSK)^u>OAl-3wPwNJB#3hmP@Rm!$v*aga|mR0807nN=8O58{_ zRq-@BJ3{4Rs!3HWBYP!2Z5D2wgbK8bAmsU<$Sdw zi-(Y9J$x?_gm8jST?9X&G@qqj18D>G9YrR)Pf_1x#~=EMnwt@Hc{5OR&oORFBf+&= z<6ThK-9})F=c~uqI)Igjo9}oOtjaabvv|RlBu<4f4q`Z78pP^V@%gYTTICoav;BqA z?pQJ{G9J&w8aN!YVq}H!E2Jxj;ljc}Bphczhd#Wu4}I9v)rUoBqvM>bT}P0@8;Tqg zm;{fZToRJaNyn)Hdafq1IGu&o~M;A>aQ$V+(d+Cxz z1GZ}z+j!2_Zu~KinNb@MmhRXt?B{aT28hcIXJ316IM+}uSP4ssAdL(_7Wa9V!G+|a zIzQ(S3Ws^_qEh%g1Mb`{H6u`XALovTu&Uc0eltp{8UQxDnl$ior2j;dJ&~kfHEY*I z6I<}CUC^KrUx2z?V*y9Xom#C4s1u-e6ei??T$zUAoV}c4&_2y8z%X7t^xMDOo`{Ok z*AtP?>(2*AAmV{=yn^ex#FrdPtp|QEniDIhY1v%8msDEuPynAXH{*;p(JF^j4UC+< z9_uH(oNn#4D9OaWAYnP~corOL*6|uvP<{_remLdNqkJxbv4E=i3?jiYGl;g% zGN%)5GHC6_V>vRKQ%XC=cH@V1V#70oFHpidp;}{y3hCH>WCZ$-^;5{b=(bcW%AoV_ zF_Xqu7J0Hk zPON@*$@=99oMi2Lva}>H3Ktk+7>~gC zMaI9U@UGLB_9CJRP1Qq82^#>4jct{>rn9@^p4!b%HYo)l%=upl?H-i63VaO?W2jIXV}tu=S>fXcUy>vJx@8}xW0V}>Y%}X zj=h!H8SQNTJw2NgA6aX|V!Yl()fJiD6#7fMCHMj?)hVb(c@^FaOozHz6oXEfJ{{35 zIQ(6lM~d^G#rgLF9u@G3{+xb+fcphB3bNg=MDi|z0A*t3b;hT{Q_PPaO!$a=kp4O4+}WzRet`0 zfJ0v6=Vt`;c%7f;3K;VSKVKGB4Eq+`FXK`<38Z$Zwi?7AwORyV3Upf{FH!wHu3Xg0>*6S=dHJJ zm?Pjf0?zq}<9`iPz!(8%2slr`mjyg6-~|DtgZ1SI6z7ow&JnOgz|{h-74W2hwE{M5 z&))*y=@73cLqLTtUz|T7;A;Xp1iU1m=cl}Un1DF~&K9stz*Pc%EZ_|Ry$<=+`#L z_y3ji*>ax4n*#3qjh`P8P~lT{p?n~T!T<_wEmXv)hn%XMX@ z&5;$h>G^pXX|qjr<$MZEdHrQ`j;X)`?$+#FvmD&5XO?U+6RE|=#h=IuO;%(_cI$_H zE7F$koD5WqjcHbvY(?#sY-@IYo}2-;bHJ{5mTUtd9)c`bDq*L5ERMT7CAVBQCZ{=++0cbRvLpdLX~>W#4k)97Z;N6VrmQDBrV~CucBWHrh(qCyXlQZ3vmzQrv zPM#nl8abG>;;w}-Xd}N6>I(_Zl4oV3^=2j;>5kLYDFqEMDl}blP1f}3oc6YKoUJ>V zG~HyGE~9HQbF$N|mj0qQLJG~6{G3^J)k+2VIdk&zbF)o3{pIkY;BNhjARV^ zEj{0sLnbAfXp-wn!MM0;KuMLy4NRp;{lmL;>lGO(hlrtWq1GCvhf~ifaxhECGUu7u zs5H^2&&bb}85g&HBv^r9MD9j$znBw zQfbcvG6w4`SdLjXLtk=!A@z8Erkn@%urpg8`VT&Wm(Uq>su9DlE3`;i`nbU2|>7gJh%+7=VrV={COlsFmTQ&^coLgX>Bd1S?ha^L6Y!yUb zNc5%*rX$W)Segvq2AuG%f!|EyI_DC)&&jdGqCoZU%XoTWX zUs7YrBm+8A3^Ouv>d%-va)ey@Ikwz9^lXNlZ?hJlw?pcQ>Tb6%$K=~o$(^tPvRL4x z(xG7Hl?6K(7EKazk`Np6WZhAou5zv=UCy#)D{~;z&luP(>BfpG3NSJCN5A1NN{qom zcn|n^2+tfwriH9}Hm^xXo{bGuKEAT&G6%&63S1ua#|9z|e8p@=Y!Nx zkXD#aekm!8(go&1n()J5^fGezFkk}c3@P>f4WFmTe8@@+tPQ#O8Fl?>Rmzio_;}(& z2}Nd4&xRLvpN(h=G#3@*(ELRe>I_zkEt9J#-7I(Gy}*2YH_CvmGZdRGnO?^!esfH6 zLXu1slIzd2F(nBeluck5 z+&V*%3{TD`uYB;IU5HtiO%6q31arw1Q}@y37qFQH?hh)D!5>DCjN!uunqdqZTbu^Y ze2zTL49A|6lRq0~F>Ma(3vwwsldA~`AF^z@5D6?;b2?+}D#NdHn2ctUC!yKNr7{;E zJ}Cufpv`$K2tkZvl5_I&3s{bePA3R^V$g?J3+3RR8KLlQby(uW8%ZINt=QX6b4WDT_HnSU9m}R=DfOr-$maKrTt2|m*Sqh9? zM1CX5ccbx=G=_}aFw2~d2#ErUX>-WTxiePWYj92mqqC58<(hNz5oXvdCd9BIu-Osj zEEAQog!V^`h?9C|>d2qMd(vR8N6%&?7Mb$apxq%ni0TqjPm-=O8O?NzpwLi8%K4ho ztu{(c+!xV~38R zE>E9<@HZFgs`ICue?G;tatL#gzgG1q(aF5H$w~&1rVq-=o zCPpWZiIY3ZS^4=HVJt+z+>%>Bb342W`A61UoPItG+YZCmS7?i z|M(b?viOL2qIHaAU0i}wCdZJ3lrbsMDI^CLQ3y>7P3bV&`h-Fb78gUj?71}7i8=39 zw3s@!TQ`{#%JQ%jIn_0Q#Hd0jia9eZ$285HW4tfea-VBpxz;l93$#uW%NcV9LSS0S zKxOPGG-r}_ZF#g9M6{nh7beEKp9KMk`tmX$88>p2s9STH3gL#KHRigA3AM5hCMu@$Sccnw+vjiQ}V}BOWiYS~*;<6E;?-;)7MHq=iVtTr4 zKmY}w5Nsji!BX6UbsEMci?JXDCZ9~$f(+k+mLNh_#<{R>j9s$t22~QdAY^oLd>zi* z5Hz8zduVS$h$Y>Q&N`=nX--jLe^4_z3dYI36y#(0WBFDua>3MKosQ8#wZQ~wa=^jL z31iDM7qKu>nU%&S#Z8Ed8JiM4Br%SRi^qYy9NdU3=aOHfMGFOLCWLg*U2Zn&M$^;N z$PLWk{Y*~N!V0o-GR1A#IXRfAau8%@mMWX1A5eSjQm%t)gy86YPbbMn(oIRoTj#;lzDX(k#7N%>ZD z|2pRIuZ3A8?rh9RXh23cc_c--6oh1E7h05U6^YBuM!ZD%k_pKM6HKcojsJ{n3oWr5%fc*I*ezCVwB2Bug+&FU4pFve_%=dp zQZhGm!w4Ri4TE8lD$!qPh9Oq*&5C`_HWkA4Wr<)uAF&ko9U`JfgqI|?8Mvh~`6A78#0hwGvIs%rPM>$NUD@KZh14*_o~Y|KaqsbgZT%olcsRCt1@A3B3{A~p!ceh{gaxecB<8!J4%TWB!Q^a{Q5)vUoF)lI|7)~7^9 z$vmflmiUyCbalIz%J2|dpFWbiLC!5ZM_4^(-aF4)pPI76xn2#}=64uDw!Q;R{WTl&I@QfKo?5KXO@!?yVAVYqvvj?>YG zE(PDp1{K;OhP7oDHUVfsq9A5AIHyepmM<(A3%ddgYFl1bp=lZ}J6ItGrY$&Lj6n>% z3eR8k`g&1(l&z~U*_^SS~MN@-|t7tZYq-#V$f23Rxwep>Q93wnI<_ z)2rJRg%!BFBR*$h$=DUkQC6vrZ+X)MQn%-=!*B{wj1db+8C&G!szRl%SO{mb;SFQ4 zq{DwwzcWjKs@$v}TSa^WR7YhpP1%LmJjKNmHZ#+z5j9W)E#@57wJ5C&V7>r=XSL`I zcs9XZ4#^P51@V#GngwoQe2XSKuX9% zKwD@lpl)Q&8qSy0##f*cHjm)b>RYtS_+v*(Asz6KM`@|yla0oRP#k=abA_jk370}5 z1S%z*U8|F(VNYX*6rD11L_&-tu4~j|(~G!}BQQwJ6M(mDl*7eI1V0HWwB^YuG07p( z*8Cx1L#+AHVc{s|LNg4@gH)nuHZPhml*^cyFeW7~NwVZ+bQm)+iQ|w+8xxn5;$9*` zDomd>IMfeF|#-x!BQ^$^GvU!Sz6d%0e$=Aj8fVkFYWM<=ADMJW7$QTVZ1S++Ze-n=r( zOh_8WPh4zzxKsA!nJEb);u>-3=T6v%6DCHFNl7E6xV1CV{UibgkynrwDna$has-=Q zS+Yl6vL{P2dlaEdn6d>JCf9`pJTRv@0oN+XAyRD4M=kjtSJb2I9!j~{Mex*g&6Zz# zWm6TdQc*lAJQjMDhP{*;oM8ygn2ePT6$!@m4!9vn$3oD7@VS(rSrMb5V7iP*6gfuZTacwfJ;i17OcV2yyi4(`0M^{5cLT%I&vnU!4g9;;gt zjj5YD`_qOBCM8VAqFuDUGUsF(XruJ@Tv+Ewa7c*h^RO$H4HeLw)0qsnv&{|HWUG6+fDjddBDUS-;Arcj#2Otj%!*Kb%c*~}Ie%dsS` z*&vu>NogkAWT7yRop+Qt1!g!}tl?rg%{V^w%CaK7>LM)B*>%#oNyCf?PC}3HeLq+U zTQbp}3lp{omnCmkg4~zemJKm*ZP-XC-H2mDBt^OP0s*siCdC2Sx%GulqX1i)NxK)a zTeFoFHTHto0-0~EnCq9NLJWiLQdoNi*50w|J-$~({nqqI7?Qa!W>q1LJ45R$C!ypvSMj(GScvTlT`mg&WjNse zx}L66SZaS=57#ODPk&v6q+`2nGzH*(0`y*g9X7ncxxY?i(G<}*i!O)b;0_EvpudiU zVY>=U3cdh=MTTJZ38fgD?Va z;pD~jNu>ByOG;psjuT4p>pv3Ps*qflAEja9-UPbn18K46XqxTXb_vEFq}bzNyL_}D z&dJAu6^1AEr#Yv;L@RHpKW5baQW|YGrRB{k>}Jg^pnZ;qo4+&c)ZCK6l&(AED4yOh zh{K8ET--D(g-1XA6dfOla!DfpqBuVpqiX9h;4KgAlY>FQZ?~M+klu0emUBPg6Tjbb z%AS(+>>szBy#Oa(zU7PuOa+_-I2o`2Fb%K-&;J?*aD%UIVNF^wmnzfF@372w(x=K)|;Ervv`%>vX;acsRi6+yj`` z)aeY+Nz%K`P#>UwbEmTi(5D6J0X);v={yZMs1^8Pf9NSd8L&TIPtyyq1hRZ<3e$45T}jKd=lL3;EHU^w6`dPD;7 zG~f!r(ReQUbdV%n0Q7AQ`XZ-u0$>VY4xnZ(n7e1Lgu=1Uv-jdygay#Y4CufDs=$ohg7<0CNDPP4p5*Nm}p`$^kmI zLcjMyj$L?^2C!x~5H1IQI`|BMVz^@9uEL+V;~od@Oat6&zV6DCszX#LP`s)G)gtW*RX z>Eb0q4D&y!Qa=OEJnwPjtw7#8uDom?Viu3{4amC>{#H*48{!|ZTs_1;Xqm?lf4S0g zh=0gZO|*abVy|fbes=Fz|EU%q|9(J3`-gx4geWkCiN)IRH+Y@7bj$e^)l;txQ{0=t z+7N>JM*n%sDa?%F@Gd)PGI04+9!EI-$X2!h*H*~4l=QOLBidiKdk*to>#5%C<1Yh+ z>X;;?;}X!m0N;+GhbMjg1I9uVq@!nnUkAKh;B%Q4&?h*j4>7ZOfbzi1u8#GOQcv?y z^iF)g2Tcm*h+Zxl_2{|(wq zcO_Ea=YaOI&k5rdEokre^$m@XqCjF`paYa%&2|9Qc^PZ8?$TJBYlWgsfw;y>OC=UnG zhXZ#MxY2}wY<9Iefhr>UMC3K`a5{Ta9uCsaRN%sZ8%PM4pSwL+6*E9q6#kZib|7f` zlANGjMz&o^w!PF7CcKzz+wK+XpRE4LhZ!}j%H60*cSpdZyQkB64sGUo;C)VUg$ncc zI>Gy{<0jc-k?Ib8PWICaeLW6yfAoLDYpO?x>UM(=d`O?g;58iaLK@OsUiDKG5kb#JHw|?BF}# z`Xi3A6GHukihz2mQmB0&gmk_)DinR2=KkDMZ-E={HN-^~E)_9q4z`D@88z6bsX;8o~z;G<}~ zT?FnR;^9w`CY*W>cX-6d7cur+#KyCDUVwTg=hF%J?|^S6@WiJdaNh#Ans99X$zhB_ zaGHX=h+B}#eGib1lnTI9tZ8if{$AqQK)nz)%P0cy4~mGu^ZZ$Cj2zjw+DGf zz~GXvd35I+f{|4WG@4;W(w}&baq6V>~0DiH{nx&4+kDg7>1__G8V}k;O_@M zkMRFgca(bU?W#^j|9uEPiNvQn_|)senH1=S5Ap9e#6POYEnRSjv^&lJTWR;Y+-d&#msjdE>9#j9* zK60o3-?Yo!kGb>wKb`)+QRX}85?4PT|*A$0qTj0&5$xi2U6r0tH zsnm}vbQG(GgYG!!#!+y0_ZSY_T^{PU?hvce`eYt>otc8y$RJJeBk^AW+)3cx6LIui z*P+F#5qDrO(VoEf;1xGjd@B{Q-hMyDBV9!0?prBrZ=zjG?46tNwq%kII>BB~4DC%& zyx$LbXOY+JZt=ca#WovUt4Wj#!Jn1*PIEdxM_Mw~+dF+s(KXh(jCL((P3iwkOYQv> zw4NDw)erH#V|&#xx7h+=?e%SiZb132RGzgro0`kk+abssgSMAA~_F4H}{;#0j3)+=L%lmV>vNj^weS;*a&myO@)!k+HZYVpIjYrwQN1V=$VqJCH z_1|;YNu}KFCX!jB=>QL|S*Ao8~z(4YY)9FKfFpS2WhZ?(NZ0-6M z@(P}GIv3EM+CS+jYWy9v#K$0A4|@^Uv)DdPJy|^_!5_FTV8o-UPO!(5xaM^odrALT zZ-K{VPX(VYj)5+8y#4(v*Vh`r)&Cj zDEYKCK*vdS6n=3(ow)r__T=Zd4T>GImY>tDA9TcveA+&sW4DkOm(tlm`ww(r%e3A> zTP^HJ=JG0g08>Qv|}pE#XX<`D)rxT^4lr<33{hE z7vf46#rbJnlqmWCF-YQiXjtnk(cg;&TqEEs0&Ws;pMc*8_=|v71oYDLcC{4negXRk zI8?xK0%i(0OTfhft`YDR0XGS_Prz>k{6)Yk0(u3A`USjSz&-*F6>yw@nF7udaIt`E z1bjunhWfhOd2vZMc55Ng(5DOB53+xHf*l(Wtt1(|CG-L|(j)j&^6f~MFp7pht)$lQVr_6m z;U3()FH84{e;uWc5}wUt|Jvi)MtcblvP%Z`uN(INd$4~!rJhoR)SLb5F7=h@udfs) zMY4Zga9yX1WRwQuMFP>%5d4e6PAB~vBn`t~yz~J64VOl+e@Rjj?g31e5~R`i8zYUC z#_l`rEF;? z{t6`v{>_q#q`CO_F#gTKGpw_vh4?F$7BM|RE2OeUhoV0v!(G4RtCf86o7`8HN{gj3 zsa#qjRZyWiW1u8q>K#gX1-V4nJyFtiHYJ}fH3TX|^`M93ft#W|G0ME~r)B@VB_DYB zCXz2GaqlS(hp>|!%S^2F)M^fk3k2NHA${J44)}3)M6Ks|^7jf(g*5%qk)Griu%!Dg z{p?9CUj1nIA4T3@_V_V1eEzPkH$G^)zWT||H`B77U9@8U?BD-*$GiJu+IKdaze;_0 ze3etYnlh_4TP;#{5^nbqv(iyh1+ZTqK6rtD2kSn`ZVc<8G2n?6f7jK1}5lPe3W z+COt`Y^xpCs)>6~4*NU1Pt{lBmc*4@Z9b>fo=&0fUG=H#bKj3YtJ)1p7&QCciJfMp z28MpI_}!Pr=#0B^H;vr(!J1J&yw`g7jm6&uuf6nY`mzr{?R@dOC4QaHb)B=y|9FQN zb`*Kv`q+1O_3(2CcHc<7IVNx5557I#)HU~vD7EHA-?ZIxTJN=Y_s-|q$X(C=xGF8& zl(F~6nS1wkxVi3ByCF9;!_^C0myP=C#_T6@My(p*XX^KX_R^7$K3&;4u-Acar_}`B zXRTZ}?AgQF565KG>QAQ~YGx{4b@Wug2cv=>xzv8Hrpfm|E{jP0Va3EtY3aQWAD=$b znH(^_aKrKAebVD?_r7a?s#W)xvuBU&Os)O1!_HmzmPKy7)X{ItiJZ@^U(bB~>!VMc z`Le^+z`o9nhbMF!eC%hhq{vn?=buIyw`)&#; zd-F=vfeYbVs+&D}J}^P|$Ghf|NB_9)yUuTZLeq_>4!#xp!eb{_tIC(2Jn+qZH$!)< z-&8r|_#4K!NAp&zCK)5&`Lm++oA#=nZ#_3?viFHSGY!KcgJ)-KSrVVyW_ItjMOX8_ zefNWJ*6rNe^G2Jerj;+b@YsP#ev^wAKI8GUw)3ZBUix6o`{NJ%xOH^I>6Qn^w{E2y zmHSll>K+RmlRv)sp~piVesB){VZ``J^JnR72j&b&DR^__!CQOFAO2w3&CgzxS2o%3 zr*UHD?`HkwhbwXh*?w4*dgJnxum2diBl?NTm;J&!M1QXucDU)f;qP};pZ(;8*B)+v z@AMPz>^s}>=vVDKzS?%&jUiE&M`ev_b2L?Z_~_6fXD2slRZ&y=RHv)Yj!5m;ab->9 zr5$ObE?$d%FF*9rQ7^2Rw)z`Q*rC6t=zh1hczyT2N&2n_U+lPZkY?YaldWr?h-_;- zd};57-l^Z6`F-1a?Ur|5?z=nTkx`YKOfNjQ^5omQL!X~r`uJPNUr#s{rt6d#e4|&Y zT;Ar*{iVSV%ou*mqvJ=5*DYV4`$)puefxiTAgIaoh1>F9z8)3^iXsbx8=7uvS#)17OJk7 z=Pc|HeDsxVU#G8)Jh}1N)r&qK(tG;MLzbqy+ID_B>%ln9fZD$fzbEeJprn3?*d~qc}u|FoC3f4c-b?MiJ&maBlnfOpIm49lRi93$;sLJSL=-DrAPusBzkM3Q0Y}*U} zdE$lFcZIG!ap=h8=&gN!n%LyyX?>5JUDbMA!h-H0TSi@4HmJ1r<42#lo|&dObG1+B zG3g5`%^&w~{=vqsNhjKLTQX+CbprVXtuBWU`#9DZ41NvH?;V9%|qoaURv|+WuMHL z%9tG%OM0slj;R?nm2vY2KQ`mrG|&8q-bW4%Tr}cJdiJpu$5#0)o_Fw=sWR@=QPS z{=DoDwtcl|;-%g_hlak;s(0uV%{^xdDow|)9oPJpIs1(%_TB1-TH60;xpCEf0gtaw z{;bWY`@J)451+_1y?;vmk>#OfXHWdlI`Z>TM-R1X7kOqx_@7^F$vRv)Xi4zQ#MHn` z(@yp|P`%@w=dOkxYn%Dts$pGc{b$CvO6_sfJiUXxKe<%#=Fza+-PZ@15<2{{W#vsz&-advTw7cI z^ZJh4Vpd;Ym-F_U3BDb=j;Xm;zI9~j$NLt3|LUl<@dNsGpV9NfmrZRuzWY`6VD;V; zrEjbsA9#4}h$~)0c1N5Wye{DAwDILnHtV@I@S)8w{V}xkLP_V^kDkA8Ot|l}k#8?Z zz47!rk9_dL^VcV43}5-}dCj{&1a#it{@l*xm2>?T)I4UJ*D9cgdGOfr=bQ<(4~%#x za&&3j@ZlZW=^j7y=Nk+1pNpTdd&ft=roa1YsNdYccMrev{F)IjO_=ri$2-y%K2vkQ z{{H;AzxSH=^T*jO+RU_kvfG%FRr>l+-?xvAynkJ2liyno_(7U-ct+~A3d2_~##9b` zVB$wTXB_zDi;=Hy={Ki(b@jcvUKf6PZpKb~?Xkgr-?kZAdyoCu4Jujl?ueFwb5>$f zYoYD3aeN1hJ|ceUzK;if-jvVkN1_8d^OORWxMx@lo`DY;mNYh0?%l0tw{Xb~(U&23 zIpsGD2_A#<=xBpjUvyOn8bDen7S0pfE~RoP&Bi+5Hn*72Q4L zdmVC7_9XnNClJkdA^7#sdjAD2d8oAXOqqw;I~L1z4^MBpgzus9TE>tX`tqo!r-t6{ z<)PKoA_P;j<}95^+y+BrbtNUi?IV=eXuY(hbgJ@NjgsDj@$;R>W%}l}wv;$t8I4>? z8%s1d7E)6CBba*pP3Zt_0vLMSq;!z>45e>TTGnT{(U|RP3am z&XYt}vy&)YCTk8miPwEVWEysotQ${^z1YbFT?TQ}szw7hRX2*rd{h%~GF|r#$>pme zfeUnH#4UiGSasv5o~Ej)$SKkV&`C>GADk5Hz9ep~RMfmjbaV0R5u|E{4zcSVAqMSK z9dS~odyvWmt7d>;g|0oFgs55}w0}}pO$?)s^+822HjlB z>7k;Xr7gM@#JVSwZHI0V<@8o{2ZKG5&s=1w;#pP`PtSn9;Nfcp&a- zSUIp>+U58SpprY02xLE`$G{8pbD4g?M+)?%A0lHvC|3<~Z<1=dR|*x-zJs*axFXO= z+WR4c*Z2iUYqc4ao=8OlwA(11%1vh%3VBW9rt>MKrz`-65bbl6PHT#?;o66Y=hVJP z_tPGyvZnD!M`_c*&C5(Yz0ul1Ti=?U6<2%k$` zG!@NQhBNO2$PV`^q$X>3z@ogYUZ_UW=20;lrL|gm@q^bKViBNSOEmK--CR4K*e#-T zkai}1z3kbwpiBMxo_;TSg=Sk{_wwge~MU6&&% zF?#PXA`Fn4M0ww@NBzExAcP2f+v42YKujd{M#$~mjaam#7jSqy?M=@-2YIZeA+L?Z zkHo-=kX#9eyui*NMB)Hf;M#k&P%%#M6G;55U*BJMW>zyY^9(^4OI_XzdEnce^DU)|rDo(*0_g|h zlek`5k|$sal4F&uKr*U8cFKOHQU;A3{*%c|rvfx3KklU^DlaWjcxgK#&DgC*g4M*? zH7Z}I5FV~iNCP>L{jiL$D3|@vhrUq(WkG6IG2y+m&)}CCC$(K^+!+N)%5jsUjy8yRUji|oi+&*95}%8Hq_mdLMJFg7z~`cqln&x^(J4yHS}hoP{6y&x zEt`sdrgXTL%|xdu-A~IVqF*Q-rDgNbSxU!i*)&u`>16Gn)M>ReUM6Tms55`1^i(aI z8_rYDO>e`dlM5trh^o!!MD)8BUOrqU`H^}&kY>Ico?{JD9o?+il+et#)666Cy|itZ zEp!AgmN!_*YbLcl3trkKGz!|Tff;JcDA~@2hU$VI0-erdg@{+0((s^{Zy-7{!SuB% z8f$crRn$c!oWjB=T7!EODCkS+brh;VxQIYiQyCQSw*4`WdzA(=)GEG&coQF%85za~wnkP4?-KNp97Ak&FcO+qs| z^%4AWiYN42sp`u4)|G?0RH}q##Ld5hl+dg@3hJA=(FU|ob#BcG0yQ8&2i(sWH z&6`1rfvw@*hyk3E(k}QGPbP0dGezQ{5YV5AY@K~>U>V?YdVJI|I^B_`n!{3kZBBCh%ck9;OGRJ}!Wm&ox_3M+?rx#xQW5qj8 zyN#i2=u)l3q#lD*9s%8kbR0CIQzzRjj{xg*HEl4D1({kJNxT~J?w*%j)SZ0@qkCSY zDcxk6QDmAvV^+k>o~Bt55jl}P3;GsjW%MeVX~{H9%g?vsQ$MBx1K$0VW9gogJ*|6I zdb$wGAl}f1Pb}rxiVRtKw(e}b&>iob&9UJH&1eQ*3y2ad(xwf=RBrkcQfZsC zX`O-#Z(iO{-fQ1q-hHoW{F@*kI1GZn$eO_xe-Oc+I?4beFqx$|h$uzC0Y|Y5oSC{{ zTv1Wc<=3=F41OXsVnSDC&w86m*Ne03&F<9?39+m0?+e0bKhgyE?Ba)zW&^$OQ9U7(tVw2 zd)O>ldK|Dz|F?OR=JRmhb=uBaa*taY6`Ue6cO=T1O;sm|W6 z-gW1uqPoFX!NkC5qPJ^xH>8P$$HJNkw+v%dG3sdglv@*d>IF1$C^k#3pSg{vh+)JT_G*%06i8p^?tDYp|CP{wC7niO%8PL?=|d9#)H_o!OBs z8}V5x1C*_;I%T!FEcPk^2$KHuI`bviA9jVx%JTi0PHaHb33EZcu+0F_s;oPQ6(^A& zRt6?GEGS+I()(TOlYy?$UFD8XeHn3PXR{Ml30H*fWLS4KP_gGc0oYH0K z@u)7V&MkUkbFj<&N zPDf#>tgU^%{&fzCQcV%CalPKtvr>ooTspzL%3fzb0*@Ff!+PwUjJ`Sn5(aM9KXbXRuSLoWXyxDjLLkj-oLv9Ub+WP;5eq3$-HuSj|Fg zt?Al9t*i}9oE(U1J#T{#UUCI;lSo><*~{qB`A^s3JHzl_zHn9%)N`Sn6bD@%-wXEy>w~*VbyhP_GWxoO zT?G5GmJg%@nm^ochz@c6p6i=jhv)hwN9WFddY3Nbdpwu!T8@idxxn0l-(wTU1#w8P+c1)FaXs;eZ5UFx_@8F{c+)CwrVTHGT)a&){Y#9C z+iAv6G%miU8GmUb?x`7nnHi%zoAG6h_npo7%Ny@qoAHy3`+m}lx0|^I@g4Xkfp<`c z&K!u7>UEo0VO;!G{9&7Ug>i9L%{Zc*wkP8d`Mk=^4Y$Hi#`nHfc!vpgw8B@Ku}fRw z81J_@+VtDi!Ut`}MUyo@Ytxksn=!d-Lxe`FqfNi}Eqv1E7FmovT7v82%uoLigY*(# z*;?WfAJ&Rq-YG1_Vwy+W16<7?m*GBJLbNlVynPp>2X zLTGWv=MBUIk53=*ArJp^;v*h@0r7qh-$dN7JTBi6;wO0crNk2+pA7LimLFe%^r#Vk z&ciP!e$2x^Nc^ZLhmR3|-lPArqkn7CW{7(^{u$?1`Z^2W+m^^X>I()eVeGRNeIMxY zg@1v67*swB{lhTneLo{_^YGGXfxnVBflJInzi|!l6|m1wek_oLW=21a`3UhD_DjkZ z&u$_9mG1;fsq=Jk^*P|nVV`53zGS|#@c-D&mOddbZg9+!KIhRtNc;fh?Cj(S@xa3$ zCI5Y|3Y725^b>0UlYW&)FK?)%oHNY#_tfLFKSVh={#(fZ?EXOc>NFTX);?6E=H^ySP_Y*Hjf>X>wk^Q^19P z>B&I(>b!egjpAjP$nBU{{&$m)`8efCeO*I7N7zpBmQ{}r5`SxNp!Wl;SYlagIm4i_%I?LxRq<<0gDEK2!Tiix7;FmdgAY;zHTOdBl*vG?eu1)CsFLw4?Az=ukKic z{+r6b!|d_=#u24oW_GaObn^e6(!1#FcR`MKDe3^Oj z>_AJhljV{1gr#2B4q9B-bj7of{AbDE^=o<3pG ap0t*|E!g>>wgcB{)z8d{<_u) z_|G`{FI#$7{;L%4Fk{s35&U!^#|OygeOm*)e@H*EmNWSrC7&yZA0++Nk68N4h~KU_ zZ(^r^Qa&AKrDy-&ApU^oZ}o>~@h6_X{+0RO@oJmzjm+a2;+L?0*-!jA;&)LmrxX7r z@hRFf#b9273$dTv9nErkC2-MW=Y2L`8Gp<1O0`>i9sfLqd@3HF(}+Ld+5cI@ulDNO zMf{LQe;)A}@=q}H4Zx+GW9I~lNMM*87n1&?9{*v|-@YnPx)10l_Cg{3T^@Z}=}8nj zUA_qZkwx&^$o~+_@9h6eO25op^7=rz%lB~@xmOq-m9-ji9;C1};Wu@;h70)mIqvO9iQ1Xz8WG!!L zcYk)!;^z>5P;uVGPEQH{r5$F7{N1Bx1&6*?(SC5N$FCOQb0Q{Uirj8xy&U~XiqF4y zb#{0va4F{_Ea$hVNLedf_}t>@w~O?{q<=Td)2H+u<^->t>&d6v^BV!_hsfWR^G&3m zW%=EBatClJ=jo3Hn&bV<_btS~KzqBB_yqa%d-?7qKIGv=^7#+)Kap}cpW})nU$b`N z%DLasztNWGa^@@Rpo`o-<;m?T#XHPV>USmSuO*)=*?tqmZz7%~ej@SD5pVx_ph$-J zy~=;3dBQ8_1H_Md_&13kBaW}bdOW85c@sMwQ+n7TzqdL${FHdVr}y73!smVHCq+Ky zek)Hm9&Sek#mAO8X*!fcFe?+}F`^UDBYFEE! z`~5BXV1rAgPmsT>?;DBFdVDq!|Foy~5%SMo94O}!`M;U;0r}4mAAo$?A)k>Wln?PS zrSE9WYjtwiOWe&G)kpuo~zT+EO2KUJ3J^M4yC=gs8*PL^ku<#GN{*0dKsFJV8j zi}cqqUpIgD4B`@0EP8o>e4LzbAfE%<1EqBB^dR{dzAv&*v6l4V=`G1P-?hyI>JMnwFZN4`zu@C->`0+a} zuKNby(a*^L1kca>8o270c4E08E{@}YqbyH?4^9Fu^1tsZfg=Axyo30K$1JYv3F4VV zq6z)uYb|~;=~ofo&F{aTAikRTqi?YEy59_*od;a>_*s_U>G5{f_Xh)({&~tFAid%I zQP*Au$^Tb>YU$m0X(#EQ@Y>N^NPo^bmc9>Vk>lOy-^D)!q<8#7@)`5wd@A`|w z2lNwbSQtw^9caZ+%djrKgm~Rgf3je>OoYxV* zNBMM^cF&(brF@h{)5ljA!N03~R+`7Wdi`J#`Z>jynLYHAFJ~?x$|ZJq*wgzj$^W+= z|KBabfB7Qg!`CUk%sf3CXpXveE3UfL-thaQC(pHu@cA|U-XYSvam!Znxz%e&dx*c_ zm4A%*;cqwVai8Y9%wz*w&cD>sV%7`s$8WOu!^Gc4{OxC3d_D2Ylz)fm_vCqv(vv85 zI;iw3%_m7uGclhg-tM)#&nq9;?JApZ7kPb&^mlpnx{vrQao3K%PTY8Mdzkz`^cu^* zLjK<)p7Qejq2eTpot|F=e=*)Oi@nW0Y~^orL9{V&X)iDKU(R}6PWn3e8;%E@AHInAZC<{+iC^#OMfS0j^8cLu{wt`+apJerpZ7A~ zJo!9F{x07t@mY`mwBj8m$NtyR{}t))^7vc@T*~v98yB5xGrpeqFK!GJxSQp?k@#7I z7SCF8^Ks(Gooewl#BV2l`dwb8z=d%5!LSbre?rjs}`zH?c zrMo*3tlp_pR{!VFbxVdQxADwGzSLF5R^wG%A+!zwn?>xMUM^wRctnSmL%Sz)y6)BMS`#5Wx0DZ))oOAYF?zM?w8>Txz!|3N#p1L^^)>En&}^I( zTWBLFZ*Pz8v26DC+Ox(0Zx0dpD!e9&U~38)#Lngrc4{W7O>`UA%o@+m?;ZPheA3 ziKRqnd$@Us9ELXSM40u~;SB>@!{Ncf(apQUT>~4oZVnA%ny~@BND^rzI6g#NylT`` zst89d;*^o?whhdKo06NT3NlSoDwGkqIhZrLMRu`X%OE6GB7jGB?=m~WvMD3FIm%(4 zhgcHAqNhxyUXzH}Ah>YrmJJ(2#Nu~B{IbJ#Dntmd*@gi0a>`89^SVX7RN7>UmD)67 z@i8w0tKsAkK3X%Q;eawlbaQ0V*+{GfQPj{;DOH(nW?vf3CDUp&$y83lQt-Z#bE+L-WJW>=2YZ7@2+0-R3km?`Mdj3a=Y`oQ zl`LU=jZbIHKSsM(*7Ya2FG z)odKzKDx_9CHTBr9%1*Dih-@C_NAs%1(XaX0T+Ly1Gfqd1Js&*DdB-R&- z!PO8-E({UVjtdyAs1NN{+PHNQX^GM=PtRLNuYnhW#hFYtZFWVqVHmKn+7Lq#VPf73 zOu#jc3R<(wQ4#4W<75rmRIs2(Jy}hH>T7VL_6i z*rljgo+#zB=(0;ij0+0tG$v(c0R%WvESGG-(EaS%HoR#wTq6V`bL^lmcwuQMwX&Br zMiP;zOeeLdt#Iy)2srMUd)Am*E{~xHT9!^}u@fjJMdYSbwi=C)6Xr1#Obs1THh;ie zQZlF*yTXJe#Ran@e(LFo|c7pfvah&H;9dNj#;pw0M&( zfMeV&wXcbpsZ6kOh9upheJ*X(wv~%ySfO3RYGf?kRTyPSrnlu}8m_sFl%<(9qt%K2oHek44>ABMoAv|ckG*L~CL)2(#sY)H@t}eYE zB_}dQs|$;$mupGbo>N5CWRrRHE*J;S(NRJFGPe(%wl*DD zr*@6IDa?5{RmboKwcoGmsh89)(Q}ID6JP0d&!uu$1$DMu$#~8tN5hf%cc!A*cm^;X z$qdbAu#}k+QDG>6Pbo&$%A%PnWru|_d^IqMarC0|E@-tuG12FSJJJ8asl&3wm6|dv z$c~c5<0L)*J}!oeWE*Xo5fN6ytM$OE*{(hrvX6ja+RmeDb_i|Ms+^evc`qC3B2ctZ z7Ojv+_r5oYP}Z!@?rE-O81CA(kt1O{vbRkzk8d%U-vjq1vl!9KOv=DU`V5SA;3W&N zTDWL&Js2~hviRJVJTP8PPiwQ$F(W#z$$F-qk!0FtjSMiP#4?LZ_^C}=W#pigGCJFw zw89M{DvH*cqq~4obfVud zU6>czrRD8PPnVF`=oy;TCo<;9mrG4IA)aA|RZ<9fRl$_QE;alvd@I1Ud`-l&vJMct zGC555k}rn2G}5{|o5FsXv?<&*7$=K)%-@=Tzn70L&A>8)S2101XZl64E1emyPas{g zG=b3pZ*{Jpdo(_dUf4a+krJOkE)Hh$*z1D-^W`Z>DX)m!`-sZY0C#vVN?=6q=0Es4 zsR5jcD|v_R($6jpaA)J@<(!a@*x}x5IY@q=z$>Lj`lCw&+!@UO(vu08q0q?T-d{LA zJ-~j6wUAx@iQ@tx!#puP>E3a2<)^n#5hsBQyz*}3@8*%o>M(LV(Pq!`d!7`<@X|T- zDlfg8XL-fXEd|x+$W_*j8(dtAe<{B!rkmGyJ=2f9Ax=FnKZkzUOYi3Y&7CG(jrlC) zuQ&Mc<@X6-@%-I9!9!=-^f_@5vBT-lL7&5gh}vc2=K0KRv*~?$ckj-3Bdz>4=hC}* zhcEn*>F-Bcu^pGbF+Xv;&413G8usP#b$0M=q!kjE-pym2lXX0BI6A$-hfD9yj{=LQ zZ_Ia;31c|=?MbiY!=-cQ?*ogccX4aM4x6wYzq7=TMEnNVVxGdwm4A%yb4M<<>F27= z2@=h>=09;Sl-(Zg(x2hsma9!8kLK|2usG=q^FI;?aqY|V4~wK9d8_66v=bEh_<6}Z zL?08<-U*9d={@vrIWLjSW2ZZFmhx?`Ve*-u{XqZq0uKv@^+~ diff --git a/tests/tcp/tcp-phi4.pml.trail b/tests/tcp/tcp-phi4.pml.trail deleted file mode 100644 index 7ac32a2..0000000 --- a/tests/tcp/tcp-phi4.pml.trail +++ /dev/null @@ -1,192 +0,0 @@ --2:2:-2 --4:-4:-4 -1:0:139 -2:1:130 -3:0:139 -4:1:131 -5:0:139 -6:1:132 -7:1:133 -8:0:139 -9:3:0 -10:0:139 -11:3:1 -12:0:139 -13:3:6 -14:0:139 -15:2:0 -16:0:139 -17:2:1 -18:0:139 -19:2:6 -20:0:139 -21:3:16 -22:0:139 -23:3:0 -24:0:139 -25:3:2 -26:0:139 -27:3:21 -28:0:139 -29:2:7 -30:0:139 -31:2:8 -32:0:139 -33:2:9 -34:0:139 -35:3:22 -36:0:139 -37:3:23 -38:0:139 -39:3:24 -40:0:139 -41:3:49 -42:0:139 -43:2:10 -44:0:139 -45:3:50 -46:0:139 -47:3:51 -48:0:139 -49:3:62 -50:0:139 -51:3:63 -52:0:139 -53:3:76 -54:0:139 -55:2:49 -56:0:139 -57:2:50 -58:0:139 -59:2:51 -60:0:139 -61:2:62 -62:0:139 -63:2:63 -64:0:139 -65:3:77 -66:0:139 -67:3:78 -68:0:139 -69:3:79 -70:0:139 -71:3:102 -72:0:139 -73:2:76 -74:0:139 -75:2:77 -76:0:139 -77:2:78 -78:0:139 -79:2:79 -80:0:139 -81:3:103 -82:0:139 -83:3:104 -84:0:139 -85:3:127 -86:0:139 -87:3:0 -88:0:139 -89:3:1 -90:0:139 -91:2:102 -92:0:139 -93:2:103 -94:0:139 -95:2:104 -96:0:139 -97:2:127 -98:0:139 -99:2:0 -100:0:139 -101:2:2 -102:0:139 -103:3:6 -104:0:139 -105:3:7 -106:0:139 -107:3:8 -108:0:139 -109:3:9 -110:0:139 -111:3:10 -112:0:139 -113:3:49 -114:0:139 -115:2:21 -116:0:139 -117:2:22 -118:0:139 -119:2:23 -120:0:139 -121:2:24 -122:0:139 -123:3:50 -124:0:139 -125:3:51 -126:0:139 -127:3:62 -128:0:139 -129:3:63 -130:0:139 -131:2:49 -132:0:139 -133:2:50 -134:0:139 -135:2:51 -136:0:139 -137:2:62 -138:0:139 -139:2:63 -140:0:139 -141:2:76 -142:0:139 -143:3:76 -144:0:139 -145:3:77 -146:0:139 -147:3:78 -148:0:139 -149:3:79 -150:0:139 -151:2:77 -152:0:139 -153:2:78 -154:0:139 -155:2:79 -156:0:139 -157:2:102 -158:0:139 -159:3:102 -160:0:139 -161:3:103 -162:0:139 -163:3:104 -164:0:139 -165:3:127 -166:0:139 -167:3:0 -168:0:139 -169:3:2 -170:0:139 -171:3:21 -172:0:139 -173:2:103 -174:0:139 -175:2:104 -176:0:139 -177:2:127 -178:0:139 -179:2:0 -180:0:139 -181:2:2 -182:0:139 -183:3:22 -184:0:139 -185:3:23 -186:0:139 -187:3:24 -188:0:139 -189:2:21 -190:0:136 diff --git a/tests/tcp/tcp-phi6.pml.trail b/tests/tcp/tcp-phi6.pml.trail deleted file mode 100644 index 63146ef..0000000 --- a/tests/tcp/tcp-phi6.pml.trail +++ /dev/null @@ -1,102 +0,0 @@ --2:2:-2 --4:-4:-4 -1:0:138 -2:1:130 -3:0:138 -4:1:131 -5:0:138 -6:1:132 -7:1:133 -8:0:138 -9:3:0 -10:0:138 -11:3:1 -12:0:138 -13:3:6 -14:0:138 -15:2:0 -16:0:138 -17:2:1 -18:0:138 -19:2:6 -20:0:138 -21:3:16 -22:0:138 -23:3:0 -24:0:138 -25:3:2 -26:0:138 -27:3:21 -28:0:138 -29:2:7 -30:0:138 -31:2:8 -32:0:138 -33:2:9 -34:0:138 -35:3:22 -36:0:138 -37:3:23 -38:0:138 -39:3:24 -40:0:138 -41:3:49 -42:0:138 -43:2:10 -44:0:138 -45:3:50 -46:0:138 -47:3:51 -48:0:138 -49:3:62 -50:0:138 -51:3:63 -52:0:138 -53:3:76 -54:0:138 -55:2:49 -56:0:138 -57:2:50 -58:0:138 -59:2:51 -60:0:138 -61:2:62 -62:0:138 -63:2:63 -64:0:138 -65:3:77 -66:0:138 -67:3:78 -68:0:138 -69:3:79 -70:0:138 -71:3:102 -72:0:138 -73:2:76 -74:0:138 -75:2:77 -76:0:138 -77:2:78 -78:0:138 -79:2:79 -80:0:138 -81:3:103 -82:0:138 -83:3:104 -84:0:138 -85:3:127 -86:0:138 -87:3:0 -88:0:138 -89:3:1 -90:0:138 -91:3:6 -92:0:138 -93:2:102 -94:0:138 -95:2:103 -96:0:138 -97:2:104 -98:0:136 -99:2:127 -100:0:143