source: vis_dev/vis-2.3/src/mark/mark.c @ 17

Last change on this file since 17 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 29.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [mark.c]
4
5  PackageName [mark]
6
7  Synopsis    [Functions for Markov analysis.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Mark_FsmComputeStateProbs()
12                <li> Mark_ComputeStateProbsWithTr()
13                </ul>
14        Internal procedures included in this module:
15                <ul>
16                <li> MarkAverageBitChange()
17                </ul> ]
18
19  Author      [Balakrishna Kumthekar]
20
21  Copyright   [This file was created at the University of Colorado at
22  Boulder.  The University of Colorado at Boulder makes no warranty
23  about the suitability of this software for any purpose.  It is
24  presented on an AS IS basis.]
25
26******************************************************************************/
27
28#include "markInt.h"
29
30static char rcsid[] UNUSED = "$Id: mark.c,v 1.29 2005/04/27 05:24:08 fabio Exp $";
31
32/*---------------------------------------------------------------------------*/
33/* Constant declarations                                                     */
34/*---------------------------------------------------------------------------*/
35
36
37/*---------------------------------------------------------------------------*/
38/* Stucture declarations                                                     */
39/*---------------------------------------------------------------------------*/
40
41
42/*---------------------------------------------------------------------------*/
43/* Type declarations                                                         */
44/*---------------------------------------------------------------------------*/
45
46
47/*---------------------------------------------------------------------------*/
48/* Variable declarations                                                     */
49/*---------------------------------------------------------------------------*/
50
51
52/*---------------------------------------------------------------------------*/
53/* Macro declarations                                                        */
54/*---------------------------------------------------------------------------*/
55
56
57/**AutomaticStart*************************************************************/
58
59/*---------------------------------------------------------------------------*/
60/* Static function prototypes                                                */
61/*---------------------------------------------------------------------------*/
62
63static void ckInterface(CK *ck);
64static bdd_node * recTC(CK *ck, bdd_node *tr);
65static bdd_node * transitiveClosureByIterSquaring(bdd_manager *ddManager, bdd_node *TR, bdd_node **xVars, bdd_node **yVars, bdd_node **zVars, int nVars);
66static bdd_node * bddCollapseTSCC(CK *ck);
67static int sccGetPeriod(CK *ck, bdd_node *reset);
68static array_t * markGetBddArray(array_t *mvfArray);
69static bdd_node ** BddNodeArrayFromIdArray(bdd_manager *ddManager, array_t *idArray);
70static bdd_node * computeTransitionRelationWithIds(bdd_manager *ddManager, array_t *nextBdds, bdd_node **yVars, int nVars);
71
72/**AutomaticEnd***************************************************************/
73
74
75/*---------------------------------------------------------------------------*/
76/* Definition of exported functions                                          */
77/*---------------------------------------------------------------------------*/
78
79/**Function********************************************************************
80
81  Synopsis    [Perform markovian analysis for Fsm.]
82
83  Description [Performs Markovian analysis on the given FSM. The function
84  takes as an input an FSM and computes the steady state probabilites. The
85  function returns a pair of DdNodes. The first bdd_node is an ADD representing
86  the steady state probabilities. The support of the ADD is the present state
87  variables. The second one is an ADD representing the one-step transition
88  probability matrix. The support of this ADD is both the present state
89  variables and the next state variables.
90
91  The function assumes that the partition of the network representing the
92  FSM, has vertices corresponding to the next state functions. No check is
93  made regarding this. Hence, this function should be called only after
94  creating BDDs for the next state functions.
95
96  solveMethod is one of Solve_GenMethod_c, Solve_FPMethod_c, Solve_CKMethod_c
97  or Solve_Default_c. Currently only Solve_FPMethod_c is supported.
98  Solve_Default_c corresponds to Solve_FPMethod_c.
99
100  startMethod is one of Start_Default_c, Start_Reset_c or Start_EquiProb_c.
101  The default method is Start_Reset_c.
102
103  inputProb is a hash table (<name>,<probability>) of primary inputs. If
104  inputProb is NULL, the primary inputs are assumed to be equi probable.
105  Probability here means the probability of the primary input to be 1.
106
107  roundOff is used to round off the calculations to "roundOff" digits
108  after the decimal.
109
110  The description of algorithms implemented here can be found in <Ref>.]
111
112  SideEffects [Reachability analysis is done.]
113
114  SeeAlso [Mark_ComputeStateProbsWithTr]
115******************************************************************************/
116bdd_node **
117Mark_FsmComputeStateProbs(
118  Fsm_Fsm_t *fsm,
119  Mark_SolveMethod solveMethod,
120  Mark_StartMethod startMethod,
121  st_table *inputProb,
122  int roundOff)
123{
124    graph_t *partition;
125    bdd_manager *ddManager;
126
127    array_t *tranFunArray, *leaveIds;
128    array_t *nextBdds, *nextMvfs;
129
130    int i, phase;
131    int nVars, nPi;
132
133    bdd_node *tranRelation, **result;
134    bdd_node **xVars,**yVars, **piVars;
135    bdd_node *ddTemp, *reachable;
136
137    mdd_t *reachStates;
138   
139    if (bdd_get_package_name() != CUDD) {
140        (void) fprintf(vis_stderr,"Synthesis package can be used only with CUDD package\n");
141        (void) fprintf(vis_stderr,"Please compile with CUDD package\n");
142        return 0;
143    }
144
145    if (solveMethod == Solve_CKMethod_c ||
146        solveMethod == Solve_GenMethod_c) {
147        fprintf(vis_stdout,"Mark: Solve_CKMethod_c and Solve_GenMethod_c");
148        fprintf(vis_stdout," not implemented yet\n");
149        return NIL(bdd_node *);
150    }
151
152    ddManager = (bdd_manager *)Fsm_FsmReadMddManager(fsm);
153
154    /*
155     * tranFunArray is a list of next state funs.
156     */
157
158    tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
159
160    leaveIds = array_join(Fsm_FsmReadInputVars(fsm),
161                          Fsm_FsmReadPresentStateVars(fsm));
162    /*
163     * Get the BDDs for transition functions.Duplicate functions are returned.
164     */
165    partition = Fsm_FsmReadPartition(fsm);
166    nextMvfs = Part_PartitionBuildFunctions(partition,tranFunArray,leaveIds,
167                                            NIL(mdd_t));
168    array_free(leaveIds);
169    array_free(tranFunArray);
170    nextBdds = markGetBddArray(nextMvfs);
171
172    Mvf_FunctionArrayFree(nextMvfs);
173
174    /* Get the DdNodes for all the variables.*/
175
176    piVars = BddNodeArrayFromIdArray(ddManager, 
177                                         Fsm_FsmReadInputVars(fsm));
178    xVars = BddNodeArrayFromIdArray(ddManager, 
179                                        Fsm_FsmReadPresentStateVars(fsm));
180    yVars = BddNodeArrayFromIdArray(ddManager,
181                                        Fsm_FsmReadNextStateVars(fsm));
182
183    nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
184    nPi = array_n(Fsm_FsmReadInputVars(fsm));
185
186    /* Compute the transition relation */
187    tranRelation = computeTransitionRelationWithIds(ddManager, nextBdds,
188                                                    yVars, nVars);
189
190    arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
191        bdd_recursive_deref(ddManager,ddTemp);
192    }
193    array_free(nextBdds);
194
195    /* Compute the reachable states. */
196    reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
197                                                Fsm_Rch_Default_c,0,0,
198                                                NIL(array_t),FALSE, NIL(array_t));
199
200    ddTemp = (bdd_node *)bdd_get_node(reachStates,&phase);
201    reachable = phase ?  bdd_not_bdd_node(ddTemp) : ddTemp;
202    bdd_ref(reachable);
203    mdd_free(reachStates);
204
205    /* Restrict the STG to only the reachale states */
206    bdd_ref(ddTemp = bdd_bdd_constrain(ddManager,tranRelation,reachable));
207    bdd_recursive_deref(ddManager,tranRelation);
208    tranRelation = ddTemp;
209   
210    /* Compute the state probabilities */
211    /* result[0] = state probabilities, result[1] = transition prob. matrix */
212    result = Mark_ComputeStateProbsWithTr(ddManager,tranRelation,
213                                          reachable,piVars,
214                                          xVars,yVars,NIL(bdd_node *),inputProb,
215                                          nVars,nPi,roundOff,
216                                          solveMethod,startMethod);
217   
218    bdd_recursive_deref(ddManager,tranRelation);
219    bdd_recursive_deref(ddManager,reachable);
220   
221    for(i = 0; i < nVars; i++) {
222        bdd_recursive_deref(ddManager,xVars[i]);
223        bdd_recursive_deref(ddManager,yVars[i]);
224    }
225    for(i = 0 ; i < nPi; i++) {
226        bdd_recursive_deref(ddManager,piVars[i]);
227    }
228    FREE(xVars);
229    FREE(yVars);
230    FREE(piVars);
231       
232    return (result);
233}
234
235/**Function********************************************************************
236
237  Synopsis    [Computes the state probabilities of an FSM.]
238
239  Description [Computes the state probabilities of an FSM via Markovian
240  analysis. Returns a pointer to a pair ADDs if successful; The ADD in index
241  0 represents the steady state probabiliites and the ADD in index 1 represents
242  the one step transition probability matrix. NULL is returned in case of a
243  failure.
244
245  TR is the transition relation of the finite state machine. reachable is a
246  BDD of reachable states. piVars, xVars and yVars are the array of primary
247  inputs, present state variables and next state variables. It is optional to
248  specify a set of auxillary variables zVars for internal use. It could be NULL.
249  If specified the size of zVars equals nVars. inputProb is a
250  hash table (<name>,<probability>) for primary inputs. Probability here means
251  the probability of the primary input to be 1. nVars equal the number of
252  present state variables, nPi the number of primary inputs, roundOff implies
253  the number of digits after decimal to round off the calculations.
254
255  method is one of Solve_GenMethod_c, Solve_FPMethod_c, Solve_CKMethod_c
256  or Solve_Default_c. Currently only Solve_FPMethod_c is supported.
257  Solve_Default_c corresponds to Solve_FPMethod_c.
258
259  start is one of Start_Default_c, Start_Reset_c or Start_EquiProb_c.
260  The default method is Start_Reset_c.]
261
262  SideEffects [None]
263
264  SeeAlso     [Mark_ComputeStateProbs]
265
266******************************************************************************/
267bdd_node **
268Mark_ComputeStateProbsWithTr(
269  bdd_manager *ddManager,
270  bdd_node *TR,
271  bdd_node *reachable,
272  bdd_node **piVars,
273  bdd_node **xVars,
274  bdd_node **yVars,
275  bdd_node **zVars,
276  st_table *inputProb,
277  int nVars,
278  int nPi,
279  int roundOff,
280  Mark_SolveMethod method,
281  Mark_StartMethod start)
282{
283    CK *ck;
284    bdd_node **piAddVars, **xAddVars, **yAddVars, **zAddVars;
285    bdd_node *rep, *scc;
286    bdd_node **result;
287    st_generator *gen;
288    int i, index;
289    int createdPia, createdXa, createdYa, createdZa;
290    int createdZ;
291    int period;
292
293    /* To suppress Alpha warnings */
294    yAddVars = NIL(bdd_node *);
295    zAddVars = NIL(bdd_node *);
296
297    if (bdd_get_package_name() != CUDD) {
298        (void) fprintf(vis_stderr,"Synthesis package can be used only with CUDD package\n");
299        (void) fprintf(vis_stderr,"Please compile with CUDD package\n");
300        return 0;
301    }
302   
303    createdPia = createdXa = createdYa = createdZa = 0;
304    createdZ = 0;
305
306    piAddVars = ALLOC(bdd_node *, nPi);
307    if (piAddVars == NULL)
308        return NULL;
309    createdPia = 1;
310
311    xAddVars = ALLOC(bdd_node *, nVars);
312    if (xAddVars == NULL)
313        goto endgame;
314    createdXa = 1;
315
316    yAddVars = ALLOC(bdd_node *, nVars);
317    if (yAddVars == NULL)
318        goto endgame;
319    createdYa = 1;
320
321    zAddVars = ALLOC(bdd_node *, nVars);
322    if (zAddVars == NULL)
323        goto endgame;
324    createdZa = 1;
325 
326    if (zVars == NULL) {
327        zVars = ALLOC(bdd_node *, nVars);
328        if (zVars == NULL) 
329            goto endgame;
330        createdZ = 1;
331        for (i = 0; i < nVars; i++)
332            bdd_ref(zVars[i] = bdd_bdd_new_var(ddManager));
333    }
334
335    for(i = 0;i < nPi; i++) {
336        index = bdd_node_read_index(piVars[i]);
337        bdd_ref(piAddVars[i] = bdd_add_ith_var(ddManager,index));
338    }
339
340    for(i = 0; i < nVars; i++) {
341        index = bdd_node_read_index(xVars[i]);
342        bdd_ref(xAddVars[i] = bdd_add_ith_var(ddManager,index));
343        index = bdd_node_read_index(yVars[i]);
344        bdd_ref(yAddVars[i] = bdd_add_ith_var(ddManager,index));
345        index = bdd_node_read_index(zVars[i]);
346        bdd_ref(zAddVars[i] = bdd_add_ith_var(ddManager,index));
347    }
348
349    /* Allocate the structure for internal use */
350    ck = ALLOC(CK,1);
351 
352    ck->manager = ddManager;
353    ck->piVars = piVars;
354    ck->xVars = xVars;
355    ck->yVars = yVars;
356    ck->zVars = zVars;
357    ck->piAddVars = piAddVars;
358    ck->xAddVars = xAddVars;
359    ck->yAddVars = yAddVars;
360    ck->zAddVars = zAddVars;
361    ck->coeff = NULL; /* assigned in ckInterface - ADD */
362    ck->nVars = nVars;
363    ck->nPi = nPi;
364    ck->abstol = bdd_read_epsilon(ddManager);
365    ck->scale = 1.0;
366    ck->reltol = 1.0e-4;
367    ck->start = start;
368    ck->roundOff = roundOff;
369    ck->inputProb = inputProb;
370    ck->transition = TR;
371    ck->reached = reachable;
372    ck->indexSCC = NULL;       /* assigned in MarkGetSCC called by recTC */
373    ck->collapsedcoeff = NULL; /* assigned in ckInterface */
374    ck->term_SCC_states = 0;
375    ck->periods = NULL;        /* assigned in bddCollapseTSCC */
376    ck->term_scc = NULL;       /* assigned in ckInterface - ADD */
377    ck->init_guess = NULL;     /* assigned and derefed in all the methods.*/
378
379    ckInterface(ck);
380
381    /* select resolution method */
382    if (method == Solve_CKMethod_c) {
383        fprintf(stdout,"Mark<->Equations' Solver uses CK Method\n");
384        result = MarkAddCKSolve(ck); 
385    } 
386    else if (method == Solve_GenMethod_c) {
387        fprintf(stdout,"Mark<->Equations' Solver uses General Method\n");
388        result = MarkAddGenSolve(ck); 
389    }
390    else {
391        fprintf(stdout,"Mark<->Equations's Solver uses FP Method\n");
392        result = MarkAddFPSolve(ck);
393    }
394
395    /* Clean up */
396    bdd_recursive_deref(ddManager,ck->coeff);
397    st_foreach_item(ck->indexSCC,gen,&rep,&scc) {
398        bdd_recursive_deref(ddManager,rep);
399        bdd_recursive_deref(ddManager,scc);
400    }
401    st_free_table(ck->indexSCC);
402    bdd_recursive_deref(ddManager,ck->collapsedcoeff);
403    st_foreach_item_int(ck->periods,gen,&rep, &period) {
404        bdd_recursive_deref(ddManager,rep);
405    }
406    st_free_table(ck->periods);
407
408    bdd_recursive_deref(ddManager,ck->term_scc);
409
410    for(i = 0; i < nPi; i++) {
411        bdd_recursive_deref(ddManager,piAddVars[i]);
412    }
413
414    for(i = 0; i < nVars; i++) {
415        bdd_recursive_deref(ddManager,xAddVars[i]);
416        bdd_recursive_deref(ddManager,yAddVars[i]);
417        bdd_recursive_deref(ddManager,zAddVars[i]);
418    }
419
420    if (createdZ) {
421        for(i = 0; i < nVars; i++) {
422            bdd_recursive_deref(ddManager,zVars[i]);
423        }
424        FREE(zVars);
425    }
426    FREE(xAddVars);
427    FREE(yAddVars);
428    FREE(zAddVars);
429    FREE(piAddVars);
430    FREE(ck);
431
432    return result;
433
434endgame:
435    if (createdPia)
436        FREE(piAddVars);
437    if (createdXa)
438        FREE(xAddVars);
439    if (createdYa)
440        FREE(yAddVars);
441    if (createdZa)
442        FREE(zAddVars);
443    if (createdZ)
444        FREE(zVars);
445
446    return NULL;
447}
448
449
450/*---------------------------------------------------------------------------*/
451/* Definition of internal functions                                          */
452/*---------------------------------------------------------------------------*/
453
454/**Function********************************************************************
455
456  Synopsis    [Not implemented yet.]
457
458  Description [Not implemented yet.]
459
460  SideEffects [None]
461
462  SeeAlso []
463
464******************************************************************************/
465bdd_node **
466MarkAddCKSolve(
467  CK *ck)
468{
469    (void) fprintf(vis_stdout,"Not implemented yet. \n");
470    return NIL(bdd_node *);
471}
472
473
474/**Function********************************************************************
475
476  Synopsis    [Not implemented yet.]
477
478  Description [Not implemented yet.]
479
480  SideEffects [None]
481
482  SeeAlso []
483
484******************************************************************************/
485bdd_node **
486MarkAddGenSolve(
487  CK *ck)
488{
489    (void) fprintf(vis_stdout,"Not implemented yet. \n");
490    return NIL(bdd_node *);
491}
492
493
494/**Function********************************************************************
495
496  Synopsis    [Calculate the average bit change in the STG.]
497
498  Description [Calculate the average bit change in the STG. probTR is an ADD
499  representing the absolute transition probability matrix of the STG.
500  xVars and yVars are the present and next state variables respectively. nVars
501  is the number of state variables.
502
503  average bit change = (\exists^+_x(probTr * HD(x,y))).
504
505  The interested reader is referred to
506 
507  R. I. Bahar and E. A. Frohm and C. M. Gaona and G. D. Hachtel and E.
508  Macii and A. Pardo and F. Somenzi, "Algebraic Decision Diagrams and
509  their Applications", International Conference on Computer Aided
510  Design, 1993.
511 
512  on details pertaining to ADDs. ]
513
514  SideEffects [None]
515
516  SeeAlso []
517******************************************************************************/
518double 
519MarkAverageBitChange(
520  bdd_manager *manager,
521  bdd_node *probTR,
522  bdd_node **xVars,
523  bdd_node **yVars,
524  int nVars)
525{
526    bdd_node *diff, *cube, *PA, *QA;
527    bdd_node **vars;
528    double Mean;
529    int i;
530
531    vars = ALLOC(bdd_node *,2*nVars);
532    for (i = 0; i < nVars; i++) {
533        vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(xVars[i]));
534        bdd_ref(vars[i]);
535    }
536    for (i = nVars; i < 2*nVars; i++) {
537        vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(yVars[i-nVars]));
538        bdd_ref(vars[i]);
539    }
540
541    cube = bdd_add_compute_cube(manager,vars,NULL,2*nVars);
542    bdd_ref(cube);
543
544    /* Calculate the Hamming distance ADD. This ADD represents the hamming
545     * distance between two vectors represented by xVars and yVars.
546     */
547    bdd_ref(diff = bdd_add_hamming(manager,xVars,yVars,nVars));
548    bdd_ref(PA = bdd_add_apply(manager,bdd_add_times,probTR,diff));
549    bdd_recursive_deref(manager,diff);
550 
551    /* And now add and abstract all the variables.*/
552    bdd_ref(QA = bdd_add_exist_abstract(manager,PA,cube));
553    bdd_recursive_deref(manager,PA);
554    bdd_recursive_deref(manager,cube);
555    Mean = (double)bdd_add_value(QA);
556    bdd_recursive_deref(manager,QA); 
557
558    for (i = 0; i < 2*nVars; i++) {
559        bdd_recursive_deref(manager,vars[i]);
560    }
561    FREE(vars);
562    return Mean;
563}
564
565/*---------------------------------------------------------------------------*/
566/* Definition of static functions                                            */
567/*---------------------------------------------------------------------------*/
568
569/**Function********************************************************************
570
571  Synopsis           [Perform structural decomposition of the markov chain.]
572
573  Description        []
574
575  SideEffects        [The data structure ck is changed.]
576
577  SeeAlso            []
578
579******************************************************************************/
580static void
581ckInterface(
582  CK *ck)
583{
584    bdd_manager *ddManager;
585    bdd_node *piCube;
586    bdd_node *new_;
587    bdd_node *tmp1,*tmp2;
588    bdd_node *p, *t;
589    bdd_node *reachable, *TR;
590    bdd_node *q, *r;
591    st_table *newSCC;
592    st_table *newperiods;
593    st_generator *gen;
594    int len, nVars;
595
596    ddManager = ck->manager;
597    reachable = ck->reached;
598    TR = ck->transition;
599    nVars = ck->nVars;
600
601    bdd_ref(piCube = bdd_bdd_compute_cube(ddManager,ck->piVars,NULL,ck->nPi));
602    /* abstract the PI variables for the SCC computation */
603    bdd_ref(new_ = bdd_bdd_exist_abstract(ddManager,TR,piCube));
604    bdd_recursive_deref(ddManager,piCube);
605
606    /* now find the set of nodes in terminal SCC's */
607    p = recTC(ck,new_);
608    bdd_recursive_deref(ddManager,new_);
609
610    /* Collapse the TSCC in the graph */
611    ck->collapsedcoeff = bddCollapseTSCC(ck);
612    bdd_ref(ck->collapsedcoeff);
613
614    /* retain only reachable terminal SCC's */
615    bdd_ref(t = bdd_bdd_and(ddManager,p,reachable));
616    bdd_recursive_deref(ddManager,p);
617
618    /* count the number of states in the terminal SCC's */
619    ck->term_SCC_states = bdd_count_minterm(ddManager,t,nVars);
620    (void) fprintf(vis_stdout,"# of states in TSCCs = %f\n",
621                   ck->term_SCC_states);
622
623    /* Translate the data in ck->collapsedcoeff and
624     * ck->indexSCC from BDDs to ADDs.
625     */
626
627    newSCC = st_init_table(st_ptrcmp,st_ptrhash);
628    newperiods = st_init_table(st_ptrcmp,st_ptrhash);
629    st_foreach_item(ck->indexSCC,gen,&tmp1,&tmp2) {
630        bdd_ref(q = bdd_bdd_to_add(ddManager,tmp1));
631        bdd_ref(r = bdd_bdd_to_add(ddManager,tmp2));
632        st_lookup_int(ck->periods,(char *)tmp1, &len);
633        st_insert(newSCC,(char *)q,(char *)r);
634        st_insert(newperiods,(char *)q,(char *)(long)len);
635        bdd_recursive_deref(ddManager,tmp1);
636        bdd_recursive_deref(ddManager,tmp2);
637    }
638    st_free_table(ck->indexSCC);
639    st_free_table(ck->periods);
640    bdd_ref(q = bdd_bdd_to_add(ddManager,ck->collapsedcoeff));
641    bdd_recursive_deref(ddManager,ck->collapsedcoeff);
642    ck->collapsedcoeff = q;
643    ck->indexSCC = newSCC;
644    ck->periods = newperiods;
645
646    /* Print the number of TSCCs */
647    (void) fprintf(vis_stdout,"# of TSCCs = %d\n",st_count(newSCC));
648
649    /* convert the transition relation BDD into an ADD */
650    bdd_ref(q = bdd_bdd_to_add(ddManager,TR));
651    ck->coeff = q;
652
653    /* convert the term_scc set BDD into an ADD */
654    bdd_ref(q = bdd_bdd_to_add(ddManager,t));
655    ck->term_scc = q;
656    bdd_recursive_deref(ddManager,t);
657
658} /* End of ckInterface */
659
660/**Function********************************************************************
661
662  Synopsis           [Compute the strongly connected components.]
663
664  Description        []
665
666  SideEffects        [ck->indexSCC changed.]
667
668  SeeAlso            []
669
670******************************************************************************/
671static bdd_node * 
672recTC(
673  CK *ck,
674  bdd_node *tr)
675{
676
677    bdd_manager *manager = ck->manager;
678    bdd_node **xVars, **yVars, **zVars;
679    bdd_node *closure;
680    bdd_node *lastScc;
681    int nVars;
682
683    xVars = ck->xVars;
684    yVars = ck->yVars;
685    zVars = ck->zVars;
686    nVars = ck->nVars;
687
688    /* Matsunaga's procedure could also be used. Will have to implement it
689     * later.
690     */ 
691   
692    closure = transitiveClosureByIterSquaring(manager,tr,xVars,yVars,zVars, 
693                                              nVars);
694    bdd_ref(closure);
695    lastScc = MarkGetSCC(manager,tr,closure,ck->reached,
696                     xVars, yVars, nVars, &(ck->indexSCC));
697
698    bdd_recursive_deref(manager,closure);
699
700    return(lastScc);
701}
702
703
704/**Function********************************************************************
705
706  Synopsis           [Computes the transitive closure by iterative squaring.]
707
708  Description        []
709
710  SideEffects        [None]
711
712  SeeAlso            []
713
714******************************************************************************/
715static bdd_node *
716transitiveClosureByIterSquaring(
717  bdd_manager *ddManager,
718  bdd_node *TR,
719  bdd_node **xVars,
720  bdd_node **yVars,
721  bdd_node **zVars,
722  int nVars)
723{
724    bdd_node *prev, *next, *TRxz, *TRzy;
725    bdd_node *inter;
726    bdd_node *zCube;
727 
728    bdd_ref(zCube = bdd_bdd_compute_cube(ddManager,zVars,NULL,nVars));
729
730    bdd_ref(prev = TR);
731    while(1) {
732        TRxz = bdd_bdd_swap_variables(ddManager,prev,yVars,zVars,nVars);
733        bdd_ref(TRxz);
734        TRzy = bdd_bdd_swap_variables(ddManager,prev,xVars,zVars,nVars);
735        bdd_ref(TRzy);
736        inter = bdd_bdd_and_abstract(ddManager,TRxz,TRzy,zCube);
737        bdd_ref(inter);
738        bdd_recursive_deref(ddManager,TRxz);
739        bdd_recursive_deref(ddManager,TRzy);
740        next = bdd_bdd_or(ddManager,TR,inter);
741        bdd_ref(next);
742        bdd_recursive_deref(ddManager,inter);
743        if(prev == next)
744            break;
745        bdd_recursive_deref(ddManager,prev);
746        prev = next;
747    }
748    bdd_recursive_deref(ddManager,zCube);
749    bdd_recursive_deref(ddManager,prev);
750    bdd_deref(next);
751    return next;
752}
753
754/**Function********************************************************************
755
756  Synopsis           [Collapse the Terminal SCCs into a macro node.]
757
758  Description        []
759
760  SideEffects        [ck->periods is changed.]
761
762  SeeAlso            []
763
764******************************************************************************/
765static bdd_node *
766bddCollapseTSCC(
767  CK *ck)
768{
769    bdd_manager *manager = ck->manager;
770    bdd_node *tmp1,*tmp2;
771    bdd_node *repr,*scc,*restscc;
772    bdd_node *newtr;
773    bdd_node *xCube,*yCube;
774    bdd_node *sccfanout,*sccfanin;
775    st_generator *gen;
776    int i;
777
778    bdd_ref(xCube = bdd_bdd_compute_cube(manager,ck->xVars,NULL,ck->nVars));
779    bdd_ref(yCube = bdd_bdd_compute_cube(manager,ck->yVars,NULL,ck->nVars));
780
781    ck->periods = st_init_table(st_ptrcmp,st_ptrhash);
782 
783    bdd_ref(newtr = ck->transition);
784    i = 0;
785    st_foreach_item(ck->indexSCC,gen,&repr,&scc) {
786        /* Traverse the SCC to obtain the period */
787        st_insert(ck->periods,(char *)repr,(char *)(long)sccGetPeriod(ck,repr));
788     
789        /* Add edges from scc to the representatives in the fanout */
790        bdd_ref(sccfanout = bdd_bdd_and_abstract(manager,newtr,scc,xCube));
791     
792        bdd_ref(tmp1 = bdd_bdd_and(manager,scc,sccfanout));
793        bdd_recursive_deref(manager,sccfanout);
794        bdd_ref(tmp2 = bdd_bdd_or(manager,newtr,tmp1));
795        bdd_recursive_deref(manager,tmp1);
796        bdd_recursive_deref(manager,newtr);
797        newtr = tmp2;
798     
799        /* Add edges from fanin to representative */
800        bdd_ref(tmp2 = bdd_bdd_swap_variables(manager,scc,ck->xVars,ck->yVars,
801                                              ck->nVars));
802        bdd_ref(sccfanin = bdd_bdd_and_abstract(manager,newtr,tmp2,yCube));
803        bdd_recursive_deref(manager,tmp2);
804     
805        /* Add edges (fanin,representative) to the TR */
806        bdd_ref(tmp1 = bdd_bdd_swap_variables(manager,repr,ck->xVars,
807                                              ck->yVars,ck->nVars));
808        bdd_ref(tmp2 = bdd_bdd_and(manager,sccfanin,tmp1));
809        bdd_recursive_deref(manager,tmp1);
810        bdd_recursive_deref(manager,sccfanin);
811        bdd_ref(tmp1 = bdd_bdd_or(manager,newtr,tmp2));
812        bdd_recursive_deref(manager,tmp2);
813        bdd_recursive_deref(manager,newtr);
814        newtr = tmp1;
815     
816        /*Delete the edges that go to the non-representative nodes */
817        bdd_ref(restscc = bdd_bdd_and(manager,scc,bdd_not_bdd_node(repr)));
818     
819        bdd_ref(tmp1 = bdd_bdd_and(manager,newtr,bdd_not_bdd_node(restscc)));
820        bdd_ref(tmp2 = bdd_bdd_swap_variables(manager,restscc,ck->xVars,
821                                            ck->yVars,ck->nVars));
822        bdd_recursive_deref(manager,restscc);
823        bdd_recursive_deref(manager,newtr);
824        bdd_ref(newtr = bdd_bdd_and(manager,tmp1,bdd_not_bdd_node(tmp2)));
825        bdd_recursive_deref(manager,tmp1);
826        bdd_recursive_deref(manager,tmp2);
827     
828        i++;
829    }
830 
831    bdd_recursive_deref(manager,xCube);
832    bdd_recursive_deref(manager,yCube);
833 
834    bdd_deref(newtr);
835    return(newtr);
836}
837
838/**Function********************************************************************
839
840  Synopsis           [Compute the period of the SCC.]
841
842  Description        []
843
844  SideEffects        [None]
845
846  SeeAlso            []
847
848******************************************************************************/
849static int
850sccGetPeriod(
851  CK *ck,
852  bdd_node *reset)
853{
854
855    bdd_manager *manager = ck->manager;
856    bdd_node *new_,*from;
857    bdd_node *tmp1;
858    bdd_node *xCube, *inputCube;
859    bdd_node *transition;
860    int pos,result = 0;
861    int depth;
862    int stop = 0; 
863    st_table *tos;
864    st_generator *gen;
865 
866    /* Calculate the cube for abstraction */
867
868    bdd_ref(xCube = bdd_bdd_compute_cube(manager,ck->xVars,NULL,ck->nVars));
869    bdd_ref(inputCube = bdd_bdd_compute_cube(manager,ck->piVars,NULL,ck->nPi));
870    bdd_ref(transition = bdd_bdd_exist_abstract(manager,ck->transition,
871                                                inputCube));
872    bdd_recursive_deref(manager,inputCube);
873 
874    depth = 0;
875    bdd_ref(from = reset);
876    bdd_ref(tmp1 = reset);
877    tos = st_init_table(st_ptrcmp,st_ptrhash);
878    depth++;
879    st_insert(tos,(char *)tmp1,(char *)(long)depth);
880
881    while(!stop) {
882        bdd_ref(tmp1 = bdd_bdd_and_abstract(manager,from,transition,xCube));
883        bdd_ref(new_ = bdd_bdd_swap_variables(manager,tmp1,ck->yVars,ck->xVars,
884                                             ck->nVars));
885        bdd_recursive_deref(manager,tmp1);
886     
887        if((stop = st_lookup_int(tos,(char *)new_, &pos)))
888            result = depth - pos;
889        else
890            st_insert(tos,(char *)new_,(char *)(long)depth);
891       
892        bdd_recursive_deref(manager,from);
893        bdd_ref(from = new_);
894        depth++;
895    }
896
897    bdd_recursive_deref(manager,new_);
898    bdd_recursive_deref(manager,xCube);
899    bdd_recursive_deref(manager,from);
900
901    st_foreach_item_int(tos,gen,&new_, &pos) {
902        bdd_recursive_deref(manager,new_);
903    }
904    st_free_table(tos);
905
906    return result;
907}
908
909
910/**Function********************************************************************
911
912  Synopsis [Returns a BDD array from an Mvf array]
913
914  SideEffects [None]
915
916  SeeAlso     []
917
918******************************************************************************/
919static array_t *
920markGetBddArray(array_t *mvfArray)
921{
922    int           i,phase;
923    array_t *bddArray;
924    Mvf_Function_t *mvf;
925
926    bddArray = array_alloc(bdd_node *,0);
927
928    arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
929        mdd_t     *mddTemp;
930        bdd_node    *ddNode;
931
932        mddTemp = array_fetch(mdd_t *, mvf, 1);
933        ddNode = (bdd_node *) bdd_get_node(mddTemp,&phase);
934        bdd_ref(ddNode);
935
936        ddNode = phase ? bdd_not_bdd_node(ddNode) : ddNode;
937        array_insert_last(bdd_node *, bddArray, ddNode);
938    }
939    return bddArray;
940}
941
942/**Function********************************************************************
943
944  Synopsis [Returns a BDD array given an integer array of variable indices.]
945
946  SideEffects [None]
947
948  SeeAlso     []
949
950******************************************************************************/
951static bdd_node **
952BddNodeArrayFromIdArray(
953  bdd_manager   *ddManager,
954  array_t       *idArray)
955{
956    bdd_node **xvars;
957    int i,id;
958    int nvars = array_n(idArray);
959
960    xvars = ALLOC(bdd_node *, nvars);
961    if (xvars == NULL)
962        return NULL;
963
964    for(i = 0; i < nvars; i++) {
965        id = array_fetch(int,idArray,i);
966        xvars[i] = bdd_bdd_ith_var(ddManager,id);
967        bdd_ref(xvars[i]);
968    }
969    return xvars;
970}
971
972/**Function********************************************************************
973
974  Synopsis [Compute the relation between an array of function and a
975  corresponding array of variables. A BDD is returned which represents
976  AND(i=0 -> i<nVars)(yVars[i]==nextBdds). ]
977
978  SideEffects []
979
980  SeeAlso     []
981
982******************************************************************************/
983static bdd_node *
984computeTransitionRelationWithIds(
985  bdd_manager   *ddManager,
986  array_t       *nextBdds,
987  bdd_node      **yVars,
988  int           nVars)
989{
990    bdd_node    *ddtemp1, *ddtemp2;
991    bdd_node    *oldTR, *fn;
992    int                  i;
993
994
995    oldTR = bdd_read_one(ddManager);
996
997    for(i = 0; i < nVars; i++) {
998        ddtemp2  = array_fetch(bdd_node *, nextBdds, i);
999
1000        fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
1001        bdd_ref(fn);
1002        ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
1003        bdd_ref(ddtemp1);
1004        bdd_recursive_deref(ddManager,fn);
1005        bdd_recursive_deref(ddManager,oldTR);
1006        oldTR = ddtemp1;
1007    }
1008
1009    return oldTR;
1010}
1011
Note: See TracBrowser for help on using the repository browser.