src/imc/imcImc.c

Go to the documentation of this file.

#include "imcInt.h" 
#include "part.h"
#include "img.h"
#include "ntm.h"

static char rcsid[] UNUSED = "$Id: imcImc.c,v 1.21 2005/04/27 00:13:01 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                                          */
/*---------------------------------------------------------------------------*/

Imc_VerificationResult
Imc_ImcEvaluateFormulaLinearRefine(
  Ntk_Network_t         *network,
  Ctlp_Formula_t        *orgFormula,
  Ctlp_Formula_t        *formula,
  Ctlp_FormulaClass     formulaClass,
  int                   incrementalSize,
  Imc_VerbosityLevel    verbosity,
  Imc_RefineMethod      refine,
  mdd_t                 *careStates,
  Fsm_Fsm_t             *exactFsm,
  Imc_DcLevel           dcLevel,
  Imc_GraphType         graphType,
  Imc_LowerMethod       lowerMethod,
  Imc_UpperMethod       upperMethod,
  boolean               computeExact,
  boolean               needLower,
  boolean               needUpper,
  Imc_PartMethod        partMethod,
  Hrc_Node_t            *currentNode,
  char                  *modelName)
{
  Imc_Info_t            *imcInfo;
  st_table              *latchNameTable;
  int                   numberOfLatches, numberOfIncludedLatches;
  int                   iterationCount;
  Imc_VerificationResult verification = Imc_VerificationError_c;

  /*
   * Initialize data structures.
   */
  imcInfo = Imc_ImcInfoInitialize(network, formula, formulaClass, verbosity,
                                  refine, careStates, dcLevel, incrementalSize,
                                  graphType, exactFsm, lowerMethod, upperMethod,
                                  computeExact, needLower, needUpper,
                                  partMethod, currentNode, modelName);

  if (imcInfo == NIL(Imc_Info_t))return(Imc_VerificationError_c); /* FIXED */

  numberOfLatches = array_n(imcInfo->systemInfo->latchNameArray);
 
  iterationCount = 1;

  numberOfIncludedLatches = array_n(imcInfo->systemInfo->includedLatchIndex);

  if (verbosity != Imc_VerbosityNone_c) {
    fprintf(vis_stdout, "IMC : Reduced system has ");
    Imc_ImcPrintSystemSize(imcInfo);
  }
  if(verbosity != Imc_VerbosityNone_c) {
    fprintf(vis_stdout, "IMC : Approximate system has ");
    Imc_ImcPrintApproxSystemSize(imcInfo);
  }

  assert(numberOfLatches >= numberOfIncludedLatches);
  while(numberOfLatches >= numberOfIncludedLatches) {
 
    /*
     * verification is one of {Imc_VerificationTrue_c, Imc_VerificationFalse_c,
     * Imc_VerificationInconclusive_c}.
     */
    verification = Imc_ImcVerifyFormula(imcInfo, formula);

    if (verification == Imc_VerificationError_c) {

      (void)fprintf(vis_stdout, "# IMC: formula inconclusive.\n");

      /* Free all */
      Imc_ImcInfoFree(imcInfo);
      return verification;

    }else if (verification != Imc_VerificationInconclusive_c){ 

      if ((verification == Imc_VerificationTrue_c)) {
        (void) fprintf(vis_stdout, "# IMC: formula passed.\n");
      }else{
        (void) fprintf(vis_stdout, "# IMC: formula failed.\n");
      }
      fprintf(vis_stdout, "IMC : ");
      Ctlp_FormulaPrint( vis_stdout, orgFormula );
      fprintf(vis_stdout, "\n");
      fprintf(vis_stdout, "IMC : ");
      Ctlp_FormulaPrint( vis_stdout, formula);
      fprintf(vis_stdout, "\n");

      Imc_ImcInfoFree(imcInfo);
      return verification;
    }else{
      if (numberOfLatches == numberOfIncludedLatches){
        if (imcInfo->graphType == Imc_GraphPDOG_c){
          (void) fprintf(vis_stdout, "# IMC: formula passed.\n");
        }else if (imcInfo->graphType == Imc_GraphNDOG_c){
          (void) fprintf(vis_stdout, "# IMC: formula failed.\n");
        }
        fprintf(vis_stdout, "IMC : ");
        Ctlp_FormulaPrint( vis_stdout,orgFormula);
        fprintf(vis_stdout, "\n");
        fprintf(vis_stdout, "IMC : ");
        Ctlp_FormulaPrint( vis_stdout, formula); 
        fprintf(vis_stdout, "\n");

        Imc_ImcInfoFree(imcInfo);
        return verification;
      }
    }       

    latchNameTable = array_fetch(st_table *, 
                     imcInfo->staticRefineSchedule, iterationCount);
    
    Imc_ImcSystemInfoUpdate(imcInfo, latchNameTable);

    /*
     * Refine the approximate system.
     */ 
    if (imcInfo->needUpper){
      Imc_UpperSystemInfoFree(imcInfo->upperSystemInfo);
      Imc_UpperSystemInfoInitialize(imcInfo, latchNameTable);
    }

    if (imcInfo->needLower){
      Imc_LowerSystemInfoFree(imcInfo->lowerSystemInfo);
      Imc_LowerSystemInfoInitialize(imcInfo, latchNameTable);
    }

    Imc_NodeInfoReset(imcInfo);

    numberOfIncludedLatches = 
        array_n(imcInfo->systemInfo->includedLatchIndex);

    iterationCount++;

    if(verbosity != Imc_VerbosityNone_c) {
      fprintf(vis_stdout, "IMC : Approximate system has ");
      Imc_ImcPrintApproxSystemSize(imcInfo);
    }

  } /* end of while(numberOfLatches >= numberOfIncludedLatches) */

  return(verification); /* FIXED */
}

Imc_VerificationResult
Imc_ImcVerifyFormula(
  Imc_Info_t *imcInfo,
  Ctlp_Formula_t *formula)
{
  Imc_VerificationResult result;

  if (!Imc_ImcEvaluateCTLFormula(imcInfo, formula, Imc_PolarityPos_c)){
    return Imc_VerificationError_c;
  }

  result = Imc_SatCheck(imcInfo, formula);

  return result;
}

Imc_VerificationResult
Imc_SatCheck(
  Imc_Info_t *imcInfo,
  Ctlp_Formula_t *formula)
{
  mdd_t *initialStates = imcInfo->initialStates;
  Imc_NodeInfo_t *nodeInfo;

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    return Imc_VerificationError_c; /* FIXED */
  }
  
  if (nodeInfo->lowerSat != NIL(mdd_t)){
    if (mdd_lequal(initialStates, nodeInfo->lowerSat, 1, 1)){
      return Imc_VerificationTrue_c;
    }
  }
  if (nodeInfo->upperSat != NIL(mdd_t)){
    if (!mdd_lequal_mod_care_set(initialStates, nodeInfo->upperSat, 1, 1,
                                 imcInfo->modelCareStates)){ /* FIXED */
      return Imc_VerificationFalse_c;
    }
  }
  return Imc_VerificationInconclusive_c;
}

