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

// An example of querying a Hoare triple.

config = new Config(CUT : Sequenic.T3.Examples.Item)
t3 = new T3groovyAPI(config)
// generate a suite:
S = t3.ADT()
// an example of Hoare triple:
h1 =  hoare({s-> s.args[0]>0 & s.tobj.price>0},"incPrice",{s-> s.tobj.price>s.args[0]})
// queries:   
ltlquery(S).with(always(h1)).valid()
ltlquery(S).with(always(h1)).print()
ltlquery(S).with(eventually(h1.antecedent())).count()