src/fsm/fsmFsm.c

Go to the documentation of this file.

#include "fsmInt.h"

static char rcsid[] UNUSED = "$Id: fsmFsm.c,v 1.88 2007/04/02 17:03:13 hhkim Exp $";

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

static Fsm_Fsm_t * FsmStructAlloc(Ntk_Network_t *network, graph_t *partition);
static void FsmCreateVariableCubes(Fsm_Fsm_t *fsm);
static int nameCompare(const void * name1, const void * name2);
static boolean VarIdArrayCompare(mdd_manager *mddMgr, array_t *vars1, array_t *vars2);
static boolean NSFunctionNamesCompare(mdd_manager *mddMgr, array_t *names1, array_t *names2);
static array_t * GetMddSupportIdArray(Fsm_Fsm_t *fsm, st_table *mddIdTable, st_table *pseudoMddIdTable);

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

Fsm_Fsm_t *
Fsm_FsmCreateFromNetworkWithPartition(
  Ntk_Network_t *network,
  graph_t       *partition)
{
  lsGen       gen;
  Ntk_Node_t *latch;
  Ntk_Node_t *input;
  Fsm_Fsm_t  *fsm;
  int i;
  
  fsm = FsmStructAlloc(network, partition);
  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t);
  fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm);
  
  /* sort by name of latch */
  Ntk_NetworkForEachLatch(network, gen, latch){
    array_insert_last(char*, fsm->fsmData.nextStateFunctions,
                      Ntk_NodeReadName(latch));
  }

  array_sort(fsm->fsmData.nextStateFunctions, nameCompare);

  for (i = 0; i < array_n(fsm->fsmData.nextStateFunctions); i ++) {
    char *nodeName;
    nodeName = array_fetch(char *, fsm->fsmData.nextStateFunctions, i);
    latch = Ntk_NetworkFindNodeByName(network, nodeName);
    array_insert(char*, fsm->fsmData.nextStateFunctions, i,
                 Ntk_NodeReadName(Ntk_LatchReadDataInput(latch)));
    array_insert_last(int, fsm->fsmData.presentStateVars,
                      Ntk_NodeReadMddId(latch));
    array_insert_last(int, fsm->fsmData.nextStateVars,
                      Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
  }
  
  Ntk_NetworkForEachInput(network, gen, input){
    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input));
  }
  
  FsmCreateVariableCubes(fsm);
  return (fsm);
}



Fsm_Fsm_t *
Fsm_FsmCreateReducedFsm(
  Ntk_Network_t *network,
  graph_t       *partition,
  array_t       *latches,
  array_t       *inputs,
  array_t       *fairArray)
{
  Ntk_Node_t *latch;
  Ntk_Node_t *input;
  Fsm_Fsm_t  *fsm;
  Fsm_Fairness_t *fairness;
  int i,j;
  
  if (array_n(latches) == 0){
    error_append("Number of latches passed = 0. Cannot create sub-FSM.");
    return (NIL(Fsm_Fsm_t));
  }
  
  fsm = FsmStructAlloc(network, partition);
  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t);

  /* initialize fairness constraints */
  if (fairArray != NIL(array_t)){
    fairness = FsmFairnessAlloc(fsm);    
    for (j = 0; j < array_n(fairArray); j++) {
      Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, fairArray, j);
      
      FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j);
    }
    fsm->fairnessInfo.constraint = fairness;
  }
  else {
    fsm->fairnessInfo.constraint =
        FsmFsmCreateDefaultFairnessConstraint(fsm);
  }

  /* sort latches by name */
  for(i=0; i<array_n(latches); i++){
    latch = array_fetch(Ntk_Node_t*, latches, i);
    array_insert_last(char*, fsm->fsmData.nextStateFunctions,
                      Ntk_NodeReadName(latch));
  }
  array_sort(fsm->fsmData.nextStateFunctions, nameCompare);

  for(i=0; i<array_n(latches); i++){
    char *nodeName;
    nodeName = array_fetch(char *, fsm->fsmData.nextStateFunctions, i);
    latch = Ntk_NetworkFindNodeByName(network, nodeName);  
    array_insert_last(int, fsm->fsmData.presentStateVars,
                      Ntk_NodeReadMddId(latch));
    array_insert_last(int, fsm->fsmData.nextStateVars,
                      Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
    array_insert(char*, fsm->fsmData.nextStateFunctions, i, 
                      Ntk_NodeReadName(Ntk_LatchReadDataInput(latch)));
  }
  
  for(i=0; i<array_n(inputs); i++){
    input = array_fetch(Ntk_Node_t*, inputs, i);
    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input));
  }

  FsmCreateVariableCubes(fsm);
  return (fsm);
}

Fsm_Fsm_t *
Fsm_FsmCreateAbstractFsm(
  Ntk_Network_t *network,
  graph_t       *partition,
  array_t       *latches,
  array_t       *invisibleVars,
  array_t       *inputs,
  array_t       *fairArray,
  boolean        independentFlag)
{
  Ntk_Node_t *latch;
  Ntk_Node_t *input;
  Ntk_Node_t *node;
  Fsm_Fsm_t  *fsm;
  Fsm_Fairness_t *fairness;
  int i,j;
  
  if (FALSE && array_n(latches) == 0){
    error_append("Number of latches passed = 0. Cannot create sub-FSM.");
    return (NIL(Fsm_Fsm_t));
  }
  
  fsm = FsmStructAlloc(network, partition);
  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t);

  /* initialize fairness constraints */
  if (fairArray != NIL(array_t)){
    fairness = FsmFairnessAlloc(fsm);    
    for (j = 0; j < array_n(fairArray); j++) {
      Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, fairArray, j);
      
      FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j);
    }
    fsm->fairnessInfo.constraint = fairness;
  }
  else {
    fsm->fairnessInfo.constraint =
        FsmFsmCreateDefaultFairnessConstraint(fsm);
  }

  /* when independentFlag==FALSE, use globalPsVars and
   * primaryInputVars (instead of presentStateVars and inputVars) to
   * build the transition relation
   */
  if (!independentFlag) {
    fsm->fsmData.globalPsVars = array_alloc(int, 0);
    fsm->fsmData.primaryInputVars = array_alloc(int, 0);
  }


  /* sort latches by name */
  for(i=0; i<array_n(latches); i++){
    latch = array_fetch(Ntk_Node_t*, latches, i);
    array_insert_last(char*, fsm->fsmData.nextStateFunctions,
                      Ntk_NodeReadName(latch));
  }
  array_sort(fsm->fsmData.nextStateFunctions, nameCompare);

  for(i=0; i<array_n(latches); i++){
    char *nodeName;
    nodeName = array_fetch(char *, fsm->fsmData.nextStateFunctions, i);
    latch = Ntk_NetworkFindNodeByName(network, nodeName);  
    array_insert_last(int, fsm->fsmData.presentStateVars,
                      Ntk_NodeReadMddId(latch));
    array_insert_last(int, fsm->fsmData.nextStateVars,
                      Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
    array_insert(char*, fsm->fsmData.nextStateFunctions, i, 
                      Ntk_NodeReadName(Ntk_LatchReadDataInput(latch)));
    
    if (!independentFlag)
      array_insert_last(int, fsm->fsmData.globalPsVars,
                        Ntk_NodeReadMddId(latch));      
  }

  for(i=0; i<array_n(inputs); i++){
    input = array_fetch(Ntk_Node_t*, inputs, i);
    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input));
    
    if (!independentFlag)
      array_insert_last(int, fsm->fsmData.primaryInputVars, 
                        Ntk_NodeReadMddId(input));
  }


  arrayForEachItem(Ntk_Node_t *, invisibleVars, i, node) {
    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(node));

    if (!independentFlag) {
      array_insert_last(int, fsm->fsmData.globalPsVars, 
                        Ntk_NodeReadMddId(node));
    }
  }


  FsmCreateVariableCubes(fsm);
  return (fsm);
}


