model ILLINOIS {

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 := 
		invalid'=invalid+shared-1,
		shared'=0,
		dirty'=dirty+1
	;
};

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

transition r7  :=  {
	from :=normal;
	to:=normal;
	guard :=
		dirty>=1
	;
	action := 
		dirty'=dirty-1,
		invalid'=invalid+1
	;
};

transition r8  :=  {
	from :=normal;
	to:=normal;
	guard :=
		shared>=1
	;
	action := 
		invalid'=invalid+1,
		shared'=shared-1
	;
};

transition r9  :=  {
	from :=normal;
	to:=normal;
	guard :=
		exclusive>=1
	;
	action := 
		exclusive'=exclusive-1,
		invalid'=invalid+1
	;
};

}


strategy s1 {

setMaxState(0);
setMaxAcc(100);


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

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

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

	
}