hysteresis_1.lus

--
-- Source: N. Halbwachs, P Raymond "A Tutorial of Lustre", 2002
--

node counter( init, incr : int; x, reset : bool ) returns ( c : int );
    var pc : int;
let
    pc = init -> pre c;
    c = if reset then init
        else if x and pc > -1000 and pc < 1000 then pc + incr
--        else if x then pc + incr
        else pc;
tel


node speed( beacon, second : bool ) returns ( late, early : bool );
    var diff, incr : int;
let
    incr = if beacon and not second then 1
           else if second and not beacon then -1
           else 0;
    diff = counter( 0, incr, beacon or second, false );
    early = false -> if pre early then diff > 0
                     else diff >= 10;
    late = false -> if pre late then diff < 0
                    else diff <= -10;
tel

node hysteresis_1( beacon, second : bool ) returns ( OK : bool );
--@ contract guarantee OK by 1-induction;
    var late, early : bool;
let
    ( late, early ) = speed( beacon, second );
    OK = not ( late and early );
    --%PROPERTY OK=true;
    --%MAIN;
tel