0b55f123 |
1 | /***** spin: pangen5.h *****/ |
2 | |
3 | /* Copyright (c) 1997-2003 by Lucent Technologies, Bell Laboratories. */ |
4 | /* All Rights Reserved. This software is for educational purposes only. */ |
5 | /* No guarantee whatsoever is expressed or implied by the distribution of */ |
6 | /* this code. Permission is given to distribute this code provided that */ |
7 | /* this introductory message is not removed and no monies are exchanged. */ |
8 | /* Software written by Gerard J. Holzmann. For tool documentation see: */ |
9 | /* http://spinroot.com/ */ |
10 | /* Send all bug-reports and/or questions to: bugs@spinroot.com */ |
11 | |
12 | static char *Xpt[] = { |
13 | "#if defined(MA) && (defined(W_XPT) || defined(R_XPT))", |
14 | "static Vertex **temptree;", |
15 | "static char wbuf[4096];", |
16 | "static int WCNT = 4096, wcnt=0;", |
17 | "static uchar stacker[MA+1];", |
18 | "static ulong stackcnt = 0;", |
19 | "extern double nstates, nlinks, truncs, truncs2;", |
20 | "", |
21 | "static void", |
22 | "xwrite(int fd, char *b, int n)", |
23 | "{", |
24 | " if (wcnt+n >= 4096)", |
25 | " { write(fd, wbuf, wcnt);", |
26 | " wcnt = 0;", |
27 | " }", |
28 | " memcpy(&wbuf[wcnt], b, n);", |
29 | " wcnt += n;", |
30 | "}", |
31 | "", |
32 | "static void", |
33 | "wclose(fd)", |
34 | "{", |
35 | " if (wcnt > 0)", |
36 | " write(fd, wbuf, wcnt);", |
37 | " wcnt = 0;", |
38 | " close(fd);", |
39 | "}", |
40 | "", |
41 | "static void", |
42 | "w_vertex(int fd, Vertex *v)", |
43 | "{ char t[3]; int i; Edge *e;", |
44 | "", |
45 | " xwrite(fd, (char *) &v, sizeof(Vertex *));", |
46 | " t[0] = 0;", |
47 | " for (i = 0; i < 2; i++)", |
48 | " if (v->dst[i])", |
49 | " { t[1] = v->from[i], t[2] = v->to[i];", |
50 | " xwrite(fd, t, 3);", |
51 | " xwrite(fd, (char *) &(v->dst[i]), sizeof(Vertex *));", |
52 | " }", |
53 | " for (e = v->Succ; e; e = e->Nxt)", |
54 | " { t[1] = e->From, t[2] = e->To;", |
55 | " xwrite(fd, t, 3);", |
56 | " xwrite(fd, (char *) &(e->Dst), sizeof(Vertex *));", |
57 | "", |
58 | " if (e->s)", |
59 | " { t[1] = t[2] = e->S;", |
60 | " xwrite(fd, t, 3);", |
61 | " xwrite(fd, (char *) &(e->Dst), sizeof(Vertex *));", |
62 | " } }", |
63 | "}", |
64 | "", |
65 | "static void", |
66 | "w_layer(int fd, Vertex *v)", |
67 | "{ uchar c=1;", |
68 | "", |
69 | " if (!v) return;", |
70 | " xwrite(fd, (char *) &c, 1);", |
71 | " w_vertex(fd, v);", |
72 | " w_layer(fd, v->lnk);", |
73 | " w_layer(fd, v->left);", |
74 | " w_layer(fd, v->right);", |
75 | "}", |
76 | "", |
77 | "void", |
78 | "w_xpoint(void)", |
79 | "{ int fd; char nm[64];", |
80 | " int i, j; uchar c;", |
81 | " static uchar xwarned = 0;", |
82 | "", |
83 | " sprintf(nm, \"%%s.xpt\", PanSource);", |
84 | " if ((fd = creat(nm, 0666)) <= 0)", |
85 | " if (!xwarned)", |
86 | " { xwarned = 1;", |
87 | " printf(\"cannot creat checkpoint file\\n\");", |
88 | " return;", |
89 | " }", |
90 | " xwrite(fd, (char *) &nstates, sizeof(double));", |
91 | " xwrite(fd, (char *) &truncs, sizeof(double));", |
92 | " xwrite(fd, (char *) &truncs2, sizeof(double));", |
93 | " xwrite(fd, (char *) &nlinks, sizeof(double));", |
94 | " xwrite(fd, (char *) &dfa_depth, sizeof(int));", |
95 | " xwrite(fd, (char *) &R, sizeof(Vertex *));", |
96 | " xwrite(fd, (char *) &F, sizeof(Vertex *));", |
97 | " xwrite(fd, (char *) &NF, sizeof(Vertex *));", |
98 | "", |
99 | " for (j = 0; j < TWIDTH; j++)", |
100 | " for (i = 0; i < dfa_depth+1; i++)", |
101 | " { w_layer(fd, layers[i*TWIDTH+j]);", |
102 | " c = 2; xwrite(fd, (char *) &c, 1);", |
103 | " }", |
104 | " wclose(fd);", |
105 | "}", |
106 | "", |
107 | "static void", |
108 | "xread(int fd, char *b, int n)", |
109 | "{ int m = wcnt; int delta = 0;", |
110 | " if (m < n)", |
111 | " { if (m > 0) memcpy(b, &wbuf[WCNT-m], m);", |
112 | " delta = m;", |
113 | " WCNT = wcnt = read(fd, wbuf, 4096);", |
114 | " if (wcnt < n-m)", |
115 | " Uerror(\"xread failed -- insufficient data\");", |
116 | " n -= m;", |
117 | " }", |
118 | " memcpy(&b[delta], &wbuf[WCNT-wcnt], n);", |
119 | " wcnt -= n;", |
120 | "}", |
121 | "", |
122 | "static void", |
123 | "x_cleanup(Vertex *c)", |
124 | "{ Edge *e; /* remove the tree and edges from c */", |
125 | " if (!c) return;", |
126 | " for (e = c->Succ; e; e = e->Nxt)", |
127 | " x_cleanup(e->Dst);", |
128 | " recyc_vertex(c);", |
129 | "}", |
130 | "", |
131 | "static void", |
132 | "x_remove(void)", |
133 | "{ Vertex *tmp; int i, s;", |
134 | " int r, j;", |
135 | " /* double-check: */", |
136 | " stacker[dfa_depth-1] = 0; r = dfa_store(stacker);", |
137 | " stacker[dfa_depth-1] = 4; j = dfa_member(dfa_depth-1);", |
138 | " if (r != 1 || j != 0)", |
139 | " { printf(\"%%d: \", stackcnt);", |
140 | " for (i = 0; i < dfa_depth; i++)", |
141 | " printf(\"%%d,\", stacker[i]);", |
142 | " printf(\" -- not a stackstate <o:%%d,4:%%d>\\n\", r, j);", |
143 | " return;", |
144 | " }", |
145 | " stacker[dfa_depth-1] = 1;", |
146 | " s = dfa_member(dfa_depth-1);", |
147 | "", |
148 | " { tmp = F; F = NF; NF = tmp; } /* complement */", |
149 | " if (s) dfa_store(stacker);", |
150 | " stacker[dfa_depth-1] = 0;", |
151 | " dfa_store(stacker);", |
152 | " stackcnt++;", |
153 | " { tmp = F; F = NF; NF = tmp; }", |
154 | "}", |
155 | "", |
156 | "static void", |
157 | "x_rm_stack(Vertex *t, int k)", |
158 | "{ int j; Edge *e;", |
159 | "", |
160 | " if (k == 0)", |
161 | " { x_remove();", |
162 | " return;", |
163 | " }", |
164 | " if (t)", |
165 | " for (e = t->Succ; e; e = e->Nxt)", |
166 | " { for (j = e->From; j <= (int) e->To; j++)", |
167 | " { stacker[k] = (uchar) j;", |
168 | " x_rm_stack(e->Dst, k-1);", |
169 | " }", |
170 | " if (e->s)", |
171 | " { stacker[k] = e->S;", |
172 | " x_rm_stack(e->Dst, k-1);", |
173 | " } }", |
174 | "}", |
175 | "", |
176 | "static Vertex *", |
177 | "insert_withkey(Vertex *v, int L)", |
178 | "{ Vertex *new, *t = temptree[L];", |
179 | "", |
180 | " if (!t) { temptree[L] = v; return v; }", |
181 | " t = splay(v->key, t);", |
182 | " if (v->key < t->key)", |
183 | " { new = v;", |
184 | " new->left = t->left;", |
185 | " new->right = t;", |
186 | " t->left = (Vertex *) 0;", |
187 | " } else if (v->key > t->key)", |
188 | " { new = v;", |
189 | " new->right = t->right;", |
190 | " new->left = t;", |
191 | " t->right = (Vertex *) 0;", |
192 | " } else", |
193 | " { if (t != R && t != F && t != NF)", |
194 | " Uerror(\"double insert, bad checkpoint data\");", |
195 | " else", |
196 | " { recyc_vertex(v);", |
197 | " new = t;", |
198 | " } }", |
199 | " temptree[L] = new;", |
200 | "", |
201 | " return new;", |
202 | "}", |
203 | "", |
204 | "static Vertex *", |
205 | "find_withkey(Vertex *v, int L)", |
206 | "{ Vertex *t = temptree[L];", |
207 | " if (t)", |
208 | " { temptree[L] = t = splay((ulong) v, t);", |
209 | " if (t->key == (ulong) v)", |
210 | " return t;", |
211 | " }", |
212 | " Uerror(\"not found error, bad checkpoint data\");", |
213 | " return (Vertex *) 0;", |
214 | "}", |
215 | "", |
216 | "void", |
217 | "r_layer(int fd, int n)", |
218 | "{ Vertex *v;", |
219 | " Edge *e;", |
220 | " char c, t[2];", |
221 | "", |
222 | " for (;;)", |
223 | " { xread(fd, &c, 1);", |
224 | " if (c == 2) break;", |
225 | " if (c == 1)", |
226 | " { v = new_vertex();", |
227 | " xread(fd, (char *) &(v->key), sizeof(Vertex *));", |
228 | " v = insert_withkey(v, n);", |
229 | " } else /* c == 0 */", |
230 | " { e = new_edge((Vertex *) 0);", |
231 | " xread(fd, t, 2);", |
232 | " e->From = t[0];", |
233 | " e->To = t[1];", |
234 | " xread(fd, (char *) &(e->Dst), sizeof(Vertex *));", |
235 | " insert_edge(v, e);", |
236 | " } }", |
237 | "}", |
238 | "", |
239 | "static void", |
240 | "v_fix(Vertex *t, int nr)", |
241 | "{ int i; Edge *e;", |
242 | "", |
243 | " if (!t) return;", |
244 | "", |
245 | " for (i = 0; i < 2; i++)", |
246 | " if (t->dst[i])", |
247 | " t->dst[i] = find_withkey(t->dst[i], nr);", |
248 | "", |
249 | " for (e = t->Succ; e; e = e->Nxt)", |
250 | " e->Dst = find_withkey(e->Dst, nr);", |
251 | " ", |
252 | " v_fix(t->left, nr);", |
253 | " v_fix(t->right, nr);", |
254 | "}", |
255 | "", |
256 | "static void", |
257 | "v_insert(Vertex *t, int nr)", |
258 | "{ Edge *e; int i;", |
259 | "", |
260 | " if (!t) return;", |
261 | " v_insert(t->left, nr);", |
262 | " v_insert(t->right, nr);", |
263 | "", |
264 | " /* remove only leafs from temptree */", |
265 | " t->left = t->right = t->lnk = (Vertex *) 0;", |
266 | " insert_it(t, nr); /* into layers */", |
267 | " for (i = 0; i < 2; i++)", |
268 | " if (t->dst[i])", |
269 | " t->dst[i]->num += (t->to[i] - t->from[i] + 1);", |
270 | " for (e = t->Succ; e; e = e->Nxt)", |
271 | " e->Dst->num += (e->To - e->From + 1 + e->s);", |
272 | "}", |
273 | "", |
274 | "static void", |
275 | "x_fixup(void)", |
276 | "{ int i;", |
277 | "", |
278 | " for (i = 0; i < dfa_depth; i++)", |
279 | " v_fix(temptree[i], (i+1));", |
280 | "", |
281 | " for (i = dfa_depth; i >= 0; i--)", |
282 | " v_insert(temptree[i], i);", |
283 | "}", |
284 | "", |
285 | "static Vertex *", |
286 | "x_tail(Vertex *t, ulong want)", |
287 | "{ int i, yes, no; Edge *e; Vertex *v = (Vertex *) 0;", |
288 | "", |
289 | " if (!t) return v;", |
290 | "", |
291 | " yes = no = 0;", |
292 | " for (i = 0; i < 2; i++)", |
293 | " if ((ulong) t->dst[i] == want)", |
294 | " { /* was t->from[i] <= 0 && t->to[i] >= 0 */", |
295 | " /* but from and to are uchar */", |
296 | " if (t->from[i] == 0)", |
297 | " yes = 1;", |
298 | " else", |
299 | " if (t->from[i] <= 4 && t->to[i] >= 4)", |
300 | " no = 1;", |
301 | " }", |
302 | "", |
303 | " for (e = t->Succ; e; e = e->Nxt)", |
304 | " if ((ulong) e->Dst == want)", |
305 | " { /* was INRANGE(e,0) but From and To are uchar */", |
306 | " if ((e->From == 0) || (e->s==1 && e->S==0))", |
307 | " yes = 1;", |
308 | " else if (INRANGE(e, 4))", |
309 | " no = 1;", |
310 | " }", |
311 | " if (yes && !no) return t;", |
312 | " v = x_tail(t->left, want); if (v) return v;", |
313 | " v = x_tail(t->right, want); if (v) return v;", |
314 | " return (Vertex *) 0;", |
315 | "}", |
316 | "", |
317 | "static void", |
318 | "x_anytail(Vertex *t, Vertex *c, int nr)", |
319 | "{ int i; Edge *e, *f; Vertex *v;", |
320 | "", |
321 | " if (!t) return;", |
322 | "", |
323 | " for (i = 0; i < 2; i++)", |
324 | " if ((ulong) t->dst[i] == c->key)", |
325 | " { v = new_vertex(); v->key = t->key;", |
326 | " f = new_edge(v);", |
327 | " f->From = t->from[i];", |
328 | " f->To = t->to[i];", |
329 | " f->Nxt = c->Succ;", |
330 | " c->Succ = f;", |
331 | " if (nr > 0)", |
332 | " x_anytail(temptree[nr-1], v, nr-1);", |
333 | " }", |
334 | "", |
335 | " for (e = t->Succ; e; e = e->Nxt)", |
336 | " if ((ulong) e->Dst == c->key)", |
337 | " { v = new_vertex(); v->key = t->key;", |
338 | " f = new_edge(v);", |
339 | " f->From = e->From;", |
340 | " f->To = e->To;", |
341 | " f->s = e->s;", |
342 | " f->S = e->S;", |
343 | " f->Nxt = c->Succ;", |
344 | " c->Succ = f;", |
345 | " x_anytail(temptree[nr-1], v, nr-1);", |
346 | " }", |
347 | "", |
348 | " x_anytail(t->left, c, nr);", |
349 | " x_anytail(t->right, c, nr);", |
350 | "}", |
351 | "", |
352 | "static Vertex *", |
353 | "x_cpy_rev(void)", |
354 | "{ Vertex *c, *v; /* find 0 and !4 predecessor of F */", |
355 | "", |
356 | " v = x_tail(temptree[dfa_depth-1], F->key);", |
357 | " if (!v) return (Vertex *) 0;", |
358 | "", |
359 | " c = new_vertex(); c->key = v->key;", |
360 | "", |
361 | " /* every node on dfa_depth-2 that has v->key as succ */", |
362 | " /* make copy and let c point to these (reversing ptrs) */", |
363 | "", |
364 | " x_anytail(temptree[dfa_depth-2], c, dfa_depth-2);", |
365 | " ", |
366 | " return c;", |
367 | "}", |
368 | "", |
369 | "void", |
370 | "r_xpoint(void)", |
371 | "{ int fd; char nm[64]; Vertex *d;", |
372 | " int i, j;", |
373 | "", |
374 | " wcnt = 0;", |
375 | " sprintf(nm, \"%%s.xpt\", PanSource);", |
376 | " if ((fd = open(nm, 0)) < 0) /* O_RDONLY */", |
377 | " Uerror(\"cannot open checkpoint file\");", |
378 | "", |
379 | " xread(fd, (char *) &nstates, sizeof(double));", |
380 | " xread(fd, (char *) &truncs, sizeof(double));", |
381 | " xread(fd, (char *) &truncs2, sizeof(double));", |
382 | " xread(fd, (char *) &nlinks, sizeof(double));", |
383 | " xread(fd, (char *) &dfa_depth, sizeof(int));", |
384 | "", |
385 | " if (dfa_depth != MA+a_cycles)", |
386 | " Uerror(\"bad dfa_depth in checkpoint file\");", |
387 | "", |
388 | " path = (Vertex **) emalloc((dfa_depth+1)*sizeof(Vertex *));", |
389 | " layers = (Vertex **) emalloc(TWIDTH*(dfa_depth+1)*sizeof(Vertex *));", |
390 | " temptree = (Vertex **) emalloc((dfa_depth+2)*sizeof(Vertex *));", |
391 | " lastword = (uchar *) emalloc((dfa_depth+1)*sizeof(uchar));", |
392 | " lastword[dfa_depth] = lastword[0] = 255; ", |
393 | "", |
394 | " path[0] = R = new_vertex();", |
395 | " xread(fd, (char *) &R->key, sizeof(Vertex *));", |
396 | " R = insert_withkey(R, 0);", |
397 | "", |
398 | " F = new_vertex();", |
399 | " xread(fd, (char *) &F->key, sizeof(Vertex *));", |
400 | " F = insert_withkey(F, dfa_depth);", |
401 | "", |
402 | " NF = new_vertex();", |
403 | " xread(fd, (char *) &NF->key, sizeof(Vertex *));", |
404 | " NF = insert_withkey(NF, dfa_depth);", |
405 | "", |
406 | " for (j = 0; j < TWIDTH; j++)", |
407 | " for (i = 0; i < dfa_depth+1; i++)", |
408 | " r_layer(fd, i);", |
409 | "", |
410 | " if (wcnt != 0) Uerror(\"bad count in checkpoint file\");", |
411 | "", |
412 | " d = x_cpy_rev();", |
413 | " x_fixup();", |
414 | " stacker[dfa_depth-1] = 0;", |
415 | " x_rm_stack(d, dfa_depth-2);", |
416 | " x_cleanup(d);", |
417 | " close(fd);", |
418 | "", |
419 | " printf(\"pan: removed %%d stackstates\\n\", stackcnt);", |
420 | " nstates -= (double) stackcnt;", |
421 | "}", |
422 | "#endif", |
423 | 0, |
424 | }; |