Imc_Info_t *
Imc_ImcInfoInitialize(
  Ntk_Network_t      *network,
  Ctlp_Formula_t     *formula,
  Ctlp_FormulaClass  formulaClass,
  Imc_VerbosityLevel verbosity,
  Imc_RefineMethod   refine,
  mdd_t              *careStates,
  Imc_DcLevel        dcLevel,
  int                incrementalSize,
  Imc_GraphType      graphType,
  Fsm_Fsm_t          *exactFsm,
  Imc_LowerMethod    lowerMethod,
  Imc_UpperMethod    upperMethod,
  boolean            computeExact,
  boolean            needLower,
  boolean            needUpper,
  Imc_PartMethod     partMethod,
  Hrc_Node_t         *currentNode, 
  char               *modelName)
{
  int                 i;
  char                *flagValue;  
  Imc_Info_t          *imcInfo;
  mdd_t               *initialStates;
  array_t             *scheduleArray;
  st_table            *latchNameTable;
  st_table            *newLatchNameTable;
  st_table            *globalLatchNameTable;
  array_t             *psMddIdArray;
  array_t             *nsMddIdArray;
  array_t             *inputMddIdArray;
  array_t             *supportMddIdArray;
  array_t             *preQMddIdArray;
  array_t             *imgQMddIdArray;
  Part_CMethod        correlationMethod;
  Ntk_Node_t          *latch, *input;
  lsGen               gen;
  array_t             *latchNameArray;

  imcInfo = ALLOC(Imc_Info_t, 1);

  /*
   * Initialize 
   */
  imcInfo->network         = network;
  imcInfo->globalFsm       = exactFsm;
  imcInfo->formulaClass    = formulaClass;
  imcInfo->incrementalSize = incrementalSize;
  imcInfo->dcLevel         = dcLevel;
  imcInfo->refine          = refine;
  imcInfo->verbosity       = verbosity;
  imcInfo->upperSystemInfo = NIL(Imc_UpperSystemInfo_t);
  imcInfo->lowerSystemInfo = NIL(Imc_LowerSystemInfo_t);
  imcInfo->initialStates   = NIL(mdd_t); 
  imcInfo->nodeInfoTable   = NIL(st_table);
  imcInfo->graphType       = graphType;
  imcInfo->nodeInfoTable   = st_init_table(st_ptrcmp , st_ptrhash);
  imcInfo->mddMgr          = Ntk_NetworkReadMddManager(network);
  imcInfo->lowerMethod     = lowerMethod;
  imcInfo->upperMethod     = upperMethod;
  imcInfo->currentNode     = currentNode;
  imcInfo->modelName       = modelName;

  if (exactFsm == NIL(Fsm_Fsm_t)){
    imcInfo->useLocalFsm = TRUE;
  }else{
    imcInfo->useLocalFsm = FALSE;
  }

  /*
   * Initialize image and preimage computation info.
   */
  if (exactFsm != NIL(Fsm_Fsm_t)){
    psMddIdArray = array_dup(Fsm_FsmReadPresentStateVars(exactFsm));
    nsMddIdArray = array_dup(Fsm_FsmReadNextStateVars(exactFsm));
    inputMddIdArray = array_dup(Fsm_FsmReadInputVars(exactFsm));
  }else{
    latchNameArray = array_alloc(char *, 0);
    psMddIdArray = array_alloc(int, 0);
    nsMddIdArray = array_alloc(int, 0);
    inputMddIdArray = array_alloc(int, 0);
    /* sort by name of latch */
    Ntk_NetworkForEachLatch(network, gen, latch){
      array_insert_last(char*, latchNameArray,
                        Ntk_NodeReadName(latch));
    }

    array_sort(latchNameArray, stringCompare);

    for (i = 0; i < array_n(latchNameArray); i++) {
      char *nodeName;
      nodeName = array_fetch(char *, latchNameArray, i);
      latch = Ntk_NetworkFindNodeByName(network, nodeName);
      array_insert_last(int, psMddIdArray,
                      Ntk_NodeReadMddId(latch));
      array_insert_last(int, nsMddIdArray,
                      Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
    }
 
    array_free(latchNameArray);
  
    Ntk_NetworkForEachInput(network, gen, input){
      array_insert_last(int, inputMddIdArray, Ntk_NodeReadMddId(input));
    }
  }

  imgQMddIdArray = array_dup(psMddIdArray);
  array_append(imgQMddIdArray,inputMddIdArray); 

  supportMddIdArray = array_dup(imgQMddIdArray);
  array_append(supportMddIdArray,nsMddIdArray);

  preQMddIdArray = array_dup(nsMddIdArray);
  array_append(preQMddIdArray,inputMddIdArray); 

  array_free(psMddIdArray);
  array_free(nsMddIdArray);
  array_free(inputMddIdArray);
  
  imcInfo->supportMddIdArray = supportMddIdArray;
  imcInfo->imgQMddIdArray = imgQMddIdArray;
  imcInfo->preQMddIdArray = preQMddIdArray;
  imcInfo->needLower = needLower;
  imcInfo->needUpper = needUpper;
  imcInfo->partMethod = partMethod;

  if (careStates == NIL(mdd_t)){
    imcInfo->modelCareStates = mdd_one(imcInfo->mddMgr);
  }else{
    imcInfo->modelCareStates = mdd_dup(careStates);
  }

  /*
   * If refine oprion is Imc_RefineLatchRelation_c,
   * correlation method should be defined.
   */
  flagValue = Cmd_FlagReadByName("part_group_correlation_method");
  if(flagValue == NIL(char)){
    correlationMethod = Part_CorrelationWithBDD; 
  }else if (strcmp(flagValue, "support") == 0){
    correlationMethod = Part_CorrelationWithSupport; 
  }else if (strcmp(flagValue, "mdd") == 0){
    correlationMethod = Part_CorrelationWithBDD;
  }else{
    correlationMethod = Part_CorrelationWithSupport;
  }

  if ((refine == Imc_RefineLatchRelation_c) &&
      (correlationMethod == Part_CorrelationWithBDD) &&
      (partMethod == Imc_PartInc_c)){
    correlationMethod = Part_CorrelationWithSupport;
  }
  imcInfo->correlationMethod = correlationMethod;

  if (computeExact){
    scheduleArray = ImcCreateScheduleArray(network, formula, TRUE, 
                      Imc_RefineLatchRelation_c, verbosity, incrementalSize,
                      correlationMethod);
    imcInfo->staticRefineSchedule = NIL(array_t);
    latchNameTable = array_fetch(st_table *, scheduleArray, 0);
    st_free_table(latchNameTable);
    latchNameTable = array_fetch(st_table *, scheduleArray, 1);
    newLatchNameTable = st_copy(latchNameTable);
    array_insert(st_table *, scheduleArray, 0, newLatchNameTable);

  }else if (refine == Imc_RefineLatchRelation_c){
    scheduleArray = ImcCreateScheduleArray(network, formula, FALSE, refine, 
                    verbosity, incrementalSize, correlationMethod);
    imcInfo->staticRefineSchedule = scheduleArray;

  }else if (refine == Imc_RefineSort_c){
    scheduleArray = ImcCreateScheduleArray(network, formula, TRUE, refine, 
                    verbosity, incrementalSize, correlationMethod);
    imcInfo->staticRefineSchedule = scheduleArray;

  }else{
    fprintf(vis_stdout, "** imc error: Unkown refinement method.\n");
    Imc_ImcInfoFree(imcInfo);
    return NIL(Imc_Info_t);
  }

  if (scheduleArray == NIL(array_t)){
    fprintf(vis_stdout, "** imc error: Can't get an initial system.\n");
    Imc_ImcInfoFree(imcInfo);
    return NIL(Imc_Info_t);
  }
    
  globalLatchNameTable = array_fetch(st_table *, scheduleArray, array_n(scheduleArray)-1);
  latchNameTable = array_fetch(st_table *, scheduleArray, 0);  

  /*
   * Initialize a total system info.
   */
  Imc_SystemInfoInitialize(imcInfo, globalLatchNameTable, latchNameTable);  

  /*
   * Initialize an initial approximate system info.
   */
  if (needUpper){
    Imc_UpperSystemInfoInitialize(imcInfo,latchNameTable);
  }
  if (needLower){
    Imc_LowerSystemInfoInitialize(imcInfo,latchNameTable);
  }

  initialStates = Fsm_FsmComputeInitialStates(imcInfo->globalFsm);  
  if (initialStates == NIL(mdd_t)){
    fprintf(vis_stdout,"** imc error : System has no initial state.\n");
    Imc_ImcInfoFree(imcInfo);
    return NIL(Imc_Info_t);
  }
  imcInfo->initialStates = initialStates;  

  if (computeExact){
    arrayForEachItem(st_table *, scheduleArray, i, latchNameTable){
      st_free_table(latchNameTable);
    }
    array_free(scheduleArray);
  }

  return(imcInfo);
}


void
Imc_ImcInfoFree(
  Imc_Info_t *imcInfo)
{
  int i;
  st_table *latchNameTable;

  Imc_UpperSystemInfoFree(imcInfo->upperSystemInfo);
  Imc_LowerSystemInfoFree(imcInfo->lowerSystemInfo);
  ImcNodeInfoTableFree(imcInfo->nodeInfoTable);
  if (imcInfo->initialStates != NIL(mdd_t)) mdd_free(imcInfo->initialStates); 

  if (imcInfo->modelCareStates!=NIL(mdd_t)) mdd_free(imcInfo->modelCareStates);
  if (imcInfo->staticRefineSchedule != NIL(array_t)){
    arrayForEachItem(st_table *,imcInfo->staticRefineSchedule, i, latchNameTable){
      st_free_table(latchNameTable);
    }
    array_free(imcInfo->staticRefineSchedule);
  }
  if (imcInfo->supportMddIdArray != NIL(array_t)) 
    array_free(imcInfo->supportMddIdArray);
  if (imcInfo->imgQMddIdArray != NIL(array_t)) 
    array_free(imcInfo->imgQMddIdArray);
  if (imcInfo->preQMddIdArray != NIL(array_t)) 
    array_free(imcInfo->preQMddIdArray);

  if ((imcInfo->useLocalFsm) && (imcInfo->globalFsm != NIL(Fsm_Fsm_t))){
    Fsm_FsmSubsystemFree(imcInfo->globalFsm);
  }

  Imc_SystemInfoFree(imcInfo->systemInfo);

  FREE(imcInfo);
}


void
Imc_SystemInfoInitialize(
  Imc_Info_t *imcInfo,
  st_table *globalLatchNameTable,
  st_table *initialLatchNameTable)
{
  int i, psMddId, nsMddId, latchSize;
  char *name, *dataInputName;
  Ntk_Node_t *node, *latchInput;  
  Ntk_Network_t *network = imcInfo->network;
  graph_t *partition = Part_NetworkReadPartition(network);
  vertex_t *vertex;
  Mvf_Function_t *mvf;
  mdd_t *singleTR, *subTR, *tempMdd;
  st_generator *stGen;
  lsList latchInputList;
  lsGen gen;
  st_table *partNameTable;
  Imc_SystemInfo_t *systemInfo;
  array_t *bddIdArray;
  array_t *latchNameArray = 
           array_alloc(char *, st_count(globalLatchNameTable));
  st_table *latchNameTable = st_init_table(strcmp, st_strhash );
  st_table *latchInputTable = st_init_table(st_ptrcmp, st_ptrhash );
  st_table *nsMddIdToIndex = st_init_table(st_numcmp, st_numhash);
  st_table *psMddIdToIndex = st_init_table(st_numcmp, st_numhash);
  array_t *latchNodeArray = 
           array_alloc(Ntk_Node_t *, st_count(globalLatchNameTable));
  array_t *nsMddIdArray = array_alloc(int,st_count(globalLatchNameTable));
  array_t *psMddIdArray = array_alloc(int,st_count(globalLatchNameTable));
  array_t *TRArray = array_alloc(mdd_t *,st_count(globalLatchNameTable));
  array_t *lowerTRArray = array_alloc(mdd_t *,st_count(globalLatchNameTable));
  array_t *mvfArray = array_alloc(mdd_t *,st_count(globalLatchNameTable));
  array_t *latchSizeArray = array_alloc(int,st_count(globalLatchNameTable));
  array_t *includedLatchIndex = array_alloc(int, 0);
  array_t *includedNsMddId = array_alloc(int, 0);
  array_t *excludedLatchIndex = array_alloc(int, 0);
  array_t *excludedNsMddId = array_alloc(int, 0);
  array_t *excludedPsMddId = array_alloc(int, 0);
  array_t *includedPsMddId = array_alloc(int, 0);
  st_table *excludedPsMddIdTable = st_init_table(st_numcmp, st_numhash);

  systemInfo = ALLOC(Imc_SystemInfo_t, 1);

  st_foreach_item(globalLatchNameTable, stGen, &name, NIL(char *)){
    array_insert_last(char *, latchNameArray, name);
  }

  array_sort(latchNameArray, stringCompare);

  if (partition == NIL(graph_t)){
    if ((imcInfo->partMethod == Imc_PartInc_c) &&
        !((imcInfo->needLower) && 
         (imcInfo->lowerMethod != Imc_LowerUniversalQuantification_c))){
      partNameTable = initialLatchNameTable;
    }else{
      partNameTable = globalLatchNameTable;
    }
    st_foreach_item(partNameTable, stGen, &name, NIL(char *)){
      node = Ntk_NetworkFindNodeByName(network, name);
      latchInput = Ntk_LatchReadDataInput(node);
      st_insert(latchInputTable, (char *)latchInput, (char *)(long)(-1));
    }
    latchInputList = lsCreate();
    st_foreach_item(latchInputTable, stGen, &node, NULL){
      lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
    }
    st_free_table(latchInputTable);
    Ntk_NetworkForEachCombOutput(network, gen, node){
      if (Ntk_NodeTestIsLatchInitialInput(node)){
        lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
      }
    }

    partition = Part_NetworkCreatePartition(network, imcInfo->currentNode, 
                  imcInfo->modelName, latchInputList, (lsList)0, NIL(mdd_t),
                  Part_InOut_c, (lsList)0, FALSE, 0, 0);
    lsDestroy(latchInputList, (void (*)(lsGeneric))0); 
    
    Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
                  (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                  (void *) partition);

    imcInfo->globalFsm = Fsm_FsmCreateSubsystemFromNetwork(network,partition,
                                                    partNameTable, FALSE, 0);

    imcInfo->useLocalFsm = TRUE;
  }else{
    st_foreach_item(initialLatchNameTable, stGen, &name, NIL(char *)){
      node = Ntk_NetworkFindNodeByName(network, name);
      latchInput = Ntk_LatchReadDataInput(node);
      st_insert(latchInputTable, (char *)latchInput, (char *)(long)(-1));
    }
    latchInputList = lsCreate();
    st_foreach_item(latchInputTable, stGen, &node, NIL(char *)){
      lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
    }
    st_free_table(latchInputTable);
    Ntk_NetworkForEachCombOutput(network, gen, node){
      if (Ntk_NodeTestIsLatchInitialInput(node)){
        lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
      }
    }
    (void) Part_PartitionChangeRoots(network, partition,
                                     latchInputList, 0);
    lsDestroy(latchInputList, (void (*)(lsGeneric))0);
  }

  for (i=0;i<array_n(latchNameArray);i++){
    name = array_fetch(char *, latchNameArray, i);
    node = Ntk_NetworkFindNodeByName(network, name);
    psMddId = Ntk_NodeReadMddId(node);
    nsMddId = Ntk_NodeReadMddId(Ntk_NodeReadShadow(node));

    dataInputName = Ntk_NodeReadName(Ntk_LatchReadDataInput(node));

    if (st_is_member(initialLatchNameTable, name)) { 
      vertex = Part_PartitionFindVertexByName(partition, dataInputName);
      mvf = Part_VertexReadFunction(vertex);      
      singleTR = Mvf_FunctionBuildRelationWithVariable(mvf, nsMddId);
      array_insert(mdd_t *, TRArray, i, 
                   bdd_minimize(singleTR, imcInfo->modelCareStates));
      array_insert(mdd_t *, lowerTRArray, i, NIL(mdd_t));
      array_insert(Mvf_Function_t *, mvfArray, i, NIL(Mvf_Function_t));
      mdd_free(singleTR);
    }else{
      array_insert(Mvf_Function_t *, mvfArray, i, NIL(Mvf_Function_t));
      array_insert(mdd_t *, lowerTRArray, i, NIL(mdd_t));
      array_insert(mdd_t *, TRArray, i, NIL(mdd_t));
    }
    

    if (!st_is_member(initialLatchNameTable, name)){
      if (imcInfo->needLower && 
         imcInfo->lowerMethod != Imc_LowerUniversalQuantification_c){
        singleTR = array_fetch(mdd_t *, TRArray, i);
        if (singleTR == NIL(mdd_t)){
          vertex = Part_PartitionFindVertexByName(partition, dataInputName);
          mvf = Part_VertexReadFunction(vertex);                  
          singleTR = Mvf_FunctionBuildRelationWithVariable(mvf, nsMddId);
          tempMdd = mdd_and(singleTR, imcInfo->modelCareStates, 1, 1);
          mdd_free(singleTR);
        }else{
          tempMdd = mdd_and(singleTR, imcInfo->modelCareStates, 1, 1);
        }           
        subTR = bdd_approx_remap_ua(tempMdd,(bdd_approx_dir_t)BDD_UNDER_APPROX,
                                    array_n(imcInfo->supportMddIdArray), 0, 1.0);
        mdd_free(tempMdd);
        tempMdd = bdd_minimize(subTR, imcInfo->modelCareStates);
        mdd_free(subTR);
        subTR = tempMdd;
        array_insert(mdd_t *, lowerTRArray, i, subTR);
        array_insert(Mvf_Function_t *, mvfArray, i, NIL(Mvf_Function_t));
      }   
    }

    if (st_is_member(initialLatchNameTable, name)){
      array_insert_last(int, includedLatchIndex, i);
      array_insert_last(int, includedNsMddId, nsMddId);
      array_insert_last(int, includedPsMddId, psMddId);
    }else{
      array_insert_last(int, excludedLatchIndex, i);
      array_insert_last(int, excludedNsMddId, nsMddId);
      array_insert_last(int, excludedPsMddId, psMddId);
      st_insert(excludedPsMddIdTable, (char *)(long)psMddId, 
                      (char *)0);
    }      
    bddIdArray = mdd_id_to_bdd_id_array(imcInfo->mddMgr, nsMddId);
    latchSize = array_n(bddIdArray);
    array_free(bddIdArray);
    st_insert(latchNameTable, name, (char *)(long)i);
    st_insert(nsMddIdToIndex,(char *)(long)nsMddId, (char *)(long)i); 
    st_insert(psMddIdToIndex,(char *)(long)psMddId, (char *)(long)i);
    array_insert(Ntk_Node_t *, latchNodeArray, i, node);
    array_insert(int, latchSizeArray, i, latchSize);
 
    array_insert(int, nsMddIdArray, i, nsMddId);
    array_insert(int, psMddIdArray, i, psMddId);
  }
  
  systemInfo->latchNameTable = latchNameTable;
  systemInfo->latchNameArray = latchNameArray;
  systemInfo->latchNodeArray = latchNodeArray;  
  systemInfo->nsMddIdArray = nsMddIdArray;
  systemInfo->psMddIdArray = psMddIdArray;
  systemInfo->inputMddIdArray = 
    array_dup(Fsm_FsmReadInputVars(imcInfo->globalFsm));
  systemInfo->TRArray = TRArray;
  systemInfo->lowerTRArray = lowerTRArray;
  systemInfo->mvfArray = mvfArray;
  systemInfo->latchSizeArray = latchSizeArray;
  systemInfo->nsMddIdToIndex = nsMddIdToIndex;
  systemInfo->psMddIdToIndex = psMddIdToIndex;
  systemInfo->excludedLatchIndex  = excludedLatchIndex;
  systemInfo->includedLatchIndex  = includedLatchIndex; 
  systemInfo->excludedNsMddId  = excludedNsMddId;
  systemInfo->includedNsMddId  = includedNsMddId; 
  systemInfo->excludedPsMddId  = excludedPsMddId; 
  systemInfo->includedPsMddId  = includedPsMddId; 
  systemInfo->excludedPsMddIdTable  = excludedPsMddIdTable;

  imcInfo->systemInfo = systemInfo;
}

void
Imc_SystemInfoFree(
  Imc_SystemInfo_t *systemInfo)
{
  int i;
  mdd_t *singleTR;

  if (systemInfo->latchNameTable != NIL(st_table))
    st_free_table(systemInfo->latchNameTable);
  if (systemInfo->latchNameArray != NIL(array_t))
    array_free(systemInfo->latchNameArray);
  if (systemInfo->latchNodeArray != NIL(array_t))
    array_free(systemInfo->latchNodeArray);
  if (systemInfo->nsMddIdArray != NIL(array_t))
    array_free(systemInfo->nsMddIdArray);
  if (systemInfo->psMddIdArray != NIL(array_t))
    array_free(systemInfo->psMddIdArray);
  if (systemInfo->inputMddIdArray != NIL(array_t))
    array_free(systemInfo->inputMddIdArray);
  if (systemInfo->TRArray != NIL(array_t)){
    for(i=0;i<array_n(systemInfo->TRArray);i++){
      singleTR = array_fetch(mdd_t *, systemInfo->TRArray, i);
      if (singleTR != NIL(mdd_t)){
        mdd_free(singleTR);
      }
    }
    array_free(systemInfo->TRArray);   
  }

  if (systemInfo->lowerTRArray != NIL(array_t)){
    for(i=0;i<array_n(systemInfo->lowerTRArray);i++){
      singleTR = array_fetch(mdd_t *, systemInfo->lowerTRArray, i);
      if (singleTR != NIL(mdd_t)){
        mdd_free(singleTR);
      }
    }
    array_free(systemInfo->lowerTRArray);
  }

  if (systemInfo->mvfArray != NIL(array_t))
    array_free(systemInfo->mvfArray);
  if (systemInfo->latchSizeArray != NIL(array_t))
    array_free(systemInfo->latchSizeArray);
  if (systemInfo->nsMddIdToIndex != NIL(st_table))
    st_free_table(systemInfo->nsMddIdToIndex);
  if (systemInfo->psMddIdToIndex != NIL(st_table))
    st_free_table(systemInfo->psMddIdToIndex);
  if (systemInfo->excludedLatchIndex != NIL(array_t))
    array_free(systemInfo->excludedLatchIndex);
  if (systemInfo->includedLatchIndex != NIL(array_t))
    array_free(systemInfo->includedLatchIndex);
  if (systemInfo->excludedNsMddId != NIL(array_t))
    array_free(systemInfo->excludedNsMddId);
  if (systemInfo->includedNsMddId != NIL(array_t))
    array_free(systemInfo->includedNsMddId);
  if (systemInfo->excludedPsMddId != NIL(array_t))
     array_free(systemInfo->excludedPsMddId);
  if (systemInfo->includedPsMddId != NIL(array_t))
     array_free(systemInfo->includedPsMddId);
  if (systemInfo->excludedPsMddIdTable != NIL(st_table))
    st_free_table(systemInfo->excludedPsMddIdTable);

  FREE(systemInfo);
}

void
Imc_ImcSystemInfoUpdate(
  Imc_Info_t *imcInfo,
  st_table *newLatchNameTable)
{
  int i, nsMddId, psMddId, index;
  char *name, *dataInputName;
  mdd_t *singleTR;
  st_generator *stGen;
  Ntk_Node_t *node, *latchInput;
  Mvf_Function_t *mvf;
  vertex_t *vertex;
  lsList latchInputList;
  lsGen gen;
  graph_t *partition = Part_NetworkReadPartition(imcInfo->network);
  st_table *latchInputTable;
  Imc_SystemInfo_t *systemInfo = imcInfo->systemInfo;

  if ((imcInfo->partMethod == Imc_PartInc_c) &&
      !(imcInfo->needLower && 
        imcInfo->lowerMethod != Imc_LowerUniversalQuantification_c)){
    latchInputTable = st_init_table(st_ptrcmp, st_ptrhash );
    st_foreach_item(newLatchNameTable, stGen, &name, NIL(char *)){
      node = Ntk_NetworkFindNodeByName(imcInfo->network, name);
      latchInput = Ntk_LatchReadDataInput(node);
      st_insert(latchInputTable, (char *)latchInput, (char *)(long)(-1));
    }
    latchInputList = lsCreate();
    st_foreach_item(latchInputTable, stGen, &node, NULL){
      lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
    }
    st_free_table(latchInputTable);
    Ntk_NetworkForEachCombOutput(imcInfo->network, gen, node){
      if (Ntk_NodeTestIsLatchInitialInput(node)){
        lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
      }
    }
    (void) Part_PartitionChangeRoots(imcInfo->network, partition,
                                     latchInputList, 0);
    lsDestroy(latchInputList, (void (*)(lsGeneric))0); 
  }

  if (systemInfo->excludedLatchIndex != NIL(array_t)){
    array_free(systemInfo->excludedLatchIndex);
    systemInfo->excludedLatchIndex = array_alloc(int, 0);
  }
  if (systemInfo->includedLatchIndex != NIL(array_t)){
    array_free(systemInfo->includedLatchIndex);
    systemInfo->includedLatchIndex = array_alloc(int, 0);
  }
  if (systemInfo->excludedNsMddId != NIL(array_t)){
    array_free(systemInfo->excludedNsMddId);
    systemInfo->excludedNsMddId = array_alloc(int, 0);
  }
  if (systemInfo->includedNsMddId != NIL(array_t)){
    array_free(systemInfo->includedNsMddId);
    systemInfo->includedNsMddId = array_alloc(int, 0);
  }
  if (systemInfo->excludedPsMddId != NIL(array_t)){
     array_free(systemInfo->excludedPsMddId);
     systemInfo->excludedPsMddId = array_alloc(int, 0);
  }
  if (systemInfo->includedPsMddId != NIL(array_t)){
     array_free(systemInfo->includedPsMddId);
     systemInfo->includedPsMddId = array_alloc(int, 0);
  }
  if (systemInfo->excludedPsMddIdTable != NIL(st_table)){
    st_free_table(systemInfo->excludedPsMddIdTable);
    systemInfo->excludedPsMddIdTable = st_init_table(st_numcmp, st_numhash);
  }
  
  for(i=0;i<array_n(imcInfo->systemInfo->latchNameArray);i++){
    name = array_fetch(char *,imcInfo->systemInfo->latchNameArray,i);
    node = Ntk_NetworkFindNodeByName(imcInfo->network, name);
    psMddId = Ntk_NodeReadMddId(node);
    nsMddId = Ntk_NodeReadMddId(Ntk_NodeReadShadow(node));

    if (st_is_member(newLatchNameTable, name)){
      array_insert_last(int, systemInfo->includedLatchIndex, i);
      array_insert_last(int, systemInfo->includedNsMddId, nsMddId);
      array_insert_last(int, systemInfo->includedPsMddId, psMddId);
    }else{
      array_insert_last(int, systemInfo->excludedLatchIndex, i);
      array_insert_last(int, systemInfo->excludedNsMddId, nsMddId);
      array_insert_last(int, systemInfo->excludedPsMddId, psMddId);
      st_insert(systemInfo->excludedPsMddIdTable, (char *)(long)psMddId, 
                      (char *)0);
    }      
  }
     
  st_foreach_item(newLatchNameTable, stGen, &name, NIL(char *)){
    st_lookup_int(imcInfo->systemInfo->latchNameTable,name, &index);
    nsMddId = array_fetch(int, imcInfo->systemInfo->nsMddIdArray, index);
    psMddId = array_fetch(int, imcInfo->systemInfo->psMddIdArray, index);

    mvf = array_fetch(Mvf_Function_t *, imcInfo->systemInfo->mvfArray, index);

    if (mvf == NIL(Mvf_Function_t)){
      node = Ntk_NetworkFindNodeByName(imcInfo->network, name); 
      latchInput = Ntk_LatchReadDataInput(node);
      dataInputName = Ntk_NodeReadName(Ntk_LatchReadDataInput(node));  
      vertex = Part_PartitionFindVertexByName(partition, dataInputName);
      mvf = Part_VertexReadFunction(vertex);
    }

    singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->TRArray, index);

    if (singleTR == NIL(mdd_t)){ 
      singleTR = Mvf_FunctionBuildRelationWithVariable(mvf, nsMddId);
      array_insert(mdd_t *, imcInfo->systemInfo->TRArray, index, 
                   bdd_minimize(singleTR, imcInfo->modelCareStates));

      array_insert(Mvf_Function_t *, imcInfo->systemInfo->mvfArray, index, 
                   NIL(Mvf_Function_t));
      mdd_free(singleTR);
    }

    singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->lowerTRArray, index);
    if (singleTR != NIL(mdd_t)){ 
      mdd_free(singleTR);
      array_insert(mdd_t *,imcInfo->systemInfo->lowerTRArray,index,NIL(mdd_t));
    }        
  }
}

