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