Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.06 KB)

1
--
2
-- Source: N. Halbwachs, P Raymond "A Tutorial of Lustre", 2002
3
--
4

    
5
node counter( init, incr : int; x, reset : bool ) returns ( c : int );
6
    var pc : int;
7
let
8
    pc = init -> pre c;
9
    c = if reset then init
10
        else if x and pc > -1000 and pc < 1000 then pc + incr
11
--        else if x then pc + incr
12
        else pc;
13
tel
14

    
15

    
16
node speed( beacon, second : bool ) returns ( late, early : bool );
17
    var diff, incr : int;
18
let
19
    incr = if beacon and not second then 1
20
           else if second and not beacon then -1
21
           else 0;
22
    diff = counter( 0, incr, beacon or second, false );
23
    early = false -> if pre early then diff > 0
24
                     else diff >= 10;
25
    late = false -> if pre late then diff < 0
26
                    else diff <= -10;
27
tel
28

    
29
node top( beacon, second : bool ) returns ( OK : bool );
30
    var late, early : bool;
31
let
32
    ( late, early ) = speed( beacon, second );
33
    OK = not ( late and early ) and
34
           (true -> not ( late and pre early )) and
35
           (true -> not ( pre late and early ));
36
    --%PROPERTY OK=true;
37
    --%MAIN;
38
tel