diff --git a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java index 3c45ca730653f768412f8527cf4af98f26d9f83a..28a3ba07deb75e6b90f0e84162a4d4aec07b8bd6 100644 --- a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java +++ b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java @@ -265,6 +265,70 @@ public class TypeRestrictionsTest { + "======"; compare(expected, machine); } - - + + @Test + public void testAnyEqual() throws Exception { + String machine = "MACHINE test\n" + + "VARIABLES x\n" + + "INVARIANT x = 1\n" + + "INITIALISATION x := 1\n" + + "OPERATIONS\n" + + "foo = ANY y WHERE y=1 THEN x:=y END\n" + + "END"; + String expected = "---- MODULE test ----\n" + + "VARIABLES x\n" + + "Invariant1 == x = 1\n" + + "Init == x = 1\n" + + "\n" + + "foo == \\E y \\in {1} : x' = y\n" + + "\n" + + "Next == \\/ foo\n" + + "===="; + compare(expected, machine); + } + + @Test + public void testAnyMember() throws Exception { + String machine = "MACHINE test\n" + + "VARIABLES x\n" + + "INVARIANT x = 1\n" + + "INITIALISATION x := 1\n" + + "OPERATIONS\n" + + "foo = ANY y WHERE y:{1} THEN x:=y END\n" + + "END"; + String expected = "---- MODULE test ----\n" + + "VARIABLES x\n" + + "Invariant1 == x = 1\n" + + "Init == x = 1\n" + + "\n" + + "foo == \\E y \\in {1} : x' = y\n" + + "\n" + + "Next == \\/ foo\n" + + "===="; + compare(expected, machine); + } + + @Ignore // TODO: improve type restrictor + @Test + public void testAnyNestedEqualInIf() throws Exception { + String machine = "MACHINE test\n" + + "CONSTANTS B\n" + + "PROPERTIES B:BOOL\n" + + "VARIABLES x\n" + + "INVARIANT x = 1\n" + + "INITIALISATION x := 1\n" + + "OPERATIONS\n" + + "foo = ANY y WHERE IF B=TRUE THEN y=1 ELSE y=1 END THEN x:=y END\n" + + "END"; + String expected = "---- MODULE test ----\n" + + "VARIABLES x\n" + + "Invariant1 == x = 1\n" + + "Init == x = 1\n" + + "\n" + + "foo == \\E y \\in {1} : x' = y\n" + + "\n" + + "Next == \\/ foo\n" + + "===="; + compare(expected, machine); + } }