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


config = new Config(CUT : Sequenic.T3.Examples.Item.class, 
                    fieldUpdateProbability : 0,
                    maxSuffixLength : 10,
                    suiteSizeMultiplierPerGoal : 5
                    )
t3 = new T3groovyAPI(config)
S = t3.ADT()
eq0 = (clause("getCode()") >> { s -> s.oUT }) . equiv Epsilon
eq1 = (clause("getCode()") >> { s -> s.oUT }) . equiv (clause("getCode()"))
eq2 = (clause("setCode(x)") >> { s -> s.oUT }) . equiv (clause("setCode(x)") >> { s -> s.oUT })
eq2b = (clause("resetCode();setCode(x)") >> { s -> s.oUT }) . equiv (clause("setCode(x)"))
eq3 = (clause("setCode()") >> { s -> 0 }) . equiv (clause("setCode()") >> { s -> 0 })

// not valid:
eq4 = (clause("getCode()") >> { s -> true }) . equiv (clause("getCode()") >> {s-> s.retval != null}) 
// valid:
eq4b = (clause("setCode(x)") >> { s -> s.retval != null }) . equiv (clause("setCode(x);getCode()") >> {s-> s.retval != null})


println(eq0.show())
algquery(S).with(eq0).print()
//S.suite.get(0).exec(config.CUT, new Pool(), null, 0, 4, System.out)