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