//==============================================================================
//	
//	Copyright (c) 2002-
//	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 prism;

import java.util.*;

import jdd.*;
import odd.*;
import parser.State;
import parser.Values;
import parser.VarList;
import parser.type.*;

/**
 * Stores a list of states as a BDD (or as a 0-1 MTBDD).
 */
public class StateListMTBDD implements StateList
{
	// States list, as a (0-1) MTBDD
	protected JDDNode states;
	
	// Info needed from model
	protected JDDVars vars;
	protected int numVars;
	protected ODDNode odd;
	protected VarList varList;
	protected double size;
	
	// stuff to keep track of variable values in print method
	protected int[] varSizes;
	protected int[] varValues;
	protected int currentVar;
	protected int currentVarLevel;
	
	// stuff to control printing limit
	protected boolean limit;
	protected int numToPrint;
	protected int count;
	
	// log for output from print method
	protected PrismLog outputLog;
	
	// string array when exporting
	protected List<String> strList;
	
	// output format
	protected enum OutputFormat { NORMAL, MATLAB, DOT, STRINGS };
	protected OutputFormat outputFormat = OutputFormat.NORMAL;
	
	// Constructors

	/**
	 * Create a states list from a BDD and the associated model.
	 * @param states The list of states
	 * @param model The model
	 */
	public StateListMTBDD(JDDNode states, Model model)
	{
		int i;
		
		// store states list bdd
		this.states = states;
		
		// get info from model
		vars = model.getAllDDRowVars();
		numVars = vars.n();
		odd = model.getODD();
		varList = model.getVarList();
		
		// count number of states in list
		size = JDD.GetNumMinterms(states, model.getNumDDRowVars());
		
		// initialise arrays
		varSizes = new int[varList.getNumVars()];
		for (i = 0; i < varList.getNumVars(); i++) {
			varSizes[i] = varList.getRangeLogTwo(i);
		}
		varValues = new int[varList.getNumVars()];
	}

	/**
	 * Create a states list from a BDD and the associated info about variables/indexing.
	 * @param states The list of states
	 * @param vars BDD variables used to represent states
	 * @param odd ODD storing state indexing info
	 * @param varList Information about (language-level) variables
	 */
	public StateListMTBDD(JDDNode states, JDDVars vars, ODDNode odd, VarList varList)
	{
		int i;

		// store states vector mtbdd
		this.states = states;

		// store variable/indexing info
		this.vars = vars;
		this.numVars = vars.n();
		this.odd = odd;
		this.varList = varList;

		// count number of states in list
		size = JDD.GetNumMinterms(states, numVars);

		// initialise arrays
		varSizes = new int[varList.getNumVars()];
		for (i = 0; i < varList.getNumVars(); i++) {
			varSizes[i] = varList.getRangeLogTwo(i);
		}
		varValues = new int[varList.getNumVars()];
	}

	@Override
	public int size()
	{
		return (size > Integer.MAX_VALUE) ? -1 : (int)Math.round(size);
	}
	
	@Override
	public String sizeString()
	{
		return (size > Long.MAX_VALUE) ? "" + size : "" + Math.round(size);
	}

	@Override
	public void print(PrismLog log)
	{
		outputFormat = OutputFormat.NORMAL;
		limit = false;
		outputLog = log;
		doPrint();
		if (count == 0)
			outputLog.println("(none)");
	}
	
	@Override
	public void print(PrismLog log, int n)
	{
		outputFormat = OutputFormat.NORMAL;
		limit = true;
		numToPrint = n;
		outputLog = log;
		doPrint();
		if (count == 0)
			outputLog.println("(none)");
	}
	
	@Override
	public void printMatlab(PrismLog log)
	{
		outputFormat = OutputFormat.MATLAB;
		limit = false;
		outputLog = log;
		doPrint();
	}
	
	@Override
	public void printMatlab(PrismLog log, int n)
	{
		outputFormat = OutputFormat.MATLAB;
		limit = true;
		numToPrint = n;
		outputLog = log;
		doPrint();
	}
	
	@Override
	public void printDot(PrismLog log)
	{
		outputFormat = OutputFormat.DOT;
		limit = false;
		outputLog = log;
		doPrint();
	}
	
	@Override
	public List<String> exportToStringList()
	{
		strList = new ArrayList<String>((int)size);
		outputFormat = OutputFormat.STRINGS;
		limit = false;
		doPrint();
		return strList;
	}
	
	/**
	 * Implementation of printing.
	 */
	private void doPrint()
	{
		int i;
		
		count = 0;
		for (i = 0; i < varList.getNumVars(); i++) {
			varValues[i] = 0;
		}
		currentVar = 0;
		currentVarLevel = 0;
		printRec(states, 0, odd, 0);
		//log.println();
	}

