src/mc/mcMc.c

Go to the documentation of this file.

#include "ctlpInt.h"
#include "mcInt.h"
#include "fsm.h"
#include "bmc.h"

static char rcsid[] UNUSED = "$Id: mcMc.c,v 1.257 2007/04/17 00:01:22 sohail Exp $";

#ifdef DEBUG_MC
void _McPrintSatisfyingMinterms(mdd_t *aMdd, Fsm_Fsm_t *fsm);
#endif

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

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static mdd_t * EvaluateFormulaRecur(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Ctlp_Approx_t TRMinimization, Ctlp_Approx_t *resultApproxType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule);
static mdd_t * McForwardReachable(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *invariantMdd, mdd_t *fairStates, array_t *careStatesArray, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);

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

mdd_t *
Mc_FsmCheckLanguageEmptiness(
  Fsm_Fsm_t *modelFsm,
  array_t *modelCareStatesArray,
  Mc_AutStrength_t automatonStrength,
  Mc_LeMethod_t leMethod,
  int dcLevel,
  int dbgLevel,
  int printInputs,
  int verbosity,
  Mc_GSHScheduleType GSHschedule,
  Mc_FwdBwdAnalysis GSHdirection,
  int lockstep,
  FILE *dbgFile,
  int UseMore,
  int SimValue,
  char *driverName)
{
  mdd_t *result;
  mdd_t *mddOne;
  mdd_t *badStates;
  mdd_t *aBadState;
  mdd_t *initialStates;
  mdd_t *fairStates;
  mdd_manager *mddMgr;
  Ctlp_Formula_t *ctlFair, *ctlFormula;
  Mc_EarlyTermination_t *earlyTermination;
  array_t *arrayOfOnionRings;
  array_t *stemArray;
  array_t *cycleArray;
  McPath_t *fairPath;
  McPath_t *normalPath;
  FILE *tmpFile = vis_stdout;
  extern FILE *vis_stdpipe;
  int i;

  if (leMethod == Mc_Le_Dnc_c && automatonStrength == 2) {
    return  Mc_FsmCheckLanguageEmptinessByDnC(modelFsm,
                                              modelCareStatesArray,
                                              Mc_Aut_Strong_c,
                                              dcLevel,
                                              dbgLevel,
                                              printInputs,
                                              verbosity,
                                              GSHschedule,
                                              GSHdirection,
                                              lockstep,
                                              dbgFile,
                                              UseMore,
                                              SimValue,
                                              driverName);
  }
  
  /**************************************************************************
   * CASE1 & CASE2: TERMINAL/WEAK AUTOMATON
   *                problem is reduced to checking !EF (fair) for TERMINAL
   *                or !EF EG (fair) for WEAK
   **************************************************************************/
  if (automatonStrength == 0 || automatonStrength == 1) {
    Fsm_Fairness_t *modelFairness;
    modelFairness = Fsm_FsmReadFairnessConstraint(modelFsm);
    assert(Fsm_FairnessTestIsBuchi(modelFairness));
    ctlFair = Ctlp_FormulaCreate(Ctlp_ID_c,
                                 (void *)util_strsav("fair1$AUT$NTK2"),
                                 (void *)util_strsav("1"));
    /*    Dup(Fsm_FairnessReadFinallyInfFormula(modelFairness, 0, 0));    */
    if (automatonStrength == 0) {
      Ctlp_Formula_t *ctlTRUE;
      ctlTRUE = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t),
                                   NIL(Ctlp_Formula_t));
      ctlFormula = Ctlp_FormulaCreate(Ctlp_EU_c, ctlTRUE, ctlFair);
      if (dbgLevel || verbosity) 
        fprintf(vis_stdout, "# %s: Terminal automaton -- check EF(states satisfy fairness)\n",
                driverName);
    }else {
      Ctlp_Formula_t *ctlTRUE, *ctlEGfair;
      ctlTRUE = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t));
      ctlEGfair = Ctlp_FormulaCreate(Ctlp_EG_c, ctlFair, NIL(Ctlp_Formula_t));
      ctlFormula = Ctlp_FormulaCreate(Ctlp_EU_c, ctlTRUE, ctlEGfair);
      if (dbgLevel || verbosity) 
        fprintf(vis_stdout, "# %s: Weak automaton -- check EF EG (states satisfy fairness)\n",
                driverName);
    }

    /* Evaluate ctlFormula */
    mddMgr = Fsm_FsmReadMddManager(modelFsm);
    mddOne = mdd_one(mddMgr);
    initialStates = Fsm_FsmComputeInitialStates(modelFsm);
    earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
    fairStates = 
      Mc_FsmEvaluateFormula(modelFsm, ctlFormula, mddOne, modelFairness, 
                            modelCareStatesArray,
                            earlyTermination,
                            NIL(Fsm_HintsArray_t), Mc_None_c,
                            (Mc_VerbosityLevel) verbosity,
                            (Mc_DcLevel) dcLevel, 
                            (dbgLevel != McDbgLevelNone_c || verbosity),
                            GSHschedule);
    Mc_EarlyTerminationFree(earlyTermination);
    mdd_free(mddOne);

    /* If there is at least one fair initial state, language is not empty. */
    if (!mdd_lequal(initialStates, fairStates, 1, 0)) {
      if (strcmp(driverName, "LE") == 0)
        fprintf(vis_stdout, "# LE: language is not empty\n");
      else
        fprintf(vis_stdout, "# %s: formula failed\n", driverName);
      result = mdd_and(fairStates, initialStates, 1, 1);
    } else {
      if (strcmp(driverName, "LE") == 0)
        fprintf(vis_stdout, "# LE: language emptiness check passes\n");
      else
        fprintf(vis_stdout, "# %s: formula passed\n", driverName);
      Ctlp_FormulaFree(ctlFormula);
      mdd_free(fairStates);
      mdd_free(initialStates);
      return NIL(mdd_t);
    }

    /* If no wintness is requested, clean up and return. */
    if (dbgLevel == McDbgLevelNone_c) {
      Ctlp_FormulaFree(ctlFormula);
      mdd_free(initialStates);
      mdd_free(fairStates);
      return result;
    }else {
      Ctlp_Formula_t *F;
      array_t *EGArrayOfOnionRings, *EGonionRings, *EFonionRings;
      array_t *newOnionRings;
      mdd_t *mdd1;
      int j;
      arrayOfOnionRings = array_alloc(array_t *, 0);
      EFonionRings = (array_t *) Ctlp_FormulaReadDebugData(ctlFormula);
      if (automatonStrength == 0) {
        array_insert_last(array_t *, arrayOfOnionRings,
                          mdd_array_duplicate(EFonionRings));
      }else if (automatonStrength == 1) {
        F = Ctlp_FormulaReadRightChild(ctlFormula);
        /* EG (states labelled fair) */
        EGArrayOfOnionRings = (array_t *)Ctlp_FormulaReadDebugData(F);
        arrayForEachItem(array_t *, EGArrayOfOnionRings, i, EGonionRings) {
          newOnionRings = mdd_array_duplicate(EGonionRings);
          arrayForEachItem(mdd_t *, EFonionRings, j, mdd1) {
            if (j != 0)
              array_insert_last(mdd_t *, newOnionRings, mdd_dup(mdd1));
          }
          array_insert_last(array_t *, arrayOfOnionRings, newOnionRings);
        }
      }
      Ctlp_FormulaFree(ctlFormula);
      fprintf(vis_stdout, "# %s: generating path to fair cycle\n", driverName);
    }
    
  }else {
    /*************************************************************************
     * CASE3:     STRONG AUTOMATON 
     *            need to solve the problem by computing EG_fair (true) 
     *************************************************************************/
    mddMgr = Fsm_FsmReadMddManager(modelFsm);
    initialStates = Fsm_FsmComputeInitialStates(modelFsm);

    /* Compute fair states. */
    if (lockstep == MC_LOCKSTEP_OFF) {
      fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray,
                                            verbosity, dcLevel, GSHschedule,
                                            GSHdirection, FALSE);
      arrayOfOnionRings = Fsm_FsmReadDebugArray(modelFsm);
    } else {
      /* For lockstep, the computed set of states is a subset of the
         reachable fair states, with the property that the subset is
         empty only if there are no reachable fair states.  Since the
         onion rings are built for the fairness constraint restricted to
         the subset of the fair states, they are not valid in general
         for the FSM.  Hence, they are not saved.  */
      array_t *SCCs = array_alloc(mdd_t *, 0);
      arrayOfOnionRings = array_alloc(array_t *, 0);
      fairStates = McFsmComputeFairSCCsByLockStep(modelFsm, lockstep, SCCs,
                                                  arrayOfOnionRings,
                                                  (Mc_VerbosityLevel)
                                                  verbosity,
                                                  (Mc_DcLevel) dcLevel);
      mdd_array_free(SCCs);
    }

    
    /* Lockstep guarantees that all fair SCCs are reachable.  However,
       it does not extend the fair states backward unless a
       counterexample is requested.  For the SCC hull approach with backward
       operators, the language is not empty if there is at least one
       fair initial state.  Finally, For SCC hull with forward operators,
       currently we do not extend the hull backward, but we enforce
       reachability of the hull.  Hence, nonemptiness of the hull signals that
       the language is not empty. */
    if ((lockstep == MC_LOCKSTEP_OFF &&
         (!mdd_lequal(initialStates, fairStates, 1, 0) ||
          (GSHdirection == McFwd_c &&
           !mdd_lequal_array(fairStates, modelCareStatesArray, 1, 0)))) ||
        (lockstep != MC_LOCKSTEP_OFF &&
         !mdd_is_tautology(fairStates, 0))) {
      if (strcmp(driverName, "LE") == 0)
        fprintf(vis_stdout, "# LE: language is not empty\n");
      else
        fprintf(vis_stdout, "# %s: formula failed\n", driverName);
      result = mdd_and(fairStates, initialStates, 1, 1);
    } else {
      if (strcmp(driverName, "LE") == 0)
        fprintf(vis_stdout, "# LE: language emptiness check passes\n");
      else
        fprintf(vis_stdout, "# %s: formula passed\n", driverName);
      /* Dispose of onion rings if produced by lockstep. */
      if (lockstep != MC_LOCKSTEP_OFF) {
        mdd_array_array_free(arrayOfOnionRings);
      }
      mdd_free(fairStates);
      mdd_free(initialStates);
      return NIL(mdd_t);
    }

    /* If no witness is requested, clean up and return. */
    if (dbgLevel == McDbgLevelNone_c) {
      /* Dispose of onion rings if produced by lockstep. */
      if (lockstep != MC_LOCKSTEP_OFF) {
        mdd_array_array_free(arrayOfOnionRings);
      }
      mdd_free(fairStates);
      mdd_free(initialStates);
      return result;
    } else {
      (void) fprintf(vis_stdout, "# %s: generating path to fair cycle\n",
                     driverName);
    }
  }

  /* Generate witness. */
  badStates = mdd_and(initialStates, fairStates, 1, 1);
  mdd_free(fairStates);
  mdd_free(initialStates);
  aBadState = Mc_ComputeAState(badStates, modelFsm);
  mdd_free(badStates);

  mddOne = mdd_one(mddMgr);
  fairPath = McBuildFairPath(aBadState, mddOne, arrayOfOnionRings, modelFsm,
                             modelCareStatesArray, 
                             (Mc_VerbosityLevel) verbosity,
                             (Mc_DcLevel) dcLevel,
                             McFwd_c);
  mdd_free(mddOne);
  mdd_free(aBadState);
  
  /* Dispose of onion rings if produced by lockstep. */
  if (lockstep != MC_LOCKSTEP_OFF || automatonStrength != 2) {
    mdd_array_array_free(arrayOfOnionRings);
  }

  /* Print witness. */
  normalPath = McPathNormalize(fairPath);
  McPathFree(fairPath);

  stemArray = McPathReadStemArray(normalPath);
  cycleArray = McPathReadCycleArray(normalPath);

  /* we should pass dbgFile/UseMore as parameters 
     dbgFile = McOptionsReadDebugFile(options);*/
  if (dbgFile != NIL(FILE)) {
    vis_stdpipe = dbgFile;
  } else if (UseMore == TRUE) {
    vis_stdpipe = popen("more","w");
  } else {
    vis_stdpipe = vis_stdout;
  }
  vis_stdout = vis_stdpipe;

  /* We should also pass SimValue as a parameter */
  if (SimValue == FALSE) {
      (void) fprintf(vis_stdout, "# %s: path to fair cycle:\n\n", driverName);
      Mc_PrintPath(stemArray, modelFsm, printInputs);
      fprintf (vis_stdout, "\n");

      (void) fprintf(vis_stdout, "# %s: fair cycle:\n\n", driverName);
      Mc_PrintPath(cycleArray, modelFsm, printInputs);
      fprintf (vis_stdout, "\n");
  }else {
      array_t *completePath = McCreateMergedPath(stemArray, cycleArray);
      (void) fprintf(vis_stdout, "# %s: counter-example\n", driverName);
      McPrintSimPath(vis_stdout, completePath, modelFsm);
      mdd_array_free(completePath);
  }

  if (dbgFile == NIL(FILE) && UseMore == TRUE) {
    (void) pclose(vis_stdpipe);
  }  
  vis_stdout = tmpFile;

  McPathFree(normalPath);

  return result;
}


mdd_t *
Mc_FsmEvaluateFormula(
  Fsm_Fsm_t *fsm,
  Ctlp_Formula_t *ctlFormula,
  mdd_t *fairStates,
  Fsm_Fairness_t *fairCondition,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  Fsm_HintsArray_t *hintsArray,
  Mc_GuidedSearch_t hintType,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  int buildOnionRing,
  Mc_GSHScheduleType GSHschedule)
{
  mdd_t *hint;      /* to iterate over hintsArray */
  int   hintnr;     /* idem                       */
  Ctlp_Approx_t resultApproxType;

  assert(hintType == Mc_None_c || hintsArray != NIL(Fsm_HintsArray_t));
  
  if(hintType != Mc_Global_c)
    return EvaluateFormulaRecur(fsm, ctlFormula, fairStates,
                                fairCondition, careStatesArray,
                                earlyTermination, hintsArray, hintType,
                                Ctlp_Exact_c, &resultApproxType,
                                verbosity, dcLevel,
                                buildOnionRing, GSHschedule);
  else{
    mdd_t *result = NIL(mdd_t);
    Ctlp_Approx_t approx;

    if(verbosity >= McVerbosityMax_c)
      fprintf(vis_stdout, "--Using global hints\n");
    
    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
      if(result != NIL(mdd_t))
        mdd_free(result);
      
      if(verbosity >= McVerbosityMax_c)
        fprintf(vis_stdout, "--Instantiating global hint %d\n", hintnr);

      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c,
                          (verbosity >= McVerbosityMax_c));

      approx = mdd_is_tautology(hint, 1) ? Ctlp_Exact_c : Ctlp_Underapprox_c;

      result = EvaluateFormulaRecur(fsm, ctlFormula, fairStates,
                                    fairCondition, careStatesArray,
                                    earlyTermination, hintsArray, hintType,
                                    approx, &resultApproxType, verbosity,
                                    dcLevel, buildOnionRing, GSHschedule); 
      /* TBD: take into account (early) termination here */
    }
    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));

    return result;
  }

} /* Mc_FsmEvaluateFormula */


