PetriNet.hh

Go to the documentation of this file.

#ifndef __DIADES__PETRI__PETRINET_HH_
#define __DIADES__PETRI__PETRINET_HH_

#include <sstream>
#include <graph/Graph.hh>
#include <graph/NodeMap.hh>
#include <utils/Substring.hh>
#include <set>
#include "PetriNetException.hh"
#include "Event.hh"



using namespace std;


namespace Diades
{
  namespace Petri
  {
        typedef Diades::Graph::Node Place;
        
        typedef  Diades::Graph::Node Transition;


        typedef  Diades::Graph::Edge Arc;


        
        class Zsl;
        class ZslFactory;
        class Vdd;
        class VddFactory;

        class PetriNet
        {
        protected:
          mutable ZslFactory * _zslFactory;
          mutable VddFactory * _vddFactory;



        public:

          typedef enum {P,T} NodeType;

          
        public:

          class Iterator
          {
          private:
                list<Arc>::const_iterator _it;
                bool _pre;
          public:
                Iterator(list<Arc>::const_iterator it, bool pre):
                  _it(it),_pre(pre){}

                Place operator *() const
                {
                  if(_pre)
                        {
                          return _it->source();
                        }
                  return _it->target();
                }

                Iterator & operator ++()
                {
                  ++_it;
                  return *this;
                }

                Iterator  operator ++(int)
                {
                  list<Arc>::const_iterator _it2= _it;
                  ++_it;
                  return Iterator(_it2,_pre);
                }

                Place operator ->(void) const
                {
                  if(_pre)
                        {
                          return _it->source();
                        }
                  return _it->target(); 
                }

                bool operator ==(const Iterator & it) const
                {
                  return (_pre == it._pre) && (_it == it._it);
                }

                
                bool operator !=(const Iterator & it) const
                {
                  return !(*this == it);
                }
          };

        public:

          class PerTypeIterator
          {

          private:
                Graph::NodeIterator _it;
                const PetriNet * _net;
                PetriNet::NodeType _type;

          public:
                PerTypeIterator(const PetriNet * net, Graph::NodeIterator it, PetriNet::NodeType type);

                Diades::Graph::Node operator *() const { return *_it; }

                Diades::Graph::Node operator ->(void) const { return *_it; }

                bool operator == (const PerTypeIterator & it) const
                {
                  return (_it == it._it) && (_net == it._net) && (_type == it._type);
                }

                bool operator != (const PerTypeIterator & it) const
                {
                  return !(*this == it);
                }

                PerTypeIterator & operator ++();

                PerTypeIterator  operator ++(int);
          };

          friend class Iterator;
          friend class PerTypeIterator;

        public:
          typedef PerTypeIterator TransitionIterator;

          typedef PerTypeIterator PlaceIterator;


          typedef set<Event>::const_iterator EventIterator;

          typedef set<Transition>::const_iterator TransitionEventIterator;

        protected:
          typedef enum{NotPostponable,Postponable} TransitionType; 
          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;
          mutable const Vdd * _initialMarking;
          set<Place> _explicitInitialMarking;
          unordered_map<string,Graph::Node> _placeOfLabel;
          vector<set<Transition> > _transitionsOfEventId;
          mutable Graph::NodeMap<const Zsl *> _preZslOfTransition;
          mutable Graph::NodeMap<const Zsl *> _incidenceZslOfTransition;
          mutable const Vdd * _reachableNodes;
          set<Event> _eventList;



        private:
          int _nbPlace;
          int _nbTrans;

        protected:
          mutable bool _readOnly;

        private:
          unsigned int _id;

        public:


          

          PetriNet();

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

          
          virtual ~PetriNet() {
                _graph.destroy();
          }






          void setName(const string & name)
          {
                require(PetriNetInvalid, !_readOnly, "setName: read only");
                if(!_readOnly) { _name = name; }
                else { printWarning("setName"); }
          }

          const string & name() const { return _name; }
          

          unsigned int id() const
          {
                return _id;
          }

          void setId(unsigned id)
          {
                _id = id;
          }

          int numberOfPlaces() const { return _nbPlace; }
          int numberOfTransitions() const { return _nbTrans; }

          void clear();

          const Diades::Graph::Graph & graph() const { return _graph; }




          
          EventIterator beginOfEvents() const
          {
                return _eventList.begin();
          }


          EventIterator endOfEvents() const
          {
                return _eventList.end();
          }

          const Event & getEvent(Transition t) const
          {
                require(PetriNetInvalid,t.valid(),"getEvent: invalid transition");
                require(PetriNetInvalid,t.owner() == _graph,"getEvent: the transition does not belong to the Petri Net");
                require(PetriNetInvalid, _nodeType[t] == T, "getEvent; this is not a transition but a place" );
                return _event[t];
          }

          virtual void setEvent(Transition t, const Event & event)
          {
                require(PetriNetInvalid,t.valid(),"setEvent: invalid transition");
                require(PetriNetInvalid,t.owner() == _graph,
                                "setEvent: the transition does not belong to the Petri Net");
                require(PetriNetInvalid, _nodeType[t] == T,
                                "setEvent; this is not a transition but a place" );
                require(PetriNetInvalid, !_readOnly, "setEvent: read only");
                if(!_readOnly)
                  {
                        _eventList.insert(event);
                        _event[t] = event;
                        if(_transitionsOfEventId.size() <= event.id())
                          {
                                _transitionsOfEventId.resize(event.id()+1);
                          }
                        _transitionsOfEventId[event.id()].insert(t);
                  }
                else
                  {
                        printWarning("setEvent");
                  }
          }


