Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.14 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
node excludes2( X1, X2 : bool ) returns ( excludes : bool );
11
let
12
    excludes = not ( X1 and X2 );
13
tel
14

    
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 ) );
45

    
46
  OK = env => speed >= 0;
47
  --%PROPERTY OK=true;
48
  --%MAIN;
49
tel