From 6386473c92bd1ec374d9f8f5dac43fb7f84d5966 Mon Sep 17 00:00:00 2001
From: Miles Vella <673-vella@users.noreply.gitlab.cs.uni-duesseldorf.de>
Date: Mon, 17 Mar 2025 19:01:08 +0100
Subject: [PATCH] add test and todo for type restrictor with if-predicate
---
.../tlc4b/analysis/TypeRestrictionsTest.java | 68 ++++++++++++++++++-
1 file changed, 66 insertions(+), 2 deletions(-)
diff --git a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
index 3c45ca7..28a3ba0 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);
+ }
}
--
GitLab