From 7ad18f3e6ec413d42789ed3381900e7126c28183 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 21:39:05 +0200
Subject: [PATCH] Test exact whitespace in compareLTLFormula and fix
inconsistencies
---
src/main/java/de/tlc4b/prettyprint/TLAPrinter.java | 8 ++++----
src/test/java/de/tlc4b/ltl/LTLFormulaTest.java | 8 ++++----
src/test/java/de/tlc4b/util/TestUtil.java | 5 +----
3 files changed, 9 insertions(+), 12 deletions(-)
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 64da8fd..4d65051 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -147,7 +147,7 @@ public class TLAPrinter extends DepthFirstAdapter {
public void printStrongFairness(String s) {
moduleStringAppend(String
- .format("([]<><<%s>>_vars \\/ <>[]~ENABLED(%s) \\/ []<> ENABLED(%s /\\ ",
+ .format("([]<><<%s>>_vars \\/ <>[]~ENABLED(%s) \\/ []<>ENABLED(%s /\\ ",
s, s, s));
printVarsStuttering();
moduleStringAppend("))");
@@ -156,7 +156,7 @@ public class TLAPrinter extends DepthFirstAdapter {
public void printWeakFairness(String s) {
moduleStringAppend(String
- .format("([]<><<%s>>_vars \\/ []<>~ENABLED(%s) \\/ []<> ENABLED(%s /\\ ",
+ .format("([]<><<%s>>_vars \\/ []<>~ENABLED(%s) \\/ []<>ENABLED(%s /\\ ",
s, s, s));
printVarsStuttering();
moduleStringAppend("))");
@@ -168,9 +168,9 @@ public class TLAPrinter extends DepthFirstAdapter {
moduleStringAppend("([]<><<");
printOperationCall(operation);
- moduleStringAppend(">>_vars \\/ []<>~ENABLED(");
+ moduleStringAppend(">>_vars \\/ []<>~ENABLED(");
printOperationCall(operation);
- moduleStringAppend(") \\/ []<> ENABLED(");
+ moduleStringAppend(") \\/ []<>ENABLED(");
printOperationCall(operation);
moduleStringAppend(" /\\ ");
printVarsStuttering();
diff --git a/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java b/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java
index dc8ed94..ba07509 100644
--- a/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java
+++ b/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java
@@ -59,7 +59,7 @@ public class LTLFormulaTest {
@Test
public void testFinally() throws Exception {
String machine = "MACHINE test END";
- compareLTLFormula("<>(1=1)", machine, "F{1 = 1}");
+ compareLTLFormula("<>(1 = 1)", machine, "F{1 = 1}");
}
@Test
@@ -222,7 +222,7 @@ public class LTLFormulaTest {
+ "INITIALISATION x := 1\n"
+ "OPERATIONS foo = skip\n"
+ "END";
- String expected = "([]<><<foo>>_vars\\/[]<>~ENABLED(foo)\\/[]<>ENABLED(foo/\\x'=x))=>TRUE";
+ String expected = "([]<><<foo>>_vars \\/ []<>~ENABLED(foo) \\/ []<>ENABLED(foo /\\ x' = x)) => TRUE";
compareLTLFormula(expected, machine, "WF(foo) => true");
}
@@ -234,14 +234,14 @@ public class LTLFormulaTest {
+ "INITIALISATION x := 1\n"
+ "OPERATIONS foo = x := 1"
+ "END";
- String expected = "([]<><<foo>>_vars\\/<>[]~ENABLED(foo)\\/[]<>ENABLED(foo/\\x'=x))=>TRUE";
+ String expected = "([]<><<foo>>_vars \\/ <>[]~ENABLED(foo) \\/ []<>ENABLED(foo /\\ x' = x)) => TRUE";
compareLTLFormula(expected, machine, "SF(foo) => true");
}
@Test
public void testExistentialQuantification() throws Exception {
String machine = "MACHINE test END";
- compareLTLFormula(" \\E p \\in {1}: p = 1", machine, "#p.({p=1} & {p = 1})");
+ compareLTLFormula("\\E p \\in {1}: p = 1", machine, "#p.({p=1} & {p = 1})");
}
@Test
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index c8ca6a9..4028da3 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -87,10 +87,7 @@ public class TestUtil {
public static void compareLTLFormula(String expected, String machine, String ltlFormula) throws BCompoundException {
Translator b2tlaTranslator = new Translator(machine, ltlFormula);
b2tlaTranslator.translate();
- String translatedLTLFormula = b2tlaTranslator.getTranslatedLTLFormula();
- translatedLTLFormula = translatedLTLFormula.replaceAll("\\s", "");
- expected = expected.replaceAll("\\s", "");
- assertEquals(expected, translatedLTLFormula);
+ assertEquals(expected, b2tlaTranslator.getTranslatedLTLFormula());
}
public static void checkMachine(String machine) throws Exception {
--
GitLab