- Generated on Wed Oct 12 2011 00:34:50 for VIS by
1.7.3
|
VIS
|
00001 00025 #include "mcInt.h" 00026 00027 /*#define SCC_NO_TRIM */ 00028 00029 /*---------------------------------------------------------------------------*/ 00030 /* Constant declarations */ 00031 /*---------------------------------------------------------------------------*/ 00032 00033 /*---------------------------------------------------------------------------*/ 00034 /* Stucture declarations */ 00035 /*---------------------------------------------------------------------------*/ 00036 struct GraphNodeSpineSet { 00037 mdd_t *states; /* V */ 00038 mdd_t *spine; /* S */ 00039 mdd_t *node; /* Node */ 00040 }; 00041 00042 /*---------------------------------------------------------------------------*/ 00043 /* Type declarations */ 00044 /*---------------------------------------------------------------------------*/ 00045 typedef struct GraphNodeSpineSet gns_t; 00046 00047 /*---------------------------------------------------------------------------*/ 00048 /* Variable declarations */ 00049 /*---------------------------------------------------------------------------*/ 00050 00051 #ifndef lint 00052 static char rcsid[] UNUSED = "$Id: mcSCC.c,v 1.11 2005/05/18 19:35:19 jinh Exp $"; 00053 #endif 00054 00055 /*---------------------------------------------------------------------------*/ 00056 /* Macro declarations */ 00057 /*---------------------------------------------------------------------------*/ 00058 00061 /*---------------------------------------------------------------------------*/ 00062 /* Static function prototypes */ 00063 /*---------------------------------------------------------------------------*/ 00064 00065 static mdd_t * LockstepPickSeed(Fsm_Fsm_t *fsm, mdd_t *V, array_t *buechiFairness, array_t *onionRings, int ringIndex); 00066 static void LockstepQueueEnqueue(Fsm_Fsm_t *fsm, Heap_t *queue, mdd_t *states, array_t *onionRings, McLockstepMode mode, array_t *buechiFairness, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); 00067 static void LinearstepQueueEnqueue(Fsm_Fsm_t *fsm, Heap_t *queue, mdd_t *states, mdd_t *spine, mdd_t *node, array_t *onionRings, McLockstepMode mode, array_t *buechiFairness, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); 00068 static int GetSccEnumerationMethod( void ); 00069 00073 /*---------------------------------------------------------------------------*/ 00074 /* Definition of exported functions */ 00075 /*---------------------------------------------------------------------------*/ 00076 00077 00093 Mc_SccGen_t * 00094 Mc_FsmFirstScc( 00095 Fsm_Fsm_t *fsm, 00096 mdd_t **scc, 00097 array_t *sccClosedSetArray, 00098 array_t *buechiFairness, 00099 array_t *onionRings, 00100 boolean earlyTermination, 00101 Mc_VerbosityLevel verbosity, 00102 Mc_DcLevel dcLevel) 00103 { 00104 Mc_SccGen_t *gen; 00105 Heap_t *heap; 00106 int i; 00107 mdd_t *closedSet; 00108 int linearStepMethod; 00109 00110 if (fsm == NIL(Fsm_Fsm_t)) return NIL(Mc_SccGen_t); 00111 00112 /* Allocate generator and initialize it. */ 00113 gen = ALLOC(Mc_SccGen_t, 1); 00114 if (gen == NIL(Mc_SccGen_t)) return NIL(Mc_SccGen_t); 00115 00116 gen->fsm = fsm; 00117 gen->heap = heap = Heap_HeapInit(1); 00118 gen->rings = onionRings; 00119 gen->buechiFairness = buechiFairness; 00120 gen->earlyTermination = earlyTermination; 00121 gen->verbosity = verbosity; 00122 gen->dcLevel = dcLevel; 00123 gen->totalExamined = 0; 00124 gen->nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); 00125 gen->nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); 00126 00127 linearStepMethod = GetSccEnumerationMethod(); 00128 /* Initialize the heap from the given sets of states. */ 00129 arrayForEachItem(mdd_t *, sccClosedSetArray, i, closedSet) { 00130 if (linearStepMethod == 1) { 00131 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 00132 LinearstepQueueEnqueue(fsm, heap, mdd_dup(closedSet), 00133 mdd_zero(mddManager), 00134 mdd_zero(mddManager), onionRings, 00135 McLS_none_c, buechiFairness, verbosity, dcLevel); 00136 }else { 00137 LockstepQueueEnqueue(fsm, heap, mdd_dup(closedSet), onionRings, 00138 McLS_none_c, buechiFairness, verbosity, dcLevel); 00139 } 00140 } 00141 /* Find first SCC. */ 00142 if (Heap_HeapCount(heap) == 0) { 00143 *scc = NIL(mdd_t); 00144 } else { 00145 if (linearStepMethod == 1) 00146 *scc = McFsmComputeOneFairSccByLinearStep(fsm, heap, buechiFairness, 00147 onionRings, earlyTermination, 00148 verbosity, dcLevel, 00149 &(gen->totalExamined)); 00150 else 00151 *scc = McFsmComputeOneFairSccByLockStep(fsm, heap, buechiFairness, 00152 onionRings, earlyTermination, 00153 verbosity, dcLevel, 00154 &(gen->totalExamined)); 00155 } 00156 if (*scc == NIL(mdd_t)) { 00157 gen->status = McSccGenEmpty_c; 00158 gen->fairSccsFound = 0; 00159 } else { 00160 gen->status = McSccGenNonEmpty_c; 00161 gen->fairSccsFound = 1; 00162 } 00163 return gen; 00164 00165 } /* Mc_FsmFirstScc */ 00166 00167 00181 boolean 00182 Mc_FsmNextScc( 00183 Mc_SccGen_t *gen, 00184 mdd_t **scc) 00185 { 00186 int linearStepMethod; 00187 00188 if (gen->earlyTermination == TRUE) { 00189 gen->status = McSccGenEmpty_c; 00190 return FALSE; 00191 } 00192 linearStepMethod = GetSccEnumerationMethod(); 00193 if (linearStepMethod == 1) 00194 *scc = McFsmComputeOneFairSccByLinearStep(gen->fsm, gen->heap, 00195 gen->buechiFairness, gen->rings, 00196 gen->earlyTermination, 00197 gen->verbosity, gen->dcLevel, 00198 &(gen->totalExamined)); 00199 else 00200 *scc = McFsmComputeOneFairSccByLockStep(gen->fsm, gen->heap, 00201 gen->buechiFairness, gen->rings, 00202 gen->earlyTermination, 00203 gen->verbosity, gen->dcLevel, 00204 &(gen->totalExamined)); 00205 if (*scc == NIL(mdd_t)) { 00206 gen->status = McSccGenEmpty_c; 00207 return FALSE; 00208 } else { 00209 gen->status = McSccGenNonEmpty_c; 00210 gen->fairSccsFound++; 00211 return TRUE; 00212 } 00213 00214 } /* Mc_FsmNextScc */ 00215 00216 00228 boolean 00229 Mc_FsmIsSccGenEmpty( 00230 Mc_SccGen_t *gen) 00231 { 00232 if (gen == NIL(Mc_SccGen_t)) return TRUE; 00233 return gen->status == McSccGenEmpty_c; 00234 00235 } /* Mc_FsmIsSccGenEmpty */ 00236 00237 00254 boolean 00255 Mc_FsmSccGenFree( 00256 Mc_SccGen_t *gen, 00257 array_t *leftover) 00258 { 00259 int linearStepMethod; 00260 00261 if (gen == NIL(Mc_SccGen_t)) return FALSE; 00262 /* Print some stats. */ 00263 if (gen->verbosity == McVerbositySome_c || gen->verbosity == McVerbosityMax_c) { 00264 fprintf(vis_stdout, 00265 "--SCC: found %d fair SCC(s) out of %d examined\n", 00266 gen->fairSccsFound, gen->totalExamined); 00267 fprintf(vis_stdout, 00268 "--SCC: %d image computations, %d preimage computations\n", 00269 Img_GetNumberOfImageComputation(Img_Forward_c) - gen->nImgComps, 00270 Img_GetNumberOfImageComputation(Img_Backward_c) - gen->nPreComps); 00271 } 00272 /* Create array from elements still on queue if so requested. */ 00273 linearStepMethod = GetSccEnumerationMethod(); 00274 if (linearStepMethod == 1) { 00275 while (Heap_HeapCount(gen->heap)) { 00276 gns_t *set; 00277 long index; 00278 int retval UNUSED = Heap_HeapExtractMin(gen->heap, &set, &index); 00279 assert(retval); 00280 if (leftover == NIL(array_t) || gen->earlyTermination == TRUE) { 00281 mdd_free(set->states); 00282 } else { 00283 array_insert_last(mdd_t *, leftover, set->states); 00284 } 00285 mdd_free(set->spine); mdd_free(set->node); 00286 FREE(set); 00287 } 00288 }else { 00289 while (Heap_HeapCount(gen->heap)) { 00290 mdd_t *set; 00291 long index; 00292 int retval UNUSED = Heap_HeapExtractMin(gen->heap, &set, &index); 00293 assert(retval); 00294 if (leftover == NIL(array_t) || gen->earlyTermination == TRUE) { 00295 mdd_free(set); 00296 } else { 00297 array_insert_last(mdd_t *, leftover, set); 00298 } 00299 } 00300 } 00301 00302 Heap_HeapFree(gen->heap); 00303 FREE(gen); 00304 return FALSE; 00305 00306 } /* Mc_FsmSccGenFree */ 00307 00308 00327 mdd_t * 00328 McFsmComputeFairSCCsByLockStep( 00329 Fsm_Fsm_t *fsm, 00330 int maxNumberOfSCCs, 00331 array_t *SCCs, 00332 array_t *onionRingsArrayForDbg, 00333 Mc_VerbosityLevel verbosity, 00334 Mc_DcLevel dcLevel) 00335 { 00336 Mc_SccGen_t *sccGen; 00337 mdd_t *mddOne, *reached, *hull, *scc, *fairStates; 00338 array_t *onionRings, *sccClosedSetArray, *careStatesArray; 00339 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 00340 int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); 00341 int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); 00342 Fsm_Fairness_t *modelFairness = Fsm_FsmReadFairnessConstraint(fsm); 00343 array_t *buechiFairness = array_alloc(mdd_t *, 0); 00344 00345 /* Initialization. */ 00346 mddOne = mdd_one(mddManager); 00347 00348 sccClosedSetArray = array_alloc(mdd_t *, 0); 00349 reached = Fsm_FsmComputeReachableStates(fsm, 0, verbosity, 0, 0, 1, 0, 0, 00350 Fsm_Rch_Default_c, 0, 0, 00351 NIL(array_t), FALSE, NIL(array_t)); 00352 array_insert_last(mdd_t *, sccClosedSetArray, reached); 00353 onionRings = Fsm_FsmReadReachabilityOnionRings(fsm); 00354 00355 careStatesArray = array_alloc(mdd_t *, 0); 00356 array_insert_last(mdd_t *, careStatesArray, reached); 00357 Img_MinimizeTransitionRelation(Fsm_FsmReadOrCreateImageInfo(fsm, 1, 1), 00358 careStatesArray, Img_DefaultMinimizeMethod_c, 00359 Img_Both_c, FALSE); 00360 00361 /* Read fairness constraints. */ 00362 if (modelFairness != NIL(Fsm_Fairness_t)) { 00363 if (!Fsm_FairnessTestIsBuchi(modelFairness)) { 00364 (void) fprintf(vis_stdout, 00365 "** mc error: non-Buechi fairness constraints not supported\n"); 00366 array_free(buechiFairness); 00367 return NIL(mdd_t); 00368 } else { 00369 int j; 00370 int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0); 00371 for (j = 0; j < numBuchi; j++) { 00372 mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j, 00373 careStatesArray, 00374 dcLevel); 00375 array_insert_last(mdd_t *, buechiFairness, tmpMdd); 00376 } 00377 } 00378 } else { 00379 array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager)); 00380 } 00381 00382 /* Enumerate the fair SCCs and accumulate their disjunction in hull. */ 00383 hull = mdd_zero(mddManager); 00384 Mc_FsmForEachFairScc(fsm, sccGen, scc, sccClosedSetArray, NIL(array_t), 00385 buechiFairness, onionRings, 00386 maxNumberOfSCCs == MC_LOCKSTEP_EARLY_TERMINATION, 00387 verbosity, dcLevel) { 00388 mdd_t *tmp = mdd_or(hull, scc, 1, 1); 00389 mdd_free(hull); 00390 hull = tmp; 00391 array_insert_last(mdd_t *, SCCs, scc); 00392 if (maxNumberOfSCCs > MC_LOCKSTEP_ALL_SCCS && 00393 array_n(SCCs) == maxNumberOfSCCs) { 00394 Mc_FsmSccGenFree(sccGen, NIL(array_t)); 00395 break; 00396 } 00397 } 00398 00399 /* Compute (subset of) fair states and onion rings. */ 00400 if (onionRingsArrayForDbg != NIL(array_t)) { 00401 mdd_t *fairSet; 00402 int i; 00403 fairStates = Mc_FsmEvaluateEUFormula(fsm, reached, hull, 00404 NIL(mdd_t), mddOne, careStatesArray, 00405 MC_NO_EARLY_TERMINATION, 00406 NIL(array_t), Mc_None_c, NIL(array_t), 00407 verbosity, dcLevel, NIL(boolean)); 00408 arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) { 00409 mdd_t *restrictedFairSet = mdd_and(fairSet, hull, 1, 1); 00410 array_t *setOfRings = array_alloc(mdd_t *, 0); 00411 mdd_t *EU = Mc_FsmEvaluateEUFormula(fsm, fairStates, restrictedFairSet, 00412 NIL(mdd_t), mddOne, careStatesArray, 00413 MC_NO_EARLY_TERMINATION, 00414 NIL(array_t), Mc_None_c, setOfRings, 00415 verbosity, dcLevel, NIL(boolean)); 00416 array_insert_last(array_t *, onionRingsArrayForDbg, setOfRings); 00417 mdd_free(restrictedFairSet); 00418 mdd_free(EU); 00419 } 00420 } else { 00421 fairStates = mdd_dup(hull); 00422 } 00423 if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { 00424 fprintf(vis_stdout, 00425 "--Fair States: %d image computations, %d preimage computations\n", 00426 Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps, 00427 Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); 00428 } 00429 00430 /* Clean up. */ 00431 array_free(sccClosedSetArray); 00432 mdd_free(reached); 00433 mdd_free(hull); 00434 mdd_free(mddOne); 00435 array_free(careStatesArray); 00436 mdd_array_free(buechiFairness); 00437 return fairStates; 00438 00439 } /* McFsmComputeFairSCCsByLockStep */ 00440 00455 mdd_t * 00456 McFsmRefineFairSCCsByLockStep( 00457 Fsm_Fsm_t *fsm, 00458 int maxNumberOfSCCs, 00459 array_t *SCCs, 00460 array_t *sccClosedSets, 00461 array_t *careStates, 00462 array_t *onionRingsArrayForDbg, 00463 Mc_VerbosityLevel verbosity, 00464 Mc_DcLevel dcLevel) 00465 { 00466 Mc_SccGen_t *sccGen; 00467 mdd_t *mddOne, *reached, *hull, *scc, *fairStates; 00468 array_t *onionRings, *careStatesArray, *sccClosedSetArray; 00469 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 00470 int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); 00471 int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); 00472 Fsm_Fairness_t *modelFairness = Fsm_FsmReadFairnessConstraint(fsm); 00473 array_t *buechiFairness = array_alloc(mdd_t *, 0); 00474 00475 /* Initialization. */ 00476 mddOne = mdd_one(mddManager); 00477 00478 if (careStates == NIL(array_t)) { 00479 reached = Fsm_FsmComputeReachableStates(fsm, 0, verbosity, 0, 0, 1, 0, 0, 00480 Fsm_Rch_Default_c, 0, 0, 00481 NIL(array_t), FALSE, NIL(array_t)); 00482 careStatesArray = array_alloc(mdd_t *, 0); 00483 array_insert_last(mdd_t *, careStatesArray, mdd_dup(reached)); 00484 }else { 00485 reached = McMddArrayAnd(careStates); 00486 careStatesArray = mdd_array_duplicate(careStates); 00487 } 00488 00489 onionRings = Fsm_FsmReadReachabilityOnionRings(fsm); 00490 if (onionRings == NIL(array_t)) { 00491 onionRings = array_alloc(mdd_t *, 0); 00492 array_insert_last(mdd_t *, onionRings, mdd_dup(mddOne)); 00493 }else 00494 onionRings = mdd_array_duplicate(onionRings); 00495 00496 if (sccClosedSets == NIL(array_t)) { 00497 sccClosedSetArray = array_alloc(mdd_t *, 0); 00498 array_insert_last(mdd_t *, sccClosedSetArray, mdd_dup(reached)); 00499 }else { 00500 if (careStates != NIL(array_t)) 00501 sccClosedSetArray = mdd_array_duplicate(sccClosedSets); 00502 else { 00503 mdd_t *mdd1, *mdd2; 00504 int i; 00505 sccClosedSetArray = array_alloc(mdd_t *, 0); 00506 arrayForEachItem(mdd_t *, sccClosedSets, i, mdd1) { 00507 mdd2 = mdd_and(mdd1, reached, 1, 1); 00508 if (mdd_is_tautology(mdd2, 0)) 00509 mdd_free(mdd2); 00510 else 00511 array_insert_last(mdd_t *, sccClosedSetArray, mdd2); 00512 } 00513 } 00514 } 00515 00516 Img_MinimizeTransitionRelation(Fsm_FsmReadOrCreateImageInfo(fsm, 1, 1), 00517 careStatesArray, Img_DefaultMinimizeMethod_c, 00518 Img_Both_c, FALSE); 00519 00520 /* Read fairness constraints. */ 00521 if (modelFairness != NIL(Fsm_Fairness_t)) { 00522 if (!Fsm_FairnessTestIsBuchi(modelFairness)) { 00523 (void) fprintf(vis_stdout, 00524 "** mc error: non-Buechi fairness constraints not supported\n"); 00525 array_free(buechiFairness); 00526 mdd_array_free(sccClosedSetArray); 00527 mdd_array_free(onionRings); 00528 mdd_array_free(careStatesArray); 00529 mdd_free(reached); 00530 return NIL(mdd_t); 00531 } else { 00532 int j; 00533 int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0); 00534 for (j = 0; j < numBuchi; j++) { 00535 mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j, 00536 careStatesArray, 00537 dcLevel); 00538 array_insert_last(mdd_t *, buechiFairness, tmpMdd); 00539 } 00540 } 00541 } else { 00542 array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager)); 00543 } 00544 00545 /* Enumerate the fair SCCs and accumulate their disjunction in hull. */ 00546 hull = mdd_zero(mddManager); 00547 Mc_FsmForEachFairScc(fsm, sccGen, scc, sccClosedSetArray, NIL(array_t), 00548 buechiFairness, onionRings, 00549 maxNumberOfSCCs == MC_LOCKSTEP_EARLY_TERMINATION, 00550 verbosity, dcLevel) { 00551 mdd_t *tmp = mdd_or(hull, scc, 1, 1); 00552 mdd_free(hull); 00553 hull = tmp; 00554 array_insert_last(mdd_t *, SCCs, scc); 00555 if (maxNumberOfSCCs > MC_LOCKSTEP_ALL_SCCS && 00556 array_n(SCCs) == maxNumberOfSCCs) { 00557 Mc_FsmSccGenFree(sccGen, NIL(array_t)); 00558 break; 00559 } 00560 } 00561 00562 /* Compute (subset of) fair states and onion rings. */ 00563 if (onionRingsArrayForDbg != NIL(array_t)) { 00564 mdd_t *fairSet; 00565 int i; 00566 fairStates = Mc_FsmEvaluateEUFormula(fsm, reached, hull, 00567 NIL(mdd_t), mddOne, careStatesArray, 00568 MC_NO_EARLY_TERMINATION, 00569 NIL(array_t), Mc_None_c, NIL(array_t), 00570 verbosity, dcLevel, NIL(boolean)); 00571 arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) { 00572 mdd_t *restrictedFairSet = mdd_and(fairSet, hull, 1, 1); 00573 array_t *setOfRings = array_alloc(mdd_t *, 0); 00574 mdd_t *EU = Mc_FsmEvaluateEUFormula(fsm, fairStates, restrictedFairSet, 00575 NIL(mdd_t), mddOne, careStatesArray, 00576 MC_NO_EARLY_TERMINATION, 00577 NIL(array_t), Mc_None_c, setOfRings, 00578 verbosity, dcLevel, NIL(boolean)); 00579 array_insert_last(array_t *, onionRingsArrayForDbg, setOfRings); 00580 mdd_free(restrictedFairSet); 00581 mdd_free(EU); 00582 } 00583 } else { 00584 fairStates = mdd_dup(hull); 00585 } 00586 if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { 00587 fprintf(vis_stdout, 00588 "--Fair States: %d image computations, %d preimage computations\n", 00589 Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps, 00590 Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); 00591 } 00592 00593 /* Clean up. */ 00594 mdd_array_free(sccClosedSetArray); 00595 mdd_free(reached); 00596 mdd_free(hull); 00597 mdd_free(mddOne); 00598 mdd_array_free(careStatesArray); 00599 mdd_array_free(buechiFairness); 00600 return fairStates; 00601 00602 } /* McFsmRefineFairSCCsByLockStep */ 00603 00604 00641 mdd_t * 00642 McFsmComputeOneFairSccByLinearStep( 00643 Fsm_Fsm_t *fsm, 00644 Heap_t *priorityQueue, 00645 array_t *buechiFairness, 00646 array_t *onionRings, 00647 boolean earlyTermination, 00648 Mc_VerbosityLevel verbosity, 00649 Mc_DcLevel dcLevel, 00650 int *sccExamined) 00651 { 00652 mdd_t *mddOne, *SCC = NIL(mdd_t); 00653 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 00654 int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); 00655 int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); 00656 array_t *careStatesArray = array_alloc(mdd_t *, 0); 00657 int totalSCCs = 0; 00658 boolean foundScc = FALSE; 00659 array_t *activeFairness = NIL(array_t); 00660 int firstActive = 0; 00661 gns_t *gns; 00662 00663 /* Initialization. */ 00664 mddOne = mdd_one(mddManager); 00665 array_insert(mdd_t *, careStatesArray, 0, mddOne); 00666 00667 while (Heap_HeapCount(priorityQueue)) { 00668 mdd_t *V, *F, *fFront, *bFront, *fairSet; 00669 mdd_t *S, *NODE, *newS, *newNODE, *preNODE; 00670 long ringIndex; 00671 int retval UNUSED = Heap_HeapExtractMin(priorityQueue, &gns, 00672 &ringIndex); 00673 assert(retval && ringIndex < array_n(onionRings)); 00674 00675 /* Extract the SCC-closed set, together with its spine-set */ 00676 V = gns->states; 00677 S = gns->spine; 00678 NODE = gns->node; 00679 FREE(gns); 00680 00681 /* Determine the seed for which the SCC is computed */ 00682 if (mdd_is_tautology(S, 0) ) { 00683 assert( mdd_is_tautology(NODE, 0) ); 00684 mdd_free(NODE); 00685 NODE = LockstepPickSeed(fsm, V, buechiFairness, onionRings, ringIndex); 00686 } 00687 00688 if (earlyTermination == TRUE) { 00689 int i; 00690 activeFairness = array_alloc(mdd_t *, 0); 00691 for (i = 0; i < array_n(buechiFairness); i++) { 00692 mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i); 00693 if (!mdd_lequal(NODE, fairSet, 1, 1)) { 00694 array_insert_last(mdd_t *, activeFairness, fairSet); 00695 } 00696 } 00697 } 00698 00699 /* Compute the forward-set of seed, together with a new spine-set */ 00700 { 00701 array_t *newCareStatesArray = array_alloc(mdd_t *, 0); 00702 array_t *stack = array_alloc(mdd_t *, 0); 00703 mdd_t *tempMdd, *tempMdd2; 00704 int i; 00705 /* (1) Compute the forward-set, and push it onto STACK */ 00706 F = mdd_zero(mddManager); 00707 fFront = mdd_dup(NODE); 00708 while (!mdd_is_tautology(fFront, 0)) { 00709 array_insert_last(mdd_t *, stack, mdd_dup(fFront)); 00710 00711 tempMdd = F; 00712 F = mdd_or(F, fFront, 1, 1); 00713 mdd_free(tempMdd); 00714 00715 tempMdd = Mc_FsmEvaluateEYFormula(fsm, fFront, mddOne, careStatesArray, 00716 verbosity, dcLevel); 00717 mdd_free(fFront); 00718 tempMdd2 = mdd_and(tempMdd, V, 1, 1); 00719 mdd_free(tempMdd); 00720 fFront = mdd_and(tempMdd2, F, 1, 0); 00721 mdd_free(tempMdd2); 00722 } 00723 mdd_free(fFront); 00724 /* (2) Determine a spine-set of the forward-set */ 00725 i = array_n(stack) - 1; 00726 fFront = array_fetch(mdd_t *, stack, i); 00727 newNODE = Mc_ComputeAState(fFront, fsm); 00728 mdd_free(fFront); 00729 00730 newS = mdd_dup(newNODE); 00731 while (i > 0) { 00732 fFront = array_fetch(mdd_t *, stack, --i); 00733 /* Chao: The use of DCs here may slow down the computation, 00734 * even though it reduces the peak BDD size 00735 */ 00736 /* array_insert(mdd_t *, newCareStatesArray, 0, fFront); */ 00737 array_insert(mdd_t *, newCareStatesArray, 0, mddOne); 00738 tempMdd = Mc_FsmEvaluateEXFormula(fsm, newS, mddOne, newCareStatesArray, 00739 verbosity, dcLevel); 00740 tempMdd2 = mdd_and(tempMdd, fFront, 1, 1); 00741 mdd_free(tempMdd); 00742 mdd_free(fFront); 00743 00744 tempMdd = Mc_ComputeAState(tempMdd2, fsm); 00745 mdd_free(tempMdd2); 00746 00747 tempMdd2 = newS; 00748 newS = mdd_or(newS, tempMdd, 1, 1); 00749 mdd_free(tempMdd2); 00750 mdd_free(tempMdd); 00751 } 00752 array_free(stack); 00753 array_free(newCareStatesArray); 00754 } 00755 /* now, we have {F, newS, newNODE} */ 00756 00757 /* Determine the SCC containing NODE */ 00758 SCC = mdd_dup(NODE); 00759 bFront = mdd_dup(NODE); 00760 while (1) { 00761 mdd_t *tempMdd, *tempMdd2; 00762 00763 if (earlyTermination == TRUE) { 00764 mdd_t * meet = mdd_and(SCC, NODE, 1, 0); 00765 if (!mdd_is_tautology(meet, 0)) { 00766 assert(mdd_lequal(meet, V, 1, 1)); 00767 for ( ; firstActive < array_n(activeFairness); firstActive++) { 00768 mdd_t *fairSet = array_fetch(mdd_t *, activeFairness, firstActive); 00769 if (mdd_lequal(meet, fairSet, 1, 0)) break; 00770 } 00771 mdd_free(meet); 00772 if (firstActive == array_n(activeFairness)) { 00773 int i; 00774 (void) fprintf(vis_stdout, "EARLY TERMINATION!\n"); 00775 totalSCCs++; 00776 /* Trim fair sets to guarantee counterexample will go through 00777 * this SCC. 00778 */ 00779 for (i = 0; i < array_n(buechiFairness); i++) { 00780 mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i); 00781 mdd_t *trimmed = mdd_and(fairSet, SCC, 1, 1); 00782 mdd_free(fairSet); 00783 array_insert(mdd_t *, buechiFairness, i, trimmed); 00784 } 00785 mdd_free(bFront); 00786 mdd_free(F); 00787 mdd_free(V); 00788 mdd_free(S); 00789 mdd_free(NODE); 00790 mdd_free(newS); 00791 mdd_free(newNODE); 00792 array_free(activeFairness); 00793 00794 foundScc = TRUE; 00795 goto cleanUp; 00796 } 00797 } 00798 mdd_free(meet); 00799 } 00800 00801 tempMdd = Mc_FsmEvaluateEXFormula(fsm, bFront, mddOne, careStatesArray, 00802 verbosity, dcLevel); 00803 tempMdd2 = mdd_and(tempMdd, F, 1, 1); 00804 mdd_free(tempMdd); 00805 00806 tempMdd = bFront; 00807 bFront = mdd_and(tempMdd2, SCC, 1, 0); 00808 mdd_free(tempMdd2); 00809 mdd_free(tempMdd); 00810 if (mdd_is_tautology(bFront, 0)) break; 00811 00812 tempMdd = SCC; 00813 SCC = mdd_or(SCC, bFront, 1, 1); 00814 mdd_free(tempMdd); 00815 } 00816 mdd_free(bFront); 00817 00818 totalSCCs++; 00819 preNODE = Mc_FsmEvaluateEYFormula(fsm, NODE, mddOne, careStatesArray, 00820 verbosity, dcLevel); 00821 00822 /* Check for fairness. If SCC is a trival SCC, skip the check */ 00823 if ( !mdd_equal(SCC, NODE) || mdd_lequal(NODE, preNODE, 1, 1) ) { 00824 /* Check fairness constraints. */ 00825 int i; 00826 arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) { 00827 if (mdd_lequal(SCC, fairSet, 1, 0)) break; 00828 } 00829 if (i == array_n(buechiFairness)) { 00830 /* All fairness iconditions intersected. We have a fair SCC. */ 00831 if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { 00832 array_t *PSvars = Fsm_FsmReadPresentStateVars(fsm); 00833 fprintf(vis_stdout, "--linearSCC: found a fair SCC with %.0f states\n", 00834 mdd_count_onset(mddManager, SCC, PSvars)); 00835 /* (void) bdd_print_minterm(SCC); */ 00836 } 00837 foundScc = TRUE; 00838 } 00839 } 00840 mdd_free(preNODE); 00841 mdd_free(NODE); 00842 00843 /* Divide the remaining states of V into V minus 00844 * the forward set F, and the rest (minus the fair SCC). Add the two 00845 * sets thus obtained to the priority queue. */ 00846 { 00847 mdd_t *V1, *S1, *NODE1; 00848 mdd_t *tempMdd, *tempMdd2; 00849 00850 V1 = mdd_and(V, F, 1, 0); 00851 S1 = mdd_and(S, SCC, 1, 0); 00852 tempMdd = mdd_and(SCC, S, 1, 1); 00853 tempMdd2 = Mc_FsmEvaluateEXFormula(fsm, tempMdd, mddOne, 00854 careStatesArray, 00855 verbosity, dcLevel); 00856 mdd_free(tempMdd); 00857 NODE1 = mdd_and(tempMdd2, S1, 1, 1); 00858 mdd_free(tempMdd2); 00859 LinearstepQueueEnqueue(fsm, priorityQueue, V1, S1, NODE1, 00860 onionRings, McLS_G_c, 00861 buechiFairness, verbosity, dcLevel); 00862 00863 V1 = mdd_and(F, SCC, 1, 0); 00864 S1 = mdd_and(newS, SCC, 1, 0); 00865 NODE1 = mdd_and(newNODE, SCC, 1, 0); 00866 LinearstepQueueEnqueue(fsm, priorityQueue, V1, S1, NODE1, 00867 onionRings, McLS_H_c, 00868 buechiFairness, verbosity, dcLevel); 00869 } 00870 mdd_free(F); 00871 mdd_free(V); 00872 mdd_free(S); 00873 mdd_free(newS); 00874 mdd_free(newNODE); 00875 00876 if (foundScc == TRUE) break; 00877 mdd_free(SCC); 00878 } 00879 00880 cleanUp: 00881 mdd_free(mddOne); 00882 array_free(careStatesArray); 00883 if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { 00884 fprintf(vis_stdout, 00885 "--linearSCC: found %s fair SCC out of %d examined\n", 00886 foundScc ? "one" : "no", totalSCCs); 00887 fprintf(vis_stdout, 00888 "--linearSCC: %d image computations, %d preimage computations\n", 00889 Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps, 00890 Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); 00891 } 00892 *sccExamined += totalSCCs; 00893 return foundScc ? SCC : NIL(mdd_t); 00894 00895 } /* McFsmComputeOneFairSccByLinearStep */ 00896 00897 00933 mdd_t * 00934 McFsmComputeOneFairSccByLockStep( 00935 Fsm_Fsm_t *fsm, 00936 Heap_t *priorityQueue, 00937 array_t *buechiFairness, 00938 array_t *onionRings, 00939 boolean earlyTermination, 00940 Mc_VerbosityLevel verbosity, 00941 Mc_DcLevel dcLevel, 00942 int *sccExamined) 00943 { 00944 mdd_t *mddOne, *SCC = NIL(mdd_t); 00945 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 00946 int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); 00947 int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); 00948 array_t *careStatesArray = array_alloc(mdd_t *, 0); 00949 int totalSCCs = 0; 00950 boolean foundScc = FALSE; 00951 array_t *activeFairness = NIL(array_t); 00952 int firstActive = 0; 00953 00954 /* Initialization. */ 00955 mddOne = mdd_one(mddManager); 00956 array_insert(mdd_t *, careStatesArray, 0, mddOne); 00957 00958 while (Heap_HeapCount(priorityQueue)) { 00959 mdd_t *V, *seed, *B, *F, *fFront, *bFront, *fairSet; 00960 mdd_t *converged, *first, *second; 00961 long ringIndex; 00962 McLockstepMode firstMode, secondMode; 00963 int retval UNUSED = Heap_HeapExtractMin(priorityQueue, &V, &ringIndex); 00964 assert(retval && ringIndex < array_n(onionRings)); 00965 /* Here, V contains at least one nontrivial SCC. We then choose the 00966 * seed for a new SCC, which may turn out to be trivial. */ 00967 seed = LockstepPickSeed(fsm, V, buechiFairness, onionRings, ringIndex); 00968 00969 if (earlyTermination == TRUE) { 00970 int i; 00971 activeFairness = array_alloc(mdd_t *, 0); 00972 for (i = 0; i < array_n(buechiFairness); i++) { 00973 mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i); 00974 if (!mdd_lequal(seed, fairSet, 1, 1)) { 00975 array_insert_last(mdd_t *, activeFairness, fairSet); 00976 } 00977 } 00978 } 00979 00980 /* Do lockstep search from seed. Leave the seed initially out of 00981 * F and B to facilitate the detection of trivial SCCs. Intersect 00982 * all results with V so that we can simplify the transition 00983 * relation. */ 00984 fFront = Mc_FsmEvaluateEYFormula(fsm, seed, mddOne, careStatesArray, 00985 verbosity, dcLevel); 00986 F = mdd_and(fFront, V, 1, 1); 00987 mdd_free(fFront); 00988 fFront = mdd_dup(F); 00989 bFront = Mc_FsmEvaluateEXFormula(fsm, seed, mddOne, careStatesArray, 00990 verbosity, dcLevel); 00991 B = mdd_and(bFront, V , 1, 1); 00992 mdd_free(bFront); 00993 bFront = mdd_dup(B); 00994 /* Go until the fastest search converges. */ 00995 while (!(mdd_is_tautology(fFront, 0) || mdd_is_tautology(bFront, 0))) { 00996 mdd_t *tmp; 00997 00998 /* If the intersection of F and B intersects all fairness 00999 * constraints the union of F and B contains at least one fair 01000 * SCC. Since the intersection of F and B is monotonically 01001 * non-decreasing, once a fair set has been intersected, there 01002 * is no need to check for it any more. */ 01003 if (earlyTermination == TRUE) { 01004 mdd_t * meet = mdd_and(F, B, 1, 1); 01005 if (!mdd_is_tautology(meet, 0)) { 01006 assert(mdd_lequal(meet, V, 1, 1)); 01007 for ( ; firstActive < array_n(activeFairness); firstActive++) { 01008 mdd_t *fairSet = array_fetch(mdd_t *, activeFairness, firstActive); 01009 if (mdd_lequal(meet, fairSet, 1, 0)) break; 01010 } 01011 if (firstActive == array_n(activeFairness)) { 01012 int i; 01013 (void) fprintf(vis_stdout, "EARLY TERMINATION!\n"); 01014 totalSCCs++; 01015 /* A fair SCC is contained in the union of F, B, and seed. */ 01016 tmp = mdd_or(F, B, 1, 1); 01017 SCC = mdd_or(tmp, seed, 1, 1); 01018 mdd_free(tmp); 01019 /* Trim fair sets to guarantee counterexample will go through 01020 * this SCC. */ 01021 tmp = mdd_or(meet, seed, 1, 1); 01022 mdd_free(meet); 01023 meet = tmp; 01024 for (i = 0; i < array_n(buechiFairness); i++) { 01025 mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i); 01026 mdd_t *trimmed = mdd_and(fairSet, meet, 1, 1); 01027 mdd_free(fairSet); 01028 array_insert(mdd_t *, buechiFairness, i, trimmed); 01029 } 01030 mdd_free(meet); 01031 mdd_free(F); mdd_free(B); 01032 mdd_free(fFront); mdd_free(bFront); 01033 mdd_free(seed); mdd_free(V); 01034 foundScc = TRUE; 01035 array_free(activeFairness); 01036 goto cleanUp; 01037 } 01038 } 01039 mdd_free(meet); 01040 } 01041 01042 /* Forward step. */ 01043 tmp = Mc_FsmEvaluateEYFormula(fsm, fFront, mddOne, careStatesArray, 01044 verbosity, dcLevel); 01045 mdd_free(fFront); 01046 fFront = mdd_and(tmp, F, 1, 0); 01047 mdd_free(tmp); 01048 tmp = mdd_and(fFront, V, 1, 1); 01049 mdd_free(fFront); 01050 fFront = tmp; 01051 if (mdd_is_tautology(fFront, 0)) break; 01052 tmp = mdd_or(F, fFront, 1, 1); 01053 mdd_free(F); 01054 F = tmp; 01055 /* Backward step. */ 01056 tmp = Mc_FsmEvaluateEXFormula(fsm, bFront, mddOne, careStatesArray, 01057 verbosity, dcLevel); 01058 mdd_free(bFront); 01059 bFront = mdd_and(tmp, B, 1, 0); 01060 mdd_free(tmp); 01061 tmp = mdd_and(bFront, V, 1, 1); 01062 mdd_free(bFront); 01063 bFront = tmp; 01064 tmp = mdd_or(B, bFront, 1, 1); 01065 mdd_free(B); 01066 B = tmp; 01067 } 01068 /* Complete the slower search within the converged one. */ 01069 if (mdd_is_tautology(fFront, 0)) { 01070 /* Forward search converged. */ 01071 mdd_t *tmp = mdd_and(bFront, F, 1, 1); 01072 mdd_free(bFront); 01073 bFront = tmp; 01074 mdd_free(fFront); 01075 converged = mdd_dup(F); 01076 /* The two sets to be enqueued come from a set that has been 01077 * already trimmed. Hence, we want to remove the trivial SCCs 01078 * left exposed at the rearguard of F, and the trivial SCCs left 01079 * exposed at the vanguard of B. */ 01080 firstMode = McLS_H_c; 01081 secondMode = McLS_G_c; 01082 while (!mdd_is_tautology(bFront, 0)) { 01083 tmp = Mc_FsmEvaluateEXFormula(fsm, bFront, mddOne, 01084 careStatesArray, verbosity, dcLevel); 01085 mdd_free(bFront); 01086 bFront = mdd_and(tmp, B, 1, 0); 01087 mdd_free(tmp); 01088 tmp = mdd_and(bFront, converged, 1, 1); 01089 mdd_free(bFront); 01090 bFront = tmp; 01091 tmp = mdd_or(B, bFront, 1, 1); 01092 mdd_free(B); 01093 B = tmp; 01094 } 01095 mdd_free(bFront); 01096 } else { 01097 /* Backward search converged. */ 01098 mdd_t *tmp = mdd_and(fFront, B, 1, 1); 01099 mdd_free(fFront); 01100 fFront = tmp; 01101 mdd_free(bFront); 01102 converged = mdd_dup(B); 01103 firstMode = McLS_G_c; 01104 secondMode = McLS_H_c; 01105 while (!mdd_is_tautology(fFront, 0)) { 01106 tmp = Mc_FsmEvaluateEYFormula(fsm, fFront, mddOne, 01107 careStatesArray, verbosity, dcLevel); 01108 mdd_free(fFront); 01109 fFront = mdd_and(tmp, F, 1 ,0); 01110 mdd_free(tmp); 01111 tmp = mdd_and(fFront, converged, 1, 1); 01112 mdd_free(fFront); 01113 fFront = tmp; 01114 tmp = mdd_or(F, fFront, 1, 1); 01115 mdd_free(F); 01116 F = tmp; 01117 } 01118 mdd_free(fFront); 01119 } 01120 01121 totalSCCs++; 01122 SCC = mdd_and(F, B, 1, 1); 01123 mdd_free(F); 01124 mdd_free(B); 01125 /* Check for fairness. If SCC is the empty set we know that seed 01126 * is a trivial strong component; hence, it is not fair. */ 01127 if (mdd_is_tautology(SCC, 0)) { 01128 mdd_t *tmp = mdd_or(converged, seed, 1, 1); 01129 mdd_free(converged); 01130 converged = tmp; 01131 mdd_free(SCC); 01132 SCC = mdd_dup(seed); 01133 } else { 01134 /* Check fairness constraints. */ 01135 int i; 01136 arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) { 01137 if (mdd_lequal(SCC, fairSet, 1, 0)) break; 01138 } 01139 if (i == array_n(buechiFairness)) { 01140 /* All fairness conditions intersected. We have a fair SCC. */ 01141 if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { 01142 array_t *PSvars = Fsm_FsmReadPresentStateVars(fsm); 01143 fprintf(vis_stdout, "--SCC: found a fair SCC with %.0f states\n", 01144 mdd_count_onset(mddManager, SCC, PSvars)); 01145 /* (void) bdd_print_minterm(SCC); */ 01146 } 01147 foundScc = TRUE; 01148 } 01149 } 01150 /* Divide the remaining states of V into the converged set minus 01151 * the fair SCC, and the rest (minus the fair SCC). Add the two 01152 * sets thus obtained to the priority queue. */ 01153 mdd_free(seed); 01154 first = mdd_and(converged, SCC, 1, 0); 01155 LockstepQueueEnqueue(fsm, priorityQueue, first, onionRings, firstMode, 01156 buechiFairness, verbosity, dcLevel); 01157 second = mdd_and(V, converged, 1, 0); 01158 mdd_free(converged); 01159 mdd_free(V); 01160 LockstepQueueEnqueue(fsm, priorityQueue, second, onionRings, secondMode, 01161 buechiFairness, verbosity, dcLevel); 01162 if (earlyTermination == TRUE) { 01163 array_free(activeFairness); 01164 } 01165 if (foundScc == TRUE) break; 01166 mdd_free(SCC); 01167 } 01168 01169 cleanUp: 01170 mdd_free(mddOne); 01171 array_free(careStatesArray); 01172 if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { 01173 fprintf(vis_stdout, 01174 "--SCC: found %s fair SCC out of %d examined\n", 01175 foundScc ? "one" : "no", totalSCCs); 01176 fprintf(vis_stdout, 01177 "--SCC: %d image computations, %d preimage computations\n", 01178 Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps, 01179 Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); 01180 } 01181 *sccExamined += totalSCCs; 01182 return foundScc ? SCC : NIL(mdd_t); 01183 01184 } /* McFsmComputeOneFairSccByLockStep */ 01185 01186 01187 /*---------------------------------------------------------------------------*/ 01188 /* Definition of internal functions */ 01189 /*---------------------------------------------------------------------------*/ 01190 01191 01192 /*---------------------------------------------------------------------------*/ 01193 /* Definition of static functions */ 01194 /*---------------------------------------------------------------------------*/ 01195 01196 01213 static mdd_t * 01214 LockstepPickSeed( 01215 Fsm_Fsm_t *fsm, 01216 mdd_t *V, 01217 array_t *buechiFairness, 01218 array_t *onionRings, 01219 int ringIndex) 01220 { 01221 mdd_t *seed; 01222 int i, j; 01223 01224 /* We know that there is at least one state in V from each fairness 01225 * constraint. */ 01226 for (i = ringIndex; i < array_n(onionRings); i++) { 01227 mdd_t *ring = array_fetch(mdd_t *, onionRings, i); 01228 for (j = 0; j < array_n(buechiFairness); j++) { 01229 mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, j); 01230 if (!mdd_lequal_mod_care_set(ring, fairSet, 1, 0, V)) { 01231 mdd_t *tmp = mdd_and(V, ring, 1, 1); 01232 mdd_t *candidates = mdd_and(tmp, fairSet, 1, 1); 01233 mdd_free(tmp); 01234 for (j++; j < array_n(buechiFairness); j++) { 01235 fairSet = array_fetch(mdd_t *, buechiFairness, j); 01236 if (!mdd_lequal(candidates, fairSet, 1, 0)) { 01237 tmp = mdd_and(candidates, fairSet, 1, 1); 01238 mdd_free(candidates); 01239 candidates = tmp; 01240 } 01241 } 01242 seed = Mc_ComputeAState(candidates, fsm); 01243 mdd_free(candidates); 01244 return seed; 01245 } 01246 } 01247 } 01248 01249 assert(FALSE); /* we should never get here */ 01250 return NIL(bdd_t); 01251 01252 } /* LockstepPickSeed */ 01253 01254 01270 static void 01271 LockstepQueueEnqueue( 01272 Fsm_Fsm_t *fsm, 01273 Heap_t *queue, 01274 mdd_t *states, 01275 array_t *onionRings, 01276 McLockstepMode mode, 01277 array_t *buechiFairness, 01278 Mc_VerbosityLevel verbosity, 01279 Mc_DcLevel dcLevel) 01280 { 01281 mdd_t *fairSet, *ring; 01282 int i; 01283 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 01284 mdd_t *mddOne = mdd_one(mddManager); 01285 array_t *careStatesArray = array_alloc(mdd_t *, 0); 01286 array_insert_last(mdd_t *, careStatesArray, mddOne); 01287 01288 #ifndef SCC_NO_TRIM 01289 if (mode == McLS_G_c || mode == McLS_GH_c) { 01290 mdd_t *trimmed = Mc_FsmEvaluateEGFormula(fsm, states, NIL(mdd_t), mddOne, 01291 NIL(Fsm_Fairness_t), 01292 careStatesArray, 01293 MC_NO_EARLY_TERMINATION, 01294 NIL(array_t), 01295 Mc_None_c, NIL(array_t *), 01296 verbosity, dcLevel, NIL(boolean), 01297 McGSH_EL_c); 01298 mdd_free(states); 01299 states = trimmed; 01300 } 01301 if (mode == McLS_H_c || mode == McLS_GH_c) { 01302 mdd_t *trimmed = Mc_FsmEvaluateEHFormula(fsm, states, NIL(mdd_t), mddOne, 01303 NIL(Fsm_Fairness_t), 01304 careStatesArray, 01305 MC_NO_EARLY_TERMINATION, 01306 NIL(array_t), 01307 Mc_None_c, NIL(array_t *), 01308 verbosity, dcLevel, NIL(boolean), 01309 McGSH_EL_c); 01310 mdd_free(states); 01311 states = trimmed; 01312 } 01313 #endif 01314 01315 mdd_free(mddOne); 01316 array_free(careStatesArray); 01317 if (mode == McLS_none_c) { 01318 mdd_t *range = mdd_range_mdd(mddManager, Fsm_FsmReadPresentStateVars(fsm)); 01319 mdd_t *valid = mdd_and(states, range, 1, 1); 01320 mdd_free(range); 01321 mdd_free(states); 01322 states = valid; 01323 } 01324 /* Discard set of states if it does not intersect all fairness conditions. */ 01325 arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) { 01326 if (mdd_lequal(states, fairSet, 1, 0)) { 01327 mdd_free(states); 01328 return; 01329 } 01330 } 01331 /* Find the innermost onion ring intersecting the set of states. 01332 * Its index is the priority of the set. */ 01333 arrayForEachItem(mdd_t *, onionRings, i, ring) { 01334 if (!mdd_lequal(states, ring, 1, 0)) break; 01335 } 01336 assert(i < array_n(onionRings)); 01337 Heap_HeapInsert(queue,states,i); 01338 return; 01339 01340 } /* LockstepQueueEnqueue */ 01341 01342 01358 static void 01359 LinearstepQueueEnqueue( 01360 Fsm_Fsm_t *fsm, 01361 Heap_t *queue, 01362 mdd_t *states, 01363 mdd_t *spine, 01364 mdd_t *node, 01365 array_t *onionRings, 01366 McLockstepMode mode, 01367 array_t *buechiFairness, 01368 Mc_VerbosityLevel verbosity, 01369 Mc_DcLevel dcLevel) 01370 { 01371 mdd_t *fairSet, *ring; 01372 mdd_t *tmp, *tmp1; 01373 int i; 01374 gns_t *gns; 01375 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 01376 mdd_t *mddOne = mdd_one(mddManager); 01377 array_t *careStatesArray = array_alloc(mdd_t *, 0); 01378 array_insert_last(mdd_t *, careStatesArray, mddOne); 01379 01380 #ifndef SCC_NO_TRIM 01381 if (mode == McLS_G_c || mode == McLS_GH_c) { 01382 mdd_t *trimmed = Mc_FsmEvaluateEGFormula(fsm, states, NIL(mdd_t), mddOne, 01383 NIL(Fsm_Fairness_t), 01384 careStatesArray, 01385 MC_NO_EARLY_TERMINATION, 01386 NIL(array_t), 01387 Mc_None_c, NIL(array_t *), 01388 verbosity, dcLevel, NIL(boolean), 01389 McGSH_EL_c); 01390 mdd_free(states); 01391 states = trimmed; 01392 } 01393 if (mode == McLS_H_c || mode == McLS_GH_c) { 01394 mdd_t *trimmed = Mc_FsmEvaluateEHFormula(fsm, states, NIL(mdd_t), mddOne, 01395 NIL(Fsm_Fairness_t), 01396 careStatesArray, 01397 MC_NO_EARLY_TERMINATION, 01398 NIL(array_t), 01399 Mc_None_c, NIL(array_t *), 01400 verbosity, dcLevel, NIL(boolean), 01401 McGSH_EL_c); 01402 mdd_free(states); 01403 states = trimmed; 01404 } 01405 #endif 01406 01407 if (mode == McLS_none_c) { 01408 mdd_t *range = mdd_range_mdd(mddManager, Fsm_FsmReadPresentStateVars(fsm)); 01409 mdd_t *valid = mdd_and(states, range, 1, 1); 01410 mdd_free(range); 01411 mdd_free(states); 01412 states = valid; 01413 } 01414 /* Discard set of states if it does not intersect all fairness conditions. */ 01415 arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) { 01416 if (mdd_lequal(states, fairSet, 1, 0)) { 01417 mdd_free(states); 01418 mdd_free(mddOne); 01419 array_free(careStatesArray); 01420 return; 01421 } 01422 } 01423 /* Find the innermost onion ring intersecting the set of states. 01424 * Its index is the priority of the set. */ 01425 arrayForEachItem(mdd_t *, onionRings, i, ring) { 01426 if (!mdd_lequal(states, ring, 1, 0)) break; 01427 } 01428 assert(i < array_n(onionRings)); 01429 01430 /* Trim the spine-set. */ 01431 while ( !mdd_lequal(node, states, 1, 1) ) { 01432 tmp = node; 01433 tmp1 = Mc_FsmEvaluateEXFormula(fsm, node, mddOne, 01434 careStatesArray, verbosity, dcLevel); 01435 mdd_free(tmp); 01436 node = mdd_and(tmp1, spine, 1, 1); 01437 mdd_free(tmp1); 01438 } 01439 01440 tmp = spine; 01441 spine = mdd_and(spine, states, 1, 1); 01442 mdd_free(tmp); 01443 01444 #if 0 01445 /* Invariants that should always hold */ 01446 assert( mdd_is_tautology(node, 0) == mdd_is_tautology(spine, 0) ); 01447 assert(mdd_lequal(node, states, 1, 1)); 01448 assert(mdd_lequal(node, spine, 1, 1)); 01449 assert(mdd_lequal(spine, states, 1, 1)); 01450 #endif 01451 01452 mdd_free(mddOne); 01453 array_free(careStatesArray); 01454 01455 gns = ALLOC(gns_t, 1); 01456 gns->states = states; 01457 gns->node = node; 01458 gns->spine = spine; 01459 01460 01461 Heap_HeapInsert(queue,gns,i); 01462 return; 01463 01464 } /* LinearstepQueueEnqueue */ 01465 01466 01480 static int 01481 GetSccEnumerationMethod( void ) 01482 { 01483 char *flagValue; 01484 int linearStepMethod = 0; 01485 01486 flagValue = Cmd_FlagReadByName("scc_method"); 01487 if (flagValue != NIL(char)) { 01488 if (strcmp(flagValue, "linearstep") == 0) 01489 linearStepMethod = 1; 01490 else if (strcmp(flagValue, "lockstep") == 0) 01491 linearStepMethod = 0; 01492 else { 01493 fprintf(vis_stderr, "** scc error: invalid scc method %s, method lockstep is used. \n", 01494 flagValue); 01495 } 01496 } 01497 01498 return linearStepMethod; 01499 }
1.7.3