mdd_t *
Mc_FsmEvaluateEXFormula(
  Fsm_Fsm_t *modelFsm,
  mdd_t *targetMdd,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  mdd_t *fromLowerBound;
  mdd_t *fromUpperBound;
  mdd_t *result;
  Img_ImageInfo_t * imageInfo;
  
  if(Fsm_FsmReadUseUnquantifiedFlag(modelFsm))
    imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 1, 0);
  else
    imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);

  /*
   * The lower bound is the conjunction of the fair states,
   * and the target states.
   */
  fromLowerBound = mdd_and(targetMdd, fairStates, 1, 1);
  /*
   * The upper bound is the same as the lower bound.
   */
  fromUpperBound = mdd_dup(fromLowerBound);

  result = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
                fromLowerBound, fromUpperBound, careStatesArray);
  mdd_free(fromLowerBound);
  mdd_free(fromUpperBound);

  if (verbosity == McVerbosityMax_c) {
    static int refCount=0;
    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
    mdd_t *tmpMdd = careStatesArray ?
        mdd_and_array(result, careStatesArray, 1, 1) : mdd_dup(result);
    fprintf(vis_stdout, "--EX called %d (bdd_size - %d)\n", ++refCount,
            mdd_size(result));
    fprintf(vis_stdout, "--There are %.0f care states satisfying EX formula\n",
            mdd_count_onset(mddMgr, tmpMdd, psVars));
    mdd_free(tmpMdd);
  }

  return result;

} /* Mc_FsmEvaluateEXFormula */


mdd_t *
Mc_FsmEvaluateMXFormula(
  Fsm_Fsm_t *modelFsm,
  mdd_t *targetMdd,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  mdd_t *resultBar, *result;

  result = Mc_FsmEvaluateEXFormula(modelFsm, targetMdd, fairStates,
                                 careStatesArray, verbosity, dcLevel);

  if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
    resultBar = Mc_QuantifyInputFAFW(modelFsm, result);
    mdd_free(result);
    result = resultBar;
  }

  return(result);
}

bdd_t *
Mc_QuantifyInputFAFW(Fsm_Fsm_t *fsm, bdd_t *result) 
{
  bdd_t *uniCube, *extCube, *newResult;
  bdd_t *oneMdd, *notResult;
  mdd_manager *mgr = Fsm_FsmReadMddManager(fsm);

  oneMdd = mdd_one(mgr);
  uniCube = Fsm_FsmReadUniQuantifyInputCube(fsm);
  extCube = Fsm_FsmReadExtQuantifyInputCube(fsm);
  if(!mdd_equal(uniCube, oneMdd)) {
    notResult = bdd_not(result);
    newResult = bdd_smooth_with_cube(notResult, uniCube); 
    bdd_free(notResult);
    result    = bdd_not(newResult);
    bdd_free(newResult);
  }
  else {
    result = mdd_dup(result);
  }
  mdd_free(oneMdd);
  return(result);
}


mdd_t *
Mc_FsmEvaluateEYFormula(
  Fsm_Fsm_t *modelFsm,
  mdd_t *targetMdd,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  mdd_t *fromLowerBound;
  mdd_t *fromUpperBound;
  mdd_t *result;

  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);

  /*
   * The lower bound is the conjunction of the fair states,
   * and the target states.
   */
  fromLowerBound = mdd_and(targetMdd, fairStates, 1, 1);
  /*
   * The upper bound is the same as the lower bound.
   */
  fromUpperBound = fromLowerBound;

  result = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
                fromLowerBound, fromUpperBound, careStatesArray);
  mdd_free(fromLowerBound);

  if (verbosity == McVerbosityMax_c) {
    static int refCount=0;
    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
    mdd_t *tmpMdd = careStatesArray ?
        mdd_and_array(result, careStatesArray, 1, 1) : mdd_dup(result);
    fprintf(vis_stdout, "--EY called %d (bdd_size - %d)\n", ++refCount,
            mdd_size(result));
    fprintf(vis_stdout, "--There are %.0f care states satisfying EY formula\n",
            mdd_count_onset(mddMgr, tmpMdd, psVars));
    mdd_free(tmpMdd);
  }

  return result;

} /* Mc_FsmEvaluateEYFormula */


mdd_t *
Mc_FsmEvaluateEUFormula(
  Fsm_Fsm_t *fsm,
  mdd_t *invariant,
  mdd_t *target,
  mdd_t *underapprox,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  Fsm_HintsArray_t *hintsArray,
  Mc_GuidedSearch_t hintType,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint)
{
  /* should be strengthened to check that rings supply a correct explanation.
   */
  /*check out
   *  assert(underapprox == NULL || onionRings == NULL ||
   *     array_n(onionRings) != 0);  */
 
  if(hintType != Mc_Local_c)
    /* postcondition: rings should explain how to get from return value to
     * target.
     */
    return McEvaluateEUFormulaWithGivenTR(fsm, invariant, target,
                                          underapprox, fairStates,
                                          careStatesArray,
                                          earlyTermination, onionRings,
                                          verbosity, dcLevel, fixpoint);  
  else{
    mdd_t *iterate, *newiterate;
    mdd_t *hint;
    int hintnr;

    if(verbosity >= McVerbosityMax_c)
        fprintf(vis_stdout, "--Using local hints\n");

    if(underapprox != NIL(mdd_t))
      iterate = mdd_dup(underapprox);
    else
      iterate = mdd_zero(Fsm_FsmReadMddManager(fsm));

    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
        if(verbosity >= McVerbosityMax_c)
            fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c,
                          (verbosity >= McVerbosityMax_c));
      
      newiterate =
        McEvaluateEUFormulaWithGivenTR(fsm, invariant, target, iterate,
                                       fairStates, careStatesArray,
                                       earlyTermination, onionRings,
                                       verbosity, dcLevel, fixpoint);    
      mdd_free(iterate);
      iterate = newiterate;

      /* check if we can terminate without considering all hints */ 
      if(mdd_is_tautology(iterate, 1)){
        *fixpoint = 1;
        break;
      }
      if(McCheckEarlyTerminationForUnderapprox(earlyTermination, iterate,
                                               careStatesArray)){ 
        *fixpoint = 0;
        break;
      }

    }/* for all hints */
    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));

    /* postcondition: rings should explain how to get from return value to
     * target.
     */
    return iterate;
  }/* if hinttype */

} /* Mc_FsmEvaluateEUFormula */


mdd_t *
Mc_FsmEvaluateESFormula(
  Fsm_Fsm_t *fsm,
  mdd_t *invariant,
  mdd_t *source,
  mdd_t *underapprox,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  Fsm_HintsArray_t *hintsArray,
  Mc_GuidedSearch_t hintType,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint)
{
  /* should be strengthened to check that rings supply a correct explanation.
   */
  assert(underapprox == NULL || onionRings == NULL ||
         array_n(onionRings) != 0);

  if(hintType != Mc_Local_c)
    /* postcondition: rings should explain how to get from return value to
     * target.
     */
    return McEvaluateESFormulaWithGivenTR(fsm, invariant, source,
                                          underapprox, fairStates,
                                          careStatesArray,
                                          earlyTermination, onionRings,
                                          verbosity, dcLevel, fixpoint);  
  else{
    mdd_t *iterate, *newiterate;
    mdd_t *hint;
    int hintnr;

    if(verbosity >= McVerbosityMax_c)
        fprintf(vis_stdout, "--Using local hints\n");

    if(underapprox != NIL(mdd_t))
      iterate = mdd_dup(underapprox);
    else
      iterate = mdd_zero(Fsm_FsmReadMddManager(fsm));

    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
        if(verbosity >= McVerbosityMax_c)
            fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c,
                          (verbosity >= McVerbosityMax_c));
      
      newiterate =
        McEvaluateESFormulaWithGivenTR(fsm, invariant, source, iterate,
                                       fairStates, careStatesArray,
                                       earlyTermination, onionRings,
                                       verbosity, dcLevel, fixpoint);    
      mdd_free(iterate);
      iterate = newiterate;

      /* check if we can terminate without considering all hints */ 
      if(mdd_is_tautology(iterate, 1)){
        *fixpoint = 1;
        break;
      }
      if(McCheckEarlyTerminationForUnderapprox(earlyTermination, iterate,
                                               careStatesArray)){ 
        *fixpoint = 0;
        break;
      }

    }/* for all hints */
    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));

    /* postcondition: rings should explain how to get from return value to
     * target.
     */

    return iterate;
  }/* if hinttype */

} /* Mc_FsmEvaluateESFormula */

mdd_t *
Mc_FsmEvaluateAUFormula(
  Fsm_Fsm_t *fsm,
  mdd_t *invariant,
  mdd_t *target,
  mdd_t *underapprox,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  Fsm_HintsArray_t *hintsArray,
  Mc_GuidedSearch_t hintType,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint)
{

  return McEvaluateAUFormulaWithGivenTR(fsm, invariant, target,
                                        underapprox, fairStates,
                                        careStatesArray,
                                        earlyTermination, onionRings,
                                        verbosity, dcLevel, fixpoint);

}



mdd_t *
Mc_FsmEvaluateEGFormula(
  Fsm_Fsm_t *fsm,
  mdd_t *invariant,
  mdd_t *overapprox,
  mdd_t *fairStates,
  Fsm_Fairness_t *modelFairness,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  Fsm_HintsArray_t *hintsArray,
  Mc_GuidedSearch_t hintType,
  array_t **pOnionRingsArrayForDbg,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint,
  Mc_GSHScheduleType GSHschedule)
{
  /* Illegal to pass in onion rings. */
#if 0
  assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
  *pOnionRingsArrayForDbg == NIL(array_t) ||
  array_n(*pOnionRingsArrayForDbg) == 0);
#endif
  if(hintType != Mc_Local_c)
    if (GSHschedule == McGSH_old_c) {
      return McEvaluateEGFormulaWithGivenTR(fsm, invariant, overapprox,
                                            fairStates,
                                            modelFairness, careStatesArray,
                                            earlyTermination,
                                            pOnionRingsArrayForDbg,
                                            verbosity,
                                            dcLevel, fixpoint);
    } else {
      return McFsmEvaluateEGFormulaUsingGSH(fsm, invariant, overapprox,
                                            fairStates,
                                            modelFairness, careStatesArray,
                                            earlyTermination,
                                            pOnionRingsArrayForDbg, verbosity,
                                            dcLevel, fixpoint, GSHschedule);
    }
  else {
    mdd_t *iterate, *newiterate;
    mdd_t *hint;
    int hintnr;
    boolean useRings;

    useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
                *pOnionRingsArrayForDbg != NIL(array_t));
    
    if(verbosity >= McVerbosityMax_c)
        fprintf(vis_stdout, "** mc Info: Using local hints\n");

    if(overapprox != NIL(mdd_t))
      iterate = mdd_dup(overapprox);
    else
      iterate = mdd_one(Fsm_FsmReadMddManager(fsm));
    
    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
        if(verbosity >= McVerbosityMax_c)
            fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Overapprox_c,
                          (verbosity >= McVerbosityMax_c));

      /* old onionrings go stale.  Fry 'em */
      if(useRings){
        mdd_array_array_free(*pOnionRingsArrayForDbg);
        *pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
      }

      if (GSHschedule == McGSH_old_c) {
        newiterate =
          McEvaluateEGFormulaWithGivenTR(fsm, invariant, iterate, fairStates,
                                         modelFairness, careStatesArray,
                                         earlyTermination,
                                         pOnionRingsArrayForDbg,
                                         verbosity, dcLevel, fixpoint);
      } else {
        newiterate =
          McFsmEvaluateEGFormulaUsingGSH(fsm, invariant, iterate,
                                         fairStates,
                                         modelFairness, careStatesArray,
                                         earlyTermination,
                                         pOnionRingsArrayForDbg, verbosity,
                                         dcLevel, fixpoint, GSHschedule);
      }
      mdd_free(iterate);
      iterate = newiterate;

      /* check if we can terminate without considering all hints */ 
      if(mdd_is_tautology(iterate, 0)){
        *fixpoint = 1;
        break;
      }
      if(McCheckEarlyTerminationForOverapprox(earlyTermination, iterate,
                                              careStatesArray)){  
        *fixpoint = 0;
        break;
      }

    } /* For all hints */
    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));

    return iterate;
  }/* if hinttype */

} /* Mc_FsmEvaluateEGFormula */


mdd_t *
Mc_FsmEvaluateEHFormula(
  Fsm_Fsm_t *fsm,
  mdd_t *invariant,
  mdd_t *overapprox,
  mdd_t *fairStates,
  Fsm_Fairness_t *modelFairness,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  Fsm_HintsArray_t *hintsArray,
  Mc_GuidedSearch_t hintType,
  array_t **pOnionRingsArrayForDbg,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint,
  Mc_GSHScheduleType GSHschedule)
{
  /* Illegal to pass in onion rings. */
  assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
         *pOnionRingsArrayForDbg == NIL(array_t) ||
         array_n(*pOnionRingsArrayForDbg) == 0);

  if(hintType != Mc_Local_c)
    if (GSHschedule == McGSH_old_c) {
      return McEvaluateEHFormulaWithGivenTR(fsm, invariant, overapprox,
                                            fairStates,
                                            modelFairness, careStatesArray,
                                            earlyTermination,
                                            pOnionRingsArrayForDbg,
                                            verbosity,
                                            dcLevel, fixpoint);
    } else {
      return McFsmEvaluateEHFormulaUsingGSH(fsm, invariant, overapprox,
                                            fairStates,
                                            modelFairness, careStatesArray,
                                            earlyTermination,
                                            pOnionRingsArrayForDbg, verbosity,
                                            dcLevel, fixpoint, GSHschedule);
    }
  else {
    mdd_t *iterate, *newiterate;
    mdd_t *hint;
    int hintnr;
    boolean useRings;

    useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
                *pOnionRingsArrayForDbg != NIL(array_t));
    
    if(verbosity >= McVerbosityMax_c)
        fprintf(vis_stdout, "** mc Info: Using local hints\n");

    if(overapprox != NIL(mdd_t))
      iterate = mdd_dup(overapprox);
    else
      iterate = mdd_one(Fsm_FsmReadMddManager(fsm));
    
    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
        if(verbosity >= McVerbosityMax_c)
            fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Overapprox_c,
                          (verbosity >= McVerbosityMax_c));

      /* old onionrings go stale.  Fry 'em */
      if(useRings){
        mdd_array_array_free(*pOnionRingsArrayForDbg);
        *pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
      }

      if (GSHschedule == McGSH_old_c) {
        newiterate =
          McEvaluateEHFormulaWithGivenTR(fsm, invariant, iterate, fairStates,
                                         modelFairness, careStatesArray,
                                         earlyTermination,
                                         pOnionRingsArrayForDbg,
                                         verbosity, dcLevel, fixpoint);
      } else {
        newiterate =
          McFsmEvaluateEHFormulaUsingGSH(fsm, invariant, iterate,
                                         fairStates,
                                         modelFairness, careStatesArray,
                                         earlyTermination,
                                         pOnionRingsArrayForDbg, verbosity,
                                         dcLevel, fixpoint, GSHschedule);
      }
      mdd_free(iterate);
      iterate = newiterate;

      /* check if we can terminate without considering all hints */ 
      if(mdd_is_tautology(iterate, 0)){
        *fixpoint = 1;
        break;
      }
      if(McCheckEarlyTerminationForOverapprox(earlyTermination, iterate,
                                              careStatesArray)){  
        *fixpoint = 0;
        break;
      }

    } /* For all hints */
    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));

    return iterate;
  }/* if hinttype */

} /* Mc_FsmEvaluateEHFormula */


