DiaDes
0.1
DIAgnosis of Discrete-Event System
|
#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... | |
Reachability graph of a Petri Net. Enumerative structure used by Houssam-Eddine Gougam for time analysis.
Definition at line 24 of file ReachabilityGraph.hh.
Definition at line 28 of file ReachabilityGraph.hh.
typedef Diades::Graph::NodeMap< unsigned > Diades::Petri::ReachabilityGraph::Ids |
Definition at line 36 of file ReachabilityGraph.hh.
Definition at line 39 of file ReachabilityGraph.hh.
typedef Diades::Graph::NodeMap< set<string> > Diades::Petri::ReachabilityGraph::Marking |
Definition at line 34 of file ReachabilityGraph.hh.
Definition at line 40 of file ReachabilityGraph.hh.
Definition at line 31 of file ReachabilityGraph.hh.
Definition at line 32 of file ReachabilityGraph.hh.
Definition at line 37 of file ReachabilityGraph.hh.
Definition at line 33 of file ReachabilityGraph.hh.
Definition at line 38 of file ReachabilityGraph.hh.
typedef unordered_map<unsigned,RState> Diades::Petri::ReachabilityGraph::StateDictionnary |
Definition at line 41 of file ReachabilityGraph.hh.
typedef Diades::Graph::EdgeMap< string > Diades::Petri::ReachabilityGraph::TransitionLabel |
Definition at line 35 of file ReachabilityGraph.hh.
|
inline |
state dictionary
Definition at line 52 of file ReachabilityGraph.hh.
|
inlinevirtual |
Definition at line 58 of file ReachabilityGraph.hh.
|
inline |
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.
|
inlinevirtual |
Reimplemented in Diades::Petri::TimeReachabilityGraph.
Definition at line 230 of file ReachabilityGraph.hh.
|
inline |
Clear the graph
Definition at line 296 of file ReachabilityGraph.hh.
|
inline |
Return true if the graph is empty
Definition at line 121 of file ReachabilityGraph.hh.
|
virtual |
filedot | file suffixed (*.dot) input to DOT |
Reimplemented in Diades::Petri::TimeReachabilityGraph.
|
inline |
state | a RState of the ReachabilityGraph |
Definition at line 325 of file ReachabilityGraph.hh.
References require.
|
inline |
state | a state of the graph |
Definition at line 87 of file ReachabilityGraph.hh.
References require.
|
inline |
state | a state of the graph |
Definition at line 66 of file ReachabilityGraph.hh.
References require.
RState Diades::Petri::ReachabilityGraph::getState | ( | unsigned | id | ) |
id | the id of the state to create |
RTransition Diades::Petri::ReachabilityGraph::getTrans | ( | RState | source, |
RState | target, | ||
const string & | label | ||
) |
source | the state of the source |
target | the state of the target |
label | the label |
|
inline |
Definition at line 238 of file ReachabilityGraph.hh.
|
inline |
Definition at line 246 of file ReachabilityGraph.hh.
|
protected |
fileAut | automaton file suffixed (*.aut) generated by TINA |
bool Diades::Petri::ReachabilityGraph::importTinaGraph | ( | const string & | fileAut, |
const string & | fileVrb | ||
) |
fileAut | automaton file suffixed (*.aut) generated by TINA |
fileVrb | class file suffixed (*.vrb) generated by TINA |
|
protectedvirtual |
fileVrb | class file suffixed (*.vrb) generated by TINA |
|
inline |
Definition at line 343 of file ReachabilityGraph.hh.
|
inline |
Return the number of states in the graph.
Definition at line 101 of file ReachabilityGraph.hh.
|
inline |
Return the number of transitions in the graph
Definition at line 111 of file ReachabilityGraph.hh.
|
inline |
Iterator on Transitions
state | : a State |
Definition at line 256 of file ReachabilityGraph.hh.
|
inline |
Iterator on Transitions
state | : a State |
Definition at line 277 of file ReachabilityGraph.hh.
|
inline |
Iterator on Transitions
node | : a State |
Definition at line 266 of file ReachabilityGraph.hh.
|
inline |
Iterator on Transitions
node | : a State |
Definition at line 287 of file ReachabilityGraph.hh.
|
inline |
state | a RState |
Definition at line 337 of file ReachabilityGraph.hh.
References require.
|
inline |
Source state of an Edge
edge | an Edge |
Definition at line 143 of file ReachabilityGraph.hh.
|
inline |
Iterator for the states in the graph
Definition at line 157 of file ReachabilityGraph.hh.
|
inline |
Iterator for the states in the graph
Definition at line 175 of file ReachabilityGraph.hh.
|
inline |
Past-the-end iterator for the states of the graph.
Definition at line 166 of file ReachabilityGraph.hh.
|
inline |
Past-the-end iterator for the states of the graph.
Definition at line 184 of file ReachabilityGraph.hh.
|
inline |
Target Node of an Edge
edge | an Edge |
Definition at line 132 of file ReachabilityGraph.hh.
|
inline |
Iterator for the transitions in the graph
Definition at line 193 of file ReachabilityGraph.hh.
|
inline |
Iterator for the transitions in the graph
Definition at line 213 of file ReachabilityGraph.hh.
|
inline |
Past-the-end iterator for the transitions of the graph.
Definition at line 203 of file ReachabilityGraph.hh.
|
inline |
Past-the-end iterator for the transitions of the graph.
Definition at line 223 of file ReachabilityGraph.hh.
|
inlinestatic |
Definition at line 27 of file ReachabilityGraph.hh.
|
private |
the ids associated to the states
Definition at line 49 of file ReachabilityGraph.hh.
|
private |
Definition at line 44 of file ReachabilityGraph.hh.
|
private |
the label associated to each RTransition of the
Definition at line 48 of file ReachabilityGraph.hh.
|
private |
the underlying graph
Definition at line 45 of file ReachabilityGraph.hh.
|
private |
the initial state
Definition at line 46 of file ReachabilityGraph.hh.
|
private |
the marking associated to each RState of the graph
Definition at line 47 of file ReachabilityGraph.hh.