AutFile.hh

Go to the documentation of this file.

#ifndef __DIADES__AUTOMATA__EXPERIMENTAL__AUTFILE__HH__
#define __DIADES__AUTOMATA__EXPERIMENTAL__AUTFILE__HH__

#include <istream>
#include <string>
#include <unordered_set>
#include <diades/utils/Label.hh>
#include <diades/graph/ConstNodeMap.hh>
#include <diades/automata/experimental/StateMachine.hh>
#include <diades/automata/experimental/Event.hh>
#include <diades/automata/experimental/StatePropertyManager.hh>
#include <diades/automata/experimental/StateCreation.hh>
#include <diades/utils/IdGenerators.hh>
#include <diades/utils/Range.hh>
#include <diades/automata/experimental/Union.hh>

namespace Diades
{
   namespace Automata
   {
      namespace Experimental
      {
         using AutStateId = StatePropertyIdAsSizeT;

         using AutEventId = std::string;


         using AutFsm = StateMachine<AutStateId, AutEventId>;

         template<typename Fsm>
         bool
         autFsmNeedEncoding(const Fsm & fsm)
         {
            std::vector<char> in(fsm.numberOfStates());
            std::fill(in.begin(), in.end(), 'o');
            std::for_each(fsm.stateBegin(), fsm.stateEnd(), [&](typename Fsm::State s)
            {
               auto sInfo = fsm.getStatePropertyId(s);
               if(sInfo < in.size())
               {
                          in[sInfo] = 'i';
               }
            });
            return std::find(in.begin(), in.end(), 'o') != in.end();
         }

         template<typename Fsm>
         void
         autFileStateEncoding(const Fsm & fsm, Diades::Graph::ConstNodeMap<AutStateId> & encoding)
         {
            encoding.init(fsm.behaviour());
            StatePropertyAsUnsigned i = 1;
            bool initialStateEncoded = false;
            std::for_each(fsm.stateBegin(), fsm.stateEnd(),
                          [&](typename Fsm::State s)
                          {
                             if(fsm.isInitial(s) && !initialStateEncoded)
                             {
                                encoding[s] = 0;
                                initialStateEncoded = true;
                             }
                             else
                             {
                                encoding[s] = i;
                                ++i;
                             }
                          });
         }


         template<typename Fsm>
         void
         autFileStateReencoding(Fsm & fsm)
         {
            Diades::Graph::ConstNodeMap<AutStateId> encoding;
            autFileStateEncoding(fsm,encoding);
            
            std::for_each(fsm.stateBegin(), fsm.stateEnd(),
                         [&](typename Fsm::State s)
            {
               auto s1 = fsm.getState(encoding[s]);
               if(s1.isValid())
               {
                  fsm.setStatePropertyId(s1,fsm.nullStatePropertyId);
               }
               fsm.setStatePropertyId(s,encoding[s]);
            });
         }






         bool fromAutFile(std::istream& stream, AutFsm & fsm);



         bool
         toAutFile(ostream& stream, const AutFsm & fsm, bool enforce = false);

         class AutStateCreator : public OnlyStateCreator<AutFsm>
         {
         public:
            using OSC = OnlyStateCreator<AutFsm>;

            using State = typename OSC::State;
            using FsmBs = typename OSC::FsmBs;
         public:

            AutStateCreator(const AutFsm & source, AutFsm & target) :
            OSC(source, target)
            {
            }

            virtual std::pair<State, bool>
            newState(const FsmBs & bs)
            {
               // why using StateCreation<StateMachine>::_target instead of _target? Does not compile
               // see https://gcc.gnu.org/onlinedocs/gcc/Name-lookup.html for explanation

               // here we do not take into account the belief state of source
               return OSC::_target.newState(_target.numberOfStates());
            }
         };

         using AutFsmEventInserter = EventInserter<AutFsm>;

         using AutFsmStateIdGenerator = StateIdGenerator<AutFsm, Diades::Utils::IncrementGenerator<AutFsm::StatePropertyId>>;

         using AutFsmStateInserter = StateInserter<AutFsmStateIdGenerator, StateCopy<AutFsm>>;
         
         
         
         using AutFsmTransitionInserter = TransitionInserter<AutFsmStateInserter,AutFsmEventInserter>;
         
         

         template<typename AutFsmRange>
         bool
         insertAutFsms(AutFsmRange range, AutFsm & output)
         {
            bool result = true;
            Diades::Utils::IncrementGenerator<AutFsm::StatePropertyId> idGen(0);
            AutFsmStateIdGenerator gen(output, idGen, true);
            std::list<AutFsmEventInserter> evtInserters;
            std::list<StateCopy < AutFsm>> stateCopies;
            std::list<AutFsmStateInserter> stateInserters;
            
            
            std::list<AutFsmTransitionInserter> tInserters;
            
            std::for_each(range.begin(), range.end(),
                          [&](const AutFsm & fsm)
                          {
                             evtInserters.emplace_back(fsm, output);
                             stateCopies.emplace_back(fsm, output);
                             stateInserters.emplace_back(gen, stateCopies.back());
                             tInserters.emplace_back(stateInserters.back(),evtInserters.back());
                          });
           
            insertRangeOfTransitions(tInserters.begin(),tInserters.end());

            // now the issue is that the aut format does not allow more than one initial state
            // i do the merge of initial states the hard way !
            if(output.numberOfInitialStates() > 1)
            {
               // which should be always the case anyway..
               auto it = output.initialStateBegin();
               AutFsm::State mergedInitialState = *it;
               std::list<AutFsm::State> statesToRemove;
               ++it;
               while(it != output.initialStateEnd())
               {
                  std::for_each(output.outputTransitionBegin(*it), output.outputTransitionEnd(*it),
                                [&](const AutFsm::Transition & transition)
                                {
                                   if(output.isInitial(transition.target()))
                                   {
                                      output.newTransition(mergedInitialState, mergedInitialState, output.getEvent(transition));
                                   }
                                   else
                                   {
                                      output.newTransition(mergedInitialState, transition.target(), output.getEvent(transition));
                                   }
                                });
                  std::for_each(output.inputTransitionBegin(*it), output.inputTransitionEnd(*it),
                                [&](const AutFsm::Transition & transition)
                                {
                                   if(!output.isInitial(transition.source()))

                                   {
                                      output.newTransition(transition.source(), mergedInitialState, output.getEvent(transition));
                                   }
                                });
                  statesToRemove.push_back(*it);
                  ++it;
               }
               deleteState(output,statesToRemove.begin(),statesToRemove.end());
            }
            // the state encoding is certainly not good 
            autFileStateReencoding(output);
            return result;
         }

      }
   }

}
#endif /* __DIADES__AUTOMATA__EXPERIMENTAL__AUTFILE__HH__ */