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