model csm {

var
     x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12,x13;

states e0;

transition t1 := {
	from :=e0;
	to:=e0;
	guard :=
    	x0 >= 1 ;
	action :=
		    x0' = x0-1 ,
		    x1' = x1+1 
	;
};

transition t2 := {
	from :=e0;
	to:=e0;
	guard :=
    x4 >= 1 && x9 >= 1; 
action :=
		    x0' = x0+1 ,
		    x2' = x2+1 ,
		    x4' = x4-1 ,
		    x9' = x9-1 
	;
};

transition t3 := {
	from :=e0;
	to:=e0;
	guard :=
    x4 >= 1 && x6 >= 1; 
action :=
		    x0' = x0+1 ,
		    x3' = x3+1 ,
		    x4' = x4-1 ,
		    x6' = x6-1 
	;
};

transition t4 := {
	from :=e0;
	to:=e0;
	guard :=
    x1 >= 1 && x3 >= 1; 
action:=
		    x1' = x1-1 ,
		    x3' = x3-1 ,
		    x5' = x5+1 ,
		    x6' = x6+1 
	;
};

transition t5 := {
	from :=e0;
	to:=e0;
	guard :=
    x1 >= 1 && x2 >= 1; 
action:=
		    x1' = x1-1 ,
		    x2' = x2-1 ,
		    x5' = x5+1 ,
		    x9' = x9+1 
	;
};

transition t6 := {
	from :=e0;
	to:=e0;
	guard :=
    x5 >= 1; 
action:=
			x4' = x4+1 ,
		       	x5' = x5-1 
	;
};

transition t7 := {
	from :=e0;
	to:=e0;
	guard :=
    x10 >= 1; 
action:=
		    x7' = x7+1 ,
		    x10' = x10-1 
	;
};

transition t8 := {
	from :=e0;
	to:=e0;
	guard :=
    x7 >= 1; 
action:=
		    x7' = x7-1 ,
		    x8' = x8+1 
	;
};

transition t9 := {
	from :=e0;
	to:=e0;
	guard :=
    x6 >= 1 && x8 >= 1; 
action:=
		    x6' = x6-1 ,
		    x8' = x8-1 ,
		    x9' = x9+1 
	;
};

transition t10 := {
	from :=e0;
	to:=e0;
	guard :=
    x9 >= 1; 
action:=
		    x6' = x6+1 ,
		    x9' = x9-1 ,
		    x10' = x10+1 
	;
};

transition t11 := {
	from :=e0;
	to:=e0;
	guard :=
    x10 >= 1; 
action:=
			x10' = x10-1 ,
			x12' = x12+1
	;
};

transition t12 := {
	from :=e0;
	to:=e0;
	guard :=
    x11 >= 1; 
action:=
		    x8' = x8+1 ,
		    x11' = x11-1 ,
		    x13' = x13+1 
	;
};

transition t13 := {
	from :=e0;
	to:=e0;
	guard :=
    x12 >= 1 && x13 >= 1; 
action:=
		    x11' = x11+1 ,
		    x12' = x12-1 ,
		    x13' = x13-1 
	;
};

}

strategy s1 {

setMaxState(0);
setMaxAcc(100);


Region init :=
	{x0=0 && x1=0 && x2=0 && x3=0 && x4=0 && x5=1 && x6=1 && x7>=1 && x8=0 && x9=0 && x10=0 &&
	 x11=0 && x12=0 && x13=1 && state=e0 };

Transitions t := {t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13};

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

	
}