--- MOESI CACHE COHERENCE PROTOCOL [Delzanno 2003]
--- VALERIO 11-07-07 - MP 23/11/07


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
-- rh
         when 
           modified+owned+exclusive+shared >= 1 
         do { } 
	 		goto ss;

-- 
-- READ MISS
-- rm
         when 
           invalid >= 1 
         do { 
	    invalid'=invalid-1,
            shared'=shared+exclusive+1,
	    owned'=owned+modified,
            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+owned >= 1 
         do { 
	    shared'=0,
	    owned'=0,
            invalid'=invalid+owned+modified+exclusive+shared-1,
            exclusive'=1,
            modified'=0
            } 
         goto ss;
--
-- WRITE MISS
-- wm
         when 
           invalid >= 1 
         do { 
	    invalid'=owned+exclusive+modified+invalid+shared-1,
            exclusive'=1,
            shared'=0,
            modified'=0,
	    owned'=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 & 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 prints "Target not reached (safety holds!)";
       print reached;
  else prints "Target reached (safety does not hold!)";

endif;