CristalCaveGem » LustreC

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

let

    Sofar = X -> X or pre Sofar;

tel

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

let

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

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

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

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

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

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

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

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

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

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

tel

node illinois(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int)

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

var

   g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool;

let

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

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

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

   g4 = pre exclusive>=1;

   g5 = pre shared>=1;

   g6 = pre invalid>=1;

   g7 = pre dirty>=1;

   g8 = pre shared>=1;

   g9 = pre exclusive>=1;

   invalid = (if(init_invalid>0) then init_invalid else 1-init_invalid) ->

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

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

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

   if(e5) then if(g5) then pre invalid+pre shared-1 else pre invalid else 

   if(e6) then if(g6) then pre invalid+pre dirty+pre shared+pre exclusive-1 else pre invalid else 

   if(e7) then if(g7) then pre invalid+1 else pre invalid else 

   if(e8) then if(g8) then pre invalid+1 else pre invalid else 

   if(e9) then if(g9) then pre invalid+1 else pre invalid else 

   pre invalid;

   dirty = 0 -> 

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

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

   if(e5) then if(g5) then pre dirty+1 else pre dirty else 

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

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

   pre dirty;

   exclusive = 0 -> 

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

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

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

   if(e6) then if(g6) then 0 else pre exclusive else 

   if(e9) then if(g9) then pre exclusive-1 else pre exclusive else 

   pre exclusive;

   shared = 0 -> 

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

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

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

   if(e6) then if(g6) then 0 else pre shared else 

   if(e8) then if(g8) then pre shared-1 else pre shared else 

   pre shared;

tel

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

returns( OK : bool);

    var invalid, dirty, exclusive, shared : int;

        env : bool;

let

    ( invalid, dirty, exclusive, shared ) =

        illinois( e1, e2, e3, e4, e5, e6, e7, e8, e9, init_invalid );

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

                 init_invalid > 0 );

    OK = env => dirty >= 0;

  --%MAIN;

  --%PROPERTY  OK=true;

tel