Net.hh

Go to the documentation of this file.

#ifndef __DIADES__PETRI__NET_HH_
#define __DIADES__PETRI__NET_HH_

#include <sstream>
#include <diades/graph/Graph.hh>
#include <diades/graph/ConstNodeMap.hh>
#include <diades/graph/NodeMap.hh>
#include <diades/utils/Substring.hh>
#include <diades/utils/Exceptions.hh>
#include <set>
#include <diades/petri/PetriEventManager.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 Net
        {
        public:

          static string typeName() { return "Diades::Petri::Net"; }

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


          
        protected:
          mutable ZslFactory * _zslFactory;
          mutable VddFactory * _vddFactory;



        public:

          typedef enum {P,T} NodeType;

          
        public:

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

                const Place &  operator *() const
                {
                  if(_pre)
                        {
                          return _it->sourceRef();
                        }
                  return _it->targetRef();
                }

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

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

                const Place * operator ->(void) const
                {
                  if(_pre)
                    {
                      return &_it->sourceRef();
                    }
                  return &_it->targetRef(); 
                }

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

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

        public:

          class PerTypeIterator
          {

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

          public:
                PerTypeIterator(const Net * net, Graph::NodeIterator it, Net::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::ConstNodeMap<const Zsl *> _preZslOfTransition;
          mutable Graph::ConstNodeMap<const Zsl *> _incidenceZslOfTransition;
          mutable const Vdd * _reachableNodes;
          set<Event> _eventList;
          


        private:
          size_t _nbPlaces;
          size_t _nbTransitions;

        protected:
          mutable bool _readOnly;

        private:
          unsigned int _id;

        public:


          

          Net();

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

          
          virtual ~Net() {
          }






          void setName(const string & name)
          {
                require(Exception, !_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;
          }


          
          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(Exception,t.valid(),"getEvent: invalid transition");
                require(Exception,&t.owner() == &_graph,"getEvent: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[t] == T, "getEvent; this is not a transition but a place" );
                return _event[t];
          }

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


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



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


          Place newPlace(const string & label);



          void setLabelOfPlace(const Place & place, const string & label)
          {
                require(Exception, !_readOnly, "setLabelOfPlace: read only");
                require(Exception,_placeOfLabel.find(label) == _placeOfLabel.end(),
                                "setLabelOfPlace: this label already exists in the net");
                _labelNode[place] = label;
                _placeOfLabel[label] = place;
          }



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

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


          size_t numberOfPlaces() const
          {
                return _nbPlaces;
          }


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

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



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









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


          


          virtual Transition newTransition(const set<Place> & pre, const set<Place> & post);


        public:
          virtual Transition newTransition(const set<Place> & pre, const set<Place> & post, const string & label)
          {
                require(Exception, !_readOnly, "newTransition: read only");
                Transition trans;
                if(!_readOnly)
                  {
                        trans = newTransition(pre,post);
                        setLabelOfTransition(trans,label);
                  }
                else
                  {
                        printWarning("newTransition");
                  }
                return trans;
          }

          
          size_t numberOfTransitions() const
          {
                return _nbTransitions;
          }

          size_t numberOfArcs() const
          {
            return _graph.numberOfEdges();
          }
          
          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 Net
          //    * @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;


          ConstIterator preTransBegin(const Place & place) const
          {
                return ConstIterator(place.inEdgeBegin(),true);
          }


          ConstIterator preTransEnd(const Place & place) const
          {
                return ConstIterator(place.inEdgeEnd(),true);
          }

          ConstIterator postTransBegin(const Place & place) const
          {
                return ConstIterator(place.outEdgeBegin(),false);
          }


          ConstIterator postTransEnd(const Place & place) const
          {
                return ConstIterator(place.outEdgeEnd(),false);
          }

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

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


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


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


          void setLabelOfTransition(const Transition & t, const string & label)
          {
                require(Exception, !_readOnly, "setLabelOfTransition: read only");
                _labelNode[t] = label;
          }

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

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

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



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


          virtual void deleteTransition(Transition t);

          virtual Transition duplicateTransition(Transition t);






          
          void setPostponable(Transition t);

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

          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
          {
                return _initialMarking != 0;
          }


          bool isMarked(Place p) const;


          void mark(Place p);


          void unmark(Place p);


          const set<Place> & initialMarking() const
          {
                return _explicitInitialMarking;
          }


          
          



          
          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