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

  FileName    [fsm.h]

  PackageName [fsm]

  Synopsis    [Finite state machine abstraction of a network.]

  Description [A finite state machine contains a pointer to a network, so it
  inherits all the information that is contained in the network, such as node
  names and MDD ids.  An FSM has a partition associated with it; the output
  and next state functions are derived from the partition.  This partition
  does not necessarily have to be the default partition associated with the
  network.<p>

  The FSM maintains information relating to state reachability
  (initial states, reachable states, underapprox or not, and the
  partition of reachable states into "onion rings"), and fairness
  information (fair states, fairness constraints, and generic
  debugging information).  Also, the FSM stores the MDD ids of present
  state, next state, and input variables, in a convenient format.]

  Author [Shaker Sarwary, Tom Shiple, Rajeev Ranjan, Kavita Ravi, 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: fsm.h,v 1.76 2005/05/13 08:30:30 hhhan Exp $]

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

#ifndef _FSM
#define _FSM

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
#include "img.h"
#include "ctlp.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
#define FSM_NETWORK_APPL_KEY "Fsm_NetworkApplKey"
#define Fsm_Rch_Default_c Fsm_Rch_Bfs_c

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef struct FsmFsmStruct Fsm_Fsm_t;
typedef struct FsmFairnessStruct Fsm_Fairness_t;
typedef struct FsmArdcOptionsStruct Fsm_ArdcOptions_t;
typedef struct FsmHdTravOptions FsmHdTravOptions_t;
typedef array_t Fsm_HintsArray_t;

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

  Synopsis [Specifies type of reachability computation.]

  Description [Specifies type of reachability
  computation. Fsm_Rch_Bfs_c specifies normal BFS. Fsm_Rch_Hd_c
  specifies HD computation (Ravi & Somenzi ICCAD95). Fsm_Rch_Oa_c
  specified Approximate reachability analysis first published by Cho
  in EDAC'93. Fsm_Rch_PureSat_c is first published by Bing Li in BMC'03 ]

  SideEffects []

  SeeAlso []
  
******************************************************************************/
typedef enum {
    Fsm_Rch_Bfs_c,
    Fsm_Rch_Gs_c,
    Fsm_Rch_Hd_c,
    Fsm_Rch_Oa_c,
    Fsm_Rch_Grab_c,
    Fsm_Rch_PureSat_c
} Fsm_RchType_t;

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

  Synopsis [Specifies the status of reachable states.]

  Description [Specifies the status of reachable states.]

  SideEffects []

  SeeAlso []
  
******************************************************************************/
typedef enum {
    Fsm_Rch_Exact_c,
    Fsm_Rch_Under_c,
    Fsm_Rch_Over_c
} Fsm_RchStatus_t;

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

  Synopsis [Specifies type of dead-end computation.]

  Description [Specifies type of dead-end computation. Fsm_Hd_DE_BF_c
  implies computation of the entire Reached set. Fsm_Hd_DE_Con_c
  specifies dead-end computation by decomposing Reached in terms of
  disjunctive factors.  Fsm_Hd_DE_Hyb_c first tries to extract a
  subset of Reached to compute its image. If no new states are found,
  it computes the image of Reached by decomposing it into disjunctive
  parts.]


  SideEffects []

  SeeAlso []
  
******************************************************************************/
typedef enum {
  Fsm_Hd_DE_BF_c,
  Fsm_Hd_DE_Con_c,
  Fsm_Hd_DE_Hyb_c
} Fsm_HdDeadEndType_t;

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

  Synopsis [Specifies type of approximate FSM traversal.]

  Description [Specifies type of approximate FSM traversal.]

  SideEffects []

  SeeAlso []
  
******************************************************************************/
typedef enum {
  Fsm_Ardc_Traversal_Mbm_c,
  Fsm_Ardc_Traversal_Rfbf_c,
  Fsm_Ardc_Traversal_Tfbf_c,
  Fsm_Ardc_Traversal_Tmbm_c,
  Fsm_Ardc_Traversal_Lmbm_c,
  Fsm_Ardc_Traversal_Tlmbm_c,
  Fsm_Ardc_Traversal_Simple_c
} Fsm_Ardc_TraversalType_t;

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

  Synopsis [Specifies type of what-to-constrain.]

  Description [Specifies type of what-to-constrain.]

  SideEffects []

  SeeAlso []
  
