diff --git a/src/test/java/de/tla2b/examples/MCTest.java b/src/test/java/de/tla2b/examples/MCTest.java index dd8032fb736aa400a9c9bf25937fd74cdf078967..86034079f08add73afa549d70e22704e2d0f81c9 100644 --- a/src/test/java/de/tla2b/examples/MCTest.java +++ b/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"; diff --git a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java index c438421b153233d73f69e15ba5e0a4f2283e9fc1..26fbc3c17ee0c45f34cad7b5b59fe69a6cbc982b 100644 --- a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java +++ b/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); + } } diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java index 01500661376e5e12fd514b414224f4895360d552..4ba3f0ed7a579be5d7377f97dcd717f7604ac5f3 100644 --- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java +++ b/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 { diff --git a/src/test/resources/MCTests/InvariantReals/RealInvariant.cfg b/src/test/resources/MCTests/InvariantReals/RealInvariant.cfg new file mode 100644 index 0000000000000000000000000000000000000000..62e5d5ccadfdaf55156e23a0b6178b23b7b35e37 --- /dev/null +++ b/src/test/resources/MCTests/InvariantReals/RealInvariant.cfg @@ -0,0 +1,6 @@ +INIT +Init +NEXT +Next +INVARIANT +Inv diff --git a/src/test/resources/MCTests/InvariantReals/RealInvariant.tla b/src/test/resources/MCTests/InvariantReals/RealInvariant.tla new file mode 100644 index 0000000000000000000000000000000000000000..f002cc1b2e2348b80d4c54a3d1f46fdb0f5fa6d5 --- /dev/null +++ b/src/test/resources/MCTests/InvariantReals/RealInvariant.tla @@ -0,0 +1,9 @@ +--------------------------- 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 + +============================================================================