mdd_t *
Mc_FsmEvaluateFwdUFormula(
  Fsm_Fsm_t *modelFsm,
  mdd_t *targetMdd,
  mdd_t *invariantMdd,
  mdd_t *fairStates,
  array_t *careStatesArray,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  mdd_t *aMdd;
  mdd_t *bMdd;
  mdd_t *cMdd;
  mdd_t *resultMdd;
  mdd_t *ringMdd;
  int nImgComps;

  /*                                                        t
  ** E[p U q]      = lfp Z[q V (p ^ EX(Z))]   :   p p ... p q
  ** FwdUntil(p,q) = lfp Z[p V EY(Z ^ q)]     :             pq q q ... q
  */

  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
  resultMdd = mdd_and(targetMdd, fairStates, 1, 1);
  ringMdd = mdd_dup(resultMdd);

  /* if until is trivially satisfied, */
  if (onionRings) {
    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
  }
  if (mdd_is_tautology(fairStates, 1)) {
    if (mdd_equal_mod_care_set_array(invariantMdd, resultMdd, careStatesArray))
    { 
      bdd_free(ringMdd);
      return(resultMdd);
    }
  } else {
    bdd_t *trivialCheck = mdd_and(invariantMdd, fairStates, 1, 1);
    if (mdd_equal_mod_care_set_array(trivialCheck, resultMdd, careStatesArray)) {
      bdd_free(trivialCheck);
      bdd_free(ringMdd);
      return(resultMdd);
    }
    bdd_free(trivialCheck);
  }

  while (TRUE) {
    aMdd = mdd_and(ringMdd, invariantMdd, 1, 1);
    mdd_free(ringMdd);
    bMdd = Mc_FsmEvaluateEYFormula(modelFsm, aMdd, fairStates, careStatesArray,
                                   verbosity, dcLevel);
    mdd_free(aMdd);
    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
    mdd_free(bMdd);

    if (mdd_equal_mod_care_set_array(cMdd, resultMdd, careStatesArray)) {
      mdd_free(cMdd);
      break;
    }

    if (dcLevel >= McDcLevelRchFrontier_c) {
      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
      ringMdd = bdd_between(tmpMdd, cMdd);
      if (verbosity == McVerbosityMax_c) {
        fprintf(vis_stdout,
          "-- FwdU |A(n+1)-A(n)| = %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
          mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
      }
      mdd_free(tmpMdd);
    }
    else {
      ringMdd = mdd_dup(cMdd);
      if (verbosity == McVerbosityMax_c) {
        fprintf(vis_stdout, "-- FwdU |ringMdd| = %d\n", mdd_size(ringMdd));
      }
    }

    mdd_free(resultMdd);
    resultMdd = cMdd;
    if (onionRings) {
      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
    }
  } /* while(!termination) for LFP */

  /* Print some debug info */
  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
    static int refCount=0;
    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);

    if (verbosity == McVerbosityMax_c) {
      mdd_t *tmpMdd = careStatesArray ?
                      mdd_and_array(resultMdd, careStatesArray, 1, 1) :
                      mdd_dup(resultMdd);
      fprintf(vis_stdout, "--FwdU called %d (bdd_size - %d)\n",
                ++refCount, mdd_size(resultMdd));
      fprintf(vis_stdout,
                "--There are %.0f care states satisfying FwdU formula\n",
                mdd_count_onset(mddMgr, tmpMdd, psVars));
#ifdef DEBUG_MC
      /* The following 2 lines are just for debug */
      fprintf(vis_stdout, "FwdU satisfying minterms :\n");
      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
      mdd_free(tmpMdd);
    } else {
      fprintf(vis_stdout,
                "--There are %.0f states satisfying FwdU formula\n",
                mdd_count_onset(mddMgr, resultMdd, psVars));
    }
    fprintf(vis_stdout, "--FwdU: %d image computations\n",
      Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
  }

  return resultMdd;
}


mdd_t *
Mc_FsmEvaluateFwdGFormula(
  Fsm_Fsm_t *modelFsm,
  mdd_t *targetMdd,
  mdd_t *invariantMdd,
  mdd_t *fairStates,
  Fsm_Fairness_t *modelFairness,
  array_t *careStatesArray,
  array_t *onionRingsArrayForDbg,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  mdd_t *resultMdd, *invariant;
  array_t *onionRings;
  int nImgComps;

  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
  onionRings = NIL(array_t);

  invariant = McForwardReachable(modelFsm, targetMdd, invariantMdd, fairStates,
                                 careStatesArray, onionRings, verbosity,
                                 dcLevel);
  resultMdd = Mc_FsmEvaluateFwdEHFormula(modelFsm, invariant, fairStates,
                                         modelFairness, careStatesArray,
                                         onionRingsArrayForDbg, verbosity,
                                         dcLevel);
  mdd_free(invariant);

  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
    fprintf(vis_stdout, "--FwdG: %d image computations\n",
      Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
  }
#ifdef DEBUG_MC
  /* The following 2 lines are just for debug */
  if ((verbosity == McVerbosityMax_c)) {
    fprintf(vis_stdout, "FwdG satisfying minterms :\n");
    (void)_McPrintSatisfyingMinterms(resultMdd, modelFsm);
  }
#endif
  return resultMdd;
}



mdd_t *
Mc_FsmEvaluateFwdEHFormula(
  Fsm_Fsm_t *modelFsm,
  mdd_t *invariantMdd,
  mdd_t *fairStates,
  Fsm_Fairness_t *modelFairness,
  array_t *careStatesArray,
  array_t *onionRingsArrayForDbg,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  int i;
  array_t *onionRings = NIL(array_t);
  array_t *tmpOnionRingsArrayForDbg = NIL(array_t);
  mdd_manager *mddManager = Fsm_FsmReadMddManager(modelFsm);
  mdd_t *mddOne = mdd_one(mddManager);
  mdd_t *Zmdd;
  int nIterations = 0;
  int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);

  /*
  **  EG(f) = gfp Z[f ^ EX(Z)]
  **  EH(f) = gfp Z[f ^ EY(Z)]
  **
  **  EcG(f) = gfp Z[f ^ EX( ^ E[Z U Z ^ c])]
  **                        c<C
  **  EcH(f) = gfp Z[f ^ EY( ^ Reachable(c,Z))]
  **                        c<C
  **  Reachable(p,q) = FwdUntil(p,q) ^ q
  */

  array_t *buchiFairness = array_alloc(mdd_t *, 0);
  if (modelFairness) {
    if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
      (void) fprintf(vis_stdout,
         "** mc error: non-Buechi fairness constraints not supported\n");
      return NIL(mdd_t);
    }
    else {
      int j;
      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
      for (j = 0; j < numBuchi; j++) {
        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
                                                careStatesArray, dcLevel);
        array_insert_last(mdd_t *, buchiFairness, tmpMdd);
      }
    }
  }
  else {
    array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager));
  }

  if (onionRingsArrayForDbg !=NIL(array_t)) {
    tmpOnionRingsArrayForDbg = array_alloc(array_t *, 0);
  }

  Zmdd = mdd_dup(invariantMdd);
  while (TRUE) {
    mdd_t *ZprimeMdd = mdd_dup(Zmdd);
    mdd_t *conjunctsMdd = NIL(mdd_t);
    mdd_t *AAmdd = mdd_dup(Zmdd);

    nIterations++;
    for (i = 0; i < array_n(buchiFairness); i++) {
      mdd_t *aMdd, *bMdd;
      mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i);

      if (tmpOnionRingsArrayForDbg) {
        onionRings = array_alloc(mdd_t *, 0);
        array_insert_last(array_t *, tmpOnionRingsArrayForDbg, onionRings);
      }

      aMdd = McForwardReachable(modelFsm, FiMdd, AAmdd, mddOne, careStatesArray,
                                onionRings, verbosity, dcLevel);
      bMdd = Mc_FsmEvaluateEYFormula(modelFsm, aMdd, mddOne, careStatesArray,
                                     verbosity, dcLevel);
      mdd_free(aMdd);

      if (conjunctsMdd == NIL(mdd_t)) {
        conjunctsMdd = mdd_dup(bMdd);
      }
      else {
        mdd_t *tmpMdd = mdd_and(bMdd, conjunctsMdd, 1, 1);
        mdd_free(conjunctsMdd);
        conjunctsMdd = tmpMdd;
      }
      mdd_free(AAmdd); AAmdd = mdd_and(conjunctsMdd, invariantMdd, 1, 1);
      mdd_free(bMdd);
    }
    mdd_free(AAmdd);

    mdd_free(ZprimeMdd);
    ZprimeMdd = mdd_and(invariantMdd, conjunctsMdd, 1, 1);
    mdd_free(conjunctsMdd);

    if (mdd_equal_mod_care_set_array(ZprimeMdd, Zmdd, careStatesArray)) {
      mdd_free(ZprimeMdd);
      break;
    }

    mdd_free(Zmdd);
    Zmdd = ZprimeMdd;

    if (tmpOnionRingsArrayForDbg) {
      arrayForEachItem(array_t *, tmpOnionRingsArrayForDbg, i, onionRings) {
        mdd_array_free(onionRings);
      }
      array_free(tmpOnionRingsArrayForDbg);
      tmpOnionRingsArrayForDbg = array_alloc(array_t *, 0);
    }
  }

  if (onionRingsArrayForDbg != NIL(array_t)) {
    arrayForEachItem(array_t *, tmpOnionRingsArrayForDbg, i, onionRings) {
      array_insert_last(array_t *, onionRingsArrayForDbg, onionRings);
    }
    array_free(tmpOnionRingsArrayForDbg);
  }

  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
    if (onionRingsArrayForDbg) {
      for (i = 0; i < array_n(onionRingsArrayForDbg); i++) {
        int j;
        mdd_t *Fi = array_fetch(mdd_t *, buchiFairness, i);
        array_t *onionRings = array_fetch(array_t *, onionRingsArrayForDbg, i);
        for (j = 0; j < array_n(onionRings); j++) {
          mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
          if (j == 0) {
            if (!mdd_lequal(ring, Fi, 1, 1)) {
              fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
              fprintf(vis_stderr,
                      "inner most ring not in Fi(fairness constraint).\n");
            }
          }
          if (!mdd_lequal(ring, Zmdd, 1, 1)) {
            fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
            fprintf(vis_stderr, "onion ring of last FwdU fails invariant\n");
          }
        }
      }
    }

    if (verbosity == McVerbosityMax_c) {
      mdd_t *tmpMdd = careStatesArray ?
                      mdd_and_array(Zmdd, careStatesArray, 1, 1) :
                      mdd_dup(Zmdd);
      fprintf(vis_stdout,
              "--There are %.0f care states satisfying EH formula\n",
              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd,
                              Fsm_FsmReadPresentStateVars(modelFsm)));
#ifdef DEBUG_MC
      /* The following 2 lines are just for debug */
      fprintf(vis_stdout, "EH satisfying minterms :\n");
      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
      mdd_free(tmpMdd);
    } else {
      fprintf(vis_stdout, "--There are %.0f states satisfying EH formula\n",
              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), Zmdd,
                              Fsm_FsmReadPresentStateVars(modelFsm)));
    }

    fprintf(vis_stdout, "--EH: %d iterations, %d image computations\n",
      nIterations, Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
  }

  mdd_array_free(buchiFairness);
  mdd_free(mddOne);

  return Zmdd;

} /* Mc_FsmEvaluateFwdEHFormula */


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

mdd_t *
McEvaluateEUFormulaWithGivenTR(
  Fsm_Fsm_t *modelFsm,
  mdd_t *invariantMdd,
  mdd_t *targetMdd,
  mdd_t *underapprox,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint
  )
{
  mdd_t *aMdd;
  mdd_t *bMdd;
  mdd_t *cMdd;
  mdd_t *resultMdd;
  mdd_t *ringMdd;
  int nPreComps;
  boolean term_tautology = FALSE; /* different termination conditions */
  boolean term_early     = FALSE; 
  boolean term_fixpoint  = FALSE; 

  nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
  resultMdd = mdd_and(targetMdd, fairStates, 1, 1);

  if(underapprox != NIL(mdd_t)){
    mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
    mdd_free(resultMdd);
    resultMdd = tmp;
  }

  ringMdd = mdd_dup(resultMdd);

  if (onionRings) {
    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
  }
  
  /* if until is trivially satisfied, or
     the early termination condition holds*/ 
  {
    bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
    boolean trivial;

    trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
                                            1, 1, careStatesArray);
    /* the lequal also takes care of the case where result = 1 */
    if(trivial ||
       McCheckEarlyTerminationForUnderapprox(earlyTermination,
                                             resultMdd,
                                             careStatesArray)){
      bdd_free(fairInvariantStates);
      bdd_free(ringMdd);

      /* trivially satisfied means that the fixpoint is complete.  If this
         information is requested, give it. */
      if(fixpoint != NIL(boolean))
        *fixpoint = trivial;
      return(resultMdd);
    }
    bdd_free(fairInvariantStates);
  }

  /* The LFP loop */
  while (!term_fixpoint && !term_tautology && !term_early) {
    /* If dclevel is maximal, ringbdd is between the frontier and the
       reached set */
    aMdd = Mc_FsmEvaluateEXFormula(modelFsm, ringMdd, fairStates,
                                   careStatesArray, verbosity, dcLevel);
    mdd_free(ringMdd);

    bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
    mdd_free(aMdd);

    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
    mdd_free(bMdd);

    /* Can we stop?  The tautology condition can be weakened to
       cMdd <= careStatesArray */
    term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
                                                 careStatesArray);
    if(!term_fixpoint)
      term_tautology = mdd_is_tautology(cMdd, 1);
    if(!term_fixpoint && !term_tautology)
      term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, 
                                                         cMdd,
                                                         careStatesArray);

    /* Print some debug info, and set ringmdd */
    if (dcLevel >= McDcLevelRchFrontier_c) {
      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
      ringMdd = bdd_between(tmpMdd, cMdd);
      if (verbosity == McVerbosityMax_c) {
        fprintf(vis_stdout,
                "--EU |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
                mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
      }
      mdd_free(tmpMdd);
    }
    else {
      ringMdd = mdd_dup(cMdd);
      if (verbosity == McVerbosityMax_c) {
          fprintf(vis_stdout, "-- EU |ringMdd| = %d\n", mdd_size(ringMdd));
      }
    }

    mdd_free(resultMdd);
    resultMdd = cMdd;
    /* add onion ring unless fixpoint reached */
    if (!term_fixpoint && onionRings != NIL(array_t)) {
      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
    }
  } /* while(!termination) for LFP */

  mdd_free(ringMdd);

  /* Print some debug info */
  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
    static int refCount=0;
    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);

    if (verbosity == McVerbosityMax_c) {
      mdd_t *tmpMdd = careStatesArray ?
                      mdd_and_array(resultMdd, careStatesArray, 1, 1) :
                      mdd_dup(resultMdd);
      fprintf(vis_stdout, "--EU called %d (bdd_size - %d)\n", ++refCount,
              mdd_size(resultMdd));
      fprintf(vis_stdout,
              "--There are %.0f care states satisfying EU formula\n",
              mdd_count_onset(mddMgr, tmpMdd, psVars));
#ifdef DEBUG_MC
      /* The following 2 lines are just for debug */
      fprintf(vis_stdout, "EU satisfying minterms :\n");
      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
      mdd_free(tmpMdd);
    } else {
      fprintf(vis_stdout,
              "--There are %.0f states satisfying EU formula\n",
              mdd_count_onset(mddMgr, resultMdd, psVars));
    }

    fprintf(vis_stdout, "--EU: %d preimage computations\n",
      Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
  }

  if(fixpoint != NIL(boolean))
    *fixpoint = term_fixpoint || term_tautology;
  return resultMdd;

} /* McEvaluateEUFormulaWithGivenTR */


