Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (976 Bytes)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X or pre Sofar;
5
tel
6
node Environment(diff: int; plus,minus: bool) returns (ok: bool);
7
let
8
  ok = (-4 <= diff or diff <= 4) and 
9
     (if (true -> pre plus) then diff >= 1 else true) and
10
     (if (false -> pre minus) then diff <= -1 else true);
11
tel
12
node Controller(diff: int) returns (speed: int; plus,minus: bool);
13
let
14
  speed = 0 -> pre(speed)+diff;
15
  plus = speed <= 9;
16
  minus = speed >= 11;
17
tel
18
node Property(speed: int) returns (ok: bool);
19
var cpt: int;
20
    acceptable: bool;
21
let
22
  acceptable = 8 <= speed and speed <= 12;
23
  cpt = 0 -> if acceptable then 0 else pre(cpt)+1;
24
  ok = true -> (pre cpt<=7);
25
tel
26
node top(diff:int) returns (OK: bool);
27
var speed: int; 
28
    plus,minus,realistic: bool;
29
let
30
  (speed,plus,minus) = Controller(diff);
31
  realistic =  Environment(diff,plus,minus);
32
  OK = Sofar( realistic and 0 <= speed and speed < 16 ) => Property(speed);
33
  --%MAIN;
34
  --%PROPERTY  OK=true;
35
tel