package de.renew.lola2.commands;

import java.io.File;

import CH.ifa.draw.DrawPlugin;
import CH.ifa.draw.application.DrawApplication;
import CH.ifa.draw.util.Command;
import de.renew.gui.CPNDrawing;
import de.renew.lola2.LolaFileCreator;
import de.renew.lola2.analysis.LolaResult;
import de.renew.lola2.analysis.PropertyAnalyzer;


/**
 * Command to check the liveness of a Petri net.
 * This command uses the LolaFileCreator to create a temporary Lola file
 * from the current drawing and then analyzes it for liveness.
 */
public class CheckLivenessCommand extends Command {
    private String _lolaPath;
    private static org.apache.log4j.Logger _logger =
        org.apache.log4j.Logger.getLogger(CheckLivenessCommand.class);

    /**
     * Constructor for CheckLivenessCommand.
     * @param name the name of the command
     * @param path the path to the Lola executable
     */
    public CheckLivenessCommand(String name, String path) {
        super(name);
        _lolaPath = path;
    }

    @Override
    public void execute() {
        DrawApplication app = DrawPlugin.getGui();
        CPNDrawing drawing = (CPNDrawing) app.drawing();
        PropertyAnalyzer analyzer = new PropertyAnalyzer(_lolaPath);

        // Write lola File
        File netFile = new LolaFileCreator().writeTemporaryLolaFile(drawing);
        if (_logger.isDebugEnabled()) {
            _logger.debug(
                CheckAllCommand.class.getSimpleName() + ": temp file name: " + netFile.getPath());
        }

        LolaResult result = analyzer.checkNetLiveness(netFile, true);
        switch (result.getStatus()) {
            case YES:
                _logger.info("YES, net is live.");
                break;
            case NO:
                _logger.info("NO, net is not live.");
                break;
            default:
                _logger.info("Unspecified result for liveness: " + result.getStatus());
        }
    }
}
