lustrec / test / src / kind_fmcad08 / misc / two_counters_e3_325.lus @ 0cbf0839
History | View | Annotate | Download (447 Bytes)
1 |
|
---|---|
2 |
node greycounter (x:bool) returns (out:bool); |
3 |
var a,b:bool; |
4 |
let |
5 |
a = false -> not pre(b); |
6 |
b = false -> pre(a); |
7 |
out = a and b; |
8 |
tel |
9 |
node intloopcounter (x:bool) returns (out:bool); |
10 |
var time: int; |
11 |
let |
12 |
time = 0 -> if pre(time) = 3 then 0 |
13 |
else pre time - 1; |
14 |
out = (time = 2); |
15 |
tel |
16 |
node top (x:bool) returns (OK:bool); |
17 |
var b,d:bool; |
18 |
let |
19 |
b = greycounter(x); |
20 |
d = intloopcounter(x); |
21 |
OK = b = d; |
22 |
--%MAIN; |
23 |
--%PROPERTY OK; |
24 |
tel |