From 3f21e26b7f7dc3e45be25e9ef1dc34930d3ae274 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 12 Dec 2014 16:45:08 +0100
Subject: [PATCH] fixed bug in trace printer
---
src/main/java/de/tlc4b/TLC4B.java | 6 +--
src/main/java/de/tlc4b/TLCRunner.java | 3 --
src/main/java/de/tlc4b/tlc/TracePrinter.java | 51 +++++++++++---------
3 files changed, 30 insertions(+), 30 deletions(-)
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index a6001ea..a32cac0 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -72,11 +72,6 @@ public class TLC4B {
private void printResults(TLCResults results, boolean createTraceFile) {
- String s = "";
- for (int i = 0; i < 10; i++) {
- s += i;
- }
-
System.out.println("Parsing time: " + StopWatch.getRunTime("Parsing")
+ " ms");
System.out.println("Translation time: " + StopWatch.getRunTime("Pure")
@@ -89,6 +84,7 @@ public class TLC4B {
+ results.getNumberOfTransitions());
System.out.println("Result: " + results.getResultString());
+
if (results.hasTrace() && createTraceFile) {
String trace = results.getTrace();
String tracefileName = machineFileNameWithoutFileExtension
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index e1ff75d..e5f97f1 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -99,11 +99,9 @@ public class TLCRunner {
//list.add("-config");
//list.add(machineName + ".cfg");
list.add(machineName);
- System.out.println(path.getPath());
ToolIO.setUserDir(path.getPath());
String[] args = list.toArray(new String[list.size()]);
TLC tlc = new TLC();
-
// handle parameters
if (tlc.handleParameters(args)) {
tlc.setResolver(new SimpleFilenameToStream());
@@ -112,7 +110,6 @@ public class TLCRunner {
tlc.process();
} catch (Exception e) {
}
-
}
// System.setOut(systemOut);
// ArrayList<String> messages = btlcStream.getArrayList();
diff --git a/src/main/java/de/tlc4b/tlc/TracePrinter.java b/src/main/java/de/tlc4b/tlc/TracePrinter.java
index 4bf91aa..a03c9a3 100644
--- a/src/main/java/de/tlc4b/tlc/TracePrinter.java
+++ b/src/main/java/de/tlc4b/tlc/TracePrinter.java
@@ -30,6 +30,7 @@ import tlc2.value.SubsetValue;
import tlc2.value.TupleValue;
import tlc2.value.UnionValue;
import tlc2.value.Value;
+import tlc2.value.ValueEnumeration;
import tlc2.value.ValueVec;
import util.UniqueString;
import static tlc2.value.ValueConstants.*;
@@ -172,13 +173,12 @@ public class TracePrinter {
res.append(")");
return res;
} else if (type instanceof FunctionType) {
- if(((TupleValue) val).elems.length == 0){
+ if (((TupleValue) val).elems.length == 0) {
res.append("{}");
return res;
- }else{
+ } else {
BType subtype = ((FunctionType) type).getRange();
res.append("[");
- System.out.println();
res.append(parseEnumerationValue(((TupleValue) val).elems,
subtype));
res.append("]");
@@ -225,7 +225,7 @@ public class TracePrinter {
case MODELVALUE:
ModelValue modelValue = (ModelValue) val;
String bName = tlcOutputInfo.getBName(modelValue.toString());
- if(bName == null){
+ if (bName == null) {
bName = modelValue.toString();
}
res.append(bName);
@@ -233,35 +233,25 @@ public class TracePrinter {
case SETOFTUPLESVALUE: {
SetOfTuplesValue s = (SetOfTuplesValue) val;
- SetType t = (SetType) type;
- PairType pair = (PairType) t.getSubtype();
- res.append(parseValue(s.sets[0], new SetType(pair.getFirst())));
- res.append("*");
- res.append(parseValue(s.sets[1], new SetType(pair.getSecond())));
- return res;
+ ValueEnumeration e = s.elements();
+ return parseSetValue(res, s.size(), type, e);
}
case SETCUPVALUE: {
SetCupValue s = (SetCupValue) val;
- res.append(parseValue(s.set1, type));
- res.append("\\/");
- res.append(parseValue(s.set2, type));
- return res;
+ ValueEnumeration e = s.elements();
+ return parseSetValue(res, s.size(), type, e);
}
case SETCAPVALUE: {
SetCapValue s = (SetCapValue) val;
- res.append(parseValue(s.set1, type));
- res.append("/\\");
- res.append(parseValue(s.set2, type));
- return res;
+ ValueEnumeration e = s.elements();
+ return parseSetValue(res, s.size(), type, e);
}
case SETDIFFVALUE: {
SetDiffValue s = (SetDiffValue) val;
- res.append(parseValue(s.set1, type));
- res.append("-");
- res.append(parseValue(s.set2, type));
- return res;
+ ValueEnumeration e = s.elements();
+ return parseSetValue(res, s.size(), type, e);
}
case SUBSETVALUE: {
@@ -338,6 +328,23 @@ public class TracePrinter {
throw new RuntimeException("not supported construct: " + val);
}
+ private StringBuilder parseSetValue(StringBuilder res, int size,
+ BType type, ValueEnumeration e) {
+ SetType t = (SetType) type;
+ res.append("{");
+ for (int i = 0; i < size; i++) {
+ Value v = e.nextElement();
+ if (i != 0) {
+ res.append(", ");
+ }
+ if (v != null) {
+ res.append(parseValue(v, t.getSubtype()));
+ }
+ }
+ res.append("}");
+ return res;
+ }
+
private StringBuilder parseValueVec(ValueVec elems, BType bType) {
StringBuilder res = new StringBuilder();
for (int i = 0; i < elems.size(); i++) {
--
GitLab