VIS

src/restr/restrFaninout.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 
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Macro declarations                                                        */
00050 /*---------------------------------------------------------------------------*/
00051 
00052 
00055 /*---------------------------------------------------------------------------*/
00056 /* Static function prototypes                                                */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 
00063 /*---------------------------------------------------------------------------*/
00064 /* Definition of exported functions                                          */
00065 /*---------------------------------------------------------------------------*/
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Definition of internal functions                                          */
00069 /*---------------------------------------------------------------------------*/
00070 
00097 bdd_node *
00098 RestrMinimizeFsmByFaninFanout(
00099   bdd_manager *ddManager,
00100   bdd_node *equivRel,
00101   bdd_node *oldTR,
00102   bdd_node **addPTR,
00103   bdd_node **possessedProbMatrix,
00104   bdd_node *initBdd,
00105   bdd_node *reachable,
00106   bdd_node *stateProbs,
00107   bdd_node **piVars,
00108   bdd_node **xVars,
00109   bdd_node **yVars,
00110   bdd_node **uVars,
00111   bdd_node **vVars,
00112   int nVars,
00113   int nPi,
00114   RestructureHeuristic heuristic,
00115   array_t **outBdds,
00116   bdd_node **newInit)
00117 {
00118   bdd_node *temp1, *temp2, *temp3;
00119   bdd_node *xCube, *yCube;
00120   bdd_node *Rxy,*Rxv;
00121   bdd_node *RxvgtRxy, *RxveqRxy; /* These are BDDs */
00122   bdd_node **xAddVars,**yAddVars,**vAddVars;
00123   bdd_node *priority, *result, *matrix;
00124   bdd_node *newEquivRel;
00125   bdd_node *oneInitState;
00126   bdd_node *hammingWeight;
00127   bdd_node *lhs, *rhs;
00128   bdd_node *bddCProj;
00129   bdd_node *bddCProjvy, *addCProjvy;
00130   bdd_node *newCProjvy, *newCProjux;
00131   bdd_node *zeroProbs, *zeroProbFactor;
00132   bdd_node *weight;
00133 
00134   array_t *newOutBdds;
00135   int i, index;
00136 
00137   /* Collect the ADD variables for futre use */
00138   xAddVars = ALLOC(bdd_node *,nVars);
00139   yAddVars = ALLOC(bdd_node *,nVars);
00140   vAddVars = ALLOC(bdd_node *,nVars);
00141 
00142   for(i = 0; i < nVars; i++) {
00143     index = bdd_node_read_index(yVars[i]);
00144     bdd_ref(yAddVars[i] = bdd_add_ith_var(ddManager,index));
00145     index = bdd_node_read_index(vVars[i]);
00146     bdd_ref(vAddVars[i] = bdd_add_ith_var(ddManager,index));
00147     index = bdd_node_read_index(xVars[i]);
00148     bdd_ref(xAddVars[i] = bdd_add_ith_var(ddManager,index));
00149   }
00150 
00151   /* Restrict the equivalence relation only to the reachable states */
00152   /* temp1 = R(v) */
00153   bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,reachable,xVars,
00154                                          vVars,nVars));
00155   /* temp2 = R(y) */
00156   bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,reachable,xVars,
00157                                          yVars,nVars));
00158   /* temp3 = R(v) * R(y) */
00159   bdd_ref(temp3 = bdd_bdd_and(ddManager,temp1,temp2));
00160   bdd_recursive_deref(ddManager,temp1);
00161   bdd_recursive_deref(ddManager,temp2);
00162   /* newEquivRel(v,y) = E(v,y) * R(v) * R(y) */
00163   bdd_ref(newEquivRel = bdd_bdd_and(ddManager,equivRel,temp3));
00164   bdd_recursive_deref(ddManager,temp3);
00165 
00166   /* Select one state from the set of initial states */
00167   oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
00168   bdd_ref(oneInitState);
00169 
00170   /* Initially an arbitrary choice of a 'nominal representative' for each
00171      equivalence class is made--using compatible projection--with the initial
00172      state as the reference vertex. bddCProj is as the name indicates, in terms
00173      of y and x. bddCProj refers to $\Psi(x,y)$ in the ISLPED 97 reference. */
00174 
00175   bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,oneInitState,xVars,
00176                                          vVars,nVars));
00177   bdd_recursive_deref(ddManager,oneInitState);
00178   bdd_ref(bddCProjvy = bdd_bdd_cprojection(ddManager, newEquivRel, temp1));
00179   bdd_recursive_deref(ddManager,newEquivRel);
00180   bdd_recursive_deref(ddManager,temp1);
00181   bdd_ref(bddCProj = bdd_bdd_swap_variables(ddManager,bddCProjvy,vVars,
00182                                             xVars,nVars));
00183   bdd_ref(addCProjvy = bdd_bdd_to_add(ddManager,bddCProjvy));
00184   bdd_recursive_deref(ddManager,bddCProjvy);
00185 
00186   /* Let's compute the weight matrix */
00187   /* hammingWeight equal (nVars - HD(x,y)) */
00188   bdd_ref(temp1 = bdd_add_const(ddManager,(double)nVars));
00189   bdd_ref(temp2 = bdd_add_hamming(ddManager,xVars,yVars,nVars));
00190   bdd_ref(hammingWeight = bdd_add_apply(ddManager,bdd_add_minus,
00191                                         temp1,temp2));
00192   bdd_recursive_deref(ddManager,temp1);
00193   bdd_recursive_deref(ddManager,temp2);
00194 
00195   /* temp1 = possessedProbMatrix * (nVars - HD(x,y)) */
00196   bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_times,hammingWeight,
00197                                 *possessedProbMatrix));
00198   bdd_recursive_deref(ddManager,*possessedProbMatrix);
00199 
00200   /* matrix = possessedProbMatrix * (nVars - HD(x,y)) * stateProbs */
00201   bdd_ref(matrix = bdd_add_apply(ddManager,bdd_add_times,temp1,
00202                                  stateProbs));
00203   bdd_recursive_deref(ddManager,temp1);
00204 
00205   /* Compute the contribution of the edges that have a state with zero
00206    * probability as its source node. The contribution is measured in terms
00207    * of the hamming distance between the end points of the edge.
00208    * The total weight on any edge is the sum of "matrix" as computed
00209    * above and "zeroProbFactor" as computed below.
00210    */
00211   bdd_ref(temp1 = bdd_add_bdd_strict_threshold(ddManager,stateProbs,0.0));
00212   bdd_ref(temp2 = bdd_not_bdd_node(temp1));
00213   bdd_recursive_deref(ddManager,temp1);
00214   /* zeroProbs evaluates to 1 for those states which have zero steady state
00215    * probability. zeroProbs is a 0-1 ADD.
00216    */
00217   bdd_ref(zeroProbs = bdd_bdd_to_add(ddManager,temp2));
00218   bdd_recursive_deref(ddManager,temp2);
00219 
00220   /* temp1 = (1 - HD(x,y)/nVars) */
00221   bdd_ref(temp2 = bdd_add_const(ddManager,(double)nVars));
00222   bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_divide,hammingWeight,
00223                                 temp2));
00224   bdd_recursive_deref(ddManager,temp2);
00225   bdd_recursive_deref(ddManager,hammingWeight);
00226 
00227   /* temp2 = (1 - HD(x,y)/nVars) * zeroProbs(x) */
00228   bdd_ref(temp2 = bdd_add_apply(ddManager,bdd_add_times,temp1,zeroProbs));
00229   bdd_recursive_deref(ddManager,temp1);
00230   bdd_recursive_deref(ddManager,zeroProbs);
00231 
00232   /* zeroProbFactor = (1 - HD(x,y)/nVars) * zeroProbs(x) * addPTR */
00233   bdd_ref(zeroProbFactor = bdd_add_apply(ddManager,bdd_add_times,
00234                                          *addPTR,temp2));
00235   bdd_recursive_deref(ddManager,*addPTR);
00236   bdd_recursive_deref(ddManager,temp2);
00237 
00238   /* Total edge weight = matrix + zeroProbFactor */
00239   bdd_ref(weight = bdd_add_apply(ddManager,bdd_add_plus,matrix,
00240                                  zeroProbFactor));
00241   bdd_recursive_deref(ddManager,matrix);
00242   bdd_recursive_deref(ddManager,zeroProbFactor);
00243     
00244   /* lhs = Abs(x) (weight(x,y)*CProj(v,y)) */
00245   bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_times,weight,
00246                                 addCProjvy));
00247   bdd_ref(temp3 = bdd_add_compute_cube(ddManager,xAddVars,NIL(int),nVars));
00248   bdd_ref(lhs = bdd_add_exist_abstract(ddManager,temp1,temp3));
00249   bdd_recursive_deref(ddManager,temp1);
00250   bdd_recursive_deref(ddManager,temp3);
00251 
00252   /* Now lhs is a function of x and y */
00253   bdd_ref(temp1 = bdd_add_swap_variables(ddManager,lhs,vAddVars,xAddVars,
00254                                          nVars));
00255   bdd_recursive_deref(ddManager,lhs);
00256   lhs = temp1;
00257 
00258   if (heuristic == RestrFaninFanout_c) {
00259     /* let's compute the rhs */
00260     bdd_ref(temp1 = bdd_add_swap_variables(ddManager,addCProjvy,yAddVars,
00261                                            xAddVars, nVars));
00262     bdd_recursive_deref(ddManager,addCProjvy);
00263     bdd_ref(rhs = bdd_add_apply(ddManager,bdd_add_times,weight,temp1));
00264     bdd_recursive_deref(ddManager,temp1);
00265     bdd_recursive_deref(ddManager,weight);
00266     temp1 = rhs;
00267     bdd_ref(temp3 = bdd_add_compute_cube(ddManager,yAddVars,NIL(int),nVars));
00268     bdd_ref(rhs = bdd_add_exist_abstract(ddManager,temp1,temp3));
00269     bdd_recursive_deref(ddManager,temp1);
00270     bdd_recursive_deref(ddManager,temp3);
00271 
00272     /* rhs is now a function of x and y */
00273     bdd_ref(temp1 = bdd_add_swap_variables(ddManager,rhs,xAddVars,
00274                                            yAddVars,nVars));
00275     bdd_recursive_deref(ddManager,rhs);
00276     bdd_ref(rhs = bdd_add_swap_variables(ddManager,temp1,vAddVars,
00277                                          xAddVars,nVars));
00278     bdd_recursive_deref(ddManager,temp1);
00279 
00280     /* take the average of lhs and rhs */
00281     bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_plus,lhs,rhs));
00282     bdd_recursive_deref(ddManager,lhs);
00283     bdd_recursive_deref(ddManager,rhs);
00284     bdd_ref(temp2 = bdd_add_const(ddManager,(double)2.0));
00285     bdd_ref(Rxy = bdd_add_apply(ddManager,bdd_add_divide,temp1,temp2));
00286     bdd_recursive_deref(ddManager,temp1);
00287     bdd_recursive_deref(ddManager,temp2);  
00288   }
00289   else {
00290     bdd_recursive_deref(ddManager,weight);
00291     bdd_recursive_deref(ddManager,addCProjvy);
00292     Rxy = lhs;
00293   }
00294 
00295   /* Rxv = Rxy(x,v) */
00296   bdd_ref(Rxv = bdd_add_swap_variables(ddManager,Rxy,yAddVars,vAddVars,
00297                                        nVars));
00298   /* RxvgtRxy(x,v,y) = Rxv(x,v) > Rxy(x,y) */
00299   bdd_ref(temp1 = bdd_add_apply(ddManager,RestrAddMaximum,Rxv,Rxy));
00300   bdd_ref(RxvgtRxy = bdd_add_bdd_threshold(ddManager,temp1,(double) 1.0));
00301   bdd_recursive_deref(ddManager,temp1);
00302 
00303   /* RxveqRxy(x,v,y) = Rxz(x,v) == Rxy(x,y) */
00304   bdd_ref(temp1 = bdd_add_apply(ddManager,RestrAddEqual,Rxv,Rxy));
00305   bdd_ref(RxveqRxy = bdd_add_bdd_threshold(ddManager,temp1,(double) 1.0));
00306   bdd_recursive_deref(ddManager,temp1);
00307   bdd_recursive_deref(ddManager,Rxv);
00308   bdd_recursive_deref(ddManager,Rxy);
00309 
00310   /* temp1 is the tie-break function. (RxveqRxy . temp1 = temp2)*/
00311   bdd_ref(temp1 = bdd_dxygtdxz(ddManager,nVars,xVars,yVars,vVars));
00312   bdd_ref(temp2 = bdd_bdd_and(ddManager,RxveqRxy,temp1));
00313   bdd_recursive_deref(ddManager,temp1);
00314   bdd_recursive_deref(ddManager,RxveqRxy);
00315 
00316   bdd_ref(priority = bdd_bdd_or(ddManager,temp2,RxvgtRxy));
00317   bdd_recursive_deref(ddManager,RxvgtRxy);
00318   bdd_recursive_deref(ddManager,temp2);
00319 
00320   /* temp1 represents the pair (oldrepresentative,newprepresentative) in terms
00321    of x and y respectively */
00322   bdd_ref(temp1 = bdd_priority_select(ddManager,bddCProj,xVars,
00323                                       yVars,vVars,priority,nVars,NULL));
00324   bdd_recursive_deref(ddManager,priority);
00325 
00326   bdd_ref(xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
00327   bdd_ref(yCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars));
00328 
00329   /* newCProjvy is in terms of v,y */
00330   /* v represents the new representative of equivalent states */
00331 
00332   bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,temp1,yVars,vVars,
00333                                          nVars));
00334   bdd_recursive_deref(ddManager,temp1);
00335   bdd_ref(newCProjvy = bdd_bdd_and_abstract(ddManager,bddCProj,temp2,
00336                                             xCube));
00337   bdd_recursive_deref(ddManager,bddCProj);
00338   bdd_recursive_deref(ddManager,temp2);
00339 
00340   bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,newCProjvy,yVars,
00341                                          xVars,nVars));
00342   bdd_ref(newCProjux = bdd_bdd_swap_variables(ddManager,temp1,vVars,
00343                                               uVars,nVars));
00344   bdd_recursive_deref(ddManager,temp1);
00345 
00346   /* Change the output functions accordingly */
00347   newOutBdds = array_alloc(bdd_node *,0);
00348   arrayForEachItem(bdd_node *,*outBdds,i,temp3) {
00349     bdd_ref(temp1 = bdd_bdd_and_abstract(ddManager,temp3,newCProjux,
00350                                          xCube));
00351     bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,temp1,uVars,xVars,
00352                                            nVars));
00353     bdd_recursive_deref(ddManager,temp1);
00354     bdd_recursive_deref(ddManager,temp3);
00355     array_insert_last(bdd_node *,newOutBdds,temp2);
00356   }
00357   array_free(*outBdds);
00358   *outBdds = newOutBdds;
00359 
00360   /* Change the initBdd accordingly */
00361   bdd_ref(temp1 = bdd_bdd_and_abstract(ddManager,initBdd,newCProjux,xCube));
00362   bdd_ref(*newInit = bdd_bdd_swap_variables(ddManager,temp1,uVars,xVars,
00363                                             nVars));
00364   bdd_recursive_deref(ddManager,temp1);
00365 
00366   /* Compute the new transition relation w.r.t the new CProjection function.
00367    * result = newCProjux * oldTR(x,y) * newCProjvy 
00368    */
00369   bdd_ref(temp1 = bdd_bdd_and(ddManager,xCube,yCube));
00370   bdd_recursive_deref(ddManager,xCube);
00371   bdd_recursive_deref(ddManager,yCube);
00372   bdd_ref(temp2 = bdd_bdd_and(ddManager,newCProjux,oldTR));
00373   bdd_recursive_deref(ddManager,newCProjux);
00374   bdd_ref(temp3 = bdd_bdd_and(ddManager,temp2,newCProjvy));
00375   bdd_recursive_deref(ddManager,newCProjvy);
00376   bdd_recursive_deref(ddManager,temp2);
00377   bdd_ref(result = bdd_bdd_exist_abstract(ddManager,temp3,temp1));
00378   bdd_recursive_deref(ddManager,temp1);
00379   bdd_recursive_deref(ddManager,temp3);
00380 
00381   bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,result,uVars,xVars,
00382                                          nVars));
00383   bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,temp1,vVars,yVars,
00384                                          nVars));
00385   bdd_recursive_deref(ddManager,temp1);
00386   bdd_recursive_deref(ddManager,result);
00387   result = temp2;
00388 
00389   /* Clean up */
00390   for(i = 0; i < nVars; i++) {
00391     bdd_recursive_deref(ddManager,yAddVars[i]);
00392     bdd_recursive_deref(ddManager,vAddVars[i]);
00393     bdd_recursive_deref(ddManager,xAddVars[i]);
00394   }
00395   FREE(yAddVars);
00396   FREE(vAddVars);
00397   FREE(xAddVars);
00398   
00399   /* Return the restructred STG */
00400   return result;
00401 }
00402 
00403 
00404 /*---------------------------------------------------------------------------*/
00405 /* Definition of static functions                                            */
00406 /*---------------------------------------------------------------------------*/