source: vis_dev/vis-2.3/src/mark/markGetScc.c @ 17

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

vis2.3
File size: 8.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [markGetScc.c]
4
5  PackageName [mark]
6
7  Synopsis    [Functions to compute terminal strongly connected components
8  in a markov chain.]
9
10  Description [Functions to compute terminal strongly connected components
11  in a markov chain.]
12
13  Author      [Balakrishna Kumthekar]
14
15  Copyright   [This file was created at the University of Colorado at
16  Boulder.  The University of Colorado at Boulder makes no warranty
17  about the suitability of this software for any purpose.  It is
18  presented on an AS IS basis.]
19
20******************************************************************************/
21
22#include "markInt.h"
23
24/*---------------------------------------------------------------------------*/
25/* Constant declarations                                                     */
26/*---------------------------------------------------------------------------*/
27
28
29/*---------------------------------------------------------------------------*/
30/* Stucture declarations                                                     */
31/*---------------------------------------------------------------------------*/
32
33
34/*---------------------------------------------------------------------------*/
35/* Type declarations                                                         */
36/*---------------------------------------------------------------------------*/
37
38
39/*---------------------------------------------------------------------------*/
40/* Variable declarations                                                     */
41/*---------------------------------------------------------------------------*/
42
43
44/*---------------------------------------------------------------------------*/
45/* Macro declarations                                                        */
46/*---------------------------------------------------------------------------*/
47
48
49/**AutomaticStart*************************************************************/
50
51/*---------------------------------------------------------------------------*/
52/* Static function prototypes                                                */
53/*---------------------------------------------------------------------------*/
54
55static bdd_node * pickOneCube(bdd_manager *manager, bdd_node *node, bdd_node **xVars, int nVars);
56
57/**AutomaticEnd***************************************************************/
58
59
60/*---------------------------------------------------------------------------*/
61/* Definition of exported functions                                          */
62/*---------------------------------------------------------------------------*/
63
64
65/*---------------------------------------------------------------------------*/
66/* Definition of internal functions                                          */
67/*---------------------------------------------------------------------------*/
68
69/**Function********************************************************************
70
71  Synopsis [Computes terminal strongly connected components of a
72  markov chain.]
73
74  Description [Computes terminal strongly connected components of a
75  markov chain. tr is the transition relation, tc represents the transitive
76  closure. xVars are the present state variables, yVars the next state
77  variables.]
78
79  SideEffects [scc_table is modified.]
80
81  SeeAlso []
82
83******************************************************************************/
84bdd_node *
85MarkGetSCC(
86  bdd_manager *manager,
87  bdd_node *tr,
88  bdd_node *tc,
89  bdd_node *reached,
90  bdd_node **xVars,
91  bdd_node **yVars,
92  int nVars,
93  st_table **scc_table)
94
95{
96    bdd_node *zero = bdd_read_logic_zero(manager);
97    bdd_node *cr,               /* Cycle relation */
98        *ee,            /* Exterior edges relation, edges between SCCs */
99        *nofanout,      /* Nodes without fanout outside the SCC */
100        *nocycle,       /* Nodes that are not in any cycle */
101        *tnofanout,     /* Temporary nodes without fanout when
102                         * decomposing into SCCs.
103                         */
104        *cub,           /* Arbitrary cube picked inside the SCC */
105        *scc,           /* States in the current SCC */
106        *tmp1,*tmp2;   
107    bdd_node *yCube;
108    bdd_node **permutArray;
109    int i, size;
110 
111
112    /* Build the cycle relation CR(x,y) = TC(x,y)*TC(y,x) */
113    /* tmp1 = tc(y,x) -- retain it to use later in edge relation */
114    bdd_ref(tmp1 = bdd_bdd_swap_variables(manager,tc,xVars,yVars,nVars));
115    bdd_ref(cr = bdd_bdd_and(manager,tc,tmp1));
116 
117    /* Break into SCCs */
118    *scc_table = st_init_table(st_ptrcmp,st_ptrhash);
119 
120    /* Build the exterior edge relation EE(x,y) = tTC(x,y)*tTC'(y,x) */
121    bdd_ref(ee = bdd_bdd_and(manager,tc,bdd_not_bdd_node(tmp1)));
122    bdd_recursive_deref(manager,tmp1);
123 
124    /* Calculate nodes without outgoing edges out the SCCS */
125    bdd_ref(yCube = bdd_bdd_compute_cube(manager,yVars,NULL,nVars));
126    bdd_ref(tmp2 = bdd_bdd_exist_abstract(manager,ee,yCube));
127    bdd_ref(tmp1 = bdd_bdd_and(manager,bdd_not_bdd_node(tmp2),reached));
128    bdd_recursive_deref(manager,tmp2);
129    bdd_recursive_deref(manager,ee);
130    nofanout = tmp1;
131
132    /* Detect the Single SCCs ( SSCCs ) */
133    bdd_ref(tmp2 = bdd_bdd_and(manager,nofanout,cr));
134    bdd_ref(tmp1 = bdd_bdd_exist_abstract(manager,tmp2,yCube));
135    bdd_recursive_deref(manager,tmp2);
136    bdd_ref(nocycle = bdd_bdd_and(manager,nofanout,bdd_not_bdd_node(tmp1)));
137    bdd_recursive_deref(manager,tmp1);
138
139    bdd_recursive_deref(manager,yCube);
140 
141    /* Given the nofanout nodes, expand the SCCs that are inside */
142    bdd_ref(tnofanout = bdd_bdd_and(manager,nofanout,bdd_not_bdd_node(nocycle)));
143    bdd_recursive_deref(manager,nocycle);
144
145    size = bdd_num_vars(manager);
146    permutArray = ALLOC(bdd_node *, size);
147    for(i = 0; i < size; i++) {
148        permutArray[i] = bdd_bdd_ith_var(manager,i);
149        bdd_ref(permutArray[i]);
150    }
151    for(i = 0; i < nVars; i++) {
152        int yindex;
153   
154        yindex = bdd_node_read_index(yVars[i]);
155        bdd_recursive_deref(manager,permutArray[yindex]);
156        bdd_ref(permutArray[yindex] = xVars[i]);
157    }
158
159    /* While there are still nodes in the set tnofanout */
160    while(tnofanout != zero) {
161     
162        /* Pick a point inside the nofanout set */
163        bdd_ref(cub = pickOneCube(manager,tnofanout,xVars,nVars));
164
165        /* Obtain the points connected to "cube" by a cycle and
166         * rename variables.
167         */
168
169        bdd_ref(tmp1 = bdd_bdd_constrain(manager,cr,cub));
170
171        bdd_ref(tmp2 = bdd_bdd_vector_compose(manager,tmp1,permutArray));
172        bdd_recursive_deref(manager,tmp1);
173
174        /* Add the cube to the set, because may be it is not in it */
175        bdd_ref(scc = bdd_bdd_or(manager,tmp2,cub));
176        bdd_recursive_deref(manager,tmp2);
177        st_insert(*scc_table,(char *)cub,(char *)scc);
178
179        /* Delete the SCC from the points without fanout */
180        bdd_ref(tmp2 = bdd_bdd_and(manager,tnofanout,bdd_not_bdd_node(scc)));
181        bdd_recursive_deref(manager,tnofanout);
182        tnofanout = tmp2; 
183    }
184 
185    for(i = 0; i < size; i++) {
186        bdd_recursive_deref(manager,permutArray[i]);
187    }
188    FREE(permutArray);
189    bdd_recursive_deref(manager,tnofanout);
190    bdd_recursive_deref(manager,cr);
191 
192    return(nofanout);
193}
194
195/*---------------------------------------------------------------------------*/
196/* Definition of static   functions                                          */
197/*---------------------------------------------------------------------------*/
198
199/**Function********************************************************************
200
201  Synopsis [Randomly picks a cube from a given function.]
202
203  Description [Randomly picks a cube from a given function.]
204
205  SideEffects [None]
206
207  SeeAlso []
208
209******************************************************************************/
210static bdd_node *
211pickOneCube(
212  bdd_manager *manager,
213  bdd_node *node,
214  bdd_node **xVars,
215  int nVars)
216{
217    char *string;
218    int i, size;
219    int *indices;
220    bdd_node *old, *new_;
221 
222    size = bdd_num_vars(manager);
223    indices = ALLOC(int,nVars);
224    string = ALLOC(char,size);
225    if(! bdd_bdd_pick_one_cube(manager,node,string)) {
226        fprintf(stdout,"mark<->MarkPickOneCube: could not pick a cube\n");
227        exit(-1);
228    }
229    for (i = 0; i < nVars; i++) {
230        indices[i] = bdd_node_read_index(xVars[i]);
231    }
232
233    bdd_ref(old = bdd_read_one(manager));
234
235    for (i = 0; i < nVars; i++) {
236        switch(string[indices[i]]) {
237        case 0:
238            bdd_ref(new_ = bdd_bdd_and(manager,old,bdd_not_bdd_node(xVars[i])));
239            bdd_recursive_deref(manager,old);
240            old = new_;
241            break;
242        case 1:
243            bdd_ref(new_ = bdd_bdd_and(manager,old,xVars[i]));
244            bdd_recursive_deref(manager,old);
245            old = new_;
246            break;
247        }
248    }
249    FREE(string);
250    FREE(indices);
251    bdd_deref(old);
252    return old;
253}
254
255
Note: See TracBrowser for help on using the repository browser.