From 9b7737d1cca3e43c22c0f25740552101899d92e6 Mon Sep 17 00:00:00 2001 From: Vojtech Forejt Date: Tue, 22 Dec 2015 13:37:24 +0000 Subject: [PATCH] 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 | 4 ++-- prism/src/prism/NondetModelChecker.java | 20 +++++++---------- prism/src/prism/OpsAndBoundsList.java | 27 ++++++++++++++++++++--- prism/src/prism/Point.java | 21 +++++++++++++----- 4 files changed, 49 insertions(+), 23 deletions(-) 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);