faudes::ComSyn Class Reference

Detailed Description

Definition at line 56 of file syn_compsyn.cpp.

Public Member Functions
	ComSyn (const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec, std::map< Idx, Idx > &rMapEventsToPlant, GeneratorVector &rDisGenVec, GeneratorVector &rSupGenVec)
	Constructer: construct the synthesis-buffer for running compositional synthesis algorithmus and initialize the map and supervisors. More...
	~ComSyn (void)
	Destructer. More...
void	Preprocess (void)
	Preprocess: firstly abstract every generator in synthesis-buffer before running synthesis-algorithmus. More...
void	Synthesis (void)
	Compositional Synthesis Algorithmus after Preprocess. More...

Private Member Functions
void	SetPartUnion (const GeneratorVector &rGenVec, GeneratorVector::Position WithoutMe, EventSet &rRestAlph)
	the union of eventset from generators but without a speicified generator More...
void	comsyn_ComputeBisimulation (Generator &rGen)
	adjust bisimulation relation to compositional synthesis More...

Private Attributes
EventSet	GConAlph
	global controllable events More...
GeneratorVector	GenVec
	synthesis-buffer More...
std::map< Idx, Idx > *	pMapEventsToPlant
	keep reference to event-map More...
GeneratorVector *	pDisGenVec
	keep reference to distinguisher-generator More...
GeneratorVector *	pSupGenVec
	keep reference to supervisor-generator More...
SymbolTable *	pEvSymTab
	keep reference to EventSymbolTable More...
Idx	w
	the termination-event More...

Constructor & Destructor Documentation

ComSyn()

faudes::ComSyn::ComSyn	(	const GeneratorVector &	rPlantGenVec,
		const EventSet &	rConAlph,
		const GeneratorVector &	rSpecGenVec,
		std::map< Idx, Idx > &	rMapEventsToPlant,
		GeneratorVector &	rDisGenVec,
		GeneratorVector &	rSupGenVec
	)

Constructer: construct the synthesis-buffer for running compositional synthesis algorithmus and initialize the map and supervisors.

Input:

Parameters

rPlantGenVec	plant generator-vector
rConAlph	controllable events
rSpecGenVec	specification generator-vector

Output:

Parameters

rMapEventsToPlant	map the events in supervisor to plant
rDisGenVec	distinguisher generator-vector
rSupGenVec	supervisor generator-vector

Definition at line 318 of file syn_compsyn.cpp.

~ComSyn()

faudes::ComSyn::~ComSyn

(

void

)

Destructer.

Definition at line 566 of file syn_compsyn.cpp.

Member Function Documentation

comsyn_ComputeBisimulation()

void faudes::ComSyn::comsyn_ComputeBisimulation ( faudes::Generator &  rGen )

private

adjust bisimulation relation to compositional synthesis

Parameters

rGen	the adjusted generator

Definition at line 587 of file syn_compsyn.cpp.

Preprocess()

void faudes::ComSyn::Preprocess

(

void

)

Preprocess: firstly abstract every generator in synthesis-buffer before running synthesis-algorithmus.

Definition at line 385 of file syn_compsyn.cpp.

SetPartUnion()

void faudes::ComSyn::SetPartUnion ( const GeneratorVector &  rGenVec, GeneratorVector::Position  WithoutMe, EventSet &  rRestAlph  )

private

the union of eventset from generators but without a speicified generator

Parameters

rGenVec	the generators which to be extracted
WithoutMe	the specified generator
rRestAlph	result

Definition at line 573 of file syn_compsyn.cpp.

Synthesis()

void faudes::ComSyn::Synthesis

(

void

)

Compositional Synthesis Algorithmus after Preprocess.

Definition at line 462 of file syn_compsyn.cpp.

Member Data Documentation

GConAlph

EventSet faudes::ComSyn::GConAlph

private

global controllable events

Definition at line 110 of file syn_compsyn.cpp.

GenVec

GeneratorVector faudes::ComSyn::GenVec

private

synthesis-buffer

Definition at line 115 of file syn_compsyn.cpp.

pDisGenVec

GeneratorVector* faudes::ComSyn::pDisGenVec

private

keep reference to distinguisher-generator

Definition at line 125 of file syn_compsyn.cpp.

pEvSymTab

SymbolTable* faudes::ComSyn::pEvSymTab

private

keep reference to EventSymbolTable

Definition at line 135 of file syn_compsyn.cpp.

pMapEventsToPlant

std::map<Idx,Idx>* faudes::ComSyn::pMapEventsToPlant

private

keep reference to event-map

Definition at line 120 of file syn_compsyn.cpp.

pSupGenVec

GeneratorVector* faudes::ComSyn::pSupGenVec

private

keep reference to supervisor-generator

Definition at line 130 of file syn_compsyn.cpp.

w

Idx faudes::ComSyn::w

private

the termination-event

Definition at line 140 of file syn_compsyn.cpp.

---

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

• syn_compsyn.cpp