diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java index 0e5efd39..65ee4a50 100644 --- a/prism/src/parser/ast/Property.java +++ b/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 liExpected = new ArrayList(); + 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 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 { diff --git a/prism/src/prism/TileList.java b/prism/src/prism/TileList.java index a5f93c85..09be9755 100644 --- a/prism/src/prism/TileList.java +++ b/prism/src/prism/TileList.java @@ -148,27 +148,27 @@ public class TileList @Override public String toString() { + List 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 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 getRealPoints() + { + List 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