model MESI {

var   modified, exclusive, shared, invalid;

states normal;


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

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

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

}

strategy s1 {

setMaxState(0);
setMaxAcc(100);


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

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

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

	
}