source: vis_dev/vis-2.3/src/fsm/fsmFair.c @ 33

/**CFile***********************************************************************

  FileName    [fsmFair.c]

  PackageName [fsm]

  Synopsis    [Implementation of fairness constraints data structure.]

  Description [Implementation of fairness constraints data structure.  The
  fairness constraint data structure has been defined to allow canonical
  fairness constraints.  However, presently, only Buchi constraints can be
  parsed, and the model checker can handle only Buchi constraints.]

  Author      [Tom Shiple and Adnan Aziz and Gitanjali Swamy]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

******************************************************************************/

#include "fsmInt.h"

static char rcsid[] UNUSED = "$Id: fsmFair.c,v 1.28 2003/01/22 18:44:20 jinh Exp $";

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


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/**Struct**********************************************************************

  Synopsis    [A leaf of the canonical fairness constraint structure.  The name
  is misleading: this is interpreted as (GF finallyinf + FG globallyInf), a
  disjunction.]

******************************************************************************/
typedef struct FairnessConjunctStruct {
  Ctlp_Formula_t *finallyInf;  /* states to visit infinitely often */
  Ctlp_Formula_t *globallyInf; /* states to visit almost always */
} FairnessConjunct_t;


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static FairnessConjunct_t * FairnessReadConjunct(Fsm_Fairness_t *fairness, int i, int j);
static mdd_t * FsmObtainStatesSatisfyingFormula(Fsm_Fsm_t *fsm, Ctlp_Formula_t *formula, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Returns the fairness constraint of an FSM.]

  Description [Returns the fairness constraint of an FSM.  This is stored as a
  "canonical fairness constraint", which is a formula of the form (OR_i (AND_j
  (F-inf S_ij + G-inf T_ij))). Each of the S_ij and T_ij are CTL formulas,
  representing a set of states in the FSM. F-inf means "globally finally", or
  "infinitely often"; G-inf means "finally globally" or "almost always".<p>

  Each (AND_j (F-inf S_ij + G-inf T_ij)) is referred to as a "disjunct", and
  each (F-inf S_ij + G-inf T_ij) is referred to as a "conjunct".  A Streett
  constraint has just one disjunct.  A Buchi constraint has just one disjunct,
  and each conjunct of this disjunct has a NULL G-inf condition.<p>

  By default, an FSM is always initialized with a single fairness constraint
  TRUE, indicating that all states are "accepting".]

  SideEffects []

  SeeAlso     [Fsm_FsmComputeFairStates Fsm_FairnessReadFinallyInfFormula
  Fsm_FairnessReadGloballyInfFormula]

******************************************************************************/
Fsm_Fairness_t *
Fsm_FsmReadFairnessConstraint(
  Fsm_Fsm_t *fsm)
{
  return (fsm->fairnessInfo.constraint);
}

mdd_t *
Fsm_FsmReadFairnessStates(Fsm_Fsm_t *fsm)
{
   return(fsm->fairnessInfo.states);
}


