diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index a7926753..e89b8abf 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -742,6 +742,7 @@ public class MultiObjModelChecker extends PrismComponent protected TileList generateParetoCurve(NondetModel modelProduct, JDDNode yes_ones, JDDNode maybe, final JDDNode st, JDDNode[] targets, List rewards, OpsAndBoundsList opsAndBounds) throws PrismException { + //TODO this method does not work for more than 2 objectives int numberOfPoints = 0; int rewardStepBounds[] = new int[rewards.size()]; for (int i = 0; i < rewardStepBounds.length; i++) diff --git a/prism/src/prism/Point.java b/prism/src/prism/Point.java index 2a9a15ba..8058f97f 100644 --- a/prism/src/prism/Point.java +++ b/prism/src/prism/Point.java @@ -148,6 +148,25 @@ public class Point return true; } + /** + * Determines if this point is pointwise smaller than {@code p+SMALL_NUMBER}. + * + */ + public boolean isCoveredBy(Point p) + { + if (p.getDimension() != this.getDimension()) + return false; + + for (int i = 0; i < this.getDimension(); i++) { + if (p.getCoord(i) + SMALL_NUMBER - this.getCoord(i) < 0) + return false; + } + //System.err.println("comparing " + this + " and " + second + " with the result " + (x == second.getX() && y == second.getY())); + return true; + } + + + /** * Returns the point in which the coordinates are reweighted so that the * norm of the point is equal to 1. @@ -278,4 +297,4 @@ public class Point return false; return true; } -} \ No newline at end of file +} diff --git a/prism/src/prism/Tile.java b/prism/src/prism/Tile.java index 03c71ea8..f3e94046 100644 --- a/prism/src/prism/Tile.java +++ b/prism/src/prism/Tile.java @@ -253,20 +253,19 @@ public class Tile double[][] d = new double [dim][dim]; double[] b = new double [dim]; - for (int j = 0; j < dim; j++) { + Point pFixed = t.cornerPoints.get(dim-1); + for (int j = 0; j < dim-1; j++) { Point p = t.cornerPoints.get(j); - //Zero points are problem, we change them while preserving the hyperplane. - if (p.isZero()) { - for (int i = 0; i < dim; i++) { - d[j][i] = t.cornerPoints.get(nonzeroIndex).getCoord(i); - } - } else { - for (int i = 0; i < dim; i++) { - d[j][i] = p.getCoord(i); - } + for (int i = 0; i < dim; i++) { + d[j][i] = p.getCoord(i) - pFixed.getCoord(i); } - b[j] = 1; + b[j] = 0; + } + + for (int i = 0; i < dim; i++) { + d[dim-1][i] = 1; } + b[dim-1] = 1; double[] ret = MultiObjUtils.solveEqns(d, b); double[] pointCoords = new double[dim]; diff --git a/prism/src/prism/TileList.java b/prism/src/prism/TileList.java index 09be9755..58200b50 100644 --- a/prism/src/prism/TileList.java +++ b/prism/src/prism/TileList.java @@ -148,30 +148,8 @@ public class TileList @Override public String toString() { - List li = getPoints(); - - String s = "["; - boolean first = true; - - for (Point p : li) { - // We want to print the user-readable values if possible - if (this.opsAndBoundsList != null) { - p = p.toRealProperties(this.opsAndBoundsList); - } - if (first) - first = false; - else - s += ","; - s += "("; - for (int i = 0; i < p.getDimension(); i++) { - if (i > 0) - s += ","; - s += p.getCoord(i); - } - s += ")"; - } - s += "]"; - return s; + List li = getRealPoints(); + return li.toString(); } /** @@ -256,6 +234,42 @@ public class TileList return a; } + /** + * Returns the points that form the tiles of this + * TileList, omitting the points that are covered by other points. + * The implementation is rather inefficient and is intended + * only for debugging purposes. + */ + public List getPointsWithoutCovered() + { + List a = getPoints(); + + boolean changed; + do { + changed = false; + for (int i = 0; i < a.size(); i++) { + boolean covered = false; + for (int j = 0; j < a.size(); j++) { + if (i==j) + continue; + if (a.get(i).isCoveredBy(a.get(j))) { + covered = true; + break; + } + } + if (covered) { + a.remove(i); + changed = true; + break; + } + } + + + } while(changed); + + return a; + } + /** * Returns the points that form the actual Pareto curve (modifying the points from tiles * according to the operator bound changes). @@ -264,7 +278,7 @@ public class TileList */ public List getRealPoints() { - List a = this.getPoints(); + List a = this.getPointsWithoutCovered(); if (this.opsAndBoundsList != null) { for (int i = 0; i < a.size(); i++) { Point p = a.get(i).toRealProperties(this.opsAndBoundsList);