From 26006bdf7b2782d199aa648a3babdf49a1a779cf Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Tue, 13 Jan 2015 15:56:24 +0100
Subject: [PATCH] added command line switch (assertion check)
---
src/main/java/de/tlc4b/TLC4B.java | 2 ++
src/main/java/de/tlc4b/TLC4BGlobals.java | 10 +++++++
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 28 +++++++++----------
3 files changed, 26 insertions(+), 14 deletions(-)
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 88638b8..7404ea7 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -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")) {
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 27fd599..366232b 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -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;
@@ -117,6 +119,10 @@ public class TLC4BGlobals {
public static boolean isInvariant() {
return checkInvariant;
}
+
+ public static boolean isAssertion() {
+ return checkAssertion;
+ }
public static boolean isCheckltl() {
return checkLTL;
@@ -169,6 +175,10 @@ public class TLC4BGlobals {
public static void setInvariant(boolean invariant) {
TLC4BGlobals.checkInvariant = invariant;
}
+
+ public static void setAssertionCheck(boolean b) {
+ TLC4BGlobals.checkAssertion = b;
+ }
public static void setCheckltl(boolean checkltl) {
TLC4BGlobals.checkLTL = checkltl;
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 6e3fe3c..b77f668 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -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()) {
@@ -236,10 +235,10 @@ public class TLAPrinter extends DepthFirstAdapter {
configFileString.append(assignments.get(i).getString(renamer));
}
}
- if(TLC4BGlobals.isPartialInvariantEvaluation()){
+ if (TLC4BGlobals.isPartialInvariantEvaluation()) {
configFileString.append("CONSTANTS\n");
configFileString.append("Init1 = Init1\n");
-
+
ArrayList<POperation> operations = tlaModule.getOperations();
StringBuilder sb = new StringBuilder();
sb.append("{");
@@ -250,7 +249,7 @@ public class TLAPrinter extends DepthFirstAdapter {
configFileString.append(name + "1");
configFileString.append("\n");
sb.append(name + "1");
- if(i < operations.size()-1){
+ if (i < operations.size() - 1) {
sb.append(", ");
}
}
@@ -260,7 +259,7 @@ public class TLAPrinter extends DepthFirstAdapter {
configFileString.append("\n");
configFileString.append("VIEW myView");
}
-
+
}
public void moduleStringAppend(String str) {
@@ -416,15 +415,16 @@ public class TLAPrinter extends DepthFirstAdapter {
}
private void printAssertions() {
- ArrayList<Node> assertions = tlaModule.getAssertions();
- if (assertions.size() == 0)
- return;
- for (int i = 0; i < assertions.size(); i++) {
- tlaModuleString.append("Assertion" + (i + 1) + " == ");
- assertions.get(i).apply(this);
- tlaModuleString.append("\n");
+ if (TLC4BGlobals.isAssertion()) {
+ ArrayList<Node> assertions = tlaModule.getAssertions();
+ if (assertions.size() == 0)
+ return;
+ for (int i = 0; i < assertions.size(); i++) {
+ tlaModuleString.append("Assertion" + (i + 1) + " == ");
+ assertions.get(i).apply(this);
+ tlaModuleString.append("\n");
+ }
}
-
}
private void printInit() {
--
GitLab