Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.16 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

    
11
node excludes2( X1, X2 : bool ) returns ( excludes : bool );
12
let
13
    excludes = not ( X1 and X2 );
14
tel
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 ) and dist < 32767);
45

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