Detailed Description

Mu-iterations on state sets.

Given an opertor on state stes, this class facilitates nested fixpoint iterations as in the mu-calculus. In tis specific class, we implement the mu-iteration, i.e., we seek for the smallest fixpoint.

The implementation is meant for a simple API, we do not care about performance at this stage.

Definition at line 217 of file syn_ctrlpfx.h.

#include <syn_ctrlpfx.h>

Public Member Functions
	MuIteration (const StateSetOperator &rOp)

	~MuIteration (void)

virtual const StateSet &	Domain (void) const

void	Rank (StateSetVector &rArgs, std::map< Idx, int > &rRMap) const

void	Rank (StateSet &rArg, std::map< Idx, int > &rRMap) const

void	Rank (std::map< Idx, int > &rRMap) const

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

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

virtual void	Indent (const std::string &indent) 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

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)

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 StateSetOperator &	mrOp

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::AttrType
static void	Skip (TokenReader &rTr)

Constructor & Destructor Documentation

◆ MuIteration()

faudes::MuIteration::MuIteration ( const StateSetOperator & rOp )

Construct from operator

The last entry of the operator argument becomes the variable we iterate in. The preceeding entries are interpreted ans constant paramters in our scope.

Parameters

rOp	Operator to iterate

Definition at line 195 of file syn_ctrlpfx.cpp.

◆ ~MuIteration()

faudes::MuIteration::~MuIteration ( void )

inline

detsruct

Definition at line 233 of file syn_ctrlpfx.h.

Member Function Documentation

◆ DoEvaluate()

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

protectedvirtual

Implement the mu-iteration to find the smallest fixpoint.

Given the parameter vector rArgs, we append one additional state set X for which we seek a fixpoint of Op(rArgs,X). Effectively we iterate

X(0) = emptyset X(i+1) = Op(rArgs,X(i))

until the fixpoint is achieved.

Parameters

rArgs	Arguments the operator performs on
rRes	Resulting state set

Implements faudes::StateSetOperator.

Definition at line 227 of file syn_ctrlpfx.cpp.

◆ Domain()

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

virtual

Domain

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

Returns: Full state set.

Reimplemented from faudes::StateSetOperator.

Definition at line 222 of file syn_ctrlpfx.cpp.

◆ Indent() [1/3]

void faudes::StateSetOperator::Indent ( void )

virtual

indent (cosmetic)

Reimplemented from faudes::StateSetOperator.

Definition at line 114 of file syn_ctrlpfx.cpp.

◆ Indent() [2/3]

void faudes::MuIteration::Indent ( const std::string & indent ) const

virtual

indent (cosmetic)

Reimplemented from faudes::StateSetOperator.

Definition at line 215 of file syn_ctrlpfx.cpp.

◆ Indent() [3/3]

const std::string & faudes::StateSetOperator::Indent ( void )

virtual

indent (cosmetic)

Reimplemented from faudes::StateSetOperator.

Definition at line 111 of file syn_ctrlpfx.cpp.

◆ Rank() [1/3]

void faudes::MuIteration::Rank	(	StateSet &	rArg,
		std::map< Idx, int > &	rRMap
	)		const

Evaluate opertor on arguments and return ranking

This is a convenience wrapper for Rank addressing operators with orny one argument.

Parameters

rArg	State-set argument the operator performs on
rRMap	Result with rank attached.

Definition at line 302 of file syn_ctrlpfx.cpp.

◆ Rank() [2/3]

void faudes::MuIteration::Rank	(	StateSetVector &	rArgs,
		std::map< Idx, int > &	rRMap
	)		const

Evaluate opertor on arguments and return ranking

The ranking is the loop count at which a state was newly added to the result.

Parameters

rArgs	State-set valued arguments the operator performs on
rRMap	Result with rank attached.

Definition at line 258 of file syn_ctrlpfx.cpp.

◆ Rank() [3/3]

void faudes::MuIteration::Rank ( std::map< Idx, int > & rRMap ) const

Evaluate opertor on arguments and return ranking

This is a convenience wrapper for Rank addressing operators with no arguments.

Parameters

rRMap Result with rank attached.

Definition at line 309 of file syn_ctrlpfx.cpp.

Member Data Documentation

◆ mrOp

const StateSetOperator& faudes::MuIteration::mrOp

protected

the base operator to iterate with

Definition at line 308 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

◆ MuIteration()

◆ ~MuIteration()

Member Function Documentation

◆ DoEvaluate()

◆ Domain()

◆ Indent() [1/3]

◆ Indent() [2/3]

◆ Indent() [3/3]

◆ Rank() [1/3]

◆ Rank() [2/3]

◆ Rank() [3/3]

Member Data Documentation

◆ mrOp