#include "markInt.h"
Include dependency graph for mark.c:
Go to the source code of this file.
Functions | |
| 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) |
| bdd_node ** | Mark_FsmComputeStateProbs (Fsm_Fsm_t *fsm, Mark_SolveMethod solveMethod, Mark_StartMethod startMethod, st_table *inputProb, int roundOff) |
| 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) |
| bdd_node ** | MarkAddCKSolve (CK *ck) |
| bdd_node ** | MarkAddGenSolve (CK *ck) |
| double | MarkAverageBitChange (bdd_manager *manager, bdd_node *probTR, bdd_node **xVars, bdd_node **yVars, int nVars) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mark.c,v 1.29 2005/04/27 05:24:08 fabio Exp $" |
Function Documentation
| static bdd_node * bddCollapseTSCC | ( | CK * | ck | ) | [static] |
Function********************************************************************
Synopsis [Collapse the Terminal SCCs into a macro node.]
Description []
SideEffects [ck->periods is changed.]
SeeAlso []
Definition at line 766 of file mark.c.
{
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);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_node ** BddNodeArrayFromIdArray | ( | bdd_manager * | ddManager, |
| array_t * | idArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Returns a BDD array given an integer array of variable indices.]
SideEffects [None]
SeeAlso []
Definition at line 952 of file mark.c.
{
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;
}
Here is the caller graph for this function:
| static void ckInterface | ( | CK * | ck | ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Perform structural decomposition of the markov chain.]
Description []
SideEffects [The data structure ck is changed.]
SeeAlso []
Definition at line 581 of file mark.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_node * computeTransitionRelationWithIds | ( | bdd_manager * | ddManager, |
| array_t * | nextBdds, | ||
| bdd_node ** | yVars, | ||
| int | nVars | ||
| ) | [static] |
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<nVars)(yVars[i]==nextBdds). ]
SideEffects []
SeeAlso []
Definition at line 984 of file mark.c.
{
bdd_node *ddtemp1, *ddtemp2;
bdd_node *oldTR, *fn;
int i;
oldTR = bdd_read_one(ddManager);
for(i = 0; i < nVars; i++) {
ddtemp2 = array_fetch(bdd_node *, nextBdds, i);
fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
bdd_ref(fn);
ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
bdd_ref(ddtemp1);
bdd_recursive_deref(ddManager,fn);
bdd_recursive_deref(ddManager,oldTR);
oldTR = ddtemp1;
}
return oldTR;
}
Here is the caller graph for this function:
| 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 | ||
| ) |
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 (<name>,<probability>) 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]
Definition at line 268 of file mark.c.
{
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;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node** Mark_FsmComputeStateProbs | ( | Fsm_Fsm_t * | fsm, |
| Mark_SolveMethod | solveMethod, | ||
| Mark_StartMethod | startMethod, | ||
| st_table * | inputProb, | ||
| int | roundOff | ||
| ) |
AutomaticEnd 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 (<name>,<probability>) 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 <Ref>.]
SideEffects [Reachability analysis is done.]
SeeAlso [Mark_ComputeStateProbsWithTr]
Definition at line 117 of file mark.c.
{
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);
}
Here is the call graph for this function:
| bdd_node** MarkAddCKSolve | ( | CK * | ck | ) |
Function********************************************************************
Synopsis [Not implemented yet.]
Description [Not implemented yet.]
SideEffects [None]
SeeAlso []
Definition at line 466 of file mark.c.
{
(void) fprintf(vis_stdout,"Not implemented yet. \n");
return NIL(bdd_node *);
}
Here is the caller graph for this function:
| bdd_node** MarkAddGenSolve | ( | CK * | ck | ) |
Function********************************************************************
Synopsis [Not implemented yet.]
Description [Not implemented yet.]
SideEffects [None]
SeeAlso []
Definition at line 486 of file mark.c.
{
(void) fprintf(vis_stdout,"Not implemented yet. \n");
return NIL(bdd_node *);
}
Here is the caller graph for this function:
| double MarkAverageBitChange | ( | bdd_manager * | manager, |
| bdd_node * | probTR, | ||
| bdd_node ** | xVars, | ||
| bdd_node ** | yVars, | ||
| int | nVars | ||
| ) |
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 = (^+_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 []
Definition at line 519 of file mark.c.
{
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;
}
| static array_t * markGetBddArray | ( | array_t * | mvfArray | ) | [static] |
Function********************************************************************
Synopsis [Returns a BDD array from an Mvf array]
SideEffects [None]
SeeAlso []
Definition at line 920 of file mark.c.
{
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;
}
Here is the caller graph for this function:
| static bdd_node * recTC | ( | CK * | ck, |
| bdd_node * | tr | ||
| ) | [static] |
Function********************************************************************
Synopsis [Compute the strongly connected components.]
Description []
SideEffects [ck->indexSCC changed.]
SeeAlso []
Definition at line 672 of file mark.c.
{
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);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int sccGetPeriod | ( | CK * | ck, |
| bdd_node * | reset | ||
| ) | [static] |
Function********************************************************************
Synopsis [Compute the period of the SCC.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 850 of file mark.c.
{
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;
}
Here is the caller graph for this function:
| static bdd_node * transitiveClosureByIterSquaring | ( | bdd_manager * | ddManager, |
| bdd_node * | TR, | ||
| bdd_node ** | xVars, | ||
| bdd_node ** | yVars, | ||
| bdd_node ** | zVars, | ||
| int | nVars | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes the transitive closure by iterative squaring.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 716 of file mark.c.
{
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;
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: mark.c,v 1.29 2005/04/27 05:24:08 fabio Exp $" [static] |
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.]
