summaryrefslogtreecommitdiff
path: root/tests/source
diff options
context:
space:
mode:
Diffstat (limited to 'tests/source')
-rw-r--r--tests/source/cdrom.scade10
1 files changed, 8 insertions, 2 deletions
diff --git a/tests/source/cdrom.scade b/tests/source/cdrom.scade
index 92438c3..03501d5 100644
--- a/tests/source/cdrom.scade
+++ b/tests/source/cdrom.scade
@@ -1,5 +1,6 @@
-node cdrom(speed: int) returns (plus, minus, error: bool)
+node cdrom(probe speed: int) returns (plus, minus, error: bool)
var ps, count: int;
+ _a, _b, _la, _lb: bool;
let
ps = 0 -> pre speed;
@@ -11,9 +12,14 @@ let
plus = (ps <= 9);
minus = (ps >= 11);
+ _a = speed < 8;
+ _b = speed > 12;
+ _la = true -> pre _a;
+ _lb = false -> pre _b;
+
count = if speed < 8 or speed > 12
then (0 -> pre count) + 1 else 0;
error = (count >= 15);
- guarantee g: not error and (true -> not pre error);
+ guarantee g: not error;
tel