src/mc/mcGFP.c

Go to the documentation of this file.

#include "mcInt.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

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                                                        */
/*---------------------------------------------------------------------------*/

#define GSHoperatorIsEX(op,set) ((op) == (array_n((set)->flags) - 1))

/*---------------------------------------------------------------------------*/
/* 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));

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


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 */


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                                            */
/*---------------------------------------------------------------------------*/


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 */


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 */


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 */


static void
FreeOperatorSetGSH(
  McGSHOpSet_t *set)
{
  array_free(set->flags);
  FREE(set);
  return;

} /* FreeOperatorSetGSH */


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 */


static boolean
IsMemberOperatorSetGSH(
  McGSHOpSet_t *set,
  int opIndex)
{
  return array_fetch(int, set->flags, opIndex);

} /* IsMemberOperatorSetGSH */


static int
SizeOperatorSetGSH(
  McGSHOpSet_t *set)
{
  return array_n(set->flags);

} /* SizeOperatorSetGSH */


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 */