diff --git a/._n_i_p_s_ b/._n_i_p_s_ new file mode 100644 index 0000000..ea80a74 --- /dev/null +++ b/._n_i_p_s_ @@ -0,0 +1,21 @@ +ltl phi3 { + !(eventually (((always (state[0] == 2)) || + (always (state[0] == 3)) || + (always (state[0] == 4)) || + (always (state[0] == 5)) || + (always (state[0] == 6)) || + (always (state[0] == 7)) || + (always (state[0] == 8)) || + (always (state[0] == 9)) || + (always (state[0] == 10))) + && + ((always (state[1] == 2)) || + (always (state[1] == 3)) || + (always (state[1] == 4)) || + (always (state[1] == 5)) || + (always (state[1] == 6)) || + (always (state[1] == 7)) || + (always (state[1] == 8)) || + (always (state[1] == 9)) || + (always (state[1] == 10))))) +} diff --git a/src/__pycache__/model_generate.cpython-313.pyc b/src/__pycache__/model_generate.cpython-313.pyc index 58b0958..7ed32ce 100644 Binary files a/src/__pycache__/model_generate.cpython-313.pyc and b/src/__pycache__/model_generate.cpython-313.pyc differ diff --git a/src/model_generate.py b/src/model_generate.py index 4729af0..b8cf2ff 100644 --- a/src/model_generate.py +++ b/src/model_generate.py @@ -283,7 +283,6 @@ def gen_replay_unbounded(chan : str, chan_type : List[str], mem : int, index : i # return ret_string - def gen_reorder(chan : str, chan_type : List[str], mem : int, index : int) -> str: ret_string = "" diff --git a/tests/abp/abp.pml b/tests/abp/abp.pml new file mode 100644 index 0000000..02f6562 --- /dev/null +++ b/tests/abp/abp.pml @@ -0,0 +1,59 @@ +mtype = { DATA0, DATA1, ACK0, ACK1 } + +chan AtoB = [1] of { mtype } +chan BtoA = [1] of { mtype } + +mtype ackA, ackB; +byte seqA = 0; +byte seqB = 0; + +mtype packetA, packetB; + +active proctype A() +{ + do + :: + if + :: seqA == 0 -> packetA = DATA0 + :: else -> packetA = DATA1 + fi; + AtoB!packetA; + do + :: BtoA?ackA -> + if + :: (seqA == 0 && ackA == ACK0) || (seqA == 1 && ackA == ACK1) -> + seqA = 1 - seqA; + break + :: else -> skip; + fi + :: + AtoB!packetA + od + od +} + +active proctype B() +{ + do + :: AtoB?packetB -> + if + :: (seqB == 0 && packetB == DATA0) || (seqB == 1 && packetB == DATA1) -> + if + :: seqB == 0 -> ackB = ACK0 + :: else -> ackB = ACK1 + fi; + BtoA!ackB; + seqB = 1 - seqB; + :: else -> + if + :: seqB == 0 -> ackB = ACK1 + :: else -> ackB = ACK0 + fi; + BtoA!ackB; + fi + od +} + +ltl liveness { + always ((packetA != packetB) implies eventually (packetA == packetB)) +} diff --git a/tests/paper.yaml b/tests/paper.yaml new file mode 100644 index 0000000..e37883d --- /dev/null +++ b/tests/paper.yaml @@ -0,0 +1,154 @@ +unidirectional-drop-abp: + - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol + +bidirectional-drop-abp: + - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol + +tcp-phi1-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping A's outbound messages alone is insufficient to create a half-open state; B cannot reach Established without receiving from A + +tcp-phi1-drop-BtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping B's outbound messages prevents B from progressing; A times out back to Closed, no half-open + +tcp-phi1-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping on both directions prevents any handshake progress; neither side reaches Established + +tcp-phi1-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replaying A's SYN can drive B into Established via a forged handshake while A returns to Closed, creating a half-open state + +tcp-phi1-replay-BtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replaying B's SYN+ACK can cause A to believe handshake completed; if A then closes, B may remain Established + +tcp-phi1-replay-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replaying on both channels gives the attacker maximum ability to manufacture a half-open state + +tcp-phi1-reorder-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: property violation + - explanation: reordering A's messages (e.g., delivering ACK before SYN) can desynchronize the handshake, leading to half-open + +tcp-phi1-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: property violation + - explanation: reordering on both channels maximizes desynchronization potential for half-open + +tcp-phi2-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping A's SYN prevents the handshake from completing, violating the liveness property that A should eventually reach Established + +tcp-phi2-drop-BtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=drop --chan=BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping B's SYN+ACK response prevents A from ever completing the handshake + +tcp-phi2-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping on both channels trivially prevents connection establishment + +tcp-phi2-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying A's messages does not prevent establishment; extra SYNs are handled by B's wildcard receives + +tcp-phi2-reorder-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi2.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: acceptance cycle + - explanation: reordering A's handshake messages can prevent B from following the correct SYN/ACK sequence, stalling establishment + +tcp-phi3-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping A's messages can cause B to stall indefinitely in SynReceived or similar waiting states + +tcp-phi3-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping on both channels can strand both sides in intermediate states with no timeout recovery + +tcp-phi3-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: replaying stale messages can trap B in a loop re-processing old handshake messages + +tcp-phi3-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: acceptance cycle + - explanation: reordering on both channels can desynchronize both sides into permanently mismatched states + +tcp-phi4-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: during simultaneous open, dropping A's SYN prevents B from advancing, breaking the simultaneous open guarantee + +tcp-phi4-drop-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping both sides' SYNs trivially prevents simultaneous open from resolving + +tcp-phi4-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying SYN messages during simultaneous open should not prevent eventual establishment; the protocol handles duplicate SYNs + +tcp-phi4-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi4.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: acceptance cycle + - explanation: reordering handshake messages during simultaneous open can prevent the SYN+ACK exchange from completing correctly + +tcp-phi5-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: if A's ACK is dropped, B remains stuck in SynReceived with no timeout to recover + +tcp-phi5-drop-BtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: acceptance cycle + - explanation: dropping B's SYN+ACK means A never sends ACK, leaving the initiator-side SynReceived unresolved + +tcp-phi5-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: replaying A's messages provides additional ACKs that can help resolve SynReceived + +tcp-phi5-reorder-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: acceptance cycle + - explanation: reordering can deliver A's SYN after the ACK, confusing B's state machine and trapping it in SynReceived + +tcp-phi6-drop-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: dropping A's messages while in Closing does not cause A to transition to an unexpected state; A remains in Closing or eventually times out + +tcp-phi6-replay-AtoN: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replaying a FIN while in Closing could cause a transition to TimeWait instead of the expected Closing or Closed + +tcp-phi6-replay-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: replaying on both channels maximizes the chance of injecting an unexpected ACK that transitions Closing to TimeWait, violating the next-state constraint + +tcp-phi6-reorder-bidirectional: + - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2 + - intended: property violation + - explanation: reordering close-sequence messages can cause ACK delivery at unexpected times, violating the strict Closing transition property diff --git a/tests/tcp/pan b/tests/tcp/pan new file mode 100755 index 0000000..7f43cf2 Binary files /dev/null and b/tests/tcp/pan differ diff --git a/tests/tcp/props/phi1.pml b/tests/tcp/props/phi1.pml new file mode 100644 index 0000000..e4bd47e --- /dev/null +++ b/tests/tcp/props/phi1.pml @@ -0,0 +1,4 @@ +/* safety: half-open prevention */ +ltl phi1 { + always ( leftClosed implies !rightEstablished ) +} diff --git a/tests/tcp/props/phi2.pml b/tests/tcp/props/phi2.pml new file mode 100644 index 0000000..ce34527 --- /dev/null +++ b/tests/tcp/props/phi2.pml @@ -0,0 +1,5 @@ +/* liveness: verifying connection establishment */ +ltl phi2 { + ( (always ( eventually ( state[0] == 1 && state[1] == 2 ) ) ) + implies ( eventually ( state[0] == 4 ) ) ) +} diff --git a/tests/tcp/props/phi3.pml b/tests/tcp/props/phi3.pml new file mode 100644 index 0000000..10b0c9b --- /dev/null +++ b/tests/tcp/props/phi3.pml @@ -0,0 +1,22 @@ +/* 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/props/phi4.pml b/tests/tcp/props/phi4.pml new file mode 100644 index 0000000..6b9cac3 --- /dev/null +++ b/tests/tcp/props/phi4.pml @@ -0,0 +1,11 @@ +/* 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/props/phi5.pml b/tests/tcp/props/phi5.pml new file mode 100644 index 0000000..17fcc0b --- /dev/null +++ b/tests/tcp/props/phi5.pml @@ -0,0 +1,13 @@ +/* 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/props/phi6.pml b/tests/tcp/props/phi6.pml new file mode 100644 index 0000000..27eb391 --- /dev/null +++ b/tests/tcp/props/phi6.pml @@ -0,0 +1,9 @@ +/* safety: strict closing transitions */ +ltl phi6 { + always ( + (state[0] == ClosingState) + implies + (next (state[0] == ClosingState || + state[0] == ClosedState)) + ) +} diff --git a/tests/tcp/tcp-phi1.pml b/tests/tcp/tcp-phi1.pml new file mode 100644 index 0000000..a8da96a --- /dev/null +++ b/tests/tcp/tcp-phi1.pml @@ -0,0 +1,149 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* safety: half-open prevention */ +ltl phi1 { + always ( leftClosed implies !rightEstablished ) +} diff --git a/tests/tcp/tcp-phi2.pml b/tests/tcp/tcp-phi2.pml new file mode 100644 index 0000000..d423edc --- /dev/null +++ b/tests/tcp/tcp-phi2.pml @@ -0,0 +1,149 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: verifying connection establishment */ +ltl phi2 { + ( (always ( eventually ( state[0] == 1 && state[1] == 2 ) ) ) + implies ( eventually ( state[0] == 4 ) ) ) diff --git a/tests/tcp/tcp-phi2.pml.trail b/tests/tcp/tcp-phi2.pml.trail new file mode 100644 index 0000000..319ff39 --- /dev/null +++ b/tests/tcp/tcp-phi2.pml.trail @@ -0,0 +1,55 @@ +-2:2:-2 +-4:-4:-4 +1:0:121 +2:1:114 +3:0:121 +4:1:115 +5:0:121 +6:1:116 +7:0:121 +8:1:117 +9:0:121 +10:3:0 +11:0:121 +12:3:1 +13:0:121 +14:3:2 +15:0:121 +16:3:9 +17:0:121 +18:2:0 +19:0:121 +20:2:1 +21:0:121 +22:2:2 +23:0:121 +24:2:9 +25:0:121 +26:3:17 +27:0:121 +28:3:1 +29:0:121 +30:3:3 +31:0:121 +32:3:22 +33:0:119 +34:2:17 +35:0:126 +36:2:1 +37:0:121 +38:2:3 +39:0:121 +40:2:22 +41:0:121 +42:2:42 +43:0:121 +44:2:1 +-1:-1:-1 +45:0:121 +46:2:2 +47:0:121 +48:2:9 +49:0:119 +50:2:17 +51:0:126 +52:2:1 diff --git a/tests/tcp/tcp-phi3.pml b/tests/tcp/tcp-phi3.pml new file mode 100644 index 0000000..b1e9e80 --- /dev/null +++ b/tests/tcp/tcp-phi3.pml @@ -0,0 +1,167 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: no infinite stalls/deadlocks */ +ltl phi3 { + !(eventually (((always (state[0] == SynSentState)) || + (always (state[0] == SynRecState)) || + (always (state[0] == EstState)) || + (always (state[0] == FinW1State)) || + (always (state[0] == CloseWaitState)) || + (always (state[0] == FinW2State)) || + (always (state[0] == ClosingState)) || + (always (state[0] == LastAckState)) || + (always (state[0] == TimeWaitState))) + && + ((always (state[1] == SynSentState)) || + (always (state[1] == SynRecState)) || + (always (state[1] == EstState)) || + (always (state[1] == FinW1State)) || + (always (state[1] == CloseWaitState)) || + (always (state[1] == FinW2State)) || + (always (state[1] == ClosingState)) || + (always (state[1] == LastAckState)) || + (always (state[1] == TimeWaitState))))) +} diff --git a/tests/tcp/tcp-phi4.pml b/tests/tcp/tcp-phi4.pml new file mode 100644 index 0000000..3ca2932 --- /dev/null +++ b/tests/tcp/tcp-phi4.pml @@ -0,0 +1,156 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: simultanous open */ +ltl phi4 { + always ( + (state[0] == SynSentState && + state[1] == SynSentState) + + implies + + ((eventually state[0] == EstState) && + (eventually state[1] == EstState))) +} diff --git a/tests/tcp/tcp-phi4.pml.trail b/tests/tcp/tcp-phi4.pml.trail new file mode 100644 index 0000000..08508a0 --- /dev/null +++ b/tests/tcp/tcp-phi4.pml.trail @@ -0,0 +1,43 @@ +-2:2:-2 +-4:-4:-4 +1:0:122 +2:1:114 +3:0:122 +4:1:115 +5:0:122 +6:1:116 +7:0:122 +8:1:117 +9:0:122 +10:3:0 +11:0:122 +12:3:1 +13:0:122 +14:3:2 +15:0:122 +16:3:9 +17:0:122 +18:2:0 +19:0:122 +20:2:1 +21:0:122 +22:2:2 +23:0:122 +24:2:9 +25:0:122 +26:3:17 +27:0:122 +28:3:1 +29:0:122 +30:3:3 +31:0:122 +32:3:22 +33:0:122 +34:2:17 +35:0:122 +36:2:1 +37:0:122 +38:2:3 +39:0:122 +40:2:22 +41:0:119 diff --git a/tests/tcp/tcp-phi5.pml b/tests/tcp/tcp-phi5.pml new file mode 100644 index 0000000..e675b63 --- /dev/null +++ b/tests/tcp/tcp-phi5.pml @@ -0,0 +1,158 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* liveness: SYN_RECEIVED resolution*/ +ltl phi5 { + always ( + (state[0] == SynRecState) + implies ( + eventually ( + (state[0] == EstState || + state[0] == FinW1State || + state[0] == ClosedState) + ) + ) + ) +} diff --git a/tests/tcp/tcp-phi6.pml b/tests/tcp/tcp-phi6.pml new file mode 100644 index 0000000..fc14aeb --- /dev/null +++ b/tests/tcp/tcp-phi6.pml @@ -0,0 +1,154 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ClosedState; + do + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + od +LISTEN: + state[i] = ListenState; + do + :: rcv ? SYN -> + atomic { + snd ! SYN; + snd ! ACK; + goto SYN_RECEIVED; + } + /* Simultaneous LISTEN */ + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; + od +SYN_SENT: + state[i] = SynSentState; + do + :: rcv ? SYN; + if + /* Standard behavior */ + :: rcv ? ACK -> snd ! ACK; goto ESTABLISHED; + /* Simultaneous open */ + :: snd ! ACK; goto SYN_RECEIVED; + fi + :: rcv ? ACK; + do + :: rcv ? SYN -> + snd ! ACK; + goto ESTABLISHED; + :: rcv ? _ -> skip; + od + :: rcv ? _ -> skip; + :: timeout -> goto CLOSED; /* Timeout */ + od +SYN_RECEIVED: + state[i] = SynRecState; + do + :: rcv ? ACK -> goto ESTABLISHED; + :: rcv ? _ -> skip; + od + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + do + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSE_WAIT; + :: rcv ? _ -> skip; + od +FIN_WAIT_1: + state[i] = FinW1State; + do + /* Simultaneous close */ + :: rcv ? FIN -> + snd ! ACK; + goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + :: rcv ? _ -> skip; + od +CLOSE_WAIT: + state[i] = CloseWaitState; + do + :: snd ! FIN; goto LAST_ACK; + :: rcv ? _ -> skip; + od +FIN_WAIT_2: + state[i] = FinW2State; + do + :: rcv ? FIN -> + snd ! ACK; + goto TIME_WAIT; + :: rcv ? _ -> skip; + od +CLOSING: + state[i] = ClosingState; + do + :: rcv ? ACK -> goto TIME_WAIT; + :: rcv ? _ -> skip; + od +LAST_ACK: + state[i] = LastAckState; + do + :: rcv ? ACK -> goto CLOSED; + :: rcv ? _ -> skip; + od +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} + +/* safety: strict closing transitions */ +ltl phi6 { + always ( + (state[0] == ClosingState) + implies + (next (state[0] == ClosingState || + state[0] == ClosedState)) + ) +} diff --git a/tests/tcp/tcp.pml b/tests/tcp/tcp.pml new file mode 100644 index 0000000..be7125b --- /dev/null +++ b/tests/tcp/tcp.pml @@ -0,0 +1,144 @@ +// models: phi1, phi2, phi3, phi5 +// does not model: phi4, phi7 +// not yet implemented: phi6 +mtype = { SYN, FIN, ACK, ABORT, CLOSE, RST, OPEN } + +chan AtoN = [1] of { mtype }; +chan NtoA = [0] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [0] 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); +}