CristalCaveGem » LustreC » Lustrec-Tests

-- a simple boolean ant int counter

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

node auto (x:bool) returns -- (out:bool);

 (_state: int);

let

  automaton four_states

  state One : 

  let 

 --   out = false;

    _state = 1;

  tel until true restart Two

  state Two : 

  let 

 --   out = false;

    _state = 2;

  tel until true restart Three

  state Three : 

  let 

--    out = true;

   _state = 3;

  tel until true restart Four

  state Four :

  let 

 --   out = false;

    _state = 4;

  tel until true restart One

tel

--@ ensures OK;

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

var a,b,d:bool;

    s:int;

    OK1,OK2,OK3: bool;

let

  b = greycounter(x);

  d = intloopcounter(x);

  s = auto(x);

  a = s= 3;

  OK1 = b = d;

  OK2 = b = a;

  OK3 = a = d;

  OK = OK3;

  --%PROPERTY OK;

tel

(*@ ensures open_light; *)

node auto (x:bool) returns (_state: int);

var ok: bool;

let

  automaton mini_states

  state One : 

  let 

    _state, ok = (1, false);

  tel until true restart One

  -- state Two : 

  -- let 

  --   _state, ok = (2, false);

  -- tel until true restart One

tel

node auto (x:bool) returns (ok: bool);

var bit: bool;

    coin: bool;

let

  automaton mini_states

  state Even : 

  let 

    bit = true;

  tel until true restart Odd

  state Odd : 

  let 

    bit = false;

  tel until true restart Even

  coin = true -> not pre coin;

  ok = bit = coin;

tel

node auto (x:bool) returns (ok: bool);

var bit: bool;

    coin: bool;

let

  automaton mini_states

  state Even : 

  let 

    bit = true;

  tel until true restart Odd

  state Odd : 

  let 

    bit = false;

  tel until true restart Even

  coin = true -> not pre coin;

  ok = bit = not coin;

tel

node auto (x:bool) returns (ok: bool);

var bit: bool;

    coin: bool;

let

  automaton mini_states

  state Even : 

  let 

    bit = true;

  tel until true restart Odd

  state Odd : 

  let 

    bit = false;

  tel until true restart Even

  coin = true -> not pre coin;

  ok = bit = coin;

tel