/*
 * Copyright 2009 Wishnu Prasetya.
 *
 * This file is part of T2.
 * T2 is free software; you can redistribute it and/or modify it under
 * the terms of the GNU General Public License (GPL) as published by the
 * Free Software Foundation; either version 3 of the License, or any
 * later version.
 * 
 * T2 is distributed in the hope that it will be useful, but WITHOUT ANY
 * WARRANTY; without even the implied warranty of MERCHANTABILITY or
 * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
 * for more details.
 *
 * A copy of the GNU General Public License can be found in T2 distribution.
 * If it is missing, see http://www.gnu.org/licenses.
 */

package Sequenic.T2ext.Analyzer;

import Sequenic.T2ext.Instrumenter.*;
import Sequenic.T2.*;
import Sequenic.T2.Engines.Util;
import Sequenic.T2.Seq.*;

import java.util.* ;
import java.lang.reflect.*;

/**
 * 
 * @author Wishnu Prasetya
 * @author Orgininal code by Maaike Gerittsen
 */
public class T2TraceFileCoverageAnalyzer {

	/**
	 * This holds the traces to run and analyze, along with some other
	 * information. It is also a representation of T2's save file.
	 */
	public TrFile tracefile ;

	/**
	 * The target class.
	 */
	Class C ;
	
	/**
	 * The used object pool.
	 */
	Pool pool ;
	
	List<Method> classinvs ;
	
	// ReportersPool  T2reporters ; no ... don't report; that's not a task of coverage analyzer
	
	CoverageAnalyzer COVanalyzer ;
	
	public boolean debug = false ;
	
	
	public T2TraceFileCoverageAnalyzer(TrFile trfile, String cfgbunchFile){
		tracefile = trfile ;
		COVanalyzer = new CoverageAnalyzer(cfgbunchFile) ;
		this.initializeDerivedData() ;	
	}

	public T2TraceFileCoverageAnalyzer(String trfile, String cfgbunchFile){
		try {
			tracefile = TrFile.load(trfile) ;
		}
		catch (Sequenic.T2.Msg.T2Exception e) { throw new Error(e) ; }
		
		COVanalyzer = new CoverageAnalyzer(cfgbunchFile) ;
		this.initializeDerivedData() ;	
	}

	
	private void initializeDerivedData() {
		try {
			C = Class.forName(tracefile.CUTname) ;
		} catch (ClassNotFoundException e) {
			throw new Error("## Fail to obtain the target class " + tracefile.CUTname + ".",e) ;
		}
		pool = (Pool) Util.mkAnInstance(tracefile.poolClassName) ;
		if (pool==null)
			throw new Error("## Fail to instantiate the pool " 
					+ tracefile.poolClassName
					+ ".") ;
		
		// Recovering the class invs:
		classinvs = new LinkedList<Method>();
		try {
			for (String cowner : tracefile.classinvariantOwners) {
				classinvs.add(Util.getClassINV(Class.forName(cowner)));
			}
		} 
		catch (Exception e) {
			throw new Error("## Fail to load the class invariant(s).", e);
		}
	}
	
	/**
	 * Given a T2-trace, this method will execute the trace and calculate the
	 * resulting coverage. It returns the coverage delivered by the trace as
	 * a whole; and also pass-out information about the coverage of each step. 
	 * 
	 * The execution of the trace is stopped if it makes a violation. If the trace
	 * is marked as diverging, its last step will not be executed.
	 * 
	 * @param coverageOfSteps Output parameter to pass-out information on the coverage 
	 * per step. This is a list Z such that Z(0) is the coverage of the trace creation
	 * step, Z(i+1) is the coverage of step trace.trace(i). If trace.trace(i) is a field
	 * update then its Z(i+1) is null.
	 */
	
	void analyzeTrace(Trace trace,
			LinkedList<Pair<Long,Trace>>   runIdTableLevel1,
			LinkedList<Pair<Long,Integer>> runIdTableLevel2) {
		
		// initialize various infos:
		pool.reset();
	    TraceExecInfo info = new TraceExecInfo(trace) ;
	    Object targetObj = null;
	    int stepNr = 0 ;
	    boolean ok = true ;
	    
	    // Do this to keep track which runids belong to which trace
	    runIdTableLevel1.add(new Pair<Long,Trace>(Sensor.currentRunId(),trace)) ;
	    	    
	    
	    // Creation step:
	    // Do this to keep track which runids belong to which step
	    runIdTableLevel2.add(new Pair<Long,Integer>(Sensor.currentRunId(),stepNr)) ;
	    ok = info.update_with_step(trace.creation.MkTargetObject(C,pool,classinvs),stepNr) ;
	    stepNr++ ;
	    // Creation step-done
	    
	    if (ok) { 
	    
	    	// Creation successful, continue with the steps:
	    
	    	targetObj = pool.get(trace.indexOfTargetObj) ; 
	    
	    	for (TraceStep step : trace.trace) {
            
	    		if (trace.diverging && step == trace.trace.getLast()) break ;

	    	    // Do this to keep track which runids belong to which step
	    		//if (step instanceof CALL_METHOD) {
	    		runIdTableLevel2.add(new Pair<Long,Integer>(Sensor.currentRunId(),stepNr)) ;
	    		//}
	    		
	    		ok = info.update_with_step(step.exec(C,pool,targetObj,stepNr,classinvs),stepNr) ;
	    		
	    		stepNr++ ;
	    		if (!ok) break;
	    	}
	    }
	    // DONE
	}
	
	
	/**
	 * Calculate the coverage measurement of all traces in the tracefile.
	 */
	public T2TraceFileCoverageResult calculateCoverage() {
		
		T2TraceFileCoverageResult result = new T2TraceFileCoverageResult() ;
		result.trfile = tracefile ;
		
		// This should be turned off if we plan to do concurrent monitoring:
	    Sensor.resetSensor() ;

		for (Trace tr : tracefile.traces) {
			 analyzeTrace(tr,result.runIdTableLevel1,result.runIdTableLevel2) ;
		 }
		 // Calculate total coverage:
		result.observedpaths = Sensor.getObservedPaths() ; 
		result.totCoverage = COVanalyzer.calculateCoverage() ;
		 
		if (debug) result.simplePrint() ;
		 
		return result ;
	}

	public Class getC() { return C;	}	
	
	public Pool getPool() { return pool;	}	
	
	public List<Method> getClassinvs() { return classinvs;	}	
	
	public CoverageAnalyzer getCOVanalyzer() { return COVanalyzer;	}

}