diff options
Diffstat (limited to 'tests/source/train.scade')
-rw-r--r-- | tests/source/train.scade | 69 |
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 + |