/**CFile***********************************************************************

  FileName    [mcCover.c]

  PackageName [mc]

  Synopsis    [Functions for coverage estimation.]

  Description [This file contains the functions implementing coverage
  estimation for CTL.  According to the proposal of Hoskote et al. (DAC99)
  a state is covered by a passing property with respect to an observable
  binary signal if flipping the value of the signal at that state causes
  the property to fail.  Hoskote et al. proposed an algorithm for the
  estimation of coverage for a subset of ACTL loosely based on this
  definition of coverage.<p>
  This file contains an implementation of Hoskote's algorithm as well as an
  implementation of the improved algorithm by Jayakumar et al. presented
  at DAC2003.  The improved algorithm deals with a larger subset of CTL and
  provides more accurate estimates.]

  SeeAlso     [mcMc.c]

  Author      [Nikhil Jayakumar]

  Copyright   [Copyright (c) 2002-2005, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]

******************************************************************************/

#include "ctlpInt.h"
#include "mcInt.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] UNUSED = "$Id: mcCover.c,v 1.4 2005/05/15 07:32:10 fabio Exp $";
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static 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);
static 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);
static 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);
static 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);
static 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);
static 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);
static 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);
static Ctlp_Formula_t * FormulaConvertSignalComplement(Fsm_Fsm_t *fsm, char *signal, Ctlp_Formula_t *formula);
static 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);
static void findallsignalsInFormula(array_t *signalList, Ctlp_Formula_t *formula);
static int positionOfSignalinList(char *signal, array_t *signalList);
static int RangeofSignalinFormula(Fsm_Fsm_t *fsm, char *signal, Ctlp_Formula_t *formula);

/**AutomaticEnd***************************************************************/

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Estimate coverage of one CTL formula.]

  Description [Depending on the options, this function applies either
  the original algorithm of Hoskote et al. or the improved algorithm of
  Jayakumar et al..  It then prints statistics on coverage (if the formula
  passes).]

  SideEffects [Updates running totals]

  SeeAlso     [CommandMc CoveredStatesHoskote CoveredStatesImproved
  McPrintCoverageSummary]

******************************************************************************/
void
McEstimateCoverage(
  Fsm_Fsm_t *modelFsm,
  Ctlp_Formula_t *ctlFormula,
  int i,
  mdd_t *fairStates,
  Fsm_Fairness_t *fairCond,
  array_t *modelCareStatesArray,
  Mc_EarlyTermination_t *earlyTermination,
  array_t *hintsStatesArray,
  Mc_GuidedSearch_t guidedSearchType,
  Mc_VerbosityLevel verbosity,
  Mc_DcLevel dcLevel,
  int buildOnionRings,
  Mc_GSHScheduleType GSHschedule,
  Mc_FwdBwdAnalysis traversalDirection,
  mdd_t *modelInitialStates,
  mdd_t *ctlFormulaStates,
  mdd_t **totalcoveredstates,
  array_t *signalTypeList,
  array_t *signalList,
  array_t *statesCoveredList,
  array_t *newCoveredStatesList,
  array_t *statesToRemoveList,
  boolean performCoverageHoskote,
  boolean performCoverageImproved)
{
  double numtotcoveredstates;
  double numnewcoveredstates;
  mdd_t *CovstatesHoskote;
  mdd_t *CovstatesImproved;
  Ctlp_Formula_t *origFormula;

  if (performCoverageHoskote &&
      (modelCareStatesArray != NIL(array_t))) { /* and no errors till now? */
    mdd_t *tmp_mdd, *zero_mdd;
    int sigarr;
    array_t *listOfSignals = array_alloc(char *,0);
    origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
    if ( ( (traversalDirection == McFwd_c) && bdd_is_tautology(ctlFormulaStates, 1) ) ||
	 mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1) ) { /* formula passes */

      if (*totalcoveredstates == NIL(mdd_t))
	*totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));

      /* add new signals if any found */
      zero_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
      findallsignals(modelFsm, signalTypeList, signalList,
		     statesCoveredList, newCoveredStatesList,
		     statesToRemoveList, origFormula,
		     zero_mdd);
      mdd_free(zero_mdd);
      fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
      fprintf(vis_stdout,"===================================\n");

      CovstatesHoskote = CoveredStatesHoskote(modelInitialStates,
					      modelFsm, origFormula,
					      fairStates, fairCond,
					      modelCareStatesArray,
					      earlyTermination,
					      hintsStatesArray,
					      guidedSearchType, verbosity,
					      dcLevel, buildOnionRings,
					      GSHschedule, signalList,
					      statesCoveredList,
					      newCoveredStatesList,
					      statesToRemoveList);
      numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
					    CovstatesHoskote,
					    Fsm_FsmReadPresentStateVars(modelFsm));
      tmp_mdd = mdd_and(CovstatesHoskote,*totalcoveredstates,1,0);

      numnewcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
					    tmp_mdd,
					    Fsm_FsmReadPresentStateVars(modelFsm));
      mdd_free(tmp_mdd);
      fprintf(vis_stdout,"\n--Total states covered by formula<%d> = %.0f , new = %.0f\n",i+1,
	      numtotcoveredstates,numnewcoveredstates);
      findallsignalsInFormula(listOfSignals,origFormula);
      for (sigarr=0;sigarr<array_n(listOfSignals);sigarr++) {
	mdd_t *newCoveredStates,*statesCovered,*tmp_mdd;
	char *signalInFormula;
	int positionInList;
	signalInFormula = array_fetch(char *,listOfSignals,sigarr);
	positionInList = positionOfSignalinList(signalInFormula,signalList);
    
	newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList);
	statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList);
	tmp_mdd = mdd_and(newCoveredStates,statesCovered,1,0);	/*newly covered States*/	
	fprintf(vis_stdout,"---States covered w.r.t. %s = %.0f, new = %.0f\n",
		signalInFormula,
		mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
				newCoveredStates,
				Fsm_FsmReadPresentStateVars(modelFsm)),
		mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
				tmp_mdd,
				Fsm_FsmReadPresentStateVars(modelFsm)));
	mdd_free(tmp_mdd);

	/* add on the newcoveredstates*/
	tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1);
	mdd_free(statesCovered);
	/*update statesCoveredList*/
	array_insert(mdd_t *,statesCoveredList,positionInList,tmp_mdd);
	mdd_free(newCoveredStates);

	/* reset newCoveredStatesList to zeroMdds for the next formula */
	tmp_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
	array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd);
      }
  
    } else { /* formula fails */
      CovstatesHoskote = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
      fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
      fprintf(vis_stdout,"===================================\n");
      fprintf(vis_stdout,"Coverage for failing formulae = 0\n");
    }
    if (*totalcoveredstates == NIL(mdd_t))
      *totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
	
    if (CovstatesHoskote != NIL(mdd_t)){
      mdd_t *tmp_mdd = mdd_or(*totalcoveredstates,CovstatesHoskote,1,1);
      mdd_free(*totalcoveredstates);
      *totalcoveredstates = tmp_mdd;
    }
	
    numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
					  *totalcoveredstates,
					  Fsm_FsmReadPresentStateVars(modelFsm));
    mdd_free(CovstatesHoskote);
    array_free(listOfSignals);
  }

  if (performCoverageImproved && (modelCareStatesArray != NIL(array_t))) { /* and no errors till now ??*/
    mdd_t *tmp_mdd, *zero_mdd;
    int sigarr;
    array_t *listOfSignals = array_alloc(char *,0);
    origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula);
    if ( ( (traversalDirection == McFwd_c) &&
	   bdd_is_tautology(ctlFormulaStates, 1) ) ||
	 (mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1)) ) {
      /* formula passes */

      if (*totalcoveredstates == NIL(mdd_t))
	*totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));  

      /*add new signals if any found*/
      zero_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
      findallsignals(modelFsm, signalTypeList, signalList,
		     statesCoveredList, newCoveredStatesList,
		     statesToRemoveList, origFormula, zero_mdd);
      mdd_free(zero_mdd);
      fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
      fprintf(vis_stdout,"===================================\n");

      CovstatesImproved = CoveredStatesImproved(modelInitialStates,
						modelFsm, origFormula,
						fairStates, fairCond,
						modelCareStatesArray,
						earlyTermination,
						hintsStatesArray,
						guidedSearchType,
						verbosity,
						dcLevel, buildOnionRings,
						GSHschedule, signalList,
						statesCoveredList,
						newCoveredStatesList,
						statesToRemoveList);
      numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
					    CovstatesImproved,
					    Fsm_FsmReadPresentStateVars(modelFsm));
      tmp_mdd = mdd_and(CovstatesImproved,*totalcoveredstates,1,0);

      numnewcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
					    tmp_mdd,
					    Fsm_FsmReadPresentStateVars(modelFsm));
      mdd_free(tmp_mdd);
      fprintf(vis_stdout,"\n--Total states covered by formula<%d> = %.0f , new = %.0f\n",i+1,
	      numtotcoveredstates,numnewcoveredstates);
      findallsignalsInFormula(listOfSignals,origFormula);
      for (sigarr=0;sigarr<array_n(listOfSignals);sigarr++) {
	mdd_t *newCoveredStates,*statesCovered,*tmp_mdd;
	char *signalInFormula;
	int positionInList;
	signalInFormula = array_fetch(char *,listOfSignals,sigarr);
	positionInList = positionOfSignalinList(signalInFormula,signalList);
    
	newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList);
	statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList);
	tmp_mdd = mdd_and(newCoveredStates,statesCovered,1,0);	/*newly covered States*/	
	fprintf(vis_stdout,"---States covered w.r.t. %s = %.0f, new = %.0f\n",
		signalInFormula,
		mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
				newCoveredStates,
				Fsm_FsmReadPresentStateVars(modelFsm)),
		mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
				tmp_mdd,
				Fsm_FsmReadPresentStateVars(modelFsm)));
	mdd_free(tmp_mdd);

	/* add on the newcoveredstates*/
	tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1);
	mdd_free(statesCovered);
	/*update statesCoveredList*/
	array_insert(mdd_t *,statesCoveredList,positionInList,tmp_mdd);
	mdd_free(newCoveredStates);

	/* reset newCoveredStatesList to zeroMdds for the next formula */
	tmp_mdd = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
	array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd);
      }

    } else { /* formula fails */
      CovstatesImproved = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
      fprintf(vis_stdout,"\n--Checking coverage for formula<%d>\n",i+1);
      fprintf(vis_stdout,"===================================\n");
      fprintf(vis_stdout,"Coverage for failing formulae = 0\n");
    }
    if (*totalcoveredstates == NIL(mdd_t))
      *totalcoveredstates = mdd_zero(Fsm_FsmReadMddManager(modelFsm));
	
    if (CovstatesImproved != NIL(mdd_t)){
      mdd_t *tmp_mdd = mdd_or(*totalcoveredstates,CovstatesImproved,1,1);
      mdd_free(*totalcoveredstates);
      *totalcoveredstates = tmp_mdd;
    }
	
    numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
					  *totalcoveredstates,
					  Fsm_FsmReadPresentStateVars(modelFsm));
    mdd_free(CovstatesImproved);
    array_free(listOfSignals);
  }

} /* McEstimateCoverage */


