edu.mit.csail.sdg.alloy4graph
Class Graph

java.lang.Object
  edu.mit.csail.sdg.alloy4graph.Graph

public final class Graph
extends java.lang.Object

Mutable; represents a graph.

Thread Safety: Can be called only by the AWT event thread.

Field Summary

java.util.List<GraphEdge>	edges An unmodifiable view of the list of edges.
java.util.List<GraphNode>	nodes An unmodifiable view of the list of nodes.

Constructor Summary

Graph(double defaultScale)
Constructs an empty Graph object.

Method Summary

void	addLegend(java.lang.Comparable<?> object, java.lang.String label, java.awt.Color color) Add a legend with the given object and the associated text label; if color==null, that means we will still add this legend into the list of legends, but this legend will be hidden.
java.lang.Object	find(double scale, int mouseX, int mouseY) Locates the node or edge at the given (X,Y) location.
int	getLeft() Assuming layout() has been called, this returns the left edge.
int	getTop() Assuming layout() has been called, this returns the top edge.
int	getTotalHeight() Assuming layout() has been called, this returns the total height.
int	getTotalWidth() Assuming layout() has been called, this returns the total width.
void	layout() (Re-)perform the layout.
java.lang.String	toString() Returns a DOT representation of this graph.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

nodes

public final java.util.List<GraphNode> nodes

An unmodifiable view of the list of nodes.

edges

public final java.util.List<GraphEdge> edges

An unmodifiable view of the list of edges.

Constructor Detail

Graph

public Graph(double defaultScale)

Constructs an empty Graph object.

Method Detail

getLeft

public int getLeft()

Assuming layout() has been called, this returns the left edge.

getTop

public int getTop()

Assuming layout() has been called, this returns the top edge.

getTotalWidth

public int getTotalWidth()

Assuming layout() has been called, this returns the total width.

getTotalHeight

public int getTotalHeight()

Assuming layout() has been called, this returns the total height.

addLegend

public void addLegend(java.lang.Comparable<?> object,
                      java.lang.String label,
                      java.awt.Color color)

Add a legend with the given object and the associated text label; if color==null, that means we will still add this legend into the list of legends, but this legend will be hidden.

layout

public void layout()

(Re-)perform the layout.

find

public java.lang.Object find(double scale,
                             int mouseX,
                             int mouseY)

Locates the node or edge at the given (X,Y) location.

toString

public java.lang.String toString()

Returns a DOT representation of this graph.

Overrides:

toString in class java.lang.Object