package heuristics;

import heuristics.decisiontree.WekaTree;

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

import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
import parser.VarList;
import parser.ast.*;
import prism.*;
import weka.classifiers.Classifier;
import weka.core.Attribute;
import weka.core.FastVector;
import weka.core.Instance;
import weka.core.Instances;
import mtbdd.PrismMTBDD;

public class Test {

	public static void main8(String[] args) throws Exception {
		PrintStream jps = System.out;
		PrismPrintStreamLog pS = new PrismPrintStreamLog(jps);
		Prism p = new Prism(pS);
		p.setEngine(Prism.EXPLICIT);
		File modules = new File("C:/workspace/prism-examples/mer/mer2_2_full.nm");
		ModulesFile mf = p.parseModelFile(modules);
		Vector<String> labels = mf.getSynchs();
		System.out.println("synchs:");
		for (String l: labels) System.out.println(l);
		for (int i = 0; i < mf.getNumModules(); i++) {
			System.out.println("module: " + i);
			for (Command c: mf.getModule(i).getCommands()) {
				if (c.getSynch().equals("")) System.out.println(c);
//				else System.out.println(c.getSynch());
			}
		}
		System.out.println("modules: ");
		for (String m: mf.getModuleNames()) {
			System.out.println(m);
		}
	}
	
	public static void main6(String[] args) {
		System.out.println((Math.pow(Math.sqrt(3),3) * 4 * Math.PI) / (Math.pow(Math.sqrt(4), 3) * 3));
	}
	
	public static void main7(String[] args) {
		JDD.InitialiseCUDD();
		JDDNode c1 = JDD.ONE;
		System.out.println("c1: " + numNodes(c1));
		
		JDDVars vars = new JDDVars();
		JDDNode x1 = JDD.Var(3);
		JDDNode x2 = JDD.Var(2);
		JDDNode x3 = JDD.Var(1);
		
		System.out.println("x1: " + x1 + "\nx2: " + x2 + "\nx3: " + x3);
		
		JDDNode c2 = JDD.Constant(2.0);
		JDDNode c3 = JDD.Constant(3.0);
		JDDNode c4 = JDD.Constant(4.0);
		
		JDDNode dec1 = JDD.ITE(x1, c1, c2);
		
		System.out.println("dec1: " + numNodes(dec1));
		JDD.Ref(dec1);
		JDDNode dec2 = JDD.ITE(x2, dec1, c3);
		System.out.println("dec2: " + numNodes(dec2));
		
//		System.out.println("dec1: " + dec1);
		
//		System.out.println("dec2 set: " + allNodes(dec2));
		
		JDDNode dec3 = JDD.ITE(x3, dec2, c3);
		System.out.println("dec3: " + numNodes(dec3));
		
		JDDNode dec4 = JDD.ITE(x3, dec2, c4);
		System.out.println("dec4: " + numNodes(dec4));
		
		JDDNode and = JDD.And(x3, x2);
		
		JDDNode dec5 = JDD.ITE(and, c4, dec4);
		System.out.println("dec5: " + numNodes(dec5));
	}
	
