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

  FileName    [markInProb.c]

  PackageName [mark]

  Synopsis    [Computation of transition probability matrix and convergence
  checks in markov analysis.]

  Description [[Computation of transition probability matrix and convergence
  checks in markov analysis.]

  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.]

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

#include "markInt.h"

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


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


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


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


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


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

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


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


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

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

  Synopsis    [Computes one-step transition probability matrix given the 0-1
  ADD of transition relation and a table of primary input probabiliites.]

  Description [Computes one-step transition probability matrix given the 0-1
  ADD of transition relation and a table of primary input probabiliites. tr is
  the 0-1 ADD, cube is a cube of primary inputs and probTable is a hash table
  that stores (<mdd_id>,<probability of x = 1>). The function returns the ADD
  for one-step transition probability matrix.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
bdd_node *
Mark_addInProb(
  bdd_manager *manager,
  bdd_node *tr,
  bdd_node *cube,
  st_table *probTable)
{
    st_table *visited;
    st_generator *gen;
    bdd_node *result, *r, *k;

    do {
	bdd_set_reordered_field(manager, 0);
	visited = st_init_table(st_ptrcmp,st_ptrhash);
	bdd_ref(result = bdd_read_one(manager));
	st_insert(visited,(char *)result,(char *)result);
	bdd_ref(result = bdd_read_zero(manager));
	st_insert(visited,(char *)result,(char *)result);
	result = MarkAddInProbRecur(manager,tr,cube,probTable,visited);
	if (result)
	  bdd_ref(result);
	st_foreach_item(visited,gen,&k,&r) {
	    bdd_recursive_deref(manager,r);
	}
	st_free_table(visited);
    } while (bdd_read_reordered_field(manager) == 1);
    
    bdd_deref(result);
    return(result);

} /* end of Mark_addInProb */


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

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

  Synopsis    [Implements the recursive step of Mark_addInProb.]

  Description [Implements the recursive step of Mark_addInProb.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
bdd_node *
MarkAddInProbRecur(
  bdd_manager *manager,
  bdd_node *tr,
  bdd_node *cube,
  st_table *probTable,
  st_table *visited)
{
    int topTR,topC;
    int index;
    double *prob;
    bdd_node *solT,*solE;
    bdd_node *solPT,*solPE;
    bdd_node *result;
    bdd_node *unique;

    /* lookup in the cache */
    if(st_lookup(visited,tr,&result)) 
	return(result);

    /* the cube is one then return */
    if ( cube == bdd_read_one(manager)) 
	return tr;

    /* Obtain the top variable indexes */
    topTR = bdd_get_level_from_id(manager,bdd_node_read_index(tr));
    topC = bdd_get_level_from_id(manager,bdd_node_read_index(cube));

    /* The function does not depend on the top variable of the cube */
    if (topTR > topC ) {
	result = MarkAddInProbRecur(manager,tr,bdd_bdd_T(cube),probTable,visited);
	return(result);
    }

    /* If both top variables are equal, solve subproblems and combine */
    if (topTR == topC ) {
	solT = MarkAddInProbRecur(manager,bdd_bdd_T(tr),bdd_bdd_T(cube),
				  probTable,visited);
	if (solT == NULL) {
	    return NULL;
	}
	bdd_ref(solT);
        solE = MarkAddInProbRecur(manager,bdd_bdd_E(tr),bdd_bdd_T(cube),
				  probTable,visited);
	if (solE == NULL) {
	    bdd_recursive_deref(manager,solT);
	    return NULL;
	}
	bdd_ref(solE);
	index = bdd_node_read_index(cube);
        st_lookup(probTable,(char *)(long)index,&prob);
        unique = bdd_add_const(manager,*prob);
	if(unique == NULL) {
	    bdd_recursive_deref(manager,solT);
	    bdd_recursive_deref(manager,solE);
	    return NULL;
	}
	bdd_ref(unique);
        solPT = bdd_add_apply_recur(manager,bdd_add_times,solT,unique);
	if (solPT == NULL) {
	    bdd_recursive_deref(manager,solT);
	    bdd_recursive_deref(manager,solE);
	    bdd_recursive_deref(manager,unique);
	    return NULL;
	}
	bdd_ref(solPT);
        bdd_recursive_deref(manager,unique);
        bdd_recursive_deref(manager,solT);
        unique = bdd_add_const(manager,1.0 - *prob);
	if (unique == NULL) {
	    bdd_recursive_deref(manager,solE);
	    bdd_recursive_deref(manager,solPT);
	    return NULL;
	}
	bdd_ref(unique);
        solPE = bdd_add_apply_recur(manager,bdd_add_times,solE,unique);
	if (solPE == NULL) {
	    bdd_recursive_deref(manager,unique);
	    bdd_recursive_deref(manager,solPT);
	    bdd_recursive_deref(manager,solE);
	    return NULL;
	}
	bdd_ref(solPE);
        bdd_recursive_deref(manager,unique);
        bdd_recursive_deref(manager,solE);
        result = bdd_add_apply_recur(manager,bdd_add_plus,solPT,solPE);
	if (result == NULL) {
	    bdd_recursive_deref(manager,solPT);
	    bdd_recursive_deref(manager,solPE);
	    return NULL;
	}
	bdd_ref(result);
        bdd_recursive_deref(manager,solPE);
        bdd_recursive_deref(manager,solPT);
        st_insert(visited,(char *)tr,(char *)result);
	/* bdd_deref(result); */
        return(result);
    }
    
    /* Split on a state variable, solve subproblems and combine by ite */
    solT = MarkAddInProbRecur(manager,bdd_bdd_T(tr),cube, probTable,visited);
    if (solT == NULL) {
	return NULL;
    }
    bdd_ref(solT);
    solE = MarkAddInProbRecur(manager,bdd_bdd_E(tr),cube,
			      probTable,visited);
    if (solE == NULL) {
	bdd_recursive_deref(manager,solT);
	return NULL;
    }
    bdd_ref(solE);
    result = bdd_unique_inter(manager,bdd_node_read_index(tr),
			      solT,solE);
    if (result == NULL) {
	bdd_recursive_deref(manager,solT);
	bdd_recursive_deref(manager,solE);
	return NULL;
    }
    bdd_ref(result);
    bdd_recursive_deref(manager,solT);
    bdd_recursive_deref(manager,solE);
    st_insert(visited,(char *)tr,(char *)result);
    /* bdd_deref(result); */
    return(result);

} /* end of MarkAddInProbRecur */


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