From c28f11a31d90661e20961ea2c906af0c0e88229d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 30 Apr 2010 09:07:19 +0000 Subject: [PATCH] Further improvements to the simulator. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1860 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/Values.java | 1 + prism/src/parser/ast/ModulesFile.java | 23 +- prism/src/parser/visitor/Simplify.java | 6 + prism/src/simulator/SimulatorEngine.java | 432 +++++++++++++----- .../simulator/GUISimLabelFormulaeList.java | 233 ---------- .../simulator/GUISimLabelList.java | 294 ++++++++++++ .../userinterface/simulator/GUISimulator.java | 254 +++++----- 7 files changed, 748 insertions(+), 495 deletions(-) delete mode 100644 prism/src/userinterface/simulator/GUISimLabelFormulaeList.java create mode 100644 prism/src/userinterface/simulator/GUISimLabelList.java diff --git a/prism/src/parser/Values.java b/prism/src/parser/Values.java index 90f7997d..419df8f7 100644 --- a/prism/src/parser/Values.java +++ b/prism/src/parser/Values.java @@ -53,6 +53,7 @@ public class Values //implements Comparable /** * Construct a new Values object by copying an existing one */ + @SuppressWarnings("unchecked") public Values(Values v) { names = (ArrayList)v.names.clone(); diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index cf2893e3..caf589a2 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -851,10 +851,17 @@ public class ModulesFile extends ASTElement /** * Perform a deep copy. */ + @SuppressWarnings("unchecked") public ASTElement deepCopy() { int i, n; ModulesFile ret = new ModulesFile(); + + // Copy ASTElement stuff + ret.setPosition(this); + // Copy type + ret.setModelType(modelType); + // Deep copy main components ret.setFormulaList((FormulaList) formulaList.deepCopy()); ret.setLabelList((LabelList) labelList.deepCopy()); ret.setConstantList((ConstantList) constantList.deepCopy()); @@ -874,7 +881,21 @@ public class ModulesFile extends ASTElement } if (initStates != null) ret.setInitialStates(initStates.deepCopy()); - ret.setPosition(this); + // Copy other (generated) info + ret.formulaIdents = (formulaIdents == null) ? null : (Vector)formulaIdents.clone(); + ret.constantIdents = (constantIdents == null) ? null : (Vector)constantIdents.clone(); + ret.varIdents = (varIdents == null) ? null : (Vector)varIdents.clone(); + ret.moduleNames = (moduleNames == null) ? null : moduleNames.clone(); + ret.synchs = (synchs == null) ? null : (Vector)synchs.clone(); + if (varDecls != null) { + ret.varDecls = new Vector(); + for (Declaration d : varDecls) + ret.varDecls.add((Declaration) d.deepCopy()); + } + ret.varNames = (varNames == null) ? null : (Vector)varNames.clone(); + ret.varTypes = (varTypes == null) ? null : (Vector)varTypes.clone(); + ret.constantValues = (constantValues == null) ? null : new Values(constantValues); + return ret; } } diff --git a/prism/src/parser/visitor/Simplify.java b/prism/src/parser/visitor/Simplify.java index ecdabb52..e8fe8dc8 100644 --- a/prism/src/parser/visitor/Simplify.java +++ b/prism/src/parser/visitor/Simplify.java @@ -173,4 +173,10 @@ public class Simplify extends ASTTraverseModify } return e; } + + public Object visit(ExpressionFormula e) throws PrismLangException + { + // If formula has an attached definition, just replace it with that + return e.getDefinition() != null ? e.getDefinition() : e; + } } diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 1130c842..2177b3ac 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -161,9 +161,6 @@ public class SimulatorEngine protected Prism prism; protected PrismLog mainLog; - // Random number generator - private RandomNumberGenerator rng; - // The current parsed model + info private ModulesFile modulesFile; private ModelType modelType; @@ -174,12 +171,22 @@ public class SimulatorEngine private Vector synchs; private int numSynchs; + // Properties info + private PropertiesFile propertiesFile; + private List pathProps; + private Values propertyConstants; + private ArrayList loadedProperties; + + // Updater object for model + protected Updater updater; + protected TransitionList transitionList; + // Random number generator + private RandomNumberGenerator rng; + // TODO: ... more from below // NEW STUFF: protected boolean onTheFly; - // Updater object for model - protected Updater updater; protected State lastState; protected State currentState; @@ -189,7 +196,6 @@ public class SimulatorEngine protected Path path = null; // TRANSITIONS: - protected TransitionList transitionList; protected List labels; @@ -228,12 +234,6 @@ public class SimulatorEngine */ public static final double UNDEFINED_DOUBLE = -10E23f; - // Infinity - /** - * Used by the simulator engine, usually for infinite rewards. etc... - */ - public static final double INFINITY = 10E23f; - // ------------------------------------------------------------------------------ // CLASS MEMBERS // ------------------------------------------------------------------------------ @@ -243,12 +243,6 @@ public class SimulatorEngine // Current model private Values constants; - // PRISM parsed properties files - private PropertiesFile propertiesFile; - - // Current Properties - private Values propertyConstants; - private ArrayList loadedProperties; // ------------------------------------------------------------------------------ // Basic setup @@ -261,7 +255,7 @@ public class SimulatorEngine { this.prism = prism; setMainLog(prism.getMainLog()); - // TODO + // TODO: finish this code once class members finalised rng = new RandomNumberGenerator(); varIndices = null; modulesFile = null; @@ -559,6 +553,107 @@ public class SimulatorEngine updater.calculateTransitions(currentState, transitionList); } + // ------------------------------------------------------------------------------ + // Methods for adding/querying labels and properties + // ------------------------------------------------------------------------------ + + /** + * Add a label to the simulator, whose value will be computed during path generation. + * The resulting index of the label is returned: this is used for later queries about the property. + * Any constants/formulas etc. appearing in the label must have been defined in the current model. + * If there are additional constants (e.g. from a properties file), + * then use the {@link #addLabel(Expression, PropertiesFile)} method. + */ + public int addLabel(Expression label) throws PrismLangException + { + // Take a copy, get rid of any constants and simplify + Expression labelNew = label.deepCopy(); + labelNew = (Expression) labelNew.replaceConstants(constants); + labelNew = (Expression) labelNew.simplify(); + labels.add(labelNew); + return labels.size() - 1; + } + + /** + * Add a label to the simulator, whose value will be computed during path generation. + * The resulting index of the label is returned: this is used for later queries about the property. + * Any constants/formulas etc. appearing in the label must have been defined in the current model + * or be supplied in the (optional) passed in PropertiesFile. + */ + public int addLabel(Expression label, PropertiesFile pf) throws PrismLangException + { + // Take a copy, get rid of any constants and simplify + Expression labelNew = label.deepCopy(); + labelNew = (Expression) labelNew.replaceConstants(constants); + labelNew = (Expression) labelNew.replaceConstants(pf.getConstantValues()); + labelNew = (Expression) labelNew.simplify(); + labels.add(labelNew); + return labels.size() - 1; + } + + /** + * Add a (path) property to the simulator, whose value will be computed during path generation. + * The resulting index of the property is returned: this is used for later queries about the property. + */ + private int addProperty(Expression prop) + { + // clone, converttountil, simplify ??? + + // TODO + return -1; + } + + /** + * Get the current value of a previously added label (specified by its index). + */ + public boolean queryLabel(int index) throws PrismLangException + { + return labels.get(index).evaluateBoolean(currentState); + } + + /** + * Get the value, at the specified path step, of a previously added label (specified by its index). + */ + public boolean queryLabel(int index, int step) throws PrismLangException + { + return labels.get(index).evaluateBoolean(path.getState(step)); + } + + /** + * Check whether the current state is an initial state. + */ + public boolean queryIsInitial() throws PrismLangException + { + // Currently init...endinit is not supported so this is easy to check + return currentState.equals(new State(modulesFile.getInitialValues())); + } + + /** + * Check whether a particular step in the current path is an initial state. + */ + public boolean queryIsInitial(int step) throws PrismLangException + { + // Currently init...endinit is not supported so this is easy to check + return path.getState(step).equals(new State(modulesFile.getInitialValues())); + } + + /** + * Check whether the current state is a deadlock. + */ + public boolean queryIsDeadlock() throws PrismLangException + { + return transitionList.getNumChoices() == 0; + } + + /** + * Check whether a particular step in the current path is a deadlock. + */ + public boolean queryIsDeadlock(int step) throws PrismLangException + { + // By definition, earlier states in the path cannot be deadlocks + return step == path.size() ? queryIsDeadlock() : false; + } + // ------------------------------------------------------------------------------ // Private methods for path creation and modification // ------------------------------------------------------------------------------ @@ -594,9 +689,10 @@ public class SimulatorEngine synchs = modulesFile.getSynchs(); numSynchs = synchs.size(); - // Evaluate constants and optimise modules file for simulation - modulesFile = (ModulesFile) modulesFile.replaceConstants(constants).simplify(); - + // Evaluate constants and optimise (a copy of) modules file for simulation + modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(constants).simplify(); + mainLog.println(modulesFile); + // Create state/transition storage lastState = new State(numVars); currentState = new State(numVars); @@ -1036,11 +1132,6 @@ public class SimulatorEngine // PROPERTIES AND SAMPLING (not yet sorted) // ------------------------------------------------------------------------------ - /** - * Allocate space for storage of sampling information - */ - private static native int allocateSampling(); - /** * Provides access to the propertyConstants * @@ -1131,9 +1222,16 @@ public class SimulatorEngine } /** - * This method completely encapsulates the model checking of multiple properties prerequisites modulesFile constants - * should all be defined propertiesFile constants should all be defined - * + * Perform approximate model checking of properties on a model, using the simulator. + * Note: All constants in the model/property files must have already been defined. + * @param modulesFile Model for simulation, constants defined + * @param propertiesFile Properties file containing property to check, constants defined + * @param exprs The properties to check + * @param initialState + * The initial state for the sampling. + * @param noIterations The number of iterations (i.e. number of samples to generate) + * @param maxPathLength The maximum path length for sampling + * *

