CristalCaveGem » LustreC » Lustrec-Tests

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

let

    Sofar = X -> X and pre Sofar;

tel

--const N=3;

node controleur(nB,nS:int) returns (diff:int; avance,retard:bool);

let

  diff = nB-nS;

  avance = false ->

	if not (pre avance) then diff >= 10 else diff > 0;

  retard = false ->

	if not (pre retard) then (diff <= -10) else (diff < 0);

tel

node hypothese(B,S,avance,retard:bool) returns (ok:bool);

var c:int;

let

  ok = true ->

	(if pre retard then not S else true) and

	(if pre c >= 9 then not B else true);

  c = 0 ->

	if pre avance and avance then

		if B then pre c + 1 else pre c

	else 

		0;

tel

node main(B0, B1 : bool; S : bool) 

returns ( ast: bool; nB0, nB1 : int; nS : int;

          diff0, diff1:int;

          avance0, avance1, retard0, retard1 : bool );

var H0, H1:bool;

let

  nB0 = 0 -> if B0 then pre nB0 + 1 else pre nB0;

  nB1 = 0 -> if B1 then pre nB1 + 1 else pre nB1;

  nS = 0 -> if S then pre nS + 1 else pre nS;

  H0 = hypothese(B0,S,avance0,retard0);

  H1 = hypothese(B1,S,avance1,retard1);

  (diff0,avance0,retard0) = controleur(nB0,nS);

  (diff1,avance1,retard1) = controleur(nB1,nS);

  ast = H0 and H1;

tel

-- Not provable?

node top(B0,B1 : bool; S : bool) 

returns (OK:bool);

--@ contract guarantees OK;

var nB0,nB1 : int;

    nS : int;

    diff0,diff1:int;

    avance0,avance1,retard0,retard1 : bool;

    ast:bool;

let

  (ast,nB0,nB1,nS,diff0,diff1,avance0,avance1,retard0,retard1) = main(B0,B1,S);

  OK = Sofar( ast )

       => true -> (((pre(nB0) - pre (nB1)) <= 30) and

                  ((pre(nB1) - pre (nB0)) <= 30));

    --%PROPERTY OK=true;

    --%MAIN;

tel