/**Function********************************************************************

  Synopsis    [Print summary for the coverage of a property file.]

  SideEffects [none]

  SeeAlso     [CommandMc McEstimateCoverage]

******************************************************************************/
void
McPrintCoverageSummary(
  Fsm_Fsm_t *modelFsm,
  Mc_DcLevel dcLevel,
  McOptions_t *options,
  array_t *modelCareStatesArray,
  mdd_t *modelCareStates,
  mdd_t *totalcoveredstates,
  array_t *signalTypeList,
  array_t *signalList,
  array_t *statesCoveredList,
  boolean performCoverageHoskote,
  boolean performCoverageImproved
  )
{
  float coverage;
  float coveragePI;
  float coveragePO;
  float coverageOther;
  float numPI;
  float numPO;
  float numOther;
  float avgCoverage;
  float avgPICoverage;
  float avgPOCoverage;
  float avgOtherCoverage;
  double numrchstates;
  double numtotcoveredstates;

  if (performCoverageHoskote &&
      (modelCareStatesArray != NIL(array_t))) { /* and no errors till now */
    int sigarr;
    if (totalcoveredstates != NIL(mdd_t) && (modelCareStates != NIL(mdd_t))) {
      numtotcoveredstates = mdd_count_onset(
	Fsm_FsmReadMddManager(modelFsm),
	totalcoveredstates,
	Fsm_FsmReadPresentStateVars(modelFsm));
    }
    else {
      numtotcoveredstates = 0;
    }
    
    if ((dcLevel == McDcLevelRch_c)||(dcLevel == McDcLevelRchFrontier_c)) {
      if (!mdd_lequal(totalcoveredstates, modelCareStates, 1, 1)) {
	(void)fprintf(vis_stdout,
		    "** mc warning: Some of the covered states are not reachable\n");
      }
      if (modelCareStates !=NIL(mdd_t)){
	int sigType;
	coveragePI = 0;
	coveragePO = 0;
	coverageOther = 0;
	numPI = 0;
	numPO = 0;
	numOther = 0;
	avgCoverage = 0;
	avgPICoverage = 0;
	avgPOCoverage = 0;
	avgOtherCoverage = 0;
	numrchstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
				       modelCareStates,
				       Fsm_FsmReadPresentStateVars(modelFsm));
	if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
	  fprintf(vis_stdout,"\nCoverage for all the Formulae w.r.t. all observable signals\n");
	  fprintf(vis_stdout,"=============================================================\n");
	}
	for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
	  mdd_t *statesCovered, *uncoveredStateCube, *uncoveredStates;
	  double numStatesCovered;
	  char *nrOfUncoveredStatesString;
	  int nrOfUncoveredStates, prntStates;   /* nr of uncovered states that we output */

	  Ntk_Network_t *modelNetworkC = Fsm_FsmReadNetwork(modelFsm);
	  array_t *PSVarsC = Fsm_FsmReadPresentStateVars(modelFsm);
	  mdd_manager *mddMgrC = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));

	  statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
	  numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
					     statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
	  coverage = (numStatesCovered / numrchstates) * 100;
	  avgCoverage = avgCoverage + coverage;
	  sigType = array_fetch(int, signalTypeList,sigarr);
	  if (sigType == 1) {
	    coveragePI = coveragePI + numStatesCovered;
	    avgPICoverage = avgPICoverage + coverage;
	    numPI = numPI + 1;
	  }
	  else if (sigType == 0) {
	    coveragePO = coveragePO + numStatesCovered;
	    avgPOCoverage = avgPOCoverage + coverage;
	    numPO = numPO + 1;
	  }
	  else {
	    coverageOther = coverageOther + numStatesCovered;
	    avgOtherCoverage = avgOtherCoverage + coverage;
	    numOther = numOther + 1;
	  }
	  if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
	    fprintf(vis_stdout,"\n# States covered w.r.t. %s = %.0f, Percentage of Coverage = %f\n",
		    array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
	    nrOfUncoveredStatesString = Cmd_FlagReadByName("nr_uncoveredstates");
	    if(nrOfUncoveredStatesString == NIL(char))
	      nrOfUncoveredStates = 1;
	    else
	      nrOfUncoveredStates = atoi(nrOfUncoveredStatesString);
	    if (numStatesCovered < numrchstates) {
	      if ((numrchstates-numStatesCovered) < nrOfUncoveredStates)
		nrOfUncoveredStates = (int)(numrchstates-numStatesCovered);
	      fprintf(vis_stdout,"#Printing reachable states NOT covered w.r.t. %s :\n",array_fetch(char *,signalList,sigarr));
	      for (prntStates = 0;prntStates<nrOfUncoveredStates;prntStates++){  
		fprintf(vis_stdout,"\n#State %d :\n",prntStates+1);
		uncoveredStates = mdd_and(modelCareStates,statesCovered,1,0);
		uncoveredStateCube = Mc_ComputeAMinterm(uncoveredStates, PSVarsC, mddMgrC);
		mdd_free(uncoveredStates);
		Mc_MintermPrint(uncoveredStateCube, PSVarsC, modelNetworkC);
		mdd_free(uncoveredStateCube);
	      }
	    }
	  }
	}
	fprintf(vis_stdout,"\nTotal Coverage for all the Formulae\n");
	fprintf(vis_stdout,"=====================================\n");
	for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
	  mdd_t *statesCovered;
	  double numStatesCovered;
	  char *type;
	  int sigType;

	  sigType = array_fetch(int, signalTypeList,sigarr);
	  if (sigType == 1)
	    type = "Primary Input";
	  else if (sigType == 0)
	    type = "Primary Output";
	  else
	    type = "Neither Primary output nor input";

	  statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);

	  numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
					     statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
	  coverage = (numStatesCovered / numrchstates) * 100;
	  fprintf(vis_stdout,"# States covered w.r.t. %s(%s) = %.0f, Percentage of Coverage = %f\n",type,
		  array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
	}
	fprintf(vis_stdout,"--There are %.0f covered states (using Hoskote et.al's implementation)\n",numtotcoveredstates);
	fprintf(vis_stdout,"--%.0f states covered by Primary Input Signals\n",coveragePI);
	fprintf(vis_stdout,"--%.0f states covered by Primary Ouput Signals\n",coveragePO);
	fprintf(vis_stdout,"--%.0f states covered by signals which are neither Primary input nor output Signals\n",coverageOther);
	fprintf(vis_stdout,"--There are %.0f reachable states\n",numrchstates);

	coverage = (numtotcoveredstates / numrchstates) * 100;
	fprintf(vis_stdout,"Percentage of coverage (using Hoskote et.al's implementation)= %f\n ",coverage);
	avgCoverage = avgCoverage / array_n(signalList);
	fprintf(vis_stdout,"Average Percentage of coverage = %f\n",avgCoverage);
	if (numPI < 1)
	  fprintf(vis_stdout,"No Primary Input signals\n");
	else {
	  avgPICoverage = avgPICoverage / numPI;
	  fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgPICoverage);
	}
	if (numPO < 1)
	  fprintf(vis_stdout,"No Primary Output signals\n");
	else {
	  avgPOCoverage = avgPOCoverage / numPO;
	  fprintf(vis_stdout,"Average Percentage of coverage for Primary outputs = %f\n",avgPOCoverage);
	}
	if (numOther < 1)
	  fprintf(vis_stdout,"No signals which are neither primary inputs nor outputs\n");
	else {
	  avgOtherCoverage = avgOtherCoverage / numOther;
	  fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgOtherCoverage);
	}
      }
      else {
	fprintf(vis_stdout,"Reachable states = NIL !\n");
      }
    }
  }

  if (performCoverageImproved && (modelCareStatesArray != NIL(array_t))) { /* and no errors till now */
    int sigarr;
    if (totalcoveredstates != NIL(mdd_t) && (modelCareStates != NIL(mdd_t))) {
      numtotcoveredstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),totalcoveredstates,Fsm_FsmReadPresentStateVars(modelFsm));
    }
    else {
      numtotcoveredstates = 0;
    }
   
    if ((dcLevel == McDcLevelRch_c)||(dcLevel == McDcLevelRchFrontier_c)) {
      if (!mdd_lequal(totalcoveredstates, modelCareStates, 1, 1)) {
	(void)fprintf(vis_stdout,
		      "** mc warning: Some of the covered states are not reachable\n");
      }
      if (modelCareStates !=NIL(mdd_t)){
	int sigType;

	coveragePI = 0;
	coveragePO = 0;
	coverageOther = 0;
	numPI = 0;
	numPO = 0;
	numOther = 0;
	avgCoverage = 0;
	avgPICoverage = 0;
	avgPOCoverage = 0;
	avgOtherCoverage = 0;

	numrchstates = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),modelCareStates,Fsm_FsmReadPresentStateVars(modelFsm));
	if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
	  fprintf(vis_stdout,"\nCoverage for all the Formulae w.r.t. all observable signals\n");
	  fprintf(vis_stdout,"=============================================================\n");
	}
	for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
	  mdd_t *statesCovered, *uncoveredStateCube, *uncoveredStates;
	  double numStatesCovered;
	  char *nrOfUncoveredStatesString;
	  int nrOfUncoveredStates, prntStates; /* nr of uncovered states that we output */

	  Ntk_Network_t *modelNetworkC = Fsm_FsmReadNetwork(modelFsm);
	  array_t *PSVarsC = Fsm_FsmReadPresentStateVars(modelFsm);
	  mdd_manager *mddMgrC = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));

	  statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
	  numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
					     statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
	  coverage = (numStatesCovered / numrchstates) * 100;
	  avgCoverage = avgCoverage + coverage;
	  sigType = array_fetch(int, signalTypeList,sigarr);
	  if (sigType == 1) {
	    coveragePI = coveragePI + numStatesCovered;
	    avgPICoverage = avgPICoverage + coverage;
	    numPI = numPI + 1;
	  }
	  else if (sigType == 0) {
	    coveragePO = coveragePO + numStatesCovered;
	    avgPOCoverage = avgPOCoverage + coverage;
	    numPO = numPO + 1;
	  }
	  else {
	    coverageOther = coverageOther + numStatesCovered;
	    avgOtherCoverage = avgOtherCoverage + coverage;
	    numOther = numOther + 1;
	  }
	  if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { /*print debug info*/
	    fprintf(vis_stdout,"\n# States covered w.r.t. %s = %.0f, Percentage of Coverage = %f\n",
		    array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
	    nrOfUncoveredStatesString = Cmd_FlagReadByName("nr_uncoveredstates");
	    if(nrOfUncoveredStatesString == NIL(char))
	      nrOfUncoveredStates = 1;
	    else
	      nrOfUncoveredStates = atoi(nrOfUncoveredStatesString);
	    if (numStatesCovered < numrchstates) {
	      if ((numrchstates-numStatesCovered) < nrOfUncoveredStates)
		nrOfUncoveredStates = (int)(numrchstates-numStatesCovered);
	      fprintf(vis_stdout,"#Printing reachable states NOT covered w.r.t. %s :\n",array_fetch(char *,signalList,sigarr));
	      for (prntStates = 0;prntStates<nrOfUncoveredStates;prntStates++){  
		fprintf(vis_stdout,"\n#State %d :\n",prntStates+1);
		uncoveredStates = mdd_and(modelCareStates,statesCovered,1,0);
		uncoveredStateCube = Mc_ComputeAMinterm(uncoveredStates, PSVarsC, mddMgrC);
		mdd_free(uncoveredStates);
		Mc_MintermPrint(uncoveredStateCube, PSVarsC, modelNetworkC);
		mdd_free(uncoveredStateCube);
	      }
	    }
	  }
	}
	fprintf(vis_stdout,"\nTotal Coverage for all the Formulae\n");
	fprintf(vis_stdout,"=====================================\n");
	for (sigarr=0;sigarr<array_n(signalList);sigarr++) {
	  mdd_t *statesCovered;
	  double numStatesCovered;
	  char *type;
	  int sigType;
	  sigType = array_fetch(int, signalTypeList,sigarr);
	  if (sigType == 1)
	    type = "Primary Input";
	  else if (sigType == 0)
	    type = "Primary Output";
	  else
	    type = "Neither Primary output nor input";
	  statesCovered = array_fetch(mdd_t *,statesCoveredList,sigarr);
	  numStatesCovered = mdd_count_onset(Fsm_FsmReadMddManager(modelFsm),
					     statesCovered,Fsm_FsmReadPresentStateVars(modelFsm));
	  coverage = (numStatesCovered / numrchstates) * 100;
	  fprintf(vis_stdout,"# States covered w.r.t. %s(%s) = %.0f, Percentage of Coverage = %f\n",type,
		  array_fetch(char *,signalList,sigarr), numStatesCovered, coverage);
	}
	fprintf(vis_stdout,"--There are %.0f covered states (using improved coverage implementation)\n",numtotcoveredstates);
	fprintf(vis_stdout,"--%.0f states covered by Primary Input Signals\n",coveragePI);
	fprintf(vis_stdout,"--%.0f states covered by Primary Ouput Signals\n",coveragePO);
	fprintf(vis_stdout,"--%.0f states covered by signals which are neither Primary input nor output Signals\n",coverageOther);
	fprintf(vis_stdout,"--There are %.0f reachable states\n",numrchstates);

	coverage = (numtotcoveredstates / numrchstates) * 100;
	fprintf(vis_stdout,"Percentage of coverage (using improved coverage implementation)= %f\n ",coverage);
	avgCoverage = avgCoverage / array_n(signalList);
	fprintf(vis_stdout,"Average Percentage of coverage = %f\n",avgCoverage);
	if (numPI < 1)
	  fprintf(vis_stdout,"No Primary Input signals\n");
	else {
	  avgPICoverage = avgPICoverage / numPI;
	  fprintf(vis_stdout,"Average Percentage of coverage for Primary inputs = %f\n",avgPICoverage);
	}
	if (numPO < 1)
	  fprintf(vis_stdout,"No Primary Output signals\n");
	else {
	  avgPOCoverage = avgPOCoverage / numPO;
	  fprintf(vis_stdout,"Average Percentage of coverage for Primary outputs = %f\n",avgPOCoverage);
	}
	if (numOther < 1)
	  fprintf(vis_stdout,"No signals which are not primary\n");
	else {
	  avgOtherCoverage = avgOtherCoverage / numOther;
	  fprintf(vis_stdout,"Average Percentage of coverage for signals which are not primary = %f\n",avgOtherCoverage);
	}
      }
      else {
	fprintf(vis_stdout,"Reachable states = NIL !\n");
      }
    }
  }
} /* McPrintCoverageSummary */

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Computes a the set of covered states for a given formula and 
               initial set of states given.]

  Description [Presently Works for only a subset 
  of ACTL viz. (propostional formulae, ->, AX, AG, AF, AU, ^ )]

  SideEffects [Updates running totals.]

  SeeAlso     [McEstimateCoverage CoveredStatesImproved]

