//==============================================================================
//	
//	Copyright (c) 2013-
//	Authors:
//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM 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 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM 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 PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package explicit;

import java.math.BigDecimal;
import java.math.RoundingMode;
import java.util.*;
import java.util.Map.Entry;

import explicit.rewards.MCRewards;
import parser.State;
import parser.Values;
import prism.ModelType;
import prism.PrismException;
import strat.MDStrategy;

/**
* Explicit-state representation of a DTMC, constructed (implicitly)
* from an MDP and a memoryless deterministic (MD) adversary.
* This class is read-only: most of the data is pointers to other model info.
*/
public class DTMCFromMDPAndDTStrategy extends DTMCExplicit
{
	// Parent MDP
	protected MDP mdp;
	// MD strategy
	protected int[][] strat;

	protected List<Distribution> trans;
	
	/**
	 * Constructor: create from MDP and memoryless adversary.
	 */
	public DTMCFromMDPAndDTStrategy(MDP mdp, int[][] strat)
	{
		this.mdp = mdp;
		this.numStates = mdp.getNumStates();
		this.strat = strat;
		initialise(numStates);
	}

	@Override
	public void initialise(int numStates)
	{
		super.initialise(numStates);
		trans = new ArrayList<Distribution>(numStates);
		for (int i = 0; i < numStates; i++) {
			int[] desiredChoices = strat[i];
			if (desiredChoices.length == 1 && desiredChoices[0] == -2) {
				int numChoices = mdp.getNumChoices(i);
				desiredChoices = new int[numChoices];
				for (int j = 0; j < numChoices; j++) desiredChoices[j] = j;
			}
			Distribution distr = new Distribution();
			for (int j = 0; j < desiredChoices.length; j++) {
				int choice = desiredChoices[j];
				Iterator<Entry<Integer,Double>> k = null;
				try {
					k = mdp.getTransitionsIterator(i, choice);
				}
				catch(Exception e) {
					System.out.println("Problems for state: " + i + " choice: " + choice + " it should have: " + mdp.getNumChoices(i) + " choices");
					e.printStackTrace();
					System.exit(-1);
				}
				HashMap<Integer,BigDecimal> gatherProbs = new HashMap<Integer,BigDecimal>();
				while (k.hasNext()) {
					Entry<Integer,Double> n = k.next();
					BigDecimal soFar = gatherProbs.get(n.getKey());
					if (soFar == null) soFar = new BigDecimal(0.0);
					gatherProbs.put(n.getKey(), soFar.add(new BigDecimal(n.getValue())));
				}
				for (Integer state: gatherProbs.keySet()) { 
					distr.add(state, gatherProbs.get(state).divide(new BigDecimal(desiredChoices.length),20,RoundingMode.HALF_EVEN).doubleValue());
				}
			}
			trans.add(distr);
		}
	}
	
	public double getTraceProbability(ArrayList<State> trace) {
		List<State> states = mdp.getStatesList();
		double prob = 1.0;
		for (int j = 0; j < trace.size() - 1; j++) {
			State currentState = trace.get(j);
			int stateIndex = states.indexOf(currentState);
			int nextStateIndex = states.indexOf(trace.get(j+1));
			Iterator<Entry<Integer,Double>> i = getTransitionsIterator(stateIndex);
			while (i.hasNext()) {
				Entry<Integer,Double> e = i.next();
				if (e.getKey().equals(nextStateIndex)) {
					System.out.println("From " + prob + " to " + prob * e.getValue());
					prob = prob * e.getValue();
				}
			}
		}
		return prob;
	}
	
	@Override
	public void buildFromPrismExplicit(String filename) throws PrismException
	{
		throw new PrismException("Not supported");
	}

	// Accessors (for Model)

	public ModelType getModelType()
	{
		return ModelType.DTMC;
	}

	public int getNumStates()
	{
		return mdp.getNumStates();
	}

	public int getNumInitialStates()
	{
		return mdp.getNumInitialStates();
	}

	public Iterable<Integer> getInitialStates()
	{
		return mdp.getInitialStates();
	}

	public int getFirstInitialState()
	{
		return mdp.getFirstInitialState();
	}

	public boolean isInitialState(int i)
	{
		return mdp.isInitialState(i);
	}

	public boolean isDeadlockState(int i)
	{
		return mdp.isDeadlockState(i);
	}

	public List<State> getStatesList()
	{
		return mdp.getStatesList();
	}

	public Values getConstantValues()
	{
		return mdp.getConstantValues();
	}

	public int getNumTransitions()
	{
		int numTransitions = 0;
		for (int s = 0; s < numStates; s++)
			numTransitions += trans.get(s).size();
		return numTransitions;
	}

	public Iterator<Integer> getSuccessorsIterator(final int s)
	{
		throw new RuntimeException("Not implemented yet");
	}

	public boolean isSuccessor(int s1, int s2)
	{
		throw new RuntimeException("Not implemented yet");
	}

	public boolean allSuccessorsInSet(int s, BitSet set)
	{
		throw new RuntimeException("Not implemented yet");
	}

	public boolean someSuccessorsInSet(int s, BitSet set)
	{
		throw new RuntimeException("Not implemented yet");
	}

	public int getNumChoices(int s)
	{
		// Always 1 for a DTMC
		return 1;
	}

	public void findDeadlocks(boolean fix) throws PrismException
	{
		// No deadlocks by definition
	}

	public void checkForDeadlocks() throws PrismException
	{
		// No deadlocks by definition
	}

	public void checkForDeadlocks(BitSet except) throws PrismException
	{
		// No deadlocks by definition
	}

	@Override
	public String infoString()
	{
		return mdp.infoString() + " + " + "???"; // TODO
	}

	@Override
	public String infoStringTable()
	{
		return mdp.infoString() + " + " + "???\n"; // TODO
	}

	// Accessors (for DTMC)

	public int getNumTransitions(int s)
	{
		return trans.get(s).size();
	}

	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s)
	{
		return trans.get(s).iterator();
	}
	
	@Override
	public void prob0step(BitSet subset, BitSet u, BitSet result)
	{
		int i;
		Distribution distr;
		for (i = 0; i < numStates; i++) {
			if (subset.get(i)) {
				distr = trans.get(i);
				result.set(i, distr.containsOneOf(u));
			}
		}
	}

	@Override
	public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
	{
		int i;
		Distribution distr;
		for (i = 0; i < numStates; i++) {
			if (subset.get(i)) {
				distr = trans.get(i);
				result.set(i, distr.containsOneOf(v) && distr.isSubsetOf(u));
			}
		}
	}

	@Override
	public double mvMultSingle(int s, double vect[])
	{
		int k;
		double d, prob;
		Distribution distr;

		distr = trans.get(s);
		d = 0.0;
		for (Map.Entry<Integer, Double> e : distr) {
			k = (Integer) e.getKey();
			prob = (Double) e.getValue();
			d += prob * vect[k];
		}

		return d;
	}

	@Override
	public double mvMultJacSingle(int s, double vect[])
	{
		int k;
		double diag, d, prob;
		Distribution distr;

		distr = trans.get(s);
		diag = 1.0;
		d = 0.0;
		for (Map.Entry<Integer, Double> e : distr) {
			k = (Integer) e.getKey();
			prob = (Double) e.getValue();
			if (k != s) {
				d += prob * vect[k];
			} else {
				diag -= prob;
			}
		}
		if (diag > 0)
			d /= diag;

		return d;
	}

	@Override
	public double mvMultRewSingle(int s, double vect[], MCRewards mcRewards)
	{
		throw new RuntimeException("Not implemented yet");
		//return mdp.mvMultRewSingle(s, adv[s], vect);
	}

	@Override
	public void vmMult(double vect[], double result[])
	{
		throw new RuntimeException("Not implemented yet");
	}

	@Override
	public String toString()
	{
		throw new RuntimeException("Not implemented yet");
	}

	@Override
	public boolean equals(Object o)
	{
		throw new RuntimeException("Not implemented yet");
	}
}
