model ttp {


var n, cf, d, df, cp, d1, c1, d0, c0; 
//cw=n at the beginning

states e1,e2,e3,e4;



transition r2 := {
	from :=e1;
	to:=e1;
	guard :=
		d<n 
	;
	action := 
		d'=d+1, 
		cp'=cp+1  
	;
};

transition r3 := {
		from := e1;
		to:= e1;
		guard := 
			df<cf	
		;
		action :=
			df'=df+1,
			cp'=cp+1
		;
};


transition r4 := {
		from := e1;
		to:= e1	;
		guard := 
			cp=n	
		;
		action :=
			cp'=0,
			d'=0,
			df'=0
		;
};

transition r5 := {
		from :=e1;
		to:= e2;
		guard :=
			c1>=1 && c0>=0 && c1+c0=n	
		;
		action :=
			d1'=1,
			d0'=0,
			df'=0,
			cp'=1
		;
};

transition r6 := {
		from := e2	;
		to:=e2	;
		guard :=
			df<cf			
		;
		action :=
			df'=df+1,
			cp'=cp+1
		;
};

transition r7 := {
		from :=e2	;
		to:=e2	;
		guard :=
			d1<c1 && c1+c0-2*d0>0
		;
		action :=
			d1'=d1+1,
			cp'=cp+1
		;
};

transition r8 := {
		from :=	e2;
		to:=e2	;
		guard :=
			d1<c1 && c1+c0-2*d0<=0				
		;
		action :=
			c1'=c1-1,
			df'=df+1,
			cf'=cf+1,
			cp'=cp+1
		;
};

transition r9 := {
		from :=e2	;
		to:=e2	;
		guard :=
			d0<c0 && c1+c0-2*d1>0
		;
		action :=
			d0'=d0+1,
			cp'=cp+1			
		;
};

transition r10 := {
		from :=e2	;
		to:=e2	;
		guard :=
			d0<c0 && c1+c0-2*d1<=0						
		;
		action :=
			c0'=c0-1,
			df'=df+1,
			cf'=cf+1,
			cp'=cp+1			
		;
};

transition r11 := {
		from :=e2	;
		to:=e3	;
		guard :=
			cp=n	
		;
		action :=
			d1'=0,
			d0'=0,
			df'=0,
			cp'=0
		;
};

transition r12 := {
		from :=e3	;
		to:=e3	;
		guard :=
			df<cf
		;
		action :=
			df'=df+1,
			cp'=cp+1
		;
};


transition r13 := {
		from :=e3	;
		to:=e3	;
		guard :=
			d1<c1 && c1>c0	
		;
		action :=
			d1'=d1+1,
			cp'=cp+1
		;
};


transition r14 := {
		from :=e3	;
		to:=e3	;
		guard :=
			d1<c1 && c1<=c0	
		;
		action :=
			c1'=c1-1,
			cf'=cf+1,
			df'=df+1,
			cp'=cp+1
		;
};


transition r15 := {
		from :=e3	;
		to:=e3	;
		guard :=
			d0<c0 && c0>c1	
		;
		action :=
			d0'=d0+1,
			cp'=cp+1
		;
};


transition r16 := {
		from :=e3	;
		to:=e3	;
		guard :=
			d0<c0 && c0 <=c1	
		;
		action :=
			c0'=c0-1,
			cf'=cf+1,
			df'=df+1,
			cp'=cp+1			
		;
};


transition r17 := {
		from :=e3	;
		to:=e3	;
		guard :=
			cp=n && !(c1=0) && !(c0=0)	
		;
		action :=
			d1'=0,
			d0'=0,
			df'=0,
			cp'=0
		;
};


transition r18 := {
		from :=e3	;
		to:=e4	;
		guard :=
			cp=n	
		;
		action := 
			cp'=cp
		;
};

}


strategy s1 {

setMaxState(0);
setMaxAcc(100);


Region init :=
	{cf=0 && n>=0 && cp=0 && d=0 && df=0 && state=e1 && c1>=1 
	 && c0>=0 && c1+c0=n && d1=1 && d0=0 };

Transitions t1 := {r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,r15,r16,r17,r18};
Region reach := post*(init, t1);
	
}