package Sequenic.T2.Obj;

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

import Common.Common;
import Sequenic.T2.XPool;
import Sequenic.T2.Obj.XShow ;
import Sequenic.T2.Obj.T3TestXShow ;
import static Sequenic.T2.Obj.T3TestXShow.* ;

//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 ReplayTestXShow {
	
	@Test
    public void test1() throws Throwable {
		T3TestXShow.CUTconfigure() ;
		XShow.Debug = false ;
		Common.replayCUTtest("Sequenic.T2.Obj.XShow"); 
	}
	
	@Test
    public void test2() throws Throwable {
		T3TestXShow.CUTconfigure() ;
		XShow.Debug = true ;
		Common.replayCUTtest("Sequenic.T2.Obj.XShow"); 
	}

	static Predicate<PreState> tt = s -> true ;
	static XShow xshow(Object o) { return (XShow) o ; }
	static String string_(Object o) { return (String) o ; }
	static int int_(Object o) { return (Integer) o ; }
	static Class class_(Object o) { return (Class) o ; }
    
	boolean primitive(Class C) {
	    return C==Byte.class || C==Short.class || C == Integer.class || C == Long.class 
	    	   || C==Character.class || C==String.class || C==Float.class || C==Double.class || C==Boolean.class ;
	}

	LTL adtSpec() {
		
		Hoare spec1a  = choare(tt, "XShow",  s -> s.normal()) ;
		
		Hoare spec1b  = choare(tt, 
				          "XShow",  
                           s -> (s.getArgs().length==0 && xshow(s.getRetval()).maxDepth==5 
                                                       && xshow(s.getRetval()).InitialIndentation==6) 
                             || (xshow(s.getRetval()).maxDepth==int_(s.x0()) && xshow(s.getRetval()).InitialIndentation == int_(s.x1()))       
                          ) ; 
		
		Hoare spec2a = hoare(tt, "showWithContNum", s->s.normal() && !s.retNull()) ;
		Hoare spec2b = hoare(s-> xshow(s.getTobj()).maxDepth<=0, 
				             "showWithContNum", 
				             s-> string_(s.getRetval()).endsWith("...")) ;
		Hoare spec2c = hoare(s-> xshow(s.getTobj()).maxDepth>0 && s.x0()==null, 
				             "showWithContNum",  
				              s-> string_(s.getRetval()).endsWith("NULL")) ;  
		
		Hoare spec2d = hoare(s-> xshow(s.getTobj()).maxDepth>0 && s.x0()!=null && primitive(s.x0().getClass()), 
		               "showWithContNum",  
		               s-> string_(s.getRetval()).indexOf(s.x0().toString()) >=0 ) ; 
		
		Hoare spec2e = hoare(s-> xshow(s.getTobj()).maxDepth>0 && s.x0()!=null && s.x0().getClass().isArray(), 
	                   "showWithContNum",  
	                    s-> string_(s.getRetval()).indexOf("ARRAY") >=0 ) ;     
	               
	    Hoare spec2f = hoare(s-> xshow(s.getTobj()).maxDepth>0 && s.x0()!=null && !s.x0().getClass().isArray(), 
	                   "showWithContNum",  
	                    s-> string_(s.getRetval()).indexOf(s.x0().getClass().getSimpleName()) >=0 ) ;                            
	               
	    Hoare spec2g = hoare(s-> xshow(s.getTobj()).maxDepth>0 && s.x0()!=null && XShow.veryCompactShow.contains(s.x0().getClass()), 
	                   "showWithContNum",  
	                    s-> string_(s.getRetval()).endsWith("...") ) ; 
		
		Hoare spec2hx = hoare(s-> xshow(s.getTobj()).maxDepth>0 && s.x0()!=null && s.x0().getClass()==Link.class, 
	                          "showWithContNum",  
	                          s-> string_(s.getRetval()).indexOf("next") >= 0 
	                              && string_(s.getRetval()).indexOf("limit") < 0 
	                              && string_(s.getRetval()).indexOf("type") < 0  )  ; 
		
		return Always(spec1a,spec1b,spec2a,spec2b,spec2c,spec2d,spec2e,spec2f,spec2g,spec2hx) ;
	}
	
	LTL nonAdtSpec() {
		Hoare spec3 = hoare(tt, "show", s-> s.normal() && !s.retNull()) ;  
		return always(spec3) ;
	}
	
	
	//@Test
	public void checkADTSpec1() throws Throwable {	
		T3TestXShow.CUTconfigure() ;
		XShow.Debug = false ;
		boolean ok =  Common.checkSpecification("ADT_Sequenic\\.T2\\.Obj\\.XShow.*",adtSpec()); 
		assertTrue(ok) ;
	}
	
	//@Test
	public void checkADTSpec2() throws Throwable {	
		T3TestXShow.CUTconfigure() ;
		XShow.Debug = true ;
		boolean ok =  Common.checkSpecification("ADT_Sequenic\\.T2\\.Obj\\.XShow.*",adtSpec()); 
		assertTrue(ok) ;
	}
	
	//@Test
	public void checkNonADTSpec1() throws Throwable {	
		T3TestXShow.CUTconfigure() ;
		XShow.Debug = false ;
		boolean ok =  Common.checkSpecification("nonADT_Sequenic\\.T2\\.Obj\\.XShow.*",nonAdtSpec()); 
		assertTrue(ok) ;
	}
	
	//@Test
	public void checkNonADTSpec2() throws Throwable {	
		T3TestXShow.CUTconfigure() ;
		XShow.Debug = true ;
		boolean ok =  Common.checkSpecification("nonADT_Sequenic\\.T2\\.Obj\\.XShow.*",nonAdtSpec()); 
		assertTrue(ok) ;
	}
	
	static class Point {
		int x = 99 ;
		int y = -1 ;
	}
	
    //@Test
    public void additionalTest()  {
    	List<String> includedFields = new LinkedList<String>() ; includedFields.add("x") ;
    	Sequenic.T2.Obj.XShow.showFilter.put(Point.class,includedFields) ;
    	String s = Sequenic.T2.Obj.XShow.show(new Point()) ;
    	System.out.println("+++ " + s) ;
    	assertTrue(s.contains("Point")) ;
    	assertTrue(s.contains("x (Integer)")) ;
    	assertFalse(s.contains("y (Integer)")) ;
    }

}