mdd_t *
McEvaluateESFormulaWithGivenTR(
  Fsm_Fsm_t *modelFsm,
  mdd_t *invariantMdd,
  mdd_t *sourceMdd,
  mdd_t *underapprox,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint
  )
{
  mdd_t *aMdd;
  mdd_t *bMdd;
  mdd_t *cMdd;
  mdd_t *resultMdd;
  mdd_t *ringMdd;
  int nImgComps;
  boolean term_tautology = FALSE; /* different termination conditions */
  boolean term_early     = FALSE; 
  boolean term_fixpoint  = FALSE; 

  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
  resultMdd = mdd_and(sourceMdd, fairStates, 1, 1);

  if(underapprox != NIL(mdd_t)){
    mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
    mdd_free(resultMdd);
    resultMdd = tmp;
  }

  ringMdd = mdd_dup(resultMdd);

  if (onionRings) {
    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
  }
  
  /* if Since is trivially satisfied, or
     the early termination condition holds*/ 
  {
    bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
    boolean trivial;

    trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
                                            1, 1, careStatesArray);
    /* the lequal also takes care of the case where result = 1 */
    if(trivial ||
       McCheckEarlyTerminationForUnderapprox(earlyTermination,
                                             resultMdd,
                                             careStatesArray)){
      bdd_free(fairInvariantStates);
      bdd_free(ringMdd);

      /* trivially satisfied means that the fixpoint is complete.  If this
         information is requested, give it. */
      if(fixpoint != NIL(boolean))
        *fixpoint = trivial;
      return(resultMdd);
    }
    bdd_free(fairInvariantStates);
  }

  /* The LFP loop */
  while (!term_fixpoint && !term_tautology && !term_early) {
    /* If dclevel is maximal, ringbdd is between the frontier and the
       reached set */
    aMdd = Mc_FsmEvaluateEYFormula(modelFsm, ringMdd, fairStates,
                                   careStatesArray, verbosity, dcLevel);
    mdd_free(ringMdd);

    bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
    mdd_free(aMdd);

    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
    mdd_free(bMdd);

    /* Can we stop?  The tautology condition can be weakened to
       cMdd <= careStatesArray */
    term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
                                                 careStatesArray);
    if(!term_fixpoint)
      term_tautology = mdd_is_tautology(cMdd, 1);
    if(!term_fixpoint && !term_tautology)
      term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, 
                                                         cMdd,
                                                         careStatesArray);

    /* Print some debug info, and set ringmdd */
    if (dcLevel >= McDcLevelRchFrontier_c) {
      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
      ringMdd = bdd_between(tmpMdd, cMdd);
      if (verbosity == McVerbosityMax_c) {
        fprintf(vis_stdout,
                "--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
                mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
      }
      mdd_free(tmpMdd);
      }
    else {
      ringMdd = mdd_dup(cMdd);
      if (verbosity == McVerbosityMax_c) {
          fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd));
      }
    }

    mdd_free(resultMdd);
    resultMdd = cMdd;
    /* add onion ring unless fixpoint reached */
    if (!term_fixpoint && onionRings != NIL(array_t)) {
      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
    }
  } /* while(!termination) for LFP */

  mdd_free(ringMdd);

  /* Print some debug info */
  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
    static int refCount=0;
    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);

    if (verbosity == McVerbosityMax_c) {
      mdd_t *tmpMdd = careStatesArray ?
                      mdd_and_array(resultMdd, careStatesArray, 1, 1) :
                      mdd_dup(resultMdd);
      fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount,
              mdd_size(resultMdd));
      fprintf(vis_stdout,
              "--There are %.0f care states satisfying ES formula\n",
              mdd_count_onset(mddMgr, tmpMdd, psVars));
#ifdef DEBUG_MC
      /* The following 2 lines are just for debug */
      fprintf(vis_stdout, "ES satisfying minterms :\n");
      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
      mdd_free(tmpMdd);
    } else {
      fprintf(vis_stdout,
              "--There are %.0f states satisfying ES formula\n",
              mdd_count_onset(mddMgr, resultMdd, psVars));
    }

    fprintf(vis_stdout, "--ES: %d image computations\n",
      Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
  }

  if(fixpoint != NIL(boolean))
    *fixpoint = term_fixpoint || term_tautology;
  return resultMdd;

} /* McEvaluateESFormulaWithGivenTR */


mdd_t *
McEvaluateESFormulaWithGivenTRWithTarget(
  Fsm_Fsm_t *modelFsm,
  mdd_t *invariantMdd,
  mdd_t *sourceMdd,
  mdd_t *targetMdd,
  mdd_t *underapprox,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint
  )
{
  mdd_t *aMdd;
  mdd_t *bMdd;
  mdd_t *cMdd;
  mdd_t *resultMdd;
  mdd_t *ringMdd;
  mdd_t *zeroMdd;
  int nImgComps;
  boolean term_tautology = FALSE; /* different termination conditions */
  boolean term_early     = FALSE; 
  boolean term_fixpoint  = FALSE; 

  mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);

  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
  resultMdd = mdd_and(sourceMdd, fairStates, 1, 1);

  if(underapprox != NIL(mdd_t)){
    mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
    mdd_free(resultMdd);
    resultMdd = tmp;
  }

  ringMdd = mdd_dup(resultMdd);
  zeroMdd = mdd_zero(mddMgr);

  if (onionRings) {
    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
  }
  
  /* if Since is trivially satisfied, or
     the early termination condition holds*/ 
  {
    bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
    boolean trivial;

    trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
                                            1, 1, careStatesArray);
    /* the lequal also takes care of the case where result = 1 */
    if(trivial ||
       McCheckEarlyTerminationForUnderapprox(earlyTermination,
                                             resultMdd,
                                             careStatesArray)){
      bdd_free(fairInvariantStates);
      bdd_free(ringMdd);

      /* trivially satisfied means that the fixpoint is complete.  If this
         information is requested, give it. */
      if(fixpoint != NIL(boolean))
        *fixpoint = trivial;
      return(resultMdd);
    }
    bdd_free(fairInvariantStates);
  }

  /* The LFP loop */
  while (!term_fixpoint && !term_tautology && !term_early) {
    /* If dclevel is maximal, ringbdd is between the frontier and the
       reached set */
    aMdd = Mc_FsmEvaluateEYFormula(modelFsm, ringMdd, fairStates,
                                   careStatesArray, verbosity, dcLevel);
    mdd_free(ringMdd);

    bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
    mdd_free(aMdd);

    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
    mdd_free(bMdd);

    /* Can we stop?  The tautology condition can be weakened to
       cMdd <= careStatesArray */
    term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
                                                 careStatesArray);
    if(!term_fixpoint)
      term_tautology = mdd_is_tautology(cMdd, 1);
    if(!term_fixpoint && !term_tautology)
      term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, 
                                                         cMdd,
                                                         careStatesArray);

    /* Print some debug info, and set ringmdd */
    if (dcLevel >= McDcLevelRchFrontier_c) {
      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
      ringMdd = bdd_between(tmpMdd, cMdd);
      if (verbosity == McVerbosityMax_c) {
        fprintf(vis_stdout,
                "--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
                mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
      }
      mdd_free(tmpMdd);
      }
    else {
      ringMdd = mdd_dup(cMdd);
      if (verbosity == McVerbosityMax_c) {
          fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd));
      }
    }

    mdd_free(resultMdd);
    resultMdd = cMdd;

    aMdd = mdd_and(resultMdd, targetMdd, 1, 1);
    if(!mdd_equal(aMdd, zeroMdd)) {
      array_insert_last(mdd_t *, onionRings, mdd_dup(targetMdd));
      mdd_free(aMdd);
      break;
    }
    mdd_free(aMdd);

    /* add onion ring unless fixpoint reached */
    if (!term_fixpoint && onionRings != NIL(array_t)) {
      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
    }
  } /* while(!termination) for LFP */

  mdd_free(ringMdd);

  /* Print some debug info */
  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
    static int refCount=0;
    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);

    if (verbosity == McVerbosityMax_c) {
      mdd_t *tmpMdd = careStatesArray ?
                      mdd_and_array(resultMdd, careStatesArray, 1, 1) :
                      mdd_dup(resultMdd);
      fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount,
              mdd_size(resultMdd));
      fprintf(vis_stdout,
              "--There are %.0f care states satisfying ES formula\n",
              mdd_count_onset(mddMgr, tmpMdd, psVars));
#ifdef DEBUG_MC
      /* The following 2 lines are just for debug */
      fprintf(vis_stdout, "ES satisfying minterms :\n");
      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
      mdd_free(tmpMdd);
    } else {
      fprintf(vis_stdout,
              "--There are %.0f states satisfying ES formula\n",
              mdd_count_onset(mddMgr, resultMdd, psVars));
    }

    fprintf(vis_stdout, "--ES: %d image computations\n",
      Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
  }
  mdd_free(zeroMdd);

  if(fixpoint != NIL(boolean))
    *fixpoint = term_fixpoint || term_tautology;
  return resultMdd;

} /* McEvaluateESFormulaWithGivenTR */


mdd_t *
McEvaluateESFormulaWithGivenTRFAFW(
  Fsm_Fsm_t *modelFsm,
  mdd_t *invariantMdd,
  mdd_t *sourceMdd,
  mdd_t *underapprox,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint,
  mdd_t *Swin
  )
{
  mdd_t *aMdd;
  mdd_t *bMdd;
  mdd_t *cMdd;
  mdd_t *resultMdd;
  mdd_t *ringMdd;
  Img_ImageInfo_t *imageInfo;
  int nImgComps;
  boolean term_tautology = FALSE; /* different termination conditions */
  boolean term_early     = FALSE; 
  boolean term_fixpoint  = FALSE; 

  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
  resultMdd = mdd_and(sourceMdd, fairStates, 1, 1);

  if(underapprox != NIL(mdd_t)){
    mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
    mdd_free(resultMdd);
    resultMdd = tmp;
  }

  ringMdd = mdd_dup(resultMdd);

  if (onionRings) {
    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
  }
  
  /* if Since is trivially satisfied, or
     the early termination condition holds*/ 
  {
    bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
    boolean trivial;

    trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
                                            1, 1, careStatesArray);
    /* the lequal also takes care of the case where result = 1 */
    if(trivial ||
       McCheckEarlyTerminationForUnderapprox(earlyTermination,
                                             resultMdd,
                                             careStatesArray)){
      bdd_free(fairInvariantStates);
      bdd_free(ringMdd);

      /* trivially satisfied means that the fixpoint is complete.  If this
         information is requested, give it. */
      if(fixpoint != NIL(boolean))
        *fixpoint = trivial;
      return(resultMdd);
    }
    bdd_free(fairInvariantStates);
  }

  imageInfo = Fsm_FsmReadOrCreateImageInfoPrunedFAFW(modelFsm, Swin, 0, 1);
  /* The LFP loop */
  while (!term_fixpoint && !term_tautology && !term_early) {
    /* If dclevel is maximal, ringbdd is between the frontier and the
       reached set */
    aMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
                ringMdd, ringMdd, careStatesArray);
    mdd_free(ringMdd);

    bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
    mdd_free(aMdd);

    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
    mdd_free(bMdd);

    /* Can we stop?  The tautology condition can be weakened to
       cMdd <= careStatesArray */
    term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
                                                 careStatesArray);
    if(!term_fixpoint)
      term_tautology = mdd_is_tautology(cMdd, 1);
    if(!term_fixpoint && !term_tautology)
      term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, 
                                                         cMdd,
                                                         careStatesArray);

    /* Print some debug info, and set ringmdd */
    if (dcLevel >= McDcLevelRchFrontier_c) {
      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
      ringMdd = bdd_between(tmpMdd, cMdd);
      if (verbosity == McVerbosityMax_c) {
        fprintf(vis_stdout,
                "--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
                mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
      }
      mdd_free(tmpMdd);
      }
    else {
      ringMdd = mdd_dup(cMdd);
      if (verbosity == McVerbosityMax_c) {
          fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd));
      }
    }

    mdd_free(resultMdd);
    resultMdd = cMdd;
    /* add onion ring unless fixpoint reached */
    if (!term_fixpoint && onionRings != NIL(array_t)) {
      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
    }
  } /* while(!termination) for LFP */

  /* Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c); */
  Img_ImageInfoFreeFAFW(imageInfo);
  Img_ImageInfoFree(imageInfo);

  mdd_free(ringMdd);

  /* Print some debug info */
  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
    static int refCount=0;
    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);

    if (verbosity == McVerbosityMax_c) {
      mdd_t *tmpMdd = careStatesArray ?
                      mdd_and_array(resultMdd, careStatesArray, 1, 1) :
                      mdd_dup(resultMdd);
      fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount,
              mdd_size(resultMdd));
      fprintf(vis_stdout,
              "--There are %.0f care states satisfying ES formula\n",
              mdd_count_onset(mddMgr, tmpMdd, psVars));
