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. |