src/mc/mcDbg.c

Go to the documentation of this file.

#include "mcInt.h"

static char rcsid[] UNUSED = "$Id: mcDbg.c,v 1.43 2005/04/23 04:40:54 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* 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);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

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;
}

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");
    }
  }
}




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                                            */
/*---------------------------------------------------------------------------*/


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 );
  }
}

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"));
}

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);
  }
}

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;
}

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;
}

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;
}


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");
  }
}


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");
    }
  }
}

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");
  }
}

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);
}
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 );
}

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);
}

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");
  }
}

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);
}

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);
}

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 );
}