src/mark/mark.c

Go to the documentation of this file.

#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                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* 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);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

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);
}

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                                          */
/*---------------------------------------------------------------------------*/

bdd_node **
MarkAddCKSolve(
  CK *ck)
{
    (void) fprintf(vis_stdout,"Not implemented yet. \n");
    return NIL(bdd_node *);
}


bdd_node **
MarkAddGenSolve(
  CK *ck)
{
    (void) fprintf(vis_stdout,"Not implemented yet. \n");
    return NIL(bdd_node *);
}


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                                            */
/*---------------------------------------------------------------------------*/

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 */

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);
}


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;
}

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);
}

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;
}


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;
}

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;
}

static bdd_node *
computeTransitionRelationWithIds(
  bdd_manager   *ddManager,
  array_t       *nextBdds,
  bdd_node      **yVars,
  int           nVars)
{
    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;
}