/*
 * This file is part of PARAM.
 *
 * PARAM is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * PARAM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with PARAM. If not, see <http://www.gnu.org/licenses/>.
 *
 * Copyright 2009-2010 Ernst Moritz Hahn (emh@cs.uni-sb.de)
 */

#include <stdlib.h>
#include <stdbool.h>
#include <string.h>
#include <sstream>
#include <iomanip>
#include "PMC.h"
#include "SPMC.h"
#include "GPMC.h"
#include "ProgramOptions.h"
#include "Statistics.h"
#include "Controller.h"
#include "PASSStateExplorer.h"
#include "LowLevelStateExplorer.h"
#include "Quotient.h"
#include "Eliminator.h"
#include "BoundedIterator.h"
#include "RegionScheduler.h"
#include "ResultPrinter.h"

namespace parametric {
  namespace po = boost::program_options;
  using namespace std;
  using namespace Rational;
  
  Controller::Controller(int argc, char *argv[]) {
    printStartMessage();

    vm = parseCommandLine(argc, argv);
    /* exit if requested or wrong syntax used */
    if (!vm.count("help")) {
      if (0 == vm.count("model-file")) {
	throw runtime_error("No model file given");
      }
      statistics = new Statistics();
      statistics->totalTime.start();
      
      if (!vm.count("nolump")) {
	pmc = new SPMC();
      } else {
	pmc = new GPMC();
      }
      parse();

      if (0 != vm.count("model-dot")) {
        printDOT(vm["model-dot"].as<string>());
      }
      RegionScheduler result;
      execute(result);
      
      ResultPrinter resultPrinter;
      resultPrinter.setPlotStep(vm["plot-step"].as<string>());
      resultPrinter.setOutputPrefix(vm["result-file"].as<string>());
      resultPrinter.setOutputFormat(vm["result-format"].as<string>());
      resultPrinter.setResult(result);
      resultPrinter.print();
      printStatistics();
    }
  }

  Controller::~Controller() {
    delete pmc;
    delete statistics;
  }

  void Controller::printStartMessage() const {
    cout << 
  " ------------------------------------------------------------------- \n"
  "|                 PARAMetric Markov Model Analyser                  |\n"
  "|                        PARAM version 1.8                          |\n"
  "|           Copyright (C) Saarland University, 2008-2010.           |\n"
  "|                             Author:                               |\n"
  "|                 E. Moritz Hahn (emh@cs.uni-sb.de)                 |\n"
  "|         Authors of parser for extension of PRISM language:        |\n"
  "|          Bjoern Wachter (bjoern.wachter@comlab.ox.ac.uk)          |\n"
  "|                 E. Moritz Hahn (emh@cs.uni-sb.de)                 |\n"
  "|          PARAM  is distributed under the GPL conditions           |\n"
  "|           (GPL stands for GNU General Public License)             |\n"
  "|          The product comes with ABSOLUTELY NO WARRANTY.           |\n"
  "|  This is a free software, and you are welcome to redistribute it. |\n"
  " ------------------------------------------------------------------- \n\n";
  }
  
  void Controller::printDOT(const string &filename) const {
    ofstream file(filename.c_str(), ios::out);
    printDOT(file);
    file.close();
  }
  
  /**
   * Print model to output stream @a stream in GraphViz format.
   *
   * @param stream stream to print model to
   */
  void Controller::printDOT(ostream &stream) const {
    stream << "digraph G {" << endl;
    
    /* print states include target/initial markings */
    for (PMM::state state(0); state < pmc->getNumStates(); state++) {
      stream << "  " << state;
      if (targetStates.find(state) != targetStates.end()) {
        stream << "[shape=\"circle\", style=\"filled\", fillcolor=\"black\"]";
      }
      stream << ";" << endl;
      if (initStates.find(state) != initStates.end()) {
        stream << "init_" << state <<
          " [label=\"\", fillcolor=\"black\", width=\"0.0\""
          " shape=\"circle\", style=\"filled\", root];" << endl;
        stream << "  init_" << state << " -> "
               << state << endl;
      }
    }

    /* print transitions between states */
    for (PMM::state state(0); state < pmc->getNumStates(); state++) {
      for (unsigned succ(0); succ < pmc->getNumSuccStates(state); succ++) {
	PMM::state succState = pmc->getSuccState(state, succ);
	RationalFunction succProb = pmc->getSuccProb(state, succ);
        stream << "  " << state << " -> "      
               << succState << " [label=\"" << succProb;
        if (isRewardAnalysis()) {
	  RationalFunction succReward = pmc->getSuccReward(state, succ);
          stream << " // " << succReward;
        }
        stream << "\",labelfontsize=10];" << endl;
      }    
    }
    stream << "}" << endl;
  }
  
