src/mc/mcUtil.c

Go to the documentation of this file.

#include "mcInt.h"
#include "mdd.h"
#include "cmd.h"
#include "fsm.h"
#include "img.h"
#include "sat.h"
#include "baig.h"
#include <errno.h>

static char rcsid[] UNUSED = "$Id: mcUtil.c,v 1.113 2009/04/11 18:26:10 fabio Exp $";

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


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

static void PrintNodes(array_t *mddIdArray, Ntk_Network_t *network);
static array_t * SortMddIds(array_t *mddIdArray, Ntk_Network_t *network);
static void PrintDeck(array_t *mddValues, array_t *mddIdArray, Ntk_Network_t *network);
static int cmp(const void * s1, const void * s2);
static boolean AtomicFormulaCheckSemantics(Ctlp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed);
static void NodeTableAddCtlFormulaNodes(Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table * nodesTable);
static void NodeTableAddLtlFormulaNodes(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table * nodesTable);
static boolean MintermCheckWellFormed(mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr);
static boolean SetCheckSupport(mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr);
static mdd_t * Mc_ComputeRangeOfPseudoInputs(Ntk_Network_t *network);
static array_t *Mc_BuildBackwardRingsWithInvariants(mdd_t *S, mdd_t *T, mdd_t *invariants, Fsm_Fsm_t *fsm);

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

int
Mc_FsmComputeStatesReachingToSet(
  Fsm_Fsm_t *modelFsm,
  mdd_t *targetStates,
  array_t *careStatesArray,
  mdd_t *specialStates,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  mdd_t *fromUpperBound;
  mdd_t *toCareSet;
  array_t *toCareSetArray = array_alloc(mdd_t *, 0);
  mdd_t *image;
  Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);

  mdd_t *reachingStates = mdd_dup( targetStates );
  mdd_t *fromLowerBound = mdd_dup( targetStates );

  /* Iterate until fromLowerBound is empty. */
  while (mdd_is_tautology(fromLowerBound, 0) == 0){
    /* fromLowerBound is the "onion shell" of states just examined. */
    array_insert_last(mdd_t*, onionRings,
                      mdd_dup(fromLowerBound));
    if ( !mdd_lequal(  fromLowerBound, specialStates, 1, 0 ) ) {
      mdd_free( fromLowerBound );
      mdd_free( reachingStates );
      return TRUE;
    }

    /* fromUpperBound is the set of all states reaching targets thus far. */
    fromUpperBound = mdd_dup( reachingStates );

    /* toCareSet is the set of all states not reached so far. */
    toCareSet = mdd_not(reachingStates);
    array_insert(mdd_t *, toCareSetArray, 0, toCareSet);

    /*
     * Pre-Image of some set between lower and upper, where we care
     * about the image only on unreaching states.
     */
    image = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
                fromLowerBound, fromUpperBound, toCareSetArray);
    mdd_free(toCareSet);
    mdd_free(fromLowerBound);

    /* New set of reaching states is old set plus new image. */
    mdd_free( reachingStates );
    reachingStates = mdd_or(fromUpperBound, image, 1, 1);
    mdd_free(image);

    /*
     * New lower bound is the states just reached (note not on
     * fromUpperBound).
     */
    fromLowerBound = mdd_and(reachingStates, fromUpperBound, 1, 0);

    mdd_free(fromUpperBound);
  }
  mdd_array_free( onionRings );
  mdd_free( reachingStates );
  mdd_free(fromLowerBound);
  array_free(toCareSetArray);

  return FALSE;
}

int
Mc_FsmComputeStatesReachableFromSet(
  Fsm_Fsm_t *modelFsm,
  mdd_t *initialStates,
  array_t *careStatesArray,
  mdd_t *specialStates,
  array_t *onionRings,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  boolean reachable=FALSE;
  mdd_t *fromUpperBound;
  mdd_t *toCareSet;
  array_t *toCareSetArray = array_alloc(mdd_t *, 0);
  mdd_t *image;
  Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);

  mdd_t *reachableStates = mdd_dup( initialStates );
  mdd_t *fromLowerBound = mdd_dup( initialStates );

  /* Iterate until fromLowerBound is empty. */
  while (mdd_is_tautology(fromLowerBound, 0) == 0){
    /* fromLowerBound is the "onion shell" of states just reached. */
    array_insert_last(mdd_t*, onionRings,
                      mdd_dup(fromLowerBound));
    if (!mdd_lequal(  fromLowerBound, specialStates, 1, 0 ) ) {
      mdd_free( fromLowerBound );
      mdd_free( reachableStates );
      return TRUE;
    }

    /* fromUpperBound is the set of all states reached thus far. */
    fromUpperBound = mdd_dup( reachableStates );

    /* toCareSet is the set of all states not reached so far. */
    toCareSet = mdd_not(reachableStates);
    array_insert(mdd_t *, toCareSetArray, 0, toCareSet);

    /*
     * Image of some set between lower and upper, where we care
     * about the image only on unreached states.
     */
    image = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
                fromLowerBound, fromUpperBound, toCareSetArray);
    mdd_free(toCareSet);
    mdd_free(fromLowerBound);

    /* New set of reachable states is old set plus new image. */
    mdd_free( reachableStates );
    reachableStates = mdd_or(fromUpperBound, image, 1, 1);
    mdd_free(image);

    /*
     * New lower bound is the states just reached (note not on
     * fromUpperBound).
     */
    fromLowerBound = mdd_and(reachableStates, fromUpperBound, 1, 0);
    mdd_free(fromUpperBound);
  }
  mdd_array_free( onionRings );
  mdd_free( reachableStates );
  mdd_free(fromLowerBound);
  array_free(toCareSetArray);

  return reachable;

}

boolean
Mc_FormulaStaticSemanticCheckOnNetwork(
  Ctlp_Formula_t *formula,
  Ntk_Network_t *network,
  boolean inputsAllowed
  )
{
  boolean lCheck;
  boolean rCheck;
  Ctlp_Formula_t *leftChild;
  Ctlp_Formula_t *rightChild;

  if(formula == NIL(Ctlp_Formula_t)){
    return TRUE;
  }

  if(Ctlp_FormulaReadType(formula) == Ctlp_ID_c){
    return AtomicFormulaCheckSemantics(formula, network, inputsAllowed);
  }

  leftChild = Ctlp_FormulaReadLeftChild(formula);
  rightChild = Ctlp_FormulaReadRightChild(formula);

  lCheck = Mc_FormulaStaticSemanticCheckOnNetwork(leftChild, network,
                                                  inputsAllowed);
  if(!lCheck)
    return FALSE;

  rCheck = Mc_FormulaStaticSemanticCheckOnNetwork(rightChild, network,
                                                  inputsAllowed);
  if (!rCheck)
      return FALSE;

  return TRUE;
}

array_t *
Mc_BuildPathToCore(
  mdd_t *aState,
  array_t *onionRings,
  Fsm_Fsm_t *modelFsm,
  Mc_PathLengthType PathLengthType)
{
  int i;  /* index into the onionRings */
  int startingPoint;
  mdd_t *currentState;
  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
  array_t *pathToCore;
  mdd_manager *mddMgr         = Fsm_FsmReadMddManager(modelFsm);
  array_t *toCareSetArray;

  if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
    return(Mc_BuildPathToCoreFAFW(
                            aState, onionRings, modelFsm, PathLengthType));
  }

  pathToCore         = array_alloc( mdd_t * , 0 );
  toCareSetArray     = array_alloc(mdd_t *, 0);
  array_insert_last(mdd_t *, toCareSetArray, mdd_one(mddMgr));

  if ( PathLengthType == McGreaterZero_c )
    startingPoint = 1;
  else if ( PathLengthType == McGreaterOrEqualZero_c )
    startingPoint = 0;
  else
    fail("Called Mc_BuildPathToCore with ill formed PathLengthType\n");

  /* RB: How do you guarantee that aState is in one of the onion rings [1,n]?*/

  /*Find the lowest ring that holds aState*/
  for ( i = startingPoint ; i < array_n( onionRings ); i++ ) {
    mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
    if ( McStateTestMembership( aState, ring ) )
      break;
  }
  if ( i == array_n( onionRings ) )
    return NIL(array_t);

  currentState = mdd_dup( aState );
  array_insert_last( mdd_t *, pathToCore, currentState );

  /* until we get to ring 0, keep finding successors for currentState */
  while( i > 0 ) {
    mdd_t *currentStateSuccs;
    mdd_t *innerRing;
    mdd_t *currentStateSuccsInInnerRing;
    mdd_t *witnessSuccState;

    i--;

    currentStateSuccs =
      Img_ImageInfoComputeImageWithDomainVars(imageInfo, currentState,
                                              currentState, toCareSetArray);
    currentStateSuccsInInnerRing = mdd_zero(mddMgr);

    /* find the highest ring that contains a successor, starting with i */
    while(mdd_is_tautology(currentStateSuccsInInnerRing, 0)){
      assert(i >= 0);
      if(i < 0) return NIL(array_t);

      innerRing = array_fetch( mdd_t *, onionRings, i );
      mdd_free(currentStateSuccsInInnerRing);
      currentStateSuccsInInnerRing = mdd_and(currentStateSuccs, innerRing,
                                             1, 1 );
      i--;
    }

    i++;

    witnessSuccState = Mc_ComputeACloseState(currentStateSuccsInInnerRing,
                                             currentState,
                                             modelFsm );
    array_insert_last( mdd_t *, pathToCore, witnessSuccState );
    currentState = witnessSuccState;

    mdd_free( currentStateSuccs );
    mdd_free( currentStateSuccsInInnerRing );

    /* next, see if we cannot move a few more rings down.  We have to do this,
     * since a nontrivial path is not guaranteed to exist from a node in ring i
     * to a node in a lower ring.  In fact a state in ring i may also be in
     * ring 0. */
    {
      boolean contained = TRUE;
      while(contained && i > 0){
        i--;
        innerRing = array_fetch( mdd_t *, onionRings, i );
        contained = mdd_lequal(witnessSuccState, innerRing, 1, 1);
      }
      /* i is highest ring not containing witnessSuccState, or i = 0 */

      if(!contained){
        i++;
      }
      /* i is lowest ring containing witnessSuccState */
    }
  }

  mdd_array_free(toCareSetArray);

  return pathToCore;
}

array_t *
Mc_BuildForwardRings(
  mdd_t *S,
  Fsm_Fsm_t *fsm,
  array_t *onionRings)
{
  mdd_t *nextStates;
  mdd_t *states, *nStates, *oneMdd;
  array_t *toCareSetArray, *forwardRings;
  int i;
  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);

  states = mdd_zero(mddMgr);
  oneMdd = mdd_one(mddMgr);
  for(i=0; i<array_n(onionRings); i++) {
    mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
    nStates = mdd_or(ring, states, 1, 1);
    mdd_free(states);
    states = nStates;
  }
  forwardRings = array_alloc(mdd_t *, 0);
  toCareSetArray = array_alloc(mdd_t *, 0);
  array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
  nextStates = Mc_FsmEvaluateESFormula(fsm, states, S,
                                       NIL(mdd_t), oneMdd, toCareSetArray,
                                       MC_NO_EARLY_TERMINATION, NIL(array_t),
                                       Mc_None_c, forwardRings,
                                       McVerbosityNone_c, McDcLevelNone_c,
                                       NIL(boolean));
  mdd_free(nextStates);
  mdd_free(states);
  mdd_array_free(toCareSetArray);

  return(forwardRings);
}

array_t *
Mc_BuildForwardRingsWithInvariants(mdd_t *S,
                                   mdd_t *T,
                                   mdd_t *invariants,
                                   Fsm_Fsm_t *fsm)
{
  mdd_t *oneMdd, *nextStates, *fairStates;
  array_t *toCareSetArray, *forwardRings;
  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);

  oneMdd = mdd_one(mddMgr);
  forwardRings = array_alloc(mdd_t *, 0);
  toCareSetArray = array_alloc(mdd_t *, 0);
  array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
  fairStates = Fsm_FsmReadFairnessStates(fsm);
  if(fairStates == 0)   fairStates = oneMdd;
  nextStates = McEvaluateESFormulaWithGivenTRWithTarget(fsm, invariants, S, T,
                                   NIL(mdd_t), fairStates, toCareSetArray,
                                   MC_NO_EARLY_TERMINATION,
                                   forwardRings, McVerbosityNone_c,
                                   McDcLevelNone_c, NIL(boolean));
  mdd_free(nextStates);
  mdd_array_free(toCareSetArray);

  return(forwardRings);
}

static array_t *
Mc_BuildBackwardRingsWithInvariants(
  mdd_t *S,
  mdd_t *T,
  mdd_t *invariants,
  Fsm_Fsm_t *fsm)
{
  mdd_t *oneMdd, *nextStates, *fairStates;
  array_t *toCareSetArray, *backwardRings;
  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);

  oneMdd = mdd_one(mddMgr);
  backwardRings = array_alloc(mdd_t *, 0);
  toCareSetArray = array_alloc(mdd_t *, 0);
  array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
  fairStates = Fsm_FsmReadFairnessStates(fsm);
  if(fairStates == 0)   fairStates = oneMdd;
  nextStates = McEvaluateEUFormulaWithGivenTR(fsm, invariants, T,
                                   NIL(mdd_t), fairStates, toCareSetArray,
                                   MC_NO_EARLY_TERMINATION,
                                   backwardRings, McVerbosityNone_c,
                                   McDcLevelNone_c, NIL(boolean));
  mdd_free(nextStates);
  mdd_array_free(toCareSetArray);

  return(backwardRings);
}

array_t *
Mc_BuildPathFromCore(
  mdd_t *aStates,
  array_t *onionRings,
  Fsm_Fsm_t *modelFsm,
  Mc_PathLengthType PathLengthType)
{
  int i, j;
  int startingPoint;
  mdd_t *currentState, *aState;
  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
  array_t *pathToCore;
  mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
  array_t *toCareSetArray;
  array_t *pathFromCore;
  mdd_t *currentStatePreds, *currentStatePredsInInnerRing;
  mdd_t *innerRing = NIL(mdd_t), *witnessPredState;
  boolean shortestDist =
        (Fsm_FsmReadReachabilityOnionRingsMode(modelFsm) == Fsm_Rch_Bfs_c);


  if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
    pathFromCore = Mc_BuildPathFromCoreFAFW(
                            aStates, onionRings,
                            modelFsm, PathLengthType);
    return(pathFromCore);
  }
  aState = Mc_ComputeAState(aStates, modelFsm);

  pathToCore = array_alloc( mdd_t * , 0 );
  toCareSetArray = NIL(array_t);

  if ( PathLengthType == McGreaterZero_c ) {
    startingPoint = 1;
  }
  else if ( PathLengthType == McGreaterOrEqualZero_c ) {
    startingPoint = 0;
  }
  else {
    fail("Called Mc_BuildPathFromCore with ill formed PathLengthType\n");
  }

  /* check that the state occurs in an onion ring. */
  for ( i = startingPoint ; i < array_n( onionRings ); i++ ) {
    mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
    if ( McStateTestMembership( aState, ring ) )
      break;
  }
  if ( i == array_n( onionRings ) ) {
    mdd_free(aState);
    return NIL(array_t);
  }

  /* insert the state in the path to the core */
  currentState = aState;
  array_insert_last( mdd_t *, pathToCore, currentState );

  /* initialize */
  toCareSetArray = array_alloc(mdd_t *, 0);
  array_insert_last(mdd_t *, toCareSetArray, mdd_one(mddMgr));

  /* loop until a path is found to the core */
  while( i-- > 0 ) {
    if (shortestDist) {
      /* a predecessor is guaranteed to be in the previous ring */
      mdd_array_free(toCareSetArray);
      toCareSetArray = array_alloc(mdd_t *, 0);
      innerRing = array_fetch( mdd_t *, onionRings, i );
      array_insert(mdd_t *, toCareSetArray, 0, mdd_dup(innerRing));
      currentStatePreds = Img_ImageInfoComputePreImageWithDomainVars(
                                imageInfo, currentState,
                                currentState, toCareSetArray);
    } else {
      /* compute the predecessors */
      currentStatePreds = Img_ImageInfoComputePreImageWithDomainVars(
                                imageInfo, currentState,
                                currentState, toCareSetArray );
      /* search for a predecessor in the earliest onion ring */
      for (j = 0; j <= i; j++) {
        innerRing = array_fetch( mdd_t *, onionRings, j );
        if (!mdd_lequal(currentStatePreds, innerRing, 1, 0)) {
          i = j;
          break;
        }
      }
    }
    /* compute the set of predecessors in the chosen ring. */
    currentStatePredsInInnerRing = mdd_and(currentStatePreds, innerRing, 1, 1);
    mdd_free( currentStatePreds );
    /* find a state in the predecessor */
    witnessPredState = Mc_ComputeACloseState(currentStatePredsInInnerRing,
                                             currentState, modelFsm);
    mdd_free( currentStatePredsInInnerRing );
    /* insert predecessor in the path */
    array_insert_last( mdd_t *, pathToCore, witnessPredState );
    currentState = witnessPredState;
  }

  mdd_array_free(toCareSetArray);

  /* flip the path to a path from the core */
  {
    int i;
    pathFromCore = array_alloc( mdd_t *, 0 );

    for( i=0; i < array_n( pathToCore ); i++ ) {
      mdd_t *tmpMdd = array_fetch(mdd_t *, pathToCore,
                                  (array_n(pathToCore) - (i+1)));
      array_insert_last( mdd_t *, pathFromCore, tmpMdd );
    }
    array_free( pathToCore );
    return pathFromCore;
  }
}

