faudes Namespace Reference

libFAUDES resides within the namespace faudes. More...

Classes

class  TaGenerator
 Generator with specified attribute types. More...
 
class  AttributeVoid
 Minimal Attribute. More...
 
class  AttributeFlags
 Boolean flags Attribute. More...
 
class  TAttrMap
 Attribute interface for TBaseSet. More...
 
class  TBaseSet
 STL style set template. More...
 
class  vBaseVector
 Vector bass class. More...
 
class  TBaseVector
 Vector template. More...
 
class  BisimulationCTA
 The Bisimulation class The following class implements a basic normal bisimulation partition algorithms and derives a class for partitioning w.r.t. delayed bisimulation and weak bisimulation . All these algorithms are introduced in "Computing Maximal Weak and Other Bisimulations" from Alexandre Boulgakov et. al. (2016). The utilised normal bisimulation algorithm originates from the "change tracking algorithm" from Stefan Blom and Simona Orzan (see ref. of cited paper). Besides, the current paper uses topological sorted states to avoid computing saturated transitions explicitly when computing delayed and weak bisimulation. More...
 
class  AbstractBisimulationCTA
 The DelayedBisimulation class Derived from Bisimulation class. We implement the "two-pass change-tracking" algorithm from the cited paper. More...
 
class  TopoSort
 The TopoSort class perform a topological sort on states of a given automaton. if s1 is before s2 in the sort then there is no path from s2 to s1. The algorithm can be found in https://en.wikipedia.org/wiki/Topological_sorting under depth-first search, which is considered as first invented by R. Tarjan in 1976. More...
 
struct  Pnode
 
class  Bisimulation
 
class  AttributeCFlags
 Attribute class to model event controllability properties. More...
 
class  TcGenerator
 Generator with controllability attributes. More...
 
class  Integer
 Elementary type. More...
 
class  String
 Elementary type. More...
 
class  Boolean
 Elementary type. More...
 
class  Exception
 Faudes exception class. More...
 
class  Parameter
 Structure to model a parameter type within the Signature of a Function. More...
 
class  Signature
 Signature of a Function. More...
 
class  FunctionDefinition
 A FunctionDefinition defines the interface to a faudes-function. More...
 
class  Function
 A faudes-function hosts parameter values of some faudes type and provides a method to perform an operation on the specified paramters, e.g. More...
 
class  vGenerator
 Base class of all FAUDES generators. More...
 
class  SccFilter
 Filter for strictly connected components (SCC) search/compute routines. More...
 
class  ConsoleOut
 Console Out. More...
 
class  ObjectCount
 Debugging counter. More...
 
class  TaIndexSet
 Set of indices with attributes. More...
 
class  IndexSet
 Set of indices. More...
 
class  TaNameSet
 Set of indices with symbolic names and attributes. More...
 
class  NameSet
 Set of indices with symbolic names. More...
 
class  OPState
 
class  ProductCompositionMap
 Rti-wrapper for composition maps. More...
 
struct  TGraph
 Graph data structure for transitionrelation – EXPERIMENTAL. More...
 
struct  TNode
 A node represents the edges related to one individual vertex. More...
 
struct  graph_iterator_t
 An iterator over the map of all nodes is interpreted as a state incl. More...
 
struct  node_iterator_t
 An iterator over the set of edges related to one vertex is interpreted as a transition. More...
 
struct  node_entry_t
 A node-entry represents one edge. More...
 
struct  TGraph< Idx, Idx >
 Specialisation of the graph template to provide convenience methods addressing the intended ussage. More...
 
class  TypeRegistry
 The TypeRegistry registers faudes-types. More...
 
class  AutoRegisterType
 Auto register faudes-type with specified type name. More...
 
class  AutoRegisterXElementTag
 
class  FunctionRegistry
 The FunctionRegistry registers faudes-functions. More...
 
class  Hopcroft
 
class  SymbolSet
 Set of symbols. More...
 
class  SymbolTable
 A SymbolTable associates sybolic names with indices. More...
 
class  Token
 Tokens model atomic data for stream IO. More...
 
class  TokenReader
 A TokenReader reads sequential tokens from a file or string. More...
 
class  TokenWriter
 A TokenWriter writes sequential tokens to a file, a string or stdout. More...
 
class  Transition
 Triple (X1,Ev,X2) to represent current state, event and next state. More...
 
class  TransSort
 Alternative ordering of Transitions. More...
 
class  TTransSet
 Set of Transitions. More...
 
class  TaTransSet
 Set of Transitions with attributes. More...
 
class  Type
 Base class of all libFAUDES objects that participate in the run-time interface. More...
 
class  Documentation
 faudes type implementation macros, overall More...
 
class  TypeDefinition
 A TypeDefinition defines a faudes-type in that it specifies a faudes-type name to identify the type and a method NewObject() to instantiate objects of the respective type. More...
 
class  ComSyn
 
class  SmallSize
 
class  SNOState
 
struct  ReductionStateInfo
 Data structure for identifying states in the same coset for supervisor reduction. More...
 
class  SOE
 
class  MCtrlPattern
 
class  OPSState
 
class  EventRelabelMap
 Rti convenience wrapper for relabeling maps. More...
 
class  AttributeDiagnoserState
 Implements state estimates for the current status of the generator. More...
 
class  AttributeFailureEvents
 Stores the failure and indicator events for a particular failure type. More...
 
class  AttributeFailureTypeMap
 Partitions the failure and indicator events. More...
 
class  DiagLabelSet
 Implements the label representation for state estimates. More...
 
struct  CoVerifierState
 
class  TdiagGenerator
 Provides the structure and methods to build and handle diagnosers. More...
 
struct  VerifierState
 
class  HioEventFlags
 Event attributes for hierarchical discrete event systems with inputs and outputs. More...
 
class  HioStateFlags
 State attributes for hierarchical discrete event systems with inputs and outputs. More...
 
class  THioConstraint
 Generator with I/O-constraint attributes. More...
 
class  THioController
 Generator with I/O-controller attributes. More...
 
class  THioEnvironment
 Generator with I/O-environment attributes. More...
 
class  HioModule
 Recurring structure in hierarchies designed according to the I/O based DES framework. More...
 
class  THioPlant
 Generator with I/O-plant attributes. More...
 
class  AttributeIosEvent
 Attributes for events in DES with in- and outputs. More...
 
class  AttributeIosState
 Attributes for states in DESs with in- and outputs. More...
 
class  TioGenerator
 Generator with I/O-system attributes. More...
 
class  AttributeColoredState
 State attributes for multitasking automata. More...
 
class  ColorSet
 Container for colors: this is a NameSet with its own static symboltable. More...
 
class  TmtcGenerator
 Allows to create colored marking generators (CMGs) as the common five tupel consisting of alphabet, stateset, transition relation, initial states, marked states, and attributes for state and event properties. More...
 
class  adjlist
 
class  AttributeTimedTrans
 Transition Attribute with guard and resets. More...
 
class  AttributeTimedState
 State attribute with invariant. More...
 
class  AttributeTimedGlobal
 Globat attribute with clockset. More...
 
class  TtGenerator
 Generator with timing extensions. More...
 
class  ClockSet
 Container class to model a set of clocks. More...
 
class  ElemConstraint
 Model of an elementary clock constraint formula. More...
 
class  TimeConstraint
 A TimeConstraint is a set of elementary clock constraints. More...
 
class  Time
 Type to represent time. More...
 
class  TimeInterval
 Model of a time interval. More...
 
class  DiscreteDensityFunction
 Density Function. More...
 
class  SampledDensityFunction
 
class  DeviceExecutor
 Executer with IO device to handle external/physical events. More...
 
class  TimedEvent
 Global Tyoedefs. More...
 
class  Executor
 An Executor is a timed generator that maintains a current state. More...
 
class  LoggingExecutor
 Executor with logging facilities. More...
 
class  ParallelExecutor
 Synchronized parallel execution of TimedGenerators. More...
 
class  ProposingExecutor
 Executer that proposes which transition to execute. More...
 
class  SimEventCondition
 Defining data of event based simulation condition. More...
 
class  SimStateCondition
 Defining data of state based simulation condition. More...
 
class  AttributeSimCondition
 Attribute for a simulation condition. More...
 
class  SimConditionSet
 Set of simulation named conditions. More...
 
class  SimPriorityEventAttribute
 Defining data to prioritise events. More...
 
class  SimStochasticEventAttribute
 Defining data of stochastic behaviour. More...
 
class  SimEventAttribute
 Attribute for an event in the context of simulation. More...
 
class  mbDevice
 Processimage synchronisation via Modbus/TCP. More...
 
class  AttributeSignalOutput
 Configuration of a signal based output mapping. More...
 
class  AttributeSignalInput
 Configuration of a signal based input mapping. More...
 
class  AttributeSignalEvent
 Configuration of a signal based input or output. More...
 
class  sDevice
 An sDevice implements signal based semantics for faudes events. More...
 
class  SimplenetAddress
 Simplenet node address. More...
 
class  AttributeSimplenetOutput
 Configuration of a network output mapping. More...
 
class  AttributeSimplenetInput
 Configuration of a network input mapping. More...
 
class  AttributeSimplenetEvent
 Configuration of a networked input or output. More...
 
class  nDevice
 An nDevice implements networked IO via a simple TCP/IP protocol. More...
 
class  AttributeDeviceEvent
 Attribute for the configuration of a input or output mapping. More...
 
class  vDevice
 Virtual base class to define the interface for event io. More...
 
class  xDevice
 Container of devices. More...
 
struct  swig_cast_info
 
struct  swig_type_info
 
struct  swig_lua_userdata
 
class  LuaFunctionDefinition
 A LuaFunctionDefinition is derived from FunctionDefinition to define a faudes-function by a Lua script. More...
 
class  LuaState
 Wrapper class to maintain a Lua state. More...
 
class  LuaFunction
 A LuaFunction is a faudes-function that executes a luafaudes script. More...
 
class  LbdAbstraction
 
class  AttributeLhaTrans
 Linear hybrid automata transition attribute with guard and resets. More...
 
class  AttributeLhaState
 Linear hybrid automata state attribute with invariant, rates and optional initial state constraint. More...
 
class  AttributeLhaGlobal
 Linear hybrid automata globat attribute to specify the overall state space. More...
 
class  pdata_t
 user data type for polyhedra More...
 
class  rdata_t
 user data type for reset relation (fake faudes type) More...
 
class  Experiment
 Finite fragment of a computation tree. More...
 
class  CompatibleStates
 Abstract dynamics operator, i.e., some set of states, that knows where it eveolves when it next triggers an event. More...
 
class  DesCompatibleStates
 
class  LhaCompatibleStates
 
class  TlhaGenerator
 Generator with linear hybrid automata extensions. More...
 
class  Scalar
 Base type for dense maths. More...
 
class  Matrix
 Matrix of scalars. More...
 
class  Vector
 Vector of scalars. More...
 
class  Polyhedron
 Polyhedron in R^n. More...
 
class  LinearRelation
 Linear relation on R^n. More...
 
class  HybridStateSet
 Set of states in an hybrid automata. More...
 

Typedefs

typedef unsigned long int fType
 Convenience typdef flag data. More...
 
typedef TaNameSet< AttributeCFlagsAlphabet
 Convenience typedef for event sets with controllability attributes. More...
 
typedef TBaseVector< AlphabetAlphaberVector
 Convenience typedef. More...
 
typedef TaNameSet< AttributeCFlagscEventSet
 Compatibility: pre 2.20b used cEventSet as C++ class name. More...
 
typedef TBaseVector< cEventSetcEventSetVector
 
typedef TcGenerator< AttributeVoid, AttributeVoid, AttributeCFlags, AttributeVoidSystem
 Convenience typedef for std System. More...
 
typedef TBaseVector< SystemSystemVector
 Convenience typedef for vectors of systems. More...
 
typedef TcGenerator< AttributeVoid, AttributeVoid, AttributeCFlags, AttributeVoidcGenerator
 Compatibility: pre 2.20b used cGenerator as C++ class name. More...
 
typedef TBaseVector< cGeneratorcGeneratorVector
 
typedef std::set< std::pair< Idx, Idx > > SetX1Ev
 
typedef uint32_t Idx
 Type definition for index type (allways 32bit) More...
 
typedef long int Int
 Type definition for integer type (let target system decide, minimum 32bit) More...
 
typedef double Float
 Type definition for real type. More...
 
typedef TBaseVector< IntegerIntegerVector
 
typedef vGenerator Generator
 Plain generator, api typedef for generator with no attributes. More...
 
typedef TBaseVector< GeneratorGeneratorVector
 Convenience typedef for vectors og generators. More...
 
typedef IndexSet StateSet
 
typedef TBaseVector< IndexSetIndexSetVector
 Convenience typedef for vectors og generators. More...
 
typedef NameSet EventSet
 Convenience typedef for plain event sets. More...
 
typedef TBaseVector< EventSetEventSetVector
 
typedef TNode< Idx, IdxNode
 
typedef TGraph< Idx, IdxGraph
 
typedef TTransSet< TransSort::X1EvX2TransSet
 Type definition for default sorted TTransSet. More...
 
typedef TTransSet< TransSort::X1EvX2TransSetX1EvX2
 Type definition for default sorted TTransSet. More...
 
typedef TTransSet< TransSort::EvX1X2TransSetEvX1X2
 Type definition for ev, x1, x2 sorted TTransSet. More...
 
typedef TTransSet< TransSort::EvX2X1TransSetEvX2X1
 Type definition for ev, x2, x1 sorted TTransSet. More...
 
typedef TTransSet< TransSort::X2EvX1TransSetX2EvX1
 Type definition for x2, ev, x1 sorted TTransSet. More...
 
typedef TTransSet< TransSort::X2X1EvTransSetX2X1Ev
 Type definition for x2, x1, ev sorted TTransSet. More...
 
typedef TTransSet< TransSort::X1X2EvTransSetX1X2Ev
 Type definition for x1, x2, ev sorted TTransSet. More...
 
typedef TdiagGenerator< AttributeFailureTypeMap, AttributeDiagnoserState, AttributeCFlags, AttributeVoidDiagnoser
 
typedef TdiagGenerator< AttributeFailureTypeMap, AttributeDiagnoserState, AttributeCFlags, AttributeVoiddiagGenerator
 Compatibility: pre 2.20b used diagGenerator as C++ class name. More...
 
typedef THioConstraint< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoidHioConstraint
 
typedef THioController< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoidHioController
 
typedef THioEnvironment< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoidHioEnvironment
 
typedef THioPlant< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoidHioPlant
 
typedef TaNameSet< AttributeIosEventIosEventSet
 
typedef TaIndexSet< AttributeIosStateIosStateSet
 
typedef TioGenerator< AttributeVoid, AttributeIosState, AttributeIosEvent, AttributeVoidIoSystem
 
typedef TmtcGenerator< AttributeVoid, AttributeColoredState, AttributeCFlags, AttributeVoidMtcSystem
 
typedef TmtcGenerator< AttributeVoid, AttributeColoredState, AttributeCFlags, AttributeVoidmtcGenerator
 Compatibility: pre 2.20b used mtcGenerator as C++ class name. More...
 
typedef TtGenerator< AttributeTimedGlobal, AttributeTimedState, AttributeCFlags, AttributeTimedTransTimedGenerator
 Convenience typedef for std TimedGenerator. More...
 
typedef TtGenerator< AttributeTimedGlobal, AttributeTimedState, AttributeCFlags, AttributeTimedTranstGenerator
 Compatibility: pre 2.20b used tGenerator as C++ class name. More...
 
typedef TaNameSet< SimEventAttributesEventSet
 Typedef for events with simulation attributes. More...
 
typedef void *(* swig_converter_func) (void *, int *)
 
typedef struct swig_type_info *(* swig_dycast_func) (void **)
 
typedef struct faudes::swig_cast_info swig_cast_info
 
typedef struct faudes::swig_type_info swig_type_info
 
typedef TlhaGenerator< AttributeLhaGlobal, AttributeLhaState, AttributeCFlags, AttributeLhaTransLinearHybridAutomaton
 Convenience typedef for std lhaGenerator. More...
 
typedef TaTransSet< AttributeLhaTransLhaTransSet
 
typedef TaIndexSet< AttributeLhaStateLhaStateSet
 

Enumerations

enum  VerifierStateLabel { NORMAL , CONFUSED , BLOCK }
 

Functions

template<class T , class Cmp >
void SetUnion (const TBaseSet< T, Cmp > &rSetA, const TBaseSet< T, Cmp > &rSetB, TBaseSet< T, Cmp > &rRes)
 
template<class T , class Cmp >
void SetIntersection (const TBaseSet< T, Cmp > &rSetA, const TBaseSet< T, Cmp > &rSetB, TBaseSet< T, Cmp > &rRes)
 
template<class T , class Cmp >
void SetDifference (const TBaseSet< T, Cmp > &rSetA, const TBaseSet< T, Cmp > &rSetB, TBaseSet< T, Cmp > &rRes)
 
template<class T , class Cmp >
bool SetEquality (const TBaseSet< T, Cmp > &rSetA, const TBaseSet< T, Cmp > &rSetB)
 
template<class T , class Cmp >
bool SetInclusion (const TBaseSet< T, Cmp > &rSetA, const TBaseSet< T, Cmp > &rSetB)
 
bool topoSort (const Generator &rGen, const EventSet &rEvs, std::list< Idx > &result)
 topoSort wrapper for topological sortation rEvs is the set of events which will be considered while sorting More...
 
void ExtendTransRel (Generator &rGen, const EventSet &rSilent, const Idx &rFlag)
 ExtendTransRel perform transition saturation w.r.t. silent evs. Two different saturation modes are set depending on flag value. More...
 
void InstallSelfloops (Generator &rGen, const EventSet &rEvs)
 InstallSelfloops install selfloops on all states of given event set. intended to install silent event selfloops for saturation. More...
 
void ComputeBisimulationCTA (const Generator &rGen, std::list< StateSet > &rResult)
 ComputeBisimulationCTA basic bisimulation partition algorithm based on change-tracking algorithm. More...
 
void ComputeBisimulationCTA (const Generator &rGen, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
 ComputeBisimulationCTA basic bisimulation partition algorithm under prepartition based on change-tracking algorithm. More...
 
void ComputeDelayedBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult)
 
void ComputeBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
 
void ComputeWeakBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult)
 ComputeWeakBisimulationCTA weak bisimulation (aka observation eq) partition based on change-tracking algorithm and topo sort. More...
 
void ComputeWeakBisimulation (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
 
void ComputeAbstractBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const Idx &rFlag, const std::vector< StateSet > &rPrePartition)
 ComputeAbstractBisimulationSatCTA saturation and change-tracking based partition algorithm for either delayed or weak bisimulation. This function is intended to be invoked by ComputeDelayedBisimulation_Sat or ComputeWeakBisimulation_Sat, not for direct external usage. More...
 
void ComputeDelayedBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult)
 ComputeDelayedBisimulationSatCTA delayed bisimulation partition based on change-tracking algorithm and saturation. More...
 
void ComputeWeakBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult)
 ComputeWeakBisimulationSatCTA weak bisimulation (aka observation eq) partition based on change-tracking algorithm and saturation. More...
 
void ComputeDelayedBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
 
void ComputeWeakBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
 
FAUDES_API void FactorTauLoops (Generator &rGen, const Idx &rSilent)
 FactorTauLoops merge silent loop and then remove silent self loops. More...
 
FAUDES_API void ComputeBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult)
 ComputeBisimulationCTA bisimulation partition based on change-tracking algorithm and topo sort. More...
 
FAUDES_API void ComputeDelayedBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
 ComputeDelayedBisimulationCTA delayed bisimulation partition under prepartition based on change-tracking algorithm and topo sort. More...
 
FAUDES_API void ComputeWeakBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
 ComputeWeakBisimulationCTA weak bisimulation (aka observation eq) partition under prepartition based on change-tracking algorithm and topo sort. More...
 
FAUDES_API void ComputeComputeWeakBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
 ComputeComputeWeakBisimulationSatCTA weak bisimulation partition under prepartition based on change-tracking algorithm and saturation. More...
 
void ComputeBisimulation (const Generator &rGenOrig, map< Idx, Idx > &rMapStateToPartition)
 Computation of the coarsest bisimulation relation for a specified generator. More...
 
void ComputeBisimulation (const Generator &rGenOrig, map< Idx, Idx > &rMapStateToPartition, Generator &rGenPart)
 Computation of the coarsest bisimulation relation for a specified generator. More...
 
void ComputeBisimulation (const Generator &rGenOrig, std::list< StateSet > &rPartitions)
 Computation of the coarsest bisimulation relation for a specified generator. More...
 
FAUDES_API void ComputeBisimulation (const Generator &rGenOrig, std::map< Idx, Idx > &rMapStateToPartition)
 Computation of the coarsest bisimulation relation for a specified generator. More...
 
FAUDES_API void ComputeBisimulation (const Generator &rGenOrig, std::map< Idx, Idx > &rMapStateToPartition, Generator &rGenPart)
 Computation of the coarsest bisimulation relation for a specified generator. More...
 