  /**
   * Print model to standard output in GraphViz format.
   */
  void Controller::printDOT() const {
    printDOT(cout);
  }
  
  void Controller::embed() {
    for (PMM::state state(0); state < pmc->getNumStates(); state++) {
      RationalFunction sum(0);
      for (unsigned succ(0); succ < pmc->getNumSuccStates(state); succ++) {
	RationalFunction succProb = pmc->getSuccProb(state, succ);
	sum += succProb;
      }
      for (unsigned succ(0); succ < pmc->getNumSuccStates(state); succ++) {
	RationalFunction succProb = pmc->getSuccProb(state, succ);
	succProb /= sum;
	pmc->setSuccProb(state, succ, succProb);
      }
    }
  }
  
  void Controller::getParamsFromModel(prismparser::Model &model) {
    for (HashMap<string,CVC3::Expr>::const_iterator i = model.variables.begin();
         i != model.variables.end(); ++i) {
      if (model.isParameterVariable(i->second)) {
	RationalFunction::addSymbol(i->first);
      }
    }
  }
  
  void Controller::prepareSymbols(prismparser::Model &model) {
    getParamsFromModel(model);
    RationalFunction::start();
  }
  
  void Controller::createSimpleRegionScheduler
  (const Results &results, RegionScheduler &scheduler) {
    const unsigned numSymbols(RationalFunction::getNumSymbols());
    Box box;
    for (unsigned symNr(0); symNr < numSymbols; symNr++) {
      box.push_back(make_pair(mpq_class(0), mpq_class(1)));
    }
    ParametricScheduler paramSched;
    scheduler.push_back(boost::make_tuple(box, results, paramSched));
  }

  void Controller::unboundedUntil(RegionScheduler &scheduler) {
    Results result;
    pmc->computeBackTransitions();
    Eliminator eliminator;
    eliminator.setRewardAnalysis(isRewardAnalysis());
    eliminator.setPMC((GPMC &) *pmc);
    eliminator.setInitStates(initStates);
    eliminator.setTargetStates(targetStates);
    Eliminator::EliminationOrder eliminationOrder;
    const string eliminationOrderString(vm["elimination-order"].as<string>());
    if ("forward" == eliminationOrderString) {
      eliminationOrder = Eliminator::forward;
    } else if ("backward" == eliminationOrderString) {
      eliminationOrder = Eliminator::backward;
    } else if ("random" == eliminationOrderString) {
      eliminationOrder = Eliminator::random;
    } else {
      throw new runtime_error("Invalid elimination order");
    }
    eliminator.setEliminationOrder(eliminationOrder);
    eliminator.eliminate(result);

    createSimpleRegionScheduler(result, scheduler);
  }

  void Controller::boundedUntil(RegionScheduler &scheduler) {
    Results result;
    BoundedIterator iterator;
    iterator.setPMC(*pmc);
    iterator.setInitStates(initStates);
    iterator.setTargetStates(targetStates);
    iterator.setTimeBound(time);
    iterator.iterate(result);

    createSimpleRegionScheduler(result, scheduler);
  }
  
