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	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	ConsoleOut
	Console Out. More...
class	ObjectCount
	Debugging counter. 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< AttributeCFlags >	Alphabet
	Convenience typedef for event sets with controllability attributes. More...
typedef TBaseVector< Alphabet >	AlphaberVector
	Convenience typedef. More...
typedef TaNameSet< AttributeCFlags >	cEventSet
	Compatibility: pre 2.20b used cEventSet as C++ class name. More...
typedef TBaseVector< cEventSet >	cEventSetVector
typedef TcGenerator< AttributeVoid, AttributeVoid, AttributeCFlags, AttributeVoid >	System
	Convenience typedef for std System. More...
typedef TBaseVector< System >	SystemVector
	Convenience typedef for vectors of systems. More...
typedef TcGenerator< AttributeVoid, AttributeVoid, AttributeCFlags, AttributeVoid >	cGenerator
	Compatibility: pre 2.20b used cGenerator as C++ class name. More...
typedef TBaseVector< cGenerator >	cGeneratorVector
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< Integer >	IntegerVector
typedef vGenerator	Generator
	Plain generator, api typedef for generator with no attributes. More...
typedef TBaseVector< Generator >	GeneratorVector
	Convenience typedef for vectors og generators. More...
typedef IndexSet	StateSet
typedef TBaseVector< IndexSet >	IndexSetVector
	Convenience typedef for vectors og generators. More...
template<class Attr >
using	TaStateSet = TaIndexSet< Attr >
	Convenience Macro (pre C++11) More...
typedef NameSet	EventSet
	Convenience typedef for plain event sets. More...
typedef TBaseVector< EventSet >	EventSetVector
typedef TNode< Idx, Idx >	Node
typedef TGraph< Idx, Idx >	Graph
typedef TTransSet< TransSort::X1EvX2 >	TransSet
	Type definition for default sorted TTransSet. More...
typedef TTransSet< TransSort::X1EvX2 >	TransSetX1EvX2
	Type definition for default sorted TTransSet. More...
typedef TTransSet< TransSort::EvX1X2 >	TransSetEvX1X2
	Type definition for ev, x1, x2 sorted TTransSet. More...
typedef TTransSet< TransSort::EvX2X1 >	TransSetEvX2X1
	Type definition for ev, x2, x1 sorted TTransSet. More...
typedef TTransSet< TransSort::X2EvX1 >	TransSetX2EvX1
	Type definition for x2, ev, x1 sorted TTransSet. More...
typedef TTransSet< TransSort::X2X1Ev >	TransSetX2X1Ev
	Type definition for x2, x1, ev sorted TTransSet. More...
typedef TTransSet< TransSort::X1X2Ev >	TransSetX1X2Ev
	Type definition for x1, x2, ev sorted TTransSet. More...
typedef TdiagGenerator< AttributeFailureTypeMap, AttributeDiagnoserState, AttributeCFlags, AttributeVoid >	Diagnoser
typedef TdiagGenerator< AttributeFailureTypeMap, AttributeDiagnoserState, AttributeCFlags, AttributeVoid >	diagGenerator
	Compatibility: pre 2.20b used diagGenerator as C++ class name. More...
typedef THioConstraint< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid >	HioConstraint
typedef THioController< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid >	HioController
typedef THioEnvironment< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid >	HioEnvironment
typedef THioPlant< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid >	HioPlant
typedef TaNameSet< AttributeIosEvent >	IosEventSet
typedef TaIndexSet< AttributeIosState >	IosStateSet
typedef TioGenerator< AttributeVoid, AttributeIosState, AttributeIosEvent, AttributeVoid >	IoSystem
typedef TmtcGenerator< AttributeVoid, AttributeColoredState, AttributeCFlags, AttributeVoid >	MtcSystem
typedef TmtcGenerator< AttributeVoid, AttributeColoredState, AttributeCFlags, AttributeVoid >	mtcGenerator
	Compatibility: pre 2.20b used mtcGenerator as C++ class name. More...
typedef TtGenerator< AttributeTimedGlobal, AttributeTimedState, AttributeCFlags, AttributeTimedTrans >	TimedGenerator
	Convenience typedef for std TimedGenerator. More...
typedef TtGenerator< AttributeTimedGlobal, AttributeTimedState, AttributeCFlags, AttributeTimedTrans >	tGenerator
	Compatibility: pre 2.20b used tGenerator as C++ class name. More...
typedef TaNameSet< SimEventAttribute >	sEventSet
	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, AttributeLhaTrans >	LinearHybridAutomaton
	Convenience typedef for std lhaGenerator. More...