/**Function********************************************************************

  Synopsis    [Computes the set of fair states of an FSM.]

  Description [Computes the set of fair states of an FSM.  If there is a
  fairness constraint associated with the FSM, and the fair states have been
  previously computed, then a copy of the fair states is returned.  If none of
  the above is true, then the CTL model checker is called to compute the set of
  fair states, and a copy of this set is returned.  Also, if the CTL model
  checker is called, information is stored in the FSM for the purpose of
  debugging CTL formulas in the presence of a fairness constraint.  The second
  argument is an optional care set array; when this is used, the set of fair
  states returned is correct on the conjunction of the elements of the care set
  array.  If careSetArray is set to NIL(mdd_t), it is defaulted to a
  one-element array containing mdd_one.

  <p> Note that when an FSM is created, by default, there is a single fairness
  constraint TRUE, indicating that all states are "accepting".  In this case,
  this function will just return TRUE, which is correct assuming that there are
  no dead-end states.]

  SideEffects []

  SeeAlso     [Fsm_FsmReadFairnessConstraint]

******************************************************************************/
mdd_t *
Fsm_FsmComputeFairStates(
  Fsm_Fsm_t *fsm,
  array_t *careSetArray,
  int verbosity,
  int dcLevel,
  Mc_GSHScheduleType schedule,
  Mc_FwdBwdAnalysis direction,
  boolean useEarlyTermination)
{
  mdd_manager    *mddManager = Fsm_FsmReadMddManager(fsm);
  Fsm_Fairness_t *constraint = Fsm_FsmReadFairnessConstraint(fsm);

  assert(constraint != NIL(Fsm_Fairness_t));

  if (fsm->fairnessInfo.states != NIL(mdd_t)) {
    /* Already computed. */
    return mdd_dup(fsm->fairnessInfo.states);
  } else {
    /* Compute from scratch. */
    mdd_t   *fairStates;
    array_t *dbgArray = array_alloc(array_t *, 0);

    /* No or trivial fairness constraint */
    if (FsmFairnessConstraintIsDefault(constraint)) {
      array_t *onionRings;
      
      fairStates = mdd_one(mddManager);
      
      onionRings = array_alloc(mdd_t *, 1);
      array_insert_last(mdd_t *, onionRings, mdd_one(mddManager));
      array_insert_last(array_t *, dbgArray, onionRings);

      fsm->fairnessInfo.states = mdd_dup(fairStates);
      fsm->fairnessInfo.dbgArray = dbgArray;
    } else {
      mdd_t   *oneMdd = mdd_one(mddManager);
      array_t *tmpCareSetArray;

      if (careSetArray) {
        tmpCareSetArray = careSetArray;
      } else {
        /* oneMdd is default */
        tmpCareSetArray = array_alloc(mdd_t *, 0);
        array_insert_last(mdd_t *, tmpCareSetArray, oneMdd);
      }

      if (direction == McBwd_c) {
        mdd_t *initialStates;
        Mc_EarlyTermination_t *earlyTermination;
        int fixpoint = 1;
        
        if (useEarlyTermination == TRUE) {
          initialStates = Fsm_FsmComputeInitialStates(fsm);
          earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
        } else {
          initialStates = NIL(mdd_t);
          earlyTermination = MC_NO_EARLY_TERMINATION;
        }

        fairStates =
          Mc_FsmEvaluateEGFormula(fsm,
                                  oneMdd, NIL(mdd_t), oneMdd,
                                  constraint, tmpCareSetArray,
                                  earlyTermination, NIL(array_t),
                                  Mc_None_c, &dbgArray,
                                  (Mc_VerbosityLevel) verbosity,
                                  (Mc_DcLevel) dcLevel,
                                  &fixpoint, schedule);
        if (useEarlyTermination == TRUE) {
          Mc_EarlyTerminationFree(earlyTermination);
          mdd_free(initialStates);
        }
        if (!fixpoint) {
          int i;
          array_t *mddArray;
          arrayForEachItem(array_t *, dbgArray, i, mddArray) {
            mdd_array_free(mddArray);
          }
          array_free(dbgArray);
        } else {
          fsm->fairnessInfo.states = mdd_dup(fairStates);
          fsm->fairnessInfo.dbgArray = dbgArray;
        }
      } else {
        fairStates =
          Mc_FsmEvaluateEHFormula(fsm,
                                  oneMdd, NIL(mdd_t), oneMdd,
                                  constraint, tmpCareSetArray,
                                  MC_NO_EARLY_TERMINATION, NIL(array_t),
                                  Mc_None_c, NIL(array_t *),
                                  (Mc_VerbosityLevel) verbosity,
                                  (Mc_DcLevel) dcLevel,
                                  NIL(boolean), schedule);
        array_free(dbgArray);
      }
      if (tmpCareSetArray != careSetArray)
        array_free(tmpCareSetArray);
      mdd_free(oneMdd);
    }

    return fairStates;
  }/* compute from scratch*/
}


