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 224 of file syn_ctrlpfx.h.

#include <syn_ctrlpfx.h>

Public Member Functions
	MuIteration (const StateSetOperator &rOp)

	~MuIteration (void)

virtual const StateSet &	Domain (void) 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) 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 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::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

◆ 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 202 of file syn_ctrlpfx.cpp.

◆ ~MuIteration()

faudes::MuIteration::~MuIteration ( void )

inline

detsruct

Definition at line 240 of file syn_ctrlpfx.h.

Member Function Documentation

◆ DoEvaluate()

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

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) = X(i) union 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 234 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 229 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 222 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.

Member Data Documentation

◆ mrOp

const StateSetOperator& faudes::MuIteration::mrOp

protected

the base operator to iterate with

Definition at line 277 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]

Member Data Documentation

◆ mrOp