From 6792f885611b2a0f9ec8513347bd071dd93482af Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Thu, 2 May 2024 10:11:10 +0200
Subject: [PATCH] add more tests for reals
---
src/test/java/de/tla2b/examples/MCTest.java | 6 +++++
.../expression/ModuleAndExpressionTest.java | 22 +++++++++++++++----
.../standardmodules/TestModuleReals.java | 17 ++++++++++++++
.../MCTests/InvariantReals/RealInvariant.cfg | 6 +++++
.../MCTests/InvariantReals/RealInvariant.tla | 9 ++++++++
5 files changed, 56 insertions(+), 4 deletions(-)
create mode 100644 src/test/resources/MCTests/InvariantReals/RealInvariant.cfg
create mode 100644 src/test/resources/MCTests/InvariantReals/RealInvariant.tla
diff --git a/src/test/java/de/tla2b/examples/MCTest.java b/src/test/java/de/tla2b/examples/MCTest.java
index dd8032f..8603407 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 c438421..26fbc3c 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 0150066..4ba3f0e 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 0000000..62e5d5c
--- /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 0000000..f002cc1
--- /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
+
+============================================================================
--
GitLab