package de.renew.lola2.gui;

import java.awt.Color;
import java.awt.GridLayout;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.io.File;
import java.net.MalformedURLException;
import javax.swing.JButton;
import javax.swing.JLabel;
import javax.swing.JPanel;
import javax.swing.SwingConstants;

import CH.ifa.draw.DrawPlugin;
import CH.ifa.draw.application.DrawApplication;
import de.renew.draw.storables.ontology.Drawing;
import de.renew.gui.CPNDrawing;
import de.renew.lola2.LolaFileCreator;
import de.renew.lola2.analysis.LolaResult;
import de.renew.lola2.analysis.LolaResultStatus;
import de.renew.lola2.analysis.PropertyAnalyzer;
import de.renew.lola2.io.LolaImportFormat;

/**
 * ChecklistPanel is a JPanel that displays the results of various net properties
 * checks performed by the LolaAnalyzer. It provides a user interface to check
 * properties like liveness, deadlock freedom, reversibility, boundedness, and
 * quasi-liveness of a Petri net.
 */
public class ChecklistPanel extends JPanel {
    private static final org.apache.log4j.Logger LOGGER =
        org.apache.log4j.Logger.getLogger(ChecklistPanel.class);
    /** The LolaGUI instance associated with this panel. */
    private LolaGUI _lolaGUI;

    // Labels showing the results of the net analysis

    /** The label for the liveness result. */
    protected JLabel _livenessResultLabel = new JLabel();
    /** The label for the deadlock freedom result. */
    protected JLabel _deadlockFreedomResultLabel = new JLabel();
    /** The label for the reversibility result. */
    protected JLabel _reversibilityResultLabel = new JLabel();
    /** The label for the boundedness result. */
    protected JLabel _boundednessResultLabel = new JLabel();
    /** The label for the quasi-liveness result. */
    protected JLabel _quasiLivenessResultLabel = new JLabel();
    /** The label showing the name of the currently checked net. */
    protected JLabel _nameOfNetLabel = new JLabel();
    /** The LolaGUI instance associated with this panel. */
    private CheckListAction _checkListListener;

    /**
     * Constructor for ChecklistPanel.
     * Initializes the panel and sets up the layout and components.
     *
     * @param lolaGUI the LolaGUI instance to interact with
     */
    public ChecklistPanel(LolaGUI lolaGUI) {
        super();
        this._lolaGUI = lolaGUI;
        setVisible(true);
        setup();
    }

