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

  FileName    [amcAmc.c]

  PackageName [amc]

  Synopsis    [Approximate Model Checker.]

  Author      [Woohyuk Lee <woohyuk@duke.colorado.edu>]

  Copyright [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

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

#include "amcInt.h" 
#include "mcInt.h" 

static char rcsid[] UNUSED = "$Id: amcAmc.c,v 1.57 2005/04/16 04:22:41 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


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


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

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
static int stringCompare(const void *s1, const void *s2);

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


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

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

  Synopsis [Evaluate formula with approximations.]

  Description [Starting from an initial coarse approximation, find an 
  approximation that produces reliable result. The degree of approximation
  is determined by the number of vertices contained in a subsystem. The initial
  number of vertices in a subsystem is set by "amc_sizeof_group" environment.
  The algorithm searches a virtual lattice of approximations in which the
  level of the lattice is defined as the degree of approximations. Once the
  approximations in a certain level fails to prove the formula, the algorithm
  automatically refines the approximation by combining(taking the synchronous
  product) of subsystems. It repeats the process until the approximation is
  refined enough to produce a reliable result. The procedure may also be
  viewed as finding a pseudo-optimal path starting from the coarse 
  approximations(in level 1 of the lattice of approximations) to the
  approximations that produce reliable result. One can draw a virtual contour
  separating the approximations that produce faulty results and the reliable
  results. We call this virtual placement of the approximations and the
  contour separting the two regions, a lattice of approximations.
  The algorithms are dual. Each algorithm makes its effort to prove whether the
  formula is positive or negative respectively. When proving true positive of
  given ACTL formula we use over-approximation  of the transition relation,
  and to prove true negative, we use under-approximation of the transition
  relation.]


  SideEffects []

  SeeAlso []
  
******************************************************************************/
void
Amc_AmcEvaluateFormula(
  Ntk_Network_t		*network,
  Ctlp_Formula_t	*formula,
  int			verbosity)
{
  Amc_Info_t		*amcInfo;
  int			levelOfLattice;
  char			*flagValue;

  long initialTime = 0;
  long finalTime;


  /* 
   * If the partition was not created, get out.  We are assuming we were able to 
   * construct BDD for each combinational outputs.
   */

  graph_t	*partition = Part_NetworkReadPartition(network);
  if (partition == NIL(graph_t)) {
    error_append("** amc error: Network has no partition. Cannot apply approximate model checking.");
    return;
  }


  /*
   * Initialize data structures.
   */
  amcInfo = Amc_AmcInfoInitialize(network, formula, Amc_Default_c, verbosity);



  /* 
   * Check every possible environment variables that user may have set.
   * And give user some assurance by reporting the flag values.
   * Explanation of possible environment variables are discussed in the
   * man page of the package.
   */
  amcInfo->isMBM = 0;

  flagValue = Cmd_FlagReadByName("amc_prove_false");
  if (flagValue == NIL(char)){
    amcInfo->lowerBound = 0;
    fprintf(vis_stdout, "\n#AMC: Proving whether the formula is true.\n");
  }
  else {
    amcInfo->lowerBound = 1;
    fprintf(vis_stdout, "\n#AMC: Proving whether the formula is false.\n");
  }

  if(verbosity) {
    flagValue = Cmd_FlagReadByName("amc_grouping_method");
    if (flagValue == NIL(char)){
      amcInfo->groupingMethod = 0;
      fprintf(vis_stdout, "\n#AMC: No grouping method has been set."); 
    }
    else {
      amcInfo->groupingMethod = 1;
      fprintf(vis_stdout, "\n#AMC: Using latch dependency method for grouping latches into subsystems.");
    }
  }



  /*
   * The lattice of approximation algorithm.
   */

  levelOfLattice = array_n(amcInfo->subSystemArray);
  amcInfo->currentLevel = 1;

  while(levelOfLattice >= amcInfo->currentLevel) {
    if(verbosity) {
      (void)fprintf(vis_stdout, "\n\n##AMC: Entering level %d(%d) of the lattice of approximations\n", 
                                   amcInfo->currentLevel, levelOfLattice);
      fflush(vis_stdout);
    }


    initialTime = util_cpu_time();

    if( (!(*amcInfo->amcBoundProc)(amcInfo, formula, verbosity)) && !(amcInfo->isVerified) ) {

      /* Automatically switches to lattice of lowerbound approximations */
      if(verbosity)
        (void)fprintf(vis_stdout, "Abandoning upper bound approximations.\n");

      /* Free all */
      (*amcInfo->amcFreeProc)(amcInfo);

      amcInfo = Amc_AmcInfoInitialize(network, formula, Amc_Default_c, verbosity);
      amcInfo->lowerBound = TRUE;
      amcInfo->currentLevel = 0;

    }
    else if(amcInfo->isVerified) {
      finalTime = util_cpu_time();
      if(verbosity == Amc_VerbosityVomit_c) {
        (void) fprintf(vis_stdout, "\n%-20s%10ld\n", "analysis time =", 
                                    (finalTime - initialTime) / 1000);
      }

      if(amcInfo->amcAnswer == Amc_Verified_True_c) {
        (void) fprintf(vis_stdout, "\n# AMC: Verified formula TRUE at level %d of %d : ",
		       amcInfo->currentLevel, levelOfLattice);
      }else if(amcInfo->amcAnswer == Amc_Verified_False_c) {
        (void) fprintf(vis_stdout, "\n# AMC: Verified formula FALSE at level %d of %d : ",
		       amcInfo->currentLevel, levelOfLattice);
      }else{
	fprintf(vis_stdout, "\n# AMC: formula unknown --- ");
        Ctlp_FormulaPrint( vis_stdout, Ctlp_FormulaReadOriginalFormula( formula ) );
	(void) fprintf(vis_stdout, "\n# AMC: Verified formula UNKNOWN at level %d of %d : ",
		       amcInfo->currentLevel, levelOfLattice);
      }
      (void) fprintf(vis_stdout, "\n# AMC: ");
      Ctlp_FormulaPrint( vis_stdout, Ctlp_FormulaReadOriginalFormula( formula ) );
      AmcPrintOptimalSystem(vis_stdout, amcInfo);
      (*amcInfo->amcFreeProc)(amcInfo);
      return;
    } /* end of else if(amcInfo->isVerified) */
    
    amcInfo->currentLevel++;
  } /* end of while(levelOfLattice >= amcInfo->currentLevel) */
  
  finalTime = util_cpu_time();
  if(verbosity == Amc_VerbosityVomit_c) {
    (void) fprintf(vis_stdout, "\n%-20s%10ld\n", "analysis time =",
		   (finalTime - initialTime) / 1000);
  }
  
  /*
  ** Now, spec was not verified becase there was an error in computation.
  */ 
  (void) fprintf(vis_stdout, "\n# AMC: The spec was not able to be verified.\n# AMC: ");
  Ctlp_FormulaPrint( vis_stdout, Ctlp_FormulaReadOriginalFormula( formula ) );
  (*amcInfo->amcFreeProc)(amcInfo);
  
}


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

  Synopsis    [Initializes an amcInfo structure for the given method.]

  Description [Regardless of the method type, the initialization procedure
  starts from constructing set of subsystems. A subsystem contains a subset
  of vertices of the partition. Based on the subset of vertices, subFSM is
  created. The subsystems are stored as an array. After the creation of
  the subsystem array, the function initializes remaining field of 
  (Amc_Info_t *) amcInfo.
  The function returns initialized (Amc_Info_t *) amcInfo.]

  SideEffects        []

  SeeAlso     []

******************************************************************************/
Amc_Info_t *
Amc_AmcInfoInitialize(
  Ntk_Network_t		*network,
  Ctlp_Formula_t	*formula,
  Amc_MethodType	methodType,
  int			verbosity)
{
  Amc_Info_t		*amcInfo;
  char			*userSpecifiedMethod;

  amcInfo = ALLOC(Amc_Info_t, 1);
  amcInfo->network = network;

  /*
   * AmcCreateSubsystems creates fsm for each subsystem and returns subSystemArray.
   */
  amcInfo->subSystemArray = AmcCreateSubsystemArray(network, formula);

#ifdef AMC_DEBUG
AmcCheckSupportAndOutputFunctions(amcInfo->subSystemArray);
#endif

  /*
   * Initialize optimalSystem, isVerified; 
   */
  amcInfo->optimalSystem = NIL(Amc_SubsystemInfo_t);
  amcInfo->isVerified = 0;
  amcInfo->amcAnswer = Amc_Verified_Unknown_c;

  /*
   * If methodType is default, use user-specified method.
   */
  if (methodType == Amc_Default_c) {
    userSpecifiedMethod = Cmd_FlagReadByName("amc_method");
    if (userSpecifiedMethod == NIL(char)) {
      methodType = Amc_Block_c;
    }
    else {
      if (strcmp(userSpecifiedMethod, "block") == 0) {
        methodType = Amc_Block_c;
      }
      else if (strcmp(userSpecifiedMethod, "variable") == 0) {
        methodType = Amc_Variable_c;
      }
      else {
        (void) fprintf(vis_stderr, "** amc error: Unrecognized amc_method %s: using Block method.\n",
                       userSpecifiedMethod);
        methodType = Amc_Block_c;
      }
    }
  }
  
  amcInfo->methodType = methodType;


  /* 
   * Every subsystem shares identical initial states. 
   * We do not abstract the state space. Only the transition relation is over or
   * under approximated.
   */
  {
    mdd_t		*sampleInitialStates;
    Amc_SubsystemInfo_t *sampleSystem;

    /* 
     * Fsm routines always returns duplicate copy. 
     */

    sampleSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, 0);
    sampleInitialStates = Fsm_FsmComputeInitialStates(sampleSystem->fsm); 
    amcInfo->initialStates = sampleInitialStates;  
  }


  /* 
   * Fill in the rest of amcInfo according to methodType.
   */
  switch(methodType) {
    case Amc_Block_c:
      amcInfo->methodData = NIL(void);
      amcInfo->amcBoundProc = AmcBlockTearingProc;
      amcInfo->amcFreeProc  = AmcFreeBlock;
      break;
/*
 ;;The variable tearing method has not been implemented yet;;
    case Amc_Variable_c:
      amcInfo->methodData = AmcInfoInitializeVariable(amcInfo);
      amcInfo->amcUpperBoundProc = AmcUpperBoundProcVariable;
      amcInfo->amcLowerBoundProc = AmcLowerBoundProcVariable;
      amcInfo->amcFreeProc = AmcFreeVariable;
      break;
*/
    default:
      fail("Invalid methodtype when initalizing amc method"); 
  }

  amcInfo->currentLevel = 0;

  return(amcInfo);
}


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

  Synopsis    [Apply existential quantification over a subsystem.]

  Description [Given a subsystem, the routine existentially quantify 
  the MDD variables from the transition relation of the subsystem.   
  The return value is the resulting MDD. There are four quantification 
  modes;   
  <dl>
  <dt> Amc_PresentVars_c
  <dd> Existentially quantify present state variables. <p>

  <dt> Amc_NextVars_c
  <dd> Existentially quantify next state variables. <p>
  
  <dt> Amc_InputVars_c
  <dd> Existentially quantify input variables. <p>

  <dt> Amc_User_c
  <dd> Existentially quantify variables provide by the user. In this
       mode user has to provide the array of MDD IDs to the function. If
       the user does not provide the array of MDD IDs, the function just
       returns the transition relation of the subsystem. <p>
  </dl>]

  SideEffects []

  SeeAlso     [Amc_SubsystemInfo, AmcInitializeQuantifyVars]

