Changing an undocumented feature (aka bug) where in the output Pareto curve, probabilistic properties came before reward properties. Now the output respects the order which user gave on input to multi(...)

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

prism/src/prism/MultiObjModelChecker.java

@@ -263,10 +263,10 @@ public class MultiObjModelChecker extends PrismComponent
 					for (int i = 0; i < opsAndBounds.probSize(); i++) {
 						if (opsAndBounds.getProbOperator(i) != Operator.P_MAX) {
 							tmpOpsAndBounds.add(opsAndBounds.getOpRelOpBound(i), opsAndBounds.getProbOperator(i), opsAndBounds.getProbBound(i),
-									opsAndBounds.getProbStepBound(i));
+									opsAndBounds.getProbStepBound(i), i);
 						}
 					}
-					tmpOpsAndBounds.add(new OpRelOpBound("R", RelOp.MAX, -1.0), Operator.R_MAX, -1.0, -1);
+					tmpOpsAndBounds.add(new OpRelOpBound("R", RelOp.MAX, -1.0), Operator.R_MAX, -1.0, -1, opsAndBounds.probSize());
 
 					ArrayList<JDDNode> tmprewards = new ArrayList<JDDNode>(1);
 					tmprewards.add(rtarget);

prism/src/prism/NondetModelChecker.java

@@ -482,7 +482,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		List<JDDNode> transRewardsList = new ArrayList<JDDNode>();
 		List<Expression> pathFormulas = new ArrayList<Expression>(numObjectives);
 		for (int i = 0; i < numObjectives; i++) {
-			extractInfoFromMultiObjectiveOperand((ExpressionQuant) exprs.get(i), opsAndBounds, transRewardsList, pathFormulas);
+			extractInfoFromMultiObjectiveOperand((ExpressionQuant) exprs.get(i), opsAndBounds, transRewardsList, pathFormulas, i);
 		}
 
 		//currently we do 1 numerical subject to booleans, or multiple numericals only 
