- Generated on Wed Oct 12 2011 00:34:49 for VIS by
1.7.3
|
VIS
|
00001 00059 #include "ctlpInt.h" 00060 #include "mcInt.h" 00061 00062 00063 /*---------------------------------------------------------------------------*/ 00064 /* Constant declarations */ 00065 /*---------------------------------------------------------------------------*/ 00066 00067 /*---------------------------------------------------------------------------*/ 00068 /* Stucture declarations */ 00069 /*---------------------------------------------------------------------------*/ 00070 00071 /*---------------------------------------------------------------------------*/ 00072 /* Type declarations */ 00073 /*---------------------------------------------------------------------------*/ 00074 00075 /*---------------------------------------------------------------------------*/ 00076 /* Variable declarations */ 00077 /*---------------------------------------------------------------------------*/ 00078 00079 #ifndef lint 00080 static char rcsid[] UNUSED = "$Id: mcCover.c,v 1.4 2005/05/15 07:32:10 fabio Exp $"; 00081 #endif 00082 00083 /*---------------------------------------------------------------------------*/ 00084 /* Macro declarations */ 00085 /*---------------------------------------------------------------------------*/ 00086 00089 /*---------------------------------------------------------------------------*/ 00090 /* Static function prototypes */ 00091 /*---------------------------------------------------------------------------*/ 00092 00093 static mdd_t * CoveredStatesHoskote(mdd_t *startstates_old, Fsm_Fsm_t *fsm, Ctlp_Formula_t *OrigFormula, 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, array_t *signalList, array_t *statesCoveredList, array_t *newCoveredStatesList, array_t *statesToRemoveList); 00094 static mdd_t * CoveredStatesImproved(mdd_t *startstates_old, Fsm_Fsm_t *fsm, Ctlp_Formula_t *OrigFormula, 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, array_t *signalList, array_t *statesCoveredList, array_t *newCoveredStatesList, array_t *statesToRemoveList); 00095 static mdd_t * CoveragePropositional(mdd_t *startstates_old, Fsm_Fsm_t *fsm, Ctlp_Formula_t *OrigFormula, 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, array_t *signalList, array_t *statesCoveredList, array_t *newCoveredStatesList, array_t *statesToRemoveList); 00096 static mdd_t * computedepend(Fsm_Fsm_t *fsm, Ctlp_Formula_t *formula, 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, char *signal, mdd_t *SoAndTb_old); 00097 static mdd_t * computedependHoskote(Fsm_Fsm_t *fsm, Ctlp_Formula_t *formula, 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 *startstates_old, char *signal, mdd_t *Tb, mdd_t *statesCovered, mdd_t *newCoveredStates, mdd_t *statesToRemove); 00098 static mdd_t * traverse(Fsm_Fsm_t *fsm, 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 *startstates, Ctlp_Formula_t *formula1, Ctlp_Formula_t *formula2); 00099 static mdd_t * firstReached(Fsm_Fsm_t *fsm, 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 *startstates, Ctlp_Formula_t *formula); 00100 static Ctlp_Formula_t * FormulaConvertSignalComplement(Fsm_Fsm_t *fsm, char *signal, Ctlp_Formula_t *formula); 00101 static void findallsignals(Fsm_Fsm_t *fsm, array_t *signalTypeList, array_t *signalList, array_t *statesCoveredList, array_t *newCoveredStatesList, array_t *statesToRemoveList, Ctlp_Formula_t *formula, mdd_t *zeroMdd); 00102 static void findallsignalsInFormula(array_t *signalList, Ctlp_Formula_t *formula); 00103 static int positionOfSignalinList(char *signal, array_t *signalList); 00104 static int RangeofSignalinFormula(Fsm_Fsm_t *fsm, char *signal, Ctlp_Formula_t *formula); 00105 00108 /*---------------------------------------------------------------------------*/ 00109 /* Definition of exported functions */ 00110 /*---------------------------------------------------------------------------*/ 00111 00112 00113 /*---------------------------------------------------------------------------*/ 00114 /* Definition of internal functions */ 00115 /*---------------------------------------------------------------------------*/ 00116 00117 00133 void 00134 McEstimateCoverage( 00135 Fsm_Fsm_t *modelFsm, 00136 Ctlp_Formula_t *ctlFormula, 00137 int i, 00138 mdd_t *fairStates, 00139 Fsm_Fairness_t *fairCond, 00140 array_t *modelCareStatesArray, 00141 Mc_EarlyTermination_t *earlyTermination, 00142 array_t *hintsStatesArray, 00143 Mc_GuidedSearch_t guidedSearchType, 00144 Mc_VerbosityLevel verbosity, 00145 Mc_DcLevel dcLevel, 00146 int buildOnionRings, 00147 Mc_GSHScheduleType GSHschedule, 00148 Mc_FwdBwdAnalysis traversalDirection, 00149 mdd_t *modelInitialStates, 00150 mdd_t *ctlFormulaStates, 00151 mdd_t **totalcoveredstates, 00152 array_t *signalTypeList, 00153 array_t *signalList, 00154 array_t *statesCoveredList, 00155 array_t *newCoveredStatesList, 00156 array_t *statesToRemoveList, 00157 boolean performCoverageHoskote, 00158 boolean performCoverageImproved) 00159 { 00160 double numtotcoveredstates; 00161 double numnewcoveredstates; 00162 mdd_t *CovstatesHoskote; 00163 mdd_t *CovstatesImproved; 00164 Ctlp_Formula_t *origFormula; 00165 00166 if (performCoverageHoskote && 00167 (modelCareStatesArray != NIL(array_t))) { /* and no errors till now? */ 00168 mdd_t *tmp_mdd, *zero_mdd; 00169 int sigarr; 00170 array_t *listOfSignals = array_alloc(char *,0); 00171 origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula); 00172 if ( ( (traversalDirection == McFwd_c) && bdd_is_tautology(ctlFormulaStates, 1) ) || 00173 mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1) ) { /* formula passes */ 00174 00175 if (*totalcoveredstates == NIL(mdd_t)) 00176 *totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 00177 00178 /* add new signals if any found */ 00179 zero_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 00180 findallsignals(modelFsm, signalTypeList, signalList, 00181 statesCoveredList, newCoveredStatesList, 00182 statesToRemoveList, origFormula, 00183 zero_mdd); 00184 mdd_free(zero_mdd); 00185 fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1); 00186 fprintf(vis_stdout,"===================================\n"); 00187 00188 CovstatesHoskote = CoveredStatesHoskote(modelInitialStates, 00189 modelFsm, origFormula, 00190 fairStates, fairCond, 00191 modelCareStatesArray, 00192 earlyTermination, 00193 hintsStatesArray, 00194 guidedSearchType, verbosity, 00195 dcLevel, buildOnionRings, 00196 GSHschedule, signalList, 00197 statesCoveredList, 00198 newCoveredStatesList, 00199 statesToRemoveList); 00200 numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00201 CovstatesHoskote, 00202 Fsm_FsmReadPresentStateVars(modelFsm)); 00203 tmp_mdd = mdd_and(CovstatesHoskote,*totalcoveredstates,1,0); 00204 00205 numnewcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00206 tmp_mdd, 00207 Fsm_FsmReadPresentStateVars(modelFsm)); 00208 mdd_free(tmp_mdd); 00209 fprintf(vis_stdout,"\n--Total states covered by formula<%d> = %.0f , new = %.0f\n",i+1, 00210 numtotcoveredstates,numnewcoveredstates); 00211 findallsignalsInFormula(listOfSignals,origFormula); 00212 for (sigarr=0;sigarr<array_n(listOfSignals);sigarr++) { 00213 mdd_t *newCoveredStates,*statesCovered,*tmp_mdd; 00214 char *signalInFormula; 00215 int positionInList; 00216 signalInFormula = array_fetch(char *,listOfSignals,sigarr); 00217 positionInList = positionOfSignalinList(signalInFormula,signalList); 00218 00219 newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList); 00220 statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList); 00221 tmp_mdd = mdd_and(newCoveredStates,statesCovered,1,0); /*newly covered States*/ 00222 fprintf(vis_stdout,"---States covered w.r.t. %s = %.0f, new = %.0f\n", 00223 signalInFormula, 00224 mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00225 newCoveredStates, 00226 Fsm_FsmReadPresentStateVars(modelFsm)), 00227 mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00228 tmp_mdd, 00229 Fsm_FsmReadPresentStateVars(modelFsm))); 00230 mdd_free(tmp_mdd); 00231 00232 /* add on the newcoveredstates*/ 00233 tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1); 00234 mdd_free(statesCovered); 00235 /*update statesCoveredList*/ 00236 array_insert(mdd_t *,statesCoveredList,positionInList,tmp_mdd); 00237 mdd_free(newCoveredStates); 00238 00239 /* reset newCoveredStatesList to zeroMdds for the next formula */ 00240 tmp_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 00241 array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd); 00242 } 00243 00244 } else { /* formula fails */ 00245 CovstatesHoskote = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 00246 fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1); 00247 fprintf(vis_stdout,"===================================\n"); 00248 fprintf(vis_stdout,"Coverage for failing formulae = 0\n"); 00249 } 00250 if (*totalcoveredstates == NIL(mdd_t)) 00251 *totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 00252 00253 if (CovstatesHoskote != NIL(mdd_t)){ 00254 mdd_t *tmp_mdd = mdd_or(*totalcoveredstates,CovstatesHoskote,1,1); 00255 mdd_free(*totalcoveredstates); 00256 *totalcoveredstates = tmp_mdd; 00257 } 00258 00259 numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00260 *totalcoveredstates, 00261 Fsm_FsmReadPresentStateVars(modelFsm)); 00262 mdd_free(CovstatesHoskote); 00263 array_free(listOfSignals); 00264 } 00265 00266 if (performCoverageImproved && (modelCareStatesArray != NIL(array_t))) { /* and no errors till now ??*/ 00267 mdd_t *tmp_mdd, *zero_mdd; 00268 int sigarr; 00269 array_t *listOfSignals = array_alloc(char *,0); 00270 origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula); 00271 if ( ( (traversalDirection == McFwd_c) && 00272 bdd_is_tautology(ctlFormulaStates, 1) ) || 00273 (mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1)) ) { 00274 /* formula passes */ 00275 00276 if (*totalcoveredstates == NIL(mdd_t)) 00277 *totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 00278 00279 /*add new signals if any found*/ 00280 zero_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 00281 findallsignals(modelFsm, signalTypeList, signalList, 00282 statesCoveredList, newCoveredStatesList, 00283 statesToRemoveList, origFormula, zero_mdd); 00284 mdd_free(zero_mdd); 00285 fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1); 00286 fprintf(vis_stdout,"===================================\n"); 00287 00288 CovstatesImproved = CoveredStatesImproved(modelInitialStates, 00289 modelFsm, origFormula, 00290 fairStates, fairCond, 00291 modelCareStatesArray, 00292 earlyTermination, 00293 hintsStatesArray, 00294 guidedSearchType, 00295 verbosity, 00296 dcLevel, buildOnionRings, 00297 GSHschedule, signalList, 00298 statesCoveredList, 00299 newCoveredStatesList, 00300 statesToRemoveList); 00301 numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00302 CovstatesImproved, 00303 Fsm_FsmReadPresentStateVars(modelFsm)); 00304 tmp_mdd = mdd_and(CovstatesImproved,*totalcoveredstates,1,0); 00305 00306 numnewcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00307 tmp_mdd, 00308 Fsm_FsmReadPresentStateVars(modelFsm)); 00309 mdd_free(tmp_mdd); 00310 fprintf(vis_stdout,"\n--Total states covered by formula<%d> = %.0f , new = %.0f\n",i+1, 00311 numtotcoveredstates,numnewcoveredstates); 00312 findallsignalsInFormula(listOfSignals,origFormula); 00313 for (sigarr=0;sigarr<array_n(listOfSignals);sigarr++) { 00314 mdd_t *newCoveredStates,*statesCovered,*tmp_mdd; 00315 char *signalInFormula; 00316 int positionInList; 00317 signalInFormula = array_fetch(char *,listOfSignals,sigarr); 00318 positionInList = positionOfSignalinList(signalInFormula,signalList); 00319 00320 newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList); 00321 statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList); 00322 tmp_mdd = mdd_and(newCoveredStates,statesCovered,1,0); /*newly covered States*/ 00323 fprintf(vis_stdout,"---States covered w.r.t. %s = %.0f, new = %.0f\n", 00324 signalInFormula, 00325 mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00326 newCoveredStates, 00327 Fsm_FsmReadPresentStateVars(modelFsm)), 00328 mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00329 tmp_mdd, 00330 Fsm_FsmReadPresentStateVars(modelFsm))); 00331 mdd_free(tmp_mdd); 00332 00333 /* add on the newcoveredstates*/ 00334 tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1); 00335 mdd_free(statesCovered); 00336 /*update statesCoveredList*/ 00337 array_insert(mdd_t *,statesCoveredList,positionInList,tmp_mdd); 00338 mdd_free(newCoveredStates); 00339 00340 /* reset newCoveredStatesList to zeroMdds for the next formula */ 00341 tmp_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 00342 array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd); 00343 } 00344 00345 } else { /* formula fails */ 00346 CovstatesImproved = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 00347 fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1); 00348 fprintf(vis_stdout,"===================================\n"); 00349 fprintf(vis_stdout,"Coverage for failing formulae = 0\n"); 00350 } 00351 if (*totalcoveredstates == NIL(mdd_t)) 00352 *totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 00353 00354 if (CovstatesImproved != NIL(mdd_t)){ 00355 mdd_t *tmp_mdd = mdd_or(*totalcoveredstates,CovstatesImproved,1,1); 00356 mdd_free(*totalcoveredstates); 00357 *totalcoveredstates = tmp_mdd; 00358 } 00359 00360 numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00361 *totalcoveredstates, 00362 Fsm_FsmReadPresentStateVars(modelFsm)); 00363 mdd_free(CovstatesImproved); 00364 array_free(listOfSignals); 00365 } 00366 00367 } /* McEstimateCoverage */ 00368 00369 00379 void 00380 McPrintCoverageSummary( 00381 Fsm_Fsm_t *modelFsm, 00382 Mc_DcLevel dcLevel, 00383 McOptions_t *options, 00384 array_t *modelCareStatesArray, 00385 mdd_t *modelCareStates, 00386 mdd_t *totalcoveredstates, 00387 array_t *signalTypeList, 00388 array_t *signalList, 00389 array_t *statesCoveredList, 00390 boolean performCoverageHoskote, 00391 boolean performCoverageImproved 00392 ) 00393 { 00394 float coverage; 00395 float coveragePI; 00396 float coveragePO; 00397 float coverageOther; 00398 float numPI; 00399 float numPO; 00400 float numOther; 00401 float avgCoverage; 00402 float avgPICoverage; 00403 float avgPOCoverage; 00404 float avgOtherCoverage; 00405 double numrchstates; 00406 double numtotcoveredstates; 00407 00408 if (performCoverageHoskote && 00409 (modelCareStatesArray != NIL(array_t))) { /* and no errors till now */ 00410 int sigarr; 00411 if (totalcoveredstates != NIL(mdd_t) && (modelCareStates != NIL(mdd_t))) { 00412 numtotcoveredstates = mdd_count_onset( 00413 Fsm_FsmReadMddManager(modelFsm), 00414 totalcoveredstates, 00415 Fsm_FsmReadPresentStateVars(modelFsm)); 00416 } 00417 else { 00418 numtotcoveredstates = 0; 00419 } 00420 00421 if ((dcLevel == McDcLevelRch_c)||(dcLevel == McDcLevelRchFrontier_c)) { 00422 if (!mdd_lequal(totalcoveredstates, modelCareStates, 1, 1)) { 00423 (void)fprintf(vis_stdout, 00424 "** mc warning: Some of the covered states are not reachable\n"); 00425 } 00426 if (modelCareStates !=NIL(mdd_t)){ 00427 int sigType; 00428 coveragePI = 0; 00429 coveragePO = 0; 00430 coverageOther = 0; 00431 numPI = 0; 00432 numPO = 0; 00433 numOther = 0; 00434 avgCoverage = 0; 00435 avgPICoverage = 0; 00436 avgPOCoverage = 0; 00437 avgOtherCoverage = 0; 00438 numrchstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00439 modelCareStates, 00440 Fsm_FsmReadPresentStateVars(modelFsm)); 00441 if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/ 00442 fprintf(vis_stdout,"\nCoverage for all the Formulae w.r.t. all observable signals\n"); 00443 fprintf(vis_stdout,"=============================================================\n"); 00444 } 00445 for (sigarr=0;sigarr<array_n(signalList);sigarr++) { 00446 mdd_t *statesCovered, *uncoveredStateCube, *uncoveredStates; 00447 double numStatesCovered; 00448 char *nrOfUncoveredStatesString; 00449 int nrOfUncoveredStates, prntStates; /* nr of uncovered states that we output */ 00450 00451 Ntk_Network_t *modelNetworkC = Fsm_FsmReadNetwork(modelFsm); 00452 array_t *PSVarsC = Fsm_FsmReadPresentStateVars(modelFsm); 00453 mdd_manager *mddMgrC = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm)); 00454 00455 statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr); 00456 numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00457 statesCovered,Fsm_FsmReadPresentStateVars(modelFsm)); 00458 coverage = (numStatesCovered / numrchstates) * 100; 00459 avgCoverage = avgCoverage + coverage; 00460 sigType = array_fetch(int, signalTypeList,sigarr); 00461 if (sigType == 1) { 00462 coveragePI = coveragePI + numStatesCovered; 00463 avgPICoverage = avgPICoverage + coverage; 00464 numPI = numPI + 1; 00465 } 00466 else if (sigType == 0) { 00467 coveragePO = coveragePO + numStatesCovered; 00468 avgPOCoverage = avgPOCoverage + coverage; 00469 numPO = numPO + 1; 00470 } 00471 else { 00472 coverageOther = coverageOther + numStatesCovered; 00473 avgOtherCoverage = avgOtherCoverage + coverage; 00474 numOther = numOther + 1; 00475 } 00476 if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/ 00477 fprintf(vis_stdout,"\n# States covered w.r.t. %s = %.0f, Percentage of Coverage = %f\n", 00478 array_fetch(char *,signalList,sigarr), numStatesCovered, coverage); 00479 nrOfUncoveredStatesString = Cmd_FlagReadByName("nr_uncoveredstates"); 00480 if(nrOfUncoveredStatesString == NIL(char)) 00481 nrOfUncoveredStates = 1; 00482 else 00483 nrOfUncoveredStates = atoi(nrOfUncoveredStatesString); 00484 if (numStatesCovered < numrchstates) { 00485 if ((numrchstates-numStatesCovered) < nrOfUncoveredStates) 00486 nrOfUncoveredStates = (int)(numrchstates-numStatesCovered); 00487 fprintf(vis_stdout,"#Printing reachable states NOT covered w.r.t. %s :\n",array_fetch(char *,signalList,sigarr)); 00488 for (prntStates = 0;prntStates<nrOfUncoveredStates;prntStates++){ 00489 fprintf(vis_stdout,"\n#State %d :\n",prntStates+1); 00490 uncoveredStates = mdd_and(modelCareStates,statesCovered,1,0); 00491 uncoveredStateCube = Mc_ComputeAMinterm(uncoveredStates, PSVarsC, mddMgrC); 00492 mdd_free(uncoveredStates); 00493 Mc_MintermPrint(uncoveredStateCube, PSVarsC, modelNetworkC); 00494 mdd_free(uncoveredStateCube); 00495 } 00496 } 00497 } 00498 } 00499 fprintf(vis_stdout,"\nTotal Coverage for all the Formulae\n"); 00500 fprintf(vis_stdout,"=====================================\n"); 00501 for (sigarr=0;sigarr<array_n(signalList);sigarr++) { 00502 mdd_t *statesCovered; 00503 double numStatesCovered; 00504 char *type; 00505 int sigType; 00506 00507 sigType = array_fetch(int, signalTypeList,sigarr); 00508 if (sigType == 1) 00509 type = "Primary Input"; 00510 else if (sigType == 0) 00511 type = "Primary Output"; 00512 else 00513 type = "Neither Primary output nor input"; 00514 00515 statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr); 00516 00517 numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00518 statesCovered,Fsm_FsmReadPresentStateVars(modelFsm)); 00519 coverage = (numStatesCovered / numrchstates) * 100; 00520 fprintf(vis_stdout,"# States covered w.r.t. %s(%s) = %.0f, Percentage of Coverage = %f\n",type, 00521 array_fetch(char *,signalList,sigarr), numStatesCovered, coverage); 00522 } 00523 fprintf(vis_stdout,"--There are %.0f covered states (using Hoskote et.al's implementation)\n",numtotcoveredstates); 00524 fprintf(vis_stdout,"--%.0f states covered by Primary Input Signals\n",coveragePI); 00525 fprintf(vis_stdout,"--%.0f states covered by Primary Ouput Signals\n",coveragePO); 00526 fprintf(vis_stdout,"--%.0f states covered by signals which are neither Primary input nor output Signals\n",coverageOther); 00527 fprintf(vis_stdout,"--There are %.0f reachable states\n",numrchstates); 00528 00529 coverage = (numtotcoveredstates / numrchstates) * 100; 00530 fprintf(vis_stdout,"Percentage of coverage (using Hoskote et.al's implementation)= %f\n ",coverage); 00531 avgCoverage = avgCoverage / array_n(signalList); 00532 fprintf(vis_stdout,"Average Percentage of coverage = %f\n",avgCoverage); 00533 if (numPI < 1) 00534 fprintf(vis_stdout,"No Primary Input signals\n"); 00535 else { 00536 avgPICoverage = avgPICoverage / numPI; 00537 fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgPICoverage); 00538 } 00539 if (numPO < 1) 00540 fprintf(vis_stdout,"No Primary Output signals\n"); 00541 else { 00542 avgPOCoverage = avgPOCoverage / numPO; 00543 fprintf(vis_stdout,"Average Percentage of coverage for Primary outputs = %f\n",avgPOCoverage); 00544 } 00545 if (numOther < 1) 00546 fprintf(vis_stdout,"No signals which are neither primary inputs nor outputs\n"); 00547 else { 00548 avgOtherCoverage = avgOtherCoverage / numOther; 00549 fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgOtherCoverage); 00550 } 00551 } 00552 else { 00553 fprintf(vis_stdout,"Reachable states = NIL !\n"); 00554 } 00555 } 00556 } 00557 00558 if (performCoverageImproved && (modelCareStatesArray != NIL(array_t))) { /* and no errors till now */ 00559 int sigarr; 00560 if (totalcoveredstates != NIL(mdd_t) && (modelCareStates != NIL(mdd_t))) { 00561 numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),totalcoveredstates,Fsm_FsmReadPresentStateVars(modelFsm)); 00562 } 00563 else { 00564 numtotcoveredstates = 0; 00565 } 00566 00567 if ((dcLevel == McDcLevelRch_c)||(dcLevel == McDcLevelRchFrontier_c)) { 00568 if (!mdd_lequal(totalcoveredstates, modelCareStates, 1, 1)) { 00569 (void)fprintf(vis_stdout, 00570 "** mc warning: Some of the covered states are not reachable\n"); 00571 } 00572 if (modelCareStates !=NIL(mdd_t)){ 00573 int sigType; 00574 00575 coveragePI = 0; 00576 coveragePO = 0; 00577 coverageOther = 0; 00578 numPI = 0; 00579 numPO = 0; 00580 numOther = 0; 00581 avgCoverage = 0; 00582 avgPICoverage = 0; 00583 avgPOCoverage = 0; 00584 avgOtherCoverage = 0; 00585 00586 numrchstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),modelCareStates,Fsm_FsmReadPresentStateVars(modelFsm)); 00587 if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/ 00588 fprintf(vis_stdout,"\nCoverage for all the Formulae w.r.t. all observable signals\n"); 00589 fprintf(vis_stdout,"=============================================================\n"); 00590 } 00591 for (sigarr=0;sigarr<array_n(signalList);sigarr++) { 00592 mdd_t *statesCovered, *uncoveredStateCube, *uncoveredStates; 00593 double numStatesCovered; 00594 char *nrOfUncoveredStatesString; 00595 int nrOfUncoveredStates, prntStates; /* nr of uncovered states that we output */ 00596 00597 Ntk_Network_t *modelNetworkC = Fsm_FsmReadNetwork(modelFsm); 00598 array_t *PSVarsC = Fsm_FsmReadPresentStateVars(modelFsm); 00599 mdd_manager *mddMgrC = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm)); 00600 00601 statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr); 00602 numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00603 statesCovered,Fsm_FsmReadPresentStateVars(modelFsm)); 00604 coverage = (numStatesCovered / numrchstates) * 100; 00605 avgCoverage = avgCoverage + coverage; 00606 sigType = array_fetch(int, signalTypeList,sigarr); 00607 if (sigType == 1) { 00608 coveragePI = coveragePI + numStatesCovered; 00609 avgPICoverage = avgPICoverage + coverage; 00610 numPI = numPI + 1; 00611 } 00612 else if (sigType == 0) { 00613 coveragePO = coveragePO + numStatesCovered; 00614 avgPOCoverage = avgPOCoverage + coverage; 00615 numPO = numPO + 1; 00616 } 00617 else { 00618 coverageOther = coverageOther + numStatesCovered; 00619 avgOtherCoverage = avgOtherCoverage + coverage; 00620 numOther = numOther + 1; 00621 } 00622 if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/ 00623 fprintf(vis_stdout,"\n# States covered w.r.t. %s = %.0f, Percentage of Coverage = %f\n", 00624 array_fetch(char *,signalList,sigarr), numStatesCovered, coverage); 00625 nrOfUncoveredStatesString = Cmd_FlagReadByName("nr_uncoveredstates"); 00626 if(nrOfUncoveredStatesString == NIL(char)) 00627 nrOfUncoveredStates = 1; 00628 else 00629 nrOfUncoveredStates = atoi(nrOfUncoveredStatesString); 00630 if (numStatesCovered < numrchstates) { 00631 if ((numrchstates-numStatesCovered) < nrOfUncoveredStates) 00632 nrOfUncoveredStates = (int)(numrchstates-numStatesCovered); 00633 fprintf(vis_stdout,"#Printing reachable states NOT covered w.r.t. %s :\n",array_fetch(char *,signalList,sigarr)); 00634 for (prntStates = 0;prntStates<nrOfUncoveredStates;prntStates++){ 00635 fprintf(vis_stdout,"\n#State %d :\n",prntStates+1); 00636 uncoveredStates = mdd_and(modelCareStates,statesCovered,1,0); 00637 uncoveredStateCube = Mc_ComputeAMinterm(uncoveredStates, PSVarsC, mddMgrC); 00638 mdd_free(uncoveredStates); 00639 Mc_MintermPrint(uncoveredStateCube, PSVarsC, modelNetworkC); 00640 mdd_free(uncoveredStateCube); 00641 } 00642 } 00643 } 00644 } 00645 fprintf(vis_stdout,"\nTotal Coverage for all the Formulae\n"); 00646 fprintf(vis_stdout,"=====================================\n"); 00647 for (sigarr=0;sigarr<array_n(signalList);sigarr++) { 00648 mdd_t *statesCovered; 00649 double numStatesCovered; 00650 char *type; 00651 int sigType; 00652 sigType = array_fetch(int, signalTypeList,sigarr); 00653 if (sigType == 1) 00654 type = "Primary Input"; 00655 else if (sigType == 0) 00656 type = "Primary Output"; 00657 else 00658 type = "Neither Primary output nor input"; 00659 statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr); 00660 numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), 00661 statesCovered,Fsm_FsmReadPresentStateVars(modelFsm)); 00662 coverage = (numStatesCovered / numrchstates) * 100; 00663 fprintf(vis_stdout,"# States covered w.r.t. %s(%s) = %.0f, Percentage of Coverage = %f\n",type, 00664 array_fetch(char *,signalList,sigarr), numStatesCovered, coverage); 00665 } 00666 fprintf(vis_stdout,"--There are %.0f covered states (using improved coverage implementation)\n",numtotcoveredstates); 00667 fprintf(vis_stdout,"--%.0f states covered by Primary Input Signals\n",coveragePI); 00668 fprintf(vis_stdout,"--%.0f states covered by Primary Ouput Signals\n",coveragePO); 00669 fprintf(vis_stdout,"--%.0f states covered by signals which are neither Primary input nor output Signals\n",coverageOther); 00670 fprintf(vis_stdout,"--There are %.0f reachable states\n",numrchstates); 00671 00672 coverage = (numtotcoveredstates / numrchstates) * 100; 00673 fprintf(vis_stdout,"Percentage of coverage (using improved coverage implementation)= %f\n ",coverage); 00674 avgCoverage = avgCoverage / array_n(signalList); 00675 fprintf(vis_stdout,"Average Percentage of coverage = %f\n",avgCoverage); 00676 if (numPI < 1) 00677 fprintf(vis_stdout,"No Primary Input signals\n"); 00678 else { 00679 avgPICoverage = avgPICoverage / numPI; 00680 fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgPICoverage); 00681 } 00682 if (numPO < 1) 00683 fprintf(vis_stdout,"No Primary Output signals\n"); 00684 else { 00685 avgPOCoverage = avgPOCoverage / numPO; 00686 fprintf(vis_stdout,"Average Percentage of coverage for Primary outputs = %f\n",avgPOCoverage); 00687 } 00688 if (numOther < 1) 00689 fprintf(vis_stdout,"No signals which are not primary\n"); 00690 else { 00691 avgOtherCoverage = avgOtherCoverage / numOther; 00692 fprintf(vis_stdout,"Average Percentage of coverage for signals which are not primary = %f\n",avgOtherCoverage); 00693 } 00694 } 00695 else { 00696 fprintf(vis_stdout,"Reachable states = NIL !\n"); 00697 } 00698 } 00699 } 00700 } /* McPrintCoverageSummary */ 00701 00702 /*---------------------------------------------------------------------------*/ 00703 /* Definition of static functions */ 00704 /*---------------------------------------------------------------------------*/ 00705 00706 00720 static mdd_t * 00721 CoveredStatesHoskote( 00722 mdd_t *startstates_old, 00723 Fsm_Fsm_t *fsm, 00724 Ctlp_Formula_t *OrigFormula, 00725 mdd_t *fairStates, 00726 Fsm_Fairness_t *fairCondition, 00727 array_t *careStatesArray, 00728 Mc_EarlyTermination_t *earlyTermination, 00729 Fsm_HintsArray_t *hintsArray, 00730 Mc_GuidedSearch_t hintType, 00731 Mc_VerbosityLevel verbosity, 00732 Mc_DcLevel dcLevel, 00733 int buildOnionRing, 00734 Mc_GSHScheduleType GSHschedule, 00735 array_t *signalList, 00736 array_t *statesCoveredList, 00737 array_t *newCoveredStatesList, 00738 array_t *statesToRemoveList) 00739 { 00740 mdd_t *Covstates1, *temp1, *temp2; 00741 mdd_t *Covstates2; 00742 mdd_t *result; 00743 mdd_t *travstates; 00744 mdd_t *frstrchstates; 00745 00746 mdd_t *startstates; 00747 00748 Ctlp_FormulaType formulaType; 00749 Ctlp_Formula_t *rightFormula, *leftFormula, *tmp_formula, *existFormula; 00750 double numresultstates; /* used for debugging <NJ> */ 00751 00752 startstates = mdd_and(startstates_old,fairStates,1,1); 00753 00754 if (mdd_is_tautology(startstates,0)) { 00755 if (verbosity > McVerbosityNone_c) 00756 fprintf(vis_stdout, 00757 "\n--Startstates are down to zero. Coverage is hence zero.\n"); 00758 result = mdd_zero(Fsm_FsmReadMddManager(fsm)); 00759 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 00760 Fsm_FsmReadPresentStateVars(fsm)); 00761 mdd_free(startstates); 00762 return result; 00763 } 00764 if (Ctlp_FormulaTestIsQuantifierFree(OrigFormula)) { 00765 /*propositional formula*/ 00766 result = CoveragePropositional(startstates, fsm, OrigFormula, fairStates, 00767 fairCondition, careStatesArray, 00768 earlyTermination, hintsArray, hintType, 00769 verbosity, dcLevel,buildOnionRing, 00770 GSHschedule, signalList, statesCoveredList, 00771 newCoveredStatesList, statesToRemoveList); 00772 temp1 = result; 00773 result = mdd_and(temp1,fairStates,1,1); 00774 mdd_free(temp1); 00775 mdd_free(startstates); 00776 return result; 00777 } 00778 formulaType = Ctlp_FormulaReadType(OrigFormula); 00779 switch (formulaType) { 00780 case Ctlp_EG_c: 00781 case Ctlp_EF_c: 00782 case Ctlp_EU_c: 00783 case Ctlp_FwdU_c: 00784 case Ctlp_FwdG_c: 00785 case Ctlp_EY_c: 00786 case Ctlp_EH_c: 00787 case Ctlp_Cmp_c: 00788 case Ctlp_EX_c: 00789 case Ctlp_Init_c: { 00790 fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL,\n"); 00791 fprintf(vis_stdout,"** can't compute coverage of : "); 00792 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 00793 fprintf(vis_stdout,"\n"); 00794 result = mdd_zero(Fsm_FsmReadMddManager(fsm)); 00795 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,Fsm_FsmReadPresentStateVars(fsm)); 00796 mdd_free(startstates); 00797 return result; 00798 break; 00799 } 00800 case Ctlp_AX_c:{ 00801 temp1 = Mc_FsmEvaluateEYFormula(fsm, startstates, fairStates, careStatesArray, verbosity, dcLevel); 00802 Covstates1 = mdd_and(temp1,fairStates,1,1); 00803 mdd_free(temp1); 00804 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 00805 result = CoveredStatesHoskote(Covstates1, fsm, leftFormula, fairStates, 00806 fairCondition, careStatesArray, 00807 earlyTermination, hintsArray, 00808 hintType, verbosity, dcLevel, buildOnionRing, 00809 GSHschedule, signalList, statesCoveredList, 00810 newCoveredStatesList, statesToRemoveList); 00811 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 00812 Fsm_FsmReadPresentStateVars(fsm)); 00813 mdd_free(Covstates1); 00814 temp1 = result; 00815 result = mdd_and(temp1,fairStates,1,1); 00816 mdd_free(temp1); 00817 mdd_free(startstates); 00818 return result; 00819 break; 00820 } 00821 case Ctlp_AG_c:{ 00822 mdd_t *initStates; 00823 double numststates; 00824 initStates = Fsm_FsmComputeInitialStates(fsm); 00825 temp1 = mdd_one(Fsm_FsmReadMddManager(fsm)); 00826 if (mdd_equal_mod_care_set_array(startstates,initStates,careStatesArray)) { 00827 if (verbosity > McVerbosityNone_c) 00828 fprintf(vis_stdout,"\nUsing the reachable states already computed..."); 00829 temp2 = Fsm_FsmComputeReachableStates(fsm, 0, 1, 0, 0, 0, 0, 0, 00830 Fsm_Rch_Default_c, 0, 0, 00831 NIL(array_t), FALSE, NIL(array_t)); 00832 } else 00833 temp2 = Mc_FsmEvaluateFwdUFormula(fsm, startstates, temp1, fairStates, 00834 careStatesArray, NIL(array_t), 00835 verbosity, dcLevel); 00836 mdd_free(initStates); 00837 numststates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),startstates, 00838 Fsm_FsmReadPresentStateVars(fsm)); 00839 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),temp2, 00840 Fsm_FsmReadPresentStateVars(fsm)); 00841 mdd_free(temp1); 00842 Covstates1 = mdd_and(temp2,fairStates,1,1); 00843 mdd_free(temp2); 00844 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 00845 result = CoveredStatesHoskote(Covstates1, fsm, leftFormula, fairStates, 00846 fairCondition, careStatesArray, 00847 earlyTermination, hintsArray, hintType, 00848 verbosity, dcLevel, buildOnionRing, 00849 GSHschedule, signalList, statesCoveredList, 00850 newCoveredStatesList, statesToRemoveList); 00851 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 00852 Fsm_FsmReadPresentStateVars(fsm)); 00853 mdd_free(Covstates1); 00854 temp1 = result; 00855 result = mdd_and(temp1,fairStates,1,1); 00856 mdd_free(temp1); 00857 mdd_free(startstates); 00858 return result; 00859 break; 00860 } 00861 case Ctlp_AF_c:{ 00862 tmp_formula = OrigFormula; 00863 OrigFormula = Ctlp_FormulaConvertAFtoAU(tmp_formula); 00864 if (verbosity > McVerbosityNone_c) { 00865 fprintf(vis_stdout,"Converting formula from\n"); 00866 Ctlp_FormulaPrint(vis_stdout,tmp_formula); 00867 fprintf(vis_stdout,"\nto\n"); 00868 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 00869 fprintf(vis_stdout,"\n"); 00870 } 00871 #if 0 00872 Ctlp_FormulaFree(tmp_formula); 00873 formulaType = Ctlp_AU_c; 00874 #endif 00875 /* convert to AFp to A (TRUE) U p and then step thru to do coverage 00876 for AU computation below*/ 00877 } 00878 case Ctlp_AU_c:{ 00879 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 00880 rightFormula = Ctlp_FormulaReadRightChild(OrigFormula); 00881 travstates = traverse(fsm, fairStates, fairCondition, careStatesArray, 00882 earlyTermination, hintsArray, hintType, verbosity, 00883 dcLevel, buildOnionRing, GSHschedule, startstates, 00884 leftFormula,rightFormula); 00885 if (verbosity > McVerbosityNone_c) { 00886 fprintf(vis_stdout,"\n---Computing coverage for LHS of U formula i.e: "); 00887 Ctlp_FormulaPrint(vis_stdout,leftFormula); 00888 fprintf(vis_stdout, 00889 "\n------------------------------------------------\n"); 00890 } 00891 Covstates1 = CoveredStatesHoskote(travstates, fsm, leftFormula, fairStates, 00892 fairCondition, careStatesArray, 00893 earlyTermination, hintsArray, hintType, 00894 verbosity, dcLevel, buildOnionRing, 00895 GSHschedule, signalList, 00896 statesCoveredList, newCoveredStatesList, 00897 statesToRemoveList); 00898 mdd_free(travstates); 00899 frstrchstates = firstReached(fsm, fairStates, fairCondition, 00900 careStatesArray, earlyTermination, hintsArray, 00901 hintType, verbosity, dcLevel, buildOnionRing, 00902 GSHschedule, startstates, rightFormula); 00903 if (verbosity > McVerbosityNone_c) { 00904 fprintf(vis_stdout,"\n---Computing coverage for RHS of U formula i.e: "); 00905 Ctlp_FormulaPrint(vis_stdout,rightFormula); 00906 fprintf(vis_stdout, 00907 "\n------------------------------------------------\n"); 00908 } 00909 Covstates2 = CoveredStatesHoskote(frstrchstates, fsm, rightFormula, 00910 fairStates, fairCondition, 00911 careStatesArray, earlyTermination, 00912 hintsArray, hintType, verbosity, dcLevel, 00913 buildOnionRing, GSHschedule, signalList, 00914 statesCoveredList, newCoveredStatesList, 00915 statesToRemoveList); 00916 mdd_free(frstrchstates); 00917 result = mdd_or(Covstates1,Covstates2,1,1); 00918 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 00919 Fsm_FsmReadPresentStateVars(fsm)); 00920 mdd_free(Covstates1); 00921 mdd_free(Covstates2); 00922 temp1 = result; 00923 result = mdd_and(temp1,fairStates,1,1); 00924 if (formulaType == Ctlp_AF_c) 00925 Ctlp_FormulaFree(OrigFormula); 00926 mdd_free(temp1); 00927 mdd_free(startstates); 00928 return result; 00929 break; 00930 } 00931 case Ctlp_AND_c:{ 00932 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 00933 if (verbosity > McVerbosityNone_c) { 00934 fprintf(vis_stdout,"---Computing coverage for LHS sub-formula: "); 00935 Ctlp_FormulaPrint(vis_stdout,leftFormula); 00936 fprintf(vis_stdout, 00937 "\n------------------------------------------------\n"); 00938 } 00939 Covstates1 = CoveredStatesHoskote(startstates,fsm, leftFormula, fairStates, 00940 fairCondition, careStatesArray, 00941 earlyTermination, hintsArray, hintType, 00942 verbosity, dcLevel, buildOnionRing, 00943 GSHschedule, signalList, 00944 statesCoveredList, newCoveredStatesList, 00945 statesToRemoveList); 00946 rightFormula = Ctlp_FormulaReadRightChild(OrigFormula); 00947 if (verbosity > McVerbosityNone_c) { 00948 fprintf(vis_stdout,"---Computing coverage for RHS sub-formula: "); 00949 Ctlp_FormulaPrint(vis_stdout,rightFormula); 00950 fprintf(vis_stdout, 00951 "\n------------------------------------------------\n"); 00952 } 00953 Covstates2 = CoveredStatesHoskote(startstates,fsm, rightFormula, 00954 fairStates, fairCondition, 00955 careStatesArray, earlyTermination, 00956 hintsArray, hintType, verbosity, dcLevel, 00957 buildOnionRing,GSHschedule, signalList, 00958 statesCoveredList, newCoveredStatesList, 00959 statesToRemoveList); 00960 result = mdd_or(Covstates1, Covstates2, 1, 1); 00961 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 00962 Fsm_FsmReadPresentStateVars(fsm)); 00963 mdd_free(Covstates1); 00964 mdd_free(Covstates2); 00965 temp1 = result; 00966 result = mdd_and(temp1,fairStates,1,1); 00967 mdd_free(temp1); 00968 mdd_free(startstates); 00969 return result; 00970 break; 00971 } 00972 case Ctlp_THEN_c:{ /*f1 -> f2 = !f2 -> !f1*/ 00973 mdd_t *nextstartstates, *Tb; 00974 00975 if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadLeftChild(OrigFormula))) { /*if f1 is propositional*/ 00976 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 00977 rightFormula = Ctlp_FormulaReadRightChild(OrigFormula); 00978 } else if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadRightChild(OrigFormula))) { /*if f2 is propositional*/ 00979 /* Convert f1->f2 to !f2->!f1 */ 00980 leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula)); 00981 rightFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula)); 00982 } else { /*neither are propositional*/ 00983 fprintf(vis_stdout,"\nCan't compute coverage of implications where neither side is propositional\n"); 00984 fprintf(vis_stdout,"Could not compute coverage of :"); 00985 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 00986 result = mdd_zero(Fsm_FsmReadMddManager(fsm)); 00987 mdd_free(startstates); 00988 return result; 00989 } 00990 existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula); 00991 Tb = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates, 00992 fairCondition, careStatesArray, 00993 earlyTermination, hintsArray, hintType, 00994 verbosity, dcLevel, buildOnionRing,GSHschedule); 00995 Ctlp_FormulaFree(existFormula); 00996 nextstartstates = mdd_and(startstates, Tb,1,1); 00997 mdd_free(Tb); 00998 Covstates1 = CoveredStatesHoskote(nextstartstates,fsm, rightFormula, 00999 fairStates, fairCondition, 01000 careStatesArray, earlyTermination, 01001 hintsArray, hintType, verbosity, dcLevel, 01002 buildOnionRing,GSHschedule, signalList, 01003 statesCoveredList, newCoveredStatesList, 01004 statesToRemoveList); 01005 mdd_free(nextstartstates); 01006 mdd_free(startstates); 01007 return Covstates1; 01008 break; 01009 } 01010 case Ctlp_XOR_c: { 01011 tmp_formula = Ctlp_FormulaConvertXORtoOR(OrigFormula); 01012 if (verbosity > McVerbosityNone_c) { 01013 fprintf(vis_stdout,"\n--Converting XOR to AND and OR from:\n"); 01014 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01015 fprintf(vis_stdout,"\nto\n"); 01016 Ctlp_FormulaPrint(vis_stdout, tmp_formula); 01017 fprintf(vis_stdout,"\n"); 01018 } 01019 result = CoveredStatesHoskote(startstates, fsm, tmp_formula, fairStates, 01020 fairCondition, careStatesArray, 01021 earlyTermination, hintsArray, 01022 hintType, verbosity, dcLevel,buildOnionRing, 01023 GSHschedule, signalList, statesCoveredList, 01024 newCoveredStatesList, statesToRemoveList); 01025 mdd_free(startstates); 01026 return result; 01027 break; 01028 } 01029 case Ctlp_EQ_c: { 01030 tmp_formula = Ctlp_FormulaConvertEQtoOR(OrigFormula); 01031 if (verbosity > McVerbosityNone_c) { 01032 fprintf(vis_stdout,"\n--Converting EQ to AND and OR from:\n"); 01033 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01034 fprintf(vis_stdout,"\nto\n"); 01035 Ctlp_FormulaPrint(vis_stdout, tmp_formula); 01036 fprintf(vis_stdout,"\n"); 01037 } 01038 result = CoveredStatesHoskote(startstates, fsm, tmp_formula, fairStates, 01039 fairCondition, careStatesArray, 01040 earlyTermination, hintsArray, 01041 hintType, verbosity, dcLevel,buildOnionRing, 01042 GSHschedule, signalList, statesCoveredList, 01043 newCoveredStatesList, statesToRemoveList); 01044 mdd_free(startstates); 01045 return result; 01046 break; 01047 } 01048 case Ctlp_OR_c:{ /*f1+f2 = !f1 -> f2 = !f2 -> f1*/ 01049 mdd_t *nextstartstates, *Tb; 01050 01051 if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadLeftChild(OrigFormula))) { /*if f1 is propositional*/ 01052 /* Convert f1+f2 to !f1->f2 */ 01053 leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula)); 01054 rightFormula = Ctlp_FormulaReadRightChild(OrigFormula); 01055 } else if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadRightChild(OrigFormula))) { /*if f2 is propositional*/ 01056 /* Convert f1+f2 to !f2->f1 */ 01057 leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula)); 01058 rightFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 01059 } else { /*neither are propositional*/ 01060 fprintf(vis_stdout,"\nCan't compute coverage of disjunctions where neither side is propositional\n"); 01061 fprintf(vis_stdout,"Could not compute coverage of :"); 01062 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01063 result = mdd_zero(Fsm_FsmReadMddManager(fsm)); 01064 mdd_free(startstates); 01065 return result; 01066 } 01067 existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula); 01068 Tb = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates, 01069 fairCondition, careStatesArray, 01070 earlyTermination, hintsArray, hintType, 01071 verbosity, dcLevel, buildOnionRing,GSHschedule); 01072 Ctlp_FormulaFree(existFormula); 01073 Ctlp_FormulaFree(leftFormula); 01074 nextstartstates = mdd_and(startstates, Tb,1,1); 01075 mdd_free(Tb); 01076 Covstates1 = CoveredStatesHoskote(nextstartstates,fsm, rightFormula, 01077 fairStates, fairCondition, 01078 careStatesArray, earlyTermination, 01079 hintsArray, hintType, verbosity, dcLevel, 01080 buildOnionRing,GSHschedule, signalList, 01081 statesCoveredList, newCoveredStatesList, 01082 statesToRemoveList); 01083 mdd_free(nextstartstates); 01084 mdd_free(startstates); 01085 return Covstates1; 01086 break; 01087 } 01088 case Ctlp_NOT_c:{ /*include code for checking for 2 NOTs*/ 01089 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 01090 if (!(Ctlp_FormulaTestIsQuantifierFree(leftFormula))) { 01091 tmp_formula = Ctlp_FormulaPushNegation(leftFormula); 01092 if (verbosity > McVerbosityNone_c) { 01093 fprintf(vis_stdout,"\n--Pushing down negation one level. Converting formula from:\n"); 01094 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01095 fprintf(vis_stdout,"\nto\n"); 01096 Ctlp_FormulaPrint(vis_stdout,tmp_formula); 01097 fprintf(vis_stdout,"\n"); 01098 } 01099 Covstates1 = CoveredStatesHoskote(startstates, fsm, tmp_formula, 01100 fairStates, fairCondition, 01101 careStatesArray, earlyTermination, 01102 hintsArray, hintType, verbosity, 01103 dcLevel, buildOnionRing,GSHschedule, 01104 signalList, statesCoveredList, 01105 newCoveredStatesList, 01106 statesToRemoveList); 01107 Ctlp_FormulaFree(tmp_formula); 01108 result = mdd_and(Covstates1,fairStates,1,1); 01109 mdd_free(Covstates1); 01110 mdd_free(startstates); 01111 return result; 01112 #if 0 01113 fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL\n"); 01114 fprintf(vis_stdout,"** can't compute coverage of : "); 01115 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01116 fprintf(vis_stdout,"\n"); 01117 mdd_free(startstates); 01118 return mdd_zero(Fsm_FsmReadMddManager(fsm)); 01119 #endif 01120 } else { /*this part of the code is now never executed*/ 01121 fprintf(vis_stdout, "\n****Error, Should not have reached here\n"); 01122 mdd_free(startstates); 01123 return mdd_zero(Fsm_FsmReadMddManager(fsm)); 01124 } 01125 break; 01126 } 01127 case Ctlp_TRUE_c: 01128 case Ctlp_FALSE_c: { 01129 if (verbosity > McVerbosityNone_c) 01130 fprintf(vis_stdout,"No observable signal, hence no coverage\n"); 01131 result = mdd_zero(Fsm_FsmReadMddManager(fsm)); 01132 mdd_free(startstates); 01133 return result; 01134 break; 01135 } 01136 case Ctlp_ID_c:{ /*should not reach here*/ 01137 fprintf(vis_stdout, "\n****Error, Should not have reached here\n"); 01138 mdd_free(startstates); 01139 return mdd_zero(Fsm_FsmReadMddManager(fsm)); 01140 break; 01141 } 01142 default: 01143 fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n"); 01144 break; 01145 } 01146 assert(0); 01147 return NIL(mdd_t); 01148 01149 } /* CoveredStatesHoskote */ 01150 01151 01164 static mdd_t * 01165 CoveredStatesImproved( 01166 mdd_t *startstates_old, 01167 Fsm_Fsm_t *fsm, 01168 Ctlp_Formula_t *OrigFormula, 01169 mdd_t *fairStates, 01170 Fsm_Fairness_t *fairCondition, 01171 array_t *careStatesArray, 01172 Mc_EarlyTermination_t *earlyTermination, 01173 Fsm_HintsArray_t *hintsArray, 01174 Mc_GuidedSearch_t hintType, 01175 Mc_VerbosityLevel verbosity, 01176 Mc_DcLevel dcLevel, 01177 int buildOnionRing, 01178 Mc_GSHScheduleType GSHschedule, 01179 array_t *signalList, 01180 array_t *statesCoveredList, 01181 array_t *newCoveredStatesList, 01182 array_t *statesToRemoveList) 01183 { 01184 mdd_t *Covstates1, *temp1, *temp2; 01185 mdd_t *Covstates2; 01186 mdd_t *result; 01187 mdd_t *travstates; 01188 mdd_t *frstrchstates; 01189 01190 mdd_t *startstates; 01191 01192 Ctlp_FormulaType formulaType; 01193 Ctlp_Formula_t *rightFormula, *leftFormula, *tmp_formula, *existFormula; 01194 double numresultstates; /* used for debugging <NJ> */ 01195 01196 startstates = mdd_and(startstates_old,fairStates,1,1); 01197 01198 if (mdd_is_tautology(startstates,0)) { 01199 if (verbosity > McVerbosityNone_c) 01200 fprintf(vis_stdout, 01201 "\n--Startstates are down to zero. Coverage is hence zero.\n"); 01202 result = mdd_zero(Fsm_FsmReadMddManager(fsm)); 01203 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 01204 Fsm_FsmReadPresentStateVars(fsm)); 01205 mdd_free(startstates); 01206 return result; 01207 } 01208 if (Ctlp_FormulaTestIsQuantifierFree(OrigFormula)) { 01209 /* propositional formula */ 01210 result = CoveragePropositional(startstates, fsm, OrigFormula, fairStates, 01211 fairCondition, careStatesArray, 01212 earlyTermination, hintsArray, hintType, 01213 verbosity, dcLevel,buildOnionRing, 01214 GSHschedule, signalList, statesCoveredList, 01215 newCoveredStatesList, statesToRemoveList); 01216 temp1 = result; 01217 result = mdd_and(temp1,fairStates,1,1); 01218 mdd_free(temp1); 01219 mdd_free(startstates); 01220 return result; 01221 } 01222 formulaType = Ctlp_FormulaReadType(OrigFormula); 01223 switch (formulaType) { 01224 case Ctlp_EG_c: {/*EGp = p * EX(EGp) => C(So,EGp) = C(So,p) */ 01225 if (verbosity > McVerbosityNone_c) { 01226 fprintf(vis_stdout,"\n--Computing underapproximation for EG formula:\n"); 01227 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01228 fprintf(vis_stdout,"\n"); 01229 } 01230 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 01231 result = CoveredStatesImproved(startstates, fsm, leftFormula, fairStates, 01232 fairCondition, careStatesArray, 01233 earlyTermination, hintsArray, hintType, 01234 verbosity, dcLevel,buildOnionRing, 01235 GSHschedule, signalList, statesCoveredList, 01236 newCoveredStatesList, statesToRemoveList); 01237 temp1 = result; 01238 result = mdd_and(temp1,fairStates,1,1); 01239 mdd_free(temp1); 01240 mdd_free(startstates); 01241 return result; 01242 break; 01243 } 01244 case Ctlp_EF_c: { 01245 if (verbosity > McVerbosityNone_c) { 01246 fprintf(vis_stdout,"\n--Computing underapproximation for EF formula:\n"); 01247 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01248 fprintf(vis_stdout,"\n"); 01249 } 01250 tmp_formula = Ctlp_FormulaConvertEFtoOR(OrigFormula); 01251 result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates, 01252 fairCondition, careStatesArray, 01253 earlyTermination, hintsArray, 01254 hintType, verbosity, dcLevel,buildOnionRing, 01255 GSHschedule, signalList, statesCoveredList, 01256 newCoveredStatesList, statesToRemoveList); 01257 Ctlp_FormulaFree(tmp_formula); 01258 mdd_free(startstates); 01259 return result; 01260 break; 01261 } 01262 case Ctlp_EU_c: { 01263 if (verbosity > McVerbosityNone_c) { 01264 fprintf(vis_stdout,"\n--Computing underapproximation for EU formula: "); 01265 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01266 fprintf(vis_stdout,"\n"); 01267 } 01268 tmp_formula = Ctlp_FormulaConvertEUtoOR(OrigFormula); 01269 result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates, 01270 fairCondition, careStatesArray, 01271 earlyTermination, hintsArray, hintType, 01272 verbosity, dcLevel,buildOnionRing, 01273 GSHschedule, signalList, statesCoveredList, 01274 newCoveredStatesList,statesToRemoveList); 01275 mdd_free(startstates); 01276 return result; 01277 break; 01278 } 01279 case Ctlp_FwdU_c: 01280 case Ctlp_FwdG_c: 01281 case Ctlp_EY_c: 01282 case Ctlp_EH_c: 01283 case Ctlp_Cmp_c: 01284 case Ctlp_EX_c: 01285 case Ctlp_Init_c: { 01286 fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL,\n"); 01287 fprintf(vis_stdout,"** can't compute coverage of : "); 01288 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01289 fprintf(vis_stdout,"\n"); 01290 result = mdd_zero(Fsm_FsmReadMddManager(fsm)); 01291 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 01292 Fsm_FsmReadPresentStateVars(fsm)); 01293 mdd_free(startstates); 01294 return result; 01295 break; 01296 } 01297 case Ctlp_AX_c:{ 01298 temp1 = Mc_FsmEvaluateEYFormula(fsm, startstates, fairStates, careStatesArray, verbosity, dcLevel); 01299 Covstates1 = mdd_and(temp1,fairStates,1,1); 01300 mdd_free(temp1); 01301 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 01302 result = CoveredStatesImproved(Covstates1, fsm, leftFormula, fairStates, 01303 fairCondition, careStatesArray, 01304 earlyTermination, hintsArray, hintType, 01305 verbosity, dcLevel,buildOnionRing, 01306 GSHschedule, signalList, statesCoveredList, 01307 newCoveredStatesList, statesToRemoveList); 01308 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 01309 Fsm_FsmReadPresentStateVars(fsm)); 01310 mdd_free(Covstates1); 01311 temp1 = result; 01312 result = mdd_and(temp1,fairStates,1,1); 01313 mdd_free(temp1); 01314 mdd_free(startstates); 01315 return result; 01316 break; 01317 } 01318 case Ctlp_AG_c:{ 01319 double numststates; 01320 mdd_t *initStates; 01321 initStates = Fsm_FsmComputeInitialStates(fsm); 01322 temp1 = mdd_one(Fsm_FsmReadMddManager(fsm)); 01323 if (mdd_equal_mod_care_set_array(startstates,initStates,careStatesArray)) { 01324 if (verbosity > McVerbosityNone_c) 01325 fprintf(vis_stdout,"\nUsing the reachable states already computed..."); 01326 temp2 = Fsm_FsmComputeReachableStates(fsm, 0, 1, 0, 0, 0, 0, 0, 01327 Fsm_Rch_Default_c, 0, 0, 01328 NIL(array_t), FALSE, NIL(array_t)); 01329 } else 01330 temp2 = Mc_FsmEvaluateFwdUFormula(fsm, startstates, temp1, fairStates, 01331 careStatesArray, NIL(array_t), 01332 verbosity, dcLevel); 01333 mdd_free(initStates); 01334 #if 0 01335 temp2 = McForwardReachable(fsm, startstates, temp1, fairStates, 01336 careStatesArray, NIL(array_t),verbosity, 01337 dcLevel); 01338 #endif 01339 numststates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),startstates, 01340 Fsm_FsmReadPresentStateVars(fsm)); 01341 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),temp2, 01342 Fsm_FsmReadPresentStateVars(fsm)); 01343 #if 0 01344 fprintf(vis_stdout,"\nNum of forward reachable states from %.0f startstates = %.0f\n",numststates,numresultstates); 01345 #endif 01346 mdd_free(temp1); 01347 Covstates1 = mdd_and(temp2,fairStates,1,1); 01348 mdd_free(temp2); 01349 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 01350 result = CoveredStatesImproved(Covstates1, fsm, leftFormula, fairStates, 01351 fairCondition, careStatesArray, 01352 earlyTermination, hintsArray, hintType, 01353 verbosity, dcLevel, buildOnionRing, 01354 GSHschedule, signalList, statesCoveredList, 01355 newCoveredStatesList, statesToRemoveList); 01356 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 01357 Fsm_FsmReadPresentStateVars(fsm)); 01358 mdd_free(Covstates1); 01359 temp1 = result; 01360 result = mdd_and(temp1,fairStates,1,1); 01361 mdd_free(temp1); 01362 mdd_free(startstates); 01363 return result; 01364 break; 01365 } 01366 case Ctlp_AF_c:{ 01367 tmp_formula = OrigFormula; 01368 OrigFormula = Ctlp_FormulaConvertAFtoAU(tmp_formula); 01369 if (verbosity > McVerbosityNone_c) { 01370 fprintf(vis_stdout,"Converting formula from\n"); 01371 Ctlp_FormulaPrint(vis_stdout,tmp_formula); 01372 fprintf(vis_stdout,"\nto\n"); 01373 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01374 fprintf(vis_stdout,"\n"); 01375 } 01376 #if 0 01377 Ctlp_FormulaFree(tmp_formula); 01378 formulaType = Ctlp_AU_c; 01379 #endif 01380 /* convert to AFp to A (TRUE) U p and then step thru to do coverage 01381 for AU computation below*/ 01382 } 01383 case Ctlp_AU_c:{ 01384 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 01385 rightFormula = Ctlp_FormulaReadRightChild(OrigFormula); 01386 tmp_formula = Ctlp_FormulaCreate(Ctlp_OR_c,leftFormula,rightFormula); 01387 CtlpFormulaIncrementRefCount(leftFormula); 01388 CtlpFormulaIncrementRefCount(rightFormula); 01389 travstates = traverse(fsm, fairStates, fairCondition, careStatesArray, 01390 earlyTermination, hintsArray, hintType, verbosity, 01391 dcLevel, buildOnionRing, GSHschedule, startstates, 01392 leftFormula, rightFormula); 01393 if (verbosity > McVerbosityNone_c) { 01394 fprintf(vis_stdout,"\n---Computing coverage for LHS of U formula i.e: "); 01395 Ctlp_FormulaPrint(vis_stdout,leftFormula); 01396 fprintf(vis_stdout, 01397 "\n------------------------------------------------\n"); 01398 } 01399 Covstates1 = CoveredStatesImproved(travstates, fsm, tmp_formula, 01400 fairStates, fairCondition, 01401 careStatesArray, earlyTermination, 01402 hintsArray, hintType, verbosity, 01403 dcLevel, buildOnionRing, GSHschedule, 01404 signalList, statesCoveredList, 01405 newCoveredStatesList, 01406 statesToRemoveList); 01407 mdd_free(travstates); 01408 Ctlp_FormulaFree(tmp_formula); 01409 frstrchstates = firstReached(fsm, fairStates, fairCondition, 01410 careStatesArray, earlyTermination, hintsArray, 01411 hintType, verbosity, dcLevel, buildOnionRing, 01412 GSHschedule,startstates,rightFormula); 01413 if (verbosity > McVerbosityNone_c) { 01414 fprintf(vis_stdout,"\n---Computing coverage for RHS of U formula i.e: "); 01415 Ctlp_FormulaPrint(vis_stdout,rightFormula); 01416 fprintf(vis_stdout, 01417 "\n------------------------------------------------\n"); 01418 } 01419 Covstates2 = CoveredStatesImproved(frstrchstates, fsm, rightFormula, 01420 fairStates, fairCondition, 01421 careStatesArray, earlyTermination, 01422 hintsArray, hintType, verbosity, 01423 dcLevel, buildOnionRing, GSHschedule, 01424 signalList, statesCoveredList, 01425 newCoveredStatesList, 01426 statesToRemoveList); 01427 mdd_free(frstrchstates); 01428 result = mdd_or(Covstates1,Covstates2,1,1); 01429 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 01430 Fsm_FsmReadPresentStateVars(fsm)); 01431 mdd_free(Covstates1); 01432 mdd_free(Covstates2); 01433 temp1 = result; 01434 result = mdd_and(temp1,fairStates,1,1); 01435 if (formulaType == Ctlp_AF_c) 01436 Ctlp_FormulaFree(OrigFormula); 01437 mdd_free(temp1); 01438 mdd_free(startstates); 01439 return result; 01440 break; 01441 } 01442 case Ctlp_AND_c:{ 01443 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 01444 if (verbosity > McVerbosityNone_c) { 01445 fprintf(vis_stdout,"\n---Computing coverage for LHS sub-formula: "); 01446 Ctlp_FormulaPrint(vis_stdout,leftFormula); 01447 fprintf(vis_stdout, 01448 "\n------------------------------------------------\n"); 01449 } 01450 Covstates1 = CoveredStatesImproved(startstates,fsm, leftFormula, 01451 fairStates, fairCondition, 01452 careStatesArray, earlyTermination, 01453 hintsArray, hintType, verbosity, 01454 dcLevel, buildOnionRing,GSHschedule, 01455 signalList, statesCoveredList, 01456 newCoveredStatesList, 01457 statesToRemoveList); 01458 rightFormula = Ctlp_FormulaReadRightChild(OrigFormula); 01459 if (verbosity > McVerbosityNone_c) { 01460 fprintf(vis_stdout,"\n---Computing coverage for RHS sub-formula: "); 01461 Ctlp_FormulaPrint(vis_stdout,rightFormula); 01462 fprintf(vis_stdout, 01463 "\n------------------------------------------------\n"); 01464 } 01465 Covstates2 = CoveredStatesImproved(startstates,fsm, rightFormula, 01466 fairStates, fairCondition, 01467 careStatesArray, earlyTermination, 01468 hintsArray, hintType, verbosity, 01469 dcLevel, buildOnionRing,GSHschedule, 01470 signalList, statesCoveredList, 01471 newCoveredStatesList, 01472 statesToRemoveList); 01473 result = mdd_or(Covstates1,Covstates2,1,1); 01474 numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result, 01475 Fsm_FsmReadPresentStateVars(fsm)); 01476 mdd_free(Covstates1); 01477 mdd_free(Covstates2); 01478 temp1 = result; 01479 result = mdd_and(temp1,fairStates,1,1); 01480 mdd_free(temp1); 01481 mdd_free(startstates); 01482 return result; 01483 break; 01484 } 01485 case Ctlp_THEN_c:{ /*f1 -> f2 = !f2 -> !f1*/ 01486 int sigarr; 01487 array_t *listOfF2Signals = array_alloc(char *,0); 01488 array_t *listOfF1Signals = array_alloc(char *,0); 01489 array_t *newstatesToRemoveList = NIL(array_t); 01490 mdd_t *nextstartstates, *Tb, *tmp_mdd; 01491 01492 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 01493 rightFormula = Ctlp_FormulaReadRightChild(OrigFormula); 01494 existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula); 01495 Tb = Mc_FsmEvaluateFormula(fsm, existFormula, 01496 fairStates, fairCondition, careStatesArray, 01497 earlyTermination, hintsArray, hintType, 01498 verbosity, dcLevel, buildOnionRing,GSHschedule); 01499 Ctlp_FormulaFree(existFormula); 01500 nextstartstates = mdd_and(startstates, Tb,1,1); 01501 mdd_free(Tb); 01502 /*To compute C(So*T(f1),f2), * 01503 *first compute states to remove*/ 01504 newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList); 01505 findallsignalsInFormula(listOfF2Signals,rightFormula); /*find all signals in f2*/ 01506 for (sigarr=0;sigarr<array_n(listOfF2Signals);sigarr++) { 01507 /*for all signals in f2*/ 01508 mdd_t *tmp_mdd2; 01509 char *signalInF2; 01510 int positionInGlobalList; 01511 int rangeOfF2SigInF1; 01512 signalInF2 = array_fetch(char *,listOfF2Signals,sigarr); 01513 positionInGlobalList = positionOfSignalinList(signalInF2,signalList); 01514 if (positionInGlobalList < 0) /*shouldn't happen*/ 01515 fprintf(vis_stdout,"Serious trouble. Found a new signal!\n"); 01516 rangeOfF2SigInF1 = RangeofSignalinFormula(fsm,signalInF2,leftFormula); 01517 tmp_mdd = mdd_dup(nextstartstates); 01518 if (rangeOfF2SigInF1 > 0) { /*signal in F2 also in F1*/ 01519 if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if f1 is propositional*/ 01520 tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition, 01521 careStatesArray, earlyTermination, 01522 hintsArray, hintType, verbosity, dcLevel, 01523 buildOnionRing, GSHschedule, signalInF2, 01524 tmp_mdd); 01525 mdd_free(tmp_mdd); 01526 tmp_mdd = tmp_mdd2; 01527 } 01528 tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList, 01529 positionInGlobalList); 01530 if (tmp_mdd2 != NIL(mdd_t)) 01531 mdd_free(tmp_mdd2); 01532 array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList, 01533 tmp_mdd); 01534 } else { 01535 mdd_free(tmp_mdd); 01536 } 01537 } 01538 Covstates1 = CoveredStatesImproved(nextstartstates,fsm, rightFormula, 01539 fairStates, fairCondition, 01540 careStatesArray, earlyTermination, 01541 hintsArray, hintType, verbosity, 01542 dcLevel, buildOnionRing, GSHschedule, 01543 signalList, statesCoveredList, 01544 newCoveredStatesList, 01545 newstatesToRemoveList); 01546 mdd_free(nextstartstates); 01547 mdd_array_free(newstatesToRemoveList); 01548 array_free(listOfF2Signals); 01549 /*End of coverage computation of f2*/ 01550 01551 /*Now simillar computation for !f1 * 01552 * Convert f1->f2 to !f2->!f1 */ 01553 leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula)); 01554 rightFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula)); 01555 existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula); 01556 Tb = Mc_FsmEvaluateFormula(fsm, existFormula, 01557 fairStates, fairCondition, careStatesArray, 01558 earlyTermination, hintsArray, hintType, 01559 verbosity, dcLevel, buildOnionRing,GSHschedule); 01560 Ctlp_FormulaFree(existFormula); 01561 nextstartstates = mdd_and(startstates, Tb, 1, 1); 01562 mdd_free(Tb); 01563 newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList); 01564 findallsignalsInFormula(listOfF1Signals,rightFormula);/*find all signals in !f1*/ 01565 for (sigarr=0;sigarr<array_n(listOfF1Signals);sigarr++) { 01566 /*for all signals in !f1*/ 01567 mdd_t *tmp_mdd2; 01568 char *signalInNotF1; 01569 int positionInGlobalList; 01570 int rangeOfNotF1SigInNotF2; 01571 signalInNotF1 = array_fetch(char *,listOfF1Signals,sigarr); 01572 positionInGlobalList = positionOfSignalinList(signalInNotF1,signalList); 01573 if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n"); 01574 rangeOfNotF1SigInNotF2 = RangeofSignalinFormula(fsm,signalInNotF1,leftFormula); 01575 tmp_mdd = mdd_dup(nextstartstates); 01576 if (rangeOfNotF1SigInNotF2 > 0) {/*signal in !F1 also in !F2*/ 01577 if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if !f2 is propositional*/ 01578 tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition, 01579 careStatesArray, earlyTermination, 01580 hintsArray, hintType, verbosity, dcLevel, 01581 buildOnionRing, GSHschedule, signalInNotF1, 01582 tmp_mdd); 01583 mdd_free(tmp_mdd); 01584 tmp_mdd = tmp_mdd2; 01585 } 01586 tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList, 01587 positionInGlobalList); 01588 if (tmp_mdd2 != NIL(mdd_t)) 01589 mdd_free(tmp_mdd2); 01590 array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList, 01591 tmp_mdd); 01592 } else { 01593 mdd_free(tmp_mdd); 01594 } 01595 } 01596 Ctlp_FormulaFree(leftFormula); 01597 Covstates2 = CoveredStatesImproved(nextstartstates,fsm, rightFormula, 01598 fairStates, fairCondition, 01599 careStatesArray, earlyTermination, 01600 hintsArray, hintType, verbosity, 01601 dcLevel, buildOnionRing,GSHschedule, 01602 signalList, statesCoveredList, 01603 newCoveredStatesList, 01604 newstatesToRemoveList); 01605 01606 mdd_free(nextstartstates); 01607 mdd_array_free(newstatesToRemoveList); 01608 array_free(listOfF1Signals); 01609 /*End of coverage computation of !f1*/ 01610 Ctlp_FormulaFree(rightFormula); 01611 result = mdd_or(Covstates1,Covstates2,1,1); 01612 mdd_free(Covstates1); 01613 mdd_free(Covstates2); 01614 mdd_free(startstates); 01615 return result; 01616 break; 01617 } 01618 case Ctlp_XOR_c: { 01619 tmp_formula = Ctlp_FormulaConvertXORtoOR(OrigFormula); 01620 if (verbosity > McVerbosityNone_c) { 01621 fprintf(vis_stdout,"\n--Converting XOR to AND and OR from:\n"); 01622 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01623 fprintf(vis_stdout,"\nto\n"); 01624 Ctlp_FormulaPrint(vis_stdout, tmp_formula); 01625 fprintf(vis_stdout,"\n"); 01626 } 01627 result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates, 01628 fairCondition, careStatesArray, 01629 earlyTermination, hintsArray, hintType, 01630 verbosity, dcLevel,buildOnionRing, 01631 GSHschedule, signalList, statesCoveredList, 01632 newCoveredStatesList, statesToRemoveList); 01633 mdd_free(startstates); 01634 return result; 01635 break; 01636 } 01637 case Ctlp_EQ_c: { 01638 tmp_formula = Ctlp_FormulaConvertEQtoOR(OrigFormula); 01639 if (verbosity > McVerbosityNone_c) { 01640 fprintf(vis_stdout,"\n--Converting EQ to AND and OR"); 01641 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01642 fprintf(vis_stdout,"\nto\n"); 01643 Ctlp_FormulaPrint(vis_stdout, tmp_formula); 01644 fprintf(vis_stdout,"\n"); 01645 } 01646 result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates, 01647 fairCondition, careStatesArray, 01648 earlyTermination, hintsArray, hintType, 01649 verbosity, dcLevel,buildOnionRing, 01650 GSHschedule, signalList, statesCoveredList, 01651 newCoveredStatesList, statesToRemoveList); 01652 mdd_free(startstates); 01653 return result; 01654 break; 01655 } 01656 case Ctlp_OR_c:{ /*f1+f2 = !f1 -> f2 = !f2 -> f1*/ 01657 int sigarr; 01658 array_t *listOfF2Signals = array_alloc(char *,0); 01659 array_t *listOfF1Signals = array_alloc(char *,0); 01660 array_t *newstatesToRemoveList = NIL(array_t); 01661 mdd_t *nextstartstates, *Tb, *tmp_mdd; 01662 01663 /*To compute C(So*T(!f1),f2), * 01664 *convert to form like !f1->f2 */ 01665 leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula)); 01666 rightFormula = Ctlp_FormulaReadRightChild(OrigFormula); 01667 existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula); 01668 Tb = Mc_FsmEvaluateFormula(fsm, existFormula, 01669 fairStates, fairCondition, careStatesArray, 01670 earlyTermination, hintsArray, hintType, 01671 verbosity, dcLevel, buildOnionRing,GSHschedule); 01672 Ctlp_FormulaFree(existFormula); 01673 nextstartstates = mdd_and(startstates, Tb, 1, 1); 01674 mdd_free(Tb); 01675 /*first compute states to remove*/ 01676 newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList); 01677 findallsignalsInFormula(listOfF2Signals,rightFormula);/*find all signals in f2*/ 01678 for (sigarr=0;sigarr<array_n(listOfF2Signals);sigarr++) { 01679 /*for all signals in f2*/ 01680 mdd_t *tmp_mdd2; 01681 char *signalInF2; 01682 int positionInGlobalList; 01683 int rangeOfF2SigInF1; 01684 signalInF2 = array_fetch(char *,listOfF2Signals,sigarr); 01685 positionInGlobalList = positionOfSignalinList(signalInF2,signalList); 01686 if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n"); 01687 rangeOfF2SigInF1 = RangeofSignalinFormula(fsm,signalInF2,leftFormula); 01688 tmp_mdd = mdd_dup(nextstartstates); 01689 if (rangeOfF2SigInF1 > 0) {/*signal in F2 also in F1*/ 01690 if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if f1 is propositional*/ 01691 tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition, 01692 careStatesArray, earlyTermination, 01693 hintsArray, hintType, verbosity, dcLevel, 01694 buildOnionRing, GSHschedule, signalInF2, 01695 tmp_mdd); 01696 mdd_free(tmp_mdd); 01697 tmp_mdd = tmp_mdd2; 01698 } 01699 tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList, 01700 positionInGlobalList); 01701 if (tmp_mdd2 != NIL(mdd_t)) 01702 mdd_free(tmp_mdd2); 01703 array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList, 01704 tmp_mdd); 01705 } else { 01706 mdd_free(tmp_mdd); 01707 } 01708 } 01709 Ctlp_FormulaFree(leftFormula); 01710 Covstates1 = CoveredStatesImproved(nextstartstates,fsm, rightFormula, 01711 fairStates, fairCondition, 01712 careStatesArray, earlyTermination, 01713 hintsArray, hintType, verbosity, 01714 dcLevel, buildOnionRing,GSHschedule, 01715 signalList, statesCoveredList, 01716 newCoveredStatesList, 01717 newstatesToRemoveList); 01718 mdd_free(nextstartstates); 01719 mdd_array_free(newstatesToRemoveList); 01720 array_free(listOfF2Signals); 01721 /*End of coverage computation of f2*/ 01722 01723 /*Now simillar computation for !f1 * 01724 * Convert f1+f2 to !f2->f1 */ 01725 leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula)); 01726 rightFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 01727 existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula); 01728 Tb = Mc_FsmEvaluateFormula(fsm, existFormula, 01729 fairStates, fairCondition, careStatesArray, 01730 earlyTermination, hintsArray, hintType, 01731 verbosity, dcLevel, buildOnionRing,GSHschedule); 01732 Ctlp_FormulaFree(existFormula); 01733 nextstartstates = mdd_and(startstates, Tb,1,1); 01734 mdd_free(Tb); 01735 newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList); 01736 findallsignalsInFormula(listOfF1Signals,rightFormula);/*find all signals in f1*/ 01737 for (sigarr=0;sigarr<array_n(listOfF1Signals);sigarr++) { 01738 /*for all signals in f1*/ 01739 mdd_t *tmp_mdd2; 01740 char *signalInF1; 01741 int positionInGlobalList; 01742 int rangeOfF1SigInF2; 01743 signalInF1 = array_fetch(char *,listOfF1Signals,sigarr); 01744 positionInGlobalList = positionOfSignalinList(signalInF1,signalList); 01745 if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n"); 01746 rangeOfF1SigInF2 = RangeofSignalinFormula(fsm,signalInF1,leftFormula); 01747 tmp_mdd = mdd_dup(nextstartstates); 01748 if (rangeOfF1SigInF2 > 0) {/*signal in !F1 also in !F2*/ 01749 if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if !f2 is propositional*/ 01750 tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition, 01751 careStatesArray, earlyTermination, 01752 hintsArray, hintType, verbosity, dcLevel, 01753 buildOnionRing, GSHschedule, signalInF1, 01754 tmp_mdd); 01755 mdd_free(tmp_mdd); 01756 tmp_mdd = tmp_mdd2; 01757 } 01758 tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList, 01759 positionInGlobalList); 01760 if (tmp_mdd2 != NIL(mdd_t)) 01761 mdd_free(tmp_mdd2); 01762 array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList, 01763 tmp_mdd); 01764 } else { 01765 mdd_free(tmp_mdd); 01766 } 01767 } 01768 Ctlp_FormulaFree(leftFormula); 01769 Covstates2 = CoveredStatesImproved(nextstartstates,fsm, rightFormula, 01770 fairStates, fairCondition, 01771 careStatesArray, earlyTermination, 01772 hintsArray, hintType, verbosity, 01773 dcLevel, buildOnionRing,GSHschedule, 01774 signalList, statesCoveredList, 01775 newCoveredStatesList, 01776 newstatesToRemoveList); 01777 mdd_free(nextstartstates); 01778 mdd_array_free(newstatesToRemoveList); 01779 array_free(listOfF1Signals); 01780 /*End of coverage computation of !f1*/ 01781 01782 result = mdd_or(Covstates1,Covstates2,1,1); 01783 mdd_free(Covstates1); 01784 mdd_free(Covstates2); 01785 mdd_free(startstates); 01786 return result; 01787 break; 01788 } 01789 case Ctlp_NOT_c:{ /*include code for checking for 2 NOTs*/ 01790 leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula); 01791 if (!(Ctlp_FormulaTestIsQuantifierFree(leftFormula))) { 01792 tmp_formula = Ctlp_FormulaPushNegation(leftFormula); 01793 if (verbosity > McVerbosityNone_c) { 01794 fprintf(vis_stdout,"\n--Pushing down negation one level. Converting formula from:\n"); 01795 Ctlp_FormulaPrint(vis_stdout,OrigFormula); 01796 fprintf(vis_stdout,"\nto\n"); 01797 Ctlp_FormulaPrint(vis_stdout,tmp_formula); 01798 fprintf(vis_stdout,"\n"); 01799 } 01800 Covstates1 = CoveredStatesImproved(startstates,fsm, tmp_formula, 01801 fairStates, fairCondition, 01802 careStatesArray, earlyTermination, 01803 hintsArray, hintType, verbosity, 01804 dcLevel, buildOnionRing,GSHschedule, 01805 signalList, statesCoveredList, 01806 newCoveredStatesList, 01807 statesToRemoveList); 01808 result = mdd_and(Covstates1,fairStates,1,1); 01809 Ctlp_FormulaFree(tmp_formula); 01810 mdd_free(Covstates1); 01811 mdd_free(startstates); 01812 return result; 01813 } else { /*this part of the code is now never executed*/ 01814 fprintf(vis_stdout, "\n****Error, Should not have reached here\n"); 01815 mdd_free(startstates); 01816 return mdd_zero(Fsm_FsmReadMddManager(fsm)); 01817 } 01818 break; 01819 } 01820 case Ctlp_TRUE_c: 01821 case Ctlp_FALSE_c: { 01822 if (verbosity > McVerbosityNone_c) 01823 fprintf(vis_stdout,"No observable signal, hence no coverage\n"); 01824 result = mdd_zero(Fsm_FsmReadMddManager(fsm)); 01825 mdd_free(startstates); 01826 return result; 01827 break; 01828 } 01829 case Ctlp_ID_c:{ /*should not reach here*/ 01830 fprintf(vis_stdout, "\n****Error, Should not have reached here\n"); 01831 mdd_free(startstates); 01832 return mdd_zero(Fsm_FsmReadMddManager(fsm)); 01833 break; 01834 } 01835 default: 01836 fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n"); 01837 mdd_free(startstates); 01838 break; 01839 } 01840 assert(0); 01841 return NIL(mdd_t); 01842 01843 } /* End of CoveredStatesImproved */ 01844 01845 01857 static mdd_t * 01858 CoveragePropositional( 01859 mdd_t *startstates_old, 01860 Fsm_Fsm_t *fsm, 01861 Ctlp_Formula_t *OrigFormula, 01862 mdd_t *fairStates, 01863 Fsm_Fairness_t *fairCondition, 01864 array_t *careStatesArray, 01865 Mc_EarlyTermination_t *earlyTermination, 01866 Fsm_HintsArray_t *hintsArray, 01867 Mc_GuidedSearch_t hintType, 01868 Mc_VerbosityLevel verbosity, 01869 Mc_DcLevel dcLevel, 01870 int buildOnionRing, 01871 Mc_GSHScheduleType GSHschedule, 01872 array_t *signalList, 01873 array_t *statesCoveredList, 01874 array_t *newCoveredStatesList, 01875 array_t *statesToRemoveList) 01876 { 01877 mdd_t *Tb, *result; 01878 mdd_t *startstates; 01879 array_t *listOfSignals = array_alloc(char *,0); 01880 int i,positionInList; 01881 char *signal; 01882 Ctlp_Formula_t *tmpFormula; 01883 01884 result = mdd_zero(Fsm_FsmReadMddManager(fsm)); 01885 findallsignalsInFormula(listOfSignals,OrigFormula); 01886 if (array_n(listOfSignals)==0) { 01887 if (verbosity > McVerbosityNone_c) 01888 fprintf(vis_stdout,"No observable signals, hence no coverage\n"); 01889 array_free(listOfSignals); 01890 return result; 01891 } 01892 /*else*/ 01893 startstates = mdd_and(startstates_old,fairStates,1,1); 01894 tmpFormula = Ctlp_FormulaConvertToExistentialForm(OrigFormula); 01895 Tb = Mc_FsmEvaluateFormula(fsm, tmpFormula, fairStates, 01896 fairCondition, careStatesArray, earlyTermination, 01897 hintsArray, hintType, verbosity, dcLevel, 01898 buildOnionRing,GSHschedule); 01899 Ctlp_FormulaFree(tmpFormula); 01900 for (i=0;i<array_n(listOfSignals);i++) { 01901 mdd_t *statesCovered, *newCoveredStates, *statesToRemove, *CovStates, *tmp_mdd, *tmp_mdd2; 01902 signal = array_fetch(char *,listOfSignals,i); 01903 positionInList = positionOfSignalinList(signal,signalList); 01904 if (positionInList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n"); 01905 statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList); 01906 newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList); 01907 statesToRemove = array_fetch(mdd_t *,statesToRemoveList,positionInList); 01908 CovStates = computedependHoskote(fsm, OrigFormula, fairStates, 01909 fairCondition, careStatesArray, 01910 earlyTermination, hintsArray, 01911 hintType, verbosity, dcLevel, 01912 buildOnionRing, GSHschedule, 01913 startstates, signal, Tb, statesCovered, 01914 newCoveredStates,statesToRemove); 01915 tmp_mdd = mdd_or(newCoveredStates,CovStates,1,1); 01916 mdd_free(newCoveredStates); 01917 array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd);/*update newCoveredStatesList*/ 01918 tmp_mdd2 = result; 01919 result = mdd_or(tmp_mdd2,CovStates,1,1); 01920 mdd_free(tmp_mdd2); 01921 mdd_free(CovStates); 01922 } 01923 mdd_free(Tb); 01924 mdd_free(startstates); 01925 array_free(listOfSignals); 01926 return result; 01927 } /* CoveragePropositional */ 01928 01929 01948 static mdd_t * 01949 computedepend( 01950 Fsm_Fsm_t *fsm, 01951 Ctlp_Formula_t *formula, 01952 mdd_t *fairStates, 01953 Fsm_Fairness_t *fairCondition, 01954 array_t *careStatesArray, 01955 Mc_EarlyTermination_t *earlyTermination, 01956 Fsm_HintsArray_t *hintsArray, 01957 Mc_GuidedSearch_t hintType, 01958 Mc_VerbosityLevel verbosity, 01959 Mc_DcLevel dcLevel, 01960 int buildOnionRing, 01961 Mc_GSHScheduleType GSHschedule, 01962 char *signal, 01963 mdd_t *SoAndTb_old) 01964 { 01965 mdd_t *TnotBnotQ, *Covstates, *SoAndTb; 01966 Ctlp_Formula_t *convertedformula, *tmp_formula, *existFormula; 01967 SoAndTb = mdd_and(SoAndTb_old,fairStates,1,1); 01968 convertedformula = FormulaConvertSignalComplement(fsm,signal,formula); 01969 if (convertedformula != NIL(Ctlp_Formula_t)) { 01970 tmp_formula = Ctlp_FormulaConverttoComplement(convertedformula); 01971 existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula); 01972 TnotBnotQ = Mc_FsmEvaluateFormula(fsm, existFormula, 01973 fairStates, fairCondition, 01974 careStatesArray, earlyTermination, 01975 hintsArray, hintType, verbosity, 01976 dcLevel, buildOnionRing,GSHschedule); 01977 Ctlp_FormulaFree(existFormula); 01978 Ctlp_FormulaFree(tmp_formula); 01979 } else { 01980 TnotBnotQ = mdd_zero(Fsm_FsmReadMddManager(fsm)); 01981 } 01982 Ctlp_FormulaFree(convertedformula); 01983 Covstates = mdd_and(SoAndTb,TnotBnotQ,1,1); /*covered states*/ 01984 mdd_free(SoAndTb); 01985 mdd_free(TnotBnotQ); 01986 return Covstates; 01987 } /* computedepend */ 01988 01989 02008 static mdd_t * 02009 computedependHoskote( 02010 Fsm_Fsm_t *fsm, 02011 Ctlp_Formula_t *formula, 02012 mdd_t *fairStates, 02013 Fsm_Fairness_t *fairCondition, 02014 array_t *careStatesArray, 02015 Mc_EarlyTermination_t *earlyTermination, 02016 Fsm_HintsArray_t *hintsArray, 02017 Mc_GuidedSearch_t hintType, 02018 Mc_VerbosityLevel verbosity, 02019 Mc_DcLevel dcLevel, 02020 int buildOnionRing, 02021 Mc_GSHScheduleType GSHschedule, 02022 mdd_t *startstates_old, 02023 char *signal, 02024 mdd_t *Tb, 02025 mdd_t *statesCovered, 02026 mdd_t *newCoveredStates, 02027 mdd_t *statesToRemove) 02028 { 02029 mdd_t *TnotBnotQ,*Covstates,*startstates,*tmp_mdd, *newCovstates; 02030 Ctlp_Formula_t *convertedformula; 02031 startstates = mdd_and(startstates_old,fairStates,1,1); 02032 convertedformula = FormulaConvertSignalComplement(fsm,signal,formula); 02033 02034 if (convertedformula != NIL(Ctlp_Formula_t)) { 02035 Ctlp_Formula_t *tmp_formula, *tmp_formula2; 02036 tmp_formula = Ctlp_FormulaConverttoComplement(convertedformula); 02037 Ctlp_FormulaFree(convertedformula); 02038 tmp_formula2 = Ctlp_FormulaConvertToExistentialForm(tmp_formula); 02039 Ctlp_FormulaFree(tmp_formula); 02040 TnotBnotQ = Mc_FsmEvaluateFormula(fsm, tmp_formula2, 02041 fairStates, fairCondition, 02042 careStatesArray, earlyTermination, 02043 hintsArray, hintType, verbosity, 02044 dcLevel, buildOnionRing,GSHschedule); 02045 Ctlp_FormulaFree(tmp_formula2); 02046 } else { 02047 TnotBnotQ = mdd_zero(Fsm_FsmReadMddManager(fsm)); 02048 } 02049 02050 tmp_mdd = mdd_and(Tb,TnotBnotQ,1,1); 02051 mdd_free(TnotBnotQ); 02052 Covstates = mdd_and(startstates,tmp_mdd,1,1); /*covered states*/ 02053 mdd_free(tmp_mdd); 02054 tmp_mdd = Covstates; 02055 mdd_free(startstates); 02056 Covstates = mdd_and(Covstates, statesToRemove,1,0); /*remove the states to remove*/ 02057 mdd_free(tmp_mdd); 02058 tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1); 02059 newCovstates = mdd_and(Covstates,tmp_mdd,1,0); /* newly covered states*/ 02060 mdd_free(tmp_mdd); 02061 #if 0 02062 fprintf(vis_stdout,"States covered w.r.t. %s = %0.f , new = %0.f\n",signal, 02063 mdd_count_onset(Fsm_FsmReadMddManager(fsm),Covstates, 02064 Fsm_FsmReadPresentStateVars(fsm)), 02065 mdd_count_onset(Fsm_FsmReadMddManager(fsm),newCovstates, 02066 Fsm_FsmReadPresentStateVars(fsm))); 02067 #endif 02068 mdd_free(newCovstates); 02069 return Covstates; 02070 02071 } /* computedependHoskote */ 02072 02073 02088 static mdd_t * 02089 traverse( 02090 Fsm_Fsm_t *fsm, 02091 mdd_t *fairStates, 02092 Fsm_Fairness_t *fairCondition, 02093 array_t *careStatesArray, 02094 Mc_EarlyTermination_t *earlyTermination, 02095 Fsm_HintsArray_t *hintsArray, 02096 Mc_GuidedSearch_t hintType, 02097 Mc_VerbosityLevel verbosity, 02098 Mc_DcLevel dcLevel, 02099 int buildOnionRing, 02100 Mc_GSHScheduleType GSHschedule, 02101 mdd_t *startstates, 02102 Ctlp_Formula_t *formula1, 02103 Ctlp_Formula_t *formula2) 02104 { 02105 mdd_t *temp_mdd,*newSo, *Tf1_and_Tnotf2, *newStates, *oldStates, *Tf1, *Tnotf2; 02106 Ctlp_Formula_t *tmp_formula, *existFormula; 02107 int travcnt; 02108 oldStates = mdd_zero(Fsm_FsmReadMddManager(fsm)); 02109 newStates = mdd_zero(Fsm_FsmReadMddManager(fsm)); 02110 newSo = mdd_dup(startstates); 02111 existFormula = Ctlp_FormulaConvertToExistentialForm(formula1); 02112 Tf1 = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates, 02113 fairCondition, careStatesArray, 02114 earlyTermination, hintsArray, 02115 hintType, verbosity, dcLevel, 02116 buildOnionRing,GSHschedule); 02117 Ctlp_FormulaFree(existFormula); 02118 tmp_formula = Ctlp_FormulaConverttoComplement(formula2); 02119 existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula); 02120 Tnotf2 = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates, fairCondition, 02121 careStatesArray, earlyTermination, hintsArray, 02122 hintType, verbosity, dcLevel, 02123 buildOnionRing, GSHschedule); 02124 Ctlp_FormulaFree(existFormula); 02125 Ctlp_FormulaFree(tmp_formula); 02126 temp_mdd = mdd_and(Tf1,Tnotf2,1,1); 02127 mdd_free(Tf1); 02128 mdd_free(Tnotf2); 02129 Tf1_and_Tnotf2 = mdd_and(temp_mdd,fairStates,1,1); 02130 mdd_free(temp_mdd); 02131 temp_mdd = newSo; 02132 newSo = mdd_and(temp_mdd,Tf1_and_Tnotf2,1,1); 02133 mdd_free(temp_mdd); 02134 temp_mdd = newStates; 02135 newStates = mdd_or(temp_mdd,newSo,1,1); 02136 mdd_free(temp_mdd); 02137 travcnt = 0; 02138 while (!(mdd_equal_mod_care_set_array(newStates,oldStates,careStatesArray))) { 02139 mdd_t *tmp_mdd = oldStates; 02140 oldStates = mdd_or(tmp_mdd,newStates,1,1); 02141 mdd_free(tmp_mdd); 02142 tmp_mdd = newSo; 02143 newSo = Mc_FsmEvaluateEYFormula(fsm, tmp_mdd, fairStates, careStatesArray, verbosity, dcLevel); 02144 mdd_free(tmp_mdd); 02145 tmp_mdd = newSo; 02146 newSo = mdd_and(tmp_mdd,Tf1_and_Tnotf2,1,1); 02147 mdd_free(tmp_mdd); 02148 tmp_mdd = newStates; 02149 newStates = mdd_or(tmp_mdd,newSo,1,1); 02150 mdd_free(tmp_mdd); 02151 } 02152 mdd_free(oldStates); 02153 mdd_free(newSo); 02154 mdd_free(Tf1_and_Tnotf2); 02155 return newStates; 02156 02157 } /* traverse */ 02158 02159 02175 static mdd_t * 02176 firstReached( 02177 Fsm_Fsm_t *fsm, 02178 mdd_t *fairStates, 02179 Fsm_Fairness_t *fairCondition, 02180 array_t *careStatesArray, 02181 Mc_EarlyTermination_t *earlyTermination, 02182 Fsm_HintsArray_t *hintsArray, 02183 Mc_GuidedSearch_t hintType, 02184 Mc_VerbosityLevel verbosity, 02185 Mc_DcLevel dcLevel, 02186 int buildOnionRing, 02187 Mc_GSHScheduleType GSHschedule, 02188 mdd_t *startstates, 02189 Ctlp_Formula_t *formula) 02190 { 02191 int frstcnt; 02192 mdd_t *temp1, *temp2, *oldSo, *CovStates, *Tf2, *Tnotf2, *zeroMDD; 02193 Ctlp_Formula_t *tmp_formula, *existFormula; 02194 oldSo = mdd_dup(startstates); 02195 zeroMDD = mdd_zero(Fsm_FsmReadMddManager(fsm)); 02196 existFormula = Ctlp_FormulaConvertToExistentialForm(formula); 02197 Tf2 = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates, 02198 fairCondition, careStatesArray, 02199 earlyTermination, hintsArray, 02200 hintType, verbosity, 02201 dcLevel, buildOnionRing, GSHschedule); 02202 Ctlp_FormulaFree(existFormula); 02203 tmp_formula = Ctlp_FormulaConverttoComplement(formula); 02204 existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula); 02205 Tnotf2 = Mc_FsmEvaluateFormula(fsm, existFormula, 02206 fairStates, fairCondition, 02207 careStatesArray,earlyTermination, 02208 hintsArray, hintType, verbosity, 02209 dcLevel, buildOnionRing,GSHschedule); 02210 Ctlp_FormulaFree(existFormula); 02211 Ctlp_FormulaFree(tmp_formula); 02212 CovStates = mdd_and(oldSo,Tf2,1,1); 02213 temp1 = mdd_dup(oldSo); 02214 temp2 = mdd_and(oldSo,Tnotf2,1,1); 02215 frstcnt = 0; 02216 while (!(mdd_equal_mod_care_set_array(temp2,zeroMDD,careStatesArray))) { 02217 mdd_t *tmp_mdd1, *tmp_mdd2, *tmp_mdd; 02218 tmp_mdd = Mc_FsmEvaluateEYFormula(fsm, temp2, fairStates, careStatesArray, verbosity, dcLevel); /*forward(So^Tnotf2)*/ 02219 tmp_mdd2 = mdd_and(tmp_mdd,Tf2,1,1); 02220 tmp_mdd1 = CovStates; 02221 CovStates = mdd_or(CovStates,tmp_mdd2,1,1); /*add on the new states*/ 02222 mdd_free(tmp_mdd1); 02223 mdd_free(tmp_mdd2); 02224 tmp_mdd1 = mdd_and(tmp_mdd,Tnotf2,1,1); /*newSo^Tnotf2*/ 02225 tmp_mdd2 = temp2; 02226 temp2 = mdd_and(tmp_mdd1,temp1,1,0); /*take out the startstates already encountered temp2 = newSo*/ 02227 mdd_free(tmp_mdd2); 02228 mdd_free(tmp_mdd1); 02229 tmp_mdd1 = temp1; 02230 temp1 = mdd_or(temp1,tmp_mdd,1,1); 02231 mdd_free(tmp_mdd1); 02232 mdd_free(tmp_mdd); 02233 } 02234 mdd_free(zeroMDD); 02235 mdd_free(oldSo); 02236 mdd_free(Tf2); 02237 mdd_free(Tnotf2); 02238 mdd_free(temp1); 02239 mdd_free(temp2); 02240 return CovStates; 02241 02242 } /* firstreached */ 02243 02244 02257 static Ctlp_Formula_t * 02258 FormulaConvertSignalComplement( 02259 Fsm_Fsm_t *fsm, 02260 char *signal, 02261 Ctlp_Formula_t *formula) 02262 { 02263 Ctlp_Formula_t *result = NIL(Ctlp_Formula_t); 02264 Ctlp_Formula_t *leftChildConverted, *leftFormula; 02265 Ctlp_Formula_t *rightChildConverted, *rightFormula; 02266 Ntk_Network_t *network; 02267 char *nodeNameString; 02268 char *nodeValueString; 02269 Ntk_Node_t *node; 02270 Var_Variable_t *nodeVar; 02271 02272 if ( formula == NIL(Ctlp_Formula_t)) { 02273 return NIL(Ctlp_Formula_t); 02274 } 02275 02276 if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c ) { 02277 leftFormula = Ctlp_FormulaReadLeftChild(formula); 02278 leftChildConverted = FormulaConvertSignalComplement(fsm, signal, 02279 leftFormula); 02280 rightFormula = Ctlp_FormulaReadRightChild(formula); 02281 rightChildConverted = FormulaConvertSignalComplement(fsm, signal, 02282 rightFormula); 02283 result = Ctlp_FormulaCreate(Ctlp_FormulaReadType(formula), 02284 leftChildConverted,rightChildConverted); 02285 } 02286 else { /* if atomic proposition*/ 02287 network = Fsm_FsmReadNetwork(fsm); 02288 nodeNameString = Ctlp_FormulaReadVariableName(formula); 02289 nodeValueString = Ctlp_FormulaReadValueName(formula); 02290 node = Ntk_NetworkFindNodeByName(network, nodeNameString); 02291 nodeVar = Ntk_NodeReadVariable(node); 02292 if ((strcmp(signal,nodeNameString)) != 0) { /* not the signal that we want to flip */ 02293 result = Ctlp_FormulaCreate(Ctlp_FormulaReadType(formula), 02294 (Ctlp_Formula_t *) util_strsav(nodeNameString), 02295 (Ctlp_Formula_t *) util_strsav(nodeValueString)); 02296 } 02297 else { /* this is the signal that we want to flip */ 02298 result = Ctlp_FormulaConverttoComplement(formula); 02299 } 02300 } 02301 return result; 02302 } /* FormulaConvertSignalComplement */ 02303 02304 02317 static void 02318 findallsignals( 02319 Fsm_Fsm_t *fsm, 02320 array_t *signalTypeList, 02321 array_t *signalList, 02322 array_t *statesCoveredList, 02323 array_t *newCoveredStatesList, 02324 array_t *statesToRemoveList, 02325 Ctlp_Formula_t *formula, 02326 mdd_t *zeroMdd) 02327 { 02328 Ntk_Network_t *network; 02329 Ntk_Node_t *node; 02330 Var_Variable_t *nodeVar; 02331 char *nodeNameString; 02332 int signalType; 02333 Ctlp_Formula_t *leftFormula, *rightFormula; 02334 if ( formula == NIL(Ctlp_Formula_t)) { 02335 return; 02336 } 02337 02338 if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c ) { 02339 leftFormula = Ctlp_FormulaReadLeftChild(formula); 02340 rightFormula = Ctlp_FormulaReadRightChild(formula); 02341 findallsignals(fsm, signalTypeList, signalList, statesCoveredList, 02342 newCoveredStatesList, statesToRemoveList, 02343 leftFormula, zeroMdd); 02344 findallsignals(fsm, signalTypeList, signalList, statesCoveredList, 02345 newCoveredStatesList, statesToRemoveList, 02346 rightFormula,zeroMdd); 02347 } 02348 else { /* atomic proposition */ 02349 nodeNameString = Ctlp_FormulaReadVariableName(formula); 02350 if ((positionOfSignalinList(nodeNameString,signalList)) == -1) { 02351 fprintf(vis_stdout,"Found new signal = %s\n",nodeNameString); 02352 network = Fsm_FsmReadNetwork(fsm); 02353 node = Ntk_NetworkFindNodeByName(network, nodeNameString); 02354 nodeVar = Ntk_NodeReadVariable(node); 02355 if (Var_VariableTestIsPI(nodeVar)) 02356 signalType = 1; 02357 else if (Var_VariableTestIsPO(nodeVar)) 02358 signalType = 0; 02359 else 02360 signalType = 2; 02361 array_insert_last(int,signalTypeList,signalType); 02362 array_insert_last(char *,signalList,nodeNameString); 02363 array_insert_last(mdd_t *,statesCoveredList,mdd_dup(zeroMdd)); 02364 array_insert_last(mdd_t *,newCoveredStatesList,mdd_dup(zeroMdd)); 02365 array_insert_last(mdd_t *,statesToRemoveList,mdd_dup(zeroMdd)); 02366 } 02367 } 02368 return; 02369 } /* findallsignals */ 02370 02371 02384 static void 02385 findallsignalsInFormula( 02386 array_t *signalList, 02387 Ctlp_Formula_t *formula) 02388 { 02389 char *nodeNameString; 02390 02391 Ctlp_Formula_t *leftFormula, *rightFormula; 02392 if ( formula == NIL(Ctlp_Formula_t)) { 02393 return; 02394 } 02395 02396 if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c ) { 02397 leftFormula = Ctlp_FormulaReadLeftChild(formula); 02398 rightFormula = Ctlp_FormulaReadRightChild(formula); 02399 findallsignalsInFormula(signalList,leftFormula); 02400 findallsignalsInFormula(signalList,rightFormula); 02401 } 02402 else { /* atomic proposition */ 02403 nodeNameString = Ctlp_FormulaReadVariableName(formula); 02404 if ((positionOfSignalinList(nodeNameString,signalList)) == -1) { 02405 array_insert_last(char *,signalList,nodeNameString); 02406 } 02407 } 02408 return; 02409 } /* findallsignalsInFormula */ 02410 02411 02424 static int 02425 positionOfSignalinList( 02426 char *signal, 02427 array_t *signalList) 02428 { 02429 int arraysize = array_n(signalList); 02430 int i; 02431 02432 for (i=0;i<arraysize;i++) { 02433 if (strcmp(signal,array_fetch(char *,signalList,i)) == 0) 02434 return i; 02435 } 02436 return -1; 02437 } /* positionOfSignalinList */ 02438 02439 02452 static int 02453 RangeofSignalinFormula( 02454 Fsm_Fsm_t *fsm, 02455 char *signal, 02456 Ctlp_Formula_t *formula) 02457 { 02458 Ntk_Network_t *network; 02459 char *nodeNameString; 02460 char *nodeValueString; 02461 Ntk_Node_t *node; 02462 Ctlp_Formula_t *leftFormula; 02463 Ctlp_Formula_t *rightFormula; 02464 02465 Var_Variable_t *nodeVar; 02466 int range_left,range_right; 02467 int range = 0; 02468 /*nodeVar = Ntk_NodeReadVariable(node);*/ 02469 02470 if ( formula == NIL(Ctlp_Formula_t)) { 02471 return range; 02472 } 02473 02474 if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c ) { 02475 leftFormula = Ctlp_FormulaReadLeftChild(formula); 02476 range_left = RangeofSignalinFormula(fsm, signal, leftFormula); 02477 #if 0 02478 Ctlp_FormulaFree(leftFormula); 02479 #endif 02480 rightFormula = Ctlp_FormulaReadRightChild (formula); 02481 range_right = RangeofSignalinFormula(fsm, signal, rightFormula); 02482 #if 0 02483 Ctlp_FormulaFree(rightFormula); 02484 #endif 02485 if (range_left==range_right) /* to avoid situation where signal exists on both sides of formula*/ 02486 range = range_left; 02487 else 02488 range = range_right+range_left; /* 0 + some value */ 02489 } 02490 else { 02491 network = Fsm_FsmReadNetwork(fsm); 02492 nodeNameString = Ctlp_FormulaReadVariableName(formula); 02493 nodeValueString = Ctlp_FormulaReadValueName(formula); 02494 node = Ntk_NetworkFindNodeByName(network, nodeNameString); 02495 nodeVar = Ntk_NodeReadVariable(node); 02496 if ((strcmp(signal,nodeNameString)) != 0) { 02497 range = 0; 02498 } 02499 else { 02500 range = Var_VariableReadNumValues(nodeVar); 02501 } 02502 } 02503 return range; 02504 } /* RangeofSignalinFormula */
1.7.3