From 466d6ab21f37a9d327dfaab64fe7f530a27bc7ba Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 18 Dec 2012 01:05:09 +0000 Subject: [PATCH] Code tidy. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6228 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/TileList.java | 96 +++++++++++++++++------------------ 1 file changed, 47 insertions(+), 49 deletions(-) diff --git a/prism/src/prism/TileList.java b/prism/src/prism/TileList.java index abe5674a..713c2e11 100644 --- a/prism/src/prism/TileList.java +++ b/prism/src/prism/TileList.java @@ -26,70 +26,72 @@ package prism; -import java.text.DecimalFormat; -import java.text.DecimalFormatSymbols; import java.util.ArrayList; -import java.util.HashSet; import java.util.List; import parser.ast.Expression; /** * This class represent a list of tiles which have corners in Pareto points, - * and which represent an underapproximation of the Pareto curve. + * and which represent an under-approximation of the Pareto curve. */ public class TileList { /** - * Threshold for approximation of the pareto curve. + * Threshold for approximation of the Pareto curve. */ private double tolerance; - + /** * This is used when printing the tileList to the user. The information * we need are whether the reward is min (to multiply by -1) and * whether the probability is min (to do 1-value) */ private OpsAndBoundsList opsAndBoundsList; - - public OpsAndBoundsList getOpsAndBoundsList() { + + public OpsAndBoundsList getOpsAndBoundsList() + { return this.opsAndBoundsList; } - + /** * This is where a TileLists are stored to be later retrieved in GUI. * It is a workaround for the fact that Pareto curve can't be * returned in any reasonable way. * * To ensure correct concurrent behaviour, object accessing any stored tile lists - * or elements should synchronize on this object; + * or elements should synchronise on this object; */ protected static List storedTileLists; + public static List getStoredTileLists() { return storedTileLists; } - + /** - * Formulas for X and Y axes (or multiobj formulas) of the corresponding + * Formulas for X and Y axes (or multi-obj formulas) of the corresponding * elements of storedTileLists. */ protected static List storedFormulasX; - protected static List storedFormulasY; - protected static List storedFormulas; + protected static List storedFormulasY; + protected static List storedFormulas; + public static List getStoredFormulasX() { return storedFormulasX; } + public static List getStoredFormulasY() { return storedFormulasY; } + public static List getStoredFormulas() { return storedFormulas; } - + /** Removes all stored tile list and associated formulas */ public static void clearStoredTileLists() { @@ -98,15 +100,14 @@ public class TileList TileList.storedFormulas.clear(); TileList.storedTileLists.clear(); } - - static - { + + static { storedFormulasX = new ArrayList(); storedFormulasY = new ArrayList(); storedFormulas = new ArrayList(); storedTileLists = new ArrayList(); } - + protected int currentProjectionIndex = 0; /** * This list holds all tiles of this TileList. @@ -121,7 +122,7 @@ public class TileList * Dimension of the space, determined from the initial tile. */ protected int dim; - + /** * Creates a new instance of the TileList, originally containing only one * tile, {@code initialTile}. @@ -131,11 +132,11 @@ public class TileList { this.dim = initialTile.cornerPoints.get(0).getDimension(); this.initialTile = initialTile; - this.list = new ArrayList(); + this.list = new ArrayList(); this.list.add(initialTile); this.opsAndBoundsList = opsAndBounds; this.tolerance = tolerance; - + //this is a HACK so that we don't try projections in 2 dimensions. //these are not needed since projections are extremes in 1 dim, //which were done for initial tile @@ -143,9 +144,10 @@ public class TileList this.currentProjectionIndex = 2; } } - + @Override - public String toString() { + public String toString() + { String s = "["; boolean first = true; for (int j = 0; j < this.list.size(); j++) { @@ -171,7 +173,7 @@ public class TileList s += "]"; return s; } - + /** * Returns a weight vector which could yield a new Pareto point when used. * {@code null} is returned if no candidate point exists. @@ -182,7 +184,7 @@ public class TileList { return getFreshRealCandidateHyperplane(); } - + /** * Queries the tiles of this TileList to get a new weight vector which * could yield a new pareto point when used. {@code null} is returned @@ -194,12 +196,11 @@ public class TileList //we have to exhaust the boundaries first while (this.currentProjectionIndex < this.dim) { for (Tile t : list) { - if (!t.isUpperBound(this.currentProjectionIndex) - && t.liesOnBoundary(this.currentProjectionIndex)) { + if (!t.isUpperBound(this.currentProjectionIndex) && t.liesOnBoundary(this.currentProjectionIndex)) { t.hyperplaneSuggested = true; //System.out.println("fresh candidate hyperplane:" + t + "with weight " + Tile.getWeightsForTile(t)); Point ret = Tile.getWeightsForTile(t); - + //We want to make sure we optimize on the boundary, //so we make the point parallel to an axis. But at //the same time we need to make sure it's not zero weight. @@ -211,12 +212,12 @@ public class TileList System.out.println("does not lie on " + this.currentProjectionIndex + " boundary: " + t); }*/ } - + this.currentProjectionIndex++; //System.out.println("Increasing projection index to " + this.currentProjectionIndex); //System.out.println(this.toString()); } - + //now the points inside the quadrant for (Tile t : list) { if (!t.isUpperBound(dim)) { @@ -225,20 +226,20 @@ public class TileList return Tile.getWeightsForTile(t); } } - + return null; } - + /** * Returns the number of different 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 int getNumberOfDifferentPoints() { return this.getPoints().size(); } - + /** * Returns the points that form the tiles of this * TileList. The implementation is rather inefficient and is intended @@ -254,27 +255,24 @@ public class TileList } 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 * "approximation is downward closed" is maintained true. */ - public void addNewPoint(Point point) throws PrismException + public void addNewPoint(Point point) throws PrismException { //first create the projection to the boundary - if (this.currentProjectionIndex < this.dim && - point.getCoord(this.currentProjectionIndex) > 0.0) { + if (this.currentProjectionIndex < this.dim && point.getCoord(this.currentProjectionIndex) > 0.0) { Point projectionPoint = point.clone(); projectionPoint.setCoord(this.currentProjectionIndex, 0.0); splitTilesByPoint(projectionPoint, false); - } - else - { + } else { splitTilesByPoint(point, this.currentProjectionIndex == dim); } } - + /** * Splits the Tiles using the new point. This basically means that * some tiles will be replaced by smaller tiles. Note that this method @@ -287,20 +285,20 @@ public class TileList protected void splitTilesByPoint(Point point, boolean isRealyFoundPoint) throws PrismException { //System.out.println("really processing point " + point); - + ArrayList affectedTiles = new ArrayList(); for (Tile t : this.list) { boolean affected = t.processNewPoint(point, true, this.currentProjectionIndex); if (affected) affectedTiles.add(t); } - + ArrayList allPoints = new ArrayList(); for (Tile t : affectedTiles) { allPoints.addAll(t.cornerPoints); } //System.out.println("allpoints " + allPoints); - + for (Tile t : affectedTiles) { list.remove(t); //System.out.println("removing " + t); @@ -308,10 +306,10 @@ public class TileList //System.out.println("adding " + l); this.list.addAll(l); } - + //System.out.println(this.toString()); - } - + } + /** * returns the dimension of the points in this TileList */