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

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

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

Modified Files:
	StateSpaceDot.java 
Log Message:
* Added the program output at the transitions to the edges (only for the
   gdf format). For an edge of the form st1->tr1->st2, the source line is
   included in the label of the first segment (st1->tr1) and the application
   output is added as the label of the second segment (tr1->st2).
* Added a -help option.
* Refactored the code slightly to make it more maintainable.
* Changed the type of the thread number field of edges to be INTs and
   not VARCHAR(32)s.

Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -d -r1.4 -r1.5
--- StateSpaceDot.java	23 Jun 2005 01:10:06 -0000	1.4
+++ StateSpaceDot.java	27 Jun 2005 21:42:09 -0000	1.5
@@ -43,10 +43,11 @@
  * 
  * Options:
  *   -gdf:                Generate the graph in GDF format. The default is DOT.
- *   -transition-numbers: Generate transition numbers
- *   -show-source:        Show source lines.
- *   -labelvisible:       Indicates if the label on the transitions is visible
- *                        (used only with the -gdf option)
+ *   -transition-numbers: Include transition numbers in transition labels.
+ *   -show-source:        Include source lines in transition labels.
+ *   -labelvisible:       Indicates if the label on the transitions is visible (used only with the -gdf option)
+ *   -help:               Prints this help information and stops.
+ * 
  * @date 9/12/03
  * @author Owen O'Malley (Initial version generating the DOT graph)
  * 
@@ -81,6 +82,8 @@
   private static int format=DOT_FORMAT;
   private String out_filename = OUT_FILENAME_NO_EXT+"."+DOT_EXT;
   private static boolean labelvisible=false;
+  private static boolean helpRequested=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
@@ -193,7 +196,7 @@
   private void endGraph() throws IOException {
     addNode(prev_state);
     if (format==GDF_FORMAT) {
-      graph.write("edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)");
+      graph.write("edgedef>node1,node2,label,labelvisible,directed,thread INT,lastoutput VARCHAR(32)");
       graph.newLine();
 
       // Output all the edges that we have accumulated so far
@@ -244,35 +247,11 @@
      
         // We need to precede the dot-specific special characters which appear
         // in the Java source line, such as ']' and '"', with the '\' escape
-        // characters and also to remove any new lines. There seems to be a bug
-        // in Java String's replaceAll() method which does not allow us to use
-        // it to replace the special chars in the source_line string, so here
-        // I am using StringBuffer's replace method to do this - masoud
-     
-        int indexOfNewLine=0;
-        while (indexOfNewLine!=-1) {
-          indexOfNewLine=sb.indexOf("\\n");
-          if (indexOfNewLine!=-1)
-            sb.replace(indexOfNewLine, indexOfNewLine+2, "");
-        }
-     
-        int indexOfBracket=0, lastIndex=0;
-        while (indexOfBracket!=-1) {
-          indexOfBracket=sb.indexOf("]", lastIndex);
-          if (indexOfBracket!=-1) {
-            sb.replace(indexOfBracket, indexOfBracket+1, "\\]");
-            lastIndex=indexOfBracket+2;
-          }
-        }
+        // characters and also to remove any new lines.
      
-        int indexOfQuote=0, lastIndexOfQueote=0;
-        while (indexOfQuote!=-1) {
-          indexOfQuote=sb.indexOf("\"",lastIndexOfQueote);
-          if (indexOfQuote!=-1) {
-            sb.replace(indexOfQuote, indexOfQuote+1, "\\\"");
-            lastIndexOfQueote=indexOfQuote+2;
-          }
-        }
+        replaceString(sb, "\n", "");
+        replaceString(sb, "]", "\\]");
+        replaceString(sb, "\"", "\\\"");
         result.append(sb.toString());
       }
     }