******************************************************************************/
static 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)
{
  mdd_t *Covstates1, *temp1, *temp2;
  mdd_t *Covstates2;
  mdd_t *result;
  mdd_t *travstates;
  mdd_t *frstrchstates;
  
  mdd_t *startstates;

  Ctlp_FormulaType formulaType;
  Ctlp_Formula_t *rightFormula, *leftFormula, *tmp_formula, *existFormula;
  double numresultstates; /* used for debugging <NJ> */

  startstates = mdd_and(startstates_old,fairStates,1,1);

  if (mdd_is_tautology(startstates,0)) {
    if (verbosity > McVerbosityNone_c)
      fprintf(vis_stdout,
	      "\n--Startstates are down to zero. Coverage is hence zero.\n");
    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(startstates);
    return result;
  }
  if (Ctlp_FormulaTestIsQuantifierFree(OrigFormula)) {
    /*propositional formula*/
    result = CoveragePropositional(startstates, fsm, OrigFormula, fairStates,
				   fairCondition, careStatesArray,
				   earlyTermination, hintsArray, hintType,
				   verbosity, dcLevel,buildOnionRing,
				   GSHschedule, signalList, statesCoveredList,
				   newCoveredStatesList, statesToRemoveList);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
  }
  formulaType = Ctlp_FormulaReadType(OrigFormula);
  switch (formulaType) {
  case Ctlp_EG_c: 
  case Ctlp_EF_c:
  case Ctlp_EU_c:
  case Ctlp_FwdU_c:
  case Ctlp_FwdG_c:
  case Ctlp_EY_c:
  case Ctlp_EH_c:
  case Ctlp_Cmp_c:
  case Ctlp_EX_c:
  case Ctlp_Init_c:  {
    fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL,\n");
    fprintf(vis_stdout,"** can't compute coverage of : ");
    Ctlp_FormulaPrint(vis_stdout,OrigFormula);
    fprintf(vis_stdout,"\n");
    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_AX_c:{
    temp1 = Mc_FsmEvaluateEYFormula(fsm, startstates, fairStates, careStatesArray, verbosity, dcLevel);
    Covstates1 = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    result = CoveredStatesHoskote(Covstates1, fsm, leftFormula, fairStates,
				  fairCondition, careStatesArray,
				  earlyTermination, hintsArray,
				  hintType, verbosity, dcLevel, buildOnionRing,
				  GSHschedule, signalList, statesCoveredList,
				  newCoveredStatesList, statesToRemoveList);
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(Covstates1);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_AG_c:{
    mdd_t *initStates;
    double numststates;
    initStates = Fsm_FsmComputeInitialStates(fsm);
    temp1 = mdd_one(Fsm_FsmReadMddManager(fsm));
    if (mdd_equal_mod_care_set_array(startstates,initStates,careStatesArray)) {
      if (verbosity > McVerbosityNone_c)
	fprintf(vis_stdout,"\nUsing the reachable states already computed...");
      temp2 = Fsm_FsmComputeReachableStates(fsm, 0, 1, 0, 0, 0, 0, 0,
					    Fsm_Rch_Default_c, 0, 0,
					    NIL(array_t), FALSE, NIL(array_t));
    } else
      temp2 = Mc_FsmEvaluateFwdUFormula(fsm, startstates, temp1, fairStates,
					careStatesArray, NIL(array_t),
					verbosity, dcLevel);
    mdd_free(initStates);
    numststates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),startstates,
				  Fsm_FsmReadPresentStateVars(fsm));
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),temp2,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(temp1);
    Covstates1 = mdd_and(temp2,fairStates,1,1);
    mdd_free(temp2);
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    result = CoveredStatesHoskote(Covstates1, fsm, leftFormula, fairStates,
				  fairCondition, careStatesArray,
				  earlyTermination, hintsArray, hintType,
				  verbosity, dcLevel, buildOnionRing,
				  GSHschedule, signalList, statesCoveredList,
				  newCoveredStatesList, statesToRemoveList);
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(Covstates1);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_AF_c:{
    tmp_formula = OrigFormula;
    OrigFormula = Ctlp_FormulaConvertAFtoAU(tmp_formula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"Converting formula from\n");
      Ctlp_FormulaPrint(vis_stdout,tmp_formula);
      fprintf(vis_stdout,"\nto\n");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      fprintf(vis_stdout,"\n");
    }
#if 0
    Ctlp_FormulaFree(tmp_formula);
    formulaType = Ctlp_AU_c;
#endif
    /* convert to AFp to A (TRUE) U p  and then step thru to do coverage
       for AU computation below*/
  }
  case Ctlp_AU_c:{
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
    travstates = traverse(fsm, fairStates, fairCondition, careStatesArray,
			  earlyTermination, hintsArray, hintType, verbosity,
			  dcLevel, buildOnionRing, GSHschedule, startstates,
			  leftFormula,rightFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n---Computing coverage for LHS of U formula i.e: ");
      Ctlp_FormulaPrint(vis_stdout,leftFormula);
      fprintf(vis_stdout,
	      "\n------------------------------------------------\n");
    }
    Covstates1 = CoveredStatesHoskote(travstates, fsm, leftFormula, fairStates,
				      fairCondition, careStatesArray,
				      earlyTermination, hintsArray, hintType,
				      verbosity, dcLevel, buildOnionRing,
				      GSHschedule, signalList,
				      statesCoveredList, newCoveredStatesList,
				      statesToRemoveList);
    mdd_free(travstates);
    frstrchstates = firstReached(fsm, fairStates, fairCondition,
				 careStatesArray, earlyTermination, hintsArray,
				 hintType, verbosity, dcLevel, buildOnionRing,
				 GSHschedule, startstates, rightFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n---Computing coverage for RHS of U formula i.e: ");
      Ctlp_FormulaPrint(vis_stdout,rightFormula);
      fprintf(vis_stdout,
	      "\n------------------------------------------------\n");
    }
    Covstates2 = CoveredStatesHoskote(frstrchstates, fsm, rightFormula,
				      fairStates, fairCondition,
				      careStatesArray, earlyTermination,
				      hintsArray, hintType, verbosity, dcLevel,
				      buildOnionRing, GSHschedule, signalList,
				      statesCoveredList, newCoveredStatesList,
				      statesToRemoveList);
    mdd_free(frstrchstates);
    result = mdd_or(Covstates1,Covstates2,1,1);
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(Covstates1);
    mdd_free(Covstates2);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    if (formulaType == Ctlp_AF_c)
      Ctlp_FormulaFree(OrigFormula);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_AND_c:{
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"---Computing coverage for LHS sub-formula: ");
      Ctlp_FormulaPrint(vis_stdout,leftFormula);
      fprintf(vis_stdout,
	      "\n------------------------------------------------\n");
    }
    Covstates1 = CoveredStatesHoskote(startstates,fsm, leftFormula, fairStates,
				      fairCondition, careStatesArray,
				      earlyTermination, hintsArray, hintType,
				      verbosity, dcLevel, buildOnionRing,
				      GSHschedule, signalList,
				      statesCoveredList, newCoveredStatesList,
				      statesToRemoveList);
    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"---Computing coverage for RHS sub-formula: ");
      Ctlp_FormulaPrint(vis_stdout,rightFormula);
      fprintf(vis_stdout,
	      "\n------------------------------------------------\n");
    }
    Covstates2 = CoveredStatesHoskote(startstates,fsm, rightFormula,
				      fairStates, fairCondition, 
				      careStatesArray, earlyTermination,
				      hintsArray, hintType, verbosity, dcLevel,
				      buildOnionRing,GSHschedule, signalList,
				      statesCoveredList, newCoveredStatesList,
				      statesToRemoveList);
    result = mdd_or(Covstates1, Covstates2, 1, 1);
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(Covstates1);
    mdd_free(Covstates2);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_THEN_c:{ /*f1 -> f2 = !f2 -> !f1*/
    mdd_t *nextstartstates, *Tb;
   
    if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadLeftChild(OrigFormula))) { /*if f1 is propositional*/
      leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
      rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
    } else if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadRightChild(OrigFormula))) { /*if f2 is propositional*/
       /* Convert f1->f2 to !f2->!f1      */
      leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
      rightFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
    } else { /*neither are propositional*/
      fprintf(vis_stdout,"\nCan't compute coverage of implications where neither side is propositional\n");
      fprintf(vis_stdout,"Could not compute coverage of :");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      result = mdd_zero(Fsm_FsmReadMddManager(fsm));
      mdd_free(startstates);
      return result;
    }
    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
    Tb = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
			       fairCondition, careStatesArray,
			       earlyTermination, hintsArray, hintType,
			       verbosity, dcLevel, buildOnionRing,GSHschedule);
    Ctlp_FormulaFree(existFormula);
    nextstartstates = mdd_and(startstates, Tb,1,1);
    mdd_free(Tb);
    Covstates1 = CoveredStatesHoskote(nextstartstates,fsm, rightFormula,
				      fairStates, fairCondition, 
				      careStatesArray, earlyTermination,
				      hintsArray, hintType, verbosity, dcLevel,
				      buildOnionRing,GSHschedule, signalList,
				      statesCoveredList, newCoveredStatesList,
				      statesToRemoveList);
    mdd_free(nextstartstates);
    mdd_free(startstates);
    return Covstates1;
    break;
  }
  case Ctlp_XOR_c: {
    tmp_formula = Ctlp_FormulaConvertXORtoOR(OrigFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n--Converting XOR to AND and OR from:\n");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      fprintf(vis_stdout,"\nto\n");
      Ctlp_FormulaPrint(vis_stdout, tmp_formula);
      fprintf(vis_stdout,"\n");
    } 
    result = CoveredStatesHoskote(startstates, fsm, tmp_formula, fairStates,
				  fairCondition, careStatesArray,
				  earlyTermination, hintsArray,
				  hintType, verbosity, dcLevel,buildOnionRing,
				  GSHschedule, signalList, statesCoveredList,
				  newCoveredStatesList, statesToRemoveList);
    mdd_free(startstates);
    return result;
    break;
  } 
  case Ctlp_EQ_c: {
    tmp_formula = Ctlp_FormulaConvertEQtoOR(OrigFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n--Converting EQ to AND and OR from:\n");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      fprintf(vis_stdout,"\nto\n");
      Ctlp_FormulaPrint(vis_stdout, tmp_formula);
      fprintf(vis_stdout,"\n");
    } 
    result = CoveredStatesHoskote(startstates, fsm, tmp_formula, fairStates,
				  fairCondition, careStatesArray,
				  earlyTermination, hintsArray,
				  hintType, verbosity, dcLevel,buildOnionRing,
				  GSHschedule, signalList, statesCoveredList,
				  newCoveredStatesList, statesToRemoveList);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_OR_c:{  /*f1+f2 = !f1 -> f2 = !f2 -> f1*/
    mdd_t *nextstartstates, *Tb;

    if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadLeftChild(OrigFormula))) { /*if f1 is propositional*/
      /* Convert f1+f2 to !f1->f2      */
      leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
      rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
    } else if (Ctlp_FormulaTestIsQuantifierFree(Ctlp_FormulaReadRightChild(OrigFormula))) { /*if f2 is propositional*/
       /* Convert f1+f2 to !f2->f1      */
      leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
      rightFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    } else { /*neither are propositional*/
      fprintf(vis_stdout,"\nCan't compute coverage of disjunctions where neither side is propositional\n");
      fprintf(vis_stdout,"Could not compute coverage of :");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      result = mdd_zero(Fsm_FsmReadMddManager(fsm));
      mdd_free(startstates);
      return result;
    }
    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
    Tb = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
			       fairCondition, careStatesArray,
			       earlyTermination, hintsArray, hintType,
			       verbosity, dcLevel, buildOnionRing,GSHschedule);
    Ctlp_FormulaFree(existFormula);
    Ctlp_FormulaFree(leftFormula);
    nextstartstates = mdd_and(startstates, Tb,1,1);
    mdd_free(Tb);
    Covstates1 = CoveredStatesHoskote(nextstartstates,fsm, rightFormula,
				      fairStates, fairCondition, 
				      careStatesArray, earlyTermination,
				      hintsArray, hintType, verbosity, dcLevel,
				      buildOnionRing,GSHschedule, signalList,
				      statesCoveredList, newCoveredStatesList,
				      statesToRemoveList);
    mdd_free(nextstartstates);
    mdd_free(startstates);
    return Covstates1;
    break;
  }
  case Ctlp_NOT_c:{ /*include code for checking for 2 NOTs*/
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    if (!(Ctlp_FormulaTestIsQuantifierFree(leftFormula))) {
      tmp_formula = Ctlp_FormulaPushNegation(leftFormula);
      if (verbosity > McVerbosityNone_c) {
	fprintf(vis_stdout,"\n--Pushing down negation one level. Converting formula from:\n");
	Ctlp_FormulaPrint(vis_stdout,OrigFormula);
	fprintf(vis_stdout,"\nto\n");
	Ctlp_FormulaPrint(vis_stdout,tmp_formula);
	fprintf(vis_stdout,"\n");
      }
      Covstates1 = CoveredStatesHoskote(startstates, fsm, tmp_formula,
					fairStates, fairCondition, 
					careStatesArray, earlyTermination,
					hintsArray, hintType, verbosity,
					dcLevel, buildOnionRing,GSHschedule,
					signalList, statesCoveredList,
					newCoveredStatesList,
					statesToRemoveList);
      Ctlp_FormulaFree(tmp_formula);
      result = mdd_and(Covstates1,fairStates,1,1);
      mdd_free(Covstates1);
      mdd_free(startstates);
      return result;
#if 0
      fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL\n");
      fprintf(vis_stdout,"** can't compute coverage of : ");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      fprintf(vis_stdout,"\n");
      mdd_free(startstates);
      return mdd_zero(Fsm_FsmReadMddManager(fsm));
#endif
    } else { /*this part of the code is now never executed*/
      fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
      mdd_free(startstates);
      return mdd_zero(Fsm_FsmReadMddManager(fsm));
    }
    break;
  }
  case Ctlp_TRUE_c:
  case Ctlp_FALSE_c: {
    if (verbosity > McVerbosityNone_c)
      fprintf(vis_stdout,"No observable signal, hence no coverage\n");
    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_ID_c:{ /*should not reach here*/
    fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
    mdd_free(startstates);
    return mdd_zero(Fsm_FsmReadMddManager(fsm));
    break;
  }
  default:
    fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
    break;
  }
  assert(0);
  return NIL(mdd_t);

} /* CoveredStatesHoskote */


