From b7af771863e5484d449146c5a789a46ede5c7954 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Tue, 24 Mar 2020 21:11:06 -0700
Subject: [PATCH] "-lncheck seqfinal" checks satisfiability branches of
liveness checking sequentially.
Multiple properties are usually split into individual branches that TLC
checks in parallel. In memory constrained environments, running the
branches sequentially trades memory (space) for time.
[Feature][TLC]
---
tlatools/src/tlc2/TLCGlobals.java | 6 +++++-
tlatools/src/tlc2/tool/liveness/LiveCheck.java | 2 +-
2 files changed, 6 insertions(+), 2 deletions(-)
diff --git a/tlatools/src/tlc2/TLCGlobals.java b/tlatools/src/tlc2/TLCGlobals.java
index d199f3fac..e6aee0b5c 100644
--- a/tlatools/src/tlc2/TLCGlobals.java
+++ b/tlatools/src/tlc2/TLCGlobals.java
@@ -52,7 +52,11 @@ public class TLCGlobals
public static String lnCheck = "default";
public static boolean doLiveness() {
- return !lnCheck.equals("final");
+ return !(lnCheck.equals("final") || lnCheck.equals("seqfinal"));
+ }
+
+ public static boolean doSequentialLiveness() {
+ return lnCheck.startsWith("seq");
}
public synchronized static void setNumWorkers(int n)
diff --git a/tlatools/src/tlc2/tool/liveness/LiveCheck.java b/tlatools/src/tlc2/tool/liveness/LiveCheck.java
index 5d15cebc3..f253e135f 100644
--- a/tlatools/src/tlc2/tool/liveness/LiveCheck.java
+++ b/tlatools/src/tlc2/tool/liveness/LiveCheck.java
@@ -227,7 +227,7 @@ public class LiveCheck implements ILiveCheck {
* a violation found by another LW. However, if any LW fails to check, we terminate
* model checking after all LWs completed.
*/
- final int wNum = Math.min(checker.length, TLCGlobals.getNumWorkers());
+ final int wNum = TLCGlobals.doSequentialLiveness() ? 1 : Math.min(checker.length, TLCGlobals.getNumWorkers());
final ExecutorService pool = Executors.newFixedThreadPool(wNum);
// CS is really just a container around the set of Futures returned by the pool. It saves us from
// creating a low-level array.
--
GitLab