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

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

automaton p
synclabs : ;

initially ss & True;
           
loc ss : while invalid >= 0 & modified >=0 & shared >= 0 & exclusive >=0 wait {} 
--
-- READ HIT
--
         when 
           modified+shared+exclusive >=1
         do {} goto ss;
-- 
-- READ MISS
--
         when 
           invalid >= 1 
         do { 
	      invalid'=invalid-1,
              shared'=shared+exclusive+modified+1,
              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 >= 1 
         do { 
	      shared'=0,
              invalid'=invalid+modified+exclusive+shared-1,
              exclusive'=1,
              modified'=0
             } 
         goto ss;
--
-- WRITE MISS
--
         when 
           invalid >= 1 
         do { 
	      invalid'=exclusive+modified+invalid+shared-1,
              exclusive'=1,
              shared'=0,
              modified'=0 
	    } 
         goto ss; 
--
-- REPLACEMENT
--
         when 
           invalid >= 0 & modified >=1 & shared >= 0 & exclusive >=0
         do { invalid'=invalid+1,modified'=modified-1 } goto ss;
         when 
           invalid >= 0 & modified >=0 & shared >= 1 & exclusive >=0
         do { invalid'=invalid+1,shared'=shared-1 } goto ss;
         when 
           invalid >= 0 & modified >=0 & shared >= 0 & exclusive >=1
         do { invalid'=invalid+1,exclusive'=exclusive-1 } goto ss;
end

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

init_reg  := invalid >=1 & exclusive = 0 & shared = 0 & modified = 0;
final_reg1 := modified >= 2;
final_reg2 := shared >= 1 & modified >= 1 ;
final_reg  := final_reg1 | final_reg2;
  
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;