From 8620bd4ff86016b6301b4f150aec93d9e8f409cd Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Thu, 26 Sep 2024 16:15:54 -0700
Subject: [PATCH] Limit the global length of all logs to 7 during model
 checking.

(Maintains the checked state space)

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
---
 tla/consensus/MCabs.cfg | 5 ++++-
 tla/consensus/MCabs.tla | 4 ++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
index e6ea03411ca..5160e4f8660 100644
--- a/tla/consensus/MCabs.cfg
+++ b/tla/consensus/MCabs.cfg
@@ -16,4 +16,7 @@ PROPERTIES
     AppendOnlyProp
 
 SYMMETRY 
-    Symmetry
\ No newline at end of file
+    Symmetry
+
+CONSTRAINT 
+    MaxLogLengthConstraint
diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla
index 849dbdcef24..b2ed29ba3bf 100644
--- a/tla/consensus/MCabs.tla
+++ b/tla/consensus/MCabs.tla
@@ -10,4 +10,8 @@ CONSTANTS NodeOne, NodeTwo, NodeThree
 MCServers == {NodeOne, NodeTwo, NodeThree}
 MCTerms == 2..4
 
+\* Limit length of logs to terminate model checking.
+MaxLogLengthConstraint ==
+    \A i \in Servers :
+        Len(cLogs[i]) <= 7
 ====
\ No newline at end of file