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};
Region reach1 := post*(init, t1);

Transitions t2 := {r5};
Region reach2 :=  post*(reach1, t2);

Transitions t3 := {r6,r7,r8,r9,r10};
Region reach3 :=  post*(reach2, t3);

Transitions t4 := {r11};
Region reach4 :=  post*(reach3, t4);

Region goal1 := {state=e3 && !(c1=c0)};
boolean test1 := subSet(reach4&&{state=e3}, goal1);
if test1 then print(" property hold ");
	else print(" not safe ");
endif

Transitions t5 := {r12, r13, r14,r15,r16};
Region reach5 :=  post*(reach4, t5);

Region goal2 := {state=e3 && (cp=n && !(c1=0) && !(c0=0))};
boolean test2 := isEmpty( (reach5&&{state=e3}) && goal2);
if test2 then print(" property hold ");
	else print(" not safe ");
endif


Transitions t6 := {r17,r18};
Region reach6 :=  post*(reach5, t6);

Region goal3 := {state=e4 && (c1=0||c0=0)};
boolean test3 := subSet(reach6&&{state=e4}, goal3);
if test3 then print(" property hold ");
	else print(" not safe ");
endif
	
}