diff --git a/specifications/tcp/MCtcp.cfg b/specifications/tcp/MCtcp.cfg
index 0b4b9c74..cc307ca9 100644
--- a/specifications/tcp/MCtcp.cfg
+++ b/specifications/tcp/MCtcp.cfg
@@ -4,6 +4,7 @@ CONSTANTS
 
 CONSTANT
     Peers <- peers
+    Init <- MCInit
 
 SYMMETRY
     Symmetry
diff --git a/specifications/tcp/MCtcp.tla b/specifications/tcp/MCtcp.tla
index 4e7810e8..e0cee03e 100644
--- a/specifications/tcp/MCtcp.tla
+++ b/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 :
diff --git a/specifications/tcp/tcp.tla b/specifications/tcp/tcp.tla
index 7e01da22..62269c84 100644
--- a/specifications/tcp/tcp.tla
+++ b/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: