#include "ctlpInt.h"#include "mcInt.h"#include "fsm.h"#include "bmc.h"
Include dependency graph for mcMc.c:
Go to the source code of this file.
Functions | |
| static mdd_t * | EvaluateFormulaRecur (Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Ctlp_Approx_t TRMinimization, Ctlp_Approx_t *resultApproxType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule) |
| static mdd_t * | McForwardReachable (Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *invariantMdd, mdd_t *fairStates, array_t *careStatesArray, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| mdd_t * | Mc_FsmCheckLanguageEmptiness (Fsm_Fsm_t *modelFsm, array_t *modelCareStatesArray, Mc_AutStrength_t automatonStrength, Mc_LeMethod_t leMethod, int dcLevel, int dbgLevel, int printInputs, int verbosity, Mc_GSHScheduleType GSHschedule, Mc_FwdBwdAnalysis GSHdirection, int lockstep, FILE *dbgFile, int UseMore, int SimValue, char *driverName) |
| mdd_t * | Mc_FsmEvaluateFormula (Fsm_Fsm_t *fsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRing, Mc_GSHScheduleType GSHschedule) |
| mdd_t * | Mc_FsmEvaluateEXFormula (Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| mdd_t * | Mc_FsmEvaluateMXFormula (Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| bdd_t * | Mc_QuantifyInputFAFW (Fsm_Fsm_t *fsm, bdd_t *result) |
| mdd_t * | Mc_FsmEvaluateEYFormula (Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| mdd_t * | Mc_FsmEvaluateEUFormula (Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *target, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) |
| mdd_t * | Mc_FsmEvaluateESFormula (Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *source, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) |
| mdd_t * | Mc_FsmEvaluateAUFormula (Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *target, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) |
| mdd_t * | Mc_FsmEvaluateEGFormula (Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, Mc_GSHScheduleType GSHschedule) |
| mdd_t * | Mc_FsmEvaluateEHFormula (Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, Mc_GSHScheduleType GSHschedule) |
| mdd_t * | Mc_FsmEvaluateFwdUFormula (Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *invariantMdd, mdd_t *fairStates, array_t *careStatesArray, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| mdd_t * | Mc_FsmEvaluateFwdGFormula (Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *invariantMdd, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| mdd_t * | Mc_FsmEvaluateFwdEHFormula (Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| mdd_t * | McEvaluateEUFormulaWithGivenTR (Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) |
| mdd_t * | McEvaluateESFormulaWithGivenTR (Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) |
| mdd_t * | McEvaluateESFormulaWithGivenTRWithTarget (Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) |
| mdd_t * | McEvaluateESFormulaWithGivenTRFAFW (Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, mdd_t *Swin) |
| mdd_t * | McEvaluateAUFormulaWithGivenTR (Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) |
| mdd_t * | McEvaluateEGFormulaWithGivenTR (Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) |
| mdd_t * | McEvaluateEHFormulaWithGivenTR (Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) |
| void | McFormulaFreeDebugData (Ctlp_Formula_t *formula) |
| void | _McPrintSatisfyingMinterms (mdd_t *aMdd, Fsm_Fsm_t *fsm) |
| boolean | McPrintPassFail (mdd_manager *mddMgr, Fsm_Fsm_t *modelFsm, Mc_FwdBwdAnalysis traversalDirection, Ctlp_Formula_t *ctlFormula, mdd_t *ctlFormulaStates, mdd_t *modelInitialStates, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity) |
| mdd_t * | McModelCheckAtomicFormula (Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula) |
| void | InvarPrintDebugInformation (Fsm_Fsm_t *modelFsm, array_t *invarFormulaArray, array_t *invarStatesArray, int *resultArray, McOptions_t *options, array_t *hintsStatesArray) |
| array_t * | SortFormulasByFsm (Fsm_Fsm_t *totalFsm, array_t *invarFormulaArray, array_t *fsmArray, McOptions_t *options) |
| int | TestInvariantsInTotalFsm (Fsm_Fsm_t *totalFsm, array_t *invarStatesArray, int shellFlag) |
| Ctlp_Approx_t | ComputeResultingApproximation (Ctlp_FormulaType formulaType, Ctlp_Approx_t leftApproxType, Ctlp_Approx_t rightApproxType, Ctlp_Approx_t TRMinimization, Mc_EarlyTermination_t *earlyTermination, boolean fixpoint) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mcMc.c,v 1.257 2007/04/17 00:01:22 sohail Exp $" |
Function Documentation
| void _McPrintSatisfyingMinterms | ( | mdd_t * | aMdd, |
| Fsm_Fsm_t * | fsm | ||
| ) |
Function********************************************************************
Synopsis [Print satisfying minterms.]
Description [Print satisfying minterms. Just made for debug.]
SideEffects []
Definition at line 2952 of file mcMc.c.
{
array_t *support = Fsm_FsmReadPresentStateVars(fsm);
mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm);
int i, n;
array_t *mintermArray;
mdd_t *aMinterm;
n = (int) mdd_count_onset(mddMgr, aMdd, support);
mintermArray = mdd_pick_arbitrary_minterms(mddMgr, aMdd, support, n);
for (i = 0; i < n; i++) {
aMinterm = array_fetch(mdd_t *, mintermArray, i);
Mc_MintermPrint(aMinterm, support, network);
mdd_free(aMinterm);
}
array_free(mintermArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Ctlp_Approx_t ComputeResultingApproximation | ( | Ctlp_FormulaType | formulaType, |
| Ctlp_Approx_t | leftApproxType, | ||
| Ctlp_Approx_t | rightApproxType, | ||
| Ctlp_Approx_t | TRMinimization, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| boolean | fixpoint | ||
| ) |
Function********************************************************************
Synopsis [Compute the approximation of the result for EvaluateFormulaRecur.]
Description []
SideEffects [None]
SeeAlso [EvaluateFormulaRecur]
Definition at line 3478 of file mcMc.c.
{
Ctlp_Approx_t thisApproxType;
switch (formulaType) {
case Ctlp_ID_c:
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
thisApproxType = Ctlp_Exact_c;
break;
case Ctlp_NOT_c:
if (leftApproxType == Ctlp_Incomparable_c) {
thisApproxType = Ctlp_Incomparable_c;
} else if (leftApproxType == Ctlp_Overapprox_c) {
thisApproxType = Ctlp_Underapprox_c;
} else if (leftApproxType == Ctlp_Underapprox_c) {
thisApproxType = Ctlp_Overapprox_c;
} else {
thisApproxType = Ctlp_Exact_c;
}
break;
case Ctlp_AND_c:
if (leftApproxType == Ctlp_Incomparable_c ||
rightApproxType == Ctlp_Incomparable_c ||
(leftApproxType == Ctlp_Overapprox_c &&
rightApproxType == Ctlp_Underapprox_c) ||
(leftApproxType == Ctlp_Underapprox_c &&
rightApproxType == Ctlp_Overapprox_c)) {
thisApproxType = Ctlp_Incomparable_c;
} else if (rightApproxType == Ctlp_Overapprox_c) {
if (earlyTermination == MC_NO_EARLY_TERMINATION &&
leftApproxType == Ctlp_Exact_c) {
thisApproxType = Ctlp_Exact_c;
} else {
thisApproxType = Ctlp_Overapprox_c;
}
} else if (leftApproxType == Ctlp_Overapprox_c) {
thisApproxType = Ctlp_Overapprox_c;
} else if (rightApproxType == Ctlp_Underapprox_c) {
if (earlyTermination == MC_NO_EARLY_TERMINATION &&
leftApproxType == Ctlp_Exact_c) {
thisApproxType = Ctlp_Exact_c;
} else {
thisApproxType = Ctlp_Underapprox_c;
}
} else if (leftApproxType == Ctlp_Underapprox_c) {
thisApproxType = Ctlp_Underapprox_c;
} else {
thisApproxType = Ctlp_Exact_c;
}
break;
case Ctlp_EQ_c:
case Ctlp_XOR_c:
if (leftApproxType != Ctlp_Exact_c || rightApproxType != Ctlp_Exact_c) {
thisApproxType = Ctlp_Incomparable_c;
} else {
thisApproxType = Ctlp_Exact_c;
}
break;
case Ctlp_THEN_c:
if (leftApproxType == Ctlp_Incomparable_c ||
rightApproxType == Ctlp_Incomparable_c ||
(leftApproxType == Ctlp_Overapprox_c &&
rightApproxType == Ctlp_Overapprox_c) ||
(leftApproxType == Ctlp_Underapprox_c &&
rightApproxType == Ctlp_Underapprox_c)) {
thisApproxType = Ctlp_Incomparable_c;
} else if (rightApproxType == Ctlp_Overapprox_c) {
if (earlyTermination == MC_NO_EARLY_TERMINATION &&
leftApproxType == Ctlp_Exact_c) {
thisApproxType = Ctlp_Exact_c;
} else {
thisApproxType = Ctlp_Overapprox_c;
}
} else if (leftApproxType == Ctlp_Underapprox_c) {
thisApproxType = Ctlp_Overapprox_c;
} else if (rightApproxType == Ctlp_Underapprox_c) {
if (earlyTermination == MC_NO_EARLY_TERMINATION &&
leftApproxType == Ctlp_Exact_c) {
thisApproxType = Ctlp_Exact_c;
} else {
thisApproxType = Ctlp_Underapprox_c;
}
} else if (leftApproxType == Ctlp_Overapprox_c) {
thisApproxType = Ctlp_Underapprox_c;
} else {
thisApproxType = Ctlp_Exact_c;
}
break;
case Ctlp_OR_c:
if (leftApproxType == Ctlp_Incomparable_c ||
rightApproxType == Ctlp_Incomparable_c ||
(leftApproxType == Ctlp_Overapprox_c &&
rightApproxType == Ctlp_Underapprox_c) ||
(leftApproxType == Ctlp_Underapprox_c &&
rightApproxType == Ctlp_Overapprox_c)) {
thisApproxType = Ctlp_Incomparable_c;
} else if (rightApproxType == Ctlp_Overapprox_c) {
if (earlyTermination == MC_NO_EARLY_TERMINATION &&
leftApproxType == Ctlp_Exact_c) {
thisApproxType = Ctlp_Exact_c;
} else {
thisApproxType = Ctlp_Overapprox_c;
}
} else if (leftApproxType == Ctlp_Overapprox_c) {
thisApproxType = Ctlp_Overapprox_c;
} else if (rightApproxType == Ctlp_Underapprox_c) {
if (earlyTermination == MC_NO_EARLY_TERMINATION &&
leftApproxType == Ctlp_Exact_c) {
thisApproxType = Ctlp_Exact_c;
} else {
thisApproxType = Ctlp_Underapprox_c;
}
} else if (leftApproxType == Ctlp_Underapprox_c) {
thisApproxType = Ctlp_Underapprox_c;
} else {
thisApproxType = Ctlp_Exact_c;
}
break;
case Ctlp_EX_c:
if (leftApproxType == Ctlp_Underapprox_c) {
if (TRMinimization == Ctlp_Overapprox_c) {
thisApproxType = Ctlp_Incomparable_c;
} else {
thisApproxType = Ctlp_Underapprox_c;
}
} else if (leftApproxType == Ctlp_Overapprox_c) {
if (TRMinimization == Ctlp_Underapprox_c) {
thisApproxType = Ctlp_Incomparable_c;
} else {
thisApproxType = Ctlp_Overapprox_c;
}
} else if (leftApproxType == Ctlp_Exact_c) {
thisApproxType = TRMinimization;
} else {
thisApproxType = Ctlp_Incomparable_c;
}
break;
case Ctlp_EU_c:
if (leftApproxType == Ctlp_Incomparable_c ||
rightApproxType == Ctlp_Incomparable_c ||
(leftApproxType == Ctlp_Overapprox_c &&
rightApproxType == Ctlp_Underapprox_c) ||
(leftApproxType == Ctlp_Underapprox_c &&
rightApproxType == Ctlp_Overapprox_c)) {
thisApproxType = Ctlp_Incomparable_c;
} else if (leftApproxType == Ctlp_Overapprox_c ||
rightApproxType == Ctlp_Overapprox_c) {
thisApproxType = Ctlp_Overapprox_c;
} else if (leftApproxType == Ctlp_Underapprox_c ||
rightApproxType == Ctlp_Underapprox_c) {
thisApproxType = Ctlp_Underapprox_c;
} else {
thisApproxType = Ctlp_Exact_c;
}
if (!fixpoint) {
if (TRMinimization == Ctlp_Overapprox_c ||
thisApproxType == Ctlp_Overapprox_c) {
thisApproxType = Ctlp_Incomparable_c;
} else if (thisApproxType == Ctlp_Exact_c) {
thisApproxType = Ctlp_Underapprox_c;
}
} else {
if ((TRMinimization == Ctlp_Overapprox_c &&
thisApproxType == Ctlp_Underapprox_c) ||
(TRMinimization == Ctlp_Underapprox_c &&
thisApproxType == Ctlp_Overapprox_c)) {
thisApproxType = Ctlp_Incomparable_c;
} else if (thisApproxType == Ctlp_Exact_c) {
thisApproxType = TRMinimization;
}
}
break;
case Ctlp_EG_c:
if (leftApproxType == Ctlp_Incomparable_c ||
rightApproxType == Ctlp_Incomparable_c ||
(leftApproxType == Ctlp_Overapprox_c &&
rightApproxType == Ctlp_Underapprox_c) ||
(leftApproxType == Ctlp_Underapprox_c &&
rightApproxType == Ctlp_Overapprox_c)) {
thisApproxType = Ctlp_Incomparable_c;
} else if (leftApproxType == Ctlp_Overapprox_c ||
rightApproxType == Ctlp_Overapprox_c) {
thisApproxType = Ctlp_Overapprox_c;
} else if (leftApproxType == Ctlp_Underapprox_c ||
rightApproxType == Ctlp_Underapprox_c) {
thisApproxType = Ctlp_Underapprox_c;
} else {
thisApproxType = Ctlp_Exact_c;
}
if (!fixpoint) {
if (TRMinimization == Ctlp_Underapprox_c ||
thisApproxType == Ctlp_Underapprox_c) {
thisApproxType = Ctlp_Incomparable_c;
} else if (thisApproxType == Ctlp_Exact_c) {
thisApproxType = Ctlp_Overapprox_c;
}
} else {
if ((TRMinimization == Ctlp_Overapprox_c &&
thisApproxType == Ctlp_Underapprox_c) ||
(TRMinimization == Ctlp_Underapprox_c &&
thisApproxType == Ctlp_Overapprox_c)) {
thisApproxType = Ctlp_Incomparable_c;
} else if (thisApproxType == Ctlp_Exact_c) {
thisApproxType = TRMinimization;
}
}
break;
case Ctlp_Cmp_c:
case Ctlp_Init_c:
case Ctlp_FwdU_c:
case Ctlp_FwdG_c:
case Ctlp_EY_c:
/* no early termination and no hints in forward model checking */
thisApproxType = Ctlp_Exact_c;
break;
default: fail("Encountered unknown type of CTL formula\n");
}
return thisApproxType;
} /* ComputeResultingApproximation */
Here is the caller graph for this function:
| static mdd_t * EvaluateFormulaRecur | ( | Fsm_Fsm_t * | modelFsm, |
| Ctlp_Formula_t * | ctlFormula, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | fairCondition, | ||
| array_t * | modelCareStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| Fsm_HintsArray_t * | hintsArray, | ||
| Mc_GuidedSearch_t | hintType, | ||
| Ctlp_Approx_t | TRMinimization, | ||
| Ctlp_Approx_t * | resultApproxType, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| int | buildOnionRings, | ||
| Mc_GSHScheduleType | GSHschedule | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Model check formula on given fsm under fairness]
Description [This is the recursive part of Mc_FsmEvaluateFormula]
Comment [See Mc_EvaluateFormula. The only difference is that EvaluateFormula takes care of global hints, and passes on an extra flag, TRMinimization that indicates how the current TR related to the exact TR. Using this flag, the procedure decides in which field of the formula to store results (states, underapproxStates or overapproxStates) ]
SideEffects []
Definition at line 3730 of file mcMc.c.
{
mdd_t *leftMdd = NIL(mdd_t);
mdd_t *rightMdd = NIL(mdd_t);
mdd_t *result = NIL(mdd_t);
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
array_t *careStatesArray = NIL(array_t);
mdd_t *tmpMdd;
mdd_t *approx = NIL(mdd_t); /* prev computed approx of sat set */
mdd_t *ctlFormulaStates = Ctlp_FormulaObtainStates( ctlFormula );
Ctlp_Approx_t leftApproxType = Ctlp_Exact_c;
Ctlp_Approx_t rightApproxType = Ctlp_Exact_c;
Ctlp_Approx_t thisApproxType = Ctlp_Exact_c;
boolean fixpoint = FALSE;
boolean skipRight = FALSE;
if ( ctlFormulaStates ) {
return ctlFormulaStates;
}
{
Ctlp_Formula_t *leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
if (leftChild) {
Mc_EarlyTermination_t *nextEarlyTermination =
McObtainUpdatedEarlyTerminationCondition(
earlyTermination, NIL(mdd_t), Ctlp_FormulaReadType(ctlFormula));
leftMdd = EvaluateFormulaRecur(modelFsm, leftChild, fairStates,
fairCondition, modelCareStatesArray,
nextEarlyTermination,
hintsArray, hintType, TRMinimization,
&leftApproxType, verbosity, dcLevel,
buildOnionRings, GSHschedule);
Mc_EarlyTerminationFree(nextEarlyTermination);
if (!leftMdd) {
return NIL(mdd_t);
}
}
}
{/* read right */
Ctlp_Formula_t *rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
if (rightChild) {
Mc_EarlyTermination_t *nextEarlyTermination =
McObtainUpdatedEarlyTerminationCondition(
earlyTermination, leftMdd, Ctlp_FormulaReadType(ctlFormula));
skipRight = Mc_EarlyTerminationIsSkip(nextEarlyTermination);
if (!skipRight) {
rightMdd = EvaluateFormulaRecur(modelFsm, rightChild, fairStates,
fairCondition, modelCareStatesArray,
nextEarlyTermination,
hintsArray, hintType, TRMinimization,
&rightApproxType, verbosity, dcLevel,
buildOnionRings, GSHschedule);
}
Mc_EarlyTerminationFree(nextEarlyTermination);
if (!(rightMdd || skipRight)) {
if (leftMdd)
mdd_free(leftMdd);
return NIL(mdd_t);
}
}
}/* read right */
if (modelCareStatesArray != NIL(array_t)) {
careStatesArray = modelCareStatesArray;
} else {
careStatesArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, careStatesArray, mdd_one(mddMgr));
}
switch (Ctlp_FormulaReadType(ctlFormula)) {
case Ctlp_ID_c:
assert(!skipRight);
result = McModelCheckAtomicFormula(modelFsm, ctlFormula);
break;
case Ctlp_TRUE_c:
assert(!skipRight);
result = mdd_one(mddMgr); break;
case Ctlp_FALSE_c:
assert(!skipRight);
result = mdd_zero(mddMgr); break;
case Ctlp_NOT_c:
assert(!skipRight);
result = mdd_not(leftMdd); break;
case Ctlp_AND_c:
if (skipRight) {
result = mdd_dup(leftMdd);
rightApproxType = Ctlp_Overapprox_c;
} else {
result = mdd_and(leftMdd, rightMdd, 1, 1);
}
break;
case Ctlp_EQ_c:
assert(!skipRight);
result = mdd_xnor(leftMdd, rightMdd); break;
case Ctlp_XOR_c:
assert(!skipRight);
result = mdd_xor(leftMdd, rightMdd); break;
case Ctlp_THEN_c:
if (skipRight) {
result = mdd_dup(leftMdd);
rightApproxType = Ctlp_Underapprox_c;
} else {
result = mdd_or(leftMdd, rightMdd, 0, 1);
}
break;
case Ctlp_OR_c:
if (skipRight) {
result = mdd_dup(leftMdd);
rightApproxType = Ctlp_Underapprox_c;
} else {
result = mdd_or(leftMdd, rightMdd, 1, 1);
}
break;
case Ctlp_EX_c:
assert(!skipRight);
result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
careStatesArray, verbosity, dcLevel);
break;
case Ctlp_EU_c: {
array_t *onionRings = NIL(array_t); /* array of mdd_t */
boolean newrings;
assert(!skipRight);
/* An underapproximation, together with its explanation may be stored. */
approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Underapprox_c );
onionRings = (array_t *) Ctlp_FormulaReadDebugData(ctlFormula);
newrings = onionRings == NIL(array_t);
if (buildOnionRings){
assert((approx != NIL(mdd_t) && onionRings != NIL(array_t)) ||
(approx == NIL(mdd_t) && onionRings == NIL(array_t)));
if(onionRings == NIL(array_t))
onionRings = array_alloc(mdd_t *, 0);
}
result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, rightMdd,
approx, fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
if(buildOnionRings && newrings)
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings,
McFormulaFreeDebugData);
if(approx != NIL(mdd_t))
mdd_free(approx);
break;
}
case Ctlp_EG_c: {
array_t *arrayOfOnionRings = NIL(array_t); /* array of array of mdd_t* */
assert(!skipRight);
if(buildOnionRings)
arrayOfOnionRings = array_alloc(array_t *, 0);
approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Overapprox_c );
result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, approx, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
&arrayOfOnionRings, verbosity,
dcLevel, &fixpoint, GSHschedule);
if(buildOnionRings)
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
McFormulaFreeDebugData);
if(approx != NIL(mdd_t)) mdd_free(approx);
break;
}
case Ctlp_Cmp_c: {
assert(!skipRight);
if (Ctlp_FormulaReadCompareValue(ctlFormula) == 0)
result = bdd_is_tautology(leftMdd, 0) ?
mdd_one(mddMgr) : mdd_zero(mddMgr);
else
result = bdd_is_tautology(leftMdd, 0) ?
mdd_zero(mddMgr) : mdd_one(mddMgr);
break;
}
case Ctlp_Init_c:
assert(!skipRight);
result = Fsm_FsmComputeInitialStates(modelFsm);
break;
case Ctlp_FwdU_c:
assert(!skipRight);
if (buildOnionRings) {
array_t *onionRings = array_alloc(mdd_t *, 0);
result = Mc_FsmEvaluateFwdUFormula(modelFsm, leftMdd, rightMdd,
fairStates, careStatesArray,
onionRings, verbosity, dcLevel);
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings,
McFormulaFreeDebugData);
}
else {
if (Ctlp_FormulaReadLeftChild(ctlFormula) &&
Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(ctlFormula)) ==
Ctlp_Init_c &&
Ctlp_FormulaReadRightChild(ctlFormula) &&
Ctlp_FormulaReadType(Ctlp_FormulaReadRightChild(ctlFormula)) ==
Ctlp_TRUE_c &&
Fsm_FsmTestIsReachabilityDone(modelFsm)) {
result = mdd_dup(Fsm_FsmReadReachableStates(modelFsm));
break;
}
result = Mc_FsmEvaluateFwdUFormula(modelFsm, leftMdd, rightMdd,
fairStates, careStatesArray,
NIL(array_t), verbosity,
dcLevel);
}
break;
case Ctlp_FwdG_c:
assert(!skipRight);
if (buildOnionRings) {
array_t *arrayOfOnionRings = array_alloc(array_t *, 0);
result = Mc_FsmEvaluateFwdGFormula(modelFsm, leftMdd, rightMdd,
fairStates, fairCondition,
careStatesArray,
arrayOfOnionRings, verbosity,
dcLevel);
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
McFormulaFreeDebugData);
} else {
result = Mc_FsmEvaluateFwdGFormula(modelFsm, leftMdd, rightMdd,
fairStates, fairCondition,
careStatesArray,
NIL(array_t), verbosity,
dcLevel);
}
break;
case Ctlp_EY_c:
assert(!skipRight);
result = Mc_FsmEvaluateEYFormula(modelFsm, leftMdd, fairStates,
careStatesArray, verbosity, dcLevel);
break;
default: fail("Encountered unknown type of CTL formula\n");
}
tmpMdd = mdd_dup(result);
thisApproxType = ComputeResultingApproximation(
Ctlp_FormulaReadType(ctlFormula), leftApproxType,
rightApproxType, TRMinimization, earlyTermination, fixpoint);
Ctlp_FormulaSetApproxStates(ctlFormula, tmpMdd, thisApproxType);
#ifdef DEBUG_MC
/* The following code is just for debugging */
if ((verbosity == McVerbosityMax_c)) {
char *type = Ctlp_FormulaGetTypeString(ctlFormula);
if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_Cmp_c) {
fprintf(vis_stdout, "Info : result for [Cmp]\n");
if (bdd_is_tautology(result, 1))
fprintf(vis_stdout, "TRUE\n");
else
fprintf(vis_stdout, "FALSE\n");
}
else if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_ID_c) {
char *atomic = Ctlp_FormulaConvertToString(ctlFormula);
fprintf(vis_stdout, "Info : satisfying minterms for [%s(%s)]:\n",
type, atomic);
free(atomic);
if (bdd_is_tautology(result, 1))
fprintf(vis_stdout, "-- TAUTOLOGY --\n");
else if (bdd_is_tautology(result, 0))
fprintf(vis_stdout, "-- null --\n");
else
(void)_McPrintSatisfyingMinterms(result, modelFsm);
}
else {
fprintf(vis_stdout, "Info : satisfying minterms for [%s]:\n", type);
if (bdd_is_tautology(result, 1))
fprintf(vis_stdout, "-- TAUTOLOGY --\n");
else if (bdd_is_tautology(result, 0))
fprintf(vis_stdout, "-- null --\n");
else
(void)_McPrintSatisfyingMinterms(result, modelFsm);
}
free(type);
}
#endif
if (modelCareStatesArray == NIL(array_t))
mdd_array_free(careStatesArray);
if (leftMdd)
mdd_free(leftMdd);
if (rightMdd)
mdd_free(rightMdd);
*resultApproxType = thisApproxType;
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void InvarPrintDebugInformation | ( | Fsm_Fsm_t * | modelFsm, |
| array_t * | invarFormulaArray, | ||
| array_t * | invarStatesArray, | ||
| int * | resultArray, | ||
| McOptions_t * | options, | ||
| array_t * | hintsStatesArray | ||
| ) |
Function********************************************************************
Synopsis [Prints out a path from the initial state to a state that violates the invariant. ]
Description [Prints out a path from the initial state to a state that violates the invariant. First it checks whether there any onion rings built for this fsm. If the onion rings already exist, it checks whether there is any violation in these rings. If not, additional onion rings are computed.]
SideEffects []
Definition at line 3156 of file mcMc.c.
{
FILE *debugFile = McOptionsReadDebugFile(options);
FILE *tmpFile = vis_stdout;
extern FILE *vis_stdpipe;
mdd_t *outerOnionRing=NIL(mdd_t);
mdd_t *reachableBadStates;
mdd_t *aBadReachableState, *reachableStates;
array_t *aPath;
boolean computeReach = TRUE;
int ringsUpToDate;
array_t *onionRings=NIL(array_t);
int i, j;
Fsm_RchType_t approxFlag;
Ctlp_Formula_t *invarFormula;
mdd_t *invarFormulaStates;
approxFlag = McOptionsReadInvarApproxFlag(options);
if (debugFile)
vis_stdpipe = debugFile;
else if (McOptionsReadUseMore(options) == TRUE)
vis_stdpipe = popen("more", "w");
else
vis_stdpipe = vis_stdout;
vis_stdout = vis_stdpipe;
arrayForEachItem(mdd_t *, invarStatesArray, i, invarFormulaStates) {
if ((invarFormulaStates == NIL(mdd_t)) || (resultArray[i] == 1))
continue;
onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm);
ringsUpToDate = Fsm_FsmTestReachabilityOnionRingsUpToDate(modelFsm);
/* search for onion ring intersecting invarStates' */
if (onionRings != NIL(array_t)) {
for (j = 0; j < array_n(onionRings); j++) {
outerOnionRing = array_fetch(mdd_t *, onionRings, j);
if (!mdd_lequal(outerOnionRing, invarFormulaStates, 1, 1)) {
computeReach = FALSE;
break;
}
}
}
/* no onion ring found, hence recompute with onion rings */
if (computeReach == TRUE) {
Mc_VerbosityLevel verbosity;
int debugFlag;
int ardc;
int dcLevel = McOptionsReadDcLevel(options);
verbosity = McOptionsReadVerbosityLevel(options);
debugFlag = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c);
if (dcLevel == McDcLevelArdc_c)
ardc = 1;
else
ardc = 0;
assert(!ringsUpToDate);
reachableStates = Fsm_FsmComputeReachableStates(
modelFsm, 0, (int)verbosity , 0, 0, debugFlag, 0, 0, approxFlag, ardc,
0, invarStatesArray, (verbosity > 1), hintsStatesArray);
mdd_free(reachableStates);
/* find the onion ring with invariant failure */
onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm);
if (onionRings == NIL(array_t)) {
fprintf(vis_stdout, "Unable to generate onion rings for counterexample.\n");
fprintf(vis_stdout, "Try again with standard (without -A) options.\n");
if (vis_stdout != tmpFile && vis_stdout != debugFile)
(void)pclose(vis_stdpipe);
vis_stdout = tmpFile;
return;
}
ringsUpToDate = Fsm_FsmTestReachabilityOnionRingsUpToDate(modelFsm);
for (j = 0; j < array_n(onionRings); j++) {
outerOnionRing = array_fetch(mdd_t *, onionRings, j);
if (!mdd_lequal(outerOnionRing, invarFormulaStates, 1, 1)) {
break;
}
}
}
invarFormula = array_fetch(Ctlp_Formula_t *, invarFormulaArray, i);
/* this is the case of true negative */
if (outerOnionRing != NIL(mdd_t)) {
/* compute the set of bad states */
if(Fsm_FsmReadFAFWFlag(modelFsm) > 1 && McOptionsReadInvarApproxFlag(options) == Fsm_Rch_Bfs_c)
reachableBadStates = mdd_not(invarFormulaStates);
else
reachableBadStates = mdd_and(invarFormulaStates, outerOnionRing, 0, 1);
/* pick one bad state */
aBadReachableState = Mc_ComputeAState(reachableBadStates, modelFsm);
mdd_free(reachableBadStates);
/* build a path from the initial states to the bad state */
aPath = Mc_BuildPathFromCore(aBadReachableState, onionRings,
modelFsm, McGreaterOrEqualZero_c);
mdd_free(aBadReachableState);
if(McOptionsReadDbgLevel(options)==2)
{
(void) Mc_PrintPathAiger(aPath, modelFsm, McOptionsReadPrintInputs(options));
}
else
{
(void) fprintf(vis_stdout, "# INV: formula %d failed --- ", i+1);
Ctlp_FormulaPrint(vis_stdout,
Ctlp_FormulaReadOriginalFormula(invarFormula));
fprintf(vis_stdout, "\n");
(void) fprintf(vis_stdout, "# INV: calling debugger\n");
if (array_n(aPath) > 1) {
(void) fprintf(vis_stdout,
"# INV: a sequence of states starting at an initial ");
(void) fprintf(vis_stdout, "state leading to a bad state\n");
} else {
(void) fprintf(vis_stdout,
"# INV: invariant fails at the following initial state\n");
}
(void) Mc_PrintPath(aPath, modelFsm, McOptionsReadPrintInputs(options));
}
(void) fprintf(vis_stdout, "\n");
McNormalizeBddPointer(aPath);
mdd_array_free(aPath);
} else {
/* Was a false negative */
assert (approxFlag == Fsm_Rch_Oa_c);
(void) fprintf(vis_stdout, "# INV: formula passed --- ");
Ctlp_FormulaPrint(vis_stdout,
Ctlp_FormulaReadOriginalFormula(invarFormula));
fprintf(vis_stdout, "\n");
}
}
if (vis_stdout != tmpFile && vis_stdout != debugFile)
(void)pclose(vis_stdpipe);
vis_stdout = tmpFile;
} /* end of InvarPrintDebugInformation */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmCheckLanguageEmptiness | ( | Fsm_Fsm_t * | modelFsm, |
| array_t * | modelCareStatesArray, | ||
| Mc_AutStrength_t | automatonStrength, | ||
| Mc_LeMethod_t | leMethod, | ||
| int | dcLevel, | ||
| int | dbgLevel, | ||
| int | printInputs, | ||
| int | verbosity, | ||
| Mc_GSHScheduleType | GSHschedule, | ||
| Mc_FwdBwdAnalysis | GSHdirection, | ||
| int | lockstep, | ||
| FILE * | dbgFile, | ||
| int | UseMore, | ||
| int | SimValue, | ||
| char * | driverName | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Compute all the states that lead to a fair cycle]
Comment [Used by LE/LTL/CTL* model checking. Different dicision procedures are applied according to the "strength of the buechi automaton": For the strong automaton, we need to compute EG(true) under the fairness constraints; If the automaton is weak, we will check !EFEG(fair); If the automaton is terminal, we only need to check !EF(fair). This is based on the CAV'99 paper of Bloem, Ravi & Somenzi: "Efficient Decision Procedures for Model Checking of Linear Time Logic Properties".
Debugging information will be print out if dbgLevel is non-zero.
Return the set of initial states from where fair paths exist.]
SideEffects [The caller should free the returned mdd_t.]
Definition at line 88 of file mcMc.c.
{
mdd_t *result;
mdd_t *mddOne;
mdd_t *badStates;
mdd_t *aBadState;
mdd_t *initialStates;
mdd_t *fairStates;
mdd_manager *mddMgr;
Ctlp_Formula_t *ctlFair, *ctlFormula;
Mc_EarlyTermination_t *earlyTermination;
array_t *arrayOfOnionRings;
array_t *stemArray;
array_t *cycleArray;
McPath_t *fairPath;
McPath_t *normalPath;
FILE *tmpFile = vis_stdout;
extern FILE *vis_stdpipe;
int i;
if (leMethod == Mc_Le_Dnc_c && automatonStrength == 2) {
return Mc_FsmCheckLanguageEmptinessByDnC(modelFsm,
modelCareStatesArray,
Mc_Aut_Strong_c,
dcLevel,
dbgLevel,
printInputs,
verbosity,
GSHschedule,
GSHdirection,
lockstep,
dbgFile,
UseMore,
SimValue,
driverName);
}
/**************************************************************************
* CASE1 & CASE2: TERMINAL/WEAK AUTOMATON
* problem is reduced to checking !EF (fair) for TERMINAL
* or !EF EG (fair) for WEAK
**************************************************************************/
if (automatonStrength == 0 || automatonStrength == 1) {
Fsm_Fairness_t *modelFairness;
modelFairness = Fsm_FsmReadFairnessConstraint(modelFsm);
assert(Fsm_FairnessTestIsBuchi(modelFairness));
ctlFair = Ctlp_FormulaCreate(Ctlp_ID_c,
(void *)util_strsav("fair1$AUT$NTK2"),
(void *)util_strsav("1"));
/* Dup(Fsm_FairnessReadFinallyInfFormula(modelFairness, 0, 0)); */
if (automatonStrength == 0) {
Ctlp_Formula_t *ctlTRUE;
ctlTRUE = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t),
NIL(Ctlp_Formula_t));
ctlFormula = Ctlp_FormulaCreate(Ctlp_EU_c, ctlTRUE, ctlFair);
if (dbgLevel || verbosity)
fprintf(vis_stdout, "# %s: Terminal automaton -- check EF(states satisfy fairness)\n",
driverName);
}else {
Ctlp_Formula_t *ctlTRUE, *ctlEGfair;
ctlTRUE = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t));
ctlEGfair = Ctlp_FormulaCreate(Ctlp_EG_c, ctlFair, NIL(Ctlp_Formula_t));
ctlFormula = Ctlp_FormulaCreate(Ctlp_EU_c, ctlTRUE, ctlEGfair);
if (dbgLevel || verbosity)
fprintf(vis_stdout, "# %s: Weak automaton -- check EF EG (states satisfy fairness)\n",
driverName);
}
/* Evaluate ctlFormula */
mddMgr = Fsm_FsmReadMddManager(modelFsm);
mddOne = mdd_one(mddMgr);
initialStates = Fsm_FsmComputeInitialStates(modelFsm);
earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
fairStates =
Mc_FsmEvaluateFormula(modelFsm, ctlFormula, mddOne, modelFairness,
modelCareStatesArray,
earlyTermination,
NIL(Fsm_HintsArray_t), Mc_None_c,
(Mc_VerbosityLevel) verbosity,
(Mc_DcLevel) dcLevel,
(dbgLevel != McDbgLevelNone_c || verbosity),
GSHschedule);
Mc_EarlyTerminationFree(earlyTermination);
mdd_free(mddOne);
/* If there is at least one fair initial state, language is not empty. */
if (!mdd_lequal(initialStates, fairStates, 1, 0)) {
if (strcmp(driverName, "LE") == 0)
fprintf(vis_stdout, "# LE: language is not empty\n");
else
fprintf(vis_stdout, "# %s: formula failed\n", driverName);
result = mdd_and(fairStates, initialStates, 1, 1);
} else {
if (strcmp(driverName, "LE") == 0)
fprintf(vis_stdout, "# LE: language emptiness check passes\n");
else
fprintf(vis_stdout, "# %s: formula passed\n", driverName);
Ctlp_FormulaFree(ctlFormula);
mdd_free(fairStates);
mdd_free(initialStates);
return NIL(mdd_t);
}
/* If no wintness is requested, clean up and return. */
if (dbgLevel == McDbgLevelNone_c) {
Ctlp_FormulaFree(ctlFormula);
mdd_free(initialStates);
mdd_free(fairStates);
return result;
}else {
Ctlp_Formula_t *F;
array_t *EGArrayOfOnionRings, *EGonionRings, *EFonionRings;
array_t *newOnionRings;
mdd_t *mdd1;
int j;
arrayOfOnionRings = array_alloc(array_t *, 0);
EFonionRings = (array_t *) Ctlp_FormulaReadDebugData(ctlFormula);
if (automatonStrength == 0) {
array_insert_last(array_t *, arrayOfOnionRings,
mdd_array_duplicate(EFonionRings));
}else if (automatonStrength == 1) {
F = Ctlp_FormulaReadRightChild(ctlFormula);
/* EG (states labelled fair) */
EGArrayOfOnionRings = (array_t *)Ctlp_FormulaReadDebugData(F);
arrayForEachItem(array_t *, EGArrayOfOnionRings, i, EGonionRings) {
newOnionRings = mdd_array_duplicate(EGonionRings);
arrayForEachItem(mdd_t *, EFonionRings, j, mdd1) {
if (j != 0)
array_insert_last(mdd_t *, newOnionRings, mdd_dup(mdd1));
}
array_insert_last(array_t *, arrayOfOnionRings, newOnionRings);
}
}
Ctlp_FormulaFree(ctlFormula);
fprintf(vis_stdout, "# %s: generating path to fair cycle\n", driverName);
}
}else {
/*************************************************************************
* CASE3: STRONG AUTOMATON
* need to solve the problem by computing EG_fair (true)
*************************************************************************/
mddMgr = Fsm_FsmReadMddManager(modelFsm);
initialStates = Fsm_FsmComputeInitialStates(modelFsm);
/* Compute fair states. */
if (lockstep == MC_LOCKSTEP_OFF) {
fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray,
verbosity, dcLevel, GSHschedule,
GSHdirection, FALSE);
arrayOfOnionRings = Fsm_FsmReadDebugArray(modelFsm);
} else {
/* For lockstep, the computed set of states is a subset of the
reachable fair states, with the property that the subset is
empty only if there are no reachable fair states. Since the
onion rings are built for the fairness constraint restricted to
the subset of the fair states, they are not valid in general
for the FSM. Hence, they are not saved. */
array_t *SCCs = array_alloc(mdd_t *, 0);
arrayOfOnionRings = array_alloc(array_t *, 0);
fairStates = McFsmComputeFairSCCsByLockStep(modelFsm, lockstep, SCCs,
arrayOfOnionRings,
(Mc_VerbosityLevel)
verbosity,
(Mc_DcLevel) dcLevel);
mdd_array_free(SCCs);
}
/* Lockstep guarantees that all fair SCCs are reachable. However,
it does not extend the fair states backward unless a
counterexample is requested. For the SCC hull approach with backward
operators, the language is not empty if there is at least one
fair initial state. Finally, For SCC hull with forward operators,
currently we do not extend the hull backward, but we enforce
reachability of the hull. Hence, nonemptiness of the hull signals that
the language is not empty. */
if ((lockstep == MC_LOCKSTEP_OFF &&
(!mdd_lequal(initialStates, fairStates, 1, 0) ||
(GSHdirection == McFwd_c &&
!mdd_lequal_array(fairStates, modelCareStatesArray, 1, 0)))) ||
(lockstep != MC_LOCKSTEP_OFF &&
!mdd_is_tautology(fairStates, 0))) {
if (strcmp(driverName, "LE") == 0)
fprintf(vis_stdout, "# LE: language is not empty\n");
else
fprintf(vis_stdout, "# %s: formula failed\n", driverName);
result = mdd_and(fairStates, initialStates, 1, 1);
} else {
if (strcmp(driverName, "LE") == 0)
fprintf(vis_stdout, "# LE: language emptiness check passes\n");
else
fprintf(vis_stdout, "# %s: formula passed\n", driverName);
/* Dispose of onion rings if produced by lockstep. */
if (lockstep != MC_LOCKSTEP_OFF) {
mdd_array_array_free(arrayOfOnionRings);
}
mdd_free(fairStates);
mdd_free(initialStates);
return NIL(mdd_t);
}
/* If no witness is requested, clean up and return. */
if (dbgLevel == McDbgLevelNone_c) {
/* Dispose of onion rings if produced by lockstep. */
if (lockstep != MC_LOCKSTEP_OFF) {
mdd_array_array_free(arrayOfOnionRings);
}
mdd_free(fairStates);
mdd_free(initialStates);
return result;
} else {
(void) fprintf(vis_stdout, "# %s: generating path to fair cycle\n",
driverName);
}
}
/* Generate witness. */
badStates = mdd_and(initialStates, fairStates, 1, 1);
mdd_free(fairStates);
mdd_free(initialStates);
aBadState = Mc_ComputeAState(badStates, modelFsm);
mdd_free(badStates);
mddOne = mdd_one(mddMgr);
fairPath = McBuildFairPath(aBadState, mddOne, arrayOfOnionRings, modelFsm,
modelCareStatesArray,
(Mc_VerbosityLevel) verbosity,
(Mc_DcLevel) dcLevel,
McFwd_c);
mdd_free(mddOne);
mdd_free(aBadState);
/* Dispose of onion rings if produced by lockstep. */
if (lockstep != MC_LOCKSTEP_OFF || automatonStrength != 2) {
mdd_array_array_free(arrayOfOnionRings);
}
/* Print witness. */
normalPath = McPathNormalize(fairPath);
McPathFree(fairPath);
stemArray = McPathReadStemArray(normalPath);
cycleArray = McPathReadCycleArray(normalPath);
/* we should pass dbgFile/UseMore as parameters
dbgFile = McOptionsReadDebugFile(options);*/
if (dbgFile != NIL(FILE)) {
vis_stdpipe = dbgFile;
} else if (UseMore == TRUE) {
vis_stdpipe = popen("more","w");
} else {
vis_stdpipe = vis_stdout;
}
vis_stdout = vis_stdpipe;
/* We should also pass SimValue as a parameter */
if (SimValue == FALSE) {
(void) fprintf(vis_stdout, "# %s: path to fair cycle:\n\n", driverName);
Mc_PrintPath(stemArray, modelFsm, printInputs);
fprintf (vis_stdout, "\n");
(void) fprintf(vis_stdout, "# %s: fair cycle:\n\n", driverName);
Mc_PrintPath(cycleArray, modelFsm, printInputs);
fprintf (vis_stdout, "\n");
}else {
array_t *completePath = McCreateMergedPath(stemArray, cycleArray);
(void) fprintf(vis_stdout, "# %s: counter-example\n", driverName);
McPrintSimPath(vis_stdout, completePath, modelFsm);
mdd_array_free(completePath);
}
if (dbgFile == NIL(FILE) && UseMore == TRUE) {
(void) pclose(vis_stdpipe);
}
vis_stdout = tmpFile;
McPathFree(normalPath);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateAUFormula | ( | Fsm_Fsm_t * | fsm, |
| mdd_t * | invariant, | ||
| mdd_t * | target, | ||
| mdd_t * | underapprox, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| Fsm_HintsArray_t * | hintsArray, | ||
| Mc_GuidedSearch_t | hintType, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint | ||
| ) |
Definition at line 974 of file mcMc.c.
{
return McEvaluateAUFormulaWithGivenTR(fsm, invariant, target,
underapprox, fairStates,
careStatesArray,
earlyTermination, onionRings,
verbosity, dcLevel, fixpoint);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateEGFormula | ( | Fsm_Fsm_t * | fsm, |
| mdd_t * | invariant, | ||
| mdd_t * | overapprox, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | modelFairness, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| Fsm_HintsArray_t * | hintsArray, | ||
| Mc_GuidedSearch_t | hintType, | ||
| array_t ** | pOnionRingsArrayForDbg, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint, | ||
| Mc_GSHScheduleType | GSHschedule | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying EG invariant]
Description [Evaluate states satisfying EG invariant. This is done by starting with all states marked with the invariant. From this initial set, recursively remove states that can not reach Buechi contraints (through paths entirely within the current set).
If overapprox is not nil, then it is a valid overapproximation to the satisfiable set of the formula that will be used to kick off the computation.
pOnionRingsArrayForDbg is a pointer to (a pointer to) an array of arrays of mdd_t *s. Upon calling this formula, it should point to an empty array if you want debug information, or be NIL (or a pointer to NIL) if you do not. After the call, it points to an array that contains one entry for every fairness constraint: entry i contains the onionrings for the last EU computation that was performed for fairness constraint i. There are two exceptions: if the satisfying set is 0, or if early termination kicks in, the onion ring array is not changed.
The arguments hintsArray and hints are used for guided search. Set hintType to Mc_None_c to ignore. If hintType is Mc_Local_c, hintsArray should be an array of mdds, of which the last entry is 1. This array will be used to obtain overapproximations of the transition system (See Mc_FsmEvaluateFormula).
fixpoint is a return argument. It is true if the formula is evaluated exactly, false if early termination kicked in. If earlyTermination is NIL, the formula is evaluated exacty, and this argument may be NIL too. See Mc_FsmEvaluateFormula for a discussion of early termination.]
SideEffects []
SeeAlso [Mc_FsmEvaluateFormula]
Definition at line 1041 of file mcMc.c.
{
/* Illegal to pass in onion rings. */
#if 0
assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
*pOnionRingsArrayForDbg == NIL(array_t) ||
array_n(*pOnionRingsArrayForDbg) == 0);
#endif
if(hintType != Mc_Local_c)
if (GSHschedule == McGSH_old_c) {
return McEvaluateEGFormulaWithGivenTR(fsm, invariant, overapprox,
fairStates,
modelFairness, careStatesArray,
earlyTermination,
pOnionRingsArrayForDbg,
verbosity,
dcLevel, fixpoint);
} else {
return McFsmEvaluateEGFormulaUsingGSH(fsm, invariant, overapprox,
fairStates,
modelFairness, careStatesArray,
earlyTermination,
pOnionRingsArrayForDbg, verbosity,
dcLevel, fixpoint, GSHschedule);
}
else {
mdd_t *iterate, *newiterate;
mdd_t *hint;
int hintnr;
boolean useRings;
useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
*pOnionRingsArrayForDbg != NIL(array_t));
if(verbosity >= McVerbosityMax_c)
fprintf(vis_stdout, "** mc Info: Using local hints\n");
if(overapprox != NIL(mdd_t))
iterate = mdd_dup(overapprox);
else
iterate = mdd_one(Fsm_FsmReadMddManager(fsm));
arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
if(verbosity >= McVerbosityMax_c)
fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Overapprox_c,
(verbosity >= McVerbosityMax_c));
/* old onionrings go stale. Fry 'em */
if(useRings){
mdd_array_array_free(*pOnionRingsArrayForDbg);
*pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
}
if (GSHschedule == McGSH_old_c) {
newiterate =
McEvaluateEGFormulaWithGivenTR(fsm, invariant, iterate, fairStates,
modelFairness, careStatesArray,
earlyTermination,
pOnionRingsArrayForDbg,
verbosity, dcLevel, fixpoint);
} else {
newiterate =
McFsmEvaluateEGFormulaUsingGSH(fsm, invariant, iterate,
fairStates,
modelFairness, careStatesArray,
earlyTermination,
pOnionRingsArrayForDbg, verbosity,
dcLevel, fixpoint, GSHschedule);
}
mdd_free(iterate);
iterate = newiterate;
/* check if we can terminate without considering all hints */
if(mdd_is_tautology(iterate, 0)){
*fixpoint = 1;
break;
}
if(McCheckEarlyTerminationForOverapprox(earlyTermination, iterate,
careStatesArray)){
*fixpoint = 0;
break;
}
} /* For all hints */
Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
return iterate;
}/* if hinttype */
} /* Mc_FsmEvaluateEGFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateEHFormula | ( | Fsm_Fsm_t * | fsm, |
| mdd_t * | invariant, | ||
| mdd_t * | overapprox, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | modelFairness, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| Fsm_HintsArray_t * | hintsArray, | ||
| Mc_GuidedSearch_t | hintType, | ||
| array_t ** | pOnionRingsArrayForDbg, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint, | ||
| Mc_GSHScheduleType | GSHschedule | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying EH invariant.]
Description [Evaluate states satisfying EH invariant. This is done by starting with all states marked with the invariant. From this initial set, recursively remove states that cannot reach Buechi contraints (through paths entirely within the current set).
If overapprox is not nil, then it is a valid overapproximation to the satisfiable set of the formula that will be used to kick off the computation.
pOnionRingsArrayForDbg is a pointer to (a pointer to) an array of arrays of mdd_t *s. Upon calling this formula, it should point to an empty array if you want debug information, or be NIL (or a pointer to NIL) if you do not. After the call, it points to an array that contains one entry for every fairness constraint: entry i contains the onionrings for the last ES computation that was performed for fairness constraint i. There are two exceptions: if the satisfying set is 0, or if early termination kicks in, the onion ring array is not changed.
The arguments hintsArray and hints are used for guided search. Set hintType to Mc_None_c to ignore. If hintType is Mc_Local_c, hintsArray should be an array of mdds, of which the last entry is 1. This array will be used to obtain overapproximations of the transition system (See Mc_FsmEvaluateFormula).
fixpoint is a return argument. It is true if the formula is evaluated exactly, false if early termination kicked in. If earlyTermination is NIL, the formula is evaluated exacty, and this argument may be NIL too. See Mc_FsmEvaluateFormula for a discussion of early termination.]
SideEffects []
SeeAlso [Mc_FsmEvaluateFormula]
Definition at line 1189 of file mcMc.c.
{
/* Illegal to pass in onion rings. */
assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
*pOnionRingsArrayForDbg == NIL(array_t) ||
array_n(*pOnionRingsArrayForDbg) == 0);
if(hintType != Mc_Local_c)
if (GSHschedule == McGSH_old_c) {
return McEvaluateEHFormulaWithGivenTR(fsm, invariant, overapprox,
fairStates,
modelFairness, careStatesArray,
earlyTermination,
pOnionRingsArrayForDbg,
verbosity,
dcLevel, fixpoint);
} else {
return McFsmEvaluateEHFormulaUsingGSH(fsm, invariant, overapprox,
fairStates,
modelFairness, careStatesArray,
earlyTermination,
pOnionRingsArrayForDbg, verbosity,
dcLevel, fixpoint, GSHschedule);
}
else {
mdd_t *iterate, *newiterate;
mdd_t *hint;
int hintnr;
boolean useRings;
useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
*pOnionRingsArrayForDbg != NIL(array_t));
if(verbosity >= McVerbosityMax_c)
fprintf(vis_stdout, "** mc Info: Using local hints\n");
if(overapprox != NIL(mdd_t))
iterate = mdd_dup(overapprox);
else
iterate = mdd_one(Fsm_FsmReadMddManager(fsm));
arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
if(verbosity >= McVerbosityMax_c)
fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Overapprox_c,
(verbosity >= McVerbosityMax_c));
/* old onionrings go stale. Fry 'em */
if(useRings){
mdd_array_array_free(*pOnionRingsArrayForDbg);
*pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
}
if (GSHschedule == McGSH_old_c) {
newiterate =
McEvaluateEHFormulaWithGivenTR(fsm, invariant, iterate, fairStates,
modelFairness, careStatesArray,
earlyTermination,
pOnionRingsArrayForDbg,
verbosity, dcLevel, fixpoint);
} else {
newiterate =
McFsmEvaluateEHFormulaUsingGSH(fsm, invariant, iterate,
fairStates,
modelFairness, careStatesArray,
earlyTermination,
pOnionRingsArrayForDbg, verbosity,
dcLevel, fixpoint, GSHschedule);
}
mdd_free(iterate);
iterate = newiterate;
/* check if we can terminate without considering all hints */
if(mdd_is_tautology(iterate, 0)){
*fixpoint = 1;
break;
}
if(McCheckEarlyTerminationForOverapprox(earlyTermination, iterate,
careStatesArray)){
*fixpoint = 0;
break;
}
} /* For all hints */
Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
return iterate;
}/* if hinttype */
} /* Mc_FsmEvaluateEHFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateESFormula | ( | Fsm_Fsm_t * | fsm, |
| mdd_t * | invariant, | ||
| mdd_t * | source, | ||
| mdd_t * | underapprox, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| Fsm_HintsArray_t * | hintsArray, | ||
| Mc_GuidedSearch_t | hintType, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying E(invariant S source)]
Description [Evaluate states satisfying E(invariant U target). Performed by a least fixed point computation -- start with source AND fair, see what can be reached from this set by a path solely in invariant. If the onionRings array is not NIL(array_t *), the ``onion rings'' arising in the least fixed point computation are stored in the array, starting from the target.
The evaluation stops once all (some) of earlyTermination.states have been found (depending on earlyTermination.mode). See Mc_FsmEvaluateFormula()
If underapprox is not NIL, it must hold a valid underapproximation of the fixpoint. This is used to kick off the new computation.
The arguments hintsArray and hints are used for guided search. Set hintType to Mc_None_c to ignore. If hintType is Mc_Local_c, hintsArray should be an array of mdds, of which the last entry is 1. This array will be used to obtain underapproximations of the transition system. (See Mc_FsmEvaluateFormula.)
fixpoint is a return argument. It is true if the formula is evaluated exactly, false if early termination kicked in. If earlyTermination is NIL, the formula is evaluated exacty, and this argument may be NIL too.
OnionRIngs is an array of mdd_t *. It should be empty on call if you want debug info, NULL otherwise. After the call, it contains the onion rings (frontier sets) that occured while computing the ES. This is used for debugging.]
Comment [Check that evaluation mod reached AND fair will lead to faster convergence. Also, it is possible there is more (?) flexibility in don't care minimization - use only the layer of the onion rings as set for evaluating EX.]
SideEffects []
SeeAlso [Mc_FsmEvaluateFormula, McEvaluateESFormulaWithGivenTR]
Definition at line 894 of file mcMc.c.
{
/* should be strengthened to check that rings supply a correct explanation.
*/
assert(underapprox == NULL || onionRings == NULL ||
array_n(onionRings) != 0);
if(hintType != Mc_Local_c)
/* postcondition: rings should explain how to get from return value to
* target.
*/
return McEvaluateESFormulaWithGivenTR(fsm, invariant, source,
underapprox, fairStates,
careStatesArray,
earlyTermination, onionRings,
verbosity, dcLevel, fixpoint);
else{
mdd_t *iterate, *newiterate;
mdd_t *hint;
int hintnr;
if(verbosity >= McVerbosityMax_c)
fprintf(vis_stdout, "--Using local hints\n");
if(underapprox != NIL(mdd_t))
iterate = mdd_dup(underapprox);
else
iterate = mdd_zero(Fsm_FsmReadMddManager(fsm));
arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
if(verbosity >= McVerbosityMax_c)
fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c,
(verbosity >= McVerbosityMax_c));
newiterate =
McEvaluateESFormulaWithGivenTR(fsm, invariant, source, iterate,
fairStates, careStatesArray,
earlyTermination, onionRings,
verbosity, dcLevel, fixpoint);
mdd_free(iterate);
iterate = newiterate;
/* check if we can terminate without considering all hints */
if(mdd_is_tautology(iterate, 1)){
*fixpoint = 1;
break;
}
if(McCheckEarlyTerminationForUnderapprox(earlyTermination, iterate,
careStatesArray)){
*fixpoint = 0;
break;
}
}/* for all hints */
Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
/* postcondition: rings should explain how to get from return value to
* target.
*/
return iterate;
}/* if hinttype */
} /* Mc_FsmEvaluateESFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateEUFormula | ( | Fsm_Fsm_t * | fsm, |
| mdd_t * | invariant, | ||
| mdd_t * | target, | ||
| mdd_t * | underapprox, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| Fsm_HintsArray_t * | hintsArray, | ||
| Mc_GuidedSearch_t | hintType, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying E(invariant U target)]
Description [Evaluate states satisfying E(invariant U target). Performed by a least fixed point computation -- start with target AND fair, see what can get to this set by a path solely in invariant. If the onionRings array is not NIL(array_t *), the ``onion rings'' arising in the least fixed point computation are stored in the array, starting from the target. The onion rings explain how to get from any state in the result to the target.
The evaluation stops once all (some) of earlyTermination.states have been found (depending on earlyTermination.mode). See Mc_FsmEvaluateFormula()
If underapprox is not NIL, it must hold a valid underapproximation of the fixpoint. This is used to kick off the new computation.
The arguments hintsArray and hints are used for guided search. Set hintType to Mc_None_c to ignore. If hintType is Mc_Local_c, hintsArray should be an array of mdds, of which the last entry is 1. This array will be used to obtain underapproximations of the transition system. (See Mc_FsmEvaluateFormula.)
fixpoint is a return argument. It is true if the formula is evaluated exactly, false if early termination kicked in. If earlyTermination is NIL, the formula is evaluated exacty, and this argument may be NIL too.
OnionRings is an array of mdd_t *. It can be NULL, in which case no onion rings are returned. If it is not NULL, there are two possibilities. In the simple case, the onion rings are empty, and underapprox is NULL. In this case, the onion rings returned explain how to get to the target from any state in the result returned (r). If underapprox u is not NULL, the onion rings that are passed in should explain how to get from any state in u to any state in the target. Rings will be added by the procudure to explain how to get from the r to a state in underapprox, resulting in an explanation of how to get from a state in r to the target. ]
Comment [Check that evaluation mod reached AND fair will lead to faster convergence. Also, it is possible there is more (?) flexibility in dont care minimization - use only the layer of the onion rings as set for evaluating EX.]
SideEffects []
SeeAlso [Mc_FsmEvaluateFormula, McEvaluateEUFormulaWithGivenTR]
Definition at line 769 of file mcMc.c.
{
/* should be strengthened to check that rings supply a correct explanation.
*/
/*check out
* assert(underapprox == NULL || onionRings == NULL ||
* array_n(onionRings) != 0); */
if(hintType != Mc_Local_c)
/* postcondition: rings should explain how to get from return value to
* target.
*/
return McEvaluateEUFormulaWithGivenTR(fsm, invariant, target,
underapprox, fairStates,
careStatesArray,
earlyTermination, onionRings,
verbosity, dcLevel, fixpoint);
else{
mdd_t *iterate, *newiterate;
mdd_t *hint;
int hintnr;
if(verbosity >= McVerbosityMax_c)
fprintf(vis_stdout, "--Using local hints\n");
if(underapprox != NIL(mdd_t))
iterate = mdd_dup(underapprox);
else
iterate = mdd_zero(Fsm_FsmReadMddManager(fsm));
arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
if(verbosity >= McVerbosityMax_c)
fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c,
(verbosity >= McVerbosityMax_c));
newiterate =
McEvaluateEUFormulaWithGivenTR(fsm, invariant, target, iterate,
fairStates, careStatesArray,
earlyTermination, onionRings,
verbosity, dcLevel, fixpoint);
mdd_free(iterate);
iterate = newiterate;
/* check if we can terminate without considering all hints */
if(mdd_is_tautology(iterate, 1)){
*fixpoint = 1;
break;
}
if(McCheckEarlyTerminationForUnderapprox(earlyTermination, iterate,
careStatesArray)){
*fixpoint = 0;
break;
}
}/* for all hints */
Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
/* postcondition: rings should explain how to get from return value to
* target.
*/
return iterate;
}/* if hinttype */
} /* Mc_FsmEvaluateEUFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateEXFormula | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | targetMdd, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying EX target]
Description [Evaluate states satisfying EX target. Basically, calls the image package -- all the smarts are in there, parameters for it can be set from the VIS prompt. In the presence of fairness, a state satisifies EX foo just in case it has a sucessor where foo is true AND that successor can be continued to an infinite path which is fair.]
SideEffects []
Definition at line 526 of file mcMc.c.
{
mdd_t *fromLowerBound;
mdd_t *fromUpperBound;
mdd_t *result;
Img_ImageInfo_t * imageInfo;
if(Fsm_FsmReadUseUnquantifiedFlag(modelFsm))
imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 1, 0);
else
imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
/*
* The lower bound is the conjunction of the fair states,
* and the target states.
*/
fromLowerBound = mdd_and(targetMdd, fairStates, 1, 1);
/*
* The upper bound is the same as the lower bound.
*/
fromUpperBound = mdd_dup(fromLowerBound);
result = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
fromLowerBound, fromUpperBound, careStatesArray);
mdd_free(fromLowerBound);
mdd_free(fromUpperBound);
if (verbosity == McVerbosityMax_c) {
static int refCount=0;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
mdd_t *tmpMdd = careStatesArray ?
mdd_and_array(result, careStatesArray, 1, 1) : mdd_dup(result);
fprintf(vis_stdout, "--EX called %d (bdd_size - %d)\n", ++refCount,
mdd_size(result));
fprintf(vis_stdout, "--There are %.0f care states satisfying EX formula\n",
mdd_count_onset(mddMgr, tmpMdd, psVars));
mdd_free(tmpMdd);
}
return result;
} /* Mc_FsmEvaluateEXFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateEYFormula | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | targetMdd, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying EY target]
Description [Evaluate states satisfying EY target.]
SideEffects []
Definition at line 671 of file mcMc.c.
{
mdd_t *fromLowerBound;
mdd_t *fromUpperBound;
mdd_t *result;
Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
/*
* The lower bound is the conjunction of the fair states,
* and the target states.
*/
fromLowerBound = mdd_and(targetMdd, fairStates, 1, 1);
/*
* The upper bound is the same as the lower bound.
*/
fromUpperBound = fromLowerBound;
result = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
fromLowerBound, fromUpperBound, careStatesArray);
mdd_free(fromLowerBound);
if (verbosity == McVerbosityMax_c) {
static int refCount=0;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
mdd_t *tmpMdd = careStatesArray ?
mdd_and_array(result, careStatesArray, 1, 1) : mdd_dup(result);
fprintf(vis_stdout, "--EY called %d (bdd_size - %d)\n", ++refCount,
mdd_size(result));
fprintf(vis_stdout, "--There are %.0f care states satisfying EY formula\n",
mdd_count_onset(mddMgr, tmpMdd, psVars));
mdd_free(tmpMdd);
}
return result;
} /* Mc_FsmEvaluateEYFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateFormula | ( | Fsm_Fsm_t * | fsm, |
| Ctlp_Formula_t * | ctlFormula, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | fairCondition, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| Fsm_HintsArray_t * | hintsArray, | ||
| Mc_GuidedSearch_t | hintType, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| int | buildOnionRing, | ||
| Mc_GSHScheduleType | GSHschedule | ||
| ) |
Function********************************************************************
Synopsis [Model check formula on given FSM under fairness]
Description [Model check formula on given FSM under fairness.]
Comment [ Recursive evaluation using Emerson-Lei LICS 1986 algorithms. The states satisfying subformulas are stored and used later if there is sharing of subformulas. Therefore, each subformula is computed just once. Large switch - base case is atomic formula, TRUE, and FALSE. Boolean operators - straightforward. Path modalities are reduced to one of the three - EX, EU, EG which are evaluated under fairness. Note the semantics for atomic formulas carefully - in addition to generating the prescribed output, the state must also be fair. Don't cares from unreached, unfair states are both used. The proof of correctness of using all these dont cares hinges on the invariant that restricted to the reached state set, the computed sets are exactly as they should be. Both backward and forward formulas are handled.
This function sets the states and debug info of the formula for use with the debugger.
ARGUMENTS:
ctlFormula: a ctl formula in simple(!) existential form, using forward and/or backward operators.
EarlyTermination: If earlyTermination.mode is McAll_c (McSome_c), the algorithm can stop as soon as
1. it is sure that all (some) of earlyTermination.states are included in the evaluation of the formula, or
2. It is sure that some (all) of these states are not included in the evaluation.
If earlyTermination.mode is McCare_c, then the algorithm can stop as soon as it is guaranteed that either all or none of earlyTermination.states are included in the evaluation.
These checks are done modulo the care set, but not modulo the fair states, which means that they will not be effective if you require unfair states to be in the evaluation. Typically {ALL, initialStates} will be good. NULL means the option has no effect.
Debugging only works if this function is called with {ALL, initialStates}. Otherwise, debugging of the EG formulae may go wrong.
hintsArray is an array of hints. Pass NULL and set hintType to Mc_None_c to ignore.
If hintType is Mc_Global_c, then the formula is evaluated once for each hint, where every hint defines an underapproximation of the formula. This only works for pure A/E CTL formulae. If hintType is Mc_Local_c, then every fixpoint goes through the sequence of hints until completion, before moving up to the next temporal operator.
]
SideEffects []
Definition at line 450 of file mcMc.c.
{
mdd_t *hint; /* to iterate over hintsArray */
int hintnr; /* idem */
Ctlp_Approx_t resultApproxType;
assert(hintType == Mc_None_c || hintsArray != NIL(Fsm_HintsArray_t));
if(hintType != Mc_Global_c)
return EvaluateFormulaRecur(fsm, ctlFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
Ctlp_Exact_c, &resultApproxType,
verbosity, dcLevel,
buildOnionRing, GSHschedule);
else{
mdd_t *result = NIL(mdd_t);
Ctlp_Approx_t approx;
if(verbosity >= McVerbosityMax_c)
fprintf(vis_stdout, "--Using global hints\n");
arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
if(result != NIL(mdd_t))
mdd_free(result);
if(verbosity >= McVerbosityMax_c)
fprintf(vis_stdout, "--Instantiating global hint %d\n", hintnr);
Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c,
(verbosity >= McVerbosityMax_c));
approx = mdd_is_tautology(hint, 1) ? Ctlp_Exact_c : Ctlp_Underapprox_c;
result = EvaluateFormulaRecur(fsm, ctlFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
approx, &resultApproxType, verbosity,
dcLevel, buildOnionRing, GSHschedule);
/* TBD: take into account (early) termination here */
}
Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
return result;
}
} /* Mc_FsmEvaluateFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateFwdEHFormula | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | invariantMdd, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | modelFairness, | ||
| array_t * | careStatesArray, | ||
| array_t * | onionRingsArrayForDbg, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying EH invariant]
Description [Evaluate states satisfying EH invariant.]
SideEffects []
Definition at line 1488 of file mcMc.c.
{
int i;
array_t *onionRings = NIL(array_t);
array_t *tmpOnionRingsArrayForDbg = NIL(array_t);
mdd_manager *mddManager = Fsm_FsmReadMddManager(modelFsm);
mdd_t *mddOne = mdd_one(mddManager);
mdd_t *Zmdd;
int nIterations = 0;
int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
/*
** EG(f) = gfp Z[f ^ EX(Z)]
** EH(f) = gfp Z[f ^ EY(Z)]
**
** EcG(f) = gfp Z[f ^ EX( ^ E[Z U Z ^ c])]
** c<C
** EcH(f) = gfp Z[f ^ EY( ^ Reachable(c,Z))]
** c<C
** Reachable(p,q) = FwdUntil(p,q) ^ q
*/
array_t *buchiFairness = array_alloc(mdd_t *, 0);
if (modelFairness) {
if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
(void) fprintf(vis_stdout,
"** mc error: non-Buechi fairness constraints not supported\n");
return NIL(mdd_t);
}
else {
int j;
int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
for (j = 0; j < numBuchi; j++) {
mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
careStatesArray, dcLevel);
array_insert_last(mdd_t *, buchiFairness, tmpMdd);
}
}
}
else {
array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager));
}
if (onionRingsArrayForDbg !=NIL(array_t)) {
tmpOnionRingsArrayForDbg = array_alloc(array_t *, 0);
}
Zmdd = mdd_dup(invariantMdd);
while (TRUE) {
mdd_t *ZprimeMdd = mdd_dup(Zmdd);
mdd_t *conjunctsMdd = NIL(mdd_t);
mdd_t *AAmdd = mdd_dup(Zmdd);
nIterations++;
for (i = 0; i < array_n(buchiFairness); i++) {
mdd_t *aMdd, *bMdd;
mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i);
if (tmpOnionRingsArrayForDbg) {
onionRings = array_alloc(mdd_t *, 0);
array_insert_last(array_t *, tmpOnionRingsArrayForDbg, onionRings);
}
aMdd = McForwardReachable(modelFsm, FiMdd, AAmdd, mddOne, careStatesArray,
onionRings, verbosity, dcLevel);
bMdd = Mc_FsmEvaluateEYFormula(modelFsm, aMdd, mddOne, careStatesArray,
verbosity, dcLevel);
mdd_free(aMdd);
if (conjunctsMdd == NIL(mdd_t)) {
conjunctsMdd = mdd_dup(bMdd);
}
else {
mdd_t *tmpMdd = mdd_and(bMdd, conjunctsMdd, 1, 1);
mdd_free(conjunctsMdd);
conjunctsMdd = tmpMdd;
}
mdd_free(AAmdd); AAmdd = mdd_and(conjunctsMdd, invariantMdd, 1, 1);
mdd_free(bMdd);
}
mdd_free(AAmdd);
mdd_free(ZprimeMdd);
ZprimeMdd = mdd_and(invariantMdd, conjunctsMdd, 1, 1);
mdd_free(conjunctsMdd);
if (mdd_equal_mod_care_set_array(ZprimeMdd, Zmdd, careStatesArray)) {
mdd_free(ZprimeMdd);
break;
}
mdd_free(Zmdd);
Zmdd = ZprimeMdd;
if (tmpOnionRingsArrayForDbg) {
arrayForEachItem(array_t *, tmpOnionRingsArrayForDbg, i, onionRings) {
mdd_array_free(onionRings);
}
array_free(tmpOnionRingsArrayForDbg);
tmpOnionRingsArrayForDbg = array_alloc(array_t *, 0);
}
}
if (onionRingsArrayForDbg != NIL(array_t)) {
arrayForEachItem(array_t *, tmpOnionRingsArrayForDbg, i, onionRings) {
array_insert_last(array_t *, onionRingsArrayForDbg, onionRings);
}
array_free(tmpOnionRingsArrayForDbg);
}
if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
if (onionRingsArrayForDbg) {
for (i = 0; i < array_n(onionRingsArrayForDbg); i++) {
int j;
mdd_t *Fi = array_fetch(mdd_t *, buchiFairness, i);
array_t *onionRings = array_fetch(array_t *, onionRingsArrayForDbg, i);
for (j = 0; j < array_n(onionRings); j++) {
mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
if (j == 0) {
if (!mdd_lequal(ring, Fi, 1, 1)) {
fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
fprintf(vis_stderr,
"inner most ring not in Fi(fairness constraint).\n");
}
}
if (!mdd_lequal(ring, Zmdd, 1, 1)) {
fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
fprintf(vis_stderr, "onion ring of last FwdU fails invariant\n");
}
}
}
}
if (verbosity == McVerbosityMax_c) {
mdd_t *tmpMdd = careStatesArray ?
mdd_and_array(Zmdd, careStatesArray, 1, 1) :
mdd_dup(Zmdd);
fprintf(vis_stdout,
"--There are %.0f care states satisfying EH formula\n",
mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd,
Fsm_FsmReadPresentStateVars(modelFsm)));
#ifdef DEBUG_MC
/* The following 2 lines are just for debug */
fprintf(vis_stdout, "EH satisfying minterms :\n");
(void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
mdd_free(tmpMdd);
} else {
fprintf(vis_stdout, "--There are %.0f states satisfying EH formula\n",
mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), Zmdd,
Fsm_FsmReadPresentStateVars(modelFsm)));
}
fprintf(vis_stdout, "--EH: %d iterations, %d image computations\n",
nIterations, Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
}
mdd_array_free(buchiFairness);
mdd_free(mddOne);
return Zmdd;
} /* Mc_FsmEvaluateFwdEHFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateFwdGFormula | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | targetMdd, | ||
| mdd_t * | invariantMdd, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | modelFairness, | ||
| array_t * | careStatesArray, | ||
| array_t * | onionRingsArrayForDbg, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying FwdG invariant]
Description [Evaluate states satisfying FwdG invariant.]
SideEffects []
Definition at line 1435 of file mcMc.c.
{
mdd_t *resultMdd, *invariant;
array_t *onionRings;
int nImgComps;
nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
onionRings = NIL(array_t);
invariant = McForwardReachable(modelFsm, targetMdd, invariantMdd, fairStates,
careStatesArray, onionRings, verbosity,
dcLevel);
resultMdd = Mc_FsmEvaluateFwdEHFormula(modelFsm, invariant, fairStates,
modelFairness, careStatesArray,
onionRingsArrayForDbg, verbosity,
dcLevel);
mdd_free(invariant);
if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
fprintf(vis_stdout, "--FwdG: %d image computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
}
#ifdef DEBUG_MC
/* The following 2 lines are just for debug */
if ((verbosity == McVerbosityMax_c)) {
fprintf(vis_stdout, "FwdG satisfying minterms :\n");
(void)_McPrintSatisfyingMinterms(resultMdd, modelFsm);
}
#endif
return resultMdd;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateFwdUFormula | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | targetMdd, | ||
| mdd_t * | invariantMdd, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying FwdUntil]
Description [Evaluate states satisfying FwdUntil.]
Comment []
SideEffects []
Definition at line 1307 of file mcMc.c.
{
mdd_t *aMdd;
mdd_t *bMdd;
mdd_t *cMdd;
mdd_t *resultMdd;
mdd_t *ringMdd;
int nImgComps;
/* t
** E[p U q] = lfp Z[q V (p ^ EX(Z))] : p p ... p q
** FwdUntil(p,q) = lfp Z[p V EY(Z ^ q)] : pq q q ... q
*/
nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
resultMdd = mdd_and(targetMdd, fairStates, 1, 1);
ringMdd = mdd_dup(resultMdd);
/* if until is trivially satisfied, */
if (onionRings) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
if (mdd_is_tautology(fairStates, 1)) {
if (mdd_equal_mod_care_set_array(invariantMdd, resultMdd, careStatesArray))
{
bdd_free(ringMdd);
return(resultMdd);
}
} else {
bdd_t *trivialCheck = mdd_and(invariantMdd, fairStates, 1, 1);
if (mdd_equal_mod_care_set_array(trivialCheck, resultMdd, careStatesArray)) {
bdd_free(trivialCheck);
bdd_free(ringMdd);
return(resultMdd);
}
bdd_free(trivialCheck);
}
while (TRUE) {
aMdd = mdd_and(ringMdd, invariantMdd, 1, 1);
mdd_free(ringMdd);
bMdd = Mc_FsmEvaluateEYFormula(modelFsm, aMdd, fairStates, careStatesArray,
verbosity, dcLevel);
mdd_free(aMdd);
cMdd = mdd_or(resultMdd, bMdd, 1, 1);
mdd_free(bMdd);
if (mdd_equal_mod_care_set_array(cMdd, resultMdd, careStatesArray)) {
mdd_free(cMdd);
break;
}
if (dcLevel >= McDcLevelRchFrontier_c) {
mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
ringMdd = bdd_between(tmpMdd, cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout,
"-- FwdU |A(n+1)-A(n)| = %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
}
mdd_free(tmpMdd);
}
else {
ringMdd = mdd_dup(cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout, "-- FwdU |ringMdd| = %d\n", mdd_size(ringMdd));
}
}
mdd_free(resultMdd);
resultMdd = cMdd;
if (onionRings) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
} /* while(!termination) for LFP */
/* Print some debug info */
if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
static int refCount=0;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
if (verbosity == McVerbosityMax_c) {
mdd_t *tmpMdd = careStatesArray ?
mdd_and_array(resultMdd, careStatesArray, 1, 1) :
mdd_dup(resultMdd);
fprintf(vis_stdout, "--FwdU called %d (bdd_size - %d)\n",
++refCount, mdd_size(resultMdd));
fprintf(vis_stdout,
"--There are %.0f care states satisfying FwdU formula\n",
mdd_count_onset(mddMgr, tmpMdd, psVars));
#ifdef DEBUG_MC
/* The following 2 lines are just for debug */
fprintf(vis_stdout, "FwdU satisfying minterms :\n");
(void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
mdd_free(tmpMdd);
} else {
fprintf(vis_stdout,
"--There are %.0f states satisfying FwdU formula\n",
mdd_count_onset(mddMgr, resultMdd, psVars));
}
fprintf(vis_stdout, "--FwdU: %d image computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
}
return resultMdd;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmEvaluateMXFormula | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | targetMdd, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying MX target]
Description [Compute EX with transition relation that contains input varaibles and then apply universial quantification to get MX target. To use this function, one has to run Fsm_FsmReadOrCreateImageInfoFAFW to create the trasition relation that contains input variables. And Fsm_FsmSetUseUnquantifiedFlag has to be called. That useUnquantifiedFlag is used to specify which imageInfo can be used in image computation. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
Definition at line 594 of file mcMc.c.
{
mdd_t *resultBar, *result;
result = Mc_FsmEvaluateEXFormula(modelFsm, targetMdd, fairStates,
careStatesArray, verbosity, dcLevel);
if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
resultBar = Mc_QuantifyInputFAFW(modelFsm, result);
mdd_free(result);
result = resultBar;
}
return(result);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_t* Mc_QuantifyInputFAFW | ( | Fsm_Fsm_t * | fsm, |
| bdd_t * | result | ||
| ) |
Function********************************************************************
Synopsis [Quantify the input variables]
Description [Quantify the input variables after applying EX. To use this function, one has to run Fsm_FsmReadOrCreateImageInfoFAFW to create the trasition relation that contains input variables. To get the result of real MX operation, the bdd_smooth_with_cube has to be applied after bdd_consensus_with_cube, but we need those input variables for path generation. If one needs real MX then bdd_smooth_with_cube has to be applied. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
newResult = bdd_consensus_with_cube(result, uniCube);
Definition at line 634 of file mcMc.c.
{
bdd_t *uniCube, *extCube, *newResult;
bdd_t *oneMdd, *notResult;
mdd_manager *mgr = Fsm_FsmReadMddManager(fsm);
oneMdd = mdd_one(mgr);
uniCube = Fsm_FsmReadUniQuantifyInputCube(fsm);
extCube = Fsm_FsmReadExtQuantifyInputCube(fsm);
if(!mdd_equal(uniCube, oneMdd)) {
notResult = bdd_not(result);
newResult = bdd_smooth_with_cube(notResult, uniCube);
bdd_free(notResult);
result = bdd_not(newResult);
bdd_free(newResult);
}
else {
result = mdd_dup(result);
}
mdd_free(oneMdd);
return(result);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McEvaluateAUFormulaWithGivenTR | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | invariantMdd, | ||
| mdd_t * | targetMdd, | ||
| mdd_t * | underapprox, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint | ||
| ) |
Function********************************************************************
Synopsis []
Description []
SeeAlso []
SideEffects []
Definition at line 2368 of file mcMc.c.
{
mdd_t *aMdd;
mdd_t *bMdd;
mdd_t *cMdd;
mdd_t *resultMdd;
mdd_t *ringMdd;
boolean term_tautology = FALSE; /* different termination conditions */
boolean term_early = FALSE;
boolean term_fixpoint = FALSE;
resultMdd = mdd_and(targetMdd, fairStates, 1, 1);
ringMdd = mdd_dup(resultMdd);
if (onionRings) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
/* The LFP loop */
while (!term_fixpoint && !term_tautology && !term_early) {
/* If dclevel is maximal, ringbdd is between the frontier and the
reached set */
aMdd = Mc_FsmEvaluateMXFormula(modelFsm, ringMdd, fairStates,
careStatesArray, verbosity, dcLevel);
bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
mdd_free(aMdd);
cMdd = mdd_or(resultMdd, bMdd, 1, 1);
mdd_free(bMdd);
mdd_free(ringMdd);
/* Can we stop? The tautology condition can be weakened to
cMdd <= careStatesArray */
term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
careStatesArray);
if(!term_fixpoint)
term_tautology = mdd_is_tautology(cMdd, 1);
if(!term_fixpoint && !term_tautology)
term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination,
cMdd,
careStatesArray);
/* Print some debug info, and set ringmdd */
if (dcLevel >= McDcLevelRchFrontier_c) {
mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
ringMdd = bdd_between(tmpMdd, cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout,
"--AU |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
}
mdd_free(tmpMdd);
}
else {
ringMdd = mdd_dup(cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout, "-- AU |ringMdd| = %d\n", mdd_size(ringMdd));
}
}
mdd_free(resultMdd);
resultMdd = cMdd;
/* add onion ring unless fixpoint reached */
if (!term_fixpoint && onionRings) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
} /* while(!termination) for LFP */
mdd_free(ringMdd);
if(fixpoint != NIL(boolean))
*fixpoint = term_fixpoint || term_tautology;
return resultMdd;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McEvaluateEGFormulaWithGivenTR | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | invariantMdd, | ||
| mdd_t * | overapprox, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | modelFairness, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| array_t ** | pOnionRingsArrayForDbg, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying EG(invariantMdd), given a transition relation]
Description [Does the same as Mc_FsmEvaluateEGFormula, minus the hints.]
SeeAlso [Mc_FsmEvaluateEGFormula]
SideEffects []
Definition at line 2470 of file mcMc.c.
{
int i;
array_t *onionRings;
boolean useRings;
mdd_manager *mddManager;
mdd_t *mddOne;
mdd_t *iterate;
array_t *buchiFairness;
int nPreComps;
int nIterations;
boolean term_fixpoint = FALSE; /* different termination conditions */
boolean term_tautology = FALSE;
boolean term_early = FALSE;
/* Here's how the onionRingsArrayForDbg works. It is an array of
arrays of mdds. It is filled in anew for every pass of the
algorithm, that is for every /\_{c inC} EXE(Y U Y*c). There is
one entry for every fairness constraint, and this entry contains
the onionrings of the EU computation that corresponds to this
constraint. */
assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
*pOnionRingsArrayForDbg == NIL(array_t) ||
array_n(*pOnionRingsArrayForDbg) == 0);
useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
*pOnionRingsArrayForDbg != NIL(array_t));
nIterations = 0;
nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
onionRings = NIL(array_t);
mddManager = Fsm_FsmReadMddManager(modelFsm);
mddOne = mdd_one(mddManager);
/* If an overapproximation of the greatest fixpoint is given, use it. */
if(overapprox != NIL(mdd_t)){
iterate = mdd_and(invariantMdd, overapprox, 1, 1);
} else {
iterate = mdd_dup(invariantMdd);
}
/* See if we need to enter the loop at all. If we wanted to test for
* early termination here, we should fix the onion rings. In the current
* case, we do not need to, since the EG does not hold, and hence a
* counterexample does not exist.
*/
if( mdd_is_tautology(iterate, 0)){
mdd_free(mddOne);
if(fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0);
return(iterate);
}
/* read fairness constraints */
buchiFairness = array_alloc(mdd_t *, 0);
if(modelFairness != NIL(Fsm_Fairness_t)) {
if(!Fsm_FairnessTestIsBuchi(modelFairness)) {
(void)fprintf(vis_stdout,
"** mc error: non-Buechi fairness constraints not supported\n");
array_free(buchiFairness);
mdd_free(iterate);
mdd_free(mddOne);
if(fixpoint != NIL(boolean)) *fixpoint = FALSE;
return NIL(mdd_t);
}
else {
int j;
int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
for (j = 0 ; j < numBuchi; j++) {
mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
careStatesArray, dcLevel);
array_insert_last(mdd_t *, buchiFairness, tmpMdd);
}
}
}
else {
array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager));
}
/* GFP. If we know that the result is a subset of a set S, we can conjoin
the iterate with that set. We use this to converge faster. */
while (TRUE) {
mdd_t *newIterate; /* the new iterate */
nIterations++;
newIterate = mdd_dup(iterate);
/* for all fairness constraints */
for (i = 0 ; i < array_n(buchiFairness) ; i++) {
mdd_t *aMdd, *bMdd, *cMdd, *dMdd;
mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i);
if(useRings) {
onionRings = array_alloc(mdd_t *, 0);
array_insert_last(array_t *, *pOnionRingsArrayForDbg, onionRings);
}
aMdd = mdd_and(FiMdd, newIterate, 1, 1);
bMdd = Mc_FsmEvaluateEUFormula(modelFsm, newIterate, aMdd, NIL(mdd_t),
mddOne, careStatesArray,
MC_NO_EARLY_TERMINATION, NIL(array_t),
Mc_None_c, onionRings, verbosity, dcLevel,
NIL(boolean));
mdd_free(aMdd);
cMdd = Mc_FsmEvaluateEXFormula(modelFsm, bMdd, mddOne, careStatesArray,
verbosity, dcLevel);
mdd_free(bMdd);
dMdd = mdd_and(newIterate, cMdd, 1, 1);
mdd_free(cMdd);
mdd_free(newIterate);
newIterate = dMdd;
/* invariants that hold here: newiterate <= iterate <= invariant. */
}/* for all fairness constraints */
/* termination */
term_tautology = mdd_is_tautology(newIterate, 0);
if(!term_tautology)
term_fixpoint = mdd_equal_mod_care_set_array(newIterate, iterate,
careStatesArray);
if(!term_tautology && !term_fixpoint)
term_early = McCheckEarlyTerminationForOverapprox(earlyTermination,
newIterate,
careStatesArray);
if(term_tautology || term_fixpoint || term_early){
mdd_free(iterate);
iterate = newIterate;
break; /* from the GFP loop */
}
/* update iterate */
mdd_free(iterate);
iterate = newIterate;
if(useRings){
mdd_array_array_free(*pOnionRingsArrayForDbg);
*pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
}
} /* while(true) for gfp */
/* Check if onionrings are OK */
if(verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
if(useRings){
for (i = 0 ; i < array_n(*pOnionRingsArrayForDbg); i++) {
int j;
mdd_t *Fi = array_fetch(mdd_t *, buchiFairness, i);
array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
i);
for (j = 0 ; j < array_n(onionRings); j++) {
mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
if(j == 0) {
if(!mdd_lequal_mod_care_set_array(ring, Fi, 1, 1,
careStatesArray)) {
fprintf(vis_stderr, "** mc error: Problem w/ dbg in EG - ");
fprintf(vis_stderr,
"inner most ring not in Fi (fairness constraint).\n");
}
}
if(!mdd_lequal_mod_care_set_array(ring, invariantMdd, 1, 1,
careStatesArray)) {
fprintf(vis_stderr, "** mc error: Problem w/ dbg in EG - ");
fprintf(vis_stderr, "An onion ring of last EU fails invariant\n");
}
} /* for all onionrings in array i */
} /* for all onionringarrays in onionringsarray */
}/* if useRings */
if(verbosity == McVerbosityMax_c) {
mdd_t *tmpMdd = careStatesArray ?
mdd_and_array(iterate, careStatesArray, 1, 1) : mdd_dup(iterate);
fprintf(vis_stdout,
"--There are %.0f care states satisfying EG formula\n",
mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd,
Fsm_FsmReadPresentStateVars(modelFsm)));
#ifdef DEBUG_MC
/* The following 2 lines are just for debug */
fprintf(vis_stdout, "EG satisfying minterms :\n");
(void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
mdd_free(tmpMdd);
} else {
fprintf(vis_stdout, "--There are %.0f states satisfying EG formula\n",
mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), iterate,
Fsm_FsmReadPresentStateVars(modelFsm)));
}
fprintf(vis_stdout, "--EG: %d iterations, %d preimage computations\n",
nIterations, Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
}
mdd_array_free(buchiFairness);
mdd_free(mddOne);
if(fixpoint != NIL(boolean))
*fixpoint = term_fixpoint || term_tautology;
return iterate;
} /* McEvaluateEGFormulaWithGivenTR */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McEvaluateEHFormulaWithGivenTR | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | invariantMdd, | ||
| mdd_t * | overapprox, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | modelFairness, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| array_t ** | pOnionRingsArrayForDbg, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying EH(invariantMdd), given a transition relation]
Description [Does the same as Mc_FsmEvaluateEHFormula, minus the hints.]
SeeAlso [Mc_FsmEvaluateEHFormula]
SideEffects []
Definition at line 2698 of file mcMc.c.
{
int i;
array_t *onionRings;
boolean useRings;
mdd_manager *mddManager;
mdd_t *mddOne;
mdd_t *iterate;
array_t *buchiFairness;
int nImgComps;
int nIterations;
boolean term_fixpoint = FALSE; /* different termination conditions */
boolean term_tautology = FALSE;
boolean term_early = FALSE;
/* Here's how the onionRingsArrayForDbg works. It is an array of
arrays of mdds. It is filled in anew for every pass of the
algorithm, that is for every /\_{c inC} EYE(Y S Y*c). There is
one entry for every fairness constraint, and this entry contains
the onionrings of the ES computation that corresponds to this
constraint. */
assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
*pOnionRingsArrayForDbg == NIL(array_t) ||
array_n(*pOnionRingsArrayForDbg) == 0);
useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
*pOnionRingsArrayForDbg != NIL(array_t));
nIterations = 0;
nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
onionRings = NIL(array_t);
mddManager = Fsm_FsmReadMddManager(modelFsm);
mddOne = mdd_one(mddManager);
/* If an overapproxiamtion of the greatest fixpoint is given, use it. */
if(overapprox != NIL(mdd_t)){
iterate = mdd_and(invariantMdd, overapprox, 1, 1);
} else {
iterate = mdd_dup(invariantMdd);
}
/* See if we need to enter the loop at all */
if( mdd_is_tautology(iterate, 0) ||
McCheckEarlyTerminationForOverapprox(earlyTermination,
iterate,
careStatesArray)){
mdd_free(mddOne);
if(fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0);
return(iterate);
}
/* read fairness constraints */
buchiFairness = array_alloc(mdd_t *, 0);
if(modelFairness != NIL(Fsm_Fairness_t)) {
if(!Fsm_FairnessTestIsBuchi(modelFairness)) {
(void)fprintf(vis_stdout,
"** mc error: non-Buechi fairness constraints not supported\n");
array_free(buchiFairness);
mdd_free(iterate);
mdd_free(mddOne);
if(fixpoint != NIL(boolean)) *fixpoint = FALSE;
return NIL(mdd_t);
}
else {
int j;
int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
for (j = 0 ; j < numBuchi; j++) {
mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
careStatesArray, dcLevel);
array_insert_last(mdd_t *, buchiFairness, tmpMdd);
}
}
}
else {
array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager));
}
/* GFP. If we know that the result is a subset of a set S, we can conjoin
the iterate with that set. We use this to converge faster. */
while (TRUE) {
mdd_t *newIterate; /* the new iterate */
nIterations++;
newIterate = mdd_dup(iterate);
/* for all fairness constraints */
for (i = 0 ; i < array_n(buchiFairness) ; i++) {
mdd_t *aMdd, *bMdd, *cMdd, *dMdd;
mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i);
if(useRings) {
onionRings = array_alloc(mdd_t *, 0);
array_insert_last(array_t *, *pOnionRingsArrayForDbg, onionRings);
}
aMdd = mdd_and(FiMdd, newIterate, 1, 1);
bMdd = Mc_FsmEvaluateESFormula(modelFsm, newIterate, aMdd, NIL(mdd_t),
mddOne, careStatesArray,
MC_NO_EARLY_TERMINATION, NIL(array_t),
Mc_None_c, onionRings, verbosity, dcLevel,
NIL(boolean));
mdd_free(aMdd);
cMdd = Mc_FsmEvaluateEYFormula(modelFsm, bMdd, mddOne, careStatesArray,
verbosity, dcLevel);
mdd_free(bMdd);
dMdd = mdd_and(newIterate, cMdd, 1, 1);
mdd_free(cMdd);
mdd_free(newIterate);
newIterate = dMdd;
/* invariants that hold here: newiterate <= iterate <= invariant. */
}/* for all fairness constraints */
/* termination */
term_tautology = mdd_is_tautology(newIterate, 0);
if(!term_tautology)
term_fixpoint = mdd_equal_mod_care_set_array(newIterate, iterate,
careStatesArray);
if(!term_tautology && !term_fixpoint)
term_early = McCheckEarlyTerminationForOverapprox(earlyTermination,
newIterate,
careStatesArray);
if(term_tautology || term_fixpoint || term_early){
mdd_free(iterate);
iterate = newIterate;
break; /* from the GFP loop */
}
/* update iterate */
mdd_free(iterate);
iterate = newIterate;
if(useRings){
mdd_array_array_free(*pOnionRingsArrayForDbg);
*pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
}
} /* while(true) for gfp */
/* Check if onionrings are OK */
if(verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
if(useRings){
for (i = 0 ; i < array_n(*pOnionRingsArrayForDbg); i++) {
int j;
mdd_t *Fi = array_fetch(mdd_t *, buchiFairness, i);
array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
i);
for (j = 0 ; j < array_n(onionRings); j++) {
mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
if(j == 0) {
if(!mdd_lequal_mod_care_set_array(ring, Fi, 1, 1,
careStatesArray)) {
fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
fprintf(vis_stderr,
"inner most ring not in Fi (fairness constraint).\n");
}
}
if(!mdd_lequal_mod_care_set_array(ring, invariantMdd, 1, 1,
careStatesArray)) {
fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
fprintf(vis_stderr, "An onion ring of last ES fails invariant\n");
}
} /* for all onionrings in array i */
} /* for all onionringarrays in onionringsarray */
}/* if useRings */
if(verbosity == McVerbosityMax_c) {
mdd_t *tmpMdd = careStatesArray ?
mdd_and_array(iterate, careStatesArray, 1, 1) : mdd_dup(iterate);
fprintf(vis_stdout,
"--There are %.0f care states satisfying EH formula\n",
mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd,
Fsm_FsmReadPresentStateVars(modelFsm)));
#ifdef DEBUG_MC
/* The following 2 lines are just for debug */
fprintf(vis_stdout, "EH satisfying minterms :\n");
(void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
mdd_free(tmpMdd);
} else {
fprintf(vis_stdout, "--There are %.0f states satisfying EH formula\n",
mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), iterate,
Fsm_FsmReadPresentStateVars(modelFsm)));
}
fprintf(vis_stdout, "--EH: %d iterations, %d image computations\n",
nIterations, Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
}
mdd_array_free(buchiFairness);
mdd_free(mddOne);
if(fixpoint != NIL(boolean))
*fixpoint = term_fixpoint || term_tautology;
return iterate;
} /* McEvaluateEHFormulaWithGivenTR */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McEvaluateESFormulaWithGivenTR | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | invariantMdd, | ||
| mdd_t * | sourceMdd, | ||
| mdd_t * | underapprox, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying E(invariant S target), given a transition relation]
Description [Does the same as Mc_FsmEvaluateESFormula, minus the hints.]
SeeAlso [Mc_FsmEvaluateESFormula]
SideEffects []
Definition at line 1846 of file mcMc.c.
{
mdd_t *aMdd;
mdd_t *bMdd;
mdd_t *cMdd;
mdd_t *resultMdd;
mdd_t *ringMdd;
int nImgComps;
boolean term_tautology = FALSE; /* different termination conditions */
boolean term_early = FALSE;
boolean term_fixpoint = FALSE;
nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
resultMdd = mdd_and(sourceMdd, fairStates, 1, 1);
if(underapprox != NIL(mdd_t)){
mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
mdd_free(resultMdd);
resultMdd = tmp;
}
ringMdd = mdd_dup(resultMdd);
if (onionRings) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
/* if Since is trivially satisfied, or
the early termination condition holds*/
{
bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
boolean trivial;
trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
1, 1, careStatesArray);
/* the lequal also takes care of the case where result = 1 */
if(trivial ||
McCheckEarlyTerminationForUnderapprox(earlyTermination,
resultMdd,
careStatesArray)){
bdd_free(fairInvariantStates);
bdd_free(ringMdd);
/* trivially satisfied means that the fixpoint is complete. If this
information is requested, give it. */
if(fixpoint != NIL(boolean))
*fixpoint = trivial;
return(resultMdd);
}
bdd_free(fairInvariantStates);
}
/* The LFP loop */
while (!term_fixpoint && !term_tautology && !term_early) {
/* If dclevel is maximal, ringbdd is between the frontier and the
reached set */
aMdd = Mc_FsmEvaluateEYFormula(modelFsm, ringMdd, fairStates,
careStatesArray, verbosity, dcLevel);
mdd_free(ringMdd);
bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
mdd_free(aMdd);
cMdd = mdd_or(resultMdd, bMdd, 1, 1);
mdd_free(bMdd);
/* Can we stop? The tautology condition can be weakened to
cMdd <= careStatesArray */
term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
careStatesArray);
if(!term_fixpoint)
term_tautology = mdd_is_tautology(cMdd, 1);
if(!term_fixpoint && !term_tautology)
term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination,
cMdd,
careStatesArray);
/* Print some debug info, and set ringmdd */
if (dcLevel >= McDcLevelRchFrontier_c) {
mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
ringMdd = bdd_between(tmpMdd, cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout,
"--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
}
mdd_free(tmpMdd);
}
else {
ringMdd = mdd_dup(cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd));
}
}
mdd_free(resultMdd);
resultMdd = cMdd;
/* add onion ring unless fixpoint reached */
if (!term_fixpoint && onionRings != NIL(array_t)) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
} /* while(!termination) for LFP */
mdd_free(ringMdd);
/* Print some debug info */
if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
static int refCount=0;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
if (verbosity == McVerbosityMax_c) {
mdd_t *tmpMdd = careStatesArray ?
mdd_and_array(resultMdd, careStatesArray, 1, 1) :
mdd_dup(resultMdd);
fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount,
mdd_size(resultMdd));
fprintf(vis_stdout,
"--There are %.0f care states satisfying ES formula\n",
mdd_count_onset(mddMgr, tmpMdd, psVars));
#ifdef DEBUG_MC
/* The following 2 lines are just for debug */
fprintf(vis_stdout, "ES satisfying minterms :\n");
(void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
mdd_free(tmpMdd);
} else {
fprintf(vis_stdout,
"--There are %.0f states satisfying ES formula\n",
mdd_count_onset(mddMgr, resultMdd, psVars));
}
fprintf(vis_stdout, "--ES: %d image computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
}
if(fixpoint != NIL(boolean))
*fixpoint = term_fixpoint || term_tautology;
return resultMdd;
} /* McEvaluateESFormulaWithGivenTR */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McEvaluateESFormulaWithGivenTRFAFW | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | invariantMdd, | ||
| mdd_t * | sourceMdd, | ||
| mdd_t * | underapprox, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint, | ||
| mdd_t * | Swin | ||
| ) |
Function********************************************************************
Synopsis []
Description []
SeeAlso []
SideEffects []
Definition at line 2194 of file mcMc.c.
{
mdd_t *aMdd;
mdd_t *bMdd;
mdd_t *cMdd;
mdd_t *resultMdd;
mdd_t *ringMdd;
Img_ImageInfo_t *imageInfo;
int nImgComps;
boolean term_tautology = FALSE; /* different termination conditions */
boolean term_early = FALSE;
boolean term_fixpoint = FALSE;
nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
resultMdd = mdd_and(sourceMdd, fairStates, 1, 1);
if(underapprox != NIL(mdd_t)){
mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
mdd_free(resultMdd);
resultMdd = tmp;
}
ringMdd = mdd_dup(resultMdd);
if (onionRings) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
/* if Since is trivially satisfied, or
the early termination condition holds*/
{
bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
boolean trivial;
trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
1, 1, careStatesArray);
/* the lequal also takes care of the case where result = 1 */
if(trivial ||
McCheckEarlyTerminationForUnderapprox(earlyTermination,
resultMdd,
careStatesArray)){
bdd_free(fairInvariantStates);
bdd_free(ringMdd);
/* trivially satisfied means that the fixpoint is complete. If this
information is requested, give it. */
if(fixpoint != NIL(boolean))
*fixpoint = trivial;
return(resultMdd);
}
bdd_free(fairInvariantStates);
}
imageInfo = Fsm_FsmReadOrCreateImageInfoPrunedFAFW(modelFsm, Swin, 0, 1);
/* The LFP loop */
while (!term_fixpoint && !term_tautology && !term_early) {
/* If dclevel is maximal, ringbdd is between the frontier and the
reached set */
aMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
ringMdd, ringMdd, careStatesArray);
mdd_free(ringMdd);
bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
mdd_free(aMdd);
cMdd = mdd_or(resultMdd, bMdd, 1, 1);
mdd_free(bMdd);
/* Can we stop? The tautology condition can be weakened to
cMdd <= careStatesArray */
term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
careStatesArray);
if(!term_fixpoint)
term_tautology = mdd_is_tautology(cMdd, 1);
if(!term_fixpoint && !term_tautology)
term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination,
cMdd,
careStatesArray);
/* Print some debug info, and set ringmdd */
if (dcLevel >= McDcLevelRchFrontier_c) {
mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
ringMdd = bdd_between(tmpMdd, cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout,
"--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
}
mdd_free(tmpMdd);
}
else {
ringMdd = mdd_dup(cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd));
}
}
mdd_free(resultMdd);
resultMdd = cMdd;
/* add onion ring unless fixpoint reached */
if (!term_fixpoint && onionRings != NIL(array_t)) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
} /* while(!termination) for LFP */
/* Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c); */
Img_ImageInfoFreeFAFW(imageInfo);
Img_ImageInfoFree(imageInfo);
mdd_free(ringMdd);
/* Print some debug info */
if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
static int refCount=0;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
if (verbosity == McVerbosityMax_c) {
mdd_t *tmpMdd = careStatesArray ?
mdd_and_array(resultMdd, careStatesArray, 1, 1) :
mdd_dup(resultMdd);
fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount,
mdd_size(resultMdd));
fprintf(vis_stdout,
"--There are %.0f care states satisfying ES formula\n",
mdd_count_onset(mddMgr, tmpMdd, psVars));
#ifdef DEBUG_MC
/* The following 2 lines are just for debug */
fprintf(vis_stdout, "ES satisfying minterms :\n");
(void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
mdd_free(tmpMdd);
} else {
fprintf(vis_stdout,
"--There are %.0f states satisfying ES formula\n",
mdd_count_onset(mddMgr, resultMdd, psVars));
}
fprintf(vis_stdout, "--ES: %d image computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
}
if(fixpoint != NIL(boolean))
*fixpoint = term_fixpoint || term_tautology;
return resultMdd;
} /* McEvaluateESFormulaWithGivenTR */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McEvaluateESFormulaWithGivenTRWithTarget | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | invariantMdd, | ||
| mdd_t * | sourceMdd, | ||
| mdd_t * | targetMdd, | ||
| mdd_t * | underapprox, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint | ||
| ) |
Function********************************************************************
Synopsis []
Description []
SeeAlso []
SideEffects []
Definition at line 2013 of file mcMc.c.
{
mdd_t *aMdd;
mdd_t *bMdd;
mdd_t *cMdd;
mdd_t *resultMdd;
mdd_t *ringMdd;
mdd_t *zeroMdd;
int nImgComps;
boolean term_tautology = FALSE; /* different termination conditions */
boolean term_early = FALSE;
boolean term_fixpoint = FALSE;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
resultMdd = mdd_and(sourceMdd, fairStates, 1, 1);
if(underapprox != NIL(mdd_t)){
mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
mdd_free(resultMdd);
resultMdd = tmp;
}
ringMdd = mdd_dup(resultMdd);
zeroMdd = mdd_zero(mddMgr);
if (onionRings) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
/* if Since is trivially satisfied, or
the early termination condition holds*/
{
bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
boolean trivial;
trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
1, 1, careStatesArray);
/* the lequal also takes care of the case where result = 1 */
if(trivial ||
McCheckEarlyTerminationForUnderapprox(earlyTermination,
resultMdd,
careStatesArray)){
bdd_free(fairInvariantStates);
bdd_free(ringMdd);
/* trivially satisfied means that the fixpoint is complete. If this
information is requested, give it. */
if(fixpoint != NIL(boolean))
*fixpoint = trivial;
return(resultMdd);
}
bdd_free(fairInvariantStates);
}
/* The LFP loop */
while (!term_fixpoint && !term_tautology && !term_early) {
/* If dclevel is maximal, ringbdd is between the frontier and the
reached set */
aMdd = Mc_FsmEvaluateEYFormula(modelFsm, ringMdd, fairStates,
careStatesArray, verbosity, dcLevel);
mdd_free(ringMdd);
bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
mdd_free(aMdd);
cMdd = mdd_or(resultMdd, bMdd, 1, 1);
mdd_free(bMdd);
/* Can we stop? The tautology condition can be weakened to
cMdd <= careStatesArray */
term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
careStatesArray);
if(!term_fixpoint)
term_tautology = mdd_is_tautology(cMdd, 1);
if(!term_fixpoint && !term_tautology)
term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination,
cMdd,
careStatesArray);
/* Print some debug info, and set ringmdd */
if (dcLevel >= McDcLevelRchFrontier_c) {
mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
ringMdd = bdd_between(tmpMdd, cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout,
"--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
}
mdd_free(tmpMdd);
}
else {
ringMdd = mdd_dup(cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd));
}
}
mdd_free(resultMdd);
resultMdd = cMdd;
aMdd = mdd_and(resultMdd, targetMdd, 1, 1);
if(!mdd_equal(aMdd, zeroMdd)) {
array_insert_last(mdd_t *, onionRings, mdd_dup(targetMdd));
mdd_free(aMdd);
break;
}
mdd_free(aMdd);
/* add onion ring unless fixpoint reached */
if (!term_fixpoint && onionRings != NIL(array_t)) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
} /* while(!termination) for LFP */
mdd_free(ringMdd);
/* Print some debug info */
if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
static int refCount=0;
array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
if (verbosity == McVerbosityMax_c) {
mdd_t *tmpMdd = careStatesArray ?
mdd_and_array(resultMdd, careStatesArray, 1, 1) :
mdd_dup(resultMdd);
fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount,
mdd_size(resultMdd));
fprintf(vis_stdout,
"--There are %.0f care states satisfying ES formula\n",
mdd_count_onset(mddMgr, tmpMdd, psVars));
#ifdef DEBUG_MC
/* The following 2 lines are just for debug */
fprintf(vis_stdout, "ES satisfying minterms :\n");
(void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
mdd_free(tmpMdd);
} else {
fprintf(vis_stdout,
"--There are %.0f states satisfying ES formula\n",
mdd_count_onset(mddMgr, resultMdd, psVars));
}
fprintf(vis_stdout, "--ES: %d image computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
}
mdd_free(zeroMdd);
if(fixpoint != NIL(boolean))
*fixpoint = term_fixpoint || term_tautology;
return resultMdd;
} /* McEvaluateESFormulaWithGivenTR */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McEvaluateEUFormulaWithGivenTR | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | invariantMdd, | ||
| mdd_t * | targetMdd, | ||
| mdd_t * | underapprox, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| boolean * | fixpoint | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying E(invariant U target), given a transition relation]
Description [Does the same as Mc_FsmEvaluateEUFormula, minus the hints.]
SeeAlso [Mc_FsmEvaluateEUFormula]
SideEffects []
Definition at line 1678 of file mcMc.c.
{
mdd_t *aMdd;
mdd_t *bMdd;
mdd_t *cMdd;
mdd_t *resultMdd;
mdd_t *ringMdd;
int nPreComps;
boolean term_tautology = FALSE; /* different termination conditions */
boolean term_early = FALSE;
boolean term_fixpoint = FALSE;
nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
resultMdd = mdd_and(targetMdd, fairStates, 1, 1);
if(underapprox != NIL(mdd_t)){
mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
mdd_free(resultMdd);
resultMdd = tmp;
}
ringMdd = mdd_dup(resultMdd);
if (onionRings) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
/* if until is trivially satisfied, or
the early termination condition holds*/
{
bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
boolean trivial;
trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
1, 1, careStatesArray);
/* the lequal also takes care of the case where result = 1 */
if(trivial ||
McCheckEarlyTerminationForUnderapprox(earlyTermination,
resultMdd,
careStatesArray)){
bdd_free(fairInvariantStates);
bdd_free(ringMdd);
/* trivially satisfied means that the fixpoint is complete. If this
information is requested, give it. */
if(fixpoint != NIL(boolean))
*fixpoint = trivial;
return(resultMdd);
}
bdd_free(fairInvariantStates);
}
/* The LFP loop */
while (!term_fixpoint && !term_tautology && !term_early) {
/* If dclevel is maximal, ringbdd is between the frontier and the
reached set */
aMdd = Mc_FsmEvaluateEXFormula(modelFsm, ringMdd, fairStates,
careStatesArray, verbosity, dcLevel);
mdd_free(ringMdd);
bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
mdd_free(aMdd);
cMdd = mdd_or(resultMdd, bMdd, 1, 1);
mdd_free(bMdd);
/* Can we stop? The tautology condition can be weakened to
cMdd <= careStatesArray */
term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
careStatesArray);
if(!term_fixpoint)
term_tautology = mdd_is_tautology(cMdd, 1);
if(!term_fixpoint && !term_tautology)
term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination,
cMdd,
careStatesArray);
/* Print some debug info, and set ringmdd */
if (dcLevel >= McDcLevelRchFrontier_c) {
mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
ringMdd = bdd_between(tmpMdd, cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout,
"--EU |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
}
mdd_free(tmpMdd);
}
else {
ringMdd = mdd_dup(cMdd);
if (verbosity == McVerbosityMax_c) {
fprintf(vis_stdout, "-- EU |ringMdd| = %d\n", mdd_size(ringMdd));
}
}
mdd_free(resultMdd);
resultMdd = cMdd;
/* add onion ring unless fixpoint reached */
if (!term_fixpoint && onionRings != NIL(array_t)) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
} /* while(!termination) for LFP */
mdd_free(ringMdd);
/* Print some debug info */
if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
static int refCount=0;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
if (verbosity == McVerbosityMax_c) {
mdd_t *tmpMdd = careStatesArray ?
mdd_and_array(resultMdd, careStatesArray, 1, 1) :
mdd_dup(resultMdd);
fprintf(vis_stdout, "--EU called %d (bdd_size - %d)\n", ++refCount,
mdd_size(resultMdd));
fprintf(vis_stdout,
"--There are %.0f care states satisfying EU formula\n",
mdd_count_onset(mddMgr, tmpMdd, psVars));
#ifdef DEBUG_MC
/* The following 2 lines are just for debug */
fprintf(vis_stdout, "EU satisfying minterms :\n");
(void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
mdd_free(tmpMdd);
} else {
fprintf(vis_stdout,
"--There are %.0f states satisfying EU formula\n",
mdd_count_onset(mddMgr, resultMdd, psVars));
}
fprintf(vis_stdout, "--EU: %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
}
if(fixpoint != NIL(boolean))
*fixpoint = term_fixpoint || term_tautology;
return resultMdd;
} /* McEvaluateEUFormulaWithGivenTR */
Here is the call graph for this function:
Here is the caller graph for this function:
| void McFormulaFreeDebugData | ( | Ctlp_Formula_t * | formula | ) |
Function********************************************************************
Synopsis [Frees memory stored at formula corresponding to debug data.]
Description [Frees memory stored at formula corresponding to debug data. It is assumed that the debug data is valid. It is an error to call this function on a formula which is not of the type EG or EU.]
SideEffects []
Definition at line 2925 of file mcMc.c.
{
Ctlp_FormulaType type = Ctlp_FormulaReadType(formula);
array_t *dbgArray = (array_t *) Ctlp_FormulaReadDebugData(formula);
if (type == Ctlp_EU_c || type == Ctlp_FwdU_c) {
mdd_array_free(dbgArray);
}
else if (type == Ctlp_EG_c || type == Ctlp_FwdG_c || type == Ctlp_EH_c)
mdd_array_array_free(dbgArray);
else {
fail("Error - called on non EG/EU formula.\n");
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * McForwardReachable | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | targetMdd, | ||
| mdd_t * | invariantMdd, | ||
| mdd_t * | fairStates, | ||
| array_t * | careStatesArray, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) | [static] |
Function********************************************************************
Synopsis [Reachable(p,q) = FwdUntil(p,q) ^ q]
Description [Reachable(p,q) = FwdUntil(p,q) ^ q. This Reachable operation is described in the paper "CTL Model Checking Based on Forward State Traversal" by H. Iwashita et al.]
SideEffects []
Definition at line 4066 of file mcMc.c.
{
mdd_t *resultMdd, *fuMdd;
/* When McForwardReachable is called by Mc_FsmEvaluateFwdEHFormula
* with no fairness constraints, this test saves one image
* computation. */
if (mdd_is_tautology(fairStates, 1) &&
mdd_lequal_mod_care_set_array(invariantMdd, targetMdd,
1, 1, careStatesArray)) {
resultMdd = mdd_dup(invariantMdd);
if (onionRings) {
array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
}
} else {
fuMdd = Mc_FsmEvaluateFwdUFormula(modelFsm, targetMdd, invariantMdd,
fairStates, careStatesArray, onionRings,
verbosity, dcLevel);
resultMdd = mdd_and(fuMdd, invariantMdd, 1, 1);
mdd_free(fuMdd);
}
/* Updates onionRings not to have warning message in
* Mc_FsmEvaluateFwdEHFormula since Reachable(p,q) = FwdUntil(p,q) ^ q.
*/
if (onionRings) {
int i;
mdd_t *ring, *tmp;
for (i = 0 ; i < array_n(onionRings); i++) {
tmp = array_fetch(mdd_t *, onionRings, i);
ring = mdd_and(tmp, invariantMdd, 1, 1);
mdd_free(tmp);
array_insert(mdd_t *, onionRings, i, ring);
}
}
return(resultMdd);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McModelCheckAtomicFormula | ( | Fsm_Fsm_t * | modelFsm, |
| Ctlp_Formula_t * | ctlFormula | ||
| ) |
Function********************************************************************
Synopsis [Find Mdd for states satisfying Atomic Formula.]
Description [An atomic formula defines a set of states in the following way: it states a designated ``net'' (specified by the full path name) takes a certain value. The net should be purely a function of latches; as a result an evaluation of the net yields a set of states.]
SideEffects []
Definition at line 3027 of file mcMc.c.
{
mdd_t * resultMdd;
mdd_t *tmpMdd;
Ntk_Network_t *network = Fsm_FsmReadNetwork(modelFsm);
char *nodeNameString = Ctlp_FormulaReadVariableName(ctlFormula);
char *nodeValueString = Ctlp_FormulaReadValueName(ctlFormula);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
Var_Variable_t *nodeVar;
int nodeValue;
graph_t *modelPartition;
vertex_t *partitionVertex;
Mvf_Function_t *MVF;
nodeVar = Ntk_NodeReadVariable(node);
if (Var_VariableTestIsSymbolic(nodeVar)) {
nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
}
else {
nodeValue = atoi(nodeValueString);
}
#if 0
modelPartition = Part_NetworkReadPartition(network);
#endif
modelPartition = Fsm_FsmReadPartition(modelFsm);
if (!(partitionVertex = Part_PartitionFindVertexByName(modelPartition,
nodeNameString))) {
lsGen tmpGen;
Ntk_Node_t *tmpNode;
array_t *mvfArray;
array_t *tmpRoots = array_alloc(Ntk_Node_t *, 0);
st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
array_insert_last(Ntk_Node_t *, tmpRoots, node);
Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED);
}
mvfArray = Ntm_NetworkBuildMvfs(network, tmpRoots, tmpLeaves,
NIL(mdd_t));
MVF = array_fetch(Mvf_Function_t *, mvfArray, 0);
array_free(tmpRoots);
st_free_table(tmpLeaves);
array_free(mvfArray);
tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
resultMdd = mdd_dup(tmpMdd);
Mvf_FunctionFree(MVF);
}
else {
MVF = Part_VertexReadFunction(partitionVertex);
tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
resultMdd = mdd_dup(tmpMdd);
}
if (Part_PartitionReadMethod(modelPartition) == Part_Frontier_c &&
Ntk_NodeTestIsCombOutput(node)) {
array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
array_t *supportList;
st_table *supportTable = st_init_table(st_numcmp, st_numhash);
int i, j;
int existIntermediateVars;
int mddId;
Mvf_Function_t *mvf;
vertex_t *vertex;
array_t *varBddRelationArray, *varArray;
mdd_t *iv, *ivMdd, *relation;
for (i = 0; i < array_n(psVars); i++) {
mddId = array_fetch(int, psVars, i);
st_insert(supportTable, (char *)(long)mddId, NULL);
}
existIntermediateVars = 1;
while (existIntermediateVars) {
existIntermediateVars = 0;
supportList = mdd_get_support(mgr, resultMdd);
for (i = 0; i < array_n(supportList); i++) {
mddId = array_fetch(int, supportList, i);
if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) {
vertex = Part_PartitionFindVertexByMddId(modelPartition, mddId);
mvf = Part_VertexReadFunction(vertex);
varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mgr, mddId, mvf);
varArray = mdd_id_to_bdd_array(mgr, mddId);
assert(array_n(varBddRelationArray) == array_n(varArray));
for (j = 0; j < array_n(varBddRelationArray); j++) {
iv = array_fetch(mdd_t *, varArray, j);
relation = array_fetch(mdd_t *, varBddRelationArray, j);
ivMdd = bdd_cofactor(relation, iv);
mdd_free(relation);
tmpMdd = resultMdd;
resultMdd = bdd_compose(resultMdd, iv, ivMdd);
mdd_free(tmpMdd);
mdd_free(iv);
mdd_free(ivMdd);
}
array_free(varBddRelationArray);
array_free(varArray);
existIntermediateVars = 1;
}
}
array_free(supportList);
}
st_free_table(supportTable);
}
return resultMdd;
} /* McModelCheckAtomicFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean McPrintPassFail | ( | mdd_manager * | mddMgr, |
| Fsm_Fsm_t * | modelFsm, | ||
| Mc_FwdBwdAnalysis | traversalDirection, | ||
| Ctlp_Formula_t * | ctlFormula, | ||
| mdd_t * | ctlFormulaStates, | ||
| mdd_t * | modelInitialStates, | ||
| array_t * | modelCareStatesArray, | ||
| McOptions_t * | options, | ||
| Mc_VerbosityLevel | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Prints whether model checking passed or failed]
Description [Prints whether model checking passed or failed, and if requested, a debug trace.]
SideEffects []
Definition at line 2985 of file mcMc.c.
{
if (mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1)) {
fprintf(vis_stdout, "# MC: formula passed --- ");
Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula));
fprintf(vis_stdout, "\n");
return TRUE;
}
else {
fprintf(vis_stdout, "# MC: formula failed --- ");
Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula));
fprintf(vis_stdout, "\n");
if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) {
McFsmDebugFormula(options, ctlFormula,modelFsm, modelCareStatesArray);
}
return FALSE;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* SortFormulasByFsm | ( | Fsm_Fsm_t * | totalFsm, |
| array_t * | invarFormulaArray, | ||
| array_t * | fsmArray, | ||
| McOptions_t * | options | ||
| ) |
Function********************************************************************
Synopsis [Sort formulae by fsm]
Description [Sort formulae by fsm. This creates an array of array of formulae. Each element of the outer array corresponds to an fsm reduced w.r.t the element (array of formulae). Both the array of formulae and the reduced fsms are returned. If there is no reduction, the reduced fsm is set to the totalFsm. While freeing the reduced fsms in the fsmArray, if the reduced fsm is set to total fsm, DO NOT free. ]
SideEffects [fsmArray is populated with reduced fsms.]
Definition at line 3315 of file mcMc.c.
{
array_t *resultArray;
array_t *formulaArray;
array_t *tempArray;
int i, j, found;
Ctlp_Formula_t *formula;
Ntk_Network_t *network = Fsm_FsmReadNetwork(totalFsm);
Fsm_Fsm_t *reducedFsm, *fsm;
int reducedFsmPos = -1;
if (invarFormulaArray == NIL(array_t)) return invarFormulaArray;
if (array_n(invarFormulaArray) == 0) return NIL(array_t);
tempArray = array_alloc(array_t *, 0);
/* do a semantic check and a quantifier check */
arrayForEachItem (Ctlp_Formula_t *, invarFormulaArray, i, formula) {
if (!Mc_FormulaStaticSemanticCheckOnNetwork(formula, network, FALSE)){
(void) fprintf(vis_stderr, "** inv error: error in parsing Atomic Formula:\n%s\n", error_string());
error_init();
Ctlp_FormulaFree(formula);
continue;
} else {
if (Ctlp_FormulaTestIsQuantifierFree(formula) == FALSE) {
(void) fprintf(vis_stderr, "** inv error: invariant formula refers to path quantifiers\n");
Ctlp_FormulaFree(formula);
continue;
}
}
array_insert_last(Ctlp_Formula_t *, tempArray, formula);
}
if (array_n(tempArray) == 0) {
array_free(tempArray);
return NIL(array_t);
}
/* if no -r option, return the original array */
resultArray = array_alloc(array_t *, 0);
if (McOptionsReadReduceFsm(options) == FALSE) {
array_insert_last(array_t *, resultArray, tempArray);
reducedFsm = McConstructReducedFsm(network, tempArray);
if (reducedFsm != NIL(Fsm_Fsm_t)) {
array_insert_last(Fsm_Fsm_t *, fsmArray, reducedFsm);
} else {
array_insert_last(Fsm_Fsm_t *, fsmArray, totalFsm);
}
return resultArray;
}
/* We want to minimize per formula only when "-r" option is not specified */
arrayForEachItem (Ctlp_Formula_t *, tempArray, i, formula) {
/* Create reduced fsm */
formulaArray = array_alloc(Ctlp_Formula_t *, 0);
array_insert_last(Ctlp_Formula_t *, formulaArray, formula);
reducedFsm = McConstructReducedFsm(network, formulaArray);
if (reducedFsm == NIL(Fsm_Fsm_t)) {
/* no reduction */
reducedFsm = totalFsm;
}
/* Check if fsm already created */
found = 0;
for (j = 0; j < array_n(fsmArray); j++) {
fsm = array_fetch (Fsm_Fsm_t *, fsmArray, j);
found = Fsm_FsmCheckSameSubFsmInTotalFsm(totalFsm, reducedFsm, fsm);
if (found) break;
}
/* If found, add to the existing list. Else add a new reduced fsm */
if (found) {
if (reducedFsm != totalFsm) Fsm_FsmFree(reducedFsm);
array_free(formulaArray);
formulaArray = array_fetch(array_t *, resultArray, j);
array_insert_last(Ctlp_Formula_t *, formulaArray, formula);
} else {
array_insert_last(Fsm_Fsm_t *, fsmArray, reducedFsm);
array_insert_last(array_t *, resultArray, formulaArray);
if (reducedFsm == totalFsm) reducedFsmPos = array_n(fsmArray)-1;
}
}
array_free(tempArray);
/* swap the last reduced fsm with the total fsm. */
if ((reducedFsmPos != -1) && (reducedFsmPos != array_n(fsmArray)-1)) {
array_t *totalFsmFormulaArray;
assert(array_n(fsmArray) == array_n(resultArray));
fsm = array_fetch(Fsm_Fsm_t *, fsmArray, array_n(fsmArray)-1);
array_insert(Fsm_Fsm_t *, fsmArray, reducedFsmPos, fsm);
array_insert(Fsm_Fsm_t *, fsmArray, array_n(fsmArray)-1, totalFsm);
formulaArray = array_fetch(array_t *, resultArray, array_n(resultArray)-1);
totalFsmFormulaArray = array_fetch(array_t *, resultArray, reducedFsmPos);
array_insert(array_t *, resultArray, reducedFsmPos, formulaArray);
array_insert(array_t *, resultArray, array_n(resultArray)-1, totalFsmFormulaArray);
}
return resultArray;
} /* end of SortFormulasByFsm */
Here is the call graph for this function:
Here is the caller graph for this function:
| int TestInvariantsInTotalFsm | ( | Fsm_Fsm_t * | totalFsm, |
| array_t * | invarStatesArray, | ||
| int | shellFlag | ||
| ) |
Function********************************************************************
Synopsis [Test if an invariant is violated in the current reachable set of the given FSM.]
Description [Test if an invariant is violated in the current reachable set of the given FSM. Returns FALSE if an invariant is violated and TRUE is no invariant is violated.]
SideEffects []
Definition at line 3431 of file mcMc.c.
{
int i;
mdd_t *invariant;
mdd_t *reachableStates;
boolean upToDate = FALSE; /* don't care initialization */
if (shellFlag) {
upToDate = Fsm_FsmReachabilityOnionRingsStates(totalFsm, &reachableStates);
} else {
reachableStates = Fsm_FsmReadCurrentReachableStates(totalFsm);
}
if (reachableStates == NIL(mdd_t)) return TRUE;
if (mdd_is_tautology(reachableStates, 0)) return TRUE;
arrayForEachItem(mdd_t *, invarStatesArray, i, invariant) {
if (invariant == NIL(mdd_t)) continue;
if (!mdd_lequal(reachableStates, invariant, 1, 1)) {
if (shellFlag) mdd_free(reachableStates);
return FALSE;
}
}
if (shellFlag) mdd_free(reachableStates);
if ((shellFlag && !upToDate) ||
(Fsm_FsmReadReachabilityApproxComputationStatus(totalFsm) ==
Fsm_Rch_Under_c))
return TRUE;
else
return FALSE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: mcMc.c,v 1.257 2007/04/17 00:01:22 sohail Exp $" [static] |
CFile***********************************************************************
FileName [mcMc.c]
PackageName [mc]
Synopsis [Fair CTL model checker.]
Description [This file contains the functions for both backward and forward model checking. Forward model checking is based on Iwashta's ICCAD96 paper. Future tense CTLs are automatically converted to past tense ones as much as possible in forward model checking.]
Author [Adnan Aziz, Tom Shiple, Rajeev Ranjan, In-Ho Moon, Roderick Bloem]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
