Java > Open Source Codes > gov > nasa > jpf > tools > StateSpaceDot


1 //
2 // Copyright (C) 2005 United States Government as represented by the
3 // Administrator of the National Aeronautics and Space Administration
4 // (NASA). All Rights Reserved.
5 //
6 // This software is distributed under the NASA Open Source Agreement
7 // (NOSA), version 1.3. The NOSA has been approved by the Open Source
8 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9 // directory tree for the complete NOSA document.
10 //
11 // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12 // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13 // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14 // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15 // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16 // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17 // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18 //
19
20 package gov.nasa.jpf.tools;
21
22 import gov.nasa.jpf.ErrorList;
23 import gov.nasa.jpf.JPF;
24 import gov.nasa.jpf.Config;
25 import gov.nasa.jpf.Search;
26 import gov.nasa.jpf.SearchListener;
27 import gov.nasa.jpf.Transition;
28 import gov.nasa.jpf.TransitionStep;
29 import java.io.BufferedWriter ;
30 import java.io.FileWriter ;
31 import java.io.IOException ;
32 import java.util.Iterator ;
33 import java.util.ArrayList ;
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 implements SearchListener {
58   private static final String DOT_EXT = "dot";
59   private static final String GDF_EXT = "gdf";
60   private static final String OUT_FILENAME_NO_EXT = "jpf-state-space";
61
62   // NODE styles constants
63 private static final int RECTABGLE = 1;
64   private static final int ELLIPSE = 2;
65   private static final int ROUND_RECTABGLE = 3;
66   private static final int RECTABGLE_WITH_TEXT = 4;
67   private static final int ELLIPSE_WITH_TEXT = 5;
68   private static final int ROUND_RECTABGLE_WITH_TEXT = 6;
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=RECTABGLE_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 gdfEdges=new ArrayList ();
94
95   private StateInformation prev_state = null;
96
97   public StateSpaceDot() {}
98
99   public void searchStarted(Search search) {
100     try {
101       beginGraph();
102     } catch (IOException e) {}
103   }
104
105   public void searchFinished(Search search) {
106     try {
107       endGraph();
108     } catch (IOException e) {}
109   }
110
111   public void stateAdvanced(Search search) {
112     int id = search.getStateNumber();
113     boolean has_next =search.hasNextState();
114     boolean is_new = search.isNewState();
115     try {
116       if (format==DOT_FORMAT) {
117         graph.write("/* searchAdvanced(" + id + ", " + makeDotLabel(search, id) +
118                     ", " + has_next + ") */");
119         graph.newLine();
120       }
121       if (prev_state != null) {
122         addEdge(prev_state.id, id, search);
123       } else {
124         prev_state = new StateInformation();
125       }
126       addNode(prev_state);
127       prev_state.reset(id, has_next, is_new);
128     } catch (IOException e) {}
129   }
130
131   public void stateRestored (Search search) {
132     prev_state.reset(search.getStateNumber(), false, false);
133   }
134
135   public void stateProcessed (Search search) {
136    // nothing to do
137 }
138
139   public void stateBacktracked(Search search) {
140     try {
141       addNode(prev_state);
142       prev_state.reset(search.getStateNumber(), false, false);
143       if (format==DOT_FORMAT) {
144         graph.write("/* searchBacktracked(" + prev_state + ") */");
145         graph.newLine();
146       }
147     } catch (IOException e) {}
148   }
149
150   public void searchConstraintHit(Search search) {
151     try {
152       if (format==DOT_FORMAT) {
153         graph.write("/* searchConstraintHit(" + search.getStateNumber() + ") */");
154         graph.newLine();
155       }
156     } catch (IOException e) {}
157   }
158   
159   private String getErrorMsg(Search search) {
160     ErrorList errs = search.getErrors();
161     Iterator itr = errs.iterator();
162     while (itr.hasNext()) {
163       return ((gov.nasa.jpf.Error) itr.next()).getMessage();
164     }
165     return null;
166   }
167
168   public void propertyViolated(Search search) {
169     try {
170       prev_state.error = getErrorMsg(search);
171       if (format==DOT_FORMAT) {
172         graph.write("/* propertyViolated(" + search.getStateNumber() + ") */");
173         graph.newLine();
174       }
175     } catch (IOException e) {}
176   }
177
178   /**
179    * Put the header for the graph into the file.
180    */
181   private void beginGraph() throws IOException {
182     graph = new BufferedWriter (new FileWriter (out_filename));
183     if (format==GDF_FORMAT) {
184       graph.write("nodedef>name,label,style,color");
185     } else { // dot
186 graph.write("digraph jpf_state_space {");
187     }
188     graph.newLine();
189   }
190
191   /**
192    * In the case of the DOT graph it is just adding the final "}" at the end.
193    * In the case of GPF format we must output edge definition and all the
194    * edges that we have found.
195    */
196   private void endGraph() throws IOException {
197     addNode(prev_state);
198     if (format==GDF_FORMAT) {
199       graph.write("edgedef>node1,node2,label,labelvisible,directed,thread INT");
200       graph.newLine();
201
202       // Output all the edges that we have accumulated so far
203 int size=gdfEdges.size();
204       for (int i=0; i<size; i++) {
205         graph.write((String ) gdfEdges.get(i));
206         graph.newLine();
207       }
208     } else {
209       graph.write("}");
210       graph.newLine();
211     }
212     graph.close();
213   }
214
215   /**
216    * Return the string that will be used to label this state for the user.
217    */
218   private String makeDotLabel(Search state, int my_id) {
219     Transition trans = state.getTransition();
220     if (trans == null) {
221       return "-init-";
222     }
223
224     StringBuffer result = new StringBuffer ();
225
226     if (transition_numbers) {
227       result.append(my_id);
228       result.append("\\n");
229     }
230
231     TransitionStep last_trans_step = trans.getLastTransitionStep();
232
233     int thread = trans.getThread();
234
235     result.append("Thd");
236     result.append(thread);
237     result.append(":");
238
239     result.append(last_trans_step.getSourceRef().toString());
240
241     if (show_source) {
242       String source_line=last_trans_step.getSourceRef().getLineString();
243       if ((source_line != null) && !source_line.equals("")) {
244         result.append("\\n");
245
246         StringBuffer sb=new StringBuffer (source_line);
247      
248         // We need to precede the dot-specific special characters which appear
249 // in the Java source line, such as ']' and '"', with the '\' escape
250 // characters and also to remove any new lines.
251
252         replaceString(sb, "\n", "");
253         replaceString(sb, "]", "\\]");
254         replaceString(sb, "\"", "\\\"");
255         result.append(sb.toString());
256       }
257     }
258
259     return result.toString();
260   }
261
262   /**
263    * Return the string that will be used to label this state in the GDF graph.
264    */
265   private String makeGdfLabel(Search state, int my_id) {
266     Transition trans = state.getTransition();
267     if (trans == null) {
268       return "-init-";
269     }
270     
271     StringBuffer result = new StringBuffer ();
272
273     if (transition_numbers) {
274       result.append(my_id);
275       result.append(":");
276     }
277
278     TransitionStep last_trans_step = trans.getLastTransitionStep();
279     result.append(last_trans_step.getSourceRef().toString());
280
281     if (show_source) {
282       String source_line=last_trans_step.getSourceRef().getLineString();
283       if ((source_line != null) && !source_line.equals("")) {
284
285         // We need to deal with gdf-specific special characters which couls appear
286 // in the Java source line, such as '"'.
287 result.append(source_line);
288         convertGdfSpecial(result);
289       }
290     }
291     return result.toString();
292   }
293
294   /**
295    * Locates and replaces all occurrences of a given string with another given
296    * string in an original string buffer. There seems to be a bug in Java
297    * String's replaceAll() method which does not allow us to use it to replace
298    * some special chars so here we use StringBuffer's replace method to do
299    * this.
300    * @param original The original string buffer.
301    * @param from The replaced string.
302    * @param to The replacing string.
303    * @return The original string buffer with the sub-string replaced
304    * throughout.
305    */
306   private StringBuffer replaceString(StringBuffer original,
307                                      String from,
308                                      String to) {
309     int indexOfReplaced=0, lastIndexOfReplaced=0;
310     while (indexOfReplaced!=-1) {
311       indexOfReplaced=original.indexOf(from,lastIndexOfReplaced);
312       if (indexOfReplaced!=-1) {
313         original.replace(indexOfReplaced, indexOfReplaced+1, to);
314         lastIndexOfReplaced=indexOfReplaced+to.length();
315       }
316     }
317     return original;
318   }
319   
320   /**
321    * Locates and replaces all occurrences of a given string with another given
322    * string in an original string buffer.
323    * @param original The original string buffer.
324    * @param from The replaced string.
325    * @param to The replacing string.
326    * @return The original string buffer with the sub-string replaced
327    * throughout.
328    */
329   private String replaceString(String original, String from, String to) {
330     if ((original!=null) && (from!=null) && (to!=null)) {
331       return replaceString(new StringBuffer (original), from, to).toString();
332     } else {
333       return original;
334     }
335   }
336
337   /**
338    * Add a new node to the graph with the relevant properties.
339    */
340   private void addNode(StateInformation state) throws IOException {
341     if (state.is_new) {
342       if (format==GDF_FORMAT) {
343         graph.write("st" + state.id + ",\"" + state.id);
344         if (state.error != null) {
345           graph.write(":" + state.error);
346         }
347         graph.write("\","+state_node_style);
348         if (state.error != null) {
349             graph.write(",red");
350           } else if (state.has_next) {
351             graph.write(",black");
352           } else {
353             graph.write(",green");
354           }
355       } else { // The dot version
356 graph.write(" st" + state.id + " [label=\"" + state.id);
357         if (state.error != null) {
358           graph.write(":" + state.error);
359         }
360         graph.write("\",shape=");
361         if (state.error != null) {
362           graph.write("diamond,color=red");
363         } else if (state.has_next) {
364           graph.write("circle,color=black");
365         } else {
366           graph.write("egg,color=green");
367         }
368         graph.write("];");
369       }
370       graph.newLine();
371     }
372   }
373
374   private static class StateInformation {
375     public StateInformation() {}
376     public void reset(int id, boolean has_next, boolean is_new) {
377       this.id = id;
378       this.has_next = has_next;
379       this.error = null;
380       this.is_new = is_new;
381     }
382     int id = -1;
383     boolean has_next = true;
384     String error = null;
385     boolean is_new = false;
386   }
387
388   /**
389    * Creates an GDF edge string.
390    */
391   private String makeGdfEdgeString(String from_id,
392                                    String to_id,
393                                    String label,
394                                    int thread) {
395     StringBuffer sb=new StringBuffer ();
396     sb.append(from_id).append(',').append(to_id).append(',').
397       append('\"');
398     if ((label!=null) && (!"".equals(label))) {
399         sb.append(label);
400     } else {
401         sb.append('-');
402     }
403     sb.append('\"').append(',').append(labelvisible).append(',').append(true).
404     append(',').append(thread);
405     replaceString(sb, "\n", "");
406     return sb.toString();
407   }
408
409   /**
410    * GUESS cannot deal with '\n' chars, so remove them. Also convert all '"'
411    * characters to "''".
412    * @param str The string to perform the conversion on.
413    * @return The converted string.
414    */
415   private String convertGdfSpecial(String str) {
416     if ((str==null) || "".equals(str)) return "";
417     
418     StringBuffer sb=new StringBuffer (str);
419     convertGdfSpecial(sb);
420     return sb.toString();
421   }
422   
423   /**
424    * GUESS cannot deal with '\n' chars, so replace them with a space. Also
425    * convert all '"' characters to "''".
426    * @param sb The string buffer to perform the conversion on.
427    */
428   private void convertGdfSpecial(StringBuffer sb) {
429     replaceString(sb, "\"", "\'\'");
430     replaceString(sb, "\n", " ");
431   }
432
433   /**
434    * Create an edge in the graph file from old_id to new_id.
435    */
436   private void addEdge(int old_id, int new_id, Search state) throws IOException {
437     int my_id = edge_id++;
438     if (format==GDF_FORMAT) {
439       Transition trans=state.getTransition();
440       int thread = trans.getThread();
441       
442       // edgedef>node1,node2,label,labelvisible,directed,thread INT
443
444       // Old State -> Transition - labeled with the source info if any.
445 gdfEdges.add(
446             makeGdfEdgeString("st"+old_id, "tr"+my_id,
447                               makeGdfLabel(state, my_id),
448                               thread));
449
450       // Transition node: name,label,style,color
451 graph.write("tr" + my_id + ",\"" +my_id+"\","+transition_node_style);
452       
453       graph.newLine();
454       // Transition -> New State - labeled with the last output if any.
455
456       String lastOutputLabel=
457         replaceString(convertGdfSpecial(trans.getOutput()), "\"", "\'\'");
458       gdfEdges.add(
459         makeGdfEdgeString("tr"+my_id, "st"+new_id, lastOutputLabel, thread));
460     } else { // DOT
461 graph.write(" st" + old_id + " -> tr" + my_id + ";");
462       graph.newLine();
463       graph.write(" tr" + my_id + " [label=\"" + makeDotLabel(state, my_id) +
464                   "\",shape=box]");
465       graph.newLine();
466       graph.write(" tr" + my_id + " -> st" + new_id + ";");
467     }
468   }
469
470   /**
471    * Show the usage message.
472    */
473   static void showUsage() {
474     System.out
475         .println("Usage: \"java [<vm-options>] gov.nasa.jpf.tools.StateSpaceDot [<graph-options>] [<jpf-options-and-args>]");
476     System.out.println(" <graph-options> : ");
477     System.out.println(" -gdf: Generate the graph in GDF format. The default is DOT.");
478     System.out.println(" -transition-numbers: Include transition numbers in transition labels.");
479     System.out.println(" -show-source: Include source lines in transition labels.");
480     System.out.println(" -labelvisible: Indicates if the label on the transitions is visible (used only with the -gdf option)");
481     System.out.println(" -help: Prints this help information and stops.");
482     System.out.println(" <jpf-options-and-args>:");
483     System.out.println(" Options and command line arguments passed directly to JPF.");
484     System.out.println(" Note: With -gdf option transition edges could also include program output ");
485     System.out.println(" but in order to enable this JPF's vm.path_output option must be set to ");
486     System.out.println(" true.");
487   }
488
489   void filterArgs (String [] args) {
490     for (int i=0; i<args.length; i++) {
491       String arg = args[i];
492       if ("-transition-numbers".equals(arg)) {
493         transition_numbers = true;
494         args[i] = null;
495       } else if ("-show-source".equals(arg)) {
496         show_source = true;
497         args[i] = null;
498       } else if ("-gdf".equals(arg)) {
499         format=GDF_FORMAT;
500         out_filename=OUT_FILENAME_NO_EXT+"."+GDF_EXT;
501         args[i] = null;
502       } else if ("-labelvisible".equals(arg)) {
503         labelvisible=true;
504         args[i] = null;
505       } else if ("-help".equals(args[i])) {
506         showUsage();
507         helpRequested=true;
508       }
509     }
510   }
511   
512   public static void main(String [] args) {
513     StateSpaceDot listener = new StateSpaceDot();
514
515     System.out.println("JPF State Space dot Graph Generator");
516     listener.filterArgs(args);
517
518     System.out.println("...graph output to " + listener.out_filename + "...");
519
520     if (helpRequested==true) {
521         return;
522     }
523     
524     Config conf = JPF.createConfig(args);
525     // do own settings here
526
527     JPF jpf = new JPF(conf);
528     jpf.addSearchListener(listener);
529
530     System.out.println("...running JPF...");
531     jpf.run();
532   }
533 }
534

A to Z: JavaDoc & Examples

---

Daily Java News & Articles

---

Open Source Projects

---

Open Source Codes

---

Free Computer Books

---

Remove Frame

---

Popular Tags