Diades::Petri::ReachabilityGraph Class Reference

#include <ReachabilityGraph.hh>

Public Types
typedef Diades::Utils::Exception< ReachabilityGraph >	Exception
typedef Diades::Graph::Graph	RGraph
typedef Diades::Graph::Node	RState
typedef Diades::Graph::Edge	RTransition
typedef Diades::Graph::NodeMap< set< string > >	Marking
typedef Diades::Graph::EdgeMap< string >	TransitionLabel
typedef Diades::Graph::NodeMap< unsigned >	Ids
typedef Diades::Graph::NodeIterator	RStateIterator
typedef Diades::Graph::EdgeIterator	RTransitionIterator
typedef Diades::Graph::InEdgeIterator	InRTransitionIterator
typedef Diades::Graph::OutEdgeIterator	OutRTransitionIterator
typedef unordered_map< unsigned, RState >	StateDictionnary

Public Member Functions
	ReachabilityGraph ()
	state dictionary More...
virtual	~ReachabilityGraph ()
const set< string > &	getMarking (RState state)
void	addMarking (RState state, const string &mark)
const string &	getLabel (RTransition transition)
unsigned	numberOfStates () const
unsigned	numberOfTransitions () const
bool	empty () const
RState	target (const RTransition &trans) const
RState	source (const RTransition &trans) const

Static Public Member Functions
static string	typeName ()

Private Attributes
RGraph	_graph
RState	_initial
	the underlying graph More...
Marking	_marking
	the initial state More...
TransitionLabel	_transLabel
	the marking associated to each RState of the graph More...
Ids	_id
	the label associated to each RTransition of the More...
StateDictionnary	_dictionary
	the ids associated to the states More...

Iterators
RStateIterator	stateBegin ()
RStateIterator	stateEnd ()
RStateIterator	stateBegin () const
RStateIterator	stateEnd () const
RTransitionIterator	transBegin ()
RTransitionIterator	transEnd ()
RTransitionIterator	transBegin () const
RTransitionIterator	transEnd () const
virtual void	addTimeConstraint (RState state, const string &transitionName, const Diades::Utils::Interval &interval)
Graph::Graph &	graph ()
const Graph::Graph &	graph () const
OutRTransitionIterator	outTransBegin (const RState &state) const
OutRTransitionIterator	outTransEnd (const RState &state) const
InRTransitionIterator	outTransBegin (const RState &state)
InRTransitionIterator	outTransEnd (const RState &state)
void	clear ()
RState	getState (unsigned id)
RTransition	getTrans (RState source, RState target, const string &label)
unsigned	getId (RState state) const
void	setInitial (RState state)
RState	initialState () const
bool	importTinaGraph (const string &fileAut, const string &fileVrb)
virtual bool	exportGraphToDot (const string &fileDot)
bool	importTinaAut (const string &fileAut)
virtual bool	importTinaVrb (const string &fileVrb)

Detailed Description

Reachability graph of a Petri Net. Enumerative structure used by Houssam-Eddine Gougam for time analysis.

Definition at line 24 of file ReachabilityGraph.hh.

Member Typedef Documentation

Exception

typedef Diades::Utils::Exception<ReachabilityGraph> Diades::Petri::ReachabilityGraph::Exception

Definition at line 28 of file ReachabilityGraph.hh.

Ids

typedef Diades::Graph::NodeMap< unsigned > Diades::Petri::ReachabilityGraph::Ids

Definition at line 36 of file ReachabilityGraph.hh.

InRTransitionIterator

typedef Diades::Graph::InEdgeIterator Diades::Petri::ReachabilityGraph::InRTransitionIterator

Definition at line 39 of file ReachabilityGraph.hh.

Marking

typedef Diades::Graph::NodeMap< set<string> > Diades::Petri::ReachabilityGraph::Marking

Definition at line 34 of file ReachabilityGraph.hh.

OutRTransitionIterator

typedef Diades::Graph::OutEdgeIterator Diades::Petri::ReachabilityGraph::OutRTransitionIterator

Definition at line 40 of file ReachabilityGraph.hh.

RGraph

typedef Diades::Graph::Graph Diades::Petri::ReachabilityGraph::RGraph

Definition at line 31 of file ReachabilityGraph.hh.

RState

typedef Diades::Graph::Node Diades::Petri::ReachabilityGraph::RState

Definition at line 32 of file ReachabilityGraph.hh.

RStateIterator

typedef Diades::Graph::NodeIterator Diades::Petri::ReachabilityGraph::RStateIterator

Definition at line 37 of file ReachabilityGraph.hh.

RTransition

typedef Diades::Graph::Edge Diades::Petri::ReachabilityGraph::RTransition

Definition at line 33 of file ReachabilityGraph.hh.

RTransitionIterator

typedef Diades::Graph::EdgeIterator Diades::Petri::ReachabilityGraph::RTransitionIterator

Definition at line 38 of file ReachabilityGraph.hh.

StateDictionnary

typedef unordered_map<unsigned,RState> Diades::Petri::ReachabilityGraph::StateDictionnary

Definition at line 41 of file ReachabilityGraph.hh.

TransitionLabel

typedef Diades::Graph::EdgeMap< string > Diades::Petri::ReachabilityGraph::TransitionLabel

Definition at line 35 of file ReachabilityGraph.hh.

Constructor & Destructor Documentation

ReachabilityGraph()

Diades::Petri::ReachabilityGraph::ReachabilityGraph ( )

inline

state dictionary

Definition at line 52 of file ReachabilityGraph.hh.

~ReachabilityGraph()

virtual Diades::Petri::ReachabilityGraph::~ReachabilityGraph ( )

inlinevirtual

Definition at line 58 of file ReachabilityGraph.hh.

Member Function Documentation

addMarking()

void Diades::Petri::ReachabilityGraph::addMarking ( RState  state, const string &  mark  )

inline

Parameters

state	a state of the graph
mark	label of the place in the marking to add

Definition at line 76 of file ReachabilityGraph.hh.

References require.

addTimeConstraint()

virtual void Diades::Petri::ReachabilityGraph::addTimeConstraint ( RState  state, const string &  transitionName, const Diades::Utils::Interval &  interval  )

inlinevirtual

Todo:

I do this stupid thing to have only one VrbParser for ReachabilityGraph and TimeReachabilityGraph: change that

Reimplemented in Diades::Petri::TimeReachabilityGraph.

Definition at line 230 of file ReachabilityGraph.hh.

clear()

void Diades::Petri::ReachabilityGraph::clear ( )

inline

Clear the graph

Definition at line 296 of file ReachabilityGraph.hh.

empty()

bool Diades::Petri::ReachabilityGraph::empty ( ) const

inline

Return true if the graph is empty

Returns

the graph is empty

Definition at line 121 of file ReachabilityGraph.hh.

exportGraphToDot()

virtual bool Diades::Petri::ReachabilityGraph::exportGraphToDot ( const string &  fileDot )

virtual

Parameters

filedot

file suffixed (*.dot) input to DOT

Returns

true if the export succeeded

Reimplemented in Diades::Petri::TimeReachabilityGraph.

getId()

unsigned Diades::Petri::ReachabilityGraph::getId ( RState  state ) const

inline

Parameters

state

a RState of the ReachabilityGraph

Returns

the associated id

Precondition

state.valid() && state.owner() == graph()

Definition at line 325 of file ReachabilityGraph.hh.

References require.

getLabel()

const string& Diades::Petri::ReachabilityGraph::getLabel ( RTransition  transition )

inline

Parameters

state

a state of the graph

Returns

the set of marked places (labels)

Definition at line 87 of file ReachabilityGraph.hh.

References require.

getMarking()

const set<string>& Diades::Petri::ReachabilityGraph::getMarking ( RState  state )

inline

Parameters

state

a state of the graph

Returns

the set of marked places (labels)

Definition at line 66 of file ReachabilityGraph.hh.

References require.

getState()

RState Diades::Petri::ReachabilityGraph::getState

(

unsigned

id

)

Parameters

id	the id of the state to create

