/*
 * 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 java.lang.reflect.Constructor;
import java.lang.reflect.Field;
import java.lang.reflect.Method;
import java.lang.reflect.Modifier;
import java.security.SecureRandom;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.Random;
import java.util.logging.Logger;

import Sequenic.T2.BaseDomain;
import Sequenic.T2.BaseDomainSmall;
import Sequenic.T2.InterfaceMap;
import Sequenic.T2.InterfaceMap0;
import Sequenic.T2.OBJECT;
import Sequenic.T2.Pool;
import Sequenic.T2.TrFile;
import Sequenic.T2.DataGen.RandomBool;
import Sequenic.T2.DataGen.RandomBoolUniform;
import Sequenic.T2.DataGen.RandomInt;
import Sequenic.T2.DataGen.RandomIntUniform;
import Sequenic.T2.Msg.Message;
import Sequenic.T2.Msg.T2Error;
import Sequenic.T2.Msg.T2Exception;
import Sequenic.T2.Seq.CALL_METHOD;
import Sequenic.T2.Seq.CONST;
import Sequenic.T2.Seq.CREATE_COLLECTION_LIKE;
import Sequenic.T2.Seq.CREATE_OBJECT;
import Sequenic.T2.Seq.ExecResult;
import Sequenic.T2.Seq.MkValStep;
import Sequenic.T2.Seq.REF;
import Sequenic.T2.Seq.ReportersPool;
import Sequenic.T2.Seq.StdReporter;
import Sequenic.T2.Seq.TraceSet;
import Sequenic.T2.Seq.TraceSetExecInfo;
import Sequenic.T2.Seq.TraceStep;
import Sequenic.T2.Seq.UPDATE_FIELD;

/**
 * A base test engine. This engine randomly generates (and executes) traces.
 */
public class BaseEngine extends EngineWithTimeOut {

    /**
     * The class under the test.
     */
    public Class CUT = null;
    /**
     * The object pool used by the engine.
     */
    public Pool pool = new Pool();
    /**
     * Specify a maximum on the numbers of total execution steps
     * generated by the engine. Default is 500.
     */
    public int maxNumOfSteps = 500;
    /**
     * Specify a maximum on the length of each execution. Default is
     * 4.
     */
    public int maxExecLength = 4;
    
    /**
     * Search mode. The default is 0, meaning that it is turned off. When 
     * it is on, the engine will behave differently. When a sequence fails 
     * due to violation to a pre-condtion or other kind of assumptive 
     * conditions, the same sequence will be retried again; except that we
     * will try a different last step. Of course this may fail again. This
     * all will be iterated up to the specified number (as specified by
     * this variable). If it still fails then the entire sequence is abandoned.
     */
    public int searchMode = 0 ;
    
