Explain.cc

Go to the documentation of this file.

#include <cstdlib>
#include<iostream>
#include<iterator>
#include<fstream>
#include<regex>
#include<boost/program_options.hpp>
#include<diades/automata/experimental/DdAutFile.hh>
#include<diades/automata/experimental/DdAutFileDescriptor.hh>
#include<diades/automata/experimental/Printer.hh>
#include<diades/automata/experimental/StateMachine.hh>
#include<diades/automata/experimental/Explanation.hh>
#include<diades/automata/experimental/TreeViewHtml.hh>
#include"../AutomataInterface.hh"

using namespace std;
using namespace Diades::Automata::Experimental;
using namespace Diades::Utils;
using namespace Diades::CmdInterface;

namespace Poptions = boost::program_options;



const string program("dd-explain");

/*
 * File suffixes
 */
FileSuffixes suffixes({"log", "ddaut", "obs", "html"});

void
initialiseOptions(int argc, char * argv[],
                  Poptions::options_description & desc,
                  Poptions::variables_map & vm)
{
  desc.add_options()
    ("help,h", "produce help message")
    ("file,f", Poptions::value< string >(), "A||P automaton file (.ddaut format)")
    ("log,l", Poptions::value< string >(), "L log file (.log format)")
    ("obs,s", Poptions::value< string >(), "observable event  file (.obs format)")
    ("output,o", Poptions::value< string >(), "outfile name (.ddaut format)")
    ("web,w", Poptions::value< string >(), "html file name (.html format)")
    ;
  Poptions::positional_options_description p;
  p.add("file", 1);
  Poptions::store(Poptions::command_line_parser(argc, argv).options(desc).positional(p).run(), vm);
  Poptions::notify(vm);
}


using Diades::Automata::Experimental::DdAutFA;
using Diades::Automata::Experimental::DdAutEventManager;
using Diades::Automata::Experimental::DdAutStateManager;


bool explainLog(const DdAutFA & fa,DdAutFA & explanations,DdAutFA & fullExplanations,
                const DdAutStateManager & sManager,DdAutStateManager & sManagerExplanation,
                const DdAutEventManager & eManager,
                std::istream & logfile,
                std::istream & obsfile,
                std::unordered_map<DdAutFA::State, unordered_set<DdAutFA::Transition> >  & safeAlternatives)
{
  std::vector<std::string> observations;
  std::istream_iterator<std::string> it(logfile);
  std::istream_iterator<std::string> end;
  while(it!=end)
    {
      observations.emplace_back(*it);
      ++it;
    } 
  Observables observables;
  std::istream_iterator<std::string> itobs(obsfile);
  while(itobs!=end)
    {
      std::for_each(eManager.begin(),eManager.end(),
                    [&](DdAutEventManager::EventId eventId)
                    {
                      if(eManager.getEvent(eventId).find(*itobs)!=DdAutEventManager::Event::npos)
                        {
                          observables.insert(eventId);
                        }
                    });
      ++itobs;
    }
  return explain(fa, sManager, eManager, observations, observables, explanations,
                 fullExplanations,sManagerExplanation,safeAlternatives);
}


void consolidateWithSafeAlternatives(const DdAutFA & fsa,
                                     const DdAutStateManager & sManager,
                                     DdAutFA & explanations,
                                     DdAutStateManager & sManagerExplanation,
                                     const SafeAlt<DdAutFA>  & safeAlternatives)
{
  for(auto stateSafeAlternatives: safeAlternatives)
    {
      auto explSafeSourceId = explanations.getStatePropertyId( stateSafeAlternatives.first);
      for(auto safeTrans : stateSafeAlternatives.second)
        {
          auto fsaSafeSourceId = fsa.getStatePropertyId(safeTrans.source()); 
          auto fsaSafeTargetId = fsa.getStatePropertyId(safeTrans.target()); 
          auto explSafeTargetId = sManagerExplanation.statePropertyId("safe_" + sManager.getStateProperty(fsaSafeSourceId) + "->" + sManager.getStateProperty(fsaSafeTargetId));
          explanations.newTransition(explSafeSourceId,explSafeTargetId,fsa.getEvent(safeTrans));
        }
    }
}