Returns

the state with the id 'id' (no creation if the state already exists)

Postcondition

BE AWARE the internal id of the returned state IS NOT 'id', use getId.

getTrans()

RTransition Diades::Petri::ReachabilityGraph::getTrans	(	RState	source,
		RState	target,
		const string &	label
	)

Parameters

source	the state of the source
target	the state of the target
label	the label

Returns

the transition of (source,target,label)

Precondition

source.valid() && source.owner()==_graph && target.valid() && target.owner()==_graph && !label.empty()

graph() [1/2]

Graph::Graph& Diades::Petri::ReachabilityGraph::graph ( )

inline

Returns

the underlying Graph

Definition at line 238 of file ReachabilityGraph.hh.

graph() [2/2]

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

inline

Returns

the underlying Graph

Definition at line 246 of file ReachabilityGraph.hh.

importTinaAut()

bool Diades::Petri::ReachabilityGraph::importTinaAut ( const string &  fileAut )

protected

Parameters

fileAut

automaton file suffixed (*.aut) generated by TINA

Returns

true if the import succeeded

Postcondition

if failure, the graph is empty

importTinaGraph()

bool Diades::Petri::ReachabilityGraph::importTinaGraph	(	const string &	fileAut,
		const string &	fileVrb
	)

Parameters

fileAut	automaton file suffixed (*.aut) generated by TINA
fileVrb	class file suffixed (*.vrb) generated by TINA

Returns

true if the import succeeded

Precondition

fileAut and fleVrb must be compatible files ! (fileVrb must contains the class description of the class in the automaton file)

Postcondition

if failure, the graph is empty

importTinaVrb()

virtual bool Diades::Petri::ReachabilityGraph::importTinaVrb ( const string &  fileVrb )

protectedvirtual

Parameters

fileVrb

class file suffixed (*.vrb) generated by TINA

Returns

true if the import succeeded

Postcondition

if failure, the graph is empty

initialState()

RState Diades::Petri::ReachabilityGraph::initialState ( ) const

inline

Definition at line 343 of file ReachabilityGraph.hh.

numberOfStates()

unsigned Diades::Petri::ReachabilityGraph::numberOfStates ( ) const

inline

Return the number of states in the graph.

Returns

number of states

Definition at line 101 of file ReachabilityGraph.hh.

numberOfTransitions()

unsigned Diades::Petri::ReachabilityGraph::numberOfTransitions ( ) const

inline

Return the number of transitions in the graph

Returns

number of transitions

Definition at line 111 of file ReachabilityGraph.hh.

outTransBegin() [1/2]

OutRTransitionIterator Diades::Petri::ReachabilityGraph::outTransBegin ( const RState &  state ) const

inline

Iterator on Transitions

Parameters

state

: a State

Precondition

state.valid() && state.owner() == graph()

Returns

a forward iterator pointing to the first output transition of state

Definition at line 256 of file ReachabilityGraph.hh.

outTransBegin() [2/2]

InRTransitionIterator Diades::Petri::ReachabilityGraph::outTransBegin ( const RState &  state )

inline

Iterator on Transitions

Parameters

state

: a State

Precondition

state.valid() && state.owner() == graph()

Returns

a forward iterator pointing to the first input transition of state

Definition at line 277 of file ReachabilityGraph.hh.

outTransEnd() [1/2]

OutRTransitionIterator Diades::Petri::ReachabilityGraph::outTransEnd ( const RState &  state ) const

inline

Iterator on Transitions

Parameters

node

: a State

Precondition

state.valid() && state.owner() == graph()

Returns

a forward iterator pointing to the end of all output transition of the state

Definition at line 266 of file ReachabilityGraph.hh.

outTransEnd() [2/2]

InRTransitionIterator Diades::Petri::ReachabilityGraph::outTransEnd ( const RState &  state )

inline

Iterator on Transitions

Parameters

node

: a State

Precondition

state.valid() && state.owner() == graph()

Returns

a forward iterator pointing to the end of all input transition of the state

Definition at line 287 of file ReachabilityGraph.hh.