    private void setup() {
        GridLayout checkListLayout = new GridLayout(7, 2, 10, 5);
        setLayout(checkListLayout);

        JLabel netnameLabel = new JLabel("Currently checking: ");
        JLabel quasiLivenessLabel = new JLabel("Quasi-Liveness");
        JLabel livenessLabel = new JLabel("Liveness");
        JLabel deadlockFreedomLabel = new JLabel("Deadlock freedom");
        JLabel reversibilityLabel = new JLabel("Reversibility");
        //        JLabel homeMarkingLabel = new JLabel("Home Marking");
        JLabel boundednessLabel = new JLabel("Boundedness");

        JLabel[] labels = new JLabel[] {
            quasiLivenessLabel, livenessLabel, deadlockFreedomLabel, reversibilityLabel,
            boundednessLabel, netnameLabel };
        JLabel[] results = new JLabel[] {
            _quasiLivenessResultLabel, _livenessResultLabel, _deadlockFreedomResultLabel,
            _reversibilityResultLabel, _boundednessResultLabel, _nameOfNetLabel };

        // set tooltips
        quasiLivenessLabel.setToolTipText(
            "Is the net quasi-live (i.e. every transition non-dead in initial marking)?");
        livenessLabel.setToolTipText(
            "Is the net live (i.e. for all reachable markings there is a firing sequence, so that every transition can be enabled)?");
        deadlockFreedomLabel.setToolTipText("Is the net deadlock-free?");
        reversibilityLabel
            .setToolTipText("Is the net reversible (is the initial marking a home state)?");
        //        homeMarkingLabel.setToolTipText("Is there a home marking in the net?");
        boundednessLabel.setToolTipText("Is the net bounded?");

        for (int i = 0; i < labels.length; i++) {
            labels[i].setHorizontalAlignment(SwingConstants.RIGHT);
            add(labels[i]);
            results[i].setText("n.y.c");
            results[i].setForeground(Color.GRAY);
            add(results[i]);
        }

        JButton checkButton = new JButton("Check properties");
        _checkListListener = new CheckListAction();
        checkButton.addActionListener(_checkListListener);

        /**
         * Clicking the button triggers the creation of a temporary lola net file
         * followed by an import of this file with {@link LolaImportFormat}.
         * The resulting drawing is then displayed.
         */
        final JButton ptnButton = new JButton("Show PTN projection");
        ptnButton.addActionListener(new ActionListener() {
            @Override
            public void actionPerformed(ActionEvent e) {
                DrawApplication app = DrawPlugin.getGui();
                if (app.drawing() instanceof CPNDrawing) {
                    _lolaGUI._drawing = (CPNDrawing) app.drawing();
                    File netFile = new LolaFileCreator().writeTemporaryLolaFile(_lolaGUI._drawing);
                    LolaImportFormat lolaImporter = new LolaImportFormat();
                    try {
                        Drawing imported = lolaImporter.importFile(netFile.toURI().toURL());
                        app.showDrawingViewContainer(imported);
                    } catch (MalformedURLException e3) {
                        LOGGER.error(
                            "[Lola GUI - Show PTN projection] Converting the file to a URL failed");
                        e3.printStackTrace();
                    } catch (Exception e3) {
                        LOGGER.error(
                            "[Lola GUI - Show PTN projection] Something went wrong with the import");
                        e3.printStackTrace();
                    }
                } else {
                    LOGGER.error("[Lola GUI - Show PTN projection] Drawing must be CPNDrawing");
                }
            }
        });

        //        final JButton drawButton = new JButton("Draw Reach. Graph");
        //        drawButton.addActionListener(new ActionListener() {
        //            @Override
        //            public void actionPerformed(ActionEvent e) {
        //                DrawApplication app = DrawPlugin.getGui();
        //                if (app.drawing() instanceof CPNDrawing) {
        //                    lolaGUI.drawing = (CPNDrawing) app.drawing();
        //                    File imgFile = drawReachGraph();
        //                    if (imgFile != null) {
        //                        BufferedImage img;
        //                        try {
        //                            img = ImageIO.read(imgFile);
        //                            ImageIcon rgIcon = new ImageIcon(img);
        //                            JFrame rgWindow = new JFrame();
        //                            rgWindow.add(new JScrollPane(new JLabel(rgIcon)));
        //                            rgWindow.setSize(300, 600);
        //                            rgWindow.setTitle(imgFile.getName());
        //
        //                            JRootPane root = rgWindow.getRootPane();
        //                            root.putClientProperty("Window.documentFile",
        //                                            imgFile);
        //
        //                            Rectangle p = drawButton.getTopLevelAncestor()
        //                                            .getBounds();
        //                            rgWindow.setLocation(p.x + p.width, p.y);
        //                            rgWindow.setVisible(true);
        //                        } catch (IOException e1) {
        //                            e1.printStackTrace();
        //                        }
        //                    }
        //                }
        //            }
        //        });

        add(checkButton);
        //        add(drawButton);
        add(ptnButton);
    }


