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 Sequenic.T2.Obj.XShow
import static Sequenic.T2.Obj.T3TestXShow.*

ADTsuites = SUITE.loadMany("ADT_Sequenic\\.T2\\.Obj\\.XShow.*",Common.getTrDir())
println("** Reading " + ADTsuites.size() + " suites") 
nonADTsuites = SUITE.loadMany("nonADT_Sequenic\\.T2\\.Obj\\.XShow.*",Common.getTrDir())
println("** Reading " + nonADTsuites.size() + " suites") 

// configuring CUT's static fields:
CUTconfigure() ;

spec1a  = choare(tt, "XShow",  {s -> s.normal()})  

spec1b  = choare(tt, "XShow",  
                     {s -> (s.args.length==0 && s.retval.maxDepth==5 && s.retval.InitialIndentation==6) ||
                           (s.retval.maxDepth==s.x0() && s.retval.InitialIndentation ==s.x1())       
                      })  
                               
spec2a = hoare(tt, "showWithContNum", {s->s.normal() && !s.retNull()})
spec2b = hoare({s-> s.tobj.maxDepth<=0}, "showWithContNum", {s->s.retval.endsWith("...")})
spec2c = hoare({s-> s.tobj.maxDepth>0 && s.x0()==null}, "showWithContNum",  {s-> s.retval.endsWith("NULL")})    


def primitive(Class C) {
    C==Byte || C==Short || C == Integer || C == Long || C==Character || C==String || C==Float || C==Double || C==Boolean
}

spec2d = hoare({s-> s.tobj.maxDepth>0 && s.x0()!=null && primitive(s.x0().getClass())}, 
               "showWithContNum",  
               {s-> s.retval.indexOf(s.args[0].toString()) >=0 }) 
               
spec2e = hoare({s-> s.tobj.maxDepth>0 && s.x0()!=null && s.x0().getClass().isArray()}, 
               "showWithContNum",  
               {s-> s.retval.indexOf("ARRAY") >=0 })     
               
spec2f = hoare({s-> s.tobj.maxDepth>0 && s.x0()!=null && !s.x0().getClass().isArray()}, 
               "showWithContNum",  
               {s-> s.retval.indexOf(s.x0().getClass().getSimpleName()) >=0 })                            
               
spec2g = hoare({s-> s.tobj.maxDepth>0 && s.x0()!=null && XShow.veryCompactShow.contains(s.x0().getClass())}, 
               "showWithContNum",  
               {s-> s.retval.endsWith("...") })   

// not a general specification! specific for CUT configuration as defined by the call
// configureCUT() above            
spec2hx = hoare({s-> s.tobj.maxDepth>0 && s.x0()!=null && s.x0().getClass()==Link}, 
               "showWithContNum",  
               {s-> s.retval.indexOf("next") >= 0 && s.retval.indexOf("limit") < 0 && s.retval.indexOf("type") < 0})  
               
               
spec3 = hoare(tt,"show",{s-> s.normal() && !s.retNull()})      

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,spec2a,spec2b,spec2c,spec2d,spec2f,spec2g,spec2hx)
allNonADTspecs = always(spec2)