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
Example
FaultTolerantControl
- FaultTolerantControl
- Introduction
- Example
- Fault-Accommodation
- Reconfiguration
- Fault-Patterns
HioSys
- HioSys
- Introduction
- Step-By-Step
- Synthesis Procedure
- Liveness Properties
- Application Example
Hybrid
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
- Rabin-Functions
- Buechi-Control
- Rabin-Control
- Partial-Obs-Control
Priorities
Simulator
- Simulator
- Introduction
- Executor Classes
- Hardware-In-The-Loop
- IO-Devices
- Simulator Interconnection
Synthesis
- Synthesis
- Introduction
- Controllability
- Normality
- Completeness
- Misc Functions
Types
ColorSet
MtcSystem
Functions
IsMtcObserver
IsStronglyCoaccessible
IsStronglyTrim
MtcDeterministic
MtcInvProject
MtcNaturalObserver
MtcParallel
MtcProject
MtcStateMin
MtcSupCon
MtcSupConClosed
OptimalColorSet
StronglyCoaccessible
StronglyTrim

Reachability Tests/Conversions

Due to colored marking of states, MtcSystems allow for variations on the notion of coaccessibility, and, hence, trimmness. Note that accessibility is not affected.

IsStronglyCoaccessible

Tests a colored generator for strong coaccessibility.

Signature:

IsStronglyCoaccessible(+In+ MtcSystem G, +Out+ Boolean BRes)

IsStronglyTrim

Tests a colored generator for strong trimness.

Signature:

IsStronglyTrim(+In+ MtcSystem G, +Out+ Boolean BRes)

StronglyCoaccessible

Delete non-stronly-coaccessible states and transitions.

Signature:

StronglyCoaccessible(+InOut+ MtcSystem G)

StronglyCoaccessible(+In+ MtcSystem GArg, +Out+ MtcSystem GRes)

StronglyTrim

Delete non-strongly-coaccessible and non-accessible states and transitions.

Signature:

StronglyTrim(+InOut+ MtcSystem G)

StronglyTrim(+In+ MtcSystem GArg, +Out+ MtcSystem GRes)

libFAUDES 2.34e --- 2026.03.16 --- with "omegaaut-synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-priorities-luabindings-hybrid-example-pybindings"