package Sequenic.T2ext;

import java.util.HashSet;
import java.util.Iterator;

import Sequenic.T2.TrFile;
import Sequenic.T2.Msg.T2Exception;
import Sequenic.T2.Seq.Trace;
import Sequenic.T2ext.Analyzer.T2TraceFileCoverageAnalyzer;
import Sequenic.T2ext.Analyzer.T2TraceFileCoverageResult;

public class MarginalGenerator {
	
	private static final int numOfExtraTraces = 1000;
	
	private static final boolean minimizeOriginal = false;
	private static final boolean minimizeAdditions = true;
	
	/**
	 * @param args
	 */
	public static void main(String[] args)
	{
		try
		{
			main("Examples.ObsoleteTest");
		} catch (T2Exception e)
		{
			e.printStackTrace();
		}

	}
	
	public static void main(String cut) throws T2Exception 
	{
		
		final String origTrFileName = "../bin/"+cut+".tr";
		final String newTrFileName = cut+".tr";
		final String cfgsFileName = cut.replace('.', '/') + ".cfgs";
		
		// 1) load existing trace file, which was created for the old version of this program.

		TrFile origTrFile = TrFile.load(origTrFileName);
		
		// 2) Remove obsolete traces.
		
		int obs = 0;
		int origTotal = origTrFile.traces.size();
		
		Iterator<Trace> iter = origTrFile.traces.iterator();
		while(iter.hasNext()) {
			if(iter.next().isObsolete()) {
				iter.remove();
				obs++;
			} 
		}
				
		// 3) Execute remaining traces T and note coverage
		
		Main.instrument(cut);
		
		T2TraceFileCoverageAnalyzer analz = new T2TraceFileCoverageAnalyzer(origTrFile, cfgsFileName);
		T2TraceFileCoverageResult rez = analz.calculateCoverage();
		
//		MarginalSelector margSel = new MarginalSelector();
//		if(minimizeOriginal)
//			origTrFile.traces = rez.selectedTraces(margSel);
//		else 
//			rez.selectedTraces(margSel);
		
		int remaining = origTrFile.traces.size();
		int redundant = origTotal - obs - remaining;
		
		System.out.println("\nOriginal trace file obsolete/redundant/remaining % total: " + obs
				+"/"+redundant+"/"+remaining+" % "+origTotal+"\n");
		

		boolean modified;
		do {
    		// 4) Instruct T2 to generate X traces in new trace file T'
    		
    		Sequenic.T2.Main.main(new String[] {cut, "--nmax="+numOfExtraTraces+"0","--savegoodtr="+numOfExtraTraces,
    				"--bdomain=Sequenic.T2.BaseDomain0"}); 		// BaseDomain0 seems to be much better than the default BaseDomainSmall:
    		
    		// 5) Execute and note coverage of T'
    		
    		TrFile newTrFile = TrFile.load(newTrFileName);
    		validate_compatibility(origTrFile, newTrFile);

    		
    		analz = new T2TraceFileCoverageAnalyzer(newTrFile, cfgsFileName);
    		rez = analz.calculateCoverage();
    		
    		// 6) Add traces in T' that cover previously not observed paths to the set T
    		
    		int oldSize = origTrFile.traces.size();

    		modified = false; //for now, because I commented the below code.
//    		if(minimizeAdditions)
//    			modified = origTrFile.traces.addAll(rez.selectedTraces(margSel));
//    		else {
//    			modified = !rez.selectedTraces(margSel).isEmpty();
//    			if(modified)
//    				origTrFile.traces.addAll(newTrFile.traces);
//    		}
    		int newSize = origTrFile.traces.size();
    		
    		System.out.println("\nGenerated "+numOfExtraTraces+" extra, of which "+(newSize-oldSize)+" were added, old size/new size: "+oldSize+"/"+newSize+"\n");
    		
    		// 7) If T is modified, go to (4)

		} while(modified);
		
		// 8) Save T, finished.	
		origTrFile.save(newTrFileName);


	}

	
	private static void validate_compatibility(TrFile o, TrFile n) {
		if(!o.CUTname.equals(n.CUTname))
			throw new Error("CUT is not the same: "+o.CUTname+" vs. "+n.CUTname);
		if(!o.poolClassName.equals(n.poolClassName))
			throw new Error("Pool is not the same: "+o.poolClassName+" vs. "+n.poolClassName);
		HashSet<String> s = new HashSet<String>(o.classinvariantOwners);
		for(String i : n.classinvariantOwners)
			if(!s.contains(i))
				throw new Error("New classinvariant: "+i);
		s.removeAll(n.classinvariantOwners);
		if(!s.isEmpty())
			throw new Error("Missing classinvariant(s): "+s);
	}
}