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

  FileName    [mark.h]

  PackageName [mark]

  Synopsis    [Data structures used in Markovian analysis.]

  Description [Data structures used in Markovian analysis.]

  SeeAlso     [markInt.h]

  Author      [Balakrishna Kumthekar]

  Copyright   [This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/
#ifndef _MARK
#define _MARK

#include "fsm.h"
#include "util.h"
#include "st.h"
#include "bdd.h"

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


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


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

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

  Synopsis    [Different methods of solving for steady state probabilities.
  For more details consult 
  
  G. D. Hachtel, E. Macii, A. Pardo and F. Somenzi, "Markovian Analysis
  of Large Finite State Machines", IEEE Trans. on CAD, December 1996.  ]

  SeeAlso     [Mark_StartMethod]

******************************************************************************/
typedef enum {
  Solve_Default_c,  /* Default method. It is Solve_FPMethod_c. */
  Solve_GenMethod_c,
  Solve_FPMethod_c, /* This is the only one that is currently supported */
  Solve_CKMethod_c
} Mark_SolveMethod;


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

  Synopsis    [Different methods of chosing the reset state. For more details
  consult 

  G. D. Hachtel, E. Macii, A. Pardo and F. Somenzi, "Markovian Analysis
  of Large Finite State Machines", IEEE Trans. on CAD, December 1996.]

  SeeAlso     [Markov_SolveMethod]

******************************************************************************/
typedef enum {
  Start_Default_c,  /* Default method. It is Start_Reset_c. */
  Start_Reset_c,
  Start_EquiProb_c
} Mark_StartMethod;

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


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

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

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

EXTERN bdd_node ** Mark_FsmComputeStateProbs(Fsm_Fsm_t *fsm, Mark_SolveMethod solveMethod, Mark_StartMethod startMethod, st_table *inputProb, int roundOff);
EXTERN bdd_node ** Mark_ComputeStateProbsWithTr(bdd_manager *ddManager, bdd_node *TR, bdd_node *reachable, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, bdd_node **zVars, st_table *inputProb, int nVars, int nPi, int roundOff, Mark_SolveMethod method, Mark_StartMethod start);
EXTERN bdd_node * Mark_addInProb(bdd_manager *manager, bdd_node *tr, bdd_node *cube, st_table *probTable);
EXTERN void Mark_Init(void);
EXTERN void Mark_End(void);

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

#endif /* _MARK */