adding CommittableIndicesAreKnownSignaturesInv to exhaustive model ch…

…ecking
microsoft · Oct 25, 2023 · 231a13e · 231a13e
1 parent 27b44fa
commit 231a13e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -77,6 +77,7 @@ INVARIANTS
     NoLeaderInTermZeroInv
     MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
+    CommittableIndicesAreKnownSignaturesInv
     \* DebugInvLeaderCannotStepDown
     \* DebugInvAnyCommitted
     \* DebugInvAllCommitted

diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -77,6 +77,7 @@ INVARIANTS
     NoLeaderInTermZeroInv
     MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
+    CommittableIndicesAreKnownSignaturesInv
     \* DebugInvLeaderCannotStepDown
     \* DebugInvAnyCommitted
     \* DebugInvAllCommitted