array_t *
Mc_BuildPathToCoreFAFW(
  mdd_t *aStates,
  array_t *onionRings,
  Fsm_Fsm_t *modelFsm,
  Mc_PathLengthType PathLengthType)
{
  int i, startingPoint;
  array_t *pathFromCore, *pathToCore;
  array_t *reachableOnionRings;
  mdd_t *currentStates;

  if ( PathLengthType == McGreaterZero_c ) {
    startingPoint = 1;
  }
  else if ( PathLengthType == McGreaterOrEqualZero_c ) {
    startingPoint = 0;
  }
  else {
    fail("Called Mc_BuildPathToCore with ill formed PathLengthType\n");
  }

  for ( i = startingPoint ; i < array_n( onionRings ); i++ ) {
    mdd_t *ring = array_fetch( mdd_t *, onionRings, i );
    if ( McStateTestMembership( aStates, ring ) )
      break;
  }
  if(i==0) {
    pathToCore = array_alloc( mdd_t * , 0 );
    array_insert_last( mdd_t *, pathToCore, mdd_dup(aStates) );
    return pathToCore;
  }

  reachableOnionRings = Mc_BuildForwardRings(aStates, modelFsm, onionRings);
  currentStates = array_fetch(mdd_t *, onionRings, 0);
  pathFromCore = Mc_BuildPathFromCoreFAFW(
                                currentStates,
                                reachableOnionRings, modelFsm, PathLengthType);
  mdd_array_free(reachableOnionRings);

  return(pathFromCore);
}


array_t *
Mc_BuildPathFromCoreFAFWGeneral(
  mdd_t *T,
  array_t *rings,
  Fsm_Fsm_t *modelFsm,
  Mc_PathLengthType PathLengthType)
{
  mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);
  mdd_t *S, *H, *nH, *ring;
  int i;
  array_t *L;
  array_t *pathFromCore;
  array_t *npathFromCore;

  H = mdd_zero(mgr);
  for(i=0; i<array_n(rings); i++) {
    ring = array_fetch(mdd_t *, rings, i);
    nH = mdd_or(ring, H, 1, 1);
    mdd_free(H);
    H = nH;
  }

  nH = mdd_and(H, T, 1, 1);
  T = nH;

  L = Mc_BuildFAFWLayer(modelFsm, mdd_dup(T), mdd_dup(H));

  if ( PathLengthType == McGreaterZero_c ) {
    S = mdd_dup(array_fetch(mdd_t *, rings, 1));
  }
  else if( PathLengthType == McGreaterOrEqualZero_c ) {
    S = mdd_dup(array_fetch(mdd_t *, rings, 0));
  }
  else {
    fail("Called Mc_BuildPathFromCoreFAFW with ill formed PathLengthType\n");
  }
  pathFromCore =
      MC_BuildCounterExampleFAFWGeneral(modelFsm, mdd_dup(S), mdd_dup(T), H, L);

  if(PathLengthType == McGreaterZero_c ) {
    S = array_fetch(mdd_t *, rings, 0);
    npathFromCore = array_alloc(mdd_t *, 0);
    array_insert_last(mdd_t *, npathFromCore, mdd_dup(S));
    for(i=0; i<array_n(pathFromCore); i++) {
      S = array_fetch(mdd_t *, pathFromCore, i);
      array_insert_last(mdd_t *, npathFromCore, S);
    }
    array_free(pathFromCore);
    pathFromCore = npathFromCore;
  }
  mdd_free(T);
  return(pathFromCore);
}


array_t *
MC_BuildCounterExampleFAFWGeneral(
        Fsm_Fsm_t *modelFsm,
        mdd_t *I,
        mdd_t *T,
        mdd_t *H,
        array_t *L)
{
  mdd_t *oneMdd, *zeroMdd;
  mdd_t *T_I, *P, *Li, *Q_Li, *Q_T, *nLi;
  mdd_t *ring, *ring_Q, *Q;
  mdd_t *layer, *Lm, *nLayer;
  mdd_t *extCube;
  mdd_t *invariantStates, *nInvariantStates;
  int m, q, free, i;
  array_t *path, *R;
  array_t *careStatesArray;
  Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
  mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);

  oneMdd = mdd_one(mgr);
  zeroMdd = mdd_zero(mgr);
  path = array_alloc(mdd_t *, 0);

  T_I = mdd_and(T, I, 1, 1);
  if(!mdd_equal(T_I, zeroMdd)) {
    mdd_free(oneMdd);
    mdd_free(zeroMdd);
    P = Mc_ComputeACloseState(T_I, T, modelFsm);
    mdd_free(T_I);
    array_insert_last(mdd_t *, path, P);
    return(path);
  }
  mdd_free(T_I);

  extCube = Fsm_FsmReadExtQuantifyInputCube(modelFsm);
  invariantStates = mdd_zero(mgr);
  layer = NULL;
  Lm = NULL;
  for(m=0; m<array_n(L); m++) {
    layer = array_fetch(mdd_t *, L, m);
    nLayer = bdd_smooth_with_cube(layer, extCube);
    nInvariantStates = mdd_or(invariantStates, nLayer, 1, 1);
    mdd_free(nLayer);
    mdd_free(invariantStates);
    invariantStates = nInvariantStates;
    Lm = mdd_and(I, layer, 1, 1);
    if(!mdd_equal(Lm, zeroMdd)) {
      break;
    }
    mdd_free(Lm);
  }

  R = Mc_BuildBackwardRingsWithInvariants(Lm, T, invariantStates, modelFsm);

  imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
  Img_ForwardImageInfoConjoinWithWinningStrategy(imageInfo, layer);
  i = m;
  Q = mdd_and(I, Lm, 1, 1);
  ring_Q = NULL;
  for(q=0; q<array_n(R); q++) {
    ring = array_fetch(mdd_t *, R, q);
    ring_Q = mdd_and(ring, Q, 1, 1);
    if(!mdd_equal(ring_Q, zeroMdd)) {
      break;
    }
    mdd_free(ring_Q);
  }
  mdd_free(Q);
  P = Mc_ComputeACloseState(ring_Q, T, modelFsm);
  mdd_free(ring_Q);

  free = 0;
  careStatesArray = array_alloc(mdd_t *, 0);
  array_insert_last(mdd_t *, careStatesArray, oneMdd);
  while(1) {
    Q = Img_ImageInfoComputeImageWithDomainVars(
                               imageInfo, P, P, careStatesArray);
    Q_T = mdd_and(Q, P, 1, 0);
    mdd_free(Q);
    Q = Q_T;

    if(i>0) {
      Li = array_fetch(mdd_t *, L, i-1);
      nLi = bdd_smooth_with_cube(Li, extCube);
      Q_Li = mdd_and(Q, nLi, 1, 1);
      mdd_free(nLi);
      if(!mdd_equal(Q_Li, zeroMdd)) {
        i--;
        mdd_free(Q);
        Q = Q_Li;
        free = 1;
        imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
        Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo);
        Img_ForwardImageInfoConjoinWithWinningStrategy(imageInfo, layer);
      }
    }

    ring_Q = NULL;
    for(q=0; q<array_n(R); q++) {
      ring = array_fetch(mdd_t *, R, q);
      ring_Q = mdd_and(ring, Q, 1, 1);
      if(!mdd_equal(ring_Q, zeroMdd)) {
          break;
      }
      mdd_free(ring_Q);
    }
    mdd_free(Q);

    if(q >= array_n(R)) {
      imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
      Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo);
      continue;
    }

    Q = Mc_ComputeACloseState(ring_Q, T, modelFsm);
    mdd_free(ring_Q);

    if(free == 0) {
      array_insert_last(mdd_t *, path, (mdd_t *)((long)P+1));
    }
    else if(free ==1) {
      array_insert_last(mdd_t *, path, P);
      free = 0;
    }

    Q_T = mdd_and(Q, T, 1, 1);
    if(!mdd_equal(Q_T, zeroMdd)) {
      array_insert_last(mdd_t *, path, (mdd_t *)((long)Q+1));
      mdd_free(Q_T);
      break;
    }
    mdd_free(Q_T);

    P = Q;
  }

  array_free(careStatesArray);
  mdd_free(oneMdd);
  mdd_free(zeroMdd);

  imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 0, 1);
  Img_ForwardImageInfoRecoverFromWinningStrategy(imageInfo);
  return(path);
}

array_t *
Mc_BuildFAFWLayer(Fsm_Fsm_t *modelFsm, mdd_t *T, mdd_t *H)
{
  mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);
  Img_ImageInfo_t *imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
  mdd_t *zeroMdd, *oneMdd;
  mdd_t *S, *nH, *EX_S, *extCube, *S_new;
  array_t *L;
  array_t *careStatesArray;

  zeroMdd = mdd_zero(mgr);
  oneMdd = mdd_one(mgr);
  L = array_alloc(mdd_t *, 0);

  extCube = Fsm_FsmReadExtQuantifyInputCube(modelFsm);
  careStatesArray = array_alloc(mdd_t *, 0);
  array_insert_last(mdd_t *, careStatesArray, oneMdd);
  while(!mdd_equal(H, zeroMdd)) {
      Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 1);
      S = Mc_FsmEvaluateAUFormula(modelFsm, H, T,
                                   NIL(mdd_t), oneMdd, careStatesArray,
                                   MC_NO_EARLY_TERMINATION, NIL(array_t),
                                   Mc_None_c, 0, McVerbosityNone_c,
                                   McDcLevelNone_c, NIL(boolean));
      Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 0);
      array_insert_last(mdd_t *, L, S);

      S_new = bdd_smooth_with_cube(S, extCube);
      mdd_free(S);
      nH = mdd_and(H, S_new, 1, 0);

      if(mdd_equal(H, nH)) {
        mdd_free(nH);
        mdd_free(S_new);
        break;
      }
      mdd_free(H);
      H = nH;
      mdd_free(T);
      EX_S = Img_ImageInfoComputePreImageWithDomainVars(
                                imageInfo, S_new, S_new, careStatesArray);
      mdd_free(S_new);
      T = mdd_and(EX_S, H, 1, 1);
  }
  array_free(careStatesArray);
  mdd_free(zeroMdd);
  mdd_free(oneMdd);
  mdd_free(T);
  mdd_free(H);

  return(L);
}

array_t *
Mc_BuildPathFromCoreFAFW(
  mdd_t *Ts,
  array_t *rings,
  Fsm_Fsm_t *modelFsm,
  Mc_PathLengthType PathLengthType)
{
  int startingPoint, prevFlag;
  int i, p, dist, forced;
  bdd_t *T, *S, *H, *nH, *Hp, *S1, *Swin;
  bdd_t *ring, *oneMdd, *zeroMdd;
  array_t *C, *newC, *AUrings, *segment;
  array_t *R, *ESrings;
  array_t *careStatesArray;
  array_t *pathFromCore;
  bdd_t *T_wedge_ring, *S1_wedge_ring, *Hp_wedge_S1;
  bdd_t *T_wedge_S, *C_T_wedge_S, *ESresult, *EX_T;
  bdd_t *EX_T_wedge_ring, *Hp_wedge_EX_T, *lastR;
  bdd_t *C_T_wedge_ring, *new_, *extCube;
  bdd_t *bundle, *single, *preSingle;
  Img_ImageInfo_t *imageInfo;
  mdd_manager *mgr = Fsm_FsmReadMddManager(modelFsm);

  if(Fsm_FsmReadFAFWFlag(modelFsm) == 2) {
      pathFromCore = Mc_BuildPathFromCoreFAFWGeneral(
                            Ts, rings,
                            modelFsm, PathLengthType);
      return(pathFromCore);
  }

  T = mdd_dup(Ts);
  imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
  if ( PathLengthType == McGreaterZero_c ) {
    startingPoint = 1;
  }
  else if( PathLengthType == McGreaterOrEqualZero_c ) {
    startingPoint = 0;
  }
  else {
    fail("Called Mc_BuildPathFromCoreFAFW with ill formed PathLengthType\n");
  }

  oneMdd = mdd_one(mgr);
  zeroMdd = mdd_zero(mgr);
  S = mdd_dup(array_fetch(mdd_t *, rings, startingPoint));
  prevFlag = 0; 
  H = mdd_zero(mgr);
  for(i=startingPoint; i<array_n(rings); i++) {
    ring = array_fetch(mdd_t *, rings, i);
    new_ = mdd_and(ring, H, 1, 0);
    mdd_free(ring);
    nH = mdd_or(new_, H, 1, 1);
    mdd_free(H);
    H = nH;
    array_insert(mdd_t *, rings, i, new_);
  }

  C = array_alloc(mdd_t *, 0);
  T_wedge_S = mdd_and(T, S, 1, 1);
  if(!mdd_equal(T_wedge_S, zeroMdd)) {
    if(startingPoint == 1) {
      mdd_free(T);
      T = array_fetch(mdd_t *, rings, 0);
      array_insert_last(mdd_t *, C, bdd_dup(T));
    }
    C_T_wedge_S = bdd_closest_cube(T_wedge_S, S, &dist);
    array_insert_last(mdd_t *, C, C_T_wedge_S);
    mdd_free(S);
    mdd_free(oneMdd);
    mdd_free(zeroMdd);
    mdd_free(H);
    mdd_free(T_wedge_S);

    return(C);
  }
  mdd_free(T_wedge_S);

  T_wedge_ring = NULL;
  for(p=startingPoint; p<array_n(rings); p++) {
    ring = array_fetch(mdd_t *, rings, p);
    T_wedge_ring = mdd_and(T, ring, 1, 1);
    if(!mdd_equal(T_wedge_ring, zeroMdd)) {
      break;
    }
    mdd_free(T_wedge_ring);
  }
  mdd_free(T);

  C_T_wedge_ring = bdd_closest_cube(T_wedge_ring, S, &dist);
  mdd_free(T_wedge_ring);
  array_insert_last(mdd_t *, C, C_T_wedge_ring);
  T = C_T_wedge_ring;

  extCube = Fsm_FsmReadExtQuantifyInputCube(modelFsm);
  careStatesArray = array_alloc(mdd_t *, 0);
  array_insert_last(mdd_t *, careStatesArray, oneMdd);
  while(1) {
    if(prevFlag == 0) { /* free segement */
      prevFlag = 1; /* force segment */

      for(i=array_n(rings)-1; i>p; i--) {
        ring = array_fetch(mdd_t *, rings, i);
        nH = mdd_and(H, ring, 1, 0);
        mdd_free(H);
        H = nH;
      }

      AUrings = array_alloc(mdd_t *, 0);
      Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 1);
      Swin = Mc_FsmEvaluateAUFormula(modelFsm, H, T,
                                   NIL(mdd_t), oneMdd, careStatesArray,
                                   MC_NO_EARLY_TERMINATION, NIL(array_t),
                                   Mc_None_c, AUrings, McVerbosityNone_c,
                                   McDcLevelNone_c, NIL(boolean));
      Fsm_FsmSetUseUnquantifiedFlag(modelFsm, 0);


      S1 = bdd_smooth_with_cube(Swin, extCube);
      mdd_array_free(AUrings);
      if(mdd_equal(S1, T)) {
        mdd_free(S1);
        mdd_free(Swin);
        continue;
      }

      for(i=p-1; i>=startingPoint; i--) {
        ring = array_fetch(mdd_t *, rings, i);
        S1_wedge_ring = mdd_and(S1, ring, 1, 1);
        if(mdd_equal(S1_wedge_ring, zeroMdd)) {
          mdd_free(S1_wedge_ring);
          break;
        }
        mdd_free(S1_wedge_ring);
      }
      p = i+1;
      Hp = array_fetch(mdd_t *, rings, p);

      ESrings = array_alloc(mdd_t *, 0);
      Hp_wedge_S1 = mdd_and(Hp, S1, 1, 1);

      ESresult = McEvaluateESFormulaWithGivenTRFAFW( modelFsm, S1, Hp_wedge_S1,
                                       NIL(mdd_t), oneMdd, careStatesArray,
                                       MC_NO_EARLY_TERMINATION, ESrings,
                                       McVerbosityNone_c, McDcLevelNone_c,
                                       NIL(boolean), Swin);
      mdd_free(ESresult);
      mdd_free(Hp_wedge_S1);
      mdd_free(S1);
      R = ESrings;
      if(array_n(R) <= 1) {
        mdd_array_free(R);
        mdd_free(Swin);
        continue;
      }
    }
    else { /* force segment */
      Swin = 0;
      prevFlag = 0; /* free segment */
      EX_T = Img_ImageInfoComputePreImageWithDomainVars(
                                imageInfo, T, T, careStatesArray);

      for(i=p-1; i>=startingPoint; i--) {
        ring = array_fetch(mdd_t *, rings, i);
        EX_T_wedge_ring = mdd_and(EX_T, ring, 1, 1);
        if(mdd_equal(EX_T_wedge_ring, zeroMdd)) {
          mdd_free(EX_T_wedge_ring);
          break;
        }
        mdd_free(EX_T_wedge_ring);
      }
      p = i+1;

      Hp = array_fetch(mdd_t *, rings, p);
      R = array_alloc(mdd_t *, 0);
      Hp_wedge_EX_T = mdd_and(Hp, EX_T, 1, 1);
      array_insert_last(mdd_t *, R, Hp_wedge_EX_T);
      array_insert_last(mdd_t *, R, mdd_dup(T));
      mdd_free(EX_T);
    }

    lastR = array_fetch(mdd_t *, R, 0);
    segment = Mc_BuildShortestPathFAFW(Swin, lastR, T, R, mgr, modelFsm, prevFlag);
    if(Swin)    {
      mdd_free(Swin);
      Swin = 0;
    }
    mdd_array_free(R);

    newC = array_join(C, segment);
    array_free(C);
    C = newC;

    T = array_fetch(mdd_t *, segment, array_n(segment)-1);
    if((long)T %2) T = (mdd_t *)((long)T - 1);
    array_free(segment);

    T_wedge_S = mdd_and(T, S, 1, 1);
    if(!mdd_equal(T_wedge_S, zeroMdd)) {
      mdd_free(T_wedge_S);
      mdd_free(S);
      mdd_free(H);
      break;
    }
    mdd_free(T_wedge_S);

    startingPoint = 0;
    mdd_free(S);
    S = mdd_dup(array_fetch(mdd_t *, rings, startingPoint));

  }

  array_free(careStatesArray);
  mdd_free(oneMdd);
  mdd_free(zeroMdd);

  {
    int i;
    pathFromCore = array_alloc( mdd_t *, 0 );

    if(startingPoint == 1) {
      T = array_fetch(mdd_t *, rings, 0);
      array_insert_last(mdd_t *, pathFromCore, bdd_dup(T));
    }

    preSingle = NULL;
    for( i=0; i < array_n( C ); i++ ) {
      bundle = array_fetch(mdd_t *, C, (array_n(C) - (i+1)));
      forced = 0;
      if((long)bundle%2) {
        bundle = (mdd_t *)((long)bundle -1);
        forced++;
      }
      if(i==0)
        single = Mc_ComputeAState(bundle, modelFsm);
      else
        single = Mc_ComputeACloseState(bundle, preSingle, modelFsm);
      array_insert_last( mdd_t *, pathFromCore,
              (mdd_t *)((long)(single) + forced) );
      preSingle = single;
    }
    McNormalizeBddPointer(C);
    mdd_array_free(C);
    return pathFromCore;
  }
}

