distr/nanotrav/ntrShort.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [ntrShort.c]
   4
   5   PackageName [ntr]
   6
   7   Synopsis    [Symbolic shortest paths algorithms.]
   8
   9   Description [This file contains the functions that implement the
  10   symbolic version of several shortest path algorithms described in the
  11   JFM paper on ADDs.]
  12
  13   Author      [Fabio Somenzi, Iris Bahar]
  14
  15   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  16
  17   All rights reserved.
  18
  19   Redistribution and use in source and binary forms, with or without
  20   modification, are permitted provided that the following conditions
  21   are met:
  22
  23   Redistributions of source code must retain the above copyright
  24   notice, this list of conditions and the following disclaimer.
  25
  26   Redistributions in binary form must reproduce the above copyright
  27   notice, this list of conditions and the following disclaimer in the
  28   documentation and/or other materials provided with the distribution.
  29
  30   Neither the name of the University of Colorado nor the names of its
  31   contributors may be used to endorse or promote products derived from
  32   this software without specific prior written permission.
  33
  34   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  35   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  36   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  37   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  38   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  39   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  40   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  41   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  42   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  43   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  44   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  45   POSSIBILITY OF SUCH DAMAGE.]
  46
  47 ******************************************************************************/
  48
  49 #include "ntr.h"
  50 #include "cuddInt.h"
  51
  52 /*---------------------------------------------------------------------------*/
  53 /* Constant declarations                                                     */
  54 /*---------------------------------------------------------------------------*/
  55
  56 /*---------------------------------------------------------------------------*/
  57 /* Stucture declarations                                                     */
  58 /*---------------------------------------------------------------------------*/
  59
  60 /*---------------------------------------------------------------------------*/
  61 /* Type declarations                                                         */
  62 /*---------------------------------------------------------------------------*/
  63
  64 /*---------------------------------------------------------------------------*/
  65 /* Variable declarations                                                     */
  66 /*---------------------------------------------------------------------------*/
  67
  68 #ifndef lint
  69 static char rcsid[] UTIL_UNUSED = "$Id: ntrShort.c,v 1.4 2004/08/13 18:28:28 fabio Exp fabio $";
  70 #endif
  71
  72 /*---------------------------------------------------------------------------*/
  73 /* Macro declarations                                                        */
  74 /*---------------------------------------------------------------------------*/
  75
  76 /**AutomaticStart*************************************************************/
  77
  78 /*---------------------------------------------------------------------------*/
  79 /* Static function prototypes                                                */
  80 /*---------------------------------------------------------------------------*/
  81
  82 static DdNode * ntrBellman (DdManager *dd, DdNode *D, DdNode *source, DdNode **x, DdNode **y, int vars, int pr);
  83 static DdNode * ntrWarshall (DdManager *dd, DdNode *D, DdNode **x, DdNode **y, int vars, int pr);
  84 static DdNode * ntrSquare (DdManager *dd, DdNode *D, DdNode **x, DdNode **y, DdNode **z, int vars, int pr, int st);
  85
  86 /**AutomaticEnd***************************************************************/
  87
  88 /*---------------------------------------------------------------------------*/
  89 /* Definition of exported functions                                          */
  90 /*---------------------------------------------------------------------------*/
  91
  92 /**Function********************************************************************
  93
  94   Synopsis    [Computes shortest paths in a state graph.]
  95
  96   Description [Computes shortest paths in the state transition graph of
  97   a network.  Three methods are availabe:
  98   <ul>
  99   <li> Bellman-Ford algorithm for single-source shortest paths; the
 100   algorithm computes the distance (number of transitions) from the initial
 101   states to all states.
 102   <li> Floyd-Warshall algorithm for all-pair shortest paths.
 103   <li> Repeated squaring algorithm for all-pair shortest paths.
 104   </ul>
 105   The function returns 1 in case of success; 0 otherwise.
 106   ]
 107
 108   SideEffects [ADD variables are created in the manager.]
 109
 110   SeeAlso     []
 111
 112 ******************************************************************************/
 113 int
 114 Ntr_ShortestPaths(
 115   DdManager * dd,
 116   BnetNetwork * net,
 117   NtrOptions * option)
 118 {
 119     NtrPartTR *TR;
 120     DdNode *edges, *source, *res, *r, *q, *bddSource;
 121     DdNode **xadd, **yadd, **zadd;
 122     int i;
 123     int pr = option->verb;
 124     int algorithm = option->shortPath;
 125     int selectiveTrace = option->selectiveTrace;
 126     int nvars = net->nlatches;
 127
 128     /* Set background to infinity for shortest paths. */
 129     Cudd_SetBackground(dd,Cudd_ReadPlusInfinity(dd));
 130
 131     /* Build the monolithic TR. */
 132     TR = Ntr_buildTR(dd,net,option,NTR_IMAGE_MONO);
 133
 134     /* Build the ADD variable vectors for x and y. */
 135     xadd = ALLOC(DdNode *, nvars);
 136     yadd = ALLOC(DdNode *, nvars);
 137     for(i = 0; i < nvars; i++) {
 138         q = Cudd_addIthVar(dd,TR->x[i]->index);
 139         Cudd_Ref(q);
 140         xadd[i] = q;
 141         q = Cudd_addIthVar(dd,TR->y[i]->index);
 142         Cudd_Ref(q);
 143         yadd[i] = q;
 144     }
 145
 146     /* Convert the transition relation BDD into an ADD... */
 147     q = Cudd_BddToAdd(dd,TR->part[0]);
 148     Cudd_Ref(q);
 149     /* ...replacing zeroes with infinities... */
 150     r = Cudd_addIte(dd,q,Cudd_ReadOne(dd),Cudd_ReadPlusInfinity(dd));
 151     Cudd_Ref(r);
 152     Cudd_RecursiveDeref(dd,q);
 153     /* ...and zeroing the diagonal. */
 154     q = Cudd_addXeqy(dd,nvars,xadd,yadd);
 155     Cudd_Ref(q);
 156     edges = Cudd_addIte(dd,q,Cudd_ReadZero(dd),r);
 157     Cudd_Ref(edges);
 158     Cudd_RecursiveDeref(dd,r);
 159     Cudd_RecursiveDeref(dd,q);
 160
 161     switch(algorithm) {
 162     case NTR_SHORT_BELLMAN:
 163         bddSource = Ntr_initState(dd,net,option);
 164         source = Cudd_BddToAdd(dd,bddSource);
 165         Cudd_Ref(source);
 166         res = ntrBellman(dd,edges,source,xadd,yadd,nvars,pr);
 167         if (res == NULL) return(0);
 168         Cudd_Ref(res);
 169         Cudd_RecursiveDeref(dd,source);
 170         Cudd_RecursiveDeref(dd,bddSource);
 171         if (pr >= 0) {
 172             (void) fprintf(stdout,"Distance Matrix");
 173             Cudd_PrintDebug(dd,res,nvars,pr);
 174         }
 175         break;
 176     case NTR_SHORT_FLOYD:
 177         res = ntrWarshall(dd,edges,xadd,yadd,nvars,pr);
 178         if (res == NULL) return(0);
 179         Cudd_Ref(res);
 180         if (pr >= 0) {
 181             (void) fprintf(stdout,"Distance Matrix");
 182             Cudd_PrintDebug(dd,res,2*nvars,pr);
 183         }
 184         break;
 185     case NTR_SHORT_SQUARE:
 186         /* Create a third set of ADD variables. */
 187         zadd = ALLOC(DdNode *, nvars);
 188         for(i = 0; i < nvars; i++) {
 189             int level;
 190             level = Cudd_ReadIndex(dd,TR->x[i]->index);
 191             q = Cudd_addNewVarAtLevel(dd,level);
 192             Cudd_Ref(q);
 193             zadd[i] = q;
 194         }
 195         /* Compute the shortest paths. */
 196         res = ntrSquare(dd,edges,zadd,yadd,xadd,nvars,pr,selectiveTrace);
 197         if (res == NULL) return(0);
 198         Cudd_Ref(res);
 199         /* Dispose of the extra variables. */
 200         for(i = 0; i < nvars; i++) {
 201             Cudd_RecursiveDeref(dd,zadd[i]);
 202         }
 203         FREE(zadd);
 204         if (pr >= 0) {
 205             (void) fprintf(stdout,"Distance Matrix");
 206             Cudd_PrintDebug(dd,res,2*nvars,pr);
 207         }
 208         break;
 209     default:
 210         (void) printf("Unrecognized method. Try again.\n");
 211         return(0);
 212     }
 213
 214     /* Here we should compute the paths. */
 215
 216     /* Clean up. */
 217     Ntr_freeTR(dd,TR);
 218     Cudd_RecursiveDeref(dd,edges);
 219     Cudd_RecursiveDeref(dd,res);
 220     for(i = 0; i < nvars; i++) {
 221         Cudd_RecursiveDeref(dd,xadd[i]);
 222         Cudd_RecursiveDeref(dd,yadd[i]);
 223     }
 224     FREE(xadd);
 225     FREE(yadd);
 226
 227     if (option->autoDyn & 1) {
 228         (void) printf("Order after short path computation\n");
 229         if (!Bnet_PrintOrder(net,dd)) return(0);
 230     }
 231
 232     return(1);
 233
 234 } /* end of Ntr_ShortestPaths */
 235
 236
 237 /*---------------------------------------------------------------------------*/
 238 /* Definition of internal functions                                          */
 239 /*---------------------------------------------------------------------------*/
 240
 241 /*---------------------------------------------------------------------------*/
 242 /* Definition of static functions                                            */
 243 /*---------------------------------------------------------------------------*/
 244
 245
 246 /**Function********************************************************************
 247
 248   Synopsis    [Bellman-Ford algorithm for single-source shortest paths.]
 249
 250   Description [Bellman-Ford algorithm for single-source shortest
 251   paths.  Returns the vector of the distances of all states from the
 252   initial states.  In case of multiple initial states the distance for
 253   each state is from the nearest initial state.  Negative-weight
 254   cycles are detected, though only in the naive way.  (Lack of
 255   convergence after nodes-1 iterations.)  In such a case, a constant
 256   ADD with value minus infinity is returned.  Bellman-Ford is based on
 257   matrix-vector multiplication.  The matrix is the distance matrix
 258   D(x,y), such that D(a,b) is the length of the arc connecting state a
 259   to state b.  The vector V(x) stores the distances of all states from
 260   the initial states.  The actual vector used in the matrix-vector
 261   multiplication is diff(x), that holds those distances that have
 262   changed during the last update.]
 263
 264   SideEffects []
 265
 266   SeeAlso     [ntrWarshall ntrSquare]
 267
 268 ******************************************************************************/
 269 static DdNode *
 270 ntrBellman(
 271   DdManager *dd,
 272   DdNode *D,
 273   DdNode *source,
 274   DdNode **x,
 275   DdNode **y,
 276   int vars,
 277   int pr)
 278 {
 279     DdNode *u, *w, *V, *min, *diff;
 280     DdApaNumber i, nodes, one;
 281     int digits = vars + 1;
 282
 283     /* To avoid overflow when there are many variables, use APA. */
 284     nodes = Cudd_NewApaNumber(digits);
 285     Cudd_ApaPowerOfTwo(digits,nodes,vars);
 286     i = Cudd_NewApaNumber(digits);
 287     one = Cudd_NewApaNumber(digits);
 288     Cudd_ApaSetToLiteral(digits,one,1);
 289
 290 #if 0
 291     /* Find the distances from the initial state along paths using one
 292     ** arc. */
 293     w = Cudd_Cofactor(dd,D,source); /* works only if source is a cube */
 294     Cudd_Ref(w);
 295     V = Cudd_addSwapVariables(dd,w,x,y,vars);
 296     Cudd_Ref(V);
 297     Cudd_RecursiveDeref(dd,w);
 298 #endif
 299
 300     /* The initial states are at distance 0. The other states are
 301     ** initially at infinite distance. */
 302     V = Cudd_addIte(dd,source,Cudd_ReadZero(dd),Cudd_ReadPlusInfinity(dd));
 303     Cudd_Ref(V);
 304
 305     /* Selective trace algorithm.  For the next update, only consider the
 306     ** nodes whose distance has changed in the last update. */
 307     diff = V;
 308     Cudd_Ref(diff);
 309
 310     for (Cudd_ApaSetToLiteral(digits,i,1);
 311          Cudd_ApaCompare(digits,i,digits,nodes) < 0;
 312          Cudd_ApaAdd(digits,i,one,i)) {
 313         if (pr>2) {(void) printf("V"); Cudd_PrintDebug(dd,V,vars,pr);}
 314         /* Compute the distances via triangulation as a function of x. */
 315         w = Cudd_addTriangle(dd,diff,D,x,vars);
 316         Cudd_Ref(w);
 317         Cudd_RecursiveDeref(dd,diff);
 318         u = Cudd_addSwapVariables(dd,w,x,y,vars);
 319         Cudd_Ref(u);
 320         Cudd_RecursiveDeref(dd,w);
 321         if (pr>2) {(void) printf("u"); Cudd_PrintDebug(dd,u,vars,pr);}
 322
 323         /* Take the minimum of the previous distances and those just
 324         ** computed. */
 325         min = Cudd_addApply(dd,Cudd_addMinimum,V,u);
 326         Cudd_Ref(min);
 327         Cudd_RecursiveDeref(dd,u);
 328         if (pr>2) {(void) printf("min"); Cudd_PrintDebug(dd,min,vars,pr);}
 329
 330         if (V == min) {         /* convergence */
 331             Cudd_RecursiveDeref(dd,min);
 332             if (pr>0) {
 333                 (void) printf("Terminating after ");
 334                 Cudd_ApaPrintDecimal(stdout,digits,i);
 335                 (void) printf(" iterations\n");
 336             }
 337             break;
 338         }
 339         /* Find the distances that decreased. */
 340         diff = Cudd_addApply(dd,Cudd_addDiff,V,min);
 341         Cudd_Ref(diff);
 342         if (pr>2) {(void) printf("diff"); Cudd_PrintDebug(dd,diff,vars,pr);}
 343         Cudd_RecursiveDeref(dd,V);
 344         V = min;
 345     }
 346     /* Negative cycle detection. */
 347     if (Cudd_ApaCompare(digits,i,digits,nodes) == 0 &&
 348         diff != Cudd_ReadPlusInfinity(dd)) {
 349         (void) printf("Negative cycle\n");
 350         Cudd_RecursiveDeref(dd,diff);
 351         Cudd_RecursiveDeref(dd,V);
 352         V = Cudd_ReadMinusInfinity(dd);
 353         Cudd_Ref(V);
 354     }
 355
 356     Cudd_Deref(V);
 357     FREE(i);
 358     FREE(nodes);
 359     FREE(one);
 360     return(V);
 361
 362 } /* end of ntrBellman */
 363
 364
 365 /**Function********************************************************************
 366
 367   Synopsis    [Floyd-Warshall algorithm for all-pair shortest paths.]
 368
 369   Description []
 370
 371   SideEffects []
 372
 373   SeeAlso     []
 374
 375 ******************************************************************************/
 376 static DdNode *
 377 ntrWarshall(
 378   DdManager *dd,
 379   DdNode *D,
 380   DdNode **x,
 381   DdNode **y,
 382   int vars,
 383   int pr)
 384 {
 385     DdNode *one, *zero;
 386     DdNode *xminterm,  *w, *V, *V2;
 387     DdNode *P, *R;
 388     int i;
 389     int nodes;
 390     int k,u;
 391     long start_time;
 392     if (vars > 30)
 393         nodes = 1000000000;
 394     else
 395         nodes = 1 << vars;
 396
 397     one = DD_ONE(dd);
 398     zero = DD_ZERO(dd);
 399     Cudd_Ref(R = D);                        /* make copy of original matrix */
 400
 401     /* Extract pivot row and column from D */
 402     start_time = util_cpu_time();
 403     for (k = 0; k < nodes; k++) {
 404         if (k % 10000 == 0) {
 405             (void) printf("Starting iteration  %d  at time %s\n",
 406                           k,util_print_time(util_cpu_time() - start_time));
 407         }
 408         Cudd_Ref(xminterm = one);
 409         u = k;
 410         for (i = vars-1; i >= 0; i--) {
 411             if (u&1) {
 412                 Cudd_Ref(w = Cudd_addIte(dd,x[i],xminterm,zero));
 413             } else {
 414                 Cudd_Ref(w = Cudd_addIte(dd,x[i],zero,xminterm));
 415             }
 416             Cudd_RecursiveDeref(dd,xminterm);
 417             xminterm = w;
 418             u >>= 1;
 419         }
 420
 421         Cudd_Ref(V = Cudd_Cofactor(dd,R,xminterm));
 422         Cudd_RecursiveDeref(dd,xminterm);
 423         if (pr>2) {(void) printf("V"); Cudd_PrintDebug(dd,V,vars,pr);}
 424
 425
 426         Cudd_Ref(xminterm = one);
 427         u = k;
 428         for (i = vars-1; i >= 0; i--) {
 429             if (u&1) {
 430                 Cudd_Ref(w = Cudd_addIte(dd,y[i],xminterm,zero));
 431             } else {
 432                 Cudd_Ref(w = Cudd_addIte(dd,y[i],zero,xminterm));
 433             }
 434             Cudd_RecursiveDeref(dd,xminterm);
 435             xminterm = w;
 436             u >>= 1;
 437         }
 438
 439         Cudd_Ref(V2 = Cudd_Cofactor(dd,R,xminterm));
 440         Cudd_RecursiveDeref(dd,xminterm);
 441         if (pr>2) {(void) printf("V2"); Cudd_PrintDebug(dd,V2,vars,pr);}
 442
 443         Cudd_Ref(P = Cudd_addOuterSum(dd,R,V,V2));
 444
 445         Cudd_RecursiveDeref(dd,V);
 446         Cudd_RecursiveDeref(dd,V2);
 447         Cudd_RecursiveDeref(dd,R);
 448         R = P;
 449         if (pr>2) {(void) printf("R"); Cudd_PrintDebug(dd,R,vars,pr);}
 450     }
 451
 452     Cudd_Deref(R);
 453     return(R);
 454
 455 } /* end of ntrWarshall */
 456
 457
 458 /**Function********************************************************************
 459
 460   Synopsis    [Repeated squaring algorithm for all-pairs shortest paths.]
 461
 462   Description []
 463
 464   SideEffects []
 465
 466   SeeAlso     []
 467
 468 ******************************************************************************/
 469 static DdNode *
 470 ntrSquare(
 471   DdManager *dd /* manager */,
 472   DdNode *D /* D(z,y): distance matrix */,
 473   DdNode **x /* array of x variables */,
 474   DdNode **y /* array of y variables */,
 475   DdNode **z /* array of z variables */,
 476   int vars /* number of variables in each of the three arrays */,
 477   int pr /* verbosity level */,
 478   int st /* use the selective trace algorithm */)
 479 {
 480     DdNode *zero;
 481     DdNode *I;              /* identity matirix */
 482     DdNode *w, *V, *P, *M, *R, *RT;
 483     DdNode *diff, *min, *minDiag;
 484     int n;
 485     int neg;
 486     long start_time;
 487
 488     zero = Cudd_ReadZero(dd);
 489     /* Make a working copy of the original matrix. */
 490     R = D;
 491     Cudd_Ref(R);
 492     I = Cudd_addXeqy(dd,vars,z,y);    /* identity matrix */
 493     Cudd_Ref(I);
 494
 495     /* Make a copy of the matrix for the selective trace algorithm. */
 496     diff = R;
 497     Cudd_Ref(diff);
 498
 499     start_time = util_cpu_time();
 500     for (n = vars; n >= 0; n--) {
 501         printf("Starting iteration %d at time %s\n",vars-n,
 502                util_print_time(util_cpu_time() - start_time));
 503
 504         /* Check for negative cycles: They are identified by negative
 505         ** elements on the diagonal.
 506         */
 507
 508         /* Extract values from the diagonal. */
 509         Cudd_Ref(w = Cudd_addIte(dd,I,R,zero));
 510         minDiag = Cudd_addFindMin(dd,w);        /* no need to ref */
 511         neg = Cudd_V(minDiag) < 0;
 512         Cudd_RecursiveDeref(dd,w);
 513         if (neg) {
 514             Cudd_RecursiveDeref(dd,diff);
 515             (void) printf("Negative cycle after %d iterations!\n",vars-n);
 516             break;
 517         }
 518
 519         /* Prepare the first operand of matrix multiplication:
 520         **   diff(z,y) -> RT(x,y) -> V(x,z)
 521         */
 522
 523         /* RT(x,y) */
 524         Cudd_Ref(RT = Cudd_addSwapVariables(dd,diff,x,z,vars));
 525         Cudd_RecursiveDeref(dd,diff);
 526         /* V(x,z) */
 527         Cudd_Ref(V = Cudd_addSwapVariables(dd,RT,y,z,vars));
 528         Cudd_RecursiveDeref(dd,RT);
 529         if (pr > 0) {
 530             double pathcount;
 531             (void) printf("V"); Cudd_PrintDebug(dd,V,2*vars,pr);
 532             pathcount = Cudd_CountPath(V);
 533             (void) printf("Path count = %g\n", pathcount);
 534         }
 535
 536         /* V(x,z) * R(z,y) -> P(x,y) */
 537         Cudd_Ref(P = Cudd_addTriangle(dd,V,R,z,vars));
 538         Cudd_RecursiveDeref(dd,V);
 539         /* P(x,y) => M(z,y) */
 540         Cudd_Ref(M = Cudd_addSwapVariables(dd,P,x,z,vars));
 541         Cudd_RecursiveDeref(dd,P);
 542         if (pr>0) {(void) printf("M"); Cudd_PrintDebug(dd,M,2*vars,pr);}
 543
 544         /* min(z,y) */
 545         Cudd_Ref(min = Cudd_addApply(dd,Cudd_addMinimum,R,M));
 546         Cudd_RecursiveDeref(dd,M);
 547
 548         if (R == min) {
 549             Cudd_RecursiveDeref(dd,min);
 550             if (pr>0) {printf("Done after %d iterations\n",vars-n+1); }
 551             break;
 552         }
 553         /* diff(z,y) */
 554         if (st) {
 555             Cudd_Ref(diff = Cudd_addApply(dd,Cudd_addDiff,min,R));
 556         } else {
 557             Cudd_Ref(diff = min);
 558         }
 559         Cudd_RecursiveDeref(dd,R);
 560         R = min;                  /* keep a copy of matrix at current iter. */
 561         if (pr > 0) {
 562             double pathcount;
 563             (void) printf("R"); Cudd_PrintDebug(dd,R,2*vars,pr);
 564             pathcount = Cudd_CountPath(R);
 565             (void) printf("Path count = %g\n", pathcount);
 566         }
 567
 568         if (n == 0) {
 569             (void) printf("Negative cycle!\n");
 570             break;
 571         }
 572
 573     }
 574     Cudd_RecursiveDeref(dd,I);
 575     Cudd_Deref(R);
 576     return(R);
 577
 578 } /* end of ntrSquare */