package de.renew.lola2.analysis;

import java.io.File;
import java.io.FileInputStream;
import java.io.IOException;

import de.renew.lola2.parser.LolaParser;
import de.renew.lola2.parser.NetFileParseError;
import de.renew.lola2.parser.Place;
import de.renew.lola2.parser.Transition;

/**
 * This class provides methods to analyze properties of Petri nets using LoLA.
 * It extends the LolaAnalyzer class and provides specific methods for checking
 * properties such as liveness, boundedness, deadlock freedom, and reachability.
 *
 * @author hewelt
 */
public class PropertyAnalyzer extends LolaAnalyzer {
    private static org.apache.log4j.Logger _logger =
        org.apache.log4j.Logger.getLogger(PropertyAnalyzer.class);

    /**
     * Constructor that allows to specify a custom path for the LoLA binaries.
     * Uses the default path defined in the LolaPlugin if no path is provided.
     *
     * @param lolaPath The path to the directory containing the LoLA binaries.
     */
    public PropertyAnalyzer(String lolaPath) {
        super(lolaPath);
    }

    /**
     * Default constructor. Uses the lola path defined in the LolaPlugin.
     * This constructor is used when no specific path is provided.
     */
    public PropertyAnalyzer() {
        super();
    }

    /**
     * Check if a transition is quasi-live (not dead).
     * @param transitionName the name of the transition
     * @param netFile the net file
     * @return true if the transition is quasi-live
     */
    public DirectLolaResult checkTransitionQuasiLiveness(String transitionName, File netFile) {
        String formula = "EF FIREABLE(" + transitionName + ")";
        _logger
            .debug("[LolaAnalyzer] Checking quasi-liveness for transition named " + transitionName);
        DirectLolaResult lolaOutput = callLola(formula, netFile);
        return lolaOutput;
    }

    /**
     * Check if a transition is live (based on the transition name).
     * @param transitionName the name of the transition
     * @param netFile the net file
     * @return true if the transition is live
     */
    public DirectLolaResult checkTransitionLiveness(String transitionName, File netFile) {
        _logger.debug("[LolaAnalyzer] Checking liveness for transition named " + transitionName);
        String formula = "AG EF FIREABLE(" + transitionName + ")";
        DirectLolaResult lolaOutput = callLola(formula, netFile);
        return lolaOutput;
    }

    /**
     * Check if a place is bounded (based on the place name)
     * @param placeName the name of the place
     * @param netFile the net file
     * @return true if the place is bounded
     */
    public DirectLolaResult checkPlaceBoundedness(String placeName, File netFile) {
        String formula = "AG " + placeName + " < oo";
        _logger.debug("[LolaAnalyzer] Checking boundedness for place named " + placeName);
        DirectLolaResult lolaOutput =
            callLola(formula, netFile, new String[] { "--search=cover", "--encoder=full" });
        return lolaOutput;
    }

    /**
     * Check if a net is bounded (based on the net file)
     * @param netFile the net file
     * @return true if the net is bounded.
     */
    public IndirectLolaResult checkNetBoundedness(File netFile) {
        LolaParser lolaParser;
        try (FileInputStream stream = new FileInputStream(netFile)) {
            lolaParser = new LolaParser();
            lolaParser.parse(stream);
        } catch (NetFileParseError | IOException e) {
            _logger.error("[LolaAnalyzer] Could not parse netFile " + netFile.getAbsolutePath());
            return new IndirectLolaResult(LolaResultStatus.ERROR);
        }

        LolaResultStatus status = LolaResultStatus.YES;
        for (Place place : lolaParser.getPlaces()) {
            String placeName = place.getName();

            DirectLolaResult pResult = checkPlaceBoundedness(placeName, netFile);
            LolaResultStatus pStatus = pResult.getStatus();

            if (pStatus == LolaResultStatus.YES) {
                continue;
            } else if (pStatus == LolaResultStatus.NO) {
                status = pStatus;
                _logger.info(
                    "[Lola Checklist] Found unbounded place " + placeName
                        + ". Net is not bounded. ");
                break;
            } else {
                status = pStatus;
                _logger.info(
                    "[Lola Checklist] Could not check boundedness for " + placeName + ". Status: "
                        + pStatus);
                break;
            }
        }
        return new IndirectLolaResult(status);
    }

