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] ******************************************************************************/ 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.
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; } } }