From bc679afc4ac59c256a1b5f200078e495c188d066 Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Wed, 2 Jul 2014 16:24:12 +0200
Subject: Fix non-termination issue in EDDs

---
 tests/source/updown2.scade | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 tests/source/updown2.scade

(limited to 'tests')

diff --git a/tests/source/updown2.scade b/tests/source/updown2.scade
new file mode 100644
index 0000000..73d111a
--- /dev/null
+++ b/tests/source/updown2.scade
@@ -0,0 +1,40 @@
+const bound: int = 7;
+
+node updown() returns(probe x, probe y, probe z: int)
+var last_x, last_y: int;
+let
+    last_x = 0 -> pre x;
+    automaton
+        initial state UP
+        let x = last_x + 1; tel
+        until if x >= bound resume DOWN;
+
+        state DOWN
+        let x = last_x - 1; tel
+        until if x <= -bound resume UP;
+
+    returns x;
+    guarantee x_bounded: x >= -bound and x <= bound;
+
+    last_y = 0 -> pre y;
+    automaton
+        initial state DOWN
+        let y = last_y - 1; tel
+        until if y <= -bound resume UP;
+
+        state UP
+        let y = last_y + 1; tel
+        until if y >= bound resume DOWN;
+
+    returns y;
+    guarantee y_bounded: y >= -bound and y <= bound;
+
+    z = x + y;
+    guarantee x_y_opp: z = 0 and (true -> pre (z = 0));
+tel
+
+node test(i: int) returns(a, b, c: int; exit: bool)
+let
+    exit = i >= 30;
+    a, b, c = updown2();
+tel
-- 
cgit v1.2.3