--- MESI CACHE COHERENCE PROTOCOL  [Delzanno 2003]
--- VS 10/07/07 - MP 23/11/2007

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
--
-- rh
     	when 
           modified+shared+exclusive >= 1
        do { } 
	 	goto ss;
         
-- 
-- READ MISS
--
-- rm
 	 when 
           invalid >= 1 
         do { 
	    invalid'=invalid-1,
            shared'=shared+exclusive+modified+1,
            modified'=0,
            exclusive'=0
            } 
	 		goto ss;
--
-- WRITE HIT
-- 
-- wh1
         when 
           modified >= 1
         do { } 
	 	 goto ss;
-- wh2          
         when 
           exclusive >= 1
         do { 
	    modified'=modified+1,
            exclusive'=exclusive-1 
	    		} 
	 		goto ss;
-- wh3
         when 
           shared >= 1 
         do { 
	    shared'=0,
            invalid'=invalid+modified+exclusive+shared-1,
            exclusive'=1,
            modified'=0
            } 
         goto ss;

--
-- WRITE MISS
--
-- wm
         when 
           invalid >= 1 
         do { 
	    invalid'=exclusive+modified+invalid+shared-1,
            exclusive'=1,
            shared'=0,
            modified'=0 
	    		} 
         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 & modified = 0;
final_reg1 := shared+exclusive >= 1 & modified >= 1 ;
final_reg2 := modified >= 2;
final_reg4 := exclusive >=2;
final_reg3 := exclusive >=1 & shared >=1;
final_reg  := final_reg1 | final_reg2 | final_reg3 | final_reg4;
  
reached:= reach backward from final_reg endreach;

 if empty(reached & init_reg)
  then prints "Target not reached (safety holds!)";
       print reached;
  else prints "Target reached (safety does not hold!)";

endif;