




FaultHiding Control ReconfigurationNominal ControlOur nominal control problem effectively is a standard control problem under partial observation. Formally, the nominal control problem is a tuple (Sigma_n,Ln,En) with the nominal plant Ln and the nominal specification En. We aim for a prefixclosed controller Hn such that the closedloop system Ln  Hn
(NC1) is complete We provide a convenience function for the computation of nominal controllers. Control ReconfigurationVirtualisationIn order to create the necessary degrees of freedom, the nominal controller needs to be decoupled from the faulty plant. Formally we relabel the controllable uncontrollable events, a process that we call virtualisation. Given is a bijective function \rho and we define Sigma_vcon := \rho Sigma_con and Sigma_vucon := \rho Sigma_vucon. We define the function h:SIGn*→SIGv* recursively according to h(epsilon) = epsilon and h(s o) = h(s) rho(o) if o\notinSigma_hi or h(s o) = h(s) o otherwise. Given a nominal controller Hn the corresponding virtual controller Hv is given by Hv := h Hn. SelfReconfiguring ClosedLoop System
We seek for a prefix closed reconfigurator R ⊆ Sigma_R* such
that for all virtualised controllers Hv
the selfreconfiguring closedloop system
LfRHv
(R1) is complete holds. Reconfigurator DesignGiven a language K ⊆ Sigma* such that
(K1) K is controllable w.r.t.
(LfHv↑,Sigma_ucon∪Sigma_vcon∪Sigma_lo∪Sigma_hi
holds, then the reconfigurator R = PR (K) ensures the properties (R2)(R4) in the selfreconfiguring closedloop system LfRHv. The properties (K1)(K7) are preserved under arbitrary union, thus for a given specification E there exists the supremal sublanguage of E w.r.t. the properties (K1)(K7). Algorithms for the computation of the supremal complete sublanguage and the supremal weakly sensorconsistent sublanguage are provided in this LuaExtension. Each of the properties (K1)(K7) satisfies the prerequisites in [FTC3], hence, the respective supremal sublanguage can be computed using a simple iterative scheme. The whole design process is prototypically shown in a tuorial Verifikation of NonConflictingness
Let M ⊆ Closure(K) denote a target language and define the operators
Omega1a = {s ∈ Closure(K)(∃ o ∈ Sigma_ucon∪Sigma_vcon)[s o ∈ M]} and let
\Omega = \Omega1a o \Omega1b o \Omega1c denote their concatenation. Consider the iteration
M0 = K Whenever K satisfies (K1)(K7) and Closure(K) is fixpoint of \Omega , then R = P_R(Closure(K)) ensures for any virtualised solution Hv to the nominal control problem (Sigma_n,Ln,En) the properties (R1)(R4). FtcIsCompleteTest completeness. Signature:FtcIsComplete(+In+ Generator gK, +Out+ Boolean bIsCmp) FtcIsComplete(+In+ Generator gK, +In+ Alphabet aSIGo, +Out+ Boolean bIsCmp) FtcIsComplete(+In+ Generator gK, +In+ Alphabet aSIGo, +Out+ StateSet sBadStates, +Out+ Boolean bIsCmp) Detailed description:This function is equivalent to IsComplete. Optionally, the set of states q_Bad that conflicts with completeness can be returned. FtcSupCompleteComputate the supremal complete sublanguage. Detailed description:This function is equivalent to Complete. Parameter Conditions:K needs to be closed FtcIsWeakSensorConsistentTest weak sensorconsistency. Signature:FtcIsWeakSensorConsistent(+In+ Generator gK, +In+ Generator gLv, +In+ Alphabet aVUCON, +In+ Alphabet aCV, +Out+ StateSet qBad, +Out+ StateSet qLsns, +Out+ StateSet qKsns, +Out+ Boolean bIsWsc) FtcIsWeakSensorConsistent(+In+ Generator gK, +In+ Generator gLv, +In+ Alphabet aVUCON, +In+ Alphabet aCV, +Out+ Boolean bIsWsc) Detailed description:Given is a reconfiguration problem (Ln,En,Lf,Ef,E_R). With Lv = h(Ln) the virtualised plant, Sigma_vucon the virtual uncontrollable events and Sigma_vc the virtual controller events. A language K ⊆ Sigma* is called weakly sensorconsistent w.r.t. Lv, if
(∀ s ∈ Closure(K))[(PV s)Sigma_vucon ∩ (Closure(Lv)) ≠ 0 ⇒
holds. Given generators gK, with L(gK) = K, gLv, with L(gLv) = Lv and containers which hold Sigma_vcon and Sigma_vc this functions tests if K is weakly sensorconsistent w.r.t. Lv and returns the result as a boolean value. Optionally, the stateset that conflicts with weak sensorconsistency qBad, and good states in gLv and gK can be returned. Parameter Conditions:Trim realisations FtcSupWeakSensorConsistentComputation of the supremal weak sensorconsistent sublanguage Signature:FtcSupWeakSensorConsistent(+In+ Generator gK, +In+ Generator gLv, +In+ Alphabet aVUCON, +In+ Alphabet aCV, +Out+ Generator gRes) Detailed description:Given is a reconfiguration problem (Ln,En,Lf,Ef,Er) and let Lv = h(Ln) denote the virtualised plant model and let K↑ = sup{M ⊆ KM is weakly sensorconsistent w.r.t. Lv} denote the supremal weakly sensorconsistent sublanguage of K. Based on a generator gK with Lm(gK) = K and containers that hold Sigma_vucon and Sigma_vc this function returns a generator gRes with Lm(gRes) = K↑ Parameter Conditions:K needs to be closed Trim realisations FtcIsNonconflictingCheck for a nonconflicting selfreconfiguring closedloop system. Signature:FtcIsNonconflicting(+In+ Generator gK, +In+ Alphabet aLO, +In+ Alphabet aHI, +In+ Alphabet aUCON, +In+ Alphabet aCON, +Out+ Boolean bRes) Detailed description:Given is a candidat K = LfRHv for the selfreconfiguring closedloop system togther with the set of lowlevel events Sigma_lo, the set of highlevel events Sigma_hi, the set of uncontrollable events Sigma_ucon and the set of virtual controllable events Sigma_vcon. Consider a target language M ⊆ Closure(K), define the operators
Omega1a = {s ∈ Closure(K)(∃ o ∈ Sigma_ucon∪Sigma_vcon)[s o ∈ M]}
and let Based on a generator gK with Lm(gK) = K and containers alpLO, alpHI, alpUCON and alpVCON that hold the alphabets Sigma_lo, Sigma_hi, Sigma_ucon and Sigma_vcon, this function computes the largest fixpoint of the operator \Omega and returns TRUE if Closure(K) = \Omega K and FALSE otherwise. FtcInactivityConditionsConstruct inactivity conditions. Signature:FtcInactivityConditions(+In+ Alphabet aCON, +In+ Alphabet aUCON, +Out+ Generator gE) FtcInactivityConditions(+In+ Alphabet aCON, +In+ Alphabet aUCON, +In+ String sF, +Out+ Generator gE) Detailed description:
Given containers aCON, aUCON, aVCON and aVUCON that hold the controllable events
Sigma_con and an empty generator genEr, this functions constructs gEr such
that Lm(gEr) = Er, with
E_R = Closure(gEr) holds. By default, the controllable and uncontrollable events are relabled by appending the postfix "_v" and the faultevent is named "F". Alternatively, the name of the faultevent can be given as a parameter. Parameter Conditions:Trim realisations FtcVirtualiseVirtualise a generator or an alphabet Signature:FtcVirtualise(+In+ Generator gOrg, +In+ Alphabet aUntouched, +Out+ Generator gRes) FtcVirtualise(+In+ Alphabet aOrg, +In+ Alphabet aUntouched, +Out+ Alphabet aRes) FtcVirtualise(+In+ Generator gOrg, +In+ Alphabet aUntouched, +In+ String aPostfix, +Out+ Generator gRes) FtcVirtualise(+In+ Alphabet aOrg, +In+ Alphabet aUntouched, +In+ String aPostfix, +Out+ Alphabet aRes) Detailed description:Given an eventset Sigma, this function returns an alphabet Sigma' such that there exists a bijective function rho such that \Sigma'=roh(\Sigma). Technically, all events are relabelled by adding the postfix sPostfix. Given a generator gOrg, with, L(gOrg) = L this function returns a generator gRes with L(gRes) = h(L). By default, all events exept alpUntouched are relabled by appending the postfix "_v". Alternatively, the postix can be given as a parameter. Example:FtcNomControllerCompute nominal controller. Signature:FtcNomController(+In+ Generator gLn, +In+ Generator gEn, +In+ Alphabet aCON, +In+ Alphabet aUCON, +In+ Alphabet aHI, +Out+ Generator gC) Detailed description:Given are generators gLn and gEn, with Lm(gLn) = Ln and Lm(gEn) = En together with containers alpCON, alpUCON and alpHI that hold the controllable events Sigma_con, uncontrollable events Sigma_ucon and the highlevel events Sigma_hi. This function return constructs a generator gC with Lm(gC) = Hn such that the controller Hn ensures (NC1)(NC4) for the closed loop system LnHn. FtcReconfiguratorCompute universal reconfigurator. Signature:FtcReconfigurator(+In+ Generator gLn, +In+ Generator gLf, +In+ Generator gEr, +In+ Generator gEf, +In+ Generator gHn, +In+ Alphabet aCON, +In+ Alphabet aUCON, +In+ Alphabet aHI, +In+ Alphabet aLO, +Out+ Generator gR) Detailed description:Given are generators gLn, gLf, gEr, gEf and gHn with Lm(gLn) = Ln, Lm(gLf) = Lf, Lm(gEr) = Er, Lm(gEf) = Ef and Lm(gHn) = Hn↑ together with containers alpCON, alpUCON, alpHI and alpLO that hold the controllable events Sigma_con, uncontrollable events Sigma_ucon, the highlevel events Sigma_hi and the lowlevel events Sigma_lo. This function return constructs a generator gR with Lm(gR) = R such that the reconfigurator R ensures (R1)(R4) for the selfreconfiguring closed loop system LfRHv, for all virtualised controllers Hv. FtcReconfiguratorTimedCompute universal reconfigurator. Use controllabity for timed DES. Signature:FtcReconfiguratorTimed(+In+ Generator gLn, +In+ Generator gLf, +In+ Generator gEr, +In+ Generator gEf, +In+ Generator gHn, +In+ Alphabet aCON, +In+ Alphabet aUCON, +In+ Alphabet aHI, +In+ Alphabet aLO, +Out+ Generator gR) Detailed description:Given are generators gLn, gLf, gEr, gEf and gHn with Lm(gLn) = Ln, Lm(gLf) = Lf, Lm(gEr) = Er, Lm(gEf) = Ef and Lm(gHn) = Hn↑ together with containers alpCON, alpUCON, alpHI and alpLO that hold the controllable events Sigma_con, uncontrollable events Sigma_ucon, the highlevel events Sigma_hi and the lowlevel events Sigma_lo. This function return constructs a generator gR with Lm(gR) = R such that the reconfigurator R ensures (R1)(R4) for the selfreconfiguring closed loop system LfRHv, for all virtualised controllers Hv. Note that the controllability property (R3) was replaced by a controllablity developed for timed discrete event systems. This function is experimental. libFAUDES 2.28b  2019.12.01  with "synthesisobserverdiagnosisiosystemhiosysmultitaskingcoordinationcontroltimediodevicesimulatorluabindings" 