Options to print prettier graphs...

[repair.git] / Repair / RepairCompiler / MCC / IR / GraphNode.java

diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java
index 13500ea661c202cff9cb99fe13d8fadda33aa9b8..424a8459852d4190620fecae79d20ff301e2bf92 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphNode.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphNode.java
@@ -72,6 +72,16 @@ public class GraphNode {
     NodeStatus status = UNVISITED;    
     String dotnodeparams = new String();
     Object owner = null;
+    boolean merge=false;
+    String nodeoption="";
+
+    public void setOption(String option) {
+       this.nodeoption=option;
+    }
+
+    public void setMerge() {
+       merge=true;
+    }
 
     public GraphNode(String label) {
         this.nodelabel = label;
@@ -113,6 +123,30 @@ public class GraphNode {
        }
     }
 
+    public static void boundedcomputeclosure(Collection nodes, Collection removed,int depth) {
+       Stack tovisit=new Stack();
+       Stack newvisit=new Stack();
+       tovisit.addAll(nodes);
+       for(int i=0;i<depth&&!tovisit.isEmpty();i++) {
+           while(!tovisit.isEmpty()) {
+               GraphNode gn=(GraphNode)tovisit.pop();
+               for(Iterator it=gn.edges();it.hasNext();) {
+                   Edge edge=(Edge)it.next();
+                   GraphNode target=edge.getTarget();
+                   if (!nodes.contains(target)) {
+                       if ((removed==null)||
+                           (!removed.contains(target))) {
+                           nodes.add(target);
+                           newvisit.push(target);
+                       }
+                   }
+               }
+           }
+           tovisit=newvisit;
+           newvisit=new Stack();
+       }
+    }
+
     public void setDotNodeParameters(String param) {
         if (param == null) {
             throw new NullPointerException();
@@ -204,12 +238,17 @@ public class GraphNode {
         }
 
         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;
             visitor.nodes = nodes;
             visitor.make();
-
         }
         
         private void make() {
@@ -234,21 +273,49 @@ public class GraphNode {
                 GraphNode gn = (GraphNode) i.next();
                 Iterator edges = gn.edges();
                 String label = gn.getTextLabel(); // + " [" + gn.discoverytime + "," + gn.finishingtime + "];";
-               String option="";
-               if (cycleset.contains(gn))
-                   option=",style=bold";
-                output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + option+"];");
+               String option=gn.nodeoption;
+               if (special!=null&&special.contains(gn))
+                   option+=",shape=box";
+               if (!gn.merge)
+                   output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + option+"];");
 
+               if (!gn.merge)
                 while (edges.hasNext()) {
                     Edge edge = (Edge) edges.next();
                     GraphNode node = edge.getTarget();
                    if (nodes.contains(node)) {
-                       String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\"";
-                       output.println("\t" + gn.getLabel() + " -> " + node.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];");
+                       for(Iterator nodeit=nonmerge(node).iterator();nodeit.hasNext();) {
+                           GraphNode node2=(GraphNode)nodeit.next();
+                           String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\"";
+                           output.println("\t" + gn.getLabel() + " -> " + node2.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];");
+                       }
                    }
                 }
             }
         }
+
+       Set nonmerge(GraphNode gn) {
+           HashSet newset=new HashSet();
+           HashSet toprocess=new HashSet();
+           toprocess.add(gn);
+           while(!toprocess.isEmpty()) {
+               GraphNode gn2=(GraphNode)toprocess.iterator().next();
+               toprocess.remove(gn2);
+               if (!gn2.merge)
+                   newset.add(gn2);
+               else {
+                   Iterator edges = gn2.edges();
+                   while (edges.hasNext()) {
+                       Edge edge = (Edge) edges.next();
+                       GraphNode node = edge.getTarget();
+                       if (!newset.contains(node)&&nodes.contains(node))
+                           toprocess.add(node);
+                   }
+               }
+           }
+           return newset;
+       }
+
     }
 
     /** This function returns the set of nodes involved in cycles.