1 |
b8dc00eb
|
bourbouh
|
|
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
|
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 |
2d37a1e1
|
ploc
|
--@ contract guarantees OK;
|
31 |
b8dc00eb
|
bourbouh
|
var toofast, stop, bump: bool;
|
32 |
|
|
dist, speed, time: int;
|
33 |
|
|
move: bool; second, meter: bool;
|
34 |
|
|
env : bool;
|
35 |
|
|
let
|
36 |
|
|
(toofast, stop, bump, dist, speed, time, move, second, meter) = voiture(m,s);
|
37 |
|
|
env = Sofar( excludes2( m, s ) and dist < 32767);
|
38 |
|
|
OK = env => dist >= 0 and dist < 11 and speed < 4 and speed >= 0;
|
39 |
|
|
--%MAIN;
|
40 |
|
|
--%PROPERTY OK=true;
|
41 |
|
|
tel
|