	/**
	 * Main recursive part of state printing.
	 * NB: Traversal of the MTBDD/ODD is quite simple; the  tricky bit is keeping track of variable values
	 * throughout traversal - we want to be efficient and not compute the values from scratch each
	 * time, but we also want to avoid passing arrays into the recursive method.
	 */
	private void printRec(JDDNode dd, int level, ODDNode o, long n)
	{
		int i, j;
		JDDNode e, t;
		String varsString;
		
		// if we've printed enough states, stop
		if (limit) if (count >= numToPrint) return;
		
		// zero constant - bottom out of recursion
		if (dd.equals(JDD.ZERO)) return;
		
		// base case - at bottom (nonzero terminal)
		if (level == numVars) {
			
			switch (outputFormat) {
			case NORMAL: outputLog.print(n + ":("); break;
			case MATLAB: break;
			case DOT: outputLog.print(n + " [label=\"" + n + "\\n("); break;
			case STRINGS: break;
			}
			j = varList.getNumVars();
			varsString = "";
			for (i = 0; i < j; i++) {
				// integer variable
				if (varList.getType(i) instanceof TypeInt) {
					varsString += varValues[i]+varList.getLow(i);
				}
				// boolean variable
				else {
					varsString += (varValues[i] == 1);
				}
				if (i < j-1) varsString += ",";
			}
			switch (outputFormat) {
			case NORMAL: outputLog.println(varsString + ")"); break;
			case MATLAB: outputLog.println(varsString); break;
			case DOT: outputLog.println(varsString + ")\"];"); break;
			case STRINGS: strList.add(varsString);
			}
			count++;
			
			return;
		}
		
		// select else and then branches
		else if (dd.getIndex() > vars.getVarIndex(level)) {
			e = t = dd;
		}
		else {
			e = dd.getElse();
			t = dd.getThen();
		}
		
		// then recurse...
		currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; }
		printRec(e, level+1, o.getElse(), n);
		currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; }
		varValues[currentVar] += (1 << (varSizes[currentVar]-1-currentVarLevel));
		currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; }
		printRec(t, level+1, o.getThen(), n+o.getEOff());
		currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; }
		varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel));
	}

	@Override
	public boolean includes(JDDNode set)
	{
		JDDNode tmp;
		boolean incl;
		
		JDD.Ref(states);
		JDD.Ref(set);
		tmp = JDD.And(states, set);
		incl = !tmp.equals(JDD.ZERO);
		JDD.Deref(tmp);
		
		return incl;	
	}

	@Override
	public boolean includesAll(JDDNode set)
	{
		JDDNode tmp;
		boolean incl;
		
		JDD.Ref(states);
		JDD.Ref(set);
		tmp = JDD.And(states, set);
		incl = tmp.equals(set);
		JDD.Deref(tmp);
		
		return incl;	
	}

	@Override
	public Values getFirstAsValues() throws PrismException
	{
		Values values;
		int i, j, n, n2, level, v;
		JDDNode first, tmp;
		Object o;
		
		// check there is a first state
		if (size < 1) throw new PrismException("The state list contains no states");
		
		// get bdd of first state
		JDD.Ref(states);
		first = JDD.RestrictToFirst(states, vars);
		
		// traverse bdd, top to bottom, getting val (v) for each var
		tmp = states;
		values = new Values();
		n = varList.getNumVars();
		level = 0;
		for (i = 0; i < n; i++) {
			v = 0;
			n2 = varSizes[i];
			for (j = 0; j < n2; j++) {
				if (tmp.getIndex() > vars.getVarIndex(level)) {
					// tmp = tmp;
				} else if (!tmp.getElse().equals(JDD.ZERO)) {
					tmp = tmp.getElse();
				} else {
					tmp = tmp.getThen();
					v += (1 << (n2-1-j));
				}
				level++;
			}
			v += varList.getLow(i);
			if (varList.getType(i) instanceof TypeInt) {
				o = new Integer(v);
			} else {
				o = new Boolean(v == 1);
			}
			values.addValue(varList.getName(i), o);
		}
		
		// derefs
		JDD.Deref(first);
		
		return values;
	}

	@Override
	public int getIndexOfState(State state)
	{
		// Traverse BDD/ODD, top to bottom, computing index
		JDDNode ptr = states;
		ODDNode o = odd;
		int level = 0;
		int index = 0;
		// Iterate through variables
		int n = varList.getNumVars();
		for (int i = 0; i < n; i++) {
			int valInt = -1;
			try {
				valInt = varList.encodeToInt(i, state.varValues[i]); 
			} catch (PrismLangException e) {
				// Problem looking up variable - bail out 
				return -1;
			}
			// Iterate through bits for this variable
			int n2 = varSizes[i];
			for (int j = 0; j < n2; j++) {
				// Traverse BDD (need to double check state is in the set)
				if (ptr.equals(JDD.ZERO)) {
					return -1;
				} else if (ptr.getIndex() > vars.getVarIndex(level)) {
					// ptr = ptr;
				} else if ((valInt & (1 << (n2-1-j))) == 0) {
					ptr = ptr.getElse();
				} else {
					ptr.getThen();					
				}
				level++;
				// Traverse ODD (to get index)
				if ((valInt & (1 << (n2-1-j))) == 0) {
					o = o.getElse();
				} else {
					index += o.getEOff();
					o = o.getThen();	
				}
				
			}
		}
		return index;
	}
	
	@Override
	public void clear()
	{
		JDD.Deref(states);
	}
}
