- Generated on Wed Oct 12 2011 00:34:50 for VIS by
1.7.3
|
VIS
|
00001 00080 #include "ctlpInt.h" 00081 #include "mcInt.h" 00082 00083 00084 /*---------------------------------------------------------------------------*/ 00085 /* Constant declarations */ 00086 /*---------------------------------------------------------------------------*/ 00087 00088 /*---------------------------------------------------------------------------*/ 00089 /* Stucture declarations */ 00090 /*---------------------------------------------------------------------------*/ 00091 00092 /*---------------------------------------------------------------------------*/ 00093 /* Type declarations */ 00094 /*---------------------------------------------------------------------------*/ 00095 00096 /*---------------------------------------------------------------------------*/ 00097 /* Variable declarations */ 00098 /*---------------------------------------------------------------------------*/ 00099 00100 #ifndef lint 00101 static char rcsid[] UNUSED = "$Id: mcVacuum.c,v 1.1 2005/05/13 05:54:05 fabio Exp $"; 00102 #endif 00103 00104 /*---------------------------------------------------------------------------*/ 00105 /* Macro declarations */ 00106 /*---------------------------------------------------------------------------*/ 00107 00110 /*---------------------------------------------------------------------------*/ 00111 /* Static function prototypes */ 00112 /*---------------------------------------------------------------------------*/ 00113 00114 static void EvaluateFormulaThoroughVacuity(Fsm_Fsm_t *fsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRing, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates); 00115 static void EvaluateFormulaWactlVacuity(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, mdd_t *modelInitialStates, McOptions_t *options); 00116 static void PrintVacuousBottom(mdd_t *modelInitialStates, Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, Mc_FwdBwdAnalysis traversalDirection, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity); 00117 static void PrintVacuous(mdd_t *modelInitialStates, Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, Mc_FwdBwdAnalysis traversalDirection, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity); 00118 static void ModelcheckAndVacuity(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Ctlp_Approx_t TRMinimization, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates); 00119 static void CreateImportantWitness(Ctlp_Formula_t *OldctlFormula, Ctlp_Formula_t *ctlFormula, int i); 00120 static void CreateImportantCounterexample(Ctlp_Formula_t *OldctlFormula, Ctlp_Formula_t *ctlFormula, int i); 00121 static array_t * McMddArrayArrayDup(array_t *arrayBddArray); 00122 static void match_top(Ctlp_Formula_t *ctlFormula, array_t *mddArray, array_t *matchfound, array_t *matchelement); 00123 static void match_bot(Ctlp_Formula_t *ctlFormula, array_t *mddArray, array_t *matchfound, array_t *matchelement); 00124 static array_t * GenerateOnionRings(array_t* TempOnionRings, array_t* onionRings); 00125 static void FormulaFreeDebugDataVac(Ctlp_Formula_t *formula); 00126 00129 /*---------------------------------------------------------------------------*/ 00130 /* Definition of exported functions */ 00131 /*---------------------------------------------------------------------------*/ 00132 00133 00134 /*---------------------------------------------------------------------------*/ 00135 /* Definition of internal functions */ 00136 /*---------------------------------------------------------------------------*/ 00137 00151 void 00152 McVacuityDetection( 00153 Fsm_Fsm_t *modelFsm, 00154 Ctlp_Formula_t *ctlFormula, 00155 int i, 00156 mdd_t *fairStates, 00157 Fsm_Fairness_t *fairCond, 00158 array_t *modelCareStatesArray, 00159 Mc_EarlyTermination_t *earlyTermination, 00160 array_t *hintsStatesArray, 00161 Mc_GuidedSearch_t guidedSearchType, 00162 mdd_t *modelInitialStates, 00163 McOptions_t *options) 00164 { 00165 00166 if (McOptionsReadBeerMethod(options)) { 00167 EvaluateFormulaWactlVacuity(modelFsm, ctlFormula, i, fairStates, fairCond, 00168 modelCareStatesArray, earlyTermination, 00169 hintsStatesArray, guidedSearchType, 00170 modelInitialStates, options); 00171 } 00172 else { 00173 mdd_t *ctlFormulaStates; 00174 boolean result; 00175 Mc_VerbosityLevel verbosity = McOptionsReadVerbosityLevel(options); 00176 Mc_DcLevel dcLevel = McOptionsReadDcLevel(options); 00177 Mc_GSHScheduleType GSHschedule = McOptionsReadSchedule(options); 00178 int buildOnionRings = 00179 (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity); 00180 Mc_FwdBwdAnalysis traversalDirection = 00181 McOptionsReadTraversalDirection(options); 00182 mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); 00183 00184 Ctlp_FormulaNegations(ctlFormula,Ctlp_Even_c); 00185 EvaluateFormulaThoroughVacuity(modelFsm, ctlFormula, fairStates, 00186 fairCond, modelCareStatesArray, 00187 earlyTermination, hintsStatesArray, 00188 guidedSearchType, verbosity, dcLevel, 00189 buildOnionRings, GSHschedule, 00190 modelInitialStates); 00191 Mc_EarlyTerminationFree(earlyTermination); 00192 if(hintsStatesArray != NIL(array_t)) 00193 mdd_array_free(hintsStatesArray); 00194 ctlFormulaStates = array_fetch(mdd_t *,ctlFormula->Bottomstates,0); 00195 /* user feedback on succes/fail */ 00196 result = McPrintPassFail(mddMgr, modelFsm, traversalDirection, 00197 ctlFormula, ctlFormulaStates, 00198 modelInitialStates, modelCareStatesArray, 00199 options, verbosity); 00200 if (result == TRUE) { 00201 PrintVacuous(modelInitialStates,modelFsm,ctlFormula, 00202 traversalDirection,modelCareStatesArray, 00203 options, verbosity); 00204 } 00205 else { 00206 PrintVacuousBottom(modelInitialStates,modelFsm,ctlFormula, 00207 traversalDirection,modelCareStatesArray, 00208 options, verbosity); 00209 } 00210 FormulaFreeDebugDataVac(ctlFormula); 00211 } 00212 00213 } /* McVacuityDetection */ 00214 00215 00216 /*---------------------------------------------------------------------------*/ 00217 /* Definition of static functions */ 00218 /*---------------------------------------------------------------------------*/ 00219 00220 00236 static void 00237 EvaluateFormulaThoroughVacuity( 00238 Fsm_Fsm_t *fsm, 00239 Ctlp_Formula_t *ctlFormula, 00240 mdd_t *fairStates, 00241 Fsm_Fairness_t *fairCondition, 00242 array_t *careStatesArray, 00243 Mc_EarlyTermination_t *earlyTermination, 00244 Fsm_HintsArray_t *hintsArray, 00245 Mc_GuidedSearch_t hintType, 00246 Mc_VerbosityLevel verbosity, 00247 Mc_DcLevel dcLevel, 00248 int buildOnionRing, 00249 Mc_GSHScheduleType GSHschedule, 00250 mdd_t *modelInitialStates) 00251 { 00252 mdd_t *hint; /* to iterate over hintsArray */ 00253 int hintnr; /* idem */ 00254 assert(hintType == Mc_None_c || hintsArray != NIL(Fsm_HintsArray_t)); 00255 00256 if(hintType != Mc_Global_c) { 00257 ModelcheckAndVacuity(fsm, ctlFormula, fairStates, 00258 fairCondition, careStatesArray, 00259 earlyTermination, hintsArray, hintType, 00260 Ctlp_Exact_c, verbosity, dcLevel, 00261 buildOnionRing, GSHschedule, 00262 modelInitialStates); 00263 return; 00264 } 00265 else{ 00266 array_t *result = NIL(array_t); 00267 Ctlp_Approx_t approx; 00268 00269 if(verbosity >= McVerbosityMax_c) 00270 fprintf(vis_stdout, "--Using global hints\n"); 00271 00272 arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){ 00273 if(result != NIL(array_t)) 00274 array_free(result); 00275 00276 if(verbosity >= McVerbosityMax_c) 00277 fprintf(vis_stdout, "--Instantiating global hint %d\n", hintnr); 00278 00279 Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c, 00280 (verbosity >= McVerbosityMax_c)); 00281 00282 approx = mdd_is_tautology(hint, 1) ? Ctlp_Exact_c : Ctlp_Underapprox_c; 00283 00284 ModelcheckAndVacuity(fsm,ctlFormula, fairStates, 00285 fairCondition, careStatesArray, 00286 earlyTermination, hintsArray, hintType, 00287 approx, verbosity, 00288 dcLevel, buildOnionRing,GSHschedule, 00289 modelInitialStates); 00290 /* TBD: take into account (early) termination here */ 00291 } 00292 Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c)); 00293 00294 return; 00295 } 00296 } /* EvaluateFormulaThoroughVacuity */ 00297 00298 00318 static void 00319 EvaluateFormulaWactlVacuity( 00320 Fsm_Fsm_t *modelFsm, 00321 Ctlp_Formula_t *ctlFormula, 00322 int i, 00323 mdd_t *fairStates, 00324 Fsm_Fairness_t *fairCond, 00325 array_t *modelCareStatesArray, 00326 Mc_EarlyTermination_t *earlyTermination, 00327 array_t *hintsStatesArray, 00328 Mc_GuidedSearch_t guidedSearchType, 00329 mdd_t *modelInitialStates, 00330 McOptions_t *options) 00331 { 00332 mdd_t *ctlFormulaStates; 00333 boolean result1, result2; 00334 Mc_VerbosityLevel verbosity = McOptionsReadVerbosityLevel(options); 00335 Mc_DcLevel dcLevel = McOptionsReadDcLevel(options); 00336 Mc_GSHScheduleType GSHschedule = McOptionsReadSchedule(options); 00337 int buildOnionRings = 00338 (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity); 00339 Mc_FwdBwdAnalysis traversalDirection = 00340 McOptionsReadTraversalDirection(options); 00341 mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); 00342 00343 ctlFormulaStates = 00344 Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates, 00345 fairCond, modelCareStatesArray, 00346 earlyTermination, hintsStatesArray, 00347 guidedSearchType, verbosity, dcLevel, 00348 buildOnionRings,GSHschedule); 00349 00350 Mc_EarlyTerminationFree(earlyTermination); 00351 if(hintsStatesArray != NIL(array_t)) 00352 mdd_array_free(hintsStatesArray); 00353 result1 = McPrintPassFail(mddMgr, modelFsm, traversalDirection, 00354 ctlFormula, ctlFormulaStates, 00355 modelInitialStates, modelCareStatesArray, 00356 options, verbosity); 00357 mdd_free(ctlFormulaStates); 00358 00359 if (result1 == FALSE) 00360 fprintf(vis_stdout, 00361 "# MC: Original formula failed. Aborting vacuity detection\n"); 00362 else { 00363 /* see if we can create a witness formula */ 00364 if ((Ctlp_CheckClassOfExistentialFormula(ctlFormula) != Ctlp_ACTL_c) && 00365 (Ctlp_CheckClassOfExistentialFormula(ctlFormula) != Ctlp_QuantifierFree_c)) { 00366 fprintf(vis_stdout, 00367 "# MC: Not an ACTL Formula. Aborting vacuity detection\n"); 00368 } 00369 else { 00370 if (Ctlp_CheckIfWACTL(Ctlp_FormulaReadOriginalFormula(ctlFormula)) == Ctlp_NONWACTL_c) { 00371 fprintf(vis_stdout, "# MC: Not a w-ACTL Formula. Aborting vacuity detection\n"); 00372 } 00373 else { 00374 Ctlp_Formula_t *origFormula, *witFormula; 00375 /* We can create a witness formula. Annotate the original 00376 * formula with negation parity info and then create a copy 00377 * with the smallest important formula replaced by bottom. */ 00378 fprintf(vis_stdout, "Model checking the witness formula\n"); 00379 origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula); 00380 Ctlp_FormulaNegations(origFormula, Ctlp_Even_c); 00381 witFormula = Ctlp_FormulaCreateWitnessFormula(origFormula); 00382 ctlFormula = Ctlp_FormulaConvertToExistentialForm(witFormula); 00383 00384 /* some user feedback */ 00385 if (verbosity != McVerbosityNone_c) { 00386 (void)fprintf(vis_stdout, "Checking witness formula[%d] : ", i + 1); 00387 Ctlp_FormulaPrint(vis_stdout, 00388 Ctlp_FormulaReadOriginalFormula(ctlFormula)); 00389 (void)fprintf (vis_stdout, "\n"); 00390 assert(traversalDirection != McFwd_c); 00391 } 00392 /************** the actual computation *************************/ 00393 earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates); 00394 ctlFormulaStates = 00395 Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates, 00396 fairCond, modelCareStatesArray, 00397 earlyTermination, hintsStatesArray, 00398 guidedSearchType, verbosity, dcLevel, 00399 buildOnionRings,GSHschedule); 00400 00401 Mc_EarlyTerminationFree(earlyTermination); 00402 if(hintsStatesArray != NIL(array_t)) 00403 mdd_array_free(hintsStatesArray); 00404 /* user feedback on succes/fail */ 00405 result2 = McPrintPassFail(mddMgr, modelFsm, traversalDirection, 00406 ctlFormula, ctlFormulaStates, 00407 modelInitialStates, 00408 modelCareStatesArray, 00409 options, verbosity); 00410 if (result2) 00411 (void)fprintf(vis_stdout, "# MC: Vacuous pass\n"); 00412 else 00413 (void)fprintf(vis_stdout, "# MC: Not a vacuous pass\n"); 00414 mdd_free(ctlFormulaStates); 00415 Ctlp_FormulaFree(ctlFormula); 00416 Ctlp_FormulaFree(witFormula); 00417 } 00418 } 00419 } 00420 00421 } /* EvaluateFormulaWactlVacuity */ 00422 00423 00437 static void 00438 PrintVacuousBottom( 00439 mdd_t *modelInitialStates, 00440 Fsm_Fsm_t *modelFsm, 00441 Ctlp_Formula_t *ctlFormula, 00442 Mc_FwdBwdAnalysis traversalDirection, 00443 array_t *modelCareStatesArray, 00444 McOptions_t *options, 00445 Mc_VerbosityLevel verbosity) 00446 { 00447 Ctlp_Formula_t *formula,*Int_Counter_CtlFormula; 00448 boolean vacuous = FALSE; 00449 int i; 00450 Ctlp_FormulaType type; 00451 if (traversalDirection == McBwd_c){ 00452 for (i=1;i<array_n(ctlFormula->Topstates);i++){ 00453 if (!(mdd_lequal(modelInitialStates, array_fetch(mdd_t *,ctlFormula->Topstates,i),1,1))){ 00454 formula = array_fetch(Ctlp_Formula_t *,ctlFormula->leaves,(i-1)); 00455 type = Ctlp_FormulaReadType(formula); 00456 if((type != Ctlp_FALSE_c) && (type != Ctlp_TRUE_c)) { 00457 fprintf(vis_stdout, "# MC: Vacuous failure : "); 00458 Ctlp_FormulaPrint(vis_stdout, formula); 00459 fprintf(vis_stdout, "\n"); 00460 if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c){ 00461 fprintf(vis_stdout, "# Generating interesting counterexample :\n"); 00462 Int_Counter_CtlFormula = Ctlp_FormulaDup(ctlFormula); 00463 CreateImportantCounterexample(ctlFormula,Int_Counter_CtlFormula,i); 00464 McFsmDebugFormula(options,Int_Counter_CtlFormula,modelFsm, 00465 modelCareStatesArray); 00466 Ctlp_FormulaFree(Int_Counter_CtlFormula); 00467 } 00468 vacuous = TRUE; 00469 } 00470 } 00471 } 00472 if (vacuous == FALSE){ 00473 (void)fprintf(vis_stdout, "# MC: No vacuous failures\n"); 00474 } 00475 } 00476 else{ 00477 (void)fprintf(vis_stderr, "# MC: Vacuity can not be checked\n"); 00478 } 00479 } /* PrintVacuousBottom */ 00480 00481 00497 static void 00498 PrintVacuous( 00499 mdd_t *modelInitialStates, 00500 Fsm_Fsm_t *modelFsm, 00501 Ctlp_Formula_t *ctlFormula, 00502 Mc_FwdBwdAnalysis traversalDirection, 00503 array_t *modelCareStatesArray, 00504 McOptions_t *options, 00505 Mc_VerbosityLevel verbosity) 00506 { 00507 Ctlp_Formula_t *formula,*Int_Wit_CtlFormula; 00508 boolean vacuous = FALSE; 00509 int i; 00510 Ctlp_FormulaType type; 00511 if (traversalDirection == McBwd_c) { 00512 for (i=1;i<array_n(ctlFormula->Bottomstates);i++) { 00513 formula = array_fetch(Ctlp_Formula_t *,ctlFormula->leaves,(i-1)); 00514 type = Ctlp_FormulaReadType(formula); 00515 if (mdd_lequal(modelInitialStates, array_fetch(mdd_t *,ctlFormula->Bottomstates,i),1,1)) { 00516 if((type != Ctlp_FALSE_c) && (type != Ctlp_TRUE_c)) { 00517 fprintf(vis_stdout, "# MC: Vacuous pass : "); 00518 Ctlp_FormulaPrint(vis_stdout, formula); 00519 fprintf(vis_stdout, "\n"); 00520 vacuous = TRUE; 00521 } 00522 } 00523 else { /* CounterExample Generation */ 00524 if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c){ 00525 fprintf(vis_stdout, "# MC: Not a vacuous pass : "); 00526 Ctlp_FormulaPrint(vis_stdout, formula); 00527 fprintf(vis_stdout, "\n"); 00528 fprintf(vis_stdout, "# Generating interesting witness :\n"); 00529 Int_Wit_CtlFormula = Ctlp_FormulaDup(ctlFormula); 00530 CreateImportantWitness(ctlFormula,Int_Wit_CtlFormula,i); 00531 McFsmDebugFormula(options,Int_Wit_CtlFormula,modelFsm, 00532 modelCareStatesArray); 00533 Ctlp_FormulaFree(Int_Wit_CtlFormula); 00534 } 00535 } 00536 } 00537 if (vacuous == FALSE){ 00538 (void)fprintf(vis_stdout, "# MC: No vacuous passes\n"); 00539 } 00540 } 00541 else{ 00542 (void)fprintf(vis_stderr, "# MC: Vacuity cannot be checked\n"); 00543 } 00544 } /* PrintVacuous */ 00545 00546 00563 static void 00564 ModelcheckAndVacuity( 00565 Fsm_Fsm_t *modelFsm, 00566 Ctlp_Formula_t *ctlFormula, 00567 mdd_t *fairStates, 00568 Fsm_Fairness_t *fairCondition, 00569 array_t *modelCareStatesArray, 00570 Mc_EarlyTermination_t *earlyTermination, 00571 Fsm_HintsArray_t *hintsArray, 00572 Mc_GuidedSearch_t hintType, 00573 Ctlp_Approx_t TRMinimization, 00574 Mc_VerbosityLevel verbosity, 00575 Mc_DcLevel dcLevel, 00576 int buildOnionRings, 00577 Mc_GSHScheduleType GSHschedule, 00578 mdd_t *modelInitialStates) 00579 { 00580 mdd_t *result = NIL(mdd_t); 00581 mdd_t *result_new = NIL(mdd_t); 00582 mdd_t *result_bot = NIL(mdd_t); 00583 mdd_t *result_top = NIL(mdd_t); 00584 mdd_t *result_underapprox = NIL(mdd_t); 00585 mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); 00586 array_t *careStatesArray = NIL(array_t); 00587 array_t *mddArray_bot = NIL(array_t); 00588 array_t *mddArray_top = NIL(array_t); 00589 array_t *leavesArray = NIL(array_t); 00590 array_t *leavesLeftArray = NIL(array_t); 00591 array_t *leavesRightArray = NIL(array_t); 00592 array_t *matchfound_bot = NIL(array_t); 00593 array_t *matchfound_top = NIL(array_t); 00594 array_t *matchelement_bot = NIL(array_t); 00595 array_t *matchelement_top = NIL(array_t); 00596 mdd_t *tmpMdd; 00597 mdd_t *approx = NIL(mdd_t); /* prev computed approx of sat set */ 00598 /* mdd_t *ctlFormulaStates = Ctlp_FormulaObtainStates( ctlFormula ); */ 00599 Ctlp_Formula_t *leftChild,*rightChild ; 00600 mdd_t *leftMdd = NIL(mdd_t); 00601 mdd_t *rightMdd = NIL(mdd_t); 00602 Ctlp_Approx_t leftApproxType = Ctlp_Exact_c; 00603 Ctlp_Approx_t rightApproxType = Ctlp_Exact_c; 00604 Ctlp_Approx_t thisApproxType = Ctlp_Exact_c; 00605 boolean fixpoint = FALSE; 00606 /* boolean approx_decide = FALSE; */ 00607 /* We will propagate early termination ONLY to the outmost fixpoint, 00608 and only propagate through negation. We should also propagate 00609 over other boolean operators, and maybe temporal operators. 00610 Propagation over negation is done by complementing the type. */ 00611 rightChild = Ctlp_FormulaReadRightChild(ctlFormula); 00612 leftChild = Ctlp_FormulaReadLeftChild(ctlFormula); 00613 00614 if (leftChild) { 00615 if ((leftChild->share) == 1){ 00616 Mc_EarlyTermination_t *nextEarlyTermination = 00617 McObtainUpdatedEarlyTerminationCondition( 00618 earlyTermination, NIL(mdd_t), Ctlp_FormulaReadType(ctlFormula)); 00619 00620 ModelcheckAndVacuity(modelFsm, leftChild,fairStates, 00621 fairCondition, modelCareStatesArray, 00622 nextEarlyTermination, 00623 hintsArray, hintType, 00624 TRMinimization, verbosity,dcLevel, 00625 buildOnionRings, GSHschedule, 00626 modelInitialStates); 00627 Mc_EarlyTerminationFree(nextEarlyTermination); 00628 } 00629 } 00630 00631 if (rightChild) { 00632 if((rightChild->share) == 1) { 00633 Mc_EarlyTermination_t *nextEarlyTermination = 00634 McObtainUpdatedEarlyTerminationCondition( 00635 earlyTermination,NIL(mdd_t) ,Ctlp_FormulaReadType(ctlFormula)); 00636 ModelcheckAndVacuity(modelFsm, rightChild, fairStates, 00637 fairCondition, 00638 modelCareStatesArray, 00639 nextEarlyTermination, 00640 hintsArray, hintType, 00641 TRMinimization, verbosity, dcLevel, 00642 buildOnionRings, GSHschedule, 00643 modelInitialStates); 00644 Mc_EarlyTerminationFree(nextEarlyTermination); 00645 } 00646 } 00647 if (modelCareStatesArray != NIL(array_t)) { 00648 careStatesArray = modelCareStatesArray; 00649 } else { 00650 careStatesArray = array_alloc(mdd_t *, 0); 00651 array_insert_last(mdd_t *, careStatesArray, mdd_one(mddMgr)); 00652 } 00653 mddArray_bot = array_alloc(mdd_t *, 0); 00654 mddArray_top = array_alloc(mdd_t *, 0); 00655 ctlFormula->share = 2; 00656 switch (Ctlp_FormulaReadType(ctlFormula)) { 00657 case Ctlp_ID_c :{ 00658 result = McModelCheckAtomicFormula(modelFsm, ctlFormula); 00659 matchfound_top = array_alloc(boolean, 0); 00660 matchfound_bot = array_alloc(boolean, 0); 00661 matchelement_top = array_alloc(int, 0); 00662 matchelement_bot = array_alloc(int, 0); 00663 leavesArray = array_alloc(Ctlp_Formula_t *, 0); 00664 array_insert(mdd_t *, mddArray_bot , 0, mdd_dup(result)); 00665 array_insert(mdd_t *, mddArray_top , 0, result); 00666 /* if the formula is an important subformula, we need to find the 00667 bottom and top set for it as well. */ 00668 if (ctlFormula->negation_parity != Ctlp_EvenOdd_c) { 00669 array_insert_last(Ctlp_Formula_t *, leavesArray, ctlFormula); 00670 if (ctlFormula->negation_parity == Ctlp_Even_c) { 00671 /* if the formula has even negation partity, it should be replaced 00672 with FALSE. */ 00673 result_bot = mdd_zero(mddMgr); 00674 result_top = mdd_one(mddMgr); 00675 } 00676 else { 00677 /* if the formula has odd negation parity, it should be replaced 00678 with TRUE. */ 00679 result_bot = mdd_one(mddMgr); 00680 result_top = mdd_zero(mddMgr); 00681 } 00682 array_insert_last(mdd_t *,mddArray_bot ,result_bot); 00683 array_insert_last(mdd_t *,mddArray_top ,result_top); 00684 /* Finding match for bottom sets */ 00685 if(mdd_equal(result_bot,array_fetch(mdd_t *, mddArray_bot, 0))){ 00686 array_insert(boolean, matchfound_bot, 1 ,TRUE); 00687 array_insert(int, matchelement_bot, 1 ,0); 00688 } 00689 else 00690 array_insert(boolean, matchfound_bot, 1 ,FALSE); 00691 /* Finding match for top sets */ 00692 if(mdd_equal(result_top,array_fetch(mdd_t *, mddArray_top, 0))){ 00693 array_insert(boolean, matchfound_top, 1 ,TRUE); 00694 array_insert(int, matchelement_top, 1 ,0); 00695 } 00696 else 00697 array_insert(boolean, matchfound_top, 1 ,FALSE); 00698 } 00699 array_insert(boolean, matchfound_bot, 0 ,FALSE); 00700 array_insert(boolean, matchfound_top, 0 ,FALSE); 00701 /* only exact set will be there if the formula is not an important 00702 subformula. */ 00703 ctlFormula->Topstates= mddArray_top; 00704 ctlFormula->matchfound_top = matchfound_top; 00705 ctlFormula->matchelement_top = matchelement_top; 00706 ctlFormula->Bottomstates = mddArray_bot; 00707 ctlFormula->matchfound_bot = matchfound_bot; 00708 ctlFormula->matchelement_bot = matchelement_bot; 00709 ctlFormula->leaves = leavesArray; 00710 break; 00711 } 00712 case Ctlp_TRUE_c :{ 00713 result = mdd_one(mddMgr); 00714 leavesArray = array_alloc(Ctlp_Formula_t *, 0); 00715 matchfound_top = array_alloc(boolean, 0); 00716 matchfound_bot = array_alloc(boolean, 0); 00717 matchelement_top = array_alloc(int, 0); 00718 matchelement_bot = array_alloc(int, 0); 00719 array_insert_last(mdd_t *,mddArray_bot , mdd_dup(result)); 00720 array_insert_last(mdd_t *,mddArray_top , result); 00721 array_insert(boolean, matchfound_bot, 0 ,FALSE); 00722 array_insert(boolean, matchfound_top, 0 ,FALSE); 00723 ctlFormula->Bottomstates = mddArray_bot; 00724 ctlFormula->matchfound_bot = matchfound_bot; 00725 ctlFormula->matchelement_bot = matchelement_bot; 00726 ctlFormula->Topstates = mddArray_top; 00727 ctlFormula->matchfound_top = matchfound_top; 00728 ctlFormula->matchelement_top = matchelement_top; 00729 ctlFormula->leaves = leavesArray; 00730 break; 00731 } 00732 case Ctlp_FALSE_c :{ 00733 result = mdd_zero(mddMgr); 00734 leavesArray = array_alloc(Ctlp_Formula_t *, 0); 00735 matchfound_top = array_alloc(boolean, 0); 00736 matchfound_bot = array_alloc(boolean, 0); 00737 matchelement_top = array_alloc(int, 0); 00738 matchelement_bot = array_alloc(int, 0); 00739 array_insert_last(mdd_t *,mddArray_bot ,mdd_dup(result)); 00740 array_insert_last(mdd_t *,mddArray_top ,mdd_dup(result)); 00741 array_insert(boolean, matchfound_bot, 0 ,FALSE); 00742 array_insert(boolean, matchfound_top, 0 ,FALSE); 00743 ctlFormula->Bottomstates = mddArray_bot; 00744 ctlFormula->matchfound_bot = matchfound_bot; 00745 ctlFormula->matchelement_bot = matchelement_bot; 00746 ctlFormula->Topstates = mddArray_top; 00747 ctlFormula->matchfound_top = matchfound_top; 00748 ctlFormula->matchelement_top = matchelement_top; 00749 ctlFormula->leaves = leavesArray; 00750 break; 00751 } 00752 case Ctlp_NOT_c :{ 00753 int i,positionmatch; 00754 arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { 00755 /* Now we shoud negate the accurate as well bottom mdds */ 00756 /* Compute Bottom sets */ 00757 if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){ 00758 result = mdd_not(leftMdd); 00759 array_insert_last(mdd_t *, mddArray_bot, mdd_dup(result)); 00760 mdd_free(result); 00761 } 00762 else{ 00763 positionmatch = array_fetch(int, leftChild->matchelement_bot, i); 00764 result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch)); 00765 array_insert_last(mdd_t *, mddArray_bot,result); 00766 } 00767 } 00768 arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { 00769 /* Compute for Top States */ 00770 if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){ 00771 result = mdd_not(leftMdd); 00772 array_insert_last(mdd_t *, mddArray_top, mdd_dup(result)); 00773 mdd_free(result); 00774 } 00775 else{ 00776 positionmatch = array_fetch(int, leftChild->matchelement_top, i); 00777 result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch)); 00778 array_insert_last(mdd_t *, mddArray_top, result); 00779 } 00780 } 00781 /* Now attach the array to the ctlFormula */ 00782 ctlFormula->Bottomstates = mddArray_bot; 00783 ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot); 00784 ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot); 00785 ctlFormula->Topstates = mddArray_top; 00786 ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top); 00787 ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top); 00788 /* find out the leaves attached to this nodes.*/ 00789 leavesLeftArray = leftChild->leaves; 00790 ctlFormula->leaves = array_dup(leavesLeftArray); 00791 break; 00792 } 00793 case Ctlp_AND_c:{ 00794 int number_right_bot = array_n(rightChild->Bottomstates); 00795 int number_right_top = array_n(rightChild->Topstates); 00796 int number_left_bot = array_n(leftChild->Bottomstates); 00797 int number_left_top = array_n(leftChild->Topstates); 00798 int i,positionmatch; 00799 leavesArray = array_alloc(Ctlp_Formula_t *, 0); 00800 matchfound_top = array_alloc(boolean, 0); 00801 matchfound_bot = array_alloc(boolean, 0); 00802 matchelement_top = array_alloc(int, 0); 00803 matchelement_bot = array_alloc(int, 0); 00804 /* And operation*/ 00805 /* for bottom sets */ 00806 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); 00807 arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { 00808 if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){ 00809 result = mdd_and(leftMdd, rightMdd, 1, 1); 00810 array_insert_last(mdd_t *, mddArray_bot, result); 00811 } 00812 else{ 00813 positionmatch = array_fetch(int,leftChild->matchelement_bot, i); 00814 result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch)); 00815 array_insert_last(mdd_t *, mddArray_bot, result); 00816 } 00817 } 00818 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); 00819 for(i=1;i<number_right_bot;i++){ 00820 if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){ 00821 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); 00822 result = mdd_and(leftMdd, rightMdd, 1, 1); 00823 array_insert_last(mdd_t *, mddArray_bot, result); 00824 } 00825 else{ 00826 positionmatch = array_fetch(int,rightChild->matchelement_bot, i); 00827 result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch + number_left_bot - 1))); 00828 array_insert_last(mdd_t *, mddArray_bot, result); 00829 } 00830 } 00831 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 00832 00833 /* for top sets */ 00834 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); 00835 arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { 00836 if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){ 00837 result = mdd_and(leftMdd, rightMdd, 1, 1); 00838 array_insert_last(mdd_t *, mddArray_top, result); 00839 } 00840 else{ 00841 positionmatch = array_fetch(int,leftChild->matchelement_top, i); 00842 result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch)); 00843 array_insert_last(mdd_t *, mddArray_top, result); 00844 } 00845 } 00846 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); 00847 for(i=1;i<number_right_top;i++){ 00848 if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){ 00849 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); 00850 result = mdd_and(leftMdd, rightMdd, 1, 1); 00851 array_insert_last(mdd_t *, mddArray_top, result); 00852 } 00853 else{ 00854 positionmatch = array_fetch(int,rightChild->matchelement_top, i); 00855 result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch + number_left_top - 1))); 00856 array_insert_last(mdd_t *, mddArray_top, result); 00857 } 00858 } 00859 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 00860 /* Now attach the array to the ctlFormula */ 00861 ctlFormula->Bottomstates = mddArray_bot; 00862 ctlFormula->Topstates = mddArray_top; 00863 /* find out the leaves attached to this nodes.*/ 00864 leavesLeftArray = leftChild->leaves; 00865 leavesRightArray = rightChild->leaves; 00866 array_append(leavesArray,leavesLeftArray); 00867 array_append(leavesArray,leavesRightArray); 00868 ctlFormula->leaves = leavesArray; 00869 break; 00870 } 00871 /* Use of EQ, XOR, THEN, OR is discouraged. Please use convert 00872 formula to simple existential form. */ 00873 case Ctlp_EQ_c :{ 00874 int number_right_bot = array_n(rightChild->Bottomstates); 00875 int number_right_top = array_n(rightChild->Topstates); 00876 int number_left_bot = array_n(leftChild->Bottomstates); 00877 int number_left_top = array_n(leftChild->Topstates); 00878 int i,positionmatch; 00879 leavesArray = array_alloc(Ctlp_Formula_t *, 0); 00880 matchfound_top = array_alloc(boolean, 0); 00881 matchfound_bot = array_alloc(boolean, 0); 00882 matchelement_top = array_alloc(int, 0); 00883 matchelement_bot = array_alloc(int, 0); 00884 /* for bottom sets */ 00885 rightMdd= array_fetch(mdd_t *,rightChild->Bottomstates,0); 00886 arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { 00887 if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){ 00888 result = mdd_xnor(leftMdd,rightMdd); 00889 array_insert_last(mdd_t *, mddArray_bot, result); 00890 } 00891 else{ 00892 positionmatch = array_fetch(int,leftChild->matchelement_bot, i); 00893 result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch)); 00894 array_insert_last(mdd_t *, mddArray_bot, result); 00895 } 00896 } 00897 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); 00898 for(i=1;i<number_right_bot;i++){ 00899 if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){ 00900 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); 00901 result = mdd_xnor(leftMdd,rightMdd ); 00902 array_insert_last(mdd_t *, mddArray_bot, result); 00903 } 00904 else{ 00905 positionmatch = array_fetch(int,rightChild->matchelement_bot, i); 00906 result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch+ number_left_bot - 1))); 00907 array_insert_last(mdd_t *, mddArray_bot, result); 00908 } 00909 } 00910 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 00911 00912 /* for top sets */ 00913 rightMdd= array_fetch(mdd_t *,rightChild->Topstates,0); 00914 arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { 00915 if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){ 00916 result = mdd_xnor(leftMdd,rightMdd); 00917 array_insert_last(mdd_t *, mddArray_top, result); 00918 } 00919 else{ 00920 positionmatch = array_fetch(int,leftChild->matchelement_top, i); 00921 result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch)); 00922 array_insert_last(mdd_t *, mddArray_top, result); 00923 } 00924 } 00925 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); 00926 for(i=1;i<number_right_top;i++){ 00927 if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){ 00928 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); 00929 result = mdd_xnor(leftMdd,rightMdd ); 00930 array_insert_last(mdd_t *, mddArray_top, result); 00931 } 00932 else{ 00933 positionmatch = array_fetch(int,rightChild->matchelement_top, i); 00934 result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch+ number_left_top - 1))); 00935 array_insert_last(mdd_t *, mddArray_top, result); 00936 } 00937 } 00938 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 00939 00940 /* Now attach the array to the ctlFormula */ 00941 ctlFormula->Bottomstates = mddArray_bot; 00942 ctlFormula->Topstates = mddArray_top; 00943 /* find out the leaves attached to this nodes.*/ 00944 leavesLeftArray = leftChild->leaves; 00945 leavesRightArray = rightChild->leaves; 00946 array_append(leavesArray,leavesLeftArray); 00947 array_append(leavesArray,leavesRightArray); 00948 ctlFormula->leaves = leavesArray; 00949 break; 00950 } 00951 case Ctlp_XOR_c :{ 00952 int number_right_bot = array_n(rightChild->Bottomstates); 00953 int number_right_top = array_n(rightChild->Topstates); 00954 int number_left_bot = array_n(leftChild->Bottomstates); 00955 int number_left_top = array_n(leftChild->Topstates); 00956 int i,positionmatch; 00957 leavesArray = array_alloc(Ctlp_Formula_t *, 0); 00958 matchfound_top = array_alloc(boolean, 0); 00959 matchfound_bot = array_alloc(boolean, 0); 00960 matchelement_top = array_alloc(int, 0); 00961 matchelement_bot = array_alloc(int, 0); 00962 /* for bottom sets */ 00963 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); 00964 arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { 00965 if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){ 00966 result = mdd_xor(leftMdd,rightMdd); 00967 array_insert_last(mdd_t *, mddArray_bot, result); 00968 } 00969 else{ 00970 positionmatch = array_fetch(int,leftChild->matchelement_bot, i); 00971 result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch)); 00972 array_insert_last(mdd_t *, mddArray_bot, result); 00973 } 00974 } 00975 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); 00976 for(i=1;i<number_right_bot;i++){ 00977 if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){ 00978 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); 00979 result = mdd_xor(leftMdd,rightMdd ); 00980 array_insert_last(mdd_t *, mddArray_bot, result); 00981 } 00982 else{ 00983 positionmatch = array_fetch(int,rightChild->matchelement_bot, i); 00984 result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch+ number_left_bot - 1))); 00985 array_insert_last(mdd_t *, mddArray_bot, result); 00986 } 00987 } 00988 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 00989 00990 /* for top sets */ 00991 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); 00992 arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { 00993 if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){ 00994 result = mdd_xor(leftMdd,rightMdd); 00995 array_insert_last(mdd_t *, mddArray_top, result); 00996 } 00997 else{ 00998 positionmatch = array_fetch(int,leftChild->matchelement_top, i); 00999 result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch)); 01000 array_insert_last(mdd_t *, mddArray_top, result); 01001 } 01002 } 01003 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); 01004 for(i=1;i<number_right_top;i++){ 01005 if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){ 01006 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); 01007 result = mdd_xor(leftMdd,rightMdd ); 01008 array_insert_last(mdd_t *, mddArray_top, result); 01009 } 01010 else{ 01011 positionmatch = array_fetch(int,rightChild->matchelement_top, i); 01012 result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch + number_left_top - 1))); 01013 array_insert_last(mdd_t *, mddArray_top, result); 01014 } 01015 } 01016 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 01017 01018 /* Now attach the array to the ctlFormula */ 01019 ctlFormula->Bottomstates = mddArray_bot; 01020 ctlFormula->Topstates = mddArray_top; 01021 /* find out the leaves attached to this nodes.*/ 01022 leavesLeftArray = leftChild->leaves; 01023 leavesRightArray = rightChild->leaves; 01024 array_append(leavesArray,leavesLeftArray); 01025 array_append(leavesArray,leavesRightArray); 01026 ctlFormula->leaves = leavesArray; 01027 break; 01028 } 01029 01030 case Ctlp_THEN_c :{ 01031 int number_right_bot = array_n(rightChild->Bottomstates); 01032 int number_right_top = array_n(rightChild->Topstates); 01033 int number_left_bot = array_n(leftChild->Bottomstates); 01034 int number_left_top = array_n(leftChild->Topstates); 01035 int i,positionmatch; 01036 leavesArray = array_alloc(Ctlp_Formula_t *, 0); 01037 matchfound_top = array_alloc(boolean, 0); 01038 matchfound_bot = array_alloc(boolean, 0); 01039 matchelement_top = array_alloc(int, 0); 01040 matchelement_bot = array_alloc(int, 0); 01041 /* bottom sets */ 01042 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); 01043 arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { 01044 if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){ 01045 result = mdd_or(leftMdd ,rightMdd,0,1); 01046 array_insert_last(mdd_t *, mddArray_bot, result); 01047 } 01048 else{ 01049 positionmatch = array_fetch(int,leftChild->matchelement_bot, i); 01050 result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch)); 01051 array_insert_last(mdd_t *, mddArray_bot, result); 01052 } 01053 } 01054 01055 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); 01056 for(i=1;i<number_right_bot;i++){ 01057 if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){ 01058 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); 01059 result = mdd_or(leftMdd,rightMdd ,0,1); 01060 array_insert_last(mdd_t *, mddArray_bot, result); 01061 } 01062 else{ 01063 positionmatch = array_fetch(int,rightChild->matchelement_bot, i); 01064 result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, (positionmatch + number_left_bot - 1))); 01065 array_insert_last(mdd_t *, mddArray_bot, result); 01066 } 01067 } 01068 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 01069 /* top sets */ 01070 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); 01071 arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { 01072 if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){ 01073 result = mdd_or(leftMdd ,rightMdd,0,1); 01074 array_insert_last(mdd_t *, mddArray_top, result); 01075 } 01076 else{ 01077 positionmatch = array_fetch(int,leftChild->matchelement_top, i); 01078 result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch)); 01079 array_insert_last(mdd_t *, mddArray_top, result); 01080 } 01081 } 01082 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); 01083 for(i=1;i<number_right_top;i++){ 01084 if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){ 01085 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); 01086 result = mdd_or(leftMdd,rightMdd ,0,1); 01087 array_insert_last(mdd_t *, mddArray_top, result); 01088 } 01089 else{ 01090 positionmatch = array_fetch(int,rightChild->matchelement_top, i); 01091 result = mdd_dup(array_fetch(mdd_t *, mddArray_top, (positionmatch + number_left_top - 1))); 01092 array_insert_last(mdd_t *, mddArray_top, result); 01093 } 01094 } 01095 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 01096 01097 /* Now attach the array to the ctlFormula */ 01098 ctlFormula->Bottomstates = mddArray_bot; 01099 ctlFormula->Topstates = mddArray_top; 01100 /* find out the leaves attached to this nodes.*/ 01101 leavesLeftArray = leftChild->leaves; 01102 leavesRightArray = rightChild->leaves; 01103 array_append(leavesArray,leavesLeftArray); 01104 array_append(leavesArray,leavesRightArray); 01105 ctlFormula->leaves = leavesArray; 01106 break; 01107 } 01108 case Ctlp_OR_c:{ 01109 int number_right_bot = array_n(rightChild->Bottomstates); 01110 int number_right_top = array_n(rightChild->Topstates); 01111 int number_left_bot = array_n(leftChild->Bottomstates); 01112 int number_left_top = array_n(leftChild->Topstates); 01113 int i,positionmatch; 01114 leavesArray = array_alloc(Ctlp_Formula_t *, 0); 01115 matchfound_top = array_alloc(boolean, 0); 01116 matchfound_bot = array_alloc(boolean, 0); 01117 matchelement_top = array_alloc(int, 0); 01118 matchelement_bot = array_alloc(int, 0); 01119 01120 /* OR operation*/ 01121 /* bottom sets */ 01122 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); 01123 arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { 01124 if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){ 01125 result = mdd_or(leftMdd,rightMdd,1,1); 01126 array_insert_last(mdd_t *, mddArray_bot, result); 01127 } 01128 else{ 01129 positionmatch = array_fetch(int,leftChild->matchelement_bot, i); 01130 result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch)); 01131 array_insert_last(mdd_t *, mddArray_bot, result); 01132 } 01133 } 01134 01135 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); 01136 for(i=1;i<number_right_bot;i++){ 01137 if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){ 01138 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); 01139 result = mdd_or(leftMdd,rightMdd ,1,1); 01140 array_insert_last(mdd_t *, mddArray_bot, result); 01141 } 01142 else{ 01143 positionmatch = array_fetch(int,rightChild->matchelement_bot, i); 01144 result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, (positionmatch + number_left_bot - 1))); 01145 array_insert_last(mdd_t *, mddArray_bot, result); 01146 } 01147 } 01148 01149 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 01150 01151 /* top sets */ 01152 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); 01153 arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { 01154 if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){ 01155 result = mdd_or(leftMdd,rightMdd,1,1); 01156 array_insert_last(mdd_t *, mddArray_top, result); 01157 } 01158 else{ 01159 positionmatch = array_fetch(int,leftChild->matchelement_top, i); 01160 result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch)); 01161 array_insert_last(mdd_t *, mddArray_top, result); 01162 } 01163 } 01164 01165 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); 01166 for(i=1;i<number_right_top;i++){ 01167 if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){ 01168 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); 01169 result = mdd_or(leftMdd,rightMdd ,1,1); 01170 array_insert_last(mdd_t *, mddArray_top, result); 01171 } 01172 else{ 01173 positionmatch = array_fetch(int,rightChild->matchelement_top, i); 01174 result = mdd_dup(array_fetch(mdd_t *, mddArray_top, (positionmatch + number_left_top - 1))); 01175 array_insert_last(mdd_t *, mddArray_top, result); 01176 } 01177 } 01178 01179 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 01180 /* Now attach the array to the ctlFormula */ 01181 ctlFormula->Topstates = mddArray_top; 01182 ctlFormula->Bottomstates = mddArray_bot; 01183 /* ctlFormula->states = array_fetch(mdd_t *, mddArray, 0); */ 01184 /* find out the leaves attached to this nodes.*/ 01185 leavesLeftArray = leftChild->leaves; 01186 leavesRightArray = rightChild->leaves; 01187 array_append(leavesArray,leavesLeftArray); 01188 array_append(leavesArray,leavesRightArray); 01189 ctlFormula->leaves = leavesArray; 01190 break; 01191 } 01192 case Ctlp_EX_c:{ 01193 int i,positionmatch; 01194 if (ctlFormula->negation_parity == Ctlp_Even_c) { 01195 /* bottom sets shoud be computed first i.e underapproximations */ 01196 arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { 01197 if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){ 01198 result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates, 01199 careStatesArray, verbosity, dcLevel); 01200 array_insert_last(mdd_t *, mddArray_bot, result); 01201 } 01202 else{ 01203 positionmatch = array_fetch(int, leftChild->matchelement_bot, i); 01204 result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch)); 01205 array_insert_last(mdd_t *, mddArray_bot, result); 01206 } 01207 } 01208 result = array_fetch(mdd_t *, mddArray_bot, 0); /* exact set */ 01209 } 01210 else{ 01211 /* top sets should be computed first i.e., underapproximations */ 01212 arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { 01213 if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){ 01214 result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates, 01215 careStatesArray, verbosity, dcLevel); 01216 array_insert_last(mdd_t *, mddArray_top, result); 01217 } 01218 else{ 01219 positionmatch = array_fetch(int, leftChild->matchelement_top, i); 01220 result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch)); 01221 array_insert_last(mdd_t *, mddArray_top, result); 01222 } 01223 } 01224 result = array_fetch(mdd_t *, mddArray_top, 0); /* exact set */ 01225 } 01226 if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)){ 01227 if (ctlFormula->negation_parity == Ctlp_Even_c) { 01228 ctlFormula->Bottomstates = mddArray_bot; 01229 arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { 01230 array_insert_last(mdd_t *, mddArray_top, mdd_dup(result)); 01231 } 01232 ctlFormula->Topstates = mddArray_top; 01233 ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot); 01234 ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot); 01235 matchfound_top = array_alloc(boolean, 0); 01236 matchelement_top = array_alloc(int, 0); 01237 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 01238 } 01239 else{ 01240 ctlFormula->Topstates = mddArray_top; 01241 arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { 01242 array_insert_last(mdd_t *, mddArray_bot, mdd_dup(result)); 01243 } 01244 ctlFormula->Bottomstates = mddArray_bot; 01245 ctlFormula->matchfound_top = array_dup(leftChild->matchfound_bot); 01246 ctlFormula->matchelement_top = array_dup(leftChild->matchelement_bot); 01247 matchfound_bot = array_alloc(int, 0); 01248 matchelement_bot = array_alloc(int, 0); 01249 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 01250 } 01251 /* find out the leaves attached to this nodes.*/ 01252 leavesLeftArray = leftChild->leaves; 01253 ctlFormula->leaves = array_dup(leavesLeftArray); 01254 break; 01255 } 01256 if (ctlFormula->negation_parity == Ctlp_Even_c) { 01257 /* top sets */ 01258 arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { 01259 if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){ 01260 result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates, 01261 careStatesArray, verbosity, dcLevel); 01262 array_insert_last(mdd_t *, mddArray_top, result); 01263 } 01264 else{ 01265 positionmatch = array_fetch(int, leftChild->matchelement_top, i); 01266 result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch)); 01267 array_insert_last(mdd_t *, mddArray_top, result); 01268 } 01269 01270 } 01271 } 01272 else { 01273 arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { 01274 if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){ 01275 result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates, 01276 careStatesArray, verbosity, dcLevel); 01277 array_insert_last(mdd_t *, mddArray_bot, result); 01278 } 01279 else{ 01280 positionmatch = array_fetch(int, leftChild->matchelement_bot, i); 01281 result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch)); 01282 array_insert_last(mdd_t *, mddArray_bot, result); 01283 } 01284 01285 } 01286 } 01287 /* Now attach the array to the ctlFormula */ 01288 ctlFormula->Bottomstates = mddArray_bot; 01289 ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot); 01290 ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot); 01291 ctlFormula->Topstates = mddArray_top; 01292 ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top); 01293 ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top); 01294 /* find out the leaves attached to this nodes.*/ 01295 leavesLeftArray = leftChild->leaves; 01296 ctlFormula->leaves = array_dup(leavesLeftArray); 01297 break; 01298 } 01299 01300 case Ctlp_EU_c:{ 01301 array_t *onionRings = NIL(array_t); 01302 array_t *MergeOnionRings = NIL(array_t); 01303 array_t *ExactOnionRings = NIL(array_t); 01304 array_t *NewOnionRings = NIL(array_t); /* array of mdd_t */ 01305 boolean fixpoint; 01306 int number_left_bot = array_n(leftChild->Bottomstates); 01307 int number_right_bot = array_n(rightChild->Bottomstates); 01308 int number_left_top = array_n(leftChild->Topstates); 01309 int number_right_top = array_n(rightChild->Topstates); 01310 int i; 01311 int j = 1; 01312 mdd_t *approx_under = NIL(mdd_t); 01313 array_t *botrings = NIL(array_t); 01314 array_t *toprings = NIL(array_t); 01315 leavesArray = array_alloc(Ctlp_Formula_t *, 0); 01316 matchfound_top = array_alloc(boolean, 0); 01317 matchfound_bot = array_alloc(boolean, 0); 01318 matchelement_top = array_alloc(int, 0); 01319 matchelement_bot = array_alloc(int, 0); 01320 approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Underapprox_c ); 01321 onionRings = NIL(array_t); 01322 if (buildOnionRings) { 01323 MergeOnionRings = array_alloc(mdd_t *, 0); 01324 botrings = array_alloc(array_t*,0); 01325 toprings = array_alloc(array_t*,0); 01326 } 01327 if (ctlFormula->negation_parity == Ctlp_Even_c) { 01328 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); 01329 result_underapprox = mdd_zero(mddMgr); 01330 /* Compute the bottom mdds first which provide the underapproximation 01331 * to the exact set*/ 01332 for(i=1;i<number_left_bot;i++) { 01333 if (buildOnionRings) 01334 onionRings = array_alloc(mdd_t *, 0); 01335 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i); 01336 result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, 01337 rightMdd, 01338 approx, fairStates, 01339 careStatesArray, 01340 earlyTermination, hintsArray, 01341 hintType, onionRings, 01342 verbosity, dcLevel, &fixpoint); 01343 array_insert(mdd_t *, mddArray_bot, j, result); 01344 if (buildOnionRings) { 01345 if(i==1) { 01346 mdd_array_free(MergeOnionRings); 01347 MergeOnionRings = mdd_array_duplicate(onionRings); 01348 /* saving the bottom computation onion rings */ 01349 array_insert(array_t*,botrings,j,onionRings); 01350 } 01351 else { 01352 MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings); 01353 /* saving the bottom computation onion rings */ 01354 array_insert(array_t*,botrings,j,onionRings); 01355 } 01356 } 01357 j++; 01358 result_new = mdd_or(result,result_underapprox,1,1); 01359 mdd_free(result_underapprox); 01360 result_underapprox = result_new; 01361 } 01362 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); 01363 for(i=1;i<number_right_bot;i++) { 01364 if (buildOnionRings) 01365 onionRings = array_alloc(mdd_t *, 0); 01366 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); 01367 result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, 01368 rightMdd, 01369 approx, fairStates, 01370 careStatesArray, 01371 earlyTermination, hintsArray, 01372 hintType, onionRings, 01373 verbosity, dcLevel, &fixpoint); 01374 array_insert(mdd_t *, mddArray_bot, j, result); 01375 if (buildOnionRings) { 01376 if(i==1) { 01377 mdd_array_free(MergeOnionRings); 01378 MergeOnionRings = mdd_array_duplicate(onionRings); 01379 /* saving the bottom computation onion rings */ 01380 array_insert(array_t*,botrings,j,onionRings); 01381 } 01382 else { 01383 MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings); 01384 /* saving the bottom computation onion rings */ 01385 array_insert(array_t*,botrings,j,onionRings); 01386 } 01387 } 01388 j++; 01389 result_new = mdd_or(result,result_underapprox,1,1); 01390 mdd_free(result_underapprox); 01391 result_underapprox = result_new; 01392 } 01393 /* Use the under approximations to calculate the exact set. */ 01394 if (approx != NIL(mdd_t)) { 01395 mdd_t *tmp = mdd_or(result_underapprox,approx,1,1); 01396 mdd_free(approx); 01397 mdd_free(result_underapprox); 01398 approx = tmp; 01399 } else { 01400 approx = result_underapprox; 01401 } 01402 if (buildOnionRings) { 01403 onionRings = array_alloc(mdd_t *, 0); 01404 } 01405 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); 01406 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); 01407 result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, 01408 rightMdd, 01409 approx, fairStates, 01410 careStatesArray, 01411 earlyTermination, hintsArray, 01412 hintType, onionRings, 01413 verbosity, dcLevel, &fixpoint); 01414 array_insert(mdd_t *, mddArray_bot, 0, mdd_dup(result)); 01415 array_insert(mdd_t *, mddArray_top, 0, result); 01416 if (buildOnionRings) { 01417 MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings); 01418 mdd_array_free(onionRings); 01419 Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) MergeOnionRings, 01420 McFormulaFreeDebugData); 01421 array_insert(array_t *,botrings,0,mdd_array_duplicate(MergeOnionRings)); 01422 array_insert(array_t *,toprings,0,mdd_array_duplicate(MergeOnionRings)); 01423 } 01424 result = array_fetch(mdd_t *,mddArray_bot,0); 01425 if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)) { 01426 leavesLeftArray = leftChild->leaves; 01427 array_append(leavesArray,leavesLeftArray); 01428 leavesRightArray = rightChild->leaves; 01429 array_append(leavesArray,leavesRightArray); 01430 ctlFormula->leaves = leavesArray; 01431 j=1; 01432 for(i=1;i<number_left_top;i++) { 01433 array_insert(mdd_t *, mddArray_top, j, mdd_dup(result)); 01434 if (buildOnionRings) { 01435 array_insert(array_t *,toprings,j, 01436 mdd_array_duplicate(MergeOnionRings)); 01437 } 01438 j++; 01439 } 01440 for(i=1;i<number_right_top;i++) { 01441 array_insert(mdd_t *, mddArray_top, j, mdd_dup(result)); 01442 if (buildOnionRings){ 01443 array_insert(array_t *,toprings,j, 01444 mdd_array_duplicate(MergeOnionRings)); 01445 } 01446 j++; 01447 } 01448 ctlFormula->Bottomstates = mddArray_bot; 01449 ctlFormula->Topstates = mddArray_top; 01450 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 01451 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 01452 if (buildOnionRings) { 01453 ctlFormula->BotOnionRings = botrings; 01454 ctlFormula->TopOnionRings = toprings; 01455 } 01456 mdd_free(approx); 01457 break; /* bottom failing */ 01458 } 01459 /* top sets 01460 * we can use the exact set as an approximation to compute the top 01461 * set. */ 01462 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); 01463 j=1; 01464 if (buildOnionRings) 01465 ExactOnionRings = mdd_array_duplicate(MergeOnionRings); 01466 /* Compute the Top mdds now */ 01467 for(i=1;i<number_left_top;i++) { 01468 if (buildOnionRings) 01469 onionRings = array_alloc(mdd_t *, 0); 01470 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i); 01471 approx_under = array_fetch(mdd_t *,mddArray_bot,0); 01472 result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, 01473 rightMdd, 01474 approx_under, fairStates, 01475 careStatesArray, 01476 earlyTermination, hintsArray, 01477 hintType, onionRings, 01478 verbosity, dcLevel, &fixpoint); 01479 array_insert(mdd_t *, mddArray_top, j, result); 01480 if (buildOnionRings) { 01481 array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings); 01482 NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings); 01483 /* saving the bottom computation onion rings */ 01484 array_insert(array_t*,toprings,j,NewOnionRings); 01485 mdd_array_free(onionRings); 01486 } 01487 j++; 01488 } 01489 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); 01490 for(i=1;i<number_right_top;i++) { 01491 if (buildOnionRings) 01492 onionRings = array_alloc(mdd_t *, 0); 01493 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); 01494 approx_under = array_fetch(mdd_t *,mddArray_top,0); 01495 result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, 01496 rightMdd, 01497 approx_under, fairStates, 01498 careStatesArray, 01499 earlyTermination, hintsArray, 01500 hintType, onionRings, 01501 verbosity, dcLevel, &fixpoint); 01502 array_insert(mdd_t *, mddArray_top, j, result); 01503 if (buildOnionRings) { 01504 array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings); 01505 NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings); 01506 /* saving the bottom computation onion rings */ 01507 array_insert(array_t*,toprings,j,NewOnionRings); 01508 mdd_array_free(onionRings); 01509 } 01510 j++; 01511 } 01512 } 01513 else { 01514 /* The negation parity is odd. So the top sets will provide 01515 underapproximations now. */ 01516 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); 01517 result_underapprox = mdd_zero(mddMgr); 01518 /* Compute the top mdds first */ 01519 for(i=1;i<number_left_top;i++) { 01520 if (buildOnionRings) 01521 onionRings = array_alloc(mdd_t *, 0); 01522 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i); 01523 result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, 01524 rightMdd, 01525 NIL(mdd_t), fairStates, 01526 careStatesArray, 01527 earlyTermination, hintsArray, 01528 hintType, onionRings, 01529 verbosity, dcLevel, &fixpoint); 01530 array_insert(mdd_t *, mddArray_top, j, result); 01531 if (buildOnionRings){ 01532 if(i==1){ 01533 mdd_array_free(MergeOnionRings); 01534 MergeOnionRings = mdd_array_duplicate(onionRings); 01535 array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */ 01536 } 01537 else { 01538 array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */ 01539 MergeOnionRings=GenerateOnionRings(MergeOnionRings,onionRings); 01540 } 01541 } 01542 j++; 01543 result_new = mdd_or(result,result_underapprox,1,1); 01544 mdd_free(result_underapprox); 01545 result_underapprox = result_new; 01546 } 01547 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); 01548 for(i=1;i<number_right_top;i++) { 01549 if (buildOnionRings) 01550 onionRings = array_alloc(mdd_t *, 0); 01551 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); 01552 result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, 01553 rightMdd, 01554 NIL(mdd_t), fairStates, 01555 careStatesArray, 01556 earlyTermination, hintsArray, 01557 hintType, onionRings, 01558 verbosity, dcLevel, &fixpoint); 01559 array_insert(mdd_t *, mddArray_top, j, result); 01560 if (buildOnionRings) { 01561 if(j==1){ 01562 mdd_array_free(MergeOnionRings); 01563 MergeOnionRings = mdd_array_duplicate(onionRings); 01564 array_insert(array_t*,toprings,j,onionRings); /* saving the top computation onion rings */ 01565 } 01566 else { 01567 MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings); 01568 array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */ 01569 } 01570 } 01571 j++; 01572 result_new = mdd_or(result,result_underapprox,1,1); 01573 mdd_free(result_underapprox); 01574 result_underapprox = result_new; 01575 } 01576 /* Use the under approximations to calculate the exact set. */ 01577 if (approx != NIL(mdd_t)) { 01578 mdd_t *tmp = mdd_or(result_underapprox,approx,1,1); 01579 mdd_free(approx); 01580 mdd_free(result_underapprox); 01581 approx = tmp; 01582 } else { 01583 approx = result_underapprox; 01584 } 01585 if (buildOnionRings) { 01586 onionRings = array_alloc(mdd_t *, 0); 01587 } 01588 /* exact set computation */ 01589 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); 01590 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); 01591 result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, 01592 rightMdd, 01593 approx, fairStates, 01594 careStatesArray, 01595 earlyTermination, hintsArray, 01596 hintType, onionRings, 01597 verbosity, dcLevel, &fixpoint); 01598 array_insert(mdd_t *, mddArray_bot, 0, mdd_dup(result)); 01599 array_insert(mdd_t *, mddArray_top, 0, result); 01600 if (buildOnionRings) { 01601 MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings); 01602 mdd_array_free(onionRings); 01603 Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) MergeOnionRings, 01604 McFormulaFreeDebugData); 01605 array_insert(array_t *,botrings,0, 01606 mdd_array_duplicate(MergeOnionRings)); 01607 array_insert(array_t *,toprings,0, 01608 mdd_array_duplicate(MergeOnionRings)); 01609 } 01610 result = array_fetch(mdd_t *,mddArray_bot,0); 01611 if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)) { 01612 leavesLeftArray = leftChild->leaves; 01613 array_append(leavesArray,leavesLeftArray); 01614 leavesRightArray = rightChild->leaves; 01615 array_append(leavesArray,leavesRightArray); 01616 ctlFormula->leaves = leavesArray; 01617 j=1; 01618 for(i=1;i<number_left_bot;i++) { 01619 array_insert(mdd_t *, mddArray_bot, j, mdd_dup(result)); 01620 if (buildOnionRings){ 01621 array_insert(array_t *,botrings,j, 01622 mdd_array_duplicate(MergeOnionRings)); 01623 } 01624 j++; 01625 } 01626 for(i=1;i<number_right_bot;i++) { 01627 array_insert(mdd_t *, mddArray_bot, j, mdd_dup(result)); 01628 if (buildOnionRings){ 01629 array_insert(array_t *,botrings,j, 01630 mdd_array_duplicate(MergeOnionRings)); 01631 } 01632 j++; 01633 } 01634 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 01635 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 01636 ctlFormula->Bottomstates = mddArray_bot; 01637 ctlFormula->Topstates = mddArray_top; 01638 if (buildOnionRings){ 01639 ctlFormula->BotOnionRings = botrings; 01640 ctlFormula->TopOnionRings = toprings; 01641 } 01642 assert(approx != NIL(mdd_t)); 01643 mdd_free(approx); 01644 break; /* bottom failing */ 01645 } 01646 if (buildOnionRings) 01647 ExactOnionRings = mdd_array_duplicate(MergeOnionRings); 01648 /* we can use the exact set as an approximation to compute 01649 the bottom set. */ 01650 rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); 01651 j=1; 01652 /* Compute the botom mdds now */ 01653 for(i=1;i<number_left_bot;i++) { 01654 if (buildOnionRings) 01655 onionRings = array_alloc(mdd_t *, 0); 01656 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i); 01657 approx_under = array_fetch(mdd_t *,mddArray_bot,0); 01658 result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, 01659 rightMdd, 01660 approx_under, fairStates, 01661 careStatesArray, 01662 earlyTermination, hintsArray, 01663 hintType, onionRings, 01664 verbosity, dcLevel, &fixpoint); 01665 array_insert(mdd_t *, mddArray_bot, j, result); 01666 if (buildOnionRings){ 01667 array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings); 01668 NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings); 01669 /* saving the bottom computation onion rings */ 01670 array_insert(array_t*,botrings,j,NewOnionRings); 01671 mdd_array_free(onionRings); 01672 } 01673 j++; 01674 } 01675 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); 01676 for(i=1;i<number_right_bot;i++) { 01677 if (buildOnionRings) 01678 onionRings = array_alloc(mdd_t *, 0); 01679 else 01680 onionRings = NIL(array_t); 01681 rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); 01682 approx_under = array_fetch(mdd_t *,mddArray_bot,0); 01683 result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, 01684 rightMdd, 01685 NIL(mdd_t), fairStates, 01686 careStatesArray, 01687 earlyTermination, hintsArray, 01688 hintType, onionRings, 01689 verbosity, dcLevel, &fixpoint); 01690 array_insert(mdd_t *, mddArray_bot, j, result); 01691 if (buildOnionRings) { 01692 array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings); 01693 NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings); 01694 array_insert(array_t*,botrings,j,NewOnionRings); 01695 mdd_array_free(onionRings); 01696 } 01697 j++; 01698 } 01699 } 01700 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 01701 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 01702 ctlFormula->Bottomstates = mddArray_bot; 01703 ctlFormula->Topstates = mddArray_top; 01704 leavesLeftArray = leftChild->leaves; 01705 array_append(leavesArray,leavesLeftArray); 01706 leavesRightArray = rightChild->leaves; 01707 array_append(leavesArray,leavesRightArray); 01708 ctlFormula->leaves = leavesArray; 01709 if (buildOnionRings) { 01710 ctlFormula->BotOnionRings = botrings; 01711 ctlFormula->TopOnionRings = toprings; 01712 mdd_array_free(ExactOnionRings); 01713 } 01714 if(approx != NIL(mdd_t)) 01715 mdd_free(approx); 01716 /* Can't combine under and overapprox */ 01717 if(!fixpoint && TRMinimization == Ctlp_Overapprox_c) 01718 TRMinimization = Ctlp_Incomparable_c; 01719 break; 01720 } 01721 01722 case Ctlp_EG_c:{ 01723 boolean fixpoint; 01724 mdd_t *result_ub; 01725 mdd_t *approx_over = NIL(mdd_t) ; 01726 int number_bot = array_n(leftChild->Bottomstates); 01727 int number_top = array_n(leftChild->Topstates); 01728 int i; 01729 array_t *arrayOfOnionRings = NIL(array_t); /* array of array of mdd_t* */ 01730 array_t *botrings = NIL(array_t); 01731 array_t *toprings = NIL(array_t); 01732 matchfound_top = array_alloc(boolean, 0); 01733 matchfound_bot = array_alloc(boolean, 0); 01734 matchelement_top = array_alloc(int, 0); 01735 matchelement_bot = array_alloc(int, 0); 01736 approx = Ctlp_FormulaObtainApproxStates(ctlFormula, Ctlp_Overapprox_c); 01737 if(buildOnionRings) { 01738 botrings = array_alloc(array_t*,0); 01739 toprings = array_alloc(array_t*,0); 01740 } 01741 if (approx == NIL(mdd_t)) { 01742 result_ub = mdd_one(mddMgr); 01743 } else { 01744 result_ub = mdd_dup(approx); 01745 } 01746 if (ctlFormula->negation_parity == Ctlp_Even_c) { 01747 /* compute the top sets first which will give us 01748 overapproximation to the exact set */ 01749 for(i=1;i<number_top;i++) { 01750 if(buildOnionRings) 01751 arrayOfOnionRings = array_alloc(array_t *, 0); 01752 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i); 01753 result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, 01754 NIL(mdd_t), fairStates, 01755 fairCondition, careStatesArray, 01756 earlyTermination, hintsArray, 01757 hintType, 01758 &arrayOfOnionRings, verbosity, 01759 dcLevel, &fixpoint, GSHschedule); 01760 array_insert(mdd_t *, mddArray_top, i, result); 01761 if(buildOnionRings) { 01762 array_insert(array_t*,toprings,i,arrayOfOnionRings); 01763 } 01764 result_new = mdd_and(result_ub,result,1,1); 01765 mdd_free(result_ub); 01766 result_ub = result_new; 01767 } 01768 /* calculate the exact set */ 01769 if(buildOnionRings) 01770 arrayOfOnionRings = array_alloc(array_t *, 0); 01771 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); 01772 result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, 01773 NIL(mdd_t), fairStates, 01774 fairCondition, careStatesArray, 01775 earlyTermination, hintsArray, 01776 hintType, 01777 &arrayOfOnionRings, verbosity, 01778 dcLevel, &fixpoint, GSHschedule); 01779 array_insert(mdd_t *,mddArray_bot,0,mdd_dup(result)); 01780 array_insert(mdd_t *,mddArray_top,0,mdd_dup(result)); 01781 mdd_free(result); 01782 if(buildOnionRings) { 01783 Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings, 01784 McFormulaFreeDebugData); 01785 array_insert(array_t*,toprings,0,McMddArrayArrayDup(arrayOfOnionRings)); 01786 array_insert(array_t*,botrings,0,McMddArrayArrayDup(arrayOfOnionRings)); 01787 } 01788 result = array_fetch(mdd_t *,mddArray_bot,0); 01789 if (McCheckEarlyTerminationForOverapprox(earlyTermination, result, careStatesArray)) { 01790 leavesLeftArray = leftChild->leaves; 01791 ctlFormula->leaves = array_dup(leavesLeftArray); 01792 for(i=1;i<number_bot;i++) { 01793 array_insert(mdd_t *, mddArray_bot, i, mdd_dup(result)); 01794 if(buildOnionRings) { 01795 array_insert(array_t*,botrings,i,McMddArrayArrayDup(arrayOfOnionRings)); 01796 } 01797 } 01798 ctlFormula->Bottomstates = mddArray_bot; 01799 ctlFormula->Topstates = mddArray_top; 01800 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 01801 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 01802 if (buildOnionRings) { 01803 ctlFormula->BotOnionRings = botrings; 01804 ctlFormula->TopOnionRings = toprings; 01805 } 01806 break;/* top passing */ 01807 } 01808 /* now calculate the bottom set */ 01809 for(i=1;i<number_bot;i++) { 01810 if(buildOnionRings) 01811 arrayOfOnionRings = array_alloc(array_t *, 0); 01812 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i); 01813 approx_over = array_fetch(mdd_t *,mddArray_bot,0); 01814 result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, 01815 approx_over, fairStates, 01816 fairCondition, careStatesArray, 01817 earlyTermination, hintsArray, 01818 hintType, 01819 &arrayOfOnionRings, verbosity, 01820 dcLevel, &fixpoint, GSHschedule); 01821 array_insert(mdd_t *, mddArray_bot, i, result); 01822 if(buildOnionRings) { 01823 array_insert(array_t*,botrings,i,arrayOfOnionRings); 01824 } 01825 } 01826 } 01827 else { 01828 /* compute the bottom sets first which will give us 01829 overapproximation to the exact set */ 01830 for(i=1;i<number_bot;i++) { 01831 if(buildOnionRings) 01832 arrayOfOnionRings = array_alloc(array_t *, 0); 01833 leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i); 01834 result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, 01835 NIL(mdd_t), fairStates, 01836 fairCondition, careStatesArray, 01837 earlyTermination, hintsArray, 01838 hintType, 01839 &arrayOfOnionRings, verbosity, 01840 dcLevel, &fixpoint, GSHschedule); 01841 if(buildOnionRings) { 01842 array_insert(array_t*,botrings,i,arrayOfOnionRings); 01843 } 01844 array_insert(mdd_t *, mddArray_bot, i, result); 01845 result_new = mdd_and(result_ub,result,1,1); 01846 mdd_free(result_ub); 01847 result_ub = result_new; 01848 } 01849 /* calculate the exact set */ 01850 if(buildOnionRings){ 01851 arrayOfOnionRings = array_alloc(array_t *, 0); 01852 } 01853 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); 01854 result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, 01855 result_ub, fairStates, 01856 fairCondition, careStatesArray, 01857 earlyTermination, hintsArray, 01858 hintType, 01859 &arrayOfOnionRings, verbosity, 01860 dcLevel, &fixpoint, GSHschedule); 01861 array_insert(mdd_t *,mddArray_bot,0,mdd_dup(result)); 01862 array_insert(mdd_t *,mddArray_top,0,mdd_dup(result)); 01863 mdd_free(result); 01864 if (buildOnionRings) { 01865 Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings, 01866 McFormulaFreeDebugData); 01867 array_insert(array_t*,botrings,0,McMddArrayArrayDup(arrayOfOnionRings)); 01868 array_insert(array_t*,toprings,0,McMddArrayArrayDup(arrayOfOnionRings)); 01869 } 01870 result = array_fetch(mdd_t *,mddArray_bot,0); 01871 if (McCheckEarlyTerminationForOverapprox(earlyTermination, result, careStatesArray)) { 01872 leavesLeftArray = leftChild->leaves; 01873 ctlFormula->leaves = array_dup(leavesLeftArray); 01874 for(i=1;i<number_top;i++) { 01875 array_insert(mdd_t *, mddArray_top, i, mdd_dup(result)); 01876 if(buildOnionRings) 01877 array_insert(array_t*,toprings,i,McMddArrayArrayDup(arrayOfOnionRings)); 01878 } 01879 ctlFormula->Bottomstates = mddArray_bot; 01880 ctlFormula->Topstates = mddArray_top; 01881 match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); 01882 match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); 01883 if (buildOnionRings) { 01884 ctlFormula->BotOnionRings = botrings; 01885 ctlFormula->TopOnionRings = toprings; 01886 } 01887 break; /* top passing */ 01888 } 01889 /* calculate the top set now */ 01890 for(i=1;i<number_top;i++) { 01891 if (buildOnionRings) { 01892 arrayOfOnionRings = array_alloc(array_t *, 0); 01893 } 01894 leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i); 01895 approx_over = array_fetch(mdd_t *,mddArray_bot,0); 01896 result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, 01897 approx, fairStates, 01898 fairCondition, careStatesArray, 01899 earlyTermination, hintsArray, 01900 hintType, 01901 &arrayOfOnionRings, verbosity, 01902 dcLevel, &fixpoint, GSHschedule); 01903 array_insert(mdd_t *, mddArray_top, i, result); 01904 if(buildOnionRings) 01905 array_insert(array_t*,toprings,i,arrayOfOnionRings); 01906 } 01907 } 01908 mdd_free(result_ub); 01909 /* Now attach the array to the ctlFormula */ 01910 ctlFormula->Bottomstates = mddArray_bot; 01911 ctlFormula->Topstates = mddArray_top; 01912 /* Discard previous copies. */ 01913 array_free(matchfound_bot); 01914 array_free(matchelement_bot); 01915 array_free(matchfound_top); 01916 array_free(matchelement_top); 01917 ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot); 01918 ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot); 01919 ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top); 01920 ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top); 01921 /* find out the leaves attached to this nodes.*/ 01922 leavesLeftArray = leftChild->leaves; 01923 ctlFormula->leaves = array_dup(leavesLeftArray); 01924 if (buildOnionRings) { 01925 ctlFormula->BotOnionRings = botrings; 01926 ctlFormula->TopOnionRings = toprings; 01927 } 01928 if(approx != NIL(mdd_t)) mdd_free(approx); 01929 01930 /* Can't combine under and overapprox */ 01931 if(!fixpoint && TRMinimization == Ctlp_Underapprox_c) 01932 TRMinimization = Ctlp_Incomparable_c; 01933 01934 break; 01935 } 01936 01937 case Ctlp_Init_c: 01938 result = Fsm_FsmComputeInitialStates(modelFsm); 01939 break; 01940 01941 default: fail("Encountered unknown type of CTL formula\n"); 01942 } 01943 tmpMdd = mdd_dup(array_fetch(mdd_t *,mddArray_bot,0)); 01944 thisApproxType = ComputeResultingApproximation( 01945 Ctlp_FormulaReadType(ctlFormula), leftApproxType, 01946 rightApproxType, TRMinimization, earlyTermination, fixpoint); 01947 Ctlp_FormulaSetApproxStates(ctlFormula,tmpMdd, TRMinimization); 01948 01949 #ifdef DEBUG_MC 01950 /* The following code is just for debugging */ 01951 if ((verbosity == McVerbosityMax_c)) { 01952 char *type = Ctlp_FormulaGetTypeString(ctlFormula); 01953 if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_Cmp_c) { 01954 fprintf(vis_stdout, "Info : result for [Cmp]\n"); 01955 if (bdd_is_tautology(result, 1)) 01956 fprintf(vis_stdout, "TRUE\n"); 01957 else 01958 fprintf(vis_stdout, "FALSE\n"); 01959 } 01960 else if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_ID_c) { 01961 char *atomic = Ctlp_FormulaConvertToString(ctlFormula); 01962 fprintf(vis_stdout, "Info : satisfying minterms for [%s(%s)]:\n", 01963 type, atomic); 01964 free(atomic); 01965 if (bdd_is_tautology(result, 1)) 01966 fprintf(vis_stdout, "-- TAUTOLOGY --\n"); 01967 else if (bdd_is_tautology(result, 0)) 01968 fprintf(vis_stdout, "-- null --\n"); 01969 else 01970 (void)_McPrintSatisfyingMinterms(result, modelFsm); 01971 } 01972 else { 01973 fprintf(vis_stdout, "Info : satisfying minterms for [%s]:\n", type); 01974 if (bdd_is_tautology(result, 1)) 01975 fprintf(vis_stdout, "-- TAUTOLOGY --\n"); 01976 else if (bdd_is_tautology(result, 0)) 01977 fprintf(vis_stdout, "-- null --\n"); 01978 else 01979 (void)_McPrintSatisfyingMinterms(result, modelFsm); 01980 } 01981 free(type); 01982 } 01983 #endif 01984 if (modelCareStatesArray == NIL(array_t)) 01985 mdd_array_free(careStatesArray); 01986 return; 01987 } /* ModelcheckAndVacuity */ 01988 01989 02002 static void 02003 CreateImportantWitness( 02004 Ctlp_Formula_t *OldctlFormula, 02005 Ctlp_Formula_t *ctlFormula, 02006 int i) 02007 { 02008 Ctlp_Formula_t *rightChild, *leftChild,*OldrightChild, *OldleftChild; 02009 int number_left_bot; 02010 array_t *onionRings = NIL(array_t); /* array of mdd_t */ 02011 array_t *arrayOfOnionRings = NIL(array_t); 02012 Ctlp_FormulaType formulaType; 02013 formulaType = Ctlp_FormulaReadType(ctlFormula); 02014 rightChild = Ctlp_FormulaReadRightChild(ctlFormula); 02015 leftChild = Ctlp_FormulaReadLeftChild(ctlFormula); 02016 OldrightChild = Ctlp_FormulaReadRightChild(OldctlFormula); 02017 OldleftChild = Ctlp_FormulaReadLeftChild(OldctlFormula); 02018 02019 if(leftChild) 02020 number_left_bot = array_n(OldleftChild->Bottomstates); 02021 else 02022 number_left_bot = -1; /* don't care */ 02023 02024 switch (formulaType) { 02025 case Ctlp_EU_c: 02026 if(ctlFormula->states != NIL(mdd_t)) 02027 mdd_free(ctlFormula->states); 02028 ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i)); 02029 #if 0 02030 fprintf(vis_stdout,"Attaching bdd for EU %d",i); 02031 bdd_print(ctlFormula->states); 02032 mdd_array_free(array_fetch(array_t*,OldctlFormula->BotOnionRings,i)); 02033 #endif 02034 onionRings = mdd_array_duplicate(array_fetch(array_t*,OldctlFormula->BotOnionRings,i)); 02035 Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings, 02036 McFormulaFreeDebugData); 02037 assert(leftChild != NULL && rightChild != NULL); 02038 if(i<number_left_bot){ 02039 CreateImportantWitness(OldleftChild,leftChild,i); 02040 } 02041 else{ 02042 CreateImportantWitness(OldleftChild,leftChild,0); 02043 } 02044 02045 if(i<number_left_bot ){ 02046 CreateImportantWitness(OldrightChild,rightChild,0); 02047 } 02048 else { 02049 CreateImportantWitness(OldrightChild,rightChild,i - number_left_bot + 1); 02050 } 02051 break; 02052 case Ctlp_EG_c: 02053 if(ctlFormula->states != NIL(mdd_t)) 02054 mdd_free(ctlFormula->states); 02055 ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i)); 02056 #if 0 02057 fprintf(vis_stdout,"Attaching bdd for EG %d",i); 02058 bdd_print(ctlFormula->states); 02059 mdd_array_free(array_fetch(array_t*,OldctlFormula->BotOnionRings,i)); 02060 #endif 02061 arrayOfOnionRings = McMddArrayArrayDup(array_fetch(array_t* ,OldctlFormula->BotOnionRings,i)); 02062 Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings, 02063 McFormulaFreeDebugData); 02064 CreateImportantWitness(OldleftChild,leftChild,i); 02065 break; 02066 case Ctlp_AX_c: 02067 case Ctlp_AG_c: 02068 case Ctlp_AF_c: 02069 case Ctlp_AU_c: 02070 case Ctlp_EX_c: 02071 case Ctlp_EF_c: 02072 case Ctlp_OR_c: 02073 case Ctlp_AND_c: 02074 case Ctlp_NOT_c: 02075 case Ctlp_THEN_c: 02076 case Ctlp_XOR_c: 02077 case Ctlp_EQ_c: 02078 if(ctlFormula->states != NIL(mdd_t)) 02079 mdd_free(ctlFormula->states); 02080 ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i)); 02081 #if 0 02082 fprintf(vis_stdout,"Attaching bdd for NOT,THEN %d",i); 02083 bdd_print(ctlFormula->states); 02084 #endif 02085 02086 if(leftChild){ 02087 if(i<number_left_bot){ 02088 CreateImportantWitness(OldleftChild,leftChild,i); 02089 } 02090 else { 02091 CreateImportantWitness(OldleftChild,leftChild,0); 02092 } 02093 } 02094 02095 if(rightChild){ 02096 if(i<number_left_bot ){ 02097 CreateImportantWitness(OldrightChild,rightChild,0); 02098 } 02099 else{ 02100 CreateImportantWitness(OldrightChild,rightChild,i - number_left_bot + 1); 02101 } 02102 } 02103 break; 02104 case Ctlp_ID_c: 02105 case Ctlp_TRUE_c: 02106 case Ctlp_FALSE_c: 02107 case Ctlp_Init_c: 02108 if(ctlFormula->states != NIL(mdd_t)) 02109 mdd_free(ctlFormula->states); 02110 ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i)); 02111 #if 0 02112 fprintf(vis_stdout,"Attaching bdd for ID,TRUE %d",i); 02113 bdd_print(ctlFormula->states); 02114 #endif 02115 break; 02116 02117 default: 02118 break; 02119 } 02120 } /* CreateImportantWitness */ 02121 02122 02135 static void 02136 CreateImportantCounterexample( 02137 Ctlp_Formula_t *OldctlFormula, 02138 Ctlp_Formula_t *ctlFormula, 02139 int i) 02140 { 02141 Ctlp_Formula_t *rightChild, *leftChild, *OldrightChild, *OldleftChild; 02142 int number_left_top; 02143 array_t *onionRings = NIL(array_t); /* array of mdd_t */ 02144 array_t *arrayOfOnionRings = NIL(array_t); 02145 Ctlp_FormulaType formulaType; 02146 formulaType = Ctlp_FormulaReadType(ctlFormula); 02147 rightChild = Ctlp_FormulaReadRightChild(ctlFormula); 02148 leftChild = Ctlp_FormulaReadLeftChild(ctlFormula); 02149 OldrightChild = Ctlp_FormulaReadRightChild(OldctlFormula); 02150 OldleftChild = Ctlp_FormulaReadLeftChild(OldctlFormula); 02151 02152 if(leftChild) 02153 number_left_top = array_n(OldleftChild->Topstates); 02154 else 02155 number_left_top = -1; /* don't care */ 02156 02157 switch (formulaType) { 02158 case Ctlp_EU_c: 02159 if(ctlFormula->states != NIL(mdd_t)) 02160 mdd_free(ctlFormula->states); 02161 ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i)); 02162 onionRings = mdd_array_duplicate(array_fetch(array_t*,OldctlFormula->TopOnionRings,i)); 02163 Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings, 02164 McFormulaFreeDebugData); 02165 assert(leftChild != NULL && rightChild != NULL); 02166 if(i<number_left_top){ 02167 CreateImportantCounterexample(OldleftChild,leftChild,i); 02168 } 02169 else{ 02170 CreateImportantCounterexample(OldleftChild,leftChild,0); 02171 } 02172 02173 if(i<number_left_top ){ 02174 CreateImportantCounterexample(OldrightChild,rightChild,0); 02175 } 02176 else { 02177 CreateImportantCounterexample(OldrightChild,rightChild,i - 02178 number_left_top + 1); 02179 } 02180 break; 02181 case Ctlp_EG_c: 02182 if(ctlFormula->states != NIL(mdd_t)) 02183 mdd_free(ctlFormula->states); 02184 ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i)); 02185 arrayOfOnionRings = McMddArrayArrayDup(array_fetch(array_t* ,OldctlFormula->TopOnionRings,i)); 02186 Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings, 02187 McFormulaFreeDebugData); 02188 CreateImportantCounterexample(OldleftChild,leftChild,i); 02189 break; 02190 case Ctlp_AX_c: 02191 case Ctlp_AG_c: 02192 case Ctlp_AF_c: 02193 case Ctlp_AU_c: 02194 case Ctlp_EX_c: 02195 case Ctlp_EF_c: 02196 case Ctlp_OR_c: 02197 case Ctlp_AND_c: 02198 case Ctlp_NOT_c: 02199 case Ctlp_THEN_c: 02200 case Ctlp_XOR_c: 02201 case Ctlp_EQ_c: 02202 if(ctlFormula->states != NIL(mdd_t)) 02203 mdd_free(ctlFormula->states); 02204 ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i)); 02205 02206 if(leftChild){ 02207 if(i<number_left_top){ 02208 CreateImportantCounterexample(OldleftChild,leftChild,i); 02209 } 02210 else { 02211 CreateImportantCounterexample(OldleftChild,leftChild,0); 02212 } 02213 } 02214 02215 if(rightChild){ 02216 if(i<number_left_top ){ 02217 CreateImportantCounterexample(OldrightChild,rightChild,0); 02218 } 02219 else{ 02220 CreateImportantCounterexample(OldrightChild,rightChild,i - 02221 number_left_top + 1); 02222 } 02223 } 02224 break; 02225 case Ctlp_ID_c: 02226 case Ctlp_TRUE_c: 02227 case Ctlp_FALSE_c: 02228 case Ctlp_Init_c: 02229 if(ctlFormula->states != NIL(mdd_t)) 02230 mdd_free(ctlFormula->states); 02231 ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i)); 02232 #if 0 02233 fprintf(vis_stdout,"Attaching bdd for ID,TRUE %d",i); 02234 bdd_print(ctlFormula->states); 02235 #endif 02236 break; 02237 02238 default: 02239 break; 02240 } 02241 } /* CreateImportantCounterexample */ 02242 02243 02255 static array_t * 02256 McMddArrayArrayDup(array_t *arrayBddArray) 02257 { 02258 int i; 02259 array_t *bddArray, *tmpbddArray; 02260 int length; 02261 array_t *result; 02262 /* put assert for this if (arrayBddArray != NIL(array_t)) { */ 02263 length = array_n(arrayBddArray); 02264 result = array_alloc(array_t *, length); 02265 for (i = 0; i < length; i++) { 02266 bddArray = array_fetch(array_t *, arrayBddArray, i); 02267 tmpbddArray = mdd_array_duplicate(bddArray); 02268 array_insert(array_t *,result,i,tmpbddArray); 02269 } 02270 return(result); 02271 } /* McMddArrayArrayDup */ 02272 02273 02285 static void 02286 match_top( 02287 Ctlp_Formula_t *ctlFormula, 02288 array_t *mddArray, 02289 array_t *matchfound, 02290 array_t *matchelement) 02291 { 02292 int i, j, positionmatch; 02293 mdd_t *leftMdd1 = NIL(mdd_t); 02294 mdd_t *leftMdd2 = NIL(mdd_t); 02295 02296 arrayForEachItem(mdd_t *, mddArray, i, leftMdd1){ 02297 array_insert(boolean, matchfound, i, FALSE); 02298 } 02299 02300 arrayForEachItem(mdd_t *, mddArray, i, leftMdd1) { 02301 arrayForEachItem(mdd_t *, mddArray, j, leftMdd2) { 02302 if((i != 0) && (j != 0) && (i != j)) { 02303 if (mdd_equal(leftMdd2, leftMdd1)) { 02304 if (array_fetch(boolean, matchfound,i) == TRUE) { 02305 if(array_fetch(int, matchelement,i) != j) { 02306 positionmatch = array_fetch(int, matchelement, i); 02307 array_insert(int, matchelement, j, positionmatch); 02308 } 02309 } 02310 else{ 02311 array_insert(int, matchelement, j, i); 02312 array_insert(boolean, matchfound, j, TRUE); 02313 } 02314 } 02315 } 02316 } 02317 } 02318 ctlFormula->matchfound_top = matchfound; 02319 ctlFormula->matchelement_top = matchelement; 02320 return; 02321 } /* match_top */ 02322 02323 02335 static void 02336 match_bot( 02337 Ctlp_Formula_t *ctlFormula, 02338 array_t *mddArray, 02339 array_t *matchfound, 02340 array_t *matchelement) 02341 { 02342 int i, j, positionmatch; 02343 mdd_t *leftMdd1 = NIL(mdd_t); 02344 mdd_t *leftMdd2 = NIL(mdd_t); 02345 02346 arrayForEachItem(mdd_t *, mddArray, i, leftMdd1){ 02347 array_insert(boolean, matchfound, i, FALSE); 02348 } 02349 02350 arrayForEachItem(mdd_t *, mddArray, i, leftMdd1) { 02351 arrayForEachItem(mdd_t *, mddArray, j, leftMdd2) { 02352 if ((i != 0) && (j != 0) && (i != j)) { 02353 if (mdd_equal(leftMdd2, leftMdd1)) { 02354 if (array_fetch(boolean, matchfound, i) == TRUE) { 02355 if (array_fetch(int, matchelement, i) != j) { 02356 positionmatch = array_fetch(int, matchelement, i); 02357 array_insert(int, matchelement, j, positionmatch); 02358 } 02359 } 02360 else { 02361 array_insert(int, matchelement, j, i); 02362 array_insert(boolean, matchfound, j ,TRUE); 02363 } 02364 } 02365 } 02366 } 02367 } 02368 ctlFormula->matchfound_bot = matchfound; 02369 ctlFormula->matchelement_bot = matchelement; 02370 return; 02371 } /* match_bot */ 02372 02373 02385 static array_t * 02386 GenerateOnionRings( 02387 array_t* TempOnionRings, 02388 array_t* onionRings) 02389 { 02390 array_t* MergeOnionRings; 02391 int mdd1number, mdd2number, k; 02392 mdd_t *temp,*temp1,*mdd1,*mdd2,*mdd3 = NIL(mdd_t); 02393 02394 mdd1number = array_n(TempOnionRings); 02395 mdd2number = array_n(onionRings); 02396 if(mdd1number == 0) { 02397 MergeOnionRings = mdd_array_duplicate(onionRings); 02398 array_free(TempOnionRings); 02399 return (MergeOnionRings); 02400 } 02401 MergeOnionRings = array_alloc(mdd_t *, 0); 02402 mdd1 = array_fetch(mdd_t *,TempOnionRings,0); 02403 mdd2 = array_fetch(mdd_t *,onionRings,0); 02404 temp = mdd_or(mdd1,mdd2,1,1); /* Building the core for EU */ 02405 array_insert(mdd_t *,MergeOnionRings,0, temp); 02406 if(mdd2number>=mdd1number) { 02407 for(k=1;k<mdd1number;k++) { 02408 mdd1 = array_fetch(mdd_t *, onionRings, k); 02409 mdd2 = array_fetch(mdd_t *, MergeOnionRings, k-1); 02410 mdd3 = array_fetch(mdd_t *, TempOnionRings, k); 02411 temp1 = mdd_or(mdd1,mdd3,1,1); 02412 temp = mdd_and(temp1,mdd2,1,0); 02413 mdd_free(temp1); 02414 array_insert(mdd_t*, MergeOnionRings, k, temp); 02415 } 02416 for(k=mdd1number;k<mdd2number;k++) { 02417 mdd1 = array_fetch(mdd_t *, onionRings, k); 02418 mdd2 = array_fetch(mdd_t *, MergeOnionRings, k-1); 02419 temp = mdd_and(mdd1,mdd2,1,0); 02420 array_insert(mdd_t*, MergeOnionRings, k, temp); 02421 } 02422 } 02423 else { 02424 for(k=1;k<mdd2number;k++) { 02425 mdd1 =array_fetch(mdd_t *, onionRings, k); 02426 mdd2 =array_fetch(mdd_t *, MergeOnionRings, k-1); 02427 mdd3 =array_fetch(mdd_t *, TempOnionRings, k); 02428 temp1 = mdd_or(mdd1,mdd3,1,1); 02429 temp = mdd_and(temp1,mdd2,1,0); 02430 mdd_free(temp1); 02431 array_insert(mdd_t*, MergeOnionRings, k, temp); 02432 } 02433 } 02434 mdd_array_free(TempOnionRings); 02435 return(MergeOnionRings); 02436 } /* GenerateOnionRings */ 02437 02438 02451 static void 02452 FormulaFreeDebugDataVac( 02453 Ctlp_Formula_t *formula) 02454 { 02455 int i; 02456 array_t *TopOnion, *BottomOnion; 02457 Ctlp_FormulaType type = Ctlp_FormulaReadType(formula); 02458 if(formula->type != Ctlp_ID_c ){ 02459 if (formula->left != NIL(Ctlp_Formula_t)) { 02460 FormulaFreeDebugDataVac(formula->left); 02461 } 02462 if (formula->right != NIL(Ctlp_Formula_t)) { 02463 FormulaFreeDebugDataVac(formula->right); 02464 } 02465 } 02466 if (type == Ctlp_EU_c || type == Ctlp_EG_c ) { 02467 if (formula->TopOnionRings != NIL(array_t)) { 02468 TopOnion = formula->TopOnionRings; 02469 for (i = 0; i < array_n(TopOnion); i++) { 02470 if (type == Ctlp_EU_c) { 02471 mdd_array_free(array_fetch(array_t *, TopOnion, i)); 02472 } 02473 else if (type == Ctlp_EG_c) 02474 mdd_array_array_free(array_fetch(array_t *, TopOnion, i)); 02475 } 02476 array_free(TopOnion); 02477 } 02478 if (formula->BotOnionRings != NIL(array_t)) { 02479 BottomOnion = formula->BotOnionRings; 02480 for (i = 0; i < array_n(BottomOnion); i++) { 02481 if (type == Ctlp_EU_c) { 02482 mdd_array_free(array_fetch(array_t *, BottomOnion, i)); 02483 } 02484 else if (type == Ctlp_EG_c) 02485 mdd_array_array_free(array_fetch(array_t *, BottomOnion, i)); 02486 } 02487 array_free(BottomOnion); 02488 } 02489 } 02490 } /* FormulaFreeDebugDataVac */
1.7.3