/*
 * 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 Sequenic.T2.Pool;
import Sequenic.T2.Obj.*;
import Sequenic.T2.Msg.*;
import Sequenic.P2.*;
import java.io.*;
import java.util.*;
import java.lang.reflect.*;

/**
 * A simple text-based reporter.
 *
 * @see Sequenic.T2.Seq.ReportersPool
 * @see Sequenic.T2.Seq.Reporter
 */
public class StdReporter extends Reporter {

    /**
     * A reference to an object shower to print the internal state of an object.
     */
    private Show Shower;

    public StdReporter() {
        Shower = new Show(Reporter.defaultShowDepth, 6);
    }

    public void setShowDepth(int d) {
        Shower.maxDepth = d;
    }

    private void println(String s) {
        out.println(s);
    }

    private StringWriter stringwriter = new StringWriter() ;
    private PrintWriter outstring = new PrintWriter(stringwriter) ;

    /**
     * For reporting the actual state of the target object after each step,
     * and the actual arguments passed to the step.
     */
    private void reportActualStates(ExecResult res, boolean isCreationStep) {

        if (isCreationStep) {
            reportConstructionOfTargetObject(
                    ((CREATE_OBJECT) res.step).con,
                    res.args,
                    res.returnedObj);
            return;
        }

        if (res.step instanceof UPDATE_FIELD) {
            reportUpdateField(
                    ((UPDATE_FIELD) res.step).field,
                    res.args[0]);
            return;
        }

        if (res.step instanceof CALL_METHOD) {
            reportMethodCall(
                    ((CALL_METHOD) res.step).method,
                    res.targetObj,
                    res.receiverObj,
                    res.args, res.returnedObj);
        }

    }

    private void reportConstructionOfTargetObject(Constructor con,
            Object[] args,
            Object result) {
        println("  ** Calling constructor " + con.getName());
        if (printMethodParamsOption && args!=null) {
            for (int i = 0; i < args.length; i++) {
                println("    ** Arg [" + i + ":]");
                println(Shower.showWithContNum(args[i]));
            }
        }
        println("    ** Resulting target object:");
        println(Shower.showWithContNum(result));
    }

    private void reportUpdateField(Field field, Object newFieldVal) {
        println("    ** Update on " + field.getName() + " with:");
        println(Shower.showWithContNum(newFieldVal));
    }

    private void reportMethodCall(Method method,
            Object targetObj,
            Object receiver,
            Object[] args,
            Object returnval) {
        println("  ** Calling method " + method.getName() + " with:");
        if (receiver != null) {
            out.print("    ** Receiver: ");
            if (targetObj == receiver) {
                println("target-obj");
            } else {
                println("");
                println(Shower.showWithContNum(receiver));
            }
        }
        if (printMethodParamsOption && args!=null) {
            for (int i = 0; i < args.length; i++) {
                out.print("    ** Arg [" + i + ":]");
                if (args[i] == targetObj) {
                    println("target-obj");
                } else {
                    println("");
                    println(Shower.showWithContNum(args[i]));
                }
            }
        }
        if (returnval != null) {
            println("    ** Return value:");
            println(Shower.showWithContNum(returnval));
        }
        println("    ** State of target object now:");
        println(Shower.showWithContNum(targetObj));
    }

    private static final String lineHsep1 = "-----------------------------------";
    private static final String lineHsep1b = "  ---------------------------------";
    private static final String lineHsep2 = "+++";
    private static final String lineHsep2b = "  ------";

    public void reportTraceBegin() {
        //println(lineHsep1b);
        println(lineHsep2);
        println("  ** Begin test sequence.");
        Shower.resetContinousNumbering();
    }

    public void reportTraceEnd() {
        println("  ** End test sequence");
    }

