2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.listener;
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;
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;
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.
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.
52 * @author Owen O'Malley (Initial version generating the DOT graph)
55 * @author Masoud Mansouri-Samani (Extended to also generate the gdf graph)
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;
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";
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;
74 // File formats supported
75 private static final int DOT_FORMAT=0;
76 private static final int GDF_FORMAT=1;
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;
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
93 ArrayList<String> gdfEdges=new ArrayList<String>();
95 private StateInformation prev_state = null;
97 public StateSpaceDot(Config conf, JPF jpf) {
100 vm.recordSteps(true);
104 public void searchStarted(Search search) {
107 } catch (IOException e) {}
111 public void searchFinished(Search search) {
114 } catch (IOException e) {}
118 public void stateAdvanced(Search search) {
119 int id = search.getStateId();
120 boolean has_next =search.hasNextState();
121 boolean is_new = search.isNewState();
123 if (format==DOT_FORMAT) {
124 graph.write("/* searchAdvanced(" + id + ", " + makeDotLabel(search, id) +
125 ", " + has_next + ") */");
128 if (prev_state != null) {
129 addEdge(prev_state.id, id, search);
131 prev_state = new StateInformation();
134 prev_state.reset(id, has_next, is_new);
135 } catch (IOException e) {}
139 public void stateRestored (Search search) {
140 prev_state.reset(search.getStateId(), false, false);
144 public void stateProcessed (Search search) {
149 public void stateBacktracked(Search search) {
152 prev_state.reset(search.getStateId(), false, false);
153 if (format==DOT_FORMAT) {
154 graph.write("/* searchBacktracked(" + prev_state + ") */");
157 } catch (IOException e) {}
161 public void searchConstraintHit(Search search) {
163 if (format==DOT_FORMAT) {
164 graph.write("/* searchConstraintHit(" + search.getStateId() + ") */");
167 } catch (IOException e) {}
170 private String getErrorMsg(Search search) {
171 List<Error> errs = search.getErrors();
172 if (errs.isEmpty()) {
175 return errs.get(0).getDescription();
180 public void propertyViolated(Search search) {
182 prev_state.error = getErrorMsg(search);
183 if (format==DOT_FORMAT) {
184 graph.write("/* propertyViolated(" + search.getStateId() + ") */");
187 } catch (IOException e) {}
191 * Put the header for the graph into the file.
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");
198 graph.write("digraph jpf_state_space {");
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.
208 private void endGraph() throws IOException {
209 if(prev_state != null)
211 if (format==GDF_FORMAT) {
212 graph.write("edgedef>node1,node2,label,labelvisible,directed,thread INT");
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));
229 * Return the string that will be used to label this state for the user.
231 private String makeDotLabel(Search state, int my_id) {
232 Transition trans = state.getTransition();
236 Step last_trans_step = trans.getLastStep();
237 if (last_trans_step == null) {
241 StringBuilder result = new StringBuilder();
243 if (transition_numbers) {
244 result.append(my_id);
245 result.append("\\n");
248 int thread = trans.getThreadIndex();
250 result.append("Thd");
251 result.append(thread);
253 result.append(last_trans_step.toString());
256 String source_line=last_trans_step.getLineString();
257 if ((source_line != null) && !source_line.equals("")) {
258 result.append("\\n");
260 StringBuilder sb=new StringBuilder(source_line);
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.
266 replaceString(sb, "\n", "");
267 replaceString(sb, "]", "\\]");
268 replaceString(sb, "\"", "\\\"");
269 result.append(sb.toString());
273 return result.toString();
277 * Return the string that will be used to label this state in the GDF graph.
279 private String makeGdfLabel(Search state, int my_id) {
280 Transition trans = state.getTransition();
285 StringBuilder result = new StringBuilder();
287 if (transition_numbers) {
288 result.append(my_id);
292 Step last_trans_step = trans.getLastStep();
293 result.append(last_trans_step.toString());
296 String source_line=last_trans_step.getLineString();
297 if ((source_line != null) && !source_line.equals("")) {
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);
305 return result.toString();
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
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
320 private StringBuilder replaceString(StringBuilder original,
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();
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
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();
352 * Add a new node to the graph with the relevant properties.
354 private void addNode(StateInformation state) throws IOException {
356 if (format==GDF_FORMAT) {
357 graph.write("st" + state.id + ",\"" + state.id);
358 if (state.error != null) {
359 graph.write(":" + state.error);
361 graph.write("\","+state_node_style);
362 if (state.error != null) {
364 } else if (state.has_next) {
365 graph.write(",black");
367 graph.write(",green");
369 } else { // The dot version
370 graph.write(" st" + state.id + " [label=\"" + state.id);
371 if (state.error != null) {
372 graph.write(":" + state.error);
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");
380 graph.write("egg,color=green");
388 private static class StateInformation {
389 public StateInformation() {}
390 public void reset(int id, boolean has_next, boolean is_new) {
392 this.has_next = has_next;
394 this.is_new = is_new;
397 boolean has_next = true;
399 boolean is_new = false;
403 * Creates an GDF edge string.
405 private String makeGdfEdgeString(String from_id,
409 StringBuilder sb=new StringBuilder(from_id);
410 sb.append(',').append(to_id).append(',').append('\"');
411 if ((label!=null) && (!"".equals(label))) {
416 sb.append('\"').append(',').append(labelvisible).append(',').append(true).
417 append(',').append(thread);
418 replaceString(sb, "\n", "");
419 return sb.toString();
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.
428 private String convertGdfSpecial(String str) {
429 if ((str==null) || "".equals(str)) return "";
431 StringBuilder sb=new StringBuilder(str);
432 convertGdfSpecial(sb);
433 return sb.toString();
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.
441 private void convertGdfSpecial(StringBuilder sb) {
442 replaceString(sb, "\"", "\'\'");
443 replaceString(sb, "\n", " ");
447 * Create an edge in the graph file from old_id to new_id.
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();
455 // edgedef>node1,node2,label,labelvisible,directed,thread INT
457 // Old State -> Transition - labeled with the source info if any.
459 makeGdfEdgeString("st"+old_id, "tr"+my_id,
460 makeGdfLabel(state, my_id),
463 // Transition node: name,label,style,color
464 graph.write("tr" + my_id + ",\"" +my_id+"\","+transition_node_style);
467 // Transition -> New State - labeled with the last output if any.
469 String lastOutputLabel=
470 replaceString(convertGdfSpecial(trans.getOutput()), "\"", "\'\'");
472 makeGdfEdgeString("tr"+my_id, "st"+new_id, lastOutputLabel, thread));
474 graph.write(" st" + old_id + " -> tr" + my_id + ";");
476 graph.write(" tr" + my_id + " [label=\"" + makeDotLabel(state, my_id) +
479 graph.write(" tr" + my_id + " -> st" + new_id + ";");
484 * Show the usage message.
486 static void showUsage() {
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.");
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;
509 } else if ("-show-source".equals(arg)) {
512 } else if ("-gdf".equals(arg)) {
514 out_filename=OUT_FILENAME_NO_EXT+"."+GDF_EXT;
516 } else if ("-labelvisible".equals(arg)) {
519 } else if ("-help".equals(args[i])) {