******************************************************************************/
typedef enum {
  Fsm_Ardc_Constrain_Tr_c, /* Tr : transition relation */
  Fsm_Ardc_Constrain_Initial_c,
  Fsm_Ardc_Constrain_Both_c
} Fsm_Ardc_ConstrainTargetType_t;

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

  Synopsis [Specifies type of when to abstract pseudo PIs.]

  Description [Specifies type of when to abstract pseudo PIs.]

  SideEffects []

  SeeAlso []
  
******************************************************************************/
typedef enum {
  Fsm_Ardc_Abst_Ppi_No_c,
  Fsm_Ardc_Abst_Ppi_Before_Image_c,
  Fsm_Ardc_Abst_Ppi_After_Image_c,
  Fsm_Ardc_Abst_Ppi_At_End_c
} Fsm_Ardc_AbstPpiType_t;

#include "mc.h"

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

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

EXTERN void Fsm_ArdcMinimizeTransitionRelation(Fsm_Fsm_t *fsm, Img_DirectionType fwdbwd);
EXTERN mdd_t * Fsm_ArdcComputeImage(Fsm_Fsm_t *fsm, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
EXTERN array_t * Fsm_FsmComputeOverApproximateReachableStates(Fsm_Fsm_t *fsm, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, int recompute);
EXTERN array_t * Fsm_ArdcComputeOverApproximateReachableStates(Fsm_Fsm_t *fsm, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, int recompute, Fsm_ArdcOptions_t *options);
EXTERN array_t * Fsm_ArdcDecomposeStateSpace(Ntk_Network_t *network, array_t *presentStateVars, array_t *nextStateFunctions, Fsm_ArdcOptions_t *options);
EXTERN Fsm_ArdcOptions_t * Fsm_ArdcAllocOptionsStruct(void);
EXTERN void Fsm_ArdcGetDefaultOptions(Fsm_ArdcOptions_t *options);
EXTERN Fsm_Ardc_TraversalType_t Fsm_ArdcOptionsReadTraversalMethod(Fsm_ArdcOptions_t *options);
EXTERN int Fsm_ArdcOptionsReadGroupSize(Fsm_ArdcOptions_t *options);
EXTERN float Fsm_ArdcOptionsReadAffinityFactor(Fsm_ArdcOptions_t *options);
EXTERN Img_MinimizeType Fsm_ArdcOptionsReadConstrainMethod(Fsm_ArdcOptions_t *options);
EXTERN Fsm_Ardc_ConstrainTargetType_t Fsm_ArdcOptionsReadConstrainTarget(Fsm_ArdcOptions_t *options);
EXTERN int Fsm_ArdcOptionsReadMaxIteration(Fsm_ArdcOptions_t *options);
EXTERN Fsm_Ardc_AbstPpiType_t Fsm_ArdcOptionsReadAbstractPseudoInput(Fsm_ArdcOptions_t *options);
EXTERN boolean Fsm_ArdcOptionsReadDecomposeFlag(Fsm_ArdcOptions_t *options);
EXTERN boolean Fsm_ArdcOptionsReadProjectedInitialFlag(Fsm_ArdcOptions_t *options);
EXTERN boolean Fsm_ArdcOptionsReadConstrainReorderFlag(Fsm_ArdcOptions_t *options);
EXTERN Img_MethodType Fsm_ArdcOptionsReadImageMethod(Fsm_ArdcOptions_t *options);
EXTERN boolean Fsm_ArdcOptionsReadUseHighDensity(Fsm_ArdcOptions_t *options);
EXTERN int Fsm_ArdcOptionsReadVerbosity(Fsm_ArdcOptions_t *options);
EXTERN void Fsm_ArdcOptionsSetTraversalMethod(Fsm_ArdcOptions_t *options, Fsm_Ardc_TraversalType_t traversalMethod);
EXTERN void Fsm_ArdcOptionsSetGroupSize(Fsm_ArdcOptions_t *options, int groupSize);
EXTERN void Fsm_ArdcOptionsSetAffinityFactor(Fsm_ArdcOptions_t *options, float affinityFactor);
EXTERN void Fsm_ArdcOptionsSetConstrainMethod(Fsm_ArdcOptions_t *options, Img_MinimizeType constrainMethod);
EXTERN void Fsm_ArdcOptionsSetConstrainTarget(Fsm_ArdcOptions_t *options, Fsm_Ardc_ConstrainTargetType_t constrainTarget);
EXTERN void Fsm_ArdcOptionsSetMaxIteration(Fsm_ArdcOptions_t *options, int maxIteration);
EXTERN void Fsm_ArdcOptionsSetAbstractPseudoInput(Fsm_ArdcOptions_t *options, Fsm_Ardc_AbstPpiType_t abstractPseudoInput);
EXTERN void Fsm_ArdcOptionsSetDecomposeFlag(Fsm_ArdcOptions_t *options, boolean decomposeFlag);
EXTERN void Fsm_ArdcOptionsSetProjectedInitialFlag(Fsm_ArdcOptions_t *options, boolean projectedInitialFlag);
EXTERN void Fsm_ArdcOptionsSetConstrainReorderFlag(Fsm_ArdcOptions_t *options, int constrainReorderFlag);
EXTERN void Fsm_ArdcOptionsSetImageMethod(Fsm_ArdcOptions_t *options, Img_MethodType ardcImageMethod);
EXTERN void Fsm_ArdcOptionsSetUseHighDensity(Fsm_ArdcOptions_t *options, boolean useHighDensity);
EXTERN void Fsm_ArdcOptionsSetVerbosity(Fsm_ArdcOptions_t *options, int verbosity);
EXTERN double Fsm_ArdcCountOnsetOfOverApproximateReachableStates(Fsm_Fsm_t *fsm);
EXTERN int Fsm_ArdcBddSizeOfOverApproximateReachableStates(Fsm_Fsm_t *fsm);
EXTERN mdd_t * Fsm_ArdcGetMddOfOverApproximateReachableStates(Fsm_Fsm_t *fsm);
EXTERN void Fsm_ArdcPrintReachabilityResults(Fsm_Fsm_t *fsm, long elapseTime);
EXTERN int Fsm_ArdcReadVerbosity(void);
EXTERN void Fsm_Init(void);
EXTERN void Fsm_End(void);
EXTERN Fsm_Fairness_t * Fsm_FsmReadFairnessConstraint(Fsm_Fsm_t *fsm);
EXTERN mdd_t * Fsm_FsmComputeFairStates(Fsm_Fsm_t *fsm, array_t *careSetArray, int verbosity, int dcLevel, Mc_GSHScheduleType schedule, Mc_FwdBwdAnalysis direction, boolean useEarlyTermination);
EXTERN Ctlp_Formula_t * Fsm_FairnessReadFinallyInfFormula(Fsm_Fairness_t *fairness, int i, int j);
EXTERN Ctlp_Formula_t * Fsm_FairnessReadGloballyInfFormula(Fsm_Fairness_t *fairness, int i, int j);
EXTERN mdd_t * Fsm_FairnessObtainFinallyInfMdd(Fsm_Fairness_t *fairness, int i, int j, array_t *careSetArray, Mc_DcLevel dcLevel);
EXTERN mdd_t * Fsm_FairnessObtainGloballyInfMdd(Fsm_Fairness_t *fairness, int i, int j, array_t *careSetArray, Mc_DcLevel dcLevel);
EXTERN boolean Fsm_FairnessTestIsStreett(Fsm_Fairness_t *fairness);
EXTERN boolean Fsm_FairnessTestIsBuchi(Fsm_Fairness_t *fairness);
EXTERN int Fsm_FairnessReadNumDisjuncts(Fsm_Fairness_t *fairness);
EXTERN int Fsm_FairnessReadNumConjunctsOfDisjunct(Fsm_Fairness_t *fairness, int i);
EXTERN array_t * Fsm_FsmReadDebugArray(Fsm_Fsm_t *fsm);
EXTERN Fsm_Fsm_t * Fsm_FsmCreateFromNetworkWithPartition(Ntk_Network_t *network, graph_t *partition);
EXTERN Fsm_Fsm_t * Fsm_FsmCreateReducedFsm(Ntk_Network_t *network, graph_t *partition, array_t *latches, array_t *inputs, array_t *fairArray);
EXTERN Fsm_Fsm_t * Fsm_FsmCreateAbstractFsm(Ntk_Network_t *network, graph_t *partition, array_t *latches, array_t *invisibleLatches, array_t *inputs, array_t *fairArray, boolean independentFlag);
EXTERN void Fsm_FsmFree(Fsm_Fsm_t * fsm);
EXTERN void Fsm_FsmSubsystemFree(Fsm_Fsm_t * fsm);
EXTERN void Fsm_FsmFreeCallback(void * data);
EXTERN Ntk_Network_t * Fsm_FsmReadNetwork(Fsm_Fsm_t * fsm);
EXTERN mdd_manager * Fsm_FsmReadMddManager(Fsm_Fsm_t * fsm);
EXTERN Fsm_Fsm_t * Fsm_NetworkReadOrCreateFsm(Ntk_Network_t * network);
EXTERN Fsm_Fsm_t * Fsm_NetworkReadFsm(Ntk_Network_t * network);
EXTERN Img_ImageInfo_t * Fsm_FsmReadImageInfo(Fsm_Fsm_t *fsm);
EXTERN void Fsm_FsmFreeImageInfo(Fsm_Fsm_t *fsm);
EXTERN graph_t * Fsm_FsmReadPartition(Fsm_Fsm_t *fsm);
EXTERN boolean Fsm_FsmTestIsReachabilityDone(Fsm_Fsm_t *fsm);
EXTERN boolean Fsm_FsmTestIsOverApproximateReachabilityDone(Fsm_Fsm_t *fsm);
EXTERN mdd_t * Fsm_FsmReadReachableStates(Fsm_Fsm_t *fsm);
EXTERN mdd_t * Fsm_FsmReadCurrentReachableStates(Fsm_Fsm_t *fsm);
EXTERN array_t * Fsm_FsmReadOverApproximateReachableStates(Fsm_Fsm_t *fsm);
EXTERN array_t * Fsm_FsmReadCurrentOverApproximateReachableStates(Fsm_Fsm_t *fsm);
EXTERN array_t * Fsm_FsmReadReachabilityOnionRings(Fsm_Fsm_t *fsm);
EXTERN boolean Fsm_FsmReachabilityOnionRingsStates(Fsm_Fsm_t *fsm, mdd_t ** result);
EXTERN boolean Fsm_FsmTestReachabilityOnionRingsUpToDate(Fsm_Fsm_t *fsm);
EXTERN Fsm_RchType_t Fsm_FsmReadReachabilityOnionRingsMode(Fsm_Fsm_t *fsm);
EXTERN Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfo(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag);
EXTERN Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfoFAFW(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag);
EXTERN Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfoForComputingRange(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag);
EXTERN mdd_t * Fsm_FsmComputeInitialStates(Fsm_Fsm_t *fsm);
EXTERN array_t * Fsm_FsmReadPresentStateVars(Fsm_Fsm_t *fsm);
EXTERN array_t * Fsm_FsmReadNextStateVars(Fsm_Fsm_t *fsm);
EXTERN array_t * Fsm_FsmReadNextStateFunctionNames(Fsm_Fsm_t *fsm);
EXTERN array_t * Fsm_FsmReadInputVars(Fsm_Fsm_t *fsm);
EXTERN array_t * Fsm_FsmReadPrimaryInputVars(Fsm_Fsm_t *fsm);
EXTERN array_t * Fsm_FsmReadPseudoInputVars(Fsm_Fsm_t *fsm);
EXTERN mdd_t * Fsm_FsmReadFairnessStates(Fsm_Fsm_t *fsm);
EXTERN void Fsm_FsmSetInputVars(Fsm_Fsm_t *fsm, array_t *inputVars);
EXTERN void Fsm_FsmSetInitialStates(Fsm_Fsm_t *fsm, mdd_t *initStates);
EXTERN Fsm_Fsm_t * Fsm_HrcManagerReadCurrentFsm(Hrc_Manager_t *hmgr);
EXTERN Fsm_Fsm_t * Fsm_FsmCreateSubsystemFromNetwork(Ntk_Network_t *network, graph_t *partition, st_table *vertexTable, boolean independentFlag, int createPseudoVarMode);
EXTERN void Fsm_InstantiateHint(Fsm_Fsm_t *fsm, mdd_t *hint, int fwdFlag, int bwdFlag, Ctlp_Approx_t type, int printStatus);
EXTERN void Fsm_CleanUpHints(Fsm_Fsm_t *fsm, int fwdFlag, int bwdFlag, int printStatus);
EXTERN void Fsm_FsmFreeReachableStates(Fsm_Fsm_t *fsm);
EXTERN void Fsm_FsmFreeOverApproximateReachableStates(Fsm_Fsm_t *fsm);
EXTERN int Fsm_FsmGetReachableDepth(Fsm_Fsm_t *fsm);
EXTERN boolean Fsm_FsmCheckSameSubFsmInTotalFsm(Fsm_Fsm_t *fsm, Fsm_Fsm_t *subFsm1, Fsm_Fsm_t *subFsm2);
EXTERN Fsm_RchStatus_t Fsm_FsmReadReachabilityApproxComputationStatus(Fsm_Fsm_t *fsm);
EXTERN void Fsm_MinimizeTransitionRelationWithReachabilityInfo(Fsm_Fsm_t *fsm, Img_DirectionType fwdbwd, boolean verbosity);
EXTERN FsmHdTravOptions_t * Fsm_FsmHdGetTravOptions(int nvars);
EXTERN void Fsm_FsmHdFreeTravOptions(FsmHdTravOptions_t *options);
EXTERN int Fsm_FsmHdOptionReadNumVars(FsmHdTravOptions_t *options);
EXTERN int Fsm_FsmHdOptionReadFrontierApproxThreshold(FsmHdTravOptions_t *options);
EXTERN boolean Fsm_FsmHdOptionReadOnlyPartialImage(FsmHdTravOptions_t *options);
EXTERN boolean Fsm_FsmHdOptionReadScrapStates(FsmHdTravOptions_t *options);
EXTERN double Fsm_FsmHdOptionReadQuality(FsmHdTravOptions_t *options);
EXTERN bdd_approx_type_t Fsm_FsmHdOptionReadFrontierApproxMethod(FsmHdTravOptions_t *options);
EXTERN Fsm_HdDeadEndType_t Fsm_FsmHdOptionReadDeadEnd(FsmHdTravOptions_t *options);
EXTERN boolean Fsm_FsmHdOptionReadNewOnly(FsmHdTravOptions_t *options);
EXTERN bdd_approx_type_t Fsm_FsmHdOptionReadDeadEndSubsetMethod(FsmHdTravOptions_t *options);
EXTERN int Fsm_FsmHdOptionSetFrontierApproxThreshold(FsmHdTravOptions_t *options, int threshold);
EXTERN void Fsm_FsmHdOptionSetOnlyPartialImage(FsmHdTravOptions_t *options, boolean onlyPartial);
EXTERN void Fsm_FsmHdOptionSetScrapStates(FsmHdTravOptions_t *options, boolean scrapStates);
EXTERN void Fsm_FsmHdOptionSetQuality(FsmHdTravOptions_t *options, double quality);
EXTERN void Fsm_FsmHdOptionSetFrontierApproxMethod(FsmHdTravOptions_t *options, bdd_approx_type_t approxMethod);
EXTERN void Fsm_FsmHdOptionSetDeadEnd(FsmHdTravOptions_t *options, Fsm_HdDeadEndType_t deadEnd);
EXTERN void Fsm_FsmHdOptionSetNewOnly(FsmHdTravOptions_t *options, boolean newOnly);
EXTERN void Fsm_FsmHdOptionSetDeadEndSubsetMethod(FsmHdTravOptions_t *options, bdd_approx_type_t approxMethod);
EXTERN mdd_t * Fsm_FsmComputeReachableStates(Fsm_Fsm_t *fsm, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, int ardc, int recompute, array_t *invarStates, boolean printWarning, array_t *guideArray);
EXTERN mdd_t * Fsm_MddMultiwayAndSmooth(mdd_manager *mddManager, array_t *mddArray, array_t *smoothingVars);
EXTERN void Fsm_FsmReachabilityPrintResults(Fsm_Fsm_t *fsm, long elapseTime, int approxFlag);
EXTERN void Fsm_FsmFairnessUpdate(Fsm_Fsm_t *fsm, array_t *formulaArray);
EXTERN mdd_t *Fsm_FsmReadUniQuantifyInputCube(Fsm_Fsm_t *fsm);
EXTERN mdd_t *Fsm_FsmReadExtQuantifyInputCube(Fsm_Fsm_t *fsm);
EXTERN Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfoPrunedFAFW(Fsm_Fsm_t *fsm, mdd_t *Winning, int bwdImgFlag, int fwdImgFlag);
EXTERN boolean Fsm_FsmReadUseUnquantifiedFlag( Fsm_Fsm_t * fsm);
EXTERN void Fsm_FsmSetImageInfo( Fsm_Fsm_t *fsm, Img_ImageInfo_t *imageInfo);
EXTERN void Fsm_FsmSetUseUnquantifiedFlag(Fsm_Fsm_t *fsm, boolean value);
EXTERN int Fsm_FsmReadFAFWFlag(Fsm_Fsm_t *fsm);
EXTERN void Fsm_FsmSetFAFWFlag(Fsm_Fsm_t *fsm, boolean FAFWFlag);
EXTERN void Fsm_FsmSetSystemVariableFAFW(Fsm_Fsm_t *fsm, st_table *bddIdTable);
EXTERN void Fsm_ImageInfoConjoinWithWinningStrategy( Fsm_Fsm_t *modelFsm, Img_DirectionType directionType, mdd_t *winningStrategy);
EXTERN void Fsm_ImageInfoRecoverFromWinningStrategy( Fsm_Fsm_t *modelFsm, Img_DirectionType directionType);
int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray);

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

#endif /* _FSM */