CheckReachability.cc

Go to the documentation of this file.

#include<iostream>
#include<vector>
#include<string>
#include<set>
#include<list>
#include<fstream>
#include "boost/date_time/posix_time/posix_time.hpp"
#include<utils/Random.hh>
#include<utils/Verbose.hh>
#include<utils/CmdInterface.hh>

#include<automata/ComposableModel.hh>
#include<automata/ObservableComponent.hh>

using namespace std;
using namespace boost::posix_time;

typedef enum { EVENT = 0, HELP = 1 } Option;
typedef enum { DESCOMP=0, RULES=1} FileExtension;
unsigned numberOfOptions = 2;
unsigned numberOfFileExtensions = 2;


vector<string> fileExtensions(numberOfFileExtensions);
vector<string> options(numberOfOptions);
vector<bool> isSet(numberOfOptions,false);
string description="Usage: dd-check-reachability  --help | model1.des_comp [model2.des_comp ... sync.rules]  [--event e1 e2 ]";

void initialiseOptions()
{
  options[EVENT]         = "--event";
  options[HELP]          = "--help";
  fileExtensions[DESCOMP]= "des_comp";
  fileExtensions[RULES]  = "rules";
}



using namespace Diades::Utils;



void clean(vector<Diades::Automata::ObservableComponent *> & components,
           Diades::Automata::ComposableModel * model,
           vector<Diades::Automata::ComposableModel::ConstPointer> & comps)
{
  if(model != nullptr)
    {
      delete model;
    }
  for(vector<Diades::Automata::ComposableModel::ConstPointer>::size_type i = 0; i < comps.size(); ++i)
    {
      delete comps[i];
      comps[i]=nullptr;
    }
  comps.clear();
  for(vector<Diades::Automata::ObservableComponent *>::size_type i = 0; i < components.size();
      ++i)
    {
      if(components[i]!= nullptr)
        {
          delete components[i];
          components[i]=nullptr;
        }
    }
  components.clear();
  Diades::Automata::EventFactory::destroy();
  Diades::Utils::LoggerFactory::destroy();
}
           
           



