Trimming.hh

Go to the documentation of this file.

#ifndef __DIADES__AUTOMATA__EXPERIMENTAL__TRIMMING__HH
#define __DIADES__AUTOMATA__EXPERIMENTAL__TRIMMING__HH

#include<unordered_map>
#include<unordered_set>
#include<list>
#include<stack>
#include<diades/automata/experimental/StateMachine.hh>
#include<diades/automata/experimental/BeliefState.hh>
#include<diades/automata/experimental/ControlPattern.hh>

namespace Diades {
  namespace Automata {
    namespace Experimental {


      template<typename Fsm, typename BeliefStateIterator, typename StateIdInsertIterator>
      void
      trimmingTraces(Fsm & machine,
                     BeliefStateIterator bfBegin,
                     BeliefStateIterator bfEnd,
                     StateIdInsertIterator insertIt)
      {
        using State = typename Fsm::State;
        using Transition = typename Fsm::Transition;
        using StateMap = Diades::Graph::NodeMap<char>;
        list<State> visitingStates;
        StateMap visited(machine.behaviour());
        std::for_each(bfBegin,bfEnd,
                      [&](State s){
                        visited[s]=1;
                        visitingStates.push_back(s);
                      });
        while(!visitingStates.empty())
          {
            std::for_each(machine.inputTransitionBegin(visitingStates.front()),
                          machine.inputTransitionEnd(visitingStates.front()),
                          [&](Transition t){
                            if(visited[t.source()]==0)
                              {
                                visitingStates.push_back(t.source());
                                visited[t.source()]=1;
                              }
                          });
            visitingStates.pop_front();
          }
        deleteState(machine,machine.stateBegin(), machine.stateEnd(),[&](State s){ return visited[s]==0; }, insertIt);
      }



      template<typename Fsm, typename BeliefStateIterator, typename StateIdInsertIterator>
      void
      trimmingUnreachableStates(Fsm & machine,
                                BeliefStateIterator bfBegin,
                                BeliefStateIterator bfEnd,
                                StateIdInsertIterator insertIt)
      {
        using State = typename Fsm::State;
        using Transition = typename Fsm::Transition;
        using StateMap = Diades::Graph::NodeMap<char>;
        list<State> visitingStates;
        StateMap visited(machine.behaviour());
        std::for_each(bfBegin,bfEnd,
                      [&](State s){
                        visited[s]=1;
                        visitingStates.push_back(s);
                      });
        while(!visitingStates.empty())
          {
            std::for_each(machine.outputTransitionBegin(visitingStates.front()),
                          machine.outputTransitionEnd(visitingStates.front()),
                          [&](Transition t){
                            if(visited[t.target()]==0)
                              {
                                visitingStates.push_back(t.target());
                                visited[t.target()]=1;
                              }
                          });
            visitingStates.pop_front();
          }
        deleteState(machine,machine.stateBegin(), machine.stateEnd(),[&](State s){ return visited[s]==0; }, insertIt);
      }


      template<typename Fsm, typename StateIdInsertIterator>
      void
      trimmingUnreachableStates(Fsm & machine,
                                StateIdInsertIterator insertIt)
      {
        trimmingUnreachableStates(machine,machine.initialStateBegin(),machine.initialStateEnd(),insertIt);
      }

      template<typename Fsm, typename BeliefStateIterator, typename StateIdInsertIterator>
      bool
      trimmingDeadlockStates(Fsm & machine,
                             BeliefStateIterator bfBegin,
                             BeliefStateIterator bfEnd,
                             StateIdInsertIterator insertIt)
      {
        using State = typename Fsm::State;
        using Transition = typename Fsm::Transition;
        using StateMap = Diades::Graph::NodeMap<char>;
        std::list<State> visitingStates;
        StateMap visited(machine.behaviour());
        std::for_each(bfBegin, bfEnd, [&](State s) { if(s.outDeg()==0) { visitingStates.push_back(s); } });
        auto toConfirmIt = visitingStates.end();
        while(visitingStates.begin() != toConfirmIt)
          {
            if(visitingStates.front().outDeg() == 0)
              {
                if(visitingStates.front().inDeg() != 0)
                  {
                    std::for_each(machine.inputTransitionBegin(visitingStates.front()),
                                  machine.inputTransitionEnd(visitingStates.front()),
                                  [&](Transition t){ visitingStates.push_back(t.source()); });
                    toConfirmIt = visitingStates.end();
                  }
                *(insertIt++)=machine.getStatePropertyId(visitingStates.front());
                machine.deleteState(visitingStates.front());
              }
            else
              {
                if(toConfirmIt == visitingStates.end())
                  {
                    toConfirmIt = visitingStates.insert(visitingStates.end(),
                                                        visitingStates.front());
                  }
                else
                  {
                    visitingStates.insert(visitingStates.end(),
                                          visitingStates.front());
                  }
              }
            visitingStates.pop_front();
          }
        return machine.initialStateBegin() != machine.initialStateEnd();
      }


      template<typename Fsm, typename StateIdInsertIterator>
      bool
      trimmingDeadlockStates(Fsm & machine,
                             StateIdInsertIterator insertIt)
      {
        return trimmingDeadlockStates(machine,machine.stateBegin(),machine.stateEnd(),insertIt);
      }


      template<typename Fsm,  typename BeliefStateIterator, typename StateIdInsertIterator, typename DisableInsertIterator>
      bool controlledTrimmingDeadlockState(Fsm & machine,
                                           ControlPattern<Fsm> & pattern,
                                           BeliefStateIterator bfBegin,
                                           BeliefStateIterator bfEnd,
                                           StateIdInsertIterator insertIt,
                                           DisableInsertIterator disableIt)
      {
        using Event = typename Fsm::EventPropertyId;
        using State = typename Fsm::State;
        using Transition = typename Fsm::Transition;
        using StateMap = Diades::Graph::NodeMap<char>;
        std::list<State> visitingStates;
        std::unordered_map<State,std::list<Event>> disabled;
        StateMap visited(machine.behaviour(),machine.numberOfStates(),0);
        std::for_each(bfBegin, bfEnd, [&](State s) { if(s.outDeg()==0) { visited[s]=1; visitingStates.push_back(s); } });
        while(!visitingStates.empty())
            {
              std::for_each(machine.inputTransitionBegin(visitingStates.front()),
                            machine.inputTransitionEnd(visitingStates.front()),
                            [&](Transition t){
                                if(pattern.enabled(machine.getEvent(t)))
                                  {
                                    if(visited[t.source()]==0)
                                      {
                                        visitingStates.push_back(t.source());
                                        visited[t.source()]=1;
                                      }
                                  }
                                else
                                  {
                                    disabled[t.source()].push_back(machine.getEvent(t));
                                    // we are about to delete t.target(). If t.source() has only one output transition
                                    // then it will become a deadlock
                                    if((t.source().outDeg() == 1) && (visited[t.source()]==0))
                                                                     {
                                                                       visitingStates.push_back(t.source());
                                                                       visited[t.source()]=1;
                                                                     }
                                  }
                            });
              *(insertIt++)=machine.getStatePropertyId(visitingStates.front());
              disabled.erase(visitingStates.front());
              machine.deleteState(visitingStates.front());
              visitingStates.pop_front();
          }
        for(const auto & disab : disabled)
          {
            for( const auto & event : disab.second)
              {
                *(disableIt++)= std::make_pair(machine.getStatePropertyId(disab.first),event);
              }
          }
        return machine.initialStateBegin() != machine.initialStateEnd();
      }
    }
  }
}

#endif /* __DIADES__AUTOMATA__EXPERIMENTAL__TRIMMING__HH */