source: vis_dev/vis-2.3/src/fsm/fsmFsm.c @ 50

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

  FileName    [fsmFsm.c]

  PackageName [fsm]

  Synopsis    [Routines to create and manipulate the FSM structure.]

  Author      [Shaker Sarwary, Tom Shiple, Rajeev Ranjan, 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 "fsmInt.h"

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

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

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

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


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

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

  Synopsis    [Creates an FSM from a network.]

  Description [Creates an FSM from a network and a partition. The FSM is
  initialized to the single fairness constraint TRUE, indicating that all
  states are "accepting". Reachability information, fair states, and
  imageInfo, are initialized to NIL, since these items are computed on
  demand. If the network has no latches, then NULL is returned and a message
  is written to error_string.<p>

  The partition gives the MVFs defining the next state functions of the
  network.  If the partition is NULL, then a duplicate of the default
  partition of the network (found using Part_NetworkReadPartition) is used.
  If the network has no default partition, then NULL is returned and a message
  is written to error_string.  Having the partition as a parameter gives the
  calling application the flexibility of using a different partition from the
  default, possibly one representing different functions than those given by
  the network (say for the purpose of computing approximations).  However, it
  is assumed (though not checked), that the partition has the same
  combinational input variables and next state function names as the network.
  Finally, note that the given partition will be freed when the FSM is freed.]

  SideEffects []

  SeeAlso     [Fsm_FsmFree]

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



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

  Synopsis    [Creates a FSM given the set of latches and the inputs.]

  Description [This function is primarily used to create a "reduced"
  FSM specific to a particular property during model checking. The
  given array of latches and inputs are associated with the FSM. If
  partition is NIL, the default partition from network is
  obtained. This partition will be used to obtain the next state
  functions of the latches. The last argument is an arry of fairness
  constraints which is used to restrict the reduced fsm to fair
  paths. </p>
  For a detailed desription of various fields of FSM, please refer to
  the function Fsm_FsmCreateFromNetworkWithPartition.]

  SideEffects []

  SeeAlso     [Fsm_FsmFree Fsm_FsmCreateFromNetworkWithPartition]

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

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

  Synopsis    [Creates a FSM given the set of latches and the inputs.]

  Description [This function is primarily used to create an "abstract"
  FSM specific to a particular property during invariant checking with
  abstraction refinement method Grab. The given array of latches and
  inputs are associated with the FSM. the array of invisible latches
  can be treated either as inputs (independentFlag==TRUE), or as
  latches (independentFlag==FALSE). It is the user's responsibility to
  make sure that latches, invisibleVars, and inputs are mutually
  disjoint. 

  When independentFlag==TRUE, the FSM is defined by the pair
  (fsmData.presentStateVars, fsmData.inputVars); when
  independentFlag==FALSE, the FSM is defined by the pair
  (fsmData.globalPsVars, fsmData.primaryInputVars). For more
  information, please check the function
  Fsm_FsmReadOrCreateImageInfo(). The two pairs are defined as
  follows:

                presentStateVars inputVars  globalPsVars primaryInputVars
  ----------------------------------------------------------------------- 
  absLatches   |        X                        X
  invisibleVars|                     X           X
  inputs       |                     X                          X  
  -----------------------------------------------------------------------

  If partition is NIL, the default partition from network is
  obtained. This partition will be used to obtain the next state
  functions of the latches. The last argument is an arry of fairness
  constraints which is used to restrict the reduced fsm to fair
  paths. </p> For a detailed desription of various fields of FSM,
  please refer to the function Fsm_FsmCreateFromNetworkWithPartition.]

  SideEffects []

  SeeAlso     [Fsm_FsmFree Fsm_FsmCreateReducedFsm]

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


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

  Synopsis    [Frees the memory associated with an FSM.]

  Description [Frees the memory associated with an FSM. In particular, frees
  all the MDDs, and frees the associated partition.  The FSM's corresponding
  network is not modified in any way.]

  SideEffects []

  SeeAlso     [Fsm_FsmCreateFromNetwork]

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

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

  Synopsis    [Frees the memory associated with an FSM.]

  Description [Identical to Fsm_FsmFree() but does not free the partition.]

  SideEffects []

  SeeAlso     [Fsm_FsmCreateSubsystemFromNetwork]

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

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

  Synopsis    [Callback function to free an FSM.]

  Description [Typecasts data to (Fsm_Fsm_t *) and then calls Fsm_FsmFree.
  This function should only be used as a callback for other applications that
  don't know the FSM type, for example the network ApplInfoTable.]

  SideEffects []

  SeeAlso     [Fsm_FsmFree]

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


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

  Synopsis    [Returns the corresponding network of an FSM.]

  SideEffects []

  SeeAlso     [Fsm_FsmCreateFromNetwork]

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

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

  Synopsis    [Read UnquantifiedFlag of an FSM.]

  Description [This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

  SeeAlso     [Fsm_FsmCreateFromNetwork]

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

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

  Synopsis    [Returns the MDD manager of the corresponding network of an FSM.]

  SideEffects []

  SeeAlso     [Fsm_FsmCreateFromNetwork]

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


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

  Synopsis    [Returns the FSM of a network; creates FSM if necessary.]

  Description [If there is an FSM associated with network, then returns it.
  Otherwise, creates an FSM from network (using a duplicate of the partition
  associated with the network), registers the FSM with the network, and then
  returns the newly created FSM.  Note that if the network has no latches or
  the network has no partition, then a NULL FSM is returned.]

  SideEffects []

  SeeAlso     [Fsm_FsmCreateFromNetwork Ntk_NetworkReadApplInfo
  Fsm_NetworkReadFsm]

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


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

  Synopsis    [Returns the FSM of a network.]

  Description [Returns the FSM of a network, which may be NULL.]

  SideEffects []

  SeeAlso     [Fsm_FsmCreateFromNetwork Ntk_NetworkReadApplInfo
  Fsm_NetworkReadOrCreateFsm]

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


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

  Synopsis    [Returns the imageInfo struct stored by the FSM.]

  Description [Returns the imageInfo struct stored by the FSM, which may be
  NULL.]

  SideEffects []

  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadOrCreateImageInfo]

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

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

  Synopsis    [Set the imageInfo.]

  Description [Set the imageInfo. ] 

  SideEffects []

  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadOrCreateImageInfo]

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

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

  Synopsis    [Returns the imageInfo struct stored by the FSM.]

  Description [Returns the imageInfo struct stored by the FSM, which may be
  NULL.]

  SideEffects []

  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadOrCreateImageInfo]

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

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

  Synopsis    [Returns the partition associated with the FSM.]

  Description [Returns the partition associated with the FSM.  This is the
  graph of MVFs defining the combinational output functions of the FSM.]

  SideEffects []

  SeeAlso     [Fsm_FsmCreateFromNetwork]

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

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

  Synopsis    [Test if reachability has been performed on the FSM.]

  Description [Return TRUE if reachability has already been performed, else FALSE.]

  SideEffects []

  SeeAlso     [Fsm_FsmComputeReachableStates]

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

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

  Synopsis    [Test if approximate reachability has been performed on the FSM.]

  Description [Return TRUE if approximate reachability has already been
  performed, else FALSE.]

  SideEffects []

  SeeAlso     [Fsm_FsmComputeReachableStates]

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


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

  Synopsis    [Returns the reachable states of an FSM.]

  SideEffects [Returns the reachable states of an FSM.]

  SeeAlso     [Fsm_FsmComputeReachableStates]

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


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

  Synopsis    [Returns the reachable states of an FSM.]

  SideEffects [Returns the reachable states of an FSM. May be an under
  approximation or an over approximation.]

  SeeAlso     [Fsm_FsmComputeReachableStates]

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


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

  Synopsis    [Returns the approximate reachable states of an FSM.]

  SideEffects []

  SeeAlso     [Fsm_ArdcComputeOverApproximateReachableStates]

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


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

  Synopsis    [Returns the current approximate reachable states of an FSM.]

  SideEffects []

  SeeAlso     [Fsm_ArdcComputeOverApproximateReachableStates]

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

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

  Synopsis    [Return array of onion rings from reachability computation]

  Description [Return array of onion rings from reachability
  computation; NIL if reachability has not been performed. DO NOT free
  this array.]

  SideEffects []

  SeeAlso     [Fsm_FsmComputeReachableStates]

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

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

  Synopsis [Checks whether the onion rings are consistent with the
  reachable states.]

  Description [Checks whether the onion rings are consistent with the
  reachable states. Returns FALSE if no states in onion
  rings.]

  SideEffects [result is set to the union of the onion rings]

  SeeAlso     [Fsm_FsmbtainBFSShells]

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

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

  Synopsis    [Checks if the onion rings are consistent with the
  reachable states.]

  Description [Checks if the onion rings are consistent with the
  reachable states.]

  SideEffects []

  SeeAlso     [Fsm_FsmComputeReachableStates]

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

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

  Synopsis    [Checks if the onion rings are due to BFS or not.]

  Description [Checks if the onion rings are due to BFS or not.]

  SideEffects []

  SeeAlso     [Fsm_FsmComputeReachableStates]

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

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

  Synopsis    [Returns the imageInfo struct stored by the FSM; creates if
  necessary.]

  Description [Returns the imageInfo struct stored by the FSM.  If one doesn't
  currently exist in the FSM, then one is initialized and set, before it is
  returned.  The imageInfo is initialized using the default image method, and
  is initialized for both forward and backward image computations. It uses the
  partition with which this FSM was created when the function
  Fsm_FsmCreateFromNetwork was called.]

  SideEffects []

  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadImageInfo]

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

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

  Synopsis    [Returns the imageInfo struct stored by the FSM; creates if
  necessary.]

  Description [Returns the imageInfo struct stored by the FSM.  If one doesn't
  currently exist in the FSM, then one is initialized and set, before it is
  returned.  The imageInfo is initialized using the default image method, and
  is initialized for both forward and backward image computations. It uses the
  partition with which this FSM was created when the function
  Fsm_FsmCreateFromNetwork was called. In this function we create the ImageInfo 
  that has no quntified input for Fate and Free will.]

  SideEffects []

  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadImageInfo]

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

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

  Synopsis    [Returns the imageInfo struct stored by the FSM; creates if
  necessary.]

  Description [Returns the imageInfo struct stored by the FSM.  If one doesn't
  currently exist in the FSM, then one is initialized and set, before it is
  returned.  The imageInfo is initialized using the default image method, and
  is initialized for both forward and backward image computations. It uses the
  partition with which this FSM was created when the function
  Fsm_FsmCreateFromNetwork was called. In this function we create the ImageInfo 
  that has no quntified input for Fate and Free will.]

  SideEffects []

  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadImageInfo]

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


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

  Synopsis    [Returns the imageInfo struct stored by the FSM; creates if
  necessary.]

  Description [Returns the imageInfo struct stored by the FSM.  If one doesn't
  currently exist in the FSM, then one is initialized and set, before it is
  returned.  The imageInfo is initialized using the default image method, and
  is initialized for both forward and backward image computations. It uses the
  partition with which this FSM was created when the function
  Fsm_FsmCreateFromNetwork was called. In this function we create the ImageInfo 
  that has no quntified input for Fate and Free will.]

  SideEffects []

  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadImageInfo]

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

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

  Synopsis [Computes the set of initial states of an FSM.]

  Description [Computes the set of initial states of an FSM.  If this set
  has already been computed, then just returns the result of the previous
  computation.  The calling application is responsible for freeing the
  returned MDD in all cases.<p>

  The nodes driving the initial inputs of the latches, called the initial
  nodes, must not have latches in their support.  If an initial node is found
  that has a latch in its transitive fanin, then a NULL MDD is returned, and a
  message is written to the error_string.<p>
  
  The initial states are computed as follows. For each latch i, the relation
  (x_i = g_i(u)) is built, where x_i is the present state variable of latch i,
  and g_i(u) is the multi-valued initialization function of latch i, in terms
  of the input variables u.  These relations are then conjuncted, and the
  input variables are existentially quantified from the result
  (i.e. init_states(x) = \exists u \[\prod (x_i = g_i(u))\]).]

  SideEffects [The result of the initial state computation is stored with
  the FSM.]

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



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

  Synopsis [Returns the array of MDD ids of the present state variables of an
  FSM.]

  Description [Returns the array of MDD ids of the present state variables of
  an FSM.  This array should not be modified or freed in any way.]

  SideEffects []

  SeeAlso [Fsm_FsmReadNextStateVars Fsm_FsmReadInputVars
  Fsm_FsmReadNextStateFunctionNames]

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

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

  Synopsis [Returns the array of MDD ids of the next state variables of an
  FSM.]

  Description [Returns the array of MDD ids of the next state variables of
  an FSM.  This array should not be modified or freed in any way.]

  SideEffects []

  SeeAlso [Fsm_FsmReadPresentStateVars Fsm_FsmReadInputVars
  Fsm_FsmReadNextStateFunctionNames]

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

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

  Synopsis [Returns an array of strings containing the names of the nodes
  driving the data inputs of the latches.]

  Description [Returns the array of strings containing the names of the nodes
  driving the data inputs of the latches. This array should not be modified or
  freed in any way.]

  SideEffects []

  SeeAlso [Fsm_FsmReadPresentStateVars Fsm_FsmReadNextStateVars
  Fsm_FsmReadInputVars]

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

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

  Synopsis [Returns the array of MDD ids of the input variables of an
  FSM.]

  Description [Returns the array of MDD ids of the input variables of an FSM.
  This includes both primary inputs and pseudo inputs. This array should not
  be modified or freed in any way.]

  SideEffects []

  SeeAlso [Fsm_FsmReadPresentStateVars Fsm_FsmReadNextStateVars
  Fsm_FsmReadNextStateFunctionNames]

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

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


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

  Synopsis [Returns the array of MDD ids of the pseudo input variables
  of a sub FSM.]

  Description [Returns the array of MDD ids of the pseudo input variables
  of a sub FSM.  This array should not be modified or freed in any way.]

  SideEffects []

  SeeAlso [Fsm_FsmReadNextStateVars Fsm_FsmReadInputVars
  Fsm_FsmReadNextStateFunctionNames]

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

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

  Synopsis [Set input variables into the FSM structure.]

  Description []

  SideEffects []

  SeeAlso     []

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

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

  Synopsis [Set useUnquantifiedFlag into the FSM structure.]

  Description [This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis [Set the initial states of an FSM.]

  Description []

  SideEffects [Old mdd_t representing the initial states is deleted and
  replaced by the argument provided.]

  SeeAlso     []

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

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

  Synopsis [Read FAFWFlag from the FSM structure.]

  Description [This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis [Set FAFWFlag in the FSM structure.]

  Description [This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis [Set input variables that are controlled by system and environment 
            in the FSM structure.]

  Description [This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis [Read input variables that is controlled by environment
            in the FSM structure.]

  Description [This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis [Read input variables that is controlled by system
            in the FSM structure.]

  Description [This is function for FateAndFreeWill counterexample generation.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Returns the current FSM of a hierarchy manager.]

  Description [Returns the FSM of the network of the current node of a
  hierarchy manager. If the 1) hmgr is NULL, 2) current node is NULL, 3)
  network is NULL, 4) the variables of the network have not been ordered, 5) a
  partition doesn't exist for the network, or 6) the network does not have any
  latches, then a message is printed to vis_stderr, and NULL is returned.  If
  all the above conditions have been satisfied, and the network doesn't
  already have an FSM, then one is created.]

  SideEffects []

  SeeAlso     [Hrc_ManagerReadCurrentNode Ntk_HrcManagerReadCurrentNetwork
  Fsm_NetworkReadOrCreateFsm]

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

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

  Synopsis    [Creates a subFSM from a network.]

  Description [Given a vertex table, the routine creates a subFSM. The routine
  reads in the vertex table  and stores only corresponding next state functions 
  into the subFSM. Every present, next state and input variables in the system
  are stored into the subFSM.
  ]

  SideEffects []

  SeeAlso     [Fsm_FsmCreateFromNetworkWithPartition, Fsm_FsmFree]

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

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

  Synopsis [Instantiate a given hint]

  Description [Instantiate a given hint. The fwd and bwd flags
  indicate whether the fwd transition relation or the backward
  transition relation is created. A non-zero value will cause the hint
  to be instantiated in that direction.  The type flag indicates
  whether the hint should be applied as an overapproximation or an
  underapproximation.

  After minimization wrt the hint is done, the TR is minimized wrt the
  conjunction of the care states in careStatesArray (an array of mdd_t *),
  unless this array is NULL, in which case it is ignored.]

  SideEffects []

  SeeAlso [Fsm_CleanUpHints]

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

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

  Synopsis [Clean up after hints]

  Description [Clean up after hints.]

  SideEffects []

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


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

  Synopsis    [Frees the reachable states of an FSM.]

  Description [Frees the reachable states of an FSM.]

  SideEffects []

  SeeAlso     [Fsm_FsmFree, Fsm_FsmFreeOverApproximateReachableStates]

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

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

  Synopsis    [Frees the approximate reachable states of an FSM.]

  Description [Frees the approximate reachable states of an FSM.]

  SideEffects []

  SeeAlso     [Fsm_FsmFree, Fsm_FsmFreeReachableStates]

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


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

  Synopsis    [Returns the reachable depth of an FSM.]

  Description [Returns the reachable depth of an FSM.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis [Checks if the 2 given fsms are the same, given that they
  are from the same total fsm. ]

  Description [Checks if the 2 given fsms are the same, given that
  they are from the same total fsm. Compares present, next state,
  input, real present state and abstract variables. Also compares the
  next state function NAMES ONLY. Since the 2 fsms are guaranteed to
  be parts of te same total fsm and they share the same network, the
  mdds of next state function nodes with the same name are guaranteed
  to be the same. ]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Returns whether reachability analysis was an approximation or 
  exact.]

  Description [Returns whether reachability analysis was an approximation or
  exact.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Minimize the transition relation wrt either ARDCs or exact
  reachability information]

  Description [Prefers exact rdcs when available, if neither exact nor
  approximate rdcs are availablem, the TR is not touched.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Sets array of onion rings from reachability computation]

  Description [Sets array of onion rings from reachability
  computation.]

  SideEffects []

  SeeAlso     [Fsm_FsmReadReachabilityOnionRings]

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

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

  Synopsis    [Sets whether  onion rings are due to BFS.]

  Description [Sets whether onion rings are due to BFS.]

  SideEffects []

  SeeAlso     [Fsm_FsmReadReachabilityOnionRingsMode]

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

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

  Synopsis    [Sets whether  onion rings are up to date.]

  Description [Sets whether  onion rings are up to date.]

  SideEffects []

  SeeAlso     [Fsm_FsmReachabilityOnionRingsUpToDate]

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

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

  Synopsis    [Sets whether reachability analysis was an approximation.]

  Description [Sets whether reachability analysis was an approximation.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Sets the status of overapproxiate reachable computation.]

  Description [Sets the status of overapproxiate reachable computation.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Reads the status of overapproxiate reachable computation.]

  Description [Reads the status of overapproxiate reachable computation.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis [Sets the mode field to indicate whether computation has
  always been BFS.]

  Description [Sets the mode field to indicate whether computation has
  always been BFS.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis [Reads the mode field to indicate whether computation has
  always been BFS.]

  Description [Reads the mode field to indicate whether computation has
  always been BFS.]

  SideEffects []

  SeeAlso     []

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


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

  Synopsis [Reset fsm fields]

  Description [Reset fsm fields. Free reachable states, onion rings.
  Reset the onion ring up-to-date flag, onion rings BFS, depth and
  under approximation flag.]

  SideEffects []

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

  Synopsis    [Allocates HD Info structure.]

  Description [Allocates HD Info structure.]

  SideEffects []

  SeeAlso     [Fsm_FsmHdStructFree]

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


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

  Synopsis    [Frees HD info struct.]

  Description [Frees HD info struct.]

  SideEffects []

  SeeAlso     [Fsm_FsmHdStructAllocate]

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

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

  Synopsis    [Prints all options that are related to guided search.]

  Description [Prints all options that are related to guided search.]

  SideEffects []

  SeeAlso     [CommandGuidedSearchOptions]

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

  Synopsis    [Allocates structure]

  Description [Allocates structure]

  SideEffects []

  SeeAlso     []

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


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

  Synopsis    [Allocates structure]

  Description [Allocates structure]

  SideEffects []

  SeeAlso     []

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


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

  Synopsis    [Compare procedure for name comparison.]

  Description [Compare procedure for name comparison.]

  SideEffects []

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

} /* end of signatureCompare */


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

  Synopsis    [ Checks that 2 arrays of variables ids are the same.]

  Description [ Checks that 2 arrays of variables ids are the same by
  computing the bdd of the cube.]
 
  SideEffects []

  SeeAlso     [Fsm_FsmCheckSameSubFsmInTotalFsm]

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


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

  Synopsis    [ Checks that 2 arrays of variables ids are the same.]

  Description [ Checks that 2 arrays of variables ids are the same by
  computing the bdd of the cube.]
 
  SideEffects []

  SeeAlso     [Fsm_FsmCheckSameSubFsmInTotalFsm]

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


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

  Synopsis    [Returns an array of mdd Ids of an FSM.]

  Description [Returns an array of mdd Ids of an FSM.]
 
  SideEffects []

  SeeAlso     []

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