package Examples;
import org.junit.* ;

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

import Examples.Triangle;

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

import Sequenic.T3.Sequence.Datatype.SUITE ;
import Sequenic.T3.SuiteUtils.Query.* ;
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 ReplayTestTriangle {

	@Test
    public void test1() throws Throwable {	Common.replayCUTtest("Examples.Triangle"); }
    
	//static boolean implies(boolean a, boolean b) { return !a || b ; }
	static Predicate<PreState> tt = s -> true ;
	static Triangle triangle(Object o) { return (Triangle) o ; }
	
	LTL spec() {
		LTL test  = now(hoare(tt,"isScalene", s -> { System.err.println("##" + triangle(s.getOUT()).isIsoleces()) ; return   true ; })) ;
		
		LTL spec1  = now(hoare(tt, "isScalene",  s -> ((boolean) s.getRetval()) == ! triangle(s.getOUT()).isIsoleces())) ;
		LTL spec2  = now(hoare(tt, "isIsoleces", s -> ((boolean) s.getRetval()) == ! triangle(s.getOUT()).isScalene())) ; 
		LTL spec3 = now(hoare(tt, "isEquilateral",
				          s -> {
				        	  Triangle t = triangle(s.getOUT()) ;
				        	  return ((boolean) s.getRetval()) == (t.a == t.b && t.b == t.c) ;
				          }
				)) ;
		
		/* spec3a and 3b do not unfortunately form a complete specification for equilatal
		
		LTL spec3a = now(hoare(tt, "isEquilateral", s -> implies((boolean)s.getRetval() , 
				triangle(s.getOUT()).isIsoleces()
				&& ! triangle(s.getOUT()).isScalene()
				))) ; 
		LTL spec3b = now(hoare(tt, "isEquilateral", 
				         s -> implies(!(boolean) s.getRetval() , 
				        		      triangle(s.getOUT()).isIsoleces() || triangle(s.getOUT()).isScalene())));
		*/
		
		LTL spec4a = now(choare(s -> ((double) s.getArgs()[0])>0 && ((double) s.getArgs()[1])>0 && ((double) s.getArgs()[2])>0, 
				         "Triangle", 
				         s -> s.getRetval() != null)) ;
		
		LTL spec4b = now(choare(s -> ((double) s.getArgs()[0]) <= 0 || ((double) s.getArgs()[1]) <= 0 || ((double) s.getArgs()[2]) <= 0, 
		                        "Triangle", 
		                        s -> s.getExc() != null )) ;
		
		//LTL allSpecs = always(spec1.and(spec2).and(spec3a).and(spec3b).and(spec4a).and(spec4b)) ;
		LTL allSpecs = always(spec1.and(spec2).and(spec3).and(spec4a).and(spec4b)) ;
		return allSpecs ;
	}
	
	//@Test
	public void checkSpec() throws Throwable {	
		boolean ok =  Common.checkSpecification("ADT_Examples\\.Tri.*",spec()); 
		assertTrue(ok) ;
	}
    
}