Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / misc / _6counter2.lus @ 65f71d05

History | View | Annotate | Download (410 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
--@ ensures OK;
5
node top (x:bool) returns (OK:bool);
6
var a,b,c:bool;
7
let
8
  a = false -> not pre(a);
9
  b = false -> (not pre(c) and not pre(b) and pre(a)) or 
10
           (pre(b) and not pre(a));
11
  c = false -> (pre(c) and not pre(a)) or (pre(b) and pre(a));
12
  OK= (c and a);
13
  --%PROPERTY OK;
14
tel