Detecting WD errors related to functions calls.

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,6 +146,7 @@ public class TLCResults {
 	}
 
 	private void evalErrorMessage(Message m) {
+//		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]);
@@ -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

src/test/java/de/tlc4b/prettyprint/FunctionsVsRelations.java

+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);
+	}
+}

src/test/java/de/tlc4b/typechecking/FunctionsVsRelations.java

+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());
+	}
+}

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);
 	}
 

src/test/resources/basics/SubstitutionsTest.mch

-MACHINE FunctionsTest
+MACHINE SubstitutionsTest
 VARIABLES x
 INVARIANT x : 1..5
 INITIALISATION x := 1