Bugfix for a case when the Pareto curve for minimising objectives contained (0,0) and the direction for a new hyperplane was not correctly computed

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

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<JDDNode> 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++)

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

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

prism/src/prism/TileList.java

@@ -148,30 +148,8 @@ public class TileList
 	@Override
 	public String toString()
 	{
-		List<Point> 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<Point> 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<Point> getPointsWithoutCovered()
+	{
+		List<Point> 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<Point> getRealPoints()
 	{
-		List<Point> a = this.getPoints();
+		List<Point> a = this.getPointsWithoutCovered();
 		if (this.opsAndBoundsList != null) {
 			for (int i = 0; i < a.size(); i++) {
 				Point p = a.get(i).toRealProperties(this.opsAndBoundsList);