Skip to content
Snippets Groups Projects
Commit 9af0b656 authored by hansen's avatar hansen
Browse files

updated result print

parent 26006bdf
No related branches found
No related tags found
No related merge requests found
...@@ -10,6 +10,7 @@ import java.io.InputStream; ...@@ -10,6 +10,7 @@ import java.io.InputStream;
import java.io.OutputStreamWriter; import java.io.OutputStreamWriter;
import java.io.UnsupportedEncodingException; import java.io.UnsupportedEncodingException;
import tlc2.TLCGlobals;
import de.be4.classicalb.core.parser.exceptions.BException; import de.be4.classicalb.core.parser.exceptions.BException;
import de.tlc4b.TLC4BGlobals; import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES; import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
...@@ -78,6 +79,8 @@ public class TLC4B { ...@@ -78,6 +79,8 @@ public class TLC4B {
+ " ms"); + " ms");
System.out.println("Model checking time: " System.out.println("Model checking time: "
+ results.getModelCheckingTime() + " sec"); + results.getModelCheckingTime() + " sec");
System.out.println("Number of workers: "
+ TLCGlobals.getNumWorkers());
System.out.println("States analysed: " System.out.println("States analysed: "
+ results.getNumberOfDistinctStates()); + results.getNumberOfDistinctStates());
System.out.println("Transitions fired: " System.out.println("Transitions fired: "
...@@ -221,6 +224,14 @@ public class TLC4B { ...@@ -221,6 +224,14 @@ public class TLC4B {
public void progress(String[] args) throws IOException, BException { public void progress(String[] args) throws IOException, BException {
handleParameter(args); 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(); handleMainFileName();
if (TLC4BGlobals.isTranslate()) { if (TLC4BGlobals.isTranslate()) {
StopWatch.start("Parsing"); StopWatch.start("Parsing");
......
...@@ -47,6 +47,7 @@ public class TLC4BGlobals { ...@@ -47,6 +47,7 @@ public class TLC4BGlobals {
checkAssertion = true; checkAssertion = true;
checkLTL = true; checkLTL = true;
checkWD= false; checkWD= false;
partialInvariantEvaluation = false;
setForceTLCToEvalConstants(true); setForceTLCToEvalConstants(true);
...@@ -69,7 +70,7 @@ public class TLC4BGlobals { ...@@ -69,7 +70,7 @@ public class TLC4BGlobals {
testingMode = false; testingMode = false;
createTraceFile = true; createTraceFile = true;
partialInvariantEvaluation = false;
} }
public static boolean isCreateTraceFile() { public static boolean isCreateTraceFile() {
......
...@@ -237,7 +237,7 @@ public class TLAPrinter extends DepthFirstAdapter { ...@@ -237,7 +237,7 @@ public class TLAPrinter extends DepthFirstAdapter {
} }
if (TLC4BGlobals.isPartialInvariantEvaluation()) { if (TLC4BGlobals.isPartialInvariantEvaluation()) {
configFileString.append("CONSTANTS\n"); configFileString.append("CONSTANTS\n");
configFileString.append("Init1 = Init1\n"); configFileString.append("Init_action = Init_action\n");
ArrayList<POperation> operations = tlaModule.getOperations(); ArrayList<POperation> operations = tlaModule.getOperations();
StringBuilder sb = new StringBuilder(); StringBuilder sb = new StringBuilder();
...@@ -245,17 +245,15 @@ public class TLAPrinter extends DepthFirstAdapter { ...@@ -245,17 +245,15 @@ public class TLAPrinter extends DepthFirstAdapter {
for (int i = 0; i < operations.size(); i++) { for (int i = 0; i < operations.size(); i++) {
AOperation node = (AOperation) operations.get(i); AOperation node = (AOperation) operations.get(i);
String name = renamer.getNameOfRef(node); String name = renamer.getNameOfRef(node);
configFileString.append(name + "1 = "); configFileString.append(name + "_action = ");
configFileString.append(name + "1"); configFileString.append(name + "_action");
configFileString.append("\n"); configFileString.append("\n");
sb.append(name + "1"); sb.append(name + "_action");
if (i < operations.size() - 1) { if (i < operations.size() - 1) {
sb.append(", "); sb.append(", ");
} }
} }
sb.append("}"); sb.append("}");
configFileString.append("OpSet = ");
configFileString.append(sb);
configFileString.append("\n"); configFileString.append("\n");
configFileString.append("VIEW myView"); configFileString.append("VIEW myView");
} }
...@@ -320,11 +318,11 @@ public class TLAPrinter extends DepthFirstAdapter { ...@@ -320,11 +318,11 @@ public class TLAPrinter extends DepthFirstAdapter {
private void printConstants() { private void printConstants() {
if (TLC4BGlobals.isPartialInvariantEvaluation()) { if (TLC4BGlobals.isPartialInvariantEvaluation()) {
ArrayList<POperation> operations = tlaModule.getOperations(); ArrayList<POperation> operations = tlaModule.getOperations();
tlaModuleString.append("CONSTANTS OpSet, Init1, "); tlaModuleString.append("CONSTANTS Init_action, ");
for (int i = 0; i < operations.size(); i++) { for (int i = 0; i < operations.size(); i++) {
AOperation node = (AOperation) operations.get(i); AOperation node = (AOperation) operations.get(i);
String name = renamer.getNameOfRef(node); String name = renamer.getNameOfRef(node);
tlaModuleString.append(name + "1"); tlaModuleString.append(name + "_action");
if (i < operations.size() - 1) if (i < operations.size() - 1)
tlaModuleString.append(", "); tlaModuleString.append(", ");
...@@ -372,7 +370,7 @@ public class TLAPrinter extends DepthFirstAdapter { ...@@ -372,7 +370,7 @@ public class TLAPrinter extends DepthFirstAdapter {
} }
if (TLC4BGlobals.isPartialInvariantEvaluation()) { if (TLC4BGlobals.isPartialInvariantEvaluation()) {
tlaModuleString.append(", lastOp"); tlaModuleString.append(", last_action");
} }
tlaModuleString.append("\n"); tlaModuleString.append("\n");
...@@ -396,12 +394,12 @@ public class TLAPrinter extends DepthFirstAdapter { ...@@ -396,12 +394,12 @@ public class TLAPrinter extends DepthFirstAdapter {
ArrayList<Node> operations = invariantPreservationAnalysis ArrayList<Node> operations = invariantPreservationAnalysis
.getPreservingOperations(inv); .getPreservingOperations(inv);
if (operations.size() > 0) { if (operations.size() > 0) {
tlaModuleString.append("lastOp \\in {"); tlaModuleString.append("last_action \\in {");
for (int j = 0; j < operations.size(); j++) { for (int j = 0; j < operations.size(); j++) {
Node op = operations.get(j); Node op = operations.get(j);
String name = renamer.getNameOfRef(op); String name = renamer.getNameOfRef(op);
tlaModuleString.append(name); tlaModuleString.append(name);
tlaModuleString.append("1"); tlaModuleString.append("_action");
if (j < operations.size() - 1) { if (j < operations.size() - 1) {
tlaModuleString.append(", "); tlaModuleString.append(", ");
} }
...@@ -444,7 +442,7 @@ public class TLAPrinter extends DepthFirstAdapter { ...@@ -444,7 +442,7 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(")"); tlaModuleString.append(")");
} }
if (TLC4BGlobals.isPartialInvariantEvaluation()) { if (TLC4BGlobals.isPartialInvariantEvaluation()) {
tlaModuleString.append(" /\\ lastOp = Init1 "); tlaModuleString.append(" /\\ last_action = Init_action");
} }
if (i < inits.size() - 1) if (i < inits.size() - 1)
tlaModuleString.append("\n\t/\\ "); tlaModuleString.append("\n\t/\\ ");
...@@ -1047,9 +1045,9 @@ public class TLAPrinter extends DepthFirstAdapter { ...@@ -1047,9 +1045,9 @@ public class TLAPrinter extends DepthFirstAdapter {
printUnchangedConstants(); printUnchangedConstants();
if (TLC4BGlobals.isPartialInvariantEvaluation()) { if (TLC4BGlobals.isPartialInvariantEvaluation()) {
tlaModuleString.append(" /\\ lastOp' = "); tlaModuleString.append(" /\\ last_action' = ");
tlaModuleString.append(name); tlaModuleString.append(name);
tlaModuleString.append("1"); tlaModuleString.append("_action");
} }
tlaModuleString.append("\n\n"); tlaModuleString.append("\n\n");
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment