8a876efd2f462db98f34f804dae095fdaa826a5b
1 /***** spin: pangen5.h *****/
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 */
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;",
22 "xwrite(int fd, char *b, int n)",
24 " if (wcnt+n >= 4096)",
25 " { write(fd, wbuf, wcnt);",
28 " memcpy(&wbuf[wcnt], b, n);",
36 " write(fd, wbuf, wcnt);",
42 "w_vertex(int fd, Vertex *v)",
43 "{ char t[3]; int i; Edge *e;",
45 " xwrite(fd, (char *) &v, sizeof(Vertex *));",
47 " for (i = 0; i < 2; i++)",
49 " { t[1] = v->from[i], t[2] = v->to[i];",
51 " xwrite(fd, (char *) &(v->dst[i]), sizeof(Vertex *));",
53 " for (e = v->Succ; e; e = e->Nxt)",
54 " { t[1] = e->From, t[2] = e->To;",
56 " xwrite(fd, (char *) &(e->Dst), sizeof(Vertex *));",
59 " { t[1] = t[2] = e->S;",
61 " xwrite(fd, (char *) &(e->Dst), sizeof(Vertex *));",
66 "w_layer(int fd, Vertex *v)",
70 " xwrite(fd, (char *) &c, 1);",
72 " w_layer(fd, v->lnk);",
73 " w_layer(fd, v->left);",
74 " w_layer(fd, v->right);",
79 "{ int fd; char nm[64];",
80 " int i, j; uchar c;",
81 " static uchar xwarned = 0;",
83 " sprintf(nm, \"%%s.xpt\", PanSource);",
84 " if ((fd = creat(nm, 0666)) <= 0)",
87 " printf(\"cannot creat checkpoint file\\n\");",
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 *));",
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);",
108 "xread(int fd, char *b, int n)",
109 "{ int m = wcnt; int delta = 0;",
111 " { if (m > 0) memcpy(b, &wbuf[WCNT-m], m);",
113 " WCNT = wcnt = read(fd, wbuf, 4096);",
115 " Uerror(\"xread failed -- insufficient data\");",
118 " memcpy(&b[delta], &wbuf[WCNT-wcnt], n);",
123 "x_cleanup(Vertex *c)",
124 "{ Edge *e; /* remove the tree and edges from c */",
126 " for (e = c->Succ; e; e = e->Nxt)",
127 " x_cleanup(e->Dst);",
133 "{ Vertex *tmp; int i, s;",
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);",
145 " stacker[dfa_depth-1] = 1;",
146 " s = dfa_member(dfa_depth-1);",
148 " { tmp = F; F = NF; NF = tmp; } /* complement */",
149 " if (s) dfa_store(stacker);",
150 " stacker[dfa_depth-1] = 0;",
151 " dfa_store(stacker);",
153 " { tmp = F; F = NF; NF = tmp; }",
157 "x_rm_stack(Vertex *t, int k)",
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);",
171 " { stacker[k] = e->S;",
172 " x_rm_stack(e->Dst, k-1);",
177 "insert_withkey(Vertex *v, int L)",
178 "{ Vertex *new, *t = temptree[L];",
180 " if (!t) { temptree[L] = v; return v; }",
181 " t = splay(v->key, t);",
182 " if (v->key < t->key)",
184 " new->left = t->left;",
186 " t->left = (Vertex *) 0;",
187 " } else if (v->key > t->key)",
189 " new->right = t->right;",
191 " t->right = (Vertex *) 0;",
193 " { if (t != R && t != F && t != NF)",
194 " Uerror(\"double insert, bad checkpoint data\");",
196 " { recyc_vertex(v);",
199 " temptree[L] = new;",
205 "find_withkey(Vertex *v, int L)",
206 "{ Vertex *t = temptree[L];",
208 " { temptree[L] = t = splay((ulong) v, t);",
209 " if (t->key == (ulong) v)",
212 " Uerror(\"not found error, bad checkpoint data\");",
213 " return (Vertex *) 0;",
217 "r_layer(int fd, int n)",
223 " { xread(fd, &c, 1);",
224 " if (c == 2) break;",
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);",
234 " xread(fd, (char *) &(e->Dst), sizeof(Vertex *));",
235 " insert_edge(v, e);",
240 "v_fix(Vertex *t, int nr)",
245 " for (i = 0; i < 2; i++)",
247 " t->dst[i] = find_withkey(t->dst[i], nr);",
249 " for (e = t->Succ; e; e = e->Nxt)",
250 " e->Dst = find_withkey(e->Dst, nr);",
252 " v_fix(t->left, nr);",
253 " v_fix(t->right, nr);",
257 "v_insert(Vertex *t, int nr)",
261 " v_insert(t->left, nr);",
262 " v_insert(t->right, nr);",
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++)",
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);",
278 " for (i = 0; i < dfa_depth; i++)",
279 " v_fix(temptree[i], (i+1));",
281 " for (i = dfa_depth; i >= 0; i--)",
282 " v_insert(temptree[i], i);",
286 "x_tail(Vertex *t, ulong want)",
287 "{ int i, yes, no; Edge *e; Vertex *v = (Vertex *) 0;",
289 " if (!t) return v;",
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)",
299 " if (t->from[i] <= 4 && t->to[i] >= 4)",
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))",
308 " else if (INRANGE(e, 4))",
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;",
318 "x_anytail(Vertex *t, Vertex *c, int nr)",
319 "{ int i; Edge *e, *f; Vertex *v;",
323 " for (i = 0; i < 2; i++)",
324 " if ((ulong) t->dst[i] == c->key)",
325 " { v = new_vertex(); v->key = t->key;",
327 " f->From = t->from[i];",
328 " f->To = t->to[i];",
329 " f->Nxt = c->Succ;",
332 " x_anytail(temptree[nr-1], v, nr-1);",
335 " for (e = t->Succ; e; e = e->Nxt)",
336 " if ((ulong) e->Dst == c->key)",
337 " { v = new_vertex(); v->key = t->key;",
339 " f->From = e->From;",
343 " f->Nxt = c->Succ;",
345 " x_anytail(temptree[nr-1], v, nr-1);",
348 " x_anytail(t->left, c, nr);",
349 " x_anytail(t->right, c, nr);",
354 "{ Vertex *c, *v; /* find 0 and !4 predecessor of F */",
356 " v = x_tail(temptree[dfa_depth-1], F->key);",
357 " if (!v) return (Vertex *) 0;",
359 " c = new_vertex(); c->key = v->key;",
361 " /* every node on dfa_depth-2 that has v->key as succ */",
362 " /* make copy and let c point to these (reversing ptrs) */",
364 " x_anytail(temptree[dfa_depth-2], c, dfa_depth-2);",
371 "{ int fd; char nm[64]; Vertex *d;",
375 " sprintf(nm, \"%%s.xpt\", PanSource);",
376 " if ((fd = open(nm, 0)) < 0) /* O_RDONLY */",
377 " Uerror(\"cannot open checkpoint file\");",
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));",
385 " if (dfa_depth != MA+a_cycles)",
386 " Uerror(\"bad dfa_depth in checkpoint file\");",
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; ",
394 " path[0] = R = new_vertex();",
395 " xread(fd, (char *) &R->key, sizeof(Vertex *));",
396 " R = insert_withkey(R, 0);",
398 " F = new_vertex();",
399 " xread(fd, (char *) &F->key, sizeof(Vertex *));",
400 " F = insert_withkey(F, dfa_depth);",
402 " NF = new_vertex();",
403 " xread(fd, (char *) &NF->key, sizeof(Vertex *));",
404 " NF = insert_withkey(NF, dfa_depth);",
406 " for (j = 0; j < TWIDTH; j++)",
407 " for (i = 0; i < dfa_depth+1; i++)",
410 " if (wcnt != 0) Uerror(\"bad count in checkpoint file\");",
414 " stacker[dfa_depth-1] = 0;",
415 " x_rm_stack(d, dfa_depth-2);",
419 " printf(\"pan: removed %%d stackstates\\n\", stackcnt);",
420 " nstates -= (double) stackcnt;",
This page took 0.039228 seconds and 3 git commands to generate.