/*******************************************************************************
 * Copyright (c) 2015-2016 ONERA.
 * Ce logiciel est la propriété de l’ONERA (the French Aerospace Lab).
 * 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).
 * 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
 *
 *******************************************************************************/

//#include "algorithms/EmptyStateVisitor.hh"
//#include "algorithms/DotStateVisitor.hh"
#include "grammars/altarica/FiacreTranslator.hh"
//#include "solvers/epochsolver.hh"
//#include "solvers/altaricaLogic.hh"
#include "console/ParsingDriverConsoleReporter.hh"

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

#include "grammars/altarica/Event.hh"
#include "grammars/altarica/Assertion.hh"


namespace epoch {
	namespace console {
		void printStates(int ps, int maxDepth, epoch::altarica::AltaricaState* s, epoch::altarica::AltaricaModel* m) {

			std::cerr << "\ndepth = "<< maxDepth-ps << std::endl;
			std::cerr << s->toString(true, true, true, true);
			if (ps == 0) {
				delete s;
				std::cerr << "\n!!!!!!!!!!!! GOING UP the tree\n"<< std::endl;
				return;
			}

			std::vector<epoch::altarica::MetaEvent*> * mev =  m->getEnabledMetaEventsAll(s);
			std::cerr<<"\n # metaEvents:  "<< mev->size() << std::endl;
			for (int i=0; i<mev->size(); ++i) {
				std::cerr << " MEV " << i << ": " << (*mev)[i]->toString() << std::endl;
			}


			for (int i=0; i<mev->size(); ++i) {
				std::cerr << "\ndoing MEV " << i << ": " << (*mev)[i]->toString() << std::endl;
				epoch::altarica::AltaricaState *s2 =  m->getNextState(s,(*mev)[i]);
				m->evaluateFlowVars(s2);
				printStates(ps-1, maxDepth, s2, m);
			}

//			std::vector<epoch::altarica::Event*> ev =  m->getAtomicEvents();
//					std::cerr<<"\n # Events:  "<< ev.size() << std::endl;
//					for (int i=0; i<ev.size(); ++i) {
//						std::cerr << " EV " << i << ": " << ev[i]->toString() << std::endl;
//					}

		}



		std::string print_pre (const epoch::altarica::AltaricaModel *amodel_, const std::vector<epoch::altarica::Event*> *ev, int n, std::ostringstream * sout) {

			std::ostringstream sret;
			std::string s ;
			if (n < 0)
				return sout->str() + "\n";

			// for (int i = ev->size(); i > 0; --i) {

					// ss << "\tEvent" << i-1;
					unsigned j = 0;
					for (auto &ti : *(ev->at(n)->getTrans()) ) {
						std::ostringstream ss;
						ss <<  sout->str() << ti->getPrecond()->toString( ti->getNode(), amodel_);
						if ( n != 0 )
							ss << " and ";
						//ss <<  sout->str() << "\tE" << n << "T" << j++;
						sret << print_pre(amodel_, ev,  n-1, &ss);


						//								const std::vector<epoch::altarica::Assignment*>* effects = ti->getAssigns();
						//								if(effects->size() > 0) {
						//									for(auto &a : *effects) {
						//										std::cout << "\tpost : "
						//												<< a->getVar()->toFiacre()
						//												//<< a->getMA()->toString()
						//												<< " := "
						//												<< a->getExpr()->toString( a->getNode() )
						//												<< ";" << std::endl;
						//									}
						//								}
				//	}

			}
			return sret.str();
		}


		bool DoAltarica(const std::string& modelFile, const std::string& initFile, const std::string& var1, const std::string& value1, const std::string& var2, const std::string& value2,bool ds, int ps, bool invert_comp1, bool invert_comp2, 
					    int ac, char* av[], int algo, int hess, int blas, double threshold, unsigned int dtimebound, double ctimebound, bool printfunction, const std::string& printGraph) {
			epoch::console::ParsingDriverConsoleReporter pdr;
			epoch::altarica::AltaricaGenerator gen(modelFile, pdr);
			gen.amodel_->setDebugSemantics(ds);

			// if (initFile.compare("") != 0)
			if (initFile.length() >= 4 &&
					0 == initFile.compare(initFile.length() - 4, 4, ".xml"))
				gen.amodel_->setInitInfoXML(initFile);
			else if (initFile.length() >= 5 &&
					0 == initFile.compare(initFile.length() - 4, 4, ".json"))
				gen.amodel_->setInitInfoJSON(initFile);

			epoch::altarica::AltaricaState * i = gen.amodel_->initialState();
			gen.amodel_->evaluateFlowVars(i);
			//			std::cerr << i->toString(true,true,true,true);
			std::cerr << std::endl << "MODEL STATS:" << std::endl;
			std::cerr << "number of state vars: " << gen.amodel_->getNStateVars() << std::endl;
			std::cerr << "number of _different_ flow vars: " << gen.amodel_->getNFlowVars() << std::endl;
			std::cerr << "number of atomic events: " << gen.amodel_->getNEvents() << std::endl;


			//// Debug printing start ////

			if (gen.amodel_->getDebugSemantics())
			{
				std::cout << std::endl << "FLOW VARS" << std::endl;

				for(auto &v : gen.amodel_->getFlowVars()) {

					std::cout << v->getFullName() <<
							" : " <<
							v->getDomain()->toString() <<
							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;
				}

				std::cout << std::endl << "ATOMIC EVTS" << std::endl;
				for(auto &e : gen.amodel_->getAtomicEvents()) {
					std::cout << e->getMA()->toString()
												<< " : "
												<< 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 : ";
								for(auto &a : *t->getAssigns()) {
									std::cout << "		"
											// << a->getVar()->toFiacre() //getVar()->getMA()->toString()
											<< a->getMA()->toString()
											<< " := "
											<< a->getExpr()->toString()
											<< std::endl;
								}
							}
						}
				}

