SupremicaFormat.cc

Go to the documentation of this file.

#include <list>
#include <map>
#include <iostream>
#include <boost/property_tree/ptree.hpp>
#include <boost/property_tree/xml_parser.hpp>
#include <boost/foreach.hpp>
#include <utils/CmdInterface.hh>


using std::list;
using std::map;
using namespace Diades::Utils;


/************************************************************************************/

typedef enum { HELP=0 } Option;
typedef enum { XML=0 } FileExtension;
unsigned numberOfOptions = 1;
unsigned numberOfFileExtensions = 2;


vector<string> fileExtensions(numberOfFileExtensions);
vector<string> options(numberOfOptions);
vector<bool> isSet(numberOfOptions,false);

string description="Usage: dd-convert-supremica [--help |  automaton.xml] \n\t Print the component described in the xml file (export of supremica) in the 'des_comp' format.";

void initialiseOptions()
{
  options[HELP]             = "--help";
  fileExtensions[XML]     = "xml";
}

/************************************************************************************/


void readParameters(int argc, char * argv[],string & filename);


/************************************************************************************/

int main(int argc, char * argv[])
{
  
  using std::string;
  string filename;
  initialiseOptions();
  readParameters(argc,argv,filename);
  string initialState;
  string otherStates;

  string observables;
  unsigned numberOfObservables = 0;

  string nonObservables;
  unsigned numberOfNonObservables = 0;
  
  unsigned stateNumber = 0;



  unsigned transNumber = 0;
  string transitions;
  
  using boost::property_tree::ptree;
  ptree pt;
  read_xml(filename,pt);

  map<unsigned,string> mapStates;
  map<unsigned,string> mapEvents;

  
    
  BOOST_FOREACH(ptree::value_type const& v, pt.get_child("Automata"))
    {
      if(v.first == "<xmlattr>")
        {
          //std::cout << v.second.get<std::string>("name") << std::endl;
          //std::cout << v.second.get<unsigned>("major") << std::endl;
          //std::cout << v.second.get<unsigned>("minor") << std::endl;
        }
      if(v.first == "Automaton")
        {
         BOOST_FOREACH(ptree::value_type const& v2, v.second.get_child(""))
           {
             
             if(v2.first == "<xmlattr>")
               {
                 std::cout << v2.second.get<std::string>("name") << std::endl;

               }
             
             if(v2.first == "Events")
               {
                 BOOST_FOREACH(ptree::value_type const& evt, v2.second.get_child(""))
                   {
                     BOOST_FOREACH(ptree::value_type const& evtAttr, evt.second.get_child(""))
                       {
                        
                         //std::cout << "Event: id=" << evtAttr.second.get<unsigned>("id") << " label=" <<   evtAttr.second.get<std::string>("label") << std::endl;
                         if(evtAttr.second.count("observable") != 0)
                           {
                             if( evtAttr.second.get<bool>("observable")  )
                               {
                                 observables += "o" + evtAttr.second.get<std::string>("id") + " ";
                                 mapEvents[evtAttr.second.get<unsigned>("id")] ="o" + evtAttr.second.get<std::string>("id");
                                 ++numberOfObservables;
                               }
                             else
                               {
                                 nonObservables += "u" + evtAttr.second.get<std::string>("id") + " ";
                                 mapEvents[evtAttr.second.get<unsigned>("id")] =  "u" + evtAttr.second.get<std::string>("id");
                                 ++numberOfNonObservables;

                               }
                             //std::cout << " observable? " <<  evtAttr.second.get<bool>("observable") <<  std::endl;
                           }
                         else
                           {
                             observables += "o" + evtAttr.second.get<std::string>("id") + " ";
                             mapEvents[evtAttr.second.get<unsigned>("id")] ="o" + evtAttr.second.get<std::string>("id");
                             ++numberOfObservables;
                             //std::cout << " observable? " << true << std::endl;
                           }
                         if(evtAttr.second.count("controllable") != 0)
                           {
                             //std::cout << " controllable? " <<  evtAttr.second.get<bool>("controllable") << std::endl;
                           }
                         else
                           {
                             //std::cout << " controllable? " <<  true  << std::endl;
                           }
                       }
                   }
             
           

               }
              if(v2.first == "States")
               {
                  BOOST_FOREACH(ptree::value_type const& state, v2.second.get_child(""))
                   {
                     
                     BOOST_FOREACH(ptree::value_type const& stateAttr, state.second.get_child(""))
                       {
                         stateNumber++;
                         mapStates[stateAttr.second.get<unsigned>("id")] = "q" + stateAttr.second.get<string>("id");
                         //std::cout << "State: id=" << stateAttr.second.get<unsigned>("id") << " name=" <<   stateAttr.second.get<std::string>("name") << std::endl;
                         // if(stateAttr.second.count("accepting") != 0)
                         //  {
                             //std::cout << " accepting? " <<  stateAttr.second.get<bool>("accepting") <<  std::endl;
                         // }
                         //else
                         // {
                             //std::cout << " accepting? " << false << std::endl;
                         //  }
                           
                         if(stateAttr.second.count("initial") != 0)
                           {
                             if(stateAttr.second.get<bool>("initial"))
                               {
                                 initialState = "q" + stateAttr.second.get<std::string>("id");
                               }
                             else
                               {
                                 otherStates +=  "q" + stateAttr.second.get<std::string>("id") + " ";
                               }
                             //std::cout << " initial? " <<  stateAttr.second.get<bool>("initial") << std::endl;
                           }
                         else
                           {
                             //std::cout << " initial? " << false << std::endl;
                             otherStates += "q" +  stateAttr.second.get<std::string>("id") + " ";
                           }
                       }
                   }
               }
              //stateAttr id="497" name="on1.open1.on2.closed2.faulty3_off.open3" accepting="true
              if(v2.first == "Transitions")
               {
                 BOOST_FOREACH(ptree::value_type const& transition, v2.second.get_child(""))
                   {
                     
                     BOOST_FOREACH(ptree::value_type const& transAttr, transition.second.get_child(""))
                       {
                         ++transNumber;
                         transitions += mapStates[transAttr.second.get<unsigned>("source")] + " -> " + mapStates[transAttr.second.get<unsigned>("dest")] + " " + mapEvents[transAttr.second.get<unsigned>("event")] + "\n";
                         //std::cout << "Transition: source=" << transAttr.second.get<unsigned>("source")
                         //        << " dest=" <<   transAttr.second.get<unsigned>("dest") <<  " event="
                         //        << transAttr.second.get<unsigned>("event") << std::endl;
                       }
                   }
               }
              //<Transition source="511" dest="509" event="8"/>

           }
           
        }
    }

  std::cout << stateNumber << std::endl;
  std::cout << initialState << " " << otherStates << std::endl;
  std::cout << 0 << std::endl;
  std::cout << numberOfNonObservables << std::endl;
  std::cout << nonObservables << std::endl;
  std::cout << 0 << std::endl;
  std::cout << numberOfObservables << std::endl;
  std::cout << observables << std::endl;
  std::cout << transNumber <<  std::endl;
  std::cout << transitions << std::endl;
}


void readParameters(int argc, char * argv[],string & filename)
{
  list<string> modelFiles;
  if(argc < 1)
    {
      printUsage(description);
      exit(1);
    }

  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.");
              exit(1);;
            }
          else
            {
              isSet[currentOption] = true;
            }
          switch(currentOption)
            {
            case HELP:
              {
                printUsage(description);
                exit(0);;
                break;
              }
            }
        }
      else
        {
          
          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]));
              exit(1);;
            }
          FileExtension extension = XML;
          switch(extension)
            {
            case XML:
              {
                modelFiles.push_back(string(argv[index]));
                break;
              }
            }
          ++index;
        }
    }
  if(modelFiles.size() >1)
    {
      printError("Too many xml files, one only is allowed");
      exit(1);
    }
  if(modelFiles.size() == 0)
    {
      printError("No xml files, one only is mandatory");
      exit(1);
    }
  filename = modelFiles.front();
}