void AppendOmegaTermination (Generator &rGen)
 
void MergeEquivalenceClasses (Generator &rGen, TransSetX2EvX1 &rRevTrans, const std::list< StateSet > &rClasses)
 
void ObservationEquivalentQuotient (Generator &g, const EventSet &silent)
 
void IncomingTransSet (const Generator &rGen, const TransSetX2EvX1 &rRTrans, const EventSet &silent, const Idx &state, SetX1Ev &result)
 
void ActiveNonTauEvs (const Generator &rGen, const EventSet &silent, const Idx &state, EventSet &result)
 
std::map< SetX1Ev, StateSetIncomingEquivalentClasses (const Generator &rGen, const EventSet &silent)
 
void ActiveEventsRule (Generator &g, const EventSet &silent)
 
void EnabledContinuationRule (Generator &g, const EventSet &silent)
 
void RemoveTauSelfloops (Generator &g, const EventSet &silent)
 
void MergeSilentLoops (Generator &g, const EventSet &silent)
 
void RemoveNonCoaccessibleOut (Generator &g)
 
void BlockingSilentEvent (Generator &g, const EventSet &silent)
 
void MergeNonCoaccessible (Generator &g)
 
void OnlySilentIncoming (Generator &g, const EventSet &silent)
 
void OnlySilentOutgoing (Generator &g, const EventSet &silent)
 
EventSet HidePriviateEvs (Generator &rGen, EventSet &silent)
 
void RemoveTauLoops (Generator &rGen, const EventSet &silent)
 Remove all silent loops in a given automaton. More...
 
void ConflictEquivalentAbstractionOnce (Generator &rGen, EventSet &silent)
 
void ConflictEquivalentAbstractionLoop (vGenerator &rGen, EventSet &rSilentEvents)
 
void ConflictEquivalentAbstraction (vGenerator &rGen, EventSet &rSilentEvents)
 Conflict equivalent abstraction. More...
 
bool IsNonconflicting (const GeneratorVector &rGenVec)
 Test for conflicts. More...
 
bool IsNonblocking (const GeneratorVector &rGvec)
 
void UniqueInit (Generator &rGen)
 Make initial states unique. More...
 
void UniqueInit (const Generator &rGen, Generator &rResGen)
 Make initial states unique. More...
 
void Deterministic (const Generator &rGen, Generator &rResGen)
 Make generator deterministic. More...
 
void aDeterministic (const Generator &rGen, Generator &rResGen)
 Make generator deterministic. More...
 
void Deterministic (const Generator &rGen, std::map< Idx, StateSet > &rEntryStatesMap, Generator &rResGen)
 Make generator deterministic. More...
 
void Deterministic (const Generator &rGen, std::vector< StateSet > &rPowerStates, std::vector< Idx > &rDetStates, Generator &rResGen)
 Make generator deterministic. More...
 
long int IntegerSum (const Integer &arg1, const Integer &arg2)
 
long int IntegerSum (const IntegerVector &intvect)
 
bool IsAccessible (const vGenerator &rGen)
 RTI wrapper function. More...
 
bool IsCoaccessible (const vGenerator &rGen)
 RTI wrapper function. More...
 
bool IsTrim (const vGenerator &rGen)
 RTI wrapper function. More...
 
bool IsOmegaTrim (const vGenerator &rGen)
 RTI wrapper function. More...
 
bool IsComplete (const vGenerator &rGen)
 RTI wrapper function. More...
 
bool IsComplete (const vGenerator &rGen, const StateSet &rStateSet)
 
bool IsComplete (const vGenerator &rGen, const EventSet &rSigmaO)
 RTI wrapper function. More...
 
bool IsDeterministic (const vGenerator &rGen)
 RTI wrapper function. More...
 
void Accessible (vGenerator &rGen)
 RTI wrapper function. More...
 
void Accessible (const vGenerator &rGen, vGenerator &rRes)
 RTI wrapper function. More...
 
void Coaccessible (vGenerator &rGen)
 RTI wrapper function. More...
 
void Coaccessible (const vGenerator &rGen, vGenerator &rRes)
 RTI wrapper function. More...
 
void Complete (vGenerator &rGen)
 RTI wrapper function. More...
 
void Complete (const vGenerator &rGen, vGenerator &rRes)
 RTI wrapper function. More...
 
void Complete (vGenerator &rGen, const EventSet &rSigmaO)
 RTI wrapper function. More...
 
void Complete (const vGenerator &rGen, const EventSet &rSigmaO, vGenerator &rRes)
 RTI wrapper function. More...
 
void Trim (vGenerator &rGen)
 RTI wrapper function. More...
 
void Trim (const vGenerator &rGen, vGenerator &rRes)
 RTI wrapper function. More...
 
void OmegaTrim (vGenerator &rGen)
 RTI wrapper function. More...
 
void OmegaTrim (const vGenerator &rGen, vGenerator &rRes)
 RTI wrapper function. More...
 
void MarkAllStates (vGenerator &rGen)
 RTI wrapper function. More...
 
void AlphabetExtract (const vGenerator &rGen, EventSet &rRes)
 RTI wrapper function. More...
 
void SetIntersection (const GeneratorVector &rGenVec, EventSet &rRes)
 RTI convenience function. More...
 
void SetUnion (const GeneratorVector &rGenVec, EventSet &rRes)
 RTI convenience function. More...
 
void SetIntersection (const vGenerator &rGenA, const vGenerator &rGenB, EventSet &rRes)
 RTI convenience function. More...
 
void SetUnion (const vGenerator &rGenA, const vGenerator &rGenB, EventSet &rRes)
 RTI convenience function. More...
 
void SetDifference (const vGenerator &rGenA, const vGenerator &rGenB, EventSet &rRes)
 RTI convenience function. More...
 
void SearchScc (const Idx vState, int &vRcount, const Generator &rGen, const SccFilter &rFilter, StateSet &rTodo, std::stack< Idx > &rStack, StateSet &rStackStates, std::map< const Idx, int > &rDfn, std::map< const Idx, int > &rLowLnk, std::list< StateSet > &rSccList, StateSet &rRoots)
 Search for strongly connected components (SCC). More...
 
bool ComputeScc (const Generator &rGen, const SccFilter &rFilter, std::list< StateSet > &rSccList, StateSet &rRoots)
 Compute strongly connected components (SCC) More...
 
bool ComputeScc (const Generator &rGen, std::list< StateSet > &rSccList, StateSet &rRoots)
 Compute strongly connected components (SCC) More...
 
bool ComputeScc (const Generator &rGen, const SccFilter &rFilter, Idx q0, StateSet &rScc)
 Compute strongly connected component (SCC) More...
 
bool ComputeScc (const Generator &rGen, const SccFilter &rFilter, StateSet &rScc)
 Compute one strongly connected component (SCC) More...
 
bool HasScc (const Generator &rGen, const SccFilter &rFilter)
 Test for strongly connected components (SCC) More...
 
bool ComputeNextScc (const Generator &rGen, SccFilter &rFilter, StateSet &rScc)
 Compute next SCC. More...
 
std::string ToStringInteger (Int number)
 integer to string More...
 
std::string ToStringInteger16 (Int number)
 integer to string base 16 More...
 
std::string ToStringFloat (Float number)
 float to string More...
 
std::string ExpandString (const std::string &rString, unsigned int len)
 Fill string with spaces up to a given length if length of the string is smaller than given length parameter. More...
 
std::string CollapsString (const std::string &rString, unsigned int len=FD_MAXCONTAINERNAME)
 Limit length of string, return head and tail of string. More...
 
Idx ToIdx (const std::string &rString)
 Convert a string to Idx. More...
 
std::string StringSubstitute (const std::string &rString, const std::string &rFrom, const std::string &rTo)
 Substitute in string. More...
 
std::string VersionString ()
 Return FAUDES_VERSION as std::string. More...
 
std::string PluginsString ()
 Return FAUDES_PLUGINS as std::string. More...
 
std::string ContributorsString ()
 Return contributors as std::string. More...
 
void ProcessDot (const std::string &rDotFile, const std::string &rOutFile, const std::string &rOutFormat="", const std::string &rDotExec="dot")
 Convenience function: process dot file to graphics output. More...
 
std::string CreateTempFile (void)
 Create a temp file, length 0. More...
 
bool RemoveFile (const std::string &rFileName)
 Delete a file. More...
 
std::string ExtractDirectory (const std::string &rFullPath)
 Extract directory from full path. More...
 
std::string ExtractFilename (const std::string &rFullName)
 Extract file name from full path. More...
 
std::string ExtractBasename (const std::string &rFullName)
 Extract file name from full path. More...
 
std::string ExtractExtension (const std::string &rFullName)
 Extract file name from full path. More...
 
std::string PrependDirectory (const std::string &rDirectory, const std::string &rFileName)
 Construct full path from directory and filename. More...
 
bool DirectoryExists (const std::string &rDirectory)
 Test existence of directory. More...
 
std::set< std::string > ReadDirectory (const std::string &rDirectory)
 Read the contents of the specified directors. More...
 
bool FileExists (const std::string &rFilename)
 Test existence of file. More...
 
bool FileDelete (const std::string &rFilename)
 Delete file. More...
 
bool FileCopy (const std::string &rFromFile, const std::string &rToFile)
 Copy file. More...
 
void ExitFunction (void)
 
std::string TestProtocol (const std::string &rSource)
 Test Protocol. More...
 
void TestProtocol (const std::string &rMessage, const Type &rData, bool core=false)
 Test Protocol. More...
 
void TestProtocol (const std::string &rMessage, bool data)
 Test Protocol. More...
 
void TestProtocol (const std::string &rMessage, long int data)
 Test Protocol. More...
 
void TestProtocol (const std::string &rMessage, const std::string &data)
 Test Protocol. More...
 
bool TestProtocol (void)
 Test Protocol. More...
 
void LoopCallback (bool pBreak(void))
 
void LoopCallback (void)
 Algorithm loop callback. More...
 
FAUDES_API const std::string & PathSeparator (void)
 Std dir-separator. More...
 
FAUDES_API void LoopCallback (bool(*pBreakFnct)(void))
 Algorithm loop callback. More...
 
StateSet LowExitStates (const Generator &rLowGen, const EventSet &rHighAlph, const std::map< Idx, StateSet > &rEntryStatesMap, const TransSetX2EvX1 &rLowRevTransRel, Idx highState)
 LowExitStates return-copy function: More...
 
void LowExitStates (const EventSet &rHighAlph, const std::map< Idx, StateSet > &rEntryStatesMap, const TransSetX2EvX1 &rLowRevTransRel, Idx highState, StateSet &rLowExitStates)
 LowExitStates call-by-reference function: More...
 
EventSet ReachableEvents (const Generator &rLowGen, const EventSet &rHighAlph, Idx lowState)
 ReachableEvents return-copy function: More...
 
void ReachableEvents (const Generator &rLowGen, const EventSet &rHighAlph, Idx lowState, EventSet &rReachableEvents)
 ReachableEvents call-by-reference function: More...
 
void LocalCoaccessibleReach (const TransSetX2EvX1 &rRevTransRel, const EventSet &rHighAlph, Idx lowState, StateSet &rCoaccessibleReach)
 Compute the coaccessible reach for a local automaton. More...
 
void LocalAccessibleReach (const Generator &rLowGen, const EventSet &rHighAlph, Idx lowState, StateSet &rAccessibleReach)
 Compute the accessible reach for a local automaton. More...
 
void SetIntersection (const EventSetVector &rSetVec, EventSet &rRes)
 
void SetUnion (const EventSetVector &rSetVec, EventSet &rRes)
 
