source: vis_dev/vis-2.3/src/mark/markFPSolve.c @ 23

Last change on this file since 23 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 8.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [markFPSolve.c]
4
5  PackageName [mark]
6
7  Synopsis    [This file contains functions that implement the fixed point
8  method. For more details please refer
9 
10  G. D. Hachtel, E. Macii, A. Pardo and F. Somenzi, "Markovian Analysis
11  of Large Finite State Machines", IEEE Trans. on CAD, December 1996.  ]
12
13  Description [This file contains functions that implement the fixed point
14  method. For more details please refer
15 
16  G. D. Hachtel, E. Macii, A. Pardo and F. Somenzi, "Markovian Analysis
17  of Large Finite State Machines", IEEE Trans. on CAD, December 1996.  ]
18
19  Author      [Balakrishna Kumthekar]
20
21  Copyright   [This file was created at the University of Colorado at
22  Boulder.  The University of Colorado at Boulder makes no warranty
23  about the suitability of this software for any purpose.  It is
24  presented on an AS IS basis.]
25
26******************************************************************************/
27
28#include "markInt.h"
29
30/*---------------------------------------------------------------------------*/
31/* Constant declarations                                                     */
32/*---------------------------------------------------------------------------*/
33
34
35/*---------------------------------------------------------------------------*/
36/* Stucture declarations                                                     */
37/*---------------------------------------------------------------------------*/
38
39
40/*---------------------------------------------------------------------------*/
41/* Type declarations                                                         */
42/*---------------------------------------------------------------------------*/
43
44
45/*---------------------------------------------------------------------------*/
46/* Variable declarations                                                     */
47/*---------------------------------------------------------------------------*/
48
49
50/*---------------------------------------------------------------------------*/
51/* Macro declarations                                                        */
52/*---------------------------------------------------------------------------*/
53
54
55/**AutomaticStart*************************************************************/
56
57/*---------------------------------------------------------------------------*/
58/* Static function prototypes                                                */
59/*---------------------------------------------------------------------------*/
60
61
62/**AutomaticEnd***************************************************************/
63
64
65/*---------------------------------------------------------------------------*/
66/* Definition of exported functions                                          */
67/*---------------------------------------------------------------------------*/
68
69
70/*---------------------------------------------------------------------------*/
71/* Definition of internal functions                                          */
72/*---------------------------------------------------------------------------*/
73
74/**Function********************************************************************
75
76  Synopsis [Computes steady state probabilities vis fixed point method.]
77
78  Description [Computes steady state probabilities via fixed point method.
79  The function returns an array of two ADDs. The ADD with index 0, represents
80  the steady state probabilities and the second one the one-step transition
81  probability matrix.]
82
83  SideEffects [None]
84
85  SeeAlso []
86
87******************************************************************************/
88bdd_node ** 
89MarkAddFPSolve(
90  CK *ck)
91{
92    bdd_manager *manager;
93    bdd_node **xAddVars, **yAddVars;
94    bdd_node *Scaling;
95    bdd_node *InitG, *G, *NewG;
96    bdd_node *p, *q, *newTr;
97    bdd_node *xCube, *ddTemp, *guess; 
98    bdd_node *zero;
99    bdd_node **result;
100    bdd_node *probMatrix;
101    int nVars, iter = 0;
102    int converged;
103    double max;
104
105    manager = ck->manager;
106    nVars = ck->nVars;
107    xAddVars = ck->xAddVars;
108    yAddVars = ck->yAddVars;
109
110    result = ALLOC(bdd_node *, 2);
111    if (result == NULL)
112        return NULL;
113    zero = bdd_read_zero(manager);
114
115    /* Build an ADD for one step transition probability matrix */
116    bdd_ref(probMatrix = MarkAddBuildCoeff(manager,ck->coeff, ck->piAddVars,
117                                            ck->inputProb, ck->scale, nVars,
118                                            ck->nPi));
119    result[1] = probMatrix;
120
121    /* create initial guess and print it;
122     * equiprobability to all the states and probability 1 to one of the
123     * reset states are currently supported
124     */
125    switch(ck->start) {
126    case Start_EquiProb_c:
127        (void)printf("Initial guess: equiprob\n");
128        bdd_ref(ck->init_guess = ck->term_scc);
129        p = bdd_add_const(manager,
130                          (double) (1/(double)(ck->term_SCC_states)));
131        bdd_ref(p);
132        bdd_ref(q = bdd_add_ite(manager,ck->init_guess,p,zero)); 
133        bdd_recursive_deref(manager,p);
134        InitG = bdd_add_swap_variables(manager,q,xAddVars,yAddVars,nVars);
135        bdd_ref(InitG);
136        bdd_recursive_deref(manager,q);
137        bdd_recursive_deref(manager,ck->init_guess);
138        break;
139    case Start_Reset_c:
140    default:
141        /* Pick one of the states in the TSCC as the initial guess */
142        bdd_ref(ddTemp = bdd_add_bdd_threshold(manager,ck->term_scc,1));
143        bdd_ref(guess = bdd_bdd_pick_one_minterm(manager, ddTemp,
144                                             ck->xVars, nVars));
145        bdd_recursive_deref(manager,ddTemp);
146        bdd_ref(ck->init_guess = bdd_bdd_to_add(manager,guess));
147        bdd_recursive_deref(manager,guess);
148        bdd_ref(InitG = bdd_add_swap_variables(manager,ck->init_guess,
149                                               xAddVars, yAddVars,nVars));
150        bdd_recursive_deref(manager,ck->init_guess);
151        break;
152    }
153
154    /* put prob. transition matrix in appropriate form (transpose)*/
155    newTr = bdd_add_swap_variables(manager,probMatrix,xAddVars,yAddVars,nVars);
156    bdd_ref(newTr);
157
158    /* calculate the x-cube for abstraction */
159    bdd_ref(xCube = bdd_add_compute_cube(manager,xAddVars,NULL,nVars));
160 
161    do {
162        iter++;
163        G = bdd_add_matrix_multiply(manager,newTr,InitG,yAddVars,nVars);
164        bdd_ref(G);
165        bdd_ref(Scaling = bdd_add_exist_abstract(manager,G,xCube));
166
167        bdd_ref(NewG = bdd_add_apply(manager,bdd_add_divide,G,Scaling));
168        bdd_recursive_deref(manager,G);
169        G = NewG; 
170        bdd_recursive_deref(manager,Scaling);
171        q = bdd_add_swap_variables(manager,G,xAddVars,yAddVars,nVars);
172        bdd_ref(q);
173        max = bdd_add_value(bdd_add_find_max(manager,InitG));
174        converged = bdd_equal_sup_norm(manager,q,InitG,ck->reltol*max,0);
175        bdd_recursive_deref( manager,InitG);
176        if (converged) {
177            (void) fprintf(vis_stdout,"Iteration = %d\n",iter);
178            bdd_recursive_deref( manager,newTr);
179            bdd_recursive_deref( manager,q);
180            bdd_recursive_deref(manager,xCube);
181            result[0] = G;
182            return result;
183        }
184        bdd_recursive_deref( manager,G);
185        InitG = q;
186    } while (1);
187
188} /* end of addFPSolve */
189
190
191/**Function********************************************************************
192
193  Synopsis    [Builds the one-step transition probability matrix given primary
194  input probabilities and 0-1 ADD transition relation.]
195
196  Description [Builds the one-step transition probability matrix given primary
197  input probabilities and 0-1 ADD transition relation.]
198
199  SideEffects [None]
200
201  SeeAlso     []
202
203******************************************************************************/
204bdd_node *
205MarkAddBuildCoeff(
206  bdd_manager *manager,
207  bdd_node *func,
208  bdd_node **piAddVars,
209  st_table *inputProb,
210  double scale,
211  int nVars,
212  int nPi)
213{
214    /* Given func, the coefficient matrix is built */
215    /* this function is used first to build the collapsed coeff matrix */
216    /* and then the matrix for every TSCC */
217
218    bdd_node *Correction;
219    bdd_node *q;
220    bdd_node *matrix;
221    bdd_node *piAddCube;
222
223    bdd_ref(piAddCube = bdd_add_compute_cube(manager,piAddVars,NULL,nPi));
224
225    /* Create the transition matrix either with equiprobable
226       or specific input probs. */
227
228    if (inputProb != NULL) {
229      bdd_ref(matrix = Mark_addInProb(manager,func,piAddCube,inputProb));
230    }
231    else {
232      /* create correction ADD and print it */
233      bdd_ref(Correction = bdd_add_const(manager,
234                                          (scale/(double)(1 << nPi))));
235     
236      bdd_ref(q = bdd_add_exist_abstract(manager,func,piAddCube));
237     
238      /* apply correction to the transition relation matrix and print it */
239      bdd_ref(matrix = bdd_add_apply(manager, bdd_add_times,q, Correction));
240      bdd_recursive_deref( manager,Correction);
241      bdd_recursive_deref(manager,q);
242    }
243    bdd_recursive_deref(manager,piAddCube);
244    bdd_deref(matrix);
245    return(matrix);
246}
247
248
Note: See TracBrowser for help on using the repository browser.