  /**
   * Executes the analysis of SparseMC.
   * The model and formula must have been loaded. Statespace must have been
   * explored, model type and analysis type etc. must have been set.
   */
  void Controller::execute(RegionScheduler& result) {
    if ((model_type == prismparser::CTMC)
        && (unboundedUntilAnalysis == analysisType)) {
      embed();
    }

    if (!vm.count("nolump")) {
      pmc->computeBackTransitions();
      Quotient quot;
      
      if ("strong" == vm["lump-method"].as<string>()) {
	quot.setBisim(Quotient::strong);
      } else if ("weak" == vm["lump-method"].as<string>()) {
	quot.setBisim(Quotient::weak);
      } else if (needsStrongBisimulation()) {
	quot.setBisim(Quotient::strong);
      } else {
	quot.setBisim(Quotient::weak);
      }
      PartRefOrder partRefOrder;
      if ("small-first" == vm["refine-order"].as<string>()) {
	partRefOrder = smallFirst;
      } else if ("big-first" == vm["refine-order"].as<string>()) {
	partRefOrder = bigFirst;
      } else if ("first-first" == vm["refine-order"].as<string>()) {
	partRefOrder = firstFirst;
	} else if ("last-first" == vm["refine-order"].as<string>()) {
	partRefOrder = lastFirst;
      } else {
	throw runtime_error("Unsupported refine order");
      }
      quot.setRewardAnalysis(isRewardAnalysis());
      quot.setPartRefOrder(partRefOrder);
      quot.setOldPMC(*pmc);
      quot.setOldInitStates(initStates);
      quot.setOldTargetStates(targetStates);
      quot.setOldStateRewards(stateRewards);
      PMC *newPMC = new GPMC();
      quot.setNewPMC(*newPMC);
      StateSet newInitStates;
      StateSet newTargetStates;
      RewardMap newStateRewards;
      quot.setNewInitStates(newInitStates);
      quot.setNewTargetStates(newTargetStates);
      quot.setNewStateRewards(newStateRewards);
      statistics->lumpTime.start();
      quot.quot();
      statistics->lumpTime.stop();
      delete pmc;
      pmc = newPMC;
      initStates.swap(newInitStates);
      targetStates.swap(newTargetStates);
      stateRewards.swap(newStateRewards);
      statistics->numStatesQuotient = pmc->getNumStates();
      statistics->numTransitionsQuotient = pmc->getNumTrans();
      if (0 != vm.count("lumped-dot")) {
	printDOT(vm["lumped-dot"].as<string>());
      }
    }
    
    RationalFunction::setCleanupMethod(RationalFunction::nocache);
    RationalFunction::removeUnusedSymbols();
    statistics->analysisTime.start();
    
    if (unboundedUntilAnalysis == analysisType) {
      unboundedUntil(result);
    } else if (boundedUntilAnalysis == analysisType) {
      boundedUntil(result);
    } else if (reachabilityRewardAnalysis == analysisType) {
      unboundedUntil(result);
    } else {
      throw runtime_error("Illegal analysis type");
    }

    statistics->analysisTime.stop();
  }
  
  void Controller::parse() {
    RationalFunction::setCleanupMethod(RationalFunction::never);
    if (0 == vm.count("low-level-input")) {
      PASSStateExplorer explorer(*this);
      explorer.explore();      
    } else {
      LowLevelStateExplorer explorer(*this);
      explorer.explore();
    }
  }

  PMC &Controller::getPMC() {
    return *pmc;
  }

  /**
   * Print statistics to file specified by program options.
   */
  void Controller::printStatistics() {
    if (0 != vm.count("statistics-file")) {
      statistics->totalTime.stop();
      statistics->print(vm["statistics-file"].as<std::string>());
    }
  }

  const StateSet &Controller::getInitStates() const {
    return initStates;
  }

  const StateSet &Controller::getTargetStates() const {
    return targetStates;
  }

  /**
   * Sets type of analysis to be done for model.
   *
   * @param type type of analysis to be done
   */
  void Controller::setAnalysisType(AnalysisType type) {
    analysisType = type;
  }
  /**
   * Usable to decide whether weak or strong analysis be used.
   *
   * @return true iff bounded time analysis
   */
  bool Controller::needsStrongBisimulation() const {
    return (reachabilityRewardAnalysis == analysisType)
      || (boundedUntilAnalysis == analysisType);
  }

  /**
   * Check whether analysis to do is reward analyis.
   *
   * @return true iff analysis is reward analysis
   */
  bool Controller::isRewardAnalysis() const {
    return (reachabilityRewardAnalysis == analysisType);
  }

  bool Controller::isDiscreteTime() const {
    return (prismparser::DTMC == model_type);
  }
}
