package heuristics.update;

import heuristics.search.StateValue;
import heuristics.*;

import java.io.*;
import java.util.*;

import odd.ODDUtils;
import dv.DoubleVector;
import jdd.*;
import parser.*;
import parser.ast.*;
import prism.*;

public class StateValueContainerMTBDDTest
{
	// logs
	private PrismLog mainLog;		// main log
	private PrismLog techLog;		// tech log

	// ModulesFile object to store syntax tree from parser
	private ModulesFile modulesFile;
	
	// model info
	
	// type
	private ModelType modelType;				// model type (dtmc/mdp/ctmc)
	// modules
	private int numModules;			// number of modules
	private String[] moduleNames;	// module names
	// vars/constants
	private int numVars;			// total number of module variables
	private VarList varList;		// list of module variables
	private Values constantValues;	// values of constants
	// synch info
	private int numSynchs;			// number of synchronisations
	private Vector<String> synchs;			// synchronisations
	// rewards
	private int numRewardStructs;		// number of reward structs
	private String[] rewardStructNames;	// reward struct names
	
	// mtbdd stuff
	
	// dds/dd vars - whole system
	private JDDNode trans;				// transition matrix dd
	private JDDNode range;				// dd giving range for system
	private JDDNode start;				// dd for start state
	private JDDNode stateRewards[];		// dds for state rewards
	private JDDNode transRewards[];		// dds for transition rewards
	private JDDNode transActions;	// dd for transition action labels (MDPs)
	private JDDNode transPerAction[];	// dds for transitions for each action (D/CTMCs)
	private JDDNode transInd;	// dds for independent bits of trans
	private JDDNode transSynch[];	// dds for synch action parts of trans
	public JDDVars allDDRowVars;		// all dd vars (rows)
	public JDDVars allDDColVars;		// all dd vars (cols)
	private JDDVars allDDSynchVars;		// all dd vars (synchronising actions)
	private JDDVars allDDSchedVars;		// all dd vars (scheduling)
	private JDDVars allDDChoiceVars;	// all dd vars (internal non-det.)
	private JDDVars allDDNondetVars;	// all dd vars (all non-det.)
	// dds/dd vars - globals
	private JDDVars globalDDRowVars;	// dd vars for all globals (rows)
	private JDDVars globalDDColVars;	// dd vars for all globals (cols)
	// dds/dd vars - modules
	private JDDVars[] moduleDDRowVars;	// dd vars for each module (rows)
	private JDDVars[] moduleDDColVars;	// dd vars for each module (cols)
	private JDDNode[] moduleRangeDDs;	// dd giving range for each module
	private JDDNode[] moduleIdentities;	// identity matrix for each module
	// dds/dd vars - variables
	private JDDVars[] varDDRowVars;		// dd vars (row/col) for each module variable
	private JDDVars[] varDDColVars;
	private JDDNode[] varRangeDDs;		// dd giving range for each module variable
	private JDDNode[] varColRangeDDs;	// dd giving range for each module variable (in col vars)
	private JDDNode[] varIdentities;	// identity matrix for each module variable
	// dds/dd vars - nondeterminism
	private JDDNode[] ddSynchVars;		// individual dd vars for synchronising actions
	private JDDNode[] ddSchedVars;		// individual dd vars for scheduling non-det.
	private JDDNode[] ddChoiceVars;		// individual dd vars for local non-det.
	// names for all dd vars used
	private Vector<String> ddVarNames;
	// flags for keeping track of which variables have been used
	private boolean[] varsUsed;
	
	// symmetry info
	private boolean doSymmetry;			// use symmetry reduction
	private JDDNode symm; 				// dd of symmetric states
	private JDDNode nonSymms[];			// dds of non-(i,i+1)-symmetric states (i=0...numSymmModules-1)
	private int numModulesBeforeSymm;	// number of modules in the PRISM file before the symmetric ones
	private int numModulesAfterSymm;	// number of modules in the PRISM file after the symmetric ones
	private int numSymmModules;			// number of symmetric components
	
