001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019:
020: package gov.nasa.jpf.tools;
021:
022: import gov.nasa.jpf.ErrorList;
023: import gov.nasa.jpf.JPF;
024: import gov.nasa.jpf.Config;
025: import gov.nasa.jpf.Search;
026: import gov.nasa.jpf.SearchListener;
027: import gov.nasa.jpf.Transition;
028: import gov.nasa.jpf.TransitionStep;
029: import java.io.BufferedWriter;
030: import java.io.FileWriter;
031: import java.io.IOException;
032: import java.util.Iterator;
033: import java.util.ArrayList;
034:
035: /*
036: * Add a state space observer to JPF and build a graph of the state space
037: * that is explored by JPF. The graph can be generated in different formats.
038: * The current formats that are supported are DOT (visualized by a tool
039: * like GraphViz from ATT - http://www.graphviz.org/) and gdf (used by GUESS
040: * from HP - http://www.hpl.hp.com/research/idl/projects/graphs/).
041: * The graph is stored in a file called "jpf-state-space.<extension>" where
042: * extension is ".dot" or ".gdf". By default it generates a DOT graph.
043: *
044: * Options:
045: * -gdf: Generate the graph in GDF format. The default is DOT.
046: * -transition-numbers: Include transition numbers in transition labels.
047: * -show-source: Include source lines in transition labels.
048: * -labelvisible: Indicates if the label on the transitions is visible (used only with the -gdf option)
049: * -help: Prints this help information and stops.
050: *
051: * @date 9/12/03
052: * @author Owen O'Malley (Initial version generating the DOT graph)
053: *
054: * @date 7/17/05
055: * @author Masoud Mansouri-Samani (Extended to also generate the gdf graph)
056: */
057: public class StateSpaceDot implements SearchListener {
058: private static final String DOT_EXT = "dot";
059: private static final String GDF_EXT = "gdf";
060: private static final String OUT_FILENAME_NO_EXT = "jpf-state-space";
061:
062: // NODE styles constants
063: private static final int RECTABGLE = 1;
064: private static final int ELLIPSE = 2;
065: private static final int ROUND_RECTABGLE = 3;
066: private static final int RECTABGLE_WITH_TEXT = 4;
067: private static final int ELLIPSE_WITH_TEXT = 5;
068: private static final int ROUND_RECTABGLE_WITH_TEXT = 6;
069:
070: // State and transition node styles used
071: private static final int state_node_style = ELLIPSE_WITH_TEXT;
072: private static final int transition_node_style = RECTABGLE_WITH_TEXT;
073:
074: // File formats supported
075: private static final int DOT_FORMAT = 0;
076: private static final int GDF_FORMAT = 1;
077:
078: private BufferedWriter graph = null;
079: private int edge_id = 0;
080: private static boolean transition_numbers = false;
081: private static boolean show_source = false;
082: private static int format = DOT_FORMAT;
083: private String out_filename = OUT_FILENAME_NO_EXT + "." + DOT_EXT;
084: private static boolean labelvisible = false;
085: private static boolean helpRequested = false;
086:
087: /* In gdf format all the edges must come after all the nodes of the graph
088: * are generated. So we first output the nodes as we come across them but
089: * we store the strings for edges in the gdfEdges list and output them when
090: * the search ends.
091: */
092: ArrayList gdfEdges = new ArrayList();
093:
094: private StateInformation prev_state = null;
095:
096: public StateSpaceDot() {
097: }
098:
099: public void searchStarted(Search search) {
100: try {
101: beginGraph();
102: } catch (IOException e) {
103: }
104: }
105:
106: public void searchFinished(Search search) {
107: try {
108: endGraph();
109: } catch (IOException e) {
110: }
111: }
112:
113: public void stateAdvanced(Search search) {
114: int id = search.getStateNumber();
115: boolean has_next = search.hasNextState();
116: boolean is_new = search.isNewState();
117: try {
118: if (format == DOT_FORMAT) {
119: graph.write("/* searchAdvanced(" + id + ", "
120: + makeDotLabel(search, id) + ", " + has_next
121: + ") */");
122: graph.newLine();
123: }
124: if (prev_state != null) {
125: addEdge(prev_state.id, id, search);
126: } else {
127: prev_state = new StateInformation();
128: }
129: addNode(prev_state);
130: prev_state.reset(id, has_next, is_new);
131: } catch (IOException e) {
132: }
133: }
134:
135: public void stateRestored(Search search) {
136: prev_state.reset(search.getStateNumber(), false, false);
137: }
138:
139: public void stateProcessed(Search search) {
140: // nothing to do
141: }
142:
143: public void stateBacktracked(Search search) {
144: try {
145: addNode(prev_state);
146: prev_state.reset(search.getStateNumber(), false, false);
147: if (format == DOT_FORMAT) {
148: graph.write("/* searchBacktracked(" + prev_state
149: + ") */");
150: graph.newLine();
151: }
152: } catch (IOException e) {
153: }
154: }
155:
156: public void searchConstraintHit(Search search) {
157: try {
158: if (format == DOT_FORMAT) {
159: graph.write("/* searchConstraintHit("
160: + search.getStateNumber() + ") */");
161: graph.newLine();
162: }
163: } catch (IOException e) {
164: }
165: }
166:
167: private String getErrorMsg(Search search) {
168: ErrorList errs = search.getErrors();
169: Iterator itr = errs.iterator();
170: while (itr.hasNext()) {
171: return ((gov.nasa.jpf.Error) itr.next()).getMessage();
172: }
173: return null;
174: }
175:
176: public void propertyViolated(Search search) {
177: try {
178: prev_state.error = getErrorMsg(search);
179: if (format == DOT_FORMAT) {
180: graph.write("/* propertyViolated("
181: + search.getStateNumber() + ") */");
182: graph.newLine();
183: }
184: } catch (IOException e) {
185: }
186: }
187:
188: /**
189: * Put the header for the graph into the file.
190: */
191: private void beginGraph() throws IOException {
192: graph = new BufferedWriter(new FileWriter(out_filename));
193: if (format == GDF_FORMAT) {
194: graph.write("nodedef>name,label,style,color");
195: } else { // dot
196: graph.write("digraph jpf_state_space {");
197: }
198: graph.newLine();
199: }
200:
201: /**
202: * In the case of the DOT graph it is just adding the final "}" at the end.
203: * In the case of GPF format we must output edge definition and all the
204: * edges that we have found.
205: */
206: private void endGraph() throws IOException {
207: addNode(prev_state);
208: if (format == GDF_FORMAT) {
209: graph
210: .write("edgedef>node1,node2,label,labelvisible,directed,thread INT");
211: graph.newLine();
212:
213: // Output all the edges that we have accumulated so far
214: int size = gdfEdges.size();
215: for (int i = 0; i < size; i++) {
216: graph.write((String) gdfEdges.get(i));
217: graph.newLine();
218: }
219: } else {
220: graph.write("}");
221: graph.newLine();
222: }
223: graph.close();
224: }
225:
226: /**
227: * Return the string that will be used to label this state for the user.
228: */
229: private String makeDotLabel(Search state, int my_id) {
230: Transition trans = state.getTransition();
231: if (trans == null) {
232: return "-init-";
233: }
234:
235: StringBuffer result = new StringBuffer();
236:
237: if (transition_numbers) {
238: result.append(my_id);
239: result.append("\\n");
240: }
241:
242: TransitionStep last_trans_step = trans.getLastTransitionStep();
243:
244: int thread = trans.getThread();
245:
246: result.append("Thd");
247: result.append(thread);
248: result.append(":");
249:
250: result.append(last_trans_step.getSourceRef().toString());
251:
252: if (show_source) {
253: String source_line = last_trans_step.getSourceRef()
254: .getLineString();
255: if ((source_line != null) && !source_line.equals("")) {
256: result.append("\\n");
257:
258: StringBuffer sb = new StringBuffer(source_line);
259:
260: // We need to precede the dot-specific special characters which appear
261: // in the Java source line, such as ']' and '"', with the '\' escape
262: // characters and also to remove any new lines.
263:
264: replaceString(sb, "\n", "");
265: replaceString(sb, "]", "\\]");
266: replaceString(sb, "\"", "\\\"");
267: result.append(sb.toString());
268: }
269: }
270:
271: return result.toString();
272: }
273:
274: /**
275: * Return the string that will be used to label this state in the GDF graph.
276: */
277: private String makeGdfLabel(Search state, int my_id) {
278: Transition trans = state.getTransition();
279: if (trans == null) {
280: return "-init-";
281: }
282:
283: StringBuffer result = new StringBuffer();
284:
285: if (transition_numbers) {
286: result.append(my_id);
287: result.append(":");
288: }
289:
290: TransitionStep last_trans_step = trans.getLastTransitionStep();
291: result.append(last_trans_step.getSourceRef().toString());
292:
293: if (show_source) {
294: String source_line = last_trans_step.getSourceRef()
295: .getLineString();
296: if ((source_line != null) && !source_line.equals("")) {
297:
298: // We need to deal with gdf-specific special characters which couls appear
299: // in the Java source line, such as '"'.
300: result.append(source_line);
301: convertGdfSpecial(result);
302: }
303: }
304: return result.toString();
305: }
306:
307: /**
308: * Locates and replaces all occurrences of a given string with another given
309: * string in an original string buffer. There seems to be a bug in Java
310: * String's replaceAll() method which does not allow us to use it to replace
311: * some special chars so here we use StringBuffer's replace method to do
312: * this.
313: * @param original The original string buffer.
314: * @param from The replaced string.
315: * @param to The replacing string.
316: * @return The original string buffer with the sub-string replaced
317: * throughout.
318: */
319: private StringBuffer replaceString(StringBuffer original,
320: String from, String to) {
321: int indexOfReplaced = 0, lastIndexOfReplaced = 0;
322: while (indexOfReplaced != -1) {
323: indexOfReplaced = original.indexOf(from,
324: lastIndexOfReplaced);
325: if (indexOfReplaced != -1) {
326: original.replace(indexOfReplaced, indexOfReplaced + 1,
327: 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 StringBuffer(original), from, to)
346: .toString();
347: } else {
348: return original;
349: }
350: }
351:
352: /**
353: * Add a new node to the graph with the relevant properties.
354: */
355: private void addNode(StateInformation state) throws IOException {
356: if (state.is_new) {
357: if (format == GDF_FORMAT) {
358: graph.write("st" + state.id + ",\"" + state.id);
359: if (state.error != null) {
360: graph.write(":" + state.error);
361: }
362: graph.write("\"," + state_node_style);
363: if (state.error != null) {
364: graph.write(",red");
365: } else if (state.has_next) {
366: graph.write(",black");
367: } else {
368: graph.write(",green");
369: }
370: } else { // The dot version
371: graph
372: .write(" st" + state.id + " [label=\""
373: + state.id);
374: if (state.error != null) {
375: graph.write(":" + state.error);
376: }
377: graph.write("\",shape=");
378: if (state.error != null) {
379: graph.write("diamond,color=red");
380: } else if (state.has_next) {
381: graph.write("circle,color=black");
382: } else {
383: graph.write("egg,color=green");
384: }
385: graph.write("];");
386: }
387: graph.newLine();
388: }
389: }
390:
391: private static class StateInformation {
392: public StateInformation() {
393: }
394:
395: public void reset(int id, boolean has_next, boolean is_new) {
396: this .id = id;
397: this .has_next = has_next;
398: this .error = null;
399: this .is_new = is_new;
400: }
401:
402: int id = -1;
403: boolean has_next = true;
404: String error = null;
405: boolean is_new = false;
406: }
407:
408: /**
409: * Creates an GDF edge string.
410: */
411: private String makeGdfEdgeString(String from_id, String to_id,
412: String label, int thread) {
413: StringBuffer sb = new StringBuffer();
414: sb.append(from_id).append(',').append(to_id).append(',')
415: .append('\"');
416: if ((label != null) && (!"".equals(label))) {
417: sb.append(label);
418: } else {
419: sb.append('-');
420: }
421: sb.append('\"').append(',').append(labelvisible).append(',')
422: .append(true).append(',').append(thread);
423: replaceString(sb, "\n", "");
424: return sb.toString();
425: }
426:
427: /**
428: * GUESS cannot deal with '\n' chars, so remove them. Also convert all '"'
429: * characters to "''".
430: * @param str The string to perform the conversion on.
431: * @return The converted string.
432: */
433: private String convertGdfSpecial(String str) {
434: if ((str == null) || "".equals(str))
435: return "";
436:
437: StringBuffer sb = new StringBuffer(str);
438: convertGdfSpecial(sb);
439: return sb.toString();
440: }
441:
442: /**
443: * GUESS cannot deal with '\n' chars, so replace them with a space. Also
444: * convert all '"' characters to "''".
445: * @param sb The string buffer to perform the conversion on.
446: */
447: private void convertGdfSpecial(StringBuffer sb) {
448: replaceString(sb, "\"", "\'\'");
449: replaceString(sb, "\n", " ");
450: }
451:
452: /**
453: * Create an edge in the graph file from old_id to new_id.
454: */
455: private void addEdge(int old_id, int new_id, Search state)
456: throws IOException {
457: int my_id = edge_id++;
458: if (format == GDF_FORMAT) {
459: Transition trans = state.getTransition();
460: int thread = trans.getThread();
461:
462: // edgedef>node1,node2,label,labelvisible,directed,thread INT
463:
464: // Old State -> Transition - labeled with the source info if any.
465: gdfEdges.add(makeGdfEdgeString("st" + old_id, "tr" + my_id,
466: makeGdfLabel(state, my_id), thread));
467:
468: // Transition node: name,label,style,color
469: graph.write("tr" + my_id + ",\"" + my_id + "\","
470: + transition_node_style);
471:
472: graph.newLine();
473: // Transition -> New State - labeled with the last output if any.
474:
475: String lastOutputLabel = replaceString(
476: convertGdfSpecial(trans.getOutput()), "\"", "\'\'");
477: gdfEdges.add(makeGdfEdgeString("tr" + my_id, "st" + new_id,
478: lastOutputLabel, thread));
479: } else { // DOT
480: graph.write(" st" + old_id + " -> tr" + my_id + ";");
481: graph.newLine();
482: graph.write(" tr" + my_id + " [label=\""
483: + makeDotLabel(state, my_id) + "\",shape=box]");
484: graph.newLine();
485: graph.write(" tr" + my_id + " -> st" + new_id + ";");
486: }
487: }
488:
489: /**
490: * Show the usage message.
491: */
492: static void showUsage() {
493: System.out
494: .println("Usage: \"java [<vm-options>] gov.nasa.jpf.tools.StateSpaceDot [<graph-options>] [<jpf-options-and-args>]");
495: System.out.println(" <graph-options> : ");
496: System.out
497: .println(" -gdf: Generate the graph in GDF format. The default is DOT.");
498: System.out
499: .println(" -transition-numbers: Include transition numbers in transition labels.");
500: System.out
501: .println(" -show-source: Include source lines in transition labels.");
502: System.out
503: .println(" -labelvisible: Indicates if the label on the transitions is visible (used only with the -gdf option)");
504: System.out
505: .println(" -help: Prints this help information and stops.");
506: System.out.println(" <jpf-options-and-args>:");
507: System.out
508: .println(" Options and command line arguments passed directly to JPF.");
509: System.out
510: .println(" Note: With -gdf option transition edges could also include program output ");
511: System.out
512: .println(" but in order to enable this JPF's vm.path_output option must be set to ");
513: System.out.println(" true.");
514: }
515:
516: void filterArgs(String[] args) {
517: for (int i = 0; i < args.length; i++) {
518: String arg = args[i];
519: if ("-transition-numbers".equals(arg)) {
520: transition_numbers = true;
521: args[i] = null;
522: } else if ("-show-source".equals(arg)) {
523: show_source = true;
524: args[i] = null;
525: } else if ("-gdf".equals(arg)) {
526: format = GDF_FORMAT;
527: out_filename = OUT_FILENAME_NO_EXT + "." + GDF_EXT;
528: args[i] = null;
529: } else if ("-labelvisible".equals(arg)) {
530: labelvisible = true;
531: args[i] = null;
532: } else if ("-help".equals(args[i])) {
533: showUsage();
534: helpRequested = true;
535: }
536: }
537: }
538:
539: public static void main(String[] args) {
540: StateSpaceDot listener = new StateSpaceDot();
541:
542: System.out.println("JPF State Space dot Graph Generator");
543: listener.filterArgs(args);
544:
545: System.out.println("...graph output to "
546: + listener.out_filename + "...");
547:
548: if (helpRequested == true) {
549: return;
550: }
551:
552: Config conf = JPF.createConfig(args);
553: // do own settings here
554:
555: JPF jpf = new JPF(conf);
556: jpf.addSearchListener(listener);
557:
558: System.out.println("...running JPF...");
559: jpf.run();
560: }
561: }
|