001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf.tools;
020:
021: import java.io.BufferedReader;
022: import java.io.InputStreamReader;
023: import java.io.PrintWriter;
024: import java.io.IOException;
025: import java.net.ConnectException;
026: import java.net.ServerSocket;
027: import java.net.Socket;
028: import java.net.UnknownHostException;
029:
030: import gov.nasa.jpf.Config;
031: import gov.nasa.jpf.JPF;
032: import gov.nasa.jpf.Search;
033: import gov.nasa.jpf.SearchListener;
034:
035: import gov.nasa.jpf.search.heuristic.*;
036:
037: /**
038: * SearchListener class to collect and report statistical
039: * data during JPF execution.
040: * This replaces the old JPF Statistics mechanism
041: */
042: public class SearchMonitor implements SearchListener {
043:
044: static final String DEF_HOSTNAME = "localhost";
045: static final int DEF_PORT = 20000;
046: static final int DEF_INTERVAL = 1000; // min duration in ms between reports
047:
048: String hostName = DEF_HOSTNAME;
049: int port = DEF_PORT;
050:
051: Socket sock;
052: PrintWriter out;
053:
054: int reportNumber;
055:
056: int interval = DEF_INTERVAL;
057: long time;
058: long lastTime;
059: long startTime;
060: long startFreeMemory;
061:
062: int searchLevel;
063:
064: int newStates;
065: int endStates;
066: int backtracks;
067: int visitedStates;
068: int processedStates;
069: int restoredStates;
070:
071: int steps;
072:
073: long maxMemory;
074: long totalMemory;
075: long freeMemory;
076:
077: boolean isHeuristic = false;
078: int queueSize = 0;
079:
080: /*
081: * SearchListener interface
082: */
083:
084: public void stateAdvanced(Search search) {
085:
086: steps += search.getTransition().getStepCount();
087:
088: if (isHeuristic)
089: queueSize = ((HeuristicSearch) (search)).getQueueSize();
090:
091: if (search.isNewState()) {
092: searchLevel = search.getSearchDepth();
093: newStates++;
094:
095: if (search.isEndState()) {
096: endStates++;
097: }
098: } else {
099: 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)
181: out.print('0');
182: out.print(h);
183: out.print(':');
184: if (m < 10)
185: out.print('0');
186: out.print(m);
187: out.print(':');
188: if (s < 10)
189: out.print('0');
190: out.print(s);
191:
192: out.print(" (");
193: out.print(td);
194: out.println(" ms)");
195: }
196:
197: void report(String header) {
198:
199: out.println(header);
200:
201: reportRuntime();
202:
203: out.print(" rel. time [ms]: ");
204: out.println(time - lastTime);
205:
206: out.println();
207: out.print(" search depth: ");
208: out.println(searchLevel);
209:
210: out.print(" new states: ");
211: out.println(newStates);
212:
213: out.print(" visited states: ");
214: out.println(visitedStates);
215:
216: out.print(" end states: ");
217: out.println(endStates);
218:
219: out.print(" backtracks: ");
220: out.println(backtracks);
221:
222: out.print(" processed states: ");
223: out.print(processedStates);
224: out.print(" (");
225: // a little ad-hoc rounding
226: double d = (double) backtracks / (double) processedStates;
227: int n = (int) d;
228: int m = (int) ((d - (double) n) * 10.0);
229: out.print(n);
230: out.print('.');
231: out.print(m);
232: out.println(" bt/proc state)");
233:
234: out.print(" restored states: ");
235: out.println(restoredStates);
236:
237: if (isHeuristic) {
238: out.print(" queue size: ");
239: out.println(queueSize);
240: }
241:
242: out.println();
243: out.print(" total memory [kB]: ");
244: out.print(totalMemory / 1024);
245: out.print(" (max: ");
246: out.print(maxMemory / 1024);
247: out.println(")");
248:
249: out.print(" free memory [kB]: ");
250: out.println(freeMemory / 1024);
251:
252: out.println();
253: }
254:
255: int consumeIntArg(String[] args, int i, String varName, int def) {
256: int ret = def;
257:
258: args[i] = null;
259: if (i < args.length - 1) {
260: i++;
261: try {
262: ret = Integer.parseInt(args[i]);
263: args[i] = null;
264: } catch (NumberFormatException nfx) {
265: System.err.print("Warning: illegal " + varName
266: + " specification: " + args[i]
267: + " using default " + ret);
268: }
269: }
270:
271: return ret;
272: }
273:
274: void filterArgs(String[] args) {
275: for (int i = 0; i < args.length; i++) {
276: if (args[i].equals("-port")) {
277: port = consumeIntArg(args, i++, "port", DEF_PORT);
278: } else if (args[i].equals("-interval")) {
279: interval = consumeIntArg(args, i++, "interval",
280: DEF_INTERVAL);
281: } else if (args[i].equals("-hostname")) {
282: args[i] = null;
283: if (i < args.length - 1) {
284: i++;
285: hostName = args[i];
286: args[i] = null;
287: }
288: }
289: }
290: }
291:
292: static void printUsage() {
293: System.out
294: .println("SearchMonitor - a JPF listener tool to monitor JPF searches");
295: System.out
296: .println("usage: java gov.nasa.jpf.tools.SearchMonitor <jpf-options> <monitor-options> <class>");
297: System.out.println("<monitor-options>:");
298: System.out
299: .println(" -hostname <name> : connect to host <name>, default: "
300: + DEF_HOSTNAME);
301: System.out
302: .println(" -port <num> : connect to port <num>, default: "
303: + DEF_PORT);
304: System.out
305: .println(" -interval <num> : report every <num> msec, default: "
306: + DEF_INTERVAL);
307: }
308:
309: void connect() {
310:
311: try {
312: sock = new Socket(hostName, port);
313: out = new PrintWriter(sock.getOutputStream(), true);
314: } catch (UnknownHostException uhx) {
315: System.err.println("Warning: unknown log host: " + hostName
316: + ", using System.out");
317: } catch (ConnectException cex) {
318: System.err
319: .println("Warning: no log host detected, using System.out");
320: } catch (IOException iox) {
321: System.err.println(iox);
322: }
323:
324: if (out == null) {
325: out = new PrintWriter(System.out, true);
326: }
327: }
328:
329: public void run(Config conf) {
330: JPF jpf = new JPF(conf);
331: jpf.addSearchListener(this );
332:
333: jpf.run();
334: }
335:
336: public static void main(String[] args) {
337: if (args.length == 0) {
338: printUsage();
339: return;
340: }
341:
342: Config conf = JPF.createConfig(args);
343: SearchMonitor listener = new SearchMonitor(conf);
344:
345: listener.filterArgs(args);
346: listener.run(conf);
347: }
348:
349: public SearchMonitor(Config config) {
350: hostName = config.getString("monitor.hostname", DEF_HOSTNAME);
351: port = config.getInt("monitor.port", DEF_PORT);
352: interval = config.getInt("monitor.interval", DEF_INTERVAL);
353: }
354: }
|