add more tests for reals

src/test/java/de/tla2b/examples/MCTest.java

@@ -83,6 +83,12 @@ public class MCTest {
 		runModule(file);
 	}
 
+	@Test
+	public void testRealDefinition() throws Exception {
+		String file = "src/test/resources/MCTests/InvariantReals/RealInvariant.tla";
+		runModule(file);
+	}
+
 	@Test
 	public void testMacroTest() throws Exception {
 		String file = "src/test/resources/renamer/MacroTest/MacroTest.tla";

src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java

@@ -9,15 +9,29 @@ public class ModuleAndExpressionTest {
 
 	@Test
 	public void testCon() throws Exception {
-		String module = "---- MODULE Testing ----\n" + "CONSTANTS k \n"
-			+ "ASSUME k = 4" + "===============";
+		String module = "---- MODULE Testing ----\n"
+			+ "CONSTANTS k \n"
+			+ "ASSUME k = 4"
+			+ "===============";
 		compareExprIncludingModel("k = 1", "k = 1", module);
 	}
 
 	@Test(expected = TypeErrorException.class)
 	public void testTypeError() throws Exception {
-		String module = "---- MODULE Testing ----\n" + "CONSTANTS k \n"
-			+ "ASSUME k = 4" + "===============";
+		String module = "---- MODULE Testing ----\n"
+			+ "CONSTANTS k \n"
+			+ "ASSUME k = 4"
+			+ "===============";
 		compareExprIncludingModel(null, "k = TRUE", module);
 	}
+
+	@Test
+	public void testReals() throws Exception {
+		String module = "---- MODULE Testing ----\n"
+			+ "EXTENDS Reals\n"
+			+ "CONSTANTS k, t1, t2 \n"
+			+ "ASSUME k = 2.0 /\\ t1 = k*k /\\ t2 = (k < 5.0)"
+			+ "===============";
+		compareExprIncludingModel("t2 = TRUE", "t2 = TRUE", module);
+	}
 }

src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java

@@ -66,6 +66,23 @@ public class TestModuleReals {
 		TestUtil.typeCheckString(module);
 	}
 
+	@Test
+	public void testRelationalOperators() throws
+		TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Reals \n"
+			+ "CONSTANTS l, leq, g, geq \n"
+			+ "ASSUME l = (2.0 < 1.0) /\\ leq = (2.0 <= 1.0) /\\ g = (2.0 > 1.0) /\\ geq = (2.0 >= 1.0)\n"
+			+ "=================================";
+
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("BOOL", t.getConstantType("l"));
+		assertEquals("BOOL", t.getConstantType("leq"));
+		assertEquals("BOOL", t.getConstantType("g"));
+		assertEquals("BOOL", t.getConstantType("geq"));
+
+	}
+
 	@Test(expected = TypeErrorException.class)
 	public void testRelationalOperatorsException1() throws
 		TLA2BException {

src/test/resources/MCTests/InvariantReals/RealInvariant.cfg

+INIT
+Init
+NEXT
+Next
+INVARIANT
+Inv

src/test/resources/MCTests/InvariantReals/RealInvariant.tla

+--------------------------- MODULE RealInvariant ---------------------------
+EXTENDS Reals
+VARIABLES x,y
+Init == x = 1.0 /\ y = 2.0
+Next == x' = 2.0 /\ y' = 3.0
+TestExpression == x*x + y*y
+Inv == TestExpression <= 10.0
+
+============================================================================