@@ -303,27 +282,59 @@
   	  String source_line=last_trans_step.getSourceRef().getLineString();
   	  if ((source_line != null) && !source_line.equals("")) {
 
-        StringBuffer sb=new StringBuffer(source_line);
-  	     
-  	    // We need to deal with gdf-specific special characters which appear
+  	    // We need to deal with gdf-specific special characters which couls appear
   	    // in the Java source line, such as '"'.
-  	     
-  	    int indexOfQuote=0, lastIndexOfQueote=0;
-  	    while (indexOfQuote!=-1) {
-  	      indexOfQuote=sb.indexOf("\"",lastIndexOfQueote);
- 	      if (indexOfQuote!=-1) {
-  	        sb.replace(indexOfQuote, indexOfQuote+1, "\'\'");
-  	        lastIndexOfQueote=indexOfQuote+2;
-  	      }
-  	    }
-  	     
-  	    result.append(sb.toString());
+  	    result.append(source_line);
+  	  	convertGdfSpecial(result);
   	  }
     }
   	return result.toString();
   }
 
   /**
+   * Locates and replaces all occurrences of a given string with another given
+   * string in an original string buffer. There seems to be a bug in Java
+   * String's replaceAll() method which does not allow us to use it to replace
+   * some special chars so here we use StringBuffer's replace method to do
+   * this.
+   * @param original The original string buffer.
+   * @param from The replaced string.
+   * @param to The replacing string.
+   * @return The original string buffer with the sub-string replaced
+   *         throughout.
+   */
+  private StringBuffer replaceString(StringBuffer original,
+  		                             String from,
+									 String to) {
+    int indexOfReplaced=0, lastIndexOfReplaced=0;
+    while (indexOfReplaced!=-1) {
+      indexOfReplaced=original.indexOf(from,lastIndexOfReplaced);
+      if (indexOfReplaced!=-1) {
+      	original.replace(indexOfReplaced, indexOfReplaced+1, to);
+        lastIndexOfReplaced=indexOfReplaced+to.length();
+      }
+    }
+    return original;
+  }
+  
+  /**
+   * Locates and replaces all occurrences of a given string with another given
+   * string in an original string buffer.
+   * @param original The original string buffer.
+   * @param from The replaced string.
+   * @param to The replacing string.
+   * @return The original string buffer with the sub-string replaced
+   *         throughout.
+   */
+  private String replaceString(String original, String from, String to) {
+  	if ((original!=null) && (from!=null) && (to!=null)) {
+      return replaceString(new StringBuffer(original), from, to).toString();
+  	} else {
+      return original;
+  	}
+  }
+
+  /**
    * Add a new node to the graph with the relevant properties.
    */
   private void addNode(StateInformation state) throws IOException {
@@ -375,25 +386,81 @@
   }
 
   /**
+   * Creates an GDF edge string.
+   */
+  private String makeGdfEdgeString(String from_id,
+  		                           String to_id,
+								   String label,
+								   int thread,
+								   String lastOutput) {
+  	StringBuffer sb=new StringBuffer();
+  	sb.append(from_id).append(',').append(to_id).append(',').
+	  append('\"');
+  	if ((label!=null) && (!"".equals(label))) {
+  		sb.append(label);
+  	} else {
+  		sb.append('-');
+  	}
+  	sb.append('\"').append(',').append(labelvisible).append(',').append(true).
+	append(',').append(thread);
+  	lastOutput=replaceString(lastOutput, "\"", "\'\'");
+  	if ((lastOutput!=null) && (!"".equals(lastOutput))) {
+  		sb.append(',').append('\"').append(lastOutput).append('\"');
+  	}
+  	replaceString(sb, "\n", "");
+  	return sb.toString();
+  }
+
+  /**
+   * GUESS cannot deal with '\n' chars, so remove them. Also convert all '"'
+   * characters to "''".
+   * @param str The string to perform the conversion on.
+   * @return The converted string.
+   */
+  private String convertGdfSpecial(String str) {
+  	if ((str==null) || "".equals(str)) return "";
+  	
+  	StringBuffer sb=new StringBuffer(str);
+  	convertGdfSpecial(sb);
+  	return sb.toString();
+  }
+  
+  /**
+   * GUESS cannot deal with '\n' chars, so replace them with a space. Also
+   * convert all '"' characters to "''".
+   * @param sb The string buffer to perform the conversion on.
+   */
+  private void convertGdfSpecial(StringBuffer sb) {
+  	replaceString(sb, "\"", "\'\'");
+  	replaceString(sb, "\n", " ");
+  }
+
+  /**
    * Create an edge in the graph file from old_id to new_id.
    */
   private void addEdge(int old_id, int new_id, Search state) throws IOException {
     int my_id = edge_id++;
     if (format==GDF_FORMAT) {
-      int thread = state.getTransition().getThread();
-      // edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)
+      Transition trans=state.getTransition();
+      int thread = trans.getThread();
+      String lastoutput=convertGdfSpecial(trans.getOutput());
+      
+      // edgedef>node1,node2,label,labelvisible,directed,thread INT
+
+      // Old State -> Transition - labeled with the last output if any.
+      gdfEdges.add(
+      		makeGdfEdgeString("st"+old_id, "tr"+my_id,
+      				          makeGdfLabel(state, my_id),
+      				          thread, lastoutput));
 
-      // 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);
+      // Transition -> New State - labeled with the source info if any.
+      gdfEdges.add(
+      		makeGdfEdgeString("tr"+my_id, "st"+new_id, lastoutput, thread,
+      				           lastoutput));
     } else { // DOT
       graph.write("  st" + old_id + " -> tr" + my_id + ";");
       graph.newLine();
@@ -404,6 +471,25 @@
     }
   }
 
+  /**
+   * Show the usage message.
+   */
+  static void showUsage() {
+    System.out
+        .println("Usage: \"java [<vm-options>] gov.nasa.jpf.tools.StateSpaceDot [<graph-options>] [<jpf-options-and-args>]");
+    System.out.println("  <graph-options> : ");
+    System.out.println("    -gdf:                Generate the graph in GDF format. The default is DOT.");
+    System.out.println("    -transition-numbers: Include transition numbers in transition labels.");
+    System.out.println("    -show-source:        Include source lines in transition labels.");
+    System.out.println("    -labelvisible:       Indicates if the label on the transitions is visible (used only with the -gdf option)");
+    System.out.println("    -help:               Prints this help information and stops.");
+    System.out.println("  <jpf-options-and-args>:");
+    System.out.println("    Options and command line arguments passed directly to JPF.");
+    System.out.println("  Note: With -gdf option transition edges could also include program output ");
+    System.out.println("  but in order to enable this JPF's vm.path_output option must be set to ");
+    System.out.println("  true.");
+  }
+
   void filterArgs (String[] args) {
     for (int i=0; i<args.length; i++) {
       String arg = args[i];
@@ -420,14 +506,20 @@
       } else if ("-labelvisible".equals(arg)) {
        	labelvisible=true;
         args[i] = null;      	
+      } else if  ("-help".equals(args[i])) {
+      	showUsage();
+      	helpRequested=true;
       }
     }    
   }
-
+  
   public static void main(String [] args) {
     StateSpaceDot listener = new StateSpaceDot();
     listener.filterArgs(args);
-
+    if (helpRequested==true) {
+    	return;
+    }
+    
     Config conf = JPF.createConfig(args);
     // do own settings here