Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (316 Bytes)

1
node top (x:bool) returns (OK:bool);
2
var a,b,c:bool;
3
let
4
  a = true -> pre(c);
5
  b = false -> pre(a);
6
  c = false -> pre(b);
7
  OK = ((not a or not b and c) and 
8
        (not a and b and not c) or 
9
        (a and not b and not c) or 
10
        (a and b and c)) and not (a and b and c);
11
  --%MAIN;
12
  --%PROPERTY OK;
13
tel