import Sequenic.T2.Obj.*
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.Obj.XShow.class.getName())
logger.setLevel(Level.SEVERE)

config = new Config(CUT : Sequenic.T2.Obj.XShow,
	regressionMode : true,
	injectOracles : false,
	fieldUpdateProbability : 0,
	maxPrefixLength : 1,
	suiteSizeMultiplierPerGoal : 10
	)

static Object genObj(int k) {
	switch (k) {
	   case 0 : println (">> SomeObject") ; return new SomeObject() ;
	   case 1 : println (">> Pair")  ; return new Pair("sponge", new Pair("bob",null)) ;
	   case 2 : println (">> list")  ; return [1,2,3,4,5,6,7,8,9] ;
	   case 3 : println (">> map")   ; Map h = new HashMap() ;  h.put(99,"99"); return h ;
	   case 4 : println (">> file")  ; return new File("sometestfile") ;
	   default : println (">> object") ; return new Object() ;
	   }
}

gen1 = FirstOf(
	new NullMG() .constant() .WithChance(0.2) ,
	Object(genXShow,"genObj",OneOf(0,1,2,3,4,5)).If(hasClass(Object))
)

t3  = new T3groovyAPI(gen1,config)
generator = { t3.ADT() + t3.nonADT() }
suite = generator() 

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