model SYNAPSE {

var   invalid, valid, dirty;

states normal;


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

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

strategy s1 {

setMaxState(0);
setMaxAcc(100);


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

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

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

	
}