# --- 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-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: property violation
  - explanation: Replaying B's packets symmetrically tricks A into entering Established while B is closed, causing a half-open state.

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: no violation
  - explanation: A sends SYN and waits for a response; it does not emit a FIN to reorder until Established. No half-open state can be triggered this way.

# --- 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-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: acceptance cycle
  - explanation: Infinite replaying by the attacker traps the model in a processing livelock, halting global 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: no violation
  - explanation: Out-of-order packets are skipped, causing endpoints to correctly resolve to ClosedState via timeouts rather than deadlocking.

# --- 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-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-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: no violation
  - explanation: Invalidly ordered ACKs are skipped, resulting in a timeout to ClosedState, which legally satisfies the phi5 property.

# --- 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-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-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: no violation
  - explanation: Swapped packets are skipped, causing endpoints to successfully timeout to ClosedState

# --- 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-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-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: no violation
  - explanation: Skipped invalid packets force a timeout to ClosedState, successfully satisfying the property.

# --- PHI 9: HANDSHAKE CANNOT BE BYPASSED ---

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.