Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / stalmark.lus @ 2d37a1e1

History | View | Annotate | Download (332 Bytes)

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

    
13
--%PROPERTY OK;
14
tel