package org.scribe.model;

import org.junit.Test;

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

import org.scribe.model.Token ;



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

import Sequenic.T2.XPool;
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 ReplayTestToken {
	
	@Test
    public void test1() throws Throwable {	Common.replayCUTtest("org.scribe.model.Token"); }

	static Predicate<PreState> tt = s -> true ;
	static Token token(Object o) { return (Token) o ; }
	static boolean bool(Object o) { return (Boolean) o ; }
	
	LTL join(Hoare... specs) {
		LTL S = now(specs[0]) ;
		for (int k=1; k<specs.length; k++) S = S.and(specs[k]) ;
		return always(S) ;
	}
	
	boolean rawResponseCrashes(Token tok) {
	    try{ tok.getRawResponse() ; }
	    catch(IllegalStateException e) { return true ; }
	    return false ;
	}
	
	LTL adtSpec() {
		Hoare spec1a = choare(s-> s.x0()==null || s.x1()==null, "Token", s-> s.threw(IllegalArgumentException.class)) ;
		Hoare spec1b = choare(s-> s.x0()!=null && s.x1()!=null,
                "Token",
                s-> token(s.getRetval()).getToken()==s.x0() && token(s.getRetval()).getSecret()==s.x1()) ;
		Hoare spec1c = choare(s-> s.x0()!=null && s.x1()!=null && (s.getArgs().length==2 || s.x2()==null),
                "Token",              
                s -> rawResponseCrashes(token(s.getRetval()))) ; 
		Hoare spec1d = choare(s-> s.x0()!=null && s.x1()!=null && (s.getArgs().length==3 && s.x2()!=null),
                "Token",              
                s -> token(s.getRetval()).getRawResponse()==s.x2() ) ;   
		
		Hoare spec3a = hoare(tt,"equals",s -> s.normal()) ;
		Hoare spec3b = hoare(s-> s.x0()==null,"equals", s-> ! bool(s.getRetval())) ;
		Hoare spec3c = hoare(s-> s.x0()==s.getTobj(),"equals", s-> bool(s.getRetval())) ;
		Hoare spec3d = hoare(tt,
				            "equals", 
				             s-> !bool(s.getRetval()) 
				             || (token(s.getOUT()).getToken().equals(token(s.x0()).getToken())  
				                 && token(s.getOUT()).getSecret().equals(token(s.x0()).getSecret())
				                 ) ) ;
		
	    Hoare spec3e = hoare(s-> s.x0()!=null,"equals", s-> bool(s.getRetval()) == (token(s.getOUT()).hashCode()==s.x0().hashCode()) ) ;
		Hoare spec3f = hoare(s-> s.x0()!=null,"equals", s-> bool(s.getRetval()) == (token(s.getOUT()).toString().equals(s.x0().toString())) ) ;

		Hoare spec4 = hoare(tt,"hashCode", s-> s.normal()) ;
		Hoare spec5 = hoare(tt,"toString", s-> s.normal()) ;
		
		Hoare spec6a = hoare(tt,"isEmpty", s -> s.normal()) ;
		Hoare spec6b = hoare(tt,"isEmpty", s -> bool(s.getRetval()) == (token(s.getOUT()).getToken().equals("") && token(s.getOUT()).getSecret().equals(""))) ;

		//return join(spec3d) ;
		return join(spec1a,spec1b,spec1c,spec1d,spec3a,spec3b,spec3c,spec3d,spec3e,spec3f,spec4,spec5,spec6a,spec6b) ;
	}
	
	LTL nonAdtSpec() {
		Hoare spec2 = hoare(tt,"empty",s -> s.normal() && token(s.getRetval()).isEmpty()) ;
		return join(spec2) ;
	}

	//@Test
	public void checkADTSpec() throws Throwable {	
		boolean ok =  Common.checkSpecification("ADT_org\\.scribe\\.model\\.Token.*",adtSpec()); 
		assertTrue(ok) ;
	}
	
	//@Test
	public void checkNonADTSpec() throws Throwable {	
		boolean ok =  Common.checkSpecification("nonADT_org\\.scribe\\.model\\.Token.*",nonAdtSpec()); 
		assertTrue(ok) ;
	}
}