source: vis_dev/vis-2.3/src/mc/mcSCC.c @ 83

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

vis2.3
File size: 49.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [mcSCC.c]
4
5  PackageName [mc]
6
7  Synopsis    [Computation of Fair Strongly Connected Components.]
8
9  Description [This file contains the functions to compute the fair
10  Strongly Connected Components (SCCs) of the state transtion graph of
11  an FSM.  Knowledge of the fair SCCs can be used to decide language
12  emptiness.  Other applications are also possible.]
13
14  SeeAlso     []
15
16  Author      [Fabio Somenzi, Chao Wang]
17
18  Copyright   [This file was created at the University of Colorado at
19  Boulder.  The University of Colorado at Boulder makes no warranty
20  about the suitability of this software for any purpose.  It is
21  presented on an AS IS basis.]
22
23******************************************************************************/
24
25#include "mcInt.h"
26
27/*#define  SCC_NO_TRIM */
28
29/*---------------------------------------------------------------------------*/
30/* Constant declarations                                                     */
31/*---------------------------------------------------------------------------*/
32
33/*---------------------------------------------------------------------------*/
34/* Stucture declarations                                                     */
35/*---------------------------------------------------------------------------*/
36struct GraphNodeSpineSet {
37  mdd_t *states;  /* V    */
38  mdd_t *spine;   /* S    */
39  mdd_t *node;    /* Node */
40};
41
42/*---------------------------------------------------------------------------*/
43/* Type declarations                                                         */
44/*---------------------------------------------------------------------------*/
45typedef struct GraphNodeSpineSet gns_t;
46
47/*---------------------------------------------------------------------------*/
48/* Variable declarations                                                     */
49/*---------------------------------------------------------------------------*/
50
51#ifndef lint
52static char rcsid[] UNUSED = "$Id: mcSCC.c,v 1.11 2005/05/18 19:35:19 jinh Exp $";
53#endif
54
55/*---------------------------------------------------------------------------*/
56/* Macro declarations                                                        */
57/*---------------------------------------------------------------------------*/
58
59/**AutomaticStart*************************************************************/
60
61/*---------------------------------------------------------------------------*/
62/* Static function prototypes                                                */
63/*---------------------------------------------------------------------------*/
64
65static mdd_t * LockstepPickSeed(Fsm_Fsm_t *fsm, mdd_t *V, array_t *buechiFairness, array_t *onionRings, int ringIndex);
66static void LockstepQueueEnqueue(Fsm_Fsm_t *fsm, Heap_t *queue, mdd_t *states, array_t *onionRings, McLockstepMode mode, array_t *buechiFairness, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
67static void LinearstepQueueEnqueue(Fsm_Fsm_t *fsm, Heap_t *queue, mdd_t *states, mdd_t *spine, mdd_t *node, array_t *onionRings, McLockstepMode mode, array_t *buechiFairness, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
68static int GetSccEnumerationMethod( void );
69
70/**AutomaticEnd***************************************************************/
71
72
73/*---------------------------------------------------------------------------*/
74/* Definition of exported functions                                          */
75/*---------------------------------------------------------------------------*/
76
77
78/**Function********************************************************************
79
80  Synopsis    [Generates the first fair SCC of a FSM.]
81
82  Description [Defines an iterator on the fair SCCs of a FSM and finds the
83  first fair SCC.  Returns a generator that contains the information
84  necessary to continue the enumeration if successful; NULL
85  otherwise.]
86
87  SideEffects [The fair SCC is retuned as a side effect.]
88
89  SeeAlso     [Mc_FsmForEachScc Mc_FsmNextScc Mc_FsmIsSccGenEmpty
90  Mc_FsmSccGenFree]
91
92******************************************************************************/
93Mc_SccGen_t *
94Mc_FsmFirstScc(
95  Fsm_Fsm_t *fsm,
96  mdd_t **scc,
97  array_t *sccClosedSetArray,
98  array_t *buechiFairness,
99  array_t *onionRings,
100  boolean earlyTermination,
101  Mc_VerbosityLevel verbosity,
102  Mc_DcLevel dcLevel)
103{
104  Mc_SccGen_t *gen;
105  Heap_t      *heap;
106  int         i;
107  mdd_t       *closedSet;
108  int         linearStepMethod;
109
110  if (fsm == NIL(Fsm_Fsm_t)) return NIL(Mc_SccGen_t);
111
112  /* Allocate generator and initialize it. */
113  gen = ALLOC(Mc_SccGen_t, 1);
114  if (gen == NIL(Mc_SccGen_t))  return NIL(Mc_SccGen_t);
115
116  gen->fsm = fsm;
117  gen->heap = heap = Heap_HeapInit(1);
118  gen->rings = onionRings;
119  gen->buechiFairness = buechiFairness;
120  gen->earlyTermination = earlyTermination;
121  gen->verbosity = verbosity;
122  gen->dcLevel = dcLevel;
123  gen->totalExamined = 0;
124  gen->nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
125  gen->nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
126
127  linearStepMethod = GetSccEnumerationMethod();
128  /* Initialize the heap from the given sets of states. */
129  arrayForEachItem(mdd_t *, sccClosedSetArray, i, closedSet) {
130    if (linearStepMethod == 1) {
131      mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
132      LinearstepQueueEnqueue(fsm, heap, mdd_dup(closedSet), 
133                             mdd_zero(mddManager),
134                             mdd_zero(mddManager), onionRings,
135                             McLS_none_c, buechiFairness, verbosity, dcLevel);
136    }else {
137      LockstepQueueEnqueue(fsm, heap, mdd_dup(closedSet), onionRings,
138                           McLS_none_c, buechiFairness, verbosity, dcLevel);
139    }
140  }
141  /* Find first SCC. */
142  if (Heap_HeapCount(heap) == 0) {
143    *scc = NIL(mdd_t);
144  } else {
145    if (linearStepMethod == 1)
146      *scc = McFsmComputeOneFairSccByLinearStep(fsm, heap, buechiFairness,
147                                                onionRings, earlyTermination,
148                                                verbosity, dcLevel,
149                                                &(gen->totalExamined));
150    else
151      *scc = McFsmComputeOneFairSccByLockStep(fsm, heap, buechiFairness,
152                                              onionRings, earlyTermination,
153                                              verbosity, dcLevel,
154                                              &(gen->totalExamined));
155  }
156  if (*scc == NIL(mdd_t)) {
157    gen->status = McSccGenEmpty_c;
158    gen->fairSccsFound = 0;
159  } else {
160    gen->status = McSccGenNonEmpty_c;
161    gen->fairSccsFound = 1;
162  }
163  return gen;
164
165} /* Mc_FsmFirstScc */
166
167
168/**Function********************************************************************
169
170  Synopsis    [Generates the next fair SCC of a FSM.]
171
172  Description [Generates the next fair SCC of a FSM, using generator
173  gen. Returns FALSE if the enumeration is completed; TRUE otherwise.]
174
175  SideEffects [The fair SCC is returned as side effect.]
176
177  SeeAlso     [Mc_FsmForEachScc Mc_FsmFirstScc Mc_FsmIsSccGenEmpty
178  Mc_FsmSccGenFree]
179
180******************************************************************************/
181boolean
182Mc_FsmNextScc(
183  Mc_SccGen_t *gen,
184  mdd_t **scc)
185{
186  int linearStepMethod;
187
188  if (gen->earlyTermination == TRUE) {
189    gen->status = McSccGenEmpty_c;
190    return FALSE;
191  }
192  linearStepMethod = GetSccEnumerationMethod();
193  if (linearStepMethod == 1) 
194    *scc = McFsmComputeOneFairSccByLinearStep(gen->fsm, gen->heap,
195                                              gen->buechiFairness, gen->rings,
196                                              gen->earlyTermination,
197                                              gen->verbosity, gen->dcLevel,
198                                              &(gen->totalExamined));
199  else
200    *scc = McFsmComputeOneFairSccByLockStep(gen->fsm, gen->heap,
201                                            gen->buechiFairness, gen->rings,
202                                            gen->earlyTermination,
203                                            gen->verbosity, gen->dcLevel,
204                                            &(gen->totalExamined));
205  if (*scc == NIL(mdd_t)) {
206    gen->status = McSccGenEmpty_c;
207    return FALSE;
208  } else {
209    gen->status = McSccGenNonEmpty_c;
210    gen->fairSccsFound++;
211    return TRUE;
212  }
213
214} /* Mc_FsmNextScc */
215
216
217/**Function********************************************************************
218
219  Synopsis    [Returns TRUE if a generator is empty; FALSE otherwise.]
220
221  Description []
222
223  SideEffects [none]
224
225  SeeAlso     [Mc_FsmForEachScc Mc_FsmFirstScc Mc_FsmNextScc Mc_FsmSccGenFree]
226
227******************************************************************************/
228boolean
229Mc_FsmIsSccGenEmpty(
230  Mc_SccGen_t *gen)
231{
232  if (gen == NIL(Mc_SccGen_t)) return TRUE;
233  return gen->status == McSccGenEmpty_c;
234
235} /* Mc_FsmIsSccGenEmpty */
236
237
238/**Function********************************************************************
239
240  Synopsis    [Frees a SCC generator.]
241
242  Description [Frees a SCC generator.  Always returns FALSE, so that it
243  can be used in iterators.
244
245  leftover is an array_t of mdd_t *s.]
246
247  SideEffects [The sets of states in the heap are returned in leftover
248  if the array pointer is non-null.]
249
250  SeeAlso     [Mc_FsmForEachScc Mc_FsmFirstScc Mc_FsmNextScc
251  Mc_FsmIsSccGenEmpty]
252
253******************************************************************************/
254boolean
255Mc_FsmSccGenFree(
256  Mc_SccGen_t *gen,
257  array_t *leftover)   
258{
259  int linearStepMethod;
260
261  if (gen == NIL(Mc_SccGen_t)) return FALSE;
262  /* Print some stats. */
263  if (gen->verbosity == McVerbositySome_c || gen->verbosity == McVerbosityMax_c) {
264    fprintf(vis_stdout,
265            "--SCC: found %d fair SCC(s) out of %d examined\n",
266            gen->fairSccsFound, gen->totalExamined);
267    fprintf(vis_stdout,
268            "--SCC: %d image computations, %d preimage computations\n",
269            Img_GetNumberOfImageComputation(Img_Forward_c) - gen->nImgComps,
270            Img_GetNumberOfImageComputation(Img_Backward_c) - gen->nPreComps);
271  }
272  /* Create array from elements still on queue if so requested. */
273  linearStepMethod = GetSccEnumerationMethod();
274  if (linearStepMethod == 1) {
275    while (Heap_HeapCount(gen->heap)) {
276      gns_t *set;
277      long index;
278      int retval UNUSED = Heap_HeapExtractMin(gen->heap, &set, &index);
279      assert(retval);
280      if (leftover == NIL(array_t) || gen->earlyTermination == TRUE) {
281        mdd_free(set->states); 
282      } else {
283        array_insert_last(mdd_t *, leftover, set->states);
284      }
285      mdd_free(set->spine); mdd_free(set->node);
286      FREE(set);
287    }
288  }else {
289    while (Heap_HeapCount(gen->heap)) {
290      mdd_t *set;
291      long index;
292      int retval UNUSED = Heap_HeapExtractMin(gen->heap, &set, &index);
293      assert(retval);
294      if (leftover == NIL(array_t) || gen->earlyTermination == TRUE) {
295        mdd_free(set);
296      } else {
297        array_insert_last(mdd_t *, leftover, set);
298      }
299    }
300  }
301
302  Heap_HeapFree(gen->heap);
303  FREE(gen);
304  return FALSE;
305
306} /* Mc_FsmSccGenFree */
307
308
309/**Function********************************************************************
310
311  Synopsis    [Computes fair SCCs of an FSM.]
312
313  Description [Returns some fair SCCs of an FSM and the states on the
314  paths leading to them.  Parameter <code>maxNumberOfSCCs</code>
315  controls the enumeration.  If its value is 0, all fair SCCs are
316  enumerated; if it is negative, early termination is applied, and at
317  most one fair SCC is computed.  Finally, if
318  <code>maxNumberOfSCCs</code> is a positive integer <code>n</code>,
319  then exactly <code>n</code> fair SCCs are computed.]
320
321  SideEffects [Returns an array with one SCC per entry as side
322  effect. May update reachability information.]
323
324  SeeAlso     []
325
326******************************************************************************/
327mdd_t *
328McFsmComputeFairSCCsByLockStep(
329  Fsm_Fsm_t *fsm,
330  int maxNumberOfSCCs,
331  array_t *SCCs,
332  array_t *onionRingsArrayForDbg,
333  Mc_VerbosityLevel verbosity,
334  Mc_DcLevel dcLevel)
335{
336  Mc_SccGen_t *sccGen;
337  mdd_t *mddOne, *reached, *hull, *scc, *fairStates;
338  array_t *onionRings, *sccClosedSetArray, *careStatesArray;
339  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
340  int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
341  int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
342  Fsm_Fairness_t *modelFairness = Fsm_FsmReadFairnessConstraint(fsm);
343  array_t *buechiFairness = array_alloc(mdd_t *, 0);
344
345  /* Initialization. */
346  mddOne = mdd_one(mddManager);
347
348  sccClosedSetArray = array_alloc(mdd_t *, 0);
349  reached = Fsm_FsmComputeReachableStates(fsm, 0, verbosity, 0, 0, 1, 0, 0,
350                                          Fsm_Rch_Default_c, 0, 0,
351                                          NIL(array_t), FALSE, NIL(array_t));
352  array_insert_last(mdd_t *, sccClosedSetArray, reached);
353  onionRings = Fsm_FsmReadReachabilityOnionRings(fsm);
354
355  careStatesArray = array_alloc(mdd_t *, 0);
356  array_insert_last(mdd_t *, careStatesArray, reached);
357  Img_MinimizeTransitionRelation(Fsm_FsmReadOrCreateImageInfo(fsm, 1, 1),
358                                 careStatesArray, Img_DefaultMinimizeMethod_c,
359                                 Img_Both_c, FALSE);
360
361  /* Read fairness constraints. */
362  if (modelFairness != NIL(Fsm_Fairness_t)) {
363    if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
364      (void) fprintf(vis_stdout,
365               "** mc error: non-Buechi fairness constraints not supported\n");
366      array_free(buechiFairness);
367      return NIL(mdd_t);
368    } else {
369      int j;
370      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
371      for (j = 0; j < numBuchi; j++) {
372        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
373                                                        careStatesArray,
374                                                        dcLevel);
375        array_insert_last(mdd_t *, buechiFairness, tmpMdd);
376      }
377    }
378  } else {
379    array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
380  }
381
382  /* Enumerate the fair SCCs and accumulate their disjunction in hull. */
383  hull = mdd_zero(mddManager);
384  Mc_FsmForEachFairScc(fsm, sccGen, scc, sccClosedSetArray, NIL(array_t),
385                       buechiFairness, onionRings,
386                       maxNumberOfSCCs == MC_LOCKSTEP_EARLY_TERMINATION,
387                       verbosity, dcLevel) {
388    mdd_t *tmp = mdd_or(hull, scc, 1, 1);
389    mdd_free(hull);
390    hull = tmp;
391    array_insert_last(mdd_t *, SCCs, scc);
392    if (maxNumberOfSCCs > MC_LOCKSTEP_ALL_SCCS &&
393        array_n(SCCs) == maxNumberOfSCCs) {
394      Mc_FsmSccGenFree(sccGen, NIL(array_t));
395      break;
396    }
397  }
398
399  /* Compute (subset of) fair states and onion rings. */
400  if (onionRingsArrayForDbg != NIL(array_t)) {
401    mdd_t *fairSet;
402    int i;
403    fairStates = Mc_FsmEvaluateEUFormula(fsm, reached, hull,
404                                         NIL(mdd_t), mddOne, careStatesArray,
405                                         MC_NO_EARLY_TERMINATION,
406                                         NIL(array_t), Mc_None_c, NIL(array_t),
407                                         verbosity, dcLevel, NIL(boolean));
408    arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
409      mdd_t *restrictedFairSet = mdd_and(fairSet, hull, 1, 1);
410      array_t *setOfRings = array_alloc(mdd_t *, 0);
411      mdd_t *EU = Mc_FsmEvaluateEUFormula(fsm, fairStates, restrictedFairSet,
412                                          NIL(mdd_t), mddOne, careStatesArray,
413                                          MC_NO_EARLY_TERMINATION,
414                                          NIL(array_t), Mc_None_c, setOfRings,
415                                          verbosity, dcLevel, NIL(boolean));
416      array_insert_last(array_t *, onionRingsArrayForDbg, setOfRings);
417      mdd_free(restrictedFairSet);
418      mdd_free(EU);
419    }
420  } else {
421    fairStates = mdd_dup(hull);
422  }
423  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
424    fprintf(vis_stdout,
425            "--Fair States: %d image computations, %d preimage computations\n",
426            Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
427            Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
428  }
429
430  /* Clean up. */
431  array_free(sccClosedSetArray);
432  mdd_free(reached);
433  mdd_free(hull);
434  mdd_free(mddOne);
435  array_free(careStatesArray);
436  mdd_array_free(buechiFairness);
437  return fairStates;
438
439} /* McFsmComputeFairSCCsByLockStep */
440
441/**Function********************************************************************
442
443  Synopsis    [Computes fair SCCs of an FSM within SCC-closed sets.]
444
445  Description [Same as McFsmComputeFairSCCsByLockStep, except that the
446  fair SCCs returned are within the given array of SCC-closed sets.]
447
448
449  SideEffects [Returns an array with one SCC per entry as side
450  effect. May update reachability information.]
451
452  SeeAlso     [McFsmComputeFairSCCsByLockStep]
453
454******************************************************************************/
455mdd_t *
456McFsmRefineFairSCCsByLockStep(
457  Fsm_Fsm_t *fsm,
458  int maxNumberOfSCCs,
459  array_t *SCCs,
460  array_t *sccClosedSets,
461  array_t *careStates,
462  array_t *onionRingsArrayForDbg,
463  Mc_VerbosityLevel verbosity,
464  Mc_DcLevel dcLevel)
465{
466  Mc_SccGen_t *sccGen;
467  mdd_t *mddOne, *reached, *hull, *scc, *fairStates;
468  array_t *onionRings, *careStatesArray, *sccClosedSetArray;
469  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
470  int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
471  int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
472  Fsm_Fairness_t *modelFairness = Fsm_FsmReadFairnessConstraint(fsm);
473  array_t *buechiFairness = array_alloc(mdd_t *, 0);
474
475  /* Initialization. */
476  mddOne = mdd_one(mddManager);
477
478  if (careStates == NIL(array_t)) {
479    reached = Fsm_FsmComputeReachableStates(fsm, 0, verbosity, 0, 0, 1, 0, 0,
480                                            Fsm_Rch_Default_c, 0, 0,
481                                            NIL(array_t), FALSE, NIL(array_t));
482    careStatesArray = array_alloc(mdd_t *, 0);
483    array_insert_last(mdd_t *, careStatesArray, mdd_dup(reached));
484  }else {
485    reached = McMddArrayAnd(careStates);
486    careStatesArray = mdd_array_duplicate(careStates);
487  }
488
489  onionRings = Fsm_FsmReadReachabilityOnionRings(fsm);
490  if (onionRings == NIL(array_t)) {
491    onionRings = array_alloc(mdd_t *, 0);
492    array_insert_last(mdd_t *, onionRings, mdd_dup(mddOne));
493  }else
494    onionRings = mdd_array_duplicate(onionRings);
495
496  if (sccClosedSets == NIL(array_t)) {
497    sccClosedSetArray = array_alloc(mdd_t *, 0);
498    array_insert_last(mdd_t *, sccClosedSetArray, mdd_dup(reached));
499  }else {
500    if (careStates != NIL(array_t))
501      sccClosedSetArray = mdd_array_duplicate(sccClosedSets);
502    else {
503      mdd_t *mdd1, *mdd2;
504      int i;
505      sccClosedSetArray = array_alloc(mdd_t *, 0);
506      arrayForEachItem(mdd_t *, sccClosedSets, i, mdd1) {
507        mdd2 = mdd_and(mdd1, reached, 1, 1);
508        if (mdd_is_tautology(mdd2, 0)) 
509          mdd_free(mdd2);
510        else
511          array_insert_last(mdd_t *, sccClosedSetArray, mdd2);
512      }
513    }
514  }
515
516  Img_MinimizeTransitionRelation(Fsm_FsmReadOrCreateImageInfo(fsm, 1, 1),
517                                 careStatesArray, Img_DefaultMinimizeMethod_c,
518                                 Img_Both_c, FALSE);
519
520  /* Read fairness constraints. */
521  if (modelFairness != NIL(Fsm_Fairness_t)) {
522    if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
523      (void) fprintf(vis_stdout,
524               "** mc error: non-Buechi fairness constraints not supported\n");
525      array_free(buechiFairness);
526      mdd_array_free(sccClosedSetArray);
527      mdd_array_free(onionRings);
528      mdd_array_free(careStatesArray);
529      mdd_free(reached);
530      return NIL(mdd_t);
531    } else {
532      int j;
533      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
534      for (j = 0; j < numBuchi; j++) {
535        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
536                                                        careStatesArray,
537                                                        dcLevel);
538        array_insert_last(mdd_t *, buechiFairness, tmpMdd);
539      }
540    }
541  } else {
542    array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
543  }
544
545  /* Enumerate the fair SCCs and accumulate their disjunction in hull. */
546  hull = mdd_zero(mddManager);
547  Mc_FsmForEachFairScc(fsm, sccGen, scc, sccClosedSetArray, NIL(array_t),
548                       buechiFairness, onionRings,
549                       maxNumberOfSCCs == MC_LOCKSTEP_EARLY_TERMINATION,
550                       verbosity, dcLevel) {
551    mdd_t *tmp = mdd_or(hull, scc, 1, 1);
552    mdd_free(hull);
553    hull = tmp;
554    array_insert_last(mdd_t *, SCCs, scc);
555    if (maxNumberOfSCCs > MC_LOCKSTEP_ALL_SCCS &&
556        array_n(SCCs) == maxNumberOfSCCs) {
557      Mc_FsmSccGenFree(sccGen, NIL(array_t));
558      break;
559    }
560  }
561
562  /* Compute (subset of) fair states and onion rings. */
563  if (onionRingsArrayForDbg != NIL(array_t)) {
564    mdd_t *fairSet;
565    int i;
566    fairStates = Mc_FsmEvaluateEUFormula(fsm, reached, hull,
567                                         NIL(mdd_t), mddOne, careStatesArray,
568                                         MC_NO_EARLY_TERMINATION,
569                                         NIL(array_t), Mc_None_c, NIL(array_t),
570                                         verbosity, dcLevel, NIL(boolean));
571    arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
572      mdd_t *restrictedFairSet = mdd_and(fairSet, hull, 1, 1);
573      array_t *setOfRings = array_alloc(mdd_t *, 0);
574      mdd_t *EU = Mc_FsmEvaluateEUFormula(fsm, fairStates, restrictedFairSet,
575                                          NIL(mdd_t), mddOne, careStatesArray,
576                                          MC_NO_EARLY_TERMINATION,
577                                          NIL(array_t), Mc_None_c, setOfRings,
578                                          verbosity, dcLevel, NIL(boolean));
579      array_insert_last(array_t *, onionRingsArrayForDbg, setOfRings);
580      mdd_free(restrictedFairSet);
581      mdd_free(EU);
582    }
583  } else {
584    fairStates = mdd_dup(hull);
585  }
586  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
587    fprintf(vis_stdout,
588            "--Fair States: %d image computations, %d preimage computations\n",
589            Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
590            Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
591  }
592
593  /* Clean up. */
594  mdd_array_free(sccClosedSetArray);
595  mdd_free(reached);
596  mdd_free(hull);
597  mdd_free(mddOne);
598  mdd_array_free(careStatesArray);
599  mdd_array_free(buechiFairness);
600  return fairStates;
601
602} /* McFsmRefineFairSCCsByLockStep */
603
604
605/**Function********************************************************************
606
607  Synopsis    [Computes one fair SCC of an FSM, by LinearStep.]
608
609  Description [Computes one fair SCC of the state transition graph of
610  an FSM.  Returns the fair SCC if one exists; NULL otherwise.  This
611  function uses the linear steps SCC enumeration algorithm of
612  Gentilini, Piazza, and Policriti, "Computing strongly connected
613  components in a linear number of symbolic steps," and with the
614  addition of an early termination test.<p>
615
616  On input, the heap is supposed to contain a set of SCC-closed state
617  sets together with their spine-sets.  If earlyTermination is
618  requested, the heap is left in an inconsistent state; otherwise, it
619  contains a set of SCC-closed sets that contains all fair SCCs that
620  were on the heap on input, except the one that has been enumerated.
621  The number of sets may be different, and some non-fair SCCs may no
622  longer be present.<p>
623
624  The onionRing parameter is an array of state sets that is used to
625  pick a seed close to a target.  Typically, these onion rings come
626  from reachability analysis.  The target states in this case are the
627  initial states of the FSM, and the objective of choosing a seed
628  close to them is to reduce the length of the stem of a
629  counterexample in the language emptiness check.  However, any
630  collection of sets that together cover all the states on the heap
631  will work.  If one is not concerned with a specific target, but
632  rather with speed, then passing an array with just one component set
633  to the constant one is preferable.]
634
635  SideEffects [Updates the priority queue. The number of SCC examined
636  (i.e., the number of chosen seeds) is added to sccExamined.]
637
638  SeeAlso     [Mc_FsmForEachFairScc]
639
640******************************************************************************/
641mdd_t *
642McFsmComputeOneFairSccByLinearStep( 
643  Fsm_Fsm_t *fsm,
644  Heap_t *priorityQueue,
645  array_t *buechiFairness,
646  array_t *onionRings,
647  boolean earlyTermination,
648  Mc_VerbosityLevel verbosity,
649  Mc_DcLevel dcLevel,
650  int *sccExamined)
651{
652  mdd_t *mddOne, *SCC = NIL(mdd_t);
653  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
654  int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
655  int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
656  array_t *careStatesArray = array_alloc(mdd_t *, 0);
657  int totalSCCs = 0;
658  boolean foundScc = FALSE;
659  array_t *activeFairness = NIL(array_t);
660  int firstActive = 0;
661  gns_t *gns;
662
663  /* Initialization. */
664  mddOne = mdd_one(mddManager);
665  array_insert(mdd_t *, careStatesArray, 0, mddOne); 
666
667  while (Heap_HeapCount(priorityQueue)) {
668    mdd_t *V, *F, *fFront, *bFront, *fairSet;
669    mdd_t *S, *NODE, *newS, *newNODE, *preNODE;
670    long ringIndex;
671    int retval UNUSED = Heap_HeapExtractMin(priorityQueue, &gns, 
672                                            &ringIndex);
673    assert(retval && ringIndex < array_n(onionRings));
674
675    /* Extract the SCC-closed set, together with its spine-set */
676    V = gns->states;
677    S = gns->spine;
678    NODE = gns->node;
679    FREE(gns);
680
681    /* Determine the seed for which the SCC is computed */
682    if (mdd_is_tautology(S, 0) ) {
683      assert( mdd_is_tautology(NODE, 0) );
684      mdd_free(NODE);
685      NODE = LockstepPickSeed(fsm, V, buechiFairness, onionRings, ringIndex);
686    } 
687
688    if (earlyTermination == TRUE) {
689      int i;
690      activeFairness = array_alloc(mdd_t *, 0);
691      for (i = 0; i < array_n(buechiFairness); i++) {
692        mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i);
693        if (!mdd_lequal(NODE, fairSet, 1, 1)) {
694          array_insert_last(mdd_t *, activeFairness, fairSet);
695        }
696      }
697    }
698   
699    /* Compute the forward-set of seed, together with a new spine-set */
700    {
701      array_t *newCareStatesArray = array_alloc(mdd_t *, 0);
702      array_t *stack = array_alloc(mdd_t *, 0);
703      mdd_t   *tempMdd, *tempMdd2;
704      int i;
705      /* (1) Compute the forward-set, and push it onto STACK */
706      F = mdd_zero(mddManager);
707      fFront = mdd_dup(NODE);
708      while (!mdd_is_tautology(fFront, 0)) {
709        array_insert_last(mdd_t *, stack, mdd_dup(fFront));
710
711        tempMdd = F;
712        F = mdd_or(F, fFront, 1, 1);
713        mdd_free(tempMdd);
714
715        tempMdd = Mc_FsmEvaluateEYFormula(fsm, fFront, mddOne, careStatesArray,
716                                          verbosity, dcLevel);
717        mdd_free(fFront);
718        tempMdd2 = mdd_and(tempMdd, V, 1, 1);
719        mdd_free(tempMdd);
720        fFront = mdd_and(tempMdd2, F, 1, 0);
721        mdd_free(tempMdd2);
722      }
723      mdd_free(fFront);
724      /* (2) Determine a spine-set of the forward-set */
725      i = array_n(stack) - 1;
726      fFront = array_fetch(mdd_t *, stack, i);
727      newNODE = Mc_ComputeAState(fFront, fsm);
728      mdd_free(fFront);
729
730      newS = mdd_dup(newNODE);
731      while (i > 0) {
732        fFront = array_fetch(mdd_t *, stack, --i);
733        /* Chao: The use of DCs here may slow down the computation,
734         *       even though it reduces the peak BDD size
735         */
736        /* array_insert(mdd_t *, newCareStatesArray, 0, fFront); */
737        array_insert(mdd_t *, newCareStatesArray, 0, mddOne);
738        tempMdd = Mc_FsmEvaluateEXFormula(fsm, newS, mddOne, newCareStatesArray,
739                                          verbosity, dcLevel);
740        tempMdd2 = mdd_and(tempMdd, fFront, 1, 1);
741        mdd_free(tempMdd);
742        mdd_free(fFront);
743       
744        tempMdd = Mc_ComputeAState(tempMdd2, fsm);
745        mdd_free(tempMdd2);
746
747        tempMdd2 = newS;
748        newS = mdd_or(newS, tempMdd, 1, 1);
749        mdd_free(tempMdd2);
750        mdd_free(tempMdd);
751      }
752      array_free(stack);
753      array_free(newCareStatesArray);
754    }
755    /* now, we have {F, newS, newNODE} */
756   
757    /* Determine the SCC containing NODE */
758    SCC    = mdd_dup(NODE);
759    bFront = mdd_dup(NODE);
760    while (1) {
761      mdd_t   *tempMdd, *tempMdd2;
762
763      if (earlyTermination == TRUE) {
764        mdd_t * meet = mdd_and(SCC, NODE, 1, 0);
765        if (!mdd_is_tautology(meet, 0)) {
766          assert(mdd_lequal(meet, V, 1, 1));
767          for ( ; firstActive < array_n(activeFairness); firstActive++) {
768            mdd_t *fairSet = array_fetch(mdd_t *, activeFairness, firstActive);
769            if (mdd_lequal(meet, fairSet, 1, 0)) break;
770          }
771          mdd_free(meet);
772          if (firstActive == array_n(activeFairness)) {
773            int i;
774            (void) fprintf(vis_stdout, "EARLY TERMINATION!\n");
775            totalSCCs++;
776            /* Trim fair sets to guarantee counterexample will go through
777             * this SCC.
778             */
779            for (i = 0; i < array_n(buechiFairness); i++) {
780              mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i);
781              mdd_t *trimmed = mdd_and(fairSet, SCC, 1, 1);
782              mdd_free(fairSet);
783              array_insert(mdd_t *, buechiFairness, i, trimmed);
784            }
785            mdd_free(bFront);
786            mdd_free(F);
787            mdd_free(V); 
788            mdd_free(S); 
789            mdd_free(NODE);
790            mdd_free(newS);
791            mdd_free(newNODE);
792            array_free(activeFairness);
793
794            foundScc = TRUE;
795            goto cleanUp;
796          }
797        }
798        mdd_free(meet);
799      }
800
801      tempMdd = Mc_FsmEvaluateEXFormula(fsm, bFront, mddOne, careStatesArray,
802                                        verbosity, dcLevel);
803      tempMdd2 = mdd_and(tempMdd, F, 1, 1);
804      mdd_free(tempMdd);
805     
806      tempMdd = bFront;
807      bFront = mdd_and(tempMdd2, SCC, 1, 0);
808      mdd_free(tempMdd2);
809      mdd_free(tempMdd);
810      if (mdd_is_tautology(bFront, 0))  break;
811
812      tempMdd = SCC;
813      SCC = mdd_or(SCC, bFront, 1, 1);
814      mdd_free(tempMdd);
815    }
816    mdd_free(bFront);
817
818    totalSCCs++;
819    preNODE = Mc_FsmEvaluateEYFormula(fsm, NODE, mddOne, careStatesArray,
820                                    verbosity, dcLevel);
821     
822    /* Check for fairness. If SCC is a trival SCC, skip the check */
823    if ( !mdd_equal(SCC, NODE) ||  mdd_lequal(NODE, preNODE, 1, 1) ) {
824      /* Check fairness constraints. */
825      int i;
826      arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
827        if (mdd_lequal(SCC, fairSet, 1, 0)) break;
828      }
829      if (i == array_n(buechiFairness)) {
830        /* All fairness iconditions intersected.  We have a fair SCC. */
831        if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
832          array_t *PSvars = Fsm_FsmReadPresentStateVars(fsm);
833          fprintf(vis_stdout, "--linearSCC: found a fair SCC with %.0f states\n",
834                  mdd_count_onset(mddManager, SCC, PSvars));
835          /* (void) bdd_print_minterm(SCC); */
836        }
837        foundScc = TRUE;
838      }
839    }
840    mdd_free(preNODE);
841    mdd_free(NODE);
842
843    /* Divide the remaining states of V into V minus
844     * the forward set F, and the rest (minus the fair SCC).  Add the two
845     * sets thus obtained to the priority queue. */
846    {
847      mdd_t *V1, *S1, *NODE1;
848      mdd_t *tempMdd, *tempMdd2;
849
850      V1 = mdd_and(V, F, 1, 0);
851      S1 = mdd_and(S, SCC, 1, 0);
852      tempMdd = mdd_and(SCC, S, 1, 1);
853      tempMdd2 = Mc_FsmEvaluateEXFormula(fsm, tempMdd, mddOne, 
854                                         careStatesArray,
855                                         verbosity, dcLevel);
856      mdd_free(tempMdd);
857      NODE1 = mdd_and(tempMdd2, S1, 1, 1);
858      mdd_free(tempMdd2);
859      LinearstepQueueEnqueue(fsm, priorityQueue, V1, S1, NODE1, 
860                             onionRings, McLS_G_c,
861                             buechiFairness, verbosity, dcLevel);
862
863      V1 = mdd_and(F, SCC, 1, 0);
864      S1 = mdd_and(newS, SCC, 1, 0);
865      NODE1 = mdd_and(newNODE, SCC, 1, 0);
866      LinearstepQueueEnqueue(fsm, priorityQueue, V1, S1, NODE1,
867                             onionRings, McLS_H_c,
868                             buechiFairness, verbosity, dcLevel);
869    }
870    mdd_free(F);
871    mdd_free(V);
872    mdd_free(S);
873    mdd_free(newS);
874    mdd_free(newNODE);
875   
876    if (foundScc == TRUE) break;
877    mdd_free(SCC);
878  }
879
880cleanUp:
881  mdd_free(mddOne);
882  array_free(careStatesArray);
883  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
884    fprintf(vis_stdout,
885            "--linearSCC: found %s fair SCC out of %d examined\n",
886            foundScc ? "one" : "no", totalSCCs);
887    fprintf(vis_stdout,
888            "--linearSCC: %d image computations, %d preimage computations\n",
889            Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
890            Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
891  }
892  *sccExamined += totalSCCs;
893  return foundScc ? SCC : NIL(mdd_t);
894
895} /* McFsmComputeOneFairSccByLinearStep */
896
897
898/**Function********************************************************************
899
900  Synopsis    [Computes one fair SCC of an FSM, by LockStep.]
901
902  Description [Computes one fair SCC of the state transition graph of
903  an FSM.  Returns the fair SCC if one exists; NULL otherwise.  This
904  function uses the lockstep SCC enumeration algorithm of Bloem,
905  Gabow, and Somenzi (FMCAD'00) implemented as described in Ravi,
906  Bloem, and Somenzi (FMCAD'00), and with the addition of an early
907  termination test.<p>
908
909  On input, the heap is supposed to contain a set of SCC-closed state
910  sets.  If earlyTermination is requested, the heap is left in an
911  inconsistent state; otherwise, it contains a set of SCC-closed sets
912  that contains all fair SCCs that were on the heap on input except
913  the one that has been enumerated.  The number of sets may be
914  different, and some non-fair SCCs may no longer be present.<p>
915
916  The onionRing parameter is an array of state sets that is used to
917  pick a seed close to a target.  Typically, these onion rings come
918  from reachability analysis.  The target states in this case are the
919  initial states of the FSM, and the objective of choosing a seed
920  close to them is to reduce the length of the stem of a
921  counterexample in the language emptiness check.  However, any
922  collection of sets that together cover all the states on the heap
923  will work.  If one is not concerned with a specific target, but
924  rather with speed, then passing an array with just one component set
925  to the constant one is preferable.]
926
927  SideEffects [Updates the priority queue. The number of SCC examined
928  (i.e., the number of chosen seeds) is added to sccExamined.]
929
930  SeeAlso     [Mc_FsmForEachFairScc]
931
932******************************************************************************/
933mdd_t *
934McFsmComputeOneFairSccByLockStep(
935  Fsm_Fsm_t *fsm,
936  Heap_t *priorityQueue,
937  array_t *buechiFairness,
938  array_t *onionRings,
939  boolean earlyTermination,
940  Mc_VerbosityLevel verbosity,
941  Mc_DcLevel dcLevel,
942  int *sccExamined)
943{
944  mdd_t *mddOne, *SCC = NIL(mdd_t);
945  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
946  int nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
947  int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
948  array_t *careStatesArray = array_alloc(mdd_t *, 0);
949  int totalSCCs = 0;
950  boolean foundScc = FALSE;
951  array_t *activeFairness = NIL(array_t);
952  int firstActive = 0;
953
954  /* Initialization. */
955  mddOne = mdd_one(mddManager);
956  array_insert(mdd_t *, careStatesArray, 0, mddOne); 
957
958  while (Heap_HeapCount(priorityQueue)) {
959    mdd_t *V, *seed, *B, *F, *fFront, *bFront, *fairSet;
960    mdd_t *converged, *first, *second;
961    long ringIndex;
962    McLockstepMode firstMode, secondMode;
963    int retval UNUSED = Heap_HeapExtractMin(priorityQueue, &V, &ringIndex);
964    assert(retval && ringIndex < array_n(onionRings));
965    /* Here, V contains at least one nontrivial SCC. We then choose the
966     * seed for a new SCC, which may turn out to be trivial. */
967    seed = LockstepPickSeed(fsm, V, buechiFairness, onionRings, ringIndex);
968
969    if (earlyTermination == TRUE) {
970      int i;
971      activeFairness = array_alloc(mdd_t *, 0);
972      for (i = 0; i < array_n(buechiFairness); i++) {
973        mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i);
974        if (!mdd_lequal(seed, fairSet, 1, 1)) {
975          array_insert_last(mdd_t *, activeFairness, fairSet);
976        }
977      }
978    }
979
980    /* Do lockstep search from seed.  Leave the seed initially out of
981     * F and B to facilitate the detection of trivial SCCs.  Intersect
982     * all results with V so that we can simplify the transition
983     * relation. */
984    fFront = Mc_FsmEvaluateEYFormula(fsm, seed, mddOne, careStatesArray,
985                                     verbosity, dcLevel);
986    F = mdd_and(fFront, V, 1, 1);
987    mdd_free(fFront);
988    fFront = mdd_dup(F);
989    bFront = Mc_FsmEvaluateEXFormula(fsm, seed, mddOne, careStatesArray,
990                                     verbosity, dcLevel);
991    B = mdd_and(bFront, V , 1, 1);
992    mdd_free(bFront);
993    bFront = mdd_dup(B);
994    /* Go until the fastest search converges. */
995    while (!(mdd_is_tautology(fFront, 0) || mdd_is_tautology(bFront, 0))) {
996      mdd_t *tmp;
997
998      /* If the intersection of F and B intersects all fairness
999       * constraints the union of F and B contains at least one fair
1000       * SCC.  Since the intersection of F and B is monotonically
1001       * non-decreasing, once a fair set has been intersected, there
1002       * is no need to check for it any more. */
1003      if (earlyTermination == TRUE) {
1004        mdd_t * meet = mdd_and(F, B, 1, 1);
1005        if (!mdd_is_tautology(meet, 0)) {
1006          assert(mdd_lequal(meet, V, 1, 1));
1007          for ( ; firstActive < array_n(activeFairness); firstActive++) {
1008            mdd_t *fairSet = array_fetch(mdd_t *, activeFairness, firstActive);
1009            if (mdd_lequal(meet, fairSet, 1, 0)) break;
1010          }
1011          if (firstActive == array_n(activeFairness)) {
1012            int i;
1013            (void) fprintf(vis_stdout, "EARLY TERMINATION!\n");
1014            totalSCCs++;
1015            /* A fair SCC is contained in the union of F, B, and seed. */
1016            tmp = mdd_or(F, B, 1, 1);
1017            SCC = mdd_or(tmp, seed, 1, 1);
1018            mdd_free(tmp);
1019            /* Trim fair sets to guarantee counterexample will go through
1020             * this SCC. */
1021            tmp = mdd_or(meet, seed, 1, 1);
1022            mdd_free(meet);
1023            meet = tmp;
1024            for (i = 0; i < array_n(buechiFairness); i++) {
1025              mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, i);
1026              mdd_t *trimmed = mdd_and(fairSet, meet, 1, 1);
1027              mdd_free(fairSet);
1028              array_insert(mdd_t *, buechiFairness, i, trimmed);
1029            }
1030            mdd_free(meet);
1031            mdd_free(F); mdd_free(B);
1032            mdd_free(fFront); mdd_free(bFront);
1033            mdd_free(seed); mdd_free(V);
1034            foundScc = TRUE;
1035            array_free(activeFairness);
1036            goto cleanUp;
1037          }
1038        }
1039        mdd_free(meet);
1040      }
1041
1042      /* Forward step. */
1043      tmp = Mc_FsmEvaluateEYFormula(fsm, fFront, mddOne, careStatesArray,
1044                                    verbosity, dcLevel);
1045      mdd_free(fFront);
1046      fFront = mdd_and(tmp, F, 1, 0);
1047      mdd_free(tmp);
1048      tmp = mdd_and(fFront, V, 1, 1);
1049      mdd_free(fFront);
1050      fFront = tmp;
1051      if (mdd_is_tautology(fFront, 0)) break;
1052      tmp = mdd_or(F, fFront, 1, 1);
1053      mdd_free(F);
1054      F = tmp;
1055      /* Backward step. */
1056      tmp = Mc_FsmEvaluateEXFormula(fsm, bFront, mddOne, careStatesArray,
1057                                    verbosity, dcLevel);
1058      mdd_free(bFront);
1059      bFront = mdd_and(tmp, B, 1, 0);
1060      mdd_free(tmp);
1061      tmp = mdd_and(bFront, V, 1, 1);
1062      mdd_free(bFront);
1063      bFront = tmp;
1064      tmp = mdd_or(B, bFront, 1, 1);
1065      mdd_free(B);
1066      B = tmp;
1067    }
1068    /* Complete the slower search within the converged one. */
1069    if (mdd_is_tautology(fFront, 0)) {
1070      /* Forward search converged. */
1071      mdd_t *tmp = mdd_and(bFront, F, 1, 1);
1072      mdd_free(bFront);
1073      bFront = tmp;
1074      mdd_free(fFront);
1075      converged = mdd_dup(F);
1076      /* The two sets to be enqueued come from a set that has been
1077       * already trimmed.  Hence, we want to remove the trivial SCCs
1078       * left exposed at the rearguard of F, and the trivial SCCs left
1079       * exposed at the vanguard of B. */
1080      firstMode = McLS_H_c;
1081      secondMode = McLS_G_c;
1082      while (!mdd_is_tautology(bFront, 0)) {
1083        tmp =  Mc_FsmEvaluateEXFormula(fsm, bFront, mddOne,
1084                                       careStatesArray, verbosity, dcLevel);
1085        mdd_free(bFront);
1086        bFront = mdd_and(tmp, B, 1, 0);
1087        mdd_free(tmp);
1088        tmp = mdd_and(bFront, converged, 1, 1);
1089        mdd_free(bFront);
1090        bFront = tmp;
1091        tmp = mdd_or(B, bFront, 1, 1);
1092        mdd_free(B);
1093        B = tmp;
1094      }
1095      mdd_free(bFront);
1096    } else {
1097      /* Backward search converged. */
1098      mdd_t *tmp = mdd_and(fFront, B, 1, 1);
1099      mdd_free(fFront);
1100      fFront = tmp;
1101      mdd_free(bFront);
1102      converged = mdd_dup(B);
1103      firstMode = McLS_G_c;
1104      secondMode = McLS_H_c;
1105      while (!mdd_is_tautology(fFront, 0)) {
1106        tmp =  Mc_FsmEvaluateEYFormula(fsm, fFront, mddOne,
1107                                       careStatesArray, verbosity, dcLevel);
1108        mdd_free(fFront);
1109        fFront = mdd_and(tmp, F, 1 ,0);
1110        mdd_free(tmp);
1111        tmp = mdd_and(fFront, converged, 1, 1);
1112        mdd_free(fFront);
1113        fFront = tmp;
1114        tmp = mdd_or(F, fFront, 1, 1);
1115        mdd_free(F);
1116        F = tmp;
1117      }
1118      mdd_free(fFront);
1119    }
1120
1121    totalSCCs++;
1122    SCC = mdd_and(F, B, 1, 1);
1123    mdd_free(F);
1124    mdd_free(B);
1125    /* Check for fairness.  If SCC is the empty set we know that seed
1126     * is a trivial strong component; hence, it is not fair. */
1127    if (mdd_is_tautology(SCC, 0)) {
1128      mdd_t *tmp = mdd_or(converged, seed, 1, 1);
1129      mdd_free(converged);
1130      converged = tmp;
1131      mdd_free(SCC);
1132      SCC = mdd_dup(seed);
1133    } else {
1134      /* Check fairness constraints. */
1135      int i;
1136      arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
1137        if (mdd_lequal(SCC, fairSet, 1, 0)) break;
1138      }
1139      if (i == array_n(buechiFairness)) {
1140        /* All fairness conditions intersected.  We have a fair SCC. */
1141        if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
1142          array_t *PSvars = Fsm_FsmReadPresentStateVars(fsm);
1143          fprintf(vis_stdout, "--SCC: found a fair SCC with %.0f states\n",
1144                  mdd_count_onset(mddManager, SCC, PSvars));
1145          /* (void) bdd_print_minterm(SCC); */
1146        }
1147        foundScc = TRUE;
1148      }
1149    }
1150    /* Divide the remaining states of V into the converged set minus
1151     * the fair SCC, and the rest (minus the fair SCC).  Add the two
1152     * sets thus obtained to the priority queue. */
1153    mdd_free(seed);
1154    first = mdd_and(converged, SCC, 1, 0);
1155    LockstepQueueEnqueue(fsm, priorityQueue, first, onionRings, firstMode,
1156                         buechiFairness, verbosity, dcLevel);
1157    second = mdd_and(V, converged, 1, 0);
1158    mdd_free(converged);
1159    mdd_free(V);
1160    LockstepQueueEnqueue(fsm, priorityQueue, second, onionRings, secondMode,
1161                         buechiFairness, verbosity, dcLevel);
1162    if (earlyTermination == TRUE) {
1163      array_free(activeFairness);
1164    }
1165    if (foundScc == TRUE) break;
1166    mdd_free(SCC);
1167  }
1168
1169cleanUp:
1170  mdd_free(mddOne);
1171  array_free(careStatesArray);
1172  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
1173    fprintf(vis_stdout,
1174            "--SCC: found %s fair SCC out of %d examined\n",
1175            foundScc ? "one" : "no", totalSCCs);
1176    fprintf(vis_stdout,
1177            "--SCC: %d image computations, %d preimage computations\n",
1178            Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
1179            Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
1180  }
1181  *sccExamined += totalSCCs;
1182  return foundScc ? SCC : NIL(mdd_t);
1183
1184} /* McFsmComputeOneFairSccByLockStep */
1185
1186
1187/*---------------------------------------------------------------------------*/
1188/* Definition of internal functions                                          */
1189/*---------------------------------------------------------------------------*/
1190
1191
1192/*---------------------------------------------------------------------------*/
1193/* Definition of static functions                                            */
1194/*---------------------------------------------------------------------------*/
1195
1196
1197/**Function********************************************************************
1198
1199  Synopsis    [Returns a seed state for lockstep search.]
1200
1201  Description [Returns a seed state for lockstep search, or NULL in
1202  case of failure.  The strategy is to first find the innermost ring
1203  that intersects the given set of states (V) and one fairness
1204  constraint.  The other fairness constraints are then checked to
1205  increase the number of fairness constraints that are satisfied by
1206  the seed.  The search is greedy.]
1207
1208  SideEffects [none]
1209
1210  SeeAlso     [McFsmComputeOneFairSccByLockStep]
1211
1212******************************************************************************/
1213static mdd_t *
1214LockstepPickSeed(
1215  Fsm_Fsm_t *fsm,
1216  mdd_t *V,
1217  array_t *buechiFairness,
1218  array_t *onionRings,
1219  int ringIndex)
1220{
1221  mdd_t *seed;
1222  int i, j;
1223
1224  /* We know that there is at least one state in V from each fairness
1225   * constraint. */
1226  for (i = ringIndex; i < array_n(onionRings); i++) {
1227    mdd_t *ring = array_fetch(mdd_t *, onionRings, i);
1228    for (j = 0; j < array_n(buechiFairness); j++) {
1229      mdd_t *fairSet = array_fetch(mdd_t *, buechiFairness, j);
1230      if (!mdd_lequal_mod_care_set(ring, fairSet, 1, 0, V)) {
1231        mdd_t *tmp = mdd_and(V, ring, 1, 1);
1232        mdd_t *candidates = mdd_and(tmp, fairSet, 1, 1);
1233        mdd_free(tmp);
1234        for (j++; j < array_n(buechiFairness); j++) {
1235          fairSet = array_fetch(mdd_t *, buechiFairness, j);
1236          if (!mdd_lequal(candidates, fairSet, 1, 0)) {
1237            tmp = mdd_and(candidates, fairSet, 1, 1);
1238            mdd_free(candidates);
1239            candidates = tmp;
1240          }
1241        }
1242        seed = Mc_ComputeAState(candidates, fsm);
1243        mdd_free(candidates);
1244        return seed;
1245      }
1246    }
1247  }
1248
1249  assert(FALSE);                /* we should never get here */
1250  return NIL(bdd_t);
1251
1252} /* LockstepPickSeed */
1253
1254
1255/**Function********************************************************************
1256
1257  Synopsis    [Adds a set of states to the priority queue of the lockstep
1258  algorithm.]
1259
1260  Description [Given a set of states, applies trimming as specified by
1261  mode.  Checks then if the trimmed set may contain a fair SCC, in
1262  which case it adds the set to the priority queue.]
1263
1264  SideEffects [May change the set of states as a result of trimming.
1265  The old set of states is freed.]
1266
1267  SeeAlso     [McFsmComputeOneFairSccByLockStep]
1268
1269******************************************************************************/
1270static void
1271LockstepQueueEnqueue(
1272  Fsm_Fsm_t *fsm,
1273  Heap_t *queue,
1274  mdd_t *states,
1275  array_t *onionRings,
1276  McLockstepMode mode,
1277  array_t *buechiFairness,
1278  Mc_VerbosityLevel verbosity,
1279  Mc_DcLevel dcLevel)
1280{
1281  mdd_t *fairSet, *ring;
1282  int i;
1283  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
1284  mdd_t *mddOne = mdd_one(mddManager);
1285  array_t *careStatesArray = array_alloc(mdd_t *, 0);
1286  array_insert_last(mdd_t *, careStatesArray, mddOne);
1287
1288#ifndef SCC_NO_TRIM
1289  if (mode == McLS_G_c || mode == McLS_GH_c) {
1290    mdd_t *trimmed = Mc_FsmEvaluateEGFormula(fsm, states, NIL(mdd_t), mddOne,
1291                                             NIL(Fsm_Fairness_t),
1292                                             careStatesArray,
1293                                             MC_NO_EARLY_TERMINATION,
1294                                             NIL(array_t),
1295                                             Mc_None_c, NIL(array_t *),
1296                                             verbosity, dcLevel, NIL(boolean),
1297                                             McGSH_EL_c);
1298    mdd_free(states);
1299    states = trimmed;
1300  }
1301  if (mode == McLS_H_c || mode == McLS_GH_c) {
1302    mdd_t *trimmed = Mc_FsmEvaluateEHFormula(fsm, states, NIL(mdd_t), mddOne,
1303                                             NIL(Fsm_Fairness_t),
1304                                             careStatesArray,
1305                                             MC_NO_EARLY_TERMINATION,
1306                                             NIL(array_t),
1307                                             Mc_None_c, NIL(array_t *),
1308                                             verbosity, dcLevel, NIL(boolean),
1309                                             McGSH_EL_c);
1310    mdd_free(states);
1311    states = trimmed;
1312  }
1313#endif
1314
1315  mdd_free(mddOne);
1316  array_free(careStatesArray);
1317  if (mode == McLS_none_c) {
1318    mdd_t *range = mdd_range_mdd(mddManager, Fsm_FsmReadPresentStateVars(fsm));
1319    mdd_t *valid = mdd_and(states, range, 1, 1);
1320    mdd_free(range);
1321    mdd_free(states);
1322    states = valid;
1323  }
1324  /* Discard set of states if it does not intersect all fairness conditions. */
1325  arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
1326    if (mdd_lequal(states, fairSet, 1, 0)) {
1327      mdd_free(states);
1328      return;
1329    }
1330  }
1331  /* Find the innermost onion ring intersecting the set of states.
1332   * Its index is the priority of the set. */
1333  arrayForEachItem(mdd_t *, onionRings, i, ring) {
1334    if (!mdd_lequal(states, ring, 1, 0)) break;
1335  }
1336  assert(i < array_n(onionRings));
1337  Heap_HeapInsert(queue,states,i);
1338  return;
1339
1340} /* LockstepQueueEnqueue */
1341
1342
1343/**Function********************************************************************
1344
1345  Synopsis    [Adds a set of states to the priority queue of the lockstep
1346  algorithm.]
1347
1348  Description [Given a set of states, applies trimming as specified by
1349  mode.  Checks then if the trimmed set may contain a fair SCC, in
1350  which case it adds the set to the priority queue.]
1351
1352  SideEffects [May change the set of states as a result of trimming.
1353  The old set of states is freed.]
1354
1355  SeeAlso     [McFsmComputeOneFairSccByLockStep]
1356
1357******************************************************************************/
1358static void
1359LinearstepQueueEnqueue(
1360  Fsm_Fsm_t *fsm,
1361  Heap_t *queue,
1362  mdd_t *states,
1363  mdd_t *spine,
1364  mdd_t *node,
1365  array_t *onionRings,
1366  McLockstepMode mode,
1367  array_t *buechiFairness,
1368  Mc_VerbosityLevel verbosity,
1369  Mc_DcLevel dcLevel)
1370{
1371  mdd_t *fairSet, *ring;
1372  mdd_t *tmp, *tmp1;
1373  int   i;
1374  gns_t *gns;
1375  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
1376  mdd_t *mddOne = mdd_one(mddManager);
1377  array_t *careStatesArray = array_alloc(mdd_t *, 0);
1378  array_insert_last(mdd_t *, careStatesArray, mddOne);
1379
1380#ifndef SCC_NO_TRIM
1381  if (mode == McLS_G_c || mode == McLS_GH_c) {
1382    mdd_t *trimmed = Mc_FsmEvaluateEGFormula(fsm, states, NIL(mdd_t), mddOne,
1383                                             NIL(Fsm_Fairness_t),
1384                                             careStatesArray,
1385                                             MC_NO_EARLY_TERMINATION,
1386                                             NIL(array_t),
1387                                             Mc_None_c, NIL(array_t *),
1388                                             verbosity, dcLevel, NIL(boolean),
1389                                             McGSH_EL_c);
1390    mdd_free(states);
1391    states = trimmed;
1392  }
1393  if (mode == McLS_H_c || mode == McLS_GH_c) {
1394    mdd_t *trimmed = Mc_FsmEvaluateEHFormula(fsm, states, NIL(mdd_t), mddOne,
1395                                             NIL(Fsm_Fairness_t),
1396                                             careStatesArray,
1397                                             MC_NO_EARLY_TERMINATION,
1398                                             NIL(array_t),
1399                                             Mc_None_c, NIL(array_t *),
1400                                             verbosity, dcLevel, NIL(boolean),
1401                                             McGSH_EL_c);
1402    mdd_free(states);
1403    states = trimmed;
1404  }
1405#endif
1406
1407  if (mode == McLS_none_c) {
1408    mdd_t *range = mdd_range_mdd(mddManager, Fsm_FsmReadPresentStateVars(fsm));
1409    mdd_t *valid = mdd_and(states, range, 1, 1);
1410    mdd_free(range);
1411    mdd_free(states);
1412    states = valid;
1413  }
1414  /* Discard set of states if it does not intersect all fairness conditions. */
1415  arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
1416    if (mdd_lequal(states, fairSet, 1, 0)) {
1417      mdd_free(states);
1418      mdd_free(mddOne);
1419      array_free(careStatesArray);
1420      return;
1421    }
1422  }
1423  /* Find the innermost onion ring intersecting the set of states.
1424   * Its index is the priority of the set. */
1425  arrayForEachItem(mdd_t *, onionRings, i, ring) {
1426    if (!mdd_lequal(states, ring, 1, 0)) break;
1427  }
1428  assert(i < array_n(onionRings));
1429
1430  /* Trim the spine-set. */
1431  while ( !mdd_lequal(node, states, 1, 1) ) {
1432    tmp = node;
1433    tmp1 =  Mc_FsmEvaluateEXFormula(fsm, node, mddOne,
1434                                    careStatesArray, verbosity, dcLevel);
1435    mdd_free(tmp);
1436    node = mdd_and(tmp1, spine, 1, 1); 
1437    mdd_free(tmp1);
1438  }
1439 
1440  tmp = spine;
1441  spine = mdd_and(spine, states, 1, 1);
1442  mdd_free(tmp);
1443
1444#if 0
1445  /* Invariants that should always hold */
1446  assert( mdd_is_tautology(node, 0) == mdd_is_tautology(spine, 0) );
1447  assert(mdd_lequal(node, states, 1, 1));
1448  assert(mdd_lequal(node, spine, 1, 1));
1449  assert(mdd_lequal(spine, states, 1, 1));
1450#endif
1451
1452  mdd_free(mddOne);
1453  array_free(careStatesArray);
1454 
1455  gns = ALLOC(gns_t, 1);
1456  gns->states = states;
1457  gns->node = node;
1458  gns->spine = spine;
1459
1460
1461  Heap_HeapInsert(queue,gns,i);
1462  return;
1463
1464} /* LinearstepQueueEnqueue */
1465
1466
1467/**Function********************************************************************
1468
1469  Synopsis    [Return the SCC enumeration method.]
1470
1471  Description [Get the SCC enumeration method from the environment
1472  setting scc_method. Return 0 if it is LockStep (default), 1 if it is
1473  LinearStep.  ]
1474
1475  SideEffects []
1476
1477  SeeAlso     [GetSccEnumerationMethod]
1478
1479******************************************************************************/
1480static int 
1481GetSccEnumerationMethod( void )
1482{
1483  char *flagValue;
1484  int  linearStepMethod = 0;
1485 
1486  flagValue = Cmd_FlagReadByName("scc_method");
1487  if (flagValue != NIL(char)) {
1488    if (strcmp(flagValue, "linearstep") == 0)
1489      linearStepMethod = 1;
1490    else if (strcmp(flagValue, "lockstep") == 0)
1491      linearStepMethod = 0;
1492    else {
1493      fprintf(vis_stderr, "** scc error: invalid scc method %s, method lockstep is used. \n", 
1494              flagValue);
1495    }
1496  }
1497
1498  return linearStepMethod;
1499}
Note: See TracBrowser for help on using the repository browser.