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