setInitial()

void Diades::Petri::ReachabilityGraph::setInitial ( RState  state )

inline

Parameters

state

a RState

Precondition

state.valid() && state.owner() == graph() Set the state 'state' to be the initial state of the ReachabilityGraph

Definition at line 337 of file ReachabilityGraph.hh.

References require.

source()

RState Diades::Petri::ReachabilityGraph::source ( const RTransition &  trans ) const

inline

Source state of an Edge

Parameters

edge

an Edge

Precondition

edge.valid() && edge.owner() = this

Returns

the source Node of the Edge edge

Definition at line 143 of file ReachabilityGraph.hh.

stateBegin() [1/2]

RStateIterator Diades::Petri::ReachabilityGraph::stateBegin ( )

inline

Iterator for the states in the graph

Returns

start of iterator

Definition at line 157 of file ReachabilityGraph.hh.

stateBegin() [2/2]

RStateIterator Diades::Petri::ReachabilityGraph::stateBegin ( ) const

inline

Iterator for the states in the graph

Returns

start of iterator

Definition at line 175 of file ReachabilityGraph.hh.

stateEnd() [1/2]

RStateIterator Diades::Petri::ReachabilityGraph::stateEnd ( )

inline

Past-the-end iterator for the states of the graph.

Returns

end of iterator

Definition at line 166 of file ReachabilityGraph.hh.

stateEnd() [2/2]

RStateIterator Diades::Petri::ReachabilityGraph::stateEnd ( ) const

inline

Past-the-end iterator for the states of the graph.

Returns

end of iterator

Definition at line 184 of file ReachabilityGraph.hh.

target()

RState Diades::Petri::ReachabilityGraph::target ( const RTransition &  trans ) const

inline

Target Node of an Edge

Parameters

edge

an Edge

Precondition

edge.valid() && edge.owner() = this

Returns

the target Node of the Edge edge

Definition at line 132 of file ReachabilityGraph.hh.

transBegin() [1/2]

RTransitionIterator Diades::Petri::ReachabilityGraph::transBegin ( )

inline

Iterator for the transitions in the graph

Returns

start of iterator

Definition at line 193 of file ReachabilityGraph.hh.

transBegin() [2/2]

RTransitionIterator Diades::Petri::ReachabilityGraph::transBegin ( ) const

inline

Iterator for the transitions in the graph

Returns

start of iterator

Definition at line 213 of file ReachabilityGraph.hh.

transEnd() [1/2]

RTransitionIterator Diades::Petri::ReachabilityGraph::transEnd ( )

inline

Past-the-end iterator for the transitions of the graph.

Returns

end of iterator

Definition at line 203 of file ReachabilityGraph.hh.

transEnd() [2/2]

RTransitionIterator Diades::Petri::ReachabilityGraph::transEnd ( ) const

inline

Past-the-end iterator for the transitions of the graph.

Returns

end of iterator

Definition at line 223 of file ReachabilityGraph.hh.

typeName()

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

inlinestatic

Definition at line 27 of file ReachabilityGraph.hh.

Member Data Documentation

_dictionary

StateDictionnary Diades::Petri::ReachabilityGraph::_dictionary

private

the ids associated to the states

Definition at line 49 of file ReachabilityGraph.hh.

_graph

RGraph Diades::Petri::ReachabilityGraph::_graph

private

Definition at line 44 of file ReachabilityGraph.hh.

_id

Ids Diades::Petri::ReachabilityGraph::_id

private

the label associated to each RTransition of the

Definition at line 48 of file ReachabilityGraph.hh.

_initial

RState Diades::Petri::ReachabilityGraph::_initial

private

the underlying graph

Definition at line 45 of file ReachabilityGraph.hh.

_marking

Marking Diades::Petri::ReachabilityGraph::_marking

private

the initial state

Definition at line 46 of file ReachabilityGraph.hh.

_transLabel

TransitionLabel Diades::Petri::ReachabilityGraph::_transLabel

private

the marking associated to each RState of the graph

Definition at line 47 of file ReachabilityGraph.hh.

---

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

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