From cf907acc072ab6596d1340f29c542ba238c8261a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 13 Jun 2012 20:17:26 +0000 Subject: [PATCH] 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 | 15 ++++++++++++++- .../userinterface/properties/GUIGraphPicker.java | 11 ++++++++--- 2 files changed, 22 insertions(+), 4 deletions(-) diff --git a/prism/src/prism/ResultsCollection.java b/prism/src/prism/ResultsCollection.java index 7301fc35..a66d185f 100644 --- a/prism/src/prism/ResultsCollection.java +++ b/prism/src/prism/ResultsCollection.java @@ -39,6 +39,8 @@ public class ResultsCollection { // Info about the constants over which these results range private Vector 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(); rangingConstants = new Vector(); - Vector 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); diff --git a/prism/src/userinterface/properties/GUIGraphPicker.java b/prism/src/userinterface/properties/GUIGraphPicker.java index 56a2740f..dc8ba5af 100644 --- a/prism/src/userinterface/properties/GUIGraphPicker.java +++ b/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);