| 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 | }; |