#include "mcInt.h"
Include dependency graph for mcDbg.c:
Go to the source code of this file.
Functions | |
| static void | DebugID (McOptions_t *options, Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm) |
| static void | DebugTrueFalse (Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm) |
| static void | DebugBoolean (McOptions_t *options, Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray) |
| static McPath_t * | DebugEX (Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray) |
| static McPath_t * | DebugEU (Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray) |
| static McPath_t * | DebugEG (Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray, McOptions_t *options) |
| static void | FsmStateDebugConvertedFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray) |
| static void | FsmPathDebugFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray) |
| static void | FsmPathDebugEXFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray) |
| static void | FsmPathDebugEUFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray) |
| static void | FsmPathDebugEGFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray) |
| static void | FsmPathDebugEFFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray) |
| static void | FsmPathDebugAXFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray) |
| static void | FsmPathDebugAFFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray) |
| static void | FsmPathDebugAGFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray) |
| static void | FsmPathDebugAUFormula (McOptions_t *options, mdd_t *aState, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, array_t *careSetArray) |
| int | McFsmDebugFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, array_t *careSetArray) |
| void | McFsmStateDebugFormula (McOptions_t *options, Ctlp_Formula_t *ctlFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray) |
| McPath_t * | McBuildFairPath (mdd_t *startState, mdd_t *invariantStates, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, Mc_FwdBwdAnalysis fwdBwd) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mcDbg.c,v 1.43 2005/04/23 04:40:54 fabio Exp $" |
Function Documentation
| static void DebugBoolean | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | aFormula, | ||
| mdd_t * | aState, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a Boolean formula]
Desciption [Debug a Boolean formula. For Boolean formula built out of binary connective, we may debug only one branch, if say the formula is an AND and the left branch is fails.]
SideEffects []
Definition at line 512 of file mcDbg.c.
{
Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(aFormula);
Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( aFormula );
Ctlp_Formula_t *rFormula = Ctlp_FormulaReadRightChild( aFormula );
McDbgLevel debugLevel = McOptionsReadDbgLevel(options);
if (McStateSatisfiesFormula(aFormula, aState)) {
McStatePassesFormula(aState, originalFormula, debugLevel, modelFsm);
} else {
McStateFailsFormula(aState, originalFormula, debugLevel, modelFsm);
}
/* We always debug the first (left) child. */
McFsmStateDebugFormula(options, lFormula, aState, modelFsm, careSetArray);
/* What we do for the second child depends on the type of the formula.
* For Ctlp_AND_c, Ctlp_OR_c, Ctlp_THEN_c the right child may not be
* needed. With early termination, the right child may not have the
* information required to produce a counterexample; hence, its debugging
* is not optional. (We may get incorrect answers.)
*/
if (Ctlp_FormulaReadType(aFormula) == Ctlp_AND_c) {
/* If aFormula fails and aState does not satisfy lFormula
* 1. The information about aState at the right child is not
* necessarilty correct. (aState was a don't care state.)
* 2. A counterexample to lFormula is a counterexample to
* aFormula.
* So, if aFormula fails, we should debug the right child only if
* aState satisfies lFormula.
* If, on the other hand, aFormula passes, then aState must satisfy
* lFormula, and we need to witness both lFormula and rFormula.
*/
if (McStateSatisfiesFormula(lFormula, aState)) {
McFsmStateDebugFormula(options, rFormula, aState, modelFsm,
careSetArray);
}
} else if (Ctlp_FormulaReadType(aFormula) == Ctlp_OR_c) {
/* if aFormula passes, we should debug the right child only if
* aState does not satisfy lFormula.
* If, on the other hand, aFormula fails, then aState may not satisfy
* lFormula, and we need to produce counterexamples for both lFormula
* and rFormula.
*/
if (!McStateSatisfiesFormula(lFormula, aState)) {
McFsmStateDebugFormula(options, rFormula, aState, modelFsm,
careSetArray);
}
} else if (Ctlp_FormulaReadType(aFormula) == Ctlp_THEN_c) {
/* This case is like the OR, with the polarity of the left
* left child reversed.
*/
if (McStateSatisfiesFormula(lFormula, aState)) {
McFsmStateDebugFormula(options, rFormula, aState, modelFsm,
careSetArray);
}
} else if (Ctlp_FormulaReadType(aFormula) != Ctlp_NOT_c) {
/* For Ctlp_EQ_c and Ctlp_XOR_c both children must be debugged. */
McFsmStateDebugFormula(options, rFormula, aState, modelFsm, careSetArray);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static McPath_t * DebugEG | ( | Ctlp_Formula_t * | aFormula, |
| mdd_t * | aState, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray, | ||
| McOptions_t * | options | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a formula of type EG.]
Description [Debug a formula of type EG at specified state. It is assumed that state fails formula. Refer to Clarke et al DAC 1995 for details of the algorithm.]
SideEffects []
Definition at line 669 of file mcDbg.c.
{
array_t *arrayOfOnionRings = (array_t *) Ctlp_FormulaReadDebugData(aFormula);
mdd_t *invariantMdd = Ctlp_FormulaObtainLatestApprox( aFormula );
McPath_t *fairPath = McBuildFairPath(aState, invariantMdd, arrayOfOnionRings,
modelFsm, careSetArray,
McOptionsReadVerbosityLevel(options),
McOptionsReadDcLevel(options),
McOptionsReadFwdBwd(options));
mdd_free( invariantMdd );
return fairPath;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static McPath_t * DebugEU | ( | Ctlp_Formula_t * | aFormula, |
| mdd_t * | aState, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a formula of type EU.]
Description [Debug a formula of type EU at specified state. It is assumed that state fails formula.]
SideEffects []
Definition at line 640 of file mcDbg.c.
{
McPath_t *witnessPath = McPathAlloc();
array_t *OnionRings = (array_t *) Ctlp_FormulaReadDebugData( aFormula );
array_t *pathToCore = Mc_BuildPathToCore(aState, OnionRings,
modelFsm,
McGreaterOrEqualZero_c );
McPathSetStemArray( witnessPath, pathToCore );
return witnessPath;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static McPath_t * DebugEX | ( | Ctlp_Formula_t * | aFormula, |
| mdd_t * | aState, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a formula of type EX.]
Description [Debug a formula of type EX at specified state. It is assumed that aState satisfies the EX formula.]
SideEffects []
Definition at line 590 of file mcDbg.c.
{
mdd_t *aDupState = mdd_dup( aState );
mdd_t *aStateSuccs;
mdd_t *statesSatisfyingLeftFormula;
mdd_t *targetStates;
mdd_t *witnessSuccState;
Ctlp_Formula_t *lFormula;
McPath_t *witnessPath = McPathAlloc();
array_t *stemArray = array_alloc( mdd_t *, 0 );
Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
/*
* By using careSet here, can end up with unreachable successors
*/
aStateSuccs = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
aState, aState, careSetArray);
lFormula = Ctlp_FormulaReadLeftChild( aFormula );
statesSatisfyingLeftFormula = Ctlp_FormulaObtainLatestApprox( lFormula );
targetStates = mdd_and( aStateSuccs, statesSatisfyingLeftFormula, 1, 1 );
mdd_free( aStateSuccs ); mdd_free( statesSatisfyingLeftFormula );
witnessSuccState = Mc_ComputeACloseState( targetStates, aState, modelFsm );
mdd_free( targetStates );
array_insert_last( mdd_t *, stemArray, aDupState );
array_insert_last( mdd_t *, stemArray, witnessSuccState );
McPathSetStemArray( witnessPath, stemArray );
return witnessPath;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void DebugID | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | aFormula, | ||
| mdd_t * | aState, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Debug an Atomic Formula]
Description [Debug an Atomic Formula. As per the semantics of fair CTL, a state satisfies an Atomic Formula just in case the given wire computes the appropriate Boolean function on that state as input. The state has to be fair; however we do NOT justify the fairness by printing a path to a fair cycle. THe user can achieve this effect by adding ANDing in a formula EG TRUE.]
SideEffects []
Definition at line 466 of file mcDbg.c.
{
Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(aFormula);
McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
if ( McStateSatisfiesFormula( aFormula, aState ) ) {
McStatePassesFormula( aState, originalFormula, debugLevel, modelFsm );
}
else {
McStateFailsFormula( aState, originalFormula, debugLevel, modelFsm );
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void DebugTrueFalse | ( | Ctlp_Formula_t * | aFormula, |
| mdd_t * | aState, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a TRUE/FALSE formula]
SideEffects []
Definition at line 491 of file mcDbg.c.
{
fprintf(vis_stdout, "--Nothing to debug for %s\n",
((Ctlp_FormulaReadType(aFormula) == Ctlp_TRUE_c) ? "TRUE\n" : "FALSE\n"));
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FsmPathDebugAFFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| McPath_t * | counterExamplePath, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a AF formula]
SideEffects []
Definition at line 1267 of file mcDbg.c.
{
Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula );
Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
Ctlp_Formula_t *llFormula = Ctlp_FormulaReadLeftChild( lFormula );
Ctlp_Formula_t *lllFormula = Ctlp_FormulaReadLeftChild( llFormula );
Ctlp_Formula_t *lllOriginalFormula = Ctlp_FormulaReadOriginalFormula(
lllFormula);
char *lllOriginalFormulaText = Ctlp_FormulaConvertToString(
lllOriginalFormula);
mdd_t *firstState;
array_t *witnessArray;
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
array_t *stemArray = McPathReadStemArray( counterExamplePath );
array_t *cycleArray = McPathReadCycleArray( counterExamplePath );
char *firstStateName;
McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
boolean printInputs = McOptionsReadPrintInputs( options );
witnessArray = McCreateMergedPath( stemArray, cycleArray );
firstState = array_fetch( mdd_t *, witnessArray, 0 );
firstStateName = Mc_MintermToString(firstState, PSVars,
Fsm_FsmReadNetwork(modelFsm));
if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
fprintf(vis_stdout, "--State\n%sfails AF formula\n\n",
firstStateName);
else
fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName,
originalFormulaText );
FREE(firstStateName);
FREE(originalFormulaText);
switch ( debugLevel ) {
case McDbgLevelMin_c:
case McDbgLevelMinVerbose_c: {
McPath_t *normalPath = McPathNormalize( counterExamplePath );
array_t *stem = McPathReadStemArray( normalPath );
array_t *cycle = McPathReadCycleArray( normalPath );
if( debugLevel != McDbgLevelMin_c)
fprintf(vis_stdout, "--A fair path on which %s is always false:\n",
lllOriginalFormulaText );
fprintf(vis_stdout, " --Counter example begins\n");
(void) fprintf( vis_stdout, "--Fair path stem:\n");
Mc_PrintPath( stem, modelFsm, printInputs );
(void) fprintf( vis_stdout, "--Fair path cycle:\n");
Mc_PrintPath( cycle, modelFsm, printInputs );
fprintf(vis_stdout, "\n");
fprintf(vis_stdout, " --Counter example ends\n\n");
McPathFree( normalPath );
break;
}
case McDbgLevelMax_c:
case McDbgLevelInteractive_c: {
int i;
McPath_t *normalPath = McPathNormalize( counterExamplePath );
array_t *stem = McPathReadStemArray( normalPath );
array_t *cycle = McPathReadCycleArray( normalPath );
fprintf(vis_stdout, "--A fair path on which %s is always false:\n",
lllOriginalFormulaText );
fprintf(vis_stdout, " --Counter example begins\n");
(void) fprintf( vis_stdout, "--Fair path stem:\n");
Mc_PrintPath( stem, modelFsm, printInputs );
(void) fprintf( vis_stdout, "--Fair path cycle:\n");
Mc_PrintPath( cycle, modelFsm, printInputs );
fprintf(vis_stdout, "\n");
fprintf(vis_stdout, " --Counter example ends\n\n");
McPathFree( normalPath );
for( i=0 ; i < ( array_n( witnessArray )-1 ); i++ ) {
mdd_t *aState = array_fetch( mdd_t *, witnessArray, i );
if (debugLevel == McDbgLevelMax_c ||
(debugLevel == McDbgLevelInteractive_c &&
McQueryContinue(
"--Continue debugging AF formula? (1-yes,0-no)\n"))) {
McFsmStateDebugFormula(options, lllFormula, aState, modelFsm,
careSetArray);
}
}
break;
}
default: {
fail("Bad case in switch for debugging AF formula\n");
}
}
McNormalizeBddPointer(witnessArray);
mdd_array_free( witnessArray );
FREE(lllOriginalFormulaText);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FsmPathDebugAGFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| McPath_t * | counterExamplePath, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug an AG formula.]
Description [Debugs an AG formula. What it really wants is a formula of the form !EF! phi, that was converted from the formula AG phi, with all the converted pointers set as required: the top ! points to the original AG formula, and top node of phi points to the original phi.]
SideEffects []
Definition at line 1381 of file mcDbg.c.
{
Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula );
Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
Ctlp_Formula_t *lrFormula = Ctlp_FormulaReadRightChild( lFormula );
Ctlp_Formula_t *lrlFormula = Ctlp_FormulaReadLeftChild( lrFormula );
Ctlp_Formula_t *lrlOriginalFormula = Ctlp_FormulaReadOriginalFormula(
lrlFormula);
char *lrlOriginalFormulaText = Ctlp_FormulaConvertToString(
lrlOriginalFormula);
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
array_t *witnessArray = McPathReadStemArray( counterExamplePath );
mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
mdd_t *lastState = GET_NORMAL_PT(array_fetch_last( mdd_t *, witnessArray ));
char *firstStateName = Mc_MintermToString(firstState, PSVars,
Fsm_FsmReadNetwork(modelFsm));
McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
boolean printInputs = McOptionsReadPrintInputs( options );
assert( Ctlp_FormulaReadType(ctlFormula) == Ctlp_NOT_c );
assert( Ctlp_FormulaTestIsConverted(ctlFormula) );
assert( Ctlp_FormulaReadType(originalFormula) == Ctlp_AG_c );
assert( originalFormulaText != NIL(char) );
assert( Ctlp_FormulaReadType(lFormula) == Ctlp_EU_c );
assert( Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(lFormula)) ==
Ctlp_TRUE_c );
assert( Ctlp_FormulaReadType(lrFormula) == Ctlp_NOT_c );
assert( lrlOriginalFormula != NIL(Ctlp_Formula_t) );
if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
fprintf(vis_stdout, "--State\n%sfails AG formula\n\n",
firstStateName);
else
fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName,
originalFormulaText );
FREE(firstStateName);
FREE(originalFormulaText);
switch ( debugLevel ) {
case McDbgLevelMin_c:
case McDbgLevelMinVerbose_c:{
if ( array_n(witnessArray ) == 1 ) {
if( debugLevel != McDbgLevelMin_c)
fprintf(vis_stdout, "since %s is false at this state\n",
lrlOriginalFormulaText );
McFsmStateDebugFormula(options, lrlFormula, lastState, modelFsm,
careSetArray);
}
else {
if( debugLevel != McDbgLevelMin_c)
fprintf(vis_stdout,
"--Counter example is a path to a state where %s is false\n",
lrlOriginalFormulaText);
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath(witnessArray, modelFsm, printInputs);
fprintf(vis_stdout, " --Counter example ends\n\n");
McFsmStateDebugFormula(options, lrlFormula, lastState, modelFsm,
careSetArray);
}
break;
}
case McDbgLevelMax_c:
case McDbgLevelInteractive_c: {
if ( array_n(witnessArray ) == 1 ) {
if( debugLevel != McDbgLevelMin_c)
fprintf(vis_stdout, "since %s is false at this state\n",
lrlOriginalFormulaText );
McFsmStateDebugFormula(options, lrlFormula, lastState, modelFsm,
careSetArray);
}
else {
fprintf(vis_stdout,
"--Counter example is a path to a state where %s is false\n",
lrlOriginalFormulaText);
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath( witnessArray, modelFsm, printInputs);
fprintf(vis_stdout, " --Counter example ends\n\n");
if (debugLevel == McDbgLevelMax_c ||
(debugLevel == McDbgLevelInteractive_c &&
McQueryContinue(
"--Continue debugging AG formula? (1-yes,0-no)\n")))
{
McFsmStateDebugFormula(options, lrlFormula, lastState, modelFsm,
careSetArray);
}
}
break;
}
default: {
fail("bad switch in debugging AG\n");
}
}
FREE(lrlOriginalFormulaText);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FsmPathDebugAUFormula | ( | McOptions_t * | options, |
| mdd_t * | aState, | ||
| Ctlp_Formula_t * | ctlFormula, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a AU formula]
SideEffects []
Definition at line 1491 of file mcDbg.c.
{
Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula );
Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
Ctlp_Formula_t *lrFormula = Ctlp_FormulaReadRightChild( lFormula );
Ctlp_Formula_t *lrlFormula = Ctlp_FormulaReadLeftChild( lrFormula );
Ctlp_Formula_t *lrllFormula = Ctlp_FormulaReadLeftChild( lrlFormula );
Ctlp_Formula_t *llFormula = Ctlp_FormulaReadLeftChild( lFormula );
Ctlp_Formula_t *llrFormula = Ctlp_FormulaReadRightChild( llFormula );
Ctlp_Formula_t *llrlFormula = Ctlp_FormulaReadLeftChild( llrFormula );
Ctlp_Formula_t *llrllFormula = Ctlp_FormulaReadLeftChild( llrlFormula );
Ctlp_Formula_t *fFormula = llrllFormula;
Ctlp_Formula_t *gFormula = lrllFormula;
Ctlp_Formula_t *fOriginalFormula = Ctlp_FormulaReadOriginalFormula(fFormula);
Ctlp_Formula_t *gOriginalFormula = Ctlp_FormulaReadOriginalFormula(gFormula);
char *fText = Ctlp_FormulaConvertToString( fOriginalFormula );
char *gText = Ctlp_FormulaConvertToString( gOriginalFormula );
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
char *firstStateName = Mc_MintermToString(aState, PSVars,
Fsm_FsmReadNetwork(modelFsm));
McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
boolean printInputs = McOptionsReadPrintInputs( options );
if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
fprintf(vis_stdout, "--State\n%sfails AU formula\n\n",
firstStateName);
else
fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName,
originalFormulaText );
FREE(firstStateName);
FREE(originalFormulaText);
/* orginal formula is A(fUg) => converted is !((E[!g U (!f*!g)]) + (EG!g)) */
if ( McStateSatisfiesFormula( llFormula, aState ) ) {
/*
* the case E[!g U (!f*!g)] is true
*/
McPath_t *counterExamplePath = DebugEU(llFormula, aState, modelFsm,
careSetArray);
array_t *stemArray = McPathReadStemArray( counterExamplePath );
array_t *witnessArray = stemArray;
mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
mdd_t *lastState = array_fetch_last( mdd_t *, witnessArray );
char *firstStateName = Mc_MintermToString(firstState, PSVars,
Fsm_FsmReadNetwork(modelFsm));
switch ( debugLevel ) {
case McDbgLevelMinVerbose_c:
fprintf(vis_stdout,
"--Counter example is a fair path where %s is false until %s is also false\n",
gText, fText);
case McDbgLevelMin_c:
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath(witnessArray, modelFsm, printInputs);
fprintf(vis_stdout, " --Counter example ends\n\n");
McFsmStateDebugFormula(options, llrFormula, lastState, modelFsm,
careSetArray);
break;
case McDbgLevelMax_c:
case McDbgLevelInteractive_c: {
if ( array_n(witnessArray ) == 1 ) {
fprintf(vis_stdout,
"--At state %s\nformula %s is false and\nformula %s is also false\n",
firstStateName, fText, gText);
if (debugLevel == McDbgLevelMax_c ||
(debugLevel == McDbgLevelInteractive_c &&
McQueryContinue(
"Continue debugging AU formula? (1-yes,0-no)\n"))) {
McFsmStateDebugFormula(options, fFormula, aState, modelFsm,
careSetArray);
McFsmStateDebugFormula(options, gFormula, aState, modelFsm,
careSetArray);
}
}
else {
int i;
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath(witnessArray,modelFsm,printInputs);
fprintf(vis_stdout, " --Counter example ends\n\n");
for( i=0 ; i < ( array_n( witnessArray ) - 1 ); i++ ) {
mdd_t *aState = array_fetch( mdd_t *, witnessArray, i );
if (debugLevel == McDbgLevelMax_c ||
(debugLevel == McDbgLevelInteractive_c &&
McQueryContinue(
"Continue debugging AU formula? (1-yes,0-no)\n"))) {
McFsmStateDebugFormula(options, gFormula, aState, modelFsm,
careSetArray);
}
}
if (debugLevel == McDbgLevelMax_c ||
(debugLevel == McDbgLevelInteractive_c &&
McQueryContinue(
"Continue debugging AU formula? (1-yes,0-no)\n"))) {
McFsmStateDebugFormula(options, fFormula, lastState, modelFsm,
careSetArray);
McFsmStateDebugFormula(options, gFormula, lastState, modelFsm,
careSetArray);
}
}
break;
}
default: {
fail("Unknown case in debugging AU\n");
}
}/* case */
McPathFree( counterExamplePath );
}
else {
/*
* must be the case that EG!g
*/
McPath_t *counterExamplePath = DebugEG(lrFormula, aState, modelFsm,
careSetArray,
options);
assert( McStateSatisfiesFormula( lrFormula, aState ) );
if( debugLevel != McDbgLevelMin_c)
fprintf(vis_stdout,
"--Counter example is a fair path where %s is always false\n",
gText);
switch ( debugLevel ) {
case McDbgLevelMin_c:
case McDbgLevelMinVerbose_c:{
McPath_t *normalPath = McPathNormalize( counterExamplePath );
array_t *stem = McPathReadStemArray( normalPath );
array_t *cycle = McPathReadCycleArray( normalPath );
fprintf(vis_stdout, " --Counter example begins\n");
(void) fprintf( vis_stdout, "--Fair path stem:\n");
Mc_PrintPath( stem, modelFsm, printInputs );
(void) fprintf( vis_stdout, "--Fair path cycle:\n");
Mc_PrintPath( cycle, modelFsm, printInputs );
fprintf(vis_stdout, " --Counter example ends\n\n");
McPathFree( normalPath );
break;
}
case McDbgLevelMax_c:
case McDbgLevelInteractive_c:
{
int i;
array_t *stemArray = McPathReadStemArray( counterExamplePath );
array_t *cycleArray = McPathReadCycleArray( counterExamplePath );
array_t *witnessArray = McCreateMergedPath( stemArray, cycleArray );
McPath_t *normalPath = McPathNormalize( counterExamplePath );
array_t *stem = McPathReadStemArray( normalPath );
array_t *cycle = McPathReadCycleArray( normalPath );
fprintf(vis_stdout, " --Counter example begins\n");
(void) fprintf( vis_stdout, "--Fair path stem:\n");
Mc_PrintPath( stem, modelFsm, printInputs );
(void) fprintf( vis_stdout, "--Fair path cycle:\n");
Mc_PrintPath( cycle, modelFsm, printInputs );
fprintf(vis_stdout, " --Counter example ends\n\n");
McPathFree( normalPath );
for( i=0 ; i < ( array_n( witnessArray )-1 ); i++ ) {
mdd_t *aState = array_fetch( mdd_t *, witnessArray, i );
if (debugLevel == McDbgLevelMax_c ||
(debugLevel == McDbgLevelInteractive_c &&
McQueryContinue(
"--Continue debugging AU formula? (1-yes,0-no)\n"))) {
McFsmStateDebugFormula(options, lrllFormula, aState, modelFsm,
careSetArray);
}
}
break;
}
default: {
fail("Bad switch in debugging AU formula\n");
}
}/* case */
McPathFree( counterExamplePath );
}
FREE( fText );
FREE( gText );
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FsmPathDebugAXFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| McPath_t * | counterExamplePath, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a AX formula]
SideEffects []
Definition at line 1202 of file mcDbg.c.
{
Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula );
Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
Ctlp_Formula_t *llFormula = Ctlp_FormulaReadLeftChild( lFormula );
Ctlp_Formula_t *lllFormula = Ctlp_FormulaReadLeftChild( llFormula );
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
array_t *witnessArray = McPathReadStemArray( counterExamplePath );
mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
mdd_t *lastState = array_fetch( mdd_t *, witnessArray, 1 );
char *firstStateName = Mc_MintermToString(firstState, PSVars,
Fsm_FsmReadNetwork(modelFsm));
boolean printInputs = McOptionsReadPrintInputs( options );
if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
fprintf(vis_stdout, "--State\n%sfails AX formula\n\n",
firstStateName);
else
fprintf(vis_stdout, "--State\n%sfails %s\n\n", firstStateName,
originalFormulaText );
FREE(firstStateName);
FREE(originalFormulaText);
switch ( McOptionsReadDbgLevel( options ) ) {
case McDbgLevelMin_c:
case McDbgLevelMinVerbose_c:
case McDbgLevelMax_c:
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath( witnessArray, modelFsm, printInputs );
fprintf(vis_stdout, " --Counter example ends\n\n");
fprintf(vis_stdout, "\n");
McFsmStateDebugFormula(options, lllFormula, lastState, modelFsm,
careSetArray);
break;
case McDbgLevelInteractive_c:
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath( witnessArray, modelFsm, printInputs );
fprintf(vis_stdout, " --Counter example ends\n\n");
if ( McQueryContinue("Continue debugging EX formula? (1-yes,0-no)\n") ) {
McFsmStateDebugFormula(options, lllFormula, lastState, modelFsm,
careSetArray);
}
break;
default:
fail("Bad switch in FsmPathDebugAXFormula\n");
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FsmPathDebugEFFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| McPath_t * | witnessPath, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a EF formula]
SideEffects []
Definition at line 1105 of file mcDbg.c.
{
Ctlp_Formula_t *originalFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
char *originalFormulaText = Ctlp_FormulaConvertToString( originalFormula );
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
array_t *witnessArray = McPathReadStemArray( witnessPath );
mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
mdd_t *lastState = array_fetch_last( mdd_t *, witnessArray );
char *firstStateName = Mc_MintermToString(firstState, PSVars,
Fsm_FsmReadNetwork(modelFsm));
Ctlp_Formula_t *rFormula = Ctlp_FormulaReadRightChild( ctlFormula );
Ctlp_Formula_t *rOriginalFormula = Ctlp_FormulaReadOriginalFormula(rFormula);
char *rOriginalFormulaText = Ctlp_FormulaConvertToString( rOriginalFormula );
char *rFormulaText = Ctlp_FormulaConvertToString( rFormula );
McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
boolean printInputs = McOptionsReadPrintInputs( options );
if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
fprintf(vis_stdout, "--State\n%spasses EF formula\n\n",
firstStateName);
else
fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName,
originalFormulaText );
FREE(firstStateName);
FREE(originalFormulaText);
switch ( debugLevel ) {
case McDbgLevelMin_c:
case McDbgLevelMinVerbose_c:
if ( array_n(witnessArray ) == 1 ) {
if( debugLevel != McDbgLevelMin_c)
fprintf(vis_stdout, "since %s is true at this state\n",
rOriginalFormulaText);
FREE( rOriginalFormulaText );
McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
careSetArray);
}
else {
if( debugLevel != McDbgLevelMin_c)
fprintf(vis_stdout,
"--Witness is a path to a state where %s is finally true\n",
rOriginalFormulaText);
(void) fprintf( vis_stdout, "\n--Fair path stem:\n");
FREE( rOriginalFormulaText );
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath( witnessArray, modelFsm, printInputs );
fprintf(vis_stdout, " --Counter example ends\n\n");
}
break;
case McDbgLevelMax_c:
case McDbgLevelInteractive_c:
if ( array_n(witnessArray ) == 1 ) {
McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
careSetArray);
}
else
{
fprintf(vis_stdout,
"--Witness is a path to a state where %s is finally true\n",
rOriginalFormulaText);
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath( witnessArray, modelFsm, printInputs);
fprintf(vis_stdout, " --Counter example ends\n\n");
if (debugLevel == McDbgLevelMax_c ||
(debugLevel == McDbgLevelInteractive_c &&
McQueryContinue(
"--Continue debugging EF formula? (1-yes,0-no)\n")))
{
McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
careSetArray);
}
}
break;
default:
fail("bad switch in debugging EF\n");
}
FREE(rFormulaText);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FsmPathDebugEGFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| McPath_t * | witnessPath, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a path for EG type formula.]
SideEffects []
Definition at line 1007 of file mcDbg.c.
{
mdd_t *firstState;
char *firstStateName;
array_t *witnessArray;
char *ctlFormulaText = Ctlp_FormulaConvertToString( ctlFormula );
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
array_t *stemArray = McPathReadStemArray( witnessPath );
array_t *cycleArray = McPathReadCycleArray( witnessPath );
Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
char *lFormulaText = Ctlp_FormulaConvertToString( lFormula );
McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
boolean printInputs = McOptionsReadPrintInputs( options );
witnessArray = McCreateMergedPath( stemArray, cycleArray );
firstState = array_fetch( mdd_t *, witnessArray, 0 );
firstStateName = Mc_MintermToString(firstState, PSVars,Fsm_FsmReadNetwork(modelFsm));
if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
fprintf(vis_stdout, "--State\n%spasses EG formula\n\n",
firstStateName);
else
fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName,
ctlFormulaText );
FREE(firstStateName);
FREE(ctlFormulaText);
switch ( debugLevel ) {
case McDbgLevelMin_c:
case McDbgLevelMinVerbose_c: {
McPath_t *normalPath = McPathNormalize( witnessPath );
array_t *stem = McPathReadStemArray( normalPath );
array_t *cycle = McPathReadCycleArray( normalPath );
if(debugLevel != McDbgLevelMin_c)
fprintf(vis_stdout, "--Witness is a fair path where %s is always true\n",
lFormulaText);
FREE( lFormulaText );
fprintf(vis_stdout, " --Counter example begins\n");
(void) fprintf( vis_stdout, "--Fair path stem:\n");
Mc_PrintPath( stem, modelFsm, printInputs );
(void) fprintf( vis_stdout, "--Fair path cycle:\n");
Mc_PrintPath( cycle, modelFsm, printInputs );
fprintf(vis_stdout, "\n");
fprintf(vis_stdout, " --Counter example ends\n\n");
McPathFree( normalPath );
break;
}
case McDbgLevelMax_c:
case McDbgLevelInteractive_c: {
McPath_t *normalPath = McPathNormalize( witnessPath );
array_t *stem = McPathReadStemArray( normalPath );
array_t *cycle = McPathReadCycleArray( normalPath );
int i;
fprintf(vis_stdout, "--Witness is a fair path where %s is always true\n",
lFormulaText);
fprintf(vis_stdout, " --Counter example begins\n");
(void) fprintf( vis_stdout, "--Fair path stem:\n");
Mc_PrintPath( stem, modelFsm, printInputs );
(void) fprintf( vis_stdout, "--Fair path cycle:\n");
Mc_PrintPath( cycle, modelFsm, printInputs );
fprintf(vis_stdout, " --Counter example ends\n\n");
for( i=0 ; i < ( array_n( witnessArray )-1 ); i++ ) {
mdd_t *aState = array_fetch( mdd_t *, witnessArray, i );
if (debugLevel == McDbgLevelMax_c ||
(debugLevel == McDbgLevelInteractive_c &&
McQueryContinue(
"--Continue debugging EG formula? (1-yes,0-no)\n"))) {
McFsmStateDebugFormula(options, lFormula, aState, modelFsm,
careSetArray);
}
}
break;
}
default:
fail("Bad switch in FsmPathDebugEGFormula\n");
}
McNormalizeBddPointer(witnessArray);
mdd_array_free( witnessArray );
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FsmPathDebugEUFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| McPath_t * | witnessPath, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a path for EU type formula.]
SideEffects []
Definition at line 913 of file mcDbg.c.
{
char *ctlFormulaText = Ctlp_FormulaConvertToString( ctlFormula );
Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
Ctlp_Formula_t *rFormula = Ctlp_FormulaReadRightChild( ctlFormula );
char *lFormulaText = Ctlp_FormulaConvertToString( lFormula );
char *rFormulaText = Ctlp_FormulaConvertToString( rFormula );
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
array_t *witnessArray = McPathReadStemArray( witnessPath );
mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
mdd_t *lastState = GET_NORMAL_PT(array_fetch_last( mdd_t *, witnessArray ));
char *firstStateName = Mc_MintermToString(firstState, PSVars,
Fsm_FsmReadNetwork(modelFsm));
McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
boolean printInputs = McOptionsReadPrintInputs( options );
if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
fprintf(vis_stdout, "--State\n%spasses EU formula\n\n",
firstStateName);
else
fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName,
ctlFormulaText );
FREE(firstStateName);
FREE(ctlFormulaText);
switch ( debugLevel ) {
case McDbgLevelMin_c:
case McDbgLevelMinVerbose_c:
if ( array_n(witnessArray ) == 1 ) {
if( debugLevel != McDbgLevelMin_c )
fprintf(vis_stdout, "since %s is true at this state", rFormulaText);
McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
careSetArray);
}
else {
if( debugLevel != McDbgLevelMin_c )
fprintf(vis_stdout, "--Path on which %s is true till %s is true\n",
lFormulaText, rFormulaText);
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath(witnessArray, modelFsm, printInputs);
fprintf(vis_stdout, " --Counter example ends\n\n");
McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
careSetArray);
}
break;
case McDbgLevelMax_c:
case McDbgLevelInteractive_c:
if ( array_n(witnessArray ) == 1 ) {
fprintf(vis_stdout, "since %s is true at this state", rFormulaText);
McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
careSetArray);
}
else {
int i;
fprintf(vis_stdout, "--Path on which %s is true till %s is true\n",
lFormulaText, rFormulaText);
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath(witnessArray,modelFsm,printInputs);
fprintf(vis_stdout, " --Counter example ends\n\n");
for( i=0 ; i < ( array_n( witnessArray ) - 1 ); i++ ) {
mdd_t *aState = array_fetch( mdd_t *, witnessArray, i );
if (debugLevel == McDbgLevelMax_c ||
(debugLevel == McDbgLevelInteractive_c &&
McQueryContinue(
"Continue debugging EU formula? (1-yes,0-no)\n"))) {
McFsmStateDebugFormula(options, lFormula, aState, modelFsm,
careSetArray);
}
}
McFsmStateDebugFormula(options, rFormula, lastState, modelFsm,
careSetArray);
}
break;
default:
fail("Should not be here - bad switch in debugging EU formula\n");
}
FREE(lFormulaText);
FREE(rFormulaText);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FsmPathDebugEXFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| McPath_t * | witnessPath, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a path for EX type formula.]
SideEffects []
Definition at line 848 of file mcDbg.c.
{
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
array_t *witnessArray = McPathReadStemArray( witnessPath );
mdd_t *firstState = array_fetch( mdd_t *, witnessArray, 0 );
char *firstStateName = Mc_MintermToString(firstState, PSVars,
Fsm_FsmReadNetwork(modelFsm));
Ctlp_Formula_t *lChild = Ctlp_FormulaReadLeftChild( ctlFormula );
char *ctlFormulaText = Ctlp_FormulaConvertToString( ctlFormula );
boolean printInputs = McOptionsReadPrintInputs( options );
mdd_t *secondlastState;
if(array_n(witnessArray)<2)
{
fprintf(vis_stdout,"witnessArray has less than two elements, return\n");
return;
}
secondlastState= array_fetch( mdd_t *, witnessArray, (array_n(witnessArray)-1) );
if( McOptionsReadDbgLevel( options ) == McDbgLevelMin_c)
fprintf(vis_stdout, "--State\n%spasses EX formula\n\n",
firstStateName);
else
fprintf(vis_stdout, "--State\n%spasses formula %s\n\n", firstStateName,
ctlFormulaText );
FREE(firstStateName);
FREE(ctlFormulaText);
switch ( McOptionsReadDbgLevel( options ) ) {
case McDbgLevelMin_c:
case McDbgLevelMinVerbose_c:
case McDbgLevelMax_c:
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath( witnessArray, modelFsm, printInputs );
fprintf(vis_stdout, " --Counter example ends\n\n");
McFsmStateDebugFormula(options, lChild, secondlastState, modelFsm,
careSetArray);
break;
case McDbgLevelInteractive_c:
fprintf(vis_stdout, " --Counter example begins\n");
Mc_PrintPath( witnessArray, modelFsm, printInputs );
fprintf(vis_stdout, " --Counter example ends\n\n");
if (McQueryContinue("Continue debugging EX formula? (1-yes,0-no)\n"))
McFsmStateDebugFormula(options, lChild, secondlastState, modelFsm,
careSetArray);
break;
default:
fail("Reached bad switch in FsmPathDebugEXFormula\n");
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FsmPathDebugFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| McPath_t * | witnessPath, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a formula of the form EX, EG, EU, EF.]
SideEffects []
Definition at line 809 of file mcDbg.c.
{
switch ( Ctlp_FormulaReadType( ctlFormula ) ) {
case Ctlp_EX_c: {
FsmPathDebugEXFormula(options, ctlFormula, modelFsm, witnessPath,
careSetArray);
break;
}
case Ctlp_EU_c: {
FsmPathDebugEUFormula(options, ctlFormula, modelFsm, witnessPath,
careSetArray);
break;
}
case Ctlp_EG_c: {
FsmPathDebugEGFormula(options, ctlFormula, modelFsm, witnessPath,
careSetArray);
break;
}
default: {
fail("bad switch in converting converted formula\n");
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void FsmStateDebugConvertedFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| mdd_t * | aState, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Debug a converted formula]
Comment [There are five kinds of formula that are converted: EF, AU, AF, AG, AX. The Ctlp_Formula_t structure has a pointer back to the original formula (where one exists). For the non-trivial cases (AU, AF, AG, AX) if the formula is false, we create a counter example, i.e. a fair path which fails the property. The AG, AX, AF cases are simple; the AU case is tricky because this can be failed on two ways.]
SideEffects []
Definition at line 704 of file mcDbg.c.
{
McPath_t *witnessPath;
McPath_t *counterExamplePath;
Ctlp_Formula_t *originalFormula =Ctlp_FormulaReadOriginalFormula(ctlFormula);
Ctlp_Formula_t *lFormula = Ctlp_FormulaReadLeftChild( ctlFormula );
McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
if ( Ctlp_FormulaReadType( ctlFormula ) == Ctlp_EU_c ) {
if ( !McStateSatisfiesFormula( ctlFormula, aState ) ) {
mdd_t *passStates = Ctlp_FormulaObtainLatestApprox(ctlFormula);
mdd_t *closeState;
Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork(modelFsm);
array_t *PSVars = Fsm_FsmReadPresentStateVars(modelFsm);
McStateFailsFormula( aState, originalFormula, debugLevel, modelFsm );
if (mdd_is_tautology(passStates, 0)) {
fprintf(vis_stdout,
"--No state satisfies the formula\n");
} else {
fprintf(vis_stdout,
"\n--A simple counter example does not exist since it\n");
fprintf(vis_stdout,
" requires generating all paths from the state\n");
fprintf(vis_stdout,
"--A state at minimum distance satisfying the formula is\n");
closeState = McComputeACloseState(passStates, aState, modelFsm);
Mc_MintermPrint(closeState, PSVars, modelNetwork);
mdd_free(closeState);
}
mdd_free(passStates);
}
else {
witnessPath = DebugEU(ctlFormula, aState, modelFsm, careSetArray);
FsmPathDebugEFFormula(options, ctlFormula, modelFsm, witnessPath,
careSetArray);
McPathFree( witnessPath );
}
return;
}
/*
* The original formula must be an AX,AF,AG, or AU formula
*/
if ( McStateSatisfiesFormula( ctlFormula, aState ) ) {
McStatePassesFormula( aState, originalFormula, debugLevel, modelFsm );
fprintf(vis_stdout,
"--A simple witness does not exist since it requires\n");
fprintf(vis_stdout, " generating all paths from the state\n");
return;
}
switch ( Ctlp_FormulaReadType( lFormula ) ) {
case Ctlp_EX_c: {
counterExamplePath = DebugEX(lFormula, aState, modelFsm, careSetArray);
FsmPathDebugAXFormula(options, ctlFormula, modelFsm, counterExamplePath,
careSetArray);
McPathFree( counterExamplePath );
break;
}
case Ctlp_EG_c: {
counterExamplePath = DebugEG(lFormula, aState, modelFsm, careSetArray,
options);
FsmPathDebugAFFormula(options, ctlFormula, modelFsm, counterExamplePath,
careSetArray);
McPathFree( counterExamplePath );
break;
}
case Ctlp_EU_c: {
counterExamplePath = DebugEU(lFormula, aState, modelFsm, careSetArray);
FsmPathDebugAGFormula(options, ctlFormula, modelFsm, counterExamplePath,
careSetArray);
McPathFree( counterExamplePath );
break;
}
case Ctlp_OR_c: {
/*
* need special functions bcoz of two possibilities
*/
FsmPathDebugAUFormula(options, aState, ctlFormula, modelFsm,
careSetArray);
break;
}
default: fail("Bad formula type in handling converted operator\n");
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| McPath_t* McBuildFairPath | ( | mdd_t * | startState, |
| mdd_t * | invariantStates, | ||
| array_t * | arrayOfOnionRings, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray, | ||
| Mc_VerbosityLevel | verbosity, | ||
| Mc_DcLevel | dcLevel, | ||
| Mc_FwdBwdAnalysis | fwdBwd | ||
| ) |
Function********************************************************************
Synopsis [Build fair path starting from aState, using given debug information.]
Description [Build fair path starting from aState, using given array of onion rings. Each member of this array of onion rings is an array of rings of states leading to a fairness constraint. Function returns an McPath_t, which consists of a stem array which is a sequence of states, and a path array which is a sequence of states starting from the last state in stem array, leading back to a state existing in stem array. In this sense, it is confusing, since the "cycle" is not a true cycle (it just completes a cycle).]
Comment [Proceed by building a path which passes through each fairness constraint. Then attempt to complete a cycle by seeing if a path can be found from the last state to the first state satisfying the first fairness constraint.]
SideEffects []
Definition at line 302 of file mcDbg.c.
{
mdd_t *tmpState;
mdd_t *lastState;
mdd_t *rootState = mdd_dup( startState );
mdd_t *currentState = mdd_dup( rootState );
mdd_t *stemState = NIL(mdd_t);
array_t *tmpStemArray;
array_t *dupArrayOfOnionRings = array_dup( arrayOfOnionRings );
array_t *stemArray = array_alloc(mdd_t *, 0 );
array_t *cycleArray = NIL(array_t);
McPath_t *fairPath;
array_insert_last( mdd_t *, stemArray, currentState );
while ( array_n( dupArrayOfOnionRings ) > 0 ) {
int index = McComputeOnionRingsWithClosestCore(currentState,
dupArrayOfOnionRings, modelFsm);
array_t *onionRingsWithClosestFairness = array_fetch(array_t *,
dupArrayOfOnionRings, index);
array_t *tmpArray = Mc_BuildPathToCore(currentState,
onionRingsWithClosestFairness,
modelFsm, McGreaterOrEqualZero_c);
if ( stemState == NIL(mdd_t) ) {
tmpState = array_fetch_last( mdd_t *, tmpArray );
stemState = mdd_dup( tmpState );
}
tmpStemArray = McCreateMergedPath( stemArray, tmpArray );
McNormalizeBddPointer(stemArray);
McNormalizeBddPointer(tmpArray);
mdd_array_free( stemArray );
mdd_array_free( tmpArray );
stemArray = tmpStemArray;
currentState = array_fetch_last( mdd_t *, stemArray );
tmpArray = McRemoveIndexedOnionRings( index, dupArrayOfOnionRings );
array_free( dupArrayOfOnionRings );
dupArrayOfOnionRings = tmpArray;
} /* while onionrings left */
array_free( dupArrayOfOnionRings );
tmpState = GET_NORMAL_PT(array_fetch_last( mdd_t *, stemArray ));
lastState = mdd_dup( tmpState );
cycleArray = Mc_CompletePath(lastState, stemState, invariantStates, modelFsm,
careSetArray, verbosity, dcLevel, fwdBwd);
if ( cycleArray != NIL(array_t) ) {
mdd_free( lastState );
}
else {
McPath_t *tmpFairPath;
array_t *tmpStemArray;
/*
* Get shortest path to lastState
*/
McNormalizeBddPointer(stemArray);
mdd_array_free( stemArray );
if ( !mdd_equal( rootState, lastState ) ) {
stemArray = Mc_CompletePath(rootState, lastState, invariantStates,
modelFsm, careSetArray, verbosity, dcLevel,
fwdBwd);
}
else {
stemArray = array_alloc( mdd_t *, 0 );
tmpState = mdd_dup( rootState );
array_insert_last( mdd_t *, stemArray, tmpState );
}
mdd_free( lastState );
tmpState = GET_NORMAL_PT(array_fetch_last( mdd_t *, stemArray ));
lastState = mdd_dup( tmpState );
if ( mdd_equal( lastState, rootState ) ) {
/*
* Force a descent in the SCC DAG
mdd_t *descendantState = McGetSuccessorInTarget(lastState,
invariantStates, modelFsm);
*/
mdd_t *descendantState = McGetSuccessorInTargetAmongFairStates(lastState,
invariantStates, arrayOfOnionRings, modelFsm);
tmpFairPath = McBuildFairPath(descendantState, invariantStates,
arrayOfOnionRings, modelFsm,
careSetArray,
verbosity, dcLevel, fwdBwd);
tmpStemArray = McCreateJoinedPath(stemArray,
McPathReadStemArray(tmpFairPath));
mdd_free( descendantState );
}
else {
tmpFairPath = McBuildFairPath(lastState, invariantStates,
arrayOfOnionRings, modelFsm,
careSetArray,
verbosity, dcLevel, fwdBwd);
tmpStemArray = McCreateMergedPath(stemArray,
McPathReadStemArray(tmpFairPath));
}
mdd_free( lastState );
McNormalizeBddPointer(stemArray);
mdd_array_free( stemArray );
stemArray = tmpStemArray;
cycleArray = McMddArrayDuplicateFAFW( McPathReadCycleArray( tmpFairPath ) );
McPathFree( tmpFairPath );
if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
mdd_t *S = GET_NORMAL_PT(array_fetch(mdd_t *, stemArray, 0));
mdd_t *T = GET_NORMAL_PT(array_fetch(mdd_t *, stemArray, array_n(stemArray)-1));
array_t *forwardRings = Mc_BuildForwardRingsWithInvariants(
S, T, invariantStates, modelFsm);
tmpStemArray = Mc_BuildPathFromCoreFAFW(
T, forwardRings, modelFsm, McGreaterOrEqualZero_c);
McNormalizeBddPointer(stemArray);
mdd_array_free(stemArray);
mdd_array_free(forwardRings);
stemArray = tmpStemArray;
}
}
mdd_free( rootState );
mdd_free( stemState );
fairPath = McPathAlloc();
McPathSetStemArray( fairPath, stemArray );
McPathSetCycleArray( fairPath, cycleArray );
return fairPath;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int McFsmDebugFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Debug CTL formula in existential normal form]
Description [Debug CTL formula in existential normal form. The extent to which debug information is generated is a function of options settings.
The debugger works with ctlFormula, but uses the pointers back to the original formula that it was converted from, to give the user more sensible feedback. To do this, it relies on a specific translation: only EF, AU, AF, AG, and AX are converted. Hence, the only times that the converted bit is set, we have a conversion of one of these formulas, and the operator is either EU, or negation. in the latter case, we can conclude from the child of the negation what formula we converted from: EX means AX, EG means AF, EU means AG, and OR means AU. ]
SideEffects [Affects vis_stdpipe]
SeeAlso [Ctlp_FormulaConvertToExistentialForm]
Definition at line 99 of file mcDbg.c.
{
mdd_t *modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm);
mdd_t *goodStates = Ctlp_FormulaObtainLatestApprox(ctlFormula);
mdd_t *badStates = mdd_and(modelInitialStates, goodStates, 1, 0);
mdd_t *witnessSuccState;
FILE *debugFile = McOptionsReadDebugFile(options);
FILE *oldStdOut;
FILE *oldStdErr;
extern FILE *vis_stdpipe;
char *nrOfTracesString;
int nrOfTraces; /* nr of debug traces that we output */
int i; /* counts debug traces */
mdd_free(modelInitialStates);
oldStdOut = vis_stdout;
oldStdErr = vis_stderr;
nrOfTracesString = Cmd_FlagReadByName("nr_counterexamples");
if(nrOfTracesString == NIL(char))
nrOfTraces = 1;
else
nrOfTraces = atoi(nrOfTracesString);
if (debugFile) {
vis_stdpipe = debugFile;
vis_stdout = vis_stdpipe;
(void)fprintf(vis_stdpipe, "# MC: formula failed --- ");
Ctlp_FormulaPrint(vis_stdpipe,Ctlp_FormulaReadOriginalFormula(ctlFormula));
(void)fprintf(vis_stdpipe, "\n");
} else if (McOptionsReadUseMore(options)){
vis_stdpipe = popen("more", "w");
vis_stdout = vis_stdpipe;
vis_stderr = vis_stdpipe;
}
else
vis_stdpipe = vis_stdout;
for(i = 0; i < nrOfTraces; i++){
(void)fprintf(vis_stdout, "# MC: Calling debugger for trace %d\n",
i+1);
witnessSuccState = McComputeACloseState(badStates, goodStates, modelFsm);
McFsmStateDebugFormula(options, ctlFormula, witnessSuccState, modelFsm,
careSetArray);
(void)fprintf(vis_stdout, "\n");
mdd_free(witnessSuccState);
}
mdd_free(badStates);
mdd_free(goodStates);
if (vis_stdout != oldStdOut && vis_stdout != debugFile)
(void)pclose(vis_stdpipe);
vis_stdout = oldStdOut;
vis_stderr = oldStdErr;
return 1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void McFsmStateDebugFormula | ( | McOptions_t * | options, |
| Ctlp_Formula_t * | ctlFormula, | ||
| mdd_t * | aState, | ||
| Fsm_Fsm_t * | modelFsm, | ||
| array_t * | careSetArray | ||
| ) |
Function********************************************************************
Synopsis [Debug CTL formula in existential normal form at state aState]
Description [Debug CTL formula in existential normal form at state aState. Formula is assumed to have been CONVERTED to existential normal form.]
SideEffects []
Definition at line 176 of file mcDbg.c.
{
Ctlp_Formula_t *originalFormula;
McDbgLevel debugLevel = McOptionsReadDbgLevel( options );
if ( ctlFormula == NIL(Ctlp_Formula_t) )
return;
if ( Ctlp_FormulaTestIsConverted( ctlFormula ) ) {
FsmStateDebugConvertedFormula(options, ctlFormula, aState, modelFsm,
careSetArray);
return;
}
originalFormula = Ctlp_FormulaReadOriginalFormula( ctlFormula );
switch ( Ctlp_FormulaReadType( ctlFormula ) ) {
case Ctlp_ID_c :
DebugID( options, ctlFormula, aState, modelFsm );
break;
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
DebugTrueFalse( ctlFormula, aState, modelFsm );
break;
case Ctlp_EQ_c:
case Ctlp_XOR_c:
case Ctlp_THEN_c:
case Ctlp_NOT_c:
case Ctlp_AND_c:
case Ctlp_OR_c:
DebugBoolean(options, ctlFormula, aState, modelFsm, careSetArray);
break;
case Ctlp_EX_c:
case Ctlp_EU_c:
case Ctlp_EG_c:
if ( !McStateSatisfiesFormula( ctlFormula, aState ) ) {
mdd_t *passStates = Ctlp_FormulaObtainLatestApprox(ctlFormula);
mdd_t *closeState;
Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork(modelFsm);
array_t *PSVars = Fsm_FsmReadPresentStateVars(modelFsm);
McStateFailsFormula(aState, originalFormula, debugLevel, modelFsm);
if (mdd_is_tautology(passStates, 0)) {
fprintf(vis_stdout,
"--No state satisfies the formula\n");
mdd_free(passStates);
break;
}
fprintf(vis_stdout,
"--A simple counter example does not exist since it\n");
fprintf(vis_stdout,
" requires generating all paths from the state\n");
fprintf(vis_stdout,
"--A state at minimum distance satisfying the formula is\n");
closeState = McComputeACloseState(passStates, aState, modelFsm);
mdd_free(passStates);
Mc_MintermPrint(closeState, PSVars, modelNetwork);
mdd_free(closeState);
break;
}
else {
McPath_t *witnessPath = NIL(McPath_t);
if ( Ctlp_FormulaReadType( ctlFormula ) == Ctlp_EX_c ) {
witnessPath = DebugEX(ctlFormula, aState, modelFsm, careSetArray);
}
else if ( Ctlp_FormulaReadType( ctlFormula ) == Ctlp_EU_c ) {
witnessPath = DebugEU(ctlFormula, aState, modelFsm, careSetArray);
}
else {
witnessPath = DebugEG(ctlFormula, aState, modelFsm, careSetArray,
options);
}
FsmPathDebugFormula(options, ctlFormula, modelFsm, witnessPath,
careSetArray);
McPathFree( witnessPath );
}
break;
case Ctlp_Cmp_c:
case Ctlp_Init_c:
case Ctlp_FwdU_c:
case Ctlp_FwdG_c:
case Ctlp_EY_c:
case Ctlp_EH_c:
break;
default: {
fail("Bad switch in debugging normal formula\n");
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: mcDbg.c,v 1.43 2005/04/23 04:40:54 fabio Exp $" [static] |
CFile***********************************************************************
FileName [mcDbg.c]
PackageName [mc]
Synopsis [Debugger for Fair CTL models]
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.]
