ReachabilityGraph.hh

Go to the documentation of this file.

#ifndef __DIADES__PETRI__REACHABILITYGRAPH__HH
#define __DIADES__PETRI__REACHABILITYGRAPH__HH

#include <string>
#include <set>
#include <unordered_map>
#include <diades/utils/Exceptions.hh>
#include <diades/utils/Interval.hh>
#include <diades/graph/Graph.hh>
#include <diades/graph/NodeMap.hh>
#include <diades/graph/EdgeMap.hh>

using namespace std;

namespace Diades
{
  namespace Petri
  {
        class ReachabilityGraph
        {
        public:
          static string typeName() { return "Diades::Petri::ReachabilityGraph"; }
          typedef Diades::Utils::Exception<ReachabilityGraph> Exception;

        public:
          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;
          
        private:
          RGraph _graph;    
          RState _initial;  
          Marking _marking; 
          TransitionLabel _transLabel; 
          Ids _id; 
          StateDictionnary _dictionary; 
          
        public:
          ReachabilityGraph():_graph(),_initial(),_marking(),_transLabel(),_id(),_dictionary()
          {
                _marking.init(_graph);
                _transLabel.init(_graph);
                _id.init(_graph);
          }
          virtual ~ReachabilityGraph()
          {
          }

          const set<string> & getMarking(RState state)
          {
                require(Exception,state.valid() && &state.owner()==&_graph,"getMarking: invalid state");
                return _marking[state];
          }

          void addMarking(RState state, const string & mark)
          {
                require(Exception,state.valid() && &state.owner()==&_graph,"addMarking: invalid state");
                require(Exception,!mark.empty(),"addMarking: empty label");
                _marking[state].insert(mark);
          }

          const string & getLabel(RTransition transition)
          {
                require(Exception,transition.valid() && &transition.owner()==&_graph,"getLabel: invalid transition");
                return _transLabel[transition];
          }
          
         


          unsigned numberOfStates() const
          {
                return _graph.numberOfNodes();
          }
  
          unsigned numberOfTransitions() const
          {
                return _graph.numberOfEdges();
          }
  
          bool empty() const
          {
                return _graph.empty();
          }


          RState  target(const RTransition & trans) const
          {
                return _graph.target(trans);
          }
          

          RState  source(const RTransition & trans) const
          {
                return _graph.source(trans);
          }


          RStateIterator stateBegin() {
                return _graph.nodeBegin();
          }

          RStateIterator stateEnd()  {
                return  _graph.nodeEnd();
          }

          RStateIterator stateBegin() const {
                return _graph.nodeBegin();
          }

          RStateIterator stateEnd()  const {
                return  _graph.nodeEnd();
          }

          RTransitionIterator transBegin()
          {
                return _graph.edgeBegin();
          }

          RTransitionIterator transEnd()
          {
                return _graph.edgeEnd();
          }

          RTransitionIterator transBegin() const
          {
                return _graph.edgeBegin();
          }

          RTransitionIterator transEnd() const
          {
                return _graph.edgeEnd();
          }


          
          virtual void addTimeConstraint(RState state, const string & transitionName, const Diades::Utils::Interval & interval)
          {
          }
                
          Graph::Graph & graph() 
          {
                return _graph;
          }
          
          const Graph::Graph & graph() const
          {
                return _graph;
          }
          
          OutRTransitionIterator outTransBegin(const RState & state) const
          {
                return _graph.outEdgeBegin(state);
          }

          OutRTransitionIterator outTransEnd(const RState & state) const
          {
                return _graph.outEdgeEnd(state);
          }


          InRTransitionIterator outTransBegin(const RState & state)
          {
                return _graph.inEdgeBegin(state);
          }

          InRTransitionIterator outTransEnd(const RState & state)
          {
                return _graph.inEdgeEnd(state);
          }


          void clear()
          {
                _graph.clear();
          }


          RState getState(unsigned id);

          
          RTransition getTrans(RState source,RState target, const string & label);


          unsigned getId(RState state) const
          {
                require(Exception, state.valid() && &state.owner() == &graph(),"getId: invalid state");
                return _id[state];
          }
          

          void setInitial(RState state)
          {
                require(Exception, state.valid() && &state.owner() == &graph(),"setInitial: invalid state");
                _initial = state;
          }

          RState initialState() const
          {
                return _initial;
          }
          

          bool importTinaGraph(const string & fileAut, const string & fileVrb);



          virtual bool exportGraphToDot(const string & fileDot);
          
          
        protected:
          bool importTinaAut(const string & fileAut);
          virtual  bool importTinaVrb(const string & fileVrb);


        };




  };
};

#endif