add isl_union_map_apply_union_pw_qpolynomial
[barvinok.git] / parker / count_paths.c
blob1bf1ecc30053c403054c2cb6de1358f17cbc1bea
1 /* Erin Parker (parker@cs.unc.edu), March 2004 */
3 #include <stdlib.h>
4 #include "dfa.h"
7 double count_accepting_paths(DFA *dfa, int num_states, int num_freevars)
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 */
19 paths pp[num_states];
20 trace_descr tp;
22 int i, j, k;
25 for (i = 0; i < num_states; i++) {
26 pp[i] = make_paths(dfa->bddm, dfa->q[i]);
28 num_edges_from[i] = 0;
29 N1[i] = N2[i] = 0;
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;
37 for (i = 0; i < num_states; i++) {
39 if(dead_state[i])
40 continue;
42 /* Do while there are remaining edges from state i . . . */
43 while (pp[i]) {
44 int found = 0;
46 for (j = 0; j < num_edges_from[i]; j++)
47 if (edge_from[i][j] == pp[i]->to) {
48 found = 1;
49 break;
51 if (!found) {
52 num_edges_from[i]++;
53 weight[i][j] = 0;
54 edge_from[i][j] = pp[i]->to;
57 /* Check if edge (i,pp[i]->to) leads to a dead state, continue if not */
58 if (!dead_state[pp[i]->to]) {
60 int count = 1;
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++) {;}
65 /* Then, the label for each remaining track must be 'X',
66 update count appropriately */
67 for (; k < num_freevars; k++)
68 count *= 2;
70 /* Update weight on edge (i,pp[i]->to) */
71 weight[i][j] += count;
74 /* Get next edge from state i and repeat */
75 pp[i] = pp[i]->next;
79 for (i = 0; i < num_states; i++)
80 kill_paths(pp[i]);
83 /* Recurrence operation on array N */
84 N1[0] = N2[0] = 1; /* base case: N = {1 0 0 0 0 ... 0 0 } */
86 while(1) {
87 double temp[num_states];
88 int same = 1;
90 /* N_i = N_{i-1} * W */
91 for (j = 0; j < num_states; j++)
92 temp[j] = 0;
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];
103 if(do_N1) {
104 for (j = 0; j < num_states; j++)
105 N2[j] = temp[j];
106 do_N1 = 0;
108 else {
109 for (j = 0; j < num_states; j++)
110 N1[j] = temp[j];
111 do_N1 = 1;
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;
118 if(same == 1)
119 break;
121 L++;
124 for(j = 0; j < num_states; j++)
125 if (dfa->f[j] == 1)
126 num_paths += N1[j];
128 return num_paths;