faudes::SOE Class Reference

Classes
struct	Relation
struct	State

Public Member Functions
	SOE (const Generator &rGenOrig, const EventSet &rConAlph, const EventSet &rLocAlph)
	~SOE (void)
void	refine (void)
void	partition (std::map< Idx, Idx > &rMapStateToPartition, Generator &rGenPart)

Private Member Functions
void	initStateMember_Pre ()
void	initStateMember_Pres ()
Pnode *	newnode ()
void	partitionClass (Pnode &B)
void	computeRel (Pnode &B, std::vector< Relation > &relations)
void	computeEquStates (Pnode &B, Relation &rel, std::set< Idx > &tb, std::stack< Pnode * > &todo)
void	relCase_1 (Pnode &B, Relation &rel, set< Idx > &tb, stack< Pnode * > &todo)
void	relCase_2 (Pnode &B, Relation &rel, set< Idx > &tb, stack< Pnode * > &todo)
void	relCase_3 (Pnode &B, Relation &rel, set< Idx > &tb, stack< Pnode * > &todo)
void	relCase_4 (Pnode &B, Relation &rel, set< Idx > &tb, stack< Pnode * > &todo)

Private Attributes
std::vector< State >	states
std::vector< Idx >	events
const Generator *	gen
std::set< Idx >	uncalph
std::set< Idx >	conalph
std::set< Idx >	localph
std::set< Idx >	shaalph
std::set< Idx >	locuncalph
std::set< Idx >	locconalph
std::set< Idx >	shauncalph
std::set< Idx >	shaconalph
Idx	nxidx
std::vector< Pnode * >	W
std::set< Pnode * >	ro
std::set< Pnode * >	roDividers

Detailed Description

Definition at line 73 of file syn_synthequiv.cpp.

Constructor & Destructor Documentation

SOE()

faudes::SOE::SOE	(	const Generator &	rGenOrig,
		const EventSet &	rConAlph,
		const EventSet &	rLocAlph
	)

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

rGenOrig	Original generator
rConAlph	controllable events
rLocAlph	local events

Definition at line 276 of file syn_synthequiv.cpp.

~SOE()

faudes::SOE::~SOE

(

void

)

Destructor

Definition at line 268 of file syn_synthequiv.cpp.

Member Function Documentation

computeEquStates()

void faudes::SOE::computeEquStates ( Pnode &  B, Relation &  rel, std::set< Idx > &  tb, std::stack< Pnode * > &  todo  )

private

collect all states from coset B which are equivalent to the speicified state and determine the related nodes which is possibly to be splitted

Parameters

B	coset
rel	a specified relation
tb	all equivalent states with respect to rel
todo	all related nodes which is possibly to be splitted

Definition at line 622 of file syn_synthequiv.cpp.

computeRel()

void faudes::SOE::computeRel ( Pnode &  B, std::vector< Relation > &  relations  )

private

construct all relations with respect to coset B

Parameters

B	coset
relations	vector of all relations

Definition at line 548 of file syn_synthequiv.cpp.

initStateMember_Pre()

void faudes::SOE::initStateMember_Pre ( )

private

construct 2st Part of Struct "State"

Definition at line 349 of file syn_synthequiv.cpp.

initStateMember_Pres()

void faudes::SOE::initStateMember_Pres ( )

private

construct 3st Part of Struct "State"

Definition at line 401 of file syn_synthequiv.cpp.

newnode()

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

private

insert new node in W-tree with empty stateset

Definition at line 256 of file syn_synthequiv.cpp.

partition()

void faudes::SOE::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 839 of file syn_synthequiv.cpp.

partitionClass()

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

private

refine current partition with respect to coset B

Parameters

B

coset

Definition at line 457 of file syn_synthequiv.cpp.

refine()

void faudes::SOE::refine

(

void

)

Perform fixpoint iteration to obtain the coarset synthesis-observation-equivalence

Definition at line 824 of file syn_synthequiv.cpp.

relCase_1()

void faudes::SOE::relCase_1 ( Pnode &  B, Relation &  rel, set< Idx > &  tb, stack< Pnode * > &  todo  )

private

implementation part for function "computeEquStates" it is organized as follows with respect to various cases:

Definition at line 646 of file syn_synthequiv.cpp.

relCase_2()

void faudes::SOE::relCase_2 ( Pnode &  B, Relation &  rel, set< Idx > &  tb, stack< Pnode * > &  todo  )

private

Definition at line 696 of file syn_synthequiv.cpp.

relCase_3()

void faudes::SOE::relCase_3 ( Pnode &  B, Relation &  rel, set< Idx > &  tb, stack< Pnode * > &  todo  )

private

Definition at line 737 of file syn_synthequiv.cpp.

relCase_4()

void faudes::SOE::relCase_4 ( Pnode &  B, Relation &  rel, set< Idx > &  tb, stack< Pnode * > &  todo  )

private

Definition at line 790 of file syn_synthequiv.cpp.

Member Data Documentation

conalph

std::set<Idx> faudes::SOE::conalph

private

Definition at line 166 of file syn_synthequiv.cpp.

events

std::vector<Idx> faudes::SOE::events

private

vector of all events [starting with 1]

Definition at line 155 of file syn_synthequiv.cpp.

gen

const Generator* faudes::SOE::gen

private

keep a reference to automaton

Definition at line 160 of file syn_synthequiv.cpp.

localph

std::set<Idx> faudes::SOE::localph

private

Definition at line 167 of file syn_synthequiv.cpp.

locconalph

std::set<Idx> faudes::SOE::locconalph

private

Definition at line 171 of file syn_synthequiv.cpp.

locuncalph

std::set<Idx> faudes::SOE::locuncalph

private

Definition at line 170 of file syn_synthequiv.cpp.

nxidx

Idx faudes::SOE::nxidx

private

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

Definition at line 178 of file syn_synthequiv.cpp.

ro

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

private

set of nodes that form current partition, i.e. leaves of W.

Definition at line 188 of file syn_synthequiv.cpp.

roDividers

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

private

set of nodes that can possibly split classes in ro

Definition at line 193 of file syn_synthequiv.cpp.

shaalph

std::set<Idx> faudes::SOE::shaalph

private

Definition at line 168 of file syn_synthequiv.cpp.

shaconalph

std::set<Idx> faudes::SOE::shaconalph

private

Definition at line 173 of file syn_synthequiv.cpp.

shauncalph

std::set<Idx> faudes::SOE::shauncalph

private

Definition at line 172 of file syn_synthequiv.cpp.

states

std::vector<State> faudes::SOE::states

private

vector of all states [starting with 1]

Definition at line 150 of file syn_synthequiv.cpp.

uncalph

std::set<Idx> faudes::SOE::uncalph

private

vorious eventsets of interest

Definition at line 165 of file syn_synthequiv.cpp.

W

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

private

W-tree contains all blocks ever created [required for destruction]

Definition at line 183 of file syn_synthequiv.cpp.

---

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

• syn_synthequiv.cpp