model readwrite {

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

states normal;

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

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

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

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

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

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

transition t7 := {
from := normal;
to := normal;
guard := x8>=1 && x12>=1;
action := x4'=x4+5, x7'=x7+1, x8'=x8-1, x12'=x12-1;
};

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

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

}



strategy s1 {

setMaxState(0);
setMaxAcc(100);

Region init := {x0=0 && state=normal && x1=0 && x2=1 && x3=0 && x4=0 && x5=0 && x6=0 && x7=0 && x8=1 && x9=0 && x10=0 && x11=1 && x12=1};
Transitions t := {t1,t2,t3,t4,t5,t6,t7,t8,t9};

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

}