typedef TaTransSet< AttributeLhaTrans >	LhaTransSet
typedef TaIndexSet< AttributeLhaState >	LhaStateSet

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, StateSet >	IncomingEquivalentClasses (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...
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...
Type *	NewFaudesObject (const std::string &rTypeName)
	Instantiate faudes typed objects by type name. More...
Function *	NewFaudesFunction (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...
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 globally 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...
std::string	ExtractDirectory (const std::string &rFullPath)
	Extract directory from (full) path; i.e., remove the last separator and anything thereafer. More...
std::string	ExtractFilename (const std::string &rFullName)
	Extract file name from full path. More...
std::string	ExtractBasename (const std::string &rFullName)
	Extract file basename from full path. More...
std::string	ExtractSuffix (const std::string &rFullName)
	Extract extension from full path, i.e. More...
std::string	PrependPath (const std::string &rLeft, const std::string &rRight)
	Prepend one path before another. 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...
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_userdata *	SwigUserData (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 >
TokenWriter *	gTestProtocolTw =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< mbDevice >	gRtiRegisterSpiDevice ("ModbusDevice")
AutoRegisterType< TaNameSet< AttributeSignalEvent > >	gRti1RegisterSignalDeviceEventSet ("SignalDeviceEventSet")
AutoRegisterXElementTag< TaNameSet< AttributeSignalEvent > >	gRti1XElementTagSignalDeviceEventSet ("SignalDeviceEventSet", "Event")
AutoRegisterType< nDevice >	gRtiRegisterSimplenetDevice ("SimplenetDevice")
static volatile AutoRegisterType< xDevice >	gRtiRegisterDeviceContainer ("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

typedef TBaseVector<Alphabet> faudes::AlphaberVector

Convenience typedef.

Definition at line 248 of file cfl_cgenerator.h.

cEventSet

typedef TaNameSet<AttributeCFlags> faudes::cEventSet

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

Definition at line 252 of file cfl_cgenerator.h.

cEventSetVector

typedef TBaseVector<cEventSet> faudes::cEventSetVector

Definition at line 253 of file cfl_cgenerator.h.

cGenerator

typedef TcGenerator<AttributeVoid, AttributeVoid, AttributeCFlags,AttributeVoid> faudes::cGenerator

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

Definition at line 931 of file cfl_cgenerator.h.

cGeneratorVector

typedef TBaseVector<cGenerator> faudes::cGeneratorVector

Definition at line 932 of file cfl_cgenerator.h.

diagGenerator

typedef TdiagGenerator<AttributeFailureTypeMap, AttributeDiagnoserState, AttributeCFlags, AttributeVoid> faudes::diagGenerator

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

Definition at line 202 of file diag_generator.h.

Diagnoser

typedef TdiagGenerator<AttributeFailureTypeMap, AttributeDiagnoserState, AttributeCFlags, AttributeVoid> faudes::Diagnoser

Definition at line 198 of file diag_generator.h.

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 189 of file cfl_attributes.h.

Graph

typedef TGraph<Idx,Idx> faudes::Graph

Definition at line 484 of file cfl_project.cpp.

HioConstraint

typedef THioConstraint<AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid> faudes::HioConstraint

Definition at line 522 of file hio_constraint.h.

HioController

typedef THioController<AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid> faudes::HioController

Definition at line 957 of file hio_controller.h.

HioEnvironment

typedef THioEnvironment<AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid> faudes::HioEnvironment

Definition at line 956 of file hio_environment.h.

HioPlant

typedef THioPlant<AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid> faudes::HioPlant

Definition at line 880 of file hio_plant.h.

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

typedef TBaseVector<Integer> faudes::IntegerVector

Definition at line 221 of file cfl_elementary.h.

IosEventSet

typedef TaNameSet<AttributeIosEvent> faudes::IosEventSet

Definition at line 227 of file ios_attributes.h.

IosStateSet

typedef TaIndexSet<AttributeIosState> faudes::IosStateSet

Definition at line 468 of file ios_attributes.h.

IoSystem

typedef TioGenerator<AttributeVoid,AttributeIosState, AttributeIosEvent, AttributeVoid> faudes::IoSystem

Definition at line 777 of file ios_system.h.

LhaStateSet

typedef TaIndexSet<AttributeLhaState> faudes::LhaStateSet

Definition at line 679 of file hyb_hgenerator.h.

LhaTransSet

typedef TaTransSet<AttributeLhaTrans> faudes::LhaTransSet

Definition at line 678 of file hyb_hgenerator.h.

LinearHybridAutomaton

typedef TlhaGenerator<AttributeLhaGlobal,AttributeLhaState,AttributeCFlags,AttributeLhaTrans> faudes::LinearHybridAutomaton

Convenience typedef for std lhaGenerator.

Definition at line 677 of file hyb_hgenerator.h.

mtcGenerator

typedef TmtcGenerator<AttributeVoid,AttributeColoredState,AttributeCFlags,AttributeVoid> faudes::mtcGenerator

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

Definition at line 753 of file mtc_generator.h.

MtcSystem

typedef TmtcGenerator<AttributeVoid,AttributeColoredState,AttributeCFlags,AttributeVoid> faudes::MtcSystem

Definition at line 748 of file mtc_generator.h.

Node

typedef TNode<Idx,Idx> faudes::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

typedef struct faudes::swig_cast_info faudes::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

typedef struct faudes::swig_type_info faudes::swig_type_info

tGenerator

typedef TtGenerator<AttributeTimedGlobal, AttributeTimedState, AttributeCFlags,AttributeTimedTrans> faudes::tGenerator

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

Definition at line 782 of file tp_tgenerator.h.

TimedGenerator

typedef TtGenerator<AttributeTimedGlobal, AttributeTimedState, AttributeCFlags,AttributeTimedTrans> faudes::TimedGenerator

Convenience typedef for std TimedGenerator.

Definition at line 777 of file tp_tgenerator.h.

Enumeration Type Documentation

VerifierStateLabel

enum faudes::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

rGen	A generator.
state	A 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

rGenVec	Vector of input generators
rResGen	Reference 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

rTransSetX2EvX1	reverse transition relation of the input generator
rControllableEvents	set of controllable events
rHighAlph	High level alphabet
exitState	start state for backward reachability
currentState	current state for backward reachability
controllablePath	false if at least one uncontrollable path to the currentState exists
rLocalStatesMap	map for states and their controllability property
rDoneStates	states 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

rLowGen	Input generator
rControllableEvents	set of controllable events
rHighAlph	High level alphabet
currentState	start 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents	Set of controllable events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapChangedTrans	Maps 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

rGen	Generator for which the dynamic system is computed
rHighAlph	Abstraction alphabet
rGenDyn	Generator 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

rGen	Generator for which the dynamic system is computed
rControllableEvents	Set of controllable events
rHighAlph	Abstraction alphabet
rGenDyn	Generator 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

rGen	Generator for which the dynamic system is computed
rHighAlph	Abstraction alphabet
rGenDyn	Generator 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

rGen	Generator for which the dynamic system is computed
rHighAlph	Abstraction alphabet
rGenDyn	Generator 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

rGen	Generator for which the dynamic system is computed
rHighAlph	Abstraction alphabet
rGenDyn	Generator 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

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rSplitAlphabet	Reference to the current alphabet for splitting verification
rNondeterministicStates	vector with states where nondeterminism has to be resolved and the related event
entryState	current 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

rString	string
len	Maximum number of charakters in string (approx)

Returns

Collapsed string

Definition at line 91 of file cfl_utils.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

rGen1	First MtcSystem for parallel composition
stdidx1	Index to first MtcSystem's current state
colors1	Color set of first MtcSystem
rGen2	Second MtcSystem for parallel composition
stdidx2	Index to second MtcSystem's current state
colors2	Color set of second MtcSystem
composedSet	Color 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

rPlantGenVec	Plant components (must be deterministic)
rConAlph	Overall set of controllable events
rSpecGenVec	Specification components (must be deterministic)
rMapEventsToPlant	Resulting event map
rDisGenVec	Resulting distinuisher automata
rSupGenVec	Resulting 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

rGen	input gen
rSilent	silent event set (contains either 0 or 1 event)
rResult	state partition without trivial classes
rFlag	rFlag == 1: dalayed bisimulation; rFlag == 2: weak bisimulation
rPrePartition	prepartition (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

rGen	input gen
rSilent	silent event set (contains either 0 or 1 event)
rResult	state 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

rGen	input gen
rResult	state 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

rGen	input gen
rResult	state partition without trivial classes
rPrePartition	prepartition (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

rGen	input gen
rSilent	silent event set (contains either 0 or 1 event)
rResult	state partition without trivial classes
rPrePartition	prepartition (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

rGen	input gen
rSilent	silent event set (contains either 0 or 1 event)
rResult	state partition without trivial classes
rPrePartition	prepartition (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

rGen	input gen
rSilent	silent event set (contains either 0 or 1 event)
rResult	state 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

rGobs	Input diagnoser G_o.
rReverseCompositionMap	Output variable containing the mapping of G_o states and G_d states (generated by Parallel()).
rGd	Output 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

rGenMarkedNonSpecBehaviour	Input generator that specifies specification violations by marked states.
rGobs	Output 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

rOrigGen	Input generator, which is a model of the original plant containing the relevant failures events.
rAttrFTMap	Failure partition.
rGobs	Output 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

rOrigGen	Input generator, which is a model of the original plant containing the relevant failures events.
rFailureType	Failure type name.
rFailureEvents	Failure events belonging to the failure type.
rGobs	Output 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

rOrigGen	the resulting composed new generator from synthesis-buffer
rConAlph	controllable events
rLocAlph	local events
rHSupGen	the 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

rGen	Input generator.
rUnobsEvents	Unobservable events in the generators alphabet.
rFailures	Unobservable failure events in the generators alphabet.
State	A state of the generators state set.
rAttrFTMap	Failure partition.
rReachabilityMap	Output 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

rGen	Input generator.
rUnobsEvents	Unobservable events in the generators alphabet.
State	A state of the generators state set.
rReachabilityMap	Output 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

rGen	Input generator.
rUnobsEvents	Unobservable events in the generators alphabet.
rFailures	Unobservable failure events in the generators alphabet.
State	The current state within the trace.
rAttrFTMap	Failure partition.
rReachabilityMap	Output 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.
FToccurred	Collects 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

rGen	Input generator.
rUnobsEvents	Unobservable events in the generators alphabet.
State	The current state within the trace.
done	Progress.
rReachabilityMap	Output 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

rGen	input gen
rSilent	silent event set (contains either 0 or 1 event)
rResult	state 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

rGen	input gen
rSilent	silent event set (contains either 0 or 1 event)
rResult	state partition without trivial classes
rPrePartition	prepartition (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

rGen	input gen
rSilent	silent event set (contains either 0 or 1 event)
rResult	state 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

rGenOrig	original generator
rConAlph	controllable events
rLocAlph	local events
rMapStateToPartition	map state to equivalent class
rResGen	the 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

rGen	generator 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_utils.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

rPlantGen	Plant generator
rCAlph	Controllable events
rOAlph	Observable events
rSpecGen	Specification 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

rPlantGen	Plant generator
rCAlph	Controllable events
rSpecGen	Specification 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

rPlantGenVec	Plant components (must be deterministic)
rConAlph	Overall set of controllable events
rSpecGenVec	Specification 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

rReverseCompositionMap	Input map as generated by Parallel().
rCompositionMap	Converted map.

cParallel() [1/3]

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

Parallel composition of multiple generators.

Parameters

rGens	STL-vector of generators.
rResGen	Output 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

rGens	STL-vector of generators.
rResGen	Output 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

mType	By the type we specify type of the specification to build constraint for
constrP	Generator to the resulting operator constraint for the specification
constrE	Generator 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

mType	By the type we specify the desired behaviour we want to model
rHioSpec	HioPlant reference to the resulting specification (result)
constrP	Generator to the resulting operator constraint for the specification
constrE	Generator 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_utils.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

rGen	Input generator.
rReport	User-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

rGen	Input generator.
rCycleOrigins	Output 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

rGen	Input generator.
rTodo	States that remain to be processed.
currState	The current state.
statesOnPath	States that occurred on the path.
rCycleOriginStates	Output 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

rGen	Reference to generator
rEntryStatesMap	Entry state map
rResGen	Reference 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

rGen	Reference to generator
rPowerStates	Vector that holds the power states
rDetStates	Vector that holds the corresponding deterministic states
rResGen	Reference 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

rDirectory

Name of file to test

Returns

True <> can open directory for reading

Definition at line 332 of file cfl_utils.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

rOrigGen	Input plant including failure events.
rFailureTypeMap	Failure partition: maps failure type names to failure events.
rDiagGen	Diagnoser 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

rGen	Input generator.
rReport	User-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

rGen	Input generator.
rTodo	States to process.
currState	Current state.
statesOnPath	States that occurred on the way to current state.
rReport	User-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

rGd	Input diagnoser generator.
rGobs	Generator G_o to look up failure labels.
rReverseCompositionMap	Mapping of G_d states with G_o states.
rFailureType	The considered failure type.
rReportString	User-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 476 of file cfl_utils.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

rString	string
len	Minimum number of charakters in string

Returns

Expanded string

Definition at line 80 of file cfl_utils.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

rGen	input gen
rSilent	silent event set (contains either 0 or 1 event)
rFlag	flag 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 basename from full path.

This version also removes the last suffix.

Parameters

rFullName

Full path of file eg "/home/friend/data/generator.gen"

Returns

Filename "generator"

Definition at line 274 of file cfl_utils.cpp.

ExtractDirectory()

FAUDES_API std::string faudes::ExtractDirectory

(

const std::string &

rFullPath

)

Extract directory from (full) path; i.e., remove the last separator and anything thereafer.

Parameters

rFullPath

Full name of file eg (1) "/home/friend/data/generator.gen" Full name of file eg (2) "C:\data\project\generator.gen"

Returns

Directory eg (1) "/home/friend/data" Directory eg (2) "C:\data\project"

Definition at line 256 of file cfl_utils.cpp.

ExtractFilename()

FAUDES_API std::string faudes::ExtractFilename

(

const std::string &

rFullName

)

Extract file name from full path.

Parameters

rFullName

Full path of file eg "/home/friend/data/generator.gen"

Returns

Filename "generator.gen"

Definition at line 265 of file cfl_utils.cpp.

ExtractSuffix()

FAUDES_API std::string faudes::ExtractSuffix

(

const std::string &

rFullName

)

Extract extension from full path, i.e.

ontain the last suffix.

Parameters

rFullName

Full path of file eg "/home/friend/data/generator.gen"

Returns

Extension "gen"

Definition at line 288 of file cfl_utils.cpp.

FactorTauLoops()

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

FactorTauLoops merge silent loop and then remove silent self loops.

Parameters

rGen	input generator
rSilent	silent 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

rGen	Input generator, is a model of the original plant containing the relevant failures events.
rFailureTypeMap	Failure partition: maps failure type names to failure events and indicator events.
rReport	User-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
	)

Definition at line 156 of file lbp_addons.cpp.

faudes_console()

FAUDES_API void faudes::faudes_console

(

const std::string &

message

)

faudes_debug()

FAUDES_API void faudes::faudes_debug

(

const std::string &

message

)

faudes_dict_insert_entry()

FAUDES_API void faudes::faudes_dict_insert_entry	(	const std::string &	topic,
		const std::string &	key,
		const std::string &	entry
	)

faudes_dict_insert_topic()

FAUDES_API void faudes::faudes_dict_insert_topic	(	const std::string &	topic,
		const std::string &	text
	)

faudes_hook()

void faudes::faudes_hook	(	lua_State *	L,
		lua_Debug *	ar
	)

Definition at line 93 of file lbp_addons.cpp.

faudes_hook_register()

FAUDES_API void faudes::faudes_hook_register

(

lua_State *

L

)

Definition at line 109 of file lbp_addons.cpp.

faudes_initialize()

FAUDES_API void faudes::faudes_initialize

(

lua_State *

pL

)

Definition at line 128 of file lbp_addons.cpp.

faudes_loaddefext()

int FAUDES_API faudes::faudes_loaddefext	(	lua_State *	pL,
		const char *	arg0
	)

Definition at line 144 of file lbp_addons.cpp.

faudes_loadext()

int FAUDES_API faudes::faudes_loadext	(	lua_State *	pL,
		const char *	filename
	)

Definition at line 133 of file lbp_addons.cpp.

faudes_mute()

FAUDES_API void faudes::faudes_mute

(

bool

on

)

faudes_print()

int faudes::faudes_print

(

lua_State *

L

)

Definition at line 49 of file lbp_addons.cpp.

faudes_print_register()

FAUDES_API void faudes::faudes_print_register

(

lua_State *

L

)

Definition at line 86 of file lbp_addons.cpp.

faudes_throw_exception()

FAUDES_API void faudes::faudes_throw_exception

(

const std::string &

msg

)

FaudesFunctionName()

const std::string& faudes::FaudesFunctionName

(

const Function &

rObject

)

Definition at line 704 of file cfl_registry.cpp.

FileCopy()

FAUDES_API bool faudes::FileCopy	(	const std::string &	rFromFile,
		const std::string &	rToFile
	)

Copy file.

Parameters

rFromFile	Name of source file
rToFile	Name of dest file

Returns

True <> operation ok

Definition at line 397 of file cfl_utils.cpp.

FileDelete()

FAUDES_API bool faudes::FileDelete

(

const std::string &

rFilename

)

Delete file.

Parameters

rFilename

Name of file to delete

Returns

True <> could delete the file

Definition at line 392 of file cfl_utils.cpp.

FileExists()

FAUDES_API bool faudes::FileExists

(

const std::string &

rFilename

)

Test existence of file.

Parameters

rFilename

Name of file to test

Returns

True <> can open file for reading

Definition at line 385 of file cfl_utils.cpp.

GlobalSelfloop()

void faudes::GlobalSelfloop

(

GeneratorVector &

rGenVec

)

remove the events from the entire buffer which have only selfloop transitions

Parameters

rGenVec

synthesis-buffer

Definition at line 673 of file syn_compsyn.cpp.

GroupHioModules()

void faudes::GroupHioModules	(	const std::vector< HioModule * > &	rChildren,
		HioModule &	rParentModule
	)

GroupHioModules: This function groups two or more HioModules to a new HioModule.

The new HioModule represents the uncontrolled behaviour of the composed HioModules.

Parameters

rChildren	vector of HioModules to group
rParentModule	resulting HioModule

Definition at line 1093 of file hio_module.cpp.

H_tocollect()

void faudes::H_tocollect	(	StateSet &	rBlockingstates,
		const TransSetX2EvX1 &	rRtrel,
		const EventSet &	rLouc,
		const EventSet &	rShuc,
		TransSetX2EvX1 &	rToredirect
	)

Definition at line 1184 of file syn_compsyn.cpp.

HidePriviateEvs()

EventSet faudes::HidePriviateEvs	(	Generator &	rGen,
		EventSet &	silent
	)

Definition at line 531 of file cfl_conflequiv.cpp.

HioShuffle_Musunoi()

void faudes::HioShuffle_Musunoi	(	const HioPlant &	rPlantA,
		const HioPlant &	rPlantB,
		int	depth,
		Generator &	rIOShuffAB
	)

Definition at line 2736 of file hio_functions.cpp.

HioStatePartition() [1/4]

FAUDES_API void faudes::HioStatePartition

(

HioConstraint &

rConstraint

)

Function definition for run-time interface.

Parameters

rConstraint

HioConstraint

Definition at line 374 of file hio_constraint.cpp.

HioStatePartition() [2/4]

FAUDES_API void faudes::HioStatePartition

(

HioController &

rController

)

Function definition for run-time interface.

Parameters

rController

HioController

Definition at line 502 of file hio_controller.cpp.

HioStatePartition() [3/4]

FAUDES_API void faudes::HioStatePartition

(

HioEnvironment &

rEnvironment

)

Function definition for run-time interface.

Parameters

rEnvironment

HioEnvironment

Definition at line 505 of file hio_environment.cpp.

HioStatePartition() [4/4]

FAUDES_API void faudes::HioStatePartition

(

HioPlant &

rPlant

)

Function definition for run-time interface.

Parameters

rPlant

HioPlant

Definition at line 445 of file hio_plant.cpp.

HioSynth_Musunoi()

void faudes::HioSynth_Musunoi	(	const Generator &	rPlant,
		const HioPlant &	rSpec,
		const Generator &	rConstr,
		const Generator &	rLocConstr,
		const EventSet &	rYp,
		const EventSet &	rUp,
		Generator &	rController
	)

Definition at line 2875 of file hio_functions.cpp.

IncomingEquivalentClasses()

std::map<SetX1Ev,StateSet> faudes::IncomingEquivalentClasses	(	const Generator &	rGen,
		const EventSet &	silent
	)

Definition at line 222 of file cfl_conflequiv.cpp.

IncomingTransSet()

void faudes::IncomingTransSet	(	const Generator &	rGen,
		const TransSetX2EvX1 &	rRTrans,
		const EventSet &	silent,
		const Idx &	state,
		SetX1Ev &	result
	)

Definition at line 152 of file cfl_conflequiv.cpp.

insertRelabeledEvents() [1/10]

FAUDES_API void faudes::insertRelabeledEvents	(	Generator &	rGenPlant,
		const EventRelabelMap &	rMapRelabeledEvents
	)

Rti convenience wrapper.

Definition at line 1934 of file op_observercomputation.cpp.

insertRelabeledEvents() [2/10]

FAUDES_API void faudes::insertRelabeledEvents	(	Generator &	rGenPlant,
		const EventRelabelMap &	rMapRelabeledEvents,
		EventSet &	rNewEvents
	)

Rti convenience wrapper.

Definition at line 1927 of file op_observercomputation.cpp.

insertRelabeledEvents() [3/10]

void faudes::insertRelabeledEvents	(	Generator &	rGenPlant,
		const std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents
	)

Convenience function for relabeling events in a given generator.

See insertRelabeledEvents(Generator&, const std::map<Idx, std::set<Idx> >&, EventSet&)

There are no restrictions on parameters.

Parameters

rGenPlant	Plant component automaton
rMapRelabeledEvents	maps the original events to sets of newly introduced events

Definition at line 1903 of file op_observercomputation.cpp.

insertRelabeledEvents() [4/10]

void faudes::insertRelabeledEvents	(	Generator &	rGenPlant,
		const std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents,
		EventSet &	rNewEvents
	)

Convenience function for relabeling events in a given generator.

This function inserts new events and respective transitions given by a relableing map into a given generator.

Technical note: Recording of new events includes attributes, provided that the third parameter has a compatible attribute type.

There are no restrictions on parameters.

Parameters

rGenPlant	Plant component automaton
rMapRelabeledEvents	Maps the original events to sets of newly introduced events
rNewEvents	Returns the newly inserted events (accumulative, call clear before)

Definition at line 1871 of file op_observercomputation.cpp.

insertRelabeledEvents() [5/10]

void faudes::insertRelabeledEvents	(	Generator &	rGenPlant,
		const std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents
	)

Convenience function for relabeling events in a given generator.

See insertRelabeledEvents(Generator&, const std::map<Idx, std::set<Idx> >&, EventSet&)

There are no restrictions on parameters.

Parameters

rGenPlant	Plant component automaton
rMapRelabeledEvents	maps the original events to sets of newly introduced events

Definition at line 1903 of file op_observercomputation.cpp.

insertRelabeledEvents() [6/10]

FAUDES_API void faudes::insertRelabeledEvents	(	Generator &	rGenPlant,
		const std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents,
		EventSet &	rNewEvents
	)

Convenience function for relabeling events in a given generator.

This function inserts new events and respective transitions given by a relableing map into a given generator.

Technical note: Recording of new events includes attributes, provided that the third parameter has a compatible attribute type.

There are no restrictions on parameters.

Parameters

rGenPlant	Plant component automaton
rMapRelabeledEvents	Maps the original events to sets of newly introduced events
rNewEvents	Returns the newly inserted events (accumulative, call clear before)

Definition at line 1871 of file op_observercomputation.cpp.

insertRelabeledEvents() [7/10]

void faudes::insertRelabeledEvents	(	System &	rGenPlant,
		const std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents
	)

Convenience function for relabeling events in a given generator.

See insertRelabeledEvents(System&, const std::map<Idx, std::set<Idx> >&, Alphabet&)

There are no restrictions on parameters.

Parameters

rGenPlant	Plant component automaton
rMapRelabeledEvents	maps the original events to sets of newly introduced events

Definition at line 1897 of file op_observercomputation.cpp.

insertRelabeledEvents() [8/10]

void faudes::insertRelabeledEvents	(	System &	rGenPlant,
		const std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents,
		Alphabet &	rNewEvents
	)

Convenience function for relabeling events in a given generator.

This function inserts new events and respective transitions given by a relableing map into a given generator. The function is used to adjust plant components to the relableing from another plant component.

Technical note: This version records newly inserted events incl. their respective controllability attribute in the third parameter. T

There are no restrictions on parameters.

Parameters

rGenPlant	Plant component automaton
rMapRelabeledEvents	Maps the original events to sets of newly introduced events
rNewEvents	Returns the newly inserted events (accumulative, call clear before)

Definition at line 1848 of file op_observercomputation.cpp.

insertRelabeledEvents() [9/10]

FAUDES_API void faudes::insertRelabeledEvents	(	System &	rGenPlant,
		const std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents
	)

Convenience function for relabeling events in a given generator.

See insertRelabeledEvents(System&, const std::map<Idx, std::set<Idx> >&, Alphabet&)

There are no restrictions on parameters.

Parameters

rGenPlant	Plant component automaton
rMapRelabeledEvents	maps the original events to sets of newly introduced events

Definition at line 1897 of file op_observercomputation.cpp.

insertRelabeledEvents() [10/10]

FAUDES_API void faudes::insertRelabeledEvents	(	System &	rGenPlant,
		const std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents,
		Alphabet &	rNewEvents
	)

Convenience function for relabeling events in a given generator.

This function inserts new events and respective transitions given by a relableing map into a given generator. The function is used to adjust plant components to the relableing from another plant component.

Technical note: This version records newly inserted events incl. their respective controllability attribute in the third parameter. T

There are no restrictions on parameters.

Parameters

rGenPlant	Plant component automaton
rMapRelabeledEvents	Maps the original events to sets of newly introduced events
rNewEvents	Returns the newly inserted events (accumulative, call clear before)

Definition at line 1848 of file op_observercomputation.cpp.

InstallSelfloops()

FAUDES_API void faudes::InstallSelfloops	(	Generator &	rGen,
		const EventSet &	rEvs
	)

InstallSelfloops install selfloops on all states of given event set. intended to install silent event selfloops for saturation.

Parameters

rGen	input gen
rEvs	events which will be installed as selfloops

Definition at line 357 of file cfl_bisimcta.cpp.

IntegerSum() [1/2]

FAUDES_API long int faudes::IntegerSum	(	const Integer &	arg1,
		const Integer &	arg2
	)

Definition at line 102 of file cfl_elementary.cpp.

IntegerSum() [2/2]

FAUDES_API long int faudes::IntegerSum

(

const IntegerVector &

intvect

)

Definition at line 107 of file cfl_elementary.cpp.

IoStatePartition()

FAUDES_API void faudes::IoStatePartition

(

IoSystem &

rIoSystem

)

Construct io state partition.

This is an rti wrapper for bool IsIoSystem(IoSystem&).

Parameters

rIoSystem

Generator to test.

Definition at line 133 of file ios_algorithms.cpp.

IoSynthesis()

FAUDES_API void faudes::IoSynthesis	(	const IoSystem &	rPlant,
		const Generator &	rSpec,
		IoSystem &	rSup
	)

IO system synthesis.

This method esentially is a wrapper for SupConComplete(), which implements a synthesis procedure to compute the supremal controllable and complete sublanguage for a given plant and specification. Input events are regarded controllable. marking is ignored, i.e., synthesis refers to the generated langugaes rather than the the marked languages. For a version thet refers to Buchi acceptance condition, see IoSynthesisNB(const IoSystem&, const Generator&, IoSystem&).

The resulting supervisor is an IO System with the plant input events as outputs and vice versa.

Note that this routine does not test whether the plant has a locally free input U, nor does it ensure that the resulting supervisor has a free input Y.

Parameters

rPlant	IO-System - plant model
rSpec	Generator - specification
rSup	IO-System - supervisor

Exceptions

Exception

Any exceptions passed on from SupConComplete

Definition at line 420 of file ios_algorithms.cpp.

IoSynthesisNB()

FAUDES_API void faudes::IoSynthesisNB	(	const IoSystem &	rPlant,
		const Generator &	rSpec,
		IoSystem &	rSup
	)

IO system synthesis.

This method esentially is a wrapper for SupConOmegaNB(), which implements a synthesis procedure to compute the supremal omega-controllable. sublanguage for a given plant and specification. Input events are regarded controllable. In contrast to IoSynthesis(const IoSystem&, const Generator&, IoSystem&), this procedure refers to the Bucji acceptance condition and ensures a omega-nonblocking closed-loop behaviour.

The resulting supervisor is an IO System with the plant input events as outputs and vice versa.

Note that this routine does not test whether the plant has a locally free input U, nor does it ensure that the resulting supervisor has a free input Y.

Parameters

rPlant	IO-System - plant model
rSpec	Generator - specification
rSup	IO-System - supervisor

Exceptions

Exception

Any exceptions passed on from SupConOmegaNB

Definition at line 406 of file ios_algorithms.cpp.

IsCD()

FAUDES_API bool faudes::IsCD	(	const Generator &	gen,
		const EventSetVector &	ee,
		const EventSet &	ek,
		const EventSet &	unionset,
		Generator &	proof
	)

Definition at line 93 of file con_decomposability.cpp.

IsCoDiagnosable() [1/2]

FAUDES_API bool faudes::IsCoDiagnosable	(	const System &	rGen,
		const Generator &	rSpec,
		const EventSetVector &	rAlphabets
	)

Function definition for run-time interface.

Definition at line 337 of file diag_decentralizeddiagnosis.cpp.

IsCoDiagnosable() [2/2]

bool faudes::IsCoDiagnosable	(	const System &	rGen,
		const Generator &	rSpec,
		const vector< const EventSet * > &	rAlphabets,
		std::string &	rReportString
	)

Definition at line 24 of file diag_decentralizeddiagnosis.cpp.

IsComplete()

bool faudes::IsComplete	(	const vGenerator &	rGen,
		const StateSet &	rStateSet
	)

Definition at line 3904 of file cfl_generator.cpp.

IsControllableUnchecked()

FAUDES_API bool faudes::IsControllableUnchecked	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSpecGen,
		StateSet &	rCriticalStates
	)

Controllability (internal function)

Checks if language of specification h is controllable with respect to language of generator g. Only for deterministic plant + spec. Controllable event set has to be given as parameter.

This internal function performs no consistency test of the given parameter.

Parameters

rPlantGen	Plant generator
rCAlph	Controllable events
rSpecGen	Specification generator
rCriticalStates	Set of critical states

Exceptions

Exception

alphabets of generators don't match (id 100) plant generator nondeterministic (id 201) specification generator nondeterministic (id 203) plant & spec generator nondeterministic (id 204)

Returns

true / false

Definition at line 243 of file syn_supcon.cpp.

IsEventDiagnosable() [1/2]

FAUDES_API bool faudes::IsEventDiagnosable	(	const System &	rGen,
		const AttributeFailureTypeMap &	rFailureTypeMap
	)

Function definition for run-time interface.

Definition at line 78 of file diag_eventdiagnosis.cpp.

IsEventDiagnosable() [2/2]

bool faudes::IsEventDiagnosable	(	const System &	rGen,
		const AttributeFailureTypeMap &	rFailureTypeMap,
		string &	rReportString
	)

Definition at line 13 of file diag_eventdiagnosis.cpp.

isExtendedEk()

FAUDES_API bool faudes::isExtendedEk	(	const Generator &	tildeGen,
		const Generator &	rGen,
		EventSet &	ek
	)

! Remembers the last symbol from E-Ek that has been read.

Definition at line 138 of file con_decomposability_extension.cpp.

IsHioConstraintForm() [1/3]

FAUDES_API bool faudes::IsHioConstraintForm

(

HioConstraint &

rHioConstraint

)

IsHioConstraintForm: check if rHioConstraint is in I/O-constraint form and assign state attributes.

This function tests if rHioConstraint meets the I/O-constraint form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioConstraint formally describe an I/O constraint. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QY flag is assigned to a state if its active eventset is a subset of the Y-Alphabet. The assignment of HioStateFlags is complete only if IsHioConstraintForm() returns true. Method: all conditions of the formal I/O-constraint form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioConstraint

HioConstraint to check, HioStateFlags are set

Returns

true if rHioConstraint is in I/O-constraint form

Definition at line 362 of file hio_constraint.cpp.

IsHioConstraintForm() [2/3]

bool faudes::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.

This function tests if rHioConstraint meets the I/O-constraint form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioConstraint formally describe an I/O constraint. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QY flag is assigned to a state if its active eventset is a subset of the Y-Alphabet. The assignment of HioStateFlags is complete only if IsHioConstraintForm() returns true. Method: all conditions in the formal I/O-constraint form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioConstraint	HioConstraint to check, HioStateFlags are set
rQY	State set containing all QY states
rQU	State set containing all QU states
rErrEvSet	Event set for possible 'bad' events
rErrTrSet	Event set for possible 'bad' transition relations
rErrStSet	Event set for possible 'bad' states
rReportStr	Information about test results

Returns

true if rHioConstraint is in I/O-constraint form

Definition at line 16 of file hio_constraint.cpp.

IsHioConstraintForm() [3/3]

FAUDES_API bool faudes::IsHioConstraintForm	(	HioConstraint &	rHioConstraint,
		std::string &	rReportStr
	)

IsHioConstraintForm: check if rHioConstraint is in I/O-constraint form and assign state attributes.

This function tests if rHioConstraint meets the I/O-constraint form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioConstraint formally describe an I/O constraint. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QY flag is assigned to a state if its active eventset is a subset of the Y-Alphabet. The assignment of HioStateFlags is complete only if IsHioConstraintForm() returns true. Method: all conditions in the formal I/O-constraint form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioConstraint	HioConstraint to check, HioStateFlags are set
rReportStr	Information about test results

Returns

true if rHioConstraint is in I/O-constraint form

Definition at line 352 of file hio_constraint.cpp.

IsHioControllerForm() [1/3]

FAUDES_API bool faudes::IsHioControllerForm

(

HioController &

rHioController

)

IsHioControllerForm: check if rHioController is in I/O-controller form and assign state attributes.

This function tests if rHioController meets the I/O-controller form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioController formally describe an I/O controller. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QYcUp flag is assigned to a state if its active eventset is a subset of the union of the YC- and the UP-Alphabet. The assignment of HioStateFlags is complete only if IsHioControllerForm() returns true. Method: all conditions of the formal I/O-controller form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioController

HioController to check, HioStateFlags are set

Returns

true if rHioController is in I/O-controller form

Definition at line 490 of file hio_controller.cpp.

IsHioControllerForm() [2/3]

bool faudes::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.

This function tests if rHioController meets the I/O-controller form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioController formally describe an I/O controller. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QYcUp flag is assigned to a state if its active eventset is a subset of the union of the YC- and the UP-Alphabet. The assignment of HioStateFlags is complete only if IsHioControllerForm() returns true. Method: all conditions in the formal I/O-controller form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioController	HioController to check, HioStateFlags are set
rQUc	State set containing all QUc states
rQYP	State set containing all QYP states
rQUp	State set containing all QUp states
rQYcUp	State set containing all QYcUp states
rErrEvSet	Event set for possible 'bad' events
rErrTrSet	Event set for possible 'bad' transition relations
rErrStSet	Event set for possible 'bad' states
rReportStr	Information about test results

Returns

true if rHioController is in I/O-controller form

Definition at line 16 of file hio_controller.cpp.

IsHioControllerForm() [3/3]

FAUDES_API bool faudes::IsHioControllerForm	(	HioController &	rHioController,
		std::string &	rReportStr
	)

IsHioControllerForm: check if rHioController is in I/O-controller form and assign state attributes.

This function tests if rHioController meets the I/O-controller form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioController formally describe an I/O controller. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QYcUp flag is assigned to a state if its active eventset is a subset of the union of the YC- and the UP-Alphabet. The assignment of HioStateFlags is complete only if IsHioControllerForm() returns true. Method: all conditions in the formal I/O-controller form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioController	HioController to check, HioStateFlags are set
rReportStr	Information about test results

Returns

true if rHioController is in I/O-controller form

Definition at line 480 of file hio_controller.cpp.

IsHioEnvironmentForm() [1/3]

FAUDES_API bool faudes::IsHioEnvironmentForm

(

HioEnvironment &

rHioEnvironment

)

IsHioEnvironmentForm: check if rHioEnvironment is in I/O-environment form and assign state attributes.

This function tests if rHioEnvironment meets the I/O-environment form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioEnvironment formally describe an I/O environment. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QYlUe flag is assigned to a state if its active eventset is a subset of the union of the YL- and the UE-Alphabet. The assignment of HioStateFlags is complete only if IsHioEnvironmentForm() returns true. Method: all conditions of the formal I/O-environment form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioEnvironment

HioEnvironment to check, HioStateFlags are set

Returns

true if rHioEnvironment is in I/O-environment form

Definition at line 493 of file hio_environment.cpp.

IsHioEnvironmentForm() [2/3]

bool faudes::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.

This function tests if rHioEnvironment meets the I/O-environment form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioEnvironment formally describe an I/O environment. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QYlUe flag is assigned to a state if its active eventset is a subset of the union of the YL- and the UE-Alphabet. The assignment of HioStateFlags is complete only if IsHioEnvironmentForm() returns true. Method: all conditions in the formal I/O-environment form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioEnvironment	HioEnvironment to check, HioStateFlags are set
rQYe	State set containing all QYe states
rQUe	State set containing all QUe states
rQUl	State set containing all QUl states
rQYlUe	State set containing all QYlUe states
rErrEvSet	Event set for possible 'bad' events
rErrTrSet	Event set for possible 'bad' transition relations
rErrStSet	Event set for possible 'bad' states
rReportStr	Information about test results

Returns

true if rHioEnvironment is in I/O-environment form

Definition at line 16 of file hio_environment.cpp.

IsHioEnvironmentForm() [3/3]

FAUDES_API bool faudes::IsHioEnvironmentForm	(	HioEnvironment &	rHioEnvironment,
		std::string &	rReportStr
	)

IsHioEnvironmentForm: check if rHioEnvironment is in I/O-environment form and assign state attributes.

This function tests if rHioEnvironment meets the I/O-environment form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioEnvironment formally describe an I/O environment. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QYlUe flag is assigned to a state if its active eventset is a subset of the union of the YL- and the UE-Alphabet. The assignment of HioStateFlags is complete only if IsHioEnvironmentForm() returns true. Method: all conditions in the formal I/O-environment form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioEnvironment	HioEnvironment to check, HioStateFlags are set
rReportStr	Information about test results

Returns

true if rHioEnvironment is in I/O-environment form

Definition at line 482 of file hio_environment.cpp.

IsHioPlantForm() [1/3]

FAUDES_API bool faudes::IsHioPlantForm

(

HioPlant &

rHioPlant

)

IsHioPlantForm: check if rHioPlant is in I/O-plant form and assign state attributes.

Function definition for run-time interface.

This function tests if rHioPlant meets the I/O-plant form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioPlant formally describe an I/O plant. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QYpYe flag is assigned to a state if its active eventset is a subset of the union of the YP- and the YE-Alphabet. The assignment of HioStateFlags is complete only if IsHioPlantForm() returns true. Method: all conditions of the formal I/O-plant form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioPlant

HioPlant to check, HioStateFlags are set

Returns

true if rHioPlant is in I/O-plant form

Definition at line 433 of file hio_plant.cpp.

IsHioPlantForm() [2/3]

bool faudes::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.

Function definition for run-time interface.

This function tests if rHioPlant meets the I/O-plant form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioPlant formally describe an I/O plant. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QYpYe flag is assigned to a state if its active even set is a subset of the union of the YP- and the YE-Alphabet. The assignment of HioStateFlags is complete only if IsHioPlantForm() returns true. Method: all conditions in the formal I/O-plant form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioPlant	HioPlant to check, HioStateFlags are set
rQYpYe	State set containing all QYpYe states
rQUp	State set containing all QUp states
rQUe	State set containing all QUe states
rErrEvSet	Event set for possible 'bad' events
rErrTrSet	Event set for possible 'bad' transition relations
rErrStSet	Event set for possible 'bad' states
rReportStr	Information about test results

Returns

true if rHioPlant is in I/O-plant form

Definition at line 16 of file hio_plant.cpp.

IsHioPlantForm() [3/3]

FAUDES_API bool faudes::IsHioPlantForm	(	HioPlant &	rHioPlant,
		std::string &	rReportStr
	)

IsHioPlantForm: check if rHioPlant is in I/O-plant form and assign state attributes.

Function definition for run-time interface.

This function tests if rHioPlant meets the I/O-plant form that has been formally defined by S.Perk. If so, then the alphabet of and the language marked by rHioPlant formally describe an I/O plant. During the test, the HioStateFlags are set according to the active event set or the respective state, for example: The QYpYe flag is assigned to a state if its active even set is a subset of the union of the YP- and the YE-Alphabet. The assignment of HioStateFlags is complete only if IsHioPlantForm() returns true. Method: all conditions in the formal I/O-plant form definition are checked individually. If crucial conditions are violated, the test of remaining conditions is omitted.

Parameters

rHioPlant	HioPlant to check, HioStateFlags are set
rReportStr	Information about test results

Returns

true if rHioPlant is in I/O-plant form

Definition at line 422 of file hio_plant.cpp.

IsIndicatorEventDiagnosable() [1/2]

FAUDES_API bool faudes::IsIndicatorEventDiagnosable	(	const System &	rGen,
		const AttributeFailureTypeMap &	rFailureTypeMap
	)

Function definition for run-time interface.

Definition at line 153 of file diag_eventdiagnosis.cpp.

IsIndicatorEventDiagnosable() [2/2]

bool faudes::IsIndicatorEventDiagnosable	(	const System &	rGen,
		const AttributeFailureTypeMap &	rFailureTypeMap,
		string &	rReportString
	)

Definition at line 85 of file diag_eventdiagnosis.cpp.

IsLanguageDiagnosable() [1/2]

FAUDES_API bool faudes::IsLanguageDiagnosable	(	const System &	rGen,
		const System &	rSpec
	)

Function definition for run-time interface.

Definition at line 20 of file diag_languagediagnosis.cpp.

IsLanguageDiagnosable() [2/2]

FAUDES_API bool faudes::IsLanguageDiagnosable	(	const System &	rGen,
		const System	rSpec,
		std::string &	rReportString
	)

Test function to verify language-diagnosability.

Definition at line 445 of file diag_languagediagnosis.cpp.

IsLCC()

FAUDES_API bool faudes::IsLCC	(	const Generator &	rLowGen,
		const EventSet &	rControllableEvents,
		const EventSet &	rHighAlph
	)

Verification of local control consistency (LCC).

For verifying if a natural projection fulfills the local control consistency condition, a backward reachability is conducted. If starting from a state, where an uncontrollable high-level event is feasible, at least one local state cannot be reached by an uncontrollable path, LCC is violated.

Parameters

rLowGen	Input generator
rControllableEvents	set of controllable events
rHighAlph	High level alphabet

Returns

true if LCC holds

Definition at line 316 of file op_obserververification.cpp.

IsLive() [1/2]

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

Test if a generator is live.

Parameters

rGen	Input generator.
rReport	User-readable information of violating condition (in case of negative result).

Returns

True if generator is live.

IsLive() [2/2]

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

Definition at line 225 of file diag_eventdiagnosis.cpp.

IsModularDiagnosable() [1/3]

FAUDES_API bool faudes::IsModularDiagnosable	(	const SystemVector &	rGsubs,
		const GeneratorVector &	rKsubs
	)

Function definition for run-time interface.

Definition at line 252 of file diag_modulardiagnosis.cpp.

IsModularDiagnosable() [2/3]

bool faudes::IsModularDiagnosable	(	const SystemVector &	rGsubs,
		const GeneratorVector &	rKsubs,
		string &	rReportString
	)

Definition at line 23 of file diag_modulardiagnosis.cpp.

IsModularDiagnosable() [3/3]

bool faudes::IsModularDiagnosable	(	const vector< const System * > &	rGSubs,
		const vector< const Generator * > &	rKSubs,
		std::string &	rReportString
	)

Definition at line 50 of file diag_modulardiagnosis.cpp.

IsMtcObs()

FAUDES_API bool faudes::IsMtcObs	(	const MtcSystem &	rLowGen,
		const EventSet &	rHighAlph
	)

Verification of the observer property.

For verifying if a natural projection has the observer property, one step in the observer algorithm is evaluated. If the resulting generator equals the input generator, then the natural projection on the abstraction alphabet is an observer.

Parameters

rLowGen	Input generator
rHighAlph	High level alphabet

Returns

true if the observer property holds

Definition at line 39 of file mtc_obserververification.cpp.

IsMutuallyControllable() [1/2]

FAUDES_API void faudes::IsMutuallyControllable	(	const System &	rGen1,
		const System &	rGen2,
		bool &	rRes
	)

RTI wrapper.

Definition at line 109 of file op_mc.cpp.

IsMutuallyControllable() [2/2]

FAUDES_API bool faudes::IsMutuallyControllable	(	const System &	rGen1,
		const System &	rGen2,
		StateSet &	rForbidden1,
		StateSet &	rForbidden2
	)

Verification of mutual controllability.

This function checks if two generators are mutually controllable w.r.t. each other. Additionally, this function provides the states where mutual controllability fails in case the condition is violated.

Parameters

rGen1	Generator 1
rGen2	Generator 2
rForbidden1	Forbidden states in Generator 1
rForbidden2	Forbidden states in Generator 2

Returns

True if mutual controllability is fulfilled

Definition at line 43 of file op_mc.cpp.

IsNonblocking()

FAUDES_API bool faudes::IsNonblocking

(

const GeneratorVector &

rGvec

)

Definition at line 705 of file cfl_conflequiv.cpp.

IsNormal()

FAUDES_API bool faudes::IsNormal	(	const System &	rPlantGen,
		const Generator &	rSupCandGen
	)

IsNormal wrapper.

Wrapper for convenient access via the run-time interface.

Definition at line 147 of file syn_supnorm.cpp.

IsOCC()

FAUDES_API bool faudes::IsOCC	(	const Generator &	rLowGen,
		const EventSet &	rControllableEvents,
		const EventSet &	rHighAlph
	)

Verification of output control consistency (OCC).

For verifying if a natural projection fulfills the output control consistency condition, a backward reachability is conducted. If starting from a state, where an uncontrollable high-level event is feasible, a controllable event can be reached on a local backward path, OCC is violated.

Parameters

rLowGen	Input generator
rControllableEvents	set of controllable events
rHighAlph	High level alphabet

Returns

true if OCC holds

Definition at line 93 of file op_obserververification.cpp.

IsRelativelyOmegaClosedUnchecked()

FAUDES_API bool faudes::IsRelativelyOmegaClosedUnchecked	(	const Generator &	rGenPlant,
		const Generator &	rGenCand
	)

Test for relative closedness, omega languages.

This variant does not perform consitency tests on the parameters. Neither does it handle the special cases on empty arguments. See also IsRelativelyOmegaClosed(const Generator&, const Generator& )

Parameters

rGenPlant	Generator GPlant
rGenCand	Generator GCand

Definition at line 452 of file syn_functions.cpp.

IsStdSynthesisConsistentUnchecked()

bool faudes::IsStdSynthesisConsistentUnchecked	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rPlant0Gen
	)

Definition at line 60 of file syn_sscon.cpp.

LabelCorrection() [1/2]

void faudes::LabelCorrection	(	const multimap< Idx, DiagLabelSet > &	mm,
		AttributeDiagnoserState &	attr
	)

Definition at line 1047 of file diag_eventdiagnosis.cpp.

LabelCorrection() [2/2]

FAUDES_API void faudes::LabelCorrection	(	const std::multimap< Idx, DiagLabelSet > &	mm,
		AttributeDiagnoserState &	attr
	)

Perform label correction on propagated failure type labels.

Parameters

mm	Propagated absolute failure type labels for a diagnoser state.
attr	Output variable for the diagnoser state attribute.

LabelPropagation()

FAUDES_API void faudes::LabelPropagation	(	const DiagLabelSet &	lastLabel,
		const DiagLabelSet &	failureTypes,
		DiagLabelSet &	newLabel
	)

Generate a new label.

From the last label and the failure types that occurred on the way, the new label is generated.

Parameters

lastLabel	Diagnoser label of state estimate.
failureTypes	Failure types that occurred.
newLabel	Output variable for the new label.

Definition at line 1020 of file diag_eventdiagnosis.cpp.

LanguageIntersection()

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

Language intersection.

See also LanguageUnion(const Generator&, const Generator&, Generator&); This version takes a vector of generators as argument to perform the intersection for multiple languages. The implementation calls the std intersection multiple times, future implementations may do better.

Parameters

rGenVec	Vector of input generators
rResGen	Reference to resulting generator

Definition at line 205 of file cfl_regular.cpp.

LanguageUnion()

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

Language union.

See also LanguageUnion(const Generator&, const Generator&, Generator&); This version takes a vector of generators as argument to perform the union for multiple languages. The implementation calls the std union multiple times, future implementations may do better.

Parameters

rGenVec	Vector of input generators
rResGen	Reference to resulting generator

Definition at line 155 of file cfl_regular.cpp.

LhaReach()

void FAUDES_API faudes::LhaReach	(	const LinearHybridAutomaton &	lha,
		const HybridStateSet &	states,
		std::map< Idx, HybridStateSet * > &	ostates,
		int *	pCnt
	)

compute sets of reachable state per successor event

Definition at line 163 of file hyb_reachability.cpp.

LocalAccessibleReach()

FAUDES_API void faudes::LocalAccessibleReach	(	const Generator &	rLowGen,
		const EventSet &	rHighAlph,
		Idx	lowState,
		StateSet &	rAccessibleReach
	)

Compute the accessible reach for a local automaton.

Parameters

rLowGen	Low level generator
rHighAlph	High level alphabet
lowState	Low level entry state
rAccessibleReach	Result

Definition at line 161 of file cfl_localgen.cpp.

LocalCoaccessibleReach()

FAUDES_API void faudes::LocalCoaccessibleReach	(	const TransSetX2EvX1 &	rRevTransRel,
		const EventSet &	rHighAlph,
		Idx	lowState,
		StateSet &	rCoaccessibleReach
	)

Compute the coaccessible reach for a local automaton.

Parameters

rRevTransRel	Reverse sorted transition relation
rHighAlph	High level alphabet
lowState	Low level exit state
rCoaccessibleReach	Result

Definition at line 129 of file cfl_localgen.cpp.

LocalObservationConsistency()

FAUDES_API bool faudes::LocalObservationConsistency	(	const System &	rPlantGen,
		const System &	rSpecGen,
		const EventSet &	rHighAlph,
		const EventSet &	rObsAlph
	)

Supervisor Reduction algorithm.

Computes a reduced supervisor from a given potentially non-reduced supervisor and the plant. This algorithm implements the results obtained in

R. Su and W. M. Wonham. Supervisor Reduction for Discrete-Event Systems. Discrete Event Dynamic Systems vol. 14, no. 1, January 2004.

Both, plant and supervisor MUST be deterministic and share the same alphabet!!!

Parameters

rPlantGen	Plant generator
rSpecGen	Specification generator
rHighAlph	high-level alphabet
rObsAlph	observable alphabet

Returns

True if a reduction was achieved

Exceptions

Exception

alphabets of generators don't match (id 100) plant nondeterministic (id 201) supervisor nondeterministic (id 203) plant and supervisor nondeterministic (id 204)

Definition at line 40 of file obs_local_observation_consistency.cpp.

LocalSelfloop()

void faudes::LocalSelfloop	(	Generator &	rGen,
		EventSet &	rLocAlph
	)

remove the events from a generator which have only selfloop transitions

Parameters

rGen	generator which is to be abstracted
rLocAlph	local events

Definition at line 725 of file syn_compsyn.cpp.

LoopCallback() [1/3]

void faudes::LoopCallback

(

bool

pBreakvoid

)

Definition at line 633 of file cfl_utils.cpp.

LoopCallback() [2/3]

FAUDES_API void faudes::LoopCallback

(

bool(*)(void)

pBreakFnct

)

Algorithm loop callback.

Set a callback function for libFAUDES algorithms. Applications are meant to use this interface to terminate an algorithm on user request. libFAUDES algorithms are meant to throw an execption when the callback function returns true. See also void LoopCallback(void).

Parameters

pBreakFnct

LoopCallback() [3/3]

FAUDES_API void faudes::LoopCallback

(

void

)

Algorithm loop callback.

Calls the loop callback function and throws an exception if it returns true.

Exceptions

Break

on appliation request (id 110)

Definition at line 640 of file cfl_utils.cpp.

LowExitStates() [1/2]

FAUDES_API void faudes::LowExitStates	(	const EventSet &	rHighAlph,
		const std::map< Idx, StateSet > &	rEntryStatesMap,
		const TransSetX2EvX1 &	rLowRevTransRel,
		Idx	highState,
		StateSet &	rLowExitStates
	)

LowExitStates call-by-reference function:

Compute the low level exit states for a corresponding hi level state

Parameters

rHighAlph	High level events
rEntryStatesMap	Entry states map (see CreateEntryStatesMap(resmap))
rLowRevTransRel	Reverse sorted low level transition relation
highState	Hi level state for which to compute low level exit states
rLowExitStates	Reference to StateSet for low level exit states (result)

Exceptions

Exception

Hi level state not found in entry states map (with FAUDES_CHECKED)

Definition at line 40 of file cfl_localgen.cpp.

LowExitStates() [2/2]

FAUDES_API StateSet faudes::LowExitStates	(	const Generator &	rLowGen,
		const EventSet &	rHighAlph,
		const std::map< Idx, StateSet > &	rEntryStatesMap,
		const TransSetX2EvX1 &	rLowRevTransRel,
		Idx	highState
	)

LowExitStates return-copy function:

Wrapper for the corresponding call-by-reference function. Creates new StateSet, calls function and returns StateSet containing low level exit states.

Parameters

rLowGen	Low level generator (just needed for determining statetable)
rHighAlph	High level events
rEntryStatesMap	Entry states map (see CreateEntryStatesMap(resmap))
rLowRevTransRel	Reverse sorted low level transition relation
highState	Hi level state for which to compute low level exit states

Exceptions

Exception

Hi level state not found in entry states map (with FAUDES_CHECKED) (id 502)

Definition at line 27 of file cfl_localgen.cpp.

MakeDistinguisher()

void faudes::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

Parameters

AbstGen	the abstracted generator
rMapStateToPartition	map state to equivalent class
OrigGen	the non-abstracted generator (after halbway-synthesis bevor abstraction)
rMapOldToNew	map the replaced events to new events

Definition at line 753 of file syn_compsyn.cpp.

MangleString()

std::string faudes::MangleString

(

const std::string &

str

)

Definition at line 146 of file lbp_function.cpp.

MeetsDiagnosabilityAssumptions()

bool faudes::MeetsDiagnosabilityAssumptions	(	const System &	rGen,
		const AttributeFailureTypeMap &	rFailureTypeMap,
		string &	rReportString
	)

Definition at line 160 of file diag_eventdiagnosis.cpp.

MergeEquivalenceClasses()

void faudes::MergeEquivalenceClasses	(	Generator &	rGen,
		TransSetX2EvX1 &	rRevTrans,
		const std::list< StateSet > &	rClasses
	)

Definition at line 74 of file cfl_conflequiv.cpp.

MergeNonCoaccessible()

void faudes::MergeNonCoaccessible

(

Generator &

g

)

Definition at line 417 of file cfl_conflequiv.cpp.

MergeSilentLoops()

void faudes::MergeSilentLoops	(	Generator &	g,
		const EventSet &	silent
	)

Definition at line 341 of file cfl_conflequiv.cpp.

ModularDiagnoser() [1/2]

FAUDES_API bool faudes::ModularDiagnoser	(	const SystemVector &	rGsubs,
		const GeneratorVector &	rKsubs,
		GeneratorVector &	rDiagsubs
	)

Function definition for run-time interface.

Definition at line 260 of file diag_modulardiagnosis.cpp.

ModularDiagnoser() [2/2]

bool faudes::ModularDiagnoser	(	const SystemVector &	rGsubs,
		const GeneratorVector &	rKsubs,
		GeneratorVector &	rDiagSubs,
		string &	rReportString
	)

Definition at line 128 of file diag_modulardiagnosis.cpp.

mtcDeterministic() [1/2]

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

Make generator deterministic.

(function wrapper)

The second parameter is an empty std::map<Idx,StateSet> which holds all the pairs of new states and their respective power states set. This is used as a so called "entry state map" for deterministic projected generators.

Parameters

rGen	Reference to generator
rEntryStatesMap	Entry state map
rResGen	Reference to resulting deterministic generator

Definition at line 82 of file mtc_project.cpp.

mtcDeterministic() [2/2]

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

Make generator deterministic.

(real function)

Second and third parameter hold the subsets + deterministic states in vectors

The multiway merge algorithm is based on a propsal in "Ted Leslie, Efficient Approaches to Subset Construction, Computer Science, University of Waterloo, 1995"

Parameters

rGen	Reference to generator
rPowerStates	Vector that holds the power states
rDetStates	Vector that holds the corresponding deterministic states
rResGen	Reference to resulting deterministic generator

Definition at line 99 of file mtc_project.cpp.

mtcInvProject()

FAUDES_API void faudes::mtcInvProject	(	const MtcSystem &	rGen,
		const EventSet &	rProjectAlphabet,
		MtcSystem &	rResGen
	)

RTI wrapper.

See mtcInvProject(MtcSystem&, const EventSet&).

Definition at line 518 of file mtc_project.cpp.

mtcParallel()

FAUDES_API void faudes::mtcParallel	(	const MtcSystem &	rGen1,
		const MtcSystem &	rGen2,
		std::map< std::pair< Idx, Idx >, Idx > &	rReverseCompositionMap,
		MtcSystem &	rResGen
	)

Parallel composition of two MtcSystems.

Parameters

rGen1	First MtcSystem for parallel composition
rGen2	Second MtcSystem for parallel composition
rReverseCompositionMap
rResGen	Generator in which the result of the parallel composition is saved

Definition at line 58 of file mtc_parallel.cpp.

mtcProject()

FAUDES_API void faudes::mtcProject	(	const MtcSystem &	rGen,
		const EventSet &	rProjectAlphabet,
		std::map< Idx, StateSet > &	rEntryStatesMap,
		MtcSystem &	rResGen
	)

Minimized Deterministic projection.

Does not modify generator. Calls project, determine and statemin. See functions for details.

Parameters

rGen	Reference to generator
rProjectAlphabet	Projection alphabet
rEntryStatesMap	Reference to entry states map, see Deterministic(..) (result)
rResGen	Reference to resulting deterministic generator (result)

Definition at line 453 of file mtc_project.cpp.

mtcStateMin() [1/3]

FAUDES_API void faudes::mtcStateMin	(	const MtcSystem &	rGen,
		MtcSystem &	rResGen
	)

RTI wrapper.

See also mtcStateMin(MtcSystem&, MtcSystem&).

Definition at line 301 of file mtc_statemin.cpp.

mtcStateMin() [2/3]

FAUDES_API void faudes::mtcStateMin	(	MtcSystem &	rGen,
		MtcSystem &	rResGen
	)

State Minimization This function implements the (n*log n) set partitioning algorithm by John E.

Hopcroft extended to colored marking. Given generator will be made accessible before computing minimized generator.

Parameters

rGen	MtcSystem
rResGen	Minimized MtcSystem (result)

Exceptions

Exception

Input automaton nondeterministic (id 505)

Definition at line 32 of file mtc_statemin.cpp.

mtcStateMin() [3/3]

FAUDES_API void faudes::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.

Hopcroft extended to colored marking. Given generator will be made accessible before computing minimized generator.

Parameters

rGen	MtcSystem
rResGen	Minimized MtcSystem (result)
rSubsets	Vector of subsets that will be constructed during running the algorithm (optional parameter)
rNewIndices	Vector of new state indices corresponding to the subsets (optional parameter)

Exceptions

Exception

Input automaton nondeterministic (id 505)

Definition at line 39 of file mtc_statemin.cpp.

mtcSupConClosed()

FAUDES_API void faudes::mtcSupConClosed	(	const MtcSystem &	rPlantGen,
		const MtcSystem &	rSpecGen,
		std::map< std::pair< Idx, Idx >, Idx > &	rReverseCompositionMap,
		MtcSystem &	rResGen
	)

Supremal Controllable Sublanguage.

Only for deterministic plant + spec. Throws exception if plant or spec is nondeterministic.

Real mtcSupCon function

Finds the "largest" sublanguage of h for that language of g is controllable with respect to h. Differing from theory the marked language of h may not be a sublanguage of g but both must share the same alphabet.

See "C.G CASSANDRAS AND S. LAFORTUNE. Introduction to Discrete Event Systems. Kluwer, 1999." for base algorithm.

This version creates a "reverse composition map" given as reference parameter.

Parameters

rPlantGen	Plant MtcSystem
rSpecGen	Specification MtcSystem
rReverseCompositionMap	std::map< std::pair<Idx,Idx>, Idx> as in the parallel composition function
rResGen	Reference to resulting MtcSystem, the minimal restrictive supervisor

Exceptions

Exception

Alphabets of generators don't match (id 500) plant nondeterministic (id 501) spec nondeterministic (id 503) plant and spec nondeterministic (id 504)

Definition at line 140 of file mtc_supcon.cpp.

mtcSupConNB()

FAUDES_API void faudes::mtcSupConNB	(	const MtcSystem &	rPlantGen,
		const MtcSystem &	rSpecGen,
		std::map< std::pair< Idx, Idx >, Idx > &	rReverseCompositionMap,
		MtcSystem &	rResGen
	)

Nonblocking Supremal Controllable Sublanguage.

Only for deterministic plant + spec. Throws exception if plant or spec is nondeterministic.

Real mtcSupConNB function

Finds the "largest" sublanguage of h for that language of g is controllable with respect to h. Differing from theory the marked language of h may not be a sublanguage of g but both must share the same alphabet.

See "C.G CASSANDRAS AND S. LAFORTUNE. Introduction to Discrete Event Systems. Kluwer, 1999." for base algorithm.

This version creates a "reverse composition map" given as reference parameter.

Parameters

rPlantGen	Plant MtcSystem
rSpecGen	Specification MtcSystem
rReverseCompositionMap	std::map< std::pair<Idx,Idx>, Idx> as in the parallel composition function
rResGen	Reference to resulting MtcSystem, the minimal restrictive nonblocking supervisor

Exceptions

Exception

Alphabets of generators don't match (id 500) plant nondeterministic (id 501) spec nondeterministic (id 503) plant and spec nondeterministic (id 504)

Definition at line 50 of file mtc_supcon.cpp.

mtcSupConParallel()

FAUDES_API void faudes::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.

Composition stops at transition paths that leave the specification by uncontrollable events in plant.

Parameters

rPlantGen	Plant MtcSystem
rSpecGen	Specification MtcSystem
rUAlph	Uncontrollable Events
rReverseCompositionMap	std::map< std::pair<Idx,Idx>, Idx> as in the parallel composition function
rResGen	Reference to resulting MtcSystem, the less restrictive supervisor

Definition at line 220 of file mtc_supcon.cpp.

mtcSupConUnchecked()

FAUDES_API void faudes::mtcSupConUnchecked	(	const MtcSystem &	rPlantGen,
		const EventSet &	rCAlph,
		MtcSystem &	rSupGen
	)

Supremal Controllable Sublangauge (Real SupCon function; unchecked)

Both, plant and spec MUST be deterministic and share the same alphabet!!!

Most likely will result in blocking states.

Parameters

rPlantGen	Plant generator
rCAlph	Controllable events
rSupGen	Specification generator

Exceptions

Exception

Alphabets of generators don't match (id 500) Plant generator nondeterministic (id 501) Specification generator nondeterministic (id 503) Plant & Spec generator nondeterministic (id 504)

Definition at line 464 of file mtc_supcon.cpp.

mtcUniqueInit()

void faudes::mtcUniqueInit

(

MtcSystem &

rGen

)

Definition at line 34 of file mtc_project.cpp.

NDeviceListen()

void * faudes::NDeviceListen

(

void *

arg

)

Definition at line 682 of file iop_simplenet.cpp.

NormalityConsistencyCheck()

FAUDES_API void faudes::NormalityConsistencyCheck	(	const Generator &	rL,
		const EventSet &	rOAlph,
		const Generator &	rK
	)

NormalityConsistencyCheck: Consistency check for normality input data.

Used e.g. in IsNormal(), and SupNorm(). See exceptions.

Parameters

rL	generator of language L
rOAlph	observable alphabet
rK	generator of language K

Exceptions

Exception

nondeterministic parameter(s) (id: 101) rOAlph not subset of rL.Alphabet() (id: 100) Alphabets of generators don't match (id: 100) K is not subset of L (id 0)

Definition at line 45 of file syn_supnorm.cpp.

ObservationEquivalentQuotient()

void faudes::ObservationEquivalentQuotient	(	Generator &	g,
		const EventSet &	silent
	)

Definition at line 128 of file cfl_conflequiv.cpp.

OmegaControlledLiveness() [1/3]

bool faudes::OmegaControlledLiveness	(	Generator &	rSupCandGen,
		const EventSet &	rCAlph,
		const StateSet &	rPlantMarking
	)

Definition at line 544 of file syn_wsupcon.cpp.

OmegaControlledLiveness() [2/3]

bool faudes::OmegaControlledLiveness	(	Generator &	rSupCandGen,
		const EventSet &	rCAlph,
		const StateSet &	rPlantMarking,
		std::map< Idx, EventSet > &	rFeedbackMap
	)

Definition at line 682 of file syn_wsupcon.cpp.

OmegaControlledLiveness() [3/3]

bool faudes::OmegaControlledLiveness	(	Generator &	rSupCandGen,
		const EventSet &	rCAlph,
		const StateSet &	rPlantMarking,
		std::map< Idx, Idx > &	rControllerStatesMap,
		std::map< Idx, EventSet > &	rFeedbackMap
	)

Definition at line 873 of file syn_wsupcon.cpp.

OmegaSupConNBUnchecked()

void faudes::OmegaSupConNBUnchecked	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSpecGen,
		StateSet &	rPlantMarking,
		Generator &	rResGen
	)

Definition at line 1345 of file syn_wsupcon.cpp.

OmegaSupConNormNBUnchecked()

void faudes::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
	)

Definition at line 1463 of file syn_wsupcon.cpp.

OmegaSupConProduct()

void faudes::OmegaSupConProduct	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSpecGen,
		std::map< OPSState, Idx > &	rProductCompositionMap,
		Generator &	rResGen
	)

Definition at line 1132 of file syn_wsupcon.cpp.

OnlySilentIncoming()

void faudes::OnlySilentIncoming	(	Generator &	g,
		const EventSet &	silent
	)

Definition at line 441 of file cfl_conflequiv.cpp.

OnlySilentOutgoing()

void faudes::OnlySilentOutgoing	(	Generator &	g,
		const EventSet &	silent
	)

Definition at line 496 of file cfl_conflequiv.cpp.

Parallel() [1/2]

FAUDES_API void faudes::Parallel	(	const Generator &	rGen1,
		const Generator &	rGen2,
		ProductCompositionMap &	rCompositionMap,
		StateSet &	rMark1,
		StateSet &	rMark2,
		Generator &	rResGen
	)

Parallel composition.

See Parallel(const Generator&, const Generator&, Generator&). This version fills a composition map to map pairs of old states to new states. It also returns the sets of states marked w.r.t. the argument generators.

Parameters

rGen1	First generator
rGen2	Second generator
rCompositionMap	Composition map (map< pair<Idx,Idx>, Idx>)
rMark2	States maked in first generator
rMark1	States maked in second generator
rResGen	Reference to resulting parallel composition generator

Definition at line 170 of file cfl_parallel.cpp.

Parallel() [2/2]

FAUDES_API void faudes::Parallel	(	const Generator &	rGen1,
		const Generator &	rGen2,
		std::map< std::pair< Idx, Idx >, Idx > &	rCompositionMap,
		Generator &	rResGen
	)

Parallel composition.

See Parallel(const Generator&, const Generator&, Generator&). This version fills a composition map to map pairs of old states to new states.

Parameters

rGen1	First generator
rGen2	Second generator
rCompositionMap	Composition map (map< pair<Idx,Idx>, Idx>)
rResGen	Reference to resulting parallel composition generator

Definition at line 213 of file cfl_parallel.cpp.

PathSeparator()

FAUDES_API const std::string& faudes::PathSeparator

(

void

)

Std dir-separator.

Returns

Separator as one-char string

PluginsString()

FAUDES_API std::string faudes::PluginsString

(

)

Return FAUDES_PLUGINS as std::string.

Returns

std::string with FAUDES_VERSION

Definition at line 136 of file cfl_utils.cpp.

PolyScratch()

void faudes::PolyScratch

(

void

)

scratch

Definition at line 199 of file hyb_compute.cpp.

PrependPath()

FAUDES_API std::string faudes::PrependPath	(	const std::string &	rLeft,
		const std::string &	rRight
	)

Prepend one path before another.

Specifically, insert a path seperator if necessary.

Parameters

rLeft	Directory eg "/home/friend/data"
rRight	File eg "generator.gen"

Returns

Path eg "/home/friend/data/generator.gen"

Definition at line 303 of file cfl_utils.cpp.

ProcessDot()

FAUDES_API void faudes::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.

If no output format is given, try to guess from filename extension.

Parameters

rDotFile	name of dot file
rOutFile	name of graphics file
rOutFormat	graphics format eg "png", "jpg"
rDotExec	path/name of executable

Exceptions

Exception

error in systemcall (id 3) unkown format (id 3)

Definition at line 148 of file cfl_utils.cpp.

Product() [1/2]

FAUDES_API void faudes::Product	(	const Generator &	rGen1,
		const Generator &	rGen2,
		std::map< std::pair< Idx, Idx >, Idx > &	rCompositionMap,
		Generator &	rResGen
	)

Product composition.

See Product(const Generator&, const Generator&, Generator&). This version fills given composition map to map pairs of old states to new states.

Parameters

rGen1	First generator
rGen2	Second generator
rCompositionMap	Composition map (map< pair<Idx,Idx>, Idx>)
rResGen	Reference to resulting product composition generator

Definition at line 518 of file cfl_parallel.cpp.

Product() [2/2]

FAUDES_API void faudes::Product	(	const Generator &	rGen1,
		const Generator &	rGen2,
		std::map< std::pair< Idx, Idx >, Idx > &	rCompositionMap,
		StateSet &	rMark1,
		StateSet &	rMark2,
		Generator &	rResGen
	)

Product composition.

See Product(const Generator&, const Generator&, Generator&). This version fills given composition map to map pairs of old states to new states. It also returns the sets of states marked w.r.t. the argument generators.

Parameters

rGen1	First generator
rGen2	Second generator
rCompositionMap	Composition map (map< pair<Idx,Idx>, Idx>)
rMark2	States maked in first generator
rMark1	States maked in second generator
rResGen	Reference to resulting product composition generator

Definition at line 493 of file cfl_parallel.cpp.

Project()

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

Deterministic projection.

Projects the generated and marked languages to a subalphabet of the original alphabet, and subsequently calls Deterministic to construct a deterministic minimal realisation of the result. The input generator does not need to be deterministic.

Parameters

rGen	Reference to generator
rProjectAlphabet	Projection alphabet
rEntryStatesMap	Reference to entry states map, see Deterministic(..) (result)
rResGen	Reference to resulting deterministic generator (result)

Definition at line 1437 of file cfl_project.cpp.

ProjectNonDet_barthel()

void faudes::ProjectNonDet_barthel	(	Generator &	rGen,
		const EventSet &	rProjectAlphabet
	)

Definition at line 681 of file cfl_project.cpp.

ProjectNonDet_fbr()

void faudes::ProjectNonDet_fbr	(	Generator &	rGen,
		const EventSet &	rProjectAlphabet
	)

Definition at line 799 of file cfl_project.cpp.

ProjectNonDet_graph()

void faudes::ProjectNonDet_graph	(	Generator &	rGen,
		const EventSet &	rProjectAlphabet
	)

Definition at line 491 of file cfl_project.cpp.

ProjectNonDet_opitz()

void faudes::ProjectNonDet_opitz	(	Generator &	rGen,
		const EventSet &	rProjectAlphabet
	)

Definition at line 46 of file cfl_project.cpp.

ProjectNonDet_ref()

void faudes::ProjectNonDet_ref	(	Generator &	rGen,
		const EventSet &	rProjectAlphabet
	)

Definition at line 128 of file cfl_project.cpp.

ProjectNonDet_scc()

void faudes::ProjectNonDet_scc	(	Generator &	rGen,
		const EventSet &	rProjectAlphabet
	)

Definition at line 1054 of file cfl_project.cpp.

ProjectNonDet_simple()

void faudes::ProjectNonDet_simple	(	Generator &	rGen,
		const EventSet &	rProjectAlphabet
	)

Definition at line 601 of file cfl_project.cpp.

ReachableEvents() [1/2]

FAUDES_API EventSet faudes::ReachableEvents	(	const Generator &	rLowGen,
		const EventSet &	rHighAlph,
		Idx	lowState
	)

ReachableEvents return-copy function:

Wrapper for the corresponding call-by-reference function. Creates new EventSet, calls function and returns EventSet containing the reachable hi level events.

Parameters

rLowGen	Low level generator
rHighAlph	High level alphabet
lowState	Low level state

Definition at line 76 of file cfl_localgen.cpp.

ReachableEvents() [2/2]

FAUDES_API void faudes::ReachableEvents	(	const Generator &	rLowGen,
		const EventSet &	rHighAlph,
		Idx	lowState,
		EventSet &	rReachableEvents
	)

ReachableEvents call-by-reference function:

Compute the set of hi level events which can be reached from a low level state. Resulting set will be cleared first.

Parameters

rLowGen	Low level generator
rHighAlph	High level alphabet
lowState	Low level state
rReachableEvents	Reference to EventSet which will contain the reachable high level events (result)

Definition at line 88 of file cfl_localgen.cpp.

ReadDirectory()

FAUDES_API std::set< std::string > faudes::ReadDirectory

(

const std::string &

rDirectory

)

Read the contents of the specified directors.

Parameters

rDirectory

Directory eg "/home/friend/data"

Returns

List of files, e.g. "gen1.gen gen2.gen data subdir"

Definition at line 348 of file cfl_utils.cpp.

rec_ComputeLoopPreservingObserver()

FAUDES_API bool faudes::rec_ComputeLoopPreservingObserver	(	const System &	rGen,
		const EventSet &	rInitialHighAlph,
		EventSet &	rHighAlph,
		const std::vector< Idx > &	rDiffVector,
		Idx	numberEvents,
		Idx	currentNumberEvents,
		Idx	currentLocation,
		EventSet	chosenEvents
	)

rec_ComputeLoopPreservingObserver(rGen, rInitialHighAlph, rHighAlph, rDdffVector, numberEvents, currentNumberEvents, currentLocation, hosenEvents)

Definition at line 715 of file diag_languagediagnosis.cpp.

rec_OptimalColorSet()

FAUDES_API void faudes::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.

This function recursively enumerates all possible subsets of colors that can be removed without affecting supervisor synthesis and remembers the color set that leads to the smallest hierarchical abstraction. It is called by the function OptimalColorSet.

Parameters

rGen	input colored marking generator
rColorVector	set of colors of the generator (ordered!)
colorNumber	number of colors currently removed
rOptimalColors	current optimal set of colors
rOptimalNumberStates	current optimal number of states
rOptimalNumberColors	size of the optimal color set
rHighAlph	initial high-level alphabet
rOptimalHighAlph	optimal high-level alphabet

Definition at line 289 of file mtc_redundantcolors.cpp.

recursiveCheckLCC()

FAUDES_API void faudes::recursiveCheckLCC	(	const TransSetX2EvX1 &	rRevTransSet,
		const EventSet &	rControllableEvents,
		const EventSet &	rHighAlph,
		Idx	currentState,
		StateSet &	rDoneStates
	)

Find states that fulfill the lcc condition.

This function performs a backward reachability computation to determine states where the lcc condition is fulfilled

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

rRevTransSet	Reversely ordered transition relation
rControllableEvents	Set of controllable events
rHighAlph	Abstraction alphabet
currentState	Index of the start state of the backward reachability computation
rDoneStates	Set of already investigated states

Definition at line 387 of file op_observercomputation.cpp.

recursiveCheckMSABackward()

FAUDES_API bool faudes::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.

This function performs a backward reachability computation to determine if the msa-observer condition is fulfilled for a given state.

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

rGen	Generator for which the dynamic system is computed
rRevTransSet	Reversely ordered transition relation
rHighAlph	Abstraction alphabet
currentState	Index of the state to be checked
rDoneStates	Set of already investigated states

Returns

True if the condition is fulfilled, false otherwise

Definition at line 278 of file op_observercomputation.cpp.

recursiveCheckMSAForward()

bool faudes::recursiveCheckMSAForward	(	const Generator &	rGen,
		const EventSet &	rHighAlph,
		Idx	currentState,
		StateSet &	rDoneStates
	)

Check if the msa-observer conditions is fulfilled for a given state.

This function performs a forward reachability computation to determine if the msa-observer condition is fulfilled for a given state.

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

rGen	Generator for which the dynamic system is computed
rHighAlph	Abstraction alphabet
currentState	Index of the state to be checked
rDoneStates	Set of already investigated states

Returns

True if the condition is fulfilled, false otherwise

Definition at line 252 of file op_observercomputation.cpp.

relabel() [1/2]

bool faudes::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.

This function checks the termination criterion of the observer algorithm. If required, transitions of the input generator are relabeled.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenRelabel. There are no further restrictions on parameters.

Parameters

rGenRelabel	Generator whose transitions are modified
rControllableEvents	Set of controllable events
rHighAlph	Abstraction alphabet
rMapStateToPartition	Maps each state of rGenRelabel to an equivalence class
rMapChangedTransReverse	Maps the relabeled transitions to the original transitions
rMapChangedTrans	Maps the the modified original transitions to its new events
rMapRelabeledEvents	Maps the original events to the set of new events they were relabeled with

Definition at line 1463 of file op_observercomputation.cpp.

relabel() [2/2]

bool faudes::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.

This function checks the termination criterion of the observer algorithm. If required, transitions of the input generator are relabeled.

The alphabets rHighAlph and rControllableEvents have to be subsets of the alphabet of rGenRelabel. There are no further restrictions on parameters.

Parameters

rGenRelabel	Generator whose transitions are modified
rControllableEvents	Set of controllable events
rHighAlph	Abstraction alphabet
rMapStateToPartition	Maps each state of rGenRelabel to an equivalence class
rMapChangedTransReverse	Maps the relabeled transitions to the original transitions
rMapChangedTrans	Maps the the modified original transitions to its new events
rMapRelabeledEvents	Maps the original events to the set of new events they were relabeled with

Definition at line 1463 of file op_observercomputation.cpp.

RemoveNonCoaccessibleOut()

void faudes::RemoveNonCoaccessibleOut

(

Generator &

g

)

Definition at line 372 of file cfl_conflequiv.cpp.

RemoveTauLoops()

FAUDES_API void faudes::RemoveTauLoops	(	Generator &	rGen,
		const EventSet &	silent
	)

Remove all silent loops in a given automaton.

This function is considered as an API not only for its general operational meaning, but most importantly due to the prerequisite for topological sort.

Parameters

rGen	input generator
silent	silent alphabet, contains at most one event

Definition at line 563 of file cfl_conflequiv.cpp.

RemoveTauSelfloops()

void faudes::RemoveTauSelfloops	(	Generator &	g,
		const EventSet &	silent
	)

Definition at line 328 of file cfl_conflequiv.cpp.

SDeviceSynchro()

void * faudes::SDeviceSynchro

(

void *

arg

)

Definition at line 772 of file iop_sdevice.cpp.

SearchScc() [1/2]

FAUDES_API void faudes::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.

This function implements the algorithm based on a depth first search presented in: -Aho, Hopcroft, Ullman: The Design and Analysis of Computer Algorithms-

Most of the comments in this function have been literally taken from this book!

Parameters

state	State, from which the current recursion is started.
rCount	denotes the current depth of the recursion.
rGen	Generator under investigation
rNewStates	Set of states that up to now were not found by the depth first search
rSTACK	stack of state indices
rStackStates	set of states whose indices are on STACK.
rDFN	map assigning to each state its Depth-First Number
rLOWLINK	map assigning to each state its LOWLINK Number
rSccSet	result - the set of strongly connected components
rRoots	result - the set of states that each are root of some SCC.

Definition at line 33 of file mtc_redundantcolors.cpp.

SearchScc() [2/2]

FAUDES_API void faudes::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).

This function partitions the stateset of a generator into equivalent 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.

This function implements the algorithm based on a recursive depth first search presented in:

– Aho, Hopcroft, Ullman: The Design and Analysis of Computer Algorithms –

While the original algorithm works on a directed graph, this implementation adds some features that refer to transition systems and allow to filter SCCs on the run. The filter condition is specified by the SccFilter parameter rFilter.

Note: this version is derived from earlier implementations used in various plug-ins; in due course, this version will replace earlier versions.

Note: Due to the recursive implementation, this function requires a stack size proportional to the largest SCC. We have experienced typical default configurations to be good for a depth of about 80000 (Mac OSX 10.6, Debian 7.4). For SCCs exceeding the default stack size, you may adjust the operating system parameters accordingly. On Unix/Linux/MacOsX this is done by the shell command "ulimit -s hard". A future revision of SearchSCC() may be re-designed to circumvent this inconvenient issue.

Note: for a convenience API see also ComputeScc()

Parameters

vState	State, from which the current recursion is started.
vRcount	Denotes the current depth of the recursion.
rGen	Transition system to investigate
rFilter	Filter out specified transitions
rTodo	Set of states that up to now were not found by the depth first search.
rStack	Stack of states to represent current path.
rStackStates	Set of states that are in rStack
rDfn	Map assigning to each state idx its Depth-First Number.
rLowLnk	Map assigning to each state its LOWLINK Number.
rSccList	Set SCCs (accumulative result).
rRoots	Set of states that each are root of some SCC (accumulative result).

Definition at line 228 of file cfl_graphfncts.cpp.

SelectSubsystem_V1()

void faudes::SelectSubsystem_V1	(	GeneratorVector &	rGenVec,
		Generator &	rResGen
	)

heuristic: vorious approaches to select subsystem from synthesis-buffer then compose them and remove them from buffer.

1. determine subsystem
2. parallel composition for subsystem
3. delete subsystem from "GenVec"

Parameters

rGenVec	synthesis-buffer
rResGen	the composed new generator

Definition at line 1032 of file syn_compsyn.cpp.

SelectSubsystem_V2()

void faudes::SelectSubsystem_V2	(	GeneratorVector &	rGenVec,
		Generator &	rResGen
	)

Definition at line 1100 of file syn_compsyn.cpp.

SetComposedStateNames()

FAUDES_API void faudes::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.

Purely cosmetic.

Parameters

rGen1	First generator
rGen2	Second generator
rCompositionMap	Composition map (map< pair<Idx,Idx>, Idx>)
rGen12	Reference to resulting parallel composition generator

Definition at line 654 of file cfl_parallel.cpp.

SetDifference()

FAUDES_API void faudes::SetDifference	(	const vGenerator &	rGenA,
		const vGenerator &	rGenB,
		EventSet &	rRes
	)

RTI convenience function.

Definition at line 4038 of file cfl_generator.cpp.

SetIntersection() [1/2]

FAUDES_API void faudes::SetIntersection	(	const GeneratorVector &	rGenVec,
		EventSet &	rRes
	)

RTI convenience function.

Definition at line 4001 of file cfl_generator.cpp.

SetIntersection() [2/2]

FAUDES_API void faudes::SetIntersection	(	const vGenerator &	rGenA,
		const vGenerator &	rGenB,
		EventSet &	rRes
	)

RTI convenience function.

Definition at line 4028 of file cfl_generator.cpp.

SetUnion() [1/2]

FAUDES_API void faudes::SetUnion	(	const GeneratorVector &	rGenVec,
		EventSet &	rRes
	)

RTI convenience function.

Definition at line 4015 of file cfl_generator.cpp.

SetUnion() [2/2]

FAUDES_API void faudes::SetUnion	(	const vGenerator &	rGenA,
		const vGenerator &	rGenB,
		EventSet &	rRes
	)

RTI convenience function.

Definition at line 4033 of file cfl_generator.cpp.

SingleTransSpec()

void faudes::SingleTransSpec	(	const Generator &	rSpecGen,
		const EventSet &	rUncAlph,
		Generator &	rResGen
	)

Definition at line 604 of file syn_compsyn.cpp.

Splitter()

void faudes::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

Parameters

rMapOldToNew	map the replaced events to new events
rConAlph	controllable events
rGenVec	synthesis-buffer
rMapEventsToPlant	map the events in supervisor to plant
rDisGenVec	distinguisher generator-vector
rSupGenVec	supervisor generator-vector

Definition at line 898 of file syn_compsyn.cpp.

SplittGen()

void faudes::SplittGen	(	Generator &	rGen,
		Idx	parent,
		const std::vector< Idx > &	kids
	)

subfunction for Splitter: splitt the events in a generator

Parameters

rGen	a generator
parent	primal event
kids	new events

Definition at line 856 of file syn_compsyn.cpp.

StateMin()

FAUDES_API void faudes::StateMin	(	const Generator &	rGen,
		Generator &	rResGen,
		std::vector< StateSet > &	rSubsets,
		std::vector< Idx > &	rNewIndices
	)

State set minimization.

This function implements the (n*log n) set partitioning algorithm by John E. Hopcroft. Given generator will be made accessible before computing minimized generator. See also StateMin(Generator&,Generator&).

Parameters

rGen	Generator
rResGen	Minimized generator (result)
rSubsets	Vector of subsets that will be constructed during running the algorithm (optional parameter)
rNewIndices	Vector of new state indices corresponding to the subsets (optional parameter)

Exceptions

Exception

Input automaton nondeterministic (id 101)

Definition at line 620 of file cfl_statemin.cpp.

StateMin_org()

void faudes::StateMin_org	(	const Generator &	rGen,
		Generator &	rResGen,
		std::vector< StateSet > &	rSubsets,
		std::vector< Idx > &	rNewIndices
	)

Definition at line 375 of file cfl_statemin.cpp.

StringSubstitute()

FAUDES_API std::string faudes::StringSubstitute	(	const std::string &	rString,
		const std::string &	rFrom,
		const std::string &	rTo
	)

Substitute globally in string.

Parameters

rString	Source string to substitute
rFrom	String to match
rTo	Replacement to fill in

Returns

Result string

Definition at line 111 of file cfl_utils.cpp.

SupConClosed()

FAUDES_API void faudes::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.

Implementation of SupConClosed.

See "C.G CASSANDRAS AND S. LAFORTUNE. Introduction to Discrete Event Systems. Kluwer, 1999." for base algorithm.

This version sets up a "composition map" provided as a reference parameter. The map is restricted such that its range matches the resulting supervisor.

Parameters

rPlantGen	Plant Generator
rCAlph	Controllable events
rSpecGen	Specification Generator
rReverseCompositionMap	std::map< std::pair<Idx,Idx>, Idx> as in the parallel composition function
rResGen	Reference to resulting Generator, the minimal restrictive supervisor

Exceptions

Exception

alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 793 of file syn_supcon.cpp.

SupConClosedUnchecked()

FAUDES_API void faudes::SupConClosedUnchecked	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		Generator &	rSupCandGen
	)

Supremal Controllable Sublangauge (internal function)

Indentifies and deletes "critical" states in the supervisor candidate, in order to achieve controllability. This version of SupConClosed performs no consistency test of the given parameter. In order to obtain indeed the supremal sublanguage, the state space of the candidate must be rich enough to discriminate plant states. This can be done by e.g. setting up the candidate SupConParallel.

In general, the result is blocking.

Parameters

rPlantGen	Plant generator
rCAlph	Controllable events
rSupCandGen	Supervisor candidate generator

Definition at line 57 of file syn_supcon.cpp.

SupConNBUnchecked()

FAUDES_API void faudes::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)

