1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
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
|
