Adding CommittableIndicesAreKnownSignaturesInv to exhaustive model …

…checking (#5775)
microsoft · Oct 25, 2023 · a26e68f · a26e68f
1 parent 2280654
commit a26e68f
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