diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/source/updown2.scade | 40 |
1 files changed, 40 insertions, 0 deletions
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 |