#ifdef DEBUG_MC
      /* The following 2 lines are just for debug */
      fprintf(vis_stdout, "ES satisfying minterms :\n");
      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
      mdd_free(tmpMdd);
    } else {
      fprintf(vis_stdout,
              "--There are %.0f states satisfying ES formula\n",
              mdd_count_onset(mddMgr, resultMdd, psVars));
    }

    fprintf(vis_stdout, "--ES: %d image computations\n",
      Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
  }

  if(fixpoint != NIL(boolean))
    *fixpoint = term_fixpoint || term_tautology;
  return resultMdd;

} /* McEvaluateESFormulaWithGivenTR */


mdd_t *
McEvaluateAUFormulaWithGivenTR(
  Fsm_Fsm_t *modelFsm,
  mdd_t *invariantMdd,
  mdd_t *targetMdd,
  mdd_t *underapprox,
  mdd_t *fairStates,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint
  )
{
  mdd_t *aMdd;
  mdd_t *bMdd;
  mdd_t *cMdd;
  mdd_t *resultMdd;
  mdd_t *ringMdd;
  boolean term_tautology = FALSE; /* different termination conditions */
  boolean term_early     = FALSE;
  boolean term_fixpoint  = FALSE;

  resultMdd = mdd_and(targetMdd, fairStates, 1, 1);

  ringMdd = mdd_dup(resultMdd);
  if (onionRings) {
    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
  }
  /* The LFP loop */
  while (!term_fixpoint && !term_tautology && !term_early) {
    /* If dclevel is maximal, ringbdd is between the frontier and the
     reached set */
    aMdd = Mc_FsmEvaluateMXFormula(modelFsm, ringMdd, fairStates, 
                                    careStatesArray, verbosity, dcLevel);

    bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
    mdd_free(aMdd);

    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
    mdd_free(bMdd);
    mdd_free(ringMdd);

    /* Can we stop?  The tautology condition can be weakened to
       cMdd <= careStatesArray */
    term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
                                                 careStatesArray);
    if(!term_fixpoint)
      term_tautology = mdd_is_tautology(cMdd, 1);
    if(!term_fixpoint && !term_tautology)
      term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination,
                                                         cMdd,
                                                         careStatesArray);

    /* Print some debug info, and set ringmdd */
    if (dcLevel >= McDcLevelRchFrontier_c) {
      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
      ringMdd = bdd_between(tmpMdd, cMdd);
      if (verbosity == McVerbosityMax_c) {
        fprintf(vis_stdout,
                "--AU |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
                mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
      }
      mdd_free(tmpMdd);
      }
    else {
      ringMdd = mdd_dup(cMdd);
      if (verbosity == McVerbosityMax_c) {
          fprintf(vis_stdout, "-- AU |ringMdd| = %d\n", mdd_size(ringMdd));
      }
    }

    mdd_free(resultMdd);
    resultMdd = cMdd;
    /* add onion ring unless fixpoint reached */
    if (!term_fixpoint && onionRings) {
      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
    }
  } /* while(!termination) for LFP */

  mdd_free(ringMdd);


  if(fixpoint != NIL(boolean))
    *fixpoint = term_fixpoint || term_tautology;
  return resultMdd;  
}


mdd_t *
McEvaluateEGFormulaWithGivenTR(
  Fsm_Fsm_t *modelFsm,
  mdd_t *invariantMdd,
  mdd_t *overapprox,
  mdd_t *fairStates,
  Fsm_Fairness_t *modelFairness,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  array_t **pOnionRingsArrayForDbg,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint)
{
  int i;
  array_t *onionRings;
  boolean useRings;
  mdd_manager *mddManager;
  mdd_t *mddOne;
  mdd_t *iterate;
  array_t *buchiFairness;
  int nPreComps;
  int nIterations;
  boolean term_fixpoint = FALSE;        /* different termination conditions */
  boolean term_tautology = FALSE;
  boolean term_early = FALSE;

  /* Here's how the onionRingsArrayForDbg works.  It is an array of
     arrays of mdds.  It is filled in anew for every pass of the
     algorithm, that is for every /\_{c inC} EXE(Y U Y*c).  There is
     one entry for every fairness constraint, and this entry contains
     the onionrings of the EU computation that corresponds to this
     constraint. */
  assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
         *pOnionRingsArrayForDbg == NIL(array_t) ||
         array_n(*pOnionRingsArrayForDbg) == 0);  

  useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
              *pOnionRingsArrayForDbg != NIL(array_t));

  nIterations = 0;
  nPreComps  = Img_GetNumberOfImageComputation(Img_Backward_c);
  onionRings = NIL(array_t);
  mddManager = Fsm_FsmReadMddManager(modelFsm);
  mddOne  = mdd_one(mddManager);

  /* If an overapproximation of the greatest fixpoint is given, use it. */
  if(overapprox != NIL(mdd_t)){
    iterate = mdd_and(invariantMdd, overapprox, 1, 1);
  } else {
    iterate = mdd_dup(invariantMdd);
  }

  /* See if we need to enter the loop at all.  If we wanted to test for
   * early termination here, we should fix the onion rings.  In the current
   * case, we do not need to, since the EG does not hold, and hence a
   * counterexample does not exist.
   */
  if( mdd_is_tautology(iterate, 0)){
    mdd_free(mddOne);
    if(fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0);
    return(iterate);
  }

  /* read fairness constraints */
  buchiFairness = array_alloc(mdd_t *, 0);
  if(modelFairness != NIL(Fsm_Fairness_t)) {
    if(!Fsm_FairnessTestIsBuchi(modelFairness)) {
      (void)fprintf(vis_stdout,
               "** mc error: non-Buechi fairness constraints not supported\n");
      array_free(buchiFairness);
      mdd_free(iterate);
      mdd_free(mddOne);

      if(fixpoint != NIL(boolean)) *fixpoint = FALSE;
      return NIL(mdd_t);
    }
    else {
      int j;
      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
      for (j = 0 ; j < numBuchi; j++) {
        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
                                                careStatesArray, dcLevel);
        array_insert_last(mdd_t *, buchiFairness, tmpMdd);
      }
    }
  }
  else {
    array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager));
  }


  /* GFP.  If we know that the result is a subset of a set S, we can conjoin
   the iterate with that set.  We use this to converge faster.  */
  while (TRUE) {
    mdd_t *newIterate;           /* the new iterate */

    nIterations++;
    newIterate = mdd_dup(iterate);
    
    /* for all fairness constraints */
    for (i = 0 ; i < array_n(buchiFairness) ; i++) {
      mdd_t *aMdd, *bMdd, *cMdd, *dMdd;
      mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i);
      
      if(useRings) {
        onionRings = array_alloc(mdd_t *, 0);
        array_insert_last(array_t *, *pOnionRingsArrayForDbg, onionRings);
      }

      aMdd = mdd_and(FiMdd, newIterate, 1, 1);

      bMdd = Mc_FsmEvaluateEUFormula(modelFsm, newIterate, aMdd, NIL(mdd_t),
                                     mddOne, careStatesArray,
                                     MC_NO_EARLY_TERMINATION, NIL(array_t),
                                     Mc_None_c, onionRings, verbosity, dcLevel,
                                     NIL(boolean));  
      mdd_free(aMdd);
      cMdd = Mc_FsmEvaluateEXFormula(modelFsm, bMdd, mddOne, careStatesArray,
                                     verbosity, dcLevel);
      mdd_free(bMdd);

      dMdd  = mdd_and(newIterate, cMdd, 1, 1);

      mdd_free(cMdd);
      mdd_free(newIterate);
      newIterate = dMdd;

      /* invariants that hold here: newiterate <= iterate <= invariant. */
    }/* for all fairness constraints */

    /* termination */
    term_tautology = mdd_is_tautology(newIterate, 0);
    if(!term_tautology)
      term_fixpoint =  mdd_equal_mod_care_set_array(newIterate, iterate,
                                                    careStatesArray);
    if(!term_tautology && !term_fixpoint)
      term_early = McCheckEarlyTerminationForOverapprox(earlyTermination,
                                                        newIterate, 
                                                        careStatesArray);
    if(term_tautology || term_fixpoint || term_early){
      mdd_free(iterate);
      iterate = newIterate;
      break; /* from the GFP loop */
    }

    /* update iterate */
    mdd_free(iterate);
    iterate = newIterate;

    if(useRings){
      mdd_array_array_free(*pOnionRingsArrayForDbg);
      *pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
    }
  } /* while(true) for gfp */

  /* Check if onionrings are OK */
  if(verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
    if(useRings){
      for (i = 0 ; i < array_n(*pOnionRingsArrayForDbg); i++) {
        int j;
        mdd_t *Fi = array_fetch(mdd_t *,  buchiFairness, i);
        array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
                                          i); 
        for (j = 0 ; j < array_n(onionRings); j++) {
          mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
          if(j == 0) {
            if(!mdd_lequal_mod_care_set_array(ring, Fi, 1, 1,
                                               careStatesArray)) {
              fprintf(vis_stderr, "** mc error: Problem w/ dbg in EG - ");
              fprintf(vis_stderr,
                      "inner most ring not in Fi (fairness constraint).\n");
            }
          }
          if(!mdd_lequal_mod_care_set_array(ring, invariantMdd, 1, 1,
                                             careStatesArray)) {
            fprintf(vis_stderr, "** mc error: Problem w/ dbg in EG - ");
            fprintf(vis_stderr, "An onion ring of last EU fails invariant\n");
          }
        } /* for all onionrings in array i */ 
      } /* for all onionringarrays in onionringsarray */
    }/* if useRings */

    if(verbosity == McVerbosityMax_c) {
      mdd_t *tmpMdd = careStatesArray ?
        mdd_and_array(iterate, careStatesArray, 1, 1) : mdd_dup(iterate);
      fprintf(vis_stdout,
              "--There are %.0f care states satisfying EG formula\n",
              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd,
                                Fsm_FsmReadPresentStateVars(modelFsm)));
#ifdef DEBUG_MC
      /* The following 2 lines are just for debug */
      fprintf(vis_stdout, "EG satisfying minterms :\n");
      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
      mdd_free(tmpMdd);
    } else {
      fprintf(vis_stdout, "--There are %.0f states satisfying EG formula\n",
              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), iterate,
                                Fsm_FsmReadPresentStateVars(modelFsm)));
    }

    fprintf(vis_stdout, "--EG: %d iterations, %d preimage computations\n",
      nIterations, Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
  }

  mdd_array_free(buchiFairness);
  mdd_free(mddOne);

  if(fixpoint != NIL(boolean))
     *fixpoint = term_fixpoint || term_tautology;
  return iterate;

} /* McEvaluateEGFormulaWithGivenTR */


mdd_t *
McEvaluateEHFormulaWithGivenTR(
  Fsm_Fsm_t *modelFsm,
  mdd_t *invariantMdd,
  mdd_t *overapprox,
  mdd_t *fairStates,
  Fsm_Fairness_t *modelFairness,
  array_t *careStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  array_t **pOnionRingsArrayForDbg,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  boolean *fixpoint)
{
  int i;
  array_t *onionRings;
  boolean useRings;
  mdd_manager *mddManager;
  mdd_t *mddOne;
  mdd_t *iterate;
  array_t *buchiFairness;
  int nImgComps;
  int nIterations;
  boolean term_fixpoint = FALSE;        /* different termination conditions */
  boolean term_tautology = FALSE;
  boolean term_early = FALSE;

  /* Here's how the onionRingsArrayForDbg works.  It is an array of
     arrays of mdds.  It is filled in anew for every pass of the
     algorithm, that is for every /\_{c inC} EYE(Y S Y*c).  There is
     one entry for every fairness constraint, and this entry contains
     the onionrings of the ES computation that corresponds to this
     constraint. */
  assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
         *pOnionRingsArrayForDbg == NIL(array_t) ||
         array_n(*pOnionRingsArrayForDbg) == 0);  

  useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
              *pOnionRingsArrayForDbg != NIL(array_t));

  nIterations = 0;
  nImgComps  = Img_GetNumberOfImageComputation(Img_Forward_c);
  onionRings = NIL(array_t);
  mddManager = Fsm_FsmReadMddManager(modelFsm);
  mddOne  = mdd_one(mddManager);

  /* If an overapproxiamtion of the greatest fixpoint is given, use it. */
  if(overapprox != NIL(mdd_t)){
    iterate = mdd_and(invariantMdd, overapprox, 1, 1);
  } else {
    iterate = mdd_dup(invariantMdd);
  }

  /* See if we need to enter the loop at all */
  if( mdd_is_tautology(iterate, 0) ||
      McCheckEarlyTerminationForOverapprox(earlyTermination,
                                           iterate,
                                           careStatesArray)){
    mdd_free(mddOne);

    if(fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0);
    return(iterate);
  }

  /* read fairness constraints */
  buchiFairness = array_alloc(mdd_t *, 0);
  if(modelFairness != NIL(Fsm_Fairness_t)) {
    if(!Fsm_FairnessTestIsBuchi(modelFairness)) {
      (void)fprintf(vis_stdout,
               "** mc error: non-Buechi fairness constraints not supported\n");
      array_free(buchiFairness);
      mdd_free(iterate);
      mdd_free(mddOne);

      if(fixpoint != NIL(boolean)) *fixpoint = FALSE;
      return NIL(mdd_t);
    }
    else {
      int j;
      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
      for (j = 0 ; j < numBuchi; j++) {
        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
                                                careStatesArray, dcLevel);
        array_insert_last(mdd_t *, buchiFairness, tmpMdd);
      }
    }
  }
  else {
    array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager));
  }


  /* GFP.  If we know that the result is a subset of a set S, we can conjoin
   the iterate with that set.  We use this to converge faster.  */
  while (TRUE) {
    mdd_t *newIterate;           /* the new iterate */

    nIterations++;
    newIterate = mdd_dup(iterate);
    
    /* for all fairness constraints */
    for (i = 0 ; i < array_n(buchiFairness) ; i++) {
      mdd_t *aMdd, *bMdd, *cMdd, *dMdd;
      mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i);
      
      if(useRings) {
        onionRings = array_alloc(mdd_t *, 0);
        array_insert_last(array_t *, *pOnionRingsArrayForDbg, onionRings);
      }

      aMdd = mdd_and(FiMdd, newIterate, 1, 1);

      bMdd = Mc_FsmEvaluateESFormula(modelFsm, newIterate, aMdd, NIL(mdd_t),
                                     mddOne, careStatesArray,
                                     MC_NO_EARLY_TERMINATION, NIL(array_t),
                                     Mc_None_c, onionRings, verbosity, dcLevel,
                                     NIL(boolean));  
      mdd_free(aMdd);
      cMdd = Mc_FsmEvaluateEYFormula(modelFsm, bMdd, mddOne, careStatesArray,
                                     verbosity, dcLevel);
      mdd_free(bMdd);

      dMdd  = mdd_and(newIterate, cMdd, 1, 1);

      mdd_free(cMdd);
      mdd_free(newIterate);
      newIterate = dMdd;

      /* invariants that hold here: newiterate <= iterate <= invariant. */
    }/* for all fairness constraints */

    /* termination */
    term_tautology = mdd_is_tautology(newIterate, 0);
    if(!term_tautology)
      term_fixpoint =  mdd_equal_mod_care_set_array(newIterate, iterate,
                                                    careStatesArray);
    if(!term_tautology && !term_fixpoint)
      term_early = McCheckEarlyTerminationForOverapprox(earlyTermination,
                                                        newIterate, 
                                                        careStatesArray);
    if(term_tautology || term_fixpoint || term_early){
      mdd_free(iterate);
      iterate = newIterate;
      break; /* from the GFP loop */
    }

    /* update iterate */
    mdd_free(iterate);
    iterate = newIterate;

    if(useRings){
      mdd_array_array_free(*pOnionRingsArrayForDbg);
      *pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
    }
  } /* while(true) for gfp */

  /* Check if onionrings are OK */
  if(verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
    if(useRings){
      for (i = 0 ; i < array_n(*pOnionRingsArrayForDbg); i++) {
        int j;
        mdd_t *Fi = array_fetch(mdd_t *,  buchiFairness, i);
        array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
                                          i); 
        for (j = 0 ; j < array_n(onionRings); j++) {
          mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
          if(j == 0) {
            if(!mdd_lequal_mod_care_set_array(ring, Fi, 1, 1,
                                               careStatesArray)) {
              fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
              fprintf(vis_stderr,
                      "inner most ring not in Fi (fairness constraint).\n");
            }
          }
          if(!mdd_lequal_mod_care_set_array(ring, invariantMdd, 1, 1,
                                             careStatesArray)) {
            fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
            fprintf(vis_stderr, "An onion ring of last ES fails invariant\n");
          }
        } /* for all onionrings in array i */ 
      } /* for all onionringarrays in onionringsarray */
    }/* if useRings */

    if(verbosity == McVerbosityMax_c) {
      mdd_t *tmpMdd = careStatesArray ?
        mdd_and_array(iterate, careStatesArray, 1, 1) : mdd_dup(iterate);
      fprintf(vis_stdout,
              "--There are %.0f care states satisfying EH formula\n",
              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd,
                                Fsm_FsmReadPresentStateVars(modelFsm)));