void
Fsm_FsmFree(
  Fsm_Fsm_t * fsm)
{
  Part_PartitionFree(fsm->partition);
  Fsm_FsmSubsystemFree(fsm);
}

void
Fsm_FsmSubsystemFree(
  Fsm_Fsm_t * fsm)
{

  Fsm_FsmFreeImageInfo(fsm);
  
  /* Free reachability info. */
  if (fsm->reachabilityInfo.initialStates != NIL(mdd_t)){
    mdd_free(fsm->reachabilityInfo.initialStates);
  }
  if (fsm->reachabilityInfo.reachableStates != NIL(mdd_t)){
    mdd_free(fsm->reachabilityInfo.reachableStates);
  }
  if (fsm->reachabilityInfo.apprReachableStates != NIL(array_t))
    mdd_array_free(fsm->reachabilityInfo.apprReachableStates);
  if (fsm->reachabilityInfo.subPsVars != NIL(array_t)){
    int i;
    array_t *psVars;
    arrayForEachItem(array_t *, fsm->reachabilityInfo.subPsVars, i, psVars) {
      array_free(psVars);
    }
    array_free(fsm->reachabilityInfo.subPsVars);
  }
  if (Fsm_FsmReadReachabilityOnionRings(fsm) != NIL(array_t)){
    mdd_array_free(Fsm_FsmReadReachabilityOnionRings(fsm));
  }

  /* Free fairness info. */
  FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), NIL(Fsm_Fairness_t), NIL(array_t));

  array_free(fsm->fsmData.presentStateVars);
  array_free(fsm->fsmData.nextStateVars);
  array_free(fsm->fsmData.inputVars);
  array_free(fsm->fsmData.nextStateFunctions);
  if (fsm->fsmData.pseudoInputVars)
    array_free(fsm->fsmData.pseudoInputVars);
  if (fsm->fsmData.primaryInputVars)
    array_free(fsm->fsmData.primaryInputVars);
  if (fsm->fsmData.globalPsVars)
    array_free(fsm->fsmData.globalPsVars);

  if (fsm->fsmData.presentStateCube)
    mdd_free(fsm->fsmData.presentStateCube);
  if (fsm->fsmData.nextStateCube)
    mdd_free(fsm->fsmData.nextStateCube);
  if (fsm->fsmData.inputCube)
    mdd_free(fsm->fsmData.inputCube);
  if (fsm->fsmData.pseudoInputCube)
    mdd_free(fsm->fsmData.pseudoInputCube);
  if (fsm->fsmData.primaryInputCube)
    mdd_free(fsm->fsmData.primaryInputCube);
  if (fsm->fsmData.globalPsCube)
    mdd_free(fsm->fsmData.globalPsCube);

  if (fsm->fsmData.pseudoInputBddVars)
    mdd_array_free(fsm->fsmData.pseudoInputBddVars);
  if (fsm->fsmData.presentStateBddVars)
    mdd_array_free(fsm->fsmData.presentStateBddVars);

  FREE(fsm);
}

void
Fsm_FsmFreeCallback(
  void * data /* an object of type Fsm_Fsm_t*  type casted to void* */)
{
  Fsm_FsmFree((Fsm_Fsm_t *) data);
}


Ntk_Network_t *
Fsm_FsmReadNetwork(
  Fsm_Fsm_t * fsm)
{
  return (fsm->network);
}

boolean
Fsm_FsmReadUseUnquantifiedFlag(
  Fsm_Fsm_t * fsm)
{
  return (fsm->useUnquantifiedFlag);
}

mdd_manager *
Fsm_FsmReadMddManager(
  Fsm_Fsm_t * fsm)
{
  return (Ntk_NetworkReadMddManager(fsm->network));
}


Fsm_Fsm_t *
Fsm_NetworkReadOrCreateFsm(
  Ntk_Network_t * network)
{
  Fsm_Fsm_t *fsm = (Fsm_Fsm_t*) Ntk_NetworkReadApplInfo(network, FSM_NETWORK_APPL_KEY);
      
  if (fsm == NIL(Fsm_Fsm_t)) {
    fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
    if (fsm != NIL(Fsm_Fsm_t)) {
      (void) Ntk_NetworkAddApplInfo(network, FSM_NETWORK_APPL_KEY,
                             (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
                             (void *) fsm);
    }
  }
  
  return fsm;
}


Fsm_Fsm_t *
Fsm_NetworkReadFsm(
  Ntk_Network_t * network)
{
  return ((Fsm_Fsm_t*) Ntk_NetworkReadApplInfo(network,
                                               FSM_NETWORK_APPL_KEY));
}


Img_ImageInfo_t *
Fsm_FsmReadImageInfo(
  Fsm_Fsm_t *fsm)
{
  return (fsm->imageInfo);
}

void
Fsm_FsmSetImageInfo(
  Fsm_Fsm_t *fsm, Img_ImageInfo_t *imageInfo)
{
  fsm->imageInfo = imageInfo;
}

void
Fsm_FsmFreeImageInfo(
  Fsm_Fsm_t *fsm)
{
  if(fsm->imageInfo) {
    Img_ImageInfoFree(fsm->imageInfo);
    fsm->imageInfo = NIL(Img_ImageInfo_t);
  }

  if(fsm->unquantifiedImageInfo) {
    Img_ImageInfoFree(fsm->unquantifiedImageInfo);
    fsm->unquantifiedImageInfo = NIL(Img_ImageInfo_t);
  }
}

graph_t *
Fsm_FsmReadPartition(
  Fsm_Fsm_t *fsm)
{
  return (fsm->partition);
}

boolean
Fsm_FsmTestIsReachabilityDone(
  Fsm_Fsm_t *fsm)
{
  
  if (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t)) {
        return TRUE;
  }
  return FALSE;
}

boolean
Fsm_FsmTestIsOverApproximateReachabilityDone(
  Fsm_Fsm_t *fsm)
{
  
  if (Fsm_FsmReadOverApproximateReachableStates(fsm) != NIL(array_t)) {
        return TRUE;
  }
  return FALSE;
}


mdd_t *
Fsm_FsmReadReachableStates(
  Fsm_Fsm_t *fsm)
{
  if (fsm->reachabilityInfo.rchStatus == Fsm_Rch_Exact_c)
    return(fsm->reachabilityInfo.reachableStates);
  else
    return(NIL(mdd_t));
}


mdd_t *
Fsm_FsmReadCurrentReachableStates(
  Fsm_Fsm_t *fsm)
{
  return(fsm->reachabilityInfo.reachableStates);
}


array_t *
Fsm_FsmReadOverApproximateReachableStates(
  Fsm_Fsm_t *fsm)
{
  if (fsm->reachabilityInfo.overApprox >= 2)
    return(fsm->reachabilityInfo.apprReachableStates);
  else
    return(NIL(array_t));
}


array_t *
Fsm_FsmReadCurrentOverApproximateReachableStates(
  Fsm_Fsm_t *fsm)
{
  return(fsm->reachabilityInfo.apprReachableStates);
}

array_t *
Fsm_FsmReadReachabilityOnionRings(
  Fsm_Fsm_t *fsm)
{
  return fsm->reachabilityInfo.onionRings;
}

boolean
Fsm_FsmReachabilityOnionRingsStates(
  Fsm_Fsm_t *fsm,
  mdd_t ** result)
{
  int i;
  mdd_t *tmpMdd;
  mdd_t *ring;
  array_t *onionRings;

  onionRings = Fsm_FsmReadReachabilityOnionRings(fsm);
  if ( onionRings == NIL(array_t) ) {
    *result = NIL(mdd_t);
    return 0;
  }

  *result = bdd_zero(Fsm_FsmReadMddManager(fsm));
  arrayForEachItem(mdd_t *, onionRings, i, ring) {
    tmpMdd = mdd_or(*result, ring, 1, 1);
    mdd_free(*result);
    *result = tmpMdd;
  }
  if (Fsm_FsmReadCurrentReachableStates(fsm)) {
    if (mdd_lequal(Fsm_FsmReadCurrentReachableStates(fsm), *result, 1,1)) {
      FsmSetReachabilityOnionRingsUpToDateFlag(fsm, TRUE);
    }
  }
  return (Fsm_FsmTestReachabilityOnionRingsUpToDate(fsm));
}

boolean
Fsm_FsmTestReachabilityOnionRingsUpToDate(
  Fsm_Fsm_t *fsm)
{
  return fsm->reachabilityInfo.onionRingsUpToDate;
}

Fsm_RchType_t
Fsm_FsmReadReachabilityOnionRingsMode(
  Fsm_Fsm_t *fsm)
{
  return fsm->reachabilityInfo.onionRingsMode;
}

  
Img_ImageInfo_t *
Fsm_FsmReadOrCreateImageInfo(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag)
{
  Img_DirectionType     imgFlag = Img_Forward_c;
  array_t               *presentStateVars, *inputVars;
  mdd_t                 *presentStateCube, *inputCube;

  if (bwdImgFlag && fwdImgFlag)
    imgFlag = Img_Both_c;
  else if (bwdImgFlag)
    imgFlag = Img_Backward_c;

  if (fsm->fsmData.globalPsVars) {
    presentStateVars = fsm->fsmData.globalPsVars;
    inputVars = fsm->fsmData.primaryInputVars;
    presentStateCube = fsm->fsmData.globalPsCube;
    inputCube = fsm->fsmData.primaryInputCube;
  } else {
    presentStateVars = fsm->fsmData.presentStateVars;
    inputVars = fsm->fsmData.inputVars;
    presentStateCube = fsm->fsmData.presentStateCube;
    inputCube = fsm->fsmData.inputCube;
  }

  fsm->imageInfo = Img_ImageInfoInitialize(fsm->imageInfo,
                                           fsm->partition,
                                           fsm->fsmData.nextStateFunctions,
                                           presentStateVars,
                                           fsm->fsmData.nextStateVars,
                                           inputVars,
                                           presentStateCube,
                                           fsm->fsmData.nextStateCube,
                                           inputCube,
                                           fsm->network,
                                           Img_Default_c, imgFlag, 0, 0);

  if (fsm->fsmData.globalPsVars) {
    Img_ImageInfoUpdateVariables(fsm->imageInfo,
                                 fsm->partition,
                                 fsm->fsmData.presentStateVars,
                                 fsm->fsmData.inputVars,
                                 fsm->fsmData.presentStateCube,
                                 fsm->fsmData.inputCube);
  }

  return(fsm->imageInfo);
}

Img_ImageInfo_t *
Fsm_FsmReadOrCreateImageInfoFAFW(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag)
{
  Img_DirectionType     imgFlag = Img_Forward_c;
  array_t               *presentStateVars, *inputVars;
  mdd_t                 *presentStateCube, *inputCube;
  mdd_manager           *mgr;

  mgr = Fsm_FsmReadMddManager(fsm);

  if (bwdImgFlag && fwdImgFlag)
    imgFlag = Img_Both_c;
  else if (bwdImgFlag)
    imgFlag = Img_Backward_c;

  presentStateVars = fsm->fsmData.presentStateVars;
  inputVars = array_alloc(int , 0);
  presentStateCube = fsm->fsmData.presentStateCube;
  inputCube = mdd_one(mgr);

  fsm->unquantifiedImageInfo = Img_ImageInfoInitialize(
                                           fsm->unquantifiedImageInfo,
                                           fsm->partition,
                                           fsm->fsmData.nextStateFunctions,
                                           presentStateVars,
                                           fsm->fsmData.nextStateVars,
                                           inputVars,
                                           presentStateCube,
                                           fsm->fsmData.nextStateCube,
                                           inputCube,
                                           fsm->network,
                                           Img_Default_c, imgFlag, 1, 0);

  if(!Img_IsQuantifyArraySame(fsm->unquantifiedImageInfo, inputVars)) {
    array_free(inputVars);
  }

  if(!Img_IsQuantifyCubeSame(fsm->unquantifiedImageInfo, inputCube)) {
    mdd_free(inputCube);
  }

  return(fsm->unquantifiedImageInfo);
}

Img_ImageInfo_t *
Fsm_FsmReadOrCreateImageInfoPrunedFAFW(Fsm_Fsm_t *fsm, mdd_t *Winning, int bwdImgFlag, int fwdImgFlag)
{
  Img_DirectionType     imgFlag = Img_Forward_c;
  array_t               *presentStateVars, *inputVars;
  mdd_t                 *presentStateCube, *inputCube;
  mdd_manager           *mgr;
  Img_ImageInfo_t *imageInfo;

  mgr = Fsm_FsmReadMddManager(fsm);

  if (bwdImgFlag && fwdImgFlag)
    imgFlag = Img_Both_c;
  else if (bwdImgFlag)
    imgFlag = Img_Backward_c;

  presentStateVars = fsm->fsmData.presentStateVars;
  inputVars = array_alloc(int , 0);
  presentStateCube = fsm->fsmData.presentStateCube;
  inputCube = mdd_one(mgr);

  imageInfo = Img_ImageInfoInitialize(
                                           0,
                                           fsm->partition,
                                           fsm->fsmData.nextStateFunctions,
                                           presentStateVars,
                                           fsm->fsmData.nextStateVars,
                                           inputVars,
                                           presentStateCube,
                                           fsm->fsmData.nextStateCube,
                                           inputCube,
                                           fsm->network,
                                           Img_Default_c, imgFlag, 0, Winning);

  if(!Img_IsQuantifyArraySame(imageInfo, inputVars)) {
    array_free(inputVars);
  }

  if(!Img_IsQuantifyCubeSame(imageInfo, inputCube)) {
    mdd_free(inputCube);
  }

  return(imageInfo);
}


Img_ImageInfo_t *
Fsm_FsmReadOrCreateImageInfoForComputingRange(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag)
{
  Img_DirectionType     imgFlag = Img_Forward_c;
  array_t               *presentStateVars, *inputVars;
  mdd_t                 *presentStateCube, *inputCube;

  if (bwdImgFlag && fwdImgFlag)
    imgFlag = Img_Both_c;
  else if (bwdImgFlag)
    imgFlag = Img_Backward_c;

  if (fsm->fsmData.globalPsVars) {
    presentStateVars = fsm->fsmData.globalPsVars;
    inputVars = fsm->fsmData.primaryInputVars;
    presentStateCube = fsm->fsmData.globalPsCube;
    inputCube = fsm->fsmData.primaryInputCube;
  } else {
    presentStateVars = fsm->fsmData.presentStateVars;
    inputVars = fsm->fsmData.inputVars;
    presentStateCube = fsm->fsmData.presentStateCube;
    inputCube = fsm->fsmData.inputCube;
  }

  fsm->imageInfo = Img_ImageInfoInitialize(fsm->imageInfo,
                                           fsm->partition,
                                           fsm->fsmData.nextStateFunctions,
                                           presentStateVars,
                                           fsm->fsmData.nextStateVars,
                                           inputVars,
                                           presentStateCube,
                                           fsm->fsmData.nextStateCube,
                                           inputCube,
                                           fsm->network,
                                           Img_Linear_Range_c, imgFlag, 0, 0);

  if (fsm->fsmData.globalPsVars) {
    Img_ImageInfoUpdateVariables(fsm->imageInfo,
                                 fsm->partition,
                                 fsm->fsmData.presentStateVars,
                                 fsm->fsmData.inputVars,
                                 fsm->fsmData.presentStateCube,
                                 fsm->fsmData.inputCube);
  }

  return(fsm->imageInfo);
}

mdd_t *
Fsm_FsmComputeInitialStates(Fsm_Fsm_t *fsm)
{
  int            i = 0;
  lsGen          gen;
  mdd_t         *initStates;
  Ntk_Node_t    *node;
  array_t       *initRelnArray;
  array_t       *initMvfs;
  array_t       *initNodes;
  array_t       *initVertices;
  array_t       *latchMddIds;
  st_table      *supportNodes;
  st_table      *supportVertices;
  mdd_manager   *mddManager = Fsm_FsmReadMddManager(fsm);
  graph_t       *partition  = fsm->partition;
  Ntk_Network_t *network    = fsm->network;
  int            numLatches;
  array_t       *psVars;
  Img_MethodType imageMethod;
  
  /* If already computed, just return a copy. */
  if (fsm->reachabilityInfo.initialStates != NIL(mdd_t)){
    return (mdd_dup(fsm->reachabilityInfo.initialStates));
  }

  psVars = fsm->fsmData.presentStateVars;
  numLatches = array_n(psVars);

  /*
   * Get the array of initial nodes, both as network nodes and as partition
   * vertices.
   */
  initNodes    = array_alloc(Ntk_Node_t *, numLatches);
  initVertices = array_alloc(vertex_t *, numLatches);
  latchMddIds  = array_alloc(int, numLatches);
  for (i=0; i<numLatches; i++){
    int latchMddId = array_fetch(int, psVars, i);
    Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
    Ntk_Node_t *initNode   = Ntk_LatchReadInitialInput(latch);
    vertex_t   *initVertex = Part_PartitionFindVertexByName(partition,
                                Ntk_NodeReadName(initNode));
    array_insert(Ntk_Node_t *, initNodes, i, initNode);
    array_insert(vertex_t *, initVertices, i, initVertex);
    array_insert(int, latchMddIds, i, Ntk_NodeReadMddId(latch));
  }

  /*
   * Get the table of legal support nodes, both as network nodes and
   * as partition vertices. Inputs (both primary and pseudo) and constants
   * constitute the legal support nodes.
   */
  supportNodes    = st_init_table(st_ptrcmp, st_ptrhash);
  supportVertices = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachNode(network, gen, node) {
    vertex_t *vertex = Part_PartitionFindVertexByName(partition,
                                                      Ntk_NodeReadName(node));

    if (Ntk_NodeTestIsConstant(node) || Ntk_NodeTestIsInput(node)) {
      st_insert(supportNodes, (char *) node, NIL(char));
      st_insert(supportVertices, (char *) vertex, NIL(char));
    }
  }

  /*
   * If the initial nodes are not covered by the legal support nodes, then
   * return NIL.
   */
  if (!Ntk_NetworkTestLeavesCoverSupportOfRoots(network, initNodes,
                                                supportNodes)) {
    array_free(initNodes);
    array_free(initVertices);
    array_free(latchMddIds);
    st_free_table(supportNodes);
    st_free_table(supportVertices);
    return NIL(mdd_t);
  }

  /*
   * At this point, we are certain that the initialization functions are
   * well-defined. Get the MVF for each initialization node, in terms of the
   * support vertices.  Note that the MVF for each initial node is guaranteed to
   * exist in the partition, since an initial node is a combinational
   * output.
   */
  array_free(initNodes);
  st_free_table(supportNodes);
  initMvfs = Part_PartitionCollapse(partition, initVertices,
                                    supportVertices, NIL(mdd_t)); 
  array_free(initVertices);
  st_free_table(supportVertices);

  /* Compute the relation (x_i = g_i(u)) for each latch. */
  initRelnArray = array_alloc(mdd_t*, numLatches);
  for (i = 0; i < numLatches; i++) {
    int latchMddId = array_fetch(int, latchMddIds, i);
    Mvf_Function_t *initMvf = array_fetch(Mvf_Function_t *, initMvfs, i);
    mdd_t *initLatchReln = Mvf_FunctionBuildRelationWithVariable(initMvf,
                                                                latchMddId);
    array_insert(mdd_t *, initRelnArray, i, initLatchReln);
  }

  array_free(latchMddIds);
  Mvf_FunctionArrayFree(initMvfs);

  /* init_states(x) = \exists u \[\prod (x_i = g_i(u))\] */
  /*initStates = Fsm_MddMultiwayAndSmooth(mddManager, initRelnArray,
                                        fsm->fsmData.inputVars);
  */    

  imageMethod = Img_UserSpecifiedMethod();
  if (imageMethod != Img_Iwls95_c && imageMethod != Img_Mlp_c)
    imageMethod = Img_Iwls95_c;
  initStates = Img_MultiwayLinearAndSmooth(mddManager, initRelnArray,
                                           fsm->fsmData.inputVars, psVars,
                                           imageMethod, Img_Forward_c); 

  mdd_array_free(initRelnArray); 

  fsm->reachabilityInfo.initialStates = initStates;
  return mdd_dup(initStates);
}



array_t *
Fsm_FsmReadPresentStateVars(Fsm_Fsm_t *fsm)
{
  return fsm->fsmData.presentStateVars;
}

array_t *
Fsm_FsmReadNextStateVars(Fsm_Fsm_t *fsm)
{
  return fsm->fsmData.nextStateVars;
}

array_t *
Fsm_FsmReadNextStateFunctionNames(Fsm_Fsm_t *fsm)
{
  return fsm->fsmData.nextStateFunctions;
}

array_t *
Fsm_FsmReadInputVars(Fsm_Fsm_t *fsm)
{
  return fsm->fsmData.inputVars;
}

array_t *
Fsm_FsmReadPrimaryInputVars(Fsm_Fsm_t *fsm)
{
  return fsm->fsmData.primaryInputVars;
}


array_t *
Fsm_FsmReadPseudoInputVars(Fsm_Fsm_t *fsm)
{
  return fsm->fsmData.pseudoInputVars;
}

void
Fsm_FsmSetInputVars(Fsm_Fsm_t *fsm, array_t *inputVars)
{
  fsm->fsmData.inputVars = inputVars;
}

void
Fsm_FsmSetUseUnquantifiedFlag(Fsm_Fsm_t *fsm, boolean value)
{
  fsm->useUnquantifiedFlag = value;
}

void
Fsm_FsmSetInitialStates(Fsm_Fsm_t *fsm, mdd_t *initStates)
{
  mdd_t *init;
  
  init = fsm->reachabilityInfo.initialStates;
  if (init != NIL(mdd_t)) {
    mdd_free(init);
  }
  fsm->reachabilityInfo.initialStates = initStates;
}

int
Fsm_FsmReadFAFWFlag(Fsm_Fsm_t *fsm) 
{
  return((int)(fsm->FAFWFlag));
}

void
Fsm_FsmSetFAFWFlag(Fsm_Fsm_t *fsm, boolean FAFWFlag) 
{
  fsm->FAFWFlag = FAFWFlag;
}

void
Fsm_FsmSetSystemVariableFAFW(Fsm_Fsm_t *fsm, st_table *bddIdTable)
{
  mdd_manager *mgr;
  array_t *inputVars, *bddIdArray;
  bdd_t *extCube, *uniCube;
  bdd_t *newCube, *varBdd;
  st_generator *gen;
  int mddId, bddId, tbddId, i, j;

  if(bddIdTable == 0 && fsm->FAFWFlag == 0) {
    if(fsm->extQuantifyInputCube)
      bdd_free(fsm->extQuantifyInputCube);
    if(fsm->uniQuantifyInputCube)
      bdd_free(fsm->uniQuantifyInputCube);
    fsm->extQuantifyInputCube = 0;
    fsm->uniQuantifyInputCube = 0;
    return;
  }

  mgr = Fsm_FsmReadMddManager(fsm);
  inputVars = Fsm_FsmReadInputVars(fsm);

  extCube = mdd_one(mgr);
  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);
      if(bddIdTable && st_lookup_int(bddIdTable, (char *)(long)bddId, &tbddId)) {
        continue;
      }
      varBdd = bdd_get_variable(mgr, bddId);
      newCube = bdd_and(extCube, varBdd, 1, 1);
      bdd_free(extCube); bdd_free(varBdd);
      extCube = newCube;
    }
    array_free(bddIdArray);
  }
  uniCube = mdd_one(mgr);
  if(bddIdTable) {
    st_foreach_item(bddIdTable, gen, &bddId, &bddId) {
      varBdd = bdd_get_variable(mgr, bddId);
      newCube = bdd_and(uniCube, varBdd, 1, 1);
      bdd_free(uniCube); bdd_free(varBdd);
      uniCube = newCube;
    }
  }
  fsm->extQuantifyInputCube = extCube;
  fsm->uniQuantifyInputCube = uniCube;
}

bdd_t *
Fsm_FsmReadExtQuantifyInputCube(Fsm_Fsm_t *fsm)
{
  return(fsm->extQuantifyInputCube);
}

bdd_t *
Fsm_FsmReadUniQuantifyInputCube(Fsm_Fsm_t *fsm)
{
  return(fsm->uniQuantifyInputCube);
}

Fsm_Fsm_t *
Fsm_HrcManagerReadCurrentFsm(Hrc_Manager_t *hmgr)
{
  Fsm_Fsm_t     *fsm;
  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(hmgr);
  
  if (network == NIL(Ntk_Network_t)) {
    return NIL(Fsm_Fsm_t);
  }

  if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == FALSE) {
    (void) fprintf(vis_stderr, "** fsm error: The MDD variables have not been ordered.  ");
    (void) fprintf(vis_stderr, "Use static_order.\n");
    return NIL(Fsm_Fsm_t);
  }

  if (Part_NetworkReadPartition(network) == NIL(graph_t)){
    (void) fprintf(vis_stderr, "** fsm error: Network has not been partitioned.  ");
    (void) fprintf(vis_stderr, "Use build_partition_mdds.\n");
    return NIL(Fsm_Fsm_t);
  }

  error_init();
  fsm = Fsm_NetworkReadOrCreateFsm(network);
  if (fsm == NIL(Fsm_Fsm_t)) {
    (void) fprintf(vis_stderr, "%s", error_string());
    (void) fprintf(vis_stderr, "\n");
  }
  
  return fsm;
}

Fsm_Fsm_t *
Fsm_FsmCreateSubsystemFromNetwork(
  Ntk_Network_t *network,
  graph_t       *partition,
  st_table      *vertexTable,
  boolean       independentFlag,
  int           createPseudoVarMode)
{
  lsGen       gen;
  Ntk_Node_t *latch;
  Ntk_Node_t *input;
  Fsm_Fsm_t  *fsm;
  char *latchName;
  int i;
  st_table *pseudoMddIdTable = NIL(st_table);

  fsm = FsmStructAlloc(network, partition);
  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t);
  fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm);

  /*
   * Creates an FSM for the subsystem.
   */
  /* sort latches by name. */
  Ntk_NetworkForEachLatch(network, gen, latch) {
    latchName = Ntk_NodeReadName(latch); 
    if(st_lookup(vertexTable, latchName, (char **)0)) {
      array_insert_last(char*, fsm->fsmData.nextStateFunctions, latchName);
    } /* end of if(st_lookup(vertexTable)) */
  }

  if (independentFlag && createPseudoVarMode) {
    fsm->fsmData.pseudoInputVars = array_alloc(int, 0);
    fsm->fsmData.primaryInputVars = array_alloc(int, 0);
    fsm->fsmData.globalPsVars = array_alloc(int, 0);
    if (createPseudoVarMode == 2)
      pseudoMddIdTable = st_init_table(st_numcmp, st_numhash);
  }

  array_sort(fsm->fsmData.nextStateFunctions, nameCompare);
  
  arrayForEachItem(char *, fsm->fsmData.nextStateFunctions, i, latchName) {
    latch = Ntk_NetworkFindNodeByName(network, latchName); 
    array_insert(char*, fsm->fsmData.nextStateFunctions, i,
                 Ntk_NodeReadName(Ntk_LatchReadDataInput(latch)));
    array_insert_last(int, fsm->fsmData.nextStateVars,
                      Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
    array_insert_last(int, fsm->fsmData.presentStateVars,
                      Ntk_NodeReadMddId(latch));
  } /* end of Ntk_NetworkForEachLatch(network, gen, latch) */

  /* Fill in remaining latch for nextStateVars */
  if (!independentFlag || createPseudoVarMode) {
    Ntk_NetworkForEachLatch(network, gen, latch) {
      char *latchName = Ntk_NodeReadName(latch); 
      if(!st_lookup(vertexTable, latchName, (char **)0)) {
        if (independentFlag) {
          if (createPseudoVarMode == 1) {
            array_insert_last(int, fsm->fsmData.pseudoInputVars,
                                Ntk_NodeReadMddId(latch));
            array_insert_last(int, fsm->fsmData.inputVars,
                                Ntk_NodeReadMddId(latch));
          } else {
            st_insert(pseudoMddIdTable, (char *)(long)Ntk_NodeReadMddId(latch),
                        NIL(char));
          }
        } else {
          array_insert_last(int, fsm->fsmData.nextStateVars, 
                            Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
          array_insert_last(int, fsm->fsmData.presentStateVars,
                            Ntk_NodeReadMddId(latch));
        }
      }
    }
  }

  /* Input variables are identical for every subsystems */
  Ntk_NetworkForEachInput(network, gen, input){
    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input));
    if (independentFlag && createPseudoVarMode) {
      array_insert_last(int, fsm->fsmData.primaryInputVars,
                        Ntk_NodeReadMddId(input));
    }
  }

  if (independentFlag && createPseudoVarMode) {
    if (createPseudoVarMode == 2) {
      int       mddId;
      array_t   *supportMddIdArray;
      st_table  *mddIdTable;

      mddIdTable = st_init_table(st_numcmp, st_numhash);
      arrayForEachItem(int, fsm->fsmData.presentStateVars, i, mddId) {
        st_insert(mddIdTable, (char *)(long)mddId, NIL(char));
      }
      arrayForEachItem(int, fsm->fsmData.inputVars, i, mddId) {
        st_insert(mddIdTable, (char *)(long)mddId, NIL(char));
      }

      supportMddIdArray = GetMddSupportIdArray(fsm, mddIdTable,
                                                pseudoMddIdTable);

      arrayForEachItem(int, supportMddIdArray, i, mddId) {
        if (!st_lookup(mddIdTable, (char *)(long)mddId, NIL(char *))) {
          array_insert_last(int, fsm->fsmData.pseudoInputVars, mddId);
          array_insert_last(int, fsm->fsmData.inputVars, mddId);
        }
      }
      st_free_table(mddIdTable);
      st_free_table(pseudoMddIdTable);
      array_free(supportMddIdArray);
    }

    array_append(fsm->fsmData.globalPsVars, fsm->fsmData.presentStateVars);
    array_append(fsm->fsmData.globalPsVars, fsm->fsmData.pseudoInputVars);
  }

  FsmCreateVariableCubes(fsm);
  fsm->fsmData.presentStateBddVars = mdd_id_array_to_bdd_array(
    Fsm_FsmReadMddManager(fsm), fsm->fsmData.presentStateVars);
  return (fsm);
}

void
Fsm_InstantiateHint(
  Fsm_Fsm_t *fsm,
  mdd_t *hint,
  int fwdFlag,
  int bwdFlag,
  Ctlp_Approx_t type,
  int printStatus)
{
  boolean underApprox = FALSE;
  Img_DirectionType imgFlag = Img_Forward_c;

  assert(type != Ctlp_Incomparable_c);
  
  if (bwdFlag && fwdFlag)
    imgFlag = Img_Both_c;
  else if (bwdFlag)
    imgFlag = Img_Backward_c;

  switch (type) {
  case (Ctlp_Underapprox_c): underApprox = TRUE; break;
  case (Ctlp_Overapprox_c): underApprox = FALSE; break;
  case (Ctlp_Exact_c):
    underApprox = TRUE;
    hint = mdd_one(Fsm_FsmReadMddManager(fsm));
    break;
  default: assert(0); break;
  }
  /* If we reach this point, underApprox has been explicitly assigned
   * by the switch. */
  
  Img_ImageConstrainAndClusterTransitionRelation(
    Fsm_FsmReadOrCreateImageInfo(fsm, bwdFlag, fwdFlag),
    imgFlag,
    hint,
    ((underApprox == TRUE) ?
     Img_GuidedSearchReadUnderApproxMinimizeMethod() :
     Img_GuidedSearchReadOverApproxMinimizeMethod()),
    underApprox, /* underapprox */
    0, /* dont clean up */
    0, /* no variable reordering */
    printStatus);

  Fsm_MinimizeTransitionRelationWithReachabilityInfo(fsm, imgFlag,
                                                     printStatus); 
  
  if (type == Ctlp_Exact_c) mdd_free(hint);

  return;
}

void
Fsm_CleanUpHints( Fsm_Fsm_t *fsm, int fwdFlag, int bwdFlag, int printStatus)
{
  Img_DirectionType     imgFlag = Img_Forward_c;
  mdd_t *one = bdd_one(Fsm_FsmReadMddManager(fsm));
  if (bwdFlag && fwdFlag)
    imgFlag = Img_Both_c;
  else if (bwdFlag)
    imgFlag = Img_Backward_c;

  Img_ImageConstrainAndClusterTransitionRelation(fsm->imageInfo,
                                                 imgFlag,
                                                 one,
                                                 Img_GuidedSearchReadUnderApproxMinimizeMethod(),
                                                 1, /* under approx */
                                                 1, /* clean up */
                                                 0, /* no variable reordering */
                                                 printStatus);
  mdd_free(one);
  return;
}


void
Fsm_FsmFreeReachableStates(Fsm_Fsm_t *fsm)
{
  if (fsm->reachabilityInfo.reachableStates) {
    mdd_free(fsm->reachabilityInfo.reachableStates);
    fsm->reachabilityInfo.reachableStates = NIL(mdd_t);
  }
}

void
Fsm_FsmFreeOverApproximateReachableStates(Fsm_Fsm_t *fsm)
{
  if (fsm->reachabilityInfo.apprReachableStates) {
    mdd_array_free(fsm->reachabilityInfo.apprReachableStates);
    fsm->reachabilityInfo.apprReachableStates = NIL(array_t);
    fsm->reachabilityInfo.overApprox = Fsm_Ardc_NotConverged_c;
  }
  if (fsm->reachabilityInfo.subPsVars) {
    int i;
    array_t *psVars;

    for (i = 0; i < array_n(fsm->reachabilityInfo.subPsVars); i++) {
      psVars = array_fetch(array_t *, fsm->reachabilityInfo.subPsVars, i);
      array_free(psVars);
    }
    array_free(fsm->reachabilityInfo.subPsVars);
    fsm->reachabilityInfo.subPsVars = NIL(array_t);
  }
}


int
Fsm_FsmGetReachableDepth(Fsm_Fsm_t *fsm)
{
    return(fsm->reachabilityInfo.depth);
}

boolean
Fsm_FsmCheckSameSubFsmInTotalFsm(Fsm_Fsm_t *fsm,
                                 Fsm_Fsm_t *subFsm1,
                                 Fsm_Fsm_t *subFsm2)
{
  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
  boolean result;
  
  assert(Fsm_FsmReadNetwork(fsm) == Fsm_FsmReadNetwork(subFsm1));
  assert(Fsm_FsmReadNetwork(fsm) == Fsm_FsmReadNetwork(subFsm2));
  assert(Fsm_FsmReadMddManager(subFsm1) == mddMgr);
  assert(Fsm_FsmReadMddManager(subFsm2) == mddMgr);

  /* compare present state variables */
  result = VarIdArrayCompare(mddMgr,
                             Fsm_FsmReadPresentStateVars(subFsm1),
                             Fsm_FsmReadPresentStateVars(subFsm2));
  if (!result) return FALSE;

  /* compare next state variables */
  result = VarIdArrayCompare(mddMgr,
                             Fsm_FsmReadNextStateVars(subFsm1),
                             Fsm_FsmReadNextStateVars(subFsm2));
  if (!result) return FALSE;

  /* compare input variables */
  result = VarIdArrayCompare(mddMgr,
                             Fsm_FsmReadInputVars(subFsm1),
                             Fsm_FsmReadInputVars(subFsm2));
  if (!result) return FALSE;

  /* compare the pseudo input variables */
  result = VarIdArrayCompare(mddMgr,
                             Fsm_FsmReadPseudoInputVars(subFsm1),
                             Fsm_FsmReadPseudoInputVars(subFsm2));
  if (!result) return FALSE;

  /* compare next state functions */
  result = NSFunctionNamesCompare(mddMgr,
                                  Fsm_FsmReadNextStateFunctionNames(subFsm1),
                                  Fsm_FsmReadNextStateFunctionNames(subFsm2));
  if (!result) return FALSE;

  return TRUE;
}

Fsm_RchStatus_t
Fsm_FsmReadReachabilityApproxComputationStatus(Fsm_Fsm_t *fsm)
{
  return fsm->reachabilityInfo.rchStatus;
}

void
Fsm_MinimizeTransitionRelationWithReachabilityInfo(
  Fsm_Fsm_t *fsm,
  Img_DirectionType fwdbwd,
  boolean verbosity)
{
  Img_ImageInfo_t *imageInfo;
  array_t *minimizeArray = NIL(array_t);
  boolean fwd            = FALSE;
  boolean bwd            = FALSE;
  int     oldVerbosity;
  Fsm_RchStatus_t status;
  boolean  freeArray;
  mdd_t *exactrdc;
  
  switch (fwdbwd) {
  case Img_Forward_c:
    fwd = 1;
    break;
  case Img_Backward_c:
    bwd = 1;
    break;
  case Img_Both_c:
    fwd = 1;
    bwd= 1;
    break;
  default:
    assert(0);
    break;
  }
  
  imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, bwd, fwd);
  oldVerbosity = Img_ReadPrintMinimizeStatus(imageInfo);
  
  status = Fsm_FsmReadReachabilityApproxComputationStatus(fsm);
  exactrdc = Fsm_FsmReadCurrentReachableStates(fsm);
  
  if((status == Fsm_Rch_Exact_c || status == Fsm_Rch_Over_c) &&
     exactrdc != NIL(mdd_t) ){
    freeArray = TRUE;
    minimizeArray = array_alloc(mdd_t *, 1);
    array_insert_last(mdd_t *, minimizeArray, mdd_dup(exactrdc)); 
  }else{
    freeArray = FALSE;
    minimizeArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm);
    if(minimizeArray == NIL(array_t))
      return;
  }

  if(verbosity)
    Img_SetPrintMinimizeStatus(imageInfo, 1);

  /* We never reorder the clusters of the iwls structure.  It is probably
     better to reorder them, but as this is written, there is no time to
     evaluate the effect of reordering. */
    Img_MinimizeTransitionRelation(imageInfo, minimizeArray,
                                 Img_DefaultMinimizeMethod_c, fwdbwd, FALSE);
  
  if(verbosity)
    Img_SetPrintMinimizeStatus(imageInfo, oldVerbosity);

  if(freeArray)
    mdd_array_free(minimizeArray);

  return;
}



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

void
FsmSetReachabilityOnionRings(
  Fsm_Fsm_t *fsm, array_t *onionRings)
{
  fsm->reachabilityInfo.onionRings = onionRings;
}

void
FsmSetReachabilityOnionRingsMode(
  Fsm_Fsm_t *fsm, Fsm_RchType_t value)
{
  fsm->reachabilityInfo.onionRingsMode = value;
}

void
FsmSetReachabilityOnionRingsUpToDateFlag(
  Fsm_Fsm_t *fsm,  boolean value)
{
  fsm->reachabilityInfo.onionRingsUpToDate = value;
}

void
FsmSetReachabilityApproxComputationStatus(
  Fsm_Fsm_t *fsm,  Fsm_RchStatus_t value)
{
  fsm->reachabilityInfo.rchStatus = value;
}

void
FsmSetReachabilityOverApproxComputationStatus(
  Fsm_Fsm_t *fsm,  Fsm_Ardc_StatusType_t status)
{
  fsm->reachabilityInfo.overApprox = status;
}

Fsm_Ardc_StatusType_t
FsmReadReachabilityOverApproxComputationStatus(Fsm_Fsm_t *fsm)
{
  return(fsm->reachabilityInfo.overApprox);
}

void
FsmSetReachabilityComputationMode(
  Fsm_Fsm_t *fsm,  Fsm_RchType_t value)
{
  fsm->reachabilityInfo.reachabilityMode = value;
}

Fsm_RchType_t
FsmReadReachabilityComputationMode(
  Fsm_Fsm_t *fsm)
{
  return fsm->reachabilityInfo.reachabilityMode;
}


void
FsmResetReachabilityFields(Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag)
{
  int i;
  mdd_t *reachableStates;
  /* free reachable states if it is necessary to recompute anyway. */
  if (approxFlag != Fsm_Rch_Oa_c) {
    if (Fsm_FsmReadCurrentReachableStates(fsm)) {
      Fsm_FsmFreeReachableStates(fsm);
    }
  } else if (Fsm_FsmReadCurrentOverApproximateReachableStates(fsm)) {
    Fsm_FsmFreeOverApproximateReachableStates(fsm);
  }
        
  /* free onion rings */
  if (Fsm_FsmReadReachabilityOnionRings(fsm) != NIL(array_t)) {
    arrayForEachItem(mdd_t *, Fsm_FsmReadReachabilityOnionRings(fsm), i,
        reachableStates) {
      mdd_free(reachableStates);
    }
    array_free(Fsm_FsmReadReachabilityOnionRings(fsm));
    FsmSetReachabilityOnionRings(fsm, NIL(array_t));
  }
  fsm->reachabilityInfo.depth = 0;
  FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Default_c);
  FsmSetReachabilityApproxComputationStatus(fsm, Fsm_Rch_Under_c);
  FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE);
  FsmSetReachabilityOnionRingsMode(fsm, Fsm_Rch_Default_c);
  return;
} /* end of FsmResetReachabilityFields */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/
FsmHdStruct_t *
FsmHdStructAlloc(int nvars)
{
  FsmHdStruct_t *hdInfo = ALLOC(FsmHdStruct_t, 1);
  if (hdInfo == NIL(FsmHdStruct_t)) return hdInfo;
  hdInfo->numDeadEnds = 0;
  hdInfo->firstSubset = TRUE;
  hdInfo->lastIter = -1;
  hdInfo->partialImage = FALSE;
  hdInfo->residueCount = 0;
  hdInfo->interiorStates = NIL(mdd_t);
  hdInfo->interiorStateCandidate = NIL(mdd_t);
  hdInfo->deadEndResidue = NIL(mdd_t);
  hdInfo->options = Fsm_FsmHdGetTravOptions(nvars);
  hdInfo->stats = FsmHdStatsStructAlloc();
  hdInfo->imageOfReachedComputed = FALSE;
  hdInfo->onlyPartialImage = FALSE;
  hdInfo->slowGrowth = 0;
  hdInfo->deadEndWithOriginalTR = FALSE;
  hdInfo->deadEndComputation = FALSE;
  return hdInfo;
}


void
FsmHdStructFree(FsmHdStruct_t *hdInfo)
{
  if (hdInfo->interiorStates != NULL) mdd_free(hdInfo->interiorStates);
  if (hdInfo->interiorStateCandidate != NULL)
    mdd_free(hdInfo->interiorStateCandidate);
  if (hdInfo->deadEndResidue != NULL) mdd_free(hdInfo->deadEndResidue);
  
  FsmHdStatsStructFree(hdInfo->stats);
  Fsm_FsmHdFreeTravOptions(hdInfo->options);
  FREE(hdInfo);
  return;
}

void
FsmGuidedSearchPrintOptions(void)
{
  char *string =  Cmd_FlagReadByName("guided_search_hint_type");
  if (string == NIL(char)) string = "local";
  fprintf(vis_stdout, "Flag guided_search_hint_type is set to %s.\n", string);
  string = Cmd_FlagReadByName("guided_search_underapprox_minimize_method");
  if (string == NIL(char)) string = "and";
  fprintf(vis_stdout, "Flag guided_search_underapprox_minimize_method is set to %s.\n", string);
  string = Cmd_FlagReadByName("guided_search_overapprox_minimize_method");
  if (string == NIL(char)) string = "ornot";
  fprintf(vis_stdout, "Flag guided_search_overapprox_minimize_method is set to %s.\n", string);
  string = Cmd_FlagReadByName("guided_search_sequence");
  if (string == NIL(char)) string = "all hints to convergence";
  fprintf(vis_stdout, "Flag guided_search_overapprox_minimize_method is set to %s.\n", string);
  return;
}



/*---------------------------------------------------------------------------*/
/* Definition of static functions                                          */
/*---------------------------------------------------------------------------*/
static Fsm_Fsm_t *
FsmStructAlloc(Ntk_Network_t *network,
            graph_t     *partition)
{
  Fsm_Fsm_t *fsm;
  if (Ntk_NetworkReadNumLatches(network) == 0) {
    error_append("Network has no latches. Cannot create FSM.");
    return (NIL(Fsm_Fsm_t));
  }
  
  fsm = ALLOC(Fsm_Fsm_t, 1);
  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t);
  memset(fsm, 0, sizeof(Fsm_Fsm_t));

  fsm->network = network;

  if (partition == NIL(graph_t)) {
    partition = Part_NetworkReadPartition(network);

    if (partition == NIL(graph_t)) {
      error_append("Network has no partition. Cannot create FSM.");
      return (NIL(Fsm_Fsm_t));
    } else {
      fsm->partition = Part_PartitionDuplicate(partition);
    }
  } else {
    fsm->partition = partition;
  }
  
  FsmSetReachabilityOnionRings(fsm, NIL(array_t));
  FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE);
  FsmSetReachabilityOnionRingsMode(fsm, Fsm_Rch_Default_c);
  FsmSetReachabilityApproxComputationStatus(fsm, Fsm_Rch_Under_c);
  FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Default_c);
  FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c);

  fsm->fsmData.presentStateVars   = array_alloc(int, 0);
  fsm->fsmData.nextStateVars      = array_alloc(int, 0);
  fsm->fsmData.inputVars          = array_alloc(int, 0);
  fsm->fsmData.nextStateFunctions = array_alloc(char *, 0);

  return (fsm);
} /* end of FsmStructAlloc */


static void
FsmCreateVariableCubes(Fsm_Fsm_t *fsm)
{
  mdd_manager *manager = Fsm_FsmReadMddManager(fsm);
  char *flagValue;
  boolean createVariableCubesFlag = TRUE;

  if (bdd_get_package_name() != CUDD)
    return;

  flagValue = Cmd_FlagReadByName("fsm_create_var_cubes");
  if (flagValue != NIL(char)) {
    if (strcmp(flagValue, "yes") == 0)
      createVariableCubesFlag = TRUE;
    else if (strcmp(flagValue, "no") == 0)
      createVariableCubesFlag = FALSE;
    else {
      fprintf(vis_stderr,
        "** ardc error : invalid value %s for create_var_cubes[yes/no]. **\n",
        flagValue);
    }
  }

  if (!createVariableCubesFlag)
    return;

  fsm->fsmData.createVarCubesFlag = TRUE;
  fsm->fsmData.presentStateCube =
        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.presentStateVars);
  fsm->fsmData.nextStateCube =
        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.nextStateVars);
  fsm->fsmData.inputCube =
        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.inputVars);
  if (fsm->fsmData.pseudoInputVars) {
    fsm->fsmData.pseudoInputCube =
        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.pseudoInputVars);
  }
  if (fsm->fsmData.primaryInputVars) {
    fsm->fsmData.primaryInputCube =
        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.primaryInputVars);
  }
  if (fsm->fsmData.globalPsVars) {
    fsm->fsmData.globalPsCube =
        mdd_id_array_to_bdd_cube(manager, fsm->fsmData.globalPsVars);
  }
}


static int
nameCompare(
  const void * name1,
  const void * name2)
{
    return(strcmp(*(char **)name1, *(char **)name2));

} /* end of signatureCompare */


static boolean
VarIdArrayCompare(mdd_manager *mddMgr,
                  array_t *vars1,
                  array_t *vars2)
{
  
  mdd_t *cube1, *cube2;
  boolean result = FALSE;
  cube1 = bdd_compute_cube(mddMgr, vars1);
  cube2 = bdd_compute_cube(mddMgr, vars2);
  if ((cube1 == NIL(mdd_t)) || (cube2 == NIL(mdd_t))) {
    result = (cube1 == cube2) ? TRUE : FALSE;
  } else {
    result =  bdd_equal(cube1, cube2) ? TRUE : FALSE;
  }
  if (cube1 != NIL(bdd_t)) bdd_free(cube1);
  if (cube2 != NIL(bdd_t)) bdd_free(cube2);
  return result;
} /* end of VarIdArrayCompare */


static boolean
NSFunctionNamesCompare(mdd_manager *mddMgr,
                       array_t *names1,
                       array_t *names2)
{
  int sizeArray = array_n(names1);
  int i, count;
  char *name;
  st_table *nameTable = st_init_table(strcmp, st_strhash);

  if (sizeArray != array_n(names2)) return FALSE;
  /* check if elements in names2 is in names1 */
  arrayForEachItem(char *, names1, i, name) {
    if (st_lookup_int(nameTable, name, &count)) {
      count++;
    } else {
      count = 1;
    }
    st_insert(nameTable, name, (char *)(long)count);
  }
  
  arrayForEachItem(char *, names2, i, name) {
    if (!st_lookup_int(nameTable, name, &count)) {
      st_free_table(nameTable);
      return FALSE;
    } else if (count == 0) { 
      st_free_table(nameTable);
      return FALSE;
    } else {
      count--;
      st_insert(nameTable, name, (char *)(long)count);   
    }
  }
  st_free_table(nameTable);

  /* check if elements in names1 is in names2 */
  nameTable = st_init_table(strcmp, st_strhash);
  arrayForEachItem(char *, names2, i, name) {
    if (st_lookup_int(nameTable, name, &count)) {
      count++;
    } else {
      count = 1;
    }
    st_insert(nameTable, name, (char *)(long)count);
  }
  
  arrayForEachItem(char *, names1, i, name) {
    if (!st_lookup_int(nameTable, name, &count)) {
      st_free_table(nameTable);
      return FALSE;
    } else if (count == 0) { 
      st_free_table(nameTable);
      return FALSE;
    } else {
      count--;
      st_insert(nameTable, name, (char *)(long)count);   
    }
  }
  st_free_table(nameTable);
  return TRUE;
} /* end of NSFunctionNamesCompare */


static array_t *
GetMddSupportIdArray(Fsm_Fsm_t *fsm, st_table *mddIdTable,
                     st_table *pseudoMddIdTable)
{
  mdd_t                 *func;
  char                  *nodeName;
  vertex_t              *vertex;
  Mvf_Function_t        *mvf;
  int                   i, j, k;
  long                  mddId;
  array_t               *varBddFunctionArray;
  mdd_manager           *mddManager;
  array_t               *supportMddIdArray, *support;
  st_table              *supportMddIdTable;
  st_generator          *stGen;

  supportMddIdTable = st_init_table(st_numcmp, st_numhash);
  mddManager = Part_PartitionReadMddManager(fsm->partition);

  for (i = 0; i < array_n(fsm->fsmData.nextStateFunctions); i++) {
    nodeName = array_fetch(char*, fsm->fsmData.nextStateFunctions, i);
    vertex = Part_PartitionFindVertexByName(fsm->partition, nodeName);
    mvf = Part_VertexReadFunction(vertex);
    mddId = (long) array_fetch(int, fsm->fsmData.nextStateVars, i);
    varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager,
                                                       (int) mddId, mvf);

    for (j = 0; j < array_n(varBddFunctionArray); j++) {
      func = array_fetch(mdd_t *, varBddFunctionArray, j);
      support = mdd_get_support(mddManager, func);
      arrayForEachItem(int, support, k, mddId) {
        if (!st_lookup(supportMddIdTable, (char *)mddId, NIL(char *))) {
          if (st_lookup(mddIdTable, (char *)mddId, NIL(char *)) ||
              st_lookup(pseudoMddIdTable, (char *)mddId, NIL(char *))) {
            st_insert(supportMddIdTable, (char *)mddId, NIL(char));
          } else { /* intermediate variables */
            /* NEEDS to get the supports of an intermediate variable */
            assert(0);
          }
        }
      }
    }
    array_free(varBddFunctionArray);
  }

  supportMddIdArray = array_alloc(int, 0);
  st_foreach_item(supportMddIdTable, stGen, &mddId, NIL(char *)) {
    array_insert_last(int, supportMddIdArray, (int) mddId);
  }

  return(supportMddIdArray);
}