CristalCaveGem » LustreC » Lustrec-Tests

--

-- Source Bertrand Jeannet, NBAC tutorial

--

node Sofar( X : bool ) returns ( Sofar : bool );

let

    Sofar = X -> X and pre Sofar;

tel

node Environment(diff: int; plus,minus: bool) returns (ok: bool);

let

  ok = (-4 <= diff and diff <= 4) and 

     (if (true -> pre plus) then diff >= 1 else true) and

     (if (false -> pre minus) then diff <= -1 else true);

tel

node Controller(diff: int) returns (speed: int; plus,minus: bool);

let

  speed = 0 -> pre(speed)+diff;

  plus = speed <= 9;

  minus = speed >= 11;

tel

node Property(speed: int) returns (ok: bool);

var cpt: int;

    acceptable: bool;

let

  acceptable = 8 <= speed and speed <= 12;

  cpt = 0 -> if acceptable then 0 else pre(cpt)+1;

  ok = true -> (pre cpt<=7);

tel

node top(diff:int) returns (OK: bool);

--@ contract guarantees OK;

var speed: int; 

    plus,minus,realistic: bool;

let

  (speed,plus,minus) = Controller(diff);

  realistic =  Environment(diff,plus,minus);

  OK = Sofar( realistic and 0 <= speed and speed < 16 ) => Property(speed);

  --%PROPERTY OK=true;

  --%MAIN;

tel