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

  FileName    [markInt.h]

  PackageName [mark]

  Synopsis    [Data structures used in Markovian analysis.]

  Description [optional]

  SeeAlso     [optional]

  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 _MARKINT
#define _MARKINT

#include "mark.h"
#include <string.h>

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


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


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

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

  Synopsis    [Data structure for performing Markovian Analysis.]

  SeeAlso     []

******************************************************************************/
typedef struct CK {
  bdd_manager *manager;
  bdd_node **piVars;      /* Primary input variables. BDD variables */
  bdd_node **xVars;       /* Present state variables. BDD variables. */
  bdd_node **yVars;       /* Next state variables. BDD variables. */
  bdd_node **zVars;       /* Auxillary BDD variables, used internally */
  bdd_node **piAddVars;   /* Primary input variables, ADD variables */
  bdd_node **xAddVars;    /* Present state variables. ADD variables. */
  bdd_node **yAddVars;    /* Next state variables. ADD variables. */
  bdd_node **zAddVars;    /* Auxillary ADD variables, used internally */
  bdd_node *coeff;        /* 0-1 ADD of TR(x,w,y) */
  int nVars;            /* Number of state variables */
  int nPi;              /* Number of input variables */
  double abstol;        /* Tolerance values, used internally */
  double scale;
  double reltol;
  Mark_StartMethod start;
  int roundOff;         /* Roundoff to "roundOff" digit after decimal */
  st_table *inputProb;  /* input probabilities */
  bdd_node *transition;   /* BDD transition relation T(x,w,y) */
  bdd_node *reached;      /* Set of reachable states R(x) */
  st_table *indexSCC;
  bdd_node *collapsedcoeff;
  double term_SCC_states;  /* # of terminal SCCs */
  st_table *periods;    /* period of TSCCs */
  bdd_node *term_scc;    /* ADD of reachable terminal SCCs */
  bdd_node *init_guess;  /* equi. probability to all TSCC states
			 or probabiliy 1 to one of the TSCC states.*/
} CK;

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


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

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

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

EXTERN bdd_node ** MarkAddCKSolve(CK *ck);
EXTERN bdd_node ** MarkAddGenSolve(CK *ck);
EXTERN double MarkAverageBitChange(bdd_manager *manager, bdd_node *probTR, bdd_node **xVars, bdd_node **yVars, int nVars);
EXTERN bdd_node ** MarkAddFPSolve(CK *ck);
EXTERN bdd_node * MarkAddBuildCoeff(bdd_manager *manager, bdd_node *func, bdd_node **piAddVars, st_table *inputProb, double scale, int nVars, int nPi);
EXTERN bdd_node * MarkGetSCC(bdd_manager *manager, bdd_node *tr, bdd_node *tc, bdd_node *reached, bdd_node **xVars, bdd_node **yVars, int nVars, st_table **scc_table);
EXTERN bdd_node * MarkAddInProbRecur(bdd_manager *manager, bdd_node *tr, bdd_node *cube, st_table *probTable, st_table *visited);

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

#endif /* _MARKINT */