BoundedNet.hh

Go to the documentation of this file.

#ifndef __DIADES__PETRI__BOUNDEDNET_HH_
#define __DIADES__PETRI__BOUNDEDNET_HH_

#include <sstream>
#include <diades/graph/Graph.hh>
#include <diades/graph/NodeMap.hh>
#include <diades/utils/Substring.hh>
#include <diades/utils/Exceptions.hh>
#include <set>
#include <unordered_set>
#include <diades/petri/Marking.hh>
#include <diades/graph/Utils.hh>

using namespace std;


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

        typedef Diades::Graph::Node Transition;


        typedef Diades::Graph::Edge Arc;

        class BoundedNet {
        public:

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

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



        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:
                Diades::Graph::NodeIterator _it;
                const BoundedNet * _net;
                BoundedNet::NodeType _type;

            public:
                PerTypeIterator(const BoundedNet * net, Diades::Graph::NodeIterator it, BoundedNet::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<Transition>::const_iterator TransitionEventIterator;


        protected:

            typedef enum {
                NotPostponable, Postponable
            } TransitionType; 
            Diades::Graph::Graph _graph;
            Diades::Graph::NodeMap<NodeType> _nodeType;
            Diades::Graph::NodeMap<string> _nameOfNode;
            Diades::Graph::NodeMap<string> _labelOfNode;
            Diades::Graph::NodeMap<int> _postponable;
            Diades::Graph::NodeMap<std::unordered_set<Transition>> _inhibitors;
                        Diades::Graph::NodeMap<std::unordered_set<Place>> _inhibited;
            string _name;
            Marking _initialMarking;
            unordered_map<string, Diades::Graph::Node> _placeOfName;
            unordered_map<string, Diades::Graph::Node> _transitionOfName;




        private:
            size_t _nbPlaces;
            size_t _nbTransitions;


        protected:


        private:
            unsigned int _id;

        public:




            BoundedNet();

            BoundedNet(const BoundedNet & net);


            BoundedNet & operator=(const BoundedNet & net);




            BoundedNet & append(const BoundedNet & net);

            virtual ~BoundedNet() {
            }





            void setName(const string & name) {
                require(Exception, !name.empty(), "setName: the given name is empty.");
                _name = name;

            }

            const string & name() const {
                ensure(Exception, !_name.empty(), "name: empty name -> invalid net");
                return _name;
            }

            unsigned int id() const {
                return _id;
            }

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



            void clear();

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



            Place newPlace() {

                Place p;

                ++_nbPlaces;
                p = _graph.newNode();
                _nodeType[p] = P;
                stringstream s;
                s << "__p" << p.id();
                _labelOfNode[p] = "";
                setNameOfPlace(p, s.str());
                ensure(Exception, p.valid(), "newPlace: invalid returned place");
                ensure(Exception, &p.owner() == &graph(), "newPlace: invalid returned place");
                return p;
            }


            Place newPlace(const string & name);

            void deletePlace(Place p);

            void setLabelOfPlace(Place place, const string & label) {
                require(Exception, place.valid(), "setLabelOfPlace: invalid place");
                require(Exception, &place.owner() == &graph(),
                        "setLabelOfPLace: this place is not own by the current net");
                require(Exception, _nodeType[place] == P, "setLabelOfPlace: this is not a place but a transition");
                _labelOfNode[place] = label;
            }

            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 {
                require(Exception, p.valid(), "labelOfPlace: invalid place");
                require(Exception, &p.owner() == &graph(),
                        "labelOfPLace: this place is not own by the current net");
                require(Exception, _nodeType[p] == P, "labelOfPlace: this is not a place but a transition");
                return _labelOfNode[p];
            }

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

            void setNameOfPlace(Place p, const string & name) {
                require(Exception, p.valid(), "setNameOfPlace: invalid place");
                require(Exception, &p.owner() == &_graph, "setNameOfPlace: the place does not belong to the Petri Net");
                require(Exception, _nodeType[p] == P, "setNameOfPlace: this is not a place but a transition");
                if (_placeOfName.find(name) == _placeOfName.end()) {
                    _nameOfNode[p] = name;
                    _placeOfName[name] = p;
                }
            }

            Place getPlace(const string & name) const {
                auto it = _placeOfName.find(name);
                if (it == _placeOfName.end()) {
                    return Place();
                }
                return it->second;
            }






            Arc getArc(Diades::Graph::Node n1, Diades::Graph::Node n2) const;


            virtual bool enables(Transition t, const Marking & marking) const;



            virtual bool fire(Transition t, const Marking & marking, Marking & newMarking) const;



            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 & name) {
                require(Exception, !name.empty(), "newTransition: empty name");
                Transition trans;
                if (_transitionOfName.find(name) == _transitionOfName.end()) {
                    trans = newTransition(pre, post);
                    setNameOfTransition(trans, name);
                }
                return trans;
            }

            virtual void setInhibition(Place p, Transition t) {
                require(Exception, p.valid(), "setInhibition: invalid place");
                require(Exception, &p.owner() == &_graph, "setInhibition: the place does not belong to the Petri Net");
                require(Exception, _nodeType[p] == P, "setInhibition: this is not a place but a transition");
                require(Exception, t.valid(), "setInhibition: invalid transition");
                require(Exception, &t.owner() == &_graph, "setInhibition: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[t] == T, "setInhibition: this is not a transition but a place");
                _inhibitors[p].insert(t);
                                _inhibited[t].insert(p);
            }

            const std::unordered_set<Transition> & inhibitors(Place p) const {
                return _inhibitors[p];
            }

            virtual void unsetInhibition(Place p, Transition t) {
                require(Exception, p.valid(), "unsetInhibition: invalid place");
                require(Exception, &p.owner() == &_graph, "unsetInhibition: the place does not belong to the Petri Net");
                require(Exception, _nodeType[p] == P, "unsetInhibition: this is not a place but a transition");
                require(Exception, t.valid(), "unsetInhibition: invalid transition");
                require(Exception, &t.owner() == &_graph, "unsetInhibition: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[t] == T, "unsetInhibition: this is not a transition but a place");
                _inhibitors[p].erase(t);
                                _inhibited[t].erase(p);
            }

            bool inhibits(Place p, Transition t) const {
                require(Exception, p.valid(), "inhibits: invalid place");
                require(Exception, &p.owner() == &_graph, "inhibits: the place does not belong to the Petri Net");
                require(Exception, _nodeType[p] == P, "inhibits: this is not a place but a transition");
                require(Exception, t.valid(), "inhibits: invalid transition");
                require(Exception, &t.owner() == &_graph, "inhibits: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[t] == T, "inhibits: this is not a transition but a place");
                return _inhibitors[p].find(t) != _inhibitors[p].end();
            }

            size_t numberOfTransitions() const {
                return _nbTransitions;
            }

            size_t numberOfArcs() const {
                return _graph.numberOfEdges();
            }

            void addPre(Transition transition, Place place) {
                require(Exception, place.valid(), "addPre: invalid place");
                require(Exception, &place.owner() == &_graph, "addPre: the place does not belong to the Petri Net");
                require(Exception, _nodeType[place] == P, "addPre: this is not a place but a transition");
                require(Exception, transition.valid(), "addPre: invalid transition");
                require(Exception, &transition.owner() == &_graph, "addPre: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[transition] == T, "addPre: this is not a transition but a place");
                _graph.newEdge(place, transition);
            }

            void addPost(Transition transition, Place place) {
                require(Exception, place.valid(), "addPost: invalid place");
                require(Exception, &place.owner() == &_graph, "addPost: the place does not belong to the Petri Net");
                require(Exception, _nodeType[place] == P, "addPost: this is not a place but a transition");
                require(Exception, transition.valid(), "addPost: invalid transition");
                require(Exception, &transition.owner() == &_graph, "addPost: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[transition] == T, "addPost: this is not a transition but a place");
                _graph.newEdge(transition, place);
            }

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

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

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

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

            ConstIterator preBegin(Transition transition) const {
                require(Exception, transition.valid(), "preBegin: invalid transition");
                require(Exception, &transition.owner() == &_graph, "preBegin: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[transition] == T, "preBegin: this is not a transition but a place");
                return ConstIterator(transition.inEdgeBegin(), true);
            }

            ConstIterator preEnd(Transition transition) const {
                require(Exception, transition.valid(), "preEnd: invalid transition");
                require(Exception, &transition.owner() == &_graph, "preEnd: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[transition] == T, "preEnd: this is not a transition but a place");
                return ConstIterator(transition.inEdgeEnd(), true);
            }

            ConstIterator postBegin(Transition transition) const {
                require(Exception, transition.valid(), "postBegin: invalid transition");
                require(Exception, &transition.owner() == &_graph, "postBegin: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[transition] == T, "postBegin: this is not a transition but a place");

                return ConstIterator(transition.outEdgeBegin(), false);
            }

            ConstIterator postEnd(Transition transition) const {
                require(Exception, transition.valid(), "postEnd: invalid transition");
                require(Exception, &transition.owner() == &_graph, "postEnd: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[transition] == T, "postEnd: this is not a transition but a place");

                return ConstIterator(transition.outEdgeEnd(), false);
            }

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

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

            void setNameOfTransition(Transition transition, const string & name) {
                require(Exception, transition.valid(), "setNameOfTransition: invalid transition");
                require(Exception, &transition.owner() == &_graph, "setNameOfTransition: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[transition] == T, "setNameOfTransition: this is not a transition but a place");
                require(Exception, !name.empty(), "setNameOfTransition: empty name");
                if (_transitionOfName.find(name) == _transitionOfName.end()) {
                    _nameOfNode[transition] = name;
                    _transitionOfName[name] = transition;
                }
            }

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

            Transition transitionOfName(const string & name) const {
                require(Exception, !name.empty(), "transitionOfName: empty name");
                auto it = _transitionOfName.find(name);
                if (it == _transitionOfName.end()) {
                    return Transition();
                }
                return it->second;
            }

            bool inPre(Transition t, Place p) const;


            bool inPost(Transition t, Place p) const;


            virtual void deleteTransition(Transition t);

            virtual Transition duplicateTransition(Transition t);











            const Marking & initialMarking() const {
                return _initialMarking;
            }

            Marking & initialMarking() {
                return _initialMarking;
            }

            bool isMarked() const {
                return !_initialMarking.empty();
            }







            virtual void net2Dot(const string & fileName) const;



            void net2Tina(ostream & os) const;

            void net2Tina(const string & filename) const;

            void printPrettyMarking(ostream & os, const Marking & marking) const;

        protected:
                        
                        
            void net2TinaWithHeader(ostream & os, const string & netHeader) const;
                        

            virtual void writeEndOfDotFile(ostream & os) const {
            }

            virtual void nameOfTransition2Dot(ostream & os, Transition transition) const {
                require(Exception, transition.valid(), "nameOfTransition2Dot: invalid transition");
                require(Exception, &transition.owner() == &_graph, "nameOfTransition2Dot: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[transition] == T, "nameOfTransition2Dot: this is not a transition but a place");
            }

            virtual void net2TinaEnd(ostream & os, const string & header) const {
                os << header << " " << name() << "\n";
            }

            virtual void net2TinaTransition(ostream & os,
                    Transition trans) const;

            virtual void net2TinaTransitionInterval(ostream & os,
                    Transition transition) const {
                require(Exception, transition.valid(), "net2TinaTransitionInterval: invalid transition");
                require(Exception, &transition.owner() == &_graph, "net2TinaTransitionInterval: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[transition] == T, "net2TinaTransitionInterval: this is not a transition but a place");

                os << " [0,w[ ";
            }

            virtual void net2TinaTransitionName(ostream & os, Transition transition) const {
                require(Exception, transition.valid(), "net2TinaTransitionInterval: invalid transition");
                require(Exception, &transition.owner() == &_graph, "net2TinaTransitionInterval: the transition does not belong to the Petri Net");
                require(Exception, _nodeType[transition] == T, "net2TinaTransitionInterval: this is not a transition but a place");

            }



            virtual void copyNet(const BoundedNet & net,
                    Diades::Graph::ConstNodeMap<Diades::Graph::Node> & nodeMap,
                    Diades::Graph::NodeMap<Diades::Graph::Node> & nodeMapCopy,
                    Diades::Graph::ConstEdgeMap<Diades::Graph::Edge> & edgeMap,
                    Diades::Graph::EdgeMap<Diades::Graph::Edge> & edgeMapCopy);

        public:

            virtual void appendNet(const BoundedNet & net,
                    Diades::Graph::ConstNodeMap<Diades::Graph::Node> & nodeMap,
                    Diades::Graph::NodeMap<Diades::Graph::Node> & nodeMapCopy,
                    Diades::Graph::ConstEdgeMap<Diades::Graph::Edge> & edgeMap,
                    Diades::Graph::EdgeMap<Diades::Graph::Edge> & edgeMapCopy);

                        
                        template<typename Iterator>
                        Place mergePlaces(Iterator first, Iterator last)
                        {
                                if(first != last)
                                {
                                Place result = newPlace();
                                while(first != last)
                                {
                                        Place current = *first;
                                        ++first;
                                        while(!inhibitors(current).empty())
                                        {       
                                                auto transition = *inhibitors(current).begin();
                                                setInhibition(result,transition);
                                                unsetInhibition(current,transition);
                                        }
                                        if(initialMarking().getMark(current)!=0)
                                        {
                                                initialMarking().mark(result,initialMarking().getMark(result) + initialMarking().getMark(current));
                                                initialMarking().unmark(current);
                                        }
                                        if(!labelOfPlace(current).empty())
                                        {
                                                setLabelOfPlace(result,labelOfPlace(result)+ " " + labelOfPlace(current));
                                        }
                                        for(auto it = preTransBegin(current); it != preTransEnd(current); ++it)
                                        {
                                                addPost(*it,result);
                                        }
                                        for(auto it = postTransBegin(current); it != postTransEnd(current); ++it)
                                        {
                                                addPre(*it,result);
                                        }
                                        deletePlace(current);
                                }
                                return result;
                                }
                                else
                                {
                                        return *beginOfPlaces();
                                }
                        }
                        
                        

        };

    };

};

#endif