Detailed Description

Finite fragment of a computation tree.

An Experiment represents a finite fragment of a computation tree of. Formaly, an Experiment avoids an explicit reference to the underlying state set of the transition system; i.e., each node represents the finite sequence of events generated when traversing from the root the respective node. Experiments are used to construct deterministic finite state abstractions.

Although an explicit reference to the underlying state set is avoided, implictly each node is associated with the set of state in which the transition could possibly reside after execution of the respective finite string. These sets of CompatibleStates can be computed by an iterative forward reachability analysis, where the choice of available computational procedures depends of the class of transition systems under consideration.

Definition at line 44 of file hyb_experiment.h.

#include <hyb_experiment.h>

Classes
class	Node
	Node record to form a tree. More...

Public Member Functions
	Experiment (const EventSet &alph)

	~Experiment (void)

void	InitialStates (CompatibleStates *istates)

void	Clear (void)

Idx	Size (void) const

const EventSet &	Alphabet (void) const

int	Cost (void) const

void	SWrite (void) const

void	DWrite (void) const

void	DWrite (Idx nid) const

Idx	Root (void) const
	Navigate tree This interface is intended for external use. More...

EventSet	EnabledEvents (Idx nid) const

Idx	SuccessorNode (Idx nid, Idx ev) const

bool	IsLeave (Idx nid) const

bool	IsLock (Idx nid) const

Idx	Find (const std::deque< Idx > &seq) const

std::deque< Idx >	Sequence (Idx nid) const

const IndexSet &	Leaves () const

const CompatibleStates *	States (Idx nid) const
	Access compatible states (note: implememtation dependant data type) More...

void	RefineAt (Idx idx)

Idx	RefineSequence (const std::deque< Idx > &seq)

void	RefineUniformly (unsigned int depth)

Protected Types
typedef std::map< Idx, Node * >::const_iterator	Iterator

Protected Member Functions
Idx &	Index (Node *node)
	Node related methods, hosted by Experiment for convenience. More...

const Idx &	Index (const Node *node) const

Node *&	Parent (Node *node)

Node *const &	Parent (const Node *node) const

Idx &	RecEvent (Node *node)

const Idx &	RecEvent (const Node *node) const

Idx &	Depth (Node *node)

const Idx &	Depth (const Node *node) const

std::map< Idx, Node * > &	Children (Node *node)

const std::map< Idx, Node * > &	Children (const Node *node) const

bool	IsLeave (const Node *node) const

Node *	Child (Node *node, Idx ev)

Node *	Insert (Node *parent, Idx ev)
	grow tree More...

CompatibleStates *&	States (Node *node)
	payload access More...

CompatibleStates *const &	States (const Node *node) const

bool &	IsLock (Node *node)

const bool &	IsLock (const Node *node) const

Node *	NodePtr (Idx idx) const
	get node ptr by index (for API wrappers) More...

Protected Attributes
Node *	mpRoot
	core experiment data: have root and track all nodes by index More...

std::map< Idx, Node * >	mNodeMap

IndexSet	mLeaves

int	mCost

const faudes::EventSet &	rAlphabet
	reference to alphabet More...

Member Typedef Documentation

◆ Iterator

typedef std::map<Idx, Node*>::const_iterator faudes::Experiment::Iterator

protected

Definition at line 96 of file hyb_experiment.h.

Constructor & Destructor Documentation

◆ Experiment()

Experiment::Experiment ( const EventSet & alph )

Definition at line 17 of file hyb_experiment.cpp.

◆ ~Experiment()

Experiment::~Experiment ( void )

Definition at line 25 of file hyb_experiment.cpp.

Member Function Documentation

◆ Alphabet()

const EventSet & Experiment::Alphabet ( void ) const

Definition at line 61 of file hyb_experiment.cpp.

◆ Child()

Node* faudes::Experiment::Child	(	Node *	node,
		Idx	ev
	)

inlineprotected

Definition at line 150 of file hyb_experiment.h.

◆ Children() [1/2]

