src/fsm/fsmFair.c

Go to the documentation of this file.

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

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


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

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

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);
}


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


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


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

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));
}


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

}


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


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);
  }
}


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


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

  return (array_n(disjunct));
}


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


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

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;
}


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;
}


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);
}


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;
}


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));
  }
}


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

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;
}


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;
    }
  }
}