Component.hh

Go to the documentation of this file.

#ifndef __DIADES__AUTOMATA__COMPONENT__HH
#define __DIADES__AUTOMATA__COMPONENT__HH

#include <sstream>
#include <string>
#include <set>
#include <unordered_set>
#include <unordered_map>
#include <list>
#include <vector>
#include <diades/utils/Loggable.hh>
#include <boost/archive/text_oarchive.hpp>
#include <boost/archive/text_iarchive.hpp>
#include <boost/serialization/vector.hpp>
#include <boost/serialization/set.hpp>
#include <boost/serialization/map.hpp>
#include <diades/utils/Exceptions.hh>
#include <diades/utils/Assertion.hh>
#include <diades/graph/Graph.hh>
#include <diades/graph/NodeMap.hh>
#include <diades/graph/ConstNodeMap.hh>
#include <diades/graph/EdgeMap.hh>
#include <diades/automata/Event.hh>
#include <diades/automata/BeliefState.hh>


namespace Diades
{
  namespace Automata
  {

      using Diades::Utils::Msg;
    using Diades::Utils::LogLevel;
    using Diades::Utils::Loggable;


        typedef Diades::Graph::Edge Transition;
  
        class Component: public Loggable {

        public:
            static const string defaultComponentName; 
          static string typeName() { return "Automata::Component"; }
          typedef Diades::Utils::Exception<Component> Exception;

          
        public:
          typedef Component * Pointer;
          typedef const Component * ConstPointer;
          typedef Diades::Graph::NodeIterator StateIterator;
          typedef Diades::Graph::EdgeIterator TransitionIterator;
          typedef list<Transition>::const_iterator EventTransitionIterator;
          typedef unordered_set<State>::const_iterator InitialStateIterator;
          typedef Diades::Graph::InEdgeIterator InputTransitionIterator;
          typedef Diades::Graph::OutEdgeIterator OutputTransitionIterator;
          typedef set<Event>::const_iterator EventIterator;
          typedef unordered_set<Transition>::const_iterator OutputEventTransitionIterator;
          typedef unordered_set<Transition>::const_iterator InputEventTransitionIterator;
          typedef unordered_set<State>::const_iterator LabelledStateIterator;
          typedef std::string StateLabel;
        
        protected:
          Diades::Graph::Graph _behav; 
          unordered_set<State> _initial; 
          Diades::Graph::NodeMap<int> _isInitial; 
        private:
          string _name; 
          int _id;     
          set<Event> _events; 
          set<Event> _faultyEvents;
          set<Event> _normalEvents;
          vector<  Diades::Graph::NodeMap< unordered_set<Transition> > > _transitionsWithTarget;
          vector<  Diades::Graph::NodeMap< unordered_set<Transition> > > _transitionsWithSource;
          vector<  unordered_set<State>  > _sourceWithEvent;
          vector<  unordered_set<State>  > _targetWithEvent;
          vector<  list<Transition> > _transitionsWithEvent;
          Diades::Graph::EdgeMap< Event > _eventOfTransition;
          Diades::Graph::NodeMap< StateLabel > _labelOfState; 
          unordered_map< StateLabel,State > _stateOfLabel; 
        public:
//        template<class Archive>
//        void serialize(Archive & ar, const unsigned int version)
//        {
//              ar & _behav;
//              ar & _initial;
//              ar & _isInitial;
//              ar & _name;
//              ar & _id;
//              ar & _events;
//              ar & _faultyEvents;
//              ar & _normalEvents;
//              ar & _transitionsWithTarget;
//              ar & _transitionsWithSource;
//              ar & _sourceWithEvent;
//              ar & _targetWithEvent;
//              ar & _transitionsWithEvent;
//              ar & _eventOfTransition;
//              ar & _labelOfState;
//              ar & _stateOfLabel;
//        }


          
        public:
          ConstPointer getPointer() const { return this; }
          Pointer getPointer() { return this; }
      
          /*********************************************************************/
          /* GENERAL MANAGEMENT */
          /*********************************************************************/
          Component():_behav(),
                      _initial(),
                      _isInitial(),
                      _name(defaultComponentName),
                      _id(),
                      _events(),
                      _faultyEvents(),
                      _normalEvents(),
                      _transitionsWithTarget(),
                      _transitionsWithSource(),
                      _sourceWithEvent(),
                      _targetWithEvent(),
                      _eventOfTransition(),
                      _labelOfState(),
                      _stateOfLabel()
          {
            _eventOfTransition.init(_behav);
            _labelOfState.init(_behav);
            _isInitial.init(_behav,0);
          }
          