	// hidden option - do we also store each part of the transition matrix separately? (now defunct)
	private boolean storeTransParts = false; 
	// hidden option - do we also store action info for the transition matrix? (supersedes the above)
	private boolean storeTransActions = true; 


	public static void main5(String[] args) throws Exception {
		PrintStream jps = System.out;
		PrismPrintStreamLog pS = new PrismPrintStreamLog(jps);
		Prism p = new Prism(pS);
		p.initialise();
		
//		testBS.set(2);
//		testBS.set(4);
//		State testState = l.convertBitSetToState(testBS);
//		
//		ECContainerMTBDD ecc = new ECContainerMTBDD(vI);
////		System.out.println(testState);
//		JDDNode jd = ecc.state2JDD(testState);
//		State testState2 = l.convertBitSetToState(testBS);
//		StateValueContainerMTBDD stv = new StateValueContainerMTBDD(new VarInfo(mf));
//		System.out.println(testState2);
//		StateValue val = new StateValue(0.2,1.0,1);
//		JDDNode jd2 = stv.state2JDD(testState2);
//		JDD.Ref(jd2);
		
//		JDD.Deref(jd);
//		JDD.Deref(jd);
//		JDD.Deref(jd);
//		JDDNode test = JDD.And(jd, jd);
//		System.out.println(DebugJDD.getRefCount(jd));
//		JDD.Deref(test);
//		System.out.println(DebugJDD.getRefCount(jd));
//		JDD.InitialiseCUDD();
//		DoubleVector.setCUDDManager();
//		ODDUtils.setCUDDManager();
//		JDD.SetOutputStream(pS.getFilePointer());
//		JDDNode test = new JDDNode(31232);
//		DebugJDD.printNonZeroTraces();
//		System.out.println(DebugJDD.localCounters.size());
//		for (int i = 0; i < 125697; i++){
//			JDDNode work = JDD.Var(i);
////			JDD.Ref(work);
//			JDD.Deref(work);
////			JDD.Deref(work);
//			System.out.println("refcount: "+ i + " " + DebugJDD.getRefCount(work));
//		}
//		DebugJDD.printNonZeroTraces();
//		System.out.println("refcount: " + DebugJDD.getRefCount(jd2));
//		JDDNode test2 = JDD.And(jd2, jd);
		JDD.CloseDownCUDD();
	}
	
	public static BitSet convert(long value) {
	    BitSet bits = new BitSet();
	    int index = 0;
	    while (value != 0L) {
	      if (value % 2L != 0) {
	        bits.set(index);
	      }
	      ++index;
	      value = value >>> 1;
	    }
	    return bits;
	  }
	
	public static void main7(String[] args) {
		JDD.InitialiseCUDD();
		JDDVars vars = new JDDVars();
		for (int i = 0; i < 48; i++) {
			vars.addVar(JDD.Var(i));
		}
		long index = (long) Integer.MAX_VALUE*3;
		int index2 = (int)index;
		System.out.println(index + " ~~ " + index2);
		System.out.println(JDD.GetVectorElement(JDD.SetVectorElement(JDD.ZERO, vars, index, 1.0), vars, index2));
		JDD.CloseDownCUDD();
	}
	
