GeneratePta.cc

Go to the documentation of this file.

#include<string>
#include<cmath>
#include<algorithm>
#include<fstream>
#include<sstream>
#include<diades/automata/ObservableComponent.hh>
#include<diades/automata/Event.hh>

using std::string;
using std::ifstream;
using Diades::Automata::Component;
using Diades::Automata::ObservableComponent;
using Diades::Automata::ObservableMask;
using Diades::Automata::EventFactory;
using Diades::Automata::Event;
using Diades::Automata::State;
using Diades::Automata::Transition;

string replaceSpace(const string & label)
{
  string result = label;
  std::replace( result.begin(), result.end(), ' ', '_');
  return result;
}

void exportToDesComp(const Component & ptaMoore, const string & fileName)
{
  ofstream file(fileName.c_str());
  file << ptaMoore.name() << endl;
  file << ptaMoore.numberOfStates() << endl;
  file << replaceSpace(ptaMoore.getLabel(*ptaMoore.initialStateBegin())) << " ";
  for(Component::StateIterator stateIt = ptaMoore.stateBegin();
      stateIt != ptaMoore.stateEnd();
      ++stateIt)
    {
      if(*stateIt != *(ptaMoore.initialStateBegin()))
        {
          file << replaceSpace(ptaMoore.getLabel(*stateIt)) << " ";
        }
    }
  file << endl << 0 << endl;


        
  set<string> events;
  vector<string> transitions;
  
  for(Component::TransitionIterator transIt= ptaMoore.transitionBegin();
      transIt!= ptaMoore.transitionEnd();
      ++transIt)
    {
      string transitionBase;
      string transition;
      transitionBase = replaceSpace(ptaMoore.getLabel(transIt->source())) + " -> " + replaceSpace(ptaMoore.getLabel(transIt->target()));
      transition = transitionBase + " " + ptaMoore.getEvent(*transIt).nickname();
      transitions.push_back(transition);
      events.insert(ptaMoore.getEvent(*transIt).nickname());
    }
  // writing the events
  file << events.size() << endl;
  for(set<string>::const_iterator it = events.begin(); it != events.end(); ++it)
    {
      file << *it << " ";
    }
  file << endl << 0 << endl;
  
  file << 0 << endl;
  
  // writing the transitions
  file << endl << transitions.size() << endl;
  for(vector<string>::size_type i = 0; i < transitions.size(); ++i)
    {
      file << transitions[i] << endl;
    }
  
  // writing the end of file
  
  file.close();
}

string stringOf(unsigned & counter)
{
  stringstream stream;
  stream << counter;
  ++counter;
  return stream.str();
}


