lustrec-tests/regression_tests/lustre_files/success/kind_fmcad08/misc/stalmark_e7_27.lus @ 2d37a1e1
| 1 |
node top (x:bool) returns (OK:bool); |
|---|---|
| 2 |
--@ contract guarantees OK;
|
| 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 and 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 |
--%PROPERTY OK;
|
| 14 |
tel
|