From 2e4ac20205b720f04a86c9c841a2182837ea7909 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 21:23:16 +0200
Subject: [PATCH] Replace TestUtil.compareEquals with .translate
---
src/test/java/de/tlc4b/analysis/RenamerTest.java | 7 ++++---
src/test/java/de/tlc4b/prettyprint/FunctionTest.java | 9 ++++-----
src/test/java/de/tlc4b/prettyprint/SetTest.java | 4 ++--
src/test/java/de/tlc4b/util/TestUtil.java | 6 ------
4 files changed, 10 insertions(+), 16 deletions(-)
diff --git a/src/test/java/de/tlc4b/analysis/RenamerTest.java b/src/test/java/de/tlc4b/analysis/RenamerTest.java
index 4150660..9a6bd6d 100644
--- a/src/test/java/de/tlc4b/analysis/RenamerTest.java
+++ b/src/test/java/de/tlc4b/analysis/RenamerTest.java
@@ -1,9 +1,10 @@
package de.tlc4b.analysis;
-import static de.tlc4b.util.TestUtil.*;
-
import org.junit.Test;
+import static de.tlc4b.util.TestUtil.*;
+import static org.junit.Assert.assertEquals;
+
public class RenamerTest {
@@ -104,7 +105,7 @@ public class RenamerTest {
+ "S == {aa}\n"
+ "ASSUME \\E aa_1 \\in {1} : TRUE\n"
+ "====";
- compareEquals(expected, machine);
+ assertEquals(expected, translate(machine));
}
}
diff --git a/src/test/java/de/tlc4b/prettyprint/FunctionTest.java b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
index f191f7b..f02da43 100644
--- a/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
@@ -1,10 +1,9 @@
package de.tlc4b.prettyprint;
-import static de.tlc4b.util.TestUtil.*;
-
import org.junit.Test;
-
+import static de.tlc4b.util.TestUtil.*;
+import static org.junit.Assert.assertEquals;
public class FunctionTest {
@@ -97,7 +96,7 @@ public class FunctionTest {
String expected = "---- MODULE test ----\n"
+ "ASSUME [{1} -> {1}] = [{1} -> {1}]\n"
+ "====";
- compareEquals(expected, machine);
+ assertEquals(expected, translate(machine));
}
@@ -109,7 +108,7 @@ public class FunctionTest {
+ "EXTENDS Functions\n"
+ "ASSUME {} = ParFunc({1, 2}, {1, 2})\n"
+ "====";
- compareEquals(expected, machine);
+ assertEquals(expected, translate(machine));
}
}
diff --git a/src/test/java/de/tlc4b/prettyprint/SetTest.java b/src/test/java/de/tlc4b/prettyprint/SetTest.java
index 8e66fcb..f08a95b 100644
--- a/src/test/java/de/tlc4b/prettyprint/SetTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/SetTest.java
@@ -190,7 +190,7 @@ public class SetTest {
+ "ASSUME UNION({{z}: z \\in {z \\in ({1, 2}): 1 = 1}}) = {1, 2}\n"
+ "====";
//TODO ERROR in TLA2B
- compareEquals(expected, machine);
+ assertEquals(expected, translate(machine));
}
@Test
@@ -201,7 +201,7 @@ public class SetTest {
+ "EXTENDS BBuiltIns\n"
+ "ASSUME Inter({{z}: z \\in {z \\in ({1, 2}): 1 = 1}}) = {}\n"
+ "====";
- compareEquals(expected, machine);
+ assertEquals(expected, translate(machine));
}
}
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 2a32472..c4eeec7 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -124,12 +124,6 @@ public class TestUtil {
// TODO Check that re-translated B machine matches original input?
}
- public static void compareEquals(String expected, String machine) throws BCompoundException {
- Translator b2tlaTranslator = new Translator(machine);
- b2tlaTranslator.translate();
- assertEquals(expected, b2tlaTranslator.getModuleString());
- }
-
public static String translate(String machine) throws BCompoundException {
Translator translator = new Translator(machine);
translator.translate();
--
GitLab