lustrec / test / src / kind_fmcad08 / simulation / car_all.lus @ 22fe1c93
History | View | Annotate | Download (1.14 KB)
1 |
|
---|---|
2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
3 |
let |
4 |
Sofar = X -> X and pre Sofar; |
5 |
tel |
6 |
|
7 |
node excludes2( X1, X2 : bool ) returns ( excludes : bool ); |
8 |
let |
9 |
excludes = not ( X1 and X2 ); |
10 |
tel |
11 |
|
12 |
node voiture(m,s: bool) returns |
13 |
( toofast, stop, bump: bool; |
14 |
dist, speed, time: int; |
15 |
move: bool; second, meter: bool ); |
16 |
let |
17 |
meter = false -> (m and not s); |
18 |
second = false -> s; |
19 |
move = true -> pre(move and not stop and not toofast and not bump); |
20 |
dist = 0 -> if move and meter then pre(dist)+1 |
21 |
else pre(dist); |
22 |
speed = 0 -> if not move or second then 0 |
23 |
else if move and meter then pre(speed) + 1 |
24 |
else pre(speed); |
25 |
time = 0 -> if second then pre(time) + 1 |
26 |
else pre(time); |
27 |
toofast = speed >= 3; |
28 |
stop = time >= 4; |
29 |
bump = dist = 10; |
30 |
|
31 |
tel |
32 |
|
33 |
node top(m, s : bool) returns (OK : bool); |
34 |
var toofast, stop, bump: bool; |
35 |
dist, speed, time: int; |
36 |
move: bool; second, meter: bool; |
37 |
env : bool; |
38 |
let |
39 |
(toofast, stop, bump, dist, speed, time, move, second, meter) = voiture(m,s); |
40 |
env = Sofar( excludes2( m, s ) and dist < 32767); |
41 |
|
42 |
OK = env => dist >= 0 and dist < 11 and speed < 4 and speed >= 0; |
43 |
--%PROPERTY OK=true; |
44 |
--%MAIN; |
45 |
tel |