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(Examples.Triangle.class.getName())
logger.setLevel(Level.SEVERE)

config = new Config(CUT : Examples.Triangle, regressionMode:true, injectOracles:false, maxPrefixLength:4)
t3a = new T3groovyAPI(config)
gen1 = Double(OneOf(-1d,0d,1d,1d,2d,3d))
t3b = new T3groovyAPI(gen1,config)
gen2 = Double(OneOf(0.001d,999d))
t3c = new T3groovyAPI(gen2,config)
//gen4 = Double(OneOf(0d))
//t3e = new T3groovyAPI(gen4,config)
suitegen = { -> t3a.ADT() + t3b.ADT() + t3c.ADT() }
suite = suitegen()

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