model kanban {

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

states normal;

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

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

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

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

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

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

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

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

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

transition t10 := {
from := normal;
to := normal;
guard := x8>=1;
action := x8'=x8-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 :=
 x8>=1;
action := x8'=x8-1, x11'=x11+1;
};

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

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

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

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

}



strategy s1 {

setMaxState(0);
setMaxAcc(100);

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

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

}