@@ -667,14 +667,9 @@ public class NondetModelChecker extends NonProbModelChecker
 		if (value instanceof TileList) {
 			if (opsAndBounds.numberOfNumerical() == 2) {			
 				synchronized(TileList.getStoredTileLists()) {
-					//in multi-obj result probs go first, so we have to swap order if needed
-					if (exprs.get(0) instanceof ExpressionReward && exprs.get(1) instanceof ExpressionProb) {
-						TileList.storedFormulasX.add(exprs.get(1));
-						TileList.storedFormulasY.add(exprs.get(0));
-					} else {
-						TileList.storedFormulasX.add(exprs.get(0));
-						TileList.storedFormulasY.add(exprs.get(1));
-					}
+					TileList.storedFormulasX.add(exprs.get(0));
+					TileList.storedFormulasY.add(exprs.get(1));
+
 					TileList.storedFormulas.add(exprs);
 					TileList.storedTileLists.add((TileList) value);
 				}
@@ -702,9 +697,10 @@ public class NondetModelChecker extends NonProbModelChecker
 	 * @param opsAndBounds Where to add info about ops/bounds
 	 * @param transRewardsList Where to add the transition rewards (R operators only)
 	 * @param pathFormulas Where to store the path formulas (for P operators; null for R operators)
+	 * @param origPosition The position (starting from 0) at which this operand occured in the call of multi(...)
 	 */
 	protected void extractInfoFromMultiObjectiveOperand(ExpressionQuant exprQuant, OpsAndBoundsList opsAndBounds, List<JDDNode> transRewardsList,
-			List<Expression> pathFormulas) throws PrismException
+			List<Expression> pathFormulas, int origPosition) throws PrismException
 	{
 		ExpressionProb exprProb = null;
 		ExpressionReward exprReward = null;
@@ -797,7 +793,7 @@ public class NondetModelChecker extends NonProbModelChecker
 			p = 1 - p;
 		}
 		// Store bound
-		opsAndBounds.add(opInfo, op, p, stepBound);
+		opsAndBounds.add(opInfo, op, p, stepBound, origPosition);
 
 		// Finally, extract path formulas
 		if (exprProb != null) {
@@ -817,7 +813,7 @@ public class NondetModelChecker extends NonProbModelChecker
 			acceptingStates = JDD.Or(acceptingStates, set);
 		targetDDs.add(acceptingStates);
 		OpRelOpBound opInfo = new OpRelOpBound("P", RelOp.GEQ, 0.0);
-		opsAndBounds.add(opInfo, Operator.P_GE, 0.0, -1);
+		opsAndBounds.add(opInfo, Operator.P_GE, 0.0, -1, -1);
 	}
 
 	//Prints info about the product model in multi-objective

prism/src/prism/OpsAndBoundsList.java

@@ -54,7 +54,7 @@ public class OpsAndBoundsList
 	protected List<OpRelOpBound> opInfos;
 	protected List<Operator> relOps, relOpsProb, relOpsReward;
 	protected List<Double> bounds,  boundsProb, boundsReward;
-	protected List<Integer> stepBounds,  stepBoundsProb, stepBoundsReward;
+	protected List<Integer> stepBounds,  stepBoundsProb, stepBoundsReward, origPositionsReward, origPositionsProb;
 	
 	/**
 	 * The default constructor which allocates the lists with size 1.
@@ -82,6 +82,8 @@ public class OpsAndBoundsList
 		relOpsReward = new ArrayList<Operator>();
 		boundsReward = new ArrayList<Double>();
 		stepBoundsReward = new ArrayList<Integer>(numObjectives);
+		origPositionsReward = new ArrayList<Integer>(numObjectives);
+		origPositionsProb = new ArrayList<Integer>(numObjectives);
 	}
 	
 	/**
@@ -89,14 +91,15 @@ public class OpsAndBoundsList
 	 * @param op
 	 * @param quantityBound
 	 * @param stepBound
+	 * @param origPosition What was the position of this operator in the user's call to the multi(...) function.
 	 */
-	public void add(OpRelOpBound opInfo, Operator op, double quantityBound, int stepBound)
+	public void add(OpRelOpBound opInfo, Operator op, double quantityBound, int stepBound, int origPosition)
 	{
 		opInfos.add(opInfo);
 		relOps.add(op);
 		bounds.add(quantityBound);
 		stepBounds.add(stepBound);
-		
+
 		switch (op)
 		{
 			case P_MAX:
@@ -106,6 +109,7 @@ public class OpsAndBoundsList
 				relOpsProb.add(op);
 				boundsProb.add(quantityBound);
 				stepBoundsProb.add(stepBound);
+				origPositionsProb.add(origPosition);
 				break;
 			case R_MAX:
 			case R_MIN:
@@ -114,12 +118,29 @@ public class OpsAndBoundsList
 				relOpsReward.add(op);
 				boundsReward.add(quantityBound);
 				stepBoundsReward.add(stepBound);
+				origPositionsReward.add(origPosition);
 				break;
 			default:
 				throw new UnsupportedOperationException("Don't know how to add" +
 						" operator " + op + ", the handling code does not exist.");
 		}
 	}
+
+	/**
+	 * Returns the original position (starting from 0) of the operator that is now at i-th position among the reward properties.
+	 */
+	public int getOrigPositionReward(int i)
+	{
+		return origPositionsReward.get(i);
+	}
+
+	/**
+	 * Returns the original position (starting from 0) of the operator that is now at i-th position among the probabilistic properties.
+	 */
+	public int getOrigPositionProb(int i)
+	{
+		return origPositionsProb.get(i);
+	}
 	
 	/**
 	 * Returns the operator at i-th position.

prism/src/prism/Point.java

@@ -263,25 +263,34 @@ public class Point
 
 	/**
 	 *  This methods ensures that the point's values corresponds to the properties
-	 *  the user did input. Namely, when the rewards were minimizing, the value
+	 *  the user did input. Namely, (i) the order of properties is restored, and
+	 *  (ii) when the rewards were minimizing, the value
 	 *  is multiplied by -1, and when the probabilities were minimizing,
 	 *  a new value is obtained by 1-value.
 	 * @return
 	 */
 	public Point toRealProperties(OpsAndBoundsList obl)
 	{
-		double[] newCoords = coords.clone();
+		double[] oldCoords = coords.clone();
+		double[] newCoords = new double[oldCoords.length];
 
 		for (int i = 0; i < obl.probSize(); i++) {
-			if (obl.isProbNegated(i)) {
-				newCoords[i] = 1-newCoords[i];
-			}
+			int newIndex = obl.getOrigPositionProb(i);
+			if (obl.isProbNegated(i))
+				newCoords[newIndex] = 1-oldCoords[i];
+			else
+				newCoords[newIndex] = oldCoords[i];
+
 		}
 
 		for (int i = 0; i < obl.rewardSize(); i++) {
+			int newIndex = obl.getOrigPositionReward(i);
 			if (obl.getRewardOperator(i) == Operator.R_MIN
 					|| obl.getRewardOperator(i) == Operator.R_LE)
-				newCoords[i + obl.probSize()] = -newCoords[i + obl.probSize()];			
+				newCoords[newIndex] = -oldCoords[i + obl.probSize()];			
+			else
+				newCoords[newIndex] = oldCoords[i + obl.probSize()];			
+
 		}
 		
 		return new Point(newCoords);