//==============================================================================
//	
//	Copyright (c) 2013-
//	Authors:
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
//	* Mateusz Ujma <mateusz.ujma@cs.ox.ac.uk> (University of 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 heuristics.update;

import java.util.ArrayList;
import java.util.List;
import java.util.Random;

import heuristics.search.StateValue;
import explicit.ModelExplorer;
import explicit.SMG;
import parser.State;
import prism.PrismException;

/*
 * StateUpdateSTPG is a subclass of the StateUpdate class. It implements a rather technical procedure
 * to update the state value in a case of a STPG. We follow a standard procedures known for SMG i.e.
 * we compute max/min values (for diamond/box states in case of Pmax) and return action that return 
 * such values. Please note that in the case when few such actions are available we randomise with 
 * uniform probability.
 * 
 */

public class StateUpdateSTPG extends StateUpdate{
	
	public StateUpdateSTPG(ModelExplorer me, StateValueContainer container, int bound, boolean min, double epsilon, boolean absolute) throws PrismException {
		super(me, container, bound, min, epsilon, absolute);
	}

	public int update(State s, int depth) throws PrismException{
		if(isTarget(s) || isZero(s) || isOnlySelfLoop(s)) return -1;
		
		int bestAction = getBestAction(s, depth);
		setQValue(s,
				new StateValue(getLowerBoundActionValue(s, bestAction, depth+1).getLowerBound(), 
							   getUpperBoundActionValue(s, bestAction, depth+1).getUpperBound(), bestAction), depth);
		
		
		return bestAction;
	}
	
	public int update(State s) throws PrismException{
		if(isTarget(s) || isZero(s) || isOnlySelfLoop(s)) return -1;
		
		int bestAction = getBestAction(s);
		setQValue(s,
				new StateValue(getLowerBoundActionValue(s, bestAction).getLowerBound(), 
							   getUpperBoundActionValue(s, bestAction).getUpperBound(), bestAction));
		if (getQValue(s).getAction() != bestAction) {
			System.out.println("StateValueContainer inconsistent");
		}
//		else System.out.println("consistent");
		return bestAction;
	}
	
	public int getBestAction(State s) throws PrismException{
		return getBestAction(s, NO_BOUND);
	}
	
	public int getBestAction(State s, int depth) throws PrismException{
		
		pme.queryState(s);
		int choices = pme.getNumChoices();
//		System.out.println("choices for " +s + " : " + choices);
		StateValue lowerBound_q_s[] = new StateValue[choices];
		StateValue upperBound_q_s[] = new StateValue[choices];
		double lowerBound = 0;
		double upperBound = 0;
		
		if((min && getPlayer(s) == SMG.PLAYER_1) || (!min && getPlayer(s) == SMG.PLAYER_2)) {
			lowerBound = Double.MAX_VALUE;
			upperBound = Double.MAX_VALUE;
		} 
		if((min && getPlayer(s) == SMG.PLAYER_2) || (!min && getPlayer(s) == SMG.PLAYER_1)) {
			lowerBound = -1;
			upperBound = -1;
		} 
		
		int bestAction = 0;
		for(int i=0;i<choices;i++) {
			pme.queryState(s);
			if((min && getPlayer(s) == SMG.PLAYER_1) || (!min && getPlayer(s) == SMG.PLAYER_2)) {
				if(depth == NO_BOUND) {
					lowerBound_q_s[i] = getLowerBoundActionValue(s, i);
					upperBound_q_s[i] = getUpperBoundActionValue(s, i);	
				} else {
					lowerBound_q_s[i] = getLowerBoundActionValue(s, i, depth+1);
					upperBound_q_s[i] = getUpperBoundActionValue(s, i, depth+1);
				}
				if(lowerBound_q_s[i].getLowerBound() < lowerBound) {
					bestAction = i;
					lowerBound = lowerBound_q_s[i].getLowerBound();
					upperBound = upperBound_q_s[i].getUpperBound();
				}
			} 
			if((min && getPlayer(s) == SMG.PLAYER_2) || (!min && getPlayer(s) == SMG.PLAYER_1)){
				if(depth == NO_BOUND) {
					lowerBound_q_s[i] = getLowerBoundActionValue(s, i);
					upperBound_q_s[i] = getUpperBoundActionValue(s, i);
				} else {
					lowerBound_q_s[i] = getLowerBoundActionValue(s, i, depth+1);
					upperBound_q_s[i] = getUpperBoundActionValue(s, i, depth+1);
				}
				if(upperBound_q_s[i].getUpperBound() > upperBound) {
					bestAction = i;
					lowerBound = lowerBound_q_s[i].getLowerBound();
					upperBound = upperBound_q_s[i].getUpperBound();
				}
			}
		}
		
		List<Integer> same = new ArrayList<Integer>();
		
		for(int i=0;i<choices;i++) {
			pme.queryState(s);
			if((min && getPlayer(s) == SMG.PLAYER_1) || (!min && getPlayer(s) == SMG.PLAYER_2)) {
				if(depth == NO_BOUND) {
					lowerBound_q_s[i] = getLowerBoundActionValue(s, i);
					upperBound_q_s[i] = getUpperBoundActionValue(s, i);	
				} else {
					lowerBound_q_s[i] = getLowerBoundActionValue(s, i, depth+1);
					upperBound_q_s[i] = getUpperBoundActionValue(s, i, depth+1);
				}
				if(same(lowerBound_q_s[i].getLowerBound(),lowerBound)) {
					same.add(i);
				}
			} 
			if((min && getPlayer(s) == SMG.PLAYER_2) || (!min && getPlayer(s) == SMG.PLAYER_1)){
				if(depth == NO_BOUND) {
					lowerBound_q_s[i] = getLowerBoundActionValue(s, i);
					upperBound_q_s[i] = getUpperBoundActionValue(s, i);
				} else {
					lowerBound_q_s[i] = getLowerBoundActionValue(s, i, depth+1);
					upperBound_q_s[i] = getUpperBoundActionValue(s, i, depth+1);
				}
				if(same(upperBound_q_s[i].getUpperBound(),upperBound)) {
					same.add(i);
				}
			}
		}
		
		Random r = new Random();
		if(same.size() > 0) {
			bestAction = same.get(r.nextInt(same.size()));
		}
		
		return bestAction;
	}
}
