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

@@ -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<String> getAllUndefinedConstantsRecursively(ConstantList constantList, LabelList labelList)
+	{
+		Vector<String> v= new Vector<String>();
+		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.
 	 */

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;

prism/src/parser/ast/ModulesFile.java

@@ -64,7 +64,7 @@ public class ModulesFile extends ASTElement
 	private Vector<String> varNames;
 	private Vector<Type> 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.
-	 * <br><br>
+	 * 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
 	{

prism/src/parser/ast/PropertiesFile.java

@@ -49,7 +49,7 @@ public class PropertiesFile extends ASTElement
 	// list of all identifiers used
 	private Vector<String> 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<String> 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.
-	 * <br><br>
+	 * 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<String> getUndefinedConstantsUsedInLabels()
+	{
+		int i, n;
+		Expression expr;
+		Vector<String> consts, tmp;
+		consts = new Vector<String>();
+		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<String> 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<String> getUndefinedConstantsUsedInProperties(List <Property> props)
+	{
+		Vector<String> consts, tmp;
+		consts = new Vector<String>();
+		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()
 	{

prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java

@@ -0,0 +1,81 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (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<String> v;
+	private ConstantList constantList;
+	private LabelList labelList;
+	
+	public GetAllUndefinedConstantsRecursively(Vector<String> 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);
+	}
+}
+

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();

prism/src/prism/PrismCL.java

@@ -131,7 +131,8 @@ public class PrismCL
 	private List<Property> 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)

prism/src/prism/ResultsCollection.java

@@ -62,10 +62,9 @@ public class ResultsCollection
 		resultListeners = new Vector<ResultListener>();
 		rangingConstants = new Vector<DefinedConstant>();
 
-		/* TODO: Fix this when/if getRangingConstants() returns Vector<DefinedConstant> */
-		Vector tmpRangingConstants = uCons.getRangingConstants();
+		Vector<DefinedConstant> 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();

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<String> 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<String> 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<String>() : modulesFile.getUndefinedConstants();
 		pfv = (propertiesFile == null) ? new Vector<String>() : propertiesFile.getUndefinedConstants();
+		if (propertiesFile == null) {
+			pfv = new Vector<String>();
+		} 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<String> mfv, pfv;
+		// store model/properties files
+		modulesFile = mf;
+		propertiesFile = pf;
+		// determine which constants are undefined
+		mfv = (modulesFile == null) ? new Vector<String>() : modulesFile.getUndefinedConstants();
+		if (propertiesFile == null || prop == null) {
+			pfv = new Vector<String>();
+		} 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<Property> props)
+	{
+		Vector<String> mfv, pfv;
+		// store model/properties files
+		modulesFile = mf;
+		propertiesFile = pf;
+		// determine which constants are undefined
+		mfv = (modulesFile == null) ? new Vector<String>() : modulesFile.getUndefinedConstants();
+		if (propertiesFile == null || props == null) {
+			pfv = new Vector<String>();
+		} else {
+			pfv = propertiesFile.getUndefinedConstantsUsedInProperties(props);
+		}
+		// create data structures
+		initialise(mfv, pfv);
+	}
+
+	/**
+	 * Set up data structures (as required by constructor methods)
+	 */
+	private void initialise(Vector<String> mfv, Vector<String> 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");
 			}
 		}
 		

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

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<Property> validProperties = new ArrayList<Property>(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<GUIProperty>();
+		ArrayList<Property> simulatableProperties = new ArrayList<Property>();
 		simulatableExprs = new ArrayList<Expression>();
 		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) {

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