sys/src/cmd/spin/pangen2.h

   1 /***** spin: pangen2.h *****/
   2
   3 /* Copyright (c) 1989-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 *Nvr1[] = {         /* allow separate compilation */
  13         "#ifdef VERI",
  14         "void",
  15         "check_claim(int st)",
  16         "{",
  17         "       if (st == endclaim)",
  18         "               uerror(\"claim violated!\");",
  19         "       if (stopstate[VERI][st])",
  20         "               uerror(\"end state in claim reached\");",
  21         "}",
  22         "#endif",
  23         0,
  24 };
  25
  26 static char *Pre0[] = {
  27 "#ifdef SC",
  28         "#define _FILE_OFFSET_BITS      64",    /* to allow file sizes greater than 2Gb */
  29 "#endif",
  30         "#include <stdio.h>",
  31         "#include <signal.h>",
  32         "#include <stdlib.h>",
  33         "#include <stdarg.h>",
  34         "#include <string.h>",
  35         "#include <ctype.h>",
  36         "#include <errno.h>",
  37         "#if defined(WIN32) || defined(WIN64)",
  38                 "#include <time.h>",
  39         "#else",
  40                 "#include <unistd.h>",
  41                 "#include <sys/times.h>",       /* new 4.3.0 */
  42         "#endif",
  43         "#include <sys/types.h>",       /* defines off_t */
  44         "#include <sys/stat.h>",
  45         "#include <fcntl.h>",
  46         "#define Offsetof(X, Y) ((unsigned long)(&(((X *)0)->Y)))",
  47         "#ifndef max",
  48         "#define max(a,b) (((a)<(b)) ? (b) : (a))",
  49         "#endif",
  50         "#ifndef PRINTF",
  51         "int Printf(const char *fmt, ...); /* prototype only */",
  52         "#endif",
  53         0,
  54 };
  55
  56 static char *Preamble[] = {
  57
  58         "#ifdef CNTRSTACK",
  59         "#define onstack_now()  (LL[trpt->j6] && LL[trpt->j7])",
  60         "#define onstack_put()   LL[trpt->j6]++; LL[trpt->j7]++",
  61         "#define onstack_zap()   LL[trpt->j6]--; LL[trpt->j7]--",
  62         "#endif",
  63
  64         "#if !defined(SAFETY) && !defined(NOCOMP)",
  65                 /*
  66                  * V_A identifies states in the current statespace
  67                  * A_V identifies states in the 'other' statespace
  68                  * S_A remembers how many leading bytes in the sv
  69                  * are used for these markers + fairness bits
  70                  */
  71                 "#define V_A    (((now._a_t&1)?2:1) << (now._a_t&2))",
  72                 "#define A_V    (((now._a_t&1)?1:2) << (now._a_t&2))",
  73                 "int    S_A = 0;",
  74         "#else",
  75                 "#define V_A    0",
  76                 "#define A_V    0",
  77                 "#define S_A    0",
  78         "#endif",
  79
  80 "#ifdef MA",
  81         "#undef onstack_now",
  82         "#undef onstack_put",
  83         "#undef onstack_zap",
  84         "#define onstack_put()  ;",
  85         "#define onstack_zap()  gstore((char *) &now, vsize, 4)",
  86 "#else",
  87         "#if defined(FULLSTACK) && !defined(BITSTATE)",
  88         "#define onstack_put()  trpt->ostate = Lstate",
  89         "#define onstack_zap()  { \\",
  90         "       if (trpt->ostate) \\",
  91         "               trpt->ostate->tagged = \\",
  92         "               (S_A)? (trpt->ostate->tagged&~V_A) : 0; \\",
  93         "       }",
  94         "#endif",
  95 "#endif",
  96         "struct H_el {",
  97         "       struct H_el *nxt;",
  98         "#ifdef FULLSTACK",
  99         "       unsigned int tagged;",
 100                 "#if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)",
 101                 "       unsigned int proviso;", /* uses just 1 bit 0/1 */
 102                 "#endif",
 103         "#endif",
 104         "#if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))",
 105         "       unsigned long st_id;",
 106         "#endif",
 107         "#ifdef COLLAPSE",
 108                 "#if VECTORSZ<65536",
 109         "       unsigned short ln;",    /* length of vector */
 110                 "#else",
 111         "       unsigned long ln;",     /* length of vector */
 112                 "#endif",
 113         "#endif",
 114         "#if !defined(SAFETY) || defined(REACH)",
 115         "       unsigned int D;",
 116         "#endif",
 117         "       unsigned state;",
 118         "} **H_tab, **S_Tab;\n",
 119
 120         "typedef struct Trail {",
 121         "       int   st;       /* current state */",
 122         "       uchar pr;       /* process id */",
 123         "       uchar tau;      /* 8 bit-flags */",
 124         "       uchar o_pm;     /* 8 more bit-flags */",
 125         "#if 0",
 126         "       Meaning of bit-flags:",
 127         "       tau&1   -> timeout enabled",
 128         "       tau&2   -> request to enable timeout 1 level up (in claim)",
 129         "       tau&4   -> current transition is a  claim move",
 130         "       tau&8   -> current transition is an atomic move",
 131         "       tau&16  -> last move was truncated on stack",
 132         "       tau&32  -> current transition is a preselected move",
 133         "       tau&64  -> at least one next state is not on the stack",
 134         "       tau&128 -> current transition is a stutter move",
 135
 136         "       o_pm&1  -> the current pid moved -- implements else",
 137         "       o_pm&2  -> this is an acceptance state",
 138         "       o_pm&4  -> this is a  progress state",
 139         "       o_pm&8  -> fairness alg rule 1 undo mark",
 140         "       o_pm&16 -> fairness alg rule 3 undo mark",
 141         "       o_pm&32 -> fairness alg rule 2 undo mark",
 142         "       o_pm&64 -> the current proc applied rule2",
 143         "       o_pm&128 -> a fairness, dummy move - all procs blocked",
 144         "#endif",
 145         "#if defined(FULLSTACK) && defined(MA) && !defined(BFS)",
 146         "       uchar proviso;",
 147         "#endif",
 148         "#ifndef BFS",
 149         "       uchar  o_n, o_ot;       /* to save locals */",
 150         "#endif",
 151         "       uchar  o_m;",
 152         "#ifdef EVENT_TRACE",
 153                 "#if nstates_event<256",
 154         "       uchar o_event;",
 155                 "#else",
 156         "       unsigned short o_event;",
 157                 "#endif",
 158         "#endif",
 159         "       int o_tt;",
 160         "#ifndef BFS",
 161         "       short o_To;",
 162                 "#ifdef RANDOMIZE",
 163         "       short oo_i;",
 164                 "#endif",
 165         "#endif",
 166         "#if defined(HAS_UNLESS) && !defined(BFS)",
 167         "       int e_state;    /* if escape trans - state of origin */",
 168         "#endif",
 169         "#if (defined(FULLSTACK) && !defined(MA)) || defined(BFS)",
 170         "       struct H_el *ostate;    /* pointer to stored state */",
 171         "#endif",
 172         /* CNTRSTACK when !NOREDUCE && BITSTATE && SAFETY, uses LL[] */
 173         "#if defined(CNTRSTACK) && !defined(BFS)",
 174         "       long    j6, j7;",
 175         "#endif",
 176         "       Trans *o_t;",   /* transition fct, next state   */
 177         "#ifdef HAS_SORTED",
 178         "       short ipt;",    /* insertion slot in q */
 179         "#endif",
 180         "       union {",
 181         "               int oval;",     /* single backup value of variable */
 182         "               int *ovals;",   /* ptr to multiple values */
 183         "       } bup;",
 184         "} Trail;",
 185         "Trail  *trail, *trpt;",
 186
 187         "FILE   *efd;",
 188         "uchar  *this;",
 189         "long   maxdepth=10000;",
 190         "long   omaxdepth=10000;",
 191         "#ifdef SC",    /* stack cycling */
 192         "char   *stackfile;",
 193         "#endif",
 194         "uchar  *SS, *LL;",
 195         "uchar  HASH_NR = 0;",
 196         "",
 197         "double memcnt = (double) 0;",
 198         "double memlim = (double) (1<<30);",
 199         "",
 200         "/* for emalloc: */",
 201         "static char *have;",
 202         "static long left = 0L;",
 203         "static double fragment = (double) 0;",
 204         "static unsigned long grow;",
 205         "",
 206         "unsigned int HASH_CONST[] = {",
 207         "       /* asuming 4 bytes per int */",
 208         "       0x88888EEF,     0x00400007,",
 209         "       0x04c11db7,     0x100d4e63,",
 210         "       0x0fc22f87,     0x3ff0c3ff,",
 211         "       0x38e84cd7,     0x02b148e9,",
 212         "       0x98b2e49d,     0xb616d379,",
 213         "       0xa5247fd9,     0xbae92a15,",
 214         "       0xb91c8bc5,     0x8e5880f3,",
 215         "       0xacd7c069,     0xb4c44bb3,",
 216         "       0x2ead1fb7,     0x8e428171,",
 217         "       0xdbebd459,     0x828ae611,",
 218         "       0x6cb25933,     0x86cdd651,",
 219         "       0x9e8f5f21,     0xd5f8d8e7,",
 220         "       0x9c4e956f,     0xb5cf2c71,",
 221         "       0x2e805a6d,     0x33fc3a55,",
 222         "       0xaf203ed1,     0xe31f5909,",
 223         "       0x5276db35,     0x0c565ef7,",
 224         "       0x273d1aa5,     0x8923b1dd,",
 225         "       0",
 226         "};",
 227         "int    mreached=0, done=0, errors=0, Nrun=1;",
 228         "double nstates=0, nlinks=0, truncs=0, truncs2=0;",
 229         "double nlost=0, nShadow=0, hcmp=0, ngrabs=0;",
 230         "#ifdef BFS",
 231         "double midrv=0, failedrv=0, revrv=0;",
 232         "#endif",
 233         "unsigned long  nr_states=0; /* nodes in DFA */",
 234         "long   Fa=0, Fh=0, Zh=0, Zn=0;",
 235         "long   PUT=0, PROBE=0, ZAPS=0;",
 236         "long   Ccheck=0, Cholds=0;",
 237         "int    a_cycles=0, upto=1, strict=0, verbose = 0, signoff = 0;",
 238         "#ifdef HAS_CODE",
 239         "int    gui = 0, coltrace = 0, readtrail = 0, whichtrail = 0, onlyproc = -1, silent = 0;",
 240         "#endif",
 241         "int    state_tables=0, fairness=0, no_rck=0, Nr_Trails=0;",
 242         "char   simvals[128];",
 243         "#ifndef INLINE",
 244         "int    TstOnly=0;",
 245         "#endif",
 246         "unsigned long mask, nmask;",
 247         "#ifdef BITSTATE",
 248         "int    ssize=23;       /* 1 Mb */",
 249         "#else",
 250         "int    ssize=19;       /* 512K slots */",
 251         "#endif",
 252         "int    hmax=0, svmax=0, smax=0;",
 253         "int    Maxbody=0, XX;",
 254         "uchar  *noptr; /* used by macro Pptr(x) */",
 255         "#ifdef VAR_RANGES",
 256         "void logval(char *, int);",
 257         "void dumpranges(void);",
 258         "#endif",
 259
 260         "#ifdef MA",
 261         "#define INLINE_REV",
 262         "extern void dfa_init(unsigned short);",
 263         "extern int  dfa_member(unsigned long);",
 264         "extern int  dfa_store(uchar *);",
 265         "unsigned int   maxgs = 0;",
 266         "#endif",
 267
 268         "State  comp_now;       /* compressed state vector */",
 269         "State  comp_msk;",
 270         "uchar  *Mask = (uchar *) &comp_msk;",
 271         "#ifdef COLLAPSE",
 272         "State  comp_tmp;",
 273         "static char    *scratch = (char *) &comp_tmp;",
 274         "#endif",
 275
 276         "Stack  *stack;         /* for queues, processes */",
 277         "Svtack *svtack;        /* for old state vectors */",
 278         "#ifdef BITSTATE",
 279         "static unsigned hfns = 3;      /* new default */",
 280         "#endif",
 281         "static unsigned long j1;",
 282         "static unsigned long K1, K2;",
 283         "static unsigned long j2, j3, j4;",
 284         "#ifdef BITSTATE",
 285 #ifndef POWOW
 286         "static long udmem;",
 287 #endif
 288         "#endif",
 289         "static long    A_depth = 0;",
 290         "long   depth = 0;",    /* not static to support -S2 option, but possible clash with embedded code */
 291         "static uchar   warned = 0, iterative = 0, like_java = 0, every_error = 0;",
 292         "static uchar   noasserts = 0, noends = 0, bounded = 0;",
 293         "#if SYNC>0 && ASYNC==0",
 294         "void set_recvs(void);",
 295         "int  no_recvs(int);",
 296         "#endif",
 297         "#if SYNC",
 298         "#define IfNotBlocked   if (boq != -1) continue;",
 299         "#define UnBlock        boq = -1",
 300         "#else",
 301         "#define IfNotBlocked   /* cannot block */",
 302         "#define UnBlock        /* don't bother */",
 303         "#endif\n",
 304         "#ifdef BITSTATE",
 305         "int (*bstore)(char *, int);",
 306         "int bstore_reg(char *, int);",
 307 #ifndef POWOW
 308         "int bstore_mod(char *, int);",
 309 #endif
 310         "#endif",
 311         "void active_procs(void);",
 312         "void cleanup(void);",
 313         "void do_the_search(void);",
 314         "void find_shorter(int);",
 315         "void iniglobals(void);",
 316         "void stopped(int);",
 317         "void wrapup(void);",
 318         "int *grab_ints(int);",
 319         "void ungrab_ints(int *, int);",
 320         0,
 321 };
 322
 323 static char *Tail[] = {
 324         "Trans *",
 325         "settr( int t_id, int a, int b, int c, int d,",
 326         "       char *t, int g, int tpe0, int tpe1)",
 327         "{      Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n",
 328         "       tmp->atom  = a&(6|32);  /* only (2|8|32) have meaning */",
 329         "       if (!g) tmp->atom |= 8; /* no global references */",
 330         "       tmp->st    = b;",
 331         "       tmp->tpe[0] = tpe0;",
 332         "       tmp->tpe[1] = tpe1;",
 333         "       tmp->tp    = t;",
 334         "       tmp->t_id  = t_id;",
 335         "       tmp->forw  = c;",
 336         "       tmp->back  = d;",
 337         "       return tmp;",
 338         "}\n",
 339         "Trans *",
 340         "cpytr(Trans *a)",
 341         "{      Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n",
 342         "       int i;",
 343         "       tmp->atom  = a->atom;",
 344         "       tmp->st    = a->st;",
 345         "#ifdef HAS_UNLESS",
 346         "       tmp->e_trans = a->e_trans;",
 347         "       for (i = 0; i < HAS_UNLESS; i++)",
 348         "               tmp->escp[i] = a->escp[i];",
 349         "#endif",
 350         "       tmp->tpe[0] = a->tpe[0];",
 351         "       tmp->tpe[1] = a->tpe[1];",
 352         "       for (i = 0; i < 6; i++)",
 353         "       {       tmp->qu[i] = a->qu[i];",
 354         "               tmp->ty[i] = a->ty[i];",
 355         "       }",
 356         "       tmp->tp    = (char *) emalloc(strlen(a->tp)+1);",
 357         "       strcpy(tmp->tp, a->tp);",
 358         "       tmp->t_id  = a->t_id;",
 359         "       tmp->forw  = a->forw;",
 360         "       tmp->back  = a->back;",
 361         "       return tmp;",
 362         "}\n",
 363         "#ifndef NOREDUCE",
 364         "int",
 365         "srinc_set(int n)",
 366         "{      if (n <= 2) return LOCAL;",
 367         "       if (n <= 2+  DELTA) return Q_FULL_F; /* 's' or nfull  */",
 368         "       if (n <= 2+2*DELTA) return Q_EMPT_F; /* 'r' or nempty */",
 369         "       if (n <= 2+3*DELTA) return Q_EMPT_T; /* empty */",
 370         "       if (n <= 2+4*DELTA) return Q_FULL_T; /* full  */",
 371         "       if (n ==   5*DELTA) return GLOBAL;",
 372         "       if (n ==   6*DELTA) return TIMEOUT_F;",
 373         "       if (n ==   7*DELTA) return ALPHA_F;",
 374         "       Uerror(\"cannot happen srinc_class\");",
 375         "       return BAD;",
 376         "}",
 377         "int",
 378         "srunc(int n, int m)",
 379         "{      switch(m) {",
 380         "       case Q_FULL_F: return n-2;",
 381         "       case Q_EMPT_F: return n-2-DELTA;",
 382         "       case Q_EMPT_T: return n-2-2*DELTA;",
 383         "       case Q_FULL_T: return n-2-3*DELTA;",
 384         "       case ALPHA_F:",
 385         "       case TIMEOUT_F: return 257; /* non-zero, and > MAXQ */",
 386         "       }",
 387         "       Uerror(\"cannot happen srunc\");",
 388         "       return 0;",
 389         "}",
 390         "#endif",
 391         "int cnt;",
 392         "#ifdef HAS_UNLESS",
 393         "int",
 394         "isthere(Trans *a, int b)", /* is b already in a's list? */
 395         "{      Trans *t;",
 396         "       for (t = a; t; t = t->nxt)",
 397         "               if (t->t_id == b)",
 398         "                       return 1;",
 399         "       return 0;",
 400         "}",
 401         "#endif",
 402         "#ifndef NOREDUCE",
 403         "int",
 404         "mark_safety(Trans *t) /* for conditional safety */",
 405         "{      int g = 0, i, j, k;",
 406         "",
 407         "       if (!t) return 0;",
 408         "       if (t->qu[0])",
 409         "               return (t->qu[1])?2:1;  /* marked */",
 410         "",
 411         "       for (i = 0; i < 2; i++)",
 412         "       {       j = srinc_set(t->tpe[i]);",
 413         "               if (j >= GLOBAL && j != ALPHA_F)",
 414         "                       return -1;",
 415         "               if (j != LOCAL)",
 416         "               {       k = srunc(t->tpe[i], j);",
 417         "                       if (g == 0",
 418         "                       ||  t->qu[0] != k",
 419         "                       ||  t->ty[0] != j)",
 420         "                       {       t->qu[g] = k;",
 421         "                               t->ty[g] = j;",
 422         "                               g++;",
 423         "       }       }       }",
 424         "       return g;",
 425         "}",
 426         "#endif",
 427         "void",
 428         "retrans(int n, int m, int is, short srcln[], uchar reach[])",
 429         "       /* process n, with m states, is=initial state */",
 430         "{      Trans *T0, *T1, *T2, *T3;",
 431         "       int i, k;",
 432         "#ifndef NOREDUCE",
 433         "       int g, h, j, aa;",
 434         "#endif",
 435         "#ifdef HAS_UNLESS",
 436         "       int p;",
 437         "#endif",
 438         "       if (state_tables >= 4)",
 439         "       {       printf(\"STEP 1 proctype %%s\\n\", ",
 440         "                       procname[n]);",
 441         "               for (i = 1; i < m; i++)",
 442         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 443         "                       crack(n, i, T0, srcln);",
 444         "               return;",
 445         "       }",
 446         "       do {",
 447         "               for (i = 1, cnt = 0; i < m; i++)",
 448         "               {       T2 = trans[n][i];",
 449         "                       T1 = T2?T2->nxt:(Trans *)0;",
 450         "/* prescan: */         for (T0 = T1; T0; T0 = T0->nxt)",
 451         "/* choice in choice */ {       if (T0->st && trans[n][T0->st]",
 452         "                               &&  trans[n][T0->st]->nxt)",
 453         "                                       break;",
 454         "                       }",
 455         "#if 0",
 456         "               if (T0)",
 457         "               printf(\"\\tstate %%d / %%d: choice in choice\\n\",",
 458         "               i, T0->st);",
 459         "#endif",
 460         "                       if (T0)",
 461         "                       for (T0 = T1; T0; T0 = T0->nxt)",
 462         "                       {       T3 = trans[n][T0->st];",
 463         "                               if (!T3->nxt)",
 464         "                               {       T2->nxt = cpytr(T0);",
 465         "                                       T2 = T2->nxt;",
 466         "                                       imed(T2, T0->st, n, i);",
 467         "                                       continue;",
 468         "                               }",
 469         "                               do {    T3 = T3->nxt;",
 470         "                                       T2->nxt = cpytr(T3);",
 471         "                                       T2 = T2->nxt;",
 472         "                                       imed(T2, T0->st, n, i);",
 473         "                               } while (T3->nxt);",
 474         "                               cnt++;",
 475         "                       }",
 476         "               }",
 477         "       } while (cnt);",
 478
 479         "       if (state_tables >= 3)",
 480         "       {       printf(\"STEP 2 proctype %%s\\n\", ",
 481         "                       procname[n]);",
 482         "               for (i = 1; i < m; i++)",
 483         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 484         "                       crack(n, i, T0, srcln);",
 485         "               return;",
 486         "       }",
 487         "       for (i = 1; i < m; i++)",
 488         "       {       if (trans[n][i] && trans[n][i]->nxt) /* optimize */",
 489         "               {       T1 = trans[n][i]->nxt;",
 490         "#if 0",
 491         "                       printf(\"\\t\\tpull %%d (%%d) to %%d\\n\",",
 492         "                       T1->st, T1->forw, i);",
 493         "#endif",
 494         "                       if (!trans[n][T1->st]) continue;",
 495         "                       T0 = cpytr(trans[n][T1->st]);",
 496         "                       trans[n][i] = T0;",
 497         "                       reach[T1->st] = 1;",
 498         "                       imed(T0, T1->st, n, i);",
 499         "                       for (T1 = T1->nxt; T1; T1 = T1->nxt)",
 500         "                       {",
 501         "#if 0",
 502         "                       printf(\"\\t\\tpull %%d (%%d) to %%d\\n\",",
 503         "                               T1->st, T1->forw, i);",
 504         "#endif",
 505         "                               if (!trans[n][T1->st]) continue;",
 506         "                               T0->nxt = cpytr(trans[n][T1->st]);",
 507         "                               T0 = T0->nxt;",
 508         "                               reach[T1->st] = 1;",
 509         "                               imed(T0, T1->st, n, i);",
 510         "       }       }       }",
 511         "       if (state_tables >= 2)",
 512         "       {       printf(\"STEP 3 proctype %%s\\n\", ",
 513         "                       procname[n]);",
 514         "               for (i = 1; i < m; i++)",
 515         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 516         "                       crack(n, i, T0, srcln);",
 517         "               return;",
 518         "       }",
 519         "#ifdef HAS_UNLESS",
 520         "       for (i = 1; i < m; i++)",
 521         "       {       if (!trans[n][i]) continue;",
 522         "               /* check for each state i if an",
 523         "                * escape to some state p is defined",
 524         "                * if so, copy and mark p's transitions",
 525         "                * and prepend them to the transition-",
 526         "                * list of state i",
 527         "                */",
 528         " if (!like_java) /* the default */",
 529         " {             for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 530         "               for (k = HAS_UNLESS-1; k >= 0; k--)",
 531         "               {       if (p = T0->escp[k])",
 532         "                       for (T1 = trans[n][p]; T1; T1 = T1->nxt)",
 533         "                       {       if (isthere(trans[n][i], T1->t_id))",
 534         "                                       continue;",
 535         "                               T2 = cpytr(T1);",
 536         "                               T2->e_trans = p;",
 537         "                               T2->nxt = trans[n][i];",
 538         "                               trans[n][i] = T2;",
 539         "               }       }",
 540         " } else /* outermost unless checked first */",
 541         " {             Trans *T4;",
 542         "               T4 = T3 = (Trans *) 0;",
 543         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 544         "               for (k = HAS_UNLESS-1; k >= 0; k--)",
 545         "               {       if (p = T0->escp[k])",
 546         "                       for (T1 = trans[n][p]; T1; T1 = T1->nxt)",
 547         "                       {       if (isthere(trans[n][i], T1->t_id))",
 548         "                                       continue;",
 549         "                               T2 = cpytr(T1);",
 550         "                               T2->nxt = (Trans *) 0;",
 551         "                               T2->e_trans = p;",
 552         "                               if (T3) T3->nxt = T2;",
 553         "                               else    T4 = T2;",
 554         "                               T3 = T2;",
 555         "               }       }",
 556         "               if (T4)",
 557         "               {       T3->nxt = trans[n][i];",
 558         "                       trans[n][i] = T4;",
 559         "               }",
 560         " }",
 561         "       }",
 562         "#endif",
 563
 564         "#ifndef NOREDUCE",
 565         "       for (i = 1; i < m; i++)",
 566         "       {",
 567         "               if (a_cycles)",
 568         "               { /* moves through these states are visible */",
 569         "#if PROG_LAB>0 && defined(HAS_NP)",
 570         "                       if (progstate[n][i])",
 571         "                               goto degrade;",
 572         "                       for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
 573         "                               if (progstate[n][T1->st])",
 574         "                                       goto degrade;",
 575         "#endif",
 576         "                       if (accpstate[n][i] || visstate[n][i])",
 577         "                               goto degrade;",
 578         "                       for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
 579         "                               if (accpstate[n][T1->st])",
 580         "                                       goto degrade;",
 581         "               }",
 582         "               T1 = trans[n][i];",
 583         "               if (!T1) continue;",
 584         "               g = mark_safety(T1);    /* V3.3.1 */",
 585         "               if (g < 0) goto degrade; /* global */",
 586         "               /* check if mixing of guards preserves reduction */",
 587         "               if (T1->nxt)",
 588         "               {       k = 0;",
 589         "                       for (T0 = T1; T0; T0 = T0->nxt)",
 590         "                       {       if (!(T0->atom&8))",
 591         "                                       goto degrade;",
 592         "                               for (aa = 0; aa < 2; aa++)",
 593         "                               {       j = srinc_set(T0->tpe[aa]);",
 594         "                                       if (j >= GLOBAL && j != ALPHA_F)",
 595         "                                               goto degrade;",
 596         "                                       if (T0->tpe[aa]",
 597         "                                       &&  T0->tpe[aa]",
 598         "                                       !=  T1->tpe[0])",
 599         "                                               k = 1;",
 600         "                       }       }",
 601         "                       /* g = 0;       V3.3.1 */",
 602         "                       if (k)  /* non-uniform selection */",
 603         "                       for (T0 = T1; T0; T0 = T0->nxt)",
 604         "                       for (aa = 0; aa < 2; aa++)",
 605         "                       {       j = srinc_set(T0->tpe[aa]);",
 606         "                               if (j != LOCAL)",
 607         "                               {       k = srunc(T0->tpe[aa], j);",
 608         "                                       for (h = 0; h < 6; h++)",
 609         "                                               if (T1->qu[h] == k",
 610         "                                               &&  T1->ty[h] == j)",
 611         "                                                       break;",
 612         "                                       if (h >= 6)",
 613         "                                       {       T1->qu[g%%6] = k;",
 614         "                                               T1->ty[g%%6] = j;",
 615         "                                               g++;",
 616         "                       }       }       }",
 617         "                       if (g > 6)",
 618         "                       {       T1->qu[0] = 0;  /* turn it off */",
 619         "                               printf(\"pan: warning, line %%d, \",",
 620         "                                       srcln[i]);",
 621         "                               printf(\"too many stmnt types (%%d)\",",
 622         "                                       g);",
 623         "                               printf(\" in selection\\n\");",
 624         "                         goto degrade;",
 625         "                       }",
 626         "               }",
 627         "               /* mark all options global if >=1 is global */",
 628         "               for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
 629         "                       if (!(T1->atom&8)) break;",
 630         "               if (T1)",
 631         "degrade:       for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
 632         "                       T1->atom &= ~8; /* mark as unsafe */",
 633
 634         "               /* can only mix 'r's or 's's if on same chan */",
 635         "               /* and not mixed with other local operations */",
 636         "               T1 = trans[n][i];",
 637
 638         "               if (!T1 || T1->qu[0]) continue;",
 639
 640         "               j = T1->tpe[0];",
 641         "               if (T1->nxt && T1->atom&8)",
 642         "               { if (j == 5*DELTA)",
 643         "                 {     printf(\"warning: line %%d \", srcln[i]);",
 644         "                       printf(\"mixed condition \");",
 645         "                       printf(\"(defeats reduction)\\n\");",
 646         "                       goto degrade;",
 647         "                 }",
 648         "                 for (T0 = T1; T0; T0 = T0->nxt)",
 649         "                 for (aa = 0; aa < 2; aa++)",
 650         "                 if  (T0->tpe[aa] && T0->tpe[aa] != j)",
 651         "                 {     printf(\"warning: line %%d \", srcln[i]);",
 652         "                       printf(\"[%%d-%%d] mixed %%stion \",",
 653         "                               T0->tpe[aa], j, ",
 654         "                               (j==5*DELTA)?\"condi\":\"selec\");",
 655         "                       printf(\"(defeats reduction)\\n\");",
 656         "                       printf(\"       '%%s' <-> '%%s'\\n\",",
 657         "                               T1->tp, T0->tp);",
 658         "                       goto degrade;",
 659         "               } }",
 660         "       }",
 661         "#endif",
 662         "       for (i = 1; i < m; i++)",       /* R */
 663         "       {       T2 = trans[n][i];",
 664         "               if (!T2",
 665         "               ||  T2->nxt",
 666         "               ||  strncmp(T2->tp, \".(goto)\", 7)",
 667         "               ||  !stopstate[n][i])",
 668         "                       continue;",
 669         "               stopstate[n][T2->st] = 1;",
 670         "       }",
 671         "       if (state_tables)",
 672         "       {       printf(\"proctype \");",
 673         "               if (!strcmp(procname[n], \":init:\"))",
 674         "                       printf(\"init\\n\");",
 675         "               else",
 676         "                       printf(\"%%s\\n\", procname[n]);",
 677         "               for (i = 1; i < m; i++)",
 678         "                       reach[i] = 1;",
 679         "               tagtable(n, m, is, srcln, reach);",
 680         "       } else",
 681         "       for (i = 1; i < m; i++)",
 682         "       {       int nrelse;",
 683         "               if (strcmp(procname[n], \":never:\") != 0)",
 684         "               {       for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 685         "                       {       if (T0->st == i",
 686         "                               && strcmp(T0->tp, \"(1)\") == 0)",
 687         "                               {       printf(\"error: proctype '%%s' \",",
 688         "                                               procname[n]);",
 689         "                                       printf(\"line %%d, state %%d: has un\",",
 690         "                                               srcln[i], i);",
 691         "                                       printf(\"conditional self-loop\\n\");",
 692         "                                       pan_exit(1);",
 693         "               }       }       }",
 694         "               nrelse = 0;",
 695         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 696         "               {       if (strcmp(T0->tp, \"else\") == 0)",
 697         "                               nrelse++;",
 698         "               }",
 699         "               if (nrelse > 1)",
 700         "               {       printf(\"error: proctype '%%s' state\",",
 701         "                               procname[n]);",
 702         "                       printf(\" %%d, inherits %%d\", i, nrelse);",
 703         "                       printf(\" 'else' stmnts\\n\");",
 704         "                       pan_exit(1);",
 705         "       }       }",
 706         "       if (!state_tables && strcmp(procname[n], \":never:\") == 0)",
 707         "       {       int h = 0;",
 708         "               for (i = 1; i < m; i++)",
 709         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 710         "                       if (T0->forw > h) h = T0->forw;",
 711         "               h++;",
 712         "               frm_st0 = (short *) emalloc(h * sizeof(short));",
 713         "               for (i = 1; i < m; i++)",
 714         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 715         "                       frm_st0[T0->forw] = i;",
 716         "       }",
 717         "}",
 718         "void",
 719         "imed(Trans *T, int v, int n, int j)    /* set intermediate state */",
 720         "{      progstate[n][T->st] |= progstate[n][v];",
 721         "       accpstate[n][T->st] |= accpstate[n][v];",
 722         "       stopstate[n][T->st] |= stopstate[n][v];",
 723         "       mapstate[n][j] = T->st;",
 724         "}",
 725         "void",
 726         "tagtable(int n, int m, int is, short srcln[], uchar reach[])",
 727         "{      Trans *z;\n",
 728         "       if (is >= m || !trans[n][is]",
 729         "       ||  is <= 0 || reach[is] == 0)",
 730         "               return;",
 731         "       reach[is] = 0;",
 732         "       if (state_tables)",
 733         "       for (z = trans[n][is]; z; z = z->nxt)",
 734         "               crack(n, is, z, srcln);",
 735         "       for (z = trans[n][is]; z; z = z->nxt)",
 736         "       {",
 737         "#ifdef HAS_UNLESS",
 738         "               int i, j;",
 739         "#endif",
 740         "               tagtable(n, m, z->st, srcln, reach);",
 741         "#ifdef HAS_UNLESS",
 742         "               for (i = 0; i < HAS_UNLESS; i++)",
 743         "               {       j = trans[n][is]->escp[i];",
 744         "                       if (!j) break;",
 745         "                       tagtable(n, m, j, srcln, reach);",
 746         "               }",
 747         "#endif",
 748         "       }",
 749         "}",
 750         "void",
 751         "crack(int n, int j, Trans *z, short srcln[])",
 752         "{      int i;\n",
 753         "       if (!z) return;",
 754         "       printf(\"\tstate %%3d -(tr %%3d)-> state %%3d  \",",
 755         "               j, z->forw, z->st);",
 756         "       printf(\"[id %%3d tp %%3d\", z->t_id, z->tpe[0]);",
 757         "       if (z->tpe[1]) printf(\",%%d\", z->tpe[1]);",
 758         "#ifdef HAS_UNLESS",
 759         "       if (z->e_trans)",
 760         "               printf(\" org %%3d\", z->e_trans);",
 761         "       else if (state_tables >= 2)",
 762         "       for (i = 0; i < HAS_UNLESS; i++)",
 763         "       {       if (!z->escp[i]) break;",
 764         "               printf(\" esc %%d\", z->escp[i]);",
 765         "       }",
 766         "#endif",
 767         "       printf(\"]\");",
 768         "       printf(\" [%%s%%s%%s%%s%%s] line %%d => \",",
 769         "               z->atom&6?\"A\":z->atom&32?\"D\":\"-\",",
 770         "               accpstate[n][j]?\"a\" :\"-\",",
 771         "               stopstate[n][j]?\"e\" : \"-\",",
 772         "               progstate[n][j]?\"p\" : \"-\",",
 773         "               z->atom & 8 ?\"L\":\"G\",",
 774         "               srcln[j]);",
 775         "       for (i = 0; z->tp[i]; i++)",
 776         "               if (z->tp[i] == \'\\n\')",
 777         "                       printf(\"\\\\n\");",
 778         "               else",
 779         "                       putchar(z->tp[i]);",
 780         "       if (z->qu[0])",
 781         "       {       printf(\"\\t[\");",
 782         "               for (i = 0; i < 6; i++)",
 783         "                       if (z->qu[i])",
 784         "                               printf(\"(%%d,%%d)\",",
 785         "                               z->qu[i], z->ty[i]);",
 786         "               printf(\"]\");",
 787         "       }",
 788         "       printf(\"\\n\");",
 789         "       fflush(stdout);",
 790         "}",
 791         "",
 792         "#ifdef VAR_RANGES",
 793         "#define BYTESIZE       32      /* 2^8 : 2^3 = 256:8 = 32 */",
 794         "",
 795         "typedef struct Vr_Ptr {",
 796         "       char    *nm;",
 797         "       uchar   vals[BYTESIZE];",
 798         "       struct Vr_Ptr *nxt;",
 799         "} Vr_Ptr;",
 800         "Vr_Ptr *ranges = (Vr_Ptr *) 0;",
 801         "",
 802         "void",
 803         "logval(char *s, int v)",
 804         "{      Vr_Ptr *tmp;",
 805         "",
 806         "       if (v<0 || v > 255) return;",
 807         "       for (tmp = ranges; tmp; tmp = tmp->nxt)",
 808         "               if (!strcmp(tmp->nm, s))",
 809         "                       goto found;",
 810         "       tmp = (Vr_Ptr *) emalloc(sizeof(Vr_Ptr));",
 811         "       tmp->nxt = ranges;",
 812         "       ranges = tmp;",
 813         "       tmp->nm = s;",
 814         "found:",
 815         "       tmp->vals[(v)/8] |= 1<<((v)%%8);",
 816         "}",
 817         "",
 818         "void",
 819         "dumpval(uchar X[], int range)",
 820         "{      int w, x, i, j = -1;",
 821         "",
 822         "       for (w = i = 0; w < range; w++)",
 823         "       for (x = 0; x < 8; x++, i++)",
 824         "       {",
 825         "from:          if ((X[w] & (1<<x)))",
 826         "               {       printf(\"%%d\", i);",
 827         "                       j = i;",
 828         "                       goto upto;",
 829         "       }       }",
 830         "       return;",
 831         "       for (w = 0; w < range; w++)",
 832         "       for (x = 0; x < 8; x++, i++)",
 833         "       {",
 834         "upto:          if (!(X[w] & (1<<x)))",
 835         "               {       if (i-1 == j)",
 836         "                               printf(\", \");",
 837         "                       else",
 838         "                               printf(\"-%%d, \", i-1);",
 839         "                       goto from;",
 840         "       }       }",
 841         "       if (j >= 0 && j != 255)",
 842         "               printf(\"-255\");",
 843         "}",
 844         "",
 845         "void",
 846         "dumpranges(void)",
 847         "{      Vr_Ptr *tmp;",
 848         "       printf(\"\\nValues assigned within \");",
 849         "       printf(\"interval [0..255]:\\n\");",
 850         "       for (tmp = ranges; tmp; tmp = tmp->nxt)",
 851         "       {       printf(\"\\t%%s\\t: \", tmp->nm);",
 852         "               dumpval(tmp->vals, BYTESIZE);",
 853         "               printf(\"\\n\");",
 854         "       }",
 855         "}",
 856         "#endif",
 857         0,
 858 };