src/restr/restrRestructure.c

Go to the documentation of this file.

#include "restrInt.h"

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


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


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

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
extern int restrCreatedPart;
extern int restrCreatedFsm;
extern boolean restrVerbose;

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


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

static array_t * BuildFunctions(graph_t *partition, array_t *rootNames);
static bdd_node ** AddPowerSolve(bdd_manager *mgr, bdd_node *bddTr, bdd_node *init, bdd_node **x, bdd_node **y, bdd_node **pi, st_table *inputProb, int nVars, int nPi);
static bdd_node * PerformRestructure(bdd_manager *ddManager, bdd_node *prunedTR, bdd_node *equivRel, bdd_node *reachable, bdd_node *initBdd, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, st_table *inputProb, int nVars, int nPi, RestructureHeuristic heuristic, boolean equivClasses, array_t **outBdds, bdd_node **newInit, bdd_node **stateProbs);
static st_table * CreateNameToMvfTable(bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray);
static st_table * CreateCareTable(Ntk_Network_t *network, mdd_t *reachMdd);
static enum st_retval StMvfFree(char *key, char *value, char *arg);
static void CountEquivalentClasses(bdd_manager *ddManager, bdd_node *equivRel, bdd_node *initBdd, bdd_node **xVars, bdd_node **uVars, int nVars);
static array_t * GetBddArrayFromMvfArray(array_t *mvfArray);
static bdd_node * DoMarkovPowerAnalysis(bdd_manager *ddManager, bdd_node *prunedTR, bdd_node *initBdd, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, st_table *inputProb, int nVars, int nPi);
static array_t * ExtractTransitionFuns(bdd_manager *ddManager, bdd_node *finalTR, bdd_node **yVars, int nVars);
static array_t * GetBddArrayFromNameArray(Fsm_Fsm_t *fsm, array_t *nameArray);
static void ExpandReachableSet(bdd_manager *ddManager, bdd_node **reachable, bdd_node *equivRel, bdd_node **xVars, bdd_node **uVars, int nVars);
static graph_t * CreateNewPartition(Ntk_Network_t *network, bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray);
static Fsm_Fsm_t * CreateNewFsm(Ntk_Network_t *network, graph_t *partition, bdd_manager *ddManager, bdd_node *finalTR, bdd_node *initBdd, bdd_node *reachable, bdd_node *stateProbs, bdd_node **xVars, bdd_node **yVars, bdd_node **piVars, st_table *inputProb, int nVars, int nPi);

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

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

