diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java index d96e9a698b69661e96851c4637821fd428d14317..6d824ff568f4d7160d2a0443fb0db8e851dbd750 100644 --- a/src/main/java/de/tlc4b/tlc/TLCResults.java +++ b/src/main/java/de/tlc4b/tlc/TLCResults.java @@ -90,7 +90,6 @@ public class TLCResults { ArrayList<Message> messages = OutputCollector.getAllMessages(); for (Message m : messages) { - switch (m.getMessageClass()) { case ERROR: evalErrorMessage(m); @@ -147,11 +146,12 @@ public class TLCResults { } private void evalErrorMessage(Message m) { - // System.out.print(m.getMessageCode() + " "+ m.getParameters().length); - // for (int i = 0; i < m.getParameters().length; i++) { - // System.out.print(" "+m.getParameters()[i]); - // } - // System.out.println(); +// System.out.println(------------------); +// System.out.print(m.getMessageCode() + " " + m.getParameters().length); +// for (int i = 0; i < m.getParameters().length; i++) { +// System.out.print(" " + m.getParameters()[i]); +// } +// System.out.println(); switch (m.getMessageCode()) { case EC.TLC_INVARIANT_VIOLATED_INITIAL: case EC.TLC_INVARIANT_VIOLATED_BEHAVIOR: @@ -219,6 +219,8 @@ public class TLCResults { return InvariantViolation; } else if (s.contains("In applying the function")) { return WellDefinednessError; + } else if (s.contains("which is not in the domain of the function")) { + return WellDefinednessError; } else if (s.contains("tlc2.module.TLC.Assert")) { return tlcResult = WellDefinednessError; } else if (s diff --git a/src/test/java/de/tlc4b/prettyprint/FunctionsVsRelations.java b/src/test/java/de/tlc4b/prettyprint/FunctionsVsRelations.java new file mode 100644 index 0000000000000000000000000000000000000000..bf3ff72a179601711918c68251dae60da4ca7207 --- /dev/null +++ b/src/test/java/de/tlc4b/prettyprint/FunctionsVsRelations.java @@ -0,0 +1,20 @@ +package de.tlc4b.prettyprint; + +import static de.tlc4b.util.TestUtil.compare; + +import org.junit.Test; + +public class FunctionsVsRelations { + + @Test + public void testCardOnAFunction() throws Exception { + String machine = "MACHINE test\n" + + "PROPERTIES 1 = card(%x.(x = 1 | 1))\n" + + "END"; + String expected = "---- MODULE test----\n" + + "EXTENDS FiniteSets\n" + + "ASSUME 1 = Cardinality(DOMAIN([x \\in {1} |-> 1 ]))\n" + + "======"; + compare(expected, machine); + } +} diff --git a/src/test/java/de/tlc4b/typechecking/FunctionsVsRelations.java b/src/test/java/de/tlc4b/typechecking/FunctionsVsRelations.java new file mode 100644 index 0000000000000000000000000000000000000000..8e8780c92eae7a1c305b9a2e1cff571e1465d58f --- /dev/null +++ b/src/test/java/de/tlc4b/typechecking/FunctionsVsRelations.java @@ -0,0 +1,20 @@ +package de.tlc4b.typechecking; + +import static org.junit.Assert.assertEquals; + +import org.junit.Test; + +import de.be4.classicalb.core.parser.exceptions.BException; + +public class FunctionsVsRelations { + + @Test + public void testCardFunction() throws BException { + String machine = "MACHINE test\n" + + "CONSTANTS k \n" + + "PROPERTIES k = %x.(x : {1} | 1) & card(k) = 1 \n" + + "END"; + TestTypechecker t = new TestTypechecker(machine); + assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k").toString()); + } +} diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java index 41414861b9998ca2837c50f73f0956b7892eb3b6..a1556b7acb2697db747339451a224518e70342c7 100644 --- a/src/test/java/testing/Testing2.java +++ b/src/test/java/testing/Testing2.java @@ -29,9 +29,9 @@ public class Testing2 extends AbstractParseMachineTest { @Test public void testRunTLC() throws Exception { String[] a = new String[] { - machine.getPath()}; - TLC4B.main(a); - //TLC4B.test(a,false); + machine.getPath(), "-noLTL", "-wdcheck"}; + //TLC4B.main(a); + TLC4B.test(a,false); //test(a); } diff --git a/src/test/resources/basics/SubstitutionsTest.mch b/src/test/resources/basics/SubstitutionsTest.mch index 6703ea100127ecb59890c04cd716f69e4bda9bf1..919d8179c291cba40b304873150957b9221b681e 100644 --- a/src/test/resources/basics/SubstitutionsTest.mch +++ b/src/test/resources/basics/SubstitutionsTest.mch @@ -1,4 +1,4 @@ -MACHINE FunctionsTest +MACHINE SubstitutionsTest VARIABLES x INVARIANT x : 1..5 INITIALISATION x := 1