model lastinfirstserved {

var I, Sa, Ea, Ma, Sb, Eb, Mb;

states normal;

transition r1 := {
from := normal;
to := normal;
guard := I>=1;
action := I'=I-1, Sa'=Sa+Ea+Ma+1, Ea'=0, Ma'=0;
};

transition r2 := {
from := normal;
to := normal;
guard := Sb>=1;
action := Sb'=Sb-1, Sa' =Ea+Ma+1, Ea'=0, Ma'=0;
};

transition r3 := {
from := normal;
to := normal;
guard := I>=1;
action := I'=I-1, Sb'=Sb+Eb+Mb+1, Eb'=0, Mb'=0;
};

transition r4 := {
from := normal;
to := normal;
guard := Sa>=1;
action := Sa'=Sa-1, Sb'=Sb+Eb+Mb+1, Eb'=0, Mb'=0;
};

transition r5 := {
from := normal;
to := normal;
guard := Sa>=1;
action := I'=I+Sa+Ea+Ma , Sa'=0, Ea'=1, Ma'=0;
};

transition r6 := {
from := normal;
to := normal;
guard := Sb>=1;
action := Sb'=Sb-1, I'=I+Sa+Ea+Ma , Sa'=0, Ea'=1, Ma'=0;
};

transition r7 := {
from := normal;
to := normal;
guard := Sb>=1;
action := I'=I+Sb+Eb+Mb, Sb'=0, Eb'=1, Mb'=0;
};

transition r8 := {
from := normal;
to := normal;
guard := Sa>=1;
action := Sa'=Sa-1, I'=I+Sb+Eb+Mb , Sb'=0, Eb'=1, Mb'=0;
};

transition r9 := {
from := normal;
to := normal;
guard := Ea>=1;
action := Ea'=Ea-1, Ma'=Ma+1;
};

transition r10 := {
from := normal;
to := normal;
guard := Eb>=1;
action := Eb'=Eb-1, Mb'=Mb+1;
};

}



strategy s1 {

setMaxState(0);
setMaxAcc(100);

Region init := {I>=1 && state=normal && Sa=0 && Ea=0 && Ma=0 && Sb=0 && Eb=0 && Mb=0};
Transitions t := {r1,r2,r3,r4,r5,r6,r7,r8,r9,r10};

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

}