	public static void main(String[] args) throws Exception {
		PrintStream jps = new PrintStream(System.out);
		PrismPrintStreamLog pS = new PrismPrintStreamLog(jps);
		Prism p = new Prism(pS);
		JDD.InitialiseCUDD();
//		p.initialise();
////		PrismParser pp = new PrismParser();
		File modules = new File("C:/Users/afellner/Documents/prism-games-heuristics/prism-examples/wlan/test.nm");
//		
//		File modules = new File("tests/heuristics/new/debug_heuristic_new_1.prism");
////		File modules = new File("examples/coins/coins.prism");
////		InputStream modules = new FileInputStream("C:/Users/afellner/Documents/prism-games-heuristics/prism-examples/wlan/test.nm");
////		ModulesFile mf = pp.parseModulesFile(modules);
		ModulesFile mf = p.parseModelFile(modules);
		Iterator<String> i = mf.getSynchs().iterator();
		
		System.out.println("#commands: " + mf.getSynchs().size());
		System.out.println("commands:");
		while (i.hasNext()) {
			System.out.println(i.next());
		}
		VarInfo vI = new VarInfo(mf);
		JDDVars vars = vI.getJDDVars();
		Double bound = Math.pow(2, vars.n());
		System.out.println(vars.n());
//		long longbound = bound.longValue();
//		boolean foundone = false;
//		Random r = new Random();
//		long index1 = 0;
//		long index2 = 1;
//		int setTo = 1;
////		JDDNode test = JDD.ZERO;
		BitSet stateBS = new BitSet();
////		State s = vI.getModuleVarList().convertBitSetToState(stateBS);
		State s;
		long index;
////		System.out.println(s);
		JDDNode plain = JDD.ZERO;
		stateBS.set(0);
		stateBS.set(1);
//		for (int i = 0; i < vI.getVarNames().length; i++) {
//			System.out.println(vI.getVarNames()[i]);
//		}
		s = vI.getModuleVarList().convertBitSetToState(stateBS);
		index = vI.state2Index(s);
		long index2 = (int)index;
		System.out.println(index + " <> " + index2);
		System.out.println("state: " + s + " index " + index + " BS: " + stateBS);
		JDDNode target = JDD.SetVectorElement(JDD.ZERO, vars, index, 1.0);
		System.out.println(JDD.GetVectorElement(target, vars, index2));
////		JDD.SetVectorElement(target, vars, 1, 1.0);
//		JDDVars testvars = new JDDVars();
//		testvars.addVar(JDD.Var(0));
//		testvars.addVar(JDD.Var(2));
//		JDD.PrintVector(target, testvars);
//		for (int i = 0; i < bound; i++) {
//			stateBS = BitSet.valueOf(new long[]{i});
//			s = vI.getModuleVarList().convertBitSetToState(stateBS);
//			index = vI.state2Index(s);
////			JDD.Ref(target);
//			JDDNode target = JDD.SetVectorElement(plain, vI.getJDDVars(), index, 1.0);
//			System.out.println("state: " + s + " index " + index + " BS: " + stateBS);
//			JDD.PrintVector(JDD.PLUS_INFINITY,vars);
//			JDD.PrintVector(target, vars);
//			JDD.PrintVector(JDD.PLUS_INFINITY,vars);
//			System.out.println("bitset: " + stateBS);
//		}
		
//		for (int i = 0; i < vI.getModuleVarList().getNumVars(); i++){
//			for (int j = vI.getModuleVarList().getLow(i); j < vI.getModuleVarList().getHigh(i); j++) {
//				System.out.println("state: " + s);
//				System.out.println("bitset: " + stateBS);
//				System.out.println("i+j:" + (i + j));
//				stateBS.set(i+j);
//				s = vI.getModuleVarList().convertBitSetToState(stateBS);
//			}
//		}
//		while (!foundone) {
//			index1 = (long)(r.nextDouble()*longbound);
//			index2 = (long)(r.nextDouble()*longbound);
//			if (index1 != index2) {
//				Boolean tmpSet = r.nextBoolean();
//				if (tmpSet) setTo = 1;
//				else setTo = 0;
//				Double val1 = JDD.GetVectorElement(test, vars, index2);
//				JDDNode tmp = JDD.SetVectorElement(test, vars, index1, setTo);
//				Double val2 = JDD.GetVectorElement(tmp, vars, index2);
//				if (val1.intValue() != val2.intValue()) {
//					foundone = true;
//					System.out.println("When setting " + index2 + " also " + index1 + " changed from " + val1 + " to " + val2);
//				}
//				else System.out.println("Check");
//			}
//		}
				
		
		
		
//		BitSet testBS = new BitSet();
//		State s = vI.getModuleVarList().convertBitSetToState(testBS);
//		
//		vI.state2JDD(s);
//		vI.state2JDD(s);
//		vI.state2JDD(s);
		
//		JDDVars vars = vI.getJDDVars();
//		JDDNode var0 = vars.getVar(0);
//		JDDNode var1 = vars.getVar(1);
//		JDDNode var2 = vars.getVar(2);
//		JDDNode var3 = vars.getVar(3);
//		JDDNode var4 = vars.getVar(4);
//		
//		
//		System.out.println("initial: ");
//		vI.printRefCounts();
//		
//		JDDNode and = JDD.And(var2, var1);
//		JDDNode or = JDD.Or(var4, var3);
//		
//		System.out.println("After and: ");
//		vI.printRefCounts();
//		System.out.println("and rc: " + DebugJDD.getRefCount(and));
//		System.out.println("or rc: " + DebugJDD.getRefCount(or));
//		
//		JDDNode ite = JDD.ITE(var2, var3, var4);
//		
//		System.out.println("After ite: ");
//		vI.printRefCounts();
//		System.out.println("and rc: " + DebugJDD.getRefCount(and));
//		System.out.println("or rc: " + DebugJDD.getRefCount(or));
//		System.out.println("ite rc: " + DebugJDD.getRefCount(ite));
	}
	
