Profile

Statistics
| Branch: | Tag: | Revision:

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

 1 ```-- ``` ```-- 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 ); ``` ```--@ contract guarantees OK; ``` ``` var late, early : bool; ``` ```let ``` ``` ( late, early ) = speed( beacon, second ); ``` ``` OK = true -> not ( pre late and early ); ``` ``` --%PROPERTY OK=true; ``` ``` --%MAIN; ``` ```tel ```