array_t *
Mc_BuildShortestPathFAFW(mdd_t *win,
                         mdd_t *S,
                         mdd_t *T,
                         array_t *rings,
                         mdd_manager *mgr,
                         Fsm_Fsm_t *fsm,
                         int prevFlag)
{
  int q, dist;
  mdd_t *zeroMdd, *oneMdd;
  mdd_t *inputCube;
  mdd_t *ring, *ring_wedge_T, *Cn, *Cs;
  mdd_t *K, *realK, *range;
  mdd_t *preimage_of_Cn;
  array_t *C, *stateVars, *inputVars;
  array_t *toCareSetArray;
  Img_ImageInfo_t *imageInfo;

  imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, 1, 0);
  stateVars = Fsm_FsmReadPresentStateVars(fsm);
  inputVars = Fsm_FsmReadInputVars(fsm);
  inputCube = mdd_id_array_to_bdd_cube(mgr, inputVars);
  zeroMdd = mdd_zero(mgr);
  oneMdd = mdd_one(mgr);
  ring_wedge_T = NULL;
  for (q = 0; q < array_n(rings); q++){
    ring = array_fetch(mdd_t *, rings, q);
    ring_wedge_T = mdd_and(T, ring, 1, 1);
    if(!mdd_equal(ring_wedge_T, zeroMdd))
      break;
    mdd_free(ring_wedge_T);
    ring_wedge_T = 0;
  }
  if(ring_wedge_T) {
    mdd_free(ring_wedge_T);
  }
  else {
    fprintf(stdout, "We cannot find T\n");
  }

  C = array_alloc(mdd_t *, 0);
  Cn = (T);
  toCareSetArray = array_alloc(mdd_t *, 0);
  array_insert(mdd_t *, toCareSetArray, 0, oneMdd);
  range = mdd_range_mdd(mgr, stateVars);
  while(q > 0) {
    preimage_of_Cn = Img_ImageInfoComputePreImageWithDomainVars(
                                imageInfo, Cn, Cn, toCareSetArray);

    K = NULL;
    for (q = 0; q < array_n(rings); q++){
      ring = array_fetch(mdd_t *, rings, q);
      K = mdd_and(preimage_of_Cn, ring, 1, 1);
      if(!mdd_equal(K, zeroMdd))
        break;
      mdd_free(K);
      K = 0;
    }

    mdd_free(preimage_of_Cn);
    realK = mdd_and(K, range, 1, 1);
    mdd_free(K);
    Cs = bdd_closest_cube(realK, Cn, &dist);
    mdd_free(realK);


    Cn = bdd_smooth_with_cube(Cs, inputCube);
    mdd_free(Cs);
    if(!prevFlag) 
      array_insert_last(mdd_t *, C, Cn);
    else          
      array_insert_last(mdd_t *, C, (mdd_t *)((long)Cn+1));
  }
  array_free(toCareSetArray);
  mdd_free(zeroMdd);
  mdd_free(oneMdd);
  mdd_free(range);
  mdd_free(inputCube);
  return(C);
}



array_t *
Mc_CompletePath(
  mdd_t *aState,
  mdd_t *bState,
  mdd_t *invariantStates,
  Fsm_Fsm_t *modelFsm,
  array_t *careSetArray,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  Mc_FwdBwdAnalysis dirn)
{

  if ( dirn == McFwd_c )  {
    return McCompletePathFwd(aState, bState, invariantStates, modelFsm,
                             careSetArray, verbosity, dcLevel );
  }
  else {
    return McCompletePathBwd(aState, bState, invariantStates, modelFsm,
                             careSetArray, verbosity, dcLevel );
  }
}

mdd_t *
Mc_ComputeAMinterm(
  mdd_t *aSet,
  array_t *Support,
  mdd_manager *mddMgr)
{
  /* check that support of set is contained in Support */
  assert( SetCheckSupport( aSet, Support, mddMgr ));
  assert(!mdd_is_tautology(aSet, 0));

  if(bdd_get_package_name() == CUDD){
    mdd_t *range;             /* range of Support             */
    mdd_t *legalSet;          /* aSet without the don't cares */
    array_t *bddSupport;      /* Support in terms of bdd vars */
    mdd_t *minterm;           /* a random minterm             */

    range      = mdd_range_mdd(mddMgr, Support);
    legalSet   = bdd_intersects(aSet, range);
    mdd_free(range);
    bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support);
    minterm    = bdd_pick_one_minterm(legalSet, bddSupport);

    assert(MintermCheckWellFormed(minterm, Support, mddMgr));
    assert(mdd_count_onset(mddMgr, minterm, Support) == 1);
    assert(mdd_lequal(minterm,legalSet,1,1));

    mdd_array_free(bddSupport);
    mdd_free(legalSet);

    return minterm;
  }else{
    int i, j;
    mdd_t *aSetDup;
    mdd_t *resultMdd;
    array_t *resultMddArray = array_alloc( mdd_t *, 0 );

    aSetDup = mdd_dup( aSet );
    for( i = 0 ; i < array_n( Support ); i++ ) {

      int aSupportVar = array_fetch( int, Support, i );

      for( j = 0 ;;) {
        mdd_t *faceMdd, *tmpMdd;
        array_t *tmpArray = array_alloc( int, 0 );
        array_insert_last( int, tmpArray, j );

        /* this call will crash if have run through range of mvar */
        faceMdd = mdd_literal( mddMgr, aSupportVar, tmpArray );
        array_free( tmpArray );
        tmpMdd = mdd_and( faceMdd, aSetDup, 1, 1 );

        if ( !mdd_is_tautology( tmpMdd, 0 ) ) {
          array_insert_last( mdd_t *, resultMddArray, faceMdd );
          mdd_free( aSetDup );
          aSetDup = tmpMdd;
          break;
        }
        mdd_free( faceMdd );
        mdd_free( tmpMdd );
        j++;
      }
    }
    mdd_free( aSetDup );

    resultMdd = mdd_one( mddMgr );
    for ( i = 0 ; i < array_n( resultMddArray ); i++ ) {
      mdd_t *faceMdd = array_fetch( mdd_t *, resultMddArray, i );
      mdd_t *tmpMdd = mdd_and( faceMdd, resultMdd, 1, 1 );
      mdd_free( resultMdd ); mdd_free( faceMdd );
      resultMdd = tmpMdd;
    }
    array_free( resultMddArray );

    return resultMdd;
  }/* IF CUDD */
}


mdd_t *
Mc_ComputeACloseMinterm(
  mdd_t *aSet,
  mdd_t *target,
  array_t *Support,
  mdd_manager *mddMgr)
{
  if (bdd_get_package_name() == CUDD && target != NIL(mdd_t)) {
    mdd_t *range;             /* range of Support             */
    mdd_t *legalSet;          /* aSet without the don't cares */
    mdd_t *closeCube;
    int dist;
    array_t *bddSupport;      /* Support in terms of bdd vars */
    mdd_t *minterm;           /* a random minterm             */

    /* Check that support of set is contained in Support. */
    assert(SetCheckSupport(aSet, Support, mddMgr));
    assert(!mdd_is_tautology(aSet, 0));
    range      = mdd_range_mdd(mddMgr, Support);
    legalSet   = bdd_and(aSet, range, 1, 1);
    mdd_free(range);
    closeCube = mdd_closest_cube(legalSet, target, &dist);
    bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support);
    minterm    = bdd_pick_one_minterm(closeCube, bddSupport);

    assert(MintermCheckWellFormed(minterm, Support, mddMgr));
    assert(mdd_count_onset(mddMgr, minterm, Support) == 1);
    assert(mdd_lequal(minterm,legalSet,1,1));

    mdd_array_free(bddSupport);
    mdd_free(legalSet);
    mdd_free(closeCube);

    return minterm;
  } else {
    return Mc_ComputeAMinterm(aSet, Support, mddMgr);
  }/* if CUDD */

} /* McComputeACloseMinterm */




char *
Mc_MintermToStringAiger(
  mdd_t *aMinterm,
  array_t *aSupport,
  Ntk_Network_t *aNetwork)
{
  int i;
  char *tmp1String;
  char *tmp2String;
  char bodyString[McMaxStringLength_c];
  char *mintermString = NIL(char);
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork );
  array_t *valueArray;
  array_t *stringArray = array_alloc( char *, 0 );

  aMinterm = GET_NORMAL_PT(aMinterm);
  valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr);
  for ( i = 0 ; i < array_n( aSupport ); i++ ) {

    int mddId = array_fetch( int, aSupport, i );
    int value = array_fetch( int, valueArray, i );
    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
    char *nodeName = Ntk_NodeReadName( node );
    if(!((nodeName[0] == '$') && (nodeName[1] == '_')))
    {
      Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );

      if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
        char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar,
                                                                   value );
        sprintf( bodyString, "%s", symbolicValue );
      }
      else {
        sprintf( bodyString, "%d", value );
      }
      tmp1String = util_strsav( bodyString );
      array_insert_last( char *, stringArray, tmp1String );
    }
  }
  array_free(valueArray);

  array_sort( stringArray, cmp);

  for ( i = 0 ; i < array_n( stringArray ); i++ ) {
    tmp1String = array_fetch( char *, stringArray, i );
    if( i == 0 )  {
      mintermString = util_strcat3(tmp1String, "", "" );
    }
    else {
      tmp2String = util_strcat3(mintermString, "", tmp1String );
      FREE(mintermString);
      mintermString = tmp2String;
    }
    FREE(tmp1String);
  }
  array_free( stringArray );

  tmp1String = util_strcat3(mintermString, " ", "");
  FREE(mintermString);
  mintermString = tmp1String;

  return mintermString;
}


char *
Mc_MintermToStringAigerInput(
  mdd_t *aMinterm,
  array_t *aSupport,
  Ntk_Network_t *aNetwork)
{
  int i;
  char *tmp1String;
  char *tmp2String;
  char bodyString[McMaxStringLength_c];
  char *mintermString = NIL(char);
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork );
  array_t *valueArray;
  array_t *stringArray = array_alloc( char *, 0 );

  aMinterm = GET_NORMAL_PT(aMinterm);
  valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr);
  for ( i = 0 ; i < array_n( aSupport ); i++ ) {

    int mddId = array_fetch( int, aSupport, i );
    int value = array_fetch( int, valueArray, i );
    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
    char *nodeName = Ntk_NodeReadName( node );
    if((nodeName[0] == '$') && (nodeName[1] == '_'))
    {
      Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );

      if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
        char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar,
                                                                   value );
        sprintf( bodyString, "%s", symbolicValue );
      }
      else {
        sprintf( bodyString, "%d", value );
      }
      tmp1String = util_strsav( bodyString );
      array_insert_last( char *, stringArray, tmp1String );
    }
  }
  array_free(valueArray);

  array_sort( stringArray, cmp);

  for ( i = 0 ; i < array_n( stringArray ); i++ ) {
    tmp1String = array_fetch( char *, stringArray, i );
    if( i == 0 )  {
      mintermString = util_strcat3(tmp1String, "", "" );
    }
    else {
      tmp2String = util_strcat3(mintermString, "", tmp1String );
      FREE(mintermString);
      mintermString = tmp2String;
    }
    FREE(tmp1String);
  }
  array_free( stringArray );

  tmp1String = util_strcat3(mintermString, " ", "");
  FREE(mintermString);
  mintermString = tmp1String;

  return mintermString;
}

char *
Mc_MintermToString(
  mdd_t *aMinterm,
  array_t *aSupport,
  Ntk_Network_t *aNetwork)
{
  int i;
  char *tmp1String;
  char *tmp2String;
  char bodyString[McMaxStringLength_c];
  char *mintermString = NIL(char);
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( aNetwork );
  array_t *valueArray;
  array_t *stringArray = array_alloc( char *, 0 );

  aMinterm = GET_NORMAL_PT(aMinterm);
  valueArray = McConvertMintermToValueArray(aMinterm, aSupport, mddMgr);
  for ( i = 0 ; i < array_n( aSupport ); i++ ) {

    int mddId = array_fetch( int, aSupport, i );
    int value = array_fetch( int, valueArray, i );
    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
    char *nodeName = Ntk_NodeReadName( node );
    Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );

    if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
      char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar,
                                                                   value );
      sprintf( bodyString, "%s:%s", nodeName, symbolicValue );
    }
    else {
      sprintf( bodyString, "%s:%d", nodeName, value );
    }
    tmp1String = util_strsav( bodyString );
    array_insert_last( char *, stringArray, tmp1String );
  }
  array_free(valueArray);

  array_sort( stringArray, cmp);

  for ( i = 0 ; i < array_n( stringArray ); i++ ) {
    tmp1String = array_fetch( char *, stringArray, i );
    if( i == 0 )  {
      mintermString = util_strcat3(tmp1String, "", "" );
    }
    else {
      tmp2String = util_strcat3(mintermString, "\n", tmp1String );
      FREE(mintermString);
      mintermString = tmp2String;
    }
    FREE(tmp1String);
  }
  array_free( stringArray );

  tmp1String = util_strcat3(mintermString, "\n", "");
  FREE(mintermString);
  mintermString = tmp1String;

  return mintermString;
}

int
Mc_PrintPath(
  array_t *aPath,
  Fsm_Fsm_t *modelFsm,
  boolean printInput)
{
  int check, forced, i;
  int numForced;
  mdd_t *inputSet=NIL(mdd_t);
  mdd_t *uInput = NIL(mdd_t);
  mdd_t *vInput = NIL(mdd_t);

  array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );
  array_t *inputVars = Fsm_FsmReadInputVars( modelFsm );
  mdd_manager *mddMgr =  Fsm_FsmReadMddManager( modelFsm );

  forced = 0;
  check = 1;
  numForced = 0;


  for( i = -1 ; i < (array_n( aPath )-1); i++ ) {

    mdd_t *aState = ( i == -1 ) ? NIL(mdd_t) : array_fetch( mdd_t *, aPath, i );
    mdd_t *bState = array_fetch( mdd_t *, aPath, (i+1) );

    if((long)aState%2) {
      aState = (mdd_t *)((long)aState -1);
      forced++;
    }
    else        forced = 0;

    if((long)bState%2) {
      bState = (mdd_t *)((long)bState -1);
    }

    if ( printInput == TRUE && i != -1) {
      inputSet = Mc_FsmComputeDrivingInputMinterms( modelFsm, aState, bState );
      vInput = Mc_ComputeACloseMinterm( inputSet, uInput, inputVars, mddMgr );
    }
    if(forced)  {
      fprintf(vis_stdout, "---- Forced %d\n", forced);
      numForced ++;
    }
    McPrintTransition( aState, bState, uInput, vInput, psVars, inputVars,
                       printInput, modelFsm, (i+1) );


    if ( uInput != NIL(mdd_t) ) {
      mdd_free(uInput);
    }
    uInput = vInput;

    if ( inputSet != NIL(mdd_t) ) {
      mdd_free(inputSet);
    }
  }

  if ( vInput != NIL(mdd_t) ) {
    mdd_free(uInput);
  }

  if(Fsm_FsmReadFAFWFlag(modelFsm) > 0) {
    fprintf(vis_stdout,
        "# MC: the number of non-trivial forced segments %d\n",
        numForced);
  }

  return 1;
}

int
Mc_PrintPathAiger(
  array_t *aPath,
  Fsm_Fsm_t *modelFsm,
  boolean printInput)
{
  int check, forced, i;
  int numForced;
  mdd_t *inputSet=NIL(mdd_t);
  mdd_t *uInput = NIL(mdd_t);
  mdd_t *vInput = NIL(mdd_t);

  array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );
  array_t *inputVars = Fsm_FsmReadInputVars( modelFsm );

  forced = 0;
  check = 1;
  numForced = 0;

  Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm );

  FILE *psO = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0);
  for(i=0; i<array_n(psVars); i++)
  {
    int mddId = array_fetch( int, psVars, i );
    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
    char *nodeName = Ntk_NodeReadName( node );
    if((nodeName[0] == '$') && (nodeName[1] == '_'))
    {
      fprintf(psO, "%s\n", &nodeName[2]);
    }
  }
  fclose(psO);

  for( i = -1 ; i < (array_n( aPath )-1); i++ ) {

    mdd_t *aState = ( i == -1 ) ? NIL(mdd_t) : array_fetch( mdd_t *, aPath, i );
    mdd_t *bState = array_fetch( mdd_t *, aPath, (i+1) );

    if((long)aState%2) {
      aState = (mdd_t *)((long)aState -1);
      forced++;
    }
    else        forced = 0;

    if((long)bState%2) {
      bState = (mdd_t *)((long)bState -1);
    }

    if(forced)  {
      fprintf(vis_stdout, "---- Forced %d\n", forced);
      numForced ++;
    }

    /* The following fix is only for Sat-competition 2007 and will need to be fixed for future */

    if(i == (array_n(aPath)-2))
    {
      McPrintTransitionAiger( aState, bState, uInput, vInput, psVars, inputVars,
                       printInput, modelFsm, 1 );
    }
    else
    {
      McPrintTransitionAiger( aState, bState, uInput, vInput, psVars, inputVars,
                       printInput, modelFsm, 0 );
    }


    if ( uInput != NIL(mdd_t) ) {
      mdd_free(uInput);
    }
    uInput = vInput;

    if ( inputSet != NIL(mdd_t) ) {
      mdd_free(inputSet);
    }
  }

  if ( vInput != NIL(mdd_t) ) {
    mdd_free(uInput);
  }

  if(Fsm_FsmReadFAFWFlag(modelFsm) > 0) {
    fprintf(vis_stdout,
        "# MC: the number of non-trivial forced segments %d\n",
        numForced);
  }

  return 1;
}


