From 9af0b656c34569707f39ae0b3230eb0c6b424541 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Tue, 3 Feb 2015 10:29:55 +0100
Subject: [PATCH] updated result print
---
src/main/java/de/tlc4b/TLC4B.java | 11 ++++++++
src/main/java/de/tlc4b/TLC4BGlobals.java | 3 ++-
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 26 +++++++++----------
3 files changed, 25 insertions(+), 15 deletions(-)
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 7404ea7..93a2294 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -10,6 +10,7 @@ import java.io.InputStream;
import java.io.OutputStreamWriter;
import java.io.UnsupportedEncodingException;
+import tlc2.TLCGlobals;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
@@ -78,6 +79,8 @@ public class TLC4B {
+ " ms");
System.out.println("Model checking time: "
+ results.getModelCheckingTime() + " sec");
+ System.out.println("Number of workers: "
+ + TLCGlobals.getNumWorkers());
System.out.println("States analysed: "
+ results.getNumberOfDistinctStates());
System.out.println("Transitions fired: "
@@ -221,6 +224,14 @@ public class TLC4B {
public void progress(String[] args) throws IOException, BException {
handleParameter(args);
+ System.out.print("Arguments: ");
+ for (int i = 0; i < args.length; i++) {
+ String string = args[i];
+ System.out.print(string);
+ 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 366232b..4e483c3 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -47,6 +47,7 @@ public class TLC4BGlobals {
checkAssertion = true;
checkLTL = true;
checkWD= false;
+ partialInvariantEvaluation = false;
setForceTLCToEvalConstants(true);
@@ -69,7 +70,7 @@ public class TLC4BGlobals {
testingMode = false;
createTraceFile = true;
- partialInvariantEvaluation = false;
+
}
public static boolean isCreateTraceFile() {
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index b77f668..ffedc49 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -237,7 +237,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
if (TLC4BGlobals.isPartialInvariantEvaluation()) {
configFileString.append("CONSTANTS\n");
- configFileString.append("Init1 = Init1\n");
+ configFileString.append("Init_action = Init_action\n");
ArrayList<POperation> operations = tlaModule.getOperations();
StringBuilder sb = new StringBuilder();
@@ -245,17 +245,15 @@ public class TLAPrinter extends DepthFirstAdapter {
for (int i = 0; i < operations.size(); i++) {
AOperation node = (AOperation) operations.get(i);
String name = renamer.getNameOfRef(node);
- configFileString.append(name + "1 = ");
- configFileString.append(name + "1");
+ configFileString.append(name + "_action = ");
+ configFileString.append(name + "_action");
configFileString.append("\n");
- sb.append(name + "1");
+ sb.append(name + "_action");
if (i < operations.size() - 1) {
sb.append(", ");
}
}
sb.append("}");
- configFileString.append("OpSet = ");
- configFileString.append(sb);
configFileString.append("\n");
configFileString.append("VIEW myView");
}
@@ -320,11 +318,11 @@ public class TLAPrinter extends DepthFirstAdapter {
private void printConstants() {
if (TLC4BGlobals.isPartialInvariantEvaluation()) {
ArrayList<POperation> operations = tlaModule.getOperations();
- tlaModuleString.append("CONSTANTS OpSet, Init1, ");
+ tlaModuleString.append("CONSTANTS Init_action, ");
for (int i = 0; i < operations.size(); i++) {
AOperation node = (AOperation) operations.get(i);
String name = renamer.getNameOfRef(node);
- tlaModuleString.append(name + "1");
+ tlaModuleString.append(name + "_action");
if (i < operations.size() - 1)
tlaModuleString.append(", ");
@@ -372,7 +370,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
if (TLC4BGlobals.isPartialInvariantEvaluation()) {
- tlaModuleString.append(", lastOp");
+ tlaModuleString.append(", last_action");
}
tlaModuleString.append("\n");
@@ -396,12 +394,12 @@ public class TLAPrinter extends DepthFirstAdapter {
ArrayList<Node> operations = invariantPreservationAnalysis
.getPreservingOperations(inv);
if (operations.size() > 0) {
- tlaModuleString.append("lastOp \\in {");
+ tlaModuleString.append("last_action \\in {");
for (int j = 0; j < operations.size(); j++) {
Node op = operations.get(j);
String name = renamer.getNameOfRef(op);
tlaModuleString.append(name);
- tlaModuleString.append("1");
+ tlaModuleString.append("_action");
if (j < operations.size() - 1) {
tlaModuleString.append(", ");
}
@@ -444,7 +442,7 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(")");
}
if (TLC4BGlobals.isPartialInvariantEvaluation()) {
- tlaModuleString.append(" /\\ lastOp = Init1 ");
+ tlaModuleString.append(" /\\ last_action = Init_action");
}
if (i < inits.size() - 1)
tlaModuleString.append("\n\t/\\ ");
@@ -1047,9 +1045,9 @@ public class TLAPrinter extends DepthFirstAdapter {
printUnchangedConstants();
if (TLC4BGlobals.isPartialInvariantEvaluation()) {
- tlaModuleString.append(" /\\ lastOp' = ");
+ tlaModuleString.append(" /\\ last_action' = ");
tlaModuleString.append(name);
- tlaModuleString.append("1");
+ tlaModuleString.append("_action");
}
tlaModuleString.append("\n\n");
--
GitLab