package heuristics;

import java.io.*;

import prism.*;


public class Experiments
{
	public static void main(String[] args) throws Exception{
		File modules = new File("tests/heuristics/experiments/modules.txt");
		File properties = new File("tests/heuristics/experiments/properties.txt");
		File constants = new File("tests/heuristics/experiments/constants.txt");
		BufferedReader modulesReader = new BufferedReader(new FileReader(modules));
		BufferedReader propertiesReader = new BufferedReader(new FileReader(properties));
		BufferedReader constantsReader = new BufferedReader(new FileReader(constants));
		double termCritParam = 1e-6;
		String module;
		String property;
		String constant;
		boolean allSame = true;
		while (((module = modulesReader.readLine()) != null) && ((property = propertiesReader.readLine()) != null) && ((constant = constantsReader.readLine()) != null)) {
			String[] props = property.split(" ");
			String[] heuristic = {module,props[0],props[1],props[2],"-brtdp_bscc:heuristic=BRTDP,verbose","-const",constant};
			for (int i= 0; i < heuristic.length; i++) {
				System.out.print(heuristic[i] +" ");
			}
			String[] prism = {module,props[0],props[1],props[2],"-const",constant};
//			Result heurResult = PrismCL.main(heuristic);
//			Result prismResult = PrismCL.main(prism);
			Result heurResult = null;
			Result prismResult = null;
			if (!(PrismUtils.doublesAreClose(Double.valueOf(heurResult.toString()), Double.valueOf(prismResult.toString()), termCritParam*2, false))) {
				System.out.println("Results don't match:\nHeuristic Result: " + heurResult + "\nPrism Result: " + prismResult);
				allSame = false;
			}
			System.out.println("Still all correct: " + allSame);
		}
		modulesReader.close();
		propertiesReader.close();
		constantsReader.close();
	}
}
