Menu
▾
▴
[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools StateSpaceDot.java,1.2,1.3
|
From: Masoud Mansouri-S. <mas...@us...> - 2005-06-21 00:07:37
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6963/src/gov/nasa/jpf/tools Modified Files: StateSpaceDot.java Log Message: * Extended this to also support gdf format used by GUESS from HP - http://www.hpl.hp.com/research/idl/projects/graphs/. This tool can handle graphs of much larger size than GraphViz could handle. You can zoom in and out and interact with the graph using a Python like notation. E.g., coloring edges based on thread numbers, finding and making visible only the path between 2 specific states, etc. The graph is stored in a file called "jpf-state-space.<extension>" where is ".dot" or ".gdf". By default it generates a DOT graph as before. Options added: -gdf: Generate the graph in GDF format. The default is DOT. -labelvisible: Indicates if the label on the transitions is visible (used only with the -gdf option) Index: StateSpaceDot.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- StateSpaceDot.java 14 Jun 2005 19:43:08 -0000 1.2 +++ StateSpaceDot.java 21 Jun 2005 00:07:19 -0000 1.3 @@ -30,23 +30,50 @@ import java.io.FileWriter; import java.io.IOException; import java.util.Iterator; - +import java.util.ArrayList; /* - * Add an state space observer to JPF and build a DOT graph of the state space - * that is explored by JPF. The graph is stored in "./jpf-state-space.dot". - * + * Add a state space observer to JPF and build a graph of the state space + * that is explored by JPF. The graph can be generated in different formats. + * The current formats that are supported are DOT (visualized by a tool + * like GraphViz from ATT - http://www.graphviz.org/) and gdf (used by GUESS + * from HP - http://www.hpl.hp.com/research/idl/projects/graphs/). + * The graph is stored in a file called "jpf-state-space.<extension>" where + * extension is ".dot" or ".gdf". By default it generates a DOT graph. + * + * 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) * @date 9/12/03 - * - * @author Owen O'Malley + * @author Owen O'Malley (Initial version generating the DOT graph) + * + * @date 7/17/05 + * @author Masoud Mansouri-Samani (Extended to also generate the gdf graph) */ - public class StateSpaceDot implements SearchListener { - private static final String GRAPH_FILENAME = "jpf-state-space.dot"; + private static final String DOT_EXT = "dot"; + private static final String GDF_EXT = "gdf"; + private static final String OUT_FILENAME_NO_EXT = "jpf-state-space"; + private BufferedWriter graph = null; private int edge_id = 0; private static boolean transition_numbers=false; private static boolean show_source=false; + private static int DOT_FORMAT=0; + private static int GDF_FORMAT=1; + private int format=DOT_FORMAT; + private String out_filename = OUT_FILENAME_NO_EXT+"."+DOT_EXT; + private boolean labelvisible=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 come across them but we store + * the strings for edges in the gdfEdges list and output them when the + * search ends. + */ + ArrayList gdfEdges=new ArrayList(); private StateInformation prev_state = null; @@ -69,9 +96,11 @@ boolean has_next =search.hasNextState(); boolean is_new = search.isNewState(); try { - graph.write("/* searchAdvanced(" + id + ", " + makeLabel(search, id) + + if (format==DOT_FORMAT) { + graph.write("/* searchAdvanced(" + id + ", " + makeDotLabel(search, id) + ", " + has_next + ") */"); - graph.newLine(); + graph.newLine(); + } if (prev_state != null) { addEdge(prev_state.id, id, search); } else { @@ -83,26 +112,30 @@ } public void stateRestored (Search search) { - // N/A + // N/A } - + public void stateProcessed (Search search) { - // nothing to do + // nothing to do } - + public void stateBacktracked(Search search) { try { addNode(prev_state); prev_state.reset(search.getStateNumber(), false, false); - graph.write("/* searchBacktracked(" + prev_state + ") */"); - graph.newLine(); + if (format==DOT_FORMAT) { + graph.write("/* searchBacktracked(" + prev_state + ") */"); + graph.newLine(); + } } catch (IOException e) {} } public void searchConstraintHit(Search search) { try { - graph.write("/* searchConstraintHit(" + search.getStateNumber() + ") */"); - graph.newLine(); + if (format==DOT_FORMAT) { + graph.write("/* searchConstraintHit(" + search.getStateNumber() + ") */"); + graph.newLine(); + } } catch (IOException e) {} } @@ -116,20 +149,26 @@ } public void propertyViolated(Search search) { - try { - prev_state.error = getErrorMsg(search); - graph.write("/* propertyViolated(" + search.getStateNumber() + ") */"); - graph.newLine(); - } catch (IOException e) {} + try { + prev_state.error = getErrorMsg(search); + if (format==DOT_FORMAT) { + graph.write("/* propertyViolated(" + search.getStateNumber() + ") */"); + graph.newLine(); + } + } catch (IOException e) {} } /** * Put the header for the graph into the file. */ private void beginGraph() throws IOException { - graph = new BufferedWriter(new FileWriter(GRAPH_FILENAME)); - graph.write("digraph jpf_state_space {"); - graph.newLine(); + graph = new BufferedWriter(new FileWriter(out_filename)); + if (format==GDF_FORMAT) { + graph.write("nodedef>name,label,style,color"); + } else { // dot + graph.write("digraph jpf_state_space {"); + } + graph.newLine(); } /** @@ -137,15 +176,25 @@ */ private void endGraph() throws IOException { addNode(prev_state); - graph.write("}"); + if (format==GDF_FORMAT) { + graph.write("edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)"); + } else { + graph.write("}"); + } graph.newLine(); + // Output all the edges that we have accumulated so far + int size=gdfEdges.size(); + for (int i=0; i<size; i++) { + graph.write((String) gdfEdges.get(i)); + graph.newLine(); + } graph.close(); } /** * Return the string that will be used to label this state for the user. */ - private String makeLabel(Search state, int my_id) { + private String makeDotLabel(Search state, int my_id) { Transition trans = state.getTransition(); if (trans == null) { return "-init-"; @@ -174,21 +223,21 @@ result.append("\\n"); StringBuffer sb=new StringBuffer(source_line); - + // 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, ""); + sb.replace(indexOfNewLine, indexOfNewLine+2, ""); } - + int indexOfBracket=0, lastIndex=0; while (indexOfBracket!=-1) { indexOfBracket=sb.indexOf("]", lastIndex); @@ -197,7 +246,7 @@ lastIndex=indexOfBracket+2; } } - + int indexOfQuote=0, lastIndexOfQueote=0; while (indexOfQuote!=-1) { indexOfQuote=sb.indexOf("\"",lastIndexOfQueote); @@ -206,7 +255,6 @@ lastIndexOfQueote=indexOfQuote+2; } } - result.append(sb.toString()); } } @@ -215,23 +263,81 @@ } /** + * Return the string that will be used to label this state in the GDF graph. + */ + private String makeGdfLabel(Search state, int my_id) { + Transition trans = state.getTransition(); + if (trans == null) { + return "-init-"; + } + + StringBuffer result = new StringBuffer(); + + if (transition_numbers) { + result.append(my_id); + result.append(":"); + } + + TransitionStep last_trans_step = trans.getLastTransitionStep(); + result.append(last_trans_step.getSourceRef().toString()); + + if (show_source) { + 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 + // 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()); + } + } + return result.toString(); + } + + /** * Add a new node to the graph with the relevant properties. */ private void addNode(StateInformation state) throws IOException { if (state.is_new) { - graph.write(" st" + state.id + " [label=\"" + state.id); - if (state.error != null) { - graph.write(":" + state.error); - } - graph.write("\",shape="); - if (state.error != null) { - graph.write("diamond,color=red"); - } else if (state.has_next) { - graph.write("circle,color=black"); - } else { - graph.write("egg,color=green"); + if (format==GDF_FORMAT) { + graph.write("st" + state.id + ",\"" + state.id); + if (state.error != null) { + graph.write(":" + state.error); + } + graph.write("\",5"); + if (state.error != null) { + graph.write(",red"); + } else if (state.has_next) { + graph.write(",black"); + } else { + graph.write(",green"); + } + } else { // The dot version + graph.write(" st" + state.id + " [label=\"" + state.id); + if (state.error != null) { + graph.write(":" + state.error); + } + graph.write("\",shape="); + if (state.error != null) { + graph.write("diamond,color=red"); + } else if (state.has_next) { + graph.write("circle,color=black"); + } else { + graph.write("egg,color=green"); + } + graph.write("];"); } - graph.write("];"); graph.newLine(); } } @@ -255,14 +361,20 @@ */ private void addEdge(int old_id, int new_id, Search state) throws IOException { int my_id = edge_id++; - graph.write(" st" + old_id + " -> tr" + my_id + ";"); - graph.newLine(); - graph.write(" tr" + my_id + - " [label=\"" + makeLabel(state, my_id) + + if (format==GDF_FORMAT) { + int thread = state.getTransition().getThread(); + // edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32) + gdfEdges.add("st" + old_id + ",st" + new_id+ + ",\"" + makeGdfLabel(state, my_id)+"\","+ + labelvisible+",true,"+thread); + } else { // DOT + graph.write(" st" + old_id + " -> tr" + my_id + ";"); + graph.newLine(); + graph.write(" tr" + my_id + " [label=\"" + makeDotLabel(state, my_id) + "\",shape=box]"); - graph.newLine(); - graph.write(" tr" + my_id + " -> st" + new_id + ";"); - graph.newLine(); + graph.newLine(); + graph.write(" tr" + my_id + " -> st" + new_id + ";"); + } } void filterArgs (String[] args) { @@ -274,23 +386,27 @@ } else if ("-show-source".equals(arg)) { show_source = true; args[i] = null; + } else if ("-gdf".equals(arg)) { + format=GDF_FORMAT; + out_filename=OUT_FILENAME_NO_EXT+"."+GDF_EXT; + args[i] = null; + } else if ("-labelvisible".equals(arg)) { + labelvisible=true; + args[i] = null; } } } - + public static void main(String [] args) { StateSpaceDot listener = new StateSpaceDot(); listener.filterArgs(args); - + Config conf = JPF.createConfig(args); // do own settings here - + JPF jpf = new JPF(conf); jpf.addSearchListener(listener); jpf.run(); } } - - - |