void aOmegaProduct (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Product composition for Buechi automata. More...
 
void OmegaProduct (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Product composition for Buechi automata. More...
 
void aOmegaParallel (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Parallel composition with relaxed acceptance condition. More...
 
void OmegaParallel (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Parallel composition with relaxed acceptance condition. More...
 
void OmegaClosure (Generator &rGen)
 Topological closure. More...
 
bool IsOmegaClosed (const Generator &rGen)
 Test for topologically closed omega language. More...
 
void Parallel (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Parallel composition. More...
 
void aParallel (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Parallel composition. More...
 
void aParallel (const GeneratorVector &rGenVec, Generator &rResGen)
 Parallel composition. More...
 
void aParallel (const Generator &rGen1, const Generator &rGen2, ProductCompositionMap &rCompositionMap, Generator &rResGen)
 Parallel composition. More...
 
void Parallel (const Generator &rGen1, const Generator &rGen2, ProductCompositionMap &rCompositionMap, Generator &rResGen)
 Parallel composition. More...
 
void Parallel (const Generator &rGen1, const Generator &rGen2, ProductCompositionMap &rCompositionMap, StateSet &rMark1, StateSet &rMark2, Generator &rResGen)
 Parallel composition. More...
 
void Parallel (const Generator &rGen1, const Generator &rGen2, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, Generator &rResGen)
 Parallel composition. More...
 
void Product (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Product composition. More...
 
void aProduct (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Product composition. More...
 
void aProduct (const Generator &rGen1, const Generator &rGen2, ProductCompositionMap &rCompositionMap, Generator &rResGen)
 Product composition. More...
 
void Product (const Generator &rGen1, const Generator &rGen2, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, StateSet &rMark1, StateSet &rMark2, Generator &rResGen)
 Product composition. More...
 
void Product (const Generator &rGen1, const Generator &rGen2, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, Generator &rResGen)
 Product composition. More...
 
void SetComposedStateNames (const Generator &rGen1, const Generator &rGen2, const std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, Generator &rGen12)
 Helper: uses composition map to track state names in a paralell composition. More...
 
void CompositionMap1 (const std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, std::map< Idx, Idx > &rCompositionMap1)
 
void CompositionMap2 (const std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, std::map< Idx, Idx > &rCompositionMap2)
 
void ProjectNonDet_opitz (Generator &rGen, const EventSet &rProjectAlphabet)
 
void ProjectNonDet_ref (Generator &rGen, const EventSet &rProjectAlphabet)
 
void ProjectNonDet_graph (Generator &rGen, const EventSet &rProjectAlphabet)
 
void ProjectNonDet_simple (Generator &rGen, const EventSet &rProjectAlphabet)
 
void ProjectNonDet_barthel (Generator &rGen, const EventSet &rProjectAlphabet)
 
void ProjectNonDet_fbr (Generator &rGen, const EventSet &rProjectAlphabet)
 
void ProjectNonDet_scc (Generator &rGen, const EventSet &rProjectAlphabet)
 
void ProjectNonDet (Generator &rGen, const EventSet &rProjectAlphabet)
 Language projection. More...
 
void ProjectNonDetScc (Generator &rGen, const EventSet &rProjectAlphabet)
 Language projection. More...
 
void Project (const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
 Deterministic projection. More...
 
void aProjectNonDet (Generator &rGen, const EventSet &rProjectAlphabet)
 Language projection. More...
 
void aProject (const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
 Deterministic projection. More...
 
void Project (const Generator &rGen, const EventSet &rProjectAlphabet, std::map< Idx, StateSet > &rEntryStatesMap, Generator &rResGen)
 Deterministic projection. More...
 
void InvProject (Generator &rGen, const EventSet &rProjectAlphabet)
 Inverse projection. More...
 
void aInvProject (Generator &rGen, const EventSet &rProjectAlphabet)
 Inverse projection. More...
 
void aInvProject (const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
 Inverse projection. More...
 
void CreateEntryStatesMap (const std::map< StateSet, Idx > &rRevEntryStatesMap, std::map< Idx, StateSet > &rEntryStatesMap)
 
void LoadRegistry (const std::string &rPath="")
 Load all registered types and functions. More...
 
void SaveRegistry (const std::string &rPath="")
 Dump all registered types and functions. More...
 
void ClearRegistry (void)
 Clear all registry. More...
 
TypeNewFaudesObject (const std::string &rTypeName)
 Instantiate faudes typed objects by type name. More...
 
FunctionNewFaudesFunction (const std::string &rFunctName)
 Instantiate faudes function objects by function name. More...
 
const std::string & FaudesTypeName (const Type &rObject)
 Query type name. More...
 
bool FaudesTypeTest (const std::string &rTypeName, const Type &rObject)
 Test type compatibility. More...
 
const std::string & FaudesFunctionName (const Function &rObject)
 
FAUDES_API const std::string & FaudesFunctionName (const Type &rObject)
 Query function name. More...
 
void LanguageUnionNonDet (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Language union, nondeterministic version. More...
 
void LanguageUnion (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Language union, deterministic version. More...
 
void LanguageUnion (const GeneratorVector &rGenVec, Generator &rResGen)
 Language union. More...
 
void LanguageIntersection (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Language intersection. More...
 
void LanguageIntersection (const GeneratorVector &rGenVec, Generator &rResGen)
 Language intersection. More...
 
bool EmptyLanguageIntersection (const Generator &rGen1, const Generator &rGen2)
 Test for empty language intersection (same as Disjoind()). More...
 
bool LanguageDisjoint (const Generator &rGen1, const Generator &rGen2)
 Test whether two languages are disjoint. More...
 
void Automaton (Generator &rGen, const EventSet &rAlphabet)
 Convert generator to automaton wrt specified alphabet. More...
 
void Automaton (Generator &rGen)
 Convert generator to automaton. More...
 
void LanguageComplement (Generator &rGen, const EventSet &rAlphabet)
 Language complement wrt specified alphabet. More...
 
void LanguageComplement (Generator &rGen)
 Language complement. More...
 
void LanguageComplement (const Generator &rGen, Generator &rRes)
 Language Complement (uniform API wrapper). More...
 
void LanguageComplement (const Generator &rGen, const EventSet &rSigma, Generator &rRes)
 Language Complement (uniform API wrapper). More...
 
void LanguageDifference (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Language difference (set-theoretic difference). More...
 
void LanguageConcatenateNonDet (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Language concatenation, nondeterministic version. More...
 
void LanguageConcatenate (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
 Language concatenation, deterministic version. More...
 
void FullLanguage (const EventSet &rAlphabet, Generator &rResGen)
 Full Language, L(G)=Lm(G)=Sigma*. More...
 
void AlphabetLanguage (const EventSet &rAlphabet, Generator &rResGen)
 Alphabet Language, L(G)=Lm(G)=Sigma. More...
 
void EmptyStringLanguage (const EventSet &rAlphabet, Generator &rResGen)
 Empty string language, L(G)=Lm(G)={epsilon}. More...
 
void EmptyLanguage (const EventSet &rAlphabet, Generator &rResGen)
 Empty language Lm(G)={}. More...
 
bool IsEmptyLanguage (const Generator &rGen)
 Test for Empty language Lm(G)=={}. More...
 
bool LanguageInclusion (const Generator &rGen1, const Generator &rGen2)
 Test language inclusion, Lm1<=Lm2. More...
 
bool LanguageEquality (const Generator &rGen1, const Generator &rGen2)
 Language equality, Lm1==Lm2. More...
 
void KleeneClosure (Generator &rGen)
 Kleene Closure. More...
 
void KleeneClosure (const Generator &rGen, Generator &rResGen)
 Kleene Closure. More...
 
void KleeneClosureNonDet (Generator &rGen)
 Kleene Closure, nondeterministic version. More...
 
void PrefixClosure (Generator &rGen)
 Prefix Closure. More...
 
bool IsPrefixClosed (const Generator &rGen)
 Test for prefix closed marked language. More...
 
bool IsNonblocking (const Generator &rGen)
 Test for nonblocking generator. More...
 
bool IsNonblocking (const Generator &rGen1, const Generator &rGen2)
 Test for nonblocking marked languages. More...
 
void SelfLoop (Generator &rGen, const EventSet &rAlphabet)
 Self-loop all states. More...
 
void SelfLoopMarkedStates (Generator &rGen, const EventSet &rAlphabet)
 Self-loop all marked states. More...
 
void SelfLoop (Generator &rGen, const EventSet &rAlphabet, const StateSet &rStates)
 Self-loop specified states. More...
 
void StateMin_org (const Generator &rGen, Generator &rResGen, std::vector< StateSet > &rSubsets, std::vector< Idx > &rNewIndices)
 
void StateMin (const Generator &rGen, Generator &rResGen)
 State set minimization. More...
 
void StateMin (const Generator &rGen, Generator &rResGen, std::vector< StateSet > &rSubsets, std::vector< Idx > &rNewIndices)
 State set minimization. More...
 
void aStateMin (const Generator &rGen, Generator &rResGen)
 State set minimization. More...
 
void aStateMin (Generator &rGen)
 State set minimization. More...
 
void TransSpec (const GeneratorVector &rSpecGenVec, const EventSet &rGUncAlph, GeneratorVector &rResGenVec)
 translate specification into plant More...
 
void ComputeWSOE (const Generator &rGenOrig, const EventSet &rConAlph, const EventSet &rLocAlph, std::map< Idx, Idx > &rMapStateToPartition, Generator &rResGen)
 weak synthesis obeservation equivalence [not implemented] More...
 
void GlobalSelfloop (GeneratorVector &rGenVec)
 remove the events from the entire buffer which have only selfloop transitions More...
 
void LocalSelfloop (Generator &rGen, EventSet &rLocAlph)
 remove the events from a generator which have only selfloop transitions More...
 
void MakeDistinguisher (Generator &AbstGen, std::map< Idx, Idx > &rMapStateToPartition, Generator &OrigGen, std::map< Idx, std::vector< Idx > > &rMapOldToNew)
 make a distinguisher and a map for solving nondeterminism and rewrite abstracted automaton More...
 
void Splitter (const std::map< Idx, std::vector< Idx > > &rMapOldToNew, EventSet &rConAlph, GeneratorVector &rGenVec, std::map< Idx, Idx > &rMapEventsToPlant, GeneratorVector &rDisGenVec, GeneratorVector &rSupGenVec)
 update the generators in synthesis-buffer and in supervisor with new events More...
 
void SelectSubsystem_V1 (GeneratorVector &rGenVec, Generator &rResGen)
 heuristic: vorious approaches to select subsystem from synthesis-buffer then compose them and remove them from buffer. More...
 
void SelectSubsystem_V2 (GeneratorVector &rGenVec, Generator &rResGen)
 
void ComputeHSupConNB (const Generator &rOrigGen, const EventSet &rConAlph, const EventSet &rLocAlph, Generator &rHSupGen)
 halbway-synthesis More...
 
void SingleTransSpec (const Generator &rSpecGen, const EventSet &rUncAlph, Generator &rResGen)
 
void SplittGen (Generator &rGen, Idx parent, const std::vector< Idx > &kids)
 subfunction for Splitter: splitt the events in a generator More...
 
bool BiggerMax (std::vector< GeneratorVector::Position > &rCandidate, GeneratorVector &rGenVec)
 
void H_tocollect (StateSet &rBlockingstates, const TransSetX2EvX1 &rRtrel, const EventSet &rLouc, const EventSet &rShuc, TransSetX2EvX1 &rToredirect)
 
void ControlProblemConsistencyCheck (const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec)
 Compositional synthesis. More...
 
void CompositionalSynthesisUnchecked (const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec, std::map< Idx, Idx > &rMapEventsToPlant, GeneratorVector &rDisGenVec, GeneratorVector &rSupGenVec)
 Compositional synthesis. More...
 
void CompositionalSynthesis (const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec, std::map< Idx, Idx > &rMapEventsToPlant, GeneratorVector &rDisGenVec, GeneratorVector &rSupGenVec)
 Compositional synthesis. More...
 
bool IsRelativelyMarked (const Generator &rGenPlant, const Generator &rGenCand)
 Test for relative marking. More...
 
bool IsRelativelyPrefixClosed (const Generator &rGenPlant, const Generator &rGenCand)
 Test for relative prefix-closedness. More...
 
void SupRelativelyPrefixClosed (const Generator &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 Supremal Relatively Closed Sublanguage. More...
 
void SupRelativelyPrefixClosedUnchecked (const Generator &rPlantGen, const Generator &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, Generator &rResGen)
 Supremal Relatively Closed Sublanguage (internal function) More...
 
bool IsRelativelyOmegaMarked (const Generator &rGenPlant, const Generator &rGenCand)
 Test for relative marking, omega langauges. More...
 
bool IsRelativelyOmegaClosed (const Generator &rGenPlant, const Generator &rGenCand)
 Test for relative closedness, omega languages. More...
 
bool IsRelativelyOmegaClosedUnchecked (const Generator &rGenPlant, const Generator &rGenCand)
 Test for relative closedness, omega languages. More...
 
bool IsStdSynthesisConsistentUnchecked (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rPlant0Gen)
 
bool IsStdSynthesisConsistent (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rPlant0Gen)
 Test consistency of an abstractions w.r.t. More...
 
bool IsStdSynthesisConsistent (const System &rPlantGen, const Generator &rPlant0Gen)
 Test consistency of an abstraction w.r.t standard synthesis. More...
 
void SupConClosedUnchecked (const Generator &rPlantGen, const EventSet &rCAlph, Generator &rSupCandGen)
 Supremal Controllable Sublangauge (internal function) More...
 
bool IsControllableUnchecked (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, StateSet &rCriticalStates)
 Controllability (internal function) More...
 
void SupConProduct (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, Generator &rResGen)
 Parallel composition optimized for the purpose of SupCon (internal function) More...
 
void SupConNBUnchecked (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, Generator &rResGen)
 Nonblocking Supremal Controllable Sublanguage (internal function) More...
 
void ControlProblemConsistencyCheck (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen)
 Consistency check for controlproblem input data. More...
 
void ControlProblemConsistencyCheck (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpecGen)
 Consistency check for controlproblem input data. More...
 
bool IsControllable (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSupCandGen)
 Test controllability. More...
 
bool IsControllable (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSupCandGen, StateSet &rCriticalStates)
 Test controllability. More...
 
void SupConNB (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
 Nonblocking Supremal Controllable Sublanguage. More...
 
void SupConClosed (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
 Supremal Controllable and Closed Sublanguage. More...
 
void SupConClosed (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, Generator &rResGen)
 Supremal Controllable and Closed Sublanguage. More...
 
void TraverseUncontrollableBackwards (const EventSet &rCAlph, TransSetX2EvX1 &rtransrel, StateSet &rCriticalStates, Idx current)
 Helper function for IsControllable. More...
 
bool IsControllable (const System &rPlantGen, const Generator &rSupCandGen)
 Test controllability. More...
 
void SupConNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 Nonblocking Supremal Controllable Sublanguage. More...
 
void SupConClosed (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 Supremal Controllable and Closed Sublanguage. More...
 
void NormalityConsistencyCheck (const Generator &rL, const EventSet &rOAlph, const Generator &rK)
 NormalityConsistencyCheck: Consistency check for normality input data. More...
 
bool IsNormal (const Generator &rL, const EventSet &rOAlph, const Generator &rK)
 IsNormal: checks normality of a language K generated by rK wrt a language L generated by rL and the subset of observable events rOAlph. More...
 
bool IsNormal (const System &rPlantGen, const Generator &rSupCandGen)
 IsNormal wrapper. More...
 
void ConcatenateFullLanguage (Generator &rGen)
 ConcatenateFullLanguage: concatenate Sigma* to language marked by rGen. More...
 
bool SupNorm (const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
 SupNorm: compute supremal normal sublanguage. More...
 
bool SupNormClosed (const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
 SupNormClosed - compute supremal normal and closed sublanguage. More...
 
void SupConNormClosed (const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
 SupConNormClosed: compute supremal controllable, normal and closed sublanguage. More...
 
void SupConNormNB (const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
 SupConNormNB: compute supremal controllable and normal sublanguage. More...
 
bool SupPrefixClosed (const Generator &rK, Generator &rResult)
 SupPrefixClosed: supremal closed sublanguage of K by cancelling all tranistions leading to a non-marked state. More...
 
void SupConNormClosedUnchecked (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, Generator &rObserverGen, Generator &rSupCandGen)
 Supremal Normal Controllable Sublangauge (internal function) More...
 
void SupNorm (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 rti wrapper More...
 
void SupNormClosed (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 rti wrapper More...
 
void SupConNormClosed (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 rti wrapper More...
 
void SupConNormNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 rti wrapper More...
 
bool TestMergibility (Idx stateI, Idx stateJ, std::vector< std::set< Idx > > &rWaitList, Idx cNode, const System &rSupGen, const std::map< Idx, ReductionStateInfo > &rSupStateInfo, const std::map< Idx, Idx > &rState2Class, const std::vector< StateSet > &rClass2States)
 
bool SupReduce (const System &rPlantGen, const System &rSupGen, System &rReducedSup)
 Supervisor Reduction algorithm. More...
 
void ComputeSynthObsEquiv (const Generator &rGenOrig, const EventSet &rConAlph, const EventSet &rLocAlph, std::map< Idx, Idx > &rMapStateToPartition, Generator &rResGen)
 Synthesis-observation equivalence. More...
 
void SupTconUnchecked (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rFAlph, const EventSet &rPAlph, const EventSet &rCPAlph, Generator &rSupCandGen)
 
void SupTconNBUnchecked (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rFAlph, const EventSet &rPAlph, const Generator &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, Generator &rResGen)
 
void SupTconNB (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rFAlph, const EventSet &rPAlph, const Generator &rSpecGen, Generator &rResGen)
 Nonblocking Supremal TDES-Controllable Sublanguage. More...
 
void SupTconNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 Nonblocking Supremal TDES-Controllable Sublanguage. More...
 
bool IsOmegaControllable (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSupCandGen)
 Test omega controllability. More...
 
bool IsOmegaControllable (const System &rPlantGen, const Generator &rSupCandGen)
 Test omega-controllability. More...
 
void SupConCmplClosed (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
 Supremal controllable and complete sublanguage. More...
 
void SupConCmplClosed (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 Supremal controllable and complete sublanguage. More...
 
void SupConCmplNB (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
 Supremal controllable and complete sublanguage. More...
 
void SupConCmplNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 Supremal controllable and complete sublanguage. More...
 
void SupConNormCmplNB (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpecGen, Generator &rResGen)
 Supremal controllable, normal and complete sublanguage. More...
 
void SupConNormCmplNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 rti wrapper More...
 
bool OmegaControlledLiveness (Generator &rSupCandGen, const EventSet &rCAlph, const StateSet &rPlantMarking)
 
bool OmegaControlledLiveness (Generator &rSupCandGen, const EventSet &rCAlph, const StateSet &rPlantMarking, std::map< Idx, EventSet > &rFeedbackMap)
 
bool OmegaControlledLiveness (Generator &rSupCandGen, const EventSet &rCAlph, const StateSet &rPlantMarking, std::map< Idx, Idx > &rControllerStatesMap, std::map< Idx, EventSet > &rFeedbackMap)
 
void OmegaSupConProduct (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, std::map< OPSState, Idx > &rProductCompositionMap, Generator &rResGen)
 
void OmegaSupConNBUnchecked (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, StateSet &rPlantMarking, Generator &rResGen)
 
void OmegaSupConNormNBUnchecked (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpecGen, StateSet &rPlantMarking, std::map< Idx, Idx > &rObserverStateMap, std::map< Idx, EventSet > &rFeedbackMap, Generator &rResGen)
 
void OmegaSupConNB (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
 Omega-synthesis. More...
 
void OmegaSupConNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 Omega-synthesis. More...
 
void OmegaConNB (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
 Omega-synthesis. More...
 
void OmegaConNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 Omega-synthesis. More...
 
void OmegaSupConNormNB (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpecGen, Generator &rResGen)
 Omega-synthesis for partial observation (experimental!) More...
 
void OmegaSupConNormNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 Omega-synthesis for partial observation. More...
 
void OmegaConNormNB (const Generator &rPlantGen, const EventSet &rOAlph, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
 Omega-synthesis for partial observation (experimental!) More...
 
void OmegaConNormNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
 Omega-synthesis for partial observation (experimental!) More...
 
bool IsMutuallyControllable (const System &rGen1, const System &rGen2)
 Verification of mutual controllability. More...
 
bool IsMutuallyControllable (const System &rGen1, const System &rGen2, StateSet &rForbidden1, StateSet &rForbidden2)
 Verification of mutual controllability. More...
 
void IsMutuallyControllable (const System &rGen1, const System &rGen2, bool &rRes)
 RTI wrapper. More...
 
void calculateDynamicSystemClosedObs (const Generator &rGen, EventSet &rHighAlph, Generator &rGenDyn)
 Computation of the dynamic system for Delta_sigma (reachable states after the occurrence of one high-level event). More...
 
void calculateDynamicSystemObs (const Generator &rGen, EventSet &rHighAlph, Generator &rGenDyn)
 Computation of the dynamic system for Delta_obs (local reachability of a marked state). More...
 
void calculateDynamicSystemMSA (const Generator &rGen, EventSet &rHighAlph, Generator &rGenDyn)
 Computation of the dynamic system for Delta_msa (local fulfillment of the msa-observer property). More...
 
bool recursiveCheckMSAForward (const Generator &rGen, const EventSet &rHighAlph, Idx currentState, StateSet &rDoneStates)
 Check if the msa-observer conditions is fulfilled for a given state. More...
 
bool recursiveCheckMSABackward (const Generator &rGen, const TransSetX2EvX1 &rRevTransSet, const EventSet &rHighAlph, Idx currentState, StateSet &rDoneStates)
 Check if the msa-observer conditions is fulfilled for a given state. More...
 
void calculateDynamicSystemLCC (const Generator &rGen, const EventSet &rControllableEvents, const EventSet &rHighAlph, Generator &rGenDyn)
 Computation of the dynamic system for Delta_lcc (fulfillment of the local control consistency property). More...
 
void recursiveCheckLCC (const TransSetX2EvX1 &rRevTransSet, const EventSet &rControllableEvents, const EventSet &rHighAlph, Idx currentState, StateSet &rDoneStates)
 Find states that fulfill the lcc condition. More...
 
Idx calcClosedObserver (const Generator &rGenObs, EventSet &rHighAlph)
 L(G)-observer computation by adding events to the high-level alphabet. More...
 
Int calcNaturalObserver (const Generator &rGenObs, EventSet &rHighAlph)
 Lm(G)-observer computation by adding events to the high-level alphabet. More...
 
Int calcNaturalObserverLCC (const Generator &rGen, const EventSet &rControllableEvents, EventSet &rHighAlph)
 Lm(G)-observer computation including local control consistency (LCC) by adding events to the high-level alphabet. More...
 
Int calcMSAObserver (const Generator &rGen, EventSet &rHighAlph)
 MSA-observer computation by adding events to the high-level alphabet. More...
 
Int calcMSAObserverLCC (const Generator &rGen, const EventSet &rControllableEvents, EventSet &rHighAlph)
 MSA-observer computation including local control consistency (LCC) by adding events to the high-level alphabet. More...
 
void ExtendHighAlphabet (const Generator &rGen, EventSet &rHighAlph, map< Idx, Idx > &rMapStateToPartition)
 Extension of the high-level alphabet to achieve the Lm-observer property. More...
 
bool CheckSplit (const Generator &rGen, const EventSet &rSplitAlphabet, const vector< pair< StateSet, Idx > > &rNondeterministicStates, Idx entryState)
 
void calcAbstAlphClosed (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
 L(G)-observer computation. More...
 
void calcAbstAlphClosed (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
 L(G)-observer computation. More...
 
void calcAbstAlphClosed (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Transition, Idx > &rMapChangedTrans)
 L(G)-observer computation. More...
 
void calcAbstAlphObs (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
 Lm-observer computation. More...
 
void calcAbstAlphObs (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
 Lm-observer computation. More...
 
void calcAbstAlphObs (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Transition, Idx > &rMapChangedTrans)
 Lm-observer computation. More...
 
void calcAbstAlphMSA (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
 MSA-observer computation. More...
 
void calcAbstAlphMSA (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
 MSA-observer computation. More...
 
void calcAbstAlphMSA (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Transition, Idx > &rMapChangedTrans)
 MSA-observer computation. More...
 
void backwardReachabilityObsOCC (const TransSetX2EvX1 &rTransSetX2EvX1, const EventSet &rControllableEvents, const EventSet &rHighAlph, Idx exitState, Idx currentState, bool controllablePath, map< Idx, map< Idx, bool > > &rExitLocalStatesMap, StateSet &rDoneStates)
 
void calcAbstAlphObsLCC (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
 Lm-observer computation including local control consistency (LCC). More...
 
void calcAbstAlphObsLCC (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Transition, Idx > &rMapChangedTrans)
 Lm-observer computation including local control consistency (LCC). More...
 
void calcAbstAlphMSALCC (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
 MSA-observer computation including local control consistency (LCC). More...
 
void calcAbstAlphMSALCC (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Transition, Idx > &rMapChangedTrans)
 MSA-observer computation including local control consistency (LCC). More...
 
bool relabel (Generator &rGenRelabel, EventSet &rControllableEvents, EventSet &rHighAlph, map< Idx, Idx > &rMapStateToPartition, map< Transition, Transition > &rMapChangedTransReverse, map< Transition, Idx > &rMapChangedTrans, map< Idx, EventSet > &rMapRelabeledEvents)
 Relabeling algorithm for the computation of an Lm-observer. More...
 
void insertRelabeledEvents (System &rGenPlant, const map< Idx, set< Idx > > &rMapRelabeledEvents, Alphabet &rNewEvents)
 Convenience function for relabeling events in a given generator. More...
 
void insertRelabeledEvents (Generator &rGenPlant, const map< Idx, set< Idx > > &rMapRelabeledEvents, EventSet &rNewEvents)
 Convenience function for relabeling events in a given generator. More...
 
void insertRelabeledEvents (System &rGenPlant, const map< Idx, set< Idx > > &rMapRelabeledEvents)
 Convenience function for relabeling events in a given generator. More...
 
void insertRelabeledEvents (Generator &rGenPlant, const map< Idx, set< Idx > > &rMapRelabeledEvents)
 Convenience function for relabeling events in a given generator. More...
 
void calcAbstAlphObs (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, EventRelabelMap &rMapRelabeledEvents)
 Rti convenience wrapper. More...
 
void insertRelabeledEvents (Generator &rGenPlant, const EventRelabelMap &rMapRelabeledEvents, EventSet &rNewEvents)
 Rti convenience wrapper. More...
 
void insertRelabeledEvents (Generator &rGenPlant, const EventRelabelMap &rMapRelabeledEvents)
 Rti convenience wrapper. More...
 
FAUDES_API void ExtendHighAlphabet (const Generator &rGenObs, EventSet &rHighAlph, std::map< Idx, Idx > &rMapStateToPartition)
 Extension of the high-level alphabet to achieve the Lm-observer property. More...
 
FAUDES_API bool CheckSplit (const Generator &rGenObs, const EventSet &rSplitAlphabet, const std::vector< std::pair< StateSet, Idx > > &rNondeterministicStates, Idx entryState)
 Check if the current alphabet splits all local automata with nondeterminims or unobservable transitions. More...
 
FAUDES_API void calcAbstAlphClosed (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 L(G)-observer computation. More...
 
FAUDES_API void calcAbstAlphClosed (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 L(G)-observer computation. More...
 
FAUDES_API void calcAbstAlphClosed (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Transition, Idx > &rMapChangedTrans)
 L(G)-observer computation. More...
 
FAUDES_API void calcAbstAlphObs (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 Lm-observer computation. More...
 
FAUDES_API void calcAbstAlphObs (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 Lm-observer computation. More...
 
FAUDES_API void calcAbstAlphObs (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Transition, Idx > &rMapChangedTrans)
 Lm-observer computation. More...
 
FAUDES_API void calcAbstAlphMSA (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 MSA-observer computation. More...
 
void calcAbstAlphMSA (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 MSA-observer computation. More...
 
FAUDES_API void calcAbstAlphMSA (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Transition, Idx > &rMapChangedTrans)
 MSA-observer computation. More...
 
FAUDES_API void calcAbstAlphObsLCC (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 Lm-observer computation including local control consistency (LCC). More...
 
FAUDES_API void calcAbstAlphObsLCC (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Transition, Idx > &rMapChangedTrans)
 Lm-observer computation including local control consistency (LCC). More...
 
FAUDES_API void calcAbstAlphMSALCC (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 MSA-observer computation including local control consistency (LCC). More...
 
FAUDES_API void calcAbstAlphMSALCC (Generator &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Transition, Idx > &rMapChangedTrans)
 MSA-observer computation including local control consistency (LCC). More...
 
bool relabel (Generator &rGenRelabel, EventSet &rControllableEvents, EventSet &rHighAlph, std::map< Idx, Idx > &rMapStateToPartition, std::map< Transition, Transition > &rMapChangedTransReverse, std::map< Transition, Idx > &rMapChangedTrans, std::map< Idx, EventSet > &rMapRelabeledEvents)
 Relabeling algorithm for the computation of an Lm-observer. More...
 
FAUDES_API void insertRelabeledEvents (System &rGenPlant, const std::map< Idx, std::set< Idx > > &rMapRelabeledEvents, Alphabet &rNewEvents)
 Convenience function for relabeling events in a given generator. More...
 
FAUDES_API void insertRelabeledEvents (Generator &rGenPlant, const std::map< Idx, std::set< Idx > > &rMapRelabeledEvents, EventSet &rNewEvents)
 Convenience function for relabeling events in a given generator. More...
 
FAUDES_API void insertRelabeledEvents (System &rGenPlant, const std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 Convenience function for relabeling events in a given generator. More...
 
void insertRelabeledEvents (Generator &rGenPlant, const std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 Convenience function for relabeling events in a given generator. More...
 
bool IsObs (const Generator &rLowGen, const EventSet &rHighAlph)
 Verification of the natural observer property. More...
 
bool IsMSA (const Generator &rLowGen, const EventSet &rHighAlph)
 Verification of the MSA observer property. More...
 
bool IsOCC (const System &rLowGen, const EventSet &rHighAlph)
 Verification of output control consistency (OCC). More...
 
bool IsOCC (const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph)
 Verification of output control consistency (OCC). More...
 
bool backwardVerificationOCC (const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph, Idx currentState)
 Function that supports the verification of output control consistency (OCC). More...
 
bool IsLCC (const System &rLowGen, const EventSet &rHighAlph)
 Verification of local control consistency (LCC). More...
 
bool IsLCC (const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph)
 Verification of local control consistency (LCC). More...
 
FAUDES_API void backwardVerificationLCC (const TransSetX2EvX1 &rTransSetX2EvX1, const EventSet &rControllableEvents, const EventSet &rHighAlph, Idx exitState, Idx currentState, bool controllablePath, std::map< Idx, bool > &rLocalStatesMap, StateSet &rDoneStates)
 Function that supports the verification of local control consistency (LCC). More...
 
bool LocalObservationConsistency (const System &rPlantGen, const System &rSpecGen, const EventSet &rHighAlph, const EventSet &rObsAlph)
 Supervisor Reduction algorithm. More...
 
bool IsCoDiagnosable (const System &rGen, const Generator &rSpec, const vector< const EventSet * > &rAlphabets, std::string &rReportString)
 
bool DecentralizedDiagnoser (const System &rGen, const Generator &rSpec, const std::vector< const EventSet * > &rAlphabets, std::vector< Diagnoser * > &rDiags, std::string &rReportString)
 Computes decentralized diagnosers for multiple local sites. More...
 
bool IsCoDiagnosable (const System &rGen, const Generator &rSpec, const EventSetVector &rAlphabets)
 Function definition for run-time interface. More...
 
bool DecentralizedDiagnoser (const System &rGen, const Generator &rSpec, const EventSetVector &rAlphabets, GeneratorVector &rDiags)
 Function definition for run-time interface. More...
 
void DecentralizedModularDiagnoser (const SystemVector &rGens, const Generator &rSpec, GeneratorVector &rDiags)
 Function definition for run-time interface. More...
 
void cParallel (const std::vector< const System * > &rGens, System &rResGen)
 Parallel composition of multiple generators. More...
 
bool IsEventDiagnosable (const System &rGen, const AttributeFailureTypeMap &rFailureTypeMap, string &rReportString)
 
bool IsEventDiagnosable (const System &rGen, const AttributeFailureTypeMap &rFailureTypeMap)
 Function definition for run-time interface. More...
 
bool IsIndicatorEventDiagnosable (const System &rGen, const AttributeFailureTypeMap &rFailureTypeMap, string &rReportString)
 
bool IsIndicatorEventDiagnosable (const System &rGen, const AttributeFailureTypeMap &rFailureTypeMap)
 Function definition for run-time interface. More...
 
bool MeetsDiagnosabilityAssumptions (const System &rGen, const AttributeFailureTypeMap &rFailureTypeMap, string &rReportString)
 
void ConvertParallelCompositionMap (const map< pair< Idx, Idx >, Idx > &rReverseCompositionMap, map< Idx, pair< Idx, Idx > > &rCompositionMap)
 
bool IsLive (const System &rGen, string &rReport)
 
bool CycleOfUnobsEvents (const System &rGen, string &rReport)
 
bool FailuresUnobservable (const System &rGen, const AttributeFailureTypeMap &rFailureTypeMap, string &rReport)
 
bool ExistsCycle (const System &rGen, string &rReport)
 
bool ExistsCycleSearch (const System &rGen, StateSet &rTodo, Idx currState, StateSet statesOnPath, string &rReport)
 
void CycleStartStates (const System &rGen, StateSet &rCycleOrigins)
 Find all start/end states of cycles of unobservable events in a generator. More...
 
void CycleStartStatesSearch (const System &rGen, StateSet &rTodo, Idx currState, StateSet statesOnPath, StateSet &rCycleOriginStates)
 Auxiliary function for CycleStartStates(). More...
 
bool ExistsViolatingCyclesInGd (System &rGd, const Diagnoser &rGobs, map< pair< Idx, Idx >, Idx > &rReverseCompositionMap, const string &rFailureType, string &rReportString)
 
void ComputeGobs (const System &rOrigGen, const string &rFailureType, const EventSet &rFailureEvents, Diagnoser &rGobs)
 
void ComputeGobs (const System &rOrigGen, const AttributeFailureTypeMap &rAttrFTMap, Diagnoser &rGobs)
 Compute G_o for a given generator with a given failure partition (according to Jiang). More...
 
void ComputeGd (const Diagnoser &rGobs, map< pair< Idx, Idx >, Idx > &rReverseCompositionMap, System &rGd)
 
void TrimNonIndicatorTracesOfGd (System &rGd, const Diagnoser &rGobs, const Idx rFailureType, const EventSet &rIndicatorEvents, const map< pair< Idx, Idx >, Idx > &rReverseCompositionMap)
 
void TrimNonIndicatorTracesOfGdRecursive (System &rGd, const Diagnoser &rGobs, const Idx rFailureType, const EventSet &rIndicatorEvents, map< Idx, pair< Idx, Idx > > &rCompositionMap, Idx state, StateSet &rStatesDone)
 
void ComputeReachability (const System &rGen, const EventSet &rUnobsEvents, const EventSet &rFailures, Idx State, const AttributeFailureTypeMap &rAttrFTMap, map< Idx, multimap< Idx, DiagLabelSet > > &rReachabilityMap)
 
void ComputeReachabilityRecursive (const System &rGen, const EventSet &rUnobsEvents, const EventSet &rFailures, Idx State, const AttributeFailureTypeMap &rAttrFTMap, map< Idx, multimap< Idx, DiagLabelSet > > &rReachabilityMap, const DiagLabelSet FToccurred)
 
TransSet ActiveBackwardTransSet (const System &rGen, Idx state)
 Obtain all transitions from other states into a given state of a generator. More...
 
void EventDiagnoser (const System &rOrigGen, const map< string, EventSet > &rFailureTypeMap, Diagnoser &rDiagGen)
 
void LabelPropagation (const DiagLabelSet &lastLabel, const DiagLabelSet &failureTypes, DiagLabelSet &newLabel)
 Generate a new label. More...
 
void LabelCorrection (const multimap< Idx, DiagLabelSet > &mm, AttributeDiagnoserState &attr)
 
FAUDES_API void ConvertParallelCompositionMap (const std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, std::map< Idx, std::pair< Idx, Idx > > &rCompositionMap)
 Convert the reverse composition map of Parallel() by switching first and second entry. More...
 
FAUDES_API bool IsLive (const System &rGen, std::string &rReport)
 Test if a generator is live. More...
 
FAUDES_API bool CycleOfUnobsEvents (const System &rGen, std::string &rReport)
 Test if there exist any cycles of unobservable events in a generator. More...
 
FAUDES_API bool FailuresUnobservable (const System &rGen, const AttributeFailureTypeMap &rFailureTypeMap, std::string &rReport)
 Check if all failure events are unobservable events in a generator's alphabet. More...
 
FAUDES_API bool ExistsCycle (const System &rGen, std::string &rReport)
 Test if there exist any cycles in a generator. More...
 
FAUDES_API bool ExistsCycleSearch (const System &rGen, StateSet &rTodo, Idx currState, StateSet statesOnPath, std::string &rReport)
 Auxiliary function for ExistsCycle(const System&, std::string&). More...
 
FAUDES_API bool ExistsViolatingCyclesInGd (System &rGd, const Diagnoser &rGobs, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, const std::string &rFailureType, std::string &rReportString)
 Remove states with same failure labels from rGd and from rReverseCompositionMap and perform cycle detection. More...
 
FAUDES_API void ComputeGobs (const System &rOrigGen, const std::string &rFailureType, const EventSet &rFailureEvents, Diagnoser &rGobs)
 Compute G_o for a single failure type of a generator. More...
 
FAUDES_API void ComputeGd (const Diagnoser &rGobs, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, System &rGd)
 Compute the diagnosability testing generator G_d as a parallel composition of G_o with itself (according to Jiang). More...
 
FAUDES_API void TrimNonIndicatorTracesOfGd (System &rGd, const Diagnoser &rGobs, const Idx rFailureType, const EventSet &rIndicatorEvents, const std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap)
 Extract all traces of a generator G_d that start with an indicator event that follows a failure event of a certain failure type. More...
 
FAUDES_API void TrimNonIndicatorTracesOfGdRecursive (System &rGd, const Diagnoser &rGobs, const Idx rFailureType, const EventSet &rIndicatorEvents, std::map< Idx, std::pair< Idx, Idx > > &rCompositionMap, Idx state, StateSet &rStatesDone)
 Auxiliary function for TrimNonIndicatorTracesOfGd(). More...
 
FAUDES_API void ComputeReachability (const System &rGen, const EventSet &rUnobsEvents, const EventSet &rFailures, Idx State, const AttributeFailureTypeMap &rAttrFTMap, std::map< Idx, std::multimap< Idx, DiagLabelSet > > &rReachabilityMap)
 Compute the reachability from a given generator state through a trace that consists of arbitrarily many unobservable events followed by one observable event. More...
 
FAUDES_API void ComputeReachabilityRecursive (const System &rGen, const EventSet &rUnobsEvents, const EventSet &rFailures, Idx State, const AttributeFailureTypeMap &rAttrFTMap, std::map< Idx, std::multimap< Idx, DiagLabelSet > > &rReachabilityMap, const DiagLabelSet FToccurred)
 Auxiliary function for ComputeReachability(const System&, const EventSet&, const EventSet&, Idx, const AttributeFailureTypeMap&, std::map<Idx,std::multimap<Idx,DiagLabelSet>>&). More...
 
FAUDES_API void EventDiagnoser (const System &rOrigGen, const std::map< std::string, EventSet > &rFailureTypeMap, Diagnoser &rDiagGen)
 Compute a standard diagnoser from an input generator and a failure partition. More...
 
FAUDES_API void LabelCorrection (const std::multimap< Idx, DiagLabelSet > &mm, AttributeDiagnoserState &attr)
 Perform label correction on propagated failure type labels. More...
 
bool IsLanguageDiagnosable (const System &rGen, const System &rSpec)
 Function definition for run-time interface. More...
 
void ComputeGobs (const System &rGenMarkedNonSpecBehaviour, Diagnoser &rGobs)
 Compute G_o for a generator that marks the faulty behaviour of a plant. More...
 
void ComputeReachability (const System &rGen, const EventSet &rUnobsEvents, Idx State, map< Idx, multimap< Idx, DiagLabelSet > > &rReachabilityMap)
 
void ComputeReachabilityRecursive (const System &rGen, const EventSet &rUnobsEvents, Idx State, StateSet done, map< Idx, multimap< Idx, DiagLabelSet > > &rReachabilityMap)
 
bool IsLanguageDiagnosable (const System &rGen, const System rSpec, std::string &rReportString)
 Test function to verify language-diagnosability. More...
 
bool rec_ComputeLoopPreservingObserver (const System &rGen, const EventSet &rInitialHighAlph, EventSet &rHighAlph, const std::vector< Idx > &rDdffVector, Idx numberEvents, Idx currentNumberEvents, Idx currentLocation, EventSet chosenEvents)
 rec_ComputeLoopPreservingObserver(rGen, rInitialHighAlph, rHighAlph, rDdffVector, numberEvents, currentNumberEvents, currentLocation, hosenEvents) More...
 
FAUDES_API void ComputeReachability (const System &rGen, const EventSet &rUnobsEvents, Idx State, std::map< Idx, std::multimap< Idx, DiagLabelSet > > &rReachabilityMap)
 Compute the reachability from a state of a generator that marks its faulty behaviour. More...
 
void ComputeReachabilityRecursive (const System &rGen, const EventSet &rUnobsEvents, Idx State, StateSet done, std::map< Idx, std::multimap< Idx, DiagLabelSet > > &rReachabilityMap)
 Auxiliary function for ComputeReachability(const System&, const EventSet&, Idx State, std::map<Idx,std::multimap< Idx,DiagLabelSet> >&). More...
 
bool IsModularDiagnosable (const SystemVector &rGsubs, const GeneratorVector &rKsubs, string &rReportString)
 
bool IsModularDiagnosable (const vector< const System * > &rGSubs, const vector< const Generator * > &rKSubs, std::string &rReportString)
 
bool ModularDiagnoser (const SystemVector &rGsubs, const GeneratorVector &rKsubs, GeneratorVector &rDiagSubs, string &rReportString)
 
bool ModularDiagnoser (const std::vector< const System * > &rGsubs, const std::vector< const Generator * > &rKsubs, std::vector< Diagnoser * > &rDiagsubs, std::string &rReportString)
 Checks modular diagnosability for a system G (which consists of the subsystems rGsubs) with respect to the specification K (consisting of local specifications rKsubs) and the local abstraction alphabets rHighAlphSubs. More...
 
bool IsModularDiagnosable (const SystemVector &rGsubs, const GeneratorVector &rKsubs)
 Function definition for run-time interface. More...
 
bool ModularDiagnoser (const SystemVector &rGsubs, const GeneratorVector &rKsubs, GeneratorVector &rDiagsubs)
 Function definition for run-time interface. More...
 
void cParallel (const vector< System > &rGens, System &rResGen)
 
FAUDES_API bool IsModularDiagnosable (const std::vector< const System * > &rGsubs, const std::vector< const Generator * > &rKsubs, std::string &rReportString)
 Checks modular diagnosability for a system G (which consists of the subsystems rGsubs) with respect to the specification K (consisting of local specifications rKsubs) and the local abstraction alphabets rHighAlphSubs. More...
 
void cParallel (const std::vector< System > &rGens, System &rResGen)
 Parallel composition of multiple generators. More...
 
bool IsHioConstraintForm (HioConstraint &rHioConstraint, StateSet &rQY, StateSet &rQU, EventSet &rErrEvSet, TransSet &rErrTrSet, StateSet &rErrStSet, std::string &rReportStr)
 IsHioConstraintForm: check if rHioConstraint is in I/O-constraint form and assign state attributes. More...
 
bool IsHioConstraintForm (HioConstraint &rHioConstraint, std::string &rReportStr)
 IsHioConstraintForm: check if rHioConstraint is in I/O-constraint form and assign state attributes. More...
 
bool IsHioConstraintForm (HioConstraint &rHioConstraint)
 IsHioConstraintForm: check if rHioConstraint is in I/O-constraint form and assign state attributes. More...
 
void HioStatePartition (HioConstraint &rConstraint)
 Function definition for run-time interface. More...
 
bool IsHioControllerForm (HioController &rHioController, StateSet &rQUc, StateSet &rQYP, StateSet &rQUp, StateSet &rQYcUp, EventSet &rErrEvSet, TransSet &rErrTrSet, StateSet &rErrStSet, std::string &rReportStr)
 IsHioControllerForm: check if rHioController is in I/O-controller form and assign state attributes. More...
 
bool IsHioControllerForm (HioController &rHioController, std::string &rReportStr)
 IsHioControllerForm: check if rHioController is in I/O-controller form and assign state attributes. More...
 
bool IsHioControllerForm (HioController &rHioController)
 IsHioControllerForm: check if rHioController is in I/O-controller form and assign state attributes. More...
 
void HioStatePartition (HioController &rController)
 Function definition for run-time interface. More...
 
bool IsHioEnvironmentForm (HioEnvironment &rHioEnvironment, StateSet &rQYe, StateSet &rQUe, StateSet &rQUl, StateSet &rQYlUe, EventSet &rErrEvSet, TransSet &rErrTrSet, StateSet &rErrStSet, std::string &rReportStr)
 IsHioEnvironmentForm: check if rHioEnvironment is in I/O-environment form and assign state attributes. More...
 
bool IsHioEnvironmentForm (HioEnvironment &rHioEnvironment, std::string &rReportStr)
 IsHioEnvironmentForm: check if rHioEnvironment is in I/O-environment form and assign state attributes. More...
 
bool IsHioEnvironmentForm (HioEnvironment &rHioEnvironment)
 IsHioEnvironmentForm: check if rHioEnvironment is in I/O-environment form and assign state attributes. More...
 
void HioStatePartition (HioEnvironment &rEnvironment)
 Function definition for run-time interface. More...
 
bool SupNormSP (Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
 
bool CompleteSynth (const Generator &rPlant, const EventSet rCAlph, const Generator &rSpec, Generator &rClosedLoop)
 CompleteSynth: compute supremal complete and controllable (and closed) sublanguage. More...
 
bool NormalCompleteSynth (Generator &rPlant, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpec, Generator &rClosedLoop)
 NormalCompleteSynth: compute normal, complete and controllable (and closed) sublanguage. More...
 
bool NormalCompleteSynthNB (Generator &rPlant, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpec, Generator &rClosedLoop)
 NormalCompleteSynthNB: compute normal, complete, controllable and nonblocking sublanguage. More...
 
Generator HioSortCL (const EventSet &rYc, const EventSet &rUc, const EventSet &rYp, const EventSet &rUp, const EventSet &rYe, const EventSet &rUe)
 IoSortCL: returns IO-sorting structure required for closed loops. More...
 
void HioFreeInput (const Generator &rGen, const EventSet &rInput, const EventSet &rOutput, Generator &rResGen, const std::string &rErrState1, const std::string &rErrState2, Idx &rErrState1Idx, Idx &rErrState2Idx)
 HioFreeInput: extend generator by obviously missing input transitions. More...
 
void HioFreeInput (const Generator &rGen, const EventSet &rInput, const EventSet &rOutput, Generator &rResGen, const std::string &rErrState1, const std::string &rErrState2)
 HioFreeInput: extend generator by obviously missing input transitions. More...
 
void HioFreeInput (const Generator &rGen, const EventSet &rInput, const EventSet &rOutput, Generator &rResGen)
 HioFreeInput: extend generator by obviously missing input transitions. More...
 
void HioFreeInput (const HioPlant &rPlant, HioPlant &rResPlant)
 HioFreeInput: extend HioPlant by obviously missing input transitions. More...
 
void HioFreeInput (const HioController &rController, HioController &rResController)
 HioFreeInput: extend HioController by obviously missing input transitions. More...
 
void HioFreeInput (const HioEnvironment &rEnvironment, HioEnvironment &rResEnvironment)
 HioFreeInput: extend HioEnvironment by obviously missing input transitions. More...
 
void HioFreeInput (const HioConstraint &rConstraint, HioConstraint &rResConstraint)
 HioFreeInput: extend HioConstraint by obviously missing input transitions. More...
 
void HioFreeInput (HioPlant &rPlant)
 HioFreeInput: convenience interface to faudes::HioFreeInput(const HioPlant&, HioPlant) More...
 
void HioFreeInput (HioController &rController)
 HioFreeInput: convenience interface to faudes::HioFreeInput(const HioController&, HioController) More...
 
void HioFreeInput (HioEnvironment &rEnvironment)
 HioFreeInput: convenience interface to faudes::HioFreeInput(const HioEnvironment&, HioEnvironment) More...
 
void HioFreeInput (HioConstraint &rConstraint)
 HioFreeInput: convenience interface to faudes::HioFreeInput(const HioConstraint&, HioConstraint) More...
 
void MarkHioShuffle (const Generator &rGen1, const Generator &rGen2, const std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, Generator &rShuffle)
 MarkHioShuffle: marking rule for HioShuffle() in case of marked parameters rGen1 and rGen2 - UNDER CONSTRUCTION. More...
 
void MarkAlternationAB (const EventSet rAset, const EventSet rBset, Generator &rAltAB)
 MarkAlternationAB: returns Generator marking the alternation of Aset-transitions with Bset-transitions. More...
 
void HioShuffleUnchecked (const Generator &rPlantA, const Generator &rPlantB, const EventSet &rYp, const EventSet &rUp, const EventSet &rYe, const EventSet &rUe, Generator &rIOShuffAB)
 HioShuffleUnchecked: IO-shuffle of rPlantA and rPlantB according to definition, no parameter check. More...
 
void HioShuffle (const Generator &rPlantA, const Generator &rPlantB, const EventSet &rYp, const EventSet &rUp, const EventSet &rYe, const EventSet &rUe, Generator &rIOShuffAB)
 HioShuffle: IO-shuffle of rPlantA and rPlantB according to definition. More...
 
void HioShuffle (const HioPlant &rPlantA, const HioPlant &rPlantB, HioPlant &rIOShuffAB)
 HioShuffle: IO-shuffle of rPlantA and rPlantB according to definition. More...
 
void CheapAltAnB (const EventSet rAset, const EventSet rBset, const int Depth, Generator &rAltAnB)
 CheapAltAnB: returns Generator of the following specification: "After a maximum of n (=depth) pairs of A-transitions, a B-transition has to occur!". More...
 
void CheapAltAB (const EventSet rAset, const EventSet rBset, const int Depth, Generator &rAltAB)
 CheapAltAB: returns Generator of the following specification: "After a maximum of n (=depth) pairs of A-transitions, a B-transition has to occur and vice-versa!". More...
 
void HioShuffleTU (const Generator &rPlantA, const Generator &rPlantB, const EventSet &rYp, const EventSet &rUp, const EventSet &rYe, const EventSet &rUe, const int Depth, Generator &rIOShuffAB)
 HioShuffleTU: IO-shuffle of rPlantA and rPlantB according to definition with additional forced alternation of depth Depth (see CheapAltAB()) between A- and B-events. More...
 
void SearchYclessScc (const Idx state, int &rcount, const Generator &rGen, const EventSet &rYc, const bool UnMarkedOnly, StateSet &rNewStates, std::stack< Idx > &rSTACK, StateSet &rStackStates, std::map< const Idx, int > &rDFN, std::map< const Idx, int > &rLOWLINK, std::set< StateSet > &rSccSet, StateSet &rRoots)
 SearchYclessSCC: Search for strongly connected ycless components (YC-less SCC's). More...
 
bool YclessScc (const Generator &rGen, const EventSet &rYc, std::set< StateSet > &rSccSet, StateSet &rRoots)
 YclessSCC: Search for strongly connected ycless components (YC-less SCC's) - convenience api. More...
 
bool YclessUnmarkedScc (const Generator &rGen, const EventSet &rYc, std::set< StateSet > &rSccSet, StateSet &rRoots)
 YclessUnmarkedSCC: Search for strongly connected ycless components (YC-less SCC's) consisting of unmarked states only. More...
 
bool YclessScc (const Generator &rGen, const EventSet &rYc, std::set< StateSet > &rSccSet)
 
bool IsYcLive (const Generator &rGen, const EventSet &rYc)
 IsYcLive: This function checks if generator is Yc-live. More...
 
void WriteStateSets (const std::set< StateSet > &rStateSets)
 WriteStateSets: Write set of StateSet's to console (indeces). More...
 
void WriteStateSets (const Generator &rGen, const std::set< StateSet > &rStateSets)
 WriteStateSets: Write set of StateSet's to console (symbolic state names taken from rGen). More...
 
void SccEntries (const Generator &rGen, const std::set< StateSet > &rSccSet, StateSet &rEntryStates, TransSetX2EvX1 &rEntryTransSet)
 SCCEntries: figure entry states and entry transitions of strongly connected components rSccSet of rGen. More...
 
void CloneScc (Generator &rGen, const StateSet &rScc, std::set< StateSet > &rSccSet, const Idx EntryState, StateSet &rEntryStates, TransSetX2EvX1 &rEntryTransSet)
 cloneSCC: makes a copy (clone) of strongly connected component (rSCC) of the generator and moves all transitions leading to some entry state EntryState of this SCC to the copy of EntryState. More...
 
void CloneUnMarkedScc (Generator &rGen, const StateSet &rScc, const Idx EntryState, const StateSet &rEntryStates, TransSetX2EvX1 &rEntryTransSet)
 CloneUnMarkedSCC: makes a copy (clone) of strongly connected unmarked component (rSCC) of rGen. More...
 
void YcAcyclic (const Generator &rGen, const EventSet &rYc, Generator &rResGen)
 YcAcyclic: Computes the supremal(?) Yc-acyclic sublanguage of L(Gen). More...
 
void ConstrSynth_Beta (Generator &rPlant, const EventSet &rYp, const EventSet &rUp, const Generator &rLocConstr, Generator &rOpConstraint)
 ConstrSynth_Beta: compute operator constraint Sp for plant under environment constraint Sl such that plant is complete & Yp-live wrt both constraints - Beta Version. More...
 
void HioSynthUnchecked (const Generator &rPlant, const Generator &rSpec, const Generator &rConstr, const Generator &rLocConstr, const EventSet &rYc, const EventSet &rUc, const EventSet &rYp, const EventSet &rUp, const EventSet &rYel, const EventSet &rUel, Generator &rController)
 HioSynthUnchecked: I/O controller synthesis procedure, no parameter check. More...
 
void HioSynth (const Generator &rPlant, const Generator &rSpec, const Generator &rConstr, const Generator &rLocConstr, const EventSet &rYc, const EventSet &rUc, const EventSet &rYp, const EventSet &rUp, const EventSet &rYel, const EventSet &rUel, Generator &rController)
 HioSynthUnchecked: I/O controller synthesis procedure. More...
 
void HioSynthMonolithic (const HioPlant &rPlant, const HioPlant &rSpec, const HioConstraint &rSc, const HioConstraint &rSp, const HioConstraint &rSe, HioController &rController)
 HioSynthMonolithic: I/O controller synthesis procedure for monolithic plant. More...
 
void HioSynthHierarchical (const HioPlant &rHioShuffle, const HioEnvironment &rEnvironment, const HioPlant &rSpec, const Generator &rIntConstr, const HioConstraint &rSc, const HioConstraint &rSl, HioController &rController)
 HioSynthHierarchical: I/O controller synthesis procedure for I/O-shuffle of i plants and their interaction via an I/O environment. More...
 
void HioShuffle_Musunoi (const HioPlant &rPlantA, const HioPlant &rPlantB, int depth, Generator &rIOShuffAB)
 
void HioSynth_Musunoi (const Generator &rPlant, const HioPlant &rSpec, const Generator &rConstr, const Generator &rLocConstr, const EventSet &rYp, const EventSet &rUp, Generator &rController)
 
FAUDES_API bool YclessSCC (const Generator &rGen, const EventSet &rYc, std::set< StateSet > &rSccSet)
 YclessSCC: Search for strongly connected ycless components (YC-less SCC's) - convenience api. More...
 
void AdjustHioController (const HioController &rHioController, const HioModule *rHioModule1, const HioModule *rHioModule2, HioController &rResEnv)
 
void GroupHioModules (const std::vector< HioModule * > &rChildren, HioModule &rParentModule)
 GroupHioModules: This function groups two or more HioModules to a new HioModule. More...
 
void CreateSpec (int mType[5], HioPlant &rHioSpec, Generator &constrP, Generator &constrE)
 This function creates new specification given by the type ("xxxxx") Note: The core of this function is a template specification model (SpecCB12.gen). More...
 
void CreateConstraint (int mType[5], Generator &constrP, Generator &constrE)
 This function creates constraints which describe the condition of completeness and Yp-liveness of a Specification. More...
 
bool IsHioPlantForm (HioPlant &rHioPlant, StateSet &rQYpYe, StateSet &rQUp, StateSet &rQUe, EventSet &rErrEvSet, TransSet &rErrTrSet, StateSet &rErrStSet, std::string &rReportStr)
 IsHioPlantForm: check if rHioPlant is in I/O-plant form and assign state attributes. More...
 
bool IsHioPlantForm (HioPlant &rHioPlant, std::string &rReportStr)
 IsHioPlantForm: check if rHioPlant is in I/O-plant form and assign state attributes. More...
 
bool IsHioPlantForm (HioPlant &rHioPlant)
 IsHioPlantForm: check if rHioPlant is in I/O-plant form and assign state attributes. More...
 
void HioStatePartition (HioPlant &rPlant)
 Function definition for run-time interface. More...
 
bool IsIoSystem (const IoSystem &rIoSystem, StateSet &rQU, StateSet &rQY, StateSet &rQErr)
 Test whether the system satisfies basic I/O conditions. More...
 
bool IsIoSystem (IoSystem &rIoSystem)
 Test whether the system satisfies the IO conditions. More...
 
void IoStatePartition (IoSystem &rIoSystem)
 Construct io state partition. More...
 
bool IsInputLocallyFree (IoSystem &rIoSystem)
 Test whether the system has a locally free input. More...
 
bool IsInputLocallyFree (const IoSystem &rIoSystem, StateSet &rQErr)
 Test whether the system has a locally free input. More...
 
bool IsInputOmegaFree (IoSystem &rIoSystem)
 Test whether the system behaviour has exhibits a free input. More...
 
bool IsInputOmegaFree (const IoSystem &rIoSystem, StateSet &rQErr)
 Test whether the system behaviour exhibits a free input. More...
 
void IoFreeInput (IoSystem &rIoSystem)
 Enable all input events for each input state. More...
 
void IoFreeInput (Generator &rIoSystem, const EventSet &rUAlph)
 Enable all input events for each input state. More...
 
void RemoveIoDummyStates (IoSystem &rIoSystem)
 Remove dummy states. More...
 
void IoSynthesisNB (const IoSystem &rPlant, const Generator &rSpec, IoSystem &rSup)
 IO system synthesis. More...
 
void IoSynthesis (const IoSystem &rPlant, const Generator &rSpec, IoSystem &rSup)
 IO system synthesis. More...
 
bool IsStronglyCoaccessible (const MtcSystem &rGen)
 RTI wrapper function. More...
 
bool IsStronglyTrim (const MtcSystem &rGen)
 RTI wrapper function. More...
 
void StronglyCoaccessible (MtcSystem &rGen)
 RTI wrapper function. More...
 
void StronglyCoaccessible (const MtcSystem &rGen, MtcSystem &rRes)
 RTI wrapper function. More...
 
void StronglyTrim (MtcSystem &rGen)
 RTI wrapper function. More...
 
void StronglyTrim (const MtcSystem &rGen, MtcSystem &rRes)
 RTI wrapper function. More...
 
Idx calcNaturalObserver (const MtcSystem &rGen, EventSet &rHighAlph)
 Calculate a colored natural observer by extending a given high-level alphabet. More...
 
void calcAbstAlphObs (MtcSystem &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
 Lm-observer computation. More...
 
void calcAbstAlphObs (MtcSystem &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
 Lm-observer computation. More...
 
void calcAbstAlphObs (MtcSystem &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Transition, Idx > &rMapChangedTrans)
 Lm-observer computation. More...
 
void calculateDynamicSystemObs (const MtcSystem &rGen, EventSet &rHighAlph, Generator &rGenDyn)
 Computation of the dynamic system for an Lm-observer. More...
 
void calcAbstAlphObs (MtcSystem &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 Lm-observer computation. More...
 
FAUDES_API void calcAbstAlphObs (MtcSystem &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
 Lm-observer computation. More...
 
FAUDES_API void calcAbstAlphObs (MtcSystem &rGenObs, EventSet &rControllableEvents, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Transition, Idx > &rMapChangedTrans)
 Lm-observer computation. More...
 
bool IsMtcObs (const MtcSystem &rLowGen, const EventSet &rHighAlph)
 Verification of the observer property. More...
 
void mtcParallel (const MtcSystem &rGen1, const MtcSystem &rGen2, MtcSystem &rResGen)
 Parallel composition of two colored marking generators, controllability status is observed. More...
 
void mtcParallel (const MtcSystem &rGen1, const MtcSystem &rGen2, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, MtcSystem &rResGen)
 Parallel composition of two MtcSystems. More...
 
void ComposedColorSet (const MtcSystem &rGen1, const Idx stdidx1, ColorSet &colors1, const MtcSystem &rGen2, const Idx stdidx2, ColorSet &colors2, ColorSet &composedSet)
 Compose the color set for a state combined from two states in two distinct automata. More...
 
void mtcUniqueInit (MtcSystem &rGen)
 
void mtcDeterministic (const MtcSystem &rGen, MtcSystem &rResGen)
 Make generator deterministic. More...
 
void mtcDeterministic (const MtcSystem &rGen, std::map< Idx, StateSet > &rEntryStatesMap, MtcSystem &rResGen)
 Make generator deterministic. More...
 
void mtcDeterministic (const MtcSystem &rGen, std::vector< StateSet > &rPowerStates, std::vector< Idx > &rDetStates, MtcSystem &rResGen)
 Make generator deterministic. More...
 
void mtcProjectNonDet (MtcSystem &rGen, const EventSet &rProjectAlphabet)
 Project generator to alphabet rProjectAlphabet. More...
 
void mtcProjectNonDet (const MtcSystem &rGen, const EventSet &rProjectAlphabet, MtcSystem &rResGen)
 Project generator to alphabet rProjectAlphabet. More...
 
void mtcProject (const MtcSystem &rGen, const EventSet &rProjectAlphabet, MtcSystem &rResGen)
 Minimized Deterministic projection. More...
 
void mtcProject (const MtcSystem &rGen, const EventSet &rProjectAlphabet, std::map< Idx, StateSet > &rEntryStatesMap, MtcSystem &rResGen)
 Minimized Deterministic projection. More...
 
void mtcInvProject (MtcSystem &rGen, const EventSet &rProjectAlphabet)
 Inverse projection. More...
 
void mtcInvProject (const MtcSystem &rGen, const EventSet &rProjectAlphabet, MtcSystem &rResGen)
 RTI wrapper. More...
 
void SearchScc (const Idx state, int &rCount, const Generator &rGen, StateSet &rNewStates, std::stack< Idx > &rSTACK, StateSet &rStackStates, std::map< const Idx, int > &rDFN, std::map< const Idx, int > &rLOWLINK, std::set< StateSet > &rSccSet, StateSet &rRoots)
 Search for strongly connected components (SCC)*** This function partitions the stateset of a generator into equivalence classes such that states x1 and x2 are equivalent iff there is a path from x1 to x2 AND a path from x2 to x1. More...
 
bool ComputeSCC (const Generator &rGen, std::set< StateSet > &rSccSet, StateSet &rRoots)
 Computes the strongly connected components (SCCs) of an automaton. More...
 
void ColoredSCC (MtcSystem &rGen, ColorSet &rColors, std::set< StateSet > &rColoredSCCs)
 Compute all strongly connected components (SCCs) in a colored marking generator (CMG) that are marked with a given set of colors. More...
 
bool CheckRedundantColor (MtcSystem rGen, Idx redundantColor)
 Check if a color in a colored marking generator is redundant for the supervisor synthesis. More...
 
void OptimalColorSet (const MtcSystem &rGen, ColorSet &rOptimalColors, EventSet &rHighAlph)
 Compute an optimal subset of the colors that should be removed. More...
 
void rec_OptimalColorSet (const MtcSystem &rGen, const std::vector< Idx > &rColorVector, Idx colorNumber, ColorSet &rOptimalColors, Idx &rOptimalNumberStates, Idx &rOptimalNumberColors, const EventSet &rHighAlph, EventSet &rOptimalHighAlph)
 Recursively find an optimal set of colors to be removed. More...
 
void mtcStateMin (MtcSystem &rGen, MtcSystem &rResGen)
 State Minimization This function implements the (n*log n) set partitioning algorithm by John E. More...
 
void mtcStateMin (MtcSystem &rGen, MtcSystem &rResGen, std::vector< StateSet > &rSubsets, std::vector< Idx > &rNewIndices)
 State Minimization This function implements the (n*log n) set partitioning algorithm by John E. More...
 
void mtcStateMin (const MtcSystem &rGen, MtcSystem &rResGen)
 RTI wrapper. More...
 
void mtcSupConNB (const MtcSystem &rPlantGen, const MtcSystem &rSpecGen, MtcSystem &rResGen)
 Nonblocking Supremal Controllable Sublanguage (wrapper function) More...
 
void mtcSupConNB (const MtcSystem &rPlantGen, const MtcSystem &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, MtcSystem &rResGen)
 Nonblocking Supremal Controllable Sublanguage. More...
 
void mtcSupConClosed (const MtcSystem &rPlantGen, const MtcSystem &rSpecGen, MtcSystem &rResGen)
 Supremal Controllable Sublanguage (wrapper function) More...
 
void mtcSupConClosed (const MtcSystem &rPlantGen, const MtcSystem &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, MtcSystem &rResGen)
 Supremal Controllable Sublanguage. More...
 
void mtcSupConParallel (const MtcSystem &rPlantGen, const MtcSystem &rSpecGen, const EventSet &rUAlph, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, MtcSystem &rResGen)
 Fast parallel composition for computation for the mtcSupConNB. More...
 
void mtcSupConUnchecked (const MtcSystem &rPlantGen, const EventSet &rCAlph, MtcSystem &rSupGen)
 Supremal Controllable Sublangauge (Real SupCon function; unchecked) More...
 
bool ccTrim (const Generator &gen, Generator &trimGen)
 A more efficient Trim() operation. More...
 
bool IsConditionalClosed (const GeneratorVector &specVect, const Generator &pk, const GeneratorVector &genVect, const Generator &gk)
 Conditionalclosedness Checking Algorithm. More...
 
bool IsConditionalControllable (const GeneratorVector &specVect, const Generator &pk, const GeneratorVector &genVect, const Generator &gk, const EventSet &ACntrl)
 Conditionalcontrollability Checking Algorithm. More...
 
bool IsConditionalDecomposable (const Generator &gen, const EventSetVector &ee, const EventSet &ek, Generator &proof)
 Conditionaldecomposability Checking Algorithm. More...
 
bool IsCD (const Generator &gen, const EventSetVector &ee, const EventSet &ek, const EventSet &unionset, Generator &proof)
 
void ConDecExtension (const Generator &gen, const EventSetVector &rAlphabets, EventSet &ek)
 Conditionaldecomposability Extension Algorithm. More...
 
void CDExt (const Generator &gen, const EventSetVector &ee, const EventSet &unionset, EventSet &ek)
 
Generator ComputeTildeG (const EventSet &unionset, const EventSetVector &ee, const EventSet &ek, const Generator &gen)
 
bool isExtendedEk (const Generator &tildeGen, const Generator &rGen, EventSet &ek)
 
bool SupConditionalControllable (const Generator &gen, const GeneratorVector &genVector, const EventSet &ACntrl, const EventSet &InitEk, GeneratorVector &supVector, Generator &Coord)
 Conditionalcontrollability Checking Algorithm. More...
 
template<class GlobalAttr1 , class StateAttr1 , class EventAttr1 , class TransAttr1 , class GlobalAttr2 , class StateAttr2 , class EventAttr2 , class TransAttr2 , class GlobalAttrR , class StateAttrR , class EventAttrR , class TransAttrR >
void TParallel (const TGEN1 &rGen1, const TGEN2 &rGen2, TGENR &rResGen)
 Parallel composition of timed generators. More...
 
template<class GlobalAttr1 , class StateAttr1 , class EventAttr1 , class TransAttr1 , class GlobalAttr2 , class StateAttr2 , class EventAttr2 , class TransAttr2 , class GlobalAttrR , class StateAttrR , class EventAttrR , class TransAttrR >
void TParallel (const TGEN1 &rGen1, const TGEN2 &rGen2, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, TGENR &rResGen)
 Parallel composition of timed generators. More...
 
void ran_plant_seeds (long x)
 Use this function to set the state of all the random number generator streams by "planting" a sequence of states (seeds), one per stream, with all states dictated by the state of the default stream. More...
 
void ran_put_seed (long seed)
 Put a seed. More...
 
void ran_select_stream (int index)
 Use this function to set the current random number generator stream – that stream from which the next random number will come. More...
 
void ran_init (long seed)
 Initialize random generator. More...
 
double ran (void)
 Run random generator Random Number Generator (for more details see "Random Number Generators: Good Ones Are Hard To Find" Steve Park and Keith Miller Communications of the ACM, October 1988) More...
 
double ran_uniform (double a, double b)
 Sample a random variable uniformly on interval [a;b) Distribution: f(t) dt= {1/(b-a)} dt for t, a <=t< b, else 0. More...
 
long ran_uniform_int (long a, long b)
 Sample a discrete random variable uniformly on interval [a;b) Distribution: p(n) = 1/(b-a-1) More...
 
double ran_exponential (double mu)
 Sample a random variable exponentially Distribution: f(t) dt = 1/mu exp(-t/mu) dt for t>=0. More...
 
double ran_exponential (double mu, Time::Type tossLB, Time::Type tossUB)
 Sample a random variable exponentially on a restricted interval Distribution: f(t) dt = 1/mu exp(-t/mu) dt for t>=0. More...
 
double ran_gauss (double mu, double sigma, Time::Type tossLB, Time::Type tossUB)
 Sample a random variable gaussian distributed on a restricted interval Distribution: f(t) = 1 / sqrt(2 pi sigma^2) * exp( -1/2 ((t-mu)/sigma)^2) for t>=0. More...
 
double ran_gaussian_cdf_P (double x)
 Help function: calculate gaussian CDF using an approximation from Abromowitz and Stegun: Handbook of Mathematical Functions. More...
 
void * SDeviceSynchro (void *arg)
 
int syncSend (int dest, const char *data, int len, int flag)
 
void * NDeviceListen (void *arg)
 
int faudes_print (lua_State *L)
 
void faudes_print_register (lua_State *L)
 
void faudes_hook (lua_State *L, lua_Debug *ar)
 
void faudes_hook_register (lua_State *L)
 
void faudes_initialize (lua_State *pL)
 
int faudes_loadext (lua_State *pL, const char *filename)
 
int faudes_loaddefext (lua_State *pL, const char *arg0)
 
char ** faudes_complete (lua_State *pL, const char *text, int start, int end)
 
void * SwigCastPtr (void *ptr, swig_type_info *from, swig_type_info *ty)
 
swig_lua_userdataSwigUserData (lua_State *L, int index)
 
std::string MangleString (const std::string &str)
 
FAUDES_API void faudes_throw_exception (const std::string &msg)
 
FAUDES_API void faudes_dict_insert_topic (const std::string &topic, const std::string &text)
 
FAUDES_API void faudes_dict_insert_entry (const std::string &topic, const std::string &key, const std::string &entry)
 
FAUDES_API void faudes_mute (bool on)
 
FAUDES_API void faudes_console (const std::string &message)
 
FAUDES_API void faudes_debug (const std::string &message)
 
void TimeInvariantAbstraction (const Experiment &exp, Generator &res)
 
void TimeVariantAbstraction (const Experiment &exp, Generator &res)
 
Parma_Polyhedra_Library::C_Polyhedron & UserData (const Polyhedron &fpoly)
 convert a faudes style polyhedron "A x <= B" to a PPL polyhedron, and keep the conversion result in the UserData entry More...
 
void PolyFinalise (const Polyhedron &fpoly)
 convert PPL polyhedron back to faudes data structures; this is required if we manipulate a polyhedron and like to access it from libFAUDES More...
 
Parma_Polyhedra_Library::C_Polyhedron & UserData (const LinearRelation &frelation)
 convert a faudes style linear relation "A' x' + A x <= B" to a PPL polyhedron, and keep the conversion result in the UserData entry More...
 
void PolyDWrite (const Polyhedron &fpoly)
 poly dump More...
 
void PolyCopy (const Polyhedron &src, Polyhedron &dst)
 copy method More...
 
void PolyIntersection (const Polyhedron &poly, Polyhedron &res)
 intersection More...
 
bool PolyIsEmpty (const Polyhedron &poly)
 test emptyness More...
 
bool PolyInclusion (const Polyhedron &poly, const Polyhedron &other)
 inclusion More...
 
void PolyScratch (void)
 scratch More...
 
void PolyLinearRelation (const LinearRelation &reset, Polyhedron &poly)
 apply reset relation A'x' + Ax <= B More...
 
void PolyTimeElapse (const Polyhedron &rate, Polyhedron &poly)
 time elapse More...
 
void LhaReach (const LinearHybridAutomaton &lha, const HybridStateSet &states, std::map< Idx, HybridStateSet * > &ostates, int *pCnt=NULL)
 compute sets of reachable state per successor event More...
 
void AlternativeAccessible (Generator &rGen)
 Alternative accessibility algorithm. More...
 
Functions (modular diagnoser computation)
void DecentralizedModularDiagnoser (const std::vector< const System * > &rGens, const Generator &rSpec, std::vector< Diagnoser * > &rDiags, std::string &rReportString)
 Function that computes decentralized diagnosers for the respective subsystems of a composed (modular) system. More...
 
FAUDES_API bool ModularDiagnoser (const SystemVector &rGsubs, const GeneratorVector &rKsubs, GeneratorVector &rDiagSubs, std::string &rReportString)
 Function that computes diagnosers for the respective subsystems of a composed system. More...
 
Functions (decentralized diagnosability)
FAUDES_API bool IsCoDiagnosable (const System &rGen, const Generator &rSpec, const std::vector< const EventSet * > &rAlphabets, std::string &rReportString)
 Checks co-diagnosability for a system G with respect to the specification K and the local observation alphabets rAlphabets. More...
 
Functions (diagnoser computation)
void EventDiagnoser (const System &rOrigGen, const AttributeFailureTypeMap &rAttrFTMap, Diagnoser &rDiagGen)
 Compute a standard diagnoser from an input generator and a failure partition. More...
 
void LanguageDiagnoser (const System &rGen, const System &rSpec, Diagnoser &rDiagGen)
 Compute a standard diagnoser from an input generator and a specification. More...
 
Functions (diagnosability with respect to a failure partition)
FAUDES_API bool IsEventDiagnosable (const System &rGen, const AttributeFailureTypeMap &rFailureTypeMap, std::string &rReportString)
 Test a system's diagnosability with respect to a given failure partition. More...
 
FAUDES_API bool IsIndicatorEventDiagnosable (const System &rGen, const AttributeFailureTypeMap &rFailureTypeMap, std::string &rReportString)
 Test a system's I-diagnosability with respect to a given failure partition. More...
 
FAUDES_API bool MeetsDiagnosabilityAssumptions (const System &rGen, const AttributeFailureTypeMap &rFailureTypeMap, std::string &rReportString)
 Check if a generator meets the general assumptions of diagnosability as required by IsDiagnosable(const System&, const AttributeFailureTypeMap&, std::string&) and IsIndicatorDiagnosable(const System&, const AttributeFailureTypeMap&, std::string&). More...
 
Functions (verification and computation of loop-preserving observers)
bool IsLoopPreservingObserver (const System &rGen, const EventSet &rHighAlph)
 Verifies a loop-preserving observer. More...
 
void LoopPreservingObserver (const System &rGen, const EventSet &rInitialHighAlph, EventSet &rHighAlph)
 Computes a loop-preserving observer with minimal state size of the abstraction. More...
 
Functions (diagnosability with respect to a specification)
FAUDES_API bool IsLanguageDiagnosableX (const System &rGen, const System &rSpec, std::string &rReportString)
 Tests a system's diagnosability with respect to a given specification. More...
 
Functions (modular diagnosability)
FAUDES_API bool IsModularDiagnosable (const SystemVector &rGsubs, const GeneratorVector &rKsubs, std::string &rReportString)
 Checks modular diagnosability for a system G (which consists of the subsystems rGsubs) with respect to the specification K (consisting of local specifications rKsubs) and the local abstraction alphabets rHighAlphSubs. More...
 

Variables

template class FAUDES_API TcGenerator< AttributeVoid, AttributeVoid, AttributeCFlags, AttributeVoid >
 
TokenWritergTestProtocolTw =NULL
 
std::string gTestProtocolFr
 
static bool(* gBreakFnct )(void)=0
 
static long ran_seed [STREAMS] = {DEFAULT}
 
static int ran_stream = 0
 
static int ran_initialized = 0
 
AutoRegisterType< mbDevicegRtiRegisterSpiDevice ("ModbusDevice")
 
AutoRegisterType< TaNameSet< AttributeSignalEvent > > gRti1RegisterSignalDeviceEventSet ("SignalDeviceEventSet")
 
AutoRegisterXElementTag< TaNameSet< AttributeSignalEvent > > gRti1XElementTagSignalDeviceEventSet ("SignalDeviceEventSet", "Event")
 
AutoRegisterType< nDevicegRtiRegisterSimplenetDevice ("SimplenetDevice")
 
static volatile AutoRegisterType< xDevicegRtiRegisterDeviceContainer ("DeviceContainer")
 
FAUDES_API std::string faudes_lastline
 

Detailed Description

libFAUDES resides within the namespace faudes.

Plug-Ins may use the same namespace.

Typedef Documentation

◆ AlphaberVector

Convenience typedef.

Definition at line 243 of file cfl_cgenerator.h.

◆ cEventSet

Compatibility: pre 2.20b used cEventSet as C++ class name.

Definition at line 247 of file cfl_cgenerator.h.

◆ cEventSetVector

Definition at line 248 of file cfl_cgenerator.h.

◆ cGenerator

Compatibility: pre 2.20b used cGenerator as C++ class name.

Definition at line 923 of file cfl_cgenerator.h.

◆ cGeneratorVector

Definition at line 924 of file cfl_cgenerator.h.

◆ diagGenerator

Compatibility: pre 2.20b used diagGenerator as C++ class name.

Definition at line 201 of file diag_generator.h.

◆ Diagnoser

◆ Float

typedef double faudes::Float

Type definition for real type.

Definition at line 52 of file cfl_definitions.h.

◆ fType

typedef unsigned long int faudes::fType

Convenience typdef flag data.

Definition at line 185 of file cfl_attributes.h.

◆ Graph

Definition at line 484 of file cfl_project.cpp.

◆ HioConstraint

◆ HioController

◆ HioEnvironment

◆ HioPlant

◆ Idx

typedef uint32_t faudes::Idx

Type definition for index type (allways 32bit)

Definition at line 43 of file cfl_definitions.h.

◆ Int

typedef long int faudes::Int

Type definition for integer type (let target system decide, minimum 32bit)

Definition at line 47 of file cfl_definitions.h.

◆ IntegerVector

Definition at line 218 of file cfl_elementary.h.

◆ IosEventSet

Definition at line 227 of file ios_attributes.h.

◆ IosStateSet

◆ IoSystem

◆ LhaStateSet

◆ LhaTransSet

◆ LinearHybridAutomaton

Convenience typedef for std lhaGenerator.

Definition at line 677 of file hyb_hgenerator.h.

◆ mtcGenerator

Compatibility: pre 2.20b used mtcGenerator as C++ class name.

Definition at line 751 of file mtc_generator.h.

◆ MtcSystem

◆ Node

Definition at line 483 of file cfl_project.cpp.

◆ SetX1Ev

typedef std::set<std::pair<Idx,Idx> > faudes::SetX1Ev

Definition at line 70 of file cfl_conflequiv.cpp.

◆ swig_cast_info

◆ swig_converter_func

typedef void*(* faudes::swig_converter_func) (void *, int *)

Definition at line 55 of file lbp_function.cpp.

◆ swig_dycast_func

typedef struct swig_type_info*(* faudes::swig_dycast_func) (void **)

Definition at line 55 of file lbp_function.cpp.

◆ swig_type_info

◆ tGenerator

Compatibility: pre 2.20b used tGenerator as C++ class name.

Definition at line 781 of file tp_tgenerator.h.

◆ TimedGenerator

Convenience typedef for std TimedGenerator.

Definition at line 776 of file tp_tgenerator.h.

Enumeration Type Documentation

◆ VerifierStateLabel

Enumerator
NORMAL 
CONFUSED 
BLOCK 

Definition at line 88 of file diag_languagediagnosis.h.

Function Documentation

◆ ActiveBackwardTransSet()

FAUDES_API TransSet faudes::ActiveBackwardTransSet ( const System rGen,
Idx  state 
)

Obtain all transitions from other states into a given state of a generator.

Parameters
rGenA generator.
stateA state from the generators state set.
Returns
A transition set.

Definition at line 802 of file diag_eventdiagnosis.cpp.

◆ ActiveEventsRule()

void faudes::ActiveEventsRule ( Generator g,
const EventSet silent 
)

Definition at line 260 of file cfl_conflequiv.cpp.

◆ ActiveNonTauEvs()

void faudes::ActiveNonTauEvs ( const Generator rGen,
const EventSet silent,
const Idx state,
EventSet result 
)

Definition at line 189 of file cfl_conflequiv.cpp.

◆ AdjustHioController()

void faudes::AdjustHioController ( const HioController rHioController,
const HioModule rHioModule1,
const HioModule rHioModule2,
HioController rResEnv 
)

Definition at line 604 of file hio_module.cpp.

◆ aParallel()

FAUDES_API void faudes::aParallel ( const GeneratorVector rGenVec,
Generator rResGen 
)

Parallel composition.

See also aParallel(const Generator&, const Generator&, Generator&). This version takes a vector of generators as argument to perform a synchronous composition of multiple generators. The implementation calls the std aParallel multiple times, future implementations may explore the overall reachable state set.

Parameters
rGenVecVector of input generators
rResGenReference to resulting composition generator

Definition at line 87 of file cfl_parallel.cpp.

◆ AppendOmegaTermination()

void faudes::AppendOmegaTermination ( Generator rGen)

Definition at line 52 of file cfl_conflequiv.cpp.

◆ backwardReachabilityObsOCC()

void faudes::backwardReachabilityObsOCC ( const TransSetX2EvX1 rTransSetX2EvX1,
const EventSet rControllableEvents,
const EventSet rHighAlph,
Idx  exitState,
Idx  currentState,
bool  controllablePath,
map< Idx, map< Idx, bool > > &  rExitLocalStatesMap,
StateSet rDoneStates 
)

Definition at line 1132 of file op_observercomputation.cpp.

◆ backwardVerificationLCC()

FAUDES_API void faudes::backwardVerificationLCC ( const TransSetX2EvX1 rTransSetX2EvX1,
const EventSet rControllableEvents,
const EventSet rHighAlph,
Idx  exitState,
Idx  currentState,
bool  controllablePath,
std::map< Idx, bool > &  rLocalStatesMap,
StateSet rDoneStates 
)

Function that supports the verification of local control consistency (LCC).

This function performs a recursive backward reachability to find if from a state where an uncontrollable high-level event is possible, another state is only reachable by local strings that contaion at least one controllable event. If this is the case, LCC is violated.

Parameters
rTransSetX2EvX1reverse transition relation of the input generator
rControllableEventsset of controllable events
rHighAlphHigh level alphabet
exitStatestart state for backward reachability
currentStatecurrent state for backward reachability
controllablePathfalse if at least one uncontrollable path to the currentState exists
rLocalStatesMapmap for states and their controllability property
rDoneStatesstates that have already been visited

◆ backwardVerificationOCC()

FAUDES_API bool faudes::backwardVerificationOCC ( const Generator rLowGen,
const EventSet rControllableEvents,
const EventSet rHighAlph,
Idx  currentState 
)

Function that supports the verification of output control consistency (OCC).

This function performs a backward reachability to find if an uncontrollable high-level event is preemted by an uncontrollable low-level event. If this is the case, OCC is violated.

Parameters
rLowGenInput generator
rControllableEventsset of controllable events
rHighAlphHigh level alphabet
currentStatestart state for backward reachability
Returns
true if no controllable low-level event has been found

Definition at line 120 of file op_obserververification.cpp.

◆ BiggerMax()

bool faudes::BiggerMax ( std::vector< GeneratorVector::Position > &  rCandidate,
GeneratorVector rGenVec 
)

Definition at line 1013 of file syn_compsyn.cpp.

◆ BlockingSilentEvent()

void faudes::BlockingSilentEvent ( Generator g,
const EventSet silent 
)

Definition at line 386 of file cfl_conflequiv.cpp.

◆ calcAbstAlphClosed() [1/4]

void faudes::calcAbstAlphClosed ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Idx, std::set< Idx > > &  rMapRelabeledEvents 
)

L(G)-observer computation.

This function is called by calcAbstAlphClosed(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an L(G)-observer for the prefix-closed language of the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

the alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs rGenObs must be a deterministic generator no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEventsMaps the original events to sets of newly introduced events (accumulatoive, call clear before)

Definition at line 678 of file op_observercomputation.cpp.

◆ calcAbstAlphClosed() [2/4]

void faudes::calcAbstAlphClosed ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

L(G)-observer computation.

This function is called by void calcAbstAlphClosed(Generator& rGenObs, EventSet& rControllableEvents, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the prefix-closed language of the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 701 of file op_observercomputation.cpp.

◆ calcAbstAlphClosed() [3/4]

FAUDES_API void faudes::calcAbstAlphClosed ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Idx, std::set< Idx > > &  rMapRelabeledEvents 
)

L(G)-observer computation.

This function is called by calcAbstAlphClosed(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an L(G)-observer for the prefix-closed language of the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

the alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs rGenObs must be a deterministic generator no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEventsMaps the original events to sets of newly introduced events (accumulatoive, call clear before)

Definition at line 678 of file op_observercomputation.cpp.

◆ calcAbstAlphClosed() [4/4]

FAUDES_API void faudes::calcAbstAlphClosed ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

L(G)-observer computation.

This function is called by void calcAbstAlphClosed(Generator& rGenObs, EventSet& rControllableEvents, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the prefix-closed language of the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 701 of file op_observercomputation.cpp.

◆ calcAbstAlphMSA() [1/4]

void faudes::calcAbstAlphMSA ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Idx, std::set< Idx > > &  rMapRelabeledEvents 
)

MSA-observer computation.

This function is called by calcAbstAlphMSA(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an MSA-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. Schmidt and Th. Moor, "Marked String Accepting Observers for the Hierarchical and Decentralized Control of Discrete Event Systems," Workshop on Discrete Event Systems, 2006.

the alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs rGenObs must be a deterministic generator no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEventsMaps the original events to sets of newly introduced events (accumulatoive, call clear before)

Definition at line 836 of file op_observercomputation.cpp.

◆ calcAbstAlphMSA() [2/4]

void faudes::calcAbstAlphMSA ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

MSA-observer computation.

This function is called by void calcAbstAlphMSA(Generator& rGenObs, EventSet& rControllableEvents, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an MSA-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. Schmidt and Th. Moor, "Marked String Accepting Observers for the Hierarchical and Decentralized Control of Discrete Event Systems," Workshop on Discrete Event Systems, 2006.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 859 of file op_observercomputation.cpp.

◆ calcAbstAlphMSA() [3/4]

void faudes::calcAbstAlphMSA ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Idx, std::set< Idx > > &  rMapRelabeledEvents 
)

MSA-observer computation.

This function is called by calcAbstAlphMSA(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an MSA-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. Schmidt and Th. Moor, "Marked String Accepting Observers for the Hierarchical and Decentralized Control of Discrete Event Systems," Workshop on Discrete Event Systems, 2006.

the alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs rGenObs must be a deterministic generator no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEventsMaps the original events to sets of newly introduced events (accumulatoive, call clear before)

Definition at line 836 of file op_observercomputation.cpp.

◆ calcAbstAlphMSA() [4/4]

FAUDES_API void faudes::calcAbstAlphMSA ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

MSA-observer computation.

This function is called by void calcAbstAlphMSA(Generator& rGenObs, EventSet& rControllableEvents, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an MSA-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. Schmidt and Th. Moor, "Marked String Accepting Observers for the Hierarchical and Decentralized Control of Discrete Event Systems," Workshop on Discrete Event Systems, 2006.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 859 of file op_observercomputation.cpp.

◆ calcAbstAlphMSALCC() [1/2]

void faudes::calcAbstAlphMSALCC ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

MSA-observer computation including local control consistency (LCC).

This function is called by calcAbstAlphMSALCC(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx,set<Idx > > & rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an MSA-observer for the language marked by the resulting generator and at the same time fulfills the local control consistency condition (LCC). This function evaluates the observer algorithm as described in K. Schmidt and C. Breindl, "On Maximal Permissiveness of Hierarchical and Modular Supervisory Control Approaches for Discrete Event Systems, Workshop on Discrete Event Systems, 2008. with an extension to LCC as indicated in K. Schmidt and C. Breindl, "On Maximal Permissiveness of Hierarchical and Modular Supervisory Control Approaches for Discrete Event Systems," Workshop on Discrete Event Systems, 2008.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 1272 of file op_observercomputation.cpp.

◆ calcAbstAlphMSALCC() [2/2]

FAUDES_API void faudes::calcAbstAlphMSALCC ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

MSA-observer computation including local control consistency (LCC).

This function is called by calcAbstAlphMSALCC(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx,set<Idx > > & rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an MSA-observer for the language marked by the resulting generator and at the same time fulfills the local control consistency condition (LCC). This function evaluates the observer algorithm as described in K. Schmidt and C. Breindl, "On Maximal Permissiveness of Hierarchical and Modular Supervisory Control Approaches for Discrete Event Systems, Workshop on Discrete Event Systems, 2008. with an extension to LCC as indicated in K. Schmidt and C. Breindl, "On Maximal Permissiveness of Hierarchical and Modular Supervisory Control Approaches for Discrete Event Systems," Workshop on Discrete Event Systems, 2008.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 1272 of file op_observercomputation.cpp.

◆ calcAbstAlphObs() [1/9]

void faudes::calcAbstAlphObs ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Idx, std::set< Idx > > &  rMapRelabeledEvents 
)

Lm-observer computation.

This function is called by calcAbstAlphObs(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

the alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs rGenObs must be a deterministic generator no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEventsMaps the original events to sets of newly introduced events (accumulatoive, call clear before)

Definition at line 757 of file op_observercomputation.cpp.

◆ calcAbstAlphObs() [2/9]

void faudes::calcAbstAlphObs ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

Lm-observer computation.

This function is called by void calcAbstAlphObs(Generator& rGenObs, EventSet& rControllableEvents, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 780 of file op_observercomputation.cpp.

◆ calcAbstAlphObs() [3/9]

FAUDES_API void faudes::calcAbstAlphObs ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Idx, std::set< Idx > > &  rMapRelabeledEvents 
)

Lm-observer computation.

This function is called by calcAbstAlphObs(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

the alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs rGenObs must be a deterministic generator no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEventsMaps the original events to sets of newly introduced events (accumulatoive, call clear before)

Definition at line 757 of file op_observercomputation.cpp.

◆ calcAbstAlphObs() [4/9]

FAUDES_API void faudes::calcAbstAlphObs ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

Lm-observer computation.

This function is called by void calcAbstAlphObs(Generator& rGenObs, EventSet& rControllableEvents, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx, set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 780 of file op_observercomputation.cpp.

◆ calcAbstAlphObs() [5/9]

void faudes::calcAbstAlphObs ( MtcSystem rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Idx, std::set< Idx > > &  rMapRelabeledEvents 
)

Lm-observer computation.

This function is called by calcAbstAlphObs(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, std::map<Idx, std::set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

the alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs rGenObs must be a deterministic generator no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEventsMaps the original events to sets of newly introduced events (accumulatoive, call clear before)

Definition at line 71 of file mtc_observercomputation.cpp.

◆ calcAbstAlphObs() [6/9]

void faudes::calcAbstAlphObs ( MtcSystem rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

Lm-observer computation.

This function is called by void calcAbstAlphObs(Generator& rGenObs, EventSet& rControllableEvents, EventSet& rHighAlph, EventSet& rNewHighAlph, std::map<Idx, std::set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 94 of file mtc_observercomputation.cpp.

◆ calcAbstAlphObs() [7/9]

FAUDES_API void faudes::calcAbstAlphObs ( MtcSystem rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Idx, std::set< Idx > > &  rMapRelabeledEvents 
)

Lm-observer computation.

This function is called by calcAbstAlphObs(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, std::map<Idx, std::set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

the alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs rGenObs must be a deterministic generator no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEventsMaps the original events to sets of newly introduced events (accumulatoive, call clear before)

Definition at line 71 of file mtc_observercomputation.cpp.

◆ calcAbstAlphObs() [8/9]

FAUDES_API void faudes::calcAbstAlphObs ( MtcSystem rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

Lm-observer computation.

This function is called by void calcAbstAlphObs(Generator& rGenObs, EventSet& rControllableEvents, EventSet& rHighAlph, EventSet& rNewHighAlph, std::map<Idx, std::set<Idx> >& rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 94 of file mtc_observercomputation.cpp.

◆ calcAbstAlphObs() [9/9]

FAUDES_API void faudes::calcAbstAlphObs ( System rGenObs,
EventSet rHighAlph,
EventSet rNewHighAlph,
EventRelabelMap rMapRelabeledEvents 
)

Rti convenience wrapper.

Definition at line 1914 of file op_observercomputation.cpp.

◆ calcAbstAlphObsLCC() [1/2]

void faudes::calcAbstAlphObsLCC ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

Lm-observer computation including local control consistency (LCC).

This function is called by calcAbstAlphObsLCC(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx,set<Idx > > & rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator and at the same time fulfills the local control consistency condition (LCC). This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004. with an extension to LCC as indicated in K. Schmidt and C. Breindl, "On Maximal Permissiveness of Hierarchical and Modular Supervisory Control Approaches for Discrete Event Systems," Workshop on Discrete Event Systems, 2008.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 1198 of file op_observercomputation.cpp.

◆ calcAbstAlphObsLCC() [2/2]

FAUDES_API void faudes::calcAbstAlphObsLCC ( Generator rGenObs,
EventSet rControllableEvents,
EventSet rHighAlph,
EventSet rNewHighAlph,
std::map< Transition, Idx > &  rMapChangedTrans 
)

Lm-observer computation including local control consistency (LCC).

This function is called by calcAbstAlphObsLCC(System& rGenObs, EventSet& rHighAlph, EventSet& rNewHighAlph, map<Idx,set<Idx > > & rMapRelabeledEvents). It modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator and at the same time fulfills the local control consistency condition (LCC). This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004. with an extension to LCC as indicated in K. Schmidt and C. Breindl, "On Maximal Permissiveness of Hierarchical and Modular Supervisory Control Approaches for Discrete Event Systems," Workshop on Discrete Event Systems, 2008.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEventsSet of controllable events
rHighAlphInitial abstraction alphabet
rNewHighAlphModified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTransMaps the original relabeled transitions to the new events

Definition at line 1198 of file op_observercomputation.cpp.

◆ calculateDynamicSystemClosedObs()

FAUDES_API void faudes::calculateDynamicSystemClosedObs ( const Generator rGen,
EventSet rHighAlph,
Generator rGenDyn 
)

Computation of the dynamic system for Delta_sigma (reachable states after the occurrence of one high-level event).

This function computes the part of the dynamic system that is needed for evaluating the observer algorithm for closed languages.

The alphabet rHighAlph has to be a subset of the alphabet of rGen. rGen must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenGenerator for which the dynamic system is computed
rHighAlphAbstraction alphabet
rGenDynGenerator representing the dynamic system

Definition at line 46 of file op_observercomputation.cpp.

◆ calculateDynamicSystemLCC()

void faudes::calculateDynamicSystemLCC ( const Generator rGen,
const EventSet rControllableEvents,
const EventSet rHighAlph,
Generator rGenDyn 
)

Computation of the dynamic system for Delta_lcc (fulfillment of the local control consistency property).

This function computes the part of the dynamic system that is needed for evaluating the observer algorithm for local control consistency

The alphabet rHighAlph has to be a subset of the alphabet of rGen. rGen must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenGenerator for which the dynamic system is computed
rControllableEventsSet of controllable events
rHighAlphAbstraction alphabet
rGenDynGenerator representing the dynamic system

Definition at line 303 of file op_observercomputation.cpp.

◆ calculateDynamicSystemMSA()

FAUDES_API void faudes::calculateDynamicSystemMSA ( const Generator rGen,
EventSet rHighAlph,
Generator rGenDyn 
)

Computation of the dynamic system for Delta_msa (local fulfillment of the msa-observer property).

This function computes the part of the dynamic system that is needed for evaluating the observer algorithm for msa-observers.

The alphabet rHighAlph has to be a subset of the alphabet of rGen. rGen must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenGenerator for which the dynamic system is computed
rHighAlphAbstraction alphabet
rGenDynGenerator representing the dynamic system

Definition at line 195 of file op_observercomputation.cpp.

◆ calculateDynamicSystemObs() [1/2]

void faudes::calculateDynamicSystemObs ( const Generator rGen,
EventSet rHighAlph,
Generator rGenDyn 
)

Computation of the dynamic system for Delta_obs (local reachability of a marked state).

This function computes the part of the dynamic system that is needed for evaluating the observer algorithm for marked languages.

The alphabet rHighAlph has to be a subset of the alphabet of rGen. rGen must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenGenerator for which the dynamic system is computed
rHighAlphAbstraction alphabet
rGenDynGenerator representing the dynamic system

Definition at line 159 of file op_observercomputation.cpp.

◆ calculateDynamicSystemObs() [2/2]

FAUDES_API void faudes::calculateDynamicSystemObs ( const MtcSystem rGen,
EventSet rHighAlph,
Generator rGenDyn 
)

Computation of the dynamic system for an Lm-observer.

This function computes the dynamic system that is needed for evaluating the observer algorithm.

The alphabet rHighAlph has to be a subset of the alphabet of rGen. rGen must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenGenerator for which the dynamic system is computed
rHighAlphAbstraction alphabet
rGenDynGenerator representing the dynamic system

Definition at line 138 of file mtc_observercomputation.cpp.

◆ CDExt()

FAUDES_API void faudes::CDExt ( const Generator gen,
const EventSetVector ee,
const EventSet unionset,
EventSet ek 
)

Definition at line 99 of file con_decomposability_extension.cpp.

◆ CheckSplit() [1/2]

bool faudes::CheckSplit ( const Generator rGen,
const EventSet rSplitAlphabet,
const vector< pair< StateSet, Idx > > &  rNondeterministicStates,
Idx  entryState 
)

Definition at line 634 of file op_observercomputation.cpp.

◆ CheckSplit() [2/2]

FAUDES_API bool faudes::CheckSplit ( const Generator rGenObs,
const EventSet rSplitAlphabet,
const std::vector< std::pair< StateSet, Idx > > &  rNondeterministicStates,
Idx  entryState 
)

Check if the current alphabet splits all local automata with nondeterminims or unobservable transitions.

This algorithm verifies if nondetermisisms or unobservable transitions are resolved if the given events in are added to the high-level alphabet. The function is called by ExtendHighAlphabet,

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters
rGenObsLow-level generator. It is modified by the algorithm by relabeling transitions and events
rSplitAlphabetReference to the current alphabet for splitting verification
rNondeterministicStatesvector with states where nondeterminism has to be resolved and the related event
entryStatecurrent state that is investigated

◆ CollapsString()

FAUDES_API std::string faudes::CollapsString ( const std::string &  rString,
unsigned int  len = FD_MAXCONTAINERNAME 
)

Limit length of string, return head and tail of string.

Parameters
rStringstring
lenMaximum number of charakters in string (approx)
Returns
Collapsed string

Definition at line 91 of file cfl_helper.cpp.

◆ ComposedColorSet()

FAUDES_API void faudes::ComposedColorSet ( const MtcSystem rGen1,
const Idx  stdidx1,
ColorSet colors1,
const MtcSystem rGen2,
const Idx  stdidx2,
ColorSet colors2,
ColorSet composedSet 
)

Compose the color set for a state combined from two states in two distinct automata.

Parameters
rGen1First MtcSystem for parallel composition
stdidx1Index to first MtcSystem's current state
colors1Color set of first MtcSystem
rGen2Second MtcSystem for parallel composition
stdidx2Index to second MtcSystem's current state
colors2Color set of second MtcSystem
composedSetColor set where composition colors will be inserted
Exceptions
Exception
  • Index not member of set (id 200)
  • Index not found in set (id 201)

Definition at line 213 of file mtc_parallel.cpp.

◆ CompositionalSynthesisUnchecked()

FAUDES_API void faudes::CompositionalSynthesisUnchecked ( const GeneratorVector rPlantGenVec,
const EventSet rConAlph,
const GeneratorVector rSpecGenVec,
std::map< Idx, Idx > &  rMapEventsToPlant,
GeneratorVector rDisGenVec,
GeneratorVector rSupGenVec 
)

Compositional synthesis.

Variant of CompositionalSynthesis(const GeneratorVector&,const EventSet&,const GeneratorVector&,std::map<Idx,Idx>&,GeneratorVector&,GeneratorVector&); without parameter-consistency test.

Parameters
rPlantGenVecPlant components (must be deterministic)
rConAlphOverall set of controllable events
rSpecGenVecSpecification components (must be deterministic)
rMapEventsToPlantResulting event map
rDisGenVecResulting distinuisher automata
rSupGenVecResulting supervisor automata

Definition at line 1361 of file syn_compsyn.cpp.

◆ CompositionMap1()

void faudes::CompositionMap1 ( const std::map< std::pair< Idx, Idx >, Idx > &  rCompositionMap,
std::map< Idx, Idx > &  rCompositionMap1 
)

Definition at line 677 of file cfl_parallel.cpp.

◆ CompositionMap2()

void faudes::CompositionMap2 ( const std::map< std::pair< Idx, Idx >, Idx > &  rCompositionMap,
std::map< Idx, Idx > &  rCompositionMap2 
)

Definition at line 689 of file cfl_parallel.cpp.

◆ ComputeAbstractBisimulationSatCTA()

void faudes::ComputeAbstractBisimulationSatCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult,
const Idx rFlag,
const std::vector< StateSet > &  rPrePartition 
)

ComputeAbstractBisimulationSatCTA saturation and change-tracking based partition algorithm for either delayed or weak bisimulation. This function is intended to be invoked by ComputeDelayedBisimulation_Sat or ComputeWeakBisimulation_Sat, not for direct external usage.

Parameters
rGeninput gen
rSilentsilent event set (contains either 0 or 1 event)
rResultstate partition without trivial classes
rFlagrFlag == 1: dalayed bisimulation; rFlag == 2: weak bisimulation
rPrePartitionprepartition (trivial classes MUST be included)

Definition at line 983 of file cfl_bisimcta.cpp.

◆ ComputeBisimulationCTA() [1/4]

FAUDES_API void faudes::ComputeBisimulationCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult 
)

ComputeBisimulationCTA bisimulation partition based on change-tracking algorithm and topo sort.

Parameters
rGeninput gen
rSilentsilent event set (contains either 0 or 1 event)
rResultstate partition without trivial classes

◆ ComputeBisimulationCTA() [2/4]

void faudes::ComputeBisimulationCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult,
const std::vector< StateSet > &  rPrePartition 
)

Definition at line 948 of file cfl_bisimcta.cpp.

◆ ComputeBisimulationCTA() [3/4]

FAUDES_API void faudes::ComputeBisimulationCTA ( const Generator rGen,
std::list< StateSet > &  rResult 
)

ComputeBisimulationCTA basic bisimulation partition algorithm based on change-tracking algorithm.

Parameters
rGeninput gen
rResultstate partition without trivial classes

Definition at line 924 of file cfl_bisimcta.cpp.

◆ ComputeBisimulationCTA() [4/4]

FAUDES_API void faudes::ComputeBisimulationCTA ( const Generator rGen,
std::list< StateSet > &  rResult,
const std::vector< StateSet > &  rPrePartition 
)

ComputeBisimulationCTA basic bisimulation partition algorithm under prepartition based on change-tracking algorithm.

Parameters
rGeninput gen
rResultstate partition without trivial classes
rPrePartitionprepartition (trivial classes MUST be included)

Definition at line 930 of file cfl_bisimcta.cpp.

◆ ComputeComputeWeakBisimulationSatCTA()

FAUDES_API void faudes::ComputeComputeWeakBisimulationSatCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult,
const std::vector< StateSet > &  rPrePartition 
)

ComputeComputeWeakBisimulationSatCTA weak bisimulation partition under prepartition based on change-tracking algorithm and saturation.

Parameters
rGeninput gen
rSilentsilent event set (contains either 0 or 1 event)
rResultstate partition without trivial classes
rPrePartitionprepartition (trivial classes MUST be included)

◆ ComputeDelayedBisimulationCTA() [1/2]

void faudes::ComputeDelayedBisimulationCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult 
)

Definition at line 935 of file cfl_bisimcta.cpp.

◆ ComputeDelayedBisimulationCTA() [2/2]

FAUDES_API void faudes::ComputeDelayedBisimulationCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult,
const std::vector< StateSet > &  rPrePartition 
)

ComputeDelayedBisimulationCTA delayed bisimulation partition under prepartition based on change-tracking algorithm and topo sort.

ComputeDelayedBisimulationCTA delayed bisimulation partition under prepartition based on change-tracking algorithm and saturation.

Parameters
rGeninput gen
rSilentsilent event set (contains either 0 or 1 event)
rResultstate partition without trivial classes
rPrePartitionprepartition (trivial classes MUST be included)

◆ ComputeDelayedBisimulationSatCTA() [1/2]

FAUDES_API void faudes::ComputeDelayedBisimulationSatCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult 
)

ComputeDelayedBisimulationSatCTA delayed bisimulation partition based on change-tracking algorithm and saturation.

Parameters
rGeninput gen
rSilentsilent event set (contains either 0 or 1 event)
rResultstate partition without trivial classes

Definition at line 999 of file cfl_bisimcta.cpp.

◆ ComputeDelayedBisimulationSatCTA() [2/2]

void faudes::ComputeDelayedBisimulationSatCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult,
const std::vector< StateSet > &  rPrePartition 
)

Definition at line 1009 of file cfl_bisimcta.cpp.

◆ ComputeGd() [1/2]

void faudes::ComputeGd ( const Diagnoser rGobs,
map< pair< Idx, Idx >, Idx > &  rReverseCompositionMap,
System rGd 
)

Definition at line 588 of file diag_eventdiagnosis.cpp.

◆ ComputeGd() [2/2]

FAUDES_API void faudes::ComputeGd ( const Diagnoser rGobs,
std::map< std::pair< Idx, Idx >, Idx > &  rReverseCompositionMap,
System rGd 
)

Compute the diagnosability testing generator G_d as a parallel composition of G_o with itself (according to Jiang).

Parameters
rGobsInput diagnoser G_o.
rReverseCompositionMapOutput variable containing the mapping of G_o states and G_d states (generated by Parallel()).
rGdOutput variable for G_d.

◆ ComputeGobs() [1/4]

FAUDES_API void faudes::ComputeGobs ( const System rGenMarkedNonSpecBehaviour,
Diagnoser rGobs 
)

Compute G_o for a generator that marks the faulty behaviour of a plant.

Every specification violation will be labelled with label "F".

Parameters
rGenMarkedNonSpecBehaviourInput generator that specifies specification violations by marked states.
rGobsOutput variable for G_o.

Definition at line 27 of file diag_languagediagnosis.cpp.

◆ ComputeGobs() [2/4]

FAUDES_API void faudes::ComputeGobs ( const System rOrigGen,
const AttributeFailureTypeMap rAttrFTMap,
Diagnoser rGobs 
)

Compute G_o for a given generator with a given failure partition (according to Jiang).

Parameters
rOrigGenInput generator, which is a model of the original plant containing the relevant failures events.
rAttrFTMapFailure partition.
rGobsOutput variable for G_o.
Exceptions
Exception
  • Input generator has no unique initial state (id 301).

Definition at line 431 of file diag_eventdiagnosis.cpp.

◆ ComputeGobs() [3/4]

FAUDES_API void faudes::ComputeGobs ( const System rOrigGen,
const std::string &  rFailureType,
const EventSet rFailureEvents,
Diagnoser rGobs 
)

Compute G_o for a single failure type of a generator.

Parameters
rOrigGenInput generator, which is a model of the original plant containing the relevant failures events.
rFailureTypeFailure type name.
rFailureEventsFailure events belonging to the failure type.
rGobsOutput variable for G_o.

◆ ComputeGobs() [4/4]

void faudes::ComputeGobs ( const System rOrigGen,
const string &  rFailureType,
const EventSet rFailureEvents,
Diagnoser rGobs 
)

Definition at line 423 of file diag_eventdiagnosis.cpp.

◆ ComputeHSupConNB()

void faudes::ComputeHSupConNB ( const Generator rOrigGen,
const EventSet rConAlph,
const EventSet rLocAlph,
Generator rHSupGen 
)

halbway-synthesis

Parameters
rOrigGenthe resulting composed new generator from synthesis-buffer
rConAlphcontrollable events
rLocAlphlocal events
rHSupGenthe resulting generator after halbway-synthesis

Definition at line 1225 of file syn_compsyn.cpp.

◆ ComputeReachability() [1/4]

void faudes::ComputeReachability ( const System rGen,
const EventSet rUnobsEvents,
const EventSet rFailures,
Idx  State,
const AttributeFailureTypeMap rAttrFTMap,
map< Idx, multimap< Idx, DiagLabelSet > > &  rReachabilityMap 
)

Definition at line 703 of file diag_eventdiagnosis.cpp.

◆ ComputeReachability() [2/4]

FAUDES_API void faudes::ComputeReachability ( const System rGen,
const EventSet rUnobsEvents,
const EventSet rFailures,
Idx  State,
const AttributeFailureTypeMap rAttrFTMap,
std::map< Idx, std::multimap< Idx, DiagLabelSet > > &  rReachabilityMap 
)

Compute the reachability from a given generator state through a trace that consists of arbitrarily many unobservable events followed by one observable event.

Parameters
rGenInput generator.
rUnobsEventsUnobservable events in the generators alphabet.
rFailuresUnobservable failure events in the generators alphabet.
StateA state of the generators state set.
rAttrFTMapFailure partition.
rReachabilityMapOutput variable for the reachability. Maps occurring observable events to the reachable generator states and the corresponding failure types that occurred within the unobservable part of the trace.

◆ ComputeReachability() [3/4]

void faudes::ComputeReachability ( const System rGen,
const EventSet rUnobsEvents,
Idx  State,
map< Idx, multimap< Idx, DiagLabelSet > > &  rReachabilityMap 
)

Definition at line 180 of file diag_languagediagnosis.cpp.

◆ ComputeReachability() [4/4]

FAUDES_API void faudes::ComputeReachability ( const System rGen,
const EventSet rUnobsEvents,
Idx  State,
std::map< Idx, std::multimap< Idx, DiagLabelSet > > &  rReachabilityMap 
)

Compute the reachability from a state of a generator that marks its faulty behaviour.

States are said to be reachable if they can be reached through a trace that consists of arbitrarily many unobservable events followed by one observable event.

Parameters
rGenInput generator.
rUnobsEventsUnobservable events in the generators alphabet.
StateA state of the generators state set.
rReachabilityMapOutput variable for the reachability. Maps occurring observable events to the reachable generator states and a label that contains information about specification violations.

◆ ComputeReachabilityRecursive() [1/4]

void faudes::ComputeReachabilityRecursive ( const System rGen,
const EventSet rUnobsEvents,
const EventSet rFailures,
Idx  State,
const AttributeFailureTypeMap rAttrFTMap,
map< Idx, multimap< Idx, DiagLabelSet > > &  rReachabilityMap,
const DiagLabelSet  FToccurred 
)

Definition at line 729 of file diag_eventdiagnosis.cpp.

◆ ComputeReachabilityRecursive() [2/4]

FAUDES_API void faudes::ComputeReachabilityRecursive ( const System rGen,
const EventSet rUnobsEvents,
const EventSet rFailures,
Idx  State,
const AttributeFailureTypeMap rAttrFTMap,
std::map< Idx, std::multimap< Idx, DiagLabelSet > > &  rReachabilityMap,
const DiagLabelSet  FToccurred 
)

Auxiliary function for ComputeReachability(const System&, const EventSet&, const EventSet&, Idx, const AttributeFailureTypeMap&, std::map<Idx,std::multimap<Idx,DiagLabelSet>>&).

Is recursively called for every occurring state on the trace (that consists of arbitrarily many unobservable events followed by one observable event).

Parameters
rGenInput generator.
rUnobsEventsUnobservable events in the generators alphabet.
rFailuresUnobservable failure events in the generators alphabet.
StateThe current state within the trace.
rAttrFTMapFailure partition.
rReachabilityMapOutput variable for the reachability. Maps occurring observable events to the reachable generator states and the coresponing failure types that occurred within the unobservable part of the trace.
FToccurredCollects occurring failure types.

◆ ComputeReachabilityRecursive() [3/4]

void faudes::ComputeReachabilityRecursive ( const System rGen,
const EventSet rUnobsEvents,
Idx  State,
StateSet  done,
map< Idx, multimap< Idx, DiagLabelSet > > &  rReachabilityMap 
)

Definition at line 207 of file diag_languagediagnosis.cpp.

◆ ComputeReachabilityRecursive() [4/4]

void faudes::ComputeReachabilityRecursive ( const System rGen,
const EventSet rUnobsEvents,
Idx  State,
StateSet  done,
std::map< Idx, std::multimap< Idx, DiagLabelSet > > &  rReachabilityMap 
)

Auxiliary function for ComputeReachability(const System&, const EventSet&, Idx State, std::map<Idx,std::multimap< Idx,DiagLabelSet> >&).

Is recursively called for every occurring state on the trace (that consists of arbitrarily many unobservable events followed by one observable event).

Parameters
rGenInput generator.
rUnobsEventsUnobservable events in the generators alphabet.
StateThe current state within the trace.
doneProgress.
rReachabilityMapOutput variable for the reachability. Maps occurring observable events to the reachable generator states and a label that contains information about specification violations.

◆ ComputeTildeG()

FAUDES_API Generator faudes::ComputeTildeG ( const EventSet unionset,
const EventSetVector ee,
const EventSet ek,
const Generator gen 
)

Definition at line 112 of file con_decomposability_extension.cpp.

◆ ComputeWeakBisimulation()

void faudes::ComputeWeakBisimulation ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult,
const std::vector< StateSet > &  rPrePartition 
)

Definition at line 972 of file cfl_bisimcta.cpp.

◆ ComputeWeakBisimulationCTA() [1/2]

FAUDES_API void faudes::ComputeWeakBisimulationCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult 
)

ComputeWeakBisimulationCTA weak bisimulation (aka observation eq) partition based on change-tracking algorithm and topo sort.

Parameters
rGeninput gen
rSilentsilent event set (contains either 0 or 1 event)
rResultstate partition without trivial classes

Definition at line 960 of file cfl_bisimcta.cpp.

◆ ComputeWeakBisimulationCTA() [2/2]

FAUDES_API void faudes::ComputeWeakBisimulationCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult,
const std::vector< StateSet > &  rPrePartition 
)

ComputeWeakBisimulationCTA weak bisimulation (aka observation eq) partition under prepartition based on change-tracking algorithm and topo sort.

Parameters
rGeninput gen
rSilentsilent event set (contains either 0 or 1 event)
rResultstate partition without trivial classes
rPrePartitionprepartition (trivial classes MUST be included)

◆ ComputeWeakBisimulationSatCTA() [1/2]

FAUDES_API void faudes::ComputeWeakBisimulationSatCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult 
)

ComputeWeakBisimulationSatCTA weak bisimulation (aka observation eq) partition based on change-tracking algorithm and saturation.

Parameters
rGeninput gen
rSilentsilent event set (contains either 0 or 1 event)
rResultstate partition without trivial classes

Definition at line 1004 of file cfl_bisimcta.cpp.

◆ ComputeWeakBisimulationSatCTA() [2/2]

void faudes::ComputeWeakBisimulationSatCTA ( const Generator rGen,
const EventSet rSilent,
std::list< StateSet > &  rResult,
const std::vector< StateSet > &  rPrePartition 
)

Definition at line 1013 of file cfl_bisimcta.cpp.

◆ ComputeWSOE()

void faudes::ComputeWSOE ( const Generator rGenOrig,
const EventSet rConAlph,
const EventSet rLocAlph,
std::map< Idx, Idx > &  rMapStateToPartition,
Generator rResGen 
)

weak synthesis obeservation equivalence [not implemented]

Parameters
rGenOrigoriginal generator
rConAlphcontrollable events
rLocAlphlocal events
rMapStateToPartitionmap state to equivalent class
rResGenthe quotient automaton

◆ ConcatenateFullLanguage()

FAUDES_API void faudes::ConcatenateFullLanguage ( Generator rGen)

ConcatenateFullLanguage: concatenate Sigma* to language marked by rGen.

Less expensive than using LanguageConcatenate() to concatenate Sigma*, as no additional nondeterminism is caused. Used in SupNorm(). Method: Transitions starting from marked states are erased. Remaining accessible marked states are provided with Sigma-selfloops. Determinism: Result can only become nondeterministic when a parameter is nondeterministic.

Parameters
rGengenerator marking the language to be concatenated with Sigma*

Definition at line 153 of file syn_supnorm.cpp.

◆ ConflictEquivalentAbstractionLoop()

void faudes::ConflictEquivalentAbstractionLoop ( vGenerator rGen,
EventSet rSilentEvents 
)

Definition at line 595 of file cfl_conflequiv.cpp.

◆ ConflictEquivalentAbstractionOnce()

void faudes::ConflictEquivalentAbstractionOnce ( Generator rGen,
EventSet silent 
)

Definition at line 570 of file cfl_conflequiv.cpp.

◆ ContributorsString()

FAUDES_API std::string faudes::ContributorsString ( )

Return contributors as std::string.

Returns
std::string

Definition at line 141 of file cfl_helper.cpp.

◆ ControlProblemConsistencyCheck() [1/3]

FAUDES_API void faudes::ControlProblemConsistencyCheck ( const Generator rPlantGen,
const EventSet rCAlph,
const EventSet rOAlph,
const Generator rSpecGen 
)

Consistency check for controlproblem input data.

Tests whether alphabets match and generators are deterministic.

Parameters
rPlantGenPlant generator
rCAlphControllable events
rOAlphObservable events
rSpecGenSpecification generator
Exceptions
Exception
  • lphabets of generators don't match (id 100)
  • plant generator nondeterministic (id 201)
  • specification generator nondeterministic (id 203)
  • plant and spec generator nondeterministic (id 204)

Definition at line 691 of file syn_supcon.cpp.

◆ ControlProblemConsistencyCheck() [2/3]

FAUDES_API void faudes::ControlProblemConsistencyCheck ( const Generator rPlantGen,
const EventSet rCAlph,
const Generator rSpecGen 
)

Consistency check for controlproblem input data.

Tests whether alphabets match and generators are deterministic.

Parameters
rPlantGenPlant generator
rCAlphControllable events
rSpecGenSpecification generator
Exceptions
Exception
  • lphabets of generators don't match (id 100)
  • plant generator nondeterministic (id 201)
  • specification generator nondeterministic (id 203)
  • plant and spec generator nondeterministic (id 204)

Definition at line 634 of file syn_supcon.cpp.

◆ ControlProblemConsistencyCheck() [3/3]

FAUDES_API void faudes::ControlProblemConsistencyCheck ( const GeneratorVector rPlantGenVec,
const EventSet rConAlph,
const GeneratorVector rSpecGenVec 
)

Compositional synthesis.

Text consistency of input-data fro compositional synthesis; through exception on error.

Parameters
rPlantGenVecPlant components (must be deterministic)
rConAlphOverall set of controllable events
rSpecGenVecSpecification components (must be deterministic)

Definition at line 1301 of file syn_compsyn.cpp.

◆ ConvertParallelCompositionMap() [1/2]

void faudes::ConvertParallelCompositionMap ( const map< pair< Idx, Idx >, Idx > &  rReverseCompositionMap,
map< Idx, pair< Idx, Idx > > &  rCompositionMap 
)

Definition at line 210 of file diag_eventdiagnosis.cpp.

◆ ConvertParallelCompositionMap() [2/2]

FAUDES_API void faudes::ConvertParallelCompositionMap ( const std::map< std::pair< Idx, Idx >, Idx > &  rReverseCompositionMap,
std::map< Idx, std::pair< Idx, Idx > > &  rCompositionMap 
)

Convert the reverse composition map of Parallel() by switching first and second entry.

Parameters
rReverseCompositionMapInput map as generated by Parallel().
rCompositionMapConverted map.

◆ cParallel() [1/3]

void faudes::cParallel ( const std::vector< const System * > &  rGens,
System rResGen 
)

Parallel composition of multiple generators.

Parameters
rGensSTL-vector of generators.
rResGenOutput variable for the resulting product generator.

◆ cParallel() [2/3]

void faudes::cParallel ( const std::vector< System > &  rGens,
System rResGen 
)

Parallel composition of multiple generators.

Parameters
rGensSTL-vector of generators.
rResGenOutput variable for the resulting product generator.

◆ cParallel() [3/3]

void faudes::cParallel ( const vector< System > &  rGens,
System rResGen 
)

Definition at line 270 of file diag_modulardiagnosis.cpp.

◆ CreateConstraint()

void faudes::CreateConstraint ( int  mType[5],
Generator constrP,
Generator constrE 
)

This function creates constraints which describe the condition of completeness and Yp-liveness of a Specification.

The implementation follows the same algorithm as the CreateSpec() function, and has the same limitation: it is only for use with a specific model

Parameters
mTypeBy the type we specify type of the specification to build constraint for
constrPGenerator to the resulting operator constraint for the specification
constrEGenerator to the resulting environment constraint for the specification

Definition at line 1810 of file hio_module.cpp.

◆ CreateEntryStatesMap()

void faudes::CreateEntryStatesMap ( const std::map< StateSet, Idx > &  rRevEntryStatesMap,
std::map< Idx, StateSet > &  rEntryStatesMap 
)

Definition at line 1536 of file cfl_project.cpp.

◆ CreateSpec()

void faudes::CreateSpec ( int  mType[5],
HioPlant rHioSpec,
Generator constrP,
Generator constrE 
)

This function creates new specification given by the type ("xxxxx") Note: The core of this function is a template specification model (SpecCB12.gen).

Based on this model are the specifications created, by simply adding corresponding states and transitions. Hence, for different models, this function can not be used directly, but can serve as an example.

Parameters
mTypeBy the type we specify the desired behaviour we want to model
rHioSpecHioPlant reference to the resulting specification (result)
constrPGenerator to the resulting operator constraint for the specification
constrEGenerator to the resulting environment constraint for the specification

Definition at line 1120 of file hio_module.cpp.

◆ CreateTempFile()

FAUDES_API std::string faudes::CreateTempFile ( void  )

Create a temp file, length 0.

Returns
Name of temp file

Definition at line 205 of file cfl_helper.cpp.

◆ CycleOfUnobsEvents() [1/2]

FAUDES_API bool faudes::CycleOfUnobsEvents ( const System rGen,
std::string &  rReport 
)

Test if there exist any cycles of unobservable events in a generator.

Parameters
rGenInput generator.
rReportUser-readable information of violating condition (in case of positive test result).
Returns
True if there exists a cycle of unobservable events.

◆ CycleOfUnobsEvents() [2/2]

bool faudes::CycleOfUnobsEvents ( const System rGen,
string &  rReport 
)

Definition at line 241 of file diag_eventdiagnosis.cpp.

◆ CycleStartStates()

FAUDES_API void faudes::CycleStartStates ( const System rGen,
StateSet rCycleOrigins 
)

Find all start/end states of cycles of unobservable events in a generator.

Parameters
rGenInput generator.
rCycleOriginsOutput variable for the states that have been found.

Definition at line 334 of file diag_eventdiagnosis.cpp.

◆ CycleStartStatesSearch()

FAUDES_API void faudes::CycleStartStatesSearch ( const System rGen,
StateSet rTodo,
Idx  currState,
StateSet  statesOnPath,
StateSet rCycleOriginStates 
)

Auxiliary function for CycleStartStates().

Parses through the active event set of the current state and checks whether any of the successor states already occurred on the path to current state (then a cycle is found).

Parameters
rGenInput generator.
rTodoStates that remain to be processed.
currStateThe current state.
statesOnPathStates that occurred on the path.
rCycleOriginStatesOutput variable for the states that have been found.

Definition at line 354 of file diag_eventdiagnosis.cpp.

◆ DecentralizedDiagnoser()

FAUDES_API bool faudes::DecentralizedDiagnoser ( const System rGen,
const Generator rSpec,
const EventSetVector rAlphabets,
GeneratorVector rDiags 
)

Function definition for run-time interface.

Definition at line 349 of file diag_decentralizeddiagnosis.cpp.

◆ DecentralizedModularDiagnoser()

FAUDES_API void faudes::DecentralizedModularDiagnoser ( const SystemVector rGens,
const Generator rSpec,
GeneratorVector rDiags 
)

Function definition for run-time interface.

Definition at line 367 of file diag_decentralizeddiagnosis.cpp.

◆ Deterministic() [1/2]

FAUDES_API void faudes::Deterministic ( const Generator rGen,
std::map< Idx, StateSet > &  rEntryStatesMap,
Generator rResGen 
)

Make generator deterministic.

Constructs a deterministic generator while preserving the generated and marked languages. See Deterministic(const Generator&,Generator& rResGen) for the intended api. This version provides as a second parameter the resulting map from new states to their respective original state set. It is used as a so called "entry state map" for deterministic projected generators.

Parameters
rGenReference to generator
rEntryStatesMapEntry state map
rResGenReference to resulting deterministic generator

Definition at line 96 of file cfl_determin.cpp.

◆ Deterministic() [2/2]

FAUDES_API void faudes::Deterministic ( const Generator rGen,
std::vector< StateSet > &  rPowerStates,
std::vector< Idx > &  rDetStates,
Generator rResGen 
)

Make generator deterministic.

Constructs a deterministic generator while preserving the generated and marked languages. See Deterministic(const Generator&,Generator& rResGen) for the intended api. This version provides as second and third parameters the correspondence between new states and the original state sets. in vectors

Parameters
rGenReference to generator
rPowerStatesVector that holds the power states
rDetStatesVector that holds the corresponding deterministic states
rResGenReference to resulting deterministic generator

Definition at line 113 of file cfl_determin.cpp.

◆ DirectoryExists()

FAUDES_API bool faudes::DirectoryExists ( const std::string &  rDirectory)

Test existence of directory.

Parameters
rDirectoryName of file to test
Returns
True <> can open directory for reading

Definition at line 320 of file cfl_helper.cpp.

◆ EnabledContinuationRule()

void faudes::EnabledContinuationRule ( Generator g,
const EventSet silent 
)

Definition at line 302 of file cfl_conflequiv.cpp.

◆ EventDiagnoser() [1/2]

void faudes::EventDiagnoser ( const System rOrigGen,
const map< string, EventSet > &  rFailureTypeMap,
Diagnoser rDiagGen 
)

Definition at line 816 of file diag_eventdiagnosis.cpp.

◆ EventDiagnoser() [2/2]

FAUDES_API void faudes::EventDiagnoser ( const System rOrigGen,
const std::map< std::string, EventSet > &  rFailureTypeMap,
Diagnoser rDiagGen 
)

Compute a standard diagnoser from an input generator and a failure partition.

Parameters
rOrigGenInput plant including failure events.
rFailureTypeMapFailure partition: maps failure type names to failure events.
rDiagGenDiagnoser generator for output.

◆ ExistsCycle() [1/2]

FAUDES_API bool faudes::ExistsCycle ( const System rGen,
std::string &  rReport 
)

Test if there exist any cycles in a generator.

Parameters
rGenInput generator.
rReportUser-readable information of violating condition (in case of positive test result).
Returns
True if there exists a cycle.

◆ ExistsCycle() [2/2]

bool faudes::ExistsCycle ( const System rGen,
string &  rReport 
)

Definition at line 283 of file diag_eventdiagnosis.cpp.

◆ ExistsCycleSearch() [1/2]

FAUDES_API bool faudes::ExistsCycleSearch ( const System rGen,
StateSet rTodo,
Idx  currState,
StateSet  statesOnPath,
std::string &  rReport 
)

Auxiliary function for ExistsCycle(const System&, std::string&).

Starting from a state currState, this function makes a depth-first-search through the generator rGen.

Parameters
rGenInput generator.
rTodoStates to process.
currStateCurrent state.
statesOnPathStates that occurred on the way to current state.
rReportUser-readable information of violating condition (in case of negative test result).
Returns
True if a cycle is found.

◆ ExistsCycleSearch() [2/2]

bool faudes::ExistsCycleSearch ( const System rGen,
StateSet rTodo,
Idx  currState,
StateSet  statesOnPath,
string &  rReport 
)

Definition at line 306 of file diag_eventdiagnosis.cpp.

◆ ExistsViolatingCyclesInGd() [1/2]

bool faudes::ExistsViolatingCyclesInGd ( System rGd,
const Diagnoser rGobs,
map< pair< Idx, Idx >, Idx > &  rReverseCompositionMap,
const string &  rFailureType,
string &  rReportString 
)

Definition at line 380 of file diag_eventdiagnosis.cpp.

◆ ExistsViolatingCyclesInGd() [2/2]

FAUDES_API bool faudes::ExistsViolatingCyclesInGd ( System rGd,
const Diagnoser rGobs,
std::map< std::pair< Idx, Idx >, Idx > &  rReverseCompositionMap,
const std::string &  rFailureType,
std::string &  rReportString 
)

Remove states with same failure labels from rGd and from rReverseCompositionMap and perform cycle detection.

Parameters
rGdInput diagnoser generator.
rGobsGenerator G_o to look up failure labels.
rReverseCompositionMapMapping of G_d states with G_o states.
rFailureTypeThe considered failure type.
rReportStringUser-readable information of violating condition (in case of negative test result).
Returns
True if violating cycles exist.

◆ ExitFunction()

void faudes::ExitFunction ( void  )

Definition at line 464 of file cfl_helper.cpp.

◆ ExpandString()

FAUDES_API std::string faudes::ExpandString ( const std::string &  rString,
unsigned int  len 
)

Fill string with spaces up to a given length if length of the string is smaller than given length parameter.

Parameters
rStringstring
lenMinimum number of charakters in string
Returns
Expanded string

Definition at line 80 of file cfl_helper.cpp.

◆ ExtendTransRel()

FAUDES_API void faudes::ExtendTransRel ( Generator rGen,
const EventSet rSilent,
const Idx rFlag 
)

ExtendTransRel perform transition saturation w.r.t. silent evs. Two different saturation modes are set depending on flag value.

Parameters
rGeninput gen
rSilentsilent event set (contains either 0 or 1 event)
rFlagflag for saturation mode – rFlag == 1: delayed transition (half-saturated); rFlag == 2: observed transition (full-saturated)

Definition at line 308 of file cfl_bisimcta.cpp.

◆ ExtractBasename()

FAUDES_API std::string faudes::ExtractBasename ( const std::string &  rFullName)

Extract file name from full path.

This version also removes the last suffix.

Parameters
rFullNameFull path of file eg "/home/friend/data/generator.gen"
Returns
Filename "generator"

Definition at line 280 of file cfl_helper.cpp.

◆ ExtractDirectory()

FAUDES_API std::string faudes::ExtractDirectory ( const std::string &  rFullPath)

Extract directory from full path.

Parameters
rFullPathFull name of file eg "/home/friend/data/generator.gen"
Returns
Directory eg "/home/friend/data"

Definition at line 262 of file cfl_helper.cpp.

◆ ExtractExtension()

FAUDES_API std::string faudes::ExtractExtension ( const std::string &  rFullName)

Extract file name from full path.

This version also remove the last suffix.

Parameters
rFullNameFull path of file eg "/home/friend/data/generator.gen"
Returns
Extension "gen"

Definition at line 294 of file cfl_helper.cpp.

◆ ExtractFilename()

FAUDES_API std::string faudes::ExtractFilename ( const std::string &  rFullName)

Extract file name from full path.

Parameters
rFullNameFull path of file eg "/home/friend/data/generator.gen"
Returns
Filename "generator.gen"

Definition at line 271 of file cfl_helper.cpp.

◆ FactorTauLoops()

FAUDES_API void faudes::FactorTauLoops ( Generator rGen,
const Idx rSilent 
)

FactorTauLoops merge silent loop and then remove silent self loops.

Parameters
rGeninput generator
rSilentsilent event

◆ FailuresUnobservable() [1/2]

FAUDES_API bool faudes::FailuresUnobservable ( const System rGen,
const AttributeFailureTypeMap rFailureTypeMap,
std::string &  rReport 
)

Check if all failure events are unobservable events in a generator's alphabet.

Parameters
rGenInput generator, is a model of the original plant containing the relevant failures events.
rFailureTypeMapFailure partition: maps failure type names to failure events and indicator events.
rReportUser-readable information of violating condition (in case of negative result).
Returns
True if all failures events are unobservable.

◆ FailuresUnobservable() [2/2]

bool faudes::FailuresUnobservable ( const System rGen,
const AttributeFailureTypeMap rFailureTypeMap,
string &  rReport 
)

Definition at line 265 of file diag_eventdiagnosis.cpp.

◆ faudes_complete()

</
FAUDES_API char ** faudes::faudes_complete ( lua_State *  pL,
const char *  text,
int  start,
int  end 
)