package de.renew.lola2.analysis;

/**
 * Enum representing the possible statuses of a LoLA analysis result.
 * This enum is used to indicate the outcome of an analysis, such as whether
 * a property holds (YES), does not hold (NO), or if there was an error during
 * the analysis (ERROR). It also includes states for unchecked results and
 * infeasible properties.
 */
public enum LolaResultStatus {
    /** Indicates that the property holds true. */
    YES,

    /** Indicates that the property does not hold true. */
    NO,

    /** Indicates that there was an error during the analysis. */
    ERROR,

    /** Indicates that the result has not been checked yet. */
    UNCHECKED,

    /** Indicates that the property is infeasible, meaning it cannot be satisfied. */
    INFEASIBLE;

    /**
     * Composes two LolaResultStatus values using a disjunctive composition.
     * This is used to combine results from different analyses.
     *
     * @param status1 The first status.
     * @param status2 The second status.
     * @return The composed status.
     */
    public static LolaResultStatus composeStatiConjunctive(
        LolaResultStatus status1, LolaResultStatus status2)
    {
        // conjunctive compositions (symmetric)
        //
        //            | YES        | NO         | ERROR      | UNCHECKED  | INFEASIBLE
        // ----------------------------------------------------------------------------
        // YES        | YES        | NO         | ERROR      | UNCHECKED  | INFEASIBLE
        // NO         |            | NO         | NO         | NO         | NO
        // ERROR      |            |            | ERROR      | ERROR      | INFEASIBLE
        // UNCHECKED  |            |            |            | UNCHECKED  | INFEASIBLE
        // INFEASIBLE |            |            |            |            | INFEASIBLE     
        LolaResultStatus result;

        if (status1 == YES) {
            result = status2;
        } else if (status2 == YES) {
            result = status1;
        } else if (status1 == NO || status2 == NO) {
            result = NO;
        } else if (status1 == ERROR || status2 == ERROR) {
            if (status1 == INFEASIBLE || status2 == INFEASIBLE) {
                result = INFEASIBLE;
            } else {
                result = ERROR;
            }
        } else if (status1 == UNCHECKED && status2 == UNCHECKED) {
            result = UNCHECKED;
        } else if (status1 == INFEASIBLE && status2 == INFEASIBLE) {
            result = INFEASIBLE;
        } else {
            // this should never happen
            result = ERROR;
        }

        return result;
    }

    /**
     * Inverts the given LolaResultStatus.
     * - YES becomes NO
     * - NO becomes YES
     * - ERROR, UNCHECKED, and INFEASIBLE remain unchanged.
     *
     * @param status The status to be inverted.
     * @return The inverted status.
     */
    public static LolaResultStatus inverse(LolaResultStatus status) {
        LolaResultStatus result;
        if (status == YES) {
            result = NO;
        } else if (status == NO) {
            result = YES;
        } else {
            result = status;
        }
        return result;
    }
}