model FIREFLY {

var   invalid, dirty, exclusive, shared;

states normal;


transition r1 := {

	from:= normal;
	to := normal;
        guard := 
		invalid>=1 && dirty=0 && shared=0 && exclusive=0 ; 
        action :=
	      	exclusive'=exclusive+1,
		invalid'=invalid-1
	;
};  	      

transition r2 := {

	from:= normal;
	to := normal;
        guard := 
           	invalid>=1 && dirty>=1;
         action :=
		shared'=shared+2,
		invalid'=invalid-1,
		dirty'=dirty-1     	
	;
};  	  

transition r3 := {

	from:= normal;
	to := normal;
        guard := 
		invalid>=1 && shared+exclusive>=1;
         action :=
		shared'=shared+exclusive+1,
		exclusive'=0,
		invalid'=invalid-1
	;
};  	  

transition r4  := {

	from:= normal;
	to := normal;
        guard := 
		exclusive>=1;
         action :=
		dirty'=dirty+1,
		exclusive'=exclusive-1
	;
};  	  

transition r5  := {

	from:= normal;
	to := normal;
        guard := 
		shared=1;
         action :=
		exclusive'=exclusive+1,
		shared'=0
	;
};  	  
transition r6  := {

	from:= normal;
	to := normal;
        guard := 
		invalid>=1 && dirty=0 && shared=0 && exclusive=0;
         action :=
		dirty'= 1,
		invalid'=invalid-1
	;
};  	  

transition r7 := {

	from:= normal;
	to := normal;
        guard := 
		invalid>=1 && dirty>=1;
	 action :=
		shared'=shared+2,
		dirty'=dirty-1,
		invalid'=invalid-1
	;
};  	  

transition r8 := {

	from:= normal;
	to := normal;
        guard := 
		invalid>=1 && shared+exclusive>=1;
         action :=
		shared'=shared+exclusive+1,
		exclusive'=0,
		invalid'=invalid-1
	;
};
  	  
}

strategy s1 {

setMaxState(0);
setMaxAcc(100);


Region init :=
	{state=normal && exclusive=0 && shared=0 && dirty=0 && invalid>=1};

Transitions t := {r1,r2,r3,r4,r5,r6,r7,r8};

Region reach := post*(init, t);

	
}