CristalCaveGem » LustreC » Lustrec-Tests

-- a simple 0 to 5 boolean counter (A is LSB, C is MSB)

-- property is that it should never reach 6 or 7

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)) or (pre(b) and pre(a));

  out = a and c;

tel

-- this resets to 1, not 0

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

var time:int;

let

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

              else pre time + 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);

  --%PROPERTY OK;

tel