CristalCaveGem » LustreC

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

let

    First = X -> pre First;

tel

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

let

    Sofar = X -> X and pre Sofar;

tel

node excludes8( X1, X2, X3, X4, X5, X6, X7, X8 : bool ) returns ( excludes : bool );

let

    excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or

                  X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or

              not X1 and     X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or

              not X1 and not X2 and     X3 and not X4 and not X5 and not X6 and not X7 and not X8 or

              not X1 and not X2 and not X3 and     X4 and not X5 and not X6 and not X7 and not X8 or

              not X1 and not X2 and not X3 and not X4 and     X5 and not X6 and not X7 and not X8 or

              not X1 and not X2 and not X3 and not X4 and not X5 and     X6 and not X7 and not X8 or

              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and     X7 and not X8 or

              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and     X8;

tel

node firefly(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) 

	returns(invalid, dirty, exclusive, shared : int);

var

	garde1, garde2, garde3, garde4, garde5, garde6, garde7, garde8 : bool;

	mem_invalid : int;

let

--	assert #(e1, e2, e3, e4, e5, e6, e7, e8);

--	assert i_invalid > 0;

	mem_invalid = i_invalid -> pre mem_invalid;

	garde1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 ;

	garde2 = pre invalid>=1 and pre dirty>=1;

	garde3 = pre invalid>=1 and pre shared+pre exclusive>=1;

	garde4 = pre exclusive>=1;

	garde5 = pre shared=1;

	garde6 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0;

	garde7 = pre invalid>=1 and pre dirty>=1;

	garde8 = pre invalid>=1 and pre shared+pre exclusive>=1;

	invalid = mem_invalid ->

	if(e1) then if(garde1) then pre invalid-1 else pre invalid else

	if(e2) then if(garde2) then pre invalid-1 else pre invalid else

	if(e3) then if(garde3) then pre invalid-1 else pre invalid else

	if(e6) then if(garde6) then pre invalid-1 else pre invalid else

	if(e7) then if(garde7) then pre invalid-1 else pre invalid else

	if(e8) then if(garde8) then pre invalid-1 else pre invalid else

	pre invalid;

	dirty = 0 -> 

	if(e2) then if(garde2) then pre dirty-1 else pre dirty else

	if(e4) then if(garde4) then pre dirty+1 else pre dirty else

	if(e6) then if(garde6) then 1 else pre dirty else

	if(e7) then if(garde7) then pre dirty-1 else pre dirty else

	pre dirty;

	exclusive = 0 -> 

	if(e1) then if(garde1) then pre exclusive+1 else pre exclusive else

	if(e3) then if(garde3) then 0 else pre exclusive else 

	if(e4) then if(garde4) then pre exclusive-1 else pre exclusive else

	if(e5) then if(garde5) then pre exclusive+1 else pre exclusive else

	if(e8) then if(garde8) then 0 else pre exclusive else

	pre exclusive;

	shared = 0 ->

	if(e2) then if(garde2) then pre shared+2 else pre shared else

	if(e3) then if(garde3) then pre shared + pre exclusive + 1 else pre shared else

	if(e5) then if(garde5) then pre 0 else pre shared else

	if(e7) then if(garde7) then pre shared+2 else pre shared else

	if(e8) then if(garde8) then pre shared + pre exclusive + 1 else pre shared else

	pre shared;

tel

node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) 

	returns( OK : bool );

    var invalid, dirty, exclusive, shared : int;

        env : bool;

let

    ( invalid, dirty, exclusive, shared ) =

        firefly( e1, e2, e3, e4, e5, e6, e7, e8, i_invalid );

    env = Sofar( excludes8( e1, e2, e3, e4, e5, e6, e7, e8 ) and

                 i_invalid >= 0 );

    OK = env => invalid + dirty + exclusive + shared = First( i_invalid );

    --%PROPERTY OK=true;

    --%MAIN;

tel