From 708f090ea55ed1ef5a9216d99bdd074cf810f022 Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Fri, 19 Oct 2007 14:01:25 +0000 Subject: [PATCH] Changed simulator to remember the view whenever possible git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@466 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../userinterface/simulator/GUISimulator.java | 231 ++++++++++++------ .../simulator/GUIViewDialog.form | 5 +- .../simulator/GUIViewDialog.java | 3 +- 3 files changed, 164 insertions(+), 75 deletions(-) diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index f2b9b356..8e5fa1cf 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -73,6 +73,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect private boolean displayStyleFast; private boolean displayPathLoops; + private SimulationView view; //Actions private Action backtrackToHere, removeToHere, newPath, resetPath, exportPath, configureView; @@ -84,7 +85,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect this.gui = gui; this.engine = gui.getPrism().getSimulator(); - SimulationView view = new SimulationView(); + view = new SimulationView(); pathTableModel = new PathTableModel(view); updateTableModel = new UpdateTableModel(); @@ -277,6 +278,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect engineBuilt = false; } pathActive = false; + pathTableModel.restartPathTable(); updateTableModel.restartUpdatesTable(); @@ -358,62 +360,66 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect Values defaultInitialState = new Values(); defaultInitialState.addValues(parsedModel.getInitialValues()); - // if required, we prompt the user for an initial state - if(isAskForInitialState()) + boolean modelChanged = false; + + // we will pass in lastInitialState to the dialog + // but first make sure it is ok, i.e. + // (a) it is non-null + if(lastInitialState == null) { + lastInitialState = defaultInitialState; + modelChanged = true; + } + // (b) var names/types are correct + else { - // we will pass in lastInitialState to the dialog - // but first make sure it is ok, i.e. - // (a) it is non-null - if(lastInitialState == null) { - lastInitialState = defaultInitialState; + boolean match = true; + int i, n; + n = defaultInitialState.getNumValues(); + if (lastInitialState.getNumValues() != defaultInitialState.getNumValues()) + { + match = false; } - // (b) var names/types are correct else { - boolean match = true; - int i, n; - n = defaultInitialState.getNumValues(); - if (lastInitialState.getNumValues() != defaultInitialState.getNumValues()) - { - match = false; - } - else + for(i = 0; i < n; i++) { - for(i = 0; i < n; i++) + if(!lastInitialState.contains(defaultInitialState.getName(i))) { - if(!lastInitialState.contains(defaultInitialState.getName(i))) + match = false; + break; + } + else + { + int index = lastInitialState.getIndexOf(defaultInitialState.getName(i)); + if(lastInitialState.getType(index) != defaultInitialState.getType(i)) { match = false; break; } - else - { - int index = lastInitialState.getIndexOf(defaultInitialState.getName(i)); - if(lastInitialState.getType(index) != defaultInitialState.getType(i)) - { - match = false; - break; - } - } } } - if(!match) // if there's a problem, just use the default - { - lastInitialState = defaultInitialState; - } } - + if(!match) // if there's a problem, just use the default + { + lastInitialState = defaultInitialState; + modelChanged = true; + } + } + + // if required, we prompt the user for an initial state + if(isAskForInitialState()) + { initialState = GUIInitialStatePicker.defineInitalValuesWithDialog(getGUI(), lastInitialState, parsedModel); // if user clicked cancel from dialog... + if (initialState == null) { return; } } - // if we don't need to ask the user at all, just use the default else { - initialState = defaultInitialState; - } + initialState = lastInitialState; + } displayPathLoops = true; engine.startNewPath(parsedModel, pf, initialState); @@ -427,7 +433,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect definedConstantsLabel.setText((uCon.getDefinedConstantsString().length() == 0) ? "None" : uCon.getDefinedConstantsString()); doEnables(); + pathTableModel.restartPathTable(); + updateTableModel.restartUpdatesTable(); pathTable.getSelectionModel().setSelectionInterval(pathTable.getRowCount()-1, pathTable.getRowCount()-1); @@ -2622,54 +2630,139 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public void refreshToDefaultView() { - visibleVariables.clear(); - hiddenVariables.clear(); - visibleRewardColumns.clear(); + // First see if we can get away with using current settings... + boolean canUseCurrentView = true; - rewards.clear(); - - useChangeRenderer = (gui.getPrism().getSettings().getInteger(PrismSettings.SIMULATOR_RENDER_ALL_VALUES) == 0); - - if (useChangeRenderer != usingChangeRenderer()) - { - GUISimulator.this.setRenderer(useChangeRenderer); - } - - if (pathActive) + if (!pathActive) + canUseCurrentView = false; + else { + // Time-wise we have a problem. + if (parsedModel.getType() != ModulesFile.STOCHASTIC && (showTime || showCumulativeTime)) + canUseCurrentView = false; + try - { - stepsVisible = true; - showTime = false; - showCumulativeTime = parsedModel.getType() == ModulesFile.STOCHASTIC; + { + // Make a set of all variable names. + TreeSet allVarNames = new TreeSet(); + + for (Object var : visibleVariables) + allVarNames.add(((Variable)var).getName()); + for (Object var : hiddenVariables) + allVarNames.add(((Variable)var).getName()); for (int i = 0; i < engine.getNumVariables(); i++) { - visibleVariables.add(new Variable(i, engine.getVariableName(i), engine.getVariableType(i))); + if (allVarNames.contains(engine.getVariableName(i))) + allVarNames.remove(engine.getVariableName(i)); + else + // Cannot use current view if a variable is not there. + canUseCurrentView = false; } - + + // Cannot use current view if we have too many variables. + if (allVarNames.size() > 0) + canUseCurrentView = false; + + // Make a list of all reward structures + ArrayList allrew = new ArrayList(); + + for (Object rew : rewards) + { + allrew.add((RewardStructure)rew); + } + for (int r = 0; r < parsedModel.getNumRewardStructs(); r++) { parser.RewardStruct rewardStruct = parsedModel.getRewardStruct(r); String rewardName = rewardStruct.getName(); - if (rewardName.trim().length() == 0) - { rewardName = null; } + boolean hasStates = parsedModel.getRewardStruct(r).getNumStateItems() != 0; + boolean hasTrans = parsedModel.getRewardStruct(r).getNumTransItems() != 0; - RewardStructure rewardStructure = new RewardStructure(r, rewardName, parsedModel.getRewardStruct(r).getNumStateItems() == 0, parsedModel.getRewardStruct(r).getNumTransItems() == 0); + boolean foundReward = false; - if (!rewardStructure.isStateEmpty() || !rewardStructure.isTransitionEmpty()) - rewards.add(rewardStructure); + for (Object rewobj : rewards) + { + RewardStructure rew = (RewardStructure)rewobj; + + if (rew.isStateEmpty() == !hasStates && rew.isTransitionEmpty() == !hasTrans && (rew.getName() == null && rewardName.equals("") || rew.getName().equals(rewardName))) + { + allrew.remove(rew); + foundReward = true; + } + } - if (!rewardStructure.isStateEmpty()) - visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, RewardStructureColumn.STATE_REWARD)); + if (!foundReward) + canUseCurrentView = false; + } + + if (allrew.size() > 0) + canUseCurrentView = false; - if (!rewardStructure.isTransitionEmpty()) - visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, RewardStructureColumn.TRANSITION_REWARD)); - } } - catch (SimulatorException e) {} - } + catch (SimulatorException e) + { + canUseCurrentView = false; + } + } + + if (!canUseCurrentView) + { + visibleVariables.clear(); + hiddenVariables.clear(); + visibleRewardColumns.clear(); + + rewards.clear(); + + useChangeRenderer = (gui.getPrism().getSettings().getInteger(PrismSettings.SIMULATOR_RENDER_ALL_VALUES) == 0); + + if (useChangeRenderer != usingChangeRenderer()) + { + GUISimulator.this.setRenderer(useChangeRenderer); + } + + if (pathActive) + { + try + { + stepsVisible = true; + showTime = false; + showCumulativeTime = parsedModel.getType() == ModulesFile.STOCHASTIC; + + for (int i = 0; i < engine.getNumVariables(); i++) + { + visibleVariables.add(new Variable(i, engine.getVariableName(i), engine.getVariableType(i))); + } + + for (int r = 0; r < parsedModel.getNumRewardStructs(); r++) + { + parser.RewardStruct rewardStruct = parsedModel.getRewardStruct(r); + String rewardName = rewardStruct.getName(); + + if (rewardName.trim().length() == 0) + { rewardName = null; } + + RewardStructure rewardStructure = new RewardStructure(r, rewardName, parsedModel.getRewardStruct(r).getNumStateItems() == 0, parsedModel.getRewardStruct(r).getNumTransItems() == 0); + + if (!rewardStructure.isStateEmpty() || !rewardStructure.isTransitionEmpty()) + rewards.add(rewardStructure); + + if (!rewardStructure.isStateEmpty()) + visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, RewardStructureColumn.STATE_REWARD)); + + if (!rewardStructure.isTransitionEmpty()) + visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, RewardStructureColumn.TRANSITION_REWARD)); + } + + System.out.println("REFRESHED VIEW " + visibleVariables.size()); + + } + catch (SimulatorException e) {} + } + } + else + System.out.println("REUSED VIEW"); this.setChanged(); this.notifyObservers(); @@ -3205,8 +3298,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect * The structure of the path may be for a different model etc. */ public void restartPathTable() - { - view.refreshToDefaultView(); + { + view.refreshToDefaultView(); } /** diff --git a/prism/src/userinterface/simulator/GUIViewDialog.form b/prism/src/userinterface/simulator/GUIViewDialog.form index 3e237cea..2b13481c 100644 --- a/prism/src/userinterface/simulator/GUIViewDialog.form +++ b/prism/src/userinterface/simulator/GUIViewDialog.form @@ -571,9 +571,6 @@ - - - @@ -600,7 +597,7 @@ - + diff --git a/prism/src/userinterface/simulator/GUIViewDialog.java b/prism/src/userinterface/simulator/GUIViewDialog.java index bd8ec5d2..47ebc5b9 100644 --- a/prism/src/userinterface/simulator/GUIViewDialog.java +++ b/prism/src/userinterface/simulator/GUIViewDialog.java @@ -537,7 +537,7 @@ public class GUIViewDialog extends JDialog implements KeyListener topInnerTimePanel.setLayout(new java.awt.GridLayout(2, 1, 5, 5)); topInnerTimePanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); - showTimeCheckBox.setText("Show the time spend in states"); + showTimeCheckBox.setText("Show the time spent in states"); showTimeCheckBox.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); showTimeCheckBox.setMargin(new java.awt.Insets(0, 0, 0, 0)); topInnerTimePanel.add(showTimeCheckBox); @@ -551,7 +551,6 @@ public class GUIViewDialog extends JDialog implements KeyListener innerTimePanel.add(topInnerTimePanel, java.awt.BorderLayout.NORTH); boxPanel.add(innerTimePanel); - innerTimePanel.getAccessibleContext().setAccessibleName("Time properties"); pathStylePanel.setLayout(new java.awt.BorderLayout());