TwinRealTimeSystemPattern.hh

Go to the documentation of this file.

#ifndef __DIADES__PETRI__TWINREALTIMESYSTEMPATTERN__HH__
#define __DIADES__PETRI__TWINREALTIMESYSTEMPATTERN__HH__
#include<diades/petri/Pattern.hh>
#include<diades/petri/RealTimeSystem.hh>
#include<diades/petri/RealTimeSystemPattern.hh>

namespace Diades
{
        namespace Petri
        {

                class TwinRealTimeSystemPattern : public RealTimeSystem
                {
                private:

                        vector<Marking> _leftFinalMarkings;
                        vector<Place> _leftNonAdmissibleSystemPlaces;
                        vector<Marking> _rightFinalMarkings;
                        vector<Place> _rightNonAdmissibleSystemPlaces;
                        std::string _seltFormula;

                public:

                        TwinRealTimeSystemPattern(const RealTimeSystemPattern & syspat);

                        
                        const vector<Marking> &
                        leftFinalMarkings() const
                        {
                                return _leftFinalMarkings;
                        }
                        
                        const vector<Place> &
                        leftNonAdmissibleSystemPlaces() const
                        {
                                return _leftNonAdmissibleSystemPlaces;
                        }
                        
                        const vector<Marking> &
                        rightFinalMarkings() const
                        {
                                return _rightFinalMarkings;
                        }

                        
                        const vector<Place> &
                        rightNonAdmissibleSystemPlaces() const
                        {
                                return _rightNonAdmissibleSystemPlaces;
                        }
                        
                        
                        const std::string & seltFormula() const
                        {
                                return _seltFormula;
                        }


                private:
                        void duplicatePlaces(const RealTimeSystemPattern & syspat,
                                                                unordered_map<Place, Place> & leftPlaceOf,
                                                                unordered_map<Place, Place> & rightPlaceOf);


                        void
                        duplicateTransitions(const RealTimeSystemPattern & syspat,
                                                                const unordered_map<Place, Place> & leftPlaceOf,
                                                                const unordered_map<Place, Place> & rightPlaceOf,
                                                                unordered_map<Transition, Transition> & leftTransitionOf,
                                                                unordered_map<Transition, Transition> & rightTransitionOf,
                                                                unordered_map<Event, unordered_set<Transition>> &leftObservableTransitions,
                                                                unordered_map<Event, unordered_set<Transition>> &rightObservableTransitions);


                        void mergeTransitions(unordered_map<Event, unordered_set<Transition>> &leftObservableTransitions,
                                                                unordered_map<Event, unordered_set<Transition>> &rightObservableTransitions);


                        Transition mergeTransition(Transition trLeft, Transition trRight);
                        
                        
                        void computeSeltFormula();

                };

        }
}



#endif /* __DIADES__PETRI__TWINREALTIMESYSTEMPATTERN__HH__ */