#include <LabelledNet.hh>

Public Types
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

Public Member Functions
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	deleteTransition (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)

Event management
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)

Static Public Member Functions
static string	typeName ()

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

Private Attributes
unordered_map< Event, unordered_set< Transition > >	_eventTransitions

set< Event >	_eventList

Diades::Graph::ConstNodeMap< Event >	_event

Event	_lambda

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

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

virtual void	writeEndOfDotFile (ostream &os) const

virtual void	net2TinaEnd (ostream &os, const string &header) 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)

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 LabelledNet is a BoundedNet where any transition is associated with an Event. The empty event is denoted lambda.

Definition at line 20 of file LabelledNet.hh.

Member Typedef Documentation

◆ Event

typedef PetriEventManager::EventId Diades::Petri::LabelledNet::Event

Definition at line 39 of file LabelledNet.hh.

◆ EventIterator

Diades::Petri::LabelledNet::EventIterator

Iteration over the set of BoundedNet::Event involved in the current Net

Definition at line 47 of file LabelledNet.hh.

◆ EventTransitionIterator

typedef unordered_set<Transition>::const_iterator Diades::Petri::LabelledNet::EventTransitionIterator

Definition at line 78 of file LabelledNet.hh.

◆ Exception

Diades::Petri::LabelledNet::Exception

Exceptions

Exception exception returned by any Net

Definition at line 37 of file LabelledNet.hh.

◆ TransitionEventIterator

typedef unordered_set<Transition>::const_iterator Diades::Petri::LabelledNet::TransitionEventIterator

Definition at line 53 of file LabelledNet.hh.

Constructor & Destructor Documentation

◆ LabelledNet() [1/3]

Diades::Petri::LabelledNet::LabelledNet ( )

inline

Default constructor: empty net

Definition at line 83 of file LabelledNet.hh.

References append(), Diades::Petri::BoundedNet::graph(), Diades::Graph::ConstNodeMap< T >::init(), merge(), and operator=().

◆ LabelledNet() [2/3]

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

Copy constructor

Todo:: implement

◆ LabelledNet() [3/3]

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

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

Parameters

lpn1	A labelledNet
lpn2	A labelledNet
syncEvents	a set of event

Todo:: implement

Member Function Documentation

◆ append()

LabelledNet& Diades::Petri::LabelledNet::append ( const LabelledNet & 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.

Referenced by LabelledNet().

◆ appendLabelledNet()

virtual void Diades::Petri::LabelledNet::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

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.

Referenced by net2TinaTransitionName().

◆ beginOfEvents()

EventIterator Diades::Petri::LabelledNet::beginOfEvents ( ) const

inline

Returns: an iterator on the set of events (begin)

Definition at line 209 of file LabelledNet.hh.

◆ beginOfTransitionWithEvent()

TransitionEventIterator Diades::Petri::LabelledNet::beginOfTransitionWithEvent ( Event event ) const

inline

Parameters

event an Event

Returns: start iterator on the Transition with the Event 'event'

Definition at line 254 of file LabelledNet.hh.

References containsEvent(), getEvent(), Diades::Petri::PetriEventManager::petriEventManager(), and require.

◆ containsEvent()

bool Diades::Petri::LabelledNet::containsEvent ( Event event ) const

inline

Is the event contained in the Petri Net

Parameters

event an Event

Returns: true if at least one Transition is associated with the Event 'event'

Definition at line 242 of file LabelledNet.hh.

Referenced by beginOfTransitionWithEvent(), and endOfTransitionWithEvent().

◆ copyLabelledNet()

virtual void Diades::Petri::LabelledNet::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

LabelledNetcopy 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

Referenced by net2TinaTransitionName().

◆ deleteTransition()

virtual void Diades::Petri::LabelledNet::deleteTransition ( Transition t )

virtual

Transition deletion

Parameters

t	a Transition

Reimplemented from Diades::Petri::BoundedNet.

Reimplemented in Diades::Petri::LabelledPrioritizedNet.

Referenced by endOfTransitionWithEvent().

◆ duplicateTransition()

Transition Diades::Petri::LabelledNet::duplicateTransition ( Transition t )

virtual

Transition duplication

Parameters

t	a Transition

Returns: the created clone of transition t. The clone has the same Event and the same pre and post conditions

Reimplemented from Diades::Petri::BoundedNet.

Referenced by endOfTransitionWithEvent().

◆ endOfEvents()

EventIterator Diades::Petri::LabelledNet::endOfEvents ( ) const

inline

Returns: an iterator on the set of events (end)

Definition at line 218 of file LabelledNet.hh.

◆ endOfTransitionWithEvent()

TransitionEventIterator Diades::Petri::LabelledNet::endOfTransitionWithEvent ( Event event ) const

inline

Parameters

event an Event

Returns: end iterator on the Transition with the Event 'event'

Definition at line 267 of file LabelledNet.hh.

References containsEvent(), deleteTransition(), duplicateTransition(), getEvent(), Diades::Petri::PetriEventManager::petriEventManager(), and require.

◆ getEvent()

Event Diades::Petri::LabelledNet::getEvent ( Transition t ) const

inline

Parameters

t	a Transition of the Net

Returns: the event associated to the transition t

Definition at line 228 of file LabelledNet.hh.

References Diades::Petri::BoundedNet::_graph, Diades::Petri::BoundedNet::_nodeType, require, and Diades::Petri::BoundedNet::T.

Referenced by beginOfTransitionWithEvent(), endOfTransitionWithEvent(), nameOfTransition2Dot(), and net2TinaTransitionName().

◆ lambda()

Event Diades::Petri::LabelledNet::lambda ( ) const

inline

Returns: the empty Event (mainly used for time point events in a TimeNet)

Definition at line 70 of file LabelledNet.hh.

References _lambda.

Referenced by Diades::Petri::RealTimeSystem::RealTimeSystem().

◆ merge()

LabelledNet& Diades::Petri::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
	)

