Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / car_5.lus @ 22fe1c93

History | View | Annotate | Download (1.21 KB)

1 22fe1c93 ploc
--
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
var toofast, stop, bump: bool;
42
    dist, speed, time: int;
43
    move: bool; second, meter: bool;
44
    env : bool;
45
let
46
  (toofast, stop, bump, dist, speed, time, move, second, meter) = voiture(m,s);
47
  env = Sofar( excludes2( m, s ) );
48
49
  OK = env => (dist > 9 => not( move and meter));
50
  --%PROPERTY OK=true;
51
  --%MAIN;
52
tel