    /**
     * The engine should stop if the number of violations found
     * reaches maxNumViolations. Default is 1.
     */
    public int maxNumViolations = 1;
    /**
     * Specify which fields and methods are to be included in the testing 
     * (e.g. whether to include protected methods etc).
     */
    public AccessOption accessOption = null;
    /**
     * The base domain used by the engine. Default is 
     * {@link Sequenic.T2.BaseDomainSmall BaseDomainSmall}.
     */
    public BaseDomain baseDomain = new BaseDomainSmall();
    /**
     * A random generator.
     */
    public Random rnd = new SecureRandom();
    /**
     * Specify a maximum on the length of every generated mkVal
     * sequence. Default is 4.
     */
    public int maxMkValSeqDepth = 4;
    /**
     * If set true then the engine will a custom "trace-director" method 
     * provided by CUT to drive its trace generation.
     */
    public boolean useCustomTraceDirector = false;
    /**
     * The probability to do field update rather than method call.
     * The default is 10%, uniformly distributed.
     */
    public RandomBool chooseFieldUpdateProb = new RandomBoolUniform(0.1);
    /**
     * When trying to generate an instance of C, and one cannot be
     * found in the base domain, and the engine decided not to look in
     * the pool (hence generating a fresh one), this is the
     * probability of generating null. The default is 10%, uniformly
     * distributed.
     */
    public RandomBool generateNullProb = new RandomBoolUniform(0.1);
    /**
     * When an object has to be generated, and it cannot be generated
     * from the engine's base domain, the engine decides whether
     * to try to look in the pool, or to generate a fresh one. This is
     * the probability that the engine chooses to look in the pool. Note
     * that the decision is taken without first looking whether a suitable
     * object can actually be found in the pool (in favor for speed). So,
     * after decising to look in the pool the engine may still find nothing
     * there, in which case it will then default to generating a fresh object.
     * 
     * <p>The default probability is 70%, uniformly distributed. 
     */
    public RandomBool pickTargetObjFromPoolProb = new RandomBoolUniform(0.7);
    /**
     * The probability for chosing to pass the target object as a
     * parameter rather than as a receiver object. Default is 40%,
     * uniformly distributed. 
     */
    public RandomBool passTObjAsParamProb = new RandomBoolUniform(0.4);
    /**
     * The probability on the size of the collection and array (along each dimension)
     * generated by the engine. The default is it is between [0..5), uniformly
     * distributed. So the default max-size is 4.
     */
    public RandomInt maxArrayLengthProb = new RandomIntUniform(0, 5);
    /**
     * Maximum depth when showing objects in reporting. That is,
     * subobjects at deeper than this depth will not be shown. The
     * default is 5.
     */
    public int maxShowDepth = 5;
    /**
     * When false will hide intermediate steps of each shown trace.
     * Default is true.
     */
    public boolean showIntermediateSteps = true;
    /**
     * If false will not show the violating traces (only global statistics
     * will be shown). Default is true.
     */
    public boolean showViolatingTraces = true;
    /**
     * Save up to this many non-violating traces from the set of generated traces.
     * Default is 0.
     */
    public int saveThisMany = 0;
    /**
     * The name/path of the file to save the traces. Default is null, which means
     * the traces will be saved to the standard name, which is CUT.tr.
     */
    public String nameOfSaveFile = null;
    /**
     * Reporters pool to report e.g. violating traces.
     */
    public ReportersPool reporters = null;
    /**
     * A sequence generator. The default is random based. We can have a different
     * generator and 'plug' it to this variable.
     */
    public BaseEngineSeqGenerator seqGenerator = new RandomSequenceGenerator(this);
    /**
     * An interface map used by the engine. The map lists interfaces,
     * and for each possible concrete classes (currently just one)
     * that implement it. When the engine needs to generate an
     * instance of an interface I, it first looks it up in this
     * interface map. If the map says it has implementations, one
     * (say, C) will be selected and the engine will then proceed by
     * trying to generate an instance of C instead.
     * 
     * <p>Default is {@link Sequenic.T2.InterfaceMap0 InterfaceMap0}.
     */
    public InterfaceMap interfaceMap = new InterfaceMap0();
    /** 
     * The list of CUT's constructors within the testing scope.
     */
    public List<Constructor> consIPs;
    /**
     * The list of CUT's fields within the testing scope.
     */
    public List<Field> fieldsIPs;
    /**
     * The list of CUT's methods within the testing scope.
     */
    public List<Method> methodsIPs;
    /**
     * The CUT's own class invariant to check.
     */
    public Method classINV;
    /** 
     * All class invariants, it should be the invariants of CUT's 
     * supper-classes.  --> but this doesn't work!
     * "invoking" a method via reflection is still forced to follow Java's
     * rule for dynamic binding of method names.
     * 
     * <p>Anyway, we can perhaps use this as a mechanism to plug in
     * additional invariants.
     */
    public List<Method> allClassINVs;
    /**  
     * The type of the elements of collections. Whenever the engine
     * has to create a collection, it needs to know the type of its
     * elements; however due to Java's type erasure this info is not
     * available via reflection. FOR NOW we'll pass this info via the
     * top level option, and store it in this variable. This is NOT a
     * generic solution. It only works for collection, and applies
     * globally. That is, the engine simply assumes that all
     * collections it has to generate will have this type of elements.
     * The default is Sequenic.T2.OBJECT.
     */
    public Class TYVAR0 = OBJECT.class;
    /**
     * Switching this on will activate some checking assertions in the 
     * engine. Default is false.
     */
    static public boolean debug = false;
    // Some derived variables:
    private List<Method> methodsCanAcceptCUTinParam;
    private List<Method> methodsCanAcceptCUTinRec;
    private HashMap<Method, Method> methodSpecs;

    public List<Method> getMethodsCanAcceptCUTinRec() {
        return methodsCanAcceptCUTinRec;
    }

