Tests for conditional controllability.
Detailed description:
The function checks conditional controllability of a given conditionally decomposable language
K = P1+k(K) || P2+k(K) || ... || Pn+k(K)
with respect to generators Gi, i=1,2,...,n,
and the corresponding sets of uncontrollable events Ei+k,u, i=1,2,...,n.
It returns true if K is conditionally controllable.
A language K is conditionally controllable with respect to generators Gk and
(Gi,i=1,2,...,n) and the set of uncontrollable events Ek,u and
(Ei,u,i=1,2,...,n) if
- Pk(K) is controllable w.r.t. L(Gk) and Ek,u
- Pi+k(K) is controllable w.r.t. L(Gi)||L(Pk(K)) and Ei+k,u,
where Ei+k,u is the set of all uncontrollable events of the event sets
Ei and Ek
It is required that the subparts Pi+k and Gi are at the same position in the
vectors, i.e., specVector.At(i) = Pi+k(K) and genVect.At(i) = Gi,
for all i.
The representation of K as the parallel composition of the components is chosen for the reason that
the computation of a projection can be of exponential complexity.
Therefore, it is rather left for the user to compute the decomposation of K.
Usually, it is required that the projection is a natural observer, which ensures the lower complexity
of the operation projection.
Parameter Conditions:
specVector is a vector of deterministic nonblocking generators for
the languages Pi+k, i=1,2,...,n.
pk is a deterministic nonblocking generator for the language Pk(K).
genVector is a vector of deterministic nonblocking generators Gi, i=1,2,...,n.
gk is a deterministic nonblocking generator for the coordinator Gk such that
its event set ek contains all shared events.
ACntrl is a set of controllable events.
The local controllable events are computed by intersection of the alphabets of
the generators Gi with the set ACntrl.