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.AlgQuery.*
import Sequenic.T3.SuiteUtils.SuitePrinter.Printer

import Common.Common

ADTsuites = SUITE.loadMany("ADT_Examples\\.Tri.*",Common.getTrDir())
println("** Reading " + ADTsuites.size() + " suites") 

spec1  = now hoare(tt, "isScalene",  {s -> s.retval == !s.oUT.isIsoleces() })  
spec2  = now hoare(tt, "isIsoleces", {s -> s.retval == !s.oUT.isScalene() }) 
spec3 = now hoare(tt, "isEquilateral", {s -> s.retval == (s.oUT.a == s.oUT.b && s.oUT.b==s.oUT.c) }) 
//spec4a = now choare(tt, "Triangle", {s -> if (s.retval == null) true ; else s.retval.a>0 && s.retval.b>0 && s.retval.c>0 ;})
spec4a = now choare({s -> s.args[0] > 0 && s.args[1] > 0 && s.args[2] > 0}, "Triangle", { s -> s.exc == null && s.retval!=null})
spec4b = now choare({s -> s.args[0] <= 0 || s.args[1] <= 0 || s.args[2] <= 0}, "Triangle", { s -> s.exc != null })
allSpecs = always(spec1 & spec2 & spec3 & spec4a & spec4b)

if (ltlvalid(ADTsuites,allSpecs)) println "**true**" ; else println "**false**"