TCP according to RFC 9293.

README.md

@@ -87,7 +87,8 @@ Here is a list of specs included in this repository, with links to the relevant
 | [RFC 3506: Voucher Transaction System](specifications/byihive)                                      | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani |          |             |         |     ✔     |          |
 | [TLA⁺ Level Checking](specifications/LevelChecking)                                                 | Leslie Lamport                                      |          |             |         |           |          |
 | [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder           |          |             |         |           |          |
-| [Yo-Yo Leader Election](specifications/YoYo)                                                 | Ludovic Yvoz, Stephan Merz           |          |             |         |      ✔    |          |
+| [Yo-Yo Leader Election](specifications/YoYo)                                                        | Ludovic Yvoz, Stephan Merz                          |          |             |         |      ✔    |          |
+| [TCP as defined in RFC 9293](specifications/tcp)                                                    | Markus Kuppe                                        |          |             |         |      ✔    |          |
 
 ## Examples Elsewhere
 Here is a list of specs stored in locations outside this repository, including submodules.

manifest.json

@@ -5144,6 +5144,49 @@
           ]
         }
       ]
+    },
+    {
+      "path": "specifications/tcp",
+      "title": "TCP as defined in RFC 9293",
+      "description": "Transmission Control Protocol (TCP)",
+      "sources": ["https://datatracker.ietf.org/doc/html/rfc9293"],
+      "authors": [
+        "Markus Kuppe"
+      ],
+      "tags": [],
+      "modules": [
+        {
+          "path": "specifications/tcp/tcp.tla",
+          "communityDependencies": [
+            "SequencesExt"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/tcp/MCtcp.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/tcp/MCtcp.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "state constraint",
+                "liveness"
+              ],
+              "result": "success",
+              "distinctStates": 1182,
+              "totalStates": 6322,
+              "stateDepth": 14
+            }
+          ]
+        }
+      ]
     }
   ]
 }

specifications/tcp/MCtcp.cfg

@@ -0,0 +1,27 @@
+CONSTANTS
+    A = A
+    B = B
+
+CONSTANT
+    Peers <- peers
+    Init <- MCInit
+
+\* Disable symmetry reduction when checking liveness.
+\* SYMMETRY
+\*     Symmetry
+
+SPECIFICATION 
+    Spec
+
+INVARIANT 
+    TypeOK
+    Inv
+
+PROPERTY 
+    Prop
+
+CONSTRAINT 
+    NoRetransmission
+
+ACTION_CONSTRAINT 
+    SingleActiveOpen

specifications/tcp/MCtcp.tla

@@ -0,0 +1,32 @@
+---- MODULE MCtcp ----
+EXTENDS tcp, TLC
+
+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 :
+            network[p][i] # network[p][i + 1]
+
+SingleActiveOpen ==
+    \* A real system will allow infinitely many active opens of TCP connections. An
+    \* explicit state model checker like TLC cannot enumerate infinitely many states.
+    \* Thus, do not allow multiple active opens (the first active open is implicit in Init).
+    ~ \E local, remote \in Peers:
+        \/ ACTIVE_OPEN(local, remote)
+        \/ PASSIVE_OPEN(local, remote)
+        \/ SEND(local, remote)
+
+=============================================================================
+\* Modification History
+\* Created Tue Apr 02 10:38:50 PDT 2024 by markus