package Examples;

import org.junit.Test;

import static org.junit.Assert.*;
import Common.Common;




//imports to support query:
import java.util.function.*;
import java.util.*;

import Sequenic.T3.Sequence.Datatype.SUITE ;
import Sequenic.T3.SuiteUtils.Query.* ;
import Sequenic.T3.SuiteUtils.Query.SeqPredicate.LTL;
import Sequenic.T3.SuiteUtils.Query.State.PreState;
import static Sequenic.T3.SuiteUtils.Query.State.* ;
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.* ;

public class ReplayTestBinarySearchTree {
	
	@Test
    public void test1() throws Throwable {	
		Common.replayCUTtest("Examples.BinarySearchTree");
    }

	static Predicate<PreState> tt = s -> true ;
	static BinarySearchTree bst(Object o) { return (BinarySearchTree) o ; }
	static boolean bool(Object o) { return (Boolean) o ; }
	static Comparable comparable(Object o) { return (Comparable) o ; }
	
	LTL spec() {
		LTL spec1 =  now(choare(tt,"BinarySearchTree",s-> bst(s.getRetval()).isEmpty())) ;
		LTL spec2 =  now(hoare(tt,"makeEmpty",s-> bst(s.getOUT()).isEmpty())) ;
		LTL spec3a = now(hoare(s-> s.getArgs()[0]==null, "remove", s-> s.getExc()!=null)) ;
		LTL spec3b = now(hoare(s-> s.getArgs()[0]!=null , 
				               "remove", 
                               s-> (s.getExc() != null && (s.getExc() instanceof ClassCastException)) 
                                   || bst(s.getOUT()).find(comparable(s.getArgs()[0]))==null)) ;
                
		LTL spec4a = now(hoare(s-> s.getArgs()[0]==null, "insert", s-> s.getExc()!=null)) ;
		LTL spec4b = now(hoare(s-> s.getArgs()[0]!=null, 
				               "insert", 
                               s-> {
                            	   if (s.getExc() != null && (s.getExc() instanceof ClassCastException)) return true ;
                            	   BinarySearchTree t = bst(s.getOUT()) ;
                            	   Comparable x = comparable(s.getArgs()[0]) ;
                                   return t.find(x).equals(x) ;
                                   }
                               )) ;
		
		LTL spec5a = now(hoare(s-> s.getArgs()[0]==null, "find", s-> s.getExc()!=null)) ;
		LTL spec5b = now(hoare(s-> s.getArgs()[0]!=null && bst(s.getTobj()).isEmpty(), 
				               "find", 
				               s-> bst(s.getOUT()).find(comparable(s.getArgs()[0]))==null)) ;
		LTL spec5c = now(hoare(tt, 
				               "find", 
                               s-> s.getExc() != null || s.getRetval()==null 
                               || (comparable(s.getRetval()).compareTo(bst(s.getOUT()).findMax()) <= 0 
                            		   && comparable(s.getRetval()).compareTo(bst(s.getOUT()).findMin()) >= 0 ))) ;  
                
		LTL spec6a = now(hoare(tt,"isEmpty", s-> bool(s.getRetval()) == (bst(s.getOUT()).findMin() == null))) ;
		LTL spec6b = now(hoare(tt,"isEmpty", s-> bool(s.getRetval()) == (bst(s.getOUT()).findMax() == null))) ;
		
		LTL allspecs = always(spec1.and(spec2).
				             and(spec3a).and(spec3b).
				             and(spec4a).and(spec4b).
				             and(spec5a).and(spec5b).and(spec5c).
				             and(spec6a).and(spec6b)) ;
		
		return allspecs ;
	}
	
	//@Test
	public void checkSpec() throws Throwable {	
		boolean ok =  Common.checkSpecification("ADT_Examples\\.Bin.*",spec()); 
		assertTrue(ok) ;
	}
}