Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (673 Bytes)

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 bool6 (x:bool) returns (out:bool);
5
var a,b,c: bool;
6
let
7
  a = false -> not pre(a);
8
  b = false -> (not pre(c) and not pre(b) and pre(a)) or
9
           (pre(b) and not pre(a));
10
  c = false -> (pre(c) and not pre(a)) or (pre(b) and pre(a));
11
  out = a and c;
12
tel
13

    
14
-- this resets to 1, not 0
15
node int6I (x:bool) returns (out:bool);
16
var time:int;
17
let
18
  time = 0 -> if pre time = 5 then 1
19
              else pre time + 1;
20
  out = time = 5;
21
tel
22

    
23

    
24

    
25
node top (x:bool) returns (OK:bool);
26
var a,b:bool;
27
let
28
  OK = a=b;
29
  a = int6I(x);
30
  b = bool6(x);
31
  --%PROPERTY OK;
32
tel