          Component(const Component & component);

          virtual ~Component();
          

          bool operator==(const Component & component) const {
                return this == &component;
          }


          bool operator!=(const Component & component) const {
                return !(*this == component);
          }


        
          virtual void clear();
        
        
          int id() const { return _id; }


        
          void setId(int identifier)  { _id = identifier; }

        

          Graph::Graph & behaviour()  { return _behav; }

          const Graph::Graph & behaviour() const { return _behav; }


          bool isEmpty() const
          {
                return (_behav.empty());
          }

          bool isValid() const { return !isEmpty() && name() != defaultComponentName; }

        
          /*********************************************************************/
          /* NAME MANAGEMENT */
          /*********************************************************************/

          void setName(const string & name)
          {
                require(Exception, !name.empty(), "setName: invalid name");
                _name = name;
                ensure(Exception, !_name.empty(), "setName");
          }

          const string & name() const {
                ensure(Exception, !_name.empty(), "name");
                return _name;
          }
          /********************************************************************/
        




        
          /*********************************************************************/
          /* EVENT MANAGEMENT */
          /*********************************************************************/
          void insertEvent(const Event & event);


          unsigned numberOfEvents() const
          {
                return _events.size();
          }
        
          void insertEvent(EventIterator start, EventIterator end);
          
        
          const Event & getEvent(Transition t) const {
                require(Exception,t.valid(),"getEvent: invalid transition");
                require(Exception,&t.owner() == &_behav,"getEvent: the transition does not belong to this component");
                ensure(Exception,_eventOfTransition[t].isValid(),"getEvent returns an invalid event");
                return _eventOfTransition[t];
          }

          const set<Event> & events() const
          {
                return _events;
          }
          

          EventIterator eventBegin() const
          {
                return _events.begin();
          }


          EventIterator eventEnd() const
          {
                return _events.end();
          }
        

          bool containsEvent(const Event & e) const
          {
                require(Exception,e.isValid(),"containsEvent: invalid event");
                return _events.find(e) != _events.end();
          }



          void setFaulty(const Event & e)
          {
            require(Exception,containsEvent(e),"setFaulty: the event does not exist in the component");
            _normalEvents.erase(e);
            _faultyEvents.insert(e);
          }


          bool isFaulty(const Event & e) const
          {
            return _faultyEvents.find(e) != _faultyEvents.end();
          }

          
          const set<Event> & faultyEvents() const
          {
                return _faultyEvents;
          }
          

          EventIterator faultyEventBegin() const
          {
                return _faultyEvents.begin();
          }


          EventIterator faultyEventEnd() const
          {
                return _faultyEvents.end();
          }

          
        
          void setNormal(const Event & e)
          {
            require(Exception,containsEvent(e),"setNormal: the event does not exist in the component");
            _faultyEvents.erase(e);
            _normalEvents.insert(e);
          }

          bool isNormal(const Event & e) const
          {
            return _normalEvents.find(e) != _normalEvents.end();
          }

          const set<Event> & normalEvents() const
          {
                return _normalEvents;
          }
          

          EventIterator normalEventBegin() const
          {
                return _normalEvents.begin();
          }


          EventIterator normalEventEnd() const
          {
                return _normalEvents.end();
          }


          

          void replaceEvent(const Event & e1, const Event & e2);
        

          /********************************************************************/
          






          /*******************************************************************/
          /* STATE MANAGEMENT */
          /*********************************************************************/

        
          State newState();


        

        
        
          State newState(const StateLabel & label);
        
        
          const StateLabel & getLabel(State state) const
          {
                require(Exception,state.valid(),"getLabel: invalid state");
                require(Exception,&state.owner() == &_behav,"getLabel: the state does not belong to this component");
                return _labelOfState[state];
          }
        
        
          State getState(const StateLabel & label) const
          {
                unordered_map< StateLabel, State >::const_iterator it;
                it = _stateOfLabel.find(label); 
                require(Exception,it != _stateOfLabel.end(),"getState: no such a state");
                return it->second;
          }     
        

          void deleteState(State state);

          void deleteState(StateIterator start, StateIterator end);


