distr/nanotrav/doc/ntrExtDet.html

   1 <html>
   2 <head><title>The ntr package</title></head>
   3 <body>
   4
   5 <h1>The ntr package</h1>
   6 <h2>Simple-minded package to do traversal.</h2>
   7 <h3></h3>
   8 <hr>
   9 <ul>
  10 <li><a href="ntrExtAbs.html"><h3>External abstracts</h3></a>
  11 <li><a href="ntrAllAbs.html"><h3>All abstracts</h3></a>
  12 <li><a href="ntrExtDet.html#prototypes"><h3>External functions</h3></a>
  13 <li><a href="ntrAllDet.html#prototypes"><h3>All functions</h3></a>
  14 </ul>
  15
  16 <hr>
  17
  18 <a name="description">
  19
  20 </a>
  21
  22 <hr>
  23 <!-- Function Prototypes and description -->
  24
  25 <dl>
  26 <a name="prototypes"></a>
  27 <dt><pre>
  28 int <i></i>
  29 <a name="Ntr_ClosureTrav"><b>Ntr_ClosureTrav</b></a>(
  30   DdManager * <b>dd</b>, <i>DD manager</i>
  31   BnetNetwork * <b>net</b>, <i>network</i>
  32   NtrOptions * <b>option</b> <i>options</i>
  33 )
  34 </pre>
  35 <dd> Traversal procedure. based on the transitive closure of the transition relation. Returns 1 in case of success; 0 otherwise.
  36 <p>
  37
  38 <dd> <b>Side Effects</b> None
  39 <p>
  40
  41 <dd> <b>See Also</b> <code><a href="ntrAllDet.html#Ntr_Trav">Ntr_Trav</a>
  42 </code>
  43
  44 <dt><pre>
  45 int <i></i>
  46 <a name="Ntr_Envelope"><b>Ntr_Envelope</b></a>(
  47   DdManager * <b>dd</b>, <i>DD manager</i>
  48   NtrPartTR * <b>TR</b>, <i>transition relation</i>
  49   FILE * <b>dfp</b>, <i>pointer to file for DD dump</i>
  50   NtrOptions * <b>option</b> <i>program options</i>
  51 )
  52 </pre>
  53 <dd> Poor man's outer envelope computation based on the monolithic transition relation. Returns 1 in case of success; 0 otherwise.
  54 <p>
  55
  56 <dd> <b>Side Effects</b> None
  57 <p>
  58
  59 <dt><pre>
  60 void <i></i>
  61 <a name="Ntr_FreeHeap"><b>Ntr_FreeHeap</b></a>(
  62   NtrHeap * <b>heap</b> <i></i>
  63 )
  64 </pre>
  65 <dd> Frees a priority queue.
  66 <p>
  67
  68 <dd> <b>Side Effects</b> None
  69 <p>
  70
  71 <dd> <b>See Also</b> <code><a href="ntrAllDet.html#Ntr_InitHeap">Ntr_InitHeap</a>
  72 </code>
  73
  74 <dt><pre>
  75 NtrHeap * <i></i>
  76 <a name="Ntr_HeapClone"><b>Ntr_HeapClone</b></a>(
  77   NtrHeap * <b>source</b> <i></i>
  78 )
  79 </pre>
  80 <dd> Clones a priority queue.
  81 <p>
  82
  83 <dd> <b>Side Effects</b> None
  84 <p>
  85
  86 <dd> <b>See Also</b> <code><a href="ntrAllDet.html#Ntr_InitHeap">Ntr_InitHeap</a>
  87 </code>
  88
  89 <dt><pre>
  90 int <i></i>
  91 <a name="Ntr_HeapCount"><b>Ntr_HeapCount</b></a>(
  92   NtrHeap * <b>heap</b> <i></i>
  93 )
  94 </pre>
  95 <dd> Returns the number of items in a priority queue.
  96 <p>
  97
  98 <dd> <b>Side Effects</b> None
  99 <p>
 100
 101 <dt><pre>
 102 int <i></i>
 103 <a name="Ntr_HeapExtractMin"><b>Ntr_HeapExtractMin</b></a>(
 104   NtrHeap * <b>heap</b>, <i></i>
 105   void ** <b>item</b>, <i></i>
 106   int * <b>key</b> <i></i>
 107 )
 108 </pre>
 109 <dd> Extracts the element with the minimum key from a priority queue. Returns 1 if successful; 0 otherwise.
 110 <p>
 111
 112 <dd> <b>Side Effects</b> The minimum key and the associated item are returned as side effects.
 113 <p>
 114
 115 <dd> <b>See Also</b> <code><a href="ntrAllDet.html#Ntr_HeapInsert">Ntr_HeapInsert</a>
 116 </code>
 117
 118 <dt><pre>
 119 int <i></i>
 120 <a name="Ntr_HeapInsert"><b>Ntr_HeapInsert</b></a>(
 121   NtrHeap * <b>heap</b>, <i></i>
 122   void * <b>item</b>, <i></i>
 123   int  <b>key</b> <i></i>
 124 )
 125 </pre>
 126 <dd> Inserts an item in a priority queue. Returns 1 if successful; 0 otherwise.
 127 <p>
 128
 129 <dd> <b>Side Effects</b> None
 130 <p>
 131
 132 <dd> <b>See Also</b> <code><a href="ntrAllDet.html#Ntr_HeapExtractMin">Ntr_HeapExtractMin</a>
 133 </code>
 134
 135 <dt><pre>
 136 NtrHeap * <i></i>
 137 <a name="Ntr_InitHeap"><b>Ntr_InitHeap</b></a>(
 138   int  <b>size</b> <i></i>
 139 )
 140 </pre>
 141 <dd> Initializes a priority queue. Returns a pointer to the heap if successful; NULL otherwise.
 142 <p>
 143
 144 <dd> <b>Side Effects</b> None
 145 <p>
 146
 147 <dd> <b>See Also</b> <code><a href="ntrAllDet.html#Ntr_FreeHeap">Ntr_FreeHeap</a>
 148 </code>
 149
 150 <dt><pre>
 151 int <i></i>
 152 <a name="Ntr_SCC"><b>Ntr_SCC</b></a>(
 153   DdManager * <b>dd</b>, <i>DD manager</i>
 154   BnetNetwork * <b>net</b>, <i>network</i>
 155   NtrOptions * <b>option</b> <i>options</i>
 156 )
 157 </pre>
 158 <dd> Computes the strongly connected components of the state transition graph. Only the first 10 SCCs are computed. Returns 1 in case of success; 0 otherwise.
 159 <p>
 160
 161 <dd> <b>Side Effects</b> None
 162 <p>
 163
 164 <dd> <b>See Also</b> <code><a href="ntrAllDet.html#Ntr_Trav">Ntr_Trav</a>
 165 </code>
 166
 167 <dt><pre>
 168 int <i></i>
 169 <a name="Ntr_ShortestPaths"><b>Ntr_ShortestPaths</b></a>(
 170   DdManager * <b>dd</b>, <i></i>
 171   BnetNetwork * <b>net</b>, <i></i>
 172   NtrOptions * <b>option</b> <i></i>
 173 )
 174 </pre>
 175 <dd> Computes shortest paths in the state transition graph of a network. Three methods are availabe: <ul> <li> Bellman-Ford algorithm for single-source shortest paths; the algorithm computes the distance (number of transitions) from the initial states to all states. <li> Floyd-Warshall algorithm for all-pair shortest paths. <li> Repeated squaring algorithm for all-pair shortest paths. </ul> The function returns 1 in case of success; 0 otherwise.
 176 <p>
 177
 178 <dd> <b>Side Effects</b> ADD variables are created in the manager.
 179 <p>
 180
 181 <dt><pre>
 182 int <i></i>
 183 <a name="Ntr_TestClipping"><b>Ntr_TestClipping</b></a>(
 184   DdManager * <b>dd</b>, <i></i>
 185   BnetNetwork * <b>net1</b>, <i></i>
 186   BnetNetwork * <b>net2</b>, <i></i>
 187   NtrOptions * <b>option</b> <i></i>
 188 )
 189 </pre>
 190 <dd> Tests BDD clipping functions. Returns 1 if successful; 0 otherwise.
 191 <p>
 192
 193 <dd> <b>Side Effects</b> None
 194 <p>
 195
 196 <dt><pre>
 197 int <i></i>
 198 <a name="Ntr_TestClosestCube"><b>Ntr_TestClosestCube</b></a>(
 199   DdManager * <b>dd</b>, <i></i>
 200   BnetNetwork * <b>net</b>, <i></i>
 201   NtrOptions * <b>option</b> <i></i>
 202 )
 203 </pre>
 204 <dd> Tests the Cudd_bddClosestCube function. Returns 1 if successful; 0 otherwise.
 205 <p>
 206
 207 <dd> <b>Side Effects</b> None
 208 <p>
 209
 210 <dt><pre>
 211 int <i></i>
 212 <a name="Ntr_TestCofactorEstimate"><b>Ntr_TestCofactorEstimate</b></a>(
 213   DdManager * <b>dd</b>, <i></i>
 214   BnetNetwork * <b>net</b>, <i></i>
 215   NtrOptions * <b>option</b> <i></i>
 216 )
 217 </pre>
 218 <dd> Tests BDD cofactor estimate functions. Returns 1 if successful; 0 otherwise.
 219 <p>
 220
 221 <dd> <b>Side Effects</b> None
 222 <p>
 223
 224 <dt><pre>
 225 int <i></i>
 226 <a name="Ntr_TestDecomp"><b>Ntr_TestDecomp</b></a>(
 227   DdManager * <b>dd</b>, <i></i>
 228   BnetNetwork * <b>net1</b>, <i></i>
 229   NtrOptions * <b>option</b> <i></i>
 230 )
 231 </pre>
 232 <dd> Tests BDD decomposition functions. Returns 1 if successful; 0 otherwise.
 233 <p>
 234
 235 <dd> <b>Side Effects</b> None
 236 <p>
 237
 238 <dt><pre>
 239 int <i></i>
 240 <a name="Ntr_TestDensity"><b>Ntr_TestDensity</b></a>(
 241   DdManager * <b>dd</b>, <i></i>
 242   BnetNetwork * <b>net1</b>, <i></i>
 243   NtrOptions * <b>option</b> <i></i>
 244 )
 245 </pre>
 246 <dd> Tests BDD density-related functions. Returns 1 if successful; 0 otherwise.
 247 <p>
 248
 249 <dd> <b>Side Effects</b> None
 250 <p>
 251
 252 <dt><pre>
 253 int <i></i>
 254 <a name="Ntr_TestEquivAndContain"><b>Ntr_TestEquivAndContain</b></a>(
 255   DdManager * <b>dd</b>, <i></i>
 256   BnetNetwork * <b>net1</b>, <i></i>
 257   BnetNetwork * <b>net2</b>, <i></i>
 258   NtrOptions * <b>option</b> <i></i>
 259 )
 260 </pre>
 261 <dd> Tests functions for BDD equivalence and containment with don't cares, including Cudd_EquivDC and Cudd_bddLeqUnless. This function uses as care set the first output of net2 and checkes equivalence and containment for of all the output pairs of net1. Returns 1 if successful; 0 otherwise.
 262 <p>
 263
 264 <dd> <b>Side Effects</b> None
 265 <p>
 266
 267 <dt><pre>
 268 int <i></i>
 269 <a name="Ntr_TestHeap"><b>Ntr_TestHeap</b></a>(
 270   NtrHeap * <b>heap</b>, <i></i>
 271   int  <b>i</b> <i></i>
 272 )
 273 </pre>
 274 <dd> Tests the heap property of a priority queue. Returns 1 if Successful; 0 otherwise.
 275 <p>
 276
 277 <dd> <b>Side Effects</b> None
 278 <p>
 279
 280 <dt><pre>
 281 int <i></i>
 282 <a name="Ntr_TestMinimization"><b>Ntr_TestMinimization</b></a>(
 283   DdManager * <b>dd</b>, <i></i>
 284   BnetNetwork * <b>net1</b>, <i></i>
 285   BnetNetwork * <b>net2</b>, <i></i>
 286   NtrOptions * <b>option</b> <i></i>
 287 )
 288 </pre>
 289 <dd> Tests BDD minimization functions, including leaf-identifying compaction, squeezing, and restrict. This function uses as constraint the first output of net2 and computes positive and negative cofactors of all the outputs of net1. For each cofactor, it checks whether compaction was safe (cofactor not larger than original function) and that the expansion based on each minimization function (used as a generalized cofactor) equals the original function. Returns 1 if successful; 0 otherwise.
 290 <p>
 291
 292 <dd> <b>Side Effects</b> None
 293 <p>
 294
 295 <dt><pre>
 296 DdNode * <i></i>
 297 <a name="Ntr_TransitiveClosure"><b>Ntr_TransitiveClosure</b></a>(
 298   DdManager * <b>dd</b>, <i></i>
 299   NtrPartTR * <b>TR</b>, <i></i>
 300   NtrOptions * <b>option</b> <i></i>
 301 )
 302 </pre>
 303 <dd> Builds the transitive closure of a transition relation. Returns a BDD if successful; NULL otherwise. Uses a simple squaring algorithm.
 304 <p>
 305
 306 <dd> <b>Side Effects</b> None
 307 <p>
 308
 309 <dt><pre>
 310 int <i></i>
 311 <a name="Ntr_Trav"><b>Ntr_Trav</b></a>(
 312   DdManager * <b>dd</b>, <i>DD manager</i>
 313   BnetNetwork * <b>net</b>, <i>network</i>
 314   NtrOptions * <b>option</b> <i>options</i>
 315 )
 316 </pre>
 317 <dd> Poor man's traversal procedure. based on the monolithic transition relation. Returns 1 in case of success; 0 otherwise.
 318 <p>
 319
 320 <dd> <b>Side Effects</b> None
 321 <p>
 322
 323 <dd> <b>See Also</b> <code><a href="ntrAllDet.html#Ntr_ClosureTrav">Ntr_ClosureTrav</a>
 324 </code>
 325
 326 <dt><pre>
 327 int <i></i>
 328 <a name="Ntr_VerifyEquivalence"><b>Ntr_VerifyEquivalence</b></a>(
 329   DdManager * <b>dd</b>, <i></i>
 330   BnetNetwork * <b>net1</b>, <i></i>
 331   BnetNetwork * <b>net2</b>, <i></i>
 332   NtrOptions * <b>option</b> <i></i>
 333 )
 334 </pre>
 335 <dd> Verify equivalence of combinational networks. Returns 1 if successful and if the networks are equivalent; -1 if successful, but the networks are not equivalent; 0 otherwise. The two networks are supposed to have the same names for inputs and outputs. The only exception is that the second network may miss output buffers that are present in the first network. This function tries to match both the output and the input of the buffer.
 336 <p>
 337
 338 <dd> <b>Side Effects</b> None
 339 <p>
 340
 341 <dt><pre>
 342 int <i></i>
 343 <a name="Ntr_buildDDs"><b>Ntr_buildDDs</b></a>(
 344   BnetNetwork * <b>net</b>, <i>network for which DDs are to be built</i>
 345   DdManager * <b>dd</b>, <i>DD manager</i>
 346   NtrOptions * <b>option</b>, <i>option structure</i>
 347   BnetNetwork * <b>net2</b> <i>companion network with which inputs may be shared</i>
 348 )
 349 </pre>
 350 <dd> Builds DDs for a network outputs and next state functions. The method is really brain-dead, but it is very simple. Returns 1 in case of success; 0 otherwise. Some inputs to the network may be shared with another network whose DDs have already been built. In this case we want to share the DDs as well.
 351 <p>
 352
 353 <dd> <b>Side Effects</b> the dd fields of the network nodes are modified. Uses the count fields of the nodes.
 354 <p>
 355
 356 <dt><pre>
 357 NtrPartTR * <i></i>
 358 <a name="Ntr_buildTR"><b>Ntr_buildTR</b></a>(
 359   DdManager * <b>dd</b>, <i>manager</i>
 360   BnetNetwork * <b>net</b>, <i>network</i>
 361   NtrOptions * <b>option</b>, <i>options</i>
 362   int  <b>image</b> <i>image type: monolithic ...</i>
 363 )
 364 </pre>
 365 <dd> Builds the transition relation for a network. Returns a pointer to the transition relation structure if successful; NULL otherwise.
 366 <p>
 367
 368 <dd> <b>Side Effects</b> None
 369 <p>
 370
 371 <dt><pre>
 372 NtrPartTR * <i></i>
 373 <a name="Ntr_cloneTR"><b>Ntr_cloneTR</b></a>(
 374   NtrPartTR * <b>TR</b> <i></i>
 375 )
 376 </pre>
 377 <dd> Makes a copy of a transition relation. Returns a pointer to the copy if successful; NULL otherwise.
 378 <p>
 379
 380 <dd> <b>Side Effects</b> None
 381 <p>
 382
 383 <dd> <b>See Also</b> <code><a href="ntrAllDet.html#Ntr_buildTR">Ntr_buildTR</a>
 384 <a href="ntrAllDet.html#Ntr_freeTR">Ntr_freeTR</a>
 385 </code>
 386
 387 <dt><pre>
 388 void <i></i>
 389 <a name="Ntr_freeTR"><b>Ntr_freeTR</b></a>(
 390   DdManager * <b>dd</b>, <i></i>
 391   NtrPartTR * <b>TR</b> <i></i>
 392 )
 393 </pre>
 394 <dd> Frees the transition relation for a network.
 395 <p>
 396
 397 <dd> <b>Side Effects</b> None
 398 <p>
 399
 400 <dt><pre>
 401 DdNode * <i></i>
 402 <a name="Ntr_getStateCube"><b>Ntr_getStateCube</b></a>(
 403   DdManager * <b>dd</b>, <i></i>
 404   BnetNetwork * <b>net</b>, <i></i>
 405   char * <b>filename</b>, <i></i>
 406   int  <b>pr</b> <i></i>
 407 )
 408 </pre>
 409 <dd> Reads a state cube from a file or create a random one. Returns a pointer to the BDD of the sink nodes if successful; NULL otherwise.
 410 <p>
 411
 412 <dd> <b>Side Effects</b> None
 413 <p>
 414
 415 <dt><pre>
 416 DdNode * <i></i>
 417 <a name="Ntr_initState"><b>Ntr_initState</b></a>(
 418   DdManager * <b>dd</b>, <i></i>
 419   BnetNetwork * <b>net</b>, <i></i>
 420   NtrOptions * <b>option</b> <i></i>
 421 )
 422 </pre>
 423 <dd> Builds the BDD of the initial state(s). Returns a BDD if successful; NULL otherwise.
 424 <p>
 425
 426 <dd> <b>Side Effects</b> None
 427 <p>
 428
 429 <dt><pre>
 430 int <i></i>
 431 <a name="Ntr_maxflow"><b>Ntr_maxflow</b></a>(
 432   DdManager * <b>dd</b>, <i></i>
 433   BnetNetwork * <b>net</b>, <i></i>
 434   NtrOptions * <b>option</b> <i></i>
 435 )
 436 </pre>
 437 <dd> Maximum 0-1 flow between source and sink states. Returns 1 in case of success; 0 otherwise.
 438 <p>
 439
 440 <dd> <b>Side Effects</b> Creates two new sets of variables.
 441 <p>
 442
 443 <dt><pre>
 444 double <i></i>
 445 <a name="Ntr_maximum01Flow"><b>Ntr_maximum01Flow</b></a>(
 446   DdManager * <b>bdd</b>, <i>manager</i>
 447   DdNode * <b>sx</b>, <i>source node</i>
 448   DdNode * <b>ty</b>, <i>sink node</i>
 449   DdNode * <b>E</b>, <i>edge relation</i>
 450   DdNode ** <b>F</b>, <i>flow relation</i>
 451   DdNode ** <b>cut</b>, <i>cutset relation</i>
 452   DdNode ** <b>x</b>, <i>array of row variables</i>
 453   DdNode ** <b>y</b>, <i>array of column variables</i>
 454   DdNode ** <b>z</b>, <i>arrays of auxiliary variables</i>
 455   int  <b>n</b>, <i>number of variables in each array</i>
 456   int  <b>pr</b> <i>verbosity level</i>
 457 )
 458 </pre>
 459 <dd> This function implements Dinits's algorithm for (0-1) max flow, using BDDs and a symbolic technique to trace multiple edge-disjoint augmenting paths to complete a phase. The outer forever loop is over phases, and the inner forever loop is to propagate a (not yet) maximal flow of edge-disjoint augmenting paths from one layer to the previous. The subprocedure call implements a least fixed point iteration to compute a (not yet) maximal flow update between layers. At the end of each phase (except the last one) the flow is actually pushed from the source to the sink. Data items: <ul> <li> sx(ty) BDD representations of s(t). <li> x(y) The variables encoding the from(to)-node u(v) of an edge (u,v) in the given digraph. <li> z Another set of variables. <li> E(x,y) The edge relation. <li> F(x,y) BDD representation of the current flow, initialized to 0 for each arc, and updated by +1, -1, or 0 at the end of each phase. <li> Ms Mt The maximum flow, that is, the cardinality of a minimum cut, measured at the source and at the sink, respectively. The two values should be identical. <li> reached The set of nodes already visited in the BFS of the digraph. <li> fos fanout of the source node s. <li> fit fanin of the sink node t. </ul>
 460 <p>
 461
 462 <dd> <b>Side Effects</b> The flow realtion F and the cutset relation cut are returned as side effects.
 463 <p>
 464
 465 <dt><pre>
 466 int <i></i>
 467 <a name="Ntr_testISOP"><b>Ntr_testISOP</b></a>(
 468   DdManager * <b>dd</b>, <i></i>
 469   BnetNetwork * <b>net</b>, <i></i>
 470   NtrOptions * <b>option</b> <i></i>
 471 )
 472 </pre>
 473 <dd> Builds ZDD covers.
 474 <p>
 475
 476 <dd> <b>Side Effects</b> Creates ZDD variables in the manager.
 477 <p>
 478
 479 <dt><pre>
 480 int <i></i>
 481 <a name="Ntr_testZDD"><b>Ntr_testZDD</b></a>(
 482   DdManager * <b>dd</b>, <i></i>
 483   BnetNetwork * <b>net</b>, <i></i>
 484   NtrOptions * <b>option</b> <i></i>
 485 )
 486 </pre>
 487 <dd> Tests ZDDs. Returns 1 if successful; 0 otherwise.
 488 <p>
 489
 490 <dd> <b>Side Effects</b> Creates ZDD variables in the manager.
 491 <p>
 492
 493
 494 </dl>
 495
 496 <hr>
 497
 498 Generated automatically by <code>extdoc</code> on 1010215
 499
 500 </body></html>