VIS

src/restr/restrRestructure.c

Go to the documentation of this file.
00001 
00027 #include "restrInt.h"
00028 
00029 /*---------------------------------------------------------------------------*/
00030 /* Constant declarations                                                     */
00031 /*---------------------------------------------------------------------------*/
00032 
00033 
00034 /*---------------------------------------------------------------------------*/
00035 /* Type declarations                                                         */
00036 /*---------------------------------------------------------------------------*/
00037 
00038 
00039 /*---------------------------------------------------------------------------*/
00040 /* Structure declarations                                                    */
00041 /*---------------------------------------------------------------------------*/
00042 
00043 /*---------------------------------------------------------------------------*/
00044 /* Variable declarations                                                     */
00045 /*---------------------------------------------------------------------------*/
00046 extern int restrCreatedPart;
00047 extern int restrCreatedFsm;
00048 extern boolean restrVerbose;
00049 
00050 /*---------------------------------------------------------------------------*/
00051 /* Macro declarations                                                        */
00052 /*---------------------------------------------------------------------------*/
00053 
00054 
00057 /*---------------------------------------------------------------------------*/
00058 /* Static function prototypes                                                */
00059 /*---------------------------------------------------------------------------*/
00060 
00061 static array_t * BuildFunctions(graph_t *partition, array_t *rootNames);
00062 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);
00063 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);
00064 static st_table * CreateNameToMvfTable(bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray);
00065 static st_table * CreateCareTable(Ntk_Network_t *network, mdd_t *reachMdd);
00066 static enum st_retval StMvfFree(char *key, char *value, char *arg);
00067 static void CountEquivalentClasses(bdd_manager *ddManager, bdd_node *equivRel, bdd_node *initBdd, bdd_node **xVars, bdd_node **uVars, int nVars);
00068 static array_t * GetBddArrayFromMvfArray(array_t *mvfArray);
00069 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);
00070 static array_t * ExtractTransitionFuns(bdd_manager *ddManager, bdd_node *finalTR, bdd_node **yVars, int nVars);
00071 static array_t * GetBddArrayFromNameArray(Fsm_Fsm_t *fsm, array_t *nameArray);
00072 static void ExpandReachableSet(bdd_manager *ddManager, bdd_node **reachable, bdd_node *equivRel, bdd_node **xVars, bdd_node **uVars, int nVars);
00073 static graph_t * CreateNewPartition(Ntk_Network_t *network, bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray);
00074 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);
00075 
00079 /*---------------------------------------------------------------------------*/
00080 /* Definition of exported functions                                          */
00081 /*---------------------------------------------------------------------------*/
00082 
00083 /*---------------------------------------------------------------------------*/
00084 /* Definition of internal functions                                          */
00085 /*---------------------------------------------------------------------------*/
00086 
00134 int
00135 RestrCommandRestructureFsm(
00136   Fsm_Fsm_t *fsm,                          
00137   RestructureHeuristic heuristic,
00138   char *orderFileName,
00139   boolean equivClasses,
00140   boolean nonReachEquiv,
00141   boolean eqvMethod,
00142   st_table *inputProb,
00143   Synth_InfoData_t *synthInfo)
00144 {
00145 
00146   graph_t *partition;
00147   Ntk_Network_t *network1;
00148   bdd_manager *ddManager;
00149 
00150   array_t *outputArray, *tranFunArray;
00151   array_t *outBdds, *nextBdds;
00152   array_t *tranRelationPair;
00153   array_t *newStateVars;
00154 
00155   st_table *careTable;
00156 
00157   int i;
00158   int nVars, nPi;
00159   int noRestruct = 0;
00160   boolean status;
00161 
00162   bdd_node *Lambda, *productTranRel, *prunedTR, *initialTR;
00163   bdd_node *equivRel;
00164   bdd_node *stateProbs;
00165   bdd_node *finalTR = NIL(bdd_node);
00166   bdd_node **xVars,**yVars,**uVars,**vVars;
00167   bdd_node **piVars;
00168   bdd_node *ddTemp, *reachable, *initBdd;
00169   bdd_node *newInit;
00170 
00171   mdd_t *reachStates, *mddTemp;
00172   mdd_t *careMdd;
00173 
00174   FILE *outFile;
00175 
00176   network1 = Fsm_FsmReadNetwork(fsm);
00177   ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network1);
00178 
00179   /* Get the bdd_node for primary, present and next state variables.*/
00180   piVars = RestrBddNodeArrayFromIdArray(ddManager, 
00181                                         Fsm_FsmReadInputVars(fsm));
00182   xVars = RestrBddNodeArrayFromIdArray(ddManager, 
00183                                        Fsm_FsmReadPresentStateVars(fsm));
00184   yVars = RestrBddNodeArrayFromIdArray(ddManager,
00185                                        Fsm_FsmReadNextStateVars(fsm));
00186   /* Create new state variables for duplicate machine. */
00187   newStateVars = RestrCreateNewStateVars(network1, ddManager,xVars,yVars);
00188   uVars = RestrBddNodeArrayFromIdArray(ddManager,
00189                                        array_fetch(array_t *, 
00190                                                    newStateVars, 0));
00191   vVars = RestrBddNodeArrayFromIdArray(ddManager,
00192                                        array_fetch(array_t *, 
00193                                                    newStateVars, 1));
00194 
00195   /* Free memory: Delete the id array for new state variables.*/
00196   array_free(array_fetch(array_t *,newStateVars,0));
00197   array_free(array_fetch(array_t *,newStateVars,1));
00198   array_free(newStateVars);
00199 
00200   /* outputArray is the list of primary outputs. It is my responsibility to
00201   free it later. Both outputArray and tranFunArray are char * arrays.  Get the
00202   BDDs for output functions and transition functions.  Duplicate functions are
00203   returned.*/
00204 
00205   /* tranFunArray should not be freed */
00206   outputArray = RestrGetOutputArray(network1);
00207   tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
00208   outBdds = GetBddArrayFromNameArray(fsm,outputArray);
00209   nextBdds = GetBddArrayFromNameArray(fsm,tranFunArray);
00210 
00211   nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
00212   nPi = array_n(Fsm_FsmReadInputVars(fsm));
00213 
00214   /* Compute Lambda = AND (out1 xnor out1$NTK2) and Transition relation.
00215    out1$NTK2 is the corresponding primary output (of output1) in the duplicate
00216    machine.*/
00217   if (restrVerbose) {
00218     fprintf(vis_stdout,"** restr info: Computing product output ... ");
00219   }
00220   Lambda = RestrCreateProductOutput(ddManager,outBdds,xVars, uVars, nVars);
00221   if (restrVerbose) {
00222     fprintf(vis_stdout,"Done.\n");
00223   }
00224 
00225   if (restrVerbose) {
00226     fprintf(vis_stdout,"** restr info: Computing TR of product machine ... ");
00227   }
00228   /* Compute the transition relation for both the single FSM and the product
00229      machine.  tranRelationPair[0] is the TR of single FSM and
00230      tranRelationPair[1] is the TR of product machine.  
00231      TR(x,w,y) = \prod_{i=0}^{i=n-1} (y_i \equiv f_i(w,x))
00232      productTR(x,u,w,y,v) = TR(x,w,y) * TR(u,w,v) */
00233   tranRelationPair = RestrComputeTRWithIds(ddManager,nextBdds,xVars, yVars,
00234                                            uVars,vVars,nVars);
00235   if (restrVerbose) {
00236     fprintf(vis_stdout,"Done.\n");
00237   }
00238 
00239   productTranRel = array_fetch(bdd_node *,tranRelationPair,1);
00240 
00241   /* Compute the state equivalence relation for the FSM */
00242   /* The support of equivRel is xVars and uVars. */
00243   if (restrVerbose) {
00244     fprintf(vis_stdout,"** restr info: Computing the equivalence relation ... ");
00245   }
00246 
00247   if (eqvMethod) {
00248     equivRel = RestrComputeEquivRelationUsingCofactors(ddManager,Lambda,
00249                                                        productTranRel,
00250                                                        xVars, yVars, uVars,
00251                                                        vVars, piVars,
00252                                                        nVars, nPi,
00253                                                        restrVerbose);
00254     bdd_recursive_deref(ddManager,Lambda);
00255   } else {
00256     equivRel = RestrGetEquivRelation(ddManager,Lambda,productTranRel,
00257                                      xVars,yVars,uVars,vVars,
00258                                      piVars,nVars,nPi,restrVerbose);
00259     bdd_recursive_deref(ddManager,Lambda);
00260   }
00261   if (restrVerbose) {
00262     fprintf(vis_stdout,"Done.\n");
00263   }
00264   /* Delete the product transition relation, as we no longer need it. */
00265   bdd_recursive_deref(ddManager,productTranRel);
00266 
00267   /* Compute the initial states */
00268   mddTemp = Fsm_FsmComputeInitialStates(fsm);
00269   initBdd = bdd_extract_node_as_is(mddTemp);
00270   bdd_ref(initBdd);
00271   mdd_free(mddTemp);
00272 
00273   /* Compute the reachable states. */
00274   reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
00275                                               Fsm_Rch_Default_c,0,0,
00276                                               NIL(array_t),FALSE, NIL(array_t));
00277 
00278   reachable = bdd_extract_node_as_is(reachStates);
00279   bdd_ref(reachable);
00280   mdd_free(reachStates);
00281 
00282   /* Check to see if there are any usable equivalence classes */
00283   if (bdd_count_minterm(ddManager,equivRel,2*nVars) == pow(2.0,nVars)) {
00284     fprintf(vis_stdout,"** restr info: Number of equivalence classes equals ");
00285     fprintf(vis_stdout,"number of possible states. \n");
00286     fprintf(vis_stdout,"** restr info: Restructuring will not help.\n");
00287     fprintf(vis_stdout,"** restr info: Proceeding with synthesis.\n");
00288     bdd_recursive_deref(ddManager,equivRel);
00289     /* Do not perform restructuring */
00290     noRestruct = 1;
00291   }
00292 
00293   /* Expand the reachable set R(x) to include those states which are equivalent
00294    to R(x) but unreachable. */
00295   if(nonReachEquiv && !noRestruct) {
00296     ExpandReachableSet(ddManager,&reachable,equivRel,xVars,uVars,nVars);
00297   }
00298 
00299   if (noRestruct) {
00300     /* Only synthesize the network */
00301     bdd_recursive_deref(ddManager,equivRel);
00302     bdd_recursive_deref(ddManager,
00303                         array_fetch(bdd_node *,tranRelationPair,0));
00304     array_free(tranRelationPair);
00305   } else {
00306     /* Constrain the original TR */
00307     initialTR = array_fetch(bdd_node *, tranRelationPair, 0);
00308     /* bdd_ref(prunedTR = bdd_bdd_and(ddManager,initialTR,reachable)); */
00309     bdd_ref(prunedTR = initialTR);
00310     bdd_recursive_deref(ddManager,initialTR);
00311     array_free(tranRelationPair);
00312 
00313     finalTR = PerformRestructure(ddManager,prunedTR,equivRel,reachable,
00314                                    initBdd,piVars,xVars,yVars,uVars,
00315                                    vVars,inputProb,nVars,nPi,heuristic,
00316                                    equivClasses,&outBdds,&newInit,
00317                                    &stateProbs);
00318     /* equivRel is dereferenced in the above procedure */
00319     if (prunedTR == finalTR) {
00320       fprintf(vis_stdout,"** restr info: Restructuring produces no changes. \n");
00321       fprintf(vis_stdout,"** restr info: Proceeding with synthesis. \n");
00322       bdd_recursive_deref(ddManager,stateProbs);
00323       noRestruct = 1;
00324     }
00325 
00326     bdd_recursive_deref(ddManager,prunedTR);
00327     bdd_recursive_deref(ddManager,initBdd);
00328 
00329     /* reachable can be deleted after computing the new reachable states.  Also
00330      need to perform markov analysis to find final bit change. */
00331     initBdd = newInit;
00332     if (!noRestruct) {
00333       arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
00334         bdd_recursive_deref(ddManager,ddTemp);
00335       }
00336       array_free(nextBdds);
00337       nextBdds = ExtractTransitionFuns(ddManager,finalTR,yVars,nVars);
00338     }
00339   }
00340 
00341   /* Create a partition for the new view of the fsm/network */
00342   if (!noRestruct) {
00343     partition = CreateNewPartition(network1,ddManager,outBdds,nextBdds,
00344                                    outputArray,tranFunArray);
00345     array_free(outBdds);
00346     array_free(nextBdds);
00347     /* Create the FSM and perform markov ananlysis */
00348     /* finalTR, stateProbs and reachabale are deleted in CreateNewFsm */
00349     fsm = CreateNewFsm(network1,partition,ddManager,finalTR,initBdd,
00350                        reachable,stateProbs,xVars,yVars,piVars,
00351                        inputProb,nVars,nPi);
00352   } else {
00353     /* Remove the outBdds, nextBdds */
00354     arrayForEachItem(bdd_node *, outBdds, i, ddTemp) {
00355       bdd_recursive_deref(ddManager,ddTemp);
00356     }
00357     arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
00358       bdd_recursive_deref(ddManager,ddTemp);
00359     }
00360     array_free(outBdds);
00361     array_free(nextBdds);
00362   }
00363 
00364   /* First create the care table for next state and primary output
00365    functions. */
00366   careMdd = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
00367                                           Fsm_Rch_Default_c,0,0,
00368                                           NIL(array_t),FALSE, NIL(array_t));
00369 
00370   careTable = CreateCareTable(network1,careMdd);
00371 
00372   /* Synthesize the restructured FSM */
00373   status = Synth_SynthesizeFsm(fsm,careTable,synthInfo,0);
00374 
00375   /* Clean up */
00376   if (!noRestruct) {
00377     Ntk_NetworkFreeApplInfo(network1,RESTR_PART_NETWORK_APPL_KEY);
00378     Ntk_NetworkFreeApplInfo(network1,RESTR_FSM_NETWORK_APPL_KEY);
00379   }
00380   mdd_free(careMdd);
00381   st_free_table(careTable);
00382 
00383   /* Dump the current BDD variable order, for future use. */
00384   if(orderFileName) {
00385     outFile = fopen(orderFileName,"w");
00386     if(outFile) {
00387       int size = array_n(mdd_ret_mvar_list(ddManager));
00388       int index;
00389       mvar_type var;
00390       for(i = 0; i < size;i++) {
00391         index = bdd_get_id_from_level(ddManager,i);
00392         var = mdd_get_var_by_id(ddManager,index);
00393         fprintf(outFile,"%s\n",var.name);
00394       }
00395       fclose(outFile);
00396     } else {
00397       fprintf(vis_stderr,"** restr error: Cannot open %s .\n",orderFileName);
00398     }
00399   }
00400 
00401   /* Clean up */
00402   for(i = 0; i < nVars; i++) {
00403     bdd_recursive_deref(ddManager,xVars[i]);
00404     bdd_recursive_deref(ddManager,yVars[i]);
00405     bdd_recursive_deref(ddManager,uVars[i]);
00406     bdd_recursive_deref(ddManager,vVars[i]);
00407   }
00408   for(i = 0 ; i < nPi; i++) {
00409     bdd_recursive_deref(ddManager,piVars[i]);
00410   }
00411   FREE(xVars);
00412   FREE(yVars);
00413   FREE(uVars);
00414   FREE(vVars);
00415   FREE(piVars);
00416 
00417   array_free(outputArray);
00418 
00419   return (status);
00420 }
00421 
00422 
00423 /*---------------------------------------------------------------------------*/
00424 /* Definition of static functions                                            */
00425 /*---------------------------------------------------------------------------*/
00426 
00436 static array_t *
00437 BuildFunctions(
00438   graph_t *partition,
00439   array_t *rootNames)
00440 {
00441   char *name;
00442   vertex_t *vertexPtr;
00443   Mvf_Function_t *mvf1;
00444   int i;
00445   array_t *result;
00446 
00447   result = array_alloc(Mvf_Function_t *,0);
00448   arrayForEachItem(char *,rootNames,i,name) {
00449     vertexPtr = Part_PartitionFindVertexByName(partition,name);
00450     mvf1 = Mvf_FunctionDuplicate(Part_VertexReadFunction(vertexPtr));
00451     array_insert(Mvf_Function_t *,result,i,mvf1);
00452   }
00453 
00454   return result;
00455 }
00456 
00471 static bdd_node **
00472 AddPowerSolve(
00473   bdd_manager   *mgr,
00474   bdd_node      *bddTr,          
00475   bdd_node      *init,   
00476   bdd_node      **x,
00477   bdd_node      **y,
00478   bdd_node      **pi,
00479   st_table      *inputProb,
00480   int            nVars,
00481   int            nPi)
00482 {
00483   bdd_node      *temp1, *temp, *q, *Correction;
00484   bdd_node        **result, *tr;
00485   bdd_node        **xAddVars, **yAddVars;
00486   bdd_node      *initG, *NewG;
00487   bdd_node      *inputCube,*xCube; 
00488   bdd_node      *newTr, *probMatrix;
00489   int           iter = 0;
00490   int           i;
00491   double        max,relTol = 0.0001;
00492   
00493   /* Initialize variables */
00494   result = ALLOC(bdd_node *, 2);
00495   xAddVars = ALLOC(bdd_node *, nVars);
00496   yAddVars = ALLOC(bdd_node *, nVars);
00497   for (i = 0; i < nVars; i++) {
00498     bdd_ref(xAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(x[i])));
00499     bdd_ref(yAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(y[i])));
00500   }
00501   bdd_ref(tr = bdd_bdd_to_add(mgr, bddTr));
00502   
00503   /* Create the input cube for abstraction */
00504   bdd_ref(temp1 = bdd_bdd_compute_cube(mgr, pi, NIL(int), nPi));
00505   bdd_ref(inputCube = bdd_bdd_to_add(mgr, temp1));
00506   bdd_recursive_deref(mgr, temp1);
00507 
00508   /* Compute the one-step transition probability matrix. */
00509   if (inputProb) {
00510     bdd_ref(probMatrix = Mark_addInProb(mgr,tr,inputCube,inputProb));
00511     bdd_recursive_deref(mgr,inputCube);
00512     bdd_recursive_deref(mgr,tr);
00513   }
00514   else {
00515     bdd_ref(Correction = bdd_add_const(mgr,(1.0/(double)(1 << nPi))));
00516     bdd_ref(q = bdd_add_exist_abstract(mgr,tr,inputCube));
00517     bdd_recursive_deref(mgr,inputCube);
00518     bdd_recursive_deref(mgr,tr);
00519     /* apply correction to the transition relation matrix and print it */
00520     bdd_ref(probMatrix = bdd_add_apply(mgr, bdd_add_times, q, Correction));
00521     bdd_recursive_deref(mgr,Correction);
00522     bdd_recursive_deref(mgr,q);
00523   }
00524   result[1] = probMatrix;
00525 
00526   /* Prepare the initial prob. vector. and the transition prob. matrix. */
00527   initG = bdd_add_swap_variables(mgr,init,xAddVars,yAddVars,nVars);
00528   bdd_ref(initG);
00529   /* Put transition prob. matrix in appropriate form (transpose). */
00530   newTr = bdd_add_swap_variables(mgr,probMatrix,xAddVars,yAddVars,nVars);
00531   bdd_ref(newTr);
00532 
00533   /* Calculate the x-cube for abstraction */
00534   bdd_ref(xCube = bdd_add_compute_cube(mgr,xAddVars,NIL(int),nVars));
00535 
00536   /* Loop until convergence */
00537   do {
00538     iter++;
00539     bdd_ref(temp = bdd_add_matrix_multiply(mgr,newTr,initG,yAddVars,nVars));
00540     bdd_ref(temp1 = bdd_add_exist_abstract(mgr,temp,xCube));
00541     bdd_ref(NewG = bdd_add_apply(mgr,bdd_add_divide,temp,temp1));
00542     bdd_recursive_deref(mgr,temp);
00543     bdd_recursive_deref(mgr,temp1);
00544     temp = NewG; 
00545     bdd_ref(q = bdd_add_swap_variables(mgr,temp,xAddVars,yAddVars,nVars));
00546     max = bdd_add_value(bdd_add_find_max(mgr,initG));
00547 
00548     if(bdd_equal_sup_norm(mgr,q,initG,relTol*max,0)) {
00549       bdd_recursive_deref(mgr,initG);
00550       bdd_recursive_deref(mgr,q);
00551       bdd_recursive_deref(mgr,xCube);
00552       bdd_recursive_deref(mgr,newTr);
00553 
00554       bdd_ref(temp1 = bdd_add_apply(mgr,bdd_add_times,probMatrix,temp));
00555       if (restrVerbose) {
00556         fprintf(vis_stdout,"** restr info: Average state bit change = %f\n",
00557                 RestrAverageBitChange(mgr,temp1,x,y,nVars));
00558       }
00559       
00560       bdd_recursive_deref(mgr,temp1);
00561       for(i = 0;i < nVars; i++) {
00562         bdd_recursive_deref(mgr,xAddVars[i]);
00563         bdd_recursive_deref(mgr,yAddVars[i]);
00564       }
00565       FREE(xAddVars);
00566       FREE(yAddVars);
00567       result[0] = temp;
00568       return result;
00569     }
00570     bdd_recursive_deref(mgr,initG);
00571     bdd_recursive_deref(mgr,temp);
00572     initG = q;
00573 
00574   } while (1);
00575 
00576 } /* end of AddPowerSolve */
00577 
00591 static bdd_node *
00592 PerformRestructure(
00593   bdd_manager *ddManager,
00594   bdd_node *prunedTR,
00595   bdd_node *equivRel,
00596   bdd_node *reachable,
00597   bdd_node *initBdd,
00598   bdd_node **piVars,
00599   bdd_node **xVars,
00600   bdd_node **yVars,
00601   bdd_node **uVars,
00602   bdd_node **vVars,
00603   st_table *inputProb,
00604   int nVars,
00605   int nPi,
00606   RestructureHeuristic heuristic,
00607   boolean equivClasses,
00608   array_t **outBdds,
00609   bdd_node **newInit,
00610   bdd_node **stateProbs)
00611 {
00612   /* equivRel is a function of uVars and xVars */
00613   /* prunedTR is a funciton of xVars, piVars and yVars */
00614 
00615   bdd_node *possessedProbMatrix;
00616   bdd_node *possessedTR = NIL(bdd_node);
00617   bdd_node *addPTR;
00618   bdd_node *finalTR;
00619   bdd_node *ddTemp;
00620   bdd_node *localStateProbs = NIL(bdd_node);
00621 
00622   if(equivClasses) {
00623     CountEquivalentClasses(ddManager,equivRel,initBdd,xVars,uVars,nVars);
00624   }
00625 
00626   /* Change the support of equivRel */
00627   bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,equivRel,xVars,yVars,
00628                                           nVars));
00629   bdd_recursive_deref(ddManager,equivRel);
00630   bdd_ref(equivRel = bdd_bdd_swap_variables(ddManager,ddTemp,uVars,vVars,
00631                                             nVars));
00632   bdd_recursive_deref(ddManager, ddTemp);
00633 
00634   /* The support of possessedTR is xVars and yVars and inputs.
00635    * If there exists an edge between x and y, and y == v, then
00636    * the following function adds an edge between x and v. These new
00637    * edges are referred to as ghost edges.
00638    */
00639   
00640   if (heuristic != RestrCProjection_c) {
00641     possessedTR = RestrComputeTrWithGhostEdges(ddManager, yVars, vVars, 
00642                                                prunedTR, equivRel, nVars);
00643   }
00644 
00645   /* stateProbs will not be used in the case of CProj and hammingD methods.  We
00646    can still compute the stateProbs to find the initial average bit change on
00647    the state lines. */
00648   *stateProbs = DoMarkovPowerAnalysis(ddManager,prunedTR,
00649                                       initBdd,piVars,xVars, 
00650                                       yVars,inputProb,nVars,nPi);
00651     
00652   if (!(heuristic == RestrCProjection_c || heuristic == RestrHammingD_c)) {
00653     bdd_node *temp, *cube;
00654 
00655     bdd_ref(cube = bdd_bdd_compute_cube(ddManager,piVars,NIL(int),nPi));
00656     bdd_ref(temp = bdd_bdd_exist_abstract(ddManager,possessedTR,cube));
00657     bdd_ref(addPTR = bdd_bdd_to_add(ddManager,temp));
00658     bdd_recursive_deref(ddManager,temp);
00659 
00660     bdd_ref(temp = bdd_bdd_to_add(ddManager, possessedTR));
00661     bdd_recursive_deref(ddManager, possessedTR);
00662 
00663     /* possessedProbMatrix is a weighted augmented STG where the weights are
00664        the transition probabilities */
00665     if (inputProb) {
00666       bdd_ref(possessedProbMatrix = Mark_addInProb(ddManager,temp,cube,
00667                                                    inputProb));
00668     } else {
00669       /* Assume equi probable primary inputs */
00670       bdd_node *q, *Correction;
00671       bdd_node *inputCube;
00672 
00673       bdd_ref(inputCube = bdd_bdd_to_add(ddManager,cube));
00674       bdd_ref(Correction = bdd_add_const(ddManager,
00675                                          (1.0/(double)(1 << nPi))));
00676       bdd_ref(q = bdd_add_exist_abstract(ddManager,temp,inputCube));
00677       bdd_ref(possessedProbMatrix = bdd_add_apply(ddManager,
00678                                                   bdd_add_times,
00679                                                   q, Correction));
00680       bdd_recursive_deref(ddManager,Correction);
00681       bdd_recursive_deref(ddManager,q);
00682       bdd_recursive_deref(ddManager,inputCube);
00683     }
00684     bdd_recursive_deref(ddManager,cube);
00685     bdd_recursive_deref(ddManager,temp);
00686     localStateProbs = *stateProbs;
00687   }
00688 
00689   switch(heuristic) {
00690   case RestrCProjection_c:
00691     finalTR = RestrMinimizeFsmByCProj(ddManager,equivRel,
00692                                       prunedTR,initBdd,
00693                                       xVars,yVars,uVars,vVars,piVars,
00694                                       nVars,nPi,outBdds,newInit);
00695     break;
00696   case RestrFanin_c:
00697   case RestrFaninFanout_c:
00698     ddTemp = bdd_read_background(ddManager);
00699     bdd_set_background(ddManager, 
00700                        bdd_read_plus_infinity(ddManager));
00701 
00702     /* addPTR and possessedProbMatrix are deleted in the following 
00703      * procedure. */
00704     finalTR = RestrMinimizeFsmByFaninFanout(ddManager,equivRel, prunedTR, 
00705                                             &addPTR,&possessedProbMatrix,initBdd,
00706                                             reachable,localStateProbs,piVars,xVars,
00707                                             yVars, uVars,vVars,
00708                                             nVars, nPi,heuristic,outBdds,newInit);
00709 
00710     /* Replace the original background value */
00711     bdd_set_background(ddManager,ddTemp);
00712     break; 
00713   case RestrHammingD_c: 
00714   default : 
00715     
00716     /* BALA, testing ... */
00717     /* Remove the edges out of the initial state. */
00718     {
00719 /*       bdd_node *outEdges; */
00720 
00721 /*       bdd_ref(outEdges = bdd_bdd_and(ddManager,prunedTR,initBdd)); */
00722 /*       bdd_ref(adjustedTR = bdd_bdd_and(ddManager,prunedTR, */
00723 /*                                     bdd_not_bdd_node(outEdges))); */
00724 /*       finalTR = RestrSelectLeastHammingDStates(ddManager,adjustedTR, */
00725 /*                                             possessedTR,xVars, */
00726 /*                                             yVars,vVars,nVars,nPi); */
00727       
00728       finalTR = RestrSelectLeastHammingDStates(ddManager,prunedTR,
00729                                                possessedTR,xVars,
00730                                                yVars,vVars,nVars,nPi);
00731       bdd_recursive_deref(ddManager,possessedTR);
00732       bdd_ref(*newInit = initBdd);
00733       break;
00734     }
00735   }
00736 
00737   bdd_recursive_deref(ddManager,equivRel);
00738   return finalTR;
00739 }
00740 
00753 static st_table *
00754 CreateNameToMvfTable(
00755   bdd_manager *ddManager,                  
00756   array_t *outBdds,
00757   array_t *nextBdds,
00758   array_t *outputArray,
00759   array_t *tranFunArray)
00760 {
00761   st_table *nameToMvf;
00762   bdd_node *ddTemp;
00763   int i;
00764 
00765   /* Initialize variables */
00766   nameToMvf = st_init_table(strcmp, st_strhash);
00767 
00768   arrayForEachItem(bdd_node *, outBdds, i, ddTemp) {
00769     bdd_node *temp;
00770     mdd_t *regular, *complement;
00771     Mvf_Function_t *mvf;
00772     char *name;
00773 
00774     bdd_ref(temp = bdd_not_bdd_node(ddTemp));
00775 
00776     regular = bdd_construct_bdd_t(ddManager,ddTemp);
00777     complement = bdd_construct_bdd_t(ddManager,temp);
00778 
00779     mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0);
00780     array_insert(mdd_t *, mvf, 0, complement);
00781     array_insert(mdd_t *, mvf, 1, regular);
00782 
00783     name = array_fetch(char *, outputArray, i);
00784     st_insert(nameToMvf,name,(char *)mvf);
00785   }
00786 
00787   arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
00788     bdd_node *temp;
00789     mdd_t *regular, *complement;
00790     Mvf_Function_t *mvf;
00791     char *name;
00792 
00793     bdd_ref(temp = bdd_not_bdd_node(ddTemp));
00794 
00795     regular = bdd_construct_bdd_t(ddManager,ddTemp);
00796     complement = bdd_construct_bdd_t(ddManager,temp);
00797 
00798     mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0);
00799     array_insert(mdd_t *, mvf, 0, complement);
00800     array_insert(mdd_t *, mvf, 1, regular);
00801 
00802     name = array_fetch(char *, tranFunArray, i);
00803     st_insert(nameToMvf,name,(char *)mvf);
00804   }
00805 
00806   return nameToMvf;
00807 }
00808 
00809 
00819 static st_table *
00820 CreateCareTable(
00821   Ntk_Network_t *network,
00822   mdd_t *reachMdd)
00823 {
00824   lsGen gen;
00825   Ntk_Node_t *node;
00826   st_table *careTable;
00827 
00828   careTable = st_init_table(strcmp, st_strhash);
00829   Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
00830     char *name;
00831     name = Ntk_NodeReadName(node);
00832     st_insert(careTable,name,(char *)reachMdd);
00833   }
00834   Ntk_NetworkForEachLatch(network,gen,node){
00835     char *name;
00836     name = Ntk_NodeReadName(Ntk_LatchReadDataInput(node));
00837     st_insert(careTable,name,(char *)reachMdd);
00838   }
00839 
00840   return careTable;
00841 }
00842 
00851 static enum st_retval
00852 StMvfFree(
00853   char *key,
00854   char *value,
00855   char *arg)
00856 {
00857   /* This will free the memory associated with the array also */
00858   Mvf_FunctionFree((Mvf_Function_t *)value);
00859   
00860   return(ST_CONTINUE);
00861   
00862 } /* end of StMvfFree */
00863 
00864 
00874 static void
00875 CountEquivalentClasses(
00876   bdd_manager *ddManager,
00877   bdd_node *equivRel,
00878   bdd_node *initBdd,
00879   bdd_node **xVars,
00880   bdd_node **uVars,
00881   int nVars)
00882 {
00883   bdd_node *resultXU,*uCube;
00884   bdd_node *oneInitState,*classes;
00885 
00886   oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
00887   bdd_ref(oneInitState);
00888 
00889   bdd_ref(resultXU = bdd_bdd_cprojection(ddManager,equivRel,oneInitState));
00890   bdd_recursive_deref(ddManager,oneInitState);
00891 
00892 #ifdef RESTR_DIAG
00893   {
00894     /* The following is valid only when equivRel is the equivalence relation on
00895        the complete set of states.*/
00896     bdd_node *xCube,*tautology;
00897     bdd_node *one;
00898     one = bdd_read_one(ddManager);
00899     bdd_ref(xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
00900     bdd_ref(tautology = bdd_bdd_exist_abstract(ddManager,resultXU,xCube));
00901     assert(tautology == one);
00902     bdd_recursive_deref(ddManager,tautology);
00903     bdd_recursive_deref(ddManager,xCube);
00904   }
00905 #endif
00906 
00907 #ifdef RESTR_DIAG
00908   {
00909     bdd_node *uCube,*zero,*classes;
00910     bdd_node *oneClass,*temp,*rep;
00911     int i;
00912 
00913     zero = bdd_not_bdd_node(bdd_read_one(ddManager));
00914     /* Extract the classes */
00915     bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
00916     bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube));
00917     bdd_recursive_deref(ddManager,uCube);
00918     
00919     i = 0;
00920     (void) fprintf(vis_stdout,"\n** restr diag: EQUIVALENT CLASSES:\n");
00921     while (classes != zero) {
00922       i++;
00923       bdd_ref(rep = bdd_bdd_pick_one_minterm(ddManager,classes,
00924                                              xVars,nVars));
00925       (void) fprintf(vis_stdout,"** restr diag: Class %d\n",i);
00926       (void) fprintf(vis_stdout,"** restr diag: Class representative:\n");
00927       RestrPrintBddNode(ddManager,rep);
00928 
00929       /* Extract the complete class now */
00930       bdd_ref(temp = bdd_bdd_cofactor(ddManager,resultXU,rep));
00931       bdd_ref(oneClass = bdd_bdd_swap_variables(ddManager,temp,uVars,
00932                                                 xVars,nVars));
00933       bdd_recursive_deref(ddManager,temp);
00934       (void) fprintf(vis_stdout,"** restr diag: Class members:\n");
00935       RestrPrintBddNode(ddManager,oneClass);
00936       bdd_recursive_deref(ddManager,oneClass);
00937 
00938       /* Remove rep from classes */
00939       bdd_ref(temp = bdd_bdd_and(ddManager,classes,bdd_not_bdd_node(rep)));
00940       bdd_recursive_deref(ddManager,rep);
00941       bdd_recursive_deref(ddManager,classes);
00942       classes = temp;
00943     }
00944     (void) fprintf(vis_stdout,"** restr diag: Number of classes = %d\n",i);
00945   }
00946 #endif
00947 
00948   /* Compute uCube and extract the u variables from resultXU */
00949   bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
00950   bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube));
00951   bdd_recursive_deref(ddManager,uCube);
00952   bdd_recursive_deref(ddManager,resultXU);
00953 
00954   fprintf(vis_stdout, "** restr info: Number of Equivalence Classes = %g\n",
00955           bdd_count_minterm(ddManager,classes,nVars));
00956   
00957   bdd_recursive_deref(ddManager,classes);
00958 }
00959 
00960 
00970 static array_t *
00971 GetBddArrayFromMvfArray(array_t *mvfArray)
00972 {
00973   int     i;
00974   array_t *bddArray;
00975   Mvf_Function_t *mvf;
00976 
00977   bddArray = array_alloc(bdd_node *,0);
00978 
00979   arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
00980     mdd_t     *mddTemp;
00981     bdd_node    *ddNode;
00982 
00983     mddTemp = array_fetch(mdd_t *, mvf, 1);
00984     ddNode = bdd_extract_node_as_is(mddTemp);
00985     bdd_ref(ddNode);
00986 
00987     array_insert_last(bdd_node *, bddArray, ddNode);
00988   }
00989   return bddArray;
00990 }
00991 
01002 static bdd_node *
01003 DoMarkovPowerAnalysis(
01004   bdd_manager *ddManager,
01005   bdd_node *prunedTR,
01006   bdd_node *initBdd,
01007   bdd_node **piVars,
01008   bdd_node **xVars,
01009   bdd_node **yVars,
01010   st_table *inputProb,
01011   int nVars,
01012   int nPi)
01013 {
01014   bdd_node **result, *stateProbs;
01015   bdd_node *init;
01016   
01017   bdd_ref(init = bdd_bdd_to_add(ddManager,initBdd));
01018   if (restrVerbose) 
01019     (void) fprintf(vis_stdout,"** restr info: Initial average state bit change:\n");
01020 
01021   result = AddPowerSolve(ddManager,prunedTR,init,xVars,yVars,
01022                               piVars,inputProb,nVars,nPi);
01023   
01024   bdd_recursive_deref(ddManager,result[1]);
01025   stateProbs = result[0];
01026   bdd_recursive_deref(ddManager,init);
01027   FREE(result);
01028   
01029   return stateProbs;
01030 }
01031 
01041 static array_t *
01042 ExtractTransitionFuns(
01043   bdd_manager   *ddManager,
01044   bdd_node      *finalTR,
01045   bdd_node      **yVars,
01046   int           nVars)
01047 {
01048   bdd_node      *completeCube, *extractCube;
01049   bdd_node      *fun, *tranFun;
01050   array_t       *allTranFuns;
01051   int           i;
01052 
01053   allTranFuns = array_alloc(bdd_node *,0);
01054 
01055   completeCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars);
01056   bdd_ref(completeCube);
01057 
01058   for(i = 0;i < nVars; i++) {
01059     extractCube = bdd_bdd_cofactor(ddManager,completeCube,yVars[i]);
01060     bdd_ref(extractCube);
01061     fun = bdd_bdd_exist_abstract(ddManager,finalTR,extractCube);
01062     bdd_ref(fun);
01063     bdd_recursive_deref(ddManager,extractCube);
01064     tranFun = bdd_bdd_cofactor(ddManager,fun,yVars[i]);
01065     bdd_ref(tranFun);
01066 
01067 #ifdef RESTR_DIAG
01068     {
01069       /* The following is to test if there are multiple edges out of a state
01070          with the same input label: in short to check if the relation is
01071          deterministic or not. */
01072 
01073       bdd_node *yBar,*yNot,*inter;
01074       bdd_ref(yNot = bdd_not_bdd_node(yVars[i]));
01075       bdd_ref(yBar = bdd_bdd_cofactor(ddManager,fun,yNot));
01076       bdd_recursive_deref(ddManager,yNot);
01077       bdd_ref(inter = bdd_bdd_and(ddManager,yBar,tranFun));
01078       yNot = bdd_not_bdd_node(bdd_read_one(ddManager));
01079       assert(inter == yNot);
01080       bdd_recursive_deref(ddManager,inter);
01081       bdd_recursive_deref(ddManager,yBar);
01082     }
01083 #endif
01084 
01085     bdd_recursive_deref(ddManager,fun);
01086     array_insert_last(bdd_node *,allTranFuns,tranFun);
01087   }
01088 
01089   bdd_recursive_deref(ddManager,completeCube);
01090   return allTranFuns;
01091 }
01092 
01102 static array_t *
01103 GetBddArrayFromNameArray(
01104   Fsm_Fsm_t *fsm,
01105   array_t *nameArray)
01106 {
01107   graph_t *partition;
01108   array_t *bdds,*mvfs;
01109   
01110   partition = Fsm_FsmReadPartition(fsm);
01111   mvfs = BuildFunctions(partition,nameArray);
01112   bdds = GetBddArrayFromMvfArray(mvfs);
01113   Mvf_FunctionArrayFree(mvfs);
01114 
01115   return bdds;
01116 }
01117 
01128 static void
01129 ExpandReachableSet(
01130   bdd_manager *ddManager,
01131   bdd_node **reachable,
01132   bdd_node *equivRel,
01133   bdd_node **xVars,
01134   bdd_node **uVars,
01135   int nVars)
01136 {
01137   bdd_node *xcube,*potUnReach,*extReach;
01138   bdd_node *temp1;
01139 
01140   bdd_ref(xcube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
01141   /* potUnReach = \exists_x (E(x,u) * R(x)) */
01142   bdd_ref(potUnReach = bdd_bdd_and_abstract(ddManager,*reachable,
01143                                             equivRel,xcube));
01144   bdd_recursive_deref(ddManager,xcube);
01145   /* temp1(x) = potUnReach(u) */
01146   bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,potUnReach,uVars,
01147                                          xVars,nVars));
01148   bdd_recursive_deref(ddManager,potUnReach);
01149   /* extReach(x) = R(x) + potUnReach(x) */
01150   bdd_ref(extReach = bdd_bdd_or(ddManager,*reachable,temp1));
01151   bdd_recursive_deref(ddManager,temp1);
01152   bdd_recursive_deref(ddManager,*reachable);
01153   *reachable = extReach;
01154 }
01155 
01165 static graph_t *
01166 CreateNewPartition(
01167   Ntk_Network_t *network,                  
01168   bdd_manager *ddManager,
01169   array_t *outBdds,
01170   array_t *nextBdds,
01171   array_t *outputArray,
01172   array_t *tranFunArray)
01173 {
01174   st_table *nameToMvf;
01175   graph_t *partition;
01176 
01177   /* Create a table of next state and output Mvfs with their names as key to
01178      the table. This table is used to create a partition for the network. */
01179   nameToMvf = CreateNameToMvfTable(ddManager,outBdds,nextBdds,
01180                                    outputArray,tranFunArray);
01181   /* Delete the old partition and old fsm as we dont need it any more */
01182   if (restrCreatedPart) {
01183     Ntk_NetworkFreeApplInfo(network,RESTR_PART_NETWORK_APPL_KEY);
01184     restrCreatedPart = 0;
01185   }
01186   if (restrCreatedFsm) {
01187     Ntk_NetworkFreeApplInfo(network,RESTR_FSM_NETWORK_APPL_KEY);
01188     restrCreatedFsm = 0;
01189   }
01190 
01191   /* Create a new partition from the new root functions */
01192   partition = Part_NetworkCreatePartitionFromMvfs(network,nameToMvf);
01193   Ntk_NetworkAddApplInfo(network, RESTR_PART_NETWORK_APPL_KEY,
01194                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
01195                          (void *) partition);
01196   st_foreach(nameToMvf,StMvfFree,NIL(char));
01197   st_free_table(nameToMvf);
01198 
01199   return partition;
01200 }
01201 
01213 static Fsm_Fsm_t *
01214 CreateNewFsm(
01215   Ntk_Network_t *network,
01216   graph_t *partition,
01217   bdd_manager *ddManager,
01218   bdd_node *finalTR,
01219   bdd_node *initBdd,
01220   bdd_node *reachable,
01221   bdd_node *stateProbs,
01222   bdd_node **xVars,
01223   bdd_node **yVars,
01224   bdd_node **piVars,
01225   st_table *inputProb,
01226   int nVars,
01227   int nPi)
01228 {
01229   Fsm_Fsm_t *fsm;
01230   mdd_t *reachStates;
01231   mdd_t *mddTemp;
01232   bdd_node *ddTemp;
01233   bdd_node **markovResult;
01234 
01235   /* Create a new Fsm for the restructured network. */
01236   fsm = Fsm_FsmCreateFromNetworkWithPartition(network,
01237                                               Part_PartitionDuplicate(partition));
01238   assert(fsm != NIL(Fsm_Fsm_t));
01239   Ntk_NetworkAddApplInfo(network, RESTR_FSM_NETWORK_APPL_KEY,
01240                          (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
01241                          (void *) fsm); 
01242   /* We need to update the initial states as the
01243      Fsm_FsmCreateFromNetworkWithPartition will pick up old initial state from
01244      the network. Fsm_FsmSetInitialStates deletes old inital states. */
01245   mddTemp = bdd_construct_bdd_t(ddManager,initBdd);
01246   Fsm_FsmSetInitialStates(fsm,mddTemp);
01247 
01248   /* Compute the new reachable states */
01249   reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
01250                                               Fsm_Rch_Default_c,0,0,
01251                                               NIL(array_t),FALSE, NIL(array_t));
01252 
01253   bdd_recursive_deref(ddManager,reachable);
01254   reachable = bdd_extract_node_as_is(reachStates);
01255   bdd_ref(reachable);
01256   mdd_free(reachStates);
01257         
01258   /* Constrain the transition relation */
01259   bdd_ref(ddTemp = bdd_bdd_constrain(ddManager,finalTR,reachable));
01260   bdd_recursive_deref(ddManager,finalTR);
01261   finalTR = ddTemp;
01262 
01263   /* Use the state probs. of the original STG as the initial guess to compute
01264      the state probs. of the restructured STG. */
01265   if (restrVerbose)
01266     (void) fprintf(vis_stdout,"** restr info: Final average state bit change:\n");
01267 
01268   markovResult = AddPowerSolve(ddManager, finalTR, stateProbs, xVars,
01269                                     yVars,piVars,inputProb,nVars,nPi);
01270   bdd_recursive_deref(ddManager, markovResult[0]);
01271   bdd_recursive_deref(ddManager, markovResult[1]);
01272   FREE(markovResult);
01273         
01274   bdd_recursive_deref(ddManager,stateProbs);
01275   bdd_recursive_deref(ddManager,finalTR);
01276   bdd_recursive_deref(ddManager,reachable);
01277 
01278   return fsm;
01279 }