LabelledNet.hh

Go to the documentation of this file.

#ifndef __DIADES_PETRI_LABELLEDNET__HH__
#define __DIADES_PETRI_LABELLEDNET__HH__

#include<unordered_set>
#include<diades/graph/ConstNodeMap.hh>
#include<diades/petri/PetriEventManager.hh>
#include<diades/petri/BoundedNet.hh>


namespace Diades {
    namespace Petri {
                using Diades::Utils::Msg;
                
        class LabelledNet : public BoundedNet {
        public:

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

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

                        typedef PetriEventManager::EventId Event;


            typedef set<Event>::const_iterator EventIterator;

            typedef unordered_set<Transition>::const_iterator TransitionEventIterator;

        private:
            unordered_map<Event, unordered_set<Transition> > _eventTransitions;
            set<Event> _eventList;
            Diades::Graph::ConstNodeMap<Event> _event;
            Event _lambda;


        public:

            Event
            lambda() const {
                return _lambda;
            }

            typedef unordered_set<Transition>::const_iterator EventTransitionIterator;

            LabelledNet() : BoundedNet(),
            _eventTransitions(),
            _eventList(),
            _event(),
            _lambda(PetriEventManager::petriEventManager().temporalEvent()) {
                _event.init(graph());
            }


            LabelledNet(const LabelledNet & net);



            LabelledNet & operator=(const LabelledNet & net);


            LabelledNet & append(const LabelledNet & net);




            LabelledNet(const LabelledNet & lpn1, const LabelledNet & lpn2, const unordered_set<Event> & syncEvents);

            LabelledNet & merge(const LabelledNet & lpn1, const LabelledNet & lpn2,
                    const unordered_set<Event> & syncEvents,
                    std::unordered_map< Transition, std::list<Transition> > & lpn1SyncTrans,
                    std::unordered_map< Transition, std::list<Transition> > & lpn2SyncTrans,
                    unordered_map<Transition, std::pair<Transition, Transition>> &synchronisations,
                                        std::unordered_map< Place, Place > & lpn1Place,
                                std::unordered_map< Place, Place > & lpn2Place,
                                std::unordered_map< Place, std::pair<Place, Place> > & syncPlaces);

            //EventTransitionIterator
            //transitionBegin(Event e) const {
            //    return _eventTransitions.find(e)->second.begin();
            //}

            //EventTransitionIterator
            //ransitionEnd(Event e) const {
            //    return _eventTransitions.find(e)->second.end();
            //}

            virtual void
            nameOfTransition2Dot(ostream & os, Transition transition) const {
                os << "                            " << nameOfTransition(transition)
                        << ":"
                        << PetriEventManager::petriEventManager().getEvent(getEvent(transition));
            }

        public:

            virtual Transition newTransition(const set<Place> & pre,
                    const set<Place> & post,
                    const string & name,
                    Event e);


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

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

            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];
            }

            bool
            containsEvent(Event event) const {
                return _eventTransitions.find(event) != _eventTransitions.end();
            }


            TransitionEventIterator
            beginOfTransitionWithEvent(Event event) const {
                require(Exception, containsEvent(event),
                        Msg("beginOfTransitionWithEvent: the event %1% (i.e. %2%) is not associated to a transition of this Petri Net")
                                                % event % PetriEventManager::petriEventManager().getEvent(event));
                return _eventTransitions.at(event).begin();
            }

            TransitionEventIterator
            endOfTransitionWithEvent(Event event) const {
                require(Exception, containsEvent(event),
                                                Msg("endOfTransitionWithEvent: the event %1% (i.e. %2%) is not associated to a transition of this Petri Net")
                                                % event % PetriEventManager::petriEventManager().getEvent(event));
                return _eventTransitions.at(event).end();
            }


            Transition duplicateTransition(Transition t);

            virtual void deleteTransition(Transition t);

            virtual void
            net2TinaTransitionName(ostream & os, Transition trans) const {
                os << " : " << PetriEventManager::petriEventManager().getEvent(getEvent(trans)) << " ";
            }


            virtual void copyLabelledNet(const LabelledNet & 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);

            virtual void appendLabelledNet(const LabelledNet & 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);


            virtual void mergeLabelledNet(const LabelledNet & lpn1, const LabelledNet & lpn2,
                    const unordered_set<Event> & syncEvents,
                    Diades::Graph::ConstNodeMap<Diades::Graph::Node> & nodeMapLpn1,
                    Diades::Graph::NodeMap<Diades::Graph::Node> & nodeMapFromLpn1,
                    Diades::Graph::ConstNodeMap<Diades::Graph::Node> & nodeMapLpn2,
                    Diades::Graph::NodeMap<Diades::Graph::Node> & nodeMapFromLpn2,
                    std::unordered_map< Transition, std::list<Transition> > & lpn1SyncTrans,
                    std::unordered_map< Transition, std::list<Transition> > & lpn2SyncTrans,
                    std::unordered_map< Transition, std::pair<Transition, Transition> > & syncTransitions,
                                        std::unordered_map< Place, Place > & lppn1Place,
                                std::unordered_map< Place, Place > & lppn2Place,
                                std::unordered_map< Place, std::pair<Place, Place> > & syncPlaces);







        };
    };
};

#endif