FtcIsComplete

Test completeness.

Detailed description:

This function is equivalent to IsComplete.

Optionally, the set of states q_Bad that conflicts with completeness can be returned.

FtcSupComplete

Computate the supremal complete sublanguage.

Detailed description:

This function is equivalent to Complete.

Parameter Conditions:

K needs to be closed

FtcIsWeakSensorConsistent

Test weak sensor-consistency.

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 sensor-consistent w.r.t. Lv, if

(∀ s ∈ Closure(K))[(PV s)Sigma_vucon ∩ (Closure(Lv)) ≠ 0  ⇒
                   s(Sigma-Sigma_vc)*Sigma_vucon ∩ ( Closure(K) ) ≠ 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 sensor-consistent w.r.t. Lv and returns the result as a boolean value. Optionally, the state-set that conflicts with weak sensor-consistency qBad, and good states in gLv and gK can be returned.

Parameter Conditions:

Trim realisations

FtcSupWeakSensorConsistent

Computation of the supremal weak sensor-consistent sublanguage

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 ⊆ K|M is weakly sensor-consistent w.r.t. Lv}

denote the supremal weakly sensor-consistent 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

FtcIsNonconflicting

Check for a non-conflicting self-reconfiguring closed-loop system.

Detailed description:

Given is a candidat K = Lf||R||Hv for the self-reconfiguring closed-loop system togther with the set of low-level events Sigma_lo, the set of high-level 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]}
Omega1b = {s ∈ Closure(K)|(∃ o ∈ Sigma_lo∪Sigma_hi)[s o ∈ M]}
Omega1c = {s ∈ Closure(K)|(∀ o ∈ Sigma)[s o ∈ M]}

and let

Omega = Omega1a o Omega1b o Omega1c

denote their concatenation. Consider the iteration

M0 = K
M_i+1 = Omega(Mi)

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 fix-point of the operator \Omega and returns TRUE if Closure(K) = \Omega K and FALSE otherwise.

FtcInactivityConditions

Construct inactivity conditions.

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)

Closure({rho(x)x|x ∈ SIGcon}∪{x rho(x)|x ∈ SIGcon}∪Sigma_hi∪Sigma_lo)*)F Sigma*

holds.

By default, the controllable and uncontrollable events are relabled by appending the postfix "_v" and the fault-event is named "F". Alternatively, the name of the fault-event can be given as a parameter.

Parameter Conditions:

Trim realisations

FtcVirtualise

Virtualise a generator or an alphabet

Detailed description:

Given an event-set 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:

FtcNomController

Compute nominal controller.

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 high-level 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 Ln||Hn.

FtcReconfigurator

Compute universal reconfigurator.

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 high-level events Sigma_hi and the low-level events Sigma_lo. This function return constructs a generator gR with Lm(gR) = R such that the reconfigurator R ensures (R1)-(R4) for the self-reconfiguring closed loop system Lf||R||Hv, for all virtualised controllers Hv.

FtcReconfiguratorTimed

Compute universal reconfigurator. Use controllabity for timed DES.

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 high-level events Sigma_hi and the low-level events Sigma_lo. This function return constructs a generator gR with Lm(gR) = R such that the reconfigurator R ensures (R1)-(R4) for the self-reconfiguring closed loop system Lf||R||Hv, 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.