/*
 * 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 "PMC.h"
#include "Controller.h"
#include "BoundedIterator.h"

namespace parametric {  
  using namespace std;
  using namespace boost;
  using namespace Rational;

  void BoundedIterator::setPMC(PMC &pmc__) {
    pmc = &pmc__;
  }

  void BoundedIterator::setInitStates(StateSet &initStates__) {
    initStates = &initStates__;
  }

  void BoundedIterator::setTargetStates(StateSet &targetStates__) {
    targetStates = &targetStates__;
  }

  void BoundedIterator::setTimeBound(double bound) {
    timeBound = (unsigned) bound;
  }

  void BoundedIterator::multiply
  (StateMap &probs, StateMap &probsPrimed) {
    for (PMM::state state(0); state < pmc->getNumStates(); state++) {
      if (targetStates->end() != targetStates->find(state)) {
	probsPrimed[state] = 1;
      } else {
	probsPrimed[state] = 0;
	for (unsigned succ(0); succ < pmc->getNumSuccStates(state); succ++) {
	  PMM::state succState = pmc->getSuccState(state, succ);
	  RationalFunction succProb = pmc->getSuccProb(state, succ);
	  probsPrimed[state] += succProb * probs[succState];
	}
      }
    }
  }

  void BoundedIterator::iterate(Results &result) {
    StateMap probs;
    StateMap probsPrimed;
    
    for (PMM::state state(0); state < pmc->getNumStates(); state++) {
      probs[state] = (targetStates->end() != targetStates->find(state)) ? 1 : 0;
      probsPrimed[state] = 0;
    }

    for (unsigned time(0); time < timeBound; time++) {
      multiply(probs, probsPrimed);
      probs.swap(probsPrimed);
    }

    for (PMM::state state(0); state < pmc->getNumStates(); state++) {
      if (initStates->find(state) != initStates->end()) {
        result.insert(make_pair(state, probs[state]));
      }
    }
  }
}
