Skip to content
Snippets Groups Projects
Commit 56f11f87 authored by dgelessus's avatar dgelessus
Browse files

Pass B2TLA-generated config file to TLA2B and adjust tests accordingly 

Needed for compatibility with newer versions of tla2bAST.
parent fb8f62a5
No related branches found
No related tags found
No related merge requests found
Pipeline #112160 passed
Stage: test
Stage: deploy
Show whitespace changes
Inline Side-by-side
src/test/java/de/tlc4b/analysis/DefinitionsTest.java
+ 1
− 1
View file @ 56f11f87
......@@ -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"
+ "======";
......
src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
+ 2
− 2
View file @ 56f11f87
......@@ -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"
......
src/test/java/de/tlc4b/prettyprint/OperationsTest.java
+ 22
− 17
View file @ 56f11f87
......@@ -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"
......
src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
+ 3
− 3
View file @ 56f11f87
......@@ -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"
+ "====";
......
src/test/java/de/tlc4b/util/TestUtil.java
+ 15
− 7
View file @ 56f11f87
......@@ -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)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment