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 |