model BERKELEY {

var   invalid, unowned,nonexclusive,exclusive;

states normal;


transition r1  :=  {
	from :=normal;
	to:=normal;
	guard :=
		invalid>=1
	;
	action :=  
		nonexclusive'=nonexclusive+exclusive,
	      	exclusive'=0,
		invalid'=invalid-1,
		unowned'=unowned+1
	;
};  	      

transition r2  :=  {
	from :=normal;
	to:=normal;
	guard :=
           	nonexclusive + unowned >=1
	;
	action := 
		invalid'=invalid + unowned + nonexclusive-1,
		exclusive'=exclusive+1,
		unowned'=0,
		nonexclusive'=0     	
	;
};

transition r3  :=  {
	from :=normal;
	to:=normal;
	guard :=
		invalid>=1 
	;
	action := 
		unowned'=0,
		nonexclusive'=0,
		exclusive'=1,
		invalid'=invalid+unowned+exclusive+nonexclusive-1
	;
};

}


strategy s1 {

setMaxState(0);
setMaxAcc(100);


Region init :=
	{state=normal && exclusive=0 && nonexclusive=0 && unowned=0 && invalid>0};

Transitions t := {r1,r2,r3};

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

	
}