Added capability for testing Pareto curves (no tests added yet, and the Pareto curve generation itself is still buggy)

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

prism/src/parser/ast/Property.java

@@ -27,6 +27,8 @@
 package parser.ast;
 
 import java.util.HashMap;
+import java.util.List;
+import java.util.ArrayList;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
@@ -38,6 +40,8 @@ import prism.PrismException;
 import prism.PrismLangException;
 import prism.PrismNotSupportedException;
 import prism.PrismUtils;
+import prism.Point;
+import prism.TileList;
 
 /**
  * PRISM property, i.e. a PRISM expression plus other (optional info) such as name, comment, etc.
@@ -380,6 +384,62 @@ public class Property extends ASTElement
 			if (!rationalRes.equals(rationalExp))
 				throw new PrismException("Wrong result (expected " + rationalExp + ", got " + rationalRes + ")");
 		}
+		else if (type instanceof TypeVoid && result instanceof TileList) { //Pareto curve
+
+			//Create the list of points from the expected results
+			List<Point> liExpected = new ArrayList<Point>();
+			Pattern p = Pattern.compile("\\(([^,]*),([^)]*)\\)");
+			Matcher m = p.matcher(strExpected);
+			if (!m.find()) {
+				throw new PrismException("The expected result does not contain any points, or does not have the required format.");
+			}
+			
+			do {
+				double x = Double.parseDouble(m.group(1));
+				double y = Double.parseDouble(m.group(2));
+				Point point = new Point(new double[] {x,y});
+				liExpected.add(point);
+			} while(m.find());
+
+			List<Point> liResult = ((TileList) result).getRealPoints();
+			System.out.println("a: " + liExpected.toString());
+			System.out.println("b: " + liResult.toString());
+
+			if (liResult.size() != liExpected.size())
+				throw new PrismException("The expected Pareto curve and the computed Pareto curve have a different number of points.");
+
+			//check if we can find a matching point for every point on the expected Pareto curve
+			for(Point point : liExpected) {
+				boolean foundClose = false;
+				for(Point point2 : liResult) {
+					if (point2.isCloseTo(point)) {
+						foundClose = true;
+						break;
+					}
+				}
+				if (!foundClose)
+				{
+					throw new PrismException("The point " + point + " in the expected Pareto curve has no match among the points in the computed Pareto curve.");
+				}
+			}
+
+			//check if we can find a matching point for every point on the computed Pareto curve
+			//(we did check if both lists have the same number of points, but that does
+			//not rule out the possibility of two very similar points contained in one list)
+			for(Point point : liResult) {
+				boolean foundClose = false;
+				for(Point point2 : liExpected) {
+					if (point2.isCloseTo(point)) {
+						foundClose = true;
+						break;
+					}
+				}
+				if (!foundClose)
+				{
+					throw new PrismException("The point " + point + " in the computed Pareto curve has no match among the points in the expected Pareto curve");
+				}
+			}
+		}
 		
 		// Unknown type
 		else {

prism/src/prism/TileList.java

@@ -148,27 +148,27 @@ public class TileList
 	@Override
 	public String toString()
 	{
+		List<Point> li = getPoints();
+
 		String s = "[";
 		boolean first = true;
-		for (int j = 0; j < this.list.size(); j++) {
-			Tile t = this.list.get(j);
-			for (Point p : t.cornerPoints) {
-				// 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 += ",\n";
-				s += "(";
-				for (int i = 0; i < p.getDimension(); i++) {
-					if (i > 0)
-						s += ",";
-					s += p.getCoord(i);
-				}
-				s += ")";
+
+		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;
@@ -243,7 +243,7 @@ public class TileList
 	/**
 	 * Returns the points that form the tiles of this
 	 * TileList. The implementation is rather inefficient and is intended
-	 * only for debugging pusposes.
+	 * only for debugging purposes.
 	 */
 	public List<Point> getPoints()
 	{
@@ -256,6 +256,24 @@ public class TileList
 		return a;
 	}
 
+	/**
+	 * Returns the points that form the actual Pareto curve (modifying the points from tiles
+	 * according to the operator bound changes).
+	 * The implementation is rather inefficient and is intended
+	 * only for debugging purposes.
+	 */
+	public List<Point> getRealPoints()
+	{
+		List<Point> a = this.getPoints();
+		if (this.opsAndBoundsList != null) {
+			for (int i = 0; i < a.size(); i++) {
+				Point p = a.get(i).toRealProperties(this.opsAndBoundsList);
+				a.set(i,p);
+			}
+		}
+		return a;
+	}
+
 	/**
 	 * Adds a newly discovered point to this TileList. This basically means that
 	 * some tiles will be split into smaller tiles. Also makes sure that the invariant