          bool containsEvent(const Event & event) const
          {
                if(_transitionsOfEventId.size() <= event.id())
                  {
                        return false;
                  }
                return !_transitionsOfEventId[event.id()].empty();
          }



          Place newPlace() {
                require(PetriNetInvalid, !_readOnly, "newPlace: read only");
                Place p;
                if(!_readOnly)
                  {
                        ++_nbPlace;
                        p = _graph.newNode();
                        _nodeType[p] = P;
                        stringstream s;
                        s << "__p" << p.id();
                        s >> _labelNode[p];
                        _infoNode[p] = "";
                  }
                else
                  {
                        printWarning("newPlace");
                  }
                ensure(PetriNetInvalid, p.valid(), "newPlace: invalid returned place");
                ensure(PetriNetInvalid, p.owner() == graph(), "newPlace: invalid returned place");
                return p;
          }

          Place newPlace(const string & label);





          PlaceIterator beginOfPlaces() const
          {
                return PerTypeIterator(this,_graph.nodeBegin(),P);
          }
          

          PlaceIterator endOfPlaces() const
          {
                return PerTypeIterator(this,_graph.nodeEnd(),P);
          }




          const string & labelOfPlace(const Place & p) const
          {
                return _labelNode[p];
          }

          const string & getInfoLabel(Place p) const
          {
                require(PetriNetInvalid,p.valid(),"getInfoLabel: invalid place");
                require(PetriNetInvalid,p.owner() == _graph,"getInfoLabel: the place does not belong to the Petri Net");
                require(PetriNetInvalid, _nodeType[p] == P, "getInfoLabel: this is not a place but a transition" );
                return _infoNode[p];
          }



          void setInfoLabel(Place p, const string & info)
          {
                require(PetriNetInvalid,p.valid(),"setInfoLabel: invalid place");
                require(PetriNetInvalid,p.owner() == _graph,"setInfoLabel: the place does not belong to the Petri Net");
                require(PetriNetInvalid, _nodeType[p] == P, "setInfoLabel: this is not a place but a transition" );
                require(PetriNetInvalid, !_readOnly, "setInfoLabel: read only");
                _infoNode[p] = info;
          }









          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)
          {
                require(PetriNetInvalid, !_readOnly, "newTransition: read only");
                Transition trans;
                if(!_readOnly)
                  {
                        trans = newTransition(pre,post); _labelNode[trans] = label;
                  }
                else
                  {
                        printWarning("newTransition");
                  }
                return trans;
          }

          void addPre(Transition transition, Place place)
          {
                _graph.newEdge(place,transition);
          }

          void addPost(Transition transition, Place place)
          {
                _graph.newEdge(transition,place);
          }

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

          //    /**
          //    * @param marking a possible marking of the PetriNet
          //    * @param t a Transition
          //    * @return true if the marking 'marking' is possible after firing the Transition 't'
          //    * @pre marking.owner() == this
          //    */
          //    bool post(const Vdd * marking, const Transition & t) const;




          Iterator preBegin(const Transition & transition) const
          {
                return Iterator(transition.inEdgeBegin(),true);
          }
          
          Iterator preEnd(const Transition & transition) const
          {
                return Iterator(transition.inEdgeEnd(),true);
          }
          
          Iterator postBegin(const Transition & transition) const
          {
                return Iterator(transition.outEdgeBegin(),false);
          }

          
          Iterator postEnd(const Transition & transition) const
          {
                return Iterator(transition.outEdgeEnd(),false);
          }


          TransitionIterator beginOfTransitions() const
          {
                return PerTypeIterator(this,_graph.nodeBegin(),T);
          }


          TransitionIterator endOfTransitions() const
          {
                return PerTypeIterator(this,_graph.nodeEnd(),T);
          }


          const string & labelOfTransition(const Transition &  t) const
          {
                return _labelNode[t];
          }

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

          TransitionEventIterator beginOfTransitionWithEvent(const Event & event) const
          {
                require(PetriNetInvalid,containsEvent(event),
                                "beginOfTransitionWithEvent: the event is not associated to a transition of this Petri Net");
                return _transitionsOfEventId[event.id()].begin();
          }



          TransitionEventIterator endOfTransitionWithEvent(const Event & event) const
          {
                require(PetriNetInvalid,containsEvent(event),
                                "endOfTransitionWithEvent: the event is not associated to a transition of this Petri Net");
                return _transitionsOfEventId[event.id()].end();
          }


          virtual void deleteTransition(Transition t);

          virtual Transition duplicateTransition(Transition t);






          
          void setPostponable(Transition t);

          bool isPostponable(Transition t) const
          {
                require(PetriNetInvalid, t.valid(),"isPostponable: invalid transition");
                require(PetriNetInvalid, t.owner() == graph(), "isPostponable: the transition does not belong to the Petri Net");
                return _postponable[t] == Postponable;
          }

          void setNotPostponable(Transition t);


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





          void setMarking(const set<Place> & marking);
          
          bool isMarked() const
          {
                return _initialMarking != 0;
          }


          bool isMarked(Place p) const;


          void mark(Place p);


          void unmark(Place p);
          
          



          
          virtual void net2Dot(const string & fileName) const;


          virtual void net2Tina(ostream & os) const;
          

          void printWarning(const string & s) const
          {
                cerr << "WARNING: attempt to modify a read-only net (" << s << ")" << endl;
          }

          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
          {
                return _zslFactory;
          }
          

          VddFactory * vddFactory() const
          {
                return _vddFactory;
          }


        };

  };

};

#endif