--- FIREFLY CACHE COHERENCE PROTOCOL
--- Last modified: May 16, 2000

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

automaton p
synclabs : ;

initially ss & True;
           

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

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


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

init_reg   := invalid >=1 &  exclusive=0 & shared = 0 & dirty = 0;
final_reg1 := dirty >= 2;
final_reg2 := exclusive >= 2;
final_reg3 := shared+exclusive >= 1 & dirty >= 1 ;
final_reg  := final_reg1 | final_reg2 | final_reg3;

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;