	public static void main3(String[] args) throws Exception {
		PrintStream jps = System.out;
		PrismPrintStreamLog pS = new PrismPrintStreamLog(jps);
		Prism p = new Prism(pS);
//		File modules = new File("tests/heuristics/debug_heuristic_2.prism");
		File modules = new File("examples/coins/coins.prism");
		ModulesFile mf = p.parseModelFile(modules);
		VarList l = new VarList(mf);
		BitSet testBS = new BitSet();
		testBS.set(1);
//		testBS.set(1);
//		testBS.set(2);
		testBS.set(4);
		State testState = l.convertBitSetToState(testBS);
		StateValueContainerMTBDD stv = new StateValueContainerMTBDD(new VarInfo(mf));
		System.out.println(testState);
		StateValue val = new StateValue(0.2,1.0,1);
		stv.setQValue(testState, val, -1);
		System.out.println(stv.getQValue(testState, -1));
//		stv.state2JDD(testState);
//		stv.setLow(testState,-1, 0.2);
//		System.out.println(stv.getLow(testState));
	}
		
	public static void main2(String[] args) throws Exception {
		InputStream modules = new FileInputStream("examples/coins/coins.prism");
		PrismParser pp = new PrismParser();
		ModulesFile mf = pp.parseModulesFile(modules);
		System.out.println(new VarList(mf));
		StateValueContainerMTBDDTest stv = new StateValueContainerMTBDDTest(mf);
		System.out.println("before");
		JDD.InitialiseCUDD();
		stv.test();
		System.out.println("after");
		System.out.println(stv.allDDColVars + "\n" + stv.allDDRowVars);
	}
	
	public StateValueContainerMTBDDTest(ModulesFile mf)
	{
		modulesFile = mf;
		// get symmetry reduction info
		doSymmetry = false;
	}
	
