|
1 package gov.nasa.jpf.tools;
20
21 import java.io.BufferedReader  ;
22 import java.io.InputStreamReader ;
23 import java.io.PrintWriter ;
24 import java.io.IOException ;
25 import java.net.ConnectException ;
26 import java.net.ServerSocket ;
27 import java.net.Socket ;
28 import java.net.UnknownHostException ;
29
30 import gov.nasa.jpf.Config;
31 import gov.nasa.jpf.JPF;
32 import gov.nasa.jpf.Search;
33 import gov.nasa.jpf.SearchListener;
34
35 import gov.nasa.jpf.search.heuristic.*;
36
37
42 public class SearchMonitor implements SearchListener {
43
44 static final String DEF_HOSTNAME = "localhost";
45 static final int DEF_PORT = 20000;
46 static final int DEF_INTERVAL = 1000;
48 String hostName = DEF_HOSTNAME;
49 int port = DEF_PORT;
50
51 Socket sock;
52 PrintWriter out;
53
54 int reportNumber;
55
56 int interval = DEF_INTERVAL;
57 long time;
58 long lastTime;
59 long startTime;
60 long startFreeMemory;
61
62 int searchLevel;
63
64 int newStates;
65 int endStates;
66 int backtracks;
67 int visitedStates;
68 int processedStates;
69 int restoredStates;
70
71 int steps;
72
73 long maxMemory;
74 long totalMemory;
75 long freeMemory;
76
77 boolean isHeuristic = false;
78 int queueSize = 0;
79
80
83
84 public void stateAdvanced(Search search) {
85
86 steps += search.getTransition().getStepCount();
87
88 if (isHeuristic)
89 queueSize = ((HeuristicSearch)(search)).getQueueSize();
90
91 if (search.isNewState()) {
92 searchLevel = search.getSearchDepth();
93 newStates++;
94
95 if (search.isEndState()) {
96 endStates++;
97 }
98 } else {
99 visitedStates++;
100 }
101
102 checkReport();
103 }
104
105 public void stateProcessed(Search search) {
106 processedStates++;
107 checkReport();
108 }
109
110 public void stateBacktracked(Search search) {
111 searchLevel = search.getSearchDepth();
112 backtracks++;
113 checkReport();
114 }
115
116 public void stateRestored(Search search) {
117 searchLevel = search.getSearchDepth();
118 restoredStates++;
119 checkReport();
120 }
121
122 public void propertyViolated(Search search) {
123 }
124
125 public void searchStarted(Search search) {
126 connect();
127
128 if (search instanceof HeuristicSearch)
129 isHeuristic = true;
130
131 startTime = lastTime = System.currentTimeMillis();
132
133 Runtime rt = Runtime.getRuntime();
134 startFreeMemory = rt.freeMemory();
135 totalMemory = rt.totalMemory();
136 maxMemory = rt.maxMemory();
137 reportNumber = 1;
138 }
139
140 public void searchConstraintHit(Search search) {
141 }
142
143 public void searchFinished(Search search) {
144 report("------------------------------------ statistics");
145
146 if (sock != null) {
147 try {
148 out.close();
149 sock.close();
150 } catch (IOException iox) {
151 }
152 }
153 }
154
155 void checkReport () {
156 time = System.currentTimeMillis();
157
158 Runtime rt = Runtime.getRuntime();
159 long m = rt.totalMemory();
160 if (m > totalMemory) {
161 totalMemory = m;
162 }
163
164 if ((time - lastTime) >= interval) {
165 freeMemory = rt.freeMemory();
166
167 report("# " + reportNumber++);
168 lastTime = time;
169 }
170 }
171
172 void reportRuntime () {
173 long td = time - startTime;
174
175 int h = (int) (td / 3600000);
176 int m = (int) (td / 60000) % 60;
177 int s = (int) (td / 1000) % 60;
178
179 out.print(" abs time: ");
180 if (h < 10) out.print('0');
181 out.print( h);
182 out.print(':');
183 if (m < 10) out.print('0');
184 out.print( m);
185 out.print(':');
186 if (s < 10) out.print('0');
187 out.print( s);
188
189 out.print( " (");
190 out.print(td);
191 out.println(" ms)");
192 }
193
194 void report (String header) {
195
196 out.println(header);
197
198 reportRuntime();
199
200 out.print(" rel. time [ms]: ");
201 out.println(time - lastTime);
202
203 out.println();
204 out.print(" search depth: ");
205 out.println(searchLevel);
206
207 out.print(" new states: ");
208 out.println(newStates);
209
210 out.print(" visited states: ");
211 out.println(visitedStates);
212
213 out.print(" end states: ");
214 out.println(endStates);
215
216 out.print(" backtracks: ");
217 out.println(backtracks);
218
219 out.print(" processed states: ");
220 out.print( processedStates);
221 out.print(" (");
222 double d = (double) backtracks / (double)processedStates;
224 int n = (int) d;
225 int m = (int) ((d-(double)n)*10.0);
226 out.print( n);
227 out.print('.');
228 out.print(m);
229 out.println( " bt/proc state)");
230
231 out.print(" restored states: ");
232 out.println(restoredStates);
233
234 if (isHeuristic) {
235 out.print(" queue size: ");
236 out.println(queueSize);
237 }
238
239 out.println();
240 out.print(" total memory [kB]: ");
241 out.print(totalMemory / 1024);
242 out.print(" (max: ");
243 out.print(maxMemory / 1024);
244 out.println(")");
245
246 out.print(" free memory [kB]: ");
247 out.println(freeMemory / 1024);
248
249 out.println();
250 }
251
252 int consumeIntArg (String [] args, int i, String varName, int def) {
253 int ret = def;
254
255 args[i] = null;
256 if (i < args.length-1){
257 i++;
258 try {
259 ret = Integer.parseInt(args[i]);
260 args[i] = null;
261 } catch (NumberFormatException nfx) {
262 System.err.print("Warning: illegal " + varName + " specification: " + args[i]
263 + " using default " + ret);
264 }
265 }
266
267 return ret;
268 }
269
270 void filterArgs (String [] args) {
271 for (int i=0; i<args.length; i++) {
272 if (args[i].equals("-port")) {
273 port = consumeIntArg(args, i++, "port", DEF_PORT);
274 } else if (args[i].equals("-interval")) {
275 interval = consumeIntArg(args, i++, "interval", DEF_INTERVAL);
276 } else if (args[i].equals("-hostname")) {
277 args[i] = null;
278 if (i < args.length-1){
279 i++;
280 hostName = args[i];
281 args[i] = null;
282 }
283 }
284 }
285 }
286
287 static void printUsage () {
288 System.out.println("SearchMonitor - a JPF listener tool to monitor JPF searches");
289 System.out.println("usage: java gov.nasa.jpf.tools.SearchMonitor <jpf-options> <monitor-options> <class>");
290 System.out.println("<monitor-options>:");
291 System.out.println(" -hostname <name> : connect to host <name>, default: " + DEF_HOSTNAME);
292 System.out.println(" -port <num> : connect to port <num>, default: " + DEF_PORT);
293 System.out.println(" -interval <num> : report every <num> msec, default: " + DEF_INTERVAL);
294 }
295
296
297 void connect () {
298
299 try {
300 sock = new Socket (hostName, port);
301 out = new PrintWriter (sock.getOutputStream(), true);
302 } catch (UnknownHostException uhx) {
303 System.err.println("Warning: unknown log host: " + hostName + ", using System.out");
304 } catch (ConnectException cex) {
305 System.err.println("Warning: no log host detected, using System.out");
306 } catch (IOException iox) {
307 System.err.println(iox);
308 }
309
310 if (out == null) {
311 out = new PrintWriter (System.out, true);
312 }
313 }
314
315 public void run (Config conf) {
316 JPF jpf = new JPF(conf);
317 jpf.addSearchListener(this);
318
319 jpf.run();
320 }
321
322 public static void main (String [] args) {
323 if (args.length == 0) {
324 printUsage();
325 return;
326 }
327
328 Config conf = JPF.createConfig(args);
329 SearchMonitor listener = new SearchMonitor(conf);
330
331 listener.filterArgs(args);
332 listener.run(conf);
333 }
334
335 public SearchMonitor (Config config) {
336 hostName = config.getString("monitor.hostname", DEF_HOSTNAME);
337 port = config.getInt("monitor.port", DEF_PORT);
338 interval = config.getInt("monitor.interval", DEF_INTERVAL);
339 }
340 }
341 |
Popular Tags |
Java API By Example, From Geeks To Geeks.