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:CUTexamples.Triangle, maxPrefixLength:4)
t3 = new T3groovyAPI(config)
suite = t3.ADT()

myGen = FirstOf(
	Double(OneOf(1d,1d,3d)),
	String(OneOf("scalene","equilateral","isoleces")).If (hasParamName("ty")))

t3b = new T3groovyAPI(myGen,config)
suite = suite + t3b.ADT()

h = hoare( { s -> s.tobj.a>0 && s.tobj.a == s.tobj.c  },
	"isIsoleces",
	{ s -> s.retval })

println ltlquery(suite).with(always(h)).valid()
println ltlquery(suite).with(eventually(h.antecedent())).count()