CristalCaveGem » LustreC » Lustrec-Tests

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

var a,b:bool;

let

  a = false -> not pre(b);

  b = false -> pre(a);

  out = a and b;

tel

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

var time: int;

let

  time = 0 -> if pre(time) = 3 then 0

            else pre time - 1;

  out = (time = 2);

tel

--@ ensures OK;

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

var b,d:bool;

let

  b = greycounter(x);

  d = intloopcounter(x);

  OK = b = d;

  --%MAIN;

  --%PROPERTY  OK;

tel