This version of SupConNB performs no consistency test of the given parameter. It set's up a "composition map" as in the parallel composition, however, the map may still contain states that have been removed from the result to obtain controllability.

Parameters

rPlantGen	Plant Generator
rCAlph	Controllable events
rSpecGen	Specification Generator
rReverseCompositionMap	std::map< std::pair<Idx,Idx>, Idx> as in the parallel composition function
rResGen	Reference to resulting System, the minimal restrictive nonblocking supervisor

Exceptions

Exception

alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 586 of file syn_supcon.cpp.

SupConNormClosed()

FAUDES_API void faudes::SupConNormClosed	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

rti wrapper

Definition at line 684 of file syn_supnorm.cpp.

SupConNormClosedUnchecked()

FAUDES_API void faudes::SupConNormClosedUnchecked	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const EventSet &	rOAlph,
		Generator &	rObserverGen,
		Generator &	rSupCandGen
	)

Supremal Normal Controllable Sublangauge (internal function)

Indentifies and deletes conflicting transitions to obtain a controllable and prefix-normal sublanguage. This function is a bit experimental it depends on various unverified preconditions and conjectures – use only after careful code-review. The completely independent implementation SupNormConClosed should be fine

Conditions

• controllabel events as specified explicitly must be a subset of the observable events
• L(H) <= L(G)
• stateset of H must be sufficiently rich to discriminate states in G (e.g. initialise by H:=H' x G)
• H_obs must be "a" observer automaton for H w.r.t. observable events (e.g. initialize with p_inv p H)

Parameters

rPlantGen	Plant generator G
rCAlph	Controllable events
rOAlph	Observable events
rObserverGen	Observer H_obs
rSupCandGen	Closed-loop candidate H

Definition at line 480 of file syn_supnorm.cpp.

SupConNormNB()

FAUDES_API void faudes::SupConNormNB	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

rti wrapper

Definition at line 706 of file syn_supnorm.cpp.

SupConProduct()

FAUDES_API void faudes::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)

Composition stops at transition paths that violate the specification by uncontrollable plant transitions.

This internal function performs no consistency test of the given parameter. It set's up a "composition map" as in the product composition, however, the map may still contain states that have been removed from the result to obtain controllability.

Parameters

rPlantGen	Plant Generator
rCAlph	Uncontrollable Events
rSpecGen	Specification Generator
rReverseCompositionMap	std::map< std::pair<Idx,Idx>, Idx> as in the parallel composition function
rResGen	Reference to resulting Generator, the less restrictive supervisor

Definition at line 386 of file syn_supcon.cpp.

SupNorm()

FAUDES_API void faudes::SupNorm	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

rti wrapper

Definition at line 639 of file syn_supnorm.cpp.

SupNormClosed()

FAUDES_API void faudes::SupNormClosed	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

rti wrapper

Definition at line 661 of file syn_supnorm.cpp.

SupNormSP()

bool faudes::SupNormSP	(	Generator &	rL,
		const EventSet &	rOAlph,
		const Generator &	rK,
		Generator &	rResult
	)

Definition at line 32 of file hio_functions.cpp.

SupPrefixClosed()

FAUDES_API bool faudes::SupPrefixClosed	(	const Generator &	rK,
		Generator &	rResult
	)

SupPrefixClosed: supremal closed sublanguage of K by cancelling all tranistions leading to a non-marked state.