/**Function********************************************************************

  Synopsis    [Computes a the set of covered states for a given formula and 
               initial set of states given. ]

  Description [Works for a larger subset of CTL than CoveredStatesHoskote.]

  SideEffects [Updates running totals.]

  SeeAlso     [McEstimateCoverage CoveredStatesHoskote]

******************************************************************************/
static 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)
{
  mdd_t *Covstates1, *temp1, *temp2;
  mdd_t *Covstates2;
  mdd_t *result;
  mdd_t *travstates;
  mdd_t *frstrchstates;
  
  mdd_t *startstates;

  Ctlp_FormulaType formulaType;
  Ctlp_Formula_t *rightFormula, *leftFormula, *tmp_formula, *existFormula;
  double numresultstates; /* used for debugging <NJ> */

  startstates = mdd_and(startstates_old,fairStates,1,1);
  
  if (mdd_is_tautology(startstates,0)) {
    if (verbosity > McVerbosityNone_c)
      fprintf(vis_stdout,
	      "\n--Startstates are down to zero. Coverage is hence zero.\n");
    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(startstates);
    return result;
  }
  if (Ctlp_FormulaTestIsQuantifierFree(OrigFormula)) {
    /* propositional formula */
    result = CoveragePropositional(startstates, fsm, OrigFormula, fairStates,
				   fairCondition, careStatesArray,
				   earlyTermination, hintsArray, hintType,
				   verbosity, dcLevel,buildOnionRing,
				   GSHschedule, signalList, statesCoveredList,
				   newCoveredStatesList, statesToRemoveList);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
  }
  formulaType = Ctlp_FormulaReadType(OrigFormula);
  switch (formulaType) {
  case Ctlp_EG_c: {/*EGp = p * EX(EGp) => C(So,EGp) = C(So,p) */
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n--Computing underapproximation for EG formula:\n");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      fprintf(vis_stdout,"\n");
    }
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    result = CoveredStatesImproved(startstates, fsm, leftFormula, fairStates,
				   fairCondition, careStatesArray,
				   earlyTermination, hintsArray, hintType,
				   verbosity, dcLevel,buildOnionRing,
				   GSHschedule, signalList, statesCoveredList,
				   newCoveredStatesList, statesToRemoveList);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_EF_c: {
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n--Computing underapproximation for EF formula:\n");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      fprintf(vis_stdout,"\n");
    }
    tmp_formula = Ctlp_FormulaConvertEFtoOR(OrigFormula);
    result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
				   fairCondition, careStatesArray,
				   earlyTermination, hintsArray,
				   hintType, verbosity, dcLevel,buildOnionRing,
				   GSHschedule, signalList, statesCoveredList,
				   newCoveredStatesList, statesToRemoveList);
    Ctlp_FormulaFree(tmp_formula);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_EU_c: {
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n--Computing underapproximation for EU formula: ");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      fprintf(vis_stdout,"\n");
    }
    tmp_formula = Ctlp_FormulaConvertEUtoOR(OrigFormula);
    result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
				   fairCondition, careStatesArray,
				   earlyTermination, hintsArray, hintType,
				   verbosity, dcLevel,buildOnionRing,
				   GSHschedule, signalList, statesCoveredList,
				   newCoveredStatesList,statesToRemoveList);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_FwdU_c:
  case Ctlp_FwdG_c:
  case Ctlp_EY_c:
  case Ctlp_EH_c:
  case Ctlp_Cmp_c:
  case Ctlp_EX_c:
  case Ctlp_Init_c:  {
    fprintf(vis_stdout,"** Can presently compute coverage for only a certain subset of ACTL,\n");
    fprintf(vis_stdout,"** can't compute coverage of : ");
    Ctlp_FormulaPrint(vis_stdout,OrigFormula);
    fprintf(vis_stdout,"\n");
    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_AX_c:{
    temp1 = Mc_FsmEvaluateEYFormula(fsm, startstates, fairStates, careStatesArray, verbosity, dcLevel);
    Covstates1 = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    result = CoveredStatesImproved(Covstates1, fsm, leftFormula, fairStates,
				   fairCondition, careStatesArray,
				   earlyTermination, hintsArray, hintType,
				   verbosity, dcLevel,buildOnionRing,
				   GSHschedule, signalList, statesCoveredList,
				   newCoveredStatesList, statesToRemoveList);
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(Covstates1);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_AG_c:{
    double numststates;
    mdd_t  *initStates;
    initStates = Fsm_FsmComputeInitialStates(fsm);
    temp1 = mdd_one(Fsm_FsmReadMddManager(fsm));
    if (mdd_equal_mod_care_set_array(startstates,initStates,careStatesArray)) {
      if (verbosity > McVerbosityNone_c)
	fprintf(vis_stdout,"\nUsing the reachable states already computed...");
      temp2 = Fsm_FsmComputeReachableStates(fsm, 0, 1, 0, 0, 0, 0, 0,
					    Fsm_Rch_Default_c, 0, 0,
					    NIL(array_t), FALSE, NIL(array_t));
    } else
      temp2 = Mc_FsmEvaluateFwdUFormula(fsm, startstates, temp1, fairStates,
					careStatesArray, NIL(array_t),
					verbosity, dcLevel);
    mdd_free(initStates);
#if 0
    temp2 = McForwardReachable(fsm, startstates, temp1, fairStates,
			       careStatesArray, NIL(array_t),verbosity,
			       dcLevel);
#endif
    numststates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),startstates,
				  Fsm_FsmReadPresentStateVars(fsm));
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),temp2,
				      Fsm_FsmReadPresentStateVars(fsm));