void MooreEncoding(const string & filename)
{
  Diades::Automata::EventFactory::init(10000);
  unsigned counter = 0;
  Component ptaMoore;
  ptaMoore.setName("ptaMoore");
  State initialMoore = ptaMoore.newState(stringOf(counter));
  ptaMoore.setInitial(initialMoore);
  // first, get the normal logs
  ifstream log(filename);
  std::string line;
  while (std::getline(log, line))
    {
      std::istringstream iss(line);
      string type;
      iss >> type;
      if(type=="N")
        {
          string event;
          State currentMoore = *ptaMoore.initialStateBegin();
          while(iss >> event)
            {
              const Event & evt = EventFactory::factory()->getEvent(event);
              ptaMoore.insertEvent(evt);
              Diades::Automata::Component::OutputEventTransitionIterator itMoore =
                ptaMoore.outputEventTransitionBegin(currentMoore,evt);
              if(itMoore != ptaMoore.outputEventTransitionEnd(currentMoore,evt))
                {
                  currentMoore = itMoore->target();
                }
              else
                {
                  State targetMoore = ptaMoore.newState(stringOf(counter));
                  ptaMoore.newTransition(currentMoore,targetMoore,evt);
                  currentMoore = targetMoore;
                }
            }
          // this is the last event, need to change the class of the last state for ptaMoore
          Transition previousMoore = *currentMoore.inEdgeBegin();
          currentMoore = previousMoore.source();
          State newTargetNormalState  = ptaMoore.newState(ptaMoore.getLabel(previousMoore.target())+ " N");
          ptaMoore.newTransition(currentMoore, newTargetNormalState, ptaMoore.getEvent(previousMoore));

          for(Component::OutputTransitionIterator oit = ptaMoore.outputTransitionBegin(previousMoore.target());
              oit != ptaMoore.outputTransitionEnd(previousMoore.target());
              ++oit)
            {
              ptaMoore.newTransition(newTargetNormalState, oit->target(), ptaMoore.getEvent(*oit));
            }
          ptaMoore.deleteState(previousMoore.target());
        }
    }
  log.close();

  ifstream log2(filename);
  while (std::getline(log2, line))
    {
      std::istringstream iss(line);
      string type;
      iss >> type;
      if(type!="N")
        {
          string event;
          State currentMoore = *ptaMoore.initialStateBegin();
          bool stateCreationMoore = false;
          while(iss >> event)
            {
              
              const Event & evt = EventFactory::factory()->getEvent(event);
              ptaMoore.insertEvent(evt);              
              Diades::Automata::Component::OutputEventTransitionIterator itMoore =
                ptaMoore.outputEventTransitionBegin(currentMoore,evt);
              if(itMoore != ptaMoore.outputEventTransitionEnd(currentMoore,evt))
                {
                  currentMoore = itMoore->target();
                }
              else
                {
                  State targetMoore = ptaMoore.newState(stringOf(counter));
                  ptaMoore.newTransition(currentMoore,targetMoore,evt);
                  currentMoore=targetMoore;
                  stateCreationMoore = true;
                }
            }

          // now we update the ptaMoore with the fault class
          Transition previousMoore = *currentMoore.inEdgeBegin();

          
          if(stateCreationMoore)
            {
              // the class of this log is unique, the current
              // state is at the end of one path
              string counter = ptaMoore.getLabel(currentMoore);
              string faultClass = counter + " " + type;
              State targetFaultMoore = ptaMoore.newState(faultClass);
              ptaMoore.newTransition(previousMoore.source(),targetFaultMoore,
                                     ptaMoore.getEvent(previousMoore));
              ptaMoore.deleteState(previousMoore.target());
            }
          else
            {
              // the log reaches a state that was already built
              // need to insert the new class
              string label = ptaMoore.getLabel(currentMoore);
              std::set<string> labels;
              istringstream iss2(label);
              string faultClass;
              while(iss2 >> faultClass)
                {
                  labels.insert(faultClass);
                }
              labels.insert(type);
              faultClass = "";
              for(const string & lbl : labels)
                {
                  faultClass += lbl + " ";
                }
              State targetFaultMoore = ptaMoore.newState(faultClass);
              ptaMoore.newTransition(previousMoore.source(),targetFaultMoore,
                                     ptaMoore.getEvent(previousMoore));

              for(Component::OutputTransitionIterator oit = ptaMoore.outputTransitionBegin(previousMoore.target());
                  oit != ptaMoore.outputTransitionEnd(previousMoore.target());
                  ++oit)
                {
                  ptaMoore.newTransition(targetFaultMoore, oit->target(), ptaMoore.getEvent(*oit));
                }
              ptaMoore.deleteState(previousMoore.target());
            }
        }
    }
  log2.close();
  ptaMoore.component2dot("ptaMoore.dot");
  exportToDesComp(ptaMoore,"ptaMoore.des_comp");
}


