sys/src/cmd/spin/pangen2.h

   1 /***** spin: pangen2.h *****/
   2
   3 /*
   4  * This file is part of the public release of Spin. It is subject to the
   5  * terms in the LICENSE file that is included in this source directory.
   6  * Tool documentation is available at http://spinroot.com
   7  */
   8
   9 static const char *Pre0[] = {
  10         "#ifdef SC",
  11         "       #define _FILE_OFFSET_BITS       64",    /* allows file sizes greater than 2Gb */
  12         "#endif",
  13         "#include <stdio.h>",
  14         "#include <signal.h>",
  15         "#include <stdlib.h>",
  16         "#include <stdarg.h>",
  17         "#include <string.h>",
  18         "#include <ctype.h>",
  19         "#include <errno.h>",
  20         "#if defined(WIN32) || defined(WIN64)",
  21                 "#include <time.h>",
  22         "#else",
  23                 "#include <unistd.h>",
  24                 "#include <sys/times.h>",
  25         "#endif",
  26         "#include <sys/types.h>",       /* defines off_t */
  27         "#include <sys/stat.h>",
  28         "#include <limits.h>",
  29         "#include <fcntl.h>",
  30
  31         "#define Offsetof(X, Y) ((ulong)(&(((X *)0)->Y)))",
  32         "#ifndef max",
  33         "#define max(a,b) (((a)<(b)) ? (b) : (a))",
  34         "#endif",
  35         "#ifndef PRINTF",
  36         "int Printf(const char *fmt, ...); /* prototype only */",
  37         "#endif",
  38         0,
  39 };
  40
  41 static const char *Separate[] = {
  42         "#ifdef COLLAPSE",
  43         "       #if (NCORE>1 && !defined(SEP_STATE)) || defined(BFS_PAR)",
  44         "               volatile ulong *ncomps; /* in shared memory */",
  45         "       #else",
  46         "               ulong ncomps[256+2];",
  47         "       #endif",
  48         "#endif",
  49         "Trans ***trans;        /* 1 ptr per state per proctype */\n",
  50         "",
  51         "#if VECTORSZ>32000",
  52         "       int P_o[MAXPROC], P_o_tmp[MAXPROC+1];",
  53         "       int Q_o[MAXQ],    Q_o_tmp[MAXPROC+1];",
  54         "",
  55         "       int *proc_offset = (int *) P_o;",
  56         "       int *q_offset    = (int *) Q_o;",
  57         "#else",
  58         "       short P_o[MAXPROC], P_o_tmp[MAXPROC+1];",
  59         "       short Q_o[MAXQ],    Q_o_tmp[MAXPROC+1];",
  60         "",
  61         "       short *proc_offset = (short *) P_o;",
  62         "       short *q_offset    = (short *) Q_o;",
  63         "#endif",
  64         "uchar P_s[MAXPROC+1], P_s_tmp[MAXPROC+1];",
  65         "uchar Q_s[MAXQ+1],    Q_s_tmp[MAXQ+1];",
  66         "uchar *proc_skip = (uchar *) P_s;",
  67         "uchar *q_skip    = (uchar *) Q_s;",
  68         "",
  69         "#ifdef TRIX",
  70         "       TRIX_v6 *freebodies;",
  71         "       TRIX_v6 *processes[MAXPROC+1];",
  72         "       TRIX_v6 *channels[MAXQ+1];",
  73         "       long _p_count[MAXPROC];",
  74         "       long _c_count[MAXPROC];",
  75         "#endif\n",
  76         "ulong  vsize;  /* vector size in bytes */",
  77         "#ifdef SVDUMP",
  78         "       int vprefix=0, svfd;    /* runtime option -pN */",
  79         "#endif",
  80         "char *tprefix = \"trail\";     /* runtime option -tsuffix */",
  81         "short boq = -1;                /* blocked_on_queue status */",
  82         "int _; /* predefined write-only variable */",
  83         "#ifdef PEG",
  84         "       long peg[NTRANS];",
  85         "#endif",
  86         0,
  87 };
  88
  89 static const char *Preamble[] = {
  90         "#ifdef RANDOMIZE",
  91         "       #define T_RAND  RANDOMIZE",
  92         "#endif",
  93         "#ifdef CNTRSTACK",
  94         "       #define onstack_now()   (LL[trpt->j6] && LL[trpt->j7])",
  95         "       #define onstack_put()    LL[trpt->j6]++; LL[trpt->j7]++",
  96         "       #define onstack_zap()    LL[trpt->j6]--; LL[trpt->j7]--",
  97         "#endif",
  98
  99         "#if !defined(SAFETY) && !defined(NOCOMP)",
 100                 /*
 101                  * V_A identifies states in the current statespace
 102                  * A_V identifies states in the 'other' statespace
 103                  * S_A remembers how many leading bytes in the sv
 104                  * are used for these markers + fairness bits
 105                  */
 106         "       #define V_A     (((now._a_t&1)?2:1) << (now._a_t&2))",
 107         "       #define A_V     (((now._a_t&1)?1:2) << (now._a_t&2))",
 108         "       int     S_A = 0;",
 109         "#else",
 110         "       #define V_A     0",
 111         "       #define A_V     0",
 112         "       #define S_A     0",
 113         "#endif",
 114
 115 "#ifdef MA",
 116         "#undef onstack_now",
 117         "#undef onstack_put",
 118         "#undef onstack_zap",
 119         "#define onstack_put()  ;",
 120         "#define onstack_zap()  g_store((char *) &now, vsize, 4)",
 121 "#else",
 122         "#if defined(FULLSTACK) && !defined(BITSTATE)",
 123         "#define onstack_put()  trpt->ostate = Lstate",
 124         "#define onstack_zap()  { \\",
 125         "       if (trpt->ostate) \\",
 126         "               trpt->ostate->tagged = \\",
 127         "               (S_A)? (trpt->ostate->tagged&~V_A) : 0; \\",
 128         "       }",
 129         "#endif",
 130 "#endif",
 131         "H_el   **H_tab, **S_Tab;",
 132         "/* #ifndef BFS_PAR */",
 133         "       H_el   *Lstate;",
 134         "/* #endif */",
 135         "Trail  *trail, *trpt;",
 136         "FILE   *efd;",
 137         "uchar  *this;",
 138         "long   maxdepth=10000;",
 139         "long   omaxdepth=10000;",
 140         "#ifdef BCS",
 141         "       /* bitflags in trpt->bcs */",
 142         "       #define B_PHASE1        1",
 143         "       #define B_PHASE2        2",
 144         "       #define B_FORCED        4",
 145         "int    sched_max = 0;",
 146         "#endif",
 147         "",
 148         "double quota;  /* time limit */",
 149         "#if NCORE>1",
 150         "       long    z_handoff = -1;",
 151         "#endif",
 152         "#ifdef SC",    /* stack cycling */
 153         "       char    *stackfile;",
 154         "#endif",
 155         "uchar  *SS, *LL;",
 156         "",
 157         "uchar  reversing = 0;",
 158         "uchar  HASH_NR = 0;",
 159         "",
 160         "double memcnt = (double) 0;",
 161         "double memlim = (double) (1<<30); /* 1 GB */",
 162         "#if NCORE>1",
 163         "double mem_reserved = (double) 0;",
 164         "#endif",
 165         "",
 166         "/* for emalloc: */",
 167         "static char *have;",
 168         "static long left = 0L;",
 169         "static double fragment = (double) 0;",
 170         "static ulong grow;",
 171         "",
 172 #if 1
 173         "unsigned int HASH_CONST[] = {",
 174         "       /* generated by hashgen 421 -- assumes 4 bytes per int */",
 175         "       0x100d4e63,     0x0fc22f87,     0xa7155c77,     0x78f2c3b9,",
 176         "       0xde32d207,     0xc27d305b,     0x1bb3fb2b,     0x2798c7a5,",
 177         "       0x9c675ffd,     0x777d9081,     0x07aef2f1,     0xae08922f,",
 178         "       0x5bd365b7,     0xed51c47b,     0x9b5aeea1,     0xbcc9d431,",
 179         "       0x396d8fff,     0xa2fd1367,     0x08616521,     0x5e84991f,",
 180         "       0x87495bc5,     0x2930039b,     0xceb6a593,     0xfe522d63,",
 181         "       0x7ff60baf,     0xf89b1fbf,     0x74c01755,     0xe0c559bf,",
 182         "       0x3669fc47,     0x8756d3bf,     0x14f78445,     0x24c41779,",
 183         "       0x0af7b129,     0xde22368d,     0x3e1c01e3,     0xaf773e49,",
 184         "       0x5b762459,     0x86d12911,     0x0953a3af,     0xb66dc23d,",
 185         "       0x96b3bd4f,     0x19b1dd51,     0xd886fbc3,     0xa7f3a025,",
 186         "       0xccb48e63,     0x87d8f027,     0x2bea270d,     0xdb0e9379,",
 187         "       0x78c09f21,     0x0cbbfe07,     0xea4bc7c3,     0x5bfbc3c9,",
 188         "       0x3c6e53fd,     0xab320cdd,     0x31041409,     0x416e7485,",
 189         "       0xe41d75fd,     0xc3c5060f,     0x201a9dc1,     0x93dee72b,",
 190         "       0x6461305f,     0xc571dec5,     0xa1fd21c5,     0xfb421ce1,",
 191         "       0x7f024b05,     0xfa518819,     0x6c9777fb,     0x0d4d9351,",
 192         "       0x08b33861,     0xccb9d0f3,     0x34112791,     0xe962d7c9,",
 193         "       0x8d742211,     0xcd9c47a1,     0x64437b69,     0x5fe40feb,",
 194         "       0x806113cb,     0x10e1d593,     0x821851b3,     0x057a1ff3,",
 195         "       0x8ededc0b,     0x90dd5b31,     0x635ff359,     0x68dbcd35,",
 196         "       0x1050ff4f,     0xdbb07257,     0x486336db,     0x83af1e75,",
 197         "       0x432f1799,     0xc1d0e7e7,     0x21f4eb5b,     0x881ec2c1,",
 198         "       0x23f3b539,     0x6cdfb80d,     0x71d474cf,     0x97d5d4a9,",
 199         "       0xf721d2e5,     0xb5ff3711,     0x3f2e58cd,     0x4e06e3d9,",
 200         "       0x7d711739,     0x927887df,     0x7d57ad71,     0x232eb767,",
 201         "       0xe3f5cc51,     0x6576b443,     0xed17bf1f,     0x8828b637,",
 202         "       0xc940f6ab,     0xc7b830ef,     0x11ed8a13,     0xaff20949,",
 203         "       0xf28a8465,     0x0da10cf9,     0xb512497d,     0x44accae1,",
 204         "       0x95e0929f,     0xe08c8901,     0xfd22d6c9,     0xb6a5c029,",
 205         "       0xaadb428d,     0x6e8a453d,     0x3d5c0195,     0x8bf4ae39,",
 206         "       0xbf83ab19,     0x3e9dac33,     0xc4df075d,     0x39472d71,",
 207         "       0xb8647725,     0x1a6d4887,     0x78a03577,     0xafd76ef7,",
 208         "       0xc1a1d6b3,     0x1afb33c5,     0x87896299,     0x5cc992ef,",
 209         "       0x7f805d0d,     0x089a039b,     0xa353cc27,     0x57b296b3,",
 210         "       0x52badec9,     0xc916e431,     0x09171957,     0x14996d51,",
 211         "       0xe87e32c7,     0xb4fdbb5d,     0xdd216a03,     0x4ddd3fff,",
 212         "       0x767d5c57,     0x79c97509,     0xab70543b,     0xc5feca4f,",
 213         "       0x8eb37b89,     0x20a2cefd,     0xf4b00b91,     0xf166593d,",
 214         "       0x7bf50f65,     0x753e6c8b,     0xfb5b81dd,     0xf2d45ef5,",
 215         "       0x9741c04f,     0x300da48d,     0x01dc4121,     0xa112cd47,",
 216         "       0x0223b24b,     0xa89fbce7,     0x681e1f7b,     0xe7c6aedf,",
 217         "       0x1fd3d523,     0x561ba723,     0xf54042fb,     0x1a516751,",
 218         "       0xcd085bd5,     0xe74246d5,     0x8b170b5d,     0x249985e9,",
 219         "       0x5b4d9cf7,     0xe9912323,     0x5fc0f339,     0x41f8f051,",
 220         "       0x8a296fb1,     0x62909f51,     0x2c05d695,     0x095efccb,",
 221         "       0xa91574f1,     0x0f5cc6c3,     0x23a2ca2b,     0xc6053ec1,",
 222         "       0xeb19e081,     0x3d1b3997,     0xb0c5f3cd,     0xe5d85b35,",
 223         "       0x1cb1bdf1,     0x0c8f278f,     0x518249c3,     0x9f61b68d,",
 224         "       0xade0919d,     0x779e29c3,     0xdbac9485,     0x2ce149a9,",
 225         "       0x254c2409,     0x205b34fb,     0xc8ab1a89,     0x6b4a2585,",
 226         "       0x2303d94b,     0x8fa186b9,     0x49826da5,     0xd23a37ad,",
 227         "       0x680b18c9,     0xa46fbd7f,     0xe42c2cf9,     0xf7cfcb5f,",
 228         "       0xb4842b8b,     0xe483780d,     0x66cf756b,     0x3eb73781,",
 229         "       0x41ca17a5,     0x59f91b0f,     0x92fb67d9,     0x0a5c330f,",
 230         "       0x46013fdb,     0x3b0634af,     0x9024f533,     0x96a001a7,",
 231         "       0x15bcd793,     0x3a311fb1,     0x78913b8b,     0x9d4a5ddf,",
 232         "       0x33189b31,     0xa99e8283,     0xf7cb29e9,     0x12d64a27,",
 233         "       0xeda770ff,     0xa7320297,     0xbd3c14a5,     0x96d0156f,",
 234         "       0x0115db95,     0x7f79f52b,     0xa6d52521,     0xa063d4bd,",
 235         "       0x9cb5e039,     0x42cf8195,     0xcb716835,     0x1bc21273,",
 236         "       0x5a67ad27,     0x4b3b0545,     0x162cda67,     0x0489166b,",
 237         "       0x85fd06a9,     0x562b037d,     0x995bc1f3,     0xe144e78b,",
 238         "       0x1e749f69,     0xa36df057,     0xcfee1667,     0x8c4116b7,",
 239         "       0x94647fe3,     0xe6899df7,     0x6d218981,     0xf1069079,",
 240         "       0xd1851a33,     0xf424fc83,     0x24467005,     0xad8caf59,",
 241         "       0x1ae5da13,     0x497612f9,     0x10f6d1ef,     0xeaf4ff05,",
 242         "       0x405f030b,     0x693b041d,     0x2065a645,     0x9fec71b3,",
 243         "       0xc3bd1b0f,     0xf29217a3,     0x0f25e15d,     0xd48c2b97,",
 244         "       0xce8acf2d,     0x0629489b,     0x1a5b0e01,     0x32d0c059,",
 245         "       0x2d3664bf,     0xc45f3833,     0xd57f551b,     0xbdd991c5,",
 246         "       0x9f97da9f,     0xa029c2a9,     0x5dd0cbdf,     0xe237ba41,",
 247         "       0x62bb0b59,     0x93e7d037,     0x7e495619,     0x51b8282f,",
 248         "       0x853e8ef3,     0x9b8abbeb,     0x055f66f9,     0x2736f7e5,",
 249         "       0x8d7e6353,     0x143abb65,     0x4e2bb5b3,     0x872e1adf,",
 250         "       0x8fcac853,     0xb7cf6e57,     0x12177f3d,     0x1d2da641,",
 251         "       0x07856425,     0xc0ed53dd,     0x252271d9,     0x79874843,",
 252         "       0x0aa8c9b5,     0x7e804f93,     0x2d080e09,     0x3929ddfd,",
 253         "       0x36433dbd,     0xd6568c17,     0xe624e939,     0xb33189ef,",
 254         "       0x29e68bff,     0x8aae2433,     0xe6335499,     0xc5facd9d,",
 255         "       0xbd5afc65,     0x7a584fa7,     0xab191435,     0x64bbdeef,",
 256         "       0x9f5cd8e1,     0xb3a1be05,     0xbd0c1753,     0xb00e2c7f,",
 257         "       0x6a96e315,     0x96a31589,     0x660af5af,     0xc0438d43,",
 258         "       0x17637373,     0x6460e8df,     0x7d458de9,     0xd76b923f,",
 259         "       0x316f045f,     0x3ccbd035,     0x63f64d81,     0xd990d969,",
 260         "       0x7c860a93,     0x99269ff7,     0x6fbcac8f,     0xd8cc562b,",
 261         "       0x67141071,     0x09f85ea3,     0x1298f2dd,     0x41fa86e5,",
 262         "       0xce1d7cf5,     0x6b232c9d,     0x8f093d4b,     0x3203ad4b,",
 263         "       0x07d70d5f,     0x38c44c75,     0x0887c9ef,     0x1833acf5,",
 264         "       0xa3607f85,     0x7d367573,     0x0ea4ffc3,     0xad2d09c1,",
 265         "       0x7a1e664f,     0xef41dff5,     0x03563491,     0x67f30a1f,",
 266         "       0x5ce5f9ef,     0xa2487a27,     0xe5077957,     0x9beb36fd,",
 267         "       0x16e41251,     0x216799ef,     0x07181f8d,     0xc191c3cf,",
 268         "       0xba21cab5,     0x73944eb7,     0xdf9eb69d,     0x5fef6cfd,",
 269         "       0xd750a6f5,     0x04f3fa43,     0x7cb2d063,     0xd3bdb369,",
 270         "       0x35f35981,     0x9f294633,     0x5e293517,     0x70e51d05,",
 271         "       0xf8db618d,     0x66ee05db,     0x835eaa77,     0x166a02c3,",
 272         "       0xb516f283,     0x94102293,     0x1ace50a5,     0x64072651,",
 273         "       0x66df7b75,     0x02e1b261,     0x8e6a73b9,     0x19dddfe7,",
 274         "       0xd551cf39,     0x391c17cb,     0xf4304de5,     0xcd67b8d1,",
 275         "       0x25873e8d,     0x115b4c71,     0x36e062f3,     0xaec0c7c9,",
 276         "       0xd929f79d,     0x935a661b,     0xda762b47,     0x170bd76b,",
 277         "       0x1a955cb5,     0x341fb0ef,     0x7f366cef,     0xc98f60c7,",
 278         "       0xa4181af3,     0xa94a8837,     0x5fa3bc43,     0x11c638c1,",
 279         "       0x4e66fabb,     0x30ab85cf,     0x250704ef,     0x8bf3bc07,",
 280         "       0x6d2cd5ab,     0x613ef9c3,     0xb8e62149,     0x0404fd91,",
 281         "       0xa04fd9b1,     0xa5e389eb,     0x9543bd23,     0xad6ca1f9,",
 282         "       0x210c49ab,     0xf8e9532b,     0x854fba89,     0xdc7fc6bb,",
 283         "       0x48a051a7,     0x6b2f383b,     0x61a4b433,     0xd3af231b,",
 284         "       0xc5023fc7,     0xa5aa85df,     0xa0cd1157,     0x4206f64d,",
 285         "       0x3fea31c3,     0x62d510a1,     0x13988957,     0x6a11a033,",
 286         "       0x46f2a3b7,     0x2784ef85,     0x229eb9eb,     0x9c0c3053,",
 287         "       0x5b7ead39,     0x82ae9afb,     0xf99e9fb3,     0x914b6459,",
 288         "       0xaf05edd7,     0xc82710dd,     0x8fc1ea1f,     0x7e0d7a8d,",
 289         "       0x7c7592e9,     0x65321017,     0xea57553f,     0x4aeb49ff,",
 290         "       0x5239ae4d,     0x4b4b4585,     0x94091c21,     0x7eaaf4cb,",
 291         "       0x6b489d6f,     0xecb9c0c3,     0x29a7af63,     0xaf117a0d,",
 292         "       0x969ea6cd,     0x7658a34d,     0x5fc0bba9,     0x26e99b7f,",
 293         "       0x7a6f260f,     0xe37c34f1,     0x1a1569bb,     0xc3bc7371,",
 294         "       0x8567543d,     0xad0c46a9,     0xa1264fd9,     0x16f10b29,",
 295         "       0x5e00dd3b,     0xf85b6bcd,     0xa2d32d8b,     0x4a3c8d43,",
 296         "       0x6b33b959,     0x4fd1e6c9,     0x7938b8a9,     0x1ec795c7,",
 297         "       0xe2ef3409,     0x83c16b9d,     0x0d3fd9eb,     0xeb461ad7,",
 298         "       0xb09c831d,     0xaf052001,     0x7911164d,     0x1a9dc191,",
 299         "       0xb52a0815,     0x0f732157,     0xc68c4831,     0x12cf3cbb };",
 300 #else
 301         "unsigned int HASH_CONST[] = {",
 302         "       /* asuming 4 bytes per int */",
 303         "       0x100d4e63,     0x0fc22f87,",
 304         "       0x3ff0c3ff,     0x38e84cd7,",
 305         "       0x02b148e9,     0x98b2e49d,",
 306         "       0xb616d379,     0xa5247fd9,",
 307         "       0xbae92a15,     0xb91c8bc5,",
 308         "       0x8e5880f3,     0xacd7c069,",
 309         "       0xb4c44bb3,     0x2ead1fb7,",
 310         "       0x8e428171,     0xdbebd459,",
 311         "       0x00400007,     0x04c11db7,",
 312         "       0x828ae611,     0x6cb25933,",
 313         "       0x86cdd651,     0x9e8f5f21,",
 314         "       0xd5f8d8e7,     0x9c4e956f,",
 315         "       0xb5cf2c71,     0x2e805a6d,",
 316         "       0x33fc3a55,     0xaf203ed1,",
 317         "       0xe31f5909,     0x5276db35,",
 318         "       0x0c565ef7,     0x273d1aa5,",
 319         "       0x8923b1dd,     0xa9acaac5,",
 320         "       0xd1f69207,     0xedfd944b,",
 321         "       0x9a68e46b,     0x5355e13f,",
 322         "       0x7eeb44f9,     0x932beea9,",
 323         "       0x330c4cd3,     0x87f34e5f,",
 324         "       0x1b5851b7,     0xb9ca6447,",
 325         "       0x58f96a8f,     0x1b3b5307,",
 326         "       0x31c387b3,     0xf35f0f35,",
 327         "       0xa0acc4df,     0xf3140303,",
 328         "       0x2446245d,     0xe4b8f4ef,",
 329         "       0x5c007383,     0x68e648af,",
 330         "       0x1814fba7,     0xcdf731b5,",
 331         "       0xd09ccb4b,     0xb92d0eff,",
 332         "       0xcc3c6b67,     0xd3af6a57,",
 333         "       0xf44fc3f5,     0x5bb67623,",
 334         "       0xaeb9c953,     0x5e0ac739,",
 335         "       0x3a7fda09,     0x5edf39eb,",
 336         "       0x661eefd9,     0x6423f0d1,",
 337         "       0x910fe413,     0x9ec92297,",
 338         "       0x4bd8159d,     0xa7b16ee1,",
 339         "       0x89d484e9,     0x7f305cb3,",
 340         "       0xc5f303e7,     0x415deeef,",
 341         "       0x09986f89,     0x7e9c4117,",
 342         "       0x0b7cbedb,     0xf9ed7561,",
 343         "       0x7a20ac99,     0xf05adef3,",
 344         "       0x5893d75b,     0x44d73327,",
 345         "       0xb583c873,     0x324d2145,",
 346         "       0x7fa3829b,     0xe4b47a23,",
 347         "       0xe256d94f,     0xb1fd8959,",
 348         "       0xe561a321,     0x1435ac09,",
 349         "       0xdd62408b,     0x02ec0bcb,",
 350         "       0x5469b785,     0x2f4f50bb,",
 351         "       0x20f19395,     0xf96ba085,",
 352         "       0x2381f937,     0x768e2a11 };",
 353 #endif
 354         "",
 355         "#if NCORE>1",
 356         "extern int core_id;",
 357         "#endif",
 358         "long   mreached=0;",
 359         "int done=0, errors=0, Nrun=1;",
 360         "int    c_init_done=0;",
 361         "char   *c_stack_start = (char *) 0;",
 362         "double nstates=0, nlinks=0, truncs=0, truncs2=0;",
 363         "double nlost=0, nShadow=0, hcmp=0, ngrabs=0;",
 364         "#ifdef BFS_PAR",
 365         "extern ulong bfs_punt;",
 366         "#endif",
 367         "#ifdef PUTPID",
 368         "char *progname;",
 369         "#endif",
 370         "#if defined(ZAPH) && defined(BITSTATE)",
 371         "double zstates = 0;",
 372         "#endif",
 373         "/* int c_init_run; */",
 374         "#ifdef REVERSE",
 375         "       #define P_REVERSE",
 376         "#endif",
 377         "#ifdef T_REVERSE",
 378         "       int     t_reverse = 1;", /* can be modified with a parameter */
 379         "#else",
 380         "       int     t_reverse = 0;",
 381         "#endif",
 382         "#ifdef BFS",
 383         "double midrv=0, failedrv=0, revrv=0;",
 384         "#endif",
 385         "ulong  nr_states=0; /* nodes in DFA */",
 386         "long   Fa=0, Fh=0, Zh=0, Zn=0;",
 387         "long   PUT=0, PROBE=0, ZAPS=0;",
 388         "long   Ccheck=0, Cholds=0;",
 389         "int    a_cycles=0, upto=1, strict=0, verbose = 0, signoff = 0;",
 390         "#ifdef HAS_CODE",
 391         "int    gui = 0, coltrace = 0, readtrail = 0;",
 392         "int    whichtrail = 0, whichclaim = -1, onlyproc = -1, silent = 0;",
 393         "char   *claimname;",
 394         "#endif",
 395         "int    state_tables=0, fairness=0, no_rck=0, Nr_Trails=0, dodot=0;",
 396         "char   simvals[256];",
 397         "#ifndef INLINE",
 398         "int    TstOnly=0;",
 399         "#endif",
 400         "ulong mask, nmask;",
 401         "#ifdef BITSTATE",
 402         "int    ssize=27;       /* 16 Mb */",
 403         "#else",
 404         "int    ssize=24;       /* 16M slots */",
 405         "#endif",
 406         "int    hmax=0, svmax=0, smax=0;",
 407         "int    Maxbody=0, XX;",
 408         "uchar  *noptr, *noqptr;        /* used by Pptr(x) and Qptr(x) */",
 409         "#ifdef VAR_RANGES",
 410         "void logval(char *, int);",
 411         "void dumpranges(void);",
 412         "#endif",
 413
 414         "#ifdef MA",
 415         "#define INLINE_REV",
 416         "extern void dfa_init(unsigned short);",
 417         "extern int  dfa_member(ulong);",
 418         "extern int  dfa_store(uchar *);",
 419         "unsigned int   maxgs = 0;",
 420         "#endif",
 421         "",
 422         "#ifdef ALIGNED",
 423         "       State   comp_now __attribute__ ((aligned (8)));",
 424         "       /* gcc 64-bit aligned for Itanium2 systems */",
 425         "       /* MAJOR runtime penalty if not used on those systems */",
 426         "#else",
 427         "       State   comp_now;       /* compressed state vector */",
 428         "#endif",
 429         "",
 430         "#ifndef HC",
 431         "       #ifdef BFS_PAR",
 432         "               State tmp_msk;",
 433         "       #endif",
 434         "       State   comp_msk;",
 435         "       uchar   *Mask = (uchar *) &comp_msk;",
 436         "#endif",
 437         "#ifdef COLLAPSE",
 438         "       State   comp_tmp;",
 439         "       static char     *scratch = (char *) &comp_tmp;",
 440         "#endif",
 441         "",
 442         "_Stack *stack;         /* for queues, processes */",
 443         "Svtack *svtack;        /* for old state vectors */",
 444         "#ifdef BITSTATE",
 445         "static unsigned int hfns = 3;  /* new default */",
 446         "#endif",
 447         "static ulong j1_spin, j2_spin; /* 5.2.1: avoid nameclash with math.h */",
 448         "static ulong j3_spin, j4_spin;",
 449         "ulong K1, K2;",
 450         "#ifdef BITSTATE",
 451         "long udmem;",
 452         "#endif",
 453         "#ifndef BFS_PAR",
 454         "static long    A_depth = 0;",
 455         "#endif",
 456         "long   depth = 0;",
 457         "long depthfound = -1;  /* loop detection */",
 458         /* depth: not static to support -S2, but possible clash with embedded code */
 459         "#if NCORE>1",
 460         "long nr_handoffs = 0;",
 461         "#endif",
 462         "uchar  warned = 0, iterative = 0, exclusive = 0, like_java = 0, every_error = 0;",
 463         "uchar  noasserts = 0, noends = 0, bounded = 0;",
 464         "uint   s_rand = 12345; /* default seed */",
 465
 466         "#if SYNC>0 && ASYNC==0",
 467         "void set_recvs(void);",
 468         "int  no_recvs(int);",
 469         "#endif",
 470         "#if SYNC",
 471         "#define IfNotBlocked   if (boq != -1) continue;",
 472         "#define UnBlock        boq = -1",
 473         "#else",
 474         "#define IfNotBlocked   /* cannot block */",
 475         "#define UnBlock        /* don't bother */",
 476         "#endif\n",
 477         "#ifdef BITSTATE",
 478         "int (*b_store)(char *, int);",
 479         "int bstore_reg(char *, int);",
 480         "int bstore_mod(char *, int);",
 481         "#endif",
 482         "",
 483         "void dfs_uerror(char *);",
 484         "void dfs_Uerror(char *);",
 485         "#ifdef BFS_PAR",
 486         "void bfs_uerror(char *);",
 487         "void bfs_Uerror(char *);",
 488         "#endif",
 489         "void (*uerror)(char *);",
 490         "void (*Uerror)(char *);",
 491         "void (*hasher)(uchar *, int);",
 492         "void (*o_hash)(uchar *, int, int);",
 493         "void d_hash(uchar *, int);",
 494         "void m_hash(uchar *, int);",
 495         "void d_sfh(uchar *, int);",
 496         "void o_hash32(uchar *, int, int);",
 497         "void o_hash64(uchar *, int, int);",
 498         "",
 499         "void active_procs(void);",
 500         "void cleanup(void);",
 501         "void do_the_search(void);",
 502         "void find_shorter(int);",
 503         "void iniglobals(int);",
 504         "void stopped(int);",
 505         "void wrapup(void);",
 506         "int *grab_ints(int);",
 507         "void ungrab_ints(int *, int);",
 508         0,
 509 };
 510
 511 static const char *Tail[] = {
 512         "Trans *",
 513         "settr( int t_id, int a, int b, int c, int d,",
 514         "       char *t, int g, int tpe0, int tpe1)",
 515         "{      Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n",
 516         "       tmp->atom  = a&(6|32);  /* only (2|8|32) have meaning */",
 517         "       if (!g) tmp->atom |= 8; /* no global references */",
 518         "       tmp->st    = b;",
 519         "       tmp->tpe[0] = tpe0;",
 520         "       tmp->tpe[1] = tpe1;",
 521         "       tmp->tp    = t;",
 522         "       tmp->t_id  = t_id;",
 523         "       tmp->forw  = c;",
 524         "       tmp->back  = d;",
 525         "       return tmp;",
 526         "}\n",
 527         "Trans *",
 528         "cpytr(Trans *a)",
 529         "{      Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n",
 530         "       int i;",
 531         "       tmp->atom  = a->atom;",
 532         "       tmp->st    = a->st;",
 533         "#ifdef HAS_UNLESS",
 534         "       tmp->e_trans = a->e_trans;",
 535         "       for (i = 0; i < HAS_UNLESS; i++)",
 536         "               tmp->escp[i] = a->escp[i];",
 537         "#endif",
 538         "       tmp->tpe[0] = a->tpe[0];",
 539         "       tmp->tpe[1] = a->tpe[1];",
 540         "       for (i = 0; i < 6; i++)",
 541         "       {       tmp->qu[i] = a->qu[i];",
 542         "               tmp->ty[i] = a->ty[i];",
 543         "       }",
 544         "       tmp->tp    = (char *) emalloc(strlen(a->tp)+1);",
 545         "       strcpy(tmp->tp, a->tp);",
 546         "       tmp->t_id  = a->t_id;",
 547         "       tmp->forw  = a->forw;",
 548         "       tmp->back  = a->back;",
 549         "       return tmp;",
 550         "}\n",
 551         "#ifndef NOREDUCE",
 552         "int",
 553         "srinc_set(int n)",
 554         "{      if (n <= 2) return LOCAL;",
 555         "       if (n <= 2+  DELTA) return Q_FULL_F; /* 's' or nfull  */",
 556         "       if (n <= 2+2*DELTA) return Q_EMPT_F; /* 'r' or nempty */",
 557         "       if (n <= 2+3*DELTA) return Q_EMPT_T; /* empty */",
 558         "       if (n <= 2+4*DELTA) return Q_FULL_T; /* full  */",
 559         "       if (n ==   5*DELTA) return GLOBAL;",
 560         "       if (n ==   6*DELTA) return TIMEOUT_F;",
 561         "       if (n ==   7*DELTA) return ALPHA_F;",
 562         "       Uerror(\"cannot happen srinc_class\");",
 563         "       return BAD;",
 564         "}",
 565         "int",
 566         "srunc(int n, int m)",
 567         "{      switch(m) {",
 568         "       case Q_FULL_F: return n-2;",
 569         "       case Q_EMPT_F: return n-2-DELTA;",
 570         "       case Q_EMPT_T: return n-2-2*DELTA;",
 571         "       case Q_FULL_T: return n-2-3*DELTA;",
 572         "       case ALPHA_F:",
 573         "       case TIMEOUT_F: return 257; /* non-zero, and > MAXQ */",
 574         "       }",
 575         "       Uerror(\"cannot happen srunc\");",
 576         "       return 0;",
 577         "}",
 578         "#endif",
 579         "int cnt;",
 580         "#ifdef HAS_UNLESS",
 581         "int",
 582         "isthere(Trans *a, int b)", /* is b already in a's list? */
 583         "{      Trans *t;",
 584         "       for (t = a; t; t = t->nxt)",
 585         "               if (t->t_id == b)",
 586         "                       return 1;",
 587         "       return 0;",
 588         "}",
 589         "#endif",
 590         "#ifndef NOREDUCE",
 591         "int",
 592         "mark_safety(Trans *t) /* for conditional safety */",
 593         "{      int g = 0, i, j, k;",
 594         "",
 595         "       if (!t) return 0;",
 596         "       if (t->qu[0])",
 597         "               return (t->qu[1])?2:1;  /* marked */",
 598         "",
 599         "       for (i = 0; i < 2; i++)",
 600         "       {       j = srinc_set(t->tpe[i]);",
 601         "               if (j >= GLOBAL && j != ALPHA_F)",
 602         "                       return -1;",
 603         "               if (j != LOCAL)",
 604         "               {       k = srunc(t->tpe[i], j);",
 605         "                       if (g == 0",
 606         "                       ||  t->qu[0] != k",
 607         "                       ||  t->ty[0] != j)",
 608         "                       {       t->qu[g] = k;",
 609         "                               t->ty[g] = j;",
 610         "                               g++;",
 611         "       }       }       }",
 612         "       return g;",
 613         "}",
 614         "#endif",
 615         "void",
 616         "retrans(int n, int m, int is, short srcln[], uchar reach[], uchar lpstate[])",
 617         "       /* process n, with m states, is=initial state */",
 618         "{      Trans *T0, *T1, *T2, *T3;",
 619         "       Trans *T4, *T5; /* t_reverse or has_unless */",
 620         "       int i;",
 621         "#if defined(HAS_UNLESS) || !defined(NOREDUCE)",
 622         "       int k;",
 623         "#endif",
 624         "#ifndef NOREDUCE",
 625         "       int g, h, j, aa;",
 626         "#endif",
 627         "#ifdef HAS_UNLESS",
 628         "       int p;",
 629         "#endif",
 630         "       if (state_tables >= 4)",
 631         "       {       printf(\"STEP 1 %%s\\n\", ",
 632         "                       procname[n]);",
 633         "               for (i = 1; i < m; i++)",
 634         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 635         "                       crack(n, i, T0, srcln);",
 636         "               return;",
 637         "       }",
 638         "       do {",
 639         "               for (i = 1, cnt = 0; i < m; i++)",
 640         "               {       T2 = trans[n][i];",
 641         "                       T1 = T2?T2->nxt:(Trans *)0;",
 642         "/* prescan: */         for (T0 = T1; T0; T0 = T0->nxt)",
 643         "/* choice in choice */ {       if (T0->st && trans[n][T0->st]",
 644         "                               &&  trans[n][T0->st]->nxt)",
 645         "                                       break;",
 646         "                       }",
 647         "#if 0",
 648         "               if (T0)",
 649         "               printf(\"\\tstate %%d / %%d: choice in choice\\n\",",
 650         "               i, T0->st);",
 651         "#endif",
 652         "                       if (T0)",
 653         "                       for (T0 = T1; T0; T0 = T0->nxt)",
 654         "                       {       T3 = trans[n][T0->st];",
 655         "                               if (!T3->nxt)",
 656         "                               {       T2->nxt = cpytr(T0);",
 657         "                                       T2 = T2->nxt;",
 658         "                                       imed(T2, T0->st, n, i);",
 659         "                                       continue;",
 660         "                               }",
 661         "                               do {    T3 = T3->nxt;",
 662         "                                       T2->nxt = cpytr(T3);",
 663         "                                       T2 = T2->nxt;",
 664         "                                       imed(T2, T0->st, n, i);",
 665         "                               } while (T3->nxt);",
 666         "                               cnt++;",
 667         "                       }",
 668         "               }",
 669         "       } while (cnt);",
 670
 671         "       if (state_tables >= 3)",
 672         "       {       printf(\"STEP 2 %%s\\n\", ",
 673         "                       procname[n]);",
 674         "               for (i = 1; i < m; i++)",
 675         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 676         "                       crack(n, i, T0, srcln);",
 677         "               return;",
 678         "       }",
 679         "       for (i = 1; i < m; i++)",
 680         "       {       if (trans[n][i] && trans[n][i]->nxt) /* optimize */",
 681         "               {       T1 = trans[n][i]->nxt;",
 682         "#if 0",
 683         "                       printf(\"\\t\\tpull %%d (%%d) to %%d\\n\",",
 684         "                       T1->st, T1->forw, i);",
 685         "#endif",               /* pull linenumber ref as well: */
 686         "                       srcln[i] = srcln[T1->st];       /* Oyvind Teig, 5.2.0 */",
 687         "",
 688         "                       if (!trans[n][T1->st]) continue;",
 689         "                       T0 = cpytr(trans[n][T1->st]);",
 690         "                       trans[n][i] = T0;",
 691         "                       reach[T1->st] = 1;",
 692         "                       imed(T0, T1->st, n, i);",
 693         "                       for (T1 = T1->nxt; T1; T1 = T1->nxt)",
 694         "                       {",
 695         "#if 0",
 696         "                       printf(\"\\t\\tpull %%d (%%d) to %%d\\n\",",
 697         "                               T1->st, T1->forw, i);",
 698         "#endif",
 699         "               /*              srcln[i] = srcln[T1->st];  gh: not useful */",
 700         "                               if (!trans[n][T1->st]) continue;",
 701         "                               T0->nxt = cpytr(trans[n][T1->st]);",
 702         "                               T0 = T0->nxt;",
 703         "                               reach[T1->st] = 1;",
 704         "                               imed(T0, T1->st, n, i);",
 705         "       }       }       }",
 706         "       if (state_tables >= 2)",
 707         "       {       printf(\"STEP 3 %%s\\n\", ",
 708         "                       procname[n]);",
 709         "               for (i = 1; i < m; i++)",
 710         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 711         "                       crack(n, i, T0, srcln);",
 712         "               return;",
 713         "       }",
 714         "#ifdef HAS_UNLESS",
 715         "       for (i = 1; i < m; i++)",
 716         "       {       if (!trans[n][i]) continue;",
 717         "               /* check for each state i if an",
 718         "                * escape to some state p is defined",
 719         "                * if so, copy and mark p's transitions",
 720         "                * and prepend them to the transition-",
 721         "                * list of state i",
 722         "                */",
 723         "        if (!like_java) /* the default */",
 724         "        {      for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 725         "               for (k = HAS_UNLESS-1; k >= 0; k--)",
 726         "               {       if (p = T0->escp[k])",
 727         "                       for (T1 = trans[n][p]; T1; T1 = T1->nxt)",
 728         "                       {       if (isthere(trans[n][i], T1->t_id))",
 729         "                                       continue;",
 730         "                               T2 = cpytr(T1);",
 731         "                               T2->e_trans = p;",
 732         "                               T2->nxt = trans[n][i];",
 733         "                               trans[n][i] = T2;",
 734         "               }       }",
 735         "        } else /* outermost unless checked first */",
 736         "        {      T4 = T3 = (Trans *) 0;",
 737         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 738         "               for (k = HAS_UNLESS-1; k >= 0; k--)",
 739         "               {       if (p = T0->escp[k])",
 740         "                       for (T1 = trans[n][p]; T1; T1 = T1->nxt)",
 741         "                       {       if (isthere(trans[n][i], T1->t_id))",
 742         "                                       continue;",
 743         "                               T2 = cpytr(T1);",
 744         "                               T2->nxt = (Trans *) 0;",
 745         "                               T2->e_trans = p;",
 746         "                               if (T3) T3->nxt = T2;",
 747         "                               else    T4 = T2;",
 748         "                               T3 = T2;",
 749         "               }       }",
 750         "               if (T4)",
 751         "               {       T3->nxt = trans[n][i];",
 752         "                       trans[n][i] = T4;",
 753         "               }",
 754         "        }",
 755         "       }",
 756         "#endif",
 757
 758         "#ifndef NOREDUCE",
 759         "       for (i = 1; i < m; i++)",
 760         "       {       if (a_cycles)",
 761         "               { /* moves through these states are visible */",
 762         "       #if PROG_LAB>0 && defined(HAS_NP)",
 763         "                       if (progstate[n][i])",
 764         "                               goto degrade;",
 765         "                       for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
 766         "                               if (progstate[n][T1->st])",
 767         "                                       goto degrade;",
 768         "       #endif",
 769         "                       if (accpstate[n][i] || visstate[n][i])",
 770         "                               goto degrade;",
 771         "                       for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
 772         "                               if (accpstate[n][T1->st])",
 773         "                                       goto degrade;",
 774         "               }",
 775         "               T1 = trans[n][i];",
 776         "               if (!T1) continue;",
 777         "               g = mark_safety(T1);    /* V3.3.1 */",
 778         "               if (g < 0) goto degrade; /* global */",
 779         "               /* check if mixing of guards preserves reduction */",
 780         "               if (T1->nxt)",
 781         "               {       k = 0;",
 782         "                       for (T0 = T1; T0; T0 = T0->nxt)",
 783         "                       {       if (!(T0->atom&8))",
 784         "                                       goto degrade;",
 785         "                               for (aa = 0; aa < 2; aa++)",
 786         "                               {       j = srinc_set(T0->tpe[aa]);",
 787         "                                       if (j >= GLOBAL && j != ALPHA_F)",
 788         "                                               goto degrade;",
 789         "                                       if (T0->tpe[aa]",
 790         "                                       &&  T0->tpe[aa]",
 791         "                                       !=  T1->tpe[0])",
 792         "                                               k = 1;",
 793         "                       }       }",
 794         "                       /* g = 0;       V3.3.1 */",
 795         "                       if (k)  /* non-uniform selection */",
 796         "                       for (T0 = T1; T0; T0 = T0->nxt)",
 797         "                       for (aa = 0; aa < 2; aa++)",
 798         "                       {       j = srinc_set(T0->tpe[aa]);",
 799         "                               if (j != LOCAL)",
 800         "                               {       k = srunc(T0->tpe[aa], j);",
 801         "                                       for (h = 0; h < 6; h++)",
 802         "                                               if (T1->qu[h] == k",
 803         "                                               &&  T1->ty[h] == j)",
 804         "                                                       break;",
 805         "                                       if (h >= 6)",
 806         "                                       {       T1->qu[g%%6] = k;",
 807         "                                               T1->ty[g%%6] = j;",
 808         "                                               g++;",
 809         "                       }       }       }",
 810         "                       if (g > 6)",
 811         "                       {       T1->qu[0] = 0;  /* turn it off */",
 812         "                               printf(\"pan: warning, line %%d, \",",
 813         "                                       srcln[i]);",
 814         "                               printf(\"too many stmnt types (%%d)\",",
 815         "                                       g);",
 816         "                               printf(\" in selection\\n\");",
 817         "                         goto degrade;",
 818         "                       }",
 819         "               }",
 820         "               /* mark all options global if >=1 is global */",
 821         "               for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
 822         "                       if (!(T1->atom&8)) break;",
 823         "               if (T1)",
 824         "degrade:       for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
 825         "                       T1->atom &= ~8; /* mark as unsafe */",
 826
 827         "               /* can only mix 'r's or 's's if on same chan */",
 828         "               /* and not mixed with other local operations */",
 829         "               T1 = trans[n][i];",
 830
 831         "               if (!T1 || T1->qu[0]) continue;",
 832
 833         "               j = T1->tpe[0];",
 834         "               if (T1->nxt && T1->atom&8)",
 835         "               { if (j == 5*DELTA)",
 836         "                 {     printf(\"warning: line %%d \", srcln[i]);",
 837         "                       printf(\"mixed condition \");",
 838         "                       printf(\"(defeats reduction)\\n\");",
 839         "                       goto degrade;",
 840         "                 }",
 841         "                 for (T0 = T1; T0; T0 = T0->nxt)",
 842         "                 for (aa = 0; aa < 2; aa++)",
 843         "                 if  (T0->tpe[aa] && T0->tpe[aa] != j)",
 844         "                 {     printf(\"warning: line %%d \", srcln[i]);",
 845         "                       printf(\"[%%d-%%d] mixed %%stion \",",
 846         "                               T0->tpe[aa], j, ",
 847         "                               (j==5*DELTA)?\"condi\":\"selec\");",
 848         "                       printf(\"(defeats reduction)\\n\");",
 849         "                       printf(\"       '%%s' <-> '%%s'\\n\",",
 850         "                               T1->tp, T0->tp);",
 851         "                       goto degrade;",
 852         "               } }",
 853         "       }",
 854         "#endif",
 855         "       for (i = 1; i < m; i++)",       /* R */
 856         "       {       T2 = trans[n][i];",
 857         "               if (!T2",
 858         "               ||  T2->nxt",
 859         "               ||  strncmp(T2->tp, \".(goto)\", 7)",
 860         "               ||  !stopstate[n][i])",
 861         "                       continue;",
 862         "               stopstate[n][T2->st] = 1;",
 863         "       }",
 864         "       if (state_tables && !verbose)",
 865         "       {       if (dodot)",
 866         "               {       char buf[256], *q = buf, *p = procname[n];",
 867         "                       while (*p != '\\0')",
 868         "                       {       if (*p != ':')",
 869         "                               {       *q++ = *p;",
 870         "                               }",
 871         "                               p++;",
 872         "                       }",
 873         "                       *q = '\\0';",
 874         "                       printf(\"digraph \");",
 875         "                       switch (Btypes[n]) {",
 876         "                       case I_PROC:  printf(\"init {\\n\"); break;",
 877         "                       case N_CLAIM: printf(\"claim_%%s {\\n\", buf); break;",
 878         "                       case E_TRACE: printf(\"notrace {\\n\"); break;",
 879         "                       case N_TRACE: printf(\"trace {\\n\"); break;",
 880         "                       default:      printf(\"p_%%s {\\n\", buf); break;",
 881         "                       }",
 882         "                       printf(\"size=\\\"8,10\\\";\\n\");",
 883         "                       printf(\"  GT [shape=box,style=dotted,label=\\\"%%s\\\"];\\n\", buf);",
 884         "                       printf(\"  GT -> S%%d;\\n\", is);",
 885         "               } else",
 886         "               {       switch (Btypes[n]) {",
 887         "                       case I_PROC:  printf(\"init\\n\"); break;",
 888         "                       case N_CLAIM: printf(\"claim %%s\\n\", procname[n]); break;",
 889         "                       case E_TRACE: printf(\"notrace assertion\\n\"); break;",
 890         "                       case N_TRACE: printf(\"trace assertion\\n\"); break;",
 891         "                       default:      printf(\"proctype %%s\\n\", procname[n]); break;",
 892         "               }       }",
 893         "               for (i = 1; i < m; i++)",
 894         "               {       reach[i] = 1;",
 895         "               }",
 896         "               tagtable(n, m, is, srcln, reach);",
 897         "               if (dodot) printf(\"}\\n\");",
 898         "       } else",
 899         "       for (i = 1; i < m; i++)",
 900         "       {       int nrelse;",
 901         "               if (Btypes[n] != N_CLAIM)",
 902         "               {       for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 903         "                       {       if (T0->st == i",
 904         "                               && strcmp(T0->tp, \"(1)\") == 0)",
 905         "                               {       printf(\"error: proctype '%%s' \",",
 906         "                                               procname[n]);",
 907         "                                       printf(\"line %%d, state %%d: has un\",",
 908         "                                               srcln[i], i);",
 909         "                                       printf(\"conditional self-loop\\n\");",
 910         "                                       pan_exit(1);",
 911         "               }       }       }",
 912         "               nrelse = 0;",
 913         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
 914         "               {       if (strcmp(T0->tp, \"else\") == 0)",
 915         "                               nrelse++;",
 916         "               }",
 917         "               if (nrelse > 1)",
 918         "               {       printf(\"error: proctype '%%s' state\",",
 919         "                               procname[n]);",
 920         "                       printf(\" %%d, inherits %%d\", i, nrelse);",
 921         "                       printf(\" 'else' stmnts\\n\");",
 922         "                       pan_exit(1);",
 923         "       }       }",
 924         "#if !defined(LOOPSTATE) && !defined(BFS_PAR)",
 925         "       if (state_tables)",
 926         "#endif",
 927         "       do_dfs(n, m, is, srcln, reach, lpstate);",
 928         "",
 929         "       if (!t_reverse)",
 930         "       {       return;",
 931         "       }",
 932         "       /* process n, with m states, is=initial state -- reverse list */",
 933         "       if (!state_tables && Btypes[n] != N_CLAIM)",
 934         "       {       for (i = 1; i < m; i++)", /* for each state */
 935         "               {       Trans *Tx = (Trans *) 0; /* list of escapes */",
 936         "                       Trans *Ty = (Trans *) 0; /* its tail element */",
 937         "                       T1 = (Trans *) 0; /* reversed list */",
 938         "                       T2 = (Trans *) 0; /* its tail */",
 939         "                       T3 = (Trans *) 0; /* remembers possible 'else' */",
 940         "",
 941         "                       /* find unless-escapes, they should go first */",
 942         "                       T4 = T5 = T0 = trans[n][i];",
 943         "       #ifdef HAS_UNLESS",
 944         "                       while (T4 && T4->e_trans) /* escapes are first in orig list */",
 945         "                       {       T5 = T4;          /* remember predecessor */",
 946         "                               T4 = T4->nxt;",
 947         "                       }",
 948         "       #endif",
 949         "                       /* T4 points to first non-escape, T5 to its parent, T0 to original list */",
 950         "                       if (T4 != T0)            /* there was at least one escape */",
 951         "                       {       T3 = T5->nxt;            /* start of non-escapes */",
 952         "                               T5->nxt = (Trans *) 0;   /* separate */",
 953         "                               Tx = T0;                 /* start of the escapes */",
 954         "                               Ty = T5;                 /* its tail */",
 955         "                               T0 = T3;                 /* the rest, to be reversed */",
 956         "                       }",
 957         "                       /* T0 points to first non-escape, Tx to the list of escapes, Ty to its tail */",
 958         "",
 959         "                       /* first tail-add non-escape transitions, reversed */",
 960         "                       T3 = (Trans *) 0;", /* remember a possible 'else' */
 961         "                       for (T5 = T0; T5; T5 = T4)",
 962         "                       {       T4 = T5->nxt;",
 963         "       #ifdef HAS_UNLESS",
 964         "                               if (T5->e_trans)",
 965         "                               {       printf(\"error: cannot happen!\\n\");",
 966         "                                       continue;",
 967         "                               }",
 968         "       #endif",
 969         "                               if (strcmp(T5->tp, \"else\") == 0)",
 970         "                               {       T3 = T5;",
 971         "                                       T5->nxt = (Trans *) 0;",
 972         "                               } else",
 973         "                               {       T5->nxt = T1;",
 974         "                                       if (!T1) { T2 = T5; }",
 975         "                                       T1 = T5;",
 976         "                       }       }",
 977         "                       /* T3 points to a possible else, which is removed from the list */",
 978         "                       /* T1 points to the reversed list so far (without escapes) */",
 979         "                       /* T2 points to the tail element -- where the else should go */",
 980         "                       if (T2 && T3)",
 981         "                       {       T2->nxt = T3;   /* add else */",
 982         "                       } else",
 983         "                       {       if (T3) /* there was an else, but there's no tail */",
 984         "                               {       if (!T1)        /* and no reversed list */",
 985         "                                       {       T1 = T3; /* odd, but possible */",
 986         "                                       } else          /* even stranger */",
 987         "                                       {       T1->nxt = T3;",
 988         "                       }       }       }",
 989         "",
 990         "                       /* add in the escapes, to that they appear at the front */",
 991         "                       if (Tx && Ty) { Ty->nxt = T1; T1 = Tx; }",
 992         "",
 993         "                       trans[n][i] = T1;",
 994         "                       /* reversed, with escapes first and else last */",
 995         "       }       }",
 996         "       if (state_tables && verbose)",
 997         "       {       printf(\"FINAL proctype %%s\\n\", ",
 998         "                       procname[n]);",
 999         "               for (i = 1; i < m; i++)",
1000         "               for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
1001         "                       crack(n, i, T0, srcln);",
1002         "       }",
1003         "}",
1004         "void",
1005         "imed(Trans *T, int v, int n, int j)    /* set intermediate state */",
1006         "{      progstate[n][T->st] |= progstate[n][v];",
1007         "       accpstate[n][T->st] |= accpstate[n][v];",
1008         "       stopstate[n][T->st] |= stopstate[n][v];",
1009         "       mapstate[n][j] = T->st;",
1010         "}",
1011         "void",
1012         "tagtable(int n, int m, int is, short srcln[], uchar reach[])",
1013         "{      Trans *z;\n",
1014         "       if (is >= m || !trans[n][is]",
1015         "       ||  is <= 0 || reach[is] == 0)",
1016         "               return;",
1017         "       reach[is] = 0;",
1018         "       if (state_tables)",
1019         "       for (z = trans[n][is]; z; z = z->nxt)",
1020         "       {       if (dodot)",
1021         "                       dot_crack(n, is, z);",
1022         "               else",
1023         "                       crack(n, is, z, srcln);",
1024         "       }",
1025         "",
1026         "       for (z = trans[n][is]; z; z = z->nxt)",
1027         "       {",
1028         "#ifdef HAS_UNLESS",
1029         "               int i, j;",
1030         "#endif",
1031         "               tagtable(n, m, z->st, srcln, reach);",
1032         "#ifdef HAS_UNLESS",
1033         "               for (i = 0; i < HAS_UNLESS; i++)",
1034         "               {       j = trans[n][is]->escp[i];",
1035         "                       if (!j) break;",
1036         "                       tagtable(n, m, j, srcln, reach);",
1037         "               }",
1038         "#endif",
1039         "       }",
1040         "}",
1041         "",
1042         "extern Trans *t_id_lkup[];",   /* needed by BFS_PAR */
1043         "",
1044         "void",
1045         "dfs_table(int n, int m, int is, short srcln[], uchar reach[], uchar lpstate[])",
1046         "{      Trans *z;\n",
1047         "       if (is >= m || is <= 0 || !trans[n][is])",
1048         "               return;",
1049         "       if ((reach[is] & (4|8|16)) != 0)",
1050         "       {       if ((reach[is] & (8|16)) == 16) /* on stack, not yet recorded */",
1051         "               {       lpstate[is] = 1;",
1052         "                       reach[is] |= 8; /* recorded */",
1053         "                       if (state_tables && verbose)",
1054         "                       {       printf(\"state %%d line %%d is a loopstate\\n\", is, srcln[is]);",
1055         "               }       }",
1056         "               return;",
1057         "       }",
1058         "       reach[is] |= (4|16);    /* visited | onstack */",
1059         "       for (z = trans[n][is]; z; z = z->nxt)",
1060         "       {       t_id_lkup[z->t_id] = z;",       /* needed by BFS_PAR */
1061         "#ifdef HAS_UNLESS",
1062         "               int i, j;",
1063         "#endif",
1064         "               dfs_table(n, m, z->st, srcln, reach, lpstate);",
1065         "#ifdef HAS_UNLESS",
1066         "               for (i = 0; i < HAS_UNLESS; i++)",
1067         "               {       j = trans[n][is]->escp[i];",
1068         "                       if (!j) break;",
1069         "                       dfs_table(n, m, j, srcln, reach, lpstate);",
1070         "               }",
1071         "#endif",
1072         "       }",
1073         "       reach[is] &= ~16; /* no longer on stack */",
1074         "}",
1075         "void",
1076         "do_dfs(int n, int m, int is, short srcln[], uchar reach[], uchar lpstate[])",
1077         "{      int i;",
1078         "       dfs_table(n, m, is, srcln, reach, lpstate);",
1079         "       for (i = 0; i < m; i++)",
1080         "               reach[i] &= ~(4|8|16);",
1081         "}",
1082         "void",
1083         "crack(int n, int j, Trans *z, short srcln[])",
1084         "{      int i;\n",
1085         "       if (!z) return;",
1086         "       printf(\"\tstate %%3d -(tr %%3d)-> state %%3d  \",",
1087         "               j, z->forw, z->st);",
1088         "       printf(\"[id %%3d tp %%3d\", z->t_id, z->tpe[0]);",
1089         "       if (z->tpe[1]) printf(\",%%d\", z->tpe[1]);",
1090         "#ifdef HAS_UNLESS",
1091         "       if (z->e_trans)",
1092         "               printf(\" org %%3d\", z->e_trans);",
1093         "       else if (state_tables >= 2)",
1094         "       for (i = 0; i < HAS_UNLESS; i++)",
1095         "       {       if (!z->escp[i]) break;",
1096         "               printf(\" esc %%d\", z->escp[i]);",
1097         "       }",
1098         "#endif",
1099         "       printf(\"]\");",
1100         "       printf(\" [%%s%%s%%s%%s%%s] %%s:%%d => \",",
1101         "               z->atom&6?\"A\":z->atom&32?\"D\":\"-\",",
1102         "               accpstate[n][j]?\"a\" :\"-\",",
1103         "               stopstate[n][j]?\"e\" : \"-\",",
1104         "               progstate[n][j]?\"p\" : \"-\",",
1105         "               z->atom & 8 ?\"L\":\"G\",",
1106         "               PanSource, srcln[j]);",
1107         "       for (i = 0; z->tp[i]; i++)",
1108         "               if (z->tp[i] == \'\\n\')",
1109         "                       printf(\"\\\\n\");",
1110         "               else",
1111         "                       putchar(z->tp[i]);",
1112         "       if (verbose && z->qu[0])",
1113         "       {       printf(\"\\t[\");",
1114         "               for (i = 0; i < 6; i++)",
1115         "                       if (z->qu[i])",
1116         "                               printf(\"(%%d,%%d)\",",
1117         "                               z->qu[i], z->ty[i]);",
1118         "               printf(\"]\");",
1119         "       }",
1120         "       printf(\"\\n\");",
1121         "       fflush(stdout);",
1122         "}",
1123         "/* spin -a m.pml; cc -o pan pan.c; ./pan -D | dot -Tps > foo.ps; ps2pdf foo.ps */",
1124         "void",
1125         "dot_crack(int n, int j, Trans *z)",
1126         "{      int i;\n",
1127         "       if (!z) return;",
1128         "       printf(\"\tS%%d -> S%%d  [color=black\", j, z->st);",
1129         "",
1130         "       if (z->atom&6) printf(\",style=dashed\");",             /* A */
1131         "       else if (z->atom&32) printf(\",style=dotted\");",       /* D */
1132         "       else if (z->atom&8) printf(\",style=solid\");",         /* L */
1133         "       else printf(\",style=bold\");",                         /* G */
1134                 /* other styles: filled dotted */
1135         "",
1136         "       printf(\",label=\\\"\");",
1137         "       for (i = 0; z->tp[i]; i++)",
1138         "       {       if (z->tp[i] == \'\\\\\'",
1139         "               &&  z->tp[i+1] == \'n\')",
1140         "               {       i++; printf(\" \");",
1141         "               } else",
1142         "               {       putchar(z->tp[i]);",
1143         "       }       }",
1144         "       printf(\"\\\"];\\n\");",
1145         "       if (accpstate[n][j]) printf(\"  S%%d [color=red,style=bold];\\n\", j);",
1146         "       else if (progstate[n][j]) printf(\"  S%%d [color=green,style=bold];\\n\", j);",
1147         "       if (stopstate[n][j]) printf(\"  S%%d [color=blue,style=bold,shape=box];\\n\", j);",
1148         "}",
1149         "",
1150         "#ifdef VAR_RANGES",
1151         "#define BYTESIZE       32      /* 2^8 : 2^3 = 256:8 = 32 */",
1152         "",
1153         "typedef struct Vr_Ptr {",
1154         "       char    *nm;",
1155         "       uchar   vals[BYTESIZE];",
1156         "       struct Vr_Ptr *nxt;",
1157         "} Vr_Ptr;",
1158         "Vr_Ptr *ranges = (Vr_Ptr *) 0;",
1159         "",
1160         "void",
1161         "logval(char *s, int v)",
1162         "{      Vr_Ptr *tmp;",
1163         "",
1164         "       if (v<0 || v > 255) return;",
1165         "       for (tmp = ranges; tmp; tmp = tmp->nxt)",
1166         "               if (!strcmp(tmp->nm, s))",
1167         "                       goto found;",
1168         "       tmp = (Vr_Ptr *) emalloc(sizeof(Vr_Ptr));",
1169         "       tmp->nxt = ranges;",
1170         "       ranges = tmp;",
1171         "       tmp->nm = s;",
1172         "found:",
1173         "       tmp->vals[(v)/8] |= 1<<((v)%%8);",
1174         "}",
1175         "",
1176         "void",
1177         "dumpval(uchar X[], int range)",
1178         "{      int w, x, i, j = -1;",
1179         "",
1180         "       for (w = i = 0; w < range; w++)",
1181         "       for (x = 0; x < 8; x++, i++)",
1182         "       {",
1183         "from:          if ((X[w] & (1<<x)))",
1184         "               {       printf(\"%%d\", i);",
1185         "                       j = i;",
1186         "                       goto upto;",
1187         "       }       }",
1188         "       return;",
1189         "       for (w = 0; w < range; w++)",
1190         "       for (x = 0; x < 8; x++, i++)",
1191         "       {",
1192         "upto:          if (!(X[w] & (1<<x)))",
1193         "               {       if (i-1 == j)",
1194         "                               printf(\", \");",
1195         "                       else",
1196         "                               printf(\"-%%d, \", i-1);",
1197         "                       goto from;",
1198         "       }       }",
1199         "       if (j >= 0 && j != 255)",
1200         "               printf(\"-255\");",
1201         "}",
1202         "",
1203         "void",
1204         "dumpranges(void)",
1205         "{      Vr_Ptr *tmp;",
1206         "       printf(\"\\nValues assigned within \");",
1207         "       printf(\"interval [0..255]:\\n\");",
1208         "       for (tmp = ranges; tmp; tmp = tmp->nxt)",
1209         "       {       printf(\"\\t%%s\\t: \", tmp->nm);",
1210         "               dumpval(tmp->vals, BYTESIZE);",
1211         "               printf(\"\\n\");",
1212         "       }",
1213         "}",
1214         "#endif",
1215         0,
1216 };