Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / misc / twisted_counters.lus @ 22fe1c93

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