GUI constant picker for graphs defaults to property constants first.

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

prism/src/prism/ResultsCollection.java

@@ -39,6 +39,8 @@ public class ResultsCollection
 {
 	// Info about the constants over which these results range
 	private Vector<DefinedConstant> rangingConstants;
+	private int numMFRangingConstants;
+	private int numPFRangingConstants;
 
 	// Storage of the actual results
 	private TreeNode root;
@@ -61,11 +63,12 @@ public class ResultsCollection
 	{
 		resultListeners = new Vector<ResultListener>();
 		rangingConstants = new Vector<DefinedConstant>();
-
 		Vector<DefinedConstant> tmpRangingConstants = uCons.getRangingConstants();
 		for (int i = 0; i < tmpRangingConstants.size(); i++) {
 			rangingConstants.add(tmpRangingConstants.get(i));
 		}
+		numMFRangingConstants = uCons.getNumModelRangingConstants(); 
+		numPFRangingConstants = uCons.getNumPropertyRangingConstants(); 
 
 		this.root = (rangingConstants.size() > 0) ? new TreeNode(0) : new TreeLeaf();
 		this.resultName = (resultName == null) ? "Result" : resultName;
@@ -81,6 +84,16 @@ public class ResultsCollection
 		return rangingConstants.size();
 	}
 
+	public int getNumModelRangingConstants()
+	{
+		return numMFRangingConstants;
+	}
+
+	public int getNumPropertyRangingConstants()
+	{
+		return numPFRangingConstants;
+	}
+
 	public boolean addResultListener(ResultListener resultListener)
 	{
 		return resultListeners.add(resultListener);

prism/src/userinterface/properties/GUIGraphPicker.java

@@ -242,9 +242,14 @@ public class GUIGraphPicker extends javax.swing.JDialog
 			this.selectAxisConstantCombo.addItem(dc.getName());
 		}
 
-		// select the first constant for the x axis
-		if (selectAxisConstantCombo.getItemCount() > 0)
-			selectAxisConstantCombo.setSelectedIndex(0);
+		// select the default constant for the x axis
+		// (first property if there is one, if not first model one)
+		if (selectAxisConstantCombo.getItemCount() > 0) {
+			if (resultsCollection.getNumPropertyRangingConstants() > 0)
+				selectAxisConstantCombo.setSelectedIndex(resultsCollection.getNumModelRangingConstants());
+			else
+				selectAxisConstantCombo.setSelectedIndex(0);
+		}
 		// and disable it in the picker list
 		pickerList.disableLine(0);