model lamport {

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

states normal;

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

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

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

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

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

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

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

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

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

}



strategy s1 {

setMaxState(0);
setMaxAcc(100);

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

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

}