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

config = new Config(CUT : Examples.PriorityQueue, 
	                regressionMode:true, 
					injectOracles:false, 
					maxPrefixLength:8,
					maximizePrefix : false,
	                suiteSizeMultiplierPerGoal : 10
	                )
t3a = new T3groovyAPI(config)
gen1 = Integer(OneOf(-1,0,1,3,5,10,11,15)).If(hasClass(Comparable))
t3b = new T3groovyAPI(gen1,config)
suitegen = { -> t3a.ADT() + t3b.ADT() }
suite = suitegen()

// infer oracles from the suite:
inf = new SubcaseInvariantFile(threshold:5 , relativeThreshold:0.001).withLogger(logger)
//double[] bounds = [0d,1d]
//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(".","pqueue",false)
inf.save("pqueue.orc")