--- SYNAPSE CACHE COHERENCE PROTOCOL
--- [Delzanno 2003]

--- VS 10/07/07 - MP 22/11/07


var  invalid,valid,dirty: discrete;  	

automaton p
synclabs : ;

initially ss & True;
           

loc ss : while invalid >= 0 & dirty >=0 & valid >= 0  wait {} 
--
-- READ HIT
-- rh1
         when 
           dirty >= 1 
         do {} 
	 		goto ss;
-- rh2
         when 
           valid >= 1 
         do {} 
	 		goto ss;

-- 
-- READ MISS
-- rm
         when 
           invalid >= 1 
         do { 
	      	invalid'=invalid+dirty-1,
            valid'=valid+1,
            dirty'=0
            } 
	 		goto ss;

--
-- WRITE HIT
-- wh1         
         when 
           dirty >=1
         do {} 
	 goto ss;
-- wh2
         when 
           valid >=1
         do {
	      dirty'=1,
	      valid'=0,
	      invalid'=invalid+dirty+valid-1
	    } 
	 goto ss;
         
--
-- WRITE MISS
-- wm          
         when 
           invalid >=1
         do {
	      dirty'=1,
	      valid'=0,
	      invalid'=invalid+dirty+valid-1
	    } 
	 goto ss;      
end

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

init_reg   := invalid >=1 &  valid = 0 & dirty = 0;
final_reg1 := valid >= 1 & dirty >= 1 ;
final_reg2 := dirty >= 2;
final_reg  := final_reg1 | final_reg2;

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;