int
RestrCommandRestructureFsm(
  Fsm_Fsm_t *fsm,                          
  RestructureHeuristic heuristic,
  char *orderFileName,
  boolean equivClasses,
  boolean nonReachEquiv,
  boolean eqvMethod,
  st_table *inputProb,
  Synth_InfoData_t *synthInfo)
{

  graph_t *partition;
  Ntk_Network_t *network1;
  bdd_manager *ddManager;

  array_t *outputArray, *tranFunArray;
  array_t *outBdds, *nextBdds;
  array_t *tranRelationPair;
  array_t *newStateVars;

  st_table *careTable;

  int i;
  int nVars, nPi;
  int noRestruct = 0;
  boolean status;

  bdd_node *Lambda, *productTranRel, *prunedTR, *initialTR;
  bdd_node *equivRel;
  bdd_node *stateProbs;
  bdd_node *finalTR = NIL(bdd_node);
  bdd_node **xVars,**yVars,**uVars,**vVars;
  bdd_node **piVars;
  bdd_node *ddTemp, *reachable, *initBdd;
  bdd_node *newInit;

  mdd_t *reachStates, *mddTemp;
  mdd_t *careMdd;

  FILE *outFile;

  network1 = Fsm_FsmReadNetwork(fsm);
  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network1);

  /* Get the bdd_node for primary, present and next state variables.*/
  piVars = RestrBddNodeArrayFromIdArray(ddManager, 
                                        Fsm_FsmReadInputVars(fsm));
  xVars = RestrBddNodeArrayFromIdArray(ddManager, 
                                       Fsm_FsmReadPresentStateVars(fsm));
  yVars = RestrBddNodeArrayFromIdArray(ddManager,
                                       Fsm_FsmReadNextStateVars(fsm));
  /* Create new state variables for duplicate machine. */
  newStateVars = RestrCreateNewStateVars(network1, ddManager,xVars,yVars);
  uVars = RestrBddNodeArrayFromIdArray(ddManager,
                                       array_fetch(array_t *, 
                                                   newStateVars, 0));
  vVars = RestrBddNodeArrayFromIdArray(ddManager,
                                       array_fetch(array_t *, 
                                                   newStateVars, 1));

  /* Free memory: Delete the id array for new state variables.*/
  array_free(array_fetch(array_t *,newStateVars,0));
  array_free(array_fetch(array_t *,newStateVars,1));
  array_free(newStateVars);

  /* outputArray is the list of primary outputs. It is my responsibility to
  free it later. Both outputArray and tranFunArray are char * arrays.  Get the
  BDDs for output functions and transition functions.  Duplicate functions are
  returned.*/

  /* tranFunArray should not be freed */
  outputArray = RestrGetOutputArray(network1);
  tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
  outBdds = GetBddArrayFromNameArray(fsm,outputArray);
  nextBdds = GetBddArrayFromNameArray(fsm,tranFunArray);

  nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
  nPi = array_n(Fsm_FsmReadInputVars(fsm));

  /* Compute Lambda = AND (out1 xnor out1$NTK2) and Transition relation.
   out1$NTK2 is the corresponding primary output (of output1) in the duplicate
   machine.*/
  if (restrVerbose) {
    fprintf(vis_stdout,"** restr info: Computing product output ... ");
  }
  Lambda = RestrCreateProductOutput(ddManager,outBdds,xVars, uVars, nVars);
  if (restrVerbose) {
    fprintf(vis_stdout,"Done.\n");
  }

  if (restrVerbose) {
    fprintf(vis_stdout,"** restr info: Computing TR of product machine ... ");
  }
  /* Compute the transition relation for both the single FSM and the product
     machine.  tranRelationPair[0] is the TR of single FSM and
     tranRelationPair[1] is the TR of product machine.  
     TR(x,w,y) = \prod_{i=0}^{i=n-1} (y_i \equiv f_i(w,x))
     productTR(x,u,w,y,v) = TR(x,w,y) * TR(u,w,v) */
  tranRelationPair = RestrComputeTRWithIds(ddManager,nextBdds,xVars, yVars,
                                           uVars,vVars,nVars);
  if (restrVerbose) {
    fprintf(vis_stdout,"Done.\n");
  }

  productTranRel = array_fetch(bdd_node *,tranRelationPair,1);

  /* Compute the state equivalence relation for the FSM */
  /* The support of equivRel is xVars and uVars. */
  if (restrVerbose) {
    fprintf(vis_stdout,"** restr info: Computing the equivalence relation ... ");
  }

  if (eqvMethod) {
    equivRel = RestrComputeEquivRelationUsingCofactors(ddManager,Lambda,
                                                       productTranRel,
                                                       xVars, yVars, uVars,
                                                       vVars, piVars,
                                                       nVars, nPi,
                                                       restrVerbose);
    bdd_recursive_deref(ddManager,Lambda);
  } else {
    equivRel = RestrGetEquivRelation(ddManager,Lambda,productTranRel,
                                     xVars,yVars,uVars,vVars,
                                     piVars,nVars,nPi,restrVerbose);
    bdd_recursive_deref(ddManager,Lambda);
  }
  if (restrVerbose) {
    fprintf(vis_stdout,"Done.\n");
  }
  /* Delete the product transition relation, as we no longer need it. */
  bdd_recursive_deref(ddManager,productTranRel);

  /* Compute the initial states */
  mddTemp = Fsm_FsmComputeInitialStates(fsm);
  initBdd = bdd_extract_node_as_is(mddTemp);
  bdd_ref(initBdd);
  mdd_free(mddTemp);

  /* Compute the reachable states. */
  reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
                                              Fsm_Rch_Default_c,0,0,
                                              NIL(array_t),FALSE, NIL(array_t));

  reachable = bdd_extract_node_as_is(reachStates);
  bdd_ref(reachable);
  mdd_free(reachStates);

  /* Check to see if there are any usable equivalence classes */
  if (bdd_count_minterm(ddManager,equivRel,2*nVars) == pow(2.0,nVars)) {
    fprintf(vis_stdout,"** restr info: Number of equivalence classes equals ");
    fprintf(vis_stdout,"number of possible states. \n");
    fprintf(vis_stdout,"** restr info: Restructuring will not help.\n");
    fprintf(vis_stdout,"** restr info: Proceeding with synthesis.\n");
    bdd_recursive_deref(ddManager,equivRel);
    /* Do not perform restructuring */
    noRestruct = 1;
  }

  /* Expand the reachable set R(x) to include those states which are equivalent
   to R(x) but unreachable. */
  if(nonReachEquiv && !noRestruct) {
    ExpandReachableSet(ddManager,&reachable,equivRel,xVars,uVars,nVars);
  }

  if (noRestruct) {
    /* Only synthesize the network */
    bdd_recursive_deref(ddManager,equivRel);
    bdd_recursive_deref(ddManager,
                        array_fetch(bdd_node *,tranRelationPair,0));
    array_free(tranRelationPair);
  } else {
    /* Constrain the original TR */
    initialTR = array_fetch(bdd_node *, tranRelationPair, 0);
    /* bdd_ref(prunedTR = bdd_bdd_and(ddManager,initialTR,reachable)); */
    bdd_ref(prunedTR = initialTR);
    bdd_recursive_deref(ddManager,initialTR);
    array_free(tranRelationPair);

    finalTR = PerformRestructure(ddManager,prunedTR,equivRel,reachable,
                                   initBdd,piVars,xVars,yVars,uVars,
                                   vVars,inputProb,nVars,nPi,heuristic,
                                   equivClasses,&outBdds,&newInit,
                                   &stateProbs);
    /* equivRel is dereferenced in the above procedure */
    if (prunedTR == finalTR) {
      fprintf(vis_stdout,"** restr info: Restructuring produces no changes. \n");
      fprintf(vis_stdout,"** restr info: Proceeding with synthesis. \n");
      bdd_recursive_deref(ddManager,stateProbs);
      noRestruct = 1;
    }

    bdd_recursive_deref(ddManager,prunedTR);
    bdd_recursive_deref(ddManager,initBdd);

    /* reachable can be deleted after computing the new reachable states.  Also
     need to perform markov analysis to find final bit change. */
    initBdd = newInit;
    if (!noRestruct) {
      arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
        bdd_recursive_deref(ddManager,ddTemp);
      }
      array_free(nextBdds);
      nextBdds = ExtractTransitionFuns(ddManager,finalTR,yVars,nVars);
    }
  }

  /* Create a partition for the new view of the fsm/network */
  if (!noRestruct) {
    partition = CreateNewPartition(network1,ddManager,outBdds,nextBdds,
                                   outputArray,tranFunArray);
    array_free(outBdds);
    array_free(nextBdds);
    /* Create the FSM and perform markov ananlysis */
    /* finalTR, stateProbs and reachabale are deleted in CreateNewFsm */
    fsm = CreateNewFsm(network1,partition,ddManager,finalTR,initBdd,
                       reachable,stateProbs,xVars,yVars,piVars,
                       inputProb,nVars,nPi);
  } else {
    /* Remove the outBdds, nextBdds */
    arrayForEachItem(bdd_node *, outBdds, i, ddTemp) {
      bdd_recursive_deref(ddManager,ddTemp);
    }
    arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
      bdd_recursive_deref(ddManager,ddTemp);
    }
    array_free(outBdds);
    array_free(nextBdds);
  }

  /* First create the care table for next state and primary output
   functions. */
  careMdd = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
                                          Fsm_Rch_Default_c,0,0,
                                          NIL(array_t),FALSE, NIL(array_t));

  careTable = CreateCareTable(network1,careMdd);

  /* Synthesize the restructured FSM */
  status = Synth_SynthesizeFsm(fsm,careTable,synthInfo,0);

  /* Clean up */
  if (!noRestruct) {
    Ntk_NetworkFreeApplInfo(network1,RESTR_PART_NETWORK_APPL_KEY);
    Ntk_NetworkFreeApplInfo(network1,RESTR_FSM_NETWORK_APPL_KEY);
  }
  mdd_free(careMdd);
  st_free_table(careTable);

  /* Dump the current BDD variable order, for future use. */
  if(orderFileName) {
    outFile = fopen(orderFileName,"w");
    if(outFile) {
      int size = array_n(mdd_ret_mvar_list(ddManager));
      int index;
      mvar_type var;
      for(i = 0; i < size;i++) {
        index = bdd_get_id_from_level(ddManager,i);
        var = mdd_get_var_by_id(ddManager,index);
        fprintf(outFile,"%s\n",var.name);
      }
      fclose(outFile);
    } else {
      fprintf(vis_stderr,"** restr error: Cannot open %s .\n",orderFileName);
    }
  }

  /* Clean up */
  for(i = 0; i < nVars; i++) {
    bdd_recursive_deref(ddManager,xVars[i]);
    bdd_recursive_deref(ddManager,yVars[i]);
    bdd_recursive_deref(ddManager,uVars[i]);
    bdd_recursive_deref(ddManager,vVars[i]);
  }
  for(i = 0 ; i < nPi; i++) {
    bdd_recursive_deref(ddManager,piVars[i]);
  }
  FREE(xVars);
  FREE(yVars);
  FREE(uVars);
  FREE(vVars);
  FREE(piVars);

  array_free(outputArray);

  return (status);
}


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

