import java.util.logging.Logger;

import CUTexamples.TriFloatsWithLogging;
import Sequenic.T3.Config
import Sequenic.T3.Pool
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.SuitePrinter.Printer
import Sequenic.T3.SuiteUtils.Inference.InvariantFile
import Sequenic.T3.SuiteUtils.Inference.SubcaseInvariantFile
import Sequenic.T3.SuiteUtils.Inference.Aggregate.AggregateInvariantGroup
config = new Config(CUT : CUTexamples.TriFloatsWithLogging, fieldUpdateProbability : 0, suiteSizeMultiplierPerGoal : 10)
t3 = new T3groovyAPI(config)
myGen = Float(OneOf(-1f,0f,1f,2f))
t3b = new T3groovyAPI(myGen,config)

S1 = t3.ADT() 
// infer structural change oracles from S1:
logger = Logger.getLogger(TriFloatsWithLogging.class.getName())
inf = new SubcaseInvariantFile(logger)
double[] bounds = [-1d,0d,1d,2d]
inf.addDiscreteBounds(".", bounds)
inf.read(S1).consolidate().print()
inf.read(t3.ADT()).consolidate().print()
inf.read(t3.ADT()).consolidate().print()
inf.read(t3b.ADT()).consolidate().print()