#include "ctlpInt.h"#include "mcInt.h"
Include dependency graph for mcCover.c:
Go to the source code of this file.
Functions | |
| 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) |
| 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) |
| 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) |
| 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) |
| 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) |
| 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) |
| 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) |
| static Ctlp_Formula_t * | FormulaConvertSignalComplement (Fsm_Fsm_t *fsm, char *signal, Ctlp_Formula_t *formula) |
| 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) |
| static void | findallsignalsInFormula (array_t *signalList, Ctlp_Formula_t *formula) |
| static int | positionOfSignalinList (char *signal, array_t *signalList) |
| static int | RangeofSignalinFormula (Fsm_Fsm_t *fsm, char *signal, Ctlp_Formula_t *formula) |
| void | McEstimateCoverage (Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule, Mc_FwdBwdAnalysis traversalDirection, mdd_t *modelInitialStates, mdd_t *ctlFormulaStates, mdd_t **totalcoveredstates, array_t *signalTypeList, array_t *signalList, array_t *statesCoveredList, array_t *newCoveredStatesList, array_t *statesToRemoveList, boolean performCoverageHoskote, boolean performCoverageImproved) |
| void | McPrintCoverageSummary (Fsm_Fsm_t *modelFsm, Mc_DcLevel dcLevel, McOptions_t *options, array_t *modelCareStatesArray, mdd_t *modelCareStates, mdd_t *totalcoveredstates, array_t *signalTypeList, array_t *signalList, array_t *statesCoveredList, boolean performCoverageHoskote, boolean performCoverageImproved) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mcCover.c,v 1.4 2005/05/15 07:32:10 fabio Exp $" |
Function Documentation
| 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 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the following for use in coverage computation for propositional formulae:
computedepend = T(b) ^ T(!b|q->!q) where, T(f) => Set of states satisfying f b is a propositional formula q is an observed signal]
Description []
SideEffects [none]
SeeAlso [computedependHoskote]
Definition at line 1949 of file mcCover.c.
{
mdd_t *TnotBnotQ, *Covstates, *SoAndTb;
Ctlp_Formula_t *convertedformula, *tmp_formula, *existFormula;
SoAndTb = mdd_and(SoAndTb_old,fairStates,1,1);
convertedformula = FormulaConvertSignalComplement(fsm,signal,formula);
if (convertedformula != NIL(Ctlp_Formula_t)) {
tmp_formula = Ctlp_FormulaConverttoComplement(convertedformula);
existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
TnotBnotQ = Mc_FsmEvaluateFormula(fsm, existFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing,GSHschedule);
Ctlp_FormulaFree(existFormula);
Ctlp_FormulaFree(tmp_formula);
} else {
TnotBnotQ = mdd_zero(Fsm_FsmReadMddManager(fsm));
}
Ctlp_FormulaFree(convertedformula);
Covstates = mdd_and(SoAndTb,TnotBnotQ,1,1); /*covered states*/
mdd_free(SoAndTb);
mdd_free(TnotBnotQ);
return Covstates;
} /* computedepend */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the following for use in coverage computation for propositional formulae:
computedepend = T(b) ^ T(!b|q->!q) where, T(f) => Set of states satisfying f b is a propositional formula q is an observed signal]
Description []
SideEffects [none]
SeeAlso [computedepend]
Definition at line 2009 of file mcCover.c.
{
mdd_t *TnotBnotQ,*Covstates,*startstates,*tmp_mdd, *newCovstates;
Ctlp_Formula_t *convertedformula;
startstates = mdd_and(startstates_old,fairStates,1,1);
convertedformula = FormulaConvertSignalComplement(fsm,signal,formula);
if (convertedformula != NIL(Ctlp_Formula_t)) {
Ctlp_Formula_t *tmp_formula, *tmp_formula2;
tmp_formula = Ctlp_FormulaConverttoComplement(convertedformula);
Ctlp_FormulaFree(convertedformula);
tmp_formula2 = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
Ctlp_FormulaFree(tmp_formula);
TnotBnotQ = Mc_FsmEvaluateFormula(fsm, tmp_formula2,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing,GSHschedule);
Ctlp_FormulaFree(tmp_formula2);
} else {
TnotBnotQ = mdd_zero(Fsm_FsmReadMddManager(fsm));
}
tmp_mdd = mdd_and(Tb,TnotBnotQ,1,1);
mdd_free(TnotBnotQ);
Covstates = mdd_and(startstates,tmp_mdd,1,1); /*covered states*/
mdd_free(tmp_mdd);
tmp_mdd = Covstates;
mdd_free(startstates);
Covstates = mdd_and(Covstates, statesToRemove,1,0); /*remove the states to remove*/
mdd_free(tmp_mdd);
tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1);
newCovstates = mdd_and(Covstates,tmp_mdd,1,0); /* newly covered states*/
mdd_free(tmp_mdd);
#if 0
fprintf(vis_stdout,"States covered w.r.t. %s = %0.f , new = %0.f\n",signal,
mdd_count_onset(Fsm_FsmReadMddManager(fsm),Covstates,
Fsm_FsmReadPresentStateVars(fsm)),
mdd_count_onset(Fsm_FsmReadMddManager(fsm),newCovstates,
Fsm_FsmReadPresentStateVars(fsm)));
#endif
mdd_free(newCovstates);
return Covstates;
} /* computedependHoskote */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the coverage for propositional formulae]
Description []
SideEffects [none]
SeeAlso [CoveredStatesImproved CoveredStatesHoskote]
Definition at line 1858 of file mcCover.c.
{
mdd_t *Tb, *result;
mdd_t *startstates;
array_t *listOfSignals = array_alloc(char *,0);
int i,positionInList;
char *signal;
Ctlp_Formula_t *tmpFormula;
result = mdd_zero(Fsm_FsmReadMddManager(fsm));
findallsignalsInFormula(listOfSignals,OrigFormula);
if (array_n(listOfSignals)==0) {
if (verbosity > McVerbosityNone_c)
fprintf(vis_stdout,"No observable signals, hence no coverage\n");
array_free(listOfSignals);
return result;
}
/*else*/
startstates = mdd_and(startstates_old,fairStates,1,1);
tmpFormula = Ctlp_FormulaConvertToExistentialForm(OrigFormula);
Tb = Mc_FsmEvaluateFormula(fsm, tmpFormula, fairStates,
fairCondition, careStatesArray, earlyTermination,
hintsArray, hintType, verbosity, dcLevel,
buildOnionRing,GSHschedule);
Ctlp_FormulaFree(tmpFormula);
for (i=0;i<array_n(listOfSignals);i++) {
mdd_t *statesCovered, *newCoveredStates, *statesToRemove, *CovStates, *tmp_mdd, *tmp_mdd2;
signal = array_fetch(char *,listOfSignals,i);
positionInList = positionOfSignalinList(signal,signalList);
if (positionInList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList);
newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList);
statesToRemove = array_fetch(mdd_t *,statesToRemoveList,positionInList);
CovStates = computedependHoskote(fsm, OrigFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType, verbosity, dcLevel,
buildOnionRing, GSHschedule,
startstates, signal, Tb, statesCovered,
newCoveredStates,statesToRemove);
tmp_mdd = mdd_or(newCoveredStates,CovStates,1,1);
mdd_free(newCoveredStates);
array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd);/*update newCoveredStatesList*/
tmp_mdd2 = result;
result = mdd_or(tmp_mdd2,CovStates,1,1);
mdd_free(tmp_mdd2);
mdd_free(CovStates);
}
mdd_free(Tb);
mdd_free(startstates);
array_free(listOfSignals);
return result;
} /* CoveragePropositional */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Computes a the set of covered states for a given formula and initial set of states given.]
Description [Presently Works for only a subset of ACTL viz. (propostional formulae, ->, AX, AG, AF, AU, ^ )]
SideEffects [Updates running totals.]
SeeAlso [McEstimateCoverage CoveredStatesImproved]
Definition at line 721 of file mcCover.c.
{
mdd_t *Covstates1, *temp1, *temp2;
mdd_t *Covstates2;
mdd_t *result;
mdd_t *travstates;
mdd_t *frstrchstates;
mdd_t *startstates;
Ctlp_FormulaType formulaType;
Ctlp_Formula_t *rightFormula, *leftFormula, *tmp_formula, *existFormula;
double numresultstates; /* used for debugging <NJ> */
startstates = mdd_and(startstates_old,fairStates,1,1);
if (mdd_is_tautology(startstates,0)) {
if (verbosity > McVerbosityNone_c)
fprintf(vis_stdout,
"\n--Startstates are down to zero. Coverage is hence zero.\n");
result = mdd_zero(Fsm_FsmReadMddManager(fsm));
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(startstates);
return result;
}
if (Ctlp_FormulaTestIsQuantifierFree(OrigFormula)) {
/*propositional formula*/
result = CoveragePropositional(startstates, fsm, OrigFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel,buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
mdd_free(startstates);
return result;
}
formulaType = Ctlp_FormulaReadType(OrigFormula);
switch (formulaType) {
case Ctlp_EG_c:
case Ctlp_EF_c:
case Ctlp_EU_c:
case Ctlp_FwdU_c:
case Ctlp_FwdG_c:
case Ctlp_EY_c:
case Ctlp_EH_c:
case Ctlp_Cmp_c:
case Ctlp_EX_c:
case Ctlp_Init_c: {
fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL,\n");
fprintf(vis_stdout,"** can't compute coverage of : ");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\n");
result = mdd_zero(Fsm_FsmReadMddManager(fsm));
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,Fsm_FsmReadPresentStateVars(fsm));
mdd_free(startstates);
return result;
break;
}
case Ctlp_AX_c:{
temp1 = Mc_FsmEvaluateEYFormula(fsm, startstates, fairStates, careStatesArray, verbosity, dcLevel);
Covstates1 = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
result = CoveredStatesHoskote(Covstates1, fsm, leftFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType, verbosity, dcLevel, buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(Covstates1);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
mdd_free(startstates);
return result;
break;
}
case Ctlp_AG_c:{
mdd_t *initStates;
double numststates;
initStates = Fsm_FsmComputeInitialStates(fsm);
temp1 = mdd_one(Fsm_FsmReadMddManager(fsm));
if (mdd_equal_mod_care_set_array(startstates,initStates,careStatesArray)) {
if (verbosity > McVerbosityNone_c)
fprintf(vis_stdout,"\nUsing the reachable states already computed...");
temp2 = Fsm_FsmComputeReachableStates(fsm, 0, 1, 0, 0, 0, 0, 0,
Fsm_Rch_Default_c, 0, 0,
NIL(array_t), FALSE, NIL(array_t));
} else
temp2 = Mc_FsmEvaluateFwdUFormula(fsm, startstates, temp1, fairStates,
careStatesArray, NIL(array_t),
verbosity, dcLevel);
mdd_free(initStates);
numststates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),startstates,
Fsm_FsmReadPresentStateVars(fsm));
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),temp2,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(temp1);
Covstates1 = mdd_and(temp2,fairStates,1,1);
mdd_free(temp2);
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
result = CoveredStatesHoskote(Covstates1, fsm, leftFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel, buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(Covstates1);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
mdd_free(startstates);
return result;
break;
}
case Ctlp_AF_c:{
tmp_formula = OrigFormula;
OrigFormula = Ctlp_FormulaConvertAFtoAU(tmp_formula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"Converting formula from\n");
Ctlp_FormulaPrint(vis_stdout,tmp_formula);
fprintf(vis_stdout,"\nto\n");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\n");
}
#if 0
Ctlp_FormulaFree(tmp_formula);
formulaType = Ctlp_AU_c;
#endif
/* convert to AFp to A (TRUE) U p and then step thru to do coverage
for AU computation below*/
}
case Ctlp_AU_c:{
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
travstates = traverse(fsm, fairStates, fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType, verbosity,
dcLevel, buildOnionRing, GSHschedule, startstates,
leftFormula,rightFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n---Computing coverage for LHS of U formula i.e: ");
Ctlp_FormulaPrint(vis_stdout,leftFormula);
fprintf(vis_stdout,
"\n------------------------------------------------\n");
}
Covstates1 = CoveredStatesHoskote(travstates, fsm, leftFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel, buildOnionRing,
GSHschedule, signalList,
statesCoveredList, newCoveredStatesList,
statesToRemoveList);
mdd_free(travstates);
frstrchstates = firstReached(fsm, fairStates, fairCondition,
careStatesArray, earlyTermination, hintsArray,
hintType, verbosity, dcLevel, buildOnionRing,
GSHschedule, startstates, rightFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n---Computing coverage for RHS of U formula i.e: ");
Ctlp_FormulaPrint(vis_stdout,rightFormula);
fprintf(vis_stdout,
"\n------------------------------------------------\n");
}
Covstates2 = CoveredStatesHoskote(frstrchstates, fsm, rightFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity, dcLevel,
buildOnionRing, GSHschedule, signalList,
statesCoveredList, newCoveredStatesList,
statesToRemoveList);
mdd_free(frstrchstates);
result = mdd_or(Covstates1,Covstates2,1,1);
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(Covstates1);
mdd_free(Covstates2);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
if (formulaType == Ctlp_AF_c)
Ctlp_FormulaFree(OrigFormula);
mdd_free(temp1);
mdd_free(startstates);
return result;
break;
}
case Ctlp_AND_c:{
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"---Computing coverage for LHS sub-formula: ");
Ctlp_FormulaPrint(vis_stdout,leftFormula);
fprintf(vis_stdout,
"\n------------------------------------------------\n");
}
Covstates1 = CoveredStatesHoskote(startstates,fsm, leftFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel, buildOnionRing,
GSHschedule, signalList,
statesCoveredList, newCoveredStatesList,
statesToRemoveList);
rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"---Computing coverage for RHS sub-formula: ");
Ctlp_FormulaPrint(vis_stdout,rightFormula);
fprintf(vis_stdout,
"\n------------------------------------------------\n");
}
Covstates2 = CoveredStatesHoskote(startstates,fsm, rightFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity, dcLevel,
buildOnionRing,GSHschedule, signalList,
statesCoveredList, newCoveredStatesList,
statesToRemoveList);
result = mdd_or(Covstates1, Covstates2, 1, 1);
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(Covstates1);
mdd_free(Covstates2);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
mdd_free(startstates);
return result;
break;
}
case Ctlp_THEN_c:{ /*f1 -> f2 = !f2 -> !f1*/
mdd_t *nextstartstates, *Tb;
if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadLeftChild(OrigFormula))) { /*if f1 is propositional*/
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
} else if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadRightChild(OrigFormula))) { /*if f2 is propositional*/
/* Convert f1->f2 to !f2->!f1 */
leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
rightFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
} else { /*neither are propositional*/
fprintf(vis_stdout,"\nCan't compute coverage of implications where neither side is propositional\n");
fprintf(vis_stdout,"Could not compute coverage of :");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
result = mdd_zero(Fsm_FsmReadMddManager(fsm));
mdd_free(startstates);
return result;
}
existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
Tb = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel, buildOnionRing,GSHschedule);
Ctlp_FormulaFree(existFormula);
nextstartstates = mdd_and(startstates, Tb,1,1);
mdd_free(Tb);
Covstates1 = CoveredStatesHoskote(nextstartstates,fsm, rightFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity, dcLevel,
buildOnionRing,GSHschedule, signalList,
statesCoveredList, newCoveredStatesList,
statesToRemoveList);
mdd_free(nextstartstates);
mdd_free(startstates);
return Covstates1;
break;
}
case Ctlp_XOR_c: {
tmp_formula = Ctlp_FormulaConvertXORtoOR(OrigFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n--Converting XOR to AND and OR from:\n");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\nto\n");
Ctlp_FormulaPrint(vis_stdout, tmp_formula);
fprintf(vis_stdout,"\n");
}
result = CoveredStatesHoskote(startstates, fsm, tmp_formula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType, verbosity, dcLevel,buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
mdd_free(startstates);
return result;
break;
}
case Ctlp_EQ_c: {
tmp_formula = Ctlp_FormulaConvertEQtoOR(OrigFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n--Converting EQ to AND and OR from:\n");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\nto\n");
Ctlp_FormulaPrint(vis_stdout, tmp_formula);
fprintf(vis_stdout,"\n");
}
result = CoveredStatesHoskote(startstates, fsm, tmp_formula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType, verbosity, dcLevel,buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
mdd_free(startstates);
return result;
break;
}
case Ctlp_OR_c:{ /*f1+f2 = !f1 -> f2 = !f2 -> f1*/
mdd_t *nextstartstates, *Tb;
if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadLeftChild(OrigFormula))) { /*if f1 is propositional*/
/* Convert f1+f2 to !f1->f2 */
leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
} else if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadRightChild(OrigFormula))) { /*if f2 is propositional*/
/* Convert f1+f2 to !f2->f1 */
leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
rightFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
} else { /*neither are propositional*/
fprintf(vis_stdout,"\nCan't compute coverage of disjunctions where neither side is propositional\n");
fprintf(vis_stdout,"Could not compute coverage of :");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
result = mdd_zero(Fsm_FsmReadMddManager(fsm));
mdd_free(startstates);
return result;
}
existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
Tb = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel, buildOnionRing,GSHschedule);
Ctlp_FormulaFree(existFormula);
Ctlp_FormulaFree(leftFormula);
nextstartstates = mdd_and(startstates, Tb,1,1);
mdd_free(Tb);
Covstates1 = CoveredStatesHoskote(nextstartstates,fsm, rightFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity, dcLevel,
buildOnionRing,GSHschedule, signalList,
statesCoveredList, newCoveredStatesList,
statesToRemoveList);
mdd_free(nextstartstates);
mdd_free(startstates);
return Covstates1;
break;
}
case Ctlp_NOT_c:{ /*include code for checking for 2 NOTs*/
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
if (!(Ctlp_FormulaTestIsQuantifierFree(leftFormula))) {
tmp_formula = Ctlp_FormulaPushNegation(leftFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n--Pushing down negation one level. Converting formula from:\n");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\nto\n");
Ctlp_FormulaPrint(vis_stdout,tmp_formula);
fprintf(vis_stdout,"\n");
}
Covstates1 = CoveredStatesHoskote(startstates, fsm, tmp_formula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing,GSHschedule,
signalList, statesCoveredList,
newCoveredStatesList,
statesToRemoveList);
Ctlp_FormulaFree(tmp_formula);
result = mdd_and(Covstates1,fairStates,1,1);
mdd_free(Covstates1);
mdd_free(startstates);
return result;
#if 0
fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL\n");
fprintf(vis_stdout,"** can't compute coverage of : ");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\n");
mdd_free(startstates);
return mdd_zero(Fsm_FsmReadMddManager(fsm));
#endif
} else { /*this part of the code is now never executed*/
fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
mdd_free(startstates);
return mdd_zero(Fsm_FsmReadMddManager(fsm));
}
break;
}
case Ctlp_TRUE_c:
case Ctlp_FALSE_c: {
if (verbosity > McVerbosityNone_c)
fprintf(vis_stdout,"No observable signal, hence no coverage\n");
result = mdd_zero(Fsm_FsmReadMddManager(fsm));
mdd_free(startstates);
return result;
break;
}
case Ctlp_ID_c:{ /*should not reach here*/
fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
mdd_free(startstates);
return mdd_zero(Fsm_FsmReadMddManager(fsm));
break;
}
default:
fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
break;
}
assert(0);
return NIL(mdd_t);
} /* CoveredStatesHoskote */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes a the set of covered states for a given formula and initial set of states given. ]
Description [Works for a larger subset of CTL than CoveredStatesHoskote.]
SideEffects [Updates running totals.]
SeeAlso [McEstimateCoverage CoveredStatesHoskote]
Definition at line 1165 of file mcCover.c.
{
mdd_t *Covstates1, *temp1, *temp2;
mdd_t *Covstates2;
mdd_t *result;
mdd_t *travstates;
mdd_t *frstrchstates;
mdd_t *startstates;
Ctlp_FormulaType formulaType;
Ctlp_Formula_t *rightFormula, *leftFormula, *tmp_formula, *existFormula;
double numresultstates; /* used for debugging <NJ> */
startstates = mdd_and(startstates_old,fairStates,1,1);
if (mdd_is_tautology(startstates,0)) {
if (verbosity > McVerbosityNone_c)
fprintf(vis_stdout,
"\n--Startstates are down to zero. Coverage is hence zero.\n");
result = mdd_zero(Fsm_FsmReadMddManager(fsm));
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(startstates);
return result;
}
if (Ctlp_FormulaTestIsQuantifierFree(OrigFormula)) {
/* propositional formula */
result = CoveragePropositional(startstates, fsm, OrigFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel,buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
mdd_free(startstates);
return result;
}
formulaType = Ctlp_FormulaReadType(OrigFormula);
switch (formulaType) {
case Ctlp_EG_c: {/*EGp = p * EX(EGp) => C(So,EGp) = C(So,p) */
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n--Computing underapproximation for EG formula:\n");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\n");
}
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
result = CoveredStatesImproved(startstates, fsm, leftFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel,buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
mdd_free(startstates);
return result;
break;
}
case Ctlp_EF_c: {
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n--Computing underapproximation for EF formula:\n");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\n");
}
tmp_formula = Ctlp_FormulaConvertEFtoOR(OrigFormula);
result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType, verbosity, dcLevel,buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
Ctlp_FormulaFree(tmp_formula);
mdd_free(startstates);
return result;
break;
}
case Ctlp_EU_c: {
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n--Computing underapproximation for EU formula: ");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\n");
}
tmp_formula = Ctlp_FormulaConvertEUtoOR(OrigFormula);
result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel,buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList,statesToRemoveList);
mdd_free(startstates);
return result;
break;
}
case Ctlp_FwdU_c:
case Ctlp_FwdG_c:
case Ctlp_EY_c:
case Ctlp_EH_c:
case Ctlp_Cmp_c:
case Ctlp_EX_c:
case Ctlp_Init_c: {
fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL,\n");
fprintf(vis_stdout,"** can't compute coverage of : ");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\n");
result = mdd_zero(Fsm_FsmReadMddManager(fsm));
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(startstates);
return result;
break;
}
case Ctlp_AX_c:{
temp1 = Mc_FsmEvaluateEYFormula(fsm, startstates, fairStates, careStatesArray, verbosity, dcLevel);
Covstates1 = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
result = CoveredStatesImproved(Covstates1, fsm, leftFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel,buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(Covstates1);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
mdd_free(startstates);
return result;
break;
}
case Ctlp_AG_c:{
double numststates;
mdd_t *initStates;
initStates = Fsm_FsmComputeInitialStates(fsm);
temp1 = mdd_one(Fsm_FsmReadMddManager(fsm));
if (mdd_equal_mod_care_set_array(startstates,initStates,careStatesArray)) {
if (verbosity > McVerbosityNone_c)
fprintf(vis_stdout,"\nUsing the reachable states already computed...");
temp2 = Fsm_FsmComputeReachableStates(fsm, 0, 1, 0, 0, 0, 0, 0,
Fsm_Rch_Default_c, 0, 0,
NIL(array_t), FALSE, NIL(array_t));
} else
temp2 = Mc_FsmEvaluateFwdUFormula(fsm, startstates, temp1, fairStates,
careStatesArray, NIL(array_t),
verbosity, dcLevel);
mdd_free(initStates);
#if 0
temp2 = McForwardReachable(fsm, startstates, temp1, fairStates,
careStatesArray, NIL(array_t),verbosity,
dcLevel);
#endif
numststates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),startstates,
Fsm_FsmReadPresentStateVars(fsm));
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),temp2,
Fsm_FsmReadPresentStateVars(fsm));
#if 0
fprintf(vis_stdout,"\nNum of forward reachable states from %.0f startstates = %.0f\n",numststates,numresultstates);
#endif
mdd_free(temp1);
Covstates1 = mdd_and(temp2,fairStates,1,1);
mdd_free(temp2);
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
result = CoveredStatesImproved(Covstates1, fsm, leftFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel, buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(Covstates1);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
mdd_free(startstates);
return result;
break;
}
case Ctlp_AF_c:{
tmp_formula = OrigFormula;
OrigFormula = Ctlp_FormulaConvertAFtoAU(tmp_formula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"Converting formula from\n");
Ctlp_FormulaPrint(vis_stdout,tmp_formula);
fprintf(vis_stdout,"\nto\n");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\n");
}
#if 0
Ctlp_FormulaFree(tmp_formula);
formulaType = Ctlp_AU_c;
#endif
/* convert to AFp to A (TRUE) U p and then step thru to do coverage
for AU computation below*/
}
case Ctlp_AU_c:{
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
tmp_formula = Ctlp_FormulaCreate(Ctlp_OR_c,leftFormula,rightFormula);
CtlpFormulaIncrementRefCount(leftFormula);
CtlpFormulaIncrementRefCount(rightFormula);
travstates = traverse(fsm, fairStates, fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType, verbosity,
dcLevel, buildOnionRing, GSHschedule, startstates,
leftFormula, rightFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n---Computing coverage for LHS of U formula i.e: ");
Ctlp_FormulaPrint(vis_stdout,leftFormula);
fprintf(vis_stdout,
"\n------------------------------------------------\n");
}
Covstates1 = CoveredStatesImproved(travstates, fsm, tmp_formula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing, GSHschedule,
signalList, statesCoveredList,
newCoveredStatesList,
statesToRemoveList);
mdd_free(travstates);
Ctlp_FormulaFree(tmp_formula);
frstrchstates = firstReached(fsm, fairStates, fairCondition,
careStatesArray, earlyTermination, hintsArray,
hintType, verbosity, dcLevel, buildOnionRing,
GSHschedule,startstates,rightFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n---Computing coverage for RHS of U formula i.e: ");
Ctlp_FormulaPrint(vis_stdout,rightFormula);
fprintf(vis_stdout,
"\n------------------------------------------------\n");
}
Covstates2 = CoveredStatesImproved(frstrchstates, fsm, rightFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing, GSHschedule,
signalList, statesCoveredList,
newCoveredStatesList,
statesToRemoveList);
mdd_free(frstrchstates);
result = mdd_or(Covstates1,Covstates2,1,1);
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(Covstates1);
mdd_free(Covstates2);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
if (formulaType == Ctlp_AF_c)
Ctlp_FormulaFree(OrigFormula);
mdd_free(temp1);
mdd_free(startstates);
return result;
break;
}
case Ctlp_AND_c:{
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n---Computing coverage for LHS sub-formula: ");
Ctlp_FormulaPrint(vis_stdout,leftFormula);
fprintf(vis_stdout,
"\n------------------------------------------------\n");
}
Covstates1 = CoveredStatesImproved(startstates,fsm, leftFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing,GSHschedule,
signalList, statesCoveredList,
newCoveredStatesList,
statesToRemoveList);
rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n---Computing coverage for RHS sub-formula: ");
Ctlp_FormulaPrint(vis_stdout,rightFormula);
fprintf(vis_stdout,
"\n------------------------------------------------\n");
}
Covstates2 = CoveredStatesImproved(startstates,fsm, rightFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing,GSHschedule,
signalList, statesCoveredList,
newCoveredStatesList,
statesToRemoveList);
result = mdd_or(Covstates1,Covstates2,1,1);
numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
Fsm_FsmReadPresentStateVars(fsm));
mdd_free(Covstates1);
mdd_free(Covstates2);
temp1 = result;
result = mdd_and(temp1,fairStates,1,1);
mdd_free(temp1);
mdd_free(startstates);
return result;
break;
}
case Ctlp_THEN_c:{ /*f1 -> f2 = !f2 -> !f1*/
int sigarr;
array_t *listOfF2Signals = array_alloc(char *,0);
array_t *listOfF1Signals = array_alloc(char *,0);
array_t *newstatesToRemoveList = NIL(array_t);
mdd_t *nextstartstates, *Tb, *tmp_mdd;
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
fairStates, fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel, buildOnionRing,GSHschedule);
Ctlp_FormulaFree(existFormula);
nextstartstates = mdd_and(startstates, Tb,1,1);
mdd_free(Tb);
/*To compute C(So*T(f1),f2), *
*first compute states to remove*/
newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
findallsignalsInFormula(listOfF2Signals,rightFormula); /*find all signals in f2*/
for (sigarr=0;sigarr<array_n(listOfF2Signals);sigarr++) {
/*for all signals in f2*/
mdd_t *tmp_mdd2;
char *signalInF2;
int positionInGlobalList;
int rangeOfF2SigInF1;
signalInF2 = array_fetch(char *,listOfF2Signals,sigarr);
positionInGlobalList = positionOfSignalinList(signalInF2,signalList);
if (positionInGlobalList < 0) /*shouldn't happen*/
fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
rangeOfF2SigInF1 = RangeofSignalinFormula(fsm,signalInF2,leftFormula);
tmp_mdd = mdd_dup(nextstartstates);
if (rangeOfF2SigInF1 > 0) { /*signal in F2 also in F1*/
if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if f1 is propositional*/
tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity, dcLevel,
buildOnionRing, GSHschedule, signalInF2,
tmp_mdd);
mdd_free(tmp_mdd);
tmp_mdd = tmp_mdd2;
}
tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
positionInGlobalList);
if (tmp_mdd2 != NIL(mdd_t))
mdd_free(tmp_mdd2);
array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
tmp_mdd);
} else {
mdd_free(tmp_mdd);
}
}
Covstates1 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing, GSHschedule,
signalList, statesCoveredList,
newCoveredStatesList,
newstatesToRemoveList);
mdd_free(nextstartstates);
mdd_array_free(newstatesToRemoveList);
array_free(listOfF2Signals);
/*End of coverage computation of f2*/
/*Now simillar computation for !f1 *
* Convert f1->f2 to !f2->!f1 */
leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
rightFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
fairStates, fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel, buildOnionRing,GSHschedule);
Ctlp_FormulaFree(existFormula);
nextstartstates = mdd_and(startstates, Tb, 1, 1);
mdd_free(Tb);
newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
findallsignalsInFormula(listOfF1Signals,rightFormula);/*find all signals in !f1*/
for (sigarr=0;sigarr<array_n(listOfF1Signals);sigarr++) {
/*for all signals in !f1*/
mdd_t *tmp_mdd2;
char *signalInNotF1;
int positionInGlobalList;
int rangeOfNotF1SigInNotF2;
signalInNotF1 = array_fetch(char *,listOfF1Signals,sigarr);
positionInGlobalList = positionOfSignalinList(signalInNotF1,signalList);
if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
rangeOfNotF1SigInNotF2 = RangeofSignalinFormula(fsm,signalInNotF1,leftFormula);
tmp_mdd = mdd_dup(nextstartstates);
if (rangeOfNotF1SigInNotF2 > 0) {/*signal in !F1 also in !F2*/
if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if !f2 is propositional*/
tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity, dcLevel,
buildOnionRing, GSHschedule, signalInNotF1,
tmp_mdd);
mdd_free(tmp_mdd);
tmp_mdd = tmp_mdd2;
}
tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
positionInGlobalList);
if (tmp_mdd2 != NIL(mdd_t))
mdd_free(tmp_mdd2);
array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
tmp_mdd);
} else {
mdd_free(tmp_mdd);
}
}
Ctlp_FormulaFree(leftFormula);
Covstates2 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing,GSHschedule,
signalList, statesCoveredList,
newCoveredStatesList,
newstatesToRemoveList);
mdd_free(nextstartstates);
mdd_array_free(newstatesToRemoveList);
array_free(listOfF1Signals);
/*End of coverage computation of !f1*/
Ctlp_FormulaFree(rightFormula);
result = mdd_or(Covstates1,Covstates2,1,1);
mdd_free(Covstates1);
mdd_free(Covstates2);
mdd_free(startstates);
return result;
break;
}
case Ctlp_XOR_c: {
tmp_formula = Ctlp_FormulaConvertXORtoOR(OrigFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n--Converting XOR to AND and OR from:\n");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\nto\n");
Ctlp_FormulaPrint(vis_stdout, tmp_formula);
fprintf(vis_stdout,"\n");
}
result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel,buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
mdd_free(startstates);
return result;
break;
}
case Ctlp_EQ_c: {
tmp_formula = Ctlp_FormulaConvertEQtoOR(OrigFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n--Converting EQ to AND and OR");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\nto\n");
Ctlp_FormulaPrint(vis_stdout, tmp_formula);
fprintf(vis_stdout,"\n");
}
result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel,buildOnionRing,
GSHschedule, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList);
mdd_free(startstates);
return result;
break;
}
case Ctlp_OR_c:{ /*f1+f2 = !f1 -> f2 = !f2 -> f1*/
int sigarr;
array_t *listOfF2Signals = array_alloc(char *,0);
array_t *listOfF1Signals = array_alloc(char *,0);
array_t *newstatesToRemoveList = NIL(array_t);
mdd_t *nextstartstates, *Tb, *tmp_mdd;
/*To compute C(So*T(!f1),f2), *
*convert to form like !f1->f2 */
leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
fairStates, fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel, buildOnionRing,GSHschedule);
Ctlp_FormulaFree(existFormula);
nextstartstates = mdd_and(startstates, Tb, 1, 1);
mdd_free(Tb);
/*first compute states to remove*/
newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
findallsignalsInFormula(listOfF2Signals,rightFormula);/*find all signals in f2*/
for (sigarr=0;sigarr<array_n(listOfF2Signals);sigarr++) {
/*for all signals in f2*/
mdd_t *tmp_mdd2;
char *signalInF2;
int positionInGlobalList;
int rangeOfF2SigInF1;
signalInF2 = array_fetch(char *,listOfF2Signals,sigarr);
positionInGlobalList = positionOfSignalinList(signalInF2,signalList);
if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
rangeOfF2SigInF1 = RangeofSignalinFormula(fsm,signalInF2,leftFormula);
tmp_mdd = mdd_dup(nextstartstates);
if (rangeOfF2SigInF1 > 0) {/*signal in F2 also in F1*/
if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if f1 is propositional*/
tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity, dcLevel,
buildOnionRing, GSHschedule, signalInF2,
tmp_mdd);
mdd_free(tmp_mdd);
tmp_mdd = tmp_mdd2;
}
tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
positionInGlobalList);
if (tmp_mdd2 != NIL(mdd_t))
mdd_free(tmp_mdd2);
array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
tmp_mdd);
} else {
mdd_free(tmp_mdd);
}
}
Ctlp_FormulaFree(leftFormula);
Covstates1 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing,GSHschedule,
signalList, statesCoveredList,
newCoveredStatesList,
newstatesToRemoveList);
mdd_free(nextstartstates);
mdd_array_free(newstatesToRemoveList);
array_free(listOfF2Signals);
/*End of coverage computation of f2*/
/*Now simillar computation for !f1 *
* Convert f1+f2 to !f2->f1 */
leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
rightFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
fairStates, fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
verbosity, dcLevel, buildOnionRing,GSHschedule);
Ctlp_FormulaFree(existFormula);
nextstartstates = mdd_and(startstates, Tb,1,1);
mdd_free(Tb);
newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
findallsignalsInFormula(listOfF1Signals,rightFormula);/*find all signals in f1*/
for (sigarr=0;sigarr<array_n(listOfF1Signals);sigarr++) {
/*for all signals in f1*/
mdd_t *tmp_mdd2;
char *signalInF1;
int positionInGlobalList;
int rangeOfF1SigInF2;
signalInF1 = array_fetch(char *,listOfF1Signals,sigarr);
positionInGlobalList = positionOfSignalinList(signalInF1,signalList);
if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
rangeOfF1SigInF2 = RangeofSignalinFormula(fsm,signalInF1,leftFormula);
tmp_mdd = mdd_dup(nextstartstates);
if (rangeOfF1SigInF2 > 0) {/*signal in !F1 also in !F2*/
if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if !f2 is propositional*/
tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity, dcLevel,
buildOnionRing, GSHschedule, signalInF1,
tmp_mdd);
mdd_free(tmp_mdd);
tmp_mdd = tmp_mdd2;
}
tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
positionInGlobalList);
if (tmp_mdd2 != NIL(mdd_t))
mdd_free(tmp_mdd2);
array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
tmp_mdd);
} else {
mdd_free(tmp_mdd);
}
}
Ctlp_FormulaFree(leftFormula);
Covstates2 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing,GSHschedule,
signalList, statesCoveredList,
newCoveredStatesList,
newstatesToRemoveList);
mdd_free(nextstartstates);
mdd_array_free(newstatesToRemoveList);
array_free(listOfF1Signals);
/*End of coverage computation of !f1*/
result = mdd_or(Covstates1,Covstates2,1,1);
mdd_free(Covstates1);
mdd_free(Covstates2);
mdd_free(startstates);
return result;
break;
}
case Ctlp_NOT_c:{ /*include code for checking for 2 NOTs*/
leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
if (!(Ctlp_FormulaTestIsQuantifierFree(leftFormula))) {
tmp_formula = Ctlp_FormulaPushNegation(leftFormula);
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout,"\n--Pushing down negation one level. Converting formula from:\n");
Ctlp_FormulaPrint(vis_stdout,OrigFormula);
fprintf(vis_stdout,"\nto\n");
Ctlp_FormulaPrint(vis_stdout,tmp_formula);
fprintf(vis_stdout,"\n");
}
Covstates1 = CoveredStatesImproved(startstates,fsm, tmp_formula,
fairStates, fairCondition,
careStatesArray, earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing,GSHschedule,
signalList, statesCoveredList,
newCoveredStatesList,
statesToRemoveList);
result = mdd_and(Covstates1,fairStates,1,1);
Ctlp_FormulaFree(tmp_formula);
mdd_free(Covstates1);
mdd_free(startstates);
return result;
} else { /*this part of the code is now never executed*/
fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
mdd_free(startstates);
return mdd_zero(Fsm_FsmReadMddManager(fsm));
}
break;
}
case Ctlp_TRUE_c:
case Ctlp_FALSE_c: {
if (verbosity > McVerbosityNone_c)
fprintf(vis_stdout,"No observable signal, hence no coverage\n");
result = mdd_zero(Fsm_FsmReadMddManager(fsm));
mdd_free(startstates);
return result;
break;
}
case Ctlp_ID_c:{ /*should not reach here*/
fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
mdd_free(startstates);
return mdd_zero(Fsm_FsmReadMddManager(fsm));
break;
}
default:
fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
mdd_free(startstates);
break;
}
assert(0);
return NIL(mdd_t);
} /* End of CoveredStatesImproved */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Used in the coverage code to gather all possible observable signals in a given formula and create necessary arrays]
Description []
SideEffects []
SeeAlso []
Definition at line 2318 of file mcCover.c.
{
Ntk_Network_t *network;
Ntk_Node_t *node;
Var_Variable_t *nodeVar;
char *nodeNameString;
int signalType;
Ctlp_Formula_t *leftFormula, *rightFormula;
if ( formula == NIL(Ctlp_Formula_t)) {
return;
}
if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c ) {
leftFormula = Ctlp_FormulaReadLeftChild(formula);
rightFormula = Ctlp_FormulaReadRightChild(formula);
findallsignals(fsm, signalTypeList, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList,
leftFormula, zeroMdd);
findallsignals(fsm, signalTypeList, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList,
rightFormula,zeroMdd);
}
else { /* atomic proposition */
nodeNameString = Ctlp_FormulaReadVariableName(formula);
if ((positionOfSignalinList(nodeNameString,signalList)) == -1) {
fprintf(vis_stdout,"Found new signal = %s\n",nodeNameString);
network = Fsm_FsmReadNetwork(fsm);
node = Ntk_NetworkFindNodeByName(network, nodeNameString);
nodeVar = Ntk_NodeReadVariable(node);
if (Var_VariableTestIsPI(nodeVar))
signalType = 1;
else if (Var_VariableTestIsPO(nodeVar))
signalType = 0;
else
signalType = 2;
array_insert_last(int,signalTypeList,signalType);
array_insert_last(char *,signalList,nodeNameString);
array_insert_last(mdd_t *,statesCoveredList,mdd_dup(zeroMdd));
array_insert_last(mdd_t *,newCoveredStatesList,mdd_dup(zeroMdd));
array_insert_last(mdd_t *,statesToRemoveList,mdd_dup(zeroMdd));
}
}
return;
} /* findallsignals */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void findallsignalsInFormula | ( | array_t * | signalList, |
| Ctlp_Formula_t * | formula | ||
| ) | [static] |
Function********************************************************************
Synopsis [Used in the coverage code to gather all possible observable signals in a given formula]
Description []
SideEffects []
SeeAlso []
Definition at line 2385 of file mcCover.c.
{
char *nodeNameString;
Ctlp_Formula_t *leftFormula, *rightFormula;
if ( formula == NIL(Ctlp_Formula_t)) {
return;
}
if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c ) {
leftFormula = Ctlp_FormulaReadLeftChild(formula);
rightFormula = Ctlp_FormulaReadRightChild(formula);
findallsignalsInFormula(signalList,leftFormula);
findallsignalsInFormula(signalList,rightFormula);
}
else { /* atomic proposition */
nodeNameString = Ctlp_FormulaReadVariableName(formula);
if ((positionOfSignalinList(nodeNameString,signalList)) == -1) {
array_insert_last(char *,signalList,nodeNameString);
}
}
return;
} /* findallsignalsInFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the following for use in coverage computation for AU: firstReached(So,f2) = (So ^ T(f2)) U firstReached(EY(So^T(!f2)),f2) where, T(f2) => Set of states satisfying f2 ]
Description []
SideEffects []
SeeAlso []
Definition at line 2176 of file mcCover.c.
{
int frstcnt;
mdd_t *temp1, *temp2, *oldSo, *CovStates, *Tf2, *Tnotf2, *zeroMDD;
Ctlp_Formula_t *tmp_formula, *existFormula;
oldSo = mdd_dup(startstates);
zeroMDD = mdd_zero(Fsm_FsmReadMddManager(fsm));
existFormula = Ctlp_FormulaConvertToExistentialForm(formula);
Tf2 = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType, verbosity,
dcLevel, buildOnionRing, GSHschedule);
Ctlp_FormulaFree(existFormula);
tmp_formula = Ctlp_FormulaConverttoComplement(formula);
existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
Tnotf2 = Mc_FsmEvaluateFormula(fsm, existFormula,
fairStates, fairCondition,
careStatesArray,earlyTermination,
hintsArray, hintType, verbosity,
dcLevel, buildOnionRing,GSHschedule);
Ctlp_FormulaFree(existFormula);
Ctlp_FormulaFree(tmp_formula);
CovStates = mdd_and(oldSo,Tf2,1,1);
temp1 = mdd_dup(oldSo);
temp2 = mdd_and(oldSo,Tnotf2,1,1);
frstcnt = 0;
while (!(mdd_equal_mod_care_set_array(temp2,zeroMDD,careStatesArray))) {
mdd_t *tmp_mdd1, *tmp_mdd2, *tmp_mdd;
tmp_mdd = Mc_FsmEvaluateEYFormula(fsm, temp2, fairStates, careStatesArray, verbosity, dcLevel); /*forward(So^Tnotf2)*/
tmp_mdd2 = mdd_and(tmp_mdd,Tf2,1,1);
tmp_mdd1 = CovStates;
CovStates = mdd_or(CovStates,tmp_mdd2,1,1); /*add on the new states*/
mdd_free(tmp_mdd1);
mdd_free(tmp_mdd2);
tmp_mdd1 = mdd_and(tmp_mdd,Tnotf2,1,1); /*newSo^Tnotf2*/
tmp_mdd2 = temp2;
temp2 = mdd_and(tmp_mdd1,temp1,1,0); /*take out the startstates already encountered temp2 = newSo*/
mdd_free(tmp_mdd2);
mdd_free(tmp_mdd1);
tmp_mdd1 = temp1;
temp1 = mdd_or(temp1,tmp_mdd,1,1);
mdd_free(tmp_mdd1);
mdd_free(tmp_mdd);
}
mdd_free(zeroMDD);
mdd_free(oldSo);
mdd_free(Tf2);
mdd_free(Tnotf2);
mdd_free(temp1);
mdd_free(temp2);
return CovStates;
} /* firstreached */
Here is the call graph for this function:
Here is the caller graph for this function:
| static Ctlp_Formula_t * FormulaConvertSignalComplement | ( | Fsm_Fsm_t * | fsm, |
| char * | signal, | ||
| Ctlp_Formula_t * | formula | ||
| ) | [static] |
Function********************************************************************
Synopsis [Duplicates a CTL formula but with a given signal's value complemented]
Description []
SideEffects [none]
SeeAlso []
Definition at line 2258 of file mcCover.c.
{
Ctlp_Formula_t *result = NIL(Ctlp_Formula_t);
Ctlp_Formula_t *leftChildConverted, *leftFormula;
Ctlp_Formula_t *rightChildConverted, *rightFormula;
Ntk_Network_t *network;
char *nodeNameString;
char *nodeValueString;
Ntk_Node_t *node;
Var_Variable_t *nodeVar;
if ( formula == NIL(Ctlp_Formula_t)) {
return NIL(Ctlp_Formula_t);
}
if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c ) {
leftFormula = Ctlp_FormulaReadLeftChild(formula);
leftChildConverted = FormulaConvertSignalComplement(fsm, signal,
leftFormula);
rightFormula = Ctlp_FormulaReadRightChild(formula);
rightChildConverted = FormulaConvertSignalComplement(fsm, signal,
rightFormula);
result = Ctlp_FormulaCreate(Ctlp_FormulaReadType(formula),
leftChildConverted,rightChildConverted);
}
else { /* if atomic proposition*/
network = Fsm_FsmReadNetwork(fsm);
nodeNameString = Ctlp_FormulaReadVariableName(formula);
nodeValueString = Ctlp_FormulaReadValueName(formula);
node = Ntk_NetworkFindNodeByName(network, nodeNameString);
nodeVar = Ntk_NodeReadVariable(node);
if ((strcmp(signal,nodeNameString)) != 0) { /* not the signal that we want to flip */
result = Ctlp_FormulaCreate(Ctlp_FormulaReadType(formula),
(Ctlp_Formula_t *) util_strsav(nodeNameString),
(Ctlp_Formula_t *) util_strsav(nodeValueString));
}
else { /* this is the signal that we want to flip */
result = Ctlp_FormulaConverttoComplement(formula);
}
}
return result;
} /* FormulaConvertSignalComplement */
Here is the call graph for this function:
Here is the caller graph for this function:
| void McEstimateCoverage | ( | Fsm_Fsm_t * | modelFsm, |
| Ctlp_Formula_t * | ctlFormula, | ||
| int | i, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | fairCond, | ||
| array_t * | modelCareStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| array_t * | hintsStatesArray, | ||
| Mc_GuidedSearch_t | guidedSearchType, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| int | buildOnionRings, | ||
| Mc_GSHScheduleType | GSHschedule, | ||
| Mc_FwdBwdAnalysis | traversalDirection, | ||
| mdd_t * | modelInitialStates, | ||
| mdd_t * | ctlFormulaStates, | ||
| mdd_t ** | totalcoveredstates, | ||
| array_t * | signalTypeList, | ||
| array_t * | signalList, | ||
| array_t * | statesCoveredList, | ||
| array_t * | newCoveredStatesList, | ||
| array_t * | statesToRemoveList, | ||
| boolean | performCoverageHoskote, | ||
| boolean | performCoverageImproved | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Estimate coverage of one CTL formula.]
Description [Depending on the options, this function applies either the original algorithm of Hoskote et al. or the improved algorithm of Jayakumar et al.. It then prints statistics on coverage (if the formula passes).]
SideEffects [Updates running totals]
SeeAlso [CommandMc CoveredStatesHoskote CoveredStatesImproved McPrintCoverageSummary]
Definition at line 134 of file mcCover.c.
{
double numtotcoveredstates;
double numnewcoveredstates;
mdd_t *CovstatesHoskote;
mdd_t *CovstatesImproved;
Ctlp_Formula_t *origFormula;
if (performCoverageHoskote &&
(modelCareStatesArray != NIL(array_t))) { /* and no errors till now? */
mdd_t *tmp_mdd, *zero_mdd;
int sigarr;
array_t *listOfSignals = array_alloc(char *,0);
origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
if ( ( (traversalDirection == McFwd_c) && bdd_is_tautology(ctlFormulaStates, 1) ) ||
mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1) ) { /* formula passes */
if (*totalcoveredstates == NIL(mdd_t))
*totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
/* add new signals if any found */
zero_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
findallsignals(modelFsm, signalTypeList, signalList,
statesCoveredList, newCoveredStatesList,
statesToRemoveList, origFormula,
zero_mdd);
mdd_free(zero_mdd);
fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
fprintf(vis_stdout,"===================================\n");
CovstatesHoskote = CoveredStatesHoskote(modelInitialStates,
modelFsm, origFormula,
fairStates, fairCond,
modelCareStatesArray,
earlyTermination,
hintsStatesArray,
guidedSearchType, verbosity,
dcLevel, buildOnionRings,
GSHschedule, signalList,
statesCoveredList,
newCoveredStatesList,
statesToRemoveList);
numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
CovstatesHoskote,
Fsm_FsmReadPresentStateVars(modelFsm));
tmp_mdd = mdd_and(CovstatesHoskote,*totalcoveredstates,1,0);
numnewcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
tmp_mdd,
Fsm_FsmReadPresentStateVars(modelFsm));
mdd_free(tmp_mdd);
fprintf(vis_stdout,"\n--Total states covered by formula<%d> = %.0f , new = %.0f\n",i+1,
numtotcoveredstates,numnewcoveredstates);
findallsignalsInFormula(listOfSignals,origFormula);
for (sigarr=0;sigarr<array_n(listOfSignals);sigarr++) {
mdd_t *newCoveredStates,*statesCovered,*tmp_mdd;
char *signalInFormula;
int positionInList;
signalInFormula = array_fetch(char *,listOfSignals,sigarr);
positionInList = positionOfSignalinList(signalInFormula,signalList);
newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList);
statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList);
tmp_mdd = mdd_and(newCoveredStates,statesCovered,1,0); /*newly covered States*/
fprintf(vis_stdout,"---States covered w.r.t. %s = %.0f, new = %.0f\n",
signalInFormula,
mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
newCoveredStates,
Fsm_FsmReadPresentStateVars(modelFsm)),
mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
tmp_mdd,
Fsm_FsmReadPresentStateVars(modelFsm)));
mdd_free(tmp_mdd);
/* add on the newcoveredstates*/
tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1);
mdd_free(statesCovered);
/*update statesCoveredList*/
array_insert(mdd_t *,statesCoveredList,positionInList,tmp_mdd);
mdd_free(newCoveredStates);
/* reset newCoveredStatesList to zeroMdds for the next formula */
tmp_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd);
}
} else { /* formula fails */
CovstatesHoskote = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
fprintf(vis_stdout,"===================================\n");
fprintf(vis_stdout,"Coverage for failing formulae = 0\n");
}
if (*totalcoveredstates == NIL(mdd_t))
*totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
if (CovstatesHoskote != NIL(mdd_t)){
mdd_t *tmp_mdd = mdd_or(*totalcoveredstates,CovstatesHoskote,1,1);
mdd_free(*totalcoveredstates);
*totalcoveredstates = tmp_mdd;
}
numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
*totalcoveredstates,
Fsm_FsmReadPresentStateVars(modelFsm));
mdd_free(CovstatesHoskote);
array_free(listOfSignals);
}
if (performCoverageImproved && (modelCareStatesArray != NIL(array_t))) { /* and no errors till now ??*/
mdd_t *tmp_mdd, *zero_mdd;
int sigarr;
array_t *listOfSignals = array_alloc(char *,0);
origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
if ( ( (traversalDirection == McFwd_c) &&
bdd_is_tautology(ctlFormulaStates, 1) ) ||
(mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1)) ) {
/* formula passes */
if (*totalcoveredstates == NIL(mdd_t))
*totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
/*add new signals if any found*/
zero_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
findallsignals(modelFsm, signalTypeList, signalList,
statesCoveredList, newCoveredStatesList,
statesToRemoveList, origFormula, zero_mdd);
mdd_free(zero_mdd);
fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
fprintf(vis_stdout,"===================================\n");
CovstatesImproved = CoveredStatesImproved(modelInitialStates,
modelFsm, origFormula,
fairStates, fairCond,
modelCareStatesArray,
earlyTermination,
hintsStatesArray,
guidedSearchType,
verbosity,
dcLevel, buildOnionRings,
GSHschedule, signalList,
statesCoveredList,
newCoveredStatesList,
statesToRemoveList);
numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
CovstatesImproved,
Fsm_FsmReadPresentStateVars(modelFsm));
tmp_mdd = mdd_and(CovstatesImproved,*totalcoveredstates,1,0);
numnewcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
tmp_mdd,
Fsm_FsmReadPresentStateVars(modelFsm));
mdd_free(tmp_mdd);
fprintf(vis_stdout,"\n--Total states covered by formula<%d> = %.0f , new = %.0f\n",i+1,
numtotcoveredstates,numnewcoveredstates);
findallsignalsInFormula(listOfSignals,origFormula);
for (sigarr=0;sigarr<array_n(listOfSignals);sigarr++) {
mdd_t *newCoveredStates,*statesCovered,*tmp_mdd;
char *signalInFormula;
int positionInList;
signalInFormula = array_fetch(char *,listOfSignals,sigarr);
positionInList = positionOfSignalinList(signalInFormula,signalList);
newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList);
statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList);
tmp_mdd = mdd_and(newCoveredStates,statesCovered,1,0); /*newly covered States*/
fprintf(vis_stdout,"---States covered w.r.t. %s = %.0f, new = %.0f\n",
signalInFormula,
mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
newCoveredStates,
Fsm_FsmReadPresentStateVars(modelFsm)),
mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
tmp_mdd,
Fsm_FsmReadPresentStateVars(modelFsm)));
mdd_free(tmp_mdd);
/* add on the newcoveredstates*/
tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1);
mdd_free(statesCovered);
/*update statesCoveredList*/
array_insert(mdd_t *,statesCoveredList,positionInList,tmp_mdd);
mdd_free(newCoveredStates);
/* reset newCoveredStatesList to zeroMdds for the next formula */
tmp_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd);
}
} else { /* formula fails */
CovstatesImproved = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
fprintf(vis_stdout,"===================================\n");
fprintf(vis_stdout,"Coverage for failing formulae = 0\n");
}
if (*totalcoveredstates == NIL(mdd_t))
*totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
if (CovstatesImproved != NIL(mdd_t)){
mdd_t *tmp_mdd = mdd_or(*totalcoveredstates,CovstatesImproved,1,1);
mdd_free(*totalcoveredstates);
*totalcoveredstates = tmp_mdd;
}
numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
*totalcoveredstates,
Fsm_FsmReadPresentStateVars(modelFsm));
mdd_free(CovstatesImproved);
array_free(listOfSignals);
}
} /* McEstimateCoverage */
Here is the call graph for this function:
Here is the caller graph for this function:
| void McPrintCoverageSummary | ( | Fsm_Fsm_t * | modelFsm, |
| Mc_DcLevel | dcLevel, | ||
| McOptions_t * | options, | ||
| array_t * | modelCareStatesArray, | ||
| mdd_t * | modelCareStates, | ||
| mdd_t * | totalcoveredstates, | ||
| array_t * | signalTypeList, | ||
| array_t * | signalList, | ||
| array_t * | statesCoveredList, | ||
| boolean | performCoverageHoskote, | ||
| boolean | performCoverageImproved | ||
| ) |
Function********************************************************************
Synopsis [Print summary for the coverage of a property file.]
SideEffects [none]
SeeAlso [CommandMc McEstimateCoverage]
Definition at line 380 of file mcCover.c.
{
float coverage;
float coveragePI;
float coveragePO;
float coverageOther;
float numPI;
float numPO;
float numOther;
float avgCoverage;
float avgPICoverage;
float avgPOCoverage;
float avgOtherCoverage;
double numrchstates;
double numtotcoveredstates;
if (performCoverageHoskote &&
(modelCareStatesArray != NIL(array_t))) { /* and no errors till now */
int sigarr;
if (totalcoveredstates != NIL(mdd_t) && (modelCareStates != NIL(mdd_t))) {
numtotcoveredstates = mdd_count_onset(
Fsm_FsmReadMddManager(modelFsm),
totalcoveredstates,
Fsm_FsmReadPresentStateVars(modelFsm));
}
else {
numtotcoveredstates = 0;
}
if ((dcLevel == McDcLevelRch_c)||(dcLevel == McDcLevelRchFrontier_c)) {
if (!mdd_lequal(totalcoveredstates, modelCareStates, 1, 1)) {
(void)fprintf(vis_stdout,
"** mc warning: Some of the covered states are not reachable\n");
}
if (modelCareStates !=NIL(mdd_t)){
int sigType;
coveragePI = 0;
coveragePO = 0;
coverageOther = 0;
numPI = 0;
numPO = 0;
numOther = 0;
avgCoverage = 0;
avgPICoverage = 0;
avgPOCoverage = 0;
avgOtherCoverage = 0;
numrchstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
modelCareStates,
Fsm_FsmReadPresentStateVars(modelFsm));
if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
fprintf(vis_stdout,"\nCoverage for all the Formulae w.r.t. all observable signals\n");
fprintf(vis_stdout,"=============================================================\n");
}
for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
mdd_t *statesCovered, *uncoveredStateCube, *uncoveredStates;
double numStatesCovered;
char *nrOfUncoveredStatesString;
int nrOfUncoveredStates, prntStates; /* nr of uncovered states that we output */
Ntk_Network_t *modelNetworkC = Fsm_FsmReadNetwork(modelFsm);
array_t *PSVarsC = Fsm_FsmReadPresentStateVars(modelFsm);
mdd_manager *mddMgrC = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
coverage = (numStatesCovered / numrchstates) * 100;
avgCoverage = avgCoverage + coverage;
sigType = array_fetch(int, signalTypeList,sigarr);
if (sigType == 1) {
coveragePI = coveragePI + numStatesCovered;
avgPICoverage = avgPICoverage + coverage;
numPI = numPI + 1;
}
else if (sigType == 0) {
coveragePO = coveragePO + numStatesCovered;
avgPOCoverage = avgPOCoverage + coverage;
numPO = numPO + 1;
}
else {
coverageOther = coverageOther + numStatesCovered;
avgOtherCoverage = avgOtherCoverage + coverage;
numOther = numOther + 1;
}
if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
fprintf(vis_stdout,"\n# States covered w.r.t. %s = %.0f, Percentage of Coverage = %f\n",
array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
nrOfUncoveredStatesString = Cmd_FlagReadByName("nr_uncoveredstates");
if(nrOfUncoveredStatesString == NIL(char))
nrOfUncoveredStates = 1;
else
nrOfUncoveredStates = atoi(nrOfUncoveredStatesString);
if (numStatesCovered < numrchstates) {
if ((numrchstates-numStatesCovered) < nrOfUncoveredStates)
nrOfUncoveredStates = (int)(numrchstates-numStatesCovered);
fprintf(vis_stdout,"#Printing reachable states NOT covered w.r.t. %s :\n",array_fetch(char *,signalList,sigarr));
for (prntStates = 0;prntStates<nrOfUncoveredStates;prntStates++){
fprintf(vis_stdout,"\n#State %d :\n",prntStates+1);
uncoveredStates = mdd_and(modelCareStates,statesCovered,1,0);
uncoveredStateCube = Mc_ComputeAMinterm(uncoveredStates, PSVarsC, mddMgrC);
mdd_free(uncoveredStates);
Mc_MintermPrint(uncoveredStateCube, PSVarsC, modelNetworkC);
mdd_free(uncoveredStateCube);
}
}
}
}
fprintf(vis_stdout,"\nTotal Coverage for all the Formulae\n");
fprintf(vis_stdout,"=====================================\n");
for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
mdd_t *statesCovered;
double numStatesCovered;
char *type;
int sigType;
sigType = array_fetch(int, signalTypeList,sigarr);
if (sigType == 1)
type = "Primary Input";
else if (sigType == 0)
type = "Primary Output";
else
type = "Neither Primary output nor input";
statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
coverage = (numStatesCovered / numrchstates) * 100;
fprintf(vis_stdout,"# States covered w.r.t. %s(%s) = %.0f, Percentage of Coverage = %f\n",type,
array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
}
fprintf(vis_stdout,"--There are %.0f covered states (using Hoskote et.al's implementation)\n",numtotcoveredstates);
fprintf(vis_stdout,"--%.0f states covered by Primary Input Signals\n",coveragePI);
fprintf(vis_stdout,"--%.0f states covered by Primary Ouput Signals\n",coveragePO);
fprintf(vis_stdout,"--%.0f states covered by signals which are neither Primary input nor output Signals\n",coverageOther);
fprintf(vis_stdout,"--There are %.0f reachable states\n",numrchstates);
coverage = (numtotcoveredstates / numrchstates) * 100;
fprintf(vis_stdout,"Percentage of coverage (using Hoskote et.al's implementation)= %f\n ",coverage);
avgCoverage = avgCoverage / array_n(signalList);
fprintf(vis_stdout,"Average Percentage of coverage = %f\n",avgCoverage);
if (numPI < 1)
fprintf(vis_stdout,"No Primary Input signals\n");
else {
avgPICoverage = avgPICoverage / numPI;
fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgPICoverage);
}
if (numPO < 1)
fprintf(vis_stdout,"No Primary Output signals\n");
else {
avgPOCoverage = avgPOCoverage / numPO;
fprintf(vis_stdout,"Average Percentage of coverage for Primary outputs = %f\n",avgPOCoverage);
}
if (numOther < 1)
fprintf(vis_stdout,"No signals which are neither primary inputs nor outputs\n");
else {
avgOtherCoverage = avgOtherCoverage / numOther;
fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgOtherCoverage);
}
}
else {
fprintf(vis_stdout,"Reachable states = NIL !\n");
}
}
}
if (performCoverageImproved && (modelCareStatesArray != NIL(array_t))) { /* and no errors till now */
int sigarr;
if (totalcoveredstates != NIL(mdd_t) && (modelCareStates != NIL(mdd_t))) {
numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),totalcoveredstates,Fsm_FsmReadPresentStateVars(modelFsm));
}
else {
numtotcoveredstates = 0;
}
if ((dcLevel == McDcLevelRch_c)||(dcLevel == McDcLevelRchFrontier_c)) {
if (!mdd_lequal(totalcoveredstates, modelCareStates, 1, 1)) {
(void)fprintf(vis_stdout,
"** mc warning: Some of the covered states are not reachable\n");
}
if (modelCareStates !=NIL(mdd_t)){
int sigType;
coveragePI = 0;
coveragePO = 0;
coverageOther = 0;
numPI = 0;
numPO = 0;
numOther = 0;
avgCoverage = 0;
avgPICoverage = 0;
avgPOCoverage = 0;
avgOtherCoverage = 0;
numrchstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),modelCareStates,Fsm_FsmReadPresentStateVars(modelFsm));
if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
fprintf(vis_stdout,"\nCoverage for all the Formulae w.r.t. all observable signals\n");
fprintf(vis_stdout,"=============================================================\n");
}
for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
mdd_t *statesCovered, *uncoveredStateCube, *uncoveredStates;
double numStatesCovered;
char *nrOfUncoveredStatesString;
int nrOfUncoveredStates, prntStates; /* nr of uncovered states that we output */
Ntk_Network_t *modelNetworkC = Fsm_FsmReadNetwork(modelFsm);
array_t *PSVarsC = Fsm_FsmReadPresentStateVars(modelFsm);
mdd_manager *mddMgrC = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
coverage = (numStatesCovered / numrchstates) * 100;
avgCoverage = avgCoverage + coverage;
sigType = array_fetch(int, signalTypeList,sigarr);
if (sigType == 1) {
coveragePI = coveragePI + numStatesCovered;
avgPICoverage = avgPICoverage + coverage;
numPI = numPI + 1;
}
else if (sigType == 0) {
coveragePO = coveragePO + numStatesCovered;
avgPOCoverage = avgPOCoverage + coverage;
numPO = numPO + 1;
}
else {
coverageOther = coverageOther + numStatesCovered;
avgOtherCoverage = avgOtherCoverage + coverage;
numOther = numOther + 1;
}
if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
fprintf(vis_stdout,"\n# States covered w.r.t. %s = %.0f, Percentage of Coverage = %f\n",
array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
nrOfUncoveredStatesString = Cmd_FlagReadByName("nr_uncoveredstates");
if(nrOfUncoveredStatesString == NIL(char))
nrOfUncoveredStates = 1;
else
nrOfUncoveredStates = atoi(nrOfUncoveredStatesString);
if (numStatesCovered < numrchstates) {
if ((numrchstates-numStatesCovered) < nrOfUncoveredStates)
nrOfUncoveredStates = (int)(numrchstates-numStatesCovered);
fprintf(vis_stdout,"#Printing reachable states NOT covered w.r.t. %s :\n",array_fetch(char *,signalList,sigarr));
for (prntStates = 0;prntStates<nrOfUncoveredStates;prntStates++){
fprintf(vis_stdout,"\n#State %d :\n",prntStates+1);
uncoveredStates = mdd_and(modelCareStates,statesCovered,1,0);
uncoveredStateCube = Mc_ComputeAMinterm(uncoveredStates, PSVarsC, mddMgrC);
mdd_free(uncoveredStates);
Mc_MintermPrint(uncoveredStateCube, PSVarsC, modelNetworkC);
mdd_free(uncoveredStateCube);
}
}
}
}
fprintf(vis_stdout,"\nTotal Coverage for all the Formulae\n");
fprintf(vis_stdout,"=====================================\n");
for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
mdd_t *statesCovered;
double numStatesCovered;
char *type;
int sigType;
sigType = array_fetch(int, signalTypeList,sigarr);
if (sigType == 1)
type = "Primary Input";
else if (sigType == 0)
type = "Primary Output";
else
type = "Neither Primary output nor input";
statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
coverage = (numStatesCovered / numrchstates) * 100;
fprintf(vis_stdout,"# States covered w.r.t. %s(%s) = %.0f, Percentage of Coverage = %f\n",type,
array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
}
fprintf(vis_stdout,"--There are %.0f covered states (using improved coverage implementation)\n",numtotcoveredstates);
fprintf(vis_stdout,"--%.0f states covered by Primary Input Signals\n",coveragePI);
fprintf(vis_stdout,"--%.0f states covered by Primary Ouput Signals\n",coveragePO);
fprintf(vis_stdout,"--%.0f states covered by signals which are neither Primary input nor output Signals\n",coverageOther);
fprintf(vis_stdout,"--There are %.0f reachable states\n",numrchstates);
coverage = (numtotcoveredstates / numrchstates) * 100;
fprintf(vis_stdout,"Percentage of coverage (using improved coverage implementation)= %f\n ",coverage);
avgCoverage = avgCoverage / array_n(signalList);
fprintf(vis_stdout,"Average Percentage of coverage = %f\n",avgCoverage);
if (numPI < 1)
fprintf(vis_stdout,"No Primary Input signals\n");
else {
avgPICoverage = avgPICoverage / numPI;
fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgPICoverage);
}
if (numPO < 1)
fprintf(vis_stdout,"No Primary Output signals\n");
else {
avgPOCoverage = avgPOCoverage / numPO;
fprintf(vis_stdout,"Average Percentage of coverage for Primary outputs = %f\n",avgPOCoverage);
}
if (numOther < 1)
fprintf(vis_stdout,"No signals which are not primary\n");
else {
avgOtherCoverage = avgOtherCoverage / numOther;
fprintf(vis_stdout,"Average Percentage of coverage for signals which are not primary = %f\n",avgOtherCoverage);
}
}
else {
fprintf(vis_stdout,"Reachable states = NIL !\n");
}
}
}
} /* McPrintCoverageSummary */
Here is the call graph for this function:
Here is the caller graph for this function:
| static int positionOfSignalinList | ( | char * | signal, |
| array_t * | signalList | ||
| ) | [static] |
Function********************************************************************
Synopsis [Used in the coverage code to find the index of a signal in an array of signals previously collected]
Description []
SideEffects []
SeeAlso []
Definition at line 2425 of file mcCover.c.
{
int arraysize = array_n(signalList);
int i;
for (i=0;i<arraysize;i++) {
if (strcmp(signal,array_fetch(char *,signalList,i)) == 0)
return i;
}
return -1;
} /* positionOfSignalinList */
Here is the caller graph for this function:
| static int RangeofSignalinFormula | ( | Fsm_Fsm_t * | fsm, |
| char * | signal, | ||
| Ctlp_Formula_t * | formula | ||
| ) | [static] |
Function********************************************************************
Synopsis [Finds the range of values that a given observed signal can take in a CTL formula]
Description []
SideEffects []
SeeAlso []
Definition at line 2453 of file mcCover.c.
{
Ntk_Network_t *network;
char *nodeNameString;
char *nodeValueString;
Ntk_Node_t *node;
Ctlp_Formula_t *leftFormula;
Ctlp_Formula_t *rightFormula;
Var_Variable_t *nodeVar;
int range_left,range_right;
int range = 0;
/*nodeVar = Ntk_NodeReadVariable(node);*/
if ( formula == NIL(Ctlp_Formula_t)) {
return range;
}
if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c ) {
leftFormula = Ctlp_FormulaReadLeftChild(formula);
range_left = RangeofSignalinFormula(fsm, signal, leftFormula);
#if 0
Ctlp_FormulaFree(leftFormula);
#endif
rightFormula = Ctlp_FormulaReadRightChild (formula);
range_right = RangeofSignalinFormula(fsm, signal, rightFormula);
#if 0
Ctlp_FormulaFree(rightFormula);
#endif
if (range_left==range_right) /* to avoid situation where signal exists on both sides of formula*/
range = range_left;
else
range = range_right+range_left; /* 0 + some value */
}
else {
network = Fsm_FsmReadNetwork(fsm);
nodeNameString = Ctlp_FormulaReadVariableName(formula);
nodeValueString = Ctlp_FormulaReadValueName(formula);
node = Ntk_NetworkFindNodeByName(network, nodeNameString);
nodeVar = Ntk_NodeReadVariable(node);
if ((strcmp(signal,nodeNameString)) != 0) {
range = 0;
}
else {
range = Var_VariableReadNumValues(nodeVar);
}
}
return range;
} /* RangeofSignalinFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the following for use in coverage computation for AU: traverse(So,f1,f2) = newstartstates(So) U traverse(EY(newstartstates(So)),f1,f2) (see function newstartstates for its definition ]
Description []
SideEffects []
SeeAlso [newstartstates]
Definition at line 2089 of file mcCover.c.
{
mdd_t *temp_mdd,*newSo, *Tf1_and_Tnotf2, *newStates, *oldStates, *Tf1, *Tnotf2;
Ctlp_Formula_t *tmp_formula, *existFormula;
int travcnt;
oldStates = mdd_zero(Fsm_FsmReadMddManager(fsm));
newStates = mdd_zero(Fsm_FsmReadMddManager(fsm));
newSo = mdd_dup(startstates);
existFormula = Ctlp_FormulaConvertToExistentialForm(formula1);
Tf1 = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType, verbosity, dcLevel,
buildOnionRing,GSHschedule);
Ctlp_FormulaFree(existFormula);
tmp_formula = Ctlp_FormulaConverttoComplement(formula2);
existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
Tnotf2 = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates, fairCondition,
careStatesArray, earlyTermination, hintsArray,
hintType, verbosity, dcLevel,
buildOnionRing, GSHschedule);
Ctlp_FormulaFree(existFormula);
Ctlp_FormulaFree(tmp_formula);
temp_mdd = mdd_and(Tf1,Tnotf2,1,1);
mdd_free(Tf1);
mdd_free(Tnotf2);
Tf1_and_Tnotf2 = mdd_and(temp_mdd,fairStates,1,1);
mdd_free(temp_mdd);
temp_mdd = newSo;
newSo = mdd_and(temp_mdd,Tf1_and_Tnotf2,1,1);
mdd_free(temp_mdd);
temp_mdd = newStates;
newStates = mdd_or(temp_mdd,newSo,1,1);
mdd_free(temp_mdd);
travcnt = 0;
while (!(mdd_equal_mod_care_set_array(newStates,oldStates,careStatesArray))) {
mdd_t *tmp_mdd = oldStates;
oldStates = mdd_or(tmp_mdd,newStates,1,1);
mdd_free(tmp_mdd);
tmp_mdd = newSo;
newSo = Mc_FsmEvaluateEYFormula(fsm, tmp_mdd, fairStates, careStatesArray, verbosity, dcLevel);
mdd_free(tmp_mdd);
tmp_mdd = newSo;
newSo = mdd_and(tmp_mdd,Tf1_and_Tnotf2,1,1);
mdd_free(tmp_mdd);
tmp_mdd = newStates;
newStates = mdd_or(tmp_mdd,newSo,1,1);
mdd_free(tmp_mdd);
}
mdd_free(oldStates);
mdd_free(newSo);
mdd_free(Tf1_and_Tnotf2);
return newStates;
} /* traverse */
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: mcCover.c,v 1.4 2005/05/15 07:32:10 fabio Exp $" [static] |
CFile***********************************************************************
FileName [mcCover.c]
PackageName [mc]
Synopsis [Functions for coverage estimation.]
Description [This file contains the functions implementing coverage estimation for CTL. According to the proposal of Hoskote et al. (DAC99) a state is covered by a passing property with respect to an observable binary signal if flipping the value of the signal at that state causes the property to fail. Hoskote et al. proposed an algorithm for the estimation of coverage for a subset of ACTL loosely based on this definition of coverage.
This file contains an implementation of Hoskote's algorithm as well as an implementation of the improved algorithm by Jayakumar et al. presented at DAC2003. The improved algorithm deals with a larger subset of CTL and provides more accurate estimates.]
SeeAlso [mcMc.c]
Author [Nikhil Jayakumar]
Copyright [Copyright (c) 2002-2005, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
