package Sequenic.T2.Seq;

import java.lang.reflect.Constructor;
import java.lang.reflect.Field;
import java.lang.reflect.Method;
import java.util.LinkedList;
import java.util.List;

import org.junit.Test;

import Sequenic.T2.Pool;

public class TraceTest {

    public TraceTest() {
    }

    public static class A {

        public String n;

        public A(String n0) {
            n = n0;
        }

        public String toString() {
            return n;
        }
    }

    public static class A2 extends A {

        public int x;

        public A2(String n0, int x0) {
            super(n0);
            x = x0;
        }

        public String toString() {
            return super.toString() + " ; " + x;
        }

        public void crash() {
            assert false ;
        }
    }

    @Test
    public void test_exec() {


        Pool pool = new Pool();

        // Constructing a trace tau:
        Trace tau = new Trace();
        Constructor A2_constr = null;
        try {
            A2_constr = A2.class.getConstructor(new Class[]{String.class, Integer.TYPE});
        } catch (Exception e) {
            assert false;
        }
        CONST param1 = CONST.nonNull("Foo");
        CONST param2 = CONST.nonNull(new Integer(888));
        tau.creation = new CREATE_OBJECT(A2_constr, new MkValStep[]{param1, param2}, -1);

        List<Method> classinvs = new LinkedList<Method>();

        // System.out.println(">>>" + Show.show(tau.creation)) ;
        tau.indexOfTargetObj = 0;

        try {
            Field fx = A2.class.getField("x");
            Field fn = A2.class.getField("n") ;
            Method m_toString = A2.class.getMethod("toString", new Class[0]) ;
            Method m_crash = A2.class.getMethod("crash", new Class[0]) ;

            tau.trace.add(new UPDATE_FIELD(fn, CONST.nonNull("Good guy")));
            tau.trace.add(new UPDATE_FIELD(fx, CONST.nonNull(new Integer(111))));

            tau.trace.add(new CALL_METHOD(m_toString, new REF(0), new MkValStep[0]));
            tau.trace.add(new CALL_METHOD(m_crash, new REF(0), new MkValStep[0]));

            //A2 a = new A2("Boo", 10) ;
            //fx.set(a, new Integer(11)) ;
            //System.out.println(">>>" + Show.show(a)) ;
            //m_toString.invoke(a, new Object[0]);
            //m_crash.invoke(a, new Object[0]);
        } catch (Exception e) {
            e.printStackTrace();
            assert false;
        }

        // Setting up reporters, etc:
        ReportersPool reporters = new ReportersPool();
        reporters.reporters.add(new StdReporter());


        // Executing the trace:
        TraceExecInfo info = tau.exec(A2.class,pool,classinvs, false, true, reporters);
        assert info.lastStepResult.isReqViolating();
        assert info.lastStepResult.postcViolation != null ;
        
    }
}