From 5d428bdc5e0d60455fce1df9b89f23c41e8bef08 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Mon, 29 Apr 2024 14:26:26 +0200
Subject: [PATCH] add more tests
---
src/test/java/de/tla2b/examples/MCTest.java | 2 +-
.../de/tla2b/expression/ComplexExpressionTest.java | 5 +++++
src/test/java/de/tla2b/expression/TestKeywords.java | 10 ++++++++++
src/test/java/de/tla2b/typechecking/InstanceTest.java | 7 +++++++
.../resources/typechecking/modules/CounterReal.tla | 10 ++++++++++
5 files changed, 33 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/typechecking/modules/CounterReal.tla
diff --git a/src/test/java/de/tla2b/examples/MCTest.java b/src/test/java/de/tla2b/examples/MCTest.java
index 2526a1f..756380b 100644
--- a/src/test/java/de/tla2b/examples/MCTest.java
+++ b/src/test/java/de/tla2b/examples/MCTest.java
@@ -72,7 +72,7 @@ public class MCTest {
@Ignore
@Test
- public void testRecursiveFunciton() throws Exception {
+ public void testRecursiveFunction() throws Exception {
String file = "src/test/resources/examples/RecursiveFunction/RecursiveFunction.tla";
runModule(file);
}
diff --git a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
index 297a8a6..520e759 100644
--- a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
@@ -38,6 +38,11 @@ public class ComplexExpressionTest {
compareExpr("1 + 2", "LET foo == 1 bar == 2 IN foo + bar ");
}
+ @Test
+ public void testLetTwoDefsReal() throws Exception {
+ compareExpr("1.0 + 2.0", "LET foo == 1.0 bar == 2.0 IN foo + bar ");
+ }
+
@Test
public void testPrime() throws Exception {
compareExpr("x_n = 1", "x' = 1");
diff --git a/src/test/java/de/tla2b/expression/TestKeywords.java b/src/test/java/de/tla2b/expression/TestKeywords.java
index 0f38543..393fec6 100644
--- a/src/test/java/de/tla2b/expression/TestKeywords.java
+++ b/src/test/java/de/tla2b/expression/TestKeywords.java
@@ -16,6 +16,16 @@ public class TestKeywords {
compareExpr("NATURAL", "Nat");
}
+ @Test
+ public void testInt() throws Exception {
+ compareExpr("INTEGER", "Int");
+ }
+
+ @Test
+ public void testReal() throws Exception {
+ compareExpr("REAL", "Real");
+ }
+
@Test
public void testExcept() throws Exception {
compareExpr("x = a <+ {1 |-> 1}", "x = [a EXCEPT ![1] = 1]");
diff --git a/src/test/java/de/tla2b/typechecking/InstanceTest.java b/src/test/java/de/tla2b/typechecking/InstanceTest.java
index 0c6ab19..159380b 100644
--- a/src/test/java/de/tla2b/typechecking/InstanceTest.java
+++ b/src/test/java/de/tla2b/typechecking/InstanceTest.java
@@ -10,6 +10,13 @@ public class InstanceTest {
private static final String path = "src/test/resources/typechecking/modules/";
+ @Test
+ public void TestCounterReal() throws Exception {
+ TestTypeChecker t = TestUtil.typeCheck(path + "CounterReal.tla");
+ assertEquals("REAL", t.getConstantType("start"));
+ assertEquals("REAL", t.getVariableType("x"));
+ }
+
@Test
public void TestNamedInstanceCounter() throws Exception {
TestTypeChecker t = TestUtil.typeCheck(path + "NamedInstanceCounter.tla");
diff --git a/src/test/resources/typechecking/modules/CounterReal.tla b/src/test/resources/typechecking/modules/CounterReal.tla
new file mode 100644
index 0000000..3631b58
--- /dev/null
+++ b/src/test/resources/typechecking/modules/CounterReal.tla
@@ -0,0 +1,10 @@
+-------------------------- MODULE CounterReal -----------------------------
+EXTENDS Reals
+CONSTANTS start
+VARIABLE x
+---------------------------------------------------------------------------
+Init == x = start
+Inc == x' = x + 1.0
+Dec == x' = x - 0.99
+Next == Inc \/ Dec
+===========================================================================
--
GitLab