* The returned result is an array each item of which is either: *

    @@ -1141,24 +1239,9 @@ public class SimulatorEngine *
  • An exception if there was a problem *
* - * @param modulesFile - * The ModulesFile, constants already defined. - * @param propertiesFile - * The PropertiesFile containing the property of interest, constants defined. - * @param exprs - * The properties of interest - * @param initialState - * The initial state for the sampling. - * @param noIterations - * The number of iterations for the sampling algorithm - * @param maxPathLength - * the maximum path length for the sampling algorithm. - * @throws PrismException - * if anything goes wrong. - * @return the result. */ public Object[] modelCheckMultipleProperties(ModulesFile modulesFile, PropertiesFile propertiesFile, - ArrayList exprs, Values initialState, int noIterations, int maxPathLength) + List exprs, Values initialState, int noIterations, int maxPathLength) throws PrismException { createNewOnTheFlyPath(modulesFile, propertiesFile); @@ -1185,7 +1268,7 @@ public class SimulatorEngine // as long as there are at least some valid props, do sampling if (validPropsCount > 0) { initialisePath(initialState); - int result = doSampling(noIterations, maxPathLength); + int result = 0;//doSampling(noIterations, maxPathLength); if (result == ERROR) { throw new PrismException(getLastErrorMessage()); } @@ -1277,7 +1360,7 @@ public class SimulatorEngine // as long as there are at least some valid props, do sampling if (validPropsCount > 0) { initialisePath(initialState); - int result = doSampling(noIterations, maxPathLength); + int result = 0;//doSampling(noIterations, maxPathLength); if (result == ERROR) { throw new PrismException(getLastErrorMessage()); } @@ -1303,17 +1386,201 @@ public class SimulatorEngine } } - /** - * Returns the index of the property, if it can be added, -1 if nots - */ - private int addProperty(Expression prop) + /* + private int doSampling(State initialState, int numIters, int maxPathLength) + { + int iteration_counter = 0; + int last_percentage_done = -1; + int percentage_done = -1; + double average_path_length = 0; + int min_path_length = 0, max_path_length = 0; + boolean stopped_early = false; + boolean deadlocks_found = false; + //The current path + int current_index; + + //double* path_cost = new double[no_reward_structs]; + //double* total_state_cost = new double[no_reward_structs]; + //double* total_transition_cost = new double[no_reward_structs]; + + // Timing info + long start, start2, stop; + double time_taken; + + //Loop detection requires that deterministic paths are + //stored, until that determinism is broken. This path + //is allocated dynamically, 10 steps at a time. + //CSamplingLoopDetectionHandler* loop_detection = new CSamplingLoopDetectionHandler(); + + //TODO: allow stopping of sampling mid-way through? + //External flag set to false + boolean should_stop_sampling = false; + + start = start2 = System.currentTimeMillis(); + + mainLog.print("\nSampling progress: ["); + mainLog.flush(); + + //The loop continues until each pctl/csl formula is satisfied: + //E.g. usually, this is when the correct number of iterations + //has been performed, but for some, such as cumulative rewards + //this can be early if a loop is detected at any point, this + //is all handled by the All_Done_Sampling() function + + // Main sampling loop + while (!should_stop_sampling && !isSamplingDone()) { + + // Display progress + percentage_done = ((10*(iteration_counter))/numIters)*10; + if (percentage_done > last_percentage_done) { + last_percentage_done = percentage_done; + //cout << " " << last_percentage_done << "%" << endl; + mainLog.print(" " + last_percentage_done + "%"); + mainLog.flush(); + } + + //do polling and feedback every 2 seconds + stop = System.currentTimeMillis(); + if (stop - start2 > 2000) { + //Write_Feedback(iteration_counter, numIters, false); + //int poll = Poll_Control_File(); + //if(poll & STOP_SAMPLING == STOP_SAMPLING) + // should_stop_sampling = true; + start2 = System.currentTimeMillis(); + } + + iteration_counter++; + + // Start the new path for this iteration (sample) + initialisePath(initialState); + + //loop_detection->Reset(); + + + notifyPathFormulae(last_state, state_variables, loop_detection); + + // Generate a path, up to at most maxPathLength steps + for (current_index = 0; + !All_PCTL_Answers_Known(loop_detection) && //not got answers for all properties yet + //!loop_detection->Is_Proven_Looping() //not looping (removed this - e.g. cumul rewards can't stop yet) + current_index < path_length; //not exceeding path_length + current_index++) + { + // Make a random transition + automaticChoice(detect); + + //if(!loop_detection->Is_Proven_Looping()) { // removed this: for e.g. cumul rewards need to keep counting in loops... + + if (modelType.continuousTime()) { + double time_in_state = Get_Sampled_Time(); + + last_state->time_spent_in_state = time_in_state; + + for (int i = 0; i < no_reward_structs; i++) { + last_state->state_cost[i] = last_state->state_instant_cost[i]*time_in_state; + last_state->transition_cost[i] = Get_Transition_Reward(i); + total_state_cost[i] += last_state->state_instant_cost[i]*time_in_state; + total_transition_cost[i] += last_state->transition_cost[i]; + path_cost[i] = total_state_cost[i] + total_transition_cost[i]; + + last_state->cumulative_state_cost[i] = total_state_cost[i]; + last_state->cumulative_transition_cost[i] = total_transition_cost[i]; + } + + Notify_Path_Formulae(last_state, state_variables, loop_detection); + } + else + { + for (int i = 0; i < no_reward_structs; i++) { + last_state->state_cost[i] = last_state->state_instant_cost[i]; + last_state->transition_cost[i] = Get_Transition_Reward(i); + total_state_cost[i] += last_state->state_instant_cost[i]; + total_transition_cost[i] += last_state->transition_cost[i]; + path_cost[i] = total_state_cost[i] + total_transition_cost[i]; + + last_state->cumulative_state_cost[i] = total_state_cost[i]; + last_state->cumulative_transition_cost[i] = total_transition_cost[i]; + } + + Notify_Path_Formulae(last_state, state_variables, loop_detection); + } + //} + + } + + // record if we found any deadlocks (can check this outside path gen loop because never escape deadlocks) + if (loop_detection->Is_Deadlock()) deadlocks_found = true; + + // compute path length statistics so far + average_path_length = (average_path_length*(iteration_counter-1)+(current_index))/iteration_counter; + min_path_length = (iteration_counter == 1) ? current_index : ((current_index < min_path_length) ? current_index : min_path_length); + max_path_length = (iteration_counter == 1) ? current_index : ((current_index > max_path_length) ? current_index : max_path_length); + + //Get samples and notify sample collectors + Do_A_Sample(loop_detection); + + // stop early if any of the properties couldn't be sampled + if (Get_Total_Num_Reached_Max_Path() > 0) { stopped_early = true; break; } + + }//end sampling while + + if (!stopped_early) { + if (!should_stop_sampling) + mainLog.print(" 100% ]"); + mainLog.println(); + stop = System.currentTimeMillis(); + time_taken = (stop - start) / 1000.0; + mainLog.print("\nSampling complete: "); + mainLog.print(iteration_counter + " iterations in " + time_taken + " seconds (average " + time_taken/iteration_counter + ")\n"); + mainLog.print("Path length statistics: average " + average_path_length + ", min " + min_path_length + ", max " + max_path_length + "\n"); + } else { + mainLog.print(" ...\n\nSampling terminated early after " + iteration_counter + " iterations.\n"); + } + + // print a warning if deadlocks occurred at any point + if (deadlocks_found) + mainLog.print("\nWarning: Deadlocks were found during simulation: self-loops were added\n"); + + // print a warning if simulation was stopped by the user + if (should_stop_sampling) + mainLog.print("\nWarning: Simulation was terminated before completion.\n"); + + //write to feedback file with true to indicate that we have finished sampling + Write_Feedback(iteration_counter, numIters, true); + + //Print_Sampling_Results(); + delete loop_detection; + delete[] starting_variables; + delete last_state; + delete[] path_cost; + delete[] total_state_cost; + delete[] total_transition_cost; + + if (stopped_early) { + Report_Error("One or more of the properties being sampled could not be checked on a sample. Consider increasing the maximum path length"); + throw 0; + } + + + // TODO: + return -1; + }*/ + + private void notifyPathFormulae() + { + /*for(int i = 0; i< no_path_formulae; i++) + { + if(!registered_path_formulae[i]->Is_Answer_Known(loop_detection)) + registered_path_formulae[i]->Notify_State(last_state, current_state); + }*/ + } + + private boolean isSamplingDone() { // TODO - return -1; + return false; } - - private static native int doSampling(int noIterations, int maxPathLength); - + private static native double getSamplingResult(int propertyIndex); private static native int getNumReachedMaxPath(int propertyIndex); @@ -1407,59 +1674,6 @@ public class SimulatorEngine } } - // ------------------------------------------------------------------------------ - // STATE PROPOSITION METHODS - // ------------------------------------------------------------------------------ - - public int addLabel(Expression label) - { - labels.add(label); - return labels.size() - 1; - } - - public boolean queryLabel(int index) throws PrismLangException - { - return labels.get(index).evaluateBoolean(currentState); - } - - public boolean queryLabel(int index, int step) throws PrismLangException - { - return labels.get(index).evaluateBoolean(path.getState(step)); - } - - /** - * For the current state, this returns 1 if it is the same as the initial state for the current path - */ - public int queryIsInitial() - { - return 0; // TODO - } - - /** - * For the state at the given index, this returns 1 if it is the same as the initial state for the current path - */ - public int queryIsInitial(int step) - { - return 0; // TODO - } - - /** - * For the current state, this returns 1 if it is a deadlock state. - */ - // TODO - public int queryIsDeadlock() - { - return 0; - } - - /** - * For the state at the given index, this returns 1 if it is a deadlock state. - */ - public int queryIsDeadlock(int step) - { - return 0; // TODO - } - // ------------------------------------------------------------------------------ // PATH FORMULA METHODS // ------------------------------------------------------------------------------ diff --git a/prism/src/userinterface/simulator/GUISimLabelFormulaeList.java b/prism/src/userinterface/simulator/GUISimLabelFormulaeList.java deleted file mode 100644 index b62064c8..00000000 --- a/prism/src/userinterface/simulator/GUISimLabelFormulaeList.java +++ /dev/null @@ -1,233 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Andrew Hinton (University of Birmingham) -// * Dave Parker (University of Oxford, formerly University of Birmingham) -// -//------------------------------------------------------------------------------ -// -// This file is part of PRISM. -// -// PRISM is free software; you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// PRISM is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. -// -// You should have received a copy of the GNU General Public License -// along with PRISM; if not, write to the Free Software Foundation, -// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -// -//============================================================================== - -package userinterface.simulator; - -import java.awt.*; -import javax.swing.*; - -import parser.ast.*; -import prism.PrismLangException; -import userinterface.properties.*; -import simulator.*; - -/** - * - * @author ug60axh - */ -public class GUISimLabelFormulaeList extends JList -{ - private static final Color background = new Color(202, 225, 255); - private GUISimulator sim; - private SimulatorEngine engine; - private DefaultListModel listModel; - - /** Creates a new instance of GUISimLabelFormulaeList */ - public GUISimLabelFormulaeList(GUISimulator sim) - { - this.sim = sim; - this.engine = sim.getPrism().getSimulator(); - listModel = new DefaultListModel(); - setModel(listModel); - - setCellRenderer(new SimLabelRenderer()); - } - - public void addLabel(String name, Expression expr, ModulesFile mf) - { - int index = engine.addLabel(expr); - SimLabel sl = new SimLabel(name, index); - listModel.addElement(sl); - } - - public void addDeadlockAndInit() - { - listModel.addElement(new InitSimLabel()); - listModel.addElement(new DeadlockSimLabel()); - } - - public void clearLabels() - { - listModel.clear(); - } - - class SimLabel - { - String formula; - int formulaIndex; - - public SimLabel(String formula, int formulaIndex) - { - this.formula = formula; - this.formulaIndex = formulaIndex; - } - - public String toString() - { - return formula; - } - - public int getResult() - { - try { - boolean b = engine.queryLabel(formulaIndex); - return b ? 1 : 0; - } catch (PrismLangException e) { - return -1; - } - } - - public int getResult(int step) - { - try { - boolean b = engine.queryLabel(formulaIndex, step); - return b ? 1 : 0; - } catch (PrismLangException e) { - return -1; - } - } - } - - class InitSimLabel extends SimLabel - { - public InitSimLabel() - { - super("init", 0); - } - - public int getResult() - { - return engine.queryIsInitial(); - } - - public int getResult(int step) - { - return engine.queryIsInitial(step); - } - } - - class DeadlockSimLabel extends SimLabel - { - public DeadlockSimLabel() - { - super("deadlock", 0); - } - - public int getResult() - { - return engine.queryIsDeadlock(); - } - - public int getResult(int step) - { - return engine.queryIsDeadlock(step); - } - } - - //RENDERERS - - class SimLabelRenderer extends JLabel implements ListCellRenderer - { - String lastText; - - public SimLabelRenderer() - { - setOpaque(true); - lastText = "Unknown"; - } - - public String getToolTipText() - { - return lastText; - } - - public Component getListCellRendererComponent(JList list, Object value, int index, boolean isSelected, - boolean cellHasFocus) - { - setBorder(new BottomBorder()); - SimLabel l = (SimLabel) value; - - setText(l.toString()); - if (!sim.isOldUpdate()) { - - if (l.getResult() == 1) { - lastText = "True"; - setIcon(GUIProperty.IMAGE_TICK); - } else if (l.getResult() == 0) { - lastText = "False"; - setIcon(GUIProperty.IMAGE_CROSS); - } else { - lastText = "Unknown"; - setIcon(GUIProperty.IMAGE_NOT_DONE); - } - } else { - if (l.getResult(sim.getOldUpdateStep()) == 1) { - lastText = "True"; - setIcon(GUIProperty.IMAGE_TICK); - } else if (l.getResult(sim.getOldUpdateStep()) == 0) { - lastText = "False"; - setIcon(GUIProperty.IMAGE_CROSS); - } else { - lastText = "Unknown"; - setIcon(GUIProperty.IMAGE_NOT_DONE); - } - } - - if (isSelected) { - setBackground(background); - - } else { - setBackground(Color.white); - } - - repaint(); - return this; - } - - } - - class BottomBorder implements javax.swing.border.Border - { - public Insets getBorderInsets(Component c) - { - return new Insets(0, 0, 0, 0); - } - - public boolean isBorderOpaque() - { - return true; - } - - public void paintBorder(Component c, Graphics g, int x, int y, int width, int height) - { - g.setColor(Color.lightGray); - g.drawLine(x, (y + height - 1), (x + width), (y + height - 1)); - - } - } - -} diff --git a/prism/src/userinterface/simulator/GUISimLabelList.java b/prism/src/userinterface/simulator/GUISimLabelList.java new file mode 100644 index 00000000..b41a09d6 --- /dev/null +++ b/prism/src/userinterface/simulator/GUISimLabelList.java @@ -0,0 +1,294 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Andrew Hinton (University of Birmingham) +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package userinterface.simulator; + +import java.awt.*; +import javax.swing.*; + +import parser.ast.*; +import prism.PrismLangException; +import userinterface.properties.*; +import simulator.*; + +/** + * List of labels in the simulator GUI. + */ +public class GUISimLabelList extends JList +{ + // Default serial ID + private static final long serialVersionUID = 1L; + // Background colour of selected list items + private static final Color background = new Color(202, 225, 255); + // Pointers to simulator and GUI + private GUISimulator sim; + private SimulatorEngine engine; + // The list of labels + private DefaultListModel listModel; + + /** + * Create a new instance of GUISimLabelList + */ + public GUISimLabelList(GUISimulator sim) + { + this.sim = sim; + this.engine = sim.getPrism().getSimulator(); + listModel = new DefaultListModel(); + setModel(listModel); + setCellRenderer(new SimLabelRenderer()); + } + + /** + * Clear the list of labels. + */ + public void clearLabels() + { + listModel.clear(); + } + + /** + * Add a (model file) label to the list. + * Any required formulas/labels will be in the associated model, already in the simulator. + */ + public void addModelLabel(String name, Expression expr) + { + try { + int index = engine.addLabel(expr); + SimLabel sl = new SimLabel(name, index); + listModel.addElement(sl); + } + catch (PrismLangException e) { + // Silently ignore any problems - just don't add label to list + } + } + + /** + * Add a (properties file) label to the list. + * The associated properties file is also (optionally) passed in so that + * any required formulas/labels (not in the model file) can be obtained. + */ + public void addPropertyLabel(String name, Expression expr, PropertiesFile pf) + { + try { + int index = engine.addLabel(expr, pf); + SimLabel sl = new SimLabel(name, index); + listModel.addElement(sl); + } + catch (PrismLangException e) { + // Silently ignore any problems - just don't add label to list + } + } + + /** + * Add the special deadlock/init labels to the list. + */ + public void addDeadlockAndInit() + { + listModel.addElement(new InitSimLabel()); + listModel.addElement(new DeadlockSimLabel()); + } + + /** + * Class to store a normal label, that has been loaded into the simulator. + */ + class SimLabel + { + // Label name + private String name; + // Index of the label in the simulator engine + private int index; + + public SimLabel(String name, int index) + { + this.name = name; + this.index = index; + } + + public String toString() + { + return name; + } + + /** + * Get the value of the label in the current state of the simulator. + * 1 denotes true, 0 false, and -1 error/unknown + */ + public int getResult() + { + try { + boolean b = engine.queryLabel(index); + return b ? 1 : 0; + } catch (PrismLangException e) { + return -1; + } + } + + /** + * Get the value of the label in a particular step of the current simulator path. + * 1 denotes true, 0 false, and -1 error/unknown + */ + public int getResult(int step) + { + try { + return engine.queryLabel(index, step) ? 1 : 0; + } catch (PrismLangException e) { + return -1; + } + } + } + + /** + * Class to store the special "init" label. + */ + class InitSimLabel extends SimLabel + { + public InitSimLabel() + { + super("init", 0); + } + + @Override + public int getResult() + { + try { + return engine.queryIsInitial() ? 1 : 0; + } catch (PrismLangException e) { + return -1; + } + } + + @Override + public int getResult(int step) + { + try { + return engine.queryIsInitial(step) ? 1 : 0; + } catch (PrismLangException e) { + return -1; + } + } + } + + /** + * Class to store the special "deadlock" label. + */ + class DeadlockSimLabel extends SimLabel + { + public DeadlockSimLabel() + { + super("deadlock", 0); + } + + @Override + public int getResult() + { + try { + return engine.queryIsDeadlock() ? 1 : 0; + } catch (PrismLangException e) { + return -1; + } + } + + @Override + public int getResult(int step) + { + try { + return engine.queryIsDeadlock(step) ? 1 : 0; + } catch (PrismLangException e) { + return -1; + } + } + } + + // RENDERERS + + class SimLabelRenderer extends JLabel implements ListCellRenderer + { + // Default serial ID + private static final long serialVersionUID = 1L; + // Tooltip text + private String text; + + public SimLabelRenderer() + { + setOpaque(true); + text = "Unknown"; + } + + public String getToolTipText() + { + return text; + } + + public Component getListCellRendererComponent(JList list, Object value, int index, boolean isSelected, boolean cellHasFocus) + { + setBorder(new BottomBorder()); + // Get label + SimLabel l = (SimLabel) value; + setText(l.toString()); + // Extract value of label (either for current state or an earlier path step). + int val = sim.isOldUpdate() ? l.getResult(sim.getOldUpdateStep()) : l.getResult(); + switch (val) { + case 1: + text = "True"; + setIcon(GUIProperty.IMAGE_TICK); + break; + case 0: + text = "False"; + setIcon(GUIProperty.IMAGE_CROSS); + break; + default: + text = "Unknown"; + setIcon(GUIProperty.IMAGE_NOT_DONE); + break; + } + // Set BG colour + setBackground(isSelected ? background : Color.white); + repaint(); + return this; + } + + } + + class BottomBorder implements javax.swing.border.Border + { + public Insets getBorderInsets(Component c) + { + return new Insets(0, 0, 0, 0); + } + + public boolean isBorderOpaque() + { + return true; + } + + public void paintBorder(Component c, Graphics g, int x, int y, int width, int height) + { + g.setColor(Color.lightGray); + g.drawLine(x, (y + height - 1), (x + width), (y + height - 1)); + } + } +} diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index ec1dc502..ee1ced8e 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -73,8 +73,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect private SimulationView view; //Actions - private Action randomExploration, backtrack, backtrackToHere, removeToHere, newPath, resetPath, exportPath, - configureView; + private Action randomExploration, backtrack, backtrackToHere, removeToHere, newPath, resetPath, exportPath, configureView; /** Creates a new instance of GUISimulator */ public GUISimulator(GUIPrism gui) @@ -133,10 +132,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect a_manualUpdate(); currentUpdatesTable.requestFocus(); } else if (e.getClickCount() == 2 && !currentUpdatesTable.isEnabled()) { - GUISimulator.this - .warning( - "Simulation", - "You cannot continue exploration from the state that is current selected.\nSelect the last state in the path table to continue"); + GUISimulator.this.warning("Simulation", + "You cannot continue exploration from the state that is current selected.\nSelect the last state in the path table to continue"); } } }); @@ -162,8 +159,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect lastInitialState = null; tableScroll.setRowHeaderView(((GUISimulatorPathTable) pathTable).getPathLoopIndicator()); - manualUpdateTableScrollPane.setRowHeaderView(((GUISimulatorUpdatesTable) currentUpdatesTable) - .getUpdateRowHeader()); + manualUpdateTableScrollPane.setRowHeaderView(((GUISimulatorUpdatesTable) currentUpdatesTable).getUpdateRowHeader()); tableScroll.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED); stateLabelList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION); @@ -259,7 +255,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathActive = false; pathTableModel.restartPathTable(); - ((GUISimLabelFormulaeList) stateLabelList).clearLabels(); + ((GUISimLabelList) stateLabelList).clearLabels(); ((GUISimPathFormulaeList) pathFormulaeList).clearList(); } @@ -276,7 +272,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect else modelTypeLabel.setText("Unknown"); - ((GUISimLabelFormulaeList) stateLabelList).clearLabels(); + ((GUISimLabelList) stateLabelList).clearLabels(); ((GUISimPathFormulaeList) pathFormulaeList).clearList(); stateLabelList.repaint(); pathFormulaeList.repaint(); @@ -310,18 +306,17 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // get properties constants/labels PropertiesFile pf; try { - pf = getPrism().parsePropertiesString(parsedModel, - guiProp.getConstantsString().toString() + guiProp.getLabelsString()); + pf = getPrism().parsePropertiesString(parsedModel, guiProp.getConstantsString().toString() + guiProp.getLabelsString()); } catch (PrismLangException e) { // ignore properties if they don't parse pf = null; //if any problems } // if necessary, get values for undefined constants from user + // TODO: only get necessary property constants (pf can decide this) UndefinedConstants uCon = new UndefinedConstants(parsedModel, pf); if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) { - int result = GUIConstantsPicker.defineConstantsWithDialog(gui, uCon, lastConstants, - lastPropertyConstants); + int result = GUIConstantsPicker.defineConstantsWithDialog(gui, uCon, lastConstants, lastPropertyConstants); if (result != GUIConstantsPicker.VALUES_DONE) return; } @@ -377,8 +372,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // if required, we prompt the user for an initial state if (isAskForInitialState()) { - initialState = GUIInitialStatePicker.defineInitalValuesWithDialog(getGUI(), lastInitialState, - parsedModel); + initialState = GUIInitialStatePicker.defineInitalValuesWithDialog(getGUI(), lastInitialState, parsedModel); // if user clicked cancel from dialog... if (initialState == null) { @@ -391,16 +385,16 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect tableScroll.setViewportView(pathTable); displayPathLoops = true; + + // Create a new path in the simulator and add labels/properties engine.createNewPath(parsedModel, pf); engine.initialisePath(initialState); - //engine.setPropertyConstants(lastPropertyConstants); - pathActive = true; + repopulateFormulae(pf); totalTimeLabel.setText(formatDouble(engine.getTotalPathTime())); pathLengthLabel.setText("" + (engine.getPathSize() - 1)); - definedConstantsLabel.setText((uCon.getDefinedConstantsString().length() == 0) ? "None" : uCon - .getDefinedConstantsString()); + definedConstantsLabel.setText((uCon.getDefinedConstantsString().length() == 0) ? "None" : uCon.getDefinedConstantsString()); doEnables(); @@ -408,10 +402,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect updateTableModel.restartUpdatesTable(); - pathTable.getSelectionModel() - .setSelectionInterval(pathTable.getRowCount() - 1, pathTable.getRowCount() - 1); + pathTable.getSelectionModel().setSelectionInterval(pathTable.getRowCount() - 1, pathTable.getRowCount() - 1); - repopulateFormulae(); stateLabelList.repaint(); pathFormulaeList.repaint(); @@ -455,8 +447,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathTableModel.updatePathTable(); updateTableModel.updateUpdatesTable(); - pathTable.scrollRectToVisible(new Rectangle(0, (int) pathTable.getPreferredSize().getHeight() - 10, - (int) pathTable.getPreferredSize().getWidth(), (int) pathTable.getPreferredSize().getHeight())); + pathTable.scrollRectToVisible(new Rectangle(0, (int) pathTable.getPreferredSize().getHeight() - 10, (int) pathTable.getPreferredSize().getWidth(), + (int) pathTable.getPreferredSize().getHeight())); totalTimeLabel.setText(formatDouble(engine.getTotalPathTime())); pathLengthLabel.setText("" + (engine.getPathSize() - 1)); @@ -501,8 +493,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathTableModel.updatePathTable(); updateTableModel.updateUpdatesTable(); - pathTable.scrollRectToVisible(new Rectangle(0, (int) pathTable.getPreferredSize().getHeight() - 10, - (int) pathTable.getPreferredSize().getWidth(), (int) pathTable.getPreferredSize().getHeight())); + pathTable.scrollRectToVisible(new Rectangle(0, (int) pathTable.getPreferredSize().getHeight() - 10, (int) pathTable.getPreferredSize().getWidth(), + (int) pathTable.getPreferredSize().getHeight())); totalTimeLabel.setText(formatDouble(engine.getTotalPathTime())); pathLengthLabel.setText("" + (engine.getPathSize() - 1)); @@ -621,7 +613,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect try { if (currentUpdatesTable.getSelectedRow() == -1) throw new PrismException("No current update is selected"); - + if (displayPathLoops && pathTableModel.isPathLooping()) { if (questionYesNo("A loop in the path has been detected. Do you wish to disable loop detection and extend the path?") == 0) { displayPathLoops = false; @@ -650,8 +642,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathTableModel.updatePathTable(); updateTableModel.updateUpdatesTable(); - pathTable.scrollRectToVisible(new Rectangle(0, pathTable.getHeight() - 10, pathTable.getWidth(), - pathTable.getHeight())); + pathTable.scrollRectToVisible(new Rectangle(0, pathTable.getHeight() - 10, pathTable.getWidth(), pathTable.getHeight())); totalTimeLabel.setText(formatDouble(engine.getTotalPathTime())); pathLengthLabel.setText("" + (engine.getPathSize() - 1)); @@ -661,7 +652,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } else { setComputing(true); - + engine.manualUpdate(currentUpdatesTable.getSelectedRow()); pathTableModel.updatePathTable(); @@ -670,16 +661,15 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect totalTimeLabel.setText("" + engine.getTotalPathTime()); pathLengthLabel.setText("" + (engine.getPathSize() - 1)); - pathTable.scrollRectToVisible(new Rectangle(0, (int) pathTable.getPreferredSize().getHeight() - 10, - (int) pathTable.getPreferredSize().getWidth(), (int) pathTable.getPreferredSize().getHeight())); + pathTable.scrollRectToVisible(new Rectangle(0, (int) pathTable.getPreferredSize().getHeight() - 10, (int) pathTable.getPreferredSize() + .getWidth(), (int) pathTable.getPreferredSize().getHeight())); setComputing(false); } stateLabelList.repaint(); pathFormulaeList.repaint(); } catch (NumberFormatException e) { - this - .error("The Auto update \'no. steps\' parameter is invalid.\nIt must be a positive integer representing a step in the path table"); + this.error("The Auto update \'no. steps\' parameter is invalid.\nIt must be a positive integer representing a step in the path table"); setComputing(false); } catch (PrismException e) { this.error(e.getMessage()); @@ -692,12 +682,36 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect new GUIViewDialog(gui, pathTableModel.getView()); } - /* Repopulate "State labels" and "Path formulae" lists */ - - public void repopulateFormulae() + /** + * Re-populate lists of labels and path formulas. + * Labels are taken from current model and passed in properties file. + * Path formulas are taken from the passed in properties file. + */ + private void repopulateFormulae(PropertiesFile propertiesFile) { - // "Path formulae" list - ((GUISimPathFormulaeList) pathFormulaeList).clearList(); + // Labels + GUISimLabelList theStateLabelList = (GUISimLabelList) stateLabelList; + theStateLabelList.clearLabels(); + if (pathActive) { + // Add the default labels: "init" and "deadlock" + theStateLabelList.addDeadlockAndInit(); + if (parsedModel != null) { + // Add labels from model + LabelList labelList1 = parsedModel.getLabelList(); + for (int i = 0; i < labelList1.size(); i++) { + theStateLabelList.addModelLabel(labelList1.getLabelName(i), labelList1.getLabel(i)); + } + // Add labels from properties file + LabelList labelList2 = propertiesFile.getLabelList(); + for (int i = 0; i < labelList2.size(); i++) { + theStateLabelList.addPropertyLabel(labelList2.getLabelName(i), labelList2.getLabel(i), propertiesFile); + } + } + } + + // TODO: fix and re-enable this (note: should use passed in properties file) + // Path formulas + /*((GUISimPathFormulaeList) pathFormulaeList).clearList(); if (pathActive) { // Go through the property list from the Properties tab of GUI GUIPropertiesList gpl = guiProp.getPropList(); @@ -706,46 +720,17 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // For properties which are simulate-able... if (gp.isValidForSimulation()) { Expression expr = gp.getProperty(); - // TODO: re-enable... // Add them to the list - /*if (expr instanceof ExpressionProb) { + if (expr instanceof ExpressionProb) { ExpressionProb prob = (ExpressionProb) expr; ((GUISimPathFormulaeList) pathFormulaeList).addProbFormula(prob); } else if (expr instanceof ExpressionReward) { ExpressionReward rew = (ExpressionReward) expr; ((GUISimPathFormulaeList) pathFormulaeList).addRewardFormula(rew); - }*/ - } - } - } - // "State labels" list - ((GUISimLabelFormulaeList) stateLabelList).clearLabels(); - if (pathActive) { - // Add the default labels: "init" and "deadlock" - ((GUISimLabelFormulaeList) stateLabelList).addDeadlockAndInit(); - if (parsedModel != null) { - // Add labels from model - LabelList labelList1 = parsedModel.getLabelList(); - for (int i = 0; i < labelList1.size(); i++) { - ((GUISimLabelFormulaeList) stateLabelList).addLabel(labelList1.getLabelName(i), labelList1 - .getLabel(i), parsedModel); - } - // Add (correctly parsing) labels from label list in Properties tab of GUI - GUIPropLabelList labelList2 = guiProp.getLabTable(); - for (int i = 0; i < labelList2.getNumLabels(); i++) { - GUILabel gl = labelList2.getLabel(i); - if (gl.isParseable()) { - try { - PropertiesFile pf = getPrism().parsePropertiesString(parsedModel, - guiProp.getConstantsString().toString() + "\n" + gl.toString()); - ((GUISimLabelFormulaeList) stateLabelList).addLabel(pf.getLabelList().getLabelName(0), pf - .getLabelList().getLabel(0), parsedModel); - } catch (PrismException e) { - } } } } - } + }*/ } //METHODS TO IMPLEMENT THE GUIPLUGIN INTERFACE @@ -941,7 +926,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect outerStateLabelPanel = new javax.swing.JPanel(); stateLabelScrollPane = new javax.swing.JScrollPane(); stateLabelList = new javax.swing.JList(); - stateLabelList = new GUISimLabelFormulaeList(this); + stateLabelList = new GUISimLabelList(this); outerPathFormulaePanel = new javax.swing.JPanel(); pathFormulaeScrollPane = new javax.swing.JScrollPane(); pathFormulaeList = new javax.swing.JList(); @@ -1052,9 +1037,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect innerButtonPanel.add(configureViewButton); - pathTable.setModel(new javax.swing.table.DefaultTableModel(new Object[][] { { null, null, null, null }, - { null, null, null, null }, { null, null, null, null }, { null, null, null, null } }, new String[] { - "Title 1", "Title 2", "Title 3", "Title 4" })); + pathTable.setModel(new javax.swing.table.DefaultTableModel(new Object[][] { { null, null, null, null }, { null, null, null, null }, + { null, null, null, null }, { null, null, null, null } }, new String[] { "Title 1", "Title 2", "Title 3", "Title 4" })); jSplitPane1.setLeftComponent(jPanel3); jSplitPane1.setRightComponent(jPanel4); @@ -1219,8 +1203,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect noStepsExplorePanel.setLayout(new java.awt.GridBagLayout()); noStepsExplorePanel.setMinimumSize(new java.awt.Dimension(107, 0)); - typeExploreCombo.setModel(new javax.swing.DefaultComboBoxModel(new String[] { "Num. steps", "Upto state", - "Max. time" })); + typeExploreCombo.setModel(new javax.swing.DefaultComboBoxModel(new String[] { "Num. steps", "Upto state", "Max. time" })); typeExploreCombo.setToolTipText(""); gridBagConstraints = new java.awt.GridBagConstraints(); gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH; @@ -1319,9 +1302,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect innerManualUpdatesPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5)); manualUpdateTableScrollPane.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); - currentUpdatesTable.setModel(new javax.swing.table.DefaultTableModel(new Object[][] { - { null, null, null, null }, { null, null, null, null }, { null, null, null, null }, - { null, null, null, null } }, new String[] { "Title 1", "Title 2", "Title 3", "Title 4" })); + currentUpdatesTable.setModel(new javax.swing.table.DefaultTableModel(new Object[][] { { null, null, null, null }, { null, null, null, null }, + { null, null, null, null }, { null, null, null, null } }, new String[] { "Title 1", "Title 2", "Title 3", "Title 4" })); currentUpdatesTable.setToolTipText("Double click on an update to manually execute the update"); manualUpdateTableScrollPane.setViewportView(currentUpdatesTable); @@ -1331,8 +1313,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect autoTimeCheckPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 0, 0, 0)); autoTimeCheck.setText("Generate time automatically"); - autoTimeCheck - .setToolTipText("When not selected, you will be prompted to manually enter the time spent in states"); + autoTimeCheck.setToolTipText("When not selected, you will be prompted to manually enter the time spent in states"); autoTimeCheck.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 0, 0, 0)); autoTimeCheck.setHorizontalAlignment(javax.swing.SwingConstants.RIGHT); autoTimeCheck.setMargin(new java.awt.Insets(0, 0, 0, 0)); @@ -1453,9 +1434,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect else a_backTrack(engine.getTotalPathTime() - time); } catch (NumberFormatException nfe) { - throw new PrismException( - "The \"Time\" parameter is invalid, it must be a positive double smaller than the cumulative path time (which is " - + engine.getTotalPathTime() + ")"); + throw new PrismException("The \"Time\" parameter is invalid, it must be a positive double smaller than the cumulative path time (which is " + + engine.getTotalPathTime() + ")"); } } else if (typeBacktrackCombo.getSelectedIndex() == 3) { double time; @@ -1798,16 +1778,14 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect a_newPath(); } if (e.isPopupTrigger() - && (e.getSource() == pathTablePlaceHolder || e.getSource() == pathTable - || e.getSource() == pathTable.getTableHeader() || e.getSource() == tableScroll)) { - randomExploration.setEnabled(!(e.getSource() == pathTable.getTableHeader() - || e.getSource() == pathTablePlaceHolder || e.getSource() == tableScroll)); - backtrack.setEnabled(!(e.getSource() == pathTable.getTableHeader() - || e.getSource() == pathTablePlaceHolder || e.getSource() == tableScroll)); - backtrackToHere.setEnabled(!(e.getSource() == pathTable.getTableHeader() - || e.getSource() == pathTablePlaceHolder || e.getSource() == tableScroll)); - removeToHere.setEnabled(!(e.getSource() == pathTable.getTableHeader() - || e.getSource() == pathTablePlaceHolder || e.getSource() == tableScroll)); + && (e.getSource() == pathTablePlaceHolder || e.getSource() == pathTable || e.getSource() == pathTable.getTableHeader() || e.getSource() == tableScroll)) { + randomExploration + .setEnabled(!(e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTablePlaceHolder || e.getSource() == tableScroll)); + backtrack.setEnabled(!(e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTablePlaceHolder || e.getSource() == tableScroll)); + backtrackToHere + .setEnabled(!(e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTablePlaceHolder || e.getSource() == tableScroll)); + removeToHere + .setEnabled(!(e.getSource() == pathTable.getTableHeader() || e.getSource() == pathTablePlaceHolder || e.getSource() == tableScroll)); doEnables(); @@ -2325,8 +2303,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public boolean equals(Object o) { - return (o instanceof RewardStructure && ((RewardStructure) o).getIndex() == index && ((RewardStructure) o) - .isCumulative() == isCumulative()); + return (o instanceof RewardStructure && ((RewardStructure) o).getIndex() == index && ((RewardStructure) o).isCumulative() == isCumulative()); } } @@ -2583,15 +2560,12 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect for (Object obj : visibleRewardListItems) { GUIViewDialog.RewardListItem item = (GUIViewDialog.RewardListItem) obj; if (item.isCumulative()) - visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), - GUISimulator.RewardStructureColumn.CUMULATIVE_REWARD)); + visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), GUISimulator.RewardStructureColumn.CUMULATIVE_REWARD)); else { if (!item.getRewardStructure().isStateEmpty()) - visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), - GUISimulator.RewardStructureColumn.STATE_REWARD)); + visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), GUISimulator.RewardStructureColumn.STATE_REWARD)); if (!item.getRewardStructure().isTransitionEmpty()) - visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), - GUISimulator.RewardStructureColumn.TRANSITION_REWARD)); + visibleRewardColumns.add(new RewardStructureColumn(item.getRewardStructure(), GUISimulator.RewardStructureColumn.TRANSITION_REWARD)); } } @@ -2679,10 +2653,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect for (Object rewobj : rewards) { RewardStructure rew = (RewardStructure) rewobj; - if (rew.isStateEmpty() == !hasStates - && rew.isTransitionEmpty() == !hasTrans - && ((rew.getName() == null && rewardName.equals("")) || (rew.getName() != null && rew - .getName().equals(rewardName)))) { + if (rew.isStateEmpty() == !hasStates && rew.isTransitionEmpty() == !hasTrans + && ((rew.getName() == null && rewardName.equals("")) || (rew.getName() != null && rew.getName().equals(rewardName)))) { allrew.remove(rew); foundReward = true; } @@ -2717,20 +2689,17 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect rewardName = null; } - RewardStructure rewardStructure = new RewardStructure(r, rewardName, parsedModel - .getRewardStruct(r).getNumStateItems() == 0, parsedModel.getRewardStruct(r) - .getNumTransItems() == 0); + 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)); + visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, RewardStructureColumn.STATE_REWARD)); if (!rewardStructure.isTransitionEmpty()) - visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, - RewardStructureColumn.TRANSITION_REWARD)); + visibleRewardColumns.add(new RewardStructureColumn(rewardStructure, RewardStructureColumn.TRANSITION_REWARD)); } } @@ -2957,8 +2926,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect { 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 varStart = timeStart + (view.canShowTime() && view.showTime() ? 1 : 0) + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); int rewardStart = varStart + view.getVisibleVariables().size(); int groupCount = 0; @@ -3066,8 +3034,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect 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.canShowTime() && view.showTime() ? 1 : 0) + (view.canShowTime() && view.showCumulativeTime() ? 1 : 0); colCount += view.getVisibleVariables().size(); colCount += view.getVisibleRewardColumns().size(); @@ -3089,8 +3056,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect { int selection = stateLabelList.getSelectedIndex(); if (selection != -1) { - GUISimLabelFormulaeList.SimLabel label = (GUISimLabelFormulaeList.SimLabel) stateLabelList.getModel() - .getElementAt(selection); + GUISimLabelList.SimLabel label = (GUISimLabelList.SimLabel) stateLabelList.getModel().getElementAt(selection); if (row == getRowCount() - 1) { if (label.getResult() == 1) return true; @@ -3129,8 +3095,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } else if (rewardStart <= columnIndex) { - return ((RewardStructureColumn) view.getVisibleRewardColumns().get(columnIndex - rewardStart)) - .getColumnName(); + return ((RewardStructureColumn) view.getVisibleRewardColumns().get(columnIndex - rewardStart)).getColumnName(); } } return "Undefined Column"; @@ -3158,13 +3123,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } // A variable column else if (varStart <= columnIndex && columnIndex < rewardStart) { - return "Values of variable \"" - + ((Variable) view.getVisibleVariables().get(columnIndex - varStart)).toString() + "\""; + return "Values of variable \"" + ((Variable) view.getVisibleVariables().get(columnIndex - varStart)).toString() + "\""; } else if (rewardStart <= columnIndex) { - RewardStructureColumn column = ((RewardStructureColumn) view.getVisibleRewardColumns().get( - columnIndex - rewardStart)); + RewardStructureColumn column = ((RewardStructureColumn) view.getVisibleRewardColumns().get(columnIndex - rewardStart)); String rewardName = column.getRewardStructure().getColumnName(); if (column.isStateReward()) @@ -3206,8 +3169,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } // Cumulative time column else if (cumulativeTimeStart <= columnIndex && columnIndex < varStart) { - timeValue = new TimeValue((rowIndex == 0) ? 0.0 : engine - .getCumulativeTimeSpentInPathState(rowIndex - 1), true); + timeValue = new TimeValue((rowIndex == 0) ? 0.0 : engine.getCumulativeTimeSpentInPathState(rowIndex - 1), true); timeValue.setTimeValueUnknown(rowIndex >= engine.getPathSize()); return timeValue; } @@ -3217,33 +3179,27 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect Object result = engine.getPathData(var.getIndex(), rowIndex); variableValue.setVariable(var); variableValue.setValue(result); - variableValue.setChanged(rowIndex == 0 - || !engine.getPathData(var.getIndex(), rowIndex - 1).equals(result)); + variableValue.setChanged(rowIndex == 0 || !engine.getPathData(var.getIndex(), rowIndex - 1).equals(result)); return variableValue; } // A reward column else if (rewardStart <= columnIndex) { - RewardStructureColumn rewardColumn = (RewardStructureColumn) view.getVisibleRewardColumns().get( - columnIndex - rewardStart); + RewardStructureColumn rewardColumn = (RewardStructureColumn) view.getVisibleRewardColumns().get(columnIndex - rewardStart); rewardStructureValue.setRewardStructureColumn(rewardColumn); rewardStructureValue.setRewardValueUnknown(false); // A state reward column if (rewardColumn.isStateReward()) { - double value = engine.getStateRewardOfPathState(rowIndex, rewardColumn.getRewardStructure() - .getIndex()); + double value = engine.getStateRewardOfPathState(rowIndex, rewardColumn.getRewardStructure().getIndex()); rewardStructureValue.setChanged(rowIndex == 0 - || value != engine.getStateRewardOfPathState(rowIndex - 1, rewardColumn - .getRewardStructure().getIndex())); + || value != engine.getStateRewardOfPathState(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())); rewardStructureValue.setRewardValue(new Double(value)); rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize() - 1); } // A transition reward column else if (rewardColumn.isTransitionReward()) { - double value = engine.getTransitionRewardOfPathState(rowIndex, rewardColumn - .getRewardStructure().getIndex()); + double value = engine.getTransitionRewardOfPathState(rowIndex, rewardColumn.getRewardStructure().getIndex()); rewardStructureValue.setChanged(rowIndex == 0 - || value != engine.getTransitionRewardOfPathState(rowIndex - 1, rewardColumn - .getRewardStructure().getIndex())); + || value != engine.getTransitionRewardOfPathState(rowIndex - 1, rewardColumn.getRewardStructure().getIndex())); rewardStructureValue.setRewardValue(new Double(value)); rewardStructureValue.setRewardValueUnknown(rowIndex >= engine.getPathSize() - 1); } @@ -3254,17 +3210,13 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect rewardStructureValue.setRewardValue(new Double(0.0)); rewardStructureValue.setRewardValueUnknown(false); } else { - double value = engine.getTotalStateRewardOfPathState(rowIndex - 1, rewardColumn - .getRewardStructure().getIndex()) - + engine.getTotalTransitionRewardOfPathState(rowIndex - 1, rewardColumn - .getRewardStructure().getIndex()); + double value = engine.getTotalStateRewardOfPathState(rowIndex - 1, rewardColumn.getRewardStructure().getIndex()) + + engine.getTotalTransitionRewardOfPathState(rowIndex - 1, rewardColumn.getRewardStructure().getIndex()); if (rowIndex == 1) rewardStructureValue.setChanged(value != 0.0); else - rewardStructureValue.setChanged(value != (engine.getTotalStateRewardOfPathState( - rowIndex - 2, rewardColumn.getRewardStructure().getIndex()) + engine - .getTotalTransitionRewardOfPathState(rowIndex - 2, rewardColumn - .getRewardStructure().getIndex()))); + rewardStructureValue.setChanged(value != (engine.getTotalStateRewardOfPathState(rowIndex - 2, rewardColumn.getRewardStructure() + .getIndex()) + engine.getTotalTransitionRewardOfPathState(rowIndex - 2, rewardColumn.getRewardStructure().getIndex()))); rewardStructureValue.setRewardValue(new Double(value)); rewardStructureValue.setRewardValueUnknown(rowIndex >= engine.getPathSize()); } @@ -3504,10 +3456,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect if (displayStyleFast != view.isChangeRenderer()) { String[] answers = { "Yes", "No" }; - if (GUISimulator.this - .question( - "You have changed the default rendering style of paths. Do you wish \nto reflect this in your current trace?", - answers, 0) == 0) { + if (GUISimulator.this.question("You have changed the default rendering style of paths. Do you wish \nto reflect this in your current trace?", + answers, 0) == 0) { view.setRenderer(displayStyleFast); } }