Diades::Petri::VddFactory Class Reference

#include <Vdd.hh>

Public Member Functions
	VddFactory (const Net &net)
virtual	~VddFactory ()
const Vdd *	getVdd (Place place, int tokens, const Vdd *eq, const Vdd *sup)
int	getCardinality (const Vdd *vdd)
bool	holds (const Vdd *vdd, Place p, int tokens) const
const Vdd *	getVdd (const Vdd *vdd, const Zsl *zsl)
const Vdd *	getVdd (const set< Place > &marking)
bool	isEmpty (const Vdd *vdd) const
bool	isNull (const Vdd *vdd) const
const Vdd *	getVdd (unsigned id)
const Vdd *	addZslToVdd (const Vdd *vdd, const Zsl *zsl)
const Vdd *	getFirable (const Vdd *vdd, const Zsl *zsl)
const Vdd *	getUnion (const Vdd *vdd1, const Vdd *vdd2)
const Vdd *	getIntersection (const Vdd *vdd1, const Vdd *vdd2)
const Net *	owner () const
void	printDot (const string &fileName) const
void	printDot (const Vdd *vdd, const string &fileName) const
const Vdd *	empty () const
const Vdd *	null () const

Private Attributes
const Net *	_net
vector< vector< unordered_map< unsigned, unordered_map< unsigned, Vdd * > > > >	_vdd
vector< Vdd * >	_table
vector< int >	_card
Vdd *	_empty
Vdd *	_null

Detailed Description

Definition at line 169 of file Vdd.hh.

Constructor & Destructor Documentation

VddFactory()

Diades::Petri::VddFactory::VddFactory ( const Net &  net )

inline

Create a ZslFactory associated to a Petri Net

Parameters

net	the associated Net

Definition at line 185 of file Vdd.hh.

References Diades::Petri::Vdd::_id.

~VddFactory()

virtual Diades::Petri::VddFactory::~VddFactory ( )

virtual

Destructor

Member Function Documentation

addZslToVdd()

const Vdd* Diades::Petri::VddFactory::addZslToVdd	(	const Vdd *	vdd,
		const Zsl *	zsl
	)

Parameters

vdd
zsl

Returns

a vdd that results from the triggering of the transition represented by zsl

See also

the operqtion oplus of molinaro

empty()

const Vdd* Diades::Petri::VddFactory::empty ( ) const

inline

Returns

the empty vdd

Definition at line 336 of file Vdd.hh.

getCardinality()

int Diades::Petri::VddFactory::getCardinality

(

const Vdd *

vdd

)

Parameters

vdd

Returns

getFirable()

const Vdd* Diades::Petri::VddFactory::getFirable	(	const Vdd *	vdd,
		const Zsl *	zsl
	)

Parameters

vdd
zsl

Returns

the vdd representing the subset of markings from which the transition represented by the zsl is firable

getIntersection()

const Vdd* Diades::Petri::VddFactory::getIntersection	(	const Vdd *	vdd1,
		const Vdd *	vdd2
	)

Parameters

vdd1
vdd2

Returns

get the vdd that represents the intersection of vdd1 and vdd2

getUnion()

const Vdd* Diades::Petri::VddFactory::getUnion	(	const Vdd *	vdd1,
		const Vdd *	vdd2
	)

Parameters

vdd1
vdd2

Returns

get the vdd that represents the union of vdd1 and vdd2

getVdd() [1/4]

const Vdd* Diades::Petri::VddFactory::getVdd	(	Place	place,
		int	tokens,
		const Vdd *	eq,
		const Vdd *	sup
	)

This method implements the find_or_add_vdd algorithm of Molinaro

Parameters

place	a Place of net()
tokens	the number of tokens in the place
eq	a Vdd or 0 (a pointer to a Vdd with a place with a greater id)
sup	a Vdd or 0 (a pointer to a Vdd with the same place but with more tokens)

Returns

the Vdd(place,tokens,eq,sup)

Postcondition

if not in the factory, the Vdd is created, guarantee that the Vdd has a unique representative in the VddFactory

getVdd() [2/4]

const Vdd* Diades::Petri::VddFactory::getVdd	(	const Vdd *	vdd,
		const Zsl *	zsl
	)

Parameters

vdd
zsl

Returns

getVdd() [3/4]

const Vdd* Diades::Petri::VddFactory::getVdd

(

const set< Place > &

marking

)

Parameters

marking

Returns

getVdd() [4/4]

const Vdd* Diades::Petri::VddFactory::getVdd ( unsigned  id )

inline

Parameters

id	a identifier

Returns

the Vdd associated with this id, if not exist return 0

Definition at line 276 of file Vdd.hh.

holds()

bool Diades::Petri::VddFactory::holds	(	const Vdd *	vdd,
		Place	p,
		int	tokens
	)		const

Parameters

vdd	a Vdd
p	a Place
tokens	a set of tokens

Returns

true if for any state of the marking in vdd, (p,tokens) is true.

isEmpty()

bool Diades::Petri::VddFactory::isEmpty ( const Vdd *  vdd ) const

inline

Parameters

vdd

Returns

true if the vdd is the empty vdd

Definition at line 259 of file Vdd.hh.

isNull()

bool Diades::Petri::VddFactory::isNull ( const Vdd *  vdd ) const

inline

Parameters

vdd

Returns

true if the vdd is the empty vdd

Definition at line 267 of file Vdd.hh.

null()

const Vdd* Diades::Petri::VddFactory::null ( ) const

inline

Returns

the null vdd

Definition at line 342 of file Vdd.hh.

owner()

const Net* Diades::Petri::VddFactory::owner ( ) const

inline

Returns

the Net associated with the ZslFactory

Definition at line 316 of file Vdd.hh.

References Diades::Graph::printDot().

printDot() [1/2]

void Diades::Petri::VddFactory::printDot

(

const string &

fileName

)

const

Export a dot output of the factory for debugging

Parameters

fileName

the name of the output file

printDot() [2/2]

void Diades::Petri::VddFactory::printDot	(	const Vdd *	vdd,
		const string &	fileName
	)		const

Export a dot output of a vdd for debugging

Parameters

fileName

the name of the output file

Member Data Documentation

_card

vector<int> Diades::Petri::VddFactory::_card

private

Definition at line 176 of file Vdd.hh.

_empty

Vdd* Diades::Petri::VddFactory::_empty

private

Definition at line 177 of file Vdd.hh.

_net

const Net* Diades::Petri::VddFactory::_net

private

Definition at line 173 of file Vdd.hh.

_null

Vdd* Diades::Petri::VddFactory::_null

private

Definition at line 178 of file Vdd.hh.

_table

vector<Vdd *> Diades::Petri::VddFactory::_table

private

Definition at line 175 of file Vdd.hh.

_vdd

vector< vector< unordered_map<unsigned, unordered_map <unsigned, Vdd *> > > > Diades::Petri::VddFactory::_vdd

private

Definition at line 174 of file Vdd.hh.

---

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

• /home/yannick/laas/redmine/tools/diades/include/diades/petri/Vdd.hh