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>
microsoft · Sep 27, 2024 · 8620bd4 · 8620bd4
1 parent e14391a
commit 8620bd4
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
@@ -16,4 +16,7 @@ PROPERTIES
     AppendOnlyProp
 
 SYMMETRY 
-    Symmetry
+    Symmetry
+
+CONSTRAINT 
+    MaxLogLengthConstraint
diff --git 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
 ====