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

/*
not a complete axiomatization: e.g. it doesn't say that insert(x) does not remove 
the elements already in the tree. To express this algquery need to be upgraded
to support more sophisticated variables binding --> todo.

constructor { isEmpty }
makeEmpty { isEmpty }
remove(x) { find(x) == null }
insert(x) { find(x)==x && ! empty }
find(x) { x!=null ==>  x<= findMax && findMin <= x }
isEmpty { retval ==  true ==> (!x. find(x) == null) }

*/

spec1  = now choare(tt,"BinarySearchTree",{s-> s.retval.isEmpty()})
spec2  = now hoare(tt,"makeEmpty",{s-> s.oUT.isEmpty()})

// this seems to be valid, but it is not!, 
// spec3a = now hoare({s-> s.args[0]==null},"remove",{s-> s.exc != null})
// when the tree is empty, it throws an exception. BUG. We should constrain
// remove(x), where x should not be allowed to be null

// Similarly, we also find a BUG to the interplat between insert(x) and find(x).
// insert(null) on an empty tree will actyally insert the null. Then find(x)
// will crash. 
// Fix: disallow null to be inserted.

spec3a = now hoare({s-> s.args[0]==null }, "remove", {s-> s.exc!=null})
spec3b = now hoare({s-> s.args[0]!=null }, "remove", 
                   {s-> (s.exc != null && (s.exc instanceof java.lang.ClassCastException)) || (s.oUT.find(s.args[0])==null)})

spec4a = now hoare({s-> s.args[0]==null }, "insert", {s-> s.exc!=null})
spec4b = now hoare({s-> s.args[0]!=null }, "insert", 
                   {s-> (s.exc != null && (s.exc instanceof java.lang.ClassCastException)) || (s.oUT.find(s.args[0])==s.args[0])})

     
spec5a = now hoare({s-> s.args[0]==null }, "find", {s-> s.exc!=null})
spec5b = now hoare({s-> s.args[0]!=null && s.tobj.isEmpty() }, "find", {s-> s.oUT.find(s.args[0])==null})
spec5c = now hoare(tt, "find", 
                   {s-> s.exc != null || s.retval==null || (s.retval <= s.oUT.findMax() && s.retval >= s.oUT.findMin())})     
                  
spec6a = now hoare(tt,"isEmpty", {s-> s.retval == (s.oUT.findMin() == null)})
spec6b = now hoare(tt,"isEmpty", {s-> s.retval == (s.oUT.findMax() == null)})

allSpecs = always(spec1 & spec2 & spec3a & spec3b & spec4a & spec4b & spec5a & spec5b & spec5c& spec6a & spec6b)


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