diff --git a/src/test/java/de/tlc4b/analysis/DefinitionsTest.java b/src/test/java/de/tlc4b/analysis/DefinitionsTest.java
index c2c1ceda0384aa1384b5d3eb4f45d6f60e2e9d58..8e70a7282161a8e1b4fb448ac29fbbe823402aea 100644
--- a/src/test/java/de/tlc4b/analysis/DefinitionsTest.java
+++ b/src/test/java/de/tlc4b/analysis/DefinitionsTest.java
@@ -66,7 +66,7 @@ public class DefinitionsTest {
+ "END";
String expected = "---- MODULE test----\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1\n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "======";
diff --git a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
index 46ffd2bfd81a9ef119bf710175115673db2c69fb..3c45ca730653f768412f8527cf4af98f26d9f83a 100644
--- a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
+++ b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
@@ -176,7 +176,7 @@ public class TypeRestrictionsTest {
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
+ "k == 1 .. 4\n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo(a) == x' = a\n"
+ "Next == \\E a \\in k: foo(a) \n"
@@ -234,7 +234,7 @@ public class TypeRestrictionsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo(a) == (a = a) /\\ x' = 3\n"
+ "Next == \\E a \\in {1} : foo(a) \n"
diff --git a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
index e9a6378c57b0147366336256206e2ed68bb0997e..ceafde9351a7f4a24630ca1797772793a840af86 100644
--- a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
@@ -67,7 +67,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
@@ -84,7 +84,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x, y \n"
- + "Invariant == x = 1 /\\ y = 1\n"
+ + "Invariant1 == x = 1\n"
+ + "Invariant2 == y = 1\n"
+ "Init == x \\in {1} /\\ y \\in {1} \n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x, y>>\n"
+ "====";
@@ -103,7 +104,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x, y \n"
- + "Invariant == x = 1 /\\ y = 1\n"
+ + "Invariant1 == x = 1\n"
+ + "Invariant2 == y = 1\n"
+ "Init == x \\in {1} /\\ y \\in {1}\n"
+ "foo == x' \\in {1} /\\ y' \\in {1}\n"
+ "Next == foo\n"
@@ -124,7 +126,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x, y \n"
- + "Invariant == x = 1 /\\ y = 1\n"
+ + "Invariant1 == x = 1\n"
+ + "Invariant2 == y = 1\n"
+ "Init == x \\in {1} /\\ y \\in {1} \n"
+ "foo == x' \\in {x + 1} /\\ UNCHANGED <<y>>\n"
+ "Next == foo\n"
@@ -144,7 +147,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo(p) == x' = p\n"
+ "Next == \\E p \\in {1} : foo(p)\n"
@@ -164,7 +167,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == \\E p \\in {1} : x' = p\n"
+ "Next == foo\n"
@@ -185,7 +188,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo(p) == \\E p2 \\in {1} : x' = p + p2\n"
+ "Next == \\E p \\in {1} : foo(p)\n"
@@ -205,7 +208,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == UNCHANGED <<x>>\n"
+ "Next == foo\n"
@@ -225,7 +228,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == 1 = 1 /\\ UNCHANGED <<x>>\n"
+ "Next == foo\n"
@@ -247,7 +250,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == x = 1 /\\ x' = x + 1\n"
+ "Next == foo \n"
@@ -268,7 +271,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo(a) == x' = a\n"
+ "Next == \\E a \\in {1}: foo(a) \n"
@@ -288,7 +291,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x \\in {1} \n"
+ "foo == x' \\in {2} \n"
+ "Next == foo\n"
@@ -308,7 +311,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == (IF 1 = 1 THEN x' = 1 ELSE UNCHANGED <<x>>)\n"
+ "Next == foo \n"
@@ -329,7 +332,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == (( ((x = 1) /\\ (x' = 1)) \\/ (x = 2 /\\ x' = 2)))\n"
+ "Next == foo \n"
@@ -351,7 +354,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x,y \n"
- + "Invariant == x = 1 /\\ y = 1\n"
+ + "Invariant1 == x = 1\n"
+ + "Invariant2 == y = 1\n"
+ "Init == x = 1 /\\ y = 1\n"
+ "foo == (( ((x = 1) /\\ (x' = 1)) \\/ (x = 2 /\\ UNCHANGED <<x>>)) /\\ UNCHANGED <<y>>)\n"
+ "Next == foo \n"
@@ -371,7 +375,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x, y \n"
- + "Invariant == x = 1 /\\ y = 1\n"
+ + "Invariant1 == x = 1\n"
+ + "Invariant2 == y = 1\n"
+ "Init == x = 1 /\\ y = 1\n"
+ "foo == x = 1 \n"
+ "/\\ (((x = 1 /\\ x' = 1) \\/ (x = 2 /\\ UNCHANGED <<x>>)) /\\ y' = 1)\n"
@@ -393,7 +398,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals\n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == TRUE /\\ UNCHANGED <<x>>\n"
+ "Next == foo \n"
diff --git a/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java b/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
index 9a4946dd4e9bf156d4695a560dd63a250b159dd9..3965d7d575b53aff3ae73d8e891f9b4ff9e27c55 100644
--- a/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
@@ -54,7 +54,7 @@ public class SubstitutionsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals \n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == \\E a \\in {1}, b \\in {2} : x = a + b \n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
@@ -107,7 +107,7 @@ public class SubstitutionsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals \n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == x \\in {1}\n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
@@ -125,7 +125,7 @@ public class SubstitutionsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals \n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
+ + "Invariant1 == x = 1\n"
+ "Init == (CASE 1 = 1 -> x = 1 [] 1 = 2 -> x = 2 [] OTHER -> x = 4)\n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 3d39315b01f14265a3f53dac9c2b360ed22d3557..765859b5fa4fc9507f268216c9a4d6164c127b4e 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -30,12 +30,24 @@ public class TestUtil {
Translator b2tlaTranslator = new Translator(machineString);
b2tlaTranslator.translate();
+ System.out.println("Input B machine:");
+ System.out.println(machineString);
+ System.out.println("Expected TLA+ module:");
+ System.out.println(expectedModule);
+ System.out.println("Translated TLA+ module:");
+ System.out.println(b2tlaTranslator.getModuleString());
// TODO create standard modules BBuildins
String moduleName = b2tlaTranslator.getMachineName();
- String actualB = de.tla2bAst.Translator.translateModuleString(moduleName, b2tlaTranslator.getModuleString(), null);
- String expectedB = de.tla2bAst.Translator.translateModuleString(moduleName, expectedModule, null);
+ String actualB = de.tla2bAst.Translator.translateModuleString(moduleName, b2tlaTranslator.getModuleString(), b2tlaTranslator.getConfigString());
+ String expectedB = de.tla2bAst.Translator.translateModuleString(moduleName, expectedModule, b2tlaTranslator.getConfigString());
+ if (!expectedB.equals(actualB)) {
+ System.out.println("Expected TLA+ module translated to B machine:");
+ System.out.println(expectedB);
+ System.out.println("Actual translated TLA+ module translated back to B machine:");
+ System.out.println(actualB);
+ }
assertEquals(expectedB, actualB);
}
@@ -52,10 +64,6 @@ public class TestUtil {
}
- public static String translateTLA2B(String moduleName, String tlaString) throws TLA2BException {
- return de.tla2bAst.Translator.translateModuleString(moduleName, tlaString, null);
- }
-
public static String translateTLA2B(String moduleName, String tlaString, String configString)
throws TLA2BException {
return de.tla2bAst.Translator.translateModuleString(moduleName, tlaString, configString);
@@ -75,7 +83,7 @@ public class TestUtil {
b2tlaTranslator.translate();
String name = b2tlaTranslator.getMachineName();
- translateTLA2B(name, b2tlaTranslator.getModuleString());
+ translateTLA2B(name, b2tlaTranslator.getModuleString(), b2tlaTranslator.getConfigString());
}
public static void compareEqualsConfig(String expectedModule, String expectedConfig, String machine)