source: vis_dev/vis-2.3/src/fsm/fsmHD.c @ 56

Last change on this file since 56 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 69.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [fsmHD.c]
4
5  PackageName [fsm]
6
7  Synopsis [Routines to perform high density reachability on the FSM
8  structure.]
9
10  Description [Routines to perform high density reachability on the
11  FSM structure. The main quantities in HD reachability analysis are:
12  MDDs:
13  0. initial states: initial states of the machine.
14  1. reachableStates
15  2. fromLowerBound : lower bound of states fed to
16  the next image computation.]
17  3. fromUpperBound: In HD, this is set to the fromLowerBound.
18  4. image: image computed in each iteration.
19  5. interiorStates: set of states that have no new successors.
20  6. deadEndResidue: We refer to residue as those states which have
21  been discarded for image computation in computing an approximation
22  of the frontier set. deadEndResidue is the residue right after a
23  dead-end. It is also the residue of the first approximation
24  performed in the traversal.
25   
26  FLAGS and COUNTS:
27  0. deadEndComputation: Indicates that this is a dead-end.
28  1. residueCount: number of times residues have been returned from a
29  dead-end. After 4 times it is freed.
30  2. fromOrDeadEnd: Indicates which type of approximation is
31  permissible. If from, then the specified method is used, if dead-end
32  remap_ua is always used. Default is remap_ua.
33  3. fronierApproxThreshold: Size of approximation of the frontier set.
34  4. nvars: Number of present state variables.
35  5. failedPartition: decomposition of reached in dead-ends failed.
36  6. reachedSize: size of reachableStates
37  7. greedy: whether dead-end computation is greedy (stop when new states
38  are found. ) or not (compute the image of the entire reached set).
39  8. firstSubset: whether the first approximation has been performed
40  or not.
41
42  Other structures:
43  0. imageInfo: required for transition relation.
44  1. varArray: present state var array.
45  2. options: HD options.
46  3. stats: holds information about minterms and size of the various
47  mdds involved.
48 
49 
50  These quantities are modified as necessary at each step of the HD
51  manipulation. The same names are used throughout this file.]
52 
53  Author      [Kavita Ravi]
54
55  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
56  All rights reserved.
57
58  Permission is hereby granted, without written agreement and without license
59  or royalty fees, to use, copy, modify, and distribute this software and its
60  documentation for any purpose, provided that the above copyright notice and
61  the following two paragraphs appear in all copies of this software.
62
63  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
64  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
65  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
66  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
67
68  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
69  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
70  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
71  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
72  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
73
74******************************************************************************/
75
76#include "fsmInt.h"
77#include "bdd.h"
78#include "ntm.h"
79#include "img.h"
80
81static char rcsid[] UNUSED = "$Id: fsmHD.c,v 1.32 2005/05/16 06:23:29 fabio Exp $";
82
83/*---------------------------------------------------------------------------*/
84/* Constant declarations                                                     */
85/*---------------------------------------------------------------------------*/
86/* thresholds for computation */
87#define FSM_HD_DEADEND_RESIDUE_LIMIT 5000/*size beyond which residue is freed*/
88#define FSM_HD_FRONTIER_APPROX_THRESHOLD 3500 /* default frontier approximation
89                                                 threshold */
90#define FSM_HD_REACHED_THRESHOLD  2000   /* Threshold below which reached is
91                                         not decomposed */ 
92#define FSM_HD_DISJ_SIZE 5000            /* default Size of disjunct whose image
93                            may be computed in dead end computation. */
94#define FSM_HD_DEADEND_MAX_SIZE_FACTOR 5 /* Factor such that when multiplied with
95        the approx threshold will allow partitioning of the reached disjunct. */
96#define FSM_HD_FROM 0 /* Constant to indicate to subsetting method whether to use
97                       * specified method or remap_ua */
98#define FSM_HD_DEADEND 1 /* Constant to indicate to subsetting method whether to use
99                       * specified method or remap_ua */
100#define FSM_HD_MIN_SIZE_FROM 700 /* threshold to indicate not to subset if under this size */
101#define FSM_HD_DONT_FREE 0 /* flag to indicate that mdds should not be freed */
102#define FSM_HD_FREE 1 /* flag to indicate that mdds should be freed */
103#define FSM_HD_SP_THRESHOLD 2000 /* Threshold for short_paths method */
104
105/*---------------------------------------------------------------------------*/
106/* Type declarations                                                         */
107/*---------------------------------------------------------------------------*/
108typedef struct FsmHdSizeStruct FsmHdSizeStruct_t;
109
110/*---------------------------------------------------------------------------*/
111/* Structure declarations                                                    */
112/*---------------------------------------------------------------------------*/
113
114
115/**Struct**********************************************************************
116  Synopsis [Stats structure to store size and minterm count]
117 
118******************************************************************************/
119struct FsmHdSizeStruct {
120  mdd_t *bdd;
121  int size;
122  long rnd;
123};
124                 
125
126/**AutomaticStart*************************************************************/
127
128/*---------------------------------------------------------------------------*/
129/* Static function prototypes                                                */
130/*---------------------------------------------------------------------------*/
131
132static mdd_t * ComputeNewSeedsAtDeadEnd(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t *reachableStates, FsmHdStruct_t *hdInfo, int greedy, int verbosity);
133static mdd_t * ComputeImageOfDecomposedParts(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t *reachedSet, mdd_t *reachableStates, FsmHdStruct_t *hdInfo, int frontierApproxThreshold, int nvars, int *failedPartition, int greedy, int verbosity);
134static mdd_t * ProcessDisjunctsRecursive(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t **reachedSet, mdd_t *reachableStates, FsmHdStruct_t *hdInfo, int frontierApproxThreshold, int nvars, int *failedPartition, int reachedSize, int greedy, int verbosity);
135static mdd_t * ComputeSubsetBasedOnMethod(mdd_t *fromBetween, mdd_t *fromLowerBound, FsmHdTravOptions_t *options, int fromOrDeadEnd);
136static mdd_t * AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB);
137static mdd_t * SubtractStates(mdd_t *a, mdd_t *b, int freeA, int freeB);
138static int RandomCompare(const void *ptrX, const void *ptrY);
139
140/**AutomaticEnd***************************************************************/
141
142
143/*---------------------------------------------------------------------------*/
144/* Definition of exported functions                                          */
145/*---------------------------------------------------------------------------*/
146
147/**Function********************************************************************
148
149  Synopsis [Returns the options required for approximate traversal.]
150
151  Description [Return the options required for approximate traversal
152  in the options structure. Will return NULL if the number of
153  variables is less than zero. Only chance to set the
154  variables. nvars should be number of BDD state variables in the
155  FSM. Caller frees this structure. This procedure sets default values
156  and overwrites with user-specified values by reading the specific
157  set variables associated with the options.]
158
159  SideEffects []
160
161  SeeAlso [Fsm_FsmHdStatsStructFree]
162 
163******************************************************************************/
164FsmHdTravOptions_t *
165Fsm_FsmHdGetTravOptions(int nvars)
166{
167  char *frontierApproxMethodString, *frontierApproxThresholdString;
168  char *scrapStatesString;
169  char *deadEndString, *qualityString;
170  char *newOnlyString, *partialImageString, *deadEndSubsetMethodString;
171  FsmHdTravOptions_t *options;
172
173  if (nvars < 0) return NIL(FsmHdTravOptions_t);
174  options = ALLOC(FsmHdTravOptions_t, 1);
175  if (options == NIL(FsmHdTravOptions_t)) {
176    return NIL(FsmHdTravOptions_t);
177  }
178
179  options->nvars = nvars;
180  /* set defaults */
181  options->frontierApproxMethod = BDD_APPROX_RUA;
182  options->frontierApproxThreshold = FSM_HD_FRONTIER_APPROX_THRESHOLD;
183  options->quality = 1.0;
184  options->deadEnd = Fsm_Hd_DE_Con_c;
185  options->deadEndSubsetMethod = BDD_APPROX_RUA;
186  options->scrapStates = TRUE;
187  options->newOnly = FALSE;
188  options->onlyPartialImage = FALSE;
189  options->qualityBias = 0.5;
190 
191  /*  method for subsetting reached, from */
192  frontierApproxMethodString = Cmd_FlagReadByName("hd_frontier_approx_method");
193  if (frontierApproxMethodString != NIL(char)) {
194    if (strcmp(frontierApproxMethodString, "heavy_branch") == 0) {
195      options->frontierApproxMethod = BDD_APPROX_HB;
196    } else if (strcmp(frontierApproxMethodString, "short_paths") == 0) {
197      options->frontierApproxMethod = BDD_APPROX_SP;
198    } else if (strcmp(frontierApproxMethodString, "under_approx") == 0) {
199      options->frontierApproxMethod = BDD_APPROX_UA;
200    } else if (strcmp(frontierApproxMethodString, "remap_ua") == 0) {
201      options->frontierApproxMethod = BDD_APPROX_RUA;
202    } else if (strcmp(frontierApproxMethodString, "compress") == 0) {
203      options->frontierApproxMethod = BDD_APPROX_COMP;
204    } else if (strcmp(frontierApproxMethodString, "biased_rua") == 0) {
205      options->frontierApproxMethod = BDD_APPROX_BIASED_RUA;
206    }
207  }
208
209  /* threshold value */
210  frontierApproxThresholdString = Cmd_FlagReadByName("hd_frontier_approx_threshold");
211  if (frontierApproxThresholdString != NIL(char)) {
212    options->frontierApproxThreshold = strtol(frontierApproxThresholdString,
213                                           NULL, 10);
214  }
215  /* adjust threshold if too small */
216  if ((options->frontierApproxMethod == BDD_APPROX_HB) ||
217      (options->frontierApproxMethod == BDD_APPROX_SP) ||
218      (options->frontierApproxMethod == BDD_APPROX_COMP)) {
219    if (options->frontierApproxThreshold < FSM_HD_SP_THRESHOLD) {
220      fprintf(vis_stdout, "** hd warning: Threshold too low, Correcting Frontier Approx Threshold to %d\n", FSM_HD_SP_THRESHOLD);
221      options->frontierApproxThreshold =  FSM_HD_SP_THRESHOLD;
222    }
223  } else if (options->frontierApproxThreshold < 0) {
224    fprintf(vis_stdout, "** hd warning: Threshold negative, Correcting Frontier Approx Threshold to 0\n");
225    options->frontierApproxThreshold = FSM_HD_FRONTIER_APPROX_THRESHOLD;
226  }
227
228
229  /* quality option for remap_ua */
230  qualityString = Cmd_FlagReadByName("hd_approx_quality");
231  if (qualityString != NIL(char)) {
232    options->quality = strtod(qualityString, NULL);
233    if (options->quality < 0.0) {
234      options->quality = 1.0;
235    }
236  }
237
238  /* quality option for biased_rua */
239  qualityString = Cmd_FlagReadByName("hd_approx_bias_quality");
240  if (qualityString != NIL(char)) {
241    options->qualityBias = strtod(qualityString, NULL);
242    if (options->qualityBias < 0.0) {
243      options->qualityBias = 0.5;
244    }
245  }
246
247  /* method for dead end computations */
248  deadEndString = Cmd_FlagReadByName("hd_dead_end");
249  if (deadEndString != NIL(char)) {
250    if (strcmp(deadEndString, "brute_force") == 0) {
251      options->deadEnd = Fsm_Hd_DE_BF_c;
252    } else if (strcmp(deadEndString, "conjuncts") == 0) {
253      options->deadEnd = Fsm_Hd_DE_Con_c;
254    } else if (strcmp(deadEndString, "hybrid") == 0) {
255      options->deadEnd = Fsm_Hd_DE_Hyb_c;
256    }
257  }
258  /*  method for subsetting reached, from during deadEnds*/
259  deadEndSubsetMethodString = Cmd_FlagReadByName("hd_dead_end_approx_method");
260  if (deadEndSubsetMethodString != NIL(char)) {
261    if (strcmp(deadEndSubsetMethodString, "heavy_branch") == 0) {
262      options->deadEndSubsetMethod = BDD_APPROX_HB;
263    } else if (strcmp(deadEndSubsetMethodString, "short_paths") == 0) {
264      options->deadEndSubsetMethod = BDD_APPROX_SP;
265    } else if (strcmp(deadEndSubsetMethodString, "under_approx") == 0) {
266      options->deadEndSubsetMethod = BDD_APPROX_UA;
267    } else if (strcmp(deadEndSubsetMethodString, "remap_ua") == 0) {
268      options->deadEndSubsetMethod = BDD_APPROX_RUA;
269    } else if (strcmp(deadEndSubsetMethodString, "compress") == 0) {
270      options->deadEndSubsetMethod = BDD_APPROX_COMP;
271    }
272  }
273  /* option to not add blocking states */
274  scrapStatesString = Cmd_FlagReadByName("hd_no_scrap_states");
275  if (scrapStatesString != NIL(char)) {
276    options->scrapStates = FALSE;
277  }
278
279  /* option to consider only new states instead of fromBetween */
280  newOnlyString = Cmd_FlagReadByName("hd_new_only");
281  if (newOnlyString != NIL(char)) {
282    options->newOnly = TRUE;
283  }
284   
285  /* perform approximate traversal with only partial images */
286  partialImageString = Cmd_FlagReadByName("hd_only_partial_image");
287  if (partialImageString != NIL(char)) {
288    options->onlyPartialImage = TRUE;
289  }
290
291  return (options);
292} /* end of Fsm_FsmHdGetTraversalOptions */
293
294/**Function********************************************************************
295
296  Synopsis    [Free options structure.]
297
298  Description [Free options structure.]
299
300  SideEffects []
301
302  SeeAlso [Fsm_FsmHdGetTraversalOptions]
303 
304******************************************************************************/
305void
306Fsm_FsmHdFreeTravOptions(FsmHdTravOptions_t *options)
307{
308  if (options) FREE(options);
309  return;
310} /* end of Fsm_FsmHdFreeTravOptions */
311
312/**Function**********************************************************************
313
314  Synopsis [Read high density threshold from HD Approximate Traversal
315  option structure]
316 
317  Description [Read high density threshold from HD Approximate
318  Traversal option structure]
319 
320  SideEffects []
321
322  SeeAlso []
323 
324******************************************************************************/
325int
326Fsm_FsmHdOptionReadNumVars(FsmHdTravOptions_t *options)
327{
328  if (options) return(options->nvars);
329  else return 0;
330}
331
332/**Function**********************************************************************
333
334  Synopsis [Read high density threshold from HD Approximate Traversal
335  option structure]
336
337  Description [Read high density threshold from HD Approximate Traversal
338  option structure]
339
340  SideEffects []
341
342  SeeAlso []
343
344******************************************************************************/
345int 
346Fsm_FsmHdOptionReadFrontierApproxThreshold(FsmHdTravOptions_t *options)
347{
348  if (options) return (options->frontierApproxThreshold);
349  else return 0;
350}
351
352/**Function**********************************************************************
353
354  Synopsis [Read only partial image option from HD Approximate
355  Traversal option structure]
356
357  Description [Read only partial image option from HD Approximate
358  Traversal option structure]
359
360  SideEffects []
361
362  SeeAlso []
363 
364******************************************************************************/
365boolean
366Fsm_FsmHdOptionReadOnlyPartialImage(FsmHdTravOptions_t *options)
367{
368  if (options) return (options->onlyPartialImage);
369  else return FALSE;
370}
371
372/**Function**********************************************************************
373
374  Synopsis [Read blocking states option from HD Approximate
375  Traversal option structure]
376
377  Description [Read blocking states option from HD Approximate
378  Traversal option structure]
379
380  SideEffects []
381
382  SeeAlso []
383 
384******************************************************************************/
385boolean
386Fsm_FsmHdOptionReadScrapStates(FsmHdTravOptions_t *options)
387{
388  if (options) return (options->scrapStates);
389  else return TRUE;
390}
391
392/**Function**********************************************************************
393
394  Synopsis [Read quality factor from HD Approximate Traversal option
395  structure]
396
397  Description [Read quality factor from HD Approximate Traversal option
398  structure]
399
400  SideEffects []
401
402  SeeAlso []
403 
404******************************************************************************/
405double
406Fsm_FsmHdOptionReadQuality(FsmHdTravOptions_t *options)
407{
408  if (options) return(options->quality);
409  else return 1.0;
410}
411
412/**Function**********************************************************************
413
414  Synopsis [Read High Density Method from HD Approximate Traversal
415  option structure]
416
417  Description [Read High Density Method from HD Approximate Traversal
418  option structure]
419
420  SideEffects []
421
422  SeeAlso []
423 
424******************************************************************************/
425bdd_approx_type_t
426Fsm_FsmHdOptionReadFrontierApproxMethod(FsmHdTravOptions_t *options)
427{
428  if (options) return(options->frontierApproxMethod);
429  else return BDD_APPROX_RUA;
430}
431
432/**Function**********************************************************************
433
434  Synopsis [Read dead-end from HD Approximate Traversal option
435  structure]
436
437  Description [Read dead-end from HD Approximate Traversal option
438  structure]
439
440  SideEffects []
441
442  SeeAlso []
443 
444******************************************************************************/
445Fsm_HdDeadEndType_t
446Fsm_FsmHdOptionReadDeadEnd(FsmHdTravOptions_t *options)
447{
448  if (options) return(options->deadEnd);
449  else return Fsm_Hd_DE_Con_c;
450}
451
452/**Function**********************************************************************
453
454  Synopsis [Read new only option from HD Approximate Traversal option
455  structure]
456
457  Description [Read new only option from HD Approximate Traversal option
458  structure]
459
460  SideEffects []
461
462  SeeAlso []
463 
464******************************************************************************/
465boolean
466Fsm_FsmHdOptionReadNewOnly(FsmHdTravOptions_t *options)
467{
468  if (options) return(options->newOnly);
469  else return FALSE;
470}
471
472/**Function**********************************************************************
473
474  Synopsis [Read dead-end subset method from HD Approximate Traversal
475  option structure]
476
477  Description [Read dead-end subset method from HD Approximate Traversal
478  option structure]
479
480  SideEffects []
481
482  SeeAlso []
483 
484******************************************************************************/
485bdd_approx_type_t
486Fsm_FsmHdOptionReadDeadEndSubsetMethod(FsmHdTravOptions_t *options)
487{
488  if (options) return(options->deadEndSubsetMethod);
489  else return BDD_APPROX_RUA;
490}
491
492/**Function**********************************************************************
493
494  Synopsis [Set high density threshold from HD Approximate Traversal
495  option structure]
496
497  Description [Set high density threshold from HD Approximate
498  Traversal option structure. Returns 0 if threshold less than number
499  of state variables in the FSM, corrects the value to number of
500  variables. Else 1.]
501
502  SideEffects []
503
504  SeeAlso []
505
506******************************************************************************/
507int 
508Fsm_FsmHdOptionSetFrontierApproxThreshold(FsmHdTravOptions_t *options,
509                                          int threshold)
510{
511  if ((options->frontierApproxMethod == BDD_APPROX_HB) ||
512      (options->frontierApproxMethod == BDD_APPROX_SP) ||
513      (options->frontierApproxMethod == BDD_APPROX_COMP)) {
514    if  (threshold < FSM_HD_SP_THRESHOLD) {
515      fprintf(vis_stdout, "** hd warning: Threshold too low, Correcting Frontier Approx Threshold to %d\n", FSM_HD_SP_THRESHOLD);
516      options->frontierApproxThreshold =  FSM_HD_SP_THRESHOLD;
517      return 0;
518    } else {
519      options->frontierApproxThreshold = threshold;
520      return 1;
521    }
522  } else if (threshold < 0) {
523    fprintf(vis_stdout, "** hd warning: Threshold negative, Correcting Frontier Approx Threshold to 0\n");
524    options->frontierApproxThreshold = FSM_HD_FRONTIER_APPROX_THRESHOLD;
525    return 0;
526  } else {
527    options->frontierApproxThreshold = threshold;
528    return 1;
529  }
530}
531
532/**Function**********************************************************************
533
534  Synopsis [Set only partial image option from HD Approximate
535  Traversal option structure]
536
537  Description [Set only partial image option from HD Approximate
538  Traversal option structure]
539
540  SideEffects []
541
542  SeeAlso []
543 
544******************************************************************************/
545void
546Fsm_FsmHdOptionSetOnlyPartialImage(FsmHdTravOptions_t *options,
547                                   boolean onlyPartial)
548{
549  if (options) options->onlyPartialImage = onlyPartial;
550  return;
551}
552
553/**Function**********************************************************************
554
555  Synopsis [Set blocking states option from HD Approximate
556  Traversal option structure]
557
558  Description [Set blocking states option from HD Approximate
559  Traversal option structure]
560
561  SideEffects []
562
563  SeeAlso []
564 
565******************************************************************************/
566void
567Fsm_FsmHdOptionSetScrapStates(FsmHdTravOptions_t *options, boolean scrapStates)
568{
569  if (options) options->scrapStates = scrapStates;
570  return;
571}
572
573/**Function**********************************************************************
574
575  Synopsis [Set quality factor from HD Approximate Traversal option
576  structure]
577
578  Description [Set quality factor from HD Approximate Traversal option
579  structure. Range of quality is positive doubles. Default value is
580  1.0. ]
581
582  SideEffects []
583
584  SeeAlso []
585 
586******************************************************************************/
587void
588Fsm_FsmHdOptionSetQuality(FsmHdTravOptions_t *options, double quality)
589{
590  if (quality > 0.0) 
591    if (options) options->quality = quality;
592  return;
593}
594
595/**Function**********************************************************************
596
597  Synopsis [Set High Density Method from HD Approximate Traversal
598  option structure]
599
600  Description [Set High Density Method from HD Approximate Traversal
601  option structure]
602
603  SideEffects []
604
605  SeeAlso []
606 
607******************************************************************************/
608void
609Fsm_FsmHdOptionSetFrontierApproxMethod(FsmHdTravOptions_t *options,
610                                       bdd_approx_type_t approxMethod)
611{
612  if (options) options->frontierApproxMethod = approxMethod;
613  if ((options->frontierApproxMethod == BDD_APPROX_HB) ||
614      (options->frontierApproxMethod == BDD_APPROX_SP) ||
615      (options->frontierApproxMethod == BDD_APPROX_COMP)) {
616    if  (options->frontierApproxThreshold < FSM_HD_SP_THRESHOLD) {
617      fprintf(vis_stdout, "** hd warning: Threshold too low, Correcting Frontier Approx Threshold to %d\n", FSM_HD_SP_THRESHOLD);
618      options->frontierApproxThreshold =  FSM_HD_SP_THRESHOLD;
619      return;
620    }
621  } else if (options->frontierApproxThreshold < 0) {
622    fprintf(vis_stdout, "** hd warning: Threshold negative, Correcting Frontier Approx Threshold to 0\n");
623    options->frontierApproxThreshold = FSM_HD_FRONTIER_APPROX_THRESHOLD;
624    return;
625  }
626
627  return;
628}
629
630/**Function**********************************************************************
631
632  Synopsis [Set dead-end from HD Approximate Traversal option
633  structure]
634
635  Description [Set dead-end from HD Approximate Traversal option
636  structure]
637
638  SideEffects []
639
640  SeeAlso []
641 
642******************************************************************************/
643void
644Fsm_FsmHdOptionSetDeadEnd(FsmHdTravOptions_t *options,
645                          Fsm_HdDeadEndType_t deadEnd)
646{
647  if (options) options->deadEnd = deadEnd;
648  return;
649}
650
651/**Function**********************************************************************
652
653  Synopsis [Set new only option from HD Approximate Traversal option
654  structure]
655
656  Description [Set new only option from HD Approximate Traversal option
657  structure]
658
659  SideEffects []
660
661  SeeAlso []
662 
663******************************************************************************/
664void
665Fsm_FsmHdOptionSetNewOnly(FsmHdTravOptions_t *options, boolean newOnly)
666{
667  if (options) options->newOnly = newOnly;
668  return;
669}
670
671/**Function**********************************************************************
672
673  Synopsis [Set dead-end subset method from HD Approximate Traversal
674  option structure]
675
676  Description [Set dead-end subset method from HD Approximate Traversal
677  option structure]
678
679  SideEffects []
680
681  SeeAlso []
682 
683******************************************************************************/
684void
685Fsm_FsmHdOptionSetDeadEndSubsetMethod(FsmHdTravOptions_t *options,
686                                      bdd_approx_type_t approxMethod)
687{
688  if (options) options->deadEndSubsetMethod = approxMethod;
689  return;
690}
691
692
693/*---------------------------------------------------------------------------*/
694/* Definition of internal functions                                          */
695/*---------------------------------------------------------------------------*/
696
697/**Function********************************************************************
698
699  Synopsis    [Allocate stats structure.]
700
701  Description [Allocate stats structure. Caller frees stats structure]
702
703  SideEffects []
704
705  SeeAlso [FsmHdStatsStructFree FsmHdStatsComputeSizeAndMinterms FsmHdStatsReset]
706 
707******************************************************************************/
708FsmHdMintSizeStats_t *
709FsmHdStatsStructAlloc(void)
710{
711  FsmHdMintSizeStats_t *stats;
712
713  stats = ALLOC(FsmHdMintSizeStats_t, 1);
714  if (stats == NULL) return NULL;
715
716  stats->sizeTo = 0;
717  stats->mintermTo = 0.0;
718  stats->sizeFrom = 0;
719  stats->mintermFrom = 0.0;
720  stats->sizeFromSubset = 0;
721  stats->mintermFromSubset = 0.0;
722  stats->sizeReached = 0;
723  stats->mintermReached = 0.0;
724 
725  return stats;
726} /* end of FsmHdStatsStructAlloc */
727
728
729/**Function********************************************************************
730
731  Synopsis    [Free stats structure.]
732
733  Description [Free stats structure.]
734
735  SideEffects []
736
737  SeeAlso [FsmHdStatsStructAlloc FsmHdStatsComputeSizeAndMinterms FsmHdStatsReset]
738 
739******************************************************************************/
740void
741FsmHdStatsStructFree(FsmHdMintSizeStats_t *stats)
742{
743  FREE(stats);
744  return;
745} /* end of FsmHdStatsStructFree */
746
747
748
749/**Function********************************************************************
750
751  Synopsis    [Compute size and minterms of a bdd]
752
753  Description [Compute size and minterms of a bdd]
754
755  SideEffects []
756
757  SeeAlso [FsmHdStatsStructFree FsmHdStatsStructFree FsmHdStatsReset]
758 
759******************************************************************************/
760void
761FsmHdStatsComputeSizeAndMinterms(mdd_manager *mddManager,
762                       mdd_t *f,
763                       array_t *varArray,
764                       int nvars,
765                       Fsm_Hd_Quant_t field,
766                       FsmHdMintSizeStats_t *stats)
767{
768  int size;
769  double minterms = 0.0;
770 
771  size = mdd_size(f);
772  if (nvars <= 1023)
773    minterms = mdd_count_onset(mddManager, f, varArray);
774 
775  switch (field) {
776  case Fsm_Hd_From: {
777    stats->sizeFrom = size;
778    stats->mintermFrom = minterms; 
779    break;
780  }
781  case Fsm_Hd_To: {
782    stats->sizeTo = size;
783    stats->mintermTo = minterms;
784    break;
785  }
786  case Fsm_Hd_FromSubset: {
787    stats->sizeFromSubset = size;
788    stats->mintermFromSubset = minterms;
789    break;
790  }
791  case Fsm_Hd_Reached: {
792    stats->sizeReached = size;
793    stats->mintermReached = minterms;
794    break;
795  }
796  default: break;
797  }
798  return;
799} /* end of FsmHdStatsComputeSizeAndMinterms */
800
801/**Function********************************************************************
802
803  Synopsis    [Resets stats structure.]
804
805  Description [Resets stats structure.]
806
807  SideEffects [FsmHdStatsStructAlloc FsmHdStatsComputeSizeAndMinterms
808  FsmHdStatsReset]
809
810******************************************************************************/
811void
812FsmHdStatsReset(FsmHdMintSizeStats_t *stats,
813                Fsm_Hd_Quant_t field)
814{
815
816  switch (field) {
817  case Fsm_Hd_To:
818    stats->sizeTo = 0;
819    stats->mintermTo = 0.0;
820    break;
821  case Fsm_Hd_From:
822    stats->sizeFrom = 0;
823    stats->mintermFrom = 0.0;
824    break;
825  case Fsm_Hd_FromSubset:
826    stats->sizeFromSubset = 0;
827    stats->mintermFromSubset = 0.0;
828    break;
829  case Fsm_Hd_Reached:
830    stats->sizeReached = 0;
831    stats->mintermReached = 0.0;
832    break;
833  }
834  return;
835} /* end of FsmHdStatsReset */
836
837
838/**Function********************************************************************
839
840  Synopsis    [Print HD options.]
841
842  Description [Print HD options.]
843
844  SideEffects [ ]
845
846  SeeAlso [FsmHdGetTraversalOptions]
847 
848******************************************************************************/
849void
850FsmHdPrintOptions(void)
851{
852  FsmHdTravOptions_t *options;
853  char *dummy;
854  options = Fsm_FsmHdGetTravOptions( 0);
855  if (options == NIL(FsmHdTravOptions_t)) {
856    fprintf(vis_stderr, "HD: Unalble to get options\n");
857    return;
858  }
859
860  dummy = ALLOC(char, 20);
861  if (dummy == NULL) return;
862  switch (options->frontierApproxMethod) {
863  case BDD_APPROX_HB: sprintf(dummy, "%s", "heavy_branch"); break;
864  case BDD_APPROX_SP: sprintf(dummy, "%s", "short_paths"); break;
865
866  case BDD_APPROX_UA: sprintf(dummy, "%s", "under_approx"); break;
867  case BDD_APPROX_RUA: sprintf(dummy, "%s", "remap_ua"); break;
868  case BDD_APPROX_BIASED_RUA: sprintf(dummy, "%s", "biased_rua"); break;
869
870  case BDD_APPROX_COMP: sprintf(dummy, "%s", "compress"); break;
871  default: sprintf(dummy, "%s", "remap_ua"); break;
872  }
873   
874  fprintf(vis_stdout, "HD: Approx method for frontier subsets = %s\n", dummy);
875  fprintf(vis_stdout, "HD: Threshold for frontier approximation = %d\n", options->frontierApproxThreshold);
876  fprintf(vis_stdout, "HD: Quality option for approx methods = %g\n", options->quality);
877  fprintf(vis_stdout, "HD: Bias quality option for the biased approx method = %g\n", options->qualityBias);
878
879  switch (options->deadEnd) {
880  case Fsm_Hd_DE_BF_c: sprintf(dummy, "%s", "brute_force"); break;
881  case Fsm_Hd_DE_Con_c: sprintf(dummy, "%s", "conjuncts"); break;
882  case Fsm_Hd_DE_Hyb_c: sprintf(dummy, "%s", "hybrid"); break;
883  }
884   
885  fprintf(vis_stdout, "HD: Dead-End method = %s\n", dummy);
886
887  switch (options->deadEndSubsetMethod) {
888  case BDD_APPROX_HB: sprintf(dummy, "%s", "heavy_branch"); break;
889  case BDD_APPROX_SP: sprintf(dummy, "%s", "short_paths"); break;
890
891  case BDD_APPROX_UA: sprintf(dummy, "%s", "under_approx"); break;
892  case BDD_APPROX_RUA: sprintf(dummy, "%s", "remap_ua"); break;
893
894  case BDD_APPROX_COMP: sprintf(dummy, "%s", "compress"); break;
895  default: sprintf(dummy, "%s", "remap_ua"); break;
896  }
897   
898  fprintf(vis_stdout, "HD: Dead-end approx method = %s\n", dummy);
899  FREE(dummy);
900 
901  fprintf(vis_stdout, "HD: Add scrap states option = ");
902  if (options->scrapStates == TRUE) fprintf(vis_stdout, "yes\n");
903  else fprintf(vis_stdout, "no\n");
904
905  fprintf(vis_stdout, "HD: Only new states in frontier option = ");
906  if (options->newOnly == TRUE) fprintf(vis_stdout, "yes\n");
907  else fprintf(vis_stdout, "no\n");
908
909  fprintf(vis_stdout, "HD: Only partial image option = ");
910  if (options->onlyPartialImage == TRUE) fprintf(vis_stdout, "yes\n");
911  else fprintf(vis_stdout, "no\n");
912
913  Fsm_FsmHdFreeTravOptions(options);
914  Img_ImagePrintPartialImageOptions();
915 
916  fprintf(vis_stdout, "See help page on print_hd_options for setting these options\n");
917  return;
918
919} /* end of FsmHdPrintOptions */
920
921/**Function********************************************************************
922
923  Synopsis [Checks if dead-end and computes new states from
924  Reached-InteriorStates.]
925
926  Description [Checks if dead-end and computes new states from
927  Reached-InteriorStates. If a residue exists, the residue states are returned,
928  else new states are returned.]
929
930  SideEffects [interior states are updated]
931
932  SeeAlso []
933
934******************************************************************************/
935mdd_t *
936FsmHdDeadEnd(mdd_manager *mddManager,
937             Img_ImageInfo_t *imageInfo,
938             mdd_t *reachableStates,
939             FsmHdStruct_t *hdInfo, 
940             array_t *varArray,
941             int greedy,
942             int verbosity)
943{
944  mdd_t *fromLowerBound;
945 
946  /* if residue is around to long, throw it away */
947  if (hdInfo->residueCount >= 4) {
948    if (hdInfo->deadEndResidue != NULL) {
949      mdd_free(hdInfo->deadEndResidue);
950      hdInfo->deadEndResidue = NULL;
951    }
952  }
953     
954  if ((hdInfo->deadEndResidue != NULL) && (greedy)) {
955    /* dont compute new seeds out of dead end
956     * if some states are left over from previous iterations.
957     */
958    fromLowerBound = hdInfo->deadEndResidue;
959    hdInfo->deadEndResidue = NULL;
960    assert(!mdd_is_tautology(fromLowerBound, 0));
961    if (hdInfo->interiorStates != NIL(mdd_t))
962      assert(mdd_lequal(fromLowerBound, hdInfo->interiorStates, 1, 0));
963    if (verbosity >= 2) fprintf(vis_stdout, "Residue had new seeds\n");
964    (hdInfo->residueCount)++;
965  } else {
966    /* compute new seeds by decomposing reachable states */
967    if (hdInfo->deadEndResidue != NULL) {
968      mdd_free(hdInfo->deadEndResidue);
969      hdInfo->deadEndResidue = NULL;
970    }
971    hdInfo->residueCount = 0;
972    fromLowerBound = ComputeNewSeedsAtDeadEnd(mddManager,
973                                              imageInfo,
974                                              reachableStates,
975                                              hdInfo,
976                                              greedy,
977                                              verbosity);
978
979  }
980           
981  /* mark that this is a dead end */
982  hdInfo->deadEndComputation = TRUE;
983
984  return (fromLowerBound);
985} /* end of FsmHdDeadEnd */
986
987/**Function********************************************************************
988
989  Synopsis    [Computes a dense subset of the frontier.]
990
991  Description [Computes a dense subset of the frontier. Assumption:
992  fromUpperBound has the old reached states, reachableStates has the
993  new reachable states if the entire set of new states were added,
994  fromLowerBound has the set of new states, interior states have
995  states all of whose successors have been computed, image is the
996  result of the previous image computation (which is not a
997  dead-end). image has to be set to NULL if already freed. Proceed as
998  follows: Swap image and reachable states if image is larger
999  (mintermwise) than reachable states. Then compute non-interior
1000  states: the only states we care about. Compute from such that it
1001  includes the dead-end residue. If new_only option is not specified,
1002  compute the set between the new states + dead-end residue and
1003  non-interior states. A subset of this set will be computed
1004  subsequently. The point is take to take as many states as possible
1005  from a set which will most likely yield new successors. The subset
1006  is computed only if the set of new states is large. The subset is
1007  kept only if it is dense enough. A flag is set to indicate a subset
1008  has been taken. The dead-end residue is computed if a dead-end
1009  preceded this. If blocking states are specified, Reached is adjusted
1010  to add only the subset. The dead-end residue is freed if too sparse
1011  and big. Set fromLowerBound, fromUpperBound, reachableStates, stats
1012  for the next iteration.]
1013
1014  SideEffects [ Set fromLowerBound, fromUpperBound, reachableStates,
1015  stats for the next iteration. Set firstSubset and
1016  deadEndResidue. Free interiorStates, image.]
1017
1018  SeeAlso []
1019 
1020******************************************************************************/
1021void
1022FsmHdFromComputeDenseSubset(mdd_manager *mddManager,
1023                            mdd_t **fromLowerBound,
1024                            mdd_t **fromUpperBound,
1025                            mdd_t **reachableStates,
1026                            mdd_t **image,
1027                            mdd_t *initialStates,
1028                            FsmHdStruct_t *hdInfo,
1029                            int shellFlag,
1030                            array_t *onionRings,
1031                            int sizeOfOnionRings,
1032                            array_t *varArray)
1033{
1034
1035  int thisTimeSubset;
1036  mdd_t *fromSubset, *fromBetween;
1037  mdd_t *temp, *temp1, *nonInteriorStates;
1038  float densityFrom = 0.0, densityFromSubset = 0.0; /* initialize to pacify */
1039  int numReorders;
1040  double mintResidue;
1041  int sizeResidue;
1042  int frontierApproxThreshold;
1043  int nvars;
1044 
1045  numReorders = bdd_read_reorderings(mddManager);
1046  frontierApproxThreshold = Fsm_FsmHdOptionReadFrontierApproxThreshold(hdInfo->options);
1047  nvars =  Fsm_FsmHdOptionReadNumVars(hdInfo->options);
1048
1049   /* if image is bigger and smaller in size, switch. Add initial states.
1050   * Reset dead states since they are no longer valid.
1051   */
1052
1053#if 0 /* taken out for counterexamples  */
1054  if ((FsmHdStatsReadMintermReached(hdInfo->stats) <
1055       FsmHdStatsReadMintermTo(hdInfo->stats)) &&
1056      (FsmHdStatsReadSizeReached(hdInfo->stats) > FsmHdStatsReadSizeTo(hdInfo->stats))) {
1057    if (hdInfo->interiorStates != NIL(mdd_t)) mdd_free(hdInfo->interiorStates);
1058    hdInfo->interiorStates = bdd_zero(mddManager);
1059    bdd_free(*reachableStates);
1060    mdd_free(*fromUpperBound);
1061    *reachableStates = mdd_or(initialStates, *image, 1, 1);
1062    *reachableStates = AddStates(*fromLowerBound, *reachableStates,
1063                                 FSM_HD_DONT_FREE, FSM_HD_FREE);
1064    FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates,
1065                             varArray, nvars, Fsm_Hd_Reached, hdInfo->stats);
1066    *fromUpperBound = mdd_dup(*reachableStates);
1067    if (shellFlag && *onionRings) {
1068      int onionRingCount;
1069      mdd_t *onionRing;
1070      fprintf(vis_stdout, "Onion Rings no longer valid. \n");
1071      arrayForEachItem(mdd_t *, *onionRings, onionRingCount, onionRing) {
1072        mdd_free(onionRing);
1073      }
1074      *onionRings = NIL(array_t);
1075    }
1076  }
1077#endif 
1078
1079  /* states which may produce new states as successors */
1080  nonInteriorStates = SubtractStates(*reachableStates, hdInfo->interiorStates,
1081                                     FSM_HD_DONT_FREE, FSM_HD_DONT_FREE);
1082
1083  /* try and reinject the residue from a dead end into the frontier */
1084  if (hdInfo->deadEndResidue != NULL) {
1085    temp = mdd_or(*fromLowerBound, hdInfo->deadEndResidue, 1, 1);
1086  } else {
1087    temp = mdd_dup(*fromLowerBound);
1088  }
1089  /* calculate the actual "from" going to be used */
1090  if ( Fsm_FsmHdOptionReadNewOnly(hdInfo->options) == FALSE) {
1091    fromBetween = bdd_squeeze(temp, nonInteriorStates);
1092    mdd_free(temp);
1093  } else {
1094    fromBetween = temp;
1095  }
1096  mdd_free(nonInteriorStates);
1097
1098  if (nvars <= 1023) {
1099    FsmHdStatsComputeSizeAndMinterms(mddManager, fromBetween,
1100                                     varArray, nvars,
1101                                     Fsm_Hd_From, hdInfo->stats);
1102  }
1103   
1104  /* if from is bigger in size than image, use image as from*/
1105  if (( Fsm_FsmHdOptionReadNewOnly(hdInfo->options) == FALSE) && (*image != NULL) &&
1106      (FsmHdStatsReadSizeTo(hdInfo->stats) < FsmHdStatsReadSizeFrom(hdInfo->stats))) {
1107    mdd_free(fromBetween);
1108    FsmHdStatsSetSizeFrom(hdInfo->stats, FsmHdStatsReadSizeTo(hdInfo->stats));
1109    FsmHdStatsSetMintermFrom(hdInfo->stats, FsmHdStatsReadMintermTo(hdInfo->stats));
1110    fromBetween = *image;
1111    *image = NULL;
1112  }
1113
1114  /* free image since no longer required */
1115  if (*image != NULL) mdd_free(*image);
1116
1117  assert(FsmHdStatsReadMintermFromSubset(hdInfo->stats) == 0.0);
1118  assert(FsmHdStatsReadSizeFromSubset(hdInfo->stats) == 0);
1119
1120  /* flag to indicate whether a subset is computed this time */
1121  thisTimeSubset = 0;
1122
1123  /* if size of from exceeds threshold, subset */
1124  if ((FsmHdStatsReadSizeFrom(hdInfo->stats) >  frontierApproxThreshold) &&
1125      (FsmHdStatsReadSizeFrom(hdInfo->stats) > FSM_HD_MIN_SIZE_FROM)) {
1126
1127    /* get subset based on the different methods */
1128    fromSubset = ComputeSubsetBasedOnMethod(fromBetween,
1129                                            *fromLowerBound, hdInfo->options,
1130                                            FSM_HD_FROM);
1131    if (nvars <= 1023) {
1132      /* record stats */
1133      FsmHdStatsComputeSizeAndMinterms(mddManager, fromSubset,
1134                             varArray, nvars, 
1135                           Fsm_Hd_FromSubset, hdInfo->stats);
1136      /* compute density */
1137      densityFromSubset = FsmHdStatsReadDensityFromSubset(hdInfo->stats);
1138      densityFrom = FsmHdStatsReadDensityFrom(hdInfo->stats);
1139    }
1140               
1141    /* check density of subset, discard the subset if not required*/
1142    if (((nvars <= 1023) &&
1143         (((densityFrom < densityFromSubset) ||
1144            (FsmHdStatsReadSizeFrom(hdInfo->stats) > 2*frontierApproxThreshold)))) ||
1145        ((nvars > 1023) &&
1146         ((bdd_apa_compare_ratios(nvars, fromSubset, fromBetween,
1147                                  FsmHdStatsReadSizeFromSubset(hdInfo->stats),
1148                                  FsmHdStatsReadSizeFrom(hdInfo->stats)) ||
1149            (FsmHdStatsReadSizeFrom(hdInfo->stats) > 2*frontierApproxThreshold))))) {
1150
1151      /* subset chosen this time */
1152      thisTimeSubset = 1;
1153     
1154      mdd_free(fromBetween);
1155
1156      /* discard the old bounds only if not required later */
1157      if (hdInfo->deadEndComputation || hdInfo->firstSubset) {
1158        /* store the residue since subset has been taken. Use them in
1159           subsequent iterations*/
1160        hdInfo->deadEndResidue = SubtractStates(*fromLowerBound, fromSubset,
1161                                         FSM_HD_DONT_FREE, FSM_HD_DONT_FREE);
1162        if(mdd_is_tautology(hdInfo->deadEndResidue, 0)) {
1163          mdd_free(hdInfo->deadEndResidue);
1164          hdInfo->deadEndResidue = NULL;
1165        } else if (mdd_size(hdInfo->deadEndResidue) > FSM_HD_DEADEND_RESIDUE_LIMIT) {
1166          mdd_free(hdInfo->deadEndResidue);
1167          hdInfo->deadEndResidue = NULL;
1168        } else {
1169          hdInfo->firstSubset = 0;
1170        }
1171               
1172      }
1173     
1174      /* set from lower bound for next image computation */
1175      mdd_free(*fromLowerBound);
1176      *fromLowerBound = fromSubset;
1177                   
1178    }  else {
1179      /* discard the old bounds; since no subset is discarded */
1180      mdd_free(*fromLowerBound);
1181      /* Undo subset computation */
1182      mdd_free(fromSubset);
1183      *fromLowerBound = fromBetween;
1184    }
1185  } else {
1186    /* No subsetting here */
1187    mdd_free(*fromLowerBound);
1188    *fromLowerBound = fromBetween;
1189  }
1190
1191  /* remove frontier from dead-end residue */
1192  if ((hdInfo->deadEndResidue != NULL) && (!hdInfo->deadEndComputation)) {
1193    hdInfo->deadEndResidue = SubtractStates(hdInfo->deadEndResidue, *fromLowerBound,
1194                                     FSM_HD_FREE, FSM_HD_DONT_FREE);
1195    if (mdd_is_tautology(hdInfo->deadEndResidue, 0)) {
1196      mdd_free(hdInfo->deadEndResidue);
1197      hdInfo->deadEndResidue = NULL;
1198    } else if (mdd_size(hdInfo->deadEndResidue) > FSM_HD_DISJ_SIZE) {
1199      mdd_free(hdInfo->deadEndResidue);
1200      hdInfo->deadEndResidue = NULL;
1201    }
1202  }
1203
1204  /*
1205   * check size of reached if there were any reorderings since
1206   * the last time the size was measured
1207   */
1208  if (bdd_read_reorderings(mddManager)> numReorders) {
1209    FsmHdStatsSetSizeReached(hdInfo->stats, mdd_size(*reachableStates));
1210  }
1211  /* Modify Reachable states if necessary. The conditions are if
1212   * blocking states are not to be included in Reached. The exceptions
1213   * are if no subset was computed or the size of Reached is less than
1214   * 30000 or if this were a DEAD-END computation (very important:
1215   * this rule isnt violated). That is ALL states computed out of a
1216   * DEAD_END must ALWAYS be added to reached.
1217   */
1218  if (thisTimeSubset && (Fsm_FsmHdOptionReadScrapStates(hdInfo->options) == FALSE) &&
1219      (!hdInfo->deadEndComputation) && 
1220      (FsmHdStatsReadSizeReached(hdInfo->stats) > 30000)) {
1221    temp = AddStates(*fromUpperBound, *fromLowerBound,
1222                     FSM_HD_FREE, FSM_HD_DONT_FREE);
1223    temp1 = bdd_squeeze(temp, *reachableStates);
1224    mdd_free(*reachableStates);
1225    mdd_free(temp);
1226    *reachableStates = temp1;
1227    FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates, varArray,
1228                           nvars, Fsm_Hd_Reached, hdInfo->stats);
1229    if (shellFlag && onionRings) { /* restrict the onion rings to the modified reachable set */
1230      int onionRingCount;
1231      for (onionRingCount = sizeOfOnionRings; onionRingCount < array_n(onionRings);
1232           onionRingCount++) {
1233        mdd_t *onionRing;
1234        onionRing = array_fetch(mdd_t *, onionRings, onionRingCount);
1235        temp = mdd_and(onionRing, *reachableStates, 1, 1);
1236        mdd_free(onionRing);
1237        array_insert(mdd_t *, onionRings, onionRingCount, temp);
1238      }
1239    }
1240
1241  } else {
1242    mdd_free(*fromUpperBound);
1243  }
1244
1245  /* Throw away dead-end residue when it gets to be a pain.
1246   * i.e., when its density is larger than Reached or when the
1247   * fraction of minterms retained in it are too small.
1248   */
1249  if (hdInfo->deadEndResidue != NULL) {
1250    mintResidue = mdd_count_onset(mddManager, hdInfo->deadEndResidue, varArray);
1251    sizeResidue = mdd_size(hdInfo->deadEndResidue);
1252    if ((mintResidue <  0.001*FsmHdStatsReadMintermReached(hdInfo->stats)) ||
1253        (mintResidue/sizeResidue > FsmHdStatsReadDensityReached(hdInfo->stats))) {
1254      mdd_free(hdInfo->deadEndResidue);
1255      hdInfo->deadEndResidue = NULL;
1256    }
1257  }
1258
1259  /* set fromUpperBound for the next iteration */
1260  *fromUpperBound = *fromLowerBound;
1261  return;
1262} /* end of FsmHdFromComputeDenseSubset */
1263
1264 
1265/*---------------------------------------------------------------------------*/
1266/* Definition of static functions                                          */
1267/*---------------------------------------------------------------------------*/
1268
1269/**Function********************************************************************
1270
1271  Synopsis    [Compute new seeds at dead-end]
1272
1273  Description [Compute new seeds at dead-end, depending on the dead
1274  end method. Hybrid method calls conjunct method.  Hybrid method
1275  tries a subset of (Reached-Interior) states first. The rest is
1276  shared between the hybrid and the conjuncts method. They proceed as
1277  follows: Decompose Reached and compute the image of small decomposed
1278  parts. If this fails to get new seeds (because decomposition failed
1279  to decompose reached into small enough parts) then compute a subset
1280  of the states whose image has not been computed. Finally give in and
1281  compute the image of a potentially large Reached. newSeeds is set to
1282  NULL if no new states. ]
1283
1284
1285  SideEffects []
1286
1287  SeeAlso [FsmHdDeadEnd ComputeImageOfDecomposedParts
1288  ComputeSubsetBasedOnMethod]
1289 
1290******************************************************************************/
1291static mdd_t *
1292ComputeNewSeedsAtDeadEnd(mdd_manager *mddManager,
1293                         Img_ImageInfo_t *imageInfo,
1294                         mdd_t *reachableStates,
1295                         FsmHdStruct_t *hdInfo, 
1296                         int greedy,
1297                         int verbosity)
1298{
1299  mdd_t *toCareSet, *newSeeds = NULL, *possibleSeeds, *temp;
1300  mdd_t *reachedSubset, *reachedSet;
1301  int failedPartition = 0;
1302  int frontierApproxThreshold =  Fsm_FsmHdOptionReadFrontierApproxThreshold(hdInfo->options);
1303  int deadEnd =  Fsm_FsmHdOptionReadDeadEnd(hdInfo->options);
1304  int nvars =  Fsm_FsmHdOptionReadNumVars(hdInfo->options);
1305 
1306  /* in brute force method, compute the image of the entire reached */
1307  if (deadEnd == Fsm_Hd_DE_BF_c) {
1308    toCareSet = mdd_not(reachableStates);
1309    possibleSeeds = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
1310                                                          reachableStates,
1311                                                          reachableStates,
1312                                                          toCareSet);
1313    mdd_free(toCareSet);
1314    newSeeds = SubtractStates(possibleSeeds, reachableStates,
1315                              FSM_HD_FREE, FSM_HD_DONT_FREE);
1316    return (newSeeds);
1317  }
1318
1319  /* in HYBRID method, first try with  a subset of the reached set */
1320  reachedSet = SubtractStates(reachableStates, hdInfo->interiorStates,
1321                            FSM_HD_DONT_FREE, FSM_HD_DONT_FREE);
1322  if (deadEnd ==  Fsm_Hd_DE_Hyb_c) {
1323    /* compute image of a subset of reached */
1324    reachedSubset = ComputeSubsetBasedOnMethod(reachedSet,
1325                                               NIL(mdd_t),
1326                                               hdInfo->options,
1327                                               FSM_HD_DEADEND);
1328                                               
1329    if (bdd_size(reachedSubset) < 2*frontierApproxThreshold) {
1330      toCareSet = mdd_not(reachableStates);
1331      possibleSeeds = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
1332                                                            reachedSubset,
1333                                                            reachableStates,
1334                                                            toCareSet);
1335      mdd_free(toCareSet);
1336      /* compute new states */
1337      newSeeds = SubtractStates(possibleSeeds, reachableStates,
1338                              FSM_HD_FREE, FSM_HD_DONT_FREE);
1339      /* add to interior states */
1340      hdInfo->interiorStates = AddStates(hdInfo->interiorStates, reachedSubset,
1341                                  FSM_HD_FREE, FSM_HD_DONT_FREE);
1342      if (verbosity >= 2) {
1343        fprintf(vis_stdout, "Interior states added, Size = %d\n",
1344                mdd_size(hdInfo->interiorStates));
1345      }
1346
1347      if ((!mdd_is_tautology(newSeeds, 0)) && (greedy))  {
1348        mdd_free(reachedSet);
1349        mdd_free(reachedSubset);
1350        return (newSeeds);
1351      } else {
1352        /* reset newSeeds value for further computations */
1353        if (mdd_is_tautology(newSeeds, 0)) {
1354          mdd_free(newSeeds);
1355          newSeeds = NULL;
1356        }
1357        /* if new seeds not found or iter_decomp unsuccessful, set
1358         * reachedSet to the other part (which may be a part of the
1359         * reachable states (former) or the reachable states itself
1360         * (latter)).
1361         */
1362        reachedSet = SubtractStates(reachedSet, reachedSubset,
1363                                      FSM_HD_FREE, FSM_HD_FREE);
1364      }
1365    } else {
1366      mdd_free(reachedSubset);
1367    }
1368  }
1369 
1370  /* compute the decomposed image of reachedSet */
1371  if ((deadEnd == Fsm_Hd_DE_Con_c) ||
1372      (deadEnd == Fsm_Hd_DE_Hyb_c)) {
1373    /* this flag is set when the image of some decomposed part is
1374     * not computed due to its size.
1375     */
1376    failedPartition = 0;
1377    /* save any previously computed new states */
1378    temp = newSeeds;
1379    /* compute new seeds by recursively decomposing reachedSet */
1380    newSeeds = ComputeImageOfDecomposedParts(mddManager,
1381                                             imageInfo,
1382                                             reachedSet,
1383                                             reachableStates,
1384                                             hdInfo,
1385                                             frontierApproxThreshold,
1386                                             nvars,
1387                                             &failedPartition,
1388                                             greedy,
1389                                             verbosity);
1390    /* combine new states */
1391    newSeeds = AddStates(newSeeds, temp, FSM_HD_FREE, FSM_HD_FREE);
1392
1393    /* if no remains or partition didnt fail, return new Seeds */
1394    /* if greedy and new states found, return */
1395    if ((mdd_lequal(reachedSet, hdInfo->interiorStates, 1, 1)) ||
1396        ((newSeeds != NULL) && (greedy))) {
1397      /* assert that the entire image was computed */
1398      if (mdd_lequal(reachedSet, hdInfo->interiorStates, 1, 1)) assert(!failedPartition);
1399      mdd_free(reachedSet);
1400      if (newSeeds == NULL)
1401        newSeeds = bdd_zero(mddManager);
1402      else
1403        assert(!mdd_is_tautology(newSeeds, 0));
1404      return(newSeeds);
1405    }
1406
1407    /* continue if either no new states have been found or the
1408     * computation is not greedy */
1409    /* new set whose image is to be computed  */
1410    reachedSet = SubtractStates(reachedSet, hdInfo->interiorStates,
1411                                FSM_HD_FREE, FSM_HD_DONT_FREE);
1412   
1413   
1414    /* one last shot with a subsetting the remains */
1415    /* reachedSubset is the subset of reached remains */
1416    reachedSubset = ComputeSubsetBasedOnMethod(reachedSet,
1417                                               NIL(mdd_t),
1418                                               hdInfo->options,
1419                                               FSM_HD_DEADEND);
1420       
1421    /* compute image of the subset above */
1422    toCareSet = mdd_not(reachableStates);
1423    possibleSeeds = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
1424                                                          reachedSubset,
1425                                                          reachableStates,
1426                                                          toCareSet);
1427    mdd_free(toCareSet);
1428    /* add to interior states */
1429    hdInfo->interiorStates = AddStates(hdInfo->interiorStates, reachedSubset,
1430                                FSM_HD_FREE, FSM_HD_FREE);
1431    if (verbosity >= 2) {
1432      fprintf(vis_stdout, "Interior states added, Size = %d\n",
1433              mdd_size(hdInfo->interiorStates));
1434    }
1435    /* combine all new states */
1436    temp = newSeeds;
1437    newSeeds = SubtractStates(possibleSeeds, reachableStates,
1438                              FSM_HD_FREE, FSM_HD_DONT_FREE);
1439    newSeeds = AddStates(newSeeds, temp, FSM_HD_FREE, FSM_HD_FREE);
1440
1441    /* if no new seeds, compute the image of (reachedSet - reachedSubset) */
1442    if ((mdd_is_tautology(newSeeds, 0) != 1) && (greedy)) {
1443      mdd_free(reachedSet);
1444      mdd_free(reachedSubset);
1445      return newSeeds;
1446    } else {
1447      /* reset newSeeds for further computation */
1448      if (mdd_is_tautology(newSeeds, 0)) {
1449        mdd_free(newSeeds);
1450        newSeeds = NULL;
1451      }
1452      /* set reached = reachedSet - reachedSubset */
1453      reachedSet  = SubtractStates(reachedSet, reachedSubset,
1454                                   FSM_HD_FREE, FSM_HD_FREE);
1455    }
1456
1457    /* save previously computed new states */
1458    temp = newSeeds;
1459    failedPartition = 0;
1460    /* try decomposition again */
1461    newSeeds = ComputeImageOfDecomposedParts(mddManager,
1462                                             imageInfo,
1463                                             reachedSet,
1464                                             reachableStates, hdInfo, 
1465                                             frontierApproxThreshold,
1466                                             nvars,
1467                                             &failedPartition,
1468                                             greedy,
1469                                             verbosity);
1470    /* combine all new states */
1471    newSeeds = AddStates(newSeeds, temp, FSM_HD_FREE, FSM_HD_FREE);
1472    /* if no remains or partition didnt fail, return new Seeds */
1473    /* if greedy and new states found, return */
1474    if ((mdd_lequal(reachedSet, hdInfo->interiorStates, 1, 1)) ||
1475        ((newSeeds != NULL) && (greedy))) {
1476      /* assert that the entire image was computed */
1477      if (mdd_lequal(reachedSet, hdInfo->interiorStates, 1, 1)) assert(!failedPartition);
1478      mdd_free(reachedSet);
1479      if (newSeeds == NULL)
1480        newSeeds = bdd_zero(mddManager);
1481      else
1482        assert(!mdd_is_tautology(newSeeds, 0));
1483      return(newSeeds);
1484    }
1485
1486    /* continue if either no new states have been found or the
1487     * computation is not greedy */
1488    /* new set whose image is to be computed  */
1489    reachedSet = SubtractStates(reachedSet, hdInfo->interiorStates,
1490                                FSM_HD_FREE, FSM_HD_DONT_FREE);
1491   
1492    /* now bite the bullet and compute the image of the whole
1493     * remainder.
1494     */
1495    toCareSet = mdd_not(reachableStates);
1496    possibleSeeds = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
1497                                                          reachedSet,
1498                                                          reachableStates,
1499                                                          toCareSet);
1500    mdd_free(toCareSet);
1501    /* add to interios states */
1502    hdInfo->interiorStates = AddStates(hdInfo->interiorStates, reachedSet,
1503                                FSM_HD_FREE, FSM_HD_FREE);
1504    if (verbosity >= 2) {
1505      fprintf(vis_stdout, "Interior states added, Size = %d\n",
1506              mdd_size(hdInfo->interiorStates));
1507    }
1508    /* combine all new states */
1509    temp = newSeeds;
1510    newSeeds = SubtractStates(possibleSeeds, reachableStates,
1511                              FSM_HD_FREE, FSM_HD_DONT_FREE);
1512    newSeeds = AddStates(newSeeds, temp, FSM_HD_FREE, FSM_HD_FREE);
1513
1514  }
1515  return newSeeds;
1516}
1517
1518
1519/**Function********************************************************************
1520
1521  Synopsis [Compute image of decomposed reached set until new seeds
1522  are found.]
1523
1524  Description [Compute image of decomposed reached set until new seeds
1525  are found. This procedure is obliged to return newSeeds = NULL if no
1526  new seeds are found. The recursive procedure tries to decompose
1527  Reached. The return value is the set of new states. ]
1528
1529  SideEffects []
1530 
1531  SeeAlso [ComputeNewSeedsAtDeadEnd ProcessDisjunctsRecursive]
1532
1533******************************************************************************/
1534static mdd_t *
1535ComputeImageOfDecomposedParts(mdd_manager *mddManager,
1536                              Img_ImageInfo_t *imageInfo,
1537                              mdd_t *reachedSet,
1538                              mdd_t *reachableStates,
1539                              FsmHdStruct_t *hdInfo, 
1540                              int frontierApproxThreshold,
1541                              int nvars,
1542                              int *failedPartition,
1543                              int greedy,
1544                              int verbosity)
1545{
1546
1547  mdd_t *temp, *newSeeds, *possibleSeeds;
1548  mdd_t *toCareSet;
1549  int reachedSize, threshold;
1550   
1551  /* initialize some variables */
1552  newSeeds = NULL;
1553  reachedSize = mdd_size(reachedSet);
1554  threshold = (FSM_HD_REACHED_THRESHOLD > frontierApproxThreshold) ? FSM_HD_REACHED_THRESHOLD : frontierApproxThreshold;
1555
1556  /* compute the image of reached if it is small */
1557  if (reachedSize < threshold) {
1558    toCareSet = mdd_not(reachableStates);
1559    possibleSeeds = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
1560                                                          reachedSet,
1561                                                          reachableStates,
1562                                                          toCareSet);
1563    mdd_free(toCareSet);
1564    newSeeds = SubtractStates(possibleSeeds, reachableStates,
1565                              FSM_HD_FREE, FSM_HD_DONT_FREE);
1566    if (mdd_is_tautology(newSeeds, 0)) {
1567      mdd_free(newSeeds);
1568      newSeeds = NULL;
1569    }
1570    hdInfo->interiorStates = AddStates(hdInfo->interiorStates, reachedSet,
1571                                FSM_HD_FREE, FSM_HD_DONT_FREE);
1572    return (newSeeds);
1573  }
1574
1575  /* create conjuncts of the complement, disjuncts of the
1576   * reachable set
1577   */
1578  temp = mdd_dup(reachedSet);
1579  /* set threshold to some non-trivial value */
1580  if (frontierApproxThreshold <= 0)
1581    frontierApproxThreshold = FSM_HD_REACHED_THRESHOLD/
1582      FSM_HD_DEADEND_MAX_SIZE_FACTOR;
1583  /* compute the image of decomposed parts. Return when some new seeds are
1584   * found.
1585   */
1586  newSeeds = ProcessDisjunctsRecursive(mddManager,
1587                                       imageInfo,
1588                                       &temp,
1589                                       reachableStates,
1590                                       hdInfo, 
1591                                       frontierApproxThreshold,
1592                                       nvars,
1593                                       failedPartition,
1594                                       reachedSize,
1595                                       greedy,
1596                                       verbosity);
1597                                         
1598  return (newSeeds);
1599   
1600}
1601
1602/**Function********************************************************************
1603
1604  Synopsis    [Computes the image of decomposed reached greedily]
1605
1606  Description [Computes the image of decomposed reached
1607  greedily. Recursive procedure that decomposes product into two
1608  conjuncts at each call. In the greedy procedure, decomposition stops
1609  if the computed partitions are below a certain threshold. The image
1610  of all partitions under this threshold are computed. Also subsets of
1611  the remaining large partitions are considered for image
1612  computation. newSeeds is set to NULL if no new states are found.  If
1613  any partition cannot be decomposed any further and it is too large,
1614  then its image is not computed and the failed partition flag is
1615  set. The calling procedure should infer this partition from the
1616  interior states and compute its image.]
1617
1618  SideEffects [Frees reachedSet]
1619
1620   SeeAlso [ComputeImageOfDecomposedParts]
1621 
1622******************************************************************************/
1623static mdd_t *
1624ProcessDisjunctsRecursive(mdd_manager *mddManager,
1625                          Img_ImageInfo_t *imageInfo,
1626                          mdd_t **reachedSet,
1627                          mdd_t *reachableStates,
1628                          FsmHdStruct_t *hdInfo, 
1629                          int frontierApproxThreshold,
1630                          int nvars,
1631                          int *failedPartition,
1632                          int reachedSize,
1633                          int greedy,
1634                          int verbosity)
1635{
1636  mdd_t *toCareSet, *newSeeds, *possibleSeeds;
1637  mdd_t *temp, *subset;
1638  int  tempSize;
1639  int hitConstant;
1640  mdd_t **disjArray;
1641  char *decompString;
1642  int i;
1643  int numParts;
1644  FsmHdSizeStruct_t sizeStruct;
1645  array_t *sizeArray;
1646 
1647  hitConstant = 0;
1648
1649  assert((!mdd_is_tautology(*reachedSet, 1)) &&
1650         (!mdd_is_tautology(*reachedSet, 0)));
1651  if (verbosity >= 2) {
1652    fprintf(vis_stdout, "Orig Size = %d, ",mdd_size(*reachedSet));
1653  }
1654
1655  /* decompose reached set into disjuntive parts */
1656  decompString = Cmd_FlagReadByName("hd_decomp");
1657  if (decompString == NIL(char)) {
1658    numParts = bdd_var_decomp(*reachedSet,
1659                                        (bdd_partition_type_t)BDD_DISJUNCTS,
1660                                        &disjArray);
1661  } else if (strcmp(decompString, "var") == 0) {
1662    numParts = bdd_var_decomp(*reachedSet,
1663                                        (bdd_partition_type_t)BDD_DISJUNCTS,
1664                                        &disjArray);
1665  } else if (strcmp(decompString, "gen") == 0) {
1666    numParts = bdd_gen_decomp(*reachedSet,
1667                                        (bdd_partition_type_t)BDD_DISJUNCTS,
1668                                        &disjArray);
1669  } else if (strcmp(decompString, "approx") == 0) {
1670    numParts = bdd_approx_decomp(*reachedSet,
1671                                           (bdd_partition_type_t)BDD_DISJUNCTS,
1672                                           &disjArray);
1673  } else if (strcmp(decompString, "iter") == 0) {
1674    numParts = bdd_iter_decomp(*reachedSet,
1675                                         (bdd_partition_type_t)BDD_DISJUNCTS,
1676                                         &disjArray);
1677  } else {
1678    numParts = bdd_var_decomp(*reachedSet,
1679                                        (bdd_partition_type_t)BDD_DISJUNCTS,
1680                                        &disjArray);
1681  }
1682  mdd_free(*reachedSet);
1683
1684  /* decomposition failed */
1685  if (numParts == 0) return NULL;
1686
1687  /* decomposition failed, stop recurring */
1688  if (numParts == 1) hitConstant = 1;
1689 
1690  /* allocate array with bdds and sizes */
1691  sizeArray = array_alloc(FsmHdSizeStruct_t,  0); 
1692  if (sizeArray == NIL(array_t)) {
1693    for (i = 0; i < numParts; i++) {
1694      mdd_free(disjArray[i]);
1695    }
1696    FREE(disjArray);
1697    return NULL;
1698  }
1699 
1700  /* free all constants and partitions that are larger than the
1701   * original reached size
1702   */
1703  for (i = 0; i < numParts; i++) {
1704    assert(!mdd_is_tautology(disjArray[i], 1));
1705    tempSize = bdd_size(disjArray[i]);
1706    if ((tempSize >= reachedSize) ||
1707        (tempSize == 1)) {
1708      if (tempSize == 1) {
1709        hitConstant = 1;
1710        assert (mdd_is_tautology(disjArray[i], 0));
1711      } else {
1712        *failedPartition = 1;
1713      }
1714      mdd_free(disjArray[i]);
1715    } else {
1716      sizeStruct.bdd = disjArray[i];
1717      sizeStruct.size = tempSize;
1718      sizeStruct.rnd = util_random();
1719      array_insert_last(FsmHdSizeStruct_t, sizeArray, sizeStruct);
1720    }
1721  }
1722  FREE(disjArray);
1723
1724  if (array_n(sizeArray) == 0) {
1725    array_free(sizeArray);
1726    return (NULL);
1727  }
1728 
1729  /* shuffle parts randomly. */
1730  if (array_n(sizeArray) > 1) {
1731    array_sort(sizeArray, RandomCompare);
1732  } 
1733
1734  if (verbosity >= 2) {
1735    arrayForEachItem(FsmHdSizeStruct_t, sizeArray, i, sizeStruct) {
1736      fprintf(vis_stdout , "disjSize[%d] = %d ", i, sizeStruct.size);
1737    }
1738    fprintf(vis_stdout, "\n");
1739  }
1740 
1741  /* now compute image of parts or recur*/
1742  newSeeds = NULL;
1743  arrayForEachItem(FsmHdSizeStruct_t, sizeArray, i, sizeStruct) {
1744    temp = NULL;
1745    if ((sizeStruct.size <
1746         frontierApproxThreshold*FSM_HD_DEADEND_MAX_SIZE_FACTOR) ||
1747        (sizeStruct.size < FSM_HD_DISJ_SIZE)) {
1748      /* if this partition is small enough, compute its image */
1749      /* compute image */
1750      toCareSet = mdd_not(reachableStates);
1751      possibleSeeds = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
1752                                                            sizeStruct.bdd,
1753                                                            reachableStates,
1754                                                            toCareSet); 
1755      mdd_free(toCareSet);
1756      /* update interior states */
1757      hdInfo->interiorStates = AddStates(hdInfo->interiorStates, sizeStruct.bdd,
1758                                  FSM_HD_FREE, FSM_HD_FREE);
1759      if (verbosity >= 2) {
1760        fprintf(vis_stdout, "Interior states added, Size = %d\n",
1761                mdd_size(hdInfo->interiorStates));
1762      }
1763      /* store new states if any were already found */
1764      temp = newSeeds;
1765      /* compute new states of this image */
1766      newSeeds = SubtractStates(possibleSeeds, reachableStates,
1767                              FSM_HD_FREE, FSM_HD_DONT_FREE);
1768      /* add up states or set newSeeds to NULL if no new states */
1769      if (temp != NULL) {
1770        assert(!mdd_is_tautology(temp, 0));
1771        newSeeds = AddStates(newSeeds, temp, FSM_HD_FREE, FSM_HD_FREE);
1772      } else if (mdd_is_tautology(newSeeds, 0) == 1) {
1773        mdd_free(newSeeds);
1774        newSeeds = NULL;
1775      } 
1776    } else if ((!hitConstant) && ((newSeeds == NULL) ||
1777                                  (!greedy) ||
1778                                  (sizeStruct.size < 3* FSM_HD_DISJ_SIZE))) {
1779      /* recur if size is small enough, or non-greedy computation or
1780       * no new states have been found yet. But not if a constant is hit. */
1781      /* store any new states already computed */
1782      temp = newSeeds;
1783      newSeeds = ProcessDisjunctsRecursive(mddManager,
1784                                           imageInfo,
1785                                           &(sizeStruct.bdd),
1786                                           reachableStates, hdInfo, 
1787                                           frontierApproxThreshold,
1788                                           nvars,
1789                                           failedPartition,
1790                                           reachedSize,
1791                                           greedy,
1792                                           verbosity);
1793      /* if new seeds not NULL, then not zero either */
1794      if (newSeeds != NULL) {
1795        assert(!mdd_is_tautology(newSeeds, 0));
1796        /* add states */
1797        if (temp != NULL) {
1798          newSeeds = AddStates(temp, newSeeds, FSM_HD_FREE, FSM_HD_FREE);
1799        }
1800      } else {
1801        newSeeds = temp;
1802      }
1803    } else {
1804      /* if this partition is too large, compute the image of its
1805       *  subset if the subset is small enough */
1806      /* set failed partition as image is not being computed of this
1807       *  whole part */
1808      *failedPartition = 1;
1809      /* compute subset */
1810      subset = bdd_approx_remap_ua(sizeStruct.bdd,
1811                                   (bdd_approx_dir_t)BDD_UNDER_APPROX,
1812                                   nvars, 0, 1.0);
1813      mdd_free(sizeStruct.bdd);
1814      tempSize = bdd_size(subset);
1815      /* compute image of subset if small enough */
1816      if ((tempSize < frontierApproxThreshold*FSM_HD_DEADEND_MAX_SIZE_FACTOR) ||
1817          (tempSize < FSM_HD_DISJ_SIZE)) {
1818        /* compute image */
1819        toCareSet = mdd_not(reachableStates);
1820        possibleSeeds = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
1821                                                              subset,
1822                                                              reachableStates,
1823                                                              toCareSet);
1824        mdd_free(toCareSet);
1825        /* update dead states */
1826        hdInfo->interiorStates = AddStates(hdInfo->interiorStates, subset,
1827                                    FSM_HD_FREE, FSM_HD_FREE);
1828        if (verbosity >= 2) {
1829          fprintf(vis_stdout, "Interior states added, Size = %d\n",
1830                  mdd_size(hdInfo->interiorStates));
1831        }
1832        /* store new states if any were already found */
1833        temp = newSeeds;
1834        /* compute new states of this image */
1835        newSeeds = SubtractStates(possibleSeeds, reachableStates,
1836                                FSM_HD_FREE, FSM_HD_DONT_FREE);
1837        /* add up states or set newSeeds to NULL if no new states */
1838        if (temp != NULL) {
1839          assert(!mdd_is_tautology(temp, 0));
1840          newSeeds = AddStates(newSeeds, temp, FSM_HD_FREE, FSM_HD_FREE);
1841        } else if (mdd_is_tautology(newSeeds, 0) == 1) {
1842          mdd_free(newSeeds);
1843          newSeeds = NULL;
1844        }       
1845      } else {
1846        mdd_free(subset);
1847      }
1848    }
1849  } /* end of array for each */
1850
1851  array_free(sizeArray);
1852               
1853  return (newSeeds);
1854
1855} /* end of ProcessDisjunctsRecursive */
1856
1857
1858
1859/**Function********************************************************************
1860
1861  Synopsis    [Computes the subset of the from set]
1862
1863  Description [Computes the subset of the from set. Makes sure that
1864  there are some new states. Returns the subset as computing be the
1865  specified approximation method.]
1866
1867
1868  SideEffects []
1869
1870******************************************************************************/
1871static mdd_t *
1872ComputeSubsetBasedOnMethod(mdd_t *fromBetween,
1873                           mdd_t *fromLowerBound,
1874                           FsmHdTravOptions_t *options,
1875                           int fromOrDeadEnd)
1876{
1877  mdd_t *fromSubset;
1878  int frontierApproxThreshold =  Fsm_FsmHdOptionReadFrontierApproxThreshold(options);
1879  int frontierApproxMethod;
1880  double quality =  Fsm_FsmHdOptionReadQuality(options);
1881  int nvars =  Fsm_FsmHdOptionReadNumVars(options);
1882                             
1883 
1884  frontierApproxMethod = (fromOrDeadEnd == FSM_HD_FROM) ?
1885     Fsm_FsmHdOptionReadFrontierApproxMethod(options) :
1886    ((fromOrDeadEnd == FSM_HD_DEADEND) ?
1887      Fsm_FsmHdOptionReadDeadEndSubsetMethod(options) :
1888      Fsm_FsmHdOptionReadFrontierApproxMethod(options));
1889 
1890  /* based on approximation method specified, compute subset */
1891  switch (frontierApproxMethod) {
1892  case BDD_APPROX_HB:
1893    frontierApproxThreshold = (frontierApproxThreshold < FSM_HD_SP_THRESHOLD) ? FSM_HD_SP_THRESHOLD: frontierApproxThreshold;
1894    fromSubset = bdd_approx_hb(fromBetween,
1895                               (bdd_approx_dir_t)BDD_UNDER_APPROX,
1896                               nvars, frontierApproxThreshold);
1897    if (fromLowerBound != NIL(mdd_t)) {
1898      if (!bdd_equal(fromBetween,fromLowerBound))  {
1899        if (mdd_lequal(fromSubset, fromLowerBound, 1, 0)) {
1900          mdd_free(fromSubset);
1901          fromSubset = bdd_approx_hb(fromLowerBound,
1902                                     (bdd_approx_dir_t)BDD_UNDER_APPROX,
1903                                     nvars, frontierApproxThreshold);
1904        }
1905      }
1906    }
1907                   
1908    break;
1909  case BDD_APPROX_SP:
1910    frontierApproxThreshold = (frontierApproxThreshold < FSM_HD_SP_THRESHOLD) ? FSM_HD_SP_THRESHOLD: frontierApproxThreshold;
1911    fromSubset = bdd_approx_sp(fromBetween,
1912                               (bdd_approx_dir_t)BDD_UNDER_APPROX,
1913                               nvars, frontierApproxThreshold,
1914                               0);
1915    if (fromLowerBound != NIL(mdd_t)) {
1916      if (!bdd_equal(fromBetween,fromLowerBound))  {
1917        if (mdd_lequal(fromSubset, fromLowerBound, 1, 0)) {
1918          mdd_free(fromSubset);
1919          fromSubset = bdd_approx_sp(fromLowerBound,
1920                                     (bdd_approx_dir_t)BDD_UNDER_APPROX,
1921                                     nvars, frontierApproxThreshold,
1922                                     0);
1923        }
1924      }
1925    }
1926                   
1927    break;
1928  case BDD_APPROX_UA:
1929    fromSubset = bdd_approx_ua(fromBetween,
1930                               (bdd_approx_dir_t)BDD_UNDER_APPROX,
1931                               nvars, frontierApproxThreshold,
1932                               0, quality);
1933    if (fromLowerBound != NIL(mdd_t)) {
1934      if (!bdd_equal(fromBetween,fromLowerBound))  {
1935        if (mdd_lequal(fromSubset, fromLowerBound, 1, 0)) {
1936          mdd_free(fromSubset);
1937          fromSubset = bdd_approx_ua(fromLowerBound,
1938                                     (bdd_approx_dir_t)BDD_UNDER_APPROX,
1939                                     nvars, frontierApproxThreshold,
1940                                     0, quality);
1941        }
1942      }
1943    }
1944    break;
1945  case BDD_APPROX_RUA:
1946    fromSubset = bdd_approx_remap_ua(fromBetween,
1947                                     (bdd_approx_dir_t)BDD_UNDER_APPROX,
1948                                     nvars, frontierApproxThreshold,
1949                                     quality );
1950    if (fromLowerBound != NIL(mdd_t)) {
1951      if (!bdd_equal(fromBetween,fromLowerBound))  {
1952        if (mdd_lequal(fromSubset, fromLowerBound, 1, 0)) {
1953          mdd_free(fromSubset);
1954          fromSubset = bdd_approx_remap_ua(fromLowerBound,
1955                                           (bdd_approx_dir_t)BDD_UNDER_APPROX,
1956                                           nvars, frontierApproxThreshold,
1957                                           quality);
1958        }
1959      }
1960    }
1961                   
1962    break;
1963  case BDD_APPROX_BIASED_RUA:
1964    if (fromLowerBound == NIL(mdd_t)) {
1965      fromLowerBound = fromBetween;
1966    }
1967    fromSubset = bdd_approx_biased_rua(fromBetween,
1968                                     (bdd_approx_dir_t)BDD_UNDER_APPROX,
1969                                       fromLowerBound,
1970                                       nvars, frontierApproxThreshold,
1971                                     quality, options->qualityBias );
1972    if (fromLowerBound != NIL(mdd_t)) {
1973      if (!bdd_equal(fromBetween,fromLowerBound))  {
1974        if (mdd_lequal(fromSubset, fromLowerBound, 1, 0)) {
1975          mdd_free(fromSubset);
1976          fromSubset = bdd_approx_remap_ua(fromLowerBound,
1977                                           (bdd_approx_dir_t)BDD_UNDER_APPROX,
1978                                           nvars, frontierApproxThreshold,
1979                                           quality);
1980        }
1981      }
1982    }
1983    break;
1984  case BDD_APPROX_COMP:
1985    frontierApproxThreshold = (frontierApproxThreshold < FSM_HD_SP_THRESHOLD) ? FSM_HD_SP_THRESHOLD: frontierApproxThreshold;
1986    fromSubset = bdd_approx_compress(fromBetween,
1987                                     (bdd_approx_dir_t)BDD_UNDER_APPROX,
1988                                     nvars, frontierApproxThreshold);
1989
1990    if (fromLowerBound != NIL(mdd_t)) {
1991      if (!bdd_equal(fromBetween,fromLowerBound))  {
1992        if (mdd_lequal(fromSubset, fromLowerBound, 1, 0)) {
1993          mdd_free(fromSubset);
1994          fromSubset = bdd_approx_compress(fromLowerBound,
1995                                           (bdd_approx_dir_t)BDD_UNDER_APPROX,
1996                                           nvars, frontierApproxThreshold);
1997        }
1998      }
1999    }
2000
2001    break;
2002  default:
2003    fromSubset = bdd_approx_remap_ua(fromBetween,
2004                                     (bdd_approx_dir_t)BDD_UNDER_APPROX,
2005                                     nvars, frontierApproxThreshold,
2006                                     quality );
2007    if (fromLowerBound != NIL(mdd_t)) {
2008      if (!bdd_equal(fromBetween,fromLowerBound))  {
2009        if (mdd_lequal(fromSubset, fromLowerBound, 1, 0)) {
2010          mdd_free(fromSubset);
2011          fromSubset = bdd_approx_remap_ua(fromLowerBound,
2012                                           (bdd_approx_dir_t)BDD_UNDER_APPROX,
2013                                           nvars, frontierApproxThreshold,
2014                                           quality);
2015        }
2016      }
2017    }
2018    break;
2019  }
2020
2021  return (fromSubset);
2022} /* end of ComputeSubsetBasedOnMethod */
2023
2024
2025/**Function********************************************************************
2026
2027  Synopsis    [Add states.]
2028
2029  Description [Add States.]
2030
2031  SideEffects [ Free the original parts]
2032
2033******************************************************************************/
2034static mdd_t *
2035AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB)
2036{
2037  mdd_t *result;
2038  if ((a != NULL) && (b != NULL)) {
2039    result = mdd_or(a, b, 1, 1);
2040  } else if ((a == NULL) && (b == NULL)) {
2041    result = a;
2042  } else if (a == NULL) {
2043    result = mdd_dup(b);
2044  } else {
2045    result =  mdd_dup(a);
2046  }
2047  if ((freeA == FSM_HD_FREE) && (a != NULL))  mdd_free(a);
2048  if ((freeB == FSM_HD_FREE) && (b != NULL)) mdd_free(b);
2049  return result;
2050} /* end of AddStates */
2051
2052
2053
2054/**Function********************************************************************
2055
2056  Synopsis    [Subtract states b from a.]
2057
2058  Description [Subtract states b from a.]
2059
2060  SideEffects [ Free the original parts]
2061
2062******************************************************************************/
2063static mdd_t *
2064SubtractStates(mdd_t *a, mdd_t *b, int freeA, int freeB)
2065{
2066  mdd_t *result;
2067  if ((a != NULL) && (b != NULL)) {
2068    result = mdd_and(a, b, 1, 0);
2069  } else if ((a == NULL) && (b == NULL)) {
2070    result = a;
2071  } else if (b == NULL) {
2072    result =  mdd_dup(a);
2073  } else { /* a = NULL , b != NULL */
2074    result = NULL;
2075  }
2076  if ((freeA == FSM_HD_FREE) && (a != NULL))  mdd_free(a);
2077  if ((freeB == FSM_HD_FREE) && (b != NULL)) mdd_free(b);
2078  return result;
2079} /* end of SubtractStates */
2080
2081
2082/**Function********************************************************************
2083
2084  Synopsis    [Random Comparison fn.]
2085
2086  Description [Random Comparison fn.]
2087
2088  SideEffects [ ]
2089
2090******************************************************************************/
2091static int
2092RandomCompare(const void *ptrX,
2093              const void *ptrY)
2094{
2095  FsmHdSizeStruct_t *sizeStruct1 = (FsmHdSizeStruct_t *)ptrX;
2096  FsmHdSizeStruct_t *sizeStruct2 = (FsmHdSizeStruct_t *)ptrY;
2097
2098  if (sizeStruct1->rnd > sizeStruct2->rnd) return 1;
2099  else if (sizeStruct1->rnd < sizeStruct2->rnd) return -1;
2100  else return 0;
2101} /* end of BddSizeCompare */
Note: See TracBrowser for help on using the repository browser.