import net.sf.javaml.core.* 

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

import Sequenic.T3.Config
import Sequenic.T3.Sequence.Datatype.SUITE
import Sequenic.T3.Generator.Generator
import static Sequenic.T3.Generator.GenCombinators.FirstOf
import static Sequenic.T3.Generator.Value.ValueMGCombinators.*
import Sequenic.T3.T3groovyAPI
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(net.sf.javaml.core.DenseInstance.class.getName())
logger.setLevel(Level.SEVERE)

config = new Config(CUT : net.sf.javaml.core.DenseInstance,
					regressionMode : true,
					injectOracles : false,
					fieldUpdateProbability : 0,
					maxPrefixLength : 5,
					suiteSizeMultiplierPerGoal : 8	)

static Object genDI(int k) {
	switch (k) {
	 case 0 : println (">> DI 1") ; return new DenseInstance(null) ;
	 case 1 : double[] a = [0] ; println (">> DI 2") ; return new DenseInstance(a) ;  }
}

gen1 =  FirstOf(
	   Serializable(MixedOneOf(-1i,0i,1i,2i,3i)).If(hasParamName("key")),
	   Serializable(MixedOneOf(-1d,0d,1d,2d,3d)).If(hasParamName("value")),
	   Object(genDenseInstance,"genDI",OneOf(0,1,1)).If(hasClass(Object)).If(hasParamName("obj"))
	)

t3a  = new T3groovyAPI(config)
t3b  = new T3groovyAPI(gen1,config)
generator = { t3a.ADT() + t3b.ADT() }
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)
t3a.info(suite)
inf.cleanup().print()
if (k!=null) println ">> oracles consistent after " + k + " iterations" ; else println ">> oracles still inconsistent "
suite.save(".","denseInstance",false)
inf.save("denseInstance.orc")

//inf2   = SubcaseInvariantFile.load("denseInstance.orc").withLogger(logger) ;
//suite2 = SUITE.load("denseInstance.tr") ;
//println inf2.check(suite2)