				// Get Syncs //
				unsigned nev=0, ne = 0;
				for(auto &sy :gen.amodel_->getSyncs())
					std::cout	<< sy->toString()<< std::endl;

				std::cout << std::endl << "SYNCS" << std::endl;
				//				for(auto &sy :gen.amodel_->getSyncs())
				//					std::cout	<< sy->toString()<< std::endl;
				unsigned n=0;
				for(auto &sy :gen.amodel_->getMetaEvents()) {
					std::cout << "Meta event" << n++ << std::endl;
					if (sy->getEvents()->size() != 0) {
						for (std::vector<epoch::altarica::Event*>::iterator i = sy->getEvents()->begin();
								i!=sy->getEvents()->end(); ++i) {
							ne = 0;
							for (auto &t : *(*i)->getTrans()) {
								std::cout << nev << "." << ne++ << ". pre : " << t->getPrecond()->toString( t->getNode(), gen.amodel_)  << std::endl;

								if(t->getAssigns()->size() > 0) {
									for(auto &a : *(t->getAssigns())) {
										std::cout << "\tpost : "
												<< a->getVar()->toFiacre()
												//<< a->getMA()->toString()
												<< " := "
												<< a->getExpr()->toString( a->getNode(), gen.amodel_ )
												<< ";" << std::endl;
									}
								}
							}
							++nev;
						}
					}
					else
						std::cout << " NO EVENT";
				}

				////////
				std::cout << std::endl << "SYNCS" << std::endl;

				nev=0; ne = 0;
				for(auto &sy :gen.amodel_->getMetaEvents()) {
					std::cout << std::endl << "Meta event" << nev++ << std::endl;
					if (sy->getEvents()->size() != 0) {

						std::ostringstream ss("init ");

						int num = sy->getEvents()->size()-1;

						std::cout << print_pre(gen.amodel_, sy->getEvents() , num, &ss );

					}
					else
						std::cout << " NO EVENT";
				}
				std::cout << std::endl << "ATOMIC DIRAC EVTS" << std::endl;
				for(auto &e : gen.amodel_->getAtomicDiracEvents()) {
					std::cout << e->getMA()->toString()
						    << " : "
						    << 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: ";
								for(auto &a : *t->getAssigns()) {
									std::cout << "		"
											// << a->getVar()->toFiacre() //getVar()->getMA()->toString()
											<< a->getMA()->toString()
											<< " := "
											<< a->getExpr()->toString()
											<< std::endl;
								}
							}
						}
				}

				std::cout << std::endl << "ASSERTIONS" << std::endl;

				for(auto &e : gen.amodel_->getAsserts()) {
					size_t et = (size_t)(e);
					std::cout << et << " "<< e->getExpr()->toString()<< std::endl;
				}
			}
			//////// Debug printing end ///////


			if (ps >= 0) {
				// Makes a FIACRE model
				std::cerr << "\n!!!!!!!!!!!! Printing FIACRE model\n\n"<< std::endl;

				epoch::altarica::FiacreTranslator f(gen.amodel_);
				f.printFiacre();

			}

			return true;
			// A partir d'ici : algorithme
			//const epoch::altarica::Node& mainNode = *(gen.amodel_->findNodeByName("main"));



			// Formule f1 : tout est ok
 /*     epoch::solvers::AltaricaLogic* f1;


     if (strcmp(var1.c_str(), "") != 0)
        f1 = new  epoch::solvers::AltaricaLogicF2(gen.amodel_,var1,value1, invert_comp1);
      else
        f1 = new  epoch::solvers::AltaricaLogicF1();
      
			epoch::solvers::AltaricaLogicF2 f2(gen.amodel_,var1,value1, invert_comp1);
			epoch::altarica::AltaricaGenerator::State is(i);

			if (printGraph.empty()) {
				return epoch::solvers::MySolver<epoch::solvers::AltaricaLogic, epoch::altarica::AltaricaGenerator, epoch::algorithm::EmptyStateVisitor>::solve(ac, av,
																					                                           algo, hess, blas, threshold, dtimebound, ctimebound,
																					                                           printfunction, epoch::algorithm::EmptyStateVisitor(),
																					                                           gen, is, *f1, f2);
			} else {
				return epoch::solvers::MySolver<epoch::solvers::AltaricaLogic, epoch::altarica::AltaricaGenerator, epoch::algorithm::DotStateVisitor>::solve(ac, av,
																					                                         algo, hess, blas, threshold, dtimebound, ctimebound,
																					                                         printfunction, epoch::algorithm::DotStateVisitor(printGraph),
																					                                         gen, is, *f1, f2);
			}*/
		}
	}
}