/**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.] ******************************************************************************/ #include "markInt.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Stucture declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ bdd_node ** MarkAddFPSolve( CK *ck) { 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 */ /**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 [] ******************************************************************************/ bdd_node * MarkAddBuildCoeff( bdd_manager *manager, bdd_node *func, bdd_node **piAddVars, st_table *inputProb, double scale, int nVars, int nPi) { /* 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); }