




Coordination Control PlugInThis plugin implements functions for coordination control synthesis of prefixclosed languages (this means that for most of the functions, input generators are required to have all states marked), see the literature. The case of nonprefixclosed languages is still under investigation and will be added as soon as the algorithms are developed. The following functions are implemented (see details below): Given a plant L =  L(G_{i}), i=1,...,n, and a specification language K, the goal is to construct the supremal conditionally controllable sublanguage of K.
Copyright (c) 2011  2015, Tomas Masopust IsConditionalClosedTests for conditional closedness. Signature:IsConditionalClosed(+In+ GeneratorVector specVect, +In+ Generator pk, +In+ GeneratorVector genVect, +In+ Generator gk, +Out+ Boolean BRes) Detailed description: The function checks conditional closedness of a given conditionally decomposable language
K = P_{1+k}(K)  P_{2+k}(K)  ...  P_{n+k}(K)
with respect to generators G_{i}, i=1,2,...,n.
Note: Lclosed is also referred to as Lrelatively prefixclosed.
Parameter Conditions:
IsConditionalControllableTests for conditional controllability. Signature:IsConditionalControllable(+In+ GeneratorVector specVect, +In+ Generator pk, +In+ GeneratorVector genVect, +In+ Generator gk, +In+ EventSet ACntrl, +Out+ Boolean BRes) Detailed description: The function checks conditional controllability of a given conditionally decomposable language
K = P_{1+k}(K)  P_{2+k}(K)  ...  P_{n+k}(K)
with respect to generators G_{i}, i=1,2,...,n,
and the corresponding sets of uncontrollable events E_{i+k,u}, i=1,2,...,n.
It returns true if K is conditionally controllable.
It is required that the subparts P_{i+k} and G_{i} are at the same position in the
vectors, i.e., specVector.At(i) = P_{i+k}(K) and genVect.At(i) = G_{i},
for all i.
Parameter Conditions:
IsConditionalDecomposableTests for conditional decomposability. Signature:IsConditionalDecomposable(+In+ System gen, +In+ EventSetVector alphVector, +In+ EventSet ek, +InOut+ System proof, +Out+ Boolean BRes) Detailed description:The function checks conditional decomposability of a given language K=L_{m}(gen) with respect to a vector of alphabets alphVector and an additional alphabet ek. It returns true if K is conditionally decomposable. A languge K is conditionally decomposable w.r.t. the event sets E_{k} and (E_{i}, i=1,2,...,n) if K = P_{1+k}(K)  P_{2+k}(K)  ...  P_{n+k}(K), where P_{i+k} is a natural projection from the global event set to the event set E_{i} union E_{k}. Parameter Conditions:
ConDecExtensionExtension of Ek for K to become conditionally decomposable. Signature:ConDecExtension(+In+ System gen, +In+ EventSetVector alphVector, +InOut+ EventSet ek) Detailed description:The function extends ek so that K=L_{m}(gen) becomes conditionally decomposable with respect to a vector of alphabets alphVector and the extended alphabet ek. It returns the extended alphabet ek. A languge K is conditionally decomposable w.r.t. the event sets E_{k} and (E_{i}, i=1,2,...,n) if K = P_{1+k}(K)  P_{2+k}(K)  ...  P_{n+k}(K), where P_{i+k} is a natural projection from the global event set to the event set E_{i} union E_{k}. Parameter Conditions:
SupConditionalControllableComputation of the supremal conditionally controllable sublanguage of the specification K Signature:SupConditionalControllable(+In+ System SpecGen, +In+ GeneratorVector genVector, +In+ EventSet ACntrl, +In+ EventSet InitEk, +Out+ GeneratorVector supVector, +Out+ Generator Coord) Detailed description:The function computes supremal conditionally controllable sublanguage of a given conditionally decomposable language K = P_{1+k}(K)  P_{2+k}(K)  ...  P_{n+k}(K) with respect to generators G_{i}, i=1,2,...,n, and the corresponding sets of uncontrollable events E_{i+k,u}, i=1,2,...,n. It returns the supervised coordinator and a vector of corresponding supervisors such that the language of their parallel composition is the supremal conditionally controllable sublanguage of K. It proceeds in the following steps:
A language K is conditionally controllable with respect to generators G_{k} and (G_{i},i=1,2,...,n) and the set of uncontrollable events E_{k,u} and (E_{i,u},i=1,2,...,n) if
Parameter Conditions:
ccTrimA bit more efficient trim operation based on graph algorithms. Detailed description:The generator is transformed to a graph representation and the graph algorithms are used. The graph representation uses the adjacency list. (Only for experimental reasons. Optimization in progress.) It returns true if the generator gen is trimmed. Parameter Conditions:
Literature[CC_AUT2012] J. Komenda, T. Masopust, J.H. van Schuppen: Supervisory Control Synthesis of DiscreteEvent Systems using a Coordination Scheme, Automatica 48(2), 247254, 2012. [CC_SCL2011] J. Komenda, T. Masopust, J.H. van Schuppen: Synthesis of controllable and normal sublanguages for discreteevent systems using a coordinator, Systems & Control Letters, 60(7), 492502, 2011. [CC_2012PP] J. Komenda, T. Masopust, J.H. van Schuppen: On Conditional Decomposability, Preprint, http://arxiv.org/abs/1201.1733. libFAUDES 2.32b  2024.03.01  with "synthesisobserverobservabilitydiagnosishiosysiosystemmultitaskingcoordinationcontroltimedsimulatoriodeviceluabindingshybridexamplepybindings" 