static Mvf_Function_t *
NodeBuildPseudoInputMvf(
  Ntk_Node_t * node,
  mdd_manager * mddMgr)
{
  Mvf_Function_t *mvf;
  int             columnIndex = Ntk_NodeReadOutputIndex(node);
  Tbl_Table_t    *table       = Ntk_NodeReadTable(node);
  int             mddId       = Ntk_NodeReadMddId(node);

  assert(mddId != NTK_UNASSIGNED_MDD_ID);
  mvf = Tbl_TableBuildNonDetConstantMvf(table, columnIndex, mddId, mddMgr);
  return mvf;
}

static mdd_t *
Mc_ComputeRangeOfPseudoInputs(
  Ntk_Network_t *network)
{
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( network );
  Mvf_Function_t *nodeMvf;
  mdd_t *tmpMdd, *zeroMdd;
  mdd_t *restrictMdd, *sumMdd;
  int restrictFlag;
  lsGen gen;
  Ntk_Node_t *node;
  int i;

  zeroMdd = mdd_zero(mddMgr);
  restrictMdd = mdd_one(mddMgr);
  restrictFlag = 0;
  Ntk_NetworkForEachPseudoInput(network, gen, node) {
    nodeMvf = NodeBuildPseudoInputMvf(node, mddMgr);
    for(i=0; i<nodeMvf->num; i++) {
      tmpMdd = array_fetch(mdd_t *, nodeMvf, i);
      if(mdd_equal(tmpMdd, zeroMdd)) {
        restrictFlag = 1;
        break;
      }
    }
    if(restrictFlag) {
      sumMdd = mdd_zero(mddMgr);
      for(i=0; i<nodeMvf->num; i++) {
        tmpMdd = array_fetch(mdd_t *, nodeMvf, i);
        if(!mdd_equal(tmpMdd, zeroMdd)) {
          tmpMdd = mdd_or( sumMdd, tmpMdd, 1, 1 );
          mdd_free(sumMdd);
          sumMdd = tmpMdd;
        }
      }
      tmpMdd = mdd_and( sumMdd, restrictMdd, 1, 1 );
      mdd_free(sumMdd);
      mdd_free(restrictMdd);
      restrictMdd = tmpMdd;
    }
    Mvf_FunctionFree(nodeMvf);
  }
  mdd_free(zeroMdd);

  return(restrictMdd);
}


mdd_t *
Mc_FsmComputeDrivingInputMinterms(
  Fsm_Fsm_t *fsm,
  mdd_t *aState,
  mdd_t *bState )
{
  int i;
  int psMddId;
  int inputMddId;
  mdd_gen *mddGen;
  Ntk_Node_t *latch, *node, *dataNode;
  array_t *aMinterm, *bMinterm;
  mdd_t *resultMdd;
  array_t *resultMvfs;
  array_t *inputArray = Fsm_FsmReadInputVars( fsm );
  array_t *psArray = Fsm_FsmReadPresentStateVars( fsm );
  Ntk_Network_t *network = Fsm_FsmReadNetwork( fsm );
  st_table *leaves = st_init_table(st_ptrcmp, st_ptrhash);
  array_t *roots = array_alloc( Ntk_Node_t *, 0 );
  array_t *latches = array_alloc( Ntk_Node_t *, 0 );
  array_t *support = array_alloc( int, 0 );
  mdd_t *rangeOfPseudoInputs, *tmpMdd;

  arrayForEachItem(int , psArray, i, psMddId ) {
    latch = Ntk_NetworkFindNodeByMddId( network, psMddId );
    dataNode = Ntk_LatchReadDataInput( latch );
    array_insert_last( int, support, psMddId );
    array_insert_last( Ntk_Node_t *, roots, dataNode );
    array_insert_last( Ntk_Node_t *, latches, latch );
  }

  /* Convert the  minterm to an array of assignments to support vars. */
  foreach_mdd_minterm(aState, mddGen, aMinterm, support) {
    mdd_gen_free(mddGen);
    break;
    /* NOT REACHED */
  }

  foreach_mdd_minterm(bState, mddGen, bMinterm, support) {
    mdd_gen_free(mddGen);
    break;
     /* NOT REACHED */
  }
  array_free( support );

  arrayForEachItem(int , inputArray, i, inputMddId ) {
    node = Ntk_NetworkFindNodeByMddId( network, inputMddId );
    st_insert(leaves, (char *) node, (char *) NTM_UNUSED );
  }

  for ( i = 0 ; i < array_n( roots ); i++ ) {
    int value = array_fetch( int, aMinterm, i );
    latch = array_fetch( Ntk_Node_t *, latches, i );
    st_insert( leaves, (char *) latch, (char *) (long) value );
  }

  resultMvfs = Ntm_NetworkBuildMvfs( network, roots, leaves, NIL(mdd_t) );

  array_free( roots );
  array_free( latches );
  st_free_table( leaves );

  rangeOfPseudoInputs = Mc_ComputeRangeOfPseudoInputs(network);

  resultMdd = rangeOfPseudoInputs;
  for ( i = 0 ; i < array_n( resultMvfs ) ; i++ ) {
    Mvf_Function_t *mvf = array_fetch( Mvf_Function_t *, resultMvfs, i );
    int value = array_fetch( int, bMinterm, i );
    mdd_t *activeMdd = Mvf_FunctionReadComponent( mvf, value );
    tmpMdd = mdd_and( activeMdd, resultMdd, 1, 1 );
    if(mdd_is_tautology(tmpMdd, 0)) {
        fprintf(stdout, "current error\n");
    }
    mdd_free( resultMdd );
    resultMdd = tmpMdd;
    Mvf_FunctionFree( mvf );
  }
  array_free( resultMvfs);
  array_free( aMinterm );
  array_free( bMinterm );

  return resultMdd;
}


mdd_t *
Mc_ComputeAState(
  mdd_t *states,
  Fsm_Fsm_t *modelFsm)
{
  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
  mdd_t *result = Mc_ComputeAMinterm( states, PSVars, mddMgr );

  return result;
}


mdd_t *
Mc_ComputeACloseState(
  mdd_t *states,
  mdd_t *target,
  Fsm_Fsm_t *modelFsm)
{
  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
  mdd_t *result = Mc_ComputeACloseMinterm( states, target, PSVars, mddMgr );

  return result;
}


void
Mc_MintermPrint(
  mdd_t *aMinterm,
  array_t *support,
  Ntk_Network_t *aNetwork)
{
  char *tmpString = Mc_MintermToString( aMinterm, support, aNetwork );
  fprintf( vis_stdout, "%s", tmpString );
  FREE(tmpString);
}

void
Mc_NodeTableAddCtlFormulaNodes(
  Ntk_Network_t *network,
  Ctlp_Formula_t *formula,
  st_table * nodesTable )
{
  NodeTableAddCtlFormulaNodes( network, formula, nodesTable );
}

void
Mc_NodeTableAddLtlFormulaNodes(
  Ntk_Network_t *network,
  Ctlsp_Formula_t *formula,
  st_table * nodesTable )
{
  NodeTableAddLtlFormulaNodes(network, formula, nodesTable);
}

Fsm_Fsm_t *
Mc_ConstructReducedFsm(
  Ntk_Network_t *network,
  array_t *ctlFormulaArray)
{
  return(McConstructReducedFsm(network, ctlFormulaArray));
}


Mc_GSHScheduleType
Mc_StringConvertToScheduleType(
  char *string)
{
  return McStringConvertToScheduleType(string);
}

int
Mc_StringConvertToLockstepMode(
  char *string)
{
  return McStringConvertToLockstepMode(string);
}


Mc_EarlyTermination_t *
Mc_EarlyTerminationAlloc(
  Mc_EarlyTerminationType mode,
  mdd_t *states)
{
  Mc_EarlyTermination_t *result = ALLOC(Mc_EarlyTermination_t, 1);

  result->mode   = mode;
  if (states != NIL(mdd_t)) {
    result->states = mdd_dup(states);
  } else {
    result->states = NIL(mdd_t);
  }

  return result;
}

void
Mc_EarlyTerminationFree(Mc_EarlyTermination_t *earlyTermination)
{
  if(earlyTermination == NIL(Mc_EarlyTermination_t) ||
     earlyTermination == MC_NO_EARLY_TERMINATION)
    return;

  if(earlyTermination->states != NIL(mdd_t))
    mdd_free(earlyTermination->states);

  free(earlyTermination);

  return;
}

boolean
Mc_EarlyTerminationIsSkip(Mc_EarlyTermination_t *earlyTermination)
{
  if (earlyTermination == NIL(Mc_EarlyTermination_t) ||
     earlyTermination == MC_NO_EARLY_TERMINATION)
    return FALSE;

  return (earlyTermination->mode == McCare_c &&
          earlyTermination->states == NIL(mdd_t));

}

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

array_t *
McCompletePathFwd(
  mdd_t *aState,
  mdd_t *bState,
  mdd_t *invariantStates,
  Fsm_Fsm_t *modelFsm,
  array_t *careSetArray,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  mdd_t *tmp1Mdd;
  array_t *result;
  mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
  mdd_t *zeroMdd = mdd_zero( mddMgr );
  array_t *onionRings = array_alloc( mdd_t *, 0 );
  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
  mdd_t *c0, *c1;

  assert( mdd_lequal( aState, invariantStates, 1, 1 ) );
  assert( mdd_lequal( bState, invariantStates, 1, 1 ) );

  if ( mdd_equal( aState, bState ) ) {

    /*
     * Alter the starting point to force routine to produce cycle if exists
     * Question: would it be quicker to do simultaneous backward/forward
     * analysis?
     */

    c0 = mdd_dup( aState );
    array_insert_last( mdd_t *, onionRings, c0 );

    tmp1Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
                aState, aState, careSetArray);
    c1 = mdd_and( tmp1Mdd, invariantStates, 1, 1 );
    mdd_free(tmp1Mdd);
    array_insert_last( mdd_t *, onionRings, c1 );
  }
  else {
    c0 = zeroMdd;
    c1 = mdd_dup( aState );
    array_insert_last( mdd_t *, onionRings, c1 );
  }

  while (!mdd_equal_mod_care_set_array(c0, c1, careSetArray)) {

    mdd_t *tmp2Mdd;

    if ( McStateTestMembership( bState, c1 ) ) {
      break;
    }

    /*
     *  performance gain from using dc's in this fp computation.
     *  use only when dclevel >= max
     */
    if ( dcLevel >= McDcLevelRchFrontier_c ) {
      mdd_t *annulusMdd = mdd_and(  c0, c1, 0, 1 );
      mdd_t *discMdd = mdd_dup( c1 );
      mdd_t *dcMdd = bdd_between( annulusMdd, discMdd );

      tmp2Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
                        annulusMdd, discMdd, careSetArray);

      if ( verbosity > McVerbosityNone_c ) {
        fprintf(vis_stdout,
                "--Fwd completion: |low| = %d\t|upper| = %d\t|between|=%d\n",
                mdd_size(annulusMdd), mdd_size(discMdd), mdd_size(dcMdd));
      }

      mdd_free( annulusMdd );
      mdd_free( discMdd );
      mdd_free( dcMdd );
    }
    else {
      tmp2Mdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, c1, c1,
                                                        careSetArray);
    }

    tmp1Mdd = mdd_and( tmp2Mdd, invariantStates, 1, 1);
    mdd_free(tmp2Mdd);

    c0 = c1;
    c1 = mdd_or( c1, tmp1Mdd, 1, 1 );
    mdd_free( tmp1Mdd );

    array_insert_last( mdd_t *, onionRings, c1 );
  }

  if ( McStateTestMembership( bState, c1 ) )  {
    result = Mc_BuildPathFromCore(bState, onionRings, modelFsm,
                                  McGreaterZero_c );
  }
  else {
    result = NIL(array_t);
  }

  mdd_free( zeroMdd );
  mdd_array_free( onionRings);

  return result;
}

array_t *
McCompletePathBwd(
  mdd_t *aState,
  mdd_t *bState,
  mdd_t *invariantStates,
  Fsm_Fsm_t *modelFsm,
  array_t *careSetArray,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel)
{
  mdd_t *tmp1Mdd;
  array_t *result;
  mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
  mdd_t *zeroMdd = mdd_zero( mddMgr );
  array_t *onionRings = array_alloc( mdd_t *, 0 );
  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
  mdd_t *c0, *c1;


  assert( mdd_lequal( aState, invariantStates, 1, 1 ) );
  assert( mdd_lequal( bState, invariantStates, 1, 1 ) );

  if ( mdd_equal( aState, bState ) ) {

    /*
     * Alter the starting point to force routine to produce cycle if exists
     * Question: would it be quicker to do simultaneous backward/forward
     * analysis?
     */

    c0 = mdd_dup( bState );
    array_insert_last( mdd_t *, onionRings, c0 );

    tmp1Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, bState,
                                                         bState, careSetArray);
    c1 = mdd_and( tmp1Mdd, invariantStates, 1, 1 );
    mdd_free(tmp1Mdd);
    array_insert_last( mdd_t *, onionRings, c1 );
  }
  else {
    c0 = zeroMdd;
    c1 = mdd_dup( bState );
    array_insert_last( mdd_t *, onionRings, c1 );
  }

  while (!mdd_equal_mod_care_set_array(c0, c1, careSetArray)) {

    mdd_t *tmp2Mdd;

    if ( McStateTestMembership( aState, c1 ) ) {
      break;
    }

    /*
     *  performance gain from using dc's in this fp computation.
     *  use only when dclevel >= max
     */
    if ( dcLevel >= McDcLevelRchFrontier_c ) {
      mdd_t *annulusMdd = mdd_and(  c0, c1, 0, 1 );
      mdd_t *discMdd = mdd_dup( c1 );
      mdd_t *dcMdd = bdd_between( annulusMdd, discMdd );

      tmp2Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
                        annulusMdd, discMdd, careSetArray);

      if ( verbosity > McVerbosityNone_c ) {
        fprintf(vis_stdout,
                "--Bwd completion: |low| = %d\t|upper| = %d\t|between|=%d\n",
                mdd_size(annulusMdd), mdd_size(discMdd), mdd_size(dcMdd));
      }

      mdd_free( annulusMdd );
      mdd_free( discMdd );
      mdd_free( dcMdd );
    }
    else {
      tmp2Mdd = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, c1, c1,
                                                           careSetArray);
    }

    tmp1Mdd = mdd_and( tmp2Mdd, invariantStates, 1, 1);
    mdd_free(tmp2Mdd);

    c0 = c1;
    c1 = mdd_or( c1, tmp1Mdd, 1, 1 );
    mdd_free( tmp1Mdd );

    array_insert_last( mdd_t *, onionRings, c1 );
  }

  if ( McStateTestMembership( aState, c1 ) )  {
    result = Mc_BuildPathToCore(aState, onionRings, modelFsm, McGreaterZero_c);
  }
  else {
    result = NIL(array_t);
  }

  mdd_free( zeroMdd );
  mdd_array_free( onionRings);

  return result;
}

int
McCommandInitState(
  Hrc_Manager_t **hmgr,
  int argc,
  char **argv)
{
  mdd_t *modelInitialStates;
  mdd_t *anInitialState;
  Fsm_Fsm_t *modelFsm;
  char *formulaTxt;
  array_t *stateVars;
  FILE *ctlFile;

  if ( argc == 1 ) {
    ctlFile = vis_stdout;
  }
  else {
    if ( !strcmp( "-h", argv[1] ) || ( argc > 2 ) ) {
      fprintf( vis_stdout, "Usage: _init_state_formula [-h] init_file\n\tinit_file - file to write init state formula to (default is stdout)\n");
      return 1;
    }
    ctlFile = Cmd_FileOpen( argv[1], "w", NIL(char *), 0 );
  }

  modelFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  if (modelFsm == NIL(Fsm_Fsm_t)) {
    if ( argc != 1 ) {
      fclose( ctlFile );
    }
    return 1;
  }
  stateVars = Fsm_FsmReadPresentStateVars( modelFsm );

  modelInitialStates = Fsm_FsmComputeInitialStates( modelFsm );
  if ( modelInitialStates == NIL(mdd_t) ) {
    (void) fprintf( vis_stdout, "** mc error: - cant build init states (mutual latch dependancy?)\n%s\n",
                    error_string() );
    if ( argc != 1 ) {
      fclose( ctlFile );
    }
    return 1;
  }
  anInitialState = Mc_ComputeAState( modelInitialStates, modelFsm );
  mdd_free(modelInitialStates);

  formulaTxt = McStatePrintAsFormula( anInitialState, stateVars, modelFsm );
  mdd_free(anInitialState);

  fprintf( ctlFile, "AG EF %s;\n", formulaTxt );
  FREE(formulaTxt);

  if ( argc != 1 ) {
    fclose(ctlFile);
  }

  return 0;
}