void
Imc_UpperSystemInfoInitialize(
  Imc_Info_t *imcInfo,
  st_table   *latchNameTable)
{
  int                   i, index;
  int                   count;
  char                  *name;
  Imc_UpperSystemInfo_t *upperSystem;
  st_table              *globalLatchNameTable;
  array_t               *globalLatchNameArray;
  array_t               *relationArray;
  mdd_t                 *singleTR;

  upperSystem = ALLOC(Imc_UpperSystemInfo_t, 1);
  upperSystem->systemInfo = imcInfo->systemInfo;

  globalLatchNameTable = imcInfo->systemInfo->latchNameTable;
  globalLatchNameArray = imcInfo->systemInfo->latchNameArray;

  relationArray = array_alloc(mdd_t *, st_count(latchNameTable));

  count = 0;

  for (i=0;i<array_n(globalLatchNameArray);i++){
    name = array_fetch(char *, globalLatchNameArray, i);  
    if (st_is_member(latchNameTable, name)){
      st_lookup_int(globalLatchNameTable, name, (int *)&index);
      singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->TRArray, index);
      array_insert(mdd_t *, relationArray, count++, singleTR);
    }
  }

  Img_ClusterRelationArray(imcInfo->mddMgr, Img_Iwls95_c, Img_Backward_c,
                           relationArray,
                           imcInfo->systemInfo->psMddIdArray,
                           imcInfo->systemInfo->nsMddIdArray,
                           imcInfo->systemInfo->inputMddIdArray,
                           &upperSystem->bwdRealationArray,
                           &upperSystem->bwdSmoothVarsArray,
                           NIL(array_t *), 0); /* FIXED */
  upperSystem->fwdRealationArray = NIL(array_t);
  upperSystem->fwdSmoothVarsArray = NIL(array_t);
  upperSystem->bwdMinimizedRealationArray = NIL(array_t);

  upperSystem->careStates = mdd_dup(imcInfo->modelCareStates);

  array_free(relationArray);
 
  imcInfo->upperSystemInfo = upperSystem;

  if ((imcInfo->verbosity == Imc_VerbosityMin_c) ||
      (imcInfo->verbosity == Imc_VerbosityMax_c)){
    fprintf(vis_stdout, "IMC: |BWD Upper T| = %10ld BDD nodes (%-4d components)\n",
      bdd_size_multiple(upperSystem->bwdRealationArray),
      array_n(upperSystem->bwdRealationArray));
  }
  return;
}

void
Imc_UpperSystemMinimize(
  Imc_Info_t *imcInfo,
  mdd_t *careStates)
{
  int i;
  mdd_t *singleTR;
  mdd_t *tempMdd;
  Imc_UpperSystemInfo_t *upperSystem = imcInfo->upperSystemInfo;

  if (mdd_equal(careStates,upperSystem->careStates)) return;

  if (upperSystem->bwdMinimizedRealationArray == NIL(array_t)){
    upperSystem->bwdMinimizedRealationArray = 
      array_alloc(mdd_t *, array_n(upperSystem->bwdRealationArray));
    for (i=0;i<array_n(upperSystem->bwdRealationArray);i++){
      array_insert(mdd_t *, upperSystem->bwdMinimizedRealationArray, i, NIL(mdd_t));
    }
  }

  for (i=0;i<array_n(upperSystem->bwdRealationArray);i++){ 
    singleTR = array_fetch(mdd_t *, upperSystem->bwdMinimizedRealationArray, i);
    if (singleTR != NIL(mdd_t)){
      mdd_free(singleTR);
    }
    singleTR = array_fetch(mdd_t *, upperSystem->bwdRealationArray, i);
    tempMdd = bdd_minimize(singleTR, careStates);
    array_insert(mdd_t *, upperSystem->bwdMinimizedRealationArray, i, tempMdd);
  }
 
  if (upperSystem->careStates != NIL(mdd_t)){
    mdd_free(upperSystem->careStates);
  }
  upperSystem->careStates = mdd_dup(careStates);

  if ((imcInfo->verbosity == Imc_VerbosityMin_c) ||
      (imcInfo->verbosity == Imc_VerbosityMax_c)){
    fprintf(vis_stdout, "IMC: |Minimized BWD Upper T| = %10ld BDD nodes (%-4d components)\n",
      bdd_size_multiple(upperSystem->bwdMinimizedRealationArray),
      array_n(upperSystem->bwdMinimizedRealationArray));
  }

  return;
}

void
Imc_UpperSystemInfoFree(
  Imc_UpperSystemInfo_t *upperSystem)
{
  int i;
  array_t *tempArray;

  if (upperSystem == NIL(Imc_UpperSystemInfo_t)) return;   

  if (upperSystem->careStates != NIL(mdd_t)){
    mdd_free(upperSystem->careStates);
  }

  if (upperSystem->fwdRealationArray != NIL(array_t)){
    mdd_array_free(upperSystem->fwdRealationArray);
    upperSystem->fwdRealationArray = NIL(array_t);
  }
  if (upperSystem->fwdSmoothVarsArray != NIL(array_t)){
    array_free(upperSystem->fwdSmoothVarsArray);
    upperSystem->fwdSmoothVarsArray = NIL(array_t);
  }
  if (upperSystem->bwdRealationArray != NIL(array_t)){
    mdd_array_free(upperSystem->bwdRealationArray);
    upperSystem->bwdRealationArray = NIL(array_t);
  }
  if (upperSystem->bwdMinimizedRealationArray != NIL(array_t)){
    mdd_array_free(upperSystem->bwdMinimizedRealationArray);
    upperSystem->bwdMinimizedRealationArray = NIL(array_t);
  }
  if (upperSystem->bwdSmoothVarsArray != NIL(array_t)){
    for (i=0; i<array_n(upperSystem->bwdSmoothVarsArray);i++){
      tempArray = array_fetch(array_t *, upperSystem->bwdSmoothVarsArray, i);
      mdd_array_free(tempArray);
    }
    array_free(upperSystem->bwdSmoothVarsArray);
    upperSystem->bwdSmoothVarsArray = NIL(array_t);
  }

  FREE(upperSystem);
  return;
}


void
Imc_LowerSystemInfoInitialize(
  Imc_Info_t *imcInfo,
  st_table   *latchNameTable)
{
  int                   i, index;
  char                  *name;
  st_generator          *stGen;
  mdd_t                 *singleTR;
  Imc_LowerSystemInfo_t *lowerSystem;
  array_t               *tempArray;
  array_t               *relationArray;
  st_table              *globalLatchNameTable;
  array_t               *latchNameArray;

  lowerSystem = ALLOC(Imc_LowerSystemInfo_t, 1);

  if ((imcInfo->lowerMethod == Imc_LowerUniversalQuantification_c) &&
      (imcInfo->upperSystemInfo != NIL(Imc_UpperSystemInfo_t))){
    lowerSystem->bwdRealationArray = mdd_array_duplicate(
      imcInfo->upperSystemInfo->bwdRealationArray);
    lowerSystem->bwdSmoothVarsArray = array_alloc(array_t *,
      array_n(imcInfo->upperSystemInfo->bwdSmoothVarsArray));
    for (i=0;i<array_n(imcInfo->upperSystemInfo->bwdSmoothVarsArray);i++){
      tempArray =  array_fetch(array_t *,
        imcInfo->upperSystemInfo->bwdSmoothVarsArray, i);
      array_insert(array_t *, lowerSystem->bwdSmoothVarsArray, i,
        mdd_array_duplicate(tempArray));
    }
    lowerSystem->careStates = mdd_dup(imcInfo->modelCareStates);
    lowerSystem->bwdMinimizedRealationArray = NIL(array_t);
    imcInfo->lowerSystemInfo = lowerSystem;
    return;
  }

  globalLatchNameTable = imcInfo->systemInfo->latchNameTable;

  latchNameArray = array_alloc(char *, 0);
  st_foreach_item(globalLatchNameTable, stGen, &name, NIL(char *)){
    array_insert_last(char *, latchNameArray, name);
  }

  array_sort(latchNameArray, stringCompare);

  relationArray = array_alloc(mdd_t *, 0);

  for (i=0;i<array_n(latchNameArray);i++){
    name = array_fetch(char *, latchNameArray, i);
    st_lookup_int(globalLatchNameTable, name, (int *)&index);
    if (st_lookup(latchNameTable, name, NIL(char *))){
      singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->TRArray, index);
    }else{
      singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->lowerTRArray, index);
    }
    if (singleTR != NIL(mdd_t)){
      array_insert_last(mdd_t *, relationArray, singleTR);
    }
  }

  array_free(latchNameArray);

  Img_ClusterRelationArray(imcInfo->mddMgr, Img_Iwls95_c, Img_Backward_c,
                           relationArray,
                           imcInfo->systemInfo->psMddIdArray,
                           imcInfo->systemInfo->nsMddIdArray,
                           imcInfo->systemInfo->inputMddIdArray,
                           &lowerSystem->bwdRealationArray,
                           &lowerSystem->bwdSmoothVarsArray,
                           NIL(array_t *), 0); /* FIXED */
  lowerSystem->bwdMinimizedRealationArray = NIL(array_t);

  lowerSystem->careStates = mdd_dup(imcInfo->modelCareStates);;

  imcInfo->lowerSystemInfo = lowerSystem;

  if ((imcInfo->verbosity == Imc_VerbosityMin_c) ||
      (imcInfo->verbosity == Imc_VerbosityMax_c)){
    fprintf(vis_stdout, "IMC: |BWD Lower T| = %10ld BDD nodes (%-4d components)\n",
      bdd_size_multiple(lowerSystem->bwdRealationArray),
      array_n(lowerSystem->bwdRealationArray));
  }

  array_free(relationArray); /* Should be freed here, I guess, Chao Wang */
  
  return;
}

void
Imc_LowerSystemMinimize(
  Imc_Info_t *imcInfo,
  mdd_t *careStates)
{
  int i;
  mdd_t *singleTR;
  mdd_t *tempMdd;

  Imc_LowerSystemInfo_t *lowerSystem = imcInfo->lowerSystemInfo;

  if (mdd_equal(careStates,lowerSystem->careStates)) return;

  if (lowerSystem->bwdMinimizedRealationArray == NIL(array_t)){
    lowerSystem->bwdMinimizedRealationArray = 
      array_alloc(mdd_t *, array_n(lowerSystem->bwdRealationArray));
    for (i=0;i<array_n(lowerSystem->bwdRealationArray);i++){
      array_insert(mdd_t *, lowerSystem->bwdMinimizedRealationArray, i, NIL(mdd_t));
    }
  } 

  for (i=0;i<array_n(lowerSystem->bwdRealationArray);i++){
    singleTR = array_fetch(mdd_t *, lowerSystem->bwdMinimizedRealationArray, i);
    if (singleTR != NIL(mdd_t)){
      mdd_free(singleTR);
    }
    singleTR = array_fetch(mdd_t *, lowerSystem->bwdRealationArray, i);
    tempMdd = bdd_minimize(singleTR, careStates);
    array_insert(mdd_t *, lowerSystem->bwdMinimizedRealationArray, i, tempMdd);
  }

  if (lowerSystem->careStates != NIL(mdd_t)){
    mdd_free(lowerSystem->careStates);
  }

  lowerSystem->careStates = mdd_dup(careStates);
  if ((imcInfo->verbosity == Imc_VerbosityMin_c) ||
      (imcInfo->verbosity == Imc_VerbosityMax_c)){
    fprintf(vis_stdout, "IMC: |Minimized BWD Lower T| = %10ld BDD nodes (%-4d components)\n",
      bdd_size_multiple(lowerSystem->bwdMinimizedRealationArray),
      array_n(lowerSystem->bwdMinimizedRealationArray));
  }
}


void
Imc_LowerSystemInfoFree(
  Imc_LowerSystemInfo_t *lowerSystem)
{
  int i;
  array_t *tempArray;

  if (lowerSystem == NIL(Imc_LowerSystemInfo_t)) return;   

  if (lowerSystem->careStates != NIL(mdd_t)){
    mdd_free(lowerSystem->careStates);
  }

  if (lowerSystem->bwdRealationArray != NIL(array_t)){
    mdd_array_free(lowerSystem->bwdRealationArray);
    lowerSystem->bwdRealationArray = NIL(array_t);
  }
  if (lowerSystem->bwdMinimizedRealationArray != NIL(array_t)){
    mdd_array_free(lowerSystem->bwdMinimizedRealationArray);
    lowerSystem->bwdMinimizedRealationArray = NIL(array_t);
  }
  if (lowerSystem->bwdSmoothVarsArray != NIL(array_t)){
    for (i=0; i<array_n(lowerSystem->bwdSmoothVarsArray);i++){
      tempArray = array_fetch(array_t *, lowerSystem->bwdSmoothVarsArray, i);
      mdd_array_free(tempArray);
    }
    array_free(lowerSystem->bwdSmoothVarsArray);
    lowerSystem->bwdSmoothVarsArray = NIL(array_t); /* FIXED */
  }

  FREE(lowerSystem);
  return;
}

Imc_NodeInfo_t *
Imc_NodeInfoInitialize(
  Imc_Polarity polarity)
{
  Imc_NodeInfo_t *nodeInfo; 

  nodeInfo = ALLOC(Imc_NodeInfo_t, 1);

  nodeInfo->isExact = FALSE;
  nodeInfo->polarity = polarity;
  nodeInfo->upperSat = NIL(mdd_t);
  nodeInfo->lowerSat = NIL(mdd_t);
  nodeInfo->propagatedGoalSet = NIL(mdd_t);
  nodeInfo->propagatedGoalSetTrue = NIL(mdd_t);
  nodeInfo->goalSet = NIL(mdd_t);
  nodeInfo->goalSetTrue = NIL(mdd_t);
  nodeInfo->answer = Imc_VerificationInconclusive_c;
  nodeInfo->upperDone = FALSE;
  nodeInfo->lowerDone = FALSE;
  nodeInfo->pseudoEdges = NIL(mdd_t);
  return nodeInfo;
}


void
Imc_NodeInfoReset(
  Imc_Info_t *imcInfo)
{
  Ctlp_Formula_t *formula;
  st_table *nodeInfoTable = imcInfo->nodeInfoTable;
  st_generator *stGen;
  Imc_NodeInfo_t *nodeInfo;

  st_foreach_item(nodeInfoTable, stGen, &formula, &nodeInfo){
    if (!nodeInfo->isExact){
      nodeInfo->lowerDone = FALSE;
      nodeInfo->upperDone = FALSE;
    }
    if (nodeInfo->propagatedGoalSet != NIL(mdd_t)){
      mdd_free(nodeInfo->propagatedGoalSet);
      nodeInfo->propagatedGoalSet = NIL(mdd_t);
    }
    if (nodeInfo->propagatedGoalSetTrue != NIL(mdd_t)){
      mdd_free(nodeInfo->propagatedGoalSetTrue);
      nodeInfo->propagatedGoalSetTrue = NIL(mdd_t);
    }
    if (nodeInfo->goalSet != NIL(mdd_t)){
      mdd_free(nodeInfo->goalSet);
      nodeInfo->goalSet = NIL(mdd_t);
    }
    if (nodeInfo->goalSetTrue != NIL(mdd_t)){
      mdd_free(nodeInfo->goalSetTrue);
      nodeInfo->goalSetTrue = NIL(mdd_t);
    }
    if (nodeInfo->pseudoEdges != NIL(mdd_t)){
      mdd_free(nodeInfo->pseudoEdges);
      nodeInfo->pseudoEdges = NIL(mdd_t);
    }   
  }
}


void
Imc_NodeInfoFree(
  Imc_NodeInfo_t *nodeInfo)
{
  if (nodeInfo->upperSat != NIL(mdd_t)){
    mdd_free(nodeInfo->upperSat);
  }
  if (nodeInfo->lowerSat != NIL(mdd_t)){
    mdd_free(nodeInfo->lowerSat);
  }
  if (nodeInfo->goalSet != NIL(mdd_t)){
    mdd_free(nodeInfo->goalSet);
  }
  if (nodeInfo->goalSetTrue != NIL(mdd_t)){  
    mdd_free(nodeInfo->goalSetTrue);
  }
  if (nodeInfo->propagatedGoalSet != NIL(mdd_t)){
    mdd_free(nodeInfo->propagatedGoalSet);
  }
  if (nodeInfo->propagatedGoalSetTrue != NIL(mdd_t)){  
    mdd_free(nodeInfo->propagatedGoalSetTrue);
  }
  if (nodeInfo->pseudoEdges != NIL(mdd_t)){  
    mdd_free(nodeInfo->pseudoEdges);
  }
  FREE(nodeInfo);
}


