From 41cf332bcbf152c522407a882bc5dee252978023 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Thu, 18 Jul 2024 06:59:53 +0200
Subject: [PATCH] add -dfid option for depth-first search
---
src/main/java/de/tlc4b/TLC4B.java | 7 +++++
src/main/java/de/tlc4b/TLC4BCliOptions.java | 1 +
src/main/java/de/tlc4b/TLC4BGlobals.java | 28 +++++++++++++------
src/main/java/de/tlc4b/TLCRunner.java | 4 +++
src/main/java/de/tlc4b/tlc/TLCResults.java | 4 +--
.../de/tlc4b/tlc/integration/BasicTest.java | 7 +++++
6 files changed, 40 insertions(+), 11 deletions(-)
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 880bd4d..046c822 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -317,6 +317,13 @@ public class TLC4B {
}
TLC4BGlobals.setWorkers(Integer.parseInt(workers));
}
+ if (line.hasOption(DFID.arg())) {
+ String dfid_initial_depth = line.getOptionValue(DFID.arg());
+ if (dfid_initial_depth == null) {
+ throw new TLC4BIOException("Error: Number required after option '-dfid'.");
+ }
+ TLC4BGlobals.setDfidInitialDepth(Integer.parseInt(dfid_initial_depth));
+ }
if (line.hasOption(CONSTANTSSETUP.arg())) {
TLC4BGlobals.setProBconstantsSetup(true);
constantsSetup = line.getOptionValue(CONSTANTSSETUP.arg());
diff --git a/src/main/java/de/tlc4b/TLC4BCliOptions.java b/src/main/java/de/tlc4b/TLC4BCliOptions.java
index 70fce66..c71b74a 100644
--- a/src/main/java/de/tlc4b/TLC4BCliOptions.java
+++ b/src/main/java/de/tlc4b/TLC4BCliOptions.java
@@ -29,6 +29,7 @@ public class TLC4BCliOptions {
DEFAULT_SETSIZE("default_setsize", "", Integer.class),
MININT("minint", "", Integer.class),
WORKERS("workers", "", Integer.class),
+ DFID("dfid", "depth-first model checking with iterative deepening, specify initial depth", Integer.class),
CONSTANTSSETUP("constantssetup", "use constants found by ProB for TLC model checking", String.class),
LTLFORMULA("ltlformula", "", String.class),
VERBOSE("verbose", "put TLC4B in verbose mode", null),
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 93b492c..8a510ca 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -34,6 +34,7 @@ public class TLC4BGlobals {
private static boolean forceTLCToEvalConstants;
private static int workers;
+ private static int dfid_initial_depth;
private static boolean runTestscript;
@@ -57,12 +58,15 @@ public class TLC4BGlobals {
printCoverage = false;
forceTLCToEvalConstants = false;
checkOnlyMainAssertions = false;
+ verbose = false;
+ silent = false;
proBconstantsSetup = false;
cleanup = true;
workers = 1;
+ dfid_initial_depth = -1; // option not selected
// for debugging purposes
runTLC = true;
@@ -147,20 +151,20 @@ public class TLC4BGlobals {
partialInvariantEvaluation = b;
}
- public static void setDEFERRED_SET_SIZE(int DEFERRED_SET_SIZE) {
- TLC4BGlobals.DEFERRED_SET_SIZE = DEFERRED_SET_SIZE;
+ public static void setDEFERRED_SET_SIZE(int deferredSetSize) {
+ TLC4BGlobals.DEFERRED_SET_SIZE = deferredSetSize;
}
- public static void setMAX_INT(int mAX_INT) {
- MAX_INT = mAX_INT;
+ public static void setMAX_INT(int maxInt) {
+ TLC4BGlobals.MAX_INT = maxInt;
}
- public static void setMIN_INT(int mIN_INT) {
- MIN_INT = mIN_INT;
+ public static void setMIN_INT(int minInt) {
+ TLC4BGlobals.MIN_INT = minInt;
}
- public static void setGOAL(boolean gOAL) {
- checkGOAL = gOAL;
+ public static void setGOAL(boolean goal) {
+ TLC4BGlobals.checkGOAL = goal;
}
public static void setDeadlockCheck(boolean deadlockCheck) {
@@ -203,6 +207,14 @@ public class TLC4BGlobals {
return TLC4BGlobals.workers;
}
+ public static void setDfidInitialDepth(int depth) {
+ TLC4BGlobals.dfid_initial_depth = depth;
+ }
+
+ public static int getDfidInitialDepth() {
+ return TLC4BGlobals.dfid_initial_depth;
+ }
+
public static boolean isCleanup() {
return cleanup;
}
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index 7bbb47f..9f06c58 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -106,6 +106,10 @@ public class TLCRunner {
list.add("-workers");
list.add("" + TLC4BGlobals.getWorkers());
}
+ if (TLC4BGlobals.getDfidInitialDepth() >= 0) {
+ list.add("-dfid");
+ list.add("" + TLC4BGlobals.getDfidInitialDepth());
+ }
if (TLC4BGlobals.isPrintCoverage()) {
list.add("-nowarning");
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index f59445b..99c032d 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -230,13 +230,11 @@ public class TLCResults implements ToolGlobals {
break;
case EC.TLC_STATS:
+ case EC.TLC_STATS_DFID:
numberOfTransitions = Integer.parseInt(m.getParameters()[0]);
numberOfDistinctStates = Integer.parseInt(m.getParameters()[1]);
break;
- case EC.TLC_STATS_DFID:
- break;
-
case EC.TLC_SUCCESS:
tlcResult = TLCResult.NoError;
break;
diff --git a/src/test/java/de/tlc4b/tlc/integration/BasicTest.java b/src/test/java/de/tlc4b/tlc/integration/BasicTest.java
index 0204d72..0c22eb6 100644
--- a/src/test/java/de/tlc4b/tlc/integration/BasicTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/BasicTest.java
@@ -12,6 +12,7 @@ import org.junit.runner.RunWith;
import java.io.File;
import java.util.ArrayList;
+import static de.tlc4b.TLC4BCliOptions.TLCOption.DFID;
import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
@@ -33,6 +34,12 @@ public class BasicTest extends AbstractParseMachineTest {
assertEquals(error, test(a));
}
+ @Test
+ public void testRunTLCDFS() throws Exception {
+ String[] a = new String[] { machine.getPath(), "-" + DFID.arg(), "20" };
+ assertEquals(error, test(a));
+ }
+
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<>();
--
GitLab