char *
McStatePrintAsFormula(
  mdd_t *aMinterm,
  array_t *aSupport,
  Fsm_Fsm_t *modelFsm)
{
  int i;
  char *tmp1String;
  char *tmp2String;
  char *tmp3String;
  char bodyString[McMaxStringLength_c];
  char *mintermString = NIL(char);
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
  Ntk_Network_t *aNetwork = Fsm_FsmReadNetwork( modelFsm );
  array_t *valueArray = McConvertMintermToValueArray( aMinterm, aSupport, mddMgr );
  array_t *stringArray = array_alloc( char *, 0 );

  for ( i = 0 ; i < array_n( aSupport ); i++ ) {

    int mddId = array_fetch( int, aSupport, i );
    int value = array_fetch( int, valueArray, i );
    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
    char *nodeName = Ntk_NodeReadName( node );
    Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );

    if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
      char *symbolicValue = Var_VariableReadSymbolicValueFromIndex( nodeVar, value );
      sprintf( bodyString, "%s=%s", nodeName, symbolicValue );
    }
    else {
      sprintf( bodyString, "%s=%d", nodeName, value );
    }
    tmp1String = util_strsav( bodyString );
    array_insert_last( char *, stringArray, tmp1String );
  }
  array_free(valueArray);

  array_sort( stringArray, cmp);

  for ( i = 0 ; i < array_n( stringArray ); i++ ) {
    tmp1String = array_fetch( char *, stringArray, i );
    if( i == 0 )  {
      mintermString = util_strcat3("(", tmp1String, ")" );
    }
    else {
      tmp2String = util_strcat3( mintermString, " * (", tmp1String );
      FREE(mintermString);
      tmp3String = util_strcat3( tmp2String, ")", "" );
      FREE(tmp2String);
      mintermString = tmp3String;
    }
    FREE(tmp1String);
  }
  array_free( stringArray );

  tmp1String = util_strcat3( "( ", mintermString, " )" );
  FREE(mintermString);
  mintermString = tmp1String;

  return mintermString;
}

int
McComputeOnionRingsWithClosestCore(
  mdd_t *aState,
  array_t *arrayOfOnionRings,
  Fsm_Fsm_t *modelFsm)
{
  int index;
  int distance = 0;

  while( TRUE ) {
    for( index = 0 ; index < array_n( arrayOfOnionRings ) ; index++ ) {
      array_t *iOnionRings = array_fetch( array_t *, arrayOfOnionRings, index );

      /* will crash if run out of rings -> if not in there */
      mdd_t *stateSet = array_fetch( mdd_t *, iOnionRings, distance );

      if ( McStateTestMembership( aState, stateSet ) )
        return index;
    }
    distance++;
  }
  assert(0);
}



array_t *
McRemoveIndexedOnionRings(
  int index,
  array_t *arrayOfOnionRings)
{
  int i;
  array_t *dupArrayOfOnionRings = array_alloc( array_t *, 0 );
  array_t *OnionRings;

  for ( i = 0 ; i < array_n( arrayOfOnionRings ) ; i++ ) {
    if ( i == index ) {
      continue;
    }
    OnionRings = array_fetch( array_t *, arrayOfOnionRings, i );
    array_insert_last( array_t *, dupArrayOfOnionRings, OnionRings );
  }

  return dupArrayOfOnionRings;
}







array_t *
McConvertMintermToValueArray(
  mdd_t *aMinterm,
  array_t *aSupport,
  mdd_manager *mddMgr)
{
  array_t *resultValueArray;

  /* this will be performed only in v0s-g executables */
  assert( MintermCheckWellFormed( aMinterm, aSupport, mddMgr ));

  resultValueArray = array_alloc( int, 0 );
  {
    int i;
    for( i = 0 ; i < array_n( aSupport ); i++ ) {
      int aSupportVar = array_fetch( int, aSupport, i );
      int j;
      for( j = 0 ; TRUE ; j++) {

        mdd_t *faceMdd, *tmpMdd;
        array_t *tmpArray = array_alloc( int, 0 );

        array_insert_last( int, tmpArray, j );
        faceMdd = mdd_literal( mddMgr, aSupportVar, tmpArray );
        array_free( tmpArray );

        tmpMdd = mdd_and( faceMdd, aMinterm, 1, 1 );
        mdd_free( faceMdd );
        if ( !mdd_is_tautology( tmpMdd, 0 ) ) {
          mdd_free( tmpMdd );
          array_insert_last( int, resultValueArray, j );
          break;
        }
        mdd_free( tmpMdd );
      }
    }
  }

  return resultValueArray;
}





void
McPrintTransitionAiger(
  mdd_t *aState,
  mdd_t *bState,
  mdd_t *uInput,
  mdd_t *vInput,
  array_t *stateSupport,
  array_t *inputSupport,
  boolean printInputs,
  Fsm_Fsm_t *modelFsm,
  int seqNumber)
{
  Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm );
  char *aString = aState ? Mc_MintermToStringAiger( aState, stateSupport, modelNetwork ) : NIL(char);
  char *bString = Mc_MintermToStringAiger( bState, stateSupport, modelNetwork );
  char *inpString = aState ? Mc_MintermToStringAigerInput( aState, stateSupport, modelNetwork ) : NIL(char);

  st_table   *node2MvfAigTable;

  node2MvfAigTable =
        (st_table *)Ntk_NetworkReadApplInfo(modelNetwork, MVFAIG_NETWORK_APPL_KEY);

  if ( aState == NIL(mdd_t) ) {
    FREE(bString);
    return;
  }

  fprintf(vis_stdout, "%s", aString);
  fprintf(vis_stdout, "%s", inpString);


   /* first test that there are inputs */
  /* if ( array_n( inputSupport ) > 0 ) {
    if ( uInput == NIL(mdd_t) ) {
      char *vString = Mc_MintermToStringAiger( vInput, inputSupport, modelNetwork );
      FREE(vString);
    }
    else {
      boolean unchanged=TRUE;
      char *uString = Mc_MintermToStringAiger( uInput, inputSupport, modelNetwork );
      char *vString = Mc_MintermToStringAiger( vInput, inputSupport, modelNetwork );
      FREE(uString);
      FREE(vString);
    }
  } */

  if(seqNumber == 1)
  {
    fprintf(vis_stdout, "1 ");
  }
  else
  {
    fprintf(vis_stdout, "0 ");
  }


  fprintf(vis_stdout, "%s", bString);

  FREE( aString );
  FREE( bString );
  fprintf (vis_stdout, "\n");
  return;
}




void
McPrintTransition(
  mdd_t *aState,
  mdd_t *bState,
  mdd_t *uInput,
  mdd_t *vInput,
  array_t *stateSupport,
  array_t *inputSupport,
  boolean printInputs,
  Fsm_Fsm_t *modelFsm,
  int seqNumber)
{
  Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm );
  char *aString = aState ? Mc_MintermToString( aState, stateSupport, modelNetwork ) : NIL(char);
  char *bString = Mc_MintermToString( bState, stateSupport, modelNetwork );

  char *tmp1String = aString;
  char *tmp2String = bString;
  char *ptr1;
  char *ptr2;
  st_table   *node2MvfAigTable;

  node2MvfAigTable =
        (st_table *)Ntk_NetworkReadApplInfo(modelNetwork, MVFAIG_NETWORK_APPL_KEY);

  if ( aState == NIL(mdd_t) ) {
    fprintf( vis_stdout, "--State %d:\n%s\n", seqNumber, bString );
    FREE(bString);
    return;
  }

  fprintf(vis_stdout, "--Goes to state %d:\n", seqNumber );

  {
    boolean unchanged=TRUE;
    while ( (tmp1String != NIL(char)) && ((ptr1 = strchr( tmp1String, '\n' ) ) != NIL(char) ) ) {
      ptr2 = strchr( tmp2String, '\n' );
      *ptr1 = 0;
      *ptr2 = 0;
      if ( (strcmp( tmp1String, tmp2String ) ) ) {
        fprintf( vis_stdout, "%s\n", tmp2String );
        unchanged = FALSE;
      }
      tmp1String = & (ptr1[1]);
      tmp2String = & (ptr2[1]);
    }
    if (unchanged == TRUE) {
      fprintf( vis_stdout, "<Unchanged>\n");
    }
  }


  if ( printInputs == TRUE ) {
    /* first test that there are inputs */
    if ( array_n( inputSupport ) > 0 ) {
      fprintf(vis_stdout, "--On input:\n");
      if ( uInput == NIL(mdd_t) ) {
        char *vString = Mc_MintermToString( vInput, inputSupport, modelNetwork );
        fprintf(vis_stdout, "%s", vString );
        FREE(vString);
      }
      else {
        boolean unchanged=TRUE;
        char *uString = Mc_MintermToString( uInput, inputSupport, modelNetwork );
        char *vString = Mc_MintermToString( vInput, inputSupport, modelNetwork );
        tmp1String = uString;
        tmp2String = vString;
        while ( (tmp1String != NIL(char)) && ((ptr1 = strchr( tmp1String, '\n' ) ) != NIL(char) ) ) {
          ptr2 = strchr( tmp2String, '\n' );
          *ptr1 = 0;
          *ptr2 = 0;
          if ( (strcmp( tmp1String, tmp2String ) ) ) {
            fprintf( vis_stdout, "%s\n", tmp2String );
            unchanged = FALSE;
          }
          tmp1String = & (ptr1[1]);
          tmp2String = & (ptr2[1]);
        }
        if (unchanged == TRUE) {
          fprintf( vis_stdout, "<Unchanged>\n");
        }
        FREE(uString);
        FREE(vString);
      }
    }
  }

  FREE( aString );
  FREE( bString );
  fprintf (vis_stdout, "\n");
}


void
McStatePassesFormula(
  mdd_t *aState,
  Ctlp_Formula_t *formula,
  McDbgLevel debugLevel,
 Fsm_Fsm_t *modelFsm)
{
  McStatePassesOrFailsFormula( aState, formula, 1, debugLevel,  modelFsm );
}


void
McStateFailsFormula(
  mdd_t *aState,
  Ctlp_Formula_t *formula,
  McDbgLevel debugLevel,
  Fsm_Fsm_t *modelFsm)
{
  McStatePassesOrFailsFormula( aState, formula, 0,  debugLevel, modelFsm );
}


void
McStatePassesOrFailsFormula(
  mdd_t *aState,
  Ctlp_Formula_t *formula,
  int pass,
  McDbgLevel debugLevel,
  Fsm_Fsm_t *modelFsm)
{
  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
  char *formulaText = Ctlp_FormulaConvertToString( formula );
  Ntk_Network_t *modelNetwork = Fsm_FsmReadNetwork( modelFsm );

  /* Nodes created in converting formulae like AU may not have text
   * attached to them. */
  if (formulaText == NIL(char))
    return;

  fprintf( vis_stdout, "--State\n");
  Mc_MintermPrint( aState, PSVars, modelNetwork );
  if ( pass )
    fprintf( vis_stdout, "passes ");
  else
    fprintf( vis_stdout, "fails ");

  if( debugLevel > McDbgLevelMin_c)
    fprintf(vis_stdout, "%s.\n\n", formulaText);
  else
    fprintf(vis_stdout, "\n\n");

  FREE(formulaText);
}



McPath_t *
McPathNormalize(
  McPath_t *aPath)
{
  int i, j;
  int forced;

  array_t *stemArray = McPathReadStemArray( aPath );
  array_t *cycleArray = McPathReadCycleArray( aPath );

  McPath_t *result = McPathAlloc();
  array_t *newStem = array_alloc( mdd_t *, 0 );
  array_t *newCycle = array_alloc( mdd_t *, 0 );

  mdd_t *lastState = GET_NORMAL_PT(array_fetch_last(mdd_t *, cycleArray));

  McPathSetStemArray( result, newStem );
  McPathSetCycleArray( result, newCycle );

  for( i = 0 ; i < array_n( stemArray ) ; i++ ) {
    mdd_t *tmpState = array_fetch( mdd_t *, stemArray, i );
    forced = 0;
    if((long)tmpState % 2) {
       forced = 1;
       tmpState = (mdd_t *)((long)tmpState - 1);
    }
    array_insert_last(mdd_t *, newStem,
            (mdd_t *)((long)(mdd_dup(tmpState)) + forced) );

    if ( mdd_equal( lastState, tmpState ) ) {
      break;
    }
  }

  for( j = i; j < array_n( stemArray ); j++ ) {
    mdd_t *tmpState = array_fetch( mdd_t *, stemArray, j );
    forced = 0;
    if((long)tmpState % 2) {
       forced = 1;
       tmpState = (mdd_t *)((long)tmpState - 1);
    }

    array_insert_last(mdd_t *, newCycle,
            (mdd_t *)((long)(mdd_dup(tmpState)) + forced) );

  }

  /* first state of cycle array == last state of stem array => start from j=1 */
  for( j = 1; j < array_n( cycleArray ); j++ ) {
    mdd_t *tmpState = array_fetch( mdd_t *, cycleArray, j );
    forced = 0;
    if((long)tmpState % 2) {
       forced = 1;
       tmpState = (mdd_t *)((long)tmpState - 1);
    }
    array_insert_last(mdd_t *, newCycle,
            (mdd_t *)((long)(mdd_dup(tmpState)) + forced) );

  }

  return result;

}



array_t *
McCreateMergedPath(
  array_t *aPath,
  array_t *bPath)
{
  int i, pos, forced;
  mdd_t *tmpState, *endOfAPath;
  array_t *aPathDup = McMddArrayDuplicateFAFW( aPath );
  array_t *bPathDup = McMddArrayDuplicateFAFW( bPath );

  for( i = 1 ; i < array_n( bPathDup ) ; i++ ) {
    tmpState = array_fetch( mdd_t *, bPathDup, i );
    array_insert_last( mdd_t *, aPathDup, tmpState );
  }
  pos = array_n(aPathDup) - array_n(bPathDup);
  endOfAPath = array_fetch(mdd_t *, aPathDup, pos);

  tmpState = array_fetch( mdd_t *, bPathDup, 0 );
  forced = 0;
  if((long)tmpState % 2) {
    forced = 1;
    tmpState = (mdd_t *)((long)tmpState - 1);
  }
  if(forced && mdd_equal(tmpState, endOfAPath)) {
    array_insert(mdd_t *, aPathDup, pos, (mdd_t *)((long)endOfAPath + forced) );
  }

  mdd_free( tmpState );
  array_free( bPathDup );

  return aPathDup;
}

array_t *
McMddArrayDuplicateFAFW(array_t *mddArray)
{
  int   i, forced;
  mdd_t *newTempMdd;
  int      length = array_n(mddArray);
  array_t *result = array_alloc(mdd_t *, length);

  for (i = 0; i < length; i++) {
    mdd_t *tempMdd = array_fetch(mdd_t *, mddArray, i);
    forced = 0;
    if((long)tempMdd % 2) {
      forced = 1;
      tempMdd = (mdd_t *)((long)tempMdd - 1);
    }

    newTempMdd = mdd_dup(tempMdd);
    array_insert(mdd_t *, result, i, (mdd_t *)((long)newTempMdd + forced));
  }

  return (result);
}

mdd_t *
McMddArrayAnd(array_t *mddArray)
{
  mdd_t *result, *mdd1, *mdd2 = NIL(mdd_t);
  int i;

  result = NIL(mdd_t);
  arrayForEachItem(mdd_t *, mddArray, i, mdd1) {
    if (result == NIL(mdd_t))
      result = mdd_dup(mdd1);
    else {
      mdd2 = result;
      result = mdd_and(result, mdd1, 1, 1);
      mdd_free(mdd2);
    }
  }

  return (result);
}

mdd_t *
McMddArrayOr(array_t *mddArray)
{
  mdd_t *result, *mdd1, *mdd2 = NIL(mdd_t);
  int i;

  result = NIL(mdd_t);
  arrayForEachItem(mdd_t *, mddArray, i, mdd1) {
    if (result == NIL(mdd_t))
      result = mdd_dup(mdd1);
    else {
      mdd2 = result;
      result = mdd_or(result, mdd1, 1, 1);
      mdd_free(mdd2);
    }
  }

  return (result);
}

array_t *
McCreateJoinedPath(
  array_t *aPath,
  array_t *bPath)
{
  int i;
  mdd_t *tmpState;
  array_t *aPathDup = McMddArrayDuplicateFAFW( aPath );
  array_t *bPathDup = McMddArrayDuplicateFAFW( bPath );

  for( i = 0 ; i < array_n( bPathDup ) ; i++ ) {
    tmpState = array_fetch( mdd_t *, bPathDup, i );
    array_insert_last( mdd_t *, aPathDup, tmpState );
  }
  array_free( bPathDup );

  return aPathDup;
}


boolean
McStateSatisfiesFormula(
  Ctlp_Formula_t *aFormula,
  mdd_t *aState )
{
  mdd_t *passStates = Ctlp_FormulaObtainLatestApprox( aFormula );

  if ( mdd_lequal( aState, passStates, 1, 1 ) ) {
    mdd_free( passStates );
    return TRUE;
  }
  else {
    mdd_free( passStates );
    return FALSE;
  }
}



boolean
McStateTestMembership(
  mdd_t *aState,
  mdd_t *setOfStates )
{
  return mdd_lequal( aState, setOfStates, 1, 1 );
}

mdd_t *
McGetSuccessorInTarget(
  mdd_t *aState,
  mdd_t *targetStates,
  Fsm_Fsm_t *modelFsm )
{
  mdd_t *tmpMdd, *succsInTarget, *result;
  array_t *careSetArray = array_alloc(mdd_t *, 0);
  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);

  array_insert_last(mdd_t *, careSetArray, targetStates);
  tmpMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, aState,
                                                   aState, careSetArray);
  array_free(careSetArray);
  succsInTarget = mdd_and(tmpMdd, targetStates, 1, 1);
#if 1
  result = Mc_ComputeAState(succsInTarget, modelFsm);
#else
  result = Mc_ComputeACloseState(succsInTarget, aState, modelFsm);
#endif

  mdd_free( tmpMdd );
  mdd_free( succsInTarget );

  return result;
}

