Add a liveness property.

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

Author: lemmy

manifest.json

@@ -5177,7 +5177,7 @@
               "mode": "exhaustive search",
               "features": [
                 "state constraint",
-                "symmetry"
+                "liveness"
               ],
               "result": "success",
               "distinctStates": 598,

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
 

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