void
Imc_ImcPrintSystemSize(
  Imc_Info_t *imcInfo)
{
  array_t *includedBooleanVars;
  array_t *psMddIdArray = imcInfo->systemInfo->psMddIdArray;

  includedBooleanVars = mdd_id_array_to_bdd_id_array(imcInfo->mddMgr,
                        psMddIdArray);

  fprintf(vis_stdout, "%d(%d) ",
          array_n(psMddIdArray), array_n(includedBooleanVars));
  fprintf(vis_stdout, "multi-value(boolean) latches.\n");

  array_free(includedBooleanVars);  
}


void
Imc_ImcPrintApproxSystemSize(
  Imc_Info_t *imcInfo)
{
  int i, index, psMddId;
  array_t *includedBooleanVars;
  array_t *includedPsMddIdArray;
  array_t *psMddIdArray = imcInfo->systemInfo->psMddIdArray;
  array_t *includedLatchIndex = imcInfo->systemInfo->includedLatchIndex;
  
  includedPsMddIdArray = array_alloc(int,array_n(includedLatchIndex));

  for(i=0;i<array_n(includedLatchIndex);i++){
    index = array_fetch(int,includedLatchIndex, i); 
    psMddId = array_fetch(int, psMddIdArray, index); 
    array_insert(int, includedPsMddIdArray, i, psMddId);
  }
 
  includedBooleanVars = mdd_id_array_to_bdd_id_array(imcInfo->mddMgr,
                        includedPsMddIdArray);

  fprintf(vis_stdout, "%d(%d) ",
          array_n(includedPsMddIdArray), array_n(includedBooleanVars));
  fprintf(vis_stdout, "multi-value(boolean) latches.\n");

  array_free(includedPsMddIdArray);
  array_free(includedBooleanVars);  
}

mdd_t *
Imc_GetUpperSat(
  Imc_Info_t *imcInfo,
  Ctlp_Formula_t *formula)
{
  Imc_NodeInfo_t *nodeInfo;

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    return NIL(mdd_t); 
  }

  return nodeInfo->upperSat;
}

mdd_t *
Imc_GetLowerSat(
  Imc_Info_t *imcInfo,
  Ctlp_Formula_t *formula)
{
  Imc_NodeInfo_t *nodeInfo;

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    return NIL(mdd_t); 
  }

  return nodeInfo->lowerSat;
}

int 
Imc_ImcEvaluateCTLFormula(
  Imc_Info_t            *imcInfo,
  Ctlp_Formula_t        *ctlFormula, 
  Imc_Polarity          polarity)
{
  Imc_Polarity newPolarity, approxPolarity;
  Ctlp_Formula_t *leftChild, *rightChild;
  Imc_NodeInfo_t *nodeInfo;
  Imc_GraphType graphType = imcInfo->graphType;

  if (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_NOT_c){
    newPolarity = (polarity == Imc_PolarityNeg_c) ? Imc_PolarityPos_c: 
                  (polarity == Imc_PolarityPos_c) ? Imc_PolarityNeg_c:
                  polarity;
  }else{
    newPolarity = polarity;
  }

  if (graphType == Imc_GraphNDOG_c){
    /* In-Ho : Why change the polarity ? */
    approxPolarity = (polarity == Imc_PolarityNeg_c) ? Imc_PolarityPos_c:
                     Imc_PolarityNeg_c;
  }else{
    approxPolarity = polarity;
  } 

  if (!st_lookup(imcInfo->nodeInfoTable, ctlFormula, &nodeInfo)){
    nodeInfo = Imc_NodeInfoInitialize(polarity);
    st_insert(imcInfo->nodeInfoTable, ctlFormula, nodeInfo);
  }else if ((nodeInfo->isExact) ||
            ((approxPolarity == Imc_PolarityNeg_c) && (nodeInfo->lowerDone)) ||
            ((approxPolarity == Imc_PolarityPos_c) && (nodeInfo->upperDone))){
    if (imcInfo->verbosity == Imc_VerbosityMax_c){
      if ((Ctlp_FormulaReadType( ctlFormula ) == Ctlp_ID_c ) ||
          (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_TRUE_c ) ||
          (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_FALSE_c )){ 
        fprintf(vis_stdout, "IMC : node simple already computed.\n");
      }else if ((Ctlp_FormulaReadType( ctlFormula ) == Ctlp_AND_c ) ||
                (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_NOT_c )){ 
        fprintf(vis_stdout, "IMC : node boolean already computed.\n");
      }else{
        /* In-Ho : Why only ECTL? */
        fprintf(vis_stdout, "IMC : node ECTL already computed.\n");
      }
    }
    return 1;
  }
  
  leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
  if (leftChild) {
    if (!Imc_ImcEvaluateCTLFormula(imcInfo,leftChild,newPolarity)){
       return 0;
    } 
  }
  rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
  if (rightChild) {
    if (!Imc_ImcEvaluateCTLFormula(imcInfo,rightChild,newPolarity)){ 
       return 0;
    } 
  }

  switch ( Ctlp_FormulaReadType( ctlFormula ) ) {

    case Ctlp_ID_c : 
      if (!ImcModelCheckAtomicFormula(imcInfo,ctlFormula)) return 0; 
      break;
    case Ctlp_TRUE_c : 
      if (!ImcModelCheckTrueFalseFormula(imcInfo,ctlFormula, TRUE)) return 0; 
      break;
    case Ctlp_FALSE_c : 
      if (!ImcModelCheckTrueFalseFormula(imcInfo,ctlFormula, FALSE)) return 0;
      break;
    case Ctlp_NOT_c :
      if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){
              if (!ImcModelCheckNotFormula(imcInfo,ctlFormula, TRUE)) return 0;
      }
      if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){
              if(!ImcModelCheckNotFormula(imcInfo,ctlFormula, FALSE)) return 0;
      } 
      break;
    case Ctlp_AND_c :
      if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){       
        if (!ImcModelCheckAndFormula(imcInfo,ctlFormula,TRUE))return 0;
      }
      if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){
        if (!ImcModelCheckAndFormula(imcInfo,ctlFormula,FALSE)) return 0;
      }   
      break;
    case Ctlp_EX_c :
      if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){
        if (!Imc_ImcEvaluateEXApprox(imcInfo,ctlFormula, TRUE, FALSE)) return 0;
      }
      if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){
        if (!Imc_ImcEvaluateEXApprox(imcInfo,ctlFormula, FALSE, FALSE)) return 0;
      }
      break;

    case Ctlp_EU_c :
      if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){ 
        if (!Imc_ImcEvaluateEUApprox(imcInfo,ctlFormula,TRUE, FALSE)) return 0;
      }
      if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){
        if (!Imc_ImcEvaluateEUApprox(imcInfo,ctlFormula, FALSE, FALSE)) return 0;
      }
      break;

    case Ctlp_EG_c :
      if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){
        if (!Imc_ImcEvaluateEGApprox(imcInfo,ctlFormula,TRUE, FALSE)) return 0;
      }
      if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){
        if (!Imc_ImcEvaluateEGApprox(imcInfo,ctlFormula, FALSE, FALSE)) return 0;
      } 
      break;

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

  if (nodeInfo->upperDone && nodeInfo->lowerDone){
    if (!nodeInfo->isExact && mdd_equal_mod_care_set(nodeInfo->upperSat, 
         nodeInfo->lowerSat, imcInfo->modelCareStates)){ /* FIXED */
      nodeInfo->isExact = TRUE;
    }
  }

  return 1;
}

int
Imc_ImcEvaluateEXApprox(
  Imc_Info_t *imcInfo,
  Ctlp_Formula_t *formula,
  boolean isUpper,
  boolean isRecomputation)
{
  mdd_t *targetStates;
  Ctlp_Formula_t *leftChild;
  mdd_t *result = NIL(mdd_t);
  mdd_t *tempResult;
  mdd_t *localCareStates;
  mdd_t *globalCareStates;
  boolean useLocalCare = FALSE;
  Imc_NodeInfo_t *nodeInfo, *lNodeInfo;
  boolean isExact;
  
  globalCareStates = imcInfo->modelCareStates;

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    fprintf(vis_stdout, "** imc error : EX nodeinfo is not initilize.\n");
    return 0;
  }

  leftChild = Ctlp_FormulaReadLeftChild(formula);
  if (!st_lookup(imcInfo->nodeInfoTable, leftChild, &lNodeInfo)){
    fprintf(vis_stdout, "** imc error : EX left nodeinfo is not initilize.\n");
    return 0;
  }

  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){      
     if (isUpper){
      fprintf(vis_stdout, "IMC :  SAT(EX)+ computation start.\n");
    }else{
      fprintf(vis_stdout, "IMC :  SAT(EX)- computation start.\n");
    }
  }

  /*
   * If exact sat is already computed from other side of approximation,
   * use it.
   */
  if (nodeInfo->isExact){
    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){      
      if (isUpper){
        fprintf(vis_stdout, "IMC :  SAT(EX)+ computation end.\n");
      }else{
        fprintf(vis_stdout, "IMC :  SAT(EX)- computation end.\n");
      }
    }
    return 1;
  }


  /*
   * If this is not for recomputation, do general satisfying states computation.
   * Otherwise, compute the subset of the propagated goalset where the formula
   * satisfies.
   * Test if tighter satisfying don't care states(ASDC) can be used to reduce
   * transition sub-relations.
   */
  if (nodeInfo->upperSat != NIL(mdd_t)){
    localCareStates = mdd_and(nodeInfo->upperSat,globalCareStates, 1, 1); 
  }else{
    localCareStates = mdd_dup(globalCareStates);
  }

  if ((mdd_lequal(localCareStates,globalCareStates, 1, 1)) &&
      (!mdd_equal(localCareStates,globalCareStates))){
    useLocalCare = TRUE;
  }

  if (!isRecomputation){
    if (isUpper){
      targetStates = lNodeInfo->upperSat;
    }else{
      targetStates = lNodeInfo->lowerSat;
    }
  }else{
    targetStates = lNodeInfo->propagatedGoalSetTrue;
  }

  if (targetStates == NIL(mdd_t)) return 0;

  if ((isUpper)|| (isRecomputation)) 
    Imc_UpperSystemMinimize(imcInfo, localCareStates);
  else
    Imc_LowerSystemMinimize(imcInfo, localCareStates);  

  if ((isUpper) || (isRecomputation)){
    tempResult = Imc_ComputeUpperPreimage(imcInfo, localCareStates, targetStates, 
                                          &isExact);
  }else{
    tempResult = Imc_ComputeLowerPreimage(imcInfo, localCareStates, targetStates, 
                                          &isExact);
  }

  if (tempResult == NIL(mdd_t)) return 0;

  if ((imcInfo->verbosity == Imc_VerbosityMax_c) ||
      (imcInfo->verbosity == Imc_VerbosityMin_c)) {
    mdd_t *tmpMdd = mdd_and(tempResult, localCareStates, 1, 1 );
    double minterm = mdd_count_onset(imcInfo->mddMgr, tmpMdd, 
              imcInfo->systemInfo->psMddIdArray);
    if (isUpper){
      fprintf(vis_stdout, "IMC : |SAT(EX)+| = %.0f (%10g)\n", minterm, minterm);
    }else{
      fprintf(vis_stdout, "IMC : |SAT(EX)-| = %.0f (%10g)\n", minterm, minterm);
    }
    mdd_free(tmpMdd);
  }

  if (useLocalCare){
     result = mdd_and(tempResult, localCareStates, 1, 1); 
     mdd_free(tempResult);
     tempResult = bdd_minimize(result, globalCareStates);
     mdd_free(result);
     result = tempResult;
  }else{
     result = tempResult;
  }

  mdd_free(localCareStates);

  if (isRecomputation){
    tempResult = mdd_and(nodeInfo->goalSet, result, 1, 1);
    mdd_free(result);
    nodeInfo->propagatedGoalSetTrue = 
      mdd_or(nodeInfo->goalSetTrue, tempResult, 1, 1);
    mdd_free(tempResult);
    return 1;
  }

  if (isUpper){
    if (nodeInfo->upperSat != NIL(mdd_t)){
      mdd_free(nodeInfo->upperSat);
    }
    nodeInfo->upperSat = result;
    nodeInfo->upperDone = TRUE;
  }else{
    if (nodeInfo->lowerSat != NIL(mdd_t)){
      tempResult = mdd_or(nodeInfo->lowerSat, result, 1, 1);
      mdd_free(nodeInfo->lowerSat);
      mdd_free(result);
      result = tempResult;
    }
    nodeInfo->lowerSat = result;
    nodeInfo->lowerDone = TRUE;
  }

  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){      
    if (isUpper){
      fprintf(vis_stdout, "IMC :  SAT(EX)+ computation end.\n");
    }else{
      fprintf(vis_stdout, "IMC :  SAT(EX)- computation end.\n");
    }
  }

  if (lNodeInfo->isExact && isExact){
    nodeInfo->isExact = TRUE;
    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){
      if (isUpper){
        fprintf(vis_stdout, "IMC :  SAT(EX)+ computation is exact.\n");
      }else{
        fprintf(vis_stdout, "IMC :  SAT(EX)- computation is exact.\n");
      }
    }      
    if (isUpper){
      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
      nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat);
      nodeInfo->lowerDone = TRUE;
    }else{
      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
      nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat);
      nodeInfo->upperDone = TRUE;
    } 
  }else{
    nodeInfo->isExact = FALSE;
  }  

  return 1;
}

