package learner;

import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.PrintStream;
import java.util.Random;
import de.ls5.jlearn.algorithms.packs.ObservationPack;
import de.ls5.jlearn.equivalenceoracles.RandomWalkEquivalenceOracle;
import de.ls5.jlearn.equivalenceoracles.WMethodEquivalenceTest;
import de.ls5.jlearn.interfaces.Automaton;
import de.ls5.jlearn.interfaces.EquivalenceOracle;
import de.ls5.jlearn.interfaces.EquivalenceOracleOutput;
import de.ls5.jlearn.interfaces.Learner;
import de.ls5.jlearn.logging.LearnLog;
import de.ls5.jlearn.logging.LogLevel;
import de.ls5.jlearn.logging.PrintStreamLoggingAppender;
import de.ls5.jlearn.util.DotUtil;
import de.ls5.jlearn.interfaces.State;
import java.util.LinkedList;
import java.io.BufferedWriter;
import java.io.FileWriter;
import java.io.IOException;


public class Main {
	private static int maxNumTraces = 1000;
	private static int minTraceLength = 10;
	private static int maxTraceLength = 50;
	private static long seed = System.currentTimeMillis();
	private static String seedStr = Long.toString(seed);

	
	public static void main(String[] args) throws FileNotFoundException {
		
		// output learned statemachine as dot and pdf file :
	    File dotfile = new File("learnresult.dot");
	    File pdffile = new File("learnresult.pdf");
	
	    LearnLog.addAppender(new PrintStreamLoggingAppender(LogLevel.INFO, System.out));
		PrintStream fileStream = new PrintStream(new FileOutputStream("out.txt",false));
		PrintStream resultFileStream = new PrintStream(new FileOutputStream("result.txt",false));
		PrintStream statisticsFileStream = new PrintStream(new FileOutputStream("statistics.txt",false));
		System.setOut(fileStream);

		seed = 1298631432295l; seedStr = Long.toString(seed) + " - Set statically";
	//	seed = 1299071606560l; seedStr = Long.toString(seed) + " - Set statically";		//Palindrome/Repdigit3
	//	seed = 1299777356020l; seedStr = Long.toString(seed) + " - Set statically";
	//	seed = 1299777356020l; seedStr = Long.toString(seed) + " - Set statically";		//FWGC

		handleArgs(args);

		System.out.println("Maximum number of traces: " + maxNumTraces);
		System.out.println("Minimum length of traces: " + minTraceLength);
		System.out.println("Maximim length of traces: " + maxTraceLength);
		System.out.println("Seed: " + seedStr);
		Random random = new Random(seed);
		Mapper mapper = new Mapper();
		MembershipOracle memberOracle = new MembershipOracle(mapper);
		mapper.setMembershipOracle(memberOracle);
		EquivalenceOracle eqOracle;
		Learner learner = null;
		boolean done = false;
		int hypCounter = 0;
		
		long start = System.currentTimeMillis();

		while (!done) {
			eqOracle = new RandomWalkEquivalenceOracle(maxNumTraces, minTraceLength, maxTraceLength);
			eqOracle.setOracle(mapper);
			((RandomWalkEquivalenceOracle)eqOracle).setRandom(random);
			
			//eqOracle = new WMethodEquivalenceTest(8) ; 
			//eqOracle.setOracle(mapper);

			learner = new ObservationPack();
			learner.setOracle(memberOracle);

			learner.setAlphabet(mapper.generateInputAlphabet());
			mapper.generateOutputAlphabet();

			try {
				while (!done) {
					System.out.println("starting learning");
					System.out.println("");
					System.out.flush();
					System.err.flush();
					learner.learn();
					System.out.flush();
					System.err.flush();
					System.out.println("done learning");
					statisticsFileStream.println("Membership: " + memberOracle.getNumMembQueries());
					System.out.flush();
					Automaton hyp = learner.getResult();
					DotUtil.writeDot(hyp, new File("tmp-learnresult" + hypCounter++ + ".dot"));

					// search for counterexample
					System.out.println("starting equivalence query");
					System.out.flush();
					System.err.flush();
					EquivalenceOracleOutput o = eqOracle.findCounterExample(hyp);
					System.out.flush();
					System.err.flush();
					System.out.println("done equivalence query");
					statisticsFileStream.println("Equivalence: " + mapper.getNumEquivQueries());
					if (o == null) {
						done = true;
						continue;
					}
					statisticsFileStream.println("Sending CE to LearnLib.");
					System.out.println("Counter Example: " + o.getCounterExample().toString());
					System.out.flush();
					System.err.flush();
					learner.addCounterExample(o.getCounterExample(), o.getOracleOutput());
					System.out.flush();
					System.err.flush();
				}
			} catch (Exception ex) {
				statisticsFileStream.println("Exception!");
				System.out.println("Exception!");
				System.out.println("Seed: " + seedStr);
				System.err.println("Seed: " + seedStr);
				ex.printStackTrace();
				System.exit(-1);
			}
		}

		long end = System.currentTimeMillis();
		statisticsFileStream.println("Running time: " + (end-start) + "ms.");

        // final output to out.txt
		System.out.println("Seed: " + seedStr);
		System.err.println("Seed: " + seedStr);
		System.out.println("Done...");

		// print final abstraction to separate text file: result.txt :
		System.setOut(resultFileStream);

		// output needed for equivalence checking
		//  - learnresult.dot : learned statemachine
		//  - output.json  : abstraction,concrete alphabet,startstate
		Automaton learnedModel = learner.getResult();
		State startState=learnedModel.getStart();

		// output learned model with start state highlighted to dot file :
		// notes:
		//   - make start state the only highlighted state in dot file
		//   - learnlib makes highlighted state by setting attribute color='red' on state

    LinkedList<State> highlights=new LinkedList<State>();
		highlights.add(startState);
		BufferedWriter out=null;
		try {
			 out= new BufferedWriter(new FileWriter(dotfile));

		    DotUtil.writeDot(learnedModel, out, learnedModel.getAlphabet().size(), highlights, "");
		} catch (IOException ex) {
			 //Logger.getLogger(DotUtil.class.getName()).log(Level.SEVERE, null, ex);
		} finally {
			try {
			  out.close();
			} catch (IOException ex) {
			  //Logger.getLogger(DotUtil.class.getName()).log(Level.SEVERE, null, ex);
			}
		}

		// write pdf
		DotUtil.invokeDot(dotfile, "pdf", pdffile);
	}

