//==============================================================================
//	
//	Copyright (c) 2013-
//	Authors:
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
//	* Ernst Moritz Hahn <emhahn@cs.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;

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

import jdd.DebugJDD;
import jdd.JDD;
import heuristics.nextstate.HeuristicNextState;
import heuristics.nextstate.HeuristicNextStateFactory;
import heuristics.nextstate.HeuristicNextStateFactory.NextState;
import heuristics.search.Heuristic;
import heuristics.search.HeuristicFactory;
import heuristics.search.HeuristicFactory.HeuristicType;
import heuristics.update.StateUpdate;
import heuristics.update.StateUpdateFactory;
import heuristics.update.StateValueContainer;
import heuristics.update.StateValueContainerMTBDD;
import heuristics.update.StateValueContainerMap;
import explicit.CachedModelExplorer;
import explicit.ModelExplorer;
import explicit.SMG;
import explicit.ProbModelChecker.TermCrit;
import parser.Values;
import parser.ast.Expression;
import parser.ast.ExpressionPATL;
import parser.ast.ExpressionProb;
import parser.ast.ExpressionTemporal;
import parser.ast.LabelList;
import parser.ast.ModulesFile;
import parser.ast.Player;
import parser.ast.PropertiesFile;
import parser.ast.Property;
import parser.ast.RelOp;
import prism.PrismComponent;
import prism.PrismException;
import prism.PrismSettings;
import prism.Result;
import simulator.PrismModelExplorer;
import simulator.SimulatorEngine;

/**
 * SMG model checker based on heuristic methods.
 */
abstract public class HeuristicsSMGModelChecker extends PrismComponent
{
	// Model file
	private ModulesFile modulesFile;
	// Properties file
	private PropertiesFile propertiesFile;
	private Property property;
	// Simulator engine
	private SimulatorEngine engine;
	// Constants from model
	private Values constantValues;
	// Labels from the model
	private LabelList labelListModel;
	// Labels from the property file
	private LabelList labelListProp;
	//Heuristic name
	private String heuristicName;
	//Next state type
	private String nextStateType;
	//Stopping criterion
	private double termCritParam = 1e-6;
//	protected TermCrit termCrit = TermCrit.ABSOLUTE;
	protected int termCrit = 1;
	private boolean verbose;
	private ExpressionTemporal currentExpression;
	private boolean collapseMECs;
	private boolean heuristicSymbolicContainers;
	
	private ECContainer eCC;
	private StateValueContainer container;
	private VarInfo varInfo;
	
	private ModelExplorer modelExplorer;
	private StateUpdate stateUpdate;
	
	private Heuristic h;
	
