src/mc/mcSCC.c File Reference
#include "mcInt.h"
Include dependency graph for mcSCC.c:
Go to the source code of this file.
Data Structures | |
| struct | GraphNodeSpineSet |
Typedefs | |
| typedef struct GraphNodeSpineSet | gns_t |
Functions | |
| static mdd_t * | LockstepPickSeed (Fsm_Fsm_t *fsm, mdd_t *V, array_t *buechiFairness, array_t *onionRings, int ringIndex) |
| 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) |
| 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) |
| static int | GetSccEnumerationMethod (void) |
| Mc_SccGen_t * | Mc_FsmFirstScc (Fsm_Fsm_t *fsm, mdd_t **scc, array_t *sccClosedSetArray, array_t *buechiFairness, array_t *onionRings, boolean earlyTermination, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| boolean | Mc_FsmNextScc (Mc_SccGen_t *gen, mdd_t **scc) |
| boolean | Mc_FsmIsSccGenEmpty (Mc_SccGen_t *gen) |
| boolean | Mc_FsmSccGenFree (Mc_SccGen_t *gen, array_t *leftover) |
| mdd_t * | McFsmComputeFairSCCsByLockStep (Fsm_Fsm_t *fsm, int maxNumberOfSCCs, array_t *SCCs, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| 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) |
| 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 * | McFsmComputeOneFairSccByLockStep (Fsm_Fsm_t *fsm, Heap_t *priorityQueue, array_t *buechiFairness, array_t *onionRings, boolean earlyTermination, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int *sccExamined) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mcSCC.c,v 1.11 2005/05/18 19:35:19 jinh Exp $" |
Typedef Documentation
| typedef struct GraphNodeSpineSet gns_t |
Function Documentation
| static int GetSccEnumerationMethod | ( | void | ) | [static] |
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]
Definition at line 1481 of file mcSCC.c.
{
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;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) | [static] |
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]
Definition at line 1359 of file mcSCC.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * LockstepPickSeed | ( | Fsm_Fsm_t * | fsm, |
| mdd_t * | V, | ||
| array_t * | buechiFairness, | ||
| array_t * | onionRings, | ||
| int | ringIndex | ||
| ) | [static] |
AutomaticStart
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]
Definition at line 1214 of file mcSCC.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) | [static] |
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]
Definition at line 1271 of file mcSCC.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| Mc_SccGen_t* Mc_FsmFirstScc | ( | Fsm_Fsm_t * | fsm, |
| mdd_t ** | scc, | ||
| array_t * | sccClosedSetArray, | ||
| array_t * | buechiFairness, | ||
| array_t * | onionRings, | ||
| boolean | earlyTermination, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Generates the first fair SCC of a FSM.]
Description [Defines an iterator on the fair SCCs of a FSM and finds the first fair SCC. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.]
SideEffects [The fair SCC is retuned as a side effect.]
SeeAlso [Mc_FsmForEachScc Mc_FsmNextScc Mc_FsmIsSccGenEmpty Mc_FsmSccGenFree]
Definition at line 94 of file mcSCC.c.
{
Mc_SccGen_t *gen;
Heap_t *heap;
int i;
mdd_t *closedSet;
int linearStepMethod;
if (fsm == NIL(Fsm_Fsm_t)) return NIL(Mc_SccGen_t);
/* Allocate generator and initialize it. */
gen = ALLOC(Mc_SccGen_t, 1);
if (gen == NIL(Mc_SccGen_t)) return NIL(Mc_SccGen_t);
gen->fsm = fsm;
gen->heap = heap = Heap_HeapInit(1);
gen->rings = onionRings;
gen->buechiFairness = buechiFairness;
gen->earlyTermination = earlyTermination;
gen->verbosity = verbosity;
gen->dcLevel = dcLevel;
gen->totalExamined = 0;
gen->nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
gen->nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
linearStepMethod = GetSccEnumerationMethod();
/* Initialize the heap from the given sets of states. */
arrayForEachItem(mdd_t *, sccClosedSetArray, i, closedSet) {
if (linearStepMethod == 1) {
mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
LinearstepQueueEnqueue(fsm, heap, mdd_dup(closedSet),
mdd_zero(mddManager),
mdd_zero(mddManager), onionRings,
McLS_none_c, buechiFairness, verbosity, dcLevel);
}else {
LockstepQueueEnqueue(fsm, heap, mdd_dup(closedSet), onionRings,
McLS_none_c, buechiFairness, verbosity, dcLevel);
}
}
/* Find first SCC. */
if (Heap_HeapCount(heap) == 0) {
*scc = NIL(mdd_t);
} else {
if (linearStepMethod == 1)
*scc = McFsmComputeOneFairSccByLinearStep(fsm, heap, buechiFairness,
onionRings, earlyTermination,
verbosity, dcLevel,
&(gen->totalExamined));
else
*scc = McFsmComputeOneFairSccByLockStep(fsm, heap, buechiFairness,
onionRings, earlyTermination,
verbosity, dcLevel,
&(gen->totalExamined));
}
if (*scc == NIL(mdd_t)) {
gen->status = McSccGenEmpty_c;
gen->fairSccsFound = 0;
} else {
gen->status = McSccGenNonEmpty_c;
gen->fairSccsFound = 1;
}
return gen;
} /* Mc_FsmFirstScc */
Here is the call graph for this function:
| boolean Mc_FsmIsSccGenEmpty | ( | Mc_SccGen_t * | gen | ) |
Function********************************************************************
Synopsis [Returns TRUE if a generator is empty; FALSE otherwise.]
Description []
SideEffects [none]
SeeAlso [Mc_FsmForEachScc Mc_FsmFirstScc Mc_FsmNextScc Mc_FsmSccGenFree]
Definition at line 229 of file mcSCC.c.
{
if (gen == NIL(Mc_SccGen_t)) return TRUE;
return gen->status == McSccGenEmpty_c;
} /* Mc_FsmIsSccGenEmpty */
| boolean Mc_FsmNextScc | ( | Mc_SccGen_t * | gen, |
| mdd_t ** | scc | ||
| ) |
Function********************************************************************
Synopsis [Generates the next fair SCC of a FSM.]
Description [Generates the next fair SCC of a FSM, using generator gen. Returns FALSE if the enumeration is completed; TRUE otherwise.]
SideEffects [The fair SCC is returned as side effect.]
SeeAlso [Mc_FsmForEachScc Mc_FsmFirstScc Mc_FsmIsSccGenEmpty Mc_FsmSccGenFree]
Definition at line 182 of file mcSCC.c.
{
int linearStepMethod;
if (gen->earlyTermination == TRUE) {
gen->status = McSccGenEmpty_c;
return FALSE;
}
linearStepMethod = GetSccEnumerationMethod();
if (linearStepMethod == 1)
*scc = McFsmComputeOneFairSccByLinearStep(gen->fsm, gen->heap,
gen->buechiFairness, gen->rings,
gen->earlyTermination,
gen->verbosity, gen->dcLevel,
&(gen->totalExamined));
else
*scc = McFsmComputeOneFairSccByLockStep(gen->fsm, gen->heap,
gen->buechiFairness, gen->rings,
gen->earlyTermination,
gen->verbosity, gen->dcLevel,
&(gen->totalExamined));
if (*scc == NIL(mdd_t)) {
gen->status = McSccGenEmpty_c;
return FALSE;
} else {
gen->status = McSccGenNonEmpty_c;
gen->fairSccsFound++;
return TRUE;
}
} /* Mc_FsmNextScc */
Here is the call graph for this function:
| boolean Mc_FsmSccGenFree | ( | Mc_SccGen_t * | gen, |
| array_t * | leftover | ||
| ) |
Function********************************************************************
Synopsis [Frees a SCC generator.]
Description [Frees a SCC generator. Always returns FALSE, so that it can be used in iterators.
leftover is an array_t of mdd_t *s.]
SideEffects [The sets of states in the heap are returned in leftover if the array pointer is non-null.]
SeeAlso [Mc_FsmForEachScc Mc_FsmFirstScc Mc_FsmNextScc Mc_FsmIsSccGenEmpty]
Definition at line 255 of file mcSCC.c.
{
int linearStepMethod;
if (gen == NIL(Mc_SccGen_t)) return FALSE;
/* Print some stats. */
if (gen->verbosity == McVerbositySome_c || gen->verbosity == McVerbosityMax_c) {
fprintf(vis_stdout,
"--SCC: found %d fair SCC(s) out of %d examined\n",
gen->fairSccsFound, gen->totalExamined);
fprintf(vis_stdout,
"--SCC: %d image computations, %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c) - gen->nImgComps,
Img_GetNumberOfImageComputation(Img_Backward_c) - gen->nPreComps);
}
/* Create array from elements still on queue if so requested. */
linearStepMethod = GetSccEnumerationMethod();
if (linearStepMethod == 1) {
while (Heap_HeapCount(gen->heap)) {
gns_t *set;
long index;
int retval UNUSED = Heap_HeapExtractMin(gen->heap, &set, &index);
assert(retval);
if (leftover == NIL(array_t) || gen->earlyTermination == TRUE) {
mdd_free(set->states);
} else {
array_insert_last(mdd_t *, leftover, set->states);
}
mdd_free(set->spine); mdd_free(set->node);
FREE(set);
}
}else {
while (Heap_HeapCount(gen->heap)) {
mdd_t *set;
long index;
int retval UNUSED = Heap_HeapExtractMin(gen->heap, &set, &index);
assert(retval);
if (leftover == NIL(array_t) || gen->earlyTermination == TRUE) {
mdd_free(set);
} else {
array_insert_last(mdd_t *, leftover, set);
}
}
}
Heap_HeapFree(gen->heap);
FREE(gen);
return FALSE;
} /* Mc_FsmSccGenFree */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McFsmComputeFairSCCsByLockStep | ( | Fsm_Fsm_t * | fsm, |
| int | maxNumberOfSCCs, | ||
| array_t * | SCCs, | ||
| array_t * | onionRingsArrayForDbg, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Computes fair SCCs of an FSM.]
Description [Returns some fair SCCs of an FSM and the states on the paths leading to them. Parameter 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 []
Definition at line 328 of file mcSCC.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) |
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]
Definition at line 642 of file mcSCC.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) |
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]
Definition at line 934 of file mcSCC.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| 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 | ||
| ) |
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]
Definition at line 456 of file mcSCC.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