    public HashMap<Method, Method> getMethodSpecs() {
        return methodSpecs;
    }
    /**
     * A logger.
     */
    public static Logger logger = Logger.getLogger("Sequenic.T2");
    public static final String CLASSINV_STR = "classinv";
    public static final String MAIN_STR = "main";
    public static final String SPEC_STR = "_spec";
    public static final String AUX_STR = "aux_";

    // Some private variables to get access to engine's runtime info:
    /**
     * Last generated sigma.
     */
    private Sequenic.T2.Seq.Trace sigma = null;

    public Sequenic.T2.Seq.Trace getLastTrace() {
        return sigma;
    }
    /**
     * The result of the last run of runEngine
     */
    private TraceSetExecInfo info = null;
    /**
     * Collected traces so far:
     */
    private LinkedList<Sequenic.T2.Seq.Trace> collectedTraces =
            new LinkedList<Sequenic.T2.Seq.Trace>();
    /**
     * Collected violating traces so far.
     */
    LinkedList<Sequenic.T2.Seq.Trace> violatingTraces =
            new LinkedList<Sequenic.T2.Seq.Trace>();
    /**
     * To save error thrown when the engine is run on a separate thread.
     */
    private Error errorThrownInEngineSeparateThread = null;

    /**
     * This will create an unconfigured engine. E.g. CUT would be still null
     * etc. 
     */
    public BaseEngine() {
    }

    /**
     * Create a test-engine for the class C as target, with default configuration.
     */
    public BaseEngine(Class C) {
        CUT = C;
        accessOption = new AccessOption(C);
        StdReporter stdR = new StdReporter();
        reporters = new ReportersPool();
        reporters.reporters.add(stdR);
        reporters.setShowDepth(maxShowDepth);
        try {
            //System.out.println("xxxxxx") ;
            rnd = new SecureRandom() ;
        } catch (Exception e) {
        }
        consIPs = Util.filterCons(accessOption, Util.getAllCons(C));
        fieldsIPs = Util.filterFields(accessOption, Util.getAllFields(C));
        methodsIPs = Util.filterMethods(accessOption, Util.getAllMeths(C));

        classINV = Util.getClassINV(C);
        allClassINVs = new LinkedList<Method>();
        if (classINV != null) {
            allClassINVs.add(classINV);
        }

        // Setting derived variables:
        methodsCanAcceptCUTinParam = Util.getMethodsCanAcceptCUTinParam(CUT, methodsIPs);
        methodsCanAcceptCUTinRec = Util.getMethodsCanAcceptCUTinRec(CUT, methodsIPs);
        methodSpecs = Util.mk_specMap(methodsIPs);

    }

    /**
     * Recomputing the values of derived variables. Call this after the engine
     * is reconfigured.
     */
    public void realign() {
        methodsCanAcceptCUTinParam = Util.getMethodsCanAcceptCUTinParam(CUT, methodsIPs);
        methodsCanAcceptCUTinRec = Util.getMethodsCanAcceptCUTinRec(CUT, methodsIPs);
        methodSpecs = Util.mk_specMap(methodsIPs);
    }

    /**
     * Just a help function to get a random element from a list.
     */
    private static <T> T getRndElem(Random rnd, List<T> s) {
        if (s.isEmpty()) {
            return null;
        } else {
            return s.get(rnd.nextInt(s.size()));
        }
    }