/**Function********************************************************************

  Synopsis    [Reads the finallyInf component of a leaf of a canonical fairness
  constraint.]

  Description [Reads the finallyInf component of the jth conjunct of the ith
  disjunct of a canonical fairness constraint (i and j start counting from
  0). This is CTL formula representing a set of states of an FSM; this formula
  is not necessarily in existential normal form. If there is no finallyInf
  component at this location, then a NULL formula is returned.  It is assumed
  that i and j are within bounds.]

  SideEffects []

  SeeAlso [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadGloballyInfFormula
  Fsm_FairnessReadFinallyInfMdd]

******************************************************************************/
Ctlp_Formula_t *
Fsm_FairnessReadFinallyInfFormula(
  Fsm_Fairness_t *fairness,
  int i,
  int j)
{
  FairnessConjunct_t *conjunct = FairnessReadConjunct(fairness, i, j);
  return (conjunct->finallyInf);
}


/**Function********************************************************************

  Synopsis    [Reads the globallyInf component of a leaf of a canonical fairness
  constraint.]

  Description [Reads the globallyInf component of the jth conjunct of the ith
  disjunct of a canonical fairness constraint (i and j start counting from
  0). This is CTL formula representing a set of states of an FSM; this formula
  is not necessarily in existential normal form. If there is no globallyInf
  component at this location, then a NULL formula is returned.  It is assumed
  that i and j are within bounds.]

  SideEffects []

  SeeAlso [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadFinallyInfFormula
  Fsm_FairnessReadGloballyInfMdd]

******************************************************************************/
Ctlp_Formula_t *
Fsm_FairnessReadGloballyInfFormula(
  Fsm_Fairness_t *fairness,
  int i,
  int j)
{
  FairnessConjunct_t *conjunct = FairnessReadConjunct(fairness, i, j);
  return (conjunct->globallyInf);
}

/**Function********************************************************************

  Synopsis [Obtains a copy of the MDD of the finallyInf component of a leaf of
  a canonical fairness constraint.]

  Description [Obtains a copy of the MDD of the finallyInf component of the
  jth conjunct of the ith disjunct of a canonical fairness constraint (i and j
  start counting from 0). This MDD represents the set of FSM states which
  satisfy the finallyInf formula.  This set is guaranteed to be correct on the
  set of reachable states.  If there is no finallyInf component at this
  location, then a NULL MDD is returned.  It is assumed that i and j are
  within bounds.  The first time this function is called with the given data,
  the CTL model checker is called to compute the set of states (with all
  states fair, and no fairness constraint); additional calls take constant
  time. It is the responsibililty of the calling function to free the returned
  mdd.]

  SideEffects []

  SeeAlso [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadFinallyInfFormula
  Fsm_FairnessReadGloballyInfMdd]

******************************************************************************/
mdd_t *
Fsm_FairnessObtainFinallyInfMdd(
  Fsm_Fairness_t *fairness,
  int i,
  int j,
  array_t *careSetArray,
  Mc_DcLevel dcLevel)
{
  Ctlp_Formula_t *formula = Fsm_FairnessReadFinallyInfFormula(fairness, i, j);
  /* hard code verbosity to Mc_VerbosityNone */
  return(FsmObtainStatesSatisfyingFormula(fairness->fsm, formula, careSetArray,
                                          McVerbosityNone_c, dcLevel));
}


/**Function********************************************************************

  Synopsis [Obtains a copy of the MDD of the globallyInf component of a leaf of
  a canonical fairness constraint.]

  Description [Obtains a copy of the MDD of the globallyInf component of the
  jth conjunct of the ith disjunct of a canonical fairness constraint (i and j
  start counting from 0). This MDD represents the set of FSM states which
  satisfy the globallyInf formula.  This set is guaranteed to be correct on
  the set of reachable states.  If there is no globallyInf component at this
  location, then a NULL MDD is returned.  It is assumed that i and j are
  within bounds. The first time this function is called with the given data,
  the CTL model checker is called to compute the set of states (with all
  states fair, and no fairness constraint); additional calls take constant
  time. It is the responsibililty of the calling function to free the returned
  mdd.]

  SideEffects []

  SeeAlso [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadGloballyInfFormula
  Fsm_FairnessReadFinallyInfMdd]

******************************************************************************/
mdd_t *
Fsm_FairnessObtainGloballyInfMdd(
  Fsm_Fairness_t *fairness,
  int i,
  int j,
  array_t *careSetArray,
  Mc_DcLevel dcLevel)
{
  Ctlp_Formula_t *formula = Fsm_FairnessReadGloballyInfFormula(fairness, i, j);
  /* hard code verbosity to Mc_VerbosityNone */
  return(FsmObtainStatesSatisfyingFormula(fairness->fsm, formula, careSetArray,
                                          McVerbosityNone_c, dcLevel));

}


