pt.ua.gboard.games

Class Labyrinth

java.lang.Object

pt.ua.gboard.games.Labyrinth

public class Labyrinth
extends java.lang.Object

GBoard's based maze module.

Top-left coordinate is (0,0).

invariant: numberOfLines >= 1 && numberOfColumns >= 1
invariant: board != null

This class follows DbC(tm) methodology. Where possible, contracts are implement with JML and native's Java assert.

Author:

Miguel Oliveira e Silva (mos@ua.pt)

Field Summary

Fields

Modifier and Type	Field and Description
GBoard	board Maze's GBoard object.
int	numberOfColumns Maze's number of columns.
int	numberOfLines Maze's number of lines.

Constructor Summary

Constructors

Constructor and Description
Labyrinth(java.lang.String filename) Creates a labyrinth from a file.
Labyrinth(java.lang.String[] maze) Creates a labyrinth from an array of Strings.
Labyrinth(java.lang.String[] maze, char[] roadSymbols) Creates a labyrinth from an array of Strings, using external road symbols.
Labyrinth(java.lang.String[] maze, char[] roadSymbols, int gelemCellsSize) Creates a labyrinth from an array of Strings, using external road symbols.
Labyrinth(java.lang.String[] maze, char[] roadSymbols, int gelemCellsSize, boolean outsideIsRoad) Creates a labyrinth from an array of Strings, using external road symbols.
Labyrinth(java.lang.String[] maze, int gelemCellsSize) Creates a labyrinth from an array of Strings.
Labyrinth(java.lang.String filename, char[] roadSymbols) Creates a labyrinth from a file, using external road symbols.
Labyrinth(java.lang.String filename, char[] roadSymbols, int gelemCellsSize) Creates a labyrinth from a file, using external road symbols.
Labyrinth(java.lang.String filename, char[] roadSymbols, int gelemCellsSize, boolean outsideIsRoad) Creates a labyrinth from a file, using external road symbols.
Labyrinth(java.lang.String filename, int gelemCellsSize) Creates a labyrinth from a file.

Method Summary

Modifier and Type	Method and Description
void	attachGelemToRoadSymbol(char roadSymbol, Gelem gelem) Attach a gelem to a road symbol.
void	attachGelemToWallSymbol(char wallSymbol, Gelem gelem) Attach a gelem to a wall symbol.
void	detachGelemToRoadSymbol(char roadSymbol, Gelem gelem) Detach a gelem to a road symbol.
void	detachGelemToWallSymbol(char wallSymbol, Gelem gelem) Detach a gelem to a wall symbol.
Gelem	gelemAttachedToRoadSymbol(char roadSymbol) Get Gelem attached to road symbol.
Gelem	gelemAttachedToWallSymbol(char wallSymbol) Get Gelem attached to wall symbol.
boolean	isOutside(int line, int column) Is (line,column) a position outside the maze?
boolean	isRoad(int line, int column) Is (line,column) a road position?
boolean	isRoadSymbol(char c) Is character c a road symbol?
boolean	isRoadSymbolAttachToGelem(char roadSymbol) Is road symbol attached to a gelem?.
boolean	isWall(int line, int column) Is (line,column) a wall position?
boolean	isWallSymbol(char c) Is character c a wall symbol?
boolean	isWallSymbolAttachToGelem(char wallSymbol) Is wall symbol attached to a gelem?.
static int	numberOfLayers() Number of layers used when creating the GBoard (default value is 2).
void	putRoadSymbol(int line, int column, char roadSymbol) Defines the road symbol at position (line,column).
void	putWallSymbol(int line, int column, char wallSymbol) Defines the wall symbol at position (line,column).
char	roadSymbol(int line, int column) Get the road symbol at position (line,column).
Position[]	roadSymbolPositions(char roadSymbol) Get all the external road symbol's positions at the maze.
static void	setNumberOfLayers(int numberOfLayers) Define the number of layers to be used when creating the GBoard.
static void	setWindowName(java.lang.String windowName) Define the name used when creating the GBoard.
Position[]	symbolPositions(char symbol) Get all the symbol's positions at the maze (applies both to wall and road symbols including space).
static boolean	validMapFile(java.lang.String filename) Checks if a file path is valid
boolean	validPosition(int line, int column) Is (line,column) a position inside the rectangle defined by the maze?
char	wallSymbol(int line, int column) Get the wall symbol at position (line,column).
static java.lang.String	windowName() Nome of window used when creating the GBoard (default value is Labyrinth).

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

numberOfLines

public final int numberOfLines

Maze's number of lines.

numberOfColumns

public final int numberOfColumns

Maze's number of columns.

board

public final GBoard board

Maze's GBoard object.

Constructor Detail

Labyrinth

public Labyrinth(java.lang.String filename)

Creates a labyrinth from a file.

requires: validMapFile(filename)

Parameters:

filename - path to the file

Labyrinth

public Labyrinth(java.lang.String filename,
                 char[] roadSymbols)

Creates a labyrinth from a file, using external road symbols.

requires: validMapFile(filename)

Parameters:

filename - path to the file

roadSymbols - array of extra character road symbols

Labyrinth

public Labyrinth(java.lang.String filename,
                 int gelemCellsSize)

Creates a labyrinth from a file.

requires: validMapFile(filename)
requires: gelemCellsSize > 0

Parameters:

filename - path to the file

gelemCellsSize - width and height of each gelem in GBoard

Labyrinth

public Labyrinth(java.lang.String filename,
                 char[] roadSymbols,
                 int gelemCellsSize)

Creates a labyrinth from a file, using external road symbols.

requires: validMapFile(filename)
requires: gelemCellsSize > 0

Parameters:

filename - path to the file

roadSymbols - array of extra character road symbols

gelemCellsSize - width and height of each gelem in GBoard

Labyrinth

public Labyrinth(java.lang.String filename,
                 char[] roadSymbols,
                 int gelemCellsSize,
                 boolean outsideIsRoad)

Creates a labyrinth from a file, using external road symbols.

requires: validMapFile(filename)
requires: gelemCellsSize > 0

Parameters:

filename - path to the file

roadSymbols - array of extra character road symbols

gelemCellsSize - width and height of each gelem in GBoard

outsideIsRoad - if true outside within rectangle limits is considered road (otherwise it is neither road nor wall)

Labyrinth

public Labyrinth(java.lang.String[] maze)

Creates a labyrinth from an array of Strings.

requires: maze != null && maze.length > 0

Parameters:

maze - array

Labyrinth

public Labyrinth(java.lang.String[] maze,
                 char[] roadSymbols)

Creates a labyrinth from an array of Strings, using external road symbols.

requires: maze != null && maze.length > 0

Parameters:

maze - array

roadSymbols - array of extra character road symbols

Labyrinth

public Labyrinth(java.lang.String[] maze,
                 int gelemCellsSize)

Creates a labyrinth from an array of Strings.

requires: maze != null && maze.length > 0
requires: gelemCellsSize > 0

Parameters:

maze - array

gelemCellsSize - width and height of each gelem in GBoard

Labyrinth

public Labyrinth(java.lang.String[] maze,
                 char[] roadSymbols,
                 int gelemCellsSize)

Creates a labyrinth from an array of Strings, using external road symbols.

requires: maze != null && maze.length > 0
requires: gelemCellsSize > 0

Parameters:

maze - array

roadSymbols - array of extra character road symbols

gelemCellsSize - width and height of each gelem in GBoard

Labyrinth

public Labyrinth(java.lang.String[] maze,
                 char[] roadSymbols,
                 int gelemCellsSize,
                 boolean outsideIsRoad)

Creates a labyrinth from an array of Strings, using external road symbols.

requires: maze != null && maze.length > 0
requires: gelemCellsSize > 0

Parameters:

maze - array

roadSymbols - array of extra character road symbols

gelemCellsSize - width and height of each gelem in GBoard

outsideIsRoad - if true outside within rectangle limits is considered road (otherwise it is neither road nor wall)

Method Detail

numberOfLayers

public static int numberOfLayers()

Number of layers used when creating the GBoard (default value is 2).

Returns:

number of layers

setNumberOfLayers

public static void setNumberOfLayers(int numberOfLayers)

Define the number of layers to be used when creating the GBoard.

requires: numberOfLayers >= 1

Parameters:

numberOfLayers - the number of layers

validMapFile

public static boolean validMapFile(java.lang.String filename)

Checks if a file path is valid

Parameters:

filename - file path

Returns:

boolean true if the path is valid, otherwise it returns false

windowName

public static java.lang.String windowName()

Nome of window used when creating the GBoard (default value is Labyrinth).

Returns:

name

setWindowName

public static void setWindowName(java.lang.String windowName)

Define the name used when creating the GBoard.

requires: windowName != null

Parameters:

windowName - name

validPosition

public boolean validPosition(int line,
                             int column)

Is (line,column) a position inside the rectangle defined by the maze?

Parameters:

line - line number

column - column number

Returns:

boolean true if position is valid, otherwise it returns false

isOutside

public boolean isOutside(int line,
                         int column)

Is (line,column) a position outside the maze?

requires: validPosition(line, column)

Parameters:

line - line number

column - column number

Returns:

boolean true if it is an outside position, otherwise it returns false

isRoadSymbol

public boolean isRoadSymbol(char c)

Is character c a road symbol?

Parameters:

c - character symbol

Returns:

boolean true if is a road symbol, otherwise it returns false (meaning that it is a wall symbol)

isWallSymbol

public boolean isWallSymbol(char c)

Is character c a wall symbol?

Parameters:

c - character symbol

Returns:

boolean true if is a wall symbol, otherwise it returns false (meaning that it is a road symbol)

isRoad

public boolean isRoad(int line,
                      int column)

Is (line,column) a road position?

requires: validPosition(line, column)

Parameters:

line - line number

column - column number

Returns:

boolean true if it is a road position, otherwise it returns false

isWall

public boolean isWall(int line,
                      int column)

Is (line,column) a wall position?

requires: validPosition(line, column)

Parameters:

line - line number

column - column number

Returns:

boolean true if it is a wall position, otherwise it returns false

roadSymbol

public char roadSymbol(int line,
                       int column)

Get the road symbol at position (line,column).

requires: isRoad(line, column)

Parameters:

line - line number

column - column number

Returns:

char road symbol

wallSymbol

public char wallSymbol(int line,
                       int column)

Get the wall symbol at position (line,column).

requires: isWall(line, column)

Parameters:

line - line number

column - column number

Returns:

char wall symbol

roadSymbolPositions

public Position[] roadSymbolPositions(char roadSymbol)

Get all the external road symbol's positions at the maze.

requires: isRoadSymbol(roadSymbol) && roadSymbol != ' '

ensures: \result != null

Parameters:

roadSymbol - character road symbol

Returns:

Position[] array of positions

symbolPositions

public Position[] symbolPositions(char symbol)

Get all the symbol's positions at the maze (applies both to wall and road symbols including space).

ensures: \result != null

Parameters:

symbol - character symbol

Returns:

Position[] array of positions

putRoadSymbol

public void putRoadSymbol(int line,
                          int column,
                          char roadSymbol)

Defines the road symbol at position (line,column).

requires: isRoad(line, column)
requires: isRoadSymbol(roadSymbol)

ensures: isRoad(line, column)
ensures: roadSymbol(line, column) == roadSymbol

Parameters:

line - line number

column - column number

roadSymbol - character road symbol

putWallSymbol

public void putWallSymbol(int line,
                          int column,
                          char wallSymbol)

Defines the wall symbol at position (line,column).

requires: isWall(line, column)
requires: isWallSymbol(wallSymbol)

ensures: isWall(line, column)
ensures: wallSymbol(line, column) == wallSymbol

Parameters:

line - line number

column - column number

wallSymbol - character wall symbol

isRoadSymbolAttachToGelem

public boolean isRoadSymbolAttachToGelem(char roadSymbol)

Is road symbol attached to a gelem?.

requires: isRoadSymbol(roadSymbol)

Parameters:

roadSymbol - character road symbol

Returns:

boolean true if is attached, otherwise it returns false

gelemAttachedToRoadSymbol

public Gelem gelemAttachedToRoadSymbol(char roadSymbol)

Get Gelem attached to road symbol.

requires: isRoadSymbol(roadSymbol)
requires: isRoadSymbolAttachToGelem(roadSymbol)

Parameters:

roadSymbol - character road symbol

Returns:

Gelem gelem's object

attachGelemToRoadSymbol

public void attachGelemToRoadSymbol(char roadSymbol,
                                    Gelem gelem)

Attach a gelem to a road symbol.

requires: isRoadSymbol(roadSymbol)
requires: gelem != null
requires: !isRoadSymbolAttachToGelem(roadSymbol)

ensures: isRoadSymbolAttachToGelem(roadSymbol)

Parameters:

roadSymbol - character road symbol

gelem - gelem object

detachGelemToRoadSymbol

public void detachGelemToRoadSymbol(char roadSymbol,
                                    Gelem gelem)

Detach a gelem to a road symbol.

requires: isRoadSymbol(roadSymbol)
requires: isRoadSymbolAttachToGelem(roadSymbol)

ensures: !isRoadSymbolAttachToGelem(roadSymbol)

Parameters:

roadSymbol - character road symbol

gelem - the gelem's object

isWallSymbolAttachToGelem

public boolean isWallSymbolAttachToGelem(char wallSymbol)

Is wall symbol attached to a gelem?.

requires: isWallSymbol(wallSymbol)

Parameters:

wallSymbol - character wall symbol

Returns:

boolean true if is attached, otherwise it returns false

gelemAttachedToWallSymbol

public Gelem gelemAttachedToWallSymbol(char wallSymbol)

Get Gelem attached to wall symbol.

requires: isWallSymbol(wallSymbol)
requires: isWallSymbolAttachToGelem(wallSymbol)

Parameters:

wallSymbol - character wall symbol

Returns:

Gelem gelem's object

attachGelemToWallSymbol

public void attachGelemToWallSymbol(char wallSymbol,
                                    Gelem gelem)

Attach a gelem to a wall symbol.

requires: isWallSymbol(wallSymbol)
requires: gelem != null
requires: !isWallSymbolAttachToGelem(wallSymbol)

ensures: isWallSymbolAttachToGelem(wallSymbol)

Parameters:

wallSymbol - character wall symbol

gelem - gelem object

detachGelemToWallSymbol

public void detachGelemToWallSymbol(char wallSymbol,
                                    Gelem gelem)

Detach a gelem to a wall symbol.

requires: isWallSymbol(wallSymbol)
requires: isWallSymbolAttachToGelem(wallSymbol)

ensures: !isWallSymbolAttachToGelem(wallSymbol)

Parameters:

wallSymbol - character wall symbol

gelem - the gelem's object