summaryrefslogtreecommitdiff
path: root/tests/source/updown.scade
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-13 14:17:22 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-13 14:17:22 +0200
commitdedc98b0c14262c53e8573d7fe1dcaa370e43fb5 (patch)
treeac02f7271b054247984caa8aac13451ba98dc15b /tests/source/updown.scade
parentf7868083de2f351b5195149870e6e77398da44f9 (diff)
downloadscade-analyzer-dedc98b0c14262c53e8573d7fe1dcaa370e43fb5.tar.gz
scade-analyzer-dedc98b0c14262c53e8573d7fe1dcaa370e43fb5.zip
Move a lot of things.
Diffstat (limited to 'tests/source/updown.scade')
-rw-r--r--tests/source/updown.scade26
1 files changed, 26 insertions, 0 deletions
diff --git a/tests/source/updown.scade b/tests/source/updown.scade
new file mode 100644
index 0000000..089293a
--- /dev/null
+++ b/tests/source/updown.scade
@@ -0,0 +1,26 @@
+const bound: int = 7;
+
+node updown() returns(probe x: int)
+var last_x: int;
+let
+ last_x = 0 -> pre x;
+ guarantee x_bounded: x >= -bound and x <= bound;
+ 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;
+tel
+
+node test(i: int) returns(a, b, c: int; exit: bool)
+let
+ exit = i >= 30;
+ a = updown();
+ b = 0;
+ c = 0;
+tel