diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java index 551ec40a2b0cf324584848d61bc140cfbcb7ab8d..369207fb8d56c19196f5c6a38dc186e5eb81b7bc 100644 --- a/src/main/java/de/tlc4b/Translator.java +++ b/src/main/java/de/tlc4b/Translator.java @@ -9,7 +9,6 @@ import de.be4.classicalb.core.parser.exceptions.BException; import de.be4.classicalb.core.parser.node.APredicateParseUnit; import de.be4.classicalb.core.parser.node.PPredicate; import de.be4.classicalb.core.parser.node.Start; -import de.tlc4b.analysis.Ast2String; import de.tlc4b.analysis.ConstantsEliminator; import de.tlc4b.analysis.ConstantsEvaluator; import de.tlc4b.analysis.DefinitionsAnalyser; @@ -27,6 +26,7 @@ import de.tlc4b.analysis.unchangedvariables.UnchangedVariablesFinder; import de.tlc4b.prettyprint.TLAPrinter; import de.tlc4b.tla.Generator; import de.tlc4b.tlc.TLCOutputInfo; +import de.tlc4b.util.Ast2String; public class Translator { diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java index 53f6f16d2767760396bea09d9f721e51b8f36366..ea233f40711cedbeb70307370a267f199ffaa39f 100644 --- a/src/main/java/de/tlc4b/analysis/Typechecker.java +++ b/src/main/java/de/tlc4b/analysis/Typechecker.java @@ -82,9 +82,6 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { node.getPredicate().apply(this); } - public MachineContext getContext() { - return machineContext; - } public void setType(Node node, BType t) { this.types.put(node, t); diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java index 9c2a523e1b5d2b5352d6c0720a4fc91480d8ff15..98202ddf7cdff9751a7f792c52b8156099022b21 100644 --- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java +++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java @@ -351,7 +351,9 @@ public class TLAPrinter extends DepthFirstAdapter { ArrayList<Node> inits = this.tlaModule.getInitPredicates(); if (inits.size() == 0) return; - tlaModuleString.append("Init ==\n\t/\\ "); + tlaModuleString.append("Init == "); + if(inits.size() > 1) + tlaModuleString.append("\n\t/\\ "); for (int i = 0; i < inits.size(); i++) { Node init = inits.get(i); if (init instanceof ADisjunctPredicate) { diff --git a/src/main/java/de/tlc4b/analysis/Ast2String.java b/src/main/java/de/tlc4b/util/Ast2String.java similarity index 93% rename from src/main/java/de/tlc4b/analysis/Ast2String.java rename to src/main/java/de/tlc4b/util/Ast2String.java index 2802949b6d20c204e8f1b3a24611a6d7c78bcf68..b0007b4d6384316225a7f33604a0332ad3018ede 100644 --- a/src/main/java/de/tlc4b/analysis/Ast2String.java +++ b/src/main/java/de/tlc4b/util/Ast2String.java @@ -1,4 +1,4 @@ -package de.tlc4b.analysis; +package de.tlc4b.util; import de.be4.classicalb.core.parser.analysis.ExtendedDFAdapter; import de.be4.classicalb.core.parser.node.Node; diff --git a/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java b/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java index 773a8674122c39c7d1223fc93b69c61dbe7adb85..e3d27dcbf84e7d3bca8e5315afb3008e150fbe4e 100644 --- a/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java +++ b/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java @@ -72,7 +72,7 @@ public class SubstitutionsTest { String expected = "---- MODULE test ----\n" + "VARIABLES x \n" + "Invariant1 == x = 1\n" - + "Init == \n/\\ 1 = 1 \n/\\ x = 1\n" + + "Init == 1 = 1 \n/\\ x = 1\n" + "Next == 1 = 2 /\\ UNCHANGED <<x>>\n" + "===="; compare(expected, machine); @@ -90,7 +90,7 @@ public class SubstitutionsTest { + "EXTENDS Naturals \n" + "VARIABLES x \n" + "Invariant1 == x = 1\n" - + "Init == \n/\\1 = 1 \n/\\ x = 1\n" + + "Init == 1 = 1 \n/\\ x = 1\n" + "Next == 1 = 2 /\\ UNCHANGED <<x>>\n" + "===="; compare(expected, machine); diff --git a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java index 959717968006db7169f6faf3242b8e8128403be8..1d3bcd8f09fbbfffd60395a9e406c6911ef7922f 100644 --- a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java +++ b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java @@ -5,10 +5,10 @@ import java.util.Hashtable; import de.be4.classicalb.core.parser.BParser; import de.be4.classicalb.core.parser.exceptions.BException; import de.be4.classicalb.core.parser.node.Start; -import de.tlc4b.analysis.Ast2String; import de.tlc4b.analysis.MachineContext; import de.tlc4b.analysis.Typechecker; import de.tlc4b.btypes.BType; +import de.tlc4b.util.Ast2String; public class TestTypechecker { diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java index 67628882818b08d4666e92a35845f821fd45fa88..607c7b8436faf90295352d91c43fc8febb01192c 100644 --- a/src/test/java/de/tlc4b/util/TestUtil.java +++ b/src/test/java/de/tlc4b/util/TestUtil.java @@ -21,7 +21,6 @@ import de.be4.classicalb.core.parser.exceptions.BException; import de.be4.classicalb.core.parser.node.Start; import de.tlc4b.TLC4BGlobals; import de.tlc4b.Translator; -import de.tlc4b.analysis.Ast2String; import de.tlc4b.tlc.TLCResults.TLCResult; public class TestUtil { diff --git a/src/test/java/testing/CompoundScopeTest.java b/src/test/java/testing/CompoundScopeTest.java index 97225f9625df1ac0c1b4159fa60313b8bf377290..efdb18bc76d2ad67395d4e764666bea68fad674c 100644 --- a/src/test/java/testing/CompoundScopeTest.java +++ b/src/test/java/testing/CompoundScopeTest.java @@ -14,13 +14,14 @@ import org.junit.Test; + import de.be4.classicalb.core.parser.BParser; import de.be4.classicalb.core.parser.analysis.pragma.Pragma; import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader; import de.be4.classicalb.core.parser.exceptions.BException; import de.be4.classicalb.core.parser.node.Start; -import de.tlc4b.analysis.Ast2String; import de.tlc4b.analysis.MachineContext; +import de.tlc4b.util.Ast2String; public class CompoundScopeTest {