Skip to content
Snippets Groups Projects
Commit 26006bdf authored by hansen's avatar hansen
Browse files

added command line switch (assertion check)

parent 674f5e9a
No related branches found
No related tags found
No related merge requests found
......@@ -139,6 +139,8 @@ public class TLC4B {
TLC4BGlobals.setGOAL(false);
} else if (args[index].toLowerCase().equals("-noinv")) {
TLC4BGlobals.setInvariant(false);
}else if (args[index].toLowerCase().equals("-noass")) {
TLC4BGlobals.setAssertionCheck(false);
} else if (args[index].toLowerCase().equals("-wdcheck")) {
TLC4BGlobals.setWelldefinednessCheck(true);
} else if (args[index].toLowerCase().equals("-tool")) {
......
......@@ -8,6 +8,7 @@ public class TLC4BGlobals {
private static boolean checkGOAL;
private static boolean checkDeadlock;
private static boolean checkInvariant;
private static boolean checkAssertion;
private static boolean checkLTL;
private static boolean checkWD;
private static boolean proBconstantsSetup;
......@@ -43,6 +44,7 @@ public class TLC4BGlobals {
checkGOAL = true;
checkDeadlock = true;
checkInvariant = true;
checkAssertion = true;
checkLTL = true;
checkWD= false;
......@@ -118,6 +120,10 @@ public class TLC4BGlobals {
return checkInvariant;
}
public static boolean isAssertion() {
return checkAssertion;
}
public static boolean isCheckltl() {
return checkLTL;
}
......@@ -170,6 +176,10 @@ public class TLC4BGlobals {
TLC4BGlobals.checkInvariant = invariant;
}
public static void setAssertionCheck(boolean b) {
TLC4BGlobals.checkAssertion = b;
}
public static void setCheckltl(boolean checkltl) {
TLC4BGlobals.checkLTL = checkltl;
}
......
......@@ -211,12 +211,11 @@ public class TLAPrinter extends DepthFirstAdapter {
this.configFileString.append("INVARIANT NotGoal\n");
}
if (configFile.getAssertionSize() > 0) {
if (TLC4BGlobals.isAssertion()) {
for (int i = 0; i < configFile.getAssertionSize(); i++) {
this.configFileString.append("INVARIANT Assertion" + (i + 1)
+ "\n");
}
}
if (TLC4BGlobals.isCheckltl()) {
......@@ -416,6 +415,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
private void printAssertions() {
if (TLC4BGlobals.isAssertion()) {
ArrayList<Node> assertions = tlaModule.getAssertions();
if (assertions.size() == 0)
return;
......@@ -424,7 +424,7 @@ public class TLAPrinter extends DepthFirstAdapter {
assertions.get(i).apply(this);
tlaModuleString.append("\n");
}
}
}
private void printInit() {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment