source: vis_dev/vis-2.3/src/mc/mcUtil.c

/**CFile***********************************************************************

  FileName    [mcUtil.c]

  PackageName [mc]

  Synopsis    [Utilities for Fair CTL model checker and debugger]

  Author      [Adnan Aziz, Tom Shiple, In-Ho Moon]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

******************************************************************************/

#include "mcInt.h"
#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                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

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

/**AutomaticEnd***************************************************************/


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

/**Function********************************************************************

  Synopsis [Return Boolean TRUE/FALSE depending on whether states in
  specialStates can reach states in targetStates.]

  Description [Return Boolean TRUE/FALSE depending on whether states in
  specialStates can reach states in targetStates. If true, onionRings is set
  to results of fixed point computation going back from targetStates to
  specialStates.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return Boolean TRUE/FALSE depending on whether states in
  specialStates are reachable from  initialStates.]

  Description [Return Boolean TRUE/FALSE depending on whether states in
  specialStates are reachable from  initialStates.If true, onionRings is set
  to results of fixed point computation going forward from initialStates to
  specialStates.  Otherwise onionRings is freed.]

  SideEffects []

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

}

/**Function********************************************************************

  Synopsis [Perform static semantic check of ctl formula on network.]

  Description [Perform static semantic check of ctl formula on network.
  Specifically, given an atomic formula of the form LHS=RHS, check that the LHS
  is the name of a latch/wire in the network, and that RHS is of appropriate
  type (enum/integer) and is lies in the range of the latch/wire values. If LHS
  is a wire, and inputsAllowed is false, check to see that the algebraic
  support of the wire consists of only latches and constants.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Build Path to Core starting at aState.]

  Description [Build Path to Core (the first onion ring) starting at aState.

  <p> For the onion rings should be built in such a way that for every state v
  in ring i+1 there is a state v' in ring i such that there is an edge from v
  to v'.  This function will also works for non-BFS rings, where we just
  require that for every state v in a ring i > 0, there is a state in a ring 0
  <= j < i that is a successor of v.

  <p>For paths of length at least one, set PathLengthType to McGreaterZero_c.
  Otherwise, use McGreaterOrEqualZero_c.  The function returns a sequence of
  states to a state in the core of onionRings, starting at aState. It is the
  users responsibility to free the array returned as well as its members.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Build a onion ring from initial state.]

  Description [Build a onion ring from initial state.
               This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Build a onion ring to target under invariants.]

  Description [Build a onion ring to target under invariants.
               This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Build a onion ring from target under invariants.]

  Description [Build a onion ring from target under invariants.
               This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Build Path from Core to aState.]

  Description [Build Path starting at a Core state (a state in the first onion
  ring) to aState.  For paths of length at least one, set PathLengthType to
  McGreaterZero_c; otherwise, use McGreaterOrEqualZero_c.  The function returns
  a sequence of states from the core of onionRings to a aState.

  <p>In the case of BFS search, the onion rings are built forward, so that any
  state in ring i+1 has at least one predecessor in ring i-1.  In non-BFS
  search that may not be true, but we will have that every state in ring i+1
  has a predecessor in ring i or less.  The fsm is checked to see if the search
  was BFS. If not, every ring from the beginning is searched to find the
  shortest path. This is a greedy heuristic and the shortest path is not
  guaranteed to be found.  McBuildPathToCore takes a different approach.

  <p>It is the users responsibility to free the array returned as well as its
  members.]

  SideEffects []

  SeeAlso[Mc_BuildPathToCore]

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

/**Function********************************************************************

  Synopsis [Build a path from initial state to target.]

  Description [Build a path from initial state to target.
               This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Build a path from target to initial state with general algorithm.]

  Description [Build a path from target to initial state with general algorithm.
               This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Build a counterexample path with general algorithm.]

  Description [Build a counterexample path with general algorithm
               This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

******************************************************************************/
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);
  /**
  Img_ImageInfoConjoinWithWinningStrategy(modelFsm, Img_Forward_c, 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);
        /**
        Fsm_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c);
        Fsm_ImageInfoConjoinWithWinningStrategy(modelFsm, Img_Forward_c, Li);
        **/
      }
    }

    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);
      /**
      Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c);
      **/
      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);
  /**
  Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c);
  **/
  return(path);
}

/**Function********************************************************************

  Synopsis [Build a fate and free will layer.]

  Description [Build a fate and free will layer.
               This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Build a path from target to initial state.]

  Description [Build a path from target to initial state.
               This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

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

  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, 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);
/**    T = mdd_dup(T); **/
    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(T);  **/
      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;
  }
}

