model rtp {

var X1, X2, X3, X4, X5, X6, X7, X8, X9;

states normal;

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

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

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

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

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

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

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

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

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

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

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

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

}



strategy s1 {

setMaxState(0);
setMaxAcc(100);

Region init := {X1=1 && state=normal && X2=0 && X3=0 && X4=0 && X5=0 && X6=0 && X7=0 && X8=0 && X9=0};
Transitions t := {t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12};

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

}