This class implements a branching process of a Net (see Esparza 2002). More...

#include <BranchingProcess.hh>

Public Types
typedef Place	Condition

typedef Transition	Event

typedef Diades::Utils::Exception< BranchingProcess >	Exception

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

typedef Diades::Utils::Exception< Net >	Exception

typedef PerTypeIterator	TransitionIterator

typedef PerTypeIterator	PlaceIterator

typedef set< Event >::const_iterator	EventIterator

typedef set< Transition >::const_iterator	TransitionEventIterator

Public Member Functions
	BranchingProcess ()

	BranchingProcess (Net &net)

void	setNet (Net &net)

Net &	net ()

void	initProcess ()

void	clear ()

const set< BranchingProcess::Condition > &	min () const

const set< BranchingProcess::Condition > &	max () const

void	unfold ()

void	getPossibleExtensions (Extensions &extensions)

Event	addExtension (const Extension &extension)

bool	isCutOff (const Event &e) const

Configuration	configuration (set< Event > &events) const

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

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

virtual	~Net ()

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

EventIterator	beginOfEvents () const

EventIterator	endOfEvents () const

const Event &	getEvent (Transition t) const

virtual void	setEvent (Transition t, Event event)

bool	containsEvent (Event event) const

Place	newPlace ()

Place	newPlace (const string &label)

void	setLabelOfPlace (const Place &place, const string &label)

PlaceIterator	beginOfPlaces () const

PlaceIterator	endOfPlaces () const

size_t	numberOfPlaces () const

const string &	labelOfPlace (const Place &p) const

const string &	getInfoLabel (Place p) const

void	setInfoLabel (Place p, const string &info)

virtual bool	enables (const Transition &t, const set< Place > &marking)

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)

size_t	numberOfTransitions () const

size_t	numberOfArcs () const

void	addPre (Transition transition, Place place)

void	addPost (Transition transition, Place place)

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

ConstIterator	preTransBegin (const Place &place) const

ConstIterator	preTransEnd (const Place &place) const

ConstIterator	postTransBegin (const Place &place) const

ConstIterator	postTransEnd (const Place &place) const

ConstIterator	preBegin (const Transition &transition) const

ConstIterator	preEnd (const Transition &transition) const

ConstIterator	postBegin (const Transition &transition) const

ConstIterator	postEnd (const Transition &transition) const

TransitionIterator	beginOfTransitions () const

TransitionIterator	endOfTransitions () const

void	setLabelOfTransition (const Transition &t, const string &label)

const string &	labelOfTransition (const Transition &t) const

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

TransitionEventIterator	beginOfTransitionWithEvent (Event event) const

TransitionEventIterator	endOfTransitionWithEvent (Event event) const

virtual void	deleteTransition (Transition t)

virtual Transition	duplicateTransition (Transition t)

void	setPostponable (Transition t)

bool	isPostponable (Transition t) const

void	setNotPostponable (Transition t)

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

void	setMarking (const set< Place > &marking)

bool	isMarked () const

bool	isMarked (Place p) const

void	mark (Place p)

void	unmark (Place p)

const set< Place > &	initialMarking () const

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

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

Static Public Member Functions
static string	typeName ()

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

Private Types
typedef Diades::Utils::Box< Net >	NetBox

Private Attributes
NetBox	_net

Diades::Graph::ConstNodeMap< Place >	_bmap

set< Condition >	_min

set< Condition >	_max

set< Transition >	_involvedTransitions

Diades::Graph::ConstNodeMap< Extensions >	_possibleExtensions

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

Protected Attributes inherited from Diades::Petri::Net
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::ConstNodeMap< const Zsl * >	_preZslOfTransition

Graph::ConstNodeMap< const Zsl * >	_incidenceZslOfTransition

const Vdd *	_reachableNodes

set< Event >	_eventList

bool	_readOnly

Detailed Description

This class implements a branching process of a Net (see Esparza 2002).

A BranchingProcess is an occurrence Net that is usually a prefix of the unfolding of a system Net.

Definition at line 36 of file BranchingProcess.hh.

Member Typedef Documentation

◆ Condition

typedef Place Diades::Petri::BranchingProcess::Condition

Condition a Place of the BranchingProcess

Definition at line 42 of file BranchingProcess.hh.

◆ Event

typedef Transition Diades::Petri::BranchingProcess::Event

Event a Transition of the BranchingProcess

Definition at line 50 of file BranchingProcess.hh.

◆ Exception

Diades::Petri::BranchingProcess::Exception

Exceptions

Exception exception returned by any Net

Definition at line 76 of file BranchingProcess.hh.

◆ NetBox

typedef Diades::Utils::Box<Net> Diades::Petri::BranchingProcess::NetBox

private

NetBox a Reference to a Net

Definition at line 61 of file BranchingProcess.hh.

Constructor & Destructor Documentation

◆ BranchingProcess() [1/2]

