lustrec / test / src / kind_fmcad08 / simulation / hysteresis_1.lus @ 0cbf0839
History | View | Annotate | Download (986 Bytes)
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 ); |
34 |
--%PROPERTY OK=true; |
35 |
--%MAIN; |
36 |
tel |