src/mark/markFPSolve.c

Go to the documentation of this file.

#include "markInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


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


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

bdd_node ** 
MarkAddFPSolve(
  CK *ck)
{
    bdd_manager *manager;
    bdd_node **xAddVars, **yAddVars;
    bdd_node *Scaling;
    bdd_node *InitG, *G, *NewG;
    bdd_node *p, *q, *newTr;
    bdd_node *xCube, *ddTemp, *guess; 
    bdd_node *zero;
    bdd_node **result;
    bdd_node *probMatrix;
    int nVars, iter = 0;
    int converged;
    double max;

    manager = ck->manager;
    nVars = ck->nVars;
    xAddVars = ck->xAddVars;
    yAddVars = ck->yAddVars;

    result = ALLOC(bdd_node *, 2);
    if (result == NULL)
        return NULL;
    zero = bdd_read_zero(manager);

    /* Build an ADD for one step transition probability matrix */
    bdd_ref(probMatrix = MarkAddBuildCoeff(manager,ck->coeff, ck->piAddVars,
                                            ck->inputProb, ck->scale, nVars,
                                            ck->nPi));
    result[1] = probMatrix;

    /* create initial guess and print it;
     * equiprobability to all the states and probability 1 to one of the
     * reset states are currently supported
     */
    switch(ck->start) {
    case Start_EquiProb_c:
        (void)printf("Initial guess: equiprob\n");
        bdd_ref(ck->init_guess = ck->term_scc);
        p = bdd_add_const(manager,
                          (double) (1/(double)(ck->term_SCC_states)));
        bdd_ref(p);
        bdd_ref(q = bdd_add_ite(manager,ck->init_guess,p,zero)); 
        bdd_recursive_deref(manager,p);
        InitG = bdd_add_swap_variables(manager,q,xAddVars,yAddVars,nVars);
        bdd_ref(InitG);
        bdd_recursive_deref(manager,q);
        bdd_recursive_deref(manager,ck->init_guess);
        break;
    case Start_Reset_c:
    default:
        /* Pick one of the states in the TSCC as the initial guess */
        bdd_ref(ddTemp = bdd_add_bdd_threshold(manager,ck->term_scc,1));
        bdd_ref(guess = bdd_bdd_pick_one_minterm(manager, ddTemp,
                                             ck->xVars, nVars));
        bdd_recursive_deref(manager,ddTemp);
        bdd_ref(ck->init_guess = bdd_bdd_to_add(manager,guess));
        bdd_recursive_deref(manager,guess);
        bdd_ref(InitG = bdd_add_swap_variables(manager,ck->init_guess,
                                               xAddVars, yAddVars,nVars));
        bdd_recursive_deref(manager,ck->init_guess);
        break;
    }

    /* put prob. transition matrix in appropriate form (transpose)*/
    newTr = bdd_add_swap_variables(manager,probMatrix,xAddVars,yAddVars,nVars);
    bdd_ref(newTr);

    /* calculate the x-cube for abstraction */
    bdd_ref(xCube = bdd_add_compute_cube(manager,xAddVars,NULL,nVars));
 
    do {
        iter++;
        G = bdd_add_matrix_multiply(manager,newTr,InitG,yAddVars,nVars);
        bdd_ref(G);
        bdd_ref(Scaling = bdd_add_exist_abstract(manager,G,xCube));

        bdd_ref(NewG = bdd_add_apply(manager,bdd_add_divide,G,Scaling));
        bdd_recursive_deref(manager,G);
        G = NewG; 
        bdd_recursive_deref(manager,Scaling);
        q = bdd_add_swap_variables(manager,G,xAddVars,yAddVars,nVars);
        bdd_ref(q);
        max = bdd_add_value(bdd_add_find_max(manager,InitG));
        converged = bdd_equal_sup_norm(manager,q,InitG,ck->reltol*max,0);
        bdd_recursive_deref( manager,InitG);
        if (converged) {
            (void) fprintf(vis_stdout,"Iteration = %d\n",iter);
            bdd_recursive_deref( manager,newTr);
            bdd_recursive_deref( manager,q);
            bdd_recursive_deref(manager,xCube);
            result[0] = G;
            return result;
        }
        bdd_recursive_deref( manager,G);
        InitG = q;
    } while (1);

} /* end of addFPSolve */


bdd_node *
MarkAddBuildCoeff(
  bdd_manager *manager,
  bdd_node *func,
  bdd_node **piAddVars,
  st_table *inputProb,
  double scale,
  int nVars,
  int nPi)
{
    /* Given func, the coefficient matrix is built */
    /* this function is used first to build the collapsed coeff matrix */
    /* and then the matrix for every TSCC */

    bdd_node *Correction;
    bdd_node *q;
    bdd_node *matrix;
    bdd_node *piAddCube;

    bdd_ref(piAddCube = bdd_add_compute_cube(manager,piAddVars,NULL,nPi));

    /* Create the transition matrix either with equiprobable
       or specific input probs. */

    if (inputProb != NULL) {
      bdd_ref(matrix = Mark_addInProb(manager,func,piAddCube,inputProb));
    }
    else {
      /* create correction ADD and print it */
      bdd_ref(Correction = bdd_add_const(manager,
                                          (scale/(double)(1 << nPi))));
      
      bdd_ref(q = bdd_add_exist_abstract(manager,func,piAddCube));
      
      /* apply correction to the transition relation matrix and print it */
      bdd_ref(matrix = bdd_add_apply(manager, bdd_add_times,q, Correction));
      bdd_recursive_deref( manager,Correction);
      bdd_recursive_deref(manager,q);
    }
    bdd_recursive_deref(manager,piAddCube);
    bdd_deref(matrix);
    return(matrix);
}