libFAUDES
Reference
Type Index
Function Index
Literature
Sections
CoreFaudes
- CoreFaudes
- Introduction
- Generators
- Alphabets
- Reachability
- Boolean Operations
- Regular Expressions
- Synchronous Composition
- Projection
- StateSet Conversion
- Elementary Types
- Miscellaneous
- Vector Types
CoordinationControl
Diagnosis
- Diagnosis
- Introduction
- Event-Diagnosis
- Language-Diagnosis
- Modular Diagnosis
- Decentralized Diagnosis
- Application Example
FaultTolerantControl
- FaultTolerantControl
- Introduction
- Example
- Fault-Accommodation
- Reconfiguration
- Fault-Patterns
HioSys
- HioSys
- Introduction
- Step-By-Step
- Synthesis Procedure
- Liveness Properties
- Application Example
IoSystem
- IoSystem
- Introduction
- Properties
- Synthesis
Multitasking
- Multitasking
- Introduction
- Functions
- Observer
- Optimal Color Set
- Reachability
- Synthesis
Observer
- Observer
- Introduction
- Verification
- Synthesis
- Example
Simulator
- Simulator
- Introduction
- Executor Classes
- Hardware-In-The-Loop
- IO-Devices
- Simulator Interconnection
Synthesis
- Synthesis
- Introduction
- Controllability
- Normality
- Omega-Controllability
- Misc Functions

Functions

Faudes-functions implement operations to be performed on faudes-typed parameters. Each faudes-function has one or more signatures to specify supported parameter types. For example, the function for the parallel composition of two generators has the following signature:

Signature:

Parallel(+In+ Generator G1, +In+ Generator G2, +Out+ Generator GRes)

Parallel(+In+ GeneratorVector GVec, +Out+ Generator GRes)

A parameter that remains constant during the execution of a function is referred to as an argument, indicated by +In+. A parameter, that does not affect the outcome of the function, but that does change its value during execution, is referred to as a result, indicated by +Out+. Other parameters are flagged +InOut+.

Faudes-functions available in this copy of libFAUDES are:

