maxNumberOfSCCs
controls the enumeration. If its value is 0, all fair SCCs are
enumerated; if it is negative, early termination is applied, and at
most one fair SCC is computed. Finally, if
maxNumberOfSCCs is a positive integer n,
then exactly n fair SCCs are computed.]
SideEffects [Returns an array with one SCC per entry as side
effect. May update reachability information.]
SeeAlso []
******************************************************************************/
mdd_t *
McFsmComputeFairSCCsByLockStep(
Fsm_Fsm_t *fsm,
int maxNumberOfSCCs,
array_t *SCCs,
array_t *onionRingsArrayForDbg,
Mc_VerbosityLevel verbosity,
Mc_DcLevel dcLevel)
{
Mc_SccGen_t *sccGen;
mdd_t *mddOne, *reached, *hull, *scc, *fairStates;
array_t *onionRings, *sccClosedSetArray, *careStatesArray;
mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
Fsm_Fairness_t *modelFairness = Fsm_FsmReadFairnessConstraint(fsm);
array_t *buechiFairness = array_alloc(mdd_t *, 0);
/* Initialization. */
mddOne = mdd_one(mddManager);
sccClosedSetArray = array_alloc(mdd_t *, 0);
reached = Fsm_FsmComputeReachableStates(fsm, 0, verbosity, 0, 0, 1, 0, 0,
Fsm_Rch_Default_c, 0, 0,
NIL(array_t), FALSE, NIL(array_t));
array_insert_last(mdd_t *, sccClosedSetArray, reached);
onionRings = Fsm_FsmReadReachabilityOnionRings(fsm);
careStatesArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, careStatesArray, reached);
Img_MinimizeTransitionRelation(Fsm_FsmReadOrCreateImageInfo(fsm, 1, 1),
careStatesArray, Img_DefaultMinimizeMethod_c,
Img_Both_c, FALSE);
/* Read fairness constraints. */
if (modelFairness != NIL(Fsm_Fairness_t)) {
if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
(void) fprintf(vis_stdout,
"** mc error: non-Buechi fairness constraints not supported\n");
array_free(buechiFairness);
return NIL(mdd_t);
} else {
int j;
int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
for (j = 0; j < numBuchi; j++) {
mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
careStatesArray,
dcLevel);
array_insert_last(mdd_t *, buechiFairness, tmpMdd);
}
}
} else {
array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
}
/* Enumerate the fair SCCs and accumulate their disjunction in hull. */
hull = mdd_zero(mddManager);
Mc_FsmForEachFairScc(fsm, sccGen, scc, sccClosedSetArray, NIL(array_t),
buechiFairness, onionRings,
maxNumberOfSCCs == MC_LOCKSTEP_EARLY_TERMINATION,
verbosity, dcLevel) {
mdd_t *tmp = mdd_or(hull, scc, 1, 1);
mdd_free(hull);
hull = tmp;
array_insert_last(mdd_t *, SCCs, scc);
if (maxNumberOfSCCs > MC_LOCKSTEP_ALL_SCCS &&
array_n(SCCs) == maxNumberOfSCCs) {
Mc_FsmSccGenFree(sccGen, NIL(array_t));
break;
}
}
/* Compute (subset of) fair states and onion rings. */
if (onionRingsArrayForDbg != NIL(array_t)) {
mdd_t *fairSet;
int i;
fairStates = Mc_FsmEvaluateEUFormula(fsm, reached, hull,
NIL(mdd_t), mddOne, careStatesArray,
MC_NO_EARLY_TERMINATION,
NIL(array_t), Mc_None_c, NIL(array_t),
verbosity, dcLevel, NIL(boolean));
arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
mdd_t *restrictedFairSet = mdd_and(fairSet, hull, 1, 1);
array_t *setOfRings = array_alloc(mdd_t *, 0);
mdd_t *EU = Mc_FsmEvaluateEUFormula(fsm, fairStates, restrictedFairSet,
NIL(mdd_t), mddOne, careStatesArray,
MC_NO_EARLY_TERMINATION,
NIL(array_t), Mc_None_c, setOfRings,
verbosity, dcLevel, NIL(boolean));
array_insert_last(array_t *, onionRingsArrayForDbg, setOfRings);
mdd_free(restrictedFairSet);
mdd_free(EU);
}
} else {
fairStates = mdd_dup(hull);
}
if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
fprintf(vis_stdout,
"--Fair States: %d image computations, %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
}
/* Clean up. */
array_free(sccClosedSetArray);
mdd_free(reached);
mdd_free(hull);
mdd_free(mddOne);
array_free(careStatesArray);
mdd_array_free(buechiFairness);
return fairStates;
} /* McFsmComputeFairSCCsByLockStep */
/**Function********************************************************************
Synopsis [Computes fair SCCs of an FSM within SCC-closed sets.]
Description [Same as McFsmComputeFairSCCsByLockStep, except that the
fair SCCs returned are within the given array of SCC-closed sets.]
SideEffects [Returns an array with one SCC per entry as side
effect. May update reachability information.]
SeeAlso [McFsmComputeFairSCCsByLockStep]
******************************************************************************/
mdd_t *
McFsmRefineFairSCCsByLockStep(
Fsm_Fsm_t *fsm,
int maxNumberOfSCCs,
array_t *SCCs,
array_t *sccClosedSets,
array_t *careStates,
array_t *onionRingsArrayForDbg,
Mc_VerbosityLevel verbosity,
Mc_DcLevel dcLevel)
{
Mc_SccGen_t *sccGen;
mdd_t *mddOne, *reached, *hull, *scc, *fairStates;
array_t *onionRings, *careStatesArray, *sccClosedSetArray;
mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
Fsm_Fairness_t *modelFairness = Fsm_FsmReadFairnessConstraint(fsm);
array_t *buechiFairness = array_alloc(mdd_t *, 0);
/* Initialization. */
mddOne = mdd_one(mddManager);
if (careStates == NIL(array_t)) {
reached = Fsm_FsmComputeReachableStates(fsm, 0, verbosity, 0, 0, 1, 0, 0,
Fsm_Rch_Default_c, 0, 0,
NIL(array_t), FALSE, NIL(array_t));
careStatesArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, careStatesArray, mdd_dup(reached));
}else {
reached = McMddArrayAnd(careStates);
careStatesArray = mdd_array_duplicate(careStates);
}
onionRings = Fsm_FsmReadReachabilityOnionRings(fsm);
if (onionRings == NIL(array_t)) {
onionRings = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, onionRings, mdd_dup(mddOne));
}else
onionRings = mdd_array_duplicate(onionRings);
if (sccClosedSets == NIL(array_t)) {
sccClosedSetArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, sccClosedSetArray, mdd_dup(reached));
}else {
if (careStates != NIL(array_t))
sccClosedSetArray = mdd_array_duplicate(sccClosedSets);
else {
mdd_t *mdd1, *mdd2;
int i;
sccClosedSetArray = array_alloc(mdd_t *, 0);
arrayForEachItem(mdd_t *, sccClosedSets, i, mdd1) {
mdd2 = mdd_and(mdd1, reached, 1, 1);
if (mdd_is_tautology(mdd2, 0))
mdd_free(mdd2);
else
array_insert_last(mdd_t *, sccClosedSetArray, mdd2);
}
}
}
Img_MinimizeTransitionRelation(Fsm_FsmReadOrCreateImageInfo(fsm, 1, 1),
careStatesArray, Img_DefaultMinimizeMethod_c,
Img_Both_c, FALSE);
/* Read fairness constraints. */
if (modelFairness != NIL(Fsm_Fairness_t)) {
if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
(void) fprintf(vis_stdout,
"** mc error: non-Buechi fairness constraints not supported\n");
array_free(buechiFairness);
mdd_array_free(sccClosedSetArray);
mdd_array_free(onionRings);
mdd_array_free(careStatesArray);
mdd_free(reached);
return NIL(mdd_t);
} else {
int j;
int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
for (j = 0; j < numBuchi; j++) {
mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
careStatesArray,
dcLevel);
array_insert_last(mdd_t *, buechiFairness, tmpMdd);
}
}
} else {
array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
}
/* Enumerate the fair SCCs and accumulate their disjunction in hull. */
hull = mdd_zero(mddManager);
Mc_FsmForEachFairScc(fsm, sccGen, scc, sccClosedSetArray, NIL(array_t),
buechiFairness, onionRings,
maxNumberOfSCCs == MC_LOCKSTEP_EARLY_TERMINATION,
verbosity, dcLevel) {
mdd_t *tmp = mdd_or(hull, scc, 1, 1);
mdd_free(hull);
hull = tmp;
array_insert_last(mdd_t *, SCCs, scc);
if (maxNumberOfSCCs > MC_LOCKSTEP_ALL_SCCS &&
array_n(SCCs) == maxNumberOfSCCs) {
Mc_FsmSccGenFree(sccGen, NIL(array_t));
break;
}
}
/* Compute (subset of) fair states and onion rings. */
if (onionRingsArrayForDbg != NIL(array_t)) {
mdd_t *fairSet;
int i;
fairStates = Mc_FsmEvaluateEUFormula(fsm, reached, hull,
NIL(mdd_t), mddOne, careStatesArray,
MC_NO_EARLY_TERMINATION,
NIL(array_t), Mc_None_c, NIL(array_t),
verbosity, dcLevel, NIL(boolean));
arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
mdd_t *restrictedFairSet = mdd_and(fairSet, hull, 1, 1);
array_t *setOfRings = array_alloc(mdd_t *, 0);
mdd_t *EU = Mc_FsmEvaluateEUFormula(fsm, fairStates, restrictedFairSet,
NIL(mdd_t), mddOne, careStatesArray,
MC_NO_EARLY_TERMINATION,
NIL(array_t), Mc_None_c, setOfRings,
verbosity, dcLevel, NIL(boolean));
array_insert_last(array_t *, onionRingsArrayForDbg, setOfRings);
mdd_free(restrictedFairSet);
mdd_free(EU);
}
} else {
fairStates = mdd_dup(hull);
}
if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
fprintf(vis_stdout,
"--Fair States: %d image computations, %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
}
/* Clean up. */
mdd_array_free(sccClosedSetArray);
mdd_free(reached);
mdd_free(hull);
mdd_free(mddOne);
mdd_array_free(careStatesArray);
mdd_array_free(buechiFairness);
return fairStates;
} /* McFsmRefineFairSCCsByLockStep */
/**Function********************************************************************
Synopsis [Computes one fair SCC of an FSM, by LinearStep.]
Description [Computes one fair SCC of the state transition graph of
an FSM. Returns the fair SCC if one exists; NULL otherwise. This
function uses the linear steps SCC enumeration algorithm of
Gentilini, Piazza, and Policriti, "Computing strongly connected
components in a linear number of symbolic steps," and with the
addition of an early termination test.On input, the heap is supposed to contain a set of SCC-closed state sets together with their spine-sets. If earlyTermination is requested, the heap is left in an inconsistent state; otherwise, it contains a set of SCC-closed sets that contains all fair SCCs that were on the heap on input, except the one that has been enumerated. The number of sets may be different, and some non-fair SCCs may no longer be present.
The onionRing parameter is an array of state sets that is used to pick a seed close to a target. Typically, these onion rings come from reachability analysis. The target states in this case are the initial states of the FSM, and the objective of choosing a seed close to them is to reduce the length of the stem of a counterexample in the language emptiness check. However, any collection of sets that together cover all the states on the heap will work. If one is not concerned with a specific target, but rather with speed, then passing an array with just one component set to the constant one is preferable.] SideEffects [Updates the priority queue. The number of SCC examined (i.e., the number of chosen seeds) is added to sccExamined.] SeeAlso [Mc_FsmForEachFairScc] ******************************************************************************/ mdd_t * McFsmComputeOneFairSccByLinearStep( Fsm_Fsm_t *fsm, Heap_t *priorityQueue, array_t *buechiFairness, array_t *onionRings, boolean earlyTermination, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int *sccExamined) { mdd_t *mddOne, *SCC = NIL(mdd_t); mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); array_t *careStatesArray = array_alloc(mdd_t *, 0); int totalSCCs = 0; boolean foundScc = FALSE; array_t *activeFairness = NIL(array_t); int firstActive = 0; gns_t *gns; /* Initialization. */ mddOne = mdd_one(mddManager); array_insert(mdd_t *, careStatesArray, 0, mddOne); while (Heap_HeapCount(priorityQueue)) { mdd_t *V, *F, *fFront, *bFront, *fairSet; mdd_t *S, *NODE, *newS, *newNODE, *preNODE; long ringIndex; int retval UNUSED = Heap_HeapExtractMin(priorityQueue, &gns, &ringIndex); assert(retval && ringIndex < array_n(onionRings)); /* Extract the SCC-closed set, together with its spine-set */ V = gns->states; S = gns->spine; NODE = gns->node; FREE(gns); /* Determine the seed for which the SCC is computed */ if (mdd_is_tautology(S, 0) ) { assert( mdd_is_tautology(NODE, 0) ); mdd_free(NODE); NODE = LockstepPickSeed(fsm, V, buechiFairness, onionRings, ringIndex); } if (earlyTermination == TRUE) { int i; activeFairness = array_alloc(mdd_t *, 0); for (i = 0; i < array_n(buechiFairness); i++) { mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i); if (!mdd_lequal(NODE, fairSet, 1, 1)) { array_insert_last(mdd_t *, activeFairness, fairSet); } } } /* Compute the forward-set of seed, together with a new spine-set */ { array_t *newCareStatesArray = array_alloc(mdd_t *, 0); array_t *stack = array_alloc(mdd_t *, 0); mdd_t *tempMdd, *tempMdd2; int i; /* (1) Compute the forward-set, and push it onto STACK */ F = mdd_zero(mddManager); fFront = mdd_dup(NODE); while (!mdd_is_tautology(fFront, 0)) { array_insert_last(mdd_t *, stack, mdd_dup(fFront)); tempMdd = F; F = mdd_or(F, fFront, 1, 1); mdd_free(tempMdd); tempMdd = Mc_FsmEvaluateEYFormula(fsm, fFront, mddOne, careStatesArray, verbosity, dcLevel); mdd_free(fFront); tempMdd2 = mdd_and(tempMdd, V, 1, 1); mdd_free(tempMdd); fFront = mdd_and(tempMdd2, F, 1, 0); mdd_free(tempMdd2); } mdd_free(fFront); /* (2) Determine a spine-set of the forward-set */ i = array_n(stack) - 1; fFront = array_fetch(mdd_t *, stack, i); newNODE = Mc_ComputeAState(fFront, fsm); mdd_free(fFront); newS = mdd_dup(newNODE); while (i > 0) { fFront = array_fetch(mdd_t *, stack, --i); /* Chao: The use of DCs here may slow down the computation, * even though it reduces the peak BDD size */ /* array_insert(mdd_t *, newCareStatesArray, 0, fFront); */ array_insert(mdd_t *, newCareStatesArray, 0, mddOne); tempMdd = Mc_FsmEvaluateEXFormula(fsm, newS, mddOne, newCareStatesArray, verbosity, dcLevel); tempMdd2 = mdd_and(tempMdd, fFront, 1, 1); mdd_free(tempMdd); mdd_free(fFront); tempMdd = Mc_ComputeAState(tempMdd2, fsm); mdd_free(tempMdd2); tempMdd2 = newS; newS = mdd_or(newS, tempMdd, 1, 1); mdd_free(tempMdd2); mdd_free(tempMdd); } array_free(stack); array_free(newCareStatesArray); } /* now, we have {F, newS, newNODE} */ /* Determine the SCC containing NODE */ SCC = mdd_dup(NODE); bFront = mdd_dup(NODE); while (1) { mdd_t *tempMdd, *tempMdd2; if (earlyTermination == TRUE) { mdd_t * meet = mdd_and(SCC, NODE, 1, 0); if (!mdd_is_tautology(meet, 0)) { assert(mdd_lequal(meet, V, 1, 1)); for ( ; firstActive < array_n(activeFairness); firstActive++) { mdd_t *fairSet = array_fetch(mdd_t *, activeFairness, firstActive); if (mdd_lequal(meet, fairSet, 1, 0)) break; } mdd_free(meet); if (firstActive == array_n(activeFairness)) { int i; (void) fprintf(vis_stdout, "EARLY TERMINATION!\n"); totalSCCs++; /* Trim fair sets to guarantee counterexample will go through * this SCC. */ for (i = 0; i < array_n(buechiFairness); i++) { mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i); mdd_t *trimmed = mdd_and(fairSet, SCC, 1, 1); mdd_free(fairSet); array_insert(mdd_t *, buechiFairness, i, trimmed); } mdd_free(bFront); mdd_free(F); mdd_free(V); mdd_free(S); mdd_free(NODE); mdd_free(newS); mdd_free(newNODE); array_free(activeFairness); foundScc = TRUE; goto cleanUp; } } mdd_free(meet); } tempMdd = Mc_FsmEvaluateEXFormula(fsm, bFront, mddOne, careStatesArray, verbosity, dcLevel); tempMdd2 = mdd_and(tempMdd, F, 1, 1); mdd_free(tempMdd); tempMdd = bFront; bFront = mdd_and(tempMdd2, SCC, 1, 0); mdd_free(tempMdd2); mdd_free(tempMdd); if (mdd_is_tautology(bFront, 0)) break; tempMdd = SCC; SCC = mdd_or(SCC, bFront, 1, 1); mdd_free(tempMdd); } mdd_free(bFront); totalSCCs++; preNODE = Mc_FsmEvaluateEYFormula(fsm, NODE, mddOne, careStatesArray, verbosity, dcLevel); /* Check for fairness. If SCC is a trival SCC, skip the check */ if ( !mdd_equal(SCC, NODE) || mdd_lequal(NODE, preNODE, 1, 1) ) { /* Check fairness constraints. */ int i; arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) { if (mdd_lequal(SCC, fairSet, 1, 0)) break; } if (i == array_n(buechiFairness)) { /* All fairness iconditions intersected. We have a fair SCC. */ if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { array_t *PSvars = Fsm_FsmReadPresentStateVars(fsm); fprintf(vis_stdout, "--linearSCC: found a fair SCC with %.0f states\n", mdd_count_onset(mddManager, SCC, PSvars)); /* (void) bdd_print_minterm(SCC); */ } foundScc = TRUE; } } mdd_free(preNODE); mdd_free(NODE); /* Divide the remaining states of V into V minus * the forward set F, and the rest (minus the fair SCC). Add the two * sets thus obtained to the priority queue. */ { mdd_t *V1, *S1, *NODE1; mdd_t *tempMdd, *tempMdd2; V1 = mdd_and(V, F, 1, 0); S1 = mdd_and(S, SCC, 1, 0); tempMdd = mdd_and(SCC, S, 1, 1); tempMdd2 = Mc_FsmEvaluateEXFormula(fsm, tempMdd, mddOne, careStatesArray, verbosity, dcLevel); mdd_free(tempMdd); NODE1 = mdd_and(tempMdd2, S1, 1, 1); mdd_free(tempMdd2); LinearstepQueueEnqueue(fsm, priorityQueue, V1, S1, NODE1, onionRings, McLS_G_c, buechiFairness, verbosity, dcLevel); V1 = mdd_and(F, SCC, 1, 0); S1 = mdd_and(newS, SCC, 1, 0); NODE1 = mdd_and(newNODE, SCC, 1, 0); LinearstepQueueEnqueue(fsm, priorityQueue, V1, S1, NODE1, onionRings, McLS_H_c, buechiFairness, verbosity, dcLevel); } mdd_free(F); mdd_free(V); mdd_free(S); mdd_free(newS); mdd_free(newNODE); if (foundScc == TRUE) break; mdd_free(SCC); } cleanUp: mdd_free(mddOne); array_free(careStatesArray); if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "--linearSCC: found %s fair SCC out of %d examined\n", foundScc ? "one" : "no", totalSCCs); fprintf(vis_stdout, "--linearSCC: %d image computations, %d preimage computations\n", Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps, Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); } *sccExamined += totalSCCs; return foundScc ? SCC : NIL(mdd_t); } /* McFsmComputeOneFairSccByLinearStep */ /**Function******************************************************************** Synopsis [Computes one fair SCC of an FSM, by LockStep.] Description [Computes one fair SCC of the state transition graph of an FSM. Returns the fair SCC if one exists; NULL otherwise. This function uses the lockstep SCC enumeration algorithm of Bloem, Gabow, and Somenzi (FMCAD'00) implemented as described in Ravi, Bloem, and Somenzi (FMCAD'00), and with the addition of an early termination test.
On input, the heap is supposed to contain a set of SCC-closed state sets. If earlyTermination is requested, the heap is left in an inconsistent state; otherwise, it contains a set of SCC-closed sets that contains all fair SCCs that were on the heap on input except the one that has been enumerated. The number of sets may be different, and some non-fair SCCs may no longer be present.
The onionRing parameter is an array of state sets that is used to pick a seed close to a target. Typically, these onion rings come from reachability analysis. The target states in this case are the initial states of the FSM, and the objective of choosing a seed close to them is to reduce the length of the stem of a counterexample in the language emptiness check. However, any collection of sets that together cover all the states on the heap will work. If one is not concerned with a specific target, but rather with speed, then passing an array with just one component set to the constant one is preferable.] SideEffects [Updates the priority queue. The number of SCC examined (i.e., the number of chosen seeds) is added to sccExamined.] SeeAlso [Mc_FsmForEachFairScc] ******************************************************************************/ mdd_t * McFsmComputeOneFairSccByLockStep( Fsm_Fsm_t *fsm, Heap_t *priorityQueue, array_t *buechiFairness, array_t *onionRings, boolean earlyTermination, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int *sccExamined) { mdd_t *mddOne, *SCC = NIL(mdd_t); mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); array_t *careStatesArray = array_alloc(mdd_t *, 0); int totalSCCs = 0; boolean foundScc = FALSE; array_t *activeFairness = NIL(array_t); int firstActive = 0; /* Initialization. */ mddOne = mdd_one(mddManager); array_insert(mdd_t *, careStatesArray, 0, mddOne); while (Heap_HeapCount(priorityQueue)) { mdd_t *V, *seed, *B, *F, *fFront, *bFront, *fairSet; mdd_t *converged, *first, *second; long ringIndex; McLockstepMode firstMode, secondMode; int retval UNUSED = Heap_HeapExtractMin(priorityQueue, &V, &ringIndex); assert(retval && ringIndex < array_n(onionRings)); /* Here, V contains at least one nontrivial SCC. We then choose the * seed for a new SCC, which may turn out to be trivial. */ seed = LockstepPickSeed(fsm, V, buechiFairness, onionRings, ringIndex); if (earlyTermination == TRUE) { int i; activeFairness = array_alloc(mdd_t *, 0); for (i = 0; i < array_n(buechiFairness); i++) { mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i); if (!mdd_lequal(seed, fairSet, 1, 1)) { array_insert_last(mdd_t *, activeFairness, fairSet); } } } /* Do lockstep search from seed. Leave the seed initially out of * F and B to facilitate the detection of trivial SCCs. Intersect * all results with V so that we can simplify the transition * relation. */ fFront = Mc_FsmEvaluateEYFormula(fsm, seed, mddOne, careStatesArray, verbosity, dcLevel); F = mdd_and(fFront, V, 1, 1); mdd_free(fFront); fFront = mdd_dup(F); bFront = Mc_FsmEvaluateEXFormula(fsm, seed, mddOne, careStatesArray, verbosity, dcLevel); B = mdd_and(bFront, V , 1, 1); mdd_free(bFront); bFront = mdd_dup(B); /* Go until the fastest search converges. */ while (!(mdd_is_tautology(fFront, 0) || mdd_is_tautology(bFront, 0))) { mdd_t *tmp; /* If the intersection of F and B intersects all fairness * constraints the union of F and B contains at least one fair * SCC. Since the intersection of F and B is monotonically * non-decreasing, once a fair set has been intersected, there * is no need to check for it any more. */ if (earlyTermination == TRUE) { mdd_t * meet = mdd_and(F, B, 1, 1); if (!mdd_is_tautology(meet, 0)) { assert(mdd_lequal(meet, V, 1, 1)); for ( ; firstActive < array_n(activeFairness); firstActive++) { mdd_t *fairSet = array_fetch(mdd_t *, activeFairness, firstActive); if (mdd_lequal(meet, fairSet, 1, 0)) break; } if (firstActive == array_n(activeFairness)) { int i; (void) fprintf(vis_stdout, "EARLY TERMINATION!\n"); totalSCCs++; /* A fair SCC is contained in the union of F, B, and seed. */ tmp = mdd_or(F, B, 1, 1); SCC = mdd_or(tmp, seed, 1, 1); mdd_free(tmp); /* Trim fair sets to guarantee counterexample will go through * this SCC. */ tmp = mdd_or(meet, seed, 1, 1); mdd_free(meet); meet = tmp; for (i = 0; i < array_n(buechiFairness); i++) { mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i); mdd_t *trimmed = mdd_and(fairSet, meet, 1, 1); mdd_free(fairSet); array_insert(mdd_t *, buechiFairness, i, trimmed); } mdd_free(meet); mdd_free(F); mdd_free(B); mdd_free(fFront); mdd_free(bFront); mdd_free(seed); mdd_free(V); foundScc = TRUE; array_free(activeFairness); goto cleanUp; } } mdd_free(meet); } /* Forward step. */ tmp = Mc_FsmEvaluateEYFormula(fsm, fFront, mddOne, careStatesArray, verbosity, dcLevel); mdd_free(fFront); fFront = mdd_and(tmp, F, 1, 0); mdd_free(tmp); tmp = mdd_and(fFront, V, 1, 1); mdd_free(fFront); fFront = tmp; if (mdd_is_tautology(fFront, 0)) break; tmp = mdd_or(F, fFront, 1, 1); mdd_free(F); F = tmp; /* Backward step. */ tmp = Mc_FsmEvaluateEXFormula(fsm, bFront, mddOne, careStatesArray, verbosity, dcLevel); mdd_free(bFront); bFront = mdd_and(tmp, B, 1, 0); mdd_free(tmp); tmp = mdd_and(bFront, V, 1, 1); mdd_free(bFront); bFront = tmp; tmp = mdd_or(B, bFront, 1, 1); mdd_free(B); B = tmp; } /* Complete the slower search within the converged one. */ if (mdd_is_tautology(fFront, 0)) { /* Forward search converged. */ mdd_t *tmp = mdd_and(bFront, F, 1, 1); mdd_free(bFront); bFront = tmp; mdd_free(fFront); converged = mdd_dup(F); /* The two sets to be enqueued come from a set that has been * already trimmed. Hence, we want to remove the trivial SCCs * left exposed at the rearguard of F, and the trivial SCCs left * exposed at the vanguard of B. */ firstMode = McLS_H_c; secondMode = McLS_G_c; while (!mdd_is_tautology(bFront, 0)) { tmp = Mc_FsmEvaluateEXFormula(fsm, bFront, mddOne, careStatesArray, verbosity, dcLevel); mdd_free(bFront); bFront = mdd_and(tmp, B, 1, 0); mdd_free(tmp); tmp = mdd_and(bFront, converged, 1, 1); mdd_free(bFront); bFront = tmp; tmp = mdd_or(B, bFront, 1, 1); mdd_free(B); B = tmp; } mdd_free(bFront); } else { /* Backward search converged. */ mdd_t *tmp = mdd_and(fFront, B, 1, 1); mdd_free(fFront); fFront = tmp; mdd_free(bFront); converged = mdd_dup(B); firstMode = McLS_G_c; secondMode = McLS_H_c; while (!mdd_is_tautology(fFront, 0)) { tmp = Mc_FsmEvaluateEYFormula(fsm, fFront, mddOne, careStatesArray, verbosity, dcLevel); mdd_free(fFront); fFront = mdd_and(tmp, F, 1 ,0); mdd_free(tmp); tmp = mdd_and(fFront, converged, 1, 1); mdd_free(fFront); fFront = tmp; tmp = mdd_or(F, fFront, 1, 1); mdd_free(F); F = tmp; } mdd_free(fFront); } totalSCCs++; SCC = mdd_and(F, B, 1, 1); mdd_free(F); mdd_free(B); /* Check for fairness. If SCC is the empty set we know that seed * is a trivial strong component; hence, it is not fair. */ if (mdd_is_tautology(SCC, 0)) { mdd_t *tmp = mdd_or(converged, seed, 1, 1); mdd_free(converged); converged = tmp; mdd_free(SCC); SCC = mdd_dup(seed); } else { /* Check fairness constraints. */ int i; arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) { if (mdd_lequal(SCC, fairSet, 1, 0)) break; } if (i == array_n(buechiFairness)) { /* All fairness conditions intersected. We have a fair SCC. */ if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { array_t *PSvars = Fsm_FsmReadPresentStateVars(fsm); fprintf(vis_stdout, "--SCC: found a fair SCC with %.0f states\n", mdd_count_onset(mddManager, SCC, PSvars)); /* (void) bdd_print_minterm(SCC); */ } foundScc = TRUE; } } /* Divide the remaining states of V into the converged set minus * the fair SCC, and the rest (minus the fair SCC). Add the two * sets thus obtained to the priority queue. */ mdd_free(seed); first = mdd_and(converged, SCC, 1, 0); LockstepQueueEnqueue(fsm, priorityQueue, first, onionRings, firstMode, buechiFairness, verbosity, dcLevel); second = mdd_and(V, converged, 1, 0); mdd_free(converged); mdd_free(V); LockstepQueueEnqueue(fsm, priorityQueue, second, onionRings, secondMode, buechiFairness, verbosity, dcLevel); if (earlyTermination == TRUE) { array_free(activeFairness); } if (foundScc == TRUE) break; mdd_free(SCC); } cleanUp: mdd_free(mddOne); array_free(careStatesArray); if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "--SCC: found %s fair SCC out of %d examined\n", foundScc ? "one" : "no", totalSCCs); fprintf(vis_stdout, "--SCC: %d image computations, %d preimage computations\n", Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps, Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); } *sccExamined += totalSCCs; return foundScc ? SCC : NIL(mdd_t); } /* McFsmComputeOneFairSccByLockStep */ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Returns a seed state for lockstep search.] Description [Returns a seed state for lockstep search, or NULL in case of failure. The strategy is to first find the innermost ring that intersects the given set of states (V) and one fairness constraint. The other fairness constraints are then checked to increase the number of fairness constraints that are satisfied by the seed. The search is greedy.] SideEffects [none] SeeAlso [McFsmComputeOneFairSccByLockStep] ******************************************************************************/ static mdd_t * LockstepPickSeed( Fsm_Fsm_t *fsm, mdd_t *V, array_t *buechiFairness, array_t *onionRings, int ringIndex) { mdd_t *seed; int i, j; /* We know that there is at least one state in V from each fairness * constraint. */ for (i = ringIndex; i < array_n(onionRings); i++) { mdd_t *ring = array_fetch(mdd_t *, onionRings, i); for (j = 0; j < array_n(buechiFairness); j++) { mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, j); if (!mdd_lequal_mod_care_set(ring, fairSet, 1, 0, V)) { mdd_t *tmp = mdd_and(V, ring, 1, 1); mdd_t *candidates = mdd_and(tmp, fairSet, 1, 1); mdd_free(tmp); for (j++; j < array_n(buechiFairness); j++) { fairSet = array_fetch(mdd_t *, buechiFairness, j); if (!mdd_lequal(candidates, fairSet, 1, 0)) { tmp = mdd_and(candidates, fairSet, 1, 1); mdd_free(candidates); candidates = tmp; } } seed = Mc_ComputeAState(candidates, fsm); mdd_free(candidates); return seed; } } } assert(FALSE); /* we should never get here */ return NIL(bdd_t); } /* LockstepPickSeed */ /**Function******************************************************************** Synopsis [Adds a set of states to the priority queue of the lockstep algorithm.] Description [Given a set of states, applies trimming as specified by mode. Checks then if the trimmed set may contain a fair SCC, in which case it adds the set to the priority queue.] SideEffects [May change the set of states as a result of trimming. The old set of states is freed.] SeeAlso [McFsmComputeOneFairSccByLockStep] ******************************************************************************/ static void LockstepQueueEnqueue( Fsm_Fsm_t *fsm, Heap_t *queue, mdd_t *states, array_t *onionRings, McLockstepMode mode, array_t *buechiFairness, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) { mdd_t *fairSet, *ring; int i; mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); mdd_t *mddOne = mdd_one(mddManager); array_t *careStatesArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, careStatesArray, mddOne); #ifndef SCC_NO_TRIM if (mode == McLS_G_c || mode == McLS_GH_c) { mdd_t *trimmed = Mc_FsmEvaluateEGFormula(fsm, states, NIL(mdd_t), mddOne, NIL(Fsm_Fairness_t), careStatesArray, MC_NO_EARLY_TERMINATION, NIL(array_t), Mc_None_c, NIL(array_t *), verbosity, dcLevel, NIL(boolean), McGSH_EL_c); mdd_free(states); states = trimmed; } if (mode == McLS_H_c || mode == McLS_GH_c) { mdd_t *trimmed = Mc_FsmEvaluateEHFormula(fsm, states, NIL(mdd_t), mddOne, NIL(Fsm_Fairness_t), careStatesArray, MC_NO_EARLY_TERMINATION, NIL(array_t), Mc_None_c, NIL(array_t *), verbosity, dcLevel, NIL(boolean), McGSH_EL_c); mdd_free(states); states = trimmed; } #endif mdd_free(mddOne); array_free(careStatesArray); if (mode == McLS_none_c) { mdd_t *range = mdd_range_mdd(mddManager, Fsm_FsmReadPresentStateVars(fsm)); mdd_t *valid = mdd_and(states, range, 1, 1); mdd_free(range); mdd_free(states); states = valid; } /* Discard set of states if it does not intersect all fairness conditions. */ arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) { if (mdd_lequal(states, fairSet, 1, 0)) { mdd_free(states); return; } } /* Find the innermost onion ring intersecting the set of states. * Its index is the priority of the set. */ arrayForEachItem(mdd_t *, onionRings, i, ring) { if (!mdd_lequal(states, ring, 1, 0)) break; } assert(i < array_n(onionRings)); Heap_HeapInsert(queue,states,i); return; } /* LockstepQueueEnqueue */ /**Function******************************************************************** Synopsis [Adds a set of states to the priority queue of the lockstep algorithm.] Description [Given a set of states, applies trimming as specified by mode. Checks then if the trimmed set may contain a fair SCC, in which case it adds the set to the priority queue.] SideEffects [May change the set of states as a result of trimming. The old set of states is freed.] SeeAlso [McFsmComputeOneFairSccByLockStep] ******************************************************************************/ static void LinearstepQueueEnqueue( Fsm_Fsm_t *fsm, Heap_t *queue, mdd_t *states, mdd_t *spine, mdd_t *node, array_t *onionRings, McLockstepMode mode, array_t *buechiFairness, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) { mdd_t *fairSet, *ring; mdd_t *tmp, *tmp1; int i; gns_t *gns; mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); mdd_t *mddOne = mdd_one(mddManager); array_t *careStatesArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, careStatesArray, mddOne); #ifndef SCC_NO_TRIM if (mode == McLS_G_c || mode == McLS_GH_c) { mdd_t *trimmed = Mc_FsmEvaluateEGFormula(fsm, states, NIL(mdd_t), mddOne, NIL(Fsm_Fairness_t), careStatesArray, MC_NO_EARLY_TERMINATION, NIL(array_t), Mc_None_c, NIL(array_t *), verbosity, dcLevel, NIL(boolean), McGSH_EL_c); mdd_free(states); states = trimmed; } if (mode == McLS_H_c || mode == McLS_GH_c) { mdd_t *trimmed = Mc_FsmEvaluateEHFormula(fsm, states, NIL(mdd_t), mddOne, NIL(Fsm_Fairness_t), careStatesArray, MC_NO_EARLY_TERMINATION, NIL(array_t), Mc_None_c, NIL(array_t *), verbosity, dcLevel, NIL(boolean), McGSH_EL_c); mdd_free(states); states = trimmed; } #endif if (mode == McLS_none_c) { mdd_t *range = mdd_range_mdd(mddManager, Fsm_FsmReadPresentStateVars(fsm)); mdd_t *valid = mdd_and(states, range, 1, 1); mdd_free(range); mdd_free(states); states = valid; } /* Discard set of states if it does not intersect all fairness conditions. */ arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) { if (mdd_lequal(states, fairSet, 1, 0)) { mdd_free(states); mdd_free(mddOne); array_free(careStatesArray); return; } } /* Find the innermost onion ring intersecting the set of states. * Its index is the priority of the set. */ arrayForEachItem(mdd_t *, onionRings, i, ring) { if (!mdd_lequal(states, ring, 1, 0)) break; } assert(i < array_n(onionRings)); /* Trim the spine-set. */ while ( !mdd_lequal(node, states, 1, 1) ) { tmp = node; tmp1 = Mc_FsmEvaluateEXFormula(fsm, node, mddOne, careStatesArray, verbosity, dcLevel); mdd_free(tmp); node = mdd_and(tmp1, spine, 1, 1); mdd_free(tmp1); } tmp = spine; spine = mdd_and(spine, states, 1, 1); mdd_free(tmp); #if 0 /* Invariants that should always hold */ assert( mdd_is_tautology(node, 0) == mdd_is_tautology(spine, 0) ); assert(mdd_lequal(node, states, 1, 1)); assert(mdd_lequal(node, spine, 1, 1)); assert(mdd_lequal(spine, states, 1, 1)); #endif mdd_free(mddOne); array_free(careStatesArray); gns = ALLOC(gns_t, 1); gns->states = states; gns->node = node; gns->spine = spine; Heap_HeapInsert(queue,gns,i); return; } /* LinearstepQueueEnqueue */ /**Function******************************************************************** Synopsis [Return the SCC enumeration method.] Description [Get the SCC enumeration method from the environment setting scc_method. Return 0 if it is LockStep (default), 1 if it is LinearStep. ] SideEffects [] SeeAlso [GetSccEnumerationMethod] ******************************************************************************/ static int GetSccEnumerationMethod( void ) { char *flagValue; int linearStepMethod = 0; flagValue = Cmd_FlagReadByName("scc_method"); if (flagValue != NIL(char)) { if (strcmp(flagValue, "linearstep") == 0) linearStepMethod = 1; else if (strcmp(flagValue, "lockstep") == 0) linearStepMethod = 0; else { fprintf(vis_stderr, "** scc error: invalid scc method %s, method lockstep is used. \n", flagValue); } } return linearStepMethod; }