/**Function********************************************************************

  Synopsis [Build a shortest path from T to S.]

  Description [Make a shortest path from T to S which only passes through
               states in rings. There is always a path from T to S.
               Returns a sequence of states starting from T, leading to S.
               It is the users responsibility to free the returned
               array as well as its members.
               This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

******************************************************************************/
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) /** free segment **/
      array_insert_last(mdd_t *, C, Cn);
    else          /** fated segment **/
      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);
}



/**Function********************************************************************

  Synopsis [Make a path from aState to bState.]

  Description [Make a path from aState to bState which only passes through
  invariantStates; it is assumed that aState and bState lie in invariantStates.
  Returns a sequence of states starting from aState, leading to bState. If
  aState == bState, a non trivial path is returned (ie a cycle). If no
  path exists, return NIL. It is the users responsibility to free the returned
  array as well as its members.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Pick an arbitrary minterm from the given set.]

  Description [Pick an arbitrary minterm from the given set. Support is an
  array of mddids representing the total support; that is, all the variables
  on which aSet may depend.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Pick a minterm from the given set close to target. Support
  is an array of mddids representing the total support; that is, all
  the variables on which aSet may depend.]

  SideEffects []

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




/**Function********************************************************************

  Synopsis [Return a string for a minterm.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Return a string for a minterm.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return a string for a minterm.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Utility function - prints states on path, inputs for transitions]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Utility function - prints states on path, inputs for transitions]

  SideEffects []

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


/**Function********************************************************************

  Synopsis    [Builds MVF for a node that is a pseudo input.]

  Description [Builds MVF for a node that is a pseudo input.  This node has a
  single output and no inputs. Its table has several row entries.  We build an
  MVF whose components correspond exactly to possible table outputs.]

  SideEffects []

  Comment [Although pseudo inputs, constants, and internal nodes all have
  tables, a single procedure cannot be used to build their MVF.  A pseudo
  input MVF is built in terms of its mddId, whereas a constant or internal is
  not.  A constant or pseudo input doesn't have any inputs, whereas an
  internal does.]

  SeeAlso     [Tbl_TableBuildMvfForNonDetConstant]

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

/**Function********************************************************************

  Synopsis [Return the range of pseudo inputs if they are defined by subsets of range.]

  Description [The result can be used to extract correct input conditions.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Return all inputs which cause a transition from aState to bState.]

  Description [Return all inputs which cause a transition from aState to bState.
  It is assumed that aState,bState are truly minterms over the PS variables.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Select an arbitrary  state from the given set]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Select a state from the given set close to target.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Print a minterm.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Add nodes for wires referred to in formula to nodesTable.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Add nodes for wires referred to in formula to nodesTable.]

  Description [Add nodes for wires referred to in formula to nodesTable.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Form an FSM reduced with respect to the specified formula]

  Description [Form an FSM reduced with respect to the CTL formula array.
  All latches and inputs which affect the given formula AND the fairness
  conditions of the system are included in this reduced fsm.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis    [Converts a string to a schedule type.]

  Description [Converts a string to a schedule type.  If string does
  not refer to one of the allowed schedule types, then returns
  McGSH_Unassigned_c.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis    [Converts a string to a lockstep mode.]

  Description [Converts a string to a lockstep mode.  If string does
  not refer to one of the allowed lockstep modes, it returns
  MC_LOCKSTEP_UNASSIGNED.  The allowed values are: MC_LOCKSTEP_OFF,
  MC_LOCKSTEP_EARLY_TERMINATION, MC_LOCKSTEP_ALL_SCCS, and a positive
  integer n (lockstep enumerates up to n fair SCCs).]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Allocate an earlytermination struct and initialize with arguments]

  SideEffects []
******************************************************************************/
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;
}

/**Function********************************************************************

  Synopsis [Free an earlytermination struct (you are allowed to pass
  MC_NO_EARLY_TERMINATION, or NULL, and it will have no effect. ]

  SideEffects []
******************************************************************************/
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;
}

