Added new expression evaluation methods (needed for explicit model checker). Unfortunately breaks some existing calls to evaluate(constVals, null) due to ambiguities. Need to replace them with evaluate(constVals).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3254 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/CTMCModelChecker.java

@@ -69,7 +69,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 		// (i.e. if until is of form U<=t)
 		exprTmp = expr.getLowerBound();
 		if (exprTmp != null) {
-			lTime = exprTmp.evaluateDouble(constantValues, null);
+			lTime = exprTmp.evaluateDouble(constantValues);
 			if (lTime < 0) {
 				throw new PrismException("Invalid lower bound " + lTime + " in time-bounded until formula");
 			}
@@ -80,7 +80,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 		// (i.e. if until is of form U>=t)
 		exprTmp = expr.getUpperBound();
 		if (exprTmp != null) {
-			uTime = exprTmp.evaluateDouble(constantValues, null);
+			uTime = exprTmp.evaluateDouble(constantValues);
 			if (uTime < 0 || (uTime == 0 && expr.upperBoundIsStrict())) {
 				String bound = (expr.upperBoundIsStrict() ? "<" : "<=") + uTime;
 				throw new PrismException("Invalid upper bound " + bound + " in time-bounded until formula");

prism/src/explicit/CTMDPModelChecker.java

@@ -48,7 +48,7 @@ public class CTMDPModelChecker extends MDPModelChecker
 		ModelCheckerResult res = null;
 
 		// get info from bounded until
-		uTime = expr.getUpperBound().evaluateDouble(constantValues, null);
+		uTime = expr.getUpperBound().evaluateDouble(constantValues);
 		if (uTime < 0 || (uTime == 0 && expr.upperBoundIsStrict())) {
 			String bound = (expr.upperBoundIsStrict() ? "<" : "<=") + uTime;
 			throw new PrismException("Invalid upper bound " + bound + " in time-bounded until formula");

prism/src/explicit/DTMCModelChecker.java

@@ -95,7 +95,7 @@ public class DTMCModelChecker extends ProbModelChecker
 		ModelCheckerResult res = null;
 
 		// get info from bounded until
-		time = expr.getUpperBound().evaluateInt(constantValues, null);
+		time = expr.getUpperBound().evaluateInt(constantValues);
 		if (expr.upperBoundIsStrict())
 			time--;
 		if (time < 0) {

prism/src/explicit/MDPModelChecker.java

@@ -98,7 +98,7 @@ public class MDPModelChecker extends ProbModelChecker
 		ModelCheckerResult res = null;
 
 		// get info from bounded until
-		time = expr.getUpperBound().evaluateInt(constantValues, null);
+		time = expr.getUpperBound().evaluateInt(constantValues);
 		if (expr.upperBoundIsStrict())
 			time--;
 		if (time < 0) {

prism/src/explicit/ProbModelChecker.java

@@ -151,7 +151,7 @@ public class ProbModelChecker extends StateModelChecker
 		relOp = expr.getRelOp();
 		rb = expr.getReward();
 		if (rb != null) {
-			r = rb.evaluateDouble(constantValues, null);
+			r = rb.evaluateDouble(constantValues);
 			if (r < 0)
 				throw new PrismException("Invalid reward bound " + r + " in R[] formula");
 		}
@@ -182,7 +182,7 @@ public class ProbModelChecker extends StateModelChecker
 		if (rs == null) {
 			rewStruct = modulesFile.getRewardStruct(0);
 		} else if (rs instanceof Expression) {
-			i = ((Expression) rs).evaluateInt(constantValues, null);
+			i = ((Expression) rs).evaluateInt(constantValues);
 			rs = new Integer(i); // for better error reporting below
 			rewStruct = modulesFile.getRewardStruct(i - 1);
 		} else if (rs instanceof String) {

prism/src/explicit/STPGModelChecker.java

@@ -94,7 +94,7 @@ public class STPGModelChecker extends ProbModelChecker
 		ModelCheckerResult res = null;
 
 		// get info from bounded until
-		time = expr.getUpperBound().evaluateInt(constantValues, null);
+		time = expr.getUpperBound().evaluateInt(constantValues);
 		if (expr.upperBoundIsStrict())
 			time--;
 		if (time < 0) {

prism/src/parser/EvaluateContextState.java

@@ -29,20 +29,33 @@ package parser;
 /**
  * Information required to evaluate an expression: a State object.
  * This is basically an array of Objects, indexed according to a model file. 
+ * Optionally values for constants can also be supplied.
  */
 public class EvaluateContextState implements EvaluateContext
 {
+	private Values constantValues;
 	private Object[] varValues;
 
 	public EvaluateContextState(State state)
 	{
+		this.constantValues = null;
+		this.varValues = state.varValues;
+	}
+
+	public EvaluateContextState(Values constantValues, State state)
+	{
+		this.constantValues = constantValues;
 		this.varValues = state.varValues;
 	}
 
 	public Object getConstantValue(String name)
 	{
-		// No constant value stored here
-		return null;
+		if (constantValues == null)
+			return null;
+		int i = constantValues.getIndexOf(name);
+		if (i == -1)
+			return null;
+		return constantValues.getValue(i);
 	}
 
 	public Object getVarValue(String name, int index)

prism/src/parser/EvaluateContextSubstate.java

@@ -30,22 +30,36 @@ package parser;
  * Information required to evaluate an expression: a subset of a State object.
  * More precisely: a State object, indexed over a subset of all variables,
  * and a mapping from indices (over all variables) to this subset (-1 if not in subset). 
+ * Optionally values for constants can also be supplied.
  */
 public class EvaluateContextSubstate implements EvaluateContext
 {
+	private Values constantValues;
 	private Object[] varValues;
 	private int[] varMap;
 
 	public EvaluateContextSubstate(State substate, int[] varMap)
 	{
+		this.constantValues = null;
+		this.varValues = substate.varValues;
+		this.varMap = varMap;
+	}
+
+	public EvaluateContextSubstate(Values constantValues, State substate, int[] varMap)
+	{
+		this.constantValues = constantValues;
 		this.varValues = substate.varValues;
 		this.varMap = varMap;
 	}
 
 	public Object getConstantValue(String name)
 	{
-		// No constant value stored here
-		return null;
+		if (constantValues == null)
+			return null;
+		int i = constantValues.getIndexOf(name);
+		if (i == -1)
+			return null;
+		return constantValues.getValue(i);
 	}
 
 	public Object getVarValue(String name, int index)

prism/src/parser/ParserUtils.java

@@ -95,7 +95,7 @@ public class ParserUtils
 		
 		// For constant expressions, this is easy
 		if (expr.isConstant())
-			return expr.evaluateInt(constantValues, null);
+			return expr.evaluateInt(constantValues);
 		
 		// Get all variables appearing in the expression and all values of them
 		vars = expr.getAllVars();
@@ -124,7 +124,7 @@ public class ParserUtils
 		
 		// For constant expressions, this is easy
 		if (expr.isConstant())
-			return expr.evaluateInt(constantValues, null);
+			return expr.evaluateInt(constantValues);
 		
 		// Get all variables appearing in the expression and all values of them
 		vars = expr.getAllVars();
@@ -154,7 +154,7 @@ public class ParserUtils
 		// For constant expressions, this is easy
 		if (expr.isConstant()) {
 			res = new HashSet<Integer>();
-			res.add(expr.evaluateInt(constantValues, null));
+			res.add(expr.evaluateInt(constantValues));
 			return res;
 		}
 		

prism/src/parser/VarList.java

@@ -145,9 +145,9 @@ public class VarList
 		// Variable is integer
 		if (declType instanceof DeclarationInt) {
 			DeclarationInt intdecl = (DeclarationInt) declType;
-			low = intdecl.getLow().evaluateInt(constantValues, null);
-			high = intdecl.getHigh().evaluateInt(constantValues, null);
-			start = decl.getStartOrDefault().evaluateInt(constantValues, null);
+			low = intdecl.getLow().evaluateInt(constantValues);
+			high = intdecl.getHigh().evaluateInt(constantValues);
+			start = decl.getStartOrDefault().evaluateInt(constantValues);
 			// Check range is valid
 			if (high - low <= 0) {
 				String s = "Invalid range (" + low + "-" + high + ") for variable \"" + decl.getName() + "\"";
@@ -167,7 +167,7 @@ public class VarList
 		else if (declType instanceof DeclarationBool) {
 			low = 0;
 			high = 1;
-			start = (decl.getStartOrDefault().evaluateBoolean(constantValues, null)) ? 1 : 0;
+			start = (decl.getStartOrDefault().evaluateBoolean(constantValues)) ? 1 : 0;
 		}
 		// Otherwise (i.e. clock) create dummy info
 		else {

prism/src/parser/ast/Expression.java

@@ -128,7 +128,27 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression, based on Values for constants/variables; return result.
+	 * Evaluate this expression, using no constant or variable values.
+	 * Note: assumes that type checking has been done already.
+	 */
+	public Object evaluate() throws PrismLangException
+	{
+		return evaluate(new EvaluateContextValues(null, null));
+	}
+
+	/**
+	 * Evaluate this expression, based on values for constants (but not variables).
+	 * Constant values are supplied as a Values object. 
+	 * Note: assumes that type checking has been done already.
+	 */
+	public Object evaluate(Values constantValues) throws PrismLangException
+	{
+		return evaluate(new EvaluateContextValues(constantValues, null));
+	}
+
+	/**
+	 * Evaluate this expression, based on values for constants/variables.
+	 * Each set of values is supplied as a Values object. 
 	 * Note: assumes that type checking has been done already.
 	 */
 	public Object evaluate(Values constantValues, Values varValues) throws PrismLangException
@@ -137,7 +157,8 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression, based on a State object, i.e. array of variable values; return result.
+	 * Evaluate this expression, based on values for variables (but not constants).
+	 * Variable values are supplied as a State object, i.e. array of variable values.
 	 * Note: assumes that constants have been evaluated and type checking has been done.
 	 */
 	public Object evaluate(State state) throws PrismLangException
@@ -146,9 +167,22 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression, based on a State object, indexed over a subset of all variables,
+	 * Evaluate this expression, based on values for constants/variables.
+	 * Constant values are supplied as a Values object. 
+	 * Variable values are supplied as a State object, i.e. array of variable values.
+	 * Note: assumes that type checking has been done.
+	 */
+	public Object evaluate(Values constantValues, State state) throws PrismLangException
+	{
+		return evaluate(new EvaluateContextState(constantValues, state));
+	}
+
+	/**
+	 * Evaluate this expression, based on values for some variables (but not constants).
+	 * Variable values are supplied as a State object, indexed over a subset of all variables,
 	 * and a mapping from indices (over all variables) to this subset (-1 if not in subset).
 	 * If any variables required for evaluation are missing, this will fail with an exception.
+	 * Note: assumes that constants have been evaluated and type checking has been done.
 	 */
 	public Object evaluate(State substate, int[] varMap) throws PrismLangException
 	{
@@ -156,11 +190,16 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression, using no constant or variable values.
+	 * Evaluate this expression, based on values for constants and some variables.
+	 * Constant values are supplied as a Values object. 
+	 * Variable values are supplied as a State object, indexed over a subset of all variables,
+	 * and a mapping from indices (over all variables) to this subset (-1 if not in subset).
+	 * If any variables required for evaluation are missing, this will fail with an exception.
+	 * Note: assumes that type checking has been done.
 	 */
-	public Object evaluate() throws PrismLangException
+	public Object evaluate(Values constantValues, State substate, int[] varMap) throws PrismLangException
 	{
-		return evaluate(new EvaluateContextValues(null, null));
+		return evaluate(new EvaluateContextSubstate(constantValues, substate, varMap));
 	}
 
 	/**
@@ -180,8 +219,31 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as an integer.
+	 * Evaluate this expression as an integer, using no constant or variable values.
+	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1).
+	 * Note: assumes that type checking has been done already.
+	 */
+	public int evaluateInt() throws PrismLangException
+	{
+		return evaluateInt(new EvaluateContextValues(null, null));
+	}
+
+	/**
+	 * Evaluate this expression as an integer, based on values for constants (but not variables).
 	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1).
+	 * Constant values are supplied as a Values object. 
+	 * Note: assumes that type checking has been done already.
+	 */
+	public int evaluateInt(Values constantValues) throws PrismLangException
+	{
+		return evaluateInt(new EvaluateContextValues(constantValues, null));
+	}
+
+	/**
+	 * Evaluate this expression as an integer, based on values for constants/variables.
+	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1).
+	 * Each set of values is supplied as a Values object. 
+	 * Note: assumes that type checking has been done already.
 	 */
 	public int evaluateInt(Values constantValues, Values varValues) throws PrismLangException
 	{
@@ -189,8 +251,10 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as an integer.
+	 * Evaluate this expression as an integer, based on values for variables (but not constants).
 	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1).
+	 * Variable values are supplied as a State object, i.e. array of variable values.
+	 * Note: assumes that constants have been evaluated and type checking has been done.
 	 */
 	public int evaluateInt(State state) throws PrismLangException
 	{
@@ -198,8 +262,24 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as an integer.
+	 * Evaluate this expression as an integer, based on values for constants/variables.
 	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1).
+	 * Constant values are supplied as a Values object. 
+	 * Variable values are supplied as a State object, i.e. array of variable values.
+	 * Note: assumes that type checking has been done.
+	 */
+	public int evaluateInt(Values constantValues, State state) throws PrismLangException
+	{
+		return evaluateInt(new EvaluateContextState(constantValues, state));
+	}
+
+	/**
+	 * Evaluate this expression as an integer, based on values for some variables (but not constants).
+	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1).
+	 * Variable values are supplied as a State object, indexed over a subset of all variables,
+	 * and a mapping from indices (over all variables) to this subset (-1 if not in subset).
+	 * If any variables required for evaluation are missing, this will fail with an exception.
+	 * Note: assumes that constants have been evaluated and type checking has been done.
 	 */
 	public int evaluateInt(State substate, int[] varMap) throws PrismLangException
 	{
@@ -207,12 +287,17 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as an integer.
+	 * Evaluate this expression as an integer, based on values for constants and some variables.
 	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1).
+	 * Constant values are supplied as a Values object. 
+	 * Variable values are supplied as a State object, indexed over a subset of all variables,
+	 * and a mapping from indices (over all variables) to this subset (-1 if not in subset).
+	 * If any variables required for evaluation are missing, this will fail with an exception.
+	 * Note: assumes that type checking has been done.
 	 */
-	public int evaluateInt() throws PrismLangException
+	public int evaluateInt(Values constantValues, State substate, int[] varMap) throws PrismLangException
 	{
-		return evaluateInt(new EvaluateContextValues(null, null));
+		return evaluateInt(new EvaluateContextSubstate(constantValues, substate, varMap));
 	}
 
 	/**
@@ -235,8 +320,31 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as a double.
+	 * Evaluate this expression as a double, using no constant or variable values.
 	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0.0/1.0).
+	 * Note: assumes that type checking has been done already.
+	 */
+	public double evaluateDouble() throws PrismLangException
+	{
+		return evaluateDouble(new EvaluateContextValues(null, null));
+	}
+
+	/**
+	 * Evaluate this expression as a double, based on values for constants (but not variables).
+	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0.0/1.0).
+	 * Constant values are supplied as a Values object. 
+	 * Note: assumes that type checking has been done already.
+	 */
+	public double evaluateDouble(Values constantValues) throws PrismLangException
+	{
+		return evaluateDouble(new EvaluateContextValues(constantValues, null));
+	}
+
+	/**
+	 * Evaluate this expression as a double, based on values for constants/variables.
+	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0.0/1.0).
+	 * Each set of values is supplied as a Values object. 
+	 * Note: assumes that type checking has been done already.
 	 */
 	public double evaluateDouble(Values constantValues, Values varValues) throws PrismLangException
 	{
@@ -244,8 +352,10 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as a double.
+	 * Evaluate this expression as a double, based on values for variables (but not constants).
 	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0.0/1.0).
+	 * Variable values are supplied as a State object, i.e. array of variable values.
+	 * Note: assumes that constants have been evaluated and type checking has been done.
 	 */
 	public double evaluateDouble(State state) throws PrismLangException
 	{
@@ -253,8 +363,24 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as a double.
+	 * Evaluate this expression as a double, based on values for constants/variables.
 	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0.0/1.0).
+	 * Constant values are supplied as a Values object. 
+	 * Variable values are supplied as a State object, i.e. array of variable values.
+	 * Note: assumes that type checking has been done.
+	 */
+	public double evaluateDouble(Values constantValues, State state) throws PrismLangException
+	{
+		return evaluateDouble(new EvaluateContextState(constantValues, state));
+	}
+
+	/**
+	 * Evaluate this expression as a double, based on values for some variables (but not constants).
+	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0.0/1.0).
+	 * Variable values are supplied as a State object, indexed over a subset of all variables,
+	 * and a mapping from indices (over all variables) to this subset (-1 if not in subset).
+	 * If any variables required for evaluation are missing, this will fail with an exception.
+	 * Note: assumes that constants have been evaluated and type checking has been done.
 	 */
 	public double evaluateDouble(State substate, int[] varMap) throws PrismLangException
 	{
@@ -262,12 +388,17 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as a double.
+	 * Evaluate this expression as a double, based on values for constants and some variables.
 	 * Any typing issues cause an exception (but: we do allow conversion of boolean to 0.0/1.0).
+	 * Constant values are supplied as a Values object. 
+	 * Variable values are supplied as a State object, indexed over a subset of all variables,
+	 * and a mapping from indices (over all variables) to this subset (-1 if not in subset).
+	 * If any variables required for evaluation are missing, this will fail with an exception.
+	 * Note: assumes that type checking has been done.
 	 */
-	public double evaluateDouble() throws PrismLangException
+	public double evaluateDouble(Values constantValues, State substate, int[] varMap) throws PrismLangException
 	{
-		return evaluateDouble(new EvaluateContextValues(null, null));
+		return evaluateDouble(new EvaluateContextSubstate(constantValues, substate, varMap));
 	}
 
 	/**
@@ -284,8 +415,31 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as a boolean.
+	 * Evaluate this expression as a boolean, using no constant or variable values.
 	 * Any typing issues cause an exception.
+	 * Note: assumes that type checking has been done already.
+	 */
+	public boolean evaluateBoolean() throws PrismLangException
+	{
+		return evaluateBoolean(new EvaluateContextValues(null, null));
+	}
+
+	/**
+	 * Evaluate this expression as a boolean, based on values for constants (but not variables).
+	 * Any typing issues cause an exception.
+	 * Constant values are supplied as a Values object. 
+	 * Note: assumes that type checking has been done already.
+	 */
+	public boolean evaluateBoolean(Values constantValues) throws PrismLangException
+	{
+		return evaluateBoolean(new EvaluateContextValues(constantValues, null));
+	}
+
+	/**
+	 * Evaluate this expression as a boolean, based on values for constants/variables.
+	 * Any typing issues cause an exception.
+	 * Each set of values is supplied as a Values object. 
+	 * Note: assumes that type checking has been done already.
 	 */
 	public boolean evaluateBoolean(Values constantValues, Values varValues) throws PrismLangException
 	{
@@ -293,8 +447,10 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as a boolean.
+	 * Evaluate this expression as a boolean, based on values for variables (but not constants).
 	 * Any typing issues cause an exception.
+	 * Variable values are supplied as a State object, i.e. array of variable values.
+	 * Note: assumes that constants have been evaluated and type checking has been done.
 	 */
 	public boolean evaluateBoolean(State state) throws PrismLangException
 	{
@@ -302,8 +458,24 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as a boolean.
+	 * Evaluate this expression as a boolean, based on values for constants/variables.
+	 * Any typing issues cause an exception.
+	 * Constant values are supplied as a Values object. 
+	 * Variable values are supplied as a State object, i.e. array of variable values.
+	 * Note: assumes that type checking has been done.
+	 */
+	public boolean evaluateBoolean(Values constantValues, State state) throws PrismLangException
+	{
+		return evaluateBoolean(new EvaluateContextState(constantValues, state));
+	}
+
+	/**
+	 * Evaluate this expression as a boolean, based on values for some variables (but not constants).
 	 * Any typing issues cause an exception.
+	 * Variable values are supplied as a State object, indexed over a subset of all variables,
+	 * and a mapping from indices (over all variables) to this subset (-1 if not in subset).
+	 * If any variables required for evaluation are missing, this will fail with an exception.
+	 * Note: assumes that constants have been evaluated and type checking has been done.
 	 */
 	public boolean evaluateBoolean(State substate, int[] varMap) throws PrismLangException
 	{
@@ -311,12 +483,17 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Evaluate this expression as a boolean.
+	 * Evaluate this expression as a boolean, based on values for constants and some variables.
 	 * Any typing issues cause an exception.
+	 * Constant values are supplied as a Values object. 
+	 * Variable values are supplied as a State object, indexed over a subset of all variables,
+	 * and a mapping from indices (over all variables) to this subset (-1 if not in subset).
+	 * If any variables required for evaluation are missing, this will fail with an exception.
+	 * Note: assumes that type checking has been done.
 	 */
-	public boolean evaluateBoolean() throws PrismLangException
+	public boolean evaluateBoolean(Values constantValues, State substate, int[] varMap) throws PrismLangException
 	{
-		return evaluateBoolean(new EvaluateContextValues(null, null));
+		return evaluateBoolean(new EvaluateContextSubstate(constantValues, substate, varMap));
 	}
 
 	// Static constructors for convenience

prism/src/parser/ast/ModulesFile.java

@@ -802,7 +802,7 @@ public class ModulesFile extends ASTElement
 		n = getNumGlobals();
 		for (i = 0; i < n; i++) {
 			decl = getGlobal(i);
-			initialState.setValue(count++, decl.getStartOrDefault().evaluate(constantValues, null));
+			initialState.setValue(count++, decl.getStartOrDefault().evaluate(constantValues));
 		}
 		n = getNumModules();
 		for (i = 0; i < n; i++) {
@@ -810,7 +810,7 @@ public class ModulesFile extends ASTElement
 			n2 = module.getNumDeclarations();
 			for (j = 0; j < n2; j++) {
 				decl = module.getDeclaration(j);
-				initialState.setValue(count++, decl.getStartOrDefault().evaluate(constantValues, null));
+				initialState.setValue(count++, decl.getStartOrDefault().evaluate(constantValues));
 			}
 		}
 
@@ -840,7 +840,7 @@ public class ModulesFile extends ASTElement
 		n = getNumGlobals();
 		for (i = 0; i < n; i++) {
 			decl = getGlobal(i);
-			values.addValue(decl.getName(), decl.getStartOrDefault().evaluate(constantValues, null));
+			values.addValue(decl.getName(), decl.getStartOrDefault().evaluate(constantValues));
 		}
 		// then add all module variables
 		n = getNumModules();
@@ -849,7 +849,7 @@ public class ModulesFile extends ASTElement
 			n2 = module.getNumDeclarations();
 			for (j = 0; j < n2; j++) {
 				decl = module.getDeclaration(j);
-				values.addValue(decl.getName(), decl.getStartOrDefault().evaluate(constantValues, null));
+				values.addValue(decl.getName(), decl.getStartOrDefault().evaluate(constantValues));
 			}
 		}
 

prism/src/prism/NondetModelChecker.java

@@ -168,7 +168,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		relOp = expr.getRelOp();
 		pb = expr.getProb();
 		if (pb != null) {
-			p = pb.evaluateDouble(constantValues, null);
+			p = pb.evaluateDouble(constantValues);
 			if (p < 0 || p > 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
@@ -244,7 +244,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		relOp = expr.getRelOp();
 		rb = expr.getReward();
 		if (rb != null) {
-			r = rb.evaluateDouble(constantValues, null);
+			r = rb.evaluateDouble(constantValues);
 			if (r < 0)
 				throw new PrismException("Invalid reward bound " + r + " in R operator");
 		}
@@ -256,7 +256,7 @@ public class NondetModelChecker extends NonProbModelChecker
 			stateRewards = model.getStateRewards(0);
 			transRewards = model.getTransRewards(0);
 		} else if (rs instanceof Expression) {
-			i = ((Expression) rs).evaluateInt(constantValues, null);
+			i = ((Expression) rs).evaluateInt(constantValues);
 			rs = new Integer(i); // for better error reporting below
 			stateRewards = model.getStateRewards(i - 1);
 			transRewards = model.getTransRewards(i - 1);
@@ -526,7 +526,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		StateValues probs = null;
 
 		// get info from bounded until
-		time = expr.getUpperBound().evaluateInt(constantValues, null);
+		time = expr.getUpperBound().evaluateInt(constantValues);
 		if (expr.upperBoundIsStrict())
 			time--;
 		if (time < 0) {
@@ -698,7 +698,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		StateValues rewards = null;
 
 		// get info from bounded until
-		time = expr.getUpperBound().evaluateInt(constantValues, null);
+		time = expr.getUpperBound().evaluateInt(constantValues);
 		if (time < 0) {
 			throw new PrismException("Invalid bound " + time + " in instantaneous reward property");
 		}

prism/src/prism/ProbModelChecker.java

@@ -163,7 +163,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		relOp = expr.getRelOp();
 		pb = expr.getProb();
 		if (pb != null) {
-			p = pb.evaluateDouble(constantValues, null);
+			p = pb.evaluateDouble(constantValues);
 			if (p < 0 || p > 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
@@ -232,7 +232,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		relOp = expr.getRelOp();
 		rb = expr.getReward();
 		if (rb != null) {
-			r = rb.evaluateDouble(constantValues, null);
+			r = rb.evaluateDouble(constantValues);
 			if (r < 0)
 				throw new PrismException("Invalid reward bound " + r + " in R[] formula");
 		}
@@ -244,7 +244,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			stateRewards = model.getStateRewards(0);
 			transRewards = model.getTransRewards(0);
 		} else if (rs instanceof Expression) {
-			i = ((Expression) rs).evaluateInt(constantValues, null);
+			i = ((Expression) rs).evaluateInt(constantValues);
 			rs = new Integer(i); // for better error reporting below
 			stateRewards = model.getStateRewards(i - 1);
 			transRewards = model.getTransRewards(i - 1);
@@ -339,7 +339,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		relOp = expr.getRelOp();
 		pb = expr.getProb();
 		if (pb != null) {
-			p = pb.evaluateDouble(constantValues, null);
+			p = pb.evaluateDouble(constantValues);
 			if (p < 0 || p > 1)
 				throw new PrismException("Invalid probability bound " + p + " in S operator");
 		}
@@ -700,7 +700,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		StateValues probs = null;
 
 		// get info from bounded until
-		time = expr.getUpperBound().evaluateInt(constantValues, null);
+		time = expr.getUpperBound().evaluateInt(constantValues);
 		if (expr.upperBoundIsStrict())
 			time--;
 		if (time < 0) {
@@ -818,7 +818,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		StateValues rewards = null;
 
 		// get info from inst reward
-		time = expr.getUpperBound().evaluateInt(constantValues, null);
+		time = expr.getUpperBound().evaluateInt(constantValues);
 		if (time < 0) {
 			throw new PrismException("Invalid time bound " + time + " in cumulative reward formula");
 		}
@@ -849,7 +849,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		StateValues rewards = null;
 
 		// get info from inst reward
-		time = expr.getUpperBound().evaluateInt(constantValues, null);
+		time = expr.getUpperBound().evaluateInt(constantValues);
 		if (time < 0) {
 			throw new PrismException("Invalid bound " + time + " in instantaneous reward property");
 		}

prism/src/prism/StateModelChecker.java

@@ -498,7 +498,7 @@ public class StateModelChecker implements ModelChecker
 			h = varList.getHigh(v);
 			// create dd
 			dd = JDD.Constant(0);
-			i = e2.evaluateInt(constantValues, null);
+			i = e2.evaluateInt(constantValues);
 			switch (op) {
 			case ExpressionBinaryOp.EQ:
 				if (i >= l && i <= h)
@@ -548,7 +548,7 @@ public class StateModelChecker implements ModelChecker
 			h = varList.getHigh(v);
 			// create dd
 			dd = JDD.Constant(0);
-			i = e1.evaluateInt(constantValues, null);
+			i = e1.evaluateInt(constantValues);
 			switch (op) {
 			case ExpressionBinaryOp.EQ:
 				if (i >= l && i <= h)

prism/src/prism/StochModelChecker.java

@@ -98,7 +98,7 @@ public class StochModelChecker extends ProbModelChecker
 		// (i.e. if until is of form U<=t)
 		exprTmp = expr.getLowerBound();
 		if (exprTmp != null) {
-			lTime = exprTmp.evaluateDouble(constantValues, null);
+			lTime = exprTmp.evaluateDouble(constantValues);
 			if (lTime < 0) {
 				throw new PrismException("Invalid lower bound " + lTime + " in time-bounded until formula");
 			}
@@ -109,7 +109,7 @@ public class StochModelChecker extends ProbModelChecker
 		// (i.e. if until is of form U>=t)
 		exprTmp = expr.getUpperBound();
 		if (exprTmp != null) {
-			uTime = exprTmp.evaluateDouble(constantValues, null);
+			uTime = exprTmp.evaluateDouble(constantValues);
 			if (uTime < 0 || (uTime == 0 && expr.upperBoundIsStrict())) {
 				String bound = (expr.upperBoundIsStrict() ? "<" : "<=") + uTime;
 				throw new PrismException("Invalid upper bound " + bound + " in time-bounded until formula");
@@ -242,7 +242,7 @@ public class StochModelChecker extends ProbModelChecker
 		StateValues rewards = null;
 
 		// get info from inst reward
-		time = expr.getUpperBound().evaluateDouble(constantValues, null);
+		time = expr.getUpperBound().evaluateDouble(constantValues);
 		if (time < 0) {
 			throw new PrismException("Invalid time bound " + time + " in cumulative reward formula");
 		}
@@ -273,7 +273,7 @@ public class StochModelChecker extends ProbModelChecker
 		StateValues sr = null, rewards = null;
 
 		// get info from inst reward
-		time = expr.getUpperBound().evaluateDouble(constantValues, null);
+		time = expr.getUpperBound().evaluateDouble(constantValues);
 		if (time < 0) {
 			throw new PrismException("Invalid bound " + time + " in instantaneous reward property");
 		}

prism/src/pta/Modules2PTA.java

@@ -417,7 +417,7 @@ public class Modules2PTA
 				x = pta.getClockIndex(((ExpressionVar) expr1).getName());
 				if (x < 0)
 					throw new PrismLangException("Unknown clock \"" + ((ExpressionVar) expr1).getName() + "\"", expr);
-				v = expr2.evaluateInt(constantValues, null);
+				v = expr2.evaluateInt(constantValues);
 				switch (exprRelOp.getOperator()) {
 				case ExpressionBinaryOp.EQ:
 					res.add(Constraint.buildGeq(x, v));
@@ -446,7 +446,7 @@ public class Modules2PTA
 			x = pta.getClockIndex(((ExpressionVar) expr2).getName());
 			if (x < 0)
 				throw new PrismLangException("Unknown clock \"" + ((ExpressionVar) expr2).getName() + "\"", expr);
-			v = expr1.evaluateInt(constantValues, null);
+			v = expr1.evaluateInt(constantValues);
 			switch (exprRelOp.getOperator()) {
 			case ExpressionBinaryOp.EQ:
 				res.add(Constraint.buildGeq(x, v));
@@ -520,7 +520,7 @@ public class Modules2PTA
 		pcInit = new State(pcNumVars);
 		for (i = 0; i < pcNumVars; i++) {
 			decl = modulesFile.getVarDeclaration(modulesFile.getVarIndex(pcVars.get(i)));
-			pcInit.setValue(i, decl.getStartOrDefault().evaluate(constantValues, null));
+			pcInit.setValue(i, decl.getStartOrDefault().evaluate(constantValues));
 		}
 
 		// Build variable index mapping

prism/src/pta/PTAModelChecker.java

@@ -212,7 +212,7 @@ public class PTAModelChecker
 		if (exprTemp.hasBounds()) {
 			mainLog.println("Modifying PTA to encode time bound from property...");
 			// Get time bound info (is always of form <=T or <T)
-			timeBound = exprTemp.getUpperBound().evaluateInt(constantValues, null);
+			timeBound = exprTemp.getUpperBound().evaluateInt(constantValues);
 			timeBoundStrict = exprTemp.upperBoundIsStrict();
 			// Modify PTA to include time bound; get new target
 			targetLocs = buildTimeBoundIntoPta(pta, targetLocs, timeBound, timeBoundStrict);