diff options
author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-13 11:31:50 +0200 |
---|---|---|
committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-13 11:31:50 +0200 |
commit | f7868083de2f351b5195149870e6e77398da44f9 (patch) | |
tree | 88e4b477edec70ead05f2a3d69e7a270966cd00e /tests | |
parent | 26b263fbe8938d1fe13ee67ab87a2edeea9c99aa (diff) | |
download | scade-analyzer-f7868083de2f351b5195149870e6e77398da44f9.tar.gz scade-analyzer-f7868083de2f351b5195149870e6e77398da44f9.zip |
Parse activate blocks.
Diffstat (limited to 'tests')
-rw-r--r-- | tests/limitera.scade | 26 |
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 |