/**Function********************************************************************

  Synopsis [Returns TRUE if fairness constraint is of type Streett.]

  Description [Returns TRUE if fairness constraint is of type Streett, else
  FALSE.  A Streett fairness constraint is a canonical fairness constraint,
  with one disjunct.]

  SideEffects []

  SeeAlso     [Fsm_FsmReadFairnessConstraint Fsm_FairnessTestIsBuchi]

******************************************************************************/
boolean
Fsm_FairnessTestIsStreett(
  Fsm_Fairness_t *fairness)
{
  return (array_n(fairness->disjunctArray) == 1);
}


/**Function********************************************************************

  Synopsis [Returns TRUE if fairness constraint is of type Buchi].

  Description [Returns TRUE if fairness constraint is of type Buchi, else
  FALSE.  A Buchi fairness constraint is a canonical fairness constraint, with
  one disjunct, where each conjunct has a NULL G-inf condition.  Note that a
  Buchi constraint is also a Streett constraint.]

  SideEffects []

  SeeAlso     [Fsm_FsmReadFairnessConstraint Fsm_FairnessTestIsStreet]

******************************************************************************/
boolean
Fsm_FairnessTestIsBuchi(
  Fsm_Fairness_t *fairness)
{
  if (array_n(fairness->disjunctArray) != 1) {
    return (FALSE);
  }
  else {
    int      j;
    array_t *disjunct = array_fetch(array_t *, fairness->disjunctArray, 0);

    for (j = 0; j < array_n(disjunct); j++) {
      FairnessConjunct_t *conjunct = array_fetch(FairnessConjunct_t *,
                                                 disjunct, j);
      if (conjunct->globallyInf != NIL(Ctlp_Formula_t)) {
        return (FALSE);
      }
    }
    return (TRUE);
  }
}


/**Function********************************************************************

  Synopsis    [Returns the number of disjuncts of a canonical fairness
  constraint.]

  SideEffects []

  SeeAlso     [Fsm_FsmReadFairnessConstraint
  Fsm_FairnessReadNumConjunctsOfDisjunct]

******************************************************************************/
int
Fsm_FairnessReadNumDisjuncts(
  Fsm_Fairness_t *fairness)
{
  return (array_n(fairness->disjunctArray));
}


/**Function********************************************************************

  Synopsis [Returns the number of conjuncts of the ith disjunct of a canonical
  fairness constraint.]

  SideEffects []

  SeeAlso     [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadNumDisjuncts]

******************************************************************************/
int
Fsm_FairnessReadNumConjunctsOfDisjunct(
  Fsm_Fairness_t *fairness,
  int i)
{
  array_t *disjunct = array_fetch(array_t *, fairness->disjunctArray, i);

  return (array_n(disjunct));
}


/**Function********************************************************************

  Synopsis    [Returns the fair CTL debugging information of an FSM.]

  Description [Returns the fair CTL debugging information of an FSM.
  Currently, the fairness constraints are limited to Buchi constraints. The
  return value is an array of array_t* of mdd_t*.  The returned array is of
  length k, where k is the number of Buchi constraints.  The ith element of
  the returned array is an array of MDDs giving the sequence of state sets
  that can reach the ith Buchi constraint.  In particular, the jth MDD of the
  ith array is the set of states that can reach the ith Buchi set in j or
  fewer steps (the 0th MDD is the ith Buchi set itself).]

  SideEffects []

  SeeAlso     [Fsm_FsmReadFairnessConstraint]

******************************************************************************/
array_t *
Fsm_FsmReadDebugArray(Fsm_Fsm_t *fsm)
{
  return (fsm->fairnessInfo.dbgArray);
}


