summaryrefslogtreecommitdiff
path: root/tests/source/train.scade
diff options
context:
space:
mode:
Diffstat (limited to 'tests/source/train.scade')
-rw-r--r--tests/source/train.scade69
1 files changed, 69 insertions, 0 deletions
diff --git a/tests/source/train.scade b/tests/source/train.scade
new file mode 100644
index 0000000..c51971e
--- /dev/null
+++ b/tests/source/train.scade
@@ -0,0 +1,69 @@
+-- Cet exemple est clairement trop compliqué.
+
+
+node diff(incr, decr: bool) returns (diff: int)
+let
+ diff = (0 -> pre diff) +
+ (if incr and not decr then 1
+ else if not incr and decr then -1
+ else 0);
+tel
+
+node train(beacon, second: bool) returns (early, late: bool)
+var probe advance: int;
+let
+ advance = diff(beacon, second);
+
+ automaton
+ initial state NotEarly
+ let early = false; tel
+ until if advance >= 10 resume Early;
+
+ state Early
+ let early = true; tel
+ until if advance = 0 resume NotEarly;
+ returns early;
+
+ automaton
+ initial state NotLate
+ let late = false; tel
+ until if advance <= -10 resume Late;
+
+ state Late
+ let late = true; tel
+ until if advance = 0 resume NotLate;
+ returns late;
+tel
+
+node observer(early, late: bool) returns (alarm: bool)
+var ontime: bool;
+let
+ ontime = not (late or early);
+ automaton
+ initial state Ok
+ let alarm = false; tel
+ until if early resume Early;
+
+ state Early
+ let alarm = late and not early; tel
+ until if ontime resume Ok;
+ returns alarm;
+tel
+
+node train_check(beacon, second: bool) returns (early, late, alarm: bool)
+let
+ early, late = train(beacon, second);
+ alarm = observer(early, late);
+ guarantee ok : not alarm;
+tel
+
+node test(i: int) returns(a, b, c: int; exit: bool)
+var early, late, alarm: bool;
+let
+ exit = i >= 100;
+ early, late, alarm = train_check((i+1) mod 2 = 0, i mod 3 = 0);
+ c = if alarm then 1 else 0;
+ a = if early then 1 else 0;
+ b = if late then 1 else 0;
+tel
+