static array_t *
BuildFunctions(
  graph_t *partition,
  array_t *rootNames)
{
  char *name;
  vertex_t *vertexPtr;
  Mvf_Function_t *mvf1;
  int i;
  array_t *result;

  result = array_alloc(Mvf_Function_t *,0);
  arrayForEachItem(char *,rootNames,i,name) {
    vertexPtr = Part_PartitionFindVertexByName(partition,name);
    mvf1 = Mvf_FunctionDuplicate(Part_VertexReadFunction(vertexPtr));
    array_insert(Mvf_Function_t *,result,i,mvf1);
  }

  return result;
}

static bdd_node **
AddPowerSolve(
  bdd_manager   *mgr,
  bdd_node      *bddTr,          
  bdd_node      *init,   
  bdd_node      **x,
  bdd_node      **y,
  bdd_node      **pi,
  st_table      *inputProb,
  int            nVars,
  int            nPi)
{
  bdd_node      *temp1, *temp, *q, *Correction;
  bdd_node        **result, *tr;
  bdd_node        **xAddVars, **yAddVars;
  bdd_node      *initG, *NewG;
  bdd_node      *inputCube,*xCube; 
  bdd_node      *newTr, *probMatrix;
  int           iter = 0;
  int           i;
  double        max,relTol = 0.0001;
  
  /* Initialize variables */
  result = ALLOC(bdd_node *, 2);
  xAddVars = ALLOC(bdd_node *, nVars);
  yAddVars = ALLOC(bdd_node *, nVars);
  for (i = 0; i < nVars; i++) {
    bdd_ref(xAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(x[i])));
    bdd_ref(yAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(y[i])));
  }
  bdd_ref(tr = bdd_bdd_to_add(mgr, bddTr));
  
  /* Create the input cube for abstraction */
  bdd_ref(temp1 = bdd_bdd_compute_cube(mgr, pi, NIL(int), nPi));
  bdd_ref(inputCube = bdd_bdd_to_add(mgr, temp1));
  bdd_recursive_deref(mgr, temp1);

  /* Compute the one-step transition probability matrix. */
  if (inputProb) {
    bdd_ref(probMatrix = Mark_addInProb(mgr,tr,inputCube,inputProb));
    bdd_recursive_deref(mgr,inputCube);
    bdd_recursive_deref(mgr,tr);
  }
  else {
    bdd_ref(Correction = bdd_add_const(mgr,(1.0/(double)(1 << nPi))));
    bdd_ref(q = bdd_add_exist_abstract(mgr,tr,inputCube));
    bdd_recursive_deref(mgr,inputCube);
    bdd_recursive_deref(mgr,tr);
    /* apply correction to the transition relation matrix and print it */
    bdd_ref(probMatrix = bdd_add_apply(mgr, bdd_add_times, q, Correction));
    bdd_recursive_deref(mgr,Correction);
    bdd_recursive_deref(mgr,q);
  }
  result[1] = probMatrix;

  /* Prepare the initial prob. vector. and the transition prob. matrix. */
  initG = bdd_add_swap_variables(mgr,init,xAddVars,yAddVars,nVars);
  bdd_ref(initG);
  /* Put transition prob. matrix in appropriate form (transpose). */
  newTr = bdd_add_swap_variables(mgr,probMatrix,xAddVars,yAddVars,nVars);
  bdd_ref(newTr);

  /* Calculate the x-cube for abstraction */
  bdd_ref(xCube = bdd_add_compute_cube(mgr,xAddVars,NIL(int),nVars));

  /* Loop until convergence */
  do {
    iter++;
    bdd_ref(temp = bdd_add_matrix_multiply(mgr,newTr,initG,yAddVars,nVars));
    bdd_ref(temp1 = bdd_add_exist_abstract(mgr,temp,xCube));
    bdd_ref(NewG = bdd_add_apply(mgr,bdd_add_divide,temp,temp1));
    bdd_recursive_deref(mgr,temp);
    bdd_recursive_deref(mgr,temp1);
    temp = NewG; 
    bdd_ref(q = bdd_add_swap_variables(mgr,temp,xAddVars,yAddVars,nVars));
    max = bdd_add_value(bdd_add_find_max(mgr,initG));

    if(bdd_equal_sup_norm(mgr,q,initG,relTol*max,0)) {
      bdd_recursive_deref(mgr,initG);
      bdd_recursive_deref(mgr,q);
      bdd_recursive_deref(mgr,xCube);
      bdd_recursive_deref(mgr,newTr);

      bdd_ref(temp1 = bdd_add_apply(mgr,bdd_add_times,probMatrix,temp));
      if (restrVerbose) {
        fprintf(vis_stdout,"** restr info: Average state bit change = %f\n",
                RestrAverageBitChange(mgr,temp1,x,y,nVars));
      }
      
      bdd_recursive_deref(mgr,temp1);
      for(i = 0;i < nVars; i++) {
        bdd_recursive_deref(mgr,xAddVars[i]);
        bdd_recursive_deref(mgr,yAddVars[i]);
      }
      FREE(xAddVars);
      FREE(yAddVars);
      result[0] = temp;
      return result;
    }
    bdd_recursive_deref(mgr,initG);
    bdd_recursive_deref(mgr,temp);
    initG = q;

  } while (1);

} /* end of AddPowerSolve */

