model fms {

var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12,x13, x14, x15, x16, x17, x18, x19, x20, x21;

states normal;

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

transition t2 := {
from := normal;
to := normal;
guard := x1>=1 && x11>=1;
action :=	x1'=x1-1, x5'=x5+1, x11'=x11-1;
};

transition t3 := {
from := normal;
to := normal;
guard := x2>=1;
action :=	x2'=x2-1, x6'=x6+1;
};

transition t4 := {
from := normal;
to := normal;
guard := x3 >= 1;
action :=	x3'=x3-1, x7'=x7+1;
};

transition t5 := {
from := normal;
to := normal;
guard := x4 >= 1 && x8 >= 1;
action :=	x4'=x4-1, x8'=x8-1, x9'=x9+1;
};

transition t6 := {
from := normal;
to := normal;
guard := x15 >= 1;
action :=	x1'=x1+1, x15'=x15-1;
};

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

transition t8 := {
from := normal;
to := normal;
guard := x6 >= 1 && x13 >= 1;
action :=	x6'=x6-1, x12'=x12+1, x13'=x13-1;
};

transition t9 := {
from := normal;
to := normal;
guard := x7 >= 1 && x13 >= 1;
action :=	x7'=x7-1, x14'=x14+1;
};

transition t10 := {
from := normal;
to := normal;
guard := x9 >= 1;
action :=	x8'=x8+1, x9'=x9-1, x15'=x15+1;
};

transition t11 := {
from := normal;
to := normal;
guard := x10 >= 1 && x16 >= 1;
action :=	x10'=x10-1, x16'=x16-1, x17'=x17+1;
};

transition t12 := {
from := normal;
to := normal;
guard := x18 >= 1;
action :=	x11'=x11+1, x18'=x18-1;
};

transition t13 := {
from := normal;
to := normal;
guard := x12 >= 1;
action :=	x12'=x12-1, x13'=x13+1, x18'=x18+1;
};

transition t14 := {
from := normal;
to := normal;
guard := x14 >= 1;
action :=	x3'=x3+1, x14'=x14-1;
};

transition t15 := {
from := normal;
to := normal;
guard := x15 >= 1;
action :=	x15'=x15-1, x19'=x19+1;
};

transition t16 := {
from := normal;
to := normal;
guard := x17 >= 1;
action :=	x16'=x16+1, x17'=x17-1, x20'=x20+1;
};

transition t17 := {
from := normal;
to := normal;
guard := x18 >= 1;
action :=	x18'=x18-1, x21'=x21+1;
};

transition t18 := {
from := normal;
to := normal;
guard := x19 >= 1;
action :=	x0'=x0+1, x19'=x19-1;
};

transition t19 := {
from := normal;
to := normal;
guard := x20 >= 1;
action :=	x0'=x0+1, x2'=x2+1, x20'=x20-1;
};

transition t20 := {
from := normal;
to := normal;
guard := x21>=1;
action :=	x2'=x2+1, x21'=x21-1;
};

}



strategy s1 {

setMaxState(0);
setMaxAcc(100);

Region init := {x0>=1 && state=normal && x1=0 && x2>=1 && x3>=1 && x4=0 && x5=0 && x6=0 && x7=0 && x8=3 && x9=0 && x10=0 && x11=0 && x12=0 && x13=1 && x14=0 && x15=0 && x16=2 && x17=0 && x18=0 && x19=0 && x20=0 && x21=0};
Transitions t := {t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15,t16,t17,t18,t19,t20};

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

}