#ifdef DEBUG_MC
      /* The following 2 lines are just for debug */
      fprintf(vis_stdout, "EH satisfying minterms :\n");
      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
#endif
      mdd_free(tmpMdd);
    } else {
      fprintf(vis_stdout, "--There are %.0f states satisfying EH formula\n",
              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), iterate,
                                Fsm_FsmReadPresentStateVars(modelFsm)));
    }

    fprintf(vis_stdout, "--EH: %d iterations, %d image computations\n",
      nIterations, Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
  }

  mdd_array_free(buchiFairness);
  mdd_free(mddOne);

  if(fixpoint != NIL(boolean))
     *fixpoint = term_fixpoint || term_tautology;
  return iterate;

} /* McEvaluateEHFormulaWithGivenTR */


void
McFormulaFreeDebugData(
  Ctlp_Formula_t *formula)
{
  Ctlp_FormulaType  type     = Ctlp_FormulaReadType(formula);
  array_t          *dbgArray = (array_t *) Ctlp_FormulaReadDebugData(formula);

  if (type == Ctlp_EU_c || type == Ctlp_FwdU_c) {
    mdd_array_free(dbgArray);
  }
  else if (type == Ctlp_EG_c || type == Ctlp_FwdG_c || type == Ctlp_EH_c) 
    mdd_array_array_free(dbgArray);
  else {
    fail("Error - called on non EG/EU formula.\n");
  }
}


void
_McPrintSatisfyingMinterms(mdd_t *aMdd, Fsm_Fsm_t *fsm)
{
  array_t *support = Fsm_FsmReadPresentStateVars(fsm);
  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
  Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm);
  int i, n;
  array_t *mintermArray;
  mdd_t *aMinterm;

  n = (int) mdd_count_onset(mddMgr, aMdd, support);
  mintermArray = mdd_pick_arbitrary_minterms(mddMgr, aMdd, support, n);

  for (i = 0; i < n; i++) {
    aMinterm = array_fetch(mdd_t *, mintermArray, i);
    Mc_MintermPrint(aMinterm, support, network);
    mdd_free(aMinterm);
  }

  array_free(mintermArray);

}

boolean
McPrintPassFail(
  mdd_manager *mddMgr,
  Fsm_Fsm_t *modelFsm,
  Mc_FwdBwdAnalysis traversalDirection,
  Ctlp_Formula_t *ctlFormula,
  mdd_t *ctlFormulaStates,
  mdd_t *modelInitialStates,
  array_t *modelCareStatesArray,
  McOptions_t *options,
  Mc_VerbosityLevel verbosity)
{
  if (mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1)) {
    fprintf(vis_stdout, "# MC: formula passed --- ");
    Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula));
    fprintf(vis_stdout, "\n");
    return TRUE;
  }
  else {
    fprintf(vis_stdout, "# MC: formula failed --- ");
    Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula));
    fprintf(vis_stdout, "\n");
    if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) {
      McFsmDebugFormula(options, ctlFormula,modelFsm, modelCareStatesArray);
    }
    return FALSE;
  }
}


mdd_t *
McModelCheckAtomicFormula(
  Fsm_Fsm_t *modelFsm,
  Ctlp_Formula_t *ctlFormula)
{
  mdd_t * resultMdd;
  mdd_t *tmpMdd;
  Ntk_Network_t *network = Fsm_FsmReadNetwork(modelFsm);
  char *nodeNameString = Ctlp_FormulaReadVariableName(ctlFormula);
  char *nodeValueString = Ctlp_FormulaReadValueName(ctlFormula);
  Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);

  Var_Variable_t *nodeVar;
  int nodeValue;

  graph_t *modelPartition;
  vertex_t *partitionVertex;
  Mvf_Function_t *MVF;

  nodeVar = Ntk_NodeReadVariable(node);
  if (Var_VariableTestIsSymbolic(nodeVar)) {
    nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
  }
  else {
    nodeValue = atoi(nodeValueString);
  }

#if 0
  modelPartition = Part_NetworkReadPartition(network);
#endif
  modelPartition = Fsm_FsmReadPartition(modelFsm);
  if (!(partitionVertex = Part_PartitionFindVertexByName(modelPartition,
                                                         nodeNameString))) {
    lsGen tmpGen;
    Ntk_Node_t *tmpNode;
    array_t *mvfArray;
    array_t *tmpRoots = array_alloc(Ntk_Node_t *, 0);
    st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
    array_insert_last(Ntk_Node_t *, tmpRoots, node);

    Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
      st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED);
    }

    mvfArray =  Ntm_NetworkBuildMvfs(network, tmpRoots, tmpLeaves,
                                      NIL(mdd_t));
    MVF = array_fetch(Mvf_Function_t *, mvfArray, 0);
    array_free(tmpRoots);
    st_free_table(tmpLeaves);
    array_free(mvfArray);

    tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
    resultMdd = mdd_dup(tmpMdd);
    Mvf_FunctionFree(MVF);
  }
  else {
    MVF = Part_VertexReadFunction(partitionVertex);
    tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
    resultMdd = mdd_dup(tmpMdd);
  }
  if (Part_PartitionReadMethod(modelPartition) == Part_Frontier_c &&
      Ntk_NodeTestIsCombOutput(node)) {
    array_t     *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
    mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
    array_t     *supportList;
    st_table    *supportTable = st_init_table(st_numcmp, st_numhash);
    int         i, j;
    int         existIntermediateVars;
    int         mddId;
    Mvf_Function_t      *mvf;
    vertex_t    *vertex;
    array_t     *varBddRelationArray, *varArray;
    mdd_t       *iv, *ivMdd, *relation;

    for (i = 0; i < array_n(psVars); i++) {
      mddId = array_fetch(int, psVars, i);
      st_insert(supportTable, (char *)(long)mddId, NULL);
    }

    existIntermediateVars = 1;
    while (existIntermediateVars) {
      existIntermediateVars = 0;
      supportList = mdd_get_support(mgr, resultMdd);
      for (i = 0; i < array_n(supportList); i++) {
        mddId = array_fetch(int, supportList, i);
        if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) {
          vertex = Part_PartitionFindVertexByMddId(modelPartition, mddId);
          mvf = Part_VertexReadFunction(vertex);
          varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mgr, mddId, mvf);
          varArray = mdd_id_to_bdd_array(mgr, mddId);
          assert(array_n(varBddRelationArray) == array_n(varArray));
          for (j = 0; j < array_n(varBddRelationArray); j++) {
            iv = array_fetch(mdd_t *, varArray, j);
            relation = array_fetch(mdd_t *, varBddRelationArray, j);
            ivMdd = bdd_cofactor(relation, iv);
            mdd_free(relation);
            tmpMdd = resultMdd;
            resultMdd = bdd_compose(resultMdd, iv, ivMdd);
            mdd_free(tmpMdd);
            mdd_free(iv);
            mdd_free(ivMdd);
          }
          array_free(varBddRelationArray);
          array_free(varArray);
          existIntermediateVars = 1;
        }
      }
      array_free(supportList);
    }
    st_free_table(supportTable);
  }
  return resultMdd;
} /* McModelCheckAtomicFormula */


void
InvarPrintDebugInformation(Fsm_Fsm_t *modelFsm,
                           array_t *invarFormulaArray,
                           array_t *invarStatesArray,
                           int *resultArray,
                           McOptions_t *options,
                           array_t *hintsStatesArray)
{
  FILE *debugFile = McOptionsReadDebugFile(options);
  FILE *tmpFile = vis_stdout;
  extern FILE *vis_stdpipe;
  mdd_t *outerOnionRing=NIL(mdd_t);
  mdd_t *reachableBadStates;
  mdd_t *aBadReachableState, *reachableStates;
  array_t *aPath;
  boolean computeReach = TRUE;
  int ringsUpToDate;
  array_t *onionRings=NIL(array_t);
  int i, j;
  Fsm_RchType_t approxFlag;
  Ctlp_Formula_t *invarFormula;
  mdd_t *invarFormulaStates;
  approxFlag = McOptionsReadInvarApproxFlag(options);

  if (debugFile)
    vis_stdpipe = debugFile;
  else if (McOptionsReadUseMore(options) == TRUE)
    vis_stdpipe = popen("more", "w");
  else
    vis_stdpipe = vis_stdout;
  vis_stdout = vis_stdpipe;

  arrayForEachItem(mdd_t *, invarStatesArray, i, invarFormulaStates) {
    if ((invarFormulaStates == NIL(mdd_t)) || (resultArray[i] == 1))
      continue;
    onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm);
    ringsUpToDate = Fsm_FsmTestReachabilityOnionRingsUpToDate(modelFsm);
    /* search for onion ring intersecting invarStates' */
    if (onionRings != NIL(array_t)) {
      for (j = 0; j < array_n(onionRings); j++) {
        outerOnionRing = array_fetch(mdd_t *, onionRings, j);
        if (!mdd_lequal(outerOnionRing, invarFormulaStates, 1, 1)) {
          computeReach = FALSE;
          break;
        }
      }
    }

    /* no onion ring found, hence recompute with onion rings */
    if (computeReach == TRUE) {
      Mc_VerbosityLevel verbosity;
      int debugFlag;
      int ardc;
      int dcLevel = McOptionsReadDcLevel(options);
      verbosity = McOptionsReadVerbosityLevel(options);
      debugFlag = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c);
      if (dcLevel == McDcLevelArdc_c)
        ardc = 1;
      else
        ardc = 0;
      assert(!ringsUpToDate);
      reachableStates = Fsm_FsmComputeReachableStates(
        modelFsm, 0, (int)verbosity , 0, 0, debugFlag, 0, 0, approxFlag, ardc,
        0, invarStatesArray, (verbosity > 1), hintsStatesArray);
      mdd_free(reachableStates);
      /* find the onion ring with invariant failure */
      onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm);
      if (onionRings == NIL(array_t)) {
        fprintf(vis_stdout, "Unable to generate onion rings for counterexample.\n");
        fprintf(vis_stdout, "Try again with standard (without -A) options.\n");
        if (vis_stdout != tmpFile && vis_stdout != debugFile)
          (void)pclose(vis_stdpipe);
        vis_stdout = tmpFile;
        return;
      }
      ringsUpToDate = Fsm_FsmTestReachabilityOnionRingsUpToDate(modelFsm);
      for (j = 0; j < array_n(onionRings); j++) {
        outerOnionRing = array_fetch(mdd_t *, onionRings, j);
        if (!mdd_lequal(outerOnionRing, invarFormulaStates, 1, 1)) {
          break;
        }
      }
    }
    invarFormula = array_fetch(Ctlp_Formula_t *, invarFormulaArray, i);
    /* this is the case of  true negative */
    if (outerOnionRing != NIL(mdd_t)) {
      /* compute the set of bad states */
      if(Fsm_FsmReadFAFWFlag(modelFsm) > 1 && McOptionsReadInvarApproxFlag(options) == Fsm_Rch_Bfs_c)
        reachableBadStates = mdd_not(invarFormulaStates);
      else
        reachableBadStates = mdd_and(invarFormulaStates, outerOnionRing, 0, 1);
      /* pick one bad state */
      aBadReachableState = Mc_ComputeAState(reachableBadStates, modelFsm);
      mdd_free(reachableBadStates);

      /* build a path from the initial states to the bad state */
      aPath = Mc_BuildPathFromCore(aBadReachableState, onionRings,
                                   modelFsm, McGreaterOrEqualZero_c);
      mdd_free(aBadReachableState);


      if(McOptionsReadDbgLevel(options)==2)
      {

        (void) Mc_PrintPathAiger(aPath, modelFsm, McOptionsReadPrintInputs(options));
      }
      else
      {
        (void) fprintf(vis_stdout, "# INV: formula %d failed --- ", i+1);
        Ctlp_FormulaPrint(vis_stdout,
                        Ctlp_FormulaReadOriginalFormula(invarFormula));
        fprintf(vis_stdout, "\n");

        (void) fprintf(vis_stdout, "# INV: calling debugger\n");
        if (array_n(aPath) > 1) {
          (void) fprintf(vis_stdout,
                        "# INV: a sequence of states starting at an initial ");
          (void) fprintf(vis_stdout, "state leading to a bad state\n");
        } else {
          (void) fprintf(vis_stdout,
                    "# INV: invariant fails at the following initial state\n");
        }
        (void) Mc_PrintPath(aPath, modelFsm, McOptionsReadPrintInputs(options));
      }
      (void) fprintf(vis_stdout, "\n");

      McNormalizeBddPointer(aPath);
      mdd_array_free(aPath);
    } else {
      /* Was a false negative */
      assert (approxFlag == Fsm_Rch_Oa_c);
      (void) fprintf(vis_stdout, "# INV: formula passed --- ");
      Ctlp_FormulaPrint(vis_stdout,
                        Ctlp_FormulaReadOriginalFormula(invarFormula));
      fprintf(vis_stdout, "\n");
    }
  }

  if (vis_stdout != tmpFile && vis_stdout != debugFile)
    (void)pclose(vis_stdpipe);
  vis_stdout = tmpFile;
} /* end of InvarPrintDebugInformation */


