diff --git a/prism/src/prism/ModelType.java b/prism/src/prism/ModelType.java index 3d982843..ffebb739 100644 --- a/prism/src/prism/ModelType.java +++ b/prism/src/prism/ModelType.java @@ -5,6 +5,9 @@ public enum ModelType { // List of model types (ordered alphabetically) CTMC, CTMDP, DTMC, MDP, PTA, STPG; + /** + * Get the full name, in words, of the this model type. + */ public String fullName() { switch (this) { @@ -25,6 +28,9 @@ public enum ModelType { return ""; } + /** + * Do the transitions in a choice sum to 1 for this model type? + */ public boolean choicesSumToOne() { switch (this) { @@ -41,6 +47,9 @@ public enum ModelType { return true; } + /** + * Are time delay continuous for this model type? + */ public boolean continuousTime() { switch (this) { @@ -56,4 +65,23 @@ public enum ModelType { // Should never happen return true; } + + /** + * Does this model allow nondeterministic choices? + */ + public boolean nondeterministic() + { + switch (this) { + case DTMC: + case CTMC: + return false; + case MDP: + case STPG: + case PTA: + case CTMDP: + return true; + } + // Should never happen + return true; + } } diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index eaffe88d..1130c842 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -732,7 +732,7 @@ public class SimulatorEngine } // ------------------------------------------------------------------------------ - // State/Choice/Transition querying + // Querying of current state and its available choices/transitions // ------------------------------------------------------------------------------ /** @@ -767,6 +767,14 @@ public class SimulatorEngine return transitionList.getChoice(i).size(); } + /** + * Get the index of the choice containing a transition of a given index. + */ + public int getChoiceIndexOfTransition(int index) + { + return transitionList.getChoiceIndexOfTransition(index); + } + /** * Get the probability/rate of a transition within a choice, specified by its index/offset. */ @@ -803,63 +811,26 @@ public class SimulatorEngine return transitionList.computeTransitionTarget(index, currentState); } - /** - * Returns the action label of a transition in the list of those currently available. - * An empty string denotes an unlabelled (asynchronous) transition. - * @param i: The index of the transition being queried - */ - public String getTransitionAction(int index) throws PrismException - { - if (index < 0 || index >= transitionList.getNumTransitions()) - throw new PrismException("Invalid transition index " + index); - return transitionList.getChoiceOfTransition(index).getAction(); - } - /** * TODO - * Returns the module name of the udpate at the given index. - * - * @param i - * the index of the update of interest. - * @return the module name of the udpate at the given index. */ public String getTransitionModuleOrAction(int index) { return transitionList.getTransitionActionString(index); + //return transitionList.getChoiceOfTransition(index).getAction(); } /** * Returns a string representation of the assignments for the current update at the given index. - * - * @param index - * the index of the update of interest. - * @return a string representation of the assignments for the current update at the given index. + * TODO */ public String getAssignmentDescriptionOfUpdate(int index) { return transitionList.getTransitionUpdateString(index); - /* - int i, n; - boolean first = true; - State v = path.getCurrentState(); - State v2 = getTransitionTarget(index); - String s = ""; - n = getNumVariables(); - for (i = 0; i < n; i++) { - if (!v.varValues[i].equals(v2.varValues[i])) { - if (first) - first = false; - else - s += "&"; - s += "(" + getVariableName(i) + "'=" + v2.varValues[i] + ")"; - } - } - return s; - */ } // ------------------------------------------------------------------------------ - // Path querying + // Querying of current path // ------------------------------------------------------------------------------ /** @@ -1061,36 +1032,6 @@ public class SimulatorEngine path.exportToLog(log, timeCumul, colSep, vars); } - // ------------------------------------------------------------------------------ - // UPDATE HANDLER UPDATE METHODS - // ------------------------------------------------------------------------------ - - /** - * Returns the index of the variable being assigned to for the current update at the given index (updateIndex) and - * for its assignment indexed assignmentIndex - */ - private static native int getAssignmentVariableIndexOfUpdate(int updateIndex, int assignmentIndex); - - /** - * Returns the value of the assignment for the current update at the given index (updateIndex and for its assignment - * indexed assignmentIndex. - */ - private static native int getAssignmentValueOfUpdate(int updateIndex, int assignmentIndex); - - /** - * For mdps, updates can belong to different probability distributions. These probability distributions are indexed. - * This returns the probability distribution that the indexed update belongs to. - * - * @param updateIndex - * the index of the update of interest. - * @return the probability distribution that the indexed update belongs to. - */ - public int getDistributionIndexOfUpdate(int updateIndex) - { - // TODO - return 0; - } - // ------------------------------------------------------------------------------ // PROPERTIES AND SAMPLING (not yet sorted) // ------------------------------------------------------------------------------ diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index cb0d60e7..ec1dc502 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -3492,9 +3492,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } } - public int getProbabilityDistributionOf(int row) + public int getChoiceIndexOf(int row) { - return engine.getDistributionIndexOfUpdate(row); + return engine.getChoiceIndexOfTransition(row); } } diff --git a/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java b/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java index 49605818..7180a986 100644 --- a/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java @@ -43,188 +43,177 @@ import userinterface.GUIPrism; */ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionListener { - public static Color [] DISTRIBUTION_COLOURS = { new Color(255,255,255), //white - new Color(253,255,201) }; //yellow - /*new Color(224,255,224), //green - new Color(255,227,255), //pink - new Color(255,234,199), //orange - new Color(209,217,255), //blue - new Color(226,199,255), //purple - new Color(212,255,255)} ;*/ //cyan - private GUISimulator.UpdateTableModel utm; - - private UpdateHeaderListModel headerModel; - private JList header; - private UpdateHeaderRenderer updateHeaderRenderer; - private UpdateTableRenderer updateTableRenderer; - - private GUISimulator sim; - - /** Creates a new instance of GUISimulatorUpdatesTable */ - public GUISimulatorUpdatesTable(GUISimulator.UpdateTableModel utm, GUISimulator sim) - { + public static Color[] DISTRIBUTION_COLOURS = { new Color(255, 255, 255), //white + new Color(253, 255, 201) }; //yellow + /*new Color(224,255,224), //green + new Color(255,227,255), //pink + new Color(255,234,199), //orange + new Color(209,217,255), //blue + new Color(226,199,255), //purple + new Color(212,255,255)} ;*///cyan + private GUISimulator.UpdateTableModel utm; + + private UpdateHeaderListModel headerModel; + private JList header; + private UpdateHeaderRenderer updateHeaderRenderer; + private UpdateTableRenderer updateTableRenderer; + + private GUISimulator sim; + + /** Creates a new instance of GUISimulatorUpdatesTable */ + public GUISimulatorUpdatesTable(GUISimulator.UpdateTableModel utm, GUISimulator sim) + { super(utm); this.sim = sim; this.utm = utm; - + this.getSelectionModel().addListSelectionListener(this); - + setColumnSelectionAllowed(false); - getSelectionModel().setSelectionMode(ListSelectionModel.SINGLE_SELECTION); - + getSelectionModel().setSelectionMode(ListSelectionModel.SINGLE_SELECTION); + headerModel = new UpdateHeaderListModel(); JList rowHeader = new JList(headerModel); - + rowHeader.setBackground(new JPanel().getBackground()); - + rowHeader.setFixedCellWidth(15); - + rowHeader.setFixedCellHeight(getRowHeight()); //+ getRowMargin()); //getIntercellSpacing().height); updateHeaderRenderer = new UpdateHeaderRenderer(this); rowHeader.setCellRenderer(updateHeaderRenderer); - + this.header = rowHeader; - + updateTableRenderer = new UpdateTableRenderer(); setDefaultRenderer(Object.class, updateTableRenderer); - - + setAutoResizeMode(JTable.AUTO_RESIZE_LAST_COLUMN); - + InputMap inputMap = new ComponentInputMap(this); - + inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_DOWN, 0), "Down"); inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_UP, 0), "Up"); - + ActionMap actionMap = new ActionMap(); - - actionMap.put("Down", new AbstractAction() + + actionMap.put("Down", new AbstractAction() { - public void actionPerformed(ActionEvent e) + public void actionPerformed(ActionEvent e) { int selectedRow = GUISimulatorUpdatesTable.this.getSelectedRow(); - if (selectedRow != -1) - { + if (selectedRow != -1) { if (selectedRow < GUISimulatorUpdatesTable.this.getRowCount() - 1) GUISimulatorUpdatesTable.this.getSelectionModel().setSelectionInterval(selectedRow + 1, selectedRow + 1); else GUISimulatorUpdatesTable.this.getSelectionModel().setSelectionInterval(0, 0); } } - }); - - actionMap.put("Up", new AbstractAction() + }); + + actionMap.put("Up", new AbstractAction() { - public void actionPerformed(ActionEvent e) + public void actionPerformed(ActionEvent e) { int selectedRow = GUISimulatorUpdatesTable.this.getSelectedRow(); - if (selectedRow != -1) - { + if (selectedRow != -1) { if (selectedRow >= 1) GUISimulatorUpdatesTable.this.getSelectionModel().setSelectionInterval(selectedRow - 1, selectedRow - 1); else - GUISimulatorUpdatesTable.this.getSelectionModel().setSelectionInterval(GUISimulatorUpdatesTable.this.getRowCount()-1, GUISimulatorUpdatesTable.this.getRowCount()-1); + GUISimulatorUpdatesTable.this.getSelectionModel().setSelectionInterval(GUISimulatorUpdatesTable.this.getRowCount() - 1, + GUISimulatorUpdatesTable.this.getRowCount() - 1); } } - }); - + }); + this.setInputMap(JComponent.WHEN_FOCUSED, inputMap); this.setActionMap(actionMap); - - - } - - /** Override set font to pass changes onto renderer(s) and set row height */ - public void setFont(Font font) - { - super.setFont(font); - if (updateTableRenderer != null) updateTableRenderer.setFont(font); - setRowHeight(getFontMetrics(font).getHeight() + 4); - if (header != null) header.setFixedCellHeight(getRowHeight()); - } - - public void valueChanged(ListSelectionEvent e) - { - if(headerModel != null) - headerModel.updateHeader(); - repaint(); - } - - public JList getUpdateRowHeader() - { - return header; - } - - class UpdateTableRenderer implements TableCellRenderer - { + + } + + /** Override set font to pass changes onto renderer(s) and set row height */ + public void setFont(Font font) + { + super.setFont(font); + if (updateTableRenderer != null) + updateTableRenderer.setFont(font); + setRowHeight(getFontMetrics(font).getHeight() + 4); + if (header != null) + header.setFixedCellHeight(getRowHeight()); + } + + public void valueChanged(ListSelectionEvent e) + { + if (headerModel != null) + headerModel.updateHeader(); + repaint(); + } + + public JList getUpdateRowHeader() + { + return header; + } + + class UpdateTableRenderer implements TableCellRenderer + { JTextField renderer; - + public UpdateTableRenderer() { - renderer = new JTextField(""); + renderer = new JTextField(""); } - + public Component getTableCellRendererComponent(JTable table, Object value, boolean isSelected, boolean hasFocus, int row, int column) { - renderer.setText(value.toString()); - - int dist; - - if(sim.getModulesFile().getModelType() == ModelType.CTMC) - dist = 0; - else dist = utm.getProbabilityDistributionOf(row); - - Color c = DISTRIBUTION_COLOURS[dist%2]; - - - if(isSelected) - { - Color newCol = new Color(c.getRed()-20, c.getGreen()-20, c.getBlue()); - if(utm.oldUpdate) - { - newCol = new Color(newCol.getRed()-7, newCol.getGreen()-7, newCol.getBlue()-7); - renderer.setBackground(newCol); - } + renderer.setText(value.toString()); + + int dist; + + // Select default background colour + // (depends on choice, for nondeterministic models) + if (sim.getModulesFile().getModelType().nondeterministic()) + dist = utm.getChoiceIndexOf(row); else - { - renderer.setBackground(newCol); - } - } - else - { - if(utm.oldUpdate) - { - Color newCol = new Color(c.getRed()-7, c.getGreen()-7, c.getBlue()-7); - renderer.setBackground(newCol); + dist = 0; + Color c = DISTRIBUTION_COLOURS[dist % 2]; + + if (isSelected) { + Color newCol = new Color(c.getRed() - 20, c.getGreen() - 20, c.getBlue()); + if (utm.oldUpdate) { + newCol = new Color(newCol.getRed() - 7, newCol.getGreen() - 7, newCol.getBlue() - 7); + renderer.setBackground(newCol); + } else { + renderer.setBackground(newCol); + } + } else { + if (utm.oldUpdate) { + Color newCol = new Color(c.getRed() - 7, c.getGreen() - 7, c.getBlue() - 7); + renderer.setBackground(newCol); + } else + renderer.setBackground(c); } - else - renderer.setBackground(c); - } - - renderer.setBorder(new EmptyBorder(1, 1, 1, 1)); - return renderer; + + renderer.setBorder(new EmptyBorder(1, 1, 1, 1)); + return renderer; } - + public void setFont(Font font) { renderer.setFont(font); } - } - - - - + } + class UpdateHeaderRenderer extends JButton implements ListCellRenderer { - + boolean selected; ImageIcon selectedIcon; - + UpdateHeaderRenderer(JTable table) { - selected = false; + selected = false; /*JTableHeader header = table.getTableHeader(); setOpaque(true); setBorder(UIManager.getBorder("TableHeader.cellBorder")); @@ -232,51 +221,46 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis setForeground(header.getForeground()); setBackground(header.getBackground()); setFont(header.getFont());*/ - setBorder(null); - selectedIcon = GUIPrism.getIconFromImage("smallItemSelected.png"); + setBorder(null); + selectedIcon = GUIPrism.getIconFromImage("smallItemSelected.png"); } - - public Component getListCellRendererComponent( JList list, - Object value, int index, boolean isSelected, boolean cellHasFocus) + + public Component getListCellRendererComponent(JList list, Object value, int index, boolean isSelected, boolean cellHasFocus) { - - setBorder(null); + + setBorder(null); selected = getSelectedRow() == index; - - if(selected) - { - setIcon(selectedIcon); - } - else - { - setIcon(null); + + if (selected) { + setIcon(selectedIcon); + } else { + setIcon(null); } - + return this; } - - + } - + class UpdateHeaderListModel extends AbstractListModel { - + public Object getElementAt(int index) { - return ""+index; + return "" + index; } - + public int getSize() { return utm.getRowCount(); } - + public void updateHeader() { fireContentsChanged(this, 0, utm.getRowCount()); - + //System.out.println("The tables width is "+getWidth()); } - + } }