    /**
     * Check if a net is live (based on the net file)
     * May check for quasi-liveness first (being not dead is a necessary
     * precondition for liveness and checking quasi-liveness is cheaper than
     * checking liveness)
     * @param netFile the net file
     * @param checkQuasiLivenessFirst if true, quasi-liveness is checked first for each transitions
     * @return true if the net is bounded.
     */
    public IndirectLolaResult checkNetLiveness(File netFile, boolean checkQuasiLivenessFirst) {
        LolaParser lolaParser;
        try (FileInputStream stream = new FileInputStream(netFile)) {
            lolaParser = new LolaParser();
            lolaParser.parse(stream);
        } catch (NetFileParseError | IOException e) {
            _logger.error("[LolaAnalyzer] Could not parse netFile " + netFile.getAbsolutePath());
            return new IndirectLolaResult(LolaResultStatus.ERROR);
        }

        LolaResultStatus status = LolaResultStatus.YES;

        // check quasi-liveness
        if (checkQuasiLivenessFirst) {
            for (Transition transition : lolaParser.getTransitions()) {
                String transitionName = transition.getName();

                DirectLolaResult tResult = checkTransitionQuasiLiveness(transitionName, netFile);
                LolaResultStatus tStatus = tResult.getStatus();

                if (tStatus == LolaResultStatus.YES) {
                    continue;
                } else if (tStatus == LolaResultStatus.NO) {
                    status = tStatus;
                    _logger.info(
                        "[Lola Checklist] Found dead transition " + transitionName
                            + ". Net is not live. ");
                    break;
                } else {
                    status = tStatus;
                    _logger.info(
                        "[Lola Checklist] Could not check quasi-liveness for " + transitionName
                            + ". Status: " + tStatus);
                    break;
                }
            }
        }

        // check liveness
        if (status == LolaResultStatus.YES) {
            for (Transition transition : lolaParser.getTransitions()) {
                String transitionName = transition.getName();

                DirectLolaResult tResult = checkTransitionLiveness(transitionName, netFile);
                LolaResultStatus tStatus = tResult.getStatus();

                if (tStatus == LolaResultStatus.YES) {
                    continue;
                } else if (tStatus == LolaResultStatus.NO) {
                    status = tStatus;
                    _logger.info(
                        "[Lola Checklist] Found not-live transition " + transitionName
                            + ". Net is not live. ");
                    break;
                } else {
                    status = tStatus;
                    _logger.info(
                        "[Lola Checklist] Could not check liveness for " + transitionName
                            + ". Status: " + tStatus);
                    break;
                }
            }
        }

        return new IndirectLolaResult(status);
    }

    /**
     * Check quasi-liveness (based on the CPNDrawing).
     * A net is quasi-live if it is not dead.
     * @param netFile the net file
     * @return true if the net is quasi-live (contains not dead transitions).
     */
    public IndirectLolaResult checkNetQuasiLiveness(File netFile) {
        LolaParser lolaParser;
        try (FileInputStream stream = new FileInputStream(netFile)) {
            lolaParser = new LolaParser();
            lolaParser.parse(stream);
        } catch (NetFileParseError | IOException e) {
            _logger.error("[LolaAnalyzer] Could not parse netFile " + netFile.getAbsolutePath());
            return new IndirectLolaResult(LolaResultStatus.ERROR);
        }

        LolaResultStatus status = LolaResultStatus.YES;
        for (Transition transition : lolaParser.getTransitions()) {
            String transitionName = transition.getName();

            DirectLolaResult tResult = checkTransitionQuasiLiveness(transitionName, netFile);
            LolaResultStatus tStatus = tResult.getStatus();
            if (tStatus == LolaResultStatus.YES) {
                continue;
            } else if (tStatus == LolaResultStatus.NO) {
                status = tStatus;
                _logger.info(
                    "[Lola Checklist] Found dead transition " + transitionName
                        + ". Net is not quasi-live. ");
                break;
            } else {
                status = tStatus;
                _logger.info(
                    "[Lola Checklist] Could not check quasi-liveness for " + transitionName
                        + ". Status: " + tStatus);
                break;
            }
        }
        return new IndirectLolaResult(status);
    }

    /**
     * Check deadlock freedom.
     * @param netFile the net file
     * @return true if the net is deadlock free
     */
    public DirectLolaResult checkNetDeadlockFreedom(File netFile) {
        String formula = "NOT EF DEADLOCK";
        _logger.debug("[LolaAnalyzer] Checking deadlock freedom");
        DirectLolaResult lolaOutput = callLola(formula, netFile);
        return lolaOutput;
    }

    /**
     * Check if given marking is reachable from the initial marking.
     * @param marking the marking whose reachability shall be checked
     * @param netFile the net file
     * @return true if the given marking is reachable from the initial marking.
     */
    public DirectLolaResult checkMarkingReachability(String marking, File netFile) {
        String formula = "EF " + marking;
        _logger.debug("[LolaAnalyzer] Checking reachability of marking " + marking);
        DirectLolaResult lolaOutput = callLola(formula, netFile);
        return lolaOutput;
    }

    /**
     * Check if a given marking is a home state.
     * @param marking the marking that shall be checked for the home state property
     * @param netFile the net file
     * @return true if the given marking is a home state
     */
    public DirectLolaResult checkMarkingHomeState(String marking, File netFile) {
        String formula = "AG EF " + marking;
        _logger.debug("[LolaAnalyzer] Checking wether " + marking + " is a home state");
        DirectLolaResult lolaOutput = callLola(formula, netFile);
        return lolaOutput;
    }

    /**
     * Check reversibility of the net
     * @param netFile the net file
     * @return true if the net is reversible (the initial marking is a home state)
     */
    public DirectLolaResult checkNetReversibility(File netFile) {
        return checkMarkingHomeState("INITIAL", netFile);
    }
}