/*
 * 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 Ernst Moritz Hahn (emh@cs.uni-sb.de)
 */

#ifndef SPARSE_MC_H
#define SPARSE_MC_H

#include <vector>

#include <boost/graph/graph_traits.hpp>
#include <boost/graph/adjacency_list.hpp>
#include <boost/graph/graph_traits.hpp>
#include <boost/program_options.hpp>

#include <fstream>
#include "lang/Model.h"

#include "TransProp.h"
#include "Statistics.h"
#include "rationalFunction/RationalFunction.h"
#include "rationalFunction/Base.h"
#include "rationalFunction/CVC3Converter.h"

namespace parametric {
  
  typedef boost::adjacency_list<boost::listS, boost::listS,
    boost::bidirectionalS, boost::no_property, TransProp> Graph;
  
  typedef boost::graph_traits<Graph>::vertex_descriptor vertex_descriptor;
  typedef boost::graph_traits<Graph>::edge_descriptor edge_descriptor;
  
  typedef boost::graph_traits<Graph>::out_edge_iterator out_edge_iterator;
  typedef boost::graph_traits<Graph>::in_edge_iterator in_edge_iterator;
  typedef boost::graph_traits<Graph>::vertex_iterator vertex_iterator;
  typedef boost::graph_traits<Graph>::edge_iterator edge_iterator;
  typedef std::set<vertex_descriptor> StateSet;
  typedef std::list<vertex_descriptor> StateList;
  typedef std::vector<vertex_descriptor> StateVector;
  typedef std::map<vertex_descriptor, Rational::RationalFunction> RewardMap;
  typedef std::map<vertex_descriptor, Rational::RationalFunction> StateMap;
  
  class PASSStateExplorer;
  class Quotient;
  class Refiner;
  class WeakRefiner;
  class StrongRefiner;
  class StateProp;
  class Gauss;
  class SteadyState;
  
  class SparseMC {
    /* too many friends, something like package visibility would be
     * more appropriate here.
     */
    friend class PASSStateExplorer;
    friend class Quotient;
    friend class Refiner;
    friend class WeakRefiner;
    friend class StrongRefiner;
    friend class StateProp;
    friend class Gauss;
    friend class SteadyState;
    friend class MayChange;
  public:
    /**
     * Type for specifying the kind of analysis to be done
     */
    enum AnalysisType {
      unboundedUntilAnalysis,
      boundedUntilAnalysis,
      reachabilityRewardAnalysis,
    };
    
    /**
     * Sets type of analysis to be done for model.
     *
     * @param type type of analysis to be done
     */
    inline void setAnalysisType(AnalysisType type) {
      analysisType = type;
    }
    /**
     * Usable to decide whether weak or strong analysis be used.
     *
     * @return true iff bounded time analysis
     */
    inline bool needsStrongBisimulation() const {
      return (reachabilityRewardAnalysis == analysisType);
    }
    /**
     * Check whether analysis to do is reward analyis.
     *
     * @return true iff analysis is reward analysis
     */
    inline bool isRewardAnalysis() const {
      return (reachabilityRewardAnalysis == analysisType);
    }
    inline bool isDiscreteTime() const {
      return (lang::DTMC == model_type) || (lang::MDP == model_type);
    }
    void transToStateRewards();
    void stateToTransRewards();
    SparseMC(boost::program_options::variables_map &);
    ~SparseMC();
    void execute(std::vector<Rational::RationalFunction> &);
    void embed();
    void unboundedUntil(std::vector<Rational::RationalFunction> &);
    void boundedUntil(std::vector<Rational::RationalFunction> &);
    void print();
    void printDOT(const std::string &) const;
    void printDOT(std::ostream &) const;
    void printDOT() const;
    void printResult(const std::vector<Rational::RationalFunction> &, const std::string &) const;
    void printResult(const std::vector<Rational::RationalFunction> &, std::ostream &) const;
    void printResult(const std::vector<Rational::RationalFunction> &) const;
    std::string toMaple();
    void parse();
    inline Graph &getGraph() {
      return *graph;
    }
    /**
     * Print statistics to file specified by program options.
     */
    inline void printStatistics() {
      if (0 != vm.count("statistics-file")) {
        statistics.totalTime.Stop();
        statistics.print(vm["statistics-file"].as<std::string>());
      }
    }
    inline const StateSet &getInitStates() const {
      return initStates;
    }
    inline const StateSet &getTargetStates() const {
      return targetStates;
    }
    
  private:
    void makeTargetStatesAbsorbing();
    void getParamsFromModel();
    void prepareSymbols();
    void prepareInitialStatesForUnbounded();
    void bisimCreateBlocks
      (std::list<std::set<vertex_descriptor> > &,
       std::map<vertex_descriptor,
       std::list<std::set<vertex_descriptor> >::iterator> &,
       std::vector<std::set<vertex_descriptor> > &);
    void bisim();
    void bisimSplit
      (const std::set<vertex_descriptor> &,
       std::list<std::set<vertex_descriptor> > &,
       std::map<vertex_descriptor,
       std::list<std::set<vertex_descriptor> >::iterator> &,
       std::vector<std::set<vertex_descriptor> > &);
    void weaksimCreateBlocks
      (std::list<std::set<vertex_descriptor> > &,
       std::map<vertex_descriptor,
       std::list<std::set<vertex_descriptor> >::iterator> &);
    bool weakIsSilent
      (vertex_descriptor, std::set<vertex_descriptor> &);
    Rational::RationalFunction weakP_Chi
      (vertex_descriptor, std::set<vertex_descriptor> &,
       std::set<vertex_descriptor> &);
    std::list<std::set<vertex_descriptor> >::iterator
      weakFindSplitter
      (std::list<std::set<vertex_descriptor> > &);
    void weakRefine
      (std::list<std::set<vertex_descriptor> > &,
       std::map<vertex_descriptor,
       std::list<std::set<vertex_descriptor> >::iterator> &,
       std::set<vertex_descriptor> &,
       std::list<std::list<std::set<vertex_descriptor> >::iterator > &);
    void weakSilentSplit
      (std::set<vertex_descriptor> &,
       std::map<vertex_descriptor,Rational::RationalFunction> &);
    void weakCreateNewPartitions
      (std::set<vertex_descriptor> &,
       std::map<vertex_descriptor,Rational::RationalFunction> &,
       std::list<std::set<vertex_descriptor> > &,
       std::map<vertex_descriptor,
       std::list<std::set<vertex_descriptor> >::iterator> &,
       std::list<std::list<std::set<vertex_descriptor> >::iterator > &);
    void weakBuildNewGraph
      (std::list<std::set<vertex_descriptor> > &,
       std::map<vertex_descriptor,
       std::list<std::set<vertex_descriptor> >::iterator> &);
    void weakBisim();
    
    Statistics statistics;
    Rational::CVC3Converter cvc3Converter;
    AnalysisType analysisType;
    double time;
    lang::ModelType model_type;
    boost::program_options::variables_map &vm;
    std::vector<std::string> nondetParams;
    Graph *graph;
    StateSet initStates;
    StateSet targetStates;
    RewardMap stateRewards;
  };
}

#endif