#if 0
    fprintf(vis_stdout,"\nNum of forward reachable states from %.0f startstates = %.0f\n",numststates,numresultstates);
#endif
    mdd_free(temp1);
    Covstates1 = mdd_and(temp2,fairStates,1,1);
    mdd_free(temp2);
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    result = CoveredStatesImproved(Covstates1, fsm, leftFormula, fairStates,
				   fairCondition, careStatesArray,
				   earlyTermination, hintsArray, hintType,
				   verbosity, dcLevel, buildOnionRing,
				   GSHschedule, signalList, statesCoveredList,
				   newCoveredStatesList, statesToRemoveList);
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(Covstates1);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_AF_c:{
    tmp_formula = OrigFormula;
    OrigFormula = Ctlp_FormulaConvertAFtoAU(tmp_formula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"Converting formula from\n");
      Ctlp_FormulaPrint(vis_stdout,tmp_formula);
      fprintf(vis_stdout,"\nto\n");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      fprintf(vis_stdout,"\n");
    }
#if 0
    Ctlp_FormulaFree(tmp_formula);
    formulaType = Ctlp_AU_c;
#endif
    /* convert to AFp to A (TRUE) U p  and then step thru to do coverage
       for AU computation below*/
  }
  case Ctlp_AU_c:{
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
    tmp_formula = Ctlp_FormulaCreate(Ctlp_OR_c,leftFormula,rightFormula);
    CtlpFormulaIncrementRefCount(leftFormula);
    CtlpFormulaIncrementRefCount(rightFormula);
    travstates = traverse(fsm, fairStates, fairCondition, careStatesArray,
			  earlyTermination, hintsArray, hintType, verbosity,
			  dcLevel, buildOnionRing, GSHschedule, startstates,
			  leftFormula, rightFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n---Computing coverage for LHS of U formula i.e: ");
      Ctlp_FormulaPrint(vis_stdout,leftFormula);
      fprintf(vis_stdout,
	      "\n------------------------------------------------\n");
    }
    Covstates1 = CoveredStatesImproved(travstates, fsm, tmp_formula,
				       fairStates, fairCondition,
				       careStatesArray, earlyTermination,
				       hintsArray, hintType, verbosity,
				       dcLevel, buildOnionRing, GSHschedule,
				       signalList, statesCoveredList,
				       newCoveredStatesList,
				       statesToRemoveList);
    mdd_free(travstates);
    Ctlp_FormulaFree(tmp_formula);
    frstrchstates = firstReached(fsm, fairStates, fairCondition,
				 careStatesArray, earlyTermination, hintsArray,
				 hintType, verbosity, dcLevel, buildOnionRing,
				 GSHschedule,startstates,rightFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n---Computing coverage for RHS of U formula i.e: ");
      Ctlp_FormulaPrint(vis_stdout,rightFormula);
      fprintf(vis_stdout,
	      "\n------------------------------------------------\n");
    }
    Covstates2 = CoveredStatesImproved(frstrchstates, fsm, rightFormula,
				       fairStates, fairCondition,
				       careStatesArray, earlyTermination,
				       hintsArray, hintType, verbosity,
				       dcLevel, buildOnionRing, GSHschedule,
				       signalList, statesCoveredList,
				       newCoveredStatesList,
				       statesToRemoveList);
    mdd_free(frstrchstates);
    result = mdd_or(Covstates1,Covstates2,1,1);
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(Covstates1);
    mdd_free(Covstates2);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    if (formulaType == Ctlp_AF_c)
      Ctlp_FormulaFree(OrigFormula);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_AND_c:{
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n---Computing coverage for LHS sub-formula: ");
      Ctlp_FormulaPrint(vis_stdout,leftFormula);
      fprintf(vis_stdout,
	      "\n------------------------------------------------\n");
    }
    Covstates1 = CoveredStatesImproved(startstates,fsm, leftFormula,
				       fairStates, fairCondition, 
				       careStatesArray, earlyTermination,
				       hintsArray, hintType, verbosity,
				       dcLevel, buildOnionRing,GSHschedule,
				       signalList, statesCoveredList,
				       newCoveredStatesList,
				       statesToRemoveList);
    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n---Computing coverage for RHS sub-formula: ");
      Ctlp_FormulaPrint(vis_stdout,rightFormula);
      fprintf(vis_stdout,
	      "\n------------------------------------------------\n");
    }
    Covstates2 = CoveredStatesImproved(startstates,fsm, rightFormula,
				       fairStates, fairCondition, 
				       careStatesArray, earlyTermination,
				       hintsArray, hintType, verbosity,
				       dcLevel, buildOnionRing,GSHschedule,
				       signalList, statesCoveredList,
				       newCoveredStatesList,
				       statesToRemoveList);
    result = mdd_or(Covstates1,Covstates2,1,1);
    numresultstates = mdd_count_onset(Fsm_FsmReadMddManager(fsm),result,
				      Fsm_FsmReadPresentStateVars(fsm));
    mdd_free(Covstates1);
    mdd_free(Covstates2);
    temp1 = result;
    result = mdd_and(temp1,fairStates,1,1);
    mdd_free(temp1);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_THEN_c:{ /*f1 -> f2 = !f2 -> !f1*/
    int sigarr;
    array_t *listOfF2Signals = array_alloc(char *,0);
    array_t *listOfF1Signals = array_alloc(char *,0);
    array_t *newstatesToRemoveList = NIL(array_t);
    mdd_t *nextstartstates, *Tb, *tmp_mdd;

    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
    Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
			       fairStates, fairCondition, careStatesArray,
			       earlyTermination, hintsArray, hintType,
			       verbosity, dcLevel, buildOnionRing,GSHschedule);
    Ctlp_FormulaFree(existFormula);
    nextstartstates = mdd_and(startstates, Tb,1,1);
    mdd_free(Tb);
    /*To compute C(So*T(f1),f2),    *
     *first compute states to remove*/
    newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
    findallsignalsInFormula(listOfF2Signals,rightFormula); /*find all signals in f2*/
    for (sigarr=0;sigarr<array_n(listOfF2Signals);sigarr++) {
      /*for all signals in f2*/
      mdd_t *tmp_mdd2;
      char *signalInF2;
      int positionInGlobalList;
      int rangeOfF2SigInF1;
      signalInF2 = array_fetch(char *,listOfF2Signals,sigarr);
      positionInGlobalList = positionOfSignalinList(signalInF2,signalList);
      if (positionInGlobalList < 0) /*shouldn't happen*/
	fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
      rangeOfF2SigInF1 = RangeofSignalinFormula(fsm,signalInF2,leftFormula);
      tmp_mdd = mdd_dup(nextstartstates);
      if (rangeOfF2SigInF1 > 0) { /*signal in F2 also in F1*/
	if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if f1 is propositional*/
	  tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
				   careStatesArray, earlyTermination,
				   hintsArray, hintType, verbosity, dcLevel,
				   buildOnionRing, GSHschedule, signalInF2,
				   tmp_mdd);
	  mdd_free(tmp_mdd);
	  tmp_mdd = tmp_mdd2;
	}
	tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
			       positionInGlobalList);
	if (tmp_mdd2 != NIL(mdd_t))
	  mdd_free(tmp_mdd2);
	array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
		     tmp_mdd);
      } else {
	mdd_free(tmp_mdd);
      }
    }
    Covstates1 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
				       fairStates, fairCondition, 
				       careStatesArray, earlyTermination,
				       hintsArray, hintType, verbosity,
				       dcLevel, buildOnionRing, GSHschedule,
				       signalList, statesCoveredList,
				       newCoveredStatesList,
				       newstatesToRemoveList);
    mdd_free(nextstartstates);
    mdd_array_free(newstatesToRemoveList);
    array_free(listOfF2Signals);
    /*End of coverage computation of f2*/

    /*Now simillar computation for !f1 *
     * Convert f1->f2 to !f2->!f1      */
    leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
    rightFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
    Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
			       fairStates, fairCondition, careStatesArray,
			       earlyTermination, hintsArray, hintType,
			       verbosity, dcLevel, buildOnionRing,GSHschedule);
    Ctlp_FormulaFree(existFormula);
    nextstartstates = mdd_and(startstates, Tb, 1, 1);
    mdd_free(Tb);
    newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
    findallsignalsInFormula(listOfF1Signals,rightFormula);/*find all signals in !f1*/
    for (sigarr=0;sigarr<array_n(listOfF1Signals);sigarr++) {
      /*for all signals in !f1*/
      mdd_t *tmp_mdd2;
      char *signalInNotF1;
      int positionInGlobalList;
      int rangeOfNotF1SigInNotF2;
      signalInNotF1 = array_fetch(char *,listOfF1Signals,sigarr);
      positionInGlobalList = positionOfSignalinList(signalInNotF1,signalList);
      if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
      rangeOfNotF1SigInNotF2 = RangeofSignalinFormula(fsm,signalInNotF1,leftFormula);
      tmp_mdd = mdd_dup(nextstartstates);
      if (rangeOfNotF1SigInNotF2 > 0) {/*signal in !F1 also in !F2*/
	if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if !f2 is propositional*/
	  tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
				   careStatesArray, earlyTermination,
				   hintsArray, hintType, verbosity, dcLevel,
				   buildOnionRing, GSHschedule, signalInNotF1,
				   tmp_mdd);
	  mdd_free(tmp_mdd);
	  tmp_mdd = tmp_mdd2;
	}
	tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
			       positionInGlobalList);
	if (tmp_mdd2 != NIL(mdd_t))
	  mdd_free(tmp_mdd2);
	array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
		     tmp_mdd);
      } else {
	mdd_free(tmp_mdd);
      }
    }
    Ctlp_FormulaFree(leftFormula);
    Covstates2 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
				       fairStates, fairCondition, 
				       careStatesArray, earlyTermination,
				       hintsArray, hintType, verbosity,
				       dcLevel, buildOnionRing,GSHschedule,
				       signalList, statesCoveredList,
				       newCoveredStatesList,
				       newstatesToRemoveList);
    
    mdd_free(nextstartstates);
    mdd_array_free(newstatesToRemoveList);
    array_free(listOfF1Signals);
    /*End of coverage computation of !f1*/
    Ctlp_FormulaFree(rightFormula);
    result = mdd_or(Covstates1,Covstates2,1,1);
    mdd_free(Covstates1);
    mdd_free(Covstates2);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_XOR_c: {
    tmp_formula = Ctlp_FormulaConvertXORtoOR(OrigFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n--Converting XOR to AND and OR from:\n");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      fprintf(vis_stdout,"\nto\n");
      Ctlp_FormulaPrint(vis_stdout, tmp_formula);
      fprintf(vis_stdout,"\n");
    } 
    result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
				   fairCondition, careStatesArray,
				   earlyTermination, hintsArray, hintType,
				   verbosity, dcLevel,buildOnionRing,
				   GSHschedule, signalList, statesCoveredList,
				   newCoveredStatesList, statesToRemoveList);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_EQ_c: {
    tmp_formula = Ctlp_FormulaConvertEQtoOR(OrigFormula);
    if (verbosity > McVerbosityNone_c) {
      fprintf(vis_stdout,"\n--Converting EQ to AND and OR");
      Ctlp_FormulaPrint(vis_stdout,OrigFormula);
      fprintf(vis_stdout,"\nto\n");
      Ctlp_FormulaPrint(vis_stdout, tmp_formula);
      fprintf(vis_stdout,"\n");
    } 
    result = CoveredStatesImproved(startstates, fsm, tmp_formula, fairStates,
				   fairCondition, careStatesArray,
				   earlyTermination, hintsArray, hintType,
				   verbosity, dcLevel,buildOnionRing,
				   GSHschedule, signalList, statesCoveredList,
				   newCoveredStatesList, statesToRemoveList);
    mdd_free(startstates);
    return result;
    break;
  }     
  case Ctlp_OR_c:{  /*f1+f2 = !f1 -> f2 = !f2 -> f1*/
    int sigarr;
    array_t *listOfF2Signals = array_alloc(char *,0);
    array_t *listOfF1Signals = array_alloc(char *,0);
    array_t *newstatesToRemoveList = NIL(array_t);
    mdd_t *nextstartstates, *Tb, *tmp_mdd;
    
    /*To compute C(So*T(!f1),f2),  *
     *convert to form like !f1->f2 */
    leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadLeftChild(OrigFormula));
    rightFormula = Ctlp_FormulaReadRightChild(OrigFormula);
    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
    Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
			       fairStates, fairCondition, careStatesArray,
			       earlyTermination, hintsArray, hintType,
			       verbosity, dcLevel, buildOnionRing,GSHschedule);
    Ctlp_FormulaFree(existFormula);
    nextstartstates = mdd_and(startstates, Tb, 1, 1);
    mdd_free(Tb);
    /*first compute states to remove*/
    newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
    findallsignalsInFormula(listOfF2Signals,rightFormula);/*find all signals in f2*/
    for (sigarr=0;sigarr<array_n(listOfF2Signals);sigarr++) {
      /*for all signals in f2*/
      mdd_t *tmp_mdd2;
      char *signalInF2;
      int positionInGlobalList;
      int rangeOfF2SigInF1;
      signalInF2 = array_fetch(char *,listOfF2Signals,sigarr);
      positionInGlobalList = positionOfSignalinList(signalInF2,signalList);
      if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
      rangeOfF2SigInF1 = RangeofSignalinFormula(fsm,signalInF2,leftFormula);
      tmp_mdd = mdd_dup(nextstartstates);
      if (rangeOfF2SigInF1 > 0) {/*signal in F2 also in F1*/
	if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if f1 is propositional*/
	  tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
				   careStatesArray, earlyTermination,
				   hintsArray, hintType, verbosity, dcLevel,
				   buildOnionRing, GSHschedule, signalInF2,
				   tmp_mdd);
	  mdd_free(tmp_mdd);
	  tmp_mdd = tmp_mdd2;
	}
	tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
			       positionInGlobalList);
	if (tmp_mdd2 != NIL(mdd_t))
	  mdd_free(tmp_mdd2);
	array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
		     tmp_mdd);
      } else {
	mdd_free(tmp_mdd);
      }
    }
    Ctlp_FormulaFree(leftFormula);
    Covstates1 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
				       fairStates, fairCondition, 
				       careStatesArray, earlyTermination,
				       hintsArray, hintType, verbosity,
				       dcLevel, buildOnionRing,GSHschedule,
				       signalList, statesCoveredList,
				       newCoveredStatesList,
				       newstatesToRemoveList);
    mdd_free(nextstartstates);
    mdd_array_free(newstatesToRemoveList);
    array_free(listOfF2Signals);
    /*End of coverage computation of f2*/

    /*Now simillar computation for !f1 *
     * Convert f1+f2 to !f2->f1      */
    leftFormula = Ctlp_FormulaConverttoComplement(Ctlp_FormulaReadRightChild(OrigFormula));
    rightFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    existFormula = Ctlp_FormulaConvertToExistentialForm(leftFormula);
    Tb = Mc_FsmEvaluateFormula(fsm, existFormula,
			       fairStates, fairCondition, careStatesArray,
			       earlyTermination, hintsArray, hintType,
			       verbosity, dcLevel, buildOnionRing,GSHschedule);
    Ctlp_FormulaFree(existFormula);
    nextstartstates = mdd_and(startstates, Tb,1,1);
    mdd_free(Tb);
    newstatesToRemoveList = mdd_array_duplicate(statesToRemoveList);
    findallsignalsInFormula(listOfF1Signals,rightFormula);/*find all signals in f1*/
    for (sigarr=0;sigarr<array_n(listOfF1Signals);sigarr++) {
      /*for all signals in f1*/
      mdd_t *tmp_mdd2;
      char *signalInF1;
      int positionInGlobalList;
      int rangeOfF1SigInF2;
      signalInF1 = array_fetch(char *,listOfF1Signals,sigarr);
      positionInGlobalList = positionOfSignalinList(signalInF1,signalList);
      if (positionInGlobalList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
      rangeOfF1SigInF2 = RangeofSignalinFormula(fsm,signalInF1,leftFormula);
      tmp_mdd = mdd_dup(nextstartstates);
      if (rangeOfF1SigInF2 > 0) {/*signal in !F1 also in !F2*/
	if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) { /*if !f2 is propositional*/
	  tmp_mdd2 = computedepend(fsm, leftFormula, fairStates, fairCondition,
				   careStatesArray, earlyTermination,
				   hintsArray, hintType, verbosity, dcLevel,
				   buildOnionRing, GSHschedule, signalInF1,
				   tmp_mdd);
	  mdd_free(tmp_mdd);
	  tmp_mdd = tmp_mdd2;
	}
	tmp_mdd2 = array_fetch(mdd_t *, newstatesToRemoveList,
			       positionInGlobalList);
	if (tmp_mdd2 != NIL(mdd_t))
	  mdd_free(tmp_mdd2);
	array_insert(mdd_t *,newstatesToRemoveList,positionInGlobalList,
		     tmp_mdd);
      } else {
	mdd_free(tmp_mdd);
      }
    }
    Ctlp_FormulaFree(leftFormula);
    Covstates2 = CoveredStatesImproved(nextstartstates,fsm, rightFormula,
				       fairStates, fairCondition, 
				       careStatesArray, earlyTermination,
				       hintsArray, hintType, verbosity,
				       dcLevel, buildOnionRing,GSHschedule,
				       signalList, statesCoveredList,
				       newCoveredStatesList,
				       newstatesToRemoveList);
    mdd_free(nextstartstates);
    mdd_array_free(newstatesToRemoveList);
    array_free(listOfF1Signals);
    /*End of coverage computation of !f1*/
    
    result = mdd_or(Covstates1,Covstates2,1,1);
    mdd_free(Covstates1);
    mdd_free(Covstates2);
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_NOT_c:{ /*include code for checking for 2 NOTs*/
    leftFormula = Ctlp_FormulaReadLeftChild(OrigFormula);
    if (!(Ctlp_FormulaTestIsQuantifierFree(leftFormula))) {
      tmp_formula = Ctlp_FormulaPushNegation(leftFormula);
      if (verbosity > McVerbosityNone_c) {
	fprintf(vis_stdout,"\n--Pushing down negation one level. Converting formula from:\n");
	Ctlp_FormulaPrint(vis_stdout,OrigFormula);
	fprintf(vis_stdout,"\nto\n");
	Ctlp_FormulaPrint(vis_stdout,tmp_formula);
	fprintf(vis_stdout,"\n");
      }
      Covstates1 = CoveredStatesImproved(startstates,fsm, tmp_formula,
					 fairStates, fairCondition, 
					 careStatesArray, earlyTermination,
					 hintsArray, hintType, verbosity,
					 dcLevel, buildOnionRing,GSHschedule,
					 signalList, statesCoveredList,
					 newCoveredStatesList,
					 statesToRemoveList);
      result = mdd_and(Covstates1,fairStates,1,1);
      Ctlp_FormulaFree(tmp_formula);
      mdd_free(Covstates1);
      mdd_free(startstates);
      return result;
    } else { /*this part of the code is now never executed*/
       fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
       mdd_free(startstates);
       return mdd_zero(Fsm_FsmReadMddManager(fsm));
    }
    break;
  }
  case Ctlp_TRUE_c:
  case Ctlp_FALSE_c: {
    if (verbosity > McVerbosityNone_c)
      fprintf(vis_stdout,"No observable signal, hence no coverage\n");
    result = mdd_zero(Fsm_FsmReadMddManager(fsm));
    mdd_free(startstates);
    return result;
    break;
  }
  case Ctlp_ID_c:{ /*should not reach here*/
    fprintf(vis_stdout, "\n****Error, Should not have reached here\n");
    mdd_free(startstates);
    return mdd_zero(Fsm_FsmReadMddManager(fsm));
    break;
  }
  default:
    fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
    mdd_free(startstates);
    break;
  }
  assert(0);
  return NIL(mdd_t);

} /* End of CoveredStatesImproved */


