From 10313b7d02084cf5b261234852c2a00120158557 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 25 Jul 2011 10:52:32 +0000 Subject: [PATCH] Improved handling of undefined constants in properties files: * don't need to provide values for all constants, just those required for model checking And a few related bug fixes: * in error handling for constants in PrismCL * in export of labels from properties file with constants And some small related API changes: * don't need to call setUndefinedConstants on ModulesFile/PropertiesFile if there are no undefined constants * more flexible UndefinedConstants classes git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3319 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ASTElement.java | 17 +++ prism/src/parser/ast/ConstantList.java | 101 +++++++++------ prism/src/parser/ast/ModulesFile.java | 21 ++-- prism/src/parser/ast/PropertiesFile.java | 98 ++++++++++++--- .../GetAllUndefinedConstantsRecursively.java | 81 ++++++++++++ prism/src/prism/Prism.java | 6 +- prism/src/prism/PrismCL.java | 67 ++++++---- prism/src/prism/ResultsCollection.java | 5 +- prism/src/prism/UndefinedConstants.java | 119 ++++++++++++++++-- .../properties/GUIExperiment.java | 2 +- .../properties/GUIMultiProperties.java | 17 ++- .../userinterface/simulator/GUISimulator.java | 6 +- 12 files changed, 427 insertions(+), 113 deletions(-) create mode 100644 prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index c0d5beb6..fdb387de 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/prism/src/parser/ast/ASTElement.java @@ -269,6 +269,23 @@ public abstract class ASTElement return v; } + /** + * Get all undefined constants used (i.e. in ExpressionConstant objects) recursively and return as a list. + * Recursive decent means that we find e.g. constants that are used within other constants, labels. + */ + public Vector getAllUndefinedConstantsRecursively(ConstantList constantList, LabelList labelList) + { + Vector v= new Vector(); + GetAllUndefinedConstantsRecursively visitor = new GetAllUndefinedConstantsRecursively(v, constantList, labelList); + try { + accept(visitor); + } catch (PrismLangException e) { + // GetAllUndefinedConstantsRecursively can throw an exception (if a constant does not exist) + // but this would have been caught by earlier checks so we ignore. + } + return v; + } + /** * Expand all constants, return result. */ diff --git a/prism/src/parser/ast/ConstantList.java b/prism/src/parser/ast/ConstantList.java index 9aa5b735..2cfe6ed5 100644 --- a/prism/src/parser/ast/ConstantList.java +++ b/prism/src/parser/ast/ConstantList.java @@ -212,20 +212,46 @@ public class ConstantList extends ASTElement return v; } - // Set values for undefined constants, evaluate all and return. - // Argument 'someValues' contains values for undefined ones, can be null if all already defined - // Argument 'otherValues' contains any other values which may be needed, null if none - + /** + * Set values for *all* undefined constants, evaluate values for *all* constants + * and return a Values object with values for *all* constants. + * Argument 'someValues' contains values for undefined ones, can be null if all already defined + * Argument 'otherValues' contains any other values which may be needed, null if none + */ public Values evaluateConstants(Values someValues, Values otherValues) throws PrismLangException + { + return evaluateSomeOrAllConstants(someValues, otherValues, true); + } + + /** + * Set values for *some* undefined constants, evaluate values for constants where possible + * and return a Values object with values for all constants that could be evaluated. + * Argument 'someValues' contains values for undefined ones, can be null if all already defined + * Argument 'otherValues' contains any other values which may be needed, null if none + */ + public Values evaluateSomeConstants(Values someValues, Values otherValues) throws PrismLangException + { + return evaluateSomeOrAllConstants(someValues, otherValues, false); + } + + /** + * Set values for *some* or *all* undefined constants, evaluate values for constants where possible + * and return a Values object with values for all constants that could be evaluated. + * Argument 'someValues' contains values for undefined ones, can be null if all already defined. + * Argument 'otherValues' contains any other values which may be needed, null if none. + * If argument 'all' is true, an exception is thrown if any undefined constant is not defined. + */ + private Values evaluateSomeOrAllConstants(Values someValues, Values otherValues, boolean all) throws PrismLangException { ConstantList cl; Expression e; Values allValues; - int i, j, n; + int i, j, n, numToEvaluate; Type t = null; ExpressionIdent s; + Object val; - // create new copy of this ConstantList + // Create new copy of this ConstantList // (copy existing constant definitions, add new ones where undefined) cl = new ConstantList(); n = constants.size(); @@ -235,55 +261,50 @@ public class ConstantList extends ASTElement t = getConstantType(i); if (e != null) { cl.addConstant((ExpressionIdent)s.deepCopy(), e.deepCopy(), t); - } - else - { - // create new literal expression using values passed in - j = someValues.getIndexOf(s.getName()); - if (j == -1) { - throw new PrismLangException("No value specified for constant", s); - } - else - { - if (t instanceof TypeInt) - cl.addConstant((ExpressionIdent)s.deepCopy(), new ExpressionLiteral(TypeInt.getInstance(), someValues.getIntValue(j)), TypeInt.getInstance()); - else if (t instanceof TypeDouble) - cl.addConstant((ExpressionIdent)s.deepCopy(), new ExpressionLiteral(TypeDouble.getInstance(), someValues.getDoubleValue(j)), TypeDouble.getInstance()); - else if (t instanceof TypeBool) - cl.addConstant((ExpressionIdent)s.deepCopy(), new ExpressionLiteral(TypeBool.getInstance(), someValues.getBooleanValue(j)), TypeBool.getInstance()); + } else { + // Create new literal expression using values passed in (if possible and needed) + if (someValues != null && (j = someValues.getIndexOf(s.getName())) != -1) { + cl.addConstant((ExpressionIdent) s.deepCopy(), new ExpressionLiteral(t, t.castValueTo(someValues.getValue(j))), t); + } else { + if (all) + throw new PrismLangException("No value specified for constant", s); } } } + numToEvaluate = cl.size(); - // now add constants corresponding to the 'otherValues' argument to the new constant list + // Now add constants corresponding to the 'otherValues' argument to the new constant list if (otherValues != null) { n = otherValues.getNumValues(); for (i = 0; i < n; i++) { Type iType = otherValues.getType(i); - if (iType instanceof TypeInt) - cl.addConstant(new ExpressionIdent(otherValues.getName(i)), new ExpressionLiteral(TypeInt.getInstance(), otherValues.getIntValue(i)), TypeInt.getInstance()); - else if (iType instanceof TypeDouble) - cl.addConstant(new ExpressionIdent(otherValues.getName(i)), new ExpressionLiteral(TypeDouble.getInstance(), otherValues.getDoubleValue(i)), TypeDouble.getInstance()); - else if (iType instanceof TypeBool) - cl.addConstant(new ExpressionIdent(otherValues.getName(i)), new ExpressionLiteral(TypeBool.getInstance(), otherValues.getBooleanValue(i)), TypeBool.getInstance()); + cl.addConstant(new ExpressionIdent(otherValues.getName(i)), new ExpressionLiteral(iType, iType.castValueTo(otherValues.getValue(i))), iType); } } - // go thru and expand definition of each constant + // Go trough and expand definition of each constant // (i.e. replace other constant references with their definitions) - // (working with new copy of constant list) - // (and ignoring extra constants added on the end which are all defined) - n = constants.size(); - for (i = 0; i < n; i++) { - cl.setConstant(i, (Expression)cl.getConstant(i).expandConstants(cl)); + // Note: work with new copy of constant list, don't need to expand 'otherValues' ones. + for (i = 0; i < numToEvaluate; i++) { + try { + e = (Expression)cl.getConstant(i).expandConstants(cl); + cl.setConstant(i, e); + } catch (PrismLangException ex) { + if (all) { + throw ex; + } else { + cl.setConstant(i, null); + } + } } - // evaluate constants and store in new Values object - // (again, ignoring extra constants added on the end) + // Evaluate constants and store in new Values object (again, ignoring 'otherValues' ones) allValues = new Values(); - n = constants.size(); - for (i = 0; i < n; i++) { - allValues.addValue(cl.getConstantName(i), cl.getConstant(i).evaluate(null, otherValues)); + for (i = 0; i < numToEvaluate; i++) { + if (cl.getConstant(i) != null) { + val = cl.getConstant(i).evaluate(null, otherValues); + allValues.addValue(cl.getConstantName(i), val); + } } return allValues; diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 1fd46eb0..0e3d6b9e 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -64,7 +64,7 @@ public class ModulesFile extends ASTElement private Vector varNames; private Vector varTypes; - // actual values of constants + // actual values of (some or all) constants private Values constantValues; // Constructor @@ -490,6 +490,14 @@ public class ModulesFile extends ASTElement // Check constants for cyclic dependencies constantList.findCycles(); + // If there are no undefined constants, set up values for constants + // (to avoid need for a later call to setUndefinedConstants). + // NB: Can't call setUndefinedConstants if there are undefined constants + // because semanticCheckAfterConstants may fail. + if (getUndefinedConstants().isEmpty()) { + setUndefinedConstants(null); + } + // Check variable names, etc. checkVarNames(); // Find all instances of variables, replace identifiers with variables. @@ -750,15 +758,12 @@ public class ModulesFile extends ASTElement } /** - * Set values for all undefined constants and then evaluate all constants. - * Always need to call this before any model building/checking/simulation/etc., - * even when there are no undefined constants - * (if this is the case, {@code someValues} can be null). - * Calling this method also triggers some additional semantic checks - * that can only be done once constant values have been specified. - *

+ * Set values for *all* undefined constants and then evaluate all constants. + * If there are no undefined constants, {@code someValues} can be null. * Undefined constants can be subsequently redefined to different values with the same method. * The current constant values (if set) are available via {@link #setUndefinedConstants(Values)}. + * Calling this method also triggers some additional semantic checks + * that can only be done once constant values have been specified. */ public void setUndefinedConstants(Values someValues) throws PrismLangException { diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 3acd6ae2..65980b1f 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -49,7 +49,7 @@ public class PropertiesFile extends ASTElement // list of all identifiers used private Vector allIdentsUsed; - // actual values of constants + // actual values of (some or all) constants private Values constantValues; // Constructor @@ -212,6 +212,10 @@ public class PropertiesFile extends ASTElement // check constants for cyclic dependencies constantList.findCycles(); + // Set up some values for constants + // (without assuming any info about undefined constants) + setSomeUndefinedConstants(null); + // Check property names checkPropertyNames(); @@ -352,7 +356,7 @@ public class PropertiesFile extends ASTElement } /** - * Get a list of constants in the model that are undefined + * Get a list of all undefined constants in the properties files * ("const int x;" rather than "const int x = 1;") */ public Vector getUndefinedConstants() @@ -361,27 +365,93 @@ public class PropertiesFile extends ASTElement } /** - * Set values for all undefined constants and then evaluate all constants. - * Always need to call this before using the properties file, - * even when there are no undefined constants - * (if this is the case, {@code someValues} can be null). - * Calling this method also triggers some additional semantic checks - * that can only be done once constant values have been specified. - *

+ * Get a list of undefined (properties file) constants appearing in labels of the properties file + * (undefined constants are those of form "const int x;" rather than "const int x = 1;") + */ + public Vector getUndefinedConstantsUsedInLabels() + { + int i, n; + Expression expr; + Vector consts, tmp; + consts = new Vector(); + n = labelList.size(); + for (i = 0; i < n; i++) { + expr = labelList.getLabel(i); + tmp = expr.getAllUndefinedConstantsRecursively(constantList, combinedLabelList); + for (String s : tmp) { + if (!consts.contains(s)) { + consts.add(s); + } + } + } + return consts; + } + + /** + * Get a list of undefined (properties file) constants used in a property + * (including those that appear in required labels/properties) + * (undefined constants are those of form "const int x;" rather than "const int x = 1;") + */ + public Vector getUndefinedConstantsUsedInProperty(Property prop) + { + return prop.getExpression().getAllUndefinedConstantsRecursively(constantList, combinedLabelList); + } + + /** + * Get a list of undefined (properties file) constants used in a list of properties + * (including those that appear in required labels/properties) + * (undefined constants are those of form "const int x;" rather than "const int x = 1;") + */ + public Vector getUndefinedConstantsUsedInProperties(List props) + { + Vector consts, tmp; + consts = new Vector(); + for (Property prop : props) { + tmp = prop.getExpression().getAllUndefinedConstantsRecursively(constantList, combinedLabelList); + for (String s : tmp) { + if (!consts.contains(s)) { + consts.add(s); + } + } + } + return consts; + } + + /** + * Set values for *all* undefined constants and then evaluate all constants. + * If there are no undefined constants, {@code someValues} can be null. * Undefined constants can be subsequently redefined to different values with the same method. * The current constant values (if set) are available via {@link #setUndefinedConstants(Values)}. */ public void setUndefinedConstants(Values someValues) throws PrismLangException { - // might need values for ModulesFile constants too + // Might need values for ModulesFile constants too constantValues = constantList.evaluateConstants(someValues, modulesFile.getConstantValues()); - semanticCheckAfterConstants(modulesFile, this); + // Note: unlike ModulesFile, we don't trigger any semantic checks at this point + // This will usually be done on a per-property basis later + // (and sometimes we don't want to have to define all constants) + } + + /** + * Set values for *some* undefined constants and then evaluate all constants where possible. + * If there are no undefined constants, {@code someValues} can be null. + * Undefined constants can be subsequently redefined to different values with the same method. + * The current constant values (if set) are available via {@link #setUndefinedConstants(Values)}. + */ + public void setSomeUndefinedConstants(Values someValues) throws PrismLangException + { + // Might need values for ModulesFile constants too + constantValues = constantList.evaluateSomeConstants(someValues, modulesFile.getConstantValues()); + // Note: unlike ModulesFile, we don't trigger any semantic checks at this point + // This will usually be done on a per-property basis later + // (and sometimes we don't want to have to define all constants) } /** - * Get access to the values assigned to undefined constants in the model, - * as set previously via the method {@link #setUndefinedConstants(Values)}. - * Until they are set for the first time, this method returns null. + * Get access to the values assigned to constants in the model, + * as set previously via the method {@link #setUndefinedConstants(Values)} + * or {@link #setUndefinedConstants(Values)}. If neither method has been called + * constant values will have been evaluated assuming that there are no undefined constants. */ public Values getConstantValues() { diff --git a/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java b/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java new file mode 100644 index 00000000..329f599e --- /dev/null +++ b/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java @@ -0,0 +1,81 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * 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 parser.visitor; + +import java.util.Vector; + +import parser.ast.*; +import prism.PrismLangException; + +/** + * Get all undefined constants used (i.e. in ExpressionConstant objects) recursively and return as a list. + * Recursive decent means that we find e.g. constants that are used within other constants, labels. + */ +public class GetAllUndefinedConstantsRecursively extends ASTTraverse +{ + private Vector v; + private ConstantList constantList; + private LabelList labelList; + + public GetAllUndefinedConstantsRecursively(Vector v, ConstantList constantList, LabelList labelList) + { + this.v = v; + this.constantList = constantList; + this.labelList = labelList; + } + + public void visitPost(ExpressionConstant e) throws PrismLangException + { + // Look up this constant in the constant list + int i = constantList.getConstantIndex(e.getName()); + if (i == -1) + throw new PrismLangException("Unknown constant \"" + e.getName() + "\""); + Expression expr = constantList.getConstant(i); + // If constant is undefined, add to the list + if (expr == null) { + if (!v.contains(e.getName())) { + v.addElement(e.getName()); + } + } + // If not, check constant definition recursively for more undefined constants + else { + expr.accept(this); + } + } + + public void visitPost(ExpressionLabel e) throws PrismLangException + { + // Look up this label in the label list + int i = labelList.getLabelIndex(e.getName()); + if (i == -1) + throw new PrismLangException("Unknown label \"" + e.getName() + "\""); + Expression expr = labelList.getLabel(i); + // Check label definition recursively for more undefined constants + expr.accept(this); + } +} + diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 14768ce2..1e63900c 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1385,7 +1385,6 @@ public class Prism implements PrismSettingsListener int i, n; LabelList ll; Expression expr; - Values constantValues; StateModelChecker mc = null; JDDNode dd, labels[]; String labelNames[]; @@ -1405,10 +1404,7 @@ public class Prism implements PrismSettingsListener // convert labels to bdds if (n > 0) { - constantValues = new Values(); - constantValues.addValues(model.getConstantValues()); - if (propertiesFile != null) constantValues.addValues(propertiesFile.getConstantValues()); - mc = new StateModelChecker(this, model, null); + mc = new StateModelChecker(this, model, propertiesFile); } labels = new JDDNode[n+2]; labels[0] = model.getStart(); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index bf25eed6..1fb4504e 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -131,7 +131,8 @@ public class PrismCL private List propertiesToCheck = null; // info about undefined constants - private UndefinedConstants undefinedConstants; + private UndefinedConstants undefinedConstants[]; + private UndefinedConstants undefinedMFConstants; private Values definedMFConstants; private Values definedPFConstants; @@ -192,10 +193,20 @@ public class PrismCL // sort out properties to check sortProperties(); - // sort out undefined constants + // process info about undefined constants try { - undefinedConstants = new UndefinedConstants(modulesFile, propertiesFile); - undefinedConstants.defineUsingConstSwitch(constSwitch); + // one set of info for model + if (exportlabels) + undefinedMFConstants = new UndefinedConstants(modulesFile, propertiesFile, true); + else + undefinedMFConstants = new UndefinedConstants(modulesFile, null); + undefinedMFConstants.defineUsingConstSwitch(constSwitch); + // and one set of info for each property + undefinedConstants = new UndefinedConstants[numPropertiesToCheck]; + for (i = 0; i < numPropertiesToCheck; i++) { + undefinedConstants[i] = new UndefinedConstants(modulesFile, propertiesFile, propertiesToCheck.get(i)); + undefinedConstants[i].defineUsingConstSwitch(constSwitch); + } } catch (PrismException e) { errorAndExit(e.getMessage()); } @@ -203,13 +214,13 @@ public class PrismCL // initialise storage for results results = new ResultsCollection[numPropertiesToCheck]; for (i = 0; i < numPropertiesToCheck; i++) { - results[i] = new ResultsCollection(undefinedConstants, propertiesToCheck.get(i).getExpression().getResultName()); + results[i] = new ResultsCollection(undefinedConstants[i], propertiesToCheck.get(i).getExpression().getResultName()); } // iterate through as many models as necessary - for (i = 0; i < undefinedConstants.getNumModelIterations(); i++) { + for (i = 0; i < undefinedMFConstants.getNumModelIterations(); i++) { - definedMFConstants = undefinedConstants.getMFConstantValues(); + definedMFConstants = undefinedMFConstants.getMFConstantValues(); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) mainLog.println("\nModel constants: " + definedMFConstants); @@ -228,7 +239,11 @@ public class PrismCL } catch (PrismException e2) { error("Problem storing results"); } - undefinedConstants.iterateModel(); + // iterate to next model + undefinedMFConstants.iterateModel(); + for (i = 0; i < numPropertiesToCheck; i++) { + undefinedConstants[i].iterateModel(); + } continue; } @@ -242,7 +257,11 @@ public class PrismCL } catch (PrismException e) { error(e.getMessage()); } - undefinedConstants.iterateModel(); + // iterate to next model + undefinedMFConstants.iterateModel(); + for (i = 0; i < numPropertiesToCheck; i++) { + undefinedConstants[i].iterateModel(); + } continue; } @@ -280,7 +299,11 @@ public class PrismCL } catch (PrismException e2) { error("Problem storing results"); } - undefinedConstants.iterateModel(); + // iterate to next model + undefinedMFConstants.iterateModel(); + for (i = 0; i < numPropertiesToCheck; i++) { + undefinedConstants[i].iterateModel(); + } continue; } @@ -312,8 +335,8 @@ public class PrismCL if (exportlabels) { try { if (propertiesFile != null) { - definedPFConstants = undefinedConstants.getPFConstantValues(); - propertiesFile.setUndefinedConstants(definedPFConstants); + definedPFConstants = undefinedMFConstants.getPFConstantValues(); + propertiesFile.setSomeUndefinedConstants(definedPFConstants); } File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename); prism.exportLabelsToFile(model, modulesFile, propertiesFile, exportType, f); @@ -331,16 +354,16 @@ public class PrismCL for (j = 0; j < numPropertiesToCheck; j++) { // for simulation we can do multiple values of property constants simultaneously - if (simulate && undefinedConstants.getNumPropertyIterations() > 1) { + if (simulate && undefinedConstants[j].getNumPropertyIterations() > 1) { try { mainLog.println("\n-------------------------------------------"); mainLog.println("\nSimulating: " + propertiesToCheck.get(j)); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) mainLog.println("Model constants: " + definedMFConstants); - mainLog.println("Property constants: " + undefinedConstants.getPFDefinedConstantsString()); + mainLog.println("Property constants: " + undefinedConstants[j].getPFDefinedConstantsString()); simMethod = processSimulationOptions(propertiesToCheck.get(j).getExpression()); - prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants, results[j], propertiesToCheck.get(j).getExpression(), null, + prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants[j], results[j], propertiesToCheck.get(j).getExpression(), null, simMaxPath, simMethod); } catch (PrismException e) { // in case of (overall) error, report it, store as result for property, and proceed @@ -350,7 +373,6 @@ public class PrismCL } catch (PrismException e2) { error("Problem storing results"); } - undefinedConstants.iterateModel(); continue; } catch (InterruptedException e) { // ignore - won't get interrupted @@ -358,13 +380,13 @@ public class PrismCL } // otherwise, treat each case individually else { - for (k = 0; k < undefinedConstants.getNumPropertyIterations(); k++) { + for (k = 0; k < undefinedConstants[j].getNumPropertyIterations(); k++) { try { // set values for PropertiesFile constants if (propertiesFile != null) { - definedPFConstants = undefinedConstants.getPFConstantValues(); - propertiesFile.setUndefinedConstants(definedPFConstants); + definedPFConstants = undefinedConstants[j].getPFConstantValues(); + propertiesFile.setSomeUndefinedConstants(definedPFConstants); } // log output @@ -449,7 +471,7 @@ public class PrismCL } // iterate to next property - undefinedConstants.iterateProperty(); + undefinedConstants[j].iterateProperty(); } } } @@ -460,7 +482,10 @@ public class PrismCL } // iterate to next model - undefinedConstants.iterateModel(); + undefinedMFConstants.iterateModel(); + for (i = 0; i < numPropertiesToCheck; i++) { + undefinedConstants[i].iterateModel(); + } } // export results (if required) diff --git a/prism/src/prism/ResultsCollection.java b/prism/src/prism/ResultsCollection.java index 863c1aa6..e789e0a7 100644 --- a/prism/src/prism/ResultsCollection.java +++ b/prism/src/prism/ResultsCollection.java @@ -62,10 +62,9 @@ public class ResultsCollection resultListeners = new Vector(); rangingConstants = new Vector(); - /* TODO: Fix this when/if getRangingConstants() returns Vector */ - Vector tmpRangingConstants = uCons.getRangingConstants(); + Vector tmpRangingConstants = uCons.getRangingConstants(); for (int i = 0; i < tmpRangingConstants.size(); i++) { - rangingConstants.add((DefinedConstant) tmpRangingConstants.get(i)); + rangingConstants.add(tmpRangingConstants.get(i)); } this.root = (rangingConstants.size() > 0) ? new TreeNode(0) : new TreeLeaf(); diff --git a/prism/src/prism/UndefinedConstants.java b/prism/src/prism/UndefinedConstants.java index 48e2d880..39d21f0c 100644 --- a/prism/src/prism/UndefinedConstants.java +++ b/prism/src/prism/UndefinedConstants.java @@ -26,6 +26,7 @@ package prism; +import java.util.List; import java.util.Vector; import parser.*; @@ -33,7 +34,7 @@ import parser.ast.*; import parser.type.*; /** - * Class to handle the undefined constants in model/properties files. + * Class to handle the undefined constants in model and/or properties file. */ public class UndefinedConstants { @@ -58,21 +59,94 @@ public class UndefinedConstants private Vector constSwitchSteps; /** - * Construct information about undefined constants from a model and, optionally, - * a properties files (in which case th latter is null). + * Construct information about undefined constants from a model and/or properties file. + * If either is not required, it can be left as null. All undefined constants, + * whether used or not, are assumed to be required to be provided. */ public UndefinedConstants(ModulesFile mf, PropertiesFile pf) { - int i; + this(mf, pf, false); + } + + /** + * Construct information about undefined constants from a model and/or properties file. + * If either is not required, it can be left as null. If {@code justLabels} is false, + * all constants, whether used or not, are assumed to be required to be provided. + * If {@code justLabels} is true, only properties file constants that are needed for labels are. + */ + public UndefinedConstants(ModulesFile mf, PropertiesFile pf, boolean justLabels) + { Vector mfv, pfv; - String s; - // store model/properties files modulesFile = mf; propertiesFile = pf; // determine which constants are undefined - mfv = modulesFile.getUndefinedConstants(); + mfv = (modulesFile == null) ? new Vector() : modulesFile.getUndefinedConstants(); pfv = (propertiesFile == null) ? new Vector() : propertiesFile.getUndefinedConstants(); + if (propertiesFile == null) { + pfv = new Vector(); + } else { + if (justLabels) { + pfv = propertiesFile.getUndefinedConstantsUsedInLabels(); + } else { + pfv = propertiesFile.getUndefinedConstants(); + } + } + // create data structures + initialise(mfv, pfv); + } + + /** + * Construct information about undefined constants for a specific property. + * It is assumed that all undefined constants from model file are needed, + * plus any from the properties file that are use in the property {@code prop}. + */ + public UndefinedConstants(ModulesFile mf, PropertiesFile pf, Property prop) + { + Vector mfv, pfv; + // store model/properties files + modulesFile = mf; + propertiesFile = pf; + // determine which constants are undefined + mfv = (modulesFile == null) ? new Vector() : modulesFile.getUndefinedConstants(); + if (propertiesFile == null || prop == null) { + pfv = new Vector(); + } else { + pfv = propertiesFile.getUndefinedConstantsUsedInProperty(prop); + } + // create data structures + initialise(mfv, pfv); + } + + /** + * Construct information about undefined constants for specific properties. + * It is assumed that all undefined constants from model file are needed, + * plus any from the properties file that are use in the properties {@code props}. + */ + public UndefinedConstants(ModulesFile mf, PropertiesFile pf, List props) + { + Vector mfv, pfv; + // store model/properties files + modulesFile = mf; + propertiesFile = pf; + // determine which constants are undefined + mfv = (modulesFile == null) ? new Vector() : modulesFile.getUndefinedConstants(); + if (propertiesFile == null || props == null) { + pfv = new Vector(); + } else { + pfv = propertiesFile.getUndefinedConstantsUsedInProperties(props); + } + // create data structures + initialise(mfv, pfv); + } + + /** + * Set up data structures (as required by constructor methods) + */ + private void initialise(Vector mfv, Vector pfv) + { + int i; + String s; // determine how many constants there are mfNumConsts = mfv.size(); pfNumConsts = pfv.size(); @@ -90,7 +164,7 @@ public class UndefinedConstants // initialise storage just created clearAllDefinitions(); } - + // accessor methods for info about undefined constants public int getMFNumUndefined() { return mfNumConsts; } @@ -135,6 +209,7 @@ public class UndefinedConstants int i; String name; boolean dupe; + boolean useAll = false; // clear any previous definitions clearAllDefinitions(); @@ -143,7 +218,7 @@ public class UndefinedConstants parseConstSwitch(constSwitch); // if there are no undefined consts... - if (mfNumConsts + pfNumConsts == 0) { + if (useAll && (mfNumConsts + pfNumConsts == 0)) { if (constSwitchNames.size() > 0) { throw new PrismException("There are no undefined constants to define"); } @@ -157,7 +232,7 @@ public class UndefinedConstants name = constSwitchNames.elementAt(i); // define constant using info from switch - dupe = defineConstant(name, constSwitchLows.elementAt(i), constSwitchHighs.elementAt(i), constSwitchSteps.elementAt(i)); + dupe = defineConstant(name, constSwitchLows.elementAt(i), constSwitchHighs.elementAt(i), constSwitchSteps.elementAt(i), useAll); // check for duplication if (dupe) { @@ -247,7 +322,7 @@ public class UndefinedConstants */ public boolean defineConstant(String name, String val) throws PrismException { - return defineConstant(name, val, null, null); + return defineConstant(name, val, null, null, false); } /** Define value for a single undefined constant. @@ -259,10 +334,29 @@ public class UndefinedConstants * @param sl If sh are sl are null, this is the value to be assigned. Otherwise, it is the lower bound for the range. * @param sh The upper bound for the range. * @param ss The step for the values. Null means 1. + * @param useAll If true, throw an exception if {@code name} is does not need to be defined * * @return True if the constant was defined before. */ public boolean defineConstant(String name, String sl, String sh, String ss) throws PrismException + { + return defineConstant(name, sl, sh, ss, false); + } + + /** Define value for a single undefined constant. + * Returns whether or not an existing definition was overwritten. + * + * The method {@link #initialiseIterators() initialiseIterators} must be called after all constants are defined. + * + * @param name The name of the constant. + * @param sl If sh are sl are null, this is the value to be assigned. Otherwise, it is the lower bound for the range. + * @param sh The upper bound for the range. + * @param ss The step for the values. Null means 1. + * @param useAll If true, throw an exception if {@code name} is does not need to be defined + * + * @return True if the constant was defined before. + */ + public boolean defineConstant(String name, String sl, String sh, String ss, boolean useAll) throws PrismException { int index = 0; boolean overwrite = false; // did definition exist already? @@ -283,7 +377,8 @@ public class UndefinedConstants pfConsts[index].define(sl, sh, ss); } else { - throw new PrismException("\"" + name + "\" is not an undefined constant"); + if (useAll) + throw new PrismException("\"" + name + "\" is not an undefined constant"); } } diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index a8f3add9..f61b8201 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/prism/src/userinterface/properties/GUIExperiment.java @@ -393,7 +393,7 @@ public class GUIExperiment // set values for PropertiesFile constants if (propertiesFile != null) { definedPFConstants = undefinedConstants.getPFConstantValues(); - propertiesFile.setUndefinedConstants(definedPFConstants); + propertiesFile.setSomeUndefinedConstants(definedPFConstants); } // log output diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index d3e38c31..5aaaacc5 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -207,9 +207,12 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List parsedProperties = getPrism().parsePropertiesString(parsedModel, propertiesString); // And get list of corresponding GUIProperty objects validGUIProperties = propList.getValidSelectedProperties(); - // Query user for undefined constant values (if required) - uCon = new UndefinedConstants(parsedModel, parsedProperties); + int n = parsedProperties.getNumProperties(); + ArrayList validProperties = new ArrayList(n); + for (int i = 0; i < n; i++) + validProperties.add(parsedProperties.getPropertyObject(i)); + uCon = new UndefinedConstants(parsedModel, parsedProperties, validProperties); if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) { // Use previous constant values as defaults in dialog int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, mfConstants, pfConstants); @@ -221,7 +224,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List mfConstants = uCon.getMFConstantValues(); // Store property constants and set in file pfConstants = uCon.getPFConstantValues(); - parsedProperties.setUndefinedConstants(pfConstants); + parsedProperties.setSomeUndefinedConstants(pfConstants); // Store properties to be verified propertiesToBeVerified = validGUIProperties; @@ -268,12 +271,14 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List // See which of the (valid) selected properties are ok for simulation // Also store a list of the expression themselves simulatableGUIProperties = new ArrayList(); + ArrayList simulatableProperties = new ArrayList(); simulatableExprs = new ArrayList(); for (int i = 0; i < validGUIProperties.size(); i++) { GUIProperty guiP = validGUIProperties.get(i); try { getPrism().checkPropertyForSimulation(guiP.getProperty()); simulatableGUIProperties.add(guiP); + simulatableProperties.add(parsedProperties.getPropertyObject(i)); simulatableExprs.add(guiP.getProperty()); } catch (PrismException e) { // do nothing @@ -291,7 +296,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List //find out any undefined constants try { - uCon = new UndefinedConstants(parsedModel, parsedProperties); + uCon = new UndefinedConstants(parsedModel, parsedProperties, simulatableProperties); if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) { // Use previous constant values as defaults in dialog int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, mfConstants, pfConstants); @@ -303,7 +308,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List mfConstants = uCon.getMFConstantValues(); pfConstants = uCon.getPFConstantValues(); parsedModel.setUndefinedConstants(mfConstants); - parsedProperties.setUndefinedConstants(pfConstants); + parsedProperties.setSomeUndefinedConstants(pfConstants); // Get simulation info with dialog SimulationInformation info = GUISimulationPicker.defineSimulationWithDialog(this.getGUI(), simulatableExprs, parsedModel, null); @@ -354,7 +359,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List } // sort out undefined constants - UndefinedConstants uCon = new UndefinedConstants(parsedModel, parsedProperties); + UndefinedConstants uCon = new UndefinedConstants(parsedModel, parsedProperties, parsedProperties.getPropertyObject(0)); boolean showGraphDialog = false; boolean useSimulation = false; if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() == 0) { diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 15bf689d..ee5d1aab 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -283,8 +283,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } // 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); + // (just get contants needed for properties file labels) + UndefinedConstants uCon = new UndefinedConstants(parsedModel, pf, true); if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) { int result = GUIConstantsPicker.defineConstantsWithDialog(gui, uCon, lastConstants, lastPropertyConstants); if (result != GUIConstantsPicker.VALUES_DONE) @@ -295,7 +295,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect lastPropertyConstants = uCon.getPFConstantValues(); // store constants parsedModel.setUndefinedConstants(lastConstants); - pf.setUndefinedConstants(lastPropertyConstants); + pf.setSomeUndefinedConstants(lastPropertyConstants); // check here for possibility of multiple initial states // (not supported yet) to avoid problems below