Make compareModuleAndConfig work properly and fix affected tests

src/test/java/de/tlc4b/analysis/DeferredSetSizeTest.java

@@ -12,8 +12,8 @@ public class DeferredSetSizeTest {
 				+ "END";
 		String expectedModule = "---- MODULE test ----\n"
 				+ "CONSTANTS S\n"
-				+ "======";
-		String expectedConfig = "CONSTANTS S = {S1, S2, S3} "; 
+				+ "====";
+		String expectedConfig = "CONSTANTS\nS = {S1,S2,S3}\n"; 
 		compareModuleAndConfig(expectedModule, expectedConfig, machine);
 	}
 	
@@ -27,8 +27,8 @@ public class DeferredSetSizeTest {
 				+ "EXTENDS FiniteSets\n"
 				+ "CONSTANTS S\n"
 				+ "ASSUME Cardinality(S) = 4\n"
-				+ "======";
-		String expectedConfig = "CONSTANTS S = {S1, S2, S3, S4} "; 
+				+ "====";
+		String expectedConfig = "CONSTANTS\nS = {S1,S2,S3,S4}\n"; 
 		compareModuleAndConfig(expectedModule, expectedConfig, machine);
 	}
 	
@@ -42,8 +42,8 @@ public class DeferredSetSizeTest {
 				+ "EXTENDS FiniteSets\n"
 				+ "CONSTANTS S\n"
 				+ "ASSUME 4 = Cardinality(S)\n"
-				+ "======";
-		String expectedConfig = "CONSTANTS S = {S1, S2, S3, S4} "; 
+				+ "====";
+		String expectedConfig = "CONSTANTS\nS = {S1,S2,S3,S4}\n"; 
 		compareModuleAndConfig(expectedModule, expectedConfig, machine);
 	}
 }

src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java

@@ -27,9 +27,10 @@ public class MachineParameterTest {
 		String expectedModule = "---- MODULE test ----\n"
 				+ "VARIABLES a\n"
 				+ "Init == a \\in {1, 2, 3}\n"
+				+ "\n"
 				+ "Next == 1 = 2 /\\ UNCHANGED <<a>>\n"
-				+ "======";
-		String expectedConfig = "INIT Init\nNEXT Next";
+				+ "====";
+		String expectedConfig = "INIT Init\nNEXT Next\n";
 		compareModuleAndConfig(expectedModule, expectedConfig, machine);
 	}
 	
@@ -53,8 +54,8 @@ public class MachineParameterTest {
 		
 		String expectedModule = "---- MODULE test ----\n"
 				+ "CONSTANTS AA\n"
-				+ "======";
-		String expectedConfig = "CONSTANTS AA = {AA1, AA2, AA3}";
+				+ "====";
+		String expectedConfig = "CONSTANTS\nAA = {AA1,AA2,AA3}\n";
 		compareModuleAndConfig(expectedModule, expectedConfig, machine);
 	}
 	
@@ -69,7 +70,7 @@ public class MachineParameterTest {
 				+ "a == 1\n"
 				+ "ASSUME Cardinality(B) = 2\n"
 				+ "====";
-		String expectedConfig = "CONSTANTS B = {B1, B2, B3}";
+		String expectedConfig = "CONSTANTS\nB = {B1,B2,B3}\n";
 		compareModuleAndConfig(expectedModule, expectedConfig, machine);
 	}
 	

src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java

@@ -12,7 +12,7 @@ public class SetsClauseTest {
 				+ "END";
 		String expectedModule = "---- MODULE test ----\n"
 				+ "CONSTANTS d\n"
-				+ "======";
+				+ "====";
 		String expectedConfig = "CONSTANTS\n" +
 				"d = {d1,d2,d3}\n";
 
@@ -27,10 +27,16 @@ public class SetsClauseTest {
 				+ "PROPERTIES k : d \n"
 				+ "END";
 		String expectedModule = "---- MODULE test ----\n"
-				+ "CONSTANTS d2asisdfapsdjfa\n"
-				+ "======";
-		String expectedConfig = "CONSTANTS\n" +
-				"d = {d1, d2, d3}\n";
+				+ "CONSTANTS d\n"
+				+ "VARIABLES k\n"
+				+ "Init == k \\in d\n"
+				+ "\n"
+				+ "Next == 1 = 2 /\\ UNCHANGED <<k>>\n"
+				+ "====";
+		String expectedConfig = "INIT Init\n"
+				+ "NEXT Next\n"
+				+ "CONSTANTS\n"
+				+ "d = {d1,d2,d3}\n";
 
 		compareModuleAndConfig(expectedModule, expectedConfig, machine);
 	}
@@ -42,9 +48,9 @@ public class SetsClauseTest {
 				+ "END";
 		String expectedModule = "---- MODULE test ----\n"
 				+ "CONSTANTS a, b, c\n"
-				+ "S == {a, b, c}"
-				+ "======";
-		String expectedConfig = "CONSTANTS a = a\n b = b \n c = c"; 
+				+ "S == {a, b, c}\n"
+				+ "====";
+		String expectedConfig = "CONSTANTS\na = a\nb = b\nc = c\n"; 
 		compareModuleAndConfig(expectedModule, expectedConfig, machine);
 	}
 }

src/test/java/de/tlc4b/util/TestUtil.java

@@ -113,6 +113,7 @@ public class TestUtil {
 
 		String name = b2tlaTranslator.getMachineName();
 		translateTLA2B(name, b2tlaTranslator.getModuleString(), b2tlaTranslator.getConfigString());
+		// TODO Check that re-translated B machine matches original input?
 	}
 
 	public static void compareEqualsConfig(String expectedModule, String expectedConfig, String machine)
@@ -124,30 +125,14 @@ public class TestUtil {
 
 		// parse check
 		translateTLA2B(name, b2tlaTranslator.getModuleString(), b2tlaTranslator.getConfigString());
+		// TODO Check that re-translated B machine matches original input?
 
 		assertEquals(expectedModule, b2tlaTranslator.getModuleString());
 		assertEquals(expectedConfig, b2tlaTranslator.getConfigString());
 	}
 
-	public static void compareModuleAndConfig(String expectedModule, String expectedConfig, String machine)
-		throws BCompoundException, TLA2BException {
-		Translator b2tlaTranslator = new Translator(machine);
-		b2tlaTranslator.translate();
-
-		// TODO include config file in back translation from TLA+ to B
-
-		// String name = b2tlaTranslator.getMachineName();
-		// StringBuilder sb1 = de.tla2b.translation.Tla2BTranslator
-		// .translateString(name, b2tlaTranslator.getModuleString(),
-		// b2tlaTranslator.getConfigString());
-		// StringBuilder sb2 = de.tla2b.translation.Tla2BTranslator
-		// .translateString(name, expectedModule, expectedConfig);
-		// if (!sb2.toString().equals(sb1.toString())) {
-		// fail("expected:\n" + expectedModule + "\nbut was:\n"
-		// + b2tlaTranslator.getModuleString() + "\n\nexpected:\n"
-		// + expectedConfig + "\nbut was:\n"
-		// + b2tlaTranslator.getConfigString());
-		// }
+	public static void compareModuleAndConfig(String expectedModule, String expectedConfig, String machine) throws Exception {
+		compareEqualsConfig(expectedModule, expectedConfig, machine);
 	}
 
 	public static void compareEquals(String expected, String machine) throws BException {