	public static void main1(String[] args) throws Exception {
		PrintStream jps = System.out;
		PrismPrintStreamLog pS = new PrismPrintStreamLog(jps);
		Prism p = new Prism(pS);
		File modules = new File("tests/heuristics/debug_heuristic_2.prism");
//		File modules = new File("examples/coins/coins.prism");
		ModulesFile mf = p.parseModelFile(modules);
		VarList l = new VarList(mf);
		System.out.println(mf.getVarNames() + " " + mf.getVarTypes());
		JDD.InitialiseCUDD();
		System.out.println("vars: " + l.getTotalNumBits() + " states: " + l.getAllStates());
		JDDVars vars = new JDDVars();
//		for (int i= 0; i < l.getNumVars(); i++) {
//			for (int j = l.getLow(0); j < l.getHigh(i); j++) {
////				JDDNode bla = new JDDNode(i*l.getNumVars()+j);
//				System.out.println("adding " + (i*l.getHigh(i)+j));
//				vars.addVar(JDD.Var(i*l.getNumVars()+j));
//			}
//		}
		JDDNode[] stateNodes = new JDDNode[l.getAllStates().size()];
//		for (State s: l.getAllStates()) {
//			JDDNode tmp = JDD.Var(l.getIndex(s.toString()));
//			System.out.println(tmp);
//		}
		int ddVars = 0;
		String[] varNames = new String[l.getTotalNumBits()];
		for (int i = 0; i < l.getNumVars(); i++) {
			System.out.println("var: " + l.getName(i) + " range: " + l.getRange(i));
			for (int j = 0; j < l.getRangeLogTwo(i); j++) {
				JDDNode tmp = JDD.Var(ddVars);
				vars.addVar(tmp);
				varNames[ddVars] = l.getName(i) + "." + j;
				ddVars++;
			}
		}
		for (int i = 0; i < vars.n(); i++) {
			System.out.println(varNames[i]);
		}
		BitSet testBS = new BitSet();
		testBS.set(1);
		testBS.set(4);
		
		JDDNode jnode = vars.getVar(0);
//		JDD.PrintVector(jnode, vars);
		System.out.println(jnode.getElse());
		
		JDDNode const5 = JDD.Constant(5.0);
		JDDNode bit2 = JDD.Var(2);
		JDDNode bit1 = JDD.Var(1);
		JDDNode bit0 = JDD.Var(0);
		JDDNode state_100 = JDD.And(bit0,JDD.And(JDD.Not(bit1), JDD.Not(bit2)));
//		JDDNode set5 = JDD.And(const5,state_100);
		JDDNode init = JDD.MINUS_INFINITY;
//		JDDNode set5 = JDD.SetVectorElement(bit0, vars, 4, 5);
//		
		JDD.PrintVector(init, vars);
		
		JDDNode set5 = JDD.SetVectorElement(init, vars, 4, 5);
		
		JDD.PrintVector(state_100, vars);
		JDD.PrintVector(set5, vars);
		
		System.out.println("Value: " + set5.getThen().getElse().getElse().getValue());
		
//		JDD.a
		
		State testState = l.convertBitSetToState(testBS);
//		System.out.println("BitSet: " + testBS + " state -> " + testState);
		int index = 0;
		for (int i =0; i < testState.varValues.length; i++) {
			int value = 0;
			if (testState.varValues[i] instanceof Boolean && ((Boolean)testState.varValues[i])) {
				value = 1;
			}
			else if (testState.varValues[i] instanceof Integer) {
				value = (Integer)testState.varValues[i];
			}
			else {
				System.out.println(testState.varValues[i] + " is not bool nor int");
			}
			index += value*Math.pow(2, i);
		}
		System.out.println("BitSet: " + testBS + " state -> " + testState + " index: " + index);
		
	}
	