const std::map< Idx, Node*>& faudes::Experiment::Children ( const Node * node ) const

inlineprotected

Definition at line 146 of file hyb_experiment.h.

◆ Children() [2/2]

std::map< Idx, Node*>& faudes::Experiment::Children ( Node * node )

inlineprotected

Definition at line 144 of file hyb_experiment.h.

◆ Clear()

void Experiment::Clear ( void )

Definition at line 31 of file hyb_experiment.cpp.

◆ Cost()

int faudes::Experiment::Cost ( void ) const

inline

Definition at line 55 of file hyb_experiment.h.

◆ Depth() [1/2]

const Idx& faudes::Experiment::Depth ( const Node * node ) const

inlineprotected

Definition at line 142 of file hyb_experiment.h.

◆ Depth() [2/2]

Idx& faudes::Experiment::Depth ( Node * node )

inlineprotected

Definition at line 140 of file hyb_experiment.h.

◆ DWrite() [1/2]

void Experiment::DWrite ( Idx nid ) const

Definition at line 157 of file hyb_experiment.cpp.

◆ DWrite() [2/2]

void Experiment::DWrite ( void ) const

Definition at line 194 of file hyb_experiment.cpp.

◆ EnabledEvents()

EventSet Experiment::EnabledEvents ( Idx nid ) const

Definition at line 70 of file hyb_experiment.cpp.

◆ Find()

Idx Experiment::Find ( const std::deque< Idx > & seq ) const

Definition at line 128 of file hyb_experiment.cpp.

◆ Index() [1/2]

const Idx& faudes::Experiment::Index ( const Node * node ) const

inlineprotected

Definition at line 130 of file hyb_experiment.h.

◆ Index() [2/2]

Idx& faudes::Experiment::Index ( Node * node )

inlineprotected

Node related methods, hosted by Experiment for convenience.

tree member access

Definition at line 128 of file hyb_experiment.h.

◆ InitialStates()

void Experiment::InitialStates ( CompatibleStates * istates )

Definition at line 50 of file hyb_experiment.cpp.

◆ Insert()

Node* faudes::Experiment::Insert	(	Node *	parent,
		Idx	ev
	)

inlineprotected

grow tree

Definition at line 157 of file hyb_experiment.h.

◆ IsLeave() [1/2]

bool faudes::Experiment::IsLeave ( const Node * node ) const

inlineprotected

Definition at line 148 of file hyb_experiment.h.

◆ IsLeave() [2/2]

bool Experiment::IsLeave ( Idx nid ) const

Definition at line 90 of file hyb_experiment.cpp.

◆ IsLock() [1/3]

const bool& faudes::Experiment::IsLock ( const Node * node ) const

inlineprotected

Definition at line 177 of file hyb_experiment.h.

◆ IsLock() [2/3]

bool Experiment::IsLock ( Idx nid ) const

Definition at line 102 of file hyb_experiment.cpp.

◆ IsLock() [3/3]

bool& faudes::Experiment::IsLock ( Node * node )

inlineprotected

Definition at line 175 of file hyb_experiment.h.

◆ Leaves()

const IndexSet & Experiment::Leaves ( void ) const

Definition at line 240 of file hyb_experiment.cpp.

◆ NodePtr()

Node* faudes::Experiment::NodePtr ( Idx idx ) const

inlineprotected

get node ptr by index (for API wrappers)

Definition at line 181 of file hyb_experiment.h.

◆ Parent() [1/2]

Node* const& faudes::Experiment::Parent ( const Node * node ) const

inlineprotected

Definition at line 134 of file hyb_experiment.h.

◆ Parent() [2/2]

Node*& faudes::Experiment::Parent ( Node * node )

inlineprotected

Definition at line 132 of file hyb_experiment.h.

◆ RecEvent() [1/2]

const Idx& faudes::Experiment::RecEvent ( const Node * node ) const

inlineprotected

Definition at line 138 of file hyb_experiment.h.

◆ RecEvent() [2/2]

Idx& faudes::Experiment::RecEvent ( Node * node )

inlineprotected

Definition at line 136 of file hyb_experiment.h.

◆ RefineAt()

void Experiment::RefineAt ( Idx idx )

Definition at line 251 of file hyb_experiment.cpp.

◆ RefineSequence()

Idx Experiment::RefineSequence ( const std::deque< Idx > & seq )

Definition at line 313 of file hyb_experiment.cpp.

◆ RefineUniformly()

void Experiment::RefineUniformly ( unsigned int depth )

Definition at line 294 of file hyb_experiment.cpp.

◆ Root()

Idx Experiment::Root ( void ) const

Navigate tree This interface is intended for external use.

All methods throw an exception when accessing a non-existent node.

Definition at line 67 of file hyb_experiment.cpp.

◆ Sequence()

std::deque< Idx > Experiment::Sequence ( Idx nid ) const

Definition at line 139 of file hyb_experiment.cpp.

◆ Size()

Idx Experiment::Size ( void ) const

Definition at line 57 of file hyb_experiment.cpp.

◆ States() [1/3]

CompatibleStates* const& faudes::Experiment::States ( const Node * node ) const

inlineprotected

Definition at line 173 of file hyb_experiment.h.

◆ States() [2/3]

const CompatibleStates * Experiment::States ( Idx nid ) const

Access compatible states (note: implememtation dependant data type)

Definition at line 111 of file hyb_experiment.cpp.

◆ States() [3/3]

CompatibleStates*& faudes::Experiment::States ( Node * node )

inlineprotected

payload access

Definition at line 171 of file hyb_experiment.h.

◆ SuccessorNode()

Idx Experiment::SuccessorNode	(	Idx	nid,
		Idx	ev
	)		const

Definition at line 83 of file hyb_experiment.cpp.

◆ SWrite()

void Experiment::SWrite ( void ) const

Definition at line 205 of file hyb_experiment.cpp.

Member Data Documentation

◆ mCost

int faudes::Experiment::mCost

protected

Definition at line 98 of file hyb_experiment.h.

◆ mLeaves

IndexSet faudes::Experiment::mLeaves

protected

Definition at line 97 of file hyb_experiment.h.

◆ mNodeMap

std::map< Idx , Node* > faudes::Experiment::mNodeMap

protected

Definition at line 95 of file hyb_experiment.h.

◆ mpRoot

Node* faudes::Experiment::mpRoot

protected

core experiment data: have root and track all nodes by index

Definition at line 94 of file hyb_experiment.h.

◆ rAlphabet

const faudes::EventSet& faudes::Experiment::rAlphabet

protected

reference to alphabet

Definition at line 101 of file hyb_experiment.h.

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

Detailed Description

Classes

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Member Typedef Documentation

◆ Iterator

Constructor & Destructor Documentation

◆ Experiment()

◆ ~Experiment()

Member Function Documentation

◆ Alphabet()

◆ Child()

◆ Children() [1/2]

◆ Children() [2/2]

◆ Clear()

◆ Cost()

◆ Depth() [1/2]

◆ Depth() [2/2]

◆ DWrite() [1/2]

◆ DWrite() [2/2]

◆ EnabledEvents()

◆ Find()

◆ Index() [1/2]

◆ Index() [2/2]

◆ InitialStates()

◆ Insert()

◆ IsLeave() [1/2]

◆ IsLeave() [2/2]

◆ IsLock() [1/3]

◆ IsLock() [2/3]

◆ IsLock() [3/3]

◆ Leaves()

◆ NodePtr()

◆ Parent() [1/2]

◆ Parent() [2/2]

◆ RecEvent() [1/2]

◆ RecEvent() [2/2]

◆ RefineAt()

◆ RefineSequence()

◆ RefineUniformly()

◆ Root()

◆ Sequence()

◆ Size()

◆ States() [1/3]

◆ States() [2/3]

◆ States() [3/3]

◆ SuccessorNode()

◆ SWrite()

Member Data Documentation

◆ mCost

◆ mLeaves

◆ mNodeMap

◆ mpRoot

◆ rAlphabet