/**CFile*********************************************************************** FileName [mcGFP.c] PackageName [mc] Synopsis [Computation of greatest fixpoints.] Description [This file contains the functions implementing the Generalized SCC Hull algorithm (GSH) for language emptiness check and for the computation of the states satisfying an EG formula.] SeeAlso [mcMc.c] Author [Fabio Somenzi] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #include "mcInt.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Stucture declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [Structure to store disabled operators in GSH.] Description [Structure to store disabled operators in GSH. A disabled operator is one whose application is known not to cause any progress towards the fixpoint. When all operators are disabled, the computation has converged to the fixpoint. If there are n fairness constraints, the EU operators receive the indices from 0 to n-1, while the one EX is given index n.] ******************************************************************************/ struct McGSHOpSetStruct { array_t *flags; /* flag array for quick membership test */ int cnt; /* number of operators in set */ int last; /* last operator applied */ int nextToLast; /* next to last operator applied */ int exBudget; /* allowed number of EXs in budget schedule */ int exCount; /* EXs applied so far (EUs included) */ Mc_GSHScheduleType schedule; /* operator schedule */ }; /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef struct McGSHOpSetStruct McGSHOpSet_t; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ #ifndef lint static char rcsid[] UNUSED = "$Id: mcGFP.c,v 1.10 2002/09/16 00:47:16 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**Macro*********************************************************************** Synopsis [Returns TRUE if an operator of GSH is an EX.] SideEffects [none] ******************************************************************************/ #define GSHoperatorIsEX(op,set) ((op) == (array_n((set)->flags) - 1)) /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ 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 void FreeOperatorSetGSH ARGS((McGSHOpSet_t *set)); static void EmptyOperatorSetGSH ARGS((McGSHOpSet_t *set)); static boolean IsMemberOperatorSetGSH ARGS((McGSHOpSet_t *set, int opIndex)); static int SizeOperatorSetGSH ARGS((McGSHOpSet_t *set)); static int PushOperatorSetGSH ARGS((McGSHOpSet_t *set, int opIndex)); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**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] ******************************************************************************/ 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) { 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 */ /**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] ******************************************************************************/ 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) { 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 */ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**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] ******************************************************************************/ static int PickOperatorForGSH( McGSHOpSet_t *set) { 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 */ /**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] ******************************************************************************/ static boolean ConvergedGSH( mdd_t *Z /* new iterate */, mdd_t *zeta /* old iterate */, int opIndex /* operator that has been just applied */, McGSHOpSet_t *opSet /* set of disabled operators */, array_t *careStatesArray /* array for care states */, Mc_EarlyTermination_t *earlyTermination /* early termination criterion */, boolean *fixpoint /* reason for termination */) { 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 */ /**Function******************************************************************** Synopsis [Creates a new operator set.] Description [Creates a new operator set to hold n operators.] SideEffects [None] SeeAlso [McFsmEvaluateEGFormulaUsingGSH FreeOperatorSetGSH] ******************************************************************************/ static McGSHOpSet_t * AllocOperatorSetGSH( int n, Mc_GSHScheduleType schedule) { 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 */ /**Function******************************************************************** Synopsis [Frees an operator set.] Description [Frees an operator set.] SideEffects [None] SeeAlso [McFsmEvaluateEGFormulaUsingGSH AllocOperatorSetGSH] ******************************************************************************/ static void FreeOperatorSetGSH( McGSHOpSet_t *set) { array_free(set->flags); FREE(set); return; } /* FreeOperatorSetGSH */ /**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] ******************************************************************************/ static void EmptyOperatorSetGSH( McGSHOpSet_t *set) { int i; for (i = 0; i < array_n(set->flags); i++) { array_insert(int, set->flags, i, 0); } set->cnt = 0; return; } /* EmptyOperatorSetGSH */ /**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] ******************************************************************************/ static boolean IsMemberOperatorSetGSH( McGSHOpSet_t *set, int opIndex) { return array_fetch(int, set->flags, opIndex); } /* IsMemberOperatorSetGSH */ /**Function******************************************************************** Synopsis [Returns the cardinality of an operator set.] Description [Returns the cardinality of an operator set.] SideEffects [None] SeeAlso [McFsmEvaluateEGFormulaUsingGSH] ******************************************************************************/ static int SizeOperatorSetGSH( McGSHOpSet_t *set) { return array_n(set->flags); } /* SizeOperatorSetGSH */ /**Function******************************************************************** Synopsis [Adds an element to an operator set.] Description [Adds an element to an operator set.] SideEffects [None] SeeAlso [McFsmEvaluateEGFormulaUsingGSH] ******************************************************************************/ static int PushOperatorSetGSH( McGSHOpSet_t *set, int opIndex) { assert(opIndex < array_n(set->flags)); array_insert(int, set->flags, opIndex, 1); set->cnt++; return set->cnt; } /* PushOperatorSetGSH */