import Sequenic.T2.*
import Sequenic.T3.utils.*

import java.util.logging.Logger
import java.util.logging.Level

import Sequenic.T3.Config
import Sequenic.T3.Pool
import Sequenic.T3.Sequence.Datatype.PARAM;
import Sequenic.T3.Sequence.Datatype.STEP;
import Sequenic.T3.Sequence.Datatype.SUITE
import Sequenic.T3.Examples.Friends.Email;
import Sequenic.T3.Generator.Generator
import static Sequenic.T3.Generator.GenCombinators.FirstOf
import static Sequenic.T3.Generator.Value.ValueMGCombinators.*
import Sequenic.T3.Generator.Value.*
import Sequenic.T3.T3groovyAPI
import Sequenic.T3.T3instrGroovyAPI
import Sequenic.T3.SuiteUtils.Query.*
import static Sequenic.T3.SuiteUtils.Query.StepPredicate.*
import static Sequenic.T3.SuiteUtils.Query.SeqPredicate.*
import static Sequenic.T3.SuiteUtils.Query.LTLQuery.*
import static Sequenic.T3.SuiteUtils.Query.Alg2Query.*
import static Sequenic.T3.SuiteUtils.Query.Equation.*
import Sequenic.T3.SuiteUtils.Inference.InvariantFile
import Sequenic.T3.SuiteUtils.Inference.SubcaseInvariantFile

logger = Logger.getLogger(Sequenic.T2.XPool.class.getName())
logger.setLevel(Level.SEVERE)

config = new Config(CUT : Sequenic.T2.XPool,
	regressionMode : true,
	injectOracles : false,
	fieldUpdateProbability : 0,
	maxPrefixLength : 5,
	maximizePrefix : false,
	suiteSizeMultiplierPerGoal : 20
	)

static Object genObj(int k) {
switch (k) {
   case 0  : println (">> SomeObject") ; return new SomeObject() ;
   case 1  : println (">> Pair") ; return new Pair("sponge","bob") ;
   case 2  : println (">> Unit") ; return new Unit() ;
   default : println (">> Object") ; return new Object() ;
   }
}

gen1 = FirstOf(
    new NullMG() .constant() .WithChance(0.1) ,
	UnguardedValue(MixedOneOf(Object,Unit,SomeObject,Pair,String,Integer)).If(hasClass(Class.class)),
    Object(genXPool,"genObj",OneOf(0,1,2,3)).If(hasClass(Object))
)

t3a  = new T3groovyAPI(config)
t3b  = new T3groovyAPI(gen1,config)
adtgenerator = { t3a.ADT() + t3b.ADT() }
suiteNonADT = t3a.nonADT()
suite = adtgenerator() + suiteNonADT

// infer oracles from the suite:
inf = new SubcaseInvariantFile().withLogger(logger)
double[] bounds = [0]
inf.addDiscreteBounds(".", bounds)
inf.read(suite)
k = inf.infer(adtgenerator, 8)
t3a.info(suite)
inf.cleanup().print()
if (k!=null) println ">> oracles consistent after " + k + " iterations" ; else println ">> oracles still inconsistent "
suite.save(".","xpool",false)
inf.save("xpool.orc")