package logic;

import java.util.HashSet;
import java.util.Set;

import model.TransitionSystem;

/**
 * This class represents a CTL formula that is the exists eventually (diamond) of a formula.
 * 
 * @author Franck van Breugel
 */
public class ExistsEventually extends Formula {
    private Formula formula;

    /**
     * Initializes this CTL formula as the exists eventually of the given formula.
     * 
     * @param formula the subformula of this exists eventually formula
     */
    public ExistsEventually(Formula formula) {
	this.formula = formula;
    }

    @Override
    public int hashCode() {
	final int prime = 51;
	return prime * this.formula.hashCode();
    }

    @Override
    public boolean equals(Object object) {
	if (object != null && this.getClass() == object.getClass()) {
	    ExistsEventually other = (ExistsEventually) object;
	    return this.formula.equals(other.formula);
	} else {
	    return false;
	}
    }

    /**
     * Returns a string representation of this exists eventually formula.
     * The string consists of "EF " followed by the string representation
     * of the subformula.
     * 
     * @return a string representation of this exists eventually formula
     */
    @Override
    public String toString() {
	return "EF " + this.formula;
    }

    @Override
    public Set<Integer> sat(TransitionSystem system) {
	Set<Integer> sat = new HashSet<Integer>();
	Set<Integer> subsat = this.formula.sat(system); // sat of the subformula
	Set<Integer> prev;
	do {
	    prev = sat;
	    sat = new HashSet<Integer>();
	    sat.addAll(subsat);
	    for (int source = 0; source < system.getStates(); source++) {
		boolean intersects = false;
		for (int target : system.post(source)) {
		    if (prev.contains(target)) {
			intersects = true;
		    }
		}
		if (intersects) {
		    sat.add(source);
		}
	    }
	} while (!sat.equals(prev));
	return sat;
    }
}