/**Function********************************************************************

  Synopsis    [Computes the coverage for propositional formulae]

  Description []

  SideEffects [none]

  SeeAlso     [CoveredStatesImproved CoveredStatesHoskote]
  
******************************************************************************/
static 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)
{
  mdd_t *Tb, *result;
  mdd_t *startstates;
  array_t *listOfSignals = array_alloc(char *,0);
  int i,positionInList;
  char *signal;
  Ctlp_Formula_t *tmpFormula;
  
  result = mdd_zero(Fsm_FsmReadMddManager(fsm));
  findallsignalsInFormula(listOfSignals,OrigFormula);
  if (array_n(listOfSignals)==0) {
    if (verbosity > McVerbosityNone_c)
      fprintf(vis_stdout,"No observable signals, hence no coverage\n");
    array_free(listOfSignals);
    return result;
  }
  /*else*/
  startstates = mdd_and(startstates_old,fairStates,1,1);
  tmpFormula = Ctlp_FormulaConvertToExistentialForm(OrigFormula);
  Tb = Mc_FsmEvaluateFormula(fsm, tmpFormula, fairStates,
			     fairCondition, careStatesArray, earlyTermination, 
			     hintsArray, hintType, verbosity, dcLevel,
			     buildOnionRing,GSHschedule);
  Ctlp_FormulaFree(tmpFormula);
  for (i=0;i<array_n(listOfSignals);i++) {
    mdd_t *statesCovered, *newCoveredStates, *statesToRemove, *CovStates, *tmp_mdd, *tmp_mdd2;
    signal = array_fetch(char *,listOfSignals,i);
    positionInList = positionOfSignalinList(signal,signalList);
    if (positionInList < 0) fprintf(vis_stdout,"Serious trouble. Found a new signal!\n");
    statesCovered = array_fetch(mdd_t *,statesCoveredList,positionInList);
    newCoveredStates = array_fetch(mdd_t *,newCoveredStatesList,positionInList);
    statesToRemove = array_fetch(mdd_t *,statesToRemoveList,positionInList);
    CovStates = computedependHoskote(fsm, OrigFormula, fairStates,
				     fairCondition, careStatesArray,
				     earlyTermination, hintsArray,
				     hintType, verbosity, dcLevel,
				     buildOnionRing, GSHschedule,
				     startstates, signal, Tb, statesCovered,
				     newCoveredStates,statesToRemove);
    tmp_mdd = mdd_or(newCoveredStates,CovStates,1,1);
    mdd_free(newCoveredStates);
    array_insert(mdd_t *,newCoveredStatesList,positionInList,tmp_mdd);/*update newCoveredStatesList*/
    tmp_mdd2 = result;
    result = mdd_or(tmp_mdd2,CovStates,1,1);
    mdd_free(tmp_mdd2);
    mdd_free(CovStates);
  }
  mdd_free(Tb);
  mdd_free(startstates);
  array_free(listOfSignals);
  return result;
} /* CoveragePropositional */


