1 |
b8dc00eb
|
bourbouh
|
--
|
2 |
|
|
-- Source: David Merchat (node voiture + property v6)
|
3 |
|
|
--
|
4 |
|
|
|
5 |
|
|
|
6 |
|
|
node Sofar( X : bool ) returns ( Sofar : bool );
|
7 |
|
|
let
|
8 |
|
|
Sofar = X -> X and pre Sofar;
|
9 |
|
|
tel
|
10 |
|
|
|
11 |
|
|
|
12 |
|
|
node excludes2( X1, X2 : bool ) returns ( excludes : bool );
|
13 |
|
|
let
|
14 |
|
|
excludes = not ( X1 and X2 );
|
15 |
|
|
tel
|
16 |
|
|
|
17 |
|
|
node voiture(m,s: bool) returns
|
18 |
|
|
( toofast, stop, bump: bool;
|
19 |
|
|
dist, speed, time: int;
|
20 |
|
|
move: bool; second, meter: bool );
|
21 |
|
|
let
|
22 |
|
|
meter = false -> (m and not s);
|
23 |
|
|
second = false -> s;
|
24 |
|
|
move = true -> pre(move and not stop and not toofast and not bump);
|
25 |
|
|
dist = 0 -> if move and meter then pre(dist)+1
|
26 |
|
|
else pre(dist);
|
27 |
|
|
speed = 0 -> if not move or second then 0
|
28 |
|
|
else if move and meter then pre(speed) + 1
|
29 |
|
|
else pre(speed);
|
30 |
|
|
time = 0 -> if second then pre(time) + 1
|
31 |
|
|
else pre(time);
|
32 |
|
|
toofast = speed >= 3;
|
33 |
|
|
stop = time >= 4;
|
34 |
|
|
bump = dist = 10;
|
35 |
|
|
|
36 |
|
|
tel
|
37 |
|
|
|
38 |
|
|
|
39 |
|
|
-- Can't prove in luke-bitvec, luke-hybrid, nbac
|
40 |
|
|
node top(m, s : bool) returns (OK : bool);
|
41 |
2d37a1e1
|
ploc
|
--@ contract guarantees OK;
|
42 |
b8dc00eb
|
bourbouh
|
var toofast, stop, bump: bool;
|
43 |
|
|
dist, speed, time: int;
|
44 |
|
|
move: bool; second, meter: bool;
|
45 |
|
|
env : bool;
|
46 |
|
|
let
|
47 |
|
|
(toofast, stop, bump, dist, speed, time, move, second, meter) = voiture(m,s);
|
48 |
|
|
env = Sofar( excludes2( m, s ) );
|
49 |
|
|
|
50 |
|
|
OK = env => (dist > 9 => not( move and meter));
|
51 |
|
|
--%PROPERTY OK=true;
|
52 |
|
|
--%MAIN;
|
53 |
|
|
tel
|