public static final NodeStatus UNVISITED = new NodeStatus("UNVISITED");
public static final NodeStatus PROCESSING = new NodeStatus("PROCESSING");
public static final NodeStatus FINISHED = new NodeStatus("FINISHED");
-
+
public static class NodeStatus {
private static String name;
private NodeStatus(String name) { this.name = name; }
int discoverytime = -1;
int finishingtime = -1; /* used for searches */
- Vector edges = new Vector();
- Vector inedges = new Vector();
+ protected Vector edges = new Vector();
+ protected Vector inedges = new Vector();
+
NodeStatus status = UNVISITED;
String dotnodeparams = new String();
public boolean merge=false;
- public String nodeoption="";
-
- public void setOption(String option) {
- this.nodeoption=","+option;
- }
public void setMerge() {
merge=true;
if (param == null) {
throw new NullPointerException();
}
- if (param.length() > 0) {
- dotnodeparams = "," + param;
+ if (dotnodeparams.length() > 0) {
+ dotnodeparams += "," + param;
} else {
- dotnodeparams = new String();
+ dotnodeparams = param;
}
}
}
this.status = status;
}
-
+
public String getLabel() {
return "";
}
public String getTextLabel() {
return "";
}
+
+ public String getName(){
+ return "";
+ }
public NodeStatus getStatus() {
return this.status;
}
+ public int numedges() {
+ return edges.size();
+ }
+
+ public int numinedges() {
+ return inedges.size();
+ }
+
+ public Edge getedge(int i) {
+ return (Edge) edges.get(i);
+ }
+
+ public Edge getinedge(int i) {
+ return (Edge) inedges.get(i);
+ }
+
+ public Vector getEdgeVector() {
+ return edges;
+ }
+
+ public Vector getInedgeVector() {
+ return inedges;
+ }
+
public Iterator edges() {
return edges.iterator();
}
public Iterator inedges() {
return inedges.iterator();
}
-
+
public void addEdge(Edge newedge) {
newedge.setSource(this);
edges.addElement(newedge);
tonode.inedges.addElement(newedge);
}
+ public void addEdge(Vector v) {
+ for (Iterator it = v.iterator(); it.hasNext();)
+ addEdge((Edge)it.next());
+ }
+
+ public void removeEdge(Edge edge) {
+ edges.remove(edge);
+ }
+
+ public void removeInedge(Edge edge) {
+ inedges.remove(edge);
+ }
+
+ public void removeAllEdges() {
+ edges.removeAllElements();
+ }
+
+ public void removeAllInedges() {
+ inedges.removeAllElements();
+ }
void reset() {
discoverytime = -1;
finishingtime = -1;
java.io.PrintWriter output;
int tokennumber;
int color;
+ Vector namers;
- private DOTVisitor(java.io.OutputStream output) {
+ private DOTVisitor(java.io.OutputStream output, Vector namers) {
tokennumber = 0;
color = 0;
this.output = new java.io.PrintWriter(output, true);
+ this.namers=namers;
}
private String getNewID(String name) {
}
Collection nodes;
- Collection special;
- public static void visit(java.io.OutputStream output, Collection nodes) {
- visit(output,nodes,null);
- }
- public static void visit(java.io.OutputStream output, Collection nodes, Collection special) {
- DOTVisitor visitor = new DOTVisitor(output);
- visitor.special=special;
+ public static void visit(java.io.OutputStream output, Collection nodes, Vector namers) {
+ DOTVisitor visitor = new DOTVisitor(output, namers);
+ visitor.nodes = nodes;
+ visitor.make();
+ }
+
+ public static void visit(java.io.OutputStream output, Collection nodes) {
+ Vector v=new Vector();
+ v.add(new Namer());
+ DOTVisitor visitor = new DOTVisitor(output, v);
visitor.nodes = nodes;
visitor.make();
}
private void make() {
output.println("digraph dotvisitor {");
- output.println("\trotate=90;");
/* output.println("\tpage=\"8.5,11\";");
output.println("\tnslimit=1000.0;");
output.println("\tnslimit1=1000.0;");
output.println("\tremincross=true;");*/
output.println("\tnode [fontsize=10,height=\"0.1\", width=\"0.1\"];");
output.println("\tedge [fontsize=6];");
- traverse();
+ traverse();
output.println("}\n");
}
+
+
private void traverse() {
Set cycleset=GraphNode.findcycles(nodes);
- Iterator i = nodes.iterator();
- while (i.hasNext()) {
- GraphNode gn = (GraphNode) i.next();
+ Iterator it = nodes.iterator();
+ while (it.hasNext()) {
+ GraphNode gn = (GraphNode) it.next();
Iterator edges = gn.edges();
- String label = gn.getTextLabel();
- String option=gn.nodeoption;
- if (special!=null&&special.contains(gn))
- option+=",shape=box";
+ String label = "";
+ String dotnodeparams="";
+
+ for(int i=0;i<namers.size();i++) {
+ Namer name=(Namer) namers.get(i);
+ String newlabel=name.nodeLabel(gn);
+ String newparams=name.nodeOption(gn);
+
+ if (!newlabel.equals("") && !label.equals("")) {
+ label+=", ";
+ }
+ if (!newparams.equals("")) {
+ dotnodeparams+=", " + name.nodeOption(gn);
+ }
+ label+=name.nodeLabel(gn);
+ }
+
if (!gn.merge)
- output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + option+"];");
+ output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + dotnodeparams + "];");
if (!gn.merge)
while (edges.hasNext()) {
if (nodes.contains(node)) {
for(Iterator nodeit=nonmerge(node).iterator();nodeit.hasNext();) {
GraphNode node2=(GraphNode)nodeit.next();
- String edgelabel = "label=\"" + edge.getLabel() + "\"" ;
- output.println("\t" + gn.getLabel() + " -> " + node2.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];");
+ String edgelabel = "";
+ String edgedotnodeparams="";
+
+ for(int i=0;i<namers.size();i++) {
+ Namer name=(Namer) namers.get(i);
+ String newlabel=name.edgeLabel(edge);
+ String newoption=name.edgeOption(edge);
+ if (!newlabel.equals("")&& ! edgelabel.equals(""))
+ edgelabel+=", ";
+ edgelabel+=newlabel;
+ if (!newoption.equals(""))
+ edgedotnodeparams+=", "+newoption;
+ }
+
+ output.println("\t" + gn.getLabel() + " -> " + node2.getLabel() + " [" + "label=\"" + edgelabel + "\"" + edgedotnodeparams + "];");
}
}
}
projects / IRC.git / blobdiff