From fa492c78c58f57b731b1d7ef141baeb617435535 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 18 Jul 2024 13:03:52 +0200
Subject: [PATCH] Adjust a few indents to simplify future merges
---
tlatools/src/tlc2/output/StatePrinter.java | 4 ++--
tlatools/src/tlc2/tool/AbstractChecker.java | 4 ++--
tlatools/src/tlc2/tool/ModelChecker.java | 8 ++++----
tlatools/src/tlc2/tool/TLCTrace.java | 8 ++++----
4 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/tlatools/src/tlc2/output/StatePrinter.java b/tlatools/src/tlc2/output/StatePrinter.java
index 295712ed3..b3a0ecad6 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 7ba4caea0..03ba61b2f 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 f5fe5a09d..5af9e893e 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 2f05a1842..39bafa533 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);
--
GitLab