Detailed Description

Definition at line 73 of file syn_synthequiv.cpp.

Classes
struct	Relation
	a relation according to SOE in one block More...

struct	State
	internal representation of transition relation with consecutive indexed states and events More...

Public Member Functions
	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. More...

	~SOE (void)
	Destructor. More...

void	refine (void)
	Perform fixpoint iteration to obtain the coarset synthesis-observation-equivalence. More...

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

Private Member Functions
void	initStateMember_Pre ()
	construct 2st Part of Struct "State" More...

void	initStateMember_Pres ()
	construct 3st Part of Struct "State" More...

Pnode *	newnode ()
	insert new node in W-tree with empty stateset More...

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

void	computeRel (Pnode &B, std::vector< Relation > &relations)
	construct all relations with respect to coset B More...

void	computeEquStates (Pnode &B, Relation &rel, std::set< Idx > &tb, std::stack< Pnode * > &todo)
	collect all states from coset B which are equivalent to the speicified state and determine the related nodes which is possibly to be splitted More...

void	relCase_1 (Pnode &B, Relation &rel, set< Idx > &tb, stack< Pnode * > &todo)
	implementation part for function "computeEquStates" it is organized as follows with respect to various cases: More...

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
	vector of all states [starting with 1] More...

std::vector< Idx >	events
	vector of all events [starting with 1] More...

const Generator *	gen
	keep a reference to automaton More...

std::set< Idx >	uncalph
	vorious eventsets of interest More...

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
	Counter to assign a unique index to each node [debugging/cosmetic only]. More...

std::vector< Pnode * >	W
	W-tree contains all blocks ever created [required for destruction]. More...

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

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

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

Detailed Description

Classes

Public Member Functions

Private Member Functions

Private Attributes

Constructor & Destructor Documentation

◆ SOE()

◆ ~SOE()

Member Function Documentation

◆ computeEquStates()

◆ computeRel()

◆ initStateMember_Pre()

◆ initStateMember_Pres()

◆ newnode()

◆ partition()

◆ partitionClass()

◆ refine()

◆ relCase_1()

◆ relCase_2()

◆ relCase_3()

◆ relCase_4()

Member Data Documentation

◆ conalph

◆ events

◆ gen

◆ localph

◆ locconalph

◆ locuncalph

◆ nxidx

◆ ro

◆ roDividers

◆ shaalph

◆ shaconalph

◆ shauncalph

◆ states

◆ uncalph

◆ W