#include <LabelledPrioritizedNet.hh>

Public Member Functions
	LabelledPrioritizedNet ()

	LabelledPrioritizedNet (const LabelledPrioritizedNet &net)

LabelledPrioritizedNet &	operator= (const LabelledPrioritizedNet &net)

LabelledPrioritizedNet &	append (const LabelledPrioritizedNet &net)

	LabelledPrioritizedNet (const LabelledPrioritizedNet &lppn1, const LabelledPrioritizedNet &lppn2, const unordered_set< Event > &syncEvents)

LabelledPrioritizedNet &	merge (const LabelledPrioritizedNet &lppn1, const LabelledPrioritizedNet &lppn2, const unordered_set< Event > &syncEvents, std::unordered_map< Transition, std::list< Transition > > &lppn1SyncTrans, std::unordered_map< Transition, std::list< Transition > > &lppn2SyncTrans, std::unordered_map< Transition, std::pair< Transition, Transition > > &syncTransitions, std::unordered_map< Place, Place > &lppn1Place, std::unordered_map< Place, Place > &lppn2Place, std::unordered_map< Place, std::pair< Place, Place > > &syncPlaces)

void	setPriority (Transition t1, Transition t2)

const set< Transition > &	priorities (Transition tr) const

const set< Transition > &	reversedPriorities (Transition tr) const

void	resetPriority (Transition t1, Transition t2)

void	priorities2Dot (ostream &os) const

virtual void	deleteTransition (Transition t1)

Public Member Functions inherited from Diades::Petri::LabelledNet
Event	lambda () const

	LabelledNet ()

	LabelledNet (const LabelledNet &net)

LabelledNet &	operator= (const LabelledNet &net)

LabelledNet &	append (const LabelledNet &net)

	LabelledNet (const LabelledNet &lpn1, const LabelledNet &lpn2, const unordered_set< Event > &syncEvents)

LabelledNet &	merge (const LabelledNet &lpn1, const LabelledNet &lpn2, const unordered_set< Event > &syncEvents, std::unordered_map< Transition, std::list< Transition > > &lpn1SyncTrans, std::unordered_map< Transition, std::list< Transition > > &lpn2SyncTrans, unordered_map< Transition, std::pair< Transition, Transition >> &synchronisations, std::unordered_map< Place, Place > &lpn1Place, std::unordered_map< Place, Place > &lpn2Place, std::unordered_map< Place, std::pair< Place, Place > > &syncPlaces)

virtual void	nameOfTransition2Dot (ostream &os, Transition transition) const

virtual Transition	newTransition (const set< Place > &pre, const set< Place > &post, const string &name, Event e)

TransitionEventIterator	beginOfTransitionWithEvent (Event event) const

TransitionEventIterator	endOfTransitionWithEvent (Event event) const

Transition	duplicateTransition (Transition t)

virtual void	net2TinaTransitionName (ostream &os, Transition trans) const

