/*
 * 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 <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() {
  }
  
  Refiner::~Refiner() {
  }
  
  void Refiner::setPartition(Partition &__partition) {
    partition = &__partition;
  }

  void Refiner::setRewardAnalysis(bool _isRewardAnalysis) {
    isRewardAnalysis = _isRewardAnalysis;
  }

  void Refiner::setOldPMC(PMC &_oldPMC) {
    oldPMC = &_oldPMC;
  }

  void Refiner::setOldInitStates(StateSet &_oldInitStates) {
    oldInitStates = &_oldInitStates;
  }

  void Refiner::setOldTargetStates(StateSet &_oldTargetStates) {
    oldTargetStates = &_oldTargetStates;
  }

  void Refiner::setOldStateRewards(RewardMap &_oldStateRewards) {
    oldStateRewards = &_oldStateRewards;
  }

  void Refiner::setNewPMC(PMC &_newPMC) {
    newPMC = &_newPMC;
  }

  void Refiner::setNewInitStates(StateSet &_newInitStates) {
    newInitStates = &_newInitStates;
  }

  void Refiner::setNewTargetStates(StateSet &_newTargetStates) {
    newTargetStates = &_newTargetStates;
  }

  void Refiner::setNewStateRewards(RewardMap &_newStateRewards) {
    newStateRewards = &_newStateRewards;
  }

  QuotMap &Refiner::getQuotMap() {
    return quotMap;
  }

  /**
   * 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<PMM::state> 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 (!isRewardAnalysis) {
      list<StateSet>::iterator inormal = P.insert(P.begin(), s);
      for (PMM::state u(0); u < oldPMC->getNumStates(); u++) {
        if (oldTargetStates->find(u) != oldTargetStates->end()) {
          itarget->insert(u);
        } else {
          inormal->insert(u);
        }
      }
    } else { // reward mode
      vector<RationalFunction> values;
      for (PMM::state u(0); u < oldPMC->getNumStates(); u++) {
        if (oldTargetStates->find(u) != oldTargetStates->end()) {
          itarget->insert(u);
        } else {
          const RationalFunction reward((*oldStateRewards)[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);
        }
      }
    }
  }
}

