1-bounded Petri nets More...

#include <PetriNet.hh>

Classes
class	Iterator
	Iterator on the PetriNet. More...

class	PerTypeIterator
	Iterators over the places or the transitions of the PetriNet. More...

Public Types
enum	NodeType { P, T }

typedef PerTypeIterator	TransitionIterator

typedef PerTypeIterator	PlaceIterator

typedef set< Event >::const_iterator	EventIterator

typedef set< Transition >::const_iterator	TransitionEventIterator

Public Member Functions
Constructors and destructor
	PetriNet ()

	PetriNet (const PetriNet &p1, const PetriNet &p2, const set< Event > &synchronization, bool strict=true)

virtual	~PetriNet ()

General accessors/modifiers
void	setName (const string &name)

const string &	name () const

unsigned int	id () const

void	setId (unsigned id)

int	numberOfPlaces () const

int	numberOfTransitions () const

void	clear ()

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

Event management
EventIterator	beginOfEvents () const

EventIterator	endOfEvents () const

const Event &	getEvent (Transition t) const

virtual void	setEvent (Transition t, const Event &event)

bool	containsEvent (const Event &event) const

Place management
Place	newPlace ()

Place	newPlace (const string &label)

PlaceIterator	beginOfPlaces () const

PlaceIterator	endOfPlaces () const

const string &	labelOfPlace (const Place &p) const

const string &	getInfoLabel (Place p) const

void	setInfoLabel (Place p, const string &info)

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

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

void	addPre (Transition transition, Place place)

void	addPost (Transition transition, Place place)

bool	pre (const Vdd *marking, const Transition &t) const

Iterator	preBegin (const Transition &transition) const

Iterator	preEnd (const Transition &transition) const

Iterator	postBegin (const Transition &transition) const

Iterator	postEnd (const Transition &transition) const

TransitionIterator	beginOfTransitions () const

TransitionIterator	endOfTransitions () const

const string &	labelOfTransition (const Transition &t) const

bool	inPre (const Transition &t, const Place &p) const

TransitionEventIterator	beginOfTransitionWithEvent (const Event &event) const

TransitionEventIterator	endOfTransitionWithEvent (const Event &event) const

virtual void	deleteTransition (Transition t)

virtual Transition	duplicateTransition (Transition t)

Methods for net synchronisation
void	setPostponable (Transition t)

bool	isPostponable (Transition t) const

void	setNotPostponable (Transition t)

void	synchronize (const PetriNet &p1, const PetriNet &p2, const set< Event > &synchronization, bool strict)

Basic Marking management
void	setMarking (const set< Place > &marking)

bool	isMarked () const

bool	isMarked (Place p) const

void	mark (Place p)

void	unmark (Place p)

IO management
virtual void	net2Dot (const string &fileName) const

virtual void	net2Tina (ostream &os) const

void	printWarning (const string &s) const

void	printFactory (const string &fileName) const

Marking Graph computation/analysis
These set of methods perform operations based on a symbolic representation of the Petri Net by the use of Zsl and Vdd.
void	lock () const

void	unlock () const

const Vdd *	marking () const

const Zsl *	getPreZsl (Transition t) const

const Zsl *	getIncidenceZsl (Transition t) const

const Vdd *	reachableNodes () const

void	printVdd (const Vdd *result, string fileName)

ZslFactory *	zslFactory () const

VddFactory *	vddFactory () const

Protected Types
enum	TransitionType { NotPostponable, Postponable }

Protected Attributes
ZslFactory *	_zslFactory

VddFactory *	_vddFactory

Graph::Graph	_graph

Graph::NodeMap< NodeType >	_nodeType

Graph::NodeMap< string >	_labelNode

Graph::NodeMap< string >	_infoNode

Graph::NodeMap< Event >	_event

Graph::NodeMap< int >	_postponable

string	_name

const Vdd *	_initialMarking

set< Place >	_explicitInitialMarking

unordered_map< string, Graph::Node >	_placeOfLabel

vector< set< Transition > >	_transitionsOfEventId

Graph::NodeMap< const Zsl * >	_preZslOfTransition

Graph::NodeMap< const Zsl * >	_incidenceZslOfTransition

const Vdd *	_reachableNodes

set< Event >	_eventList

bool	_readOnly

Private Attributes
int	_nbPlace

int	_nbTrans

unsigned int	_id

Friends
class	Iterator

class	PerTypeIterator

Detailed Description

1-bounded Petri nets

This class implements 1-bounded finite Petri Nets with the use of Diades::Graph::Graph. Each Place/Transition is a Diades::Graph::Node. Arcs between places and transitions are encoded with Diades::Graph::Edge.

Todo:: add lambda-transitions

Definition at line 61 of file PetriNet.hh.

Member Typedef Documentation

Diades::Petri::PetriNet::EventIterator

Iteration over the set of PetriNet::Event involved in the current PetriNet

Definition at line 288 of file PetriNet.hh.

Diades::Petri::PetriNet::PlaceIterator

Iteration over the set of places in a PetriNet. It is encoded by a PerTypeIterator (type PetriNet:P)

Definition at line 280 of file PetriNet.hh.

typedef set<Transition>::const_iterator Diades::Petri::PetriNet::TransitionEventIterator

Definition at line 294 of file PetriNet.hh.

Diades::Petri::PetriNet::TransitionIterator

Iteration over the set of transitions in a PetriNet. It is encoded by a PerTypeIterator (type PetriNet:T)

Definition at line 273 of file PetriNet.hh.

Member Enumeration Documentation

enum Diades::Petri::PetriNet::NodeType

A PetriNet is a set of nodes: some are places (type P), some are transitions (type T)

Enumerator
P
T

Definition at line 76 of file PetriNet.hh.

enum Diades::Petri::PetriNet::TransitionType

protected

Enumerator
NotPostponable
Postponable

Definition at line 297 of file PetriNet.hh.

Constructor & Destructor Documentation

Diades::Petri::PetriNet::PetriNet ( )

Default constructor

Diades::Petri::PetriNet::PetriNet	(	const PetriNet &	p1,
		const PetriNet &	p2,
		const set< Event > &	synchronization,
		bool	strict = `true`
	)

Parameterized constructor

Parameters

p1	PetriNet to synchronize
p2	PetriNet to synchronize
synchronization	synchronized Event
strict	type of synchronization

Returns

a PetriNet that results from the event synchronization of two PetriNet p1 and p2 If the synchronisation is strict every transition of Event e in p1 is synchronised with a Transition in p2. If the synchronisation is not strict, it is defined releying on the property "postponable" of a transition. Let t1 and t2 be two transitions that have the same synchronised event: many cases hold:

both are not postponable, one synchronised transition is created.
t1 is postponable but not t2, two versions of t2 remains, one that is synchronised with t1 one that is not.
t2 is postponable but not t1, two versions of t1 remains, one that is synchronised with t2 one that is not.
both are postponable, one version of t1 remains, one version of t2 remains and a synchronised version

virtual Diades::Petri::PetriNet::~PetriNet ( )

inlinevirtual

Destructor

Definition at line 369 of file PetriNet.hh.

Member Function Documentation

void Diades::Petri::PetriNet::addPost	(	Transition	transition,
		Place	place
	)

inline

Add a new Place to post(transition)

Parameters

transition	a Transition
place	a Place

Precondition: place is a Place of the current PetriNet; transition is a Transition of the current PetriNet

Definition at line 699 of file PetriNet.hh.

void Diades::Petri::PetriNet::addPre	(	Transition	transition,
		Place	place
	)

inline

Add a new Place to pre(transition)

Parameters

transition	a Transition
place	a Place

Precondition: place is a Place of the current PetriNet; transition is a Transition of the current PetriNet

Definition at line 687 of file PetriNet.hh.

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

inline

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