int
Imc_ImcEvaluateEUApprox(
  Imc_Info_t *imcInfo,
  Ctlp_Formula_t *formula,
  boolean isUpper,
  boolean isRecomputation)
{
  mdd_t *localCareStates;
  mdd_t *targetStates, *invariantStates;
  mdd_t *aMdd, *bMdd, *cMdd;
  mdd_t *result;
  mdd_t *tmpMdd1, *tmpMdd2;
  mdd_t * globalCareStates;
  double size1, size2;
  Ctlp_Formula_t *lFormula, *rFormula;
  Imc_NodeInfo_t *nodeInfo, *lNodeInfo, *rNodeInfo;
  boolean isExact, globalIsExact;

  globalIsExact = TRUE;
  globalCareStates = imcInfo->modelCareStates;
  lFormula = Ctlp_FormulaReadLeftChild(formula);
  rFormula = Ctlp_FormulaReadRightChild(formula);

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    fprintf(vis_stdout, "** imc error : EU nodeinfo is not initilize.\n");
    return 0;
  }
  if (!st_lookup(imcInfo->nodeInfoTable, lFormula, &lNodeInfo)){
    fprintf(vis_stdout, "** imc error : EU left nodeinfo is not initilize.\n");
    return 0;
  }
  if (!st_lookup(imcInfo->nodeInfoTable, rFormula, &rNodeInfo)){
    fprintf(vis_stdout, "** imc error : EU right nodeinfo is not initilize.\n");
    return 0;
  }

  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){      
    if (isUpper){
      fprintf(vis_stdout, "IMC :  SAT(EU)+ computation start.\n");
    }else{
      fprintf(vis_stdout, "IMC :  SAT(EU)- computation start.\n");
    }
  }

  /*
   * If exact sat is already computed from other side of approximation,
   * use it.
   */
  if (nodeInfo->isExact){
    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){      
      if (isUpper){
        fprintf(vis_stdout, "IMC :  SAT(EU)+ computation end.\n");
      }else{
        fprintf(vis_stdout, "IMC :  SAT(EU)- computation end.\n");
      }
    }
    return 1;
  }


  /*
   * Test if tighter satisfying don't care states(ASDC) can be used to reduce
   * transition sub-relations.
   */
  
  if (nodeInfo->upperSat != NIL(mdd_t)){
    localCareStates = mdd_and(nodeInfo->upperSat,globalCareStates, 1, 1); 
  }else{
    localCareStates = mdd_dup(globalCareStates);
  }

  if ((mdd_lequal(localCareStates,globalCareStates, 1, 1)) &&
      (!mdd_equal(localCareStates,globalCareStates))){
  }

  if (!isRecomputation){
    if (isUpper){
      if (nodeInfo->lowerSat != NIL(mdd_t)){
        targetStates = mdd_or(rNodeInfo->upperSat, nodeInfo->lowerSat, 1, 1);
      }else{
        targetStates = mdd_dup(rNodeInfo->upperSat);
      }
      invariantStates = lNodeInfo->upperSat;
    }else{
      targetStates = mdd_dup(rNodeInfo->lowerSat);
      invariantStates = lNodeInfo->lowerSat;
    }
  }else{
    targetStates = mdd_dup(rNodeInfo->propagatedGoalSetTrue);
    invariantStates = lNodeInfo->propagatedGoalSetTrue;    
  }

  result = targetStates;

  if ((isUpper) || (isRecomputation))
    Imc_UpperSystemMinimize(imcInfo, localCareStates);
  else
    Imc_LowerSystemMinimize(imcInfo, localCareStates);

  while (TRUE) { 

    if (isUpper){
      aMdd = Imc_ComputeUpperPreimage(imcInfo, localCareStates, 
                                      result, &isExact);      
    }else{
      aMdd = Imc_ComputeLowerPreimage(imcInfo, localCareStates, 
                                      result, &isExact);
    }
    if (aMdd == NIL(mdd_t)) return 0;

    globalIsExact = (globalIsExact && isExact);

    bMdd = mdd_and( aMdd, invariantStates, 1, 1 );
    mdd_free( aMdd );
    aMdd = mdd_and(bMdd, localCareStates, 1, 1);
    mdd_free(bMdd);
    bMdd = bdd_minimize(aMdd, globalCareStates);
    mdd_free(aMdd);
    cMdd = mdd_or(result, bMdd, 1, 1);
    mdd_free( bMdd );
    
    tmpMdd1 = mdd_and( result, globalCareStates, 1, 1 );
    tmpMdd2 = mdd_and( cMdd, globalCareStates, 1, 1 );
    if (mdd_equal(tmpMdd1, tmpMdd2)){
      mdd_free(cMdd);
      break;
    }else if (mdd_equal(tmpMdd2, localCareStates)){ 
      mdd_free(result);
      result = cMdd;     
      break;
    }else if (( imcInfo->verbosity == Imc_VerbosityMax_c ) ||
              (imcInfo->verbosity == Imc_VerbosityMin_c)) { 
      size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1,
                               imcInfo->systemInfo->psMddIdArray);
      size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2,
                               imcInfo->systemInfo->psMddIdArray);
      if (isUpper){
        fprintf(vis_stdout, "IMC : |SAT(EU)+| = %.0f (%10g)-> %.0f (%10g)\n", 
                size1, size1, size2, size2);
      }else{
        fprintf(vis_stdout, "IMC : |SAT(EU)-| = %.0f (%10g)-> %.0f (%10g)\n", 
                size1, size1, size2, size2);
      }
    }      
    mdd_free(tmpMdd1);
    mdd_free(tmpMdd2);

    mdd_free( result );
    result = bdd_minimize(cMdd, globalCareStates);
    mdd_free(cMdd);
  }

  if ((imcInfo->verbosity == Imc_VerbosityMax_c) ||
      (imcInfo->verbosity == Imc_VerbosityMin_c)) {
    size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1,
                             imcInfo->systemInfo->psMddIdArray);
    size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2,
                       imcInfo->systemInfo->psMddIdArray);    
    if (isUpper){
      fprintf(vis_stdout, "IMC : |SAT(EU)+| = %.0f (%10g)-> %.0f (%10g)\n", 
              size1, size1, size2, size2);
    }else{
      fprintf(vis_stdout, "IMC : |SAT(EU)-| = %.0f (%10g)-> %.0f (%10g)\n", 
              size1, size1, size2, size2);
    }
  }

  mdd_free(tmpMdd1);
  mdd_free(tmpMdd2);

  mdd_free(localCareStates);

  if (isRecomputation){
    tmpMdd1 = mdd_and(nodeInfo->goalSet, result, 1, 1);
    mdd_free(result);
    nodeInfo->propagatedGoalSetTrue = mdd_or(nodeInfo->goalSetTrue, tmpMdd1, 1, 1);
    mdd_free(tmpMdd1);
    return 1;
  }

  if (isUpper){
    if (nodeInfo->upperSat != NIL(mdd_t)){
      mdd_free(nodeInfo->upperSat);
    }
    nodeInfo->upperSat = result;
    nodeInfo->upperDone = TRUE;
  }else{
    if (nodeInfo->lowerSat != NIL(mdd_t)){
      tmpMdd1 = mdd_or(nodeInfo->lowerSat, result, 1, 1);
      mdd_free(nodeInfo->lowerSat);
      mdd_free(result);
      result = tmpMdd1;
    }
    nodeInfo->lowerSat = result;
    nodeInfo->lowerDone = TRUE;
  } 

  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){      
    if (isUpper){
      fprintf(vis_stdout, "IMC :  SAT(EU)+ computation end.\n");
    }else{
      fprintf(vis_stdout, "IMC :  SAT(EU)- computation end.\n");
    }
  }

  if (lNodeInfo->isExact && rNodeInfo->isExact && globalIsExact){
    nodeInfo->isExact = TRUE;
    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){
      if (isUpper){
        fprintf(vis_stdout, "IMC :  SAT(EU)+ computation is exact.\n");
      }else{
        fprintf(vis_stdout, "IMC :  SAT(EU)- computation is exact.\n");
      }
    }   
    if (isUpper){
      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
      nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat);
      nodeInfo->lowerDone = TRUE;
    }else{
      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
      nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat);
      nodeInfo->upperDone = TRUE;
    } 
  }else{
    nodeInfo->isExact = FALSE;
  } 

  return 1;
}

int
Imc_ImcEvaluateEGApprox( 
  Imc_Info_t *imcInfo,
  Ctlp_Formula_t *formula,
  boolean isUpper,
  boolean isRecomputation)
{
  mdd_t *Zmdd;
  mdd_t *bMdd;
  mdd_t *ZprimeMdd;
  mdd_t *tmpMdd1, *tmpMdd2;
  mdd_t *result;
  mdd_t *localCareStates;
  mdd_t *globalCareStates;
  mdd_t *invariantStates;
  double size1, size2;
  Ctlp_Formula_t *lFormula;
  Imc_NodeInfo_t *nodeInfo, *lNodeInfo;
  boolean isExact, globalIsExact;
  

  lFormula = Ctlp_FormulaReadLeftChild(formula);

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    fprintf(vis_stdout, "** imc error : EG nodeinfo is not initilize.\n");
    return 0;
  }
  if (!st_lookup(imcInfo->nodeInfoTable, lFormula, &lNodeInfo)){
    fprintf(vis_stdout, "** imc error : EG left nodeinfo is not initilize.\n");
    return 0;
  }

  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){      
    if (isUpper){
      fprintf(vis_stdout, "IMC :  SAT(EG)+ computation start.\n");
    }else{
      fprintf(vis_stdout, "IMC :  SAT(EG)- computation start.\n");
    }
  }

  /*
   * If exact sat is already computed from other side of approximation,
   * use it.
   */
  if (nodeInfo->isExact){
    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){      
      if (isUpper){
        fprintf(vis_stdout, "IMC :  SAT(EG)+ computation end.\n");
      }else{
        fprintf(vis_stdout, "IMC :  SAT(EG)- computation end.\n");
      }
    }
    return 1;
  }

  globalCareStates = imcInfo->modelCareStates;

  /*
   * Test if tighter satisfying don't care states(ASDC) can be used to reduce
   * transition sub-relations.
   */
  if (nodeInfo->upperSat != NIL(mdd_t)){ 
    localCareStates = mdd_and(nodeInfo->upperSat,globalCareStates, 1, 1); 
  }else{
    localCareStates = mdd_dup(globalCareStates);
  }

  if ((mdd_lequal(localCareStates,globalCareStates, 1, 1)) &&
      (!mdd_equal(localCareStates,globalCareStates))){
  }

  if (!isRecomputation){
    if (isUpper){
      if (nodeInfo->upperSat != NIL(mdd_t)){
        invariantStates = mdd_and(lNodeInfo->upperSat, nodeInfo->upperSat,1,1);
      }else{
        invariantStates = mdd_dup(lNodeInfo->upperSat);
      } 
    }else{
      if (nodeInfo->upperSat != NIL(mdd_t)){
        invariantStates = mdd_and(lNodeInfo->lowerSat, nodeInfo->upperSat,1,1);
      }else{
        invariantStates = mdd_dup(lNodeInfo->lowerSat);
      }
    }
  }else{
    invariantStates = mdd_dup(lNodeInfo->propagatedGoalSetTrue);
  }

  Zmdd = mdd_dup(invariantStates);
  ZprimeMdd = NIL(mdd_t);

  globalIsExact = TRUE;

  if ((isUpper) || (isRecomputation))
    Imc_UpperSystemMinimize(imcInfo, localCareStates);
  else
    Imc_LowerSystemMinimize(imcInfo, localCareStates);

  while (TRUE) {

    if (isUpper){
      bMdd = Imc_ComputeUpperPreimage(imcInfo, localCareStates, 
                                      Zmdd, &isExact);
    }else{
      bMdd = Imc_ComputeLowerPreimage(imcInfo, localCareStates, 
                                      Zmdd, &isExact);
    }
    if (bMdd == NIL(mdd_t)){
      mdd_free(invariantStates);
      mdd_free(Zmdd);
      if (ZprimeMdd !=NIL(mdd_t)) mdd_free(ZprimeMdd);
      return 0;
    }

    ZprimeMdd = mdd_and(Zmdd, bMdd, 1, 1);
    globalIsExact = (globalIsExact && isExact);

    mdd_free(bMdd);
    
    tmpMdd1 = mdd_and( Zmdd, globalCareStates, 1, 1 );
    tmpMdd2 = mdd_and( ZprimeMdd, localCareStates, 1, 1 );

    mdd_free(Zmdd);
    mdd_free(ZprimeMdd);

    if ((mdd_equal(tmpMdd1, tmpMdd2)) ||
        (mdd_is_tautology(tmpMdd2, 0))){
      break;
    }else if (( imcInfo->verbosity == Imc_VerbosityMax_c ) ||
              (imcInfo->verbosity == Imc_VerbosityMin_c)) {      
      size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1,
                               imcInfo->systemInfo->psMddIdArray);
      size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2,
                               imcInfo->systemInfo->psMddIdArray);
      if (isUpper){
        fprintf(vis_stdout, "IMC : |SAT(EG)+| = %.0f (%10g)-> %.0f (%10g)\n", 
                size1, size1, size2, size2);
      }else{
        fprintf(vis_stdout, "IMC : |SAT(EG)-| = %.0f (%10g)-> %.0f (%10g)\n", 
                size1, size1, size2, size2);
      }
    }

    mdd_free(tmpMdd1);
    Zmdd = bdd_minimize(tmpMdd2, globalCareStates);
    mdd_free(tmpMdd2);
  }
        
  if (( imcInfo->verbosity == Imc_VerbosityMax_c ) ||
      (imcInfo->verbosity == Imc_VerbosityMin_c)) {
    size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1,
                             imcInfo->systemInfo->psMddIdArray);
    size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2,
                             imcInfo->systemInfo->psMddIdArray);
    if (isUpper){
      fprintf(vis_stdout, "IMC : |SAT(EG)+| = %.0f (%10g)-> %.0f (%10g)\n", 
              size1, size1, size2, size2);
    }else{
      fprintf(vis_stdout, "IMC : |SAT(EG)-| = %.0f (%10g)-> %.0f (%10g)\n", 
              size1, size1, size2, size2);
    }
  }

  mdd_free(tmpMdd1);
  mdd_free(localCareStates);

  result = bdd_minimize(tmpMdd2, globalCareStates);
  mdd_free(tmpMdd2);

  if (isRecomputation){
    tmpMdd1 = mdd_and(nodeInfo->goalSet, result, 1, 1);
    mdd_free(result);
    nodeInfo->propagatedGoalSetTrue = mdd_or(nodeInfo->goalSetTrue,tmpMdd1,1,1);
    mdd_free(tmpMdd1);
    return 1;
  }

  mdd_free(invariantStates);

  if (isUpper){
    if (nodeInfo->upperSat != NIL(mdd_t)){
      mdd_free(nodeInfo->upperSat);
    }
    nodeInfo->upperSat = result;
    nodeInfo->upperDone = TRUE;
  }else{
    if (nodeInfo->lowerSat != NIL(mdd_t)){
      tmpMdd1 = mdd_or(nodeInfo->lowerSat, result, 1, 1);
      mdd_free(nodeInfo->lowerSat);
      mdd_free(result);
      result = bdd_minimize(tmpMdd1, globalCareStates);
      mdd_free(tmpMdd1);
    }
    nodeInfo->lowerSat = result;
    nodeInfo->lowerDone = TRUE;
  } 

  if ( imcInfo->verbosity == Imc_VerbosityMax_c ){      
    if (isUpper){
      fprintf(vis_stdout, "IMC :  SAT(EG)+ computation end.\n");
    }else{
      fprintf(vis_stdout, "IMC :  SAT(EG)- computation end.\n");
    }
  }

  if (lNodeInfo->isExact && globalIsExact){
    nodeInfo->isExact = TRUE;
    if ( imcInfo->verbosity == Imc_VerbosityMax_c ){
      if (isUpper){
        fprintf(vis_stdout, "IMC :  SAT(EG)+ computation is exact.\n");
      }else{
        fprintf(vis_stdout, "IMC :  SAT(EG)- computation is exact.\n");
      }
    }    
    if (isUpper){
      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
      nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat);
      nodeInfo->lowerDone = TRUE;
    }else{
      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
      nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat);
      nodeInfo->upperDone = TRUE;
    } 
  }else{
    nodeInfo->isExact = FALSE;
  } 

  return 1;
}

