--- ILLINOIS CACHE COHERENCE PROTOCOL

var  invalid,dirty,exclusive,shared: discrete;  	
     p : parameter;

automaton p
synclabs : ;

initially ss & True;
           

loc ss : while invalid >= 0 & 
               dirty >=0 & 
               shared >= 0 & 
               exclusive >=0  wait {} 
--
-- READ HIT
--
         when 
           dirty+shared+exclusive >= 1 
         do {} goto ss;
-- 
-- READ MISS
--
         when 
           invalid >= 1 & dirty =0 & shared = 0 & exclusive =0
         do { invalid'=invalid-1,exclusive'=exclusive+1 } goto ss;
         when 
           invalid >= 1 & dirty >=1 
         do { invalid'=invalid-1,dirty'=dirty-1,shared'=shared+2 } goto ss;
         when 
           invalid >= 1 & shared+exclusive >=1
         do { invalid'=invalid-1,shared'=shared+exclusive+1,exclusive'=0  } 
         goto ss;
--
-- dirty=0?? before?
--
-- WRITE HIT
--           
         when 
           dirty >=1 
         do {} goto ss;
         when 
           exclusive >= 1
         do { dirty'=dirty+1,exclusive'=exclusive-1 } goto ss;
         when 
           shared >= 1
         do { shared'=0,invalid'=invalid+shared-1,dirty'=dirty+1}
goto ss;
--
-- WRITE MISS
--
         when 
           invalid >= 1
         do { invalid'=exclusive+dirty+invalid+shared-1,
              exclusive'=0,
              shared'=0,
              dirty'=1 } goto ss; 
--
-- REPLACEMEN
--
         when 
           dirty >=1 
         do { invalid'=invalid+1,dirty'=dirty-1 } goto ss;
         when 
           shared >= 1 
         do { invalid'=invalid+1,shared'=shared-1 } goto ss;
         when 
           exclusive >=1
         do { invalid'=invalid+1,exclusive'=exclusive-1 } goto ss;
end

var 
   init_reg, final_reg1, final_reg2, final_reg, reached, old, new, Aux
: region;

init_reg  := loc[p]=ss & invalid >=1 & exclusive = 0 & shared = 0 & dirty = 0;
final_reg1 := loc[p]=ss &  shared >= 0 & dirty >= 2;
final_reg2 := loc[p]=ss &  shared >= 1 & dirty >= 1 ;
final_reg := final_reg1 | final_reg2;

reached:= reach backward from final_reg endreach;
--   reached:= reach forward  from init_reg  endreach;

 if empty(reached & init_reg)
--if empty(reached & final_reg)
  then prints "SAFE";
---       print reached;
  else prints "ERROR";

endif;