Accessible	Delete non-accessible states and transitions.
AlphabetDifference	Difference of two alphabets.
AlphabetEquality	Tests whether two alphabets match.
AlphabetExtract	Extract alphabet from generator.
AlphabetInclusion	Tests whether an alphabet includes another alphabet.
AlphabetIntersection	Intersection over alphabets.
AlphabetLanguage	Generator with Lm(G)=Sigma.
AlphabetUnion	Union over Alphabets
Automaton	Convert generator to formal automaton.
Coaccessible	Delete non-coaccessible states and transitions.
Complete	Delete states that evolve into a terminal state.
ConDecExtension	Extension of Ek for K to become conditionally decomposable.
DecentralizedDiagnoser	Computes decentralized diagnosers for multiple local sites.
DecentralizedModularDiagnoser	Computes decentralized diagnosers for systems that consist of multiple components.
Deterministic	Powerset construction to enforce determinism.
EmptyLanguage	Set generator to mark empty language.
EmptyStringLanguage	Generator with Lm(G)={epsilon}.
EventDiagnoser	Computes event-diagnoser w.r.t. failure types.
FtcFaBehaviour	Computation of fault-accommodating behaviours.
FtcFaController	Check properness
FtcInactivityConditions	Construct inactivity conditions.
FtcIsComplete	Test completeness.
FtcIsNonconflicting	Check for a non-conflicting self-reconfiguring closed-loop system.
FtcIsProper	Test properness
FtcIsWeakSensorConsistent	Test weak sensor-consistency.
FtcNomController	Compute nominal controller.
FtcPermanentBreakdown	Construct plant-failure model for actuator failure-pattern "Permanent Breakdown"
FtcPermanentMute	Construct plant-failure model for failure-pattern "Permanent Mute"
FtcPermanentOperation	Construct plant-failure model for failure-pattern "Permanent Operation"
FtcRandomTrigger	Construct plant-failure model for failure-pattern "Random Trigger"
FtcReconfigurator	Compute universal reconfigurator.
FtcReconfiguratorTimed	Compute universal reconfigurator. Use controllabity for timed DES.
FtcRecurrentBreakdown	Construct plant-failure model for failure-pattern "Recurrent Breakdown"
FtcRecurrentMute	Construct plant-failure model for failure-pattern "Recurrent Mute"
FtcSupComplete	Computate the supremal complete sublanguage.
FtcSupWeakSensorConsistent	Computation of the supremal weak sensor-consistent sublanguage
FtcVirtualise	Virtualise a generator or an alphabet
FullLanguage	Generator with Lm(G)=Sigma*.
HioFreeInput	Enforces free input for I/O dynamics by adding error behaviour.
HioShuffle	Shuffle-composition of two HioPlant systems.
HioSynth	Basic I/O controller synthesis procedure, without parameter check.
HioSynthHierarchical	I/O-Controller synthesis, hierarchical version.
HioSynthMonolithic	I/O-Controller synthesis, monolithic version.
InsertRelabeledEvents	Apply relabeling map to specified generator.
IntegerSum	Sum of integer arguments.
InvProject	Inverse projection of marked and generated language.
IoFreeInput	Inserts transitions to obtain a free input.
IoSynthesis	Controller synthesis for I/O systems.
IoSynthesisNB	Controller synthesis for I/O systems (marked languages).
IsAccessible	Tests a generator for accessibility.
IsCoDiagnosable	Tests for co-diagnosability w.r.t. local observations.
IsCoaccessible	Tests a generator for coaccessibility.
IsComplete	Test completeness of a generator.
IsConditionalClosed	Tests for conditional closedness.
IsConditionalControllable	Tests for conditional controllability.
IsConditionalDecomposable	Tests for conditional decomposability.
IsControllable	Tests controllablity condition.
IsDeterministic	Test for determinsim.
IsEmptyLanguage	Test Generator G for empty marked language Lm(G).
IsEventDiagnosable	Tests for event-diagnosability w.r.t. failure types.
IsHioConstraintForm	Test for dynamics compatible with the formal definition of I/O constraints.
IsHioControllerForm	Test for dynamics compatible the formal definition of I/O controllers.
IsHioEnvironmentForm	Test for dynamics compatible the formal definition of the I/O environments.
IsHioPlantForm	Test for dynamics compatible with the formal definition of I/O plants.
IsIndicatorEventDiagnosable	Tests for event-diagnosability w.r.t. failure types incl. indicator events.
IsInputLocallyFree	Test for the input to be locally free.
IsInputOmegaFree	Test for the input to be free in the behavioral sense.
IsIoSystem	Test for basic I/O properties.
IsLanguageDiagnosable	Tests for language-diagnosability w.r.t. a specification language.
IsLocallyControlConsistent	Verification of local control consistency (LCC).
IsLoopPreservingObserver	Tests if a given projection is a loop-preserving observer.
IsModularDiagnosable	Tests for modular diagnosability w.r.t. local specifications for each subsystem.
IsMsaObserver	Verification of the msa-observer property.
IsMtcObserver	Verification of the observer property.
IsMutuallyControllable	Test mutual controllability of two generators
IsNaturalObserver	Verification of the natural observer property.
IsNonblocking	Test a generator/ two languages for being nonblocking.
IsNormal	Tests normality condition.
IsOmegaClosed	Tests a language for being omega-closed.
IsOmegaControllable	Test controllablity condition.
IsOmegaTrim	Tests a generator for omega trimness.
IsOutputControlConsistent	Verification of output control consistency (OCC).
IsPrefixClosed	Tests a language for being prefix-closed.
IsRelativelyMarked	Test for relative marking.
IsRelativelyOmegaClosed	Test for relative omega-closedness.
IsRelativelyPrefixClosed	Test for relative prefix-closedness.
IsStdSynthesisConsistent	Test consistency of an abstraction w.r.t. standard controller synthesis.
IsStronglyCoaccessible	Tests a colored generator for strong coaccessibility.
IsStronglyTrim	Tests a colored generator for strong trimness.
IsTrim	Tests a generator for trimness.
KleeneClosure	Compute Kleene closure for given language.
LanguageComplement	Computes the complement of a language.
LanguageConcatenate	Concatenates two languages.
LanguageDiagnoser	Computes event-diagnoser w.r.t. failure types.
LanguageDifference	Computes the difference of two languages.
LanguageDisjoint	Tests whether two languages are disjoint.
LanguageEquality	Tests whether two languages are equal.
LanguageInclusion	Tests whether a languages includes another language.
LanguageIntersection	Computes the intersection of languages.
LanguageUnion	Computes the union of languages.
LoopPreservingObserver	Compute a loop-preserving observer from a given initial alphabet.
MarkAllStates	Mark all states in generator.
ModularDiagnoser	Compute diagnoser for subsystems with local specifications.
MsaObserver	Marked string accepting (MSA) observer computation by alphabet extension.
MsaObserverLcc	Marked string accepting (MSA) observer computation with local control consistency (LCC) condition by alphabet extension.
MtcDeterministic	Powerset construction to enforce determinism incl. colored markings.
MtcInvProject	Inverse projection of colored languages.
MtcNaturalObserver	Copmute a colored natural observer by extending a given high-level alphabet.
MtcParallel	Parallel composition of two colored genertors.
MtcProject	Natural projection of colored languages.
MtcProjectNonDet	Natural projection of colored languages, non deterministic version.
MtcStateMin	State spsce minimisation w.r.t. colored languages
MtcSupConClosed	Computes the supremal controllable sublanguage.
MtcSupConNB	Supremal controllable sublanguage with colored marking nonblocking condition.
NaturalObserverExtension	Natural observer computation by alphabet extension.
NaturalObserverLcc	Natural observer computation with local control consistency (LCC) condition by alphabet extension.
NaturalObserverRelabeling	Natural observer computation with event relabeling.
OmegaClosure	Compute omega closure for given language.
OmegaConNB	Synthesis for omega-languages.
OmegaConNormNB	Synthesis for omega-languages (experimental!).
OmegaParallel	Parallel composition with relaxed acceptance condition.
OmegaProduct	Product composition for Buechi acceptance condition.
OmegaSupConNB	Synthesis for omega-languages.
OmegaSupConNormNB	Synthesis for omega-languages (experimental!).
OmegaTrim	Delete states to achieve omega-trimness.
OptimalColorSet	Compute an optimal subset of the colors that should be removed.
Parallel	Computes the parallel composition of two or more generators.
PrefixClosure	Compute prefix closure for given language.
Product	Computes the product composition of two genertors.
Project	Natural projection of marked and generated language.
SelfLoop	Self loop with specified alphabet.
StateMin	Stateset minimization.
StronglyCoaccessible	Delete non-stronly-coaccessible states and transitions.
StronglyTrim	Delete non-strongly-coaccessible and non-accessible states and transitions.
SupConClosed	Computes the supremal controllable sublanguage.
SupConCmplClosed	Computes the supremal controllable and complete sublanguage.
SupConCmplNB	Computes the supremal controllable and complete sublanguage.
SupConNB	Computes the supremal controllable sublanguage.
SupConNormClosed	Computes the supremal controllable, normal and closed sublanguage.
SupConNormCmplNB	Computes the supremal controllable normal and complete sublanguage.
SupConNormNB	Computes the supremal controllable and normal sublanguage.
SupConditionalControllable	Computation of the supremal conditionally controllable sublanguage of the specification K
SupNorm	Computes the supremal normal sublanguage.
SupNormClosed	Computes the supremal normal and closed sublanguage.
SupReduce	Compute a reduced supervisor.
SupRelativelyPrefixClosed	Computes the supremal relatively prefix-closed sublanguage.
SupTconNB	Computes the supremal controllable sublanguage w.r.t. forcible/preemptyble events.
Trim	Delete non-coaccessible and non-accessible states and transitions.
UniqueInit	Enforce unique initial state.
ccTrim	A bit more efficient trim operation based on graph algorithms.

libFAUDES 2.32b --- 2024.03.08 --- with "synthesis-observer-diagnosis-iosystem-hiosys-multitasking-coordinationcontrol-timed-iodevice-simulator-luabindings"