mdd_t *
Imc_ComputeUpperPreimage(
  Imc_Info_t *imcInfo,
  mdd_t *rangeCareStates,
  mdd_t *targetStates,
  boolean *isExact)
{
  if (imcInfo->upperMethod == Imc_UpperExistentialQuantification_c){
    return Imc_ComputeApproxPreimageByQuantification(imcInfo, rangeCareStates,
             targetStates, isExact, FALSE);
  }

  return NIL(mdd_t);
}


mdd_t *
Imc_ComputeApproxPreimageByQuantification(
  Imc_Info_t *imcInfo, 
  mdd_t *rangeCareStates, 
  mdd_t *targetStates,
  boolean *isExact,
  boolean computeLower)
{
  int i;
  int psMddId;
  double orgSize, newSize;
  mdd_t *result;
  mdd_t *nextTarget;
  mdd_t *reducedTarget;
  mdd_t *tempMdd;
  mdd_t *reducedTargetInCare;
  mdd_t *targetInCare;
  array_t *supportArray;

  *isExact = TRUE;
  if (mdd_is_tautology(targetStates, 0)){
    return mdd_zero(imcInfo->mddMgr);
  }

  supportArray = mdd_get_support(imcInfo->mddMgr, targetStates);

  for(i=0;i<array_n(supportArray);i++){
    psMddId = array_fetch(int, supportArray, i);
    if (st_is_member(imcInfo->systemInfo->excludedPsMddIdTable, 
                     (char *)(long)psMddId)){
      *isExact = FALSE;
      break;
    }
  }
  array_free(supportArray);
 
  if (array_n(imcInfo->systemInfo->excludedPsMddId) >0){
    if (!computeLower){
      reducedTarget = mdd_smooth(imcInfo->mddMgr, targetStates, 
                               imcInfo->systemInfo->excludedPsMddId);
    }else{
      reducedTarget = mdd_consensus(imcInfo->mddMgr, targetStates, 
                               imcInfo->systemInfo->excludedPsMddId);
    }
    if ((mdd_is_tautology(reducedTarget,1)) || (mdd_is_tautology(reducedTarget,0))){
      return reducedTarget;
    }
  }else{
    reducedTarget = mdd_dup(targetStates);
  }

  if (imcInfo->verbosity == Imc_VerbosityMax_c){
    targetInCare = mdd_and(targetStates, imcInfo->modelCareStates, 1, 1);
    reducedTargetInCare = mdd_and(reducedTarget, imcInfo->modelCareStates, 1, 1);
    orgSize = mdd_count_onset(imcInfo->mddMgr, targetInCare,
                        imcInfo->systemInfo->psMddIdArray);
    newSize = mdd_count_onset(imcInfo->mddMgr, reducedTargetInCare,
                          imcInfo->systemInfo->psMddIdArray);
    if (!computeLower){
      fprintf(vis_stdout, "IMC : Upper Approximation    |S| = %.0f (%10g)-> %.0f (%10g)\n",
              orgSize, orgSize, newSize, newSize);
    }else{
      fprintf(vis_stdout, "IMC : Lower Approximation    |S| = %.0f (%10g)-> %.0f (%10g)\n",
              orgSize, orgSize, newSize, newSize);
    }
    mdd_free(targetInCare);
    mdd_free(reducedTargetInCare);
  }

  nextTarget = mdd_substitute(imcInfo->mddMgr, reducedTarget,
                              imcInfo->systemInfo->psMddIdArray,
                              imcInfo->systemInfo->nsMddIdArray);

  mdd_free(reducedTarget);

  if (!computeLower){
    if (imcInfo->upperSystemInfo->bwdMinimizedRealationArray == NIL(array_t)){
      result = Imc_ProductAbstract(imcInfo->mddMgr, 
                                   imcInfo->upperSystemInfo->bwdRealationArray,
                                   imcInfo->upperSystemInfo->bwdSmoothVarsArray,
                                   nextTarget);
    }else{
      result = Imc_ProductAbstract(imcInfo->mddMgr, 
                                   imcInfo->upperSystemInfo->bwdMinimizedRealationArray,
                                   imcInfo->upperSystemInfo->bwdSmoothVarsArray,
                                   nextTarget);
    }
  }else{
    if (imcInfo->lowerSystemInfo->bwdMinimizedRealationArray == NIL(array_t)){
      result = Imc_ProductAbstract(imcInfo->mddMgr, 
                                   imcInfo->lowerSystemInfo->bwdRealationArray,
                                   imcInfo->lowerSystemInfo->bwdSmoothVarsArray,
                                   nextTarget);
    }else{
      result = Imc_ProductAbstract(imcInfo->mddMgr, 
                                   imcInfo->lowerSystemInfo->bwdMinimizedRealationArray,
                                   imcInfo->lowerSystemInfo->bwdSmoothVarsArray,
                                   nextTarget);
    }
  }

  mdd_free(nextTarget);

  if (imcInfo->verbosity == Imc_VerbosityMax_c){
    double exactSize, approxSize;
    tempMdd = mdd_and(result, rangeCareStates, 1, 1);  
    approxSize = mdd_count_onset(imcInfo->mddMgr, result,
                    imcInfo->systemInfo->psMddIdArray);
    exactSize = mdd_count_onset(imcInfo->mddMgr, tempMdd,
                      imcInfo->systemInfo->psMddIdArray);
    mdd_free(tempMdd);
    if (!computeLower){
      fprintf(vis_stdout, "IMC : Upper Preimage      |S+DC| = %.0f (%10g)\n",
              approxSize, approxSize);
      fprintf(vis_stdout, "IMC : Upper Preimage         |S| = %.0f (%10g)\n",
              exactSize, exactSize);
    }else{
      fprintf(vis_stdout, "IMC : Lower Preimage      |S+DC| = %.0f (%10g)\n",
              approxSize, approxSize);
      fprintf(vis_stdout, "IMC : Lower Preimage         |S| = %.0f (%10g)\n",
              exactSize, exactSize);
    } 
  }

  /* 
   * If preimage is zero, don't need compute again
   */
  if (mdd_is_tautology(result,0)){
    *isExact = TRUE;
  }

  return result;
}

mdd_t *
Imc_ComputeLowerPreimage(
  Imc_Info_t *imcInfo,
  mdd_t *rangeCareStates,
  mdd_t *targetStates,
  boolean *isExact)
{
  if (imcInfo->lowerMethod == Imc_LowerSubsetTR_c){
    return Imc_ComputeLowerPreimageBySubsetTR(imcInfo, rangeCareStates,
                                                targetStates, isExact);
  }else if (imcInfo->lowerMethod == Imc_LowerUniversalQuantification_c){
    return Imc_ComputeApproxPreimageByQuantification(imcInfo, rangeCareStates,
             targetStates, isExact, TRUE);
  }

  return NIL(mdd_t);
}


mdd_t *
Imc_ComputeLowerPreimageBySubsetTR(
  Imc_Info_t *imcInfo,
  mdd_t *rangeCareStates,
  mdd_t *targetStates,
  boolean *isExact)
{
  mdd_t *tempMdd, *result;
  mdd_t *toStates;

  *isExact = TRUE;

  if (mdd_is_tautology(targetStates,0)){
    return mdd_zero(imcInfo->mddMgr);
  }

  if (mdd_is_tautology(targetStates, 1)){
    return mdd_one(imcInfo->mddMgr);
  }

  /*
   * T_i is T_i for all included latches.
   */

  /*arrayOfMdd = array_alloc(mdd_t *, 0); never used, I guess. Chao Wang*/

  toStates = mdd_substitute(imcInfo->mddMgr, targetStates,
                            imcInfo->systemInfo->psMddIdArray,
                            imcInfo->systemInfo->nsMddIdArray);

  /* Not works with partitioned transition relation 
  supportArray = mdd_get_support(imcInfo->mddMgr, targetStates);

  for(i=0;i<array_n(supportArray);i++){
    psMddId = array_fetch(int, supportArray,i);

    if (st_is_member(imcInfo->systemInfo->excludedPsMddIdTable, 
        (char *)(long)psMddId)){
      *isExact = FALSE;
    }
  }
  array_free(supportArray);
  */
  if (st_count(imcInfo->systemInfo->excludedPsMddIdTable)>0){
    *isExact = FALSE;
  }

  if (imcInfo->lowerSystemInfo->bwdMinimizedRealationArray == NIL(array_t)){
    result = Imc_ProductAbstract(imcInfo->mddMgr,
                                 imcInfo->lowerSystemInfo->bwdRealationArray,
                                 imcInfo->lowerSystemInfo->bwdSmoothVarsArray,
                                 toStates);
  }else{
    result = Imc_ProductAbstract(imcInfo->mddMgr,
                                 imcInfo->lowerSystemInfo->bwdMinimizedRealationArray,
                                 imcInfo->lowerSystemInfo->bwdSmoothVarsArray,
                                 toStates);
  }

  mdd_free(toStates);

  if (imcInfo->verbosity == Imc_VerbosityMax_c){
    double exactSize, approxSize;
    tempMdd = mdd_and(result, rangeCareStates, 1, 1);  
    approxSize = mdd_count_onset(imcInfo->mddMgr, result,
                    imcInfo->systemInfo->psMddIdArray);
    exactSize = mdd_count_onset(imcInfo->mddMgr, tempMdd,
                      imcInfo->systemInfo->psMddIdArray);
    mdd_free(tempMdd);
    fprintf(vis_stdout, "IMC : Lower Preimage      |S+DC| = %.0f (%10g)\n",
            approxSize, approxSize);
    fprintf(vis_stdout, "IMC : Lower Preimage         |S| = %.0f (%10g)\n",
            exactSize, exactSize);
  }

  return result;
}

