package Examples;

import org.junit.Test;

import static org.junit.Assert.* ;
import Common.Common;
import Sequenic.T3.T3Cmd;
import Sequenic.T3.T3Random;
import Sequenic.T3.Generator.*;
import Sequenic.T3.JavaType.JTypeUtils;
import Sequenic.T3.Sequence.Datatype.*;
import Sequenic.T3.utils.Maybe;
import static Sequenic.T3.Generator.Value.ValueMGCombinators.* ;

public class T3TestBinarySearchTree {
	
	// A simpler variant like the one below does not really  work, because the type-solver
	// would make Comparable to a randomly chosen subclass.
	// static public Generator<PARAM,STEP> myvalgen = Integer(OneOf(0,1,2)) ;

    static public Generator<PARAM,STEP> myvalgen = UnguardedValue(MixedOneOf(1,0,2)).If(isSubclassOf(Comparable.class)) ;
			
    public static void generate(String CUT, boolean withCustomgen, boolean injectOracle) throws Exception {	
    	
		String cvgOption = "" ;
		String oracleOption = "" ;
		if (withCustomgen) cvgOption = " -cvg Examples.T3TestBinarySearchTree " ;
		if (!injectOracle) oracleOption =" -norc " ;
		
		T3Cmd.main("-reg -core 2 -pl 4 -vp -sl 1 -fup 0 -ms 200 " // -ms 300
				+ cvgOption
				+ oracleOption
				+ " -sd " + Common.getCUTrootBindir()
				+ " -d "  + Common.getTrDir()
				+ " " + CUT);						
	}
   
	static String CUT = "Examples.BinarySearchTree" ;
	
    @Test
    public void testPlainWithOracles() throws Throwable { generate(CUT,false,true) ;	}
    
    @Test
    public void testWithCustomGenWithOracles() throws Throwable { generate(CUT,true,true) ;	}
    
    // without injected oracles:
    //@Test
    public void testPlain() throws Throwable { generate(CUT,false,false) ; }

    // without injected oracles:
    //@Test
    public void testWithCustomGen() throws Throwable { generate(CUT,true,false) ; }
    
    //@Test this additional test is no longer needed, the above customgen, with -ms 300 will do
    public void additionaltest() {
    	Examples.BinarySearchTree t = new Examples.BinarySearchTree() ;
    	t.insert(1);
    	t.insert(0);
    	t.insert(2);
    	assertTrue(t.find(1) == (Integer) 1) ;
    	t.remove(1);
    	assertNull(t.find(1)) ;
    }
    
}