[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools StateSpaceDot.java,1.5,1.6

[Masoud Mansouri-S. <mas...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20518/src/gov/nasa/jpf/tools

Modified Files:
	StateSpaceDot.java 
Log Message:
* Now last output is only added to the second portion of a transition.
   For 2 states s1 and s2 and a transition t1 between them (s1->t1->s2),
   the last output is only added to t1->s2 portion.

Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.5
retrieving revision 1.6
diff -u -d -r1.5 -r1.6
--- StateSpaceDot.java	27 Jun 2005 21:42:09 -0000	1.5
+++ StateSpaceDot.java	12 Aug 2005 22:12:51 -0000	1.6
@@ -196,7 +196,7 @@
   private void endGraph() throws IOException {
     addNode(prev_state);
     if (format==GDF_FORMAT) {
-      graph.write("edgedef>node1,node2,label,labelvisible,directed,thread INT,lastoutput VARCHAR(32)");
+      graph.write("edgedef>node1,node2,label,labelvisible,directed,thread INT");
       graph.newLine();
 
       // Output all the edges that we have accumulated so far
@@ -391,8 +391,7 @@
   private String makeGdfEdgeString(String from_id,
   		                           String to_id,
 								   String label,
-								   int thread,
-								   String lastOutput) {
+								   int thread) {
   	StringBuffer sb=new StringBuffer();
   	sb.append(from_id).append(',').append(to_id).append(',').
 	  append('\"');
@@ -403,10 +402,6 @@
   	}
   	sb.append('\"').append(',').append(labelvisible).append(',').append(true).
 	append(',').append(thread);
-  	lastOutput=replaceString(lastOutput, "\"", "\'\'");
-  	if ((lastOutput!=null) && (!"".equals(lastOutput))) {
-  		sb.append(',').append('\"').append(lastOutput).append('\"');
-  	}
   	replaceString(sb, "\n", "");
   	return sb.toString();
   }
@@ -443,24 +438,25 @@
     if (format==GDF_FORMAT) {
       Transition trans=state.getTransition();
       int thread = trans.getThread();
-      String lastoutput=convertGdfSpecial(trans.getOutput());
       
       // edgedef>node1,node2,label,labelvisible,directed,thread INT
 
-      // Old State -> Transition - labeled with the last output if any.
+      // Old State -> Transition - labeled with the source info if any.
       gdfEdges.add(
       		makeGdfEdgeString("st"+old_id, "tr"+my_id,
       				          makeGdfLabel(state, my_id),
-      				          thread, lastoutput));
+      				          thread));
 
       // Transition node: name,label,style,color
       graph.write("tr" + my_id + ",\"" +my_id+"\","+transition_node_style);
       
       graph.newLine();
-      // Transition -> New State - labeled with the source info if any.
+      // Transition -> New State - labeled with the last output if any.
+      
+      String lastOutputLabel=
+      	replaceString(convertGdfSpecial(trans.getOutput()), "\"", "\'\'");
       gdfEdges.add(
-      		makeGdfEdgeString("tr"+my_id, "st"+new_id, lastoutput, thread,
-      				           lastoutput));
+      	makeGdfEdgeString("tr"+my_id, "st"+new_id, lastOutputLabel, thread));
     } else { // DOT
       graph.write("  st" + old_id + " -> tr" + my_id + ";");
       graph.newLine();