Code to print graph to output so that dot can be used to generate pdf of graph.

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index b05c9f3837f115902a14b19fb746c9068ef94f94..12eb14f22215095f3d635988d5d44c26a54959c2 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -300,6 +300,10 @@ public class ConflictTracker extends ListenerAdapter {
         (getApp().hashCode() << 1) ^
         getValue().hashCode();
     }
+
+    public String toString() {
+      return "<"+getAttribute()+", "+getValue()+", "+getApp()+", "+ismanual+">";
+    }
   }
 
   static class IndexObject {
@@ -344,6 +348,30 @@ public class ConflictTracker extends ListenerAdapter {
     return nodes.get(id);
   }
 
+  public void printGraph() {
+    System.out.println("digraph testgraph {");
+    for(Integer i : nodes.keySet()) {
+      Node n = nodes.get(i);
+      System.out.print("N"+i+"[label=\"");
+
+      for(IndexObject io:n.lastUpdates.keySet()) {
+        for(Update u:n.lastUpdates.get(io)) {
+          System.out.print(u.toString().replace("\"", "\\\"")+", ");
+        }
+      }
+      System.out.println("\"];");
+      for(Edge e:n.outEdges) {
+        System.out.print("N"+e.getSrc().getId()+"->N"+e.getDst().getId()+"[label=\"");
+        for(Update u:e.getUpdates()) {
+          System.out.print(u.toString().replace("\"", "\\\"")+", ");
+        }
+        System.out.println("\"];");
+      }
+    }
+
+    System.out.println("}");
+  }
+  
   @Override
   public void stateAdvanced(Search search) {
     String theEnd = null;
@@ -399,6 +427,9 @@ public class ConflictTracker extends ListenerAdapter {
   @Override
   public void searchFinished(Search search) {
     out.println("----------------------------------- search finished");
+
+    //Comment out the following line to print the explored graph
+    // printGraph();
   }
 
   private String getValue(ThreadInfo ti, Instruction inst, byte type) {