    /**
     * Randomly construct a meta-step that would construct an object of class
     * C.
     * 
     * @param allowNull When true the method will also try to generate null,
     * with a certain probability. When false will try to avoid null. There is
     * however no guarantee that it won't generate null; it will however do so
     * more efficiently.
     * @param depth The depth of the object we want to generate, relative to
     * the 'root' object. After a certain max depth, this method will just
     * generate null.
     */
    public MkValStep META_mkObject(Class C, int depth, boolean allowNull) {

        // System.out.print(".") ;
    	
        // If C is in the base domain, always generate it, even if the
        // depth exceeds max:
        Object[] r = baseDomain.get(C);
        if (r != null) {
        	if(r[0] == null) CONST.nullConst(C);
            return CONST.nonNull(r[0]);
        }
        // If it is not base, and max depth is exceeded, then return
        // null:
        if (depth >= maxMkValSeqDepth) {
            return CONST.nullConst(C);
        }

        //System.out.println("...") ;
        // Consult the interface map first:
        Class C_implementation = interfaceMap.getImplementation(C);
        if (C_implementation != null) {
            return META_mkObject(C_implementation, depth, allowNull);
        }
        // If C is class "Object", replace it with TYVAR0 if defined,
        // else make an instance of the class Object:
        //System.out.println("... ") ;
        //if (C.getName().equals("java.lang.Object")) {
        if (C == Object.class) {
            if (TYVAR0 != null && TYVAR0 != Object.class) {
                return META_mkObject(TYVAR0, depth, allowNull);
            }
        //else {
        //    return CREATE_OBJECT.META_Construct_an_Object();
        //}
        }

        // Else pick from the pool or generate fresh:
        //System.out.println(">>> " + pickTargetObjFromPoolProb.low + " | " + pickTargetObjFromPoolProb.high) ;
        //System.out.println(">>> " + pickTargetObjFromPoolProb.nextValue() + pickTargetObjFromPoolProb.nextValue() 
        //        + pickTargetObjFromPoolProb.nextValue()) ;
        if (pickTargetObjFromPoolProb.nextValue()) {
            //System.out.println("%%%" + prob + " <= " + pickTargetObjFromPoolProb) ;
            // Deciding to pick the target object from the pool:
            Integer index = pool.rndGetIndex(C);
            //System.out.println(">>> " + index) ;
            if (index != null) {
                return new REF(index);
            }
        }
        //else System.out.println("!!! ") ;
        // ELSE we have to generate a fresh object

        // To generate null:
        if (allowNull && generateNullProb.nextValue()) {
            return CONST.nullConst(C);
        }
        
        // If C is an array, linkedlist, or hashset, then make
        // one. 
        
        Class ClassCollection = null;
        try {
            ClassCollection = Class.forName("java.util.Collection");
        } catch (Exception e) {
        }
        if (C.isArray() ||
                (!C.isInterface() &&
                !(C == CUT) &&
                ClassCollection.isAssignableFrom(C))) {

            Class elemType = null;
            if (C.isArray()) {
                elemType = C.getComponentType();
            } else // Deciding the element type of the collection; for
            // now we'll defaul it to TYVAR0 if it is not
            // null. TYVAR0 can be set via top level option. If it
            // is null, we'll default to Object:
            if (TYVAR0 != null) {
                elemType = TYVAR0;
            } else {
                elemType = Object.class;
            }
            // Set size to be between 0 and this max length:
            int size = maxArrayLengthProb.nextValue();
            //System.out.println(">>> " + size) ;
            MkValStep[] elems = new MkValStep[size];
            for (int i = 0; i < size; i++) {
                elems[i] = META_mkObject(elemType, depth + 1, true);
            }
            String collectionType = MkValStep.ARRAY;
            if (!C.isArray()) {
                collectionType = C.getName();
            }
            return new CREATE_COLLECTION_LIKE(collectionType, elemType, size, elems);
        }

        // else, creating a fresh object from a constructor.

        List<Constructor> constructors = null;
        if (C == CUT) {
            constructors = consIPs;
        } else {
            constructors = Util.getPubCons(C);
        }
        if (constructors.isEmpty()) // C has no constructor! Would just return null:
        {
            return CONST.nullConst(C);
        // ELSE:
        }
        Constructor chosenConstructor = getRndElem(rnd, constructors);
        Class[] paramTypes = chosenConstructor.getParameterTypes();
        MkValStep[] params = new MkValStep[paramTypes.length];

        for (int i = 0; i < paramTypes.length; i++) {
            params[i] = META_mkObject(paramTypes[i], depth + 1, true);
        }
        return (new CREATE_OBJECT(chosenConstructor,
                params,
                // note that it is
                // important that the
                // index is set to -1
                // here:
                -1));

    }

    /**
     * As the other META_mkObject, but produce an array of objects of the given classes.
     */
    public MkValStep[] META_mkObject(Class[] Cs, int depth, boolean allowNull) {
        int N = Cs.length;
        MkValStep[] result = new MkValStep[N];
        for (int i = 0; i < N; i++) {
            result[i] = META_mkObject(Cs[i], depth, allowNull);
        }
        return result;
    }

    /**
     * This is the engine's standard sequence generator, which would generate
     * the sequence randomly.
     */
    static public class RandomSequenceGenerator extends BaseEngineSeqGenerator {

        public RandomSequenceGenerator(BaseEngine e) {
            engine = e;
        }

