Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / car_3.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

    
11
node excludes2( X1, X2 : bool ) returns ( excludes : bool );
12
let
13
    excludes = not ( X1 and X2 );
14
tel
15

    
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
node top(m, s : bool) returns (OK : bool);
40
var toofast, stop, bump: bool;
41
    dist, speed, time: int;
42
    move: bool; second, meter: bool;
43
    env : bool;
44
let
45
  (toofast, stop, bump, dist, speed, time, move, second, meter) = voiture(m,s);
46
  env = Sofar( excludes2( m, s ) );
47

    
48
  OK = env => speed < 4;
49
  --%PROPERTY OK=true;
50
  --%MAIN;
51
tel