/**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.] ******************************************************************************/ #include "markInt.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Stucture declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static bdd_node * pickOneCube(bdd_manager *manager, bdd_node *node, bdd_node **xVars, int nVars); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ 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) { 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); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Randomly picks a cube from a given function.] Description [Randomly picks a cube from a given function.] SideEffects [None] SeeAlso [] ******************************************************************************/ static bdd_node * pickOneCube( bdd_manager *manager, bdd_node *node, bdd_node **xVars, int nVars) { 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; }