diff --git a/tests/paper3.yaml b/tests/paper3.yaml new file mode 100644 index 0000000..76f4cbb --- /dev/null +++ b/tests/paper3.yaml @@ -0,0 +1,122 @@ +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 - shared channel model (AtoB, BtoA) +# +# A sends on AtoB, B reads AtoB. B sends on BtoA, A reads BtoA. +# Korg attackers directly interpose on the shared channel. +# ============================================================================= + +# phi1: safety - half-open prevention +# always (leftClosed implies !rightEstablished) +# Expected: holds. B reaching Established requires A's ACK, which means +# A was also in Established. A cannot reach Closed from Established +# without a full teardown that also moves B out of Established. + +tcp-phi1-drop-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping A's messages prevents B from reaching Established; no half-open possible + +tcp-phi1-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping on both channels prevents any handshake completion; neither side reaches Established + +tcp-phi1-replay-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying A's messages cannot create half-open; B reaching Established still requires valid handshake, and A cannot close without teardown + +tcp-phi1-replay-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replay on both channels still cannot violate the structural invariant; A must pass through Established before reaching Closed + +tcp-phi1-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: reordering cannot bypass the handshake dependency; half-open prevention holds structurally + +# phi3: liveness - no infinite stalls/deadlocks +# neither side stuck forever in a non-terminal state +# Expected: drop on both channels can strand both sides post-Established +# (e.g., both in FinWait1 after FINs are dropped) + +tcp-phi3-drop-AtoB: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: handshake completes via nondeterministic pass; then attacker drops A's FIN, stranding both sides in post-Established states with no timeout recovery + +tcp-phi3-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: attackers let handshake through, then drop FINs on both channels; both sides stuck in FinWait1 or similar permanently + +tcp-phi3-replay-AtoB: + - 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: replay attacker can consume A's FIN and never replay it, effectively dropping it; B stays in Established, A stuck in FinWait1 + +tcp-phi3-reorder-bidirectional: + - 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: reorder attacker consumes teardown messages and delays them indefinitely, stranding both sides + +# phi5: liveness - SYN_RECEIVED resolution +# SynReceived implies eventually (Established or FinWait1 or Closed) +# Expected: drop on AtoB traps A in SynReceived (no timeout modeled) + +tcp-phi5-drop-AtoB: + - 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: A goes to Listen, B's SYN arrives via BtoA, A enters SynReceived and sends SYN+ACK on AtoB; attacker drops it; B never completes handshake, A stuck in SynReceived permanently (no timeout in model) + +tcp-phi5-drop-BtoA: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: B sends SYN on BtoA, attacker drops it; but A can also initiate — if A goes Listen and B goes SynSent, A needs B's SYN which is dropped; however A can enter SynReceived via simultaneous open path and get stuck + +tcp-phi5-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping on both channels after SynReceived is entered prevents any ACK from arriving to resolve it + +tcp-phi5-replay-AtoB: + - 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: replay attacker consumes A's SYN+ACK and never replays it (terminates with empty mem), effectively a drop; A stuck in SynReceived + +tcp-phi5-reorder-AtoB: + - 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: reorder attacker consumes A's SYN+ACK during the handshake; even if replayed later, the ordering disruption can prevent SynReceived resolution + +# phi6: safety - strict closing transitions +# Closing implies next(Closing or Closed) +# Expected: violated even without attacker. Closing transitions to +# TimeWait on ACK (not Closed), and TimeWaitState is neither +# ClosingState nor ClosedState. + +tcp-phi6-drop-AtoB: + - 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: base model already violates phi6; simultaneous close leads to Closing, then ACK transitions to TimeWait which is not Closing or Closed; attacker goes to BREAK, preserving the pre-existing violation + +tcp-phi6-replay-AtoB: + - 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: same base-model violation; Closing -> TimeWait is always reachable once simultaneous close occurs + +tcp-phi6-reorder-bidirectional: + - 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: same base-model violation; attacker presence does not affect the Closing -> TimeWait transition path diff --git a/tests/tcp/no-network/tcp-phi1.pml b/tests/tcp/no-network/tcp-phi1.pml new file mode 100644 index 0000000..243cfd0 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi1.pml @@ -0,0 +1,149 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [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 new file mode 100644 index 0000000..960a173 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi2.pml @@ -0,0 +1,149 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [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 new file mode 100644 index 0000000..319ff39 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi2.pml.trail @@ -0,0 +1,55 @@ +-2:2:-2 +-4:-4:-4 +1:0:121 +2:1:114 +3:0:121 +4:1:115 +5:0:121 +6:1:116 +7:0:121 +8:1:117 +9:0:121 +10:3:0 +11:0:121 +12:3:1 +13:0:121 +14:3:2 +15:0:121 +16:3:9 +17:0:121 +18:2:0 +19:0:121 +20:2:1 +21:0:121 +22:2:2 +23:0:121 +24:2:9 +25:0:121 +26:3:17 +27:0:121 +28:3:1 +29:0:121 +30:3:3 +31:0:121 +32:3:22 +33:0:119 +34:2:17 +35:0:126 +36:2:1 +37:0:121 +38:2:3 +39:0:121 +40:2:22 +41:0:121 +42:2:42 +43:0:121 +44:2:1 +-1:-1:-1 +45:0:121 +46:2:2 +47:0:121 +48:2:9 +49:0:119 +50:2:17 +51:0:126 +52:2:1 diff --git a/tests/tcp/no-network/tcp-phi3.pml b/tests/tcp/no-network/tcp-phi3.pml new file mode 100644 index 0000000..35a9049 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi3.pml @@ -0,0 +1,167 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [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 new file mode 100644 index 0000000..68c2d48 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi4.pml @@ -0,0 +1,156 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [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 new file mode 100644 index 0000000..08508a0 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi4.pml.trail @@ -0,0 +1,43 @@ +-2:2:-2 +-4:-4:-4 +1:0:122 +2:1:114 +3:0:122 +4:1:115 +5:0:122 +6:1:116 +7:0:122 +8:1:117 +9:0:122 +10:3:0 +11:0:122 +12:3:1 +13:0:122 +14:3:2 +15:0:122 +16:3:9 +17:0:122 +18:2:0 +19:0:122 +20:2:1 +21:0:122 +22:2:2 +23:0:122 +24:2:9 +25:0:122 +26:3:17 +27:0:122 +28:3:1 +29:0:122 +30:3:3 +31:0:122 +32:3:22 +33:0:122 +34:2:17 +35:0:122 +36:2:1 +37:0:122 +38:2:3 +39:0:122 +40:2:22 +41:0:119 diff --git a/tests/tcp/no-network/tcp-phi5.pml b/tests/tcp/no-network/tcp-phi5.pml new file mode 100644 index 0000000..417ac59 --- /dev/null +++ b/tests/tcp/no-network/tcp-phi5.pml @@ -0,0 +1,158 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [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 new file mode 100644 index 0000000..2cf306a --- /dev/null +++ b/tests/tcp/no-network/tcp-phi6.pml @@ -0,0 +1,154 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [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 new file mode 100644 index 0000000..4e39675 --- /dev/null +++ b/tests/tcp/no-network/tcp.pml @@ -0,0 +1,144 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [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 index 7f43cf2..8d793e1 100755 Binary files a/tests/tcp/pan and b/tests/tcp/pan differ diff --git a/tests/tcp/tcp-phi1.pml b/tests/tcp/tcp-phi1.pml index 243cfd0..a95ba99 100644 --- a/tests/tcp/tcp-phi1.pml +++ b/tests/tcp/tcp-phi1.pml @@ -1,12 +1,7 @@ -// 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 }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* safety: half-open prevention */ diff --git a/tests/tcp/tcp-phi2.pml b/tests/tcp/tcp-phi2.pml index 960a173..620854f 100644 --- a/tests/tcp/tcp-phi2.pml +++ b/tests/tcp/tcp-phi2.pml @@ -1,12 +1,7 @@ -// 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 }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* liveness: verifying connection establishment */ diff --git a/tests/tcp/tcp-phi2.pml.trail b/tests/tcp/tcp-phi2.pml.trail index 319ff39..7c3fba0 100644 --- a/tests/tcp/tcp-phi2.pml.trail +++ b/tests/tcp/tcp-phi2.pml.trail @@ -1,55 +1,53 @@ --2:2:-2 +-2:3:-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:0:129 +2:2:122 +3:0:129 +4:2:123 +5:0:129 +6:2:124 +7:0:129 +8:2:125 +9:0:129 +10:4:0 +11:0:129 +12:4:1 +13:0:129 +14:4:2 +15:0:129 +16:4:9 +17:0:129 +18:3:0 +19:0:129 +20:3:1 +21:0:129 +22:3:2 +23:0:129 +24:3:9 +25:0:129 +26:4:17 +27:0:129 +28:4:1 +29:0:129 +30:4:3 +31:0:129 +32:4:22 +33:0:127 +34:1:116 -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 +35:0:134 +36:1:117 +37:0:127 +38:3:15 +39:0:134 +40:3:16 +41:0:127 +42:4:42 +43:0:134 +44:4:1 +45:0:129 +46:4:3 +47:0:129 +48:4:22 +49:0:127 +50:1:116 diff --git a/tests/tcp/tcp-phi3.pml b/tests/tcp/tcp-phi3.pml index 35a9049..45f6418 100644 --- a/tests/tcp/tcp-phi3.pml +++ b/tests/tcp/tcp-phi3.pml @@ -1,12 +1,7 @@ -// 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 }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* liveness: no infinite stalls/deadlocks */ diff --git a/tests/tcp/tcp-phi3.pml.trail b/tests/tcp/tcp-phi3.pml.trail new file mode 100644 index 0000000..bb2a009 --- /dev/null +++ b/tests/tcp/tcp-phi3.pml.trail @@ -0,0 +1,62 @@ +-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/tcp-phi4.pml b/tests/tcp/tcp-phi4.pml index 68c2d48..b34fa36 100644 --- a/tests/tcp/tcp-phi4.pml +++ b/tests/tcp/tcp-phi4.pml @@ -1,12 +1,7 @@ -// 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 }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* liveness: simultanous open */ diff --git a/tests/tcp/tcp-phi4.pml.trail b/tests/tcp/tcp-phi4.pml.trail index 08508a0..88bdbca 100644 --- a/tests/tcp/tcp-phi4.pml.trail +++ b/tests/tcp/tcp-phi4.pml.trail @@ -1,43 +1,322 @@ --2:2:-2 +-2:3:-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 +1:0:130 +2:2:122 +3:0:130 +4:2:123 +5:0:130 +6:2:124 +7:0:130 +8:2:125 +9:0:130 +10:4:0 +11:0:130 +12:4:1 +13:0:130 +14:4:2 +15:0:130 +16:4:9 +17:0:130 +18:3:0 +19:0:130 +20:3:1 +21:0:130 +22:3:2 +23:0:130 +24:3:9 +25:0:130 +26:4:17 +27:0:130 +28:4:1 +29:0:130 +30:4:3 +31:0:130 +32:4:22 +33:0:130 +34:1:116 +35:0:130 +36:1:117 +37:0:130 +38:3:10 +39:0:130 +40:3:11 +41:3:12 +42:0:130 +43:3:47 +44:0:130 +45:1:114 +46:0:130 +47:1:115 +48:0:130 +49:4:23 +50:0:130 +51:4:27 +52:0:130 +53:4:47 +54:0:130 +55:1:114 +56:0:130 +57:1:115 +58:0:130 +59:4:48 +60:0:130 +61:4:55 +62:0:130 +63:4:56 +64:0:130 +65:4:66 +66:0:130 +67:1:116 +68:0:130 +69:1:117 +70:0:130 +71:3:48 +72:0:130 +73:3:55 +74:0:130 +75:3:56 +76:0:130 +77:3:66 +78:0:130 +79:1:114 +80:0:130 +81:1:115 +82:0:130 +83:4:67 +84:0:130 +85:4:68 +86:0:130 +87:4:94 +88:0:130 +89:1:116 +90:0:130 +91:1:117 +92:0:130 +93:3:67 +94:0:130 +95:3:68 +96:0:130 +97:3:94 +98:0:130 +99:1:114 +100:0:130 +101:1:115 +102:0:130 +103:4:95 +104:0:130 +105:4:110 +106:0:130 +107:4:1 +108:0:130 +109:4:2 +110:0:130 +111:4:9 +112:0:130 +113:1:116 +114:0:130 +115:1:117 +116:0:130 +117:3:95 +118:0:130 +119:3:110 +120:0:130 +121:3:1 +122:0:130 +123:3:2 +124:0:130 +125:3:9 +126:0:130 +127:4:17 +128:0:130 +129:4:1 +130:0:130 +131:4:3 +132:0:130 +133:1:116 +134:0:130 +135:1:117 +136:0:130 +137:3:10 +138:0:130 +139:3:11 +140:3:12 +141:0:130 +142:3:47 +143:0:130 +144:1:114 +145:0:130 +146:1:115 +147:0:130 +148:1:114 +149:0:130 +150:4:22 +151:0:130 +152:4:23 +153:0:130 +154:4:27 +155:0:130 +156:1:115 +157:0:130 +158:1:116 +159:0:130 +160:4:47 +161:0:130 +162:4:48 +163:0:130 +164:4:55 +165:0:130 +166:4:56 +167:0:130 +168:1:117 +169:0:130 +170:3:48 +171:0:130 +172:3:55 +173:0:130 +174:3:56 +175:0:130 +176:3:66 +177:0:130 +178:1:114 +179:0:130 +180:1:115 +181:0:130 +182:1:116 +183:0:130 +184:4:66 +185:0:130 +186:4:67 +187:0:130 +188:4:68 +189:0:130 +190:1:117 +191:0:130 +192:3:67 +193:0:130 +194:3:68 +195:0:130 +196:3:94 +197:0:130 +198:1:114 +199:0:130 +200:1:115 +201:0:130 +202:1:116 +203:0:130 +204:4:94 +205:0:130 +206:4:95 +207:0:130 +208:4:110 +209:0:130 +210:4:1 +211:0:130 +212:4:2 +213:0:130 +214:1:117 +215:0:130 +216:3:95 +217:0:130 +218:3:110 +219:0:130 +220:3:1 +221:0:130 +222:3:3 +223:0:130 +224:4:9 +225:0:130 +226:3:22 +227:0:130 +228:1:114 +229:0:130 +230:1:115 +231:0:130 +232:4:10 +233:0:130 +234:4:11 +235:4:12 +236:0:130 +237:4:47 +238:0:130 +239:1:116 +240:0:130 +241:1:117 +242:0:130 +243:3:23 +244:0:130 +245:3:27 +246:0:130 +247:1:114 +248:0:130 +249:1:115 +250:0:130 +251:4:48 +252:0:130 +253:4:55 +254:0:130 +255:4:56 +256:0:130 +257:4:66 +258:0:130 +259:1:116 +260:0:130 +261:1:117 +262:0:130 +263:1:116 +264:0:130 +265:3:47 +266:0:130 +267:3:48 +268:0:130 +269:3:55 +270:0:130 +271:3:56 +272:0:130 +273:3:66 +274:0:130 +275:1:117 +276:0:130 +277:3:67 +278:0:130 +279:3:68 +280:0:130 +281:1:114 +282:0:130 +283:1:115 +284:0:130 +285:4:67 +286:0:130 +287:1:114 +288:0:130 +289:4:68 +290:0:130 +291:4:94 +292:0:130 +293:1:115 +294:0:130 +295:4:95 +296:0:130 +297:4:110 +298:0:130 +299:4:1 +300:0:130 +301:4:3 +302:0:130 +303:4:22 +304:0:130 +305:3:94 +306:0:130 +307:1:116 +308:0:130 +309:1:117 +310:0:130 +311:3:95 +312:0:130 +313:3:110 +314:0:130 +315:3:1 +316:0:130 +317:3:3 +318:0:130 +319:3:22 +320:0:127 diff --git a/tests/tcp/tcp-phi5.pml b/tests/tcp/tcp-phi5.pml index 417ac59..3b65921 100644 --- a/tests/tcp/tcp-phi5.pml +++ b/tests/tcp/tcp-phi5.pml @@ -1,12 +1,7 @@ -// 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 }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* liveness: SYN_RECEIVED resolution*/ diff --git a/tests/tcp/tcp-phi5.pml.trail b/tests/tcp/tcp-phi5.pml.trail new file mode 100644 index 0000000..3ac1dc9 --- /dev/null +++ b/tests/tcp/tcp-phi5.pml.trail @@ -0,0 +1,86 @@ +-2:3:-2 +-4:-4:-4 +1:0:129 +2:2:122 +3:0:129 +4:2:123 +5:0:129 +6:2:124 +7:0:129 +8:2:125 +9:0:129 +10:4:0 +11:0:129 +12:4:1 +13:0:129 +14:4:2 +15:0:129 +16:4:9 +17:0:129 +18:3:0 +19:0:129 +20:3:1 +21:0:129 +22:3:2 +23:0:129 +24:3:9 +25:0:129 +26:4:17 +27:0:129 +28:4:1 +29:0:129 +30:4:3 +31:0:129 +32:4:22 +33:0:129 +34:1:116 +35:0:129 +36:1:117 +37:0:129 +38:3:10 +39:0:129 +40:3:11 +41:3:12 +42:0:129 +43:3:47 +44:0:127 +45:1:114 +46:0:134 +47:1:115 +48:0:134 +49:4:23 +50:0:134 +51:4:27 +52:0:134 +53:4:47 +54:0:134 +55:1:114 +56:0:134 +57:1:115 +58:0:134 +59:4:48 +60:0:134 +61:4:55 +62:0:134 +63:4:56 +64:0:134 +65:4:66 +66:0:134 +67:1:116 +68:0:134 +69:1:117 +70:0:134 +71:3:50 +72:0:134 +73:3:51 +74:0:134 +75:1:116 +76:0:134 +77:1:117 +78:0:134 +79:3:50 +80:0:134 +81:3:51 +-1:-1:-1 +82:0:134 +83:0:134 diff --git a/tests/tcp/tcp-phi6.pml b/tests/tcp/tcp-phi6.pml index 2cf306a..d0cf9a0 100644 --- a/tests/tcp/tcp-phi6.pml +++ b/tests/tcp/tcp-phi6.pml @@ -1,12 +1,7 @@ -// 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 }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,8 +133,8 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); } /* safety: strict closing transitions */ diff --git a/tests/tcp/tcp-phi6.pml.trail b/tests/tcp/tcp-phi6.pml.trail new file mode 100644 index 0000000..8bc7191 --- /dev/null +++ b/tests/tcp/tcp-phi6.pml.trail @@ -0,0 +1,122 @@ +-2:3:-2 +-4:-4:-4 +1:0:129 +2:2:122 +3:0:129 +4:2:123 +5:0:129 +6:2:124 +7:0:129 +8:2:125 +9:0:129 +10:4:0 +11:0:129 +12:4:1 +13:0:129 +14:4:2 +15:0:129 +16:4:9 +17:0:129 +18:3:0 +19:0:129 +20:3:1 +21:0:129 +22:3:2 +23:0:129 +24:3:9 +25:0:129 +26:4:17 +27:0:129 +28:4:1 +29:0:129 +30:4:3 +31:0:129 +32:4:22 +33:0:129 +34:1:116 +35:0:129 +36:1:117 +37:0:129 +38:3:10 +39:0:129 +40:3:11 +41:3:12 +42:0:129 +43:3:47 +44:0:129 +45:1:114 +46:0:129 +47:1:115 +48:0:129 +49:4:23 +50:0:129 +51:4:27 +52:0:129 +53:4:47 +54:0:129 +55:1:114 +56:0:129 +57:1:115 +58:0:129 +59:4:48 +60:0:129 +61:4:55 +62:0:129 +63:4:56 +64:0:129 +65:4:66 +66:0:129 +67:1:116 +68:0:129 +69:1:117 +70:0:129 +71:3:48 +72:0:129 +73:3:55 +74:0:129 +75:3:56 +76:0:129 +77:3:66 +78:0:129 +79:1:114 +80:0:129 +81:1:115 +82:0:129 +83:4:67 +84:0:129 +85:4:68 +86:0:129 +87:4:94 +88:0:129 +89:1:116 +90:0:129 +91:1:117 +92:0:129 +93:3:67 +94:0:129 +95:3:68 +96:0:129 +97:3:94 +98:0:129 +99:1:114 +100:0:129 +101:1:115 +102:0:129 +103:4:95 +104:0:129 +105:4:110 +106:0:129 +107:4:1 +108:0:129 +109:4:2 +110:0:129 +111:4:9 +112:0:129 +113:1:116 +114:0:129 +115:1:117 +116:0:129 +117:3:95 +118:0:127 +119:3:110 +120:0:134 diff --git a/tests/tcp/tcp.pml b/tests/tcp/tcp.pml index 4e39675..1792fbe 100644 --- a/tests/tcp/tcp.pml +++ b/tests/tcp/tcp.pml @@ -1,12 +1,7 @@ -// 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 }; +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; int state[2]; int pids[2]; @@ -80,7 +75,6 @@ SYN_RECEIVED: :: rcv ? ACK -> goto ESTABLISHED; :: rcv ? _ -> skip; od - /* We may want to consider putting a timeout -> CLOSED here. */ ESTABLISHED: state[i] = EstState; do @@ -139,6 +133,6 @@ end: init { state[0] = ClosedState; state[1] = ClosedState; - run TCP(AtoN, NtoA, 0); - run TCP(BtoN, NtoB, 1); + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); }