CristalCaveGem » LustreC

node bool6 (x:bool) returns (out:bool);

var a,b,c: bool;

let

  a = false -> not pre(a);

  b = false -> (not pre(c) and not pre(b) and pre(a)) or

           (pre(b) and not pre(a));

  c = false -> (pre(c) and not pre(a)) and (pre(b) and pre(a));

  out = a and c;

tel

node int6I (x:bool) returns (out:bool);

var time:int;

let

  time = 0 -> if pre time = 5 then 1

              else pre time -1+ 1;

  out = time = 5;

tel

--@ ensures OK;

node top (x:bool) returns (OK:bool);

var a,b:bool;

let

  OK = a=b;

  a = int6I(x);

  b = bool6(x);

--!k:2;

--!PROPERTY: OK;

tel