model DRAGON {

var   invalid, dirty, exclusive, shared, shared_dirty;

states normal;


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

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


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


transition r4  := {
	from :=normal;
	to:=normal;
	guard :=
		shared_dirty=1 && shared=0
	;
	action :=
		dirty'=dirty+1,
		shared_dirty'=0
	;
};

transition r5  := {
	from :=normal;
	to:=normal;
	guard := 
		shared_dirty=0 && shared=1
	;
	action :=
		dirty'=dirty+1,
		shared'=0
	;
};

transition r6  := {
	from :=normal;
	to:=normal;
	guard :=
		shared_dirty+ shared>=2
	;
	action :=
		shared'=shared+shared_dirty-1,
		shared_dirty'=1
	;
};

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

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

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

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

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

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

}

strategy s1 {

setMaxState(0);
setMaxAcc(100);


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

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

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

	
}