src/mark/markGetScc.c File Reference
#include "markInt.h"
Include dependency graph for markGetScc.c:
Go to the source code of this file.
Functions | |
| static bdd_node * | pickOneCube (bdd_manager *manager, bdd_node *node, bdd_node **xVars, int nVars) |
| bdd_node * | MarkGetSCC (bdd_manager *manager, bdd_node *tr, bdd_node *tc, bdd_node *reached, bdd_node **xVars, bdd_node **yVars, int nVars, st_table **scc_table) |
Function Documentation
| bdd_node* MarkGetSCC | ( | bdd_manager * | manager, |
| bdd_node * | tr, | ||
| bdd_node * | tc, | ||
| bdd_node * | reached, | ||
| bdd_node ** | xVars, | ||
| bdd_node ** | yVars, | ||
| int | nVars, | ||
| st_table ** | scc_table | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Computes terminal strongly connected components of a markov chain.]
Description [Computes terminal strongly connected components of a markov chain. tr is the transition relation, tc represents the transitive closure. xVars are the present state variables, yVars the next state variables.]
SideEffects [scc_table is modified.]
SeeAlso []
Definition at line 85 of file markGetScc.c.
{
bdd_node *zero = bdd_read_logic_zero(manager);
bdd_node *cr, /* Cycle relation */
*ee, /* Exterior edges relation, edges between SCCs */
*nofanout, /* Nodes without fanout outside the SCC */
*nocycle, /* Nodes that are not in any cycle */
*tnofanout, /* Temporary nodes without fanout when
* decomposing into SCCs.
*/
*cub, /* Arbitrary cube picked inside the SCC */
*scc, /* States in the current SCC */
*tmp1,*tmp2;
bdd_node *yCube;
bdd_node **permutArray;
int i, size;
/* Build the cycle relation CR(x,y) = TC(x,y)*TC(y,x) */
/* tmp1 = tc(y,x) -- retain it to use later in edge relation */
bdd_ref(tmp1 = bdd_bdd_swap_variables(manager,tc,xVars,yVars,nVars));
bdd_ref(cr = bdd_bdd_and(manager,tc,tmp1));
/* Break into SCCs */
*scc_table = st_init_table(st_ptrcmp,st_ptrhash);
/* Build the exterior edge relation EE(x,y) = tTC(x,y)*tTC'(y,x) */
bdd_ref(ee = bdd_bdd_and(manager,tc,bdd_not_bdd_node(tmp1)));
bdd_recursive_deref(manager,tmp1);
/* Calculate nodes without outgoing edges out the SCCS */
bdd_ref(yCube = bdd_bdd_compute_cube(manager,yVars,NULL,nVars));
bdd_ref(tmp2 = bdd_bdd_exist_abstract(manager,ee,yCube));
bdd_ref(tmp1 = bdd_bdd_and(manager,bdd_not_bdd_node(tmp2),reached));
bdd_recursive_deref(manager,tmp2);
bdd_recursive_deref(manager,ee);
nofanout = tmp1;
/* Detect the Single SCCs ( SSCCs ) */
bdd_ref(tmp2 = bdd_bdd_and(manager,nofanout,cr));
bdd_ref(tmp1 = bdd_bdd_exist_abstract(manager,tmp2,yCube));
bdd_recursive_deref(manager,tmp2);
bdd_ref(nocycle = bdd_bdd_and(manager,nofanout,bdd_not_bdd_node(tmp1)));
bdd_recursive_deref(manager,tmp1);
bdd_recursive_deref(manager,yCube);
/* Given the nofanout nodes, expand the SCCs that are inside */
bdd_ref(tnofanout = bdd_bdd_and(manager,nofanout,bdd_not_bdd_node(nocycle)));
bdd_recursive_deref(manager,nocycle);
size = bdd_num_vars(manager);
permutArray = ALLOC(bdd_node *, size);
for(i = 0; i < size; i++) {
permutArray[i] = bdd_bdd_ith_var(manager,i);
bdd_ref(permutArray[i]);
}
for(i = 0; i < nVars; i++) {
int yindex;
yindex = bdd_node_read_index(yVars[i]);
bdd_recursive_deref(manager,permutArray[yindex]);
bdd_ref(permutArray[yindex] = xVars[i]);
}
/* While there are still nodes in the set tnofanout */
while(tnofanout != zero) {
/* Pick a point inside the nofanout set */
bdd_ref(cub = pickOneCube(manager,tnofanout,xVars,nVars));
/* Obtain the points connected to "cube" by a cycle and
* rename variables.
*/
bdd_ref(tmp1 = bdd_bdd_constrain(manager,cr,cub));
bdd_ref(tmp2 = bdd_bdd_vector_compose(manager,tmp1,permutArray));
bdd_recursive_deref(manager,tmp1);
/* Add the cube to the set, because may be it is not in it */
bdd_ref(scc = bdd_bdd_or(manager,tmp2,cub));
bdd_recursive_deref(manager,tmp2);
st_insert(*scc_table,(char *)cub,(char *)scc);
/* Delete the SCC from the points without fanout */
bdd_ref(tmp2 = bdd_bdd_and(manager,tnofanout,bdd_not_bdd_node(scc)));
bdd_recursive_deref(manager,tnofanout);
tnofanout = tmp2;
}
for(i = 0; i < size; i++) {
bdd_recursive_deref(manager,permutArray[i]);
}
FREE(permutArray);
bdd_recursive_deref(manager,tnofanout);
bdd_recursive_deref(manager,cr);
return(nofanout);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_node * pickOneCube | ( | bdd_manager * | manager, |
| bdd_node * | node, | ||
| bdd_node ** | xVars, | ||
| int | nVars | ||
| ) | [static] |
CFile***********************************************************************
FileName [markGetScc.c]
PackageName [mark]
Synopsis [Functions to compute terminal strongly connected components in a markov chain.]
Description [Functions to compute terminal strongly connected components in a markov chain.]
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
Function********************************************************************
Synopsis [Randomly picks a cube from a given function.]
Description [Randomly picks a cube from a given function.]
SideEffects [None]
SeeAlso []
Definition at line 211 of file markGetScc.c.
{
char *string;
int i, size;
int *indices;
bdd_node *old, *new_;
size = bdd_num_vars(manager);
indices = ALLOC(int,nVars);
string = ALLOC(char,size);
if(! bdd_bdd_pick_one_cube(manager,node,string)) {
fprintf(stdout,"mark<->MarkPickOneCube: could not pick a cube\n");
exit(-1);
}
for (i = 0; i < nVars; i++) {
indices[i] = bdd_node_read_index(xVars[i]);
}
bdd_ref(old = bdd_read_one(manager));
for (i = 0; i < nVars; i++) {
switch(string[indices[i]]) {
case 0:
bdd_ref(new_ = bdd_bdd_and(manager,old,bdd_not_bdd_node(xVars[i])));
bdd_recursive_deref(manager,old);
old = new_;
break;
case 1:
bdd_ref(new_ = bdd_bdd_and(manager,old,xVars[i]));
bdd_recursive_deref(manager,old);
old = new_;
break;
}
}
FREE(string);
FREE(indices);
bdd_deref(old);
return old;
}
Here is the caller graph for this function:
