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:


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:

AccessibleDelete non-accessible states and transitions.
AlphabetDifferenceDifference of two alphabets.
AlphabetEqualityTests whether two alphabets match.
AlphabetExtractExtract alphabet from generator.
AlphabetInclusionTests whether an alphabet includes another alphabet.
AlphabetIntersectionIntersection over alphabets.
AlphabetLanguageGenerator with Lm(G)=Sigma.
AlphabetUnionUnion over Alphabets
AutomatonConvert generator to formal automaton.
CoaccessibleDelete non-coaccessible states and transitions.
CompleteDelete states that evolve into a terminal state.
ConDecExtensionExtension of Ek for K to become conditionally decomposable.
DecentralizedDiagnoserComputes decentralized diagnosers for multiple local sites.
DecentralizedModularDiagnoserComputes decentralized diagnosers for systems that consist of multiple components.
DeterministicPowerset construction to enforce determinism.
EmptyLanguageSet generator to mark empty language.
EmptyStringLanguageGenerator with Lm(G)={epsilon}.
EventDiagnoserComputes event-diagnoser w.r.t. failure types.
FtcFaBehaviourComputation of fault-accommodating behaviours.
FtcFaControllerCheck properness
FtcInactivityConditionsConstruct inactivity conditions.
FtcIsCompleteTest completeness.
FtcIsNonconflictingCheck for a non-conflicting self-reconfiguring closed-loop system.
FtcIsProperTest properness
FtcIsWeakSensorConsistentTest weak sensor-consistency.
FtcNomControllerCompute nominal controller.
FtcPermanentBreakdownConstruct plant-failure model for actuator failure-pattern "Permanent Breakdown"
FtcPermanentMuteConstruct plant-failure model for failure-pattern "Permanent Mute"
FtcPermanentOperationConstruct plant-failure model for failure-pattern "Permanent Operation"
FtcRandomTriggerConstruct plant-failure model for failure-pattern "Random Trigger"
FtcReconfiguratorCompute universal reconfigurator.
FtcReconfiguratorTimedCompute universal reconfigurator. Use controllabity for timed DES.
FtcRecurrentBreakdownConstruct plant-failure model for failure-pattern "Recurrent Breakdown"
FtcRecurrentMuteConstruct plant-failure model for failure-pattern "Recurrent Mute"
FtcSupCompleteComputate the supremal complete sublanguage.
FtcSupWeakSensorConsistentComputation of the supremal weak sensor-consistent sublanguage
FtcVirtualiseVirtualise a generator or an alphabet
FullLanguageGenerator with Lm(G)=Sigma*.
HioFreeInputEnforces free input for I/O dynamics by adding error behaviour.
HioShuffleShuffle-composition of two HioPlant systems.
HioSynthBasic I/O controller synthesis procedure, without parameter check.
HioSynthHierarchicalI/O-Controller synthesis, hierarchical version.
HioSynthMonolithicI/O-Controller synthesis, monolithic version.
InsertRelabeledEventsApply relabeling map to specified generator.
IntegerSumSum of integer arguments.
InvProjectInverse projection of marked and generated language.
IoFreeInputInserts transitions to obtain a free input.
IoSynthesisController synthesis for I/O systems.
IoSynthesisNBController synthesis for I/O systems (marked languages).
IsAccessibleTests a generator for accessibility.
IsCoDiagnosableTests for co-diagnosability w.r.t. local observations.
IsCoaccessibleTests a generator for coaccessibility.
IsCompleteTest completeness of a generator.
IsConditionalClosedTests for conditional closedness.
IsConditionalControllableTests for conditional controllability.
IsConditionalDecomposableTests for conditional decomposability.
IsControllableTests controllablity condition.
IsDeterministicTest for determinsim.
IsEmptyLanguageTest Generator G for empty marked language Lm(G).
IsEventDiagnosableTests for event-diagnosability w.r.t. failure types.
IsHioConstraintFormTest for dynamics compatible with the formal definition of I/O constraints.
IsHioControllerFormTest for dynamics compatible the formal definition of I/O controllers.
IsHioEnvironmentFormTest for dynamics compatible the formal definition of the I/O environments.
IsHioPlantFormTest for dynamics compatible with the formal definition of I/O plants.
IsIndicatorEventDiagnosableTests for event-diagnosability w.r.t. failure types incl. indicator events.
IsInputLocallyFreeTest for the input to be locally free.
IsInputOmegaFreeTest for the input to be free in the behavioral sense.
IsIoSystemTest for basic I/O properties.
IsLanguageDiagnosableTests for language-diagnosability w.r.t. a specification language.
IsLocallyControlConsistentVerification of local control consistency (LCC).
IsLoopPreservingObserverTests if a given projection is a loop-preserving observer.
IsModularDiagnosableTests for modular diagnosability w.r.t. local specifications for each subsystem.
IsMsaObserverVerification of the msa-observer property.
IsMtcObserverVerification of the observer property.
IsMutuallyControllableTest mutual controllability of two generators
IsNaturalObserverVerification of the natural observer property.
IsNonblockingTest a generator/ two languages for being nonblocking.
IsNormalTests normality condition.
IsOmegaClosedTests a language for being omega-closed.
IsOmegaControllableTest controllablity condition.
IsOmegaTrimTests a generator for omega trimness.
IsOutputControlConsistentVerification of output control consistency (OCC).
IsPrefixClosedTests a language for being prefix-closed.
IsRelativelyMarkedTest for relative marking.
IsRelativelyOmegaClosedTest for relative omega-closedness.
IsRelativelyPrefixClosedTest for relative prefix-closedness.
IsStdSynthesisConsistentTest consistency of an abstraction w.r.t. standard controller synthesis.
IsStronglyCoaccessibleTests a colored generator for strong coaccessibility.
IsStronglyTrimTests a colored generator for strong trimness.
IsTrimTests a generator for trimness.
KleeneClosureCompute Kleene closure for given language.
LanguageComplementComputes the complement of a language.
LanguageConcatenateConcatenates two languages.
LanguageDiagnoserComputes event-diagnoser w.r.t. failure types.
LanguageDifferenceComputes the difference of two languages.
LanguageDisjointTests whether two languages are disjoint.
LanguageEqualityTests whether two languages are equal.
LanguageInclusionTests whether a languages includes another language.
LanguageIntersectionComputes the intersection of languages.
LanguageUnionComputes the union of languages.
LoopPreservingObserverCompute a loop-preserving observer from a given initial alphabet.
MarkAllStatesMark all states in generator.
ModularDiagnoserCompute diagnoser for subsystems with local specifications.
MsaObserverMarked string accepting (MSA) observer computation by alphabet extension.
MsaObserverLccMarked string accepting (MSA) observer computation with local control consistency (LCC) condition by alphabet extension.
MtcDeterministicPowerset construction to enforce determinism incl. colored markings.
MtcInvProjectInverse projection of colored languages.
MtcNaturalObserverCopmute a colored natural observer by extending a given high-level alphabet.
MtcParallelParallel composition of two colored genertors.
MtcProjectNatural projection of colored languages.
MtcProjectNonDetNatural projection of colored languages, non deterministic version.
MtcStateMinState spsce minimisation w.r.t. colored languages
MtcSupConClosedComputes the supremal controllable sublanguage.
MtcSupConNBSupremal controllable sublanguage with colored marking nonblocking condition.
NaturalObserverExtensionNatural observer computation by alphabet extension.
NaturalObserverLccNatural observer computation with local control consistency (LCC) condition by alphabet extension.
NaturalObserverRelabelingNatural observer computation with event relabeling.
OmegaClosureCompute omega closure for given language.
OmegaConNBSynthesis for omega-languages.
OmegaConNormNBSynthesis for omega-languages (experimental!).
OmegaParallelParallel composition with relaxed acceptance condition.
OmegaProductProduct composition for Buechi acceptance condition.
OmegaSupConNBSynthesis for omega-languages.
OmegaSupConNormNBSynthesis for omega-languages (experimental!).
OmegaTrimDelete states to achieve omega-trimness.
OptimalColorSetCompute an optimal subset of the colors that should be removed.
ParallelComputes the parallel composition of two or more generators.
PrefixClosureCompute prefix closure for given language.
ProductComputes the product composition of two genertors.
ProjectNatural projection of marked and generated language.
SelfLoopSelf loop with specified alphabet.
StateMinStateset minimization.
StronglyCoaccessibleDelete non-stronly-coaccessible states and transitions.
StronglyTrimDelete non-strongly-coaccessible and non-accessible states and transitions.
SupConClosedComputes the supremal controllable sublanguage.
SupConCmplClosedComputes the supremal controllable and complete sublanguage.
SupConCmplNBComputes the supremal controllable and complete sublanguage.
SupConNBComputes the supremal controllable sublanguage.
SupConNormClosedComputes the supremal controllable, normal and closed sublanguage.
SupConNormCmplNBComputes the supremal controllable normal and complete sublanguage.
SupConNormNBComputes the supremal controllable and normal sublanguage.
SupConditionalControllableComputation of the supremal conditionally controllable sublanguage of the specification K
SupNormComputes the supremal normal sublanguage.
SupNormClosedComputes the supremal normal and closed sublanguage.
SupReduceCompute a reduced supervisor.
SupRelativelyPrefixClosedComputes the supremal relatively prefix-closed sublanguage.
SupTconNBComputes the supremal controllable sublanguage w.r.t. forcible/preemptyble events.
TrimDelete non-coaccessible and non-accessible states and transitions.
UniqueInitEnforce unique initial state.
ccTrimA bit more efficient trim operation based on graph algorithms.

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