[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools StateSpaceDot.java,1.3,1.4

[Masoud Mansouri-S. <mas...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv13604/src/gov/nasa/jpf/tools

Modified Files:
	StateSpaceDot.java 
Log Message:
- Added transition nodes rather than using just edges for transitions.
   We need multiple transitions between two states which GUESS/GDF
   cannot handle at the moment so rather than st0->st1, we now have
   st0->tr0->st1. The source line information is on the label of the first segment (st0->tr0). The (tr0->st1) is labeled with the transition number only. By default labels are set to be invisible. Must use -labelvisible option to generate the graph with visible transition labels otherwise when GUESS is run you can use "g.edges.labelvisible=true" from the GUESS Jython command line.
- stateRestored() method was modified to solve a bug that I discovered
  which caused wrong edges to be drawn when BFS HeuristicSearch was
  used. Willem found and suggested the fix.


Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- StateSpaceDot.java	21 Jun 2005 00:07:19 -0000	1.3
+++ StateSpaceDot.java	23 Jun 2005 01:10:06 -0000	1.4
@@ -58,20 +58,34 @@
   private static final String GDF_EXT = "gdf";
   private static final String OUT_FILENAME_NO_EXT = "jpf-state-space";
 
+  // NODE styles constants
+  private static final int RECTABGLE = 1;
+  private static final int ELLIPSE   = 2;
+  private static final int ROUND_RECTABGLE = 3;
+  private static final int RECTABGLE_WITH_TEXT = 4;
+  private static final int ELLIPSE_WITH_TEXT = 5;
+  private static final int ROUND_RECTABGLE_WITH_TEXT = 6;
+
+  // State and transition node styles used
+  private static final int state_node_style=ELLIPSE_WITH_TEXT;
+  private static final int transition_node_style=RECTABGLE_WITH_TEXT;
+
+  // File formats supported
+  private static final int DOT_FORMAT=0;
+  private static final int GDF_FORMAT=1;
+
   private BufferedWriter graph = null;
   private int edge_id = 0;
   private static boolean transition_numbers=false;
   private static boolean show_source=false;
-  private static int DOT_FORMAT=0;
-  private static int GDF_FORMAT=1;
-  private int format=DOT_FORMAT;
+  private static int format=DOT_FORMAT;
   private String out_filename = OUT_FILENAME_NO_EXT+"."+DOT_EXT;
-  private boolean labelvisible=false;
-
-  /* In gdf format all the edges must come after all the nodes of the graph are
-   * generated. So we first output the nodes as come across them but we store
-   * the strings for edges in the gdfEdges list and output them when the
-   * search ends.
+  private static boolean labelvisible=false;
+  
+  /* In gdf format all the edges must come after all the nodes of the graph
+   * are generated. So we first output the nodes as we come across them but
+   * we store the strings for edges in the gdfEdges list and output them when
+   * the search ends.
    */
   ArrayList gdfEdges=new ArrayList();
 
@@ -112,7 +126,7 @@
   }
 
   public void stateRestored (Search search) {
-   // N/A
+    prev_state.reset(search.getStateNumber(), false, false);
   }
 
   public void stateProcessed (Search search) {
@@ -172,22 +186,26 @@
   }
 
   /**
-   * Put the footer for the graph into the file.
+   * In the case of the DOT graph it is just adding the final "}" at the end.
+   * In the case of GPF format we must output edge definition and all the
+   * edges that we have found.
    */
   private void endGraph() throws IOException {
     addNode(prev_state);
     if (format==GDF_FORMAT) {
       graph.write("edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)");
+      graph.newLine();
+
+      // Output all the edges that we have accumulated so far
+      int size=gdfEdges.size();
+  	  for (int i=0; i<size; i++) {
+  		graph.write((String) gdfEdges.get(i));
+  	    graph.newLine();
+  	  }
     } else {
       graph.write("}");
+      graph.newLine();
     }
-    graph.newLine();
-	// Output all the edges that we have accumulated so far
-	int size=gdfEdges.size();
-	for (int i=0; i<size; i++) {
-		graph.write((String) gdfEdges.get(i));
-	    graph.newLine();
-	}
     graph.close();
   }
 
@@ -270,7 +288,7 @@
     if (trans == null) {
   	  return "-init-";
   	}
-
+    
   	StringBuffer result = new StringBuffer();
 
   	if (transition_numbers) {
@@ -315,7 +333,7 @@
         if (state.error != null) {
           graph.write(":" + state.error);
         }
-        graph.write("\",5");
+        graph.write("\","+state_node_style);
         if (state.error != null) {
             graph.write(",red");
           } else if (state.has_next) {
@@ -364,9 +382,18 @@
     if (format==GDF_FORMAT) {
       int thread = state.getTransition().getThread();
       // edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)
-      gdfEdges.add("st" + old_id + ",st" + new_id+
-                   ",\"" + makeGdfLabel(state, my_id)+"\","+
-                   labelvisible+",true,"+thread);
+
+      // Old State -> Transition. Only this segment is labeled with the source
+      // information.
+      gdfEdges.add("st" + old_id + ",tr" + my_id+",\""+
+      		       makeGdfLabel(state, my_id) +"\","+
+				   labelvisible+",true,"+thread);
+      // Transition node: name,label,style,color
+      graph.write("tr" + my_id + ",\"" +my_id+"\","+transition_node_style);
+      graph.newLine();
+      // Transition -> New State
+      gdfEdges.add("tr" + my_id + ",st" + new_id+",\"" +my_id+
+      		       "\","+labelvisible+",true,"+thread);
     } else { // DOT
       graph.write("  st" + old_id + " -> tr" + my_id + ";");
       graph.newLine();