source: vis_dev/vis-2.3/src/mc/mcVacuum.c @ 31

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

vis2.3
File size: 92.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [mcVacuum.c]
4
5  PackageName [mc]
6
7  Synopsis    [Functions for vacuity detection.]
8
9  Description [This file contains the functions implementing vacuity
10  detection for CTL.  A CTL formula passes vacuously if it can be strengthened
11  by replacing subformulae by "bottom" (either TRUE or FALSE, depending on the
12  negation parity) without changing the outcome of model checking.  Likewise,
13  a formula fails vacuously if it can be weakened by replacing subformulae by
14  top (the negation of bottom) and still fail.  Under the assumption that a
15  formula is represented by a parse tree (as opposed to a more general parse
16  DAG) each subformula has a given negation parity.  Bottom stands for FALSE
17  if the replaced subformula appears under an even number of negation; it
18  stands for TRUE otherwise.  Since all CTL operators besides neagtion are
19  monotonically increasing in their operands, replacing a subformula with
20  bottom result in a stronger property, that is, one that implies the original
21  one.  A dual argument applies to replacements with top.<p>
22  This file contains two algorithms for CTL vacuity detection: The original
23  one of Beer et al. (CAV97), and an extension of the thorough vacuity
24  detection algorithm of Purandare and Somenzi (CAV2002), also known as "CTL
25  vacuum cleaning."<p>
26  The algorithm of Beer et al. applies to passing weak ACTL (w-ACTL)
27  properties.  Roughly speaking, in a w-ACTL property each binary opeartor has
28  at least one child that is a propositional formula.  A w-ACTL formula
29  contains a unique smallest important subformula.  This is replaced by bottom
30  to produce a witness formula.  If the witness formula passes, then the
31  original formula passed vacuously; otherwise, the counterexample to the
32  witness formula is an interesting witness to the original one.<p>
33  The implementation of the CTL vacuum cleaning algorithm in this file applies
34  to both passing and failing CTL properties.  For each formula, replacement
35  is attempted for all leaves, therefore identifying many more cases of
36  vacuity.  All the replacements are dealt with in one traversal of the parse
37  tree of the formula, paying attention to combining the cases that produce
38  identical sets of states.  For this reason, thorough vacuity detection is
39  usually much cheaper than running as many model checking experiments as
40  there are leaves.]
41
42  SeeAlso     [mcCmd.c mcMc.c]
43
44  Author      [Mitra Purandare]
45
46  Copyright   [Copyright (c) 2002-2005, Regents of the University of Colorado
47
48  All rights reserved.
49
50  Redistribution and use in source and binary forms, with or without
51  modification, are permitted provided that the following conditions
52  are met:
53
54  Redistributions of source code must retain the above copyright
55  notice, this list of conditions and the following disclaimer.
56
57  Redistributions in binary form must reproduce the above copyright
58  notice, this list of conditions and the following disclaimer in the
59  documentation and/or other materials provided with the distribution.
60
61  Neither the name of the University of Colorado nor the names of its
62  contributors may be used to endorse or promote products derived from
63  this software without specific prior written permission.
64
65  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
66  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
67  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
68  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
69  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
70  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
71  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
72  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
73  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
74  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
75  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
76  POSSIBILITY OF SUCH DAMAGE.]
77
78******************************************************************************/
79
80#include "ctlpInt.h"
81#include "mcInt.h"
82
83
84/*---------------------------------------------------------------------------*/
85/* Constant declarations                                                     */
86/*---------------------------------------------------------------------------*/
87
88/*---------------------------------------------------------------------------*/
89/* Stucture declarations                                                     */
90/*---------------------------------------------------------------------------*/
91
92/*---------------------------------------------------------------------------*/
93/* Type declarations                                                         */
94/*---------------------------------------------------------------------------*/
95
96/*---------------------------------------------------------------------------*/
97/* Variable declarations                                                     */
98/*---------------------------------------------------------------------------*/
99
100#ifndef lint
101static char rcsid[] UNUSED = "$Id: mcVacuum.c,v 1.1 2005/05/13 05:54:05 fabio Exp $";
102#endif
103
104/*---------------------------------------------------------------------------*/
105/* Macro declarations                                                        */
106/*---------------------------------------------------------------------------*/
107
108/**AutomaticStart*************************************************************/
109
110/*---------------------------------------------------------------------------*/
111/* Static function prototypes                                                */
112/*---------------------------------------------------------------------------*/
113
114static void EvaluateFormulaThoroughVacuity(Fsm_Fsm_t *fsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRing, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates);
115static void EvaluateFormulaWactlVacuity(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, mdd_t *modelInitialStates, McOptions_t *options);
116static void PrintVacuousBottom(mdd_t *modelInitialStates, Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, Mc_FwdBwdAnalysis traversalDirection, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity);
117static void PrintVacuous(mdd_t *modelInitialStates, Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, Mc_FwdBwdAnalysis traversalDirection, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity);
118static void ModelcheckAndVacuity(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, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates);
119static void CreateImportantWitness(Ctlp_Formula_t *OldctlFormula, Ctlp_Formula_t *ctlFormula, int i);
120static void CreateImportantCounterexample(Ctlp_Formula_t *OldctlFormula, Ctlp_Formula_t *ctlFormula, int i);
121static array_t * McMddArrayArrayDup(array_t *arrayBddArray);
122static void match_top(Ctlp_Formula_t *ctlFormula, array_t *mddArray, array_t *matchfound, array_t *matchelement);
123static void match_bot(Ctlp_Formula_t *ctlFormula, array_t *mddArray, array_t *matchfound, array_t *matchelement);
124static array_t * GenerateOnionRings(array_t* TempOnionRings, array_t* onionRings);
125static void FormulaFreeDebugDataVac(Ctlp_Formula_t *formula);
126
127/**AutomaticEnd***************************************************************/
128
129/*---------------------------------------------------------------------------*/
130/* Definition of exported functions                                          */
131/*---------------------------------------------------------------------------*/
132
133
134/*---------------------------------------------------------------------------*/
135/* Definition of internal functions                                          */
136/*---------------------------------------------------------------------------*/
137
138/**Function********************************************************************
139
140  Synopsis    [Model checks a formula and checks for its vacuity.]
141
142  Description [This function dispatches either w-ACTL vacuity detection or
143  CTL vacuum cleaning.  In the latter case also takes care of printing
144  results.]
145
146  SideEffects [Annotates the nodes of the CTL formula with various sets.]
147
148  SeeAlso     [EvaluateFormulaWactlVacuity EvaluateFormulaThoroughVacuity]
149
150******************************************************************************/
151void
152McVacuityDetection(
153  Fsm_Fsm_t *modelFsm,
154  Ctlp_Formula_t *ctlFormula,
155  int i,
156  mdd_t *fairStates,
157  Fsm_Fairness_t *fairCond,
158  array_t *modelCareStatesArray,
159  Mc_EarlyTermination_t *earlyTermination,
160  array_t *hintsStatesArray,
161  Mc_GuidedSearch_t guidedSearchType,
162  mdd_t *modelInitialStates,
163  McOptions_t *options)
164{
165
166  if (McOptionsReadBeerMethod(options)) {
167    EvaluateFormulaWactlVacuity(modelFsm, ctlFormula, i, fairStates, fairCond,
168                                modelCareStatesArray, earlyTermination,
169                                hintsStatesArray, guidedSearchType,
170                                modelInitialStates, options);
171  }
172  else {
173    mdd_t *ctlFormulaStates;
174    boolean result;
175    Mc_VerbosityLevel verbosity = McOptionsReadVerbosityLevel(options);
176    Mc_DcLevel dcLevel = McOptionsReadDcLevel(options);
177    Mc_GSHScheduleType GSHschedule = McOptionsReadSchedule(options);
178    int buildOnionRings =
179      (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity);
180    Mc_FwdBwdAnalysis traversalDirection =
181      McOptionsReadTraversalDirection(options);
182    mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
183
184    Ctlp_FormulaNegations(ctlFormula,Ctlp_Even_c);
185    EvaluateFormulaThoroughVacuity(modelFsm, ctlFormula, fairStates,
186                                   fairCond, modelCareStatesArray,
187                                   earlyTermination, hintsStatesArray,
188                                   guidedSearchType, verbosity, dcLevel,
189                                   buildOnionRings, GSHschedule,
190                                   modelInitialStates);
191    Mc_EarlyTerminationFree(earlyTermination);
192    if(hintsStatesArray != NIL(array_t))
193      mdd_array_free(hintsStatesArray);
194    ctlFormulaStates = array_fetch(mdd_t *,ctlFormula->Bottomstates,0);
195    /* user feedback on succes/fail */
196    result = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
197                             ctlFormula, ctlFormulaStates,
198                             modelInitialStates, modelCareStatesArray,
199                             options, verbosity);
200    if (result == TRUE) {
201      PrintVacuous(modelInitialStates,modelFsm,ctlFormula,
202                   traversalDirection,modelCareStatesArray,
203                   options, verbosity);
204    }
205    else {
206      PrintVacuousBottom(modelInitialStates,modelFsm,ctlFormula,
207                         traversalDirection,modelCareStatesArray,
208                         options, verbosity);
209    }
210    FormulaFreeDebugDataVac(ctlFormula);
211  }
212
213} /* McVacuityDetection */
214
215
216/*---------------------------------------------------------------------------*/
217/* Definition of static functions                                            */
218/*---------------------------------------------------------------------------*/
219
220
221/**Function********************************************************************
222
223  Synopsis    [Applies vacuum cleaning to a CTL formula.]
224
225  Description [This function evaluates all possible leaf replacements in
226  parallel and attaches the information to the parse tree.  This is a wrapper
227  around ModelcheckAndVacuity; it is mainly responsible of dealing with
228  global/local hints.]
229
230  SideEffects [Annotates the formula parse tree.]
231
232  SeeAlso     [McVacuityDetection EvaluateFormulaWactlVacuity
233  ModelcheckAndVacuity]
234
235******************************************************************************/
236static void
237EvaluateFormulaThoroughVacuity(
238  Fsm_Fsm_t *fsm,
239  Ctlp_Formula_t *ctlFormula,
240  mdd_t *fairStates,
241  Fsm_Fairness_t *fairCondition,
242  array_t *careStatesArray,
243  Mc_EarlyTermination_t *earlyTermination,
244  Fsm_HintsArray_t *hintsArray,
245  Mc_GuidedSearch_t hintType,
246  Mc_VerbosityLevel verbosity,
247  Mc_DcLevel dcLevel,
248  int buildOnionRing,
249  Mc_GSHScheduleType GSHschedule,
250  mdd_t *modelInitialStates)
251{
252  mdd_t *hint;      /* to iterate over hintsArray */
253  int   hintnr;     /* idem                       */
254  assert(hintType == Mc_None_c || hintsArray != NIL(Fsm_HintsArray_t));
255
256  if(hintType != Mc_Global_c) {
257    ModelcheckAndVacuity(fsm, ctlFormula, fairStates,
258                         fairCondition, careStatesArray,
259                         earlyTermination, hintsArray, hintType,
260                         Ctlp_Exact_c, verbosity, dcLevel,
261                         buildOnionRing, GSHschedule,
262                         modelInitialStates);
263    return;
264  }
265  else{
266    array_t *result = NIL(array_t);
267    Ctlp_Approx_t approx;
268
269    if(verbosity >= McVerbosityMax_c)
270      fprintf(vis_stdout, "--Using global hints\n");
271   
272    arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){
273      if(result != NIL(array_t))
274        array_free(result);
275     
276      if(verbosity >= McVerbosityMax_c)
277        fprintf(vis_stdout, "--Instantiating global hint %d\n", hintnr);
278     
279      Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c,
280                          (verbosity >= McVerbosityMax_c));
281     
282      approx = mdd_is_tautology(hint, 1) ? Ctlp_Exact_c : Ctlp_Underapprox_c;
283
284      ModelcheckAndVacuity(fsm,ctlFormula, fairStates,
285                           fairCondition, careStatesArray,
286                           earlyTermination, hintsArray, hintType,
287                           approx, verbosity,
288                           dcLevel, buildOnionRing,GSHschedule,
289                           modelInitialStates); 
290      /* TBD: take into account (early) termination here */
291    }
292    Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c));
293
294    return;
295  }
296} /* EvaluateFormulaThoroughVacuity */
297
298
299/**Function********************************************************************
300
301  Synopsis [Applies vacuity detection to a w-ACTL formula.]
302
303  Description [This function applies the algorithm of Beer et al. (CAV97) for
304  vacuity detection of passing w-ACTL formulae.  First regular model checking
305  is applied to the given CTL formula.  If the formula passes and is in w-ACTL,
306  the witness formula is obtained by replacing the smallest important
307  subformula with bottom.  Model checking is then applied to the witness
308  formula.  A vacuous pass is reported if the witness property holds.
309  Otherwise, the counterexample is an interesting witness to the original
310  formula, that is, an execution of the model in which the given property
311  holds in a non trivial manner.]
312
313  SideEffects [Annotates the parse tree of the formula.]
314
315  SeeAlso     [McVacuityDetection EvaluateFormulaThoroughVacuity]
316
317******************************************************************************/
318static void
319EvaluateFormulaWactlVacuity(
320  Fsm_Fsm_t *modelFsm,
321  Ctlp_Formula_t *ctlFormula,
322  int i,
323  mdd_t *fairStates,
324  Fsm_Fairness_t *fairCond,
325  array_t *modelCareStatesArray,
326  Mc_EarlyTermination_t *earlyTermination,
327  array_t *hintsStatesArray,
328  Mc_GuidedSearch_t guidedSearchType,
329  mdd_t *modelInitialStates,
330  McOptions_t *options)
331{
332  mdd_t *ctlFormulaStates;
333  boolean result1, result2;
334  Mc_VerbosityLevel verbosity = McOptionsReadVerbosityLevel(options);
335  Mc_DcLevel dcLevel = McOptionsReadDcLevel(options);
336  Mc_GSHScheduleType GSHschedule = McOptionsReadSchedule(options);
337  int buildOnionRings =
338    (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity);
339  Mc_FwdBwdAnalysis traversalDirection =
340    McOptionsReadTraversalDirection(options);
341  mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
342
343  ctlFormulaStates =
344    Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates,
345                          fairCond, modelCareStatesArray,
346                          earlyTermination, hintsStatesArray,
347                          guidedSearchType, verbosity, dcLevel,
348                          buildOnionRings,GSHschedule);
349
350  Mc_EarlyTerminationFree(earlyTermination);
351  if(hintsStatesArray != NIL(array_t))
352    mdd_array_free(hintsStatesArray);
353  result1 = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
354                            ctlFormula, ctlFormulaStates,
355                            modelInitialStates, modelCareStatesArray,
356                            options, verbosity); 
357  mdd_free(ctlFormulaStates);
358
359  if (result1 == FALSE)
360    fprintf(vis_stdout,
361            "# MC: Original formula failed. Aborting vacuity detection\n");
362  else {
363    /* see if we can create a witness formula */
364    if ((Ctlp_CheckClassOfExistentialFormula(ctlFormula) != Ctlp_ACTL_c) &&
365        (Ctlp_CheckClassOfExistentialFormula(ctlFormula) != Ctlp_QuantifierFree_c)) {
366      fprintf(vis_stdout,
367              "# MC: Not an ACTL Formula. Aborting vacuity detection\n");
368    }
369    else {
370      if (Ctlp_CheckIfWACTL(Ctlp_FormulaReadOriginalFormula(ctlFormula)) == Ctlp_NONWACTL_c) {
371        fprintf(vis_stdout, "# MC: Not a w-ACTL Formula. Aborting vacuity detection\n");
372      }
373      else {
374        Ctlp_Formula_t *origFormula, *witFormula;
375        /* We can create a witness formula.  Annotate the original
376         * formula with negation parity info and then create a copy
377         * with the smallest important formula replaced by bottom. */
378        fprintf(vis_stdout, "Model checking the witness formula\n");
379        origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
380        Ctlp_FormulaNegations(origFormula, Ctlp_Even_c);
381        witFormula = Ctlp_FormulaCreateWitnessFormula(origFormula);
382        ctlFormula = Ctlp_FormulaConvertToExistentialForm(witFormula);
383
384        /* some user feedback */
385        if (verbosity != McVerbosityNone_c) {
386          (void)fprintf(vis_stdout, "Checking witness formula[%d] : ", i + 1);
387          Ctlp_FormulaPrint(vis_stdout,
388                            Ctlp_FormulaReadOriginalFormula(ctlFormula));
389          (void)fprintf (vis_stdout, "\n");
390          assert(traversalDirection != McFwd_c);
391        }
392        /************** the actual computation *************************/
393        earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates);
394        ctlFormulaStates =
395          Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates,
396                                fairCond, modelCareStatesArray,
397                                earlyTermination, hintsStatesArray,
398                                guidedSearchType, verbosity, dcLevel,
399                                buildOnionRings,GSHschedule);
400
401        Mc_EarlyTerminationFree(earlyTermination);
402        if(hintsStatesArray != NIL(array_t))
403          mdd_array_free(hintsStatesArray);
404        /* user feedback on succes/fail */
405        result2 = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
406                                  ctlFormula, ctlFormulaStates,
407                                  modelInitialStates,
408                                  modelCareStatesArray,
409                                  options, verbosity);
410        if (result2)
411          (void)fprintf(vis_stdout, "# MC: Vacuous pass\n");
412        else
413          (void)fprintf(vis_stdout, "# MC: Not a vacuous pass\n");
414        mdd_free(ctlFormulaStates);
415        Ctlp_FormulaFree(ctlFormula);
416        Ctlp_FormulaFree(witFormula);
417      }
418    }
419  }
420
421} /* EvaluateFormulaWactlVacuity */
422
423
424/**Function********************************************************************
425
426  Synopsis    [Prints results of vacuum cleaning for a failing CTL property.]
427
428  Description [For a failing CTL property reports all vacuous failures.  If so
429  requested, it also produces interesting counterexamples, that is,
430  computations of the model for which even the weakened property fails.]
431
432  SideEffects [none]
433
434  SeeAlso     [PrintVacuous]
435
436******************************************************************************/
437static void
438PrintVacuousBottom(
439  mdd_t *modelInitialStates,
440  Fsm_Fsm_t *modelFsm,
441  Ctlp_Formula_t *ctlFormula,
442  Mc_FwdBwdAnalysis traversalDirection,
443  array_t *modelCareStatesArray,
444  McOptions_t *options,
445  Mc_VerbosityLevel verbosity)
446{
447  Ctlp_Formula_t *formula,*Int_Counter_CtlFormula;
448  boolean vacuous = FALSE;
449  int i;
450  Ctlp_FormulaType  type;
451  if (traversalDirection == McBwd_c){
452    for (i=1;i<array_n(ctlFormula->Topstates);i++){
453      if (!(mdd_lequal(modelInitialStates, array_fetch(mdd_t *,ctlFormula->Topstates,i),1,1))){
454        formula = array_fetch(Ctlp_Formula_t *,ctlFormula->leaves,(i-1));
455        type = Ctlp_FormulaReadType(formula);
456        if((type != Ctlp_FALSE_c) && (type != Ctlp_TRUE_c)) {
457          fprintf(vis_stdout, "# MC: Vacuous failure : ");
458          Ctlp_FormulaPrint(vis_stdout, formula);
459          fprintf(vis_stdout, "\n");
460          if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c){
461            fprintf(vis_stdout, "# Generating interesting counterexample :\n");
462            Int_Counter_CtlFormula = Ctlp_FormulaDup(ctlFormula);
463            CreateImportantCounterexample(ctlFormula,Int_Counter_CtlFormula,i);
464            McFsmDebugFormula(options,Int_Counter_CtlFormula,modelFsm,
465                              modelCareStatesArray);
466            Ctlp_FormulaFree(Int_Counter_CtlFormula);
467          }
468          vacuous = TRUE;
469        }
470      }
471    }
472    if (vacuous == FALSE){
473      (void)fprintf(vis_stdout, "# MC: No vacuous failures\n");
474    }
475  }
476  else{
477    (void)fprintf(vis_stderr, "# MC: Vacuity can not be checked\n");
478  }
479} /* PrintVacuousBottom */
480
481
482/**Function********************************************************************
483
484  Synopsis    [Prints results of vacuum cleaning for a passing CTL property.]
485
486  Description [For a passing CTL property reports all vacuous passes.  If so
487  requested, it also produces interesting witnesses, that is,
488  computations of the model for which the original property holds non
489  trivially. (Alternatively, the strengthened property that gave the vacuous
490  pass fails.)]
491
492  SideEffects [none]
493
494  SeeAlso     [McVacuityDetection PrintVacuousBottom]
495
496******************************************************************************/
497static void
498PrintVacuous(
499  mdd_t *modelInitialStates,
500  Fsm_Fsm_t *modelFsm,
501  Ctlp_Formula_t *ctlFormula,
502  Mc_FwdBwdAnalysis traversalDirection,
503  array_t *modelCareStatesArray,
504  McOptions_t *options,
505  Mc_VerbosityLevel verbosity)
506{
507  Ctlp_Formula_t *formula,*Int_Wit_CtlFormula;
508  boolean vacuous = FALSE;
509  int i;
510  Ctlp_FormulaType  type;
511  if (traversalDirection == McBwd_c) {
512    for (i=1;i<array_n(ctlFormula->Bottomstates);i++) {
513      formula = array_fetch(Ctlp_Formula_t *,ctlFormula->leaves,(i-1));
514      type = Ctlp_FormulaReadType(formula);
515      if (mdd_lequal(modelInitialStates, array_fetch(mdd_t *,ctlFormula->Bottomstates,i),1,1)) {
516        if((type != Ctlp_FALSE_c) && (type != Ctlp_TRUE_c)) {
517          fprintf(vis_stdout, "# MC: Vacuous pass : ");
518          Ctlp_FormulaPrint(vis_stdout, formula);
519          fprintf(vis_stdout, "\n");
520          vacuous = TRUE;
521        }
522      }
523      else { /* CounterExample Generation */
524        if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c){
525          fprintf(vis_stdout, "# MC: Not a vacuous pass : ");
526          Ctlp_FormulaPrint(vis_stdout, formula);
527          fprintf(vis_stdout, "\n");
528          fprintf(vis_stdout, "# Generating interesting witness :\n");
529          Int_Wit_CtlFormula = Ctlp_FormulaDup(ctlFormula);
530          CreateImportantWitness(ctlFormula,Int_Wit_CtlFormula,i);
531          McFsmDebugFormula(options,Int_Wit_CtlFormula,modelFsm,
532                            modelCareStatesArray);
533          Ctlp_FormulaFree(Int_Wit_CtlFormula);
534        }
535      }
536    }
537    if (vacuous == FALSE){
538      (void)fprintf(vis_stdout, "# MC: No vacuous passes\n");
539    }
540  }
541  else{
542    (void)fprintf(vis_stderr, "# MC: Vacuity cannot be checked\n");
543  }
544} /* PrintVacuous */
545
546
547/**Function********************************************************************
548
549  Synopsis    [Core algorithm for CTL vacuum cleaning.]
550
551  Description [This function recursively annotates the parse tree of a
552  CTL formula with the sets of states that satisfy the original formula as
553  well as the various replacements.  If debugging is requested, it also stores
554  onion rings.  Since it is not known in advance whether the original formula
555  passes or fails, this function computes both bottom and top replacements and
556  tries to use monotonicity properties to accelerate fixpoint computations.]
557
558  SideEffects [Annotates the formula parse tree.]
559
560  SeeAlso [EvaluateFormulaThoroughVacuity]
561
562******************************************************************************/
563static void
564ModelcheckAndVacuity(
565  Fsm_Fsm_t *modelFsm,
566  Ctlp_Formula_t *ctlFormula,
567  mdd_t *fairStates,
568  Fsm_Fairness_t *fairCondition,
569  array_t *modelCareStatesArray,
570  Mc_EarlyTermination_t *earlyTermination,
571  Fsm_HintsArray_t *hintsArray,
572  Mc_GuidedSearch_t hintType,
573  Ctlp_Approx_t TRMinimization,
574  Mc_VerbosityLevel verbosity,
575  Mc_DcLevel dcLevel,
576  int buildOnionRings,
577  Mc_GSHScheduleType GSHschedule,
578  mdd_t *modelInitialStates)
579{
580  mdd_t *result  = NIL(mdd_t);
581  mdd_t *result_new = NIL(mdd_t);
582  mdd_t *result_bot  = NIL(mdd_t);
583  mdd_t *result_top  = NIL(mdd_t);
584  mdd_t *result_underapprox = NIL(mdd_t);
585  mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm);
586  array_t     *careStatesArray = NIL(array_t);
587  array_t     *mddArray_bot = NIL(array_t);
588  array_t     *mddArray_top = NIL(array_t);
589  array_t     *leavesArray = NIL(array_t);
590  array_t     *leavesLeftArray = NIL(array_t);
591  array_t     *leavesRightArray = NIL(array_t);
592  array_t     *matchfound_bot = NIL(array_t);
593  array_t     *matchfound_top = NIL(array_t);
594  array_t     *matchelement_bot = NIL(array_t);
595  array_t     *matchelement_top = NIL(array_t);
596  mdd_t       *tmpMdd;
597  mdd_t       *approx = NIL(mdd_t); /* prev computed approx of sat set */ 
598  /*  mdd_t *ctlFormulaStates = Ctlp_FormulaObtainStates( ctlFormula ); */
599  Ctlp_Formula_t *leftChild,*rightChild ;
600  mdd_t *leftMdd = NIL(mdd_t);
601  mdd_t *rightMdd = NIL(mdd_t);
602  Ctlp_Approx_t leftApproxType = Ctlp_Exact_c;
603  Ctlp_Approx_t rightApproxType = Ctlp_Exact_c;
604  Ctlp_Approx_t thisApproxType = Ctlp_Exact_c;
605  boolean fixpoint = FALSE;
606  /* boolean approx_decide = FALSE; */
607  /* We will propagate early termination ONLY to the outmost fixpoint,
608     and only propagate through negation. We should also propagate
609     over other boolean operators, and maybe temporal operators.
610     Propagation over negation is done by complementing the type. */
611  rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
612  leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
613
614  if (leftChild) {
615    if ((leftChild->share) == 1){
616      Mc_EarlyTermination_t *nextEarlyTermination =
617        McObtainUpdatedEarlyTerminationCondition(
618          earlyTermination, NIL(mdd_t), Ctlp_FormulaReadType(ctlFormula));
619
620      ModelcheckAndVacuity(modelFsm, leftChild,fairStates,
621                           fairCondition, modelCareStatesArray,
622                           nextEarlyTermination,
623                           hintsArray, hintType,
624                           TRMinimization, verbosity,dcLevel,
625                           buildOnionRings, GSHschedule,
626                           modelInitialStates);
627      Mc_EarlyTerminationFree(nextEarlyTermination);
628    }
629  }
630
631  if (rightChild) {
632    if((rightChild->share) == 1) {
633      Mc_EarlyTermination_t *nextEarlyTermination =
634        McObtainUpdatedEarlyTerminationCondition(
635          earlyTermination,NIL(mdd_t) ,Ctlp_FormulaReadType(ctlFormula));
636      ModelcheckAndVacuity(modelFsm, rightChild, fairStates,
637                           fairCondition,
638                           modelCareStatesArray,
639                           nextEarlyTermination,
640                           hintsArray, hintType,
641                           TRMinimization, verbosity, dcLevel,
642                           buildOnionRings, GSHschedule,
643                           modelInitialStates);
644      Mc_EarlyTerminationFree(nextEarlyTermination);
645    }
646  }
647  if (modelCareStatesArray != NIL(array_t)) {
648    careStatesArray = modelCareStatesArray;
649  } else {
650    careStatesArray = array_alloc(mdd_t *, 0);
651    array_insert_last(mdd_t *, careStatesArray, mdd_one(mddMgr));
652  }
653  mddArray_bot = array_alloc(mdd_t *, 0);
654  mddArray_top = array_alloc(mdd_t *, 0);
655  ctlFormula->share = 2;
656  switch (Ctlp_FormulaReadType(ctlFormula)) {
657  case Ctlp_ID_c :{
658    result = McModelCheckAtomicFormula(modelFsm, ctlFormula);
659    matchfound_top = array_alloc(boolean, 0);
660    matchfound_bot = array_alloc(boolean, 0);
661    matchelement_top = array_alloc(int, 0);
662    matchelement_bot = array_alloc(int, 0);
663    leavesArray = array_alloc(Ctlp_Formula_t *, 0);
664    array_insert(mdd_t *, mddArray_bot , 0, mdd_dup(result));
665    array_insert(mdd_t *, mddArray_top , 0, result);
666    /* if the formula is an important subformula, we need to find the
667       bottom and top set for it as well. */
668    if (ctlFormula->negation_parity != Ctlp_EvenOdd_c) {
669      array_insert_last(Ctlp_Formula_t *, leavesArray, ctlFormula);
670      if (ctlFormula->negation_parity == Ctlp_Even_c) {
671        /* if the formula has even negation partity, it should be replaced
672           with FALSE. */
673        result_bot = mdd_zero(mddMgr);
674        result_top = mdd_one(mddMgr);
675      }
676      else {
677        /* if the formula has odd negation parity, it should be replaced
678           with TRUE. */
679        result_bot = mdd_one(mddMgr);
680        result_top = mdd_zero(mddMgr);
681      }
682      array_insert_last(mdd_t *,mddArray_bot ,result_bot);
683      array_insert_last(mdd_t *,mddArray_top ,result_top);
684      /*  Finding match for bottom sets */
685      if(mdd_equal(result_bot,array_fetch(mdd_t *, mddArray_bot, 0))){
686        array_insert(boolean, matchfound_bot, 1 ,TRUE);
687        array_insert(int, matchelement_bot, 1 ,0);
688      }
689      else
690        array_insert(boolean, matchfound_bot, 1 ,FALSE);
691      /* Finding match for top sets */
692      if(mdd_equal(result_top,array_fetch(mdd_t *, mddArray_top, 0))){
693        array_insert(boolean, matchfound_top, 1 ,TRUE);
694        array_insert(int, matchelement_top, 1 ,0);
695      }
696      else
697        array_insert(boolean, matchfound_top, 1 ,FALSE);
698    }
699    array_insert(boolean, matchfound_bot, 0 ,FALSE);
700    array_insert(boolean, matchfound_top, 0 ,FALSE);
701    /* only exact set will be there if the formula is not an important
702       subformula. */
703    ctlFormula->Topstates= mddArray_top;
704    ctlFormula->matchfound_top = matchfound_top;
705    ctlFormula->matchelement_top = matchelement_top;
706    ctlFormula->Bottomstates = mddArray_bot;
707    ctlFormula->matchfound_bot = matchfound_bot;
708    ctlFormula->matchelement_bot = matchelement_bot;
709    ctlFormula->leaves = leavesArray;
710    break;
711  }
712  case Ctlp_TRUE_c :{
713    result = mdd_one(mddMgr);
714    leavesArray = array_alloc(Ctlp_Formula_t *, 0);
715    matchfound_top = array_alloc(boolean, 0);
716    matchfound_bot = array_alloc(boolean, 0);
717    matchelement_top = array_alloc(int, 0);
718    matchelement_bot = array_alloc(int, 0);
719    array_insert_last(mdd_t *,mddArray_bot , mdd_dup(result));
720    array_insert_last(mdd_t *,mddArray_top , result);
721    array_insert(boolean, matchfound_bot, 0 ,FALSE);
722    array_insert(boolean, matchfound_top, 0 ,FALSE);
723    ctlFormula->Bottomstates = mddArray_bot;
724    ctlFormula->matchfound_bot = matchfound_bot;
725    ctlFormula->matchelement_bot = matchelement_bot;
726    ctlFormula->Topstates = mddArray_top;
727    ctlFormula->matchfound_top = matchfound_top;
728    ctlFormula->matchelement_top = matchelement_top;
729    ctlFormula->leaves = leavesArray;
730    break;
731  }
732  case Ctlp_FALSE_c :{
733    result = mdd_zero(mddMgr);
734    leavesArray = array_alloc(Ctlp_Formula_t *, 0);
735    matchfound_top = array_alloc(boolean, 0);
736    matchfound_bot = array_alloc(boolean, 0);
737    matchelement_top = array_alloc(int, 0);
738    matchelement_bot = array_alloc(int, 0);
739    array_insert_last(mdd_t *,mddArray_bot ,mdd_dup(result));
740    array_insert_last(mdd_t *,mddArray_top ,mdd_dup(result));   
741    array_insert(boolean, matchfound_bot, 0 ,FALSE);
742    array_insert(boolean, matchfound_top, 0 ,FALSE);
743    ctlFormula->Bottomstates = mddArray_bot;
744    ctlFormula->matchfound_bot = matchfound_bot;
745    ctlFormula->matchelement_bot = matchelement_bot;
746    ctlFormula->Topstates = mddArray_top;
747    ctlFormula->matchfound_top = matchfound_top;
748    ctlFormula->matchelement_top = matchelement_top;
749    ctlFormula->leaves = leavesArray;
750    break;
751  }
752  case Ctlp_NOT_c :{
753    int i,positionmatch;
754    arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
755      /* Now we shoud negate the accurate as well bottom mdds */
756      /* Compute Bottom sets */
757      if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){
758        result = mdd_not(leftMdd);
759        array_insert_last(mdd_t *, mddArray_bot, mdd_dup(result));
760        mdd_free(result);
761      }
762      else{
763        positionmatch =  array_fetch(int, leftChild->matchelement_bot, i);
764        result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch));
765        array_insert_last(mdd_t *, mddArray_bot,result);
766      }
767    }
768    arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
769      /* Compute for Top States */
770      if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){
771        result = mdd_not(leftMdd);
772        array_insert_last(mdd_t *, mddArray_top, mdd_dup(result));
773        mdd_free(result);
774      }
775      else{
776        positionmatch =  array_fetch(int, leftChild->matchelement_top, i);
777        result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch));
778        array_insert_last(mdd_t *, mddArray_top, result);
779      }
780    }
781    /* Now attach the array to the ctlFormula */
782    ctlFormula->Bottomstates = mddArray_bot;
783    ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot);
784    ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot);
785    ctlFormula->Topstates = mddArray_top;
786    ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top);
787    ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top);
788    /* find out the leaves attached to this nodes.*/
789    leavesLeftArray = leftChild->leaves;
790    ctlFormula->leaves = array_dup(leavesLeftArray);   
791    break;
792  }
793  case Ctlp_AND_c:{
794    int number_right_bot = array_n(rightChild->Bottomstates);
795    int number_right_top = array_n(rightChild->Topstates);
796    int number_left_bot = array_n(leftChild->Bottomstates);
797    int number_left_top = array_n(leftChild->Topstates);
798    int i,positionmatch;
799    leavesArray = array_alloc(Ctlp_Formula_t *, 0);
800    matchfound_top = array_alloc(boolean, 0);
801    matchfound_bot = array_alloc(boolean, 0);
802    matchelement_top = array_alloc(int, 0);
803    matchelement_bot = array_alloc(int, 0);
804    /* And operation*/
805    /* for bottom sets */
806    rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
807    arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
808      if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){
809        result = mdd_and(leftMdd, rightMdd, 1, 1);
810        array_insert_last(mdd_t *, mddArray_bot, result);
811      }
812      else{
813        positionmatch = array_fetch(int,leftChild->matchelement_bot, i);
814        result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch));
815        array_insert_last(mdd_t *, mddArray_bot, result);
816      }
817    }
818    leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
819    for(i=1;i<number_right_bot;i++){
820      if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){
821        rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
822        result = mdd_and(leftMdd, rightMdd, 1, 1);
823        array_insert_last(mdd_t *, mddArray_bot, result);
824      }
825      else{
826        positionmatch = array_fetch(int,rightChild->matchelement_bot, i);
827        result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch + number_left_bot - 1)));
828        array_insert_last(mdd_t *, mddArray_bot, result);
829      }
830    }
831    match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
832
833    /* for top sets */
834    rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
835    arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
836      if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){
837        result = mdd_and(leftMdd, rightMdd, 1, 1);
838        array_insert_last(mdd_t *, mddArray_top, result);
839      }
840      else{
841        positionmatch = array_fetch(int,leftChild->matchelement_top, i);
842        result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch));
843        array_insert_last(mdd_t *, mddArray_top, result);
844      }
845    }
846    leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
847    for(i=1;i<number_right_top;i++){
848      if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){
849        rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
850        result = mdd_and(leftMdd, rightMdd, 1, 1);
851        array_insert_last(mdd_t *, mddArray_top, result);
852      }
853      else{
854        positionmatch = array_fetch(int,rightChild->matchelement_top, i);
855        result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch + number_left_top - 1)));
856        array_insert_last(mdd_t *, mddArray_top, result);
857      }
858    }
859    match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
860    /* Now attach the array to the ctlFormula */
861    ctlFormula->Bottomstates = mddArray_bot;
862    ctlFormula->Topstates = mddArray_top;
863    /* find out the leaves attached to this nodes.*/   
864    leavesLeftArray = leftChild->leaves;
865    leavesRightArray = rightChild->leaves;   
866    array_append(leavesArray,leavesLeftArray);
867    array_append(leavesArray,leavesRightArray);
868    ctlFormula->leaves = leavesArray;
869    break;
870  }
871  /* Use of EQ, XOR, THEN, OR is discouraged.    Please use convert
872     formula to simple existential form. */
873  case Ctlp_EQ_c :{
874    int number_right_bot = array_n(rightChild->Bottomstates);
875    int number_right_top = array_n(rightChild->Topstates);
876    int number_left_bot  = array_n(leftChild->Bottomstates);
877    int number_left_top  = array_n(leftChild->Topstates);
878    int i,positionmatch;
879    leavesArray = array_alloc(Ctlp_Formula_t *, 0);
880    matchfound_top = array_alloc(boolean, 0);
881    matchfound_bot = array_alloc(boolean, 0);
882    matchelement_top = array_alloc(int, 0);
883    matchelement_bot = array_alloc(int, 0);
884    /* for bottom sets */
885    rightMdd= array_fetch(mdd_t *,rightChild->Bottomstates,0);
886    arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
887      if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){
888        result = mdd_xnor(leftMdd,rightMdd);
889        array_insert_last(mdd_t *, mddArray_bot, result);
890      }
891      else{
892        positionmatch = array_fetch(int,leftChild->matchelement_bot, i);
893        result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch));
894        array_insert_last(mdd_t *, mddArray_bot, result);
895      }
896    }
897    leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
898    for(i=1;i<number_right_bot;i++){
899      if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){
900        rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
901        result = mdd_xnor(leftMdd,rightMdd );
902        array_insert_last(mdd_t *, mddArray_bot, result);
903      }
904      else{
905        positionmatch = array_fetch(int,rightChild->matchelement_bot, i);
906        result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch+ number_left_bot - 1)));
907        array_insert_last(mdd_t *, mddArray_bot, result);
908      }
909    }
910    match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
911
912    /* for top sets */
913    rightMdd= array_fetch(mdd_t *,rightChild->Topstates,0);
914    arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
915      if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){
916        result = mdd_xnor(leftMdd,rightMdd);
917        array_insert_last(mdd_t *, mddArray_top, result);
918      }
919      else{
920        positionmatch = array_fetch(int,leftChild->matchelement_top, i);
921        result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch));
922        array_insert_last(mdd_t *, mddArray_top, result);
923      }
924    }
925    leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
926    for(i=1;i<number_right_top;i++){
927      if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){
928        rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
929        result = mdd_xnor(leftMdd,rightMdd );
930        array_insert_last(mdd_t *, mddArray_top, result);
931      }
932      else{
933        positionmatch = array_fetch(int,rightChild->matchelement_top, i);
934        result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch+ number_left_top - 1)));
935        array_insert_last(mdd_t *, mddArray_top, result);
936      }
937    }
938    match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
939
940    /* Now attach the array to the ctlFormula */
941    ctlFormula->Bottomstates = mddArray_bot;
942    ctlFormula->Topstates = mddArray_top;
943    /* find out the leaves attached to this nodes.*/   
944    leavesLeftArray = leftChild->leaves;
945    leavesRightArray = rightChild->leaves;   
946    array_append(leavesArray,leavesLeftArray);
947    array_append(leavesArray,leavesRightArray);
948    ctlFormula->leaves = leavesArray;
949    break;
950  }
951  case Ctlp_XOR_c :{
952    int number_right_bot = array_n(rightChild->Bottomstates);
953    int number_right_top = array_n(rightChild->Topstates);
954    int number_left_bot  = array_n(leftChild->Bottomstates);
955    int number_left_top  = array_n(leftChild->Topstates);
956    int i,positionmatch;
957    leavesArray = array_alloc(Ctlp_Formula_t *, 0);
958    matchfound_top = array_alloc(boolean, 0);
959    matchfound_bot = array_alloc(boolean, 0);
960    matchelement_top = array_alloc(int, 0);
961    matchelement_bot = array_alloc(int, 0);
962    /* for bottom sets */
963    rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
964    arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
965      if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){
966        result = mdd_xor(leftMdd,rightMdd);
967        array_insert_last(mdd_t *, mddArray_bot, result);
968      }
969      else{
970        positionmatch = array_fetch(int,leftChild->matchelement_bot, i);
971        result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch));
972        array_insert_last(mdd_t *, mddArray_bot, result);
973      }
974    }
975    leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
976    for(i=1;i<number_right_bot;i++){
977      if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){
978        rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
979        result = mdd_xor(leftMdd,rightMdd );
980        array_insert_last(mdd_t *, mddArray_bot, result);
981      }
982      else{
983        positionmatch = array_fetch(int,rightChild->matchelement_bot, i);
984        result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch+ number_left_bot - 1)));
985        array_insert_last(mdd_t *, mddArray_bot, result);
986      }
987    }
988    match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
989
990    /* for top sets */
991    rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
992    arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
993      if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){
994        result = mdd_xor(leftMdd,rightMdd);
995        array_insert_last(mdd_t *, mddArray_top, result);
996      }
997      else{
998        positionmatch = array_fetch(int,leftChild->matchelement_top, i);
999        result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch));
1000        array_insert_last(mdd_t *, mddArray_top, result);
1001      }
1002    }
1003    leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
1004    for(i=1;i<number_right_top;i++){
1005      if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){
1006        rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
1007        result = mdd_xor(leftMdd,rightMdd );
1008        array_insert_last(mdd_t *, mddArray_top, result);
1009      }
1010      else{
1011        positionmatch = array_fetch(int,rightChild->matchelement_top, i);
1012        result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch + number_left_top - 1)));
1013        array_insert_last(mdd_t *, mddArray_top, result);
1014      }
1015    }
1016    match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
1017
1018    /* Now attach the array to the ctlFormula */
1019    ctlFormula->Bottomstates = mddArray_bot;
1020    ctlFormula->Topstates = mddArray_top;
1021    /* find out the leaves attached to this nodes.*/   
1022    leavesLeftArray = leftChild->leaves;
1023    leavesRightArray = rightChild->leaves;   
1024    array_append(leavesArray,leavesLeftArray);
1025    array_append(leavesArray,leavesRightArray);
1026    ctlFormula->leaves = leavesArray;
1027    break;
1028  }
1029
1030  case Ctlp_THEN_c :{
1031    int number_right_bot = array_n(rightChild->Bottomstates);
1032    int number_right_top = array_n(rightChild->Topstates);
1033    int number_left_bot = array_n(leftChild->Bottomstates);
1034    int number_left_top = array_n(leftChild->Topstates);
1035    int i,positionmatch;
1036    leavesArray = array_alloc(Ctlp_Formula_t *, 0);
1037    matchfound_top = array_alloc(boolean, 0);
1038    matchfound_bot = array_alloc(boolean, 0);
1039    matchelement_top = array_alloc(int, 0);
1040    matchelement_bot = array_alloc(int, 0);
1041    /* bottom sets */
1042    rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
1043    arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
1044      if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){
1045        result = mdd_or(leftMdd ,rightMdd,0,1);
1046        array_insert_last(mdd_t *, mddArray_bot, result);
1047      }
1048      else{
1049        positionmatch = array_fetch(int,leftChild->matchelement_bot, i);
1050        result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch));
1051        array_insert_last(mdd_t *, mddArray_bot, result);
1052      }
1053    }
1054
1055    leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
1056    for(i=1;i<number_right_bot;i++){
1057      if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){
1058      rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
1059      result = mdd_or(leftMdd,rightMdd ,0,1);
1060      array_insert_last(mdd_t *, mddArray_bot, result);
1061    }
1062      else{
1063        positionmatch = array_fetch(int,rightChild->matchelement_bot, i);
1064        result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, (positionmatch + number_left_bot - 1)));
1065        array_insert_last(mdd_t *, mddArray_bot, result);
1066      }
1067    }
1068    match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
1069    /* top sets */
1070    rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
1071    arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
1072      if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){
1073        result = mdd_or(leftMdd ,rightMdd,0,1);
1074        array_insert_last(mdd_t *, mddArray_top, result);
1075      }
1076      else{
1077        positionmatch = array_fetch(int,leftChild->matchelement_top, i);
1078        result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch));
1079        array_insert_last(mdd_t *, mddArray_top, result);
1080      }
1081    }
1082    leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
1083    for(i=1;i<number_right_top;i++){
1084      if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){
1085      rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
1086      result = mdd_or(leftMdd,rightMdd ,0,1);
1087      array_insert_last(mdd_t *, mddArray_top, result);
1088    }
1089      else{
1090        positionmatch = array_fetch(int,rightChild->matchelement_top, i);
1091        result = mdd_dup(array_fetch(mdd_t *, mddArray_top, (positionmatch + number_left_top - 1)));
1092        array_insert_last(mdd_t *, mddArray_top, result);
1093      }
1094    }
1095    match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
1096   
1097    /* Now attach the array to the ctlFormula */
1098    ctlFormula->Bottomstates = mddArray_bot;
1099    ctlFormula->Topstates = mddArray_top;
1100    /* find out the leaves attached to this nodes.*/   
1101    leavesLeftArray = leftChild->leaves;
1102    leavesRightArray = rightChild->leaves;   
1103    array_append(leavesArray,leavesLeftArray);
1104    array_append(leavesArray,leavesRightArray);
1105    ctlFormula->leaves = leavesArray;
1106    break;
1107  }
1108  case Ctlp_OR_c:{
1109    int number_right_bot = array_n(rightChild->Bottomstates);
1110    int number_right_top = array_n(rightChild->Topstates);
1111    int number_left_bot = array_n(leftChild->Bottomstates);
1112    int number_left_top = array_n(leftChild->Topstates);
1113    int i,positionmatch;
1114    leavesArray = array_alloc(Ctlp_Formula_t *, 0);
1115    matchfound_top = array_alloc(boolean, 0);
1116    matchfound_bot = array_alloc(boolean, 0);
1117    matchelement_top = array_alloc(int, 0);
1118    matchelement_bot = array_alloc(int, 0);
1119
1120    /* OR operation*/
1121    /* bottom sets */
1122    rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
1123    arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
1124      if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){
1125        result = mdd_or(leftMdd,rightMdd,1,1);
1126        array_insert_last(mdd_t *, mddArray_bot, result);
1127      }
1128      else{
1129        positionmatch = array_fetch(int,leftChild->matchelement_bot, i);
1130        result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch));
1131        array_insert_last(mdd_t *, mddArray_bot, result);
1132      }
1133    }
1134
1135    leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
1136    for(i=1;i<number_right_bot;i++){
1137      if ((array_fetch(boolean,rightChild->matchfound_bot,i) == FALSE)){
1138      rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
1139      result = mdd_or(leftMdd,rightMdd ,1,1);
1140      array_insert_last(mdd_t *, mddArray_bot, result);
1141      }
1142      else{
1143        positionmatch = array_fetch(int,rightChild->matchelement_bot, i);
1144        result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, (positionmatch + number_left_bot - 1)));
1145        array_insert_last(mdd_t *, mddArray_bot, result);
1146      }
1147    }
1148
1149    match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
1150
1151    /* top sets */
1152    rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
1153    arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
1154      if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){
1155        result = mdd_or(leftMdd,rightMdd,1,1);
1156        array_insert_last(mdd_t *, mddArray_top, result);
1157      }
1158      else{
1159        positionmatch = array_fetch(int,leftChild->matchelement_top, i);
1160        result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch));
1161        array_insert_last(mdd_t *, mddArray_top, result);
1162      }
1163    }
1164
1165    leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
1166    for(i=1;i<number_right_top;i++){
1167      if ((array_fetch(boolean,rightChild->matchfound_top,i) == FALSE)){
1168      rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
1169      result = mdd_or(leftMdd,rightMdd ,1,1);
1170      array_insert_last(mdd_t *, mddArray_top, result);
1171      }
1172      else{
1173        positionmatch = array_fetch(int,rightChild->matchelement_top, i);
1174        result = mdd_dup(array_fetch(mdd_t *, mddArray_top, (positionmatch + number_left_top - 1)));
1175        array_insert_last(mdd_t *, mddArray_top, result);
1176      }
1177    }
1178
1179    match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
1180    /* Now attach the array to the ctlFormula */
1181    ctlFormula->Topstates = mddArray_top;
1182    ctlFormula->Bottomstates = mddArray_bot;
1183    /* ctlFormula->states = array_fetch(mdd_t *, mddArray, 0); */
1184    /* find out the leaves attached to this nodes.*/   
1185    leavesLeftArray = leftChild->leaves;
1186    leavesRightArray = rightChild->leaves;   
1187    array_append(leavesArray,leavesLeftArray);
1188    array_append(leavesArray,leavesRightArray);
1189    ctlFormula->leaves = leavesArray;
1190    break;
1191  }
1192  case Ctlp_EX_c:{
1193    int i,positionmatch;
1194    if (ctlFormula->negation_parity == Ctlp_Even_c) {
1195      /* bottom sets shoud be computed first i.e underapproximations */
1196      arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
1197        if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){
1198          result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
1199                                           careStatesArray, verbosity, dcLevel);
1200          array_insert_last(mdd_t *, mddArray_bot, result);
1201        }
1202        else{
1203          positionmatch =  array_fetch(int, leftChild->matchelement_bot, i);
1204          result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch));
1205          array_insert_last(mdd_t *, mddArray_bot, result);
1206        }
1207      }
1208      result = array_fetch(mdd_t *, mddArray_bot, 0); /* exact set */
1209    }
1210    else{
1211      /* top sets should be computed first i.e., underapproximations */
1212      arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
1213        if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){
1214          result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
1215                                           careStatesArray, verbosity, dcLevel);
1216          array_insert_last(mdd_t *, mddArray_top, result);
1217        }
1218        else{
1219          positionmatch =  array_fetch(int, leftChild->matchelement_top, i);
1220          result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch));
1221          array_insert_last(mdd_t *, mddArray_top, result);
1222        }
1223      }
1224      result = array_fetch(mdd_t *, mddArray_top, 0); /* exact set */
1225    }
1226    if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)){
1227      if (ctlFormula->negation_parity == Ctlp_Even_c) {
1228        ctlFormula->Bottomstates = mddArray_bot;
1229        arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
1230          array_insert_last(mdd_t *, mddArray_top, mdd_dup(result));
1231        }
1232        ctlFormula->Topstates = mddArray_top;
1233        ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot);
1234        ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot);
1235        matchfound_top = array_alloc(boolean, 0);
1236        matchelement_top = array_alloc(int, 0);
1237        match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
1238      }
1239      else{
1240        ctlFormula->Topstates = mddArray_top;
1241        arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
1242          array_insert_last(mdd_t *, mddArray_bot, mdd_dup(result));
1243        }
1244        ctlFormula->Bottomstates = mddArray_bot;
1245        ctlFormula->matchfound_top = array_dup(leftChild->matchfound_bot);
1246        ctlFormula->matchelement_top = array_dup(leftChild->matchelement_bot);
1247        matchfound_bot = array_alloc(int, 0);
1248        matchelement_bot = array_alloc(int, 0);
1249        match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
1250      }
1251      /* find out the leaves attached to this nodes.*/
1252      leavesLeftArray = leftChild->leaves;
1253      ctlFormula->leaves = array_dup(leavesLeftArray);   
1254      break;
1255    }
1256    if (ctlFormula->negation_parity == Ctlp_Even_c) {
1257      /* top sets */
1258      arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) {
1259        if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){
1260          result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
1261                                           careStatesArray, verbosity, dcLevel);
1262          array_insert_last(mdd_t *, mddArray_top, result);
1263        }
1264        else{
1265          positionmatch =  array_fetch(int, leftChild->matchelement_top, i);
1266          result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch));
1267          array_insert_last(mdd_t *, mddArray_top, result);
1268        }
1269
1270      }
1271    }
1272    else {
1273      arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) {
1274        if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){
1275          result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates,
1276                                           careStatesArray, verbosity, dcLevel);
1277          array_insert_last(mdd_t *, mddArray_bot, result);
1278        }
1279        else{
1280          positionmatch =  array_fetch(int, leftChild->matchelement_bot, i);
1281          result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch));
1282          array_insert_last(mdd_t *, mddArray_bot, result);
1283        }
1284
1285      }
1286    }
1287    /* Now attach the array to the ctlFormula */
1288    ctlFormula->Bottomstates = mddArray_bot;
1289    ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot);
1290    ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot);
1291    ctlFormula->Topstates = mddArray_top;
1292    ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top);
1293    ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top);
1294    /* find out the leaves attached to this nodes.*/
1295    leavesLeftArray = leftChild->leaves;
1296    ctlFormula->leaves = array_dup(leavesLeftArray);   
1297    break;
1298    }
1299
1300  case Ctlp_EU_c:{
1301    array_t *onionRings = NIL(array_t);
1302    array_t *MergeOnionRings = NIL(array_t);
1303    array_t *ExactOnionRings = NIL(array_t);
1304    array_t *NewOnionRings = NIL(array_t); /* array of mdd_t */
1305    boolean fixpoint;
1306    int number_left_bot = array_n(leftChild->Bottomstates);
1307    int number_right_bot = array_n(rightChild->Bottomstates);
1308    int number_left_top = array_n(leftChild->Topstates);
1309    int number_right_top = array_n(rightChild->Topstates);
1310    int i;
1311    int j = 1;
1312    mdd_t *approx_under = NIL(mdd_t);
1313    array_t *botrings = NIL(array_t);
1314    array_t *toprings = NIL(array_t);
1315    leavesArray = array_alloc(Ctlp_Formula_t *, 0);
1316    matchfound_top = array_alloc(boolean, 0);
1317    matchfound_bot = array_alloc(boolean, 0);
1318    matchelement_top = array_alloc(int, 0);
1319    matchelement_bot = array_alloc(int, 0);
1320    approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Underapprox_c );
1321    onionRings = NIL(array_t);
1322    if (buildOnionRings) {
1323      MergeOnionRings = array_alloc(mdd_t *, 0);
1324      botrings = array_alloc(array_t*,0);
1325      toprings = array_alloc(array_t*,0);
1326    }
1327    if (ctlFormula->negation_parity == Ctlp_Even_c) {
1328      rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
1329      result_underapprox = mdd_zero(mddMgr);
1330      /* Compute the bottom mdds first which provide the underapproximation
1331       * to the exact set*/
1332      for(i=1;i<number_left_bot;i++) {
1333        if (buildOnionRings)
1334          onionRings = array_alloc(mdd_t *, 0);
1335        leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i);
1336        result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
1337                                         rightMdd,
1338                                         approx, fairStates,
1339                                         careStatesArray,
1340                                         earlyTermination, hintsArray,
1341                                         hintType, onionRings,
1342                                         verbosity, dcLevel, &fixpoint);
1343        array_insert(mdd_t *, mddArray_bot, j, result);
1344        if (buildOnionRings) {
1345          if(i==1) {
1346            mdd_array_free(MergeOnionRings);
1347            MergeOnionRings = mdd_array_duplicate(onionRings);
1348            /* saving the bottom computation onion rings */
1349            array_insert(array_t*,botrings,j,onionRings);
1350          }
1351          else {
1352            MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings);
1353            /* saving the bottom computation onion rings */
1354            array_insert(array_t*,botrings,j,onionRings);
1355          }
1356        }
1357        j++;
1358        result_new = mdd_or(result,result_underapprox,1,1);
1359        mdd_free(result_underapprox);
1360        result_underapprox = result_new;
1361      }
1362      leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
1363      for(i=1;i<number_right_bot;i++) {
1364        if (buildOnionRings)
1365          onionRings = array_alloc(mdd_t *, 0);
1366        rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
1367        result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd,
1368                                         rightMdd,
1369                                         approx, fairStates,
1370                                         careStatesArray,
1371                                         earlyTermination, hintsArray,
1372                                         hintType, onionRings,
1373                                         verbosity, dcLevel, &fixpoint);
1374        array_insert(mdd_t *, mddArray_bot, j, result);
1375        if (buildOnionRings) {
1376          if(i==1) {
1377            mdd_array_free(MergeOnionRings);
1378            MergeOnionRings = mdd_array_duplicate(onionRings);
1379            /* saving the bottom computation onion rings */
1380            array_insert(array_t*,botrings,j,onionRings);
1381          }
1382          else {
1383            MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings);
1384            /* saving the bottom computation onion rings */
1385            array_insert(array_t*,botrings,j,onionRings);
1386          }
1387        }
1388        j++;
1389        result_new = mdd_or(result,result_underapprox,1,1);
1390        mdd_free(result_underapprox);
1391        result_underapprox = result_new;
1392      }
1393      /* Use the under approximations to calculate the exact set. */
1394      if (approx != NIL(mdd_t)) {
1395        mdd_t *tmp = mdd_or(result_underapprox,approx,1,1);
1396        mdd_free(approx);
1397        mdd_free(result_underapprox);
1398        approx = tmp;
1399      } else {
1400        approx = result_underapprox; 
1401      }
1402      if (buildOnionRings) {
1403        onionRings = array_alloc(mdd_t *, 0);
1404      }
1405      rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0);
1406      leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
1407      result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
1408                                       rightMdd,
1409                                       approx, fairStates,
1410                                       careStatesArray,
1411                                       earlyTermination, hintsArray,
1412                                       hintType, onionRings,
1413                                       verbosity, dcLevel, &fixpoint);
1414      array_insert(mdd_t *, mddArray_bot, 0, mdd_dup(result));
1415      array_insert(mdd_t *, mddArray_top, 0, result);
1416      if (buildOnionRings) {
1417        MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings);
1418        mdd_array_free(onionRings);
1419        Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) MergeOnionRings,
1420                               McFormulaFreeDebugData);
1421        array_insert(array_t *,botrings,0,mdd_array_duplicate(MergeOnionRings));
1422        array_insert(array_t *,toprings,0,mdd_array_duplicate(MergeOnionRings));
1423      }
1424      result = array_fetch(mdd_t *,mddArray_bot,0);
1425      if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)) {
1426        leavesLeftArray = leftChild->leaves;
1427        array_append(leavesArray,leavesLeftArray);
1428        leavesRightArray = rightChild->leaves;
1429        array_append(leavesArray,leavesRightArray);
1430        ctlFormula->leaves = leavesArray;
1431        j=1;
1432        for(i=1;i<number_left_top;i++) {
1433          array_insert(mdd_t *, mddArray_top, j, mdd_dup(result));
1434          if (buildOnionRings) {
1435            array_insert(array_t *,toprings,j,
1436                         mdd_array_duplicate(MergeOnionRings));
1437          }
1438          j++;
1439        } 
1440        for(i=1;i<number_right_top;i++) {
1441          array_insert(mdd_t *, mddArray_top, j, mdd_dup(result));
1442          if (buildOnionRings){
1443            array_insert(array_t *,toprings,j,
1444                         mdd_array_duplicate(MergeOnionRings));
1445          }
1446          j++;
1447      }
1448        ctlFormula->Bottomstates = mddArray_bot;
1449        ctlFormula->Topstates = mddArray_top;
1450        match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
1451        match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
1452        if (buildOnionRings) {
1453          ctlFormula->BotOnionRings = botrings;
1454          ctlFormula->TopOnionRings = toprings;
1455        }
1456        mdd_free(approx);
1457        break; /* bottom failing */
1458      }
1459      /* top sets
1460       * we can use the exact set as an approximation to compute the top
1461       * set. */
1462      rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
1463      j=1;
1464      if (buildOnionRings) 
1465        ExactOnionRings = mdd_array_duplicate(MergeOnionRings);
1466      /* Compute the Top mdds now */
1467      for(i=1;i<number_left_top;i++) {
1468        if (buildOnionRings)
1469          onionRings = array_alloc(mdd_t *, 0);
1470        leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i);
1471        approx_under = array_fetch(mdd_t *,mddArray_bot,0);
1472        result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
1473                                         rightMdd,
1474                                         approx_under, fairStates,
1475                                         careStatesArray,
1476                                         earlyTermination, hintsArray,
1477                                         hintType, onionRings,
1478                                         verbosity, dcLevel, &fixpoint);
1479        array_insert(mdd_t *, mddArray_top, j, result);
1480        if (buildOnionRings) {
1481          array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings);
1482          NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings);
1483          /* saving the bottom computation onion rings */
1484          array_insert(array_t*,toprings,j,NewOnionRings);
1485          mdd_array_free(onionRings);
1486        }
1487        j++;
1488      }
1489      leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
1490      for(i=1;i<number_right_top;i++) {
1491        if (buildOnionRings)
1492          onionRings = array_alloc(mdd_t *, 0);
1493        rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
1494        approx_under = array_fetch(mdd_t *,mddArray_top,0);
1495        result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd,
1496                                         rightMdd,
1497                                         approx_under, fairStates,
1498                                         careStatesArray,
1499                                         earlyTermination, hintsArray,
1500                                         hintType, onionRings,
1501                                         verbosity, dcLevel, &fixpoint);
1502        array_insert(mdd_t *, mddArray_top, j, result);
1503        if (buildOnionRings) {
1504          array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings);
1505          NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings);
1506          /* saving the bottom computation onion rings */
1507          array_insert(array_t*,toprings,j,NewOnionRings);
1508          mdd_array_free(onionRings);
1509        }
1510        j++;
1511      }
1512    }
1513    else {
1514      /* The negation parity is odd. So the top sets will provide
1515         underapproximations now. */
1516      rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
1517      result_underapprox = mdd_zero(mddMgr);
1518      /* Compute the top mdds first */
1519      for(i=1;i<number_left_top;i++) {
1520        if (buildOnionRings)
1521          onionRings = array_alloc(mdd_t *, 0);
1522        leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i);
1523        result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
1524                                         rightMdd,
1525                                         NIL(mdd_t), fairStates,
1526                                         careStatesArray,
1527                                         earlyTermination, hintsArray,
1528                                         hintType, onionRings,
1529                                         verbosity, dcLevel, &fixpoint);
1530        array_insert(mdd_t *, mddArray_top, j, result);
1531        if (buildOnionRings){
1532          if(i==1){
1533            mdd_array_free(MergeOnionRings);
1534            MergeOnionRings = mdd_array_duplicate(onionRings);
1535            array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */
1536          }
1537          else {
1538            array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */
1539            MergeOnionRings=GenerateOnionRings(MergeOnionRings,onionRings);
1540          }
1541        }
1542        j++;
1543        result_new = mdd_or(result,result_underapprox,1,1);
1544        mdd_free(result_underapprox);
1545        result_underapprox = result_new;
1546      }
1547      leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
1548      for(i=1;i<number_right_top;i++) {
1549        if (buildOnionRings)
1550          onionRings = array_alloc(mdd_t *, 0);
1551        rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i);
1552        result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd,
1553                                         rightMdd,
1554                                         NIL(mdd_t), fairStates,
1555                                         careStatesArray,
1556                                         earlyTermination, hintsArray,
1557                                         hintType, onionRings,
1558                                         verbosity, dcLevel, &fixpoint);
1559        array_insert(mdd_t *, mddArray_top, j, result);
1560        if (buildOnionRings) {
1561          if(j==1){
1562            mdd_array_free(MergeOnionRings);
1563            MergeOnionRings = mdd_array_duplicate(onionRings);
1564            array_insert(array_t*,toprings,j,onionRings); /* saving the top computation onion rings */
1565          }
1566          else {
1567            MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings);
1568            array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */
1569          }
1570        }
1571        j++;
1572        result_new = mdd_or(result,result_underapprox,1,1);
1573        mdd_free(result_underapprox);
1574        result_underapprox = result_new;
1575      }
1576      /* Use the under approximations to calculate the exact set. */
1577      if (approx != NIL(mdd_t)) {
1578        mdd_t *tmp = mdd_or(result_underapprox,approx,1,1);
1579        mdd_free(approx);
1580        mdd_free(result_underapprox);
1581        approx = tmp;
1582      } else {
1583        approx = result_underapprox; 
1584      }
1585      if (buildOnionRings) {
1586        onionRings = array_alloc(mdd_t *, 0);
1587      }
1588      /* exact set computation */
1589      rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
1590      leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
1591      result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
1592                                       rightMdd,
1593                                       approx, fairStates,
1594                                       careStatesArray,
1595                                       earlyTermination, hintsArray,
1596                                       hintType, onionRings,
1597                                       verbosity, dcLevel, &fixpoint);
1598      array_insert(mdd_t *, mddArray_bot, 0, mdd_dup(result));
1599      array_insert(mdd_t *, mddArray_top, 0, result);
1600      if (buildOnionRings) {
1601        MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings);
1602        mdd_array_free(onionRings);
1603        Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) MergeOnionRings,
1604                               McFormulaFreeDebugData);
1605        array_insert(array_t *,botrings,0,
1606                     mdd_array_duplicate(MergeOnionRings));
1607        array_insert(array_t *,toprings,0,
1608                     mdd_array_duplicate(MergeOnionRings));
1609      }
1610      result = array_fetch(mdd_t *,mddArray_bot,0);
1611      if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)) {
1612        leavesLeftArray = leftChild->leaves;
1613        array_append(leavesArray,leavesLeftArray);
1614        leavesRightArray = rightChild->leaves;
1615        array_append(leavesArray,leavesRightArray);
1616        ctlFormula->leaves = leavesArray;
1617        j=1;
1618        for(i=1;i<number_left_bot;i++) {
1619          array_insert(mdd_t *, mddArray_bot, j, mdd_dup(result));
1620          if (buildOnionRings){
1621            array_insert(array_t *,botrings,j,
1622                         mdd_array_duplicate(MergeOnionRings));
1623          }
1624          j++;
1625        } 
1626        for(i=1;i<number_right_bot;i++) {
1627          array_insert(mdd_t *, mddArray_bot, j, mdd_dup(result));
1628          if (buildOnionRings){
1629            array_insert(array_t *,botrings,j,
1630                         mdd_array_duplicate(MergeOnionRings));
1631          }
1632          j++;
1633        }
1634        match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
1635        match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
1636        ctlFormula->Bottomstates = mddArray_bot;
1637        ctlFormula->Topstates = mddArray_top;
1638        if (buildOnionRings){
1639          ctlFormula->BotOnionRings = botrings;
1640          ctlFormula->TopOnionRings = toprings;
1641        }
1642        assert(approx != NIL(mdd_t));
1643        mdd_free(approx);
1644        break; /* bottom failing */
1645      }
1646      if (buildOnionRings) 
1647        ExactOnionRings = mdd_array_duplicate(MergeOnionRings);
1648      /* we can use the exact set as an approximation to compute
1649         the bottom set. */
1650      rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0);
1651      j=1;
1652      /* Compute the botom mdds now */
1653      for(i=1;i<number_left_bot;i++) {
1654        if (buildOnionRings)
1655          onionRings = array_alloc(mdd_t *, 0);
1656        leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i);
1657        approx_under = array_fetch(mdd_t *,mddArray_bot,0);
1658        result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd,
1659                                         rightMdd,
1660                                         approx_under, fairStates,
1661                                         careStatesArray,
1662                                         earlyTermination, hintsArray,
1663                                         hintType, onionRings,
1664                                         verbosity, dcLevel, &fixpoint);
1665        array_insert(mdd_t *, mddArray_bot, j, result);
1666        if (buildOnionRings){
1667          array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings);
1668          NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings);
1669          /* saving the bottom computation onion rings */
1670          array_insert(array_t*,botrings,j,NewOnionRings);
1671          mdd_array_free(onionRings);
1672        }
1673        j++;
1674      } 
1675      leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0);
1676      for(i=1;i<number_right_bot;i++) {
1677        if (buildOnionRings)
1678          onionRings = array_alloc(mdd_t *, 0);
1679        else
1680          onionRings = NIL(array_t);
1681        rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i);
1682        approx_under = array_fetch(mdd_t *,mddArray_bot,0);
1683        result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd,
1684                                         rightMdd,
1685                                         NIL(mdd_t), fairStates,
1686                                         careStatesArray,
1687                                         earlyTermination, hintsArray,
1688                                         hintType, onionRings,
1689                                         verbosity, dcLevel, &fixpoint);
1690        array_insert(mdd_t *, mddArray_bot, j, result);
1691        if (buildOnionRings) {
1692          array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings);
1693          NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings);
1694          array_insert(array_t*,botrings,j,NewOnionRings);
1695          mdd_array_free(onionRings);
1696        }
1697        j++;
1698      }
1699    }
1700    match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
1701    match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
1702    ctlFormula->Bottomstates = mddArray_bot;
1703    ctlFormula->Topstates = mddArray_top;
1704    leavesLeftArray = leftChild->leaves;
1705    array_append(leavesArray,leavesLeftArray);
1706    leavesRightArray = rightChild->leaves;
1707    array_append(leavesArray,leavesRightArray);
1708    ctlFormula->leaves = leavesArray;
1709    if (buildOnionRings) {
1710      ctlFormula->BotOnionRings = botrings;
1711      ctlFormula->TopOnionRings = toprings;
1712      mdd_array_free(ExactOnionRings);
1713    }
1714    if(approx != NIL(mdd_t))
1715      mdd_free(approx);   
1716    /* Can't combine under and overapprox */
1717    if(!fixpoint && TRMinimization == Ctlp_Overapprox_c)
1718      TRMinimization = Ctlp_Incomparable_c;
1719    break;
1720  }
1721
1722  case Ctlp_EG_c:{
1723    boolean fixpoint;
1724    mdd_t *result_ub;
1725    mdd_t *approx_over = NIL(mdd_t)    ;
1726    int number_bot = array_n(leftChild->Bottomstates);
1727    int number_top = array_n(leftChild->Topstates);
1728    int i;
1729    array_t *arrayOfOnionRings = NIL(array_t); /* array of array of mdd_t* */
1730    array_t *botrings = NIL(array_t);
1731    array_t *toprings = NIL(array_t);
1732    matchfound_top = array_alloc(boolean, 0);
1733    matchfound_bot = array_alloc(boolean, 0);
1734    matchelement_top = array_alloc(int, 0);
1735    matchelement_bot = array_alloc(int, 0);
1736    approx = Ctlp_FormulaObtainApproxStates(ctlFormula, Ctlp_Overapprox_c);
1737    if(buildOnionRings) {
1738      botrings = array_alloc(array_t*,0);
1739      toprings = array_alloc(array_t*,0);
1740    }
1741    if (approx == NIL(mdd_t)) {
1742      result_ub = mdd_one(mddMgr);
1743    } else {
1744      result_ub = mdd_dup(approx);
1745    }
1746    if (ctlFormula->negation_parity == Ctlp_Even_c) {
1747      /* compute the top sets first which will give us
1748         overapproximation to the exact set */
1749      for(i=1;i<number_top;i++) {
1750        if(buildOnionRings) 
1751          arrayOfOnionRings = array_alloc(array_t *, 0);
1752        leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i);
1753        result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
1754                                         NIL(mdd_t), fairStates, 
1755                                         fairCondition, careStatesArray,
1756                                         earlyTermination, hintsArray,
1757                                         hintType, 
1758                                         &arrayOfOnionRings, verbosity,
1759                                         dcLevel, &fixpoint, GSHschedule);
1760        array_insert(mdd_t *, mddArray_top, i, result);
1761        if(buildOnionRings) {
1762          array_insert(array_t*,toprings,i,arrayOfOnionRings);
1763        }
1764        result_new =  mdd_and(result_ub,result,1,1);
1765        mdd_free(result_ub);
1766        result_ub = result_new;
1767      }
1768      /* calculate the exact set */
1769      if(buildOnionRings)
1770        arrayOfOnionRings = array_alloc(array_t *, 0);
1771      leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
1772      result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
1773                                       NIL(mdd_t), fairStates,
1774                                       fairCondition, careStatesArray,
1775                                       earlyTermination, hintsArray,
1776                                       hintType,
1777                                       &arrayOfOnionRings, verbosity,
1778                                       dcLevel, &fixpoint, GSHschedule);
1779      array_insert(mdd_t *,mddArray_bot,0,mdd_dup(result));
1780      array_insert(mdd_t *,mddArray_top,0,mdd_dup(result));
1781      mdd_free(result);
1782      if(buildOnionRings) {
1783        Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
1784                               McFormulaFreeDebugData);
1785        array_insert(array_t*,toprings,0,McMddArrayArrayDup(arrayOfOnionRings));
1786        array_insert(array_t*,botrings,0,McMddArrayArrayDup(arrayOfOnionRings));
1787      }
1788      result = array_fetch(mdd_t *,mddArray_bot,0);
1789      if (McCheckEarlyTerminationForOverapprox(earlyTermination, result, careStatesArray)) {
1790        leavesLeftArray = leftChild->leaves;
1791        ctlFormula->leaves = array_dup(leavesLeftArray);
1792        for(i=1;i<number_bot;i++) {
1793          array_insert(mdd_t *, mddArray_bot, i, mdd_dup(result));
1794          if(buildOnionRings) {
1795            array_insert(array_t*,botrings,i,McMddArrayArrayDup(arrayOfOnionRings));
1796          }
1797        }
1798        ctlFormula->Bottomstates = mddArray_bot;
1799        ctlFormula->Topstates = mddArray_top;
1800        match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
1801        match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
1802        if (buildOnionRings) {
1803          ctlFormula->BotOnionRings = botrings;
1804          ctlFormula->TopOnionRings = toprings;
1805        }
1806        break;/* top passing */
1807      }
1808      /* now calculate the bottom set */
1809      for(i=1;i<number_bot;i++) {
1810        if(buildOnionRings) 
1811          arrayOfOnionRings = array_alloc(array_t *, 0);
1812        leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i);
1813        approx_over = array_fetch(mdd_t *,mddArray_bot,0);
1814        result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
1815                                         approx_over, fairStates, 
1816                                         fairCondition, careStatesArray,
1817                                         earlyTermination, hintsArray,
1818                                         hintType, 
1819                                         &arrayOfOnionRings, verbosity,
1820                                         dcLevel, &fixpoint, GSHschedule);
1821        array_insert(mdd_t *, mddArray_bot, i, result);
1822        if(buildOnionRings) {
1823          array_insert(array_t*,botrings,i,arrayOfOnionRings);
1824        }
1825      }
1826    }
1827    else {
1828      /* compute the bottom sets first which will give us
1829         overapproximation to the exact set */
1830      for(i=1;i<number_bot;i++) {
1831        if(buildOnionRings) 
1832          arrayOfOnionRings = array_alloc(array_t *, 0);
1833        leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,i);
1834        result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
1835                                         NIL(mdd_t), fairStates, 
1836                                         fairCondition, careStatesArray,
1837                                         earlyTermination, hintsArray,
1838                                         hintType, 
1839                                         &arrayOfOnionRings, verbosity,
1840                                         dcLevel, &fixpoint, GSHschedule);
1841        if(buildOnionRings) {
1842          array_insert(array_t*,botrings,i,arrayOfOnionRings);
1843        }
1844        array_insert(mdd_t *, mddArray_bot, i, result);
1845        result_new =  mdd_and(result_ub,result,1,1);
1846        mdd_free(result_ub);
1847        result_ub = result_new;
1848      }
1849      /* calculate the exact set */
1850      if(buildOnionRings){
1851        arrayOfOnionRings = array_alloc(array_t *, 0);
1852      }
1853      leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0);
1854      result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
1855                                       result_ub, fairStates, 
1856                                       fairCondition, careStatesArray,
1857                                       earlyTermination, hintsArray,
1858                                       hintType, 
1859                                       &arrayOfOnionRings, verbosity,
1860                                       dcLevel, &fixpoint, GSHschedule);
1861      array_insert(mdd_t *,mddArray_bot,0,mdd_dup(result));
1862      array_insert(mdd_t *,mddArray_top,0,mdd_dup(result));
1863      mdd_free(result);
1864      if (buildOnionRings) {
1865        Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
1866                               McFormulaFreeDebugData);
1867        array_insert(array_t*,botrings,0,McMddArrayArrayDup(arrayOfOnionRings));
1868        array_insert(array_t*,toprings,0,McMddArrayArrayDup(arrayOfOnionRings));
1869      }
1870      result = array_fetch(mdd_t *,mddArray_bot,0);
1871      if (McCheckEarlyTerminationForOverapprox(earlyTermination, result, careStatesArray)) {
1872        leavesLeftArray = leftChild->leaves;
1873        ctlFormula->leaves = array_dup(leavesLeftArray);
1874        for(i=1;i<number_top;i++) {
1875          array_insert(mdd_t *, mddArray_top, i, mdd_dup(result));
1876          if(buildOnionRings)
1877            array_insert(array_t*,toprings,i,McMddArrayArrayDup(arrayOfOnionRings));
1878        }
1879        ctlFormula->Bottomstates = mddArray_bot;
1880        ctlFormula->Topstates = mddArray_top;
1881        match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot);
1882        match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top);
1883        if (buildOnionRings) {
1884          ctlFormula->BotOnionRings = botrings;
1885          ctlFormula->TopOnionRings = toprings;
1886        }
1887        break; /* top passing */
1888      }
1889      /* calculate the top set now */
1890      for(i=1;i<number_top;i++) {
1891        if (buildOnionRings) {
1892          arrayOfOnionRings = array_alloc(array_t *, 0);
1893        }
1894        leftMdd = array_fetch(mdd_t *,leftChild->Topstates,i);
1895        approx_over = array_fetch(mdd_t *,mddArray_bot,0);
1896        result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd,
1897                                         approx, fairStates, 
1898                                         fairCondition, careStatesArray,
1899                                         earlyTermination, hintsArray,
1900                                         hintType, 
1901                                         &arrayOfOnionRings, verbosity,
1902                                         dcLevel, &fixpoint, GSHschedule);
1903        array_insert(mdd_t *, mddArray_top, i, result);
1904        if(buildOnionRings)
1905          array_insert(array_t*,toprings,i,arrayOfOnionRings);
1906      }
1907    }
1908    mdd_free(result_ub);
1909    /* Now attach the array to the ctlFormula */
1910    ctlFormula->Bottomstates = mddArray_bot;
1911    ctlFormula->Topstates = mddArray_top;
1912    /* Discard previous copies. */
1913    array_free(matchfound_bot);
1914    array_free(matchelement_bot);
1915    array_free(matchfound_top);
1916    array_free(matchelement_top);
1917    ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot);
1918    ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot);
1919    ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top);
1920    ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top);
1921    /* find out the leaves attached to this nodes.*/
1922    leavesLeftArray = leftChild->leaves;
1923    ctlFormula->leaves = array_dup(leavesLeftArray);
1924    if (buildOnionRings) {
1925      ctlFormula->BotOnionRings = botrings;
1926      ctlFormula->TopOnionRings = toprings;
1927    }
1928    if(approx != NIL(mdd_t)) mdd_free(approx);
1929
1930    /* Can't combine under and overapprox */
1931    if(!fixpoint && TRMinimization == Ctlp_Underapprox_c)
1932      TRMinimization = Ctlp_Incomparable_c;
1933
1934    break;
1935  }
1936 
1937  case Ctlp_Init_c:
1938    result = Fsm_FsmComputeInitialStates(modelFsm);
1939    break;
1940   
1941  default: fail("Encountered unknown type of CTL formula\n");
1942  }
1943  tmpMdd = mdd_dup(array_fetch(mdd_t *,mddArray_bot,0));
1944  thisApproxType = ComputeResultingApproximation(
1945    Ctlp_FormulaReadType(ctlFormula), leftApproxType,
1946    rightApproxType, TRMinimization, earlyTermination, fixpoint);
1947  Ctlp_FormulaSetApproxStates(ctlFormula,tmpMdd, TRMinimization);
1948 
1949#ifdef DEBUG_MC
1950  /* The following code is just for debugging */
1951  if ((verbosity == McVerbosityMax_c)) {
1952    char *type = Ctlp_FormulaGetTypeString(ctlFormula);
1953    if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_Cmp_c) {
1954      fprintf(vis_stdout, "Info : result for [Cmp]\n");
1955      if (bdd_is_tautology(result, 1))
1956        fprintf(vis_stdout, "TRUE\n");
1957      else
1958        fprintf(vis_stdout, "FALSE\n");
1959    }
1960    else if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_ID_c) {
1961      char *atomic = Ctlp_FormulaConvertToString(ctlFormula);
1962      fprintf(vis_stdout, "Info : satisfying minterms for [%s(%s)]:\n",
1963              type, atomic);
1964      free(atomic);
1965      if (bdd_is_tautology(result, 1))
1966        fprintf(vis_stdout, "-- TAUTOLOGY --\n");
1967      else if (bdd_is_tautology(result, 0))
1968        fprintf(vis_stdout, "-- null --\n");
1969      else
1970        (void)_McPrintSatisfyingMinterms(result, modelFsm);
1971    }
1972    else {
1973      fprintf(vis_stdout, "Info : satisfying minterms for [%s]:\n", type);
1974      if (bdd_is_tautology(result, 1))
1975        fprintf(vis_stdout, "-- TAUTOLOGY --\n");
1976      else if (bdd_is_tautology(result, 0))
1977        fprintf(vis_stdout, "-- null --\n");
1978      else
1979        (void)_McPrintSatisfyingMinterms(result, modelFsm);
1980    }
1981    free(type);
1982  }
1983#endif
1984  if (modelCareStatesArray == NIL(array_t))
1985      mdd_array_free(careStatesArray);
1986  return;
1987} /* ModelcheckAndVacuity */
1988
1989
1990/**Function********************************************************************
1991
1992  Synopsis    [Annotates formula with satisfying sets of i-th replacement.]
1993 
1994  Description [This function is applied to vacuously passing properties
1995  to generate intersting witnesses.]
1996
1997  SideEffects []
1998
1999  SeeAlso     [CreateImportantCounterexample]
2000
2001******************************************************************************/
2002static void
2003CreateImportantWitness(
2004  Ctlp_Formula_t *OldctlFormula,
2005  Ctlp_Formula_t *ctlFormula,
2006  int i)
2007{
2008  Ctlp_Formula_t *rightChild, *leftChild,*OldrightChild, *OldleftChild;
2009  int number_left_bot;
2010  array_t *onionRings = NIL(array_t); /* array of mdd_t */
2011  array_t  *arrayOfOnionRings = NIL(array_t);
2012  Ctlp_FormulaType formulaType;
2013  formulaType = Ctlp_FormulaReadType(ctlFormula);
2014  rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
2015  leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
2016  OldrightChild = Ctlp_FormulaReadRightChild(OldctlFormula);
2017  OldleftChild = Ctlp_FormulaReadLeftChild(OldctlFormula);
2018
2019  if(leftChild)
2020    number_left_bot = array_n(OldleftChild->Bottomstates);
2021  else
2022    number_left_bot = -1; /* don't care */
2023
2024  switch (formulaType) {
2025  case Ctlp_EU_c:
2026    if(ctlFormula->states != NIL(mdd_t))
2027      mdd_free(ctlFormula->states);
2028    ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i));
2029#if 0
2030    fprintf(vis_stdout,"Attaching bdd for EU %d",i);
2031    bdd_print(ctlFormula->states);
2032    mdd_array_free(array_fetch(array_t*,OldctlFormula->BotOnionRings,i));
2033#endif
2034    onionRings = mdd_array_duplicate(array_fetch(array_t*,OldctlFormula->BotOnionRings,i));
2035    Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings,
2036                           McFormulaFreeDebugData);
2037    assert(leftChild != NULL && rightChild != NULL);
2038    if(i<number_left_bot){
2039      CreateImportantWitness(OldleftChild,leftChild,i);
2040    }
2041    else{
2042      CreateImportantWitness(OldleftChild,leftChild,0);
2043    }
2044
2045    if(i<number_left_bot ){
2046      CreateImportantWitness(OldrightChild,rightChild,0);
2047    }
2048    else {
2049      CreateImportantWitness(OldrightChild,rightChild,i - number_left_bot + 1);
2050    }
2051    break;
2052  case Ctlp_EG_c:
2053    if(ctlFormula->states != NIL(mdd_t))
2054      mdd_free(ctlFormula->states);
2055    ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i));
2056#if 0
2057    fprintf(vis_stdout,"Attaching bdd for EG %d",i);
2058    bdd_print(ctlFormula->states);
2059    mdd_array_free(array_fetch(array_t*,OldctlFormula->BotOnionRings,i));
2060#endif
2061    arrayOfOnionRings = McMddArrayArrayDup(array_fetch(array_t* ,OldctlFormula->BotOnionRings,i));
2062    Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
2063                           McFormulaFreeDebugData);
2064    CreateImportantWitness(OldleftChild,leftChild,i);
2065    break;
2066  case Ctlp_AX_c:
2067  case Ctlp_AG_c:
2068  case Ctlp_AF_c:
2069  case Ctlp_AU_c:
2070  case Ctlp_EX_c:
2071  case Ctlp_EF_c:
2072  case Ctlp_OR_c:
2073  case Ctlp_AND_c: 
2074  case Ctlp_NOT_c: 
2075  case Ctlp_THEN_c:
2076  case Ctlp_XOR_c:
2077  case Ctlp_EQ_c:
2078    if(ctlFormula->states != NIL(mdd_t))
2079      mdd_free(ctlFormula->states);
2080    ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i));
2081#if 0
2082    fprintf(vis_stdout,"Attaching bdd for NOT,THEN %d",i);
2083    bdd_print(ctlFormula->states);
2084#endif
2085
2086    if(leftChild){
2087      if(i<number_left_bot){
2088        CreateImportantWitness(OldleftChild,leftChild,i);
2089      }
2090      else {
2091        CreateImportantWitness(OldleftChild,leftChild,0);
2092      }
2093    }
2094
2095    if(rightChild){
2096      if(i<number_left_bot ){
2097        CreateImportantWitness(OldrightChild,rightChild,0);
2098      }
2099      else{
2100        CreateImportantWitness(OldrightChild,rightChild,i - number_left_bot + 1);
2101      }
2102    }
2103    break;
2104  case Ctlp_ID_c:
2105  case Ctlp_TRUE_c:
2106  case Ctlp_FALSE_c:
2107  case Ctlp_Init_c:
2108    if(ctlFormula->states != NIL(mdd_t))
2109      mdd_free(ctlFormula->states);
2110    ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i));
2111#if 0
2112    fprintf(vis_stdout,"Attaching bdd for ID,TRUE %d",i);
2113    bdd_print(ctlFormula->states);
2114#endif
2115    break;
2116
2117  default:
2118    break;
2119  }
2120} /* CreateImportantWitness */
2121
2122
2123/**Function********************************************************************
2124
2125  Synopsis    [Annotates formula with satisfying sets of i-th replacement.]
2126
2127  Description [This function is applied to vacuously failing properties
2128  to generate intersting counterexamples.]
2129
2130  SideEffects []
2131
2132  SeeAlso     [CreateImportantWitness]
2133
2134******************************************************************************/
2135static void
2136CreateImportantCounterexample(
2137  Ctlp_Formula_t *OldctlFormula,
2138  Ctlp_Formula_t *ctlFormula,
2139  int i)
2140{
2141  Ctlp_Formula_t *rightChild, *leftChild, *OldrightChild, *OldleftChild;
2142  int number_left_top;
2143  array_t *onionRings = NIL(array_t); /* array of mdd_t */
2144  array_t  *arrayOfOnionRings = NIL(array_t);
2145  Ctlp_FormulaType formulaType;
2146  formulaType = Ctlp_FormulaReadType(ctlFormula);
2147  rightChild = Ctlp_FormulaReadRightChild(ctlFormula);
2148  leftChild = Ctlp_FormulaReadLeftChild(ctlFormula);
2149  OldrightChild = Ctlp_FormulaReadRightChild(OldctlFormula);
2150  OldleftChild = Ctlp_FormulaReadLeftChild(OldctlFormula);
2151
2152  if(leftChild)
2153    number_left_top = array_n(OldleftChild->Topstates);
2154  else
2155    number_left_top = -1; /* don't care */
2156
2157  switch (formulaType) {
2158  case Ctlp_EU_c:
2159    if(ctlFormula->states != NIL(mdd_t))
2160      mdd_free(ctlFormula->states);
2161    ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i));
2162    onionRings = mdd_array_duplicate(array_fetch(array_t*,OldctlFormula->TopOnionRings,i));
2163    Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings,
2164                           McFormulaFreeDebugData);
2165    assert(leftChild != NULL && rightChild != NULL);
2166    if(i<number_left_top){
2167      CreateImportantCounterexample(OldleftChild,leftChild,i);
2168    }
2169    else{
2170      CreateImportantCounterexample(OldleftChild,leftChild,0);
2171    }
2172
2173    if(i<number_left_top ){
2174      CreateImportantCounterexample(OldrightChild,rightChild,0);
2175    }
2176    else {
2177      CreateImportantCounterexample(OldrightChild,rightChild,i -
2178                                    number_left_top + 1);
2179    }
2180    break;
2181  case Ctlp_EG_c:
2182    if(ctlFormula->states != NIL(mdd_t))
2183      mdd_free(ctlFormula->states);
2184    ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i));
2185    arrayOfOnionRings = McMddArrayArrayDup(array_fetch(array_t* ,OldctlFormula->TopOnionRings,i));
2186    Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings,
2187                           McFormulaFreeDebugData);
2188    CreateImportantCounterexample(OldleftChild,leftChild,i);
2189    break;
2190  case Ctlp_AX_c:
2191  case Ctlp_AG_c:
2192  case Ctlp_AF_c:
2193  case Ctlp_AU_c:
2194  case Ctlp_EX_c:
2195  case Ctlp_EF_c:
2196  case Ctlp_OR_c:
2197  case Ctlp_AND_c: 
2198  case Ctlp_NOT_c: 
2199  case Ctlp_THEN_c:
2200  case Ctlp_XOR_c:
2201  case Ctlp_EQ_c:
2202    if(ctlFormula->states != NIL(mdd_t))
2203      mdd_free(ctlFormula->states);
2204    ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i));
2205
2206    if(leftChild){
2207      if(i<number_left_top){
2208        CreateImportantCounterexample(OldleftChild,leftChild,i);
2209      }
2210      else {
2211        CreateImportantCounterexample(OldleftChild,leftChild,0);
2212      }
2213    }
2214
2215    if(rightChild){
2216      if(i<number_left_top ){
2217        CreateImportantCounterexample(OldrightChild,rightChild,0);
2218      }
2219      else{
2220        CreateImportantCounterexample(OldrightChild,rightChild,i -
2221                                      number_left_top + 1);
2222      }
2223    }
2224    break;
2225  case Ctlp_ID_c:
2226  case Ctlp_TRUE_c:
2227  case Ctlp_FALSE_c:
2228  case Ctlp_Init_c:
2229    if(ctlFormula->states != NIL(mdd_t))
2230      mdd_free(ctlFormula->states);
2231    ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i));
2232#if 0
2233    fprintf(vis_stdout,"Attaching bdd for ID,TRUE %d",i);
2234    bdd_print(ctlFormula->states);
2235#endif
2236    break;
2237
2238  default:
2239    break;
2240  }
2241} /* CreateImportantCounterexample */
2242
2243
2244/**Function********************************************************************
2245
2246  Synopsis    [Duplicates an array of arrays of MDDs.]
2247
2248  Description [Makes sure ref counts are correct.]
2249
2250  SideEffects [none]
2251
2252  SeeAlso     []
2253
2254******************************************************************************/
2255static array_t *
2256McMddArrayArrayDup(array_t *arrayBddArray)
2257{
2258  int           i;
2259  array_t       *bddArray, *tmpbddArray;
2260  int           length;
2261  array_t       *result;
2262  /* put assert for this  if (arrayBddArray != NIL(array_t)) { */
2263  length = array_n(arrayBddArray);
2264  result = array_alloc(array_t *, length);
2265  for (i = 0; i < length; i++) {
2266    bddArray = array_fetch(array_t *, arrayBddArray, i);
2267    tmpbddArray = mdd_array_duplicate(bddArray);
2268    array_insert(array_t *,result,i,tmpbddArray);
2269  }
2270  return(result);
2271} /* McMddArrayArrayDup */
2272
2273
2274/**Function********************************************************************
2275
2276  Synopsis    [Searches an mdd array of top sets for matches.]
2277
2278  Description []
2279
2280  SideEffects [The node of the formula is annotated with the match info.]
2281
2282  SeeAlso     [match_bot]
2283
2284******************************************************************************/
2285static void
2286match_top(
2287  Ctlp_Formula_t *ctlFormula,
2288  array_t *mddArray,
2289  array_t *matchfound,
2290  array_t *matchelement)
2291{
2292  int i, j, positionmatch;
2293  mdd_t *leftMdd1 = NIL(mdd_t);
2294  mdd_t *leftMdd2 = NIL(mdd_t);
2295
2296  arrayForEachItem(mdd_t *, mddArray, i, leftMdd1){
2297    array_insert(boolean, matchfound, i, FALSE);
2298  }
2299
2300  arrayForEachItem(mdd_t *, mddArray, i, leftMdd1) {
2301    arrayForEachItem(mdd_t *, mddArray, j, leftMdd2) {
2302      if((i != 0) && (j != 0) && (i != j)) {
2303        if (mdd_equal(leftMdd2, leftMdd1)) {
2304          if (array_fetch(boolean, matchfound,i) == TRUE) {
2305            if(array_fetch(int, matchelement,i) != j) {
2306              positionmatch = array_fetch(int, matchelement, i);
2307              array_insert(int, matchelement, j, positionmatch);
2308            }
2309          }
2310          else{
2311            array_insert(int, matchelement, j, i);
2312            array_insert(boolean, matchfound, j, TRUE);
2313          }
2314        }
2315      }
2316    }
2317  }
2318  ctlFormula->matchfound_top = matchfound;
2319  ctlFormula->matchelement_top = matchelement;
2320  return;
2321} /* match_top */
2322
2323
2324/**Function********************************************************************
2325
2326  Synopsis    [Searches an mdd array of bottom sets for matches.]
2327
2328  Description []
2329
2330  SideEffects [The node of the formula is annotated with the match info.]
2331
2332  SeeAlso     [match_top]
2333
2334******************************************************************************/
2335static void
2336match_bot(
2337  Ctlp_Formula_t *ctlFormula,
2338  array_t *mddArray,
2339  array_t *matchfound,
2340  array_t *matchelement)
2341{
2342  int i, j, positionmatch;
2343  mdd_t *leftMdd1 = NIL(mdd_t);
2344  mdd_t *leftMdd2 = NIL(mdd_t);
2345
2346  arrayForEachItem(mdd_t *, mddArray, i, leftMdd1){
2347    array_insert(boolean, matchfound, i, FALSE);
2348  }
2349
2350  arrayForEachItem(mdd_t *, mddArray, i, leftMdd1) {
2351    arrayForEachItem(mdd_t *, mddArray, j, leftMdd2) {
2352      if ((i != 0) && (j != 0) && (i != j)) {
2353        if (mdd_equal(leftMdd2, leftMdd1)) {
2354          if (array_fetch(boolean, matchfound, i) == TRUE) {
2355            if (array_fetch(int, matchelement, i) != j) {
2356              positionmatch = array_fetch(int, matchelement, i);
2357              array_insert(int, matchelement, j, positionmatch);
2358            }
2359          }
2360          else {
2361            array_insert(int, matchelement, j, i);
2362            array_insert(boolean, matchfound, j ,TRUE);
2363          }
2364        }
2365      }
2366    }
2367  }
2368  ctlFormula->matchfound_bot = matchfound;
2369  ctlFormula->matchelement_bot = matchelement;
2370  return;
2371} /* match_bot */
2372
2373
2374/**Function********************************************************************
2375
2376  Synopsis    [Merge onion rings for EU operators.]
2377
2378  Description []
2379 
2380  SideEffects [The first argument is freed.]
2381
2382  SeeAlso     [ModelcheckAndVacuity]
2383
2384******************************************************************************/
2385static array_t *
2386GenerateOnionRings(
2387  array_t* TempOnionRings,
2388  array_t* onionRings)
2389{
2390  array_t* MergeOnionRings;
2391  int  mdd1number, mdd2number, k;
2392  mdd_t *temp,*temp1,*mdd1,*mdd2,*mdd3 = NIL(mdd_t);
2393
2394  mdd1number = array_n(TempOnionRings);
2395  mdd2number = array_n(onionRings);
2396  if(mdd1number == 0) {
2397    MergeOnionRings = mdd_array_duplicate(onionRings);
2398    array_free(TempOnionRings);
2399    return (MergeOnionRings);
2400  }
2401  MergeOnionRings = array_alloc(mdd_t *, 0);
2402  mdd1 = array_fetch(mdd_t *,TempOnionRings,0);
2403  mdd2 = array_fetch(mdd_t *,onionRings,0);
2404  temp = mdd_or(mdd1,mdd2,1,1); /* Building the core for EU */
2405  array_insert(mdd_t *,MergeOnionRings,0, temp);
2406  if(mdd2number>=mdd1number) {
2407    for(k=1;k<mdd1number;k++) {
2408      mdd1 = array_fetch(mdd_t *, onionRings, k);
2409      mdd2 = array_fetch(mdd_t *, MergeOnionRings, k-1);
2410      mdd3 = array_fetch(mdd_t *, TempOnionRings, k);
2411      temp1 = mdd_or(mdd1,mdd3,1,1); 
2412      temp = mdd_and(temp1,mdd2,1,0);
2413      mdd_free(temp1);
2414      array_insert(mdd_t*, MergeOnionRings, k, temp);
2415    }
2416    for(k=mdd1number;k<mdd2number;k++) {
2417      mdd1 = array_fetch(mdd_t *, onionRings, k);
2418      mdd2 = array_fetch(mdd_t *, MergeOnionRings, k-1);
2419      temp = mdd_and(mdd1,mdd2,1,0);
2420      array_insert(mdd_t*, MergeOnionRings, k, temp);
2421    }
2422  }
2423  else {
2424    for(k=1;k<mdd2number;k++) {
2425      mdd1 =array_fetch(mdd_t *, onionRings, k);
2426      mdd2 =array_fetch(mdd_t *, MergeOnionRings, k-1);
2427      mdd3 =array_fetch(mdd_t *, TempOnionRings, k);
2428      temp1 = mdd_or(mdd1,mdd3,1,1); 
2429      temp = mdd_and(temp1,mdd2,1,0);
2430      mdd_free(temp1);
2431      array_insert(mdd_t*, MergeOnionRings, k, temp);
2432    }
2433  }
2434  mdd_array_free(TempOnionRings);
2435  return(MergeOnionRings);
2436} /* GenerateOnionRings */
2437
2438
2439/**Function********************************************************************
2440
2441  Synopsis    [Free debugging info computed during CTL vacuum cleaning.]
2442
2443  Description [Frees debugging info attached to the parse tree by the
2444  CTL vacuum cleaning algorithm.]
2445 
2446  SideEffects [Disposes of various sets attached to nodes of the parse tree.]
2447
2448  SeeAlso     [McVacuityDetection]
2449
2450******************************************************************************/
2451static void
2452FormulaFreeDebugDataVac(
2453  Ctlp_Formula_t *formula)
2454{
2455  int i;
2456  array_t *TopOnion, *BottomOnion;
2457  Ctlp_FormulaType  type = Ctlp_FormulaReadType(formula);
2458  if(formula->type != Ctlp_ID_c ){
2459    if (formula->left  != NIL(Ctlp_Formula_t)) {
2460      FormulaFreeDebugDataVac(formula->left);
2461    }
2462    if (formula->right != NIL(Ctlp_Formula_t)) {
2463      FormulaFreeDebugDataVac(formula->right);
2464    }
2465  }
2466  if (type == Ctlp_EU_c || type == Ctlp_EG_c ) {
2467    if (formula->TopOnionRings != NIL(array_t)) {
2468      TopOnion = formula->TopOnionRings;
2469      for (i = 0; i < array_n(TopOnion); i++) {
2470        if (type == Ctlp_EU_c) {
2471          mdd_array_free(array_fetch(array_t *, TopOnion, i));
2472        }
2473        else if (type == Ctlp_EG_c)
2474          mdd_array_array_free(array_fetch(array_t *, TopOnion, i));
2475      }
2476      array_free(TopOnion);
2477    }
2478    if (formula->BotOnionRings != NIL(array_t)) {
2479      BottomOnion = formula->BotOnionRings;
2480      for (i = 0; i < array_n(BottomOnion); i++) {
2481        if (type == Ctlp_EU_c) {
2482          mdd_array_free(array_fetch(array_t *, BottomOnion, i));
2483        }
2484        else if (type == Ctlp_EG_c)
2485          mdd_array_array_free(array_fetch(array_t *, BottomOnion, i));
2486      }
2487      array_free(BottomOnion);
2488    }
2489  }
2490} /* FormulaFreeDebugDataVac */
Note: See TracBrowser for help on using the repository browser.