summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-13 11:31:50 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-13 11:31:50 +0200
commitf7868083de2f351b5195149870e6e77398da44f9 (patch)
tree88e4b477edec70ead05f2a3d69e7a270966cd00e /tests
parent26b263fbe8938d1fe13ee67ab87a2edeea9c99aa (diff)
downloadscade-analyzer-f7868083de2f351b5195149870e6e77398da44f9.tar.gz
scade-analyzer-f7868083de2f351b5195149870e6e77398da44f9.zip
Parse activate blocks.
Diffstat (limited to 'tests')
-rw-r--r--tests/limitera.scade26
1 files changed, 26 insertions, 0 deletions
diff --git a/tests/limitera.scade b/tests/limitera.scade
new file mode 100644
index 0000000..1e4927e
--- /dev/null
+++ b/tests/limitera.scade
@@ -0,0 +1,26 @@
+const bound: int = 128;
+
+node limiter(x: int; d: int) returns (probe y: int)
+ var s, r: int;
+ let
+ assume in_bounded: x >= -bound and x <= bound;
+ guarantee out_bounded: y >= -bound and y <= bound;
+ s = 0 -> pre y;
+ r = x - s;
+ activate
+ if r <= -d then
+ let y = s - d; tel
+ else if r >= d then
+ let y = s + d; tel
+ else
+ let y = x; tel
+ returns y;
+ tel
+
+node test(i: int) returns(a, b, c: int; exit: bool)
+ let
+ exit = i >= 30;
+ a = (i * 21 + 122) mod (2 * bound) - bound; -- not really random
+ b = 16;
+ c = limiter(a, b);
+ tel