array_t *
SortFormulasByFsm(Fsm_Fsm_t *totalFsm,
                  array_t *invarFormulaArray,
                  array_t *fsmArray,
                  McOptions_t *options)
{
  array_t *resultArray;
  array_t *formulaArray;
  array_t *tempArray;
  int i, j, found;
  Ctlp_Formula_t *formula;
  Ntk_Network_t *network = Fsm_FsmReadNetwork(totalFsm);
  Fsm_Fsm_t *reducedFsm, *fsm;
  int reducedFsmPos = -1;

  if (invarFormulaArray == NIL(array_t)) return invarFormulaArray;
  if (array_n(invarFormulaArray) == 0) return NIL(array_t);

  tempArray = array_alloc(array_t *, 0);
  /* do a semantic check and a quantifier check */
  arrayForEachItem (Ctlp_Formula_t *, invarFormulaArray, i, formula) {
    if (!Mc_FormulaStaticSemanticCheckOnNetwork(formula, network, FALSE)){
      (void) fprintf(vis_stderr, "** inv error: error in parsing Atomic Formula:\n%s\n", error_string());
      error_init();
      Ctlp_FormulaFree(formula);
      continue;
    } else {
      if (Ctlp_FormulaTestIsQuantifierFree(formula) == FALSE) {
        (void) fprintf(vis_stderr, "** inv error: invariant formula refers to path quantifiers\n");
        Ctlp_FormulaFree(formula);
        continue;
      }
    }
    array_insert_last(Ctlp_Formula_t *, tempArray, formula);
  }
  if (array_n(tempArray) == 0) {
    array_free(tempArray);
    return NIL(array_t);
  }

  /* if no -r option, return the original array */
  resultArray = array_alloc(array_t *, 0);
  if (McOptionsReadReduceFsm(options) == FALSE) {
    array_insert_last(array_t *, resultArray, tempArray);
    reducedFsm = McConstructReducedFsm(network, tempArray);
    if (reducedFsm != NIL(Fsm_Fsm_t)) {
      array_insert_last(Fsm_Fsm_t *, fsmArray, reducedFsm);
    } else {
      array_insert_last(Fsm_Fsm_t *, fsmArray, totalFsm);
    }
    return resultArray;
  }

  /* We want to minimize per formula only when "-r" option is not specified */
  arrayForEachItem (Ctlp_Formula_t *, tempArray, i, formula) {
    /* Create reduced fsm */
    formulaArray = array_alloc(Ctlp_Formula_t *, 0);
    array_insert_last(Ctlp_Formula_t *, formulaArray, formula);

    reducedFsm = McConstructReducedFsm(network, formulaArray);
    if (reducedFsm == NIL(Fsm_Fsm_t)) {
      /* no reduction */
      reducedFsm = totalFsm;
    }

    /* Check if fsm already created */
    found = 0;
    for (j = 0; j < array_n(fsmArray); j++) {
      fsm = array_fetch (Fsm_Fsm_t *, fsmArray, j);
      found = Fsm_FsmCheckSameSubFsmInTotalFsm(totalFsm, reducedFsm, fsm);
      if (found) break;
    }

    /* If found, add to the existing list. Else add a new reduced fsm */
    if (found) {
      if (reducedFsm != totalFsm) Fsm_FsmFree(reducedFsm);
      array_free(formulaArray);
      formulaArray = array_fetch(array_t *, resultArray, j);
      array_insert_last(Ctlp_Formula_t *, formulaArray, formula);
    } else {
      array_insert_last(Fsm_Fsm_t *, fsmArray, reducedFsm);
      array_insert_last(array_t *, resultArray, formulaArray);
      if (reducedFsm == totalFsm) reducedFsmPos = array_n(fsmArray)-1;
    }
  }

  array_free(tempArray);
  /* swap the last reduced fsm with the total fsm. */
  if ((reducedFsmPos != -1) && (reducedFsmPos != array_n(fsmArray)-1)) {
    array_t *totalFsmFormulaArray;
    assert(array_n(fsmArray) == array_n(resultArray));
    fsm = array_fetch(Fsm_Fsm_t *, fsmArray, array_n(fsmArray)-1);
    array_insert(Fsm_Fsm_t *, fsmArray, reducedFsmPos, fsm);
    array_insert(Fsm_Fsm_t *, fsmArray, array_n(fsmArray)-1, totalFsm);
    formulaArray =  array_fetch(array_t *, resultArray, array_n(resultArray)-1);
    totalFsmFormulaArray = array_fetch(array_t *, resultArray, reducedFsmPos);
    array_insert(array_t *, resultArray, reducedFsmPos, formulaArray);
    array_insert(array_t *, resultArray, array_n(resultArray)-1, totalFsmFormulaArray);
  }

  return resultArray;
} /* end of SortFormulasByFsm */


int
TestInvariantsInTotalFsm(Fsm_Fsm_t *totalFsm,
                         array_t *invarStatesArray,
                         int shellFlag)
{
  int i;
  mdd_t *invariant;
  mdd_t *reachableStates;
  boolean upToDate = FALSE; /* don't care initialization */
  if (shellFlag) {
    upToDate = Fsm_FsmReachabilityOnionRingsStates(totalFsm, &reachableStates);
  } else {
    reachableStates = Fsm_FsmReadCurrentReachableStates(totalFsm);
  }
  if (reachableStates == NIL(mdd_t)) return TRUE;
  if (mdd_is_tautology(reachableStates, 0)) return TRUE;
  
  arrayForEachItem(mdd_t *, invarStatesArray, i, invariant) {
    if (invariant == NIL(mdd_t)) continue;
    if (!mdd_lequal(reachableStates, invariant, 1, 1)) {
      if (shellFlag) mdd_free(reachableStates);
      return FALSE;
    }
  }
  if (shellFlag) mdd_free(reachableStates);
  if ((shellFlag && !upToDate) ||
      (Fsm_FsmReadReachabilityApproxComputationStatus(totalFsm) ==
       Fsm_Rch_Under_c))
    return TRUE;
  else
    return FALSE;
    
}


Ctlp_Approx_t
ComputeResultingApproximation(
  Ctlp_FormulaType formulaType,
  Ctlp_Approx_t leftApproxType,
  Ctlp_Approx_t rightApproxType,
  Ctlp_Approx_t TRMinimization,
  Mc_EarlyTermination_t *earlyTermination,
  boolean fixpoint)
{
  Ctlp_Approx_t thisApproxType;

  switch (formulaType) {
  case Ctlp_ID_c:
  case Ctlp_TRUE_c:
  case Ctlp_FALSE_c:
    thisApproxType = Ctlp_Exact_c;
    break;
  case Ctlp_NOT_c:
    if (leftApproxType == Ctlp_Incomparable_c) {
      thisApproxType = Ctlp_Incomparable_c;
    } else if (leftApproxType == Ctlp_Overapprox_c) {
      thisApproxType = Ctlp_Underapprox_c;
    } else if (leftApproxType == Ctlp_Underapprox_c) {
      thisApproxType = Ctlp_Overapprox_c;
    } else {
      thisApproxType = Ctlp_Exact_c;
    }
    break;
  case Ctlp_AND_c:
    if (leftApproxType == Ctlp_Incomparable_c ||
        rightApproxType == Ctlp_Incomparable_c ||
        (leftApproxType == Ctlp_Overapprox_c &&
         rightApproxType == Ctlp_Underapprox_c) ||
        (leftApproxType == Ctlp_Underapprox_c &&
         rightApproxType == Ctlp_Overapprox_c)) {
      thisApproxType = Ctlp_Incomparable_c;
    } else if (rightApproxType == Ctlp_Overapprox_c) {
      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
          leftApproxType == Ctlp_Exact_c) {
        thisApproxType = Ctlp_Exact_c;
      } else {
        thisApproxType = Ctlp_Overapprox_c;
      }
    } else if (leftApproxType == Ctlp_Overapprox_c) {
      thisApproxType = Ctlp_Overapprox_c;
    } else if (rightApproxType == Ctlp_Underapprox_c) {
      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
          leftApproxType == Ctlp_Exact_c) {
        thisApproxType = Ctlp_Exact_c;
      } else {
        thisApproxType = Ctlp_Underapprox_c;
      }
    } else if (leftApproxType == Ctlp_Underapprox_c) {
      thisApproxType = Ctlp_Underapprox_c;
    } else {
      thisApproxType = Ctlp_Exact_c;
    }
    break;
  case Ctlp_EQ_c:
  case Ctlp_XOR_c:
    if (leftApproxType != Ctlp_Exact_c || rightApproxType != Ctlp_Exact_c) {
      thisApproxType = Ctlp_Incomparable_c;
    } else {
      thisApproxType = Ctlp_Exact_c;
    }
    break;
  case Ctlp_THEN_c:
    if (leftApproxType == Ctlp_Incomparable_c ||
        rightApproxType == Ctlp_Incomparable_c ||
        (leftApproxType == Ctlp_Overapprox_c &&
         rightApproxType == Ctlp_Overapprox_c) ||
        (leftApproxType == Ctlp_Underapprox_c &&
         rightApproxType == Ctlp_Underapprox_c)) {
      thisApproxType = Ctlp_Incomparable_c;
    } else if (rightApproxType == Ctlp_Overapprox_c) {
      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
          leftApproxType == Ctlp_Exact_c) {
        thisApproxType = Ctlp_Exact_c;
      } else {
        thisApproxType = Ctlp_Overapprox_c;
      }
    } else if (leftApproxType == Ctlp_Underapprox_c) {
      thisApproxType = Ctlp_Overapprox_c;
    } else if (rightApproxType == Ctlp_Underapprox_c) {
      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
          leftApproxType == Ctlp_Exact_c) {
        thisApproxType = Ctlp_Exact_c;
      } else {
        thisApproxType = Ctlp_Underapprox_c;
      }
    } else if (leftApproxType == Ctlp_Overapprox_c) {
      thisApproxType = Ctlp_Underapprox_c;
    } else {
      thisApproxType = Ctlp_Exact_c;
    }
    break;
  case Ctlp_OR_c:
    if (leftApproxType == Ctlp_Incomparable_c ||
        rightApproxType == Ctlp_Incomparable_c ||
        (leftApproxType == Ctlp_Overapprox_c &&
         rightApproxType == Ctlp_Underapprox_c) ||
        (leftApproxType == Ctlp_Underapprox_c &&
         rightApproxType == Ctlp_Overapprox_c)) {
      thisApproxType = Ctlp_Incomparable_c;
    } else if (rightApproxType == Ctlp_Overapprox_c) {
      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
          leftApproxType == Ctlp_Exact_c) {
        thisApproxType = Ctlp_Exact_c;
      } else {
        thisApproxType = Ctlp_Overapprox_c;
      }
    } else if (leftApproxType == Ctlp_Overapprox_c) {
      thisApproxType = Ctlp_Overapprox_c;
    } else if (rightApproxType == Ctlp_Underapprox_c) {
      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
          leftApproxType == Ctlp_Exact_c) {
        thisApproxType = Ctlp_Exact_c;
      } else {
        thisApproxType = Ctlp_Underapprox_c;
      }
    } else if (leftApproxType == Ctlp_Underapprox_c) {
      thisApproxType = Ctlp_Underapprox_c;
    } else {
      thisApproxType = Ctlp_Exact_c;
    }
    break;
  case Ctlp_EX_c:
    if (leftApproxType == Ctlp_Underapprox_c) {
      if (TRMinimization == Ctlp_Overapprox_c) {
        thisApproxType = Ctlp_Incomparable_c;
      } else {
        thisApproxType = Ctlp_Underapprox_c;
      }
    } else if (leftApproxType == Ctlp_Overapprox_c) {
      if (TRMinimization == Ctlp_Underapprox_c) {
        thisApproxType = Ctlp_Incomparable_c;
      } else {
        thisApproxType = Ctlp_Overapprox_c;
      }
    } else if (leftApproxType == Ctlp_Exact_c) {
      thisApproxType = TRMinimization;
    } else {
      thisApproxType = Ctlp_Incomparable_c;
    }
    break;
  case Ctlp_EU_c:
    if (leftApproxType == Ctlp_Incomparable_c ||
        rightApproxType == Ctlp_Incomparable_c ||
        (leftApproxType == Ctlp_Overapprox_c &&
         rightApproxType == Ctlp_Underapprox_c) ||
        (leftApproxType == Ctlp_Underapprox_c &&
         rightApproxType == Ctlp_Overapprox_c)) {
      thisApproxType = Ctlp_Incomparable_c;
    } else if (leftApproxType == Ctlp_Overapprox_c ||
               rightApproxType == Ctlp_Overapprox_c) {
      thisApproxType = Ctlp_Overapprox_c;
    } else if (leftApproxType == Ctlp_Underapprox_c ||
               rightApproxType == Ctlp_Underapprox_c) {
      thisApproxType = Ctlp_Underapprox_c;
    } else {
      thisApproxType = Ctlp_Exact_c;
    }
    if (!fixpoint) {
      if (TRMinimization == Ctlp_Overapprox_c ||
          thisApproxType == Ctlp_Overapprox_c) {
        thisApproxType = Ctlp_Incomparable_c;
      } else if (thisApproxType == Ctlp_Exact_c) {
        thisApproxType = Ctlp_Underapprox_c;
      }
    } else {
      if ((TRMinimization == Ctlp_Overapprox_c &&
           thisApproxType == Ctlp_Underapprox_c) ||
          (TRMinimization == Ctlp_Underapprox_c &&
           thisApproxType == Ctlp_Overapprox_c)) {
        thisApproxType = Ctlp_Incomparable_c;
      } else if (thisApproxType == Ctlp_Exact_c) {
        thisApproxType = TRMinimization;
      }
    }
    break;
  case Ctlp_EG_c:
    if (leftApproxType == Ctlp_Incomparable_c ||
        rightApproxType == Ctlp_Incomparable_c ||
        (leftApproxType == Ctlp_Overapprox_c &&
         rightApproxType == Ctlp_Underapprox_c) ||
        (leftApproxType == Ctlp_Underapprox_c &&
         rightApproxType == Ctlp_Overapprox_c)) {
      thisApproxType = Ctlp_Incomparable_c;
    } else if (leftApproxType == Ctlp_Overapprox_c ||
               rightApproxType == Ctlp_Overapprox_c) {
      thisApproxType = Ctlp_Overapprox_c;
    } else if (leftApproxType == Ctlp_Underapprox_c ||
               rightApproxType == Ctlp_Underapprox_c) {
      thisApproxType = Ctlp_Underapprox_c;
    } else {
      thisApproxType = Ctlp_Exact_c;
    }
    if (!fixpoint) {
      if (TRMinimization == Ctlp_Underapprox_c ||
          thisApproxType == Ctlp_Underapprox_c) {
        thisApproxType = Ctlp_Incomparable_c;
      } else if (thisApproxType == Ctlp_Exact_c) {
        thisApproxType = Ctlp_Overapprox_c;
      }
    } else {
      if ((TRMinimization == Ctlp_Overapprox_c &&
           thisApproxType == Ctlp_Underapprox_c) ||
          (TRMinimization == Ctlp_Underapprox_c &&
           thisApproxType == Ctlp_Overapprox_c)) {
        thisApproxType = Ctlp_Incomparable_c;
      } else if (thisApproxType == Ctlp_Exact_c) {
        thisApproxType = TRMinimization;
      }
    }
    break;
  case Ctlp_Cmp_c:
  case Ctlp_Init_c:
  case Ctlp_FwdU_c:
  case Ctlp_FwdG_c:
  case Ctlp_EY_c:
    /* no early termination and no hints in forward model checking */
    thisApproxType = Ctlp_Exact_c;
    break;
  default: fail("Encountered unknown type of CTL formula\n");
  }

  return thisApproxType;
  
} /* ComputeResultingApproximation */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