static bdd_node *
PerformRestructure(
  bdd_manager *ddManager,
  bdd_node *prunedTR,
  bdd_node *equivRel,
  bdd_node *reachable,
  bdd_node *initBdd,
  bdd_node **piVars,
  bdd_node **xVars,
  bdd_node **yVars,
  bdd_node **uVars,
  bdd_node **vVars,
  st_table *inputProb,
  int nVars,
  int nPi,
  RestructureHeuristic heuristic,
  boolean equivClasses,
  array_t **outBdds,
  bdd_node **newInit,
  bdd_node **stateProbs)
{
  /* equivRel is a function of uVars and xVars */
  /* prunedTR is a funciton of xVars, piVars and yVars */

  bdd_node *possessedProbMatrix;
  bdd_node *possessedTR = NIL(bdd_node);
  bdd_node *addPTR;
  bdd_node *finalTR;
  bdd_node *ddTemp;
  bdd_node *localStateProbs = NIL(bdd_node);

  if(equivClasses) {
    CountEquivalentClasses(ddManager,equivRel,initBdd,xVars,uVars,nVars);
  }

  /* Change the support of equivRel */
  bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,equivRel,xVars,yVars,
                                          nVars));
  bdd_recursive_deref(ddManager,equivRel);
  bdd_ref(equivRel = bdd_bdd_swap_variables(ddManager,ddTemp,uVars,vVars,
                                            nVars));
  bdd_recursive_deref(ddManager, ddTemp);

  /* The support of possessedTR is xVars and yVars and inputs.
   * If there exists an edge between x and y, and y == v, then
   * the following function adds an edge between x and v. These new
   * edges are referred to as ghost edges.
   */
  
  if (heuristic != RestrCProjection_c) {
    possessedTR = RestrComputeTrWithGhostEdges(ddManager, yVars, vVars, 
                                               prunedTR, equivRel, nVars);
  }

  /* stateProbs will not be used in the case of CProj and hammingD methods.  We
   can still compute the stateProbs to find the initial average bit change on
   the state lines. */
  *stateProbs = DoMarkovPowerAnalysis(ddManager,prunedTR,
                                      initBdd,piVars,xVars, 
                                      yVars,inputProb,nVars,nPi);
    
  if (!(heuristic == RestrCProjection_c || heuristic == RestrHammingD_c)) {
    bdd_node *temp, *cube;

    bdd_ref(cube = bdd_bdd_compute_cube(ddManager,piVars,NIL(int),nPi));
    bdd_ref(temp = bdd_bdd_exist_abstract(ddManager,possessedTR,cube));
    bdd_ref(addPTR = bdd_bdd_to_add(ddManager,temp));
    bdd_recursive_deref(ddManager,temp);

    bdd_ref(temp = bdd_bdd_to_add(ddManager, possessedTR));
    bdd_recursive_deref(ddManager, possessedTR);

    /* possessedProbMatrix is a weighted augmented STG where the weights are
       the transition probabilities */
    if (inputProb) {
      bdd_ref(possessedProbMatrix = Mark_addInProb(ddManager,temp,cube,
                                                   inputProb));
    } else {
      /* Assume equi probable primary inputs */
      bdd_node *q, *Correction;
      bdd_node *inputCube;

      bdd_ref(inputCube = bdd_bdd_to_add(ddManager,cube));
      bdd_ref(Correction = bdd_add_const(ddManager,
                                         (1.0/(double)(1 << nPi))));
      bdd_ref(q = bdd_add_exist_abstract(ddManager,temp,inputCube));
      bdd_ref(possessedProbMatrix = bdd_add_apply(ddManager,
                                                  bdd_add_times,
                                                  q, Correction));
      bdd_recursive_deref(ddManager,Correction);
      bdd_recursive_deref(ddManager,q);
      bdd_recursive_deref(ddManager,inputCube);
    }
    bdd_recursive_deref(ddManager,cube);
    bdd_recursive_deref(ddManager,temp);
    localStateProbs = *stateProbs;
  }

  switch(heuristic) {
  case RestrCProjection_c:
    finalTR = RestrMinimizeFsmByCProj(ddManager,equivRel,
                                      prunedTR,initBdd,
                                      xVars,yVars,uVars,vVars,piVars,
                                      nVars,nPi,outBdds,newInit);
    break;
  case RestrFanin_c:
  case RestrFaninFanout_c:
    ddTemp = bdd_read_background(ddManager);
    bdd_set_background(ddManager, 
                       bdd_read_plus_infinity(ddManager));

    /* addPTR and possessedProbMatrix are deleted in the following 
     * procedure. */
    finalTR = RestrMinimizeFsmByFaninFanout(ddManager,equivRel, prunedTR, 
                                            &addPTR,&possessedProbMatrix,initBdd,
                                            reachable,localStateProbs,piVars,xVars,
                                            yVars, uVars,vVars,
                                            nVars, nPi,heuristic,outBdds,newInit);

    /* Replace the original background value */
    bdd_set_background(ddManager,ddTemp);
    break; 
  case RestrHammingD_c: 
  default : 
    
    /* BALA, testing ... */
    /* Remove the edges out of the initial state. */
    {
/*       bdd_node *outEdges; */

/*       bdd_ref(outEdges = bdd_bdd_and(ddManager,prunedTR,initBdd)); */
/*       bdd_ref(adjustedTR = bdd_bdd_and(ddManager,prunedTR, */
/*                                     bdd_not_bdd_node(outEdges))); */
/*       finalTR = RestrSelectLeastHammingDStates(ddManager,adjustedTR, */
/*                                             possessedTR,xVars, */
/*                                             yVars,vVars,nVars,nPi); */
      
      finalTR = RestrSelectLeastHammingDStates(ddManager,prunedTR,
                                               possessedTR,xVars,
                                               yVars,vVars,nVars,nPi);
      bdd_recursive_deref(ddManager,possessedTR);
      bdd_ref(*newInit = initBdd);
      break;
    }
  }

  bdd_recursive_deref(ddManager,equivRel);
  return finalTR;
}

