trunk/verif/Spin/Src5.1.6/pangen5.h

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