diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 45714e7f..deec3172 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -40,6 +40,8 @@ import java.awt.event.KeyEvent; import java.awt.event.MouseAdapter; import java.awt.event.MouseEvent; import java.awt.event.MouseListener; +import java.util.ArrayList; +import java.util.List; import java.util.Vector; import javax.swing.AbstractAction; @@ -2221,8 +2223,13 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect repaint(); } + enum UpdateTableModelColumn { + ACTION, PROB, UPDATE + }; + class UpdateTableModel extends AbstractTableModel { + private List visibleColumns = new ArrayList<>(); public boolean oldUpdate; private int oldStep; @@ -2235,7 +2242,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public int getColumnCount() { - return pathActive ? 3 : 0; + return visibleColumns.size(); } public int getRowCount() @@ -2251,12 +2258,12 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect { if (pathActive) { try { - switch (columnIndex) { - case 0: + switch (visibleColumns.get(columnIndex)) { + case ACTION: return engine.getTransitionActionString(rowIndex); - case 1: + case PROB: return "" + engine.getTransitionProbability(rowIndex); - case 2: + case UPDATE: return engine.getTransitionUpdateString(rowIndex); default: return ""; @@ -2268,21 +2275,21 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect return ""; } - public String getColumnName(int column) + public String getColumnName(int columnIndex) { if (pathActive) { - switch (column) { - case 0: + switch (visibleColumns.get(columnIndex)) { + case ACTION: return engine.getModel().getActionStringDescription(); - case 1: + case PROB: return parsedModel == null ? "Probability" : parsedModel.getModelType().probabilityOrRate(); - case 2: + case UPDATE: return "Update"; default: return ""; } - } else - return ""; + } + return ""; } /** @@ -2295,12 +2302,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } oldUpdate = false; oldStep = -1; + setVisibleColumns(); doEnables(); fireTableDataChanged(); - currentUpdatesTable.setEnabled(true); currentUpdatesTable.setToolTipText("Double click on an update to manually execute it"); - if (getRowCount() > 0) { currentUpdatesTable.getSelectionModel().setSelectionInterval(0, 0); } @@ -2311,19 +2317,18 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect */ public void updateUpdatesTable(int oldStep) throws PrismException { - if (oldStep == pathTable.getRowCount() - 1) // if current state selected - { + if (oldStep == pathTable.getRowCount() - 1) { + // if current state selected updateUpdatesTable(); } else { this.oldStep = oldStep; oldUpdate = true; + setVisibleColumns(); doEnables(); engine.computeTransitionsForStep(oldStep); fireTableDataChanged(); - currentUpdatesTable.setEnabled(false); currentUpdatesTable.setToolTipText(null); - if (getRowCount() > 0) { int selectThis = engine.getChoiceOfPathStep(oldStep); currentUpdatesTable.getSelectionModel().setSelectionInterval(selectThis, selectThis); @@ -2331,6 +2336,16 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } } + public void setVisibleColumns() + { + visibleColumns.clear(); + visibleColumns.add(UpdateTableModelColumn.ACTION); + if (parsedModel != null && parsedModel.getModelType().isProbabilistic()) { + visibleColumns.add(UpdateTableModelColumn.PROB); + } + visibleColumns.add(UpdateTableModelColumn.UPDATE); + } + public void restartUpdatesTable() { fireTableStructureChanged();