Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (441 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 top (x:bool) returns (OK: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
  OK = true -> pre(true -> pre b) = not b;
12
--  --%PROPERTY not (c and b);
13
--%PROPERTY OK;
14
tel