refactoring

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 {
 

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);

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) {

src/main/java/de/tlc4b/analysis/Ast2String.java → src/main/java/de/tlc4b/util/Ast2String.java

-package de.tlc4b.analysis;
+package de.tlc4b.util;
 
 import de.be4.classicalb.core.parser.analysis.ExtendedDFAdapter;
 import de.be4.classicalb.core.parser.node.Node;

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);

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 {
 

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 {

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 {