/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package Sequenic.T2.Engines;
import Sequenic.T2.Debug ;
import org.junit.Test;
import static org.junit.Assert.*;

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

    public BaseEngineTest() {
    }
    
    static void configureOutStreamToDebugStream(BaseEngine E) {
        Debug.FlushDebugOutStream() ;
        E.out = Debug.pout ;
        E.reporters.setOutStream(Debug.pout) ;
    }
    
    static public class C1 {

        private int x = 0;
        public C1 next = null;

        public C1(int x0) {
            x = x0;
        }

        public void m() {
        }

        public void ouch() {
            assert false;
        }
    }

    @Test
    public void test1() {
        System.out.println(">>> A class with error...");
        BaseEngine engine = new BaseEngine(C1.class);
        engine.maxNumViolations = 3;
        engine.timeOutPeriod = 4000 ;
        configureOutStreamToDebugStream(engine) ;
        engine.timedRun();
        assert Debug.out.toString().contains("3 assertion violations") ;
    }

    static public class C2 {

        private int x = 0;
        public C2 next = null;

        public C2(int x0) {
            x = x0;
        }

        public void DOG(Object x) {
        }

        public void CAT(C2 y) {
            assert false : "PRE";
        }
    }

    @Test
    public void test2() {
        System.out.println(">>> A class without error, but with false PRE ...");
        BaseEngine engine = new BaseEngine(C2.class);
        configureOutStreamToDebugStream(engine) ;
        engine.timedRun() ;
        assert Debug.out.toString().contains("NO violation found") ;
        assert Debug.out.toString().contains("PRE violations") ;
    }

    static public class C2b extends C2 {

        public C2b(int x0) {
            super(x0);
        }

        public boolean classinv() throws Exception {
            throw new Exception();
        }
    }
    
    @Test
    public void test3() {
        System.out.println(">>> A class whose class invariant throws an exeception ...");
        BaseEngine engine = new BaseEngine(C2b.class);
        engine.maxNumViolations = 3;
        configureOutStreamToDebugStream(engine) ;
        engine.timedRun();
        assert Debug.out.toString().contains("VIOLATIONS FOUND: 3") ;
        assert Debug.out.toString().contains("3 exceptions thrown by class invariant") ;
    }
    
    static public class C4 {

        public C4(){ };
        public C4(C4 x){ }
        
        public void forever(C4 x) { int i=0 ; while (i==0) { ; } }
    }
    
    @Test
    public void test4() {
        System.out.println(">>> A class that loops forever ...");
        BaseEngine engine = new BaseEngine(C4.class);
        configureOutStreamToDebugStream(engine) ;
        engine.timeOutPeriod = 4000 ;
        engine.timedRun();
        assert Debug.out.toString().contains("Possible NON-TERMINATION") ;
        assert Debug.out.toString().contains("VIOLATIONS FOUND: 1") ;
    }
    
}