/**CFile*********************************************************************** FileName [mark.c] PackageName [mark] Synopsis [Functions for Markov analysis.] Description [External procedures included in this module: Internal procedures included in this module: ] 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" static char rcsid[] UNUSED = "$Id: mark.c,v 1.29 2005/04/27 05:24:08 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Stucture declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static void ckInterface(CK *ck); static bdd_node * recTC(CK *ck, bdd_node *tr); static bdd_node * transitiveClosureByIterSquaring(bdd_manager *ddManager, bdd_node *TR, bdd_node **xVars, bdd_node **yVars, bdd_node **zVars, int nVars); static bdd_node * bddCollapseTSCC(CK *ck); static int sccGetPeriod(CK *ck, bdd_node *reset); static array_t * markGetBddArray(array_t *mvfArray); static bdd_node ** BddNodeArrayFromIdArray(bdd_manager *ddManager, array_t *idArray); static bdd_node * computeTransitionRelationWithIds(bdd_manager *ddManager, array_t *nextBdds, bdd_node **yVars, int nVars); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Perform markovian analysis for Fsm.] Description [Performs Markovian analysis on the given FSM. The function takes as an input an FSM and computes the steady state probabilites. The function returns a pair of DdNodes. The first bdd_node is an ADD representing the steady state probabilities. The support of the ADD is the present state variables. The second one is an ADD representing the one-step transition probability matrix. The support of this ADD is both the present state variables and the next state variables. The function assumes that the partition of the network representing the FSM, has vertices corresponding to the next state functions. No check is made regarding this. Hence, this function should be called only after creating BDDs for the next state functions. solveMethod is one of Solve_GenMethod_c, Solve_FPMethod_c, Solve_CKMethod_c or Solve_Default_c. Currently only Solve_FPMethod_c is supported. Solve_Default_c corresponds to Solve_FPMethod_c. startMethod is one of Start_Default_c, Start_Reset_c or Start_EquiProb_c. The default method is Start_Reset_c. inputProb is a hash table (,) of primary inputs. If inputProb is NULL, the primary inputs are assumed to be equi probable. Probability here means the probability of the primary input to be 1. roundOff is used to round off the calculations to "roundOff" digits after the decimal. The description of algorithms implemented here can be found in .] SideEffects [Reachability analysis is done.] SeeAlso [Mark_ComputeStateProbsWithTr] ******************************************************************************/ bdd_node ** Mark_FsmComputeStateProbs( Fsm_Fsm_t *fsm, Mark_SolveMethod solveMethod, Mark_StartMethod startMethod, st_table *inputProb, int roundOff) { graph_t *partition; bdd_manager *ddManager; array_t *tranFunArray, *leaveIds; array_t *nextBdds, *nextMvfs; int i, phase; int nVars, nPi; bdd_node *tranRelation, **result; bdd_node **xVars,**yVars, **piVars; bdd_node *ddTemp, *reachable; mdd_t *reachStates; if (bdd_get_package_name() != CUDD) { (void) fprintf(vis_stderr,"Synthesis package can be used only with CUDD package\n"); (void) fprintf(vis_stderr,"Please compile with CUDD package\n"); return 0; } if (solveMethod == Solve_CKMethod_c || solveMethod == Solve_GenMethod_c) { fprintf(vis_stdout,"Mark: Solve_CKMethod_c and Solve_GenMethod_c"); fprintf(vis_stdout," not implemented yet\n"); return NIL(bdd_node *); } ddManager = (bdd_manager *)Fsm_FsmReadMddManager(fsm); /* * tranFunArray is a list of next state funs. */ tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm); leaveIds = array_join(Fsm_FsmReadInputVars(fsm), Fsm_FsmReadPresentStateVars(fsm)); /* * Get the BDDs for transition functions.Duplicate functions are returned. */ partition = Fsm_FsmReadPartition(fsm); nextMvfs = Part_PartitionBuildFunctions(partition,tranFunArray,leaveIds, NIL(mdd_t)); array_free(leaveIds); array_free(tranFunArray); nextBdds = markGetBddArray(nextMvfs); Mvf_FunctionArrayFree(nextMvfs); /* Get the DdNodes for all the variables.*/ piVars = BddNodeArrayFromIdArray(ddManager, Fsm_FsmReadInputVars(fsm)); xVars = BddNodeArrayFromIdArray(ddManager, Fsm_FsmReadPresentStateVars(fsm)); yVars = BddNodeArrayFromIdArray(ddManager, Fsm_FsmReadNextStateVars(fsm)); nVars = array_n(Fsm_FsmReadNextStateVars(fsm)); nPi = array_n(Fsm_FsmReadInputVars(fsm)); /* Compute the transition relation */ tranRelation = computeTransitionRelationWithIds(ddManager, nextBdds, yVars, nVars); arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) { bdd_recursive_deref(ddManager,ddTemp); } array_free(nextBdds); /* Compute the reachable states. */ reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000, Fsm_Rch_Default_c,0,0, NIL(array_t),FALSE, NIL(array_t)); ddTemp = (bdd_node *)bdd_get_node(reachStates,&phase); reachable = phase ? bdd_not_bdd_node(ddTemp) : ddTemp; bdd_ref(reachable); mdd_free(reachStates); /* Restrict the STG to only the reachale states */ bdd_ref(ddTemp = bdd_bdd_constrain(ddManager,tranRelation,reachable)); bdd_recursive_deref(ddManager,tranRelation); tranRelation = ddTemp; /* Compute the state probabilities */ /* result[0] = state probabilities, result[1] = transition prob. matrix */ result = Mark_ComputeStateProbsWithTr(ddManager,tranRelation, reachable,piVars, xVars,yVars,NIL(bdd_node *),inputProb, nVars,nPi,roundOff, solveMethod,startMethod); bdd_recursive_deref(ddManager,tranRelation); bdd_recursive_deref(ddManager,reachable); for(i = 0; i < nVars; i++) { bdd_recursive_deref(ddManager,xVars[i]); bdd_recursive_deref(ddManager,yVars[i]); } for(i = 0 ; i < nPi; i++) { bdd_recursive_deref(ddManager,piVars[i]); } FREE(xVars); FREE(yVars); FREE(piVars); return (result); } /**Function******************************************************************** Synopsis [Computes the state probabilities of an FSM.] Description [Computes the state probabilities of an FSM via Markovian analysis. Returns a pointer to a pair ADDs if successful; The ADD in index 0 represents the steady state probabiliites and the ADD in index 1 represents the one step transition probability matrix. NULL is returned in case of a failure. TR is the transition relation of the finite state machine. reachable is a BDD of reachable states. piVars, xVars and yVars are the array of primary inputs, present state variables and next state variables. It is optional to specify a set of auxillary variables zVars for internal use. It could be NULL. If specified the size of zVars equals nVars. inputProb is a hash table (,) for primary inputs. Probability here means the probability of the primary input to be 1. nVars equal the number of present state variables, nPi the number of primary inputs, roundOff implies the number of digits after decimal to round off the calculations. method is one of Solve_GenMethod_c, Solve_FPMethod_c, Solve_CKMethod_c or Solve_Default_c. Currently only Solve_FPMethod_c is supported. Solve_Default_c corresponds to Solve_FPMethod_c. start is one of Start_Default_c, Start_Reset_c or Start_EquiProb_c. The default method is Start_Reset_c.] SideEffects [None] SeeAlso [Mark_ComputeStateProbs] ******************************************************************************/ bdd_node ** Mark_ComputeStateProbsWithTr( bdd_manager *ddManager, bdd_node *TR, bdd_node *reachable, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, bdd_node **zVars, st_table *inputProb, int nVars, int nPi, int roundOff, Mark_SolveMethod method, Mark_StartMethod start) { CK *ck; bdd_node **piAddVars, **xAddVars, **yAddVars, **zAddVars; bdd_node *rep, *scc; bdd_node **result; st_generator *gen; int i, index; int createdPia, createdXa, createdYa, createdZa; int createdZ; int period; /* To suppress Alpha warnings */ yAddVars = NIL(bdd_node *); zAddVars = NIL(bdd_node *); if (bdd_get_package_name() != CUDD) { (void) fprintf(vis_stderr,"Synthesis package can be used only with CUDD package\n"); (void) fprintf(vis_stderr,"Please compile with CUDD package\n"); return 0; } createdPia = createdXa = createdYa = createdZa = 0; createdZ = 0; piAddVars = ALLOC(bdd_node *, nPi); if (piAddVars == NULL) return NULL; createdPia = 1; xAddVars = ALLOC(bdd_node *, nVars); if (xAddVars == NULL) goto endgame; createdXa = 1; yAddVars = ALLOC(bdd_node *, nVars); if (yAddVars == NULL) goto endgame; createdYa = 1; zAddVars = ALLOC(bdd_node *, nVars); if (zAddVars == NULL) goto endgame; createdZa = 1; if (zVars == NULL) { zVars = ALLOC(bdd_node *, nVars); if (zVars == NULL) goto endgame; createdZ = 1; for (i = 0; i < nVars; i++) bdd_ref(zVars[i] = bdd_bdd_new_var(ddManager)); } for(i = 0;i < nPi; i++) { index = bdd_node_read_index(piVars[i]); bdd_ref(piAddVars[i] = bdd_add_ith_var(ddManager,index)); } for(i = 0; i < nVars; i++) { index = bdd_node_read_index(xVars[i]); bdd_ref(xAddVars[i] = bdd_add_ith_var(ddManager,index)); index = bdd_node_read_index(yVars[i]); bdd_ref(yAddVars[i] = bdd_add_ith_var(ddManager,index)); index = bdd_node_read_index(zVars[i]); bdd_ref(zAddVars[i] = bdd_add_ith_var(ddManager,index)); } /* Allocate the structure for internal use */ ck = ALLOC(CK,1); ck->manager = ddManager; ck->piVars = piVars; ck->xVars = xVars; ck->yVars = yVars; ck->zVars = zVars; ck->piAddVars = piAddVars; ck->xAddVars = xAddVars; ck->yAddVars = yAddVars; ck->zAddVars = zAddVars; ck->coeff = NULL; /* assigned in ckInterface - ADD */ ck->nVars = nVars; ck->nPi = nPi; ck->abstol = bdd_read_epsilon(ddManager); ck->scale = 1.0; ck->reltol = 1.0e-4; ck->start = start; ck->roundOff = roundOff; ck->inputProb = inputProb; ck->transition = TR; ck->reached = reachable; ck->indexSCC = NULL; /* assigned in MarkGetSCC called by recTC */ ck->collapsedcoeff = NULL; /* assigned in ckInterface */ ck->term_SCC_states = 0; ck->periods = NULL; /* assigned in bddCollapseTSCC */ ck->term_scc = NULL; /* assigned in ckInterface - ADD */ ck->init_guess = NULL; /* assigned and derefed in all the methods.*/ ckInterface(ck); /* select resolution method */ if (method == Solve_CKMethod_c) { fprintf(stdout,"Mark<->Equations' Solver uses CK Method\n"); result = MarkAddCKSolve(ck); } else if (method == Solve_GenMethod_c) { fprintf(stdout,"Mark<->Equations' Solver uses General Method\n"); result = MarkAddGenSolve(ck); } else { fprintf(stdout,"Mark<->Equations's Solver uses FP Method\n"); result = MarkAddFPSolve(ck); } /* Clean up */ bdd_recursive_deref(ddManager,ck->coeff); st_foreach_item(ck->indexSCC,gen,&rep,&scc) { bdd_recursive_deref(ddManager,rep); bdd_recursive_deref(ddManager,scc); } st_free_table(ck->indexSCC); bdd_recursive_deref(ddManager,ck->collapsedcoeff); st_foreach_item_int(ck->periods,gen,&rep, &period) { bdd_recursive_deref(ddManager,rep); } st_free_table(ck->periods); bdd_recursive_deref(ddManager,ck->term_scc); for(i = 0; i < nPi; i++) { bdd_recursive_deref(ddManager,piAddVars[i]); } for(i = 0; i < nVars; i++) { bdd_recursive_deref(ddManager,xAddVars[i]); bdd_recursive_deref(ddManager,yAddVars[i]); bdd_recursive_deref(ddManager,zAddVars[i]); } if (createdZ) { for(i = 0; i < nVars; i++) { bdd_recursive_deref(ddManager,zVars[i]); } FREE(zVars); } FREE(xAddVars); FREE(yAddVars); FREE(zAddVars); FREE(piAddVars); FREE(ck); return result; endgame: if (createdPia) FREE(piAddVars); if (createdXa) FREE(xAddVars); if (createdYa) FREE(yAddVars); if (createdZa) FREE(zAddVars); if (createdZ) FREE(zVars); return NULL; } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Not implemented yet.] Description [Not implemented yet.] SideEffects [None] SeeAlso [] ******************************************************************************/ bdd_node ** MarkAddCKSolve( CK *ck) { (void) fprintf(vis_stdout,"Not implemented yet. \n"); return NIL(bdd_node *); } /**Function******************************************************************** Synopsis [Not implemented yet.] Description [Not implemented yet.] SideEffects [None] SeeAlso [] ******************************************************************************/ bdd_node ** MarkAddGenSolve( CK *ck) { (void) fprintf(vis_stdout,"Not implemented yet. \n"); return NIL(bdd_node *); } /**Function******************************************************************** Synopsis [Calculate the average bit change in the STG.] Description [Calculate the average bit change in the STG. probTR is an ADD representing the absolute transition probability matrix of the STG. xVars and yVars are the present and next state variables respectively. nVars is the number of state variables. average bit change = (\exists^+_x(probTr * HD(x,y))). The interested reader is referred to R. I. Bahar and E. A. Frohm and C. M. Gaona and G. D. Hachtel and E. Macii and A. Pardo and F. Somenzi, "Algebraic Decision Diagrams and their Applications", International Conference on Computer Aided Design, 1993. on details pertaining to ADDs. ] SideEffects [None] SeeAlso [] ******************************************************************************/ double MarkAverageBitChange( bdd_manager *manager, bdd_node *probTR, bdd_node **xVars, bdd_node **yVars, int nVars) { bdd_node *diff, *cube, *PA, *QA; bdd_node **vars; double Mean; int i; vars = ALLOC(bdd_node *,2*nVars); for (i = 0; i < nVars; i++) { vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(xVars[i])); bdd_ref(vars[i]); } for (i = nVars; i < 2*nVars; i++) { vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(yVars[i-nVars])); bdd_ref(vars[i]); } cube = bdd_add_compute_cube(manager,vars,NULL,2*nVars); bdd_ref(cube); /* Calculate the Hamming distance ADD. This ADD represents the hamming * distance between two vectors represented by xVars and yVars. */ bdd_ref(diff = bdd_add_hamming(manager,xVars,yVars,nVars)); bdd_ref(PA = bdd_add_apply(manager,bdd_add_times,probTR,diff)); bdd_recursive_deref(manager,diff); /* And now add and abstract all the variables.*/ bdd_ref(QA = bdd_add_exist_abstract(manager,PA,cube)); bdd_recursive_deref(manager,PA); bdd_recursive_deref(manager,cube); Mean = (double)bdd_add_value(QA); bdd_recursive_deref(manager,QA); for (i = 0; i < 2*nVars; i++) { bdd_recursive_deref(manager,vars[i]); } FREE(vars); return Mean; } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Perform structural decomposition of the markov chain.] Description [] SideEffects [The data structure ck is changed.] SeeAlso [] ******************************************************************************/ static void ckInterface( CK *ck) { bdd_manager *ddManager; bdd_node *piCube; bdd_node *new_; bdd_node *tmp1,*tmp2; bdd_node *p, *t; bdd_node *reachable, *TR; bdd_node *q, *r; st_table *newSCC; st_table *newperiods; st_generator *gen; int len, nVars; ddManager = ck->manager; reachable = ck->reached; TR = ck->transition; nVars = ck->nVars; bdd_ref(piCube = bdd_bdd_compute_cube(ddManager,ck->piVars,NULL,ck->nPi)); /* abstract the PI variables for the SCC computation */ bdd_ref(new_ = bdd_bdd_exist_abstract(ddManager,TR,piCube)); bdd_recursive_deref(ddManager,piCube); /* now find the set of nodes in terminal SCC's */ p = recTC(ck,new_); bdd_recursive_deref(ddManager,new_); /* Collapse the TSCC in the graph */ ck->collapsedcoeff = bddCollapseTSCC(ck); bdd_ref(ck->collapsedcoeff); /* retain only reachable terminal SCC's */ bdd_ref(t = bdd_bdd_and(ddManager,p,reachable)); bdd_recursive_deref(ddManager,p); /* count the number of states in the terminal SCC's */ ck->term_SCC_states = bdd_count_minterm(ddManager,t,nVars); (void) fprintf(vis_stdout,"# of states in TSCCs = %f\n", ck->term_SCC_states); /* Translate the data in ck->collapsedcoeff and * ck->indexSCC from BDDs to ADDs. */ newSCC = st_init_table(st_ptrcmp,st_ptrhash); newperiods = st_init_table(st_ptrcmp,st_ptrhash); st_foreach_item(ck->indexSCC,gen,&tmp1,&tmp2) { bdd_ref(q = bdd_bdd_to_add(ddManager,tmp1)); bdd_ref(r = bdd_bdd_to_add(ddManager,tmp2)); st_lookup_int(ck->periods,(char *)tmp1, &len); st_insert(newSCC,(char *)q,(char *)r); st_insert(newperiods,(char *)q,(char *)(long)len); bdd_recursive_deref(ddManager,tmp1); bdd_recursive_deref(ddManager,tmp2); } st_free_table(ck->indexSCC); st_free_table(ck->periods); bdd_ref(q = bdd_bdd_to_add(ddManager,ck->collapsedcoeff)); bdd_recursive_deref(ddManager,ck->collapsedcoeff); ck->collapsedcoeff = q; ck->indexSCC = newSCC; ck->periods = newperiods; /* Print the number of TSCCs */ (void) fprintf(vis_stdout,"# of TSCCs = %d\n",st_count(newSCC)); /* convert the transition relation BDD into an ADD */ bdd_ref(q = bdd_bdd_to_add(ddManager,TR)); ck->coeff = q; /* convert the term_scc set BDD into an ADD */ bdd_ref(q = bdd_bdd_to_add(ddManager,t)); ck->term_scc = q; bdd_recursive_deref(ddManager,t); } /* End of ckInterface */ /**Function******************************************************************** Synopsis [Compute the strongly connected components.] Description [] SideEffects [ck->indexSCC changed.] SeeAlso [] ******************************************************************************/ static bdd_node * recTC( CK *ck, bdd_node *tr) { bdd_manager *manager = ck->manager; bdd_node **xVars, **yVars, **zVars; bdd_node *closure; bdd_node *lastScc; int nVars; xVars = ck->xVars; yVars = ck->yVars; zVars = ck->zVars; nVars = ck->nVars; /* Matsunaga's procedure could also be used. Will have to implement it * later. */ closure = transitiveClosureByIterSquaring(manager,tr,xVars,yVars,zVars, nVars); bdd_ref(closure); lastScc = MarkGetSCC(manager,tr,closure,ck->reached, xVars, yVars, nVars, &(ck->indexSCC)); bdd_recursive_deref(manager,closure); return(lastScc); } /**Function******************************************************************** Synopsis [Computes the transitive closure by iterative squaring.] Description [] SideEffects [None] SeeAlso [] ******************************************************************************/ static bdd_node * transitiveClosureByIterSquaring( bdd_manager *ddManager, bdd_node *TR, bdd_node **xVars, bdd_node **yVars, bdd_node **zVars, int nVars) { bdd_node *prev, *next, *TRxz, *TRzy; bdd_node *inter; bdd_node *zCube; bdd_ref(zCube = bdd_bdd_compute_cube(ddManager,zVars,NULL,nVars)); bdd_ref(prev = TR); while(1) { TRxz = bdd_bdd_swap_variables(ddManager,prev,yVars,zVars,nVars); bdd_ref(TRxz); TRzy = bdd_bdd_swap_variables(ddManager,prev,xVars,zVars,nVars); bdd_ref(TRzy); inter = bdd_bdd_and_abstract(ddManager,TRxz,TRzy,zCube); bdd_ref(inter); bdd_recursive_deref(ddManager,TRxz); bdd_recursive_deref(ddManager,TRzy); next = bdd_bdd_or(ddManager,TR,inter); bdd_ref(next); bdd_recursive_deref(ddManager,inter); if(prev == next) break; bdd_recursive_deref(ddManager,prev); prev = next; } bdd_recursive_deref(ddManager,zCube); bdd_recursive_deref(ddManager,prev); bdd_deref(next); return next; } /**Function******************************************************************** Synopsis [Collapse the Terminal SCCs into a macro node.] Description [] SideEffects [ck->periods is changed.] SeeAlso [] ******************************************************************************/ static bdd_node * bddCollapseTSCC( CK *ck) { bdd_manager *manager = ck->manager; bdd_node *tmp1,*tmp2; bdd_node *repr,*scc,*restscc; bdd_node *newtr; bdd_node *xCube,*yCube; bdd_node *sccfanout,*sccfanin; st_generator *gen; int i; bdd_ref(xCube = bdd_bdd_compute_cube(manager,ck->xVars,NULL,ck->nVars)); bdd_ref(yCube = bdd_bdd_compute_cube(manager,ck->yVars,NULL,ck->nVars)); ck->periods = st_init_table(st_ptrcmp,st_ptrhash); bdd_ref(newtr = ck->transition); i = 0; st_foreach_item(ck->indexSCC,gen,&repr,&scc) { /* Traverse the SCC to obtain the period */ st_insert(ck->periods,(char *)repr,(char *)(long)sccGetPeriod(ck,repr)); /* Add edges from scc to the representatives in the fanout */ bdd_ref(sccfanout = bdd_bdd_and_abstract(manager,newtr,scc,xCube)); bdd_ref(tmp1 = bdd_bdd_and(manager,scc,sccfanout)); bdd_recursive_deref(manager,sccfanout); bdd_ref(tmp2 = bdd_bdd_or(manager,newtr,tmp1)); bdd_recursive_deref(manager,tmp1); bdd_recursive_deref(manager,newtr); newtr = tmp2; /* Add edges from fanin to representative */ bdd_ref(tmp2 = bdd_bdd_swap_variables(manager,scc,ck->xVars,ck->yVars, ck->nVars)); bdd_ref(sccfanin = bdd_bdd_and_abstract(manager,newtr,tmp2,yCube)); bdd_recursive_deref(manager,tmp2); /* Add edges (fanin,representative) to the TR */ bdd_ref(tmp1 = bdd_bdd_swap_variables(manager,repr,ck->xVars, ck->yVars,ck->nVars)); bdd_ref(tmp2 = bdd_bdd_and(manager,sccfanin,tmp1)); bdd_recursive_deref(manager,tmp1); bdd_recursive_deref(manager,sccfanin); bdd_ref(tmp1 = bdd_bdd_or(manager,newtr,tmp2)); bdd_recursive_deref(manager,tmp2); bdd_recursive_deref(manager,newtr); newtr = tmp1; /*Delete the edges that go to the non-representative nodes */ bdd_ref(restscc = bdd_bdd_and(manager,scc,bdd_not_bdd_node(repr))); bdd_ref(tmp1 = bdd_bdd_and(manager,newtr,bdd_not_bdd_node(restscc))); bdd_ref(tmp2 = bdd_bdd_swap_variables(manager,restscc,ck->xVars, ck->yVars,ck->nVars)); bdd_recursive_deref(manager,restscc); bdd_recursive_deref(manager,newtr); bdd_ref(newtr = bdd_bdd_and(manager,tmp1,bdd_not_bdd_node(tmp2))); bdd_recursive_deref(manager,tmp1); bdd_recursive_deref(manager,tmp2); i++; } bdd_recursive_deref(manager,xCube); bdd_recursive_deref(manager,yCube); bdd_deref(newtr); return(newtr); } /**Function******************************************************************** Synopsis [Compute the period of the SCC.] Description [] SideEffects [None] SeeAlso [] ******************************************************************************/ static int sccGetPeriod( CK *ck, bdd_node *reset) { bdd_manager *manager = ck->manager; bdd_node *new_,*from; bdd_node *tmp1; bdd_node *xCube, *inputCube; bdd_node *transition; int pos,result = 0; int depth; int stop = 0; st_table *tos; st_generator *gen; /* Calculate the cube for abstraction */ bdd_ref(xCube = bdd_bdd_compute_cube(manager,ck->xVars,NULL,ck->nVars)); bdd_ref(inputCube = bdd_bdd_compute_cube(manager,ck->piVars,NULL,ck->nPi)); bdd_ref(transition = bdd_bdd_exist_abstract(manager,ck->transition, inputCube)); bdd_recursive_deref(manager,inputCube); depth = 0; bdd_ref(from = reset); bdd_ref(tmp1 = reset); tos = st_init_table(st_ptrcmp,st_ptrhash); depth++; st_insert(tos,(char *)tmp1,(char *)(long)depth); while(!stop) { bdd_ref(tmp1 = bdd_bdd_and_abstract(manager,from,transition,xCube)); bdd_ref(new_ = bdd_bdd_swap_variables(manager,tmp1,ck->yVars,ck->xVars, ck->nVars)); bdd_recursive_deref(manager,tmp1); if((stop = st_lookup_int(tos,(char *)new_, &pos))) result = depth - pos; else st_insert(tos,(char *)new_,(char *)(long)depth); bdd_recursive_deref(manager,from); bdd_ref(from = new_); depth++; } bdd_recursive_deref(manager,new_); bdd_recursive_deref(manager,xCube); bdd_recursive_deref(manager,from); st_foreach_item_int(tos,gen,&new_, &pos) { bdd_recursive_deref(manager,new_); } st_free_table(tos); return result; } /**Function******************************************************************** Synopsis [Returns a BDD array from an Mvf array] SideEffects [None] SeeAlso [] ******************************************************************************/ static array_t * markGetBddArray(array_t *mvfArray) { int i,phase; array_t *bddArray; Mvf_Function_t *mvf; bddArray = array_alloc(bdd_node *,0); arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) { mdd_t *mddTemp; bdd_node *ddNode; mddTemp = array_fetch(mdd_t *, mvf, 1); ddNode = (bdd_node *) bdd_get_node(mddTemp,&phase); bdd_ref(ddNode); ddNode = phase ? bdd_not_bdd_node(ddNode) : ddNode; array_insert_last(bdd_node *, bddArray, ddNode); } return bddArray; } /**Function******************************************************************** Synopsis [Returns a BDD array given an integer array of variable indices.] SideEffects [None] SeeAlso [] ******************************************************************************/ static bdd_node ** BddNodeArrayFromIdArray( bdd_manager *ddManager, array_t *idArray) { bdd_node **xvars; int i,id; int nvars = array_n(idArray); xvars = ALLOC(bdd_node *, nvars); if (xvars == NULL) return NULL; for(i = 0; i < nvars; i++) { id = array_fetch(int,idArray,i); xvars[i] = bdd_bdd_ith_var(ddManager,id); bdd_ref(xvars[i]); } return xvars; } /**Function******************************************************************** Synopsis [Compute the relation between an array of function and a corresponding array of variables. A BDD is returned which represents AND(i=0 -> i