#include "mcInt.h"
Include dependency graph for mcDnC.c:
Go to the source code of this file.
Functions | |
| static int | SccIsStrong (mdd_manager *mddMgr, array_t *buechiFairness, mdd_t *SCC) |
| static array_t * | SortMddArrayBySize (Fsm_Fsm_t *fsm, array_t *mddArray) |
| static int | stringCompare (const void *s1, const void *s2) |
| mdd_t * | Mc_FsmCheckLanguageEmptinessByDnC (Fsm_Fsm_t *modelFsm, array_t *modelCareStates, Mc_AutStrength_t automatonStrength, int dcLevel, int dbgLevel, int printInputs, int verbosity, Mc_GSHScheduleType GSHschedule, Mc_FwdBwdAnalysis GSHdirection, int lockstep, FILE *dbgFile, int UseMore, int SimValue, char *driverName) |
| array_t * | Mc_CreateStaticRefinementScheduleArray (Ntk_Network_t *network, array_t *ctlArray, array_t *ltlArray, array_t *fairArray, boolean dynamicIncrease, boolean isLatchNameSort, int verbosity, int incrementalSize, Part_CMethod correlationMethod) |
| mdd_t * | McFsmRefineWeakFairSCCs (Fsm_Fsm_t *modelFsm, mdd_t *sccClosedSet, array_t *modelCareStatesArray, array_t *arrayOfOnionRings, boolean isSccTerminal, int dcLevel, int verbosity) |
| mdd_t * | McComputeAbstractStates (Fsm_Fsm_t *absFsm, mdd_t *states) |
| boolean | McGetDncEnabled (void) |
| static int | array_mdd_compare_size (const void *obj1, const void *obj2) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mcDnC.c,v 1.9 2005/05/18 18:12:00 jinh Exp $" |
| static st_table * | array_mdd_compare_table = NIL(st_table) |
Function Documentation
| static int array_mdd_compare_size | ( | const void * | obj1, |
| const void * | obj2 | ||
| ) | [static] |
Definition at line 985 of file mcDnC.c.
{
double *val1, *val2;
int flag1, flag2;
flag1 = st_lookup(array_mdd_compare_table, *((char **)obj1), &val1);
flag2 = st_lookup(array_mdd_compare_table, *((char **)obj2), &val2);
assert(flag1 && flag2);
if (*val1 < *val2)
return -1;
else if (*val1> *val2)
return +1;
else
return 0;
}
Here is the caller graph for this function:
| array_t* Mc_CreateStaticRefinementScheduleArray | ( | Ntk_Network_t * | network, |
| array_t * | ctlArray, | ||
| array_t * | ltlArray, | ||
| array_t * | fairArray, | ||
| boolean | dynamicIncrease, | ||
| boolean | isLatchNameSort, | ||
| int | verbosity, | ||
| int | incrementalSize, | ||
| Part_CMethod | correlationMethod | ||
| ) |
Function********************************************************************
Synopsis [Create a refinement schedule array.]
Description [If dynamicIncrease is true, the first element of return array includes varibales appeared in formula. The size of the first element should be less than or equal to incrementalSize. The second element includes all variables in formula's cone of influence. When dynamicIncrease is false, all variables in formula's cone of influence (let's say n variables) are partitioned into ceil(n/incrementalSize) elements. Then one more element which includes all n variables are added to return array.]
SideEffects []
SeeAlso [Part_SubsystemInfo_t]
Definition at line 601 of file mcDnC.c.
{
array_t *partitionArray;
Part_Subsystem_t *partitionSubsystem;
Part_SubsystemInfo_t *subsystemInfo;
st_table *latchNameTable;
st_table *latchNameTableSum, *latchNameTableSumCopy;
char *flagValue;
st_generator *stGen;
char *name;
double affinityFactor;
array_t *scheduleArray;
boolean dynamicAndDependency = isLatchNameSort;
array_t *tempArray, *tempArray2;
int i, count;
/* affinity factor to decompose state space */
flagValue = Cmd_FlagReadByName("part_group_affinity_factor");
if(flagValue != NIL(char)){
affinityFactor = atof(flagValue);
}
else{
/* default value */
affinityFactor = 0.5;
}
/*
* Obtain submachines as array: The first sub-system includes
* variables in CTL/LTL/fair formulas and other latches are grouped
* in the same way as Part_PartCreateSubsystems()
*/
subsystemInfo = Part_PartitionSubsystemInfoInit(network);
Part_PartitionSubsystemInfoSetBound(subsystemInfo, incrementalSize);
Part_PartitionSubsystemInfoSetVerbosity(subsystemInfo, verbosity);
Part_PartitionSubsystemInfoSetCorrelationMethod(subsystemInfo,
correlationMethod);
Part_PartitionSubsystemInfoSetAffinityFactor(subsystemInfo, affinityFactor);
partitionArray = Part_PartCreateSubsystemsWithCtlAndLtl(subsystemInfo,
ctlArray, ltlArray, fairArray,
dynamicIncrease,dynamicAndDependency,FALSE);
Part_PartitionSubsystemInfoFree(subsystemInfo);
scheduleArray = array_alloc(st_table *, 0);
/*
* For each partitioned submachines build an FSM.
*/
latchNameTableSum = st_init_table(strcmp, st_strhash);
if (!dynamicAndDependency){
for (i=0;i<array_n(partitionArray);i++){
partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, i);
if (partitionSubsystem != NIL(Part_Subsystem_t)) {
latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
if (!st_lookup(latchNameTableSum, name, NIL(char *))){
st_insert(latchNameTableSum, name, NIL(char));
}
}
Part_PartitionSubsystemFree(partitionSubsystem);
}
latchNameTableSumCopy = st_copy(latchNameTableSum);
array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
}
}else{
partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 0);
latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
st_insert(latchNameTableSum, name, NIL(char));
}
latchNameTableSumCopy = st_copy(latchNameTableSum);
array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
Part_PartitionSubsystemFree(partitionSubsystem);
partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 1);
tempArray = array_alloc(char *, 0);
if (partitionSubsystem != NIL(Part_Subsystem_t)){
latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
array_insert_last(char *, tempArray, name);
}
array_sort(tempArray, stringCompare);
Part_PartitionSubsystemFree(partitionSubsystem);
}
partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 2);
tempArray2 = array_alloc(char *, 0);
if (partitionSubsystem != NIL(Part_Subsystem_t)) {
latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
array_insert_last(char *, tempArray2, name);
}
array_sort(tempArray2, stringCompare);
Part_PartitionSubsystemFree(partitionSubsystem);
}
array_append(tempArray, tempArray2);
array_free(tempArray2);
count = 0;
arrayForEachItem(char *, tempArray, i, name){
if (!st_lookup(latchNameTableSum, name, NIL(char *))){
st_insert(latchNameTableSum, (char *)name, (char *)0);
count++;
}
if ((count == incrementalSize) && (i < array_n(tempArray)-1)){
latchNameTableSumCopy = st_copy(latchNameTableSum);
array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
count = 0;
}
}
array_free(tempArray);
latchNameTableSumCopy = st_copy(latchNameTableSum);
array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
}
array_free(partitionArray);
st_free_table(latchNameTableSum);
return (scheduleArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmCheckLanguageEmptinessByDnC | ( | Fsm_Fsm_t * | modelFsm, |
| array_t * | modelCareStates, | ||
| Mc_AutStrength_t | automatonStrength, | ||
| int | dcLevel, | ||
| int | dbgLevel, | ||
| int | printInputs, | ||
| int | verbosity, | ||
| Mc_GSHScheduleType | GSHschedule, | ||
| Mc_FwdBwdAnalysis | GSHdirection, | ||
| int | lockstep, | ||
| FILE * | dbgFile, | ||
| int | UseMore, | ||
| int | SimValue, | ||
| char * | driverName | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Compute all the states that lead to a fair cycle by Compositional SCC analysis (DnC -- Divide and Compose).]
Comment [Used by LE/LTL/CTL* model checking. The Divide and Compose (D'n'C) approach is used for the symbolic SCC enumeration, which first creates SCC-closed sets on an abstract model and then successively refines these sets on the refined abstract models, until either no fair SCC exists or the concrete (original) model is reached.
Strength reduction is also applied during the process -- as soon as the SCC-closed sets become weak/terminal, special decision procedures will be used to determine their language emptiness.
For more information, please check the CONCUR'01 paper of Wang et al., "Divide and Compose: SCC refinement for language emptiness."
Debugging information will be print out if dbgLevel is non-zero.
Return the set of initial states from where fair paths exist.]
SideEffects []
Definition at line 97 of file mcDnC.c.
{
Ntk_Network_t *network = Fsm_FsmReadNetwork(modelFsm);
mdd_manager *mddManager = Fsm_FsmReadMddManager(modelFsm);
Fsm_Fairness_t *modelFairness = NIL(Fsm_Fairness_t);
array_t *buechiFairness = NIL(array_t);
int isExactReachableStatesAvailable = 0;
mdd_t *reachableStates, *initialStates = NIL(mdd_t);
mdd_t *fairStates, *fairInitialStates = NIL(mdd_t);
array_t *onionRings = NIL(array_t);
array_t *strongSccClosedSets = NIL(array_t);
array_t *absLatchNameTableArray = NIL(array_t);
int numOfAbstractModels, iter, i, exitFlag;
array_t *arrayOfOnionRings = NIL(array_t);
array_t *ctlArray = array_alloc(Ctlp_Formula_t *, 0);
array_t *modelCareStatesArray = mdd_array_duplicate(modelCareStates);
Mc_SccGen_t *sccgen;
int composeIncSize, numOfLatches, maxLatchesToCompose;
int maxComposePercentage = 30;
int maxSccsToEnum = 100;
/*
* Read fairness constraints.
*/
modelFairness = Fsm_FsmReadFairnessConstraint(modelFsm);
buechiFairness = array_alloc(mdd_t *, 0);
if (modelFairness != NIL(Fsm_Fairness_t)) {
if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
(void) fprintf(vis_stdout,
"** non-Buechi fairness constraints not supported\n");
array_free(buechiFairness);
assert(0);
} else {
int j;
int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
for (j = 0; j < numBuchi; j++) {
Ctlp_Formula_t *tmpFormula;
mdd_t *tempMdd;
tmpFormula = Fsm_FairnessReadFinallyInfFormula(modelFairness, 0, j );
tempMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
modelCareStatesArray,
(Mc_DcLevel) dcLevel);
array_insert_last(mdd_t *, buechiFairness, tempMdd);
array_insert_last( Ctlp_Formula_t *, ctlArray,
Ctlp_FormulaDup(tmpFormula));
#if 1
fprintf(vis_stdout,"\nFairness[%d]:",j);
Ctlp_FormulaPrint(vis_stdout, tmpFormula);
fprintf(vis_stdout,"\n");
#endif
}
}
} else {
array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
}
/*
* If we need debugging information, arrayOfOnionRings != NIL(array_t),
*/
if (dbgLevel != McDbgLevelNone_c)
arrayOfOnionRings = array_alloc(array_t *, 0);
else
arrayOfOnionRings = NIL(array_t);
/*
* If exact/approximate reachable states are available, use them.
*/
initialStates = Fsm_FsmComputeInitialStates(modelFsm);
reachableStates = Fsm_FsmReadReachableStates(modelFsm);
isExactReachableStatesAvailable = (reachableStates != NIL(mdd_t));
if (!isExactReachableStatesAvailable)
reachableStates = McMddArrayAnd(modelCareStatesArray);
else
reachableStates = mdd_dup(reachableStates);
onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm);
if (onionRings == NIL(array_t)) {
onionRings = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, onionRings, 0, mdd_dup(reachableStates));
}else
onionRings = mdd_array_duplicate(onionRings);
strongSccClosedSets = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, strongSccClosedSets, 0, mdd_dup(reachableStates));
/*
* Compute a series of over-approximated abstract models
*/
numOfLatches = array_n(Fsm_FsmReadPresentStateVars(modelFsm));
maxLatchesToCompose = (numOfLatches * maxComposePercentage/100);
maxLatchesToCompose = (maxLatchesToCompose > 20)? maxLatchesToCompose:20;
composeIncSize = maxLatchesToCompose/10;
composeIncSize = (composeIncSize > 4)? composeIncSize:4;
absLatchNameTableArray =
Mc_CreateStaticRefinementScheduleArray(network,
ctlArray,
NIL(array_t),
NIL(array_t),
FALSE,
FALSE,
((verbosity<McVerbosityMax_c)?
0:McVerbositySome_c),
composeIncSize,
Part_CorrelationWithSupport);
numOfAbstractModels = (array_n(absLatchNameTableArray) - 1);
if (verbosity >= McVerbosityLittle_c) {
fprintf(vis_stdout,
"-- DnC: scheduled total %d abs models with %d latches\n",
numOfAbstractModels, numOfLatches);
}
if (verbosity >= McVerbositySome_c) {
fprintf(vis_stdout, "-- DnC:\n");
fprintf(vis_stdout,
"-- DnC: maxComposePercentage = %d\n", maxComposePercentage);
fprintf(vis_stdout,
"-- DnC: numOfLatches = %d\n", numOfLatches);
fprintf(vis_stdout,
"-- DnC: composeIncSize = %d\n", composeIncSize);
fprintf(vis_stdout,
"-- DnC: numOfAbstractModels = %d\n", numOfAbstractModels);
fprintf(vis_stdout,
"-- DnC: maxLatchesToCompose = %d\n", maxLatchesToCompose);
fprintf(vis_stdout,
"-- DnC: maxSccsToEnum = %d\n", maxSccsToEnum);
fprintf(vis_stdout, "-- Dnc: \n");
}
exitFlag = 0;
for (iter=0; iter<numOfAbstractModels; iter++) {
Fsm_Fsm_t *absFsm = NIL(Fsm_Fsm_t);
st_table *absLatchNameTable = NIL(st_table);
array_t *absOnionRings;
array_t *tempArray = NIL(array_t);
mdd_t *sccClosedSet = NIL(mdd_t);
mdd_t *tempMdd = NIL(mdd_t);
mdd_t *absReachableStates = NIL(mdd_t);
absLatchNameTable = array_fetch(st_table *, absLatchNameTableArray, iter);
absFsm = Fsm_FsmCreateSubsystemFromNetwork(network, NIL(graph_t),
absLatchNameTable, TRUE, 1);
if (!isExactReachableStatesAvailable) {
absReachableStates = Fsm_FsmComputeReachableStates(absFsm, 0, 0, 0, 0,
1, 0, 0,
Fsm_Rch_Default_c,
0, 0,
NIL(array_t), FALSE,
NIL(array_t));
absOnionRings = Fsm_FsmReadReachabilityOnionRings(absFsm);
assert(absOnionRings);
absOnionRings = mdd_array_duplicate(absOnionRings);
}else {
absReachableStates = McComputeAbstractStates(absFsm, reachableStates);
absOnionRings = array_alloc(mdd_t *, array_n(onionRings));
arrayForEachItem(mdd_t *, onionRings, i, tempMdd) {
array_insert(mdd_t *, absOnionRings, i,
McComputeAbstractStates(absFsm, tempMdd) );
}
}
tempArray = strongSccClosedSets;
strongSccClosedSets = array_alloc(mdd_t *, 0);
arrayForEachItem(mdd_t *, tempArray, i, sccClosedSet) {
sccClosedSet = (iter == 0)?
McComputeAbstractStates(absFsm, sccClosedSet): mdd_dup(sccClosedSet);
tempMdd = mdd_and(sccClosedSet, absReachableStates, 1, 1);
if (mdd_is_tautology(tempMdd, 0))
mdd_free(tempMdd);
else
array_insert_last(mdd_t *, strongSccClosedSets, tempMdd);
mdd_free(sccClosedSet);
}
mdd_array_free(tempArray);
/* Refine SCC-closed sets, but up to a certain number */
tempArray = strongSccClosedSets;
strongSccClosedSets = array_alloc(mdd_t *, 0);
Mc_FsmForEachFairScc(absFsm, sccgen, sccClosedSet, tempArray,
strongSccClosedSets, /* new scc-closed sets */
buechiFairness, absOnionRings, FALSE,
((verbosity<McVerbosityMax_c)?
McVerbosityNone_c:McVerbositySome_c),
(Mc_DcLevel) dcLevel) {
if (SccIsStrong(mddManager, buechiFairness, sccClosedSet)) {
array_insert_last(mdd_t *, strongSccClosedSets, sccClosedSet);
if (maxSccsToEnum>0 && array_n(strongSccClosedSets)>maxSccsToEnum) {
Mc_FsmSccGenFree(sccgen, strongSccClosedSets);
break;
}
}else {
array_t *newCareStatesArray;
newCareStatesArray = mdd_array_duplicate(modelCareStatesArray);
if (!isExactReachableStatesAvailable)
array_insert_last(mdd_t *, newCareStatesArray, absReachableStates);
if (verbosity >= McVerbositySome_c)
fprintf(vis_stdout, "-- DnC: search in a weak SCC-closed set\n");
fairStates = McFsmRefineWeakFairSCCs(modelFsm, sccClosedSet,
newCareStatesArray,
arrayOfOnionRings, FALSE,
dcLevel,
((verbosity<McVerbosityMax_c)? 0:McVerbositySome_c) );
fairInitialStates = mdd_and(initialStates, fairStates, 1, 1);
mdd_free(fairStates);
if (!mdd_is_tautology(fairInitialStates, 0)) {
/* Done, find a reachable fair cycle */
exitFlag = 2;
if (verbosity >= McVerbosityLittle_c)
fprintf(vis_stdout, "-- DnC: find a weak SCC!\n");
Mc_FsmSccGenFree(sccgen, NIL(array_t));
break;
}else {
mdd_free(fairInitialStates);
}
}
}/*Mc_FsmForEachFairScc( ) {*/
mdd_array_free(tempArray);
SortMddArrayBySize(absFsm, strongSccClosedSets);
if (verbosity >= McVerbosityLittle_c && exitFlag != 2) {
fprintf(vis_stdout,
"-- DnC: found %d SCC-closed sets in abs model %d with %d latches\n",
array_n(strongSccClosedSets), iter+1,
st_count(absLatchNameTable));
if (verbosity >= McVerbositySome_c) {
array_t *absPSvars = Fsm_FsmReadPresentStateVars(absFsm);
array_t *PSvars = Fsm_FsmReadPresentStateVars(modelFsm);
arrayForEachItem(mdd_t *, strongSccClosedSets, i, tempMdd) {
fprintf(vis_stdout, "-- An SCC-closed set with %5g abs (%5g concrete) states\n",
mdd_count_onset(mddManager, tempMdd, absPSvars),
mdd_count_onset(mddManager, tempMdd, PSvars)
);
}
}
}
if(exitFlag == 0 && array_n(strongSccClosedSets) == 0) {
/* Done, no reachable fair cycle exists */
exitFlag = 1;
}
mdd_array_free(absOnionRings);
Fsm_FsmFree(absFsm);
/* existFlag: 0 --> unknown; 1 --> no fair SCC; 2 --> find a fair SCC */
if ( exitFlag != 0 || st_count(absLatchNameTable) > maxLatchesToCompose ) {
if (!isExactReachableStatesAvailable) {
array_insert_last(mdd_t *, modelCareStatesArray, absReachableStates);
tempMdd = reachableStates;
reachableStates = mdd_and(reachableStates, absReachableStates,1,1);
mdd_free(tempMdd);
}
break;
}
mdd_free(absReachableStates);
}/*for (iter=0; iter<numOfAbstractModels; iter++) {*/
for (i=0; i<array_n(absLatchNameTableArray); i++) {
st_free_table( array_fetch(st_table *, absLatchNameTableArray, i) );
}
array_free(absLatchNameTableArray);
/*
* Compute fair SCCs on the concrete model if necessary
*/
if (exitFlag == 0) {
array_t *tempArray;
mdd_t *sccClosedSet = NIL(mdd_t);
mdd_t *tempMdd = NIL(mdd_t);
if (verbosity >= McVerbosityLittle_c)
fprintf(vis_stdout, "-- DnC: check the concrete model\n");
tempArray = strongSccClosedSets;
strongSccClosedSets = array_alloc(mdd_t *, 0);
arrayForEachItem(mdd_t *, tempArray, i, sccClosedSet) {
tempMdd = mdd_and(sccClosedSet, reachableStates, 1, 1);
if (mdd_is_tautology(tempMdd, 0))
mdd_free(tempMdd);
else
array_insert_last(mdd_t *, strongSccClosedSets, tempMdd);
mdd_free(sccClosedSet);
}
array_free(tempArray);
if (lockstep != MC_LOCKSTEP_OFF) {
tempArray = array_alloc(mdd_t *, 0);
fairStates = McFsmRefineFairSCCsByLockStep(modelFsm, lockstep,
tempArray,
strongSccClosedSets,
NIL(array_t),
arrayOfOnionRings,
(Mc_VerbosityLevel) verbosity,
(Mc_DcLevel) dcLevel);
mdd_array_free(tempArray);
}else{
mdd_t *fairStates0, *sccClosedSet;
array_t *EUonionRings;
mdd_t *mddOne = mdd_one(mddManager);
Mc_EarlyTermination_t *earlyTermination;
sccClosedSet = McMddArrayOr(strongSccClosedSets);
fairStates0 = Mc_FsmEvaluateEGFormula(modelFsm, sccClosedSet,
NIL(mdd_t), mddOne,
modelFairness,
modelCareStatesArray,
MC_NO_EARLY_TERMINATION,
NIL(array_t),
Mc_None_c,
&arrayOfOnionRings,
(Mc_VerbosityLevel) verbosity,
(Mc_DcLevel) dcLevel,
NIL(boolean),
GSHschedule);
mdd_free(sccClosedSet);
EUonionRings = ( (arrayOfOnionRings == NIL(array_t))?
NIL(array_t):array_alloc(mdd_t *,0) );
earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
fairStates = Mc_FsmEvaluateEUFormula(modelFsm, mddOne,
fairStates0, NIL(mdd_t), mddOne,
modelCareStatesArray,
earlyTermination,
NIL(array_t), Mc_None_c,
EUonionRings,
(Mc_VerbosityLevel) verbosity,
(Mc_DcLevel) dcLevel,
NIL(boolean));
mdd_free(fairStates0);
mdd_free(mddOne);
Mc_EarlyTerminationFree(earlyTermination);
if (arrayOfOnionRings != NIL(array_t)) {
int j;
arrayForEachItem(array_t *, arrayOfOnionRings, i, tempArray) {
#ifndef NDEBUG
mdd_t *mdd1 = array_fetch_last(mdd_t *, tempArray);
#endif
arrayForEachItem(mdd_t *, EUonionRings, j, tempMdd) {
if (j != 0)
array_insert_last(mdd_t *, tempArray, mdd_dup(tempMdd));
else
assert( mdd_equal(tempMdd, mdd1) );
}
}
mdd_array_free(EUonionRings);
}
}
fairInitialStates = mdd_and(initialStates, fairStates, 1, 1);
mdd_free(fairStates);
exitFlag = mdd_is_tautology(fairInitialStates, 0)? 1:2;
}
/* Clean-Ups */
mdd_array_free(modelCareStatesArray);
mdd_array_free(strongSccClosedSets);
mdd_array_free(onionRings);
mdd_free(reachableStates);
mdd_free(initialStates);
/*
* Print out the verification result (pass/fail, empty/non-empty)
*/
if (exitFlag == 1) {
if (strcmp(driverName, "LE") == 0)
fprintf(vis_stdout, "# LE: language emptiness check passes\n");
else
fprintf(vis_stdout, "# %s: formula passed\n", driverName);
if (arrayOfOnionRings != NIL(array_t))
mdd_array_array_free(arrayOfOnionRings);
return fairInitialStates;
}else if (exitFlag == 2) {
if (strcmp(driverName, "LE") == 0)
fprintf(vis_stdout, "# LE: language is not empty\n");
else
fprintf(vis_stdout, "# %s: formula failed\n", driverName);
}else {
fprintf(vis_stderr, "* DnC error, result is unknown!\n");
assert(0);
}
/*
* Print out the debugging information if requested
*/
if (dbgLevel == McDbgLevelNone_c) {
if (arrayOfOnionRings != NIL(array_t))
mdd_array_array_free(arrayOfOnionRings);
return fairInitialStates;
}else {
mdd_t *badStates, *aBadState, *mddOne;
McPath_t *fairPath, *normalPath;
array_t *stemArray, *cycleArray;
FILE *tmpFile = vis_stdout;
extern FILE *vis_stdpipe;
fprintf(vis_stdout, "# %s: generating path to fair cycle\n", driverName);
/* Generate witness. */
badStates = mdd_dup(fairInitialStates);
aBadState = Mc_ComputeAState(badStates, modelFsm);
mdd_free(badStates);
mddOne = mdd_one(mddManager);
fairPath = McBuildFairPath(aBadState, mddOne, arrayOfOnionRings, modelFsm,
modelCareStates,
(Mc_VerbosityLevel) verbosity,
(Mc_DcLevel) dcLevel,
McFwd_c);
mdd_free(mddOne);
mdd_free(aBadState);
mdd_array_array_free(arrayOfOnionRings);
/* Print witness. */
normalPath = McPathNormalize(fairPath);
McPathFree(fairPath);
stemArray = McPathReadStemArray(normalPath);
cycleArray = McPathReadCycleArray(normalPath);
/* we should pass dbgFile/UseMore as parameters
dbgFile = McOptionsReadDebugFile(options);*/
if (dbgFile != NIL(FILE)) {
vis_stdpipe = dbgFile;
} else if (UseMore == TRUE) {
vis_stdpipe = popen("more","w");
} else {
vis_stdpipe = vis_stdout;
}
vis_stdout = vis_stdpipe;
/* We should also pass SimValue as a parameter */
if (SimValue == FALSE) {
(void) fprintf(vis_stdout, "# %s: path to fair cycle:\n\n", driverName);
Mc_PrintPath(stemArray, modelFsm, printInputs);
fprintf (vis_stdout, "\n");
(void) fprintf(vis_stdout, "# %s: fair cycle:\n\n", driverName);
Mc_PrintPath(cycleArray, modelFsm, printInputs);
fprintf (vis_stdout, "\n");
}else {
array_t *completePath = McCreateMergedPath(stemArray, cycleArray);
(void) fprintf(vis_stdout, "# %s: counter-example\n", driverName);
McPrintSimPath(vis_stdout, completePath, modelFsm);
mdd_array_free(completePath);
}
if (dbgFile == NIL(FILE) && UseMore == TRUE) {
(void) pclose(vis_stdpipe);
}
vis_stdout = tmpFile;
McPathFree(normalPath);
}
return fairInitialStates;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McComputeAbstractStates | ( | Fsm_Fsm_t * | absFsm, |
| mdd_t * | states | ||
| ) |
Function********************************************************************
Synopsis [Compute the abstract states from the concrete states.]
Description [By existentially quantify out the invisible variables. Invisible variables are those state variables (or latches) that are not in the supports of the abstract states---they have been abstracted away.]
SideEffects []
Definition at line 858 of file mcDnC.c.
{
mdd_t *result;
mdd_manager *mddManager = Fsm_FsmReadMddManager(absFsm);
array_t *psVars = Fsm_FsmReadPresentStateVars(absFsm);
array_t *supportVars;
array_t *invisibleVars = array_alloc(long, 0);
st_table *psVarTable = st_init_table(st_numcmp, st_numhash);
int i;
long mddId;
arrayForEachItem(long, psVars, i, mddId) {
st_insert(psVarTable, (char *)mddId, NIL(char));
}
supportVars = mdd_get_support(mddManager, states);
arrayForEachItem(long, supportVars, i, mddId) {
if (!st_is_member(psVarTable, (char *)mddId))
array_insert_last(long, invisibleVars, mddId);
}
array_free(supportVars);
st_free_table(psVarTable);
result = mdd_smooth(mddManager, states, invisibleVars);
array_free(invisibleVars);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McFsmRefineWeakFairSCCs | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | sccClosedSet, | ||
| array_t * | modelCareStatesArray, | ||
| array_t * | arrayOfOnionRings, | ||
| boolean | isSccTerminal, | ||
| int | dcLevel, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Compute the fair SCCs within the given weak SCC-closed set.]
Description [Used by the Divide and Compose (D'n'C) approach for language emptiness checking. Because it's a weak SCC-closed set, fair states can be computed through the evaluation of EF EG (sccClosedSet).
Debugging information will be returned if arrayOfOnionRings is not NIL.
Return the fair states leading to a fair cycle within the given SCC-closed set.]
SideEffects [arrayOfOnionRings will be changed if it is not NIL and the initial states intersect the fair states.]
Definition at line 757 of file mcDnC.c.
{
mdd_manager *mddManager = Fsm_FsmReadMddManager(modelFsm);
mdd_t *initialStates;
mdd_t *mddOne, *mddEgFair, *mddEfEgFair, *fairInitStates, *mdd1;
array_t *EFonionRings, *EGArrayOfOnionRings, *EGonionRings;
array_t *newOnionRings;
int i, j;
Mc_EarlyTermination_t *earlyTermination;
initialStates = Fsm_FsmComputeInitialStates(modelFsm);
mddOne = mdd_one(mddManager);
/* if debugging information is requested, arrayOfOnionRings!=NIL(array_t) */
if (arrayOfOnionRings != NIL(array_t)) {
EGArrayOfOnionRings = array_alloc(array_t *, 0);
EFonionRings = array_alloc(mdd_t *, 0);
}else {
EGArrayOfOnionRings = NIL(array_t);
EFonionRings = NIL(array_t);
}
if (isSccTerminal)
mddEgFair = mdd_dup(sccClosedSet);
else
mddEgFair = Mc_FsmEvaluateEGFormula(modelFsm, sccClosedSet,
NIL(mdd_t), mddOne,
NIL(Fsm_Fairness_t),
modelCareStatesArray,
NIL(Mc_EarlyTermination_t),
NIL(array_t), Mc_None_c,
&EGArrayOfOnionRings,
(Mc_VerbosityLevel) verbosity,
(Mc_DcLevel) dcLevel,
NIL(boolean), McGSH_EL_c);
earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
mddEfEgFair = Mc_FsmEvaluateEUFormula(modelFsm, mddOne,
mddEgFair, NIL(mdd_t), mddOne,
modelCareStatesArray,
earlyTermination,
NIL(array_t), Mc_None_c,
EFonionRings,
(Mc_VerbosityLevel) verbosity,
(Mc_DcLevel) dcLevel,
NIL(boolean));
mdd_free(mddEgFair);
Mc_EarlyTerminationFree(earlyTermination);
fairInitStates = mdd_and(mddEfEgFair, initialStates, 1, 1);
/* create the arrayOfOnionRings */
if (arrayOfOnionRings!=NIL(array_t) && !mdd_is_tautology(fairInitStates,0)) {
if (isSccTerminal)
array_insert_last(array_t *,
arrayOfOnionRings, mdd_array_duplicate(EFonionRings));
else {
arrayForEachItem(array_t *, EGArrayOfOnionRings, i, EGonionRings) {
newOnionRings = mdd_array_duplicate(EGonionRings);
arrayForEachItem(mdd_t *, EFonionRings, j, mdd1) {
if (j != 0)
array_insert_last(mdd_t *, newOnionRings, mdd_dup(mdd1));
}
array_insert_last(array_t *, arrayOfOnionRings, newOnionRings);
}
}
}
mdd_free(fairInitStates);
if (arrayOfOnionRings != NIL(array_t)) {
mdd_array_free(EFonionRings);
mdd_array_array_free(EGArrayOfOnionRings);
}
mdd_free(initialStates);
mdd_free(mddOne);
return mddEfEgFair;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean McGetDncEnabled | ( | void | ) |
Function********************************************************************
Synopsis [Return true if the Divide and Compose (D'n'C) approach for language emptiness checking is enabled.]
Description [Return true if the D'n'C approach for language emptiness is enabled.]
SideEffects []
Definition at line 903 of file mcDnC.c.
{
char *flagValue;
boolean result = FALSE;
flagValue = Cmd_FlagReadByName("divide_and_compose");
if (flagValue != NIL(char)) {
if (strcmp(flagValue, "true") == 0)
result = TRUE;
else if (strcmp(flagValue, "false") == 0)
result = FALSE;
else {
fprintf(vis_stderr, "** dnc error: invalid dnc_enable flag %s, dnc is disabled. \n", flagValue);
}
}
return result;
}
Here is the call graph for this function:
| static boolean SccIsStrong | ( | mdd_manager * | mddMgr, |
| array_t * | buechiFairness, | ||
| mdd_t * | SCC | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Return true if the given SCC is strong.]
Description [Return true if the given SCC is strong. Note that the check is conservative -- for the purpose of efficiency -- When it returns false, the SCC is definitely weak; when it returns true, the SCC may be still be weak. For the language emptiness checking, this is not going to hurt us.]
SideEffects []
Definition at line 941 of file mcDnC.c.
{
boolean strength;
mdd_t *LabeledAllFairness = mdd_dup(SCC);
mdd_t *NotLabeledAllFairness;
mdd_t *fairSet;
int i;
/*
* check whether SCC intersects all the fairness constraints
* if yes, WEAK
* if no, WEAK or STRONG
*/
arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
mdd_t *tmpMdd = LabeledAllFairness;
LabeledAllFairness = mdd_and(LabeledAllFairness, fairSet, 1,1 );
mdd_free( tmpMdd );
}
NotLabeledAllFairness = mdd_and(SCC, LabeledAllFairness, 1, 0);
mdd_free(LabeledAllFairness);
if(mdd_is_tautology(NotLabeledAllFairness, 0)) {
mdd_free(NotLabeledAllFairness);
strength = FALSE; /* WEAK*/
}
else {
mdd_free(NotLabeledAllFairness);
strength = TRUE;
}
return strength;
}
Here is the caller graph for this function:
| static array_t * SortMddArrayBySize | ( | Fsm_Fsm_t * | fsm, |
| array_t * | mddArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Sort the array of mdds by their number of minterms.]
Description [Sort the array of mdds by their number of minterms. The present state variables of the given FSM is used to count the minterms. The sorting will be skipped if the number of present state variables is larger than 1024.]
SideEffects [array_mdd_compare_size]
Definition at line 1017 of file mcDnC.c.
{
mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
array_t *psVars = Fsm_FsmReadPresentStateVars(fsm);
if (array_n(psVars) < 1024) {
st_table *mddToSizeTable =st_init_table(st_ptrcmp, st_ptrhash);
double *sizes = ALLOC(double, array_n(mddArray));
mdd_t *mdd1;
int i;
arrayForEachItem(mdd_t *, mddArray, i, mdd1) {
*(sizes+i) = mdd_count_onset(mddManager, mdd1, psVars);
st_insert(mddToSizeTable, (char *)mdd1, (char *)(sizes+i));
}
array_mdd_compare_table = mddToSizeTable;
array_sort(mddArray, array_mdd_compare_size);
FREE(sizes);
st_free_table(mddToSizeTable);
}
return mddArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int stringCompare | ( | const void * | s1, |
| const void * | s2 | ||
| ) | [static] |
Variable Documentation
st_table* array_mdd_compare_table = NIL(st_table) [static] |
char rcsid [] UNUSED = "$Id: mcDnC.c,v 1.9 2005/05/18 18:12:00 jinh Exp $" [static] |
CFile***********************************************************************
FileName [mcDnC.c]
PackageName [mc]
Synopsis [The Divide and Compose (D'n'C) Approach of SCC Enumeration.]
Description [This file contains the functions to compute the fair Strongly Connected Components (SCCs) of the state translation graph of an FSM by Divide and Compose. Knowledge of the fair SCCs can be used to decide language emptiness. For more information, please check the CONCUR'01 paper of Wang et al., "Divide and Compose: SCC refinement for language emptiness." Other applications are also possible.]
SeeAlso []
Author [Chao Wang]
Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.]