    /**
     * When checkButton is clicked the net properties are
     * checked by the LolaAnalyzer. The result of each property
     * is shown on the right and is either a green checkmark or
     * a red X. Initially the result is a gray n.y.c (not yet checked)
     *
     * @author hewelt, wagner
     */
    class CheckListAction implements ActionListener {
        @Override
        public void actionPerformed(ActionEvent arg0) {
            _nameOfNetLabel.setText("...");
            update(getGraphics());
            DrawApplication app = DrawPlugin.getGui();
            if (app.drawing() instanceof CPNDrawing) {
                _lolaGUI._drawing = (CPNDrawing) app.drawing();
            }
            LOGGER.info(
                "[Lola] performing checklist action with drawing " + _lolaGUI._drawing.getName());


            PropertyAnalyzer analyzer = new PropertyAnalyzer(_lolaGUI._lolaPath);
            File tmpLolaFile = new LolaFileCreator().writeTemporaryLolaFile(_lolaGUI._drawing);


            /*
             * Check whether net is quasi-live
             */
            LOGGER.debug("[Lola Checklist] Check whether net is quasi-live");
            LolaResult quasiLivenessResult = analyzer.checkNetQuasiLiveness(tmpLolaFile);
            colorResultLabel(_quasiLivenessResultLabel, quasiLivenessResult.getStatus());

            /*
             * Check whether net is live
             */
            if (quasiLivenessResult.getStatus() == LolaResultStatus.YES) {
                LOGGER.debug("[Lola Checklist] Check whether net is live");
                LolaResult livenessResult = analyzer.checkNetLiveness(tmpLolaFile, false);
                colorResultLabel(_livenessResultLabel, livenessResult.getStatus());
            } else {
                colorResultLabel(_livenessResultLabel, quasiLivenessResult.getStatus());
            }

            /*
             * Check whether net is bounded
             */
            LOGGER.debug("[Lola Checklist] Check whether net is bounded");
            LolaResult boundednessResult = analyzer.checkNetBoundedness(tmpLolaFile);
            colorResultLabel(_boundednessResultLabel, boundednessResult.getStatus());

            /*
             * Check whether net is reversible
             */
            if (LOGGER.isDebugEnabled()) {
                LOGGER.debug("[Lola Checklist] Check whether net is reversible");
            }
            LolaResult reversibilityResult = analyzer.checkNetReversibility(tmpLolaFile);
            colorResultLabel(_reversibilityResultLabel, reversibilityResult.getStatus());

            /*
             * Check whether net is deadlock free.
             */
            LOGGER.debug("[Lola Checklist] Check whether net is deadlock free");
            LolaResult deadlockFreedomResult = analyzer.checkNetDeadlockFreedom(tmpLolaFile);
            colorResultLabel(_deadlockFreedomResultLabel, deadlockFreedomResult.getStatus());

            //            // not supported by Lola 2.0 
            //            /*
            //             * Check whether net has home-state
            //             */
            //            if (logger.isDebugEnabled()) {
            //                logger.debug("[Lola Checklist] Check whether net has home-state");
            //            }
            //            LolaResult homeResult = analyzer.checkNetProperty(LolaHelper.nethomeStateCommand,
            //                                                      tmpLolaFile);
            //            colorResultLabel(homeMarkingResult, homeResult.getExitValue());
        }


        /**
         * Changes a given result label according to the result of the net property
         * this label represents. [yes] means, that the net has the property, [no]
         * the opposite and [n/a] that it couldn't be verified by lola (in most cases
         * because the state space is infinite).
         *
         * @param label  which label to color
         * @param status lola status
         */
        public void colorResultLabel(JLabel label, LolaResultStatus status) {
            Color color = LolaGUIHelper.getStatusColor(status);
            label.setForeground(color);
            switch (status) {
                case YES:
                    label.setText("[yes]");
                    break;
                case NO:
                    label.setText("[no]");
                    break;
                case ERROR:
                    label.setText("ERROR");
                    label.setToolTipText(
                        "An error occured, check the console output for more information.");
                    LOGGER
                        .error("[Lola CheckList] The lola call resulted in an unexpected result.");
                    break;
                case UNCHECKED:
                    label.setText("n.y.c");
                    break;
                case INFEASIBLE:
                    label.setText("[n/a]");
                    break;
            }
            _nameOfNetLabel.setText(_lolaGUI._drawing.getName());
        }
    }

    void updateChecklist() {
        _checkListListener.actionPerformed(null);
    }

