/*******************************************************************************
 * Copyright (c) 2015-2017 ONERA and IRT AESE (IRT Saint Exupéry).
 * Ce logiciel est la propriété de l’ONERA (the French Aerospace Lab) et de
 * l'IRT AESE (IRT Saint Exupéry).
 * Tous droits réservés.
 *
 * Ce programme et les éléments qui l'accompagnent sont mis à disposition
 * aux conditions définies par le contrat de licence logiciel CeCILL-C soumise
 * au droit français et respectant les principes de diffusion des logiciels libres.
 * Vous pouvez utiliser, modifier et/ou redistribuer ce programme
 * sous les conditions de la licence CeCILL-C (http://www.cecill.info).

 * This software is property of ONERA (the French Aerospace Lab) and of
 * the IRT AESE (IRT Saint Exupéry).
 * All rights reserved.
 *
 * This program and the accompanying materials are made available under
 * the terms of the CeCILL-C license under French law and
 * abiding by the rules of distribution of free software.
 * You can  use, modify and/ or redistribute the software under the terms of
 * the CeCILL-C license (http://www.cecill.info).
 *
 * Contributeurs/contributors:
 *     Xavier Pucel (ONERA - Centre de Toulouse) - initial API and implementation
 *     Alexandre Albore (IRT Saint-Exupéry) - Altarica/Fiacre translation
 *
 *******************************************************************************/

#include <boost/filesystem.hpp>
#include <boost/program_options.hpp>
#include <boost/exception/diagnostic_information.hpp>

#include "epochconsolealtarica.hh"

#include "grammars/altarica/AltaricaGenerator.hh"
#include "grammars/altarica/Assignment.hh"
#include "grammars/altarica/Event.hh"
#include "grammars/altarica/MemberAccess.hh"
#include "grammars/altarica/Node.hh"
#include "grammars/altarica/Synchronisation.hh"
#include "grammars/altarica/Transition.hh"
#include "grammars/altarica/Variable.hh"

#include "symbolic/SymModel.hh"
//using namespace epoch;

int main(int ac, char* av[]) {
  unsigned int verbosity; // verbosity level
  std::string modelFile;
  std::string initFile;
  bool ds;
  bool printFlow;
  bool printNULL;
  bool printDomain;

  // try {
    boost::program_options::options_description desc("Allowed options");
    desc.add_options()
      ("help", "produce help message")
      ("ds",
       boost::program_options::value<bool>(&ds)->default_value(false),
       "print    semantic debug messages for discrete models")
      ("file",
       boost::program_options::value<std::string>(&modelFile)-> default_value(""),
       "model file (either .alt (altartica) or [.prism|.nm|.pm|.sm] (prism)")
      ("init",
       boost::program_options::value<std::string>(&initFile)->default_value(""),
       "init file")
      ("pf",
       boost::program_options::value<bool>(&printFlow)->default_value(false),
       "print flow vars")
      ("pn",
       boost::program_options::value<bool>(&printNULL)->default_value(false),
       "print null values")
      ("pd",
       boost::program_options::value<bool>(&printDomain)->default_value(false),
       "print var domains")
      ;

    boost::program_options::positional_options_description p;
    p.add("file", 1);


    namespace options_style_ns = boost::program_options::command_line_style;
    int options_style = options_style_ns::allow_short
      | options_style_ns::short_allow_adjacent
      | options_style_ns::short_allow_next
      | options_style_ns::allow_long
      | options_style_ns::long_allow_adjacent
      | options_style_ns::long_allow_next
      | options_style_ns::allow_sticky
      | options_style_ns::allow_dash_for_short;
    boost::program_options::variables_map vm;
    // boost::program_options::store
    // (boost::program_options::parse_command_line(ac, av, desc, options_style),
    // vm);
    boost::program_options::store
      (boost::program_options::command_line_parser(ac,av).options(desc).
       positional(p).style(options_style).run(),
       vm);
    boost::program_options::notify(vm);

    if (vm.count("help")) {
      std::cout << desc << std::endl;
      return 1;
    }

    epoch::console::ParsingDriverConsoleReporter pdr;
    epoch::altarica::AltaricaGenerator gen(modelFile, pdr);
    gen.amodel_->setDebugSemantics(ds);

    // if (initFile.compare("") != 0)
    //    gen.amodel_->setInitInfo(initFile);

    // std::cout << std::endl << "MODEL STATS:" << std::endl;

    // std::cout << "number of state vars: "
    //            << gen.amodel_->getNStateVars()
    //            << std::endl;

    // std::cout << "number of _different_ flow vars: "
    //            << gen.amodel_->getNFlowVars()
    //            << std::endl;

    // std::cout << "number of atomic events: "
    //            << gen.amodel_->getNEvents()
    //            << std::endl
    //            << std::endl;

    std::cout << std::endl << "FLOW VARS" << std::endl;
    for(auto &v : gen.amodel_->getFlowVars()) {
      std::cout << v->getFullName() << " : "
                << v->getDomain()->toString()
                // << std::endl
                // << "var at " << v->getIndex()
                // << " is "
                // << gen.amodel_->getFlowVar(v->getIndex())->getFullName()
                << std::endl;
    }

    std::cout << std::endl << "STATE VARS" << std::endl;
    for(auto &v : gen.amodel_->getStateVars()) {
      std::cout << v->getFullName()
                << " : "
                << v->getDomain()->toString()
                // << std::endl
                // << "var at " << v->getIndex()
                // << " is "
                // << gen.amodel_->getStateVar(v->getIndex())->getFullName()
                << std::endl;
    }

    std::cout << std::endl << "ATOMIC EVTS" << std::endl;
    for(auto &e : gen.amodel_->getAtomicEvents()) {
      std::cout << e->getFullName()
                << " : "
                << std::endl;
      if(e->getTrans()->size() > 0)
        for(auto &t : *e->getTrans()) {
          std::cout << "  pre : "
                    << t->getPrecond()->toString()
                    << std::endl;
          if(t->getAssigns()->size() > 0) {
            std::cout   << "  post: " << std::endl;
            for(auto &a : *t->getAssigns()) {
              std::cout << "    "
                        << a->getVar()->toString()
                        << " := "
                        << a->getExpr()->toString()
                        << std::endl;
            }
          }
        }
    }

    std::cout << std::endl << "SYNCS" << std::endl;
    for(auto &s: gen.amodel_->getSyncs()) {
      if(s->getMA() != NULL)
        std::cout << s->toString() << std::endl;
      if(s->getMandatoryEvents()->size() > 0) {
        std::cout << "  Mandatory events:" << std::endl;
        for(auto &e : *s->getMandatoryEvents())
          std::cout << "    " << e->getFullName() << std::endl;
      }
      if(s->getOptionalEvents()->size() > 0) {
        std::cout << "  Optional events:" << std::endl;
        for(auto &e : *s->getOptionalEvents())
          std::cout << "    " << e->getFullName() << std::endl;
      }
      if(s->getNumericalConstant() >= 0) {
        std::cout << "  Constraint type: " << s->getConstraintType() << std::endl;
        std::cout << "  Numerical constant: "
                  << s->getNumericalConstant()
                  << std::endl;
      }
    }

    epoch::symbolic::SymModel bddmodel(gen.amodel_);

    // } 
// catch (const boost::program_options::error& error) {
//     std::cerr << error.what() << std::endl;
//     return -1;
//   } catch (const epoch::altarica::AltaricaException& error) {
//     std::cerr << error.what() << std::endl;
//     return -1;
//   } catch (const std::exception& error) {
//     std::cerr << boost::diagnostic_information(error) << std::endl;
//     return -1;
//   }
}