/**Function********************************************************************

  Synopsis    [Computes the following for use in coverage computation for 
               propositional formulae:

               computedepend = T(b) ^ T(!b|q->!q)
	      where,
	          T(f) => Set of states satisfying f
		  b is a propositional formula
		  q is an observed signal]

  Description []

  SideEffects [none]

  SeeAlso     [computedependHoskote]

******************************************************************************/
static 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)     
{
  mdd_t *TnotBnotQ, *Covstates, *SoAndTb;
  Ctlp_Formula_t *convertedformula, *tmp_formula, *existFormula;
  SoAndTb = mdd_and(SoAndTb_old,fairStates,1,1); 
  convertedformula = FormulaConvertSignalComplement(fsm,signal,formula);
  if (convertedformula != NIL(Ctlp_Formula_t)) {
    tmp_formula = Ctlp_FormulaConverttoComplement(convertedformula);
    existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
    TnotBnotQ =  Mc_FsmEvaluateFormula(fsm, existFormula,
				       fairStates, fairCondition,
				       careStatesArray, earlyTermination,
				       hintsArray, hintType, verbosity,
				       dcLevel, buildOnionRing,GSHschedule);
    Ctlp_FormulaFree(existFormula);
    Ctlp_FormulaFree(tmp_formula);
  } else {
    TnotBnotQ = mdd_zero(Fsm_FsmReadMddManager(fsm));
  }
  Ctlp_FormulaFree(convertedformula);
  Covstates = mdd_and(SoAndTb,TnotBnotQ,1,1); /*covered states*/
  mdd_free(SoAndTb);
  mdd_free(TnotBnotQ);
  return Covstates;
} /* computedepend */


/**Function********************************************************************

  Synopsis    [Computes the following for use in coverage computation for 
               propositional formulae:

               computedepend = T(b) ^ T(!b|q->!q)
	      where,
	          T(f) => Set of states satisfying f
		  b is a propositional formula
		  q is an observed signal]

  Description []

  SideEffects [none]

  SeeAlso     [computedepend]
  
******************************************************************************/
static 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)     
{
  mdd_t *TnotBnotQ,*Covstates,*startstates,*tmp_mdd, *newCovstates;
  Ctlp_Formula_t *convertedformula;
  startstates = mdd_and(startstates_old,fairStates,1,1); 
  convertedformula = FormulaConvertSignalComplement(fsm,signal,formula);

  if (convertedformula != NIL(Ctlp_Formula_t)) {
    Ctlp_Formula_t *tmp_formula, *tmp_formula2;
    tmp_formula = Ctlp_FormulaConverttoComplement(convertedformula);
    Ctlp_FormulaFree(convertedformula);
    tmp_formula2 = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
    Ctlp_FormulaFree(tmp_formula);
    TnotBnotQ =  Mc_FsmEvaluateFormula(fsm, tmp_formula2, 
				       fairStates, fairCondition,
				       careStatesArray, earlyTermination,
				       hintsArray, hintType, verbosity,
				       dcLevel, buildOnionRing,GSHschedule);
    Ctlp_FormulaFree(tmp_formula2);
  } else {
    TnotBnotQ = mdd_zero(Fsm_FsmReadMddManager(fsm));
  }
  
  tmp_mdd = mdd_and(Tb,TnotBnotQ,1,1);
  mdd_free(TnotBnotQ);
  Covstates = mdd_and(startstates,tmp_mdd,1,1); /*covered states*/
  mdd_free(tmp_mdd);
  tmp_mdd = Covstates;
  mdd_free(startstates);
  Covstates = mdd_and(Covstates, statesToRemove,1,0); /*remove the states to remove*/
  mdd_free(tmp_mdd);
  tmp_mdd = mdd_or(statesCovered,newCoveredStates,1,1);
  newCovstates = mdd_and(Covstates,tmp_mdd,1,0); /* newly covered states*/
  mdd_free(tmp_mdd);
#if 0
  fprintf(vis_stdout,"States covered w.r.t. %s = %0.f , new = %0.f\n",signal,
	    mdd_count_onset(Fsm_FsmReadMddManager(fsm),Covstates,
			    Fsm_FsmReadPresentStateVars(fsm)),
	    mdd_count_onset(Fsm_FsmReadMddManager(fsm),newCovstates,
			    Fsm_FsmReadPresentStateVars(fsm)));
#endif
  mdd_free(newCovstates);  
  return Covstates;

} /* computedependHoskote */


/**Function********************************************************************

  Synopsis    [Computes the following for use in coverage computation for AU:
              traverse(So,f1,f2) = newstartstates(So) U 
	                             traverse(EY(newstartstates(So)),f1,f2)
	       (see function newstartstates for its definition ]

  Description []

  SideEffects []

  SeeAlso     [newstartstates]

******************************************************************************/
static 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)
{
  mdd_t *temp_mdd,*newSo, *Tf1_and_Tnotf2, *newStates, *oldStates, *Tf1, *Tnotf2;
  Ctlp_Formula_t *tmp_formula, *existFormula;
  int travcnt;
  oldStates = mdd_zero(Fsm_FsmReadMddManager(fsm));
  newStates = mdd_zero(Fsm_FsmReadMddManager(fsm));
  newSo = mdd_dup(startstates);
  existFormula = Ctlp_FormulaConvertToExistentialForm(formula1);
  Tf1 = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
			      fairCondition, careStatesArray,
			      earlyTermination, hintsArray,
			      hintType, verbosity, dcLevel,
			      buildOnionRing,GSHschedule);
  Ctlp_FormulaFree(existFormula);
  tmp_formula = Ctlp_FormulaConverttoComplement(formula2);
  existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
  Tnotf2 = Mc_FsmEvaluateFormula(fsm, existFormula, fairStates, fairCondition,
				 careStatesArray, earlyTermination, hintsArray,
				 hintType, verbosity, dcLevel,
				 buildOnionRing, GSHschedule);
  Ctlp_FormulaFree(existFormula);
  Ctlp_FormulaFree(tmp_formula);
  temp_mdd = mdd_and(Tf1,Tnotf2,1,1);
  mdd_free(Tf1);
  mdd_free(Tnotf2);
  Tf1_and_Tnotf2 = mdd_and(temp_mdd,fairStates,1,1);
  mdd_free(temp_mdd);
  temp_mdd = newSo;
  newSo = mdd_and(temp_mdd,Tf1_and_Tnotf2,1,1);
  mdd_free(temp_mdd);
  temp_mdd = newStates;
  newStates = mdd_or(temp_mdd,newSo,1,1);
  mdd_free(temp_mdd);
  travcnt = 0;
  while (!(mdd_equal_mod_care_set_array(newStates,oldStates,careStatesArray))) {
    mdd_t *tmp_mdd = oldStates;
    oldStates = mdd_or(tmp_mdd,newStates,1,1);
    mdd_free(tmp_mdd);
    tmp_mdd = newSo;
    newSo = Mc_FsmEvaluateEYFormula(fsm, tmp_mdd, fairStates, careStatesArray, verbosity, dcLevel);
    mdd_free(tmp_mdd);
    tmp_mdd = newSo;
    newSo = mdd_and(tmp_mdd,Tf1_and_Tnotf2,1,1);
    mdd_free(tmp_mdd);
    tmp_mdd = newStates;
    newStates = mdd_or(tmp_mdd,newSo,1,1);
    mdd_free(tmp_mdd);
  }
  mdd_free(oldStates);
  mdd_free(newSo);
  mdd_free(Tf1_and_Tnotf2);
  return newStates;

} /* traverse */


