parker/count_paths.c

   1 /* Erin Parker (parker@cs.unc.edu), March 2004 */
   2
   3 #include <stdlib.h>
   4 #include "dfa.h"
   5
   6
   7 double count_accepting_paths(DFA *dfa, int num_states, int num_freevars)
   8 {
   9   int dead_state[num_states];           /* list of dead states */
  10   int num_edges_from[num_states];       /* number of (live) edges from state i */
  11   int edge_from[num_states][num_states];/* state on edge from state i */
  12   double weight[num_states][num_states];/* weight on edge from state i */
  13   double N1[num_states];                /* number of paths to state i */
  14   double N2[num_states];
  15   int do_N1 = 1;
  16   double num_paths = 0;
  17   int L = 0;                            /* length of longest path considered */
  18
  19   paths pp[num_states];
  20   trace_descr tp;
  21
  22   int i, j, k;
  23
  24
  25   for (i = 0; i < num_states; i++) {
  26     pp[i] = make_paths(dfa->bddm, dfa->q[i]);
  27
  28     num_edges_from[i] = 0;
  29     N1[i] = N2[i] = 0;
  30
  31     if (dfa->f[i]==-1 && pp[i]->next==NULL && pp[i]->to==i)
  32       dead_state[i] = 1;
  33     else
  34       dead_state[i] = 0;
  35   }
  36
  37   for (i = 0; i < num_states; i++) {
  38
  39     if(dead_state[i])
  40       continue;
  41
  42     /* Do while there are remaining edges from state i . . . */
  43     while (pp[i]) {
  44       int found = 0;
  45
  46       for (j = 0; j < num_edges_from[i]; j++)
  47         if (edge_from[i][j] == pp[i]->to) {
  48           found = 1;
  49           break;
  50         }
  51       if (!found) {
  52         num_edges_from[i]++;
  53         weight[i][j] = 0;
  54         edge_from[i][j] = pp[i]->to;
  55       }
  56
  57       /* Check if edge (i,pp[i]->to) leads to a dead state, continue if not */
  58       if (!dead_state[pp[i]->to]) {
  59
  60         int count = 1;
  61
  62         /* First, go through each track whose label is '0' or '1' */
  63         for (tp = pp[i]->trace, k=0; tp; tp = tp->next, k++) {;}
  64
  65         /* Then, the label for each remaining track must be 'X',
  66            update count appropriately */
  67         for (; k < num_freevars; k++)
  68           count *= 2;
  69
  70         /* Update weight on edge (i,pp[i]->to) */
  71         weight[i][j] += count;
  72       }
  73
  74       /* Get next edge from state i and repeat */
  75       pp[i] = pp[i]->next;
  76     }
  77   }
  78
  79   for (i = 0; i < num_states; i++)
  80     kill_paths(pp[i]);
  81
  82
  83   /* Recurrence operation on array N */
  84   N1[0] = N2[0] = 1;  /* base case: N = {1 0 0 0 0 ... 0 0 } */
  85
  86   while(1) {
  87     double temp[num_states];
  88     int same = 1;
  89
  90     /* N_i = N_{i-1} * W */
  91     for (j = 0; j < num_states; j++)
  92       temp[j] = 0;
  93
  94     if(do_N1)
  95       for (k = 0; k < num_states; k++)
  96         for (j = 0; j < num_edges_from[k]; j++)
  97           temp[edge_from[k][j]] += N1[k] * weight[k][j];
  98     else
  99       for (k = 0; k < num_states; k++)
 100         for (j = 0; j < num_edges_from[k]; j++)
 101           temp[edge_from[k][j]] += N2[k] * weight[k][j];
 102
 103     if(do_N1) {
 104       for (j = 0; j < num_states; j++)
 105         N2[j] = temp[j];
 106       do_N1 = 0;
 107     }
 108     else {
 109       for (j = 0; j < num_states; j++)
 110         N1[j] = temp[j];
 111       do_N1 = 1;
 112     }
 113
 114     for (j = 0; j < num_states && same==1; j++)
 115       if((N1[j]==0 && N2[j]>0) || (N1[j]>0 && N2[j]==0))
 116         same = 0;
 117
 118     if(same == 1)
 119       break;
 120
 121     L++;
 122   }
 123
 124   for(j = 0; j < num_states; j++)
 125     if (dfa->f[j] == 1)
 126       num_paths += N1[j];
 127
 128   return num_paths;
 129 }
 130