Add DebugInvUpToDepth invariant to SIMccfraft to quickly generate a t…

…race of length N by passing N to TLC's `-depth` cli.
microsoft · Dec 22, 2023 · 580e865 · 580e865
1 parent a850a08
commit 580e865
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
@@ -90,3 +90,4 @@ INVARIANTS
     \* DebugInvSuccessfulCommitAfterReconfig
     \* DebugInvAllMessagesProcessable
     \* DebugInvRetirementReachable
+    \* DebugInvUpToDepth
diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
@@ -48,6 +48,10 @@ StopAfter ==
     (* The smoke test has a time budget of 20 minutes. *)
     IN TLCSet("exit", TLCGet("duration") > timeout)
 
+DebugInvUpToDepth ==
+    \* The following invariant causes TLC to terminate with a counterexample of length
+    \* -depth after generating the first trace.
+    TLCGet("level") < TLCGet("config").depth
 =============================================================================
 
 ------------------------------- MODULE SIMPostCondition -------------------------------