removing MatchIndexLowerBoundNextIndexInv

microsoft · Jan 8, 2024 · 7bce884 · 7bce884
1 parent ec7e172
commit 7bce884
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 4 deletions.
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -77,6 +77,5 @@ INVARIANTS
     MonoLogInv
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
-    MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -77,6 +77,5 @@ INVARIANTS
     MonoLogInv
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
-    MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
@@ -77,8 +77,6 @@ INVARIANTS
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
 
-    MatchIndexLowerBoundNextIndexInv
-
     CommitCommittableIndices
 
     CommittableIndicesAreKnownSignaturesInv

diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -1247,6 +1247,9 @@ NoLeaderBeforeInitialTerm ==
     \A i \in Servers :
         currentTerm[i] < StartTerm => state[i] # Leader
 
+\* MatchIndexLowerBoundNextIndexInv is not currently an invariant but 
+\* we might wish to add it in the future. This could be achieved by updating 
+\* nextIndex to max of current nextIndex and matchIndex when an AE ACK is received.
 MatchIndexLowerBoundNextIndexInv ==
     \A i,j \in Servers :
         state[i] = Leader =>