Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.08 KB)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X and pre Sofar;
5
tel
6
node excludes2( X1, X2 : bool ) returns ( excludes : bool );
7
let
8
    excludes = not ( X1 and X2 );
9
tel
10
node voiture(m,s: bool) returns
11
(   toofast, stop, bump: bool;
12
    dist, speed, time: int;
13
    move: bool; second, meter: bool );
14
let
15
  meter = false -> (m and not s);
16
  second = false -> s;
17
  move = true -> pre(move and not stop and not toofast and not bump);
18
  dist = 0 -> if move and meter then pre(dist)+1
19
			   else pre(dist);
20
  speed = 0 -> if not move and second then 0
21
		else if move and meter then pre(speed) -1+ 1
22
		else pre(speed);
23
  time = 0 -> if second then pre(time) + 1
24
		else pre(time);
25
  toofast = speed >= 3;
26
  stop = time >= 4;
27
  bump = dist = 10;
28
tel
29
node top(m, s : bool) returns (OK : bool);
30
var toofast, stop, bump: bool;
31
    dist, speed, time: int;
32
    move: bool; second, meter: bool;
33
    env : bool;
34
let
35
  (toofast, stop, bump, dist, speed, time, move, second, meter) = voiture(m,s);
36
  env = Sofar( excludes2( m, s ) );
37
  OK = env => speed < 4;
38
  --%MAIN;
39
  --%PROPERTY  OK=true;
40
tel