//==============================================================================
//	
//	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.search;

import java.util.HashMap;
import java.util.Set;

import jdd.JDD;
import heuristics.CollapseModelExplorer;
import heuristics.ECContainer;
import heuristics.HeuristicsSMGModelChecker;
import heuristics.decisiontree.DecisionTree;
import heuristics.decisiontree.DeltaStar;
import heuristics.decisiontree.PlayDT;
import heuristics.nextstate.HeuristicNextState;
import heuristics.update.StateUpdate;
import explicit.ModelExplorer;
import parser.State;
import prism.PrismException;

/**
 * The basic class for all heuristics. In the method compute() (called from HeuristicsSMGModelChecker) implements
 * the framework used for every heuristic.
 * 
 * The subclasses should be mostly interested in implementing three methods: heuristicStart, heuristicStep, heuristicStop
 * Where heuristicStart and heuristicStop are used to setup/cleanup before/after heuristic is run and heuristicStep
 * is used to implement the heuristic.
 * 
 * In case of heuristics that cannot follow the framework given in compute() the subclass may override this method. 
 * 
 */

public abstract class Heuristic {
	
	protected HeuristicsSMGModelChecker mc;
	protected ModelExplorer pme;
	protected State initialState;
	protected int bound = -1;
	protected HeuristicNextState nextState;
	protected StateUpdate stateUpdate;
	protected boolean verbose;
	protected boolean min = false;
	protected boolean collapseMECs = true;
	
	//Statistics
	protected int trialSteps = 0;
	protected int trials = 0;
	protected int reportEvery = 10000;
	protected long modelCheckingTime = 0;
	protected Set<State> nonDetStates;
	protected int nondettotal;
	
	public Heuristic(HeuristicsSMGModelChecker mc,StateUpdate su, ECContainer eCC, HeuristicNextState nextState, ModelExplorer pme, boolean min, boolean collapseMECs) throws PrismException{
		this.mc = mc;
		this.pme = pme;
		this.stateUpdate = su;
		this.nextState = nextState;
		initialState = pme.getDefaultInitialState();
		this.min = min;
		this.collapseMECs = collapseMECs;
	}
	
	public abstract void heuristicStep(State s) throws PrismException;
	
	public boolean isDone() throws PrismException {
		return isDone(initialState);
	}
	
	public boolean isDone(State s) throws PrismException {
		StateValue sv = stateUpdate.getQValue(s);
		if(sv != null) {
			double lowerBoundInitialState = sv.getLowerBound();
			double upperBoundInitialState = sv.getUpperBound();
			return stateUpdate.same(lowerBoundInitialState, upperBoundInitialState);
		}
		return false;
	}
	
	
	public void compute() throws PrismException{
		State initial = pme.getDefaultInitialState();
		double lowerBoundInitialState = 0;
		double upperBoundInitialState = 1;
		boolean done = false;
		
		stateUpdate.setQValue(initial, new StateValue(lowerBoundInitialState, upperBoundInitialState, StateValue.ACTION_UNDEF), 0);
		
		heuristicStart();
		
		while(!done) {
			State s = initial;
			heuristicStep(s);
			done = isDone();
		}
		
		heuristicStop();
		reportProgress(trials, trialSteps, true);
		
	}
	
	protected void heuristicStart() throws PrismException{
		mc.getLog().println("Solution method: " + getClass().getName().toString());
		mc.getLog().println("Using heuristic: " + nextState.getType().toString());
		modelCheckingTime = System.currentTimeMillis();
	}
	
	protected void heuristicStop() throws PrismException{
		long duration = System.currentTimeMillis() - modelCheckingTime;
		mc.getLog().println();
		mc.getLog().println("Heuristic model checking time in " + ((double)duration/1000)  + " secs.");
		mc.getLog().println();
	}
	
	public int getBound() {
		return bound;
	}
	
	public void setBound(int b) {
		this.bound = b;
	}
	
	public void setVerbose(boolean v) {
		this.verbose = v;
	}
	
	public boolean getVerbose() {
		return this.verbose;
	}
	
	public StateValue getInitialStateValue() {
		return stateUpdate.getQValue(initialState,0) == null ? new StateValue(-1, -1, StateValue.ACTION_UNDEF) : stateUpdate.getQValue(initialState,0);
	}
	
	public StateUpdate getStateUpdate() {
		return stateUpdate;
	}
	
	public double getUpper(State s, int a) throws PrismException {
		pme.queryState(s);
		return stateUpdate.getUpperBoundActionValue(s, a).getUpperBound();
	}
	
	protected void reportProgress(int trials, int trialSteps, boolean finished) throws PrismException{
		if(verbose) {
			double lowerBoundInitialState = stateUpdate.getQValue(initialState,0).getLowerBound();
			double upperBoundInitialState = stateUpdate.getQValue(initialState,0).getUpperBound();
			mc.getLog().println("Trials: " + trials);
			mc.getLog().println("Trial steps: " + trialSteps);
			mc.getLog().println("Trial steps avg: " + (double)trialSteps/(double)trials);
			mc.getLog().println("Explore: " + stateUpdate.getNumExplored());
			mc.getLog().println("Non-Det states: " + nonDetStates.size());
			mc.getLog().println("#choices per non det state: " + (double)nondettotal/nonDetStates.size());
			mc.getLog().println("Lower bound: " + lowerBoundInitialState);
			mc.getLog().println("Upper bound: " + upperBoundInitialState);
			//mc.getLog().println("All values: " + stateUpdate.getNumAllValues());
			if(finished) {
				mc.getLog().println("Reachable: " + stateUpdate.getNumReachable());
			}
			mc.getLog().flush();
		}
	}
}
