source: vis_dev/vis-2.3/src/mc/mcMc.c @ 38

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

vis2.3
File size: 132.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [mcMc.c]
4
5  PackageName [mc]
6
7  Synopsis    [Fair CTL model checker.]
8
9  Description [This file contains the functions for both backward and
10  forward model checking. Forward model checking is based on Iwashta's
11  ICCAD96 paper. Future tense CTLs are automatically converted to past
12  tense ones as much as possible in forward model checking.]
13
14  Author [Adnan Aziz, Tom Shiple, Rajeev Ranjan, In-Ho Moon, Roderick Bloem]
15
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35******************************************************************************/
36
37#include "ctlpInt.h"
38#include "mcInt.h"
39#include "fsm.h"
40#include "bmc.h"
41
42static char rcsid[] UNUSED = "$Id: mcMc.c,v 1.257 2007/04/17 00:01:22 sohail Exp $";
43
44#ifdef DEBUG_MC
45void _McPrintSatisfyingMinterms(mdd_t *aMdd, Fsm_Fsm_t *fsm);
46#endif
47
48/*---------------------------------------------------------------------------*/
49/* Macro declarations                                                        */
50/*---------------------------------------------------------------------------*/
51
52/**AutomaticStart*************************************************************/
53
54/*---------------------------------------------------------------------------*/
55/* Static function prototypes                                                */
56/*---------------------------------------------------------------------------*/
57
58static mdd_t * EvaluateFormulaRecur(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Ctlp_Approx_t TRMinimization, Ctlp_Approx_t *resultApproxType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule);
59static mdd_t * McForwardReachable(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *invariantMdd, mdd_t *fairStates, array_t *careStatesArray, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
60
61/**AutomaticEnd***************************************************************/
62
63
64/*---------------------------------------------------------------------------*/
65/* Definition of exported functions                                          */
66/*---------------------------------------------------------------------------*/
67
68/**Function********************************************************************
69
70  Synopsis [Compute all the states that lead to a fair cycle]
71
72  Comment  [Used by LE/LTL/CTL* model checking. Different dicision procedures
73  are applied according to the "strength of the  buechi automaton": For the
74  strong automaton, we need to compute EG(true) under the fairness constraints;
75  If the automaton is weak, we will check !EFEG(fair); If the automaton is
76  terminal, we only need to check !EF(fair). This is based on the CAV'99 paper
77  of Bloem, Ravi & Somenzi: "Efficient Decision Procedures for Model Checking
78  of Linear Time Logic Properties".
79 
80  Debugging information will be print out if dbgLevel is non-zero.
81
82  Return the set of initial states from where fair paths exist.]
83 
84  SideEffects [The caller should free the returned mdd_t.]
85
86******************************************************************************/
87mdd_t *
88Mc_FsmCheckLanguageEmptiness(
89  Fsm_Fsm_t *modelFsm,
90  array_t *modelCareStatesArray,
91  Mc_AutStrength_t automatonStrength,
92  Mc_LeMethod_t leMethod,
93  int dcLevel,
94  int dbgLevel,
95  int printInputs,
96  int verbosity,
97  Mc_GSHScheduleType GSHschedule,
98  Mc_FwdBwdAnalysis GSHdirection,
99  int lockstep,
100  FILE *dbgFile,
101  int UseMore,
102  int SimValue,
103  char *driverName)
104{
105  mdd_t *result;
106  mdd_t *mddOne;
107  mdd_t *badStates;
108  mdd_t *aBadState;
109  mdd_t *initialStates;
110  mdd_t *fairStates;
111  mdd_manager *mddMgr;
112  Ctlp_Formula_t *ctlFair, *ctlFormula;
113  Mc_EarlyTermination_t *earlyTermination;
114  array_t *arrayOfOnionRings;
115  array_t *stemArray;
116  array_t *cycleArray;
117  McPath_t *fairPath;
118  McPath_t *normalPath;
119  FILE *tmpFile = vis_stdout;
120  extern FILE *vis_stdpipe;
121  int i;
122
123  if (leMethod == Mc_Le_Dnc_c && automatonStrength == 2) {
124    return  Mc_FsmCheckLanguageEmptinessByDnC(modelFsm,
125                                              modelCareStatesArray,
126                                              Mc_Aut_Strong_c,
127                                              dcLevel,
128                                              dbgLevel,
129                                              printInputs,
130                                              verbosity,
131                                              GSHschedule,
132                                              GSHdirection,
133                                              lockstep,
134                                              dbgFile,
135                                              UseMore,
136                                              SimValue,
137                                              driverName);
138  }
139 
140  /**************************************************************************
141   * CASE1 & CASE2: TERMINAL/WEAK AUTOMATON
142   *                problem is reduced to checking !EF (fair) for TERMINAL
143   *                or !EF EG (fair) for WEAK
144   **************************************************************************/
145  if (automatonStrength == 0 || automatonStrength == 1) {
146    Fsm_Fairness_t *modelFairness;
147    modelFairness = Fsm_FsmReadFairnessConstraint(modelFsm);
148    assert(Fsm_FairnessTestIsBuchi(modelFairness));
149    ctlFair = Ctlp_FormulaCreate(Ctlp_ID_c,
150                                 (void *)util_strsav("fair1$AUT$NTK2"),
151                                 (void *)util_strsav("1"));
152    /*    Dup(Fsm_FairnessReadFinallyInfFormula(modelFairness, 0, 0));    */
153    if (automatonStrength == 0) {
154      Ctlp_Formula_t *ctlTRUE;
155      ctlTRUE = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t),
156                                   NIL(Ctlp_Formula_t));
157      ctlFormula = Ctlp_FormulaCreate(Ctlp_EU_c, ctlTRUE, ctlFair);
158      if (dbgLevel || verbosity) 
159        fprintf(vis_stdout, "# %s: Terminal automaton -- check EF(states satisfy fairness)\n",
160                driverName);
161    }else {
162      Ctlp_Formula_t *ctlTRUE, *ctlEGfair;
163      ctlTRUE = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t));
164      ctlEGfair = Ctlp_FormulaCreate(Ctlp_EG_c, ctlFair, NIL(Ctlp_Formula_t));
165      ctlFormula = Ctlp_FormulaCreate(Ctlp_EU_c, ctlTRUE, ctlEGfair);
166      if (dbgLevel || verbosity) 
167        fprintf(vis_stdout, "# %s: Weak automaton -- check EF EG (states satisfy fairness)\n",
168                driverName);
169    }
170
171    /* Evaluate ctlFormula */
172    mddMgr = Fsm_FsmReadMddManager(modelFsm);
173    mddOne = mdd_one(mddMgr);
174    initialStates = Fsm_FsmComputeInitialStates(modelFsm);
175    earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
176    fairStates = 
177      Mc_FsmEvaluateFormula(modelFsm, ctlFormula, mddOne, modelFairness, 
178                            modelCareStatesArray,
179                            earlyTermination,
180                            NIL(Fsm_HintsArray_t), Mc_None_c,
181                            (Mc_VerbosityLevel) verbosity,
182                            (Mc_DcLevel) dcLevel, 
183                            (dbgLevel != McDbgLevelNone_c || verbosity),
184                            GSHschedule);
185    Mc_EarlyTerminationFree(earlyTermination);
186    mdd_free(mddOne);
187
188    /* If there is at least one fair initial state, language is not empty. */
189    if (!mdd_lequal(initialStates, fairStates, 1, 0)) {
190      if (strcmp(driverName, "LE") == 0)
191        fprintf(vis_stdout, "# LE: language is not empty\n");
192      else
193        fprintf(vis_stdout, "# %s: formula failed\n", driverName);
194      result = mdd_and(fairStates, initialStates, 1, 1);
195    } else {
196      if (strcmp(driverName, "LE") == 0)
197        fprintf(vis_stdout, "# LE: language emptiness check passes\n");
198      else
199        fprintf(vis_stdout, "# %s: formula passed\n", driverName);
200      Ctlp_FormulaFree(ctlFormula);
201      mdd_free(fairStates);
202      mdd_free(initialStates);
203      return NIL(mdd_t);
204    }
205
206    /* If no wintness is requested, clean up and return. */
207    if (dbgLevel == McDbgLevelNone_c) {
208      Ctlp_FormulaFree(ctlFormula);
209      mdd_free(initialStates);
210      mdd_free(fairStates);
211      return result;
212    }else {
213      Ctlp_Formula_t *F;
214      array_t *EGArrayOfOnionRings, *EGonionRings, *EFonionRings;
215      array_t *newOnionRings;
216      mdd_t *mdd1;
217      int j;
218      arrayOfOnionRings = array_alloc(array_t *, 0);
219      EFonionRings = (array_t *) Ctlp_FormulaReadDebugData(ctlFormula);
220      if (automatonStrength == 0) {
221        array_insert_last(array_t *, arrayOfOnionRings,
222                          mdd_array_duplicate(EFonionRings));
223      }else if (automatonStrength == 1) {
224        F = Ctlp_FormulaReadRightChild(ctlFormula);
225        /* EG (states labelled fair) */
226        EGArrayOfOnionRings = (array_t *)Ctlp_FormulaReadDebugData(F);
227        arrayForEachItem(array_t *, EGArrayOfOnionRings, i, EGonionRings) {
228          newOnionRings = mdd_array_duplicate(EGonionRings);
229          arrayForEachItem(mdd_t *, EFonionRings, j, mdd1) {
230            if (j != 0)
231              array_insert_last(mdd_t *, newOnionRings, mdd_dup(mdd1));
232          }
233          array_insert_last(array_t *, arrayOfOnionRings, newOnionRings);
234        }
235      }
236      Ctlp_FormulaFree(ctlFormula);
237      fprintf(vis_stdout, "# %s: generating path to fair cycle\n", driverName);
238    }
239   
240  }else {
241    /*************************************************************************
242     * CASE3:     STRONG AUTOMATON
243     *            need to solve the problem by computing EG_fair (true)
244     *************************************************************************/
245    mddMgr = Fsm_FsmReadMddManager(modelFsm);
246    initialStates = Fsm_FsmComputeInitialStates(modelFsm);
247
248    /* Compute fair states. */
249    if (lockstep == MC_LOCKSTEP_OFF) {
250      fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray,
251                                            verbosity, dcLevel, GSHschedule,
252                                            GSHdirection, FALSE);
253      arrayOfOnionRings = Fsm_FsmReadDebugArray(modelFsm);
254    } else {
255      /* For lockstep, the computed set of states is a subset of the
256         reachable fair states, with the property that the subset is
257         empty only if there are no reachable fair states.  Since the
258         onion rings are built for the fairness constraint restricted to
259         the subset of the fair states, they are not valid in general
260         for the FSM.  Hence, they are not saved.  */
261      array_t *SCCs = array_alloc(mdd_t *, 0);
262      arrayOfOnionRings = array_alloc(array_t *, 0);
263      fairStates = McFsmComputeFairSCCsByLockStep(modelFsm, lockstep, SCCs,
264                                                  arrayOfOnionRings,
265                                                  (Mc_VerbosityLevel)
266                                                  verbosity,
267                                                  (Mc_DcLevel) dcLevel);
268      mdd_array_free(SCCs);
269    }
270
271   
272    /* Lockstep guarantees that all fair SCCs are reachable.  However,
273       it does not extend the fair states backward unless a
274       counterexample is requested.  For the SCC hull approach with backward
275       operators, the language is not empty if there is at least one
276       fair initial state.  Finally, For SCC hull with forward operators,
277       currently we do not extend the hull backward, but we enforce
278       reachability of the hull.  Hence, nonemptiness of the hull signals that
279       the language is not empty. */
280    if ((lockstep == MC_LOCKSTEP_OFF &&
281         (!mdd_lequal(initialStates, fairStates, 1, 0) ||
282          (GSHdirection == McFwd_c &&
283           !mdd_lequal_array(fairStates, modelCareStatesArray, 1, 0)))) ||
284        (lockstep != MC_LOCKSTEP_OFF &&
285         !mdd_is_tautology(fairStates, 0))) {
286      if (strcmp(driverName, "LE") == 0)
287        fprintf(vis_stdout, "# LE: language is not empty\n");
288      else
289        fprintf(vis_stdout, "# %s: formula failed\n", driverName);
290      result = mdd_and(fairStates, initialStates, 1, 1);
291    } else {
292      if (strcmp(driverName, "LE") == 0)
293        fprintf(vis_stdout, "# LE: language emptiness check passes\n");
294      else
295        fprintf(vis_stdout, "# %s: formula passed\n", driverName);
296      /* Dispose of onion rings if produced by lockstep. */
297      if (lockstep != MC_LOCKSTEP_OFF) {
298        mdd_array_array_free(arrayOfOnionRings);
299      }
300      mdd_free(fairStates);
301      mdd_free(initialStates);
302      return NIL(mdd_t);
303    }
304
305    /* If no witness is requested, clean up and return. */
306    if (dbgLevel == McDbgLevelNone_c) {
307      /* Dispose of onion rings if produced by lockstep. */
308      if (lockstep != MC_LOCKSTEP_OFF) {
309        mdd_array_array_free(arrayOfOnionRings);
310      }
311      mdd_free(fairStates);
312      mdd_free(initialStates);
313      return result;
314    } else {
315      (void) fprintf(vis_stdout, "# %s: generating path to fair cycle\n",
316                     driverName);
317    }
318  }
319
320  /* Generate witness. */
321  badStates = mdd_and(initialStates, fairStates, 1, 1);
322  mdd_free(fairStates);
323  mdd_free(initialStates);
324  aBadState = Mc_ComputeAState(badStates, modelFsm);
325  mdd_free(badStates);
326
327  mddOne = mdd_one(mddMgr);
328  fairPath = McBuildFairPath(aBadState, mddOne, arrayOfOnionRings, modelFsm,
329                             modelCareStatesArray, 
330                             (Mc_VerbosityLevel) verbosity,
331                             (Mc_DcLevel) dcLevel,
332                             McFwd_c);
333  mdd_free(mddOne);
334  mdd_free(aBadState);
335 
336  /* Dispose of onion rings if produced by lockstep. */
337  if (lockstep != MC_LOCKSTEP_OFF || automatonStrength != 2) {
338    mdd_array_array_free(arrayOfOnionRings);
339  }
340
341  /* Print witness. */
342  normalPath = McPathNormalize(fairPath);
343  McPathFree(fairPath);
344
345  stemArray = McPathReadStemArray(normalPath);
346  cycleArray = McPathReadCycleArray(normalPath);
347
348  /* we should pass dbgFile/UseMore as parameters
349     dbgFile = McOptionsReadDebugFile(options);*/
350  if (dbgFile != NIL(FILE)) {
351    vis_stdpipe = dbgFile;
352  } else if (UseMore == TRUE) {
353    vis_stdpipe = popen("more","w");
354  } else {
355    vis_stdpipe = vis_stdout;
356  }
357  vis_stdout = vis_stdpipe;
358
359  /* We should also pass SimValue as a parameter */
360  if (SimValue == FALSE) {
361      (void) fprintf(vis_stdout, "# %s: path to fair cycle:\n\n", driverName);
362      Mc_PrintPath(stemArray, modelFsm, printInputs);
363      fprintf (vis_stdout, "\n");
364
365      (void) fprintf(vis_stdout, "# %s: fair cycle:\n\n", driverName);
366      Mc_PrintPath(cycleArray, modelFsm, printInputs);
367      fprintf (vis_stdout, "\n");
368  }else {
369      array_t *completePath = McCreateMergedPath(stemArray, cycleArray);
370      (void) fprintf(vis_stdout, "# %s: counter-example\n", driverName);
371      McPrintSimPath(vis_stdout, completePath, modelFsm);
372      mdd_array_free(completePath);
373  }
374
375  if (dbgFile == NIL(FILE) && UseMore == TRUE) {
376    (void) pclose(vis_stdpipe);
377  } 
378  vis_stdout = tmpFile;
379
380  McPathFree(normalPath);
381
382  return result;
383}
384
385
386/**Function********************************************************************
387
388  Synopsis    [Model check formula on given FSM under fairness]
389
390  Description [Model check formula on given FSM under fairness.]
391
392  Comment [ Recursive evaluation using Emerson-Lei LICS 1986 algorithms. The
393  states satisfying subformulas are stored and used later if there is sharing
394  of subformulas. Therefore, each subformula is computed just once. Large
395  switch - base case is atomic formula, TRUE, and FALSE.  Boolean operators -
396  straightforward. Path modalities are reduced to one of the three - EX, EU,
397  EG which are evaluated under fairness. Note the semantics for atomic
398  formulas carefully - in addition to generating the prescribed output, the
399  state must also be fair. Don't cares from unreached, unfair states are both
400  used. The proof of correctness of using all these dont cares hinges on the
401  invariant that restricted to the reached state set, the computed sets are
402  exactly as they should be. Both backward and forward formulas are handled.
403
404  This function sets the states and debug info of the formula for use
405  with the debugger.
406 
407  ARGUMENTS:
408
409  ctlFormula: a ctl formula in simple(!) existential form, using
410  forward and/or backward operators.
411 
412  EarlyTermination: If earlyTermination.mode is McAll_c
413  (McSome_c), the algorithm can stop as soon as
414
415  1. it is sure that all (some) of earlyTermination.states are
416  included in the evaluation of the formula, or
417
418  2. It is sure that some (all) of these states are not included in
419  the evaluation.
420 
421  If earlyTermination.mode is McCare_c, then the algorithm can stop as
422  soon as it is guaranteed that either all or none of
423  earlyTermination.states are included in the evaluation.
424
425  These checks are done modulo the care set, but not modulo the fair
426  states, which means that they will not be effective if you
427  require unfair states to be in the evaluation.
428  Typically {ALL, initialStates} will be good. NULL means the option has no
429  effect.
430
431  Debugging only works if this function is called with {ALL,
432  initialStates}.  Otherwise, debugging of the EG formulae may go
433  wrong.
434
435  hintsArray is an array of hints.  Pass NULL and set hintType to
436  Mc_None_c to ignore.
437
438  If hintType is Mc_Global_c, then the formula is evaluated once for
439  each hint, where every hint defines an underapproximation of the
440  formula.  This only works for pure A/E CTL formulae.  If hintType is
441  Mc_Local_c, then every fixpoint goes through the sequence of hints
442  until completion, before moving up to the next temporal operator.
443 
444  ]
445
446  SideEffects []
447
448******************************************************************************/
449mdd_t *
450Mc_FsmEvaluateFormula(
451  Fsm_Fsm_t *fsm,
452  Ctlp_Formula_t *ctlFormula,
453  mdd_t *fairStates,
454  Fsm_Fairness_t *fairCondition,
455  array_t *careStatesArray,
456  Mc_EarlyTermination_t *earlyTermination,
457  Fsm_HintsArray_t *hintsArray,
458  Mc_GuidedSearch_t hintType,
459  Mc_VerbosityLevel verbosity,
460  Mc_DcLevel dcLevel,
461  int buildOnionRing,
462  Mc_GSHScheduleType GSHschedule)
463{
464  mdd_t *hint;      /* to iterate over hintsArray */
465  int   hintnr;     /* idem                       */
466  Ctlp_Approx_t resultApproxType;
467
468  assert(hintType == Mc_None_c || hintsArray != NIL(Fsm_HintsArray_t));
469 
470  if(hintType != Mc_Global_c)
471    return EvaluateFormulaRecur(fsm, ctlFormula, fairStates,
472                                fairCondition, careStatesArray,
473                                earlyTermination, hintsArray, hintType,
474                                Ctlp_Exact_c, &resultApproxType,
475                                verbosity, dcLevel,
476                                buildOnionRing, GSHschedule);
477  else{
478    mdd_t *result = NIL(mdd_t);
479    Ctlp_Approx_t approx;
480
481    if(verbosity >= McVerbosityMax_c)
482      fprintf(vis_stdout, "--Using global hints\n");
483   
484    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
485      if(result != NIL(mdd_t))
486        mdd_free(result);
487     
488      if(verbosity >= McVerbosityMax_c)
489        fprintf(vis_stdout, "--Instantiating global hint %d\n", hintnr);
490
491      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c,
492                          (verbosity >= McVerbosityMax_c));
493
494      approx = mdd_is_tautology(hint, 1) ? Ctlp_Exact_c : Ctlp_Underapprox_c;
495
496      result = EvaluateFormulaRecur(fsm, ctlFormula, fairStates,
497                                    fairCondition, careStatesArray,
498                                    earlyTermination, hintsArray, hintType,
499                                    approx, &resultApproxType, verbosity,
500                                    dcLevel, buildOnionRing, GSHschedule); 
501      /* TBD: take into account (early) termination here */
502    }
503    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
504
505    return result;
506  }
507
508} /* Mc_FsmEvaluateFormula */
509
510
511/**Function********************************************************************
512
513  Synopsis    [Evaluate states satisfying EX target]
514
515  Description [Evaluate states satisfying EX target.  Basically, calls
516  the image package -- all the smarts are in there, parameters for it
517  can be set from the VIS prompt.  In the presence of fairness, a
518  state satisifies EX foo just in case it has a sucessor where foo is
519  true AND that successor can be continued to an infinite path which
520  is fair.]
521
522  SideEffects []
523
524******************************************************************************/
525mdd_t *
526Mc_FsmEvaluateEXFormula(
527  Fsm_Fsm_t *modelFsm,
528  mdd_t *targetMdd,
529  mdd_t *fairStates,
530  array_t *careStatesArray,
531  Mc_VerbosityLevel verbosity,
532  Mc_DcLevel dcLevel)
533{
534  mdd_t *fromLowerBound;
535  mdd_t *fromUpperBound;
536  mdd_t *result;
537  Img_ImageInfo_t * imageInfo;
538 
539  if(Fsm_FsmReadUseUnquantifiedFlag(modelFsm))
540    imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 1, 0);
541  else
542    imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
543
544  /*
545   * The lower bound is the conjunction of the fair states,
546   * and the target states.
547   */
548  fromLowerBound = mdd_and(targetMdd, fairStates, 1, 1);
549  /*
550   * The upper bound is the same as the lower bound.
551   */
552  fromUpperBound = mdd_dup(fromLowerBound);
553
554  result = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
555                fromLowerBound, fromUpperBound, careStatesArray);
556  mdd_free(fromLowerBound);
557  mdd_free(fromUpperBound);
558
559  if (verbosity == McVerbosityMax_c) {
560    static int refCount=0;
561    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
562    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
563    mdd_t *tmpMdd = careStatesArray ?
564        mdd_and_array(result, careStatesArray, 1, 1) : mdd_dup(result);
565    fprintf(vis_stdout, "--EX called %d (bdd_size - %d)\n", ++refCount,
566            mdd_size(result));
567    fprintf(vis_stdout, "--There are %.0f care states satisfying EX formula\n",
568            mdd_count_onset(mddMgr, tmpMdd, psVars));
569    mdd_free(tmpMdd);
570  }
571
572  return result;
573
574} /* Mc_FsmEvaluateEXFormula */
575
576
577/**Function********************************************************************
578
579  Synopsis    [Evaluate states satisfying MX target]
580
581  Description [Compute EX with transition relation that contains input varaibles
582               and then apply universial quantification to get MX target.
583               To use this function, one has to run
584               Fsm_FsmReadOrCreateImageInfoFAFW to create the trasition relation
585               that contains input variables. And Fsm_FsmSetUseUnquantifiedFlag
586               has to be called. That useUnquantifiedFlag is used to specify
587               which imageInfo can be used in image computation.
588               This is function for FateAndFreeWill counterexample generation.]
589
590  SideEffects []
591
592******************************************************************************/
593mdd_t *
594Mc_FsmEvaluateMXFormula(
595  Fsm_Fsm_t *modelFsm,
596  mdd_t *targetMdd,
597  mdd_t *fairStates,
598  array_t *careStatesArray,
599  Mc_VerbosityLevel verbosity,
600  Mc_DcLevel dcLevel)
601{
602  mdd_t *resultBar, *result;
603
604  result = Mc_FsmEvaluateEXFormula(modelFsm, targetMdd, fairStates,
605                                 careStatesArray, verbosity, dcLevel);
606
607  if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) {
608    resultBar = Mc_QuantifyInputFAFW(modelFsm, result);
609    mdd_free(result);
610    result = resultBar;
611  }
612
613  return(result);
614}
615
616/**Function********************************************************************
617
618  Synopsis    [Quantify the input variables]
619
620  Description [Quantify the input variables after applying EX.
621               To use this function, one has to run
622               Fsm_FsmReadOrCreateImageInfoFAFW to create the trasition relation
623               that contains input variables.
624               To get the result of real MX operation, the bdd_smooth_with_cube
625               has to be applied after bdd_consensus_with_cube, but we need
626               those input variables for path generation. If one needs real MX
627               then bdd_smooth_with_cube has to be applied.
628               This is function for FateAndFreeWill counterexample generation.]
629
630  SideEffects []
631
632******************************************************************************/
633bdd_t *
634Mc_QuantifyInputFAFW(Fsm_Fsm_t *fsm, bdd_t *result) 
635{
636  bdd_t *uniCube, *extCube, *newResult;
637  bdd_t *oneMdd, *notResult;
638  mdd_manager *mgr = Fsm_FsmReadMddManager(fsm);
639
640  oneMdd = mdd_one(mgr);
641  uniCube = Fsm_FsmReadUniQuantifyInputCube(fsm);
642  extCube = Fsm_FsmReadExtQuantifyInputCube(fsm);
643  if(!mdd_equal(uniCube, oneMdd)) {
644      /**
645    newResult = bdd_consensus_with_cube(result, uniCube);
646    **/
647    notResult = bdd_not(result);
648    newResult = bdd_smooth_with_cube(notResult, uniCube); 
649    bdd_free(notResult);
650    result    = bdd_not(newResult);
651    bdd_free(newResult);
652  }
653  else {
654    result = mdd_dup(result);
655  }
656  mdd_free(oneMdd);
657  return(result);
658}
659
660
661/**Function********************************************************************
662
663  Synopsis    [Evaluate states satisfying EY target]
664
665  Description [Evaluate states satisfying EY target.]
666
667  SideEffects []
668
669******************************************************************************/
670mdd_t *
671Mc_FsmEvaluateEYFormula(
672  Fsm_Fsm_t *modelFsm,
673  mdd_t *targetMdd,
674  mdd_t *fairStates,
675  array_t *careStatesArray,
676  Mc_VerbosityLevel verbosity,
677  Mc_DcLevel dcLevel)
678{
679  mdd_t *fromLowerBound;
680  mdd_t *fromUpperBound;
681  mdd_t *result;
682
683  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1);
684
685  /*
686   * The lower bound is the conjunction of the fair states,
687   * and the target states.
688   */
689  fromLowerBound = mdd_and(targetMdd, fairStates, 1, 1);
690  /*
691   * The upper bound is the same as the lower bound.
692   */
693  fromUpperBound = fromLowerBound;
694
695  result = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
696                fromLowerBound, fromUpperBound, careStatesArray);
697  mdd_free(fromLowerBound);
698
699  if (verbosity == McVerbosityMax_c) {
700    static int refCount=0;
701    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
702    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
703    mdd_t *tmpMdd = careStatesArray ?
704        mdd_and_array(result, careStatesArray, 1, 1) : mdd_dup(result);
705    fprintf(vis_stdout, "--EY called %d (bdd_size - %d)\n", ++refCount,
706            mdd_size(result));
707    fprintf(vis_stdout, "--There are %.0f care states satisfying EY formula\n",
708            mdd_count_onset(mddMgr, tmpMdd, psVars));
709    mdd_free(tmpMdd);
710  }
711
712  return result;
713
714} /* Mc_FsmEvaluateEYFormula */
715
716
717/**Function********************************************************************
718
719  Synopsis    [Evaluate states satisfying E(invariant U target)]
720
721  Description [Evaluate states satisfying E(invariant U target).
722  Performed by a least fixed point computation -- start with target
723  AND fair, see what can get to this set by a path solely in
724  invariant.  If the onionRings array is not NIL(array_t *), the
725  ``onion rings'' arising in the least fixed point computation are
726  stored in the array, starting from the target.  The onion rings
727  explain how to get from any state in the result to the target.
728
729  The evaluation stops once all (some) of earlyTermination.states
730  have been found (depending on earlyTermination.mode).  See
731  Mc_FsmEvaluateFormula()
732
733  If underapprox is not NIL, it must hold a valid underapproximation
734  of the fixpoint.  This is used to kick off the new computation.
735
736  The arguments hintsArray and hints are used for guided search.  Set
737  hintType to Mc_None_c to ignore.  If hintType is Mc_Local_c,
738  hintsArray should be an array of mdds, of which the last entry is 1.
739  This array will be used to obtain underapproximations of the
740  transition system.  (See Mc_FsmEvaluateFormula.)
741
742  fixpoint is a return argument.  It is true if the formula is
743  evaluated exactly, false if early termination kicked in.  If
744  earlyTermination is NIL, the formula is evaluated exacty, and this
745  argument may be NIL too.
746
747  OnionRings is an array of mdd_t *.  It can be NULL, in which case no
748  onion rings are returned.  If it is not NULL, there are two
749  possibilities.  In the simple case, the onion rings are empty, and
750  underapprox is NULL.  In this case, the onion rings returned explain
751  how to get to the target from any state in the result returned (r).
752  If underapprox u is not NULL, the onion rings that are passed in
753  should explain how to get from any state in u to any state in the
754  target.  Rings will be added by the procudure to explain how to get
755  from the r to a state in underapprox, resulting in an explanation of
756  how to get from a state in r to the target.  ]
757
758  Comment     [Check that evaluation mod reached AND fair will lead to
759  faster convergence.  Also, it is possible there is more (?)
760  flexibility in dont care minimization - use only the layer of the
761  onion rings as set for evaluating EX.]
762
763  SideEffects []
764
765  SeeAlso [Mc_FsmEvaluateFormula, McEvaluateEUFormulaWithGivenTR]
766
767******************************************************************************/
768mdd_t *
769Mc_FsmEvaluateEUFormula(
770  Fsm_Fsm_t *fsm,
771  mdd_t *invariant,
772  mdd_t *target,
773  mdd_t *underapprox,
774  mdd_t *fairStates,
775  array_t *careStatesArray,
776  Mc_EarlyTermination_t *earlyTermination,
777  Fsm_HintsArray_t *hintsArray,
778  Mc_GuidedSearch_t hintType,
779  array_t *onionRings,
780  Mc_VerbosityLevel verbosity,
781  Mc_DcLevel dcLevel,
782  boolean *fixpoint)
783{
784  /* should be strengthened to check that rings supply a correct explanation.
785   */
786  /*check out
787   *  assert(underapprox == NULL || onionRings == NULL ||
788   *     array_n(onionRings) != 0);  */
789 
790  if(hintType != Mc_Local_c)
791    /* postcondition: rings should explain how to get from return value to
792     * target.
793     */
794    return McEvaluateEUFormulaWithGivenTR(fsm, invariant, target,
795                                          underapprox, fairStates,
796                                          careStatesArray,
797                                          earlyTermination, onionRings,
798                                          verbosity, dcLevel, fixpoint); 
799  else{
800    mdd_t *iterate, *newiterate;
801    mdd_t *hint;
802    int hintnr;
803
804    if(verbosity >= McVerbosityMax_c)
805        fprintf(vis_stdout, "--Using local hints\n");
806
807    if(underapprox != NIL(mdd_t))
808      iterate = mdd_dup(underapprox);
809    else
810      iterate = mdd_zero(Fsm_FsmReadMddManager(fsm));
811
812    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
813        if(verbosity >= McVerbosityMax_c)
814            fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
815      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c,
816                          (verbosity >= McVerbosityMax_c));
817     
818      newiterate =
819        McEvaluateEUFormulaWithGivenTR(fsm, invariant, target, iterate,
820                                       fairStates, careStatesArray,
821                                       earlyTermination, onionRings,
822                                       verbosity, dcLevel, fixpoint);   
823      mdd_free(iterate);
824      iterate = newiterate;
825
826      /* check if we can terminate without considering all hints */ 
827      if(mdd_is_tautology(iterate, 1)){
828        *fixpoint = 1;
829        break;
830      }
831      if(McCheckEarlyTerminationForUnderapprox(earlyTermination, iterate,
832                                               careStatesArray)){ 
833        *fixpoint = 0;
834        break;
835      }
836
837    }/* for all hints */
838    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
839
840    /* postcondition: rings should explain how to get from return value to
841     * target.
842     */
843    return iterate;
844  }/* if hinttype */
845
846} /* Mc_FsmEvaluateEUFormula */
847
848
849/**Function********************************************************************
850
851  Synopsis    [Evaluate states satisfying E(invariant S source)]
852
853  Description [Evaluate states satisfying E(invariant U target).
854  Performed by a least fixed point computation -- start with source
855  AND fair, see what can be reached from this set by a path solely in
856  invariant.  If the onionRings array is not NIL(array_t *), the
857  ``onion rings'' arising in the least fixed point computation are
858  stored in the array, starting from the target.
859
860  The evaluation stops once all (some) of earlyTermination.states
861  have been found (depending on earlyTermination.mode).  See
862  Mc_FsmEvaluateFormula()
863
864  If underapprox is not NIL, it must hold a valid underapproximation
865  of the fixpoint.  This is used to kick off the new computation.
866
867  The arguments hintsArray and hints are used for guided search.  Set
868  hintType to Mc_None_c to ignore.  If hintType is Mc_Local_c,
869  hintsArray should be an array of mdds, of which the last entry is 1.
870  This array will be used to obtain underapproximations of the
871  transition system.  (See Mc_FsmEvaluateFormula.)
872
873  fixpoint is a return argument.  It is true if the formula is
874  evaluated exactly, false if early termination kicked in.  If
875  earlyTermination is NIL, the formula is evaluated exacty, and this
876  argument may be NIL too.
877
878  OnionRIngs is an array of mdd_t *.  It should be empty on call if
879  you want debug info, NULL otherwise.  After the call, it contains
880  the onion rings (frontier sets) that occured while computing the
881  ES.  This is used for debugging.]
882
883  Comment [Check that evaluation mod reached AND fair will lead to
884  faster convergence.  Also, it is possible there is more (?)
885  flexibility in don't care minimization - use only the layer of the
886  onion rings as set for evaluating EX.]
887
888  SideEffects []
889
890  SeeAlso [Mc_FsmEvaluateFormula, McEvaluateESFormulaWithGivenTR]
891
892******************************************************************************/
893mdd_t *
894Mc_FsmEvaluateESFormula(
895  Fsm_Fsm_t *fsm,
896  mdd_t *invariant,
897  mdd_t *source,
898  mdd_t *underapprox,
899  mdd_t *fairStates,
900  array_t *careStatesArray,
901  Mc_EarlyTermination_t *earlyTermination,
902  Fsm_HintsArray_t *hintsArray,
903  Mc_GuidedSearch_t hintType,
904  array_t *onionRings,
905  Mc_VerbosityLevel verbosity,
906  Mc_DcLevel dcLevel,
907  boolean *fixpoint)
908{
909  /* should be strengthened to check that rings supply a correct explanation.
910   */
911  assert(underapprox == NULL || onionRings == NULL ||
912         array_n(onionRings) != 0);
913
914  if(hintType != Mc_Local_c)
915    /* postcondition: rings should explain how to get from return value to
916     * target.
917     */
918    return McEvaluateESFormulaWithGivenTR(fsm, invariant, source,
919                                          underapprox, fairStates,
920                                          careStatesArray,
921                                          earlyTermination, onionRings,
922                                          verbosity, dcLevel, fixpoint); 
923  else{
924    mdd_t *iterate, *newiterate;
925    mdd_t *hint;
926    int hintnr;
927
928    if(verbosity >= McVerbosityMax_c)
929        fprintf(vis_stdout, "--Using local hints\n");
930
931    if(underapprox != NIL(mdd_t))
932      iterate = mdd_dup(underapprox);
933    else
934      iterate = mdd_zero(Fsm_FsmReadMddManager(fsm));
935
936    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
937        if(verbosity >= McVerbosityMax_c)
938            fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
939      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c,
940                          (verbosity >= McVerbosityMax_c));
941     
942      newiterate =
943        McEvaluateESFormulaWithGivenTR(fsm, invariant, source, iterate,
944                                       fairStates, careStatesArray,
945                                       earlyTermination, onionRings,
946                                       verbosity, dcLevel, fixpoint);   
947      mdd_free(iterate);
948      iterate = newiterate;
949
950      /* check if we can terminate without considering all hints */ 
951      if(mdd_is_tautology(iterate, 1)){
952        *fixpoint = 1;
953        break;
954      }
955      if(McCheckEarlyTerminationForUnderapprox(earlyTermination, iterate,
956                                               careStatesArray)){ 
957        *fixpoint = 0;
958        break;
959      }
960
961    }/* for all hints */
962    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
963
964    /* postcondition: rings should explain how to get from return value to
965     * target.
966     */
967
968    return iterate;
969  }/* if hinttype */
970
971} /* Mc_FsmEvaluateESFormula */
972
973mdd_t *
974Mc_FsmEvaluateAUFormula(
975  Fsm_Fsm_t *fsm,
976  mdd_t *invariant,
977  mdd_t *target,
978  mdd_t *underapprox,
979  mdd_t *fairStates,
980  array_t *careStatesArray,
981  Mc_EarlyTermination_t *earlyTermination,
982  Fsm_HintsArray_t *hintsArray,
983  Mc_GuidedSearch_t hintType,
984  array_t *onionRings,
985  Mc_VerbosityLevel verbosity,
986  Mc_DcLevel dcLevel,
987  boolean *fixpoint)
988{
989
990  return McEvaluateAUFormulaWithGivenTR(fsm, invariant, target,
991                                        underapprox, fairStates,
992                                        careStatesArray,
993                                        earlyTermination, onionRings,
994                                        verbosity, dcLevel, fixpoint);
995
996}
997
998
999
1000/**Function********************************************************************
1001
1002  Synopsis    [Evaluate states satisfying EG invariant]
1003
1004  Description [Evaluate states satisfying EG invariant.  This is done
1005  by starting with all states marked with the invariant.  From this
1006  initial set, recursively remove states that can not reach Buechi
1007  contraints (through paths entirely within the current set).
1008
1009  If overapprox is not nil, then it is a valid overapproximation to the
1010  satisfiable set of the formula that will be used to kick off the
1011  computation.
1012
1013  pOnionRingsArrayForDbg is a pointer to (a pointer to) an array of
1014  arrays of mdd_t *s.  Upon calling this formula, it should point to
1015  an empty array if you want debug information, or be NIL (or a
1016  pointer to NIL) if you do not.  After the call, it points to an
1017  array that contains one entry for every fairness constraint: entry i
1018  contains the onionrings for the last EU computation that was
1019  performed for fairness constraint i.  There are two exceptions: if
1020  the satisfying set is 0, or if early termination kicks in, the onion
1021  ring array is not changed.
1022
1023  The arguments hintsArray and hints are used for guided search.  Set
1024  hintType to Mc_None_c to ignore.  If hintType is Mc_Local_c,
1025  hintsArray should be an array of mdds, of which the last entry is 1.
1026  This array will be used to obtain overapproximations of the
1027  transition system (See Mc_FsmEvaluateFormula).
1028
1029  fixpoint is a return argument.  It is true if the formula is
1030  evaluated exactly, false if early termination kicked in.  If
1031  earlyTermination is NIL, the formula is evaluated exacty, and this
1032  argument may be NIL too.  See Mc_FsmEvaluateFormula for a discussion
1033  of early termination.]
1034
1035  SideEffects []
1036
1037  SeeAlso     [Mc_FsmEvaluateFormula]
1038
1039******************************************************************************/
1040mdd_t *
1041Mc_FsmEvaluateEGFormula(
1042  Fsm_Fsm_t *fsm,
1043  mdd_t *invariant,
1044  mdd_t *overapprox,
1045  mdd_t *fairStates,
1046  Fsm_Fairness_t *modelFairness,
1047  array_t *careStatesArray,
1048  Mc_EarlyTermination_t *earlyTermination,
1049  Fsm_HintsArray_t *hintsArray,
1050  Mc_GuidedSearch_t hintType,
1051  array_t **pOnionRingsArrayForDbg,
1052  Mc_VerbosityLevel verbosity,
1053  Mc_DcLevel dcLevel,
1054  boolean *fixpoint,
1055  Mc_GSHScheduleType GSHschedule)
1056{
1057  /* Illegal to pass in onion rings. */
1058#if 0
1059  assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
1060  *pOnionRingsArrayForDbg == NIL(array_t) ||
1061  array_n(*pOnionRingsArrayForDbg) == 0);
1062#endif
1063  if(hintType != Mc_Local_c)
1064    if (GSHschedule == McGSH_old_c) {
1065      return McEvaluateEGFormulaWithGivenTR(fsm, invariant, overapprox,
1066                                            fairStates,
1067                                            modelFairness, careStatesArray,
1068                                            earlyTermination,
1069                                            pOnionRingsArrayForDbg,
1070                                            verbosity,
1071                                            dcLevel, fixpoint);
1072    } else {
1073      return McFsmEvaluateEGFormulaUsingGSH(fsm, invariant, overapprox,
1074                                            fairStates,
1075                                            modelFairness, careStatesArray,
1076                                            earlyTermination,
1077                                            pOnionRingsArrayForDbg, verbosity,
1078                                            dcLevel, fixpoint, GSHschedule);
1079    }
1080  else {
1081    mdd_t *iterate, *newiterate;
1082    mdd_t *hint;
1083    int hintnr;
1084    boolean useRings;
1085
1086    useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
1087                *pOnionRingsArrayForDbg != NIL(array_t));
1088   
1089    if(verbosity >= McVerbosityMax_c)
1090        fprintf(vis_stdout, "** mc Info: Using local hints\n");
1091
1092    if(overapprox != NIL(mdd_t))
1093      iterate = mdd_dup(overapprox);
1094    else
1095      iterate = mdd_one(Fsm_FsmReadMddManager(fsm));
1096   
1097    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
1098        if(verbosity >= McVerbosityMax_c)
1099            fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
1100      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Overapprox_c,
1101                          (verbosity >= McVerbosityMax_c));
1102
1103      /* old onionrings go stale.  Fry 'em */
1104      if(useRings){
1105        mdd_array_array_free(*pOnionRingsArrayForDbg);
1106        *pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
1107      }
1108
1109      if (GSHschedule == McGSH_old_c) {
1110        newiterate =
1111          McEvaluateEGFormulaWithGivenTR(fsm, invariant, iterate, fairStates,
1112                                         modelFairness, careStatesArray,
1113                                         earlyTermination,
1114                                         pOnionRingsArrayForDbg,
1115                                         verbosity, dcLevel, fixpoint);
1116      } else {
1117        newiterate =
1118          McFsmEvaluateEGFormulaUsingGSH(fsm, invariant, iterate,
1119                                         fairStates,
1120                                         modelFairness, careStatesArray,
1121                                         earlyTermination,
1122                                         pOnionRingsArrayForDbg, verbosity,
1123                                         dcLevel, fixpoint, GSHschedule);
1124      }
1125      mdd_free(iterate);
1126      iterate = newiterate;
1127
1128      /* check if we can terminate without considering all hints */ 
1129      if(mdd_is_tautology(iterate, 0)){
1130        *fixpoint = 1;
1131        break;
1132      }
1133      if(McCheckEarlyTerminationForOverapprox(earlyTermination, iterate,
1134                                              careStatesArray)){ 
1135        *fixpoint = 0;
1136        break;
1137      }
1138
1139    } /* For all hints */
1140    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
1141
1142    return iterate;
1143  }/* if hinttype */
1144
1145} /* Mc_FsmEvaluateEGFormula */
1146
1147
1148/**Function********************************************************************
1149
1150  Synopsis    [Evaluate states satisfying EH invariant.]
1151
1152  Description [Evaluate states satisfying EH invariant.  This is done
1153  by starting with all states marked with the invariant.  From this
1154  initial set, recursively remove states that cannot reach Buechi
1155  contraints (through paths entirely within the current set).
1156
1157  If overapprox is not nil, then it is a valid overapproximation to the
1158  satisfiable set of the formula that will be used to kick off the
1159  computation.
1160
1161  pOnionRingsArrayForDbg is a pointer to (a pointer to) an array of
1162  arrays of mdd_t *s.  Upon calling this formula, it should point to
1163  an empty array if you want debug information, or be NIL (or a
1164  pointer to NIL) if you do not.  After the call, it points to an
1165  array that contains one entry for every fairness constraint: entry i
1166  contains the onionrings for the last ES computation that was
1167  performed for fairness constraint i.  There are two exceptions: if
1168  the satisfying set is 0, or if early termination kicks in, the onion
1169  ring array is not changed.
1170
1171  The arguments hintsArray and hints are used for guided search.  Set
1172  hintType to Mc_None_c to ignore.  If hintType is Mc_Local_c,
1173  hintsArray should be an array of mdds, of which the last entry is 1.
1174  This array will be used to obtain overapproximations of the
1175  transition system (See Mc_FsmEvaluateFormula).
1176
1177  fixpoint is a return argument.  It is true if the formula is
1178  evaluated exactly, false if early termination kicked in.  If
1179  earlyTermination is NIL, the formula is evaluated exacty, and this
1180  argument may be NIL too.  See Mc_FsmEvaluateFormula for a discussion
1181  of early termination.]
1182
1183  SideEffects []
1184
1185  SeeAlso [Mc_FsmEvaluateFormula]
1186
1187******************************************************************************/
1188mdd_t *
1189Mc_FsmEvaluateEHFormula(
1190  Fsm_Fsm_t *fsm,
1191  mdd_t *invariant,
1192  mdd_t *overapprox,
1193  mdd_t *fairStates,
1194  Fsm_Fairness_t *modelFairness,
1195  array_t *careStatesArray,
1196  Mc_EarlyTermination_t *earlyTermination,
1197  Fsm_HintsArray_t *hintsArray,
1198  Mc_GuidedSearch_t hintType,
1199  array_t **pOnionRingsArrayForDbg,
1200  Mc_VerbosityLevel verbosity,
1201  Mc_DcLevel dcLevel,
1202  boolean *fixpoint,
1203  Mc_GSHScheduleType GSHschedule)
1204{
1205  /* Illegal to pass in onion rings. */
1206  assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
1207         *pOnionRingsArrayForDbg == NIL(array_t) ||
1208         array_n(*pOnionRingsArrayForDbg) == 0);
1209
1210  if(hintType != Mc_Local_c)
1211    if (GSHschedule == McGSH_old_c) {
1212      return McEvaluateEHFormulaWithGivenTR(fsm, invariant, overapprox,
1213                                            fairStates,
1214                                            modelFairness, careStatesArray,
1215                                            earlyTermination,
1216                                            pOnionRingsArrayForDbg,
1217                                            verbosity,
1218                                            dcLevel, fixpoint);
1219    } else {
1220      return McFsmEvaluateEHFormulaUsingGSH(fsm, invariant, overapprox,
1221                                            fairStates,
1222                                            modelFairness, careStatesArray,
1223                                            earlyTermination,
1224                                            pOnionRingsArrayForDbg, verbosity,
1225                                            dcLevel, fixpoint, GSHschedule);
1226    }
1227  else {
1228    mdd_t *iterate, *newiterate;
1229    mdd_t *hint;
1230    int hintnr;
1231    boolean useRings;
1232
1233    useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
1234                *pOnionRingsArrayForDbg != NIL(array_t));
1235   
1236    if(verbosity >= McVerbosityMax_c)
1237        fprintf(vis_stdout, "** mc Info: Using local hints\n");
1238
1239    if(overapprox != NIL(mdd_t))
1240      iterate = mdd_dup(overapprox);
1241    else
1242      iterate = mdd_one(Fsm_FsmReadMddManager(fsm));
1243   
1244    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
1245        if(verbosity >= McVerbosityMax_c)
1246            fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr);
1247      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Overapprox_c,
1248                          (verbosity >= McVerbosityMax_c));
1249
1250      /* old onionrings go stale.  Fry 'em */
1251      if(useRings){
1252        mdd_array_array_free(*pOnionRingsArrayForDbg);
1253        *pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
1254      }
1255
1256      if (GSHschedule == McGSH_old_c) {
1257        newiterate =
1258          McEvaluateEHFormulaWithGivenTR(fsm, invariant, iterate, fairStates,
1259                                         modelFairness, careStatesArray,
1260                                         earlyTermination,
1261                                         pOnionRingsArrayForDbg,
1262                                         verbosity, dcLevel, fixpoint);
1263      } else {
1264        newiterate =
1265          McFsmEvaluateEHFormulaUsingGSH(fsm, invariant, iterate,
1266                                         fairStates,
1267                                         modelFairness, careStatesArray,
1268                                         earlyTermination,
1269                                         pOnionRingsArrayForDbg, verbosity,
1270                                         dcLevel, fixpoint, GSHschedule);
1271      }
1272      mdd_free(iterate);
1273      iterate = newiterate;
1274
1275      /* check if we can terminate without considering all hints */ 
1276      if(mdd_is_tautology(iterate, 0)){
1277        *fixpoint = 1;
1278        break;
1279      }
1280      if(McCheckEarlyTerminationForOverapprox(earlyTermination, iterate,
1281                                              careStatesArray)){ 
1282        *fixpoint = 0;
1283        break;
1284      }
1285
1286    } /* For all hints */
1287    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
1288
1289    return iterate;
1290  }/* if hinttype */
1291
1292} /* Mc_FsmEvaluateEHFormula */
1293
1294
1295/**Function********************************************************************
1296
1297  Synopsis    [Evaluate states satisfying FwdUntil]
1298
1299  Description [Evaluate states satisfying FwdUntil.]
1300
1301  Comment []
1302
1303  SideEffects []
1304
1305******************************************************************************/
1306mdd_t *
1307Mc_FsmEvaluateFwdUFormula(
1308  Fsm_Fsm_t *modelFsm,
1309  mdd_t *targetMdd,
1310  mdd_t *invariantMdd,
1311  mdd_t *fairStates,
1312  array_t *careStatesArray,
1313  array_t *onionRings,
1314  Mc_VerbosityLevel verbosity,
1315  Mc_DcLevel dcLevel)
1316{
1317  mdd_t *aMdd;
1318  mdd_t *bMdd;
1319  mdd_t *cMdd;
1320  mdd_t *resultMdd;
1321  mdd_t *ringMdd;
1322  int nImgComps;
1323
1324  /*                                                        t
1325  ** E[p U q]      = lfp Z[q V (p ^ EX(Z))]   :   p p ... p q
1326  ** FwdUntil(p,q) = lfp Z[p V EY(Z ^ q)]     :             pq q q ... q
1327  */
1328
1329  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
1330  resultMdd = mdd_and(targetMdd, fairStates, 1, 1);
1331  ringMdd = mdd_dup(resultMdd);
1332
1333  /* if until is trivially satisfied, */
1334  if (onionRings) {
1335    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
1336  }
1337  if (mdd_is_tautology(fairStates, 1)) {
1338    if (mdd_equal_mod_care_set_array(invariantMdd, resultMdd, careStatesArray))
1339    { 
1340      bdd_free(ringMdd);
1341      return(resultMdd);
1342    }
1343  } else {
1344    bdd_t *trivialCheck = mdd_and(invariantMdd, fairStates, 1, 1);
1345    if (mdd_equal_mod_care_set_array(trivialCheck, resultMdd, careStatesArray)) {
1346      bdd_free(trivialCheck);
1347      bdd_free(ringMdd);
1348      return(resultMdd);
1349    }
1350    bdd_free(trivialCheck);
1351  }
1352
1353  while (TRUE) {
1354    aMdd = mdd_and(ringMdd, invariantMdd, 1, 1);
1355    mdd_free(ringMdd);
1356    bMdd = Mc_FsmEvaluateEYFormula(modelFsm, aMdd, fairStates, careStatesArray,
1357                                   verbosity, dcLevel);
1358    mdd_free(aMdd);
1359    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
1360    mdd_free(bMdd);
1361
1362    if (mdd_equal_mod_care_set_array(cMdd, resultMdd, careStatesArray)) {
1363      mdd_free(cMdd);
1364      break;
1365    }
1366
1367    if (dcLevel >= McDcLevelRchFrontier_c) {
1368      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
1369      ringMdd = bdd_between(tmpMdd, cMdd);
1370      if (verbosity == McVerbosityMax_c) {
1371        fprintf(vis_stdout,
1372          "-- FwdU |A(n+1)-A(n)| = %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
1373          mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
1374      }
1375      mdd_free(tmpMdd);
1376    }
1377    else {
1378      ringMdd = mdd_dup(cMdd);
1379      if (verbosity == McVerbosityMax_c) {
1380        fprintf(vis_stdout, "-- FwdU |ringMdd| = %d\n", mdd_size(ringMdd));
1381      }
1382    }
1383
1384    mdd_free(resultMdd);
1385    resultMdd = cMdd;
1386    if (onionRings) {
1387      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
1388    }
1389  } /* while(!termination) for LFP */
1390
1391  /* Print some debug info */
1392  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
1393    static int refCount=0;
1394    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
1395    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
1396
1397    if (verbosity == McVerbosityMax_c) {
1398      mdd_t *tmpMdd = careStatesArray ?
1399                      mdd_and_array(resultMdd, careStatesArray, 1, 1) :
1400                      mdd_dup(resultMdd);
1401      fprintf(vis_stdout, "--FwdU called %d (bdd_size - %d)\n",
1402                ++refCount, mdd_size(resultMdd));
1403      fprintf(vis_stdout,
1404                "--There are %.0f care states satisfying FwdU formula\n",
1405                mdd_count_onset(mddMgr, tmpMdd, psVars));
1406#ifdef DEBUG_MC
1407      /* The following 2 lines are just for debug */
1408      fprintf(vis_stdout, "FwdU satisfying minterms :\n");
1409      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
1410#endif
1411      mdd_free(tmpMdd);
1412    } else {
1413      fprintf(vis_stdout,
1414                "--There are %.0f states satisfying FwdU formula\n",
1415                mdd_count_onset(mddMgr, resultMdd, psVars));
1416    }
1417    fprintf(vis_stdout, "--FwdU: %d image computations\n",
1418      Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
1419  }
1420
1421  return resultMdd;
1422}
1423
1424
1425/**Function********************************************************************
1426
1427  Synopsis    [Evaluate states satisfying FwdG invariant]
1428
1429  Description [Evaluate states satisfying FwdG invariant.]
1430
1431  SideEffects []
1432
1433******************************************************************************/
1434mdd_t *
1435Mc_FsmEvaluateFwdGFormula(
1436  Fsm_Fsm_t *modelFsm,
1437  mdd_t *targetMdd,
1438  mdd_t *invariantMdd,
1439  mdd_t *fairStates,
1440  Fsm_Fairness_t *modelFairness,
1441  array_t *careStatesArray,
1442  array_t *onionRingsArrayForDbg,
1443  Mc_VerbosityLevel verbosity,
1444  Mc_DcLevel dcLevel)
1445{
1446  mdd_t *resultMdd, *invariant;
1447  array_t *onionRings;
1448  int nImgComps;
1449
1450  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
1451  onionRings = NIL(array_t);
1452
1453  invariant = McForwardReachable(modelFsm, targetMdd, invariantMdd, fairStates,
1454                                 careStatesArray, onionRings, verbosity,
1455                                 dcLevel);
1456  resultMdd = Mc_FsmEvaluateFwdEHFormula(modelFsm, invariant, fairStates,
1457                                         modelFairness, careStatesArray,
1458                                         onionRingsArrayForDbg, verbosity,
1459                                         dcLevel);
1460  mdd_free(invariant);
1461
1462  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
1463    fprintf(vis_stdout, "--FwdG: %d image computations\n",
1464      Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
1465  }
1466#ifdef DEBUG_MC
1467  /* The following 2 lines are just for debug */
1468  if ((verbosity == McVerbosityMax_c)) {
1469    fprintf(vis_stdout, "FwdG satisfying minterms :\n");
1470    (void)_McPrintSatisfyingMinterms(resultMdd, modelFsm);
1471  }
1472#endif
1473  return resultMdd;
1474}
1475
1476
1477
1478/**Function********************************************************************
1479
1480  Synopsis    [Evaluate states satisfying EH invariant]
1481
1482  Description [Evaluate states satisfying EH invariant.]
1483
1484  SideEffects []
1485
1486******************************************************************************/
1487mdd_t *
1488Mc_FsmEvaluateFwdEHFormula(
1489  Fsm_Fsm_t *modelFsm,
1490  mdd_t *invariantMdd,
1491  mdd_t *fairStates,
1492  Fsm_Fairness_t *modelFairness,
1493  array_t *careStatesArray,
1494  array_t *onionRingsArrayForDbg,
1495  Mc_VerbosityLevel verbosity,
1496  Mc_DcLevel dcLevel)
1497{
1498  int i;
1499  array_t *onionRings = NIL(array_t);
1500  array_t *tmpOnionRingsArrayForDbg = NIL(array_t);
1501  mdd_manager *mddManager = Fsm_FsmReadMddManager(modelFsm);
1502  mdd_t *mddOne = mdd_one(mddManager);
1503  mdd_t *Zmdd;
1504  int nIterations = 0;
1505  int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
1506
1507  /*
1508  **  EG(f) = gfp Z[f ^ EX(Z)]
1509  **  EH(f) = gfp Z[f ^ EY(Z)]
1510  **
1511  **  EcG(f) = gfp Z[f ^ EX( ^ E[Z U Z ^ c])]
1512  **                        c<C
1513  **  EcH(f) = gfp Z[f ^ EY( ^ Reachable(c,Z))]
1514  **                        c<C
1515  **  Reachable(p,q) = FwdUntil(p,q) ^ q
1516  */
1517
1518  array_t *buchiFairness = array_alloc(mdd_t *, 0);
1519  if (modelFairness) {
1520    if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
1521      (void) fprintf(vis_stdout,
1522         "** mc error: non-Buechi fairness constraints not supported\n");
1523      return NIL(mdd_t);
1524    }
1525    else {
1526      int j;
1527      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
1528      for (j = 0; j < numBuchi; j++) {
1529        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
1530                                                careStatesArray, dcLevel);
1531        array_insert_last(mdd_t *, buchiFairness, tmpMdd);
1532      }
1533    }
1534  }
1535  else {
1536    array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager));
1537  }
1538
1539  if (onionRingsArrayForDbg !=NIL(array_t)) {
1540    tmpOnionRingsArrayForDbg = array_alloc(array_t *, 0);
1541  }
1542
1543  Zmdd = mdd_dup(invariantMdd);
1544  while (TRUE) {
1545    mdd_t *ZprimeMdd = mdd_dup(Zmdd);
1546    mdd_t *conjunctsMdd = NIL(mdd_t);
1547    mdd_t *AAmdd = mdd_dup(Zmdd);
1548
1549    nIterations++;
1550    for (i = 0; i < array_n(buchiFairness); i++) {
1551      mdd_t *aMdd, *bMdd;
1552      mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i);
1553
1554      if (tmpOnionRingsArrayForDbg) {
1555        onionRings = array_alloc(mdd_t *, 0);
1556        array_insert_last(array_t *, tmpOnionRingsArrayForDbg, onionRings);
1557      }
1558
1559      aMdd = McForwardReachable(modelFsm, FiMdd, AAmdd, mddOne, careStatesArray,
1560                                onionRings, verbosity, dcLevel);
1561      bMdd = Mc_FsmEvaluateEYFormula(modelFsm, aMdd, mddOne, careStatesArray,
1562                                     verbosity, dcLevel);
1563      mdd_free(aMdd);
1564
1565      if (conjunctsMdd == NIL(mdd_t)) {
1566        conjunctsMdd = mdd_dup(bMdd);
1567      }
1568      else {
1569        mdd_t *tmpMdd = mdd_and(bMdd, conjunctsMdd, 1, 1);
1570        mdd_free(conjunctsMdd);
1571        conjunctsMdd = tmpMdd;
1572      }
1573      mdd_free(AAmdd); AAmdd = mdd_and(conjunctsMdd, invariantMdd, 1, 1);
1574      mdd_free(bMdd);
1575    }
1576    mdd_free(AAmdd);
1577
1578    mdd_free(ZprimeMdd);
1579    ZprimeMdd = mdd_and(invariantMdd, conjunctsMdd, 1, 1);
1580    mdd_free(conjunctsMdd);
1581
1582    if (mdd_equal_mod_care_set_array(ZprimeMdd, Zmdd, careStatesArray)) {
1583      mdd_free(ZprimeMdd);
1584      break;
1585    }
1586
1587    mdd_free(Zmdd);
1588    Zmdd = ZprimeMdd;
1589
1590    if (tmpOnionRingsArrayForDbg) {
1591      arrayForEachItem(array_t *, tmpOnionRingsArrayForDbg, i, onionRings) {
1592        mdd_array_free(onionRings);
1593      }
1594      array_free(tmpOnionRingsArrayForDbg);
1595      tmpOnionRingsArrayForDbg = array_alloc(array_t *, 0);
1596    }
1597  }
1598
1599  if (onionRingsArrayForDbg != NIL(array_t)) {
1600    arrayForEachItem(array_t *, tmpOnionRingsArrayForDbg, i, onionRings) {
1601      array_insert_last(array_t *, onionRingsArrayForDbg, onionRings);
1602    }
1603    array_free(tmpOnionRingsArrayForDbg);
1604  }
1605
1606  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
1607    if (onionRingsArrayForDbg) {
1608      for (i = 0; i < array_n(onionRingsArrayForDbg); i++) {
1609        int j;
1610        mdd_t *Fi = array_fetch(mdd_t *, buchiFairness, i);
1611        array_t *onionRings = array_fetch(array_t *, onionRingsArrayForDbg, i);
1612        for (j = 0; j < array_n(onionRings); j++) {
1613          mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
1614          if (j == 0) {
1615            if (!mdd_lequal(ring, Fi, 1, 1)) {
1616              fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
1617              fprintf(vis_stderr,
1618                      "inner most ring not in Fi(fairness constraint).\n");
1619            }
1620          }
1621          if (!mdd_lequal(ring, Zmdd, 1, 1)) {
1622            fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
1623            fprintf(vis_stderr, "onion ring of last FwdU fails invariant\n");
1624          }
1625        }
1626      }
1627    }
1628
1629    if (verbosity == McVerbosityMax_c) {
1630      mdd_t *tmpMdd = careStatesArray ?
1631                      mdd_and_array(Zmdd, careStatesArray, 1, 1) :
1632                      mdd_dup(Zmdd);
1633      fprintf(vis_stdout,
1634              "--There are %.0f care states satisfying EH formula\n",
1635              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd,
1636                              Fsm_FsmReadPresentStateVars(modelFsm)));
1637#ifdef DEBUG_MC
1638      /* The following 2 lines are just for debug */
1639      fprintf(vis_stdout, "EH satisfying minterms :\n");
1640      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
1641#endif
1642      mdd_free(tmpMdd);
1643    } else {
1644      fprintf(vis_stdout, "--There are %.0f states satisfying EH formula\n",
1645              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), Zmdd,
1646                              Fsm_FsmReadPresentStateVars(modelFsm)));
1647    }
1648
1649    fprintf(vis_stdout, "--EH: %d iterations, %d image computations\n",
1650      nIterations, Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
1651  }
1652
1653  mdd_array_free(buchiFairness);
1654  mdd_free(mddOne);
1655
1656  return Zmdd;
1657
1658} /* Mc_FsmEvaluateFwdEHFormula */
1659
1660
1661/*---------------------------------------------------------------------------*/
1662/* Definition of internal functions                                          */
1663/*---------------------------------------------------------------------------*/
1664
1665/**Function********************************************************************
1666
1667  Synopsis    [Evaluate states satisfying E(invariant U target), given
1668  a transition relation]
1669
1670  Description [Does the same as Mc_FsmEvaluateEUFormula, minus the hints.]
1671
1672  SeeAlso     [Mc_FsmEvaluateEUFormula]
1673 
1674  SideEffects []
1675
1676******************************************************************************/
1677mdd_t *
1678McEvaluateEUFormulaWithGivenTR(
1679  Fsm_Fsm_t *modelFsm,
1680  mdd_t *invariantMdd,
1681  mdd_t *targetMdd,
1682  mdd_t *underapprox,
1683  mdd_t *fairStates,
1684  array_t *careStatesArray,
1685  Mc_EarlyTermination_t *earlyTermination,
1686  array_t *onionRings,
1687  Mc_VerbosityLevel verbosity,
1688  Mc_DcLevel dcLevel,
1689  boolean *fixpoint
1690  )
1691{
1692  mdd_t *aMdd;
1693  mdd_t *bMdd;
1694  mdd_t *cMdd;
1695  mdd_t *resultMdd;
1696  mdd_t *ringMdd;
1697  int nPreComps;
1698  boolean term_tautology = FALSE; /* different termination conditions */
1699  boolean term_early     = FALSE; 
1700  boolean term_fixpoint  = FALSE; 
1701
1702  nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
1703  resultMdd = mdd_and(targetMdd, fairStates, 1, 1);
1704
1705  if(underapprox != NIL(mdd_t)){
1706    mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
1707    mdd_free(resultMdd);
1708    resultMdd = tmp;
1709  }
1710
1711  ringMdd = mdd_dup(resultMdd);
1712
1713  if (onionRings) {
1714    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
1715  }
1716 
1717  /* if until is trivially satisfied, or
1718     the early termination condition holds*/ 
1719  {
1720    bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
1721    boolean trivial;
1722
1723    trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
1724                                            1, 1, careStatesArray);
1725    /* the lequal also takes care of the case where result = 1 */
1726    if(trivial ||
1727       McCheckEarlyTerminationForUnderapprox(earlyTermination,
1728                                             resultMdd,
1729                                             careStatesArray)){
1730      bdd_free(fairInvariantStates);
1731      bdd_free(ringMdd);
1732
1733      /* trivially satisfied means that the fixpoint is complete.  If this
1734         information is requested, give it. */
1735      if(fixpoint != NIL(boolean))
1736        *fixpoint = trivial;
1737      return(resultMdd);
1738    }
1739    bdd_free(fairInvariantStates);
1740  }
1741
1742  /* The LFP loop */
1743  while (!term_fixpoint && !term_tautology && !term_early) {
1744    /* If dclevel is maximal, ringbdd is between the frontier and the
1745       reached set */
1746    aMdd = Mc_FsmEvaluateEXFormula(modelFsm, ringMdd, fairStates,
1747                                   careStatesArray, verbosity, dcLevel);
1748    mdd_free(ringMdd);
1749
1750    bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
1751    mdd_free(aMdd);
1752
1753    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
1754    mdd_free(bMdd);
1755
1756    /* Can we stop?  The tautology condition can be weakened to
1757       cMdd <= careStatesArray */
1758    term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
1759                                                 careStatesArray);
1760    if(!term_fixpoint)
1761      term_tautology = mdd_is_tautology(cMdd, 1);
1762    if(!term_fixpoint && !term_tautology)
1763      term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, 
1764                                                         cMdd,
1765                                                         careStatesArray);
1766
1767    /* Print some debug info, and set ringmdd */
1768    if (dcLevel >= McDcLevelRchFrontier_c) {
1769      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
1770      ringMdd = bdd_between(tmpMdd, cMdd);
1771      if (verbosity == McVerbosityMax_c) {
1772        fprintf(vis_stdout,
1773                "--EU |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
1774                mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
1775      }
1776      mdd_free(tmpMdd);
1777    }
1778    else {
1779      ringMdd = mdd_dup(cMdd);
1780      if (verbosity == McVerbosityMax_c) {
1781          fprintf(vis_stdout, "-- EU |ringMdd| = %d\n", mdd_size(ringMdd));
1782      }
1783    }
1784
1785    mdd_free(resultMdd);
1786    resultMdd = cMdd;
1787    /* add onion ring unless fixpoint reached */
1788    if (!term_fixpoint && onionRings != NIL(array_t)) {
1789      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
1790    }
1791  } /* while(!termination) for LFP */
1792
1793  mdd_free(ringMdd);
1794
1795  /* Print some debug info */
1796  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
1797    static int refCount=0;
1798    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
1799    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
1800
1801    if (verbosity == McVerbosityMax_c) {
1802      mdd_t *tmpMdd = careStatesArray ?
1803                      mdd_and_array(resultMdd, careStatesArray, 1, 1) :
1804                      mdd_dup(resultMdd);
1805      fprintf(vis_stdout, "--EU called %d (bdd_size - %d)\n", ++refCount,
1806              mdd_size(resultMdd));
1807      fprintf(vis_stdout,
1808              "--There are %.0f care states satisfying EU formula\n",
1809              mdd_count_onset(mddMgr, tmpMdd, psVars));
1810#ifdef DEBUG_MC
1811      /* The following 2 lines are just for debug */
1812      fprintf(vis_stdout, "EU satisfying minterms :\n");
1813      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
1814#endif
1815      mdd_free(tmpMdd);
1816    } else {
1817      fprintf(vis_stdout,
1818              "--There are %.0f states satisfying EU formula\n",
1819              mdd_count_onset(mddMgr, resultMdd, psVars));
1820    }
1821
1822    fprintf(vis_stdout, "--EU: %d preimage computations\n",
1823      Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
1824  }
1825
1826  if(fixpoint != NIL(boolean))
1827    *fixpoint = term_fixpoint || term_tautology;
1828  return resultMdd;
1829
1830} /* McEvaluateEUFormulaWithGivenTR */
1831
1832
1833/**Function********************************************************************
1834
1835  Synopsis    [Evaluate states satisfying E(invariant S target), given
1836  a transition relation]
1837
1838  Description [Does the same as Mc_FsmEvaluateESFormula, minus the hints.]
1839
1840  SeeAlso [Mc_FsmEvaluateESFormula]
1841 
1842  SideEffects []
1843
1844******************************************************************************/
1845mdd_t *
1846McEvaluateESFormulaWithGivenTR(
1847  Fsm_Fsm_t *modelFsm,
1848  mdd_t *invariantMdd,
1849  mdd_t *sourceMdd,
1850  mdd_t *underapprox,
1851  mdd_t *fairStates,
1852  array_t *careStatesArray,
1853  Mc_EarlyTermination_t *earlyTermination,
1854  array_t *onionRings,
1855  Mc_VerbosityLevel verbosity,
1856  Mc_DcLevel dcLevel,
1857  boolean *fixpoint
1858  )
1859{
1860  mdd_t *aMdd;
1861  mdd_t *bMdd;
1862  mdd_t *cMdd;
1863  mdd_t *resultMdd;
1864  mdd_t *ringMdd;
1865  int nImgComps;
1866  boolean term_tautology = FALSE; /* different termination conditions */
1867  boolean term_early     = FALSE; 
1868  boolean term_fixpoint  = FALSE; 
1869
1870  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
1871  resultMdd = mdd_and(sourceMdd, fairStates, 1, 1);
1872
1873  if(underapprox != NIL(mdd_t)){
1874    mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
1875    mdd_free(resultMdd);
1876    resultMdd = tmp;
1877  }
1878
1879  ringMdd = mdd_dup(resultMdd);
1880
1881  if (onionRings) {
1882    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
1883  }
1884 
1885  /* if Since is trivially satisfied, or
1886     the early termination condition holds*/ 
1887  {
1888    bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
1889    boolean trivial;
1890
1891    trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
1892                                            1, 1, careStatesArray);
1893    /* the lequal also takes care of the case where result = 1 */
1894    if(trivial ||
1895       McCheckEarlyTerminationForUnderapprox(earlyTermination,
1896                                             resultMdd,
1897                                             careStatesArray)){
1898      bdd_free(fairInvariantStates);
1899      bdd_free(ringMdd);
1900
1901      /* trivially satisfied means that the fixpoint is complete.  If this
1902         information is requested, give it. */
1903      if(fixpoint != NIL(boolean))
1904        *fixpoint = trivial;
1905      return(resultMdd);
1906    }
1907    bdd_free(fairInvariantStates);
1908  }
1909
1910  /* The LFP loop */
1911  while (!term_fixpoint && !term_tautology && !term_early) {
1912    /* If dclevel is maximal, ringbdd is between the frontier and the
1913       reached set */
1914    aMdd = Mc_FsmEvaluateEYFormula(modelFsm, ringMdd, fairStates,
1915                                   careStatesArray, verbosity, dcLevel);
1916    mdd_free(ringMdd);
1917
1918    bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
1919    mdd_free(aMdd);
1920
1921    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
1922    mdd_free(bMdd);
1923
1924    /* Can we stop?  The tautology condition can be weakened to
1925       cMdd <= careStatesArray */
1926    term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
1927                                                 careStatesArray);
1928    if(!term_fixpoint)
1929      term_tautology = mdd_is_tautology(cMdd, 1);
1930    if(!term_fixpoint && !term_tautology)
1931      term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, 
1932                                                         cMdd,
1933                                                         careStatesArray);
1934
1935    /* Print some debug info, and set ringmdd */
1936    if (dcLevel >= McDcLevelRchFrontier_c) {
1937      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
1938      ringMdd = bdd_between(tmpMdd, cMdd);
1939      if (verbosity == McVerbosityMax_c) {
1940        fprintf(vis_stdout,
1941                "--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
1942                mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
1943      }
1944      mdd_free(tmpMdd);
1945      }
1946    else {
1947      ringMdd = mdd_dup(cMdd);
1948      if (verbosity == McVerbosityMax_c) {
1949          fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd));
1950      }
1951    }
1952
1953    mdd_free(resultMdd);
1954    resultMdd = cMdd;
1955    /* add onion ring unless fixpoint reached */
1956    if (!term_fixpoint && onionRings != NIL(array_t)) {
1957      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
1958    }
1959  } /* while(!termination) for LFP */
1960
1961  mdd_free(ringMdd);
1962
1963  /* Print some debug info */
1964  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
1965    static int refCount=0;
1966    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
1967    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
1968
1969    if (verbosity == McVerbosityMax_c) {
1970      mdd_t *tmpMdd = careStatesArray ?
1971                      mdd_and_array(resultMdd, careStatesArray, 1, 1) :
1972                      mdd_dup(resultMdd);
1973      fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount,
1974              mdd_size(resultMdd));
1975      fprintf(vis_stdout,
1976              "--There are %.0f care states satisfying ES formula\n",
1977              mdd_count_onset(mddMgr, tmpMdd, psVars));
1978#ifdef DEBUG_MC
1979      /* The following 2 lines are just for debug */
1980      fprintf(vis_stdout, "ES satisfying minterms :\n");
1981      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
1982#endif
1983      mdd_free(tmpMdd);
1984    } else {
1985      fprintf(vis_stdout,
1986              "--There are %.0f states satisfying ES formula\n",
1987              mdd_count_onset(mddMgr, resultMdd, psVars));
1988    }
1989
1990    fprintf(vis_stdout, "--ES: %d image computations\n",
1991      Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
1992  }
1993
1994  if(fixpoint != NIL(boolean))
1995    *fixpoint = term_fixpoint || term_tautology;
1996  return resultMdd;
1997
1998} /* McEvaluateESFormulaWithGivenTR */
1999
2000
2001/**Function********************************************************************
2002
2003  Synopsis    []
2004
2005  Description []
2006
2007  SeeAlso []
2008 
2009  SideEffects []
2010
2011******************************************************************************/
2012mdd_t *
2013McEvaluateESFormulaWithGivenTRWithTarget(
2014  Fsm_Fsm_t *modelFsm,
2015  mdd_t *invariantMdd,
2016  mdd_t *sourceMdd,
2017  mdd_t *targetMdd,
2018  mdd_t *underapprox,
2019  mdd_t *fairStates,
2020  array_t *careStatesArray,
2021  Mc_EarlyTermination_t *earlyTermination,
2022  array_t *onionRings,
2023  Mc_VerbosityLevel verbosity,
2024  Mc_DcLevel dcLevel,
2025  boolean *fixpoint
2026  )
2027{
2028  mdd_t *aMdd;
2029  mdd_t *bMdd;
2030  mdd_t *cMdd;
2031  mdd_t *resultMdd;
2032  mdd_t *ringMdd;
2033  mdd_t *zeroMdd;
2034  int nImgComps;
2035  boolean term_tautology = FALSE; /* different termination conditions */
2036  boolean term_early     = FALSE; 
2037  boolean term_fixpoint  = FALSE; 
2038
2039  mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
2040
2041  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
2042  resultMdd = mdd_and(sourceMdd, fairStates, 1, 1);
2043
2044  if(underapprox != NIL(mdd_t)){
2045    mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
2046    mdd_free(resultMdd);
2047    resultMdd = tmp;
2048  }
2049
2050  ringMdd = mdd_dup(resultMdd);
2051  zeroMdd = mdd_zero(mddMgr);
2052
2053  if (onionRings) {
2054    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
2055  }
2056 
2057  /* if Since is trivially satisfied, or
2058     the early termination condition holds*/ 
2059  {
2060    bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
2061    boolean trivial;
2062
2063    trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
2064                                            1, 1, careStatesArray);
2065    /* the lequal also takes care of the case where result = 1 */
2066    if(trivial ||
2067       McCheckEarlyTerminationForUnderapprox(earlyTermination,
2068                                             resultMdd,
2069                                             careStatesArray)){
2070      bdd_free(fairInvariantStates);
2071      bdd_free(ringMdd);
2072
2073      /* trivially satisfied means that the fixpoint is complete.  If this
2074         information is requested, give it. */
2075      if(fixpoint != NIL(boolean))
2076        *fixpoint = trivial;
2077      return(resultMdd);
2078    }
2079    bdd_free(fairInvariantStates);
2080  }
2081
2082  /* The LFP loop */
2083  while (!term_fixpoint && !term_tautology && !term_early) {
2084    /* If dclevel is maximal, ringbdd is between the frontier and the
2085       reached set */
2086    aMdd = Mc_FsmEvaluateEYFormula(modelFsm, ringMdd, fairStates,
2087                                   careStatesArray, verbosity, dcLevel);
2088    mdd_free(ringMdd);
2089
2090    bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
2091    mdd_free(aMdd);
2092
2093    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
2094    mdd_free(bMdd);
2095
2096    /* Can we stop?  The tautology condition can be weakened to
2097       cMdd <= careStatesArray */
2098    term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
2099                                                 careStatesArray);
2100    if(!term_fixpoint)
2101      term_tautology = mdd_is_tautology(cMdd, 1);
2102    if(!term_fixpoint && !term_tautology)
2103      term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, 
2104                                                         cMdd,
2105                                                         careStatesArray);
2106
2107    /* Print some debug info, and set ringmdd */
2108    if (dcLevel >= McDcLevelRchFrontier_c) {
2109      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
2110      ringMdd = bdd_between(tmpMdd, cMdd);
2111      if (verbosity == McVerbosityMax_c) {
2112        fprintf(vis_stdout,
2113                "--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
2114                mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
2115      }
2116      mdd_free(tmpMdd);
2117      }
2118    else {
2119      ringMdd = mdd_dup(cMdd);
2120      if (verbosity == McVerbosityMax_c) {
2121          fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd));
2122      }
2123    }
2124
2125    mdd_free(resultMdd);
2126    resultMdd = cMdd;
2127
2128    aMdd = mdd_and(resultMdd, targetMdd, 1, 1);
2129    if(!mdd_equal(aMdd, zeroMdd)) {
2130      array_insert_last(mdd_t *, onionRings, mdd_dup(targetMdd));
2131      mdd_free(aMdd);
2132      break;
2133    }
2134    mdd_free(aMdd);
2135
2136    /* add onion ring unless fixpoint reached */
2137    if (!term_fixpoint && onionRings != NIL(array_t)) {
2138      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
2139    }
2140  } /* while(!termination) for LFP */
2141
2142  mdd_free(ringMdd);
2143
2144  /* Print some debug info */
2145  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
2146    static int refCount=0;
2147    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
2148
2149    if (verbosity == McVerbosityMax_c) {
2150      mdd_t *tmpMdd = careStatesArray ?
2151                      mdd_and_array(resultMdd, careStatesArray, 1, 1) :
2152                      mdd_dup(resultMdd);
2153      fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount,
2154              mdd_size(resultMdd));
2155      fprintf(vis_stdout,
2156              "--There are %.0f care states satisfying ES formula\n",
2157              mdd_count_onset(mddMgr, tmpMdd, psVars));
2158#ifdef DEBUG_MC
2159      /* The following 2 lines are just for debug */
2160      fprintf(vis_stdout, "ES satisfying minterms :\n");
2161      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
2162#endif
2163      mdd_free(tmpMdd);
2164    } else {
2165      fprintf(vis_stdout,
2166              "--There are %.0f states satisfying ES formula\n",
2167              mdd_count_onset(mddMgr, resultMdd, psVars));
2168    }
2169
2170    fprintf(vis_stdout, "--ES: %d image computations\n",
2171      Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
2172  }
2173  mdd_free(zeroMdd);
2174
2175  if(fixpoint != NIL(boolean))
2176    *fixpoint = term_fixpoint || term_tautology;
2177  return resultMdd;
2178
2179} /* McEvaluateESFormulaWithGivenTR */
2180
2181
2182/**Function********************************************************************
2183
2184  Synopsis    []
2185
2186  Description []
2187
2188  SeeAlso []
2189 
2190  SideEffects []
2191
2192******************************************************************************/
2193mdd_t *
2194McEvaluateESFormulaWithGivenTRFAFW(
2195  Fsm_Fsm_t *modelFsm,
2196  mdd_t *invariantMdd,
2197  mdd_t *sourceMdd,
2198  mdd_t *underapprox,
2199  mdd_t *fairStates,
2200  array_t *careStatesArray,
2201  Mc_EarlyTermination_t *earlyTermination,
2202  array_t *onionRings,
2203  Mc_VerbosityLevel verbosity,
2204  Mc_DcLevel dcLevel,
2205  boolean *fixpoint,
2206  mdd_t *Swin
2207  )
2208{
2209  mdd_t *aMdd;
2210  mdd_t *bMdd;
2211  mdd_t *cMdd;
2212  mdd_t *resultMdd;
2213  mdd_t *ringMdd;
2214  Img_ImageInfo_t *imageInfo;
2215  int nImgComps;
2216  boolean term_tautology = FALSE; /* different termination conditions */
2217  boolean term_early     = FALSE; 
2218  boolean term_fixpoint  = FALSE; 
2219
2220  nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
2221  resultMdd = mdd_and(sourceMdd, fairStates, 1, 1);
2222
2223  if(underapprox != NIL(mdd_t)){
2224    mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1);
2225    mdd_free(resultMdd);
2226    resultMdd = tmp;
2227  }
2228
2229  ringMdd = mdd_dup(resultMdd);
2230
2231  if (onionRings) {
2232    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
2233  }
2234 
2235  /* if Since is trivially satisfied, or
2236     the early termination condition holds*/ 
2237  {
2238    bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1);
2239    boolean trivial;
2240
2241    trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd,
2242                                            1, 1, careStatesArray);
2243    /* the lequal also takes care of the case where result = 1 */
2244    if(trivial ||
2245       McCheckEarlyTerminationForUnderapprox(earlyTermination,
2246                                             resultMdd,
2247                                             careStatesArray)){
2248      bdd_free(fairInvariantStates);
2249      bdd_free(ringMdd);
2250
2251      /* trivially satisfied means that the fixpoint is complete.  If this
2252         information is requested, give it. */
2253      if(fixpoint != NIL(boolean))
2254        *fixpoint = trivial;
2255      return(resultMdd);
2256    }
2257    bdd_free(fairInvariantStates);
2258  }
2259
2260  imageInfo = Fsm_FsmReadOrCreateImageInfoPrunedFAFW(modelFsm, Swin, 0, 1);
2261  /* The LFP loop */
2262  while (!term_fixpoint && !term_tautology && !term_early) {
2263    /* If dclevel is maximal, ringbdd is between the frontier and the
2264       reached set */
2265    aMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
2266                ringMdd, ringMdd, careStatesArray);
2267    mdd_free(ringMdd);
2268
2269    bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
2270    mdd_free(aMdd);
2271
2272    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
2273    mdd_free(bMdd);
2274
2275    /* Can we stop?  The tautology condition can be weakened to
2276       cMdd <= careStatesArray */
2277    term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
2278                                                 careStatesArray);
2279    if(!term_fixpoint)
2280      term_tautology = mdd_is_tautology(cMdd, 1);
2281    if(!term_fixpoint && !term_tautology)
2282      term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, 
2283                                                         cMdd,
2284                                                         careStatesArray);
2285
2286    /* Print some debug info, and set ringmdd */
2287    if (dcLevel >= McDcLevelRchFrontier_c) {
2288      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
2289      ringMdd = bdd_between(tmpMdd, cMdd);
2290      if (verbosity == McVerbosityMax_c) {
2291        fprintf(vis_stdout,
2292                "--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
2293                mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
2294      }
2295      mdd_free(tmpMdd);
2296      }
2297    else {
2298      ringMdd = mdd_dup(cMdd);
2299      if (verbosity == McVerbosityMax_c) {
2300          fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd));
2301      }
2302    }
2303
2304    mdd_free(resultMdd);
2305    resultMdd = cMdd;
2306    /* add onion ring unless fixpoint reached */
2307    if (!term_fixpoint && onionRings != NIL(array_t)) {
2308      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
2309    }
2310  } /* while(!termination) for LFP */
2311
2312  /* Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c); */
2313  Img_ImageInfoFreeFAFW(imageInfo);
2314  Img_ImageInfoFree(imageInfo);
2315
2316  mdd_free(ringMdd);
2317
2318  /* Print some debug info */
2319  if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
2320    static int refCount=0;
2321    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
2322    array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
2323
2324    if (verbosity == McVerbosityMax_c) {
2325      mdd_t *tmpMdd = careStatesArray ?
2326                      mdd_and_array(resultMdd, careStatesArray, 1, 1) :
2327                      mdd_dup(resultMdd);
2328      fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount,
2329              mdd_size(resultMdd));
2330      fprintf(vis_stdout,
2331              "--There are %.0f care states satisfying ES formula\n",
2332              mdd_count_onset(mddMgr, tmpMdd, psVars));
2333#ifdef DEBUG_MC
2334      /* The following 2 lines are just for debug */
2335      fprintf(vis_stdout, "ES satisfying minterms :\n");
2336      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
2337#endif
2338      mdd_free(tmpMdd);
2339    } else {
2340      fprintf(vis_stdout,
2341              "--There are %.0f states satisfying ES formula\n",
2342              mdd_count_onset(mddMgr, resultMdd, psVars));
2343    }
2344
2345    fprintf(vis_stdout, "--ES: %d image computations\n",
2346      Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
2347  }
2348
2349  if(fixpoint != NIL(boolean))
2350    *fixpoint = term_fixpoint || term_tautology;
2351  return resultMdd;
2352
2353} /* McEvaluateESFormulaWithGivenTR */
2354
2355
2356/**Function********************************************************************
2357
2358  Synopsis    []
2359
2360  Description []
2361
2362  SeeAlso []
2363 
2364  SideEffects []
2365
2366******************************************************************************/
2367mdd_t *
2368McEvaluateAUFormulaWithGivenTR(
2369  Fsm_Fsm_t *modelFsm,
2370  mdd_t *invariantMdd,
2371  mdd_t *targetMdd,
2372  mdd_t *underapprox,
2373  mdd_t *fairStates,
2374  array_t *careStatesArray,
2375  Mc_EarlyTermination_t *earlyTermination,
2376  array_t *onionRings,
2377  Mc_VerbosityLevel verbosity,
2378  Mc_DcLevel dcLevel,
2379  boolean *fixpoint
2380  )
2381{
2382  mdd_t *aMdd;
2383  mdd_t *bMdd;
2384  mdd_t *cMdd;
2385  mdd_t *resultMdd;
2386  mdd_t *ringMdd;
2387  boolean term_tautology = FALSE; /* different termination conditions */
2388  boolean term_early     = FALSE;
2389  boolean term_fixpoint  = FALSE;
2390
2391  resultMdd = mdd_and(targetMdd, fairStates, 1, 1);
2392
2393  ringMdd = mdd_dup(resultMdd);
2394  if (onionRings) {
2395    array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
2396  }
2397  /* The LFP loop */
2398  while (!term_fixpoint && !term_tautology && !term_early) {
2399    /* If dclevel is maximal, ringbdd is between the frontier and the
2400     reached set */
2401    aMdd = Mc_FsmEvaluateMXFormula(modelFsm, ringMdd, fairStates, 
2402                                    careStatesArray, verbosity, dcLevel);
2403
2404    bMdd = mdd_and(aMdd, invariantMdd, 1, 1);
2405    mdd_free(aMdd);
2406
2407    cMdd = mdd_or(resultMdd, bMdd, 1, 1);
2408    mdd_free(bMdd);
2409    mdd_free(ringMdd);
2410
2411    /* Can we stop?  The tautology condition can be weakened to
2412       cMdd <= careStatesArray */
2413    term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd,
2414                                                 careStatesArray);
2415    if(!term_fixpoint)
2416      term_tautology = mdd_is_tautology(cMdd, 1);
2417    if(!term_fixpoint && !term_tautology)
2418      term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination,
2419                                                         cMdd,
2420                                                         careStatesArray);
2421
2422    /* Print some debug info, and set ringmdd */
2423    if (dcLevel >= McDcLevelRchFrontier_c) {
2424      mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1);
2425      ringMdd = bdd_between(tmpMdd, cMdd);
2426      if (verbosity == McVerbosityMax_c) {
2427        fprintf(vis_stdout,
2428                "--AU |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n",
2429                mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd));
2430      }
2431      mdd_free(tmpMdd);
2432      }
2433    else {
2434      ringMdd = mdd_dup(cMdd);
2435      if (verbosity == McVerbosityMax_c) {
2436          fprintf(vis_stdout, "-- AU |ringMdd| = %d\n", mdd_size(ringMdd));
2437      }
2438    }
2439
2440    mdd_free(resultMdd);
2441    resultMdd = cMdd;
2442    /* add onion ring unless fixpoint reached */
2443    if (!term_fixpoint && onionRings) {
2444      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
2445    }
2446  } /* while(!termination) for LFP */
2447
2448  mdd_free(ringMdd);
2449
2450
2451  if(fixpoint != NIL(boolean))
2452    *fixpoint = term_fixpoint || term_tautology;
2453  return resultMdd; 
2454}
2455
2456
2457/**Function********************************************************************
2458
2459  Synopsis    [Evaluate states satisfying EG(invariantMdd), given
2460  a transition relation]
2461
2462  Description [Does the same as Mc_FsmEvaluateEGFormula, minus the hints.]
2463
2464  SeeAlso [Mc_FsmEvaluateEGFormula]
2465 
2466  SideEffects []
2467
2468******************************************************************************/
2469mdd_t *
2470McEvaluateEGFormulaWithGivenTR(
2471  Fsm_Fsm_t *modelFsm,
2472  mdd_t *invariantMdd,
2473  mdd_t *overapprox,
2474  mdd_t *fairStates,
2475  Fsm_Fairness_t *modelFairness,
2476  array_t *careStatesArray,
2477  Mc_EarlyTermination_t *earlyTermination,
2478  array_t **pOnionRingsArrayForDbg,
2479  Mc_VerbosityLevel verbosity,
2480  Mc_DcLevel dcLevel,
2481  boolean *fixpoint)
2482{
2483  int i;
2484  array_t *onionRings;
2485  boolean useRings;
2486  mdd_manager *mddManager;
2487  mdd_t *mddOne;
2488  mdd_t *iterate;
2489  array_t *buchiFairness;
2490  int nPreComps;
2491  int nIterations;
2492  boolean term_fixpoint = FALSE;        /* different termination conditions */
2493  boolean term_tautology = FALSE;
2494  boolean term_early = FALSE;
2495
2496  /* Here's how the onionRingsArrayForDbg works.  It is an array of
2497     arrays of mdds.  It is filled in anew for every pass of the
2498     algorithm, that is for every /\_{c inC} EXE(Y U Y*c).  There is
2499     one entry for every fairness constraint, and this entry contains
2500     the onionrings of the EU computation that corresponds to this
2501     constraint. */
2502  assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
2503         *pOnionRingsArrayForDbg == NIL(array_t) ||
2504         array_n(*pOnionRingsArrayForDbg) == 0); 
2505
2506  useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
2507              *pOnionRingsArrayForDbg != NIL(array_t));
2508
2509  nIterations = 0;
2510  nPreComps  = Img_GetNumberOfImageComputation(Img_Backward_c);
2511  onionRings = NIL(array_t);
2512  mddManager = Fsm_FsmReadMddManager(modelFsm);
2513  mddOne  = mdd_one(mddManager);
2514
2515  /* If an overapproximation of the greatest fixpoint is given, use it. */
2516  if(overapprox != NIL(mdd_t)){
2517    iterate = mdd_and(invariantMdd, overapprox, 1, 1);
2518  } else {
2519    iterate = mdd_dup(invariantMdd);
2520  }
2521
2522  /* See if we need to enter the loop at all.  If we wanted to test for
2523   * early termination here, we should fix the onion rings.  In the current
2524   * case, we do not need to, since the EG does not hold, and hence a
2525   * counterexample does not exist.
2526   */
2527  if( mdd_is_tautology(iterate, 0)){
2528    mdd_free(mddOne);
2529    if(fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0);
2530    return(iterate);
2531  }
2532
2533  /* read fairness constraints */
2534  buchiFairness = array_alloc(mdd_t *, 0);
2535  if(modelFairness != NIL(Fsm_Fairness_t)) {
2536    if(!Fsm_FairnessTestIsBuchi(modelFairness)) {
2537      (void)fprintf(vis_stdout,
2538               "** mc error: non-Buechi fairness constraints not supported\n");
2539      array_free(buchiFairness);
2540      mdd_free(iterate);
2541      mdd_free(mddOne);
2542
2543      if(fixpoint != NIL(boolean)) *fixpoint = FALSE;
2544      return NIL(mdd_t);
2545    }
2546    else {
2547      int j;
2548      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
2549      for (j = 0 ; j < numBuchi; j++) {
2550        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
2551                                                careStatesArray, dcLevel);
2552        array_insert_last(mdd_t *, buchiFairness, tmpMdd);
2553      }
2554    }
2555  }
2556  else {
2557    array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager));
2558  }
2559
2560
2561  /* GFP.  If we know that the result is a subset of a set S, we can conjoin
2562   the iterate with that set.  We use this to converge faster.  */
2563  while (TRUE) {
2564    mdd_t *newIterate;           /* the new iterate */
2565
2566    nIterations++;
2567    newIterate = mdd_dup(iterate);
2568   
2569    /* for all fairness constraints */
2570    for (i = 0 ; i < array_n(buchiFairness) ; i++) {
2571      mdd_t *aMdd, *bMdd, *cMdd, *dMdd;
2572      mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i);
2573     
2574      if(useRings) {
2575        onionRings = array_alloc(mdd_t *, 0);
2576        array_insert_last(array_t *, *pOnionRingsArrayForDbg, onionRings);
2577      }
2578
2579      aMdd = mdd_and(FiMdd, newIterate, 1, 1);
2580
2581      bMdd = Mc_FsmEvaluateEUFormula(modelFsm, newIterate, aMdd, NIL(mdd_t),
2582                                     mddOne, careStatesArray,
2583                                     MC_NO_EARLY_TERMINATION, NIL(array_t),
2584                                     Mc_None_c, onionRings, verbosity, dcLevel,
2585                                     NIL(boolean)); 
2586      mdd_free(aMdd);
2587      cMdd = Mc_FsmEvaluateEXFormula(modelFsm, bMdd, mddOne, careStatesArray,
2588                                     verbosity, dcLevel);
2589      mdd_free(bMdd);
2590
2591      dMdd  = mdd_and(newIterate, cMdd, 1, 1);
2592
2593      mdd_free(cMdd);
2594      mdd_free(newIterate);
2595      newIterate = dMdd;
2596
2597      /* invariants that hold here: newiterate <= iterate <= invariant. */
2598    }/* for all fairness constraints */
2599
2600    /* termination */
2601    term_tautology = mdd_is_tautology(newIterate, 0);
2602    if(!term_tautology)
2603      term_fixpoint =  mdd_equal_mod_care_set_array(newIterate, iterate,
2604                                                    careStatesArray);
2605    if(!term_tautology && !term_fixpoint)
2606      term_early = McCheckEarlyTerminationForOverapprox(earlyTermination,
2607                                                        newIterate, 
2608                                                        careStatesArray);
2609    if(term_tautology || term_fixpoint || term_early){
2610      mdd_free(iterate);
2611      iterate = newIterate;
2612      break; /* from the GFP loop */
2613    }
2614
2615    /* update iterate */
2616    mdd_free(iterate);
2617    iterate = newIterate;
2618
2619    if(useRings){
2620      mdd_array_array_free(*pOnionRingsArrayForDbg);
2621      *pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
2622    }
2623  } /* while(true) for gfp */
2624
2625  /* Check if onionrings are OK */
2626  if(verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
2627    if(useRings){
2628      for (i = 0 ; i < array_n(*pOnionRingsArrayForDbg); i++) {
2629        int j;
2630        mdd_t *Fi = array_fetch(mdd_t *,  buchiFairness, i);
2631        array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
2632                                          i); 
2633        for (j = 0 ; j < array_n(onionRings); j++) {
2634          mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
2635          if(j == 0) {
2636            if(!mdd_lequal_mod_care_set_array(ring, Fi, 1, 1,
2637                                               careStatesArray)) {
2638              fprintf(vis_stderr, "** mc error: Problem w/ dbg in EG - ");
2639              fprintf(vis_stderr,
2640                      "inner most ring not in Fi (fairness constraint).\n");
2641            }
2642          }
2643          if(!mdd_lequal_mod_care_set_array(ring, invariantMdd, 1, 1,
2644                                             careStatesArray)) {
2645            fprintf(vis_stderr, "** mc error: Problem w/ dbg in EG - ");
2646            fprintf(vis_stderr, "An onion ring of last EU fails invariant\n");
2647          }
2648        } /* for all onionrings in array i */ 
2649      } /* for all onionringarrays in onionringsarray */
2650    }/* if useRings */
2651
2652    if(verbosity == McVerbosityMax_c) {
2653      mdd_t *tmpMdd = careStatesArray ?
2654        mdd_and_array(iterate, careStatesArray, 1, 1) : mdd_dup(iterate);
2655      fprintf(vis_stdout,
2656              "--There are %.0f care states satisfying EG formula\n",
2657              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd,
2658                                Fsm_FsmReadPresentStateVars(modelFsm)));
2659#ifdef DEBUG_MC
2660      /* The following 2 lines are just for debug */
2661      fprintf(vis_stdout, "EG satisfying minterms :\n");
2662      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
2663#endif
2664      mdd_free(tmpMdd);
2665    } else {
2666      fprintf(vis_stdout, "--There are %.0f states satisfying EG formula\n",
2667              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), iterate,
2668                                Fsm_FsmReadPresentStateVars(modelFsm)));
2669    }
2670
2671    fprintf(vis_stdout, "--EG: %d iterations, %d preimage computations\n",
2672      nIterations, Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
2673  }
2674
2675  mdd_array_free(buchiFairness);
2676  mdd_free(mddOne);
2677
2678  if(fixpoint != NIL(boolean))
2679     *fixpoint = term_fixpoint || term_tautology;
2680  return iterate;
2681
2682} /* McEvaluateEGFormulaWithGivenTR */
2683
2684
2685/**Function********************************************************************
2686
2687  Synopsis    [Evaluate states satisfying EH(invariantMdd), given
2688  a transition relation]
2689
2690  Description [Does the same as Mc_FsmEvaluateEHFormula, minus the hints.]
2691
2692  SeeAlso     [Mc_FsmEvaluateEHFormula]
2693 
2694  SideEffects []
2695
2696******************************************************************************/
2697mdd_t *
2698McEvaluateEHFormulaWithGivenTR(
2699  Fsm_Fsm_t *modelFsm,
2700  mdd_t *invariantMdd,
2701  mdd_t *overapprox,
2702  mdd_t *fairStates,
2703  Fsm_Fairness_t *modelFairness,
2704  array_t *careStatesArray,
2705  Mc_EarlyTermination_t *earlyTermination,
2706  array_t **pOnionRingsArrayForDbg,
2707  Mc_VerbosityLevel verbosity,
2708  Mc_DcLevel dcLevel,
2709  boolean *fixpoint)
2710{
2711  int i;
2712  array_t *onionRings;
2713  boolean useRings;
2714  mdd_manager *mddManager;
2715  mdd_t *mddOne;
2716  mdd_t *iterate;
2717  array_t *buchiFairness;
2718  int nImgComps;
2719  int nIterations;
2720  boolean term_fixpoint = FALSE;        /* different termination conditions */
2721  boolean term_tautology = FALSE;
2722  boolean term_early = FALSE;
2723
2724  /* Here's how the onionRingsArrayForDbg works.  It is an array of
2725     arrays of mdds.  It is filled in anew for every pass of the
2726     algorithm, that is for every /\_{c inC} EYE(Y S Y*c).  There is
2727     one entry for every fairness constraint, and this entry contains
2728     the onionrings of the ES computation that corresponds to this
2729     constraint. */
2730  assert(pOnionRingsArrayForDbg == NIL(array_t *) ||
2731         *pOnionRingsArrayForDbg == NIL(array_t) ||
2732         array_n(*pOnionRingsArrayForDbg) == 0); 
2733
2734  useRings = (pOnionRingsArrayForDbg != NIL(array_t *) &&
2735              *pOnionRingsArrayForDbg != NIL(array_t));
2736
2737  nIterations = 0;
2738  nImgComps  = Img_GetNumberOfImageComputation(Img_Forward_c);
2739  onionRings = NIL(array_t);
2740  mddManager = Fsm_FsmReadMddManager(modelFsm);
2741  mddOne  = mdd_one(mddManager);
2742
2743  /* If an overapproxiamtion of the greatest fixpoint is given, use it. */
2744  if(overapprox != NIL(mdd_t)){
2745    iterate = mdd_and(invariantMdd, overapprox, 1, 1);
2746  } else {
2747    iterate = mdd_dup(invariantMdd);
2748  }
2749
2750  /* See if we need to enter the loop at all */
2751  if( mdd_is_tautology(iterate, 0) ||
2752      McCheckEarlyTerminationForOverapprox(earlyTermination,
2753                                           iterate,
2754                                           careStatesArray)){
2755    mdd_free(mddOne);
2756
2757    if(fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0);
2758    return(iterate);
2759  }
2760
2761  /* read fairness constraints */
2762  buchiFairness = array_alloc(mdd_t *, 0);
2763  if(modelFairness != NIL(Fsm_Fairness_t)) {
2764    if(!Fsm_FairnessTestIsBuchi(modelFairness)) {
2765      (void)fprintf(vis_stdout,
2766               "** mc error: non-Buechi fairness constraints not supported\n");
2767      array_free(buchiFairness);
2768      mdd_free(iterate);
2769      mdd_free(mddOne);
2770
2771      if(fixpoint != NIL(boolean)) *fixpoint = FALSE;
2772      return NIL(mdd_t);
2773    }
2774    else {
2775      int j;
2776      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
2777      for (j = 0 ; j < numBuchi; j++) {
2778        mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
2779                                                careStatesArray, dcLevel);
2780        array_insert_last(mdd_t *, buchiFairness, tmpMdd);
2781      }
2782    }
2783  }
2784  else {
2785    array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager));
2786  }
2787
2788
2789  /* GFP.  If we know that the result is a subset of a set S, we can conjoin
2790   the iterate with that set.  We use this to converge faster.  */
2791  while (TRUE) {
2792    mdd_t *newIterate;           /* the new iterate */
2793
2794    nIterations++;
2795    newIterate = mdd_dup(iterate);
2796   
2797    /* for all fairness constraints */
2798    for (i = 0 ; i < array_n(buchiFairness) ; i++) {
2799      mdd_t *aMdd, *bMdd, *cMdd, *dMdd;
2800      mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i);
2801     
2802      if(useRings) {
2803        onionRings = array_alloc(mdd_t *, 0);
2804        array_insert_last(array_t *, *pOnionRingsArrayForDbg, onionRings);
2805      }
2806
2807      aMdd = mdd_and(FiMdd, newIterate, 1, 1);
2808
2809      bMdd = Mc_FsmEvaluateESFormula(modelFsm, newIterate, aMdd, NIL(mdd_t),
2810                                     mddOne, careStatesArray,
2811                                     MC_NO_EARLY_TERMINATION, NIL(array_t),
2812                                     Mc_None_c, onionRings, verbosity, dcLevel,
2813                                     NIL(boolean)); 
2814      mdd_free(aMdd);
2815      cMdd = Mc_FsmEvaluateEYFormula(modelFsm, bMdd, mddOne, careStatesArray,
2816                                     verbosity, dcLevel);
2817      mdd_free(bMdd);
2818
2819      dMdd  = mdd_and(newIterate, cMdd, 1, 1);
2820
2821      mdd_free(cMdd);
2822      mdd_free(newIterate);
2823      newIterate = dMdd;
2824
2825      /* invariants that hold here: newiterate <= iterate <= invariant. */
2826    }/* for all fairness constraints */
2827
2828    /* termination */
2829    term_tautology = mdd_is_tautology(newIterate, 0);
2830    if(!term_tautology)
2831      term_fixpoint =  mdd_equal_mod_care_set_array(newIterate, iterate,
2832                                                    careStatesArray);
2833    if(!term_tautology && !term_fixpoint)
2834      term_early = McCheckEarlyTerminationForOverapprox(earlyTermination,
2835                                                        newIterate, 
2836                                                        careStatesArray);
2837    if(term_tautology || term_fixpoint || term_early){
2838      mdd_free(iterate);
2839      iterate = newIterate;
2840      break; /* from the GFP loop */
2841    }
2842
2843    /* update iterate */
2844    mdd_free(iterate);
2845    iterate = newIterate;
2846
2847    if(useRings){
2848      mdd_array_array_free(*pOnionRingsArrayForDbg);
2849      *pOnionRingsArrayForDbg = array_alloc(array_t *, 0);
2850    }
2851  } /* while(true) for gfp */
2852
2853  /* Check if onionrings are OK */
2854  if(verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) {
2855    if(useRings){
2856      for (i = 0 ; i < array_n(*pOnionRingsArrayForDbg); i++) {
2857        int j;
2858        mdd_t *Fi = array_fetch(mdd_t *,  buchiFairness, i);
2859        array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg,
2860                                          i); 
2861        for (j = 0 ; j < array_n(onionRings); j++) {
2862          mdd_t *ring = array_fetch(mdd_t *, onionRings, j);
2863          if(j == 0) {
2864            if(!mdd_lequal_mod_care_set_array(ring, Fi, 1, 1,
2865                                               careStatesArray)) {
2866              fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
2867              fprintf(vis_stderr,
2868                      "inner most ring not in Fi (fairness constraint).\n");
2869            }
2870          }
2871          if(!mdd_lequal_mod_care_set_array(ring, invariantMdd, 1, 1,
2872                                             careStatesArray)) {
2873            fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - ");
2874            fprintf(vis_stderr, "An onion ring of last ES fails invariant\n");
2875          }
2876        } /* for all onionrings in array i */ 
2877      } /* for all onionringarrays in onionringsarray */
2878    }/* if useRings */
2879
2880    if(verbosity == McVerbosityMax_c) {
2881      mdd_t *tmpMdd = careStatesArray ?
2882        mdd_and_array(iterate, careStatesArray, 1, 1) : mdd_dup(iterate);
2883      fprintf(vis_stdout,
2884              "--There are %.0f care states satisfying EH formula\n",
2885              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd,
2886                                Fsm_FsmReadPresentStateVars(modelFsm)));
2887#ifdef DEBUG_MC
2888      /* The following 2 lines are just for debug */
2889      fprintf(vis_stdout, "EH satisfying minterms :\n");
2890      (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm);
2891#endif
2892      mdd_free(tmpMdd);
2893    } else {
2894      fprintf(vis_stdout, "--There are %.0f states satisfying EH formula\n",
2895              mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), iterate,
2896                                Fsm_FsmReadPresentStateVars(modelFsm)));
2897    }
2898
2899    fprintf(vis_stdout, "--EH: %d iterations, %d image computations\n",
2900      nIterations, Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps);
2901  }
2902
2903  mdd_array_free(buchiFairness);
2904  mdd_free(mddOne);
2905
2906  if(fixpoint != NIL(boolean))
2907     *fixpoint = term_fixpoint || term_tautology;
2908  return iterate;
2909
2910} /* McEvaluateEHFormulaWithGivenTR */
2911
2912
2913/**Function********************************************************************
2914
2915  Synopsis    [Frees memory stored at formula corresponding to debug data.]
2916
2917  Description [Frees memory stored at formula corresponding to debug data.  It
2918  is assumed that the debug data is valid.  It is an error to call this
2919  function on a formula which is not of the type EG or EU.]
2920
2921  SideEffects []
2922
2923******************************************************************************/
2924void
2925McFormulaFreeDebugData(
2926  Ctlp_Formula_t *formula)
2927{
2928  Ctlp_FormulaType  type     = Ctlp_FormulaReadType(formula);
2929  array_t          *dbgArray = (array_t *) Ctlp_FormulaReadDebugData(formula);
2930
2931  if (type == Ctlp_EU_c || type == Ctlp_FwdU_c) {
2932    mdd_array_free(dbgArray);
2933  }
2934  else if (type == Ctlp_EG_c || type == Ctlp_FwdG_c || type == Ctlp_EH_c) 
2935    mdd_array_array_free(dbgArray);
2936  else {
2937    fail("Error - called on non EG/EU formula.\n");
2938  }
2939}
2940
2941
2942/**Function********************************************************************
2943
2944  Synopsis    [Print satisfying minterms.]
2945
2946  Description [Print satisfying minterms. Just made for debug.]
2947
2948  SideEffects []
2949
2950******************************************************************************/
2951void
2952_McPrintSatisfyingMinterms(mdd_t *aMdd, Fsm_Fsm_t *fsm)
2953{
2954  array_t *support = Fsm_FsmReadPresentStateVars(fsm);
2955  mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
2956  Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm);
2957  int i, n;
2958  array_t *mintermArray;
2959  mdd_t *aMinterm;
2960
2961  n = (int) mdd_count_onset(mddMgr, aMdd, support);
2962  mintermArray = mdd_pick_arbitrary_minterms(mddMgr, aMdd, support, n);
2963
2964  for (i = 0; i < n; i++) {
2965    aMinterm = array_fetch(mdd_t *, mintermArray, i);
2966    Mc_MintermPrint(aMinterm, support, network);
2967    mdd_free(aMinterm);
2968  }
2969
2970  array_free(mintermArray);
2971
2972}
2973
2974/**Function********************************************************************
2975
2976  Synopsis [Prints whether model checking passed or failed]
2977
2978  Description [Prints whether model checking passed or failed, and if
2979  requested, a debug trace.]
2980
2981  SideEffects []
2982
2983******************************************************************************/
2984boolean
2985McPrintPassFail(
2986  mdd_manager *mddMgr,
2987  Fsm_Fsm_t *modelFsm,
2988  Mc_FwdBwdAnalysis traversalDirection,
2989  Ctlp_Formula_t *ctlFormula,
2990  mdd_t *ctlFormulaStates,
2991  mdd_t *modelInitialStates,
2992  array_t *modelCareStatesArray,
2993  McOptions_t *options,
2994  Mc_VerbosityLevel verbosity)
2995{
2996  if (mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1)) {
2997    fprintf(vis_stdout, "# MC: formula passed --- ");
2998    Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula));
2999    fprintf(vis_stdout, "\n");
3000    return TRUE;
3001  }
3002  else {
3003    fprintf(vis_stdout, "# MC: formula failed --- ");
3004    Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula));
3005    fprintf(vis_stdout, "\n");
3006    if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) {
3007      McFsmDebugFormula(options, ctlFormula,modelFsm, modelCareStatesArray);
3008    }
3009    return FALSE;
3010  }
3011}
3012
3013
3014/**Function********************************************************************
3015
3016  Synopsis    [Find Mdd for states satisfying Atomic Formula.]
3017
3018  Description [An atomic formula defines a set of states in the following
3019  way: it states a designated ``net'' (specified by the full path name)
3020  takes a certain value. The net should be purely a function of latches;
3021  as a result an evaluation of the net yields a set of states.]
3022
3023  SideEffects []
3024
3025******************************************************************************/
3026mdd_t *
3027McModelCheckAtomicFormula(
3028  Fsm_Fsm_t *modelFsm,
3029  Ctlp_Formula_t *ctlFormula)
3030{
3031  mdd_t * resultMdd;
3032  mdd_t *tmpMdd;
3033  Ntk_Network_t *network = Fsm_FsmReadNetwork(modelFsm);
3034  char *nodeNameString = Ctlp_FormulaReadVariableName(ctlFormula);
3035  char *nodeValueString = Ctlp_FormulaReadValueName(ctlFormula);
3036  Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
3037
3038  Var_Variable_t *nodeVar;
3039  int nodeValue;
3040
3041  graph_t *modelPartition;
3042  vertex_t *partitionVertex;
3043  Mvf_Function_t *MVF;
3044
3045  nodeVar = Ntk_NodeReadVariable(node);
3046  if (Var_VariableTestIsSymbolic(nodeVar)) {
3047    nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
3048  }
3049  else {
3050    nodeValue = atoi(nodeValueString);
3051  }
3052
3053#if 0
3054  modelPartition = Part_NetworkReadPartition(network);
3055#endif
3056  modelPartition = Fsm_FsmReadPartition(modelFsm);
3057  if (!(partitionVertex = Part_PartitionFindVertexByName(modelPartition,
3058                                                         nodeNameString))) {
3059    lsGen tmpGen;
3060    Ntk_Node_t *tmpNode;
3061    array_t *mvfArray;
3062    array_t *tmpRoots = array_alloc(Ntk_Node_t *, 0);
3063    st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
3064    array_insert_last(Ntk_Node_t *, tmpRoots, node);
3065
3066    Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
3067      st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED);
3068    }
3069
3070    mvfArray =  Ntm_NetworkBuildMvfs(network, tmpRoots, tmpLeaves,
3071                                      NIL(mdd_t));
3072    MVF = array_fetch(Mvf_Function_t *, mvfArray, 0);
3073    array_free(tmpRoots);
3074    st_free_table(tmpLeaves);
3075    array_free(mvfArray);
3076
3077    tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
3078    resultMdd = mdd_dup(tmpMdd);
3079    Mvf_FunctionFree(MVF);
3080  }
3081  else {
3082    MVF = Part_VertexReadFunction(partitionVertex);
3083    tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
3084    resultMdd = mdd_dup(tmpMdd);
3085  }
3086  if (Part_PartitionReadMethod(modelPartition) == Part_Frontier_c &&
3087      Ntk_NodeTestIsCombOutput(node)) {
3088    array_t     *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
3089    mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
3090    array_t     *supportList;
3091    st_table    *supportTable = st_init_table(st_numcmp, st_numhash);
3092    int         i, j;
3093    int         existIntermediateVars;
3094    int         mddId;
3095    Mvf_Function_t      *mvf;
3096    vertex_t    *vertex;
3097    array_t     *varBddRelationArray, *varArray;
3098    mdd_t       *iv, *ivMdd, *relation;
3099
3100    for (i = 0; i < array_n(psVars); i++) {
3101      mddId = array_fetch(int, psVars, i);
3102      st_insert(supportTable, (char *)(long)mddId, NULL);
3103    }
3104
3105    existIntermediateVars = 1;
3106    while (existIntermediateVars) {
3107      existIntermediateVars = 0;
3108      supportList = mdd_get_support(mgr, resultMdd);
3109      for (i = 0; i < array_n(supportList); i++) {
3110        mddId = array_fetch(int, supportList, i);
3111        if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) {
3112          vertex = Part_PartitionFindVertexByMddId(modelPartition, mddId);
3113          mvf = Part_VertexReadFunction(vertex);
3114          varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mgr, mddId, mvf);
3115          varArray = mdd_id_to_bdd_array(mgr, mddId);
3116          assert(array_n(varBddRelationArray) == array_n(varArray));
3117          for (j = 0; j < array_n(varBddRelationArray); j++) {
3118            iv = array_fetch(mdd_t *, varArray, j);
3119            relation = array_fetch(mdd_t *, varBddRelationArray, j);
3120            ivMdd = bdd_cofactor(relation, iv);
3121            mdd_free(relation);
3122            tmpMdd = resultMdd;
3123            resultMdd = bdd_compose(resultMdd, iv, ivMdd);
3124            mdd_free(tmpMdd);
3125            mdd_free(iv);
3126            mdd_free(ivMdd);
3127          }
3128          array_free(varBddRelationArray);
3129          array_free(varArray);
3130          existIntermediateVars = 1;
3131        }
3132      }
3133      array_free(supportList);
3134    }
3135    st_free_table(supportTable);
3136  }
3137  return resultMdd;
3138} /* McModelCheckAtomicFormula */
3139
3140
3141/**Function********************************************************************
3142
3143  Synopsis [Prints out a path from the initial state to a state that
3144  violates the invariant. ]
3145
3146  Description [Prints out a path from the initial state to a state
3147  that violates the invariant. First it checks whether there any onion
3148  rings built for this fsm. If the onion rings already exist, it
3149  checks whether there is any violation in these rings. If not,
3150  additional onion rings are computed.]
3151
3152  SideEffects []
3153
3154******************************************************************************/
3155void
3156InvarPrintDebugInformation(Fsm_Fsm_t *modelFsm,
3157                           array_t *invarFormulaArray,
3158                           array_t *invarStatesArray,
3159                           int *resultArray,
3160                           McOptions_t *options,
3161                           array_t *hintsStatesArray)
3162{
3163  FILE *debugFile = McOptionsReadDebugFile(options);
3164  FILE *tmpFile = vis_stdout;
3165  extern FILE *vis_stdpipe;
3166  mdd_t *outerOnionRing=NIL(mdd_t);
3167  mdd_t *reachableBadStates;
3168  mdd_t *aBadReachableState, *reachableStates;
3169  array_t *aPath;
3170  boolean computeReach = TRUE;
3171  int ringsUpToDate;
3172  array_t *onionRings=NIL(array_t);
3173  int i, j;
3174  Fsm_RchType_t approxFlag;
3175  Ctlp_Formula_t *invarFormula;
3176  mdd_t *invarFormulaStates;
3177  approxFlag = McOptionsReadInvarApproxFlag(options);
3178
3179  if (debugFile)
3180    vis_stdpipe = debugFile;
3181  else if (McOptionsReadUseMore(options) == TRUE)
3182    vis_stdpipe = popen("more", "w");
3183  else
3184    vis_stdpipe = vis_stdout;
3185  vis_stdout = vis_stdpipe;
3186
3187  arrayForEachItem(mdd_t *, invarStatesArray, i, invarFormulaStates) {
3188    if ((invarFormulaStates == NIL(mdd_t)) || (resultArray[i] == 1))
3189      continue;
3190    onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm);
3191    ringsUpToDate = Fsm_FsmTestReachabilityOnionRingsUpToDate(modelFsm);
3192    /* search for onion ring intersecting invarStates' */
3193    if (onionRings != NIL(array_t)) {
3194      for (j = 0; j < array_n(onionRings); j++) {
3195        outerOnionRing = array_fetch(mdd_t *, onionRings, j);
3196        if (!mdd_lequal(outerOnionRing, invarFormulaStates, 1, 1)) {
3197          computeReach = FALSE;
3198          break;
3199        }
3200      }
3201    }
3202
3203    /* no onion ring found, hence recompute with onion rings */
3204    if (computeReach == TRUE) {
3205      Mc_VerbosityLevel verbosity;
3206      int debugFlag;
3207      int ardc;
3208      int dcLevel = McOptionsReadDcLevel(options);
3209      verbosity = McOptionsReadVerbosityLevel(options);
3210      debugFlag = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c);
3211      if (dcLevel == McDcLevelArdc_c)
3212        ardc = 1;
3213      else
3214        ardc = 0;
3215      assert(!ringsUpToDate);
3216      reachableStates = Fsm_FsmComputeReachableStates(
3217        modelFsm, 0, (int)verbosity , 0, 0, debugFlag, 0, 0, approxFlag, ardc,
3218        0, invarStatesArray, (verbosity > 1), hintsStatesArray);
3219      mdd_free(reachableStates);
3220      /* find the onion ring with invariant failure */
3221      onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm);
3222      if (onionRings == NIL(array_t)) {
3223        fprintf(vis_stdout, "Unable to generate onion rings for counterexample.\n");
3224        fprintf(vis_stdout, "Try again with standard (without -A) options.\n");
3225        if (vis_stdout != tmpFile && vis_stdout != debugFile)
3226          (void)pclose(vis_stdpipe);
3227        vis_stdout = tmpFile;
3228        return;
3229      }
3230      ringsUpToDate = Fsm_FsmTestReachabilityOnionRingsUpToDate(modelFsm);
3231      for (j = 0; j < array_n(onionRings); j++) {
3232        outerOnionRing = array_fetch(mdd_t *, onionRings, j);
3233        if (!mdd_lequal(outerOnionRing, invarFormulaStates, 1, 1)) {
3234          break;
3235        }
3236      }
3237    }
3238    invarFormula = array_fetch(Ctlp_Formula_t *, invarFormulaArray, i);
3239    /* this is the case of  true negative */
3240    if (outerOnionRing != NIL(mdd_t)) {
3241      /* compute the set of bad states */
3242      if(Fsm_FsmReadFAFWFlag(modelFsm) > 1 && McOptionsReadInvarApproxFlag(options) == Fsm_Rch_Bfs_c)
3243        reachableBadStates = mdd_not(invarFormulaStates);
3244      else
3245        reachableBadStates = mdd_and(invarFormulaStates, outerOnionRing, 0, 1);
3246      /* pick one bad state */
3247      aBadReachableState = Mc_ComputeAState(reachableBadStates, modelFsm);
3248      mdd_free(reachableBadStates);
3249
3250      /* build a path from the initial states to the bad state */
3251      aPath = Mc_BuildPathFromCore(aBadReachableState, onionRings,
3252                                   modelFsm, McGreaterOrEqualZero_c);
3253      mdd_free(aBadReachableState);
3254
3255
3256      if(McOptionsReadDbgLevel(options)==2)
3257      {
3258
3259        (void) Mc_PrintPathAiger(aPath, modelFsm, McOptionsReadPrintInputs(options));
3260      }
3261      else
3262      {
3263        (void) fprintf(vis_stdout, "# INV: formula %d failed --- ", i+1);
3264        Ctlp_FormulaPrint(vis_stdout,
3265                        Ctlp_FormulaReadOriginalFormula(invarFormula));
3266        fprintf(vis_stdout, "\n");
3267
3268        (void) fprintf(vis_stdout, "# INV: calling debugger\n");
3269        if (array_n(aPath) > 1) {
3270          (void) fprintf(vis_stdout,
3271                        "# INV: a sequence of states starting at an initial ");
3272          (void) fprintf(vis_stdout, "state leading to a bad state\n");
3273        } else {
3274          (void) fprintf(vis_stdout,
3275                    "# INV: invariant fails at the following initial state\n");
3276        }
3277        (void) Mc_PrintPath(aPath, modelFsm, McOptionsReadPrintInputs(options));
3278      }
3279      (void) fprintf(vis_stdout, "\n");
3280
3281      McNormalizeBddPointer(aPath);
3282      mdd_array_free(aPath);
3283    } else {
3284      /* Was a false negative */
3285      assert (approxFlag == Fsm_Rch_Oa_c);
3286      (void) fprintf(vis_stdout, "# INV: formula passed --- ");
3287      Ctlp_FormulaPrint(vis_stdout,
3288                        Ctlp_FormulaReadOriginalFormula(invarFormula));
3289      fprintf(vis_stdout, "\n");
3290    }
3291  }
3292
3293  if (vis_stdout != tmpFile && vis_stdout != debugFile)
3294    (void)pclose(vis_stdpipe);
3295  vis_stdout = tmpFile;
3296} /* end of InvarPrintDebugInformation */
3297
3298
3299/**Function********************************************************************
3300
3301  Synopsis    [Sort formulae by fsm]
3302
3303  Description [Sort formulae by fsm. This creates an array of array of
3304  formulae. Each element of the outer array corresponds to an fsm
3305  reduced w.r.t the element (array of formulae). Both the array of
3306  formulae and the reduced fsms are returned. If there is no
3307  reduction, the reduced fsm is set to the totalFsm. While freeing the
3308  reduced fsms in the fsmArray, if the reduced fsm is set to total
3309  fsm, DO NOT free. ]
3310
3311  SideEffects [fsmArray is populated with reduced fsms.]
3312
3313******************************************************************************/
3314array_t *
3315SortFormulasByFsm(Fsm_Fsm_t *totalFsm,
3316                  array_t *invarFormulaArray,
3317                  array_t *fsmArray,
3318                  McOptions_t *options)
3319{
3320  array_t *resultArray;
3321  array_t *formulaArray;
3322  array_t *tempArray;
3323  int i, j, found;
3324  Ctlp_Formula_t *formula;
3325  Ntk_Network_t *network = Fsm_FsmReadNetwork(totalFsm);
3326  Fsm_Fsm_t *reducedFsm, *fsm;
3327  int reducedFsmPos = -1;
3328
3329  if (invarFormulaArray == NIL(array_t)) return invarFormulaArray;
3330  if (array_n(invarFormulaArray) == 0) return NIL(array_t);
3331
3332  tempArray = array_alloc(array_t *, 0);
3333  /* do a semantic check and a quantifier check */
3334  arrayForEachItem (Ctlp_Formula_t *, invarFormulaArray, i, formula) {
3335    if (!Mc_FormulaStaticSemanticCheckOnNetwork(formula, network, FALSE)){
3336      (void) fprintf(vis_stderr, "** inv error: error in parsing Atomic Formula:\n%s\n", error_string());
3337      error_init();
3338      Ctlp_FormulaFree(formula);
3339      continue;
3340    } else {
3341      if (Ctlp_FormulaTestIsQuantifierFree(formula) == FALSE) {
3342        (void) fprintf(vis_stderr, "** inv error: invariant formula refers to path quantifiers\n");
3343        Ctlp_FormulaFree(formula);
3344        continue;
3345      }
3346    }
3347    array_insert_last(Ctlp_Formula_t *, tempArray, formula);
3348  }
3349  if (array_n(tempArray) == 0) {
3350    array_free(tempArray);
3351    return NIL(array_t);
3352  }
3353
3354  /* if no -r option, return the original array */
3355  resultArray = array_alloc(array_t *, 0);
3356  if (McOptionsReadReduceFsm(options) == FALSE) {
3357    array_insert_last(array_t *, resultArray, tempArray);
3358    reducedFsm = McConstructReducedFsm(network, tempArray);
3359    if (reducedFsm != NIL(Fsm_Fsm_t)) {
3360      array_insert_last(Fsm_Fsm_t *, fsmArray, reducedFsm);
3361    } else {
3362      array_insert_last(Fsm_Fsm_t *, fsmArray, totalFsm);
3363    }
3364    return resultArray;
3365  }
3366
3367  /* We want to minimize per formula only when "-r" option is not specified */
3368  arrayForEachItem (Ctlp_Formula_t *, tempArray, i, formula) {
3369    /* Create reduced fsm */
3370    formulaArray = array_alloc(Ctlp_Formula_t *, 0);
3371    array_insert_last(Ctlp_Formula_t *, formulaArray, formula);
3372
3373    reducedFsm = McConstructReducedFsm(network, formulaArray);
3374    if (reducedFsm == NIL(Fsm_Fsm_t)) {
3375      /* no reduction */
3376      reducedFsm = totalFsm;
3377    }
3378
3379    /* Check if fsm already created */
3380    found = 0;
3381    for (j = 0; j < array_n(fsmArray); j++) {
3382      fsm = array_fetch (Fsm_Fsm_t *, fsmArray, j);
3383      found = Fsm_FsmCheckSameSubFsmInTotalFsm(totalFsm, reducedFsm, fsm);
3384      if (found) break;
3385    }
3386
3387    /* If found, add to the existing list. Else add a new reduced fsm */
3388    if (found) {
3389      if (reducedFsm != totalFsm) Fsm_FsmFree(reducedFsm);
3390      array_free(formulaArray);
3391      formulaArray = array_fetch(array_t *, resultArray, j);
3392      array_insert_last(Ctlp_Formula_t *, formulaArray, formula);
3393    } else {
3394      array_insert_last(Fsm_Fsm_t *, fsmArray, reducedFsm);
3395      array_insert_last(array_t *, resultArray, formulaArray);
3396      if (reducedFsm == totalFsm) reducedFsmPos = array_n(fsmArray)-1;
3397    }
3398  }
3399
3400  array_free(tempArray);
3401  /* swap the last reduced fsm with the total fsm. */
3402  if ((reducedFsmPos != -1) && (reducedFsmPos != array_n(fsmArray)-1)) {
3403    array_t *totalFsmFormulaArray;
3404    assert(array_n(fsmArray) == array_n(resultArray));
3405    fsm = array_fetch(Fsm_Fsm_t *, fsmArray, array_n(fsmArray)-1);
3406    array_insert(Fsm_Fsm_t *, fsmArray, reducedFsmPos, fsm);
3407    array_insert(Fsm_Fsm_t *, fsmArray, array_n(fsmArray)-1, totalFsm);
3408    formulaArray =  array_fetch(array_t *, resultArray, array_n(resultArray)-1);
3409    totalFsmFormulaArray = array_fetch(array_t *, resultArray, reducedFsmPos);
3410    array_insert(array_t *, resultArray, reducedFsmPos, formulaArray);
3411    array_insert(array_t *, resultArray, array_n(resultArray)-1, totalFsmFormulaArray);
3412  }
3413
3414  return resultArray;
3415} /* end of SortFormulasByFsm */
3416
3417
3418/**Function********************************************************************
3419
3420  Synopsis [Test if an invariant is violated in the current reachable
3421  set of the given FSM.]
3422
3423  Description [Test if an invariant is violated in the current
3424  reachable set of the given FSM. Returns FALSE if an invariant is
3425  violated and TRUE is no invariant is violated.]
3426
3427  SideEffects []
3428
3429******************************************************************************/
3430int
3431TestInvariantsInTotalFsm(Fsm_Fsm_t *totalFsm,
3432                         array_t *invarStatesArray,
3433                         int shellFlag)
3434{
3435  int i;
3436  mdd_t *invariant;
3437  mdd_t *reachableStates;
3438  boolean upToDate = FALSE; /* don't care initialization */
3439  if (shellFlag) {
3440    upToDate = Fsm_FsmReachabilityOnionRingsStates(totalFsm, &reachableStates);
3441  } else {
3442    reachableStates = Fsm_FsmReadCurrentReachableStates(totalFsm);
3443  }
3444  if (reachableStates == NIL(mdd_t)) return TRUE;
3445  if (mdd_is_tautology(reachableStates, 0)) return TRUE;
3446 
3447  arrayForEachItem(mdd_t *, invarStatesArray, i, invariant) {
3448    if (invariant == NIL(mdd_t)) continue;
3449    if (!mdd_lequal(reachableStates, invariant, 1, 1)) {
3450      if (shellFlag) mdd_free(reachableStates);
3451      return FALSE;
3452    }
3453  }
3454  if (shellFlag) mdd_free(reachableStates);
3455  if ((shellFlag && !upToDate) ||
3456      (Fsm_FsmReadReachabilityApproxComputationStatus(totalFsm) ==
3457       Fsm_Rch_Under_c))
3458    return TRUE;
3459  else
3460    return FALSE;
3461   
3462}
3463
3464
3465/**Function********************************************************************
3466
3467  Synopsis    [Compute the approximation of the result for
3468  EvaluateFormulaRecur.]
3469
3470  Description []
3471
3472  SideEffects [None]
3473
3474  SeeAlso     [EvaluateFormulaRecur]
3475
3476******************************************************************************/
3477Ctlp_Approx_t
3478ComputeResultingApproximation(
3479  Ctlp_FormulaType formulaType,
3480  Ctlp_Approx_t leftApproxType,
3481  Ctlp_Approx_t rightApproxType,
3482  Ctlp_Approx_t TRMinimization,
3483  Mc_EarlyTermination_t *earlyTermination,
3484  boolean fixpoint)
3485{
3486  Ctlp_Approx_t thisApproxType;
3487
3488  switch (formulaType) {
3489  case Ctlp_ID_c:
3490  case Ctlp_TRUE_c:
3491  case Ctlp_FALSE_c:
3492    thisApproxType = Ctlp_Exact_c;
3493    break;
3494  case Ctlp_NOT_c:
3495    if (leftApproxType == Ctlp_Incomparable_c) {
3496      thisApproxType = Ctlp_Incomparable_c;
3497    } else if (leftApproxType == Ctlp_Overapprox_c) {
3498      thisApproxType = Ctlp_Underapprox_c;
3499    } else if (leftApproxType == Ctlp_Underapprox_c) {
3500      thisApproxType = Ctlp_Overapprox_c;
3501    } else {
3502      thisApproxType = Ctlp_Exact_c;
3503    }
3504    break;
3505  case Ctlp_AND_c:
3506    if (leftApproxType == Ctlp_Incomparable_c ||
3507        rightApproxType == Ctlp_Incomparable_c ||
3508        (leftApproxType == Ctlp_Overapprox_c &&
3509         rightApproxType == Ctlp_Underapprox_c) ||
3510        (leftApproxType == Ctlp_Underapprox_c &&
3511         rightApproxType == Ctlp_Overapprox_c)) {
3512      thisApproxType = Ctlp_Incomparable_c;
3513    } else if (rightApproxType == Ctlp_Overapprox_c) {
3514      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
3515          leftApproxType == Ctlp_Exact_c) {
3516        thisApproxType = Ctlp_Exact_c;
3517      } else {
3518        thisApproxType = Ctlp_Overapprox_c;
3519      }
3520    } else if (leftApproxType == Ctlp_Overapprox_c) {
3521      thisApproxType = Ctlp_Overapprox_c;
3522    } else if (rightApproxType == Ctlp_Underapprox_c) {
3523      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
3524          leftApproxType == Ctlp_Exact_c) {
3525        thisApproxType = Ctlp_Exact_c;
3526      } else {
3527        thisApproxType = Ctlp_Underapprox_c;
3528      }
3529    } else if (leftApproxType == Ctlp_Underapprox_c) {
3530      thisApproxType = Ctlp_Underapprox_c;
3531    } else {
3532      thisApproxType = Ctlp_Exact_c;
3533    }
3534    break;
3535  case Ctlp_EQ_c:
3536  case Ctlp_XOR_c:
3537    if (leftApproxType != Ctlp_Exact_c || rightApproxType != Ctlp_Exact_c) {
3538      thisApproxType = Ctlp_Incomparable_c;
3539    } else {
3540      thisApproxType = Ctlp_Exact_c;
3541    }
3542    break;
3543  case Ctlp_THEN_c:
3544    if (leftApproxType == Ctlp_Incomparable_c ||
3545        rightApproxType == Ctlp_Incomparable_c ||
3546        (leftApproxType == Ctlp_Overapprox_c &&
3547         rightApproxType == Ctlp_Overapprox_c) ||
3548        (leftApproxType == Ctlp_Underapprox_c &&
3549         rightApproxType == Ctlp_Underapprox_c)) {
3550      thisApproxType = Ctlp_Incomparable_c;
3551    } else if (rightApproxType == Ctlp_Overapprox_c) {
3552      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
3553          leftApproxType == Ctlp_Exact_c) {
3554        thisApproxType = Ctlp_Exact_c;
3555      } else {
3556        thisApproxType = Ctlp_Overapprox_c;
3557      }
3558    } else if (leftApproxType == Ctlp_Underapprox_c) {
3559      thisApproxType = Ctlp_Overapprox_c;
3560    } else if (rightApproxType == Ctlp_Underapprox_c) {
3561      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
3562          leftApproxType == Ctlp_Exact_c) {
3563        thisApproxType = Ctlp_Exact_c;
3564      } else {
3565        thisApproxType = Ctlp_Underapprox_c;
3566      }
3567    } else if (leftApproxType == Ctlp_Overapprox_c) {
3568      thisApproxType = Ctlp_Underapprox_c;
3569    } else {
3570      thisApproxType = Ctlp_Exact_c;
3571    }
3572    break;
3573  case Ctlp_OR_c:
3574    if (leftApproxType == Ctlp_Incomparable_c ||
3575        rightApproxType == Ctlp_Incomparable_c ||
3576        (leftApproxType == Ctlp_Overapprox_c &&
3577         rightApproxType == Ctlp_Underapprox_c) ||
3578        (leftApproxType == Ctlp_Underapprox_c &&
3579         rightApproxType == Ctlp_Overapprox_c)) {
3580      thisApproxType = Ctlp_Incomparable_c;
3581    } else if (rightApproxType == Ctlp_Overapprox_c) {
3582      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
3583          leftApproxType == Ctlp_Exact_c) {
3584        thisApproxType = Ctlp_Exact_c;
3585      } else {
3586        thisApproxType = Ctlp_Overapprox_c;
3587      }
3588    } else if (leftApproxType == Ctlp_Overapprox_c) {
3589      thisApproxType = Ctlp_Overapprox_c;
3590    } else if (rightApproxType == Ctlp_Underapprox_c) {
3591      if (earlyTermination == MC_NO_EARLY_TERMINATION &&
3592          leftApproxType == Ctlp_Exact_c) {
3593        thisApproxType = Ctlp_Exact_c;
3594      } else {
3595        thisApproxType = Ctlp_Underapprox_c;
3596      }
3597    } else if (leftApproxType == Ctlp_Underapprox_c) {
3598      thisApproxType = Ctlp_Underapprox_c;
3599    } else {
3600      thisApproxType = Ctlp_Exact_c;
3601    }
3602    break;
3603  case Ctlp_EX_c:
3604    if (leftApproxType == Ctlp_Underapprox_c) {
3605      if (TRMinimization == Ctlp_Overapprox_c) {
3606        thisApproxType = Ctlp_Incomparable_c;
3607      } else {
3608        thisApproxType = Ctlp_Underapprox_c;
3609      }
3610    } else if (leftApproxType == Ctlp_Overapprox_c) {
3611      if (TRMinimization == Ctlp_Underapprox_c) {
3612        thisApproxType = Ctlp_Incomparable_c;
3613      } else {
3614        thisApproxType = Ctlp_Overapprox_c;
3615      }
3616    } else if (leftApproxType == Ctlp_Exact_c) {
3617      thisApproxType = TRMinimization;
3618    } else {
3619      thisApproxType = Ctlp_Incomparable_c;
3620    }
3621    break;
3622  case Ctlp_EU_c:
3623    if (leftApproxType == Ctlp_Incomparable_c ||
3624        rightApproxType == Ctlp_Incomparable_c ||
3625        (leftApproxType == Ctlp_Overapprox_c &&
3626         rightApproxType == Ctlp_Underapprox_c) ||
3627        (leftApproxType == Ctlp_Underapprox_c &&
3628         rightApproxType == Ctlp_Overapprox_c)) {
3629      thisApproxType = Ctlp_Incomparable_c;
3630    } else if (leftApproxType == Ctlp_Overapprox_c ||
3631               rightApproxType == Ctlp_Overapprox_c) {
3632      thisApproxType = Ctlp_Overapprox_c;
3633    } else if (leftApproxType == Ctlp_Underapprox_c ||
3634               rightApproxType == Ctlp_Underapprox_c) {
3635      thisApproxType = Ctlp_Underapprox_c;
3636    } else {
3637      thisApproxType = Ctlp_Exact_c;
3638    }
3639    if (!fixpoint) {
3640      if (TRMinimization == Ctlp_Overapprox_c ||
3641          thisApproxType == Ctlp_Overapprox_c) {
3642        thisApproxType = Ctlp_Incomparable_c;
3643      } else if (thisApproxType == Ctlp_Exact_c) {
3644        thisApproxType = Ctlp_Underapprox_c;
3645      }
3646    } else {
3647      if ((TRMinimization == Ctlp_Overapprox_c &&
3648           thisApproxType == Ctlp_Underapprox_c) ||
3649          (TRMinimization == Ctlp_Underapprox_c &&
3650           thisApproxType == Ctlp_Overapprox_c)) {
3651        thisApproxType = Ctlp_Incomparable_c;
3652      } else if (thisApproxType == Ctlp_Exact_c) {
3653        thisApproxType = TRMinimization;
3654      }
3655    }
3656    break;
3657  case Ctlp_EG_c:
3658    if (leftApproxType == Ctlp_Incomparable_c ||
3659        rightApproxType == Ctlp_Incomparable_c ||
3660        (leftApproxType == Ctlp_Overapprox_c &&
3661         rightApproxType == Ctlp_Underapprox_c) ||
3662        (leftApproxType == Ctlp_Underapprox_c &&
3663         rightApproxType == Ctlp_Overapprox_c)) {
3664      thisApproxType = Ctlp_Incomparable_c;
3665    } else if (leftApproxType == Ctlp_Overapprox_c ||
3666               rightApproxType == Ctlp_Overapprox_c) {
3667      thisApproxType = Ctlp_Overapprox_c;
3668    } else if (leftApproxType == Ctlp_Underapprox_c ||
3669               rightApproxType == Ctlp_Underapprox_c) {
3670      thisApproxType = Ctlp_Underapprox_c;
3671    } else {
3672      thisApproxType = Ctlp_Exact_c;
3673    }
3674    if (!fixpoint) {
3675      if (TRMinimization == Ctlp_Underapprox_c ||
3676          thisApproxType == Ctlp_Underapprox_c) {
3677        thisApproxType = Ctlp_Incomparable_c;
3678      } else if (thisApproxType == Ctlp_Exact_c) {
3679        thisApproxType = Ctlp_Overapprox_c;
3680      }
3681    } else {
3682      if ((TRMinimization == Ctlp_Overapprox_c &&
3683           thisApproxType == Ctlp_Underapprox_c) ||
3684          (TRMinimization == Ctlp_Underapprox_c &&
3685           thisApproxType == Ctlp_Overapprox_c)) {
3686        thisApproxType = Ctlp_Incomparable_c;
3687      } else if (thisApproxType == Ctlp_Exact_c) {
3688        thisApproxType = TRMinimization;
3689      }
3690    }
3691    break;
3692  case Ctlp_Cmp_c:
3693  case Ctlp_Init_c:
3694  case Ctlp_FwdU_c:
3695  case Ctlp_FwdG_c:
3696  case Ctlp_EY_c:
3697    /* no early termination and no hints in forward model checking */
3698    thisApproxType = Ctlp_Exact_c;
3699    break;
3700  default: fail("Encountered unknown type of CTL formula\n");
3701  }
3702
3703  return thisApproxType;
3704 
3705} /* ComputeResultingApproximation */
3706
3707
3708/*---------------------------------------------------------------------------*/
3709/* Definition of static functions                                            */
3710/*---------------------------------------------------------------------------*/
3711
3712
3713/**Function********************************************************************
3714
3715  Synopsis    [Model check formula on given fsm under fairness]
3716
3717  Description [This is the recursive part of Mc_FsmEvaluateFormula]
3718
3719  Comment [See Mc_EvaluateFormula.  The only difference is that
3720  EvaluateFormula takes care of global hints, and passes on an extra
3721  flag, TRMinimization that indicates how the current TR related to
3722  the exact TR.  Using this flag, the procedure decides in which field
3723  of the formula to store results (states, underapproxStates or
3724  overapproxStates) ]
3725
3726  SideEffects []
3727
3728******************************************************************************/
3729static mdd_t *
3730EvaluateFormulaRecur(
3731  Fsm_Fsm_t *modelFsm,
3732  Ctlp_Formula_t *ctlFormula,
3733  mdd_t *fairStates,
3734  Fsm_Fairness_t *fairCondition,
3735  array_t *modelCareStatesArray,
3736  Mc_EarlyTermination_t *earlyTermination,
3737  Fsm_HintsArray_t *hintsArray,
3738  Mc_GuidedSearch_t hintType,
3739  Ctlp_Approx_t TRMinimization,
3740  Ctlp_Approx_t *resultApproxType,
3741  Mc_VerbosityLevel verbosity,
3742  Mc_DcLevel dcLevel,
3743  int buildOnionRings,
3744  Mc_GSHScheduleType GSHschedule)
3745{
3746  mdd_t *leftMdd  = NIL(mdd_t);
3747  mdd_t *rightMdd = NIL(mdd_t);
3748  mdd_t *result   = NIL(mdd_t);
3749 
3750  mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
3751  array_t     *careStatesArray = NIL(array_t);
3752  mdd_t       *tmpMdd;
3753  mdd_t       *approx = NIL(mdd_t); /* prev computed approx of sat set */ 
3754  mdd_t *ctlFormulaStates = Ctlp_FormulaObtainStates( ctlFormula );
3755  Ctlp_Approx_t leftApproxType = Ctlp_Exact_c;
3756  Ctlp_Approx_t rightApproxType = Ctlp_Exact_c;
3757  Ctlp_Approx_t thisApproxType = Ctlp_Exact_c;
3758  boolean fixpoint = FALSE;
3759  boolean skipRight = FALSE;
3760
3761  if ( ctlFormulaStates ) {
3762    return ctlFormulaStates;
3763  }
3764 
3765  {
3766    Ctlp_Formula_t *leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
3767
3768    if (leftChild) {
3769      Mc_EarlyTermination_t *nextEarlyTermination =
3770        McObtainUpdatedEarlyTerminationCondition(
3771          earlyTermination, NIL(mdd_t), Ctlp_FormulaReadType(ctlFormula));
3772
3773      leftMdd = EvaluateFormulaRecur(modelFsm, leftChild, fairStates,
3774                                     fairCondition, modelCareStatesArray,
3775                                     nextEarlyTermination,
3776                                     hintsArray, hintType, TRMinimization,
3777                                     &leftApproxType, verbosity, dcLevel,
3778                                     buildOnionRings, GSHschedule);
3779      Mc_EarlyTerminationFree(nextEarlyTermination);
3780      if (!leftMdd) {
3781        return NIL(mdd_t);
3782      }
3783    }
3784  }
3785
3786  {/* read right */
3787    Ctlp_Formula_t *rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
3788
3789    if (rightChild) {
3790      Mc_EarlyTermination_t *nextEarlyTermination =
3791        McObtainUpdatedEarlyTerminationCondition(
3792          earlyTermination, leftMdd, Ctlp_FormulaReadType(ctlFormula));
3793
3794      skipRight = Mc_EarlyTerminationIsSkip(nextEarlyTermination);
3795      if (!skipRight) {
3796        rightMdd = EvaluateFormulaRecur(modelFsm, rightChild, fairStates,
3797                                        fairCondition, modelCareStatesArray,
3798                                        nextEarlyTermination,
3799                                        hintsArray, hintType, TRMinimization,
3800                                        &rightApproxType, verbosity, dcLevel,
3801                                        buildOnionRings, GSHschedule);
3802      }
3803      Mc_EarlyTerminationFree(nextEarlyTermination);
3804      if (!(rightMdd || skipRight)) {
3805        if (leftMdd)
3806          mdd_free(leftMdd);
3807        return NIL(mdd_t);
3808      }
3809    }
3810  }/* read right */
3811
3812  if (modelCareStatesArray != NIL(array_t)) {
3813    careStatesArray = modelCareStatesArray;
3814  } else {
3815    careStatesArray = array_alloc(mdd_t *, 0);
3816    array_insert_last(mdd_t *, careStatesArray, mdd_one(mddMgr));
3817  }
3818  switch (Ctlp_FormulaReadType(ctlFormula)) {
3819  case Ctlp_ID_c:
3820    assert(!skipRight);
3821    result = McModelCheckAtomicFormula(modelFsm, ctlFormula);
3822    break;
3823
3824  case Ctlp_TRUE_c:
3825    assert(!skipRight);
3826    result = mdd_one(mddMgr); break;
3827
3828  case Ctlp_FALSE_c:
3829    assert(!skipRight);
3830    result = mdd_zero(mddMgr); break;
3831
3832  case Ctlp_NOT_c:
3833    assert(!skipRight);
3834    result = mdd_not(leftMdd); break;
3835
3836  case Ctlp_AND_c:
3837    if (skipRight) {
3838      result = mdd_dup(leftMdd);
3839      rightApproxType = Ctlp_Overapprox_c;
3840    } else {
3841      result = mdd_and(leftMdd, rightMdd, 1, 1);
3842    }
3843    break;
3844
3845  case Ctlp_EQ_c:
3846    assert(!skipRight);
3847    result = mdd_xnor(leftMdd, rightMdd); break;
3848
3849  case Ctlp_XOR_c:
3850    assert(!skipRight);
3851    result = mdd_xor(leftMdd, rightMdd); break;
3852
3853  case Ctlp_THEN_c:
3854    if (skipRight) {
3855      result = mdd_dup(leftMdd);
3856      rightApproxType = Ctlp_Underapprox_c;
3857    } else {
3858      result = mdd_or(leftMdd, rightMdd, 0, 1);
3859    }
3860    break;
3861
3862  case Ctlp_OR_c:
3863    if (skipRight) {
3864      result = mdd_dup(leftMdd);
3865      rightApproxType = Ctlp_Underapprox_c;
3866    } else {
3867      result = mdd_or(leftMdd, rightMdd, 1, 1);
3868    }
3869    break;
3870
3871  case Ctlp_EX_c:
3872    assert(!skipRight);
3873    result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
3874                                     careStatesArray, verbosity, dcLevel);
3875    break;
3876
3877  case Ctlp_EU_c: {
3878    array_t *onionRings = NIL(array_t); /* array of mdd_t */
3879    boolean newrings;
3880
3881    assert(!skipRight);
3882    /* An underapproximation, together with its explanation may be stored. */
3883    approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Underapprox_c );
3884    onionRings = (array_t *) Ctlp_FormulaReadDebugData(ctlFormula);
3885    newrings = onionRings == NIL(array_t);
3886
3887    if (buildOnionRings){
3888      assert((approx != NIL(mdd_t) && onionRings != NIL(array_t)) ||
3889             (approx == NIL(mdd_t) && onionRings == NIL(array_t)));
3890      if(onionRings == NIL(array_t))
3891        onionRings = array_alloc(mdd_t *, 0);
3892    }
3893
3894    result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, rightMdd,
3895                                     approx, fairStates,
3896                                     careStatesArray,
3897                                     earlyTermination, hintsArray,
3898                                     hintType, onionRings,
3899                                     verbosity, dcLevel, &fixpoint);
3900
3901    if(buildOnionRings && newrings)
3902      Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings,
3903                             McFormulaFreeDebugData);
3904    if(approx != NIL(mdd_t))
3905      mdd_free(approx);
3906
3907    break;
3908  }
3909  case Ctlp_EG_c: {
3910    array_t  *arrayOfOnionRings = NIL(array_t); /* array of array of mdd_t* */
3911
3912    assert(!skipRight);
3913    if(buildOnionRings)
3914      arrayOfOnionRings = array_alloc(array_t *, 0);
3915
3916    approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Overapprox_c );
3917
3918    result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, approx, fairStates, 
3919                                     fairCondition, careStatesArray,
3920                                     earlyTermination, hintsArray, hintType, 
3921                                     &arrayOfOnionRings, verbosity,
3922                                     dcLevel, &fixpoint, GSHschedule);
3923
3924    if(buildOnionRings)
3925      Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
3926                             McFormulaFreeDebugData);
3927
3928    if(approx != NIL(mdd_t)) mdd_free(approx);
3929
3930    break;
3931  }
3932  case Ctlp_Cmp_c: {
3933    assert(!skipRight);
3934    if (Ctlp_FormulaReadCompareValue(ctlFormula) == 0)
3935      result = bdd_is_tautology(leftMdd, 0) ?
3936                mdd_one(mddMgr) : mdd_zero(mddMgr);
3937    else
3938      result = bdd_is_tautology(leftMdd, 0) ?
3939                mdd_zero(mddMgr) : mdd_one(mddMgr);
3940    break;
3941  }
3942  case Ctlp_Init_c:
3943    assert(!skipRight);
3944    result = Fsm_FsmComputeInitialStates(modelFsm);
3945    break;
3946  case Ctlp_FwdU_c:
3947    assert(!skipRight);
3948    if (buildOnionRings) {
3949      array_t *onionRings = array_alloc(mdd_t *, 0);
3950      result = Mc_FsmEvaluateFwdUFormula(modelFsm, leftMdd, rightMdd,
3951                                         fairStates, careStatesArray,
3952                                         onionRings, verbosity, dcLevel);
3953      Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings,
3954                             McFormulaFreeDebugData);
3955    }
3956    else {
3957      if (Ctlp_FormulaReadLeftChild(ctlFormula) &&
3958          Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(ctlFormula)) ==
3959          Ctlp_Init_c &&
3960          Ctlp_FormulaReadRightChild(ctlFormula) &&
3961          Ctlp_FormulaReadType(Ctlp_FormulaReadRightChild(ctlFormula)) ==
3962          Ctlp_TRUE_c &&
3963          Fsm_FsmTestIsReachabilityDone(modelFsm)) {
3964        result = mdd_dup(Fsm_FsmReadReachableStates(modelFsm));
3965        break;
3966      }
3967      result = Mc_FsmEvaluateFwdUFormula(modelFsm, leftMdd, rightMdd,
3968                                         fairStates, careStatesArray,
3969                                         NIL(array_t), verbosity, 
3970                                         dcLevel);
3971    }
3972    break;
3973  case Ctlp_FwdG_c:
3974    assert(!skipRight);
3975    if (buildOnionRings) {
3976      array_t *arrayOfOnionRings = array_alloc(array_t *, 0);
3977      result = Mc_FsmEvaluateFwdGFormula(modelFsm, leftMdd, rightMdd,
3978                                         fairStates, fairCondition,
3979                                         careStatesArray,
3980                                         arrayOfOnionRings, verbosity,
3981                                         dcLevel);   
3982      Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
3983                             McFormulaFreeDebugData);
3984    } else {
3985      result = Mc_FsmEvaluateFwdGFormula(modelFsm, leftMdd, rightMdd,
3986                                         fairStates, fairCondition,
3987                                         careStatesArray,
3988                                         NIL(array_t), verbosity,
3989                                         dcLevel);
3990    }
3991    break;
3992  case Ctlp_EY_c:
3993    assert(!skipRight);
3994    result = Mc_FsmEvaluateEYFormula(modelFsm, leftMdd, fairStates,
3995                                     careStatesArray, verbosity, dcLevel);
3996    break;
3997
3998  default: fail("Encountered unknown type of CTL formula\n");
3999  }
4000
4001  tmpMdd = mdd_dup(result);
4002  thisApproxType = ComputeResultingApproximation(
4003    Ctlp_FormulaReadType(ctlFormula), leftApproxType,
4004    rightApproxType, TRMinimization, earlyTermination, fixpoint);
4005  Ctlp_FormulaSetApproxStates(ctlFormula, tmpMdd, thisApproxType);
4006
4007#ifdef DEBUG_MC
4008  /* The following code is just for debugging */
4009  if ((verbosity == McVerbosityMax_c)) {
4010    char *type = Ctlp_FormulaGetTypeString(ctlFormula);
4011    if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_Cmp_c) {
4012      fprintf(vis_stdout, "Info : result for [Cmp]\n");
4013      if (bdd_is_tautology(result, 1))
4014        fprintf(vis_stdout, "TRUE\n");
4015      else
4016        fprintf(vis_stdout, "FALSE\n");
4017    }
4018    else if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_ID_c) {
4019      char *atomic = Ctlp_FormulaConvertToString(ctlFormula);
4020      fprintf(vis_stdout, "Info : satisfying minterms for [%s(%s)]:\n",
4021              type, atomic);
4022      free(atomic);
4023      if (bdd_is_tautology(result, 1))
4024        fprintf(vis_stdout, "-- TAUTOLOGY --\n");
4025      else if (bdd_is_tautology(result, 0))
4026        fprintf(vis_stdout, "-- null --\n");
4027      else
4028        (void)_McPrintSatisfyingMinterms(result, modelFsm);
4029    }
4030    else {
4031      fprintf(vis_stdout, "Info : satisfying minterms for [%s]:\n", type);
4032      if (bdd_is_tautology(result, 1))
4033        fprintf(vis_stdout, "-- TAUTOLOGY --\n");
4034      else if (bdd_is_tautology(result, 0))
4035        fprintf(vis_stdout, "-- null --\n");
4036      else
4037        (void)_McPrintSatisfyingMinterms(result, modelFsm);
4038    }
4039    free(type);
4040  }
4041#endif
4042 
4043  if (modelCareStatesArray == NIL(array_t))
4044    mdd_array_free(careStatesArray);
4045  if (leftMdd)
4046    mdd_free(leftMdd);
4047  if (rightMdd)
4048    mdd_free(rightMdd);
4049  *resultApproxType = thisApproxType;
4050  return result;
4051}
4052
4053
4054/**Function********************************************************************
4055
4056  Synopsis    [Reachable(p,q) = FwdUntil(p,q) ^ q]
4057
4058  Description [Reachable(p,q) = FwdUntil(p,q) ^ q. This Reachable operation is
4059  described in the paper "CTL Model Checking Based on Forward State Traversal"
4060  by H. Iwashita et al.]
4061
4062  SideEffects []
4063
4064******************************************************************************/
4065static mdd_t *
4066McForwardReachable(
4067  Fsm_Fsm_t *modelFsm,
4068  mdd_t *targetMdd,
4069  mdd_t *invariantMdd,
4070  mdd_t *fairStates,
4071  array_t *careStatesArray,
4072  array_t *onionRings,
4073  Mc_VerbosityLevel verbosity,
4074  Mc_DcLevel dcLevel)
4075{
4076  mdd_t *resultMdd, *fuMdd;
4077
4078  /* When McForwardReachable is called by Mc_FsmEvaluateFwdEHFormula
4079   * with no fairness constraints, this test saves one image
4080   * computation. */
4081  if (mdd_is_tautology(fairStates, 1) &&
4082      mdd_lequal_mod_care_set_array(invariantMdd, targetMdd,
4083                                    1, 1, careStatesArray)) {
4084    resultMdd = mdd_dup(invariantMdd);
4085    if (onionRings) {
4086      array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd));
4087    }
4088  } else {
4089    fuMdd = Mc_FsmEvaluateFwdUFormula(modelFsm, targetMdd, invariantMdd,
4090                                      fairStates, careStatesArray, onionRings,
4091                                      verbosity, dcLevel);
4092    resultMdd = mdd_and(fuMdd, invariantMdd, 1, 1);
4093    mdd_free(fuMdd);
4094  }
4095
4096  /* Updates onionRings not to have warning message in
4097   * Mc_FsmEvaluateFwdEHFormula since Reachable(p,q) = FwdUntil(p,q) ^ q.
4098   */
4099  if (onionRings) {
4100    int         i;
4101    mdd_t       *ring, *tmp;
4102
4103    for (i = 0 ; i < array_n(onionRings); i++) {
4104      tmp = array_fetch(mdd_t *, onionRings, i);
4105      ring = mdd_and(tmp, invariantMdd, 1, 1);
4106      mdd_free(tmp);
4107      array_insert(mdd_t *, onionRings, i, ring);
4108    }
4109  }
4110
4111  return(resultMdd);
4112}
Note: See TracBrowser for help on using the repository browser.