/*
 * 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.Engines;

import Sequenic.T2.*;
import Sequenic.T2.Msg.*;
import Sequenic.T2.Seq.*;
import java.util.*;
import java.lang.reflect.*;

/**
 * Provide a facility to replay saved traces. This can be used to support
 * regression.
 */
public class Replay extends EngineWithTimeOut {

    /**
     * The maximumum show depth. Default is 5.
     */
    public int maxShowDepth = 5;
    /**
     * The name of the file from where the tests will be loaded.
     * Default is null, in which case that the name of this file
     * is assumed to be C.tr.
     */
    public String saveFile = null;
    /**
     * Reporters to report the execution of the traces.
     */
    public ReportersPool reporters = null;
    /**
     * If false will not print intermediated test steps. Default is true.
     */
    public boolean printIntermediateStepsOption = true;
    /**
     * Set to true if you only want to regress over tests which were
     * violating. Default is false.
     */
    public boolean replayOnlyViolatingTraces = false;
    /**
     * Will reply up to this many traces. If negative then there is no
     * maximum. Default: -1.
     */
    public int replayUpToThisMany = -1;
    
    /**
     * Will stop replay after it finds this much violations. If negative
     * then there is no maximum. Default: -1.
     */
    public int stopAfterThisManyViolations = -1 ;
    
    /**
     * Replay random traces. Will ignore the replayOnlyViolatingTraces 
     * flag. Default is false. 
     */
    public boolean replayRandomTraces = false;
    
    /**
     * If true will assume the last step of traces marked as diverging
     * to be non-terminating. This last step will then not be executed.
     * Default is false.
     */
    public boolean dont_execute_last_diverging_step = false ;
        
    
    /**
     * This will hold the traces loaded from a save-file.
     */
    public TrFile loadedTraces;
    public List<Method> classinvs;
    public Pool pool = null;
    public Class CUT = null;
    public TraceSet selected = null;
    
    /**
     * This will hold the result of running the replay.
     */
     protected TraceSetExecInfo replayresult ;
    
    /**
     * Creat a replay object with a default configuration. You may need
     * to first reconfigure it. Furthermore, the traces are not yet loaded.
     * 
     * @see Sequenic.T2.Engines.Replay#load 
     */
    public Replay(String savefile) { 
        saveFile = savefile ;
        StdReporter stdR = new StdReporter();
        reporters = new ReportersPool();
        reporters.reporters.add(stdR);
        reporters.setShowDepth(maxShowDepth);
    }

    /**
     * Make an instance of the class C whose name is given. The assumption 
     * is that C has a constructor of signature C(). Just returns null is
     * it fails to do it.
     */
    public static Object mkAnInstance(String cname) {
        try {
            Class C = Class.forName(cname);
            Class[] paramTypes = new Class[0];
            Constructor con = C.getConstructor(paramTypes);
            Object[] params = new Object[0];
            Object result = con.newInstance(params);
            return result;
        } catch (Exception e) {
            return null;
        }
    }

    /**
     * To actually load the saved traces into this replay object.
     */
    public void load() throws T2Exception {

        // Load saved traces:
        loadedTraces = TrFile.load(saveFile);

        // Identifying CUT:
        CUT = null;
        try {
            CUT = Class.forName(loadedTraces.CUTname);
        } catch (ClassNotFoundException e) {
            throw new T2Error("Fail to obtain the target class " + loadedTraces.CUTname + ".");
        }

        // Identifying the used pool:
        pool = (Pool) mkAnInstance(loadedTraces.poolClassName);
        if (pool == null) {
            throw new T2Error("Fail to instantiate the pool " + loadedTraces.poolClassName + ".");
        // Recovering the class invs:
        }
        classinvs = new LinkedList<Method>();
        try {
            for (String cowner : loadedTraces.classinvariantOwners) {
                classinvs.add(Util.getClassINV(Class.forName(cowner)));
            }
        } catch (Exception e) {
            throw new T2Error("Fail to load the class invariant(s).");
        }
        // Apply the innitial selection (according to the configuration
        // now) :
        selectTraces();
    }

    /**
     * Will take out selected traces according to the configuration.
     */
    public void selectTraces() {

        selected = new TraceSet(CUT, pool, new LinkedList<Sequenic.T2.Seq.Trace>());

        // The case when we just include all loaded traces (so none is
        // filtered away) :
        if (!replayOnlyViolatingTraces 
                && 
                (replayUpToThisMany<0 || loadedTraces.traces.size() <= replayUpToThisMany)) {
            selected.traces = loadedTraces.traces;
            //System.out.println("Boo!") ;
            return;
        }

        // Taking only violating traces:
        int i = 0;
        if (replayOnlyViolatingTraces && !replayRandomTraces) {
            for (Sequenic.T2.Seq.Trace tau : loadedTraces.traces) {
                if (replayUpToThisMany>=0 && i >= replayUpToThisMany) {
                    break;
                }
                if (tau.violating) selected.traces.add(tau);
                i++;
            }
            return;
        }

        // Taking either the first N traces, or randomly N traces:    

        Random rnd = new Random();
        //assert replayUpToThisMany>=0 ;
        float prob = ((float) replayUpToThisMany) / ((float) loadedTraces.traces.size());

        i = 0;
        for (Sequenic.T2.Seq.Trace tau : loadedTraces.traces) {
            if (i >= replayUpToThisMany) {
                break;
            }
            if (!replayRandomTraces || rnd.nextFloat() <= prob) {
                selected.traces.add(tau);
            }
            i++;
        }


    }

    /**
     * This is the main-loop of Replay-engine. It will executes the
     * {@link selected selected traces}.
     */
    public void mainloop() {
        reporters.reportTestSetBegin(CUT, Message.GREET) ;
        replayresult = selected.exec(classinvs, 
                dont_execute_last_diverging_step,
                printIntermediateStepsOption, 
                stopAfterThisManyViolations, 
                reporters);
        reporters.reportTestSetEnd(CUT, replayresult,"");
    }
    

}