diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index 5294e4c8..ab22143b 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/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 tmprewards = new ArrayList(1); tmprewards.add(rtarget); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index a47ef344..71605807 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -482,7 +482,7 @@ public class NondetModelChecker extends NonProbModelChecker List transRewardsList = new ArrayList(); List pathFormulas = new ArrayList(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 transRewardsList, - List pathFormulas) throws PrismException + List 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 diff --git a/prism/src/prism/OpsAndBoundsList.java b/prism/src/prism/OpsAndBoundsList.java index 64fee789..782ceefa 100644 --- a/prism/src/prism/OpsAndBoundsList.java +++ b/prism/src/prism/OpsAndBoundsList.java @@ -54,7 +54,7 @@ public class OpsAndBoundsList protected List opInfos; protected List relOps, relOpsProb, relOpsReward; protected List bounds, boundsProb, boundsReward; - protected List stepBounds, stepBoundsProb, stepBoundsReward; + protected List 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(); boundsReward = new ArrayList(); stepBoundsReward = new ArrayList(numObjectives); + origPositionsReward = new ArrayList(numObjectives); + origPositionsProb = new ArrayList(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. diff --git a/prism/src/prism/Point.java b/prism/src/prism/Point.java index 8058f97f..6cea86c2 100644 --- a/prism/src/prism/Point.java +++ b/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);