lustrec-tests/regression_tests/lustre_files/success/kind_fmcad08/misc/_6counter.lus @ 2d37a1e1
1 |
-- a simple 0 to 5 boolean counter (A is LSB, C is MSB)
|
---|---|
2 |
-- property is that it should never reach 6 or 7
|
3 |
|
4 |
node top (x:bool) returns (OK:bool); |
5 |
--@ contract guarantees OK;
|
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 = true -> pre(true -> pre b) = not b; |
13 |
-- --%PROPERTY not (c and b);
|
14 |
--%PROPERTY OK;
|
15 |
tel
|