void MealyEncodingV1(const string & filename)
{
  Diades::Automata::EventFactory::init(10000);
  Component pta;
  pta.setName("pta");
  State initial = pta.newState();
  pta.setInitial(initial);

  // first, get the normal logs
  ifstream log(filename);
  std::string line;
  while (std::getline(log, line))
    {
      std::istringstream iss(line);
      string type;
      iss >> type;
      if(type=="N")
        {
          string event;
          State current = *pta.initialStateBegin();
          while(iss >> event)
            {
              const Event & evt = EventFactory::factory()->getEvent(event);
              pta.insertEvent(evt);
              Diades::Automata::Component::OutputEventTransitionIterator it =
                pta.outputEventTransitionBegin(current,evt);
              if(it != pta.outputEventTransitionEnd(current,evt))
                {
                  current = it->target();
                }
              else
                {
                  State target = pta.newState();
                  pta.newTransition(current,target,evt);
                  current = target;
                }
            }
        }
    }
  log.close();

  ifstream log2(filename);
  while (std::getline(log2, line))
    {
      std::istringstream iss(line);
      string type;
      iss >> type;
      if(type!="N")
        {
          const Event & fault = EventFactory::factory()->getEvent(type);
          pta.insertEvent(fault);
          string event;
          State current = *pta.initialStateBegin();
          bool stateCreation = false;
          while(iss >> event)
            {
              
              const Event & evt = EventFactory::factory()->getEvent(event);
              pta.insertEvent(evt);
              
              Diades::Automata::Component::OutputEventTransitionIterator it =
                pta.outputEventTransitionBegin(current,evt);
              if(it != pta.outputEventTransitionEnd(current,evt))
                {
                  current = it->target();
                }
              else
                {
                  State target = pta.newState();
                  pta.newTransition(current,target,evt);
                  current=target;
                  stateCreation = true;
                }
            }

          // now we add the fault transition in the mealy pta
          Transition previous = *current.inEdgeBegin();
          current = previous.source();
          State targetFault = pta.newState();
          pta.newTransition(current,targetFault,fault);
          current = targetFault;
          State target = pta.newState();
          pta.newTransition(current, target, pta.getEvent(previous));

          if(stateCreation)
            {
              // the log was definitely not a normal one
              // so the transition with the last observable event that
              // was created within the loop must be destroyed
              pta.deleteState(previous.target());
            }
        }
    }
  log2.close();
  pta.component2dot("pta.dot");
  pta.exportDesCompModel("pta.des_comp");
}


string encodeTargetState(unsigned id, const vector<string> & varNames)
{
  string result;
  string op= ":=";
  string fals = "false";
  string tru = "true";
  
  for(unsigned i = 0; i < varNames.size(); ++i)
    {
      string assign = varNames[i] + op + ((id % 2 == 0) ?  fals : tru);
      result += (i < varNames.size() -1) ? assign + "," : assign;
      id = id/2;
    }
  return result;
}

string encodeSourceState(unsigned id, const vector<string> & varNames)
{
  string result= "(" ;
  string notS = " not ";
  string andS = " and ";
  string equal= "=";
  for(unsigned i = 0; i < varNames.size(); ++i)
    {
      string assign = (id % 2 == 0) ? notS + varNames[i] : varNames[i];
      result += (i < varNames.size() -1) ? assign + andS : assign;
      id = id/2;
    }
  result+= ")";
  return result;
}