static st_table *
CreateNameToMvfTable(
  bdd_manager *ddManager,                  
  array_t *outBdds,
  array_t *nextBdds,
  array_t *outputArray,
  array_t *tranFunArray)
{
  st_table *nameToMvf;
  bdd_node *ddTemp;
  int i;

  /* Initialize variables */
  nameToMvf = st_init_table(strcmp, st_strhash);

  arrayForEachItem(bdd_node *, outBdds, i, ddTemp) {
    bdd_node *temp;
    mdd_t *regular, *complement;
    Mvf_Function_t *mvf;
    char *name;

    bdd_ref(temp = bdd_not_bdd_node(ddTemp));

    regular = bdd_construct_bdd_t(ddManager,ddTemp);
    complement = bdd_construct_bdd_t(ddManager,temp);

    mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0);
    array_insert(mdd_t *, mvf, 0, complement);
    array_insert(mdd_t *, mvf, 1, regular);

    name = array_fetch(char *, outputArray, i);
    st_insert(nameToMvf,name,(char *)mvf);
  }

  arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
    bdd_node *temp;
    mdd_t *regular, *complement;
    Mvf_Function_t *mvf;
    char *name;

    bdd_ref(temp = bdd_not_bdd_node(ddTemp));

    regular = bdd_construct_bdd_t(ddManager,ddTemp);
    complement = bdd_construct_bdd_t(ddManager,temp);

    mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0);
    array_insert(mdd_t *, mvf, 0, complement);
    array_insert(mdd_t *, mvf, 1, regular);

    name = array_fetch(char *, tranFunArray, i);
    st_insert(nameToMvf,name,(char *)mvf);
  }

  return nameToMvf;
}