          unsigned numberOfStates() const {
                return _behav.numberOfNodes();
          }

        
        
          StateIterator stateBegin() const {
                return _behav.nodeBegin();
          }

          StateIterator stateEnd() const {
                return _behav.nodeEnd();
          }


          void setInitial(State state) {
                if(state.valid() && (&state.owner() == &_behav))
                  {
                        _initial.insert(state);
                        _isInitial[state] = 1;
                  }
          }


          void unsetInitial(State state) {
                if(state.valid() && (&state.owner() == &_behav))
                  {
                        _initial.erase(state);
                        _isInitial[state] = 0;
                  }
          }

          void setAllInitialStates()
          {
                _initial.insert(stateBegin(),stateEnd());
                _isInitial.initValue(stateBegin(),stateEnd(),1);
          }

          void clearAllInitialStates()
          {
                _isInitial.initValue(stateBegin(),stateEnd(),0);
                _initial.clear();
          }

        
          InitialStateIterator initialStateBegin() const {
                return _initial.begin();
          }

          InitialStateIterator initialStateEnd() const {
                return _initial.end();
          }


          unsigned numberOfInitialStates() const
          {
                return _initial.size();
          }
          
        
          bool isInitial(State state) const {
                return (state.valid()) && (&state.owner() == &_behav) && (_isInitial[state] == 1);
          }


          virtual void mergeInfoStates(const vector<const Component *> & components, const vector<State> & states, State currentState);
        
        
          /*******************************************************************/
        




          /*******************************************************************/
          /*  TRANSITION MANAGEMENT   */
          /*********************************************************************/

        public:
          Transition newTransition(State source, State target,  Event  event);

        

          Transition newTransition(const StateLabel & source, const StateLabel &  target,  Event  event);



        

          void deleteTransition(Transition t);



          void deleteTransition(TransitionIterator start, TransitionIterator end);
        
          void deleteTransition(EventTransitionIterator start, EventTransitionIterator end);
        
        
          LabelledStateIterator beginOfSourceStateOfEvent(const Event & e) const {
                require(Exception, _events.find(e) != _events.end(),
                                "beginOfSourceStateOfEvent: the event does not belong to the component");
                return _sourceWithEvent[e.id()].begin();
          }


          LabelledStateIterator endOfSourceStateOfEvent(const Event & e) const {
                require(Exception, _events.find(e) !=  _events.end(),
                                "endOfSourceStateOfEvent: the event does not belong to the component");
                return _sourceWithEvent[e.id()].end();
          }
        
        
        
          LabelledStateIterator beginOfTargetStateOfEvent(const Event & e) const {
                require(Exception, _events.find(e) !=  _events.end(),
                                "beginOfTargetStateOfEvent: the event does not belong to the component");
                return _targetWithEvent[e.id()].begin();
          }
        
        
          LabelledStateIterator endOfTargetStateOfEvent(const Event & e) const {
                require(Exception, _events.find(e) !=  _events.end(),
                                "endOfTargetStateOfEvent: the event does not belong to the component");
                return _targetWithEvent[e.id()].end();
          }


          EventTransitionIterator eventTransitionBegin(const Event & e) const {
                require(Exception, _events.find(e) !=  _events.end(),
                                "eventTransitionBegin: the event does not belong to the component");
                return _transitionsWithEvent[e.id()].begin();
          }

          EventTransitionIterator eventTransitionEnd(const Event & e) const {
                require(Exception, _events.find(e) !=  _events.end(),
                                "eventTransitionEnd: the event does not belong to the component");
                return _transitionsWithEvent[e.id()].end();
          }



          OutputEventTransitionIterator outputEventTransitionBegin(State s, Event e) const {
                require(Exception, e.isValid(),  "outputEventTransitionBegin: the event is invalid");
                require(Exception, _events.find(e) !=  _events.end(),
                                Msg("outputEventTransitionBegin: the event '%1%' does not belong to the component") % e);
                require(Exception,s.valid(),"outputEventTransitionBegin: invalid state");
                require(Exception,&s.owner() == &_behav,"outputEventTransitionBegin: the state does not belong to this component");
                return _transitionsWithSource[e.id()][s].begin();
          }
        