static mdd_t *
EvaluateFormulaRecur(
  Fsm_Fsm_t *modelFsm,
  Ctlp_Formula_t *ctlFormula,
  mdd_t *fairStates,
  Fsm_Fairness_t *fairCondition,
  array_t *modelCareStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  Fsm_HintsArray_t *hintsArray,
  Mc_GuidedSearch_t hintType,
  Ctlp_Approx_t TRMinimization,
  Ctlp_Approx_t *resultApproxType,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  int buildOnionRings,
  Mc_GSHScheduleType GSHschedule)
{
  mdd_t *leftMdd  = NIL(mdd_t);
  mdd_t *rightMdd = NIL(mdd_t);
  mdd_t *result   = NIL(mdd_t);
  
  mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
  array_t     *careStatesArray = NIL(array_t);
  mdd_t       *tmpMdd;
  mdd_t       *approx = NIL(mdd_t); /* prev computed approx of sat set */ 
  mdd_t *ctlFormulaStates = Ctlp_FormulaObtainStates( ctlFormula );
  Ctlp_Approx_t leftApproxType = Ctlp_Exact_c;
  Ctlp_Approx_t rightApproxType = Ctlp_Exact_c;
  Ctlp_Approx_t thisApproxType = Ctlp_Exact_c;
  boolean fixpoint = FALSE;
  boolean skipRight = FALSE;

  if ( ctlFormulaStates ) {
    return ctlFormulaStates;
  }
  
  {
    Ctlp_Formula_t *leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);

    if (leftChild) {
      Mc_EarlyTermination_t *nextEarlyTermination =
        McObtainUpdatedEarlyTerminationCondition(
          earlyTermination, NIL(mdd_t), Ctlp_FormulaReadType(ctlFormula));

      leftMdd = EvaluateFormulaRecur(modelFsm, leftChild, fairStates,
                                     fairCondition, modelCareStatesArray,
                                     nextEarlyTermination,
                                     hintsArray, hintType, TRMinimization,
                                     &leftApproxType, verbosity, dcLevel,
                                     buildOnionRings, GSHschedule);
      Mc_EarlyTerminationFree(nextEarlyTermination);
      if (!leftMdd) {
        return NIL(mdd_t);
      }
    }
  }

  {/* read right */
    Ctlp_Formula_t *rightChild = Ctlp_FormulaReadRightChild(ctlFormula);

    if (rightChild) {
      Mc_EarlyTermination_t *nextEarlyTermination =
        McObtainUpdatedEarlyTerminationCondition(
          earlyTermination, leftMdd, Ctlp_FormulaReadType(ctlFormula));

      skipRight = Mc_EarlyTerminationIsSkip(nextEarlyTermination);
      if (!skipRight) {
        rightMdd = EvaluateFormulaRecur(modelFsm, rightChild, fairStates,
                                        fairCondition, modelCareStatesArray,
                                        nextEarlyTermination,
                                        hintsArray, hintType, TRMinimization,
                                        &rightApproxType, verbosity, dcLevel,
                                        buildOnionRings, GSHschedule);
      }
      Mc_EarlyTerminationFree(nextEarlyTermination);
      if (!(rightMdd || skipRight)) {
        if (leftMdd)
          mdd_free(leftMdd);
        return NIL(mdd_t);
      }
    }
  }/* read right */

  if (modelCareStatesArray != NIL(array_t)) {
    careStatesArray = modelCareStatesArray;
  } else {
    careStatesArray = array_alloc(mdd_t *, 0);
    array_insert_last(mdd_t *, careStatesArray, mdd_one(mddMgr));
  }
  switch (Ctlp_FormulaReadType(ctlFormula)) {
  case Ctlp_ID_c:
    assert(!skipRight);
    result = McModelCheckAtomicFormula(modelFsm, ctlFormula);
    break;

  case Ctlp_TRUE_c:
    assert(!skipRight);
    result = mdd_one(mddMgr); break;

  case Ctlp_FALSE_c:
    assert(!skipRight);
    result = mdd_zero(mddMgr); break;

  case Ctlp_NOT_c:
    assert(!skipRight);
    result = mdd_not(leftMdd); break;

  case Ctlp_AND_c:
    if (skipRight) {
      result = mdd_dup(leftMdd);
      rightApproxType = Ctlp_Overapprox_c;
    } else {
      result = mdd_and(leftMdd, rightMdd, 1, 1);
    }
    break;

  case Ctlp_EQ_c:
    assert(!skipRight);
    result = mdd_xnor(leftMdd, rightMdd); break;

  case Ctlp_XOR_c:
    assert(!skipRight);
    result = mdd_xor(leftMdd, rightMdd); break;

  case Ctlp_THEN_c:
    if (skipRight) {
      result = mdd_dup(leftMdd);
      rightApproxType = Ctlp_Underapprox_c;
    } else {
      result = mdd_or(leftMdd, rightMdd, 0, 1);
    }
    break;

  case Ctlp_OR_c:
    if (skipRight) {
      result = mdd_dup(leftMdd);
      rightApproxType = Ctlp_Underapprox_c;
    } else {
      result = mdd_or(leftMdd, rightMdd, 1, 1);
    }
    break;

  case Ctlp_EX_c:
    assert(!skipRight);
    result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
                                     careStatesArray, verbosity, dcLevel);
    break;

  case Ctlp_EU_c: {
    array_t *onionRings = NIL(array_t); /* array of mdd_t */
    boolean newrings;

    assert(!skipRight);
    /* An underapproximation, together with its explanation may be stored. */
    approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Underapprox_c );
    onionRings = (array_t *) Ctlp_FormulaReadDebugData(ctlFormula);
    newrings = onionRings == NIL(array_t);

    if (buildOnionRings){
      assert((approx != NIL(mdd_t) && onionRings != NIL(array_t)) ||
             (approx == NIL(mdd_t) && onionRings == NIL(array_t)));
      if(onionRings == NIL(array_t))
        onionRings = array_alloc(mdd_t *, 0);
    }

    result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, rightMdd,
                                     approx, fairStates,
                                     careStatesArray,
                                     earlyTermination, hintsArray,
                                     hintType, onionRings,
                                     verbosity, dcLevel, &fixpoint);

    if(buildOnionRings && newrings)
      Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings,
                             McFormulaFreeDebugData);
    if(approx != NIL(mdd_t))
      mdd_free(approx);

    break;
  }
  case Ctlp_EG_c: {
    array_t  *arrayOfOnionRings = NIL(array_t); /* array of array of mdd_t* */

    assert(!skipRight);
    if(buildOnionRings)
      arrayOfOnionRings = array_alloc(array_t *, 0);

    approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Overapprox_c );

    result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, approx, fairStates, 
                                     fairCondition, careStatesArray,
                                     earlyTermination, hintsArray, hintType, 
                                     &arrayOfOnionRings, verbosity,
                                     dcLevel, &fixpoint, GSHschedule);

    if(buildOnionRings)
      Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
                             McFormulaFreeDebugData);

    if(approx != NIL(mdd_t)) mdd_free(approx);

    break;
  }
  case Ctlp_Cmp_c: {
    assert(!skipRight);
    if (Ctlp_FormulaReadCompareValue(ctlFormula) == 0)
      result = bdd_is_tautology(leftMdd, 0) ?
                mdd_one(mddMgr) : mdd_zero(mddMgr);
    else
      result = bdd_is_tautology(leftMdd, 0) ?
                mdd_zero(mddMgr) : mdd_one(mddMgr);
    break;
  }
  case Ctlp_Init_c:
    assert(!skipRight);
    result = Fsm_FsmComputeInitialStates(modelFsm);
    break;
  case Ctlp_FwdU_c:
    assert(!skipRight);
    if (buildOnionRings) {
      array_t *onionRings = array_alloc(mdd_t *, 0);
      result = Mc_FsmEvaluateFwdUFormula(modelFsm, leftMdd, rightMdd,
                                         fairStates, careStatesArray,
                                         onionRings, verbosity, dcLevel);
      Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings,
                             McFormulaFreeDebugData);
    }
    else {
      if (Ctlp_FormulaReadLeftChild(ctlFormula) &&
          Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(ctlFormula)) ==
          Ctlp_Init_c &&
          Ctlp_FormulaReadRightChild(ctlFormula) &&
          Ctlp_FormulaReadType(Ctlp_FormulaReadRightChild(ctlFormula)) ==
          Ctlp_TRUE_c &&
          Fsm_FsmTestIsReachabilityDone(modelFsm)) {
        result = mdd_dup(Fsm_FsmReadReachableStates(modelFsm));
        break;
      }
      result = Mc_FsmEvaluateFwdUFormula(modelFsm, leftMdd, rightMdd,
                                         fairStates, careStatesArray,
                                         NIL(array_t), verbosity, 
                                         dcLevel);
    }
    break;
  case Ctlp_FwdG_c:
    assert(!skipRight);
    if (buildOnionRings) {
      array_t *arrayOfOnionRings = array_alloc(array_t *, 0);
      result = Mc_FsmEvaluateFwdGFormula(modelFsm, leftMdd, rightMdd,
                                         fairStates, fairCondition,
                                         careStatesArray,
                                         arrayOfOnionRings, verbosity,
                                         dcLevel);   
      Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
                             McFormulaFreeDebugData);
    } else {
      result = Mc_FsmEvaluateFwdGFormula(modelFsm, leftMdd, rightMdd,
                                         fairStates, fairCondition,
                                         careStatesArray,
                                         NIL(array_t), verbosity,
                                         dcLevel);
    }
    break;
  case Ctlp_EY_c:
    assert(!skipRight);
    result = Mc_FsmEvaluateEYFormula(modelFsm, leftMdd, fairStates,
                                     careStatesArray, verbosity, dcLevel);
    break;

  default: fail("Encountered unknown type of CTL formula\n");
  }

  tmpMdd = mdd_dup(result);
  thisApproxType = ComputeResultingApproximation(
    Ctlp_FormulaReadType(ctlFormula), leftApproxType,
    rightApproxType, TRMinimization, earlyTermination, fixpoint);
  Ctlp_FormulaSetApproxStates(ctlFormula, tmpMdd, thisApproxType);

#ifdef DEBUG_MC
  /* The following code is just for debugging */
  if ((verbosity == McVerbosityMax_c)) {
    char *type = Ctlp_FormulaGetTypeString(ctlFormula);
    if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_Cmp_c) {
      fprintf(vis_stdout, "Info : result for [Cmp]\n");
      if (bdd_is_tautology(result, 1))
        fprintf(vis_stdout, "TRUE\n");
      else
        fprintf(vis_stdout, "FALSE\n");
    }
    else if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_ID_c) {
      char *atomic = Ctlp_FormulaConvertToString(ctlFormula);
      fprintf(vis_stdout, "Info : satisfying minterms for [%s(%s)]:\n",
              type, atomic);
      free(atomic);
      if (bdd_is_tautology(result, 1))
        fprintf(vis_stdout, "-- TAUTOLOGY --\n");
      else if (bdd_is_tautology(result, 0))
        fprintf(vis_stdout, "-- null --\n");
      else
        (void)_McPrintSatisfyingMinterms(result, modelFsm);
    }
    else {
      fprintf(vis_stdout, "Info : satisfying minterms for [%s]:\n", type);
      if (bdd_is_tautology(result, 1))
        fprintf(vis_stdout, "-- TAUTOLOGY --\n");
      else if (bdd_is_tautology(result, 0))
        fprintf(vis_stdout, "-- null --\n");
      else
        (void)_McPrintSatisfyingMinterms(result, modelFsm);
    }
    free(type);
  }
#endif
  
  if (modelCareStatesArray == NIL(array_t))
    mdd_array_free(careStatesArray);
  if (leftMdd)
    mdd_free(leftMdd);
  if (rightMdd)
    mdd_free(rightMdd);
  *resultApproxType = thisApproxType;
  return result;
}


static mdd_t *
McForwardReachable(
  Fsm_Fsm_t *modelFsm,
  mdd_t *targetMdd,
  mdd_t *invariantMdd,
  mdd_t *fairStates,
  array_t *careStatesArray,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  mdd_t *resultMdd, *fuMdd;

  /* When McForwardReachable is called by Mc_FsmEvaluateFwdEHFormula
   * with no fairness constraints, this test saves one image
   * computation. */
  if (mdd_is_tautology(fairStates, 1) &&
      mdd_lequal_mod_care_set_array(invariantMdd, targetMdd,
                                    1, 1, careStatesArray)) {
    resultMdd = mdd_dup(invariantMdd);
    if (onionRings) {
      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
    }
  } else {
    fuMdd = Mc_FsmEvaluateFwdUFormula(modelFsm, targetMdd, invariantMdd,
                                      fairStates, careStatesArray, onionRings,
                                      verbosity, dcLevel);
    resultMdd = mdd_and(fuMdd, invariantMdd, 1, 1);
    mdd_free(fuMdd);
  }

  /* Updates onionRings not to have warning message in
   * Mc_FsmEvaluateFwdEHFormula since Reachable(p,q) = FwdUntil(p,q) ^ q.
   */
  if (onionRings) {
    int         i;
    mdd_t       *ring, *tmp;

    for (i = 0 ; i < array_n(onionRings); i++) {
      tmp = array_fetch(mdd_t *, onionRings, i);
      ring = mdd_and(tmp, invariantMdd, 1, 1);
      mdd_free(tmp);
      array_insert(mdd_t *, onionRings, i, ring);
    }
  }

  return(resultMdd);
}