package Sequenic.T2;

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

import Common.Common;
import Sequenic.T2.XPool;


//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 ReplayTestXPool {
	
	@Test
    public void test1() throws Throwable {	Common.replayCUTtest("Sequenic.T2.XPool"); }
	
	static Predicate<PreState> tt = s -> true ;
	static XPool xpool(Object o) { return (XPool) o ; }
	static int int_(Object o) { return (Integer) o ; }
	static Class class_(Object o) { return (Class) o ; }
	
	LTL spec() {
		LTL spec1  = now(choare(tt, "XPool",  s -> s.normal() && xpool(s.getRetval()).get_objectCount()==0 )) ;  
		
		LTL spec2a = now(hoare(s -> 0<=int_(s.x0()) && int_(s.x0()) < xpool(s.getTobj()).get_objectCount(), 
		                       "get",  
		                        s -> s.normal() && !s.retNull())) ;
		
		LTL spec2b = now(hoare(s -> int_(s.x0())<0 || int_(s.x0()) >= xpool(s.getTobj()).get_objectCount(), 
				              "get",  
				              s -> s.normal() && s.retNull())) ;
		
		LTL spec3a  = now(hoare(s-> xpool(s.getTobj()).get(0) == null, "get_objectCount",  s -> int_(s.getRetval()) == 0)) ;
		LTL spec3b  = now(hoare(s-> xpool(s.getTobj()).get(0) != null, "get_objectCount",  s -> int_(s.getRetval()) > 0 )) ;
		
		LTL spec4  = now(hoare(tt, "reset",  s -> s.normal() && xpool(s.getOUT()).get_objectCount()==0 )) ;

		LTL spec5a = now(hoare(s -> s.x0()!=null, "getIndex", s -> s.normal())) ;
		LTL spec5b = now(hoare(s -> s.x0()!=null, 
				               "getIndex", 
				               s -> s.retNull()
				                    || (0<=int_(s.getRetval()) && int_(s.getRetval()) < xpool(s.getOUT()).get_objectCount()))) ;

		LTL spec5c = now(hoare(s -> s.x0()!=null, 
				               "getIndex",  
				               s -> s.retNull() || class_(s.x0()).isInstance(xpool(s.getOUT()).get(int_(s.getRetval()))))) ;
		
		LTL spec5d = now(hoare(s -> s.x0()!=null && xpool(s.getTobj()).get_objectCount()>0  , 
	               "getIndex",  
	               s -> !s.retNull() || !class_(s.x0()).isInstance(xpool(s.getOUT()).get(0)))) ;
		
		LTL spec6a = now(hoare(s -> s.x0()==null, "put", s -> s.threw(NullPointerException.class))) ;
		LTL spec6b = now(hoare(s -> s.x0()!=null, "put", s -> xpool(s.getOUT()).get_objectCount() > int_(s.getRetval()))) ;
		LTL spec6c = now(hoare(s -> s.x0()!=null, "put", s -> xpool(s.getOUT()).get(int_(s.getRetval())) == s.x0())) ;

		
		return always(spec1.and(spec2a).and(spec2b).
				      and(spec3a).and(spec3b).and(spec4).
				      and(spec5a).and(spec5b).and(spec5c).and(spec5d).
				      and(spec6a).and(spec6b).and(spec6c)      
				      ) ;
	}
	 
	//@Test
	public void checkSpec() throws Throwable {	
		boolean ok =  Common.checkSpecification("ADT_Sequenic\\.T2\\.XPool.*",spec()); 
		assertTrue(ok) ;
	}
}