          OutputEventTransitionIterator  outputEventTransitionEnd(State s, Event e) const {
                require(Exception, _events.find(e) !=  _events.end(),
                                Msg("outputEventTransitionEnd: the event '%1%' does not belong to the component")% e);
                require(Exception,s.valid(),"outputEventTransitionEnd: invalid state");
                require(Exception,&s.owner() == &_behav,"outputEventTransitionEnd: the state does not belong to this component");
                return _transitionsWithSource[e.id()][s].end();
          }



          InputEventTransitionIterator inputEventTransitionBegin(State s, Event e) const {
                require(Exception, _events.find(e) !=  _events.end(),
                                Msg("inputEventTransitionBegin: the event '%1%' does not belong to the component") % e);
                require(Exception,s.valid(),"inputEventTransitionBegin: invalid state");
                require(Exception,&s.owner() == &_behav,"inputEventTransitionBegin: the state does not belong to this component");
                return _transitionsWithTarget[e.id()][s].begin();
          }
        


          InputEventTransitionIterator  inputEventTransitionEnd(State s, Event e) const {
                require(Exception, _events.find(e) !=  _events.end(),
                                Msg("inputEventTransitionEnd: the event '%1%' does not belong to the component")% e);
                require(Exception,s.valid(),"inputEventTransitionEnd: invalid state");
                require(Exception,&s.owner() == &_behav,"inputEventTransitionEnd: the state does not belong to this component");
                return _transitionsWithTarget[e.id()][s].end();
          }
   


          TransitionIterator transitionBegin() const {
                return _behav.edgeBegin();
          }
        
          TransitionIterator transitionEnd() const {
                return _behav.edgeEnd();
          }
        
          OutputTransitionIterator outputTransitionBegin(State s) const
          {
                require(Exception, s.valid(), "outputTransitionBegin: the state is not valid");
                require(Exception, &s.owner() == &_behav, "outputTransitionBegin: the state does not belong to the component");
                return s.outEdgeBegin();
          }

          OutputTransitionIterator outputTransitionEnd(State s) const {
                require(Exception, s.valid(), "outputTransitionEnd: the state is not valid");
                require(Exception, &s.owner() == &_behav, "outputTransitionEnd: the state does not belong to the component");
                return s.outEdgeEnd();
          }

          InputTransitionIterator inputTransitionBegin(State s) const {
                require(Exception, s.valid(), "inputTransitionBegin: the state is not valid");
                require(Exception, &s.owner() == &_behav, "inputTransitionBegin: the state does not belong to the component");
                return s.inEdgeBegin();
          }


          InputTransitionIterator inputTransitionEnd(State s) const {
                require(Exception, s.valid(), "inputTransitionEnd: the state is not valid");
                require(Exception, &s.owner() == &_behav, "inputTransitionEnd: the state does not belong to the component");
                return s.inEdgeEnd();
          }

          unsigned numberOfTransitions() const {
                return _behav.numberOfEdges();
          }


          /*********************************************************************/
          /* ALGORITHMS FOR DEBUGGING                                          */
          /*********************************************************************/

          bool sanityCheck(string & log) const;

        

          /*********************************************************************/
          /*  ALGORITHMS FOR DETERMINISM  */
          /*********************************************************************/

        protected:

          virtual void determine(const Component * comp, const unordered_set<State> & acceptors,
                                                         unordered_set<State> & newAcceptors);
        
          virtual void determine(const Component * comp);


        
        public:
        
          bool isDeterministic() const;







          /*********************************************************************/
          /*  ALGORITHMS FOR PROJECTION  */
          /*********************************************************************/
        public:
        
          virtual bool project(const Component * comp,
                               const set<Event> & projectedEvents);
          
          virtual bool project(const Component * comp,
                               const set<Event> & projectedEvents,
                               unordered_map<Diades::Automata::State,unordered_set<Diades::Automata::State> > & dictionary);
          
          virtual bool project(const Component * comp,
                                                   const set<Event> & projectedEvents,
                                                   const unordered_set<State> & acceptors,
                                                   unordered_set<State> & newAcceptors);


        private:

                
          void reachableStates(const BeliefState & bs, Event event,
                                                   const set<Event> & projectedEvents,
                                                   BeliefState & nextBs) const;

          void reachableStates(const BeliefState & bs, Event event,
                                                   const set<Event> & projectedEvents,
                                                   BeliefState & nextBs, const unordered_set<State> & acceptors, bool & presenceOfAcceptors) const;


