VIS

src/mark/markInProb.c File Reference

#include "markInt.h"
Include dependency graph for markInProb.c:

Go to the source code of this file.

Functions

bdd_node * Mark_addInProb (bdd_manager *manager, bdd_node *tr, bdd_node *cube, st_table *probTable)
bdd_node * MarkAddInProbRecur (bdd_manager *manager, bdd_node *tr, bdd_node *cube, st_table *probTable, st_table *visited)

Function Documentation

bdd_node* Mark_addInProb ( bdd_manager *  manager,
bdd_node *  tr,
bdd_node *  cube,
st_table *  probTable 
)

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.]AutomaticStart AutomaticEnd 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 []

Definition at line 80 of file markInProb.c.

{
    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 */

Here is the call graph for this function:

Here is the caller graph for this function:

bdd_node* MarkAddInProbRecur ( bdd_manager *  manager,
bdd_node *  tr,
bdd_node *  cube,
st_table *  probTable,
st_table *  visited 
)

Function********************************************************************

Synopsis [Implements the recursive step of Mark_addInProb.]

Description [Implements the recursive step of Mark_addInProb.]

SideEffects [None]

SeeAlso []

Definition at line 128 of file markInProb.c.

{
    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 */

Here is the caller graph for this function: