Detailed Description

Definition at line 132 of file cfl_bisimulation.cpp.

Classes
struct	State

Public Member Functions
	Bisimulation (const Generator &g)
	Contructor: keep a reference to the generator and initialize the partition and the W-Tree to represent the universal equivalence relation, i.e. More...

	~Bisimulation (void)
	Destructor. More...

void	writeW (void)
	Write W-tree to console. More...

void	writeRo (void)
	Write the set of equivalence classes to console. More...

void	refine (void)
	Perform fixpoint iteration to obtain the coarset bisimulation relation. More...

void	partition (std::map< Idx, Idx > &rMapStateToPartition, Generator &rGenPart)
	Extract output generator that represents the resulting quotient automaton. More...

void	partition (std::map< Idx, Idx > &rMapStateToPartition)
	Extract the coarsest quasi-congruence as an STL map (need to invoke refine() befor) More...

void	partition (std::list< StateSet > &rPartition)
	Extract the coarsest quasi-congruence as a list of equivalence classes. More...

Private Member Functions
Pnode *	newnode ()
	insert new node to W-tree (empty stateset) note: this method only cares about indexing, and initialisation of node members note: cross references are left to the caller More...

void	computeInfoMaps (Pnode &node, Pnode pSmallerPart, Pnode pLargerPart, Idx ev)
	compute info-maps for two cosets pSmallerPart and pLargerpart. More...

void	computeInfoMap (Pnode &B, Pnode &Bstates, Idx ev, vector< Idx > &tb)
	Compute info-map for coset B. More...

void	setInfoMap (Pnode &BSmaller, Pnode &BLarger, Idx ev)
	Alternative: compute and set info-map to state data — this is for testing/debugging only, it did neither buy nor cost relevant performance. More...

void	invImage (Pnode &B, Pnode &Bstates, Idx ev, vector< Idx > &tb)

bool	stateLeadsToPartition (Idx state, Pnode &node, Idx ev)
	Test wehther a state has an ev-transitions into the specified coset. More...

void	partitionClass (Pnode &B)
	Refine current partition with respect to coset B. More...

void	partitionSplitter (Pnode &B)
	Refine current partition with respect to partition B and make use of the fact that the current partition is stable with respect to the parent coset of B (compound splitter). More...

void	writeNode (Pnode &node)
	Function for recursively plotting the W-tree to console [debugging]. More...

Private Attributes
vector< State >	states

vector< Idx >	events

const Generator *	gen
	Keep reference to Automaton. More...

Idx	nxidx
	Counter to assign a unique index to each node [debugging/cosmetic only]. More...

std::vector< Pnode * >	W
	W-tree. More...

std::set< Pnode * >	ro
	set of nodes that form current partition ro (i.e. More...

std::set< Pnode * >	roDividers
	set of nodes that can possibly split classes in ro More...

Constructor & Destructor Documentation

◆ Bisimulation()

faudes::Bisimulation::Bisimulation ( const Generator & g )

Contructor: keep a reference to the generator and initialize the partition and the W-Tree to represent the universal equivalence relation, i.e.

every two states are equivalent.

Parameters

g	Original generator

Definition at line 335 of file cfl_bisimulation.cpp.

◆ ~Bisimulation()

faudes::Bisimulation::~Bisimulation ( void )

Destructor.

Definition at line 383 of file cfl_bisimulation.cpp.

Member Function Documentation

◆ computeInfoMap()

void faudes::Bisimulation::computeInfoMap	(	Pnode &	B,
		Pnode &	Bstates,
		Idx	ev,
		vector< Idx > &	tb
	)

private

Compute info-map for coset B.

Parameters

B	Coset for which the info-map is computed
Bstates	Node to provide states of B
ev	Event to use
tb	sorted vector containing all the states that have an ev-transition into coset B

Definition at line 904 of file cfl_bisimulation.cpp.

◆ computeInfoMaps()

void faudes::Bisimulation::computeInfoMaps	(	Pnode &	node,
		Pnode *	pSmallerPart,
		Pnode *	pLargerPart,
		Idx	ev
	)

private

compute info-maps for two cosets pSmallerPart and pLargerpart.

the current partition must be stable wrt the common parent the both parts
the smaller part and larger part info maps must be initialized empty and by parent, resp.

Parameters

node	Node to provide states of pSmallerPart (call with pSmallerPart)
pSmallerPart	Child coset P1 of P with smaller number of states
pLargerPart	Child coset P2 of P with larger number of states
ev	Event

Definition at line 654 of file cfl_bisimulation.cpp.

◆ invImage()

void faudes::Bisimulation::invImage	(	Pnode &	B,
		Pnode &	Bstates,
		Idx	ev,
		vector< Idx > &	tb
	)

private

Definition at line 1013 of file cfl_bisimulation.cpp.

◆ newnode()

Pnode * faudes::Bisimulation::newnode ( void )

private

insert new node to W-tree (empty stateset) note: this method only cares about indexing, and initialisation of node members note: cross references are left to the caller

Definition at line 392 of file cfl_bisimulation.cpp.

◆ partition() [1/3]

void faudes::Bisimulation::partition ( std::list< StateSet > & rPartition )

Extract the coarsest quasi-congruence as a list of equivalence classes.

(need to invoke refine() befor)

Parameters

rPartition List of equivcalent sets ogf states

Definition at line 1175 of file cfl_bisimulation.cpp.

◆ partition() [2/3]

void faudes::Bisimulation::partition ( std::map< Idx, Idx > & rMapStateToPartition )

Extract the coarsest quasi-congruence as an STL map (need to invoke refine() befor)

Parameters

rMapStateToPartition Maps each state to its equivalence class

Definition at line 1149 of file cfl_bisimulation.cpp.

◆ partition() [3/3]

void faudes::Bisimulation::partition	(	std::map< Idx, Idx > &	rMapStateToPartition,
		Generator &	rGenPart
	)

Extract output generator that represents the resulting quotient automaton.

(need to invoke refine() befor)

Parameters

rMapStateToPartition	Maps each state to its equivalence class
rGenPart	Generator representing the result of the computation. Each state corresponds to an euivalence class

Definition at line 1081 of file cfl_bisimulation.cpp.

◆ partitionClass()

void faudes::Bisimulation::partitionClass ( Pnode & B )

private

Refine current partition with respect to coset B.

Parameters

B Coset

Definition at line 785 of file cfl_bisimulation.cpp.

◆ partitionSplitter()

void faudes::Bisimulation::partitionSplitter ( Pnode & B )

private

Refine current partition with respect to partition B and make use of the fact that the current partition is stable with respect to the parent coset of B (compound splitter).

Parameters

B Coset

Definition at line 412 of file cfl_bisimulation.cpp.

◆ refine()

void faudes::Bisimulation::refine ( void )

Perform fixpoint iteration to obtain the coarset bisimulation relation.

Definition at line 1048 of file cfl_bisimulation.cpp.

◆ setInfoMap()

void faudes::Bisimulation::setInfoMap	(	Pnode &	BSmaller,
		Pnode &	BLarger,
		Idx	ev
	)

private

Alternative: compute and set info-map to state data — this is for testing/debugging only, it did neither buy nor cost relevant performance.

Definition at line 956 of file cfl_bisimulation.cpp.

◆ stateLeadsToPartition()

bool faudes::Bisimulation::stateLeadsToPartition	(	Idx	state,
		Pnode &	node,
		Idx	ev
	)

private

Test wehther a state has an ev-transitions into the specified coset.

Parameters

state	State to be examined
node	Coset
ev	Event

Definition at line 724 of file cfl_bisimulation.cpp.

◆ writeNode()

void faudes::Bisimulation::writeNode ( Pnode & node )

private

Function for recursively plotting the W-tree to console [debugging].

Parameters

node Coset

Definition at line 1203 of file cfl_bisimulation.cpp.

◆ writeRo()

void faudes::Bisimulation::writeRo ( void )

Write the set of equivalence classes to console.

Definition at line 1246 of file cfl_bisimulation.cpp.

◆ writeW()

void faudes::Bisimulation::writeW ( void )

Write W-tree to console.

Definition at line 1195 of file cfl_bisimulation.cpp.

Member Data Documentation

◆ events

vector<Idx> faudes::Bisimulation::events

private

Definition at line 214 of file cfl_bisimulation.cpp.

◆ gen

const Generator* faudes::Bisimulation::gen

private

Keep reference to Automaton.

Definition at line 220 of file cfl_bisimulation.cpp.

◆ nxidx

Idx faudes::Bisimulation::nxidx

private

Counter to assign a unique index to each node [debugging/cosmetic only].

Definition at line 225 of file cfl_bisimulation.cpp.

◆ ro

std::set<Pnode*> faudes::Bisimulation::ro

private

set of nodes that form current partition ro (i.e.

leaves of W)

Definition at line 245 of file cfl_bisimulation.cpp.

◆ roDividers

std::set<Pnode*> faudes::Bisimulation::roDividers

private

set of nodes that can possibly split classes in ro

Definition at line 250 of file cfl_bisimulation.cpp.

◆ states

vector<State> faudes::Bisimulation::states

private

Definition at line 213 of file cfl_bisimulation.cpp.

◆ W

std::vector<Pnode*> faudes::Bisimulation::W

private

W-tree.

Contains all blocks ever created [required for destruction]

Definition at line 230 of file cfl_bisimulation.cpp.

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

cfl_bisimulation.cpp

Detailed Description

Classes

Public Member Functions

Private Member Functions

Private Attributes

Constructor & Destructor Documentation

◆ Bisimulation()

◆ ~Bisimulation()

Member Function Documentation

◆ computeInfoMap()

◆ computeInfoMaps()

◆ invImage()

◆ newnode()

◆ partition() [1/3]

◆ partition() [2/3]

◆ partition() [3/3]

◆ partitionClass()

◆ partitionSplitter()

◆ refine()

◆ setInfoMap()

◆ stateLeadsToPartition()

◆ writeNode()

◆ writeRo()

◆ writeW()

Member Data Documentation

◆ events

◆ gen

◆ nxidx

◆ ro

◆ roDividers

◆ states

◆ W