#include "fsmInt.h"

Include dependency graph for fsmFair.c:

Data Structures
struct	FairnessConjunctStruct
Typedefs
typedef struct FairnessConjunctStruct	FairnessConjunct_t
Functions
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)
Fsm_Fairness_t *	Fsm_FsmReadFairnessConstraint (Fsm_Fsm_t *fsm)
mdd_t *	Fsm_FsmReadFairnessStates (Fsm_Fsm_t *fsm)
mdd_t *	Fsm_FsmComputeFairStates (Fsm_Fsm_t fsm, array_t careSetArray, int verbosity, int dcLevel, Mc_GSHScheduleType schedule, Mc_FwdBwdAnalysis direction, boolean useEarlyTermination)
Ctlp_Formula_t *	Fsm_FairnessReadFinallyInfFormula (Fsm_Fairness_t *fairness, int i, int j)
Ctlp_Formula_t *	Fsm_FairnessReadGloballyInfFormula (Fsm_Fairness_t *fairness, int i, int j)
mdd_t *	Fsm_FairnessObtainFinallyInfMdd (Fsm_Fairness_t fairness, int i, int j, array_t careSetArray, Mc_DcLevel dcLevel)
mdd_t *	Fsm_FairnessObtainGloballyInfMdd (Fsm_Fairness_t fairness, int i, int j, array_t careSetArray, Mc_DcLevel dcLevel)
boolean	Fsm_FairnessTestIsStreett (Fsm_Fairness_t *fairness)
boolean	Fsm_FairnessTestIsBuchi (Fsm_Fairness_t *fairness)
int	Fsm_FairnessReadNumDisjuncts (Fsm_Fairness_t *fairness)
int	Fsm_FairnessReadNumConjunctsOfDisjunct (Fsm_Fairness_t *fairness, int i)
array_t *	Fsm_FsmReadDebugArray (Fsm_Fsm_t *fsm)
void	Fsm_FsmFairnessUpdate (Fsm_Fsm_t fsm, array_t formulaArray)
Fsm_Fairness_t *	FsmFsmCreateDefaultFairnessConstraint (Fsm_Fsm_t *fsm)
boolean	FsmFairnessConstraintIsDefault (Fsm_Fairness_t *fairness)
void	FsmFairnessFree (Fsm_Fairness_t *fairness)
Fsm_Fairness_t *	FsmFairnessAlloc (Fsm_Fsm_t *fsm)
void	FsmFairnessAddConjunct (Fsm_Fairness_t fairness, Ctlp_Formula_t finallyInf, Ctlp_Formula_t *globallyInf, int i, int j)
void	FsmFsmFairnessInfoUpdate (Fsm_Fsm_t fsm, mdd_t states, Fsm_Fairness_t constraint, array_t dbgArray)
Variables
static char rcsid[]	UNUSED = "$Id: fsmFair.c,v 1.28 2003/01/22 18:44:20 jinh Exp $"

Typedef Documentation

typedef struct FairnessConjunctStruct FairnessConjunct_t

Struct**********************************************************************

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

Function Documentation

static FairnessConjunct_t * FairnessReadConjunct	(	Fsm_Fairness_t *	fairness,
		int	i,
		int	j
	)		`[static]`

AutomaticStart

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]

Definition at line 833 of file fsmFair.c.

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

Here is the caller graph for this function:

mdd_t* Fsm_FairnessObtainFinallyInfMdd	(	Fsm_Fairness_t *	fairness,
		int	i,
		int	j,
		array_t *	careSetArray,
		Mc_DcLevel	dcLevel
	)

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]

Definition at line 345 of file fsmFair.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_t* Fsm_FairnessObtainGloballyInfMdd	(	Fsm_Fairness_t *	fairness,
		int	i,
		int	j,
		array_t *	careSetArray,
		Mc_DcLevel	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]

Definition at line 383 of file fsmFair.c.

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

}

Here is the call graph for this function:

Ctlp_Formula_t* Fsm_FairnessReadFinallyInfFormula	(	Fsm_Fairness_t *	fairness,
		int	i,
		int	j
	)

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]

Definition at line 283 of file fsmFair.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlp_Formula_t* Fsm_FairnessReadGloballyInfFormula	(	Fsm_Fairness_t *	fairness,
		int	i,
		int	j
	)

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]

Definition at line 312 of file fsmFair.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Fsm_FairnessReadNumConjunctsOfDisjunct	(	Fsm_Fairness_t *	fairness,
		int	i
	)

