Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / simulation / cd_e7_8.lus @ 2d37a1e1

History | View | Annotate | Download (1005 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 and 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
--@ contract guarantees OK;
28
var speed: int; 
29
    plus,minus,realistic: bool;
30
let
31
  (speed,plus,minus) = Controller(diff);
32
  realistic =  Environment(diff,plus,minus);
33
  OK = Sofar( realistic and 0 <= speed and speed < 16 ) => Property(speed);
34
  --%MAIN;
35
  --%PROPERTY  OK=true;
36
tel