Definition at line 454 of file PetriNet.hh.

PlaceIterator Diades::Petri::PetriNet::beginOfPlaces ( ) const

inline

Returns: start iterator on the places of the PetriNet

Definition at line 578 of file PetriNet.hh.

TransitionIterator Diades::Petri::PetriNet::beginOfTransitions ( ) const

inline

Returns: start iterator on the transitions of the PetriNet

Definition at line 769 of file PetriNet.hh.

TransitionEventIterator Diades::Petri::PetriNet::beginOfTransitionWithEvent ( const Event & event ) const

inline

Parameters

event an Event

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

Definition at line 808 of file PetriNet.hh.

References require.

void Diades::Petri::PetriNet::clear ( )

Clear the current Petri Net

bool Diades::Petri::PetriNet::containsEvent ( const 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 518 of file PetriNet.hh.

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

virtual

Transition deletion

Parameters

t	a Transition

Reimplemented in Diades::Petri::TimePetriNet.

virtual Transition Diades::Petri::PetriNet::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 in Diades::Petri::TimePetriNet.

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

inline

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

Definition at line 464 of file PetriNet.hh.

PlaceIterator Diades::Petri::PetriNet::endOfPlaces ( ) const

inline

Returns: end iterator on the places of the PetriNet

Definition at line 588 of file PetriNet.hh.

TransitionIterator Diades::Petri::PetriNet::endOfTransitions ( ) const

inline

Returns: end iterator on the transitions of the PetriNet

Definition at line 779 of file PetriNet.hh.

TransitionEventIterator Diades::Petri::PetriNet::endOfTransitionWithEvent ( const Event & event ) const

inline

Parameters

event an Event

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

Definition at line 822 of file PetriNet.hh.

References require.

const Event& Diades::Petri::PetriNet::getEvent ( Transition t ) const

inline

Parameters

t	a Transition of the PetriNet

Returns: the event associated to the transition t

Definition at line 474 of file PetriNet.hh.

References require.

const Zsl* Diades::Petri::PetriNet::getIncidenceZsl ( Transition t ) const

Parameters

t	a Transition of the Petri Net

Returns: the associated Zsl (incidence)

Postcondition: with the first call of this method, the Petri becomes unmodifiable

const string& Diades::Petri::PetriNet::getInfoLabel ( Place p ) const

inline

Parameters

p a Place

Get the information associated to Place p. This information can be set by setInfoLabel

Definition at line 612 of file PetriNet.hh.

References require.

const Zsl* Diades::Petri::PetriNet::getPreZsl ( Transition t ) const

Parameters

t	a Transition of the Petri Net

Returns: the associated Zsl (precondition)

Postcondition: with the first call of this method, the Petri becomes unmodifiable

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

inline

Returns: the underlying Graph that encodes the PetriNet

Definition at line 439 of file PetriNet.hh.

unsigned int Diades::Petri::PetriNet::id ( ) const

inline

Returns: the id of the Petri Net

Definition at line 405 of file PetriNet.hh.

bool Diades::Petri::PetriNet::inPre	(	const Transition &	t,
		const Place &	p
	)		const

Parameters

t	a Transition
p	a Place

Returns: true if the Place p is in the precondition of t

bool Diades::Petri::PetriNet::isMarked ( ) const

inline

Returns: true if the current PetriNet has a non-empty marking

Definition at line 931 of file PetriNet.hh.

bool Diades::Petri::PetriNet::isMarked ( Place p ) const

Returns: true if the place p is marked in the current PetriNet

bool Diades::Petri::PetriNet::isPostponable ( Transition t ) const

inline

Parameters

t	a Transition

Returns: true if the given Transition is postponable

Definition at line 875 of file PetriNet.hh.

References require.

const string& Diades::Petri::PetriNet::labelOfPlace ( const Place & p ) const

inline

Parameters

p a Place

Returns: the label associated to the Place p

Definition at line 601 of file PetriNet.hh.

Referenced by Diades::Petri::ZslFactory::printZsl().

const string& Diades::Petri::PetriNet::labelOfTransition ( const Transition & t ) const

inline

Parameters

t	a Transition

Returns: the label associated to the Transition t

Definition at line 790 of file PetriNet.hh.

void Diades::Petri::PetriNet::lock ( ) const

Make the Petri Net read-only (to use the symbolic implementation) The call of this method is mandatory before calling anything method that is using the symbolic representation with Zsl / Vdd

void Diades::Petri::PetriNet::mark ( Place p )

Parameters

p	a Place Add p to the marking of the PetriNet

const Vdd* Diades::Petri::PetriNet::marking ( ) const

Returns: the marking of the PetriNet

const string& Diades::Petri::PetriNet::name ( ) const

inline

Returns: the name of the PetriNet

Definition at line 398 of file PetriNet.hh.

virtual void Diades::Petri::PetriNet::net2Dot ( const string & fileName ) const

virtual

Parameters

fileName the name of an output file Write in the file 'fileName' the dot description of the PetriNet

Reimplemented in Diades::Petri::TimePetriNet.

virtual void Diades::Petri::PetriNet::net2Tina ( ostream & os ) const

virtual

Parameters

os	output stream Write the TINA '.net' description of the PetriNet (see TINA ) on the output stream

Referenced by main().

Place Diades::Petri::PetriNet::newPlace ( )

inline

Returns: a new Place of the PetriNet

Postcondition: the place has an internal and generated label "__pX" where X is a number; the return place is invalid if the Petri Net is in "readonly mode"

Definition at line 540 of file PetriNet.hh.

References ensure, and require.

Place Diades::Petri::PetriNet::newPlace ( const string & label )

Parameters

label Label associated to the created Place

Returns: a new Place of the PetriNet

Postcondition: If there is a place that already has the label, return the predefined place

virtual Transition Diades::Petri::PetriNet::newTransition	(	const set< Place > &	pre,
		const set< Place > &	post
	)

virtual

Parameters

pre	precondition of the transition
post	postcondition of the transition

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

virtual Transition Diades::Petri::PetriNet::newTransition	(	const set< Place > &	pre,
		const set< Place > &	post,
		const string &	label
	)

inlinevirtual

Parameters

pre	precondition of the transition
post	postcondition of the transition
label	Label associated to the created Transition

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

Postcondition: the return transition is invalid if the Petri Net is in "readonly mode"

Definition at line 665 of file PetriNet.hh.

References require.

int Diades::Petri::PetriNet::numberOfPlaces ( ) const

inline

Returns: the number of places in the PetriNet

Definition at line 423 of file PetriNet.hh.

Referenced by main().

int Diades::Petri::PetriNet::numberOfTransitions ( ) const

inline

Returns: the number of transitions in the PetriNet

Definition at line 428 of file PetriNet.hh.

Referenced by main().

Iterator Diades::Petri::PetriNet::postBegin ( const Transition & transition ) const

inline

Parameters

transition a Transition

Returns: start iterator on post(t)

Definition at line 748 of file PetriNet.hh.

Iterator Diades::Petri::PetriNet::postEnd ( const Transition & transition ) const

inline

Parameters

transition a Transition

Returns: end iterator on post(t)

Definition at line 759 of file PetriNet.hh.

bool Diades::Petri::PetriNet::pre	(	const Vdd *	marking,
		const Transition &	t
	)		const

Parameters

marking	a possible marking of the PetriNet
t	a Transition

Returns: true if the Transition 't' is enabled by the marking 'marking'

Precondition: marking.owner() == this

Iterator Diades::Petri::PetriNet::preBegin ( const Transition & transition ) const

inline

Parameters

marking	a possible marking of the PetriNet
t	a Transition

Returns: true if the marking 'marking' is possible after firing the Transition 't'

Precondition: marking.owner() == this

Parameters

transition a Transition

Returns: start iterator on pre(t)

Definition at line 728 of file PetriNet.hh.

Iterator Diades::Petri::PetriNet::preEnd ( const Transition & transition ) const

inline

Parameters

transition a Transition

Returns: end iterator on pre(t)

Definition at line 738 of file PetriNet.hh.

void Diades::Petri::PetriNet::printFactory ( const string & fileName ) const

Print factory

Parameters

fileName the output file name

void Diades::Petri::PetriNet::printVdd	(	const Vdd *	result,
		string	fileName
	)

Print the content of a given vdd into a file

Parameters

vdd	a Vdd
fileName	file name

void Diades::Petri::PetriNet::printWarning ( const string & s ) const

inline

Print warning message

Parameters

s	a string that contains a contextual information

Definition at line 991 of file PetriNet.hh.

const Vdd* Diades::Petri::PetriNet::reachableNodes ( ) const

Compute the set of reachable states from the initial marking

Returns: the Vdd representation of this set of states.

virtual void Diades::Petri::PetriNet::setEvent	(	Transition	t,
		const Event &	event
	)

inlinevirtual

Parameters

t	a Transition of the PetriNet
event	an Event Associates the Event 'event' to the Transition 't'

Definition at line 488 of file PetriNet.hh.

References Diades::Petri::Event::id(), and require.

void Diades::Petri::PetriNet::setId ( unsigned id )

inline

Set the id of the Petri net

Parameters

id	the new id

Definition at line 414 of file PetriNet.hh.

void Diades::Petri::PetriNet::setInfoLabel	(	Place	p,
		const string &	info
	)

inline

Parameters

p	a Place
info	an information Associates to the Place p the information info. This information can be retrieved by getInfoLabel

Definition at line 628 of file PetriNet.hh.

References require.

void Diades::Petri::PetriNet::setMarking ( const set< Place > & marking )

Set a marking

Parameters

marking the set of marked places The marking of the PetriNet is 'marking'

void Diades::Petri::PetriNet::setName ( const string & name )

inline

Set the name of the PetriNet

Parameters

name	the new name of the PetriNet

Definition at line 387 of file PetriNet.hh.

References require.

Referenced by main().

void Diades::Petri::PetriNet::setNotPostponable ( Transition t )

Set a Transition not postponable. If a Transition is not postponable, it means that it must be synhronised with a Transition from the other PetriNet when performing the synchronise() operation.

Parameters

t	a Transition

void Diades::Petri::PetriNet::setPostponable ( Transition t )

Set a Transition postponable. A postponable Transition is a transition that can be independently fired even if the associated event is usually synchronised with an event from another Petri Net by the synchronise() operator. In other words, a postponable transition can be fired even if there is no transition in the other Petri Net that can be synchronised. In the case it is possible to synchronise this Transition with another one, the synchronisation results in two Transitions. One is the synchronised one, the one is the independent one. Transition

Parameters

t	a Transition

void Diades::Petri::PetriNet::synchronize	(	const PetriNet &	p1,
		const PetriNet &	p2,
		const set< Event > &	synchronization,
		bool	strict
	)

Synchronization operator

Parameters

p1	PetriNet to synchronize
p2	PetriNet to synchronize
synchronization	synchronized Event
strict	type of synchronization

Returns: a PetriNet that results from the event synchronization of two PetriNet p1 and p2 If the synchronisation is strict every transition of Event e in p1 is synchronised with a Transition in p2. If the synchronisation is not strict, it is defined releying on the property "postponable" of a transition. Let t1 and t2 be two transitions that have the same synchronised event: many cases hold: 1) both are not postponable, one synchronised transition is created. 2) t1 is postponable but not t2, two versions of t2 remains, one that is synchronised with t1 one that is not. 3) t2 is postponable but not t1, two versions of t1 remains, one that is synchronised with t2 one that is not. 4) both are postponable, one version of t1 remains, one version of t2 remains and a synchronised version

