src/mc/mcGFP.c File Reference
#include "mcInt.h"
Include dependency graph for mcGFP.c:
Go to the source code of this file.
Data Structures | |
| struct | McGSHOpSetStruct |
Defines | |
| #define | GSHoperatorIsEX(op, set) ((op) == (array_n((set)->flags) - 1)) |
Typedefs | |
| typedef struct McGSHOpSetStruct | McGSHOpSet_t |
Functions | |
| static int PickOperatorForGSH | ARGS ((McGSHOpSet_t *set)) |
| static boolean ConvergedGSH | ARGS ((mdd_t *Z, mdd_t *zeta, int opIndex, McGSHOpSet_t *opSet, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, boolean *fixpoint)) |
| static McGSHOpSet_t *AllocOperatorSetGSH | ARGS ((int n, Mc_GSHScheduleType schedule)) |
| static boolean IsMemberOperatorSetGSH | ARGS ((McGSHOpSet_t *set, int opIndex)) |
| mdd_t * | McFsmEvaluateEGFormulaUsingGSH (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, Mc_GSHScheduleType schedule) |
| mdd_t * | McFsmEvaluateEHFormulaUsingGSH (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, Mc_GSHScheduleType schedule) |
| static int | PickOperatorForGSH (McGSHOpSet_t *set) |
| static boolean | ConvergedGSH (mdd_t *Z, mdd_t *zeta, int opIndex, McGSHOpSet_t *opSet, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, boolean *fixpoint) |
| static McGSHOpSet_t * | AllocOperatorSetGSH (int n, Mc_GSHScheduleType schedule) |
| static void | FreeOperatorSetGSH (McGSHOpSet_t *set) |
| static void | EmptyOperatorSetGSH (McGSHOpSet_t *set) |
| static boolean | IsMemberOperatorSetGSH (McGSHOpSet_t *set, int opIndex) |
| static int | SizeOperatorSetGSH (McGSHOpSet_t *set) |
| static int | PushOperatorSetGSH (McGSHOpSet_t *set, int opIndex) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mcGFP.c,v 1.10 2002/09/16 00:47:16 fabio Exp $" |
Define Documentation
| #define GSHoperatorIsEX | ( | op, | |
| set | |||
| ) | ((op) == (array_n((set)->flags) - 1)) |
Typedef Documentation
| typedef struct McGSHOpSetStruct McGSHOpSet_t |
Function Documentation
| static McGSHOpSet_t* AllocOperatorSetGSH | ( | int | n, |
| Mc_GSHScheduleType | schedule | ||
| ) | [static] |
Function********************************************************************
Synopsis [Creates a new operator set.]
Description [Creates a new operator set to hold n operators.]
SideEffects [None]
SeeAlso [McFsmEvaluateEGFormulaUsingGSH FreeOperatorSetGSH]
Definition at line 732 of file mcGFP.c.
{
int i;
McGSHOpSet_t *set = ALLOC(McGSHOpSet_t, 1);
array_t *flags = set->flags = array_alloc(int, n+1);
for (i = 0; i < n+1; i++) {
array_insert(int, flags, i, 0);
}
set->cnt = 0;
set->schedule = schedule;
if (set->schedule == McGSH_EL_c) {
set->last = n;
set->nextToLast = n - 1;
} else if (set->schedule == McGSH_EL1_c) {
set->last = n;
} else if (set->schedule == McGSH_EL2_c) {
set->last = 0;
} else if (set->schedule == McGSH_Budget_c) {
set->last = n;
set->nextToLast = n - 1;
set->exBudget = 1;
set->exCount = Img_GetNumberOfImageComputation(Img_Backward_c);
} else {
/* The random schedule has no history. Hence, this initialization is
* immaterial. */
set->last = 0;
}
return set;
} /* AllocOperatorSetGSH */
Here is the call graph for this function:
| static int SizeOperatorSetGSH ARGS | ( | (McGSHOpSet_t *set) | ) | [static] |
AutomaticStart
| static boolean ConvergedGSH ARGS | ( | (mdd_t *Z, mdd_t *zeta, int opIndex, McGSHOpSet_t *opSet, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, boolean *fixpoint) | ) | [static] |
| static int PushOperatorSetGSH ARGS | ( | (McGSHOpSet_t *set, int opIndex) | ) | [static] |
| static McGSHOpSet_t* AllocOperatorSetGSH ARGS | ( | (int n, Mc_GSHScheduleType schedule) | ) | [static] |
| static boolean ConvergedGSH | ( | mdd_t * | Z, |
| mdd_t * | zeta, | ||
| int | opIndex, | ||
| McGSHOpSet_t * | opSet, | ||
| array_t * | careStatesArray, | ||
| Mc_EarlyTermination_t * | earlyTermination, | ||
| boolean * | fixpoint | ||
| ) | [static] |
Function********************************************************************
Synopsis [Performs the convergence test for the GSH algorithm.]
Description [Performs the convergence test for the GSH algorithm. Returns TRUE if convergence is achived; FALSE otherwise.]
SideEffects [Updates the operator set. An operator is disabled after application if it is an EU, or if has caused no progress toward the fixpoint. If convergence is reached, ConvergedGSH sets the location pointed by parameter fixpoint to TRUE if a fixpoint was reached, or to FALSE if early termination occured.]
SeeAlso [McFsmEvaluateEGFormulaUsingGSH]
Definition at line 677 of file mcGFP.c.
{
boolean term_tautology = FALSE;
boolean term_fixpoint = FALSE;
boolean term_early = FALSE;
term_tautology = mdd_is_tautology(Z, 0);
if (!term_tautology)
term_fixpoint = mdd_equal_mod_care_set_array(Z, zeta, careStatesArray);
if (!term_tautology && !term_fixpoint)
term_early = McCheckEarlyTerminationForOverapprox(earlyTermination, Z,
careStatesArray);
if (term_tautology || term_early) {
if (fixpoint != NIL(boolean))
*fixpoint = term_tautology;
return TRUE;
} else if (term_fixpoint) {
if (PushOperatorSetGSH(opSet,opIndex) == SizeOperatorSetGSH(opSet)) {
if (fixpoint != NIL(boolean))
*fixpoint = TRUE;
return TRUE;
} else {
return FALSE;
}
} else {
EmptyOperatorSetGSH(opSet);
if (!GSHoperatorIsEX(opIndex,opSet)) {
/* The operator is an EU. Add to set. */
(void) PushOperatorSetGSH(opSet,opIndex);
}
return FALSE;
}
} /* ConvergedGSH */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void EmptyOperatorSetGSH | ( | McGSHOpSet_t * | set | ) | [static] |
Function********************************************************************
Synopsis [Empties an operator set.]
Description [Empties an operator set. This is done in the GSH algorithm when progress is made towards the fixpoint. The information about the last operator applied is unaffected.]
SideEffects [None]
SeeAlso [McFsmEvaluateEGFormulaUsingGSH]
Definition at line 802 of file mcGFP.c.
{
int i;
for (i = 0; i < array_n(set->flags); i++) {
array_insert(int, set->flags, i, 0);
}
set->cnt = 0;
return;
} /* EmptyOperatorSetGSH */
Here is the caller graph for this function:
| static void FreeOperatorSetGSH | ( | McGSHOpSet_t * | set | ) | [static] |
Function********************************************************************
Synopsis [Frees an operator set.]
Description [Frees an operator set.]
SideEffects [None]
SeeAlso [McFsmEvaluateEGFormulaUsingGSH AllocOperatorSetGSH]
Definition at line 778 of file mcGFP.c.
{
array_free(set->flags);
FREE(set);
return;
} /* FreeOperatorSetGSH */
Here is the caller graph for this function:
| static boolean IsMemberOperatorSetGSH | ( | McGSHOpSet_t * | set, |
| int | opIndex | ||
| ) | [static] |
Function********************************************************************
Synopsis [Checks for membership of an operator in a set.]
Description [Checks for membership of an operator in a set.]
SideEffects [None]
SeeAlso [McFsmEvaluateEGFormulaUsingGSH]
Definition at line 827 of file mcGFP.c.
{
return array_fetch(int, set->flags, opIndex);
} /* IsMemberOperatorSetGSH */
| mdd_t* McFsmEvaluateEGFormulaUsingGSH | ( | 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, | ||
| Mc_GSHScheduleType | schedule | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Evaluate states satisfying EG(invariantMdd), given a transition relation.]
Description [Evaluate states satisfying EG(invariantMdd) under Buechi fairness conditions, given a transition relation. Use the GSH (Generalized SCC Hull, Ravi et al., FMCAD00) algorithm restricted to backward operators. (We can mix forward and backward operators in language emptiness, but not in the EG computation.)]
SideEffects [If onionRingsArrayForDbg is not NULL on entry, leaves the onion rings of the EU computations in the array it points to. If fixpoint is not NULL, stores in the location pointed by it the information about the cause for termination. (That is, whether a fixpoint was reached or not.)]
SeeAlso [Mc_FsmEvaluateEGFormula]
Definition at line 129 of file mcGFP.c.
{
int i,n;
array_t *onionRings;
boolean useRings;
mdd_manager *mddManager;
mdd_t *mddOne;
mdd_t *iterate;
array_t *buechiFairness;
int nPreComps;
int nIterations;
McGSHOpSet_t *operatorSet;
/* Here's how the pOnionRingsArrayForDbg works. It is a pointer to
** an array of arrays of mdds. There is one entry for every
** fairness constraint, and this entry is the array of the onion
** rings of the EU computation that corresponds to this constraint.
** Every time the EU for a given constraint is recomputed, the
** corresponding array of rings is renewed. */
assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
*pOnionRingsArrayForDbg == NIL(array_t) ||
array_n(*pOnionRingsArrayForDbg) == 0);
useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
*pOnionRingsArrayForDbg != NIL(array_t));
/* Initialization. */
nIterations = 0;
nPreComps = Img_GetNumberOfImageComputation(Img_Backward_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 we wanted to test for
** early termination here, we should fix the onion rings. */
if (mdd_is_tautology(iterate, 0)) {
mdd_free(mddOne);
if (fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0);
return(iterate);
}
/* Read fairness constraints. */
buechiFairness = 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(buechiFairness);
mdd_free(iterate);
mdd_free(mddOne);
if (fixpoint != NIL(boolean)) *fixpoint = FALSE;
return NIL(mdd_t);
} else {
int j;
int numBuechi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
for (j = 0; j < numBuechi; j++) {
mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
careStatesArray, dcLevel);
array_insert_last(mdd_t *, buechiFairness, tmpMdd);
}
}
} else {
array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
}
/* Initialize set of disabled operators (to the empty set). */
n = array_n(buechiFairness);
operatorSet = AllocOperatorSetGSH(n, schedule);
/* Iterate until all operators disabled or early termination. */
while (TRUE) {
mdd_t *oldIterate = iterate;
int opIndex = PickOperatorForGSH(operatorSet);
nIterations++;
if (GSHoperatorIsEX(opIndex,operatorSet)) {
mdd_t *EX = Mc_FsmEvaluateEXFormula(modelFsm, oldIterate, mddOne,
careStatesArray, verbosity,
dcLevel);
iterate = mdd_and(EX, oldIterate, 1, 1);
mdd_free(EX);
} else {
mdd_t *Fi = array_fetch(mdd_t *, buechiFairness, opIndex);
mdd_t *target = mdd_and(Fi, iterate, 1, 1);
/* Dispose of the old set of onion rings for this fairness constraint
** if it exists, and allocate a fresh array for a new set of rings. */
if (useRings) {
if (opIndex < array_n(*pOnionRingsArrayForDbg)) {
onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
opIndex);
mdd_array_free(onionRings);
}
onionRings = array_alloc(mdd_t *, 0);
array_insert(array_t *, *pOnionRingsArrayForDbg, opIndex, onionRings);
}
iterate = Mc_FsmEvaluateEUFormula(modelFsm, oldIterate, target,
NIL(mdd_t), mddOne, careStatesArray,
MC_NO_EARLY_TERMINATION, NIL(array_t),
Mc_None_c, onionRings, verbosity,
dcLevel, NIL(boolean));
mdd_free(target);
}
if (ConvergedGSH(iterate, oldIterate, opIndex, operatorSet,
careStatesArray, earlyTermination, fixpoint)) {
mdd_free(oldIterate);
break;
}
mdd_free(oldIterate);
}
/* Free operator set. */
FreeOperatorSetGSH(operatorSet);
/* Sanity checks for onion rings and diagnostic prints. */
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 *, buechiFairness, i);
array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
i);
/* Early termination with random schedules may leave holes. */
if (onionRings == NIL(array_t)) continue;
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, "onion ring of last EU fails invariant\n");
}
}
}
}
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(mddManager, 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(mddManager, iterate,
Fsm_FsmReadPresentStateVars(modelFsm)));
}
fprintf(vis_stdout, "--EG: %d iterations, %d preimage computations\n",
nIterations,
Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
}
mdd_array_free(buechiFairness);
mdd_free(mddOne);
return iterate;
} /* McFsmEvaluateEGFormulaUsingGSH */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McFsmEvaluateEHFormulaUsingGSH | ( | 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, | ||
| Mc_GSHScheduleType | schedule | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying EH(invariantMdd), given a transition relation.]
Description [Evaluate states satisfying EH(invariantMdd) under Buechi fairness conditions, given a transition relation. Use the GSH (Generalized SCC Hull, Ravi et al., FMCAD00) algorithm restricted to forward operators. (We can mix forward and backward operators in language emptiness, but not in the EH computation.)]
SideEffects [If onionRingsArrayForDbg is not NULL on entry, leaves the onion rings of the ES computations in the array it points to. If fixpoint is not NULL, stores in the location pointed by it the information about the cause for termination. (That is, whether a fixpoint was reached or not.)]
SeeAlso [Mc_FsmEvaluateEHFormula]
Definition at line 345 of file mcGFP.c.
{
int i,n;
array_t *onionRings;
boolean useRings;
mdd_manager *mddManager;
mdd_t *mddOne;
mdd_t *iterate;
array_t *buechiFairness;
int nImgComps;
int nIterations;
McGSHOpSet_t *operatorSet;
/* Here's how the pOnionRingsArrayForDbg works. It is a pointer to
** an array of arrays of mdds. There is one entry for every
** fairness constraint, and this entry is the array of the onion
** rings of the ES computation that corresponds to this constraint.
** Every time the ES for a given constraint is recomputed, the
** corresponding array of rings is renewed. */
assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
*pOnionRingsArrayForDbg == NIL(array_t) ||
array_n(*pOnionRingsArrayForDbg) == 0);
useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
*pOnionRingsArrayForDbg != NIL(array_t));
/* Initialization. */
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. */
buechiFairness = 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(buechiFairness);
mdd_free(iterate);
mdd_free(mddOne);
if (fixpoint != NIL(boolean)) *fixpoint = FALSE;
return NIL(mdd_t);
} else {
int j;
int numBuechi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
for (j = 0; j < numBuechi; j++) {
mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
careStatesArray, dcLevel);
array_insert_last(mdd_t *, buechiFairness, tmpMdd);
}
}
} else {
array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
}
/* Initialize set of disabled operators (to the empty set). */
n = array_n(buechiFairness);
operatorSet = AllocOperatorSetGSH(n, schedule);
/* Iterate until all operators disabled or early termination. */
while (TRUE) {
mdd_t *oldIterate = iterate;
int opIndex = PickOperatorForGSH(operatorSet);
nIterations++;
if (GSHoperatorIsEX(opIndex,operatorSet)) {
mdd_t *EY = Mc_FsmEvaluateEYFormula(modelFsm, oldIterate, mddOne,
careStatesArray, verbosity,
dcLevel);
iterate = mdd_and(EY, oldIterate, 1, 1);
mdd_free(EY);
} else {
mdd_t *Fi = array_fetch(mdd_t *, buechiFairness, opIndex);
mdd_t *source = mdd_and(Fi, iterate, 1, 1);
/* Dispose of the old set of onion rings for this fairness constraint
** if it exists, and allocate a fresh array for a new set of rings. */
if (useRings) {
if (opIndex < array_n(*pOnionRingsArrayForDbg)) {
onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
opIndex);
mdd_array_free(onionRings);
}
onionRings = array_alloc(mdd_t *, 0);
array_insert(array_t *, *pOnionRingsArrayForDbg, opIndex, onionRings);
}
iterate = Mc_FsmEvaluateESFormula(modelFsm, oldIterate, source,
NIL(mdd_t), mddOne, careStatesArray,
MC_NO_EARLY_TERMINATION, NIL(array_t),
Mc_None_c, onionRings, verbosity,
dcLevel, NIL(boolean));
mdd_free(source);
}
if (ConvergedGSH(iterate, oldIterate, opIndex, operatorSet,
careStatesArray, earlyTermination, fixpoint)) {
mdd_free(oldIterate);
break;
}
mdd_free(oldIterate);
}
/* Free operator set. */
FreeOperatorSetGSH(operatorSet);
/* Sanity checks for onion rings and diagnostic prints. */
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 *, buechiFairness, i);
array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
i);
/* Early termination with random schedules may leave holes. */
if (onionRings == NIL(array_t)) continue;
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, "onion ring of last ES fails invariant\n");
}
}
}
}
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(mddManager, 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(mddManager, iterate,
Fsm_FsmReadPresentStateVars(modelFsm)));
}
fprintf(vis_stdout, "--EH: %d iterations, %d image computations\n",
nIterations,
Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
}
mdd_array_free(buechiFairness);
mdd_free(mddOne);
return iterate;
} /* McFsmEvaluateEHFormulaUsingGSH */
Here is the call graph for this function:
Here is the caller graph for this function:
| static int PickOperatorForGSH | ( | McGSHOpSet_t * | set | ) | [static] |
Function********************************************************************
Synopsis [Returns the next operator for the GSH algorithm.]
Description [Returns the next operator for the GSH algorithm.]
SideEffects [Updates the operator set.]
SeeAlso [McFsmEvaluateEGFormulaUsingGSH]
Definition at line 559 of file mcGFP.c.
{
int nop = array_n(set->flags);
int opIndex;
if (set->schedule == McGSH_EL_c) {
int exIndex = nop - 1;
if ((set->last != exIndex) && !array_fetch(int, set->flags, exIndex)) {
opIndex = exIndex;
} else {
if (set->last == exIndex) {
opIndex = (set->nextToLast + 1) % exIndex;
} else {
opIndex = (set->last + 1) % exIndex;
}
while (array_fetch(int, set->flags, opIndex))
opIndex = (opIndex + 1) % nop;
}
set->nextToLast = set->last;
} else if (set->schedule == McGSH_EL1_c) {
/* EL1 implements a round-robin policy. */
opIndex = (set->last + 1) % nop;
while (array_fetch(int, set->flags, opIndex))
opIndex = (opIndex + 1) % nop;
} else if (set->schedule == McGSH_EL2_c) {
/* EL2 differs from EL1 in that it repeats EX to convergence.
* We rely on the fact that EUs are always disabled after their
* application. */
opIndex = set->last;
while (array_fetch(int, set->flags, opIndex))
opIndex = (opIndex + 1) % nop;
} else if (set->schedule == McGSH_Budget_c) {
int exIndex = nop - 1;
int newCount = Img_GetNumberOfImageComputation(Img_Backward_c);
if (set->last == exIndex)
set->exBudget--;
else
set->exBudget += newCount - set->exCount;
set->exCount = newCount;
/* (void) printf("budget = %d\n", set->exBudget); */
if ((set->last != exIndex) && !array_fetch(int, set->flags, exIndex)) {
/* At least one EX after each EU, unless EX is disabled */
opIndex = exIndex;
set->nextToLast = set->last;
} else {
if (set->last == exIndex) {
if (set->exBudget > 0 && set->nextToLast == exIndex - 1) {
opIndex = exIndex;
} else {
opIndex = (set->nextToLast + 1) % exIndex;
set->nextToLast = set->last;
}
} else { /* EX is disabled */
opIndex = (set->last + 1) % exIndex;
set->nextToLast = set->last;
}
while (array_fetch(int, set->flags, opIndex))
opIndex = (opIndex + 1) % nop;
}
if (opIndex == 0)
set->exBudget = 0;
#if 0
opIndex = set->last;
if (opIndex == exIndex && set->exBudget == 0)
opIndex = 0;
while (array_fetch(int, set->flags, opIndex))
opIndex = (opIndex + 1) % nop;
#endif
} else {
/* The random schedule uses a rather primitive way of selecting a
* random integer. However, as long as the number of operators is
* small, the distribution is acceptably uniform even if we use
* mod to map the result of util_random to 0 ... nop-1. */
int exIndex = nop - 1;
long rn = util_random();
int exDisabled = array_fetch(int, set->flags, exIndex);
if ((!exDisabled) && ((rn & 1024) || (set->cnt == exIndex))) {
/* rn & 1024 should be true 50% of the times */
opIndex = exIndex;
} else {
int enabledEUs = exIndex - (set->cnt - exDisabled);
rn = rn % enabledEUs;
assert(0 <= rn && rn < exIndex);
for (opIndex = 0; TRUE; opIndex++) {
assert(opIndex < exIndex);
if (!array_fetch(int, set->flags, opIndex)) {
if (rn == 0) {
break;
} else {
rn--;
}
}
}
}
}
set->last = opIndex;
return opIndex;
} /* PickOperatorForGSH */
Here is the call graph for this function:
Here is the caller graph for this function:
| static int PushOperatorSetGSH | ( | McGSHOpSet_t * | set, |
| int | opIndex | ||
| ) | [static] |
Function********************************************************************
Synopsis [Adds an element to an operator set.]
Description [Adds an element to an operator set.]
SideEffects [None]
SeeAlso [McFsmEvaluateEGFormulaUsingGSH]
Definition at line 868 of file mcGFP.c.
{
assert(opIndex < array_n(set->flags));
array_insert(int, set->flags, opIndex, 1);
set->cnt++;
return set->cnt;
} /* PushOperatorSetGSH */
Here is the caller graph for this function:
| static int SizeOperatorSetGSH | ( | McGSHOpSet_t * | set | ) | [static] |
Function********************************************************************
Synopsis [Returns the cardinality of an operator set.]
Description [Returns the cardinality of an operator set.]
SideEffects [None]
SeeAlso [McFsmEvaluateEGFormulaUsingGSH]
Definition at line 848 of file mcGFP.c.
{
return array_n(set->flags);
} /* SizeOperatorSetGSH */
Here is the caller graph for this function:
