package test;

import java.lang.reflect.Constructor;
import java.lang.reflect.InvocationTargetException;
import java.util.BitSet;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Random;
import java.util.Set;

import org.junit.jupiter.api.Assertions;
import org.junit.jupiter.api.RepeatedTest;
import org.junit.jupiter.api.Test;

import logic.AtomicProposition;
import logic.ExistsNext;
import logic.Formula;
import model.TransitionSystem;

/**
 * Tests the ExistsNext class.
 * 
 * @author Franck van Breugel
 */
class ExistsNextTest {
    /**
     * Number of times that the test is repeated.
     */
    private static final int TIMES = 100;
    
    /**
     * Maximum number of states of a random transition system.
     */
    private static final int MAX_STATES = 100;
    
    /**
     * Randomness.
     */
    private static final Random random = new Random();
    
    /**
     * Tests equals method.
     */
    @RepeatedTest(TIMES)
    void testEquals() {
	Formula subformula = Formula.random();
	Formula formula = new ExistsNext(subformula);
	
	Assertions.assertNotEquals(formula, null, "Failed for " + formula);
	Assertions.assertNotEquals(formula, new Object(), "Failed for " + formula);
	
	Formula copy = new ExistsNext(subformula);
	Assertions.assertEquals(formula, copy, "Failed for " + formula);
	
	Formula otherSubformula = Formula.random();
	Formula otherFormula = new ExistsNext(otherSubformula);
	if (subformula.equals(otherSubformula)) {
	    Assertions.assertEquals(formula, otherFormula, "Failed for " + formula + " and " + otherFormula);
	} else {
	    Assertions.assertNotEquals(formula, otherFormula, "Failed for " + formula + " and " + otherFormula);
	}
    }
    
    /**
     * Tests the toString method.
     */
    @RepeatedTest(TIMES)
    void testToString() {
	Formula subformula = Formula.random();
	Formula formula = new ExistsNext(subformula);
	
	String expected = "EX " + subformula.toString();
	String actual = formula.toString();
	
	Assertions.assertEquals(expected, actual, "Failed for " + formula);
    }
    
    /**
     * Basic tests for sat method.
     */
    @Test
    void testSatBasic() {
	try {
	    Constructor<TransitionSystem> constructor = (Constructor<TransitionSystem>) TransitionSystem.class.getDeclaredConstructors()[0];
	    constructor.setAccessible(true);

	    Map<Integer, BitSet> transitions = new HashMap<Integer, BitSet>();
	    BitSet targets = new BitSet();
	    targets.set(1);
	    transitions.put(0, targets);
	    transitions.put(1, targets);

	    Map<String, BitSet> labelling = new HashMap<String, BitSet>();
	    targets = new BitSet();
	    targets.set(0);
	    labelling.put("a", targets);

	    TransitionSystem system = constructor.newInstance(2, transitions, labelling);
	    Formula formula = new ExistsNext(new AtomicProposition("a"));
	    BitSet sat = formula.sat(system);
	    Assertions.assertFalse(sat.get(0));
	    Assertions.assertFalse(sat.get(1));
	            
	    labelling = new HashMap<String, BitSet>();
	    targets = new BitSet();
	    targets.set(1);
	    labelling.put("a", targets);

	    system = constructor.newInstance(2, transitions, labelling);
	    sat = formula.sat(system);
	    Assertions.assertTrue(sat.get(0));
	    Assertions.assertTrue(sat.get(1));
	            
	} catch (SecurityException | InstantiationException | IllegalAccessException | IllegalArgumentException | InvocationTargetException e) {
	    System.out.println("WARNING: something went wrong with the creation of a transition system.");
	    e.printStackTrace();
	}      
    }
    
    /**
     * Intermediate tests for sat method.
     */
    @Test
    void testSatIntermediate() {
	try {
	    Constructor<TransitionSystem> constructor = (Constructor<TransitionSystem>) TransitionSystem.class.getDeclaredConstructors()[0];
	    constructor.setAccessible(true);
	    
	    Map<Integer, BitSet> transitions = new HashMap<Integer, BitSet>();
	    BitSet targets = new BitSet();
	    targets.set(1);
	    targets.set(2);
	    transitions.put(0, targets);
	    targets = new BitSet();
	    targets.set(1);
	    transitions.put(1, targets);
	    targets = new BitSet();
	    targets.set(2);
	    transitions.put(2, targets);

	    Map<String, BitSet> labelling = new HashMap<String, BitSet>();
	    targets = new BitSet();
	    targets.set(2);
	    labelling.put("a", targets);

	    TransitionSystem system = constructor.newInstance(3, transitions, labelling);
	    Formula formula = new ExistsNext(new AtomicProposition("a"));
	    BitSet sat = formula.sat(system);
	    Assertions.assertTrue(sat.get(0));
	    Assertions.assertFalse(sat.get(1));
	    Assertions.assertTrue(sat.get(2));
	            
	    transitions = new HashMap<Integer, BitSet>();
	    targets = new BitSet();
	    targets.set(0);
	    transitions.put(1, targets);
	    transitions.put(2, targets);
	    transitions.put(0, targets);
	    
	    labelling = new HashMap<String, BitSet>();
	    targets = new BitSet();
	    targets.set(0);
	    labelling.put("a", targets);

	    system = constructor.newInstance(3, transitions, labelling);
	    sat = formula.sat(system);
	    Assertions.assertTrue(sat.get(0));
	    Assertions.assertTrue(sat.get(1));
	    Assertions.assertTrue(sat.get(2));
	} catch (SecurityException | InstantiationException | IllegalAccessException | IllegalArgumentException | InvocationTargetException e) {
	    System.out.println("WARNING: something went wrong with the creation of a transition system.");
	    e.printStackTrace();
	}    
    }
    
    /**
     * Advanced tests for sat method.
     */
    @RepeatedTest(TIMES)
    void testSatAdvanced() {
	int states = 1 + random.nextInt(MAX_STATES);
	TransitionSystem system = TransitionSystem.random(states);
	
	Formula subformula = Formula.random();
	Formula formula = new ExistsNext(subformula);
	
	BitSet subsat = subformula.sat(system);
	BitSet sat = formula.sat(system);
	for (int state = 0; state < system.getStates(); state++) {
	    Assertions.assertEquals(sat.get(state), subsat.intersects(system.post(state)), "Failed for " + state + " and " + formula + " and\n" + system);
	}
    }
}