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