******************************************************************************/
mdd_t *
Amc_AmcExistentialQuantifySubsystem(
  Amc_SubsystemInfo_t	*subSystem,
  array_t		*quantifyVars,
Amc_QuantificationMode	quantificationMode)
{
  Fsm_Fsm_t	*subSystemFsm	= AmcSubsystemReadFsm(subSystem);	
  Ntk_Network_t *network	= Fsm_FsmReadNetwork(subSystemFsm);
  mdd_manager	*mddManager	= Ntk_NetworkReadMddManager(network);
  graph_t	*partition	= Part_NetworkReadPartition(network);

  mdd_t		*result;

  array_t	*transitionRelationArray = Amc_AmcSubsystemReadRelationArray(subSystem);

  if( transitionRelationArray == NIL(array_t) ) { 
    /* Build the transition relation of this subsystem. */
    st_table	*vertexTable	= AmcSubsystemReadVertexTable(subSystem);
    st_generator		*stGen;
    char			*latchName;

    transitionRelationArray	= array_alloc(mdd_t *, 0);   
    st_foreach_item(vertexTable, stGen, &latchName, NIL(char *)) {

      Ntk_Node_t	*latch		= Ntk_NetworkFindNodeByName(network, latchName);
      int		functionMddId	= Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch));

      char	*nameLatchDataInput	= Ntk_NodeReadName(Ntk_LatchReadDataInput(latch));
      vertex_t	*ptrVertex	= Part_PartitionFindVertexByName(partition, nameLatchDataInput);

      Mvf_Function_t	*nextStateFunction;
      mdd_t         	*transitionRelation;
      nextStateFunction		= Part_VertexReadFunction(ptrVertex);
      transitionRelation	= Mvf_FunctionBuildRelationWithVariable(nextStateFunction,
                                                                functionMddId);
#ifdef AMC_DEBUG
    {
      int y, mddId; array_t *supportOfRelation;
      fprintf(vis_stdout, "\nThe transition relation of the output function of the node : %s", latchName);
      supportOfRelation = mdd_get_support(mddManager, transitionRelation);
      arrayForEachItem(int, supportOfRelation, y, mddId) {
        Ntk_Node_t *supportNode = Ntk_NetworkFindNodeByMddId(network, mddId);
        fprintf(vis_stdout, "\n\tThe node in the support : %s", 
                                       Ntk_NodeReadName(supportNode));
      }
    }
#endif 

      if( nextStateFunction == NIL(Mvf_Function_t) ) {
         error_append("** amc error: Build partition before running approximate model checker.");
         return NIL(mdd_t);
      }

      array_insert_last(mdd_t *, transitionRelationArray, transitionRelation);
    } /* end of st_foreach_item */

    /* Cache the transition relation of the subsystem. */
    Amc_AmcSubsystemSetRelationArray(subSystem, transitionRelationArray);

  } /* end of transition relation construction. */


  /*
   * Notice : The present and next state variable of a subsystem is identical
   * to that of the original system. The subsystem carries the subset of the
   * output functions of the original system.
   */
  if( quantificationMode == Amc_User_c ) {
    /* result = Img_MultiwayLinearAndSmooth(mddManager, transitionRelationArray, quantifyVars,
					 NIL(array_t)); */
    if( AmcSubsystemReadNextStateVarSmoothen(subSystem) == NIL(mdd_t) ) {
      result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, quantifyVars);
      AmcSubsystemSetNextStateVarSmoothen(subSystem, result);
    }
    else {
      result = AmcSubsystemReadNextStateVarSmoothen(subSystem);
    }
  }
  else if( quantificationMode == Amc_PresentVars_c ) {
    array_t	*presentVars	= Fsm_FsmReadPresentStateVars(subSystemFsm);
    result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, presentVars);
  }
  else if( quantificationMode == Amc_NextVars_c ) {
    array_t	*nextVars	= Fsm_FsmReadNextStateVars(subSystemFsm);
    result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, nextVars);
  }
  else if( quantificationMode == Amc_InputVars_c ) {
    array_t	*inputVars	= Fsm_FsmReadInputVars(subSystemFsm);
    result = Fsm_MddMultiwayAndSmooth(mddManager, transitionRelationArray, inputVars);
  }
  else {
    error_append("** amc error: Invalid quantification mode.");
    return NIL(mdd_t);
  }


  return(result);

}

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

  Synopsis    [Apply existential quantification to the array of subsystems.]

  Description [Given an array of subsystems, the routine existentially 
  quantifies the MDD variables from the transition relations of the subsystems.
  The existential quantification is applied to the subsystems that hasn't
  yet been taken into the optimal system. The optimal system is the group 
  of subsystems that has been synchronously combined. 
  There are four quantification modes;
  <dl>
  <dt> Amc_PresentVars_c
  <dd> Existentially quantify present state variables. <p>

  <dt> Amc_NextVars_c
  <dd> Existentially quantify next state variables. <p>
  
  <dt> Amc_InputVars_c
  <dd> Existentially quantify input variables. <p>

  <dt> Amc_User_c
  <dd> Existentially quantify variables provide by the user. In this
       mode user has to provide the array of MDD IDs to the function. If
       the user does not provide the array of MDD IDs, the function just
       returns the transition relation of the subsystem. <p>
  </dl>
  The return value is the array of quantified result of the MDD 
  representation of the transition relation.  ]
  
  SideEffects []

  SeeAlso     [Amc_SubsystemInfo, Amc_AmcExistentialQuantifySubsystem]

******************************************************************************/
array_t *
Amc_AmcExistentialQuantifySubsystemArray(
  array_t			*subSystemArray,
  Amc_SubsystemInfo_t		*currentSystem,
  array_t			*quantifyVars,
  Amc_QuantificationMode	quantificationMode)
{
  int i;
  Amc_SubsystemInfo_t	*subSystem; 
  mdd_t              	*quantifiedSystemMdd;
  array_t		*quantifiedSystemMddArray = array_alloc(mdd_t *, 0);

  if( (quantificationMode == Amc_User_c) && (quantifyVars == NIL(array_t)) ) {
    error_append("** amc error: Subsystem has no output functions.");
    return NIL(array_t);
  }

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
    if( (!subSystem->takenIntoOptimal) && (i != currentSystem->takenIntoOptimal) ) {

      quantifiedSystemMdd =
	Amc_AmcExistentialQuantifySubsystem(subSystem, quantifyVars, 
					    quantificationMode);
      array_insert_last(mdd_t *, quantifiedSystemMddArray, quantifiedSystemMdd);
    }
  }

  return(quantifiedSystemMddArray);

}


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

  Synopsis           [Read the fsm field of a Amc_SubsystemInfo]

  SideEffects        []

  SeeAlso            [Amc_SubsystemInfo]

******************************************************************************/
Fsm_Fsm_t *
Amc_AmcSubsystemReadFsm(
  Amc_SubsystemInfo_t *system)
{
  return AmcSubsystemReadFsm(system);
} /* End of Amc_AmcSubsystemReadFsm */

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

  Synopsis           [Set the fsm field of a Amc_SubsystemInfo]

  SideEffects        []

  SeeAlso            [Amc_SubsystemInfo_t]

******************************************************************************/
void
Amc_AmcSubsystemSetFsm(
  Amc_SubsystemInfo_t *system,
  Fsm_Fsm_t *info)
{
  AmcSubsystemSetFsm(system, info);
} /* End of Amc_AmcSubsystemReadFsm */


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

  Synopsis           [Read the transition relation field of the 
  Amc_SubsystemInfo]

  SideEffects        []

  SeeAlso            [Amc_SubsystemInfo]

