CristalCaveGem » LustreC » Lustrec-Tests

node First( X : int ) returns ( First : int );

let

    First = X -> pre First;

tel

node FirstB( X : bool ) returns ( First : bool );

let

    First = X -> pre First;

tel

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

let

    Sofar = X -> X and pre Sofar;

tel

node excludes3( X1, X2, X3 : bool ) returns ( excludes : bool );

let

    excludes = not ( X1 and X2 or X1 and X3 or X2 and X3 );

tel

node PRODUCER_CONSUMMER(etat1, etat2, etat3 : bool; a_init : int

) returns(i, b, a, o1, o2 : int);

var

	garde1, garde2, garde3 : bool;

let

	garde1 = pre i >= 1;

	garde2 = pre b >= 1;

	garde3 = pre b >= 1;

	i = a ->

	if(etat1) then if(garde1) then pre i -1 else pre i else 

	pre i;

	b = 0 -> 

	if(etat1) then if(garde1) then pre b+1 else pre b else 

	if(etat2) then if(garde2) then pre b-1 else pre b else 

	if(garde3) then pre b-1 else pre b;

	a = a_init -> pre a;

	o1 = 0 -> 

	if(etat2) then if(garde2) then pre o1+1 else pre o1 else 

	pre o1;

	o2 = 0 -> 

	if(etat3) then if(garde3) then pre o2+1 else pre o2 else

	pre o2;

tel

node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool );

--@ contract guarantees OK;

    var i, b, a, o1, o2 : int;

        env : bool;

let

   ( i, b, a, o1, o2 ) = PRODUCER_CONSUMMER(etat1, etat2, etat3, a_init );

   env = Sofar( excludes3( etat1, etat2, etat3 ) or

                not ( etat1 or etat2 or etat3 ) ) and

         FirstB( not ( etat1 or etat2 or etat3 ) ) and

         First( a_init ) > 0;

   OK = env => o1 + o2 <= First( a );

  --%MAIN;

  --%PROPERTY  OK=true;

tel