void Diades::Petri::PetriNet::unlock ( ) const

Make the Petri Net modifiable.

Postcondition: any symbolic implementation of the current PetriNet is erased. If the PetriNet was locked, a new call to lock() is required to use the symbolic implementation of the Petri Net.

void Diades::Petri::PetriNet::unmark ( Place p )

Parameters

p	a Place Remove p to the marking of the PetriNet

VddFactory* Diades::Petri::PetriNet::vddFactory ( ) const

inline

Returns: the factory of the Vdd

Definition at line 1080 of file PetriNet.hh.

ZslFactory* Diades::Petri::PetriNet::zslFactory ( ) const

inline

Returns: the factory of the Zsl

Definition at line 1071 of file PetriNet.hh.

Friends And Related Function Documentation

friend class Iterator

friend

Definition at line 264 of file PetriNet.hh.

friend class PerTypeIterator

friend

Definition at line 265 of file PetriNet.hh.

Member Data Documentation

Graph::NodeMap<Event> Diades::Petri::PetriNet::_event

protected

Definition at line 302 of file PetriNet.hh.

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

protected

Definition at line 312 of file PetriNet.hh.

set<Place> Diades::Petri::PetriNet::_explicitInitialMarking

protected

Definition at line 306 of file PetriNet.hh.

