/*
 * Copyright 2007 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.T2.Seq;

import java.io.IOException;
import java.io.ObjectInput;
import java.io.ObjectOutput;
import java.io.Serializable;
import java.lang.reflect.Method;
import java.util.ArrayDeque;
import java.util.Collections;
import java.util.Deque;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;

import Sequenic.T2.Pool;
import Sequenic.T2.Coverage.BasicPath;

/**
 * A Trace is a meta representation of test, which is a sequence of test-steps.
 * A test-step is for example updating a field of a target object, or calling
 * one of its methods. Being a meta representation means that a Trace in itself
 * does not cause the test to execute. To execute it, we have to call a special
 * method that will interpret the trace, and turns it to an execution. The
 * advantage of having a meta representation of a test is that we can do things
 * with it, like saving it, reloading it, changing it, and so on.
 * See also the doc of the {@link Sequenic.T2 Sequenic.T2 package}. 
 *
 * <p>To be more precise, a trace consists of a <u>creation step</u>, that creates a
 * target object (the object on which the test will be applied on), and a sequence of subsequent {@link
 * Sequenic.T2.Trace.TraceStep TraceStep objects}. The creation step is a
 * {@link Sequenic.T2.Trace.MkValStep MkVal object}. A
 * MkVal object is also a meta representation, which is ínterpreted can create an 
 * object, whereas a trace step is
 * used to apply side effects on the target object.  A trace step may
 * also consist of MkVal steps, e.g. when it needs to create objects
 * to pass as parameters to a method.
 */
public class Trace implements Serializable{
	
	public Trace() 
	{
		this(null,new ArrayDeque<TraceStep>(), -1, false, false, Collections.EMPTY_SET);
	}
	
	private Trace(MkValStep c, Deque<TraceStep> t, int iOTO, boolean vio, boolean div, Set<BasicPath> cov)
	{
		creation = c;
		trace = t;
		indexOfTargetObj = iOTO;
		violating = vio;
		diverging = div;
		coverage = cov;
	}
	
	/**
     * The creation step that starts this execution trace.
     */
    transient public MkValStep creation;
    /**
     * The sequence of steps belonging to this trace.
     */
    transient public Deque<TraceStep> trace;
    /**
     * Implicitly there is a pool associated to a trace. The pool
     * is used to keep track of object generated when the trace
     * is generated. This field gives the index of the target object
     * in this pool.
     */
    public int indexOfTargetObj;
    
    /**
     * Is set to true when this trace is marked a violating.
     */
    public boolean violating;
    
    /**
     * Is set to true when this trace is marked as diverging.
     */
    public boolean diverging;
    
    /**
     * We maintain the invariant that coverage is never null.
     */
   	private Set<BasicPath> coverage;

    
    /**
     * Used to classify different kind of traces, e.g. to distinguish
     * violating and non-violating traces. The purpose of this field is
     * mainly to quickly filter traces without having to execute them.
     */
    //public String classification = null;
    /**
     * Currently these are the only classifications :)
     */
    //public static final String VIOLATING_TRACE = "VIOLATING TRACE";
    //public static final String DIVERGING_TRACE = "POSSIBLY NON TERMINATING TRACE";


    /**
     * This method will try to execute *all* steps in this trace, even if
     * it is marked as DIVERGING. The execution is stopped when a violation
     * is detected. An trace execution report will be returned, from which
     * it can be inferred if e.g. the execution finds a new violation,
     * or if a violation that was found in the execution producing the trace
     * now disappears.
     * 
     * <p> Particularly with divergence, this method in itself does not 
     * implement a time out mechanism or such. So it cannot force a diverging
     * step to stop. Such a mechanism is assumed to be implemented in either
     * the step execution system, or on the external framework that uses this
     * method.
     * 
     * <p>If no such stopping mechanism is present, then one should take into
     * account that this method may thus diverge.
     * 
     * @param pool Pass here the same pool as used to produce this
     * execution trace.
     * 
     * @param printIntermediateStepsOption When true (default) report will 
     * include the report of intermediate steps in a trace. Else only the 
     * creation of the target object and the last two steps will be reported.
     */
    public TraceExecInfo execAllSteps(Class CUT, 
            Pool pool, 
            List<Method> classinvs, 
            boolean printIntermediateStepsOption,
            ReportersPool reporters) {

        boolean produceReport = reporters != null;

        pool.reset();
        TraceExecInfo info = new TraceExecInfo(this) ;
        Object targetObj = null;
        int stepNr = 0 ;
        boolean ok = true ;
        
        //System.out.println("***"+ Show.show(creation)) ;
        if (produceReport) reporters.reportTraceBegin();
        
        ok = info.update_with_step(creation.MkTargetObject(CUT, pool, classinvs, reporters), stepNr) ;
        
        //System.out.println(">>> " + ok + info.new_violating_flag + info.lastStepResult.isAsmOrReqViolating()) ;
        
        stepNr++;

        if (ok) { // no violation found

            targetObj = pool.get(indexOfTargetObj) ;
            assert (targetObj == info.lastStepResult.targetObj) ;
            
            for (TraceStep step : trace) {
                
                //System.out.println(">>> " + trace.size()) ;
                
                if (!printIntermediateStepsOption && stepNr <= trace.size() - 2) {
                    
                    ok = info.update_with_step(step.exec(CUT, pool, targetObj, stepNr, classinvs, ReportersPool.NULLreporter),
                            stepNr) ;
                } else {
                    ok = info.update_with_step(step.exec(CUT, pool, targetObj, stepNr, classinvs, reporters),
                            stepNr) ;
                }
                stepNr++ ;
                if (!ok) break;
            }
        }

        if (produceReport) {
            reporters.reportTraceEnd();
        }
        return info;
    }

    /**
     * As either execAllSteps or execAllStepsButLastDiv, depending on the boolean
     * flag given.
     */
    public TraceExecInfo exec(Class CUT, 
            Pool pool, 
            List<Method> classinvs,
            boolean assumeLastStepDiverging,
            boolean printIntermediateStepsOption, 
            ReportersPool reporters
            ) {
        
        if (assumeLastStepDiverging)
            return execAllStepsButLastDiv(CUT,pool,classinvs,printIntermediateStepsOption,reporters) ;
        else
            return execAllSteps (CUT,pool,classinvs,printIntermediateStepsOption,reporters) ;
    }
    
    public TraceStep getStep(int index)
    {
    	if(index<0 || index>=trace.size())
    		throw new IndexOutOfBoundsException();
    	Iterator<TraceStep> iter = trace.iterator();
    	while(index--!=0)
    		iter.next();
    	return iter.next();
    }
    
    /**
     * This is as execAllSteps. BUT the last step in the trace is ASSUMED
     * to be diverging, and will not be executed. If no violation up to
     * this last-step, this method will provide a meta-reporting of the
     * last-step, and just assume that it is diverging (which will be 
     * reflected in the info it returns).
     */
    public TraceExecInfo execAllStepsButLastDiv(Class CUT,
            Pool pool, 
            List<Method> classinvs, 
            boolean printIntermediateStepsOption, 
            ReportersPool reporters) {
        
        assert (creation != null) ;
        
        TraceExecInfo info = null ;
        int traceLength = this.trace.size() + 1 ; 
               
        METARUN laststep = null ;
        
        if (trace.size()>0) {
        	// remove the last step first, then execute:
            laststep = trace.removeLast() ;
            info = execAllSteps(CUT, pool,classinvs,printIntermediateStepsOption,reporters) ;
            // putting back the last-step:
            trace.add((TraceStep) laststep) ;
            if (info.found_new_violation()) return info ;
        }
        else laststep = creation ;
        
        // No new violation found; now only the last step remains.
        
        // We don't execute the last step, we just
        // make a meta-report of it, and ASSUMING it would be diverging:
        Object targetObj = null ;
        if (indexOfTargetObj >= 0) targetObj = pool.get(indexOfTargetObj) ;
        info.lastStepResult = new ExecResult(CUT,laststep,targetObj) ;
        info.lastStepResult.possiblyDiverging = true ;
        info.new_diverging_flag = true  ;
        info.violation_location = traceLength - 1 ;
        if (reporters!=null) reporters.reportStep(info.lastStepResult,0) ;
        return info ;
    }
     
    public boolean isObsolete() {
    	if(creation.isObsolete())
    		return true;
    	for(TraceStep ts : trace)
    	{
    		if(ts.isObsolete())
    			return true;
    	}
    	return false;
    }
        
	public Set<BasicPath> coverage()
	{
		return coverage;
	}

	public void setCoverage(Set<BasicPath> coverage)
	{
		if(coverage==null)
			throw new NullPointerException("Coverage can not be null");
		this.coverage = coverage;
	}
	
//	/** 
//	 *  If this trace does not cover any modification-traversing paths
//	 *  then the coverage data is cleared and the method returns true.
//	 *  
//	 *  Otherwise the coverage data is updated and this method returns false.
//	 * 
//	 * @param selector
//	 * @return
//	 */
//	public boolean updateCoverageAndSelect(BasicPath.Selector selector)
//	{
//		HashSet<BasicPath> newCoverage = new HashSet<BasicPath>(coverage.size());
//		BasicPath newBP;
//		for(BasicPath bp : coverage) 
//		{
//			newBP = bp.cachedSelectAndUpdate(selector);
//			if(newBP==null) 
//			{
//				//bp is modification-traversing: clear coverage, return true
//				coverage = Collections.emptySet();
//				return true;
//			} 
//			else
//				//bp is not modification-traversing, update coverage tentatively, continue
//				newCoverage.add(newBP);
//		}
//		//No bp was modification-traversing, update coverage definitely, return false
//		coverage = newCoverage;
//		return false;
//	}   	
//    