static st_table *
CreateCareTable(
  Ntk_Network_t *network,
  mdd_t *reachMdd)
{
  lsGen gen;
  Ntk_Node_t *node;
  st_table *careTable;

  careTable = st_init_table(strcmp, st_strhash);
  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
    char *name;
    name = Ntk_NodeReadName(node);
    st_insert(careTable,name,(char *)reachMdd);
  }
  Ntk_NetworkForEachLatch(network,gen,node){
    char *name;
    name = Ntk_NodeReadName(Ntk_LatchReadDataInput(node));
    st_insert(careTable,name,(char *)reachMdd);
  }

  return careTable;
}

static enum st_retval
StMvfFree(
  char *key,
  char *value,
  char *arg)
{
  /* This will free the memory associated with the array also */
  Mvf_FunctionFree((Mvf_Function_t *)value);
  
  return(ST_CONTINUE);
  
} /* end of StMvfFree */


static void
CountEquivalentClasses(
  bdd_manager *ddManager,
  bdd_node *equivRel,
  bdd_node *initBdd,
  bdd_node **xVars,
  bdd_node **uVars,
  int nVars)
{
  bdd_node *resultXU,*uCube;
  bdd_node *oneInitState,*classes;

  oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
  bdd_ref(oneInitState);

  bdd_ref(resultXU = bdd_bdd_cprojection(ddManager,equivRel,oneInitState));
  bdd_recursive_deref(ddManager,oneInitState);

#ifdef RESTR_DIAG
  {
    /* The following is valid only when equivRel is the equivalence relation on
       the complete set of states.*/
    bdd_node *xCube,*tautology;
    bdd_node *one;
    one = bdd_read_one(ddManager);
    bdd_ref(xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
    bdd_ref(tautology = bdd_bdd_exist_abstract(ddManager,resultXU,xCube));
    assert(tautology == one);
    bdd_recursive_deref(ddManager,tautology);
    bdd_recursive_deref(ddManager,xCube);
  }
#endif

#ifdef RESTR_DIAG
  {
    bdd_node *uCube,*zero,*classes;
    bdd_node *oneClass,*temp,*rep;
    int i;

    zero = bdd_not_bdd_node(bdd_read_one(ddManager));
    /* Extract the classes */
    bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
    bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube));
    bdd_recursive_deref(ddManager,uCube);
    
    i = 0;
    (void) fprintf(vis_stdout,"\n** restr diag: EQUIVALENT CLASSES:\n");
    while (classes != zero) {
      i++;
      bdd_ref(rep = bdd_bdd_pick_one_minterm(ddManager,classes,
                                             xVars,nVars));
      (void) fprintf(vis_stdout,"** restr diag: Class %d\n",i);
      (void) fprintf(vis_stdout,"** restr diag: Class representative:\n");
      RestrPrintBddNode(ddManager,rep);

      /* Extract the complete class now */
      bdd_ref(temp = bdd_bdd_cofactor(ddManager,resultXU,rep));
      bdd_ref(oneClass = bdd_bdd_swap_variables(ddManager,temp,uVars,
                                                xVars,nVars));
      bdd_recursive_deref(ddManager,temp);
      (void) fprintf(vis_stdout,"** restr diag: Class members:\n");
      RestrPrintBddNode(ddManager,oneClass);
      bdd_recursive_deref(ddManager,oneClass);

      /* Remove rep from classes */
      bdd_ref(temp = bdd_bdd_and(ddManager,classes,bdd_not_bdd_node(rep)));
      bdd_recursive_deref(ddManager,rep);
      bdd_recursive_deref(ddManager,classes);
      classes = temp;
    }
    (void) fprintf(vis_stdout,"** restr diag: Number of classes = %d\n",i);
  }