/**Function********************************************************************

  Synopsis    [Create and Update the fairness constraint of the FSM.]

  Description [Given the FSM and an array of CTL formula, build the buechi
  fairness constraints, and update.]

  SideEffects []

  SeeAlso     [Fsm_FsmReadFairnessConstraint]

******************************************************************************/
void
Fsm_FsmFairnessUpdate(
  Fsm_Fsm_t *fsm,
  array_t *formulaArray)
{
    Fsm_Fairness_t *fairness = FsmFairnessAlloc(fsm);
    int j;
    /*
     * Interpret the array of CTL formulas as a set of Buchi conditions.
     * Hence, create a single disjunct, consisting of k conjuncts, where k is
     * the number of CTL formulas read in.  The jth conjunct has the jth
     * formula as its finallyInf component, and NULL as its globallyInf
     * component.
     */
    
    for (j = 0; j < array_n(formulaArray); j++) {
      Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, j);

      FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j);
    }

    /*
     * Remove any existing fairnessInfo associated with the FSM, and update
     * the fairnessInfo.constraint with the new fairness just read.
     */
    FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), fairness, NIL(array_t));
}


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

/**Function********************************************************************

  Synopsis    [Create a default fairness constraint.]

  Description [Create a default fairness constraint containing a single
  formula, TRUE, indicating that all states are "accepting".]

  SideEffects []

  SeeAlso     [Fsm_FsmReadFairnessConstraint]

******************************************************************************/
Fsm_Fairness_t *
FsmFsmCreateDefaultFairnessConstraint(
  Fsm_Fsm_t *fsm)
{
  Fsm_Fairness_t *fairness    = FsmFairnessAlloc(fsm);
  Ctlp_Formula_t *trueFormula = Ctlp_FormulaCreate(Ctlp_TRUE_c,
                                                   NIL(Ctlp_Formula_t),
                                                   NIL(Ctlp_Formula_t));

  FsmFairnessAddConjunct(fairness, trueFormula, NIL(Ctlp_Formula_t), 0, 0);
  return fairness;
}


/**Function********************************************************************

  Synopsis    [See whether the fairness constraint is the default one]

  Description [See if the fairness constraint is the default one, which implies
  that all states are accepting.]

  SideEffects []

  SeeAlso     [FsmFsmCreateDefaultFairnessConstraint]

******************************************************************************/
boolean
FsmFairnessConstraintIsDefault(
  Fsm_Fairness_t *fairness)
{
  array_t            *disjuncts;
  array_t            *conjuncts;
  FairnessConjunct_t *leaf;
  Ctlp_Formula_t     *tautology;
  boolean            result;
  
  /* one disjunct */
  disjuncts = fairness->disjunctArray;
  if(array_n(disjuncts) !=  1)
    return FALSE;

  /* one conjunct */
  conjuncts = array_fetch(array_t *, disjuncts, 0);
  if(array_n(conjuncts) != 1)
    return FALSE;

  /* set to (GF TRUE * FG NULL) */
  leaf = array_fetch(FairnessConjunct_t *, conjuncts, 0);
  if(leaf->globallyInf != NIL(Ctlp_Formula_t))
    return FALSE;

  tautology = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t),
                                 NIL(Ctlp_Formula_t));
  result = Ctlp_FormulaIdentical(tautology, leaf->finallyInf);
  Ctlp_FormulaFree(tautology);

  return result;
}


/**Function********************************************************************

  Synopsis    [Frees a fairness constraint.]

  Description [Frees all the memory associated with a fairness constraint,
  including the underlying CTL formulas.]

  SideEffects []

  SeeAlso     [FsmFairnessAlloc]

******************************************************************************/
void
FsmFairnessFree(
  Fsm_Fairness_t *fairness)
{
  int i;

  for (i = 0; i < array_n(fairness->disjunctArray); i++) {
    int j;
    array_t *disjunct = array_fetch(array_t *, fairness->disjunctArray, i);

    for (j = 0; j < array_n(disjunct); j++) {
      FairnessConjunct_t *conjunct = array_fetch(FairnessConjunct_t *,
                                                 disjunct, j);
      Ctlp_FormulaFree(conjunct->finallyInf);
      Ctlp_FormulaFree(conjunct->globallyInf);
      FREE(conjunct);
    }
    array_free(disjunct);
  }
  array_free(fairness->disjunctArray);
  FREE(fairness);
}


