diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 381e2e1a..b2a01bb7 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/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"); diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index cec62204..bb2c8fba 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/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"); diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index fbb5d887..0081d1ea 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/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) { diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index d4d78687..fbe5ddb8 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/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) { diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index e279298b..6ecfce96 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/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) { diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 1804260e..734ee34e 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/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) { diff --git a/prism/src/parser/EvaluateContextState.java b/prism/src/parser/EvaluateContextState.java index a223fde4..9f25e7c0 100644 --- a/prism/src/parser/EvaluateContextState.java +++ b/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) diff --git a/prism/src/parser/EvaluateContextSubstate.java b/prism/src/parser/EvaluateContextSubstate.java index 00b96caf..b360e2ce 100644 --- a/prism/src/parser/EvaluateContextSubstate.java +++ b/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) diff --git a/prism/src/parser/ParserUtils.java b/prism/src/parser/ParserUtils.java index 2de807c4..88b1c7c0 100644 --- a/prism/src/parser/ParserUtils.java +++ b/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(); - res.add(expr.evaluateInt(constantValues, null)); + res.add(expr.evaluateInt(constantValues)); return res; } diff --git a/prism/src/parser/VarList.java b/prism/src/parser/VarList.java index 04901dd4..b7edf0ce 100644 --- a/prism/src/parser/VarList.java +++ b/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 { diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 0f489e06..e8864e9f 100644 --- a/prism/src/parser/ast/Expression.java +++ b/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 diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 2a680f2c..8a6eafcc 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/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)); } } diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 8bdf9b62..f0b1dad4 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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"); } diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 5bdc6050..d87363dd 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/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"); } diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 4f6f68e2..66ff7c31 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/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) diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index 480aa8c6..bb731e27 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/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"); } diff --git a/prism/src/pta/Modules2PTA.java b/prism/src/pta/Modules2PTA.java index b583a97f..3eb25e14 100644 --- a/prism/src/pta/Modules2PTA.java +++ b/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 diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 1e373600..2cbebb3f 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/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