virtual void	copyLabelledNet (const LabelledNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

virtual void	appendLabelledNet (const LabelledNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

virtual void	mergeLabelledNet (const LabelledNet &lpn1, const LabelledNet &lpn2, const unordered_set< Event > &syncEvents, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMapLpn1, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapFromLpn1, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMapLpn2, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapFromLpn2, std::unordered_map< Transition, std::list< Transition > > &lpn1SyncTrans, std::unordered_map< Transition, std::list< Transition > > &lpn2SyncTrans, std::unordered_map< Transition, std::pair< Transition, Transition > > &syncTransitions, std::unordered_map< Place, Place > &lppn1Place, std::unordered_map< Place, Place > &lppn2Place, std::unordered_map< Place, std::pair< Place, Place > > &syncPlaces)

EventIterator	beginOfEvents () const

EventIterator	endOfEvents () const

Event	getEvent (Transition t) const

bool	containsEvent (Event event) const

Public Member Functions inherited from Diades::Petri::BoundedNet
	BoundedNet ()

	BoundedNet (const BoundedNet &net)

BoundedNet &	operator= (const BoundedNet &net)

BoundedNet &	append (const BoundedNet &net)

virtual	~BoundedNet ()

void	setName (const string &name)

const string &	name () const

unsigned int	id () const

void	setId (unsigned id)

void	clear ()

const Diades::Graph::Graph &	graph () const

Place	newPlace ()

Place	newPlace (const string &name)

void	deletePlace (Place p)

void	setLabelOfPlace (Place place, const string &label)

PlaceIterator	beginOfPlaces () const

PlaceIterator	endOfPlaces () const

size_t	numberOfPlaces () const

const string &	labelOfPlace (const Place &p) const

const string &	nameOfPlace (Place p) const

void	setNameOfPlace (Place p, const string &name)

Place	getPlace (const string &name) const

Arc	getArc (Diades::Graph::Node n1, Diades::Graph::Node n2) const

virtual bool	enables (Transition t, const Marking &marking) const

virtual bool	fire (Transition t, const Marking &marking, Marking &newMarking) const

virtual Transition	newTransition (const set< Place > &pre, const set< Place > &post)

virtual Transition	newTransition (const set< Place > &pre, const set< Place > &post, const string &name)

virtual void	setInhibition (Place p, Transition t)

const std::unordered_set< Transition > &	inhibitors (Place p) const

virtual void	unsetInhibition (Place p, Transition t)

bool	inhibits (Place p, Transition t) const

size_t	numberOfTransitions () const

size_t	numberOfArcs () const

void	addPre (Transition transition, Place place)

void	addPost (Transition transition, Place place)

ConstIterator	preTransBegin (Place place) const

ConstIterator	preTransEnd (Place place) const

ConstIterator	postTransBegin (Place place) const

ConstIterator	postTransEnd (Place place) const

ConstIterator	preBegin (Transition transition) const

ConstIterator	preEnd (Transition transition) const

ConstIterator	postBegin (Transition transition) const

ConstIterator	postEnd (Transition transition) const

TransitionIterator	beginOfTransitions () const

TransitionIterator	endOfTransitions () const

void	setNameOfTransition (Transition transition, const string &name)

const string &	nameOfTransition (Transition transition) const

Transition	transitionOfName (const string &name) const

bool	inPre (Transition t, Place p) const

bool	inPost (Transition t, Place p) const

const Marking &	initialMarking () const

Marking &	initialMarking ()

bool	isMarked () const

virtual void	net2Dot (const string &fileName) const

void	net2Tina (ostream &os) const

void	net2Tina (const string &filename) const

void	printPrettyMarking (ostream &os, const Marking &marking) const

virtual void	appendNet (const BoundedNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

template<typename Iterator >
Place	mergePlaces (Iterator first, Iterator last)

Protected Member Functions
virtual void	priorities2Tina (ostream &os) const

virtual void	net2TinaEnd (ostream &os, const string &header) const

virtual void	writeEndOfDotFile (ostream &os) const

virtual void	copyLabelledPrioritizedNet (const LabelledPrioritizedNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

virtual void	appendLabelledPrioritizedNet (const LabelledPrioritizedNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

virtual void	mergeLabelledPrioritizedNet (const LabelledPrioritizedNet &lppn1, const LabelledPrioritizedNet &lppn2, const unordered_set< Event > &syncEvents, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMapLppn1, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapFromLppn1, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMapLppn2, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapFromLppn2, std::unordered_map< Transition, std::list< Transition > > &lppn1SyncTrans, std::unordered_map< Transition, std::list< Transition > > &lppn2SyncTrans, std::unordered_map< Transition, std::pair< Transition, Transition > > &syncTransitions, std::unordered_map< Place, Place > &lppn1Place, std::unordered_map< Place, Place > &lppn2Place, std::unordered_map< Place, std::pair< Place, Place > > &syncPlaces)

Protected Member Functions inherited from Diades::Petri::BoundedNet
void	net2TinaWithHeader (ostream &os, const string &netHeader) const

virtual void	net2TinaTransition (ostream &os, Transition trans) const

virtual void	net2TinaTransitionInterval (ostream &os, Transition transition) const

virtual void	copyNet (const BoundedNet &net, Diades::Graph::ConstNodeMap< Diades::Graph::Node > &nodeMap, Diades::Graph::NodeMap< Diades::Graph::Node > &nodeMapCopy, Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &edgeMap, Diades::Graph::EdgeMap< Diades::Graph::Edge > &edgeMapCopy)

Private Attributes
std::set< Transition >	_involved

std::set< Transition >	_reversedInvolved

Diades::Graph::NodeMap< std::set< Transition > >	_priorities

Diades::Graph::NodeMap< std::set< Transition > >	_reversedPriorities

Additional Inherited Members
Public Types inherited from Diades::Petri::LabelledNet
typedef Diades::Utils::Exception< LabelledNet >	Exception

typedef PetriEventManager::EventId	Event

typedef set< Event >::const_iterator	EventIterator

typedef unordered_set< Transition >::const_iterator	TransitionEventIterator

typedef unordered_set< Transition >::const_iterator	EventTransitionIterator

Public Types inherited from Diades::Petri::BoundedNet
enum	NodeType { P, T }

typedef Diades::Utils::Exception< BoundedNet >	Exception

typedef PerTypeIterator	TransitionIterator

typedef PerTypeIterator	PlaceIterator

typedef set< Transition >::const_iterator	TransitionEventIterator

Static Public Member Functions inherited from Diades::Petri::LabelledNet
static string	typeName ()

Static Public Member Functions inherited from Diades::Petri::BoundedNet
static string	typeName ()

Protected Types inherited from Diades::Petri::BoundedNet
enum	TransitionType { NotPostponable, Postponable }

Protected Attributes inherited from Diades::Petri::BoundedNet
Diades::Graph::Graph	_graph

Diades::Graph::NodeMap< NodeType >	_nodeType

Diades::Graph::NodeMap< string >	_nameOfNode

Diades::Graph::NodeMap< string >	_labelOfNode

Diades::Graph::NodeMap< int >	_postponable

Diades::Graph::NodeMap< std::unordered_set< Transition > >	_inhibitors

Diades::Graph::NodeMap< std::unordered_set< Place > >	_inhibited

string	_name

Marking	_initialMarking

unordered_map< string, Diades::Graph::Node >	_placeOfName

unordered_map< string, Diades::Graph::Node >	_transitionOfName

Detailed Description

A LabelledPrioritizedNet is a LabelledNet with priorities

Definition at line 18 of file LabelledPrioritizedNet.hh.

Constructor & Destructor Documentation

◆ LabelledPrioritizedNet() [1/3]

Diades::Petri::LabelledPrioritizedNet::LabelledPrioritizedNet ( )

Default constructor

◆ LabelledPrioritizedNet() [2/3]

Diades::Petri::LabelledPrioritizedNet::LabelledPrioritizedNet ( const LabelledPrioritizedNet & net )

Copy constructor

◆ LabelledPrioritizedNet() [3/3]

Diades::Petri::LabelledPrioritizedNet::LabelledPrioritizedNet	(	const LabelledPrioritizedNet &	lppn1,
		const LabelledPrioritizedNet &	lppn2,
		const unordered_set< Event > &	syncEvents
	)

Construct the product of lpn1 and lpn2 synchronised on the events whose labels are in syncEventLabels

Parameters

lppn1	A labelledPrioritizedNet
lppn2	A labelledPrioritizedNet
syncEvents	a set of event

Member Function Documentation

◆ append()

LabelledPrioritizedNet& Diades::Petri::LabelledPrioritizedNet::append ( const LabelledPrioritizedNet & net )

Appending of the current net with 'net'

Parameters

net	the LabelledNet to append

Returns: the current net

Postcondition: the places/ransitions of the current net before the appending are renamed with an infix 'l' (left). The places/ransitions of the appended net are named with an infix 'r' (right) in the resulting net.

◆ appendLabelledPrioritizedNet()

virtual void Diades::Petri::LabelledPrioritizedNet::appendLabelledPrioritizedNet	(	const LabelledPrioritizedNet &	net,
		Diades::Graph::ConstNodeMap< Diades::Graph::Node > &	nodeMap,
		Diades::Graph::NodeMap< Diades::Graph::Node > &	nodeMapCopy,
		Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &	edgeMap,
		Diades::Graph::EdgeMap< Diades::Graph::Edge > &	edgeMapCopy
	)

protectedvirtual

Labelled net appending with map recording

Parameters

net	the LabelledNet to be appended
nodeMap	the node mapping: graph's node -> copy's node
nodeMapCopy	the node mapping: copy's node -> graph's node
edgeMap	the edge mapping: graph's edge -> copy's edge
edgeMapCopy	the edge mapping: copy's edge -> graph's edge

Postcondition: the places/ransitions of the current net before the appending are renamed with an infix 'l' (left). The places/ransitions of the appended net are named with an infix 'r' (right) in the resulting net.

◆ copyLabelledPrioritizedNet()

virtual void Diades::Petri::LabelledPrioritizedNet::copyLabelledPrioritizedNet	(	const LabelledPrioritizedNet &	net,
		Diades::Graph::ConstNodeMap< Diades::Graph::Node > &	nodeMap,
		Diades::Graph::NodeMap< Diades::Graph::Node > &	nodeMapCopy,
		Diades::Graph::ConstEdgeMap< Diades::Graph::Edge > &	edgeMap,
		Diades::Graph::EdgeMap< Diades::Graph::Edge > &	edgeMapCopy
	)

protectedvirtual

LabelledPrioritizedNetcopy with map recording

Parameters

net	the LabelledNet to copy
copy	the resulting copy of the graph
nodeMap	the node mapping: graph's node -> copy's node
nodeMapCopy	the node mapping: copy's node -> graph's node
edgeMap	the edge mapping: graph's edge -> copy's edge
edgeMapCopy	the edge mapping: copy's edge -> graph's edge

◆ deleteTransition()

virtual void Diades::Petri::LabelledPrioritizedNet::deleteTransition ( Transition t1 )

virtual

Parameters

t1	Transition to delete

Reimplemented from Diades::Petri::LabelledNet.

◆ merge()

LabelledPrioritizedNet& Diades::Petri::LabelledPrioritizedNet::merge	(	const LabelledPrioritizedNet &	lppn1,
		const LabelledPrioritizedNet &	lppn2,
		const unordered_set< Event > &	syncEvents,
		std::unordered_map< Transition, std::list< Transition > > &	lppn1SyncTrans,
		std::unordered_map< Transition, std::list< Transition > > &	lppn2SyncTrans,
		std::unordered_map< Transition, std::pair< Transition, Transition > > &	syncTransitions,
		std::unordered_map< Place, Place > &	lppn1Place,
		std::unordered_map< Place, Place > &	lppn2Place,
		std::unordered_map< Place, std::pair< Place, Place > > &	syncPlaces
	)

Synchronisation of two LabelledPrioritizedNets based on set of events

Parameters

lppn1	'left' LabelledPrioritizedNet
lppn2	'right' LabelledPrioritizedNet
syncEvents	set of synchronised events
lppn1SyncTrans	mapping between synchronisable transitions of lppn1 and the synchronised one
lppn2SyncTrans	mapping between synchronisable transitions of lppn2 and the synchronised one syncTransitions mapping between the synchronised transitions and their lppn1/lppn2 counterparts

Returns: the current net that results from the synchonisation of lppn1 and lppn2

Postcondition: the places/ransitions of the left net are renamed with an infix 'l' (left). The places/ransitions of the right net are named with an infix 'r' (right) in the resulting net.

◆ mergeLabelledPrioritizedNet()

virtual void Diades::Petri::LabelledPrioritizedNet::mergeLabelledPrioritizedNet	(	const LabelledPrioritizedNet &	lppn1,
		const LabelledPrioritizedNet &	lppn2,
		const unordered_set< Event > &	syncEvents,
		Diades::Graph::ConstNodeMap< Diades::Graph::Node > &	nodeMapLppn1,
		Diades::Graph::NodeMap< Diades::Graph::Node > &	nodeMapFromLppn1,
		Diades::Graph::ConstNodeMap< Diades::Graph::Node > &	nodeMapLppn2,
		Diades::Graph::NodeMap< Diades::Graph::Node > &	nodeMapFromLppn2,
		std::unordered_map< Transition, std::list< Transition > > &	lppn1SyncTrans,
		std::unordered_map< Transition, std::list< Transition > > &	lppn2SyncTrans,
		std::unordered_map< Transition, std::pair< Transition, Transition > > &	syncTransitions,
		std::unordered_map< Place, Place > &	lppn1Place,
		std::unordered_map< Place, Place > &	lppn2Place,
		std::unordered_map< Place, std::pair< Place, Place > > &	syncPlaces
	)

protectedvirtual

Synchronisation of two LabelledPrioritizedNets based on set of events

Parameters

lppn1	'left' LabelledPrioritizedNet
lppn2	'right' LabelledPrioritizedNet
syncEvents	set of synchronised events
nodeMapLppn1	the node mapping: lppn1 graph's node -> merged net's node
nodeMapFromLppn1	the node mapping: merged net's node -> lppn1 graph's node
nodeMapLppn2	the node mapping: lppn2 graph's node -> merged net's node
nodeMapFromLppn2	the node mapping: merged net's node -> lppn2 graph's node
lppn1SyncTrans	mapping between synchronisable transitions of lppn1 and the synchronised one
lppn2SyncTrans	mapping between synchronisable transitions of lppn2 and the synchronised one syncTransitions mapping between the synchronised transitions and their lppn1/lppn2 counterparts

Postcondition: the places/ransitions of the left net are renamed with an infix 'l' (left). The places/ransitions of the right net are named with an infix 'r' (right) in the resulting net.

◆ net2TinaEnd()

virtual void Diades::Petri::LabelledPrioritizedNet::net2TinaEnd	(	ostream &	os,
		const string &	header
	)		const

protectedvirtual

Output the end of a TINA file

Parameters

os	the updated stream

Reimplemented from Diades::Petri::BoundedNet.

◆ operator=()

LabelledPrioritizedNet& Diades::Petri::LabelledPrioritizedNet::operator= ( const LabelledPrioritizedNet & net )

Assignment operator

◆ priorities()

const set<Transition>& Diades::Petri::LabelledPrioritizedNet::priorities ( Transition tr ) const

Parameters

tr	a Transition

Returns: the set of Transitions that have a lower priority than tr

◆ priorities2Dot()

void Diades::Petri::LabelledPrioritizedNet::priorities2Dot ( ostream & os ) const

Export priorities to dot format

Parameters

os	the updated stream

◆ priorities2Tina()

virtual void Diades::Petri::LabelledPrioritizedNet::priorities2Tina ( ostream & os ) const

protectedvirtual

Export priorities to tina format

Parameters

os	the updated stream

◆ resetPriority()

void Diades::Petri::LabelledPrioritizedNet::resetPriority	(	Transition	t1,
		Transition	t2
	)

Reset the priority between t1 and t2

Parameters

t1	Transition with the highest priority
t2	Transition with the lowest priority

◆ reversedPriorities()

const set<Transition>& Diades::Petri::LabelledPrioritizedNet::reversedPriorities ( Transition tr ) const

Parameters

tr	a Transition

Returns: the set of Transitions that have a greater priority than tr

◆ setPriority()

void Diades::Petri::LabelledPrioritizedNet::setPriority	(	Transition	t1,
		Transition	t2
	)

Set the priority between Transition t1 and Transition t2

Parameters

t1	Transition with the highest priority
t2	Transition with the lowest priority

Todo:: implement transitivity + error management

◆ writeEndOfDotFile()

virtual void Diades::Petri::LabelledPrioritizedNet::writeEndOfDotFile ( ostream & os ) const

protectedvirtual

Output the end of a dot file

Parameters

os	the updated stream

Reimplemented from Diades::Petri::BoundedNet.

Member Data Documentation

◆ _involved

std::set<Transition> Diades::Petri::LabelledPrioritizedNet::_involved

private

Definition at line 21 of file LabelledPrioritizedNet.hh.

◆ _priorities

Diades::Graph::NodeMap<std::set<Transition> > Diades::Petri::LabelledPrioritizedNet::_priorities

private

Definition at line 23 of file LabelledPrioritizedNet.hh.

◆ _reversedInvolved

std::set<Transition> Diades::Petri::LabelledPrioritizedNet::_reversedInvolved

private

Definition at line 22 of file LabelledPrioritizedNet.hh.

◆ _reversedPriorities

Diades::Graph::NodeMap<std::set<Transition> > Diades::Petri::LabelledPrioritizedNet::_reversedPriorities

private

Definition at line 24 of file LabelledPrioritizedNet.hh.

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

/home/yannick/laas/redmine/tools/diades/include/diades/petri/LabelledPrioritizedNet.hh

Public Member Functions

Protected Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ LabelledPrioritizedNet() [1/3]

◆ LabelledPrioritizedNet() [2/3]

◆ LabelledPrioritizedNet() [3/3]

Member Function Documentation

◆ append()

◆ appendLabelledPrioritizedNet()

◆ copyLabelledPrioritizedNet()

◆ deleteTransition()

◆ merge()

◆ mergeLabelledPrioritizedNet()

◆ net2TinaEnd()

◆ operator=()

◆ priorities()

◆ priorities2Dot()

◆ priorities2Tina()

◆ resetPriority()

◆ reversedPriorities()

◆ setPriority()

◆ writeEndOfDotFile()

Member Data Documentation

◆ _involved

◆ _priorities

◆ _reversedInvolved

◆ _reversedPriorities