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
OmegaAut
- OmegaAut
- Introduction
- Buechi-Functions
- Buechi-Control
Priorities
Simulator
- Simulator
- Introduction
- Executor Classes
- Hardware-In-The-Loop
- IO-Devices
- Simulator Interconnection
Synthesis
- Synthesis
- Introduction
- Controllability
- Normality
- Completeness
- 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.
BuechiClosure	Realise topological closure for given language.
BuechiCon	OmegaAut for omega-languages.
BuechiConNorm	OmegaAut for omega-languages (experimental!).
BuechiParallel	Parallel composition with relaxed acceptance condition.
BuechiProduct	Product composition for Buechi acceptance condition.
BuechiTrim	Delete states to achieve omega-trimness.
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 (marked languages).
IoSynthesisClosed	Controller synthesis for I/O systems.
IsAccessible	Tests a generator for accessibility.
IsBuechiClosed	Tests a language for being topolicigally closed.
IsBuechiControllable	Test controllablity condition.
IsBuechiRelativelyClosed	Test for relative closedness of Buechi accepted language
IsBuechiTrim	Tests a Buechi automaton for trimness.
IsClosed	Tests a language for being prefix-closed.
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.
IsOutputControlConsistent	Verification of output control consistency (OCC).
IsPNonblocking	Test for nonblockingness with prioritiesed events.
IsRelativelyClosed	Test for relative prefix-closedness.
IsRelativelyMarked	Test for relative marking.
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
MtcSupCon	Supremal controllable sublanguage with colored marking nonblocking condition.
MtcSupConClosed	Computes the supremal controllable sublanguage.
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.
OptimalColorSet	Compute an optimal subset of the colors that should be removed.
Parallel	Computes the parallel composition of two or more generators.
ParallelLive	Computes the parallel composition of multiple 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.
ShapePriorities	Shape a generator by prioritiesing events.
StateMin	Stateset minimization.
StronglyCoaccessible	Delete non-stronly-coaccessible states and transitions.
StronglyTrim	Delete non-strongly-coaccessible and non-accessible states and transitions.
SupBuechiCon	OmegaAut for omega-languages.
SupBuechiConNorm	OmegaAut for omega-languages (experimental!).
SupClosed	Computes the supremal prefix-closed sublanguage.
SupCon	Computes the supremal controllable sublanguage.
SupConClosed	Computes the supremal controllable sublanguage.
SupConCmpl	Computes the supremal controllable and complete sublanguage.
SupConCmplClosed	Computes the supremal controllable and complete sublanguage.
SupConNorm	Computes the supremal controllable and normal sublanguage.
SupConNormClosed	Computes the supremal controllable, normal and closed sublanguage.
SupConNormCmpl	Computes the supremal controllable normal and complete 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.
SupRelativelyClosed	Computes the supremal relatively prefix-closed sublanguage.
SupTcon	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.33h --- 2025.06.17 --- with "synthesis-omegaaut-observer-diagnosis-iosystem-hiosys-multitasking-coordinationcontrol-timed-iodevice-priorities-simulator-luabindings"