#include "amcInt.h"#include "mcInt.h"
Include dependency graph for amcAmc.c:
Go to the source code of this file.
Functions | |
| static int | stringCompare (const void *s1, const void *s2) |
| void | Amc_AmcEvaluateFormula (Ntk_Network_t *network, Ctlp_Formula_t *formula, int verbosity) |
| Amc_Info_t * | Amc_AmcInfoInitialize (Ntk_Network_t *network, Ctlp_Formula_t *formula, Amc_MethodType methodType, int verbosity) |
| mdd_t * | Amc_AmcExistentialQuantifySubsystem (Amc_SubsystemInfo_t *subSystem, array_t *quantifyVars, Amc_QuantificationMode quantificationMode) |
| array_t * | Amc_AmcExistentialQuantifySubsystemArray (array_t *subSystemArray, Amc_SubsystemInfo_t *currentSystem, array_t *quantifyVars, Amc_QuantificationMode quantificationMode) |
| Fsm_Fsm_t * | Amc_AmcSubsystemReadFsm (Amc_SubsystemInfo_t *system) |
| void | Amc_AmcSubsystemSetFsm (Amc_SubsystemInfo_t *system, Fsm_Fsm_t *info) |
| array_t * | Amc_AmcSubsystemReadRelationArray (Amc_SubsystemInfo_t *system) |
| void | Amc_AmcSubsystemSetRelationArray (Amc_SubsystemInfo_t *system, array_t *info) |
| mdd_t * | Amc_AmcSubsystemReadNextStateVarSmoothen (Amc_SubsystemInfo_t *system) |
| void | Amc_AmcSubsystemSetNextStateVarSmoothen (Amc_SubsystemInfo_t *system, mdd_t *info) |
| mdd_t * | Amc_AmcSubsystemReadSatisfy (Amc_SubsystemInfo_t *system) |
| void | Amc_AmcSubsystemSetSatisfy (Amc_SubsystemInfo_t *system, mdd_t *data) |
| st_table * | Amc_AmcSubsystemReadVertexTable (Amc_SubsystemInfo_t *system) |
| void | Amc_AmcSubsystemSetVertexTable (Amc_SubsystemInfo_t *system, st_table *data) |
| st_table * | Amc_AmcSubsystemReadFanInTable (Amc_SubsystemInfo_t *system) |
| void | Amc_AmcSubsystemSetFanInTable (Amc_SubsystemInfo_t *system, st_table *data) |
| st_table * | Amc_AmcSubsystemReadFanOutTable (Amc_SubsystemInfo_t *system) |
| void | Amc_AmcSubsystemSetFanOutTable (Amc_SubsystemInfo_t *system, st_table *data) |
| char * | Amc_AmcSubsystemReadMethodSpecificData (Amc_SubsystemInfo_t *system) |
| void | Amc_AmcSubsystemSetMethodSpecificData (Amc_SubsystemInfo_t *system, char *data) |
| mdd_t * | Amc_AmcReadInitialStates (Amc_Info_t *system) |
| void | Amc_AmcSetInitialStates (Amc_Info_t *system, mdd_t *data) |
| Amc_SubsystemInfo_t * | Amc_AmcReadOptimalSystem (Amc_Info_t *system) |
| void | Amc_AmcSetOptimalSystem (Amc_Info_t *system, Amc_SubsystemInfo_t *data) |
| void * | Amc_AmcReadMethodData (Amc_Info_t *system) |
| void | Amc_AmcSetMethodData (Amc_Info_t *system, void *data) |
| Amc_SubsystemInfo_t * | Amc_AmcSubsystemAllocate (void) |
| Amc_SubsystemInfo_t * | Amc_AmcSubsystemCreate (Fsm_Fsm_t *fsm, mdd_t *satisfyStates, st_table *vertexTable, st_table *fanInTable, st_table *fanOutTable) |
| Amc_SubsystemInfo_t * | Amc_AmcSubsystemDuplicate (Ntk_Network_t *network, Amc_SubsystemInfo_t *subSystem) |
| void | Amc_AmcSubsystemFree (Amc_SubsystemInfo_t *subSystem) |
| void | Amc_AmcSubsystemFreeAlsoPartition (Amc_SubsystemInfo_t *subSystem) |
| Amc_SubsystemInfo_t * | Amc_CombineSubsystems (Ntk_Network_t *network, Amc_SubsystemInfo_t *subSystem1, Amc_SubsystemInfo_t *subSystem2) |
| mdd_t * | Amc_AmcEvaluateCTLFormula (Amc_SubsystemInfo_t *subSystem, array_t *subSystemArray, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, mdd_t *modelCareStates, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| mdd_t * | Amc_AmcEvaluateEXFormula (Fsm_Fsm_t *modelFsm, array_t *subSystemArray, Amc_SubsystemInfo_t *subSystem, mdd_t *targetMdd, mdd_t *fairStates, mdd_t *careStates, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| mdd_t * | Amc_AmcEvaluateEUFormula (Fsm_Fsm_t *modelFsm, array_t *subSystemArray, Amc_SubsystemInfo_t *subSystem, mdd_t *invariantMdd, mdd_t *targetMdd, mdd_t *fairStates, mdd_t *careStates, array_t *onionRings, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| mdd_t * | Amc_AmcEvaluateEGFormula (Fsm_Fsm_t *modelFsm, array_t *subSystemArray, Amc_SubsystemInfo_t *subSystem, mdd_t *invariantMdd, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, mdd_t *careStates, array_t *onionRingsArrayForDbg, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| array_t * | AmcCreateSubsystemArray (Ntk_Network_t *network, Ctlp_Formula_t *formula) |
| void | AmcPrintOptimalSystem (FILE *fp, Amc_Info_t *amcInfo) |
| mdd_t * | AmcModelCheckAtomicFormula (Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: amcAmc.c,v 1.57 2005/04/16 04:22:41 fabio Exp $" |
Function Documentation
| mdd_t* Amc_AmcEvaluateCTLFormula | ( | Amc_SubsystemInfo_t * | subSystem, |
| array_t * | subSystemArray, | ||
| Ctlp_Formula_t * | ctlFormula, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | fairCondition, | ||
| mdd_t * | modelCareStates, | ||
| boolean | lowerBound, | ||
| array_t * | quantifyVars, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Model check formula with approxmiations.]
Description [The routine evaluates given formula with approximations.]
Comment []
SideEffects []
Definition at line 1328 of file amcAmc.c.
{
Fsm_Fsm_t *modelFsm = Amc_AmcSubsystemReadFsm(subSystem);
mdd_t *leftMdd = NIL(mdd_t);
mdd_t *rightMdd = NIL(mdd_t);
mdd_t *result = NIL(mdd_t);
mdd_t *tmpResult = NIL(mdd_t);
mdd_t *ctlFormulaStates = Ctlp_FormulaObtainStates(ctlFormula );
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
mdd_t *careStates = NIL(mdd_t);
if (ctlFormulaStates) {
return ctlFormulaStates;
}
{
Ctlp_Formula_t *leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
if (leftChild) {
leftMdd = Amc_AmcEvaluateCTLFormula(subSystem, subSystemArray, leftChild, fairStates, fairCondition,
modelCareStates, lowerBound, quantifyVars, verbosity, dcLevel);
if (!leftMdd)
return NIL(mdd_t);
}
}
{
Ctlp_Formula_t *rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
if (rightChild) {
rightMdd = Amc_AmcEvaluateCTLFormula(subSystem, subSystemArray, rightChild, fairStates, fairCondition,
modelCareStates, lowerBound, quantifyVars, verbosity, dcLevel);
if (!rightMdd )
return NIL(mdd_t);
}
}
careStates = (modelCareStates != NIL(mdd_t)) ? mdd_dup(modelCareStates) : mdd_one(mddMgr);
switch ( Ctlp_FormulaReadType( ctlFormula ) ) {
case Ctlp_ID_c : tmpResult = AmcModelCheckAtomicFormula( modelFsm, ctlFormula );
/* #AMC : Obtain lowerbound of the constraint set. */
if(0 && lowerBound) { /*Chao: this is not correct! consider !EF(!p) */
array_t *quantifyPresentVars = array_fetch(array_t *, quantifyVars, 0);
int numOfPresentQuantifyVars = array_n(quantifyPresentVars);
/*
* Currently VIS does not allow primary input as the variable of
* the atomic propositions.
*/
if(numOfPresentQuantifyVars > 0) {
result = mdd_consensus(mddMgr, tmpResult, quantifyPresentVars);
mdd_free(tmpResult);
}
else
result = tmpResult;
}
else
result = tmpResult;
break;
case Ctlp_TRUE_c : result = mdd_one( mddMgr ); break;
case Ctlp_FALSE_c : result = mdd_zero( mddMgr ); break;
case Ctlp_NOT_c : result = mdd_not( leftMdd ); break;
case Ctlp_EQ_c : result = mdd_xnor( leftMdd, rightMdd ); break;
case Ctlp_XOR_c : result = mdd_xor( leftMdd, rightMdd ); break;
case Ctlp_THEN_c : result = mdd_or( leftMdd, rightMdd, 0, 1 ); break;
case Ctlp_AND_c: result = mdd_and( leftMdd, rightMdd, 1, 1 ); break;
case Ctlp_OR_c: result = mdd_or( leftMdd, rightMdd, 1, 1 ); break;
case Ctlp_EX_c:
result = Amc_AmcEvaluateEXFormula( modelFsm, subSystemArray, subSystem, leftMdd, fairStates,
careStates, lowerBound, quantifyVars, verbosity, dcLevel );
break;
case Ctlp_EU_c: {
array_t *onionRings = array_alloc( mdd_t *, 0 );
result = Amc_AmcEvaluateEUFormula( modelFsm, subSystemArray, subSystem, leftMdd, rightMdd, fairStates,
careStates, onionRings, lowerBound, quantifyVars, verbosity, dcLevel );
Ctlp_FormulaSetDbgInfo( ctlFormula, (void *) onionRings, McFormulaFreeDebugData);
break;
}
case Ctlp_EG_c: {
array_t *arrayOfOnionRings = array_alloc( array_t *, 0 );
result = Amc_AmcEvaluateEGFormula( modelFsm, subSystemArray, subSystem, leftMdd,
fairStates, fairCondition, careStates,
arrayOfOnionRings, lowerBound, quantifyVars, verbosity, dcLevel );
Ctlp_FormulaSetDbgInfo( ctlFormula, (void *) arrayOfOnionRings, McFormulaFreeDebugData);
break;
}
default: fail("Encountered unknown type of CTL formula\n");
}
Ctlp_FormulaSetStates( ctlFormula, result );
mdd_free( careStates );
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Amc_AmcEvaluateEGFormula | ( | Fsm_Fsm_t * | modelFsm, |
| array_t * | subSystemArray, | ||
| Amc_SubsystemInfo_t * | subSystem, | ||
| mdd_t * | invariantMdd, | ||
| mdd_t * | fairStates, | ||
| Fsm_Fairness_t * | modelFairness, | ||
| mdd_t * | careStates, | ||
| array_t * | onionRingsArrayForDbg, | ||
| boolean | lowerBound, | ||
| array_t * | quantifyVars, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Evaluate EG formula with approximations.]
Description []
SideEffects []
Definition at line 1895 of file amcAmc.c.
{
int i;
array_t *onionRings = NIL(array_t);
array_t *tmpOnionRingsArrayForDbg = NIL(array_t);
mdd_manager *mddManager = Fsm_FsmReadMddManager( modelFsm );
mdd_t *mddOne = mdd_one( mddManager );
mdd_t *Zmdd;
array_t *buchiFairness = array_alloc( mdd_t *, 0 );
if (modelFairness) {
if ( !Fsm_FairnessTestIsBuchi( modelFairness ) ) {
(void) fprintf(vis_stdout, "#** mc error: non Buchi fairness constraints not supported\n");
return NIL(mdd_t);
}
else {
int j;
int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct( modelFairness, 0 );
array_t *careStatesArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, careStatesArray, 0, careStates);
for( j = 0 ; j < numBuchi; j++ ) {
mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness,
0, j, careStatesArray,
dcLevel);
array_insert_last( mdd_t *, buchiFairness, tmpMdd );
}
array_free(careStatesArray);
}
}
else {
array_insert_last( mdd_t *, buchiFairness, mdd_one(mddManager) );
}
if ( onionRingsArrayForDbg !=NIL(array_t) ) {
tmpOnionRingsArrayForDbg = array_alloc( array_t *, 0 );
}
Zmdd = mdd_dup( invariantMdd );
while (TRUE) {
mdd_t *ZprimeMdd = mdd_dup(Zmdd);
mdd_t *conjunctsMdd = NIL(mdd_t);
mdd_t *AAmdd = mdd_dup(Zmdd);
for ( i = 0 ; i < array_n( buchiFairness ) ; i++ ) {
mdd_t *aMdd, *bMdd, *cMdd;
mdd_t *FiMdd = array_fetch( mdd_t *, buchiFairness, i );
if ( tmpOnionRingsArrayForDbg ) {
onionRings = array_alloc( mdd_t *, 0 );
array_insert_last( array_t *, tmpOnionRingsArrayForDbg, onionRings );
}
/* aMdd = mdd_and( FiMdd, Zmdd, 1, 1); */
aMdd = mdd_and( FiMdd, AAmdd, 1, 1);
bMdd = Amc_AmcEvaluateEUFormula( modelFsm, subSystemArray, subSystem, AAmdd, aMdd, mddOne, careStates,
onionRings, lowerBound, quantifyVars, verbosity, dcLevel );
mdd_free(aMdd);
cMdd = Amc_AmcEvaluateEXFormula( modelFsm, subSystemArray, subSystem, bMdd, mddOne, careStates,
lowerBound, quantifyVars, verbosity, dcLevel );
mdd_free(bMdd);
if ( conjunctsMdd == NIL(mdd_t) ) {
conjunctsMdd = mdd_dup( cMdd );
mdd_free( AAmdd ); AAmdd = mdd_and( conjunctsMdd, invariantMdd,1 ,1 );
}
else {
mdd_t *tmpMdd = mdd_and( cMdd, conjunctsMdd, 1, 1 );
mdd_free( conjunctsMdd );
conjunctsMdd = tmpMdd;
mdd_free( AAmdd ); AAmdd = mdd_and( conjunctsMdd, invariantMdd,1 ,1 );
}
mdd_free( cMdd );
}
mdd_free(AAmdd);
mdd_free(ZprimeMdd);
ZprimeMdd = mdd_and( invariantMdd, conjunctsMdd, 1, 1 );
mdd_free( conjunctsMdd );
if ( mdd_equal_mod_care_set( ZprimeMdd, Zmdd, careStates ) ) {
mdd_free( ZprimeMdd );
break;
}
mdd_free( Zmdd );
Zmdd = ZprimeMdd;
if ( tmpOnionRingsArrayForDbg ) {
arrayForEachItem(array_t *, tmpOnionRingsArrayForDbg, i, onionRings ) {
mdd_array_free( onionRings );
}
array_free( tmpOnionRingsArrayForDbg );
tmpOnionRingsArrayForDbg = array_alloc( array_t *, 0 );
}
}
if ( onionRingsArrayForDbg != NIL(array_t) ) {
arrayForEachItem(array_t *, tmpOnionRingsArrayForDbg, i, onionRings ) {
array_insert_last( array_t *, onionRingsArrayForDbg, onionRings );
}
array_free( tmpOnionRingsArrayForDbg );
}
if ( ( verbosity == McVerbositySome_c ) || ( verbosity == McVerbosityMax_c ) ) {
{
for ( i = 0 ; i < array_n( onionRingsArrayForDbg ); i++ ) {
int j;
mdd_t *Fi = array_fetch( mdd_t *, buchiFairness, i );
array_t *onionRings = array_fetch( array_t *, onionRingsArrayForDbg, i );
for( j = 0 ; j < array_n( onionRings ) ; j++ ) {
mdd_t *ring = array_fetch( mdd_t *, onionRings, j );
if ( j == 0 ) {
if ( ! mdd_lequal( ring, Fi, 1, 1 ) ) {
fprintf( vis_stderr, "Problem w/ dbg - inner most ring not in Fi\n");
}
}
if ( ! mdd_lequal( ring, Zmdd, 1, 1 ) ) {
fprintf( vis_stderr, "Problem w/ dbg - onion ring fails invariant\n");
}
}
}
}
{
mdd_t *tmpMdd = careStates ? mdd_and( Zmdd, careStates, 1, 1 ) : mdd_dup( Zmdd );
fprintf(vis_stdout, "--There are %.0f states satisfying EG formula\n",
mdd_count_onset( Fsm_FsmReadMddManager( modelFsm ), tmpMdd,
Fsm_FsmReadPresentStateVars( modelFsm ) ) );
mdd_free( tmpMdd );
}
}
mdd_array_free( buchiFairness );
mdd_free( mddOne );
return Zmdd;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Amc_AmcEvaluateEUFormula | ( | Fsm_Fsm_t * | modelFsm, |
| array_t * | subSystemArray, | ||
| Amc_SubsystemInfo_t * | subSystem, | ||
| mdd_t * | invariantMdd, | ||
| mdd_t * | targetMdd, | ||
| mdd_t * | fairStates, | ||
| mdd_t * | careStates, | ||
| array_t * | onionRings, | ||
| boolean | lowerBound, | ||
| array_t * | quantifyVars, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Evaluate EU formula with approximations.]
Description []
Comment []
SideEffects []
Definition at line 1805 of file amcAmc.c.
{
mdd_t *aMdd;
mdd_t *bMdd;
mdd_t *cMdd;
mdd_t *resultMdd = mdd_and( targetMdd, fairStates, 1, 1 );
mdd_t *ringMdd = mdd_dup( resultMdd );
while (TRUE) {
if ( onionRings ) {
array_insert_last( mdd_t *, onionRings, mdd_dup( resultMdd ) );
}
/*
* When trying to use dont cares to the hilt,
* use a bdd between succ iterations -> ringMdd
*/
aMdd = Amc_AmcEvaluateEXFormula( modelFsm, subSystemArray, subSystem, ringMdd, fairStates, careStates,
lowerBound, quantifyVars, verbosity, dcLevel );
mdd_free( ringMdd );
bMdd = mdd_and( aMdd, invariantMdd, 1, 1 );
cMdd = mdd_or( resultMdd, bMdd, 1, 1 );
mdd_free( aMdd );
mdd_free( bMdd );
if ( mdd_equal_mod_care_set( cMdd, resultMdd, careStates ) ) {
mdd_free( cMdd );
break;
}
if ( dcLevel >= McDcLevelRchFrontier_c ) {
mdd_t *tmpMdd = mdd_and( resultMdd, cMdd, 0, 1 );
ringMdd = bdd_between( tmpMdd, cMdd );
if ( verbosity == McVerbosityMax_c ) {
fprintf(vis_stdout, "-- EU |A(n+1)-A(n)| = %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
mdd_size( tmpMdd ), mdd_size( resultMdd ), mdd_size( ringMdd ) );
}
mdd_free( tmpMdd );
}
else {
ringMdd = mdd_dup( cMdd );
if ( verbosity == McVerbosityMax_c ) {
fprintf(vis_stdout, "-- EU |ringMdd| = %d\n", mdd_size( ringMdd ) );
}
}
mdd_free( resultMdd );
resultMdd = cMdd;
}
if ( ( verbosity == McVerbosityMax_c ) ) {
static int refCount=0;
mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );
mdd_t *tmpMdd = careStates ? mdd_and( resultMdd, careStates, 1, 1 ) : mdd_dup( resultMdd );
fprintf(vis_stdout, "--EU called %d (bdd_size - %d)\n", ++refCount, mdd_size( resultMdd ) );
fprintf(vis_stdout, "--There are %.0f care states satisfying EU formula\n",
mdd_count_onset( mddMgr, tmpMdd, psVars ) );
mdd_free(tmpMdd);
}
return resultMdd;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Amc_AmcEvaluateEXFormula | ( | Fsm_Fsm_t * | modelFsm, |
| array_t * | subSystemArray, | ||
| Amc_SubsystemInfo_t * | subSystem, | ||
| mdd_t * | targetMdd, | ||
| mdd_t * | fairStates, | ||
| mdd_t * | careStates, | ||
| boolean | lowerBound, | ||
| array_t * | quantifyVars, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Evaluate EX formula with approximations.]
Description [The routine evaluates EX formula with approximations. The routine is used both to obtain lower- and upper- bound of the exact preimage.
Chao: Let's use the following symbols to represent the present-state vars, next-state vars, and the input vars: s -- Present-State Vars t -- Next-State Vars x -- Input Vars s_A,t_A -- PS or NS vars in the abstract model s_R,t_R -- PS or NS vars in the remaining models T -- Transition Relation of the concrete model, T = T_A * T_R T_A,T_R -- TR of the abstract model or the remaining models
The upper-bound EX computation is (s_R) ( (t,x) (T_A(s,x,t_A) * C(t)) )
The lower-bound EX computation is (s_R) ( (t_A,x) ( T_A(s,x,t_A) * ( (t_R) C(t)) ) ]
SideEffects []
SeeAlso [AmcInitializeQuantifyVars]
Definition at line 1474 of file amcAmc.c.
{
/*
* The care set consists of the passed careStates
*/
mdd_t *toCareSet = mdd_dup( careStates );
mdd_t *fromLowerBound;
mdd_t *fromUpperBound;
mdd_t *result = NIL(mdd_t);
mdd_t *tmpResult;
mdd_manager *mddManager = Fsm_FsmReadMddManager( modelFsm );
array_t *quantifyPresentVars = array_fetch(array_t *, quantifyVars, 0);
Img_ImageInfo_t * imageInfo;
assert(quantifyPresentVars != NIL(array_t));
imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 1);
if ( dcLevel == McDcLevelRchFrontier_c ) {
/*
* The lower bound is the conjunction of the fair states,
* the target states, and the care states.
*/
mdd_t *tmpMdd = mdd_and( targetMdd, fairStates, 1, 1 );
fromLowerBound = mdd_and( tmpMdd, careStates, 1, 1 );
mdd_free( tmpMdd );
/*
* The upper bound is the OR of the lower bound with the
* complement of the care states.
*/
fromUpperBound = mdd_or( fromLowerBound, careStates, 1, 0 );
}
else {
/*
* The lower bound is the conjunction of the fair states,
* and the target states.
*/
fromLowerBound = mdd_and( targetMdd, fairStates, 1, 1 );
/*
* The upper bound is the same as the lower bound.
*/
fromUpperBound = mdd_dup( fromLowerBound );
}
/***************************************************************************
* compute C1(s) =
* C(s) for upper-bound EX computation
* ( \forall (s_R) C(s) ) for lower-bound EX computation
***************************************************************************/
if (lowerBound) {
mdd_t *mdd1, *mdd2;
mdd1 = fromLowerBound;
mdd2 = fromUpperBound;
if (array_n(quantifyPresentVars) > 0) {
fromLowerBound = mdd_consensus(mddManager, fromLowerBound,
quantifyPresentVars);
} else {
fromLowerBound = mdd_dup(fromLowerBound);
}
if (mdd_equal(mdd1, mdd2)) {
fromUpperBound = mdd_dup(fromLowerBound);
}else {
if (array_n(quantifyPresentVars) > 0) {
fromUpperBound = mdd_consensus(mddManager, fromUpperBound,
quantifyPresentVars);
} else {
fromUpperBound = mdd_dup(fromUpperBound);
}
}
mdd_free(mdd1);
mdd_free(mdd2);
}
/***************************************************************************
* Compute \exist (t,x) ( T_A(s,x,t_A) * C1(t) ), where
* C1(t) = C(t) for upper-bound EX
* C1(t) = (\forall (t_R) C(t) ) for lower-bound EX
***************************************************************************/
tmpResult = Img_ImageInfoComputeBwdWithDomainVars( imageInfo,
fromLowerBound,
fromUpperBound,
toCareSet );
/***************************************************************************
* Compute the final result
* \exist (s_R) (tmpResult(s)) for upper-bound EX
* \forall (s_R) (tmpResult(s)) for lower-bound EX
**************************************************************************/
if (lowerBound) {
if (array_n(quantifyPresentVars) > 0) {
result = mdd_consensus(mddManager, tmpResult, quantifyPresentVars);
} else {
result = mdd_dup(tmpResult);
}
}else {
result = mdd_dup(tmpResult);
/* result = mdd_smooth(mddManager, tmpResult, quantifyPresentVars);*/
}
mdd_free(tmpResult);
mdd_free( fromLowerBound );
mdd_free( fromUpperBound );
mdd_free( toCareSet );
if ( verbosity == McVerbosityMax_c ) {
static int refCount = 0;
mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );
mdd_t *tmpMdd = careStates ? mdd_and( result, careStates, 1, 1 ) : mdd_dup( result );
fprintf(vis_stdout, "--EX called %d (bdd_size - %d)\n", ++refCount, mdd_size( result ) );
fprintf(vis_stdout, "--There are %.0f care states satisfying EX formula\n",
mdd_count_onset( mddMgr, tmpMdd, psVars ) );
mdd_free(tmpMdd);
}
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Amc_AmcEvaluateFormula | ( | Ntk_Network_t * | network, |
| Ctlp_Formula_t * | formula, | ||
| int | verbosity | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Evaluate formula with approximations.]
Description [Starting from an initial coarse approximation, find an approximation that produces reliable result. The degree of approximation is determined by the number of vertices contained in a subsystem. The initial number of vertices in a subsystem is set by "amc_sizeof_group" environment. The algorithm searches a virtual lattice of approximations in which the level of the lattice is defined as the degree of approximations. Once the approximations in a certain level fails to prove the formula, the algorithm automatically refines the approximation by combining(taking the synchronous product) of subsystems. It repeats the process until the approximation is refined enough to produce a reliable result. The procedure may also be viewed as finding a pseudo-optimal path starting from the coarse approximations(in level 1 of the lattice of approximations) to the approximations that produce reliable result. One can draw a virtual contour separating the approximations that produce faulty results and the reliable results. We call this virtual placement of the approximations and the contour separting the two regions, a lattice of approximations. The algorithms are dual. Each algorithm makes its effort to prove whether the formula is positive or negative respectively. When proving true positive of given ACTL formula we use over-approximation of the transition relation, and to prove true negative, we use under-approximation of the transition relation.]
SideEffects []
SeeAlso []
Definition at line 94 of file amcAmc.c.
{
Amc_Info_t *amcInfo;
int levelOfLattice;
char *flagValue;
long initialTime = 0;
long finalTime;
/*
* If the partition was not created, get out. We are assuming we were able to
* construct BDD for each combinational outputs.
*/
graph_t *partition = Part_NetworkReadPartition(network);
if (partition == NIL(graph_t)) {
error_append("** amc error: Network has no partition. Cannot apply approximate model checking.");
return;
}
/*
* Initialize data structures.
*/
amcInfo = Amc_AmcInfoInitialize(network, formula, Amc_Default_c, verbosity);
/*
* Check every possible environment variables that user may have set.
* And give user some assurance by reporting the flag values.
* Explanation of possible environment variables are discussed in the
* man page of the package.
*/
amcInfo->isMBM = 0;
flagValue = Cmd_FlagReadByName("amc_prove_false");
if (flagValue == NIL(char)){
amcInfo->lowerBound = 0;
fprintf(vis_stdout, "\n#AMC: Proving whether the formula is true.\n");
}
else {
amcInfo->lowerBound = 1;
fprintf(vis_stdout, "\n#AMC: Proving whether the formula is false.\n");
}
if(verbosity) {
flagValue = Cmd_FlagReadByName("amc_grouping_method");
if (flagValue == NIL(char)){
amcInfo->groupingMethod = 0;
fprintf(vis_stdout, "\n#AMC: No grouping method has been set.");
}
else {
amcInfo->groupingMethod = 1;
fprintf(vis_stdout, "\n#AMC: Using latch dependency method for grouping latches into subsystems.");
}
}
/*
* The lattice of approximation algorithm.
*/
levelOfLattice = array_n(amcInfo->subSystemArray);
amcInfo->currentLevel = 1;
while(levelOfLattice >= amcInfo->currentLevel) {
if(verbosity) {
(void)fprintf(vis_stdout, "\n\n##AMC: Entering level %d(%d) of the lattice of approximations\n",
amcInfo->currentLevel, levelOfLattice);
fflush(vis_stdout);
}
initialTime = util_cpu_time();
if( (!(*amcInfo->amcBoundProc)(amcInfo, formula, verbosity)) && !(amcInfo->isVerified) ) {
/* Automatically switches to lattice of lowerbound approximations */
if(verbosity)
(void)fprintf(vis_stdout, "Abandoning upper bound approximations.\n");
/* Free all */
(*amcInfo->amcFreeProc)(amcInfo);
amcInfo = Amc_AmcInfoInitialize(network, formula, Amc_Default_c, verbosity);
amcInfo->lowerBound = TRUE;
amcInfo->currentLevel = 0;
}
else if(amcInfo->isVerified) {
finalTime = util_cpu_time();
if(verbosity == Amc_VerbosityVomit_c) {
(void) fprintf(vis_stdout, "\n%-20s%10ld\n", "analysis time =",
(finalTime - initialTime) / 1000);
}
if(amcInfo->amcAnswer == Amc_Verified_True_c) {
(void) fprintf(vis_stdout, "\n# AMC: Verified formula TRUE at level %d of %d : ",
amcInfo->currentLevel, levelOfLattice);
}else if(amcInfo->amcAnswer == Amc_Verified_False_c) {
(void) fprintf(vis_stdout, "\n# AMC: Verified formula FALSE at level %d of %d : ",
amcInfo->currentLevel, levelOfLattice);
}else{
fprintf(vis_stdout, "\n# AMC: formula unknown --- ");
Ctlp_FormulaPrint( vis_stdout, Ctlp_FormulaReadOriginalFormula( formula ) );
(void) fprintf(vis_stdout, "\n# AMC: Verified formula UNKNOWN at level %d of %d : ",
amcInfo->currentLevel, levelOfLattice);
}
(void) fprintf(vis_stdout, "\n# AMC: ");
Ctlp_FormulaPrint( vis_stdout, Ctlp_FormulaReadOriginalFormula( formula ) );
AmcPrintOptimalSystem(vis_stdout, amcInfo);
(*amcInfo->amcFreeProc)(amcInfo);
return;
} /* end of else if(amcInfo->isVerified) */
amcInfo->currentLevel++;
} /* end of while(levelOfLattice >= amcInfo->currentLevel) */
finalTime = util_cpu_time();
if(verbosity == Amc_VerbosityVomit_c) {
(void) fprintf(vis_stdout, "\n%-20s%10ld\n", "analysis time =",
(finalTime - initialTime) / 1000);
}
/*
** Now, spec was not verified becase there was an error in computation.
*/
(void) fprintf(vis_stdout, "\n# AMC: The spec was not able to be verified.\n# AMC: ");
Ctlp_FormulaPrint( vis_stdout, Ctlp_FormulaReadOriginalFormula( formula ) );
(*amcInfo->amcFreeProc)(amcInfo);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Amc_AmcExistentialQuantifySubsystem | ( | Amc_SubsystemInfo_t * | subSystem, |
| array_t * | quantifyVars, | ||
| Amc_QuantificationMode | quantificationMode | ||
| ) |
Function********************************************************************
Synopsis [Apply existential quantification over a subsystem.]
Description [Given a subsystem, the routine existentially quantify the MDD variables from the transition relation of the subsystem. The return value is the resulting MDD. There are four quantification modes;
- Amc_PresentVars_c
Existentially quantify present state variables.
- Amc_NextVars_c
Existentially quantify next state variables.
- Amc_InputVars_c
Existentially quantify input variables.
- Amc_User_c
Existentially quantify variables provide by the user. In this mode user has to provide the array of MDD IDs to the function. If the user does not provide the array of MDD IDs, the function just returns the transition relation of the subsystem.
]
SideEffects []
SeeAlso [Amc_SubsystemInfo, AmcInitializeQuantifyVars]
Definition at line 384 of file amcAmc.c.
{
Fsm_Fsm_t *subSystemFsm = AmcSubsystemReadFsm(subSystem);
Ntk_Network_t *network = Fsm_FsmReadNetwork(subSystemFsm);
mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
graph_t *partition = Part_NetworkReadPartition(network);
mdd_t *result;
array_t *transitionRelationArray = Amc_AmcSubsystemReadRelationArray(subSystem);
if( transitionRelationArray == NIL(array_t) ) {
/* Build the transition relation of this subsystem. */
st_table *vertexTable = AmcSubsystemReadVertexTable(subSystem);
st_generator *stGen;
char *latchName;
transitionRelationArray = array_alloc(mdd_t *, 0);
st_foreach_item(vertexTable, stGen, &latchName, NIL(char *)) {
Ntk_Node_t *latch = Ntk_NetworkFindNodeByName(network, latchName);
int functionMddId = Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch));
char *nameLatchDataInput = Ntk_NodeReadName(Ntk_LatchReadDataInput(latch));
vertex_t *ptrVertex = Part_PartitionFindVertexByName(partition, nameLatchDataInput);
Mvf_Function_t *nextStateFunction;
mdd_t *transitionRelation;
nextStateFunction = Part_VertexReadFunction(ptrVertex);
transitionRelation = Mvf_FunctionBuildRelationWithVariable(nextStateFunction,
functionMddId);
#ifdef AMC_DEBUG
{
int y, mddId; array_t *supportOfRelation;
fprintf(vis_stdout, "\nThe transition relation of the output function of the node : %s", latchName);
supportOfRelation = mdd_get_support(mddManager, transitionRelation);
arrayForEachItem(int, supportOfRelation, y, mddId) {
Ntk_Node_t *supportNode = Ntk_NetworkFindNodeByMddId(network, mddId);
fprintf(vis_stdout, "\n\tThe node in the support : %s",
Ntk_NodeReadName(supportNode));
}
}
#endif
if( nextStateFunction == NIL(Mvf_Function_t) ) {
error_append("** amc error: Build partition before running approximate model checker.");
return NIL(mdd_t);
}
array_insert_last(mdd_t *, transitionRelationArray, transitionRelation);
} /* end of st_foreach_item */
/* Cache the transition relation of the subsystem. */
Amc_AmcSubsystemSetRelationArray(subSystem, transitionRelationArray);
} /* end of transition relation construction. */
/*
* Notice : The present and next state variable of a subsystem is identical
* to that of the original system. The subsystem carries the subset of the
* output functions of the original system.
*/
if( quantificationMode == Amc_User_c ) {
/* result = Img_MultiwayLinearAndSmooth(mddManager, transitionRelationArray, quantifyVars,
NIL(array_t)); */
if( AmcSubsystemReadNextStateVarSmoothen(subSystem) == NIL(mdd_t) ) {
result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, quantifyVars);
AmcSubsystemSetNextStateVarSmoothen(subSystem, result);
}
else {
result = AmcSubsystemReadNextStateVarSmoothen(subSystem);
}
}
else if( quantificationMode == Amc_PresentVars_c ) {
array_t *presentVars = Fsm_FsmReadPresentStateVars(subSystemFsm);
result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, presentVars);
}
else if( quantificationMode == Amc_NextVars_c ) {
array_t *nextVars = Fsm_FsmReadNextStateVars(subSystemFsm);
result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, nextVars);
}
else if( quantificationMode == Amc_InputVars_c ) {
array_t *inputVars = Fsm_FsmReadInputVars(subSystemFsm);
result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, inputVars);
}
else {
error_append("** amc error: Invalid quantification mode.");
return NIL(mdd_t);
}
return(result);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Amc_AmcExistentialQuantifySubsystemArray | ( | array_t * | subSystemArray, |
| Amc_SubsystemInfo_t * | currentSystem, | ||
| array_t * | quantifyVars, | ||
| Amc_QuantificationMode | quantificationMode | ||
| ) |
Function********************************************************************
Synopsis [Apply existential quantification to the array of subsystems.]
Description [Given an array of subsystems, the routine existentially quantifies the MDD variables from the transition relations of the subsystems. The existential quantification is applied to the subsystems that hasn't yet been taken into the optimal system. The optimal system is the group of subsystems that has been synchronously combined. There are four quantification modes;
- Amc_PresentVars_c
Existentially quantify present state variables.
- Amc_NextVars_c
Existentially quantify next state variables.
- Amc_InputVars_c
Existentially quantify input variables.
- Amc_User_c
Existentially quantify variables provide by the user. In this mode user has to provide the array of MDD IDs to the function. If the user does not provide the array of MDD IDs, the function just returns the transition relation of the subsystem.
The return value is the array of quantified result of the MDD representation of the transition relation. ]
SideEffects []
SeeAlso [Amc_SubsystemInfo, Amc_AmcExistentialQuantifySubsystem]
Definition at line 518 of file amcAmc.c.
{
int i;
Amc_SubsystemInfo_t *subSystem;
mdd_t *quantifiedSystemMdd;
array_t *quantifiedSystemMddArray = array_alloc(mdd_t *, 0);
if( (quantificationMode == Amc_User_c) && (quantifyVars == NIL(array_t)) ) {
error_append("** amc error: Subsystem has no output functions.");
return NIL(array_t);
}
arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
if( (!subSystem->takenIntoOptimal) && (i != currentSystem->takenIntoOptimal) ) {
quantifiedSystemMdd =
Amc_AmcExistentialQuantifySubsystem(subSystem, quantifyVars,
quantificationMode);
array_insert_last(mdd_t *, quantifiedSystemMddArray, quantifiedSystemMdd);
}
}
return(quantifiedSystemMddArray);
}
Here is the call graph for this function:
| Amc_Info_t* Amc_AmcInfoInitialize | ( | Ntk_Network_t * | network, |
| Ctlp_Formula_t * | formula, | ||
| Amc_MethodType | methodType, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Initializes an amcInfo structure for the given method.]
Description [Regardless of the method type, the initialization procedure starts from constructing set of subsystems. A subsystem contains a subset of vertices of the partition. Based on the subset of vertices, subFSM is created. The subsystems are stored as an array. After the creation of the subsystem array, the function initializes remaining field of (Amc_Info_t *) amcInfo. The function returns initialized (Amc_Info_t *) amcInfo.]
SideEffects []
SeeAlso []
Definition at line 252 of file amcAmc.c.
{
Amc_Info_t *amcInfo;
char *userSpecifiedMethod;
amcInfo = ALLOC(Amc_Info_t, 1);
amcInfo->network = network;
/*
* AmcCreateSubsystems creates fsm for each subsystem and returns subSystemArray.
*/
amcInfo->subSystemArray = AmcCreateSubsystemArray(network, formula);
#ifdef AMC_DEBUG
AmcCheckSupportAndOutputFunctions(amcInfo->subSystemArray);
#endif
/*
* Initialize optimalSystem, isVerified;
*/
amcInfo->optimalSystem = NIL(Amc_SubsystemInfo_t);
amcInfo->isVerified = 0;
amcInfo->amcAnswer = Amc_Verified_Unknown_c;
/*
* If methodType is default, use user-specified method.
*/
if (methodType == Amc_Default_c) {
userSpecifiedMethod = Cmd_FlagReadByName("amc_method");
if (userSpecifiedMethod == NIL(char)) {
methodType = Amc_Block_c;
}
else {
if (strcmp(userSpecifiedMethod, "block") == 0) {
methodType = Amc_Block_c;
}
else if (strcmp(userSpecifiedMethod, "variable") == 0) {
methodType = Amc_Variable_c;
}
else {
(void) fprintf(vis_stderr, "** amc error: Unrecognized amc_method %s: using Block method.\n",
userSpecifiedMethod);
methodType = Amc_Block_c;
}
}
}
amcInfo->methodType = methodType;
/*
* Every subsystem shares identical initial states.
* We do not abstract the state space. Only the transition relation is over or
* under approximated.
*/
{
mdd_t *sampleInitialStates;
Amc_SubsystemInfo_t *sampleSystem;
/*
* Fsm routines always returns duplicate copy.
*/
sampleSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, 0);
sampleInitialStates = Fsm_FsmComputeInitialStates(sampleSystem->fsm);
amcInfo->initialStates = sampleInitialStates;
}
/*
* Fill in the rest of amcInfo according to methodType.
*/
switch(methodType) {
case Amc_Block_c:
amcInfo->methodData = NIL(void);
amcInfo->amcBoundProc = AmcBlockTearingProc;
amcInfo->amcFreeProc = AmcFreeBlock;
break;
/*
;;The variable tearing method has not been implemented yet;;
case Amc_Variable_c:
amcInfo->methodData = AmcInfoInitializeVariable(amcInfo);
amcInfo->amcUpperBoundProc = AmcUpperBoundProcVariable;
amcInfo->amcLowerBoundProc = AmcLowerBoundProcVariable;
amcInfo->amcFreeProc = AmcFreeVariable;
break;
*/
default:
fail("Invalid methodtype when initalizing amc method");
}
amcInfo->currentLevel = 0;
return(amcInfo);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Amc_AmcReadInitialStates | ( | Amc_Info_t * | system | ) |
| void* Amc_AmcReadMethodData | ( | Amc_Info_t * | system | ) |
| Amc_SubsystemInfo_t* Amc_AmcReadOptimalSystem | ( | Amc_Info_t * | system | ) |
| void Amc_AmcSetInitialStates | ( | Amc_Info_t * | system, |
| mdd_t * | data | ||
| ) |
| void Amc_AmcSetMethodData | ( | Amc_Info_t * | system, |
| void * | data | ||
| ) |
| void Amc_AmcSetOptimalSystem | ( | Amc_Info_t * | system, |
| Amc_SubsystemInfo_t * | data | ||
| ) |
| Amc_SubsystemInfo_t* Amc_AmcSubsystemAllocate | ( | void | ) |
Function********************************************************************
Synopsis [Allocate and initialize a Amc_SubsystemInfo_t]
SideEffects []
SeeAlso [Amc_AmcSubsystemFree]
Definition at line 958 of file amcAmc.c.
{
Amc_SubsystemInfo_t *result;
result = ALLOC(Amc_SubsystemInfo_t, 1);
return result;
} /* End of Amc_SubsystemAllocate */
| Amc_SubsystemInfo_t* Amc_AmcSubsystemCreate | ( | Fsm_Fsm_t * | fsm, |
| mdd_t * | satisfyStates, | ||
| st_table * | vertexTable, | ||
| st_table * | fanInTable, | ||
| st_table * | fanOutTable | ||
| ) |
Function********************************************************************
Synopsis [Create a subsystem.]
Description [Create and initialize a subsystem.]
SideEffects []
SeeAlso []
Definition at line 980 of file amcAmc.c.
{
Amc_SubsystemInfo_t *result;
result = ALLOC(Amc_SubsystemInfo_t, 1);
result->fsm = fsm;
result->relationArray = NIL(array_t);
result->nextStateVarSmoothen = NIL(mdd_t);
result->satisfyStates = satisfyStates;
result->vertexTable = vertexTable;
result->fanInTable = fanInTable;
result->fanOutTable = fanOutTable;
result->takenIntoOptimal = 0; /* Initialize to 0 */
result->methodSpecificData = NIL(char);
return result;
}
Here is the caller graph for this function:
| Amc_SubsystemInfo_t* Amc_AmcSubsystemDuplicate | ( | Ntk_Network_t * | network, |
| Amc_SubsystemInfo_t * | subSystem | ||
| ) |
Function********************************************************************
Synopsis [Duplicate a subsystem.]
SideEffects []
SeeAlso [Amc_AmcSubsystemAllocate]
Definition at line 1013 of file amcAmc.c.
{
Fsm_Fsm_t *fsm;
mdd_t *satisfyStates = NIL(mdd_t);
st_table *vertexTable = NIL(st_table);
st_table *fanInTable = NIL(st_table);
st_table *fanOutTable = NIL(st_table);
graph_t *partition = Part_NetworkReadPartition(network);
if(subSystem->satisfyStates != NIL(mdd_t)) {
satisfyStates = mdd_dup(subSystem->satisfyStates);
}
if(subSystem->vertexTable != NIL(st_table)) {
vertexTable = st_copy(subSystem->vertexTable);
}
if(subSystem->fanInTable != NIL(st_table)) {
fanInTable = st_copy(subSystem->fanInTable);
}
if(subSystem->fanOutTable != NIL(st_table)) {
fanOutTable = st_copy(subSystem->fanOutTable);
}
fsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition, vertexTable,
FALSE, 0);
return(Amc_AmcSubsystemCreate(fsm, satisfyStates, vertexTable, fanInTable, fanOutTable));
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Amc_AmcSubsystemFree | ( | Amc_SubsystemInfo_t * | subSystem | ) |
Function********************************************************************
Synopsis [Free a subsystem.]
Description [Frees a subsystem plus associated fields except the partition. This is to reuse the partition without recreating it.]
SideEffects []
SeeAlso [Amc_AmcSubsystemAllocate]
Definition at line 1058 of file amcAmc.c.
{
st_table *vertexTable;
st_table *fanInTable, *fanOutTable;
/* Do not free partition associated to this fsm */
if (AmcSubsystemReadFsm(subSystem) != NIL(Fsm_Fsm_t)) {
Fsm_FsmSubsystemFree(AmcSubsystemReadFsm(subSystem));
}
if (AmcSubsystemReadRelationArray(subSystem) != NIL(array_t)) {
array_t *transitionRelationArray = AmcSubsystemReadRelationArray(subSystem);
mdd_t *transitionRelation;
int i;
arrayForEachItem(mdd_t *, transitionRelationArray, i, transitionRelation) {
mdd_free(transitionRelation);
}
array_free(transitionRelationArray);
}
if (AmcSubsystemReadNextStateVarSmoothen(subSystem) != NIL(mdd_t)) {
mdd_free(AmcSubsystemReadNextStateVarSmoothen(subSystem));
}
if (AmcSubsystemReadSatisfy(subSystem) != NIL(mdd_t)) {
mdd_free(AmcSubsystemReadSatisfy(subSystem));
}
/* Do not free vertex!! */
vertexTable = AmcSubsystemReadVertexTable(subSystem);
if (vertexTable != NIL(st_table)) {
st_free_table(vertexTable);
}
fanInTable = AmcSubsystemReadFanInTable(subSystem);
if (fanInTable != NIL(st_table)) {
st_free_table(fanInTable);
}
fanOutTable = AmcSubsystemReadFanOutTable(subSystem);
if (fanOutTable != NIL(st_table)) {
st_free_table(fanOutTable);
}
FREE(subSystem);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Amc_AmcSubsystemFreeAlsoPartition | ( | Amc_SubsystemInfo_t * | subSystem | ) |
Function********************************************************************
Synopsis [Free a subsystem.]
Description [Frees a subsystem including the associated partition.]
SideEffects []
SeeAlso [Amc_AmcSubsystemAllocate]
Definition at line 1119 of file amcAmc.c.
{
st_table *vertexTable;
st_table *fanInTable, *fanOutTable;
/* Do not free partition associated to this fsm */
if (AmcSubsystemReadFsm(subSystem) != NIL(Fsm_Fsm_t)) {
Fsm_FsmFree(AmcSubsystemReadFsm(subSystem));
}
if (AmcSubsystemReadRelationArray(subSystem) != NIL(array_t)) {
array_t *transitionRelationArray = AmcSubsystemReadRelationArray(subSystem);
mdd_t *transitionRelation;
int i;
arrayForEachItem(mdd_t *, transitionRelationArray, i, transitionRelation) {
mdd_free(transitionRelation);
}
array_free(transitionRelationArray);
}
if (AmcSubsystemReadNextStateVarSmoothen(subSystem) != NIL(mdd_t)) {
mdd_free(AmcSubsystemReadNextStateVarSmoothen(subSystem));
}
if (AmcSubsystemReadSatisfy(subSystem) != NIL(mdd_t)) {
mdd_free(AmcSubsystemReadSatisfy(subSystem));
}
/* Do not free vertex!! */
vertexTable = AmcSubsystemReadVertexTable(subSystem);
if (vertexTable != NIL(st_table)) {
st_free_table(vertexTable);
}
fanInTable = AmcSubsystemReadFanInTable(subSystem);
if (fanInTable != NIL(st_table)) {
st_free_table(fanInTable);
}
fanOutTable = AmcSubsystemReadFanOutTable(subSystem);
if (fanOutTable != NIL(st_table)) {
st_free_table(fanOutTable);
}
FREE(subSystem);
}
Here is the call graph for this function:
| st_table* Amc_AmcSubsystemReadFanInTable | ( | Amc_SubsystemInfo_t * | system | ) |
Function********************************************************************
Synopsis [Read the fanInTable field of the Amc_SubsystemInfo_t]
Description [The fanInTable is the hash table of the subsystem index. The subsystem index is the pointer value uniquely distinguishing subsystems. The table contains the index of the subsystems whose component vertex is one of the transitive fan-ins of the vertex in this subsystem.]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 747 of file amcAmc.c.
{
return AmcSubsystemReadFanInTable(system);
} /* End of Amc_AmcSubsystemReadFanInTable */
| st_table* Amc_AmcSubsystemReadFanOutTable | ( | Amc_SubsystemInfo_t * | system | ) |
Function********************************************************************
Synopsis [Read the fanOutTable field of the Amc_SubsystemInfo_t]
Description [The fanOutTable is the hash table of the subsystem index. The subsystem index is the pointer value uniquely distinguishing subsystems. The table contains the index of the subsystems whose component vertex is one of the transitive fan-outs of the vertex in this subsystem.]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 785 of file amcAmc.c.
{
return AmcSubsystemReadFanOutTable(system);
} /* End of Amc_AmcSubsystemReadFanOutTable */
| Fsm_Fsm_t* Amc_AmcSubsystemReadFsm | ( | Amc_SubsystemInfo_t * | system | ) |
Function********************************************************************
Synopsis [Read the fsm field of a Amc_SubsystemInfo]
SideEffects []
SeeAlso [Amc_SubsystemInfo]
Definition at line 559 of file amcAmc.c.
{
return AmcSubsystemReadFsm(system);
} /* End of Amc_AmcSubsystemReadFsm */
Here is the caller graph for this function:
| char* Amc_AmcSubsystemReadMethodSpecificData | ( | Amc_SubsystemInfo_t * | system | ) |
Function********************************************************************
Synopsis [Read the MethodSpecific field of Amc_SubsystemInfo_t]
Description [The method specific field may hold any value(s) that are specific to the various methods.]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 822 of file amcAmc.c.
{
return AmcSubsystemReadMethodSpecificData(system);
} /* End of Amc_AmcSubsystemReadMethodSpecificData */
| mdd_t* Amc_AmcSubsystemReadNextStateVarSmoothen | ( | Amc_SubsystemInfo_t * | system | ) |
Function********************************************************************
Synopsis [Read the nextStateVarSmoothen field of the Amc_SubsystemInfo]
Description [nextStateVarSmoothen field contains the MDD of the transition relation with the next state variable existentially quantified.]
SideEffects []
SeeAlso [Amc_SubsystemInfo]
Definition at line 633 of file amcAmc.c.
{
return AmcSubsystemReadNextStateVarSmoothen(system);
} /* End of Amc_AmcSubsystemReadNextStateVarSmooth */
| array_t* Amc_AmcSubsystemReadRelationArray | ( | Amc_SubsystemInfo_t * | system | ) |
Function********************************************************************
Synopsis [Read the transition relation field of the Amc_SubsystemInfo]
SideEffects []
SeeAlso [Amc_SubsystemInfo]
Definition at line 594 of file amcAmc.c.
{
return AmcSubsystemReadRelationArray(system);
} /* End of Amc_AmcSubsystemReadTransitionRelation */
Here is the caller graph for this function:
| mdd_t* Amc_AmcSubsystemReadSatisfy | ( | Amc_SubsystemInfo_t * | system | ) |
Function********************************************************************
Synopsis [Read the satisfyStates field of the Amc_SubsystemInfo_t]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 667 of file amcAmc.c.
{
return AmcSubsystemReadSatisfy(system);
} /* End of Amc_AmcSubsystemReadSatisfy */
| st_table* Amc_AmcSubsystemReadVertexTable | ( | Amc_SubsystemInfo_t * | system | ) |
Function********************************************************************
Synopsis [Read the vertexTable field of the Amc_SubsystemInfo_t]
Description [The vertexTable field of the subsystem is the hash table of vertex names. Only the vertices contained in the subsystem is stored in this table.]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 709 of file amcAmc.c.
{
return AmcSubsystemReadVertexTable(system);
} /* End of Amc_AmcSubsystemReadVertexTable */
| void Amc_AmcSubsystemSetFanInTable | ( | Amc_SubsystemInfo_t * | system, |
| st_table * | data | ||
| ) |
Function********************************************************************
Synopsis [Set the fanInTable field of Amc_SubsystemInfo_t ]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 763 of file amcAmc.c.
{
AmcSubsystemSetFanInTable(system, data);
} /* End of Amc_AmcSubsystemSetFanInTable */
| void Amc_AmcSubsystemSetFanOutTable | ( | Amc_SubsystemInfo_t * | system, |
| st_table * | data | ||
| ) |
Function********************************************************************
Synopsis [Set the fanOutTable field of Amc_SubsystemInfo_t ]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 801 of file amcAmc.c.
{
AmcSubsystemSetFanOutTable(system, data);
} /* End of Amc_AmcSubsystemSetFanOutTable */
| void Amc_AmcSubsystemSetFsm | ( | Amc_SubsystemInfo_t * | system, |
| Fsm_Fsm_t * | info | ||
| ) |
| void Amc_AmcSubsystemSetMethodSpecificData | ( | Amc_SubsystemInfo_t * | system, |
| char * | data | ||
| ) |
Function********************************************************************
Synopsis [Set the MethodSpecific field of Amc_SubsystemInfo_t]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 838 of file amcAmc.c.
{
AmcSubsystemSetMethodSpecificData(system, data);
} /* End of Amc_AmcSubsystemSetMethodSpecificData */
| void Amc_AmcSubsystemSetNextStateVarSmoothen | ( | Amc_SubsystemInfo_t * | system, |
| mdd_t * | info | ||
| ) |
Function********************************************************************
Synopsis [Set the nextStateVarSmoothen field of the Amc_SubsystemInfo]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 650 of file amcAmc.c.
{
AmcSubsystemSetNextStateVarSmoothen(system, info);
} /* End of Amc_AmcSubsystemSetNextStateVarSmooth */
| void Amc_AmcSubsystemSetRelationArray | ( | Amc_SubsystemInfo_t * | system, |
| array_t * | info | ||
| ) |
Function********************************************************************
Synopsis [Set the transition relation field of the Amc_SubsystemInfo]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 611 of file amcAmc.c.
{
AmcSubsystemSetRelationArray(system, info);
} /* End of Amc_AmcSubsystemSetTransitionRelation */
Here is the caller graph for this function:
| void Amc_AmcSubsystemSetSatisfy | ( | Amc_SubsystemInfo_t * | system, |
| mdd_t * | data | ||
| ) |
Function********************************************************************
Synopsis [Set the satisfyStates field of Amc_SubsystemInfo_t ]
Description [satisfyStates field contains the MDD representation of the super(sub)set of states satisfying given formula. The super(sub)set of states satisfying given formula is obtained by utilizing the information of the subsystem.]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 688 of file amcAmc.c.
{
AmcSubsystemSetSatisfy(system, data);
} /* End of Amc_AmcSubsystemSetSatisfy */
| void Amc_AmcSubsystemSetVertexTable | ( | Amc_SubsystemInfo_t * | system, |
| st_table * | data | ||
| ) |
Function********************************************************************
Synopsis [Set the vertexTable field of Amc_SubsystemInfo_t ]
SideEffects []
SeeAlso [Amc_SubsystemInfo_t]
Definition at line 725 of file amcAmc.c.
{
AmcSubsystemSetVertexTable(system, data);
} /* End of Amc_AmcSubsystemSetVertexTable */
| Amc_SubsystemInfo_t* Amc_CombineSubsystems | ( | Ntk_Network_t * | network, |
| Amc_SubsystemInfo_t * | subSystem1, | ||
| Amc_SubsystemInfo_t * | subSystem2 | ||
| ) |
Function********************************************************************
Synopsis [Combine two subsystems and return the resulting subsystem.]
Description [Take the synchronous product of two subsystems. The routine returns resulting subsystem. If either one of the subsystem is NIL return the other. It is an error to pass two NIL pointers. Either one has to be a subsystem.]
SideEffects []
SeeAlso []
Definition at line 1187 of file amcAmc.c.
{
Amc_SubsystemInfo_t *subSystemInfo;
Amc_SubsystemInfo_t *subSystem;
st_table *vertexTable, *vertexTable1, *vertexTable2;
st_table *fanInTable = NIL(st_table);
st_table *fanOutTable = NIL(st_table);
st_table *fanInTable1, *fanInTable2;
st_table *fanOutTable1, *fanOutTable2;
Ntk_Node_t *latch;
graph_t *partition = Part_NetworkReadPartition(network);
Fsm_Fsm_t *fsm;
lsGen gen;
st_generator *stGen;
/* If two subsystem are identical return error */
if(subSystem1 == subSystem2) {
error_append("** amc error: illegal subsystem combination");
return NIL(Amc_SubsystemInfo_t);
}
/* If two subsystem are NIL return error */
if( (subSystem1 == NIL(Amc_SubsystemInfo_t)) &&
(subSystem2 == NIL(Amc_SubsystemInfo_t)) ) {
error_append("** amc error: illegal subsystem combination");
return NIL(Amc_SubsystemInfo_t);
}
/* If either of two subsystem is NIL return copy of the other */
if(subSystem1 == NIL(Amc_SubsystemInfo_t)) {
return Amc_AmcSubsystemDuplicate(network, subSystem2);
}
if(subSystem2 == NIL(Amc_SubsystemInfo_t)) {
return Amc_AmcSubsystemDuplicate(network, subSystem1);
}
vertexTable = st_init_table(strcmp, st_strhash);
vertexTable1 = AmcSubsystemReadVertexTable(subSystem1);
vertexTable2 = AmcSubsystemReadVertexTable(subSystem2);
Ntk_NetworkForEachLatch(network, gen, latch) {
char *latchName = Ntk_NodeReadName(latch);
if( st_lookup(vertexTable1, latchName, (char **)0) ||
st_lookup(vertexTable2, latchName, (char **)0) ) {
st_insert(vertexTable, latchName, (char *)0);
}
} /* end of Ntk_NetworkForEachLatch */
fanInTable1 = AmcSubsystemReadFanInTable(subSystem1);
fanInTable2 = AmcSubsystemReadFanInTable(subSystem2);
if( (fanInTable1 != NIL(st_table)) && (fanInTable2 != NIL(st_table)) ) {
fanInTable = st_init_table(st_ptrcmp, st_ptrhash);
st_foreach_item(fanInTable1, stGen, &subSystem, NIL(char *)) {
st_insert(fanInTable, (char *)subSystem, (char *)0);
}
st_foreach_item(fanInTable2, stGen, &subSystem, NIL(char *)) {
st_insert(fanInTable, (char *)subSystem, (char *)0);
}
}
fanOutTable1 = AmcSubsystemReadFanOutTable(subSystem1);
fanOutTable2 = AmcSubsystemReadFanOutTable(subSystem2);
if( (fanOutTable1 != NIL(st_table)) && (fanOutTable2 != NIL(st_table)) ) {
fanOutTable = st_init_table(st_ptrcmp, st_ptrhash);
st_foreach_item(fanInTable1, stGen, &subSystem, NIL(char *)) {
st_insert(fanOutTable, subSystem, (char *)0);
}
st_foreach_item(fanInTable2, stGen, &subSystem, NIL(char *)) {
st_insert(fanOutTable, subSystem, (char *)0);
}
}
fsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition, vertexTable,
FALSE, 0);
subSystemInfo = Amc_AmcSubsystemCreate(fsm, NIL(mdd_t), vertexTable,
fanInTable, fanOutTable);
/* Does not free tables */
return(subSystemInfo);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* AmcCreateSubsystemArray | ( | Ntk_Network_t * | network, |
| Ctlp_Formula_t * | formula | ||
| ) |
Function********************************************************************
Synopsis [Create an array of subsystems.]
Description [Based on the array of set of vertices, create an array of subsystems. Depending on the grouping method, different function call is made to obtain an array of structure typed Part_SubsystemInfo_t. From this information, the vertex table, fan-in table, and the fan-out table is obtained to create an array of subFSMs and the subsystems. ]
SideEffects []
SeeAlso [Part_SubsystemInfo_t]
Definition at line 2073 of file amcAmc.c.
{
array_t *partitionArray, *subSystemArray;
Part_Subsystem_t *partitionSubsystem;
Part_SubsystemInfo_t *subsystemInfo;
st_table *vertexTable;
array_t *fanInIndexArray, *fanOutIndexArray;
st_table *fanInSystemTable, *fanOutSystemTable;
Amc_SubsystemInfo_t *subSystem;
graph_t *partition = Part_NetworkReadPartition(network);
int i, j;
int fanInIndex, fanOutIndex, numOfVertex;
Amc_SubsystemInfo_t *fanInSubsystem, *fanOutSubsystem;
char *flagValue, *numberOfVertexInGroup;
array_t *ctlArray;
/* Obtain the size of the subsystem */
numberOfVertexInGroup = Cmd_FlagReadByName("amc_sizeof_group");
if(numberOfVertexInGroup != NIL(char)){
numOfVertex = atoi(numberOfVertexInGroup);
}
else{
/* default value */
numOfVertex = 8;
}
/*
* Obtain subsystem partitioned as submachines.
*/
flagValue = Cmd_FlagReadByName("amc_grouping_method");
if( (flagValue != NIL(char)) &&
(strcmp(flagValue, "latch_dependency")) == 0){
subsystemInfo = Part_PartitionSubsystemInfoInit(network);
Part_PartitionSubsystemInfoSetBound(subsystemInfo, numOfVertex);
partitionArray = Part_PartCreateSubsystems(subsystemInfo, NIL(array_t),
NIL(array_t));
Part_PartitionSubsystemInfoFree(subsystemInfo);
}
else{
/*
* Latches which have dependency relation with given formulae
* are computed and grouped into sub-systems.
*/
lsGen gen;
Ntk_Node_t *node;
char *name;
array_t *arrayOfDataInputName;
lsList latchInputList = lsCreate();
if (latchInputList == (lsList)0){
return NIL(array_t);
}
ctlArray = array_alloc(Ctlp_Formula_t *, 1);
array_insert(Ctlp_Formula_t *, ctlArray, 0, formula);
if (!Part_PartitionGetLatchInputListFromCTL(network, ctlArray,
NIL(array_t),
latchInputList)) {
array_free(ctlArray);
return NIL(array_t);
}
arrayOfDataInputName = array_alloc(Ntk_Node_t *, lsLength(latchInputList));
lsForEachItem(latchInputList, gen, node){
name = Ntk_NodeReadName(node);
array_insert_last(char *, arrayOfDataInputName, name);
}
lsDestroy(latchInputList, (void (*)(lsGeneric))0);
array_sort(arrayOfDataInputName, stringCompare);
partitionArray = Part_PartGroupVeriticesBasedOnHierarchy(network,
arrayOfDataInputName);
array_free(arrayOfDataInputName);
array_free(ctlArray);
}
subSystemArray = array_alloc(Amc_SubsystemInfo_t *, array_n(partitionArray));
/*
* For each partitioned submachines build an FSM.
*/
arrayForEachItem(Part_Subsystem_t *, partitionArray, i, partitionSubsystem) {
Fsm_Fsm_t *fsm;
vertexTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
fanInIndexArray = Part_PartitionSubsystemReadFanIn(partitionSubsystem);
fanOutIndexArray = Part_PartitionSubsystemReadFanOut(partitionSubsystem);
FREE(partitionSubsystem);
fsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition, vertexTable,
FALSE, 0);
subSystem = Amc_AmcSubsystemCreate(fsm, NIL(mdd_t), vertexTable,
/* NIL(st_table), NIL(st_table) ); */
(st_table *)fanInIndexArray,
(st_table *)fanOutIndexArray);
array_insert_last(Amc_SubsystemInfo_t *, subSystemArray, subSystem);
} /* end of arrayForEachItem(partitionArray) */
array_free(partitionArray);
/*
* Convert fanInIndexTable to fanInSystemTable
* Convert fanOutIndexTable to fanOutSystemTable
*/
arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
fanInIndexArray = (array_t *) AmcSubsystemReadFanInTable(subSystem);
fanInSystemTable = st_init_table(st_ptrcmp, st_ptrhash);
if( fanInIndexArray != NIL(array_t) ) {
arrayForEachItem(int, fanInIndexArray, j, fanInIndex) {
fanInSubsystem = array_fetch(Amc_SubsystemInfo_t *, subSystemArray,
fanInIndex);
st_insert(fanInSystemTable, (char *)fanInSubsystem, NIL(char));
}
array_free(fanInIndexArray);
}
AmcSubsystemSetFanInTable(subSystem, fanInSystemTable);
fanOutIndexArray = (array_t *) AmcSubsystemReadFanOutTable(subSystem);
fanOutSystemTable = st_init_table(st_ptrcmp, st_ptrhash);
if( fanOutIndexArray != NIL(array_t) ) {
arrayForEachItem(int, fanOutIndexArray, j, fanOutIndex) {
fanOutSubsystem = array_fetch(Amc_SubsystemInfo_t *, subSystemArray,
fanOutIndex);
st_insert(fanOutSystemTable, (char *)fanOutSubsystem, NIL(char));
}
array_free(fanOutIndexArray);
}
AmcSubsystemSetFanOutTable(subSystem, fanOutSystemTable);
}
return subSystemArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* AmcModelCheckAtomicFormula | ( | Fsm_Fsm_t * | modelFsm, |
| Ctlp_Formula_t * | ctlFormula | ||
| ) |
Function********************************************************************
Synopsis [Find Mdd for states satisfying Atomic Formula.]
Description [This is a duplicate copy of static function, ModelCheckAtomicFormula(). ]
SideEffects []
Definition at line 2411 of file amcAmc.c.
{
mdd_t * resultMdd;
mdd_t *tmpMdd;
Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm );
char *nodeNameString = Ctlp_FormulaReadVariableName( ctlFormula );
char *nodeValueString = Ctlp_FormulaReadValueName( ctlFormula );
Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
Var_Variable_t *nodeVar;
int nodeValue;
graph_t *modelPartition;
vertex_t *partitionVertex;
Mvf_Function_t *MVF;
nodeVar = Ntk_NodeReadVariable( node );
if ( Var_VariableTestIsSymbolic( nodeVar ) ){
nodeValue = Var_VariableReadIndexFromSymbolicValue( nodeVar, nodeValueString );
}
else {
nodeValue = atoi( nodeValueString );
}
modelPartition = Part_NetworkReadPartition( network );
if ( !( partitionVertex = Part_PartitionFindVertexByName( modelPartition,
nodeNameString ) )) {
lsGen tmpGen;
Ntk_Node_t *tmpNode;
array_t *mvfArray;
array_t *tmpRoots = array_alloc( Ntk_Node_t *, 0 );
st_table *tmpLeaves = st_init_table( st_ptrcmp, st_ptrhash );
array_insert_last( Ntk_Node_t *, tmpRoots, node );
Ntk_NetworkForEachCombInput( network, tmpGen, tmpNode ) {
st_insert( tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED );
}
mvfArray = Ntm_NetworkBuildMvfs( network, tmpRoots, tmpLeaves,
NIL(mdd_t) );
MVF = array_fetch( Mvf_Function_t *, mvfArray, 0 );
array_free( tmpRoots );
st_free_table( tmpLeaves );
array_free( mvfArray );
tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue );
resultMdd = mdd_dup( tmpMdd );
Mvf_FunctionFree( MVF );
return resultMdd;
}
else {
MVF = Part_VertexReadFunction( partitionVertex );
tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue );
resultMdd = mdd_dup( tmpMdd );
return resultMdd;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void AmcPrintOptimalSystem | ( | FILE * | fp, |
| Amc_Info_t * | amcInfo | ||
| ) |
Function********************************************************************
Synopsis [Print subsystem(s) taken into the optimal system.]
SideEffects [From the array of subsystems, prints the subsystems that has been added(combined) to form a optimal system.]
SeeAlso []
Definition at line 2237 of file amcAmc.c.
{
int i;
Amc_SubsystemInfo_t *subSystem;
fprintf(fp, "\nSubsystems in optimal path : ");
arrayForEachItem(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, i, subSystem) {
if(subSystem->takenIntoOptimal)
fprintf(fp, " %d ", i);
}
}
Here is the caller graph for this function:
| static int stringCompare | ( | const void * | s1, |
| const void * | s2 | ||
| ) | [static] |
Variable Documentation
char rcsid [] UNUSED = "$Id: amcAmc.c,v 1.57 2005/04/16 04:22:41 fabio Exp $" [static] |
CFile***********************************************************************
FileName [amcAmc.c]
PackageName [amc]
Synopsis [Approximate Model Checker.]
Author [Woohyuk Lee <woohyuk@duke.colorado.edu>]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
