Changing index into Configurations in MCccfraft.tla (#5779)

microsoft · Oct 25, 2023 · 22d92a8 · 22d92a8
1 parent b7cfab8
commit 22d92a8
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 4 deletions.
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -78,6 +78,7 @@ INVARIANTS
     MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
+    \* DebugAllReconfigurationsReachableInv
     \* DebugInvLeaderCannotStepDown
     \* DebugInvAnyCommitted
     \* DebugInvAllCommitted

diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
@@ -22,10 +22,9 @@ CCF == INSTANCE ccfraft
 \* In addition to basic settings of how many nodes are to be model checked,
 \* the model allows to place additional limitations on the state space of the program.
 MCChangeConfigurationInt(i, newConfiguration) ==
-    /\ reconfigurationCount < Len(Configurations)-1
+    /\ reconfigurationCount < Len(Configurations)
     \* +1 because TLA+ sequences are 1-index
-    \* +1 to lookup the *next* and not the current configuration. 
-    /\ newConfiguration = Configurations[reconfigurationCount+2]
+    /\ newConfiguration = Configurations[reconfigurationCount+1]
     /\ CCF!ChangeConfigurationInt(i, newConfiguration)
 
 \* Limit the terms that can be reached. Needs to be set to at least 3 to
@@ -102,6 +101,16 @@ View == << reconfigurationVars, <<messages, commitsNotified>>, serverVars, candi
 
 ----
 
+AllReconfigurationsCommitted == 
+    \E s \in ToServers:
+        \A c \in ToSet(Configurations):
+            \E i \in DOMAIN Committed(s):
+                /\ HasTypeReconfiguration(Committed(s)[i])
+                /\ Committed(s)[i].configuration = c
+
+DebugAllReconfigurationsReachableInv ==
+    ~AllReconfigurationsCommitted
+
 \* Returns true if server i has committed value v, false otherwise
 IsCommittedByServer(v,i) ==
     IF commitIndex[i]  = 0

diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -4,7 +4,7 @@ CONSTANTS
     Configurations <- 3Configurations
     Servers <- ToServers
 
-    MaxTermLimit = 2
+    MaxTermLimit = 3
     MaxCommitsNotified = 2
 
     Timeout <- MCTimeout
@@ -78,6 +78,7 @@ INVARIANTS
     MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
+    DebugAllReconfigurationsReachableInv
     \* DebugInvLeaderCannotStepDown
     \* DebugInvAnyCommitted
     \* DebugInvAllCommitted