package de.renew.lola2.gui;

import java.awt.BorderLayout;
import java.awt.GridLayout;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.io.File;
import java.util.HashMap;
import javax.swing.JButton;
import javax.swing.JCheckBox;
import javax.swing.JOptionPane;
import javax.swing.JPanel;
import javax.swing.JScrollPane;
import javax.swing.JTable;
import javax.swing.table.DefaultTableModel;

import CH.ifa.draw.DrawPlugin;
import CH.ifa.draw.application.DrawApplication;
import CH.ifa.draw.framework.FigureWithID;
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.VirtualPlaceFigure;
import de.renew.lola2.LolaFileCreator;
import de.renew.lola2.analysis.DirectLolaResult;
import de.renew.lola2.analysis.LolaResult;
import de.renew.lola2.analysis.LolaResultStatus;
import de.renew.lola2.analysis.PropertyAnalyzer;


/**
 * The MarkingEditorPanel is a JPanel that allows users to edit markings
 * in a Lola net. It provides functionality to update places, check reachability,
 * home state, and coverability of markings.
 */
public class MarkingEditorPanel extends JPanel {
    /**
     * The LolaGUI instance that this panel belongs to.
     * It is used to access the current drawing and Lola path.
     */
    private LolaGUI _lolaGUI;
    /**
     * The JTable that displays the markings for places.
     * It has three columns: Place, Initial, and Check.
     */
    private JTable _markingTable;
    /**
     * The action listener that updates the places in the marking table.
     * It is triggered when the "Update places!" button is clicked.
     */
    private UpdatePlacesAction _updatePlacesListener;

    /**
     * Marking editor components, which are needed globally.
     */
    private JCheckBox _updateInitialMarkingCheckbox = new JCheckBox("Update initial marking", true);
    private static org.apache.log4j.Logger _logger =
        org.apache.log4j.Logger.getLogger(MarkingEditorPanel.class);

    /**
     * Constructor for the MarkingEditorPanel.
     * @param lolaGUI the LolaGUI instance that this panel belongs to
     */
    public MarkingEditorPanel(LolaGUI lolaGUI) {
        super();
        this._lolaGUI = lolaGUI;
        setVisible(true);
        setup();
    }

    private void setup() {
        /*
         * Set up initial table (1 row, 3 columns) and set column names
         */
        int numColumns = 3;
        int numRows = 1;
        _markingTable = new JTable(numRows, numColumns);

        _markingTable.getColumnModel().getColumn(0).setHeaderValue("Place");
        _markingTable.getColumnModel().getColumn(1).setHeaderValue("Initial");
        _markingTable.getColumnModel().getColumn(2).setHeaderValue("Check");

        /*
         * Create buttons and panes and make them visible/layout them
         */
        JScrollPane scrollPane = new JScrollPane(_markingTable);
        _markingTable.setFillsViewportHeight(true);

        JButton updateButton = new JButton("Update places!");
        updateButton.setToolTipText("Update the places from the currently active net.");
        JButton reachButton = new JButton("Check reachability!");
        reachButton.setToolTipText(
            "Check if the marking entered into the table can be reached from the initial marking (from the table).");
        JButton homeButton = new JButton("Check home status!");
        homeButton.setToolTipText(
            "Check if the marking entered into the table is a home state w.r.t. the initial marking (from the table).");
        JButton coverButton = new JButton("Check coverability!");
        coverButton.setToolTipText(
            "Check if the marking entered into the table is coverable w.r.t. the initial marking (from the table).");

        setLayout(new BorderLayout());
        JPanel sidePanel = new JPanel();
        sidePanel.setLayout(new GridLayout(5, 1));

        add("Center", scrollPane);

        /*
         * Add action to the buttons and then add the buttons
         */
        _updatePlacesListener = new UpdatePlacesAction();
        updateButton.addActionListener(_updatePlacesListener);
        sidePanel.add(updateButton);

        ReachableMarkingAction reachableMarkingListener = new ReachableMarkingAction();
        reachButton.addActionListener(reachableMarkingListener);
        sidePanel.add(reachButton);

        HomeStateMarkingAction homeStateListener = new HomeStateMarkingAction();
        homeButton.addActionListener(homeStateListener);
        sidePanel.add(homeButton);

        CoverableMarkingAction coverabilityListener = new CoverableMarkingAction();
        coverButton.addActionListener(coverabilityListener);
        sidePanel.add(coverButton);


        /*
         * Also add a checkbox, so that the user can decide if he wants to update the initial marking
         * from the net or keep the manually input one.
         */


        // JCheckBox updateInitialMarkingCheckbox = new JCheckBox("Update IM",true);
        _updateInitialMarkingCheckbox.setToolTipText(
            "If this is checked the initial marking will be updated"
                + " from the net when the places are updated.");
        sidePanel.add(_updateInitialMarkingCheckbox);
        add("East", sidePanel);
    }