/**Function********************************************************************

  Synopsis [Return TRUE iff the early termination condition specifies that
  the computation can be entirely skipped.]

  SideEffects [none]
******************************************************************************/
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                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis [Make a path from aState to bState using fwd reachability.]

  Description [Make a path from aState to bState which only passes through
  invariantStates; it is assumed that aState and bState lie in invariantStates.
  Returns a sequence of states starting from aState, leading to bState. If
  aState == bState, a non trivial path is returned (ie a cycle). If no
  path exists, return NIL. It is the users responsibility to free the returned
  array as well as its members. This function starts from aState and does
  forward reachability till it hits bState or a fixed point.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Make a path from aState to bState using bwd reachability.]

  Description [Make a path from aState to bState which only passes through
  invariantStates; it is assumed that aState and bState lie in invariantStates.
  Returns a sequence of states starting from aState, leading to bState. If
  aState == bState, a non trivial path is returned (ie a cycle). If no
  path exists, return NIL. It is the users responsibility to free the returned
  array as well as its members. This function starts from bState and does
  backward reachability till it hits aState or a fixed point.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Write resettability condition as a CTL formula]

  CommandName      [_init_state_formula]

  CommandSynopsis [write resettability condition as a CTL formula]

  CommandArguments [ \[-h\] \[&lt;init_file&gt;\] ]

  CommandDescription [Write resettability condition as a CTL formula. Writes to
  <code>init_file</code> is specified, else stdout.]

  SideEffects []

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



/**Function********************************************************************

  Synopsis [Return a CTL formula for a minterm.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Search the given array of "Onion Rings" for the Onion Rings
  with the clore closest to specified state.]

  Description [Search the given array of "Onion Rings" for the Onion Rings with
  the core closest to specified state. By "Onion Rings" we refer to an array of
  sets of states (so arrayOfOnionRings is an array of arrays of states).  The
  first member of a set of onion rings is referred to as the "core". The "Onion
  Rings" array has the property that the first set is all states that can reach
  the core (this may be mod a care set like the reached states).  The succesive
  sets are those which can reach the core in successively fewer iterations.

  We find the i with the smallest index j for which arrayOfOnionRings[i][j]
  contains aState.]

  SideEffects []

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



/**Function********************************************************************

  Synopsis [Remove array indexed by index from array of arrays.]

  Description [Remove array indexed by index from array of arrays. Does NOT
  free the input arrayOfOnionRings.]

  SideEffects []

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







/**Function********************************************************************

  Synopsis [Convert a minterm to an array of integers]

  SideEffects []

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





/**Function********************************************************************

  Synopsis [Print a transition to vis_stdout.]

  Description [Print a transition to vis_stdout. The transition is supposed to be
  from aState to bState on input vInput. If uInput is not NIL, instead of
  printing vInput, we only print the places where it differs from uInput. If there
  is no difference anywhere, we print "-Unchanged-". Similarly, we print only the
  incremental difference from aState to bState; if there is none, we print "-Unchanged-".
  If aState is NIL we simply print bState and return.]

  SideEffects []

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




/**Function********************************************************************

  Synopsis [Print a transition to vis_stdout.]

  Description [Print a transition to vis_stdout. The transition is supposed to be
  from aState to bState on input vInput. If uInput is not NIL, instead of
  printing vInput, we only print the places where it differs from uInput. If there
  is no difference anywhere, we print "-Unchanged-". Similarly, we print only the
  incremental difference from aState to bState; if there is none, we print "-Unchanged-".
  If aState is NIL we simply print bState and return.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Print message saying given state passes formula.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Print message saying given state fails formula.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Utility function - prints state passes or fails formula]

  SideEffects []

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



/**Function********************************************************************

  Synopsis [Utility function - convert McPath_t to normal form.]

  Description [Utility function - convert McPath_t to normal form.
  A normal McPath_t is one where the stem leads to a state, which then returns
  it self in the cycle.]

  SideEffects []

******************************************************************************/

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;

}



