lustrec/test/src/kind_fmcad08/misc/_6counter2.lus @ 3e36d4e0
| 1 | 0cbf0839 | ploc | -- 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 | 3e36d4e0 | ploc | --@ ensures OK;
|
| 5 | 0cbf0839 | ploc | 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
|