3 /* Edge *****************/
6 protected GraphNode target;
7 protected GraphNode source;
9 protected String dotnodeparams = new String();
11 public Edge(GraphNode target) {
15 public String getLabel() {
19 public void setSource(GraphNode s) {
23 public GraphNode getSource() {
27 public GraphNode getTarget() {
31 public void setDotNodeParameters(String param) {
33 throw new NullPointerException();
35 if (dotnodeparams.length() > 0) {
36 dotnodeparams += "," + param;
38 dotnodeparams = param;
42 public static final EdgeStatus UNVISITED = new EdgeStatus("UNVISITED");
43 public static final EdgeStatus PROCESSING = new EdgeStatus("PROCESSING");
44 public static final EdgeStatus FINISHED = new EdgeStatus("FINISHED");
46 public static class EdgeStatus {
47 private static String name;
48 private EdgeStatus(String name) {
51 public String toString() {
56 int discoverytime = -1;
57 int finishingtime = -1; /* used for searches */
58 EdgeStatus status = UNVISITED;
66 void discover(int time) {
71 void finish(int time) {
72 assert status == PROCESSING;