lustrec/tests/misc/stalmark_e7_27_e7_31.lus @ 105b3645
| 1 |
--@ ensures OK;
|
|---|---|
| 2 |
node top (x:bool) returns (OK:bool); |
| 3 |
var a,b,c:bool; |
| 4 |
let
|
| 5 |
a = true -> pre(c); |
| 6 |
b = false -> pre(a); |
| 7 |
c = false -> pre(b); |
| 8 |
OK = ((not a or not b or c) or |
| 9 |
(not a and b and not c) or |
| 10 |
(a and not b and not c) or |
| 11 |
(a and b and c)) and not (a and b and c); |
| 12 |
--%MAIN;
|
| 13 |
--!k:4;
|
| 14 |
--!PROPERTY: OK;
|
| 15 |
tel
|