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