diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 93a2294332d24f60f2047d3bc5358f7eee17453d..9ce03d6c5def446b69bcb3935bd6c906630a43ea 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -71,16 +71,32 @@ public class TLC4B {
}
- private void printResults(TLCResults results, boolean createTraceFile) {
+ private void printResults(TLCResults results, boolean createTraceFile) {
+ //options
+ System.out.println("Used Options");
+ System.out.println("| Number of workers: " + TLC4BGlobals.getWorkers());
+ System.out.println("| Invariants check: " + TLC4BGlobals.isInvariant());
+ System.out.println("| Deadlock check: " + TLC4BGlobals.isDeadlockCheck());
+ System.out.println("| Assertion check: " + TLC4BGlobals.isAssertion());
+ System.out.println("| Find Goal check: " + TLC4BGlobals.isGOAL());
+ System.out.println("| LTL formulas check: " + TLC4BGlobals.isCheckLTL());
+ System.out.println("| Partial invariant evaluation: " + TLC4BGlobals.isPartialInvariantEvaluation());
+ System.out.println("| Lazy constants setup: " + !TLC4BGlobals.isForceTLCToEvalConstants());
+ System.out.println("| Agressive well-definedness check: " + TLC4BGlobals.checkWelldefinedness());
+ System.out.println("| Prob constant setup: " + TLC4BGlobals.isProBconstantsSetup());
+ System.out.println("| Symmetry used: " + TLC4BGlobals.useSymmetry());
+ System.out.print("| MIN Int: " + TLC4BGlobals.getMIN_INT());
+ System.out.print(" | MAX Int: " + TLC4BGlobals.getMAX_INT());
+ System.out.println(" | Deferret set size: " + TLC4BGlobals.getDEFERRED_SET_SIZE());
+ System.out.println("--------------------------------");
System.out.println("Parsing time: " + StopWatch.getRunTime("Parsing")
+ " ms");
System.out.println("Translation time: " + StopWatch.getRunTime("Pure")
+ " ms");
System.out.println("Model checking time: "
+ results.getModelCheckingTime() + " sec");
- System.out.println("Number of workers: "
- + TLCGlobals.getNumWorkers());
+ //System.out.println("Number of workers: " + TLCGlobals.getNumWorkers());
System.out.println("States analysed: "
+ results.getNumberOfDistinctStates());
System.out.println("Transitions fired: "
@@ -142,7 +158,7 @@ public class TLC4B {
TLC4BGlobals.setGOAL(false);
} else if (args[index].toLowerCase().equals("-noinv")) {
TLC4BGlobals.setInvariant(false);
- }else if (args[index].toLowerCase().equals("-noass")) {
+ } else if (args[index].toLowerCase().equals("-noass")) {
TLC4BGlobals.setAssertionCheck(false);
} else if (args[index].toLowerCase().equals("-wdcheck")) {
TLC4BGlobals.setWelldefinednessCheck(true);
@@ -231,7 +247,7 @@ public class TLC4B {
System.out.print(" ");
}
System.out.println();
-
+
handleMainFileName();
if (TLC4BGlobals.isTranslate()) {
StopWatch.start("Parsing");
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 4e483c39fe6086cee77f12512a7690010533af92..48180c17444466adc6b787d814fd1fe9a74fdf46 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -13,6 +13,7 @@ public class TLC4BGlobals {
private static boolean checkWD;
private static boolean proBconstantsSetup;
private static boolean partialInvariantEvaluation;
+ private static boolean useSymmetry;
private static boolean deleteFilesOnExit;
@@ -20,16 +21,15 @@ public class TLC4BGlobals {
private static boolean translate;
private static boolean hideTLCConsoleOutput;
private static boolean createTraceFile;
-
+
private static boolean testingMode;
-
+
private static boolean cleanup;
private static boolean forceTLCToEvalConstants;
-
+
private static int workers;
-
-
+
private static boolean runTestscript;
static {
@@ -46,17 +46,17 @@ public class TLC4BGlobals {
checkInvariant = true;
checkAssertion = true;
checkLTL = true;
- checkWD= false;
+ checkWD = false;
partialInvariantEvaluation = false;
-
+ useSymmetry = false;
setForceTLCToEvalConstants(true);
-
+
setProBconstantsSetup(false);
setCleanup(true);
-
+
workers = 1;
-
+
// for debugging purposes
runTLC = true;
translate = true;
@@ -69,8 +69,7 @@ public class TLC4BGlobals {
runTestscript = false;
testingMode = false;
createTraceFile = true;
-
-
+
}
public static boolean isCreateTraceFile() {
@@ -120,12 +119,12 @@ public class TLC4BGlobals {
public static boolean isInvariant() {
return checkInvariant;
}
-
+
public static boolean isAssertion() {
return checkAssertion;
}
- public static boolean isCheckltl() {
+ public static boolean isCheckLTL() {
return checkLTL;
}
@@ -136,12 +135,12 @@ public class TLC4BGlobals {
public static boolean isDeleteOnExit() {
return deleteFilesOnExit;
}
-
- public static boolean isPartialInvariantEvaluation(){
+
+ public static boolean isPartialInvariantEvaluation() {
return partialInvariantEvaluation;
}
-
- public static void setPartialInvariantEvaluation(boolean b){
+
+ public static void setPartialInvariantEvaluation(boolean b) {
partialInvariantEvaluation = b;
}
@@ -176,7 +175,7 @@ public class TLC4BGlobals {
public static void setInvariant(boolean invariant) {
TLC4BGlobals.checkInvariant = invariant;
}
-
+
public static void setAssertionCheck(boolean b) {
TLC4BGlobals.checkAssertion = b;
}
@@ -193,11 +192,11 @@ public class TLC4BGlobals {
TLC4BGlobals.deleteFilesOnExit = deleteOnExit;
}
- public static void setWorkers(int w){
+ public static void setWorkers(int w) {
TLC4BGlobals.workers = w;
}
-
- public static int getWorkers(){
+
+ public static int getWorkers() {
return TLC4BGlobals.workers;
}
@@ -216,20 +215,20 @@ public class TLC4BGlobals {
public static void setProBconstantsSetup(boolean proBconstantsSetup) {
TLC4BGlobals.proBconstantsSetup = proBconstantsSetup;
}
-
- public static void setTestingMode(boolean b){
+
+ public static void setTestingMode(boolean b) {
TLC4BGlobals.testingMode = b;
}
-
- public static boolean getTestingMode(){
+
+ public static boolean getTestingMode() {
return TLC4BGlobals.testingMode;
}
-
- public static void setWelldefinednessCheck(boolean b){
+
+ public static void setWelldefinednessCheck(boolean b) {
TLC4BGlobals.checkWD = b;
}
-
- public static boolean checkWelldefinedness(){
+
+ public static boolean checkWelldefinedness() {
return TLC4BGlobals.checkWD;
}
@@ -237,8 +236,17 @@ public class TLC4BGlobals {
return forceTLCToEvalConstants;
}
- public static void setForceTLCToEvalConstants(boolean forceTLCToEvalConstants) {
+ public static void setForceTLCToEvalConstants(
+ boolean forceTLCToEvalConstants) {
TLC4BGlobals.forceTLCToEvalConstants = forceTLCToEvalConstants;
}
-
+
+ public static boolean useSymmetry() {
+ return useSymmetry;
+ }
+
+ public static void setSymmetryUse(boolean b) {
+ useSymmetry = b;
+ }
+
}
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index e5f97f15d7c04165a86c8f48404ff5d00a55a5af..0838dff52ce6df8446d889e8e66d07809f3b3555 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -61,7 +61,7 @@ public class TLCRunner {
list.add("-deadlock");
}
- if (TLC4BGlobals.isCheckltl()) {
+ if (TLC4BGlobals.isCheckLTL()) {
list.add("-cleanup");
}
// list.add("-coverage");
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 90cc278554f1663b05f2c43e66b4c3c1b6d16d95..0db6b07057522f599df6ea665ddd52d8707e3ebd 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -298,7 +298,7 @@ public class MachineContext extends DepthFirstAdapter {
AExpressionDefinitionDefinition def = (AExpressionDefinitionDefinition) e;
String name = def.getName().getText();
if (name.startsWith("ASSERT_LTL")) {
- if (TLC4BGlobals.isCheckltl()) {
+ if (TLC4BGlobals.isCheckLTL()) {
LTLFormulaVisitor visitor = new LTLFormulaVisitor(name,
this);
visitor.parseDefinition(def);
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index ffedc495c64bbb2446269657a4bb18993c08b7c0..2e93d96b142e7e0eb78f7e9ab7b01168494c1cd9 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -179,7 +179,7 @@ public class TLAPrinter extends DepthFirstAdapter {
private void printLTLFormulas() {
ArrayList<LTLFormulaVisitor> visitors = machineContext.getLTLFormulas();
- if (TLC4BGlobals.isCheckltl()) {
+ if (TLC4BGlobals.isCheckLTL()) {
for (int i = 0; i < visitors.size(); i++) {
LTLFormulaVisitor visitor = visitors.get(i);
tlaModuleString.append(visitor.getName() + " == ");
@@ -218,7 +218,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
}
- if (TLC4BGlobals.isCheckltl()) {
+ if (TLC4BGlobals.isCheckLTL()) {
for (int i = 0; i < machineContext.getLTLFormulas().size(); i++) {
LTLFormulaVisitor ltlVisitor = machineContext.getLTLFormulas()
.get(i);
diff --git a/src/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java
index d944885186b5b731891dca208d553902d356a54b..9174a97bea44dffc4dc88150d048e960f95c206a 100644
--- a/src/main/java/de/tlc4b/tla/Generator.java
+++ b/src/main/java/de/tlc4b/tla/Generator.java
@@ -89,7 +89,7 @@ public class Generator extends DepthFirstAdapter {
private void evalSpec() {
if (this.configFile.isInit() && this.configFile.isNext()
- && TLC4BGlobals.isCheckltl()
+ && TLC4BGlobals.isCheckLTL()
&& machineContext.getLTLFormulas().size() > 0) {
this.configFile.setSpec();
}