******************************************************************************/
array_t *
Amc_AmcSubsystemReadRelationArray(
  Amc_SubsystemInfo_t *system)
{
  return AmcSubsystemReadRelationArray(system);
} /* End of Amc_AmcSubsystemReadTransitionRelation */

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

  Synopsis           [Set the transition relation field of the 
  Amc_SubsystemInfo]

  SideEffects        []

  SeeAlso            [Amc_SubsystemInfo_t]

******************************************************************************/
void
Amc_AmcSubsystemSetRelationArray(
  Amc_SubsystemInfo_t	*system,
  array_t		*info)
{
  AmcSubsystemSetRelationArray(system, info);
} /* End of Amc_AmcSubsystemSetTransitionRelation */


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

  Synopsis           [Read the nextStateVarSmoothen field of the 
  Amc_SubsystemInfo]

  Description 	     [nextStateVarSmoothen field contains the MDD of the 
  transition relation with the next state variable existentially quantified.]

  SideEffects        []

  SeeAlso            [Amc_SubsystemInfo]

******************************************************************************/
mdd_t *
Amc_AmcSubsystemReadNextStateVarSmoothen(
  Amc_SubsystemInfo_t *system)
{
  return AmcSubsystemReadNextStateVarSmoothen(system);
} /* End of Amc_AmcSubsystemReadNextStateVarSmooth */

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

  Synopsis           [Set the nextStateVarSmoothen field of the 
  Amc_SubsystemInfo]

  SideEffects        []

  SeeAlso            [Amc_SubsystemInfo_t]

******************************************************************************/
void
Amc_AmcSubsystemSetNextStateVarSmoothen(
  Amc_SubsystemInfo_t	*system,
  mdd_t			*info)
{
  AmcSubsystemSetNextStateVarSmoothen(system, info);
} /* End of Amc_AmcSubsystemSetNextStateVarSmooth */

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

  Synopsis 	[Read the satisfyStates field of the Amc_SubsystemInfo_t]

  SideEffects   []

  SeeAlso       [Amc_SubsystemInfo_t]

******************************************************************************/
mdd_t *
Amc_AmcSubsystemReadSatisfy(
  Amc_SubsystemInfo_t *system)
{
  return AmcSubsystemReadSatisfy(system);
} /* End of Amc_AmcSubsystemReadSatisfy */

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

  Synopsis 	[Set the satisfyStates field of Amc_SubsystemInfo_t ]

  Description   [satisfyStates field contains the MDD representation of the
  super(sub)set of states satisfying given formula. The super(sub)set of states 
  satisfying given formula is obtained by utilizing the information of 
  the subsystem.] 

  SideEffects   []

  SeeAlso       [Amc_SubsystemInfo_t]

******************************************************************************/
void
Amc_AmcSubsystemSetSatisfy(
  Amc_SubsystemInfo_t *system,
  mdd_t *data)
{
  AmcSubsystemSetSatisfy(system, data);
} /* End of Amc_AmcSubsystemSetSatisfy */

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

  Synopsis  	[Read the vertexTable field of the Amc_SubsystemInfo_t]

  Description   [The vertexTable field of the subsystem is the hash table
  of vertex names. Only the vertices contained in the subsystem is stored
  in this table.]

  SideEffects   []

  SeeAlso       [Amc_SubsystemInfo_t]

******************************************************************************/
st_table *
Amc_AmcSubsystemReadVertexTable(
  Amc_SubsystemInfo_t *system)
{
  return AmcSubsystemReadVertexTable(system);
} /* End of Amc_AmcSubsystemReadVertexTable */

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

  Synopsis 	[Set the vertexTable field of Amc_SubsystemInfo_t ]

  SideEffects   []

  SeeAlso       [Amc_SubsystemInfo_t]

******************************************************************************/
void
Amc_AmcSubsystemSetVertexTable(
  Amc_SubsystemInfo_t *system,
  st_table *data)
{
  AmcSubsystemSetVertexTable(system, data);
} /* End of Amc_AmcSubsystemSetVertexTable */

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

  Synopsis   	[Read the fanInTable field of the Amc_SubsystemInfo_t]

  Description   [The fanInTable is the hash table of the subsystem index.
  The subsystem index is the pointer value uniquely distinguishing subsystems.
  The table contains the index of the subsystems whose component vertex
  is one of the transitive fan-ins of the vertex in this subsystem.]

  SideEffects   []

  SeeAlso       [Amc_SubsystemInfo_t]

******************************************************************************/
st_table *
Amc_AmcSubsystemReadFanInTable(
  Amc_SubsystemInfo_t *system)
{
  return AmcSubsystemReadFanInTable(system);
} /* End of Amc_AmcSubsystemReadFanInTable */

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

  Synopsis 	[Set the fanInTable field of Amc_SubsystemInfo_t ]

  SideEffects   []

  SeeAlso       [Amc_SubsystemInfo_t]

******************************************************************************/
void
Amc_AmcSubsystemSetFanInTable(
  Amc_SubsystemInfo_t *system,
  st_table *data)
{
  AmcSubsystemSetFanInTable(system, data);
} /* End of Amc_AmcSubsystemSetFanInTable */

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

  Synopsis 	[Read the fanOutTable field of the Amc_SubsystemInfo_t]

  Description   [The fanOutTable is the hash table of the subsystem index.
  The subsystem index is the pointer value uniquely distinguishing subsystems.
  The table contains the index of the subsystems whose component vertex
  is one of the transitive fan-outs of the vertex in this subsystem.]

  SideEffects   []

  SeeAlso       [Amc_SubsystemInfo_t]

******************************************************************************/
st_table *
Amc_AmcSubsystemReadFanOutTable(
  Amc_SubsystemInfo_t *system)
{
  return AmcSubsystemReadFanOutTable(system);
} /* End of Amc_AmcSubsystemReadFanOutTable */

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

  Synopsis 	[Set the fanOutTable field of Amc_SubsystemInfo_t ]

  SideEffects   []

  SeeAlso       [Amc_SubsystemInfo_t]

******************************************************************************/
void
Amc_AmcSubsystemSetFanOutTable(
  Amc_SubsystemInfo_t *system,
  st_table *data)
{
  AmcSubsystemSetFanOutTable(system, data);
} /* End of Amc_AmcSubsystemSetFanOutTable */


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

  Synopsis           [Read the MethodSpecific field of Amc_SubsystemInfo_t]

  Description        [The method specific field may hold any value(s) that are
  specific to the various methods.]

  SideEffects        []

  SeeAlso            [Amc_SubsystemInfo_t]

******************************************************************************/
char *
Amc_AmcSubsystemReadMethodSpecificData(
  Amc_SubsystemInfo_t *system)
{
  return AmcSubsystemReadMethodSpecificData(system);
} /* End of Amc_AmcSubsystemReadMethodSpecificData */

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

  Synopsis           [Set the MethodSpecific field of Amc_SubsystemInfo_t]

  SideEffects        []

  SeeAlso            [Amc_SubsystemInfo_t]

******************************************************************************/
void 
Amc_AmcSubsystemSetMethodSpecificData(
  Amc_SubsystemInfo_t *system,
  char                *data)
{
  AmcSubsystemSetMethodSpecificData(system, data);
} /* End of Amc_AmcSubsystemSetMethodSpecificData */



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

  Synopsis 	[Read the initial states from Amc_Info_t]

  SideEffects   []

  SeeAlso       [Amc_Info_t]

******************************************************************************/
mdd_t *
Amc_AmcReadInitialStates(
  Amc_Info_t *system)
{
  return AmcReadInitialStates(system);
} /* End of Amc_AmcReadInitialStates */

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

  Synopsis 	[Sets the initial states from Amc_Info_t]

  SideEffects   []

  SeeAlso       [Amc_Info_t]

******************************************************************************/
void
Amc_AmcSetInitialStates(
  Amc_Info_t	*system,
  mdd_t		*data)
{
  AmcSetInitialStates(system, data);
} /* End of Amc_AmcSetInitialStates */

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

  Synopsis 	[Read the optimal system from Amc_Info_t]

  SideEffects   []

  SeeAlso       [Amc_Info_t]

******************************************************************************/
Amc_SubsystemInfo_t *
Amc_AmcReadOptimalSystem(
  Amc_Info_t *system)
{
  return AmcReadOptimalSystem(system);
} /* End of Amc_AmcReadOptimalSystem */

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

  Synopsis 	[Sets the optimal system from Amc_Info_t]

  SideEffects   []

  SeeAlso       [Amc_Info_t]

******************************************************************************/
void
Amc_AmcSetOptimalSystem(
  Amc_Info_t *system,
  Amc_SubsystemInfo_t    *data)
{
  AmcSetOptimalSystem(system, data);
} /* End of Amc_AmcSetOptimalSystem */

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

  Synopsis 	[Read the MethodData from Amc_Info_t]

  SideEffects   []

  SeeAlso       [Amc_Info_t]

******************************************************************************/
void *
Amc_AmcReadMethodData(
  Amc_Info_t *system)
{
  return AmcReadMethodData(system);
} /* End of Amc_AmcReadMethodData */

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

  Synopsis 	[Sets the MethodData from Amc_Info_t]

  SideEffects   []

  SeeAlso       [Amc_Info_t]

******************************************************************************/
void
Amc_AmcSetMethodData(
  Amc_Info_t	*system,
  void		*data)
{
  AmcSetMethodData(system, data);
} /* End of Amc_AmcSetMethodData */



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

  Synopsis           [Allocate and initialize a Amc_SubsystemInfo_t]

  SideEffects        []

  SeeAlso            [Amc_AmcSubsystemFree]

******************************************************************************/
Amc_SubsystemInfo_t *
Amc_AmcSubsystemAllocate(void)
{
  Amc_SubsystemInfo_t *result;

  result = ALLOC(Amc_SubsystemInfo_t, 1);

  return result;
} /* End of Amc_SubsystemAllocate */


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

  Synopsis           [Create a subsystem.]

  Description        [Create and initialize a subsystem.]

  SideEffects        []

  SeeAlso            []

******************************************************************************/
Amc_SubsystemInfo_t *
Amc_AmcSubsystemCreate(
  Fsm_Fsm_t             *fsm,
  mdd_t                 *satisfyStates,
  st_table              *vertexTable,
  st_table		*fanInTable,
  st_table 		*fanOutTable)
{
  Amc_SubsystemInfo_t *result;

  result                    	= ALLOC(Amc_SubsystemInfo_t, 1);
  result->fsm               	= fsm;
  result->relationArray		= NIL(array_t);
  result->nextStateVarSmoothen	= NIL(mdd_t);
  result->satisfyStates     	= satisfyStates;
  result->vertexTable       	= vertexTable;
  result->fanInTable        	= fanInTable;
  result->fanOutTable       	= fanOutTable;
  result->takenIntoOptimal  	= 0;  /* Initialize to 0 */
  result->methodSpecificData 	= NIL(char);

  return result;
} 

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

  Synopsis           [Duplicate a subsystem.]

  SideEffects        []

  SeeAlso            [Amc_AmcSubsystemAllocate]

******************************************************************************/
Amc_SubsystemInfo_t *
Amc_AmcSubsystemDuplicate(
  Ntk_Network_t       *network, 
  Amc_SubsystemInfo_t *subSystem)
{
  Fsm_Fsm_t	*fsm;
  mdd_t		*satisfyStates	= NIL(mdd_t);
  st_table      *vertexTable	= NIL(st_table);
  st_table	*fanInTable	= NIL(st_table);
  st_table	*fanOutTable	= NIL(st_table);
  graph_t       *partition	= Part_NetworkReadPartition(network);

  if(subSystem->satisfyStates != NIL(mdd_t)) {
    satisfyStates = mdd_dup(subSystem->satisfyStates);
  }
  if(subSystem->vertexTable != NIL(st_table)) {
    vertexTable = st_copy(subSystem->vertexTable);
  }
  if(subSystem->fanInTable != NIL(st_table)) {
    fanInTable = st_copy(subSystem->fanInTable);
  }
  if(subSystem->fanOutTable != NIL(st_table)) {
    fanOutTable = st_copy(subSystem->fanOutTable);
  }

  fsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition, vertexTable,
	FALSE, 0);

  return(Amc_AmcSubsystemCreate(fsm, satisfyStates, vertexTable, fanInTable, fanOutTable));
}



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

  Synopsis           [Free a subsystem.]

  Description        [Frees a subsystem plus associated fields except the 
  partition. This is to reuse the partition without recreating it.]

  SideEffects        []

  SeeAlso            [Amc_AmcSubsystemAllocate]

******************************************************************************/
void
Amc_AmcSubsystemFree(
  Amc_SubsystemInfo_t *subSystem)
{
  st_table 	*vertexTable;
  st_table	*fanInTable, *fanOutTable;

  /* Do not free partition associated to this fsm */
  if (AmcSubsystemReadFsm(subSystem) != NIL(Fsm_Fsm_t)) {
    Fsm_FsmSubsystemFree(AmcSubsystemReadFsm(subSystem));
  } 

  if (AmcSubsystemReadRelationArray(subSystem) != NIL(array_t)) {
    array_t *transitionRelationArray = AmcSubsystemReadRelationArray(subSystem);
    mdd_t   *transitionRelation;
    int		i;
    arrayForEachItem(mdd_t *, transitionRelationArray, i, transitionRelation) {
      mdd_free(transitionRelation); 
    } 
    array_free(transitionRelationArray);
  }

  if (AmcSubsystemReadNextStateVarSmoothen(subSystem) != NIL(mdd_t)) {
    mdd_free(AmcSubsystemReadNextStateVarSmoothen(subSystem));
  }

  if (AmcSubsystemReadSatisfy(subSystem) != NIL(mdd_t)) {
    mdd_free(AmcSubsystemReadSatisfy(subSystem));
  } 

  /* Do not free vertex!! */
  vertexTable = AmcSubsystemReadVertexTable(subSystem);
  if (vertexTable != NIL(st_table)) {
    st_free_table(vertexTable);
  }

  fanInTable = AmcSubsystemReadFanInTable(subSystem);
  if (fanInTable != NIL(st_table)) {
    st_free_table(fanInTable);
  }

  fanOutTable = AmcSubsystemReadFanOutTable(subSystem);
  if (fanOutTable != NIL(st_table)) {
    st_free_table(fanOutTable);
  }


  FREE(subSystem);
} 

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

  Synopsis           [Free a subsystem.]

  Description        [Frees a subsystem including the associated partition.]

  SideEffects        []

  SeeAlso            [Amc_AmcSubsystemAllocate]

******************************************************************************/
void
Amc_AmcSubsystemFreeAlsoPartition(
  Amc_SubsystemInfo_t *subSystem)
{
  st_table      *vertexTable;
  st_table      *fanInTable, *fanOutTable;

  /* Do not free partition associated to this fsm */
  if (AmcSubsystemReadFsm(subSystem) != NIL(Fsm_Fsm_t)) {
    Fsm_FsmFree(AmcSubsystemReadFsm(subSystem));
  } 

  if (AmcSubsystemReadRelationArray(subSystem) != NIL(array_t)) {
    array_t *transitionRelationArray = AmcSubsystemReadRelationArray(subSystem);
    mdd_t   *transitionRelation;
    int         i;
    arrayForEachItem(mdd_t *, transitionRelationArray, i, transitionRelation) {
      mdd_free(transitionRelation); 
    } 
    array_free(transitionRelationArray);
  }

  if (AmcSubsystemReadNextStateVarSmoothen(subSystem) != NIL(mdd_t)) {
    mdd_free(AmcSubsystemReadNextStateVarSmoothen(subSystem));
  }

  if (AmcSubsystemReadSatisfy(subSystem) != NIL(mdd_t)) {
    mdd_free(AmcSubsystemReadSatisfy(subSystem));
  } 

  /* Do not free vertex!! */
  vertexTable = AmcSubsystemReadVertexTable(subSystem);
  if (vertexTable != NIL(st_table)) {
    st_free_table(vertexTable);
  }

  fanInTable = AmcSubsystemReadFanInTable(subSystem);
  if (fanInTable != NIL(st_table)) {
    st_free_table(fanInTable);
  }

  fanOutTable = AmcSubsystemReadFanOutTable(subSystem);
  if (fanOutTable != NIL(st_table)) {
    st_free_table(fanOutTable);
  }


  FREE(subSystem);
} 




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

  Synopsis           [Combine two subsystems and return the resulting
  subsystem.]

  Description        [Take the synchronous product of two subsystems. The routine
  returns resulting subsystem. If either one of the subsystem is NIL return
  the other. It is an error to pass two NIL pointers. Either one has to be
  a subsystem.]

  SideEffects        []

  SeeAlso            []

******************************************************************************/
Amc_SubsystemInfo_t *
Amc_CombineSubsystems(
  Ntk_Network_t		*network,
  Amc_SubsystemInfo_t	*subSystem1,
  Amc_SubsystemInfo_t   *subSystem2)
{
  Amc_SubsystemInfo_t 	*subSystemInfo;
  Amc_SubsystemInfo_t   *subSystem;
  st_table		*vertexTable, *vertexTable1, *vertexTable2;
  st_table		*fanInTable = NIL(st_table);
  st_table 		*fanOutTable = NIL(st_table);
  st_table		*fanInTable1, *fanInTable2;
  st_table		*fanOutTable1, *fanOutTable2;
  Ntk_Node_t    	*latch;  
  graph_t		*partition = Part_NetworkReadPartition(network);
  Fsm_Fsm_t		*fsm;
  lsGen         	gen;
  st_generator          *stGen;

  /* If two subsystem are identical return error */
  if(subSystem1 == subSystem2) {
    error_append("** amc error: illegal subsystem combination");
    return NIL(Amc_SubsystemInfo_t);
  }
  /* If two subsystem are NIL return error */
  if( (subSystem1 == NIL(Amc_SubsystemInfo_t)) && 
      (subSystem2 == NIL(Amc_SubsystemInfo_t)) ) {
    error_append("** amc error: illegal subsystem combination");
    return NIL(Amc_SubsystemInfo_t);
  }

  /* If either of two subsystem is NIL return copy of the other */
  if(subSystem1 == NIL(Amc_SubsystemInfo_t)) {
    return Amc_AmcSubsystemDuplicate(network, subSystem2);
  }
  if(subSystem2 == NIL(Amc_SubsystemInfo_t)) {
    return Amc_AmcSubsystemDuplicate(network, subSystem1);
  }

  vertexTable  = st_init_table(strcmp, st_strhash); 
  vertexTable1 = AmcSubsystemReadVertexTable(subSystem1);
  vertexTable2 = AmcSubsystemReadVertexTable(subSystem2);

  Ntk_NetworkForEachLatch(network, gen, latch) {
    char *latchName = Ntk_NodeReadName(latch);
    if( st_lookup(vertexTable1, latchName, (char **)0) || 
        st_lookup(vertexTable2, latchName, (char **)0) ) {

      st_insert(vertexTable, latchName, (char *)0);

    }
  } /* end of Ntk_NetworkForEachLatch */


  fanInTable1 = AmcSubsystemReadFanInTable(subSystem1);
  fanInTable2 = AmcSubsystemReadFanInTable(subSystem2);
  if( (fanInTable1 != NIL(st_table)) && (fanInTable2 != NIL(st_table)) ) { 

    fanInTable  = st_init_table(st_ptrcmp, st_ptrhash); 

    st_foreach_item(fanInTable1, stGen, &subSystem, NIL(char *)) {
      st_insert(fanInTable, (char *)subSystem, (char *)0);
    }
    st_foreach_item(fanInTable2, stGen, &subSystem, NIL(char *)) {
      st_insert(fanInTable, (char *)subSystem, (char *)0);
    }
  }


  fanOutTable1 = AmcSubsystemReadFanOutTable(subSystem1);
  fanOutTable2 = AmcSubsystemReadFanOutTable(subSystem2);

  if( (fanOutTable1 != NIL(st_table)) && (fanOutTable2 != NIL(st_table)) ) { 

    fanOutTable  = st_init_table(st_ptrcmp, st_ptrhash); 

    st_foreach_item(fanInTable1, stGen, &subSystem, NIL(char *)) {
      st_insert(fanOutTable, subSystem, (char *)0);
    }
    st_foreach_item(fanInTable2, stGen, &subSystem, NIL(char *)) {
      st_insert(fanOutTable, subSystem, (char *)0);
    }
  }


  fsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition, vertexTable,
	FALSE, 0);

  subSystemInfo = Amc_AmcSubsystemCreate(fsm, NIL(mdd_t), vertexTable, 
                                            fanInTable, fanOutTable);

  /* Does not free tables */

  return(subSystemInfo);
}

#ifdef AMC_DEBUG_
/**Function********************************************************************

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

  Description [_Obsolete_]

  SideEffects []

  SeeAlso     [Img_ImageInfoInitialize Fsm_FsmReadImageInfo]

******************************************************************************/
Img_ImageInfo_t *
Amc_AmcReadOrCreateImageInfo(
  Fsm_Fsm_t *fsm)
{
  Img_ImageInfo_t *imageInfo;
  if( Fsm_FsmReadImageInfo(fsm) == NIL(Img_ImageInfo_t)) {
    array_t *dummyInputVars 	= array_alloc(int, 0);
    imageInfo = Img_ImageInfoInitialize(Fsm_FsmReadPartition(fsm),
                                        Fsm_FsmReadNextStateFunctions(fsm),
                                        Fsm_FsmReadPresentStateVars(fsm),
                                        Fsm_FsmReadNextStateVars(fsm),
                                        dummyInputVars,
                                        Fsm_FsmReadNetwork(fsm),
                                        Img_Default_c, Img_Both_c);
    Fsm_FsmSetImageInfo(fsm, imageInfo);
    array_free(dummyInputVars);
  }
  return (imageInfo);
}
#endif

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

  Synopsis    [Model check formula with approxmiations.]

  Description [The routine evaluates given formula with approximations.]
  
  Comment     []

  SideEffects []

******************************************************************************/
mdd_t * 
Amc_AmcEvaluateCTLFormula(
  Amc_SubsystemInfo_t   *subSystem,
  array_t		*subSystemArray,
  Ctlp_Formula_t        *ctlFormula, 
  mdd_t                 *fairStates, 
  Fsm_Fairness_t        *fairCondition, 
  mdd_t                 *modelCareStates,
  boolean               lowerBound,
  array_t		*quantifyVars,
  Mc_VerbosityLevel     verbosity,
  Mc_DcLevel            dcLevel )
{
  Fsm_Fsm_t     *modelFsm = Amc_AmcSubsystemReadFsm(subSystem);

  mdd_t  *leftMdd  = NIL(mdd_t);
  mdd_t  *rightMdd = NIL(mdd_t);
  mdd_t  *result   = NIL(mdd_t);
  mdd_t  *tmpResult = NIL(mdd_t);

  mdd_t *ctlFormulaStates = Ctlp_FormulaObtainStates(ctlFormula );
  mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
  mdd_t *careStates = NIL(mdd_t);
  

  if (ctlFormulaStates) {
    return ctlFormulaStates;
  }
  
  { 
    Ctlp_Formula_t *leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
    if (leftChild) {
      leftMdd = Amc_AmcEvaluateCTLFormula(subSystem, subSystemArray, leftChild, fairStates, fairCondition, 
                                   modelCareStates, lowerBound, quantifyVars, verbosity, dcLevel); 
      if (!leftMdd) 
        return NIL(mdd_t);
    }
  }

  {
    Ctlp_Formula_t *rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
    if (rightChild) {
      rightMdd = Amc_AmcEvaluateCTLFormula(subSystem, subSystemArray, rightChild, fairStates, fairCondition, 
                                    modelCareStates, lowerBound, quantifyVars, verbosity, dcLevel);
      if (!rightMdd ) 
        return NIL(mdd_t);
    }
  }

  careStates = (modelCareStates != NIL(mdd_t)) ?  mdd_dup(modelCareStates) : mdd_one(mddMgr);
  switch ( Ctlp_FormulaReadType( ctlFormula ) ) {

    case Ctlp_ID_c : tmpResult = AmcModelCheckAtomicFormula( modelFsm, ctlFormula ); 

       /* #AMC : Obtain lowerbound of the constraint set. */
      if(0 && lowerBound) { /*Chao: this is not correct! consider !EF(!p) */
        array_t *quantifyPresentVars     = array_fetch(array_t *, quantifyVars, 0);
        int	numOfPresentQuantifyVars = array_n(quantifyPresentVars);
        /* 
         * Currently VIS does not allow primary input as the variable of 
         * the atomic propositions. 
         */
        if(numOfPresentQuantifyVars > 0) {
           result = mdd_consensus(mddMgr, tmpResult, quantifyPresentVars);  
           mdd_free(tmpResult);
        }
        else
           result = tmpResult;
        }
      else
        result = tmpResult;

      break;

    case Ctlp_TRUE_c : result = mdd_one( mddMgr ); break;
    case Ctlp_FALSE_c : result = mdd_zero( mddMgr ); break;

    case Ctlp_NOT_c : result = mdd_not( leftMdd ); break;
    case Ctlp_EQ_c : result = mdd_xnor( leftMdd, rightMdd ); break;
    case Ctlp_XOR_c : result = mdd_xor( leftMdd, rightMdd ); break;
    case Ctlp_THEN_c : result = mdd_or( leftMdd, rightMdd, 0, 1 ); break;
    case Ctlp_AND_c: result = mdd_and( leftMdd, rightMdd, 1, 1 ); break;
    case Ctlp_OR_c: result = mdd_or( leftMdd, rightMdd, 1, 1 ); break;

    case Ctlp_EX_c: 
      result = Amc_AmcEvaluateEXFormula( modelFsm, subSystemArray, subSystem, leftMdd, fairStates, 
					careStates, lowerBound, quantifyVars, verbosity, dcLevel );
      break;

    case Ctlp_EU_c: {
      array_t *onionRings = array_alloc( mdd_t *, 0 );
      result = Amc_AmcEvaluateEUFormula( modelFsm, subSystemArray, subSystem, leftMdd, rightMdd, fairStates, 
                                    careStates, onionRings, lowerBound, quantifyVars, verbosity, dcLevel );
      Ctlp_FormulaSetDbgInfo( ctlFormula, (void *) onionRings, McFormulaFreeDebugData); 
      break;
    }

    case Ctlp_EG_c: {
      array_t *arrayOfOnionRings = array_alloc( array_t *, 0 );
      result = Amc_AmcEvaluateEGFormula( modelFsm, subSystemArray, subSystem, leftMdd, 
					fairStates, fairCondition, careStates, 
					arrayOfOnionRings, lowerBound, quantifyVars, verbosity, dcLevel );
      Ctlp_FormulaSetDbgInfo( ctlFormula, (void *) arrayOfOnionRings, McFormulaFreeDebugData); 
      break;
    }

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


  Ctlp_FormulaSetStates( ctlFormula, result );

  mdd_free( careStates );
  return result;
}

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

  Synopsis    	[Evaluate EX formula with approximations.]

  Description 	[The routine evaluates EX formula with approximations. The 
  routine is used both to obtain lower- and upper- bound of the exact preimage.

  Chao: Let's use the following symbols to represent the present-state vars,
  next-state vars, and the input vars:
    s        -- Present-State Vars
    t        -- Next-State Vars
    x        -- Input Vars
    s_A,t_A  -- PS or NS vars in the abstract model
    s_R,t_R  -- PS or NS vars in the remaining models
    T        -- Transition Relation of the concrete model, T = T_A * T_R
    T_A,T_R  -- TR of the abstract model or the remaining models
  
  The upper-bound EX computation is
    \exist  (s_R) ( \exist (t,x)   (T_A(s,x,t_A)  * C(t))                )

  The lower-bound EX computation is
    \forall (s_R) ( \exist (t_A,x) ( T_A(s,x,t_A) * (\forall (t_R) C(t)) )
  ]

  SideEffects 	[]

  SeeAlso       [AmcInitializeQuantifyVars]

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

mdd_t *
Amc_AmcEvaluateEXFormula(
  Fsm_Fsm_t		*modelFsm,
  array_t		*subSystemArray, 
  Amc_SubsystemInfo_t   *subSystem,
  mdd_t			*targetMdd,
  mdd_t			*fairStates,
  mdd_t			*careStates,
  boolean		lowerBound,
  array_t		*quantifyVars,
  Mc_VerbosityLevel	verbosity,
  Mc_DcLevel		dcLevel )
{
  /* 
   * The care set consists of the passed careStates 
   */
  mdd_t *toCareSet = mdd_dup( careStates );

  mdd_t *fromLowerBound;
  mdd_t *fromUpperBound;
  mdd_t *result = NIL(mdd_t);
  mdd_t *tmpResult;
  mdd_manager *mddManager = Fsm_FsmReadMddManager( modelFsm );
  array_t *quantifyPresentVars = array_fetch(array_t *, quantifyVars, 0);
  
  Img_ImageInfo_t * imageInfo;

  assert(quantifyPresentVars != NIL(array_t));

  imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 1);

  if ( dcLevel == McDcLevelRchFrontier_c ) {
    /*
     * The lower bound is the conjunction of the fair states,
     * the target states, and the care states.
     */
    mdd_t *tmpMdd = mdd_and( targetMdd, fairStates, 1, 1 );
    fromLowerBound = mdd_and( tmpMdd, careStates, 1, 1 );
    mdd_free( tmpMdd );
    /* 
     * The upper bound is the OR of the lower bound with the 
     * complement of the care states.
     */
    fromUpperBound = mdd_or( fromLowerBound, careStates, 1, 0 );
  }
  else {
    /*
     * The lower bound is the conjunction of the fair states,
     * and the target states.
     */
    fromLowerBound = mdd_and( targetMdd, fairStates, 1, 1 );
    /*
     * The upper bound is the same as the lower bound.
     */
    fromUpperBound = mdd_dup( fromLowerBound );
  }


  /***************************************************************************
   * compute C1(s) =
   *    C(s)                         for upper-bound EX computation
   *    ( \forall (s_R) C(s) )       for lower-bound EX computation
   ***************************************************************************/
  if (lowerBound) {
      mdd_t *mdd1, *mdd2;
      mdd1 = fromLowerBound;
      mdd2 = fromUpperBound;
      if (array_n(quantifyPresentVars) > 0) {
	fromLowerBound = mdd_consensus(mddManager, fromLowerBound,
				       quantifyPresentVars);
      } else {
	fromLowerBound = mdd_dup(fromLowerBound);
      }
      if (mdd_equal(mdd1, mdd2)) {
	fromUpperBound = mdd_dup(fromLowerBound);
      }else {
	if (array_n(quantifyPresentVars) > 0) {
	  fromUpperBound = mdd_consensus(mddManager, fromUpperBound,
					 quantifyPresentVars);
	} else {
	  fromUpperBound = mdd_dup(fromUpperBound);
	}
      }
      mdd_free(mdd1);
      mdd_free(mdd2);
  }

  /***************************************************************************
   * Compute \exist (t,x) ( T_A(s,x,t_A) * C1(t) ), where
   *    C1(t) = C(t)                      for upper-bound EX
   *    C1(t) = (\forall (t_R) C(t) )     for lower-bound EX
   ***************************************************************************/
  tmpResult = Img_ImageInfoComputeBwdWithDomainVars( imageInfo,
                                                     fromLowerBound,
                                                     fromUpperBound,
                                                     toCareSet );

  /***************************************************************************
   * Compute the final result
   *    \exist  (s_R)  (tmpResult(s))      for upper-bound EX
   *    \forall (s_R)  (tmpResult(s))      for lower-bound EX
   **************************************************************************/
  if (lowerBound) {
    if (array_n(quantifyPresentVars) > 0) {
      result = mdd_consensus(mddManager, tmpResult, quantifyPresentVars);
    } else {
      result = mdd_dup(tmpResult);
    }
  }else {
    result = mdd_dup(tmpResult);
    /*  result = mdd_smooth(mddManager, tmpResult, quantifyPresentVars);*/
  } 
  mdd_free(tmpResult);
  
  mdd_free( fromLowerBound );
  mdd_free( fromUpperBound );
  mdd_free( toCareSet );

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

  return result;
}

#if 0
/* this is the original (buggy) version */
mdd_t *
Amc_AmcEvaluateEXFormula_Old(
  Fsm_Fsm_t		*modelFsm,
  array_t		*subSystemArray, 
  Amc_SubsystemInfo_t   *subSystem,
  mdd_t			*targetMdd,
  mdd_t			*fairStates,
  mdd_t			*careStates,
  boolean		lowerBound,
  array_t		*quantifyVars,
  Mc_VerbosityLevel	verbosity,
  Mc_DcLevel		dcLevel )
{
  /* 
   * The care set consists of the passed careStates 
   */
  mdd_t *toCareSet = mdd_dup( careStates );

  mdd_t *fromLowerBound;
  mdd_t *fromUpperBound;
  mdd_t *result = NIL(mdd_t);
  mdd_t *tmpResult;

  Img_ImageInfo_t * imageInfo;

  imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 1);

  /*
   * this condition will never  be true; we didnt find it to be 
   * especially effective, are avoiding using it for now. later
   * we may add a McDcLevelMax+1 field which will allow us to use it
   *
   */
  if ( dcLevel > McDcLevelRchFrontier_c ) {
    /*
     * The lower bound is the conjunction of the fair states,
     * the target states, and the care states.
     */
    mdd_t *tmpMdd = mdd_and( targetMdd, fairStates, 1, 1 );
    fromLowerBound = mdd_and( tmpMdd, careStates, 1, 1 );
    mdd_free( tmpMdd );
    /* 
     * The upper bound is the OR of the lower bound with the 
     * complement of the care states.
     */
    fromUpperBound = mdd_or( fromLowerBound, careStates, 1, 0 );
  }
  else {
    /*
     * The lower bound is the conjunction of the fair states,
     * and the target states.
     */
    fromLowerBound = mdd_and( targetMdd, fairStates, 1, 1 );
    /*
     * The upper bound is the same as the lower bound.
     */
    fromUpperBound = mdd_dup( fromLowerBound );
  }

  /* #AMC : */
#ifdef AMC_DEBUG
  if(lowerBound) {
    /* 
     * Sanity check. The set to compute a preimage from should only contain the present
     * state variables of the subsystem.
     */
    {
      mdd_manager       *mddManager	= Fsm_FsmReadMddManager( modelFsm );
      Ntk_Network_t	*network	= Fsm_FsmReadNetwork(modelFsm);
      array_t		*supportArray	= mdd_get_support(mddManager, fromLowerBound);
      st_table		*vertexTable	= Amc_AmcSubsystemReadVertexTable(subSystem);
      int 		i, varId;

      fprintf(vis_stdout, "\n#AMC : Sanity check of the support of the constraint set");
      arrayForEachItem(int, supportArray, i, varId) {
        Ntk_Node_t  *node = Ntk_NetworkFindNodeByMddId(network, varId);
        char *latchName = Ntk_NodeReadName(node); 
        fprintf(vis_stdout, "\n#  fromLowerBound -- Node : %s", latchName);
      }

      arrayForEachItem(int, supportArray, i, varId) {
        char *latchName = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(network, varId)); 
        if( !st_lookup(vertexTable, latchName, (char **)0 )) {
          fprintf(vis_stdout, "\n** amc error : Whoops!! Something's wrong in lowerbound routine.");
          fflush(vis_stdout); 
        }
      } /* end of arrayForEachItem */
    }
  } /* end of if(lowerBound) */
#endif

  tmpResult = Img_ImageInfoComputeBwdWithDomainVars( imageInfo,
                                                     fromLowerBound,
                                                     fromUpperBound,
                                                     toCareSet );
#ifdef AMC_DEBUG
    {
      Ntk_Network_t	*network	= Fsm_FsmReadNetwork(modelFsm);
      mdd_manager 	*mddManager	= Fsm_FsmReadMddManager( modelFsm );
      array_t		*supportArray	= mdd_get_support(mddManager, tmpResult);
      int 		i, varId;

      fprintf(vis_stdout, "\n#AMC : Sanity check of the support of the preimage");
      arrayForEachItem(int, supportArray, i, varId) {
        Ntk_Node_t  *node = Ntk_NetworkFindNodeByMddId(network, varId);
        char *latchName = Ntk_NodeReadName(node); 
        fprintf(vis_stdout, "\n## The preimage contains the node : %s", latchName);
	if( Ntk_NodeTestIsLatch(node) ) 
          fprintf(vis_stdout, "\n##  The node is a latch");
	else
          fprintf(vis_stdout, "\n##  The node is not a latch");

      } /* end of arrayForEachItem */
    }
#endif

  /* #AMC : */
  if(lowerBound) {
    mdd_manager *mddManager	  = Fsm_FsmReadMddManager( modelFsm );
    array_t 	*quantifyNextVars = array_fetch(array_t *, quantifyVars, 1);
    array_t 	*exQuantifiedSystemMddArray; 

    /* 
     * Existential abstraction of next state variables from subsystems that are
     * not currently in consideration. Each subsystem has disjoint next state
     * functions, hence we distribute existential abstraction over subsystems.
     */

    exQuantifiedSystemMddArray =
      Amc_AmcExistentialQuantifySubsystemArray(subSystemArray, subSystem,
					       quantifyNextVars, Amc_User_c);

    /* 
     * Universal abstraction of present state and input variables from
     * subsystems that are not currently in consideration. 
     */
    {
      array_t 	*quantifyPresentVars = array_fetch(array_t *, quantifyVars, 0);
      array_t 	*quantifyInputVars   = array_fetch(array_t *, quantifyVars, 2);
      array_t	*consensusVarArray   = array_join(quantifyPresentVars,
						  quantifyInputVars);
      mdd_t	*interResult	     = mdd_one( mddManager );
      mdd_t	*subMdd;
      int	i;

      array_insert_last(mdd_t *, exQuantifiedSystemMddArray, tmpResult);
      arrayForEachItem(mdd_t *, exQuantifiedSystemMddArray, i, subMdd) {
        mdd_t *cResult = mdd_consensus(mddManager, subMdd, consensusVarArray); 
        result = mdd_and(cResult, interResult, 1, 1); 
        mdd_free(cResult); mdd_free(interResult);
        interResult = result;

        if( mdd_is_tautology(result, 0) ) break;
      }

      mdd_free(tmpResult);
      /* Do not free Mdds. These are cached. */
      array_free(exQuantifiedSystemMddArray);
      array_free(consensusVarArray);
    }


  } /* end of if(lowerBound) */
  else {
   result = tmpResult;
  } /* end of #AMC insertion */

  mdd_free( fromLowerBound );
  mdd_free( fromUpperBound );
  mdd_free( toCareSet );

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

  return result;
}
#endif

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

  Synopsis    [Evaluate EU formula with approximations.]

  Description []

  Comment     []

  SideEffects []

******************************************************************************/
mdd_t *
Amc_AmcEvaluateEUFormula( 
  Fsm_Fsm_t *modelFsm,
  array_t   *subSystemArray, 
  Amc_SubsystemInfo_t   *subSystem,
  mdd_t *invariantMdd,
  mdd_t *targetMdd,
  mdd_t *fairStates,
  mdd_t *careStates,
  array_t *onionRings,
  boolean lowerBound,
  array_t *quantifyVars,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel )
{
  mdd_t *aMdd;
  mdd_t *bMdd;
  mdd_t *cMdd;
  mdd_t *resultMdd = mdd_and( targetMdd, fairStates, 1, 1 );
  mdd_t *ringMdd   = mdd_dup( resultMdd ); 

  while (TRUE) { 

    if ( onionRings ) {
      array_insert_last( mdd_t *, onionRings, mdd_dup( resultMdd ) );
    }

    /*
     * When trying to use dont cares to the hilt, 
     * use a bdd between succ iterations -> ringMdd 
     */
    aMdd = Amc_AmcEvaluateEXFormula( modelFsm, subSystemArray, subSystem, ringMdd, fairStates, careStates,
                                    lowerBound, quantifyVars, verbosity, dcLevel );  
    mdd_free( ringMdd );
    bMdd = mdd_and( aMdd, invariantMdd, 1, 1 ); 
    cMdd = mdd_or( resultMdd, bMdd, 1, 1 ); 

    mdd_free( aMdd );
    mdd_free( bMdd );

    if ( mdd_equal_mod_care_set( cMdd, resultMdd, careStates ) ) {
      mdd_free( cMdd );
      break;
    }

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

    mdd_free( resultMdd );
    resultMdd = cMdd;

  }

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

  return resultMdd;
}

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

  Synopsis    [Evaluate EG formula with approximations.]

  Description []

  SideEffects []

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

mdd_t *
Amc_AmcEvaluateEGFormula( 
  Fsm_Fsm_t *modelFsm,
  array_t   *subSystemArray,
  Amc_SubsystemInfo_t   *subSystem,
  mdd_t *invariantMdd,
  mdd_t *fairStates,
  Fsm_Fairness_t *modelFairness,
  mdd_t *careStates,
  array_t *onionRingsArrayForDbg,
  boolean lowerBound,
  array_t *quantifyVars,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel )
{
  int i;
  array_t *onionRings = NIL(array_t);
  array_t *tmpOnionRingsArrayForDbg = NIL(array_t);
  mdd_manager *mddManager = Fsm_FsmReadMddManager( modelFsm );
  mdd_t *mddOne = mdd_one( mddManager );
  mdd_t *Zmdd;

 
  array_t *buchiFairness = array_alloc( mdd_t *, 0 );
  if (modelFairness) {
    if ( !Fsm_FairnessTestIsBuchi( modelFairness ) ) {
      (void) fprintf(vis_stdout, "#** mc error: non Buchi fairness constraints not supported\n");
      return NIL(mdd_t);
    }
    else {
      int j;
      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct( modelFairness, 0 );
      array_t	*careStatesArray = array_alloc(mdd_t *, 0);

      array_insert(mdd_t *, careStatesArray, 0, careStates);
      for( j = 0 ; j < numBuchi; j++ ) {
        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness,
							0, j, careStatesArray,
							dcLevel);
        array_insert_last( mdd_t *, buchiFairness, tmpMdd );
      }
      array_free(careStatesArray);
    }
  }
  else {
    array_insert_last( mdd_t *, buchiFairness, mdd_one(mddManager) );
  }

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


  Zmdd = mdd_dup( invariantMdd );
  while (TRUE) {

    mdd_t *ZprimeMdd = mdd_dup(Zmdd);
    mdd_t *conjunctsMdd = NIL(mdd_t);
    mdd_t *AAmdd = mdd_dup(Zmdd);

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

      mdd_t *aMdd, *bMdd, *cMdd;
      mdd_t *FiMdd = array_fetch( mdd_t *, buchiFairness, i );

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

      /* aMdd = mdd_and( FiMdd, Zmdd, 1, 1); */
      aMdd = mdd_and( FiMdd, AAmdd, 1, 1);

      bMdd = Amc_AmcEvaluateEUFormula( modelFsm, subSystemArray, subSystem, AAmdd, aMdd, mddOne, careStates, 
                                      onionRings, lowerBound, quantifyVars, verbosity, dcLevel );
      mdd_free(aMdd);
      cMdd = Amc_AmcEvaluateEXFormula( modelFsm, subSystemArray, subSystem, bMdd, mddOne, careStates,
                                      lowerBound, quantifyVars, verbosity, dcLevel ); 
      mdd_free(bMdd);

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

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

    if ( mdd_equal_mod_care_set( ZprimeMdd, Zmdd, careStates ) ) {
      mdd_free( ZprimeMdd );
      break;
    }

    mdd_free( Zmdd );
    Zmdd = ZprimeMdd;

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

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

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

    { 
      mdd_t *tmpMdd = careStates ? mdd_and( Zmdd, careStates, 1, 1 ) : mdd_dup( Zmdd );
      fprintf(vis_stdout, "--There are %.0f states satisfying EG formula\n", 
              mdd_count_onset(  Fsm_FsmReadMddManager( modelFsm ), tmpMdd,
                                Fsm_FsmReadPresentStateVars( modelFsm ) ) );
      mdd_free( tmpMdd );
    }
  }

  mdd_array_free( buchiFairness );
  mdd_free( mddOne );

  return Zmdd;
}


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

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

  Synopsis           [Create an array of subsystems.] 

  Description        [Based on the array of set of vertices, create an 
  array of subsystems. Depending on the grouping method, different function
  call is made to obtain an array of structure typed Part_SubsystemInfo_t. 
  From this information, the vertex table, fan-in table, and the fan-out 
  table is obtained to create an array of subFSMs and the subsystems.
  ]

  SideEffects        []

  SeeAlso            [Part_SubsystemInfo_t]

******************************************************************************/
array_t	*
AmcCreateSubsystemArray(
  Ntk_Network_t         *network,
  Ctlp_Formula_t        *formula)
{
  array_t		*partitionArray, *subSystemArray;
  Part_Subsystem_t	*partitionSubsystem;
  Part_SubsystemInfo_t *subsystemInfo; 
  st_table		*vertexTable;
  array_t	 	*fanInIndexArray, *fanOutIndexArray;
  st_table		*fanInSystemTable, *fanOutSystemTable;
  Amc_SubsystemInfo_t	*subSystem; 
  graph_t		*partition = Part_NetworkReadPartition(network);
  int			i, j;
  int			fanInIndex, fanOutIndex, numOfVertex;
  Amc_SubsystemInfo_t   *fanInSubsystem, *fanOutSubsystem;
  char			*flagValue, *numberOfVertexInGroup;
  array_t               *ctlArray;

  /* Obtain the size of the subsystem */
  numberOfVertexInGroup = Cmd_FlagReadByName("amc_sizeof_group");
  if(numberOfVertexInGroup != NIL(char)){
    numOfVertex = atoi(numberOfVertexInGroup); 
  }
  else{
    /* default value */
    numOfVertex = 8; 
  }

  /* 
   * Obtain subsystem partitioned as submachines. 
   */
  flagValue = Cmd_FlagReadByName("amc_grouping_method");
  if( (flagValue != NIL(char)) && 
           (strcmp(flagValue, "latch_dependency")) == 0){

    subsystemInfo = Part_PartitionSubsystemInfoInit(network);
    Part_PartitionSubsystemInfoSetBound(subsystemInfo, numOfVertex);
    partitionArray = Part_PartCreateSubsystems(subsystemInfo, NIL(array_t),
    	NIL(array_t));
    
    Part_PartitionSubsystemInfoFree(subsystemInfo); 

  }
  else{
    /*
     * Latches which have dependency relation with given formulae
     * are computed and grouped into sub-systems.
     */
    lsGen  gen;
    Ntk_Node_t *node;
    char *name;
    array_t *arrayOfDataInputName;
    lsList latchInputList = lsCreate();

    if (latchInputList == (lsList)0){
      return NIL(array_t);
    }

    ctlArray = array_alloc(Ctlp_Formula_t *, 1);
    array_insert(Ctlp_Formula_t *, ctlArray, 0, formula);

    if (!Part_PartitionGetLatchInputListFromCTL(network, ctlArray,
						NIL(array_t),
						latchInputList)) {
      array_free(ctlArray);
      return NIL(array_t);
    }
    arrayOfDataInputName = array_alloc(Ntk_Node_t *, lsLength(latchInputList));
    lsForEachItem(latchInputList, gen, node){
      name = Ntk_NodeReadName(node);
      array_insert_last(char *, arrayOfDataInputName, name);
    }
    lsDestroy(latchInputList, (void (*)(lsGeneric))0);
    array_sort(arrayOfDataInputName, stringCompare);

    partitionArray = Part_PartGroupVeriticesBasedOnHierarchy(network,
                     arrayOfDataInputName);
    array_free(arrayOfDataInputName);
    array_free(ctlArray);
  }

  subSystemArray = array_alloc(Amc_SubsystemInfo_t *, array_n(partitionArray));


  /* 
   * For each partitioned submachines build an FSM. 
   */
  arrayForEachItem(Part_Subsystem_t *, partitionArray, i, partitionSubsystem) {
    Fsm_Fsm_t *fsm;

    vertexTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
    fanInIndexArray  = Part_PartitionSubsystemReadFanIn(partitionSubsystem);
    fanOutIndexArray = Part_PartitionSubsystemReadFanOut(partitionSubsystem); 

    FREE(partitionSubsystem);

    fsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition, vertexTable,
	FALSE, 0);

    subSystem = Amc_AmcSubsystemCreate(fsm, NIL(mdd_t), vertexTable, 
                                    /*   NIL(st_table), NIL(st_table) ); */
				       (st_table *)fanInIndexArray, 
				       (st_table *)fanOutIndexArray); 
    array_insert_last(Amc_SubsystemInfo_t *, subSystemArray, subSystem);
  } /* end of arrayForEachItem(partitionArray) */

  array_free(partitionArray);

  /* 
   * Convert fanInIndexTable to fanInSystemTable
   * Convert fanOutIndexTable to fanOutSystemTable
   */
  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    fanInIndexArray = (array_t *) AmcSubsystemReadFanInTable(subSystem);
    fanInSystemTable = st_init_table(st_ptrcmp, st_ptrhash);

    if( fanInIndexArray != NIL(array_t) ) {
      arrayForEachItem(int, fanInIndexArray, j, fanInIndex) {
     
        fanInSubsystem = array_fetch(Amc_SubsystemInfo_t *, subSystemArray,
				     fanInIndex);
        st_insert(fanInSystemTable, (char *)fanInSubsystem, NIL(char));

      }
      array_free(fanInIndexArray);
    }

    AmcSubsystemSetFanInTable(subSystem, fanInSystemTable);


    fanOutIndexArray = (array_t *) AmcSubsystemReadFanOutTable(subSystem);
    fanOutSystemTable = st_init_table(st_ptrcmp, st_ptrhash);

    if( fanOutIndexArray != NIL(array_t) ) {
      arrayForEachItem(int, fanOutIndexArray, j, fanOutIndex) {
     
        fanOutSubsystem = array_fetch(Amc_SubsystemInfo_t *, subSystemArray,
				      fanOutIndex);
        st_insert(fanOutSystemTable, (char *)fanOutSubsystem, NIL(char));

      }
      array_free(fanOutIndexArray);
    }

    AmcSubsystemSetFanOutTable(subSystem, fanOutSystemTable);

  }


  return subSystemArray;
}

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

  Synopsis           [Print subsystem(s) taken into the optimal system.]

  SideEffects        [From the array of subsystems, prints the subsystems
  that has been added(combined) to form a optimal system.]

  SeeAlso            []

******************************************************************************/
void
AmcPrintOptimalSystem(
  FILE *fp,
  Amc_Info_t *amcInfo)
{
  int i;
  Amc_SubsystemInfo_t *subSystem;

  fprintf(fp, "\nSubsystems in optimal path : ");

  arrayForEachItem(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, i, subSystem) {
   
    if(subSystem->takenIntoOptimal)
      fprintf(fp, " %d ", i); 
  
  }

}

#ifdef AMC_DEBUG
/**Function********************************************************************

  Synopsis           [Only for the debugging purpose.]

  SideEffects        []

  SeeAlso            []

******************************************************************************/
void
AmcCheckSupportAndOutputFunctions(
  array_t *subSystemArray)
{
  int i;
  Amc_SubsystemInfo_t *subSystem;
  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
    Fsm_Fsm_t	*subSystemFsm	= AmcSubsystemReadFsm(subSystem);	
    Ntk_Network_t *network	= Fsm_FsmReadNetwork(subSystemFsm);
    mdd_manager	*mddManager	= Ntk_NetworkReadMddManager(network);
    graph_t	*partition	= Part_NetworkReadPartition(network);

    st_table	*vertexTable	= AmcSubsystemReadVertexTable(subSystem);
    st_generator		*stGen;
    char			*latchName;

    st_foreach_item(vertexTable, stGen, &latchName, NIL(char *)) {

      Ntk_Node_t	*latch		= Ntk_NetworkFindNodeByName(network, latchName);
      int		functionMddId	= Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch));

      char	*nameLatchDataInput	= Ntk_NodeReadName(Ntk_LatchReadDataInput(latch));
      vertex_t	*ptrVertex	= Part_PartitionFindVertexByName(partition, nameLatchDataInput);
      Mvf_Function_t	*nextStateFunction;
      st_table		*supportTable;

      nextStateFunction	= Part_VertexReadFunction(ptrVertex);
      supportTable 	= AmcCreateFunctionSupportTable(nextStateFunction);

      /* print the name of the latch vars and its mddId in this subsystem*/
      fprintf(vis_stdout, "\nSubsystem %d : Has latch : %s MddId : %d", 
                                             i, latchName, Ntk_NodeReadMddId(latch));
      fprintf(vis_stdout, "\n\tIts corresponding next state var : %s MddId : %d", 
                                             Ntk_NodeReadName(Ntk_NodeReadShadow(latch)),
                                             Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)) );

      /* print the name of the output function and its mddId */
      {
        int outputMddId = Ntk_NodeReadMddId(Ntk_LatchReadDataInput(latch));
        fprintf(vis_stdout, "\n\tIts output function  Output Function : %s  MddId : %d", 
                                              nameLatchDataInput, outputMddId); 
      }

      /* print the support of its output function */
      {
        st_generator		*stGen2;
        long			supportId;
        st_foreach_item(supportTable, stGen2, (char **)&supportId, NIL(char *)) {
          Ntk_Node_t  *supportNode = Ntk_NetworkFindNodeByMddId(network, (int) supportId);
          char		*supportName = Ntk_NodeReadName(supportNode);
          fprintf(vis_stdout, "\n\tOutput function's support : %s MddId : %d",
                                                supportName, (int) supportId); 
          fflush(vis_stdout);
        } 
      }


    } /* end of st_foreach_item */

  } /* end of ArrayForEachItem */


  /* Print the name of the present state vars and its mddId */
  /* Print the name of the next state vars and its mddId */
  /* Print the input vars */
  {
    Amc_SubsystemInfo_t *subSystem = array_fetch(Amc_SubsystemInfo_t *, subSystemArray, 0);
    Fsm_Fsm_t   *subSystemFsm	   = AmcSubsystemReadFsm(subSystem);
    Ntk_Network_t *network         = Fsm_FsmReadNetwork(subSystemFsm);
    lsGen gen; Ntk_Node_t *inputNode;
    Ntk_NetworkForEachPrimaryInput(network, gen, inputNode) {
      fprintf(vis_stdout, "\nPrimary Input : %s MddId : %d", 
                             Ntk_NodeReadName(inputNode), Ntk_NodeReadMddId(inputNode));
    }
  }

  /* Print the pseudo input vars */
  {
    Amc_SubsystemInfo_t *subSystem = array_fetch(Amc_SubsystemInfo_t *, subSystemArray, 0); 
    Fsm_Fsm_t   *subSystemFsm	   = AmcSubsystemReadFsm(subSystem);
    Ntk_Network_t *network         = Fsm_FsmReadNetwork(subSystemFsm);
    lsGen gen; Ntk_Node_t *inputNode;
    Ntk_NetworkForEachPseudoInput(network, gen, inputNode) {
      fprintf(vis_stdout, "\nPseudo Input : %s MddId : %d", 
                             Ntk_NodeReadName(inputNode), Ntk_NodeReadMddId(inputNode));
      fflush(vis_stdout);
    }
  }

}

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

  Synopsis           [Only for debugging.]

  SideEffects        []

  SeeAlso            [Amc_SubsystemInfo]

******************************************************************************/
st_table *
AmcCreateFunctionSupportTable(
  Mvf_Function_t *mvf)
{
  mdd_manager  *mddManager;        /* Manager for the MDDs */
  array_t      *support;
  st_table     *mddSupport = st_init_table(st_numcmp, st_numhash);
  int          numComponents = Mvf_FunctionReadNumComponents(mvf);
  int          j, k;
  mdd_t        *unit;

  assert(numComponents!= 0);
  
  mddManager = Mvf_FunctionReadMddManager(mvf);

  /*
   * compute the support of an mdd as the union of supports of every
   * function component 
   */
  for(j = 0; j < numComponents; j++) {
    unit = Mvf_FunctionReadComponent(mvf, j);
    support = mdd_get_support(mddManager, unit);
    
    /* For every element of its support */
    for(k = 0; k < array_n(support); k++) {
      st_insert(mddSupport, (char *)(long)array_fetch(int, support, k), (char *)0);
    } /* End of for */
    array_free(support);
  } /* End of for */

  return mddSupport;
} /* End of */
#endif


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

  Synopsis    [Find Mdd for states satisfying Atomic Formula.]

  Description [This is a duplicate copy of static function, 
  ModelCheckAtomicFormula(). ] 

  SideEffects []

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

  Var_Variable_t *nodeVar;
  int nodeValue;

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

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

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

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

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

    tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue );
    resultMdd = mdd_dup( tmpMdd );
    Mvf_FunctionFree( MVF );
    return resultMdd;
  }
  else {
    MVF = Part_VertexReadFunction( partitionVertex );
    tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue );
    resultMdd = mdd_dup( tmpMdd );
    return resultMdd;
  }
}


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

  Synopsis [Compare two strings]

  SideEffects []

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