Re-factoring in multi-objective model checking.

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

prism/src/prism/NondetModelChecker.java

@@ -268,7 +268,6 @@ public class NondetModelChecker extends NonProbModelChecker
 		Expression[] ltl;
 		DRA<BitSet>[] 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) {

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;

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;
 	}
 }