CristalCaveGem » LustreC

--

-- Source: Koen Classen

--

-- given

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

let

  Y = (true -> pre Y) and X;

tel

-- assignment other

node Store( Delta : int ) returns ( Total : int );

var Prev : int;

let

  Prev  = 0 -> pre Total;

  Total = if Delta < 0 and Prev > 0  then Prev+Delta

     else if Delta > 0 and Prev < 10 then Prev+Delta

     else Prev;

tel

--@ ensures OK;

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

var Total : int;

let

  Total = Store( Delta );

  OK = Sofar( -1 <= Delta and Delta <= 1 ) => 0 <= Total and Total <= 20; 

--!k:2;

--!PROPERTY: OK=true;

  --%MAIN;

tel