void  writeTreeViewSafeAlternative(std::ostream & html,
                                   const DdAutFA & fa,
                                   const DdAutStateManager & sManager,
                                   const DdAutEventManager & eManager,
                                   DdAutFA::Transition t)
{

  html << listSingleItem("Safe alternative: from state "
                         + sManager.getStateProperty(fa.getStatePropertyId(t.source()))
                         + " to state "
                         + sManager.getStateProperty(fa.getStatePropertyId(t.target()))
                         + " by event "
                         + eManager.getEvent(fa.getEvent(t))
                         + ".") << "\n";
}


void writeTreeViewTransition(std::ostream & html,
                             const DdAutFA & fa,
                             const DdAutStateManager & sManager,
                             const DdAutEventManager & eManager,
                             const DdAutFA & explanation,
                             const DdAutStateManager & sManagerExplanation,
                             const SafeAlt<DdAutFA> & safeAlternatives,
                             DdAutFA::Transition transition)
{
  using Fsm = DdAutFA;
  using Transition = typename Fsm::Transition;

  if(explanation.isAcceptingState(transition.target()))
    {
      html << listSingleItem("Event "
                             +
                             eManager.getEvent(explanation.getEvent(transition))
                             +
                             " leading to state "
                             +
                             sManagerExplanation.getStateProperty(explanation.getStatePropertyId(transition.target()))
                             +
                             " violates the property.") << "\n";
    
  
    }
  else
    {
      html << startListCaretItem("Event "
                                 +
                                 eManager.getEvent(explanation.getEvent(transition))
                                 +
                                 " leading to state "
                                 +
                                 sManagerExplanation.getStateProperty(explanation.getStatePropertyId(transition.target())))
           << "\n"
           << startNestedTree()
           << "\n";
      std::for_each(explanation.outputTransitionBegin(transition.target()),
                    explanation.outputTransitionEnd(transition.target()),
                    [&](Transition t)
                    {
                      writeTreeViewTransition(html,fa,sManager,eManager,explanation,sManagerExplanation,safeAlternatives,t);
                    });
      auto altIt = safeAlternatives.find(transition.target());
      if(altIt != safeAlternatives.end())
        {
          const auto & safeAlt = altIt->second;
          std::for_each(safeAlt.begin(),safeAlt.end(),
                        [&](Transition t)
                        {
                          writeTreeViewSafeAlternative(html,fa,sManager,eManager,t);
                        });

        }
      html << endNestedTree()
           << "\n"
           << endListCaretItem()
           << "\n";
      
    }
 
}



void writeTreeView(std::ostream & html,
                   const DdAutFA & fa,
                   const DdAutStateManager & sManager,
                   const DdAutEventManager & eManager,
                   const DdAutFA & explanation,
                   const DdAutStateManager & sManagerExplanation,
                   const SafeAlt<DdAutFA> & safeAlternatives)
{
  using Fsm = DdAutFA;
  using Transition = typename Fsm::Transition;
  toTreeViewHtmlStart(html);
  html << startTree("myexplanation") << "\n";
  for(auto it = explanation.initialStateBegin();
      it != explanation.initialStateEnd();
      ++it)
    {
      if(it->outDeg()==0)
        {
          html << listSingleItem(sManagerExplanation.getStateProperty(explanation.getStatePropertyId(*it))) << "\n";
        }
      else
        {
          html << startListCaretItem(sManagerExplanation.getStateProperty(explanation.getStatePropertyId(*it)))
               << "\n"
               << startNestedTree()
               << "\n";
          std::for_each(explanation.outputTransitionBegin(*it),
                        explanation.outputTransitionEnd(*it),
                        [&](Transition t)
                        {
                          writeTreeViewTransition(html,fa,sManager,eManager,explanation,sManagerExplanation,safeAlternatives,t);
                        });
          auto altIt = safeAlternatives.find(*it);
          if(altIt != safeAlternatives.end())
            {
              const auto & safeAlt = altIt->second;
              std::for_each(safeAlt.begin(),safeAlt.end(),
                            [&](Transition t)
                            {
                              writeTreeViewSafeAlternative(html,fa,sManager,eManager,t);
                            });

            }
          html << endNestedTree()
               << "\n"
               << endListCaretItem()
               << "\n";
        }
      html << endTree();
      toTreeViewHtmlEnd(html);
    }
}



