lustrec / test / src / kind_fmcad08 / misc / twisted_counters.lus @ 0cbf0839
History | View | Annotate | Download (882 Bytes)
1 |
|
---|---|
2 |
|
3 |
--A messed up counter: |
4 |
--x = 0: 0,1,2,3,4,3,4,... |
5 |
--x = 1: 0,1,2,3,4,5,2,3,4,5,... |
6 |
--A is MSB, C is LSB |
7 |
--property: never reach state 6 or 7 |
8 |
|
9 |
node loop6counter (x:bool) returns (out:bool); |
10 |
var a,b,c:bool; |
11 |
let |
12 |
a = false -> (pre(b) and pre(c)) or |
13 |
(pre(x) and pre(a) and not pre(c)); |
14 |
b = false -> (not pre(b) and pre(c)) or |
15 |
(pre(b) and not pre(c)) or |
16 |
(not pre(x) and pre(a)); |
17 |
c = false -> not pre(c); |
18 |
out = a and c; |
19 |
tel |
20 |
|
21 |
node intloop6counter (x:bool) returns (out:bool); |
22 |
var time: int; |
23 |
let |
24 |
time = 0 -> if pre(time) = 5 then 2 |
25 |
else if pre(time) = 4 then |
26 |
if not pre(x) then 3 |
27 |
else 5 |
28 |
else pre time + 1; |
29 |
out = (time = 5); |
30 |
tel |
31 |
|
32 |
|
33 |
node top (x:bool) returns (OK:bool); |
34 |
var b,d:bool; |
35 |
let |
36 |
b = loop6counter(x); |
37 |
d = intloop6counter(x); |
38 |
OK = not x or b = d; |
39 |
--%PROPERTY OK; |
40 |
tel |