diff --git a/src/test/java/de/tla2b/typechecking/InstanceTest.java b/src/test/java/de/tla2b/typechecking/InstanceTest.java index 22795acd8f2008b1c9a177da52a1e0184d5f7b4c..dd6ce97fa86c877853ecb04dcc61e2fed7973596 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 0000000000000000000000000000000000000000..7b868807939b755c51b8dde2afc42b20866468fd --- /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