src/main/gov/nasa/jpf/listener/StateSpaceDot.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.listener;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.Error;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.ListenerAdapter;
  24 import gov.nasa.jpf.search.Search;
  25 import gov.nasa.jpf.vm.VM;
  26 import gov.nasa.jpf.vm.Step;
  27 import gov.nasa.jpf.vm.Transition;
  28
  29 import java.io.BufferedWriter;
  30 import java.io.FileWriter;
  31 import java.io.IOException;
  32 import java.util.ArrayList;
  33 import java.util.List;
  34
  35 /*
  36  * Add a state space observer to JPF and build a graph of the state space
  37  * that is explored by JPF. The graph can be generated in different formats.
  38  * The current formats that are supported are DOT (visualized by a tool
  39  * like GraphViz from ATT - http://www.graphviz.org/) and gdf (used by GUESS
  40  * from HP - http://www.hpl.hp.com/research/idl/projects/graphs/).
  41  * The graph is stored in a file called "jpf-state-space.<extension>" where
  42  * extension is ".dot" or ".gdf". By default it generates a DOT graph.
  43  *
  44  * Options:
  45  *   -gdf:                Generate the graph in GDF format. The default is DOT.
  46  *   -transition-numbers: Include transition numbers in transition labels.
  47  *   -show-source:        Include source lines in transition labels.
  48  *   -labelvisible:       Indicates if the label on the transitions is visible (used only with the -gdf option)
  49  *   -help:               Prints this help information and stops.
  50  *
  51  * @date 9/12/03
  52  * @author Owen O'Malley (Initial version generating the DOT graph)
  53  *
  54  * @date 7/17/05
  55  * @author Masoud Mansouri-Samani (Extended to also generate the gdf graph)
  56  */
  57 public class StateSpaceDot extends ListenerAdapter {
  58   // NODE styles constants
  59   static final int RECTANGLE = 1;
  60   static final int ELLIPSE   = 2;
  61   static final int ROUND_RECTANGLE = 3;
  62   static final int RECTANGLE_WITH_TEXT = 4;
  63   static final int ELLIPSE_WITH_TEXT = 5;
  64   static final int ROUND_RECTANGLE_WITH_TEXT = 6;
  65
  66   private static final String DOT_EXT = "dot";
  67   private static final String GDF_EXT = "gdf";
  68   private static final String OUT_FILENAME_NO_EXT = "jpf-state-space";
  69
  70   // State and transition node styles used
  71   private static final int state_node_style = ELLIPSE_WITH_TEXT;
  72   private static final int transition_node_style = RECTANGLE_WITH_TEXT;
  73
  74   // File formats supported
  75   private static final int DOT_FORMAT=0;
  76   private static final int GDF_FORMAT=1;
  77
  78   private BufferedWriter graph = null;
  79   private int edge_id = 0;
  80   private static boolean transition_numbers=false;
  81   private static boolean show_source=false;
  82   private static int format=DOT_FORMAT;
  83   private String out_filename = OUT_FILENAME_NO_EXT+"."+DOT_EXT;
  84   private static boolean labelvisible=false;
  85   private static boolean helpRequested=false;
  86
  87
  88   /* In gdf format all the edges must come after all the nodes of the graph
  89    * are generated. So we first output the nodes as we come across them but
  90    * we store the strings for edges in the gdfEdges list and output them when
  91    * the search ends.
  92    */
  93   ArrayList<String> gdfEdges=new ArrayList<String>();
  94
  95   private StateInformation prev_state = null;
  96
  97   public StateSpaceDot(Config conf, JPF jpf) {
  98
  99     VM vm = jpf.getVM();
 100     vm.recordSteps(true);
 101   }
 102
 103   @Override
 104   public void searchStarted(Search search) {
 105     try {
 106       beginGraph();
 107     } catch (IOException e) {}
 108   }
 109
 110   @Override
 111   public void searchFinished(Search search) {
 112     try {
 113       endGraph();
 114     } catch (IOException e) {}
 115   }
 116
 117   @Override
 118   public void stateAdvanced(Search search) {
 119     int id = search.getStateId();
 120     boolean has_next =search.hasNextState();
 121     boolean is_new = search.isNewState();
 122     try {
 123       if (format==DOT_FORMAT) {
 124         graph.write("/* searchAdvanced(" + id + ", " + makeDotLabel(search, id) +
 125                     ", " + has_next + ") */");
 126         graph.newLine();
 127       }
 128       if (prev_state != null) {
 129         addEdge(prev_state.id, id, search);
 130       } else {
 131         prev_state = new StateInformation();
 132       }
 133       addNode(prev_state);
 134       prev_state.reset(id, has_next, is_new);
 135     } catch (IOException e) {}
 136   }
 137
 138   @Override
 139   public void stateRestored (Search search) {
 140     prev_state.reset(search.getStateId(), false, false);
 141   }
 142
 143   @Override
 144   public void stateProcessed (Search search) {
 145    // nothing to do
 146   }
 147
 148   @Override
 149   public void stateBacktracked(Search search) {
 150     try {
 151       addNode(prev_state);
 152       prev_state.reset(search.getStateId(), false, false);
 153       if (format==DOT_FORMAT) {
 154         graph.write("/* searchBacktracked(" + prev_state + ") */");
 155         graph.newLine();
 156       }
 157     } catch (IOException e) {}
 158   }
 159
 160   @Override
 161   public void searchConstraintHit(Search search) {
 162     try {
 163       if (format==DOT_FORMAT) {
 164         graph.write("/* searchConstraintHit(" + search.getStateId() + ") */");
 165         graph.newLine();
 166       }
 167     } catch (IOException e) {}
 168   }
 169
 170   private String getErrorMsg(Search search) {
 171     List<Error> errs = search.getErrors();
 172     if (errs.isEmpty()) {
 173       return null;
 174     } else {
 175       return errs.get(0).getDescription();
 176     }
 177   }
 178
 179   @Override
 180   public void propertyViolated(Search search) {
 181         try {
 182           prev_state.error = getErrorMsg(search);
 183           if (format==DOT_FORMAT) {
 184             graph.write("/* propertyViolated(" + search.getStateId() + ") */");
 185             graph.newLine();
 186           }
 187         } catch (IOException e) {}
 188   }
 189
 190   /**
 191    * Put the header for the graph into the file.
 192    */
 193   private void beginGraph() throws IOException {
 194         graph = new BufferedWriter(new FileWriter(out_filename));
 195         if (format==GDF_FORMAT) {
 196           graph.write("nodedef>name,label,style,color");
 197         } else { // dot
 198           graph.write("digraph jpf_state_space {");
 199         }
 200         graph.newLine();
 201   }
 202
 203   /**
 204    * In the case of the DOT graph it is just adding the final "}" at the end.
 205    * In the case of GPF format we must output edge definition and all the
 206    * edges that we have found.
 207    */
 208   private void endGraph() throws IOException {
 209     if(prev_state != null)
 210       addNode(prev_state);
 211     if (format==GDF_FORMAT) {
 212       graph.write("edgedef>node1,node2,label,labelvisible,directed,thread INT");
 213       graph.newLine();
 214
 215       // Output all the edges that we have accumulated so far
 216       int size=gdfEdges.size();
 217           for (int i=0; i<size; i++) {
 218                 graph.write(gdfEdges.get(i));
 219             graph.newLine();
 220           }
 221     } else {
 222       graph.write("}");
 223       graph.newLine();
 224     }
 225     graph.close();
 226   }
 227
 228   /**
 229    * Return the string that will be used to label this state for the user.
 230    */
 231   private String makeDotLabel(Search state, int my_id) {
 232     Transition trans = state.getTransition();
 233     if (trans == null) {
 234       return "-init-";
 235     }
 236     Step last_trans_step = trans.getLastStep();
 237     if (last_trans_step == null) {
 238       return "?";
 239     }
 240
 241     StringBuilder result = new StringBuilder();
 242
 243     if (transition_numbers) {
 244       result.append(my_id);
 245       result.append("\\n");
 246     }
 247
 248     int thread = trans.getThreadIndex();
 249
 250     result.append("Thd");
 251     result.append(thread);
 252     result.append(':');
 253     result.append(last_trans_step.toString());
 254
 255     if (show_source) {
 256       String source_line=last_trans_step.getLineString();
 257       if ((source_line != null) && !source_line.equals("")) {
 258         result.append("\\n");
 259
 260         StringBuilder sb=new StringBuilder(source_line);
 261
 262         // We need to precede the dot-specific special characters which appear
 263         // in the Java source line, such as ']' and '"', with the '\' escape
 264         // characters and also to remove any new lines.
 265
 266         replaceString(sb, "\n", "");
 267         replaceString(sb, "]", "\\]");
 268         replaceString(sb, "\"", "\\\"");
 269         result.append(sb.toString());
 270       }
 271     }
 272
 273     return result.toString();
 274   }
 275
 276   /**
 277    * Return the string that will be used to label this state in the GDF graph.
 278    */
 279   private String makeGdfLabel(Search state, int my_id) {
 280     Transition trans = state.getTransition();
 281     if (trans == null) {
 282           return "-init-";
 283         }
 284
 285         StringBuilder result = new StringBuilder();
 286
 287         if (transition_numbers) {
 288           result.append(my_id);
 289           result.append(':');
 290         }
 291
 292         Step last_trans_step = trans.getLastStep();
 293         result.append(last_trans_step.toString());
 294
 295         if (show_source) {
 296           String source_line=last_trans_step.getLineString();
 297           if ((source_line != null) && !source_line.equals("")) {
 298
 299             // We need to deal with gdf-specific special characters which couls appear
 300             // in the Java source line, such as '"'.
 301             result.append(source_line);
 302                 convertGdfSpecial(result);
 303           }
 304     }
 305         return result.toString();
 306   }
 307
 308   /**
 309    * Locates and replaces all occurrences of a given string with another given
 310    * string in an original string buffer. There seems to be a bug in Java
 311    * String's replaceAll() method which does not allow us to use it to replace
 312    * some special chars so here we use StringBuilder's replace method to do
 313    * this.
 314    * @param original The original string builder.
 315    * @param from The replaced string.
 316    * @param to The replacing string.
 317    * @return The original string builder with the substring replaced
 318    *         throughout.
 319    */
 320   private StringBuilder replaceString(StringBuilder original,
 321                                       String from,
 322                                       String to) {
 323     int indexOfReplaced=0, lastIndexOfReplaced=0;
 324     while (indexOfReplaced!=-1) {
 325       indexOfReplaced=original.indexOf(from,lastIndexOfReplaced);
 326       if (indexOfReplaced!=-1) {
 327         original.replace(indexOfReplaced, indexOfReplaced+1, to);
 328         lastIndexOfReplaced=indexOfReplaced+to.length();
 329       }
 330     }
 331     return original;
 332   }
 333
 334   /**
 335    * Locates and replaces all occurrences of a given string with another given
 336    * string in an original string buffer.
 337    * @param original The original string buffer.
 338    * @param from The replaced string.
 339    * @param to The replacing string.
 340    * @return The original string buffer with the sub-string replaced
 341    *         throughout.
 342    */
 343   private String replaceString(String original, String from, String to) {
 344         if ((original!=null) && (from!=null) && (to!=null)) {
 345       return replaceString(new StringBuilder(original), from, to).toString();
 346         } else {
 347       return original;
 348         }
 349   }
 350
 351   /**
 352    * Add a new node to the graph with the relevant properties.
 353    */
 354   private void addNode(StateInformation state) throws IOException {
 355     if (state.is_new) {
 356       if (format==GDF_FORMAT) {
 357         graph.write("st" + state.id + ",\"" + state.id);
 358         if (state.error != null) {
 359           graph.write(":" + state.error);
 360         }
 361         graph.write("\","+state_node_style);
 362         if (state.error != null) {
 363             graph.write(",red");
 364           } else if (state.has_next) {
 365             graph.write(",black");
 366           } else {
 367             graph.write(",green");
 368           }
 369       } else { // The dot version
 370         graph.write("  st" + state.id + " [label=\"" + state.id);
 371         if (state.error != null) {
 372           graph.write(":" + state.error);
 373         }
 374         graph.write("\",shape=");
 375         if (state.error != null) {
 376           graph.write("diamond,color=red");
 377         } else if (state.has_next) {
 378           graph.write("circle,color=black");
 379         } else {
 380           graph.write("egg,color=green");
 381         }
 382         graph.write("];");
 383       }
 384       graph.newLine();
 385     }
 386   }
 387
 388   private static class StateInformation {
 389     public StateInformation() {}
 390     public void reset(int id, boolean has_next, boolean is_new) {
 391       this.id = id;
 392       this.has_next = has_next;
 393       this.error = null;
 394       this.is_new = is_new;
 395     }
 396     int id = -1;
 397     boolean has_next = true;
 398     String error = null;
 399     boolean is_new = false;
 400   }
 401
 402   /**
 403    * Creates an GDF edge string.
 404    */
 405   private String makeGdfEdgeString(String from_id,
 406                                            String to_id,
 407                                                                    String label,
 408                                                                    int thread) {
 409         StringBuilder sb=new StringBuilder(from_id);
 410         sb.append(',').append(to_id).append(',').append('\"');
 411         if ((label!=null) && (!"".equals(label))) {
 412                 sb.append(label);
 413         } else {
 414                 sb.append('-');
 415         }
 416         sb.append('\"').append(',').append(labelvisible).append(',').append(true).
 417         append(',').append(thread);
 418         replaceString(sb, "\n", "");
 419         return sb.toString();
 420   }
 421
 422   /**
 423    * GUESS cannot deal with '\n' chars, so remove them. Also convert all '"'
 424    * characters to "''".
 425    * @param str The string to perform the conversion on.
 426    * @return The converted string.
 427    */
 428   private String convertGdfSpecial(String str) {
 429         if ((str==null) || "".equals(str)) return "";
 430
 431         StringBuilder sb=new StringBuilder(str);
 432         convertGdfSpecial(sb);
 433         return sb.toString();
 434   }
 435
 436   /**
 437    * GUESS cannot deal with '\n' chars, so replace them with a space. Also
 438    * convert all '"' characters to "''".
 439    * @param sb The string buffer to perform the conversion on.
 440    */
 441   private void convertGdfSpecial(StringBuilder sb) {
 442         replaceString(sb, "\"", "\'\'");
 443         replaceString(sb, "\n", " ");
 444   }
 445
 446   /**
 447    * Create an edge in the graph file from old_id to new_id.
 448    */
 449   private void addEdge(int old_id, int new_id, Search state) throws IOException {
 450     int my_id = edge_id++;
 451     if (format==GDF_FORMAT) {
 452       Transition trans=state.getTransition();
 453       int thread = trans.getThreadIndex();
 454
 455       // edgedef>node1,node2,label,labelvisible,directed,thread INT
 456
 457       // Old State -> Transition - labeled with the source info if any.
 458       gdfEdges.add(
 459                 makeGdfEdgeString("st"+old_id, "tr"+my_id,
 460                                           makeGdfLabel(state, my_id),
 461                                           thread));
 462
 463       // Transition node: name,label,style,color
 464       graph.write("tr" + my_id + ",\"" +my_id+"\","+transition_node_style);
 465
 466       graph.newLine();
 467       // Transition -> New State - labeled with the last output if any.
 468
 469       String lastOutputLabel=
 470         replaceString(convertGdfSpecial(trans.getOutput()), "\"", "\'\'");
 471       gdfEdges.add(
 472         makeGdfEdgeString("tr"+my_id, "st"+new_id, lastOutputLabel, thread));
 473     } else { // DOT
 474       graph.write("  st" + old_id + " -> tr" + my_id + ";");
 475       graph.newLine();
 476       graph.write("  tr" + my_id + " [label=\"" + makeDotLabel(state, my_id) +
 477                   "\",shape=box]");
 478       graph.newLine();
 479       graph.write("  tr" + my_id + " -> st" + new_id + ";");
 480     }
 481   }
 482
 483   /**
 484    * Show the usage message.
 485    */
 486   static void showUsage() {
 487     System.out
 488         .println("Usage: \"java [<vm-options>] gov.nasa.jpf.tools.StateSpaceDot [<graph-options>] [<jpf-options-and-args>]");
 489     System.out.println("  <graph-options> : ");
 490     System.out.println("    -gdf:                Generate the graph in GDF format. The default is DOT.");
 491     System.out.println("    -transition-numbers: Include transition numbers in transition labels.");
 492     System.out.println("    -show-source:        Include source lines in transition labels.");
 493     System.out.println("    -labelvisible:       Indicates if the label on the transitions is visible (used only with the -gdf option)");
 494     System.out.println("    -help:               Prints this help information and stops.");
 495     System.out.println("  <jpf-options-and-args>:");
 496     System.out.println("    Options and command line arguments passed directly to JPF.");
 497     System.out.println("  Note: With -gdf option transition edges could also include program output ");
 498     System.out.println("  but in order to enable this JPF's vm.path_output option must be set to ");
 499     System.out.println("  true.");
 500   }
 501
 502   void filterArgs (String[] args) {
 503     for (int i=0; i<args.length; i++) {
 504       if (args[i] != null){
 505         String arg = args[i];
 506         if ("-transition-numbers".equals(arg)) {
 507           transition_numbers = true;
 508           args[i] = null;
 509         } else if ("-show-source".equals(arg)) {
 510           show_source = true;
 511           args[i] = null;
 512         } else if ("-gdf".equals(arg)) {
 513           format=GDF_FORMAT;
 514           out_filename=OUT_FILENAME_NO_EXT+"."+GDF_EXT;
 515           args[i] = null;
 516         } else if ("-labelvisible".equals(arg)) {
 517           labelvisible=true;
 518           args[i] = null;
 519         } else if  ("-help".equals(args[i])) {
 520           showUsage();
 521           helpRequested=true;
 522         }
 523       }
 524     }
 525   }
 526
 527 }