        public boolean isExhausted() {
            return false;
        }

                
        /**
         * As META_mkObject, but specifically for producing the target object. 
         * A target object is always created with a constructor.
         */
        public MkValStep META_mkTargetObject(Class C) {

            // Redoing a sigma is requested:
            if (sigma_to_redo != null) return sigma_to_redo.creation ;
            
            // consIPs should not be empty :

            Constructor chosen = null;
            if (C == engine.CUT) {
                chosen = getRndElem(engine.rnd, engine.consIPs);
            } else {
                chosen = getRndElem(engine.rnd, Util.getAllCons(C));
            }
            Class[] paramTypes = chosen.getParameterTypes();
            MkValStep[] params = engine.META_mkObject(paramTypes, 1, true);

            return (new CREATE_OBJECT(chosen,
                    params,
                    // note that it is important that the index is set to -1
                    // here:
                    -1));
        }

        /**
         * Randomly construct a meta-step that would make a single test-step.
         * 
         * @param sigma The trace so far.
         */
        public TraceStep META_mkTestStep(Sequenic.T2.Seq.Trace sigma) {

            // Redoing a sigma is requested:
            if (sigma_to_redo!=null) {
               if (sigma_to_redo.trace.isEmpty()) sigma_to_redo = null ;
               else return sigma_to_redo.trace.removeFirst() ;
            }
            
            int numberOfFieldsInScope = engine.fieldsIPs.size();
            int numberOfMethodsInScope = engine.methodsCanAcceptCUTinParam.size() +
                    engine.methodsCanAcceptCUTinRec.size();
            Random rnd = engine.rnd;

            // Case 1: nothing in scope:
            if (numberOfFieldsInScope + numberOfMethodsInScope == 0) {
                return null;
            // Case 2: decide to update a field, and there are some fields:
            }
            if (((numberOfMethodsInScope == 0 && numberOfFieldsInScope > 0) ||
                    (numberOfFieldsInScope > 0 && engine.chooseFieldUpdateProb.nextValue())) &&
                    !engine.useCustomTraceDirector) {
                Field chosen = getRndElem(rnd, engine.fieldsIPs);
                return (new UPDATE_FIELD(chosen, engine.META_mkObject(chosen.getType(), 0, true)));
            }

            // Case 3: decide to call a method:

            Method method = null;
            int whichParam = -1;
            Class[] paramTypes = null;

            // Case 2.a: the normal use, with no custom trace director used:
            if (!engine.useCustomTraceDirector) {

                // No methods are in scope! Return null :
                if (numberOfMethodsInScope == 0) {
                    return null;
                // Else we have at least one method to choose:
                }
                if (engine.methodsCanAcceptCUTinRec.size() == 0 ||
                        (engine.methodsCanAcceptCUTinParam.size() > 0 && engine.passTObjAsParamProb.nextValue())) {

                    // Deciding to pass target object as parameter instead 
                    method = getRndElem(rnd, engine.methodsCanAcceptCUTinParam);
                    List<Integer> possiblePlaces = Util.canAcceptAsParameter(engine.CUT, method);
                    whichParam = getRndElem(rnd, possiblePlaces);

                } else {  // methodsCanAcceptCUTinRec is not empty

                    method = getRndElem(rnd, engine.methodsCanAcceptCUTinRec);
                // whichParam should be -1
                }
                paramTypes = method.getParameterTypes();
            } // Else, case 2.a: the use of a custom trace director is requested:
            else {
                try {
                    Object targetObj = engine.pool.get(sigma.indexOfTargetObj);
                    Method customTracedirector = targetObj.getClass().getDeclaredMethod("customTraceDirector", new Class[0]);
                    customTracedirector.setAccessible(true);
                    List<Method> possibleSteps = (List<Method>) customTracedirector.invoke(targetObj, new Object[0]);
                    if (possibleSteps.isEmpty()) //Message.throwT2Error(T2Error.ABORT,
                    //					 CUT.getName() + "'s customTraceDirector returns an empty set of next step.") ;
                    // Change the behavior, from ABORT to returning null:
                    {
                        return null;
                    // Else at least one choice is possible, then choose one:
                    }
                    method = possibleSteps.get(rnd.nextInt(possibleSteps.size()));
                    paramTypes = method.getParameterTypes();
                } catch (NoSuchMethodException e) {
                    throw new T2Error(engine.CUT.getName() + " does not specify a custom trace director.");
                } catch (Exception e) {
                    assert false;
                }
            }

            // method should be non-null now
            // Get its specification, if exists:
            if (engine.methodSpecs.containsKey(method)) {
                method = engine.methodSpecs.get(method);
            // else System.out.println(">> " + method.getName()) ;
            }
            setCurrentMethod(method);
            
            MkValStep[] params = new MkValStep[paramTypes.length];

            for (int i = 0; i < params.length; i++) {

                // note that i>=0, so if whichParam=-1 the guard is false
                // anyway:
                if (i == whichParam) {
                    params[i] = new REF(sigma.indexOfTargetObj);
                } else {
                    params[i] = engine.META_mkObject(paramTypes[i], 0, true);
                }
            }

            if (Modifier.isStatic(method.getModifiers())) {
                return (new CALL_METHOD(method, null, params));

            // else, if method is not static:
            }
            MkValStep receiver = null;

            if (whichParam < 0) {
                receiver = new REF(sigma.indexOfTargetObj);
            } else {
                receiver = engine.META_mkObject(method.getDeclaringClass(), 0, false);
            //receiver = META_mkTargetObject(method.getDeclaringClass());
            }
            return (new CALL_METHOD(method, receiver, params));

        }
        
        
    }