/**Function********************************************************************

  Synopsis    [Computes the following for use in coverage computation for AU:
              firstReached(So,f2) = (So ^ T(f2)) U 
	                             firstReached(EY(So^T(!f2)),f2)
	      where,
	          T(f2) => Set of states satisfying f2 ]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static 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)
{
  int frstcnt;
  mdd_t *temp1, *temp2, *oldSo, *CovStates, *Tf2, *Tnotf2, *zeroMDD;
  Ctlp_Formula_t *tmp_formula, *existFormula;
  oldSo = mdd_dup(startstates);
  zeroMDD = mdd_zero(Fsm_FsmReadMddManager(fsm));
  existFormula = Ctlp_FormulaConvertToExistentialForm(formula);
  Tf2 =  Mc_FsmEvaluateFormula(fsm, existFormula, fairStates,
			       fairCondition, careStatesArray,
			       earlyTermination, hintsArray,
			       hintType, verbosity,
			       dcLevel, buildOnionRing, GSHschedule);
  Ctlp_FormulaFree(existFormula);
  tmp_formula = Ctlp_FormulaConverttoComplement(formula);
  existFormula = Ctlp_FormulaConvertToExistentialForm(tmp_formula);
  Tnotf2 = Mc_FsmEvaluateFormula(fsm, existFormula,
				 fairStates, fairCondition, 
				 careStatesArray,earlyTermination, 
				 hintsArray, hintType, verbosity, 
				 dcLevel, buildOnionRing,GSHschedule);
  Ctlp_FormulaFree(existFormula);
  Ctlp_FormulaFree(tmp_formula);
  CovStates = mdd_and(oldSo,Tf2,1,1);
  temp1 = mdd_dup(oldSo);
  temp2 = mdd_and(oldSo,Tnotf2,1,1);
  frstcnt = 0;
  while (!(mdd_equal_mod_care_set_array(temp2,zeroMDD,careStatesArray))) {
    mdd_t *tmp_mdd1, *tmp_mdd2, *tmp_mdd;
    tmp_mdd = Mc_FsmEvaluateEYFormula(fsm, temp2, fairStates, careStatesArray, verbosity, dcLevel); /*forward(So^Tnotf2)*/
    tmp_mdd2 = mdd_and(tmp_mdd,Tf2,1,1);
    tmp_mdd1 = CovStates;
    CovStates = mdd_or(CovStates,tmp_mdd2,1,1); /*add on the new states*/
    mdd_free(tmp_mdd1);
    mdd_free(tmp_mdd2);
    tmp_mdd1 = mdd_and(tmp_mdd,Tnotf2,1,1); /*newSo^Tnotf2*/
    tmp_mdd2 = temp2;
    temp2 = mdd_and(tmp_mdd1,temp1,1,0); /*take out the startstates already encountered temp2 = newSo*/
    mdd_free(tmp_mdd2);
    mdd_free(tmp_mdd1);
    tmp_mdd1 = temp1;
    temp1 = mdd_or(temp1,tmp_mdd,1,1);
    mdd_free(tmp_mdd1);
    mdd_free(tmp_mdd);
  }
  mdd_free(zeroMDD);
  mdd_free(oldSo);
  mdd_free(Tf2);
  mdd_free(Tnotf2);
  mdd_free(temp1);
  mdd_free(temp2);
  return CovStates;

} /* firstreached */


/**Function********************************************************************

  Synopsis    [Duplicates a CTL formula but with a given signal's value
  complemented]

  Description []

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static Ctlp_Formula_t *
FormulaConvertSignalComplement(
  Fsm_Fsm_t *fsm,
  char *signal,
  Ctlp_Formula_t *formula)
{
  Ctlp_Formula_t *result = NIL(Ctlp_Formula_t);
  Ctlp_Formula_t *leftChildConverted, *leftFormula;
  Ctlp_Formula_t *rightChildConverted, *rightFormula;
  Ntk_Network_t *network;
  char *nodeNameString;
  char *nodeValueString;
  Ntk_Node_t *node;
  Var_Variable_t *nodeVar;

  if ( formula == NIL(Ctlp_Formula_t)) {
	return NIL(Ctlp_Formula_t);
  }

  if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c )  {
    leftFormula = Ctlp_FormulaReadLeftChild(formula);
    leftChildConverted = FormulaConvertSignalComplement(fsm, signal,
							leftFormula);
    rightFormula = Ctlp_FormulaReadRightChild(formula);
    rightChildConverted = FormulaConvertSignalComplement(fsm, signal,
							 rightFormula);
    result = Ctlp_FormulaCreate(Ctlp_FormulaReadType(formula),
				leftChildConverted,rightChildConverted);
  }
  else { /* if atomic proposition*/
    network = Fsm_FsmReadNetwork(fsm);
    nodeNameString = Ctlp_FormulaReadVariableName(formula);
    nodeValueString = Ctlp_FormulaReadValueName(formula);
    node = Ntk_NetworkFindNodeByName(network, nodeNameString);
    nodeVar = Ntk_NodeReadVariable(node);
    if ((strcmp(signal,nodeNameString)) != 0) { /* not the signal that we want to flip */
      result = Ctlp_FormulaCreate(Ctlp_FormulaReadType(formula),
				  (Ctlp_Formula_t *) util_strsav(nodeNameString),
				  (Ctlp_Formula_t *) util_strsav(nodeValueString));
    }
    else { /* this is the signal that we want to flip */
      result  = Ctlp_FormulaConverttoComplement(formula);
    }
  }
  return result;
} /* FormulaConvertSignalComplement */


/**Function********************************************************************

  Synopsis    [Used in the coverage code to gather all possible observable
               signals in a given formula and create necessary arrays]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static 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)
{
  Ntk_Network_t *network;
  Ntk_Node_t *node;
  Var_Variable_t *nodeVar;
  char *nodeNameString;
  int signalType;
  Ctlp_Formula_t *leftFormula, *rightFormula;
  if ( formula == NIL(Ctlp_Formula_t)) {
	return;
  }

  if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c )  {
    leftFormula = Ctlp_FormulaReadLeftChild(formula);
    rightFormula = Ctlp_FormulaReadRightChild(formula);
    findallsignals(fsm, signalTypeList, signalList, statesCoveredList,
		   newCoveredStatesList, statesToRemoveList,
		   leftFormula, zeroMdd);
    findallsignals(fsm, signalTypeList, signalList, statesCoveredList,
		   newCoveredStatesList, statesToRemoveList,
		   rightFormula,zeroMdd);
  }
  else { /* atomic proposition */
    nodeNameString = Ctlp_FormulaReadVariableName(formula);
    if ((positionOfSignalinList(nodeNameString,signalList)) == -1) {
      fprintf(vis_stdout,"Found new signal = %s\n",nodeNameString);
      network = Fsm_FsmReadNetwork(fsm);
      node = Ntk_NetworkFindNodeByName(network, nodeNameString);
      nodeVar = Ntk_NodeReadVariable(node);
      if (Var_VariableTestIsPI(nodeVar))
	signalType = 1;
      else if (Var_VariableTestIsPO(nodeVar))
	signalType = 0;
      else
	signalType = 2;
      array_insert_last(int,signalTypeList,signalType);
      array_insert_last(char *,signalList,nodeNameString);
      array_insert_last(mdd_t *,statesCoveredList,mdd_dup(zeroMdd));
      array_insert_last(mdd_t *,newCoveredStatesList,mdd_dup(zeroMdd));
      array_insert_last(mdd_t *,statesToRemoveList,mdd_dup(zeroMdd));
    }
  }
  return;
} /* findallsignals */


/**Function********************************************************************

  Synopsis    [Used in the coverage code to gather all possible observable
               signals in a given formula]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
findallsignalsInFormula(
  array_t *signalList,
  Ctlp_Formula_t *formula)
{
  char *nodeNameString;

  Ctlp_Formula_t *leftFormula, *rightFormula;
  if ( formula == NIL(Ctlp_Formula_t)) {
    return;
  }

  if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c )  {
    leftFormula = Ctlp_FormulaReadLeftChild(formula);
    rightFormula = Ctlp_FormulaReadRightChild(formula);
    findallsignalsInFormula(signalList,leftFormula);
    findallsignalsInFormula(signalList,rightFormula);
  }
  else { /* atomic proposition */
    nodeNameString = Ctlp_FormulaReadVariableName(formula);
    if ((positionOfSignalinList(nodeNameString,signalList)) == -1) {
      array_insert_last(char *,signalList,nodeNameString); 
    }
  }
  return;
} /* findallsignalsInFormula */


/**Function********************************************************************

  Synopsis    [Used in the coverage code to find the index of a signal in an
               array of signals previously collected]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
positionOfSignalinList(
  char *signal,
  array_t *signalList)
{
  int arraysize = array_n(signalList);
  int i;

  for (i=0;i<arraysize;i++) {
    if (strcmp(signal,array_fetch(char *,signalList,i)) == 0)
      return i;
  }
  return -1;
} /* positionOfSignalinList */


/**Function********************************************************************

  Synopsis    [Finds the range of values that a given observed signal can take
               in a CTL formula]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
RangeofSignalinFormula(
  Fsm_Fsm_t *fsm,
  char *signal,
  Ctlp_Formula_t *formula)
{
  Ntk_Network_t *network;
  char *nodeNameString;
  char *nodeValueString;
  Ntk_Node_t *node;
  Ctlp_Formula_t *leftFormula;
  Ctlp_Formula_t *rightFormula;
 
  Var_Variable_t *nodeVar;
  int range_left,range_right;
  int range = 0;
  /*nodeVar = Ntk_NodeReadVariable(node);*/
  
  if ( formula == NIL(Ctlp_Formula_t)) {
    return range;
  }

  if (Ctlp_FormulaReadType(formula) != Ctlp_ID_c )  {
    leftFormula = Ctlp_FormulaReadLeftChild(formula);
    range_left = RangeofSignalinFormula(fsm, signal, leftFormula);
#if 0
    Ctlp_FormulaFree(leftFormula);
#endif
    rightFormula = Ctlp_FormulaReadRightChild (formula);
    range_right = RangeofSignalinFormula(fsm, signal, rightFormula);
#if 0
    Ctlp_FormulaFree(rightFormula);
#endif
    if (range_left==range_right) /* to avoid situation where signal exists on both sides of formula*/
      range = range_left;
    else
      range = range_right+range_left; /* 0 + some value */
  }
  else {
    network = Fsm_FsmReadNetwork(fsm);
    nodeNameString = Ctlp_FormulaReadVariableName(formula);
    nodeValueString = Ctlp_FormulaReadValueName(formula);
    node = Ntk_NetworkFindNodeByName(network, nodeNameString);
    nodeVar = Ntk_NodeReadVariable(node);
    if ((strcmp(signal,nodeNameString)) != 0) { 
      range = 0;
    }
    else { 
      range = Var_VariableReadNumValues(nodeVar);
    }
  }
  return range;
} /* RangeofSignalinFormula */