	public static void main9(String[] args) {
		
		FastVector attributes = new FastVector(3);

		FastVector fvAttrVal = new FastVector(3);
		fvAttrVal.addElement("[action_1]");
		fvAttrVal.addElement("[action_2]");
		fvAttrVal.addElement("[action_3]");

		attributes.addElement(new Attribute("played_action",fvAttrVal));
		
//		attributes.addElement(new Attribute("played_action"));
		
		attributes.addElement(new Attribute("some_state_var"));
		
		FastVector fvClassVal = new FastVector(2);
		fvClassVal.addElement("good");
		fvClassVal.addElement("bad");
		
		Attribute classAttribute = new Attribute("classification", fvClassVal);
		attributes.addElement(classAttribute);
		Instances trainingSet = new Instances("Rel", attributes, 100);
		trainingSet.setClassIndex(2);
		Classifier tree = WekaTree.createTree(0);
		
		Instance test1 = new Instance(3);
		Instance test2 = new Instance(3);
		Instance test3 = new Instance(3);
				
		test1.setDataset(trainingSet);
		test2.setDataset(trainingSet);
		test3.setDataset(trainingSet);
		
		test1.setValue(0, "[action_1]");
		test1.setValue(1, 3);
		test1.setValue(2, "good");

		test2.setValue(0, "[action_2]");
		test2.setValue(1, 3);
		test2.setValue(2, "bad");

		test3.setValue(0, "[action_3]");
		test3.setValue(1, 3);
		test3.setValue(2, "good");
		
		trainingSet.add(test1);
		trainingSet.add(test2);
		trainingSet.add(test3);
		
		test1.setValue(0, "[action_2]");
		test1.setValue(1, 1);
		test1.setValue(2, "bad");
		
		trainingSet.add(test1);
		
		try {
			String[] opts = {"-M","1"};
			tree.setOptions(opts);
			tree.buildClassifier(trainingSet);
			System.out.println(tree);
		} catch (Exception e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		
	}
	
	public static void main(String[] args) {
		int minIt = 20;
		
		
		int instances = 75390;
		double b = Math.log(instances) / minIt;
		System.out.println(b);
		double factor = (instances - 1) / (Math.exp(b*(minIt-1)));
		int minInstances = 2;
		System.out.println("factor: " + factor);
		for (int l = 0; l < minIt; l++) {
			minInstances = (int) Math.round(factor * Math.exp(l*b) - factor + 1);
//			if (l != 0) {
//				minInstances = (int) Math.round(2 + factor*Math.exp(1.1*l));
//			}
			System.out.println(minInstances);
		}
	}
		
	public static void main2(String[] args) throws Exception {
		PrintStream jps = System.out;
		PrismPrintStreamLog pS = new PrismPrintStreamLog(jps);
		Prism p = new Prism(pS);
		p.setEngine(Prism.EXPLICIT);
		File modules = new File("tests/heuristics/debug_heuristic_2.prism");
		File properties = new File("tests/heuristics/debug_heuristic_2.prism.props");
		ModulesFile mf = p.parseModelFile(modules);
		mf.getModule(0);
		PropertiesFile prop = p.parsePropertiesFile(mf, properties);
		p.loadPRISMModel(mf);
		p.setVerbose(true);
		p.modelCheck(prop, prop.getProperty(0));
	}
	
	public static void main3(String[] args) throws Exception {
		System.out.println("test123");
		PrintStream jps = System.out;
		PrismPrintStreamLog pS = new PrismPrintStreamLog(jps);
		Prism p = new Prism(pS);
		p.setEngine(Prism.EXPLICIT);
//		File modules = new File("tests/heuristics/test1.prism");
//		File properties = new File("tests/heuristics/test1.prism.props");
		File modules = new File("tests/heuristics_new/mer2_2_full.nm");
		File properties = new File("tests/heuristics_new/mer.pctl");
//		File modules = new File("tests/heuristics_new/zeroconf.nm");
//		File properties = new File("tests/heuristics_new/zeroconf.pctl");
		ModulesFile mf = p.parseModelFile(modules);
		PropertiesFile prop = p.parsePropertiesFile(mf, properties);
		p.loadPRISMModel(mf);
//		p.setVerbose(true);
		p.setHeuristic(true);
		p.setHeuristicName("RR");
		p.setHeuristicNextStateName("BRTDP");
//		p.buildModel();
		p.modelCheck(prop, prop.getProperty(0));
//			
	}
	
//	public static void main(String[] args) throws Exception {
//		PrintStream jps = System.out;
//		PrismPrintStreamLog pS = new PrismPrintStreamLog(jps);
//		Prism p = new Prism(pS);
//		ModulesFile mf = p.parseModelFile(new File("tests/heuristics/mectest.prism"));
//		
//		explicit.ECComputer ec = explicit.ECComputer.createECComputer(mc, smg);
//		ec.computeMECStates();
//	}
	
	public static void main5(String[] args) throws Exception{
		boolean allsame = true;
		for (int i = 1; i <= 12; i++) {
			String file = "tests/heuristics/debug_heuristic_"+i+".prism";
			String prop = "tests/heuristics/debug_heuristic_"+i+".prism.props";
			String[] arguments = {file,prop,"-property","2","-brtdp:heuristic=BRTDP"};
//			Result res = PrismCL.main(arguments);
			Result res = null;
			String[] arguments2 = {file,prop,"-property","2","-brtdp_bscc:heuristic=BRTDP"};
//			Result res2 = PrismCL.main(arguments2);
			Result res2 = null;
			if (!res.equals(res2)) {
				System.out.println("**********************************Test "+i+"\nResult1: " + res + "\nResult2: " + res2 + "\n**********************************");
				allsame = false;
			}
		}
		System.out.println("same results: " + allsame);
//		String[] test = {"tests/heuristics_new/coins.prism","tests/heuristics_new/coins.props","-property","1","-brtdp:heuristic=BRTDP,verbose"};
		
//		PrismMTBDD mt = new PrismMTBDD();
//		PrintStream jps = System.out;
//		PrismPrintStreamLog pS = new PrismPrintStreamLog(jps);
//		mt.initialise(pS, pS);
//		System.out.println(mt);
	}
	
	public static void main1(String[] args) throws Exception{
		JDD.InitialiseCUDD();
		JDDVars vars = new JDDVars();
//		vars.addVar(JDD.Var(0));
		JDDNode a = new JDDNode(JDD.Var(0));
		JDD.PrintVector(a,vars);
	}
	
	public static void main4(String[] args) throws Exception{
		JDDNode a, b, c, d, e;
		JDDVars vars;		
		
		System.out.println("\nTest program for JDD\n====================");
		
		// initialise cudd
		JDD.InitialiseCUDD();
			
		// set up some variables
		vars = new JDDVars();
		vars.addVar(JDD.Var(0));
		
		
		
//		a = JDD.Create();
		a = new JDDNode(0);
		System.out.println(a);
		JDD.PrintVector(a,vars);
		a = JDD.SetVectorElement(a, vars, 0, 1);
		a = JDD.SetVectorElement(a, vars, 1, 2);
//		
//		b = JDD.Create();
//		b = JDD.SetVectorElement(b, vars, 0, 2);
//		b = JDD.SetVectorElement(b, vars, 1, 3);
//		JDD.PrintVector(a, vars);
//		JDD.PrintVector(b, vars);
//		
//		vars.addVar(JDD.Var(1));
//		
//		c = JDD.Var(1);
//		
//		d = JDD.ITE(c, b, a);
//		
////		d = JDD.Apply(JDD.MAX, a, b);
//		
//
//		JDD.PrintVector(d, vars);
//		
////		e = JDD.GreaterThanEquals(JDD.Var(1), 1.0);
//		
//		JDD.PrintVector(JDD.Var(0),vars);
//		JDD.PrintVector(JDD.Var(1),vars);
//		
//		JDD.PrintInfo(d, 2);
//		JDD.Deref(d);
//		JDD.Deref(a);
//		JDD.Deref(b);
	}
	
	private static int numNodes(JDDNode node) {
		return allNodes(node).size();
	}
	
	
	private static Set<JDDNode> allNodes(JDDNode node) {
		Set<JDDNode> out = new HashSet<JDDNode>();
		out.add(node);
//		System.out.println(node + " ~ " + node.getIndex() + " ~ " + node.ptr());
		if (!node.isConstant()) {
//			JDDNode left = node.getElse();
//			JDDNode right = node.getThen();
//			JDD.Ref(left);
//			JDD.Ref(right);
			out.addAll(allNodes(node.getElse()));
			out.addAll(allNodes(node.getThen()));
		}
		return out;
	}
}