          /*********************************************************************/
          /*  ALGORITHMS FOR MINIMISATION  */
          /*********************************************************************/

        public:

          bool minimize();

          bool minimize(unordered_set<State> & acceptors);


          bool isComplete() const;

        
        private:


          State mergeStates(BeliefState & states);

        
        
          void nerodePartition(vector < BeliefState * > & partition) const;

        
          void nerodePartition(const unordered_set<State> & acceptors,
                                                   vector< BeliefState * > & partition);


          void splitPartition(const BeliefState * bigQ0,
                                                  const BeliefState * bigQ1,
                                                  Event littleA,
                                                  BeliefState * bigQ0prime,
                                                  BeliefState * bigQ0MinusbigQ0prime) const;
        
          void splitPartition2(const BeliefState * bigQ0,
                                                   const BeliefState * bigQ1,
                                                   Event littleA,
                                                   BeliefState * bigQ0prime,
                                                   BeliefState * bigQ0MinusbigQ0prime, State sinkState) const;
        
        

          /*********************************************************************/
          /* IMPORT/EXPORT MANAGEMENT  */
          /*********************************************************************/
        
        public:
          virtual bool import(const string & filename);
        

          virtual bool component2dot(const string & fileName) const;
        

          virtual bool exportDesCompModel(const string & filename) const;
        
        public: 
                
                
          virtual bool importDesCompModel(const string & filename);

          virtual bool importDesCompModel(istream & stream);




        protected:

          virtual bool parseDesCompName(istream & stream);


          virtual bool parseDesCompStates(istream & stream);

          virtual bool parseDesCompFaultyEvents(istream & stream);

          virtual bool parseDesCompNormalEvents(istream & stream);

          virtual bool parseDesCompObservableEvents(istream & stream);


          virtual bool parseDesCompMaskedEvents(istream & stream,
                                                unsigned number,
                                                map< string, set<string> > & maskEvents);

          virtual bool parseDesCompTransitions(istream & stream);
          
        };


        template<typename InputIterator>
        inline void deleteTransition(Component & comp, InputIterator first, InputIterator last)
        {
          for(; first!= last; ++first)
                {
                  comp.deleteTransition(*first);
                }
        }

        template<typename InputIterator>
        inline void deleteState(Component & comp, InputIterator first, InputIterator last)
        {
          for(; first!= last; ++first)
                {
                  comp.deleteState(*first);
                }
        }


        template<typename InputIterator,typename Predicate>
        inline void deleteState(Component & comp, InputIterator first, InputIterator last, Predicate pred)
        {
          for(; first!= last; ++first)
                {
                  if(pred(*first))
                        {
                          comp.deleteState(*first);
                        }
                }
        }

        
        struct GetEvent: public unary_function<Transition,Event>
        {
          const Component & _comp;
          GetEvent(const Component & component):_comp(component){}
          const Event & operator()(Transition t) const
          {
                return _comp.getEvent(t);
          }
        };

        
        struct NonPredecessorFunctor
        {
          typedef enum{NonPredecessor,Predecessor} Status;
          NodeMap<Status> * _map;
          NonPredecessorFunctor(NodeMap<Status> * mapPredecessor):_map(mapPredecessor){}
          bool operator()(State s) const
          {
                return (*_map)[s]==NonPredecessor;
          }
        };
  
  
        template<typename InputIterator>
        inline void purgeNonPredecessors(Component & comp, InputIterator first, InputIterator last)
        {
          typedef NonPredecessorFunctor::Status Status;
          NodeMap<Status> status(comp.behaviour(),comp.numberOfStates(), Status::NonPredecessor);
          list<State> states;
          states.insert(states.end(),first,last);
          for(; first!= last; ++first)
                {
                  status[*first]= Status::Predecessor;
                }
          while(!states.empty())
                {
                  State current = states.front();
                  states.pop_front();
                  for(Component::InputTransitionIterator it = comp.inputTransitionBegin(current);
                          it != comp.inputTransitionEnd(current);
                          ++it)
                        {
                          if(status[it->source()] == Status::NonPredecessor)
                                {
                                  status[it->source()] =  Status::Predecessor;
                                  states.push_back(it->source());
                                }
                        }       
                }
          deleteState(comp,comp.stateBegin(),comp.stateEnd(),NonPredecessorFunctor(&status));
        }
  
  };
};



#endif