	private static void handleArgs(String[] args) {
		for (int i = 0; i < args.length; i++) {
			if ("--max-traces".equals(args[i])) {
				if (i == args.length - 1) {
					System.err.println("Missing argument for --max-traces.");
					printUsage();
					System.exit(-1);
				}
				try {
					maxNumTraces = new Integer(args[++i]);
				} catch (NumberFormatException ex) {
					System.err.println("Error parsing argument for --max-traces. Must be integer. " + args[i]);
					System.exit(-1);
				}
			}
			if ("--min-trace-length".equals(args[i])) {
				if (i == args.length - 1) {
					System.err.println("Missing argument for --min-trace-length.");
					printUsage();
					System.exit(-1);
				}
				try {
					minTraceLength = new Integer(args[++i]);
				} catch (NumberFormatException ex) {
					System.err.println("Error parsing argument for --min-trace-length. Must be integer. " + args[i]);
					System.exit(-1);
				}
			}
			if ("--max-trace-length".equals(args[i])) {
				if (i == args.length - 1) {
					System.err.println("Missing argument for --max-trace-length.");
					printUsage();
					System.exit(-1);
				}
				try {
					maxTraceLength = new Integer(args[++i]);
				} catch (NumberFormatException ex) {
					System.err.println("Error parsing argument for --max-trace-length. Must be integer. " + args[i]);
					System.exit(-1);
				}
			}
			if ("--seed".equals(args[i])) {
				if (i == args.length - 1) {
					System.err.println("Missing argument for --min-trace-length.");
					printUsage();
					System.exit(-1);
				}
				try {
					seed = new Integer(args[++i]);
					seedStr = Long.toString(seed);
				} catch (NumberFormatException ex) {
					System.err.println("Error parsing argument for --seed. Must be integer. " + args[i]);
					System.exit(-1);
				}
			}
		}
	}

	public static void printUsage() {
		System.out.println(" --max-traces       - Maximum number of traces to run during equivalence testing.");
		System.out.println(" --min-trace-length - Minimum length of traces during equivalence query.");
		System.out.println(" --max-trace-length - Maximum length of traces during equivalence query.");
		System.out.println(" --seed             - Seed to use for random number generator.");
	}
}
