/*
 * 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 "Controller.h"
#include "Partition.h"
#include "Quotient.h"
#include "Refiner.h"
#include "StrongRefiner.h"
#include "WeakRefiner.h"

namespace parametric {
  
  using namespace std;
  using namespace Rational;

  void Quotient::setBisim(bisim_t _bisim) {
    bisim = _bisim;
  }
  
  void Quotient::setOldPMC(PMC &_oldPMC) {
    oldPMC = &_oldPMC;
  }

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

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

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

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

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

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

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

  void Quotient::setPartRefOrder(PartRefOrder _partRefOrder) {
    partRefOrder = _partRefOrder;
  }

  void Quotient::setRewardAnalysis(bool _rewardAnalysis) {
    rewardAnalysis = _rewardAnalysis;
  }

  QuotMap &Quotient::getQuotMap() {
    return refiner->getQuotMap();
  }

  Quotient::Quotient() {
    partition = NULL;
    refiner = NULL;
  }

  Quotient::~Quotient() {
    if (NULL != partition) {
      delete partition;
    }
    if (NULL != refiner) {
      delete refiner;
    }
  }

  Partition &Quotient::getPartition() {
    assert(NULL != partition);
    return *partition;
  }

  /**
   * Lump the Markov model.
   */
  void Quotient::quot() {
    if (weak == bisim) {
      refiner = new WeakRefiner();
    } else if (strong == bisim) {
      refiner = new StrongRefiner();
    } else {
      throw runtime_error("Unsupported bisimulation type");
    }
    refiner->setRewardAnalysis(rewardAnalysis);
    refiner->setOldPMC(*oldPMC);
    refiner->setOldInitStates(*oldInitStates);
    refiner->setOldStateRewards(*oldStateRewards);
    refiner->setOldTargetStates(*oldTargetStates);
    refiner->setNewPMC(*newPMC);
    refiner->setNewInitStates(*newInitStates);
    refiner->setNewStateRewards(*newStateRewards);
    refiner->setNewTargetStates(*newTargetStates);
    
    partition = new Partition(partRefOrder);
    partition->pmc = oldPMC;
    refiner->createInitialPartition(*partition);
    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;
      refiner->refineClass(p);
      partition->afterRefine();
      partition->erase(P_it);
    }
    
    refiner->createQuotient(*partition);
  }
}