/**Function********************************************************************

  Synopsis [Utility function - merges two paths.]

  Description [Utility function - merges two paths. Note that the merge is done
  by adding the elements of the second array starting from the second element onwards.
  This is because we often have to merge paths where the end point of the first is the
  starting point of the second.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Utility function - duplicate bdd array.]

  Description [To represent the forced segment, the mdd_t is complemented.
               Therefore one cannot use mdd_array_duplicate.
               This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Utility function - compute the intersection of the elements.]

  Description [Utility function - compute the intersection of the elements.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Utility function - compute the union of the elements.]

  Description [Utility function - compute the union of the elements.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Utility function - joins two paths.]

  Description [Utility function - joins two paths. Note that the joins is done
  by adding the elements of the second array starting from the first element onwards.]

  SeeAlso [McCreateMergedPath]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [ Check to see if aState lies in set of states satisfying aFormula ]

  SideEffects []

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



/**Function********************************************************************

  Synopsis [ Tests aState is a member of setOfStates ]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Obtain a successor of aState which is in targetStates]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Obtain a successor of aState which is in targetStates]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Obtain stem of fair path]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Obtain cycle of fair path]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set stem of fair path]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set cycle of fair path]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Allocate a  Path Struct]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Free a  Path Struct]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Allocate an McOptions_t struct.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Free an McOptions_t struct.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Return Dbg level set at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return filepointer for guide file (NULL if guided search
  is disabled)]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return filepointer for system variables file for FAFW ]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return time out period set at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return Verbosity level of options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return the language emptiness checking method of options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return Dbg level of options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return ctl file set at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return debug file set at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read sim flag at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read use more as pipe at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Returns the value of Vacuity Detection option.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Returns the value of the option for the Beer method.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Read use CTL formula specific reduction.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read print inputs in debug trace.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read use of CTL formula tree.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read schedule for GSH.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read lockstep option.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read reachability analysis type for check_invariant]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read onion rings flag for check_invariant]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read whether to use forward or backward analysis]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read whether to use forward or backward traversal.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read ARDC options.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Read whether to do coverage computation using Hoskote et.al's algorithm]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Read whether to do coverage computation using the improved algorithm]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set use forward or backward analysis]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set guided search file (set to NULL if no guided search)]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set varibles for system file for FAFW]

  SideEffects []

******************************************************************************/
void
McOptionsSetVariablesForSystem(
  McOptions_t *options,
  FILE  *systemFile )
{
  options->systemFile = systemFile;
}
/**Function********************************************************************

  Synopsis [Set use forward or backward traversal]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set use more pipe flag at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set reduce fsm flag]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set Vacuity Detect flag]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set Beer Method for vacuity detection flag]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set flag for fate and free will algorithm]

  SideEffects []

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

  Synopsis [Set print inputs flag]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set use formula tree flag]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set GSH schedule]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set lockstep option]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set sim flag at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set Dbg level at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set Verbosity at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set language emptiness checking method at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set Dc level at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set ARDC options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set a flag to store onion rings during invariant checking.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Set CTL File at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set Debug File at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set ime out periopd at options.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set reachability analysis type]

  SideEffects []

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



/**Function********************************************************************

  Synopsis [Set do Coverage-Hoskote flag]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Set do Coverage-Improved flag]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Query user to continue.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Print Support of Function]

  SideEffects []

******************************************************************************/

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



/**Function********************************************************************

  Synopsis [Print path as sim trace]

  SideEffects []

******************************************************************************/



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


/**Function********************************************************************

  Synopsis [Form an FSM reduced with respect to the specified formula]

  Description [Form an FSM reduced with respect to the CTL formula array. All latches
  and inputs which affect the given formula AND the fairness conditions of the
  system are included in this reduced fsm.]

  SideEffects []

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

}

/**Function********************************************************************

  Synopsis [Update the early termination condition.]

  Description [Update the early termination condition.

  MC_NO_EARLY_TERMINATION is equivalent to mode=CARE and
  states=mdd_one.  careStates=NIL is equivalent to either
  careStates=mdd_zero (for disjunction) or careStates=mdd_one (in the
  other cases).  With these provisions, the propagation algorithm can
  be summarized thus.

  <p> For negation, ALL becomes SOME and vice versa, while CARE is
  passed unchanged.

  <p> For conjunction, disjunction, and implication: if the current
  node has a termination condition of type ALL or SOME, this is
  refined and propagated.  Otherwise, the returned early termination
  condition is of type CARE.  The care states are the conjunction of
  earlyTermination->states and either careStates (for conjunction and
  implication) or the complement of careStates (for disjunction).

  <p> In some cases, one can immediately determine that the goal
  cannot be reached, or has already been reached.  In these cases, the
  termination condition has mode=CARE and states=mdd_zero.

  <p> The other types of formulae produce no early termination
  condition for their children.  That is, they declare that all states
  are care states.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Check if an underapproximation of the evaluation
  guarantees that the early termination conditions hold.]

  Description [Check if an underapproximation of the evaluation
  guarantees that the early termination conditions hold , modulo a
  care set modeled by an implicitly conjoined array of bdds.

  If we are looking for ALL of ETstates, or we are are given a set of
  CARE states, then we are done if ETstates \subseteq underapprox,
  because that implies ETstates \subseteq exactset.

  If we are looking for SOME of ETstates, we are done if underapprox and
  ETstates overlap, because that means that the exact set and ETstates also
  overlap.

  If earlyTermination == MC_NO_EARLY_TERMINATION, the result of the
  function is false.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Check if an overapproximation of the evaluation guarantees
  that the early termination conditions hold.]

  Description [Check if an overapproximation of the evaluation
  guarantees that the early termination conditions hold, modulo a care
  set modeled by an implicitly conjoined array of bdds.

  If we are looking for ALL of ETstates, then we are done if we have
  overapprox is not a superset of ETstates, because the exact set will
  not hold all of ETstates.

  If we are looking for SOME of ETstates, or we are given a set of
  CARE states, we are done if overapprox is disjoint from ETstates,
  because that means that the exact set is also disjoint from
  ETstates.

  If earlyTermination == MC_NO_EARLY_TERMINATION, the result of the
  function is false.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Return an array of formulae representing the hints]

  Description [Read the guide file and store the hint formulae in an
  array. Adds the 1 hint to the end of the array.

  Returns NIL if something goes wrong: parse error in the file or temporal
  operators in the hints]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return an array of variables controlled by system ]

  Description [Read the system variables file and store the variables controlled by system in an array.

  Returns NIL if something goes wrong: parse error in the file or variables that  are not contained in model.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis []

  Description []

  SideEffects []

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

}

/**Function********************************************************************

  Synopsis [Return an array of states corresponding to the hints]

  Description [Flushes the states associated with the hints,and reevaluates
  them in the current fsm. Quantifies out variables in the hint that are not in
  present state or primary input set of the current FSM.

  Returns NIL if something goes wrong (the hint does not fit the fsm).]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Return an array of hints]

  Description [Read the guide file and compute the BDDs of the hints
  and store in an array. Adds the 1 hint to the end of the array.

  Closes the guideFP.

  Returns NIL if something goes wrong.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Read and parse the hints_type set flag]

  Description [Read and parse the hints_type set flag.  If it is not
  set return the default: local.  Return Mc_None_c if there is an
  error.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Debug function to check if there exists a proper input value]

  Description [Check the existence of path by extracting input condition.]

  SideEffects []

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

}

/**Function********************************************************************

  Synopsis [Debug function to check if there exists a proper input value]

  Description [Check the existence of path by extracting input condition.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Print states in terms of state variables]

  Description [Print states in terms of state variables]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Print the number of states]

  Description [Print the number of states.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Print the states of each ring]

  Description [Print the states of each ring]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Print the number of states of each ring]

  Description [Print the number of states of each ring]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Pick a minterm from the given set close to target. Support
  is an array of mddids representing the total support; that is, all
  the variables on which aSet may depend.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Select a state from the given set]

  SideEffects []

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


/**Function********************************************************************

  Synopsis    [Converts a string to a schedule type.]

  Description [Converts a string to a schedule type.  If string does
  not refer to one of the allowed schedule types, then returns
  McGSH_Unassigned_c.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis    [Converts a string to a lockstep mode.]

  Description [Converts a string to a lockstep mode.  If string does
  not refer to one of the allowed lockstep modes, it returns
  MC_LOCKSTEP_UNASSIGNED.  The allowed values are: MC_LOCKSTEP_OFF,
  MC_LOCKSTEP_EARLY_TERMINATION, MC_LOCKSTEP_ALL_SCCS, and a positive
  integer n (lockstep enumerates up to n fair SCCs).]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Print  an array of nodes]

  SideEffects []

******************************************************************************/

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


/**Function********************************************************************

  Synopsis [Print  an array of nodes]

  SideEffects []

******************************************************************************/

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

/**Function********************************************************************

  Synopsis [Print  an array of nodes]

  SideEffects []

******************************************************************************/


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

/**Function********************************************************************

  Synopsis [Compare two strings in the from of char **]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Perform simple static semantic checks on formula.]

  SideEffects []

  SeeAlso [Mc_FormulaStaticSemanticCheckOnNetwork]
******************************************************************************/
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;
}

/**Function********************************************************************

  Synopsis [Add nodes for wires referred to in formula to nodesTable.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Add nodes for wires referred to in formula to nodesTable.]

  SideEffects []

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

/**Function********************************************************************

  Synopsis [Test that given mdd is a minterm.]

  SideEffects []

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


/**Function********************************************************************

  Synopsis [Test that given mdd is a minterm.]

  SideEffects []

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