source: vis_dev/vis-2.3/src/mc/mcGFP.c

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

vis2.3
File size: 29.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [mcGFP.c]
4
5  PackageName [mc]
6
7  Synopsis    [Computation of greatest fixpoints.]
8
9  Description [This file contains the functions implementing the Generalized
10  SCC Hull algorithm (GSH) for language emptiness check and for the
11  computation of the states satisfying an EG formula.]
12
13  SeeAlso     [mcMc.c]
14
15  Author      [Fabio Somenzi]
16
17  Copyright   [This file was created at the University of Colorado at
18  Boulder.  The University of Colorado at Boulder makes no warranty
19  about the suitability of this software for any purpose.  It is
20  presented on an AS IS basis.]
21
22******************************************************************************/
23
24#include "mcInt.h"
25
26
27/*---------------------------------------------------------------------------*/
28/* Constant declarations                                                     */
29/*---------------------------------------------------------------------------*/
30
31/*---------------------------------------------------------------------------*/
32/* Stucture declarations                                                     */
33/*---------------------------------------------------------------------------*/
34
35/**Struct**********************************************************************
36
37  Synopsis    [Structure to store disabled operators in GSH.]
38
39  Description [Structure to store disabled operators in GSH.  A
40  disabled operator is one whose application is known not to cause any
41  progress towards the fixpoint.  When all operators are disabled, the
42  computation has converged to the fixpoint.  If there are n fairness
43  constraints, the EU operators receive the indices from 0 to n-1,
44  while the one EX is given index n.]
45
46******************************************************************************/
47struct McGSHOpSetStruct {
48  array_t *flags;               /* flag array for quick membership test */
49  int cnt;                      /* number of operators in set */
50  int last;                     /* last operator applied */
51  int nextToLast;               /* next to last operator applied */
52  int exBudget;                 /* allowed number of EXs in budget schedule */
53  int exCount;                  /* EXs applied so far (EUs included) */
54  Mc_GSHScheduleType schedule;  /* operator schedule */
55};
56
57
58/*---------------------------------------------------------------------------*/
59/* Type declarations                                                         */
60/*---------------------------------------------------------------------------*/
61
62typedef struct McGSHOpSetStruct McGSHOpSet_t;
63
64/*---------------------------------------------------------------------------*/
65/* Variable declarations                                                     */
66/*---------------------------------------------------------------------------*/
67
68#ifndef lint
69static char rcsid[] UNUSED = "$Id: mcGFP.c,v 1.10 2002/09/16 00:47:16 fabio Exp $";
70#endif
71
72/*---------------------------------------------------------------------------*/
73/* Macro declarations                                                        */
74/*---------------------------------------------------------------------------*/
75
76/**Macro***********************************************************************
77
78  Synopsis    [Returns TRUE if an operator of GSH is an EX.]
79
80  SideEffects [none]
81
82******************************************************************************/
83#define GSHoperatorIsEX(op,set) ((op) == (array_n((set)->flags) - 1))
84
85/**AutomaticStart*************************************************************/
86
87/*---------------------------------------------------------------------------*/
88/* Static function prototypes                                                */
89/*---------------------------------------------------------------------------*/
90
91static int PickOperatorForGSH ARGS((McGSHOpSet_t *set));
92static boolean ConvergedGSH ARGS((mdd_t *Z, mdd_t *zeta, int opIndex, McGSHOpSet_t *opSet, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, boolean *fixpoint));
93static McGSHOpSet_t * AllocOperatorSetGSH ARGS((int n, Mc_GSHScheduleType schedule));
94static void FreeOperatorSetGSH ARGS((McGSHOpSet_t *set));
95static void EmptyOperatorSetGSH ARGS((McGSHOpSet_t *set));
96static boolean IsMemberOperatorSetGSH ARGS((McGSHOpSet_t *set, int opIndex));
97static int SizeOperatorSetGSH ARGS((McGSHOpSet_t *set));
98static int PushOperatorSetGSH ARGS((McGSHOpSet_t *set, int opIndex));
99
100/**AutomaticEnd***************************************************************/
101
102
103/*---------------------------------------------------------------------------*/
104/* Definition of internal functions                                          */
105/*---------------------------------------------------------------------------*/
106
107
108/**Function********************************************************************
109
110  Synopsis    [Evaluate states satisfying EG(invariantMdd), given
111  a transition relation.]
112
113  Description [Evaluate states satisfying EG(invariantMdd) under
114  Buechi fairness conditions, given a transition relation.  Use the
115  GSH (Generalized SCC Hull, Ravi et al., FMCAD00) algorithm
116  restricted to backward operators.  (We can mix forward and backward
117  operators in language emptiness, but not in the EG computation.)]
118
119  SideEffects [If onionRingsArrayForDbg is not NULL on entry, leaves
120  the onion rings of the EU computations in the array it points to.
121  If fixpoint is not NULL, stores in the location pointed by it the
122  information about the cause for termination.  (That is, whether a
123  fixpoint was reached or not.)]
124
125  SeeAlso     [Mc_FsmEvaluateEGFormula]
126
127******************************************************************************/
128mdd_t*
129McFsmEvaluateEGFormulaUsingGSH(
130  Fsm_Fsm_t *modelFsm,
131  mdd_t *invariantMdd,
132  mdd_t *overapprox,
133  mdd_t *fairStates,
134  Fsm_Fairness_t *modelFairness,
135  array_t *careStatesArray,
136  Mc_EarlyTermination_t *earlyTermination,
137  array_t **pOnionRingsArrayForDbg,
138  Mc_VerbosityLevel verbosity,
139  Mc_DcLevel dcLevel,
140  boolean *fixpoint,
141  Mc_GSHScheduleType schedule)
142{
143  int i,n;
144  array_t *onionRings;
145  boolean useRings;
146  mdd_manager *mddManager;
147  mdd_t *mddOne;
148  mdd_t *iterate;
149  array_t *buechiFairness;
150  int nPreComps;
151  int nIterations;
152  McGSHOpSet_t *operatorSet;
153
154  /* Here's how the pOnionRingsArrayForDbg works.  It is a pointer to
155  ** an array of arrays of mdds.  There is one entry for every
156  ** fairness constraint, and this entry is the array of the onion
157  ** rings of the EU computation that corresponds to this constraint.
158  ** Every time the EU for a given constraint is recomputed, the
159  ** corresponding array of rings is renewed.  */
160  assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
161         *pOnionRingsArrayForDbg == NIL(array_t) ||
162         array_n(*pOnionRingsArrayForDbg) == 0); 
163
164  useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
165              *pOnionRingsArrayForDbg != NIL(array_t));
166
167  /* Initialization. */
168  nIterations = 0;
169  nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
170  onionRings = NIL(array_t);
171  mddManager = Fsm_FsmReadMddManager(modelFsm);
172  mddOne = mdd_one(mddManager);
173
174  /* If an overapproxiamtion of the greatest fixpoint is given, use it. */
175  if(overapprox != NIL(mdd_t)){
176    iterate = mdd_and(invariantMdd, overapprox, 1, 1);
177  } else {
178    iterate = mdd_dup(invariantMdd);
179  }
180
181  /* See if we need to enter the loop at all.  If we wanted to test for
182  ** early termination here, we should fix the onion rings. */
183  if (mdd_is_tautology(iterate, 0)) {
184    mdd_free(mddOne);
185    if (fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0);
186    return(iterate);
187  }
188
189  /* Read fairness constraints. */
190  buechiFairness = array_alloc(mdd_t *, 0);
191  if (modelFairness != NIL(Fsm_Fairness_t)) {
192    if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
193      (void) fprintf(vis_stdout,
194               "** mc error: non-Buechi fairness constraints not supported\n");
195      array_free(buechiFairness);
196      mdd_free(iterate);
197      mdd_free(mddOne);
198
199      if (fixpoint != NIL(boolean)) *fixpoint = FALSE;
200      return NIL(mdd_t);
201    } else {
202      int j;
203      int numBuechi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
204      for (j = 0; j < numBuechi; j++) {
205        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
206                                                careStatesArray, dcLevel);
207        array_insert_last(mdd_t *, buechiFairness, tmpMdd);
208      }
209    }
210  } else {
211    array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
212  }
213
214  /* Initialize set of disabled operators (to the empty set). */
215  n = array_n(buechiFairness);
216  operatorSet = AllocOperatorSetGSH(n, schedule);
217
218  /* Iterate until all operators disabled or early termination. */
219  while (TRUE) {
220    mdd_t *oldIterate = iterate;
221    int opIndex = PickOperatorForGSH(operatorSet);
222    nIterations++;
223    if (GSHoperatorIsEX(opIndex,operatorSet)) {
224      mdd_t *EX = Mc_FsmEvaluateEXFormula(modelFsm, oldIterate, mddOne,
225                                          careStatesArray, verbosity,
226                                          dcLevel);
227      iterate = mdd_and(EX, oldIterate, 1, 1);
228      mdd_free(EX);
229    } else {
230      mdd_t *Fi = array_fetch(mdd_t *, buechiFairness, opIndex);
231      mdd_t *target = mdd_and(Fi, iterate, 1, 1);
232
233      /* Dispose of the old set of onion rings for this fairness constraint
234      ** if it exists, and allocate a fresh array for a new set of rings. */
235      if (useRings) {
236        if (opIndex < array_n(*pOnionRingsArrayForDbg)) {
237          onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
238                                   opIndex);
239          mdd_array_free(onionRings);
240        }
241        onionRings = array_alloc(mdd_t *, 0);
242        array_insert(array_t *, *pOnionRingsArrayForDbg, opIndex, onionRings);
243      }
244
245      iterate = Mc_FsmEvaluateEUFormula(modelFsm, oldIterate, target,
246                                        NIL(mdd_t), mddOne, careStatesArray,
247                                        MC_NO_EARLY_TERMINATION, NIL(array_t),
248                                        Mc_None_c, onionRings, verbosity,
249                                        dcLevel, NIL(boolean));
250      mdd_free(target);
251    }
252    if (ConvergedGSH(iterate, oldIterate, opIndex, operatorSet,
253                     careStatesArray, earlyTermination, fixpoint)) {
254      mdd_free(oldIterate);
255      break;
256    }
257    mdd_free(oldIterate);
258  }
259
260  /* Free operator set. */
261  FreeOperatorSetGSH(operatorSet);
262
263  /* Sanity checks for onion rings and diagnostic prints. */
264  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
265    if (useRings) {
266      for (i = 0 ; i < array_n(*pOnionRingsArrayForDbg); i++) {
267        int j;
268        mdd_t *Fi = array_fetch(mdd_t *, buechiFairness, i);
269        array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
270                                          i);
271        /* Early termination with random schedules may leave holes. */
272        if (onionRings == NIL(array_t)) continue;
273        for (j = 0; j < array_n(onionRings); j++) {
274          mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
275          if (j == 0) {
276            if (!mdd_lequal_mod_care_set_array(ring, Fi, 1, 1,
277                                               careStatesArray)) {
278              fprintf(vis_stderr, "** mc error: Problem w/ dbg in EG - ");
279              fprintf(vis_stderr,
280                      "inner most ring not in Fi (fairness constraint).\n");
281            }
282          }
283          if (!mdd_lequal_mod_care_set_array(ring, invariantMdd, 1, 1,
284                                             careStatesArray)) {
285            fprintf(vis_stderr, "** mc error: Problem w/ dbg in EG - ");
286            fprintf(vis_stderr, "onion ring of last EU fails invariant\n");
287          }
288        }
289      }
290    }
291
292    if (verbosity == McVerbosityMax_c) {
293      mdd_t *tmpMdd = careStatesArray ?
294        mdd_and_array(iterate, careStatesArray, 1, 1) : mdd_dup(iterate);
295      fprintf(vis_stdout,
296              "--There are %.0f care states satisfying EG formula\n",
297              mdd_count_onset(mddManager, tmpMdd,
298                              Fsm_FsmReadPresentStateVars(modelFsm)));
299#ifdef DEBUG_MC
300      /* The following 2 lines are just for debug. */
301      fprintf(vis_stdout, "EG satisfying minterms :\n");
302      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
303#endif
304      mdd_free(tmpMdd);
305    } else {
306      fprintf(vis_stdout, "--There are %.0f states satisfying EG formula\n",
307              mdd_count_onset(mddManager, iterate,
308                              Fsm_FsmReadPresentStateVars(modelFsm)));
309    }
310
311    fprintf(vis_stdout, "--EG: %d iterations, %d preimage computations\n",
312            nIterations,
313            Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
314  }
315
316  mdd_array_free(buechiFairness);
317  mdd_free(mddOne);
318
319  return iterate;
320
321} /* McFsmEvaluateEGFormulaUsingGSH */
322
323
324/**Function********************************************************************
325
326  Synopsis    [Evaluate states satisfying EH(invariantMdd), given
327  a transition relation.]
328
329  Description [Evaluate states satisfying EH(invariantMdd) under
330  Buechi fairness conditions, given a transition relation.  Use the
331  GSH (Generalized SCC Hull, Ravi et al., FMCAD00) algorithm
332  restricted to forward operators.  (We can mix forward and backward
333  operators in language emptiness, but not in the EH computation.)]
334
335  SideEffects [If onionRingsArrayForDbg is not NULL on entry, leaves
336  the onion rings of the ES computations in the array it points to.
337  If fixpoint is not NULL, stores in the location pointed by it the
338  information about the cause for termination.  (That is, whether a
339  fixpoint was reached or not.)]
340
341  SeeAlso     [Mc_FsmEvaluateEHFormula]
342
343******************************************************************************/
344mdd_t*
345McFsmEvaluateEHFormulaUsingGSH(
346  Fsm_Fsm_t *modelFsm,
347  mdd_t *invariantMdd,
348  mdd_t *overapprox,
349  mdd_t *fairStates,
350  Fsm_Fairness_t *modelFairness,
351  array_t *careStatesArray,
352  Mc_EarlyTermination_t *earlyTermination,
353  array_t **pOnionRingsArrayForDbg,
354  Mc_VerbosityLevel verbosity,
355  Mc_DcLevel dcLevel,
356  boolean *fixpoint,
357  Mc_GSHScheduleType schedule)
358{
359  int i,n;
360  array_t *onionRings;
361  boolean useRings;
362  mdd_manager *mddManager;
363  mdd_t *mddOne;
364  mdd_t *iterate;
365  array_t *buechiFairness;
366  int nImgComps;
367  int nIterations;
368  McGSHOpSet_t *operatorSet;
369
370  /* Here's how the pOnionRingsArrayForDbg works.  It is a pointer to
371  ** an array of arrays of mdds.  There is one entry for every
372  ** fairness constraint, and this entry is the array of the onion
373  ** rings of the ES computation that corresponds to this constraint.
374  ** Every time the ES for a given constraint is recomputed, the
375  ** corresponding array of rings is renewed.  */
376  assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
377         *pOnionRingsArrayForDbg == NIL(array_t) ||
378         array_n(*pOnionRingsArrayForDbg) == 0); 
379
380  useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
381              *pOnionRingsArrayForDbg != NIL(array_t));
382
383  /* Initialization. */
384  nIterations = 0;
385  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
386  onionRings = NIL(array_t);
387  mddManager = Fsm_FsmReadMddManager(modelFsm);
388  mddOne = mdd_one(mddManager);
389
390  /* If an overapproxiamtion of the greatest fixpoint is given, use it. */
391  if(overapprox != NIL(mdd_t)){
392    iterate = mdd_and(invariantMdd, overapprox, 1, 1);
393  } else {
394    iterate = mdd_dup(invariantMdd);
395  }
396
397  /* See if we need to enter the loop at all. */
398  if (mdd_is_tautology(iterate, 0) ||
399    McCheckEarlyTerminationForOverapprox(earlyTermination,
400                                         iterate, careStatesArray)) {
401    mdd_free(mddOne);
402
403    if (fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0);
404    return(iterate);
405  }
406
407  /* Read fairness constraints. */
408  buechiFairness = array_alloc(mdd_t *, 0);
409  if (modelFairness != NIL(Fsm_Fairness_t)) {
410    if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
411      (void) fprintf(vis_stdout,
412               "** mc error: non-Buechi fairness constraints not supported\n");
413      array_free(buechiFairness);
414      mdd_free(iterate);
415      mdd_free(mddOne);
416
417      if (fixpoint != NIL(boolean)) *fixpoint = FALSE;
418      return NIL(mdd_t);
419    } else {
420      int j;
421      int numBuechi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
422      for (j = 0; j < numBuechi; j++) {
423        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
424                                                careStatesArray, dcLevel);
425        array_insert_last(mdd_t *, buechiFairness, tmpMdd);
426      }
427    }
428  } else {
429    array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
430  }
431
432  /* Initialize set of disabled operators (to the empty set). */
433  n = array_n(buechiFairness);
434  operatorSet = AllocOperatorSetGSH(n, schedule);
435
436  /* Iterate until all operators disabled or early termination. */
437  while (TRUE) {
438    mdd_t *oldIterate = iterate;
439    int opIndex = PickOperatorForGSH(operatorSet);
440    nIterations++;
441    if (GSHoperatorIsEX(opIndex,operatorSet)) {
442      mdd_t *EY = Mc_FsmEvaluateEYFormula(modelFsm, oldIterate, mddOne,
443                                          careStatesArray, verbosity,
444                                          dcLevel);
445      iterate = mdd_and(EY, oldIterate, 1, 1);
446      mdd_free(EY);
447    } else {
448      mdd_t *Fi = array_fetch(mdd_t *, buechiFairness, opIndex);
449      mdd_t *source = mdd_and(Fi, iterate, 1, 1);
450
451      /* Dispose of the old set of onion rings for this fairness constraint
452      ** if it exists, and allocate a fresh array for a new set of rings. */
453      if (useRings) {
454        if (opIndex < array_n(*pOnionRingsArrayForDbg)) {
455          onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
456                                   opIndex);
457          mdd_array_free(onionRings);
458        }
459        onionRings = array_alloc(mdd_t *, 0);
460        array_insert(array_t *, *pOnionRingsArrayForDbg, opIndex, onionRings);
461      }
462
463      iterate = Mc_FsmEvaluateESFormula(modelFsm, oldIterate, source,
464                                        NIL(mdd_t), mddOne, careStatesArray,
465                                        MC_NO_EARLY_TERMINATION, NIL(array_t),
466                                        Mc_None_c, onionRings, verbosity,
467                                        dcLevel, NIL(boolean));
468      mdd_free(source);
469    }
470    if (ConvergedGSH(iterate, oldIterate, opIndex, operatorSet,
471                     careStatesArray, earlyTermination, fixpoint)) {
472      mdd_free(oldIterate);
473      break;
474    }
475    mdd_free(oldIterate);
476  }
477
478  /* Free operator set. */
479  FreeOperatorSetGSH(operatorSet);
480
481  /* Sanity checks for onion rings and diagnostic prints. */
482  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
483    if (useRings) {
484      for (i = 0 ; i < array_n(*pOnionRingsArrayForDbg); i++) {
485        int j;
486        mdd_t *Fi = array_fetch(mdd_t *, buechiFairness, i);
487        array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
488                                          i);
489        /* Early termination with random schedules may leave holes. */
490        if (onionRings == NIL(array_t)) continue;
491        for (j = 0; j < array_n(onionRings); j++) {
492          mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
493          if (j == 0) {
494            if (!mdd_lequal_mod_care_set_array(ring, Fi, 1, 1,
495                                               careStatesArray)) {
496              fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
497              fprintf(vis_stderr,
498                      "inner most ring not in Fi (fairness constraint).\n");
499            }
500          }
501          if (!mdd_lequal_mod_care_set_array(ring, invariantMdd, 1, 1,
502                                             careStatesArray)) {
503            fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
504            fprintf(vis_stderr, "onion ring of last ES fails invariant\n");
505          }
506        }
507      }
508    }
509
510    if (verbosity == McVerbosityMax_c) {
511      mdd_t *tmpMdd = careStatesArray ?
512        mdd_and_array(iterate, careStatesArray, 1, 1) : mdd_dup(iterate);
513      fprintf(vis_stdout,
514              "--There are %.0f care states satisfying EH formula\n",
515              mdd_count_onset(mddManager, tmpMdd,
516                              Fsm_FsmReadPresentStateVars(modelFsm)));
517#ifdef DEBUG_MC
518      /* The following 2 lines are just for debug. */
519      fprintf(vis_stdout, "EH satisfying minterms :\n");
520      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
521#endif
522      mdd_free(tmpMdd);
523    } else {
524      fprintf(vis_stdout, "--There are %.0f states satisfying EH formula\n",
525              mdd_count_onset(mddManager, iterate,
526                              Fsm_FsmReadPresentStateVars(modelFsm)));
527    }
528
529    fprintf(vis_stdout, "--EH: %d iterations, %d image computations\n",
530            nIterations,
531            Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
532  }
533
534  mdd_array_free(buechiFairness);
535  mdd_free(mddOne);
536
537  return iterate;
538
539} /* McFsmEvaluateEHFormulaUsingGSH */
540
541
542/*---------------------------------------------------------------------------*/
543/* Definition of static functions                                            */
544/*---------------------------------------------------------------------------*/
545
546
547/**Function********************************************************************
548
549  Synopsis    [Returns the next operator for the GSH algorithm.]
550
551  Description [Returns the next operator for the GSH algorithm.]
552
553  SideEffects [Updates the operator set.]
554
555  SeeAlso     [McFsmEvaluateEGFormulaUsingGSH]
556
557******************************************************************************/
558static int
559PickOperatorForGSH(
560  McGSHOpSet_t *set)
561{
562  int nop = array_n(set->flags);
563  int opIndex;
564  if (set->schedule == McGSH_EL_c) {
565    int exIndex = nop - 1;
566    if ((set->last != exIndex) && !array_fetch(int, set->flags, exIndex)) {
567      opIndex = exIndex;
568    } else {
569      if (set->last == exIndex) {
570        opIndex = (set->nextToLast + 1) % exIndex;
571      } else {
572        opIndex = (set->last + 1) % exIndex;
573      }
574      while (array_fetch(int, set->flags, opIndex))
575        opIndex = (opIndex + 1) % nop;
576    }
577    set->nextToLast = set->last;
578  } else if (set->schedule == McGSH_EL1_c) {
579    /* EL1 implements a round-robin policy. */
580    opIndex = (set->last + 1) % nop;
581    while (array_fetch(int, set->flags, opIndex))
582      opIndex = (opIndex + 1) % nop;
583  } else if (set->schedule == McGSH_EL2_c) {
584    /* EL2 differs from EL1 in that it repeats EX to convergence.
585     * We rely on the fact that EUs are always disabled after their
586     * application. */
587    opIndex = set->last;
588    while (array_fetch(int, set->flags, opIndex))
589      opIndex = (opIndex + 1) % nop;
590  } else if (set->schedule == McGSH_Budget_c) {
591    int exIndex = nop - 1;
592    int newCount = Img_GetNumberOfImageComputation(Img_Backward_c);
593    if (set->last == exIndex)
594      set->exBudget--;
595    else
596      set->exBudget += newCount - set->exCount;
597    set->exCount = newCount;
598    /* (void) printf("budget = %d\n", set->exBudget); */
599    if ((set->last != exIndex) && !array_fetch(int, set->flags, exIndex)) {
600      /* At least one EX after each EU, unless EX is disabled */
601      opIndex = exIndex;
602      set->nextToLast = set->last;
603    } else {
604      if (set->last == exIndex) {
605        if (set->exBudget > 0 && set->nextToLast == exIndex - 1) {
606          opIndex = exIndex;
607        } else {
608          opIndex = (set->nextToLast + 1) % exIndex;
609          set->nextToLast = set->last;
610        }
611      } else { /* EX is disabled */
612        opIndex = (set->last + 1) % exIndex;
613        set->nextToLast = set->last;
614      }
615      while (array_fetch(int, set->flags, opIndex))
616        opIndex = (opIndex + 1) % nop;
617    }
618    if (opIndex == 0)
619      set->exBudget = 0;
620#if 0
621    opIndex = set->last;
622    if (opIndex == exIndex && set->exBudget == 0)
623      opIndex = 0;
624    while (array_fetch(int, set->flags, opIndex))
625      opIndex = (opIndex + 1) % nop;
626#endif
627  } else {
628    /* The random schedule uses a rather primitive way of selecting a
629     * random integer.  However, as long as the number of operators is
630     * small, the distribution is acceptably uniform even if we use
631     * mod to map the result of util_random to 0 ... nop-1. */
632    int exIndex = nop - 1;
633    long rn = util_random();
634    int exDisabled = array_fetch(int, set->flags, exIndex);
635    if ((!exDisabled) && ((rn & 1024) || (set->cnt == exIndex))) {
636      /* rn & 1024 should be true 50% of the times */
637      opIndex = exIndex;
638    } else {
639      int enabledEUs = exIndex - (set->cnt - exDisabled);
640      rn = rn % enabledEUs;
641      assert(0 <= rn && rn < exIndex);
642      for (opIndex = 0; TRUE; opIndex++) {
643        assert(opIndex < exIndex);
644        if (!array_fetch(int, set->flags, opIndex)) {
645          if (rn == 0) {
646            break;
647          } else {
648            rn--;
649          }
650        }
651      }
652    }
653  }
654  set->last = opIndex;
655  return opIndex;
656
657} /* PickOperatorForGSH */
658
659
660/**Function********************************************************************
661
662  Synopsis    [Performs the convergence test for the GSH algorithm.]
663
664  Description [Performs the convergence test for the GSH algorithm.
665  Returns TRUE if convergence is achived; FALSE otherwise.]
666
667  SideEffects [Updates the operator set.  An operator is disabled
668  after application if it is an EU, or if has caused no progress
669  toward the fixpoint.  If convergence is reached, ConvergedGSH sets
670  the location pointed by parameter fixpoint to TRUE if a fixpoint was
671  reached, or to FALSE if early termination occured.]
672
673  SeeAlso     [McFsmEvaluateEGFormulaUsingGSH]
674
675******************************************************************************/
676static boolean
677ConvergedGSH(
678  mdd_t *Z                      /* new iterate */,
679  mdd_t *zeta                   /* old iterate */,
680  int opIndex                   /* operator that has been just applied */,
681  McGSHOpSet_t *opSet           /* set of disabled operators */,
682  array_t *careStatesArray      /* array for care states */,
683  Mc_EarlyTermination_t *earlyTermination /* early termination criterion */,
684  boolean *fixpoint             /* reason for termination */)
685{
686  boolean term_tautology = FALSE;
687  boolean term_fixpoint = FALSE;
688  boolean term_early = FALSE;
689
690  term_tautology = mdd_is_tautology(Z, 0);
691  if (!term_tautology)
692    term_fixpoint =  mdd_equal_mod_care_set_array(Z, zeta, careStatesArray);
693  if (!term_tautology && !term_fixpoint)
694    term_early = McCheckEarlyTerminationForOverapprox(earlyTermination, Z, 
695                                                      careStatesArray);
696  if (term_tautology || term_early) {
697    if (fixpoint != NIL(boolean))
698      *fixpoint = term_tautology;
699    return TRUE;
700  } else if (term_fixpoint) {
701    if (PushOperatorSetGSH(opSet,opIndex) == SizeOperatorSetGSH(opSet)) {
702      if (fixpoint != NIL(boolean))
703        *fixpoint = TRUE;
704      return TRUE;
705    } else {
706      return FALSE;
707    }
708  } else {
709    EmptyOperatorSetGSH(opSet);
710    if (!GSHoperatorIsEX(opIndex,opSet)) {
711      /* The operator is an EU.  Add to set. */
712      (void) PushOperatorSetGSH(opSet,opIndex);
713    }
714    return FALSE;
715  }
716
717} /* ConvergedGSH */
718
719
720/**Function********************************************************************
721
722  Synopsis    [Creates a new operator set.]
723
724  Description [Creates a new operator set to hold n operators.]
725
726  SideEffects [None]
727
728  SeeAlso     [McFsmEvaluateEGFormulaUsingGSH FreeOperatorSetGSH]
729
730******************************************************************************/
731static McGSHOpSet_t *
732AllocOperatorSetGSH(
733  int n,
734  Mc_GSHScheduleType schedule)
735{
736  int i;
737  McGSHOpSet_t *set = ALLOC(McGSHOpSet_t, 1);
738  array_t *flags = set->flags = array_alloc(int, n+1);
739  for (i = 0; i < n+1; i++) {
740    array_insert(int, flags, i, 0);
741  }
742  set->cnt = 0;
743  set->schedule = schedule;
744  if (set->schedule == McGSH_EL_c) {
745    set->last = n;
746    set->nextToLast = n - 1;
747  } else if (set->schedule == McGSH_EL1_c) {
748    set->last = n;
749  } else if (set->schedule == McGSH_EL2_c) {
750    set->last = 0;
751  } else if (set->schedule == McGSH_Budget_c) {
752    set->last = n;
753    set->nextToLast = n - 1;
754    set->exBudget = 1;
755    set->exCount = Img_GetNumberOfImageComputation(Img_Backward_c);
756  } else {
757    /* The random schedule has no history.  Hence, this initialization is
758     * immaterial. */
759    set->last = 0;
760  }
761  return set;
762
763} /* AllocOperatorSetGSH */
764
765
766/**Function********************************************************************
767
768  Synopsis    [Frees an operator set.]
769
770  Description [Frees an operator set.]
771
772  SideEffects [None]
773
774  SeeAlso     [McFsmEvaluateEGFormulaUsingGSH AllocOperatorSetGSH]
775
776******************************************************************************/
777static void
778FreeOperatorSetGSH(
779  McGSHOpSet_t *set)
780{
781  array_free(set->flags);
782  FREE(set);
783  return;
784
785} /* FreeOperatorSetGSH */
786
787
788/**Function********************************************************************
789
790  Synopsis    [Empties an operator set.]
791
792  Description [Empties an operator set.  This is done in the GSH
793  algorithm when progress is made towards the fixpoint.  The
794  information about the last operator applied is unaffected.]
795
796  SideEffects [None]
797
798  SeeAlso     [McFsmEvaluateEGFormulaUsingGSH]
799
800******************************************************************************/
801static void
802EmptyOperatorSetGSH(
803  McGSHOpSet_t *set)
804{
805  int i;
806  for (i = 0; i < array_n(set->flags); i++) {
807    array_insert(int, set->flags, i, 0);
808  }
809  set->cnt = 0;
810  return;
811
812} /* EmptyOperatorSetGSH */
813
814
815/**Function********************************************************************
816
817  Synopsis    [Checks for membership of an operator in a set.]
818
819  Description [Checks for membership of an operator in a set.]
820
821  SideEffects [None]
822
823  SeeAlso     [McFsmEvaluateEGFormulaUsingGSH]
824
825******************************************************************************/
826static boolean
827IsMemberOperatorSetGSH(
828  McGSHOpSet_t *set,
829  int opIndex)
830{
831  return array_fetch(int, set->flags, opIndex);
832
833} /* IsMemberOperatorSetGSH */
834
835
836/**Function********************************************************************
837
838  Synopsis    [Returns the cardinality of an operator set.]
839
840  Description [Returns the cardinality of an operator set.]
841
842  SideEffects [None]
843
844  SeeAlso     [McFsmEvaluateEGFormulaUsingGSH]
845
846******************************************************************************/
847static int
848SizeOperatorSetGSH(
849  McGSHOpSet_t *set)
850{
851  return array_n(set->flags);
852
853} /* SizeOperatorSetGSH */
854
855
856/**Function********************************************************************
857
858  Synopsis    [Adds an element to an operator set.]
859
860  Description [Adds an element to an operator set.]
861
862  SideEffects [None]
863
864  SeeAlso     [McFsmEvaluateEGFormulaUsingGSH]
865
866******************************************************************************/
867static int
868PushOperatorSetGSH(
869  McGSHOpSet_t *set,
870  int opIndex)
871{
872  assert(opIndex < array_n(set->flags));
873  array_insert(int, set->flags, opIndex, 1);
874  set->cnt++;
875  return set->cnt;
876
877} /* PushOperatorSetGSH */
Note: See TracBrowser for help on using the repository browser.