model multipoll {

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

states normal;

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

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

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

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

transition t5 := {
from := normal;
to := normal;
guard := x4>=1;
action := x1'=x1+1, x4'=x4-1, x7'=x7+1;
};

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

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

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

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

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

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

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

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

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

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

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

transition t17 := {
from := normal;
to := normal;
guard := x13>=1;
action := x7'=x7+1, x13'=x13-1, x16'=x16+1;
};

transition t18 := {
from := normal;
to := normal;
guard := x14>=1;
action := x7'=x7+1, x14'=x14-1, x17'=x17+1;
};

transition t19 := {
from := normal;
to := normal;
guard := x11>=1 && x15>=1;
action := x11'=x11-1, x14'=x14+1, x15'=x15-1;
};

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

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

}



strategy s1 {

setMaxState(0);
setMaxAcc(100);

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

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

}