model centralserversystem {

var Think,WaitC,UseC,Stopped,WaitD,UseD,IdleD,BusyD,IdleC,BusyC,Pbusy,Int;

states normal;

transition req := {
from := normal;
to := normal;
guard := Think>=1;
action := Think'=Think-1, WaitC'=WaitC+1;
};

transition useC := {
from := normal;
to := normal;
guard := WaitC>=1 && IdleC>=1;
action := WaitC'=WaitC-1, UseC'=UseC+1, IdleC'=IdleC-1, BusyC'=BusyC+1;
};

transition releaseC1 := {
from := normal;
to := normal; 
guard := UseC>=1 && BusyC>=1;
action := BusyC'=BusyC-1, IdleC'=IdleC+1, UseC'=UseC-1, Think'=Think+1;
};

transition releaseC2 := {
from := normal;
to := normal;
guard := UseC>=1 && BusyC>=1;
action := BusyC'=BusyC-1, IdleC'=IdleC+1, UseC'=UseC-1, WaitD'=WaitD+1;
};

transition useD := {
from := normal;
to := normal;
guard := WaitD>=1 && IdleD>=1;
action := WaitD'=WaitD-1, UseD'=UseD+1, IdleD'=IdleD-1, BusyD'=BusyD+1;
};

transition releaseD := {
from := normal;
to := normal;
guard := UseD>=1 && BusyD>=1;
action := BusyD'=BusyD-1, IdleD'=IdleD+1, UseD'=UseD-1, WaitC'=WaitC+1;
};

transition stop := {
from := normal;
to := normal;
guard := Int=0;
action := Int'=1, Stopped'=UseC+Stopped, UseC'=0, IdleC'=Pbusy+IdleC, Pbusy'=0;
};

transition return := {
from := normal;
to := normal;
guard := Int =1;
action := UseC'=Stopped+UseC, Stopped'=0, Int'=0, Pbusy'=IdleC+Pbusy, IdleC'=0;
};

}



strategy s1 {

setMaxState(0);
setMaxAcc(100);

Region init := {Think>=1 && state=normal && WaitC=0 && UseC=0 && Stopped=0 && WaitD=0 && UseD=0 && IdleD=1 && BusyD=0 && IdleC=1 && BusyC=0 && Pbusy=0 && Int=0};
Transitions t := {req,useC,releaseC1,releaseC2,useD,releaseD,stop,return};

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

}