void component2Orange(const ObservableComponent & pta, ostream & os)
{
  os << "componenttype PTA {" << std::endl;
  int encodingSize = (int) ceil(log(std::max((unsigned int)2,pta.numberOfStates())) / log(2));
  vector<string> varNames(encodingSize);
  os << std::endl;
  for(unsigned i = 0; i < varNames.size(); ++i)
    {
      stringstream stream;
      stream << "v" << i;
      varNames[i] = stream.str();
      os << " var " << varNames[i] << ":  bool;" << std::endl;
    }
  os << std::endl;
  for(auto & event : pta.events())
    {
      if(pta.mask().isUnobservable(event))
      {
          os << " event " << event << ";" << std::endl;
      }
    }
  os << std::endl;
  for(auto it = pta.observableBegin();
      it != pta.observableEnd();
      ++it)
    {
      if(*it!=pta.mask().noEvent())
        {
          os << " observable event " << *it << ";" << std::endl;
        }
    }
  os << std::endl;
   for(auto it = pta.observableBegin();
      it != pta.observableEnd();
      ++it)
    {
      if(*it!=pta.mask().noEvent())
        {
          unsigned counter = 0;
          stringstream stream;
          stream << " transition T" << *it;
          os << stream.str() << std::endl;
          for(auto trIt = pta.eventTransitionBegin(*it);
              trIt != pta.eventTransitionEnd(*it);
              ++trIt)
            {
              stringstream stream2;
              stream2 << stream.str() << "_" << ++counter; 
              os << stream2.str() << " "
                 << encodeSourceState(trIt->source().id(),varNames)
                 << " -> "
                 << encodeTargetState(trIt->target().id(),varNames)
                 << ";" << std::endl;
            }
          os << " triggeredby " << *it << ";" << std::endl << std::endl;
        }
    }

   for(auto & event : pta.events())
    {
      if(event!=pta.mask().noEvent())
        {
          unsigned counter = 0;
          stringstream stream;
          stream << " transition T" << event;
          os << stream.str() << std::endl;
          for(auto trIt = pta.eventTransitionBegin(event);
              trIt != pta.eventTransitionEnd(event);
              ++trIt)
            {
              stringstream stream2;
              stream2 << stream.str() << "_" << ++counter; 
              os << stream2.str() << " "
                 << encodeSourceState(trIt->source().id(),varNames)
                 << " -> "
                 << encodeTargetState(trIt->target().id(),varNames)
                 << ";" << std::endl;
            }
          os << " triggeredby " << event << ";" << std::endl << std::endl;
        }
    }
   os << "}" << std::endl << std::endl;
   os << "component pta0 = PTA;" << std::endl;
}






void MealyEncoding(const string & filename,const string & targetName)
{
  Diades::Automata::EventFactory::init(10000);
  ObservableComponent pta;
  ObservableMask mask;
  pta.setName("pta");
  State initial = pta.newState();
  pta.setInitial(initial);

  // first, get the normal logs
  ifstream log(filename);
  std::string line;
  while (std::getline(log, line))
    {
      std::istringstream iss(line);
      string type;
      iss >> type;

      string event;
      State current = *pta.initialStateBegin();
      while(iss >> event)
        {
          const Event & evt = EventFactory::factory()->getEvent(event);
          pta.insertEvent(evt);
          mask.addMask(evt,evt);
          Diades::Automata::Component::OutputEventTransitionIterator it =
            pta.outputEventTransitionBegin(current,evt);
          if(it != pta.outputEventTransitionEnd(current,evt))
            {
              current = it->target();
            }
          else
            {
              State target = pta.newState();
              pta.newTransition(current,target,evt);
              current = target;
            }
        }

      if(type!="N")
        {
          const Event & faultEvt =  EventFactory::factory()->getEvent(type);
          pta.insertEvent(faultEvt);
          mask.makeUnobservable(faultEvt);
          Diades::Automata::Component::OutputEventTransitionIterator it =
            pta.outputEventTransitionBegin(current,faultEvt);
          if(it == pta.outputEventTransitionEnd(current,faultEvt))
            {
              State target = pta.newState();
              pta.newTransition(current,target,faultEvt);
              current = target;
            }
          else
            {
              current = it->target();
            }
        }
      const Event & endEvt =  EventFactory::factory()->getEvent("$");
      pta.insertEvent(endEvt);
      mask.makeUnobservable(endEvt);
      Diades::Automata::Component::OutputEventTransitionIterator it =
        pta.outputEventTransitionBegin(current,endEvt);
      if(it == pta.outputEventTransitionEnd(current,endEvt))
        {
          State target = pta.newState();
          pta.newTransition(current,target,endEvt);
          current = target;
        }
    }
  log.close();
  pta.setMask(mask);
  pta.component2dot(targetName + ".dot");
  pta.exportDesCompModel(targetName + ".des_comp");
  ofstream file(targetName + ".orange");
  component2Orange(pta,file);
  file.close();
}




int main(int argc, char ** argv)
{
  string fileName = argv[1];
  string targetName = argv[2];
  MealyEncoding(fileName,targetName);  
}