From d7958a24983365510497f05f3841c8fe16f8ddbb Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Thu, 24 Oct 2024 09:50:04 +0200
Subject: [PATCH] adapt test for NamedInstanceCounterReal
---
src/test/java/de/tla2b/typechecking/InstanceTest.java | 6 +++---
.../typechecking/modules/NamedInstanceCounterReal.tla | 7 +++++++
2 files changed, 10 insertions(+), 3 deletions(-)
create mode 100644 src/test/resources/typechecking/modules/NamedInstanceCounterReal.tla
diff --git a/src/test/java/de/tla2b/typechecking/InstanceTest.java b/src/test/java/de/tla2b/typechecking/InstanceTest.java
index 22795ac..dd6ce97 100644
--- a/src/test/java/de/tla2b/typechecking/InstanceTest.java
+++ b/src/test/java/de/tla2b/typechecking/InstanceTest.java
@@ -11,10 +11,10 @@ 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");
+ public void TestNamedInstanceCounterReal() throws Exception {
+ TestTypeChecker t = TestUtil.typeCheck(path + "NamedInstanceCounterReal.tla");
+ assertEquals("REAL", t.getVariableType("c"));
assertEquals("REAL", t.getConstantType("start"));
- assertEquals("REAL", t.getVariableType("x"));
}
@Test
diff --git a/src/test/resources/typechecking/modules/NamedInstanceCounterReal.tla b/src/test/resources/typechecking/modules/NamedInstanceCounterReal.tla
new file mode 100644
index 0000000..7b86880
--- /dev/null
+++ b/src/test/resources/typechecking/modules/NamedInstanceCounterReal.tla
@@ -0,0 +1,7 @@
+-------------- MODULE NamedInstanceCounterReal ----------------
+CONSTANTS start
+VARIABLES c
+count == INSTANCE CounterReal WITH x <- c
+Init == count!Init
+Next == count!Next
+=================================
\ No newline at end of file
--
GitLab