2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
18 package gov.nasa.jpf.listener;
20 import gov.nasa.jpf.ListenerAdapter;
21 import gov.nasa.jpf.search.Search;
22 import gov.nasa.jpf.search.heuristic.HeuristicSearch;
24 import java.io.PrintStream;
27 * An alternative to SearchMonitor that just reports statistics at the end.
29 public class SearchStats extends ListenerAdapter {
30 PrintStream out = System.out;
52 boolean isHeuristic = false;
55 int currentHeapCount = 0;
59 * SearchListener interface
62 public void stateAdvanced(Search search) {
63 steps += search.getTransition().getStepCount();
66 queueSize = ((HeuristicSearch)(search)).getQueueSize();
68 if (search.isNewState()) {
69 searchLevel = search.getDepth();
70 if (searchLevel > maxSearchLevel)
71 maxSearchLevel = searchLevel;
75 currentHeapCount = search.getVM().getHeap().size();
77 if (currentHeapCount > maxHeapCount)
78 maxHeapCount = currentHeapCount;
80 if (search.isEndState()) {
89 public void stateProcessed(Search search) {
94 public void stateBacktracked(Search search) {
95 searchLevel = search.getDepth();
100 public void stateRestored(Search search) {
101 searchLevel = search.getDepth();
106 public void propertyViolated(Search search) {
110 public void searchStarted(Search search) {
111 if (search instanceof HeuristicSearch) {
115 startTime = System.currentTimeMillis();
117 Runtime rt = Runtime.getRuntime();
118 startFreeMemory = rt.freeMemory();
119 totalMemory = rt.totalMemory();
120 maxMemory = rt.maxMemory();
124 public void searchConstraintHit(Search search) {
127 void reportRuntime () {
128 long td = time - startTime;
130 int h = (int) (td / 3600000);
131 int m = (int) (td / 60000) % 60;
132 int s = (int) (td / 1000) % 60;
134 out.print(" abs time: ");
135 if (h < 10) out.print('0');
138 if (m < 10) out.print('0');
141 if (s < 10) out.print('0');
150 public void searchFinished(Search search) {
151 report("------ Search statistics: ------");
154 void report (String header) {
155 time = System.currentTimeMillis();
162 out.print(" search depth: ");
163 out.print(searchLevel);
164 out.print(" (max: ");
165 out.print(maxSearchLevel);
168 out.print(" new states: ");
169 out.println(newStates);
171 out.print(" revisited states: ");
172 out.println(revisitedStates);
174 out.print(" end states: ");
175 out.println(endStates);
177 out.print(" backtracks: ");
178 out.println(backtracks);
180 out.print(" processed states: ");
181 out.print( processedStates);
183 // a little ad-hoc rounding
184 double d = (double) backtracks / (double)processedStates;
186 int m = (int) ((d - /*(double)*/ n) * 10.0);
190 out.println( " bt/proc state)");
192 out.print(" restored states: ");
193 out.println(restoredStates);
196 out.print(" queue size: ");
197 out.println(queueSize);
201 out.print(" total memory [kB]: ");
202 out.print(totalMemory / 1024);
203 out.print(" (max: ");
204 out.print(maxMemory / 1024);
207 out.print(" free memory [kB]: ");
208 out.println(freeMemory / 1024);
210 out.print(" max heap objects: ");
211 out.print(maxHeapCount);