/**CHeaderFile*****************************************************************

  FileName    [mcInt.h]

  PackageName [mc]

  Synopsis    [Internal declarations.]

  Author      [Adnan Aziz and Tom Shiple, In-Ho Moon]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

  Revision    [$Id: mcInt.h,v 1.51 2008/04/22 21:24:49 fabio Exp $]

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

#ifndef _MCINT
#define _MCINT

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
#include "heap.h"
#include "ntm.h"
#include "part.h"
#include "mc.h"
#include <string.h>


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

#define McMaxStringLength_c 1000


/**Enum************************************************************************

  Synopsis    [Level to which debugging of CTL formulae is performed.]

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

typedef enum {
  McDbgLevelNone_c,
  McDbgLevelMin_c,
  McDbgLevelMinVerbose_c,
  McDbgLevelMax_c,
  McDbgLevelInteractive_c
} McDbgLevel;

/**Enum************************************************************************

  Synopsis    [Trimming mode for the enqueued sets of states.]

  Description []

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

typedef enum {
  McLS_none_c, /* do not apply any trimming */
  McLS_G_c,    /* apply EG to set of states */
  McLS_H_c,    /* apply EH to set of states */
  McLS_GH_c    /* apply both EG and EH to set of states */
} McLockstepMode;


/**Enum************************************************************************

  Synopsis    [SCC generator status.]

  Description [SCC generator status.  Empty means that there are no more
  fair SCCs to be enumerated.]

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

typedef enum {
  McSccGenEmpty_c,
  McSccGenNonEmpty_c
} McSccGenStatus;


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/**Struct**********************************************************************

  Synopsis    [A struct for representing a paths.]

  Description [Structure consists of two arrays of mdd's - the stem,
  and the cycle (possibley empty if we are dealing with finite paths)]

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

struct McPathStruct {
  array_t *stemArray; /* represents a sequence of mdd's each corresponding to
                       * a state, for the finite segment of the path
                       */

  array_t *cycleArray; /* represents a sequence of mdd's each corresponding to
                        * a state, for the cycle of the path
                        */
};

/**Struct**********************************************************************

  Synopsis    [A struct for keeping the command line options.]

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

struct McOptionsStruct {
  boolean useMore;      /* use more as pipe for debug output */
  boolean reduceFsm;
  boolean printInputs;
  boolean useFormulaTree;
  boolean vd;   
  boolean beer;   
  boolean simFormat;
  boolean FAFWFlag;
  FILE *ctlFile;
  FILE *guideFile;      /* file with hints (null if no guided search) */
  FILE *systemFile;      /* file with system controlled variable for FAFW */
  FILE *debugFile;
  Mc_FwdBwdAnalysis fwdBwd;
  Mc_LeMethod_t leMethod;
  Mc_DcLevel dcLevel;
  McDbgLevel dbgLevel;
  Mc_GSHScheduleType schedule;
  int lockstep;
  Mc_VerbosityLevel verbosityLevel;
  int timeOutPeriod;
  boolean doCoverageHoskote;
  boolean doCoverageImproved;
  /* The following options are related with ARDC */
  Fsm_ArdcOptions_t *ardcOptions;
  Fsm_RchType_t invarApproxFlag; /* the type of reachability analysis for
				    invariant checking */
  boolean invarOnionRingsFlag; /* flag to indicate whether onion rings should
				  be kept during reahability analysis */
  /* The following option is for forward traversal */
  Mc_FwdBwdAnalysis traversalDirection;
  boolean incre; /* flag for incremental SAT solver in PureSAT*/
  boolean sss; /* flag for SSS/Interpolation, 0 for ip, 1 for SSS*/
  boolean flatIP; /* flag for flat interpolation algorithm*/
  int IPspeed; /*enable various speed up techniques for PureSat+IP algorithm*/
};

