diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java index 64da8fd456397e7796aa4d4ed6afe723566b0ebb..4d6505118bea0c9d6a44346ec9d50d3898bd343e 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 dc8ed947e1dc8d491358748c378dee66f9e730ac..ba07509abca2fb6a49134057a96a061e73bbc634 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 c8ca6a921ed936e3dfdd93208412b86a989db0b0..4028da3ec65b08bca613174796415c16438ebe0b 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 {