/*******************************************************************************
 * 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:
 *     Florent Teichteil-Königsbuch (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 "grammars/altarica/altarica_lexer.h"
#include "epochconsolealtarica.hh"
//#include "epochconsoleprism.hh"

#include "grammars/altarica/AltaricaGenerator.hh"
#include "grammars/altarica/AltaricaJson.hh"
#include "grammars/altarica/AltaricaInitInfoXML2.hh"
#include "grammars/altarica/AltaricaInteractive.hh"
//#include "algorithms/incrTarjan.hh"
// #include "algorithms/LinearSystemExactParametricSolver.hh"
#include "grammars/details/parsingdriverbaseimpl.hh"
// #include "solvers/altaricaLogic.hh"
#include <ios>

//using namespace epoch;

int main (int ac, char* av[])
{
	unsigned int verbosity; // verbosity level
	std::string modelFile;
	std::string jsonFile;
	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)")
		("json", boost::program_options::value<std::string>(&jsonFile)->default_value(""), "json file (init, testcases)")
		("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;	    


		boost::filesystem::path filepath(modelFile);
		if (!filepath.has_extension()) {
			std::cerr << "File '" << filepath << "' has no extension!" << std::endl;
			return -1;
		} else if (filepath.extension().generic_string() == ".alt") { // altarica
      epoch::altarica::AltaricaGenerator gen(modelFile, pdr);
      gen.amodel_->setDebugSemantics(ds);
      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;


		epoch::altarica::AltaricaJson * aj;
		if (jsonFile.compare("") != 0)  {
		    aj = gen.amodel_->setInitInfoJSON(jsonFile);
		    std::cout << aj->toString() <<std::endl;
		}
		
		epoch::altarica::AltaricaState * cstate = gen.amodel_->initialState();		
		std::cout << "Initial State:\n";
		if (printFlow)
		    gen.amodel_->evaluateFlowVars(cstate);
		std::cout << cstate->toString(true,printFlow,printNULL,printDomain);       

		if (jsonFile.compare("") != 0) {
		    if (aj->hasEvents())
			return aj->runTestCase(cstate);
		} 
		if (jsonFile.compare("") == 0 || !aj->hasEvents())
		    epoch::altarica::interactiveExecute(cstate, gen.amodel_,printFlow, printNULL, printDomain);		



//      epoch::altarica::interactiveExecute(gen.amodel_->initialState(),  gen.amodel_,true, false, false);		

      // typedef epoch::algorithm::IncrTarjan<epoch::solvers::AltaricaLogic,
      //                                      epoch::altarica::AltaricaGenerator, 
      //                                      epoch::graph::HashTable, 
      //                                      epoch::graph::List,
      //                                      epoch::algorithm::LinearSystemExactParametricSolver> myTarjanAlt;
      // myTarjanAlt mt(gen);
      // epoch::solvers::AltaricaLogicF1 f1;
      // epoch::solvers::AltaricaLogicF2 f2(gen.amodel_, "main.s", "s9", false);
      
      // mt.launch(gen.amodel_->initialState(), f1, f2);
//      delete gen.amodel_;


		}

		/*** removing PRISM extension ****

      else if (filepath.extension().generic_string() == ".prism" ||
               filepath.extension().generic_string() ==".nm" ||
               filepath.extension().generic_string() == ".pm" ||
               filepath.extension().generic_string() == ".sm") { // prism file
      epoch::prism::ParsingDriver parser(epoch::prism::ParsingDriver::PARSE_MODULES, pdr, modelFile);
      parser.context().setType(epoch::prism::Context::PRISM_TYPE_DTMC);
      parser.Parse();      
      parser.context().setType(epoch::prism::Context::PRISM_TYPE_DTMC);
      epoch::prism::Generator<epoch::prism::Context::PRISM_TYPE_DTMC> gen(parser.context());
      typedef
        epoch::algorithm::IncrTarjan<epoch::solvers::PrismLogic,
                                     epoch::prism::Generator<epoch::prism::Context::PRISM_TYPE_DTMC>, 
                                     epoch::graph::HashTable, 
                                     epoch::graph::List,
                                     epoch::algorithm::LinearSystemExactParametricSolver> myTarjanPrism;
      myTarjanPrism mt(gen);

      typename epoch::prism::Generator<epoch::prism::Context::PRISM_TYPE_DTMC>::State is(parser.context());
      for (epoch::prism::Context::BooleanVariableMap::const_iterator bi = parser.context().getBooleanVariables().begin() ; bi != parser.context().getBooleanVariables().end() ; ++bi) {
        if (!(bi->second->isInitialValueSpecified())) {
          std::cerr << "Initial value not specified for variable '" << *(bi->first) << "': assuming lowest value of its range" << std::endl;
        }
        is.m_BooleanVariables[bi->second->getIndex()] = bi->second->getInitialValue();
      }
      for (epoch::prism::Context::IntegerVariableMap::const_iterator ii = parser.context().getIntegerVariables().begin() ; ii != parser.context().getIntegerVariables().end() ; ++ii) {
        if (!(ii->second->isInitialValueSpecified())) {
          std::cerr << "Initial value not specified for variable '" << *(ii->first) << "': assuming lowest value of its range" << std::endl;
        }
        is.m_IntegerVariables[ii->second->getIndex()] = ii->second->getInitialValue();
      }
      for (epoch::prism::Context::DecimalVariableMap::const_iterator di = parser.context().getDecimalVariables().begin() ; di != parser.context().getDecimalVariables().end() ; ++di) {
        if (!(di->second->isInitialValueSpecified())) {
          std::cerr << "Initial value not specified for variable '" << *(di->first) << "': assuming lowest value of its range" << std::endl;
        }
        is.m_DecimalVariables[di->second->getIndex()] = di->second->getInitialValue();
      }
      for (epoch::prism::Context::ModuleMap::const_iterator mi = parser.context().getModules().begin() ; mi != parser.context().getModules().end() ; ++mi) {
        for (epoch::prism::Context::BooleanVariableMap::const_iterator bi = mi->second->getBooleanVariables().begin() ; bi != mi->second->getBooleanVariables().end() ; ++bi) {
          if (!(bi->second->isInitialValueSpecified())) {
            std::cerr << "Initial value not specified for variable '" << *(bi->first) << "': assuming lowest value of its range" << std::endl;
          }
          is.m_BooleanVariables[bi->second->getIndex()] = bi->second->getInitialValue();
        }
        for (epoch::prism::Context::IntegerVariableMap::const_iterator ii = mi->second->getIntegerVariables().begin() ; ii != mi->second->getIntegerVariables().end() ; ++ii) {
          if (!(ii->second->isInitialValueSpecified())) {
            std::cerr << "Initial value not specified for variable '" << *(ii->first) << "': assuming lowest value of its range" << std::endl;
          }
          is.m_IntegerVariables[ii->second->getIndex()] = ii->second->getInitialValue();
        }
        for (epoch::prism::Context::DecimalVariableMap::const_iterator di = mi->second->getDecimalVariables().begin() ; di != mi->second->getDecimalVariables().end() ; ++di) {
          if (!(di->second->isInitialValueSpecified())) {
            std::cerr << "Initial value not specified for variable '" << *(di->first) << "': assuming lowest value of its range" << std::endl;
          }
          is.m_DecimalVariables[di->second->getIndex()] = di->second->getInitialValue();
        }
      }
      epoch::solvers::PrismLogic F1("", parser.context(),pdr);
      epoch::solvers::PrismLogic F2("", parser.context(),pdr);
      
      mt.launch(is, F1, F2);

    }
    
    */


    // epoch::altarica::AltaricaInitInfoXML2 *aix2 = new  epoch::altarica::AltaricaInitInfoXML2(jsonFile, gen.amodel_);
    // std::cout << aix2->toString();
    // exit(0);



  
    
    exit(0);
    
    
    

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