fix error in Sailfish

Author: nano-o

specifications/dag-consensus/Sailfish.tla

@@ -30,8 +30,8 @@ INSTANCE BlockDag \* Import definitions related to DAGs of blocks
         es = {}; \* the edges of the DAG
     define {
         dag == <<vs, es>>
-        NoLeaderVoteQuorum(r, deliveredVertices, add) ==
-            LET NoLeaderVote == {v \in deliveredVertices : LeaderVertex(r-1) \notin Children(dag, v)}
+        NoLeaderVoteQuorum(r, vertices, add) ==
+            LET NoLeaderVote == {v \in vertices : LeaderVertex(r-1) \notin Children(dag, v)}
             IN  IsQuorum({Node(v) : v \in NoLeaderVote} \cup add)
     }
     process (correctNode \in N \ F)
@@ -63,7 +63,7 @@ l0:     while (TRUE) {
                     \* have evidence it cannot commit:
                     if (Leader(r) = self)
                         await   \/ LeaderVertex(r-1) \in deliveredVertices
-                                \/ NoLeaderVoteQuorum(r, deliveredVertices, {self});
+                                \/ NoLeaderVoteQuorum(r, {v \in vs : Round(v) = r}, {self});
                     \* create a new vertex:
                     with (newV = <<self, r>>) {
                         vs := vs \cup {newV};
@@ -104,14 +104,14 @@ l0:     while (TRUE) {
         }
     }
 }*)
-\* BEGIN TRANSLATION (chksum(pcal) = "444b3304" /\ chksum(tla) = "3580c6e5")
+\* BEGIN TRANSLATION (chksum(pcal) = "c16dfa43" /\ chksum(tla) = "9cdbd4f5")
 \* Label l0 of process correctNode at line 42 col 9 changed to l0_
 VARIABLES vs, es
 
 (* define statement *)
 dag == <<vs, es>>
-NoLeaderVoteQuorum(r, deliveredVertices, add) ==
-    LET NoLeaderVote == {v \in deliveredVertices : LeaderVertex(r-1) \notin Children(dag, v)}
+NoLeaderVoteQuorum(r, vertices, add) ==
+    LET NoLeaderVote == {v \in vertices : LeaderVertex(r-1) \notin Children(dag, v)}
     IN  IsQuorum({Node(v) : v \in NoLeaderVote} \cup add)
 
 VARIABLES round, log
@@ -142,7 +142,7 @@ correctNode(self) == IF round[self] = 0
                                          \/ NoLeaderVoteQuorum(r-1, deliveredVertices, {})
                                     /\ IF Leader(r) = self
                                           THEN /\ \/ LeaderVertex(r-1) \in deliveredVertices
-                                                  \/ NoLeaderVoteQuorum(r, deliveredVertices, {self})
+                                                  \/ NoLeaderVoteQuorum(r, {v \in vs : Round(v) = r}, {self})
                                           ELSE /\ TRUE
                                     /\ LET newV == <<self, r>> IN
                                          /\ vs' = (vs \cup {newV})

specifications/dag-consensus/TLCSailfish1.cfg

@@ -1,4 +1,4 @@
-SPECIFICATION Spec
+SPECIFICATION TerminatingSpec
 
 CONSTANTS
     n1 = n1

specifications/dag-consensus/TLCSailfish1.tla

@@ -17,12 +17,12 @@ CONSTANTS
 
 N == {n1,n2,n3}
 F == {n1}
-R == 1..4
+R == 1..5
 IsQuorum(Q) == Q \in {{n1,n3},{n2,n3},{n1,n2,n3}}
 IsBlocking(B) == B \in {{n3},{n1,n3},{n2,n3},{n1,n2,n3}}
 LeaderSchedule == <<n1,n2,n3>>
 Leader(r) == LeaderSchedule[((r-1) % Cardinality(N))+1]
-GST == 2
+GST == 3
 
 INSTANCE Sailfish
 
@@ -31,6 +31,10 @@ INSTANCE Sailfish
 (**************************************************************************************)
 StateConstraint == \A n \in N \ F : round[n] \in 0..Max(R)
 
+Done == \A n \in N \ F : round[n] = Max(R)
+Terminate == Done /\ UNCHANGED <<vs, es, round, log>>
+TerminatingSpec == Init /\ [][Next \/ Terminate]_<<vs, es, round, log>>
+
 (**************************************************************************************)
 (* Finally, we give some properties we expect to be violated (useful to get the       *)
 (* model-checker to print interesting executions).                                    *)

specifications/dag-consensus/TLCSailfish2.cfg

@@ -1,4 +1,4 @@
-SPECIFICATION Spec
+SPECIFICATION TerminatingSpec
 
 CONSTANTS
     n1 = n1

specifications/dag-consensus/TLCSailfish2.tla

@@ -26,4 +26,8 @@ INSTANCE Sailfish
 
 StateConstraint == \A n \in N \ F : round[n] \in 0..Max(R)
 
+Done == \A n \in N \ F : round[n] = Max(R)
+Terminate == Done /\ UNCHANGED <<vs, es, round, log>>
+TerminatingSpec == Init /\ [][Next \/ Terminate]_<<vs, es, round, log>>
+
 ===========================================================================

specifications/dag-consensus/manifest.json

@@ -41,9 +41,9 @@
           "runtime": "00:00:10",
           "mode": "exhaustive search",
           "result": "success",
-          "distinctStates": 5158,
-          "totalStates": 13180,
-          "stateDepth": 13
+          "distinctStates": 109604,
+          "totalStates": 314144,
+          "stateDepth": 16
         }
       ]
     },