CristalCaveGem » LustreC

--

-- 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 top( beacon, second : bool ) returns ( OK : bool );

    var late, early : bool;

let

    ( late, early ) = speed( beacon, second );

    OK = true -> not ( pre late and early );

    --%PROPERTY OK=true;

    --%MAIN;

tel