lustrec / test / src / kind_fmcad08 / simulation / car_4_e7_592.lus @ 0cbf0839
History | View | Annotate | Download (1.08 KB)
1 | 0cbf0839 | ploc | |
---|---|---|---|
2 | node Sofar( X : bool ) returns ( Sofar : bool ); |
||
3 | let |
||
4 | Sofar = X -> X or 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 or second then 0 |
||
21 | else if move and meter then pre(speed) + 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 ) ); |
||
37 | OK = env => speed >= 0; |
||
38 | --%MAIN; |
||
39 | --%PROPERTY OK=true; |
||
40 | tel |