Mercurial > hg > Members > kono > jpf-core

annotate src/main/gov/nasa/jpf/listener/SimpleDot.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
1 /*
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
2 * Copyright (C) 2014, United States Government, as represented by the
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
3 * Administrator of the National Aeronautics and Space Administration.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
4 * All rights reserved.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
5 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
8 * in compliance with the License. You may obtain a copy of the License at
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
9 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
10 * http://www.apache.org/licenses/LICENSE-2.0.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
11 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
12 * Unless required by applicable law or agreed to in writing, software
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
13 * distributed under the License is distributed on an "AS IS" BASIS,
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
15 * See the License for the specific language governing permissions and
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
16 * limitations under the License.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
17 */
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
18
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
19 package gov.nasa.jpf.listener;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
20
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
21 import gov.nasa.jpf.Config;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
22 import gov.nasa.jpf.Error;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
23 import gov.nasa.jpf.JPF;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
24 import gov.nasa.jpf.JPFConfigException;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
25 import gov.nasa.jpf.ListenerAdapter;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
26 import gov.nasa.jpf.Property;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
27 import gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
28 import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
29 import gov.nasa.jpf.jvm.bytecode.INVOKESTATIC;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
30 import gov.nasa.jpf.jvm.bytecode.JVMInstanceFieldInstruction;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
31 import gov.nasa.jpf.jvm.bytecode.InstanceInvocation;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
32 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
33 import gov.nasa.jpf.jvm.bytecode.LockInstruction;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
34 import gov.nasa.jpf.jvm.bytecode.PUTFIELD;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
35 import gov.nasa.jpf.jvm.bytecode.PUTSTATIC;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
36 import gov.nasa.jpf.jvm.bytecode.JVMStaticFieldInstruction;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
37 import gov.nasa.jpf.report.ConsolePublisher;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
38 import gov.nasa.jpf.report.Publisher;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
39 import gov.nasa.jpf.search.Search;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
40 import gov.nasa.jpf.util.FileUtils;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
41 import gov.nasa.jpf.util.Misc;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
42 import gov.nasa.jpf.vm.ChoiceGenerator;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
43 import gov.nasa.jpf.vm.ElementInfo;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
44 import gov.nasa.jpf.vm.ExceptionInfo;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
45 import gov.nasa.jpf.vm.Instruction;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
46 import gov.nasa.jpf.vm.VM;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
47 import gov.nasa.jpf.vm.MethodInfo;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
48 import gov.nasa.jpf.vm.NoUncaughtExceptionsProperty;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
49 import gov.nasa.jpf.vm.NotDeadlockedProperty;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
50 import gov.nasa.jpf.vm.ThreadInfo;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
51
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
52 import java.io.File;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
53 import java.io.FileWriter;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
54 import java.io.IOException;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
55 import java.io.PrintWriter;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
56 import java.util.HashSet;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
57
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
58 /**
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
59 * an alternative Graphviz dot-file generator for simple,educational state graphs
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
60 * except of creating funny wallpapers, it doesn't help much in real life if the
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
61 * state count gets > 50, but for the small ones it's actually quite readable.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
62 * Good for papers.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
63 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
64 * normal states are labeled with their numeric ids, end states are double circled.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
65 * start, end and error states are color filled
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
66 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
67 * edges have two labels: the choice value at the beginning and the CG cause
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
68 * at the end. Only the first incoming edge into a state shows the CG cause
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
69 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
70 * we only render one backtrack edge per from-state
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
71 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
72 * <2do> GraphViz doesn't seem to handle color or fontname for head/tail labels correctly
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
73 */
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
74 public class SimpleDot extends ListenerAdapter {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
75
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
76 static final String GRAPH_ATTRS = "pad=0.5";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
77 static final String GENERIC_NODE_ATTRS = "shape=circle,style=filled,fillcolor=white";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
78 static final String GENERIC_EDGE_ATTRS = "fontsize=10,fontname=Helvetica,fontcolor=blue,color=cadetblue,style=\"setlinewidth(0.5)\",arrowhead=empty,arrowsize=0.5";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
79 static final String START_NODE_ATTRS = "fillcolor=green";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
80 static final String END_NODE_ATTRS = "shape=doublecircle,fillcolor=cyan";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
81 static final String ERROR_NODE_ATTRS = "color=red,fillcolor=lightcoral";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
82 static final String BACKTRACK_EDGE_ATTRS = "arrowhead=onormal,color=gray52,style=\"dotted\"";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
83 static final String RESTORED_EDGE_ATTRS = "arrowhead=onormal,color=red,style=\"dotted\"";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
84 static final String NEW_EDGE_ATTRS = "arrowhead=normal";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
85 static final String VISITED_EDGE_ATTRS = "arrowhead=vee";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
86
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
87
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
88 //--- configurable Graphviz attributes
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
89 protected String graphAttrs;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
90 protected String genericNodeAttrs;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
91 protected String genericEdgeAttrs;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
92 protected String startNodeAttrs;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
93 protected String endNodeAttrs;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
94 protected String errorNodeAttrs;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
95 protected String newEdgeAttrs;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
96 protected String visitedEdgeAttrs;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
97 protected String backtrackEdgeAttrs;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
98 protected String restoreEdgeAttrs;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
99
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
100 protected boolean showTarget;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
101 protected boolean printFile;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
102
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
103 protected VM vm;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
104 protected String app;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
105 protected File file;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
106 protected PrintWriter pw;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
107
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
108 protected int lastId = -1; // where we come from
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
109 protected String lastErrorId;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
110 protected ElementInfo lastEi;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
111 protected ThreadInfo lastTi; // the last started thread
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
112
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
113 // helper because GraphViz cannot eliminate duplicate edges
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
114 HashSet<Long> seenEdges;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
115
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
116 public SimpleDot( Config config, JPF jpf){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
117
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
118 graphAttrs = config.getString("dot.graph_attr", GRAPH_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
119 genericNodeAttrs = config.getString("dot.node_attr", GENERIC_NODE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
120 genericEdgeAttrs = config.getString("dot.edge_attr", GENERIC_EDGE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
121 newEdgeAttrs = config.getString("dot.new_edge_attr", NEW_EDGE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
122 visitedEdgeAttrs = config.getString("dot.visited_edge_attr", VISITED_EDGE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
123 startNodeAttrs = config.getString("dot.start_node_attr", START_NODE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
124 endNodeAttrs = config.getString("dot.end_node_attr", END_NODE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
125 errorNodeAttrs = config.getString("dot.error_node_attr", ERROR_NODE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
126 backtrackEdgeAttrs = config.getString("dot.bt_edge_attr", BACKTRACK_EDGE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
127 restoreEdgeAttrs = config.getString("dot.restore_edge_attr", RESTORED_EDGE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
128
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
129 printFile = config.getBoolean("dot.print_file", false);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
130 showTarget = config.getBoolean("dot.show_target", false);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
131
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
132 // app and filename are not known until the search is started
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
133
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
134 jpf.addPublisherExtension(ConsolePublisher.class, this);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
135 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
136
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
137 void initialize (VM vm){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
138 Config config = vm.getConfig();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
139
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
140 app = vm.getSUTName();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
141 app = app.replace("+", "__");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
142 app = app.replace('.', '_');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
143
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
144 String fname = config.getString("dot.file");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
145 if (fname == null){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
146 fname = app + ".dot";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
147 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
148
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
149 try {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
150 file = new File(fname);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
151 FileWriter fw = new FileWriter(file);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
152 pw = new PrintWriter(fw);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
153 } catch (IOException iox){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
154 throw new JPFConfigException("unable to open SimpleDot output file: " + fname);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
155 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
156
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
157 seenEdges = new HashSet<Long>();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
158 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
159
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
160 //--- the listener interface
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
161
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
162 @Override
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
163 public void searchStarted(Search search){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
164 vm = search.getVM();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
165
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
166 initialize(vm);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
167
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
168 printHeader();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
169 printStartState("S");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
170 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
171
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
172 @Override
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
173 public void stateAdvanced(Search search){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
174 int id = search.getStateId();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
175 long edgeId = ((long)lastId << 32) | id;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
176
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
177 if (id <0 || seenEdges.contains(edgeId)){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
178 return; // skip the root state and property violations (reported separately)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
179 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
180
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
181
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
182 if (search.isErrorState()) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
183 String eid = "e" + search.getNumberOfErrors();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
184 printTransition(getStateId(lastId), eid, getLastChoice(), getError(search));
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
185 printErrorState(eid);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
186 lastErrorId = eid;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
187
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
188 } else if (search.isNewState()) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
189
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
190 if (search.isEndState()) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
191 printTransition(getStateId(lastId), getStateId(id), getLastChoice(), "return");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
192 printEndState(getStateId(id));
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
193 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
194 printTransition(getStateId(lastId), getStateId(id), getLastChoice(), getNextCG());
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
195 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
196
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
197 } else { // already visited state
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
198 printTransition(getStateId(lastId), getStateId(id), getLastChoice(), null);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
199 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
200
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
201 seenEdges.add(edgeId);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
202 lastId = id;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
203 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
204
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
205 @Override
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
206 public void stateBacktracked(Search search){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
207 int id = search.getStateId();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
208 long edgeId = ((long)lastId << 32) | id;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
209
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
210 if (!seenEdges.contains(edgeId)) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
211 if(lastErrorId!=null) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
212 printBacktrack(lastErrorId, getStateId(id));
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
213 lastErrorId = null;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
214 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
215 printBacktrack(getStateId(lastId), getStateId(id));
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
216 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
217 seenEdges.add(edgeId);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
218 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
219 lastId = id;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
220 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
221
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
222 @Override
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
223 public void stateRestored(Search search) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
224 int id = search.getStateId();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
225 long edgeId = ((long)lastId << 32) | id;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
226
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
227 if (!seenEdges.contains(edgeId)) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
228 printRestored(getStateId(lastId), getStateId(id));
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
229 seenEdges.add(edgeId);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
230 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
231 lastId = id;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
232 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
233
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
234 @Override
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
235 public void searchFinished (Search search){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
236 pw.println("}");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
237 pw.close();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
238 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
239
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
240 @Override
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
241 public void threadStarted (VM vm, ThreadInfo ti){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
242 lastTi = ti;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
243 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
244
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
245 @Override
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
246 public void objectWait (VM vm, ThreadInfo ti, ElementInfo ei){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
247 lastEi = ei;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
248 lastTi = ti;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
249 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
250
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
251 @Override
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
252 public void publishFinished (Publisher publisher) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
253 PrintWriter ppw = publisher.getOut();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
254 publisher.publishTopicStart("SimpleDot");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
255
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
256 ppw.println("dot file generated: " + file.getPath());
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
257
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
258 if (printFile){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
259 ppw.println();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
260 FileUtils.printFile(ppw,file);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
261 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
262 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
263
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
264
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
265 //--- data collection
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
266
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
267 protected String getStateId (int id){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
268 return id < 0 ? "S" : Integer.toString(id);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
269 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
270
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
271 protected String getLastChoice() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
272 ChoiceGenerator<?> cg = vm.getChoiceGenerator();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
273 Object choice = cg.getNextChoice();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
274
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
275 if (choice instanceof ThreadInfo){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
276 int idx = ((ThreadInfo)choice).getId();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
277 return "T"+idx;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
278 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
279 return choice.toString(); // we probably want more here
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
280 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
281 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
282
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
283 // this is the only method that's more tricky - we have to find a balance
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
284 // between being conscious enough to not clutter the graph, and expressive
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
285 // enough to understand it.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
286 // <2do> this doesn't deal well with custom or data CGs yet
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
287 protected String getNextCG(){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
288 ChoiceGenerator<?> cg = vm.getNextChoiceGenerator(); // that's the next one
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
289 Instruction insn = cg.getInsn();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
290
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
291 if (insn instanceof EXECUTENATIVE) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
292 return getNativeExecCG((EXECUTENATIVE)insn);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
293
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
294 } else if (insn instanceof JVMFieldInstruction) { // shared object field access
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
295 return getFieldAccessCG((JVMFieldInstruction)insn);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
296
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
297 } else if (insn instanceof LockInstruction){ // monitor_enter
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
298 return getLockCG((LockInstruction)insn);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
299
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
300 } else if (insn instanceof JVMInvokeInstruction){ // sync method invoke
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
301 return getInvokeCG((JVMInvokeInstruction)insn);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
302 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
303
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
304 return insn.getMnemonic(); // our generic fallback
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
305 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
306
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
307 protected String getNativeExecCG (EXECUTENATIVE insn){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
308 MethodInfo mi = insn.getExecutedMethod();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
309 String s = mi.getName();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
310
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
311 if (s.equals("start")) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
312 s = "T" + lastTi.getId() + ".start";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
313 } else if (s.equals("wait")) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
314 s = "T" + lastTi.getId() + ".wait";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
315 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
316
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
317 return s;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
318 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
319
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
320 protected String getFieldAccessCG (JVMFieldInstruction insn){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
321 String s;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
322
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
323 if (insn instanceof JVMInstanceFieldInstruction) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
324
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
325 if (insn instanceof PUTFIELD) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
326 s = "put";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
327 } else /* if (insn instanceof GETFIELD) */ {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
328 s = "get";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
329 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
330
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
331 if (showTarget){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
332 int ref = ((JVMInstanceFieldInstruction) insn).getLastThis();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
333 s = getInstanceRef(ref) + '.' + s;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
334 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
335
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
336 } else /* if (insn instanceof StaticFieldInstruction) */ {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
337 if (insn instanceof PUTSTATIC) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
338 s = "put";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
339 } else /* if (insn instanceof GETSTATIC) */ {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
340 s = "get";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
341 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
342
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
343 if (showTarget){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
344 String clsName = ((JVMStaticFieldInstruction) insn).getLastClassName();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
345 s = Misc.stripToLastDot(clsName) + '.' + s;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
346 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
347 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
348
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
349 String varId = insn.getFieldName();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
350 s = s + ' ' + varId;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
351
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
352 return s;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
353 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
354
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
355 protected String getLockCG(LockInstruction insn){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
356 String s = "sync";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
357
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
358 if (showTarget){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
359 int ref = insn.getLastLockRef();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
360 s = getInstanceRef(ref) + '.' + s;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
361 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
362
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
363 return s;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
364 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
365
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
366 protected String getInvokeCG (JVMInvokeInstruction insn){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
367 MethodInfo mi = insn.getInvokedMethod();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
368 String s = mi.getName() + "()";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
369
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
370 if (showTarget){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
371 if (insn instanceof InstanceInvocation) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
372 int ref = ((InstanceInvocation) insn).getLastObjRef();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
373 s = getInstanceRef(ref) + '.' + s;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
374
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
375 } else if (insn instanceof INVOKESTATIC) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
376 String clsName = ((INVOKESTATIC) insn).getInvokedClassName();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
377 s = Misc.stripToLastDot(clsName) + '.' + s;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
378 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
379 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
380
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
381 return s;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
382 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
383
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
384 protected String getError (Search search){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
385 String e;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
386 Error error = search.getLastError();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
387 Property prop = error.getProperty();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
388
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
389 if (prop instanceof NoUncaughtExceptionsProperty){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
390 ExceptionInfo xi = ((NoUncaughtExceptionsProperty)prop).getUncaughtExceptionInfo();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
391 return Misc.stripToLastDot(xi.getExceptionClassname());
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
392
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
393 } else if (prop instanceof NotDeadlockedProperty){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
394 return "deadlock";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
395 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
396
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
397 // fallback
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
398 return Misc.stripToLastDot(prop.getClass().getName());
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
399 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
400
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
401 protected static String getInstanceRef (int ref){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
402 return "@" + Integer.toHexString(ref).toUpperCase();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
403 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
404
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
405 protected static String getClassObjectRef (int ref){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
406 return "#" + Integer.toHexString(ref).toUpperCase();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
407 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
408
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
409 //--- dot file stuff
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
410
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
411 protected void printHeader(){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
412 pw.print("digraph ");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
413 pw.print(app);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
414 pw.println(" {");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
415
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
416 pw.print("node [");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
417 pw.print(genericNodeAttrs);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
418 pw.println(']');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
419
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
420 pw.print("edge [");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
421 pw.print(genericEdgeAttrs);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
422 pw.println(']');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
423
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
424 pw.println(graphAttrs);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
425
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
426 pw.println();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
427 pw.print("label=\"");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
428 pw.print(app);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
429 pw.print("\"");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
430 pw.println();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
431 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
432
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
433 protected void printTransition(String fromState, String toState, String choiceVal, String cgCause){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
434 pw.println();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
435 pw.print(fromState);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
436 pw.print(" -> ");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
437 pw.print( toState);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
438 pw.print(" [label=\"");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
439 pw.print(choiceVal);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
440 pw.print('"');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
441 if (cgCause != null){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
442 pw.print(NEW_EDGE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
443 pw.print(",headlabel=\"");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
444 pw.print(cgCause);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
445 pw.print('"');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
446 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
447 pw.print(VISITED_EDGE_ATTRS);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
448 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
449 pw.println(']');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
450 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
451
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
452 protected void printBacktrack (String fromState, String toState){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
453 pw.println();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
454 pw.print(fromState);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
455 pw.print(" -> ");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
456 pw.print( toState);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
457
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
458 pw.print(" [");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
459 pw.print(backtrackEdgeAttrs);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
460 pw.print(']');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
461
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
462 pw.println(" // backtrack");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
463 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
464
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
465 protected void printRestored (String fromState, String toState){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
466 pw.println();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
467 pw.print(fromState);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
468 pw.print(" -> ");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
469 pw.print( toState);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
470
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
471 pw.print(" [");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
472 pw.print(restoreEdgeAttrs);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
473 pw.print(']');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
474
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
475 pw.println(" // restored");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
476 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
477
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
478 protected void printStartState(String stateId){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
479 pw.print(stateId);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
480
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
481 pw.print(" [");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
482 pw.print(startNodeAttrs);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
483 pw.print(']');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
484
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
485 pw.println(" // start state");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
486 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
487
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
488 protected void printEndState(String stateId){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
489 pw.print(stateId);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
490
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
491 pw.print(" [");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
492 pw.print(endNodeAttrs);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
493 pw.print(']');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
494
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
495 pw.println(" // end state");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
496 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
497
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
498 protected void printErrorState(String error){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
499 pw.print(error);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
500
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
501 pw.print(" [");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
502 pw.print(errorNodeAttrs);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
503 pw.print(']');
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
504
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
505 pw.println(" // error state");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
506 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
507 }