model dekker {

var    X1, X9, X11, X13, X15, X2, X3, X4, X5, X6, X7, X8, X10, X12, X14, X16, X17, X18, X19, X20, X21, X22;

states normal;

transition r1 := {
from := normal;
to := normal;
guard := X1 >= 1 && X9 >= 1;
action := X1'=X1-1, X9'=X9-1, X2'=X2+1, X10'=X10+1;
};

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

transition r3 := {
from := normal;
to := normal;
guard := X3>=1 && X11>=1;
action := X3'=X3-1, X11'=X11-1, X4'=X4+1, X12'=X12+1;
};

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

transition r5 := {
from := normal;
to := normal;
guard := X4>=1 && X10>=1;
action := X4'=X4-1, X10'=X10-1, X1'=X1+1, X9'=X9+1;
};

transition r6 := {
from := normal;
to := normal;
guard := X2>=1 && X14>=1;
action :=  X2'=X2-1, X5'=X5+1;
};

transition r7 := {
from := normal;
to := normal;
guard := X5>=1 && X11>=1;
action := X5'=X5-1, X2'=X2+1;
};

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

transition r9 := {
from := normal;
to := normal;
guard := X6>=1 && X10>=1;
action := X6'=X6-1, X10'=X10-1, X7'=X7+1, X9'=X9+1;
};	

transition r10 := {
from := normal;
to := normal;
guard := X7>=1 && X11>=1;
action := X7'=X7-1, X8'=X8+1;
};

transition r11 := {
from := normal;
to := normal;
guard := X8>=1 && X9>=1;
action := X8'=X8-1, X9'=X9-1, X2'=X2+1, X10'=X10+1;
};

transition r12 := {
from := normal;
to := normal;
guard := X15>=1 && X13>=1;
action := X15'=X15-1, X13'=X13-1, X16'=X16+1, X14'=X14+1;
};

transition r13 := {
from := normal;
to := normal;
guard := X16>=1 && X9>=1;
action := X16'=X16-1, X17'=X17+1;
};

transition r14 := {
from := normal;
to := normal;
guard := X17>=1 && X12>=1;
action := X17'=X17-1, X12'=X12-1, X18'=X18+1, X11'=X11+1;
};

transition r15 := {
from := normal;
to := normal;
guard := X17>=1 && X11>=1;
action := X17'=X17-1, X18'=X18+1;
};

transition r16 := {
from := normal;
to := normal;
guard := X18>=1 && X14>=1;
action := X18'=X18-1, X14'=X14-1, X15'=X15+1, X13'=X13+1;
};

transition r17 := {
from := normal;
to := normal;
guard := X16>=1 && X10>=1;
action := X16'=X16-1, X19'=X19+1;
};

transition r18 := {
from := normal;
to := normal;
guard := X19>=1 && X12>=1;
action := X19'=X19-1, X16'=X16+1;
};

transition r19 := {
from := normal;
to := normal;
guard := X19>=1 && X11>=1;
action := X19'=X19-1, X20'=X20+1;
};

transition r20 := {
from := normal;
to := normal;
guard := X20>=1 && X14>=1;
action := X20'=X20-1, X14'=X14-1, X21'=X21+1, X13'=X13+1;
};

transition r21 := {
from := normal;
to := normal;
guard := X21>=1 && X12>=1;
action := X21'=X21-1, X22'=X22+1;
};

transition r22 := {
from := normal;
to := normal;  	   
guard := X22>=1 && X13>=1;
action := X22'=X22-1, X13'=X13-1, X16'=X16+1, X14'=X14+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=1 && X10=0 && X11=1 && X12=0 && X13=1 && X14=0 && X15=1 && X16=0 && X17=0 && X18=0 && X19=0 && X20=0 && X21=0 && X22=0};
Transitions t := {r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,r15,r16,r17,r18,r19,r20,r21,r22};

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

}