src/amc/amcAmc.c

Go to the documentation of this file.

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


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

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

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


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


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

}

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

}


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

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


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

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


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

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

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

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

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

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

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

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

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

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


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

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



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

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

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

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

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

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



Amc_SubsystemInfo_t *
Amc_AmcSubsystemAllocate(void)
{
  Amc_SubsystemInfo_t *result;

  result = ALLOC(Amc_SubsystemInfo_t, 1);

  return result;
} /* End of Amc_SubsystemAllocate */


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

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



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

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




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_

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

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

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

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

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

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

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

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

}

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


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                                            */
/*---------------------------------------------------------------------------*/
static int
stringCompare(
  const void * s1,
  const void * s2)
{
  return(strcmp(*(char **)s1, *(char **)s2));
}