diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java index 96f65628f5d0946657221eb116a8169d586b4108..f3aac592f34254ee495ba0e96b672618a6ab40da 100644 --- a/src/main/java/de/tlc4b/TLC4B.java +++ b/src/main/java/de/tlc4b/TLC4B.java @@ -81,8 +81,7 @@ public class TLC4B { * @return results of TLC model check */ public static TLCResults run(String[] args) throws TLC4BException, IOException, BCompoundException { - System.setProperty("apple.awt.UIElement", "true"); - // avoiding pop up window + System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up window TLC4B tlc4b = new TLC4B(); tlc4b.process(args); @@ -150,6 +149,8 @@ public class TLC4B { printOperationsCount(results); // options printlnSilent("Used Options"); + if (TLC4BGlobals.getDfidInitialDepth() > 0) // -1 if disabled + printlnSilent("| Use DFS with initial depth: " + TLC4BGlobals.getDfidInitialDepth()); printlnSilent("| Number of workers: " + TLC4BGlobals.getWorkers()); printlnSilent("| Invariants check: " + TLC4BGlobals.isInvariant()); printlnSilent("| Deadlock check: " + TLC4BGlobals.isDeadlockCheck()); @@ -208,8 +209,6 @@ public class TLC4B { public static void test(String[] args, boolean deleteFiles) throws Exception { System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows - TLC4BGlobals.resetGlobals(); - TLC4BGlobals.setDeleteOnExit(deleteFiles); TLC4B tlc4b = new TLC4B(); try { tlc4b.process(args); @@ -218,6 +217,7 @@ public class TLC4B { printlnErr(e.getMessage()); throw e; } + TLC4BGlobals.setDeleteOnExit(deleteFiles); if (TLC4BGlobals.isRunTLC()) { MP.TLCOutputStream.changeOutputStream(); TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension, tlc4b.buildDir); @@ -233,7 +233,6 @@ public class TLC4B { public static void testString(String machineString, boolean deleteFiles) throws Exception { System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows - TLC4BGlobals.resetGlobals(); TLC4BGlobals.setDeleteOnExit(deleteFiles); TLC4B tlc4b = new TLC4B(); tlc4b.buildDir = new File("temp/"); @@ -288,6 +287,8 @@ public class TLC4B { mainfile = new File(remainingArgs[0]); } + // reset all parameters to default, then apply current args + TLC4BGlobals.resetGlobals(); TLC4BGlobals.setVerbose(line.hasOption(VERBOSE.arg())); TLC4BGlobals.setSilent(line.hasOption(SILENT.arg())); TLC4BGlobals.setDeadlockCheck(!line.hasOption(NODEAD.arg())); diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java index 9f06c585c1c3f7adb9ba92f28ac6d732af4c0149..d6ccdea86faace053e5851b9806f3eb42e5815fb 100644 --- a/src/main/java/de/tlc4b/TLCRunner.java +++ b/src/main/java/de/tlc4b/TLCRunner.java @@ -19,6 +19,7 @@ import java.util.Set; import de.tlc4b.tlc.TLCMessageListener; import de.tlc4b.util.StopWatch; +import tlc2.TLCGlobals; import util.SimpleFilenameToStream; import util.ToolIO; import tlc2.TLC; @@ -105,10 +106,18 @@ public class TLCRunner { if (TLC4BGlobals.getWorkers() > 1) { list.add("-workers"); list.add("" + TLC4BGlobals.getWorkers()); + } else { + // When running multiple model checks from ProB2, the global state is not reset. + // Reset number of workers manually here, are there any other problematic options?! + TLCGlobals.setNumWorkers(1); } if (TLC4BGlobals.getDfidInitialDepth() >= 0) { list.add("-dfid"); list.add("" + TLC4BGlobals.getDfidInitialDepth()); + } else { + // When running multiple model checks from ProB2, the global state is not reset. + // Reset DFID manually here if not selected, are there any other problematic options?! + TLCGlobals.DFIDMax = -1; } if (TLC4BGlobals.isPrintCoverage()) {