	public void test() throws PrismException, FileNotFoundException
	{
		
		JDDNode tmp, tmp2;
		JDDVars ddv;
		int i;
		
		// get variable info from ModulesFile
		varList = modulesFile.createVarList();
		if (varList.containsUnboundedVariables())
			throw new PrismException("Cannot build a model that contains a variable with unbounded range (try the explicit engine instead)");
		numVars = varList.getNumVars();
		constantValues = modulesFile.getConstantValues();
		
		// get basic system info
		modelType = modulesFile.getModelType();
		moduleNames = modulesFile.getModuleNames();
		numModules = modulesFile.getNumModules();
		synchs = modulesFile.getSynchs();
		System.out.println(synchs);
		if (synchs != null) {
			numSynchs = synchs.size();
		}
		
		// allocate dd variables
		allocateDDVars();
//		sortDDVars();
//		sortIdentities();
//		sortRanges();
		
		// get rid of any nondet dd variables not needed
		if (modelType == ModelType.MDP) {
			tmp = JDD.GetSupport(trans);
			tmp = JDD.ThereExists(tmp, allDDRowVars);
			tmp = JDD.ThereExists(tmp, allDDColVars);
			tmp2 = tmp;
			ddv = new JDDVars();
			while (!tmp2.equals(JDD.ONE)) {
				ddv.addVar(JDD.Var(tmp2.getIndex()));
				tmp2 = tmp2.getThen();
			}
			JDD.Deref(tmp);
			allDDNondetVars.derefAll();
			allDDNondetVars = ddv;
		}
	}
	private void allocateDDVars()
	{
		JDDNode v, vr, vc;
		int i, j, m, n, last;
		int ddVarsUsed = 0;
		ddVarNames = new Vector<String>();

//		switch (prism.getOrdering()) {
		int bla = 1;
		switch(bla) {
		case 1:
		// ordering: (a ... a) (s ... s) (l ... l) (r c ... r c)
		
			// create arrays/etc. first
			
			// nondeterministic variables
			if (modelType == ModelType.MDP) {
				// synchronizing action variables
				ddSynchVars = new JDDNode[numSynchs];
				// sched nondet vars
				ddSchedVars = new JDDNode[numModules];
				// local nondet vars
				// max num needed = total num of commands in all modules + num of modules
				// (actually, might need more for complex parallel compositions? hmmm...)
				m = numModules;
				for (i = 0; i < numModules; i++) {
					m += modulesFile.getModule(i).getNumCommands();
				}
				ddChoiceVars = new JDDNode[m];
			}
			// module variable (row/col) vars
			varDDRowVars = new JDDVars[numVars];
			varDDColVars = new JDDVars[numVars];
			for (i = 0; i < numVars; i++) {
				varDDRowVars[i] = new JDDVars();
				varDDColVars[i] = new JDDVars();
			}
			
			// now allocate variables

			// allocate synchronizing action variables
			if (modelType == ModelType.MDP) {
				// allocate vars
				for (i = 0; i < numSynchs; i++) {
					v = JDD.Var(ddVarsUsed++);
					ddSynchVars[i] = v;
					ddVarNames.add(synchs.elementAt(i)+".a");
				}
			}
		
			// allocate scheduling nondet dd variables
			if (modelType == ModelType.MDP) {
				// allocate vars
				for (i = 0; i < numModules; i++) {
					v = JDD.Var(ddVarsUsed++);
					ddSchedVars[i] = v;
					ddVarNames.add(moduleNames[i] + ".s");
				}
			}
			
			// allocate internal nondet choice dd variables
			if (modelType == ModelType.MDP) {
				m = ddChoiceVars.length;
				for (i = 0; i < m; i++) {
					v = JDD.Var(ddVarsUsed++);
					ddChoiceVars[i] = v;
					ddVarNames.add("l" + i);
				}
			}
			
			// create a gap in the dd variables
			// this allows to prepend additionl row/col vars, e.g. for constructing
			// a product model when doing LTL model checking
			for (i = 0; i < 20; i++) {
				ddVarsUsed++;
				ddVarNames.add("");
			}
			
			// allocate dd variables for module variables (i.e. rows/cols)
			// go through all vars in order (incl. global variables)
			// so overall ordering can be specified by ordering in the input file
			for (i = 0; i < numVars; i++) {
				// get number of dd variables needed
				// (ceiling of log2 of range of variable)
				System.out.println(varList);
				n = varList.getRangeLogTwo(i);
				// add pairs of variables (row/col)
				for (j = 0; j < n; j++) {
					// new dd row variable
//					ddVarsUsed = 0;
					vr = JDD.Var(ddVarsUsed++);
					// new dd col variable
					vc = JDD.Var(ddVarsUsed++);
					varDDRowVars[i].addVar(vr);
					varDDColVars[i].addVar(vc);
					// add names to list
					ddVarNames.add(varList.getName(i) + "." + j);
					ddVarNames.add(varList.getName(i) + "'." + j);
				}
			}
			
			break;
			
		case 2:
		// ordering: (a ... a) (l ... l) (s r c ... r c) (s r c ... r c) ...
	
			// create arrays/etc. first
			
			// nondeterministic variables
			if (modelType == ModelType.MDP) {
				// synchronizing action variables
				ddSynchVars = new JDDNode[numSynchs];
				// sched nondet vars
				ddSchedVars = new JDDNode[numModules];
				// local nondet vars: num = total num of commands in all modules + num of modules
				m = numModules;
				for (i = 0; i < numModules; i++) {
					m += modulesFile.getModule(i).getNumCommands();
				}
				ddChoiceVars = new JDDNode[m];
			}
			// module variable (row/col) vars
			varDDRowVars = new JDDVars[numVars];
			varDDColVars = new JDDVars[numVars];
			for (i = 0; i < numVars; i++) {
				varDDRowVars[i] = new JDDVars();
				varDDColVars[i] = new JDDVars();
			}
			
			// now allocate variables
			
			// allocate synchronizing action variables
			if (modelType == ModelType.MDP) {
				for (i = 0; i < numSynchs; i++) {
					v = JDD.Var(ddVarsUsed++);
					ddSynchVars[i] = v;
					ddVarNames.add(synchs.elementAt(i)+".a");
				}
			}

			// allocate internal nondet choice dd variables
			if (modelType == ModelType.MDP) {
				m = ddChoiceVars.length;
				for (i = 0; i < m; i++) {
					v = JDD.Var(ddVarsUsed++);
					ddChoiceVars[i] = v;
					ddVarNames.add("l" + i);
				}
			}
			
			// go through all vars in order (incl. global variables)
			// so overall ordering can be specified by ordering in the input file
			// use 'last' to detect when starting a new module
			last = -1; // globals are -1
			for (i = 0; i < numVars; i++) {
				// if at the start of a module's variables
				// and model is an mdp...
				if ((modelType == ModelType.MDP) && (last != varList.getModule(i))) {
					// add scheduling dd var(s) (may do multiple ones here if modules have no vars)
					for (j = last+1; j <= varList.getModule(i); j++) {
						v = JDD.Var(ddVarsUsed++);
						ddSchedVars[j] = v;
						ddVarNames.add(moduleNames[j] + ".s");
					}
					// change 'last'
					last = varList.getModule(i);
				}
				// now add row/col dd vars for the variable
				// get number of dd variables needed
				// (ceiling of log2 of range of variable)
				n = varList.getRangeLogTwo(i);
				// add pairs of variables (row/col)
				for (j = 0; j < n; j++) {
					vr = JDD.Var(ddVarsUsed++);
					vc = JDD.Var(ddVarsUsed++);
					varDDRowVars[i].addVar(vr);
					varDDColVars[i].addVar(vc);
					ddVarNames.add(varList.getName(i) + "." + j);
					ddVarNames.add(varList.getName(i) + "'." + j);
				}
			}
			// add any remaining scheduling dd var(s) (happens if some modules have no vars)
			if (modelType == ModelType.MDP) for (j = last+1; j <numModules; j++) {
				v = JDD.Var(ddVarsUsed++);
				ddSchedVars[j] = v;
				ddVarNames.add(moduleNames[j] + ".s");
			}
			break;
			
		default:
			mainLog.printWarning("Invalid MTBDD ordering selected - it's all going to go wrong.");
			break;
		}
		
		// print out all mtbdd variables allocated
		System.out.print("\nMTBDD variables:");
		for (i = 0; i < ddVarNames.size(); i++) {
			System.out.print(" (" + i + ")" + ddVarNames.elementAt(i));
		}
		System.out.println();
	}

