--- DRAGON CACHE COHERENCE PROTOCOL [Delzanno 2003]

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


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

automaton p
synclabs : ;

initially ss & True;
           

loc ss : while invalid >= 0 & 
         dirty >=0 & 
         shared >= 0 & 
         exclusive >=0 & 
         shared_dirty>=0  wait {} 
--
-- READ HIT
-- rh

         when
           dirty+shared+exclusive+shared_dirty >= 1
         do { } 
			goto ss;
         
--
-- READ MISS
-- rm1
         when 
           invalid >= 1 & 
           dirty =0 & 
           shared = 0 & 
           exclusive =0  & 
           shared_dirty=0
         do { 
	      	invalid'=invalid-1,
            exclusive'=exclusive+1 
	 			} 
			goto ss;
-- rm2
        when 
           invalid >= 1 & dirty+shared+exclusive+shared_dirty >= 1  
         do { 
	      	invalid'=invalid-1,
            dirty'=0,
            shared_dirty'=shared_dirty+dirty,
            shared'=shared+exclusive+1,
            exclusive'=0 
	 			} 
			goto ss;
--
-- WRITE HIT
--  wh2         
         when 
           exclusive >= 1
         do { 
	     		dirty'=dirty+1,
            exclusive'=exclusive-1 
	 		} goto ss;
-- wh3
         when 
           shared_dirty = 1 & shared =0   
          do { 
	       		shared_dirty'=0, 
               dirty'=dirty+1
	 		} goto ss;
-- wh4
         when 
            shared_dirty = 0 & shared =1   
          do { 
	        shared'=0, 
                dirty'=dirty+1
	 		} goto ss;
-- wh5
         when
            shared_dirty+shared >= 2 
         do {  
	        shared'=shared+shared_dirty-1, 
            	shared_dirty'=1
	 		} goto ss;
-- wh1
         when
            dirty >= 1
         do { } goto ss;

--
-- WRITE MISS
-- wm1
         when 
           invalid >= 1 & 
           dirty =0 & 
           shared = 0 & 
           exclusive =0  & 
           shared_dirty=0
         do { 
	      	invalid'=invalid-1,
              	dirty'=dirty+1 
	 		} goto ss;
-- wm2
         when 
           invalid >= 1 & dirty+shared+exclusive+shared_dirty >= 1  
         do { 
	      		invalid'=invalid-1,
              	shared'=shared+exclusive+shared_dirty+dirty,
              	exclusive'=0,
              	dirty'=0,
              	shared_dirty'=1
	 		} goto ss;

end

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

init_reg    := invalid >=1 & exclusive = 0 & shared = 0 & shared_dirty=0 & dirty = 0;
final_reg1 := shared+exclusive+shared_dirty >= 1 & dirty >= 1 ;
final_reg2 := shared+shared_dirty >= 1 & exclusive >=  1;
final_reg3 := dirty >= 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;



-- reached:= reach forward from init_reg endreach;

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

-- endif;