From 04ba71ec2b883ee8cbf754da45c18bf3bb65677b Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Thu, 23 Nov 2006 13:33:34 +0000 Subject: [PATCH] Added a multi-headered table in the simulator. Added this in a general way in userinterface.util.GUIGroupedTable git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@164 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../userinterface/simulator/GUISimulator.java | 122 +++++++++++- .../simulator/GUISimulatorPathTable.java | 15 +- .../userinterface/util/GUIGroupedTable.java | 118 +++++++++++ .../util/GUIGroupedTableColumnModel.java | 145 ++++++++++++++ .../util/GUIGroupedTableHeader.java | 188 ++++++++++++++++++ .../util/GUIGroupedTableModel.java | 53 +++++ 6 files changed, 631 insertions(+), 10 deletions(-) create mode 100644 prism/src/userinterface/util/GUIGroupedTable.java create mode 100644 prism/src/userinterface/util/GUIGroupedTableColumnModel.java create mode 100644 prism/src/userinterface/util/GUIGroupedTableHeader.java create mode 100644 prism/src/userinterface/util/GUIGroupedTableModel.java diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 3284206e..230cf9e4 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -2179,7 +2179,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } } - class PathTableModel extends AbstractTableModel + class PathTableModel extends AbstractTableModel implements GUIGroupedTableModel { private boolean SHOW_STEP = true; @@ -2217,6 +2217,118 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect { fireTableStructureChanged(); } } + public int getGroupCount() + { + if(!pathActive) + { + return 0; + } + else + { + int groupCount = 0; + + if (SHOW_STEP) + { groupCount++; } + + if (this.visibleVariables.size() > 0) + { groupCount++; } + + if (mf.getType() == ModulesFile.STOCHASTIC) + { groupCount++; } + + // Add state and transitions rewards for each reward structure. + if ((2*mf.getNumRewardStructs()) > 0) + { groupCount++; } + + return groupCount; + } + } + + public String getGroupName(int groupIndex) + { + int groupCount = 0; + + if (SHOW_STEP) + { + if (groupCount == groupIndex) + { return "Step"; } + + groupCount++; + } + + if (this.visibleVariables.size() > 0) + { + if (groupCount == groupIndex) + { return "Variables"; } + + groupCount++; + } + + if (mf.getType() == ModulesFile.STOCHASTIC) + { + if (groupCount == groupIndex) + { return "Time"; } + + groupCount++; + } + + // Add state and transitions rewards for each reward structure. + if ((2*mf.getNumRewardStructs()) > 0) + { + if (groupCount == groupIndex) + { return "Rewards"; } + + groupCount++; + } + + return ""; + } + + public int getLastColumnOfGroup(int groupIndex) + { + int stepStart = 0; + int varStart = (SHOW_STEP) ? stepStart + 1 : stepStart; + int timeStart = varStart + visibleVariables.size(); + int rewardStart = timeStart + 1; + + int groupCount = 0; + + if (SHOW_STEP) + { + if (groupCount == groupIndex) + { return stepStart; } + + groupCount++; + } + + if (this.visibleVariables.size() > 0) + { + if (groupCount == groupIndex) + { return varStart + visibleVariables.size() -1; } + + groupCount++; + } + + if (mf.getType() == ModulesFile.STOCHASTIC) + { + if (groupCount == groupIndex) + { return timeStart; } + + groupCount++; + } + + // Add state and transitions rewards for each reward structure. + if ((2*mf.getNumRewardStructs()) > 0) + { + if (groupCount == groupIndex) + { return rewardStart + 2*mf.getNumRewardStructs() - 1; } + + groupCount++; + } + + return 0; + } + /** * Returns the number of columns. * @see javax.swing.table.TableModel#getColumnCount() @@ -2228,7 +2340,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect else { // At least we have the step count and s. - int colCount = 1 + visibleVariables.size(); + int colCount = (SHOW_STEP) ? 1 : 0; + + colCount += this.visibleVariables.size(); // Add state and transitions rewards for each reward structure. colCount += (2*mf.getNumRewardStructs()); @@ -2307,11 +2421,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect if(mf.getType() == ModulesFile.STOCHASTIC) { int n = visibleVariables.size(); - if(columnIndex == n+1) //where time should be + if(columnIndex == timeStart) //where time should be { return new Double(SimulatorEngine.getTimeSpentInPathState(rowIndex)); } - else if(columnIndex > n+1) //rewards + else if(columnIndex > timeStart) //rewards { int i = columnIndex-(n+2); if (i%2 == 0) return new Double(SimulatorEngine.getStateRewardOfPathState(rowIndex,i/2)); diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java index a61dd468..6f534374 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java @@ -24,19 +24,23 @@ package userinterface.simulator; import javax.swing.*; import javax.swing.table.*; +import userinterface.util.*; import java.awt.*; import java.awt.geom.*; import javax.swing.border.*; import java.text.*; import java.awt.font.*; import simulator.*; +import javax.swing.plaf.basic.*; +import javax.swing.plaf.*; +import javax.swing.event.*; /** * * @author ug60axh */ -public class GUISimulatorPathTable extends JTable +public class GUISimulatorPathTable extends GUIGroupedTable { private GUISimulator.PathTableModel ptm; private PathRowHeader pathRowHeader; @@ -71,12 +75,12 @@ public class GUISimulatorPathTable extends JTable rowHeader.setCellRenderer(new RowHeaderRenderer(this)); this.header = rowHeader; - + setDefaultRenderer(Object.class, new PathChangeTableRenderer()); - //setAutoResizeMode(JTable.AUTO_RESIZE_SUBSEQUENT_COLUMNS); + //setAutoResizeMode(JTable.AUTO_RESIZE_SUBSEQUENT_COLUMNS); } - + public void switchToChangeRenderer() { setDefaultRenderer(Object.class, new PathChangeTableRenderer()); @@ -94,8 +98,7 @@ public class GUISimulatorPathTable extends JTable super.paintComponent(g); //pathRowHeader.paintComponent(g); - headerModel.updateHeader(); - + headerModel.updateHeader(); } /** diff --git a/prism/src/userinterface/util/GUIGroupedTable.java b/prism/src/userinterface/util/GUIGroupedTable.java new file mode 100644 index 00000000..ae0d218d --- /dev/null +++ b/prism/src/userinterface/util/GUIGroupedTable.java @@ -0,0 +1,118 @@ +//============================================================================== +// +// Copyright (c) 2002-2006, Mark Kattenbelt +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package userinterface.util; + +import javax.swing.*; +import javax.swing.table.*; + +import java.util.*; + + +/** + * @author mxk + * A table object that is capable of grouping headers, effectively by means of two JTableHeader + * Objects on top of each other. + */ +public class GUIGroupedTable extends JTable +{ + + /** + * Creates a new GUIGroupedTable. + * @param tableModel The (grouped) table data model on which to base this table. + */ + public GUIGroupedTable(GUIGroupedTableModel tableModel) + { + super(tableModel); + } + + /** + * The default TableColumnModel Object (and the only valid one) is a GUIGroupedColumnModel Object. + * @see javax.swing.JTable#createDefaultColumnModel() + */ + @Override + protected TableColumnModel createDefaultColumnModel() + { + return new GUIGroupedTableColumnModel(); + } + + + /** + * Given a GUIGroupedTableModel, this function creates a GUIGroupedColumnModel. + * This function is called by JTable when the structure of the table changes, such that + * it is not necessary to worry about the header. + * @see javax.swing.JTable#createDefaultColumnsFromModel() + */ + @Override + public void createDefaultColumnsFromModel() + { + GUIGroupedTableColumnModel groupedColumnModel = (GUIGroupedTableColumnModel)columnModel; + + groupedColumnModel.clear(); + + if (dataModel != null && dataModel instanceof GUIGroupedTableModel && columnModel instanceof GUIGroupedTableColumnModel) + { + GUIGroupedTableModel groupedDataModel = (GUIGroupedTableModel)dataModel; + + int group = 0; + int element = 0; + + // Add a group every iteration + while (group < groupedDataModel.getGroupCount() && element < groupedDataModel.getColumnCount()) + { + ArrayList groupElements = new ArrayList(); + + // Add an element every iteration + while (groupedDataModel.getLastColumnOfGroup(group) >= element) + { + TableColumn elementColumn = new TableColumn(element); + elementColumn.setHeaderValue(groupedDataModel.getColumnName(element)); + groupElements.add(elementColumn); + element++; + } + + TableColumn groupColumn = new TableColumn(group); + groupColumn.setHeaderValue(groupedDataModel.getGroupName(group)); + group++; + + groupedColumnModel.addColumnGroup(groupColumn, groupElements); + } + } + } + + /** + * Creates a default table header from the current column model. + * Also called by JTable such that there is no need to worry about headers once you implemented + * GUIGroupedTableModel. + * @see javax.swing.JTable#createDefaultTableHeader() + */ + @Override + protected JTableHeader createDefaultTableHeader() { + + if (columnModel != null && columnModel instanceof GUIGroupedTableColumnModel) + { + return new GUIGroupedTableHeader((GUIGroupedTableColumnModel)columnModel); + } + return new GUIGroupedTableHeader(new GUIGroupedTableColumnModel()); + } +} + diff --git a/prism/src/userinterface/util/GUIGroupedTableColumnModel.java b/prism/src/userinterface/util/GUIGroupedTableColumnModel.java new file mode 100644 index 00000000..f04b0542 --- /dev/null +++ b/prism/src/userinterface/util/GUIGroupedTableColumnModel.java @@ -0,0 +1,145 @@ +//============================================================================== +// +// Copyright (c) 2002-2006, Mark Kattenbelt +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package userinterface.util; + +import java.util.*; +import javax.swing.event.*; +import javax.swing.table.*; + +/** + * @author mxk + * The TableColumnModel with the addition of Groups. A group is a set of columns. The set of columns + * belonging to each group are disjoint and non-empty (!). + */ +/** + * @author mxk + * + */ +public class GUIGroupedTableColumnModel extends DefaultTableColumnModel implements TableColumnModelListener +{ + //private DefaultTableColumnModel elementTableColumnModel; + private DefaultTableColumnModel groupTableColumnModel; + + // The nth element is the index of the last element in the nth group. + private ArrayList lastColumn; + + /** + * Creates a new GUIGroupedTableModel with no groups. + */ + public GUIGroupedTableColumnModel() + { + lastColumn = new ArrayList(); + + //this.elementTableColumnModel = new DefaultTableColumnModel(); + this.groupTableColumnModel = new DefaultTableColumnModel(); + } + + + /** + * Returns The columns of all groups in terms of a DefaultTableColumnModel. + * @return The columns of all groups in terms of a DefaultTableColumnModel. + */ + public DefaultTableColumnModel getGroupTableColumnModel() + { + return groupTableColumnModel; + } + + + /** + * Adds a group to this grouped column model. + * @param groupColumn A TableColumn representing all of the group. + * @param elementColumns An ArrayList of TableColumns representing the columns of this group in the model. + */ + public void addColumnGroup(TableColumn groupColumn, ArrayList elementColumns) + { + groupTableColumnModel.addColumn(groupColumn); + + for (int i = 0; i < elementColumns.size(); i++) + { + this.addColumn(((TableColumn)elementColumns.get(i))); + } + + lastColumn.add(new Integer(this.getColumnCount()-1)); + } + + /** + * A function that updates the widths of the group columns. + */ + public void updateGroups() + { + int group = 0; + int groupWidth = 0; + + for (int i = 0; i < this.getColumnCount(); i++) + { + groupWidth += this.getColumn(i).getWidth(); + + // If this is the last column of a group. + if (i == ((Integer)lastColumn.get(group)).intValue()) + { + while (group < groupTableColumnModel.getColumnCount() && i == ((Integer)lastColumn.get(group)).intValue()) + { + groupTableColumnModel.getColumn(group).setWidth(groupWidth); + + groupWidth = 0; + group++; + } + } + } + } + + public void columnAdded(TableColumnModelEvent e) {} + public void columnMarginChanged(ChangeEvent e) {} + public void columnMoved(TableColumnModelEvent e) {} + public void columnRemoved(TableColumnModelEvent e) {} + public void columnSelectionChanged(ListSelectionEvent e) {} + + /** + * If something changed in the columns of the table, then adjust the group widths. + */ + @Override + protected void fireColumnMarginChanged() { + // Size must have changed then. + updateGroups(); + super.fireColumnMarginChanged(); + } + + /** + * Empties this GUIGroupedTableColumnModel. + */ + public void clear() + { + while (this.getColumnCount() > 0) + { + this.removeColumn(this.getColumn(0)); + } + + while (groupTableColumnModel.getColumnCount() > 0) + { + groupTableColumnModel.removeColumn(groupTableColumnModel.getColumn(0)); + } + + this.lastColumn.clear(); + } +} + diff --git a/prism/src/userinterface/util/GUIGroupedTableHeader.java b/prism/src/userinterface/util/GUIGroupedTableHeader.java new file mode 100644 index 00000000..818f2c13 --- /dev/null +++ b/prism/src/userinterface/util/GUIGroupedTableHeader.java @@ -0,0 +1,188 @@ +//============================================================================== +// +// Copyright (c) 2002-2006, Mark Kattenbelt +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package userinterface.util; + +import java.awt.*; +import java.awt.event.*; + +import javax.swing.*; +import javax.swing.event.*; +import javax.swing.table.*; + + +/** + * @author mxk + * An object to represent a grouped TableHeader. It extends JTableHeader, but actually consists of two separate + * JTableHeaders. Some of this could be tidied up, but it is build more or less to Swings concepts. + */ +public class GUIGroupedTableHeader extends JTableHeader implements TableColumnModelListener, MouseListener +{ + private JTableHeader bottomHeader; + private JTableHeader topHeader; + + /** + * Creates a new GUIGroupedTableHeader. + * @param model The column model that is the basis of this table header (must be grouped). + */ + public GUIGroupedTableHeader(GUIGroupedTableColumnModel model) + { + super(); + removeAll(); + + topHeader = new JTableHeader(model.getGroupTableColumnModel()); + topHeader.setResizingAllowed(false); + topHeader.setReorderingAllowed(false); + + final TableCellRenderer renderer = topHeader.getDefaultRenderer(); + topHeader.setDefaultRenderer(new TableCellRenderer() { + public Component getTableCellRendererComponent(JTable table, Object value, boolean isSelected, boolean hasFocus, int row, int column) + { + Component component = renderer.getTableCellRendererComponent(table, value, isSelected, hasFocus, row, column); + component.setFont(topHeader.getFont().deriveFont(Font.BOLD)); + return component; + } + }); + + bottomHeader = new JTableHeader(model); + bottomHeader.setReorderingAllowed(false); + + setLayout(new GridLayout(2,1)); + + add(topHeader); + add(bottomHeader); + + model.updateGroups(); + + this.setPreferredSize(new Dimension(bottomHeader.getPreferredSize().width, bottomHeader.getPreferredSize().height * 2)); + this.setMinimumSize(new Dimension(bottomHeader.getMinimumSize().width, bottomHeader.getMinimumSize().height * 2)); + this.setMaximumSize(new Dimension(bottomHeader.getMaximumSize().width, bottomHeader.getMaximumSize().height * 2)); + + Component[] cs = this.getComponents(); + for (int i = 0; i < cs.length; i++) + { + cs[i].addMouseListener(this); + } + } + + + /** + * A fairly ugly hack to prevent a CellRenderer to be added to this container. More elegant solutions are welcome. + * @see java.awt.Container#addImpl(java.awt.Component, java.lang.Object, int) + */ + @Override + protected void addImpl(Component comp, Object constraints, int index) { + // TODO Auto-generated method stub + if (this.getComponents().length < 2) + { + super.addImpl(comp, constraints, index); + } + } + + /** + * Overwritten to never allow reordering. + * @see javax.swing.table.JTableHeader#setReorderingAllowed(boolean) + */ + @Override + public void setReorderingAllowed(boolean reorderingAllowed) { + super.setReorderingAllowed(false); + } + + /** + * Overwritten to always return the resizing column of the bottom JTableHeader. + * @see javax.swing.table.JTableHeader#getResizingColumn() + */ + @Override + public TableColumn getResizingColumn() + { + return bottomHeader.getResizingColumn(); + } + + /** + * Overwritten to give the JTableHeaders a change to resize as well. + * @see javax.swing.table.JTableHeader#resizeAndRepaint() + */ + @Override + public void resizeAndRepaint() + { + if (topHeader != null && bottomHeader != null) + { + this.setPreferredSize(new Dimension(bottomHeader.getPreferredSize().width, bottomHeader.getPreferredSize().height * 2)); + this.setMinimumSize(new Dimension(bottomHeader.getMinimumSize().width, bottomHeader.getMinimumSize().height * 2)); + this.setMaximumSize(new Dimension(bottomHeader.getMaximumSize().width, bottomHeader.getMaximumSize().height * 2)); + + this.doLayout(); + } + + super.resizeAndRepaint(); + } + + /** + * Set the column model. + * @param columnModel The grouped column model to use. + */ + public void setColumnModel(GUIGroupedTableColumnModel columnModel) { + + topHeader.setColumnModel(columnModel.getGroupTableColumnModel()); + bottomHeader.setColumnModel(columnModel); + + this.resizeAndRepaint(); + + columnModel.updateGroups(); + super.setColumnModel(columnModel); + } + + /** + * Overwritten to catch events of child components. + */ + public void mouseClicked(MouseEvent e) { + this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); + } + + /** + * Overwritten to catch events of child components. + */ + public void mouseEntered(MouseEvent e) { + this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); + } + + /** + * Overwritten to catch events of child components. + */ + public void mouseExited(MouseEvent e) { + this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); + } + + /** + * Overwritten to catch events of child components. + */ + public void mousePressed(MouseEvent e) { + this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); + } + + /** + * Overwritten to catch events of child components. + */ + public void mouseReleased(MouseEvent e) { + this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); + } +} diff --git a/prism/src/userinterface/util/GUIGroupedTableModel.java b/prism/src/userinterface/util/GUIGroupedTableModel.java new file mode 100644 index 00000000..6718b87d --- /dev/null +++ b/prism/src/userinterface/util/GUIGroupedTableModel.java @@ -0,0 +1,53 @@ +//============================================================================== +// +// Copyright (c) 2002-2006, Mark Kattenbelt +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package userinterface.util; + +import javax.swing.table.TableModel; + +/** + * @author mxk + * An interface which extends {@link TableModel} such that also group information can + * be extracted automatically. Note that groups are always non-empty. + */ +public interface GUIGroupedTableModel extends TableModel +{ + /** + * @return The number of groups in this model. + */ + public int getGroupCount(); + + /** + * Retrieves the name of a group. + * @param groupIndex The index of a group. + * @return The name of the nth group, where n = groupIndex. + * @see TableModel.getColumnName(int columnIndex). + */ + public String getGroupName(int groupIndex); + + /** + * Retrieves the index of the last `normal' column in a group. + * @param groupIndex The index of a group. + * @return The index of the last column in this group. + */ + public int getLastColumnOfGroup(int groupIndex); +}