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_Sequenic\\.T2\\.XPool.*",Common.getTrDir())
println("** Reading " + ADTsuites.size() + " suites") 

spec1  = now choare(tt, "XPool",  {s -> s.normal() && s.retval.get_objectCount()==0 })  

spec2a  = now hoare({s -> 0<=s.x0() && s.x0()<s.tobj.get_objectCount()}, "get",  {s -> s.normal() && !s.retNull() })  
spec2b  = now hoare({s -> s.x0()<0 || s.x0()>=s.tobj.get_objectCount()}, "get",  {s -> s.normal() && s.retNull() })  

spec3a  = now hoare({s-> s.tobj.get(0) == null}, "get_objectCount",  {s -> s.retval == 0})
spec3b  = now hoare({s-> s.tobj.get(0) != null}, "get_objectCount",  {s -> s.retval > 0})
  
spec4  = now hoare(tt, "reset",  {s -> s.exc==null && s.oUT.get_objectCount()==0 })

spec5a = now hoare({s -> s.x0()!=null}, "getIndex", {s -> s.normal()}) 
spec5b = now hoare({s -> s.x0()!=null}, 
				    "getIndex", 
				    {s -> s.retNull() || (0<=s.retval && s.retval < s.oUT.get_objectCount())} ) 
spec5c = now hoare({s -> s.x0()!=null}, 
				    "getIndex",  
				    {s -> s.retNull() || s.x0().isInstance(s.oUT.get(s.retval)) } ) ;
spec5d = now hoare({s -> s.x0()!=null && s.tobj.get_objectCount()>0 }, 
	                "getIndex",  
	                {s -> !s.retNull() || ! s.x0().isInstance(s.oUT.get(0)) }) ;


spec6a = now hoare({s -> s.x0()==null}, "put", {s -> s.threw(NullPointerException)})
spec6b = now hoare({s -> s.x0()!=null}, "put", {s -> s.oUT.get_objectCount() > s.retval})
spec6c = now hoare({s -> s.x0()!=null}, "put", {s -> s.oUT.get(s.retval) == s.x0()})


//spec7x = now hoare(tt, "put", {s -> s.exc != null})


allSpecs = always(spec1 & spec2a & spec2b 
                  & spec3a & spec3b & spec4
                  & spec5a & spec5b & spec5c & spec5d
                  & spec6a & spec6b & spec6c)

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