Diades::Petri::BranchingProcess::BranchingProcess ( )

Default constructor

◆ BranchingProcess() [2/2]

Diades::Petri::BranchingProcess::BranchingProcess ( Net & net )

Parametrized constructor

Parameters

net	the underlying Net of this BranchingProcess

Member Function Documentation

◆ addExtension()

Event Diades::Petri::BranchingProcess::addExtension ( const Extension & extension )

Parameters

extension the Extension to add in the current BranchingProcess

Returns: the Event of the BranchingProcess associated to this Extension

Todo:: implement

Referenced by max().

◆ clear()

void Diades::Petri::BranchingProcess::clear ( )

Clear the BranchingProcess

Referenced by net().

◆ configuration()

Configuration Diades::Petri::BranchingProcess::configuration ( set< Event > & events ) const

Parameters

events a set of events

Returns: the Configuration of the BranchingProcess associated to this set of events

Referenced by max().

◆ getPossibleExtensions()

void Diades::Petri::BranchingProcess::getPossibleExtensions ( Extensions & extensions )

Get the set of possible extensions of the current BranchingProcess

Parameters

extensions the set of possible Extensions

Todo:: implement

Referenced by max().

◆ initProcess()

void Diades::Petri::BranchingProcess::initProcess ( )

Initialise the process

Referenced by net().

◆ isCutOff()

bool Diades::Petri::BranchingProcess::isCutOff ( const Event & e ) const

Parameters

e	the Event to test

Returns: true if the Event is a cutOff

Todo:: implement

Referenced by max().

◆ max()

const set<BranchingProcess::Condition>& Diades::Petri::BranchingProcess::max ( ) const

inline

Returns: the set of maximal conditions of the BranchingProcess

Definition at line 205 of file BranchingProcess.hh.

References _max, addExtension(), configuration(), getPossibleExtensions(), isCutOff(), and unfold().

◆ min()

const set<BranchingProcess::Condition>& Diades::Petri::BranchingProcess::min ( ) const

inline

Returns: the set of minimal conditions of the BranchingProcess

Definition at line 193 of file BranchingProcess.hh.

References _min.

◆ net()

Net& Diades::Petri::BranchingProcess::net ( )

inline

Returns: the underlying Net of the BranchingProcess

Definition at line 167 of file BranchingProcess.hh.

References clear(), initProcess(), and Diades::Utils::Box< Object >::obj().

◆ setNet()

void Diades::Petri::BranchingProcess::setNet ( Net & net )

Reset the BranchingProcess and associates it to the new Net

Parameters

net	the new underlying Net of this BranchingProcess

◆ typeName()

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

inlinestatic

Returns: the absolute name of this class

Definition at line 70 of file BranchingProcess.hh.

◆ unfold()

void Diades::Petri::BranchingProcess::unfold ( )

Compute the complete finite prefix

Referenced by max().

Member Data Documentation

◆ _bmap

Diades::Graph::ConstNodeMap<Place> Diades::Petri::BranchingProcess::_bmap

private

_bmap mapping condition -> place of the underlying net

Definition at line 91 of file BranchingProcess.hh.

◆ _involvedTransitions

set<Transition> Diades::Petri::BranchingProcess::_involvedTransitions

private

_involvedTransitions current set of Transitions of the underlying Net that have a possible Extension

Definition at line 120 of file BranchingProcess.hh.

◆ _max

set<Condition> Diades::Petri::BranchingProcess::_max

private

_max the set of maximal Conditions of the BranchingProcess

Definition at line 110 of file BranchingProcess.hh.

Referenced by max().

◆ _min

set<Condition> Diades::Petri::BranchingProcess::_min

private

_min the set of minimal Conditions of the BranchingProcess

Definition at line 101 of file BranchingProcess.hh.

Referenced by min().

◆ _net

NetBox Diades::Petri::BranchingProcess::_net

private

_net the underlying net associated to this BranchingProcess

Definition at line 83 of file BranchingProcess.hh.

◆ _possibleExtensions

Diades::Graph::ConstNodeMap<Extensions> Diades::Petri::BranchingProcess::_possibleExtensions

private

_possibleExtensions map that associates to each Transition of the Net its corresponding set of Extensions

Definition at line 132 of file BranchingProcess.hh.

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

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

Public Types

Public Member Functions

Static Public Member Functions

Private Types

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ Condition

◆ Event

◆ Exception

◆ NetBox

Constructor & Destructor Documentation

◆ BranchingProcess() [1/2]

◆ BranchingProcess() [2/2]

Member Function Documentation

◆ addExtension()

◆ clear()

◆ configuration()

◆ getPossibleExtensions()

◆ initProcess()

◆ isCutOff()

◆ max()

◆ min()

◆ net()

◆ setNet()

◆ typeName()

◆ unfold()

Member Data Documentation

◆ _bmap

◆ _involvedTransitions

◆ _max

◆ _min

◆ _net

◆ _possibleExtensions