MC.java Source File

00001 package gov.nasa.arc.ase.jpf;
00002 
00003 import gov.nasa.arc.ase.util.Debug;
00004 import java.io.*;
00005 import java.util.*;
00006 
00007 public class MC implements iSearch {
00008   private boolean verificationResult = false; // has there been an error
00009   private ErrorTrailInterface error;
00010   private Path errorPath;
00011   private SM buchi;
00012 
00013 // ifdef BUCHI
00014 
00015 
00016 
00017 
00018 
00019 
00020 
00021 
00022 
00023 
00024 
00025 
00026 
00027 
00028 
00029 
00030 
00031 
00032 
00033 
00034 
00035 
00036 
00037 
00038 
00039 
00040 
00041 
00042 
00043 
00044 
00045 
00046 
00047 
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 
00080 
00081 
00082 
00083 // ifdef DEBUG
00084 
00085 //#endif DEBUG
00086 
00087 
00088 
00089 
00090 
00091 
00092 
00093 // ifdef DEBUG
00094 
00095 //#endif DEBUG
00096 
00097 
00098 // ifdef DEBUG
00099 
00100 //#endif DEBUG
00101 
00102 
00103 
00104 
00105 
00106 
00107 
00108 
00109 
00110 // ifdef DEBUG
00111 
00112 //#endif DEBUG
00113 
00114 
00115 
00116 
00117 
00118 
00119 
00120 
00121 
00122 
00123 
00124 
00125 
00126 
00127 
00128 
00129 
00130 
00131 
00132 
00133 
00134 
00135 
00136 
00137 
00138 
00139 
00140 
00141 
00142 
00143 
00144 
00145 
00146 
00147 
00148 
00149 
00150 
00151 
00152 
00153 
00154 
00155 
00156 
00157 
00158 
00159 
00160 
00161 
00162 
00163 
00164 
00165 
00166 
00167 
00168 
00169 
00170 
00171 
00172 
00173 
00174 
00175 
00176 
00177 
00178 
00179 
00180 
00181 
00182 
00183 
00184 
00185 
00186 
00187 
00188 
00189 
00190 
00191 
00192 
00193 
00194 
00195 
00196 
00197 
00198 
00199 
00200 
00201 
00202 
00203 
00204 
00205 
00206 
00207 
00208 
00209 
00210 
00211 
00212 // ifdef DEBUG
00213 
00214 //#endif DEBUG
00215 
00216 
00217 
00218 
00219 // ifdef DEBUG
00220 
00221 //#endif DEBUG
00222 
00223 
00224 
00225 
00226 
00227 
00228 
00229 
00230 
00231 
00232 
00233 
00234 
00235 
00236 
00237 
00238 
00239 
00240 
00241 
00242 
00243 
00244 
00245 
00246 
00247 
00248 
00249 
00250 
00251 
00252 
00253 
00254 
00255 
00256 
00257 
00258 
00259 
00260 
00261 
00262 
00263 
00264 
00265 
00266 
00267 
00268 
00269 
00270 
00271 
00272 
00273 
00274 
00275 
00276 
00277 
00278 
00279 
00280 
00281 
00282 
00283 
00284 
00285 
00286 
00287 
00288 
00289 
00290 
00291 
00292 
00293 
00294 
00295 
00296 
00297 
00298 
00299 
00300 
00301 //#endif BUCHI
00302   public void Deadlock() {
00303 // ifdef DISTRIBUTED
00304 
00305 
00306 
00307 
00308 
00309 
00310 
00311 
00312 
00313 
00314 
00315 
00316 
00317 
00318 
00319 
00320 
00321 
00322 // ifdef DEBUG_DISTRIBUTED
00323 
00324 //#endif DEBUG_DISTRIBUTED
00325 
00326 // ifdef DEBUG_DISTRIBUTED
00327 
00328 //#endif DEBUG_DISTRIBUTED
00329 // ifdef CHILDREN_LOOKAHEAD
00330 
00331 
00332 
00333 //#endif CHILDREN_LOOKAHEAD
00334 
00335 
00336 
00337 
00338 
00339 
00340 // ifdef DEBUG_DISTRIBUTED
00341 
00342 //#endif DEBUG_DISTRIBUTED
00343 
00344 
00345 // ifdef DEBUG_DISTRIBUTED
00346 
00347 //#endif DEBUG_DISTRIBUTED
00348 
00349 
00350 
00351 
00352 
00353 
00354 
00355 // ifdef DEBUG_DISTRIBUTED
00356 
00357 //#endif DEBUG_DISTRIBUTED
00358 
00359 
00360 
00361 //#endif DISTRIBUTED
00362 
00363       /******************************************************************/
00364       if(Engine.options.path_simulation) {
00365     Path ePath = Engine.vm.getErrorTrail_from_file();
00366     Engine.vm.SimulateErrorTrail(ePath);
00367     error = Engine.vm.getErrorTrail();
00368     error.print();
00369     return;
00370       }
00371 
00372       else
00373     /******************************************************************/
00374 
00375     if(Engine.options.assertions)
00376       verifyAssertion();
00377 // ifdef BUCHI
00378 
00379 
00380 //#endif BUCHI
00381     else
00382       verifyDeadlock();
00383   }  
00384   public ErrorTrailInterface getError() {
00385     return error;
00386   }  
00387   public Path getErrorPath() {
00388     return errorPath;
00389   }  
00390   public boolean getResult() {
00391     return verificationResult;
00392   }  
00393   public void Invariant(iProperty p){
00394     //    verifyInvariant(p);
00395     //    Engine.status.print("The invariant is satisfied!");
00396   }  
00397   public void verifyAssertion() {
00398     int depth = 0;
00399 // ifdef DISTRIBUTED
00400 
00401 //#endif DISTRIBUTED
00402     int result;
00403 // ifdef DISTRIBUTED
00404 
00405 //#endif DISTRIBUTED
00406 
00407     Engine.status.incrStates(depth);
00408 // ifdef MESSAGE_SEARCH
00409 
00410 
00411 // ifdef DISTRIBUTED
00412 
00413 //#endif DISTRIBUTED
00414 
00415 
00416 
00417 
00418 
00419 // ifdef DISTRIBUTED
00420 
00421 
00422 
00423 
00424 
00425 
00426 //#endif DISTRIBUTED
00427 
00428 //#endif MESSAGE_SEARCH
00429     depth++;
00430     verificationResult = false;
00431     while(depth > 0 && !verificationResult) {
00432 // ifdef MESSAGE_SEARCH
00433 // ifdef DISTRIBUTED
00434 
00435 
00436 // ifdef DISTRIBUTED
00437 
00438 //#endif DISTRIBUTED
00439 
00440 
00441 
00442 
00443 //#endif DISTRIBUTED
00444 //#endif MESSAGE_SEARCH
00445       result = Engine.vm.Forward();
00446 // ifdef MESSAGE_SEARCH
00447 
00448 // ifdef DISTRIBUTED
00449 
00450 //#endif DISTRIBUTED
00451 
00452 
00453 
00454 
00455 
00456 
00457 
00458 // ifdef DISTRIBUTED
00459 
00460 
00461 
00462 
00463 
00464 
00465 //#endif DISTRIBUTED
00466 
00467 
00468 
00469 
00470 
00471 // ifdef DISTRIBUTED
00472 
00473 
00474 
00475 
00476 
00477 
00478 //#endif DISTRIBUTED
00479 
00480 
00481 
00482 
00483 
00484 // ifdef DISTRIBUTED
00485 
00486 
00487 
00488 
00489 
00490 
00491 //#endif DISTRIBUTED
00492 
00493 
00494 
00495 
00496 
00497 // ifdef DISTRIBUTED
00498 
00499 
00500 
00501 
00502 
00503 
00504 //#endif DISTRIBUTED
00505 
00506 
00507 
00508 //#endif MESSAGE_SEARCH
00509 
00510       if (TransitionResult.isAssertionViolated()) {
00511     verificationResult = true;
00512     if (Engine.options.bandera) {
00513       errorPath = Engine.vm.getErrorTrail1();
00514     } else {
00515       error = Engine.vm.getErrorTrail();        
00516     }
00517       } else {
00518     switch(result) {
00519       case RESULT.NEW : 
00520         depth++;
00521         Engine.status.incrStates(depth);
00522         Engine.status.incrTransitions(depth);
00523         break;
00524 
00525       case RESULT.OLD : 
00526         depth++;
00527         Engine.status.incrTransitions(depth);
00528 
00529       case RESULT.EXIT:
00530       case RESULT.END : 
00531         Engine.vm.Backtrack(); 
00532         depth--;
00533 // ifdef MESSAGE_SEARCH
00534 
00535 // ifdef DISTRIBUTED
00536 
00537 //#endif DISTRIBUTED
00538 
00539 
00540 
00541 
00542 
00543 //#endif MESSAGE_SEARCH
00544         break;           
00545     }
00546       }
00547     }
00548   }  
00549   public void verifyDeadlock() {
00550     int depth = 0;
00551 // ifdef DISTRIBUTED
00552 
00553 //#endif DISTRIBUTED
00554     boolean init = true;
00555     int result;
00556 // ifdef DISTRIBUTED
00557 
00558 //#endif DISTRIBUTED
00559 
00560     Engine.status.incrStates(depth);
00561 // ifdef MESSAGE_SEARCH
00562 
00563 
00564 // ifdef DISTRIBUTED
00565 
00566 //#endif DISTRIBUTED
00567 
00568 
00569 
00570 
00571 
00572 // ifdef DISTRIBUTED
00573 
00574 
00575 
00576 
00577 
00578 
00579 //#endif DISTRIBUTED
00580 
00581 //#endif MESSAGE_SEARCH
00582     depth++;
00583     verificationResult = false;
00584     while(depth > 0 && !verificationResult) {
00585 // ifdef MESSAGE_SEARCH
00586 // ifdef DISTRIBUTED
00587 
00588 
00589 // ifdef DISTRIBUTED
00590 
00591 //#endif DISTRIBUTED
00592 
00593 
00594 
00595 
00596 //#endif DISTRIBUTED
00597 //#endif MESSAGE_SEARCH
00598       result = Engine.vm.Forward();
00599 // ifdef MESSAGE_SEARCH
00600 
00601 // ifdef DISTRIBUTED
00602 
00603 //#endif DISTRIBUTED
00604 
00605 
00606 
00607 
00608 
00609 
00610 
00611 // ifdef DISTRIBUTED
00612 
00613 
00614 
00615 
00616 
00617 
00618 //#endif DISTRIBUTED
00619 
00620 
00621 
00622 
00623 
00624 // ifdef DISTRIBUTED
00625 
00626 
00627 
00628 
00629 
00630 
00631 //#endif DISTRIBUTED
00632 
00633 
00634 
00635 
00636 
00637 // ifdef DISTRIBUTED
00638 
00639 
00640 
00641 
00642 
00643 
00644 //#endif DISTRIBUTED
00645 
00646 
00647 
00648 
00649 
00650 // ifdef DISTRIBUTED
00651 
00652 
00653 
00654 
00655 
00656 
00657 //#endif DISTRIBUTED
00658 
00659 
00660 
00661 //#endif MESSAGE_SEARCH
00662 
00663       if (result == RESULT.END && init) {
00664     verificationResult = true;
00665     if (Engine.options.bandera) {
00666       errorPath = Engine.vm.getErrorTrail1();
00667     } else {
00668       error = Engine.vm.getErrorTrail();        
00669     }
00670       } else {
00671     init = false;
00672     switch(result) {
00673       case RESULT.NEW : 
00674         depth++;
00675         Engine.status.incrStates(depth);
00676         Engine.status.incrTransitions(depth);
00677         init = true;
00678         break;
00679 
00680       case RESULT.OLD : 
00681         depth++;
00682         Engine.status.incrTransitions(depth);
00683 
00684       case RESULT.EXIT:
00685       case RESULT.END : 
00686         Engine.vm.Backtrack(); 
00687         depth--;
00688 // ifdef MESSAGE_SEARCH
00689 
00690 // ifdef DISTRIBUTED
00691 
00692 //#endif DISTRIBUTED
00693 
00694 
00695 
00696 
00697 
00698 //#endif MESSAGE_SEARCH
00699         break;           
00700     }
00701       }
00702     }
00703   }  
00704 }