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

Last change on this file since 82 was 14, checked in by cecile, 15 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.