    private int findCorrectRow(String value, int column) {
        int result = -1;
        for (int i = 0; i < _markingTable.getRowCount(); i++) {
            if (value.equals(_markingTable.getValueAt(i, column))) {
                result = i;
            }
        }

        return result;
    }

    void updatePlaces() {
        _updatePlacesListener.actionPerformed(null);
    }


    /**
     * Get a String from the column column in the _markingTable of the marking editor
     * Depending on mode, the StringBuffer can have different forms:
     *
     * mode = 1 for reachability returns a StringBuffer of the form "MARKING p1:x,p2:y". This
     * is used if you want to get an initial or check marking from the table
     *
     * mode = 2 for coverability checks returns a StringBuffer of the form
     * "p1 bigger or equal than x AND p2 bigger or equal than y". This
     * is used if a task for coverability needs to be extracted from th table
     *
     * mode = 3 for home marking checks returns a StringBuffer of the form "p1=x AND p2=y". This
     * is used if a task for home status of a marking needs to be extracted from the table
     *
     * @param column the column in which the marking is input
     * @param mode to be used for the different kind of StringBuffer results
     * @return a StringBuffer with Lola understandable marking text
     */
    public String getTableMarking(int column, int mode) {
        String separator = "";
        String comparator = "";
        switch (mode) {
            // For reachability
            case 1: {
                separator = " , ";
                comparator = " : ";
                break;
            }

            // For coverability
            case 2: {
                separator = " AND ";
                comparator = " >= ";
                break;
            }

            // For Home marking
            case 3: {
                separator = " AND ";
                comparator = " = ";
                break;
            }
        }

        StringBuffer sb = new StringBuffer();
        if (mode == 1) {
            sb.append("MARKING ");
        } else {
            sb.append("(");
        }

        for (int i = 0; i < _markingTable.getRowCount(); i++) {
            if (i > 0) {
                sb.append(separator);
            }
            sb.append(_markingTable.getValueAt(i, 0) + comparator);
            if (!(_markingTable.getValueAt(i, column) == null
                || _markingTable.getValueAt(i, column).equals(""))) {
                sb.append(_markingTable.getValueAt(i, column));
            } else {
                sb.append("0");
            }
        }

        if (mode == 2 || mode == 3) {
            sb.append(")");
        }
        return sb.toString();
    }

    /**
     * When updateButton is clicked the places and initial marking
     * are read from the current net and displayed in the marking
     * table
     *
     * @author hewelt, wagner
     */
    class UpdatePlacesAction implements ActionListener {
        @Override
        public void actionPerformed(ActionEvent arg0) {
            LolaFileCreator fileCreator = new LolaFileCreator();

            /*
             * Get current drawing
             */
            DrawApplication app = DrawPlugin.getGui();
            if (app.drawing() instanceof CPNDrawing) {
                _lolaGUI._drawing = (CPNDrawing) app.drawing();
            }
            _logger.info(
                "[Lola] performing updatePlacesAction with drawing " + _lolaGUI._drawing.getName());

            FigureEnumeration figs = _lolaGUI._drawing.figures();

            DefaultTableModel tableModel = new DefaultTableModel();
            tableModel.addColumn("Place");
            tableModel.addColumn("Initial");
            tableModel.addColumn("Check");
            String[] currentRow = { "", "", "" };
            HashMap<String, String> markingMap;
            String figureName;
            int correctRow;

            /*
             * Check all figures if they are places. If they are find out their name,
             * their marking in the net and if a second marking for that place is already
             * in the table (this is the only thing stored, the rest is overwritten with
             * data from the net)
             * Collect these three things in an Array and then add a row to a new Tablemodel
             * That Tablemodel replaces the previous model. This means we dont have to check
             * for removed places.
             */
            while (figs.hasMoreElements()) {
                Figure fig = figs.nextElement();
                if (fig instanceof PlaceFigure && !(fig instanceof VirtualPlaceFigure)) {
                    figureName = fileCreator.name((FigureWithID) fig);

                    _logger.info("[Lola] found place named " + figureName);

                    currentRow[0] = figureName;

                    if (_markingTable.getRowCount() >= tableModel.getRowCount()) {
                        correctRow = findCorrectRow(currentRow[0], 0);
                        if (correctRow > -1) {
                            currentRow[2] = (String) _markingTable.getValueAt(correctRow, 2);
                            if (!_updateInitialMarkingCheckbox.isSelected()) {
                                currentRow[1] = (String) _markingTable.getValueAt(correctRow, 1);
                            }
                        }
                    }


                    if (_updateInitialMarkingCheckbox.isSelected()) {
                        markingMap = fileCreator.getInitialMarking(_lolaGUI._drawing);
                        currentRow[1] = markingMap.get(currentRow[0]);
                    }

                    tableModel.addRow(currentRow);
                    _logger.info("[Lola] adding marking table column " + currentRow.toString());


                }
            }

            _markingTable.setModel(tableModel);
        }
    }

