summaryrefslogtreecommitdiff
path: root/tests/updown.scade
diff options
context:
space:
mode:
Diffstat (limited to 'tests/updown.scade')
-rw-r--r--tests/updown.scade10
1 files changed, 3 insertions, 7 deletions
diff --git a/tests/updown.scade b/tests/updown.scade
index 02e2029..089293a 100644
--- a/tests/updown.scade
+++ b/tests/updown.scade
@@ -4,19 +4,15 @@ node updown() returns(probe x: int)
var last_x: int;
let
last_x = 0 -> pre x;
- guarantee x_bounded : x >= -bound and x <= bound;
+ guarantee x_bounded: x >= -bound and x <= bound;
automaton
initial state UP
let x = last_x + 1; tel
- until if x >= bound
- do guarantee x_up : x = bound;
- resume DOWN;
+ until if x >= bound resume DOWN;
state DOWN
let x = last_x - 1; tel
- until if x <= -bound
- do guarantee x_down : x = -bound;
- resume UP;
+ until if x <= -bound resume UP;
returns x;
tel