Browse Source

Code tidy.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6228 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
commit
466d6ab21f
  1. 96
      prism/src/prism/TileList.java

96
prism/src/prism/TileList.java

@ -26,70 +26,72 @@
package prism; package prism;
import java.text.DecimalFormat;
import java.text.DecimalFormatSymbols;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.HashSet;
import java.util.List; import java.util.List;
import parser.ast.Expression; import parser.ast.Expression;
/** /**
* This class represent a list of tiles which have corners in Pareto points, * 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 public class TileList
{ {
/** /**
* Threshold for approximation of the pareto curve.
* Threshold for approximation of the Pareto curve.
*/ */
private double tolerance; private double tolerance;
/** /**
* This is used when printing the tileList to the user. The information * 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 * we need are whether the reward is min (to multiply by -1) and
* whether the probability is min (to do 1-value) * whether the probability is min (to do 1-value)
*/ */
private OpsAndBoundsList opsAndBoundsList; private OpsAndBoundsList opsAndBoundsList;
public OpsAndBoundsList getOpsAndBoundsList() {
public OpsAndBoundsList getOpsAndBoundsList()
{
return this.opsAndBoundsList; return this.opsAndBoundsList;
} }
/** /**
* This is where a TileLists are stored to be later retrieved in GUI. * 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 * It is a workaround for the fact that Pareto curve can't be
* returned in any reasonable way. * returned in any reasonable way.
* *
* To ensure correct concurrent behaviour, object accessing any stored tile lists * 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<TileList> storedTileLists; protected static List<TileList> storedTileLists;
public static List<TileList> getStoredTileLists() public static List<TileList> getStoredTileLists()
{ {
return storedTileLists; 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. * elements of storedTileLists.
*/ */
protected static List<Expression> storedFormulasX; protected static List<Expression> storedFormulasX;
protected static List<Expression> storedFormulasY;
protected static List<Expression> storedFormulas;
protected static List<Expression> storedFormulasY;
protected static List<Expression> storedFormulas;
public static List<Expression> getStoredFormulasX() public static List<Expression> getStoredFormulasX()
{ {
return storedFormulasX; return storedFormulasX;
} }
public static List<Expression> getStoredFormulasY() public static List<Expression> getStoredFormulasY()
{ {
return storedFormulasY; return storedFormulasY;
} }
public static List<Expression> getStoredFormulas() public static List<Expression> getStoredFormulas()
{ {
return storedFormulas; return storedFormulas;
} }
/** Removes all stored tile list and associated formulas */ /** Removes all stored tile list and associated formulas */
public static void clearStoredTileLists() public static void clearStoredTileLists()
{ {
@ -98,15 +100,14 @@ public class TileList
TileList.storedFormulas.clear(); TileList.storedFormulas.clear();
TileList.storedTileLists.clear(); TileList.storedTileLists.clear();
} }
static
{
static {
storedFormulasX = new ArrayList<Expression>(); storedFormulasX = new ArrayList<Expression>();
storedFormulasY = new ArrayList<Expression>(); storedFormulasY = new ArrayList<Expression>();
storedFormulas = new ArrayList<Expression>(); storedFormulas = new ArrayList<Expression>();
storedTileLists = new ArrayList<TileList>(); storedTileLists = new ArrayList<TileList>();
} }
protected int currentProjectionIndex = 0; protected int currentProjectionIndex = 0;
/** /**
* This list holds all tiles of this TileList. * This list holds all tiles of this TileList.
@ -121,7 +122,7 @@ public class TileList
* Dimension of the space, determined from the initial tile. * Dimension of the space, determined from the initial tile.
*/ */
protected int dim; protected int dim;
/** /**
* Creates a new instance of the TileList, originally containing only one * Creates a new instance of the TileList, originally containing only one
* tile, {@code initialTile}. * tile, {@code initialTile}.
@ -131,11 +132,11 @@ public class TileList
{ {
this.dim = initialTile.cornerPoints.get(0).getDimension(); this.dim = initialTile.cornerPoints.get(0).getDimension();
this.initialTile = initialTile; this.initialTile = initialTile;
this.list = new ArrayList<Tile>();
this.list = new ArrayList<Tile>();
this.list.add(initialTile); this.list.add(initialTile);
this.opsAndBoundsList = opsAndBounds; this.opsAndBoundsList = opsAndBounds;
this.tolerance = tolerance; this.tolerance = tolerance;
//this is a HACK so that we don't try projections in 2 dimensions. //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, //these are not needed since projections are extremes in 1 dim,
//which were done for initial tile //which were done for initial tile
@ -143,9 +144,10 @@ public class TileList
this.currentProjectionIndex = 2; this.currentProjectionIndex = 2;
} }
} }
@Override @Override
public String toString() {
public String toString()
{
String s = "["; String s = "[";
boolean first = true; boolean first = true;
for (int j = 0; j < this.list.size(); j++) { for (int j = 0; j < this.list.size(); j++) {
@ -171,7 +173,7 @@ public class TileList
s += "]"; s += "]";
return s; return s;
} }
/** /**
* Returns a weight vector which could yield a new Pareto point when used. * Returns a weight vector which could yield a new Pareto point when used.
* {@code null} is returned if no candidate point exists. * {@code null} is returned if no candidate point exists.
@ -182,7 +184,7 @@ public class TileList
{ {
return getFreshRealCandidateHyperplane(); return getFreshRealCandidateHyperplane();
} }
/** /**
* Queries the tiles of this TileList to get a new weight vector which * 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 * 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 //we have to exhaust the boundaries first
while (this.currentProjectionIndex < this.dim) { while (this.currentProjectionIndex < this.dim) {
for (Tile t : list) { 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; t.hyperplaneSuggested = true;
//System.out.println("fresh candidate hyperplane:" + t + "with weight " + Tile.getWeightsForTile(t)); //System.out.println("fresh candidate hyperplane:" + t + "with weight " + Tile.getWeightsForTile(t));
Point ret = Tile.getWeightsForTile(t); Point ret = Tile.getWeightsForTile(t);
//We want to make sure we optimize on the boundary, //We want to make sure we optimize on the boundary,
//so we make the point parallel to an axis. But at //so we make the point parallel to an axis. But at
//the same time we need to make sure it's not zero weight. //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); System.out.println("does not lie on " + this.currentProjectionIndex + " boundary: " + t);
}*/ }*/
} }
this.currentProjectionIndex++; this.currentProjectionIndex++;
//System.out.println("Increasing projection index to " + this.currentProjectionIndex); //System.out.println("Increasing projection index to " + this.currentProjectionIndex);
//System.out.println(this.toString()); //System.out.println(this.toString());
} }
//now the points inside the quadrant //now the points inside the quadrant
for (Tile t : list) { for (Tile t : list) {
if (!t.isUpperBound(dim)) { if (!t.isUpperBound(dim)) {
@ -225,20 +226,20 @@ public class TileList
return Tile.getWeightsForTile(t); return Tile.getWeightsForTile(t);
} }
} }
return null; return null;
} }
/** /**
* Returns the number of different points that form the tiles of this * Returns the number of different points that form the tiles of this
* TileList. The implementation is rather inefficient and is intended * TileList. The implementation is rather inefficient and is intended
* only for debugging pusposes.
* only for debugging purposes.
*/ */
public int getNumberOfDifferentPoints() public int getNumberOfDifferentPoints()
{ {
return this.getPoints().size(); return this.getPoints().size();
} }
/** /**
* Returns the points that form the tiles of this * Returns the points that form the tiles of this
* TileList. The implementation is rather inefficient and is intended * TileList. The implementation is rather inefficient and is intended
@ -254,27 +255,24 @@ public class TileList
} }
return a; return a;
} }
/** /**
* Adds a newly discovered point to this TileList. This basically means that * 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 * some tiles will be split into smaller tiles. Also makes sure that the invariant
* "approximation is downward closed" is maintained true. * "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 //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(); Point projectionPoint = point.clone();
projectionPoint.setCoord(this.currentProjectionIndex, 0.0); projectionPoint.setCoord(this.currentProjectionIndex, 0.0);
splitTilesByPoint(projectionPoint, false); splitTilesByPoint(projectionPoint, false);
}
else
{
} else {
splitTilesByPoint(point, this.currentProjectionIndex == dim); splitTilesByPoint(point, this.currentProjectionIndex == dim);
} }
} }
/** /**
* Splits the Tiles using the new point. This basically means that * Splits the Tiles using the new point. This basically means that
* some tiles will be replaced by smaller tiles. Note that this method * 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 protected void splitTilesByPoint(Point point, boolean isRealyFoundPoint) throws PrismException
{ {
//System.out.println("really processing point " + point); //System.out.println("really processing point " + point);
ArrayList<Tile> affectedTiles = new ArrayList<Tile>(); ArrayList<Tile> affectedTiles = new ArrayList<Tile>();
for (Tile t : this.list) { for (Tile t : this.list) {
boolean affected = t.processNewPoint(point, true, this.currentProjectionIndex); boolean affected = t.processNewPoint(point, true, this.currentProjectionIndex);
if (affected) if (affected)
affectedTiles.add(t); affectedTiles.add(t);
} }
ArrayList<Point> allPoints = new ArrayList<Point>(); ArrayList<Point> allPoints = new ArrayList<Point>();
for (Tile t : affectedTiles) { for (Tile t : affectedTiles) {
allPoints.addAll(t.cornerPoints); allPoints.addAll(t.cornerPoints);
} }
//System.out.println("allpoints " + allPoints); //System.out.println("allpoints " + allPoints);
for (Tile t : affectedTiles) { for (Tile t : affectedTiles) {
list.remove(t); list.remove(t);
//System.out.println("removing " + t); //System.out.println("removing " + t);
@ -308,10 +306,10 @@ public class TileList
//System.out.println("adding " + l); //System.out.println("adding " + l);
this.list.addAll(l); this.list.addAll(l);
} }
//System.out.println(this.toString()); //System.out.println(this.toString());
}
}
/** /**
* returns the dimension of the points in this TileList * returns the dimension of the points in this TileList
*/ */

Loading…
Cancel
Save