Skip to content
Snippets Groups Projects
Commit d7958a24 authored by Jan Gruteser's avatar Jan Gruteser
Browse files

adapt test for NamedInstanceCounterReal

parent 0235f216
Branches
Tags
No related merge requests found
......@@ -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
......
-------------- MODULE NamedInstanceCounterReal ----------------
CONSTANTS start
VARIABLES c
count == INSTANCE CounterReal WITH x <- c
Init == count!Init
Next == count!Next
=================================
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment