/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package Sequenic.T2;
import Sequenic.T2.Seq.* ;
import java.io.* ;
import java.util.* ;
import java.lang.reflect.* ;
import org.junit.Test;
import static org.junit.Assert.*;

/**
 *
 * @author underdarkprime
 */
public class Main_Test_1 {

    public Main_Test_1() {
    }

/**
     * Test purpose: check if T2 can reach private method.
     */
    static public class Cprivmeth {

        private void m1() {
        }

        private void m1_spec() {
            m1();
            assert false;
        }
    }

    @Test
    public void test_privmeth() {
        System.out.println("@@@ check if T2 can reach private method...");
        Class C = Cprivmeth.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --inclprivate --silent");
        Debug.assertTrfNonEmpty(C);
    }
    
     /**
     * Test purpose: check if T2 can exclude private, default, protected, and static methods.
     */
    static public class Cexclude {

        private void m0() {
            assert false;
        }

        void m1() {
            assert false;
        }

        protected void m2() {
            assert false;
        }

        static public void s() {
            assert false;
        }

        public void m3() {
        }
    }

    @Test
    public void test_exclude() {
        System.out.println("@@@ check if T2 can exclude default, protected, and static methods...");
        Class C = Cexclude.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --excldefault --exclprotected --exclstatic --silent");
        Debug.assertTrfEmpty(C);
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --pubonly --exclstatic --silent");
        Debug.assertTrfEmpty(C);
    }

    /**
     * Test purpose: check if T2 can check static method.
     */
    static public class Cstaticmeth {
        // T2 needs at least a method to which it can pass a target object,
        // so this won't work:
        // static public s() { assert false ; }
        // Instead, test with:
        static public void s(Cstaticmeth x) {
            assert false;
        }
    }

    @Test
    public void test_staticmeth() {
        System.out.println("@@@ check if T2 can check static method...");
        Class C = Cstaticmeth.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfNonEmpty(C);
    }

    /**
     * Test purpose: check if T2 indeed ignores static or final or aux var.
     */
    static public class CignoreStaticFinalField {

        static public boolean b = true;
        public final boolean c = true;
        public boolean aux_d = true;

        void m() {
            assert b && c && aux_d;
        }

        private boolean classinv() {
            return b && c && aux_d;
        }
    }

    @Test
    public void test_ignoreStaticFinalField() {
        System.out.println("@@@ check if T2 indeed ignores static or final or aux var...");
        Class C = CignoreStaticFinalField.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfEmpty(C);
    }

    /**
     * Test purpose: check if T2 can reach private field.
     */
    static public class Cprivfield {

        private int x = -100;
        private int aux_count = 0;

        private boolean classinv() {
            assert (x == -100) ;
            aux_count++;
            return true;
        }

        void m() {
        }
    }

    @Test
    public void test_privfield() {
        System.out.println("@@@ check if T2 can reach private field...");
        Class C = Cprivfield.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --inclprivate --silent");
        Debug.assertTrfNonEmpty(C);
    }
    
    static public class Cfield{
        int x = 0 ;
        void m1() { assert x==0 ; } 
    }

    @Test
    public void test_fupdate_option() {
        System.out.println("@@@ check if the fupdateprob option works ...");
        Class C = Cfield.class;
        // First option is not set
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfNonEmpty(C);
        
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --fupdateprob=0.5 --silent");
        Debug.assertTrfNonEmpty(C);
    }
    
    /**
     * Test purpose: check if T2's meth and xmeth options, and exclude annotation.
     */
    static public class Cexclincl {

        private void m1() {
        }

        private void m2() {
            assert false;
        }

        void m3() {
            assert false;
        }

        @T2annotation.exclude
        void m3b() {
            assert false;
        }

        void m4() {
        }
    }

    @Test
    public void test_exclincl() {
        System.out.println("@@@ check if T2's meth and xmeth options, and exclude annotation...");
        Class C = Cexclincl.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --xmeth=m3 --silent");
        Debug.assertTrfEmpty(C);
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --inclprivate --meth=m1 --silent");
        Debug.assertTrfEmpty(C);
    }

    /**
     * Test purpose: check if T2 can handle a class with empty IPs.
     */
    static public class CemptyIPs {
    }

    @Test
    public void test_emptyIPs() {
        System.out.println("@@@ check if T2 can handle a class with empty IPs...");
        Class C = CemptyIPs.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent --nmax=10 --ownclassonly --savegoodtr=100");
        Debug.assertTrfNonEmpty(C);
    }

    /**
     * Test purpose: check if T2 can detect error in the constructor.
     */
    static public class CfailConstr1 {

        public CfailConstr1() {
            assert false;
        }

        public void m() {
        }
    }

    @Test
    public void test_failConstr1() {
        System.out.println("@@@ check if T2 can detect error in the constructor...");
        Class C = CfailConstr1.class;
        TrFile.delete(C);
        Main.main(C.getName() + "  --silent --nmax=10 --ownclassonly");
        Debug.assertTrfNonEmpty(C);
    }

    /**
     * Test purpose: check if T2 can handle the situation when all
     * constructors of the target class are failing.
     */
    static public class CfailConstr2 {

        public CfailConstr2() {
            assert false : "PRE" ;
        }

        public void m() {
        }
    }
    
    @Test
    public void test_failConstr2() {
        System.out.println("@@@ check if T2 can handle situation when all constructors keep faling...");
        Class C = CfailConstr2.class;
        TrFile.delete(C);
        try {
        	Main.main(C.getName() + " --silent --nmax=10 --ownclassonly");
        }
        catch (Sequenic.T2.Msg.T2Error e) {
        	assert e.getMessage().startsWith("## T2 ABORT.\n## Keep failing") ;
        	Debug.assertTrfEmpty(C);
        	return ;
        }
        assert false ;
    }
    
    /**
     * Test purpose: check if T2 can handle the situation when there is
     * no constructor in scope..
     */
    static public class CnoConstrInScope {

        private CnoConstrInScope() { assert false ;
        }

        public void m() {
        }
    }
    
    @Test
    public void test_noConstrInScope() {
        System.out.println("@@@ check if T2 can handle situation when there is no constructor in scope...");
        Class C = CnoConstrInScope.class;
        TrFile.delete(C);
        try {
            // This should throw an error:
            Main.main(C.getName() + "  --silent --nmax=10 --ownclassonly");
            assert false ;
        }
        catch (Error e) { 
            //System.out.println("xxxx ") ; e.printStackTrace() ; 
            String msg = e.getMessage() ;
            assert msg.contains("The set of constructor-IPs is empty") ;
        }
    }

    /**
     * Test purpose: check if T2 recognizes PRE condition.
     */
    static public class Cpre {

        void m() {
            assert false : "PRE";
            assert false;
        }
    }

    static public class Cpre2 {

        public Cpre2() {
            assert false : "PRE";
            assert false;
        }
    }
    
    @Test
    public void test_pre() {
        System.out.println("@@@ check if T2 recognizes PRE condition ...");
        Class C = Cpre.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfEmpty(C);
        System.out.println("@@@ check if T2 recognizes PRE condition in the constructor ...");
        C = Cpre2.class;
        //TrFile2.delete(C);
        try {
            // Should fail:
            Main.main(C.getName() + " --debug --ownclassonly --silent --nmax=10");
            assert false ;
        }
        catch (Error e) {
            String msg = e.getMessage() ;
            assert msg.contains("Keep failing to create a target object") ;
        }
    }

    /**
     * Test purpose: check if T2 recognizes that an indirect PRE violation should
     * counts as a post-condition violation.
     */
    static public class Cpre3a {

    	private Cpre3b x = new Cpre3b() ;
    	
        public void m1() {
        	x.m1() ;
        }
    }
    
    static public class SuperCpre3b {
        public void m1() {
        	assert false : "PRE" ;
        }
    }
    
    static public class Cpre3b extends SuperCpre3b {
        public void m1() {
        	super.m1() ;
        }
    }
    
    @Test
    public void test_pre2() {
        System.out.println("@@@ check if T2 recognizes indirect PRE violation ...");
        Class C = Cpre3a.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfNonEmpty(C);
        System.out.println("@@@ check if T2 correctly categorize PRE violation from superclass as assumption violation...");
        C = Cpre3b.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfEmpty(C);
      }
  
    /**
     * Test purpose: check if T2 recognizes PRE in a method when it
     * is shadowed with a specification.
     */
    static public class Cpre4 {

        public void m_spec() {
        	m() ;
        }
        
        public void m() {
        	assert false : "PRE" ;
        }
    }
    
    @Test
    public void test_pre3() {
        System.out.println("@@@ check if T2 recognizes shadowed PRE ...");
        Class C = Cpre4.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfEmpty(C);
      }
    
    /**
     * Test purpose: check if T2 recognizes APPMODEL .
     */
    static public class Cappmodel {

        private boolean classinv() {
            assert false : "APPMODEL";
            return false;
        }

        public void m() {
        }
    }

    @Test
    public void test_appmodel() {
        System.out.println("@@@ check if T2 recognizes APPMODEL...");
        Class C = Cappmodel.class;
        TrFile.delete(C);
        try {
            // This should fail:
            Main.main(C.getName() + " --debug --silent");
            assert false ;
        }
        catch (Error e) {
            //e.printStackTrace();
            assert e.getMessage().contains("Keep failing to create a target object") ;
        }
        //Debug.assertTrfEmpty(C);
    }

    /**
     * Test purpose: check if normal exception, error, runtime exception thrown 
     * by methods are interpreted correctly.
     */
    static public class Cthrowable {

        void m1() {
            throw new Error();
        }

        void m2() {
            throw new RuntimeException();
        }

        void m3() throws IOException {
            throw new IOException();
        }
    }

    @Test
    public void test_throwable() {
        System.out.println("@@@ check if normal exception, error, runtime exception thrown by methods are interpreted correctly...");
        Class C = Cthrowable.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --meth=m1 --silent");
        Debug.assertTrfNonEmpty(C);
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --meth=m2 --silent");
        Debug.assertTrfNonEmpty(C);
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --meth=m3 --silent");
        Debug.assertTrfEmpty(C);
    }

    /**
     * Test purpose: check if normal exception, error, runtime exception thrown 
     * by classinv are interpreted correctly.
     */
    static public class CthrowableInv1 {

        void m() {
        }

        private boolean classinv() {
            throw new Error();
        }
    }

    static public class CthrowableInv2 {

        void m() {
        }

        private boolean classinv() {
            throw new RuntimeException();
        }
    }

    static public class CthrowableInv3 {

        void m() {
        }

        private boolean classinv() throws IOException {
            throw new IOException();
        }
    }

    @Test
    public void test_throwableInv() {
        System.out.println("@@@ check if normal exception, error, runtime exception thrown by classinv are interpreted correctly...");
        Class C = CthrowableInv1.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfNonEmpty(C);

        C = CthrowableInv2.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfNonEmpty(C);

        C = CthrowableInv3.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfNonEmpty(C);

    }

    /**
     * Test purpose: check if aux_laststep is updated correctly.
     */
    static public class Claststep {

        private String aux_laststep = "boo!";

        void m() {
        }

        private boolean classinv() {
            return aux_laststep.equals("m") || aux_laststep.equals(Claststep.class.getName());
        }
    }

    @Test
    public void test_laststep() {
        System.out.println("@@@ check if aux_laststep is updated correctly...");
        Class C = Claststep.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --silent");
        Debug.assertTrfEmpty(C);
    }

    /**
     * Test purpose: check if aux_trace is updated correctly.
     */
    static public class Cauxtrace {

        private Sequenic.T2.Seq.Trace aux_trace;

        public void m1() {
            //System.out.println("!!! " + aux_trace.trace.size()) ;
            assert aux_trace.trace.getLast().getName().equals("m1");
        }

        public void m2() {
            //System.out.println("!!! " + aux_trace.trace.size()) ;
            assert aux_trace.trace.getLast().getName().equals("m2");
        }
    }

    @Test
    public void test_auxtrace() {
        System.out.println("@@@ check if aux_trace is updated correctly...");
        Class C = Cauxtrace.class;
        TrFile.delete(C);
        Main.main(C.getName() + "  --pubonly --exclfield");
        Debug.assertTrfEmpty(C);
    }

    /**
     * Test purpose: check if the mechanism to use custom trace director works properly.
     */
    static public class Ccustomtracedir {

        static String M1 = "m1";
        static String M2 = "m2";
        String last = M2;

        private void m1(int x) {
            assert (last == M2);
            last = M1;
        }

        private void m2(boolean b) {
            assert (last == M1);
            last = M2;
        }

        private List<Method> customTraceDirector() {
            LinkedList<Method> nextsteps = new LinkedList<Method>();
            Class[] paramTypes = new Class[1];
            try {
                if (last == M2) {
                    paramTypes[0] = Integer.TYPE;
                    nextsteps.add(this.getClass().getDeclaredMethod("m1", paramTypes));
                    //paramTypes[0] = Boolean.TYPE;
                    //nextsteps.add(this.getClass().getDeclaredMethod("m2", paramTypes));
                } else {
                    paramTypes[0] = Boolean.TYPE;
                    nextsteps.add(this.getClass().getDeclaredMethod("m2", paramTypes));
                }
            } catch (Exception e) {
            }
            return nextsteps;
        }
    }

    @Test
    public void test_customtracedir() {
        System.out.println("@@@ check if custom trace director is engaged correctly...");
        Class C = Ccustomtracedir.class;
        TrFile.delete(C);
        Main.main(C.getName() + " --debug --customtracedir ");
        Debug.assertTrfEmpty(C);
    }
     
    @Test
    public void test_LogFile() {
        System.out.println("@@@ check if report can be saved to a file...");
        File f = new File("test.log") ;
        f.delete() ;
        assert ! f.exists() ;
        Main.main(Cprivmeth.class.getName() + " --inclprivate --outfile=test.log") ;
        assert f.exists() ;
    }
    
}