Refactor hardcoded set of all Servers out of ccfraft.

microsoft · Oct 31, 2023 · 0afd920 · 0afd920
1 parent 40a3783
commit 0afd920
Show file tree

Hide file tree

Showing 7 changed files with 10 additions and 28 deletions.
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -42,8 +42,6 @@ CONSTANTS
     NodeOne = n1
     NodeTwo = n2
     NodeThree = n3
-    NodeFour = n4
-    NodeFive = n5
 
 SYMMETRY Symmetry
 VIEW View

diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
@@ -1,6 +1,9 @@
 ---------- MODULE MCccfraft ----------
 EXTENDS ccfraft, TLC
 
+CONSTANTS
+    NodeOne, NodeTwo, NodeThree
+
 1Configuration == <<{NodeOne, NodeTwo, NodeThree}>>
 3Configurations == <<{NodeOne}, {NodeOne, NodeTwo}, {NodeTwo}>>
 

diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -42,8 +42,6 @@ CONSTANTS
     NodeOne = n1
     NodeTwo = n2
     NodeThree = n3
-    NodeFour = n4
-    NodeFive = n5
 
 SYMMETRY Symmetry
 VIEW View

diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
@@ -1,6 +1,9 @@
 ---------- MODULE SIMccfraft ----------
 EXTENDS ccfraft, TLC, Integers
 
+CONSTANTS
+    NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive
+
 Servers_mc == {NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive}
 
 ----

diff --git a/tla/consensus/Traceccfraft.cfg b/tla/consensus/Traceccfraft.cfg
@@ -39,7 +39,6 @@ CHECK_DEADLOCK
 
 CONSTANTS
     Servers <- TraceServers
-    AllServers <- TraceServers
 
     \* Redefine the AppendEntries batch size to model empty and batches with arbitrary size.
     AppendEntriesBatchsize <- TraceAppendEntriesBatchsize

diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
@@ -76,6 +76,9 @@ JsonServers ==
 
 ASSUME JsonServers \in Nat \ {0}
 
+CONSTANTS
+    NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive
+
 TraceServers ==
     Range(SubSeq(<<NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive>>, 1, JsonServers))
 ASSUME TraceServers \subseteq Servers

diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -81,25 +81,9 @@ CONSTANTS
     TypeSignature,
     TypeReconfiguration
 
-CONSTANTS
-    NodeOne,
-    NodeTwo,
-    NodeThree,
-    NodeFour,
-    NodeFive
-
-AllServers == {
-    NodeOne,
-    NodeTwo,
-    NodeThree,
-    NodeFour,
-    NodeFive
-}
-
 \* Set of nodes for this model
 CONSTANTS Servers
-ASSUME Servers /= {}
-ASSUME Servers \subseteq AllServers
+ASSUME Servers /= {} /\ IsFiniteSet(Servers)
 
 Nil ==
   (*************************************************************************)
@@ -1401,12 +1385,6 @@ DebugInvLeaderCannotStepDown ==
         /\ currentTerm[m.source] = m.term
         => state[m.source] = Leader
 
-\* This invariant shows that it should be possible for Node 4 or 5 to become leader
-\* Note that symmetry for the set of servers should be disabled to check this debug invariant
-DebugInvReconfigLeader ==
-    /\ state[NodeFour] /= Leader
-    /\ state[NodeFive] /= Leader
-
 \* This invariant shows that a txn can be committed after a reconfiguration
 DebugInvSuccessfulCommitAfterReconfig ==
     \lnot (