Move TLC-specific Init to MCInit in MCtcp.tla and rewrite Init to a g…

…eneric one (both CLOSED, no TCB, and empty network).

Signed-off-by: Markus Alexander Kuppe <[email protected]>

specifications/tcp/MCtcp.cfg

@@ -4,6 +4,7 @@ CONSTANTS
 
 CONSTANT
     Peers <- peers
+    Init <- MCInit
 
 SYMMETRY
     Symmetry

specifications/tcp/MCtcp.tla

@@ -5,6 +5,14 @@ CONSTANTS A, B
 peers == {A, B}
 Symmetry == Permutations(peers)
 
+MCInit ==
+    \* One node starts in the SYN-SENT state, i.e., one node has already received the active open command. The other node
+    \* is in the listen state, i.e., it has received the passive open command.
+    \E node \in Peers:
+        /\ tcb = [p \in Peers |-> TRUE]
+        /\ connstate = [p \in Peers |-> IF p = node THEN "SYN-SENT" ELSE "LISTEN"]
+        /\ network = [p \in Peers |-> IF p = node THEN <<>> ELSE << "SYN" >>]
+
 NoRetransmission ==
     \A p \in Peers :
         \A i \in 1..Len(network[p]) - 1 :

specifications/tcp/tcp.tla

@@ -31,12 +31,9 @@ TypeOK ==
     /\ network \in [ Peers -> Seq({"SYN", "SYN,ACK", "ACK", "RST", "FIN"} \cup {"ACKofFIN"}) ]
 
 Init ==
-    \* One node starts in the SYN-SENT state, i.e., one node has already received the active open command. The other node
-    \* is in the listen state, i.e., it has received the passive open command.
-    \E node \in Peers:
-        /\ tcb = [p \in Peers |-> TRUE]
-        /\ connstate = [p \in Peers |-> IF p = node THEN "SYN-SENT" ELSE "LISTEN"]
-        /\ network = [p \in Peers |-> IF p = node THEN <<>> ELSE << "SYN" >>]
+    /\ tcb = [p \in Peers |-> FALSE]
+    /\ connstate = [p \in Peers |-> "CLOSED"]
+    /\ network = [p \in Peers |-> <<>>]
 
 \* Action triggered by user commands: