Detailed Description

Operator used for the computation of the controllability prefix.

Definition at line 157 of file syn_ctrlpfx.h.

#include <syn_ctrlpfx.h>

Public Member Functions
	CtrlPfxOperator (const vGenerator &rGenerator, const EventSet &rSigmaCtrl)

	~CtrlPfxOperator ()

virtual const StateSet &	Domain (void) const

Public Member Functions inherited from faudes::StateSetOperator
	StateSetOperator (void)

	StateSetOperator (const StateSetOperator &)=delete

	~StateSetOperator (void)

void	Evaluate (StateSetVector &rArgs, StateSet &rRes) const

void	Evaluate (StateSet &rArg, StateSet &rRes) const

void	Evaluate (StateSet &rRes) const

StateSetVector::Position	ArgCount (void) const

const std::string &	ArgName (StateSetVector::Position pos) const

std::string	ArgStatistics (const StateSetVector &rArgs) const

virtual const std::string &	Indent (void) const

virtual void	Indent (const std::string &indent) const

Public Member Functions inherited from faudes::ExtType
	ExtType (void)

	ExtType (const ExtType &rType)

virtual	~ExtType (void)

const std::string &	Name (void) const

void	Name (const std::string &rName)

virtual const std::string &	TypeName (void) const

virtual void	TypeName (const std::string &rType)

virtual const std::string &	ElementTag (void) const

virtual void	ElementTag (const std::string &rTag)

virtual const std::string &	ElementType (void) const

virtual const TypeDefinition *	TypeDefinitionp (void) const

Type &	operator= (const Type &rSrc)

bool	operator== (const Type &rOther) const

bool	operator!= (const Type &rOther) const

Public Member Functions inherited from faudes::AttrType
	AttrType (void)

	AttrType (const AttrType &rSrc)

virtual	~AttrType (void)

virtual bool	IsDefault (void) const

Type &	operator= (const Type &rSrc)

bool	operator== (const Type &rOther) const

bool	operator!= (const Type &rOther) const

Public Member Functions inherited from faudes::Type
	Type (void)

	Type (const Type &rType)

virtual	~Type (void)

virtual Type *	New (void) const

virtual Type *	Copy (void) const

virtual const Type *	Cast (const Type *pOther) const

virtual void	Clear (void)

virtual Type &	Assign (const Type &rSrc)

Type &	operator= (const Type &rSrc)

virtual bool	Equal (const Type &rOther) const

bool	operator== (const Type &rOther) const

bool	operator!= (const Type &rOther) const

void	Write (const Type *pContext=0) const

void	Write (const std::string &pFileName, const std::string &rLabel="", const Type *pContext=0, std::ios::openmode openmode=std::ios::out\|std::ios::trunc) const

void	Write (const std::string &pFileName, std::ios::openmode openmode) const

void	Write (TokenWriter &rTw, const std::string &rLabel="", const Type *pContext=0) const

virtual void	XWrite (const std::string &pFileName, const std::string &rLabel="", const Type *pContext=0) const

void	XWrite (const Type *pContext=0) const

void	XWrite (TokenWriter &rTw, const std::string &rLabel="", const Type *pContext=0) const

std::string	ToString (const std::string &rLabel="", const Type *pContext=0) const

std::string	ToText (const std::string &rLabel="", const Type *pContext=0) const

void	DWrite (const Type *pContext=0) const

void	DWrite (const std::string &pFileName, const std::string &rLabel="", const Type *pContext=0, std::ios::openmode openmode=std::ios::out\|std::ios::trunc) const

void	DWrite (TokenWriter &rTw, const std::string &rLabel="", const Type *pContext=0) const

void	SWrite (TokenWriter &rTw) const

void	SWrite (void) const

std::string	ToSText (void) const

void	Read (const std::string &rFileName, const std::string &rLabel="", const Type *pContext=0)

void	FromString (const std::string &rString, const std::string &rLabel="", const Type *pContext=0)

void	Read (TokenReader &rTr, const std::string &rLabel="", const Type *pContext=0)

Protected Member Functions
virtual void	DoEvaluate (StateSetVector &rArgs, StateSet &rRes) const

Protected Member Functions inherited from faudes::AttrType
void	DoAssign (const AttrType &rSrc)

bool	DoEqual (const AttrType &rOther) const

Protected Member Functions inherited from faudes::Type
void	DoAssign (const Type &rSrc)

bool	DoEqual (const Type &rOther) const

virtual void	DoRead (TokenReader &rTr, const std::string &rLabel="", const Type *pContext=0)

virtual void	DoWrite (TokenWriter &rTw, const std::string &rLabel="", const Type *pContext=0) const

virtual void	DoXWrite (TokenWriter &rTw, const std::string &rLabel="", const Type *pContext=0) const

virtual void	DoDWrite (TokenWriter &rTw, const std::string &rLabel="", const Type *pContext=0) const

virtual void	DoSWrite (TokenWriter &rTw) const

virtual Token	XBeginTag (const std::string &rLabel="", const std::string &rFallbackLabel="") const

Protected Attributes
const vGenerator &	rGen

EventSet	mSigmaCtrl

const TransSet &	rTransRel

TransSetX2EvX1	mRevTransRel

Protected Attributes inherited from faudes::StateSetOperator
StateSetVector::Position	mArgCount

std::vector< std::string >	mArgNames

std::string	mIndent

Protected Attributes inherited from faudes::ExtType
std::string	mElementType

std::string	mElementTagDef

std::string	mObjectName

Additional Inherited Members
Static Public Member Functions inherited from faudes::StateSetOperator
static void	LogMuNu (bool on)

Static Public Member Functions inherited from faudes::AttrType
static void	Skip (TokenReader &rTr)

Static Protected Attributes inherited from faudes::StateSetOperator
static bool	mLogMuNu

Constructor & Destructor Documentation

◆ CtrlPfxOperator()

faudes::CtrlPfxOperator::CtrlPfxOperator	(	const vGenerator &	rGenerator,
		const EventSet &	rSigmaCtrl
	)

construct

Definition at line 127 of file syn_ctrlpfx.cpp.

◆ ~CtrlPfxOperator()

faudes::CtrlPfxOperator::~CtrlPfxOperator ( )

inline

destruct

Definition at line 165 of file syn_ctrlpfx.h.

Member Function Documentation

◆ DoEvaluate()

void faudes::CtrlPfxOperator::DoEvaluate	(	StateSetVector &	rArgs,
		StateSet &	rRes
	)		const

protectedvirtual

Evaluate opertor on arguments

For the purpose of the controllability prefix, we evalate to

eval([Y,X]) = (pre_exitential(X) union marked_states) intersected with pre_universal_ctrl(Y)

Note: the order of the argument vector matters. The last entry is the iterate in the inner most iteration.

Parameters

rArgs	Argument [Y,X] in that order
rRes	Resulting state set

Implements faudes::StateSetOperator.

Definition at line 147 of file syn_ctrlpfx.cpp.

◆ Domain()

const StateSet & faudes::CtrlPfxOperator::Domain ( void ) const

virtual

Domain

Report the universe of all states, as given by the generator on construction.

Returns: Full state set.

Reimplemented from faudes::StateSetOperator.

Definition at line 142 of file syn_ctrlpfx.cpp.

Member Data Documentation

◆ mRevTransRel

TransSetX2EvX1 faudes::CtrlPfxOperator::mRevTransRel

protected

have a reverse transition relation

Definition at line 208 of file syn_ctrlpfx.h.

◆ mSigmaCtrl

EventSet faudes::CtrlPfxOperator::mSigmaCtrl

protected

set up conbtext references

Definition at line 202 of file syn_ctrlpfx.h.

◆ rGen

const vGenerator& faudes::CtrlPfxOperator::rGen

protected

set up context references

Definition at line 199 of file syn_ctrlpfx.h.

◆ rTransRel

const TransSet& faudes::CtrlPfxOperator::rTransRel

protected

set up context references

Definition at line 205 of file syn_ctrlpfx.h.

The documentation for this class was generated from the following files:

Detailed Description

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Constructor & Destructor Documentation

◆ CtrlPfxOperator()

◆ ~CtrlPfxOperator()

Member Function Documentation

◆ DoEvaluate()

◆ Domain()

Member Data Documentation

◆ mRevTransRel

◆ mSigmaCtrl

◆ rGen

◆ rTransRel