From 64a9291aada2da41af614f3e57cd9fea38c63c49 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Sat, 6 Apr 2024 13:10:38 -0700
Subject: [PATCH] Add a liveness property.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
---
 manifest.json                | 6 +++---
 specifications/tcp/MCtcp.cfg | 8 ++++++--
 specifications/tcp/tcp.tla   | 6 +++++-
 3 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/manifest.json b/manifest.json
index 9cad59fa..4385e8f3 100644
--- 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
index cc307ca9..0b4087b2 100644
--- 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
index 62269c84..6fe7a523 100644
--- 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