1 /***** spin: pangen4.h *****/
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
8 * The DFA code below was written by Anuj Puri and Gerard J. Holzmann in
9 * May 1997, and was inspired by earlier work on data compression using
10 * sharing tree data structures and graph-encoded sets by J-Ch. Gregoire
11 * (INRS Telecom, Quebec, Canada) and D.Zampunieris (Univ.Namur, Belgium)
12 * The splay routine code included here is based on the public domain
13 * version written by D. Sleator <sleator@cs.cmu.edu> in 1992.
16 static const char *Dfa[] = {
21 "#define uchar unsigned char",
23 "#define ulong unsigned long",
24 "#define ushort unsigned short",
28 "#define HASH(y,n) (n)*(((long)y))",
29 "#define INRANGE(e,h) ((h>=e->From && h<=e->To)||(e->s==1 && e->S==h))",
31 "extern char *emalloc(unsigned long); /* imported routine */",
32 "extern void dfa_init(ushort); /* 4 exported routines */",
33 "extern int dfa_member(ulong);",
34 "extern int dfa_store(uchar *);",
35 "extern void dfa_stats(void);",
37 "typedef struct Edge {",
38 " uchar From, To; /* max range 0..255 */",
39 " uchar s, S; /* if s=1, S is singleton */",
40 " struct Vertex *Dst;",
44 "typedef struct Vertex {",
45 " ulong key, num; /* key for splay tree, nr incoming edges */",
46 " uchar from[2], to[2]; /* in-node predefined edge info */",
47 " struct Vertex *dst[2];/* most nodes have 2 or more edges */",
48 " struct Edge *Succ; /* in case there are more edges */",
49 " struct Vertex *lnk, *left, *right; /* splay tree plumbing */",
52 "static Edge *free_edges;",
53 "static Vertex *free_vertices;",
54 "static Vertex **layers; /* one splay tree of nodes per layer */",
55 "static Vertex **path; /* run of word in the DFA */",
56 "static Vertex *R, *F, *NF; /* Root, Final, Not-Final */",
57 "static uchar *word, *lastword;/* string, and last string inserted */",
58 "static int dfa_depth, iv=0, nv=0, pfrst=0, Tally;",
60 "static void insert_it(Vertex *, int); /* splay-tree code */",
61 "static void delete_it(Vertex *, int);",
62 "static Vertex *find_it(Vertex *, Vertex *, uchar, int);",
65 "recyc_edges(Edge *e)",
68 " recyc_edges(e->Nxt);",
69 " e->Nxt = free_edges;",
74 "new_edge(Vertex *dst)",
79 " free_edges = e->Nxt;",
80 " e->From = e->To = e->s = e->S = 0;",
81 " e->Nxt = (Edge *) 0;",
83 " e = (Edge *) emalloc(sizeof(Edge));",
90 "recyc_vertex(Vertex *v)",
92 " recyc_edges(v->Succ);",
93 " v->Succ = (Edge *) free_vertices;",
94 " free_vertices = v;",
102 " if (free_vertices)",
103 " { v = free_vertices;",
104 " free_vertices = (Vertex *) v->Succ;",
105 " v->Succ = (Edge *) 0;",
108 " v = (Vertex *) emalloc(sizeof(Vertex));",
115 "allDelta(Vertex *v, int n)",
116 "{ Vertex *dst = new_vertex();",
127 "insert_edge(Vertex *v, Edge *e)",
128 "{ /* put new edge first */",
130 " { v->dst[0] = e->Dst;",
131 " v->from[0] = e->From;",
132 " v->to[0] = e->To;",
137 " { v->from[1] = v->from[0]; v->from[0] = e->From;",
138 " v->to[1] = v->to[0]; v->to[0] = e->To;",
139 " v->dst[1] = v->dst[0]; v->dst[0] = e->Dst;",
143 " { int f = v->from[1];",
144 " int t = v->to[1];",
145 " Vertex *d = v->dst[1];",
146 " v->from[1] = v->from[0]; v->from[0] = e->From;",
147 " v->to[1] = v->to[0]; v->to[0] = e->To;",
148 " v->dst[1] = v->dst[0]; v->dst[0] = e->Dst;",
153 " e->Nxt = v->Succ;",
158 "copyRecursive(Vertex *v, Edge *e)",
160 " if (e->Nxt) copyRecursive(v, e->Nxt);",
161 " f = new_edge(e->Dst);",
162 " f->From = e->From;",
166 " f->Nxt = v->Succ;",
171 "copyEdges(Vertex *to, Vertex *from)",
173 " for (i = 0; i < 2; i++)",
174 " { to->from[i] = from->from[i];",
175 " to->to[i] = from->to[i];",
176 " to->dst[i] = from->dst[i];",
178 " if (from->Succ) copyRecursive(to, from->Succ);",
182 "cacheDelta(Vertex *v, int h, int first)",
183 "{ static Edge *ov, tmp; int i;",
185 " if (!first && INRANGE(ov,h))",
186 " return ov; /* intercepts about 10%% */",
187 " for (i = 0; i < 2; i++)",
188 " if (v->dst[i] && h >= v->from[i] && h <= v->to[i])",
189 " { tmp.From = v->from[i];",
190 " tmp.To = v->to[i];",
191 " tmp.Dst = v->dst[i];",
192 " tmp.s = tmp.S = 0;",
196 " for (ov = v->Succ; ov; ov = ov->Nxt)",
197 " if (INRANGE(ov,h)) return ov;",
199 " Uerror(\"cannot get here, cacheDelta\");",
200 " return (Edge *) 0;",
204 "Delta(Vertex *v, int h) /* v->delta[h] */",
207 " if (v->dst[0] && h >= v->from[0] && h <= v->to[0])",
208 " return v->dst[0]; /* oldest edge */",
209 " if (v->dst[1] && h >= v->from[1] && h <= v->to[1])",
210 " return v->dst[1];",
211 " for (e = v->Succ; e; e = e->Nxt)",
212 " if (INRANGE(e,h))",
214 " Uerror(\"cannot happen Delta\");",
215 " return (Vertex *) 0;",
219 "numDelta(Vertex *v, int d)",
224 " for (i = 0; i < 2; i++)",
226 " { cnt = v->dst[i]->num + d*(1 + v->to[i] - v->from[i]);",
227 " if (d == 1 && cnt < v->dst[i]->num) goto bad;",
228 " v->dst[i]->num = cnt;",
230 " for (e = v->Succ; e; e = e->Nxt)",
231 " { cnt = e->Dst->num + d*(1 + e->To - e->From + e->s);",
232 " if (d == 1 && cnt < e->Dst->num)",
233 "bad: Uerror(\"too many incoming edges\");",
234 " e->Dst->num = cnt;",
239 "setDelta(Vertex *v, int h, Vertex *newdst) /* v->delta[h] = newdst; */",
240 "{ Edge *e, *f = (Edge *) 0, *g;",
243 " /* remove the old entry, if there */",
244 " for (i = 0; i < 2; i++)",
245 " if (v->dst[i] && h >= v->from[i] && h <= v->to[i])",
246 " { if (h == v->from[i])",
247 " { if (h == v->to[i])",
248 " { v->dst[i] = (Vertex *) 0;",
249 " v->from[i] = v->to[i] = 0;",
252 " } else if (h == v->to[i])",
255 " { g = new_edge(v->dst[i]);/* same dst */",
256 " g->From = v->from[i];",
257 " g->To = h-1; /* left half */",
258 " v->from[i] = h+1; /* right half */",
259 " insert_edge(v, g);",
263 " for (e = v->Succ; e; f = e, e = e->Nxt)",
264 " { if (e->s == 1 && e->S == h)",
265 " { e->s = e->S = 0;",
268 " if (h >= e->From && h <= e->To)",
269 " { if (h == e->From)",
270 " { if (h == e->To)",
272 " { e->From = e->To = e->S;",
279 " } else if (h == e->To)",
281 " } else /* split */",
282 " { g = new_edge(e->Dst); /* same dst */",
283 " g->From = e->From;",
284 " g->To = h-1; /* g=left half */",
285 " e->From = h+1; /* e=right half */",
286 " g->Nxt = e->Nxt; /* insert g */",
287 " e->Nxt = g; /* behind e */",
288 " break; /* done */",
291 "rem_tst: if (e->From > e->To)",
292 " { if (e->s == 0) {",
296 " v->Succ = e->Nxt;",
297 " e->Nxt = (Edge *) 0;",
300 " { e->From = e->To = e->S;",
306 " /* check if newdst is already there */",
307 " for (i = 0; i < 2; i++)",
308 " if (v->dst[i] == newdst)",
309 " { if (h+1 == (int) v->from[i])",
310 " { v->from[i] = h;",
313 " if (h == (int) v->to[i]+1)",
317 " for (e = v->Succ; e; e = e->Nxt)",
318 " { if (e->Dst == newdst)",
319 " { if (h+1 == (int) e->From)",
321 " if (e->s == 1 && e->S+1 == e->From)",
322 " { e->From = e->S;",
327 " if (h == (int) e->To+1)",
329 " if (e->s == 1 && e->S == e->To+1)",
340 " /* add as a new edge */",
341 " e = new_edge(newdst);",
342 " e->From = e->To = h;",
343 " insert_edge(v, e);",
347 "cheap_key(Vertex *v)",
351 " { vk2 = (ulong) v->dst[0];",
352 " if ((ulong) v->dst[1] > vk2)",
353 " vk2 = (ulong) v->dst[1];",
354 " } else if (v->dst[1])",
355 " vk2 = (ulong) v->dst[1]; ",
358 " for (e = v->Succ; e; e = e->Nxt)",
359 " if ((ulong) e->Dst > vk2)",
360 " vk2 = (ulong) e->Dst;",
362 " Tally = (vk2>>2)&(TWIDTH-1);",
367 "mk_key(Vertex *v) /* not sensitive to order */",
368 "{ ulong m = 0, vk2 = 0;",
372 " { m += HASH(v->dst[0], v->to[0] - v->from[0] + 1);",
373 " vk2 = (ulong) v->dst[0]; ",
376 " { m += HASH(v->dst[1], v->to[1] - v->from[1] + 1);",
377 " if ((ulong) v->dst[1] > vk2) vk2 = (ulong) v->dst[1]; ",
379 " for (e = v->Succ; e; e = e->Nxt)",
380 " { m += HASH(e->Dst, e->To - e->From + 1 + e->s);",
381 " if ((ulong) e->Dst > vk2) vk2 = (ulong) e->Dst; ",
383 " Tally = (vk2>>2)&(TWIDTH-1);",
388 "mk_special(int sigma, Vertex *n, Vertex *v)",
389 "{ ulong m = 0, vk2 = 0;",
393 " for (i = 0; i < 2; i++)",
395 " { if (sigma >= v->from[i] && sigma <= v->to[i])",
396 " { m += HASH(v->dst[i], v->to[i]-v->from[i]);",
397 " if ((ulong) v->dst[i] > vk2",
398 " && v->to[i] > v->from[i])",
399 " vk2 = (ulong) v->dst[i]; ",
401 " { m += HASH(v->dst[i], v->to[i]-v->from[i]+1);",
402 " if ((ulong) v->dst[i] > vk2)",
403 " vk2 = (ulong) v->dst[i]; ",
405 " for (f = v->Succ; f; f = f->Nxt)",
406 " { if (sigma >= f->From && sigma <= f->To)",
407 " { m += HASH(f->Dst, f->To - f->From + f->s);",
408 " if ((ulong) f->Dst > vk2",
409 " && f->To - f->From + f->s > 0)",
410 " vk2 = (ulong) f->Dst; ",
411 " } else if (f->s == 1 && sigma == f->S)",
412 " { m += HASH(f->Dst, f->To - f->From + 1);",
413 " if ((ulong) f->Dst > vk2) vk2 = (ulong) f->Dst; ",
415 " { m += HASH(f->Dst, f->To - f->From + 1 + f->s);",
416 " if ((ulong) f->Dst > vk2) vk2 = (ulong) f->Dst; ",
419 " if ((ulong) n > vk2) vk2 = (ulong) n; ",
420 " Tally = (vk2>>2)&(TWIDTH-1);",
426 "dfa_init(ushort nr_layers)",
427 "{ int i; Vertex *r, *t;",
429 " dfa_depth = nr_layers; /* one byte per layer */",
430 " path = (Vertex **) emalloc((dfa_depth+1)*sizeof(Vertex *));",
431 " layers = (Vertex **) emalloc(TWIDTH*(dfa_depth+1)*sizeof(Vertex *));",
432 " lastword = (uchar *) emalloc((dfa_depth+1)*sizeof(uchar));",
433 " lastword[dfa_depth] = lastword[0] = 255;",
434 " path[0] = R = new_vertex(); F = new_vertex();",
436 " for (i = 1, r = R; i < dfa_depth; i++, r = t)",
437 " t = allDelta(r, i-1);",
438 " NF = allDelta(r, i-1);",
442 "static void complement_dfa(void) { Vertex *tmp = F; F = NF; NF = tmp; }",
446 "tree_stats(Vertex *t)",
447 "{ Edge *e; double cnt=0.0;",
448 " if (!t) return 0;",
449 " if (!t->key) return 0;",
450 " t->key = 0; /* precaution */",
451 " if (t->dst[0]) cnt++;",
452 " if (t->dst[1]) cnt++;",
453 " for (e = t->Succ; e; e = e->Nxt)",
455 " cnt += tree_stats(t->lnk);",
456 " cnt += tree_stats(t->left);",
457 " cnt += tree_stats(t->right);",
463 "{ int i, j; double cnt = 0.0;",
464 " for (j = 0; j < TWIDTH; j++)",
465 " for (i = 0; i < dfa_depth+1; i++)",
466 " cnt += tree_stats(layers[i*TWIDTH+j]);",
467 " printf(\"Minimized Automaton:\t%%6lu nodes and %%6g edges\\n\",",
472 "dfa_member(ulong n)",
473 "{ Vertex **p, **q;",
474 " uchar *w = &word[n];",
477 " p = &path[n]; q = (p+1);",
478 " for (i = n; i < dfa_depth; i++)",
479 " *q++ = Delta(*p++, *w++);",
480 " return (*p == F);",
484 "dfa_store(uchar *sv)",
485 "{ Vertex **p, **q, *s, *y, *old, *new = F;",
486 " uchar *w, *u = lastword;",
490 " while (*w++ == *u++) /* find first byte that differs */",
492 " pfrst = (int) (u - lastword) - 1;",
493 " memcpy(&lastword[pfrst], &sv[pfrst], dfa_depth-pfrst);",
494 " if (pfrst > iv) pfrst = iv;",
495 " if (pfrst > nv) pfrst = nv;",
497 " p = &path[pfrst]; q = (p+1); w = &word[pfrst];",
498 " for (i = pfrst; i < dfa_depth; i++)",
499 " *q++ = Delta(*p++, *w++); /* (*p)->delta[*w++]; */",
501 " if (*p == F) return 1; /* it's already there */",
506 " new = find_it(path[iv], old, word[iv], iv);",
507 " } while (new && iv > 0);",
510 " nv = k = 0; s = path[0];",
511 " for (j = 1; j <= iv; ++j) ",
512 " if (path[j]->num > 1)",
513 " { y = new_vertex();",
514 " copyEdges(y, path[j]);",
517 " delete_it(s, j-1);",
518 " setDelta(s, word[j-1], y);",
519 " insert_it(s, j-1);",
520 " y->num = 1; /* initial value 1 */",
522 " path[j]->num--; /* only 1 moved from j to y */",
528 " y = Delta(s, word[iv]);",
530 " delete_it(s, iv); ",
531 " setDelta(s, word[iv], old);",
532 " insert_it(s, iv); ",
535 " for (j = iv+1; j < dfa_depth; j++)",
536 " if (path[j]->num == 0)",
537 " { numDelta(path[j], -1);",
538 " delete_it(path[j], j);",
539 " recyc_vertex(path[j]);",
546 "splay(ulong i, Vertex *t)",
547 "{ Vertex N, *l, *r, *y;",
549 " if (!t) return t;",
550 " N.left = N.right = (Vertex *) 0;",
553 " { if (i < t->key)",
554 " { if (!t->left) break;",
555 " if (i < t->left->key)",
557 " t->left = y->right;",
560 " if (!t->left) break;",
565 " } else if (i > t->key)",
566 " { if (!t->right) break;",
567 " if (i > t->right->key)",
569 " t->right = y->left;",
572 " if (!t->right) break;",
580 " l->right = t->left;",
581 " r->left = t->right;",
582 " t->left = N.right;",
583 " t->right = N.left;",
588 "insert_it(Vertex *v, int L)",
589 "{ Vertex *new, *t;",
593 " nr = ((L*TWIDTH)+Tally);",
598 " { layers[nr] = v;",
604 " new->left = t->left;",
606 " t->left = (Vertex *) 0;",
607 " } else if (i > t->key)",
609 " new->right = t->right;",
611 " t->right = (Vertex *) 0;",
612 " } else /* it's already there */",
613 " { v->lnk = t->lnk; /* put in linked list off v */",
617 " layers[nr] = new;",
621 "checkit(Vertex *h, Vertex *v, Vertex *n, uchar sigma)",
625 " for (k = 0; k < 2; k++)",
627 " { if (sigma >= h->from[k] && sigma <= h->to[k])",
628 " { if (h->dst[k] != n) goto no_match;",
630 " for (i = h->from[k]; i <= h->to[k]; i++)",
631 " { if (i == sigma) continue;",
632 " g = cacheDelta(v, i, j); j = 0;",
633 " if (h->dst[k] != g->Dst)",
635 " if (g->s == 0 || g->S != i)",
638 " for (f = h->Succ; f; f = f->Nxt)",
639 " { if (INRANGE(f,sigma))",
640 " { if (f->Dst != n) goto no_match;",
642 " for (i = f->From; i <= f->To; i++)",
643 " { if (i == sigma) continue;",
644 " g = cacheDelta(v, i, j); j = 0;",
645 " if (f->Dst != g->Dst)",
647 " if (g->s == 1 && i == g->S)",
651 " if (f->s && f->S != sigma)",
652 " { g = cacheDelta(v, f->S, 1);",
653 " if (f->Dst != g->Dst)",
657 " if (h->Succ || h->dst[0] || h->dst[1]) return 1;",
663 "find_it(Vertex *v, Vertex *n, uchar sigma, int L)",
667 " i = mk_special(sigma,n,v);",
668 " nr = ((L*TWIDTH)+Tally);",
671 " if (!t) return (Vertex *) 0;",
672 " layers[nr] = t = splay(i, t);",
674 " for (z = t; z; z = z->lnk)",
675 " if (checkit(z, v, n, sigma))",
678 " return (Vertex *) 0;",
682 "delete_it(Vertex *v, int L)",
686 " i = cheap_key(v);",
687 " nr = ((L*TWIDTH)+Tally);",
693 " { Vertex *z, *y = (Vertex *) 0;",
694 " for (z = t; z && z != v; y = z, z = z->lnk)",
696 " if (z != v) goto bad;",
698 " { y->lnk = z->lnk;",
699 " z->lnk = (Vertex *) 0;",
702 " } else if (z->lnk) /* z == t == v */",
704 " y->left = t->left;",
705 " y->right = t->right;",
706 " t->left = t->right = t->lnk = (Vertex *) 0;",
710 " /* delete the node itself */",
714 " { x = splay(i, t->left);",
715 " x->right = t->right;",
717 " t->left = t->right = t->lnk = (Vertex *) 0;",
721 "bad: Uerror(\"cannot happen delete\");",