/**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.] ******************************************************************************/ #include "mcInt.h" static char rcsid[] UNUSED = "$Id: mcDbg.c,v 1.43 2005/04/23 04:40:54 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ 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); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**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] ******************************************************************************/ int McFsmDebugFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, array_t *careSetArray) { 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; } /**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 [] ******************************************************************************/ void McFsmStateDebugFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray) { 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"); } } } /**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 [] ******************************************************************************/ 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 ) { 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; } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ static void DebugID( McOptions_t *options, Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm) { 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 ); } } /**Function******************************************************************** Synopsis [Debug a TRUE/FALSE formula] SideEffects [] ******************************************************************************/ static void DebugTrueFalse( Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm) { fprintf(vis_stdout, "--Nothing to debug for %s\n", ((Ctlp_FormulaReadType(aFormula) == Ctlp_TRUE_c) ? "TRUE\n" : "FALSE\n")); } /**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 [] ******************************************************************************/ static void DebugBoolean( McOptions_t *options, Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray) { 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); } } /**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 [] ******************************************************************************/ static McPath_t * DebugEX( Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray) { 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; } /**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 [] ******************************************************************************/ static McPath_t * DebugEU( Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray) { 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; } /**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 [] ******************************************************************************/ static McPath_t * DebugEG( Ctlp_Formula_t *aFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray, McOptions_t *options) { 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; } /**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 [] ******************************************************************************/ static void FsmStateDebugConvertedFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray) { 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"); } } /**Function******************************************************************** Synopsis [Debug a formula of the form EX, EG, EU, EF.] SideEffects [] ******************************************************************************/ static void FsmPathDebugFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray) { 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"); } } } /**Function******************************************************************** Synopsis [Debug a path for EX type formula.] SideEffects [] ******************************************************************************/ static void FsmPathDebugEXFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray) { 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"); } } /**Function******************************************************************** Synopsis [Debug a path for EU type formula.] SideEffects [] ******************************************************************************/ static void FsmPathDebugEUFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray) { 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); } /**Function******************************************************************** Synopsis [Debug a path for EG type formula.] SideEffects [] ******************************************************************************/ static void FsmPathDebugEGFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray) { 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 ); } /**Function******************************************************************** Synopsis [Debug a EF formula] SideEffects [] ******************************************************************************/ static void FsmPathDebugEFFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *witnessPath, array_t *careSetArray) { 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); } /**Function******************************************************************** Synopsis [Debug a AX formula] SideEffects [] ******************************************************************************/ static void FsmPathDebugAXFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray) { 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"); } } /**Function******************************************************************** Synopsis [Debug a AF formula] SideEffects [] ******************************************************************************/ static void FsmPathDebugAFFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray) { 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); } /**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 [] ******************************************************************************/ static void FsmPathDebugAGFormula( McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, McPath_t *counterExamplePath, array_t *careSetArray) { 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); } /**Function******************************************************************** Synopsis [Debug a AU formula] SideEffects [] ******************************************************************************/ static void FsmPathDebugAUFormula( McOptions_t *options, mdd_t *aState, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, array_t *careSetArray) { 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 ); }