package de.renew.net.inscription.transition;

import java.util.Collection;
import java.util.Collections;

import de.renew.engine.searcher.Occurrence;
import de.renew.engine.searcher.Searcher;
import de.renew.expression.Expression;
import de.renew.expression.VariableMapper;
import de.renew.net.NetInstance;
import de.renew.net.inscription.TransitionInscription;
import de.renew.unify.CalculationChecker;
import de.renew.unify.ICalculationChecker;
import de.renew.unify.IStateRecorder;
import de.renew.unify.Impossible;
import de.renew.unify.StateRecorder;
import de.renew.unify.Unify;
import de.renew.util.Value;

/**
 * A GuardInscription behaves like an {@link ExpressionInscription} but requires the result of the evaluation to be
 * {@code true}. Otherwise, an {@link Impossible} is thrown to force backtracking.
 * For example, a {@code CreationInscription} is created for a transition that is inscribed with "guard x != y;".
 * In this case, for the transition to fire, it is required for the values bound to x and y to be unequal, so that the
 * expression "x != y" evaluates to {@code true}.
 */
public class GuardInscription implements TransitionInscription {
    /**
     * The {@code Expression} that is required to evaluate to {@code true}.
     */
    private final Expression _expression;

    /**
     * Constructs a new {@code GuardInscription} based on the given {@code Expression}.
     *
     * @param expression the {@code Expression} that will be required to evaluate to {@code true}
     */
    public GuardInscription(Expression expression) {
        _expression = expression;
    }

    /**
     * Returns the expression that is required to evaluate to {@code true} by this {@code GuardInscription}.
     *
     * @return the {@code Expression} that is required to evaluate to {@code true} by this {@code GuardInscription}.
     */
    public Expression getExpression() {
        return _expression;
    }

    @Override
    public Collection<Occurrence> makeOccurrences(
        VariableMapper mapper, NetInstance netInstance, Searcher searcher) throws Impossible
    {
        IStateRecorder stateRecorder = new StateRecorder();
        ICalculationChecker calculationChecker = new CalculationChecker();

        Unify.unify(
            _expression.startEvaluation(mapper, stateRecorder, calculationChecker),
            new Value(Boolean.TRUE), stateRecorder);
        return Collections.emptySet();
    }
}