    public void reportStep(ExecResult res, int stepNr) {

        if (stepNr == 0) {
            println("  ** STEP 0: creating target object.");
        } else {
            println("  ** STEP " + stepNr + ".");        // Argument fauilure case:
        }
        
        if (res.argumentFailure == null 
                && res.CUT_constructor_failure==null
                && !res.possiblyDiverging )
            // In this case it is possible to report actual states:
            reportActualStates(res, stepNr == 0) ;
        else {
            // else resort to meta-printing:
           if (res.possiblyDiverging) { 
                println("  xx Possible NON-TERMINATION at this step (but may also be in classinvs).");
                println("     Meta-printing the step:\n" + StringFormater.indent(res.step.toString(), 7));
                return ;
            }
            if (res.argumentFailure != null && res.CUT_constructor_failure == null) { 
                println("  xx Argument failure, meta-printing the step:");
                println(StringFormater.indent(res.step.toString(), 7));
                res.argumentFailure.printStackTrace(outstring) ;
                println("  ** Strack trace: " + stringwriter);
                stringwriter.flush();
                return ;
            }
            if (res.CUT_constructor_failure != null) {
                println("  xx CUT constructor failure, meta-printing the step:");
                println(StringFormater.indent(res.CUT_constructor_failure.toString(), 7));
            }
        }
        
        // Reporting violation classification:      
        
        if (res.returnedException != null) {
            println("  ** Throwing exception (expected) " + res.returnedException);
        }
        if (res.precViolation != null) {
            println("  xx Pre-condition VIOLATED!");
            res.precViolation.printStackTrace(outstring);
            println("  ** Strack trace: " + stringwriter);
            stringwriter.flush();
        }
        if (res.argumentFailure != null) {
            println("  xx FAIL to construct an argument.");
        }
        if (res.appmodViolation != null) {
            println("  xx Application model VIOLATED!");
        }
        if (res.postcViolation != null) {
            println("  xx Assertion VIOLATED!");
            res.postcViolation.printStackTrace(outstring);
            println("  ** Strack trace: " + stringwriter);
            stringwriter.flush();
        }

        if (res.classinvViolation) {
            println("  xx Class invariant VIOLATED!");
            //if (res.postcViolation != null) {
            //    res.postcViolation.printStackTrace(outstring);
            //    println("  ** Strack trace: " + stringwriter);
            //    stringwriter.flush();
           // }
        }

        if (res.classinvExecptionalViolation != null) {
            println("  xx Class invariant throws (UNEXPECTED) " + res.classinvExecptionalViolation);
            res.classinvExecptionalViolation.printStackTrace(outstring);
            println("  ** Strack trace: " + stringwriter);
            stringwriter.flush();
        }

        if (res.internalError != null) {
            println("  xx INTERNAL ERROR!");
            res.internalError.printStackTrace(outstring);
            println("  ** Strack trace: " + stringwriter);
            stringwriter.flush();
        }
    }

    public void reportTestSetBegin(Class C, String header) {
        println(header);
        println(Message.BEGIN);
        println("** BEGIN TEST SET. Target: " + C.getName());
    }

    public void reportTestSetEnd(Class C, TraceSetExecInfo info, String footer) {
        //println(lineHsep1);
        println(lineHsep2);
        if (info.numOfViolations <= 0) {
            println("** NO violation found.");
        } else {
            println("** VIOLATIONS FOUND: " + info.numOfViolations);
            if (info.numOfAssertViolation > 0) {
                println("     " + info.numOfAssertViolation + " assertion violations.");
            }
            if (info.numOfClassInvViolation > 0) {
                println("     " + info.numOfClassInvViolation + " class-inv violations.");
            }
            if (info.numOfErrorViolation > 0) {
                println("     " + info.numOfErrorViolation + " internal errors.");
            }
            if (info.numOfClassInvException > 0) {
                println("     " + info.numOfClassInvException + " exceptions thrown by class invariant");
            }
        }
        if (info.numOfIrrelevantChecks <= 0) {
        	println("** NO assumption invalidations.") ;
        }
        else {
        	println("** assumption invalidations: " + info.numOfIrrelevantChecks + ".");
        	if (info.numOfPreCondViolations > 0) {
        		println("     " + info.numOfPreCondViolations + " PRE violations.");
        	}
        	if (info.numOfAppModelViolations > 0) {
        		println("     " + info.numOfAppModelViolations + " APPMODEL violations.");
        	}
        }
        println("** tot.  num. full traces : " + info.numOfFullTraces);
        println("** total number of traces : " + info.numOfTraces);
        println("** total execution steps  : " + info.totNumOfSteps);
        float average = ((float) info.totNumOfSteps) / ((float) info.numOfTraces);
        average = Math.round(100 * average) / 100f ;
        println("** average trace lenght   : " + average);
        println("** time                   : " + info.time + "ms.");
        average = ((float) info.time) / ((float) info.totNumOfSteps);
        average = Math.round(100 * average) / 100;
        println("** average time per step  : " + average + "ms.");
        //println(lineHsep2);
        println("** END TEST SET");
        println(Message.END);
        out.print(footer);
    }
}