/**Function********************************************************************

  Synopsis    [Allocates a fairness constraint.]

  Description [Allocates a fairness constraint.  Sets the FSM pointer, and
  allocates a disjunct array containing 0 elements.]

  SideEffects []

  SeeAlso     [FsmFairnessFree FsmFairnessAddConjunct]

******************************************************************************/
Fsm_Fairness_t *
FsmFairnessAlloc(Fsm_Fsm_t *fsm)
{
  Fsm_Fairness_t *fairness = ALLOC(Fsm_Fairness_t, 1);

  fairness->fsm           = fsm;
  fairness->disjunctArray = array_alloc(array_t *, 0);

  return fairness;
}


/**Function********************************************************************

  Synopsis    [Adds a conjunct to a fairness constraint.]

  Description [Adds a conjunct to a fairness constraint. i and j must not be
  negative; otherwise, there is no restriction on their values.  i and j start
  counting from 0.  Note that it is possible to create a 2-D array with
  "holes" in it, although this is probably not desirable.  If holes are
  created, they are zeroed out.]

  SideEffects []

  SeeAlso     [FsmFairnessAlloc]

******************************************************************************/
void
FsmFairnessAddConjunct(
  Fsm_Fairness_t *fairness,
  Ctlp_Formula_t *finallyInf,
  Ctlp_Formula_t *globallyInf,
  int             i,
  int             j)
{
  int k;
  array_t *disjunct;
  int numConjuncts;
  int                 numDisjuncts = array_n(fairness->disjunctArray);
  FairnessConjunct_t *conjunct     = ALLOC(FairnessConjunct_t, 1);

  assert((i >= 0) && (j >= 0));

  /* Get the array for row i. */
  if (i >= numDisjuncts) {
    /*
     * i is out of range.  Create a new disjunct, add it to the array, and
     * zero out the intervening entries.
     */
    disjunct = array_alloc(FairnessConjunct_t *, 0);

    /* Note that the array is dynamically extended. */
    array_insert(array_t *, fairness->disjunctArray, i, disjunct);

    /* Zero out the holes just created (if any). */
    for (k = numDisjuncts; k < i; k++) {
      array_insert(array_t *, fairness->disjunctArray, k, NIL(array_t));
    }
  }
  else {
    /*
     * i is in range.  However, there may not be a non-NIL array at entry i
     * yet.
     */
    disjunct = array_fetch(array_t *, fairness->disjunctArray, i);
    if (disjunct == NIL(array_t)) {
      disjunct = array_alloc(FairnessConjunct_t *, 0);
      array_insert(array_t *, fairness->disjunctArray, i, disjunct);
    }
  }

  /*
   * Fill in the conjunct, and add it to the jth position of the ith row.  If
   * holes are created, then zero them out.
   */
  conjunct->finallyInf  = finallyInf;
  conjunct->globallyInf = globallyInf;

  array_insert(FairnessConjunct_t *, disjunct, j, conjunct);
  numConjuncts = array_n(disjunct);
  for (k = numConjuncts; k < j; k++) {
    array_insert(FairnessConjunct_t *, disjunct, k, NIL(FairnessConjunct_t));
  }
}


