![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to pret0.c CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [Research Unix] / researchv10dc / cmd / pret|
Return to pret0.c CVS log | Up to [Research Unix] / researchv10dc / cmd / pret |
1.1 root 1: #include <stdio.h>
2: #include "pret.h"
3: #include "pret.d"
4:
5: #define DEBUG6 0
6: #define DEBUG7 0
7:
8: extern struct COL column[MANY];
9: extern struct ROW row[MANY];
10: extern int nrrows, nrcols, redrows;
11:
12: struct ENTRY * find();
13: char * Emalloc();
14:
15: char **triangle;
16: short **successor;
17: short *tmpsucc;
18: int *unmap; /* reverses maptwo values to original row numbers */
19:
20: MAP(x)
21: { int y = row[x].maptwo; /* gives a value between 0 and redrows */
22:
23: unmap[y] = x;
24: return y;
25: }
26:
27: minimize()
28: { int i, j;
29: int n = redrows;
30:
31: unmap = (int *)
32: Emalloc( n * sizeof (int) );
33: triangle = (char **)
34: Emalloc( n * sizeof (char *) );
35: /*
36: ** allocate a triangle of states
37: ** triangle[i][j] == 1
38: ** will indicate that the states i and j are
39: ** in the same equivalence class
40: ** initially, claim all pairs to be equivalent
41: */
42:
43: for (i = 1; i < n; i++)
44: { triangle[i] = (char *)
45: Emalloc(i * sizeof (char));
46: for (j = 0; j < i; j++)
47: triangle[i][j] = 1;
48: }
49: tmpsucc = (short *)
50: Emalloc( n * sizeof (short));
51: successor = (short **)
52: Emalloc( n * sizeof (short *) );
53:
54: for (i = 0; i < n; i++)
55: { successor[i] = (short *)
56: Emalloc(n * sizeof (short));
57: for (j = 0; j < n; j++)
58: successor[i][j] = 0;
59: }
60: partition();
61:
62: #if DEBUG6
63: putriangle();
64: #endif
65: squash();
66:
67: for (i = 1; i < n; i++)
68: free(triangle[i]);
69: free(triangle);
70: free(unmap);
71: }
72:
73: /*
74: newgeneration()
75: { register int i,j;
76:
77: for (j = 0; j < n; i++)
78: tmpsucc[j] = 0;
79: for (i = 0; i < n; i++)
80: { for (j = 0; j < n; j++)
81: addkids(successor[i][j]);
82: for (j = 0; j < n; j++)
83: { successor[i][j] = tmpsucc[j];
84: tmpsucc[i] = 0;
85: }
86: }
87: }
88:
89: addkids(whosekids)
90: { register int h,k,x,y;
91: struct ENTRY *one = find(i, 0);
92: struct ENTRY *two = find(j, 0);
93: struct PILAR *a;
94:
95:
96: for (k = 0; k < nrcols; k++)
97: { for (h = 0; h < one->nrpils; h++)
98: { a = one->pilar;
99:
100: tmpsucc[target(a->transf)] = 1;
101:
102: a = a->nxtp;
103: }
104: one = one->nextcol;
105: two = two->nextcol;
106: }
107: }
108: */
109:
110: partition()
111: { register int i, j, K;
112: int anychange = 1;
113:
114: /*
115: ** recursively scan through the
116: ** triangle to find non-equivalent pairs
117: ** until pi(1) -> pi(k) == pi(k-1)
118: */
119:
120: for (K = 1; anychange == 1; K++)
121: { anychange = 0;
122: #if DEBUG7
123: printf("%d Equivalence:\n", K);
124: #endif DEBUG7
125: for (i = nrrows-1; i > 0; i--)
126: { if (row[i].mapping != NOSTATE)
127: continue;
128:
129: for (j = 0; j < i; j++)
130: { if (row[j].mapping != NOSTATE
131: || triangle[MAP(i)][MAP(j)] == 0)
132: continue;
133:
134: if ( !equiv(K, i, j) )
135: { triangle[MAP(i)][MAP(j)] = 0;
136: anychange = 1;
137: }
138: #if DEBUG7
139: else
140: { printf("\tstates: %2d,", MAP(i));
141: printf("%2d\n", MAP(j));
142: }
143: #endif DEBUG7
144: } } } }
145:
146: #if DEBUG6
147: putriangle()
148: { int i, j;
149: int n = redrows;
150: int cn = 0;
151: char * class = (char *) Emalloc (n * sizeof (char) );
152:
153: for (i = 0; i < n; i++)
154: class[i] = 0;
155:
156: for (i = 1; i < n; i++)
157: for (j = 0; j < i; j++)
158: if ( triangle[i][j] )
159: { if (class[i] == 0 && class[j] == 0)
160: class[i] = class[j] = ++cn;
161: else if (class[i] != 0)
162: class[j] = class[i];
163: else if (class[j] != 0)
164: class[i] = class[j];
165: else
166: whoops("cannot happen, classes");
167: }
168:
169: for (i = 1; i <= cn; i++)
170: { printf("class %2d: ", i);
171: for (j = 0; j < n; j++)
172: if (class[j] == i)
173: printf("%d,", j);
174: printf("\n\n");
175: }
176:
177: free(class);
178: }
179: #endif
180:
181: squash()
182: { int i, j;
183: int n = redrows;
184: for (i = 1; i < n; i++)
185: for (j = 0; j < i; j++)
186: if ( triangle[i][j] )
187: { row[unmap[i]].mapping = unmap[j];
188: row[unmap[j]].labeled |= row[unmap[i]].labeled;
189: }
190: }
191:
192: outequiv(A, B)
193: struct ENTRY *A, *B;
194: { struct PILAR *at = A->pilar;
195: struct PILAR *it = B->pilar;
196:
197: /*
198: ** don't look at the at->transf's,
199: ** equal columns implicitly give
200: ** equal inputs or outputs, so
201: ** just compare the cargo codes
202: */
203:
204: while (it != NULL && at != NULL)
205: { if (at->code != it->code)
206: break;
207:
208: at = at->nxtp;
209: it = it->nxtp;
210: }
211:
212: return (it == NULL && at == NULL);
213: }
214:
215: equiv(K, i, j)
216: { int h, k, x, y, z;
217: struct ENTRY *one = find(i, 0);
218: struct ENTRY *two = find(j, 0);
219: struct PILAR *a, *b;
220:
221: if (one->nrpils != two->nrpils)
222: return 0;
223:
224: if (K == 1)
225: { for (k = 0; k < nrcols; k++)
226: { if ( !outequiv(one, two) )
227: return 0;
228:
229: one = one->nextcol;
230: two = two->nextcol;
231: }
232: } else
233: for (k = 0; k < nrcols; k++)
234: { a = one->pilar;
235: b = two->pilar;
236: for (h = 0; h < one->nrpils; h++)
237: {
238: x = target(a->transf);
239: y = target(b->transf);
240: x = MAP(x); y = MAP(y);
241: if (y > x) { z=x; x=y; y=z; }
242: if (x != y && triangle[x][y] == 0)
243: return 0;
244:
245: a = a->nxtp;
246: b = b->nxtp;
247: }
248: one = one->nextcol;
249: two = two->nextcol;
250: }
251:
252: return 1;
253: }
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.