




Observer SynthesisVerification algorithms for various conditions on natural projections of plant languages L(G) that are sufficient for the nonblocking and maximally permissive hierarchical supervisor synthesis are provided on the Observer Test page. In contrast, the algorithms described on this page are concerned with the situation where these sufficient conditions are not fulfilled such that a given natural projection has to be modified in order to perform a hierarchical supervisor synthesis. In the observer plugin, such modifications are offered for the natural observer condition (NaturalObserverExtension,NaturalObserverRelabeling) and the msaobserver condition (MsaObserver) in order to achieve nonblocking hierarchical control and for the combination of both conditions with local control consistency (NaturalObserverLcc,MsaObserverLcc) in order to achieve nonblocking and maximally permissive control. The general approach taken in our algorithms is to extend the projection alphabet of a given natural projection until the repective sufficient condition is fulfilled. In the algorithmic implementation, we use the fact that all conditions can be represented in terms of a specific equivalence relation (quasicongruence) for a dynamic system that is defined on the state space of the plant automaton G [O5]. After obtaining an appropriate dynamic system representation for each condition, either the heuristic alphabet extension algorithm in [O6] is used to obtain a suitable alphabet extension (NaturalObserverExtension, NaturalObserverLcc, MsaObserver, MsaObserverLcc) or an appropriate event relabeling is performed according to [O1] (NaturalObserverRelabeling). NaturalObserverExtensionNatural observer computation by alphabet extension. Signature:NaturalObserverExtension(+In+ Generator GArg, +InOut+ EventSet Sigma_h) NaturalObserverExtension(+In+ Generator GArg, +InOut+ EventSet Sigma_h, +Out+ Integer #Q) Detailed description:This function extends a given projection alphabet Sigma_h such that the resulting projection is a natural observer for the marked language of the given generator GArg. Parameter Conditions:The alphabet Sigma_h has to be a subset of the alphabet of GArg. GArg must be a deterministic generator. NaturalObserverRelabelingNatural observer computation with event relabeling. Signature:NaturalObserverRelabeling(+InOut+ System GPlant, +InOut+ EventSet SigmaHi, +Out+ EventSet SigmaHiNew, +Out+ EventRelabelMap Map) Detailed description:This function relabels events in a given generator GPlant and relabels and extends a given projection alphabet SigmaHi to a new projection alphabet SigmaHiNew such that the resulting natural projection is a natural observer for the marked language of the modified generator GPlant. Parameter Conditions:The alphabet SigmaHi has to be a subset of the alphabet of GPlant. GPlant must be a deterministic generator. NaturalObserverLccNatural observer computation with local control consistency (LCC) condition by alphabet extension. Signature:NaturalObserverLcc(+In+ Generator Plant, +In+ EventSet Sigma_c, +InOut+ EventSet Sigma_h) NaturalObserverLcc(+In+ Generator Plant, +In+ EventSet Sigma_c, +InOut+ EventSet Sigma_h, +Out+ Integer #Q) Detailed description:This function extends a given projection alphabet Sigma_h such that the resulting projection is both a natural observer for the marked language of the given generator Plant and locally control consistent for the system Plant with the controllable events Sigma_c. Parameter Conditions:The alphabet Sigma_h has to be a subset of the alphabet of Plant. Plant must be a deterministic generator. MsaObserverMarked string accepting (MSA) observer computation by alphabet extension. Signature:MsaObserver(+In+ Generator GArg, +InOut+ EventSet Sigma_h) MsaObserver(+In+ Generator GArg, +InOut+ EventSet Sigma_h, +Out+ Integer #Q) Detailed description:This function extends a given projection alphabet Sigma_h such that the resulting projection is an msaobserver for the marked language of the given generator GArg. Parameter Conditions:The alphabet Sigma_h has to be a subset of the alphabet of GArg. GArg must be a deterministic generator. MsaObserverLccMarked string accepting (MSA) observer computation with local control consistency (LCC) condition by alphabet extension. Signature:MsaObserverLcc(+In+ Generator GArg, +In+ EventSet Sigma_c, +InOut+ EventSet Sigma_h) MsaObserverLcc(+In+ Generator GArg, +In+ EventSet Sigma_c, +InOut+ EventSet Sigma_h, +Out+ Integer #Q) Detailed description:This function extends a given projection alphabet Sigma_h such that the resulting projection is both an msaobserver for the marked language of the given generator GArg and locally control consistent for the system GArg with the controllable events Sigma_c. Parameter Conditions:The alphabet Sigma_h has to be a subset of the alphabet of GArg. GArg must be a deterministic generator. libFAUDES 2.28b  2019.12.01  with "synthesisobserverdiagnosisiosystemhiosysmultitaskingcoordinationcontroltimediodevicesimulatorluabindings" 