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