source: vis_dev/vis-2.3/src/mc/mcCover.c @ 45

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

vis2.3
File size: 95.6 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [mcCover.c]
4
5  PackageName [mc]
6
7  Synopsis    [Functions for coverage estimation.]
8
9  Description [This file contains the functions implementing coverage
10  estimation for CTL.  According to the proposal of Hoskote et al. (DAC99)
11  a state is covered by a passing property with respect to an observable
12  binary signal if flipping the value of the signal at that state causes
13  the property to fail.  Hoskote et al. proposed an algorithm for the
14  estimation of coverage for a subset of ACTL loosely based on this
15  definition of coverage.<p>
16  This file contains an implementation of Hoskote's algorithm as well as an
17  implementation of the improved algorithm by Jayakumar et al. presented
18  at DAC2003.  The improved algorithm deals with a larger subset of CTL and
19  provides more accurate estimates.]
20
21  SeeAlso     [mcMc.c]
22
23  Author      [Nikhil Jayakumar]
24
25  Copyright   [Copyright (c) 2002-2005, Regents of the University of Colorado
26
27  All rights reserved.
28
29  Redistribution and use in source and binary forms, with or without
30  modification, are permitted provided that the following conditions
31  are met:
32
33  Redistributions of source code must retain the above copyright
34  notice, this list of conditions and the following disclaimer.
35
36  Redistributions in binary form must reproduce the above copyright
37  notice, this list of conditions and the following disclaimer in the
38  documentation and/or other materials provided with the distribution.
39
40  Neither the name of the University of Colorado nor the names of its
41  contributors may be used to endorse or promote products derived from
42  this software without specific prior written permission.
43
44  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
45  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
46  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
47  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
48  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
49  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
50  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
51  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
52  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
53  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
54  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
55  POSSIBILITY OF SUCH DAMAGE.]
56
57******************************************************************************/
58
59#include "ctlpInt.h"
60#include "mcInt.h"
61
62
63/*---------------------------------------------------------------------------*/
64/* Constant declarations                                                     */
65/*---------------------------------------------------------------------------*/
66
67/*---------------------------------------------------------------------------*/
68/* Stucture declarations                                                     */
69/*---------------------------------------------------------------------------*/
70
71/*---------------------------------------------------------------------------*/
72/* Type declarations                                                         */
73/*---------------------------------------------------------------------------*/
74
75/*---------------------------------------------------------------------------*/
76/* Variable declarations                                                     */
77/*---------------------------------------------------------------------------*/
78
79#ifndef lint
80static char rcsid[] UNUSED = "$Id: mcCover.c,v 1.4 2005/05/15 07:32:10 fabio Exp $";
81#endif
82
83/*---------------------------------------------------------------------------*/
84/* Macro declarations                                                        */
85/*---------------------------------------------------------------------------*/
86
87/**AutomaticStart*************************************************************/
88
89/*---------------------------------------------------------------------------*/
90/* Static function prototypes                                                */
91/*---------------------------------------------------------------------------*/
92
93static mdd_t * CoveredStatesHoskote(mdd_t *startstates_old, Fsm_Fsm_t *fsm, Ctlp_Formula_t *OrigFormula, 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, array_t *signalList, array_t *statesCoveredList, array_t *newCoveredStatesList, array_t *statesToRemoveList);
94static mdd_t * CoveredStatesImproved(mdd_t *startstates_old, Fsm_Fsm_t *fsm, Ctlp_Formula_t *OrigFormula, 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, array_t *signalList, array_t *statesCoveredList, array_t *newCoveredStatesList, array_t *statesToRemoveList);
95static mdd_t * CoveragePropositional(mdd_t *startstates_old, Fsm_Fsm_t *fsm, Ctlp_Formula_t *OrigFormula, 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, array_t *signalList, array_t *statesCoveredList, array_t *newCoveredStatesList, array_t *statesToRemoveList);
96static mdd_t * computedepend(Fsm_Fsm_t *fsm, Ctlp_Formula_t *formula, 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, char *signal, mdd_t *SoAndTb_old);
97static mdd_t * computedependHoskote(Fsm_Fsm_t *fsm, Ctlp_Formula_t *formula, 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 *startstates_old, char *signal, mdd_t *Tb, mdd_t *statesCovered, mdd_t *newCoveredStates, mdd_t *statesToRemove);
98static mdd_t * traverse(Fsm_Fsm_t *fsm, 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 *startstates, Ctlp_Formula_t *formula1, Ctlp_Formula_t *formula2);
99static mdd_t * firstReached(Fsm_Fsm_t *fsm, 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 *startstates, Ctlp_Formula_t *formula);
100static Ctlp_Formula_t * FormulaConvertSignalComplement(Fsm_Fsm_t *fsm, char *signal, Ctlp_Formula_t *formula);
101static void findallsignals(Fsm_Fsm_t *fsm, array_t *signalTypeList, array_t *signalList, array_t *statesCoveredList, array_t *newCoveredStatesList, array_t *statesToRemoveList, Ctlp_Formula_t *formula, mdd_t *zeroMdd);
102static void findallsignalsInFormula(array_t *signalList, Ctlp_Formula_t *formula);
103static int positionOfSignalinList(char *signal, array_t *signalList);
104static int RangeofSignalinFormula(Fsm_Fsm_t *fsm, char *signal, Ctlp_Formula_t *formula);
105
106/**AutomaticEnd***************************************************************/
107
108/*---------------------------------------------------------------------------*/
109/* Definition of exported functions                                          */
110/*---------------------------------------------------------------------------*/
111
112
113/*---------------------------------------------------------------------------*/
114/* Definition of internal functions                                          */
115/*---------------------------------------------------------------------------*/
116
117
118/**Function********************************************************************
119
120  Synopsis    [Estimate coverage of one CTL formula.]
121
122  Description [Depending on the options, this function applies either
123  the original algorithm of Hoskote et al. or the improved algorithm of
124  Jayakumar et al..  It then prints statistics on coverage (if the formula
125  passes).]
126
127  SideEffects [Updates running totals]
128
129  SeeAlso     [CommandMc CoveredStatesHoskote CoveredStatesImproved
130  McPrintCoverageSummary]
131
132******************************************************************************/
133void
134McEstimateCoverage(
135  Fsm_Fsm_t *modelFsm,
136  Ctlp_Formula_t *ctlFormula,
137  int i,
138  mdd_t *fairStates,
139  Fsm_Fairness_t *fairCond,
140  array_t *modelCareStatesArray,
141  Mc_EarlyTermination_t *earlyTermination,
142  array_t *hintsStatesArray,
143  Mc_GuidedSearch_t guidedSearchType,
144  Mc_VerbosityLevel verbosity,
145  Mc_DcLevel dcLevel,
146  int buildOnionRings,
147  Mc_GSHScheduleType GSHschedule,
148  Mc_FwdBwdAnalysis traversalDirection,
149  mdd_t *modelInitialStates,
150  mdd_t *ctlFormulaStates,
151  mdd_t **totalcoveredstates,
152  array_t *signalTypeList,
153  array_t *signalList,
154  array_t *statesCoveredList,
155  array_t *newCoveredStatesList,
156  array_t *statesToRemoveList,
157  boolean performCoverageHoskote,
158  boolean performCoverageImproved)
159{
160  double numtotcoveredstates;
161  double numnewcoveredstates;
162  mdd_t *CovstatesHoskote;
163  mdd_t *CovstatesImproved;
164  Ctlp_Formula_t *origFormula;
165
166  if (performCoverageHoskote &&
167      (modelCareStatesArray != NIL(array_t))) { /* and no errors till now? */
168    mdd_t *tmp_mdd, *zero_mdd;
169    int sigarr;
170    array_t *listOfSignals = array_alloc(char *,0);
171    origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
172    if ( ( (traversalDirection == McFwd_c) && bdd_is_tautology(ctlFormulaStates, 1) ) ||
173         mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1) ) { /* formula passes */
174
175      if (*totalcoveredstates == NIL(mdd_t))
176        *totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
177
178      /* add new signals if any found */
179      zero_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
180      findallsignals(modelFsm, signalTypeList, signalList,
181                     statesCoveredList, newCoveredStatesList,
182                     statesToRemoveList, origFormula,
183                     zero_mdd);
184      mdd_free(zero_mdd);
185      fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
186      fprintf(vis_stdout,"===================================\n");
187
188      CovstatesHoskote = CoveredStatesHoskote(modelInitialStates,
189                                              modelFsm, origFormula,
190                                              fairStates, fairCond,
191                                              modelCareStatesArray,
192                                              earlyTermination,
193                                              hintsStatesArray,
194                                              guidedSearchType, verbosity,
195                                              dcLevel, buildOnionRings,
196                                              GSHschedule, signalList,
197                                              statesCoveredList,
198                                              newCoveredStatesList,
199                                              statesToRemoveList);
200      numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
201                                            CovstatesHoskote,
202                                            Fsm_FsmReadPresentStateVars(modelFsm));
203      tmp_mdd = mdd_and(CovstatesHoskote,*totalcoveredstates,1,0);
204
205      numnewcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
206                                            tmp_mdd,
207                                            Fsm_FsmReadPresentStateVars(modelFsm));
208      mdd_free(tmp_mdd);
209      fprintf(vis_stdout,"\n--Total states covered by formula<%d> = %.0f , new = %.0f\n",i+1,
210              numtotcoveredstates,numnewcoveredstates);
211      findallsignalsInFormula(listOfSignals,origFormula);
212      for (sigarr=0;sigarr<array_n(listOfSignals);sigarr++) {
213        mdd_t *newCoveredStates,*statesCovered,*tmp_mdd;
214        char *signalInFormula;
215        int positionInList;
216        signalInFormula = array_fetch(char *,listOfSignals,sigarr);
217        positionInList = positionOfSignalinList(signalInFormula,signalList);
218   
219        newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList);
220        statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList);
221        tmp_mdd = mdd_and(newCoveredStates,statesCovered,1,0);  /*newly covered States*/       
222        fprintf(vis_stdout,"---States covered w.r.t. %s = %.0f, new = %.0f\n",
223                signalInFormula,
224                mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
225                                newCoveredStates,
226                                Fsm_FsmReadPresentStateVars(modelFsm)),
227                mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
228                                tmp_mdd,
229                                Fsm_FsmReadPresentStateVars(modelFsm)));
230        mdd_free(tmp_mdd);
231
232        /* add on the newcoveredstates*/
233        tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1);
234        mdd_free(statesCovered);
235        /*update statesCoveredList*/
236        array_insert(mdd_t *,statesCoveredList,positionInList,tmp_mdd);
237        mdd_free(newCoveredStates);
238
239        /* reset newCoveredStatesList to zeroMdds for the next formula */
240        tmp_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
241        array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd);
242      }
243 
244    } else { /* formula fails */
245      CovstatesHoskote = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
246      fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
247      fprintf(vis_stdout,"===================================\n");
248      fprintf(vis_stdout,"Coverage for failing formulae = 0\n");
249    }
250    if (*totalcoveredstates == NIL(mdd_t))
251      *totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
252       
253    if (CovstatesHoskote != NIL(mdd_t)){
254      mdd_t *tmp_mdd = mdd_or(*totalcoveredstates,CovstatesHoskote,1,1);
255      mdd_free(*totalcoveredstates);
256      *totalcoveredstates = tmp_mdd;
257    }
258       
259    numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
260                                          *totalcoveredstates,
261                                          Fsm_FsmReadPresentStateVars(modelFsm));
262    mdd_free(CovstatesHoskote);
263    array_free(listOfSignals);
264  }
265
266  if (performCoverageImproved && (modelCareStatesArray != NIL(array_t))) { /* and no errors till now ??*/
267    mdd_t *tmp_mdd, *zero_mdd;
268    int sigarr;
269    array_t *listOfSignals = array_alloc(char *,0);
270    origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
271    if ( ( (traversalDirection == McFwd_c) &&
272           bdd_is_tautology(ctlFormulaStates, 1) ) ||
273         (mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1)) ) {
274      /* formula passes */
275
276      if (*totalcoveredstates == NIL(mdd_t))
277        *totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm)); 
278
279      /*add new signals if any found*/
280      zero_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
281      findallsignals(modelFsm, signalTypeList, signalList,
282                     statesCoveredList, newCoveredStatesList,
283                     statesToRemoveList, origFormula, zero_mdd);
284      mdd_free(zero_mdd);
285      fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
286      fprintf(vis_stdout,"===================================\n");
287
288      CovstatesImproved = CoveredStatesImproved(modelInitialStates,
289                                                modelFsm, origFormula,
290                                                fairStates, fairCond,
291                                                modelCareStatesArray,
292                                                earlyTermination,
293                                                hintsStatesArray,
294                                                guidedSearchType,
295                                                verbosity,
296                                                dcLevel, buildOnionRings,
297                                                GSHschedule, signalList,
298                                                statesCoveredList,
299                                                newCoveredStatesList,
300                                                statesToRemoveList);
301      numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
302                                            CovstatesImproved,
303                                            Fsm_FsmReadPresentStateVars(modelFsm));
304      tmp_mdd = mdd_and(CovstatesImproved,*totalcoveredstates,1,0);
305
306      numnewcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
307                                            tmp_mdd,
308                                            Fsm_FsmReadPresentStateVars(modelFsm));
309      mdd_free(tmp_mdd);
310      fprintf(vis_stdout,"\n--Total states covered by formula<%d> = %.0f , new = %.0f\n",i+1,
311              numtotcoveredstates,numnewcoveredstates);
312      findallsignalsInFormula(listOfSignals,origFormula);
313      for (sigarr=0;sigarr<array_n(listOfSignals);sigarr++) {
314        mdd_t *newCoveredStates,*statesCovered,*tmp_mdd;
315        char *signalInFormula;
316        int positionInList;
317        signalInFormula = array_fetch(char *,listOfSignals,sigarr);
318        positionInList = positionOfSignalinList(signalInFormula,signalList);
319   
320        newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList);
321        statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList);
322        tmp_mdd = mdd_and(newCoveredStates,statesCovered,1,0);  /*newly covered States*/       
323        fprintf(vis_stdout,"---States covered w.r.t. %s = %.0f, new = %.0f\n",
324                signalInFormula,
325                mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
326                                newCoveredStates,
327                                Fsm_FsmReadPresentStateVars(modelFsm)),
328                mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
329                                tmp_mdd,
330                                Fsm_FsmReadPresentStateVars(modelFsm)));
331        mdd_free(tmp_mdd);
332
333        /* add on the newcoveredstates*/
334        tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1);
335        mdd_free(statesCovered);
336        /*update statesCoveredList*/
337        array_insert(mdd_t *,statesCoveredList,positionInList,tmp_mdd);
338        mdd_free(newCoveredStates);
339
340        /* reset newCoveredStatesList to zeroMdds for the next formula */
341        tmp_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
342        array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd);
343      }
344
345    } else { /* formula fails */
346      CovstatesImproved = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
347      fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
348      fprintf(vis_stdout,"===================================\n");
349      fprintf(vis_stdout,"Coverage for failing formulae = 0\n");
350    }
351    if (*totalcoveredstates == NIL(mdd_t))
352      *totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
353       
354    if (CovstatesImproved != NIL(mdd_t)){
355      mdd_t *tmp_mdd = mdd_or(*totalcoveredstates,CovstatesImproved,1,1);
356      mdd_free(*totalcoveredstates);
357      *totalcoveredstates = tmp_mdd;
358    }
359       
360    numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
361                                          *totalcoveredstates,
362                                          Fsm_FsmReadPresentStateVars(modelFsm));
363    mdd_free(CovstatesImproved);
364    array_free(listOfSignals);
365  }
366
367} /* McEstimateCoverage */
368
369
370/**Function********************************************************************
371
372  Synopsis    [Print summary for the coverage of a property file.]
373
374  SideEffects [none]
375
376  SeeAlso     [CommandMc McEstimateCoverage]
377
378******************************************************************************/
379void
380McPrintCoverageSummary(
381  Fsm_Fsm_t *modelFsm,
382  Mc_DcLevel dcLevel,
383  McOptions_t *options,
384  array_t *modelCareStatesArray,
385  mdd_t *modelCareStates,
386  mdd_t *totalcoveredstates,
387  array_t *signalTypeList,
388  array_t *signalList,
389  array_t *statesCoveredList,
390  boolean performCoverageHoskote,
391  boolean performCoverageImproved
392  )
393{
394  float coverage;
395  float coveragePI;
396  float coveragePO;
397  float coverageOther;
398  float numPI;
399  float numPO;
400  float numOther;
401  float avgCoverage;
402  float avgPICoverage;
403  float avgPOCoverage;
404  float avgOtherCoverage;
405  double numrchstates;
406  double numtotcoveredstates;
407
408  if (performCoverageHoskote &&
409      (modelCareStatesArray != NIL(array_t))) { /* and no errors till now */
410    int sigarr;
411    if (totalcoveredstates != NIL(mdd_t) && (modelCareStates != NIL(mdd_t))) {
412      numtotcoveredstates = mdd_count_onset(
413        Fsm_FsmReadMddManager(modelFsm),
414        totalcoveredstates,
415        Fsm_FsmReadPresentStateVars(modelFsm));
416    }
417    else {
418      numtotcoveredstates = 0;
419    }
420   
421    if ((dcLevel == McDcLevelRch_c)||(dcLevel == McDcLevelRchFrontier_c)) {
422      if (!mdd_lequal(totalcoveredstates, modelCareStates, 1, 1)) {
423        (void)fprintf(vis_stdout,
424                    "** mc warning: Some of the covered states are not reachable\n");
425      }
426      if (modelCareStates !=NIL(mdd_t)){
427        int sigType;
428        coveragePI = 0;
429        coveragePO = 0;
430        coverageOther = 0;
431        numPI = 0;
432        numPO = 0;
433        numOther = 0;
434        avgCoverage = 0;
435        avgPICoverage = 0;
436        avgPOCoverage = 0;
437        avgOtherCoverage = 0;
438        numrchstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
439                                       modelCareStates,
440                                       Fsm_FsmReadPresentStateVars(modelFsm));
441        if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
442          fprintf(vis_stdout,"\nCoverage for all the Formulae w.r.t. all observable signals\n");
443          fprintf(vis_stdout,"=============================================================\n");
444        }
445        for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
446          mdd_t *statesCovered, *uncoveredStateCube, *uncoveredStates;
447          double numStatesCovered;
448          char *nrOfUncoveredStatesString;
449          int nrOfUncoveredStates, prntStates;   /* nr of uncovered states that we output */
450
451          Ntk_Network_t *modelNetworkC = Fsm_FsmReadNetwork(modelFsm);
452          array_t *PSVarsC = Fsm_FsmReadPresentStateVars(modelFsm);
453          mdd_manager *mddMgrC = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
454
455          statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
456          numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
457                                             statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
458          coverage = (numStatesCovered / numrchstates) * 100;
459          avgCoverage = avgCoverage + coverage;
460          sigType = array_fetch(int, signalTypeList,sigarr);
461          if (sigType == 1) {
462            coveragePI = coveragePI + numStatesCovered;
463            avgPICoverage = avgPICoverage + coverage;
464            numPI = numPI + 1;
465          }
466          else if (sigType == 0) {
467            coveragePO = coveragePO + numStatesCovered;
468            avgPOCoverage = avgPOCoverage + coverage;
469            numPO = numPO + 1;
470          }
471          else {
472            coverageOther = coverageOther + numStatesCovered;
473            avgOtherCoverage = avgOtherCoverage + coverage;
474            numOther = numOther + 1;
475          }
476          if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
477            fprintf(vis_stdout,"\n# States covered w.r.t. %s = %.0f, Percentage of Coverage = %f\n",
478                    array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
479            nrOfUncoveredStatesString = Cmd_FlagReadByName("nr_uncoveredstates");
480            if(nrOfUncoveredStatesString == NIL(char))
481              nrOfUncoveredStates = 1;
482            else
483              nrOfUncoveredStates = atoi(nrOfUncoveredStatesString);
484            if (numStatesCovered < numrchstates) {
485              if ((numrchstates-numStatesCovered) < nrOfUncoveredStates)
486                nrOfUncoveredStates = (int)(numrchstates-numStatesCovered);
487              fprintf(vis_stdout,"#Printing reachable states NOT covered w.r.t. %s :\n",array_fetch(char *,signalList,sigarr));
488              for (prntStates = 0;prntStates<nrOfUncoveredStates;prntStates++){ 
489                fprintf(vis_stdout,"\n#State %d :\n",prntStates+1);
490                uncoveredStates = mdd_and(modelCareStates,statesCovered,1,0);
491                uncoveredStateCube = Mc_ComputeAMinterm(uncoveredStates, PSVarsC, mddMgrC);
492                mdd_free(uncoveredStates);
493                Mc_MintermPrint(uncoveredStateCube, PSVarsC, modelNetworkC);
494                mdd_free(uncoveredStateCube);
495              }
496            }
497          }
498        }
499        fprintf(vis_stdout,"\nTotal Coverage for all the Formulae\n");
500        fprintf(vis_stdout,"=====================================\n");
501        for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
502          mdd_t *statesCovered;
503          double numStatesCovered;
504          char *type;
505          int sigType;
506
507          sigType = array_fetch(int, signalTypeList,sigarr);
508          if (sigType == 1)
509            type = "Primary Input";
510          else if (sigType == 0)
511            type = "Primary Output";
512          else
513            type = "Neither Primary output nor input";
514
515          statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
516
517          numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
518                                             statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
519          coverage = (numStatesCovered / numrchstates) * 100;
520          fprintf(vis_stdout,"# States covered w.r.t. %s(%s) = %.0f, Percentage of Coverage = %f\n",type,
521                  array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
522        }
523        fprintf(vis_stdout,"--There are %.0f covered states (using Hoskote et.al's implementation)\n",numtotcoveredstates);
524        fprintf(vis_stdout,"--%.0f states covered by Primary Input Signals\n",coveragePI);
525        fprintf(vis_stdout,"--%.0f states covered by Primary Ouput Signals\n",coveragePO);
526        fprintf(vis_stdout,"--%.0f states covered by signals which are neither Primary input nor output Signals\n",coverageOther);
527        fprintf(vis_stdout,"--There are %.0f reachable states\n",numrchstates);
528
529        coverage = (numtotcoveredstates / numrchstates) * 100;
530        fprintf(vis_stdout,"Percentage of coverage (using Hoskote et.al's implementation)= %f\n ",coverage);
531        avgCoverage = avgCoverage / array_n(signalList);
532        fprintf(vis_stdout,"Average Percentage of coverage = %f\n",avgCoverage);
533        if (numPI < 1)
534          fprintf(vis_stdout,"No Primary Input signals\n");
535        else {
536          avgPICoverage = avgPICoverage / numPI;
537          fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgPICoverage);
538        }
539        if (numPO < 1)
540          fprintf(vis_stdout,"No Primary Output signals\n");
541        else {
542          avgPOCoverage = avgPOCoverage / numPO;
543          fprintf(vis_stdout,"Average Percentage of coverage for Primary outputs = %f\n",avgPOCoverage);
544        }
545        if (numOther < 1)
546          fprintf(vis_stdout,"No signals which are neither primary inputs nor outputs\n");
547        else {
548          avgOtherCoverage = avgOtherCoverage / numOther;
549          fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgOtherCoverage);
550        }
551      }
552      else {
553        fprintf(vis_stdout,"Reachable states = NIL !\n");
554      }
555    }
556  }
557
558  if (performCoverageImproved && (modelCareStatesArray != NIL(array_t))) { /* and no errors till now */
559    int sigarr;
560    if (totalcoveredstates != NIL(mdd_t) && (modelCareStates != NIL(mdd_t))) {
561      numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),totalcoveredstates,Fsm_FsmReadPresentStateVars(modelFsm));
562    }
563    else {
564      numtotcoveredstates = 0;
565    }
566   
567    if ((dcLevel == McDcLevelRch_c)||(dcLevel == McDcLevelRchFrontier_c)) {
568      if (!mdd_lequal(totalcoveredstates, modelCareStates, 1, 1)) {
569        (void)fprintf(vis_stdout,
570                      "** mc warning: Some of the covered states are not reachable\n");
571      }
572      if (modelCareStates !=NIL(mdd_t)){
573        int sigType;
574
575        coveragePI = 0;
576        coveragePO = 0;
577        coverageOther = 0;
578        numPI = 0;
579        numPO = 0;
580        numOther = 0;
581        avgCoverage = 0;
582        avgPICoverage = 0;
583        avgPOCoverage = 0;
584        avgOtherCoverage = 0;
585
586        numrchstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),modelCareStates,Fsm_FsmReadPresentStateVars(modelFsm));
587        if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
588          fprintf(vis_stdout,"\nCoverage for all the Formulae w.r.t. all observable signals\n");
589          fprintf(vis_stdout,"=============================================================\n");
590        }
591        for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
592          mdd_t *statesCovered, *uncoveredStateCube, *uncoveredStates;
593          double numStatesCovered;
594          char *nrOfUncoveredStatesString;
595          int nrOfUncoveredStates, prntStates; /* nr of uncovered states that we output */
596
597          Ntk_Network_t *modelNetworkC = Fsm_FsmReadNetwork(modelFsm);
598          array_t *PSVarsC = Fsm_FsmReadPresentStateVars(modelFsm);
599          mdd_manager *mddMgrC = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
600
601          statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
602          numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
603                                             statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
604          coverage = (numStatesCovered / numrchstates) * 100;
605          avgCoverage = avgCoverage + coverage;
606          sigType = array_fetch(int, signalTypeList,sigarr);
607          if (sigType == 1) {
608            coveragePI = coveragePI + numStatesCovered;
609            avgPICoverage = avgPICoverage + coverage;
610            numPI = numPI + 1;
611          }
612          else if (sigType == 0) {
613            coveragePO = coveragePO + numStatesCovered;
614            avgPOCoverage = avgPOCoverage + coverage;
615            numPO = numPO + 1;
616          }
617          else {
618            coverageOther = coverageOther + numStatesCovered;
619            avgOtherCoverage = avgOtherCoverage + coverage;
620            numOther = numOther + 1;
621          }
622          if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
623            fprintf(vis_stdout,"\n# States covered w.r.t. %s = %.0f, Percentage of Coverage = %f\n",
624                    array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
625            nrOfUncoveredStatesString = Cmd_FlagReadByName("nr_uncoveredstates");
626            if(nrOfUncoveredStatesString == NIL(char))
627              nrOfUncoveredStates = 1;
628            else
629              nrOfUncoveredStates = atoi(nrOfUncoveredStatesString);
630            if (numStatesCovered < numrchstates) {
631              if ((numrchstates-numStatesCovered) < nrOfUncoveredStates)
632                nrOfUncoveredStates = (int)(numrchstates-numStatesCovered);
633              fprintf(vis_stdout,"#Printing reachable states NOT covered w.r.t. %s :\n",array_fetch(char *,signalList,sigarr));
634              for (prntStates = 0;prntStates<nrOfUncoveredStates;prntStates++){ 
635                fprintf(vis_stdout,"\n#State %d :\n",prntStates+1);
636                uncoveredStates = mdd_and(modelCareStates,statesCovered,1,0);
637                uncoveredStateCube = Mc_ComputeAMinterm(uncoveredStates, PSVarsC, mddMgrC);
638                mdd_free(uncoveredStates);
639                Mc_MintermPrint(uncoveredStateCube, PSVarsC, modelNetworkC);
640                mdd_free(uncoveredStateCube);
641              }
642            }
643          }
644        }
645        fprintf(vis_stdout,"\nTotal Coverage for all the Formulae\n");
646        fprintf(vis_stdout,"=====================================\n");
647        for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
648          mdd_t *statesCovered;
649          double numStatesCovered;
650          char *type;
651          int sigType;
652          sigType = array_fetch(int, signalTypeList,sigarr);
653          if (sigType == 1)
654            type = "Primary Input";
655          else if (sigType == 0)
656            type = "Primary Output";
657          else
658            type = "Neither Primary output nor input";
659          statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
660          numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
661                                             statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
662          coverage = (numStatesCovered / numrchstates) * 100;
663          fprintf(vis_stdout,"# States covered w.r.t. %s(%s) = %.0f, Percentage of Coverage = %f\n",type,
664                  array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
665        }
666        fprintf(vis_stdout,"--There are %.0f covered states (using improved coverage implementation)\n",numtotcoveredstates);
667        fprintf(vis_stdout,"--%.0f states covered by Primary Input Signals\n",coveragePI);
668        fprintf(vis_stdout,"--%.0f states covered by Primary Ouput Signals\n",coveragePO);
669        fprintf(vis_stdout,"--%.0f states covered by signals which are neither Primary input nor output Signals\n",coverageOther);
670        fprintf(vis_stdout,"--There are %.0f reachable states\n",numrchstates);
671
672        coverage = (numtotcoveredstates / numrchstates) * 100;
673        fprintf(vis_stdout,"Percentage of coverage (using improved coverage implementation)= %f\n ",coverage);
674        avgCoverage = avgCoverage / array_n(signalList);
675        fprintf(vis_stdout,"Average Percentage of coverage = %f\n",avgCoverage);
676        if (numPI < 1)
677          fprintf(vis_stdout,"No Primary Input signals\n");
678        else {
679          avgPICoverage = avgPICoverage / numPI;
680          fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgPICoverage);
681        }
682        if (numPO < 1)
683          fprintf(vis_stdout,"No Primary Output signals\n");
684        else {
685          avgPOCoverage = avgPOCoverage / numPO;
686          fprintf(vis_stdout,"Average Percentage of coverage for Primary outputs = %f\n",avgPOCoverage);
687        }
688        if (numOther < 1)
689          fprintf(vis_stdout,"No signals which are not primary\n");
690        else {
691          avgOtherCoverage = avgOtherCoverage / numOther;
692          fprintf(vis_stdout,"Average Percentage of coverage for signals which are not primary = %f\n",avgOtherCoverage);
693        }
694      }
695      else {
696        fprintf(vis_stdout,"Reachable states = NIL !\n");
697      }
698    }
699  }
700} /* McPrintCoverageSummary */
701
702/*---------------------------------------------------------------------------*/
703/* Definition of static functions                                            */
704/*---------------------------------------------------------------------------*/
705
706
707/**Function********************************************************************
708
709  Synopsis    [Computes a the set of covered states for a given formula and
710               initial set of states given.]
711
712  Description [Presently Works for only a subset
713  of ACTL viz. (propostional formulae, ->, AX, AG, AF, AU, ^ )]
714
715  SideEffects [Updates running totals.]
716
717  SeeAlso     [McEstimateCoverage CoveredStatesImproved]
718
719******************************************************************************/
720static mdd_t *
721CoveredStatesHoskote(
722  mdd_t *startstates_old,
723  Fsm_Fsm_t *fsm,
724  Ctlp_Formula_t *OrigFormula,
725  mdd_t *fairStates,
726  Fsm_Fairness_t *fairCondition,
727  array_t *careStatesArray,
728  Mc_EarlyTermination_t *earlyTermination,
729  Fsm_HintsArray_t *hintsArray,
730  Mc_GuidedSearch_t hintType,
731  Mc_VerbosityLevel verbosity,
732  Mc_DcLevel dcLevel,
733  int buildOnionRing,
734  Mc_GSHScheduleType GSHschedule,
735  array_t *signalList,
736  array_t *statesCoveredList,
737  array_t *newCoveredStatesList,
738  array_t *statesToRemoveList)
739{
740  mdd_t *Covstates1, *temp1, *temp2;
741  mdd_t *Covstates2;
742  mdd_t *result;
743  mdd_t *travstates;
744  mdd_t *frstrchstates;
745 
746  mdd_t *startstates;
747
748  Ctlp_FormulaType formulaType;
749  Ctlp_Formula_t *rightFormula, *leftFormula, *tmp_formula, *existFormula;
750  double numresultstates; /* used for debugging <NJ> */
751
752  startstates = mdd_and(startstates_old,fairStates,1,1);
753
754  if (mdd_is_tautology(startstates,0)) {
755    if (verbosity > McVerbosityNone_c)
756      fprintf(vis_stdout,
757              "\n--Startstates are down to zero. Coverage is hence zero.\n");
758    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
759    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
760                                      Fsm_FsmReadPresentStateVars(fsm));
761    mdd_free(startstates);
762    return result;
763  }
764  if (Ctlp_FormulaTestIsQuantifierFree(OrigFormula)) {
765    /*propositional formula*/
766    result = CoveragePropositional(startstates, fsm, OrigFormula, fairStates,
767                                   fairCondition, careStatesArray,
768                                   earlyTermination, hintsArray, hintType,
769                                   verbosity, dcLevel,buildOnionRing,
770                                   GSHschedule, signalList, statesCoveredList,
771                                   newCoveredStatesList, statesToRemoveList);
772    temp1 = result;
773    result = mdd_and(temp1,fairStates,1,1);
774    mdd_free(temp1);
775    mdd_free(startstates);
776    return result;
777  }
778  formulaType = Ctlp_FormulaReadType(OrigFormula);
779  switch (formulaType) {
780  case Ctlp_EG_c: 
781  case Ctlp_EF_c:
782  case Ctlp_EU_c:
783  case Ctlp_FwdU_c:
784  case Ctlp_FwdG_c:
785  case Ctlp_EY_c:
786  case Ctlp_EH_c:
787  case Ctlp_Cmp_c:
788  case Ctlp_EX_c:
789  case Ctlp_Init_c:  {
790    fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL,\n");
791    fprintf(vis_stdout,"** can't compute coverage of : ");
792    Ctlp_FormulaPrint(vis_stdout,OrigFormula);
793    fprintf(vis_stdout,"\n");
794    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
795    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,Fsm_FsmReadPresentStateVars(fsm));
796    mdd_free(startstates);
797    return result;
798    break;
799  }
800  case Ctlp_AX_c:{
801    temp1 = Mc_FsmEvaluateEYFormula(fsm, startstates, fairStates, careStatesArray, verbosity, dcLevel);
802    Covstates1 = mdd_and(temp1,fairStates,1,1);
803    mdd_free(temp1);
804    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
805    result = CoveredStatesHoskote(Covstates1, fsm, leftFormula, fairStates,
806                                  fairCondition, careStatesArray,
807                                  earlyTermination, hintsArray,
808                                  hintType, verbosity, dcLevel, buildOnionRing,
809                                  GSHschedule, signalList, statesCoveredList,
810                                  newCoveredStatesList, statesToRemoveList);
811    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
812                                      Fsm_FsmReadPresentStateVars(fsm));
813    mdd_free(Covstates1);
814    temp1 = result;
815    result = mdd_and(temp1,fairStates,1,1);
816    mdd_free(temp1);
817    mdd_free(startstates);
818    return result;
819    break;
820  }
821  case Ctlp_AG_c:{
822    mdd_t *initStates;
823    double numststates;
824    initStates = Fsm_FsmComputeInitialStates(fsm);
825    temp1 = mdd_one(Fsm_FsmReadMddManager(fsm));
826    if (mdd_equal_mod_care_set_array(startstates,initStates,careStatesArray)) {
827      if (verbosity > McVerbosityNone_c)
828        fprintf(vis_stdout,"\nUsing the reachable states already computed...");
829      temp2 = Fsm_FsmComputeReachableStates(fsm, 0, 1, 0, 0, 0, 0, 0,
830                                            Fsm_Rch_Default_c, 0, 0,
831                                            NIL(array_t), FALSE, NIL(array_t));
832    } else
833      temp2 = Mc_FsmEvaluateFwdUFormula(fsm, startstates, temp1, fairStates,
834                                        careStatesArray, NIL(array_t),
835                                        verbosity, dcLevel);
836    mdd_free(initStates);
837    numststates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),startstates,
838                                  Fsm_FsmReadPresentStateVars(fsm));
839    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),temp2,
840                                      Fsm_FsmReadPresentStateVars(fsm));
841    mdd_free(temp1);
842    Covstates1 = mdd_and(temp2,fairStates,1,1);
843    mdd_free(temp2);
844    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
845    result = CoveredStatesHoskote(Covstates1, fsm, leftFormula, fairStates,
846                                  fairCondition, careStatesArray,
847                                  earlyTermination, hintsArray, hintType,
848                                  verbosity, dcLevel, buildOnionRing,
849                                  GSHschedule, signalList, statesCoveredList,
850                                  newCoveredStatesList, statesToRemoveList);
851    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
852                                      Fsm_FsmReadPresentStateVars(fsm));
853    mdd_free(Covstates1);
854    temp1 = result;
855    result = mdd_and(temp1,fairStates,1,1);
856    mdd_free(temp1);
857    mdd_free(startstates);
858    return result;
859    break;
860  }
861  case Ctlp_AF_c:{
862    tmp_formula = OrigFormula;
863    OrigFormula = Ctlp_FormulaConvertAFtoAU(tmp_formula);
864    if (verbosity > McVerbosityNone_c) {
865      fprintf(vis_stdout,"Converting formula from\n");
866      Ctlp_FormulaPrint(vis_stdout,tmp_formula);
867      fprintf(vis_stdout,"\nto\n");
868      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
869      fprintf(vis_stdout,"\n");
870    }
871#if 0
872    Ctlp_FormulaFree(tmp_formula);
873    formulaType = Ctlp_AU_c;
874#endif
875    /* convert to AFp to A (TRUE) U p  and then step thru to do coverage
876       for AU computation below*/
877  }
878  case Ctlp_AU_c:{
879    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
880    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
881    travstates = traverse(fsm, fairStates, fairCondition, careStatesArray,
882                          earlyTermination, hintsArray, hintType, verbosity,
883                          dcLevel, buildOnionRing, GSHschedule, startstates,
884                          leftFormula,rightFormula);
885    if (verbosity > McVerbosityNone_c) {
886      fprintf(vis_stdout,"\n---Computing coverage for LHS of U formula i.e: ");
887      Ctlp_FormulaPrint(vis_stdout,leftFormula);
888      fprintf(vis_stdout,
889              "\n------------------------------------------------\n");
890    }
891    Covstates1 = CoveredStatesHoskote(travstates, fsm, leftFormula, fairStates,
892                                      fairCondition, careStatesArray,
893                                      earlyTermination, hintsArray, hintType,
894                                      verbosity, dcLevel, buildOnionRing,
895                                      GSHschedule, signalList,
896                                      statesCoveredList, newCoveredStatesList,
897                                      statesToRemoveList);
898    mdd_free(travstates);
899    frstrchstates = firstReached(fsm, fairStates, fairCondition,
900                                 careStatesArray, earlyTermination, hintsArray,
901                                 hintType, verbosity, dcLevel, buildOnionRing,
902                                 GSHschedule, startstates, rightFormula);
903    if (verbosity > McVerbosityNone_c) {
904      fprintf(vis_stdout,"\n---Computing coverage for RHS of U formula i.e: ");
905      Ctlp_FormulaPrint(vis_stdout,rightFormula);
906      fprintf(vis_stdout,
907              "\n------------------------------------------------\n");
908    }
909    Covstates2 = CoveredStatesHoskote(frstrchstates, fsm, rightFormula,
910                                      fairStates, fairCondition,
911                                      careStatesArray, earlyTermination,
912                                      hintsArray, hintType, verbosity, dcLevel,
913                                      buildOnionRing, GSHschedule, signalList,
914                                      statesCoveredList, newCoveredStatesList,
915                                      statesToRemoveList);
916    mdd_free(frstrchstates);
917    result = mdd_or(Covstates1,Covstates2,1,1);
918    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
919                                      Fsm_FsmReadPresentStateVars(fsm));
920    mdd_free(Covstates1);
921    mdd_free(Covstates2);
922    temp1 = result;
923    result = mdd_and(temp1,fairStates,1,1);
924    if (formulaType == Ctlp_AF_c)
925      Ctlp_FormulaFree(OrigFormula);
926    mdd_free(temp1);
927    mdd_free(startstates);
928    return result;
929    break;
930  }
931  case Ctlp_AND_c:{
932    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
933    if (verbosity > McVerbosityNone_c) {
934      fprintf(vis_stdout,"---Computing coverage for LHS sub-formula: ");
935      Ctlp_FormulaPrint(vis_stdout,leftFormula);
936      fprintf(vis_stdout,
937              "\n------------------------------------------------\n");
938    }
939    Covstates1 = CoveredStatesHoskote(startstates,fsm, leftFormula, fairStates,
940                                      fairCondition, careStatesArray,
941                                      earlyTermination, hintsArray, hintType,
942                                      verbosity, dcLevel, buildOnionRing,
943                                      GSHschedule, signalList,
944                                      statesCoveredList, newCoveredStatesList,
945                                      statesToRemoveList);
946    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
947    if (verbosity > McVerbosityNone_c) {
948      fprintf(vis_stdout,"---Computing coverage for RHS sub-formula: ");
949      Ctlp_FormulaPrint(vis_stdout,rightFormula);
950      fprintf(vis_stdout,
951              "\n------------------------------------------------\n");
952    }
953    Covstates2 = CoveredStatesHoskote(startstates,fsm, rightFormula,
954                                      fairStates, fairCondition, 
955                                      careStatesArray, earlyTermination,
956                                      hintsArray, hintType, verbosity, dcLevel,
957                                      buildOnionRing,GSHschedule, signalList,
958                                      statesCoveredList, newCoveredStatesList,
959                                      statesToRemoveList);
960    result = mdd_or(Covstates1, Covstates2, 1, 1);
961    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
962                                      Fsm_FsmReadPresentStateVars(fsm));
963    mdd_free(Covstates1);
964    mdd_free(Covstates2);
965    temp1 = result;
966    result = mdd_and(temp1,fairStates,1,1);
967    mdd_free(temp1);
968    mdd_free(startstates);
969    return result;
970    break;
971  }
972  case Ctlp_THEN_c:{ /*f1 -> f2 = !f2 -> !f1*/
973    mdd_t *nextstartstates, *Tb;
974   
975    if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadLeftChild(OrigFormula))) { /*if f1 is propositional*/
976      leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
977      rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
978    } else if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadRightChild(OrigFormula))) { /*if f2 is propositional*/
979       /* Convert f1->f2 to !f2->!f1      */
980      leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
981      rightFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
982    } else { /*neither are propositional*/
983      fprintf(vis_stdout,"\nCan't compute coverage of implications where neither side is propositional\n");
984      fprintf(vis_stdout,"Could not compute coverage of :");
985      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
986      result = mdd_zero(Fsm_FsmReadMddManager(fsm));
987      mdd_free(startstates);
988      return result;
989    }
990    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
991    Tb = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
992                               fairCondition, careStatesArray,
993                               earlyTermination, hintsArray, hintType,
994                               verbosity, dcLevel, buildOnionRing,GSHschedule);
995    Ctlp_FormulaFree(existFormula);
996    nextstartstates = mdd_and(startstates, Tb,1,1);
997    mdd_free(Tb);
998    Covstates1 = CoveredStatesHoskote(nextstartstates,fsm, rightFormula,
999                                      fairStates, fairCondition, 
1000                                      careStatesArray, earlyTermination,
1001                                      hintsArray, hintType, verbosity, dcLevel,
1002                                      buildOnionRing,GSHschedule, signalList,
1003                                      statesCoveredList, newCoveredStatesList,
1004                                      statesToRemoveList);
1005    mdd_free(nextstartstates);
1006    mdd_free(startstates);
1007    return Covstates1;
1008    break;
1009  }
1010  case Ctlp_XOR_c: {
1011    tmp_formula = Ctlp_FormulaConvertXORtoOR(OrigFormula);
1012    if (verbosity > McVerbosityNone_c) {
1013      fprintf(vis_stdout,"\n--Converting XOR to AND and OR from:\n");
1014      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1015      fprintf(vis_stdout,"\nto\n");
1016      Ctlp_FormulaPrint(vis_stdout, tmp_formula);
1017      fprintf(vis_stdout,"\n");
1018    } 
1019    result = CoveredStatesHoskote(startstates, fsm, tmp_formula, fairStates,
1020                                  fairCondition, careStatesArray,
1021                                  earlyTermination, hintsArray,
1022                                  hintType, verbosity, dcLevel,buildOnionRing,
1023                                  GSHschedule, signalList, statesCoveredList,
1024                                  newCoveredStatesList, statesToRemoveList);
1025    mdd_free(startstates);
1026    return result;
1027    break;
1028  } 
1029  case Ctlp_EQ_c: {
1030    tmp_formula = Ctlp_FormulaConvertEQtoOR(OrigFormula);
1031    if (verbosity > McVerbosityNone_c) {
1032      fprintf(vis_stdout,"\n--Converting EQ to AND and OR from:\n");
1033      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1034      fprintf(vis_stdout,"\nto\n");
1035      Ctlp_FormulaPrint(vis_stdout, tmp_formula);
1036      fprintf(vis_stdout,"\n");
1037    } 
1038    result = CoveredStatesHoskote(startstates, fsm, tmp_formula, fairStates,
1039                                  fairCondition, careStatesArray,
1040                                  earlyTermination, hintsArray,
1041                                  hintType, verbosity, dcLevel,buildOnionRing,
1042                                  GSHschedule, signalList, statesCoveredList,
1043                                  newCoveredStatesList, statesToRemoveList);
1044    mdd_free(startstates);
1045    return result;
1046    break;
1047  }
1048  case Ctlp_OR_c:{  /*f1+f2 = !f1 -> f2 = !f2 -> f1*/
1049    mdd_t *nextstartstates, *Tb;
1050
1051    if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadLeftChild(OrigFormula))) { /*if f1 is propositional*/
1052      /* Convert f1+f2 to !f1->f2      */
1053      leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
1054      rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
1055    } else if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadRightChild(OrigFormula))) { /*if f2 is propositional*/
1056       /* Convert f1+f2 to !f2->f1      */
1057      leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
1058      rightFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
1059    } else { /*neither are propositional*/
1060      fprintf(vis_stdout,"\nCan't compute coverage of disjunctions where neither side is propositional\n");
1061      fprintf(vis_stdout,"Could not compute coverage of :");
1062      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1063      result = mdd_zero(Fsm_FsmReadMddManager(fsm));
1064      mdd_free(startstates);
1065      return result;
1066    }
1067    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
1068    Tb = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
1069                               fairCondition, careStatesArray,
1070                               earlyTermination, hintsArray, hintType,
1071                               verbosity, dcLevel, buildOnionRing,GSHschedule);
1072    Ctlp_FormulaFree(existFormula);
1073    Ctlp_FormulaFree(leftFormula);
1074    nextstartstates = mdd_and(startstates, Tb,1,1);
1075    mdd_free(Tb);
1076    Covstates1 = CoveredStatesHoskote(nextstartstates,fsm, rightFormula,
1077                                      fairStates, fairCondition, 
1078                                      careStatesArray, earlyTermination,
1079                                      hintsArray, hintType, verbosity, dcLevel,
1080                                      buildOnionRing,GSHschedule, signalList,
1081                                      statesCoveredList, newCoveredStatesList,
1082                                      statesToRemoveList);
1083    mdd_free(nextstartstates);
1084    mdd_free(startstates);
1085    return Covstates1;
1086    break;
1087  }
1088  case Ctlp_NOT_c:{ /*include code for checking for 2 NOTs*/
1089    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
1090    if (!(Ctlp_FormulaTestIsQuantifierFree(leftFormula))) {
1091      tmp_formula = Ctlp_FormulaPushNegation(leftFormula);
1092      if (verbosity > McVerbosityNone_c) {
1093        fprintf(vis_stdout,"\n--Pushing down negation one level. Converting formula from:\n");
1094        Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1095        fprintf(vis_stdout,"\nto\n");
1096        Ctlp_FormulaPrint(vis_stdout,tmp_formula);
1097        fprintf(vis_stdout,"\n");
1098      }
1099      Covstates1 = CoveredStatesHoskote(startstates, fsm, tmp_formula,
1100                                        fairStates, fairCondition, 
1101                                        careStatesArray, earlyTermination,
1102                                        hintsArray, hintType, verbosity,
1103                                        dcLevel, buildOnionRing,GSHschedule,
1104                                        signalList, statesCoveredList,
1105                                        newCoveredStatesList,
1106                                        statesToRemoveList);
1107      Ctlp_FormulaFree(tmp_formula);
1108      result = mdd_and(Covstates1,fairStates,1,1);
1109      mdd_free(Covstates1);
1110      mdd_free(startstates);
1111      return result;
1112#if 0
1113      fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL\n");
1114      fprintf(vis_stdout,"** can't compute coverage of : ");
1115      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1116      fprintf(vis_stdout,"\n");
1117      mdd_free(startstates);
1118      return mdd_zero(Fsm_FsmReadMddManager(fsm));
1119#endif
1120    } else { /*this part of the code is now never executed*/
1121      fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
1122      mdd_free(startstates);
1123      return mdd_zero(Fsm_FsmReadMddManager(fsm));
1124    }
1125    break;
1126  }
1127  case Ctlp_TRUE_c:
1128  case Ctlp_FALSE_c: {
1129    if (verbosity > McVerbosityNone_c)
1130      fprintf(vis_stdout,"No observable signal, hence no coverage\n");
1131    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
1132    mdd_free(startstates);
1133    return result;
1134    break;
1135  }
1136  case Ctlp_ID_c:{ /*should not reach here*/
1137    fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
1138    mdd_free(startstates);
1139    return mdd_zero(Fsm_FsmReadMddManager(fsm));
1140    break;
1141  }
1142  default:
1143    fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
1144    break;
1145  }
1146  assert(0);
1147  return NIL(mdd_t);
1148
1149} /* CoveredStatesHoskote */
1150
1151
1152/**Function********************************************************************
1153
1154  Synopsis    [Computes a the set of covered states for a given formula and
1155               initial set of states given. ]
1156
1157  Description [Works for a larger subset of CTL than CoveredStatesHoskote.]
1158
1159  SideEffects [Updates running totals.]
1160
1161  SeeAlso     [McEstimateCoverage CoveredStatesHoskote]
1162
1163******************************************************************************/
1164static mdd_t *
1165CoveredStatesImproved(
1166  mdd_t *startstates_old,
1167  Fsm_Fsm_t *fsm,
1168  Ctlp_Formula_t *OrigFormula,
1169  mdd_t *fairStates,
1170  Fsm_Fairness_t *fairCondition,
1171  array_t *careStatesArray,
1172  Mc_EarlyTermination_t *earlyTermination,
1173  Fsm_HintsArray_t *hintsArray,
1174  Mc_GuidedSearch_t hintType,
1175  Mc_VerbosityLevel verbosity,
1176  Mc_DcLevel dcLevel,
1177  int buildOnionRing,
1178  Mc_GSHScheduleType GSHschedule,
1179  array_t *signalList,
1180  array_t *statesCoveredList,
1181  array_t *newCoveredStatesList,
1182  array_t *statesToRemoveList)
1183{
1184  mdd_t *Covstates1, *temp1, *temp2;
1185  mdd_t *Covstates2;
1186  mdd_t *result;
1187  mdd_t *travstates;
1188  mdd_t *frstrchstates;
1189 
1190  mdd_t *startstates;
1191
1192  Ctlp_FormulaType formulaType;
1193  Ctlp_Formula_t *rightFormula, *leftFormula, *tmp_formula, *existFormula;
1194  double numresultstates; /* used for debugging <NJ> */
1195
1196  startstates = mdd_and(startstates_old,fairStates,1,1);
1197 
1198  if (mdd_is_tautology(startstates,0)) {
1199    if (verbosity > McVerbosityNone_c)
1200      fprintf(vis_stdout,
1201              "\n--Startstates are down to zero. Coverage is hence zero.\n");
1202    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
1203    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
1204                                      Fsm_FsmReadPresentStateVars(fsm));
1205    mdd_free(startstates);
1206    return result;
1207  }
1208  if (Ctlp_FormulaTestIsQuantifierFree(OrigFormula)) {
1209    /* propositional formula */
1210    result = CoveragePropositional(startstates, fsm, OrigFormula, fairStates,
1211                                   fairCondition, careStatesArray,
1212                                   earlyTermination, hintsArray, hintType,
1213                                   verbosity, dcLevel,buildOnionRing,
1214                                   GSHschedule, signalList, statesCoveredList,
1215                                   newCoveredStatesList, statesToRemoveList);
1216    temp1 = result;
1217    result = mdd_and(temp1,fairStates,1,1);
1218    mdd_free(temp1);
1219    mdd_free(startstates);
1220    return result;
1221  }
1222  formulaType = Ctlp_FormulaReadType(OrigFormula);
1223  switch (formulaType) {
1224  case Ctlp_EG_c: {/*EGp = p * EX(EGp) => C(So,EGp) = C(So,p) */
1225    if (verbosity > McVerbosityNone_c) {
1226      fprintf(vis_stdout,"\n--Computing underapproximation for EG formula:\n");
1227      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1228      fprintf(vis_stdout,"\n");
1229    }
1230    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
1231    result = CoveredStatesImproved(startstates, fsm, leftFormula, fairStates,
1232                                   fairCondition, careStatesArray,
1233                                   earlyTermination, hintsArray, hintType,
1234                                   verbosity, dcLevel,buildOnionRing,
1235                                   GSHschedule, signalList, statesCoveredList,
1236                                   newCoveredStatesList, statesToRemoveList);
1237    temp1 = result;
1238    result = mdd_and(temp1,fairStates,1,1);
1239    mdd_free(temp1);
1240    mdd_free(startstates);
1241    return result;
1242    break;
1243  }
1244  case Ctlp_EF_c: {
1245    if (verbosity > McVerbosityNone_c) {
1246      fprintf(vis_stdout,"\n--Computing underapproximation for EF formula:\n");
1247      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1248      fprintf(vis_stdout,"\n");
1249    }
1250    tmp_formula = Ctlp_FormulaConvertEFtoOR(OrigFormula);
1251    result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
1252                                   fairCondition, careStatesArray,
1253                                   earlyTermination, hintsArray,
1254                                   hintType, verbosity, dcLevel,buildOnionRing,
1255                                   GSHschedule, signalList, statesCoveredList,
1256                                   newCoveredStatesList, statesToRemoveList);
1257    Ctlp_FormulaFree(tmp_formula);
1258    mdd_free(startstates);
1259    return result;
1260    break;
1261  }
1262  case Ctlp_EU_c: {
1263    if (verbosity > McVerbosityNone_c) {
1264      fprintf(vis_stdout,"\n--Computing underapproximation for EU formula: ");
1265      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1266      fprintf(vis_stdout,"\n");
1267    }
1268    tmp_formula = Ctlp_FormulaConvertEUtoOR(OrigFormula);
1269    result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
1270                                   fairCondition, careStatesArray,
1271                                   earlyTermination, hintsArray, hintType,
1272                                   verbosity, dcLevel,buildOnionRing,
1273                                   GSHschedule, signalList, statesCoveredList,
1274                                   newCoveredStatesList,statesToRemoveList);
1275    mdd_free(startstates);
1276    return result;
1277    break;
1278  }
1279  case Ctlp_FwdU_c:
1280  case Ctlp_FwdG_c:
1281  case Ctlp_EY_c:
1282  case Ctlp_EH_c:
1283  case Ctlp_Cmp_c:
1284  case Ctlp_EX_c:
1285  case Ctlp_Init_c:  {
1286    fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL,\n");
1287    fprintf(vis_stdout,"** can't compute coverage of : ");
1288    Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1289    fprintf(vis_stdout,"\n");
1290    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
1291    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
1292                                      Fsm_FsmReadPresentStateVars(fsm));
1293    mdd_free(startstates);
1294    return result;
1295    break;
1296  }
1297  case Ctlp_AX_c:{
1298    temp1 = Mc_FsmEvaluateEYFormula(fsm, startstates, fairStates, careStatesArray, verbosity, dcLevel);
1299    Covstates1 = mdd_and(temp1,fairStates,1,1);
1300    mdd_free(temp1);
1301    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
1302    result = CoveredStatesImproved(Covstates1, fsm, leftFormula, fairStates,
1303                                   fairCondition, careStatesArray,
1304                                   earlyTermination, hintsArray, hintType,
1305                                   verbosity, dcLevel,buildOnionRing,
1306                                   GSHschedule, signalList, statesCoveredList,
1307                                   newCoveredStatesList, statesToRemoveList);
1308    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
1309                                      Fsm_FsmReadPresentStateVars(fsm));
1310    mdd_free(Covstates1);
1311    temp1 = result;
1312    result = mdd_and(temp1,fairStates,1,1);
1313    mdd_free(temp1);
1314    mdd_free(startstates);
1315    return result;
1316    break;
1317  }
1318  case Ctlp_AG_c:{
1319    double numststates;
1320    mdd_t  *initStates;
1321    initStates = Fsm_FsmComputeInitialStates(fsm);
1322    temp1 = mdd_one(Fsm_FsmReadMddManager(fsm));
1323    if (mdd_equal_mod_care_set_array(startstates,initStates,careStatesArray)) {
1324      if (verbosity > McVerbosityNone_c)
1325        fprintf(vis_stdout,"\nUsing the reachable states already computed...");
1326      temp2 = Fsm_FsmComputeReachableStates(fsm, 0, 1, 0, 0, 0, 0, 0,
1327                                            Fsm_Rch_Default_c, 0, 0,
1328                                            NIL(array_t), FALSE, NIL(array_t));
1329    } else
1330      temp2 = Mc_FsmEvaluateFwdUFormula(fsm, startstates, temp1, fairStates,
1331                                        careStatesArray, NIL(array_t),
1332                                        verbosity, dcLevel);
1333    mdd_free(initStates);
1334#if 0
1335    temp2 = McForwardReachable(fsm, startstates, temp1, fairStates,
1336                               careStatesArray, NIL(array_t),verbosity,
1337                               dcLevel);
1338#endif
1339    numststates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),startstates,
1340                                  Fsm_FsmReadPresentStateVars(fsm));
1341    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),temp2,
1342                                      Fsm_FsmReadPresentStateVars(fsm));
1343#if 0
1344    fprintf(vis_stdout,"\nNum of forward reachable states from %.0f startstates = %.0f\n",numststates,numresultstates);
1345#endif
1346    mdd_free(temp1);
1347    Covstates1 = mdd_and(temp2,fairStates,1,1);
1348    mdd_free(temp2);
1349    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
1350    result = CoveredStatesImproved(Covstates1, fsm, leftFormula, fairStates,
1351                                   fairCondition, careStatesArray,
1352                                   earlyTermination, hintsArray, hintType,
1353                                   verbosity, dcLevel, buildOnionRing,
1354                                   GSHschedule, signalList, statesCoveredList,
1355                                   newCoveredStatesList, statesToRemoveList);
1356    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
1357                                      Fsm_FsmReadPresentStateVars(fsm));
1358    mdd_free(Covstates1);
1359    temp1 = result;
1360    result = mdd_and(temp1,fairStates,1,1);
1361    mdd_free(temp1);
1362    mdd_free(startstates);
1363    return result;
1364    break;
1365  }
1366  case Ctlp_AF_c:{
1367    tmp_formula = OrigFormula;
1368    OrigFormula = Ctlp_FormulaConvertAFtoAU(tmp_formula);
1369    if (verbosity > McVerbosityNone_c) {
1370      fprintf(vis_stdout,"Converting formula from\n");
1371      Ctlp_FormulaPrint(vis_stdout,tmp_formula);
1372      fprintf(vis_stdout,"\nto\n");
1373      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1374      fprintf(vis_stdout,"\n");
1375    }
1376#if 0
1377    Ctlp_FormulaFree(tmp_formula);
1378    formulaType = Ctlp_AU_c;
1379#endif
1380    /* convert to AFp to A (TRUE) U p  and then step thru to do coverage
1381       for AU computation below*/
1382  }
1383  case Ctlp_AU_c:{
1384    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
1385    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
1386    tmp_formula = Ctlp_FormulaCreate(Ctlp_OR_c,leftFormula,rightFormula);
1387    CtlpFormulaIncrementRefCount(leftFormula);
1388    CtlpFormulaIncrementRefCount(rightFormula);
1389    travstates = traverse(fsm, fairStates, fairCondition, careStatesArray,
1390                          earlyTermination, hintsArray, hintType, verbosity,
1391                          dcLevel, buildOnionRing, GSHschedule, startstates,
1392                          leftFormula, rightFormula);
1393    if (verbosity > McVerbosityNone_c) {
1394      fprintf(vis_stdout,"\n---Computing coverage for LHS of U formula i.e: ");
1395      Ctlp_FormulaPrint(vis_stdout,leftFormula);
1396      fprintf(vis_stdout,
1397              "\n------------------------------------------------\n");
1398    }
1399    Covstates1 = CoveredStatesImproved(travstates, fsm, tmp_formula,
1400                                       fairStates, fairCondition,
1401                                       careStatesArray, earlyTermination,
1402                                       hintsArray, hintType, verbosity,
1403                                       dcLevel, buildOnionRing, GSHschedule,
1404                                       signalList, statesCoveredList,
1405                                       newCoveredStatesList,
1406                                       statesToRemoveList);
1407    mdd_free(travstates);
1408    Ctlp_FormulaFree(tmp_formula);
1409    frstrchstates = firstReached(fsm, fairStates, fairCondition,
1410                                 careStatesArray, earlyTermination, hintsArray,
1411                                 hintType, verbosity, dcLevel, buildOnionRing,
1412                                 GSHschedule,startstates,rightFormula);
1413    if (verbosity > McVerbosityNone_c) {
1414      fprintf(vis_stdout,"\n---Computing coverage for RHS of U formula i.e: ");
1415      Ctlp_FormulaPrint(vis_stdout,rightFormula);
1416      fprintf(vis_stdout,
1417              "\n------------------------------------------------\n");
1418    }
1419    Covstates2 = CoveredStatesImproved(frstrchstates, fsm, rightFormula,
1420                                       fairStates, fairCondition,
1421                                       careStatesArray, earlyTermination,
1422                                       hintsArray, hintType, verbosity,
1423                                       dcLevel, buildOnionRing, GSHschedule,
1424                                       signalList, statesCoveredList,
1425                                       newCoveredStatesList,
1426                                       statesToRemoveList);
1427    mdd_free(frstrchstates);
1428    result = mdd_or(Covstates1,Covstates2,1,1);
1429    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
1430                                      Fsm_FsmReadPresentStateVars(fsm));
1431    mdd_free(Covstates1);
1432    mdd_free(Covstates2);
1433    temp1 = result;
1434    result = mdd_and(temp1,fairStates,1,1);
1435    if (formulaType == Ctlp_AF_c)
1436      Ctlp_FormulaFree(OrigFormula);
1437    mdd_free(temp1);
1438    mdd_free(startstates);
1439    return result;
1440    break;
1441  }
1442  case Ctlp_AND_c:{
1443    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
1444    if (verbosity > McVerbosityNone_c) {
1445      fprintf(vis_stdout,"\n---Computing coverage for LHS sub-formula: ");
1446      Ctlp_FormulaPrint(vis_stdout,leftFormula);
1447      fprintf(vis_stdout,
1448              "\n------------------------------------------------\n");
1449    }
1450    Covstates1 = CoveredStatesImproved(startstates,fsm, leftFormula,
1451                                       fairStates, fairCondition, 
1452                                       careStatesArray, earlyTermination,
1453                                       hintsArray, hintType, verbosity,
1454                                       dcLevel, buildOnionRing,GSHschedule,
1455                                       signalList, statesCoveredList,
1456                                       newCoveredStatesList,
1457                                       statesToRemoveList);
1458    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
1459    if (verbosity > McVerbosityNone_c) {
1460      fprintf(vis_stdout,"\n---Computing coverage for RHS sub-formula: ");
1461      Ctlp_FormulaPrint(vis_stdout,rightFormula);
1462      fprintf(vis_stdout,
1463              "\n------------------------------------------------\n");
1464    }
1465    Covstates2 = CoveredStatesImproved(startstates,fsm, rightFormula,
1466                                       fairStates, fairCondition, 
1467                                       careStatesArray, earlyTermination,
1468                                       hintsArray, hintType, verbosity,
1469                                       dcLevel, buildOnionRing,GSHschedule,
1470                                       signalList, statesCoveredList,
1471                                       newCoveredStatesList,
1472                                       statesToRemoveList);
1473    result = mdd_or(Covstates1,Covstates2,1,1);
1474    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
1475                                      Fsm_FsmReadPresentStateVars(fsm));
1476    mdd_free(Covstates1);
1477    mdd_free(Covstates2);
1478    temp1 = result;
1479    result = mdd_and(temp1,fairStates,1,1);
1480    mdd_free(temp1);
1481    mdd_free(startstates);
1482    return result;
1483    break;
1484  }
1485  case Ctlp_THEN_c:{ /*f1 -> f2 = !f2 -> !f1*/
1486    int sigarr;
1487    array_t *listOfF2Signals = array_alloc(char *,0);
1488    array_t *listOfF1Signals = array_alloc(char *,0);
1489    array_t *newstatesToRemoveList = NIL(array_t);
1490    mdd_t *nextstartstates, *Tb, *tmp_mdd;
1491
1492    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
1493    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
1494    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
1495    Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
1496                               fairStates, fairCondition, careStatesArray,
1497                               earlyTermination, hintsArray, hintType,
1498                               verbosity, dcLevel, buildOnionRing,GSHschedule);
1499    Ctlp_FormulaFree(existFormula);
1500    nextstartstates = mdd_and(startstates, Tb,1,1);
1501    mdd_free(Tb);
1502    /*To compute C(So*T(f1),f2),    *
1503     *first compute states to remove*/
1504    newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
1505    findallsignalsInFormula(listOfF2Signals,rightFormula); /*find all signals in f2*/
1506    for (sigarr=0;sigarr<array_n(listOfF2Signals);sigarr++) {
1507      /*for all signals in f2*/
1508      mdd_t *tmp_mdd2;
1509      char *signalInF2;
1510      int positionInGlobalList;
1511      int rangeOfF2SigInF1;
1512      signalInF2 = array_fetch(char *,listOfF2Signals,sigarr);
1513      positionInGlobalList = positionOfSignalinList(signalInF2,signalList);
1514      if (positionInGlobalList < 0) /*shouldn't happen*/
1515        fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
1516      rangeOfF2SigInF1 = RangeofSignalinFormula(fsm,signalInF2,leftFormula);
1517      tmp_mdd = mdd_dup(nextstartstates);
1518      if (rangeOfF2SigInF1 > 0) { /*signal in F2 also in F1*/
1519        if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if f1 is propositional*/
1520          tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
1521                                   careStatesArray, earlyTermination,
1522                                   hintsArray, hintType, verbosity, dcLevel,
1523                                   buildOnionRing, GSHschedule, signalInF2,
1524                                   tmp_mdd);
1525          mdd_free(tmp_mdd);
1526          tmp_mdd = tmp_mdd2;
1527        }
1528        tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
1529                               positionInGlobalList);
1530        if (tmp_mdd2 != NIL(mdd_t))
1531          mdd_free(tmp_mdd2);
1532        array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
1533                     tmp_mdd);
1534      } else {
1535        mdd_free(tmp_mdd);
1536      }
1537    }
1538    Covstates1 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
1539                                       fairStates, fairCondition, 
1540                                       careStatesArray, earlyTermination,
1541                                       hintsArray, hintType, verbosity,
1542                                       dcLevel, buildOnionRing, GSHschedule,
1543                                       signalList, statesCoveredList,
1544                                       newCoveredStatesList,
1545                                       newstatesToRemoveList);
1546    mdd_free(nextstartstates);
1547    mdd_array_free(newstatesToRemoveList);
1548    array_free(listOfF2Signals);
1549    /*End of coverage computation of f2*/
1550
1551    /*Now simillar computation for !f1 *
1552     * Convert f1->f2 to !f2->!f1      */
1553    leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
1554    rightFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
1555    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
1556    Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
1557                               fairStates, fairCondition, careStatesArray,
1558                               earlyTermination, hintsArray, hintType,
1559                               verbosity, dcLevel, buildOnionRing,GSHschedule);
1560    Ctlp_FormulaFree(existFormula);
1561    nextstartstates = mdd_and(startstates, Tb, 1, 1);
1562    mdd_free(Tb);
1563    newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
1564    findallsignalsInFormula(listOfF1Signals,rightFormula);/*find all signals in !f1*/
1565    for (sigarr=0;sigarr<array_n(listOfF1Signals);sigarr++) {
1566      /*for all signals in !f1*/
1567      mdd_t *tmp_mdd2;
1568      char *signalInNotF1;
1569      int positionInGlobalList;
1570      int rangeOfNotF1SigInNotF2;
1571      signalInNotF1 = array_fetch(char *,listOfF1Signals,sigarr);
1572      positionInGlobalList = positionOfSignalinList(signalInNotF1,signalList);
1573      if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
1574      rangeOfNotF1SigInNotF2 = RangeofSignalinFormula(fsm,signalInNotF1,leftFormula);
1575      tmp_mdd = mdd_dup(nextstartstates);
1576      if (rangeOfNotF1SigInNotF2 > 0) {/*signal in !F1 also in !F2*/
1577        if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if !f2 is propositional*/
1578          tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
1579                                   careStatesArray, earlyTermination,
1580                                   hintsArray, hintType, verbosity, dcLevel,
1581                                   buildOnionRing, GSHschedule, signalInNotF1,
1582                                   tmp_mdd);
1583          mdd_free(tmp_mdd);
1584          tmp_mdd = tmp_mdd2;
1585        }
1586        tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
1587                               positionInGlobalList);
1588        if (tmp_mdd2 != NIL(mdd_t))
1589          mdd_free(tmp_mdd2);
1590        array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
1591                     tmp_mdd);
1592      } else {
1593        mdd_free(tmp_mdd);
1594      }
1595    }
1596    Ctlp_FormulaFree(leftFormula);
1597    Covstates2 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
1598                                       fairStates, fairCondition, 
1599                                       careStatesArray, earlyTermination,
1600                                       hintsArray, hintType, verbosity,
1601                                       dcLevel, buildOnionRing,GSHschedule,
1602                                       signalList, statesCoveredList,
1603                                       newCoveredStatesList,
1604                                       newstatesToRemoveList);
1605   
1606    mdd_free(nextstartstates);
1607    mdd_array_free(newstatesToRemoveList);
1608    array_free(listOfF1Signals);
1609    /*End of coverage computation of !f1*/
1610    Ctlp_FormulaFree(rightFormula);
1611    result = mdd_or(Covstates1,Covstates2,1,1);
1612    mdd_free(Covstates1);
1613    mdd_free(Covstates2);
1614    mdd_free(startstates);
1615    return result;
1616    break;
1617  }
1618  case Ctlp_XOR_c: {
1619    tmp_formula = Ctlp_FormulaConvertXORtoOR(OrigFormula);
1620    if (verbosity > McVerbosityNone_c) {
1621      fprintf(vis_stdout,"\n--Converting XOR to AND and OR from:\n");
1622      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1623      fprintf(vis_stdout,"\nto\n");
1624      Ctlp_FormulaPrint(vis_stdout, tmp_formula);
1625      fprintf(vis_stdout,"\n");
1626    } 
1627    result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
1628                                   fairCondition, careStatesArray,
1629                                   earlyTermination, hintsArray, hintType,
1630                                   verbosity, dcLevel,buildOnionRing,
1631                                   GSHschedule, signalList, statesCoveredList,
1632                                   newCoveredStatesList, statesToRemoveList);
1633    mdd_free(startstates);
1634    return result;
1635    break;
1636  }
1637  case Ctlp_EQ_c: {
1638    tmp_formula = Ctlp_FormulaConvertEQtoOR(OrigFormula);
1639    if (verbosity > McVerbosityNone_c) {
1640      fprintf(vis_stdout,"\n--Converting EQ to AND and OR");
1641      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1642      fprintf(vis_stdout,"\nto\n");
1643      Ctlp_FormulaPrint(vis_stdout, tmp_formula);
1644      fprintf(vis_stdout,"\n");
1645    } 
1646    result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
1647                                   fairCondition, careStatesArray,
1648                                   earlyTermination, hintsArray, hintType,
1649                                   verbosity, dcLevel,buildOnionRing,
1650                                   GSHschedule, signalList, statesCoveredList,
1651                                   newCoveredStatesList, statesToRemoveList);
1652    mdd_free(startstates);
1653    return result;
1654    break;
1655  }     
1656  case Ctlp_OR_c:{  /*f1+f2 = !f1 -> f2 = !f2 -> f1*/
1657    int sigarr;
1658    array_t *listOfF2Signals = array_alloc(char *,0);
1659    array_t *listOfF1Signals = array_alloc(char *,0);
1660    array_t *newstatesToRemoveList = NIL(array_t);
1661    mdd_t *nextstartstates, *Tb, *tmp_mdd;
1662   
1663    /*To compute C(So*T(!f1),f2),  *
1664     *convert to form like !f1->f2 */
1665    leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
1666    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
1667    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
1668    Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
1669                               fairStates, fairCondition, careStatesArray,
1670                               earlyTermination, hintsArray, hintType,
1671                               verbosity, dcLevel, buildOnionRing,GSHschedule);
1672    Ctlp_FormulaFree(existFormula);
1673    nextstartstates = mdd_and(startstates, Tb, 1, 1);
1674    mdd_free(Tb);
1675    /*first compute states to remove*/
1676    newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
1677    findallsignalsInFormula(listOfF2Signals,rightFormula);/*find all signals in f2*/
1678    for (sigarr=0;sigarr<array_n(listOfF2Signals);sigarr++) {
1679      /*for all signals in f2*/
1680      mdd_t *tmp_mdd2;
1681      char *signalInF2;
1682      int positionInGlobalList;
1683      int rangeOfF2SigInF1;
1684      signalInF2 = array_fetch(char *,listOfF2Signals,sigarr);
1685      positionInGlobalList = positionOfSignalinList(signalInF2,signalList);
1686      if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
1687      rangeOfF2SigInF1 = RangeofSignalinFormula(fsm,signalInF2,leftFormula);
1688      tmp_mdd = mdd_dup(nextstartstates);
1689      if (rangeOfF2SigInF1 > 0) {/*signal in F2 also in F1*/
1690        if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if f1 is propositional*/
1691          tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
1692                                   careStatesArray, earlyTermination,
1693                                   hintsArray, hintType, verbosity, dcLevel,
1694                                   buildOnionRing, GSHschedule, signalInF2,
1695                                   tmp_mdd);
1696          mdd_free(tmp_mdd);
1697          tmp_mdd = tmp_mdd2;
1698        }
1699        tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
1700                               positionInGlobalList);
1701        if (tmp_mdd2 != NIL(mdd_t))
1702          mdd_free(tmp_mdd2);
1703        array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
1704                     tmp_mdd);
1705      } else {
1706        mdd_free(tmp_mdd);
1707      }
1708    }
1709    Ctlp_FormulaFree(leftFormula);
1710    Covstates1 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
1711                                       fairStates, fairCondition, 
1712                                       careStatesArray, earlyTermination,
1713                                       hintsArray, hintType, verbosity,
1714                                       dcLevel, buildOnionRing,GSHschedule,
1715                                       signalList, statesCoveredList,
1716                                       newCoveredStatesList,
1717                                       newstatesToRemoveList);
1718    mdd_free(nextstartstates);
1719    mdd_array_free(newstatesToRemoveList);
1720    array_free(listOfF2Signals);
1721    /*End of coverage computation of f2*/
1722
1723    /*Now simillar computation for !f1 *
1724     * Convert f1+f2 to !f2->f1      */
1725    leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
1726    rightFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
1727    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
1728    Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
1729                               fairStates, fairCondition, careStatesArray,
1730                               earlyTermination, hintsArray, hintType,
1731                               verbosity, dcLevel, buildOnionRing,GSHschedule);
1732    Ctlp_FormulaFree(existFormula);
1733    nextstartstates = mdd_and(startstates, Tb,1,1);
1734    mdd_free(Tb);
1735    newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
1736    findallsignalsInFormula(listOfF1Signals,rightFormula);/*find all signals in f1*/
1737    for (sigarr=0;sigarr<array_n(listOfF1Signals);sigarr++) {
1738      /*for all signals in f1*/
1739      mdd_t *tmp_mdd2;
1740      char *signalInF1;
1741      int positionInGlobalList;
1742      int rangeOfF1SigInF2;
1743      signalInF1 = array_fetch(char *,listOfF1Signals,sigarr);
1744      positionInGlobalList = positionOfSignalinList(signalInF1,signalList);
1745      if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
1746      rangeOfF1SigInF2 = RangeofSignalinFormula(fsm,signalInF1,leftFormula);
1747      tmp_mdd = mdd_dup(nextstartstates);
1748      if (rangeOfF1SigInF2 > 0) {/*signal in !F1 also in !F2*/
1749        if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if !f2 is propositional*/
1750          tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
1751                                   careStatesArray, earlyTermination,
1752                                   hintsArray, hintType, verbosity, dcLevel,
1753                                   buildOnionRing, GSHschedule, signalInF1,
1754                                   tmp_mdd);
1755          mdd_free(tmp_mdd);
1756          tmp_mdd = tmp_mdd2;
1757        }
1758        tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
1759                               positionInGlobalList);
1760        if (tmp_mdd2 != NIL(mdd_t))
1761          mdd_free(tmp_mdd2);
1762        array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
1763                     tmp_mdd);
1764      } else {
1765        mdd_free(tmp_mdd);
1766      }
1767    }
1768    Ctlp_FormulaFree(leftFormula);
1769    Covstates2 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
1770                                       fairStates, fairCondition, 
1771                                       careStatesArray, earlyTermination,
1772                                       hintsArray, hintType, verbosity,
1773                                       dcLevel, buildOnionRing,GSHschedule,
1774                                       signalList, statesCoveredList,
1775                                       newCoveredStatesList,
1776                                       newstatesToRemoveList);
1777    mdd_free(nextstartstates);
1778    mdd_array_free(newstatesToRemoveList);
1779    array_free(listOfF1Signals);
1780    /*End of coverage computation of !f1*/
1781   
1782    result = mdd_or(Covstates1,Covstates2,1,1);
1783    mdd_free(Covstates1);
1784    mdd_free(Covstates2);
1785    mdd_free(startstates);
1786    return result;
1787    break;
1788  }
1789  case Ctlp_NOT_c:{ /*include code for checking for 2 NOTs*/
1790    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
1791    if (!(Ctlp_FormulaTestIsQuantifierFree(leftFormula))) {
1792      tmp_formula = Ctlp_FormulaPushNegation(leftFormula);
1793      if (verbosity > McVerbosityNone_c) {
1794        fprintf(vis_stdout,"\n--Pushing down negation one level. Converting formula from:\n");
1795        Ctlp_FormulaPrint(vis_stdout,OrigFormula);
1796        fprintf(vis_stdout,"\nto\n");
1797        Ctlp_FormulaPrint(vis_stdout,tmp_formula);
1798        fprintf(vis_stdout,"\n");
1799      }
1800      Covstates1 = CoveredStatesImproved(startstates,fsm, tmp_formula,
1801                                         fairStates, fairCondition, 
1802                                         careStatesArray, earlyTermination,
1803                                         hintsArray, hintType, verbosity,
1804                                         dcLevel, buildOnionRing,GSHschedule,
1805                                         signalList, statesCoveredList,
1806                                         newCoveredStatesList,
1807                                         statesToRemoveList);
1808      result = mdd_and(Covstates1,fairStates,1,1);
1809      Ctlp_FormulaFree(tmp_formula);
1810      mdd_free(Covstates1);
1811      mdd_free(startstates);
1812      return result;
1813    } else { /*this part of the code is now never executed*/
1814       fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
1815       mdd_free(startstates);
1816       return mdd_zero(Fsm_FsmReadMddManager(fsm));
1817    }
1818    break;
1819  }
1820  case Ctlp_TRUE_c:
1821  case Ctlp_FALSE_c: {
1822    if (verbosity > McVerbosityNone_c)
1823      fprintf(vis_stdout,"No observable signal, hence no coverage\n");
1824    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
1825    mdd_free(startstates);
1826    return result;
1827    break;
1828  }
1829  case Ctlp_ID_c:{ /*should not reach here*/
1830    fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
1831    mdd_free(startstates);
1832    return mdd_zero(Fsm_FsmReadMddManager(fsm));
1833    break;
1834  }
1835  default:
1836    fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
1837    mdd_free(startstates);
1838    break;
1839  }
1840  assert(0);
1841  return NIL(mdd_t);
1842
1843} /* End of CoveredStatesImproved */
1844
1845
1846/**Function********************************************************************
1847
1848  Synopsis    [Computes the coverage for propositional formulae]
1849
1850  Description []
1851
1852  SideEffects [none]
1853
1854  SeeAlso     [CoveredStatesImproved CoveredStatesHoskote]
1855 
1856******************************************************************************/
1857static mdd_t *
1858CoveragePropositional(
1859  mdd_t *startstates_old,
1860  Fsm_Fsm_t *fsm,
1861  Ctlp_Formula_t *OrigFormula,
1862  mdd_t *fairStates,
1863  Fsm_Fairness_t *fairCondition,
1864  array_t *careStatesArray,
1865  Mc_EarlyTermination_t *earlyTermination,
1866  Fsm_HintsArray_t *hintsArray,
1867  Mc_GuidedSearch_t hintType,
1868  Mc_VerbosityLevel verbosity,
1869  Mc_DcLevel dcLevel,
1870  int buildOnionRing,
1871  Mc_GSHScheduleType GSHschedule,
1872  array_t *signalList,
1873  array_t *statesCoveredList,
1874  array_t *newCoveredStatesList,
1875  array_t *statesToRemoveList)
1876{
1877  mdd_t *Tb, *result;
1878  mdd_t *startstates;
1879  array_t *listOfSignals = array_alloc(char *,0);
1880  int i,positionInList;
1881  char *signal;
1882  Ctlp_Formula_t *tmpFormula;
1883 
1884  result = mdd_zero(Fsm_FsmReadMddManager(fsm));
1885  findallsignalsInFormula(listOfSignals,OrigFormula);
1886  if (array_n(listOfSignals)==0) {
1887    if (verbosity > McVerbosityNone_c)
1888      fprintf(vis_stdout,"No observable signals, hence no coverage\n");
1889    array_free(listOfSignals);
1890    return result;
1891  }
1892  /*else*/
1893  startstates = mdd_and(startstates_old,fairStates,1,1);
1894  tmpFormula = Ctlp_FormulaConvertToExistentialForm(OrigFormula);
1895  Tb = Mc_FsmEvaluateFormula(fsm, tmpFormula, fairStates,
1896                             fairCondition, careStatesArray, earlyTermination, 
1897                             hintsArray, hintType, verbosity, dcLevel,
1898                             buildOnionRing,GSHschedule);
1899  Ctlp_FormulaFree(tmpFormula);
1900  for (i=0;i<array_n(listOfSignals);i++) {
1901    mdd_t *statesCovered, *newCoveredStates, *statesToRemove, *CovStates, *tmp_mdd, *tmp_mdd2;
1902    signal = array_fetch(char *,listOfSignals,i);
1903    positionInList = positionOfSignalinList(signal,signalList);
1904    if (positionInList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
1905    statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList);
1906    newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList);
1907    statesToRemove = array_fetch(mdd_t *,statesToRemoveList,positionInList);
1908    CovStates = computedependHoskote(fsm, OrigFormula, fairStates,
1909                                     fairCondition, careStatesArray,
1910                                     earlyTermination, hintsArray,
1911                                     hintType, verbosity, dcLevel,
1912                                     buildOnionRing, GSHschedule,
1913                                     startstates, signal, Tb, statesCovered,
1914                                     newCoveredStates,statesToRemove);
1915    tmp_mdd = mdd_or(newCoveredStates,CovStates,1,1);
1916    mdd_free(newCoveredStates);
1917    array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd);/*update newCoveredStatesList*/
1918    tmp_mdd2 = result;
1919    result = mdd_or(tmp_mdd2,CovStates,1,1);
1920    mdd_free(tmp_mdd2);
1921    mdd_free(CovStates);
1922  }
1923  mdd_free(Tb);
1924  mdd_free(startstates);
1925  array_free(listOfSignals);
1926  return result;
1927} /* CoveragePropositional */
1928
1929
1930/**Function********************************************************************
1931
1932  Synopsis    [Computes the following for use in coverage computation for
1933               propositional formulae:
1934
1935               computedepend = T(b) ^ T(!b|q->!q)
1936              where,
1937                  T(f) => Set of states satisfying f
1938                  b is a propositional formula
1939                  q is an observed signal]
1940
1941  Description []
1942
1943  SideEffects [none]
1944
1945  SeeAlso     [computedependHoskote]
1946
1947******************************************************************************/
1948static mdd_t *
1949computedepend(
1950  Fsm_Fsm_t *fsm,
1951  Ctlp_Formula_t *formula,
1952  mdd_t *fairStates,
1953  Fsm_Fairness_t *fairCondition,
1954  array_t *careStatesArray,
1955  Mc_EarlyTermination_t *earlyTermination,
1956  Fsm_HintsArray_t *hintsArray,
1957  Mc_GuidedSearch_t hintType,
1958  Mc_VerbosityLevel verbosity,
1959  Mc_DcLevel dcLevel,
1960  int buildOnionRing,
1961  Mc_GSHScheduleType GSHschedule,
1962  char *signal,
1963  mdd_t *SoAndTb_old)     
1964{
1965  mdd_t *TnotBnotQ, *Covstates, *SoAndTb;
1966  Ctlp_Formula_t *convertedformula, *tmp_formula, *existFormula;
1967  SoAndTb = mdd_and(SoAndTb_old,fairStates,1,1); 
1968  convertedformula = FormulaConvertSignalComplement(fsm,signal,formula);
1969  if (convertedformula != NIL(Ctlp_Formula_t)) {
1970    tmp_formula = Ctlp_FormulaConverttoComplement(convertedformula);
1971    existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
1972    TnotBnotQ =  Mc_FsmEvaluateFormula(fsm, existFormula,
1973                                       fairStates, fairCondition,
1974                                       careStatesArray, earlyTermination,
1975                                       hintsArray, hintType, verbosity,
1976                                       dcLevel, buildOnionRing,GSHschedule);
1977    Ctlp_FormulaFree(existFormula);
1978    Ctlp_FormulaFree(tmp_formula);
1979  } else {
1980    TnotBnotQ = mdd_zero(Fsm_FsmReadMddManager(fsm));
1981  }
1982  Ctlp_FormulaFree(convertedformula);
1983  Covstates = mdd_and(SoAndTb,TnotBnotQ,1,1); /*covered states*/
1984  mdd_free(SoAndTb);
1985  mdd_free(TnotBnotQ);
1986  return Covstates;
1987} /* computedepend */
1988
1989
1990/**Function********************************************************************
1991
1992  Synopsis    [Computes the following for use in coverage computation for
1993               propositional formulae:
1994
1995               computedepend = T(b) ^ T(!b|q->!q)
1996              where,
1997                  T(f) => Set of states satisfying f
1998                  b is a propositional formula
1999                  q is an observed signal]
2000
2001  Description []
2002
2003  SideEffects [none]
2004
2005  SeeAlso     [computedepend]
2006 
2007******************************************************************************/
2008static mdd_t *
2009computedependHoskote(
2010  Fsm_Fsm_t *fsm,
2011  Ctlp_Formula_t *formula,
2012  mdd_t *fairStates,
2013  Fsm_Fairness_t *fairCondition,
2014  array_t *careStatesArray,
2015  Mc_EarlyTermination_t *earlyTermination,
2016  Fsm_HintsArray_t *hintsArray,
2017  Mc_GuidedSearch_t hintType,
2018  Mc_VerbosityLevel verbosity,
2019  Mc_DcLevel dcLevel,
2020  int buildOnionRing,
2021  Mc_GSHScheduleType GSHschedule,
2022  mdd_t *startstates_old,
2023  char *signal,
2024  mdd_t *Tb,
2025  mdd_t *statesCovered,
2026  mdd_t *newCoveredStates,
2027  mdd_t *statesToRemove)     
2028{
2029  mdd_t *TnotBnotQ,*Covstates,*startstates,*tmp_mdd, *newCovstates;
2030  Ctlp_Formula_t *convertedformula;
2031  startstates = mdd_and(startstates_old,fairStates,1,1); 
2032  convertedformula = FormulaConvertSignalComplement(fsm,signal,formula);
2033
2034  if (convertedformula != NIL(Ctlp_Formula_t)) {
2035    Ctlp_Formula_t *tmp_formula, *tmp_formula2;
2036    tmp_formula = Ctlp_FormulaConverttoComplement(convertedformula);
2037    Ctlp_FormulaFree(convertedformula);
2038    tmp_formula2 = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
2039    Ctlp_FormulaFree(tmp_formula);
2040    TnotBnotQ =  Mc_FsmEvaluateFormula(fsm, tmp_formula2, 
2041                                       fairStates, fairCondition,
2042                                       careStatesArray, earlyTermination,
2043                                       hintsArray, hintType, verbosity,
2044                                       dcLevel, buildOnionRing,GSHschedule);
2045    Ctlp_FormulaFree(tmp_formula2);
2046  } else {
2047    TnotBnotQ = mdd_zero(Fsm_FsmReadMddManager(fsm));
2048  }
2049 
2050  tmp_mdd = mdd_and(Tb,TnotBnotQ,1,1);
2051  mdd_free(TnotBnotQ);
2052  Covstates = mdd_and(startstates,tmp_mdd,1,1); /*covered states*/
2053  mdd_free(tmp_mdd);
2054  tmp_mdd = Covstates;
2055  mdd_free(startstates);
2056  Covstates = mdd_and(Covstates, statesToRemove,1,0); /*remove the states to remove*/
2057  mdd_free(tmp_mdd);
2058  tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1);
2059  newCovstates = mdd_and(Covstates,tmp_mdd,1,0); /* newly covered states*/
2060  mdd_free(tmp_mdd);
2061#if 0
2062  fprintf(vis_stdout,"States covered w.r.t. %s = %0.f , new = %0.f\n",signal,
2063            mdd_count_onset(Fsm_FsmReadMddManager(fsm),Covstates,
2064                            Fsm_FsmReadPresentStateVars(fsm)),
2065            mdd_count_onset(Fsm_FsmReadMddManager(fsm),newCovstates,
2066                            Fsm_FsmReadPresentStateVars(fsm)));
2067#endif
2068  mdd_free(newCovstates); 
2069  return Covstates;
2070
2071} /* computedependHoskote */
2072
2073
2074/**Function********************************************************************
2075
2076  Synopsis    [Computes the following for use in coverage computation for AU:
2077              traverse(So,f1,f2) = newstartstates(So) U
2078                                     traverse(EY(newstartstates(So)),f1,f2)
2079               (see function newstartstates for its definition ]
2080
2081  Description []
2082
2083  SideEffects []
2084
2085  SeeAlso     [newstartstates]
2086
2087******************************************************************************/
2088static mdd_t *
2089traverse(
2090  Fsm_Fsm_t *fsm,
2091  mdd_t *fairStates,
2092  Fsm_Fairness_t *fairCondition,
2093  array_t *careStatesArray,
2094  Mc_EarlyTermination_t *earlyTermination,
2095  Fsm_HintsArray_t *hintsArray,
2096  Mc_GuidedSearch_t hintType,
2097  Mc_VerbosityLevel verbosity,
2098  Mc_DcLevel dcLevel,
2099  int buildOnionRing,
2100  Mc_GSHScheduleType GSHschedule,
2101  mdd_t *startstates,
2102  Ctlp_Formula_t *formula1,
2103  Ctlp_Formula_t *formula2)
2104{
2105  mdd_t *temp_mdd,*newSo, *Tf1_and_Tnotf2, *newStates, *oldStates, *Tf1, *Tnotf2;
2106  Ctlp_Formula_t *tmp_formula, *existFormula;
2107  int travcnt;
2108  oldStates = mdd_zero(Fsm_FsmReadMddManager(fsm));
2109  newStates = mdd_zero(Fsm_FsmReadMddManager(fsm));
2110  newSo = mdd_dup(startstates);
2111  existFormula = Ctlp_FormulaConvertToExistentialForm(formula1);
2112  Tf1 = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
2113                              fairCondition, careStatesArray,
2114                              earlyTermination, hintsArray,
2115                              hintType, verbosity, dcLevel,
2116                              buildOnionRing,GSHschedule);
2117  Ctlp_FormulaFree(existFormula);
2118  tmp_formula = Ctlp_FormulaConverttoComplement(formula2);
2119  existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
2120  Tnotf2 = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates, fairCondition,
2121                                 careStatesArray, earlyTermination, hintsArray,
2122                                 hintType, verbosity, dcLevel,
2123                                 buildOnionRing, GSHschedule);
2124  Ctlp_FormulaFree(existFormula);
2125  Ctlp_FormulaFree(tmp_formula);
2126  temp_mdd = mdd_and(Tf1,Tnotf2,1,1);
2127  mdd_free(Tf1);
2128  mdd_free(Tnotf2);
2129  Tf1_and_Tnotf2 = mdd_and(temp_mdd,fairStates,1,1);
2130  mdd_free(temp_mdd);
2131  temp_mdd = newSo;
2132  newSo = mdd_and(temp_mdd,Tf1_and_Tnotf2,1,1);
2133  mdd_free(temp_mdd);
2134  temp_mdd = newStates;
2135  newStates = mdd_or(temp_mdd,newSo,1,1);
2136  mdd_free(temp_mdd);
2137  travcnt = 0;
2138  while (!(mdd_equal_mod_care_set_array(newStates,oldStates,careStatesArray))) {
2139    mdd_t *tmp_mdd = oldStates;
2140    oldStates = mdd_or(tmp_mdd,newStates,1,1);
2141    mdd_free(tmp_mdd);
2142    tmp_mdd = newSo;
2143    newSo = Mc_FsmEvaluateEYFormula(fsm, tmp_mdd, fairStates, careStatesArray, verbosity, dcLevel);
2144    mdd_free(tmp_mdd);
2145    tmp_mdd = newSo;
2146    newSo = mdd_and(tmp_mdd,Tf1_and_Tnotf2,1,1);
2147    mdd_free(tmp_mdd);
2148    tmp_mdd = newStates;
2149    newStates = mdd_or(tmp_mdd,newSo,1,1);
2150    mdd_free(tmp_mdd);
2151  }
2152  mdd_free(oldStates);
2153  mdd_free(newSo);
2154  mdd_free(Tf1_and_Tnotf2);
2155  return newStates;
2156
2157} /* traverse */
2158
2159
2160/**Function********************************************************************
2161
2162  Synopsis    [Computes the following for use in coverage computation for AU:
2163              firstReached(So,f2) = (So ^ T(f2)) U
2164                                     firstReached(EY(So^T(!f2)),f2)
2165              where,
2166                  T(f2) => Set of states satisfying f2 ]
2167
2168  Description []
2169
2170  SideEffects []
2171
2172  SeeAlso     []
2173
2174******************************************************************************/
2175static mdd_t *
2176firstReached(
2177  Fsm_Fsm_t *fsm,
2178  mdd_t *fairStates,
2179  Fsm_Fairness_t *fairCondition,
2180  array_t *careStatesArray,
2181  Mc_EarlyTermination_t *earlyTermination,
2182  Fsm_HintsArray_t *hintsArray,
2183  Mc_GuidedSearch_t hintType,
2184  Mc_VerbosityLevel verbosity,
2185  Mc_DcLevel dcLevel,
2186  int buildOnionRing,
2187  Mc_GSHScheduleType GSHschedule,
2188  mdd_t *startstates,
2189  Ctlp_Formula_t *formula)
2190{
2191  int frstcnt;
2192  mdd_t *temp1, *temp2, *oldSo, *CovStates, *Tf2, *Tnotf2, *zeroMDD;
2193  Ctlp_Formula_t *tmp_formula, *existFormula;
2194  oldSo = mdd_dup(startstates);
2195  zeroMDD = mdd_zero(Fsm_FsmReadMddManager(fsm));
2196  existFormula = Ctlp_FormulaConvertToExistentialForm(formula);
2197  Tf2 =  Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
2198                               fairCondition, careStatesArray,
2199                               earlyTermination, hintsArray,
2200                               hintType, verbosity,
2201                               dcLevel, buildOnionRing, GSHschedule);
2202  Ctlp_FormulaFree(existFormula);
2203  tmp_formula = Ctlp_FormulaConverttoComplement(formula);
2204  existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
2205  Tnotf2 = Mc_FsmEvaluateFormula(fsm, existFormula,
2206                                 fairStates, fairCondition, 
2207                                 careStatesArray,earlyTermination, 
2208                                 hintsArray, hintType, verbosity, 
2209                                 dcLevel, buildOnionRing,GSHschedule);
2210  Ctlp_FormulaFree(existFormula);
2211  Ctlp_FormulaFree(tmp_formula);
2212  CovStates = mdd_and(oldSo,Tf2,1,1);
2213  temp1 = mdd_dup(oldSo);
2214  temp2 = mdd_and(oldSo,Tnotf2,1,1);
2215  frstcnt = 0;
2216  while (!(mdd_equal_mod_care_set_array(temp2,zeroMDD,careStatesArray))) {
2217    mdd_t *tmp_mdd1, *tmp_mdd2, *tmp_mdd;
2218    tmp_mdd = Mc_FsmEvaluateEYFormula(fsm, temp2, fairStates, careStatesArray, verbosity, dcLevel); /*forward(So^Tnotf2)*/
2219    tmp_mdd2 = mdd_and(tmp_mdd,Tf2,1,1);
2220    tmp_mdd1 = CovStates;
2221    CovStates = mdd_or(CovStates,tmp_mdd2,1,1); /*add on the new states*/
2222    mdd_free(tmp_mdd1);
2223    mdd_free(tmp_mdd2);
2224    tmp_mdd1 = mdd_and(tmp_mdd,Tnotf2,1,1); /*newSo^Tnotf2*/
2225    tmp_mdd2 = temp2;
2226    temp2 = mdd_and(tmp_mdd1,temp1,1,0); /*take out the startstates already encountered temp2 = newSo*/
2227    mdd_free(tmp_mdd2);
2228    mdd_free(tmp_mdd1);
2229    tmp_mdd1 = temp1;
2230    temp1 = mdd_or(temp1,tmp_mdd,1,1);
2231    mdd_free(tmp_mdd1);
2232    mdd_free(tmp_mdd);
2233  }
2234  mdd_free(zeroMDD);
2235  mdd_free(oldSo);
2236  mdd_free(Tf2);
2237  mdd_free(Tnotf2);
2238  mdd_free(temp1);
2239  mdd_free(temp2);
2240  return CovStates;
2241
2242} /* firstreached */
2243
2244
2245/**Function********************************************************************
2246
2247  Synopsis    [Duplicates a CTL formula but with a given signal's value
2248  complemented]
2249
2250  Description []
2251
2252  SideEffects [none]
2253
2254  SeeAlso     []
2255
2256******************************************************************************/
2257static Ctlp_Formula_t *
2258FormulaConvertSignalComplement(
2259  Fsm_Fsm_t *fsm,
2260  char *signal,
2261  Ctlp_Formula_t *formula)
2262{
2263  Ctlp_Formula_t *result = NIL(Ctlp_Formula_t);
2264  Ctlp_Formula_t *leftChildConverted, *leftFormula;
2265  Ctlp_Formula_t *rightChildConverted, *rightFormula;
2266  Ntk_Network_t *network;
2267  char *nodeNameString;
2268  char *nodeValueString;
2269  Ntk_Node_t *node;
2270  Var_Variable_t *nodeVar;
2271
2272  if ( formula == NIL(Ctlp_Formula_t)) {
2273        return NIL(Ctlp_Formula_t);
2274  }
2275
2276  if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c )  {
2277    leftFormula = Ctlp_FormulaReadLeftChild(formula);
2278    leftChildConverted = FormulaConvertSignalComplement(fsm, signal,
2279                                                        leftFormula);
2280    rightFormula = Ctlp_FormulaReadRightChild(formula);
2281    rightChildConverted = FormulaConvertSignalComplement(fsm, signal,
2282                                                         rightFormula);
2283    result = Ctlp_FormulaCreate(Ctlp_FormulaReadType(formula),
2284                                leftChildConverted,rightChildConverted);
2285  }
2286  else { /* if atomic proposition*/
2287    network = Fsm_FsmReadNetwork(fsm);
2288    nodeNameString = Ctlp_FormulaReadVariableName(formula);
2289    nodeValueString = Ctlp_FormulaReadValueName(formula);
2290    node = Ntk_NetworkFindNodeByName(network, nodeNameString);
2291    nodeVar = Ntk_NodeReadVariable(node);
2292    if ((strcmp(signal,nodeNameString)) != 0) { /* not the signal that we want to flip */
2293      result = Ctlp_FormulaCreate(Ctlp_FormulaReadType(formula),
2294                                  (Ctlp_Formula_t *) util_strsav(nodeNameString),
2295                                  (Ctlp_Formula_t *) util_strsav(nodeValueString));
2296    }
2297    else { /* this is the signal that we want to flip */
2298      result  = Ctlp_FormulaConverttoComplement(formula);
2299    }
2300  }
2301  return result;
2302} /* FormulaConvertSignalComplement */
2303
2304
2305/**Function********************************************************************
2306
2307  Synopsis    [Used in the coverage code to gather all possible observable
2308               signals in a given formula and create necessary arrays]
2309
2310  Description []
2311
2312  SideEffects []
2313
2314  SeeAlso     []
2315
2316******************************************************************************/
2317static void
2318findallsignals(
2319  Fsm_Fsm_t *fsm,
2320  array_t *signalTypeList,
2321  array_t *signalList,
2322  array_t *statesCoveredList,
2323  array_t *newCoveredStatesList,
2324  array_t *statesToRemoveList,
2325  Ctlp_Formula_t *formula,
2326  mdd_t *zeroMdd)
2327{
2328  Ntk_Network_t *network;
2329  Ntk_Node_t *node;
2330  Var_Variable_t *nodeVar;
2331  char *nodeNameString;
2332  int signalType;
2333  Ctlp_Formula_t *leftFormula, *rightFormula;
2334  if ( formula == NIL(Ctlp_Formula_t)) {
2335        return;
2336  }
2337
2338  if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c )  {
2339    leftFormula = Ctlp_FormulaReadLeftChild(formula);
2340    rightFormula = Ctlp_FormulaReadRightChild(formula);
2341    findallsignals(fsm, signalTypeList, signalList, statesCoveredList,
2342                   newCoveredStatesList, statesToRemoveList,
2343                   leftFormula, zeroMdd);
2344    findallsignals(fsm, signalTypeList, signalList, statesCoveredList,
2345                   newCoveredStatesList, statesToRemoveList,
2346                   rightFormula,zeroMdd);
2347  }
2348  else { /* atomic proposition */
2349    nodeNameString = Ctlp_FormulaReadVariableName(formula);
2350    if ((positionOfSignalinList(nodeNameString,signalList)) == -1) {
2351      fprintf(vis_stdout,"Found new signal = %s\n",nodeNameString);
2352      network = Fsm_FsmReadNetwork(fsm);
2353      node = Ntk_NetworkFindNodeByName(network, nodeNameString);
2354      nodeVar = Ntk_NodeReadVariable(node);
2355      if (Var_VariableTestIsPI(nodeVar))
2356        signalType = 1;
2357      else if (Var_VariableTestIsPO(nodeVar))
2358        signalType = 0;
2359      else
2360        signalType = 2;
2361      array_insert_last(int,signalTypeList,signalType);
2362      array_insert_last(char *,signalList,nodeNameString);
2363      array_insert_last(mdd_t *,statesCoveredList,mdd_dup(zeroMdd));
2364      array_insert_last(mdd_t *,newCoveredStatesList,mdd_dup(zeroMdd));
2365      array_insert_last(mdd_t *,statesToRemoveList,mdd_dup(zeroMdd));
2366    }
2367  }
2368  return;
2369} /* findallsignals */
2370
2371
2372/**Function********************************************************************
2373
2374  Synopsis    [Used in the coverage code to gather all possible observable
2375               signals in a given formula]
2376
2377  Description []
2378
2379  SideEffects []
2380
2381  SeeAlso     []
2382
2383******************************************************************************/
2384static void
2385findallsignalsInFormula(
2386  array_t *signalList,
2387  Ctlp_Formula_t *formula)
2388{
2389  char *nodeNameString;
2390
2391  Ctlp_Formula_t *leftFormula, *rightFormula;
2392  if ( formula == NIL(Ctlp_Formula_t)) {
2393    return;
2394  }
2395
2396  if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c )  {
2397    leftFormula = Ctlp_FormulaReadLeftChild(formula);
2398    rightFormula = Ctlp_FormulaReadRightChild(formula);
2399    findallsignalsInFormula(signalList,leftFormula);
2400    findallsignalsInFormula(signalList,rightFormula);
2401  }
2402  else { /* atomic proposition */
2403    nodeNameString = Ctlp_FormulaReadVariableName(formula);
2404    if ((positionOfSignalinList(nodeNameString,signalList)) == -1) {
2405      array_insert_last(char *,signalList,nodeNameString); 
2406    }
2407  }
2408  return;
2409} /* findallsignalsInFormula */
2410
2411
2412/**Function********************************************************************
2413
2414  Synopsis    [Used in the coverage code to find the index of a signal in an
2415               array of signals previously collected]
2416
2417  Description []
2418
2419  SideEffects []
2420
2421  SeeAlso     []
2422
2423******************************************************************************/
2424static int
2425positionOfSignalinList(
2426  char *signal,
2427  array_t *signalList)
2428{
2429  int arraysize = array_n(signalList);
2430  int i;
2431
2432  for (i=0;i<arraysize;i++) {
2433    if (strcmp(signal,array_fetch(char *,signalList,i)) == 0)
2434      return i;
2435  }
2436  return -1;
2437} /* positionOfSignalinList */
2438
2439
2440/**Function********************************************************************
2441
2442  Synopsis    [Finds the range of values that a given observed signal can take
2443               in a CTL formula]
2444
2445  Description []
2446
2447  SideEffects []
2448
2449  SeeAlso     []
2450
2451******************************************************************************/
2452static int
2453RangeofSignalinFormula(
2454  Fsm_Fsm_t *fsm,
2455  char *signal,
2456  Ctlp_Formula_t *formula)
2457{
2458  Ntk_Network_t *network;
2459  char *nodeNameString;
2460  char *nodeValueString;
2461  Ntk_Node_t *node;
2462  Ctlp_Formula_t *leftFormula;
2463  Ctlp_Formula_t *rightFormula;
2464 
2465  Var_Variable_t *nodeVar;
2466  int range_left,range_right;
2467  int range = 0;
2468  /*nodeVar = Ntk_NodeReadVariable(node);*/
2469 
2470  if ( formula == NIL(Ctlp_Formula_t)) {
2471    return range;
2472  }
2473
2474  if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c )  {
2475    leftFormula = Ctlp_FormulaReadLeftChild(formula);
2476    range_left = RangeofSignalinFormula(fsm, signal, leftFormula);
2477#if 0
2478    Ctlp_FormulaFree(leftFormula);
2479#endif
2480    rightFormula = Ctlp_FormulaReadRightChild (formula);
2481    range_right = RangeofSignalinFormula(fsm, signal, rightFormula);
2482#if 0
2483    Ctlp_FormulaFree(rightFormula);
2484#endif
2485    if (range_left==range_right) /* to avoid situation where signal exists on both sides of formula*/
2486      range = range_left;
2487    else
2488      range = range_right+range_left; /* 0 + some value */
2489  }
2490  else {
2491    network = Fsm_FsmReadNetwork(fsm);
2492    nodeNameString = Ctlp_FormulaReadVariableName(formula);
2493    nodeValueString = Ctlp_FormulaReadValueName(formula);
2494    node = Ntk_NetworkFindNodeByName(network, nodeNameString);
2495    nodeVar = Ntk_NodeReadVariable(node);
2496    if ((strcmp(signal,nodeNameString)) != 0) { 
2497      range = 0;
2498    }
2499    else { 
2500      range = Var_VariableReadNumValues(nodeVar);
2501    }
2502  }
2503  return range;
2504} /* RangeofSignalinFormula */
Note: See TracBrowser for help on using the repository browser.