    /**
     * This implements the main loop of the engine. It generates traces,
     * collect results, and generate report.
     */
    public void mainloop() {

        if (consIPs.isEmpty()) {
            throw new T2Error("The set of constructor-IPs is empty.");
        }
        if (maxExecLength <= 0) {
            throw new T2Error("Max. trace length is set to 0 or negative (should be positive!).");
        }

        // Make sigma global, so that we can inspect what the last generated
        // sequence was.
        // Sequenic.T2.Seq.Trace sigma = null;
        TraceStep step = null;
        Object targetObj = null;
        ExecResult stepResult = null;
        Sequenic.T2.Seq.Trace sigma_old = null ;
        info = new TraceSetExecInfo();
        //boolean invOk = true;
        int numOfattempsToCreateTargetObj = 0;
        boolean creationMeaningful = false;
        // Execution length:
        int depth = 0;
        // Innitialize the sequence generator:
        seqGenerator.init();

        info.time = System.currentTimeMillis();

        collectedTraces.clear();
        violatingTraces.clear();

        int aux_temination_metric_old = maxNumOfSteps - info.totNumOfSteps + 1;
        int aux_sigma_length = 0;
        int aux_sigma_length_frozen = -1;

        reporters.reportTestSetBegin(CUT, Message.GREET);

        while (info.totNumOfSteps < maxNumOfSteps &&
                !seqGenerator.isExhausted() &&
                (saveThisMany > 0 || info.numOfViolations < maxNumViolations)) {

            //System.out.println(">>> ntraces = " + info.numOfTraces) ;
            //System.out.println(">>> nsteps  = " + info.totNumOfSteps) ;
            //if (sigma==null) System.out.println(">>> sigma = null") ;
            //else System.out.println(">>> sigma = " + sigma.creation + " // " + sigma.trace) ;

            if (debug) {
                if (sigma == null) {
                    aux_sigma_length = 0;
                } else {
                    aux_sigma_length = sigma.trace.size() + 1;
                // proof of loop termination:
                }
                assert (maxNumOfSteps - info.totNumOfSteps < aux_temination_metric_old) ||
                        ((maxNumOfSteps - info.totNumOfSteps == aux_temination_metric_old) &&
                        aux_sigma_length_frozen > 0 && aux_sigma_length == 0) : "LOOP TERMINATION";

                assert aux_sigma_length == 0 ||
                        aux_sigma_length > aux_sigma_length_frozen : "LOOPINV";

                assert depth == aux_sigma_length : "LOOPINV";

                aux_temination_metric_old = maxNumOfSteps - info.totNumOfSteps;
                aux_sigma_length_frozen = aux_sigma_length;
            }


            if (depth >= maxExecLength) { // max depth exceeded, reset sigma:

                if (saveThisMany > 0) {
                    collectedTraces.add(sigma);
                    saveThisMany--;
                }
                depth = 0;
                info.numOfFullTraces++ ;
                sigma = null;
                seqGenerator.notify_non_asmfailing_trace() ;
                continue;
            }
            // ELSE, create sigma, or extend it with a step:

            if (sigma == null) { // create the target object first:
                //System.out.println(">>>") ;
                // Try 100 times (at the moment hard wired):

                numOfattempsToCreateTargetObj = 0;
                creationMeaningful = false;
                while (numOfattempsToCreateTargetObj < 100) {
                    // don't forget to reset the pool !!
                    pool.reset();
                    sigma = new Sequenic.T2.Seq.Trace();
                    sigma.creation = seqGenerator.META_mkTargetObject(CUT);
                    if (sigma.creation == null) {
                        // Creation fails
                        numOfattempsToCreateTargetObj++;
                        continue;
                    }
                    stepResult = sigma.creation.MkTargetObject(CUT, pool, allClassINVs);
                    if (stepResult.isAsmViolating()) {
                        // Creation fails due to pre-cond failure or args failire:
                        numOfattempsToCreateTargetObj++;
                        continue;
                    }
                    // Else creation step is at least meaningful (it may still
                    // fail due to violation):
                    creationMeaningful = true;
                    sigma.indexOfTargetObj =
                            ((CREATE_OBJECT) sigma.creation).indexOfNewObject;
                    targetObj = pool.get(sigma.indexOfTargetObj);
                    break;
                }
                if (!creationMeaningful) {
                    if (seqGenerator.isExhausted()) {
                        break;
                    } else {
                        throw new T2Error("Keep failing to create a target object.");
                    }
                }
                // so the creation was successful:
                depth = 1;
                info.totNumOfSteps++;
                info.numOfTraces++;
            } else { // Else extend the sigma with a step:

                if (debug) {
                    assert pool.get(sigma.indexOfTargetObj) != null : "TargetObj should not be null";
                }
                step = seqGenerator.META_mkTestStep(sigma);
                if (step == null) {
                    if (saveThisMany > 0) {
                        collectedTraces.add(sigma);
                        saveThisMany--;
                    }
                    depth = 0;
                    sigma = null;
                    continue;
                }
                sigma.trace.add(step);
                stepResult = step.exec(CUT, pool, targetObj, depth, allClassINVs);
                depth++;
                //System.out.println("...") ;
                info.totNumOfSteps++;
            }
            // Collect statistics:
            info.accumulateResult(stepResult);

            if (stepResult.isAsmViolating()) {
                //System.out.println("--- nsteps  = " + info.totNumOfSteps) ;
                //System.out.println("--- sigma = " + sigma.creation + " // " + sigma.trace) ;
                //System.out.println("ASM violation!") ;
                // irrelavant step     
                // discarding sigma:
                seqGenerator.notify_asmfailing_trace(sigma) ;
                depth = 0;
                sigma = null;
                continue;
            }
            if (stepResult.isReqViolating()) {
                if (info.numOfViolations <= maxNumViolations) {
                    collectedTraces.add(sigma);
                    violatingTraces.add(sigma);
                }
                sigma.violating = true;

                // Break immediately after suspecting divergence:
                if (stepResult.possiblyDiverging) {
                    sigma.diverging = true;
                    break;
                }
                seqGenerator.notify_non_asmfailing_trace() ;
                depth = 0;
                sigma = null;
            }
        }  // End of loop

        info.time = System.currentTimeMillis() - info.time;

        reportAndSave();

    }

    /**
     * For reporting and saving results after doing runEngine.
     */
    public void reportAndSave() {

        //reporters.reportTestSetBegin(CUT,Message.GREET);

        // Report violating traces:
        if (showViolatingTraces) {
            //println("XXX " + violatingTraces.size()) ;
            TraceSet tset = new TraceSet(CUT, pool, violatingTraces);
            boolean dont_execute_last_diverging_step = true;
            tset.exec(allClassINVs, dont_execute_last_diverging_step,
                    showIntermediateSteps,
                    -1,
                    reporters);
        }
        // Report collected statistics:
        reporters.reportTestSetEnd(CUT, info, "");

        // Saving traces:
        if (collectedTraces.size() > 0) {
            println("** Saving " + collectedTraces.size() + " traces...");
            TrFile trfile = new TrFile(CUT.getName(),
                    pool.getClass().getName(),
                    collectedTraces,
                    allClassINVs);
            try {
                if (nameOfSaveFile != null) {
                    trfile.save(nameOfSaveFile);
                } else {
                    trfile.save();
                }
            } catch (T2Exception exc) {
                println(exc.getMessage());
                exc.printStackTrace();
            }
        }
    }
}