/**Struct**********************************************************************

  Synopsis [Keeps info on early termination: you can stop model
  checking if you have some or all of the states]

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

struct McEarlyTerminationStruct {
  Mc_EarlyTerminationType mode;
  mdd_t *states;
};

/**Struct**********************************************************************

  Synopsis    [Fair SCC generator.]

  Description []

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

struct McSccGenStruct {
  McSccGenStatus status;
  Fsm_Fsm_t *fsm;
  Heap_t *heap;
  array_t *rings;		/* of mdd_t */
  array_t *buechiFairness;	/* of mdd_t */
  boolean earlyTermination;
  Mc_VerbosityLevel verbosity;
  Mc_DcLevel dcLevel;
  int fairSccsFound;
  int totalExamined;
  int nImgComps;
  int nPreComps;
};

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

typedef struct McPathStruct McPath_t;
typedef struct McOptionsStruct McOptions_t;

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

#define GET_NORMAL_PT(_pt) ((mdd_t *)((unsigned long)(_pt) & ~01L))

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

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

EXTERN int McFsmDebugFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, Fsm_Fsm_t *modelFsm, array_t *careSetArray);
EXTERN void McFsmStateDebugFormula(McOptions_t *options, Ctlp_Formula_t *ctlFormula, mdd_t *aState, Fsm_Fsm_t *modelFsm, array_t *careSetArray);
EXTERN McPath_t * McBuildFairPath(mdd_t *startState, mdd_t *invariantStates, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, Mc_FwdBwdAnalysis fwdBwd);
EXTERN mdd_t* McFsmEvaluateEGFormulaUsingGSH(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, Mc_GSHScheduleType schedule);
EXTERN mdd_t* McFsmEvaluateEHFormulaUsingGSH(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, Mc_GSHScheduleType schedule);
EXTERN mdd_t * McEvaluateEUFormulaWithGivenTR(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
EXTERN mdd_t * McEvaluateAUFormulaWithGivenTR(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
EXTERN mdd_t * McEvaluateESFormulaWithGivenTR(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
EXTERN mdd_t * McEvaluateEGFormulaWithGivenTR(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
EXTERN mdd_t * McEvaluateEHFormulaWithGivenTR(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
EXTERN mdd_t * McEvaluateESFormulaWithGivenTRWithTarget( Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint);
EXTERN mdd_t * McEvaluateESFormulaWithGivenTRFAFW( Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, mdd_t *Swin);
EXTERN void McFormulaFreeDebugData(Ctlp_Formula_t *formula);
EXTERN void _McPrintSatisfyingMinterms(mdd_t *aMdd, Fsm_Fsm_t *fsm);
EXTERN mdd_t * McFsmComputeFairSCCsByLockStep(Fsm_Fsm_t *fsm, int maxNumberOfSCCs, array_t *SCCs, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
EXTERN mdd_t * McFsmRefineFairSCCsByLockStep(Fsm_Fsm_t *fsm, int maxNumberOfSCCs, array_t *SCCs, array_t *sccClosedSets, array_t *careStates, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
EXTERN mdd_t * McFsmRefineWeakFairSCCs(Fsm_Fsm_t *modelFsm, mdd_t *sccClosedSet, array_t *modelCareStatesArray, array_t *arrayOfOnionRings,boolean isSccTerminal,int dcLevel, int verbosity);
EXTERN mdd_t * McFsmComputeOneFairSccByLinearStep(Fsm_Fsm_t *fsm, Heap_t *priorityQueue, array_t *buechiFairness, array_t *onionRings, boolean earlyTermination, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int *sccExamined);
EXTERN mdd_t * McFsmComputeOneFairSccByLockStep(Fsm_Fsm_t *fsm, Heap_t *priorityQueue, array_t *buechiFairness, array_t *onionRings, boolean earlyTermination, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int *sccExamined);
EXTERN array_t * McCompletePathFwd(mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
EXTERN array_t * McCompletePathBwd(mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
EXTERN int McCommandInitState(Hrc_Manager_t **hmgr, int argc, char **argv);
EXTERN char * McStatePrintAsFormula(mdd_t *aMinterm, array_t *aSupport, Fsm_Fsm_t *modelFsm);
EXTERN int McComputeOnionRingsWithClosestCore(mdd_t *aState, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm);
EXTERN array_t * McRemoveIndexedOnionRings(int index, array_t *arrayOfOnionRings);
EXTERN array_t * McConvertMintermToValueArray(mdd_t *aMinterm, array_t *aSupport, mdd_manager *mddMgr);
EXTERN void McPrintTransition(mdd_t *aState, mdd_t *bState, mdd_t *uInput, mdd_t *vInput, array_t *stateSupport, array_t *inputSupport, boolean printInputs, Fsm_Fsm_t *modelFsm, int seqNumber);
EXTERN void McPrintTransitionAiger(mdd_t *aState, mdd_t *bState, mdd_t *uInput, mdd_t *vInput, array_t *stateSupport, array_t *inputSupport, boolean printInputs, Fsm_Fsm_t *modelFsm, int seqNumber);
EXTERN void McStatePassesFormula(mdd_t *aState, Ctlp_Formula_t *formula, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm);
EXTERN void McStateFailsFormula(mdd_t *aState, Ctlp_Formula_t *formula, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm);
EXTERN void McStatePassesOrFailsFormula(mdd_t *aState, Ctlp_Formula_t *formula, int pass, McDbgLevel debugLevel, Fsm_Fsm_t *modelFsm);
EXTERN McPath_t * McPathNormalize(McPath_t *aPath);
EXTERN array_t * McCreateMergedPath(array_t *aPath, array_t *bPath);
EXTERN array_t * McCreateJoinedPath(array_t *aPath, array_t *bPath);
EXTERN boolean McStateSatisfiesFormula(Ctlp_Formula_t *aFormula, mdd_t *aState);
EXTERN boolean McStateTestMembership(mdd_t *aState, mdd_t *setOfStates);
EXTERN mdd_t * McGetSuccessorInTarget(mdd_t *aState, mdd_t *targetStates, Fsm_Fsm_t *modelFsm);
EXTERN mdd_t * McGetSuccessorInTargetAmongFairStates(mdd_t *aState, mdd_t *targetStates, array_t *arrayOfOnionRings, Fsm_Fsm_t *modelFsm);
EXTERN array_t * McPathReadStemArray(McPath_t *aPath);
EXTERN array_t * McPathReadCycleArray(McPath_t *aPath);
EXTERN void McPathSetStemArray(McPath_t *aPath, array_t *stemArray);
EXTERN void McPathSetCycleArray(McPath_t *aPath, array_t *cycleArray);
EXTERN McPath_t * McPathAlloc(void);
EXTERN void McPathFree(McPath_t * aPath);
EXTERN McOptions_t * McOptionsAlloc(void);
EXTERN void McOptionsFree(McOptions_t *options);
EXTERN Mc_LeMethod_t McOptionsReadLeMethod(McOptions_t *options);
EXTERN McDbgLevel McOptionsReadDbgLevel(McOptions_t *options);
EXTERN FILE * McOptionsReadGuideFile(McOptions_t *options);
EXTERN FILE * McOptionsReadSystemFile(McOptions_t *options);
EXTERN int McOptionsReadTimeOutPeriod(McOptions_t *options);
EXTERN Mc_VerbosityLevel McOptionsReadVerbosityLevel(McOptions_t *options);
EXTERN Mc_DcLevel McOptionsReadDcLevel(McOptions_t *options);
EXTERN FILE * McOptionsReadCtlFile(McOptions_t *options);
EXTERN FILE * McOptionsReadDebugFile(McOptions_t *options);
EXTERN int McOptionsReadSimValue(McOptions_t *options);
EXTERN int McOptionsReadUseMore(McOptions_t *options);
EXTERN int McOptionsReadReduceFsm(McOptions_t *options);
EXTERN int McOptionsReadPrintInputs(McOptions_t *options);
EXTERN boolean McOptionsReadUseFormulaTree(McOptions_t *options);
EXTERN Mc_GSHScheduleType McOptionsReadSchedule(McOptions_t *options);
EXTERN int McOptionsReadLockstep(McOptions_t *options);
EXTERN Fsm_RchType_t McOptionsReadInvarApproxFlag(McOptions_t *options);
EXTERN boolean McOptionsReadInvarOnionRingsFlag(McOptions_t *options);
EXTERN Mc_FwdBwdAnalysis McOptionsReadFwdBwd(McOptions_t *options);
EXTERN Mc_FwdBwdAnalysis McOptionsReadTraversalDirection(McOptions_t *options);
EXTERN Fsm_ArdcOptions_t * McOptionsReadArdcOptions(McOptions_t *options);
EXTERN int McOptionsReadCoverageHoskote(McOptions_t *options);
EXTERN int McOptionsReadCoverageImproved(McOptions_t *options);
EXTERN void McOptionsSetFwdBwd(McOptions_t *options, Mc_FwdBwdAnalysis fwdBwd);
EXTERN void McOptionsSetGuideFile(McOptions_t *options, FILE *guideFile);
EXTERN void McOptionsSetTraversalDirection(McOptions_t *options, Mc_FwdBwdAnalysis fwdBwd);
EXTERN void McOptionsSetUseMore(McOptions_t *options, boolean useMore);
EXTERN void McOptionsSetReduceFsm(McOptions_t *options, boolean reduceFsm);
EXTERN void McOptionsSetPrintInputs(McOptions_t *options, boolean printInputs);
EXTERN void McOptionsSetUseFormulaTree(McOptions_t *options, boolean useFormulaTree);
EXTERN void McOptionsSetSchedule(McOptions_t *options, Mc_GSHScheduleType schedule);
EXTERN void McOptionsSetLockstep(McOptions_t *options, int lockstep);
EXTERN void McOptionsSetSimValue(McOptions_t *options, boolean simValue);
EXTERN void McOptionsSetDbgLevel(McOptions_t *options, McDbgLevel dbgLevel);
EXTERN void McOptionsSetVerbosityLevel(McOptions_t *options, Mc_VerbosityLevel verbosityLevel);
EXTERN void McOptionsSetLeMethod(McOptions_t *options, Mc_LeMethod_t leMethod);
EXTERN void McOptionsSetDcLevel(McOptions_t *options, Mc_DcLevel dcLevel);
EXTERN void McOptionsSetArdcOptions(McOptions_t *options, Fsm_ArdcOptions_t *ardcOptions);
EXTERN void McOptionsSetInvarOnionRingsFlag(McOptions_t *options, int shellFlag);
EXTERN void McOptionsSetCtlFile(McOptions_t *options, FILE *file);
EXTERN void McOptionsSetDebugFile(McOptions_t *options, FILE *file);
EXTERN void McOptionsSetTimeOutPeriod(McOptions_t *options, int timeOutPeriod);
EXTERN void McOptionsSetInvarApproxFlag(McOptions_t *options, Fsm_RchType_t approxFlag);
EXTERN void McOptionsSetCoverageHoskote(McOptions_t *options, boolean doCoverageHoskote);
EXTERN void McOptionsSetCoverageImproved(McOptions_t *options, boolean doCoverageImproved);
EXTERN void McOptionsSetVacuityDetect(McOptions_t *options, boolean vd);
EXTERN boolean McOptionsReadVacuityDetect(McOptions_t *options);
EXTERN void McOptionsSetBeerMethod(McOptions_t *options, boolean beer);
EXTERN int McOptionsReadBeerMethod(McOptions_t *options);
EXTERN void McOptionsSetFAFWFlag(McOptions_t *options, boolean FAFWFlag);
EXTERN void McOptionsSetVariablesForSystem(McOptions_t *options, FILE  *systemFile);
EXTERN boolean McQueryContinue(char *query);
EXTERN void McPrintSupport(mdd_t *aMdd, mdd_manager *mddMgr, Ntk_Network_t *aNetwork);
EXTERN int McPrintSimPath(FILE *outputFile, array_t *aPath, Fsm_Fsm_t *modelFsm);
EXTERN Fsm_Fsm_t * McConstructReducedFsm(Ntk_Network_t *network, array_t *ctlFormulaArray);
EXTERN Mc_EarlyTermination_t * McObtainUpdatedEarlyTerminationCondition(Mc_EarlyTermination_t *earlyTermination, mdd_t *careStates, Ctlp_FormulaType formulaType);
EXTERN boolean McCheckEarlyTerminationForUnderapprox(Mc_EarlyTermination_t *earlyTermination, mdd_t *underApprox, array_t *careStatesArray);
EXTERN boolean McCheckEarlyTerminationForOverapprox(Mc_EarlyTermination_t *earlyTermination, mdd_t *overApprox, array_t *careStatesArray);
EXTERN mdd_t * McComputeACloseMinterm(mdd_t *aSet, mdd_t *target, array_t *Support, mdd_manager *mddMgr);
EXTERN mdd_t * McComputeACloseState(mdd_t *states, mdd_t *target, Fsm_Fsm_t *modelFsm);
EXTERN Mc_GSHScheduleType McStringConvertToScheduleType(char *string);
EXTERN int McStringConvertToLockstepMode(char *string);
EXTERN array_t *McMddArrayDuplicateFAFW(array_t *aPath);
EXTERN void McNormalizeBddPointer(array_t *bddArray);

EXTERN mdd_t *McMddArrayAnd(array_t *mddArray);
EXTERN mdd_t *McMddArrayOr(array_t *mddArray);
EXTERN mdd_t *McComputeAbstractStates(Fsm_Fsm_t *absFsm, mdd_t *reachableStates);
EXTERN boolean McGetDncEnabled(void);
EXTERN array_t * Mc_BuildForwardRings(mdd_t *S, Fsm_Fsm_t *fsm, array_t *onionRings); 
EXTERN void Mc_CheckPathToCore(Fsm_Fsm_t *fsm, array_t *pathToCore);
EXTERN void Mc_CheckPathFromCore(Fsm_Fsm_t *fsm, array_t *pathFromCore);
EXTERN void Mc_PrintStates( Fsm_Fsm_t *modelFsm, mdd_t *states);
EXTERN void Mc_PrintNumStates( Fsm_Fsm_t *modelFsm, mdd_t *states);
EXTERN void Mc_PrintRings( Fsm_Fsm_t *modelFsm, array_t *onionRings);
EXTERN void Mc_PrintNumRings( Fsm_Fsm_t *modelFsm, array_t *onionRings);
EXTERN boolean McPrintPassFail(mdd_manager *mddMgr, Fsm_Fsm_t *modelFsm, Mc_FwdBwdAnalysis traversalDirection, Ctlp_Formula_t *ctlFormula, mdd_t *ctlFormulaStates, mdd_t *modelInitialStates, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity);
EXTERN mdd_t * McModelCheckAtomicFormula(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula);
EXTERN void InvarPrintDebugInformation(Fsm_Fsm_t *modelFsm, array_t *invarFormulaArray, array_t *invarStatesArray, int *resultArray, McOptions_t *options, array_t *hintsStatesArray);
EXTERN array_t * SortFormulasByFsm(Fsm_Fsm_t *totalFsm, array_t *invarFormulaArray, array_t *fsmArray, McOptions_t *options);
EXTERN int TestInvariantsInTotalFsm(Fsm_Fsm_t *totalFsm, array_t *invarStatesArray, int shellFlag);
EXTERN 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);
EXTERN 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);
EXTERN Ctlp_Approx_t ComputeResultingApproximation(Ctlp_FormulaType formulaType, Ctlp_Approx_t leftApproxType, Ctlp_Approx_t rightApproxType, Ctlp_Approx_t TRMinimization, Mc_EarlyTermination_t *earlyTermination, boolean fixpoint);
EXTERN void McVacuityDetection(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, mdd_t *modelInitialStates, McOptions_t *options);

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

#endif /* _MCINT */