package rwth.i2.ltlrv.afastate.interfaze;

import java.util.Set;

import rwth.i2.ltlrv.data.PropositionSet;
import rwth.i2.ltlrv.data.WeakValuesMap;
import rwth.i2.ltlrv.formula.interfaze.IFormula;

/**
 * This interface reflects any subformula which is valid as input
 * for AFA generation.
 * Those are IUntil, IRelease, IAnd, IOr, INot, INext, ITT, IFF and IProposition subformulae.
 * Such formulae can be obtained by invoking {@link rwth.i2.ltlrv.formula.interfaze.IFormula#negationNormalForm()}.<br>
 * <b>Attention:</b> A lot of algorithms here assume that the whole term structure <i>remains</i> in negation normal form.
 * So be careful when generating {@link rwth.i2.ltlrv.afastate.interfaze.INot} terms somewhere: Always invoke
 * {@link rwth.i2.ltlrv.formula.interfaze.IFormula#negationNormalForm()} on the newly created term!
 * (@see rwth.i2.ltlrv.formula.impl.Implies#negationNormalForm())
 *
 * @author Eric Bodden
 * @see IUntil
 * @see IRelease
 * @see IAnd
 * @see IOr
 * @see INext
 * @see ITT
 * @see IFF
 * @see IProposition
 */
public interface IAFAState extends IFormula {

    /**
     * ValidationException - Exception that is thrown on validation of a formula.
     * 
     * @author Eric Bodden
     */
    @SuppressWarnings("serial")
    public class ValidationException extends Exception {

  
        /**
         * @param variableName name of potentially unbound variable
         * @param subformula subformulae in where <code>variableName</code>
         * is potentially unbound
         */
        public ValidationException(String variableName, IAFAState subformula) {
            super("Variable '"+variableName+"' may be unbound in '"+subformula+"'");
        }
        
    }

	/**
     * Returns <code>true</code> if this formula represents a final
     * state in the AFA. This is the case if the formula is either
     * a <i>Release</i> subformula, <i>TT</i>, or a boolean combination of
     * subformulae evaluating to <code>true</code>.
     * @return <code>true</code> if this formula represents a final
     * state in the AFA
     * @see IRelease
     * @see ITT
     */
    public boolean isFinalStateInAFA();

    /**
     * Returns a fresh copy of this subformula with bindings in propositions specialized
     * by the bindings of propositions, which are passed in as argument. 
     * @param bindings Set of propositions holding actual bindings.
     * @return subformula with free bindings replaced by the bindings passed in
     */
    public IAFAState specializeBindings(WeakValuesMap<String, Object> bindings);
    
    /**
     * Specializes the bindings of all items in <code>clauseSet</code> except the ones that are
     * equal to <code>this</code> term. 
     * @param bindings set of propositions holding actual bindings
     * @param clauseSet the set of clauses containing terms whose bindings shall be specialized;
     * the operation performs a destructive update, so the result will be passed here as well
     *  @see #specializeBindings(WeakValuesMap)
     */
    public void specializeBindings(WeakValuesMap<String, Object> bindings, Set<Set<IAFAState>> clauseSet);
    
	/**
     * Performs a transition on this term under the given propositions and bindings.
     * The result is returned in the <code>result</code> variable and is actually a set of clauses
     * representing a disjunct of a conjunct of states. This may not yet be the minimal model. It can be
     * reduced by applying subset reduction (@see rwth.i2.ltlrv.management.Configuration#subSetReduction(Set)).
     * A typicall initial call would be:<br>
     * <code><pre>
       Set<Set<IAFAState>> result = new HashSet<Set<IAFAState>>();
       transition(new HastSet<String>(), props, binding, result);
       </pre></code>
	 * @param context The context holds the set of variables that are provided by the outer (previous) temporal layers.
     * Initially this is empty. Then it has to be updated on each layer by adding the variables which
     * {@link #provides(Set)} returns. It is only used by the {@link INext} operator
     * (@see Next#doTransition(Set, PropositionSet, WeakValuesMap, Set)). 
	 * @param currentProps The set of propositions that are currently active.
     * Those must hold all bindings they provide.
	 * @param currentBinding The current binding to evaluate under. (@see PropositionSet#validCombinationsOfBindings())
	 * @param result The result will be placed here.
	 */
	public void transition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String, Object> currentBinding, Set<Set<IAFAState>> result);
    
    //TODO STILL USED?
    public enum VariableKind { ALL, IF_CLOSURES_ONLY };
    //TODO STILL USED?
    public void unboundVariablesAtCurrentJoinpoint(VariableKind variableKind, Set<String> result);
    
    /**
     * This returns the set of provided variables at the current temporal levels.
     * At each state <i>s</i> it holds, that <i>provides(s) = providesPos(s) join providesNeg(s)</i>.
     * @param result The result will be placed here.
     * @see #providesPos(Set)
     * @see #providesNeg(Set)
     */
    public void provides(Set<String> result);

    /**
     * This returns the set of positively provided variables at the current temporal levels.
     * This function is defined as:
       <pre>
        providesPos( phi /\ psi ) = providesPos( phi ) join providesPos( psi )
            
        providesPos( phi \/ psi ) = providesPos( phi ) intersect providesPos( psi )
                        
        providesPos( phi R psi ) =  providesPos( (psi /\ phi) \/ (psi /\ X(phi R psi)) )
                                 =  providesPos( psi )
                        
        providesPos( phi U psi ) = providesPos( psi \/ (phi /\ X(phi U psi) )
                                 = providesPos( psi ) intersect providesPos( phi ) 
            
        providesPos( X phi )     = emptyset
                        
        providesPos( !prop )     = emptyset
            
        providesPos( prop )      = provided variables of prop
     </pre>
     * @param result The result will be placed here.
     */
    public void providesPos(Set<String> result);
    
    /**
     * This returns the set of negatively provided variables at the current temporal levels.
     * This function is defined as:
       <pre>
        providesNeg( phi /\ psi ) = providesNeg( phi ) intersect providesNeg( psi )
            
        providesNeg( phi \/ psi ) = providesNeg( phi ) join providesNeg( psi )
                        
        providesNeg( phi R psi ) =  providesNeg( psi ) intersect providesNeg( phi )
                        
        providesNeg( phi U psi ) =  providesNeg( psi )
            
        providesNeg( X phi )     = emptyset
                        
        providesNeg( !prop )     = provided variables of prop
            
        providesNeg( prop )      = emptyset
     </pre>
     * @param result The result will be placed here.
     */
    public void providesNeg(Set<String> result);

    /**
     * This returns the set of required variables. This is the set of all variables which are free
     * in propositions, meaning they occur in an if-pointcut but are not provided by the same
     * pointcut at the same time.
     * @param result The result will be placed here.
     */
    public void requires(Set<String> result);    
    //TODO refactor: visitors

    /**
     * Validates a formula for consistent bindings. Bindings are consistent, when at each point in time,
     * the set of povided variables can be guaranteed to be a superset of the set of required variables.
     * @throws ValidationException Thrown if a variable is unbound. 
     * @see #provides(Set)
     * @see #requires(Set)
     * @see ValidationException#IAFAState.ValidationException(String, IAFAState)
     */
    public void validate() throws ValidationException;
    
}