import org.scribe.model.*

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

import Sequenic.T3.Config
import Sequenic.T3.Pool
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(org.scribe.model.Token.class.getName())
logger.setLevel(Level.SEVERE)

config = new Config(CUT : org.scribe.model.Token,
					regressionMode : true,
					injectOracles : false,
					fieldUpdateProbability : 0,
					maxPrefixLength : 1,
					suiteSizeMultiplierPerGoal : 20
					)
				
static Object genObj(int k) {
	switch (k) {
	 case 0  : println (">> token 1") ; return new Token("sponge","bob") ;
	 case 1  : println (">> token 2") ; return new Token("sponge","square") ;
	 default : println (">> not token") ; return "whatever" ;
	}
}

	
gen1 = FirstOf(
	     new NullMG() .constant() .WithChance(0.2) ,
	     String(OneOf("","sponge","bob","square")),
		 Object(genToken,"genObj",OneOf(0,0,1,2)).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(".","token",false)
inf.save("token.orc")