/**Function********************************************************************

  Synopsis    [Updates the fairnessInfo of an FSM.]

  Description [Updates the fairnessInfo of an FSM with the supplied arguments.
  If any of the existing fields are currently non-NULL, then first frees
  them. DbgArray is assumed to be an array of arrays of mdd_t's.]

  SideEffects []

******************************************************************************/
void
FsmFsmFairnessInfoUpdate(
  Fsm_Fsm_t *fsm,
  mdd_t *states,
  Fsm_Fairness_t *constraint,
  array_t *dbgArray)
{
  array_t *oldDbgArray = fsm->fairnessInfo.dbgArray;

  if (fsm->fairnessInfo.states != NIL(mdd_t)){
    mdd_free(fsm->fairnessInfo.states);
  }
  fsm->fairnessInfo.states = states;

  if (fsm->fairnessInfo.constraint != NIL(Fsm_Fairness_t)) {
    FsmFairnessFree(fsm->fairnessInfo.constraint);
  }
  fsm->fairnessInfo.constraint = constraint;

  if (oldDbgArray != NIL(array_t)) {
    int i;
    for (i = 0; i < array_n(oldDbgArray); i++) {
      array_t *mddArray = array_fetch(array_t *, oldDbgArray, i);
      mdd_array_free(mddArray);
    }
    array_free(oldDbgArray);
  }
  fsm->fairnessInfo.dbgArray = dbgArray;
}



/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Reads a leaf of a canonical fairness constraint.]

  Description [Reads the the jth conjunct of the ith disjunct of a canonical
  fairness constraint.  It is assumed that i and j are within bounds.]

  SideEffects []

  SeeAlso     [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadGloballyInfFormula
  Fsm_FairnessReadFinallyInfMdd]

******************************************************************************/
static FairnessConjunct_t *
FairnessReadConjunct(
  Fsm_Fairness_t *fairness,
  int i,
  int j)
{
  array_t            *disjunct;
  FairnessConjunct_t *conjunct;

  assert((i >= 0) && (i < array_n(fairness->disjunctArray)));
  disjunct = array_fetch(array_t *, fairness->disjunctArray, i);

  assert((j >= 0) && (j < array_n(disjunct)));
  conjunct = array_fetch(FairnessConjunct_t *, disjunct, j);

  return conjunct;
}


/**Function********************************************************************

  Synopsis    [Obtains the set of states satisfying a formula.]

  Description [Returns a copy of the set of states satisfying a CTL formula,
  in the context of an FSM.  If this set has already been computed for this
  formula, then a copy is returned.  Otherwise, the CTL model checker is
  called on the existential normal form of the formula, with all states fair,
  and no fairness constraint.  The result is guaranteed correct on reachable
  states.  If formula is NULL, then a NULL MDD is returned.]

  SideEffects []

  SeeAlso     [Fsm_FairnessObtainFinallyInfMdd Fsm_FairnessObtainGloballyInfMdd]

******************************************************************************/
static mdd_t *
FsmObtainStatesSatisfyingFormula(
  Fsm_Fsm_t      *fsm,
  Ctlp_Formula_t *formula,
  array_t *careSetArray,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  if (formula == NIL(Ctlp_Formula_t)) {
    return (NIL(mdd_t));
  }
  else {
    mdd_t *stateSet = Ctlp_FormulaObtainStates(formula);

    if (stateSet != NIL(mdd_t)) {
      return stateSet;
    }
    else {
      mdd_t          *result;
      mdd_manager    *mddManager  = Fsm_FsmReadMddManager(fsm);
      mdd_t          *oneMdd      = mdd_one(mddManager);
      Ctlp_Formula_t *convFormula =
                        Ctlp_FormulaConvertToExistentialForm(formula);

      /* Note that Mc_FsmEvaluateFormula returns a copy of the MDD. */
      result = Mc_FsmEvaluateFormula(fsm, convFormula, oneMdd,
                                     NIL(Fsm_Fairness_t),
                                     careSetArray,
                                     MC_NO_EARLY_TERMINATION,
                                     NIL(Fsm_HintsArray_t),
                                     Mc_None_c, verbosity, dcLevel, 0,
                                     McGSH_EL_c);
      mdd_free(oneMdd);

      /*
       * We must make a copy of the MDD for the return value.
       */
      Ctlp_FormulaSetStates(formula, result);
      stateSet = mdd_dup(result);

      Ctlp_FormulaFree(convFormula);

      return stateSet;
    }
  }
}