ResultInfo.java Source File

00001 package gov.nasa.arc.ase.jpf;
00002 
00003 import gov.nasa.arc.ase.jpf.jvm.VirtualMachine;
00004 import gov.nasa.arc.ase.util.Debug;
00005 import gov.nasa.arc.ase.util.kMG;
00006 import gov.nasa.arc.ase.util.Comma;
00007 import java.io.PrintStream;
00008 
00009 class ResultInfo implements java.io.Serializable {
00010 // ifdef RACE
00011   private int   race_conditions;
00012 //#endif RACE
00013 // ifdef MARK_N_SWEEP
00014   private int   GCRuns;
00015 //#endif MARK_N_SWEEP
00016 // ifdef MARK_N_SWEEP
00017   private int   GCs;
00018 //#endif MARK_N_SWEEP
00019   private int   states;
00020   private int   transitions;
00021   private long  time_used;
00022   private long  memory;
00023   private long  memory_gc;
00024 // ifdef NO_COMPRESSION
00025   private int   storage_memory;
00026 //#endif NO_COMPRESSION
00027 // ifdef DISTRIBUTED
00028 
00029 
00030 
00031 
00032 // ifdef NO_COMPRESSION
00033 
00034 //#endif NO_COMPRESSION
00035 
00036 
00037 
00038 // ifdef SIBLING_STORING
00039 
00040 //#endif SIBLING_STORING
00041 // ifdef SIBLING_STORING
00042 
00043 //#endif SIBLING_STORING
00044 // ifdef SIBLING_CACHING
00045 
00046 //#endif SIBLING_CACHING
00047 // ifdef CHILDREN_LOOKAHEAD
00048 
00049 //#endif CHILDREN_LOOKAHEAD
00050 //#endif DISTRIBUTED
00051   private int instructions;
00052 
00053   public ResultInfo() {
00054 // ifdef DISTRIBUTED
00055 
00056 
00057 
00058 
00059 
00060 
00061 
00062 // ifdef NO_COMPRESSION
00063 
00064 //#endif NO_COMPRESSION
00065 
00066 //#endif DISTRIBUTED
00067   }  
00068   public ResultInfo(rStatus s) {
00069     Runtime rt = Runtime.getRuntime();
00070 
00071 // ifdef RACE
00072     race_conditions = Runner.race_conditions;
00073 //#endif RACE
00074 // ifdef MARK_N_SWEEP
00075     GCRuns = Runner.GCRuns;
00076 //#endif MARK_N_SWEEP
00077 // ifdef MARK_N_SWEEP
00078     GCs = Runner.GCs;
00079 //#endif MARK_N_SWEEP
00080     states = s.states;
00081     transitions = s.transitions;
00082     time_used = System.currentTimeMillis() - s.begin_time;
00083     memory = (rt.totalMemory() - rt.freeMemory());
00084     rt.gc();
00085     memory_gc = (rt.totalMemory() - rt.freeMemory());
00086 // ifdef NO_COMPRESSION
00087     storage_memory = Runner.storage_memory;
00088 //#endif NO_COMPRESSION
00089 // ifdef DISTRIBUTED
00090 
00091 
00092 
00093 
00094 // ifdef SIBLING_STORING
00095 
00096 //#endif SIBLING_STORING
00097 // ifdef SIBLING_STORING
00098 
00099 //#endif SIBLING_STORING
00100 // ifdef SIBLING_CACHING
00101 
00102 //#endif SIBLING_CACHING
00103 // ifdef CHILDREN_LOOKAHEAD
00104 
00105 //#endif CHILDREN_LOOKAHEAD
00106 
00107 //#endif DISTRIBUTED
00108     instructions = Runner.instructions;
00109   }  
00110 // ifdef DISTRIBUTED
00111 
00112 // ifdef RACE
00113 
00114 //#endif RACE
00115 // ifdef MARK_N_SWEEP
00116 
00117 //#endif MARK_N_SWEEP
00118 // ifdef MARK_N_SWEEP
00119 
00120 //#endif MARK_N_SWEEP
00121 
00122 
00123 
00124 
00125 // ifdef NO_COMPRESSION
00126 
00127 //#endif NO_COMPRESSION
00128 
00129 
00130 
00131 
00132 // ifdef NO_COMPRESSION
00133 
00134 //#endif NO_COMPRESSION
00135 
00136 
00137 // ifdef SIBLING_STORING
00138 
00139 //#endif SIBLING_STORING
00140 // ifdef SIBLING_STORING
00141 
00142 //#endif SIBLING_STORING
00143 // ifdef SIBLING_CACHING
00144 
00145 //#endif SIBLING_CACHING
00146 // ifdef CHILDREN_LOOKAHEAD
00147 
00148 //#endif CHILDREN_LOOKAHEAD
00149 
00150 
00151 
00152 //#endif DISTRIBUTED
00153 
00154   public void print(PrintStream out, String message) {
00155     long minutes = (time_used / 1000) / 60;
00156     long seconds = (time_used / 1000) % 60;
00157     long milliseconds = (time_used % 1000);
00158     String stime_used = minutes + ":";
00159     if (seconds < 10) stime_used = stime_used + "0";
00160     stime_used = stime_used + seconds + ".";
00161     if (milliseconds < 100) stime_used = stime_used + "0";
00162     if (milliseconds < 10) stime_used = stime_used + "0";
00163     stime_used = stime_used + milliseconds + "s";
00164 // ifdef DISTRIBUTED
00165 
00166 //#endif DISTRIBUTED
00167 
00168     out.println("\n");
00169     out.println("*******************************");
00170     out.println(message);
00171     out.println("-------------------------------");
00172 // ifdef RACE
00173     if(VirtualMachine.options.race)
00174       out.println("Race conditions      : " + race_conditions);
00175 //#endif RACE
00176 // ifdef DISTRIBUTED
00177 
00178 
00179 
00180 
00181 
00182 
00183 
00184 
00185 
00186 
00187 
00188 
00189 
00190 
00191 
00192 
00193 
00194 
00195 // ifdef NO_COMPRESSION
00196 
00197 
00198 
00199 
00200 
00201 //#endif NO_COMPRESSION
00202 
00203 //#endif DISTRIBUTED
00204       out.println("States visited       : " + Comma.format(states));
00205       out.println("Transitions executed : " + Comma.format(transitions));
00206       out.println("Instructions executed: " + Comma.format(instructions));
00207       out.println("Memory Usage         : " + kMG.format(memory));
00208       out.println("Memory Usage gc      : " + kMG.format(memory_gc));
00209 // ifdef NO_COMPRESSION
00210       int p = (int)(0.5 + 100.0 * storage_memory / memory_gc);
00211       out.println("Storage Memory       : " + kMG.format(storage_memory) + " (" + p + "% of total memory)");
00212 //#endif NO_COMPRESSION
00213 // ifdef DISTRIBUTED
00214 
00215 //#endif DISTRIBUTED
00216     out.println("Time (min:sec:msec)  : " + stime_used);
00217     out.println("Speed (transition/s) : " + Comma.format(speed(transitions,time_used)) + "t/s");
00218     out.println("Speed (instruction/s): " + Comma.format(speed(instructions,time_used)) + "i/s");
00219 // ifdef DISTRIBUTED
00220 
00221 
00222 
00223 
00224 
00225 
00226 
00227 // ifdef SIBLING_STORING
00228 
00229 
00230 //#else SIBLING_STORING
00231 
00232 // ifdef SIBLING_STORING
00233 
00234 
00235 //#endif SIBLING_STORING
00236 
00237 // ifdef SIBLING_CACHING
00238 
00239 
00240 //#endif SIBLING_CACHING
00241 
00242 //#endif SIBLING_STORING
00243 
00244 // ifdef SIBLING_STORING
00245 
00246 
00247 //#endif SIBLING_STORING
00248 
00249 // ifdef SIBLING_CACHING
00250 
00251 
00252 //#endif SIBLING_CACHING
00253 
00254 // ifdef CHILDREN_LOOKAHEAD
00255 
00256 
00257 //#endif CHILDREN_LOOKAHEAD
00258 
00259 //#endif DISTRIBUTED
00260     out.println("*******************************");
00261   }  
00262   public void print(String message) {
00263     long minutes = time_used / 60000;
00264     long seconds = (time_used / 1000) % 60;
00265     long milliseconds = time_used % 1000;
00266     String stime_used = minutes + ":";
00267     if (seconds < 10) stime_used = stime_used + "0";
00268     stime_used = stime_used + seconds + ".";
00269     if (milliseconds < 100) stime_used = stime_used + "0";
00270     if (milliseconds < 10) stime_used = stime_used + "0";
00271     stime_used = stime_used + milliseconds + "s";
00272 // ifdef DISTRIBUTED
00273 
00274 //#endif DISTRIBUTED
00275 
00276     Debug.println(Debug.WARNING, "\n");
00277     Debug.println(Debug.WARNING, "*******************************");
00278     Debug.println(Debug.WARNING, message);
00279     Debug.println(Debug.WARNING, "-------------------------------");
00280 // ifdef RACE
00281     if(VirtualMachine.options.race)
00282       Debug.println(Debug.WARNING, "Race conditions      : " + race_conditions);
00283 //#endif RACE
00284 // ifdef DISTRIBUTED
00285 
00286 
00287 
00288 
00289 
00290 
00291 
00292 
00293 
00294 
00295 
00296 
00297 
00298 
00299 
00300 
00301 
00302 
00303 // ifdef NO_COMPRESSION
00304 
00305 
00306 
00307 
00308 
00309 //#endif NO_COMPRESSION
00310 
00311 //#endif DISTRIBUTED
00312       Debug.println(Debug.WARNING, "States visited       : " + Comma.format(states));
00313       Debug.println(Debug.WARNING, "Transitions executed : " + Comma.format(transitions));
00314       Debug.println(Debug.WARNING, "Instructions executed: " + Comma.format(instructions));
00315       Debug.println(Debug.WARNING, "Memory Usage         : " + kMG.format(memory));
00316       Debug.println(Debug.WARNING, "Memory Usage gc      : " + kMG.format(memory_gc));
00317 // ifdef NO_COMPRESSION
00318       int p = (int)(0.5 + 100.0 * storage_memory / memory_gc);
00319       Debug.println(Debug.WARNING, "Storage Memory       : " + kMG.format(storage_memory) + " (" + p + "% of total memory)");
00320 //#endif NO_COMPRESSION
00321 // ifdef DISTRIBUTED
00322 
00323 //#endif DISTRIBUTED
00324 // ifdef MARK_N_SWEEP
00325     if(VirtualMachine.options.garbage_collection) {
00326 // ifdef MARK_N_SWEEP
00327       Debug.println(Debug.WARNING, "GC runs              : " + GCRuns);
00328 //#endif MARK_N_SWEEP
00329       Debug.println(Debug.WARNING, "Objects Collected    : " + GCs);
00330     }
00331 //#endif MARK_N_SWEEP
00332     Debug.println(Debug.WARNING, "Time (min:sec:msec)  : " + stime_used);
00333     Debug.println(Debug.WARNING, "Speed (transition/s) : " + Comma.format(speed(transitions,time_used)) + "t/s");
00334     Debug.println(Debug.WARNING, "Speed (instruction/s): " + Comma.format(speed(instructions,time_used)) + "i/s");
00335 // ifdef DISTRIBUTED
00336 
00337 
00338 
00339 
00340 
00341 
00342 
00343 // ifdef SIBLING_STORING
00344 
00345 
00346 //#else SIBLING_STORING
00347 
00348 // ifdef SIBLING_STORING
00349 
00350 
00351 //#endif SIBLING_STORING
00352 
00353 // ifdef SIBLING_CACHING
00354 
00355 
00356 //#endif SIBLING_CACHING
00357 
00358 //#endif SIBLING_STORING
00359 
00360 // ifdef SIBLING_STORING
00361 
00362 
00363 //#endif SIBLING_STORING
00364 // ifdef SIBLING_CACHING
00365 
00366 
00367 //#endif SIBLING_CACHING
00368 // ifdef CHILDREN_LOOKAHEAD
00369 
00370 
00371 //#endif CHILDREN_LOOKAHEAD
00372 
00373 //#endif DISTRIBUTED
00374     Debug.println(Debug.WARNING, "*******************************");
00375   }  
00376   public void setTimeUsed(long t) {
00377     time_used = t;
00378   }  
00379 // ifdef DISTRIBUTED
00380 
00381 
00382 
00383 
00384 
00385 
00386 
00387 
00388 
00389 
00390 
00391 
00392 
00393 
00394 
00395 
00396 
00397 
00398 
00399 
00400 
00401 
00402 
00403 
00404 
00405 
00406 
00407 
00408 
00409 
00410 
00411 //#endif DISTRIBUTED
00412 
00413   public static long speed(long ticks, long time) {
00414     double a = (double)ticks;
00415     double b = (double)time;
00416 
00417     return (long)(a * 1000 / b);
00418   }  
00419 }