int main(int argc, char ** argv)
{
  verbose<VbOutput>("DiaDes: check-reachability\n");
  verbose<VbOutput>("LAAS-CNRS, 2006-2015, 7 avenue du Colonel Roche, Toulouse, France\n");
  verbose<VbOutput>("Contact: yannick.pencole@laas.fr\n");
  initialiseOptions();
  vector<unsigned> values(numberOfOptions);
  set<string>  events;
  set<string> modelFile;
  string ruleFile;
 
  
  if(argc==1)
        {
          printUsage(description);
          return 0;
        }
  int index = 1;
  while(index < argc)
        {
          Option currentOption;
          if(getOption<Option>(argv[index],options,currentOption))
                {
                  if(isSet[currentOption])
                        {
                          printError("The option '" + options[currentOption] + "' occurs at least twice.");
                          return 1;
                        }
                  else
                        {
                          isSet[currentOption] = true;
                        }
                  
                  switch(currentOption)
                        {
                        case HELP:
                          {
                                if((index!=1) || (argc !=2))
                                  {
                                        printError("Incorrect use of option --help.");
                                        return 1;
                                  }
                                else
                                  {
                                        printUsage(description);
                                        return 0;
                                  }
                          }
                        case EVENT:
                          {
                                ++index;
                                getParameterList<string>(argc,argv,options,fileExtensions,
                                                                                 index,events);
                                if(events.size() == 0)
                                  {
                                        printError("One or more  arguments wre expected after option --event.");
                                        return 1;
                                  }
                                break;
                          }
                                
                        default:
                          {
                                printError("Unrecognized option: " + string(argv[index]));
                                return 1;
                                break;
                          }

                        }
                }
          else
                {
                  // then it should be the name of a file
                  vector<string>::const_iterator it =
                        getFileExtension(string(argv[index]),fileExtensions.begin(),fileExtensions.end());

                  if(it == fileExtensions.end())
                        {
                          printError("Unrecognized file extension in file name: " + string(argv[index]));
                          return 1;
                        }

                  
                  FileExtension extension = DESCOMP;
                  if(*it==fileExtensions[RULES]) { extension = RULES; }
                  switch(extension)
                        {
                        case DESCOMP:
                          {
                                modelFile.insert(string(argv[index]));
                                break;
                          }
                        case RULES:
                          {
                                if(!ruleFile.empty())
                                  {
                                        printError("It seems that there are more than one synchronization rules file as a argument.");
                                        return 1;
                                  }
                                ruleFile = string(argv[index]); 
                                break;
                          }
                        }
                  ++index;
                }
        }
  if(modelFile.empty())
        {
          printError("No model, so no check.");return 1;
        }
  if((modelFile.size() == 1) && (!ruleFile.empty()))
        {
          printError("There is one synchronization rule file but no more than one component.");return 1;
        }
  if((modelFile.size() > 1) && (ruleFile.empty()))
        {
          printError("There is no synchronization rule file but it is required as there is more than one component in the model.");return 1;
        }
  
  vector<Diades::Automata::ObservableComponent *> components(modelFile.size(),nullptr);
  Diades::Automata::ComposableModel * model = nullptr;
  vector<Diades::Automata::ComposableModel::ConstPointer> comps;
  Diades::Automata::ParametrizedSynchronisation rules;
  Diades::Automata::ParametrizedSynchronisation::ComponentVector vectorComp;
  try
        {
          unsigned i = 0;
          for(const string & name: modelFile)
                {
                  components[i] = new Diades::Automata::ObservableComponent();
                  if(!components[i]->importOldModel(name))
                        {
                          throw(FunctionException("main", Diades::Utils::Msg("Cannot load the model file '%1%'") % name));
                        }
                  vectorComp.push_back(components[i]);
                  ++i;
                }
          if(!ruleFile.empty())
                {
                  rules.loadRules(vectorComp,ruleFile);
                }
        }
  catch(exception & e)
        {
          log<LgProcess>("The main function caught the following exception: \n\t%1%") % e.what();
          saveLog(cerr);
          clean(components,model,comps);
          printError("Load of the files has failed. See log above.");
          return 1;
        }  
  stringstream toDot;
  Diades::Automata::ObservableMask mask;
  if(components.size()==1)
        {
          unsigned visitedTransitions = 0;
          unsigned visitedStates = 0;
          unsigned deadlocks = 0;
          
          mask = components[0]->mask();
          // check
          unordered_map<Diades::Automata::Event,bool> searchedEvent;
          for(const Diades::Automata::Event & event : components[0]->events())
            {
              if(events.find(event.label()) != events.end())
                {
                  searchedEvent.insert(make_pair(event,false));
                }
            }
          unsigned found = 0;
          std::list< std::pair<Diades::Automata::State,
                               Diades::Automata::ObservableComponent::OutputTransitionIterator> > queue;
          Diades::Graph::NodeMap<bool> visited;
          visited.init(components[0]->behaviour(),false);
          for(Diades::Automata::ObservableComponent::InitialStateIterator it =
                components[0]->initialStateBegin();
              it != components[0]->initialStateEnd();
              ++it)
            {
              queue.push_back(make_pair(*it, components[0]->outputTransitionBegin(*it)));
              visited[*it] = true;
              toDot << "\t " << *it << "\t [label=\"";
              toDot << components[0]->getLabel(*it);
              toDot << "\"];" << endl;
              toDot << "\t init" << *it <<  "\t [label=\"\",color=white];" << endl;
              toDot << "\t init" << *it << " -> " << *it << ";" << endl;

              ++visitedStates;
              if(it->outDeg() == 0)
                {
                  ++deadlocks;
                }
            }
          while((found < searchedEvent.size()) && !(queue.empty()))
            {
              Diades::Automata::State currentState = queue.front().first;
              if(queue.front().second == components[0]->outputTransitionEnd(currentState))
                {
                  queue.pop_front();
                  std::cout << currentState << ": SATURATED" << std::endl;
                }
              else
                {
                  Diades::Automata::Transition currentTrans =  *queue.front().second;
                  ++visitedTransitions;
                  toDot << "\t" << currentState << " -> " << currentTrans.target()
                        <<  " [label=\"" << components[0]->getEvent(currentTrans).nickname();
                  toDot << "\"];" << endl;
                  unordered_map<Diades::Automata::Event,bool>::iterator it =
                    searchedEvent.find(components[0]->getEvent(currentTrans));
                  if(it != searchedEvent.end())
                    {
                      if(it->second == false)
                        {
                          it -> second = true;
                          ++found;
                          std::cout << "FOUND" << std::endl;
                        }
                    }
                  if(!visited[currentTrans.target()])
                    {
                      queue.push_back(make_pair(currentTrans.target(), components[0]->outputTransitionBegin(currentTrans.target())));
                      toDot << "\t " << currentTrans.target() << "\t [label=\"";
                      toDot << components[0]->getLabel(currentTrans.target());
                      toDot << "\"];" << endl;
                      visited[currentTrans.target()]=true;
                      ++visitedStates;
                      if(currentTrans.target().outDeg() == 0)
                        {
                          ++deadlocks;
                        }
                    }
                  ++queue.front().second;
                }
            }
          std::cout << "REACHABILITY ANALYSIS" << std::endl;
          for(unordered_map<Diades::Automata::Event,bool>::const_iterator it = searchedEvent.begin();
              it != searchedEvent.end(); ++it)
            {
              std::cout << it->first << ": ";
              if(it->second)
                {
                  std::cout << "YES" << std::endl;
                }
              else
                {
                  std::cout << "NO" << std::endl;
                }
            }
          std::cout << "Visited States: " << ((double) visitedStates / (double) components[0]->numberOfStates() * 100.0 ) << "% (" <<  visitedStates << " has been visited)" <<  std::endl;
          std::cout << "Visited Transitions: " << ((double) visitedTransitions / (double) components[0]->numberOfTransitions() * 100.0 ) << "% (" <<  visitedTransitions << " has been visited)" << std::endl;
          std::cout << "Visited deadlocks: " << deadlocks << std::endl;
        }
  else
        {
          Diades::Automata::ComposableModel * model = nullptr;
        

          for(unsigned i = 0 ; i < components.size(); ++i)
                {
                  comps.push_back(new Diades::Automata::ComposableModel(*components[i],rules));
                  for(Diades::Automata::ObservableMask::EventIterator it = components[i]->mask().eventBegin();
                          it !=  components[i]->mask().eventEnd();
                          ++it)
                        {
                          for(Diades::Automata::ObservableMask::ObservableEventIterator it2 = components[i]->mask().observableBegin(*it);
                                  it2 != components[i]->mask().observableEnd(*it);
                                  ++it2)
                                {
                                  mask.addMask(*it,*it2);
                                }
                        }
                }

          model = new  Diades::Automata::ComposableModel(comps,rules,true);
          // check
        }

  std::ofstream file("reachability.dot");
  
  // writing the header
  file << "digraph G {" << endl;
  file << "\tratio=fill;" << endl;
  file << "\tpage=\"8.5,11.6\";" << endl;
  file << "\tsize=\"7.5,10.5\";" << endl;
  file << "\tlabel=\"Component name = reachability\";" << endl;
  file << toDot.str() << endl;
   // writing the end of file
  file << "}" << endl;
  file.close();
 
  clean(components,model,comps);
  return 0;
}