edu.mit.csail.sdg.alloy4graph
Class GraphEdge

java.lang.Object
  extended by edu.mit.csail.sdg.alloy4graph.GraphEdge

public final class GraphEdge
extends java.lang.Object

Mutable; represents a graphical edge.

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


Field Summary
 java.lang.Object group
          a user-provided annotation that will be associated with this edge (all edges with same group will be highlighted together)
 java.lang.Object uuid
          a user-provided annotation that will be associated with this edge (can be null) (need not be unique)
 
Constructor Summary
GraphEdge(GraphNode from, GraphNode to, java.lang.Object uuid, java.lang.String label, java.lang.Object group)
          Construct an edge from "from" to "to", then add the edge to the graph.
 
Method Summary
 GraphNode a()
          Returns the "from" node.
 boolean ahead()
          Returns true if we will draw an arrow head on the "from" node.
 GraphNode b()
          Returns the "to" node.
 boolean bhead()
          Returns true if we will draw an arrow head on the "to" node.
 java.awt.Color color()
          Returns the line color; never null.
 int getLabelH()
          Return the height of the label box.
 int getLabelW()
          Return the width of the label box.
 int getLabelX()
          Return the X coordinate of the top-left corner of the label box.
 int getLabelY()
          Return the Y coordinate of the top-left corner of the label box.
 java.lang.String label()
          Returns the label on this edge.
 GraphEdge set(boolean from, boolean to)
          Sets whether we will draw an arrow head on the "from" node, and whether we will draw an arrow head on the "to" node.
 GraphEdge set(java.awt.Color color)
          Sets the line color.
 GraphEdge set(DotStyle style)
          Sets the line style.
 GraphEdge set(int weightBetween1And10000)
          Sets the edge weight between 1 and 10000.
 DotStyle style()
          Returns the line style; never null.
 java.lang.String toString()
          Returns a DOT representation of this edge (or "" if the start node is a dummy node)
 int weight()
          Returns the edge weight (which is always between 1 and 10000 inclusively).
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

uuid

public final java.lang.Object uuid
a user-provided annotation that will be associated with this edge (can be null) (need not be unique)


group

public final java.lang.Object group
a user-provided annotation that will be associated with this edge (all edges with same group will be highlighted together)

Constructor Detail

GraphEdge

public GraphEdge(GraphNode from,
                 GraphNode to,
                 java.lang.Object uuid,
                 java.lang.String label,
                 java.lang.Object group)
Construct an edge from "from" to "to", then add the edge to the graph.

Method Detail

a

public GraphNode a()
Returns the "from" node.


b

public GraphNode b()
Returns the "to" node.


getLabelX

public int getLabelX()
Return the X coordinate of the top-left corner of the label box.


getLabelY

public int getLabelY()
Return the Y coordinate of the top-left corner of the label box.


getLabelW

public int getLabelW()
Return the width of the label box.


getLabelH

public int getLabelH()
Return the height of the label box.


weight

public int weight()
Returns the edge weight (which is always between 1 and 10000 inclusively).


style

public DotStyle style()
Returns the line style; never null.


color

public java.awt.Color color()
Returns the line color; never null.


ahead

public boolean ahead()
Returns true if we will draw an arrow head on the "from" node.


bhead

public boolean bhead()
Returns true if we will draw an arrow head on the "to" node.


label

public java.lang.String label()
Returns the label on this edge.


set

public GraphEdge set(int weightBetween1And10000)
Sets the edge weight between 1 and 10000.


set

public GraphEdge set(boolean from,
                     boolean to)
Sets whether we will draw an arrow head on the "from" node, and whether we will draw an arrow head on the "to" node.


set

public GraphEdge set(DotStyle style)
Sets the line style.


set

public GraphEdge set(java.awt.Color color)
Sets the line color.


toString

public java.lang.String toString()
Returns a DOT representation of this edge (or "" if the start node is a dummy node)

Overrides:
toString in class java.lang.Object