pangen5.h 11 KB

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