src/main/gov/nasa/jpf/listener/SearchStats.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   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
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  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.
  17  */
  18 package gov.nasa.jpf.listener;
  19
  20 import gov.nasa.jpf.ListenerAdapter;
  21 import gov.nasa.jpf.search.Search;
  22 import gov.nasa.jpf.search.heuristic.HeuristicSearch;
  23
  24 import java.io.PrintStream;
  25
  26 /**
  27  * An alternative to SearchMonitor that just reports statistics at the end.
  28  */
  29 public class SearchStats extends ListenerAdapter {
  30   PrintStream out = System.out;
  31
  32   long time;
  33   long startTime;
  34   long startFreeMemory;
  35
  36   int searchLevel=0;
  37   int maxSearchLevel=0;
  38
  39   int newStates;
  40   int endStates;
  41   int backtracks;
  42   int revisitedStates;
  43   int processedStates;
  44   int restoredStates;
  45
  46   int steps;
  47
  48   long maxMemory;
  49   long totalMemory;
  50   long freeMemory;
  51
  52   boolean isHeuristic = false;
  53   int queueSize = 0;
  54
  55   int currentHeapCount = 0;
  56   int maxHeapCount = 0;
  57
  58   /*
  59    * SearchListener interface
  60    */
  61   @Override
  62   public void stateAdvanced(Search search) {
  63     steps += search.getTransition().getStepCount();
  64
  65     if (isHeuristic)
  66         queueSize = ((HeuristicSearch)(search)).getQueueSize();
  67
  68     if (search.isNewState()) {
  69       searchLevel = search.getDepth();
  70       if (searchLevel > maxSearchLevel)
  71         maxSearchLevel = searchLevel;
  72
  73       newStates++;
  74
  75       currentHeapCount = search.getVM().getHeap().size();
  76
  77       if (currentHeapCount > maxHeapCount)
  78         maxHeapCount = currentHeapCount;
  79
  80       if (search.isEndState()) {
  81         endStates++;
  82       }
  83     } else {
  84       revisitedStates++;
  85     }
  86   }
  87
  88   @Override
  89   public void stateProcessed(Search search) {
  90     processedStates++;
  91   }
  92
  93   @Override
  94   public void stateBacktracked(Search search) {
  95     searchLevel = search.getDepth();
  96     backtracks++;
  97   }
  98
  99   @Override
 100   public void stateRestored(Search search) {
 101     searchLevel = search.getDepth();
 102     restoredStates++;
 103   }
 104
 105   @Override
 106   public void propertyViolated(Search search) {
 107   }
 108
 109   @Override
 110   public void searchStarted(Search search) {
 111     if (search instanceof HeuristicSearch) {
 112       isHeuristic = true;
 113     }
 114
 115     startTime = System.currentTimeMillis();
 116
 117     Runtime rt = Runtime.getRuntime();
 118     startFreeMemory = rt.freeMemory();
 119     totalMemory = rt.totalMemory();
 120     maxMemory = rt.maxMemory();
 121   }
 122
 123   @Override
 124   public void searchConstraintHit(Search search) {
 125   }
 126
 127   void reportRuntime () {
 128     long td = time - startTime;
 129
 130     int h = (int) (td / 3600000);
 131     int m = (int) (td / 60000) % 60;
 132     int s = (int) (td / 1000) % 60;
 133
 134     out.print("  abs time:          ");
 135     if (h < 10) out.print('0');
 136     out.print( h);
 137     out.print(':');
 138     if (m < 10) out.print('0');
 139     out.print( m);
 140     out.print(':');
 141     if (s < 10) out.print('0');
 142     out.print( s);
 143
 144     out.print( "  (");
 145     out.print(td);
 146     out.println(" ms)");
 147   }
 148
 149   @Override
 150   public void searchFinished(Search search) {
 151     report("------ Search statistics: ------");
 152   }
 153
 154   void report (String header) {
 155     time = System.currentTimeMillis();
 156
 157     out.println(header);
 158
 159     reportRuntime();
 160
 161     out.println();
 162     out.print("  search depth:      ");
 163     out.print(searchLevel);
 164     out.print(" (max: ");
 165     out.print(maxSearchLevel);
 166     out.println(")");
 167
 168     out.print("  new states:        ");
 169     out.println(newStates);
 170
 171     out.print("  revisited states:  ");
 172     out.println(revisitedStates);
 173
 174     out.print("  end states:        ");
 175     out.println(endStates);
 176
 177     out.print("  backtracks:        ");
 178     out.println(backtracks);
 179
 180     out.print("  processed states:  ");
 181     out.print( processedStates);
 182     out.print(" (");
 183     // a little ad-hoc rounding
 184     double d = (double) backtracks / (double)processedStates;
 185     int n = (int) d;
 186     int m = (int) ((d - /*(double)*/ n) * 10.0);
 187     out.print( n);
 188     out.print('.');
 189     out.print(m);
 190     out.println( " bt/proc state)");
 191
 192     out.print("  restored states:   ");
 193     out.println(restoredStates);
 194
 195     if (isHeuristic) {
 196         out.print("  queue size:        ");
 197         out.println(queueSize);
 198     }
 199
 200     out.println();
 201     out.print("  total memory [kB]: ");
 202     out.print(totalMemory / 1024);
 203     out.print(" (max: ");
 204     out.print(maxMemory / 1024);
 205     out.println(")");
 206
 207     out.print("  free memory [kB]:  ");
 208     out.println(freeMemory / 1024);
 209
 210     out.print("  max heap objects:  ");
 211     out.print(maxHeapCount);
 212
 213     out.println();
 214   }
 215 }