    // not supported in Lola 2.0
    //    private File drawReachGraph() {
    //        LolaAnalyzer analyzer = new LolaAnalyzer();
    //        File tmpLolaFile = LolaFileCreator.writeTemporaryLolaFile(drawing);
    //        String baseName = tmpLolaFile.getAbsolutePath()
    //                                     .substring(0,
    //                                                tmpLolaFile.getAbsolutePath()
    //                                                           .lastIndexOf("."));
    //        String graphFileName = baseName + ".graph";
    //        String dotFileName = baseName + ".dot";
    //        String imgType = "png";
    //        String imgFileName = baseName + "." + imgType;
    //        File imageFile = null;
    //
    ////        LolaResult netBounded = analyzer.checkNetBoundedness(drawing);
    //        if (netBounded.propertySatisfied()) { // net is bounded
    //            Runtime myrun = Runtime.getRuntime();
    //
    //            // construct lola command
    //            String[] lolaCmd = { lolaPath + "lola", tmpLolaFile.toString(), "-m" };
    //            String line = "";
    //            Boolean wasError = false;
    //            ArrayList<String> result = new ArrayList<String>();
    //            try {
    //                // run the lola command and let it finish, writing graph to file
    //                logger.info("[Lola Graph] Calling " + lolaCmd[0] + " "
    //                            + lolaCmd[1] + " " + lolaCmd[2] + " ");
    //                Process lolproc = myrun.exec(lolaCmd);
    //                BufferedReader output = new BufferedReader(new InputStreamReader(lolproc
    //                                                                                 .getInputStream()));
    //                while ((line = output.readLine()) != null) {
    //                    System.out.println(line);
    //                }
    //                output.close();
    //                lolproc.waitFor();
    //
    //                // run graph2dot command, it reads the graph from file and produces a dot file
    //                String[] g2dCmd = { lolaPath + LolaHelper.dotCommand, "-g", graphFileName, "-d", dotFileName };
    //
    //                logger.info("[Lola Graph] Calling " + g2dCmd[0] + " "
    //                            + g2dCmd[1] + " " + g2dCmd[2] + " " + g2dCmd[3]
    //                            + " " + g2dCmd[4] + " ");
    //                Process g2dproc = myrun.exec(g2dCmd);
    //                BufferedReader graph = new BufferedReader(new InputStreamReader(g2dproc
    //                                                                                .getInputStream()));
    //                BufferedReader error = new BufferedReader(new InputStreamReader(g2dproc
    //                                                                                .getErrorStream()));
    //                while ((line = error.readLine()) != null) {
    //                    logger.error("[graph2dot ERROR]" + line);
    //                    wasError = true;
    //                }
    //                while ((line = graph.readLine()) != null) {
    //                    result.add(line);
    //                    logger.error("[graph2dot]" + line);
    //                }
    //                int g2dRetVal = g2dproc.waitFor();
    //                if (!(wasError) && g2dRetVal == 0) {
    //                    logger.info("[graph2dot] Call returned exit value "
    //                                + g2dRetVal);
    //                    logger.info("[Lola Graph] Successfully created dot file in "
    //                                + dotFileName);
    //                }
    //                graph.close();
    //
    //                // run dot on the dot File and create image
    //                if (!wasError) { // if no error occurred
    //                    String[] args = { "dot", "-T" + imgType, dotFileName, "-o", imgFileName };
    //                    Process dotproc = myrun.exec(args);
    //                    BufferedReader dotIn = new BufferedReader(new InputStreamReader(dotproc
    //                                                                                    .getInputStream()));
    //                    BufferedReader dotEr = new BufferedReader(new InputStreamReader(dotproc
    //                                                                                    .getErrorStream()));
    //                    while ((line = dotEr.readLine()) != null) {
    //                        if (logger.isDebugEnabled()) {
    //                            logger.debug("[dot ERROR]" + line);
    //                        }
    //                        wasError = true;
    //                    }
    //                    while ((line = dotIn.readLine()) != null) {
    //                        result.add(line);
    //                        if (logger.isDebugEnabled()) {
    //                            logger.debug("[dot]" + line);
    //                        }
    //                    }
    //                    int dotExitVal = dotproc.waitFor();
    //
    //                    // create file, which is returned
    //                    imageFile = new File(imgFileName);
    //                    logger.info("[Lola Graph] dot returned " + dotExitVal
    //                                + " and imgFile in " + imgFileName
    //                                + (imageFile.exists() ? " exists." : "don't exist"));
    //                }
    //            } catch (IOException e) {
    //                logger.error(e.getMessage());
    //                if (logger.isDebugEnabled()) {
    //                    logger.debug(LolaGUI.class.getSimpleName() + ": ", e);
    //                }
    //                JOptionPane.showMessageDialog(null,
    //                                              "Cannot find dot.\n"
    //                                              + "Make shure graphviz is installed and dot is available in your path.\n"
    //                                              + "Current PATH is set to : \n"
    //                                              + System.getenv("PATH"),
    //                                              "Cannot find dot.",
    //                                              JOptionPane.ERROR_MESSAGE,
    //                                              GuiPlugin.getRenewIcon());
    //            } catch (InterruptedException e) {
    //                e.printStackTrace();
    //            }
    //        } else { // net is unbounded
    //            logger.error("[Lola GUI] Reachability graph not supported for unbounded nets.");
    //        }
    //        return imageFile;
    //        return null;
    //    }
}
