diff --git a/tlatools/src/tlc2/output/StatePrinter.java b/tlatools/src/tlc2/output/StatePrinter.java index 295712ed3aadcc0e6547c898dc2e6e2ca41bcd51..b3a0ecad6f1c4429c447a088ed0a709bfdc00be9 100644 --- a/tlatools/src/tlc2/output/StatePrinter.java +++ b/tlatools/src/tlc2/output/StatePrinter.java @@ -62,8 +62,8 @@ public class StatePrinter stateString = currentStateInfo.state.toString(); } MP.printState(EC.TLC_STATE_PRINT2, new String[] { String.valueOf(num), currentStateInfo.info.toString(), - stateString }, currentStateInfo, num); - OutputCollector.addStateToTrace(currentStateInfo); + stateString }, currentStateInfo, num); + OutputCollector.addStateToTrace(currentStateInfo); } /** diff --git a/tlatools/src/tlc2/tool/AbstractChecker.java b/tlatools/src/tlc2/tool/AbstractChecker.java index 7ba4caea0207d961d797c682c1ec44380db506f1..03ba61b2f8deed40b5e9da13bfc2be121029b8c4 100644 --- a/tlatools/src/tlc2/tool/AbstractChecker.java +++ b/tlatools/src/tlc2/tool/AbstractChecker.java @@ -77,12 +77,12 @@ public abstract class AbstractChecker implements Cancelable specFile = specFile.substring(lastSep + 1); this.tool = new Tool(specDir, specFile, configFile, resolver); - + this.specObj = this.tool.init(preprocess, spec); this.checkLiveness = !this.tool.livenessIsTrue(); OutputCollector.setModuleNode(this.tool.rootModule); - + // moved to file utilities this.metadir = FileUtil.makeMetaDir(specDir, fromChkpt); diff --git a/tlatools/src/tlc2/tool/ModelChecker.java b/tlatools/src/tlc2/tool/ModelChecker.java index f5fe5a09d3c13b1e142579adc5549f9a0c02ee67..5af9e893e274d91863be03c6b3ca3e8d697ca1b7 100644 --- a/tlatools/src/tlc2/tool/ModelChecker.java +++ b/tlatools/src/tlc2/tool/ModelChecker.java @@ -274,7 +274,7 @@ public class ModelChecker extends AbstractChecker { if ((!isAxiom[i]) && !this.tool.isValid(assumps[i])) { - OutputCollector.addViolatedAssumption(assumps[i]); + OutputCollector.addViolatedAssumption(assumps[i]); MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString()); //return false; assumptionsAreTRUE = false; @@ -282,7 +282,7 @@ public class ModelChecker extends AbstractChecker } catch (Exception e) { // Assert.printStack(e); - OutputCollector.addViolatedAssumption(assumps[i]); + OutputCollector.addViolatedAssumption(assumps[i]); MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR, new String[] { assumps[i].toString(), e.getMessage() }); //return false; @@ -353,9 +353,9 @@ public class ModelChecker extends AbstractChecker if (!this.tool.isValid(this.invariants[j], curState)) { // We get here because of invariant violation: - MP.printError(EC.TLC_INVARIANT_VIOLATED_INITIAL, new String[] { + MP.printError(EC.TLC_INVARIANT_VIOLATED_INITIAL, new String[] { this.tool.getInvNames()[j].toString(), curState.toString() }); - if (!TLCGlobals.continuation) + if (!TLCGlobals.continuation) return false; } } diff --git a/tlatools/src/tlc2/tool/TLCTrace.java b/tlatools/src/tlc2/tool/TLCTrace.java index 2f05a1842eacd7b43192850e3295b70367a8b315..39bafa533e36eb36b3310ed8365b6d5786be0a36 100644 --- a/tlatools/src/tlc2/tool/TLCTrace.java +++ b/tlatools/src/tlc2/tool/TLCTrace.java @@ -263,9 +263,9 @@ public class TLCTrace { public synchronized final void printTrace(final TLCState s1, final TLCState s2) throws IOException, WorkerException { - ArrayList<TLCStateInfo> trace = new ArrayList<TLCStateInfo>(); // collecting the whole error trace - - MP.printError(EC.TLC_BEHAVIOR_UP_TO_THIS_POINT); + ArrayList<TLCStateInfo> trace = new ArrayList<TLCStateInfo>(); // collecting the whole error trace + + MP.printError(EC.TLC_BEHAVIOR_UP_TO_THIS_POINT); // Print the prefix leading to s1: long loc1 = s1.uid; TLCState lastState = null; @@ -309,7 +309,7 @@ public class TLCTrace { StatePrinter.printState(sinfo, lastState, ++idx); lastState = sinfo.state; trace.add(sinfo); - + // Print s2: if (s2 != null) { sinfo = this.tool.getState(s2, s1);