lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / _6counter2.lus @ 8aaf9f57
History | View | Annotate | Download (410 Bytes)
| 1 | b8dc00eb | bourbouh | -- a simple 0 to 5 boolean counter (A is LSB, C is MSB) |
|---|---|---|---|
| 2 | -- invalid property is that it should never reach 5 or 7 |
||
| 3 | |||
| 4 | --@ ensures OK; |
||
| 5 | node top (x:bool) returns (OK:bool); |
||
| 6 | var a,b,c:bool; |
||
| 7 | let |
||
| 8 | a = false -> not pre(a); |
||
| 9 | b = false -> (not pre(c) and not pre(b) and pre(a)) or |
||
| 10 | (pre(b) and not pre(a)); |
||
| 11 | c = false -> (pre(c) and not pre(a)) or (pre(b) and pre(a)); |
||
| 12 | OK= (c and a); |
||
| 13 | --%PROPERTY OK; |
||
| 14 | tel |