lustrec / test / src / kind_fmcad08 / misc / stalmark_e7_27_e7_31.lus @ 22fe1c93
History | View | Annotate | Download (315 Bytes)
1 |
node top (x:bool) returns (OK:bool); |
---|---|
2 |
var a,b,c:bool; |
3 |
let |
4 |
a = true -> pre(c); |
5 |
b = false -> pre(a); |
6 |
c = false -> pre(b); |
7 |
OK = ((not a or not b or c) or |
8 |
(not a and b and not c) or |
9 |
(a and not b and not c) or |
10 |
(a and b and c)) and not (a and b and c); |
11 |
--%MAIN; |
12 |
--%PROPERTY OK; |
13 |
tel |