mdd_t *
McGetSuccessorInTargetAmongFairStates(
  mdd_t *aState,
  mdd_t *targetStates,
  array_t *arrayOfOnionRings,
  Fsm_Fsm_t *modelFsm )
{
  mdd_t *tmpMdd, *succsInTarget, *result;
  mdd_t *fairStates, *newFairStates, *onionRing;
  mdd_t *targetStatesInFairStates;
  array_t *onionRings;
  int i, j;
  array_t *careSetArray = array_alloc(mdd_t *, 0);

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


  fairStates = 0;
  for(i=0; i<array_n(arrayOfOnionRings); i++) {
    onionRings = array_fetch(array_t *, arrayOfOnionRings, i);
    for(j=0; j<array_n(onionRings); j++) {
      onionRing = array_fetch(mdd_t *,onionRings, j);

      if(fairStates) {
        newFairStates = mdd_or(fairStates, onionRing, 1, 1);
        mdd_free(fairStates);
        fairStates = newFairStates;
      }
      else {
        fairStates = mdd_dup(onionRing);
      }
    }
  }
  targetStatesInFairStates = mdd_and(fairStates, targetStates, 1, 1);
  mdd_free(fairStates);

  array_insert_last(mdd_t *, careSetArray, targetStatesInFairStates);
  tmpMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, aState,
                                                   aState, careSetArray);
  succsInTarget = mdd_and(tmpMdd, targetStatesInFairStates, 1, 1);
  mdd_array_free(careSetArray);
  result = Mc_ComputeACloseState(succsInTarget, aState, modelFsm);

  mdd_free( tmpMdd );
  mdd_free( succsInTarget );

  return result;
}


array_t *
McPathReadStemArray(
  McPath_t *aPath )
{
  return aPath->stemArray;
}

array_t *
McPathReadCycleArray(
  McPath_t *aPath )
{
  return aPath->cycleArray;
}

void
McPathSetStemArray(
  McPath_t *aPath,
  array_t *stemArray)
{
  aPath->stemArray = stemArray;
}

void
McPathSetCycleArray(
  McPath_t *aPath,
  array_t *cycleArray )
{
  aPath->cycleArray = cycleArray;
}

McPath_t *
McPathAlloc(void)
{
  McPath_t *tmpPath = ( McPath_t * ) malloc( sizeof( McPath_t ) );

  tmpPath->stemArray = NIL(array_t);
  tmpPath->cycleArray = NIL(array_t);

  return tmpPath;
}

void
McNormalizeBddPointer(array_t *bddArray)
{
  int i;
  bdd_t *p;

  for(i=0; i<array_n(bddArray); i++) {
    p = array_fetch(bdd_t *, bddArray, i);
    if((long)p%2) p = (mdd_t *)( (long)p -1 );
    array_insert(bdd_t *, bddArray, i, p);
  }
}

void
McPathFree(
  McPath_t * aPath )
{
  if ( aPath->stemArray ) {
    McNormalizeBddPointer(aPath->stemArray);
    mdd_array_free( aPath->stemArray );
  }

  if ( aPath->cycleArray ) {
    McNormalizeBddPointer(aPath->cycleArray);
    mdd_array_free( aPath->cycleArray );
  }

  FREE( aPath );
}

McOptions_t *
McOptionsAlloc(void)
{
  McOptions_t *result = ALLOC(McOptions_t, 1);

  memset(result, 0, sizeof(McOptions_t));

  result->useMore = FALSE;
  result->reduceFsm = FALSE;
  result->printInputs = FALSE;
  result->useFormulaTree = FALSE;
  result->simFormat = FALSE;
  result->ctlFile = NIL(FILE);
  result->guideFile = NIL(FILE);
  result->debugFile = NIL(FILE);
  result->fwdBwd = McFwd_c;
  result->dcLevel = McDcLevelNone_c;
  result->dbgLevel = McDbgLevelMin_c;
  result->schedule = McGSH_EL_c;
  result->lockstep = MC_LOCKSTEP_OFF;
  result->verbosityLevel = McVerbosityNone_c;
  result->timeOutPeriod = 0;
  result->ardcOptions = NIL(Fsm_ArdcOptions_t);
  result->invarApproxFlag = Fsm_Rch_Default_c;
  result->invarOnionRingsFlag = FALSE;
  result->traversalDirection = McBwd_c;
  result->doCoverageHoskote = FALSE;
  result->doCoverageImproved = FALSE;
  result->incre = TRUE;


  return result;
}

void
McOptionsFree(
  McOptions_t *options)
{
  if (options->debugFile != NIL(FILE)){
    fclose(options->debugFile);
  }
  if (options->ardcOptions != NIL(Fsm_ArdcOptions_t)){
    FREE(options->ardcOptions);
  }
  FREE(options);
}


McDbgLevel
McOptionsReadDbgLevel(
  McOptions_t *options )
{
  return options->dbgLevel;
}

FILE *
McOptionsReadGuideFile(
  McOptions_t *options )
{
  return options->guideFile;
}

FILE *
McOptionsReadSystemFile(
  McOptions_t *options )
{
  return options->systemFile;
}

int
McOptionsReadTimeOutPeriod(
  McOptions_t *options )
{
  return options->timeOutPeriod;
}

Mc_VerbosityLevel
McOptionsReadVerbosityLevel(
  McOptions_t *options )
{
  return options->verbosityLevel;
}

Mc_LeMethod_t
McOptionsReadLeMethod(
  McOptions_t *options )
{
  return options->leMethod;
}

Mc_DcLevel
McOptionsReadDcLevel(
  McOptions_t *options )
{
  return options->dcLevel;
}

FILE *
McOptionsReadCtlFile(
  McOptions_t *options )
{
  return options->ctlFile;
}

FILE *
McOptionsReadDebugFile(
  McOptions_t *options )
{
  return options->debugFile;
}

int
McOptionsReadSimValue(
  McOptions_t *options)
{
  return options->simFormat;
}

int
McOptionsReadUseMore(
  McOptions_t *options)
{
  return options->useMore;
}

boolean
McOptionsReadVacuityDetect(
  McOptions_t *options)
{
  return options->vd ;
}

int
McOptionsReadBeerMethod(
  McOptions_t *options)
{
  return options->beer ;
}


int
McOptionsReadReduceFsm(
  McOptions_t *options)
{
  return options->reduceFsm;
}

int
McOptionsReadPrintInputs(
  McOptions_t *options)
{
  return options->printInputs;
}

boolean
McOptionsReadUseFormulaTree(
  McOptions_t *options)
{
  return options->useFormulaTree;
}

Mc_GSHScheduleType
McOptionsReadSchedule(
  McOptions_t *options)
{
  return options->schedule;
}

int
McOptionsReadLockstep(
  McOptions_t *options)
{
  return options->lockstep;
}

Fsm_RchType_t
McOptionsReadInvarApproxFlag(
  McOptions_t *options)
{
  return (options->invarApproxFlag);
}

boolean
McOptionsReadInvarOnionRingsFlag(
  McOptions_t *options)
{
  return (options->invarOnionRingsFlag);
}

Mc_FwdBwdAnalysis
McOptionsReadFwdBwd(
  McOptions_t *options)
{
  return options->fwdBwd;
}

Mc_FwdBwdAnalysis
McOptionsReadTraversalDirection(
  McOptions_t *options)
{
  return options->traversalDirection;
}

Fsm_ArdcOptions_t *
McOptionsReadArdcOptions(
  McOptions_t *options)
{
  return options->ardcOptions;
}


int
McOptionsReadCoverageHoskote(
  McOptions_t *options)
{
  return options->doCoverageHoskote;
}

int
McOptionsReadCoverageImproved(
  McOptions_t *options)
{
  return options->doCoverageImproved;
}

void
McOptionsSetFwdBwd(
  McOptions_t *options,
  Mc_FwdBwdAnalysis fwdBwd )
{
  options->fwdBwd = fwdBwd;
}

void
McOptionsSetGuideFile(
  McOptions_t *options,
  FILE  *guideFile )
{
  options->guideFile = guideFile;
}

void
McOptionsSetVariablesForSystem(
  McOptions_t *options,
  FILE  *systemFile )
{
  options->systemFile = systemFile;
}
void
McOptionsSetTraversalDirection(
  McOptions_t *options,
  Mc_FwdBwdAnalysis fwdBwd )
{
  options->traversalDirection = fwdBwd;
}

void
McOptionsSetUseMore(
  McOptions_t *options,
  boolean useMore )
{
  options->useMore = useMore;
}

void
McOptionsSetReduceFsm(
  McOptions_t *options,
  boolean reduceFsm )
{
  options->reduceFsm = reduceFsm;
}

void
McOptionsSetVacuityDetect(
  McOptions_t *options,
  boolean vd )
{
  options->vd = vd;
}

void
McOptionsSetBeerMethod(
  McOptions_t *options,
  boolean beer )
{
  options->beer = beer;
}

void
McOptionsSetFAFWFlag(
  McOptions_t *options,
  boolean FAFWFlag )
{
  options->FAFWFlag = FAFWFlag;
}
void
McOptionsSetPrintInputs(
  McOptions_t *options,
  boolean printInputs )
{
  options->printInputs = printInputs;
}

void
McOptionsSetUseFormulaTree(
  McOptions_t *options,
  boolean useFormulaTree )
{
  options->useFormulaTree = useFormulaTree;
}

void
McOptionsSetSchedule(
  McOptions_t *options,
  Mc_GSHScheduleType schedule )
{
  options->schedule = schedule;
}

void
McOptionsSetLockstep(
  McOptions_t *options,
  int lockstep )
{
  options->lockstep = lockstep;
}

void
McOptionsSetSimValue(
  McOptions_t *options,
  boolean simValue )
{
  options->simFormat = simValue;
}

void
McOptionsSetDbgLevel(
  McOptions_t *options,
  McDbgLevel dbgLevel )
{
  options->dbgLevel = dbgLevel;
}

void
McOptionsSetVerbosityLevel(
  McOptions_t *options,
  Mc_VerbosityLevel verbosityLevel )
{
  options->verbosityLevel = verbosityLevel;
}

void
McOptionsSetLeMethod(
  McOptions_t *options,
  Mc_LeMethod_t leMethod)
{
  options->leMethod = leMethod;
}

void
McOptionsSetDcLevel(
  McOptions_t *options,
  Mc_DcLevel dcLevel)
{
  options->dcLevel = dcLevel;
}

void
McOptionsSetArdcOptions(
  McOptions_t *options,
  Fsm_ArdcOptions_t *ardcOptions)
{
  options->ardcOptions = ardcOptions;
}

void
McOptionsSetInvarOnionRingsFlag(
  McOptions_t *options, int shellFlag)
{
  if (shellFlag) options->invarOnionRingsFlag = TRUE;
  else options->invarOnionRingsFlag = FALSE;
}


void
McOptionsSetCtlFile(
  McOptions_t *options,
  FILE *file)
{
  options->ctlFile = file;
}

void
McOptionsSetDebugFile(
  McOptions_t *options,
  FILE *file)
{
  options->debugFile = file;
}

void
McOptionsSetTimeOutPeriod(
  McOptions_t *options,
  int timeOutPeriod)
{
  options->timeOutPeriod = timeOutPeriod;
}

void
McOptionsSetInvarApproxFlag(
  McOptions_t *options,
  Fsm_RchType_t approxFlag)
{
  options->invarApproxFlag = approxFlag;
}



void
McOptionsSetCoverageHoskote(
  McOptions_t *options,
  boolean doCoverageHoskote )
{
  options->doCoverageHoskote = doCoverageHoskote;
}

void
McOptionsSetCoverageImproved(
  McOptions_t *options,
  boolean doCoverageImproved )
{
  options->doCoverageImproved = doCoverageImproved;
}


boolean
McQueryContinue(char *query)
{
  char result[2];

  fprintf(vis_stdout, "%s", query);
  if (fgets(result, 2, stdin) == NULL) return FALSE;

  if(!strcmp(result,"1"))
    return TRUE;
  else if(!strcmp(result,"0"))
    return FALSE;
  else {
    fprintf(vis_stdout, "-- Must enter 0/1\n");
    return McQueryContinue(query);
  }
}


void
McPrintSupport(
  mdd_t *aMdd,
  mdd_manager *mddMgr,
  Ntk_Network_t *aNetwork )
{
  int i;
  char *tmp1String, *tmp2String;
  char *mintermString = NIL(char);
  char bodyString[McMaxStringLength_c];
  array_t *aSupport = mdd_get_support( mddMgr, aMdd );
  array_t *stringArray = array_alloc( char *, 0 );

  for ( i = 0 ; i < array_n( aSupport ); i++ ) {

    int mddId = array_fetch( int, aSupport, i );
    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( aNetwork, mddId );
    char *nodeName = Ntk_NodeReadName( node );
    sprintf( bodyString, "%s", nodeName );
    tmp1String = util_strsav( bodyString );
    array_insert_last( char *, stringArray, tmp1String );
  }

  array_sort( stringArray, cmp);

  for ( i = 0 ; i < array_n( stringArray ); i++ ) {
    tmp1String = array_fetch( char *, stringArray, i );
    if( i == 0 )  {
      mintermString = util_strcat3(tmp1String, "", "" );
    }
    else {
      tmp2String = util_strcat3(mintermString, "\n", tmp1String );
      FREE(mintermString);
      mintermString = tmp2String;
    }
    FREE(tmp1String);
  }
  fprintf(vis_stdout, "%s\n", mintermString );
}



int
McPrintSimPath(
  FILE *outputFile,
  array_t *aPath,
  Fsm_Fsm_t *modelFsm)
{
  int i;

  array_t *inputVars = Fsm_FsmReadInputVars( modelFsm );
  array_t *psVars = Fsm_FsmReadPresentStateVars( modelFsm );

  Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm );
  mdd_manager *mddMgr =  Fsm_FsmReadMddManager( modelFsm );

  array_t *inputSortedVars = SortMddIds( inputVars, network );
  array_t *psSortedVars = SortMddIds( psVars, network );

  fprintf(outputFile, "# UC Berkeley, VIS Release 1.3\n");
  fprintf(outputFile, "# Network: %s\n", Ntk_NetworkReadName( network ) );
  fprintf(outputFile, "# Simulation vectors have been generated to show language non-empty\n\n");

  fprintf( outputFile, ".inputs " );
  PrintNodes( inputSortedVars, network );
  fprintf( outputFile, "\n" );

  fprintf( outputFile, ".latches " );
  PrintNodes( psSortedVars, network );
  fprintf( outputFile, "\n" );

  fprintf( outputFile, ".outputs\n" );

  for( i = -1 ; i < (array_n( aPath ) - 1); i++ ) {

    if ( i == -1 ) {
      mdd_t *initState = array_fetch( mdd_t *, aPath, (i+1) );
      array_t *initValues = McConvertMintermToValueArray( initState, psSortedVars, mddMgr );

      fprintf( outputFile, ".initial ");
      PrintDeck( initValues, psSortedVars, network );
      array_free( initValues );

      fprintf( outputFile, "\n" );
      fprintf( outputFile, ".start_vectors\n");
    }
    else {
      array_t *psValues;
      array_t *nsValues;
      array_t *inputValues;

      mdd_t *psState = array_fetch( mdd_t *, aPath, i );
      mdd_t *nsState = array_fetch( mdd_t *, aPath, (i+1) );
      mdd_t *inputSet = Mc_FsmComputeDrivingInputMinterms( modelFsm, psState, nsState );
      mdd_t *input = Mc_ComputeAMinterm( inputSet, inputVars, mddMgr );

      inputValues = McConvertMintermToValueArray( input, inputSortedVars, mddMgr );
      PrintDeck( inputValues, inputSortedVars, network );
      array_free( inputValues );
      fprintf( outputFile, " ;");

      psValues = McConvertMintermToValueArray( psState, psSortedVars, mddMgr );
      PrintDeck( psValues, psSortedVars, network );
      array_free( psValues );
      fprintf( outputFile, " ;");

      nsValues = McConvertMintermToValueArray( nsState, psSortedVars, mddMgr );
      PrintDeck( nsValues, psSortedVars, network );
      array_free( nsValues );
      fprintf( outputFile, " ;\n");

      mdd_free( inputSet );
      mdd_free( input );
    }
  }
  array_free( psSortedVars );
  array_free( inputSortedVars );

  return 1;
}