#endif

  /* Compute uCube and extract the u variables from resultXU */
  bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
  bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube));
  bdd_recursive_deref(ddManager,uCube);
  bdd_recursive_deref(ddManager,resultXU);

  fprintf(vis_stdout, "** restr info: Number of Equivalence Classes = %g\n",
          bdd_count_minterm(ddManager,classes,nVars));
  
  bdd_recursive_deref(ddManager,classes);
}


static array_t *
GetBddArrayFromMvfArray(array_t *mvfArray)
{
  int     i;
  array_t *bddArray;
  Mvf_Function_t *mvf;

  bddArray = array_alloc(bdd_node *,0);

  arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
    mdd_t     *mddTemp;
    bdd_node    *ddNode;

    mddTemp = array_fetch(mdd_t *, mvf, 1);
    ddNode = bdd_extract_node_as_is(mddTemp);
    bdd_ref(ddNode);

    array_insert_last(bdd_node *, bddArray, ddNode);
  }
  return bddArray;
}

static bdd_node *
DoMarkovPowerAnalysis(
  bdd_manager *ddManager,
  bdd_node *prunedTR,
  bdd_node *initBdd,
  bdd_node **piVars,
  bdd_node **xVars,
  bdd_node **yVars,
  st_table *inputProb,
  int nVars,
  int nPi)
{
  bdd_node **result, *stateProbs;
  bdd_node *init;
  
  bdd_ref(init = bdd_bdd_to_add(ddManager,initBdd));
  if (restrVerbose) 
    (void) fprintf(vis_stdout,"** restr info: Initial average state bit change:\n");

  result = AddPowerSolve(ddManager,prunedTR,init,xVars,yVars,
                              piVars,inputProb,nVars,nPi);
  
  bdd_recursive_deref(ddManager,result[1]);
  stateProbs = result[0];
  bdd_recursive_deref(ddManager,init);
  FREE(result);
  
  return stateProbs;
}

static array_t *
ExtractTransitionFuns(
  bdd_manager   *ddManager,
  bdd_node      *finalTR,
  bdd_node      **yVars,
  int           nVars)
{
  bdd_node      *completeCube, *extractCube;
  bdd_node      *fun, *tranFun;
  array_t       *allTranFuns;
  int           i;

  allTranFuns = array_alloc(bdd_node *,0);

  completeCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars);
  bdd_ref(completeCube);

  for(i = 0;i < nVars; i++) {
    extractCube = bdd_bdd_cofactor(ddManager,completeCube,yVars[i]);
    bdd_ref(extractCube);
    fun = bdd_bdd_exist_abstract(ddManager,finalTR,extractCube);
    bdd_ref(fun);
    bdd_recursive_deref(ddManager,extractCube);
    tranFun = bdd_bdd_cofactor(ddManager,fun,yVars[i]);
    bdd_ref(tranFun);

#ifdef RESTR_DIAG
    {
      /* The following is to test if there are multiple edges out of a state
         with the same input label: in short to check if the relation is
         deterministic or not. */

      bdd_node *yBar,*yNot,*inter;
      bdd_ref(yNot = bdd_not_bdd_node(yVars[i]));
      bdd_ref(yBar = bdd_bdd_cofactor(ddManager,fun,yNot));
      bdd_recursive_deref(ddManager,yNot);
      bdd_ref(inter = bdd_bdd_and(ddManager,yBar,tranFun));
      yNot = bdd_not_bdd_node(bdd_read_one(ddManager));
      assert(inter == yNot);
      bdd_recursive_deref(ddManager,inter);
      bdd_recursive_deref(ddManager,yBar);
    }
#endif

    bdd_recursive_deref(ddManager,fun);
    array_insert_last(bdd_node *,allTranFuns,tranFun);
  }

  bdd_recursive_deref(ddManager,completeCube);
  return allTranFuns;
}

static array_t *
GetBddArrayFromNameArray(
  Fsm_Fsm_t *fsm,
  array_t *nameArray)
{
  graph_t *partition;
  array_t *bdds,*mvfs;
  
  partition = Fsm_FsmReadPartition(fsm);
  mvfs = BuildFunctions(partition,nameArray);
  bdds = GetBddArrayFromMvfArray(mvfs);
  Mvf_FunctionArrayFree(mvfs);

  return bdds;
}

