




FaultAccommodating ModelsWe model the occurrence of a fault by an unobservable and uncontrollable event F, i. e. we extend nominal lowlevel events Sigma_nlo by the event F to the event set Sigma_lo = Sigma_nlo∪ {F}. A faultaccommodating model is set up in a 2step procedure. Firstly, we model the nominal plant behaviour Ln ⊆ Sigma_pn*. Secondly we establish a model that includes the faults previous history and its impact on the plant, which we denote the plantfailure behaviour Ld ⊆ Sigma_fp*. The pair (Ln,Ld) is called a faultaccommodating model. A faultaccommodating model (Ln,Ld) is called proper if
(1) Ld ∩ Sigma_np* ⊆ Ln
With a faultaccommodating model (Ln,Ld) we associate the
faultaccommodating behaviour
Lf = Ln ∪ Ld
If the faultaccommodating model (Ln,Ld)
is proper,
then, FaultAccommodating Control ReconfigurationThe problem of faultaccommodating control reconfiguration effectively is a standard control problem under partial observation. Formally, it is a tuple (Sigma_f,Lf,Ef) with a faultaccommodating plant Ln and a faultaccommodating specification Ef. We aim for a prefixclosed controller Hf such that the closedloop system Lf  Hf
(FA1) is complete We provide a convenience function for the computation of faultaccommodating controllers. FtcFaBehaviourComputation of faultaccommodating behaviours. Detailed description:
Given a faultaccommodating model (Ln,Ld) represented by Gn and Gd, respectively, i. e.
L(Gn) = Ln and L(Gd) = Ld this function evaluates
Example:FtcIsProperTest properness Detailed description:
Given a faultaccommodating model (Ln,Ld) represented by Gn and Gd, respectively, i. e.
L(Gn) = Ln and L(Gd) = Ld this function checks
(1) Ld ∩ Sigma_np* ⊆ Ln and
FtcFaControllerCheck properness Signature:FtcFaController(+In+ Generator gLfa, +In+ Generator gEfa, +In+ Alphabet aCON, +In+ Alphabet aUCON, +In+ Alphabet aHI, +Out+ Generator gC) Detailed description:Given are generators gLf and gEf, with Lm(gLn) = Lf and Lm(gEf) = Ef 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) = Hf such that the controller Hf ensures (FA1)(FA4) for the closed loop system LfHf. libFAUDES 2.32b  2024.03.08  with "synthesisobserverdiagnosisiosystemhiosysmultitaskingcoordinationcontroltimediodevicesimulatorluabindings" 