Status.java Source File

00001 package gov.nasa.arc.ase.jpf;
00002 
00003 import java.io.Serializable;
00004 
00005 import gov.nasa.arc.ase.util.Debug;
00006 import gov.nasa.arc.ase.util.Comma;
00007 import gov.nasa.arc.ase.util.kMG;
00008 import gov.nasa.arc.ase.util.hms;
00009 
00010 import gov.nasa.arc.ase.jpf.jvm.VirtualMachine;
00011 
00012 /**
00013  * This class represents the status of the model checker.
00014  */
00015 public class Status implements Serializable {
00016   /**
00017    * Number of states that has been visited.
00018    */
00019   public int    states      = 0;
00020 
00021   /**
00022    * Number of transitions that has been executed.
00023    */
00024   public int    transitions = 0;
00025 
00026   /**
00027    * Number of instruction that has been executed.
00028    */
00029   public int    instructions    = 0;
00030 
00031   /**
00032    * Size of the heap used to store objects.
00033    */
00034   public long   memory      = 0;
00035 
00036   /**
00037    * Size of the heap after running the garbage
00038    * collector.
00039    */
00040   public long   memoryGC    = 0;
00041 
00042   /**
00043    * Memory used to store states in the hash table.
00044    */
00045   public int    storageMemory   = 0;
00046 
00047 //#ifdef HEURISTIC
00048 
00049 
00050 
00051 
00052 
00053 
00054 
00055 
00056 
00057 
00058 
00059 
00060 
00061 
00062 
00063 
00064 
00065 
00066 
00067 
00068 
00069 
00070 
00071 
00072 
00073 
00074 
00075 
00076 
00077 
00078 
00079 //#endif HEURISTIC
00080 
00081 //#ifdef RACE
00082 
00083 
00084 
00085 
00086 
00087 
00088 //#endif RACE
00089 
00090 //#ifdef LOCK_ORDER
00091 
00092 
00093 
00094 
00095 
00096 
00097 //#endif LOCK_ORDER
00098 
00099 
00100 //#ifdef MARK_N_SWEEP
00101 
00102   /**
00103    * Number of types the garbage collector has been
00104    * activated.
00105    */
00106   public int   GCRuns       = 0;
00107 
00108 //#endif MARK_N_SWEEP
00109 
00110 //#ifdef MARK_N_SWEEP || REFERENCE_COUNT
00111 
00112   /**
00113    * Number of objects collected by the garbage
00114    * collector.
00115    */
00116   public int   GCs      = 0;
00117 
00118 //#endif MARK_N_SWEEP || REFERENCE_COUNT
00119 
00120   /**
00121    * Time the verification was started.
00122    */
00123   public static long startingTime = System.currentTimeMillis();
00124 
00125   /**
00126    * Current maximum depth searched by the stack.
00127    */
00128   public int maxStackDepth  = 0;
00129 
00130 //#ifdef STACK_STATS
00131 
00132 
00133 
00134 
00135 
00136 
00137 
00138 
00139 
00140 
00141 
00142 
00143 
00144 
00145 
00146 
00147 //#endif STACK_STATS
00148 
00149   /**
00150    * Number of intermediate transitions.
00151    */
00152   public int intermediateTransitions = 0;
00153 
00154 //#ifdef BUCHI
00155 
00156   /**
00157    * Number of unique states stored.
00158    */
00159   public int unique = 0;
00160 
00161 //#endif BUCHI
00162 
00163   /**
00164    * Initializes the status.
00165    */
00166   public Status() {
00167   }  
00168   /**
00169    * Creates a copy of a Status object.
00170    *
00171    * @param s a Status object
00172    */
00173   public Status(Status s) {
00174     states = s.states;
00175     transitions = s.transitions;
00176     instructions = s.instructions;
00177     memory = s.memory;
00178     memoryGC = s.memoryGC;
00179     storageMemory = s.storageMemory;
00180 //#ifdef RACE
00181 
00182 //#endif RACE
00183 //#ifdef LOCK_ORDER
00184 
00185 //#endif LOCK_ORDER
00186 //#ifdef HEURISTIC
00187 
00188 //#endif HEURISTIC
00189 //#ifdef MARK_N_SWEEP
00190     GCRuns = s.GCRuns;
00191 //#endif MARK_N_SWEEP
00192 //#ifdef MARK_N_SWEEP || REFERENCE_COUNT
00193     GCs = s.GCs;
00194 //#endif MARK_N_SWEEP || REFERENCE_COUNT
00195     maxStackDepth = s.maxStackDepth;
00196     /* removed by WV
00197 //#ifdef STACK_STATS
00198 
00199 
00200 //#endif STACK_STATS
00201     */
00202     intermediateTransitions = s.intermediateTransitions;
00203 //#ifdef BUCHI
00204     unique = s.unique;
00205 //#endif BUCHI
00206   }  
00207   /**
00208    * Adds the status of a node to the state of the system.
00209    */
00210   public void add(Status s) {
00211     states += s.states;
00212     transitions += s.transitions;
00213     instructions += s.instructions;
00214     memory += s.memory;
00215     memoryGC += s.memoryGC;
00216     storageMemory += s.storageMemory;
00217 
00218 //#ifdef RACE
00219 
00220 //#endif RACE
00221 
00222 //#ifdef LOCK_ORDER
00223 
00224 //#endif LOCK_ORDER
00225 
00226 //#ifdef MARK_N_SWEEP
00227     GCRuns += s.GCRuns;
00228 //#endif MARK_N_SWEEP
00229 
00230 //#ifdef MARK_N_SWEEP || REFERENCE_COUNT
00231     GCs += s.GCs;
00232 //#endif MARK_N_SWEEP || REFERENCE_COUNT
00233 
00234     maxStackDepth = Math.max(maxStackDepth, s.maxStackDepth);
00235 
00236     /* removed by WV
00237 //#ifdef STACK_STATS
00238 
00239 
00240 
00241 
00242 
00243 
00244 
00245 //#endif STACK_STATS
00246     */
00247     intermediateTransitions += s.intermediateTransitions;
00248 
00249 //#ifdef BUCHI
00250 
00251     unique += unique;
00252 
00253 //#endif BUCHI
00254 
00255   }  
00256   /**
00257    * Prints the current status to the console.
00258    */
00259   public void print() {
00260     updateMemoryUsage();
00261     long currentTime = System.currentTimeMillis();
00262     double deltaTime = currentTime - startingTime;
00263     int speed = (int)((transitions / deltaTime) * 1000);
00264 
00265     Debug.println(Debug.ERROR, "-----------------------------------");
00266     Debug.println(Debug.ERROR, "States visited       : " + Comma.format(states));
00267 //#ifdef BUCHI
00268     if(Engine.options.buchi != null)
00269       Debug.println(Debug.ERROR, "System states        : " + Comma.format(unique));
00270 //#endif BUCHI
00271 //#ifdef HEURISTIC
00272 
00273 
00274 
00275 
00276 
00277 
00278 
00279 
00280 
00281 
00282 //#endif HEURISTIC
00283 
00284     Debug.println(Debug.ERROR, "Transitions executed : " + Comma.format(transitions));
00285     Debug.println(Debug.ERROR, "Instructions executed: " + Comma.format(instructions));
00286 //#ifdef RACE
00287 
00288 
00289 //#endif RACE
00290 //#ifdef LOCK_ORDER
00291 
00292 
00293 //#endif LOCK_ORDER
00294     if(Engine.options.verify)
00295       Debug.println(Debug.ERROR, "Maximum stack depth  : " + Comma.format(maxStackDepth));
00296     Debug.println(Debug.ERROR, "Intermediate steps   : " + Comma.format(intermediateTransitions));
00297     Debug.println(Debug.ERROR, "Memory used          : " + kMG.format(memory) + "B");
00298     Debug.println(Debug.ERROR, "Memory used after gc : " + kMG.format(memoryGC) + "B");
00299     Debug.println(Debug.ERROR, "Storage memory       : " + kMG.format(storageMemory) + "B");
00300 //#ifdef MARK_N_SWEEP || REFERENCE_COUNT
00301     if(VirtualMachine.options.garbage_collection)
00302       Debug.println(Debug.ERROR, "Collected objects    : " + Comma.format(GCs));
00303 //#endif MARK_N_SWEEP || REFERENCE_COUNT
00304 //#ifdef MARK_N_SWEEP
00305     if(VirtualMachine.options.garbage_collection) {
00306       Debug.print(Debug.ERROR, "Mark and sweep runs  : ");
00307       Debug.println(Debug.ERROR, Comma.format(GCRuns));
00308     }
00309 //#endif MARK_N_SWEEP
00310     Debug.println(Debug.ERROR, "Execution time       : " + hms.format((long)deltaTime) + "s");
00311     Debug.println(Debug.ERROR, "Speed                : " + Comma.format(speed) + "tr/s");
00312     Debug.println(Debug.ERROR, "-----------------------------------");
00313   }  
00314   public int report(long deltaTime, int lastReportTransitions) {
00315     updateMemoryUsage();
00316     double deltaTransitions = transitions - lastReportTransitions;
00317     int speed = (int)((deltaTransitions/deltaTime) * 1000);
00318 
00319     Debug.println(Debug.WARNING,
00320     Comma.format(states) + 
00321     " tr " + Comma.format(transitions) +
00322     " sd " + Comma.format(maxStackDepth) +
00323 //#ifdef STACK_STATS
00324 
00325 
00326 
00327 
00328 
00329 //#endif STACK_STATS
00330 //#ifdef HEURISTIC
00331 
00332 //#endif HEURISTIC
00333     " spd " + Comma.format(speed) + "tr/s" +
00334         " mem " + kMG.format(memory));
00335 //#ifdef STACK_STATS
00336 
00337 //#endif STACK_STATS
00338 
00339     return transitions;
00340   }  
00341   /**
00342    * Updates the information regarding memory usage.
00343    */
00344   public void updateMemoryUsage() {
00345     Runtime runtime = Runtime.getRuntime();
00346 
00347     memory = runtime.totalMemory() - runtime.freeMemory();
00348     runtime.gc();
00349     memoryGC = runtime.totalMemory() - runtime.freeMemory();
00350   }  
00351 }