diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java index a6001eac014396c201478e6310c77784cef0e6e7..a32cac08b0e69e5bb2186b713f7646e777e5c58e 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 e1ff75d56932e5c2b3c34e46a7bfa7da31b94864..e5f97f15d7c04165a86c8f48404ff5d00a55a5af 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 4bf91aa304b91032e0dea1b5804351c5b2d3067d..a03c9a34f3111734c0b8277e924392f5f1a61a5a 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++) {