/*
 * 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)
 */

/**
 * TODOs:
 * - try out using HashMap-s instead of map-s
 */

#include <stdlib.h>
#include <stdbool.h>
#include <string.h>
#include <boost/graph/strong_components.hpp>
#include <boost/graph/depth_first_search.hpp>
#include "SparseMC.h"
#include "Partition.h"
#include "Quotient.h"
#include "Refiner.h"
#include "StrongRefiner.h"
#include "WeakRefiner.h"

namespace parametric {
  
  using namespace std;
  using namespace boost;
  using namespace Rational;
  
  util::Timer hashtime;
  util::Timer ringTime;
  util::Timer refineTime;
  util::Timer mayChangeTime;
  util::Timer nonSilentRefineTime;
  util::Timer silentRefineTime;
  
  template < typename Set > class dfs_non_div_visitor :
    public default_dfs_visitor {
  public:
    dfs_non_div_visitor(Set &_marking)
      : marking(_marking) {
    }
    template < typename Vertex, typename Graph >
    void discover_vertex(Vertex u, const Graph & g) const {
      marking.insert(u);
    }
    template < typename Vertex, typename Graph >
    void finish_vertex(Vertex u, const Graph & g) const {
      
    }
    
    Set &marking;
  };
  
  /**
   * Generate new quotient constructor object.
   *
   * @param mc Markov chain to be refined
   */
  Quotient::Quotient(SparseMC &__mc) : mc(__mc) {
    bisim = bisim_def;
  }
  
  /**
   * Quotien the Markov model.
   */
  void Quotient::quot() {
    mc.statistics.lumpTime.Start();
    
    quotSigref();
    
    mc.statistics.lumpTime.Stop();
    mc.statistics.numStatesQuotient = num_vertices(*mc.graph);
    mc.statistics.numTransitionsQuotient = num_edges(*mc.graph);
    if (0 != mc.vm.count("lumped-dot")) {
      mc.printDOT(mc.vm["lumped-dot"].as<string>());
    }
  }
  
  /**
   * Do signature-refinement based quotioning.
   */
  void Quotient::quotSigref() {
    auto_ptr<Refiner> refiner;
    if (bisim_def == bisim) {
      bisim = mc.needsStrongBisimulation() ? strong : weak;
    }
    if (weak == bisim) {
      refiner.reset(new WeakRefiner(*this));
    } else if (strong == bisim) {
      refiner.reset(new StrongRefiner(*this));
    } else {
      throw runtime_error("Unsupported bisimulation type");
    }
    
    Partition p1(mc);
    Partition *partition = &p1;  
    partition->graph = mc.graph;
    refiner->createInitialPartition(p1);
    refiner->setPartition(*partition);
    partition->remapAll();
    PartitionList &P = partition->P;
    for (PartitionList::iterator P_it = P.begin(); P_it != P.end(); P_it++) {
      partition->mayChange->push(P_it);
    }
    
    while (!partition->mayChange->empty()) {
      PartitionList::iterator P_it = partition->mayChange->top();
      partition->mayChange->pop();
      EqClass &p = *P_it;
      refineTime.Start();
      refiner->refineClass(p);
      partition->afterRefine();
      refineTime.Stop();
      partition->erase(P_it);
    }
    
    refiner->createQuotient(*partition);
  }
}
