Further simulator improvements.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1856 bbc10eb1-c90d-0410-af57-cb519fbb1720

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;
+	}
 }

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)
 	// ------------------------------------------------------------------------------

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);
 		}
 	}
 

prism/src/userinterface/simulator/GUISimulatorUpdatesTable.java

@@ -90,7 +90,6 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis
 		updateTableRenderer = new UpdateTableRenderer();
 		setDefaultRenderer(Object.class, updateTableRenderer);
 
-	
 		setAutoResizeMode(JTable.AUTO_RESIZE_LAST_COLUMN);
 
 		InputMap inputMap = new ComponentInputMap(this);
@@ -105,8 +104,7 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis
 			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
@@ -120,12 +118,12 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis
 			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);
 				}
 			}
 		});
@@ -133,16 +131,17 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis
 		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);
+		if (updateTableRenderer != null)
+			updateTableRenderer.setFont(font);
 		setRowHeight(getFontMetrics(font).getHeight() + 4);
-    	if (header != null) header.setFixedCellHeight(getRowHeight());
+		if (header != null)
+			header.setFixedCellHeight(getRowHeight());
 	}
 
 	public void valueChanged(ListSelectionEvent e)
@@ -172,34 +171,27 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis
 
 			int dist;
 
-		    if(sim.getModulesFile().getModelType() == ModelType.CTMC)
+			// Select default background colour
+			// (depends on choice, for nondeterministic models)
+			if (sim.getModulesFile().getModelType().nondeterministic())
+				dist = utm.getChoiceIndexOf(row);
+			else
 				dist = 0;
-		    else dist = utm.getProbabilityDistributionOf(row);
-		    
 			Color c = DISTRIBUTION_COLOURS[dist % 2];
 
-		   
-		    if(isSelected)
-		    {
+			if (isSelected) {
 				Color newCol = new Color(c.getRed() - 20, c.getGreen() - 20, c.getBlue());
-			if(utm.oldUpdate)
-			{
+				if (utm.oldUpdate) {
 					newCol = new Color(newCol.getRed() - 7, newCol.getGreen() - 7, newCol.getBlue() - 7);
 					renderer.setBackground(newCol);
-			}
-			else
-			{
+				} else {
 					renderer.setBackground(newCol);
 				}
-		    }
-		    else
-		    {
-			if(utm.oldUpdate)
-			{
+			} else {
+				if (utm.oldUpdate) {
 					Color newCol = new Color(c.getRed() - 7, c.getGreen() - 7, c.getBlue() - 7);
 					renderer.setBackground(newCol);
-			}
-			else
+				} else
 					renderer.setBackground(c);
 			}
 
@@ -213,9 +205,6 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis
 		}
 	}
 
-    
-    
-    
 	class UpdateHeaderRenderer extends JButton implements ListCellRenderer
 	{
 
@@ -236,26 +225,21 @@ public class GUISimulatorUpdatesTable extends JTable implements ListSelectionLis
 			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);
 			selected = getSelectedRow() == index;
 
-			if(selected)
-			{
+			if (selected) {
 				setIcon(selectedIcon);
-			}
-			else
-			{
+			} else {
 				setIcon(null);
 			}
 
 			return this;
 		}
 
-		
 	}
 
 	class UpdateHeaderListModel extends AbstractListModel