diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 250871e8..2b082ee5 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -268,7 +268,6 @@ public class NondetModelChecker extends NonProbModelChecker Expression[] ltl; DRA[] dra; // State index info - JDDNode ddStateIndex = null; // Misc boolean negateresult = false; int conflictformulae = 0; @@ -277,6 +276,7 @@ public class NondetModelChecker extends NonProbModelChecker // Make sure we are only expected to compute a value for a single state // Assuming yes, determine index of state of interest and build BDD + JDDNode ddStateIndex = null; if (currentFilter == null || !(currentFilter.getOperator() == Filter.FilterOperator.STATE)) throw new PrismException("Multi-objective model checking can only compute values from a single state"); else { @@ -585,21 +585,14 @@ public class NondetModelChecker extends NonProbModelChecker op = (exprProb != null) ? Operator.P_LE : Operator.R_LE; } else throw new PrismException("Multi-objective properties can only contain P/R operators with max/min=? or lower/upper probability bounds"); - // Store probability/rewards bound - Expression pb = (exprProb != null) ? exprProb.getProb() : exprReward.getReward(); - if (pb != null) { - double p = pb.evaluateDouble(constantValues); - if ((exprProb != null) && (p < 0 || p > 1)) - throw new PrismException("Invalid probability bound " + p + " in P operator"); - if ((exprProb == null) && (p < 0)) - throw new PrismException("Invalid reward bound " + p + " in P operator"); - if (exprProb != null && relOp == RelOp.LEQ) - p = 1 - p; - - opsAndBounds.add(opInfo, op, p, stepBound); - } else { - opsAndBounds.add(opInfo, op, -1.0, stepBound); - } + + // Find bound + double p = opInfo.isNumeric() ? -1.0 : opInfo.getBound(); + // Subtract bound from 1 if of the form P<=p + if (opInfo.isProbabilistic() && opInfo.getRelOp().isUpperBound()) + p = 1 - p; + // Store bound + opsAndBounds.add(opInfo, op, p, stepBound); // Now extract targets if (exprProb != null) { diff --git a/prism/src/prism/OpRelOpBound.java b/prism/src/prism/OpRelOpBound.java index e2328930..3cd33962 100644 --- a/prism/src/prism/OpRelOpBound.java +++ b/prism/src/prism/OpRelOpBound.java @@ -22,6 +22,16 @@ public class OpRelOpBound bound = boundObject.doubleValue(); } + public boolean isProbabilistic() + { + return "P".equals(op); + } + + public boolean isReward() + { + return "R".equals(op); + } + public RelOp getRelOp() { return relOp; diff --git a/prism/src/prism/OpsAndBoundsList.java b/prism/src/prism/OpsAndBoundsList.java index 8c20f476..c047b89d 100644 --- a/prism/src/prism/OpsAndBoundsList.java +++ b/prism/src/prism/OpsAndBoundsList.java @@ -256,7 +256,7 @@ public class OpsAndBoundsList } /** - * Returns number of reward operators added so far + * Returns the number of reward (R) operators added so far. */ public int rewardSize() { @@ -264,8 +264,7 @@ public class OpsAndBoundsList } /** - * Returns number of probabilistic operators added so far. - * @return + * Returns the number of probabilistic (P) operators added so far. */ public int probSize() { @@ -273,7 +272,7 @@ public class OpsAndBoundsList } /** - * Returns true if the list contains the operator op + * Returns true if the list contains the operator op. */ public boolean contains(Operator op) { @@ -281,25 +280,27 @@ public class OpsAndBoundsList } /** - * returns the number of min/max operators. - * @return + * Returns the number of numerical (=?) operators. */ public int numberOfNumerical() { int num = 0; - for(Operator op : relOps) { - if (op == Operator.P_MAX - || op == Operator.P_MIN - || op == Operator.R_MAX - || op == Operator.R_MIN) { + for (OpRelOpBound opInfo : opInfos) + if (opInfo.isNumeric()) num++; - } - } return num; } @Override - public String toString() { - return "Quantity bounds: " + this.bounds + "; Step bounds: " + this.stepBounds + "; Operators" + this.relOps; + public String toString() + { + String ret = ""; + for (int i = 0; i < opInfos.size(); i++) { + if (i > 0) + ret += ","; + ret += opInfos.get(i); + ret += stepBounds.get(i); + } + return ret; } }