From d0a4ff3c5484c9a0795010d2db0f92bea9fdb444 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 20:21:22 +0200
Subject: [PATCH] Make compareModuleAndConfig work properly and fix affected
tests
---
.../tlc4b/analysis/DeferredSetSizeTest.java | 26 ++++++++--------
.../prettyprint/MachineParameterTest.java | 17 ++++++-----
.../de/tlc4b/prettyprint/SetsClauseTest.java | 30 +++++++++++--------
src/test/java/de/tlc4b/util/TestUtil.java | 23 +++-----------
4 files changed, 44 insertions(+), 52 deletions(-)
diff --git a/src/test/java/de/tlc4b/analysis/DeferredSetSizeTest.java b/src/test/java/de/tlc4b/analysis/DeferredSetSizeTest.java
index ebd3193..9ebb7d7 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 2ee04a8..e612394 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 2d12db4..ca6f87f 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 02c8ea0..f0da9dd 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 {
--
GitLab