--- MOESI CACHE COHERENCE PROTOCOL
--- Last version: May 16, 2000

var  invalid,modified,exclusive,owned,shared: discrete;  	
     p : parameter;

automaton p
synclabs : ;

initially ss & True;
           
loc ss : while invalid >= 0 & modified >=0 & shared >= 0 & owned >= 0 & exclusive >=0 wait {} 
--
-- READ HIT
--
         when 
           modified+shared+exclusive+owned >=1
         do {} goto ss;
-- 
-- READ MISS
--
         when 
           invalid >= 1 
         do { 
	      invalid'=invalid-1,
              shared'=shared+exclusive+1,
	      owned'=owned+modified,
              modified'=0,
              exclusive'=0
             } 
	 goto ss;
--
-- WRITE HIT
--           
         when 
           modified >=1
         do {} goto ss;

         when 
           exclusive >= 1
         do { 
	      modified'=modified+1,
              exclusive'=exclusive-1 
	    } 
	 goto ss;
         when 
           shared+owned >= 1 
         do { 
	      shared'=0,
	      owned'=0,
              invalid'=invalid+owned+modified+exclusive+shared-1,
              exclusive'=1,
              modified'=0
             } 
         goto ss;
--
-- WRITE MISS
--
         when 
           invalid >= 1 
         do { 
	      invalid'=owned+exclusive+modified+invalid+shared-1,
              exclusive'=1,
              shared'=0,
              modified'=0,
	      owned'=0 
	    } 
         goto ss; 
--
-- REPLACEMENT
--
         when 
           modified >=1 
         do { invalid'=invalid+1,modified'=modified-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;
	 when 
           owned >=1
         do { invalid'=invalid+1,owned'=owned-1 } goto ss;
end

var 
   init_reg, final_reg, final_reg1, final_reg2, final_reg3, final_reg4, reached: region;

init_reg  := invalid >=1 & exclusive = 0 & shared = 0 & owned = 0 & modified = 0;
final_reg1 := exclusive+owned+shared >=1 & modified >= 1;
final_reg2 := shared+owned >= 1          & exclusive>= 1;
final_reg3 := modified  >=  2;
final_reg4 := exclusive >= 2;

final_reg  := final_reg1 | final_reg2 | final_reg3 | final_reg4;
  
reached:= reach backward from final_reg endreach;

 if empty(reached & init_reg)
  then print reached;
       prints "=================================== ";
       prints "SAFETY HOLD!";
       prints "=================================== ";
  else print reached;
       prints " ";
       prints "SAFETY DOES NOT HOLD!";
endif;