static void
ExpandReachableSet(
  bdd_manager *ddManager,
  bdd_node **reachable,
  bdd_node *equivRel,
  bdd_node **xVars,
  bdd_node **uVars,
  int nVars)
{
  bdd_node *xcube,*potUnReach,*extReach;
  bdd_node *temp1;

  bdd_ref(xcube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
  /* potUnReach = \exists_x (E(x,u) * R(x)) */
  bdd_ref(potUnReach = bdd_bdd_and_abstract(ddManager,*reachable,
                                            equivRel,xcube));
  bdd_recursive_deref(ddManager,xcube);
  /* temp1(x) = potUnReach(u) */
  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,potUnReach,uVars,
                                         xVars,nVars));
  bdd_recursive_deref(ddManager,potUnReach);
  /* extReach(x) = R(x) + potUnReach(x) */
  bdd_ref(extReach = bdd_bdd_or(ddManager,*reachable,temp1));
  bdd_recursive_deref(ddManager,temp1);
  bdd_recursive_deref(ddManager,*reachable);
  *reachable = extReach;
}

static graph_t *
CreateNewPartition(
  Ntk_Network_t *network,                  
  bdd_manager *ddManager,
  array_t *outBdds,
  array_t *nextBdds,
  array_t *outputArray,
  array_t *tranFunArray)
{
  st_table *nameToMvf;
  graph_t *partition;

  /* Create a table of next state and output Mvfs with their names as key to
     the table. This table is used to create a partition for the network. */
  nameToMvf = CreateNameToMvfTable(ddManager,outBdds,nextBdds,
                                   outputArray,tranFunArray);
  /* Delete the old partition and old fsm as we dont need it any more */
  if (restrCreatedPart) {
    Ntk_NetworkFreeApplInfo(network,RESTR_PART_NETWORK_APPL_KEY);
    restrCreatedPart = 0;
  }
  if (restrCreatedFsm) {
    Ntk_NetworkFreeApplInfo(network,RESTR_FSM_NETWORK_APPL_KEY);
    restrCreatedFsm = 0;
  }

  /* Create a new partition from the new root functions */
  partition = Part_NetworkCreatePartitionFromMvfs(network,nameToMvf);
  Ntk_NetworkAddApplInfo(network, RESTR_PART_NETWORK_APPL_KEY,
                         (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                         (void *) partition);
  st_foreach(nameToMvf,StMvfFree,NIL(char));
  st_free_table(nameToMvf);

  return partition;
}

static Fsm_Fsm_t *
CreateNewFsm(
  Ntk_Network_t *network,
  graph_t *partition,
  bdd_manager *ddManager,
  bdd_node *finalTR,
  bdd_node *initBdd,
  bdd_node *reachable,
  bdd_node *stateProbs,
  bdd_node **xVars,
  bdd_node **yVars,
  bdd_node **piVars,
  st_table *inputProb,
  int nVars,
  int nPi)
{
  Fsm_Fsm_t *fsm;
  mdd_t *reachStates;
  mdd_t *mddTemp;
  bdd_node *ddTemp;
  bdd_node **markovResult;

  /* Create a new Fsm for the restructured network. */
  fsm = Fsm_FsmCreateFromNetworkWithPartition(network,
                                              Part_PartitionDuplicate(partition));
  assert(fsm != NIL(Fsm_Fsm_t));
  Ntk_NetworkAddApplInfo(network, RESTR_FSM_NETWORK_APPL_KEY,
                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
                         (void *) fsm); 
  /* We need to update the initial states as the
     Fsm_FsmCreateFromNetworkWithPartition will pick up old initial state from
     the network. Fsm_FsmSetInitialStates deletes old inital states. */
  mddTemp = bdd_construct_bdd_t(ddManager,initBdd);
  Fsm_FsmSetInitialStates(fsm,mddTemp);

  /* Compute the new reachable states */
  reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
                                              Fsm_Rch_Default_c,0,0,
                                              NIL(array_t),FALSE, NIL(array_t));

  bdd_recursive_deref(ddManager,reachable);
  reachable = bdd_extract_node_as_is(reachStates);
  bdd_ref(reachable);
  mdd_free(reachStates);
        
  /* Constrain the transition relation */
  bdd_ref(ddTemp = bdd_bdd_constrain(ddManager,finalTR,reachable));
  bdd_recursive_deref(ddManager,finalTR);
  finalTR = ddTemp;

  /* Use the state probs. of the original STG as the initial guess to compute
     the state probs. of the restructured STG. */
  if (restrVerbose)
    (void) fprintf(vis_stdout,"** restr info: Final average state bit change:\n");

  markovResult = AddPowerSolve(ddManager, finalTR, stateProbs, xVars,
                                    yVars,piVars,inputProb,nVars,nPi);
  bdd_recursive_deref(ddManager, markovResult[0]);
  bdd_recursive_deref(ddManager, markovResult[1]);
  FREE(markovResult);
        
  bdd_recursive_deref(ddManager,stateProbs);
  bdd_recursive_deref(ddManager,finalTR);
  bdd_recursive_deref(ddManager,reachable);

  return fsm;
}