source: vis_dev/vis-2.3/src/fsm/fsmReach.c @ 84

Last change on this file since 84 was 15, checked in by cecile, 13 years ago

Vis main file for expermeriments
File size: 80.8 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [fsmReach.c]
4
5  PackageName [fsm]
6
7  Synopsis    [Routines to perform reachability on the FSM structure.]
8
9  Author      [Rajeev K. Ranjan, In-Ho Moon, Kavita Ravi]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30******************************************************************************/
31
32#include "fsmInt.h"
33#include "bdd.h"
34#include "ntm.h"
35#include "img.h"
36#include "sim.h"
37
38static char rcsid[] UNUSED = "$Id: fsmReach.c,v 1.102 2009/04/11 01:40:54 fabio Exp $";
39
40/*---------------------------------------------------------------------------*/
41/* Constant declarations                                                     */
42/*---------------------------------------------------------------------------*/
43/* HD constants */
44#define FSM_HD_NONGREEDY 0 /* flag to indicate non-greedy computation at
45                              dead-ends */
46#define FSM_HD_GREEDY 1 /* flag to indicate greedy computation at dead-ends */
47#define FSM_HD_LARGE_SIZE 100000 /* size considered large for reached */
48#define FSM_HD_MID_SIZE 50000    /* size considered medium for reached*/
49#define FSM_HD_MINT_GROWTH 0.5   /* factor measuring minterm jump of reached*/
50#define FSM_HD_GROWTH_RATE 0.04 /* Growth rate for reached in measuring slow
51                                 * growth. */
52#define FSM_MDD_DONT_FREE 0  /* flag to indicate that bdd should not be freed. */
53#define FSM_MDD_FREE 1       /* flag to indicate that bdd should be freed.*/
54#define FSM_HD_NUM_SLOW_GROWTHS 5 /* number of iterations of allowed
55                                   * slow growth of reached. */
56/*---------------------------------------------------------------------------*/
57/* Structure declarations                                                    */
58/*---------------------------------------------------------------------------*/
59
60/**AutomaticStart*************************************************************/
61
62/*---------------------------------------------------------------------------*/
63/* Static function prototypes                                                */
64/*---------------------------------------------------------------------------*/
65
66static int CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray);
[15]67/*static*/ int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray);
[14]68static mdd_t * AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB);
69static void RandomSimulation(int simNVec, Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag, mdd_t *initialStates, mdd_t **reachableStates, mdd_t **fromLowerBound, FsmHdStruct_t *hdInfo);
70static void PrintStatsPerIteration(Fsm_RchType_t approxFlag, int nvars, int depth, FsmHdStruct_t *hdInfo, mdd_manager *mddManager, mdd_t *reachableStates, mdd_t *fromLowerBound, array_t *mintermVarArray);
71static void HdInduceFullDeadEndIfNecessary(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t **fromLowerBound, mdd_t **fromUpperBound, mdd_t **reachableStates, mdd_t **image, FsmHdStruct_t *hdInfo, int *depth, int shellFlag, array_t *onionRings, array_t *mintermVarArray, int oldSize, double oldMint, int verbosityLevel);
72static mdd_t * ComputeInitialStates(Fsm_Fsm_t *fsm, int shellFlag, boolean printWarning);
73static int CheckStatesContainedInInvariant(mdd_t *reachableStates, array_t *invarStates);
74static void HdComputeReachabilityParameters(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t **reachableStates, mdd_t **fromUpperBound, mdd_t **fromLowerBound, mdd_t **image, FsmHdStruct_t *hdInfo, mdd_t *initialStates, array_t *mintermVarArray, int *depth, int printStep, int shellFlag, array_t *onionRings, int verbosityLevel);
75static int InitializeIncrementalParameters(Fsm_Fsm_t *fsm, Ntk_Network_t *network, array_t **arrayOfRoots, st_table **tableOfLeaves);
76static mdd_t * IncrementalImageCompute(Ntk_Network_t *network, Fsm_Fsm_t *fsm, mdd_manager *mddManager, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet, array_t *arrayOfRoots, st_table *tableOfLeaves, array_t *smoothVarArray, array_t *relationArray, int numLatch);
77static void PrintOnionRings(Fsm_Fsm_t *fsm, int printStep, Fsm_RchType_t approxFlag, int nvars);
78static array_t * GenerateGuidedSearchSequenceArray(array_t *guideArray);
79static void ComputeReachabilityParameters(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, Fsm_RchType_t approxFlag, mdd_t **reachableStates, mdd_t **fromUpperBound, mdd_t **fromLowerBound, mdd_t **image, FsmHdStruct_t *hdInfo, mdd_t *initialStates, array_t *mintermVarArray, int *depth, int printStep, int shellFlag, array_t *onionRings, int verbosityLevel, boolean guidedSearchMode, mdd_t *hint, int *hintDepth, boolean *notConverged);
80
81/**AutomaticEnd***************************************************************/
82
83
84/*---------------------------------------------------------------------------*/
85/* Definition of exported functions                                          */
86/*---------------------------------------------------------------------------*/
87/**Function********************************************************************
88
89  Synopsis [Computes the set of reachable states of an FSM.]
90
91  Description [Computes the set of reachable states of an FSM.  If
92  this set has already been computed, then just returns the result of
93  the previous computation. The recomputation is done anyway if onion
94  rings are required and have not been previously computed. The
95  calling application is responsible for freeing the returned MDD in
96  all cases.  If verbosityLevel is greater than 1, then information is
97  printed after every k steps of reachability, where k is defined by
98  the -s option in the compute_reach command (the default for k is
99  1). If reorderFlag is set, then dynamic reordering is invoked once
100  when the size of the reachable state set reaches the threshold given
101  by reorderThreshold.  This is independent of the
102  dynamic_variable_reordering command. The shell flag indicates that
103  the onion rings of frontier states should be stored. The default
104  does not store the onion rings. The default value for approxFlag is
105  Fsm_Rch_Default_c. See fsm.h for values.
106
107  The procedure offers the following variations of reachability
108  analysis: 1. Exact Reachability analysis by breadth-first search
109  (default). 2. Reachability Analysis (HD) . 3. Reachability Analysis
110  (upper bound by overapproximate FSM traversal). 4 ARDC-accelerated
111  Reachability Analysis.  5. Invariant checking with early termination.
112
113  A lower bound (specified by depthValue) on the reachable states may
114  be obtained by performing a specified number of iterations
115  (depthValue argument). It updates a field in the
116  fsm.reachabilityInfo signalling that the reachable states are an
117  under approximation. The default for the depthValue argument is 0
118  which indicates that reachability analysis computation should
119  proceed to a fixpoint. If a depthValue is specified after the
120  computation of reachable states, the reachable states is returned,
121  else depthValue number of computations are performed. Every non-zero
122  depthValue is interpreted as the number of iterations (image
123  computations) to be performed from the current state (not from the
124  initial state).
125
126  Reachability Analysis (HD) is requested as approxFlag =  Fsm_Rch_Hd_c.
127  HD provides an exact set of reachable states with memory efficiency or
128  a lower bound if reachability analysis does not complete.
129  HD Principles: 1. compute image of small BDDs. 2. compute partial
130  image if necessary 3. When no new states are generated (dead-end),
131  compute new states from image of reached in a decomposed form.  Allow
132  no partial image.  4. When there is a big jump in the size of
133  reached, compute its entire image.  5. store states that will
134  produce no new successors (interior states)
135
136  The algorithm is implemented as follows
137  from = init; reached = init;
138  while (reached != 1 && from != 0) {
139    Allow partial image;
140    image = Image(from);
141    Check if partial image;
142    from = image - reached;
143    if (!partial image) interior_states_candidate = from;
144    if (from == 0 || slow growth of Reached for 5 iterations) {
145      Dead-end computation(greedy): find new states from image of reached;
146    }
147    if (from != 0 and (reached+from) size has a big jump) {
148      Dead-end computation(non-greedy): find the entire image of reached;
149    }
150    if (from != 0) {
151      Compute dense subset of from with at least 1 new state;
152      if subset contains from (i.e., all new states)
153                       interior states += interior states candidate;
154      reached = reached + from/subset;
155    }
156  }
157
158  Legend:  fromLowerBound = from; initialStates = init;
159           reachableStates = reached
160           fromUpperBound = reachableStates (BFS)/fromLowerBound(HD)
161           interiorStates = states with no new successors
162           interiorStateCandidates = states that may be interior
163                  states depending on whether all of them are added to
164                  reachableStates.
165
166  Currently, this does not support the incrementalFlag = 1 option.
167
168  Reachability Analysis (upper bound by overapproximate FSM traversal)
169  gives an upper bound of exact reachable states by overapproximation.
170  It is requested as approxFlag = Fsm_Rch_Oa_c. To do this, first, it
171  groups latch variables by using SSD(State Space Decomposition in the
172  paper Cho et.al, TCAD96-DEC) algorithm, then computes the reachable
173  states of each submachines until convergence, then the product of
174  reachable states of all submachines is an overapproximate reachable
175  states. In this case, depthValue and shellFlag and incrementalFlag
176  are incompatible with this option.
177
178  ARDC-accelerated Reachability Analysis may allow faster and smaller
179  memory usage reachability analysis. First, it computes
180  overapproximated reachable states (if already computed, just use it).
181  Reachability Analysis is then performed (any value of approxFlag is
182  applicable) with a transition relation minimized with the complement
183  of overapproximate reachable states as don't cares (called
184  ARDC). This option is requested as ardc = 1.
185
186  invarStates is a set of invariant states that can be specified. The
187  reachable states must satisfy all invariants. The default value is
188  NULL. Any invalid invariant must also be set to NULL in the
189  invarStaes array. This option is used by the check_invariant
190  command. When an array of invariant states is provided, reachability
191  analysis is done until an invariant is violated or when reachability
192  finishes, whichever is earlier. If an approximation of the reachable
193  states exists, then each invariant is checked for violation. If none
194  are violated, the set of reachable states is returned. It is the
195  caller's resposibility to remove the violating invariant from the
196  invarStates array to continue checking the remaining
197  invariants. The presence of invarStates takes precedence over a
198  non-zero depthValue.
199
200  In general, the reachable states may not be consistent with the
201  onion rings i.e., sum of onion rings is always contained in the
202  reachable states.  When the shell flag is specified and onion rings
203  exist, the initial states are set to the sum of the onion ring
204  states instead of the default initial states of the fsm or
205  previously computed reachable states.
206
207  Some random simulation of the reachable states can be done prior to
208  reachability analysis. This is turned on using the rch_simulate
209  flag. A number should be specifed in the command : set sim_reach
210  <number>, which specifies the number of vectors to be simulated.
211  The initial states are then set to the simulated set of states. If
212  HD is specified, a subset may be taken.
213
214  The recompute flag asks for an explicit recomputation. This means
215  that even reachable states have been computed, they will be
216  recomputed.
217
218  On consecutive calls, recomputation is avoided as much as
219  possible. The specific cases are when
220  Case a. No shell Flag: Recomputation is avoided when reachability is
221  done, when an underapproximation exists and it violates an
222  invariant,  an overapproximation exists and all invariants pass.
223
224  Case b. With shell flag: Recomputation is avoided when onion rings
225  are up-to-date and reachability is done or when onion rings are
226  up-to-date, an underapproximation exists and an invariant fails.
227
228  Update of fsm.reachabiltiyInfo fields are also based on minimum
229  recomputation. The reachability field is updated only if the current
230  set of reachable states are larger than the previous set.
231
232  printWarning flag turns is used to turn on/off the warning message
233  printed when the previously computed reachable states are used to
234  proceed with computation. The default is TRUE.  ]
235
236  SideEffects [The result of the reachable state computation is stored
237  with the FSM. i.e., depth, reachable set, underapprox flag. ]
238
239  SeeAlso [Fsm_FsmComputeInitialStates
240  Fsm_ArdcComputeOverApproximateReachableStates]
241
242******************************************************************************/
243mdd_t *
244Fsm_FsmComputeReachableStates(
245  Fsm_Fsm_t *fsm,
246  int incrementalFlag,
247  int verbosityLevel,
248  int printStep,
249  int depthValue,
250  int shellFlag,
251  int reorderFlag,
252  int reorderThreshold,
253  Fsm_RchType_t approxFlag,
254  int ardc,
255  int recompute,
256  array_t *invarStates,
257  boolean printWarning,
258  array_t *guideArray)
259{
260  /* BFS variables */
261  Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t); /* image info structure*/
262  Img_ImageInfo_t *oldImageInfo = NIL(Img_ImageInfo_t);
263  mdd_t           *reachableStates;/* reachable states */
264  mdd_t           *unreachableStates;
265  mdd_t           *fromLowerBound; /* new states in each iteration */
266  mdd_t           *fromUpperBound; /* set to reachable states */
267  mdd_t           *image, *newImage;/* image computed at each iteration */
268  mdd_t           *initialStates;  /* initial states */
269  mdd_t           *toCareSet;      /* the complement of the reached set */
270  int              depth = 0;      /* depth upto which the computation is
271                                    * performed.
272                                    */
273  graph_t         *partition, *oldPartition;
274  mdd_manager     *mddManager = Fsm_FsmReadMddManager(fsm); /* mdd manager */
275  Ntk_Network_t   *network = fsm->network; /* network */
276  bdd_reorder_type_t currentMethod =
277    Ntk_NetworkReadDynamicVarOrderingMethod(network); /* current reordering
278                                                       * method */
279  int firstTimeFlag = TRUE, firstReorderFlag = FALSE;
280                         /* a flag to indicate the start of the computation */
281  Fsm_RchStatus_t rchStatus = Fsm_Rch_Under_c;
282                         /* under approximation of the reached set computed */
283  int reachableStateSetSize; /* bdd size of the reached set */
284  array_t *mintermVarArray; /* array of present state variables */
285  array_t *onionRings = NIL(array_t);
286                            /* onionringarray for shellFlag computation */
287
288  /* Incremental flag  variables */
289  array_t *arrayOfRoots = NIL(array_t);
290  st_table *tableOfLeaves = NIL(st_table);
291  int numLatch = 0;
292  array_t *relationArray = NIL(array_t), *smoothVarArray = NIL(array_t);
293
294  boolean notConverged = FALSE; /* flag that says that the fixpoint procedure
295                                   did not converge. */
296  /* HD variables */
297  FsmHdStruct_t *hdInfo = NULL;
298  int nvars;       /* number of present state variables */
299
300
301  /* Simulation variables */
302  int simNVec = 0;                 /* number of simulation vectors. */
303  char *simString = Cmd_FlagReadByName("rch_simulate");
304
305  /* Guided Search */
306  array_t *hintDepthArray = NIL(array_t);
307  int hintDepth = -1;
308  mdd_t   *hint = NIL(mdd_t); /* iterates over guide array */
309  int      hintnr;            /* idem                      */
310  boolean guidedSearchMode = FALSE;
311  boolean guideArrayAllocated = FALSE;
312
313  boolean invariantFailed = FALSE;
314
315  /* initializations */
316  /* if fsm is a submachine, takes realPsVars to count minterm correctly. */
317  mintermVarArray = Fsm_FsmReadPresentStateVars(fsm);
318
319  /* compute number of present state variables */
320  nvars = ComputeNumberOfBinaryStateVariables(mddManager, mintermVarArray);
321  assert(nvars > 0);
322
323  /* initializations */
324  if (recompute) {
325    if (incrementalFlag &&
326        ((approxFlag == Fsm_Rch_Hd_c) || (approxFlag == Fsm_Rch_Oa_c))) {
327      fprintf(vis_stdout,
328              "** rch error: Incremental flag and HD computation are not compatible\n");
329      return NIL(mdd_t);
330    }
331    FsmResetReachabilityFields(fsm, approxFlag);
332  } else if ((!shellFlag) || Fsm_FsmTestReachabilityOnionRingsUpToDate(fsm)) {
333    /* If already computed and exact , just return a copy. */
334    reachableStates = Fsm_FsmReadReachableStates(fsm);
335    if (reachableStates != NIL(mdd_t)){
336      if (printWarning) {
337        fprintf(vis_stdout, "** rch info: Reachable states have been previously computed.\n");
338        fprintf(vis_stdout, "** rch info: Not recomputing reachable states.\n");
339        fprintf(vis_stdout, "** rch info: Use compute_reach -F to recompute if necessary.\n");
340      }
341      if (!shellFlag) {
342        if (printWarning) {
343          if (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Bfs_c) {
344            fprintf(vis_stdout, "** rch info: All previous computations done using BFS (-A 0 option).\n");
345          } else {
346            fprintf(vis_stdout, "** rch info: Some previous computations done using BFS/DFS mode (-A 1 or -g option).\n");
347          }
348        }
349        return (mdd_dup(reachableStates));
350      } else if (Fsm_FsmReadReachabilityOnionRings(fsm)) {
351        /* if onion rings exist, since they are up-to-date, return the
352         * reachable states
353         */
354        if (printWarning) {
355          if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Bfs_c) {
356            fprintf(vis_stdout, "** rch info: Onion rings have been computed using BFS (-A 0 option)\n");
357          } else {
358            fprintf(vis_stdout, "** rch info: Some onion rings have been computed using BFS/DFS (-A 1 or -g option)\n");
359          }
360        }
361        if (printStep)
362          PrintOnionRings(fsm, printStep, approxFlag, nvars);
363        return (mdd_dup(reachableStates));
364      }
365    }
366
367    /* if some computed states exist and they violate an invariant,
368       return the current set of reachable states */
369    reachableStates = Fsm_FsmReadCurrentReachableStates(fsm);
370    if (reachableStates != NIL(mdd_t)) {
371      if (!shellFlag) {
372        /* if an underApprox  exists, check invariant, if any */
373        if (invarStates != NIL(array_t)) {
374          if (!CheckStatesContainedInInvariant(reachableStates, invarStates)) {
375            if (printWarning) {
376              fprintf(vis_stdout, "** rch info: Invariant violation using previously computed states\n");
377            }
378            /* return violating reachable states */
379            return (mdd_dup(reachableStates));
380          }
381        }
382      } else if (Fsm_FsmReadReachabilityOnionRings(fsm)) {
383        /* an invariant fails. */
384        if (invarStates != NIL(array_t)) {
385          if (!CheckStatesContainedInInvariant(reachableStates, invarStates)) {
386            if (printWarning) {
387              fprintf(vis_stdout, "** rch info: Invariant violation using previously computed states\n");
388              if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Bfs_c) {
389                fprintf(vis_stdout, "** rch info: Previous onion rings computed in BFS (-A 0 option).\n");
390              } else {
391                fprintf(vis_stdout, "** rch info: Some set of onion rings have been computed using BFS/DFS (-A 1 or -g option)\n");
392              }
393              fprintf(vis_stdout, "** rch info: Use compute_reach -F to recompute if necessary.\n");
394            }
395            if (printStep) {
396              PrintOnionRings(fsm, printStep, approxFlag, nvars);
397            }
398            return (mdd_dup(reachableStates));
399          }
400        }
401      }
402    }
403    /* if an over approx exists, check invariant, if any */
404    if ((invarStates != NIL(array_t)) && (!shellFlag) && (!depthValue) &&
405        (Fsm_FsmReadOverApproximateReachableStates(fsm)
406         != NIL(array_t))) {
407      if (FsmArdcCheckInvariant(fsm, invarStates)) {
408        fprintf(vis_stdout, "** rch info: Over approximation exists, using over approximation for invariant checking.\n");
409         return(Fsm_ArdcGetMddOfOverApproximateReachableStates(fsm));
410      }
411    }
412
413    if (incrementalFlag &&
414        ((approxFlag == Fsm_Rch_Hd_c) || (approxFlag == Fsm_Rch_Oa_c))) {
415      fprintf(vis_stdout,
416              "** rch error: Incremental flag and HD computation are not compatible\n");
417
418      return NIL(mdd_t);
419    }
420  }
421  /* onion rings make no sense with Over approx */
422  if (shellFlag && (approxFlag == Fsm_Rch_Oa_c)) {
423    fprintf(vis_stdout, "** rch error: Can't generate onion rings with over approx\n");
424    return NIL(mdd_t);
425  }
426
427  /* depth value makes no sense with over approximation */
428  if (depthValue && (approxFlag == Fsm_Rch_Oa_c)) {
429    fprintf(vis_stdout, "** rch error: Can't generate over approx with depth Value\n");
430    return NIL(mdd_t);
431  }
432
433  /* guided search cannot be done with Over approximation */
434  if ((guideArray != NIL(array_t)) && (approxFlag == Fsm_Rch_Oa_c)) {
435    fprintf(vis_stdout, "Guided search is not implemented with Over approximations\n");
436    return NIL(mdd_t);
437  }
438
439  /* initializations */
440  reachableStateSetSize = 0;
441  if ((approxFlag == Fsm_Rch_Hd_c) || (guideArray != NIL(array_t))) {
442    /* this structure is needed for HD and guidedSearch */
443    hdInfo = FsmHdStructAlloc(nvars);
444  }
445
446  simNVec = 0;
447  if (simString != NIL(char)) {
448    simNVec = strtol(simString, NULL, 10);
449    if (simNVec <= 0)  simNVec = 0;
450  }
451  /* initialize onion ring array */
452  if (shellFlag) {
453    if (Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t)) {
454      onionRings = array_alloc(mdd_t *, 0);
455    } else {
456      onionRings = Fsm_FsmReadReachabilityOnionRings(fsm);
457    }
458  }
459
460  /* Computes ARDCs, and  overapproximation by SSD traversal, if required. */
461  if (approxFlag == Fsm_Rch_Oa_c || ardc) {
462    long initialTime = 0;
463    long finalTime;
464
465    assert(!incrementalFlag);
466
467    if (verbosityLevel > 0)
468      initialTime = util_cpu_time();
469
470    (void)Fsm_FsmComputeOverApproximateReachableStates(fsm, incrementalFlag,
471        verbosityLevel, printStep, depthValue, shellFlag, reorderFlag,
472        reorderThreshold, recompute);
473
474    if (approxFlag == Fsm_Rch_Oa_c) {
475      if (hdInfo != NIL(FsmHdStruct_t)) FsmHdStructFree(hdInfo);
476      return(Fsm_ArdcGetMddOfOverApproximateReachableStates(fsm));
477    }
478
479    if (verbosityLevel > 0) {
480      finalTime = util_cpu_time();
481      Fsm_ArdcPrintReachabilityResults(fsm, finalTime-initialTime);
482    }
483  }
484
485  if(Cmd_FlagReadByName("linear_compute_range")) {
486    partition = Part_NetworkCreatePartition(network, 0, "temp", (lsList)0,
487        (lsList)0, NIL(mdd_t), Part_Fine_c, 0, 0, 0, 0);
488    oldPartition = fsm->partition;
489    oldImageInfo = fsm->imageInfo;
490    fsm->imageInfo = 0;
491    imageInfo = Fsm_FsmReadOrCreateImageInfoForComputingRange(fsm, 0, 1);
492    unreachableStates = Img_ImageGetUnreachableStates(imageInfo);
493    fprintf(vis_stdout, "%-20s%10g\n", "reachable states =",
494                     mdd_count_onset(mddManager, unreachableStates,
495                                     fsm->fsmData.presentStateVars));
496    fflush(vis_stdout);
497    /* get unreachable states */
498    Img_ImageInfoFree(imageInfo);
499    fsm->imageInfo = oldImageInfo;
500    fsm->partition = oldPartition;
501    Part_PartitionFree(partition);
502    exit(0);
503  }
504  /* Compute the set of initial states. Start with the
505   * underapproximation of Reached states if it exists or sum of
506   * onion rings if shell flag is specified or the initial states of
507   * the fsm.
508   */
509  initialStates = ComputeInitialStates(fsm, shellFlag, printWarning);
510  if (initialStates == NIL(mdd_t)) {
511    fprintf(vis_stdout, "** rch error: No initial states computed.");
512    fprintf(vis_stdout, " No reachability will be performed.\n");
513    if (hdInfo != NIL(FsmHdStruct_t)) FsmHdStructFree(hdInfo);
514    return NIL(mdd_t);
515  }
516
517  if (incrementalFlag){
518    /* Note: if incrementalflag is set, no imageinfo is created! */
519    numLatch = InitializeIncrementalParameters(fsm, network, &arrayOfRoots,
520                                               &tableOfLeaves);
521    smoothVarArray = array_join(fsm->fsmData.presentStateVars,
522                                fsm->fsmData.inputVars);
523    relationArray = array_alloc(mdd_t *, numLatch+1);
524  } else {
525    /* Create an imageInfo for image computations, if not already created. */
526    imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, 0, 1);
527    if (ardc) {
528      Fsm_ArdcMinimizeTransitionRelation(fsm, Img_Forward_c);
529    }
530  }
531
532  /* Get approximate traversal options */
533  if ((!incrementalFlag) && (approxFlag == Fsm_Rch_Hd_c)) {
534    /* only partial image allowed. No approximation of frontier set */
535    hdInfo->onlyPartialImage =  Fsm_FsmHdOptionReadOnlyPartialImage(hdInfo->options);
536    /* states which can produce no new successors. */
537    hdInfo->interiorStates = bdd_zero(mddManager);
538  }
539
540  /* pertaining to simulation */
541  if (simNVec > 0) {
542    RandomSimulation(simNVec, fsm, approxFlag, initialStates,
543                     &reachableStates, &fromLowerBound, hdInfo);
544  } else {
545    /* start reached set with initial states */
546    reachableStates = mdd_dup(initialStates);
547    fromLowerBound = mdd_dup(reachableStates);
548  }
549
550  /* initialize variables to print */
551  if ((!incrementalFlag) && (approxFlag == Fsm_Rch_Hd_c)) {
552
553    FsmHdStatsComputeSizeAndMinterms(mddManager, reachableStates,
554                           mintermVarArray, nvars,
555                           Fsm_Hd_Reached, hdInfo->stats);
556    FsmHdStatsComputeSizeAndMinterms(mddManager, fromLowerBound,
557                           mintermVarArray, nvars,
558                           Fsm_Hd_From, hdInfo->stats);
559    FsmHdStatsSetMintermFromSubset(hdInfo->stats, FsmHdStatsReadMintermFrom(hdInfo->stats));
560    FsmHdStatsSetSizeFromSubset(hdInfo->stats, FsmHdStatsReadSizeFrom(hdInfo->stats));
561  }
562
563  if (printStep && ((depth % printStep) == 0) && (approxFlag == Fsm_Rch_Hd_c)){
564    fprintf(vis_stdout, "\nIndex: R = Reached; I = Image, F = Frontier, FA = Approximation of Frontier\n");
565    fprintf(vis_stdout, "       f = Minterms in f; |f| = Bdd nodes in f\n\n");
566  }
567  /* initialize for the first iteration */
568   fromUpperBound = reachableStates;
569
570  /* hint array */
571  if (guideArray == NIL(array_t)) {
572    guideArray = array_alloc(mdd_t *, 0);
573    guideArrayAllocated = TRUE;
574  }
575  /* pad with 1 when no hints are provided */
576  if (array_n(guideArray) == 0) {
577    array_insert_last(mdd_t *, guideArray, bdd_one(mddManager));
578  }
579  /* depth sequence for hints. 1-to-1 correspondence with guidearray */
580  /* -1 implies apply hint to convergence. */
581  hintDepthArray = GenerateGuidedSearchSequenceArray(guideArray);
582
583  assert(array_n(hintDepthArray) == array_n(guideArray));
584
585  if (array_n(guideArray) == 0) hint = mdd_one(mddManager);
586
587  arrayForEachItem(mdd_t *, guideArray, hintnr, hint){
588
589    /* check the depth for which this hint is to be applied. */
590    hintDepth = array_fetch(int, hintDepthArray, hintnr);
591
592    if(hintnr == 0 && mdd_is_tautology(hint, 1) && array_n(guideArray) == 1){
593      assert(hintDepth == -1);
594    }  else {
595      assert(!incrementalFlag);
596      guidedSearchMode  = TRUE;
597      Fsm_InstantiateHint(fsm, hint, 1, 0, Ctlp_Underapprox_c,
598                          verbosityLevel > 1);
599      if (hintnr < (array_n(guideArray)-1))
600        fprintf(vis_stdout, "**GS info: Instantiating  hint number %d\n", hintnr+1);
601      else
602        fprintf(vis_stdout, "**GS info: Restoring original transition relation\n");
603
604      if (approxFlag == Fsm_Rch_Hd_c) {
605        /* clean up all the invalid state information */
606        if (hdInfo->interiorStates != NIL(mdd_t))
607          mdd_free(hdInfo->interiorStates);
608        hdInfo->interiorStates = NIL(mdd_t); /* for every new hint, this is invalid. */
609        if (hdInfo->interiorStateCandidate != NIL(mdd_t))
610          mdd_free(hdInfo->interiorStateCandidate);
611        hdInfo->interiorStateCandidate = NIL(mdd_t); /* for every new hint, this is invalid */
612        hdInfo->imageOfReachedComputed = FALSE; /* since it doesn't matter for every new hint */
613        if (hdInfo->deadEndResidue != NIL(mdd_t))
614          mdd_free(hdInfo->deadEndResidue);
615        hdInfo->deadEndResidue = NIL(mdd_t);
616      }
617      /* generate a frontier by doing a dead-end computation if the
618         frontier is empty. This is non-greedy for BFS and greedy for
619         HD. */
620      if (mdd_is_tautology(fromLowerBound, 0)) {
621        ComputeReachabilityParameters(mddManager, imageInfo, approxFlag,
622                                      &reachableStates, &fromUpperBound,
623                                      &fromLowerBound, &image, hdInfo,
624                                      initialStates,
625                                      mintermVarArray,
626                                      &depth, printStep,
627                                      shellFlag, onionRings,
628                                      verbosityLevel,
629                                      guidedSearchMode, hint, &hintDepth,
630                                      &notConverged);
631      }
632    }
633    /* initialize */
634    notConverged = FALSE;
635    if (!incrementalFlag)
636      Img_ImageInfoResetUseOptimizedRelationFlag(imageInfo);
637    /* Main loop of reachability computation. */
638    /* Iterate until fromLowerBound is empty or all states are reached. */
639    while (!mdd_is_tautology(fromLowerBound, 0)) {
640      if(depth > 0 && !incrementalFlag)
641        Img_ImageInfoSetUseOptimizedRelationFlag(imageInfo);
642      /* fromLowerBound is the "onion shell" of states just reached. */
643      if ((shellFlag && (approxFlag != Fsm_Rch_Hd_c) &&
644          (!firstTimeFlag ||
645           (Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t)))) ||
646          (shellFlag && (approxFlag == Fsm_Rch_Hd_c) &&
647          (Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t)) &&
648          firstTimeFlag)) {
649        array_insert_last(mdd_t*, onionRings, mdd_dup(fromLowerBound));
650      }
651
652      /* if it is the print step, print out the iteration and the */
653      if (printStep && ((depth % printStep) == 0)) {
654        int step;
655        /* for BFS, preserve earlier format of printing */
656        step = (shellFlag) ? array_n(onionRings) : Fsm_FsmGetReachableDepth(fsm)+depth;
657        PrintStatsPerIteration(approxFlag,
658                               nvars,
659                               step,
660                               hdInfo,
661                               mddManager,
662                               reachableStates,
663                               fromLowerBound,
664                               mintermVarArray);
665      }
666
667      /* Check if invariant contains the new states.  In case of HD
668       * computation, check the containment of the entire reached set.
669       */
670      if (invarStates != NIL(array_t)) {
671        mdd_t *temp;
672        temp = (approxFlag == Fsm_Rch_Hd_c) ? reachableStates : fromLowerBound;
673        if (!CheckStatesContainedInInvariant(temp, invarStates)) {
674          notConverged = TRUE;
675          invariantFailed = TRUE; /* flag used for early termination */
676          break;
677        }
678      }
679
680      if (mdd_is_tautology(reachableStates, 1)) {
681        break;
682      }
683
684      if ((depthValue && (depth == depthValue)) ||
685          /* limited depth hint is implemented this way */
686          (hintDepth == 0)) {
687        /* No more steps */
688        notConverged = TRUE;
689        break;
690      }
691
692      if (reorderFlag && !firstReorderFlag &&
693          (reachableStateSetSize >= reorderThreshold )){
694        firstReorderFlag = TRUE;
695        (void) fprintf(vis_stdout, "Dynamic variable ordering forced ");
696        (void) fprintf(vis_stdout, "with method sift\n");
697        Ntk_NetworkSetDynamicVarOrderingMethod(network,
698                                               BDD_REORDER_SIFT,
699                                               BDD_REORDER_VERBOSITY_DEFAULT);
700        bdd_reorder(Ntk_NetworkReadMddManager(network));
701        Ntk_NetworkSetDynamicVarOrderingMethod(network, currentMethod,
702                                               BDD_REORDER_VERBOSITY_DEFAULT);
703      }
704
705      firstTimeFlag = FALSE;
706      /* careSet for image computation is the set of all states not reached
707       * so far.
708       */
709      toCareSet = mdd_not(reachableStates);
710
711      /*
712       * Image of some set between lower and upper, where we care
713       * about the image only on unreached states.
714       */
715      if (incrementalFlag){
716        image = IncrementalImageCompute(network, fsm, mddManager,
717                                        fromLowerBound,
718                                        fromUpperBound, toCareSet,
719                                        arrayOfRoots, tableOfLeaves,
720                                        smoothVarArray, relationArray,
721                                        numLatch);
722      } else{
723        assert(!incrementalFlag);
724
725        if (approxFlag == Fsm_Rch_Hd_c) {
726          /* allow partial image computation */
727          Img_ImageAllowPartialImage(imageInfo, TRUE);
728        }
729
730        /* compute the image of this iteration */
731        image = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
732                                                      fromLowerBound,
733                                                      fromUpperBound,
734                                                      toCareSet);
735
736
737
738        /* record if partial image or not */
739        if (approxFlag == Fsm_Rch_Hd_c) {
740          /* Check if partial image computation, disallow partial image
741           * computation.
742           */
743          hdInfo->partialImage = Img_ImageWasPartial(imageInfo);
744          /* record this to prevent dead-end computation. */
745          hdInfo->imageOfReachedComputed = (!hdInfo->partialImage) &&
746            mdd_equal(reachableStates, fromLowerBound);
747          /* potential candidates for interior states (only if not a
748           * partial image)
749           */
750          if (!hdInfo->partialImage) hdInfo->interiorStateCandidate = mdd_dup(fromLowerBound);
751        }
752      }
753
754      /* free the used bdds */
755      mdd_free(toCareSet);
756
757      /* New lower bound is the states just reached. */
758      mdd_free(fromLowerBound);
759      fromLowerBound = mdd_and(image, reachableStates, 1, 0);
760      depth++;
761      hintDepth--;
762
763
764      if ((!incrementalFlag) && (approxFlag == Fsm_Rch_Hd_c)) {
765        FsmHdStatsComputeSizeAndMinterms(mddManager, image,
766                                         mintermVarArray, nvars,
767                                         Fsm_Hd_To, hdInfo->stats);
768      }
769
770      /* need image only if HD and not dead-end */
771      if (approxFlag != Fsm_Rch_Hd_c) {
772          mdd_free(image);
773          image = NULL;
774      } else {
775        if (hdInfo->imageOfReachedComputed ||   hdInfo->onlyPartialImage ||
776          (hdInfo->slowGrowth >= FSM_HD_NUM_SLOW_GROWTHS) ||
777          mdd_is_tautology(fromLowerBound, 0)) {
778          mdd_free(image);
779          image = NULL;
780        }
781      }
782
783      /* computes reachable states, fromlowerBound and fromupperbound
784       * for BFS.  For HD it computes the above as well as interior
785       * statess, dead-end residue, etc. All the other parameteres are
786       * updated. For guided search, this call does not perform a
787       * non-greedy dead-end computation, even if the frontier is 0. */
788       ComputeReachabilityParameters(mddManager, imageInfo, approxFlag,
789                                    &reachableStates,
790                                    &fromUpperBound,
791                                    &fromLowerBound,
792                                    &image,
793                                     hdInfo,
794                                    initialStates,
795                                    mintermVarArray,
796                                     &depth,  printStep,
797                                     shellFlag, onionRings,
798                                    verbosityLevel, FALSE, hint,
799                                    &hintDepth,
800                                    &notConverged);
801
802
803       if (mdd_is_tautology(fromLowerBound, 0) &&
804           (approxFlag == Fsm_Rch_Bfs_c) &&
805           (!guidedSearchMode) && (!depthValue))
806         depth--;
807
808    } /* end of main while loop (while frontier != 0) */
809
810    /* stop iterating over hint if invariants are violated or all
811       states are reachable or limited depth value has been
812       reached. */
813    if (invariantFailed) break;
814    if (mdd_is_tautology(reachableStates, 1)) {
815      break;
816    }
817    if (depthValue && (depth == depthValue)) {
818      /* No more steps */
819      break;
820    }
821
822  }/* for each hint */
823
824
825  if(!incrementalFlag &&
826     Img_ImageInfoObtainMethodType(imageInfo) == Img_Linear_c &&
827     Img_ImageInfoObtainOptimizeType(imageInfo) == Opt_NS &&
828     Img_IsTransitionRelationOptimized(imageInfo)) {
829    Img_ImageInfoResetUseOptimizedRelationFlag(imageInfo);
830    fprintf(vis_stdout, "%-20s%10g\n", "reachable states =",
831                 mdd_count_onset(mddManager, reachableStates,
832                                 fsm->fsmData.presentStateVars));
833    fromLowerBound = mdd_dup(reachableStates);
834    fromUpperBound = reachableStates;
835    while (1) {
836      toCareSet = mdd_dup(reachableStates);
837      image = Img_ImageInfoComputeFwdWithDomainVars(imageInfo,
838                                                  fromLowerBound,
839                                                  fromUpperBound,
840                                                  toCareSet);
841      newImage = bdd_or(image, initialStates, 1, 1);
842      bdd_free(image);
843      image = newImage;
844      if(mdd_equal(fromLowerBound, image)) {
845        mdd_free(toCareSet);
846        mdd_free(fromLowerBound);
847        mdd_free(reachableStates);
848        fromLowerBound = image;
849        reachableStates = mdd_dup(fromLowerBound);
850        fromUpperBound = reachableStates;
851        fprintf(vis_stdout, "%-20s%10g\n", "reachable states =",
852                 mdd_count_onset(mddManager, reachableStates,
853                                 fsm->fsmData.presentStateVars));
854        break;
855      }
856      mdd_free(toCareSet);
857      mdd_free(fromLowerBound);
858      mdd_free(reachableStates);
859      fromLowerBound = image;
860      reachableStates = mdd_dup(fromLowerBound);
861      fromUpperBound = reachableStates;
862
863      fprintf(vis_stdout, "%-20s%10g\n", "reachable states =",
864                 mdd_count_onset(mddManager, reachableStates,
865                                 fsm->fsmData.presentStateVars));
866    }
867  }
868
869
870  /* clean up for Guided search mainly, only if needed */
871  /* we rely on the fact that the variable hint is set to the last hint from
872   * the previous loop.
873   */
874  if (guidedSearchMode && !mdd_is_tautology(hint, 1))
875    Fsm_CleanUpHints(fsm, 1, 0, printStep);
876  array_free(hintDepthArray);
877
878  /* If (1) all states are reachable, or (2) not limited depth computation
879     and not a converge with a hint, or (3) limited depth and not
880     guided search mode and BFS and frontier = 0, or (4) in guided
881     search, if limited depth and frontier = 0 then one full dead-end
882     should have occured */
883  if(mdd_is_tautology(reachableStates, 1) ||
884     ((notConverged == FALSE) && mdd_is_tautology(hint, 1)) ||
885     (!guidedSearchMode && (notConverged == TRUE) &&
886      mdd_is_tautology(fromLowerBound, 0) && (approxFlag == Fsm_Rch_Bfs_c)) ||
887     (guidedSearchMode && hdInfo->deadEndWithOriginalTR &&
888      mdd_is_tautology(fromLowerBound, 0) && (approxFlag == Fsm_Rch_Bfs_c))) {
889
890    rchStatus = Fsm_Rch_Exact_c;
891    if (mdd_is_tautology(reachableStates, 1) &&
892        !mdd_is_tautology(fromLowerBound, 0) &&
893        printStep && ((depth % printStep) == 0) ) {
894      int step;
895      /* for BFS, preserve earlier format of printing */
896      step = (shellFlag) ?
897        array_n(onionRings) :
898        Fsm_FsmGetReachableDepth(fsm)+depth;
899      PrintStatsPerIteration(approxFlag, nvars, step, hdInfo,
900                             mddManager, reachableStates,
901                             fromLowerBound, mintermVarArray);
902    }
903  }
904
905  /* clean up the hints if allocated here */
906  if (guideArrayAllocated) mdd_array_free(guideArray);
907
908  if (hdInfo != NIL(FsmHdStruct_t)) {
909    FsmHdStructFree(hdInfo);
910  }
911
912  mdd_free(fromLowerBound);
913  mdd_free(initialStates);
914
915  /* Update FSM reahcability fields */
916
917  /* indicate whether the shells are consistent with the reachable states */
918  if (!shellFlag) {
919    /* if any states were added from a previous computation, shells
920       are not up-to-date */
921    if (Fsm_FsmReadCurrentReachableStates(fsm) != NIL(mdd_t)) {
922      if (!mdd_lequal(reachableStates, Fsm_FsmReadCurrentReachableStates(fsm), 1, 1)) {
923        FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE);
924      } /* otherwise the previous iteration was computed with onion
925      rings, in which case it is still up-to-date or the previous
926      iteration was computed without onion rings and it was set to not
927      up-to-date in the previous iteration */
928    } else {
929      assert(Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t));
930      /* not up-to-date because no onion rings */
931      FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE);
932    }
933
934  } else {
935    /* shells are up to date only if current set adds upto previously
936       computed states or more */
937    if (Fsm_FsmReadCurrentReachableStates(fsm)) {
938      if (!mdd_lequal(Fsm_FsmReadCurrentReachableStates(fsm),
939                    reachableStates, 1, 1)) {
940        FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE);
941      } else {
942        FsmSetReachabilityOnionRingsUpToDateFlag(fsm, TRUE);
943      }
944
945    } else FsmSetReachabilityOnionRingsUpToDateFlag(fsm, TRUE);
946
947    /* Onion rings are not BFS, i.e., HD or Guided search. */
948    if ((approxFlag == Fsm_Rch_Hd_c) ||
949        (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Hd_c) ||
950        guidedSearchMode)
951      FsmSetReachabilityOnionRingsMode(fsm, Fsm_Rch_Hd_c);
952
953    if (array_n(onionRings) == 0) {
954      array_free(onionRings);
955      onionRings = NIL(array_t);
956    }
957    FsmSetReachabilityOnionRings(fsm, onionRings);
958  }
959
960  /* update fsm structure */
961  /* record depth of traversal, depth is consistent with reachable
962     states, hence may not be consistent with the onion rings */
963  /* replace reachable states if only more states have been computed now */
964  if (Fsm_FsmReadCurrentReachableStates(fsm) != NIL(mdd_t)) {
965    if (!mdd_lequal(reachableStates, Fsm_FsmReadCurrentReachableStates(fsm), 1, 1)) {
966      Fsm_FsmFreeReachableStates(fsm);
967      fsm->reachabilityInfo.reachableStates = mdd_dup(reachableStates);
968      if (!shellFlag) fsm->reachabilityInfo.depth = Fsm_FsmGetReachableDepth(fsm) + depth;
969      else if (Fsm_FsmReadReachabilityOnionRings(fsm))
970        fsm->reachabilityInfo.depth = array_n(Fsm_FsmReadReachabilityOnionRings(fsm));
971      /* set computation mode as HD if HD or Guided search, basically to indicate not BFS */
972      if ((approxFlag == Fsm_Rch_Hd_c) ||
973          (FsmReadReachabilityComputationMode(fsm)  == Fsm_Rch_Hd_c) ||
974          guidedSearchMode) {
975        FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Hd_c);
976      }
977    }
978  } else {
979    fsm->reachabilityInfo.reachableStates = mdd_dup(reachableStates);
980    if (!shellFlag) fsm->reachabilityInfo.depth = depth;
981    else if (Fsm_FsmReadReachabilityOnionRings(fsm))
982      fsm->reachabilityInfo.depth = array_n(Fsm_FsmReadReachabilityOnionRings(fsm));
983    /* set computation mode as HD if HD or Guided search, basically to indicate not BFS */
984      if ((approxFlag == Fsm_Rch_Hd_c) || guidedSearchMode) {
985        FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Hd_c);
986      } else {
987        FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Bfs_c);
988      }
989
990  }
991  /* indicate whether reachability analysis is completed or not */
992  FsmSetReachabilityApproxComputationStatus(fsm, rchStatus);
993
994  if (incrementalFlag){
995    array_free(relationArray);
996    array_free(arrayOfRoots);
997    st_free_table(tableOfLeaves);
998    array_free(smoothVarArray);
999    /* Need to put in next state function data for the partition */
1000  }
1001
1002  return reachableStates;
1003} /* end of Fsm_FsmComputeReachableStates */
1004
1005
1006
1007/**Function********************************************************************
1008
1009  Synopsis [Existentially quantifies variables from an implicit product.]
1010
1011  Description [Existentially quantifies the smoothing variables from the
1012  product of the MDDs in mddArray, and returns the result. SmoothingVars is an
1013  array of MDD ids. For now, uses the simplistic approach of conjunction all
1014  the MDDs, and then quantifying the smoothing variables.]
1015
1016  SideEffects []
1017
1018******************************************************************************/
1019mdd_t *
1020Fsm_MddMultiwayAndSmooth(mdd_manager *mddManager, array_t *mddArray,
1021                         array_t *smoothingVars)
1022{
1023  int i;
1024  mdd_t *resultMdd;
1025  mdd_t *product = mdd_one(mddManager);
1026
1027  for (i = 0; i<array_n(mddArray); i++){
1028    mdd_t *mdd         = array_fetch(mdd_t*, mddArray, i);
1029    mdd_t *tempProduct = mdd_and(product, mdd, 1, 1);
1030    mdd_free(product);
1031    product = tempProduct;
1032  }
1033
1034  if (array_n(smoothingVars) == 0) {
1035    resultMdd = mdd_dup(product);
1036  }
1037  else{
1038    resultMdd =  mdd_smooth(mddManager, product, smoothingVars);
1039  }
1040
1041  mdd_free(product);
1042  return resultMdd;
1043}
1044
1045/**Function********************************************************************
1046
1047  Synopsis    [Prints the results of reachability analysis.]
1048
1049  Description    [Prints the results of reachability analysis.]
1050
1051  SideEffects []
1052
1053  SeeAlso     []
1054
1055******************************************************************************/
1056void
1057Fsm_FsmReachabilityPrintResults(
1058  Fsm_Fsm_t *fsm,
1059  long elapseTime,
1060  int approxFlag)
1061{
1062  mdd_manager   *mddManager = Fsm_FsmReadMddManager(fsm);
1063  mdd_t         *reachableStates = fsm->reachabilityInfo.reachableStates;
1064  array_t       *psVarsArray;
1065  int           nvars;
1066
1067  if (!reachableStates)
1068    return;
1069
1070  psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
1071  /* compute number of present state variables */
1072  nvars = ComputeNumberOfBinaryStateVariables(mddManager, psVarsArray);
1073
1074  (void) fprintf(vis_stdout,"********************************\n");
1075  (void) fprintf(vis_stdout,"Reachability analysis results:\n");
1076  if ((FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Bfs_c) &&
1077      (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t))) {
1078    (void) fprintf(vis_stdout, "%-20s%10d\n", "FSM depth =",
1079                   fsm->reachabilityInfo.depth);
1080  } else {
1081    (void) fprintf(vis_stdout, "%-20s%10d\n", "computation depth =",
1082                   fsm->reachabilityInfo.depth);
1083  }
1084  if (nvars <= 1023) {
1085    (void) fprintf(vis_stdout, "%-20s%10g\n", "reachable states =",
1086                   mdd_count_onset(mddManager, reachableStates,
1087                                   fsm->fsmData.presentStateVars));
1088  } else {
1089    /*
1090    (void) fprintf(vis_stdout, "%-20s", "reachable states = ");
1091    bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6);
1092    */
1093    EpDouble    epd;
1094    char        strValue[20];
1095
1096    mdd_epd_count_onset(mddManager, reachableStates,
1097                        fsm->fsmData.presentStateVars, &epd);
1098    EpdGetString(&epd, strValue);
1099    (void) fprintf(vis_stdout, "%-20s%10s\n", "reachable states =", strValue);
1100  }
1101  (void) fprintf(vis_stdout, "%-20s%10d\n", "BDD size =",
1102                 mdd_size(reachableStates));
1103  (void) fprintf(vis_stdout, "%-20s%10g\n", "analysis time =",
1104                 (double)elapseTime/1000.0);
1105  if (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t)) {
1106    (void) fprintf(vis_stdout, "%-20s%10s\n", "reachability analysis = ", "complete");
1107  } else {
1108    (void) fprintf(vis_stdout, "%-20s%10s\n", "reachability analysis = ", "incomplete");
1109  }
1110}
1111
1112
1113/*---------------------------------------------------------------------------*/
1114/* Definition of static functions                                          */
1115/*---------------------------------------------------------------------------*/
1116
1117/**Function********************************************************************
1118
1119  Synopsis    [Checks the validity of image]
1120
1121  Description [In a properly formed image, there should not be any
1122  domain or quantify variables in its support. This function checks
1123  for that fact.]
1124
1125  SideEffects []
1126
1127******************************************************************************/
1128static int
1129CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t
1130                   *domainVarMddIdArray, array_t *quantifyVarMddIdArray)
1131{
1132  int i;
1133  array_t *imageSupportArray = mdd_get_support(mddManager, image);
1134  st_table *imageSupportTable = st_init_table(st_numcmp, st_numhash);
1135  for (i=0; i<array_n(imageSupportArray); i++){
1136    int mddId = array_fetch(int, imageSupportArray, i);
1137    (void) st_insert(imageSupportTable, (char *) (long) mddId, NIL(char));
1138  }
1139  for (i=0; i<array_n(domainVarMddIdArray); i++){
1140    int domainVarId;
1141    domainVarId = array_fetch(int, domainVarMddIdArray, i);
1142    assert(st_is_member(imageSupportTable, (char *)(long)domainVarId) == 0);
1143  }
1144  for (i=0; i<array_n(quantifyVarMddIdArray); i++){
1145    int quantifyVarId;
1146    quantifyVarId = array_fetch(int, quantifyVarMddIdArray, i);
1147    assert(st_is_member(imageSupportTable, (char *)(long)quantifyVarId) == 0);
1148  }
1149  st_free_table(imageSupportTable);
1150  array_free(imageSupportArray);
1151  return 1;
1152}
1153
1154/**Function********************************************************************
1155
1156  Synopsis    [Counts the number of Bdd variables for the given Mdd id array].
1157
1158  Description [Counts the number of Bdd variables for the given Mdd id array]
1159
1160
1161  SideEffects []
1162
1163******************************************************************************/
[15]1164/*static*/ int
[14]1165ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager,
1166                               array_t *mddIdArray)
1167{
1168  int mddId, i;
1169  mvar_type mddVar;
1170  int numEncodingBits, count = 0;
1171  array_t *mvar_list = mdd_ret_mvar_list(mddManager);
1172
1173  arrayForEachItem(int, mddIdArray, i, mddId) {
1174    mddVar = array_fetch(mvar_type, mvar_list, mddId);
1175    numEncodingBits = mddVar.encode_length;
1176    count += numEncodingBits;
1177  }
1178  return count;
1179} /* end of ComputeNumberOfBinaryStateVariables */
1180
1181
1182/**Function********************************************************************
1183
1184  Synopsis    [Add states.]
1185
1186  Description [Add States.]
1187
1188  SideEffects [ Free the original parts]
1189
1190******************************************************************************/
1191static mdd_t *
1192AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB)
1193{
1194  mdd_t *result;
1195  if ((a != NULL) && (b != NULL)) {
1196    result = mdd_or(a, b, 1, 1);
1197  } else if ((a == NULL) && (b == NULL)) {
1198    result = a;
1199  } else if (a == NULL) {
1200    result = mdd_dup(b);
1201  } else {
1202    result =  mdd_dup(a);
1203  }
1204  if ((freeA == FSM_MDD_FREE) && (a != NULL)) mdd_free(a);
1205  if ((freeB == FSM_MDD_FREE) && (b != NULL)) mdd_free(b);
1206  return result;
1207} /* end of AddStates */
1208
1209
1210/**Function********************************************************************
1211
1212  Synopsis    [Simulates randomly specified number of states.]
1213
1214  Description [Simulates randomly specified number of states.]
1215
1216  SideEffects []
1217
1218******************************************************************************/
1219static void
1220RandomSimulation(int simNVec,
1221                 Fsm_Fsm_t *fsm,
1222                 Fsm_RchType_t approxFlag,
1223                 mdd_t *initialStates,
1224                 mdd_t **reachableStates,
1225                 mdd_t **fromLowerBound,
1226                 FsmHdStruct_t *hdInfo)
1227{
1228  Ntk_Network_t   *network = fsm->network;
1229
1230  /* Compute specified number of simulated states. */
1231  *reachableStates = Sim_RandomSimulate(network, simNVec, 0);
1232  *reachableStates = AddStates(*reachableStates, initialStates, FSM_MDD_FREE, FSM_MDD_DONT_FREE);
1233  *fromLowerBound = mdd_dup(*reachableStates);
1234
1235  if (approxFlag == Fsm_Rch_Hd_c) {
1236    if (mdd_size(*fromLowerBound) >
1237        Fsm_FsmHdOptionReadFrontierApproxThreshold(hdInfo->options)) {
1238      /* Reset frontier if too large. */
1239      mdd_free(*fromLowerBound);
1240      *fromLowerBound = bdd_between(initialStates, *reachableStates);
1241      if (!mdd_equal(*fromLowerBound, *reachableStates)) {
1242        hdInfo->firstSubset = FALSE;
1243        hdInfo->deadEndResidue = mdd_and(*reachableStates,
1244                                         *fromLowerBound, 1, 0);
1245      }
1246    }
1247  }
1248  return;
1249} /* end of RandomSimulation */
1250
1251
1252/**Function********************************************************************
1253
1254  Synopsis    [Prints stats per iteration]
1255
1256  Description [Prints stats per iteration]
1257
1258  SideEffects []
1259
1260******************************************************************************/
1261static void
1262PrintStatsPerIteration(Fsm_RchType_t approxFlag,
1263                       int nvars,
1264                       int depth,
1265                       FsmHdStruct_t *hdInfo,
1266                       mdd_manager *mddManager,
1267                       mdd_t *reachableStates,
1268                       mdd_t *fromLowerBound,
1269                       array_t *mintermVarArray)
1270{
1271  if (approxFlag != Fsm_Rch_Hd_c) {
1272    int reachableStateSetSize = mdd_size(reachableStates);
1273    if (nvars <= 1023) {
1274      (void)fprintf(vis_stdout, "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n",
1275                    depth, mdd_count_onset(mddManager, reachableStates,
1276                                           mintermVarArray),
1277                    (long)reachableStateSetSize);
1278      /*                            bdd_print_minterm(reachableStates); */
1279    } else {
1280      (void)fprintf(vis_stdout, "BFS step = %d\tBdd size = %8d\t|states| = ",
1281                    depth, reachableStateSetSize);
1282      (void) bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6);
1283    }
1284
1285  } else { /* HD */
1286
1287    if (nvars <= 1023) {
1288      (void)fprintf(vis_stdout, "Step = %d, R = %8g, |R| = %8d,  I = %8g,  |I| = %8d\n",
1289                    depth,  FsmHdStatsReadMintermReached(hdInfo->stats),
1290                    FsmHdStatsReadSizeReached(hdInfo->stats), FsmHdStatsReadMintermTo(hdInfo->stats) ,
1291                    FsmHdStatsReadSizeTo(hdInfo->stats));
1292      (void)fprintf(vis_stdout, "Completed iteration %d at %g seconds\n",
1293                    depth, (util_cpu_time()/1000.0));
1294
1295      (void)fprintf(vis_stdout, "Step = %d, F = %8g, |F| = %8d, FA = %8g, |FA| = %8d\n",
1296                    depth+1, FsmHdStatsReadMintermFrom(hdInfo->stats),
1297                    FsmHdStatsReadSizeFrom(hdInfo->stats),
1298                    FsmHdStatsReadMintermFromSubset(hdInfo->stats),
1299                    FsmHdStatsReadSizeFromSubset(hdInfo->stats));
1300    } else {
1301      int status;
1302      (void)fprintf(vis_stdout, "Step = %d, |R| = %8d, R = ",
1303                    depth, FsmHdStatsReadSizeReached(hdInfo->stats));
1304      status = bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6);
1305      if (!status) {
1306        error_append("** rch error: Error in printing arbitrary precision minterm count of Reached");
1307      }
1308
1309      (void)fprintf(vis_stdout, "Completed iteration %d at %g seconds\n",
1310                    depth, (util_cpu_time()/1000.0));
1311      (void)fprintf(vis_stdout, "Step = %d, |F| = %8d, F = %8g, |FA| = %8d, FA = ",
1312                    depth, FsmHdStatsReadSizeFrom(hdInfo->stats), 0.0,
1313                    FsmHdStatsReadSizeFromSubset(hdInfo->stats) );
1314      status = bdd_print_apa_minterm(vis_stdout, fromLowerBound, nvars, 6);
1315      if (!status) {
1316        error_append("** rch error: Error in printing arbitrary precision minterm count of From");
1317      }
1318    }
1319  }
1320  return;
1321} /* end of PrintStatsPerIteration */
1322
1323/**Function********************************************************************
1324
1325  Synopsis [Induce full dead-end if there is a big jump in Reached
1326  size]
1327
1328  Description [Induce full dead-end if there is a big jump in Reached
1329  size and not enough increase in minterms of Reached. So throw away
1330  the new large-sized Reached and compute its entire image. Use the
1331  dead-end computation for this and use the non-greedy flag. This is a
1332  recovery mechanism to combat fragmentation of the state space.]
1333
1334  SideEffects [Other quantities are adjusted accordingly. Now the Reached
1335  set before the dead-end computation will be added to the interior states.]
1336
1337******************************************************************************/
1338static void
1339HdInduceFullDeadEndIfNecessary(mdd_manager *mddManager,
1340                               Img_ImageInfo_t *imageInfo,
1341                               mdd_t **fromLowerBound,
1342                               mdd_t **fromUpperBound,
1343                               mdd_t **reachableStates,
1344                               mdd_t **image,
1345                               FsmHdStruct_t *hdInfo,
1346                               int *depth,
1347                               int shellFlag,
1348                               array_t *onionRings,
1349                               array_t *mintermVarArray,
1350                               int oldSize,
1351                               double oldMint,
1352                               int verbosityLevel)
1353{
1354  int nvars =  Fsm_FsmHdOptionReadNumVars(hdInfo->options);
1355  /*
1356   * Compute a full (non-greedy) dead-end when a dead-end computation
1357   * hasn't occurred, and the jump in minterms is lower than MINT_GROWTH and
1358   * either the old reached size is between MID_SIZE and LARGE_SIZE and the
1359   * jump is MID_SIZE or the new size is larger than LARGE_SIZE and the jump
1360   * is LARGE_SIZE.
1361   */
1362  if ((hdInfo->deadEndComputation == FALSE) &&
1363      ((FsmHdStatsReadMintermReached(hdInfo->stats) - oldMint)/oldMint < FSM_HD_MINT_GROWTH) &&
1364      (((FsmHdStatsReadSizeReached(hdInfo->stats)  > FSM_HD_MID_SIZE) &&
1365        (FsmHdStatsReadSizeReached(hdInfo->stats) - oldSize > FSM_HD_MID_SIZE) &&
1366        (oldSize > FSM_HD_MID_SIZE) && (oldSize < FSM_HD_LARGE_SIZE)) ||
1367       ((FsmHdStatsReadSizeReached(hdInfo->stats) > FSM_HD_LARGE_SIZE) &&
1368        (FsmHdStatsReadSizeReached(hdInfo->stats) - oldSize > FSM_HD_LARGE_SIZE)))) {
1369    if (verbosityLevel >= 2) {
1370      fprintf(vis_stdout, "Full Dead End: New Reached = %d, Minterms = %g\n",
1371              FsmHdStatsReadSizeReached(hdInfo->stats), FsmHdStatsReadMintermReached(hdInfo->stats));
1372    }
1373
1374    if (*image != NULL) {
1375      mdd_free(*image);
1376      *image = NULL;
1377    }
1378    /* throw away the reached with the jump in size */
1379    mdd_free(*reachableStates);
1380    if (shellFlag && onionRings) {
1381      mdd_free(array_fetch(mdd_t *, onionRings, array_n(onionRings)-1));
1382      array_insert(mdd_t *, onionRings, array_n(onionRings)-1, NIL(mdd_t));
1383    }
1384
1385    *reachableStates = *fromUpperBound;
1386    /* throw away interior state candidates since we just threw away
1387     * the new states
1388     */
1389    if (hdInfo->interiorStateCandidate != NIL(mdd_t)) {
1390      mdd_free(hdInfo->interiorStateCandidate);
1391      hdInfo->interiorStateCandidate = NIL(mdd_t);
1392    }
1393
1394    if (verbosityLevel >= 2) {
1395      /* record number of dead ends */
1396      (hdInfo->numDeadEnds)++;
1397      fprintf(vis_stdout, "Dead-End %d at %g seconds - FULL\n",
1398              hdInfo->numDeadEnds, (util_cpu_time()/1000.0));
1399    }
1400
1401    /* perform a full non-greedy dead-end computation */
1402    *fromLowerBound = FsmHdDeadEnd(mddManager, imageInfo, *reachableStates,
1403                                  hdInfo,
1404                                  mintermVarArray,
1405                                  FSM_HD_NONGREEDY, verbosityLevel);
1406    (*depth)++;
1407    /* update reached since a new set of seeds have been found */
1408    assert (!mdd_is_tautology(*fromLowerBound, 0));
1409    if (shellFlag && onionRings) {
1410      mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0);
1411      if (!mdd_is_tautology(temp, 0))
1412        array_insert(mdd_t *, onionRings, array_n(onionRings)-1, temp);
1413      else
1414        mdd_free(temp);
1415    }
1416    *fromUpperBound = *reachableStates;
1417    *reachableStates = mdd_or(*fromLowerBound, *fromUpperBound, 1, 1);
1418    FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates,
1419                                     mintermVarArray,  nvars,
1420                                     Fsm_Hd_Reached, hdInfo->stats);
1421  } /* end of if jump in Reached */
1422} /* end of  HdInduceFullDeadEndIfNecessary */
1423
1424
1425/**Function********************************************************************
1426
1427  Synopsis [Compute initial states.]
1428
1429  Description [Compute initial states. Return fsm initial states if no
1430  previously computed states are found. If shell flag, compute union
1431  of rings. If not shell flag, return previously computed states.]
1432
1433  SideEffects []
1434
1435******************************************************************************/
1436static mdd_t *
1437ComputeInitialStates(Fsm_Fsm_t *fsm, int shellFlag, boolean printWarning)
1438{
1439  mdd_t *initialStates = NIL(mdd_t);
1440  boolean rings = FALSE;
1441  array_t *mintermVarArray = Fsm_FsmReadPresentStateVars(fsm);
1442
1443  if (Fsm_FsmReadCurrentReachableStates(fsm) == NIL(mdd_t)) {
1444    initialStates = Fsm_FsmComputeInitialStates(fsm);
1445    return (initialStates);
1446  } else if (shellFlag) {
1447    (void) Fsm_FsmReachabilityOnionRingsStates(fsm, &initialStates);
1448    if (initialStates == NIL(mdd_t)) {
1449      initialStates = Fsm_FsmComputeInitialStates(fsm);
1450      return (initialStates);
1451    } else if (mdd_is_tautology(initialStates, 0)) {
1452      initialStates = Fsm_FsmComputeInitialStates(fsm);
1453      return (initialStates);
1454    }
1455    /* some states are found in the onion rings */
1456    rings = TRUE;
1457  } else {
1458    /* use previously computed states */
1459    initialStates = mdd_dup(Fsm_FsmReadCurrentReachableStates(fsm));
1460  }
1461  if (printWarning) {
1462    fprintf(vis_stdout, "** rch warning: Starting reachability analysis from previously computed states.\n");
1463    fprintf(vis_stdout, "** rch warning: Use compute_reach -F to recompute if necessary.\n");
1464    fprintf(vis_stdout, "** rch warning: Previously computed states = %g, Size = %d, computation depth = 0-%d\n", mdd_count_onset(Fsm_FsmReadMddManager(fsm), initialStates, mintermVarArray), mdd_size(initialStates), fsm->reachabilityInfo.depth);
1465    if (!rings) {
1466      if (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Bfs_c) {
1467        fprintf(vis_stdout, "** rch warning: Previous computation done with BFS (-A 0 option)\n");
1468      } else if (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Hd_c) {
1469        fprintf(vis_stdout, "** rch warning: Some previous computations done using BFS/DFS mode (-A 1 or -g option)\n");
1470      }
1471    } else {
1472      if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Bfs_c) {
1473        fprintf(vis_stdout, "** rch warning: Previous onion rings computed with BFS (-A 0 option)\n");
1474      } else if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Hd_c) {
1475        fprintf(vis_stdout, "** rch warning: Some set of onion rings have been computed using BFS/DFS (-A 1 or -g option)\n");
1476      }
1477    }
1478  }
1479  return (initialStates);
1480} /* end of ComputeInitialStates */
1481
1482
1483/**Function********************************************************************
1484
1485  Synopsis [Checks if the reachable states are contained in each
1486  element of an array of invariants.]
1487
1488  Description [Checks if the reachable states are contained in each
1489  element of an array of invariants. Returns 0 as soon as a violation
1490  is found.]
1491
1492  SideEffects []
1493
1494******************************************************************************/
1495static int
1496CheckStatesContainedInInvariant(mdd_t *reachableStates,
1497                                array_t *invarStates)
1498{
1499  int i;
1500  mdd_t *invariant;
1501
1502  arrayForEachItem(mdd_t *, invarStates, i, invariant) {
1503    if (invariant == NIL(mdd_t)) continue;
1504    if (!mdd_lequal(reachableStates, invariant, 1, 1)) {
1505      return 0;
1506    }
1507  }
1508  return 1;
1509}
1510
1511/**Function********************************************************************
1512
1513  Synopsis [Computes the reachable states, fromLowerBound and
1514  fromUpperBound for HD Traversal.]
1515
1516  Description [Computes the reachable states, fromLowerBound and
1517  fromUpperBound for HD Traversal. Updates all other arguments such as
1518  interiorStates, deadEndResidue . There are 3 major operations in
1519  this procedure. 1. Induce (if slow growth in reached) and compute a
1520  dead-end if necessary. 2. Compute the image of Reached if there is a
1521  big jump in its size. 3. Compute a dense subset of states to be used
1522  as a frontier in the next iteration.
1523
1524  1. A dead-end is the situation where no new states have been
1525  produced (fromLowerBound = 0), It is induced if the rate of growth
1526  of Reached is slow. If the image of the Entire Reached set has been
1527  computed in the previous iteration, then pretend this is a dead-end.
1528
1529  2. If the jump in Reached is large, compute its entire image to
1530  recover from fragmentation.
1531
1532  3. A dense subset of the frontier set is computed to be used as the
1533  frontier set in the next iteration. The update of reached is
1534  performed in this step (may not add scrap states if
1535  specified.). If a dead-end has just been performed, the new states
1536  are always added to Reached. Growth rate monitors are also
1537  updated. ]
1538
1539  SideEffects []
1540
1541******************************************************************************/
1542static void
1543HdComputeReachabilityParameters(mdd_manager *mddManager,
1544                                Img_ImageInfo_t *imageInfo,
1545                                mdd_t **reachableStates,
1546                                mdd_t **fromUpperBound,
1547                                mdd_t **fromLowerBound,
1548                                mdd_t **image,
1549                                FsmHdStruct_t *hdInfo,
1550                                mdd_t *initialStates,
1551                                array_t *mintermVarArray,
1552                                int *depth,
1553                                int printStep,
1554                                int shellFlag,
1555                                array_t *onionRings,
1556                                int verbosityLevel)
1557{
1558  float growth;
1559  boolean scrapStates;
1560  int nvars = Fsm_FsmHdOptionReadNumVars(hdInfo->options);
1561  int oldSize;
1562  double oldMint;
1563  int sizeOfOnionRings = 0;
1564  if (shellFlag && onionRings) {
1565    sizeOfOnionRings = array_n(onionRings);
1566  }
1567
1568  verbosityLevel = (printStep && (((*depth) % printStep) == 0)) ? verbosityLevel : 0;
1569
1570  /* keep image if small, record size of the image */
1571  oldSize = FsmHdStatsReadSizeReached(hdInfo->stats);
1572  oldMint = FsmHdStatsReadMintermReached(hdInfo->stats);
1573  FsmHdStatsReset(hdInfo->stats, Fsm_Hd_Reached);
1574  FsmHdStatsReset(hdInfo->stats, Fsm_Hd_FromSubset);
1575  FsmHdStatsReset(hdInfo->stats, Fsm_Hd_From);
1576
1577  scrapStates =  Fsm_FsmHdOptionReadScrapStates(hdInfo->options);
1578  hdInfo->onlyPartialImage =  Fsm_FsmHdOptionReadOnlyPartialImage(hdInfo->options);
1579
1580  /* Step 1: Check comments at the top of this function */
1581  /* Check if this is a dead end */
1582  /* if growth rate of reached is really small, induce a dead-end */
1583  hdInfo->deadEndComputation = FALSE;
1584  if ((hdInfo->imageOfReachedComputed) ||
1585      (mdd_is_tautology(*fromLowerBound, 0)) ||
1586      (hdInfo->slowGrowth >= 5)) {
1587    /*
1588     * if image of reached is computed, add to the dead states.
1589     * Set dead-end computation flag and add all new states to Reached.
1590     */
1591
1592    /* add to interior states */
1593    hdInfo->interiorStates = AddStates(hdInfo->interiorStates,
1594                                       hdInfo->interiorStateCandidate,
1595                                       FSM_MDD_FREE, FSM_MDD_FREE);
1596    hdInfo->interiorStateCandidate = NIL(mdd_t);
1597    if ((verbosityLevel >= 2) && (hdInfo->interiorStates != NIL(mdd_t))) {
1598      fprintf(vis_stdout, "Interior states added, Size = %d, Minterms = %g\n",
1599              mdd_size(hdInfo->interiorStates), mdd_count_onset(mddManager,
1600                                        hdInfo->interiorStates, mintermVarArray));
1601    }
1602
1603    hdInfo->deadEndComputation = TRUE;
1604    hdInfo->firstSubset = FALSE;
1605    hdInfo->slowGrowth = 0;
1606    hdInfo->lastIter = *depth;
1607
1608    if (!hdInfo->imageOfReachedComputed) {
1609      /* Either slow growth or real dead-end */
1610      if (verbosityLevel >= 2) {
1611        if (!mdd_is_tautology(*fromLowerBound, 0))
1612          fprintf(vis_stdout, "Dead-End triggered by slow growth\n");
1613        /* record number of dead ends */
1614        (hdInfo->numDeadEnds)++;
1615        fprintf(vis_stdout, "Dead-End %d at %g seconds\n", hdInfo->numDeadEnds,
1616                (util_cpu_time()/1000.0));
1617      }
1618
1619      /* add another onion ring. */
1620      if (shellFlag && onionRings && !mdd_is_tautology(*fromLowerBound, 0)) {
1621        mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0);
1622        if (!mdd_is_tautology(temp, 0))
1623          array_insert_last(mdd_t *, onionRings, temp);
1624        else
1625          mdd_free(temp);
1626      }
1627      *reachableStates = AddStates(*fromLowerBound, *reachableStates,
1628                                  FSM_MDD_FREE, FSM_MDD_FREE);
1629      *fromUpperBound = *reachableStates;
1630
1631          /* perform a dead-end computation */
1632      *fromLowerBound = FsmHdDeadEnd(mddManager, imageInfo, *reachableStates,
1633                                    hdInfo,
1634                                    mintermVarArray,
1635                                    FSM_HD_GREEDY, verbosityLevel);
1636
1637      (*depth)++;
1638    }
1639  } /* end of if dead-end computation */
1640
1641  /* Step 2: Check comments at the top of this function */
1642  if (!mdd_is_tautology(*fromLowerBound, 0)) {
1643    /* add another onion ring. */
1644    if (shellFlag && onionRings) {
1645      mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0);
1646      if (!mdd_is_tautology(temp, 0))
1647        array_insert_last(mdd_t *, onionRings, temp);
1648      else
1649        mdd_free(temp);
1650    }
1651    /* compute reachable states with new states */
1652    *fromUpperBound = *reachableStates;
1653    *reachableStates = mdd_or(*fromLowerBound, *fromUpperBound, 1, 1);
1654    FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates,
1655                                     mintermVarArray, nvars,
1656                                     Fsm_Hd_Reached, hdInfo->stats);
1657
1658
1659    /*
1660         * induce a full dead-end computation if jump in size of Reached is
1661         * large. But when the image of Reached has been computed or a dead-end
1662         * computation was just done, this is not done because deadEndComputation
1663         * has been set to 1.
1664         */
1665    HdInduceFullDeadEndIfNecessary(mddManager, imageInfo, fromLowerBound,
1666                                   fromUpperBound, reachableStates, image,
1667                                   hdInfo, depth, shellFlag, onionRings,
1668                                   mintermVarArray, oldSize,
1669                                   oldMint, verbosityLevel);
1670  } /* end of  if (!mdd_is_tautology(fromLowerBound, 0)) */
1671
1672  /* Step 3: Check comments at the top of this function */
1673  /* Create subset if necessary */
1674  if (!mdd_is_tautology(*fromLowerBound, 0)) {
1675    if (!hdInfo->onlyPartialImage) {
1676      mdd_t *newStates;
1677      /*
1678       * Now fromUpperBound has the old reached states, reachableStates
1679       * has the new set of states.
1680       */
1681      newStates = mdd_dup(*fromLowerBound);
1682      FsmHdFromComputeDenseSubset(mddManager, fromLowerBound,
1683                                  fromUpperBound, reachableStates,
1684                                  image, initialStates, hdInfo,
1685                                  shellFlag, onionRings, sizeOfOnionRings,
1686                                  mintermVarArray);
1687
1688      /* if all new states are chosen from the previous iteration and
1689       * all these states have been added then add to interior states.
1690       * All new states are sometimes not added when
1691       * hdInfo->options->scrapStates is 0. Dead-end computations need not be
1692       * considered here since the interior states were already added then.
1693       */
1694      if ((hdInfo->interiorStateCandidate != NIL(mdd_t)) &&
1695          ((mdd_lequal(newStates, *fromLowerBound, 1, 1)) ||
1696           (scrapStates == TRUE))) {
1697        hdInfo->interiorStates = AddStates(hdInfo->interiorStates, hdInfo->interiorStateCandidate,
1698                                   FSM_MDD_FREE, FSM_MDD_FREE);
1699        hdInfo->interiorStateCandidate = NIL(mdd_t);
1700        if (verbosityLevel >= 2) {
1701          fprintf(vis_stdout,
1702                  "Interior states added, Size = %d, Minterms = %g\n",
1703                  mdd_size(hdInfo->interiorStates),
1704                  mdd_count_onset(mddManager, hdInfo->interiorStates,
1705                                  mintermVarArray));
1706        }
1707      }
1708      mdd_free(newStates);
1709
1710      /* end of if fromLowerbound == 0 && subset Flag*/
1711    } else  {
1712      mdd_free(*fromUpperBound);
1713      if (printStep && ((*depth) % printStep == 0)) {
1714        FsmHdStatsComputeSizeAndMinterms(mddManager, *fromLowerBound,
1715                                         mintermVarArray, nvars, Fsm_Hd_From, hdInfo->stats);
1716        FsmHdStatsSetMintermFromSubset(hdInfo->stats, 0.0);
1717        FsmHdStatsSetSizeFromSubset(hdInfo->stats, 0);
1718      }
1719      *fromUpperBound = *reachableStates;
1720    }
1721  } /* end of if fromLowerBound == 0 */
1722  if (hdInfo->interiorStateCandidate != NIL(mdd_t)) {
1723    mdd_free(hdInfo->interiorStateCandidate);
1724    hdInfo->interiorStateCandidate = NIL(mdd_t);
1725  }
1726
1727  /* monitor growth rate of reached, record if slow growth in consecutive
1728   * iterations
1729   */
1730  if (!mdd_is_tautology(*fromLowerBound, 0)) {
1731    FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates,
1732                                     mintermVarArray, nvars, Fsm_Hd_Reached, hdInfo->stats);
1733    growth = (float)(FsmHdStatsReadMintermReached(hdInfo->stats) - oldMint)/
1734      (float)oldMint;
1735    if ((growth < FSM_HD_GROWTH_RATE) &&
1736        (((hdInfo->slowGrowth) && ((*depth) == (hdInfo->lastIter) + 1)) || (!(hdInfo->slowGrowth)))) {
1737      if (verbosityLevel >= 2) {
1738        fprintf(vis_stdout, "Growth rate = %f\n", growth);
1739      }
1740      (hdInfo->slowGrowth)++;
1741      hdInfo->lastIter = *depth;
1742    } else {
1743      /* reset value */
1744      hdInfo->slowGrowth = 0;
1745    }
1746  }
1747  return;
1748} /* end of HdComputeReachabilityParameters */
1749
1750/**Function********************************************************************
1751
1752  Synopsis [Initializes parameters for incremental computation.]
1753
1754  Description [Initializes parameters for incremental computation.
1755  Instantiates arrayOfRoots and tableOfLeafs, and returns the number of latches
1756  in the sytstem.  Upon return, arrayOfRoots is an array of Ntk_Node_t *, and
1757  tableOfLeaves is an st_table of Ntk_Node_t *.]
1758
1759  SideEffects []
1760
1761******************************************************************************/
1762static int
1763InitializeIncrementalParameters(
1764  Fsm_Fsm_t *fsm,
1765  Ntk_Network_t *network,
1766  array_t **arrayOfRoots,
1767  st_table **tableOfLeaves)
1768{
1769  int numLatch;
1770  Ntk_Node_t *node;
1771  lsGen gen;
1772  int i, mddId;  /* iterate over the nextStateVars of the fsm */
1773
1774  numLatch = Ntk_NetworkReadNumLatches(network);
1775
1776  /* This changed to fix a bug.  Instead of reading the roots using
1777     Ntk_NetworkForEachCombOutput, we now get them from
1778     fsm->fsdData.nextStateVars, which means that the order is consistent with
1779     the latter field, as required later on in the incremental reachability
1780     code
1781
1782     old code:
1783     *arrayOfRoots = array_alloc(Ntk_Node_t *, numLatch);
1784     Ntk_NetworkForEachCombOutput(network, gen, node) {
1785     if(Ntk_NodeTestIsLatchDataInput(node)){
1786     array_insert_last(Ntk_Node_t *, *arrayOfRoots, node);
1787    }
1788  }
1789  */
1790
1791  assert(numLatch == array_n(fsm->fsmData.nextStateVars));
1792  *arrayOfRoots = array_alloc(Ntk_Node_t *, numLatch);
1793
1794  arrayForEachItem(int, fsm->fsmData.nextStateVars, i, mddId){
1795    Ntk_Node_t *shadow;
1796    Ntk_Node_t *latch;
1797    Ntk_Node_t *dataInput;
1798
1799    shadow = Ntk_NetworkFindNodeByMddId(network, mddId);
1800    assert(Ntk_NodeTestIsShadow(shadow));
1801    latch = Ntk_ShadowReadOrigin(shadow);
1802    assert(Ntk_NodeTestIsLatch(latch));
1803    dataInput = Ntk_LatchReadDataInput(latch);
1804    assert(dataInput != NIL(Ntk_Node_t));
1805
1806    array_insert(Ntk_Node_t *, *arrayOfRoots, i, dataInput);
1807  }
1808
1809  *tableOfLeaves = st_init_table(st_ptrcmp, st_ptrhash);
1810  Ntk_NetworkForEachCombInput(network, gen, node) {
1811    st_insert(*tableOfLeaves, (char *)node, (char *) (long) (-1) );
1812  }
1813  return (numLatch);
1814}
1815
1816
1817/**Function********************************************************************
1818
1819  Synopsis [Computes image for incremental computation.]
1820
1821  Description [Computes image for  incremental computation.]
1822
1823  SideEffects []
1824
1825******************************************************************************/
1826static mdd_t *
1827IncrementalImageCompute(Ntk_Network_t *network,
1828                        Fsm_Fsm_t *fsm,
1829                        mdd_manager *mddManager,
1830                        mdd_t *fromLowerBound,
1831                        mdd_t *fromUpperBound,
1832                        mdd_t *toCareSet,
1833                        array_t *arrayOfRoots,
1834                        st_table *tableOfLeaves,
1835                        array_t *smoothVarArray,
1836                        array_t *relationArray,
1837                        int numLatch)
1838{
1839  Mvf_Function_t *function;
1840  mdd_t *relation, *optimizedRelation, *toCareSetRV, *imageRV;
1841  mdd_t  *subOptimizedRelation, *image;
1842  int mddId, i;
1843  array_t *arrayOfMvf;
1844  mdd_t *frontierSet;
1845
1846  frontierSet = bdd_between(fromLowerBound, fromUpperBound);
1847  /* Create the array of transition relations */
1848  toCareSetRV = mdd_substitute(mddManager, toCareSet,
1849                               fsm->fsmData.presentStateVars,
1850                               fsm->fsmData.nextStateVars);
1851
1852  arrayOfMvf = Ntm_NetworkBuildMvfs(network, arrayOfRoots,
1853                                    tableOfLeaves, frontierSet);
1854  for (i=0; i < numLatch; i++){
1855    function = array_fetch(Mvf_Function_t *, arrayOfMvf, i);
1856    mddId = array_fetch(int, fsm->fsmData.nextStateVars, i);
1857    /* Since both arrayOfMvf and fsmData have been obtained from */
1858    /* the same generator */
1859    relation = Mvf_FunctionBuildRelationWithVariable(function,
1860                                                     mddId);
1861    subOptimizedRelation = bdd_cofactor(relation, toCareSetRV);
1862    mdd_free(relation);
1863    optimizedRelation = bdd_cofactor(subOptimizedRelation, frontierSet);
1864    mdd_free(subOptimizedRelation);
1865    array_insert(mdd_t *, relationArray, i, optimizedRelation);
1866  }
1867  Mvf_FunctionArrayFree(arrayOfMvf);
1868  mdd_free(toCareSetRV);
1869  array_insert(mdd_t *, relationArray, numLatch, frontierSet);
1870  imageRV = Fsm_MddMultiwayAndSmooth(mddManager, relationArray,
1871                                     smoothVarArray);
1872  /*
1873  ** The above call can be substituted by more sophisticated
1874  ** Img_MultiwayLinearAndSmooth. However, that will have its
1875  ** associated overhead, and could offset any advantage. We
1876  ** expect that individual transition relation relations should
1877  ** be small and monolithic way to handle them would be ok.
1878  ** However, a good strategy would be find the quantification
1879  ** schedule which does not change with the computation of
1880  ** incremental transition relations.
1881  */
1882  for (i = 0; i <= numLatch; i++){
1883    mdd_free(array_fetch(mdd_t*, relationArray, i));
1884  }
1885  assert(CheckImageValidity(mddManager, imageRV,
1886                            fsm->fsmData.presentStateVars,
1887                            fsm->fsmData.inputVars));
1888  image = mdd_substitute(mddManager, imageRV,
1889                         fsm->fsmData.nextStateVars,
1890                         fsm->fsmData.presentStateVars);
1891  mdd_free(imageRV);
1892  assert(CheckImageValidity(mddManager, image,
1893                            fsm->fsmData.nextStateVars,
1894                            fsm->fsmData.inputVars));
1895  return image;
1896}
1897
1898/**Function********************************************************************
1899
1900  Synopsis [Prints information about onion rings]
1901
1902  Description [Prints information about onion rings.]
1903
1904  SideEffects []
1905
1906******************************************************************************/
1907static void
1908PrintOnionRings(Fsm_Fsm_t *fsm, int printStep,
1909                Fsm_RchType_t approxFlag, int nvars)
1910{
1911  int i;
1912  mdd_t *reachableStates;
1913  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
1914  array_t *mintermVarArray = Fsm_FsmReadPresentStateVars(fsm);
1915
1916  fprintf(vis_stdout, "** rch warning: Not possible to compute size of reachable states at every iteration\n");
1917  if (Fsm_FsmReadReachabilityOnionRings(fsm) != NIL(array_t)) {
1918    arrayForEachItem(mdd_t *, Fsm_FsmReadReachabilityOnionRings(fsm),
1919                     i, reachableStates) {
1920      if (printStep && (i % printStep == 0)) {
1921        if (approxFlag != Fsm_Rch_Hd_c) {
1922          if (nvars <= 1023) {
1923            (void)fprintf(vis_stdout, "BFS step = %d\t|onion ring states| = %8g",
1924                          i, mdd_count_onset(mddManager, reachableStates,
1925                                             mintermVarArray));
1926            if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) {
1927              fprintf(vis_stdout, "\n");
1928            } else {
1929              fprintf(vis_stdout, "\tSize = %d\n", mdd_size(reachableStates));
1930            }
1931
1932          } else {
1933            (void)fprintf(vis_stdout, "BFS step = %d\t|onion ring states| = ",
1934                          i);
1935            (void) bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6);
1936            if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) {
1937              fprintf(vis_stdout, "Final Size = %d\n", mdd_size(reachableStates));
1938            }
1939          }
1940        } else {
1941
1942          if (nvars <= 1023) {
1943            (void)fprintf(vis_stdout, "Step = %d\t|onion ring states| = %8g",
1944                          i, mdd_count_onset(mddManager, reachableStates,
1945                                             mintermVarArray));
1946            if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) {
1947              fprintf(vis_stdout, "\n");
1948            } else {
1949              fprintf(vis_stdout, "\tSize = %d\n", mdd_size(reachableStates));
1950            }
1951          } else {
1952            (void)fprintf(vis_stdout, "Step = %d\t|onion ring states| = ",
1953                          i);
1954            (void) bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6);
1955            if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) {
1956              fprintf(vis_stdout, "Final Size = %d\n", mdd_size(reachableStates));
1957            }
1958          }
1959        }
1960      }
1961    }
1962  }
1963  return;
1964}/* printonionrings */
1965
1966/**Function********************************************************************
1967
1968  Synopsis [Reads in a sequence of integers separated by commas and
1969  stores them in an array.]
1970
1971  Description [Reads in a sequence of integers separated by commas from the
1972  environment variable guided_search_sequence.  It stores them in an array that
1973  it returns.  Alpha characters and 0 integers are replaced by
1974  -1.  Pads the remaining entries corresponding to the guide array with -1.
1975  Every number indicates the number of times the corresponding (in sequence)
1976  hint should be used.  The value -1 means `to convergence'.]
1977
1978
1979  SideEffects []
1980
1981******************************************************************************/
1982static array_t *
1983GenerateGuidedSearchSequenceArray(array_t *guideArray)
1984{
1985  char *seqStr = Cmd_FlagReadByName("guided_search_sequence");
1986  char *preStr;
1987  int intEntry;
1988  array_t *depthArray = array_alloc(int, 0);
1989  int i;
1990
1991  /* Skip parsing if we have no guided search sequence  */
1992  if (seqStr != NIL(char)  && strcmp(seqStr, "") != 0){
1993    preStr = strtok(seqStr, ",");
1994
1995    while(preStr != NIL(char)){
1996      intEntry = strtol(preStr, (char **) NULL, 10);
1997      array_insert_last(int, depthArray, (intEntry == 0 ? -1 : intEntry));
1998      preStr = strtok(NIL(char), ",");
1999    }
2000  }
2001
2002  if(array_n(depthArray) > array_n(guideArray)){
2003    fprintf(vis_stdout, "** rch warning: guided_search_sequence has more entries\n");
2004    fprintf(vis_stdout,"than there are hints.  Extra entires will be ignored\n");
2005  }
2006
2007  /* pad with -1s */
2008  for (i = array_n(depthArray); i < array_n(guideArray); i++) {
2009    array_insert_last(int, depthArray, -1);
2010  }
2011
2012  assert(array_n(depthArray) >= array_n(guideArray));
2013
2014  return depthArray;
2015}
2016
2017
2018/**Function********************************************************************
2019
2020  Synopsis [Computes the reachable states, frontier and fromUpperBound.]
2021
2022  Description [Computes the reachable states, frontier and
2023  fromUpperBound. For HD it also generates interior states, interior
2024  state candidates, dead-end residue, number of dead-ends, residue
2025  count, etc. For guided search, this procedure also generates a
2026  dead-end if the frontier is 0. Also this procedure keeps track of
2027  convergence and whether a dead-end is required at the end.]
2028
2029  SideEffects [All arguments are updated.]
2030
2031  SeeAlso [HdComputeReachabilityParameters FsmHdDeadEnd]
2032
2033******************************************************************************/
2034static void
2035ComputeReachabilityParameters(mdd_manager *mddManager,
2036                              Img_ImageInfo_t *imageInfo,
2037                              Fsm_RchType_t approxFlag,
2038                              mdd_t **reachableStates,
2039                              mdd_t **fromUpperBound,
2040                              mdd_t **fromLowerBound,
2041                              mdd_t **image,
2042                              FsmHdStruct_t *hdInfo,
2043                              mdd_t *initialStates,
2044                              array_t *mintermVarArray,
2045                              int *depth,
2046                              int printStep,
2047                              int shellFlag,
2048                              array_t *onionRings,
2049                              int verbosityLevel,
2050                              boolean guidedSearchMode,
2051                              mdd_t *hint,
2052                              int *hintDepth,
2053                              boolean *notConverged)
2054{
2055  if (approxFlag == Fsm_Rch_Bfs_c) {
2056    /* New set of reachable states is old set plus new states in image. */
2057    *reachableStates = AddStates(*fromLowerBound, *reachableStates,
2058                                 FSM_MDD_DONT_FREE, FSM_MDD_FREE);
2059    *fromUpperBound = *reachableStates;
2060
2061    /* in guided search, if the mode is to convergence or the
2062       limited depth has not been reached, and the frontier is empty,
2063       then generate a frontier in BFS mode (that is a full dead-end).  */
2064    if (guidedSearchMode &&
2065        mdd_is_tautology(*fromLowerBound, 0) /* no frontier */ &&
2066        (hdInfo->deadEndWithOriginalTR == FALSE) /* and guided search */ ) {
2067      assert(imageInfo != NIL(Img_ImageInfo_t));
2068      if (*hintDepth != 0) {
2069        /* add another onion ring. */
2070        if (shellFlag && onionRings) {
2071          mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0);
2072          if (!mdd_is_tautology(temp, 0))
2073            array_insert_last(mdd_t *, onionRings, temp);
2074          else
2075            mdd_free(temp);
2076        }
2077        /* do a full dead-end (non-greedy), compute all the frontier states */
2078        mdd_free(*fromLowerBound);
2079        *fromLowerBound = FsmHdDeadEnd(mddManager, imageInfo, *reachableStates,
2080                                       hdInfo,
2081                                       mintermVarArray,
2082                                       FSM_HD_NONGREEDY, verbosityLevel);
2083        mdd_free(hdInfo->interiorStates);
2084        hdInfo->interiorStates = NIL(mdd_t);
2085        *reachableStates = AddStates(*fromLowerBound, *reachableStates,
2086                                     FSM_MDD_DONT_FREE, FSM_MDD_FREE);
2087        *fromUpperBound = *reachableStates;
2088        (*hintDepth)--;
2089        (*depth)++;
2090        if (mdd_is_tautology(hint, 1)) hdInfo->deadEndWithOriginalTR = TRUE;
2091      } else {
2092        *notConverged = TRUE;
2093        /* set this flag for correct detection of convergence
2094           Corner case: when limited depth and frontier = 0 */
2095      }
2096    }
2097  } else if (approxFlag == Fsm_Rch_Hd_c) {
2098    assert(imageInfo != NIL(Img_ImageInfo_t));
2099      if (!guidedSearchMode || (*hintDepth != 0)) {
2100        /* computes reachable states, fromLowerBound and fromUpperBound.
2101         * Updates all other quantities such as interiorStates,
2102         * deadEndResidue. */
2103        HdComputeReachabilityParameters(mddManager, imageInfo,
2104                                        reachableStates,
2105                                        fromUpperBound,
2106                                        fromLowerBound,
2107                                        image,
2108                                        hdInfo,
2109                                        initialStates,
2110                                        mintermVarArray,
2111                                        depth, printStep,
2112                                        shellFlag, onionRings,
2113                                        verbosityLevel);
2114        if (guidedSearchMode) (*hintDepth)--;
2115
2116      } else { /* guidedSearchMode and hint depth is 0 */
2117        if (mdd_is_tautology(*fromLowerBound, 0)) {
2118          *notConverged = TRUE;
2119        /* set this flag for correct detection of convergence
2120           Corner case: when limited depth and frontier = 0 */
2121        }
2122        /* add another onion ring. */
2123        if (shellFlag && onionRings) {
2124          mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0);
2125          if (!mdd_is_tautology(temp, 0))
2126            array_insert_last(mdd_t *, onionRings, temp);
2127          else
2128            mdd_free(temp);
2129        }
2130
2131      }
2132  }
2133  return;
2134} /* End of ComputeReachabilityParameters */
Note: See TracBrowser for help on using the repository browser.