Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.01 KB)

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