    abstract class AbstractMarkingAction implements ActionListener {
        String _property;
        String _adjective;

        protected AbstractMarkingAction(String property, String adjective) {
            this._property = property;
            this._adjective = adjective;
        }

        protected abstract LolaResult checkProperty(File netFile);

        @Override
        public void actionPerformed(ActionEvent arg0) {
            /*
             * Get current drawing
             */
            DrawApplication app = DrawPlugin.getGui();
            if (app.drawing() instanceof CPNDrawing) {
                _lolaGUI._drawing = (CPNDrawing) app.drawing();
            }

            /*
             * Get the Marking StringBuffers from the table for both columns
             */
            String initialMarking = getTableMarking(1, 1);
            String checkMarking = getTableMarking(2, 1);;

            _logger.info("[Lola] Initial marking from table " + initialMarking.toString());
            _logger.info("[Lola] second marking from table " + checkMarking.toString());

            /*
             * Only check if there is anything in the third column
             */
            if (checkMarking.trim() != "MARKING") {
                File tmpLolaFile =
                    new LolaFileCreator().writeTemporaryLolaFile(_lolaGUI._drawing, initialMarking);
                LolaResult result = checkProperty(tmpLolaFile);
                LolaResultStatus status = result.getStatus();

                /*
                 * Depending on the result, show a positive or negative message
                 */
                if (status == LolaResultStatus.YES) {
                    JOptionPane.showMessageDialog(
                        MarkingEditorPanel.this,
                        "The marking \n" + "\n" + checkMarking.toString().substring(8) + "\n" + "\n"
                            + "is " + _adjective + "!",
                        "Lola " + _property, JOptionPane.INFORMATION_MESSAGE);
                } else if (status == LolaResultStatus.NO) {
                    JOptionPane.showMessageDialog(
                        MarkingEditorPanel.this,
                        "The marking \n" + "\n" + checkMarking.toString().substring(8) + "\n" + "\n"
                            + "<html>is <b>not</b> " + _adjective + "! </html>",
                        "Lola " + _property, JOptionPane.ERROR_MESSAGE);
                } else {
                    JOptionPane.showMessageDialog(
                        MarkingEditorPanel.this,
                        "The marking \n" + "\n" + checkMarking.toString().substring(8) + "\n" + "\n"
                            + "is not " + _adjective + " or cannot be computed!",
                        "Lola " + _property, JOptionPane.WARNING_MESSAGE);
                }
            } else {
                _logger
                    .info("[Lola] No secondary marking input. Cancelling " + _property + " check!");
            }
        }
    }

    class ReachableMarkingAction extends AbstractMarkingAction {
        public ReachableMarkingAction() {
            super("Reachability", "reachable");
        }

        @Override
        protected DirectLolaResult checkProperty(File netFile) {
            PropertyAnalyzer analyzer = new PropertyAnalyzer(_lolaGUI._lolaPath);
            String checkMarkingFormula = getTableMarking(2, 3);
            DirectLolaResult result =
                analyzer.checkMarkingReachability(checkMarkingFormula, netFile);
            return result;
        }
    }

    class HomeStateMarkingAction extends AbstractMarkingAction {
        public HomeStateMarkingAction() {
            super("Home State", "a home state");
        }

        @Override
        protected DirectLolaResult checkProperty(File netFile) {
            PropertyAnalyzer analyzer = new PropertyAnalyzer(_lolaGUI._lolaPath);
            String checkMarkingFormula = getTableMarking(2, 3);
            DirectLolaResult result = analyzer.checkMarkingHomeState(checkMarkingFormula, netFile);
            return result;
        }
    }

    class CoverableMarkingAction extends AbstractMarkingAction {
        public CoverableMarkingAction() {
            super("Coverability", "coverable");
        }

        @Override
        protected DirectLolaResult checkProperty(File netFile) {
            PropertyAnalyzer analyzer = new PropertyAnalyzer(_lolaGUI._lolaPath);
            String checkMarkingFormula = getTableMarking(2, 2);
            DirectLolaResult result =
                analyzer.checkMarkingReachability(checkMarkingFormula, netFile);
            return result;
        }
    }
}
