#include "markInt.h"

Include dependency graph for markFPSolve.c:

Functions
bdd_node **	MarkAddFPSolve (CK *ck)
bdd_node *	MarkAddBuildCoeff (bdd_manager manager, bdd_node func, bdd_node *piAddVars, st_table inputProb, double scale, int nVars, int nPi)

Function Documentation

bdd_node* MarkAddBuildCoeff	(	bdd_manager *	manager,
		bdd_node *	func,
		bdd_node **	piAddVars,
		st_table *	inputProb,
		double	scale,
		int	nVars,
		int	nPi
	)

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

Synopsis [Builds the one-step transition probability matrix given primary input probabilities and 0-1 ADD transition relation.]

Description [Builds the one-step transition probability matrix given primary input probabilities and 0-1 ADD transition relation.]

SideEffects [None]

SeeAlso []

Definition at line 205 of file markFPSolve.c.

{
    /* Given func, the coefficient matrix is built */
    /* this function is used first to build the collapsed coeff matrix */
    /* and then the matrix for every TSCC */

    bdd_node *Correction;
    bdd_node *q;
    bdd_node *matrix;
    bdd_node *piAddCube;

    bdd_ref(piAddCube = bdd_add_compute_cube(manager,piAddVars,NULL,nPi));

    /* Create the transition matrix either with equiprobable
       or specific input probs. */

    if (inputProb != NULL) {
      bdd_ref(matrix = Mark_addInProb(manager,func,piAddCube,inputProb));
    }
    else {
      /* create correction ADD and print it */
      bdd_ref(Correction = bdd_add_const(manager,
                                          (scale/(double)(1 << nPi))));
      
      bdd_ref(q = bdd_add_exist_abstract(manager,func,piAddCube));
      
      /* apply correction to the transition relation matrix and print it */
      bdd_ref(matrix = bdd_add_apply(manager, bdd_add_times,q, Correction));
      bdd_recursive_deref( manager,Correction);
      bdd_recursive_deref(manager,q);
    }
    bdd_recursive_deref(manager,piAddCube);
    bdd_deref(matrix);
    return(matrix);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bdd_node** MarkAddFPSolve ( CK * ck )

CFile***********************************************************************

FileName [markFPSolve.c]

PackageName [mark]

Synopsis [This file contains functions that implement the fixed point method. For more details please refer

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

Description [This file contains functions that implement the fixed point method. For more details please refer

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

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 steady state probabilities vis fixed point method.]

Description [Computes steady state probabilities via fixed point method. The function returns an array of two ADDs. The ADD with index 0, represents the steady state probabilities and the second one the one-step transition probability matrix.]

SideEffects [None]

SeeAlso []

Definition at line 89 of file markFPSolve.c.

{
    bdd_manager *manager;
    bdd_node **xAddVars, **yAddVars;
    bdd_node *Scaling;
    bdd_node *InitG, *G, *NewG;
    bdd_node *p, *q, *newTr;
    bdd_node *xCube, *ddTemp, *guess; 
    bdd_node *zero;
    bdd_node **result;
    bdd_node *probMatrix;
    int nVars, iter = 0;
    int converged;
    double max;

    manager = ck->manager;
    nVars = ck->nVars;
    xAddVars = ck->xAddVars;
    yAddVars = ck->yAddVars;

    result = ALLOC(bdd_node *, 2);
    if (result == NULL)
        return NULL;
    zero = bdd_read_zero(manager);

    /* Build an ADD for one step transition probability matrix */
    bdd_ref(probMatrix = MarkAddBuildCoeff(manager,ck->coeff, ck->piAddVars,
                                            ck->inputProb, ck->scale, nVars,
                                            ck->nPi));
    result[1] = probMatrix;

    /* create initial guess and print it;
     * equiprobability to all the states and probability 1 to one of the
     * reset states are currently supported
     */
    switch(ck->start) {
    case Start_EquiProb_c:
        (void)printf("Initial guess: equiprob\n");
        bdd_ref(ck->init_guess = ck->term_scc);
        p = bdd_add_const(manager,
                          (double) (1/(double)(ck->term_SCC_states)));
        bdd_ref(p);
        bdd_ref(q = bdd_add_ite(manager,ck->init_guess,p,zero)); 
        bdd_recursive_deref(manager,p);
        InitG = bdd_add_swap_variables(manager,q,xAddVars,yAddVars,nVars);
        bdd_ref(InitG);
        bdd_recursive_deref(manager,q);
        bdd_recursive_deref(manager,ck->init_guess);
        break;
    case Start_Reset_c:
    default:
        /* Pick one of the states in the TSCC as the initial guess */
        bdd_ref(ddTemp = bdd_add_bdd_threshold(manager,ck->term_scc,1));
        bdd_ref(guess = bdd_bdd_pick_one_minterm(manager, ddTemp,
                                             ck->xVars, nVars));
        bdd_recursive_deref(manager,ddTemp);
        bdd_ref(ck->init_guess = bdd_bdd_to_add(manager,guess));
        bdd_recursive_deref(manager,guess);
        bdd_ref(InitG = bdd_add_swap_variables(manager,ck->init_guess,
                                               xAddVars, yAddVars,nVars));
        bdd_recursive_deref(manager,ck->init_guess);
        break;
    }

    /* put prob. transition matrix in appropriate form (transpose)*/
    newTr = bdd_add_swap_variables(manager,probMatrix,xAddVars,yAddVars,nVars);
    bdd_ref(newTr);

    /* calculate the x-cube for abstraction */
    bdd_ref(xCube = bdd_add_compute_cube(manager,xAddVars,NULL,nVars));
 
    do {
        iter++;
        G = bdd_add_matrix_multiply(manager,newTr,InitG,yAddVars,nVars);
        bdd_ref(G);
        bdd_ref(Scaling = bdd_add_exist_abstract(manager,G,xCube));

        bdd_ref(NewG = bdd_add_apply(manager,bdd_add_divide,G,Scaling));
        bdd_recursive_deref(manager,G);
        G = NewG; 
        bdd_recursive_deref(manager,Scaling);
        q = bdd_add_swap_variables(manager,G,xAddVars,yAddVars,nVars);
        bdd_ref(q);
        max = bdd_add_value(bdd_add_find_max(manager,InitG));
        converged = bdd_equal_sup_norm(manager,q,InitG,ck->reltol*max,0);
        bdd_recursive_deref( manager,InitG);
        if (converged) {
            (void) fprintf(vis_stdout,"Iteration = %d\n",iter);
            bdd_recursive_deref( manager,newTr);
            bdd_recursive_deref( manager,q);
            bdd_recursive_deref(manager,xCube);
            result[0] = G;
            return result;
        }
        bdd_recursive_deref( manager,G);
        InitG = q;
    } while (1);

} /* end of addFPSolve */

Here is the call graph for this function:

Here is the caller graph for this function:

src/mark/markFPSolve.c File Reference

Functions

Function Documentation