	/**
	 * Constructor.
	 */
	public HeuristicsSMGModelChecker(PrismComponent parent, ModulesFile modulesFile, PropertiesFile propertiesFile, Property property, SimulatorEngine engine, String heuristicName, String nextStateName, boolean verbose, boolean collapseMECs, boolean heuristicSymbolicContainers) throws PrismException
	{
		super(parent);
		this.modulesFile = modulesFile;
		this.propertiesFile = propertiesFile;
		this.property = property;
		this.engine = engine;

		// Get combined constant values from model/properties
		constantValues = new Values();
		constantValues.addValues(modulesFile.getConstantValues());
		if (propertiesFile != null)
			constantValues.addValues(propertiesFile.getConstantValues());
		this.labelListModel = modulesFile.getLabelList();
		this.labelListProp = propertiesFile.getLabelList();
		this.heuristicName = heuristicName;
		this.nextStateType = nextStateName;
		this.termCrit = settings.getChoice(PrismSettings.PRISM_TERM_CRIT);
		this.termCritParam = settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM);
		this.verbose = verbose;
		this.collapseMECs = collapseMECs;
		varInfo = new VarInfo(modulesFile);
		if (heuristicSymbolicContainers) {
			System.out.println("Using symbolic containers");
			eCC = new ECContainerMTBDD(varInfo);
//			eCC = new ECContainerMap();
			container = new StateValueContainerMTBDD(varInfo);
//			container = new StateValueContainerMap();
		}
		else {
			System.out.println("Using explicit containers");
			eCC = new ECContainerMap();
			container = new StateValueContainerMap();
		}
	}
	
	public Heuristic getHeuristic() {
		return h;
	}
	
	public ModulesFile getModulesFile() {
		return modulesFile;
	}
	
	public PropertiesFile getPropertiesFile() {
		return propertiesFile;
	}
	
	public Property getProperty() {
	  return property;
	}
	
	public SimulatorEngine getEngine() {
		return engine;
	}
	
	public ExpressionTemporal getExpression() {
		return currentExpression;
	}

	public ModelExplorer getModelExplorer() {
		return modelExplorer;
	}
	
	public StateUpdate getStateUpdate() {
		return stateUpdate;
	}
	/**
	 * Model check a property.
	 */
	public Result check(Expression expr) throws PrismException
	{
		Result res;
		String resultString;
		long timer;

		// Starting model checking
		timer = System.currentTimeMillis();

		// Do model checking
		res = checkExpression(expr);

		// Model checking complete
		timer = System.currentTimeMillis() - timer;
		mainLog.println("\nModel checking completed in " + (timer / 1000.0) + " secs.");

		// Print result to log
		resultString = "Result";
		if (!("Result".equals(expr.getResultName())))
			resultString += " (" + expr.getResultName().toLowerCase() + ")";
		resultString += ": " + res;
		mainLog.print("\n" + resultString + "\n");

		// Return result
		return res;
	}
	
	protected double getTermCritParam() {
		return termCritParam;
	}
	
	protected int getTermCrit() {
		return termCrit;
	}
	
	abstract protected ModelExplorer createModelExplorer(SimulatorEngine engine, ModulesFile modulesFile, ECContainer eCC) throws PrismException;
	
	/**
	 * Model check an expression (used recursively).
	 */
	
	private ExpressionPATL lastExprRPATL;
	
	private Result checkExpression(Expression expr) throws PrismException
	{
		// Current range of supported properties is quite limited...
		if(expr instanceof ExpressionPATL) {
			ExpressionPATL exprRPATL = (ExpressionPATL)expr;
			lastExprRPATL = exprRPATL;
			if(exprRPATL.getExpressionType() == ExpressionPATL.PRB) {
				return checkExpressionProb((ExpressionProb) exprRPATL.getExpressionProb());
			}
			//else if (expr instanceof ExpressionReward)
				//res = checkExpressionReward((ExpressionReward) expr);
		}
		if(expr instanceof ExpressionProb) {
			ExpressionProb exprProb = (ExpressionProb)expr;
			return checkExpressionProb((ExpressionProb) exprProb);
			//else if (expr instanceof ExpressionReward)
				//res = checkExpressionReward((ExpressionReward) expr);
		}
		throw new PrismException("Only P queries are supported by heuristics" + expr.getClass());
	}

	/**
	 * Model check a P operator, this is the only supported query by the heuristics.
	 */
	private Result checkExpressionProb(ExpressionProb expr) throws PrismException
	{
		boolean min = false;
		// Check whether P=? (only case allowed)
		if (expr.getProb() != null) {
			throw new PrismException("Only P=? properties are supported");
		}

		if (!(expr.getExpression() instanceof ExpressionTemporal)) {
			throw new PrismException("Heuristic model checking currently only supports simple path operators");
		}
		ExpressionProb exprProb = (ExpressionProb)expr;
		if(exprProb.getRelOp() == RelOp.MIN) {
			min = true;
		}
		
		ExpressionTemporal exprTemp = (ExpressionTemporal) expr.getExpression();
		currentExpression = exprTemp;
		if (!exprTemp.isSimplePathFormula()) {
			throw new PrismException("Heuristic model checking currently only supports simple until operators");
		}

		int bound = StateUpdate.NO_BOUND;
		
		if(exprTemp.hasBounds()) {
			bound = exprTemp.getUpperBound().evaluateInt(this.propertiesFile.getConstantValues());
			if (exprTemp.upperBoundIsStrict())
				bound--;
			if (bound < 0) {
				String boundS = exprTemp.upperBoundIsStrict() ? "<" + (bound + 1) : "<=" + bound;
				throw new PrismException("Invalid bound " + boundS + " in bounded until formula");
			}
		}
		
		modelExplorer = createModelExplorer(engine,modulesFile,eCC);
		stateUpdate = StateUpdateFactory.getStateUpdate(modulesFile.getModelType(), modelExplorer, container, bound, min, termCritParam, termCrit == 1);
		stateUpdate.setConstantValues(constantValues);
		if(lastExprRPATL != null) {
			int numPlayer = modulesFile.getNumPlayers();
			Set<Integer> playersInCoalition = new HashSet<Integer>();
			for(int i=0;i<numPlayer;i++) {
				Player player = modulesFile.getPlayer(i);
				if(lastExprRPATL.getCoalition().contains(player.getName())) {
					// 0-indexed to 1-indexed
					playersInCoalition.add(i+1);
				}
			}
			stateUpdate.setCoalition(playersInCoalition);
		} else {
		    //In this case we work on a MDP
		    Set<Integer> coalition = new HashSet<Integer>();
		    coalition.add(SMG.PLAYER_1);
		    stateUpdate.setCoalition(coalition);
		}
		
		HeuristicNextState nextState = HeuristicNextStateFactory.getHeuristicNextState(NextState.forName(nextStateType), modelExplorer, stateUpdate);
		
		h = HeuristicFactory.createHeuristic(HeuristicType.forName(heuristicName, bound != StateUpdate.NO_BOUND),this, stateUpdate, eCC, nextState, modelExplorer, min, collapseMECs);
		
//		System.out.println("creating " + h + " for hN: " + heuristicName);
		
		h.setBound(bound);
		h.setVerbose(verbose);

		Expression op1 = exprTemp.getOperand1();
		if (op1 == null) {
			op1 = Expression.True();
		}
		Expression op2 = exprTemp.getOperand2();
		op1 = (Expression) op1.expandPropRefsAndLabels(propertiesFile, labelListModel);
		op1 = (Expression) op1.expandPropRefsAndLabels(propertiesFile, labelListProp);
		op2 = (Expression) op2.expandPropRefsAndLabels(propertiesFile, labelListModel);
		op2 = (Expression) op2.expandPropRefsAndLabels(propertiesFile, labelListProp);
		int operator = exprTemp.getOperator();

		Expression target = null;
		switch (operator) {
		case ExpressionTemporal.P_F:
			target = op2;
			break;
		case ExpressionTemporal.P_U:
		case ExpressionTemporal.P_G:
		case ExpressionTemporal.P_W:
		case ExpressionTemporal.P_R:
		default:
			throw new PrismException("Operator currently not supported");
		}
		stateUpdate.setTarget(target);
		
		try {
			h.compute();
		}
		finally {
//			((ECContainerMTBDD)eCC).printAllInserted();
		}
//		varInfo.printRefCounts();
//		
//		container.derefAll();
//		eCC.derefAll();
		varInfo.derefAll();
//		varInfo.derefAll();
		stateUpdate.getNumReachable();
		DebugJDD.printNonZeroTraces();
		
		
//		DebugJDD.printNegativeTraces();
		
//		System.out.println(DebugJDD.localCounters);
		
		return new Result(new Double(h.getInitialStateValue().getLowerBound()));
	}

}
