#include "mcInt.h"#include "mdd.h"#include "cmd.h"#include "fsm.h"#include "img.h"#include "sat.h"#include "baig.h"#include <errno.h>
Include dependency graph for mcUtil.c:
Go to the source code of this file.
Functions | |
| static void | PrintNodes (array_t *mddIdArray, Ntk_Network_t *network) |
| static array_t * | SortMddIds (array_t *mddIdArray, Ntk_Network_t *network) |
| static void | PrintDeck (array_t *mddValues, array_t *mddIdArray, Ntk_Network_t *network) |
| static int | cmp (const void *s1, const void *s2) |
| static boolean | AtomicFormulaCheckSemantics (Ctlp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed) |
| static void | NodeTableAddCtlFormulaNodes (Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table *nodesTable) |
| static void | NodeTableAddLtlFormulaNodes (Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *nodesTable) |
| static boolean | MintermCheckWellFormed (mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr) |
| static boolean | SetCheckSupport (mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr) |
| static mdd_t * | Mc_ComputeRangeOfPseudoInputs (Ntk_Network_t *network) |
| static array_t * | Mc_BuildBackwardRingsWithInvariants (mdd_t *S, mdd_t *T, mdd_t *invariants, Fsm_Fsm_t *fsm) |
| int | Mc_FsmComputeStatesReachingToSet (Fsm_Fsm_t *modelFsm, mdd_t *targetStates, array_t *careStatesArray, mdd_t *specialStates, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| int | Mc_FsmComputeStatesReachableFromSet (Fsm_Fsm_t *modelFsm, mdd_t *initialStates, array_t *careStatesArray, mdd_t *specialStates, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| boolean | Mc_FormulaStaticSemanticCheckOnNetwork (Ctlp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed) |
| array_t * | Mc_BuildPathToCore (mdd_t *aState, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType) |
| array_t * | Mc_BuildForwardRings (mdd_t *S, Fsm_Fsm_t *fsm, array_t *onionRings) |
| array_t * | Mc_BuildForwardRingsWithInvariants (mdd_t *S, mdd_t *T, mdd_t *invariants, Fsm_Fsm_t *fsm) |
| array_t * | Mc_BuildPathFromCore (mdd_t *aStates, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType) |
| array_t * | Mc_BuildPathToCoreFAFW (mdd_t *aStates, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType) |
| array_t * | Mc_BuildPathFromCoreFAFWGeneral (mdd_t *T, array_t *rings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType) |
| array_t * | MC_BuildCounterExampleFAFWGeneral (Fsm_Fsm_t *modelFsm, mdd_t *I, mdd_t *T, mdd_t *H, array_t *L) |
| array_t * | Mc_BuildFAFWLayer (Fsm_Fsm_t *modelFsm, mdd_t *T, mdd_t *H) |
| array_t * | Mc_BuildPathFromCoreFAFW (mdd_t *Ts, array_t *rings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType) |
| array_t * | Mc_BuildShortestPathFAFW (mdd_t *win, mdd_t *S, mdd_t *T, array_t *rings, mdd_manager *mgr, Fsm_Fsm_t *fsm, int prevFlag) |
| array_t * | Mc_CompletePath (mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, Mc_FwdBwdAnalysis dirn) |
| mdd_t * | Mc_ComputeAMinterm (mdd_t *aSet, array_t *Support, mdd_manager *mddMgr) |
| mdd_t * | Mc_ComputeACloseMinterm (mdd_t *aSet, mdd_t *target, array_t *Support, mdd_manager *mddMgr) |
| char * | Mc_MintermToStringAiger (mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork) |
| char * | Mc_MintermToStringAigerInput (mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork) |
| char * | Mc_MintermToString (mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork) |
| int | Mc_PrintPath (array_t *aPath, Fsm_Fsm_t *modelFsm, boolean printInput) |
| int | Mc_PrintPathAiger (array_t *aPath, Fsm_Fsm_t *modelFsm, boolean printInput) |
| static Mvf_Function_t * | NodeBuildPseudoInputMvf (Ntk_Node_t *node, mdd_manager *mddMgr) |
| mdd_t * | Mc_FsmComputeDrivingInputMinterms (Fsm_Fsm_t *fsm, mdd_t *aState, mdd_t *bState) |
| mdd_t * | Mc_ComputeAState (mdd_t *states, Fsm_Fsm_t *modelFsm) |
| mdd_t * | Mc_ComputeACloseState (mdd_t *states, mdd_t *target, Fsm_Fsm_t *modelFsm) |
| void | Mc_MintermPrint (mdd_t *aMinterm, array_t *support, Ntk_Network_t *aNetwork) |
| void | Mc_NodeTableAddCtlFormulaNodes (Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table *nodesTable) |
| void | Mc_NodeTableAddLtlFormulaNodes (Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *nodesTable) |
| Fsm_Fsm_t * | Mc_ConstructReducedFsm (Ntk_Network_t *network, array_t *ctlFormulaArray) |
| Mc_GSHScheduleType | Mc_StringConvertToScheduleType (char *string) |
| int | Mc_StringConvertToLockstepMode (char *string) |
| Mc_EarlyTermination_t * | Mc_EarlyTerminationAlloc (Mc_EarlyTerminationType mode, mdd_t *states) |
| void | Mc_EarlyTerminationFree (Mc_EarlyTermination_t *earlyTermination) |
| boolean | Mc_EarlyTerminationIsSkip (Mc_EarlyTermination_t *earlyTermination) |
| array_t * | McCompletePathFwd (mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| array_t * | McCompletePathBwd (mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) |
| int | McCommandInitState (Hrc_Manager_t **hmgr, int argc, char **argv) |
| char * | McStatePrintAsFormula (mdd_t *aMinterm, array_t *aSupport, Fsm_Fsm_t *modelFsm) |
| int | McComputeOnionRingsWithClosestCore (mdd_t *aState, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm) |
| array_t * | McRemoveIndexedOnionRings (int index, array_t *arrayOfOnionRings) |
| array_t * | McConvertMintermToValueArray (mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr) |
| void | McPrintTransitionAiger (mdd_t *aState, mdd_t *bState, mdd_t *uInput, mdd_t *vInput, array_t *stateSupport, array_t *inputSupport, boolean printInputs, Fsm_Fsm_t *modelFsm, int seqNumber) |
| void | McPrintTransition (mdd_t *aState, mdd_t *bState, mdd_t *uInput, mdd_t *vInput, array_t *stateSupport, array_t *inputSupport, boolean printInputs, Fsm_Fsm_t *modelFsm, int seqNumber) |
| void | McStatePassesFormula (mdd_t *aState, Ctlp_Formula_t *formula, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm) |
| void | McStateFailsFormula (mdd_t *aState, Ctlp_Formula_t *formula, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm) |
| void | McStatePassesOrFailsFormula (mdd_t *aState, Ctlp_Formula_t *formula, int pass, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm) |
| McPath_t * | McPathNormalize (McPath_t *aPath) |
| array_t * | McCreateMergedPath (array_t *aPath, array_t *bPath) |
| array_t * | McMddArrayDuplicateFAFW (array_t *mddArray) |
| mdd_t * | McMddArrayAnd (array_t *mddArray) |
| mdd_t * | McMddArrayOr (array_t *mddArray) |
| array_t * | McCreateJoinedPath (array_t *aPath, array_t *bPath) |
| boolean | McStateSatisfiesFormula (Ctlp_Formula_t *aFormula, mdd_t *aState) |
| boolean | McStateTestMembership (mdd_t *aState, mdd_t *setOfStates) |
| mdd_t * | McGetSuccessorInTarget (mdd_t *aState, mdd_t *targetStates, Fsm_Fsm_t *modelFsm) |
| mdd_t * | McGetSuccessorInTargetAmongFairStates (mdd_t *aState, mdd_t *targetStates, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm) |
| array_t * | McPathReadStemArray (McPath_t *aPath) |
| array_t * | McPathReadCycleArray (McPath_t *aPath) |
| void | McPathSetStemArray (McPath_t *aPath, array_t *stemArray) |
| void | McPathSetCycleArray (McPath_t *aPath, array_t *cycleArray) |
| McPath_t * | McPathAlloc (void) |
| void | McNormalizeBddPointer (array_t *bddArray) |
| void | McPathFree (McPath_t *aPath) |
| McOptions_t * | McOptionsAlloc (void) |
| void | McOptionsFree (McOptions_t *options) |
| McDbgLevel | McOptionsReadDbgLevel (McOptions_t *options) |
| FILE * | McOptionsReadGuideFile (McOptions_t *options) |
| FILE * | McOptionsReadSystemFile (McOptions_t *options) |
| int | McOptionsReadTimeOutPeriod (McOptions_t *options) |
| Mc_VerbosityLevel | McOptionsReadVerbosityLevel (McOptions_t *options) |
| Mc_LeMethod_t | McOptionsReadLeMethod (McOptions_t *options) |
| Mc_DcLevel | McOptionsReadDcLevel (McOptions_t *options) |
| FILE * | McOptionsReadCtlFile (McOptions_t *options) |
| FILE * | McOptionsReadDebugFile (McOptions_t *options) |
| int | McOptionsReadSimValue (McOptions_t *options) |
| int | McOptionsReadUseMore (McOptions_t *options) |
| boolean | McOptionsReadVacuityDetect (McOptions_t *options) |
| int | McOptionsReadBeerMethod (McOptions_t *options) |
| int | McOptionsReadReduceFsm (McOptions_t *options) |
| int | McOptionsReadPrintInputs (McOptions_t *options) |
| boolean | McOptionsReadUseFormulaTree (McOptions_t *options) |
| Mc_GSHScheduleType | McOptionsReadSchedule (McOptions_t *options) |
| int | McOptionsReadLockstep (McOptions_t *options) |
| Fsm_RchType_t | McOptionsReadInvarApproxFlag (McOptions_t *options) |
| boolean | McOptionsReadInvarOnionRingsFlag (McOptions_t *options) |
| Mc_FwdBwdAnalysis | McOptionsReadFwdBwd (McOptions_t *options) |
| Mc_FwdBwdAnalysis | McOptionsReadTraversalDirection (McOptions_t *options) |
| Fsm_ArdcOptions_t * | McOptionsReadArdcOptions (McOptions_t *options) |
| int | McOptionsReadCoverageHoskote (McOptions_t *options) |
| int | McOptionsReadCoverageImproved (McOptions_t *options) |
| void | McOptionsSetFwdBwd (McOptions_t *options, Mc_FwdBwdAnalysis fwdBwd) |
| void | McOptionsSetGuideFile (McOptions_t *options, FILE *guideFile) |
| void | McOptionsSetVariablesForSystem (McOptions_t *options, FILE *systemFile) |
| void | McOptionsSetTraversalDirection (McOptions_t *options, Mc_FwdBwdAnalysis fwdBwd) |
| void | McOptionsSetUseMore (McOptions_t *options, boolean useMore) |
| void | McOptionsSetReduceFsm (McOptions_t *options, boolean reduceFsm) |
| void | McOptionsSetVacuityDetect (McOptions_t *options, boolean vd) |
| void | McOptionsSetBeerMethod (McOptions_t *options, boolean beer) |
| void | McOptionsSetFAFWFlag (McOptions_t *options, boolean FAFWFlag) |
| void | McOptionsSetPrintInputs (McOptions_t *options, boolean printInputs) |
| void | McOptionsSetUseFormulaTree (McOptions_t *options, boolean useFormulaTree) |
| void | McOptionsSetSchedule (McOptions_t *options, Mc_GSHScheduleType schedule) |
| void | McOptionsSetLockstep (McOptions_t *options, int lockstep) |
| void | McOptionsSetSimValue (McOptions_t *options, boolean simValue) |
| void | McOptionsSetDbgLevel (McOptions_t *options, McDbgLevel dbgLevel) |
| void | McOptionsSetVerbosityLevel (McOptions_t *options, Mc_VerbosityLevel verbosityLevel) |
| void | McOptionsSetLeMethod (McOptions_t *options, Mc_LeMethod_t leMethod) |
| void | McOptionsSetDcLevel (McOptions_t *options, Mc_DcLevel dcLevel) |
| void | McOptionsSetArdcOptions (McOptions_t *options, Fsm_ArdcOptions_t *ardcOptions) |
| void | McOptionsSetInvarOnionRingsFlag (McOptions_t *options, int shellFlag) |
| void | McOptionsSetCtlFile (McOptions_t *options, FILE *file) |
| void | McOptionsSetDebugFile (McOptions_t *options, FILE *file) |
| void | McOptionsSetTimeOutPeriod (McOptions_t *options, int timeOutPeriod) |
| void | McOptionsSetInvarApproxFlag (McOptions_t *options, Fsm_RchType_t approxFlag) |
| void | McOptionsSetCoverageHoskote (McOptions_t *options, boolean doCoverageHoskote) |
| void | McOptionsSetCoverageImproved (McOptions_t *options, boolean doCoverageImproved) |
| boolean | McQueryContinue (char *query) |
| void | McPrintSupport (mdd_t *aMdd, mdd_manager *mddMgr, Ntk_Network_t *aNetwork) |
| int | McPrintSimPath (FILE *outputFile, array_t *aPath, Fsm_Fsm_t *modelFsm) |
| Fsm_Fsm_t * | McConstructReducedFsm (Ntk_Network_t *network, array_t *ctlFormulaArray) |
| Mc_EarlyTermination_t * | McObtainUpdatedEarlyTerminationCondition (Mc_EarlyTermination_t *earlyTermination, mdd_t *careStates, Ctlp_FormulaType formulaType) |
| boolean | McCheckEarlyTerminationForUnderapprox (Mc_EarlyTermination_t *earlyTermination, mdd_t *underApprox, array_t *careStatesArray) |
| boolean | McCheckEarlyTerminationForOverapprox (Mc_EarlyTermination_t *earlyTermination, mdd_t *overApprox, array_t *careStatesArray) |
| array_t * | Mc_ReadHints (FILE *guideFP) |
| st_table * | Mc_ReadSystemVariablesFAFW (Fsm_Fsm_t *fsm, FILE *systemFP) |
| st_table * | Mc_SetAllInputToSystem (Fsm_Fsm_t *fsm) |
| array_t * | Mc_EvaluateHints (Fsm_Fsm_t *fsm, Ctlp_FormulaArray_t *invarArray) |
| array_t * | Mc_ComputeGuideArray (Fsm_Fsm_t *fsm, FILE *guideFP) |
| Mc_GuidedSearch_t | Mc_ReadGuidedSearchType (void) |
| void | Mc_CheckPathToCore (Fsm_Fsm_t *fsm, array_t *pathToCore) |
| void | Mc_CheckPathFromCore (Fsm_Fsm_t *fsm, array_t *pathFromCore) |
| void | Mc_PrintStates (Fsm_Fsm_t *modelFsm, mdd_t *states) |
| void | Mc_PrintNumStates (Fsm_Fsm_t *modelFsm, mdd_t *states) |
| void | Mc_PrintRings (Fsm_Fsm_t *modelFsm, array_t *onionRings) |
| void | Mc_PrintNumRings (Fsm_Fsm_t *modelFsm, array_t *onionRings) |
| mdd_t * | McComputeACloseMinterm (mdd_t *aSet, mdd_t *target, array_t *Support, mdd_manager *mddMgr) |
| mdd_t * | McComputeACloseState (mdd_t *states, mdd_t *target, Fsm_Fsm_t *modelFsm) |
| Mc_GSHScheduleType | McStringConvertToScheduleType (char *string) |
| int | McStringConvertToLockstepMode (char *string) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mcUtil.c,v 1.113 2009/04/11 18:26:10 fabio Exp $" |
Function Documentation
| static boolean AtomicFormulaCheckSemantics | ( | Ctlp_Formula_t * | formula, |
| Ntk_Network_t * | network, | ||
| boolean | inputsAllowed | ||
| ) | [static] |
Function********************************************************************
Synopsis [Perform simple static semantic checks on formula.]
SideEffects []
SeeAlso [Mc_FormulaStaticSemanticCheckOnNetwork]
Definition at line 5836 of file mcUtil.c.
{
char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
char *nodeValueString = Ctlp_FormulaReadValueName( formula );
Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
Var_Variable_t *nodeVar;
int nodeValue;
if ( !node ) {
error_append("Could not find node corresponding to the name\n\t- ");
error_append( nodeNameString );
error_append("\n(Wire for this name may have been removed by synthesis)");
return FALSE;
}
nodeVar = Ntk_NodeReadVariable( node );
if ( Var_VariableTestIsSymbolic( nodeVar ) ){
nodeValue = Var_VariableReadIndexFromSymbolicValue( nodeVar, nodeValueString );
if ( nodeValue == -1 ) {
error_append("Value specified in RHS is not in domain of variable\n");
error_append( Ctlp_FormulaReadVariableName( formula ) );
error_append("=");
error_append( Ctlp_FormulaReadValueName( formula ) );
return FALSE;
}
}
else {
int check;
check = Cmd_StringCheckIsInteger(nodeValueString, &nodeValue);
if( check==0 ) {
error_append("Value in the RHS is illegal\n");
error_append( Ctlp_FormulaReadVariableName( formula ) );
error_append("=");
error_append( Ctlp_FormulaReadValueName( formula ) );
return FALSE;
}
if( check==1 ) {
error_append("Value in the RHS is out of range of int\n");
error_append( Ctlp_FormulaReadVariableName( formula ) );
error_append("=");
error_append( Ctlp_FormulaReadValueName( formula ) );
return FALSE;
}
if ( !(Var_VariableTestIsValueInRange( nodeVar, nodeValue ) ) ) {
error_append("Value specified in RHS is not in domain of variable\n");
error_append( Ctlp_FormulaReadVariableName( formula ) );
error_append("=");
error_append( Ctlp_FormulaReadValueName( formula ) );
return FALSE;
}
}
if(!inputsAllowed){
boolean coverSupport;
lsGen tmpGen;
Ntk_Node_t *tmpNode;
st_table *supportNodes = st_init_table(st_ptrcmp, st_ptrhash);
array_t *thisNodeArray = array_alloc( Ntk_Node_t *, 0);
array_insert_last( Ntk_Node_t *, thisNodeArray, node );
Ntk_NetworkForEachNode(network, tmpGen, tmpNode) {
if (Ntk_NodeTestIsConstant(tmpNode) || Ntk_NodeTestIsLatch(tmpNode)) {
st_insert(supportNodes, (char *) tmpNode, NIL(char));
}
}
coverSupport = Ntk_NetworkTestLeavesCoverSupportOfRoots(network,
thisNodeArray,
supportNodes);
array_free(thisNodeArray);
st_free_table(supportNodes);
if ( coverSupport == FALSE ) {
char *tmpString =
util_strcat3( "\nNode ", nodeNameString,
" is not driven only by latches and constants.\n");
error_append(tmpString);
return FALSE;
}
}
return TRUE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int cmp | ( | const void * | s1, |
| const void * | s2 | ||
| ) | [static] |
| static array_t * Mc_BuildBackwardRingsWithInvariants | ( | mdd_t * | S, |
| mdd_t * | T, | ||
| mdd_t * | invariants, | ||
| Fsm_Fsm_t * | fsm | ||
| ) | [static] |
Function********************************************************************
Synopsis [Build a onion ring from target under invariants.]
Description [Build a onion ring from target under invariants. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
Definition at line 505 of file mcUtil.c.
{
mdd_t *oneMdd, *nextStates, *fairStates;
array_t *toCareSetArray, *backwardRings;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
oneMdd = mdd_one(mddMgr);
backwardRings = array_alloc(mdd_t *, 0);
toCareSetArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
fairStates = Fsm_FsmReadFairnessStates(fsm);
if(fairStates == 0) fairStates = oneMdd;
nextStates = McEvaluateEUFormulaWithGivenTR(fsm, invariants, T,
NIL(mdd_t), fairStates, toCareSetArray,
MC_NO_EARLY_TERMINATION,
backwardRings, McVerbosityNone_c,
McDcLevelNone_c, NIL(boolean));
mdd_free(nextStates);
mdd_array_free(toCareSetArray);
return(backwardRings);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* MC_BuildCounterExampleFAFWGeneral | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | I, | ||
| mdd_t * | T, | ||
| mdd_t * | H, | ||
| array_t * | L | ||
| ) |
Function********************************************************************
Synopsis [Build a counterexample path with general algorithm.]
Description [Build a counterexample path with general algorithm This is function for FateAndFreeWill counterexample generation.]
SideEffects []
Img_ImageInfoConjoinWithWinningStrategy(modelFsm, Img_Forward_c, layer);
Fsm_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c); Fsm_ImageInfoConjoinWithWinningStrategy(modelFsm, Img_Forward_c, Li);
Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c);
Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c);
Definition at line 802 of file mcUtil.c.
{
mdd_t *oneMdd, *zeroMdd;
mdd_t *T_I, *P, *Li, *Q_Li, *Q_T, *nLi;
mdd_t *ring, *ring_Q, *Q;
mdd_t *layer, *Lm, *nLayer;
mdd_t *extCube;
mdd_t *invariantStates, *nInvariantStates;
int m, q, free, i;
array_t *path, *R;
array_t *careStatesArray;
Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);
oneMdd = mdd_one(mgr);
zeroMdd = mdd_zero(mgr);
path = array_alloc(mdd_t *, 0);
T_I = mdd_and(T, I, 1, 1);
if(!mdd_equal(T_I, zeroMdd)) {
mdd_free(oneMdd);
mdd_free(zeroMdd);
P = Mc_ComputeACloseState(T_I, T, modelFsm);
mdd_free(T_I);
array_insert_last(mdd_t *, path, P);
return(path);
}
mdd_free(T_I);
extCube = Fsm_FsmReadExtQuantifyInputCube(modelFsm);
invariantStates = mdd_zero(mgr);
layer = NULL;
Lm = NULL;
for(m=0; m<array_n(L); m++) {
layer = array_fetch(mdd_t *, L, m);
nLayer = bdd_smooth_with_cube(layer, extCube);
nInvariantStates = mdd_or(invariantStates, nLayer, 1, 1);
mdd_free(nLayer);
mdd_free(invariantStates);
invariantStates = nInvariantStates;
Lm = mdd_and(I, layer, 1, 1);
if(!mdd_equal(Lm, zeroMdd)) {
break;
}
mdd_free(Lm);
}
R = Mc_BuildBackwardRingsWithInvariants(Lm, T, invariantStates, modelFsm);
imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
Img_ForwardImageInfoConjoinWithWinningStrategy(imageInfo, layer);
i = m;
Q = mdd_and(I, Lm, 1, 1);
ring_Q = NULL;
for(q=0; q<array_n(R); q++) {
ring = array_fetch(mdd_t *, R, q);
ring_Q = mdd_and(ring, Q, 1, 1);
if(!mdd_equal(ring_Q, zeroMdd)) {
break;
}
mdd_free(ring_Q);
}
mdd_free(Q);
P = Mc_ComputeACloseState(ring_Q, T, modelFsm);
mdd_free(ring_Q);
free = 0;
careStatesArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, careStatesArray, oneMdd);
while(1) {
Q = Img_ImageInfoComputeImageWithDomainVars(
imageInfo, P, P, careStatesArray);
Q_T = mdd_and(Q, P, 1, 0);
mdd_free(Q);
Q = Q_T;
if(i>0) {
Li = array_fetch(mdd_t *, L, i-1);
nLi = bdd_smooth_with_cube(Li, extCube);
Q_Li = mdd_and(Q, nLi, 1, 1);
mdd_free(nLi);
if(!mdd_equal(Q_Li, zeroMdd)) {
i--;
mdd_free(Q);
Q = Q_Li;
free = 1;
imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo);
Img_ForwardImageInfoConjoinWithWinningStrategy(imageInfo, layer);
}
}
ring_Q = NULL;
for(q=0; q<array_n(R); q++) {
ring = array_fetch(mdd_t *, R, q);
ring_Q = mdd_and(ring, Q, 1, 1);
if(!mdd_equal(ring_Q, zeroMdd)) {
break;
}
mdd_free(ring_Q);
}
mdd_free(Q);
if(q >= array_n(R)) {
imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo);
continue;
}
Q = Mc_ComputeACloseState(ring_Q, T, modelFsm);
mdd_free(ring_Q);
if(free == 0) {
array_insert_last(mdd_t *, path, (mdd_t *)((long)P+1));
}
else if(free ==1) {
array_insert_last(mdd_t *, path, P);
free = 0;
}
Q_T = mdd_and(Q, T, 1, 1);
if(!mdd_equal(Q_T, zeroMdd)) {
array_insert_last(mdd_t *, path, (mdd_t *)((long)Q+1));
mdd_free(Q_T);
break;
}
mdd_free(Q_T);
P = Q;
}
array_free(careStatesArray);
mdd_free(oneMdd);
mdd_free(zeroMdd);
imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo);
return(path);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_BuildFAFWLayer | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | T, | ||
| mdd_t * | H | ||
| ) |
Function********************************************************************
Synopsis [Build a fate and free will layer.]
Description [Build a fate and free will layer. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
Definition at line 972 of file mcUtil.c.
{
mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);
Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
mdd_t *zeroMdd, *oneMdd;
mdd_t *S, *nH, *EX_S, *extCube, *S_new;
array_t *L;
array_t *careStatesArray;
zeroMdd = mdd_zero(mgr);
oneMdd = mdd_one(mgr);
L = array_alloc(mdd_t *, 0);
extCube = Fsm_FsmReadExtQuantifyInputCube(modelFsm);
careStatesArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, careStatesArray, oneMdd);
while(!mdd_equal(H, zeroMdd)) {
Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 1);
S = Mc_FsmEvaluateAUFormula(modelFsm, H, T,
NIL(mdd_t), oneMdd, careStatesArray,
MC_NO_EARLY_TERMINATION, NIL(array_t),
Mc_None_c, 0, McVerbosityNone_c,
McDcLevelNone_c, NIL(boolean));
Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 0);
array_insert_last(mdd_t *, L, S);
S_new = bdd_smooth_with_cube(S, extCube);
mdd_free(S);
nH = mdd_and(H, S_new, 1, 0);
if(mdd_equal(H, nH)) {
mdd_free(nH);
mdd_free(S_new);
break;
}
mdd_free(H);
H = nH;
mdd_free(T);
EX_S = Img_ImageInfoComputePreImageWithDomainVars(
imageInfo, S_new, S_new, careStatesArray);
mdd_free(S_new);
T = mdd_and(EX_S, H, 1, 1);
}
array_free(careStatesArray);
mdd_free(zeroMdd);
mdd_free(oneMdd);
mdd_free(T);
mdd_free(H);
return(L);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_BuildForwardRings | ( | mdd_t * | S, |
| Fsm_Fsm_t * | fsm, | ||
| array_t * | onionRings | ||
| ) |
Function********************************************************************
Synopsis [Build a onion ring from initial state.]
Description [Build a onion ring from initial state. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
Definition at line 422 of file mcUtil.c.
{
mdd_t *nextStates;
mdd_t *states, *nStates, *oneMdd;
array_t *toCareSetArray, *forwardRings;
int i;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
states = mdd_zero(mddMgr);
oneMdd = mdd_one(mddMgr);
for(i=0; i<array_n(onionRings); i++) {
mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
nStates = mdd_or(ring, states, 1, 1);
mdd_free(states);
states = nStates;
}
forwardRings = array_alloc(mdd_t *, 0);
toCareSetArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
nextStates = Mc_FsmEvaluateESFormula(fsm, states, S,
NIL(mdd_t), oneMdd, toCareSetArray,
MC_NO_EARLY_TERMINATION, NIL(array_t),
Mc_None_c, forwardRings,
McVerbosityNone_c, McDcLevelNone_c,
NIL(boolean));
mdd_free(nextStates);
mdd_free(states);
mdd_array_free(toCareSetArray);
return(forwardRings);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_BuildForwardRingsWithInvariants | ( | mdd_t * | S, |
| mdd_t * | T, | ||
| mdd_t * | invariants, | ||
| Fsm_Fsm_t * | fsm | ||
| ) |
Function********************************************************************
Synopsis [Build a onion ring to target under invariants.]
Description [Build a onion ring to target under invariants. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
Definition at line 468 of file mcUtil.c.
{
mdd_t *oneMdd, *nextStates, *fairStates;
array_t *toCareSetArray, *forwardRings;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
oneMdd = mdd_one(mddMgr);
forwardRings = array_alloc(mdd_t *, 0);
toCareSetArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
fairStates = Fsm_FsmReadFairnessStates(fsm);
if(fairStates == 0) fairStates = oneMdd;
nextStates = McEvaluateESFormulaWithGivenTRWithTarget(fsm, invariants, S, T,
NIL(mdd_t), fairStates, toCareSetArray,
MC_NO_EARLY_TERMINATION,
forwardRings, McVerbosityNone_c,
McDcLevelNone_c, NIL(boolean));
mdd_free(nextStates);
mdd_array_free(toCareSetArray);
return(forwardRings);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_BuildPathFromCore | ( | mdd_t * | aStates, |
| array_t * | onionRings, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| Mc_PathLengthType | PathLengthType | ||
| ) |
Function********************************************************************
Synopsis [Build Path from Core to aState.]
Description [Build Path starting at a Core state (a state in the first onion ring) to aState. For paths of length at least one, set PathLengthType to McGreaterZero_c; otherwise, use McGreaterOrEqualZero_c. The function returns a sequence of states from the core of onionRings to a aState.
In the case of BFS search, the onion rings are built forward, so that any state in ring i+1 has at least one predecessor in ring i-1. In non-BFS search that may not be true, but we will have that every state in ring i+1 has a predecessor in ring i or less. The fsm is checked to see if the search was BFS. If not, every ring from the beginning is searched to find the shortest path. This is a greedy heuristic and the shortest path is not guaranteed to be found. McBuildPathToCore takes a different approach.
It is the users responsibility to free the array returned as well as its members.]
SideEffects []
SeeAlso[Mc_BuildPathToCore]
Definition at line 558 of file mcUtil.c.
{
int i, j;
int startingPoint;
mdd_t *currentState, *aState;
Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
array_t *pathToCore;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
array_t *toCareSetArray;
array_t *pathFromCore;
mdd_t *currentStatePreds, *currentStatePredsInInnerRing;
mdd_t *innerRing = NIL(mdd_t), *witnessPredState;
boolean shortestDist =
(Fsm_FsmReadReachabilityOnionRingsMode(modelFsm) == Fsm_Rch_Bfs_c);
if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
pathFromCore = Mc_BuildPathFromCoreFAFW(
aStates, onionRings,
modelFsm, PathLengthType);
return(pathFromCore);
}
aState = Mc_ComputeAState(aStates, modelFsm);
pathToCore = array_alloc( mdd_t * , 0 );
toCareSetArray = NIL(array_t);
if ( PathLengthType == McGreaterZero_c ) {
startingPoint = 1;
}
else if ( PathLengthType == McGreaterOrEqualZero_c ) {
startingPoint = 0;
}
else {
fail("Called Mc_BuildPathFromCore with ill formed PathLengthType\n");
}
/* check that the state occurs in an onion ring. */
for ( i = startingPoint ; i < array_n( onionRings ); i++ ) {
mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
if ( McStateTestMembership( aState, ring ) )
break;
}
if ( i == array_n( onionRings ) ) {
mdd_free(aState);
return NIL(array_t);
}
/* insert the state in the path to the core */
currentState = aState;
array_insert_last( mdd_t *, pathToCore, currentState );
/* initialize */
toCareSetArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, toCareSetArray, mdd_one(mddMgr));
/* loop until a path is found to the core */
while( i-- > 0 ) {
if (shortestDist) {
/* a predecessor is guaranteed to be in the previous ring */
mdd_array_free(toCareSetArray);
toCareSetArray = array_alloc(mdd_t *, 0);
innerRing = array_fetch( mdd_t *, onionRings, i );
array_insert(mdd_t *, toCareSetArray, 0, mdd_dup(innerRing));
currentStatePreds = Img_ImageInfoComputePreImageWithDomainVars(
imageInfo, currentState,
currentState, toCareSetArray);
} else {
/* compute the predecessors */
currentStatePreds = Img_ImageInfoComputePreImageWithDomainVars(
imageInfo, currentState,
currentState, toCareSetArray );
/* search for a predecessor in the earliest onion ring */
for (j = 0; j <= i; j++) {
innerRing = array_fetch( mdd_t *, onionRings, j );
if (!mdd_lequal(currentStatePreds, innerRing, 1, 0)) {
i = j;
break;
}
}
}
/* compute the set of predecessors in the chosen ring. */
currentStatePredsInInnerRing = mdd_and(currentStatePreds, innerRing, 1, 1);
mdd_free( currentStatePreds );
/* find a state in the predecessor */
witnessPredState = Mc_ComputeACloseState(currentStatePredsInInnerRing,
currentState, modelFsm);
mdd_free( currentStatePredsInInnerRing );
/* insert predecessor in the path */
array_insert_last( mdd_t *, pathToCore, witnessPredState );
currentState = witnessPredState;
}
mdd_array_free(toCareSetArray);
/* flip the path to a path from the core */
{
int i;
pathFromCore = array_alloc( mdd_t *, 0 );
for( i=0; i < array_n( pathToCore ); i++ ) {
mdd_t *tmpMdd = array_fetch(mdd_t *, pathToCore,
(array_n(pathToCore) - (i+1)));
array_insert_last( mdd_t *, pathFromCore, tmpMdd );
}
array_free( pathToCore );
return pathFromCore;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_BuildPathFromCoreFAFW | ( | mdd_t * | Ts, |
| array_t * | rings, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| Mc_PathLengthType | PathLengthType | ||
| ) |
Function********************************************************************
Synopsis [Build a path from target to initial state.]
Description [Build a path from target to initial state. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
free
array_insert_last(mdd_t *, R, T);
T = mdd_dup(T);
mdd_free(T);
Definition at line 1035 of file mcUtil.c.
{
int startingPoint, prevFlag;
int i, p, dist, forced;
bdd_t *T, *S, *H, *nH, *Hp, *S1, *Swin;
bdd_t *ring, *oneMdd, *zeroMdd;
array_t *C, *newC, *AUrings, *segment;
array_t *R, *ESrings;
array_t *careStatesArray;
array_t *pathFromCore;
bdd_t *T_wedge_ring, *S1_wedge_ring, *Hp_wedge_S1;
bdd_t *T_wedge_S, *C_T_wedge_S, *ESresult, *EX_T;
bdd_t *EX_T_wedge_ring, *Hp_wedge_EX_T, *lastR;
bdd_t *C_T_wedge_ring, *new_, *extCube;
bdd_t *bundle, *single, *preSingle;
Img_ImageInfo_t *imageInfo;
mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);
if(Fsm_FsmReadFAFWFlag(modelFsm) == 2) {
pathFromCore = Mc_BuildPathFromCoreFAFWGeneral(
Ts, rings,
modelFsm, PathLengthType);
return(pathFromCore);
}
T = mdd_dup(Ts);
imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
if ( PathLengthType == McGreaterZero_c ) {
startingPoint = 1;
}
else if( PathLengthType == McGreaterOrEqualZero_c ) {
startingPoint = 0;
}
else {
fail("Called Mc_BuildPathFromCoreFAFW with ill formed PathLengthType\n");
}
oneMdd = mdd_one(mgr);
zeroMdd = mdd_zero(mgr);
S = mdd_dup(array_fetch(mdd_t *, rings, startingPoint));
prevFlag = 0;
H = mdd_zero(mgr);
for(i=startingPoint; i<array_n(rings); i++) {
ring = array_fetch(mdd_t *, rings, i);
new_ = mdd_and(ring, H, 1, 0);
mdd_free(ring);
nH = mdd_or(new_, H, 1, 1);
mdd_free(H);
H = nH;
array_insert(mdd_t *, rings, i, new_);
}
C = array_alloc(mdd_t *, 0);
T_wedge_S = mdd_and(T, S, 1, 1);
if(!mdd_equal(T_wedge_S, zeroMdd)) {
if(startingPoint == 1) {
mdd_free(T);
T = array_fetch(mdd_t *, rings, 0);
array_insert_last(mdd_t *, C, bdd_dup(T));
}
C_T_wedge_S = bdd_closest_cube(T_wedge_S, S, &dist);
array_insert_last(mdd_t *, C, C_T_wedge_S);
mdd_free(S);
mdd_free(oneMdd);
mdd_free(zeroMdd);
mdd_free(H);
mdd_free(T_wedge_S);
return(C);
}
mdd_free(T_wedge_S);
T_wedge_ring = NULL;
for(p=startingPoint; p<array_n(rings); p++) {
ring = array_fetch(mdd_t *, rings, p);
T_wedge_ring = mdd_and(T, ring, 1, 1);
if(!mdd_equal(T_wedge_ring, zeroMdd)) {
break;
}
mdd_free(T_wedge_ring);
}
mdd_free(T);
C_T_wedge_ring = bdd_closest_cube(T_wedge_ring, S, &dist);
mdd_free(T_wedge_ring);
array_insert_last(mdd_t *, C, C_T_wedge_ring);
T = C_T_wedge_ring;
extCube = Fsm_FsmReadExtQuantifyInputCube(modelFsm);
careStatesArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, careStatesArray, oneMdd);
while(1) {
if(prevFlag == 0) { /* free segement */
prevFlag = 1; /* force segment */
for(i=array_n(rings)-1; i>p; i--) {
ring = array_fetch(mdd_t *, rings, i);
nH = mdd_and(H, ring, 1, 0);
mdd_free(H);
H = nH;
}
AUrings = array_alloc(mdd_t *, 0);
Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 1);
Swin = Mc_FsmEvaluateAUFormula(modelFsm, H, T,
NIL(mdd_t), oneMdd, careStatesArray,
MC_NO_EARLY_TERMINATION, NIL(array_t),
Mc_None_c, AUrings, McVerbosityNone_c,
McDcLevelNone_c, NIL(boolean));
Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 0);
S1 = bdd_smooth_with_cube(Swin, extCube);
mdd_array_free(AUrings);
if(mdd_equal(S1, T)) {
mdd_free(S1);
mdd_free(Swin);
continue;
}
for(i=p-1; i>=startingPoint; i--) {
ring = array_fetch(mdd_t *, rings, i);
S1_wedge_ring = mdd_and(S1, ring, 1, 1);
if(mdd_equal(S1_wedge_ring, zeroMdd)) {
mdd_free(S1_wedge_ring);
break;
}
mdd_free(S1_wedge_ring);
}
p = i+1;
Hp = array_fetch(mdd_t *, rings, p);
ESrings = array_alloc(mdd_t *, 0);
Hp_wedge_S1 = mdd_and(Hp, S1, 1, 1);
ESresult = McEvaluateESFormulaWithGivenTRFAFW( modelFsm, S1, Hp_wedge_S1,
NIL(mdd_t), oneMdd, careStatesArray,
MC_NO_EARLY_TERMINATION, ESrings,
McVerbosityNone_c, McDcLevelNone_c,
NIL(boolean), Swin);
mdd_free(ESresult);
mdd_free(Hp_wedge_S1);
mdd_free(S1);
R = ESrings;
if(array_n(R) <= 1) {
mdd_array_free(R);
mdd_free(Swin);
continue;
}
}
else { /* force segment */
Swin = 0;
prevFlag = 0; /* free segment */
EX_T = Img_ImageInfoComputePreImageWithDomainVars(
imageInfo, T, T, careStatesArray);
for(i=p-1; i>=startingPoint; i--) {
ring = array_fetch(mdd_t *, rings, i);
EX_T_wedge_ring = mdd_and(EX_T, ring, 1, 1);
if(mdd_equal(EX_T_wedge_ring, zeroMdd)) {
mdd_free(EX_T_wedge_ring);
break;
}
mdd_free(EX_T_wedge_ring);
}
p = i+1;
Hp = array_fetch(mdd_t *, rings, p);
R = array_alloc(mdd_t *, 0);
Hp_wedge_EX_T = mdd_and(Hp, EX_T, 1, 1);
array_insert_last(mdd_t *, R, Hp_wedge_EX_T);
array_insert_last(mdd_t *, R, mdd_dup(T));
mdd_free(EX_T);
}
lastR = array_fetch(mdd_t *, R, 0);
segment = Mc_BuildShortestPathFAFW(Swin, lastR, T, R, mgr, modelFsm, prevFlag);
if(Swin) {
mdd_free(Swin);
Swin = 0;
}
mdd_array_free(R);
newC = array_join(C, segment);
array_free(C);
C = newC;
T = array_fetch(mdd_t *, segment, array_n(segment)-1);
if((long)T %2) T = (mdd_t *)((long)T - 1);
array_free(segment);
T_wedge_S = mdd_and(T, S, 1, 1);
if(!mdd_equal(T_wedge_S, zeroMdd)) {
mdd_free(T_wedge_S);
mdd_free(S);
mdd_free(H);
break;
}
mdd_free(T_wedge_S);
startingPoint = 0;
mdd_free(S);
S = mdd_dup(array_fetch(mdd_t *, rings, startingPoint));
}
array_free(careStatesArray);
mdd_free(oneMdd);
mdd_free(zeroMdd);
{
int i;
pathFromCore = array_alloc( mdd_t *, 0 );
if(startingPoint == 1) {
T = array_fetch(mdd_t *, rings, 0);
array_insert_last(mdd_t *, pathFromCore, bdd_dup(T));
}
preSingle = NULL;
for( i=0; i < array_n( C ); i++ ) {
bundle = array_fetch(mdd_t *, C, (array_n(C) - (i+1)));
forced = 0;
if((long)bundle%2) {
bundle = (mdd_t *)((long)bundle -1);
forced++;
}
if(i==0)
single = Mc_ComputeAState(bundle, modelFsm);
else
single = Mc_ComputeACloseState(bundle, preSingle, modelFsm);
array_insert_last( mdd_t *, pathFromCore,
(mdd_t *)((long)(single) + forced) );
preSingle = single;
}
McNormalizeBddPointer(C);
mdd_array_free(C);
return pathFromCore;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_BuildPathFromCoreFAFWGeneral | ( | mdd_t * | T, |
| array_t * | rings, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| Mc_PathLengthType | PathLengthType | ||
| ) |
Function********************************************************************
Synopsis [Build a path from target to initial state with general algorithm.]
Description [Build a path from target to initial state with general algorithm. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
Definition at line 737 of file mcUtil.c.
{
mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);
mdd_t *S, *H, *nH, *ring;
int i;
array_t *L;
array_t *pathFromCore;
array_t *npathFromCore;
H = mdd_zero(mgr);
for(i=0; i<array_n(rings); i++) {
ring = array_fetch(mdd_t *, rings, i);
nH = mdd_or(ring, H, 1, 1);
mdd_free(H);
H = nH;
}
nH = mdd_and(H, T, 1, 1);
T = nH;
L = Mc_BuildFAFWLayer(modelFsm, mdd_dup(T), mdd_dup(H));
if ( PathLengthType == McGreaterZero_c ) {
S = mdd_dup(array_fetch(mdd_t *, rings, 1));
}
else if( PathLengthType == McGreaterOrEqualZero_c ) {
S = mdd_dup(array_fetch(mdd_t *, rings, 0));
}
else {
fail("Called Mc_BuildPathFromCoreFAFW with ill formed PathLengthType\n");
}
pathFromCore =
MC_BuildCounterExampleFAFWGeneral(modelFsm, mdd_dup(S), mdd_dup(T), H, L);
if(PathLengthType == McGreaterZero_c ) {
S = array_fetch(mdd_t *, rings, 0);
npathFromCore = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, npathFromCore, mdd_dup(S));
for(i=0; i<array_n(pathFromCore); i++) {
S = array_fetch(mdd_t *, pathFromCore, i);
array_insert_last(mdd_t *, npathFromCore, S);
}
array_free(pathFromCore);
pathFromCore = npathFromCore;
}
mdd_free(T);
return(pathFromCore);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_BuildPathToCore | ( | mdd_t * | aState, |
| array_t * | onionRings, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| Mc_PathLengthType | PathLengthType | ||
| ) |
Function********************************************************************
Synopsis [Build Path to Core starting at aState.]
Description [Build Path to Core (the first onion ring) starting at aState.
For the onion rings should be built in such a way that for every state v in ring i+1 there is a state v' in ring i such that there is an edge from v to v'. This function will also works for non-BFS rings, where we just require that for every state v in a ring i > 0, there is a state in a ring 0 <= j < i that is a successor of v.
For paths of length at least one, set PathLengthType to McGreaterZero_c. Otherwise, use McGreaterOrEqualZero_c. The function returns a sequence of states to a state in the core of onionRings, starting at aState. It is the users responsibility to free the array returned as well as its members.]
SideEffects []
Definition at line 305 of file mcUtil.c.
{
int i; /* index into the onionRings */
int startingPoint;
mdd_t *currentState;
Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
array_t *pathToCore;
mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
array_t *toCareSetArray;
if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
return(Mc_BuildPathToCoreFAFW(
aState, onionRings, modelFsm, PathLengthType));
}
pathToCore = array_alloc( mdd_t * , 0 );
toCareSetArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, toCareSetArray, mdd_one(mddMgr));
if ( PathLengthType == McGreaterZero_c )
startingPoint = 1;
else if ( PathLengthType == McGreaterOrEqualZero_c )
startingPoint = 0;
else
fail("Called Mc_BuildPathToCore with ill formed PathLengthType\n");
/* RB: How do you guarantee that aState is in one of the onion rings [1,n]?*/
/*Find the lowest ring that holds aState*/
for ( i = startingPoint ; i < array_n( onionRings ); i++ ) {
mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
if ( McStateTestMembership( aState, ring ) )
break;
}
if ( i == array_n( onionRings ) )
return NIL(array_t);
currentState = mdd_dup( aState );
array_insert_last( mdd_t *, pathToCore, currentState );
/* until we get to ring 0, keep finding successors for currentState */
while( i > 0 ) {
mdd_t *currentStateSuccs;
mdd_t *innerRing;
mdd_t *currentStateSuccsInInnerRing;
mdd_t *witnessSuccState;
i--;
currentStateSuccs =
Img_ImageInfoComputeImageWithDomainVars(imageInfo, currentState,
currentState, toCareSetArray);
currentStateSuccsInInnerRing = mdd_zero(mddMgr);
/* find the highest ring that contains a successor, starting with i */
while(mdd_is_tautology(currentStateSuccsInInnerRing, 0)){
assert(i >= 0);
if(i < 0) return NIL(array_t);
innerRing = array_fetch( mdd_t *, onionRings, i );
mdd_free(currentStateSuccsInInnerRing);
currentStateSuccsInInnerRing = mdd_and(currentStateSuccs, innerRing,
1, 1 );
i--;
}
i++;
witnessSuccState = Mc_ComputeACloseState(currentStateSuccsInInnerRing,
currentState,
modelFsm );
array_insert_last( mdd_t *, pathToCore, witnessSuccState );
currentState = witnessSuccState;
mdd_free( currentStateSuccs );
mdd_free( currentStateSuccsInInnerRing );
/* next, see if we cannot move a few more rings down. We have to do this,
* since a nontrivial path is not guaranteed to exist from a node in ring i
* to a node in a lower ring. In fact a state in ring i may also be in
* ring 0. */
{
boolean contained = TRUE;
while(contained && i > 0){
i--;
innerRing = array_fetch( mdd_t *, onionRings, i );
contained = mdd_lequal(witnessSuccState, innerRing, 1, 1);
}
/* i is highest ring not containing witnessSuccState, or i = 0 */
if(!contained){
i++;
}
/* i is lowest ring containing witnessSuccState */
}
}
mdd_array_free(toCareSetArray);
return pathToCore;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_BuildPathToCoreFAFW | ( | mdd_t * | aStates, |
| array_t * | onionRings, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| Mc_PathLengthType | PathLengthType | ||
| ) |
Function********************************************************************
Synopsis [Build a path from initial state to target.]
Description [Build a path from initial state to target. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
Definition at line 683 of file mcUtil.c.
{
int i, startingPoint;
array_t *pathFromCore, *pathToCore;
array_t *reachableOnionRings;
mdd_t *currentStates;
if ( PathLengthType == McGreaterZero_c ) {
startingPoint = 1;
}
else if ( PathLengthType == McGreaterOrEqualZero_c ) {
startingPoint = 0;
}
else {
fail("Called Mc_BuildPathToCore with ill formed PathLengthType\n");
}
for ( i = startingPoint ; i < array_n( onionRings ); i++ ) {
mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
if ( McStateTestMembership( aStates, ring ) )
break;
}
if(i==0) {
pathToCore = array_alloc( mdd_t * , 0 );
array_insert_last( mdd_t *, pathToCore, mdd_dup(aStates) );
return pathToCore;
}
reachableOnionRings = Mc_BuildForwardRings(aStates, modelFsm, onionRings);
currentStates = array_fetch(mdd_t *, onionRings, 0);
pathFromCore = Mc_BuildPathFromCoreFAFW(
currentStates,
reachableOnionRings, modelFsm, PathLengthType);
mdd_array_free(reachableOnionRings);
return(pathFromCore);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_BuildShortestPathFAFW | ( | mdd_t * | win, |
| mdd_t * | S, | ||
| mdd_t * | T, | ||
| array_t * | rings, | ||
| mdd_manager * | mgr, | ||
| Fsm_Fsm_t * | fsm, | ||
| int | prevFlag | ||
| ) |
Function********************************************************************
Synopsis [Build a shortest path from T to S.]
Description [Make a shortest path from T to S which only passes through states in rings. There is always a path from T to S. Returns a sequence of states starting from T, leading to S. It is the users responsibility to free the returned array as well as its members. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
free segment
fated segment
Definition at line 1299 of file mcUtil.c.
{
int q, dist;
mdd_t *zeroMdd, *oneMdd;
mdd_t *inputCube;
mdd_t *ring, *ring_wedge_T, *Cn, *Cs;
mdd_t *K, *realK, *range;
mdd_t *preimage_of_Cn;
array_t *C, *stateVars, *inputVars;
array_t *toCareSetArray;
Img_ImageInfo_t *imageInfo;
imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, 1, 0);
stateVars = Fsm_FsmReadPresentStateVars(fsm);
inputVars = Fsm_FsmReadInputVars(fsm);
inputCube = mdd_id_array_to_bdd_cube(mgr, inputVars);
zeroMdd = mdd_zero(mgr);
oneMdd = mdd_one(mgr);
ring_wedge_T = NULL;
for (q = 0; q < array_n(rings); q++){
ring = array_fetch(mdd_t *, rings, q);
ring_wedge_T = mdd_and(T, ring, 1, 1);
if(!mdd_equal(ring_wedge_T, zeroMdd))
break;
mdd_free(ring_wedge_T);
ring_wedge_T = 0;
}
if(ring_wedge_T) {
mdd_free(ring_wedge_T);
}
else {
fprintf(stdout, "We cannot find T\n");
}
C = array_alloc(mdd_t *, 0);
Cn = (T);
toCareSetArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
range = mdd_range_mdd(mgr, stateVars);
while(q > 0) {
preimage_of_Cn = Img_ImageInfoComputePreImageWithDomainVars(
imageInfo, Cn, Cn, toCareSetArray);
K = NULL;
for (q = 0; q < array_n(rings); q++){
ring = array_fetch(mdd_t *, rings, q);
K = mdd_and(preimage_of_Cn, ring, 1, 1);
if(!mdd_equal(K, zeroMdd))
break;
mdd_free(K);
K = 0;
}
mdd_free(preimage_of_Cn);
realK = mdd_and(K, range, 1, 1);
mdd_free(K);
Cs = bdd_closest_cube(realK, Cn, &dist);
mdd_free(realK);
Cn = bdd_smooth_with_cube(Cs, inputCube);
mdd_free(Cs);
if(!prevFlag)
array_insert_last(mdd_t *, C, Cn);
else
array_insert_last(mdd_t *, C, (mdd_t *)((long)Cn+1));
}
array_free(toCareSetArray);
mdd_free(zeroMdd);
mdd_free(oneMdd);
mdd_free(range);
mdd_free(inputCube);
return(C);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Mc_CheckPathFromCore | ( | Fsm_Fsm_t * | fsm, |
| array_t * | pathFromCore | ||
| ) |
Function********************************************************************
Synopsis [Debug function to check if there exists a proper input value]
Description [Check the existence of path by extracting input condition.]
SideEffects []
Definition at line 5372 of file mcUtil.c.
{
array_t *inputVars;
int i;
mdd_t *fromState, *toState, *inputSet;
mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm));
inputVars = Fsm_FsmReadInputVars( fsm );
for(i=array_n(pathFromCore); i>0; i--) {
fromState = (i==array_n(pathFromCore)) ? 0 : array_fetch(mdd_t *, pathFromCore, i);
toState = array_fetch(mdd_t *, pathFromCore, i-1);
if((long)fromState % 2) fromState = (mdd_t *)((long)fromState - 1);
if((long)toState % 2) toState = (mdd_t *)((long)toState - 1);
inputSet = ( i == array_n(pathFromCore)) ? 0 :
Mc_FsmComputeDrivingInputMinterms( fsm, fromState, toState );
if(inputSet)
Mc_ComputeAMinterm( inputSet, inputVars, mgr );
else if(i != array_n(pathFromCore))
fprintf(vis_stderr, "Illegal path from %d to %d\n", i, i+1);
}
}
Here is the call graph for this function:
| void Mc_CheckPathToCore | ( | Fsm_Fsm_t * | fsm, |
| array_t * | pathToCore | ||
| ) |
Function********************************************************************
Synopsis [Debug function to check if there exists a proper input value]
Description [Check the existence of path by extracting input condition.]
SideEffects []
Definition at line 5338 of file mcUtil.c.
{
array_t *inputVars;
int i;
mdd_t *fromState, *toState, *inputSet;
mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm));
inputVars = Fsm_FsmReadInputVars( fsm );
for(i=-1; i<array_n(pathToCore)-1; i++) {
fromState = (i==-1) ? 0 : array_fetch(mdd_t *, pathToCore, i);
toState = array_fetch(mdd_t *, pathToCore, i+1);
if((long)fromState % 2) fromState = (mdd_t *)((long)fromState - 1);
if((long)toState % 2) toState = (mdd_t *)((long)toState - 1);
inputSet = ( i == -1) ? 0 :
Mc_FsmComputeDrivingInputMinterms( fsm, fromState, toState );
if(inputSet)
Mc_ComputeAMinterm( inputSet, inputVars, mgr );
else if(i != -1)
fprintf(vis_stderr, "Illegal path from %d to %d\n", i, i+1);
}
}
Here is the call graph for this function:
| array_t* Mc_CompletePath | ( | mdd_t * | aState, |
| mdd_t * | bState, | ||
| mdd_t * | invariantStates, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| Mc_FwdBwdAnalysis | dirn | ||
| ) |
Function********************************************************************
Synopsis [Make a path from aState to bState.]
Description [Make a path from aState to bState which only passes through invariantStates; it is assumed that aState and bState lie in invariantStates. Returns a sequence of states starting from aState, leading to bState. If aState == bState, a non trivial path is returned (ie a cycle). If no path exists, return NIL. It is the users responsibility to free the returned array as well as its members.]
SideEffects []
Definition at line 1397 of file mcUtil.c.
{
if ( dirn == McFwd_c ) {
return McCompletePathFwd(aState, bState, invariantStates, modelFsm,
careSetArray, verbosity, dcLevel );
}
else {
return McCompletePathBwd(aState, bState, invariantStates, modelFsm,
careSetArray, verbosity, dcLevel );
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_ComputeACloseMinterm | ( | mdd_t * | aSet, |
| mdd_t * | target, | ||
| array_t * | Support, | ||
| mdd_manager * | mddMgr | ||
| ) |
Function********************************************************************
Synopsis [Pick a minterm from the given set close to target. Support is an array of mddids representing the total support; that is, all the variables on which aSet may depend.]
SideEffects []
Definition at line 1517 of file mcUtil.c.
{
if (bdd_get_package_name() == CUDD && target != NIL(mdd_t)) {
mdd_t *range; /* range of Support */
mdd_t *legalSet; /* aSet without the don't cares */
mdd_t *closeCube;
int dist;
array_t *bddSupport; /* Support in terms of bdd vars */
mdd_t *minterm; /* a random minterm */
/* Check that support of set is contained in Support. */
assert(SetCheckSupport(aSet, Support, mddMgr));
assert(!mdd_is_tautology(aSet, 0));
range = mdd_range_mdd(mddMgr, Support);
legalSet = bdd_and(aSet, range, 1, 1);
mdd_free(range);
closeCube = mdd_closest_cube(legalSet, target, &dist);
bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support);
minterm = bdd_pick_one_minterm(closeCube, bddSupport);
assert(MintermCheckWellFormed(minterm, Support, mddMgr));
assert(mdd_count_onset(mddMgr, minterm, Support) == 1);
assert(mdd_lequal(minterm,legalSet,1,1));
mdd_array_free(bddSupport);
mdd_free(legalSet);
mdd_free(closeCube);
return minterm;
} else {
return Mc_ComputeAMinterm(aSet, Support, mddMgr);
}/* if CUDD */
} /* McComputeACloseMinterm */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_ComputeACloseState | ( | mdd_t * | states, |
| mdd_t * | target, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Select a state from the given set close to target.]
SideEffects []
Definition at line 2161 of file mcUtil.c.
{
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
mdd_t *result = Mc_ComputeACloseMinterm( states, target, PSVars, mddMgr );
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_ComputeAMinterm | ( | mdd_t * | aSet, |
| array_t * | Support, | ||
| mdd_manager * | mddMgr | ||
| ) |
Function********************************************************************
Synopsis [Pick an arbitrary minterm from the given set.]
Description [Pick an arbitrary minterm from the given set. Support is an array of mddids representing the total support; that is, all the variables on which aSet may depend.]
SideEffects []
Definition at line 1430 of file mcUtil.c.
{
/* check that support of set is contained in Support */
assert( SetCheckSupport( aSet, Support, mddMgr ));
assert(!mdd_is_tautology(aSet, 0));
if(bdd_get_package_name() == CUDD){
mdd_t *range; /* range of Support */
mdd_t *legalSet; /* aSet without the don't cares */
array_t *bddSupport; /* Support in terms of bdd vars */
mdd_t *minterm; /* a random minterm */
range = mdd_range_mdd(mddMgr, Support);
legalSet = bdd_intersects(aSet, range);
mdd_free(range);
bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support);
minterm = bdd_pick_one_minterm(legalSet, bddSupport);
assert(MintermCheckWellFormed(minterm, Support, mddMgr));
assert(mdd_count_onset(mddMgr, minterm, Support) == 1);
assert(mdd_lequal(minterm,legalSet,1,1));
mdd_array_free(bddSupport);
mdd_free(legalSet);
return minterm;
}else{
int i, j;
mdd_t *aSetDup;
mdd_t *resultMdd;
array_t *resultMddArray = array_alloc( mdd_t *, 0 );
aSetDup = mdd_dup( aSet );
for( i = 0 ; i < array_n( Support ); i++ ) {
int aSupportVar = array_fetch( int, Support, i );
for( j = 0 ;;) {
mdd_t *faceMdd, *tmpMdd;
array_t *tmpArray = array_alloc( int, 0 );
array_insert_last( int, tmpArray, j );
/* this call will crash if have run through range of mvar */
faceMdd = mdd_literal( mddMgr, aSupportVar, tmpArray );
array_free( tmpArray );
tmpMdd = mdd_and( faceMdd, aSetDup, 1, 1 );
if ( !mdd_is_tautology( tmpMdd, 0 ) ) {
array_insert_last( mdd_t *, resultMddArray, faceMdd );
mdd_free( aSetDup );
aSetDup = tmpMdd;
break;
}
mdd_free( faceMdd );
mdd_free( tmpMdd );
j++;
}
}
mdd_free( aSetDup );
resultMdd = mdd_one( mddMgr );
for ( i = 0 ; i < array_n( resultMddArray ); i++ ) {
mdd_t *faceMdd = array_fetch( mdd_t *, resultMddArray, i );
mdd_t *tmpMdd = mdd_and( faceMdd, resultMdd, 1, 1 );
mdd_free( resultMdd ); mdd_free( faceMdd );
resultMdd = tmpMdd;
}
array_free( resultMddArray );
return resultMdd;
}/* IF CUDD */
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_ComputeAState | ( | mdd_t * | states, |
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Select an arbitrary state from the given set]
SideEffects []
Definition at line 2141 of file mcUtil.c.
{
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
mdd_t *result = Mc_ComputeAMinterm( states, PSVars, mddMgr );
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_ComputeGuideArray | ( | Fsm_Fsm_t * | fsm, |
| FILE * | guideFP | ||
| ) |
Function********************************************************************
Synopsis [Return an array of hints]
Description [Read the guide file and compute the BDDs of the hints and store in an array. Adds the 1 hint to the end of the array.
Closes the guideFP.
Returns NIL if something goes wrong.]
SideEffects []
Definition at line 5280 of file mcUtil.c.
{
Ctlp_FormulaArray_t *hintFormulae;
array_t * hintSets;
hintFormulae = Mc_ReadHints(guideFP);
fclose(guideFP);
if( hintFormulae == NIL(Ctlp_FormulaArray_t))
return NIL(array_t);
hintSets = Mc_EvaluateHints(fsm, hintFormulae);
Ctlp_FormulaArrayFree(hintFormulae);
return hintSets;
}/* Mc_ComputeGuideArray */
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * Mc_ComputeRangeOfPseudoInputs | ( | Ntk_Network_t * | network | ) | [static] |
Function********************************************************************
Synopsis [Return the range of pseudo inputs if they are defined by subsets of range.]
Description [The result can be used to extract correct input conditions.]
SideEffects []
Definition at line 1991 of file mcUtil.c.
{
mdd_manager *mddMgr = Ntk_NetworkReadMddManager( network );
Mvf_Function_t *nodeMvf;
mdd_t *tmpMdd, *zeroMdd;
mdd_t *restrictMdd, *sumMdd;
int restrictFlag;
lsGen gen;
Ntk_Node_t *node;
int i;
zeroMdd = mdd_zero(mddMgr);
restrictMdd = mdd_one(mddMgr);
restrictFlag = 0;
Ntk_NetworkForEachPseudoInput(network, gen, node) {
nodeMvf = NodeBuildPseudoInputMvf(node, mddMgr);
for(i=0; i<nodeMvf->num; i++) {
tmpMdd = array_fetch(mdd_t *, nodeMvf, i);
if(mdd_equal(tmpMdd, zeroMdd)) {
restrictFlag = 1;
break;
}
}
if(restrictFlag) {
sumMdd = mdd_zero(mddMgr);
for(i=0; i<nodeMvf->num; i++) {
tmpMdd = array_fetch(mdd_t *, nodeMvf, i);
if(!mdd_equal(tmpMdd, zeroMdd)) {
tmpMdd = mdd_or( sumMdd, tmpMdd, 1, 1 );
mdd_free(sumMdd);
sumMdd = tmpMdd;
}
}
tmpMdd = mdd_and( sumMdd, restrictMdd, 1, 1 );
mdd_free(sumMdd);
mdd_free(restrictMdd);
restrictMdd = tmpMdd;
}
Mvf_FunctionFree(nodeMvf);
}
mdd_free(zeroMdd);
return(restrictMdd);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Fsm_Fsm_t* Mc_ConstructReducedFsm | ( | Ntk_Network_t * | network, |
| array_t * | ctlFormulaArray | ||
| ) |
Function********************************************************************
Synopsis [Form an FSM reduced with respect to the specified formula]
Description [Form an FSM reduced with respect to the CTL formula array. All latches and inputs which affect the given formula AND the fairness conditions of the system are included in this reduced fsm.]
SideEffects []
Definition at line 2238 of file mcUtil.c.
{
return(McConstructReducedFsm(network, ctlFormulaArray));
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Mc_EarlyTermination_t* Mc_EarlyTerminationAlloc | ( | Mc_EarlyTerminationType | mode, |
| mdd_t * | states | ||
| ) |
Function********************************************************************
Synopsis [Allocate an earlytermination struct and initialize with arguments]
SideEffects []
Definition at line 2292 of file mcUtil.c.
{
Mc_EarlyTermination_t *result = ALLOC(Mc_EarlyTermination_t, 1);
result->mode = mode;
if (states != NIL(mdd_t)) {
result->states = mdd_dup(states);
} else {
result->states = NIL(mdd_t);
}
return result;
}
Here is the caller graph for this function:
| void Mc_EarlyTerminationFree | ( | Mc_EarlyTermination_t * | earlyTermination | ) |
Function********************************************************************
Synopsis [Free an earlytermination struct (you are allowed to pass MC_NO_EARLY_TERMINATION, or NULL, and it will have no effect. ]
SideEffects []
Definition at line 2316 of file mcUtil.c.
{
if(earlyTermination == NIL(Mc_EarlyTermination_t) ||
earlyTermination == MC_NO_EARLY_TERMINATION)
return;
if(earlyTermination->states != NIL(mdd_t))
mdd_free(earlyTermination->states);
free(earlyTermination);
return;
}
Here is the caller graph for this function:
| boolean Mc_EarlyTerminationIsSkip | ( | Mc_EarlyTermination_t * | earlyTermination | ) |
Function********************************************************************
Synopsis [Return TRUE iff the early termination condition specifies that the computation can be entirely skipped.]
SideEffects [none]
Definition at line 2338 of file mcUtil.c.
{
if (earlyTermination == NIL(Mc_EarlyTermination_t) ||
earlyTermination == MC_NO_EARLY_TERMINATION)
return FALSE;
return (earlyTermination->mode == McCare_c &&
earlyTermination->states == NIL(mdd_t));
}
Here is the caller graph for this function:
| array_t* Mc_EvaluateHints | ( | Fsm_Fsm_t * | fsm, |
| Ctlp_FormulaArray_t * | invarArray | ||
| ) |
Function********************************************************************
Synopsis [Return an array of states corresponding to the hints]
Description [Flushes the states associated with the hints,and reevaluates them in the current fsm. Quantifies out variables in the hint that are not in present state or primary input set of the current FSM.
Returns NIL if something goes wrong (the hint does not fit the fsm).]
SideEffects []
Definition at line 5175 of file mcUtil.c.
{
array_t *invarStatesArray = NIL(array_t);/* array of sets of states: hints*/
int i, j; /* to iterate over formulae */
Ctlp_Formula_t *formula= NIL(Ctlp_Formula_t);/* idem */
mdd_t *invarFormulaStates = NIL(mdd_t);/* states in which formula is true */
mdd_t *one = NIL(mdd_t);
array_t *psVars = Fsm_FsmReadPresentStateVars(fsm);
array_t *inputVars = Fsm_FsmReadInputVars(fsm);
array_t *psInputVars = array_join(psVars, inputVars);
mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
invarStatesArray = array_alloc(mdd_t *, 0);
one = mdd_one(Fsm_FsmReadMddManager(fsm));
arrayForEachItem(Ctlp_Formula_t *, invarArray, i, formula){
/* semantic checks */
if(!Mc_FormulaStaticSemanticCheckOnNetwork(formula,
Fsm_FsmReadNetwork(fsm),
TRUE)){
(void) fprintf(vis_stdout,
"** mc error: Error evaluating hint:\n%s\n",
error_string());
mdd_free(one);
mdd_array_free(invarStatesArray);
return NIL(array_t);
}/* if semantic error */
assert(Ctlp_FormulaTestIsQuantifierFree(formula));
Ctlp_FlushStates(formula);
/* compute the set of states represented by the invariant. */
invarFormulaStates =
Mc_FsmEvaluateFormula(fsm, formula, one,
NIL(Fsm_Fairness_t), NIL(array_t),
MC_NO_EARLY_TERMINATION,
NIL(Fsm_HintsArray_t), Mc_None_c,
McVerbosityNone_c, McDcLevelNone_c, 0,
McGSH_EL_c);
if (!mdd_check_support(mddMgr, invarFormulaStates, psInputVars)) {
mdd_t *temp;
int mddId;
array_t *supportArray = mdd_get_support(mddMgr, invarFormulaStates);
array_t *leftOverVars = array_alloc(int, 0);
/* store the PS and the Input Vars of this FSM */
st_table *supportTable = st_init_table(st_numcmp, st_numhash);
arrayForEachItem(int, psInputVars, j, mddId) {
(void) st_insert(supportTable, (char *) (long) mddId, NIL(char));
}
/* isolate the vars outside this FSM */
arrayForEachItem(int, supportArray, j, mddId) {
if (st_is_member(supportTable, (char *)(long)mddId) == 0) {
array_insert_last(int, leftOverVars, mddId);
}
}
/* Quantify them out */
if (array_n(leftOverVars) > 0) {
fprintf(vis_stdout, "GS warning ** Quantifying out variables not relevant to the reduced FSM in hint %d. \n", i+1);
arrayForEachItem(int, leftOverVars, j, mddId) {
fprintf(vis_stdout, "%s\n", (mdd_get_var_by_id(mddMgr, mddId)).name);
}
temp = mdd_smooth(mddMgr, invarFormulaStates, leftOverVars);
mdd_free(invarFormulaStates);
invarFormulaStates = temp;
}
array_free(leftOverVars);
st_free_table(supportTable);
array_free(supportArray);
}
array_insert_last(mdd_t *, invarStatesArray, invarFormulaStates);
}/* for each formula */
array_free(psInputVars);
mdd_free(one);
return invarStatesArray;
}/* Mc_EvaluateHints */
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean Mc_FormulaStaticSemanticCheckOnNetwork | ( | Ctlp_Formula_t * | formula, |
| Ntk_Network_t * | network, | ||
| boolean | inputsAllowed | ||
| ) |
Function********************************************************************
Synopsis [Perform static semantic check of ctl formula on network.]
Description [Perform static semantic check of ctl formula on network. Specifically, given an atomic formula of the form LHS=RHS, check that the LHS is the name of a latch/wire in the network, and that RHS is of appropriate type (enum/integer) and is lies in the range of the latch/wire values. If LHS is a wire, and inputsAllowed is false, check to see that the algebraic support of the wire consists of only latches and constants.]
SideEffects []
Definition at line 249 of file mcUtil.c.
{
boolean lCheck;
boolean rCheck;
Ctlp_Formula_t *leftChild;
Ctlp_Formula_t *rightChild;
if(formula == NIL(Ctlp_Formula_t)){
return TRUE;
}
if(Ctlp_FormulaReadType(formula) == Ctlp_ID_c){
return AtomicFormulaCheckSemantics(formula, network, inputsAllowed);
}
leftChild = Ctlp_FormulaReadLeftChild(formula);
rightChild = Ctlp_FormulaReadRightChild(formula);
lCheck = Mc_FormulaStaticSemanticCheckOnNetwork(leftChild, network,
inputsAllowed);
if(!lCheck)
return FALSE;
rCheck = Mc_FormulaStaticSemanticCheckOnNetwork(rightChild, network,
inputsAllowed);
if (!rCheck)
return FALSE;
return TRUE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mc_FsmComputeDrivingInputMinterms | ( | Fsm_Fsm_t * | fsm, |
| mdd_t * | aState, | ||
| mdd_t * | bState | ||
| ) |
Function********************************************************************
Synopsis [Return all inputs which cause a transition from aState to bState.]
Description [Return all inputs which cause a transition from aState to bState. It is assumed that aState,bState are truly minterms over the PS variables.]
SideEffects []
Definition at line 2049 of file mcUtil.c.
{
int i;
int psMddId;
int inputMddId;
mdd_gen *mddGen;
Ntk_Node_t *latch, *node, *dataNode;
array_t *aMinterm, *bMinterm;
mdd_t *resultMdd;
array_t *resultMvfs;
array_t *inputArray = Fsm_FsmReadInputVars( fsm );
array_t *psArray = Fsm_FsmReadPresentStateVars( fsm );
Ntk_Network_t *network = Fsm_FsmReadNetwork( fsm );
st_table *leaves = st_init_table(st_ptrcmp, st_ptrhash);
array_t *roots = array_alloc( Ntk_Node_t *, 0 );
array_t *latches = array_alloc( Ntk_Node_t *, 0 );
array_t *support = array_alloc( int, 0 );
mdd_t *rangeOfPseudoInputs, *tmpMdd;
arrayForEachItem(int , psArray, i, psMddId ) {
latch = Ntk_NetworkFindNodeByMddId( network, psMddId );
dataNode = Ntk_LatchReadDataInput( latch );
array_insert_last( int, support, psMddId );
array_insert_last( Ntk_Node_t *, roots, dataNode );
array_insert_last( Ntk_Node_t *, latches, latch );
}
/* Convert the minterm to an array of assignments to support vars. */
foreach_mdd_minterm(aState, mddGen, aMinterm, support) {
mdd_gen_free(mddGen);
break;
/* NOT REACHED */
}
foreach_mdd_minterm(bState, mddGen, bMinterm, support) {
mdd_gen_free(mddGen);
break;
/* NOT REACHED */
}
array_free( support );
arrayForEachItem(int , inputArray, i, inputMddId ) {
node = Ntk_NetworkFindNodeByMddId( network, inputMddId );
st_insert(leaves, (char *) node, (char *) NTM_UNUSED );
}
for ( i = 0 ; i < array_n( roots ); i++ ) {
int value = array_fetch( int, aMinterm, i );
latch = array_fetch( Ntk_Node_t *, latches, i );
st_insert( leaves, (char *) latch, (char *) (long) value );
}
resultMvfs = Ntm_NetworkBuildMvfs( network, roots, leaves, NIL(mdd_t) );
array_free( roots );
array_free( latches );
st_free_table( leaves );
rangeOfPseudoInputs = Mc_ComputeRangeOfPseudoInputs(network);
resultMdd = rangeOfPseudoInputs;
for ( i = 0 ; i < array_n( resultMvfs ) ; i++ ) {
Mvf_Function_t *mvf = array_fetch( Mvf_Function_t *, resultMvfs, i );
int value = array_fetch( int, bMinterm, i );
mdd_t *activeMdd = Mvf_FunctionReadComponent( mvf, value );
tmpMdd = mdd_and( activeMdd, resultMdd, 1, 1 );
if(mdd_is_tautology(tmpMdd, 0)) {
fprintf(stdout, "current error\n");
}
mdd_free( resultMdd );
resultMdd = tmpMdd;
Mvf_FunctionFree( mvf );
}
array_free( resultMvfs);
array_free( aMinterm );
array_free( bMinterm );
return resultMdd;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int Mc_FsmComputeStatesReachableFromSet | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | initialStates, | ||
| array_t * | careStatesArray, | ||
| mdd_t * | specialStates, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Return Boolean TRUE/FALSE depending on whether states in specialStates are reachable from initialStates.]
Description [Return Boolean TRUE/FALSE depending on whether states in specialStates are reachable from initialStates.If true, onionRings is set to results of fixed point computation going forward from initialStates to specialStates. Otherwise onionRings is freed.]
SideEffects []
Definition at line 167 of file mcUtil.c.
{
boolean reachable=FALSE;
mdd_t *fromUpperBound;
mdd_t *toCareSet;
array_t *toCareSetArray = array_alloc(mdd_t *, 0);
mdd_t *image;
Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
mdd_t *reachableStates = mdd_dup( initialStates );
mdd_t *fromLowerBound = mdd_dup( initialStates );
/* Iterate until fromLowerBound is empty. */
while (mdd_is_tautology(fromLowerBound, 0) == 0){
/* fromLowerBound is the "onion shell" of states just reached. */
array_insert_last(mdd_t*, onionRings,
mdd_dup(fromLowerBound));
if (!mdd_lequal( fromLowerBound, specialStates, 1, 0 ) ) {
mdd_free( fromLowerBound );
mdd_free( reachableStates );
return TRUE;
}
/* fromUpperBound is the set of all states reached thus far. */
fromUpperBound = mdd_dup( reachableStates );
/* toCareSet is the set of all states not reached so far. */
toCareSet = mdd_not(reachableStates);
array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
/*
* Image of some set between lower and upper, where we care
* about the image only on unreached states.
*/
image = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
fromLowerBound, fromUpperBound, toCareSetArray);
mdd_free(toCareSet);
mdd_free(fromLowerBound);
/* New set of reachable states is old set plus new image. */
mdd_free( reachableStates );
reachableStates = mdd_or(fromUpperBound, image, 1, 1);
mdd_free(image);
/*
* New lower bound is the states just reached (note not on
* fromUpperBound).
*/
fromLowerBound = mdd_and(reachableStates, fromUpperBound, 1, 0);
mdd_free(fromUpperBound);
}
mdd_array_free( onionRings );
mdd_free( reachableStates );
mdd_free(fromLowerBound);
array_free(toCareSetArray);
return reachable;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int Mc_FsmComputeStatesReachingToSet | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | targetStates, | ||
| array_t * | careStatesArray, | ||
| mdd_t * | specialStates, | ||
| array_t * | onionRings, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Return Boolean TRUE/FALSE depending on whether states in specialStates can reach states in targetStates.]
Description [Return Boolean TRUE/FALSE depending on whether states in specialStates can reach states in targetStates. If true, onionRings is set to results of fixed point computation going back from targetStates to specialStates.]
SideEffects []
Definition at line 87 of file mcUtil.c.
{
mdd_t *fromUpperBound;
mdd_t *toCareSet;
array_t *toCareSetArray = array_alloc(mdd_t *, 0);
mdd_t *image;
Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
mdd_t *reachingStates = mdd_dup( targetStates );
mdd_t *fromLowerBound = mdd_dup( targetStates );
/* Iterate until fromLowerBound is empty. */
while (mdd_is_tautology(fromLowerBound, 0) == 0){
/* fromLowerBound is the "onion shell" of states just examined. */
array_insert_last(mdd_t*, onionRings,
mdd_dup(fromLowerBound));
if ( !mdd_lequal( fromLowerBound, specialStates, 1, 0 ) ) {
mdd_free( fromLowerBound );
mdd_free( reachingStates );
return TRUE;
}
/* fromUpperBound is the set of all states reaching targets thus far. */
fromUpperBound = mdd_dup( reachingStates );
/* toCareSet is the set of all states not reached so far. */
toCareSet = mdd_not(reachingStates);
array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
/*
* Pre-Image of some set between lower and upper, where we care
* about the image only on unreaching states.
*/
image = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
fromLowerBound, fromUpperBound, toCareSetArray);
mdd_free(toCareSet);
mdd_free(fromLowerBound);
/* New set of reaching states is old set plus new image. */
mdd_free( reachingStates );
reachingStates = mdd_or(fromUpperBound, image, 1, 1);
mdd_free(image);
/*
* New lower bound is the states just reached (note not on
* fromUpperBound).
*/
fromLowerBound = mdd_and(reachingStates, fromUpperBound, 1, 0);
mdd_free(fromUpperBound);
}
mdd_array_free( onionRings );
mdd_free( reachingStates );
mdd_free(fromLowerBound);
array_free(toCareSetArray);
return FALSE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Mc_MintermPrint | ( | mdd_t * | aMinterm, |
| array_t * | support, | ||
| Ntk_Network_t * | aNetwork | ||
| ) |
Function********************************************************************
Synopsis [Print a minterm.]
SideEffects []
Definition at line 2182 of file mcUtil.c.
{
char *tmpString = Mc_MintermToString( aMinterm, support, aNetwork );
fprintf( vis_stdout, "%s", tmpString );
FREE(tmpString);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| char* Mc_MintermToString | ( | mdd_t * | aMinterm, |
| array_t * | aSupport, | ||
| Ntk_Network_t * | aNetwork | ||
| ) |
Function********************************************************************
Synopsis [Return a string for a minterm.]
SideEffects []
Definition at line 1710 of file mcUtil.c.
{
int i;
char *tmp1String;
char *tmp2String;
char bodyString[McMaxStringLength_c];
char *mintermString = NIL(char);
mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork );
array_t *valueArray;
array_t *stringArray = array_alloc( char *, 0 );
aMinterm = GET_NORMAL_PT(aMinterm);
valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr);
for ( i = 0 ; i < array_n( aSupport ); i++ ) {
int mddId = array_fetch( int, aSupport, i );
int value = array_fetch( int, valueArray, i );
Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
char *nodeName = Ntk_NodeReadName( node );
Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar,
value );
sprintf( bodyString, "%s:%s", nodeName, symbolicValue );
}
else {
sprintf( bodyString, "%s:%d", nodeName, value );
}
tmp1String = util_strsav( bodyString );
array_insert_last( char *, stringArray, tmp1String );
}
array_free(valueArray);
array_sort( stringArray, cmp);
for ( i = 0 ; i < array_n( stringArray ); i++ ) {
tmp1String = array_fetch( char *, stringArray, i );
if( i == 0 ) {
mintermString = util_strcat3(tmp1String, "", "" );
}
else {
tmp2String = util_strcat3(mintermString, "\n", tmp1String );
FREE(mintermString);
mintermString = tmp2String;
}
FREE(tmp1String);
}
array_free( stringArray );
tmp1String = util_strcat3(mintermString, "\n", "");
FREE(mintermString);
mintermString = tmp1String;
return mintermString;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| char* Mc_MintermToStringAiger | ( | mdd_t * | aMinterm, |
| array_t * | aSupport, | ||
| Ntk_Network_t * | aNetwork | ||
| ) |
Function********************************************************************
Synopsis [Return a string for a minterm.]
SideEffects []
Definition at line 1567 of file mcUtil.c.
{
int i;
char *tmp1String;
char *tmp2String;
char bodyString[McMaxStringLength_c];
char *mintermString = NIL(char);
mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork );
array_t *valueArray;
array_t *stringArray = array_alloc( char *, 0 );
aMinterm = GET_NORMAL_PT(aMinterm);
valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr);
for ( i = 0 ; i < array_n( aSupport ); i++ ) {
int mddId = array_fetch( int, aSupport, i );
int value = array_fetch( int, valueArray, i );
Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
char *nodeName = Ntk_NodeReadName( node );
if(!((nodeName[0] == '$') && (nodeName[1] == '_')))
{
Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar,
value );
sprintf( bodyString, "%s", symbolicValue );
}
else {
sprintf( bodyString, "%d", value );
}
tmp1String = util_strsav( bodyString );
array_insert_last( char *, stringArray, tmp1String );
}
}
array_free(valueArray);
array_sort( stringArray, cmp);
for ( i = 0 ; i < array_n( stringArray ); i++ ) {
tmp1String = array_fetch( char *, stringArray, i );
if( i == 0 ) {
mintermString = util_strcat3(tmp1String, "", "" );
}
else {
tmp2String = util_strcat3(mintermString, "", tmp1String );
FREE(mintermString);
mintermString = tmp2String;
}
FREE(tmp1String);
}
array_free( stringArray );
tmp1String = util_strcat3(mintermString, " ", "");
FREE(mintermString);
mintermString = tmp1String;
return mintermString;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| char* Mc_MintermToStringAigerInput | ( | mdd_t * | aMinterm, |
| array_t * | aSupport, | ||
| Ntk_Network_t * | aNetwork | ||
| ) |
Function********************************************************************
Synopsis [Return a string for a minterm.]
SideEffects []
Definition at line 1639 of file mcUtil.c.
{
int i;
char *tmp1String;
char *tmp2String;
char bodyString[McMaxStringLength_c];
char *mintermString = NIL(char);
mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork );
array_t *valueArray;
array_t *stringArray = array_alloc( char *, 0 );
aMinterm = GET_NORMAL_PT(aMinterm);
valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr);
for ( i = 0 ; i < array_n( aSupport ); i++ ) {
int mddId = array_fetch( int, aSupport, i );
int value = array_fetch( int, valueArray, i );
Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
char *nodeName = Ntk_NodeReadName( node );
if((nodeName[0] == '$') && (nodeName[1] == '_'))
{
Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar,
value );
sprintf( bodyString, "%s", symbolicValue );
}
else {
sprintf( bodyString, "%d", value );
}
tmp1String = util_strsav( bodyString );
array_insert_last( char *, stringArray, tmp1String );
}
}
array_free(valueArray);
array_sort( stringArray, cmp);
for ( i = 0 ; i < array_n( stringArray ); i++ ) {
tmp1String = array_fetch( char *, stringArray, i );
if( i == 0 ) {
mintermString = util_strcat3(tmp1String, "", "" );
}
else {
tmp2String = util_strcat3(mintermString, "", tmp1String );
FREE(mintermString);
mintermString = tmp2String;
}
FREE(tmp1String);
}
array_free( stringArray );
tmp1String = util_strcat3(mintermString, " ", "");
FREE(mintermString);
mintermString = tmp1String;
return mintermString;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Mc_NodeTableAddCtlFormulaNodes | ( | Ntk_Network_t * | network, |
| Ctlp_Formula_t * | formula, | ||
| st_table * | nodesTable | ||
| ) |
Function********************************************************************
Synopsis [Add nodes for wires referred to in formula to nodesTable.]
SideEffects []
Definition at line 2200 of file mcUtil.c.
{
NodeTableAddCtlFormulaNodes( network, formula, nodesTable );
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Mc_NodeTableAddLtlFormulaNodes | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | formula, | ||
| st_table * | nodesTable | ||
| ) |
Function********************************************************************
Synopsis [Add nodes for wires referred to in formula to nodesTable.]
Description [Add nodes for wires referred to in formula to nodesTable.]
SideEffects []
Definition at line 2218 of file mcUtil.c.
{
NodeTableAddLtlFormulaNodes(network, formula, nodesTable);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Mc_PrintNumRings | ( | Fsm_Fsm_t * | modelFsm, |
| array_t * | onionRings | ||
| ) |
Function********************************************************************
Synopsis [Print the number of states of each ring]
Description [Print the number of states of each ring]
SideEffects []
Definition at line 5546 of file mcUtil.c.
{
int j;
mdd_t *innerRing;
if(array_n(onionRings) > 0) {
for(j=0; j<array_n(onionRings); j++) {
innerRing = array_fetch(mdd_t *, onionRings, j);
fprintf(vis_stdout, "%d'th ring : ", j);
if(innerRing)
Mc_PrintNumStates(modelFsm, innerRing);
else
fprintf(vis_stdout, "\n");
}
}
}
Here is the call graph for this function:
| void Mc_PrintNumStates | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | states | ||
| ) |
Function********************************************************************
Synopsis [Print the number of states]
Description [Print the number of states.]
SideEffects []
Definition at line 5472 of file mcUtil.c.
{
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
mdd_t *zeroMdd;
double size;
/*
* sometimes, this function will be constrained by number of minterm
* in the given set of states.
* num_minterm = mdd_num_of_mintern(states);
* if(num_minterm > MAX_MINTERM) {
* fprintf( stdout, "Too many minterms in given states\n" );
* return;
* }
*/
if((long)states % 2) {
states = (mdd_t *)((long)states - 1);
}
zeroMdd = mdd_zero( mddMgr );
states = mdd_dup(states);
if(mdd_equal(states, zeroMdd)) {
fprintf(stdout, "ZERO mdd\n");
mdd_free(zeroMdd);
mdd_free(states);
return;
}
size = mdd_count_onset(mddMgr, states, PSVars);
fprintf(stdout, "num states : %.0f\n", size);
mdd_free(zeroMdd);
mdd_free(states);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int Mc_PrintPath | ( | array_t * | aPath, |
| Fsm_Fsm_t * | modelFsm, | ||
| boolean | printInput | ||
| ) |
Function********************************************************************
Synopsis [Utility function - prints states on path, inputs for transitions]
SideEffects []
Definition at line 1778 of file mcUtil.c.
{
int check, forced, i;
int numForced;
mdd_t *inputSet=NIL(mdd_t);
mdd_t *uInput = NIL(mdd_t);
mdd_t *vInput = NIL(mdd_t);
array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );
array_t *inputVars = Fsm_FsmReadInputVars( modelFsm );
mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
forced = 0;
check = 1;
numForced = 0;
for( i = -1 ; i < (array_n( aPath )-1); i++ ) {
mdd_t *aState = ( i == -1 ) ? NIL(mdd_t) : array_fetch( mdd_t *, aPath, i );
mdd_t *bState = array_fetch( mdd_t *, aPath, (i+1) );
if((long)aState%2) {
aState = (mdd_t *)((long)aState -1);
forced++;
}
else forced = 0;
if((long)bState%2) {
bState = (mdd_t *)((long)bState -1);
}
if ( printInput == TRUE && i != -1) {
inputSet = Mc_FsmComputeDrivingInputMinterms( modelFsm, aState, bState );
vInput = Mc_ComputeACloseMinterm( inputSet, uInput, inputVars, mddMgr );
}
if(forced) {
fprintf(vis_stdout, "---- Forced %d\n", forced);
numForced ++;
}
McPrintTransition( aState, bState, uInput, vInput, psVars, inputVars,
printInput, modelFsm, (i+1) );
if ( uInput != NIL(mdd_t) ) {
mdd_free(uInput);
}
uInput = vInput;
if ( inputSet != NIL(mdd_t) ) {
mdd_free(inputSet);
}
}
if ( vInput != NIL(mdd_t) ) {
mdd_free(uInput);
}
if(Fsm_FsmReadFAFWFlag(modelFsm) > 0) {
fprintf(vis_stdout,
"# MC: the number of non-trivial forced segments %d\n",
numForced);
}
return 1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int Mc_PrintPathAiger | ( | array_t * | aPath, |
| Fsm_Fsm_t * | modelFsm, | ||
| boolean | printInput | ||
| ) |
Function********************************************************************
Synopsis [Utility function - prints states on path, inputs for transitions]
SideEffects []
Definition at line 1856 of file mcUtil.c.
{
int check, forced, i;
int numForced;
mdd_t *inputSet=NIL(mdd_t);
mdd_t *uInput = NIL(mdd_t);
mdd_t *vInput = NIL(mdd_t);
array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );
array_t *inputVars = Fsm_FsmReadInputVars( modelFsm );
forced = 0;
check = 1;
numForced = 0;
Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm );
FILE *psO = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0);
for(i=0; i<array_n(psVars); i++)
{
int mddId = array_fetch( int, psVars, i );
Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
char *nodeName = Ntk_NodeReadName( node );
if((nodeName[0] == '$') && (nodeName[1] == '_'))
{
fprintf(psO, "%s\n", &nodeName[2]);
}
}
fclose(psO);
for( i = -1 ; i < (array_n( aPath )-1); i++ ) {
mdd_t *aState = ( i == -1 ) ? NIL(mdd_t) : array_fetch( mdd_t *, aPath, i );
mdd_t *bState = array_fetch( mdd_t *, aPath, (i+1) );
if((long)aState%2) {
aState = (mdd_t *)((long)aState -1);
forced++;
}
else forced = 0;
if((long)bState%2) {
bState = (mdd_t *)((long)bState -1);
}
if(forced) {
fprintf(vis_stdout, "---- Forced %d\n", forced);
numForced ++;
}
/* The following fix is only for Sat-competition 2007 and will need to be fixed for future */
if(i == (array_n(aPath)-2))
{
McPrintTransitionAiger( aState, bState, uInput, vInput, psVars, inputVars,
printInput, modelFsm, 1 );
}
else
{
McPrintTransitionAiger( aState, bState, uInput, vInput, psVars, inputVars,
printInput, modelFsm, 0 );
}
if ( uInput != NIL(mdd_t) ) {
mdd_free(uInput);
}
uInput = vInput;
if ( inputSet != NIL(mdd_t) ) {
mdd_free(inputSet);
}
}
if ( vInput != NIL(mdd_t) ) {
mdd_free(uInput);
}
if(Fsm_FsmReadFAFWFlag(modelFsm) > 0) {
fprintf(vis_stdout,
"# MC: the number of non-trivial forced segments %d\n",
numForced);
}
return 1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Mc_PrintRings | ( | Fsm_Fsm_t * | modelFsm, |
| array_t * | onionRings | ||
| ) |
Function********************************************************************
Synopsis [Print the states of each ring]
Description [Print the states of each ring]
SideEffects []
Definition at line 5517 of file mcUtil.c.
{
int j;
mdd_t *innerRing;
if(array_n(onionRings) > 0) {
for(j=0; j<array_n(onionRings); j++) {
innerRing = array_fetch(mdd_t *, onionRings, j);
fprintf(vis_stdout, "%d'th ring : ", j);
if(innerRing)
Mc_PrintStates(modelFsm, innerRing);
else
fprintf(vis_stdout, "\n");
}
}
}
Here is the call graph for this function:
| void Mc_PrintStates | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | states | ||
| ) |
Function********************************************************************
Synopsis [Print states in terms of state variables]
Description [Print states in terms of state variables]
SideEffects []
Definition at line 5405 of file mcUtil.c.
{
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
Ntk_Network_t *aNetwork = Fsm_FsmReadNetwork( modelFsm );
mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
mdd_t *zeroMdd, *new_states;
char *tmpString;
double size;
/*
* sometimes, this function will be constrained by number of minterm
* in the given set of states.
* num_minterm = mdd_num_of_mintern(states);
* if(num_minterm > MAX_MINTERM) {
* fprintf( stdout, "Too many minterms in given states\n" );
* return;
* }
*/
if((long)states % 2) {
states = (mdd_t *)((long)states - 1);
}
zeroMdd = mdd_zero( mddMgr );
states = mdd_dup(states);
if(mdd_equal(states, zeroMdd)) {
fprintf(stdout, "ZERO mdd\n");
mdd_free(zeroMdd);
return;
}
size = mdd_count_onset(mddMgr, states, PSVars);
if(size > 40.0) {
fprintf(stdout, "Too many minterms in given states %.0f\n", size);
return;
}
fprintf( stdout, " " );
while(1) {
mdd_t *result = Mc_ComputeAMinterm( states, PSVars, mddMgr );
new_states = mdd_and( states, result, 1, 0 );
mdd_free( states );
states = new_states;
tmpString = Mc_MintermToString( result, PSVars, aNetwork );
fprintf( stdout, "%s ", tmpString );
FREE(tmpString);
mdd_free( result );
if(mdd_equal(states, zeroMdd)) {
mdd_free(zeroMdd);
mdd_free(states);
break;
}
}
fprintf(stdout, "\n");
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Mc_GuidedSearch_t Mc_ReadGuidedSearchType | ( | void | ) |
Function********************************************************************
Synopsis [Read and parse the hints_type set flag]
Description [Read and parse the hints_type set flag. If it is not set return the default: local. Return Mc_None_c if there is an error.]
SideEffects []
Definition at line 5313 of file mcUtil.c.
{
char *string = Cmd_FlagReadByName("guided_search_hint_type");
if(string == NIL(char)) /* default */
return Mc_Local_c;
if(!strcmp(string, "global"))
return Mc_Global_c;
if(!strcmp(string, "local"))
return Mc_Local_c;
else
return Mc_None_c;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Mc_ReadHints | ( | FILE * | guideFP | ) |
Function********************************************************************
Synopsis [Return an array of formulae representing the hints]
Description [Read the guide file and store the hint formulae in an array. Adds the 1 hint to the end of the array.
Returns NIL if something goes wrong: parse error in the file or temporal operators in the hints]
SideEffects []
Definition at line 4989 of file mcUtil.c.
{
Ctlp_FormulaArray_t *invarArray; /* formulae representing hints */
int i; /* to iterate over formulae */
Ctlp_Formula_t *formula; /* idem */
if (guideFP == NIL(FILE)){
fprintf(vis_stderr,
"** mc error: can't read hint file.\n");
return NIL(array_t);
}
invarArray = Ctlp_FileParseFormulaArray( guideFP );
if (invarArray == NIL(array_t)){
fprintf(vis_stderr,
"** mc error: parse error in hints file.\n");
return NIL(array_t);
}
if (array_n(invarArray) == 0){
fprintf(vis_stdout, "** mc error: File contained no hints.\n");
Ctlp_FormulaArrayFree(invarArray);
return NIL(array_t);
}
array_insert_last(Ctlp_Formula_t *, invarArray,
Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(void), NIL(void)));
/* some checks */
arrayForEachItem(Ctlp_Formula_t *, invarArray, i, formula){
if(!Ctlp_FormulaTestIsQuantifierFree(formula)){
(void) fprintf(vis_stdout,
"** mc error: Hints contain temporal operators\n");
Ctlp_FormulaArrayFree(invarArray);
return NIL(array_t);
} /* quantifier free */
}/* checks */
return invarArray;
}/* Mc_ReadHints */
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* Mc_ReadSystemVariablesFAFW | ( | Fsm_Fsm_t * | fsm, |
| FILE * | systemFP | ||
| ) |
Function********************************************************************
Synopsis [Return an array of variables controlled by system ]
Description [Read the system variables file and store the variables controlled by system in an array.
Returns NIL if something goes wrong: parse error in the file or variables that are not contained in model.]
SideEffects []
Definition at line 5049 of file mcUtil.c.
{
st_table *variablesTable;
array_t *bddIdArray;
char line[1024], nodeName[1024], *next;
int mddId, bddId;
int i, j, len, index;
int errorFlag;
Ntk_Node_t *node;
Ntk_Network_t *network;
mdd_manager *mgr;
errorFlag = 0;
if (systemFP == NIL(FILE)){
fprintf(vis_stderr,
"** mc error: can't read system file.\n");
return NIL(st_table);
}
network = Fsm_FsmReadNetwork(fsm);
mgr = Fsm_FsmReadMddManager(fsm);
variablesTable = st_init_table(st_numcmp, st_numhash);
while(fgets(line, 1024, systemFP)) {
len = strlen(line);
for(i=0; i<len; i++) {
if(line[i] == ' ') continue;
if(line[i] == '\t') continue;
break;
}
next = &(line[i]);
if(next[0] == '\n') continue;
if(next[0] == '#') continue;
len = strlen(next);
index = 0;
nodeName[0] = '\0';
for(i=0; i<len; i++) {
if(next[i] == ' ') break;
if(next[i] == '\t') break;
if(next[i] == '\n') break;
nodeName[index] = next[i];
index++;
}
nodeName[index] = '\0';
node = Ntk_NetworkFindNodeByName(network, nodeName);
if(node == NIL(Ntk_Node_t)) {
fprintf(vis_stderr, "Error : Can't find node '%s'\n", nodeName);
errorFlag = 1;
continue;
}
mddId = Ntk_NodeReadMddId(node);
bddIdArray = mdd_id_to_bdd_id_array(mgr, mddId);
for(j=0; j<array_n(bddIdArray); j++) {
bddId = array_fetch(int, bddIdArray, j);
st_insert(variablesTable, (char *)(long)bddId, (char *)(long)bddId);
}
array_free(bddIdArray);
}
if(variablesTable->num_entries == 0) {
st_free_table(variablesTable);
variablesTable = 0;
}
if(errorFlag) {
if(variablesTable)
st_free_table(variablesTable);
variablesTable = 0;
return((st_table *)-1);
}
return variablesTable;
}/* Mc_ReadSystemVariablesFAFW */
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* Mc_SetAllInputToSystem | ( | Fsm_Fsm_t * | fsm | ) |
Function********************************************************************
Synopsis []
Description []
SideEffects []
Definition at line 5134 of file mcUtil.c.
{
mdd_manager *mgr;
array_t *inputVars, *bddIdArray;
int i, j;
int mddId, bddId;
st_table *idTable;
idTable = st_init_table(st_numcmp, st_numhash);
mgr = Fsm_FsmReadMddManager(fsm);
/* inputVars = Fsm_FsmReadPrimaryInputVars(fsm); */
inputVars = Fsm_FsmReadInputVars(fsm);
if(inputVars) {
for(i=0; i<array_n(inputVars); i++) {
mddId = array_fetch(int, inputVars, i);
bddIdArray = mdd_id_to_bdd_id_array(mgr, mddId);
for(j=0; j<array_n(bddIdArray); j++) {
bddId = array_fetch(int, bddIdArray, j);
st_insert(idTable, (char *)(long)bddId, (char *)(long)bddId);
}
}
}
return(idTable);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int Mc_StringConvertToLockstepMode | ( | char * | string | ) |
Function********************************************************************
Synopsis [Converts a string to a lockstep mode.]
Description [Converts a string to a lockstep mode. If string does not refer to one of the allowed lockstep modes, it returns MC_LOCKSTEP_UNASSIGNED. The allowed values are: MC_LOCKSTEP_OFF, MC_LOCKSTEP_EARLY_TERMINATION, MC_LOCKSTEP_ALL_SCCS, and a positive integer n (lockstep enumerates up to n fair SCCs).]
SideEffects []
Definition at line 2278 of file mcUtil.c.
{
return McStringConvertToLockstepMode(string);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Mc_GSHScheduleType Mc_StringConvertToScheduleType | ( | char * | string | ) |
Function********************************************************************
Synopsis [Converts a string to a schedule type.]
Description [Converts a string to a schedule type. If string does not refer to one of the allowed schedule types, then returns McGSH_Unassigned_c.]
SideEffects []
Definition at line 2258 of file mcUtil.c.
{
return McStringConvertToScheduleType(string);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean McCheckEarlyTerminationForOverapprox | ( | Mc_EarlyTermination_t * | earlyTermination, |
| mdd_t * | overApprox, | ||
| array_t * | careStatesArray | ||
| ) |
Function********************************************************************
Synopsis [Check if an overapproximation of the evaluation guarantees that the early termination conditions hold.]
Description [Check if an overapproximation of the evaluation guarantees that the early termination conditions hold, modulo a care set modeled by an implicitly conjoined array of bdds.
If we are looking for ALL of ETstates, then we are done if we have overapprox is not a superset of ETstates, because the exact set will not hold all of ETstates.
If we are looking for SOME of ETstates, or we are given a set of CARE states, we are done if overapprox is disjoint from ETstates, because that means that the exact set is also disjoint from ETstates.
If earlyTermination == MC_NO_EARLY_TERMINATION, the result of the function is false.]
SideEffects []
Definition at line 4954 of file mcUtil.c.
{
if(earlyTermination == MC_NO_EARLY_TERMINATION)
return FALSE;
/* For an overapproximation and McAll_c (McSome_c), you check
whether some state (all states) are already missing */
return(((earlyTermination->mode == McAll_c) &&
(!mdd_lequal_mod_care_set_array(earlyTermination->states,
overApprox, 1, 1, careStatesArray)))
||
((earlyTermination->mode != McAll_c) &&
(mdd_lequal_mod_care_set_array(earlyTermination->states,
overApprox, 1, 0,
careStatesArray))));
}
Here is the caller graph for this function:
| boolean McCheckEarlyTerminationForUnderapprox | ( | Mc_EarlyTermination_t * | earlyTermination, |
| mdd_t * | underApprox, | ||
| array_t * | careStatesArray | ||
| ) |
Function********************************************************************
Synopsis [Check if an underapproximation of the evaluation guarantees that the early termination conditions hold.]
Description [Check if an underapproximation of the evaluation guarantees that the early termination conditions hold , modulo a care set modeled by an implicitly conjoined array of bdds.
If we are looking for ALL of ETstates, or we are are given a set of CARE states, then we are done if ETstates underapprox, because that implies ETstates exactset.
If we are looking for SOME of ETstates, we are done if underapprox and ETstates overlap, because that means that the exact set and ETstates also overlap.
If earlyTermination == MC_NO_EARLY_TERMINATION, the result of the function is false.]
SideEffects []
Definition at line 4907 of file mcUtil.c.
{
if(earlyTermination == MC_NO_EARLY_TERMINATION)
return FALSE;
/* for an underapproximation and McAll_c (McSome_c), you just check
whether all states (some states) are already reached */
return(((earlyTermination->mode != McSome_c) &&
(mdd_lequal_mod_care_set_array(earlyTermination->states, underApprox,
1, 1, careStatesArray)))
||
(
(earlyTermination->mode == McSome_c) &&
(!mdd_lequal_mod_care_set_array(underApprox,
earlyTermination->states, 1,
0, careStatesArray))));
}
Here is the caller graph for this function:
| int McCommandInitState | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) |
Function********************************************************************
Synopsis [Write resettability condition as a CTL formula]
CommandName [_init_state_formula]
CommandSynopsis [write resettability condition as a CTL formula]
CommandArguments [ \[-h\] \[<init_file>\] ]
CommandDescription [Write resettability condition as a CTL formula. Writes to init_file is specified, else stdout.]
SideEffects []
Definition at line 2606 of file mcUtil.c.
{
mdd_t *modelInitialStates;
mdd_t *anInitialState;
Fsm_Fsm_t *modelFsm;
char *formulaTxt;
array_t *stateVars;
FILE *ctlFile;
if ( argc == 1 ) {
ctlFile = vis_stdout;
}
else {
if ( !strcmp( "-h", argv[1] ) || ( argc > 2 ) ) {
fprintf( vis_stdout, "Usage: _init_state_formula [-h] init_file\n\tinit_file - file to write init state formula to (default is stdout)\n");
return 1;
}
ctlFile = Cmd_FileOpen( argv[1], "w", NIL(char *), 0 );
}
modelFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
if (modelFsm == NIL(Fsm_Fsm_t)) {
if ( argc != 1 ) {
fclose( ctlFile );
}
return 1;
}
stateVars = Fsm_FsmReadPresentStateVars( modelFsm );
modelInitialStates = Fsm_FsmComputeInitialStates( modelFsm );
if ( modelInitialStates == NIL(mdd_t) ) {
(void) fprintf( vis_stdout, "** mc error: - cant build init states (mutual latch dependancy?)\n%s\n",
error_string() );
if ( argc != 1 ) {
fclose( ctlFile );
}
return 1;
}
anInitialState = Mc_ComputeAState( modelInitialStates, modelFsm );
mdd_free(modelInitialStates);
formulaTxt = McStatePrintAsFormula( anInitialState, stateVars, modelFsm );
mdd_free(anInitialState);
fprintf( ctlFile, "AG EF %s;\n", formulaTxt );
FREE(formulaTxt);
if ( argc != 1 ) {
fclose(ctlFile);
}
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* McCompletePathBwd | ( | mdd_t * | aState, |
| mdd_t * | bState, | ||
| mdd_t * | invariantStates, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Make a path from aState to bState using bwd reachability.]
Description [Make a path from aState to bState which only passes through invariantStates; it is assumed that aState and bState lie in invariantStates. Returns a sequence of states starting from aState, leading to bState. If aState == bState, a non trivial path is returned (ie a cycle). If no path exists, return NIL. It is the users responsibility to free the returned array as well as its members. This function starts from bState and does backward reachability till it hits aState or a fixed point.]
SideEffects []
Definition at line 2487 of file mcUtil.c.
{
mdd_t *tmp1Mdd;
array_t *result;
mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
mdd_t *zeroMdd = mdd_zero( mddMgr );
array_t *onionRings = array_alloc( mdd_t *, 0 );
Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
mdd_t *c0, *c1;
assert( mdd_lequal( aState, invariantStates, 1, 1 ) );
assert( mdd_lequal( bState, invariantStates, 1, 1 ) );
if ( mdd_equal( aState, bState ) ) {
/*
* Alter the starting point to force routine to produce cycle if exists
* Question: would it be quicker to do simultaneous backward/forward
* analysis?
*/
c0 = mdd_dup( bState );
array_insert_last( mdd_t *, onionRings, c0 );
tmp1Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, bState,
bState, careSetArray);
c1 = mdd_and( tmp1Mdd, invariantStates, 1, 1 );
mdd_free(tmp1Mdd);
array_insert_last( mdd_t *, onionRings, c1 );
}
else {
c0 = zeroMdd;
c1 = mdd_dup( bState );
array_insert_last( mdd_t *, onionRings, c1 );
}
while (!mdd_equal_mod_care_set_array(c0, c1, careSetArray)) {
mdd_t *tmp2Mdd;
if ( McStateTestMembership( aState, c1 ) ) {
break;
}
/*
* performance gain from using dc's in this fp computation.
* use only when dclevel >= max
*/
if ( dcLevel >= McDcLevelRchFrontier_c ) {
mdd_t *annulusMdd = mdd_and( c0, c1, 0, 1 );
mdd_t *discMdd = mdd_dup( c1 );
mdd_t *dcMdd = bdd_between( annulusMdd, discMdd );
tmp2Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
annulusMdd, discMdd, careSetArray);
if ( verbosity > McVerbosityNone_c ) {
fprintf(vis_stdout,
"--Bwd completion: |low| = %d\t|upper| = %d\t|between|=%d\n",
mdd_size(annulusMdd), mdd_size(discMdd), mdd_size(dcMdd));
}
mdd_free( annulusMdd );
mdd_free( discMdd );
mdd_free( dcMdd );
}
else {
tmp2Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, c1, c1,
careSetArray);
}
tmp1Mdd = mdd_and( tmp2Mdd, invariantStates, 1, 1);
mdd_free(tmp2Mdd);
c0 = c1;
c1 = mdd_or( c1, tmp1Mdd, 1, 1 );
mdd_free( tmp1Mdd );
array_insert_last( mdd_t *, onionRings, c1 );
}
if ( McStateTestMembership( aState, c1 ) ) {
result = Mc_BuildPathToCore(aState, onionRings, modelFsm, McGreaterZero_c);
}
else {
result = NIL(array_t);
}
mdd_free( zeroMdd );
mdd_array_free( onionRings);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* McCompletePathFwd | ( | mdd_t * | aState, |
| mdd_t * | bState, | ||
| mdd_t * | invariantStates, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel | ||
| ) |
Function********************************************************************
Synopsis [Make a path from aState to bState using fwd reachability.]
Description [Make a path from aState to bState which only passes through invariantStates; it is assumed that aState and bState lie in invariantStates. Returns a sequence of states starting from aState, leading to bState. If aState == bState, a non trivial path is returned (ie a cycle). If no path exists, return NIL. It is the users responsibility to free the returned array as well as its members. This function starts from aState and does forward reachability till it hits bState or a fixed point.]
SideEffects []
Definition at line 2369 of file mcUtil.c.
{
mdd_t *tmp1Mdd;
array_t *result;
mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
mdd_t *zeroMdd = mdd_zero( mddMgr );
array_t *onionRings = array_alloc( mdd_t *, 0 );
Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
mdd_t *c0, *c1;
assert( mdd_lequal( aState, invariantStates, 1, 1 ) );
assert( mdd_lequal( bState, invariantStates, 1, 1 ) );
if ( mdd_equal( aState, bState ) ) {
/*
* Alter the starting point to force routine to produce cycle if exists
* Question: would it be quicker to do simultaneous backward/forward
* analysis?
*/
c0 = mdd_dup( aState );
array_insert_last( mdd_t *, onionRings, c0 );
tmp1Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
aState, aState, careSetArray);
c1 = mdd_and( tmp1Mdd, invariantStates, 1, 1 );
mdd_free(tmp1Mdd);
array_insert_last( mdd_t *, onionRings, c1 );
}
else {
c0 = zeroMdd;
c1 = mdd_dup( aState );
array_insert_last( mdd_t *, onionRings, c1 );
}
while (!mdd_equal_mod_care_set_array(c0, c1, careSetArray)) {
mdd_t *tmp2Mdd;
if ( McStateTestMembership( bState, c1 ) ) {
break;
}
/*
* performance gain from using dc's in this fp computation.
* use only when dclevel >= max
*/
if ( dcLevel >= McDcLevelRchFrontier_c ) {
mdd_t *annulusMdd = mdd_and( c0, c1, 0, 1 );
mdd_t *discMdd = mdd_dup( c1 );
mdd_t *dcMdd = bdd_between( annulusMdd, discMdd );
tmp2Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
annulusMdd, discMdd, careSetArray);
if ( verbosity > McVerbosityNone_c ) {
fprintf(vis_stdout,
"--Fwd completion: |low| = %d\t|upper| = %d\t|between|=%d\n",
mdd_size(annulusMdd), mdd_size(discMdd), mdd_size(dcMdd));
}
mdd_free( annulusMdd );
mdd_free( discMdd );
mdd_free( dcMdd );
}
else {
tmp2Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, c1, c1,
careSetArray);
}
tmp1Mdd = mdd_and( tmp2Mdd, invariantStates, 1, 1);
mdd_free(tmp2Mdd);
c0 = c1;
c1 = mdd_or( c1, tmp1Mdd, 1, 1 );
mdd_free( tmp1Mdd );
array_insert_last( mdd_t *, onionRings, c1 );
}
if ( McStateTestMembership( bState, c1 ) ) {
result = Mc_BuildPathFromCore(bState, onionRings, modelFsm,
McGreaterZero_c );
}
else {
result = NIL(array_t);
}
mdd_free( zeroMdd );
mdd_array_free( onionRings);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McComputeACloseMinterm | ( | mdd_t * | aSet, |
| mdd_t * | target, | ||
| array_t * | Support, | ||
| mdd_manager * | mddMgr | ||
| ) |
Function********************************************************************
Synopsis [Pick a minterm from the given set close to target. Support is an array of mddids representing the total support; that is, all the variables on which aSet may depend.]
SideEffects []
Definition at line 5576 of file mcUtil.c.
{
if (bdd_get_package_name() == CUDD) {
mdd_t *range; /* range of Support */
mdd_t *legalSet; /* aSet without the don't cares */
mdd_t *closeCube;
int dist;
array_t *bddSupport; /* Support in terms of bdd vars */
mdd_t *minterm; /* a random minterm */
/* Check that support of set is contained in Support. */
assert(SetCheckSupport(aSet, Support, mddMgr));
assert(!mdd_is_tautology(aSet, 0));
range = mdd_range_mdd(mddMgr, Support);
legalSet = bdd_and(aSet, range, 1, 1);
mdd_free(range);
closeCube = mdd_closest_cube(legalSet, target, &dist);
bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support);
minterm = bdd_pick_one_minterm(closeCube, bddSupport);
assert(MintermCheckWellFormed(minterm, Support, mddMgr));
assert(mdd_count_onset(mddMgr, minterm, Support) == 1);
assert(mdd_lequal(minterm,legalSet,1,1));
mdd_array_free(bddSupport);
mdd_free(legalSet);
mdd_free(closeCube);
return minterm;
} else {
return Mc_ComputeAMinterm(aSet, Support, mddMgr);
}/* if CUDD */
} /* McComputeACloseMinterm */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McComputeACloseState | ( | mdd_t * | states, |
| mdd_t * | target, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Select a state from the given set]
SideEffects []
Definition at line 5623 of file mcUtil.c.
{
array_t *PSVars = Fsm_FsmReadPresentStateVars(modelFsm);
mdd_manager *mddMgr = Ntk_NetworkReadMddManager(
Fsm_FsmReadNetwork(modelFsm));
mdd_t *result;
if (mdd_is_tautology(target, 0)) {
result = Mc_ComputeAMinterm(states, PSVars, mddMgr);
} else {
result = McComputeACloseMinterm(states, target, PSVars, mddMgr);
}
return result;
} /* McComputeACloseState */
Here is the call graph for this function:
Here is the caller graph for this function:
| int McComputeOnionRingsWithClosestCore | ( | mdd_t * | aState, |
| array_t * | arrayOfOnionRings, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Search the given array of "Onion Rings" for the Onion Rings with the clore closest to specified state.]
Description [Search the given array of "Onion Rings" for the Onion Rings with the core closest to specified state. By "Onion Rings" we refer to an array of sets of states (so arrayOfOnionRings is an array of arrays of states). The first member of a set of onion rings is referred to as the "core". The "Onion Rings" array has the property that the first set is all states that can reach the core (this may be mod a care set like the reached states). The succesive sets are those which can reach the core in successively fewer iterations.
We find the i with the smallest index j for which arrayOfOnionRings[i][j] contains aState.]
SideEffects []
Definition at line 2754 of file mcUtil.c.
{
int index;
int distance = 0;
while( TRUE ) {
for( index = 0 ; index < array_n( arrayOfOnionRings ) ; index++ ) {
array_t *iOnionRings = array_fetch( array_t *, arrayOfOnionRings, index );
/* will crash if run out of rings -> if not in there */
mdd_t *stateSet = array_fetch( mdd_t *, iOnionRings, distance );
if ( McStateTestMembership( aState, stateSet ) )
return index;
}
distance++;
}
assert(0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Fsm_Fsm_t* McConstructReducedFsm | ( | Ntk_Network_t * | network, |
| array_t * | ctlFormulaArray | ||
| ) |
Function********************************************************************
Synopsis [Form an FSM reduced with respect to the specified formula]
Description [Form an FSM reduced with respect to the CTL formula array. All latches and inputs which affect the given formula AND the fairness conditions of the system are included in this reduced fsm.]
SideEffects []
Definition at line 4609 of file mcUtil.c.
{
int i;
Ntk_Node_t *node;
array_t *nodeArray;
st_table *formulaNodes;
Ctlp_Formula_t *fairnessCondition;
Ctlp_Formula_t *ctlFormula;
array_t *formulaCombNodes;
Fsm_Fsm_t *netFsm = Fsm_NetworkReadFsm( network );
Fsm_Fsm_t *reducedFsm;
Fsm_Fairness_t *netFairness = Fsm_FsmReadFairnessConstraint( netFsm );
array_t *reducedFsmFairness = array_alloc( Ctlp_Formula_t *, 0 );
if (netFairness) {
if ( !Fsm_FairnessTestIsBuchi( netFairness ) ) {
(void) fprintf(vis_stderr, "** mc error: non Buchi fairness constraints not supported\n");
(void) fprintf(vis_stderr, "** mc error: ignoring fairness constraints\n");
}
else {
int j;
int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct( netFairness, 0 );
for( j = 0 ; j < numBuchi; j++ ) {
Ctlp_Formula_t *tmpFormula = Fsm_FairnessReadFinallyInfFormula( netFairness, 0, j );
Ctlp_Formula_t *reducedFsmCondition = Ctlp_FormulaDup( tmpFormula );
array_insert_last( Ctlp_Formula_t *, reducedFsmFairness, reducedFsmCondition );
}
}
}
formulaNodes = st_init_table( st_ptrcmp, st_ptrhash );
arrayForEachItem( Ctlp_Formula_t *, ctlFormulaArray, i, ctlFormula ) {
NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
}
arrayForEachItem( Ctlp_Formula_t *, reducedFsmFairness, i, fairnessCondition ) {
NodeTableAddCtlFormulaNodes( network, fairnessCondition, formulaNodes );
}
{
st_generator *stGen;
nodeArray = array_alloc( Ntk_Node_t *, 0 );
st_foreach_item( formulaNodes, stGen, &node, NIL(char *) ) {
array_insert_last( Ntk_Node_t *, nodeArray, node );
}
}
st_free_table( formulaNodes );
formulaCombNodes = Ntk_NodeComputeCombinationalSupport( network, nodeArray, FALSE );
array_free( nodeArray );
if(array_n(formulaCombNodes) == 0) {
/* Free the fairness constraint array (if any) */
for (i=0; i<array_n(reducedFsmFairness); i++){
Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t*,
reducedFsmFairness, i);
Ctlp_FormulaFree(formula);
}
array_free(reducedFsmFairness);
/* Free the formulaCombNodes */
array_free(formulaCombNodes);
/* We should return a NIL fsm */
return NIL(Fsm_Fsm_t);
}
{
graph_t *dupPart;
graph_t *origPart = Part_NetworkReadPartition( network );
array_t *reducedFsmLatches = array_alloc( Ntk_Node_t *, 0 );
array_t *reducedFsmInputs = array_alloc( Ntk_Node_t *, 0 );
int i;
arrayForEachItem( Ntk_Node_t *, formulaCombNodes, i, node ) {
if ( Ntk_NodeTestIsInput( node ) == TRUE ) {
array_insert_last( Ntk_Node_t *, reducedFsmInputs, node );
}
else {
assert( Ntk_NodeTestIsLatch( node ) == TRUE );
array_insert_last( Ntk_Node_t *, reducedFsmLatches, node );
}
}
if ((array_n(reducedFsmInputs) ==
Ntk_NetworkReadNumInputs(network)) &&
(array_n(reducedFsmLatches) ==
Ntk_NetworkReadNumLatches(network))){
/* We did not observe any reduction. Return a NIL fsm. */
/* After freeing appropriate stuff */
/* Free the fairness constraint array (if any) */
for (i=0; i<array_n(reducedFsmFairness); i++){
Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t*,
reducedFsmFairness, i);
Ctlp_FormulaFree(formula);
}
array_free(reducedFsmFairness);
array_free(formulaCombNodes);
array_free(reducedFsmLatches);
array_free(reducedFsmInputs);
return NIL(Fsm_Fsm_t);
}
dupPart = Part_PartitionDuplicate( origPart );
array_free( formulaCombNodes );
reducedFsm = Fsm_FsmCreateReducedFsm( network, dupPart, reducedFsmLatches,
reducedFsmInputs, reducedFsmFairness );
array_free( reducedFsmLatches );
array_free( reducedFsmInputs );
array_free( reducedFsmFairness );
}
return reducedFsm;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* McConvertMintermToValueArray | ( | mdd_t * | aMinterm, |
| array_t * | aSupport, | ||
| mdd_manager * | mddMgr | ||
| ) |
Function********************************************************************
Synopsis [Convert a minterm to an array of integers]
SideEffects []
Definition at line 2823 of file mcUtil.c.
{
array_t *resultValueArray;
/* this will be performed only in v0s-g executables */
assert( MintermCheckWellFormed( aMinterm, aSupport, mddMgr ));
resultValueArray = array_alloc( int, 0 );
{
int i;
for( i = 0 ; i < array_n( aSupport ); i++ ) {
int aSupportVar = array_fetch( int, aSupport, i );
int j;
for( j = 0 ; TRUE ; j++) {
mdd_t *faceMdd, *tmpMdd;
array_t *tmpArray = array_alloc( int, 0 );
array_insert_last( int, tmpArray, j );
faceMdd = mdd_literal( mddMgr, aSupportVar, tmpArray );
array_free( tmpArray );
tmpMdd = mdd_and( faceMdd, aMinterm, 1, 1 );
mdd_free( faceMdd );
if ( !mdd_is_tautology( tmpMdd, 0 ) ) {
mdd_free( tmpMdd );
array_insert_last( int, resultValueArray, j );
break;
}
mdd_free( tmpMdd );
}
}
}
return resultValueArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* McCreateJoinedPath | ( | array_t * | aPath, |
| array_t * | bPath | ||
| ) |
Function********************************************************************
Synopsis [Utility function - joins two paths.]
Description [Utility function - joins two paths. Note that the joins is done by adding the elements of the second array starting from the first element onwards.]
SeeAlso [McCreateMergedPath]
SideEffects []
Definition at line 3360 of file mcUtil.c.
{
int i;
mdd_t *tmpState;
array_t *aPathDup = McMddArrayDuplicateFAFW( aPath );
array_t *bPathDup = McMddArrayDuplicateFAFW( bPath );
for( i = 0 ; i < array_n( bPathDup ) ; i++ ) {
tmpState = array_fetch( mdd_t *, bPathDup, i );
array_insert_last( mdd_t *, aPathDup, tmpState );
}
array_free( bPathDup );
return aPathDup;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* McCreateMergedPath | ( | array_t * | aPath, |
| array_t * | bPath | ||
| ) |
Function********************************************************************
Synopsis [Utility function - merges two paths.]
Description [Utility function - merges two paths. Note that the merge is done by adding the elements of the second array starting from the second element onwards. This is because we often have to merge paths where the end point of the first is the starting point of the second.]
SideEffects []
Definition at line 3223 of file mcUtil.c.
{
int i, pos, forced;
mdd_t *tmpState, *endOfAPath;
array_t *aPathDup = McMddArrayDuplicateFAFW( aPath );
array_t *bPathDup = McMddArrayDuplicateFAFW( bPath );
for( i = 1 ; i < array_n( bPathDup ) ; i++ ) {
tmpState = array_fetch( mdd_t *, bPathDup, i );
array_insert_last( mdd_t *, aPathDup, tmpState );
}
pos = array_n(aPathDup) - array_n(bPathDup);
endOfAPath = array_fetch(mdd_t *, aPathDup, pos);
tmpState = array_fetch( mdd_t *, bPathDup, 0 );
forced = 0;
if((long)tmpState % 2) {
forced = 1;
tmpState = (mdd_t *)((long)tmpState - 1);
}
if(forced && mdd_equal(tmpState, endOfAPath)) {
array_insert(mdd_t *, aPathDup, pos, (mdd_t *)((long)endOfAPath + forced) );
}
mdd_free( tmpState );
array_free( bPathDup );
return aPathDup;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McGetSuccessorInTarget | ( | mdd_t * | aState, |
| mdd_t * | targetStates, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Obtain a successor of aState which is in targetStates]
SideEffects []
Definition at line 3428 of file mcUtil.c.
{
mdd_t *tmpMdd, *succsInTarget, *result;
array_t *careSetArray = array_alloc(mdd_t *, 0);
Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
array_insert_last(mdd_t *, careSetArray, targetStates);
tmpMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, aState,
aState, careSetArray);
array_free(careSetArray);
succsInTarget = mdd_and(tmpMdd, targetStates, 1, 1);
#if 1
result = Mc_ComputeAState(succsInTarget, modelFsm);
#else
result = Mc_ComputeACloseState(succsInTarget, aState, modelFsm);
#endif
mdd_free( tmpMdd );
mdd_free( succsInTarget );
return result;
}
Here is the call graph for this function:
| mdd_t* McGetSuccessorInTargetAmongFairStates | ( | mdd_t * | aState, |
| mdd_t * | targetStates, | ||
| array_t * | arrayOfOnionRings, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Obtain a successor of aState which is in targetStates]
SideEffects []
Definition at line 3462 of file mcUtil.c.
{
mdd_t *tmpMdd, *succsInTarget, *result;
mdd_t *fairStates, *newFairStates, *onionRing;
mdd_t *targetStatesInFairStates;
array_t *onionRings;
int i, j;
array_t *careSetArray = array_alloc(mdd_t *, 0);
Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
fairStates = 0;
for(i=0; i<array_n(arrayOfOnionRings); i++) {
onionRings = array_fetch(array_t *, arrayOfOnionRings, i);
for(j=0; j<array_n(onionRings); j++) {
onionRing = array_fetch(mdd_t *,onionRings, j);
if(fairStates) {
newFairStates = mdd_or(fairStates, onionRing, 1, 1);
mdd_free(fairStates);
fairStates = newFairStates;
}
else {
fairStates = mdd_dup(onionRing);
}
}
}
targetStatesInFairStates = mdd_and(fairStates, targetStates, 1, 1);
mdd_free(fairStates);
array_insert_last(mdd_t *, careSetArray, targetStatesInFairStates);
tmpMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, aState,
aState, careSetArray);
succsInTarget = mdd_and(tmpMdd, targetStatesInFairStates, 1, 1);
mdd_array_free(careSetArray);
result = Mc_ComputeACloseState(succsInTarget, aState, modelFsm);
mdd_free( tmpMdd );
mdd_free( succsInTarget );
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* McMddArrayAnd | ( | array_t * | mddArray | ) |
Function********************************************************************
Synopsis [Utility function - compute the intersection of the elements.]
Description [Utility function - compute the intersection of the elements.]
SideEffects []
Definition at line 3299 of file mcUtil.c.
{
mdd_t *result, *mdd1, *mdd2 = NIL(mdd_t);
int i;
result = NIL(mdd_t);
arrayForEachItem(mdd_t *, mddArray, i, mdd1) {
if (result == NIL(mdd_t))
result = mdd_dup(mdd1);
else {
mdd2 = result;
result = mdd_and(result, mdd1, 1, 1);
mdd_free(mdd2);
}
}
return (result);
}
Here is the caller graph for this function:
| array_t* McMddArrayDuplicateFAFW | ( | array_t * | mddArray | ) |
Function********************************************************************
Synopsis [Utility function - duplicate bdd array.]
Description [To represent the forced segment, the mdd_t is complemented. Therefore one cannot use mdd_array_duplicate. This is function for FateAndFreeWill counterexample generation.]
SideEffects []
Definition at line 3267 of file mcUtil.c.
{
int i, forced;
mdd_t *newTempMdd;
int length = array_n(mddArray);
array_t *result = array_alloc(mdd_t *, length);
for (i = 0; i < length; i++) {
mdd_t *tempMdd = array_fetch(mdd_t *, mddArray, i);
forced = 0;
if((long)tempMdd % 2) {
forced = 1;
tempMdd = (mdd_t *)((long)tempMdd - 1);
}
newTempMdd = mdd_dup(tempMdd);
array_insert(mdd_t *, result, i, (mdd_t *)((long)newTempMdd + forced));
}
return (result);
}
Here is the caller graph for this function:
| mdd_t* McMddArrayOr | ( | array_t * | mddArray | ) |
Function********************************************************************
Synopsis [Utility function - compute the union of the elements.]
Description [Utility function - compute the union of the elements.]
SideEffects []
Definition at line 3328 of file mcUtil.c.
{
mdd_t *result, *mdd1, *mdd2 = NIL(mdd_t);
int i;
result = NIL(mdd_t);
arrayForEachItem(mdd_t *, mddArray, i, mdd1) {
if (result == NIL(mdd_t))
result = mdd_dup(mdd1);
else {
mdd2 = result;
result = mdd_or(result, mdd1, 1, 1);
mdd_free(mdd2);
}
}
return (result);
}
Here is the caller graph for this function:
| void McNormalizeBddPointer | ( | array_t * | bddArray | ) |
Function********************************************************************
Synopsis [Free a Path Struct]
SideEffects []
Definition at line 3595 of file mcUtil.c.
{
int i;
bdd_t *p;
for(i=0; i<array_n(bddArray); i++) {
p = array_fetch(bdd_t *, bddArray, i);
if((long)p%2) p = (mdd_t *)( (long)p -1 );
array_insert(bdd_t *, bddArray, i, p);
}
}
Here is the caller graph for this function:
| Mc_EarlyTermination_t* McObtainUpdatedEarlyTerminationCondition | ( | Mc_EarlyTermination_t * | earlyTermination, |
| mdd_t * | careStates, | ||
| Ctlp_FormulaType | formulaType | ||
| ) |
Function********************************************************************
Synopsis [Update the early termination condition.]
Description [Update the early termination condition.
MC_NO_EARLY_TERMINATION is equivalent to mode=CARE and states=mdd_one. careStates=NIL is equivalent to either careStates=mdd_zero (for disjunction) or careStates=mdd_one (in the other cases). With these provisions, the propagation algorithm can be summarized thus.
For negation, ALL becomes SOME and vice versa, while CARE is passed unchanged.
For conjunction, disjunction, and implication: if the current node has a termination condition of type ALL or SOME, this is refined and propagated. Otherwise, the returned early termination condition is of type CARE. The care states are the conjunction of earlyTermination->states and either careStates (for conjunction and implication) or the complement of careStates (for disjunction).
In some cases, one can immediately determine that the goal cannot be reached, or has already been reached. In these cases, the termination condition has mode=CARE and states=mdd_zero.
The other types of formulae produce no early termination condition for their children. That is, they declare that all states are care states.]
SideEffects []
Definition at line 4756 of file mcUtil.c.
{
Mc_EarlyTermination_t *result;
switch (formulaType) {
case Ctlp_NOT_c:
if (earlyTermination == MC_NO_EARLY_TERMINATION)
return MC_NO_EARLY_TERMINATION;
result = Mc_EarlyTerminationAlloc(earlyTermination->mode,
earlyTermination->states);
switch (result->mode) {
case McAll_c:
result->mode = McSome_c;
break;
case McSome_c:
result->mode = McAll_c;
break;
case McCare_c:
break;
default:
assert(0);
}
break;
case Ctlp_AND_c:
if (careStates == NIL(mdd_t)) {
if (earlyTermination == MC_NO_EARLY_TERMINATION) {
result = MC_NO_EARLY_TERMINATION;
} else if (earlyTermination->mode == McAll_c) {
result = Mc_EarlyTerminationAlloc(McAll_c, earlyTermination->states);
} else {
/* Here mode is CARE or SOME: inherit care states from parent. */
result = Mc_EarlyTerminationAlloc(McCare_c, earlyTermination->states);
}
} else {
/* There are care states from sibling. */
if (earlyTermination == MC_NO_EARLY_TERMINATION) {
/* No early termination from parent: just use sibling's care states. */
result = Mc_EarlyTerminationAlloc(McCare_c, careStates);
} else if (earlyTermination->mode == McAll_c) {
/* If some goal states are not in care set, we know we cannot achieve
* the goal; otherwise, we just propagate the parent's condition.
*/
if (mdd_lequal(earlyTermination->states, careStates, 1, 1)) {
result = Mc_EarlyTerminationAlloc(McAll_c, earlyTermination->states);
} else {
result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* failure */
}
} else if (earlyTermination->mode == McSome_c) {
/* If no goal states are in the care set, we have failed; otherwise
* we refine the goal set to those states also in the care set.
*/
if (mdd_lequal(earlyTermination->states, careStates, 1, 0)) {
result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* failure */
} else {
mdd_t *andMdd = mdd_and(earlyTermination->states, careStates, 1, 1);
result = Mc_EarlyTerminationAlloc(McSome_c, andMdd);
mdd_free(andMdd);
}
} else { /* if (earlyTermination->mode == McCare_c) */
/* Intersect care states from parent and sibling. */
mdd_t *andMdd = mdd_and(earlyTermination->states, careStates, 1, 1);
result = Mc_EarlyTerminationAlloc(McCare_c, andMdd);
mdd_free(andMdd);
}
}
break;
case Ctlp_THEN_c:
case Ctlp_OR_c:
if (careStates == NIL(mdd_t)) {
if (earlyTermination == MC_NO_EARLY_TERMINATION) {
result = MC_NO_EARLY_TERMINATION;
} else if (earlyTermination->mode == McSome_c) {
if (formulaType == Ctlp_OR_c) {
result = Mc_EarlyTerminationAlloc(McSome_c,
earlyTermination->states);
} else {
result = Mc_EarlyTerminationAlloc(McAll_c,
earlyTermination->states);
}
} else {
/* Here mode is CARE or ALL: inherit care states from parent. */
result = Mc_EarlyTerminationAlloc(McCare_c, earlyTermination->states);
}
} else {
/* There are care states from sibling.
* Since f->g is !f+g, we treat the THEN and OR cases together by
* complementing the care set in the latter case. */
mdd_t *mask = (formulaType == Ctlp_OR_c) ?
bdd_not(careStates) : bdd_dup(careStates);
if (earlyTermination == MC_NO_EARLY_TERMINATION) {
/* No early termination from parent: just use sibling's care states. */
result = Mc_EarlyTerminationAlloc(McCare_c, mask);
} else if (earlyTermination->mode == McAll_c) {
/* Remove the goal states already attained from the goal set. */
mdd_t *andMdd = mdd_and(earlyTermination->states, mask, 1, 1);
result = Mc_EarlyTerminationAlloc(McAll_c, andMdd);
mdd_free(andMdd);
} else if (earlyTermination->mode == McSome_c) {
/* If some goal states were already attained, declare success;
* otherwise just propagate the parent's condition.
*/
if (mdd_lequal(earlyTermination->states, mask, 1, 1)) {
result = Mc_EarlyTerminationAlloc(McSome_c,
earlyTermination->states);
} else {
result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* success */
}
} else { /* if (earlyTermination->mode == McCare_c) */
/* Intersect care states from parent and sibling. */
mdd_t *andMdd = mdd_and(earlyTermination->states, mask, 1, 1);
result = Mc_EarlyTerminationAlloc(McCare_c, andMdd);
mdd_free(andMdd);
}
mdd_free(mask);
}
break;
default:
result = MC_NO_EARLY_TERMINATION;
}
return result;
} /* McObtainUpdatedEarlyTerminationCondition */
Here is the call graph for this function:
Here is the caller graph for this function:
| McOptions_t* McOptionsAlloc | ( | void | ) |
Function********************************************************************
Synopsis [Allocate an McOptions_t struct.]
SideEffects []
Definition at line 3632 of file mcUtil.c.
{
McOptions_t *result = ALLOC(McOptions_t, 1);
memset(result, 0, sizeof(McOptions_t));
result->useMore = FALSE;
result->reduceFsm = FALSE;
result->printInputs = FALSE;
result->useFormulaTree = FALSE;
result->simFormat = FALSE;
result->ctlFile = NIL(FILE);
result->guideFile = NIL(FILE);
result->debugFile = NIL(FILE);
result->fwdBwd = McFwd_c;
result->dcLevel = McDcLevelNone_c;
result->dbgLevel = McDbgLevelMin_c;
result->schedule = McGSH_EL_c;
result->lockstep = MC_LOCKSTEP_OFF;
result->verbosityLevel = McVerbosityNone_c;
result->timeOutPeriod = 0;
result->ardcOptions = NIL(Fsm_ArdcOptions_t);
result->invarApproxFlag = Fsm_Rch_Default_c;
result->invarOnionRingsFlag = FALSE;
result->traversalDirection = McBwd_c;
result->doCoverageHoskote = FALSE;
result->doCoverageImproved = FALSE;
result->incre = TRUE;
return result;
}
Here is the caller graph for this function:
| void McOptionsFree | ( | McOptions_t * | options | ) |
Function********************************************************************
Synopsis [Free an McOptions_t struct.]
SideEffects []
Definition at line 3673 of file mcUtil.c.
{
if (options->debugFile != NIL(FILE)){
fclose(options->debugFile);
}
if (options->ardcOptions != NIL(Fsm_ArdcOptions_t)){
FREE(options->ardcOptions);
}
FREE(options);
}
Here is the caller graph for this function:
| Fsm_ArdcOptions_t* McOptionsReadArdcOptions | ( | McOptions_t * | options | ) |
| int McOptionsReadBeerMethod | ( | McOptions_t * | options | ) |
| int McOptionsReadCoverageHoskote | ( | McOptions_t * | options | ) |
| int McOptionsReadCoverageImproved | ( | McOptions_t * | options | ) |
| FILE* McOptionsReadCtlFile | ( | McOptions_t * | options | ) |
| McDbgLevel McOptionsReadDbgLevel | ( | McOptions_t * | options | ) |
| Mc_DcLevel McOptionsReadDcLevel | ( | McOptions_t * | options | ) |
| FILE* McOptionsReadDebugFile | ( | McOptions_t * | options | ) |
| Mc_FwdBwdAnalysis McOptionsReadFwdBwd | ( | McOptions_t * | options | ) |
| FILE* McOptionsReadGuideFile | ( | McOptions_t * | options | ) |
| Fsm_RchType_t McOptionsReadInvarApproxFlag | ( | McOptions_t * | options | ) |
| boolean McOptionsReadInvarOnionRingsFlag | ( | McOptions_t * | options | ) |
| Mc_LeMethod_t McOptionsReadLeMethod | ( | McOptions_t * | options | ) |
| int McOptionsReadLockstep | ( | McOptions_t * | options | ) |
| int McOptionsReadPrintInputs | ( | McOptions_t * | options | ) |
| int McOptionsReadReduceFsm | ( | McOptions_t * | options | ) |
| Mc_GSHScheduleType McOptionsReadSchedule | ( | McOptions_t * | options | ) |
| int McOptionsReadSimValue | ( | McOptions_t * | options | ) |
| FILE* McOptionsReadSystemFile | ( | McOptions_t * | options | ) |
| int McOptionsReadTimeOutPeriod | ( | McOptions_t * | options | ) |
| Mc_FwdBwdAnalysis McOptionsReadTraversalDirection | ( | McOptions_t * | options | ) |
| boolean McOptionsReadUseFormulaTree | ( | McOptions_t * | options | ) |
| int McOptionsReadUseMore | ( | McOptions_t * | options | ) |
| boolean McOptionsReadVacuityDetect | ( | McOptions_t * | options | ) |
| Mc_VerbosityLevel McOptionsReadVerbosityLevel | ( | McOptions_t * | options | ) |
| void McOptionsSetArdcOptions | ( | McOptions_t * | options, |
| Fsm_ArdcOptions_t * | ardcOptions | ||
| ) |
| void McOptionsSetBeerMethod | ( | McOptions_t * | options, |
| boolean | beer | ||
| ) |
| void McOptionsSetCoverageHoskote | ( | McOptions_t * | options, |
| boolean | doCoverageHoskote | ||
| ) |
| void McOptionsSetCoverageImproved | ( | McOptions_t * | options, |
| boolean | doCoverageImproved | ||
| ) |
| void McOptionsSetCtlFile | ( | McOptions_t * | options, |
| FILE * | file | ||
| ) |
| void McOptionsSetDbgLevel | ( | McOptions_t * | options, |
| McDbgLevel | dbgLevel | ||
| ) |
| void McOptionsSetDcLevel | ( | McOptions_t * | options, |
| Mc_DcLevel | dcLevel | ||
| ) |
| void McOptionsSetDebugFile | ( | McOptions_t * | options, |
| FILE * | file | ||
| ) |
| void McOptionsSetFAFWFlag | ( | McOptions_t * | options, |
| boolean | FAFWFlag | ||
| ) |
| void McOptionsSetFwdBwd | ( | McOptions_t * | options, |
| Mc_FwdBwdAnalysis | fwdBwd | ||
| ) |
| void McOptionsSetGuideFile | ( | McOptions_t * | options, |
| FILE * | guideFile | ||
| ) |
| void McOptionsSetInvarApproxFlag | ( | McOptions_t * | options, |
| Fsm_RchType_t | approxFlag | ||
| ) |
| void McOptionsSetInvarOnionRingsFlag | ( | McOptions_t * | options, |
| int | shellFlag | ||
| ) |
Function********************************************************************
Synopsis [Set a flag to store onion rings during invariant checking.]
SideEffects []
Definition at line 4330 of file mcUtil.c.
{
if (shellFlag) options->invarOnionRingsFlag = TRUE;
else options->invarOnionRingsFlag = FALSE;
}
Here is the caller graph for this function:
| void McOptionsSetLeMethod | ( | McOptions_t * | options, |
| Mc_LeMethod_t | leMethod | ||
| ) |
| void McOptionsSetLockstep | ( | McOptions_t * | options, |
| int | lockstep | ||
| ) |
| void McOptionsSetPrintInputs | ( | McOptions_t * | options, |
| boolean | printInputs | ||
| ) |
| void McOptionsSetReduceFsm | ( | McOptions_t * | options, |
| boolean | reduceFsm | ||
| ) |
| void McOptionsSetSchedule | ( | McOptions_t * | options, |
| Mc_GSHScheduleType | schedule | ||
| ) |
| void McOptionsSetSimValue | ( | McOptions_t * | options, |
| boolean | simValue | ||
| ) |
| void McOptionsSetTimeOutPeriod | ( | McOptions_t * | options, |
| int | timeOutPeriod | ||
| ) |
| void McOptionsSetTraversalDirection | ( | McOptions_t * | options, |
| Mc_FwdBwdAnalysis | fwdBwd | ||
| ) |
| void McOptionsSetUseFormulaTree | ( | McOptions_t * | options, |
| boolean | useFormulaTree | ||
| ) |
| void McOptionsSetUseMore | ( | McOptions_t * | options, |
| boolean | useMore | ||
| ) |
| void McOptionsSetVacuityDetect | ( | McOptions_t * | options, |
| boolean | vd | ||
| ) |
| void McOptionsSetVariablesForSystem | ( | McOptions_t * | options, |
| FILE * | systemFile | ||
| ) |
| void McOptionsSetVerbosityLevel | ( | McOptions_t * | options, |
| Mc_VerbosityLevel | verbosityLevel | ||
| ) |
| McPath_t* McPathAlloc | ( | void | ) |
Function********************************************************************
Synopsis [Allocate a Path Struct]
SideEffects []
Definition at line 3577 of file mcUtil.c.
{
McPath_t *tmpPath = ( McPath_t * ) malloc( sizeof( McPath_t ) );
tmpPath->stemArray = NIL(array_t);
tmpPath->cycleArray = NIL(array_t);
return tmpPath;
}
Here is the caller graph for this function:
| void McPathFree | ( | McPath_t * | aPath | ) |
Definition at line 3608 of file mcUtil.c.
{
if ( aPath->stemArray ) {
McNormalizeBddPointer(aPath->stemArray);
mdd_array_free( aPath->stemArray );
}
if ( aPath->cycleArray ) {
McNormalizeBddPointer(aPath->cycleArray);
mdd_array_free( aPath->cycleArray );
}
FREE( aPath );
}
Here is the call graph for this function:
Here is the caller graph for this function:
| McPath_t* McPathNormalize | ( | McPath_t * | aPath | ) |
Function********************************************************************
Synopsis [Utility function - convert McPath_t to normal form.]
Description [Utility function - convert McPath_t to normal form. A normal McPath_t is one where the stem leads to a state, which then returns it self in the cycle.]
SideEffects []
Definition at line 3145 of file mcUtil.c.
{
int i, j;
int forced;
array_t *stemArray = McPathReadStemArray( aPath );
array_t *cycleArray = McPathReadCycleArray( aPath );
McPath_t *result = McPathAlloc();
array_t *newStem = array_alloc( mdd_t *, 0 );
array_t *newCycle = array_alloc( mdd_t *, 0 );
mdd_t *lastState = GET_NORMAL_PT(array_fetch_last(mdd_t *, cycleArray));
McPathSetStemArray( result, newStem );
McPathSetCycleArray( result, newCycle );
for( i = 0 ; i < array_n( stemArray ) ; i++ ) {
mdd_t *tmpState = array_fetch( mdd_t *, stemArray, i );
forced = 0;
if((long)tmpState % 2) {
forced = 1;
tmpState = (mdd_t *)((long)tmpState - 1);
}
array_insert_last(mdd_t *, newStem,
(mdd_t *)((long)(mdd_dup(tmpState)) + forced) );
if ( mdd_equal( lastState, tmpState ) ) {
break;
}
}
for( j = i; j < array_n( stemArray ); j++ ) {
mdd_t *tmpState = array_fetch( mdd_t *, stemArray, j );
forced = 0;
if((long)tmpState % 2) {
forced = 1;
tmpState = (mdd_t *)((long)tmpState - 1);
}
array_insert_last(mdd_t *, newCycle,
(mdd_t *)((long)(mdd_dup(tmpState)) + forced) );
}
/* first state of cycle array == last state of stem array => start from j=1 */
for( j = 1; j < array_n( cycleArray ); j++ ) {
mdd_t *tmpState = array_fetch( mdd_t *, cycleArray, j );
forced = 0;
if((long)tmpState % 2) {
forced = 1;
tmpState = (mdd_t *)((long)tmpState - 1);
}
array_insert_last(mdd_t *, newCycle,
(mdd_t *)((long)(mdd_dup(tmpState)) + forced) );
}
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* McPathReadCycleArray | ( | McPath_t * | aPath | ) |
| array_t* McPathReadStemArray | ( | McPath_t * | aPath | ) |
| void McPathSetCycleArray | ( | McPath_t * | aPath, |
| array_t * | cycleArray | ||
| ) |
| void McPathSetStemArray | ( | McPath_t * | aPath, |
| array_t * | stemArray | ||
| ) |
| int McPrintSimPath | ( | FILE * | outputFile, |
| array_t * | aPath, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Print path as sim trace]
SideEffects []
Definition at line 4518 of file mcUtil.c.
{
int i;
array_t *inputVars = Fsm_FsmReadInputVars( modelFsm );
array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );
Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm );
mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
array_t *inputSortedVars = SortMddIds( inputVars, network );
array_t *psSortedVars = SortMddIds( psVars, network );
fprintf(outputFile, "# UC Berkeley, VIS Release 1.3\n");
fprintf(outputFile, "# Network: %s\n", Ntk_NetworkReadName( network ) );
fprintf(outputFile, "# Simulation vectors have been generated to show language non-empty\n\n");
fprintf( outputFile, ".inputs " );
PrintNodes( inputSortedVars, network );
fprintf( outputFile, "\n" );
fprintf( outputFile, ".latches " );
PrintNodes( psSortedVars, network );
fprintf( outputFile, "\n" );
fprintf( outputFile, ".outputs\n" );
for( i = -1 ; i < (array_n( aPath ) - 1); i++ ) {
if ( i == -1 ) {
mdd_t *initState = array_fetch( mdd_t *, aPath, (i+1) );
array_t *initValues = McConvertMintermToValueArray( initState, psSortedVars, mddMgr );
fprintf( outputFile, ".initial ");
PrintDeck( initValues, psSortedVars, network );
array_free( initValues );
fprintf( outputFile, "\n" );
fprintf( outputFile, ".start_vectors\n");
}
else {
array_t *psValues;
array_t *nsValues;
array_t *inputValues;
mdd_t *psState = array_fetch( mdd_t *, aPath, i );
mdd_t *nsState = array_fetch( mdd_t *, aPath, (i+1) );
mdd_t *inputSet = Mc_FsmComputeDrivingInputMinterms( modelFsm, psState, nsState );
mdd_t *input = Mc_ComputeAMinterm( inputSet, inputVars, mddMgr );
inputValues = McConvertMintermToValueArray( input, inputSortedVars, mddMgr );
PrintDeck( inputValues, inputSortedVars, network );
array_free( inputValues );
fprintf( outputFile, " ;");
psValues = McConvertMintermToValueArray( psState, psSortedVars, mddMgr );
PrintDeck( psValues, psSortedVars, network );
array_free( psValues );
fprintf( outputFile, " ;");
nsValues = McConvertMintermToValueArray( nsState, psSortedVars, mddMgr );
PrintDeck( nsValues, psSortedVars, network );
array_free( nsValues );
fprintf( outputFile, " ;\n");
mdd_free( inputSet );
mdd_free( input );
}
}
array_free( psSortedVars );
array_free( inputSortedVars );
return 1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void McPrintSupport | ( | mdd_t * | aMdd, |
| mdd_manager * | mddMgr, | ||
| Ntk_Network_t * | aNetwork | ||
| ) |
Function********************************************************************
Synopsis [Print Support of Function]
SideEffects []
Definition at line 4466 of file mcUtil.c.
{
int i;
char *tmp1String, *tmp2String;
char *mintermString = NIL(char);
char bodyString[McMaxStringLength_c];
array_t *aSupport = mdd_get_support( mddMgr, aMdd );
array_t *stringArray = array_alloc( char *, 0 );
for ( i = 0 ; i < array_n( aSupport ); i++ ) {
int mddId = array_fetch( int, aSupport, i );
Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
char *nodeName = Ntk_NodeReadName( node );
sprintf( bodyString, "%s", nodeName );
tmp1String = util_strsav( bodyString );
array_insert_last( char *, stringArray, tmp1String );
}
array_sort( stringArray, cmp);
for ( i = 0 ; i < array_n( stringArray ); i++ ) {
tmp1String = array_fetch( char *, stringArray, i );
if( i == 0 ) {
mintermString = util_strcat3(tmp1String, "", "" );
}
else {
tmp2String = util_strcat3(mintermString, "\n", tmp1String );
FREE(mintermString);
mintermString = tmp2String;
}
FREE(tmp1String);
}
fprintf(vis_stdout, "%s\n", mintermString );
}
Here is the call graph for this function:
| void McPrintTransition | ( | mdd_t * | aState, |
| mdd_t * | bState, | ||
| mdd_t * | uInput, | ||
| mdd_t * | vInput, | ||
| array_t * | stateSupport, | ||
| array_t * | inputSupport, | ||
| boolean | printInputs, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| int | seqNumber | ||
| ) |
Function********************************************************************
Synopsis [Print a transition to vis_stdout.]
Description [Print a transition to vis_stdout. The transition is supposed to be from aState to bState on input vInput. If uInput is not NIL, instead of printing vInput, we only print the places where it differs from uInput. If there is no difference anywhere, we print "-Unchanged-". Similarly, we print only the incremental difference from aState to bState; if there is none, we print "-Unchanged-". If aState is NIL we simply print bState and return.]
SideEffects []
Definition at line 2963 of file mcUtil.c.
{
Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm );
char *aString = aState ? Mc_MintermToString( aState, stateSupport, modelNetwork ) : NIL(char);
char *bString = Mc_MintermToString( bState, stateSupport, modelNetwork );
char *tmp1String = aString;
char *tmp2String = bString;
char *ptr1;
char *ptr2;
st_table *node2MvfAigTable;
node2MvfAigTable =
(st_table *)Ntk_NetworkReadApplInfo(modelNetwork, MVFAIG_NETWORK_APPL_KEY);
if ( aState == NIL(mdd_t) ) {
fprintf( vis_stdout, "--State %d:\n%s\n", seqNumber, bString );
FREE(bString);
return;
}
fprintf(vis_stdout, "--Goes to state %d:\n", seqNumber );
{
boolean unchanged=TRUE;
while ( (tmp1String != NIL(char)) && ((ptr1 = strchr( tmp1String, '\n' ) ) != NIL(char) ) ) {
ptr2 = strchr( tmp2String, '\n' );
*ptr1 = 0;
*ptr2 = 0;
if ( (strcmp( tmp1String, tmp2String ) ) ) {
fprintf( vis_stdout, "%s\n", tmp2String );
unchanged = FALSE;
}
tmp1String = & (ptr1[1]);
tmp2String = & (ptr2[1]);
}
if (unchanged == TRUE) {
fprintf( vis_stdout, "<Unchanged>\n");
}
}
if ( printInputs == TRUE ) {
/* first test that there are inputs */
if ( array_n( inputSupport ) > 0 ) {
fprintf(vis_stdout, "--On input:\n");
if ( uInput == NIL(mdd_t) ) {
char *vString = Mc_MintermToString( vInput, inputSupport, modelNetwork );
fprintf(vis_stdout, "%s", vString );
FREE(vString);
}
else {
boolean unchanged=TRUE;
char *uString = Mc_MintermToString( uInput, inputSupport, modelNetwork );
char *vString = Mc_MintermToString( vInput, inputSupport, modelNetwork );
tmp1String = uString;
tmp2String = vString;
while ( (tmp1String != NIL(char)) && ((ptr1 = strchr( tmp1String, '\n' ) ) != NIL(char) ) ) {
ptr2 = strchr( tmp2String, '\n' );
*ptr1 = 0;
*ptr2 = 0;
if ( (strcmp( tmp1String, tmp2String ) ) ) {
fprintf( vis_stdout, "%s\n", tmp2String );
unchanged = FALSE;
}
tmp1String = & (ptr1[1]);
tmp2String = & (ptr2[1]);
}
if (unchanged == TRUE) {
fprintf( vis_stdout, "<Unchanged>\n");
}
FREE(uString);
FREE(vString);
}
}
}
FREE( aString );
FREE( bString );
fprintf (vis_stdout, "\n");
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void McPrintTransitionAiger | ( | mdd_t * | aState, |
| mdd_t * | bState, | ||
| mdd_t * | uInput, | ||
| mdd_t * | vInput, | ||
| array_t * | stateSupport, | ||
| array_t * | inputSupport, | ||
| boolean | printInputs, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| int | seqNumber | ||
| ) |
Function********************************************************************
Synopsis [Print a transition to vis_stdout.]
Description [Print a transition to vis_stdout. The transition is supposed to be from aState to bState on input vInput. If uInput is not NIL, instead of printing vInput, we only print the places where it differs from uInput. If there is no difference anywhere, we print "-Unchanged-". Similarly, we print only the incremental difference from aState to bState; if there is none, we print "-Unchanged-". If aState is NIL we simply print bState and return.]
SideEffects []
Definition at line 2882 of file mcUtil.c.
{
Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm );
char *aString = aState ? Mc_MintermToStringAiger( aState, stateSupport, modelNetwork ) : NIL(char);
char *bString = Mc_MintermToStringAiger( bState, stateSupport, modelNetwork );
char *inpString = aState ? Mc_MintermToStringAigerInput( aState, stateSupport, modelNetwork ) : NIL(char);
st_table *node2MvfAigTable;
node2MvfAigTable =
(st_table *)Ntk_NetworkReadApplInfo(modelNetwork, MVFAIG_NETWORK_APPL_KEY);
if ( aState == NIL(mdd_t) ) {
FREE(bString);
return;
}
fprintf(vis_stdout, "%s", aString);
fprintf(vis_stdout, "%s", inpString);
/* first test that there are inputs */
/* if ( array_n( inputSupport ) > 0 ) {
if ( uInput == NIL(mdd_t) ) {
char *vString = Mc_MintermToStringAiger( vInput, inputSupport, modelNetwork );
FREE(vString);
}
else {
boolean unchanged=TRUE;
char *uString = Mc_MintermToStringAiger( uInput, inputSupport, modelNetwork );
char *vString = Mc_MintermToStringAiger( vInput, inputSupport, modelNetwork );
FREE(uString);
FREE(vString);
}
} */
if(seqNumber == 1)
{
fprintf(vis_stdout, "1 ");
}
else
{
fprintf(vis_stdout, "0 ");
}
fprintf(vis_stdout, "%s", bString);
FREE( aString );
FREE( bString );
fprintf (vis_stdout, "\n");
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean McQueryContinue | ( | char * | query | ) |
Function********************************************************************
Synopsis [Query user to continue.]
SideEffects []
Definition at line 4439 of file mcUtil.c.
{
char result[2];
fprintf(vis_stdout, "%s", query);
if (fgets(result, 2, stdin) == NULL) return FALSE;
if(!strcmp(result,"1"))
return TRUE;
else if(!strcmp(result,"0"))
return FALSE;
else {
fprintf(vis_stdout, "-- Must enter 0/1\n");
return McQueryContinue(query);
}
}
Here is the caller graph for this function:
| array_t* McRemoveIndexedOnionRings | ( | int | index, |
| array_t * | arrayOfOnionRings | ||
| ) |
Function********************************************************************
Synopsis [Remove array indexed by index from array of arrays.]
Description [Remove array indexed by index from array of arrays. Does NOT free the input arrayOfOnionRings.]
SideEffects []
Definition at line 2790 of file mcUtil.c.
{
int i;
array_t *dupArrayOfOnionRings = array_alloc( array_t *, 0 );
array_t *OnionRings;
for ( i = 0 ; i < array_n( arrayOfOnionRings ) ; i++ ) {
if ( i == index ) {
continue;
}
OnionRings = array_fetch( array_t *, arrayOfOnionRings, i );
array_insert_last( array_t *, dupArrayOfOnionRings, OnionRings );
}
return dupArrayOfOnionRings;
}
Here is the caller graph for this function:
| void McStateFailsFormula | ( | mdd_t * | aState, |
| Ctlp_Formula_t * | formula, | ||
| McDbgLevel | debugLevel, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Print message saying given state fails formula.]
SideEffects []
Definition at line 3081 of file mcUtil.c.
{
McStatePassesOrFailsFormula( aState, formula, 0, debugLevel, modelFsm );
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void McStatePassesFormula | ( | mdd_t * | aState, |
| Ctlp_Formula_t * | formula, | ||
| McDbgLevel | debugLevel, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Print message saying given state passes formula.]
SideEffects []
Definition at line 3063 of file mcUtil.c.
{
McStatePassesOrFailsFormula( aState, formula, 1, debugLevel, modelFsm );
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void McStatePassesOrFailsFormula | ( | mdd_t * | aState, |
| Ctlp_Formula_t * | formula, | ||
| int | pass, | ||
| McDbgLevel | debugLevel, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Utility function - prints state passes or fails formula]
SideEffects []
Definition at line 3099 of file mcUtil.c.
{
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
char *formulaText = Ctlp_FormulaConvertToString( formula );
Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm );
/* Nodes created in converting formulae like AU may not have text
* attached to them. */
if (formulaText == NIL(char))
return;
fprintf( vis_stdout, "--State\n");
Mc_MintermPrint( aState, PSVars, modelNetwork );
if ( pass )
fprintf( vis_stdout, "passes ");
else
fprintf( vis_stdout, "fails ");
if( debugLevel > McDbgLevelMin_c)
fprintf(vis_stdout, "%s.\n\n", formulaText);
else
fprintf(vis_stdout, "\n\n");
FREE(formulaText);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| char* McStatePrintAsFormula | ( | mdd_t * | aMinterm, |
| array_t * | aSupport, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
Function********************************************************************
Synopsis [Return a CTL formula for a minterm.]
SideEffects []
Definition at line 2673 of file mcUtil.c.
{
int i;
char *tmp1String;
char *tmp2String;
char *tmp3String;
char bodyString[McMaxStringLength_c];
char *mintermString = NIL(char);
mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
Ntk_Network_t *aNetwork = Fsm_FsmReadNetwork( modelFsm );
array_t *valueArray = McConvertMintermToValueArray( aMinterm, aSupport, mddMgr );
array_t *stringArray = array_alloc( char *, 0 );
for ( i = 0 ; i < array_n( aSupport ); i++ ) {
int mddId = array_fetch( int, aSupport, i );
int value = array_fetch( int, valueArray, i );
Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
char *nodeName = Ntk_NodeReadName( node );
Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
char *symbolicValue = Var_VariableReadSymbolicValueFromIndex( nodeVar, value );
sprintf( bodyString, "%s=%s", nodeName, symbolicValue );
}
else {
sprintf( bodyString, "%s=%d", nodeName, value );
}
tmp1String = util_strsav( bodyString );
array_insert_last( char *, stringArray, tmp1String );
}
array_free(valueArray);
array_sort( stringArray, cmp);
for ( i = 0 ; i < array_n( stringArray ); i++ ) {
tmp1String = array_fetch( char *, stringArray, i );
if( i == 0 ) {
mintermString = util_strcat3("(", tmp1String, ")" );
}
else {
tmp2String = util_strcat3( mintermString, " * (", tmp1String );
FREE(mintermString);
tmp3String = util_strcat3( tmp2String, ")", "" );
FREE(tmp2String);
mintermString = tmp3String;
}
FREE(tmp1String);
}
array_free( stringArray );
tmp1String = util_strcat3( "( ", mintermString, " )" );
FREE(mintermString);
mintermString = tmp1String;
return mintermString;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean McStateSatisfiesFormula | ( | Ctlp_Formula_t * | aFormula, |
| mdd_t * | aState | ||
| ) |
Function********************************************************************
Synopsis [ Check to see if aState lies in set of states satisfying aFormula ]
SideEffects []
Definition at line 3387 of file mcUtil.c.
{
mdd_t *passStates = Ctlp_FormulaObtainLatestApprox( aFormula );
if ( mdd_lequal( aState, passStates, 1, 1 ) ) {
mdd_free( passStates );
return TRUE;
}
else {
mdd_free( passStates );
return FALSE;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean McStateTestMembership | ( | mdd_t * | aState, |
| mdd_t * | setOfStates | ||
| ) |
| int McStringConvertToLockstepMode | ( | char * | string | ) |
Function********************************************************************
Synopsis [Converts a string to a lockstep mode.]
Description [Converts a string to a lockstep mode. If string does not refer to one of the allowed lockstep modes, it returns MC_LOCKSTEP_UNASSIGNED. The allowed values are: MC_LOCKSTEP_OFF, MC_LOCKSTEP_EARLY_TERMINATION, MC_LOCKSTEP_ALL_SCCS, and a positive integer n (lockstep enumerates up to n fair SCCs).]
SideEffects []
Definition at line 5692 of file mcUtil.c.
{
int n;
if (strcmp("off", string) == 0) {
return MC_LOCKSTEP_OFF;
} else if (strcmp("on", string) == 0) {
return MC_LOCKSTEP_EARLY_TERMINATION;
} else if (strcmp("all", string) == 0) {
return MC_LOCKSTEP_ALL_SCCS;
} else if (Cmd_StringCheckIsInteger(string, &n) == 2) {
return n;
} else {
return MC_LOCKSTEP_UNASSIGNED;
}
} /* McStringConvertToLockstepMode */
Here is the call graph for this function:
Here is the caller graph for this function:
| Mc_GSHScheduleType McStringConvertToScheduleType | ( | char * | string | ) |
Function********************************************************************
Synopsis [Converts a string to a schedule type.]
Description [Converts a string to a schedule type. If string does not refer to one of the allowed schedule types, then returns McGSH_Unassigned_c.]
SideEffects []
Definition at line 5656 of file mcUtil.c.
{
if (strcmp("off", string) == 0) {
return McGSH_old_c;
} else if (strcmp("EL", string) == 0) {
return McGSH_EL_c;
} else if (strcmp("EL1", string) == 0) {
return McGSH_EL1_c;
} else if (strcmp("EL2", string) == 0) {
return McGSH_EL2_c;
} else if (strcmp("random", string) == 0) {
return McGSH_Random_c;
} else if (strcmp("budget", string) == 0) {
return McGSH_Budget_c;
} else {
return McGSH_Unassigned_c;
}
} /* McStringConvertToScheduleType */
Here is the caller graph for this function:
| static boolean MintermCheckWellFormed | ( | mdd_t * | aMinterm, |
| array_t * | aSupport, | ||
| mdd_manager * | mddMgr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Test that given mdd is a minterm.]
SideEffects []
Definition at line 5997 of file mcUtil.c.
{
/* first check its support */
if (!SetCheckSupport(aMinterm, aSupport, mddMgr)) {
return FALSE;
}
/* now check its a minterm */
{
float cardinality = mdd_count_onset( mddMgr, aMinterm, aSupport );
if ( cardinality != 1 ) {
fprintf( vis_stderr, "-- onset is not one\n");
return FALSE;
}
}
return TRUE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static Mvf_Function_t* NodeBuildPseudoInputMvf | ( | Ntk_Node_t * | node, |
| mdd_manager * | mddMgr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Builds MVF for a node that is a pseudo input.]
Description [Builds MVF for a node that is a pseudo input. This node has a single output and no inputs. Its table has several row entries. We build an MVF whose components correspond exactly to possible table outputs.]
SideEffects []
Comment [Although pseudo inputs, constants, and internal nodes all have tables, a single procedure cannot be used to build their MVF. A pseudo input MVF is built in terms of its mddId, whereas a constant or internal is not. A constant or pseudo input doesn't have any inputs, whereas an internal does.]
SeeAlso [Tbl_TableBuildMvfForNonDetConstant]
Definition at line 1967 of file mcUtil.c.
{
Mvf_Function_t *mvf;
int columnIndex = Ntk_NodeReadOutputIndex(node);
Tbl_Table_t *table = Ntk_NodeReadTable(node);
int mddId = Ntk_NodeReadMddId(node);
assert(mddId != NTK_UNASSIGNED_MDD_ID);
mvf = Tbl_TableBuildNonDetConstantMvf(table, columnIndex, mddId, mddMgr);
return mvf;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void NodeTableAddCtlFormulaNodes | ( | Ntk_Network_t * | network, |
| Ctlp_Formula_t * | formula, | ||
| st_table * | nodesTable | ||
| ) | [static] |
Function********************************************************************
Synopsis [Add nodes for wires referred to in formula to nodesTable.]
SideEffects []
Definition at line 5935 of file mcUtil.c.
{
if ( formula == NIL(Ctlp_Formula_t) ) {
return;
}
if ( Ctlp_FormulaReadType( formula ) == Ctlp_ID_c ) {
char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
if( node )
st_insert( nodesTable, ( char *) node, NIL(char) );
return;
}
NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadRightChild( formula ), nodesTable );
NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadLeftChild( formula ), nodesTable );
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void NodeTableAddLtlFormulaNodes | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | formula, | ||
| st_table * | nodesTable | ||
| ) | [static] |
Function********************************************************************
Synopsis [Add nodes for wires referred to in formula to nodesTable.]
SideEffects []
Definition at line 5966 of file mcUtil.c.
{
if ( formula == NIL(Ctlsp_Formula_t) ) {
return;
}
if ( Ctlsp_FormulaReadType( formula ) == Ctlsp_ID_c ) {
char *nodeNameString = Ctlsp_FormulaReadVariableName( formula );
Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
if( node )
st_insert( nodesTable, ( char *) node, NIL(char) );
return;
}
NodeTableAddLtlFormulaNodes( network, Ctlsp_FormulaReadRightChild( formula ), nodesTable );
NodeTableAddLtlFormulaNodes( network, Ctlsp_FormulaReadLeftChild( formula ), nodesTable );
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void PrintDeck | ( | array_t * | mddValues, |
| array_t * | mddIdArray, | ||
| Ntk_Network_t * | network | ||
| ) | [static] |
Function********************************************************************
Synopsis [Print an array of nodes]
SideEffects []
Definition at line 5790 of file mcUtil.c.
{
int i;
int mddId;
arrayForEachItem(int, mddIdArray, i, mddId) {
int value = array_fetch( int, mddValues, i );
Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
char *symbolicValue = Var_VariableReadSymbolicValueFromIndex( nodeVar, value );
fprintf( vis_stdout, "%s ", symbolicValue );
}
else {
fprintf( vis_stdout, "%d ", value );
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void PrintNodes | ( | array_t * | mddIdArray, |
| Ntk_Network_t * | network | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Print an array of nodes]
SideEffects []
Definition at line 5725 of file mcUtil.c.
{
int i;
int mddId;
arrayForEachItem(int , mddIdArray, i, mddId) {
Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
char *nodeName = Ntk_NodeReadName( node );
fprintf(vis_stdout, " %s ", nodeName );
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static boolean SetCheckSupport | ( | mdd_t * | aMinterm, |
| array_t * | aSupport, | ||
| mdd_manager * | mddMgr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Test that given mdd is a minterm.]
SideEffects []
Definition at line 6028 of file mcUtil.c.
{
if (!mdd_check_support(mddMgr, aMinterm, aSupport)) {
fprintf(vis_stderr,
"** mc error: support of minterm is not contained in claimed support\n");
return FALSE;
}
return TRUE;
}
Here is the caller graph for this function:
| static array_t * SortMddIds | ( | array_t * | mddIdArray, |
| Ntk_Network_t * | network | ||
| ) | [static] |
Function********************************************************************
Synopsis [Print an array of nodes]
SideEffects []
Definition at line 5749 of file mcUtil.c.
{
int i;
int mddId;
char *nodeName;
st_table *nameToIndex = st_init_table( strcmp, st_strhash );
array_t *nodeNameArray = array_alloc( char *, 0 );
array_t *result = array_alloc( int, 0 );
arrayForEachItem(int, mddIdArray, i, mddId) {
Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
nodeName = Ntk_NodeReadName( node );
st_insert( nameToIndex, nodeName, (char *) (long) i );
array_insert_last( char *, nodeNameArray, nodeName );
}
array_sort( nodeNameArray, cmp);
arrayForEachItem(char *, nodeNameArray, i, nodeName ) {
int index;
st_lookup_int( nameToIndex, nodeName, & index );
mddId = array_fetch( int, mddIdArray, index );
array_insert_last( int, result, mddId );
}
st_free_table( nameToIndex );
array_free( nodeNameArray );
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: mcUtil.c,v 1.113 2009/04/11 18:26:10 fabio Exp $" [static] |
CFile***********************************************************************
FileName [mcUtil.c]
PackageName [mc]
Synopsis [Utilities for Fair CTL model checker and debugger]
Author [Adnan Aziz, Tom Shiple, In-Ho Moon]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. 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.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
