diff --git a/tests/paper-attempt1.yaml b/tests/paper-attempt1.yaml new file mode 100644 index 0000000..3bc8ec1 --- /dev/null +++ b/tests/paper-attempt1.yaml @@ -0,0 +1,216 @@ +# --- 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/paper2.yaml b/tests/paper2.yaml deleted file mode 100644 index 4c46c60..0000000 --- a/tests/paper2.yaml +++ /dev/null @@ -1,127 +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 tests -# -# NOTE: The TCP model uses separate send/receive channel pairs -# (AtoN[1], NtoA[0], BtoN[1], NtoB[0]) with no network forwarding process. -# A sends on AtoN but B receives on NtoB; Korg's single-channel attacker -# gadgets cannot bridge this gap. As a result, all single-channel attacks -# are ineffective: consumed/replayed/reordered messages on AtoN never -# reach B (and vice versa). Both TCP processes fall back to Closed via -# timeout transitions, so all properties hold trivially or vacuously. -# -# This demonstrates a structural limitation: Korg's channel-local attackers -# require that communicating processes share the attacked channel. A network -# forwarding process (AtoN -> NtoB, BtoN -> NtoA) would be needed for -# meaningful cross-channel attacks. -# ============================================================================= - -# phi1: safety - half-open prevention -# always (leftClosed implies !rightEstablished) - -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: attacker consumes from AtoN but B reads NtoB; no messages are delivered cross-channel so neither side reaches Established, and phi1 holds trivially - -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 outbound channels still cannot affect the inbound rendezvous channels NtoA/NtoB; no handshake progress occurs - -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: no violation - - explanation: replayed messages land back on AtoN, which only A writes to; B never reads AtoN so no half-open state can be manufactured - -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: no violation - - explanation: replaying on both outbound channels cannot bridge to the rendezvous inbound channels; property holds vacuously - -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: no violation - - explanation: reordering on AtoN is invisible to B; the channel architecture prevents any cross-channel effect - -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: no violation - - explanation: reordering both outbound channels still cannot deliver messages to the inbound rendezvous channels - -# phi3: liveness - no infinite stalls/deadlocks - -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: no violation - - explanation: timeout transitions in LISTEN and SYN_SENT return both processes to Closed; no permanent stall occurs because no cross-channel delivery happens - -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: no violation - - explanation: same as above; both sides cycle through Closed via timeout, preventing any permanent intermediate state - -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: no violation - - explanation: replayed messages on AtoN do not reach B; both sides timeout-cycle through Closed, so no stall - -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: no violation - - explanation: reordering cannot create stalls when messages never cross between the two TCP processes - -# phi5: liveness - SYN_RECEIVED resolution -# SynReceived implies eventually (Established or FinWait1 or Closed) - -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: no violation - - explanation: neither process enters SynReceived because no SYN is ever delivered cross-channel; the property holds vacuously - -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: no violation - - explanation: same as above; without cross-channel delivery, SynReceived is never entered - -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 on AtoN cannot deliver a SYN to B via NtoB; SynReceived is never reached, so the property holds vacuously - -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: no violation - - explanation: reordering on AtoN has no cross-channel effect; property holds vacuously as SynReceived is unreachable - -# phi6: safety - strict closing transitions -# Closing implies next(Closing or Closed) - -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: Closing state is never reached without cross-channel message delivery; property holds vacuously - -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: no violation - - explanation: replay on AtoN cannot drive either process into Closing; property holds vacuously - -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: no violation - - explanation: replaying on both outbound channels still cannot bridge to inbound rendezvous channels; Closing never entered - -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: no violation - - explanation: reordering both outbound channels has no effect on the rendezvous inbound channels; Closing never entered diff --git a/tests/paper3.yaml b/tests/paper3.yaml deleted file mode 100644 index 41089d6..0000000 --- a/tests/paper3.yaml +++ /dev/null @@ -1,133 +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 - 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: property violation - - explanation: replay attacker copies A's message non-destructively, allowing normal handshake and teardown; after A returns to Closed, the replayed stale message drives B through a new handshake into Established, creating a half-open state - -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: property violation - - explanation: replay on both channels injects stale handshake messages in both directions; after A tears down to Closed, replayed messages push B into Established without A's participation - -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-nodeadlock: - - 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: with mem=0 the drop attacker cannot consume any messages; it goes straight to BREAK, leaving the model unmodified; timeout transitions prevent permanent stalls in the base model - -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-replay-BtoA: - - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=replay --chan=BtoA --output=temp.pml --eval --cleanup --mem=1 - - intended: no violation - - explanation: replaying B's messages on BtoA delivers extra SYNs to A; if A enters SynReceived, the replayed messages do not prevent ACK delivery on AtoB (which is unattacked), so SynReceived resolves normally - -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/attempt1/tcp-phi1.pml b/tests/tcp/attempt1/tcp-phi1.pml new file mode 100644 index 0000000..a95ba99 --- /dev/null +++ b/tests/tcp/attempt1/tcp-phi1.pml @@ -0,0 +1,143 @@ +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 new file mode 100644 index 0000000..620854f --- /dev/null +++ b/tests/tcp/attempt1/tcp-phi2.pml @@ -0,0 +1,143 @@ +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/tcp-phi2.pml.trail b/tests/tcp/attempt1/tcp-phi2.pml.trail similarity index 100% rename from tests/tcp/tcp-phi2.pml.trail rename to tests/tcp/attempt1/tcp-phi2.pml.trail diff --git a/tests/tcp/attempt1/tcp-phi3.pml b/tests/tcp/attempt1/tcp-phi3.pml new file mode 100644 index 0000000..45f6418 --- /dev/null +++ b/tests/tcp/attempt1/tcp-phi3.pml @@ -0,0 +1,161 @@ +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/tcp-phi3.pml.trail b/tests/tcp/attempt1/tcp-phi3.pml.trail similarity index 100% rename from tests/tcp/tcp-phi3.pml.trail rename to tests/tcp/attempt1/tcp-phi3.pml.trail diff --git a/tests/tcp/attempt1/tcp-phi4.pml b/tests/tcp/attempt1/tcp-phi4.pml new file mode 100644 index 0000000..b34fa36 --- /dev/null +++ b/tests/tcp/attempt1/tcp-phi4.pml @@ -0,0 +1,150 @@ +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 new file mode 100644 index 0000000..cf64d44 --- /dev/null +++ b/tests/tcp/attempt1/tcp-phi4.pml.trail @@ -0,0 +1,157 @@ +-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 new file mode 100644 index 0000000..3b65921 --- /dev/null +++ b/tests/tcp/attempt1/tcp-phi5.pml @@ -0,0 +1,152 @@ +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/tcp-phi5.pml.trail b/tests/tcp/attempt1/tcp-phi5.pml.trail similarity index 100% rename from tests/tcp/tcp-phi5.pml.trail rename to tests/tcp/attempt1/tcp-phi5.pml.trail diff --git a/tests/tcp/attempt1/tcp-phi6.pml b/tests/tcp/attempt1/tcp-phi6.pml new file mode 100644 index 0000000..d0cf9a0 --- /dev/null +++ b/tests/tcp/attempt1/tcp-phi6.pml @@ -0,0 +1,148 @@ +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 new file mode 100644 index 0000000..1840bcf --- /dev/null +++ b/tests/tcp/attempt1/tcp-phi6.pml.trail @@ -0,0 +1,88 @@ +-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 new file mode 100644 index 0000000..1792fbe --- /dev/null +++ b/tests/tcp/attempt1/tcp.pml @@ -0,0 +1,138 @@ +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/pan b/tests/tcp/pan index b304ec1..79a5e06 100755 Binary files a/tests/tcp/pan and b/tests/tcp/pan differ diff --git a/tests/tcp/props/phi7.pml b/tests/tcp/props/phi7.pml new file mode 100644 index 0000000..c179125 --- /dev/null +++ b/tests/tcp/props/phi7.pml @@ -0,0 +1,9 @@ +/* liveness: simultaneous close resolution */ +ltl phi7 { + always ( + (state[0] == FinW1State && state[1] == FinW1State) + implies + (eventually (state[0] == ClosedState) && + eventually (state[1] == ClosedState)) + ) +} diff --git a/tests/tcp/props/phi8.pml b/tests/tcp/props/phi8.pml new file mode 100644 index 0000000..361d567 --- /dev/null +++ b/tests/tcp/props/phi8.pml @@ -0,0 +1,6 @@ +/* liveness: active close eventually terminates */ +ltl phi8 { + always ( + (state[0] == FinW1State) implies (eventually (state[0] == ClosedState)) + ) +} diff --git a/tests/tcp/props/phi9.pml b/tests/tcp/props/phi9.pml new file mode 100644 index 0000000..06bcd20 --- /dev/null +++ b/tests/tcp/props/phi9.pml @@ -0,0 +1,8 @@ +/* safety: handshake cannot be bypassed */ +ltl phi9 { + always ( + (state[0] == ListenState) + implies + !(next (state[0] == EstState)) + ) +} diff --git a/tests/tcp/tcp-phi1.pml b/tests/tcp/tcp-phi1.pml index a95ba99..5e8fc4f 100644 --- a/tests/tcp/tcp-phi1.pml +++ b/tests/tcp/tcp-phi1.pml @@ -1,10 +1,9 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } +mtype = { SYN, FIN, ACK } chan AtoB = [2] of { mtype }; chan BtoA = [2] of { mtype }; int state[2]; -int pids[2]; #define ClosedState 0 #define ListenState 1 @@ -17,127 +16,128 @@ int pids[2]; #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; + mtype msg; CLOSED: - state[i] = ClosedState; - do - /* Passive open */ - :: goto LISTEN; - /* Active open */ - :: snd ! SYN; goto SYN_SENT; - /* Terminate */ - :: goto end; - od + state[i] = ClosedState; + if + :: goto LISTEN; + :: snd ! SYN; goto SYN_SENT; + fi; + 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; + state[i] = ListenState; do - :: rcv ? SYN -> - snd ! ACK; - goto ESTABLISHED; - :: rcv ? _ -> skip; - od - :: rcv ? _ -> skip; - :: timeout -> goto CLOSED; /* Timeout */ - od + :: rcv ? msg -> + if + :: msg == SYN -> snd ! SYN; snd ! ACK; goto SYN_RECEIVED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto SYN_RECEIVED; + :: msg == ACK -> + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + SYN_RECEIVED: - state[i] = SynRecState; - do - :: rcv ? ACK -> goto ESTABLISHED; - :: rcv ? _ -> skip; - od + state[i] = SynRecState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + 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 + state[i] = EstState; + do + :: snd ! FIN; goto FIN_WAIT_1; + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSE_WAIT; + :: else -> skip; + fi + 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 + state[i] = FinW1State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSING; + :: msg == ACK -> goto FIN_WAIT_2; + :: else -> skip; + fi + od; + FIN_WAIT_2: - state[i] = FinW2State; - do - :: rcv ? FIN -> - snd ! ACK; - goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = FinW2State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto TIME_WAIT; + :: else -> skip; + fi + od; + CLOSING: - state[i] = ClosingState; - do - :: rcv ? ACK -> goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = ClosingState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; + LAST_ACK: - state[i] = LastAckState; - do - :: rcv ? ACK -> goto CLOSED; - :: rcv ? _ -> skip; - od + state[i] = LastAckState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto CLOSED; + :: else -> skip; + fi + od; + TIME_WAIT: - state[i] = TimeWaitState; - goto CLOSED; -end: - state[i] = EndState; + state[i] = TimeWaitState; + goto CLOSED; } init { - state[0] = ClosedState; - state[1] = ClosedState; - run TCP(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 1); + state[0] = ClosedState; + state[1] = ClosedState; + atomic { + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); + } } -/* safety: half-open prevention */ ltl phi1 { - always ( leftClosed implies !rightEstablished ) + always ( (state[0] == ClosedState) implies !(state[1] == EstState) ) } diff --git a/tests/tcp/tcp-phi2.pml b/tests/tcp/tcp-phi2.pml index 620854f..6392dd0 100644 --- a/tests/tcp/tcp-phi2.pml +++ b/tests/tcp/tcp-phi2.pml @@ -1,10 +1,9 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } +mtype = { SYN, FIN, ACK } chan AtoB = [2] of { mtype }; chan BtoA = [2] of { mtype }; int state[2]; -int pids[2]; #define ClosedState 0 #define ListenState 1 @@ -17,127 +16,130 @@ int pids[2]; #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; + mtype msg; CLOSED: - state[i] = ClosedState; - do - /* Passive open */ - :: goto LISTEN; - /* Active open */ - :: snd ! SYN; goto SYN_SENT; - /* Terminate */ - :: goto end; - od + state[i] = ClosedState; + if + :: goto LISTEN; + :: snd ! SYN; goto SYN_SENT; + fi; + 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; + state[i] = ListenState; do - :: rcv ? SYN -> - snd ! ACK; - goto ESTABLISHED; - :: rcv ? _ -> skip; - od - :: rcv ? _ -> skip; - :: timeout -> goto CLOSED; /* Timeout */ - od + :: rcv ? msg -> + if + :: msg == SYN -> snd ! SYN; snd ! ACK; goto SYN_RECEIVED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto SYN_RECEIVED; + :: msg == ACK -> + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + SYN_RECEIVED: - state[i] = SynRecState; - do - :: rcv ? ACK -> goto ESTABLISHED; - :: rcv ? _ -> skip; - od + state[i] = SynRecState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + 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 + state[i] = EstState; + do + :: snd ! FIN; goto FIN_WAIT_1; + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSE_WAIT; + :: else -> skip; + fi + 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 + state[i] = FinW1State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSING; + :: msg == ACK -> goto FIN_WAIT_2; + :: else -> skip; + fi + od; + FIN_WAIT_2: - state[i] = FinW2State; - do - :: rcv ? FIN -> - snd ! ACK; - goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = FinW2State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto TIME_WAIT; + :: else -> skip; + fi + od; + CLOSING: - state[i] = ClosingState; - do - :: rcv ? ACK -> goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = ClosingState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; + LAST_ACK: - state[i] = LastAckState; - do - :: rcv ? ACK -> goto CLOSED; - :: rcv ? _ -> skip; - od + state[i] = LastAckState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto CLOSED; + :: else -> skip; + fi + od; + TIME_WAIT: - state[i] = TimeWaitState; - goto CLOSED; -end: - state[i] = EndState; + state[i] = TimeWaitState; + goto CLOSED; } init { - state[0] = ClosedState; - state[1] = ClosedState; - run TCP(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 1); + state[0] = ClosedState; + state[1] = ClosedState; + atomic { + 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/tcp-phi3.pml b/tests/tcp/tcp-phi3.pml index 45f6418..3e11967 100644 --- a/tests/tcp/tcp-phi3.pml +++ b/tests/tcp/tcp-phi3.pml @@ -1,10 +1,9 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } +mtype = { SYN, FIN, ACK } chan AtoB = [2] of { mtype }; chan BtoA = [2] of { mtype }; int state[2]; -int pids[2]; #define ClosedState 0 #define ListenState 1 @@ -17,124 +16,126 @@ int pids[2]; #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; + mtype msg; CLOSED: - state[i] = ClosedState; - do - /* Passive open */ - :: goto LISTEN; - /* Active open */ - :: snd ! SYN; goto SYN_SENT; - /* Terminate */ - :: goto end; - od + state[i] = ClosedState; + if + :: goto LISTEN; + :: snd ! SYN; goto SYN_SENT; + fi; + 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; + state[i] = ListenState; do - :: rcv ? SYN -> - snd ! ACK; - goto ESTABLISHED; - :: rcv ? _ -> skip; - od - :: rcv ? _ -> skip; - :: timeout -> goto CLOSED; /* Timeout */ - od + :: rcv ? msg -> + if + :: msg == SYN -> snd ! SYN; snd ! ACK; goto SYN_RECEIVED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto SYN_RECEIVED; + :: msg == ACK -> + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + SYN_RECEIVED: - state[i] = SynRecState; - do - :: rcv ? ACK -> goto ESTABLISHED; - :: rcv ? _ -> skip; - od + state[i] = SynRecState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + 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 + state[i] = EstState; + do + :: snd ! FIN; goto FIN_WAIT_1; + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSE_WAIT; + :: else -> skip; + fi + 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 + state[i] = FinW1State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSING; + :: msg == ACK -> goto FIN_WAIT_2; + :: else -> skip; + fi + od; + FIN_WAIT_2: - state[i] = FinW2State; - do - :: rcv ? FIN -> - snd ! ACK; - goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = FinW2State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto TIME_WAIT; + :: else -> skip; + fi + od; + CLOSING: - state[i] = ClosingState; - do - :: rcv ? ACK -> goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = ClosingState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; + LAST_ACK: - state[i] = LastAckState; - do - :: rcv ? ACK -> goto CLOSED; - :: rcv ? _ -> skip; - od + state[i] = LastAckState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto CLOSED; + :: else -> skip; + fi + od; + TIME_WAIT: - state[i] = TimeWaitState; - goto CLOSED; -end: - state[i] = EndState; + state[i] = TimeWaitState; + goto CLOSED; } init { - state[0] = ClosedState; - state[1] = ClosedState; - run TCP(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 1); + state[0] = ClosedState; + state[1] = ClosedState; + atomic { + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); + } } /* liveness: no infinite stalls/deadlocks */ diff --git a/tests/tcp/tcp-phi4.pml b/tests/tcp/tcp-phi4.pml index b34fa36..038c1b4 100644 --- a/tests/tcp/tcp-phi4.pml +++ b/tests/tcp/tcp-phi4.pml @@ -1,10 +1,9 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } +mtype = { SYN, FIN, ACK } chan AtoB = [2] of { mtype }; chan BtoA = [2] of { mtype }; int state[2]; -int pids[2]; #define ClosedState 0 #define ListenState 1 @@ -17,124 +16,126 @@ int pids[2]; #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; + mtype msg; CLOSED: - state[i] = ClosedState; - do - /* Passive open */ - :: goto LISTEN; - /* Active open */ - :: snd ! SYN; goto SYN_SENT; - /* Terminate */ - :: goto end; - od + state[i] = ClosedState; + if + :: goto LISTEN; + :: snd ! SYN; goto SYN_SENT; + fi; + 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; + state[i] = ListenState; do - :: rcv ? SYN -> - snd ! ACK; - goto ESTABLISHED; - :: rcv ? _ -> skip; - od - :: rcv ? _ -> skip; - :: timeout -> goto CLOSED; /* Timeout */ - od + :: rcv ? msg -> + if + :: msg == SYN -> snd ! SYN; snd ! ACK; goto SYN_RECEIVED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto SYN_RECEIVED; + :: msg == ACK -> + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + SYN_RECEIVED: - state[i] = SynRecState; - do - :: rcv ? ACK -> goto ESTABLISHED; - :: rcv ? _ -> skip; - od + state[i] = SynRecState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + 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 + state[i] = EstState; + do + :: snd ! FIN; goto FIN_WAIT_1; + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSE_WAIT; + :: else -> skip; + fi + 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 + state[i] = FinW1State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSING; + :: msg == ACK -> goto FIN_WAIT_2; + :: else -> skip; + fi + od; + FIN_WAIT_2: - state[i] = FinW2State; - do - :: rcv ? FIN -> - snd ! ACK; - goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = FinW2State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto TIME_WAIT; + :: else -> skip; + fi + od; + CLOSING: - state[i] = ClosingState; - do - :: rcv ? ACK -> goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = ClosingState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; + LAST_ACK: - state[i] = LastAckState; - do - :: rcv ? ACK -> goto CLOSED; - :: rcv ? _ -> skip; - od + state[i] = LastAckState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto CLOSED; + :: else -> skip; + fi + od; + TIME_WAIT: - state[i] = TimeWaitState; - goto CLOSED; -end: - state[i] = EndState; + state[i] = TimeWaitState; + goto CLOSED; } init { - state[0] = ClosedState; - state[1] = ClosedState; - run TCP(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 1); + state[0] = ClosedState; + state[1] = ClosedState; + atomic { + 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 cf64d44..7ac32a2 100644 --- a/tests/tcp/tcp-phi4.pml.trail +++ b/tests/tcp/tcp-phi4.pml.trail @@ -1,157 +1,192 @@ -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 +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-phi5.pml b/tests/tcp/tcp-phi5.pml index 3b65921..a2b6f11 100644 --- a/tests/tcp/tcp-phi5.pml +++ b/tests/tcp/tcp-phi5.pml @@ -1,10 +1,9 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } +mtype = { SYN, FIN, ACK } chan AtoB = [2] of { mtype }; chan BtoA = [2] of { mtype }; int state[2]; -int pids[2]; #define ClosedState 0 #define ListenState 1 @@ -17,124 +16,126 @@ int pids[2]; #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; + mtype msg; CLOSED: - state[i] = ClosedState; - do - /* Passive open */ - :: goto LISTEN; - /* Active open */ - :: snd ! SYN; goto SYN_SENT; - /* Terminate */ - :: goto end; - od + state[i] = ClosedState; + if + :: goto LISTEN; + :: snd ! SYN; goto SYN_SENT; + fi; + 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; + state[i] = ListenState; do - :: rcv ? SYN -> - snd ! ACK; - goto ESTABLISHED; - :: rcv ? _ -> skip; - od - :: rcv ? _ -> skip; - :: timeout -> goto CLOSED; /* Timeout */ - od + :: rcv ? msg -> + if + :: msg == SYN -> snd ! SYN; snd ! ACK; goto SYN_RECEIVED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto SYN_RECEIVED; + :: msg == ACK -> + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + SYN_RECEIVED: - state[i] = SynRecState; - do - :: rcv ? ACK -> goto ESTABLISHED; - :: rcv ? _ -> skip; - od + state[i] = SynRecState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + 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 + state[i] = EstState; + do + :: snd ! FIN; goto FIN_WAIT_1; + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSE_WAIT; + :: else -> skip; + fi + 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 + state[i] = FinW1State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSING; + :: msg == ACK -> goto FIN_WAIT_2; + :: else -> skip; + fi + od; + FIN_WAIT_2: - state[i] = FinW2State; - do - :: rcv ? FIN -> - snd ! ACK; - goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = FinW2State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto TIME_WAIT; + :: else -> skip; + fi + od; + CLOSING: - state[i] = ClosingState; - do - :: rcv ? ACK -> goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = ClosingState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; + LAST_ACK: - state[i] = LastAckState; - do - :: rcv ? ACK -> goto CLOSED; - :: rcv ? _ -> skip; - od + state[i] = LastAckState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto CLOSED; + :: else -> skip; + fi + od; + TIME_WAIT: - state[i] = TimeWaitState; - goto CLOSED; -end: - state[i] = EndState; + state[i] = TimeWaitState; + goto CLOSED; } init { - state[0] = ClosedState; - state[1] = ClosedState; - run TCP(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 1); + state[0] = ClosedState; + state[1] = ClosedState; + atomic { + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); + } } /* liveness: SYN_RECEIVED resolution*/ diff --git a/tests/tcp/tcp-phi6.pml b/tests/tcp/tcp-phi6.pml index d0cf9a0..c2771fe 100644 --- a/tests/tcp/tcp-phi6.pml +++ b/tests/tcp/tcp-phi6.pml @@ -1,10 +1,9 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } +mtype = { SYN, FIN, ACK } chan AtoB = [2] of { mtype }; chan BtoA = [2] of { mtype }; int state[2]; -int pids[2]; #define ClosedState 0 #define ListenState 1 @@ -17,124 +16,126 @@ int pids[2]; #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; + mtype msg; CLOSED: - state[i] = ClosedState; - do - /* Passive open */ - :: goto LISTEN; - /* Active open */ - :: snd ! SYN; goto SYN_SENT; - /* Terminate */ - :: goto end; - od + state[i] = ClosedState; + if + :: goto LISTEN; + :: snd ! SYN; goto SYN_SENT; + fi; + 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; + state[i] = ListenState; do - :: rcv ? SYN -> - snd ! ACK; - goto ESTABLISHED; - :: rcv ? _ -> skip; - od - :: rcv ? _ -> skip; - :: timeout -> goto CLOSED; /* Timeout */ - od + :: rcv ? msg -> + if + :: msg == SYN -> snd ! SYN; snd ! ACK; goto SYN_RECEIVED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto SYN_RECEIVED; + :: msg == ACK -> + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + SYN_RECEIVED: - state[i] = SynRecState; - do - :: rcv ? ACK -> goto ESTABLISHED; - :: rcv ? _ -> skip; - od + state[i] = SynRecState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + 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 + state[i] = EstState; + do + :: snd ! FIN; goto FIN_WAIT_1; + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSE_WAIT; + :: else -> skip; + fi + 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 + state[i] = FinW1State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSING; + :: msg == ACK -> goto FIN_WAIT_2; + :: else -> skip; + fi + od; + FIN_WAIT_2: - state[i] = FinW2State; - do - :: rcv ? FIN -> - snd ! ACK; - goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = FinW2State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto TIME_WAIT; + :: else -> skip; + fi + od; + CLOSING: - state[i] = ClosingState; - do - :: rcv ? ACK -> goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = ClosingState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; + LAST_ACK: - state[i] = LastAckState; - do - :: rcv ? ACK -> goto CLOSED; - :: rcv ? _ -> skip; - od + state[i] = LastAckState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto CLOSED; + :: else -> skip; + fi + od; + TIME_WAIT: - state[i] = TimeWaitState; - goto CLOSED; -end: - state[i] = EndState; + state[i] = TimeWaitState; + goto CLOSED; } init { - state[0] = ClosedState; - state[1] = ClosedState; - run TCP(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 1); + state[0] = ClosedState; + state[1] = ClosedState; + atomic { + 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 index 1840bcf..63146ef 100644 --- a/tests/tcp/tcp-phi6.pml.trail +++ b/tests/tcp/tcp-phi6.pml.trail @@ -1,88 +1,102 @@ -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 +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 diff --git a/tests/tcp/tcp-phi7.pml b/tests/tcp/tcp-phi7.pml new file mode 100644 index 0000000..0c0e18d --- /dev/null +++ b/tests/tcp/tcp-phi7.pml @@ -0,0 +1,149 @@ +mtype = { SYN, FIN, ACK } + +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; + +int state[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 + +proctype TCP(chan snd, rcv; int i) { + mtype msg; +CLOSED: + state[i] = ClosedState; + if + :: goto LISTEN; + :: snd ! SYN; goto SYN_SENT; + fi; + +LISTEN: + state[i] = ListenState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! SYN; snd ! ACK; goto SYN_RECEIVED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto SYN_RECEIVED; + :: msg == ACK -> + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +ESTABLISHED: + state[i] = EstState; + do + :: snd ! FIN; goto FIN_WAIT_1; + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSE_WAIT; + :: else -> skip; + fi + od; + +FIN_WAIT_1: + state[i] = FinW1State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSING; + :: msg == ACK -> goto FIN_WAIT_2; + :: else -> skip; + fi + od; + +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSING: + state[i] = ClosingState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; + +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto CLOSED; + :: else -> skip; + fi + od; + +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + atomic { + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); + } +} + +/* liveness: simultaneous close resolution */ +ltl phi7 { + always ( + (state[0] == FinW1State && state[1] == FinW1State) + implies + (eventually (state[0] == ClosedState) && + eventually (state[1] == ClosedState)) + ) +} diff --git a/tests/tcp/tcp-phi8.pml b/tests/tcp/tcp-phi8.pml new file mode 100644 index 0000000..14e264c --- /dev/null +++ b/tests/tcp/tcp-phi8.pml @@ -0,0 +1,146 @@ +mtype = { SYN, FIN, ACK } + +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; + +int state[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 + +proctype TCP(chan snd, rcv; int i) { + mtype msg; +CLOSED: + state[i] = ClosedState; + if + :: goto LISTEN; + :: snd ! SYN; goto SYN_SENT; + fi; + +LISTEN: + state[i] = ListenState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! SYN; snd ! ACK; goto SYN_RECEIVED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto SYN_RECEIVED; + :: msg == ACK -> + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +ESTABLISHED: + state[i] = EstState; + do + :: snd ! FIN; goto FIN_WAIT_1; + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSE_WAIT; + :: else -> skip; + fi + od; + +FIN_WAIT_1: + state[i] = FinW1State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSING; + :: msg == ACK -> goto FIN_WAIT_2; + :: else -> skip; + fi + od; + +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSING: + state[i] = ClosingState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; + +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto CLOSED; + :: else -> skip; + fi + od; + +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + atomic { + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); + } +} + +/* liveness: active close eventually terminates */ +ltl phi8 { + always ( + (state[0] == FinW1State) implies (eventually (state[0] == ClosedState)) + ) +} diff --git a/tests/tcp/tcp-phi9.pml b/tests/tcp/tcp-phi9.pml new file mode 100644 index 0000000..a1971dd --- /dev/null +++ b/tests/tcp/tcp-phi9.pml @@ -0,0 +1,148 @@ +mtype = { SYN, FIN, ACK } + +chan AtoB = [2] of { mtype }; +chan BtoA = [2] of { mtype }; + +int state[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 + +proctype TCP(chan snd, rcv; int i) { + mtype msg; +CLOSED: + state[i] = ClosedState; + if + :: goto LISTEN; + :: snd ! SYN; goto SYN_SENT; + fi; + +LISTEN: + state[i] = ListenState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! SYN; snd ! ACK; goto SYN_RECEIVED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto SYN_RECEIVED; + :: msg == ACK -> + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +ESTABLISHED: + state[i] = EstState; + do + :: snd ! FIN; goto FIN_WAIT_1; + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSE_WAIT; + :: else -> skip; + fi + od; + +FIN_WAIT_1: + state[i] = FinW1State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSING; + :: msg == ACK -> goto FIN_WAIT_2; + :: else -> skip; + fi + od; + +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSING: + state[i] = ClosingState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; + +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto CLOSED; + :: else -> skip; + fi + od; + +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + atomic { + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); + } +} + +/* safety: handshake cannot be bypassed */ +ltl phi9 { + always ( + (state[0] == ListenState) + implies + !(next (state[0] == EstState)) + ) +} diff --git a/tests/tcp/tcp.pml b/tests/tcp/tcp.pml index 1792fbe..890107c 100644 --- a/tests/tcp/tcp.pml +++ b/tests/tcp/tcp.pml @@ -1,10 +1,9 @@ -mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } +mtype = { SYN, FIN, ACK } chan AtoB = [2] of { mtype }; chan BtoA = [2] of { mtype }; int state[2]; -int pids[2]; #define ClosedState 0 #define ListenState 1 @@ -17,122 +16,124 @@ int pids[2]; #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; + mtype msg; CLOSED: - state[i] = ClosedState; - do - /* Passive open */ - :: goto LISTEN; - /* Active open */ - :: snd ! SYN; goto SYN_SENT; - /* Terminate */ - :: goto end; - od + state[i] = ClosedState; + if + :: goto LISTEN; + :: snd ! SYN; goto SYN_SENT; + fi; + 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; + state[i] = ListenState; do - :: rcv ? SYN -> - snd ! ACK; - goto ESTABLISHED; - :: rcv ? _ -> skip; - od - :: rcv ? _ -> skip; - :: timeout -> goto CLOSED; /* Timeout */ - od + :: rcv ? msg -> + if + :: msg == SYN -> snd ! SYN; snd ! ACK; goto SYN_RECEIVED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto SYN_RECEIVED; + :: msg == ACK -> + do + :: rcv ? msg -> + if + :: msg == SYN -> snd ! ACK; goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od + :: else -> skip; + fi + :: timeout -> goto CLOSED; + od; + SYN_RECEIVED: - state[i] = SynRecState; - do - :: rcv ? ACK -> goto ESTABLISHED; - :: rcv ? _ -> skip; - od + state[i] = SynRecState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto ESTABLISHED; + :: else -> skip; + fi + :: timeout -> goto CLOSED; + 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 + state[i] = EstState; + do + :: snd ! FIN; goto FIN_WAIT_1; + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSE_WAIT; + :: else -> skip; + fi + 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 + state[i] = FinW1State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto CLOSING; + :: msg == ACK -> goto FIN_WAIT_2; + :: else -> skip; + fi + od; + FIN_WAIT_2: - state[i] = FinW2State; - do - :: rcv ? FIN -> - snd ! ACK; - goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = FinW2State; + do + :: rcv ? msg -> + if + :: msg == FIN -> snd ! ACK; goto TIME_WAIT; + :: else -> skip; + fi + od; + CLOSING: - state[i] = ClosingState; - do - :: rcv ? ACK -> goto TIME_WAIT; - :: rcv ? _ -> skip; - od + state[i] = ClosingState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto TIME_WAIT; + :: else -> skip; + fi + od; + +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; + LAST_ACK: - state[i] = LastAckState; - do - :: rcv ? ACK -> goto CLOSED; - :: rcv ? _ -> skip; - od + state[i] = LastAckState; + do + :: rcv ? msg -> + if + :: msg == ACK -> goto CLOSED; + :: else -> skip; + fi + od; + TIME_WAIT: - state[i] = TimeWaitState; - goto CLOSED; -end: - state[i] = EndState; + state[i] = TimeWaitState; + goto CLOSED; } init { - state[0] = ClosedState; - state[1] = ClosedState; - run TCP(AtoB, BtoA, 0); - run TCP(BtoA, AtoB, 1); + state[0] = ClosedState; + state[1] = ClosedState; + atomic { + run TCP(AtoB, BtoA, 0); + run TCP(BtoA, AtoB, 1); + } }