diff --git a/src/test/java/de/tlc4b/analysis/DeferredSetSizeTest.java b/src/test/java/de/tlc4b/analysis/DeferredSetSizeTest.java
index ebd3193d910182cd768a353f6ae844507e5182fa..9ebb7d750c4cd4ca5f8ad793c002ae4cc98017f5 100644
--- a/src/test/java/de/tlc4b/analysis/DeferredSetSizeTest.java
+++ b/src/test/java/de/tlc4b/analysis/DeferredSetSizeTest.java
@@ -10,10 +10,10 @@ public class DeferredSetSizeTest {
String machine = "MACHINE test\n"
+ "SETS S \n"
+ "END";
- String expectedModule = "---- MODULE test----\n"
+ 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);
}
@@ -23,12 +23,12 @@ public class DeferredSetSizeTest {
+ "SETS S \n"
+ "PROPERTIES card(S) = 4"
+ "END";
- String expectedModule = "---- MODULE test----\n"
- + "EXTENDS FiniteSets \n"
+ String expectedModule = "---- MODULE test ----\n"
+ + "EXTENDS FiniteSets\n"
+ "CONSTANTS S\n"
- + "ASSUME Cardinality(S) = 4 \n"
- + "======";
- String expectedConfig = "CONSTANTS S = {S1, S2, S3, S4} ";
+ + "ASSUME Cardinality(S) = 4\n"
+ + "====";
+ String expectedConfig = "CONSTANTS\nS = {S1,S2,S3,S4}\n";
compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
@@ -38,12 +38,12 @@ public class DeferredSetSizeTest {
+ "SETS S \n"
+ "PROPERTIES 4 = card(S)"
+ "END";
- String expectedModule = "---- MODULE test----\n"
- + "EXTENDS FiniteSets \n"
+ String expectedModule = "---- MODULE test ----\n"
+ + "EXTENDS FiniteSets\n"
+ "CONSTANTS S\n"
- + "ASSUME 4 = Cardinality(S) \n"
- + "======";
- String expectedConfig = "CONSTANTS S = {S1, S2, S3, S4} ";
+ + "ASSUME 4 = Cardinality(S)\n"
+ + "====";
+ String expectedConfig = "CONSTANTS\nS = {S1,S2,S3,S4}\n";
compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
}
diff --git a/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java b/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
index 2ee04a8252b9371af16bb1eefc7bcc9580acb020..e6123946cee8bd4ca9b8eb8744fa9901ae3263d3 100644
--- a/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
@@ -24,12 +24,13 @@ public class MachineParameterTest {
+ "CONSTRAINTS a : {1,2,3}\n"
+ "END";
- String expectedModule = "---- MODULE test----\n"
+ String expectedModule = "---- MODULE test ----\n"
+ "VARIABLES a\n"
- + "Init == a \\in {1,2,3}\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);
}
@@ -51,10 +52,10 @@ public class MachineParameterTest {
String machine = "MACHINE test(AA)\n"
+ "END";
- String expectedModule = "---- MODULE test----\n"
+ 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);
}
diff --git a/src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java b/src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java
index 2d12db49152344912eb7f14fbd4edd2d8011fe23..ca6f87fcecb24523e763b636ba0ee235c9f4abfc 100644
--- a/src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java
@@ -10,11 +10,11 @@ public class SetsClauseTest {
String machine = "MACHINE test\n"
+ "SETS d \n"
+ "END";
- String expectedModule = "---- MODULE test----\n"
+ String expectedModule = "---- MODULE test ----\n"
+ "CONSTANTS d\n"
- + "======";
+ + "====";
String expectedConfig = "CONSTANTS\n" +
- "d = {d1, d2, d3}\n";
+ "d = {d1,d2,d3}\n";
compareModuleAndConfig(expectedModule, expectedConfig, machine);
}
@@ -26,11 +26,17 @@ public class SetsClauseTest {
+ "CONSTANTS k \n"
+ "PROPERTIES k : d \n"
+ "END";
- String expectedModule = "---- MODULE test----\n"
- + "CONSTANTS d2asisdfapsdjfa\n"
- + "======";
- String expectedConfig = "CONSTANTS\n" +
- "d = {d1, d2, d3}\n";
+ String expectedModule = "---- MODULE test ----\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);
}
@@ -40,11 +46,11 @@ public class SetsClauseTest {
String machine = "MACHINE test\n"
+ "SETS S = {a,b,c} \n"
+ "END";
- String expectedModule = "---- MODULE test----\n"
+ 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);
}
}
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 02c8ea03eafdb7aaa0806fb5f0a40df8175766da..f0da9dd2a1c4e5c8df87e62a4d0dd0533d9c8ee1 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/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 {