package de.renew.lola2.commands;

import java.awt.Color;
import java.io.File;
import java.io.PrintStream;

import CH.ifa.draw.DrawPlugin;
import CH.ifa.draw.application.DrawApplication;
import CH.ifa.draw.util.Command;
import de.renew.draw.storables.ontology.Figure;
import de.renew.draw.storables.ontology.FigureEnumeration;
import de.renew.gui.CPNDrawing;
import de.renew.gui.PlaceFigure;
import de.renew.gui.TransitionFigure;
import de.renew.gui.VirtualPlaceFigure;
import de.renew.lola2.LolaFileCreator;
import de.renew.lola2.analysis.LolaResult;
import de.renew.lola2.analysis.PropertyAnalyzer;
import de.renew.lola2.gui.LolaGUIHelper;
import de.renew.plugin.command.CLCommand;

/**
 * This command checks all places and transitions in the current drawing
 * for boundedness and liveness, respectively.
 */
public class CheckAllCommand extends Command implements CLCommand {
    private String _lolaPath;
    private static org.apache.log4j.Logger _logger =
        org.apache.log4j.Logger.getLogger(CheckAllCommand.class);

    /**
     * Constructs a command with the given name and path.
     * @param name the name of the command
     * @param path the path to the Lola executable
     */
    public CheckAllCommand(String name, String path) {
        super(name);
        _lolaPath = path;
    }

    @Override
    public void execute() {
        DrawApplication app = DrawPlugin.getGui();
        CPNDrawing drawing = (CPNDrawing) app.drawing();
        // enable undo
        app.getUndoRedoManager().prepareUndoSnapshot(app.drawing());


        PropertyAnalyzer analyzer = new PropertyAnalyzer(_lolaPath);

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

        FigureEnumeration figures = drawing.figures();


        boolean changed = false;
        while (figures.hasMoreElements()) {
            Figure fig = figures.nextElement();
            LolaResult result = null;
            if (fig instanceof PlaceFigure) {
                if (fig instanceof VirtualPlaceFigure) {
                    continue;
                }
                String placeName = creator.getNameForFigure(fig);
                result = analyzer.checkPlaceBoundedness(placeName, netFile);
            } else if (fig instanceof TransitionFigure) {
                String transitionName = creator.getNameForFigure(fig);
                result = analyzer.checkTransitionLiveness(transitionName, netFile);
            }
            if (result != null) {
                switch (result.getStatus()) {
                    case YES:
                        LolaGUIHelper.colorFigure(fig, Color.GREEN);
                        break;
                    case NO:
                        LolaGUIHelper.colorFigure(fig, Color.RED);
                        break;
                    default:
                        break;
                }
                changed = true;
            }
        }
        if (changed) {
            DrawPlugin.getGui().view().checkDamage();
            app.getUndoRedoManager().commitUndoSnapshot(drawing);
        }
    }

    @Override
    public void execute(String[] args, PrintStream response) {
        //TODO: implement the check from console
    }

    @Override
    public String getDescription() {
        return "Check all places and transitions.";
    }
}