Graph::Graph Diades::Petri::PetriNet::_graph

protected

Type of Transition

Definition at line 298 of file PetriNet.hh.

unsigned int Diades::Petri::PetriNet::_id

private

Definition at line 324 of file PetriNet.hh.

Graph::NodeMap<const Zsl *> Diades::Petri::PetriNet::_incidenceZslOfTransition

mutableprotected

Definition at line 310 of file PetriNet.hh.

Graph::NodeMap<string> Diades::Petri::PetriNet::_infoNode

protected

Definition at line 301 of file PetriNet.hh.

const Vdd* Diades::Petri::PetriNet::_initialMarking

mutableprotected

Definition at line 305 of file PetriNet.hh.

Graph::NodeMap<string> Diades::Petri::PetriNet::_labelNode

protected

Definition at line 300 of file PetriNet.hh.

string Diades::Petri::PetriNet::_name

protected

Definition at line 304 of file PetriNet.hh.

int Diades::Petri::PetriNet::_nbPlace

private

Definition at line 317 of file PetriNet.hh.

int Diades::Petri::PetriNet::_nbTrans

private

Definition at line 318 of file PetriNet.hh.

Graph::NodeMap<NodeType> Diades::Petri::PetriNet::_nodeType

protected

Definition at line 299 of file PetriNet.hh.

