From 4f84c123222ff6f4b43ab97e013b6dc989c11039 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Wed, 28 May 2014 14:33:20 +0200
Subject: [PATCH] Fixed bug in "find guards" algorithm
---
.../java/de/tla2b/analysis/BOperation.java | 9 ++-
.../de/tla2b/prettyprintb/EventsTest.java | 63 +++++++++++++++++++
2 files changed, 71 insertions(+), 1 deletion(-)
create mode 100644 src/test/java/de/tla2b/prettyprintb/EventsTest.java
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 43aaac2..fddcb1f 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -256,7 +256,14 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
}
}
- beforeAfterPredicates.add(node);
+ if (node.level < 2) {
+ guards.add(node);
+ return;
+ } else {
+ beforeAfterPredicates.add(node);
+ return;
+ }
+ //beforeAfterPredicates.add(node);
}
private void evalParams() {
diff --git a/src/test/java/de/tla2b/prettyprintb/EventsTest.java b/src/test/java/de/tla2b/prettyprintb/EventsTest.java
new file mode 100644
index 0000000..1db65ff
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/EventsTest.java
@@ -0,0 +1,63 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class EventsTest {
+
+
+ @Test
+ public void testOperation1() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "VARIABLES x, y \n"
+ + "Init == x = 1 /\\ y = 1 \n"
+ + "Next == x' = 1 /\\ UNCHANGED y\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "VARIABLES x, y\n"
+ + "INVARIANT x : INTEGER & y : INTEGER \n"
+ + "INITIALISATION x, y:(x = 1 & y = 1) \n"
+ + "OPERATIONS Next = ANY y_n WHERE y_n : INTEGER & y_n = y THEN x,y := 1,y_n END \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testOperation2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "VARIABLES x, y \n"
+ + "Init == x = 1 /\\ y = 1 \n"
+ + "Next == x = 2 /\\ x' = 1 /\\ y' = y\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "VARIABLES x, y\n"
+ + "INVARIANT x : INTEGER & y : INTEGER \n"
+ + "INITIALISATION x, y:(x = 1 & y = 1) \n"
+ + "OPERATIONS Next = SELECT x = 2 THEN x,y := 1,y END \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testOperation3() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "VARIABLES x, y \n"
+ + "Init == x = 1 /\\ y = 1 \n"
+ + "Next == x < 2 /\\ x' = 1 /\\ y' = y\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "VARIABLES x, y\n"
+ + "INVARIANT x : INTEGER & y : INTEGER \n"
+ + "INITIALISATION x, y:(x = 1 & y = 1) \n"
+ + "OPERATIONS Next = SELECT x < 2 THEN x,y := 1,y END \n"
+ + "END";
+ compare(expected, module);
+ }
+}
--
GitLab