From 580e8654a831d854cf5b2422ad1da2a4ddfc5d0b Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Fri, 22 Dec 2023 15:45:00 +0000
Subject: [PATCH] Add DebugInvUpToDepth invariant to SIMccfraft to quickly
 generate a trace of length N by passing N to TLC's `-depth` cli.

---
 tla/consensus/SIMccfraft.cfg | 1 +
 tla/consensus/SIMccfraft.tla | 4 ++++
 2 files changed, 5 insertions(+)

diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
index b920aaba8f2b..c778561b2650 100644
--- a/tla/consensus/SIMccfraft.cfg
+++ b/tla/consensus/SIMccfraft.cfg
@@ -90,3 +90,4 @@ INVARIANTS
     \* DebugInvSuccessfulCommitAfterReconfig
     \* DebugInvAllMessagesProcessable
     \* DebugInvRetirementReachable
+    \* DebugInvUpToDepth
\ No newline at end of file
diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
index bfacc4e7fda5..916fb2bc1d5f 100644
--- 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 -------------------------------