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

#include <set>

#include "Quotient.h"
#include "Refiner.h"

namespace parametric {
  
  using namespace std;
  using namespace Rational;
  
  /**
   * Initializes the refiner.
   *
   * @param _quot quotient to use
   */
  Refiner::Refiner(Quotient &_quot)
    : quot(_quot), mc(quot.getSparseMC()), graph(mc.getGraph()) {
  }
  
  Refiner::~Refiner() {
  }
  
  /**
   * Creates default initial partition.
   * Notice: This may not be enough for some equivalence classes as an
   * initial partition, for example for weak bisimulation one must split
   * off divergent states. This means you may have to extend this method
   * for some equivalence classes!
   */
  void Refiner::createInitialPartition(Partition &partition) {
    PartitionList &P = partition.P;
    set<vertex_descriptor> s;
    list<StateSet>::iterator itarget =
      P.insert(P.begin(), s);
    vector<list<StateSet>::iterator> rewardBlocks;
    
    /*
     * Non-reward mode: place all target states in one block and the other ones
     * in another
     * Reward mode: place all states which are target states in one partition.
     * Place all non-target states with same reward in one partition.
     */
    if (!mc.isRewardAnalysis()) {
      list<StateSet>::iterator inormal = P.insert(P.begin(), s);
      pair<vertex_iterator, vertex_iterator> vp;
      for (vp = vertices(graph); vp.first != vp.second; ++vp.first) {
        vertex_descriptor u =  *vp.first;
        if (mc.targetStates.find(u) != mc.targetStates.end()) {
          itarget->insert(u);
        } else {
          inormal->insert(u);
        }
      }
    } else { // reward mode
      vector<RationalFunction> values;
      pair<vertex_iterator, vertex_iterator> vp;
      for (vp = vertices(graph); vp.first != vp.second; ++vp.first) {
        vertex_descriptor u =  *vp.first;
        if (mc.targetStates.find(u) != mc.targetStates.end()) {
          itarget->insert(u);
        } else {
          const RationalFunction reward(mc.stateRewards[u]);
          unsigned valNr;
          for (valNr = 0; valNr < values.size(); valNr++) {
            if (values[valNr] == reward) {
              break;
            }
          }
          if (valNr == values.size()) {
            values.push_back(reward);
            list<StateSet>::iterator ireward(P.insert(P.begin(), s));
          rewardBlocks.push_back(ireward);
          }
          rewardBlocks[valNr]->insert(u);
        }
      }
    }
  }
}

