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 |