From 93526c953c8f9e5b93a99af8a63c248a67df2951 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 20 Apr 2011 09:53:12 +0000 Subject: [PATCH] More sensible column ordering in GUI simulator (action labels, time columns). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2819 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../userinterface/simulator/GUISimulator.java | 102 +++++++++--------- .../simulator/GUISimulatorPathTable.java | 11 +- 2 files changed, 60 insertions(+), 53 deletions(-) diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 7642329f..1d56efa6 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -2666,7 +2666,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } else { int groupCount = 0; - if (view.showSteps() || view.showActions()) { + if (view.showActions() || view.showSteps()) { groupCount++; } @@ -2724,7 +2724,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } else { int groupCount = 0; - if (view.showSteps() || view.showActions()) { + if (view.showActions() || view.showSteps()) { if (groupCount == groupIndex) { return "Step"; } @@ -2800,7 +2800,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect int groupCount = 0; - if (view.showSteps() || view.showActions()) { + if (view.showActions() || view.showSteps()) { if (groupCount == groupIndex) { return null; } @@ -2856,15 +2856,15 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public int getLastColumnOfGroup(int groupIndex) { int stepStart = 0; - int timeStart = stepStart + (view.showSteps() ? 1 : 0) + (view.showActions() ? 1 : 0); - int varStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0) + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); + int timeStart = stepStart + (view.showActions() ? 1 : 0) + (view.showSteps() ? 1 : 0); + int varStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0) + (view.showCumulativeTime() && view.showTime() ? 1 : 0); int rewardStart = varStart + view.getVisibleVariables().size(); int groupCount = 0; - if (view.showSteps() || view.showActions()) { + if (view.showActions() || view.showSteps()) { if (groupCount == groupIndex) { - if (view.showSteps() && view.showActions()) + if (view.showActions() && view.showSteps()) return stepStart + 1; else return stepStart; @@ -2873,9 +2873,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect groupCount++; } - if (view.canShowTime() && (view.showTime() || view.showCumulativeTime())) { + if (view.canShowTime() && (view.showCumulativeTime() || view.showTime())) { if (groupCount == groupIndex) { - if (view.showTime() && view.showCumulativeTime()) + if (view.showCumulativeTime() && view.showTime()) return timeStart + 1; else return timeStart; @@ -2963,9 +2963,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } else { int colCount = 0; - colCount += (view.showSteps() ? 1 : 0); colCount += (view.showActions() ? 1 : 0); - colCount += (view.canShowTime() && view.showTime() ? 1 : 0) + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); + colCount += (view.showSteps() ? 1 : 0); + colCount += (view.canShowTime() && view.showCumulativeTime() ? 1 : 0) + (view.canShowTime() && view.showTime() ? 1 : 0); colCount += view.getVisibleVariables().size(); colCount += view.getVisibleRewardColumns().size(); @@ -3003,22 +3003,22 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public String getColumnName(int columnIndex) { if (pathActive) { - int stepStart = 0; - int actionStart = stepStart + (view.showSteps() ? 1 : 0); - int timeStart = actionStart + (view.showActions() ? 1 : 0); - int cumulativeTimeStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0); - int varStart = cumulativeTimeStart + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); + int actionStart = 0; + int stepStart = actionStart + (view.showActions() ? 1 : 0); + int cumulativeTimeStart = stepStart + (view.showSteps() ? 1 : 0); + int timeStart = cumulativeTimeStart + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); + int varStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0); int rewardStart = varStart + view.getVisibleVariables().size(); // The step column - if (stepStart <= columnIndex && columnIndex < actionStart) { - return "#"; - } else if (actionStart <= columnIndex && columnIndex < timeStart) { + if (actionStart <= columnIndex && columnIndex < stepStart) { return "Action"; - } else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) { - return "Time"; - } else if (cumulativeTimeStart <= columnIndex && columnIndex < varStart) { + } else if (stepStart <= columnIndex && columnIndex < cumulativeTimeStart) { + return "#"; + } else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) { return "Time (+)"; + } else if (timeStart <= columnIndex && columnIndex < varStart) { + return "Time"; } // A variable column else if (varStart <= columnIndex && columnIndex < rewardStart) { @@ -3035,22 +3035,22 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public String getColumnToolTip(int columnIndex) { if (pathActive) { - int stepStart = 0; - int actionStart = stepStart + (view.showSteps() ? 1 : 0); - int timeStart = actionStart + (view.showActions() ? 1 : 0); - int cumulativeTimeStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0); - int varStart = cumulativeTimeStart + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); + int actionStart = 0; + int stepStart = actionStart + (view.showActions() ? 1 : 0); + int cumulativeTimeStart = stepStart + (view.showSteps() ? 1 : 0); + int timeStart = cumulativeTimeStart + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); + int varStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0); int rewardStart = varStart + view.getVisibleVariables().size(); // The step column - if (stepStart <= columnIndex && columnIndex < actionStart) { - return "Index of state in path"; - } else if (actionStart <= columnIndex && columnIndex < timeStart) { + if (actionStart <= columnIndex && columnIndex < stepStart) { return "Action label or module name"; - } else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) { - return "Time spent in state"; - } else if (cumulativeTimeStart <= columnIndex && columnIndex < varStart) { + } else if (stepStart <= columnIndex && columnIndex < cumulativeTimeStart) { + return "Index of state in path"; + } else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) { return "Cumulative time"; + } else if (timeStart <= columnIndex && columnIndex < varStart) { + return "Time spent in state"; } // A variable column else if (varStart <= columnIndex && columnIndex < rewardStart) { @@ -3075,35 +3075,35 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public Object getValueAt(int rowIndex, int columnIndex) { if (pathActive) { - int stepStart = 0; - int actionStart = stepStart + (view.showSteps() ? 1 : 0); - int timeStart = actionStart + (view.showActions() ? 1 : 0); - int cumulativeTimeStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0); - int varStart = cumulativeTimeStart + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); + int actionStart = 0; + int stepStart = actionStart + (view.showActions() ? 1 : 0); + int cumulativeTimeStart = stepStart + (view.showSteps() ? 1 : 0); + int timeStart = cumulativeTimeStart + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); + int varStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0); int rewardStart = varStart + view.getVisibleVariables().size(); - // The step column - if (stepStart <= columnIndex && columnIndex < actionStart) { - return "" + rowIndex; - } // The action column - else if (actionStart <= columnIndex && columnIndex < timeStart) { - actionValue = new ActionValue(engine.getModuleOrActionOfPathStep(rowIndex)); - actionValue.setActionValueUnknown(rowIndex >= engine.getPathSize()); + if (actionStart <= columnIndex && columnIndex < stepStart) { + actionValue = new ActionValue(rowIndex == 0 ? "" : engine.getModuleOrActionOfPathStep(rowIndex - 1)); + actionValue.setActionValueUnknown(false); return actionValue; } - // Time column - else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) { - timeValue = new TimeValue(engine.getTimeSpentInPathStep(rowIndex), false); - timeValue.setTimeValueUnknown(rowIndex >= engine.getPathSize()); - return timeValue; + // The step column + else if (stepStart <= columnIndex && columnIndex < cumulativeTimeStart) { + return "" + rowIndex; } // Cumulative time column - else if (cumulativeTimeStart <= columnIndex && columnIndex < varStart) { + else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) { timeValue = new TimeValue(engine.getCumulativeTimeUpToPathStep(rowIndex), true); timeValue.setTimeValueUnknown(rowIndex > engine.getPathSize()); // Never unknown return timeValue; } + // Time column + else if (timeStart <= columnIndex && columnIndex < varStart) { + timeValue = new TimeValue(engine.getTimeSpentInPathStep(rowIndex), false); + timeValue.setTimeValueUnknown(rowIndex >= engine.getPathSize()); + return timeValue; + } // A variable column else if (varStart <= columnIndex && columnIndex < rewardStart) { Variable var = ((Variable) view.getVisibleVariables().get(columnIndex - varStart)); diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java index dbd382bd..94559a0e 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java @@ -280,13 +280,20 @@ public class GUISimulatorPathTable extends GUIGroupedTable GUISimulator.ActionValue actionValue = (GUISimulator.ActionValue)value; if (actionValue.isActionValueUnknown()) { + // unused: stringValue = "?"; - this.setToolTipText("Action label or module name for transition from state " + (row) + " to " + (row + 1) + " (not yet known)"); + this.setToolTipText("Action label or module name for transition from state " + (row - 1) + " to " + (row) + " (not yet known)"); } else { stringValue = actionValue.getValue(); - this.setToolTipText("Action label or module name for transition from state " + (row) + " to " + (row + 1)); + String tooltip; + if (row == 0) { + tooltip = null; + } else { + tooltip = "Action label or module name for transition from state " + (row - 1) + " to " + (row); + } + this.setToolTipText(tooltip); } } else if (value instanceof GUISimulator.TimeValue)