size_t
    explainFsm(const std::string & fileName,
               const std::string & logName,
               const std::string & observableName,
               const std::string & output,
               const std::string & htmlName)
{

  if(!suffixes.match(fileName, "ddaut"))
    {
      return printCommandLineError(Msg("Expecting a file with a name ending with .ddaut, but I read %1%") % fileName);
    }
  if(!suffixes.match(logName,"log"))
    {
      return printCommandLineError(Msg("Expecting a file with a name ending with .log, but I read %1%") % fileName);
    }
  if(!suffixes.match(observableName,"obs"))
    {
      return printCommandLineError(Msg("Expecting a file with a name ending with .obs, but I read %1%") % fileName);
    }

  DdAutFileDescriptor descriptor;
  DdAutEventManager eManager;
  DdAutStateManager sManager;
  DdAutStateManager sManagerExplanation;
  ifstream file(fileName.c_str());
  if(file.is_open())
    {
      auto loaded = descriptor.readStream(file);
      file.close();
      if(!loaded)
        {
          return printCommandLineError(Msg("Error when loading the 'ddaut' automaton file %1%") % fileName);
        }
    }
  else
    {
      return printCommandLineError(Msg("Error when opening the 'ddaut' automaton file %1%") % fileName);
    }
  if(descriptor.acceptorBegin() == descriptor.acceptorEnd())
    {
      return printCommandLineError(Msg("Error the 'ddaut' automaton file %1% has no acceptor states that assert how the behaviour of the system can violate a given property") % fileName);
    }
  DdAutFA fa;
  if(!faFromDescriptor(descriptor, fa, sManager, eManager))
    {
      return printCommandLineError(Msg("Error cannot read the descriptor of the 'ddaut' automaton file %1%, BUG") % fileName);
    }
  ifstream logfile(logName.c_str());
  if(!logfile.is_open())
    {
      return printCommandLineError(Msg("Error when opening the 'log' file %1%") % logName);
    }
  ifstream obsfile(observableName.c_str());
  if(!obsfile.is_open())
    {
      return printCommandLineError(Msg("Error when opening the 'obs' file %1%") % observableName);
    }
  
  DdAutFA explanation;
  DdAutFA fullExplanation;
  SafeAlt<DdAutFA>  safeAlternatives;
  if(!explainLog(fa,explanation,fullExplanation,
                 sManager,sManagerExplanation,eManager,
                 logfile,obsfile,safeAlternatives))
    {
      return printCommandLineError(Msg("Error in the explanation phase of why system %1% violates the safety property based on the observations %2% and the observability of the system defined in %3%") % fileName % logName % observableName);
    }
 
  if(!htmlName.empty())
    {
      if(!suffixes.match(htmlName, "html"))
        {
          printCommandLineWarning(Msg("Expecting a file with a name ending with .html, but I read %1% so I do not export the explanation tree.") % htmlName);
        }
      else
        {
          ofstream htmlfile(htmlName.c_str());
          if(!htmlfile.is_open())
            {
              printCommandLineWarning(Msg("Error when opening the 'html' file %1% so I do not export the explanation tree.") % logName);
            }
          writeTreeView(htmlfile,fa,sManager,eManager,explanation,sManagerExplanation,safeAlternatives);
          htmlfile.close();
        }
    }
  consolidateWithSafeAlternatives(fa,sManager,explanation,sManagerExplanation,safeAlternatives);
  writeFiniteAutomaton({explanation, sManagerExplanation, eManager}, output, suffixes);
  return writeFiniteAutomaton({fullExplanation, sManagerExplanation, eManager}, "full_" + output, suffixes);
}

int
main(int argc, char** argv)
{
  std::string fileName, output, logName, observableName, htmlName;
  try
    {
      Poptions::options_description desc("Options");
      Poptions::variables_map vm;
      initialiseOptions(argc, argv, desc, vm);
      if(vm.count("help"))
        {
          return printUsage(program, desc);
        }
      if(vm.count("file"))
        {
          fileName = vm["file"].as<std::string>();
        }
      if(vm.count("log"))
        {
          logName = vm["log"].as<std::string>();
        }
      if(vm.count("output"))
        {
          output = vm["output"].as<std::string>();
        }
      if(vm.count("obs"))
        {
          observableName = vm["obs"].as<std::string>();
        }
      if(vm.count("web"))
        {
          htmlName = vm["web"].as<std::string>();
        }
    }
  catch(Poptions::required_option & e)
    {
      return printCommandLineError(e.what());
    }
  catch(Poptions::error & e)
    {
      return printCommandLineError(e.what());
    }
  return explainFsm(fileName,logName,observableName,output,htmlName);
}