Returns false on empty result. todo: implement test routines, verify correctness

Parameters

rK	marks the (not necessarily closed) language K=Lm(rK)
rResult	generates and marks the supremal closed sublanguage, where L(rResult)=Lm(rResult)

Returns

true for nonempty result

Exceptions

Exception

todo: check determinism of rK

Definition at line 419 of file syn_supnorm.cpp.

SupRelativelyPrefixClosedUnchecked()

FAUDES_API void faudes::SupRelativelyPrefixClosedUnchecked	(	const Generator &	rPlantGen,
		const Generator &	rSpecGen,
		std::map< std::pair< Idx, Idx >, Idx > &	rCompositionMap,
		Generator &	rResGen
	)

Supremal Relatively Closed Sublanguage (internal function)

This version of SupRelativelyPrefixClosed performs no consistency test of the given parameter. It set's up a "composition map" as in the parallel composition, however, the map may still contain states that have been removed from the result to obtain controllability.

Parameter restrictions: both generators must be deterministic and have the same alphabet.

Parameters

rPlantGen	Plant G
rSpecGen	Specification Generator E
rCompositionMap	Record parallel composition state mapping
rResGen	Reference to resulting Generator,

Definition at line 292 of file syn_functions.cpp.

SupTconNBUnchecked()

void faudes::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
	)

Definition at line 211 of file syn_tsupcon.cpp.

SupTconUnchecked()

void faudes::SupTconUnchecked	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const EventSet &	rFAlph,
		const EventSet &	rPAlph,
		const EventSet &	rCPAlph,
		Generator &	rSupCandGen
	)

Definition at line 40 of file syn_tsupcon.cpp.

SwigCastPtr()

void* faudes::SwigCastPtr	(	void *	ptr,
		swig_type_info *	from,
		swig_type_info *	ty
	)

Definition at line 86 of file lbp_function.cpp.

SwigUserData()

swig_lua_userdata* faudes::SwigUserData	(	lua_State *	L,
		int	index
	)

Definition at line 117 of file lbp_function.cpp.

syncSend()

int faudes::syncSend	(	int	dest,
		const char *	data,
		int	len,
		int	flag
	)

Definition at line 248 of file iop_simplenet.cpp.

TestMergibility()

bool faudes::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
	)

Definition at line 72 of file syn_supreduce.cpp.

TestProtocol() [1/6]

FAUDES_API void faudes::TestProtocol	(	const std::string &	rMessage,
		bool	data
	)

Test Protocol.

Specialized version for boolean test data. See also TestProtocol(const std::string&, const Type&, bool);

Parameters

rMessage	Informal identifyer of the test
data	Test data

Definition at line 553 of file cfl_utils.cpp.

TestProtocol() [2/6]

FAUDES_API void faudes::TestProtocol	(	const std::string &	rMessage,
		const std::string &	data
	)

Test Protocol.

Specialized version for string data. See also TestProtocol(const std::string&, const Type&, bool);

Parameters

rMessage	Informal identifyer of the test
data	Test data

Definition at line 561 of file cfl_utils.cpp.

TestProtocol() [3/6]

FAUDES_API void faudes::TestProtocol	(	const std::string &	rMessage,
		const Type &	rData,
		bool	core = false
	)

Test Protocol.

This function dumps the specified data to the protocol file for the purpose of later comparison with a refernce value. If the protocol file has not been set up, this function does nothing; see also TestProtocol(const std::string&.

Parameters

rMessage	Informal identifyer of the test
rData	Formal result of the test case
core	Whether to record full token io or statistics only.

Definition at line 543 of file cfl_utils.cpp.

TestProtocol() [4/6]

FAUDES_API void faudes::TestProtocol	(	const std::string &	rMessage,
		long int	data
	)

Test Protocol.

Specialized version for integer test data. See also TestProtocol(const std::string&, const Type&, bool);

Parameters

rMessage	Informal identifyer of the test
data	Test data

Definition at line 557 of file cfl_utils.cpp.

TestProtocol() [5/6]

FAUDES_API std::string faudes::TestProtocol

(

const std::string &

rSource

)

Test Protocol.

Sets the filename for the test protocol by

• removing any path specififucation,
• replacing "." by "_",
• appending ".prot", and finaly
• prepending "tmp_". The function returns the filename except for the "tmp_" prefix. The latter is considered the nominal protocol output (aka reference protocol).

Note: only the first invocation of this functions actually sets the protocol file. Further invocations are ignored, but can be used to query the reference protocol.

Parameters

rSource

Source file to protocol

Returns

Filename with nominal protocol.

Definition at line 518 of file cfl_utils.cpp.

TestProtocol() [6/6]

FAUDES_API bool faudes::TestProtocol

(

void

)

Test Protocol.

Perform a comparison of the recent protocol file and the corresponding reference. Returns true if the test passes.

Note: this function closes the current protocol.

Returns

True <=> test past

Definition at line 567 of file cfl_utils.cpp.

TimeInvariantAbstraction()

void faudes::TimeInvariantAbstraction	(	const Experiment &	exp,
		Generator &	res
	)

TimeVariantAbstraction()

void faudes::TimeVariantAbstraction	(	const Experiment &	exp,
		Generator &	res
	)

ToIdx()

FAUDES_API Idx faudes::ToIdx

(

const std::string &

rString

)

Convert a string to Idx.

Parameters

rString

string to convert

Returns

Idx

Exceptions

Idx	overflow (id 600)

Definition at line 100 of file cfl_utils.cpp.

topoSort()

bool faudes::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

Definition at line 419 of file cfl_bisimcta.cpp.

ToStringFloat()

FAUDES_API std::string faudes::ToStringFloat

(

Float

number

)

float to string

Parameters

number

double

Returns

string

Definition at line 64 of file cfl_utils.cpp.

ToStringInteger()

FAUDES_API std::string faudes::ToStringInteger

(

Int

number

)

integer to string

Parameters

number

integer

Returns

string

Definition at line 43 of file cfl_utils.cpp.

ToStringInteger16()

FAUDES_API std::string faudes::ToStringInteger16

(

Int

number

)

integer to string base 16

Parameters

number

integer

Returns

string

Definition at line 54 of file cfl_utils.cpp.

TransSpec()

void faudes::TransSpec	(	const GeneratorVector &	rSpecGenVec,
		const EventSet &	rGUncAlph,
		GeneratorVector &	rResGenVec
	)

translate specification into plant

Parameters

rSpecGenVec	specification generator-vector
rGUncAlph	global uncontrollable events
rResGenVec	synthesis-buffer

Definition at line 649 of file syn_compsyn.cpp.

TraverseUncontrollableBackwards()

FAUDES_API void faudes::TraverseUncontrollableBackwards	(	const EventSet &	rCAlph,
		TransSetX2EvX1 &	rtransrel,
		StateSet &	rCriticalStates,
		Idx	current
	)

Helper function for IsControllable.

The state given as "current" is considered critical. Itself and all uncontrollable predecessor states are added to the set "rCriticalStates".

Parameters

rCAlph	Set of controllable events
rtransrel	Reverse sorted transition relation
rCriticalStates	Set of critical states in composition generator
current	Current state

Definition at line 847 of file syn_supcon.cpp.

TrimNonIndicatorTracesOfGd() [1/2]

void faudes::TrimNonIndicatorTracesOfGd	(	System &	rGd,
		const Diagnoser &	rGobs,
		const Idx	rFailureType,
		const EventSet &	rIndicatorEvents,
		const map< pair< Idx, Idx >, Idx > &	rReverseCompositionMap
	)

Definition at line 606 of file diag_eventdiagnosis.cpp.

TrimNonIndicatorTracesOfGd() [2/2]

FAUDES_API void faudes::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.

Parameters

rGd	Input generator G_d which will be prunded.
rGobs	Generator G_o (containing failure label information).
rFailureType	Failure type index.
rIndicatorEvents	Set of indicator events.
rReverseCompositionMap	Mapping of G_d states with G_o states.

TrimNonIndicatorTracesOfGdRecursive() [1/2]

void faudes::TrimNonIndicatorTracesOfGdRecursive	(	System &	rGd,
		const Diagnoser &	rGobs,
		const Idx	rFailureType,
		const EventSet &	rIndicatorEvents,
		map< Idx, pair< Idx, Idx > > &	rCompositionMap,
		Idx	state,
		StateSet &	rStatesDone
	)

Definition at line 618 of file diag_eventdiagnosis.cpp.

TrimNonIndicatorTracesOfGdRecursive() [2/2]

FAUDES_API void faudes::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().

Parse through active transition set of the current state and delete transitions if occurring event is not an indicator event or there did not occur a failure before the indicator.

Parameters

rGd	Input generator G_d which will be pruned.
rGobs	Generator G_o (containing failure label information).
rFailureType	Failure type index.
rIndicatorEvents	Set of indicator events.
rCompositionMap	Inverted mapping of G_d states with G_o states.
state	Current state.
rStatesDone	States that have been processed already.

UserData() [1/2]

Parma_Polyhedra_Library::C_Polyhedron& faudes::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

Definition at line 119 of file hyb_compute.cpp.

UserData() [2/2]

Parma_Polyhedra_Library::C_Polyhedron& faudes::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

Definition at line 22 of file hyb_compute.cpp.

VersionString()

FAUDES_API std::string faudes::VersionString

(

)

Return FAUDES_VERSION as std::string.

Returns

std::string with FAUDES_VERSION

Definition at line 131 of file cfl_utils.cpp.

YclessScc()

bool faudes::YclessScc	(	const Generator &	rGen,
		const EventSet &	rYc,
		std::set< StateSet > &	rSccSet
	)

Definition at line 1803 of file hio_functions.cpp.

Variable Documentation

faudes_lastline

FAUDES_API std::string faudes::faudes_lastline

extern

gBreakFnct

bool(* faudes::gBreakFnct) (void)=0 ( void  )

static

Definition at line 630 of file cfl_utils.cpp.

gRti1RegisterSignalDeviceEventSet

AutoRegisterType< TaNameSet<AttributeSignalEvent> > faudes::gRti1RegisterSignalDeviceEventSet("SignalDeviceEventSet")

(

"SignalDeviceEventSet"

)

gRti1XElementTagSignalDeviceEventSet

AutoRegisterXElementTag< TaNameSet<AttributeSignalEvent> > faudes::gRti1XElementTagSignalDeviceEventSet("SignalDeviceEventSet", "Event")	(	"SignalDeviceEventSet"	,
		"Event"
	)

gRtiRegisterDeviceContainer

volatile AutoRegisterType<xDevice> faudes::gRtiRegisterDeviceContainer("DeviceContainer") ( "DeviceContainer"  )

static

gRtiRegisterSimplenetDevice

AutoRegisterType<nDevice> faudes::gRtiRegisterSimplenetDevice("SimplenetDevice")

(

"SimplenetDevice"

)

gRtiRegisterSpiDevice

AutoRegisterType<mbDevice> faudes::gRtiRegisterSpiDevice("ModbusDevice")

(

"ModbusDevice"

)

gTestProtocolFr

std::string faudes::gTestProtocolFr

Definition at line 515 of file cfl_utils.cpp.

gTestProtocolTw

TokenWriter* faudes::gTestProtocolTw =NULL

Definition at line 514 of file cfl_utils.cpp.

ran_initialized

int faudes::ran_initialized = 0

static

Definition at line 31 of file sp_random.cpp.

ran_seed

long faudes::ran_seed[STREAMS] = {DEFAULT}

static

Definition at line 29 of file sp_random.cpp.

ran_stream

int faudes::ran_stream = 0

static

Definition at line 30 of file sp_random.cpp.

TcGenerator< AttributeVoid, AttributeVoid, AttributeCFlags, AttributeVoid >

template class FAUDES_API faudes::TcGenerator< AttributeVoid, AttributeVoid, AttributeCFlags, AttributeVoid >

Definition at line 36 of file cfl_cgenerator.cpp.