#include "ctlpInt.h"#include "mcInt.h"
Include dependency graph for mcVacuum.c:
Go to the source code of this file.
Functions | |
| static void | EvaluateFormulaThoroughVacuity (Fsm_Fsm_t *fsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRing, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates) |
| static void | EvaluateFormulaWactlVacuity (Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, mdd_t *modelInitialStates, McOptions_t *options) |
| static void | PrintVacuousBottom (mdd_t *modelInitialStates, Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, Mc_FwdBwdAnalysis traversalDirection, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity) |
| static void | PrintVacuous (mdd_t *modelInitialStates, Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, Mc_FwdBwdAnalysis traversalDirection, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity) |
| static void | ModelcheckAndVacuity (Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Ctlp_Approx_t TRMinimization, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates) |
| static void | CreateImportantWitness (Ctlp_Formula_t *OldctlFormula, Ctlp_Formula_t *ctlFormula, int i) |
| static void | CreateImportantCounterexample (Ctlp_Formula_t *OldctlFormula, Ctlp_Formula_t *ctlFormula, int i) |
| static array_t * | McMddArrayArrayDup (array_t *arrayBddArray) |
| static void | match_top (Ctlp_Formula_t *ctlFormula, array_t *mddArray, array_t *matchfound, array_t *matchelement) |
| static void | match_bot (Ctlp_Formula_t *ctlFormula, array_t *mddArray, array_t *matchfound, array_t *matchelement) |
| static array_t * | GenerateOnionRings (array_t *TempOnionRings, array_t *onionRings) |
| static void | FormulaFreeDebugDataVac (Ctlp_Formula_t *formula) |
| void | McVacuityDetection (Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, mdd_t *modelInitialStates, McOptions_t *options) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mcVacuum.c,v 1.1 2005/05/13 05:54:05 fabio Exp $" |
Function Documentation
| static void CreateImportantCounterexample | ( | Ctlp_Formula_t * | OldctlFormula, |
| Ctlp_Formula_t * | ctlFormula, | ||
| int | i | ||
| ) | [static] |
Function********************************************************************
Synopsis [Annotates formula with satisfying sets of i-th replacement.]
Description [This function is applied to vacuously failing properties to generate intersting counterexamples.]
SideEffects []
SeeAlso [CreateImportantWitness]
Definition at line 2136 of file mcVacuum.c.
{
Ctlp_Formula_t *rightChild, *leftChild, *OldrightChild, *OldleftChild;
int number_left_top;
array_t *onionRings = NIL(array_t); /* array of mdd_t */
array_t *arrayOfOnionRings = NIL(array_t);
Ctlp_FormulaType formulaType;
formulaType = Ctlp_FormulaReadType(ctlFormula);
rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
OldrightChild = Ctlp_FormulaReadRightChild(OldctlFormula);
OldleftChild = Ctlp_FormulaReadLeftChild(OldctlFormula);
if(leftChild)
number_left_top = array_n(OldleftChild->Topstates);
else
number_left_top = -1; /* don't care */
switch (formulaType) {
case Ctlp_EU_c:
if(ctlFormula->states != NIL(mdd_t))
mdd_free(ctlFormula->states);
ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i));
onionRings = mdd_array_duplicate(array_fetch(array_t*,OldctlFormula->TopOnionRings,i));
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings,
McFormulaFreeDebugData);
assert(leftChild != NULL && rightChild != NULL);
if(i<number_left_top){
CreateImportantCounterexample(OldleftChild,leftChild,i);
}
else{
CreateImportantCounterexample(OldleftChild,leftChild,0);
}
if(i<number_left_top ){
CreateImportantCounterexample(OldrightChild,rightChild,0);
}
else {
CreateImportantCounterexample(OldrightChild,rightChild,i -
number_left_top + 1);
}
break;
case Ctlp_EG_c:
if(ctlFormula->states != NIL(mdd_t))
mdd_free(ctlFormula->states);
ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i));
arrayOfOnionRings = McMddArrayArrayDup(array_fetch(array_t* ,OldctlFormula->TopOnionRings,i));
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
McFormulaFreeDebugData);
CreateImportantCounterexample(OldleftChild,leftChild,i);
break;
case Ctlp_AX_c:
case Ctlp_AG_c:
case Ctlp_AF_c:
case Ctlp_AU_c:
case Ctlp_EX_c:
case Ctlp_EF_c:
case Ctlp_OR_c:
case Ctlp_AND_c:
case Ctlp_NOT_c:
case Ctlp_THEN_c:
case Ctlp_XOR_c:
case Ctlp_EQ_c:
if(ctlFormula->states != NIL(mdd_t))
mdd_free(ctlFormula->states);
ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i));
if(leftChild){
if(i<number_left_top){
CreateImportantCounterexample(OldleftChild,leftChild,i);
}
else {
CreateImportantCounterexample(OldleftChild,leftChild,0);
}
}
if(rightChild){
if(i<number_left_top ){
CreateImportantCounterexample(OldrightChild,rightChild,0);
}
else{
CreateImportantCounterexample(OldrightChild,rightChild,i -
number_left_top + 1);
}
}
break;
case Ctlp_ID_c:
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
case Ctlp_Init_c:
if(ctlFormula->states != NIL(mdd_t))
mdd_free(ctlFormula->states);
ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i));
#if 0
fprintf(vis_stdout,"Attaching bdd for ID,TRUE %d",i);
bdd_print(ctlFormula->states);
#endif
break;
default:
break;
}
} /* CreateImportantCounterexample */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void CreateImportantWitness | ( | Ctlp_Formula_t * | OldctlFormula, |
| Ctlp_Formula_t * | ctlFormula, | ||
| int | i | ||
| ) | [static] |
Function********************************************************************
Synopsis [Annotates formula with satisfying sets of i-th replacement.]
Description [This function is applied to vacuously passing properties to generate intersting witnesses.]
SideEffects []
SeeAlso [CreateImportantCounterexample]
Definition at line 2003 of file mcVacuum.c.
{
Ctlp_Formula_t *rightChild, *leftChild,*OldrightChild, *OldleftChild;
int number_left_bot;
array_t *onionRings = NIL(array_t); /* array of mdd_t */
array_t *arrayOfOnionRings = NIL(array_t);
Ctlp_FormulaType formulaType;
formulaType = Ctlp_FormulaReadType(ctlFormula);
rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
OldrightChild = Ctlp_FormulaReadRightChild(OldctlFormula);
OldleftChild = Ctlp_FormulaReadLeftChild(OldctlFormula);
if(leftChild)
number_left_bot = array_n(OldleftChild->Bottomstates);
else
number_left_bot = -1; /* don't care */
switch (formulaType) {
case Ctlp_EU_c:
if(ctlFormula->states != NIL(mdd_t))
mdd_free(ctlFormula->states);
ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i));
#if 0
fprintf(vis_stdout,"Attaching bdd for EU %d",i);
bdd_print(ctlFormula->states);
mdd_array_free(array_fetch(array_t*,OldctlFormula->BotOnionRings,i));
#endif
onionRings = mdd_array_duplicate(array_fetch(array_t*,OldctlFormula->BotOnionRings,i));
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings,
McFormulaFreeDebugData);
assert(leftChild != NULL && rightChild != NULL);
if(i<number_left_bot){
CreateImportantWitness(OldleftChild,leftChild,i);
}
else{
CreateImportantWitness(OldleftChild,leftChild,0);
}
if(i<number_left_bot ){
CreateImportantWitness(OldrightChild,rightChild,0);
}
else {
CreateImportantWitness(OldrightChild,rightChild,i - number_left_bot + 1);
}
break;
case Ctlp_EG_c:
if(ctlFormula->states != NIL(mdd_t))
mdd_free(ctlFormula->states);
ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i));
#if 0
fprintf(vis_stdout,"Attaching bdd for EG %d",i);
bdd_print(ctlFormula->states);
mdd_array_free(array_fetch(array_t*,OldctlFormula->BotOnionRings,i));
#endif
arrayOfOnionRings = McMddArrayArrayDup(array_fetch(array_t* ,OldctlFormula->BotOnionRings,i));
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
McFormulaFreeDebugData);
CreateImportantWitness(OldleftChild,leftChild,i);
break;
case Ctlp_AX_c:
case Ctlp_AG_c:
case Ctlp_AF_c:
case Ctlp_AU_c:
case Ctlp_EX_c:
case Ctlp_EF_c:
case Ctlp_OR_c:
case Ctlp_AND_c:
case Ctlp_NOT_c:
case Ctlp_THEN_c:
case Ctlp_XOR_c:
case Ctlp_EQ_c:
if(ctlFormula->states != NIL(mdd_t))
mdd_free(ctlFormula->states);
ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i));
#if 0
fprintf(vis_stdout,"Attaching bdd for NOT,THEN %d",i);
bdd_print(ctlFormula->states);
#endif
if(leftChild){
if(i<number_left_bot){
CreateImportantWitness(OldleftChild,leftChild,i);
}
else {
CreateImportantWitness(OldleftChild,leftChild,0);
}
}
if(rightChild){
if(i<number_left_bot ){
CreateImportantWitness(OldrightChild,rightChild,0);
}
else{
CreateImportantWitness(OldrightChild,rightChild,i - number_left_bot + 1);
}
}
break;
case Ctlp_ID_c:
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
case Ctlp_Init_c:
if(ctlFormula->states != NIL(mdd_t))
mdd_free(ctlFormula->states);
ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i));
#if 0
fprintf(vis_stdout,"Attaching bdd for ID,TRUE %d",i);
bdd_print(ctlFormula->states);
#endif
break;
default:
break;
}
} /* CreateImportantWitness */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void EvaluateFormulaThoroughVacuity | ( | Fsm_Fsm_t * | fsm, |
| Ctlp_Formula_t * | ctlFormula, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | fairCondition, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| Fsm_HintsArray_t * | hintsArray, | ||
| Mc_GuidedSearch_t | hintType, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| int | buildOnionRing, | ||
| Mc_GSHScheduleType | GSHschedule, | ||
| mdd_t * | modelInitialStates | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Applies vacuum cleaning to a CTL formula.]
Description [This function evaluates all possible leaf replacements in parallel and attaches the information to the parse tree. This is a wrapper around ModelcheckAndVacuity; it is mainly responsible of dealing with global/local hints.]
SideEffects [Annotates the formula parse tree.]
SeeAlso [McVacuityDetection EvaluateFormulaWactlVacuity ModelcheckAndVacuity]
Definition at line 237 of file mcVacuum.c.
{
mdd_t *hint; /* to iterate over hintsArray */
int hintnr; /* idem */
assert(hintType == Mc_None_c || hintsArray != NIL(Fsm_HintsArray_t));
if(hintType != Mc_Global_c) {
ModelcheckAndVacuity(fsm, ctlFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
Ctlp_Exact_c, verbosity, dcLevel,
buildOnionRing, GSHschedule,
modelInitialStates);
return;
}
else{
array_t *result = NIL(array_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(array_t))
array_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;
ModelcheckAndVacuity(fsm,ctlFormula, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray, hintType,
approx, verbosity,
dcLevel, buildOnionRing,GSHschedule,
modelInitialStates);
/* TBD: take into account (early) termination here */
}
Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
return;
}
} /* EvaluateFormulaThoroughVacuity */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void EvaluateFormulaWactlVacuity | ( | Fsm_Fsm_t * | modelFsm, |
| Ctlp_Formula_t * | ctlFormula, | ||
| int | i, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | fairCond, | ||
| array_t * | modelCareStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| array_t * | hintsStatesArray, | ||
| Mc_GuidedSearch_t | guidedSearchType, | ||
| mdd_t * | modelInitialStates, | ||
| McOptions_t * | options | ||
| ) | [static] |
Function********************************************************************
Synopsis [Applies vacuity detection to a w-ACTL formula.]
Description [This function applies the algorithm of Beer et al. (CAV97) for vacuity detection of passing w-ACTL formulae. First regular model checking is applied to the given CTL formula. If the formula passes and is in w-ACTL, the witness formula is obtained by replacing the smallest important subformula with bottom. Model checking is then applied to the witness formula. A vacuous pass is reported if the witness property holds. Otherwise, the counterexample is an interesting witness to the original formula, that is, an execution of the model in which the given property holds in a non trivial manner.]
SideEffects [Annotates the parse tree of the formula.]
SeeAlso [McVacuityDetection EvaluateFormulaThoroughVacuity]
Definition at line 319 of file mcVacuum.c.
{
mdd_t *ctlFormulaStates;
boolean result1, result2;
Mc_VerbosityLevel verbosity = McOptionsReadVerbosityLevel(options);
Mc_DcLevel dcLevel = McOptionsReadDcLevel(options);
Mc_GSHScheduleType GSHschedule = McOptionsReadSchedule(options);
int buildOnionRings =
(McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity);
Mc_FwdBwdAnalysis traversalDirection =
McOptionsReadTraversalDirection(options);
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
ctlFormulaStates =
Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates,
fairCond, modelCareStatesArray,
earlyTermination, hintsStatesArray,
guidedSearchType, verbosity, dcLevel,
buildOnionRings,GSHschedule);
Mc_EarlyTerminationFree(earlyTermination);
if(hintsStatesArray != NIL(array_t))
mdd_array_free(hintsStatesArray);
result1 = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
ctlFormula, ctlFormulaStates,
modelInitialStates, modelCareStatesArray,
options, verbosity);
mdd_free(ctlFormulaStates);
if (result1 == FALSE)
fprintf(vis_stdout,
"# MC: Original formula failed. Aborting vacuity detection\n");
else {
/* see if we can create a witness formula */
if ((Ctlp_CheckClassOfExistentialFormula(ctlFormula) != Ctlp_ACTL_c) &&
(Ctlp_CheckClassOfExistentialFormula(ctlFormula) != Ctlp_QuantifierFree_c)) {
fprintf(vis_stdout,
"# MC: Not an ACTL Formula. Aborting vacuity detection\n");
}
else {
if (Ctlp_CheckIfWACTL(Ctlp_FormulaReadOriginalFormula(ctlFormula)) == Ctlp_NONWACTL_c) {
fprintf(vis_stdout, "# MC: Not a w-ACTL Formula. Aborting vacuity detection\n");
}
else {
Ctlp_Formula_t *origFormula, *witFormula;
/* We can create a witness formula. Annotate the original
* formula with negation parity info and then create a copy
* with the smallest important formula replaced by bottom. */
fprintf(vis_stdout, "Model checking the witness formula\n");
origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
Ctlp_FormulaNegations(origFormula, Ctlp_Even_c);
witFormula = Ctlp_FormulaCreateWitnessFormula(origFormula);
ctlFormula = Ctlp_FormulaConvertToExistentialForm(witFormula);
/* some user feedback */
if (verbosity != McVerbosityNone_c) {
(void)fprintf(vis_stdout, "Checking witness formula[%d] : ", i + 1);
Ctlp_FormulaPrint(vis_stdout,
Ctlp_FormulaReadOriginalFormula(ctlFormula));
(void)fprintf (vis_stdout, "\n");
assert(traversalDirection != McFwd_c);
}
/************** the actual computation *************************/
earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates);
ctlFormulaStates =
Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates,
fairCond, modelCareStatesArray,
earlyTermination, hintsStatesArray,
guidedSearchType, verbosity, dcLevel,
buildOnionRings,GSHschedule);
Mc_EarlyTerminationFree(earlyTermination);
if(hintsStatesArray != NIL(array_t))
mdd_array_free(hintsStatesArray);
/* user feedback on succes/fail */
result2 = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
ctlFormula, ctlFormulaStates,
modelInitialStates,
modelCareStatesArray,
options, verbosity);
if (result2)
(void)fprintf(vis_stdout, "# MC: Vacuous pass\n");
else
(void)fprintf(vis_stdout, "# MC: Not a vacuous pass\n");
mdd_free(ctlFormulaStates);
Ctlp_FormulaFree(ctlFormula);
Ctlp_FormulaFree(witFormula);
}
}
}
} /* EvaluateFormulaWactlVacuity */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FormulaFreeDebugDataVac | ( | Ctlp_Formula_t * | formula | ) | [static] |
Function********************************************************************
Synopsis [Free debugging info computed during CTL vacuum cleaning.]
Description [Frees debugging info attached to the parse tree by the CTL vacuum cleaning algorithm.]
SideEffects [Disposes of various sets attached to nodes of the parse tree.]
SeeAlso [McVacuityDetection]
Definition at line 2452 of file mcVacuum.c.
{
int i;
array_t *TopOnion, *BottomOnion;
Ctlp_FormulaType type = Ctlp_FormulaReadType(formula);
if(formula->type != Ctlp_ID_c ){
if (formula->left != NIL(Ctlp_Formula_t)) {
FormulaFreeDebugDataVac(formula->left);
}
if (formula->right != NIL(Ctlp_Formula_t)) {
FormulaFreeDebugDataVac(formula->right);
}
}
if (type == Ctlp_EU_c || type == Ctlp_EG_c ) {
if (formula->TopOnionRings != NIL(array_t)) {
TopOnion = formula->TopOnionRings;
for (i = 0; i < array_n(TopOnion); i++) {
if (type == Ctlp_EU_c) {
mdd_array_free(array_fetch(array_t *, TopOnion, i));
}
else if (type == Ctlp_EG_c)
mdd_array_array_free(array_fetch(array_t *, TopOnion, i));
}
array_free(TopOnion);
}
if (formula->BotOnionRings != NIL(array_t)) {
BottomOnion = formula->BotOnionRings;
for (i = 0; i < array_n(BottomOnion); i++) {
if (type == Ctlp_EU_c) {
mdd_array_free(array_fetch(array_t *, BottomOnion, i));
}
else if (type == Ctlp_EG_c)
mdd_array_array_free(array_fetch(array_t *, BottomOnion, i));
}
array_free(BottomOnion);
}
}
} /* FormulaFreeDebugDataVac */
Here is the call graph for this function:
Here is the caller graph for this function:
| static array_t * GenerateOnionRings | ( | array_t * | TempOnionRings, |
| array_t * | onionRings | ||
| ) | [static] |
Function********************************************************************
Synopsis [Merge onion rings for EU operators.]
Description []
SideEffects [The first argument is freed.]
SeeAlso [ModelcheckAndVacuity]
Definition at line 2386 of file mcVacuum.c.
{
array_t* MergeOnionRings;
int mdd1number, mdd2number, k;
mdd_t *temp,*temp1,*mdd1,*mdd2,*mdd3 = NIL(mdd_t);
mdd1number = array_n(TempOnionRings);
mdd2number = array_n(onionRings);
if(mdd1number == 0) {
MergeOnionRings = mdd_array_duplicate(onionRings);
array_free(TempOnionRings);
return (MergeOnionRings);
}
MergeOnionRings = array_alloc(mdd_t *, 0);
mdd1 = array_fetch(mdd_t *,TempOnionRings,0);
mdd2 = array_fetch(mdd_t *,onionRings,0);
temp = mdd_or(mdd1,mdd2,1,1); /* Building the core for EU */
array_insert(mdd_t *,MergeOnionRings,0, temp);
if(mdd2number>=mdd1number) {
for(k=1;k<mdd1number;k++) {
mdd1 = array_fetch(mdd_t *, onionRings, k);
mdd2 = array_fetch(mdd_t *, MergeOnionRings, k-1);
mdd3 = array_fetch(mdd_t *, TempOnionRings, k);
temp1 = mdd_or(mdd1,mdd3,1,1);
temp = mdd_and(temp1,mdd2,1,0);
mdd_free(temp1);
array_insert(mdd_t*, MergeOnionRings, k, temp);
}
for(k=mdd1number;k<mdd2number;k++) {
mdd1 = array_fetch(mdd_t *, onionRings, k);
mdd2 = array_fetch(mdd_t *, MergeOnionRings, k-1);
temp = mdd_and(mdd1,mdd2,1,0);
array_insert(mdd_t*, MergeOnionRings, k, temp);
}
}
else {
for(k=1;k<mdd2number;k++) {
mdd1 =array_fetch(mdd_t *, onionRings, k);
mdd2 =array_fetch(mdd_t *, MergeOnionRings, k-1);
mdd3 =array_fetch(mdd_t *, TempOnionRings, k);
temp1 = mdd_or(mdd1,mdd3,1,1);
temp = mdd_and(temp1,mdd2,1,0);
mdd_free(temp1);
array_insert(mdd_t*, MergeOnionRings, k, temp);
}
}
mdd_array_free(TempOnionRings);
return(MergeOnionRings);
} /* GenerateOnionRings */
Here is the caller graph for this function:
| static void match_bot | ( | Ctlp_Formula_t * | ctlFormula, |
| array_t * | mddArray, | ||
| array_t * | matchfound, | ||
| array_t * | matchelement | ||
| ) | [static] |
Function********************************************************************
Synopsis [Searches an mdd array of bottom sets for matches.]
Description []
SideEffects [The node of the formula is annotated with the match info.]
SeeAlso [match_top]
Definition at line 2336 of file mcVacuum.c.
{
int i, j, positionmatch;
mdd_t *leftMdd1 = NIL(mdd_t);
mdd_t *leftMdd2 = NIL(mdd_t);
arrayForEachItem(mdd_t *, mddArray, i, leftMdd1){
array_insert(boolean, matchfound, i, FALSE);
}
arrayForEachItem(mdd_t *, mddArray, i, leftMdd1) {
arrayForEachItem(mdd_t *, mddArray, j, leftMdd2) {
if ((i != 0) && (j != 0) && (i != j)) {
if (mdd_equal(leftMdd2, leftMdd1)) {
if (array_fetch(boolean, matchfound, i) == TRUE) {
if (array_fetch(int, matchelement, i) != j) {
positionmatch = array_fetch(int, matchelement, i);
array_insert(int, matchelement, j, positionmatch);
}
}
else {
array_insert(int, matchelement, j, i);
array_insert(boolean, matchfound, j ,TRUE);
}
}
}
}
}
ctlFormula->matchfound_bot = matchfound;
ctlFormula->matchelement_bot = matchelement;
return;
} /* match_bot */
Here is the caller graph for this function:
| static void match_top | ( | Ctlp_Formula_t * | ctlFormula, |
| array_t * | mddArray, | ||
| array_t * | matchfound, | ||
| array_t * | matchelement | ||
| ) | [static] |
Function********************************************************************
Synopsis [Searches an mdd array of top sets for matches.]
Description []
SideEffects [The node of the formula is annotated with the match info.]
SeeAlso [match_bot]
Definition at line 2286 of file mcVacuum.c.
{
int i, j, positionmatch;
mdd_t *leftMdd1 = NIL(mdd_t);
mdd_t *leftMdd2 = NIL(mdd_t);
arrayForEachItem(mdd_t *, mddArray, i, leftMdd1){
array_insert(boolean, matchfound, i, FALSE);
}
arrayForEachItem(mdd_t *, mddArray, i, leftMdd1) {
arrayForEachItem(mdd_t *, mddArray, j, leftMdd2) {
if((i != 0) && (j != 0) && (i != j)) {
if (mdd_equal(leftMdd2, leftMdd1)) {
if (array_fetch(boolean, matchfound,i) == TRUE) {
if(array_fetch(int, matchelement,i) != j) {
positionmatch = array_fetch(int, matchelement, i);
array_insert(int, matchelement, j, positionmatch);
}
}
else{
array_insert(int, matchelement, j, i);
array_insert(boolean, matchfound, j, TRUE);
}
}
}
}
}
ctlFormula->matchfound_top = matchfound;
ctlFormula->matchelement_top = matchelement;
return;
} /* match_top */
Here is the caller graph for this function:
| static array_t * McMddArrayArrayDup | ( | array_t * | arrayBddArray | ) | [static] |
Function********************************************************************
Synopsis [Duplicates an array of arrays of MDDs.]
Description [Makes sure ref counts are correct.]
SideEffects [none]
SeeAlso []
Definition at line 2256 of file mcVacuum.c.
{
int i;
array_t *bddArray, *tmpbddArray;
int length;
array_t *result;
/* put assert for this if (arrayBddArray != NIL(array_t)) { */
length = array_n(arrayBddArray);
result = array_alloc(array_t *, length);
for (i = 0; i < length; i++) {
bddArray = array_fetch(array_t *, arrayBddArray, i);
tmpbddArray = mdd_array_duplicate(bddArray);
array_insert(array_t *,result,i,tmpbddArray);
}
return(result);
} /* McMddArrayArrayDup */
Here is the caller graph for this function:
| void McVacuityDetection | ( | Fsm_Fsm_t * | modelFsm, |
| Ctlp_Formula_t * | ctlFormula, | ||
| int | i, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | fairCond, | ||
| array_t * | modelCareStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| array_t * | hintsStatesArray, | ||
| Mc_GuidedSearch_t | guidedSearchType, | ||
| mdd_t * | modelInitialStates, | ||
| McOptions_t * | options | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Model checks a formula and checks for its vacuity.]
Description [This function dispatches either w-ACTL vacuity detection or CTL vacuum cleaning. In the latter case also takes care of printing results.]
SideEffects [Annotates the nodes of the CTL formula with various sets.]
SeeAlso [EvaluateFormulaWactlVacuity EvaluateFormulaThoroughVacuity]
Definition at line 152 of file mcVacuum.c.
{
if (McOptionsReadBeerMethod(options)) {
EvaluateFormulaWactlVacuity(modelFsm, ctlFormula, i, fairStates, fairCond,
modelCareStatesArray, earlyTermination,
hintsStatesArray, guidedSearchType,
modelInitialStates, options);
}
else {
mdd_t *ctlFormulaStates;
boolean result;
Mc_VerbosityLevel verbosity = McOptionsReadVerbosityLevel(options);
Mc_DcLevel dcLevel = McOptionsReadDcLevel(options);
Mc_GSHScheduleType GSHschedule = McOptionsReadSchedule(options);
int buildOnionRings =
(McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity);
Mc_FwdBwdAnalysis traversalDirection =
McOptionsReadTraversalDirection(options);
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
Ctlp_FormulaNegations(ctlFormula,Ctlp_Even_c);
EvaluateFormulaThoroughVacuity(modelFsm, ctlFormula, fairStates,
fairCond, modelCareStatesArray,
earlyTermination, hintsStatesArray,
guidedSearchType, verbosity, dcLevel,
buildOnionRings, GSHschedule,
modelInitialStates);
Mc_EarlyTerminationFree(earlyTermination);
if(hintsStatesArray != NIL(array_t))
mdd_array_free(hintsStatesArray);
ctlFormulaStates = array_fetch(mdd_t *,ctlFormula->Bottomstates,0);
/* user feedback on succes/fail */
result = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
ctlFormula, ctlFormulaStates,
modelInitialStates, modelCareStatesArray,
options, verbosity);
if (result == TRUE) {
PrintVacuous(modelInitialStates,modelFsm,ctlFormula,
traversalDirection,modelCareStatesArray,
options, verbosity);
}
else {
PrintVacuousBottom(modelInitialStates,modelFsm,ctlFormula,
traversalDirection,modelCareStatesArray,
options, verbosity);
}
FormulaFreeDebugDataVac(ctlFormula);
}
} /* McVacuityDetection */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void ModelcheckAndVacuity | ( | Fsm_Fsm_t * | modelFsm, |
| Ctlp_Formula_t * | ctlFormula, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | fairCondition, | ||
| array_t * | modelCareStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| Fsm_HintsArray_t * | hintsArray, | ||
| Mc_GuidedSearch_t | hintType, | ||
| Ctlp_Approx_t | TRMinimization, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| int | buildOnionRings, | ||
| Mc_GSHScheduleType | GSHschedule, | ||
| mdd_t * | modelInitialStates | ||
| ) | [static] |
Function********************************************************************
Synopsis [Core algorithm for CTL vacuum cleaning.]
Description [This function recursively annotates the parse tree of a CTL formula with the sets of states that satisfy the original formula as well as the various replacements. If debugging is requested, it also stores onion rings. Since it is not known in advance whether the original formula passes or fails, this function computes both bottom and top replacements and tries to use monotonicity properties to accelerate fixpoint computations.]
SideEffects [Annotates the formula parse tree.]
SeeAlso [EvaluateFormulaThoroughVacuity]
Definition at line 564 of file mcVacuum.c.
{
mdd_t *result = NIL(mdd_t);
mdd_t *result_new = NIL(mdd_t);
mdd_t *result_bot = NIL(mdd_t);
mdd_t *result_top = NIL(mdd_t);
mdd_t *result_underapprox = NIL(mdd_t);
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
array_t *careStatesArray = NIL(array_t);
array_t *mddArray_bot = NIL(array_t);
array_t *mddArray_top = NIL(array_t);
array_t *leavesArray = NIL(array_t);
array_t *leavesLeftArray = NIL(array_t);
array_t *leavesRightArray = NIL(array_t);
array_t *matchfound_bot = NIL(array_t);
array_t *matchfound_top = NIL(array_t);
array_t *matchelement_bot = NIL(array_t);
array_t *matchelement_top = 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_Formula_t *leftChild,*rightChild ;
mdd_t *leftMdd = NIL(mdd_t);
mdd_t *rightMdd = NIL(mdd_t);
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 approx_decide = FALSE; */
/* We will propagate early termination ONLY to the outmost fixpoint,
and only propagate through negation. We should also propagate
over other boolean operators, and maybe temporal operators.
Propagation over negation is done by complementing the type. */
rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
if (leftChild) {
if ((leftChild->share) == 1){
Mc_EarlyTermination_t *nextEarlyTermination =
McObtainUpdatedEarlyTerminationCondition(
earlyTermination, NIL(mdd_t), Ctlp_FormulaReadType(ctlFormula));
ModelcheckAndVacuity(modelFsm, leftChild,fairStates,
fairCondition, modelCareStatesArray,
nextEarlyTermination,
hintsArray, hintType,
TRMinimization, verbosity,dcLevel,
buildOnionRings, GSHschedule,
modelInitialStates);
Mc_EarlyTerminationFree(nextEarlyTermination);
}
}
if (rightChild) {
if((rightChild->share) == 1) {
Mc_EarlyTermination_t *nextEarlyTermination =
McObtainUpdatedEarlyTerminationCondition(
earlyTermination,NIL(mdd_t) ,Ctlp_FormulaReadType(ctlFormula));
ModelcheckAndVacuity(modelFsm, rightChild, fairStates,
fairCondition,
modelCareStatesArray,
nextEarlyTermination,
hintsArray, hintType,
TRMinimization, verbosity, dcLevel,
buildOnionRings, GSHschedule,
modelInitialStates);
Mc_EarlyTerminationFree(nextEarlyTermination);
}
}
if (modelCareStatesArray != NIL(array_t)) {
careStatesArray = modelCareStatesArray;
} else {
careStatesArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, careStatesArray, mdd_one(mddMgr));
}
mddArray_bot = array_alloc(mdd_t *, 0);
mddArray_top = array_alloc(mdd_t *, 0);
ctlFormula->share = 2;
switch (Ctlp_FormulaReadType(ctlFormula)) {
case Ctlp_ID_c :{
result = McModelCheckAtomicFormula(modelFsm, ctlFormula);
matchfound_top = array_alloc(boolean, 0);
matchfound_bot = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
leavesArray = array_alloc(Ctlp_Formula_t *, 0);
array_insert(mdd_t *, mddArray_bot , 0, mdd_dup(result));
array_insert(mdd_t *, mddArray_top , 0, result);
/* if the formula is an important subformula, we need to find the
bottom and top set for it as well. */
if (ctlFormula->negation_parity != Ctlp_EvenOdd_c) {
array_insert_last(Ctlp_Formula_t *, leavesArray, ctlFormula);
if (ctlFormula->negation_parity == Ctlp_Even_c) {
/* if the formula has even negation partity, it should be replaced
with FALSE. */
result_bot = mdd_zero(mddMgr);
result_top = mdd_one(mddMgr);
}
else {
/* if the formula has odd negation parity, it should be replaced
with TRUE. */
result_bot = mdd_one(mddMgr);
result_top = mdd_zero(mddMgr);
}
array_insert_last(mdd_t *,mddArray_bot ,result_bot);
array_insert_last(mdd_t *,mddArray_top ,result_top);
/* Finding match for bottom sets */
if(mdd_equal(result_bot,array_fetch(mdd_t *, mddArray_bot, 0))){
array_insert(boolean, matchfound_bot, 1 ,TRUE);
array_insert(int, matchelement_bot, 1 ,0);
}
else
array_insert(boolean, matchfound_bot, 1 ,FALSE);
/* Finding match for top sets */
if(mdd_equal(result_top,array_fetch(mdd_t *, mddArray_top, 0))){
array_insert(boolean, matchfound_top, 1 ,TRUE);
array_insert(int, matchelement_top, 1 ,0);
}
else
array_insert(boolean, matchfound_top, 1 ,FALSE);
}
array_insert(boolean, matchfound_bot, 0 ,FALSE);
array_insert(boolean, matchfound_top, 0 ,FALSE);
/* only exact set will be there if the formula is not an important
subformula. */
ctlFormula->Topstates= mddArray_top;
ctlFormula->matchfound_top = matchfound_top;
ctlFormula->matchelement_top = matchelement_top;
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->matchfound_bot = matchfound_bot;
ctlFormula->matchelement_bot = matchelement_bot;
ctlFormula->leaves = leavesArray;
break;
}
case Ctlp_TRUE_c :{
result = mdd_one(mddMgr);
leavesArray = array_alloc(Ctlp_Formula_t *, 0);
matchfound_top = array_alloc(boolean, 0);
matchfound_bot = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
array_insert_last(mdd_t *,mddArray_bot , mdd_dup(result));
array_insert_last(mdd_t *,mddArray_top , result);
array_insert(boolean, matchfound_bot, 0 ,FALSE);
array_insert(boolean, matchfound_top, 0 ,FALSE);
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->matchfound_bot = matchfound_bot;
ctlFormula->matchelement_bot = matchelement_bot;
ctlFormula->Topstates = mddArray_top;
ctlFormula->matchfound_top = matchfound_top;
ctlFormula->matchelement_top = matchelement_top;
ctlFormula->leaves = leavesArray;
break;
}
case Ctlp_FALSE_c :{
result = mdd_zero(mddMgr);
leavesArray = array_alloc(Ctlp_Formula_t *, 0);
matchfound_top = array_alloc(boolean, 0);
matchfound_bot = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
array_insert_last(mdd_t *,mddArray_bot ,mdd_dup(result));
array_insert_last(mdd_t *,mddArray_top ,mdd_dup(result));
array_insert(boolean, matchfound_bot, 0 ,FALSE);
array_insert(boolean, matchfound_top, 0 ,FALSE);
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->matchfound_bot = matchfound_bot;
ctlFormula->matchelement_bot = matchelement_bot;
ctlFormula->Topstates = mddArray_top;
ctlFormula->matchfound_top = matchfound_top;
ctlFormula->matchelement_top = matchelement_top;
ctlFormula->leaves = leavesArray;
break;
}
case Ctlp_NOT_c :{
int i,positionmatch;
arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
/* Now we shoud negate the accurate as well bottom mdds */
/* Compute Bottom sets */
if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){
result = mdd_not(leftMdd);
array_insert_last(mdd_t *, mddArray_bot, mdd_dup(result));
mdd_free(result);
}
else{
positionmatch = array_fetch(int, leftChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch));
array_insert_last(mdd_t *, mddArray_bot,result);
}
}
arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
/* Compute for Top States */
if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){
result = mdd_not(leftMdd);
array_insert_last(mdd_t *, mddArray_top, mdd_dup(result));
mdd_free(result);
}
else{
positionmatch = array_fetch(int, leftChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
/* Now attach the array to the ctlFormula */
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot);
ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot);
ctlFormula->Topstates = mddArray_top;
ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top);
ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top);
/* find out the leaves attached to this nodes.*/
leavesLeftArray = leftChild->leaves;
ctlFormula->leaves = array_dup(leavesLeftArray);
break;
}
case Ctlp_AND_c:{
int number_right_bot = array_n(rightChild->Bottomstates);
int number_right_top = array_n(rightChild->Topstates);
int number_left_bot = array_n(leftChild->Bottomstates);
int number_left_top = array_n(leftChild->Topstates);
int i,positionmatch;
leavesArray = array_alloc(Ctlp_Formula_t *, 0);
matchfound_top = array_alloc(boolean, 0);
matchfound_bot = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
/* And operation*/
/* for bottom sets */
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){
result = mdd_and(leftMdd, rightMdd, 1, 1);
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int,leftChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
for(i=1;i<number_right_bot;i++){
if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
result = mdd_and(leftMdd, rightMdd, 1, 1);
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int,rightChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch + number_left_bot - 1)));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
/* for top sets */
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){
result = mdd_and(leftMdd, rightMdd, 1, 1);
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int,leftChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
for(i=1;i<number_right_top;i++){
if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
result = mdd_and(leftMdd, rightMdd, 1, 1);
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int,rightChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch + number_left_top - 1)));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
/* Now attach the array to the ctlFormula */
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->Topstates = mddArray_top;
/* find out the leaves attached to this nodes.*/
leavesLeftArray = leftChild->leaves;
leavesRightArray = rightChild->leaves;
array_append(leavesArray,leavesLeftArray);
array_append(leavesArray,leavesRightArray);
ctlFormula->leaves = leavesArray;
break;
}
/* Use of EQ, XOR, THEN, OR is discouraged. Please use convert
formula to simple existential form. */
case Ctlp_EQ_c :{
int number_right_bot = array_n(rightChild->Bottomstates);
int number_right_top = array_n(rightChild->Topstates);
int number_left_bot = array_n(leftChild->Bottomstates);
int number_left_top = array_n(leftChild->Topstates);
int i,positionmatch;
leavesArray = array_alloc(Ctlp_Formula_t *, 0);
matchfound_top = array_alloc(boolean, 0);
matchfound_bot = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
/* for bottom sets */
rightMdd= array_fetch(mdd_t *,rightChild->Bottomstates,0);
arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){
result = mdd_xnor(leftMdd,rightMdd);
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int,leftChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
for(i=1;i<number_right_bot;i++){
if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
result = mdd_xnor(leftMdd,rightMdd );
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int,rightChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch+ number_left_bot - 1)));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
/* for top sets */
rightMdd= array_fetch(mdd_t *,rightChild->Topstates,0);
arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){
result = mdd_xnor(leftMdd,rightMdd);
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int,leftChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
for(i=1;i<number_right_top;i++){
if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
result = mdd_xnor(leftMdd,rightMdd );
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int,rightChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch+ number_left_top - 1)));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
/* Now attach the array to the ctlFormula */
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->Topstates = mddArray_top;
/* find out the leaves attached to this nodes.*/
leavesLeftArray = leftChild->leaves;
leavesRightArray = rightChild->leaves;
array_append(leavesArray,leavesLeftArray);
array_append(leavesArray,leavesRightArray);
ctlFormula->leaves = leavesArray;
break;
}
case Ctlp_XOR_c :{
int number_right_bot = array_n(rightChild->Bottomstates);
int number_right_top = array_n(rightChild->Topstates);
int number_left_bot = array_n(leftChild->Bottomstates);
int number_left_top = array_n(leftChild->Topstates);
int i,positionmatch;
leavesArray = array_alloc(Ctlp_Formula_t *, 0);
matchfound_top = array_alloc(boolean, 0);
matchfound_bot = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
/* for bottom sets */
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){
result = mdd_xor(leftMdd,rightMdd);
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int,leftChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
for(i=1;i<number_right_bot;i++){
if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
result = mdd_xor(leftMdd,rightMdd );
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int,rightChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch+ number_left_bot - 1)));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
/* for top sets */
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){
result = mdd_xor(leftMdd,rightMdd);
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int,leftChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
for(i=1;i<number_right_top;i++){
if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
result = mdd_xor(leftMdd,rightMdd );
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int,rightChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch + number_left_top - 1)));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
/* Now attach the array to the ctlFormula */
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->Topstates = mddArray_top;
/* find out the leaves attached to this nodes.*/
leavesLeftArray = leftChild->leaves;
leavesRightArray = rightChild->leaves;
array_append(leavesArray,leavesLeftArray);
array_append(leavesArray,leavesRightArray);
ctlFormula->leaves = leavesArray;
break;
}
case Ctlp_THEN_c :{
int number_right_bot = array_n(rightChild->Bottomstates);
int number_right_top = array_n(rightChild->Topstates);
int number_left_bot = array_n(leftChild->Bottomstates);
int number_left_top = array_n(leftChild->Topstates);
int i,positionmatch;
leavesArray = array_alloc(Ctlp_Formula_t *, 0);
matchfound_top = array_alloc(boolean, 0);
matchfound_bot = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
/* bottom sets */
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){
result = mdd_or(leftMdd ,rightMdd,0,1);
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int,leftChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
for(i=1;i<number_right_bot;i++){
if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
result = mdd_or(leftMdd,rightMdd ,0,1);
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int,rightChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, (positionmatch + number_left_bot - 1)));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
/* top sets */
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){
result = mdd_or(leftMdd ,rightMdd,0,1);
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int,leftChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
for(i=1;i<number_right_top;i++){
if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
result = mdd_or(leftMdd,rightMdd ,0,1);
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int,rightChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_top, (positionmatch + number_left_top - 1)));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
/* Now attach the array to the ctlFormula */
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->Topstates = mddArray_top;
/* find out the leaves attached to this nodes.*/
leavesLeftArray = leftChild->leaves;
leavesRightArray = rightChild->leaves;
array_append(leavesArray,leavesLeftArray);
array_append(leavesArray,leavesRightArray);
ctlFormula->leaves = leavesArray;
break;
}
case Ctlp_OR_c:{
int number_right_bot = array_n(rightChild->Bottomstates);
int number_right_top = array_n(rightChild->Topstates);
int number_left_bot = array_n(leftChild->Bottomstates);
int number_left_top = array_n(leftChild->Topstates);
int i,positionmatch;
leavesArray = array_alloc(Ctlp_Formula_t *, 0);
matchfound_top = array_alloc(boolean, 0);
matchfound_bot = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
/* OR operation*/
/* bottom sets */
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){
result = mdd_or(leftMdd,rightMdd,1,1);
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int,leftChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
for(i=1;i<number_right_bot;i++){
if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
result = mdd_or(leftMdd,rightMdd ,1,1);
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int,rightChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, (positionmatch + number_left_bot - 1)));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
/* top sets */
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){
result = mdd_or(leftMdd,rightMdd,1,1);
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int,leftChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
for(i=1;i<number_right_top;i++){
if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
result = mdd_or(leftMdd,rightMdd ,1,1);
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int,rightChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_top, (positionmatch + number_left_top - 1)));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
/* Now attach the array to the ctlFormula */
ctlFormula->Topstates = mddArray_top;
ctlFormula->Bottomstates = mddArray_bot;
/* ctlFormula->states = array_fetch(mdd_t *, mddArray, 0); */
/* find out the leaves attached to this nodes.*/
leavesLeftArray = leftChild->leaves;
leavesRightArray = rightChild->leaves;
array_append(leavesArray,leavesLeftArray);
array_append(leavesArray,leavesRightArray);
ctlFormula->leaves = leavesArray;
break;
}
case Ctlp_EX_c:{
int i,positionmatch;
if (ctlFormula->negation_parity == Ctlp_Even_c) {
/* bottom sets shoud be computed first i.e underapproximations */
arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){
result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
careStatesArray, verbosity, dcLevel);
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int, leftChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
result = array_fetch(mdd_t *, mddArray_bot, 0); /* exact set */
}
else{
/* top sets should be computed first i.e., underapproximations */
arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){
result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
careStatesArray, verbosity, dcLevel);
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int, leftChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
result = array_fetch(mdd_t *, mddArray_top, 0); /* exact set */
}
if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)){
if (ctlFormula->negation_parity == Ctlp_Even_c) {
ctlFormula->Bottomstates = mddArray_bot;
arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
array_insert_last(mdd_t *, mddArray_top, mdd_dup(result));
}
ctlFormula->Topstates = mddArray_top;
ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot);
ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot);
matchfound_top = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
}
else{
ctlFormula->Topstates = mddArray_top;
arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
array_insert_last(mdd_t *, mddArray_bot, mdd_dup(result));
}
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->matchfound_top = array_dup(leftChild->matchfound_bot);
ctlFormula->matchelement_top = array_dup(leftChild->matchelement_bot);
matchfound_bot = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
}
/* find out the leaves attached to this nodes.*/
leavesLeftArray = leftChild->leaves;
ctlFormula->leaves = array_dup(leavesLeftArray);
break;
}
if (ctlFormula->negation_parity == Ctlp_Even_c) {
/* top sets */
arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){
result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
careStatesArray, verbosity, dcLevel);
array_insert_last(mdd_t *, mddArray_top, result);
}
else{
positionmatch = array_fetch(int, leftChild->matchelement_top, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch));
array_insert_last(mdd_t *, mddArray_top, result);
}
}
}
else {
arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){
result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
careStatesArray, verbosity, dcLevel);
array_insert_last(mdd_t *, mddArray_bot, result);
}
else{
positionmatch = array_fetch(int, leftChild->matchelement_bot, i);
result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch));
array_insert_last(mdd_t *, mddArray_bot, result);
}
}
}
/* Now attach the array to the ctlFormula */
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot);
ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot);
ctlFormula->Topstates = mddArray_top;
ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top);
ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top);
/* find out the leaves attached to this nodes.*/
leavesLeftArray = leftChild->leaves;
ctlFormula->leaves = array_dup(leavesLeftArray);
break;
}
case Ctlp_EU_c:{
array_t *onionRings = NIL(array_t);
array_t *MergeOnionRings = NIL(array_t);
array_t *ExactOnionRings = NIL(array_t);
array_t *NewOnionRings = NIL(array_t); /* array of mdd_t */
boolean fixpoint;
int number_left_bot = array_n(leftChild->Bottomstates);
int number_right_bot = array_n(rightChild->Bottomstates);
int number_left_top = array_n(leftChild->Topstates);
int number_right_top = array_n(rightChild->Topstates);
int i;
int j = 1;
mdd_t *approx_under = NIL(mdd_t);
array_t *botrings = NIL(array_t);
array_t *toprings = NIL(array_t);
leavesArray = array_alloc(Ctlp_Formula_t *, 0);
matchfound_top = array_alloc(boolean, 0);
matchfound_bot = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Underapprox_c );
onionRings = NIL(array_t);
if (buildOnionRings) {
MergeOnionRings = array_alloc(mdd_t *, 0);
botrings = array_alloc(array_t*,0);
toprings = array_alloc(array_t*,0);
}
if (ctlFormula->negation_parity == Ctlp_Even_c) {
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
result_underapprox = mdd_zero(mddMgr);
/* Compute the bottom mdds first which provide the underapproximation
* to the exact set*/
for(i=1;i<number_left_bot;i++) {
if (buildOnionRings)
onionRings = array_alloc(mdd_t *, 0);
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i);
result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
rightMdd,
approx, fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
array_insert(mdd_t *, mddArray_bot, j, result);
if (buildOnionRings) {
if(i==1) {
mdd_array_free(MergeOnionRings);
MergeOnionRings = mdd_array_duplicate(onionRings);
/* saving the bottom computation onion rings */
array_insert(array_t*,botrings,j,onionRings);
}
else {
MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings);
/* saving the bottom computation onion rings */
array_insert(array_t*,botrings,j,onionRings);
}
}
j++;
result_new = mdd_or(result,result_underapprox,1,1);
mdd_free(result_underapprox);
result_underapprox = result_new;
}
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
for(i=1;i<number_right_bot;i++) {
if (buildOnionRings)
onionRings = array_alloc(mdd_t *, 0);
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd,
rightMdd,
approx, fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
array_insert(mdd_t *, mddArray_bot, j, result);
if (buildOnionRings) {
if(i==1) {
mdd_array_free(MergeOnionRings);
MergeOnionRings = mdd_array_duplicate(onionRings);
/* saving the bottom computation onion rings */
array_insert(array_t*,botrings,j,onionRings);
}
else {
MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings);
/* saving the bottom computation onion rings */
array_insert(array_t*,botrings,j,onionRings);
}
}
j++;
result_new = mdd_or(result,result_underapprox,1,1);
mdd_free(result_underapprox);
result_underapprox = result_new;
}
/* Use the under approximations to calculate the exact set. */
if (approx != NIL(mdd_t)) {
mdd_t *tmp = mdd_or(result_underapprox,approx,1,1);
mdd_free(approx);
mdd_free(result_underapprox);
approx = tmp;
} else {
approx = result_underapprox;
}
if (buildOnionRings) {
onionRings = array_alloc(mdd_t *, 0);
}
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
rightMdd,
approx, fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
array_insert(mdd_t *, mddArray_bot, 0, mdd_dup(result));
array_insert(mdd_t *, mddArray_top, 0, result);
if (buildOnionRings) {
MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings);
mdd_array_free(onionRings);
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) MergeOnionRings,
McFormulaFreeDebugData);
array_insert(array_t *,botrings,0,mdd_array_duplicate(MergeOnionRings));
array_insert(array_t *,toprings,0,mdd_array_duplicate(MergeOnionRings));
}
result = array_fetch(mdd_t *,mddArray_bot,0);
if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)) {
leavesLeftArray = leftChild->leaves;
array_append(leavesArray,leavesLeftArray);
leavesRightArray = rightChild->leaves;
array_append(leavesArray,leavesRightArray);
ctlFormula->leaves = leavesArray;
j=1;
for(i=1;i<number_left_top;i++) {
array_insert(mdd_t *, mddArray_top, j, mdd_dup(result));
if (buildOnionRings) {
array_insert(array_t *,toprings,j,
mdd_array_duplicate(MergeOnionRings));
}
j++;
}
for(i=1;i<number_right_top;i++) {
array_insert(mdd_t *, mddArray_top, j, mdd_dup(result));
if (buildOnionRings){
array_insert(array_t *,toprings,j,
mdd_array_duplicate(MergeOnionRings));
}
j++;
}
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->Topstates = mddArray_top;
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
if (buildOnionRings) {
ctlFormula->BotOnionRings = botrings;
ctlFormula->TopOnionRings = toprings;
}
mdd_free(approx);
break; /* bottom failing */
}
/* top sets
* we can use the exact set as an approximation to compute the top
* set. */
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
j=1;
if (buildOnionRings)
ExactOnionRings = mdd_array_duplicate(MergeOnionRings);
/* Compute the Top mdds now */
for(i=1;i<number_left_top;i++) {
if (buildOnionRings)
onionRings = array_alloc(mdd_t *, 0);
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i);
approx_under = array_fetch(mdd_t *,mddArray_bot,0);
result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
rightMdd,
approx_under, fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
array_insert(mdd_t *, mddArray_top, j, result);
if (buildOnionRings) {
array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings);
NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings);
/* saving the bottom computation onion rings */
array_insert(array_t*,toprings,j,NewOnionRings);
mdd_array_free(onionRings);
}
j++;
}
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
for(i=1;i<number_right_top;i++) {
if (buildOnionRings)
onionRings = array_alloc(mdd_t *, 0);
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
approx_under = array_fetch(mdd_t *,mddArray_top,0);
result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd,
rightMdd,
approx_under, fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
array_insert(mdd_t *, mddArray_top, j, result);
if (buildOnionRings) {
array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings);
NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings);
/* saving the bottom computation onion rings */
array_insert(array_t*,toprings,j,NewOnionRings);
mdd_array_free(onionRings);
}
j++;
}
}
else {
/* The negation parity is odd. So the top sets will provide
underapproximations now. */
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
result_underapprox = mdd_zero(mddMgr);
/* Compute the top mdds first */
for(i=1;i<number_left_top;i++) {
if (buildOnionRings)
onionRings = array_alloc(mdd_t *, 0);
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i);
result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
rightMdd,
NIL(mdd_t), fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
array_insert(mdd_t *, mddArray_top, j, result);
if (buildOnionRings){
if(i==1){
mdd_array_free(MergeOnionRings);
MergeOnionRings = mdd_array_duplicate(onionRings);
array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */
}
else {
array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */
MergeOnionRings=GenerateOnionRings(MergeOnionRings,onionRings);
}
}
j++;
result_new = mdd_or(result,result_underapprox,1,1);
mdd_free(result_underapprox);
result_underapprox = result_new;
}
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
for(i=1;i<number_right_top;i++) {
if (buildOnionRings)
onionRings = array_alloc(mdd_t *, 0);
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd,
rightMdd,
NIL(mdd_t), fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
array_insert(mdd_t *, mddArray_top, j, result);
if (buildOnionRings) {
if(j==1){
mdd_array_free(MergeOnionRings);
MergeOnionRings = mdd_array_duplicate(onionRings);
array_insert(array_t*,toprings,j,onionRings); /* saving the top computation onion rings */
}
else {
MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings);
array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */
}
}
j++;
result_new = mdd_or(result,result_underapprox,1,1);
mdd_free(result_underapprox);
result_underapprox = result_new;
}
/* Use the under approximations to calculate the exact set. */
if (approx != NIL(mdd_t)) {
mdd_t *tmp = mdd_or(result_underapprox,approx,1,1);
mdd_free(approx);
mdd_free(result_underapprox);
approx = tmp;
} else {
approx = result_underapprox;
}
if (buildOnionRings) {
onionRings = array_alloc(mdd_t *, 0);
}
/* exact set computation */
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
rightMdd,
approx, fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
array_insert(mdd_t *, mddArray_bot, 0, mdd_dup(result));
array_insert(mdd_t *, mddArray_top, 0, result);
if (buildOnionRings) {
MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings);
mdd_array_free(onionRings);
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) MergeOnionRings,
McFormulaFreeDebugData);
array_insert(array_t *,botrings,0,
mdd_array_duplicate(MergeOnionRings));
array_insert(array_t *,toprings,0,
mdd_array_duplicate(MergeOnionRings));
}
result = array_fetch(mdd_t *,mddArray_bot,0);
if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)) {
leavesLeftArray = leftChild->leaves;
array_append(leavesArray,leavesLeftArray);
leavesRightArray = rightChild->leaves;
array_append(leavesArray,leavesRightArray);
ctlFormula->leaves = leavesArray;
j=1;
for(i=1;i<number_left_bot;i++) {
array_insert(mdd_t *, mddArray_bot, j, mdd_dup(result));
if (buildOnionRings){
array_insert(array_t *,botrings,j,
mdd_array_duplicate(MergeOnionRings));
}
j++;
}
for(i=1;i<number_right_bot;i++) {
array_insert(mdd_t *, mddArray_bot, j, mdd_dup(result));
if (buildOnionRings){
array_insert(array_t *,botrings,j,
mdd_array_duplicate(MergeOnionRings));
}
j++;
}
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->Topstates = mddArray_top;
if (buildOnionRings){
ctlFormula->BotOnionRings = botrings;
ctlFormula->TopOnionRings = toprings;
}
assert(approx != NIL(mdd_t));
mdd_free(approx);
break; /* bottom failing */
}
if (buildOnionRings)
ExactOnionRings = mdd_array_duplicate(MergeOnionRings);
/* we can use the exact set as an approximation to compute
the bottom set. */
rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
j=1;
/* Compute the botom mdds now */
for(i=1;i<number_left_bot;i++) {
if (buildOnionRings)
onionRings = array_alloc(mdd_t *, 0);
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i);
approx_under = array_fetch(mdd_t *,mddArray_bot,0);
result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
rightMdd,
approx_under, fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
array_insert(mdd_t *, mddArray_bot, j, result);
if (buildOnionRings){
array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings);
NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings);
/* saving the bottom computation onion rings */
array_insert(array_t*,botrings,j,NewOnionRings);
mdd_array_free(onionRings);
}
j++;
}
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
for(i=1;i<number_right_bot;i++) {
if (buildOnionRings)
onionRings = array_alloc(mdd_t *, 0);
else
onionRings = NIL(array_t);
rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
approx_under = array_fetch(mdd_t *,mddArray_bot,0);
result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd,
rightMdd,
NIL(mdd_t), fairStates,
careStatesArray,
earlyTermination, hintsArray,
hintType, onionRings,
verbosity, dcLevel, &fixpoint);
array_insert(mdd_t *, mddArray_bot, j, result);
if (buildOnionRings) {
array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings);
NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings);
array_insert(array_t*,botrings,j,NewOnionRings);
mdd_array_free(onionRings);
}
j++;
}
}
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->Topstates = mddArray_top;
leavesLeftArray = leftChild->leaves;
array_append(leavesArray,leavesLeftArray);
leavesRightArray = rightChild->leaves;
array_append(leavesArray,leavesRightArray);
ctlFormula->leaves = leavesArray;
if (buildOnionRings) {
ctlFormula->BotOnionRings = botrings;
ctlFormula->TopOnionRings = toprings;
mdd_array_free(ExactOnionRings);
}
if(approx != NIL(mdd_t))
mdd_free(approx);
/* Can't combine under and overapprox */
if(!fixpoint && TRMinimization == Ctlp_Overapprox_c)
TRMinimization = Ctlp_Incomparable_c;
break;
}
case Ctlp_EG_c:{
boolean fixpoint;
mdd_t *result_ub;
mdd_t *approx_over = NIL(mdd_t) ;
int number_bot = array_n(leftChild->Bottomstates);
int number_top = array_n(leftChild->Topstates);
int i;
array_t *arrayOfOnionRings = NIL(array_t); /* array of array of mdd_t* */
array_t *botrings = NIL(array_t);
array_t *toprings = NIL(array_t);
matchfound_top = array_alloc(boolean, 0);
matchfound_bot = array_alloc(boolean, 0);
matchelement_top = array_alloc(int, 0);
matchelement_bot = array_alloc(int, 0);
approx = Ctlp_FormulaObtainApproxStates(ctlFormula, Ctlp_Overapprox_c);
if(buildOnionRings) {
botrings = array_alloc(array_t*,0);
toprings = array_alloc(array_t*,0);
}
if (approx == NIL(mdd_t)) {
result_ub = mdd_one(mddMgr);
} else {
result_ub = mdd_dup(approx);
}
if (ctlFormula->negation_parity == Ctlp_Even_c) {
/* compute the top sets first which will give us
overapproximation to the exact set */
for(i=1;i<number_top;i++) {
if(buildOnionRings)
arrayOfOnionRings = array_alloc(array_t *, 0);
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i);
result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
NIL(mdd_t), fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType,
&arrayOfOnionRings, verbosity,
dcLevel, &fixpoint, GSHschedule);
array_insert(mdd_t *, mddArray_top, i, result);
if(buildOnionRings) {
array_insert(array_t*,toprings,i,arrayOfOnionRings);
}
result_new = mdd_and(result_ub,result,1,1);
mdd_free(result_ub);
result_ub = result_new;
}
/* calculate the exact set */
if(buildOnionRings)
arrayOfOnionRings = array_alloc(array_t *, 0);
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
NIL(mdd_t), fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType,
&arrayOfOnionRings, verbosity,
dcLevel, &fixpoint, GSHschedule);
array_insert(mdd_t *,mddArray_bot,0,mdd_dup(result));
array_insert(mdd_t *,mddArray_top,0,mdd_dup(result));
mdd_free(result);
if(buildOnionRings) {
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
McFormulaFreeDebugData);
array_insert(array_t*,toprings,0,McMddArrayArrayDup(arrayOfOnionRings));
array_insert(array_t*,botrings,0,McMddArrayArrayDup(arrayOfOnionRings));
}
result = array_fetch(mdd_t *,mddArray_bot,0);
if (McCheckEarlyTerminationForOverapprox(earlyTermination, result, careStatesArray)) {
leavesLeftArray = leftChild->leaves;
ctlFormula->leaves = array_dup(leavesLeftArray);
for(i=1;i<number_bot;i++) {
array_insert(mdd_t *, mddArray_bot, i, mdd_dup(result));
if(buildOnionRings) {
array_insert(array_t*,botrings,i,McMddArrayArrayDup(arrayOfOnionRings));
}
}
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->Topstates = mddArray_top;
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
if (buildOnionRings) {
ctlFormula->BotOnionRings = botrings;
ctlFormula->TopOnionRings = toprings;
}
break;/* top passing */
}
/* now calculate the bottom set */
for(i=1;i<number_bot;i++) {
if(buildOnionRings)
arrayOfOnionRings = array_alloc(array_t *, 0);
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i);
approx_over = array_fetch(mdd_t *,mddArray_bot,0);
result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
approx_over, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType,
&arrayOfOnionRings, verbosity,
dcLevel, &fixpoint, GSHschedule);
array_insert(mdd_t *, mddArray_bot, i, result);
if(buildOnionRings) {
array_insert(array_t*,botrings,i,arrayOfOnionRings);
}
}
}
else {
/* compute the bottom sets first which will give us
overapproximation to the exact set */
for(i=1;i<number_bot;i++) {
if(buildOnionRings)
arrayOfOnionRings = array_alloc(array_t *, 0);
leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i);
result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
NIL(mdd_t), fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType,
&arrayOfOnionRings, verbosity,
dcLevel, &fixpoint, GSHschedule);
if(buildOnionRings) {
array_insert(array_t*,botrings,i,arrayOfOnionRings);
}
array_insert(mdd_t *, mddArray_bot, i, result);
result_new = mdd_and(result_ub,result,1,1);
mdd_free(result_ub);
result_ub = result_new;
}
/* calculate the exact set */
if(buildOnionRings){
arrayOfOnionRings = array_alloc(array_t *, 0);
}
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
result_ub, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType,
&arrayOfOnionRings, verbosity,
dcLevel, &fixpoint, GSHschedule);
array_insert(mdd_t *,mddArray_bot,0,mdd_dup(result));
array_insert(mdd_t *,mddArray_top,0,mdd_dup(result));
mdd_free(result);
if (buildOnionRings) {
Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
McFormulaFreeDebugData);
array_insert(array_t*,botrings,0,McMddArrayArrayDup(arrayOfOnionRings));
array_insert(array_t*,toprings,0,McMddArrayArrayDup(arrayOfOnionRings));
}
result = array_fetch(mdd_t *,mddArray_bot,0);
if (McCheckEarlyTerminationForOverapprox(earlyTermination, result, careStatesArray)) {
leavesLeftArray = leftChild->leaves;
ctlFormula->leaves = array_dup(leavesLeftArray);
for(i=1;i<number_top;i++) {
array_insert(mdd_t *, mddArray_top, i, mdd_dup(result));
if(buildOnionRings)
array_insert(array_t*,toprings,i,McMddArrayArrayDup(arrayOfOnionRings));
}
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->Topstates = mddArray_top;
match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
if (buildOnionRings) {
ctlFormula->BotOnionRings = botrings;
ctlFormula->TopOnionRings = toprings;
}
break; /* top passing */
}
/* calculate the top set now */
for(i=1;i<number_top;i++) {
if (buildOnionRings) {
arrayOfOnionRings = array_alloc(array_t *, 0);
}
leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i);
approx_over = array_fetch(mdd_t *,mddArray_bot,0);
result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
approx, fairStates,
fairCondition, careStatesArray,
earlyTermination, hintsArray,
hintType,
&arrayOfOnionRings, verbosity,
dcLevel, &fixpoint, GSHschedule);
array_insert(mdd_t *, mddArray_top, i, result);
if(buildOnionRings)
array_insert(array_t*,toprings,i,arrayOfOnionRings);
}
}
mdd_free(result_ub);
/* Now attach the array to the ctlFormula */
ctlFormula->Bottomstates = mddArray_bot;
ctlFormula->Topstates = mddArray_top;
/* Discard previous copies. */
array_free(matchfound_bot);
array_free(matchelement_bot);
array_free(matchfound_top);
array_free(matchelement_top);
ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot);
ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot);
ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top);
ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top);
/* find out the leaves attached to this nodes.*/
leavesLeftArray = leftChild->leaves;
ctlFormula->leaves = array_dup(leavesLeftArray);
if (buildOnionRings) {
ctlFormula->BotOnionRings = botrings;
ctlFormula->TopOnionRings = toprings;
}
if(approx != NIL(mdd_t)) mdd_free(approx);
/* Can't combine under and overapprox */
if(!fixpoint && TRMinimization == Ctlp_Underapprox_c)
TRMinimization = Ctlp_Incomparable_c;
break;
}
case Ctlp_Init_c:
result = Fsm_FsmComputeInitialStates(modelFsm);
break;
default: fail("Encountered unknown type of CTL formula\n");
}
tmpMdd = mdd_dup(array_fetch(mdd_t *,mddArray_bot,0));
thisApproxType = ComputeResultingApproximation(
Ctlp_FormulaReadType(ctlFormula), leftApproxType,
rightApproxType, TRMinimization, earlyTermination, fixpoint);
Ctlp_FormulaSetApproxStates(ctlFormula,tmpMdd, TRMinimization);
#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);
return;
} /* ModelcheckAndVacuity */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void PrintVacuous | ( | mdd_t * | modelInitialStates, |
| Fsm_Fsm_t * | modelFsm, | ||
| Ctlp_Formula_t * | ctlFormula, | ||
| Mc_FwdBwdAnalysis | traversalDirection, | ||
| array_t * | modelCareStatesArray, | ||
| McOptions_t * | options, | ||
| Mc_VerbosityLevel | verbosity | ||
| ) | [static] |
Function********************************************************************
Synopsis [Prints results of vacuum cleaning for a passing CTL property.]
Description [For a passing CTL property reports all vacuous passes. If so requested, it also produces interesting witnesses, that is, computations of the model for which the original property holds non trivially. (Alternatively, the strengthened property that gave the vacuous pass fails.)]
SideEffects [none]
SeeAlso [McVacuityDetection PrintVacuousBottom]
Definition at line 498 of file mcVacuum.c.
{
Ctlp_Formula_t *formula,*Int_Wit_CtlFormula;
boolean vacuous = FALSE;
int i;
Ctlp_FormulaType type;
if (traversalDirection == McBwd_c) {
for (i=1;i<array_n(ctlFormula->Bottomstates);i++) {
formula = array_fetch(Ctlp_Formula_t *,ctlFormula->leaves,(i-1));
type = Ctlp_FormulaReadType(formula);
if (mdd_lequal(modelInitialStates, array_fetch(mdd_t *,ctlFormula->Bottomstates,i),1,1)) {
if((type != Ctlp_FALSE_c) && (type != Ctlp_TRUE_c)) {
fprintf(vis_stdout, "# MC: Vacuous pass : ");
Ctlp_FormulaPrint(vis_stdout, formula);
fprintf(vis_stdout, "\n");
vacuous = TRUE;
}
}
else { /* CounterExample Generation */
if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c){
fprintf(vis_stdout, "# MC: Not a vacuous pass : ");
Ctlp_FormulaPrint(vis_stdout, formula);
fprintf(vis_stdout, "\n");
fprintf(vis_stdout, "# Generating interesting witness :\n");
Int_Wit_CtlFormula = Ctlp_FormulaDup(ctlFormula);
CreateImportantWitness(ctlFormula,Int_Wit_CtlFormula,i);
McFsmDebugFormula(options,Int_Wit_CtlFormula,modelFsm,
modelCareStatesArray);
Ctlp_FormulaFree(Int_Wit_CtlFormula);
}
}
}
if (vacuous == FALSE){
(void)fprintf(vis_stdout, "# MC: No vacuous passes\n");
}
}
else{
(void)fprintf(vis_stderr, "# MC: Vacuity cannot be checked\n");
}
} /* PrintVacuous */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void PrintVacuousBottom | ( | mdd_t * | modelInitialStates, |
| Fsm_Fsm_t * | modelFsm, | ||
| Ctlp_Formula_t * | ctlFormula, | ||
| Mc_FwdBwdAnalysis | traversalDirection, | ||
| array_t * | modelCareStatesArray, | ||
| McOptions_t * | options, | ||
| Mc_VerbosityLevel | verbosity | ||
| ) | [static] |
Function********************************************************************
Synopsis [Prints results of vacuum cleaning for a failing CTL property.]
Description [For a failing CTL property reports all vacuous failures. If so requested, it also produces interesting counterexamples, that is, computations of the model for which even the weakened property fails.]
SideEffects [none]
SeeAlso [PrintVacuous]
Definition at line 438 of file mcVacuum.c.
{
Ctlp_Formula_t *formula,*Int_Counter_CtlFormula;
boolean vacuous = FALSE;
int i;
Ctlp_FormulaType type;
if (traversalDirection == McBwd_c){
for (i=1;i<array_n(ctlFormula->Topstates);i++){
if (!(mdd_lequal(modelInitialStates, array_fetch(mdd_t *,ctlFormula->Topstates,i),1,1))){
formula = array_fetch(Ctlp_Formula_t *,ctlFormula->leaves,(i-1));
type = Ctlp_FormulaReadType(formula);
if((type != Ctlp_FALSE_c) && (type != Ctlp_TRUE_c)) {
fprintf(vis_stdout, "# MC: Vacuous failure : ");
Ctlp_FormulaPrint(vis_stdout, formula);
fprintf(vis_stdout, "\n");
if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c){
fprintf(vis_stdout, "# Generating interesting counterexample :\n");
Int_Counter_CtlFormula = Ctlp_FormulaDup(ctlFormula);
CreateImportantCounterexample(ctlFormula,Int_Counter_CtlFormula,i);
McFsmDebugFormula(options,Int_Counter_CtlFormula,modelFsm,
modelCareStatesArray);
Ctlp_FormulaFree(Int_Counter_CtlFormula);
}
vacuous = TRUE;
}
}
}
if (vacuous == FALSE){
(void)fprintf(vis_stdout, "# MC: No vacuous failures\n");
}
}
else{
(void)fprintf(vis_stderr, "# MC: Vacuity can not be checked\n");
}
} /* PrintVacuousBottom */
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: mcVacuum.c,v 1.1 2005/05/13 05:54:05 fabio Exp $" [static] |
CFile***********************************************************************
FileName [mcVacuum.c]
PackageName [mc]
Synopsis [Functions for vacuity detection.]
Description [This file contains the functions implementing vacuity detection for CTL. A CTL formula passes vacuously if it can be strengthened by replacing subformulae by "bottom" (either TRUE or FALSE, depending on the negation parity) without changing the outcome of model checking. Likewise, a formula fails vacuously if it can be weakened by replacing subformulae by top (the negation of bottom) and still fail. Under the assumption that a formula is represented by a parse tree (as opposed to a more general parse DAG) each subformula has a given negation parity. Bottom stands for FALSE if the replaced subformula appears under an even number of negation; it stands for TRUE otherwise. Since all CTL operators besides neagtion are monotonically increasing in their operands, replacing a subformula with bottom result in a stronger property, that is, one that implies the original one. A dual argument applies to replacements with top.
This file contains two algorithms for CTL vacuity detection: The original one of Beer et al. (CAV97), and an extension of the thorough vacuity detection algorithm of Purandare and Somenzi (CAV2002), also known as "CTL vacuum cleaning."
The algorithm of Beer et al. applies to passing weak ACTL (w-ACTL) properties. Roughly speaking, in a w-ACTL property each binary opeartor has at least one child that is a propositional formula. A w-ACTL formula contains a unique smallest important subformula. This is replaced by bottom to produce a witness formula. If the witness formula passes, then the original formula passed vacuously; otherwise, the counterexample to the witness formula is an interesting witness to the original one.
The implementation of the CTL vacuum cleaning algorithm in this file applies to both passing and failing CTL properties. For each formula, replacement is attempted for all leaves, therefore identifying many more cases of vacuity. All the replacements are dealt with in one traversal of the parse tree of the formula, paying attention to combining the cases that produce identical sets of states. For this reason, thorough vacuity detection is usually much cheaper than running as many model checking experiments as there are leaves.]
Author [Mitra Purandare]
Copyright [Copyright (c) 2002-2005, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
Definition at line 101 of file mcVacuum.c.
