Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (394 Bytes)

1
-- a simple 0 to 5 boolean counter (A is LSB, C is MSB)
2
-- invalid property is that it should never reach 5 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= (c and a);
12
  --%PROPERTY OK;
13
tel