	// sort out DD variables and the arrays they are stored in
	// (more than one copy of most variables is stored)
			
	private void sortDDVars()
	{
		int i, m;
		
		// put refs for all globals and all vars in each module together
		// create arrays
		globalDDRowVars = new JDDVars();
		globalDDColVars = new JDDVars();
		moduleDDRowVars = new JDDVars[numModules];
		moduleDDColVars = new JDDVars[numModules];
		for (i = 0; i < numModules; i++) {
			moduleDDRowVars[i] = new JDDVars();
			moduleDDColVars[i] = new JDDVars();
		}
		// go thru all variables
		for (i = 0; i < numVars; i++) {
			varDDRowVars[i].refAll();
			varDDColVars[i].refAll();
			// check which module it belongs to
			m = varList.getModule(i);
			// if global...
			if (m == -1) {
				globalDDRowVars.addVars(varDDRowVars[i]);
				globalDDColVars.addVars(varDDColVars[i]);
			}
			// otherwise...
			else {
				moduleDDRowVars[m].addVars(varDDRowVars[i]);
				moduleDDColVars[m].addVars(varDDColVars[i]);
			}
		}
		
		// put refs for all vars in whole system together
		// create arrays
		allDDRowVars = new JDDVars();
		allDDColVars = new JDDVars();
		if (modelType == ModelType.MDP) {
			allDDSynchVars = new JDDVars();
			allDDSchedVars = new JDDVars();
			allDDChoiceVars = new JDDVars();
			allDDNondetVars = new JDDVars();
		}
		// go thru all variables
		for (i = 0; i < numVars; i++) {
			// add to list
			varDDRowVars[i].refAll();
			varDDColVars[i].refAll();
			allDDRowVars.addVars(varDDRowVars[i]);
			allDDColVars.addVars(varDDColVars[i]);
		}
		if (modelType == ModelType.MDP) {
			// go thru all syncronising action vars
			for (i = 0; i < ddSynchVars.length; i++) {
				// add to list
				JDD.Ref(ddSynchVars[i]);
				JDD.Ref(ddSynchVars[i]);
				allDDSynchVars.addVar(ddSynchVars[i]);
				allDDNondetVars.addVar(ddSynchVars[i]);
			}
			// go thru all scheduler nondet vars
			for (i = 0; i < ddSchedVars.length; i++) {
				// add to list
				JDD.Ref(ddSchedVars[i]);
				JDD.Ref(ddSchedVars[i]);
				allDDSchedVars.addVar(ddSchedVars[i]);
				allDDNondetVars.addVar(ddSchedVars[i]);
			}
			// go thru all local nondet vars
			for (i = 0; i < ddChoiceVars.length; i++) {
				// add to list
				JDD.Ref(ddChoiceVars[i]);
				JDD.Ref(ddChoiceVars[i]);
				allDDChoiceVars.addVar(ddChoiceVars[i]);
				allDDNondetVars.addVar(ddChoiceVars[i]);
			}
		}
	}
	