Synchronisation of two LabelledNets based on set of events

Parameters

lpn1	'left' LabelledNet
lpn2	'right' LabelledNet
syncEvents	set of synchronised events
lpn1SyncTrans	mapping between synchronisable transitions of lpn1 and the synchronised one
lpn2SyncTrans	mapping between synchronisable transitions of lpn2 and the synchronised one
synchronisations	set of synchronised transitions with their lpn1 and lpn2 mapping

Returns: the current net that results from the synchonisation of lpn1 and lpn2

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.

Referenced by LabelledNet().

◆ mergeLabelledNet()

virtual void Diades::Petri::LabelledNet::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
	)

virtual

Synchronisation of two LabelledNets based on set of events

Parameters

lpn1	'left' LabelledNet
lpn2	'right' LabelledNet
syncEvents	set of synchronised events
nodeMapLpn1	the node mapping: lpn1 graph's node -> merged net's node
nodeMapFromLpn1	the node mapping: merged net's node -> lpn1 graph's node
nodeMapLpn2	the node mapping: lpn2 graph's node -> merged net's node
nodeMapFromLpn2	the node mapping: merged net's node -> lpn2 graph's node
lpn1SyncTrans	mapping between synchronisable transitions of lpn1 and the synchronised one
lpn2SyncTrans	mapping between synchronisable transitions of lpn2 and the synchronised one
synchronisations	set of synchronised transitions with their lpn1 and lpn2 mapping

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.

Referenced by net2TinaTransitionName().

◆ nameOfTransition2Dot()

virtual void Diades::Petri::LabelledNet::nameOfTransition2Dot	(	ostream &	os,
		Transition	transition
	)		const

inlinevirtual

Parameters

e an Event

Returns: an iterator on the first transition labelled with 'e'

Parameters

e an Event

Returns: an iterator on the element after the last transition labelled with 'e' Output a LabelledNet transition in dot format.

Parameters

os	output stream
transition	a LabelledNet transition

Reimplemented from Diades::Petri::BoundedNet.

Reimplemented in Diades::Petri::LabelledPrioritizedTimeNet.

Definition at line 178 of file LabelledNet.hh.

References Diades::Automata::Experimental::EventManager< _Event, _EventId, NullEvent, NullEventId, Hash >::getEvent(), getEvent(), Diades::Petri::BoundedNet::name(), Diades::Petri::BoundedNet::nameOfTransition(), newTransition(), and Diades::Petri::PetriEventManager::petriEventManager().

◆ net2TinaTransitionName()

virtual void Diades::Petri::LabelledNet::net2TinaTransitionName	(	ostream &	os,
		Transition	trans
	)		const

inlinevirtual

Output a LabelledNet transition event in tine format.

Parameters

os	output stream
transition	a LabelledNet transition

Reimplemented from Diades::Petri::BoundedNet.

Definition at line 296 of file LabelledNet.hh.

References appendLabelledNet(), copyLabelledNet(), Diades::Automata::Experimental::EventManager< _Event, _EventId, NullEvent, NullEventId, Hash >::getEvent(), getEvent(), mergeLabelledNet(), and Diades::Petri::PetriEventManager::petriEventManager().

◆ newTransition()

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

virtual

Parameters

pre	precondition of the transition
post	postcondition of the transition
name	Name associated to the created Transition

Returns: the new Transition t such that pre(t) = pre and post(t) = post

Reimplemented in Diades::Petri::Observations.

Referenced by nameOfTransition2Dot().

◆ operator=()

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

Assignment operator

Todo:: implement

Referenced by LabelledNet().

◆ typeName()

static string Diades::Petri::LabelledNet::typeName ( )

inlinestatic

Returns: the absolute name of this class

Definition at line 29 of file LabelledNet.hh.

Member Data Documentation

◆ _event

Diades::Graph::ConstNodeMap<Event> Diades::Petri::LabelledNet::_event

private

Definition at line 58 of file LabelledNet.hh.

◆ _eventList

set<Event> Diades::Petri::LabelledNet::_eventList

private

Definition at line 57 of file LabelledNet.hh.

◆ _eventTransitions

unordered_map<Event, unordered_set<Transition> > Diades::Petri::LabelledNet::_eventTransitions

private

Definition at line 56 of file LabelledNet.hh.

◆ _lambda

Event Diades::Petri::LabelledNet::_lambda

private

Definition at line 59 of file LabelledNet.hh.

Referenced by lambda().

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

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

Public Types

Public Member Functions

Static Public Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ Event

◆ EventIterator

◆ EventTransitionIterator

◆ Exception

◆ TransitionEventIterator

Constructor & Destructor Documentation

◆ LabelledNet() [1/3]

◆ LabelledNet() [2/3]

◆ LabelledNet() [3/3]

Member Function Documentation

◆ append()

◆ appendLabelledNet()

◆ beginOfEvents()

◆ beginOfTransitionWithEvent()

◆ containsEvent()

◆ copyLabelledNet()

◆ deleteTransition()

◆ duplicateTransition()

◆ endOfEvents()

◆ endOfTransitionWithEvent()

◆ getEvent()

◆ lambda()

◆ merge()

◆ mergeLabelledNet()

◆ nameOfTransition2Dot()

◆ net2TinaTransitionName()

◆ newTransition()

◆ operator=()

◆ typeName()

Member Data Documentation

◆ _event

◆ _eventList

◆ _eventTransitions

◆ _lambda