mdd_t *
Imc_ProductAbstract(
  mdd_manager *mddMgr,
  array_t *relationArray,
  array_t *smoothVarsMddIdArray,
  mdd_t *toStates)
{
  int i;
  mdd_t *product, *tempProd;
  mdd_t *singleTR;
  array_t *smoothVars;

  product = mdd_dup(toStates);

  for(i=0;i<array_n(relationArray);i++){
    singleTR = array_fetch(mdd_t *, relationArray, i);
    smoothVars = array_fetch(array_t*, smoothVarsMddIdArray, i);
    if (array_n(smoothVars) == 0){
      tempProd = mdd_and(product, singleTR, 1, 1);
    }else{
      tempProd = bdd_and_smooth(product, singleTR, smoothVars);
    }
    mdd_free(product);
    product = tempProd;
  }
  if (i < array_n(smoothVarsMddIdArray)) {
    smoothVars = array_fetch(array_t*, smoothVarsMddIdArray, i);
    tempProd = bdd_smooth(product, smoothVars);
    mdd_free(product);
    product = tempProd;
  }

  return product;  
}


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

array_t *
ImcCreateScheduleArray(
  Ntk_Network_t         *network,
  Ctlp_Formula_t        *formula,
  boolean               dynamicIncrease,
  Imc_RefineMethod      refine,
  int                   verbosity,
  int                   incrementalSize,
  Part_CMethod          correlationMethod)
{
  array_t               *partitionArray;
  Part_Subsystem_t      *partitionSubsystem;
  Part_SubsystemInfo_t  *subsystemInfo; 
  st_table              *latchNameTable;
  st_table              *latchNameTableSum, *latchNameTableSumCopy;
  int                   i;
  char                  *flagValue;
  st_generator          *stGen;
  char                  *name;
  array_t               *ctlArray;
  double                affinityFactor;
  array_t               *scheduleArray;
  boolean               dynamicAndDependency;
  array_t               *tempArray, *tempArray2;
  int                   count;

  /* affinity factor to decompose state space */
  flagValue = Cmd_FlagReadByName("part_group_affinity_factor");
  if(flagValue != NIL(char)){
    affinityFactor = atof(flagValue); 
  }
  else{
    /* default value */
    affinityFactor = 0.5; 
  }

  if (refine == Imc_RefineSort_c) dynamicAndDependency = TRUE;
  else dynamicAndDependency = FALSE;

  /* 
   * Obtain submachines as array. 
   * The first sub-system includes variables in CTL formulas and other
   * latches are groupted in the same way as Part_PartCreateSubsystems()
   */
  ctlArray = array_alloc(Ctlp_Formula_t *, 1);
  subsystemInfo = Part_PartitionSubsystemInfoInit(network);
  Part_PartitionSubsystemInfoSetBound(subsystemInfo, incrementalSize);
  Part_PartitionSubsystemInfoSetVerbosity(subsystemInfo, verbosity);
  Part_PartitionSubsystemInfoSetCorrelationMethod(subsystemInfo,
    correlationMethod); 
  Part_PartitionSubsystemInfoSetAffinityFactor(subsystemInfo, affinityFactor);
  array_insert(Ctlp_Formula_t *, ctlArray, 0, formula);

  partitionArray = Part_PartCreateSubsystemsWithCTL(subsystemInfo,
                   ctlArray, NIL(array_t), dynamicIncrease,dynamicAndDependency);
  Part_PartitionSubsystemInfoFree(subsystemInfo);
  array_free(ctlArray);
  scheduleArray = array_alloc(st_table *, 0);


  /* 
   * For each partitioned submachines build an FSM. 
   */
  latchNameTableSum = st_init_table(strcmp, st_strhash);
  if (!dynamicAndDependency){
    for (i=0;i<array_n(partitionArray);i++){
      partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, i);
      if (partitionSubsystem != NIL(Part_Subsystem_t)) {
        latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
        st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
          if (!st_lookup(latchNameTableSum, name, NIL(char *))){ 
            st_insert(latchNameTableSum, name, NIL(char));
          }
        }
        Part_PartitionSubsystemFree(partitionSubsystem);
      } 
      latchNameTableSumCopy = st_copy(latchNameTableSum);
      array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
    }
  }else{
    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 0);
    latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
    st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
      st_insert(latchNameTableSum, name, NIL(char));
    }
    latchNameTableSumCopy = st_copy(latchNameTableSum);
    array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
    Part_PartitionSubsystemFree(partitionSubsystem);

    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 1);
    tempArray = array_alloc(char *, 0);    
    if (partitionSubsystem != NIL(Part_Subsystem_t)){
      latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
      st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
        array_insert_last(char *, tempArray, name);
      }
      array_sort(tempArray, stringCompare);
      Part_PartitionSubsystemFree(partitionSubsystem);
    }
    
    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 2);
    tempArray2 = array_alloc(char *, 0);
    if (partitionSubsystem != NIL(Part_Subsystem_t)) {
      latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
      st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
        array_insert_last(char *, tempArray2, name);
      }
      array_sort(tempArray2, stringCompare);
      Part_PartitionSubsystemFree(partitionSubsystem);
    }

    array_append(tempArray, tempArray2);
    array_free(tempArray2);

    count = 0;
    arrayForEachItem(char *, tempArray, i, name){   
      if (!st_lookup(latchNameTableSum, name, NIL(char *))){ 
        st_insert(latchNameTableSum, (char *)name, (char *)0);
        count++;
      }
      if ((count == incrementalSize) && (i < array_n(tempArray)-1)){
        latchNameTableSumCopy = st_copy(latchNameTableSum);
        array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
        count = 0;
      }
    }
    array_free(tempArray);
    latchNameTableSumCopy = st_copy(latchNameTableSum);
    array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
  }

  array_free(partitionArray);
  st_free_table(latchNameTableSum);

  return scheduleArray;
}


int
ImcModelCheckAtomicFormula(
  Imc_Info_t *imcInfo, 
  Ctlp_Formula_t *formula)
{
  mdd_t * resultMdd;
  mdd_t *tmpMdd;
  Fsm_Fsm_t *modelFsm = imcInfo->globalFsm;
  Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm );
  char *nodeNameString = Ctlp_FormulaReadVariableName( formula );
  char *nodeValueString = Ctlp_FormulaReadValueName( formula );
  Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
  Var_Variable_t *nodeVar;
  int nodeValue;
  graph_t *modelPartition;
  vertex_t *partitionVertex;
  Mvf_Function_t *MVF;
  Imc_NodeInfo_t *nodeInfo;

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    fprintf(vis_stdout, "** imc error : Atomic nodeinfo is not initilize.\n");
    return 0;
  }

  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 );
  }
  else {
    MVF = Part_VertexReadFunction( partitionVertex );
    tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue );
    resultMdd = mdd_dup( tmpMdd );
  }

  tmpMdd = bdd_minimize(resultMdd, imcInfo->modelCareStates);
  mdd_free(resultMdd);
  resultMdd = tmpMdd;

  nodeInfo->upperSat = resultMdd;
  nodeInfo->lowerSat = mdd_dup(resultMdd);
  nodeInfo->upperDone = TRUE;
  nodeInfo->lowerDone = TRUE;
  nodeInfo->isExact = TRUE;
  return 1;  
}

int
ImcModelCheckTrueFalseFormula(
  Imc_Info_t *imcInfo, 
  Ctlp_Formula_t *formula,
  boolean isTrue)
{
  mdd_t *resultMdd;
  Imc_NodeInfo_t *nodeInfo;

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    fprintf(vis_stdout, "** imc error : TRUE or FALSE nodeinfo is not initilize.\n");
    return 0;
  }

  /*
   * Already computed, then return. 
   */
  if (nodeInfo->isExact) return 1;

  if (isTrue)
    resultMdd = mdd_one(imcInfo->mddMgr);
  else
    resultMdd = mdd_zero(imcInfo->mddMgr);

  nodeInfo->upperSat = resultMdd;
  nodeInfo->lowerSat = mdd_dup(resultMdd);  
  nodeInfo->upperDone = TRUE;
  nodeInfo->lowerDone = TRUE;
  nodeInfo->isExact = TRUE;
  return 1;
}

int
ImcModelCheckNotFormula(
  Imc_Info_t *imcInfo, 
  Ctlp_Formula_t *formula,
  boolean isUpper
  )
{
  mdd_t *upperSAT, *lowerSAT;
  Ctlp_Formula_t *leftChild;
  Imc_NodeInfo_t *nodeInfo, *leftNodeInfo;

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    return 0;
  }


  leftChild = Ctlp_FormulaReadLeftChild(formula);
  if (!st_lookup(imcInfo->nodeInfoTable, leftChild, &leftNodeInfo)){
    fprintf(vis_stdout, "** imc error : NOT nodeinfo is not initilize.\n");
    return 0;
  }


  if (isUpper){
    if  (leftNodeInfo->lowerSat == NIL(mdd_t)){
      return 0;
    }else{
      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
      upperSAT = mdd_not(leftNodeInfo->lowerSat);
      nodeInfo->upperSat = upperSAT;
      nodeInfo->upperDone = TRUE;
    }
  }else{
    if  (leftNodeInfo->upperSat == NIL(mdd_t)){
      return 0;
    }else{
      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
      lowerSAT = mdd_not(leftNodeInfo->upperSat);
      nodeInfo->lowerSat = lowerSAT;
      nodeInfo->lowerDone = TRUE;
    }
  }

  if (leftNodeInfo->isExact){
    nodeInfo->isExact = TRUE;
    if (isUpper){
      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
      nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat);
      nodeInfo->lowerDone = TRUE;
    }else{
      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
      nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat);
      nodeInfo->upperDone = TRUE;
    }
  }

  return 1;
}

int
ImcModelCheckAndFormula(
  Imc_Info_t *imcInfo, 
  Ctlp_Formula_t *formula,
  boolean isUpper)
{
  mdd_t *tmpMdd;
  mdd_t *upperSat, *lowerSat;
  Ctlp_Formula_t *leftChild, *rightChild;
  Imc_NodeInfo_t *nodeInfo, *leftNodeInfo, *rightNodeInfo;

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    return 0;
  }

  /*
   * Already computed, then return. 
   */
  if (nodeInfo->isExact) return 1;

  leftChild = Ctlp_FormulaReadLeftChild(formula);
  rightChild = Ctlp_FormulaReadRightChild(formula);
  if (!st_lookup(imcInfo->nodeInfoTable, leftChild, &leftNodeInfo)){
    fprintf(vis_stdout, "** imc error : AND left nodeinfo is not initilize.\n");
    return 0;
  }
  if (!st_lookup(imcInfo->nodeInfoTable, rightChild, &rightNodeInfo)){
    fprintf(vis_stdout, "** imc error : AND right nodeinfo is not initilize.\n");
    return 0;
  } 

  /*
   * Already computed, then return. 
   */
  if (isUpper){
    if ((leftNodeInfo->upperSat == NIL(mdd_t))||
        (rightNodeInfo->upperSat == NIL(mdd_t))){
      fprintf(vis_stdout, "** imc error : AND child nodeinfo->upperSat is not computed.\n");
      return 0;
    }else{
      tmpMdd = mdd_and(leftNodeInfo->upperSat,rightNodeInfo->upperSat, 1, 1);
      upperSat = bdd_minimize(tmpMdd, imcInfo->modelCareStates);
      mdd_free(tmpMdd);
      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
      nodeInfo->upperSat = upperSat;
      nodeInfo->upperDone = TRUE;
    }
  }else{
    if ((leftNodeInfo->lowerSat == NIL(mdd_t))||
        (rightNodeInfo->lowerSat == NIL(mdd_t))){
      fprintf(vis_stdout, "** imc error : AND child nodeinfo->lowerSat is not computed.\n");
      return 0;
    }else{
      tmpMdd = mdd_and(leftNodeInfo->lowerSat,rightNodeInfo->lowerSat, 1, 1);
      
      lowerSat = bdd_minimize(tmpMdd, imcInfo->modelCareStates);
      mdd_free(tmpMdd);
      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
      nodeInfo->lowerSat = lowerSat;
      nodeInfo->lowerDone = TRUE;
    }
  }

  if ((leftNodeInfo->isExact) && (rightNodeInfo->isExact)){
    nodeInfo->isExact = TRUE;
    if (isUpper){
      if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat);
      nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat);
      nodeInfo->lowerDone = TRUE;
    }else{
      if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat);
      nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat);
      nodeInfo->upperDone = TRUE;
    }
  }

  return 1;
}

void
ImcPrintLatchInApproxSystem(
  Imc_Info_t *imcInfo)
{
  int i, index;
  char *name;
  array_t *includedLatchIndex = imcInfo->systemInfo->includedLatchIndex;

  fprintf(vis_stdout, "Latches in approximate system\n");
  fprintf(vis_stdout, "-----------------------------\n");

  for(i=0;i<array_n(includedLatchIndex);i++){
    index = array_fetch(int,includedLatchIndex,i);
    name = array_fetch(char *, imcInfo->systemInfo->latchNameArray, index);
    fprintf(vis_stdout, "%s\n", name);
  }
}

void
ImcNodeInfoTableFree(
  st_table *nodeInfoTable)
{
  Ctlp_Formula_t *formula;
  Imc_NodeInfo_t *nodeInfo;
  st_generator *stGen;

  st_foreach_item(nodeInfoTable, stGen, &formula, &nodeInfo){
    Imc_NodeInfoFree(nodeInfo);
  }

  st_free_table(nodeInfoTable);
}

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

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