Add a liveness property.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
tlaplus · Apr 6, 2024 · 64a9291 · 64a9291
1 parent 43b4c93
commit 64a9291
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 6 deletions.
diff --git a/manifest.json b/manifest.json
@@ -5177,11 +5177,11 @@
               "mode": "exhaustive search",
               "features": [
                 "state constraint",
-                "symmetry"
+                "liveness"
               ],
               "result": "success",
-              "distinctStates": 598,
-              "totalStates": 3196,
+              "distinctStates": 1182,
+              "totalStates": 6322,
               "stateDepth": 14
             }
           ]

diff --git a/specifications/tcp/MCtcp.cfg b/specifications/tcp/MCtcp.cfg
@@ -6,8 +6,9 @@ CONSTANT
     Peers <- peers
     Init <- MCInit
 
-SYMMETRY
-    Symmetry
+\* Disable symmetry reduction when checking liveness.
+\* SYMMETRY
+\*     Symmetry
 
 SPECIFICATION 
     Spec
@@ -16,6 +17,9 @@ INVARIANT
     TypeOK
     Inv
 
+PROPERTY 
+    Prop
+
 CONSTRAINT 
     NoRetransmission
 

diff --git a/specifications/tcp/tcp.tla b/specifications/tcp/tcp.tla
@@ -261,7 +261,7 @@ Spec ==
     /\ [][Next]_vars
     /\ WF_vars(System)
     \* Would get stuck in SYN-SENT if we don't assert a user command.
-    /\ WF_vars(\E local, remote \in Peers: CLOSE_CLOSE_WAIT(local, remote))
+    /\ WF_vars(\E local, remote \in Peers: CLOSE_SYN_SENT(local, remote))
 
 -----------------------------------------------------------------------------
 
@@ -272,6 +272,10 @@ Inv ==
     \A local, remote \in { p \in Peers : network[p] = <<>> } :
         connstate[local] = "ESTABLISHED" <=> connstate[remote] = "ESTABLISHED"
 
+Prop ==
+    \A p \in Peers :
+        connstate[p] = "SYN-SENT" ~> connstate[p] \in {"ESTABLISHED", "LISTEN", "CLOSED"}
+
 =============================================================================
 \* Modification History
 \* Created Tue Apr 02 10:38:50 PDT 2024 by markus