    /*=================================================================
     *====					SERIALIZATION 						======= 
     *================================================================= 
     *
     * There are two ways to serialize Traces.
     * Choose which to use in the serialization routines of TraceFile.
     *
     */
    
    /*  ========= METHOD 1: Conventional Serialization ================
     * 
     * This implements Serializable and only deviates where necessary.
     */

	private static final long serialVersionUID = -14045306304279703L;

    /** These methods are for Serialization, because TraceSteps and MkValSteps are no longer Serializable.
     * Doing this reduces the storage size of a Trace by 50% and allows us to (de)serialize Obsolete traces.
     * 
     */
    private void writeObject(java.io.ObjectOutputStream out)
    throws IOException{
    	out.defaultWriteObject();
    	Externalize_MkValStep.write(creation,out);
    	out.writeInt(trace.size());
    	for(TraceStep ts : trace) {
    		ts.write(out);
    	}
    }
    
    private void readObject(java.io.ObjectInputStream in)
    throws IOException, ClassNotFoundException{
    	in.defaultReadObject();
    	creation = Externalize_MkValStep.read(in);
    	int size = in.readInt();
    	trace = new LinkedList<TraceStep>();
    	while(size-->0)
    		trace.add( TraceStep.read(in));
    }

    /*  ///// END METHOD 1 
     * 
     * ========= METHOD 2: Manual Serialization ================
     * 
     * A custom, manual serialization routine that is harder to maintain, but uses less storage space.
     * It should also be faster.
     */    
    
	
    private static final int maskDiverging = 1;
    private static final int maskViolating = 2;
    private static final int maskCreationIsNull = 4;
    private static final int maskTraceIsNull = 8;
    private static final int maskUseInt = 32;
    private static final int maxUnsignedShort = 65535;
    
    public static final int endOfStream = 16;

    /**
     * A custom, manual serialization routine that is harder to maintain, but uses less storage space.
     * It should also be faster.
     */
   	public void alternativeSerializationWrite(ObjectOutput out) throws IOException
	{
		int mask = 0;
		int covSize = -1;
		int traceSize = -1;
		boolean useInt = false;
		if(diverging) mask |= maskDiverging;
		if(violating) mask |= maskViolating;
		if(creation == null) mask |= maskCreationIsNull;
		
		if(trace == null) 
			mask |= maskTraceIsNull;       
		else if(maxUnsignedShort < (traceSize=trace.size())) 
			useInt = true;
		else if(maxUnsignedShort < (covSize=coverage.size())) 
			useInt = true;
		
		if(useInt || indexOfTargetObj > Short.MAX_VALUE || indexOfTargetObj < Short.MIN_VALUE)
			mask |= maskUseInt;
		
		out.write(mask);
		
		if(useInt)
			out.writeInt(indexOfTargetObj);
		else 
			out.writeShort(indexOfTargetObj);
		
		if(creation!=null)
			Externalize_MkValStep.write(creation, out);
		
		if(covSize>=0) {
			if(useInt)
				out.writeInt(covSize);
			else 
				out.writeShort(covSize);
			for(BasicPath bp : coverage)
				out.writeObject(bp);
		}
		
		if(traceSize >= 0) {
			if(useInt)
				out.writeInt(traceSize);
			else 
				out.writeShort(traceSize);
			for(TraceStep ts : trace)
				ts.write(out);
		}
	}

	
	/** Dual of the 'write' method.
	 */
	public static Trace alternativeSerializationRead(ObjectInput in) throws IOException,
			ClassNotFoundException
	{
		final int mask = in.read();	
		if(mask==endOfStream)
			return null;
		final boolean useInt = (mask & maskUseInt)!=0;
		
		final int iOTO = useInt ? in.readInt() : in.readShort();
		
		final MkValStep c;
		
		if((mask & maskCreationIsNull) != 0) 
			c = null;
		else 
			c = Externalize_MkValStep.read(in);

		final Set<BasicPath> cov;
		//coverage
		{
    		int size = useInt ? in.readInt() : in.readUnsignedShort();    		
    		if(size>1) 
    		{
    			cov = new HashSet<BasicPath>(2*size); 
        		while(size-->0)
        			cov.add((BasicPath) in.readObject());
    		} else if(size==0){
    			cov = Collections.emptySet();
    		} else {
    			cov = Collections.singleton((BasicPath)in.readObject()); 
    		}
		}
		
		final Deque<TraceStep> t;
		
		if((mask & maskTraceIsNull) != 0) {
			t = null;
		}
		else {
			int size = useInt ? in.readInt() : in.readShort();
			t = new ArrayDeque<TraceStep>(size);
			while(size-->0)
				t.add(TraceStep.read(in));
		}
		return new Trace(c,t,iOTO,(mask & maskViolating)!=0,(mask & maskDiverging)!=0,cov);

	}

}