	// sort DDs for identities
	
	private void sortIdentities()
	{
		int i, j;
		JDDNode id;
		
		// variable identities
		varIdentities = new JDDNode[numVars];
		for (i = 0; i < numVars; i++) {
			// set each element of the identity matrix
			id = JDD.Constant(0);
			for (j = 0; j < varList.getRange(i); j++) {
				id = JDD.SetMatrixElement(id, varDDRowVars[i], varDDColVars[i], j, j, 1);
			}
			varIdentities[i] = id;
		}
		// module identities
		moduleIdentities = new JDDNode[numModules];
		for (i = 0; i < numModules; i++) {
			// product of identities for vars in module
			id = JDD.Constant(1);
			for (j = 0; j < numVars; j++) {
				if (varList.getModule(j) == i) {
					JDD.Ref(varIdentities[j]);
					id = JDD.Apply(JDD.TIMES, id, varIdentities[j]);
				}
			}
			moduleIdentities[i] = id;
		}
	}

	// Sort DDs for ranges
	
	private void sortRanges()
	{
		int i;
		
		// initialise raneg for whole system
		range = JDD.Constant(1);
		
		// variable ranges		
		varRangeDDs = new JDDNode[numVars];
		varColRangeDDs = new JDDNode[numVars];
		for (i = 0; i < numVars; i++) {
			// obtain range dd by abstracting from identity matrix
			JDD.Ref(varIdentities[i]);
			varRangeDDs[i] = JDD.SumAbstract(varIdentities[i], varDDColVars[i]);
			// obtain range dd by abstracting from identity matrix
			JDD.Ref(varIdentities[i]);
			varColRangeDDs[i] = JDD.SumAbstract(varIdentities[i], varDDRowVars[i]);
			// build up range for whole system as we go
			JDD.Ref(varRangeDDs[i]);
			range = JDD.Apply(JDD.TIMES, range, varRangeDDs[i]);
		}
		// module ranges
		moduleRangeDDs = new JDDNode[numModules];
		for (i = 0; i < numModules; i++) {
			// obtain range dd by abstracting from identity matrix
			JDD.Ref(moduleIdentities[i]);
			moduleRangeDDs[i] = JDD.SumAbstract(moduleIdentities[i], moduleDDColVars[i]);			
		}
	}
}
