import javax.swing.*; import java.awt.*; // // Grid.java // public class Grid extends JPanel { // OVERVIEW: A Grid is a 2-dimensional grid. Each square in the grid is either // empty or contains a SimObject object. // // A typical Grid is: [ [ s_0_ymax - 1, s_1_ymax - 1, ..., s_xmax - 1_ymax - 1 ], // ... , // [ s_0_1, s_1_1, ..., s_xmax - 1_1], // [ s_0_0, s_1_0, ..., s_xmax - 1_0] ] // // Where each s_x_y is either a SimObject object or is empty. // /*@spec_public@*/ protected int xsize; //@invariant xsize > 0; /*@spec_public@*/ protected int ysize; //@invariant ysize > 0; /*@non_null@*/ SimObject[][] simobjects; // invariant // simobjects.length == x_max; // forall 0 <= i < x_max, simobjects[i].length == y_max; // simobjects[x][y] == null // or simobjects[x][y].getX() == x && simobjects[x][y].getY() == y //@invariant simobjects != null; //@invariant simobjects.length == xsize; //@invariant (\forall int i; (0 <= i && i < xsize) ==> (simobjects[i] != null)); //@invariant (\forall int i; (0 <= i && i < xsize) ==> (simobjects[i].length == ysize)); Grid(int p_xsize, int p_ysize) //@requires p_xsize > 0; //@requires p_ysize > 0; // EFFECTS: Constructs a new grid with the specified maximum x and y // values. { xsize = p_xsize; ysize = p_ysize; simobjects = new SimObject[xsize][ysize]; } public int numHorizontal() // EFFECTS: Returns the number of horizontal squares in this. //@ensures \result == xsize; { return xsize; } public int numVertical() // EFFECTS: Returns the number of vertical squares in this. //@ensures \result == ysize; { return ysize; } private int getSquareWidth() //@ensures \result > 0 { int swidth = getWidth() / numHorizontal(); if (swidth > 0) { return swidth; } else { return 1; } } private int getSquareHeight() //@ensures \result > 0 { int sheight = getHeight() / numVertical(); if (sheight > 0) { return sheight; } else { return 1; } } private int getHorizontalOffset() { return (getWidth() - (getSquareWidth() * numHorizontal())) / 2; } private int getVerticalOffset() { return (getHeight() - (getSquareHeight() * numVertical())) / 2; } synchronized public void setObjectAt(int x, int y, SimObject newObject) throws BadLocationException //@requires newObject != null //@requires x >= 0 && x < xsize //@requires y >= 0 && y < ysize // EFFECTS: places newObject on the grid at location (x,y) (replacing any // object currently on the grid at that location). { //@nowarn Deadlock if (validLocation (x, y)) { simobjects[x][y] = newObject; //@nowarn ArrayStore } else { throw new BadLocationException ("" + x + ", " + y); } } //@nowarn Exception synchronized public void setObjectAt(Coordinate coord, SimObject newObject) throws BadLocationException //@requires coord != null //@requires newObject != null //@requires !newObject.isInitialized //@requires coord.x >= 0 && coord.x < xsize && coord.y >= 0 && coord.y < ysize // REQUIRES: newObject is not initialized // EFFECTS: If coord is a location on grid, places newObject on the grid at location (x,y) // (replacing any object currently on the grid at that location). // Otherwise, throws BadLocationException. { //@nowarn Deadlock setObjectAt(coord.getX(), coord.getY(), newObject); } synchronized public void pauseObjects() // EFFECTS: Pause all object threads. { //@nowarn Deadlock for (int x = 0; x < numHorizontal(); x++) { for (int y = 0; y < numVertical(); y++) { SimObject current = simobjects[x][y]; if (current != null) { current.pauseObject(); } } } } synchronized public void startObjects() // EFFECTS: Start all object threads. Previously started // threads will be resumed. { //@nowarn Deadlock for (int x = 0; x < numHorizontal(); x++) { for (int y = 0; y < numVertical(); y++) { SimObject current = simobjects[x][y]; if (current != null) { current.resumeObject(); } } } } synchronized public void removeAllObjects() // EFFECTS: removes all objects from the grid. { //@nowarn Deadlock for (int x = 0; x < numHorizontal(); x++) { for (int y = 0; y < numVertical(); y++) { simobjects[x][y] = null; } } } synchronized public void removeObjectAt(int x, int y) //@requires x >= 0 && x < xsize && y >= 0 && y < ysize // EFFECTS: If there is an object at (x, y), removes it. { //@nowarn Deadlock SimObject obj = getObjectAt(x, y); simobjects[x][y] = null; } //@nowarn Exception synchronized public void removeObjectAt(Coordinate c) //@requires c != null //@requires c.x >= 0 && c.x < xsize && c.y >= 0 && c.y < ysize // EFFECTS: If there is an object at c, removes it. { //@nowarn Deadlock removeObjectAt(c.getX(), c.getY()); } synchronized public boolean isSquareEmpty(int x, int y) throws RuntimeException //@requires x >= 0 && x < xsize && y >= 0 && y < ysize // EFFECTS: Returns the Cell at the specified x, y location. // Returns null if nothing is present there. { //@nowarn Deadlock return (getObjectAt(x, y) == null); } public boolean validLocation(Coordinate c) //@requires c != null //@ensures \result ==> c.x >= 0 && c.x < xsize && c.y >= 0 && c.y < ysize { return validLocation(c.getX(), c.getY()); } public boolean validLocation(int x, int y) // EFFECTS: Returns true iff x, y is a valid grid location. //@ensures \result ==> x >= 0 && x < xsize && y >= 0 && y < ysize { return (x >= 0 && y >= 0 && y < numVertical () && x < numHorizontal ()); } // We need the unsynchronized version of getObjectAt for the display --- we want to // be able to display the grid without acquiring a lock. This runs the risk that // the grid will be temporarily displayed in an inconsistent state. /* unsynchronized */ public SimObject grabObjectAt(int x, int y) throws RuntimeException //@requires x >= 0 && x < xsize && y >= 0 && y < ysize // EFFECTS: Returns the Cell at the specified row and column. // Returns null if nothing is present there. { if ((x < 0) || (x >= numHorizontal())) { throw new RuntimeException("Bad x parameter to getObjectAt: " + x); } if ((y < 0) || (y >= numVertical())) { throw new RuntimeException("Bad y parameter to getObjectAt: " + y); } return simobjects[x][y]; } synchronized public SimObject getObjectAt(int x, int y) throws RuntimeException //@requires x >= 0 && x < xsize && y >= 0 && y < ysize // EFFECTS: Returns the Cell at the specified location // Returns null if nothing is present there. { //@nowarn Deadlock return grabObjectAt(x, y); } synchronized public SimObject getObjectAt(Coordinate c) throws RuntimeException //@requires c != null //@requires c.x >= 0 && c.x < xsize && c.y >= 0 && c.y < ysize // EFFECTS: Returns the Cell at the specified location // Returns null if nothing is present there. { //@nowarn Deadlock return grabObjectAt(c.getX(), c.getY()); } public void paintComponent(Graphics g) throws RuntimeException { //@ assume g != null; int squarewidth = getSquareWidth(); int squareheight = getSquareHeight(); int hoffset = getHorizontalOffset(); int voffset = getVerticalOffset(); for (int y = 0; y < numVertical(); y++) { for (int x = 0; x < numHorizontal(); x++) { SimObject tmp = grabObjectAt(x, y); if (tmp == null) { g.setColor(Color.darkGray); } else { g.setColor(tmp.getColor()); } g.fillRect( hoffset + x * squarewidth, voffset + y * squareheight, squarewidth - 1, squareheight - 1); } } } }