Function********************************************************************

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

SideEffects []

SeeAlso [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadNumDisjuncts]

Definition at line 486 of file fsmFair.c.

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

  return (array_n(disjunct));
}

Here is the caller graph for this function:

int Fsm_FairnessReadNumDisjuncts ( Fsm_Fairness_t * fairness )

Function********************************************************************

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

SideEffects []

SeeAlso [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadNumConjunctsOfDisjunct]

Definition at line 468 of file fsmFair.c.

{
  return (array_n(fairness->disjunctArray));
}

Here is the caller graph for this function:

boolean Fsm_FairnessTestIsBuchi ( Fsm_Fairness_t * fairness )

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]

Definition at line 434 of file fsmFair.c.

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

Here is the caller graph for this function:

boolean Fsm_FairnessTestIsStreett ( Fsm_Fairness_t * fairness )

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]

Definition at line 412 of file fsmFair.c.

{
  return (array_n(fairness->disjunctArray) == 1);
}

mdd_t* Fsm_FsmComputeFairStates	(	Fsm_Fsm_t *	fsm,
		array_t *	careSetArray,
		int	verbosity,
		int	dcLevel,
		Mc_GSHScheduleType	schedule,
		Mc_FwdBwdAnalysis	direction,
		boolean	useEarlyTermination
	)

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.

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]

Definition at line 159 of file fsmFair.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void Fsm_FsmFairnessUpdate	(	Fsm_Fsm_t *	fsm,
		array_t *	formulaArray
	)

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]

Definition at line 534 of file fsmFair.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* Fsm_FsmReadDebugArray ( Fsm_Fsm_t * fsm )

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]

Definition at line 515 of file fsmFair.c.

{
  return (fsm->fairnessInfo.dbgArray);
}

Here is the caller graph for this function:

Fsm_Fairness_t* Fsm_FsmReadFairnessConstraint ( Fsm_Fsm_t * fsm )

AutomaticEnd 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".

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.

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]

Definition at line 119 of file fsmFair.c.

{
  return (fsm->fairnessInfo.constraint);
}

Here is the caller graph for this function:

mdd_t* Fsm_FsmReadFairnessStates ( Fsm_Fsm_t * fsm )

Definition at line 126 of file fsmFair.c.

{
   return(fsm->fairnessInfo.states);
}

Here is the caller graph for this function:

void FsmFairnessAddConjunct	(	Fsm_Fairness_t *	fairness,
		Ctlp_Formula_t *	finallyInf,
		Ctlp_Formula_t *	globallyInf,
		int	i,
		int	j
	)

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]

Definition at line 714 of file fsmFair.c.

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

Here is the caller graph for this function:

Fsm_Fairness_t* FsmFairnessAlloc ( Fsm_Fsm_t * fsm )

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]

Definition at line 687 of file fsmFair.c.

{
  Fsm_Fairness_t *fairness = ALLOC(Fsm_Fairness_t, 1);

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

  return fairness;
}

Here is the caller graph for this function:

boolean FsmFairnessConstraintIsDefault ( Fsm_Fairness_t * 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]

Definition at line 605 of file fsmFair.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void FsmFairnessFree ( Fsm_Fairness_t * fairness )

Function********************************************************************

Synopsis [Frees a fairness constraint.]

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

SideEffects []

SeeAlso [FsmFairnessAlloc]

Definition at line 651 of file fsmFair.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Fsm_Fairness_t* FsmFsmCreateDefaultFairnessConstraint ( Fsm_Fsm_t * fsm )

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]

Definition at line 579 of file fsmFair.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void FsmFsmFairnessInfoUpdate	(	Fsm_Fsm_t *	fsm,
		mdd_t *	states,
		Fsm_Fairness_t *	constraint,
		array_t *	dbgArray
	)

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 []

Definition at line 784 of file fsmFair.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static mdd_t * FsmObtainStatesSatisfyingFormula	(	Fsm_Fsm_t *	fsm,
		Ctlp_Formula_t *	formula,
		array_t *	careSetArray,
		Mc_VerbosityLevel	verbosity,
		Mc_DcLevel	dcLevel
	)		`[static]`

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]

Definition at line 868 of file fsmFair.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

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

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]

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.]

Definition at line 39 of file fsmFair.c.

src/fsm/fsmFair.c File Reference

Data Structures

Typedefs

Functions

Variables

Typedef Documentation

Function Documentation

Variable Documentation