Fsm_Fsm_t *
McConstructReducedFsm(
  Ntk_Network_t *network,
  array_t *ctlFormulaArray )
{
  int i;
  Ntk_Node_t *node;
  array_t *nodeArray;
  st_table *formulaNodes;
  Ctlp_Formula_t *fairnessCondition;
  Ctlp_Formula_t *ctlFormula;
  array_t *formulaCombNodes;
  Fsm_Fsm_t *netFsm =  Fsm_NetworkReadFsm( network );
  Fsm_Fsm_t *reducedFsm;
  Fsm_Fairness_t *netFairness = Fsm_FsmReadFairnessConstraint( netFsm );
  array_t *reducedFsmFairness = array_alloc( Ctlp_Formula_t *, 0 );

  if (netFairness) {
    if ( !Fsm_FairnessTestIsBuchi( netFairness ) ) {
      (void) fprintf(vis_stderr, "** mc error: non Buchi fairness constraints not supported\n");
      (void) fprintf(vis_stderr, "** mc error: ignoring fairness constraints\n");
    }
    else {
      int j;
      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct( netFairness, 0 );
      for( j = 0 ; j < numBuchi; j++ ) {
        Ctlp_Formula_t *tmpFormula = Fsm_FairnessReadFinallyInfFormula( netFairness, 0, j );
        Ctlp_Formula_t *reducedFsmCondition = Ctlp_FormulaDup( tmpFormula );
        array_insert_last( Ctlp_Formula_t *, reducedFsmFairness, reducedFsmCondition );
      }
    }
  }

  formulaNodes = st_init_table( st_ptrcmp, st_ptrhash );
  arrayForEachItem( Ctlp_Formula_t *, ctlFormulaArray, i, ctlFormula ) {
    NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
  }

  arrayForEachItem( Ctlp_Formula_t *, reducedFsmFairness, i, fairnessCondition ) {
    NodeTableAddCtlFormulaNodes( network, fairnessCondition, formulaNodes );
  }

  {
    st_generator *stGen;
    nodeArray = array_alloc( Ntk_Node_t *, 0 );
    st_foreach_item( formulaNodes, stGen, &node, NIL(char *) ) {
      array_insert_last( Ntk_Node_t *, nodeArray, node );
    }
  }
  st_free_table( formulaNodes );

  formulaCombNodes  = Ntk_NodeComputeCombinationalSupport( network, nodeArray, FALSE );
  array_free( nodeArray );
  if(array_n(formulaCombNodes) == 0) {

    /* Free the fairness constraint array (if any) */
    for (i=0; i<array_n(reducedFsmFairness); i++){
      Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t*,
                                            reducedFsmFairness, i);
      Ctlp_FormulaFree(formula);
    }
    array_free(reducedFsmFairness);
    /* Free the formulaCombNodes */
    array_free(formulaCombNodes);
    /* We should return a NIL fsm */
    return NIL(Fsm_Fsm_t);
  }
  {
    graph_t *dupPart;
    graph_t *origPart = Part_NetworkReadPartition( network );
    array_t *reducedFsmLatches = array_alloc( Ntk_Node_t *, 0 );
    array_t *reducedFsmInputs = array_alloc( Ntk_Node_t *, 0 );
    int i;
    arrayForEachItem( Ntk_Node_t *, formulaCombNodes, i, node ) {
      if ( Ntk_NodeTestIsInput( node ) == TRUE ) {
        array_insert_last( Ntk_Node_t *, reducedFsmInputs, node );
      }
      else {
        assert( Ntk_NodeTestIsLatch( node ) == TRUE );
        array_insert_last( Ntk_Node_t *, reducedFsmLatches, node );
      }
    }
    if ((array_n(reducedFsmInputs) ==
         Ntk_NetworkReadNumInputs(network)) &&
        (array_n(reducedFsmLatches) ==
         Ntk_NetworkReadNumLatches(network))){
      /* We did not observe any reduction. Return a NIL fsm. */
      /* After freeing appropriate stuff */

      /* Free the fairness constraint array (if any) */
      for (i=0; i<array_n(reducedFsmFairness); i++){
        Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t*,
                                              reducedFsmFairness, i);
        Ctlp_FormulaFree(formula);
      }
      array_free(reducedFsmFairness);
      array_free(formulaCombNodes);
      array_free(reducedFsmLatches);
      array_free(reducedFsmInputs);
      return NIL(Fsm_Fsm_t);
    }
    dupPart = Part_PartitionDuplicate( origPart );
    array_free( formulaCombNodes );
    reducedFsm = Fsm_FsmCreateReducedFsm( network, dupPart, reducedFsmLatches,
                                          reducedFsmInputs, reducedFsmFairness );
    array_free( reducedFsmLatches );
    array_free( reducedFsmInputs );
    array_free( reducedFsmFairness );
  }

  return reducedFsm;

}

Mc_EarlyTermination_t *
McObtainUpdatedEarlyTerminationCondition(
  Mc_EarlyTermination_t *earlyTermination,
  mdd_t *careStates,
  Ctlp_FormulaType formulaType)
{
  Mc_EarlyTermination_t *result;

  switch (formulaType) {
  case Ctlp_NOT_c:
    if (earlyTermination == MC_NO_EARLY_TERMINATION)
      return MC_NO_EARLY_TERMINATION;
    result = Mc_EarlyTerminationAlloc(earlyTermination->mode,
                                      earlyTermination->states);
    switch (result->mode) {
    case McAll_c:
      result->mode = McSome_c;
      break;
    case McSome_c:
      result->mode = McAll_c;
      break;
    case McCare_c:
      break;
    default:
      assert(0);
    }
    break;
  case Ctlp_AND_c:
    if (careStates == NIL(mdd_t)) {
      if (earlyTermination == MC_NO_EARLY_TERMINATION) {
        result = MC_NO_EARLY_TERMINATION;
      } else if (earlyTermination->mode == McAll_c) {
        result = Mc_EarlyTerminationAlloc(McAll_c, earlyTermination->states);
      } else {
        /* Here mode is CARE or SOME: inherit care states from parent. */
        result = Mc_EarlyTerminationAlloc(McCare_c, earlyTermination->states);
      }
    } else {
      /* There are care states from sibling. */
      if (earlyTermination == MC_NO_EARLY_TERMINATION) {
        /* No early termination from parent: just use sibling's care states. */
        result = Mc_EarlyTerminationAlloc(McCare_c, careStates);
      } else if (earlyTermination->mode == McAll_c) {
        /* If some goal states are not in care set, we know we cannot achieve
         * the goal; otherwise, we just propagate the parent's condition.
         */
        if (mdd_lequal(earlyTermination->states, careStates, 1, 1)) {
          result = Mc_EarlyTerminationAlloc(McAll_c, earlyTermination->states);
        } else {
          result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* failure */
        }
      } else if (earlyTermination->mode == McSome_c) {
        /* If no goal states are in the care set, we have failed; otherwise
         * we refine the goal set to those states also in the care set.
         */
        if (mdd_lequal(earlyTermination->states, careStates, 1, 0)) {
          result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* failure */
        } else {
          mdd_t *andMdd = mdd_and(earlyTermination->states, careStates, 1, 1);
          result = Mc_EarlyTerminationAlloc(McSome_c, andMdd);
          mdd_free(andMdd);
        }
      } else { /* if (earlyTermination->mode == McCare_c) */
        /* Intersect care states from parent and sibling. */
        mdd_t *andMdd = mdd_and(earlyTermination->states, careStates, 1, 1);
        result = Mc_EarlyTerminationAlloc(McCare_c, andMdd);
        mdd_free(andMdd);
      }
    }
    break;
  case Ctlp_THEN_c:
  case Ctlp_OR_c:
    if (careStates == NIL(mdd_t)) {
      if (earlyTermination == MC_NO_EARLY_TERMINATION) {
        result = MC_NO_EARLY_TERMINATION;
      } else if (earlyTermination->mode == McSome_c) {
        if (formulaType == Ctlp_OR_c) {
          result = Mc_EarlyTerminationAlloc(McSome_c,
                                            earlyTermination->states);
        } else {
          result = Mc_EarlyTerminationAlloc(McAll_c,
                                            earlyTermination->states);
        }
      } else {
        /* Here mode is CARE or ALL: inherit care states from parent. */
        result = Mc_EarlyTerminationAlloc(McCare_c, earlyTermination->states);
      }
    } else {
      /* There are care states from sibling.
       * Since f->g is !f+g, we treat the THEN and OR cases together by
       * complementing the care set in the latter case. */
      mdd_t *mask = (formulaType == Ctlp_OR_c) ?
        bdd_not(careStates) : bdd_dup(careStates);
      if (earlyTermination == MC_NO_EARLY_TERMINATION) {
        /* No early termination from parent: just use sibling's care states. */
        result = Mc_EarlyTerminationAlloc(McCare_c, mask);
      } else if (earlyTermination->mode == McAll_c) {
        /* Remove the goal states already attained from the goal set. */
        mdd_t *andMdd = mdd_and(earlyTermination->states, mask, 1, 1);
        result = Mc_EarlyTerminationAlloc(McAll_c, andMdd);
        mdd_free(andMdd);
      } else if (earlyTermination->mode == McSome_c) {
        /* If some goal states were already attained, declare success;
         * otherwise just propagate the parent's condition.
         */
        if (mdd_lequal(earlyTermination->states, mask, 1, 1)) {
          result = Mc_EarlyTerminationAlloc(McSome_c,
                                            earlyTermination->states);
        } else {
          result = Mc_EarlyTerminationAlloc(McCare_c, NIL(mdd_t)); /* success */
        }
      } else { /* if (earlyTermination->mode == McCare_c) */
        /* Intersect care states from parent and sibling. */
        mdd_t *andMdd = mdd_and(earlyTermination->states, mask, 1, 1);
        result = Mc_EarlyTerminationAlloc(McCare_c, andMdd);
        mdd_free(andMdd);
      }
      mdd_free(mask);
    }
    break;
  default:
    result = MC_NO_EARLY_TERMINATION;
  }
  return result;

} /* McObtainUpdatedEarlyTerminationCondition */


boolean
McCheckEarlyTerminationForUnderapprox(
  Mc_EarlyTermination_t *earlyTermination,
  mdd_t *underApprox,
  array_t *careStatesArray)
{
  if(earlyTermination == MC_NO_EARLY_TERMINATION)
    return FALSE;

  /* for an underapproximation and McAll_c (McSome_c), you just check
     whether all states (some states) are already reached */
  return(((earlyTermination->mode != McSome_c) &&
          (mdd_lequal_mod_care_set_array(earlyTermination->states, underApprox,
                                         1, 1, careStatesArray)))
         ||
         (
           (earlyTermination->mode == McSome_c) &&
           (!mdd_lequal_mod_care_set_array(underApprox,
                                           earlyTermination->states, 1,
                                           0, careStatesArray))));
}


boolean
McCheckEarlyTerminationForOverapprox(
  Mc_EarlyTermination_t *earlyTermination,
  mdd_t *overApprox,
  array_t *careStatesArray)
{
  if(earlyTermination == MC_NO_EARLY_TERMINATION)
    return FALSE;

  /* For an overapproximation and McAll_c (McSome_c), you check
     whether some state (all states) are already missing */
  return(((earlyTermination->mode == McAll_c) &&
          (!mdd_lequal_mod_care_set_array(earlyTermination->states,
                                          overApprox, 1, 1, careStatesArray)))
         ||
         ((earlyTermination->mode != McAll_c) &&
          (mdd_lequal_mod_care_set_array(earlyTermination->states,
                                          overApprox, 1, 0,
                                          careStatesArray))));
}


array_t *
Mc_ReadHints(
  FILE *guideFP
  )
{
  Ctlp_FormulaArray_t *invarArray;   /* formulae representing hints */
  int i;                      /* to iterate over formulae        */
  Ctlp_Formula_t *formula;    /* idem                            */

  if (guideFP == NIL(FILE)){
    fprintf(vis_stderr,
            "** mc error: can't read hint file.\n");
    return NIL(array_t);
  }

  invarArray = Ctlp_FileParseFormulaArray( guideFP );

  if (invarArray == NIL(array_t)){
    fprintf(vis_stderr,
            "** mc error: parse error in hints file.\n");
    return NIL(array_t);
  }

  if (array_n(invarArray) == 0){
    fprintf(vis_stdout, "** mc error: File contained no hints.\n");
    Ctlp_FormulaArrayFree(invarArray);
    return NIL(array_t);
  }


  array_insert_last(Ctlp_Formula_t *, invarArray,
                    Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(void), NIL(void)));

  /* some checks */
  arrayForEachItem(Ctlp_Formula_t *, invarArray, i, formula){
    if(!Ctlp_FormulaTestIsQuantifierFree(formula)){
      (void) fprintf(vis_stdout,
                     "** mc error: Hints contain temporal operators\n");

      Ctlp_FormulaArrayFree(invarArray);
      return NIL(array_t);
    } /* quantifier free */

  }/* checks */


  return invarArray;
}/* Mc_ReadHints */

st_table *
Mc_ReadSystemVariablesFAFW(
  Fsm_Fsm_t *fsm,
  FILE *systemFP
  )
{
  st_table *variablesTable;
  array_t *bddIdArray;
  char line[1024], nodeName[1024], *next;
  int mddId, bddId;
  int i, j, len, index;
  int errorFlag;
  Ntk_Node_t *node;
  Ntk_Network_t *network;
  mdd_manager *mgr;

  errorFlag = 0;
  if (systemFP == NIL(FILE)){
    fprintf(vis_stderr,
            "** mc error: can't read system file.\n");
    return NIL(st_table);
  }

  network = Fsm_FsmReadNetwork(fsm);
  mgr = Fsm_FsmReadMddManager(fsm);
  variablesTable = st_init_table(st_numcmp, st_numhash);
  while(fgets(line, 1024, systemFP)) {
    len = strlen(line);
    for(i=0; i<len; i++) {
      if(line[i] == ' ')        continue;
      if(line[i] == '\t')       continue;
      break;
    }
    next = &(line[i]);
    if(next[0] == '\n') continue;
    if(next[0] == '#')  continue;
    len = strlen(next);
    index = 0;
    nodeName[0] = '\0';
    for(i=0; i<len; i++) {
      if(next[i] == ' ') break;
      if(next[i] == '\t') break;
      if(next[i] == '\n') break;
      nodeName[index] = next[i];
      index++;
    }
    nodeName[index] = '\0';
    node = Ntk_NetworkFindNodeByName(network, nodeName);
    if(node == NIL(Ntk_Node_t)) {
      fprintf(vis_stderr, "Error : Can't find node '%s'\n", nodeName);
      errorFlag = 1;
      continue;
    }
    mddId = Ntk_NodeReadMddId(node);
    bddIdArray = mdd_id_to_bdd_id_array(mgr, mddId);
    for(j=0; j<array_n(bddIdArray); j++) {
      bddId = array_fetch(int, bddIdArray, j);
      st_insert(variablesTable, (char *)(long)bddId, (char *)(long)bddId);
    }
    array_free(bddIdArray);
  }

  if(variablesTable->num_entries == 0)  {
    st_free_table(variablesTable);
    variablesTable = 0;
  }
  if(errorFlag) {
    if(variablesTable)
      st_free_table(variablesTable);
    variablesTable = 0;
    return((st_table *)-1);
  }
  return variablesTable;
}/* Mc_ReadSystemVariablesFAFW */


st_table *
Mc_SetAllInputToSystem(Fsm_Fsm_t *fsm)
{
  mdd_manager *mgr;
  array_t *inputVars, *bddIdArray;
  int i, j;
  int mddId, bddId;
  st_table *idTable;

  idTable = st_init_table(st_numcmp, st_numhash);
  mgr = Fsm_FsmReadMddManager(fsm);
  /* inputVars = Fsm_FsmReadPrimaryInputVars(fsm); */
  inputVars = Fsm_FsmReadInputVars(fsm);

  if(inputVars) {
    for(i=0; i<array_n(inputVars); i++) {
      mddId = array_fetch(int, inputVars, i);
      bddIdArray = mdd_id_to_bdd_id_array(mgr, mddId);
      for(j=0; j<array_n(bddIdArray); j++) {
        bddId = array_fetch(int, bddIdArray, j);
        st_insert(idTable, (char *)(long)bddId, (char *)(long)bddId);
      }
    }
  }
  return(idTable);

}

array_t *
Mc_EvaluateHints(
  Fsm_Fsm_t *fsm,
  Ctlp_FormulaArray_t *invarArray
  )
{
  array_t *invarStatesArray = NIL(array_t);/* array of sets of states: hints*/
  int i, j;                                       /* to iterate over formulae  */
  Ctlp_Formula_t *formula= NIL(Ctlp_Formula_t);/* idem                      */
  mdd_t *invarFormulaStates = NIL(mdd_t);/* states in which formula is true */
  mdd_t *one = NIL(mdd_t);
  array_t *psVars = Fsm_FsmReadPresentStateVars(fsm);
  array_t *inputVars = Fsm_FsmReadInputVars(fsm);
  array_t *psInputVars = array_join(psVars, inputVars);
  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);

  invarStatesArray = array_alloc(mdd_t *, 0);

  one = mdd_one(Fsm_FsmReadMddManager(fsm));

  arrayForEachItem(Ctlp_Formula_t *, invarArray, i, formula){
    /* semantic checks */
    if(!Mc_FormulaStaticSemanticCheckOnNetwork(formula,
                                               Fsm_FsmReadNetwork(fsm),
                                               TRUE)){
      (void) fprintf(vis_stdout,
                     "** mc error: Error evaluating hint:\n%s\n",
                     error_string());

      mdd_free(one);
      mdd_array_free(invarStatesArray);
      return NIL(array_t);
    }/* if semantic error */

    assert(Ctlp_FormulaTestIsQuantifierFree(formula));

    Ctlp_FlushStates(formula);


    /* compute the set of states represented by the invariant. */
    invarFormulaStates =
      Mc_FsmEvaluateFormula(fsm, formula, one,
                            NIL(Fsm_Fairness_t), NIL(array_t),
                            MC_NO_EARLY_TERMINATION,
                            NIL(Fsm_HintsArray_t), Mc_None_c,
                            McVerbosityNone_c, McDcLevelNone_c, 0,
                            McGSH_EL_c);


    if (!mdd_check_support(mddMgr, invarFormulaStates, psInputVars)) {
      mdd_t *temp;
      int mddId;
      array_t *supportArray = mdd_get_support(mddMgr, invarFormulaStates);
      array_t *leftOverVars = array_alloc(int, 0);
      /* store the PS and the Input Vars of this FSM */
      st_table *supportTable = st_init_table(st_numcmp, st_numhash);

      arrayForEachItem(int, psInputVars, j, mddId) {
        (void) st_insert(supportTable, (char *) (long) mddId, NIL(char));
      }

      /* isolate the vars outside this FSM */
      arrayForEachItem(int, supportArray, j, mddId) {
        if (st_is_member(supportTable, (char *)(long)mddId) == 0) {
          array_insert_last(int, leftOverVars, mddId);
        }
      }

      /* Quantify them out */
      if (array_n(leftOverVars) > 0) {
        fprintf(vis_stdout, "GS warning ** Quantifying out variables not relevant to the reduced FSM in hint %d. \n", i+1);
        arrayForEachItem(int, leftOverVars, j, mddId) {
          fprintf(vis_stdout, "%s\n", (mdd_get_var_by_id(mddMgr, mddId)).name);
        }
        temp = mdd_smooth(mddMgr,  invarFormulaStates, leftOverVars);
        mdd_free(invarFormulaStates);
        invarFormulaStates = temp;
      }
      array_free(leftOverVars);
      st_free_table(supportTable);
      array_free(supportArray);
    }

    array_insert_last(mdd_t *, invarStatesArray, invarFormulaStates);
  }/* for each formula */

  array_free(psInputVars);
  mdd_free(one);
  return invarStatesArray;
}/* Mc_EvaluateHints */

array_t *
Mc_ComputeGuideArray(
  Fsm_Fsm_t *fsm,
  FILE *guideFP
  )
{
  Ctlp_FormulaArray_t *hintFormulae;
  array_t             * hintSets;

  hintFormulae = Mc_ReadHints(guideFP);
  fclose(guideFP);

  if( hintFormulae == NIL(Ctlp_FormulaArray_t))
    return NIL(array_t);

  hintSets = Mc_EvaluateHints(fsm, hintFormulae);

  Ctlp_FormulaArrayFree(hintFormulae);

  return hintSets;
}/* Mc_ComputeGuideArray */


Mc_GuidedSearch_t Mc_ReadGuidedSearchType(void)
{
  char *string =  Cmd_FlagReadByName("guided_search_hint_type");

  if(string == NIL(char))  /* default */
    return Mc_Local_c;
  if(!strcmp(string, "global"))
    return Mc_Global_c;
  if(!strcmp(string, "local"))
    return Mc_Local_c;
  else
    return Mc_None_c;
}


void
Mc_CheckPathToCore(Fsm_Fsm_t *fsm, array_t *pathToCore)
{
  array_t *inputVars;
  int i;
  mdd_t *fromState, *toState, *inputSet;
  mdd_manager   *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm));

  inputVars = Fsm_FsmReadInputVars( fsm );
  for(i=-1; i<array_n(pathToCore)-1; i++) {
    fromState = (i==-1) ? 0 : array_fetch(mdd_t *, pathToCore, i);
    toState = array_fetch(mdd_t *, pathToCore, i+1);
    if((long)fromState % 2)     fromState = (mdd_t *)((long)fromState - 1);
    if((long)toState % 2)       toState = (mdd_t *)((long)toState - 1);
    inputSet = ( i == -1) ? 0 :
                 Mc_FsmComputeDrivingInputMinterms( fsm, fromState, toState );

    if(inputSet)
      Mc_ComputeAMinterm( inputSet, inputVars, mgr );
    else if(i != -1)
      fprintf(vis_stderr, "Illegal path from %d to %d\n", i, i+1);
  }

}

void
Mc_CheckPathFromCore(Fsm_Fsm_t *fsm, array_t *pathFromCore)
{
  array_t *inputVars;
  int i;
  mdd_t *fromState, *toState, *inputSet;
  mdd_manager   *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm));

  inputVars = Fsm_FsmReadInputVars( fsm );
  for(i=array_n(pathFromCore); i>0; i--) {
    fromState = (i==array_n(pathFromCore)) ? 0 : array_fetch(mdd_t *, pathFromCore, i);
    toState = array_fetch(mdd_t *, pathFromCore, i-1);
    if((long)fromState % 2)     fromState = (mdd_t *)((long)fromState - 1);
    if((long)toState % 2)       toState = (mdd_t *)((long)toState - 1);
    inputSet = ( i == array_n(pathFromCore)) ? 0 :
      Mc_FsmComputeDrivingInputMinterms( fsm, fromState, toState );

    if(inputSet)
      Mc_ComputeAMinterm( inputSet, inputVars, mgr );
    else if(i != array_n(pathFromCore))
      fprintf(vis_stderr, "Illegal path from %d to %d\n", i, i+1);
  }
}

void
Mc_PrintStates(
  Fsm_Fsm_t *modelFsm,
  mdd_t *states)
{
  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
  Ntk_Network_t *aNetwork = Fsm_FsmReadNetwork( modelFsm );
  mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
  mdd_t *zeroMdd, *new_states;
  char  *tmpString;
  double   size;

 /*
  *  sometimes, this function will be constrained by number of minterm
  *     in the given set of states.
  *     num_minterm = mdd_num_of_mintern(states);
  *     if(num_minterm > MAX_MINTERM)   {
  *       fprintf( stdout, "Too many minterms in given states\n" );
  *       return;
  *     }
  */
  if((long)states % 2) {
    states = (mdd_t *)((long)states - 1);
  }
  zeroMdd = mdd_zero( mddMgr );
  states = mdd_dup(states);
  if(mdd_equal(states, zeroMdd)) {
    fprintf(stdout, "ZERO mdd\n");
    mdd_free(zeroMdd);
    return;
  }
  size = mdd_count_onset(mddMgr, states, PSVars);
  if(size > 40.0) {
    fprintf(stdout, "Too many minterms in given states %.0f\n", size);
    return;
  }
  fprintf( stdout, "    " );
  while(1) {
    mdd_t *result = Mc_ComputeAMinterm( states, PSVars, mddMgr );

    new_states = mdd_and( states, result, 1, 0 );
    mdd_free( states );
    states = new_states;

    tmpString = Mc_MintermToString( result, PSVars, aNetwork );
    fprintf( stdout, "%s ", tmpString );
    FREE(tmpString);
    mdd_free( result );

    if(mdd_equal(states, zeroMdd)) {
      mdd_free(zeroMdd);
      mdd_free(states);
      break;
    }
  }
  fprintf(stdout, "\n");
}

void
Mc_PrintNumStates(
  Fsm_Fsm_t *modelFsm,
  mdd_t *states)
{
  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
  mdd_manager *mddMgr = Fsm_FsmReadMddManager( modelFsm );
  mdd_t *zeroMdd;
  double size;

 /*
  *  sometimes, this function will be constrained by number of minterm
  *     in the given set of states.
  *     num_minterm = mdd_num_of_mintern(states);
  *     if(num_minterm > MAX_MINTERM)   {
  *       fprintf( stdout, "Too many minterms in given states\n" );
  *       return;
  *     }
  */
  if((long)states % 2) {
    states = (mdd_t *)((long)states - 1);
  }
  zeroMdd = mdd_zero( mddMgr );
  states = mdd_dup(states);
  if(mdd_equal(states, zeroMdd)) {
    fprintf(stdout, "ZERO mdd\n");
    mdd_free(zeroMdd);
    mdd_free(states);
    return;
  }
  size = mdd_count_onset(mddMgr, states, PSVars);
  fprintf(stdout, "num states : %.0f\n", size);
  mdd_free(zeroMdd);
  mdd_free(states);
}

void
Mc_PrintRings(
  Fsm_Fsm_t *modelFsm,
  array_t *onionRings)
{
  int j;
  mdd_t *innerRing;

  if(array_n(onionRings) > 0) {
    for(j=0; j<array_n(onionRings); j++) {
      innerRing = array_fetch(mdd_t *, onionRings, j);
      fprintf(vis_stdout, "%d'th ring : ", j);
      if(innerRing)
        Mc_PrintStates(modelFsm, innerRing);
      else
        fprintf(vis_stdout, "\n");
    }
  }
}

void
Mc_PrintNumRings(
  Fsm_Fsm_t *modelFsm,
  array_t *onionRings)
{
  int j;
  mdd_t *innerRing;

  if(array_n(onionRings) > 0) {
    for(j=0; j<array_n(onionRings); j++) {
      innerRing = array_fetch(mdd_t *, onionRings, j);
      fprintf(vis_stdout, "%d'th ring : ", j);
      if(innerRing)
        Mc_PrintNumStates(modelFsm, innerRing);
      else
        fprintf(vis_stdout, "\n");
    }
  }
}


mdd_t *
McComputeACloseMinterm(
  mdd_t *aSet,
  mdd_t *target,
  array_t *Support,
  mdd_manager *mddMgr)
{
  if (bdd_get_package_name() == CUDD) {
    mdd_t *range;             /* range of Support             */
    mdd_t *legalSet;          /* aSet without the don't cares */
    mdd_t *closeCube;
    int dist;
    array_t *bddSupport;      /* Support in terms of bdd vars */
    mdd_t *minterm;           /* a random minterm             */

    /* Check that support of set is contained in Support. */
    assert(SetCheckSupport(aSet, Support, mddMgr));
    assert(!mdd_is_tautology(aSet, 0));
    range      = mdd_range_mdd(mddMgr, Support);
    legalSet   = bdd_and(aSet, range, 1, 1);
    mdd_free(range);
    closeCube = mdd_closest_cube(legalSet, target, &dist);
    bddSupport = mdd_id_array_to_bdd_array(mddMgr, Support);
    minterm    = bdd_pick_one_minterm(closeCube, bddSupport);

    assert(MintermCheckWellFormed(minterm, Support, mddMgr));
    assert(mdd_count_onset(mddMgr, minterm, Support) == 1);
    assert(mdd_lequal(minterm,legalSet,1,1));

    mdd_array_free(bddSupport);
    mdd_free(legalSet);
    mdd_free(closeCube);

    return minterm;
  } else {
    return Mc_ComputeAMinterm(aSet, Support, mddMgr);
  }/* if CUDD */

} /* McComputeACloseMinterm */

mdd_t *
McComputeACloseState(
  mdd_t *states,
  mdd_t *target,
  Fsm_Fsm_t *modelFsm)
{
  array_t *PSVars = Fsm_FsmReadPresentStateVars(modelFsm);
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager(
    Fsm_FsmReadNetwork(modelFsm));
  mdd_t *result;

  if (mdd_is_tautology(target, 0)) {
    result = Mc_ComputeAMinterm(states, PSVars, mddMgr);
  } else {
    result = McComputeACloseMinterm(states, target, PSVars, mddMgr);
  }

  return result;

} /* McComputeACloseState */


Mc_GSHScheduleType
McStringConvertToScheduleType(
  char *string)
{
  if (strcmp("off", string) == 0) {
    return McGSH_old_c;
  } else if (strcmp("EL", string) == 0) {
    return McGSH_EL_c;
  } else if (strcmp("EL1", string) == 0) {
    return McGSH_EL1_c;
  } else if (strcmp("EL2", string) == 0) {
    return McGSH_EL2_c;
  } else if (strcmp("random", string) == 0) {
    return McGSH_Random_c;
  } else if (strcmp("budget", string) == 0) {
    return McGSH_Budget_c;
  } else {
    return McGSH_Unassigned_c;
  }

} /* McStringConvertToScheduleType */


int
McStringConvertToLockstepMode(
  char *string)
{
  int n;

  if (strcmp("off", string) == 0) {
    return MC_LOCKSTEP_OFF;
  } else if (strcmp("on", string) == 0) {
    return MC_LOCKSTEP_EARLY_TERMINATION;
  } else if (strcmp("all", string) == 0) {
    return MC_LOCKSTEP_ALL_SCCS;
  } else if (Cmd_StringCheckIsInteger(string, &n) == 2) {
    return n;
  } else {
    return MC_LOCKSTEP_UNASSIGNED;
  }

} /* McStringConvertToLockstepMode */


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

static void
PrintNodes(
  array_t *mddIdArray,
  Ntk_Network_t *network )
{
  int i;
  int mddId;

  arrayForEachItem(int , mddIdArray, i, mddId) {
    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
    char *nodeName = Ntk_NodeReadName( node );
    fprintf(vis_stdout, " %s ", nodeName );
  }
}


static array_t *
SortMddIds(
  array_t *mddIdArray,
  Ntk_Network_t *network )
{
  int i;
  int mddId;
  char *nodeName;
  st_table *nameToIndex = st_init_table( strcmp, st_strhash );
  array_t *nodeNameArray = array_alloc( char *, 0 );
  array_t *result = array_alloc( int, 0 );

  arrayForEachItem(int, mddIdArray, i, mddId) {
    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
    nodeName = Ntk_NodeReadName( node );
    st_insert( nameToIndex, nodeName, (char *) (long) i );
    array_insert_last(  char *, nodeNameArray, nodeName );
  }
  array_sort( nodeNameArray, cmp);

  arrayForEachItem(char *, nodeNameArray, i, nodeName ) {
    int index;
    st_lookup_int( nameToIndex, nodeName, & index );
    mddId = array_fetch( int, mddIdArray, index );
    array_insert_last( int, result, mddId );
  }
  st_free_table( nameToIndex );
  array_free( nodeNameArray );

  return result;
}

static void
PrintDeck(
  array_t *mddValues,
  array_t *mddIdArray,
  Ntk_Network_t *network )
{
  int i;
  int mddId;

  arrayForEachItem(int, mddIdArray, i, mddId) {
    int value = array_fetch( int, mddValues, i );
    Ntk_Node_t *node = Ntk_NetworkFindNodeByMddId( network, mddId );
    Var_Variable_t *nodeVar = Ntk_NodeReadVariable( node );
    if ( Var_VariableTestIsSymbolic( nodeVar ) ) {
      char *symbolicValue = Var_VariableReadSymbolicValueFromIndex( nodeVar, value );
      fprintf( vis_stdout, "%s ", symbolicValue );
    }
    else {
      fprintf( vis_stdout, "%d ", value );
    }
  }
}

static int
cmp(
  const void * s1,
  const void * s2)
{
  return(strcmp(*(char **)s1, *(char **)s2));
}

static boolean
AtomicFormulaCheckSemantics(
  Ctlp_Formula_t *formula,
  Ntk_Network_t *network,
  boolean inputsAllowed)
{

  char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
  char *nodeValueString = Ctlp_FormulaReadValueName( formula );
  Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );

  Var_Variable_t *nodeVar;
  int nodeValue;

  if ( !node ) {
    error_append("Could not find node corresponding to the name\n\t- ");
    error_append( nodeNameString );
    error_append("\n(Wire for this name may have been removed by synthesis)");
    return FALSE;
  }

  nodeVar = Ntk_NodeReadVariable( node );
  if ( Var_VariableTestIsSymbolic( nodeVar ) ){

    nodeValue = Var_VariableReadIndexFromSymbolicValue( nodeVar, nodeValueString );
    if ( nodeValue == -1 ) {
      error_append("Value specified in RHS is not in domain of variable\n");
      error_append( Ctlp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlp_FormulaReadValueName( formula ) );
      return FALSE;
    }
  }
  else {
    int check;

    check = Cmd_StringCheckIsInteger(nodeValueString, &nodeValue);
    if( check==0 ) {
      error_append("Value in the RHS is illegal\n");
      error_append( Ctlp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlp_FormulaReadValueName( formula ) );
      return FALSE;
    }
    if( check==1 ) {
      error_append("Value in the RHS is out of range of int\n");
      error_append( Ctlp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlp_FormulaReadValueName( formula ) );
      return FALSE;
    }
    if ( !(Var_VariableTestIsValueInRange( nodeVar, nodeValue ) ) ) {
      error_append("Value specified in RHS is not in domain of variable\n");
      error_append( Ctlp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlp_FormulaReadValueName( formula ) );
      return FALSE;
    }
  }

  if(!inputsAllowed){
    boolean coverSupport;
    lsGen tmpGen;
    Ntk_Node_t *tmpNode;
    st_table *supportNodes    = st_init_table(st_ptrcmp, st_ptrhash);
    array_t *thisNodeArray = array_alloc( Ntk_Node_t *, 0);

    array_insert_last( Ntk_Node_t *, thisNodeArray, node );
    Ntk_NetworkForEachNode(network, tmpGen, tmpNode) {
      if (Ntk_NodeTestIsConstant(tmpNode) || Ntk_NodeTestIsLatch(tmpNode)) {
        st_insert(supportNodes, (char *) tmpNode, NIL(char));
      }
    }

    coverSupport = Ntk_NetworkTestLeavesCoverSupportOfRoots(network,
                                                            thisNodeArray,
                                                            supportNodes);
    array_free(thisNodeArray);
    st_free_table(supportNodes);

    if ( coverSupport == FALSE ) {
      char *tmpString =
        util_strcat3( "\nNode ", nodeNameString,
                      " is not driven only by latches and constants.\n");
      error_append(tmpString);
      return FALSE;
    }
  }

  return TRUE;
}

static void
NodeTableAddCtlFormulaNodes(
  Ntk_Network_t *network,
  Ctlp_Formula_t *formula,
  st_table * nodesTable )
{
  if ( formula == NIL(Ctlp_Formula_t) ) {
        return;
  }

  if ( Ctlp_FormulaReadType( formula ) == Ctlp_ID_c ) {
    char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
    Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
    if( node )
      st_insert( nodesTable, ( char *) node, NIL(char) );
    return;
  }

  NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadRightChild( formula ), nodesTable );
  NodeTableAddCtlFormulaNodes( network, Ctlp_FormulaReadLeftChild( formula ), nodesTable );

  return;
}

static void
NodeTableAddLtlFormulaNodes(
  Ntk_Network_t *network,
  Ctlsp_Formula_t *formula,
  st_table * nodesTable )
{
  if ( formula == NIL(Ctlsp_Formula_t) ) {
        return;
  }

  if ( Ctlsp_FormulaReadType( formula ) == Ctlsp_ID_c ) {
    char *nodeNameString = Ctlsp_FormulaReadVariableName( formula );
    Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
    if( node )
      st_insert( nodesTable, ( char *) node, NIL(char) );
    return;
  }

  NodeTableAddLtlFormulaNodes( network, Ctlsp_FormulaReadRightChild( formula ), nodesTable );
  NodeTableAddLtlFormulaNodes( network, Ctlsp_FormulaReadLeftChild( formula ), nodesTable );

  return;
}

static boolean
MintermCheckWellFormed(
  mdd_t *aMinterm,
  array_t *aSupport,
  mdd_manager *mddMgr)
{

  /* first check its support */
  if (!SetCheckSupport(aMinterm, aSupport, mddMgr)) {
    return FALSE;
  }

  /* now check its a minterm */
  {
    float cardinality = mdd_count_onset( mddMgr, aMinterm, aSupport );
    if ( cardinality != 1 ) {
      fprintf( vis_stderr, "-- onset is not one\n");
      return FALSE;
    }
  }
  return TRUE;
}


static boolean
SetCheckSupport(
  mdd_t *aMinterm,
  array_t *aSupport,
  mdd_manager *mddMgr)
{
  if (!mdd_check_support(mddMgr, aMinterm, aSupport)) {
    fprintf(vis_stderr,
      "** mc error: support of minterm is not contained in claimed support\n");
    return FALSE;
  }
  return TRUE;
}