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
import org.scribe.model.Token

ADTsuites = SUITE.loadMany("ADT_org\\.scribe.*",Common.getTrDir())
println("** Reading " + ADTsuites.size() + " suites") 
nonADTsuites = SUITE.loadMany("nonADT_org\\.scribe.*",Common.getTrDir())
println("** Reading " + nonADTsuites.size() + " suites") 

spec1a = choare({s-> s.x0()==null || s.x1()==null},"Token",{s-> s.threw(IllegalArgumentException)})
spec1b = choare({s-> s.x0()!=null && s.x1()!=null},
                "Token",
                {s-> s.retval.getToken()==s.x0() && s.retval.getSecret()==s.x1()})
              
def rawResponseCrashes(Token tok) {
    try{ tok.getRawResponse() }
    catch(IllegalStateException e) { return true }
    return false 
}          
              
spec1c = choare({s-> s.x0()!=null && s.x1()!=null && (s.args.length==2 || s.x2()==null)},
                "Token",              
                {s -> rawResponseCrashes(s.retval)} ) 
                
spec1d = choare({s-> s.x0()!=null && s.x1()!=null && (s.args.length==3 && s.x2()!=null)},
                "Token",              
                {s -> s.retval.getRawResponse()==s.x2()} )                 
                
spec2 = hoare(tt,"empty",{s -> s.normal() && s.retval.isEmpty()})

spec3a = hoare(tt,"equals",{s -> s.normal()})
spec3b = hoare({s-> s.x0()==null},"equals",{s-> ! s.retval})
spec3c = hoare({s-> s.x0()==s.tobj},"equals",{s-> s.retval})
spec3d = hoare(tt,"equals",{s-> !s.retval || (s.oUT.getToken()==s.x0().getToken()  && s.oUT.getSecret()==s.x0().getSecret()) })
spec3e = hoare({s-> s.x0()!=null},"equals",{s-> s.retval == (s.oUT.hashCode()==s.x0().hashCode()) })
spec3f = hoare({s-> s.x0()!=null},"equals",{s-> s.retval == (s.oUT.toString()==s.x0().toString()) })

spec4 = hoare(tt,"hashCode", {s-> s.normal()})
spec5 = hoare(tt,"toString", {s-> s.normal()})

spec6a = hoare(tt,"isEmpty", {s -> s.normal()}) 
spec6b = hoare(tt,"isEmpty", {s -> s.retval == (s.oUT.getToken() == "" && s.oUT.getSecret()=="")}) ;


def join(Hoare... hs) {
    LTL phi = now(hs[0])
    for(int i=1; i<hs.length; i++) phi = phi.and(hs[i]) 
    return always(phi)   
}

allADTspecs = join(spec1a,spec1b,spec1c,spec1d,spec3a,spec3b,spec3c,spec3d,spec3e,spec3f,spec4,spec5,spec6a,spec6b)
allNonADTspecs = always(spec2)