unordered_map<string,Graph::Node> Diades::Petri::PetriNet::_placeOfLabel

protected

Definition at line 307 of file PetriNet.hh.

Graph::NodeMap<int> Diades::Petri::PetriNet::_postponable

protected

Definition at line 303 of file PetriNet.hh.

Graph::NodeMap<const Zsl *> Diades::Petri::PetriNet::_preZslOfTransition

mutableprotected

Definition at line 309 of file PetriNet.hh.

const Vdd* Diades::Petri::PetriNet::_reachableNodes

mutableprotected

Definition at line 311 of file PetriNet.hh.

bool Diades::Petri::PetriNet::_readOnly

mutableprotected

Definition at line 321 of file PetriNet.hh.

vector<set<Transition> > Diades::Petri::PetriNet::_transitionsOfEventId

protected

Definition at line 308 of file PetriNet.hh.

VddFactory* Diades::Petri::PetriNet::_vddFactory

mutableprotected

Definition at line 65 of file PetriNet.hh.

ZslFactory* Diades::Petri::PetriNet::_zslFactory

mutableprotected

Definition at line 64 of file PetriNet.hh.

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

/home/yannick/compilation/stable/include/petri/PetriNet.hh

Classes

Public Types

Public Member Functions

Protected Types

Protected Attributes

Private Attributes

Friends

Detailed Description

Member Typedef Documentation

Member Enumeration Documentation

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation