diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java index a8c4e42ff931a342cf2aad6a02fb3651e56b149f..35782201000dd8db029749d1e9a04b24be1fd841 100644 --- a/src/main/java/de/tlc4b/tlc/TLCResults.java +++ b/src/main/java/de/tlc4b/tlc/TLCResults.java @@ -9,6 +9,7 @@ import tlc2.output.MP; import tlc2.output.Message; import tlc2.output.OutputCollector; import tlc2.tool.BuiltInOPs; +import tlc2.tool.TLCState; import tlc2.tool.TLCStateInfo; import tlc2.tool.ToolGlobals; @@ -179,13 +180,13 @@ public class TLCResults implements ToolGlobals { private void evalTrace() { List<TLCStateInfo> trace = OutputCollector.getTrace(); - TracePrinter printer = null; - if (!trace.isEmpty()) { - printer = new TracePrinter(trace, tlcOutputInfo); - } else if (OutputCollector.getInitialState() != null) { - printer = new TracePrinter(OutputCollector.getInitialState(), tlcOutputInfo); + TLCState initialState = OutputCollector.getInitialState(); + if (trace.isEmpty() && initialState != null) { + trace = Collections.singletonList(new TLCStateInfo(initialState)); } - if (printer != null) { + + if (!trace.isEmpty()) { + TracePrinter printer = new TracePrinter(trace, tlcOutputInfo); traceString = printer.getTrace().toString(); } } diff --git a/src/main/java/de/tlc4b/tlc/TracePrinter.java b/src/main/java/de/tlc4b/tlc/TracePrinter.java index c3dcfb943f86e3a099432b170a30237830e5f417..6e5fd3eb22f8e87fe234dd31ac78ec7c84c8e848 100644 --- a/src/main/java/de/tlc4b/tlc/TracePrinter.java +++ b/src/main/java/de/tlc4b/tlc/TracePrinter.java @@ -31,10 +31,6 @@ public class TracePrinter { this.trace = trace; this.tlcOutputInfo = tlcOutputInfo; - setup(); - } - - private void setup() { constants = new ArrayList<>(); variables = new ArrayList<>(); for (int i = 0; i < TLCState.vars.length; i++) { @@ -49,12 +45,6 @@ public class TracePrinter { evalTrace(); } - public TracePrinter(TLCState initialState, TLCOutputInfo tlcOutputInfo) { - this.initialState = initialState; - this.tlcOutputInfo = tlcOutputInfo; - setup(); - } - public StringBuilder getTrace() { return traceBuilder; }