sys/src/cmd/spin/pangen2.c

   1 /***** spin: pangen2.c *****/
   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 #include "spin.h"
  13 #include "version.h"
  14 #include "y.tab.h"
  15 #include "pangen2.h"
  16 #include "pangen4.h"
  17 #include "pangen5.h"
  18
  19 #define DELTA   500     /* sets an upperbound on nr of chan names */
  20
  21 #define blurb(fd, e)    { fprintf(fd, "\n"); if (!merger) fprintf(fd, "\t\t/* %s:%d */\n", \
  22                                 e->n->fn->name, e->n->ln); }
  23 #define tr_map(m, e)    { if (!merger) fprintf(tt, "\t\ttr_2_src(%d, %s, %d);\n", \
  24                                 m, e->n->fn->name, e->n->ln); }
  25
  26 extern ProcList *rdy;
  27 extern RunList  *run;
  28 extern Symbol   *Fname, *oFname, *context;
  29 extern char     *claimproc, *eventmap;
  30 extern int      lineno, verbose, Npars, Mpars;
  31 extern int      m_loss, has_remote, has_remvar, merger, rvopt, separate;
  32 extern int      Ntimeouts, Etimeouts, deadvar;
  33 extern int      u_sync, u_async, nrRdy;
  34 extern int      GenCode, IsGuard, Level, TestOnly;
  35 extern short    has_stack;
  36 extern char     *NextLab[];
  37
  38 FILE    *tc, *th, *tt, *tm, *tb;
  39
  40 int     OkBreak = -1;
  41 short   nocast=0;       /* to turn off casts in lvalues */
  42 short   terse=0;        /* terse printing of varnames */
  43 short   no_arrays=0;
  44 short   has_last=0;     /* spec refers to _last */
  45 short   has_badelse=0;  /* spec contains else combined with chan refs */
  46 short   has_enabled=0;  /* spec contains enabled() */
  47 short   has_pcvalue=0;  /* spec contains pc_value() */
  48 short   has_np=0;       /* spec contains np_ */
  49 short   has_sorted=0;   /* spec contains `!!' (sorted-send) operator */
  50 short   has_random=0;   /* spec contains `??' (random-recv) operator */
  51 short   has_xu=0;       /* spec contains xr or xs assertions */
  52 short   has_unless=0;   /* spec contains unless statements */
  53 short   has_provided=0; /* spec contains PROVIDED clauses on procs */
  54 short   has_code=0;     /* spec contains c_code, c_expr, c_state */
  55 short   _isok=0;        /* checks usage of predefined variable _ */
  56 short   evalindex=0;    /* evaluate index of var names */
  57 short   withprocname=0; /* prefix local varnames with procname */
  58 int     mst=0;          /* max nr of state/process */
  59 int     claimnr = -1;   /* claim process, if any */
  60 int     eventmapnr = -1; /* event trace, if any */
  61 int     Pid;            /* proc currently processed */
  62 int     multi_oval;     /* set in merges, used also in pangen4.c */
  63
  64 #define MAXMERGE        256     /* max nr of bups per merge sequence */
  65
  66 static short    CnT[MAXMERGE];
  67 static Lextok   XZ, YZ[MAXMERGE];
  68 static int      didcase, YZmax, YZcnt;
  69
  70 static Lextok   *Nn[2];
  71 static int      Det;    /* set if deterministic */
  72 static int      T_sum, T_mus, t_cyc;
  73 static int      TPE[2], EPT[2];
  74 static int      uniq=1;
  75 static int      multi_needed, multi_undo;
  76 static short    AllGlobal=0;    /* set if process has provided clause */
  77
  78 int     has_global(Lextok *);
  79 static int      getweight(Lextok *);
  80 static int      scan_seq(Sequence *);
  81 static void     genconditionals(void);
  82 static void     mark_seq(Sequence *);
  83 static void     patch_atomic(Sequence *);
  84 static void     put_seq(Sequence *, int, int);
  85 static void     putproc(ProcList *);
  86 static void     Tpe(Lextok *);
  87 extern void     spit_recvs(FILE *, FILE*);
  88
  89 static int
  90 fproc(char *s)
  91 {       ProcList *p;
  92
  93         for (p = rdy; p; p = p->nxt)
  94                 if (strcmp(p->n->name, s) == 0)
  95                         return p->tn;
  96
  97         fatal("proctype %s not found", s);
  98         return -1;
  99 }
 100
 101 static void
 102 reverse_procs(RunList *q)
 103 {
 104         if (!q) return;
 105         reverse_procs(q->nxt);
 106         fprintf(tc, "   Addproc(%d);\n", q->tn);
 107 }
 108
 109 static void
 110 tm_predef_np(void)
 111 {
 112         fprintf(th, "#define _T5        %d\n", uniq++);
 113         fprintf(th, "#define _T2        %d\n", uniq++);
 114         fprintf(tm, "\tcase  _T5:\t/* np_ */\n");
 115
 116         if (separate == 2)
 117         fprintf(tm, "\t\tif (!((!(o_pm&4) && !(tau&128))))\n");
 118         else
 119         fprintf(tm, "\t\tif (!((!(trpt->o_pm&4) && !(trpt->tau&128))))\n");
 120
 121         fprintf(tm, "\t\t\tcontinue;\n");
 122         fprintf(tm, "\t\t/* else fall through */\n");
 123         fprintf(tm, "\tcase  _T2:\t/* true */\n");
 124         fprintf(tm, "\t\t_m = 3; goto P999;\n");
 125 }
 126
 127 static void
 128 tt_predef_np(void)
 129 {
 130         fprintf(tt, "\t/* np_ demon: */\n");
 131         fprintf(tt, "\ttrans[_NP_] = ");
 132         fprintf(tt, "(Trans **) emalloc(2*sizeof(Trans *));\n");
 133         fprintf(tt, "\tT = trans[_NP_][0] = ");
 134         fprintf(tt, "settr(9997,0,1,_T5,0,\"(np_)\", 1,2,0);\n");
 135         fprintf(tt, "\t    T->nxt         = ");
 136         fprintf(tt, "settr(9998,0,0,_T2,0,\"(1)\",   0,2,0);\n");
 137         fprintf(tt, "\tT = trans[_NP_][1] = ");
 138         fprintf(tt, "settr(9999,0,1,_T5,0,\"(np_)\", 1,2,0);\n");
 139 }
 140
 141 static struct {
 142         char *nm[3];
 143 } Cfile[] = {
 144         { { "pan.c", "pan_s.c", "pan_t.c" } },
 145         { { "pan.h", "pan_s.h", "pan_t.h" } },
 146         { { "pan.t", "pan_s.t", "pan_t.t" } },
 147         { { "pan.m", "pan_s.m", "pan_t.m" } },
 148         { { "pan.b", "pan_s.b", "pan_t.b" } }
 149 };
 150
 151 void
 152 gensrc(void)
 153 {       ProcList *p;
 154
 155         if (!(tc = fopen(Cfile[0].nm[separate], "w"))           /* main routines */
 156         ||  !(th = fopen(Cfile[1].nm[separate], "w"))           /* header file   */
 157         ||  !(tt = fopen(Cfile[2].nm[separate], "w"))           /* transition matrix */
 158         ||  !(tm = fopen(Cfile[3].nm[separate], "w"))           /* forward  moves */
 159         ||  !(tb = fopen(Cfile[4].nm[separate], "w")))  /* backward moves */
 160         {       printf("spin: cannot create pan.[chtmfb]\n");
 161                 alldone(1);
 162         }
 163
 164         fprintf(th, "#define Version    \"%s\"\n", Version);
 165         fprintf(th, "#define Source     \"%s\"\n\n", oFname->name);
 166         if (separate != 2)
 167         fprintf(th, "char *TrailFile = Source; /* default */\n");
 168
 169         fprintf(th, "#if defined(BFS)\n");
 170         fprintf(th, "#ifndef SAFETY\n");
 171         fprintf(th, "#define SAFETY\n");
 172         fprintf(th, "#endif\n");
 173         fprintf(th, "#ifndef XUSAFE\n");
 174         fprintf(th, "#define XUSAFE\n");
 175         fprintf(th, "#endif\n");
 176         fprintf(th, "#endif\n");
 177
 178         fprintf(th, "#ifndef uchar\n");
 179         fprintf(th, "#define uchar      unsigned char\n");
 180         fprintf(th, "#endif\n");
 181         fprintf(th, "#ifndef uint\n");
 182         fprintf(th, "#define uint       unsigned int\n");
 183         fprintf(th, "#endif\n");
 184
 185         if (sizeof(void *) > 4) /* 64 bit machine */
 186         {       fprintf(th, "#ifndef HASH32\n");
 187                 fprintf(th, "#define HASH64\n");
 188                 fprintf(th, "#endif\n");
 189         }
 190 #if 0
 191         if (sizeof(long)==sizeof(int))
 192                 fprintf(th, "#define long       int\n");
 193 #endif
 194         if (separate == 1 && !claimproc)
 195         {       Symbol *n = (Symbol *) emalloc(sizeof(Symbol));
 196                 Sequence *s = (Sequence *) emalloc(sizeof(Sequence));
 197                 claimproc = n->name = "_:never_template:_";
 198                 ready(n, ZN, s, 0, ZN);
 199         }
 200         if (separate == 2)
 201         {       if (has_remote)
 202                 {       printf("spin: warning, make sure that the S1 model\n");
 203                         printf("      includes the same remote references\n");
 204                 }
 205                 fprintf(th, "#ifndef NFAIR\n");
 206                 fprintf(th, "#define NFAIR      2       /* must be >= 2 */\n");
 207                 fprintf(th, "#endif\n");
 208                 if (has_last)
 209                 fprintf(th, "#define HAS_LAST   %d\n", has_last);
 210                 goto doless;
 211         }
 212
 213         fprintf(th, "#define DELTA      %d\n", DELTA);
 214         fprintf(th, "#ifdef MA\n");
 215         fprintf(th, "#if MA==1\n"); /* user typed -DMA without size */
 216         fprintf(th, "#undef MA\n#define MA      100\n");
 217         fprintf(th, "#endif\n#endif\n");
 218         fprintf(th, "#ifdef W_XPT\n");
 219         fprintf(th, "#if W_XPT==1\n"); /* user typed -DW_XPT without size */
 220         fprintf(th, "#undef W_XPT\n#define W_XPT 1000000\n");
 221         fprintf(th, "#endif\n#endif\n");
 222         fprintf(th, "#ifndef NFAIR\n");
 223         fprintf(th, "#define NFAIR      2       /* must be >= 2 */\n");
 224         fprintf(th, "#endif\n");
 225         if (Ntimeouts)
 226         fprintf(th, "#define NTIM       %d\n", Ntimeouts);
 227         if (Etimeouts)
 228         fprintf(th, "#define ETIM       %d\n", Etimeouts);
 229         if (has_remvar)
 230         fprintf(th, "#define REM_VARS   1\n");
 231         if (has_remote)
 232         fprintf(th, "#define REM_REFS   %d\n", has_remote); /* not yet used */
 233         if (has_last)
 234         fprintf(th, "#define HAS_LAST   %d\n", has_last);
 235         if (has_sorted)
 236         fprintf(th, "#define HAS_SORTED %d\n", has_sorted);
 237         if (m_loss)
 238         fprintf(th, "#define M_LOSS\n");
 239         if (has_random)
 240         fprintf(th, "#define HAS_RANDOM %d\n", has_random);
 241         fprintf(th, "#define HAS_CODE\n");      /* doesn't seem to cause measurable overhead */
 242         if (has_stack)
 243         fprintf(th, "#define HAS_STACK\n");
 244         if (has_enabled)
 245         fprintf(th, "#define HAS_ENABLED        1\n");
 246         if (has_unless)
 247         fprintf(th, "#define HAS_UNLESS %d\n", has_unless);
 248         if (has_provided)
 249         fprintf(th, "#define HAS_PROVIDED       %d\n", has_provided);
 250         if (has_pcvalue)
 251         fprintf(th, "#define HAS_PCVALUE        %d\n", has_pcvalue);
 252         if (has_badelse)
 253         fprintf(th, "#define HAS_BADELSE        %d\n", has_badelse);
 254         if (has_enabled
 255         ||  has_pcvalue
 256         ||  has_badelse
 257         ||  has_last)
 258         {       fprintf(th, "#ifndef NOREDUCE\n");
 259                 fprintf(th, "#define NOREDUCE   1\n");
 260                 fprintf(th, "#endif\n");
 261         }
 262         if (has_np)
 263         fprintf(th, "#define HAS_NP     %d\n", has_np);
 264         if (merger)
 265         fprintf(th, "#define MERGED     1\n");
 266
 267 doless:
 268         fprintf(th, "#ifdef NP  /* includes np_ demon */\n");
 269         if (!has_np)
 270         fprintf(th, "#define HAS_NP     2\n");
 271         fprintf(th, "#define VERI       %d\n",  nrRdy);
 272         fprintf(th, "#define endclaim   3 /* none */\n");
 273         fprintf(th, "#endif\n");
 274         if (claimproc)
 275         {       claimnr = fproc(claimproc);
 276                 /* NP overrides claimproc */
 277                 fprintf(th, "#if !defined(NOCLAIM) && !defined NP\n");
 278                 fprintf(th, "#define VERI       %d\n",  claimnr);
 279                 fprintf(th, "#define endclaim   endstate%d\n",  claimnr);
 280                 fprintf(th, "#endif\n");
 281         }
 282         if (eventmap)
 283         {       eventmapnr = fproc(eventmap);
 284                 fprintf(th, "#define EVENT_TRACE        %d\n",  eventmapnr);
 285                 fprintf(th, "#define endevent   endstate%d\n",  eventmapnr);
 286                 if (eventmap[2] == 'o') /* ":notrace:" */
 287                 fprintf(th, "#define NEGATED_TRACE      1\n");
 288         }
 289
 290         fprintf(th, "typedef struct S_F_MAP {\n");
 291         fprintf(th, "   char *fnm; int from; int upto;\n");
 292         fprintf(th, "} S_F_MAP;\n");
 293
 294         fprintf(tc, "/*** Generated by %s ***/\n", Version);
 295         fprintf(tc, "/*** From source: %s ***/\n\n", oFname->name);
 296
 297         ntimes(tc, 0, 1, Pre0);
 298
 299         plunk_c_decls(tc);      /* types can be refered to in State */
 300
 301         switch (separate) {
 302         case 0: fprintf(tc, "#include \"pan.h\"\n"); break;
 303         case 1: fprintf(tc, "#include \"pan_s.h\"\n"); break;
 304         case 2: fprintf(tc, "#include \"pan_t.h\"\n"); break;
 305         }
 306
 307         fprintf(tc, "State      A_Root; /* seed-state for cycles */\n");
 308         fprintf(tc, "State      now;    /* the full state-vector */\n");
 309         plunk_c_fcts(tc);       /* State can be used in fcts */
 310
 311         if (separate != 2)
 312                 ntimes(tc, 0, 1, Preamble);
 313         else
 314                 fprintf(tc, "extern int verbose; extern long depth;\n");
 315
 316         fprintf(tc, "#ifndef NOBOUNDCHECK\n");
 317         fprintf(tc, "#define Index(x, y)\tBoundcheck(x, y, II, tt, t)\n");
 318         fprintf(tc, "#else\n");
 319         fprintf(tc, "#define Index(x, y)\tx\n");
 320         fprintf(tc, "#endif\n");
 321
 322         c_preview();    /* sets hastrack */
 323
 324         for (p = rdy; p; p = p->nxt)
 325                 mst = max(p->s->maxel, mst);
 326
 327         if (separate != 2)
 328         {       fprintf(tt, "#ifdef PEG\n");
 329                 fprintf(tt, "struct T_SRC {\n");
 330                 fprintf(tt, "   char *fl; int ln;\n");
 331                 fprintf(tt, "} T_SRC[NTRANS];\n\n");
 332                 fprintf(tt, "void\ntr_2_src(int m, char *file, int ln)\n");
 333                 fprintf(tt, "{  T_SRC[m].fl = file;\n");
 334                 fprintf(tt, "   T_SRC[m].ln = ln;\n");
 335                 fprintf(tt, "}\n\n");
 336                 fprintf(tt, "void\nputpeg(int n, int m)\n");
 337                 fprintf(tt, "{  printf(\"%%5d\ttrans %%4d \", m, n);\n");
 338                 fprintf(tt, "   printf(\"file %%s line %%3d\\n\",\n");
 339                 fprintf(tt, "           T_SRC[n].fl, T_SRC[n].ln);\n");
 340                 fprintf(tt, "}\n");
 341                 if (!merger)
 342                 {       fprintf(tt, "#else\n");
 343                         fprintf(tt, "#define tr_2_src(m,f,l)\n");
 344                 }
 345                 fprintf(tt, "#endif\n\n");
 346                 fprintf(tt, "void\nsettable(void)\n{\tTrans *T;\n");
 347                 fprintf(tt, "\tTrans *settr(int, int, int, int, int,");
 348                 fprintf(tt, " char *, int, int, int);\n\n");
 349                 fprintf(tt, "\ttrans = (Trans ***) ");
 350                 fprintf(tt, "emalloc(%d*sizeof(Trans **));\n", nrRdy+1);
 351                                 /* +1 for np_ automaton */
 352
 353                 if (separate == 1)
 354                 {
 355                 fprintf(tm, "   if (II == 0)\n");
 356                 fprintf(tm, "   { _m = step_claim(trpt->o_pm, trpt->tau, tt, ot, t);\n");
 357                 fprintf(tm, "     if (_m) goto P999; else continue;\n");
 358                 fprintf(tm, "   } else\n");
 359                 }
 360
 361                 fprintf(tm, "#define rand       pan_rand\n");
 362                 fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n");
 363                 fprintf(tm, "   printf(\"Pr: %%d Tr: %%d\\n\", II, t->forw);\n");
 364                 fprintf(tm, "#endif\n");
 365                 fprintf(tm, "   switch (t->forw) {\n");
 366         } else
 367         {       fprintf(tt, "#ifndef PEG\n");
 368                 fprintf(tt, "#define tr_2_src(m,f,l)\n");
 369                 fprintf(tt, "#endif\n");
 370                 fprintf(tt, "void\nset_claim(void)\n{\tTrans *T;\n");
 371                 fprintf(tt, "\textern Trans ***trans;\n");
 372                 fprintf(tt, "\textern Trans *settr(int, int, int, int, int,");
 373                 fprintf(tt, " char *, int, int, int);\n\n");
 374
 375                 fprintf(tm, "#define rand       pan_rand\n");
 376                 fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n");
 377                 fprintf(tm, "   printf(\"Pr: %%d Tr: %%d\\n\", II, forw);\n");
 378                 fprintf(tm, "#endif\n");
 379                 fprintf(tm, "   switch (forw) {\n");
 380         }
 381
 382         fprintf(tm, "   default: Uerror(\"bad forward move\");\n");
 383         fprintf(tm, "   case 0: /* if without executable clauses */\n");
 384         fprintf(tm, "           continue;\n");
 385         fprintf(tm, "   case 1: /* generic 'goto' or 'skip' */\n");
 386         if (separate != 2)
 387                 fprintf(tm, "           IfNotBlocked\n");
 388         fprintf(tm, "           _m = 3; goto P999;\n");
 389         fprintf(tm, "   case 2: /* generic 'else' */\n");
 390         if (separate == 2)
 391                 fprintf(tm, "           if (o_pm&1) continue;\n");
 392         else
 393         {       fprintf(tm, "           IfNotBlocked\n");
 394                 fprintf(tm, "           if (trpt->o_pm&1) continue;\n");
 395         }
 396         fprintf(tm, "           _m = 3; goto P999;\n");
 397         uniq = 3;
 398
 399         if (separate == 1)
 400                 fprintf(tb, "   if (II == 0) goto R999;\n");
 401
 402         fprintf(tb, "   switch (t->back) {\n");
 403         fprintf(tb, "   default: Uerror(\"bad return move\");\n");
 404         fprintf(tb, "   case  0: goto R999; /* nothing to undo */\n");
 405
 406         for (p = rdy; p; p = p->nxt)
 407                 putproc(p);
 408
 409
 410         if (separate != 2)
 411         {       fprintf(th, "struct {\n");
 412                 fprintf(th, "   int tp; short *src;\n");
 413                 fprintf(th, "} src_all[] = {\n");
 414                 for (p = rdy; p; p = p->nxt)
 415                         fprintf(th, "   { %d, &src_ln%d[0] },\n",
 416                                 p->tn, p->tn);
 417                 fprintf(th, "   { 0, (short *) 0 }\n");
 418                 fprintf(th, "};\n");
 419                 fprintf(th, "short *frm_st0;\n");       /* records src states for transitions in never claim */
 420         } else
 421         {       fprintf(th, "extern short *frm_st0;\n");
 422         }
 423
 424         gencodetable(th);
 425
 426         if (separate != 1)
 427         {       tm_predef_np();
 428                 tt_predef_np();
 429         }
 430         fprintf(tt, "}\n\n");   /* end of settable() */
 431
 432         fprintf(tm, "#undef rand\n");
 433         fprintf(tm, "   }\n\n");
 434         fprintf(tb, "   }\n\n");
 435
 436         if (separate != 2)
 437         {       ntimes(tt, 0, 1, Tail);
 438                 genheader();
 439                 if (separate == 1)
 440                 {       fprintf(th, "#define FORWARD_MOVES\t\"pan_s.m\"\n");
 441                         fprintf(th, "#define REVERSE_MOVES\t\"pan_s.b\"\n");
 442                         fprintf(th, "#define SEPARATE\n");
 443                         fprintf(th, "#define TRANSITIONS\t\"pan_s.t\"\n");
 444                         fprintf(th, "extern void ini_claim(int, int);\n");
 445                 } else
 446                 {       fprintf(th, "#define FORWARD_MOVES\t\"pan.m\"\n");
 447                         fprintf(th, "#define REVERSE_MOVES\t\"pan.b\"\n");
 448                         fprintf(th, "#define TRANSITIONS\t\"pan.t\"\n");
 449                 }
 450                 genaddproc();
 451                 genother();
 452                 genaddqueue();
 453                 genunio();
 454                 genconditionals();
 455                 gensvmap();
 456                 if (!run) fatal("no runable process", (char *)0);
 457                 fprintf(tc, "void\n");
 458                 fprintf(tc, "active_procs(void)\n{\n");
 459                         reverse_procs(run);
 460                 fprintf(tc, "}\n");
 461                 ntimes(tc, 0, 1, Dfa);
 462                 ntimes(tc, 0, 1, Xpt);
 463
 464                 fprintf(th, "#define NTRANS     %d\n", uniq);
 465                 fprintf(th, "#ifdef PEG\n");
 466                 fprintf(th, "long peg[NTRANS];\n");
 467                 fprintf(th, "#endif\n");
 468
 469                 if (u_sync && !u_async)
 470                         spit_recvs(th, tc);
 471         } else
 472         {       genheader();
 473                 fprintf(th, "#define FORWARD_MOVES\t\"pan_t.m\"\n");
 474                 fprintf(th, "#define REVERSE_MOVES\t\"pan_t.b\"\n");
 475                 fprintf(th, "#define TRANSITIONS\t\"pan_t.t\"\n");
 476                 fprintf(tc, "extern int Maxbody;\n");
 477                 fprintf(tc, "#if VECTORSZ>32000\n");
 478                 fprintf(tc, "extern int proc_offset[];\n");
 479                 fprintf(tc, "#else\n");
 480                 fprintf(tc, "extern short proc_offset[];\n");
 481                 fprintf(tc, "#endif\n");
 482                 fprintf(tc, "extern uchar proc_skip[];\n");
 483                 fprintf(tc, "extern uchar *reached[];\n");
 484                 fprintf(tc, "extern uchar *accpstate[];\n");
 485                 fprintf(tc, "extern uchar *progstate[];\n");
 486                 fprintf(tc, "extern uchar *stopstate[];\n");
 487                 fprintf(tc, "extern uchar *visstate[];\n\n");
 488                 fprintf(tc, "extern short *mapstate[];\n");
 489
 490                 fprintf(tc, "void\nini_claim(int n, int h)\n{");
 491                 fprintf(tc, "\textern State now;\n");
 492                 fprintf(tc, "\textern void set_claim(void);\n\n");
 493                 fprintf(tc, "#ifdef PROV\n");
 494                 fprintf(tc, "#include PROV\n");
 495                 fprintf(tc, "#endif\n");
 496                 fprintf(tc, "\tset_claim();\n");
 497                 genother();
 498                 fprintf(tc, "\n\tswitch (n) {\n");
 499                 genaddproc();
 500                 fprintf(tc, "\t}\n");
 501                 fprintf(tc, "\n}\n");
 502                 fprintf(tc, "int\nstep_claim(int o_pm, int tau, int tt, int ot, Trans *t)\n");
 503                 fprintf(tc, "{  int forw = t->forw; int _m = 0; extern char *noptr; int II=0;\n");
 504                 fprintf(tc, "   extern State now;\n");
 505                 fprintf(tc, "#define continue   return 0\n");
 506                 fprintf(tc, "#include \"pan_t.m\"\n");
 507                 fprintf(tc, "P999:\n\treturn _m;\n}\n");
 508                 fprintf(tc, "#undef continue\n");
 509                 fprintf(tc, "int\nrev_claim(int backw)\n{ return 0; }\n");
 510                 fprintf(tc, "#include TRANSITIONS\n");
 511         }
 512         if (separate != 1)
 513                 ntimes(tc, 0, 1, Nvr1);
 514
 515         if (separate != 2)
 516         {       c_wrapper(tc);
 517                 c_chandump(tc);
 518         }
 519 }
 520
 521 static int
 522 find_id(Symbol *s)
 523 {       ProcList *p;
 524
 525         if (s)
 526         for (p = rdy; p; p = p->nxt)
 527                 if (s == p->n)
 528                         return p->tn;
 529         return 0;
 530 }
 531
 532 static void
 533 dolen(Symbol *s, char *pre, int pid, int ai, int qln)
 534 {
 535         if (ai > 0)
 536                 fprintf(tc, "\n\t\t\t ||    ");
 537         fprintf(tc, "%s(", pre);
 538         if (!(s->hidden&1))
 539         {       if (s->context)
 540                         fprintf(tc, "((P%d *)this)->", pid);
 541                 else
 542                         fprintf(tc, "now.");
 543         }
 544         fprintf(tc, "%s", s->name);
 545         if (qln > 1) fprintf(tc, "[%d]", ai);
 546         fprintf(tc, ")");
 547 }
 548
 549 struct AA {     char TT[9];     char CC[8]; };
 550
 551 static struct AA BB[4] = {
 552         { "Q_FULL_F",   " q_full" },
 553         { "Q_FULL_T",   "!q_full" },
 554         { "Q_EMPT_F",   " !q_len" },
 555         { "Q_EMPT_T",   "  q_len" }
 556         };
 557
 558 static struct AA DD[4] = {
 559         { "Q_FULL_F",   " q_e_f" },     /* empty or full */
 560         { "Q_FULL_T",   "!q_full" },
 561         { "Q_EMPT_F",   " q_e_f" },
 562         { "Q_EMPT_T",   " q_len" }
 563         };
 564         /* this reduces the number of cases where 's' and 'r'
 565            are considered conditionally safe under the
 566            partial order reduction rules;  as a price for
 567            this simple implementation, it also affects the
 568            cases where nfull and nempty can be considered
 569            safe -- since these are labeled the same way as
 570            's' and 'r' respectively
 571            it only affects reduction, not functionality
 572          */
 573
 574 void
 575 bb_or_dd(int j, int which)
 576 {
 577         if (which)
 578         {       if (has_unless)
 579                         fprintf(tc, "%s", DD[j].CC);
 580                 else
 581                         fprintf(tc, "%s", BB[j].CC);
 582         } else
 583         {       if (has_unless)
 584                         fprintf(tc, "%s", DD[j].TT);
 585                 else
 586                         fprintf(tc, "%s", BB[j].TT);
 587         }
 588 }
 589
 590 void
 591 Done_case(char *nm, Symbol *z)
 592 {       int j, k;
 593         int nid = z->Nid;
 594         int qln = z->nel;
 595
 596         fprintf(tc, "\t\tcase %d: if (", nid);
 597         for (j = 0; j < 4; j++)
 598         {       fprintf(tc, "\t(t->ty[i] == ");
 599                 bb_or_dd(j, 0);
 600                 fprintf(tc, " && (");
 601                 for (k = 0; k < qln; k++)
 602                 {       if (k > 0)
 603                                 fprintf(tc, "\n\t\t\t ||    ");
 604                         bb_or_dd(j, 1);
 605                         fprintf(tc, "(%s%s", nm, z->name);
 606                         if (qln > 1)
 607                                 fprintf(tc, "[%d]", k);
 608                         fprintf(tc, ")");
 609                 }
 610                 fprintf(tc, "))\n\t\t\t ");
 611                 if (j < 3)
 612                         fprintf(tc, "|| ");
 613                 else
 614                         fprintf(tc, "   ");
 615         }
 616         fprintf(tc, ") return 0; break;\n");
 617 }
 618
 619 static void
 620 Docase(Symbol *s, int pid, int nid)
 621 {       int i, j;
 622
 623         fprintf(tc, "\t\tcase %d: if (", nid);
 624         for (j = 0; j < 4; j++)
 625         {       fprintf(tc, "\t(t->ty[i] == ");
 626                 bb_or_dd(j, 0);
 627                 fprintf(tc, " && (");
 628                 if (has_unless)
 629                 {       for (i = 0; i < s->nel; i++)
 630                                 dolen(s, DD[j].CC, pid, i, s->nel);
 631                 } else
 632                 {       for (i = 0; i < s->nel; i++)
 633                                 dolen(s, BB[j].CC, pid, i, s->nel);
 634                 }
 635                 fprintf(tc, "))\n\t\t\t ");
 636                 if (j < 3)
 637                         fprintf(tc, "|| ");
 638                 else
 639                         fprintf(tc, "   ");
 640         }
 641         fprintf(tc, ") return 0; break;\n");
 642 }
 643
 644 static void
 645 genconditionals(void)
 646 {       Symbol *s;
 647         int last=0, j;
 648         extern Ordered  *all_names;
 649         Ordered *walk;
 650
 651         fprintf(th, "#define LOCAL      1\n");
 652         fprintf(th, "#define Q_FULL_F   2\n");
 653         fprintf(th, "#define Q_EMPT_F   3\n");
 654         fprintf(th, "#define Q_EMPT_T   4\n");
 655         fprintf(th, "#define Q_FULL_T   5\n");
 656         fprintf(th, "#define TIMEOUT_F  6\n");
 657         fprintf(th, "#define GLOBAL     7\n");
 658         fprintf(th, "#define BAD        8\n");
 659         fprintf(th, "#define ALPHA_F    9\n");
 660
 661         fprintf(tc, "int\n");
 662         fprintf(tc, "q_cond(short II, Trans *t)\n");
 663         fprintf(tc, "{  int i = 0;\n");
 664         fprintf(tc, "   for (i = 0; i < 6; i++)\n");
 665         fprintf(tc, "   {       if (t->ty[i] == TIMEOUT_F) return %s;\n",
 666                                         (Etimeouts)?"(!(trpt->tau&1))":"1");
 667         fprintf(tc, "           if (t->ty[i] == ALPHA_F)\n");
 668         fprintf(tc, "#ifdef GLOB_ALPHA\n");
 669         fprintf(tc, "                   return 0;\n");
 670         fprintf(tc, "#else\n\t\t\treturn ");
 671         fprintf(tc, "(II+1 == (short) now._nr_pr && II+1 < MAXPROC);\n");
 672         fprintf(tc, "#endif\n");
 673
 674         /* we switch on the chan name from the spec (as identified by
 675          * the corresponding Nid number) rather than the actual qid
 676          * because we cannot predict at compile time which specific qid
 677          * will be accessed by the statement at runtime.  that is:
 678          * we do not know which qid to pass to q_cond at runtime
 679          * but we do know which name is used.  if it's a chan array, we
 680          * must check all elements of the array for compliance (bummer)
 681          */
 682         fprintf(tc, "           switch (t->qu[i]) {\n");
 683         fprintf(tc, "           case 0: break;\n");
 684
 685         for (walk = all_names; walk; walk = walk->next)
 686         {       s = walk->entry;
 687                 if (s->owner) continue;
 688                 j = find_id(s->context);
 689                 if (s->type == CHAN)
 690                 {       if (last == s->Nid) continue;   /* chan array */
 691                         last = s->Nid;
 692                         Docase(s, j, last);
 693                 } else if (s->type == STRUCT)
 694                 {       /* struct may contain a chan */
 695                         char pregat[128];
 696                         extern void walk2_struct(char *, Symbol *);
 697                         strcpy(pregat, "");
 698                         if (!(s->hidden&1))
 699                         {       if (s->context)
 700                                         sprintf(pregat, "((P%d *)this)->",j);
 701                                 else
 702                                         sprintf(pregat, "now.");
 703                         }
 704                         walk2_struct(pregat, s);
 705                 }
 706         }
 707         fprintf(tc, "   \tdefault: Uerror(\"unknown qid - q_cond\");\n");
 708         fprintf(tc, "   \t\t\treturn 0;\n");
 709         fprintf(tc, "   \t}\n");
 710         fprintf(tc, "   }\n");
 711         fprintf(tc, "   return 1;\n");
 712         fprintf(tc, "}\n");
 713 }
 714
 715 static void
 716 putproc(ProcList *p)
 717 {       Pid = p->tn;
 718         Det = p->det;
 719
 720         if (Pid == claimnr
 721         &&  separate == 1)
 722         {       fprintf(th, "extern uchar reached%d[];\n", Pid);
 723 #if 0
 724                 fprintf(th, "extern short nstates%d;\n", Pid);
 725 #else
 726                 fprintf(th, "\n#define nstates%d        %d\t/* %s */\n",
 727                         Pid, p->s->maxel, p->n->name);
 728 #endif
 729                 fprintf(th, "extern short src_ln%d[];\n", Pid);
 730                 fprintf(th, "extern S_F_MAP src_file%d[];\n", Pid);
 731                 fprintf(th, "#define endstate%d %d\n",
 732                         Pid, p->s->last?p->s->last->seqno:0);
 733                 fprintf(th, "#define src_claim  src_ln%d\n", claimnr);
 734
 735                 return;
 736         }
 737         if (Pid != claimnr
 738         &&  separate == 2)
 739         {       fprintf(th, "extern short src_ln%d[];\n", Pid);
 740                 return;
 741         }
 742
 743         AllGlobal = (p->prov)?1:0;      /* process has provided clause */
 744
 745         fprintf(th, "\n#define nstates%d        %d\t/* %s */\n",
 746                 Pid, p->s->maxel, p->n->name);
 747         if (Pid == claimnr)
 748         fprintf(th, "#define nstates_claim      nstates%d\n", Pid);
 749         if (Pid == eventmapnr)
 750         fprintf(th, "#define nstates_event      nstates%d\n", Pid);
 751
 752         fprintf(th, "#define endstate%d %d\n",
 753                 Pid, p->s->last->seqno);
 754         fprintf(tm, "\n          /* PROC %s */\n", p->n->name);
 755         fprintf(tb, "\n          /* PROC %s */\n", p->n->name);
 756         fprintf(tt, "\n /* proctype %d: %s */\n", Pid, p->n->name);
 757         fprintf(tt, "\n trans[%d] = (Trans **)", Pid);
 758         fprintf(tt, " emalloc(%d*sizeof(Trans *));\n\n", p->s->maxel);
 759
 760         if (Pid == eventmapnr)
 761         {       fprintf(th, "\n#define in_s_scope(x_y3_)        0");
 762                 fprintf(tc, "\n#define in_r_scope(x_y3_)        0");
 763         }
 764
 765         put_seq(p->s, 2, 0);
 766         if (Pid == eventmapnr)
 767         {       fprintf(th, "\n\n");
 768                 fprintf(tc, "\n\n");
 769         }
 770         dumpsrc(p->s->maxel, Pid);
 771 }
 772
 773 static void
 774 addTpe(int x)
 775 {       int i;
 776
 777         if (x <= 2) return;
 778
 779         for (i = 0; i < T_sum; i++)
 780                 if (TPE[i] == x)
 781                         return;
 782         TPE[(T_sum++)%2] = x;
 783 }
 784
 785 static void
 786 cnt_seq(Sequence *s)
 787 {       Element *f;
 788         SeqList *h;
 789
 790         if (s)
 791         for (f = s->frst; f; f = f->nxt)
 792         {       Tpe(f->n);      /* sets EPT */
 793                 addTpe(EPT[0]);
 794                 addTpe(EPT[1]);
 795                 for (h = f->sub; h; h = h->nxt)
 796                         cnt_seq(h->this);
 797                 if (f == s->last)
 798                         break;
 799         }
 800 }
 801
 802 static void
 803 typ_seq(Sequence *s)
 804 {
 805         T_sum = 0;
 806         TPE[0] = 2; TPE[1] = 0;
 807         cnt_seq(s);
 808         if (T_sum > 2)          /* more than one type */
 809         {       TPE[0] = 5*DELTA;       /* non-mixing */
 810                 TPE[1] = 0;
 811         }
 812 }
 813
 814 static int
 815 hidden(Lextok *n)
 816 {
 817         if (n)
 818         switch (n->ntyp) {
 819         case  FULL: case  EMPTY:
 820         case NFULL: case NEMPTY: case TIMEOUT:
 821                 Nn[(T_mus++)%2] = n;
 822                 break;
 823         case '!': case UMIN: case '~': case ASSERT: case 'c':
 824                 (void) hidden(n->lft);
 825                 break;
 826         case '/': case '*': case '-': case '+':
 827         case '%': case LT:  case GT: case '&': case '^':
 828         case '|': case LE:  case GE:  case NE: case '?':
 829         case EQ:  case OR:  case AND: case LSHIFT: case RSHIFT:
 830                 (void) hidden(n->lft);
 831                 (void) hidden(n->rgt);
 832                 break;
 833         }
 834         return T_mus;
 835 }
 836
 837 static int
 838 getNid(Lextok *n)
 839 {
 840         if (n->sym
 841         &&  n->sym->type == STRUCT
 842         &&  n->rgt && n->rgt->lft)
 843                 return getNid(n->rgt->lft);
 844
 845         if (!n->sym || n->sym->Nid == 0)
 846         {       fatal("bad channel name '%s'",
 847                 (n->sym)?n->sym->name:"no name");
 848         }
 849         return n->sym->Nid;
 850 }
 851
 852 static int
 853 valTpe(Lextok *n)
 854 {       int res = 2;
 855         /*
 856         2 = local
 857         2+1         .. 2+1*DELTA = nfull,  's'  - require q_full==false
 858         2+1+1*DELTA .. 2+2*DELTA = nempty, 'r'  - require q_len!=0
 859         2+1+2*DELTA .. 2+3*DELTA = empty        - require q_len==0
 860         2+1+3*DELTA .. 2+4*DELTA = full         - require q_full==true
 861         5*DELTA = non-mixing (i.e., always makes the selection global)
 862         6*DELTA = timeout (conditionally safe)
 863         7*DELTA = @, process deletion (conditionally safe)
 864          */
 865         switch (n->ntyp) { /* a series of fall-thru cases: */
 866         case   FULL:    res += DELTA;           /* add 3*DELTA + chan nr */
 867         case  EMPTY:    res += DELTA;           /* add 2*DELTA + chan nr */
 868         case    'r':
 869         case NEMPTY:    res += DELTA;           /* add 1*DELTA + chan nr */
 870         case    's':
 871         case  NFULL:    res += getNid(n->lft);  /* add channel nr */
 872                         break;
 873
 874         case TIMEOUT:   res = 6*DELTA; break;
 875         case '@':       res = 7*DELTA; break;
 876         default:        break;
 877         }
 878         return res;
 879 }
 880
 881 static void
 882 Tpe(Lextok *n)  /* mixing in selections */
 883 {
 884         EPT[0] = 2; EPT[1] = 0;
 885
 886         if (!n) return;
 887
 888         T_mus = 0;
 889         Nn[0] = Nn[1] = ZN;
 890
 891         if (n->ntyp == 'c')
 892         {       if (hidden(n->lft) > 2)
 893                 {       EPT[0] = 5*DELTA; /* non-mixing */
 894                         EPT[1] = 0;
 895                         return;
 896                 }
 897         } else
 898                 Nn[0] = n;
 899
 900         if (Nn[0]) EPT[0] = valTpe(Nn[0]);
 901         if (Nn[1]) EPT[1] = valTpe(Nn[1]);
 902 }
 903
 904 static void
 905 put_escp(Element *e)
 906 {       int n;
 907         SeqList *x;
 908
 909         if (e->esc /* && e->n->ntyp != GOTO */ && e->n->ntyp != '.')
 910         {       for (x = e->esc, n = 0; x; x = x->nxt, n++)
 911                 {       int i = huntele(x->this->frst, e->status, -1)->seqno;
 912                         fprintf(tt, "\ttrans[%d][%d]->escp[%d] = %d;\n",
 913                                 Pid, e->seqno, n, i);
 914                         fprintf(tt, "\treached%d[%d] = 1;\n",
 915                                 Pid, i);
 916                 }
 917                 for (x = e->esc, n=0; x; x = x->nxt, n++)
 918                 {       fprintf(tt, "   /* escape #%d: %d */\n", n,
 919                                 huntele(x->this->frst, e->status, -1)->seqno);
 920                         put_seq(x->this, 2, 0); /* args?? */
 921                 }
 922                 fprintf(tt, "   /* end-escapes */\n");
 923         }
 924 }
 925
 926 static void
 927 put_sub(Element *e, int Tt0, int Tt1)
 928 {       Sequence *s = e->n->sl->this;
 929         Element *g = ZE;
 930         int a;
 931
 932         patch_atomic(s);
 933         putskip(s->frst->seqno);
 934         g = huntstart(s->frst);
 935         a = g->seqno;
 936
 937         if (0) printf("put_sub %d -> %d -> %d\n", e->seqno, s->frst->seqno, a);
 938
 939         if ((e->n->ntyp == ATOMIC
 940         ||  e->n->ntyp == D_STEP)
 941         &&  scan_seq(s))
 942                 mark_seq(s);
 943         s->last->nxt = e->nxt;
 944
 945         typ_seq(s);     /* sets TPE */
 946
 947         if (e->n->ntyp == D_STEP)
 948         {       int inherit = (e->status&(ATOM|L_ATOM));
 949                 fprintf(tm, "\tcase %d: ", uniq++);
 950                 fprintf(tm, "/* STATE %d - line %d %s - [",
 951                         e->seqno, e->n->ln, e->n->fn->name);
 952                 comment(tm, e->n, 0);
 953                 fprintf(tm, "] */\n\t\t");
 954
 955                 if (s->last->n->ntyp == BREAK)
 956                         OkBreak = target(huntele(s->last->nxt,
 957                                 s->last->status, -1))->Seqno;
 958                 else
 959                         OkBreak = -1;
 960
 961                 if (!putcode(tm, s, e->nxt, 0, e->n->ln, e->seqno))
 962                 {
 963                         fprintf(tm, "\n#if defined(C_States) && (HAS_TRACK==1)\n");
 964                         fprintf(tm, "\t\tc_update((uchar *) &(now.c_state[0]));\n");
 965                         fprintf(tm, "#endif\n");
 966
 967                         fprintf(tm, "\t\t_m = %d", getweight(s->frst->n));
 968                         if (m_loss && s->frst->n->ntyp == 's')
 969                                 fprintf(tm, "+delta_m; delta_m = 0");
 970                         fprintf(tm, "; goto P999;\n\n");
 971                 }
 972
 973                 fprintf(tb, "\tcase %d: ", uniq-1);
 974                 fprintf(tb, "/* STATE %d */\n", e->seqno);
 975                 fprintf(tb, "\t\tsv_restor();\n");
 976                 fprintf(tb, "\t\tgoto R999;\n");
 977                 if (e->nxt)
 978                         a = huntele(e->nxt, e->status, -1)->seqno;
 979                 else
 980                         a = 0;
 981                 tr_map(uniq-1, e);
 982                 fprintf(tt, "/*->*/\ttrans[%d][%d]\t= ",
 983                         Pid, e->seqno);
 984                 fprintf(tt, "settr(%d,%d,%d,%d,%d,\"",
 985                         e->Seqno, D_ATOM|inherit, a, uniq-1, uniq-1);
 986                 comment(tt, e->n, e->seqno);
 987                 fprintf(tt, "\", %d, ", (s->frst->status&I_GLOB)?1:0);
 988                 fprintf(tt, "%d, %d);\n", TPE[0], TPE[1]);
 989                 put_escp(e);
 990         } else
 991         {       /* ATOMIC or NON_ATOMIC */
 992                 fprintf(tt, "\tT = trans[ %d][%d] = ", Pid, e->seqno);
 993                 fprintf(tt, "settr(%d,%d,0,0,0,\"",
 994                         e->Seqno, (e->n->ntyp == ATOMIC)?ATOM:0);
 995                 comment(tt, e->n, e->seqno);
 996                 if ((e->status&CHECK2)
 997                 ||  (g->status&CHECK2))
 998                         s->frst->status |= I_GLOB;
 999                 fprintf(tt, "\", %d, %d, %d);",
1000                         (s->frst->status&I_GLOB)?1:0, Tt0, Tt1);
1001                 blurb(tt, e);
1002                 fprintf(tt, "\tT->nxt\t= ");
1003                 fprintf(tt, "settr(%d,%d,%d,0,0,\"",
1004                         e->Seqno, (e->n->ntyp == ATOMIC)?ATOM:0, a);
1005                 comment(tt, e->n, e->seqno);
1006                 fprintf(tt, "\", %d, ", (s->frst->status&I_GLOB)?1:0);
1007                 if (e->n->ntyp == NON_ATOMIC)
1008                 {       fprintf(tt, "%d, %d);", Tt0, Tt1);
1009                         blurb(tt, e);
1010                         put_seq(s, Tt0, Tt1);
1011                 } else
1012                 {       fprintf(tt, "%d, %d);", TPE[0], TPE[1]);
1013                         blurb(tt, e);
1014                         put_seq(s, TPE[0], TPE[1]);
1015                 }
1016         }
1017 }
1018
1019 typedef struct CaseCache {
1020         int m, b, owner;
1021         Element *e;
1022         Lextok *n;
1023         FSM_use *u;
1024         struct CaseCache *nxt;
1025 } CaseCache;
1026
1027 CaseCache *casing[6];
1028
1029 static int
1030 identical(Lextok *p, Lextok *q)
1031 {
1032         if ((!p && q) || (p && !q))
1033                 return 0;
1034         if (!p)
1035                 return 1;
1036
1037         if (p->ntyp    != q->ntyp
1038         ||  p->ismtyp  != q->ismtyp
1039         ||  p->val     != q->val
1040         ||  p->indstep != q->indstep
1041         ||  p->sym     != q->sym
1042         ||  p->sq      != q->sq
1043         ||  p->sl      != q->sl)
1044                 return 0;
1045
1046         return  identical(p->lft, q->lft)
1047         &&      identical(p->rgt, q->rgt);
1048 }
1049
1050 static int
1051 samedeads(FSM_use *a, FSM_use *b)
1052 {       FSM_use *p, *q;
1053
1054         for (p = a, q = b; p && q; p = p->nxt, q = q->nxt)
1055                 if (p->var != q->var
1056                 ||  p->special != q->special)
1057                         return 0;
1058         return (!p && !q);
1059 }
1060
1061 static Element *
1062 findnext(Element *f)
1063 {       Element *g;
1064
1065         if (f->n->ntyp == GOTO)
1066         {       g = get_lab(f->n, 1);
1067                 return huntele(g, f->status, -1);
1068         }
1069         return f->nxt;
1070 }
1071
1072 static Element *
1073 advance(Element *e, int stopat)
1074 {       Element *f = e;
1075
1076         if (stopat)
1077         while (f && f->seqno != stopat)
1078         {       f = findnext(f);
1079                 switch (f->n->ntyp) {
1080                 case GOTO:
1081                 case '.':
1082                 case PRINT:
1083                 case PRINTM:
1084                         break;
1085                 default:
1086                         return f;
1087                 }
1088         }
1089         return (Element *) 0;
1090 }
1091
1092 static int
1093 equiv_merges(Element *a, Element *b)
1094 {       Element *f, *g;
1095         int stopat_a, stopat_b;
1096
1097         if (a->merge_start)
1098                 stopat_a = a->merge_start;
1099         else
1100                 stopat_a = a->merge;
1101
1102         if (b->merge_start)
1103                 stopat_b = b->merge_start;
1104         else
1105                 stopat_b = b->merge;
1106
1107         if (!stopat_a && !stopat_b)
1108                 return 1;
1109
1110         for (;;)
1111         {
1112                 f = advance(a, stopat_a);
1113                 g = advance(b, stopat_b);
1114                 if (!f && !g)
1115                         return 1;
1116                 if (f && g)
1117                         return identical(f->n, g->n);
1118                 else
1119                         return 0;
1120         }
1121         return 1;
1122 }
1123
1124 static CaseCache *
1125 prev_case(Element *e, int owner)
1126 {       int j; CaseCache *nc;
1127
1128         switch (e->n->ntyp) {
1129         case 'r':       j = 0; break;
1130         case 's':       j = 1; break;
1131         case 'c':       j = 2; break;
1132         case ASGN:      j = 3; break;
1133         case ASSERT:    j = 4; break;
1134         default:        j = 5; break;
1135         }
1136         for (nc = casing[j]; nc; nc = nc->nxt)
1137                 if (identical(nc->n, e->n)
1138                 &&  samedeads(nc->u, e->dead)
1139                 &&  equiv_merges(nc->e, e)
1140                 &&  nc->owner == owner)
1141                         return nc;
1142
1143         return (CaseCache *) 0;
1144 }
1145
1146 static void
1147 new_case(Element *e, int m, int b, int owner)
1148 {       int j; CaseCache *nc;
1149
1150         switch (e->n->ntyp) {
1151         case 'r':       j = 0; break;
1152         case 's':       j = 1; break;
1153         case 'c':       j = 2; break;
1154         case ASGN:      j = 3; break;
1155         case ASSERT:    j = 4; break;
1156         default:        j = 5; break;
1157         }
1158         nc = (CaseCache *) emalloc(sizeof(CaseCache));
1159         nc->owner = owner;
1160         nc->m = m;
1161         nc->b = b;
1162         nc->e = e;
1163         nc->n = e->n;
1164         nc->u = e->dead;
1165         nc->nxt = casing[j];
1166         casing[j] = nc;
1167 }
1168
1169 static int
1170 nr_bup(Element *e)
1171 {       FSM_use *u;
1172         Lextok *v;
1173         int nr = 0;
1174
1175         switch (e->n->ntyp) {
1176         case ASGN:
1177                 nr++;
1178                 break;
1179         case  'r':
1180                 if (e->n->val >= 1)
1181                         nr++;   /* random recv */
1182                 for (v = e->n->rgt; v; v = v->rgt)
1183                 {       if ((v->lft->ntyp == CONST
1184                         ||   v->lft->ntyp == EVAL))
1185                                 continue;
1186                         nr++;
1187                 }
1188                 break;
1189         default:
1190                 break;
1191         }
1192         for (u = e->dead; u; u = u->nxt)
1193         {       switch (u->special) {
1194                 case 2:         /* dead after write */
1195                         if (e->n->ntyp == ASGN
1196                         &&  e->n->rgt->ntyp == CONST
1197                         &&  e->n->rgt->val == 0)
1198                                 break;
1199                         nr++;
1200                         break;
1201                 case 1:         /* dead after read */
1202                         nr++;
1203                         break;
1204         }       }
1205         return nr;
1206 }
1207
1208 static int
1209 nrhops(Element *e)
1210 {       Element *f = e, *g;
1211         int cnt = 0;
1212         int stopat;
1213
1214         if (e->merge_start)
1215                 stopat = e->merge_start;
1216         else
1217                 stopat = e->merge;
1218 #if 0
1219         printf("merge: %d merge_start %d - seqno %d\n",
1220                 e->merge, e->merge_start, e->seqno);
1221 #endif
1222         do {
1223                 cnt += nr_bup(f);
1224
1225                 if (f->n->ntyp == GOTO)
1226                 {       g = get_lab(f->n, 1);
1227                         if (g->seqno == stopat)
1228                                 f = g;
1229                         else
1230                                 f = huntele(g, f->status, stopat);
1231                 } else
1232                 {
1233                         f = f->nxt;
1234                 }
1235
1236                 if (f && !f->merge && !f->merge_single && f->seqno != stopat)
1237                 {       fprintf(tm, "\n\t\tbad hop %s:%d -- at %d, <",
1238                                 f->n->fn->name,f->n->ln, f->seqno);
1239                         comment(tm, f->n, 0);
1240                         fprintf(tm, "> looking for %d -- merge %d:%d:%d\n\t\t",
1241                                 stopat, f->merge, f->merge_start, f->merge_single);
1242                         break;
1243                 }
1244         } while (f && f->seqno != stopat);
1245
1246         return cnt;
1247 }
1248
1249 static void
1250 check_needed(void)
1251 {
1252         if (multi_needed)
1253         {       fprintf(tm, "(trpt+1)->bup.ovals = grab_ints(%d);\n\t\t",
1254                         multi_needed);
1255                 multi_undo = multi_needed;
1256                 multi_needed = 0;
1257         }
1258 }
1259
1260 static void
1261 doforward(FILE *tm, Element *e)
1262 {       FSM_use *u;
1263
1264         putstmnt(tm, e->n, e->seqno);
1265
1266         if (e->n->ntyp != ELSE && Det)
1267         {       fprintf(tm, ";\n\t\tif (trpt->o_pm&1)\n\t\t");
1268                 fprintf(tm, "\tuerror(\"non-determinism in D_proctype\")");
1269         }
1270         if (deadvar && !has_code)
1271         for (u = e->dead; u; u = u->nxt)
1272         {       fprintf(tm, ";\n\t\t/* dead %d: %s */  ",
1273                         u->special, u->var->name);
1274
1275                 switch (u->special) {
1276                 case 2:         /* dead after write -- lval already bupped */
1277                         if (e->n->ntyp == ASGN) /* could be recv or asgn */
1278                         {       if (e->n->rgt->ntyp == CONST
1279                                 &&  e->n->rgt->val == 0)
1280                                         continue;       /* already set to 0 */
1281                         }
1282                         if (e->n->ntyp != 'r')
1283                         {       XZ.sym = u->var;
1284                                 fprintf(tm, "\n#ifdef HAS_CODE\n");
1285                                 fprintf(tm, "\t\tif (!readtrail)\n");
1286                                 fprintf(tm, "#endif\n\t\t\t");
1287                                 putname(tm, "", &XZ, 0, " = 0");
1288                                 break;
1289                         } /* else fall through */
1290                 case 1:         /* dead after read -- add asgn of rval -- needs bup */
1291                         YZ[YZmax].sym = u->var; /* store for pan.b */
1292                         CnT[YZcnt]++;           /* this step added bups */
1293                         if (multi_oval)
1294                         {       check_needed();
1295                                 fprintf(tm, "(trpt+1)->bup.ovals[%d] = ",
1296                                         multi_oval-1);
1297                                 multi_oval++;
1298                         } else
1299                                 fprintf(tm, "(trpt+1)->bup.oval = ");
1300                         putname(tm, "", &YZ[YZmax], 0, ";\n");
1301                         fprintf(tm, "#ifdef HAS_CODE\n");
1302                         fprintf(tm, "\t\tif (!readtrail)\n");
1303                         fprintf(tm, "#endif\n\t\t\t");
1304                         putname(tm, "", &YZ[YZmax], 0, " = 0");
1305                         YZmax++;
1306                         break;
1307         }       }
1308         fprintf(tm, ";\n\t\t");
1309 }
1310
1311 static int
1312 dobackward(Element *e, int casenr)
1313 {
1314         if (!any_undo(e->n) && CnT[YZcnt] == 0)
1315         {       YZcnt--;
1316                 return 0;
1317         }
1318
1319         if (!didcase)
1320         {       fprintf(tb, "\n\tcase %d: ", casenr);
1321                 fprintf(tb, "/* STATE %d */\n\t\t", e->seqno);
1322                 didcase++;
1323         }
1324
1325         _isok++;
1326         while (CnT[YZcnt] > 0)  /* undo dead variable resets */
1327         {       CnT[YZcnt]--;
1328                 YZmax--;
1329                 if (YZmax < 0)
1330                         fatal("cannot happen, dobackward", (char *)0);
1331                 fprintf(tb, ";\n\t/* %d */\t", YZmax);
1332                 putname(tb, "", &YZ[YZmax], 0, " = trpt->bup.oval");
1333                 if (multi_oval > 0)
1334                 {       multi_oval--;
1335                         fprintf(tb, "s[%d]", multi_oval-1);
1336                 }
1337         }
1338
1339         if (e->n->ntyp != '.')
1340         {       fprintf(tb, ";\n\t\t");
1341                 undostmnt(e->n, e->seqno);
1342         }
1343         _isok--;
1344
1345         YZcnt--;
1346         return 1;
1347 }
1348
1349 static void
1350 lastfirst(int stopat, Element *fin, int casenr)
1351 {       Element *f = fin, *g;
1352
1353         if (f->n->ntyp == GOTO)
1354         {       g = get_lab(f->n, 1);
1355                 if (g->seqno == stopat)
1356                         f = g;
1357                 else
1358                         f = huntele(g, f->status, stopat);
1359         } else
1360                 f = f->nxt;
1361
1362         if (!f || f->seqno == stopat
1363         || (!f->merge && !f->merge_single))
1364                 return;
1365         lastfirst(stopat, f, casenr);
1366 #if 0
1367         fprintf(tb, "\n\t/* merge %d -- %d:%d %d:%d:%d (casenr %d)      ",
1368                 YZcnt,
1369                 f->merge_start, f->merge,
1370                 f->seqno, f?f->seqno:-1, stopat,
1371                 casenr);
1372         comment(tb, f->n, 0);
1373         fprintf(tb, " */\n");
1374         fflush(tb);
1375 #endif
1376         dobackward(f, casenr);
1377 }
1378
1379 static int modifier;
1380
1381 static void
1382 lab_transfer(Element *to, Element *from)
1383 {       Symbol *ns, *s = has_lab(from, (1|2|4));
1384         Symbol *oc;
1385         int ltp, usedit=0;
1386
1387         if (!s) return;
1388
1389         /* "from" could have all three labels -- rename
1390          * to prevent jumps to the transfered copies
1391          */
1392         oc = context;   /* remember */
1393         for (ltp = 1; ltp < 8; ltp *= 2)        /* 1, 2, and 4 */
1394                 if ((s = has_lab(from, ltp)) != (Symbol *) 0)
1395                 {       ns = (Symbol *) emalloc(sizeof(Symbol));
1396                         ns->name = (char *) emalloc((int) strlen(s->name) + 4);
1397                         sprintf(ns->name, "%s%d", s->name, modifier);
1398
1399                         context = s->context;
1400                         set_lab(ns, to);
1401                         usedit++;
1402                 }
1403         context = oc;   /* restore */
1404         if (usedit)
1405         {       if (modifier++ > 990)
1406                         fatal("modifier overflow error", (char *) 0);
1407         }
1408 }
1409
1410 static int
1411 case_cache(Element *e, int a)
1412 {       int bupcase = 0, casenr = uniq, fromcache = 0;
1413         CaseCache *Cached = (CaseCache *) 0;
1414         Element *f, *g;
1415         int j, nrbups, mark, target;
1416         extern int ccache;
1417
1418         mark = (e->status&ATOM); /* could lose atomicity in a merge chain */
1419
1420         if (e->merge_mark > 0
1421         ||  (merger && e->merge_in == 0))
1422         {       /* state nominally unreachable (part of merge chains) */
1423                 if (e->n->ntyp != '.'
1424                 &&  e->n->ntyp != GOTO)
1425                 {       fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
1426                         fprintf(tt, "settr(0,0,0,0,0,\"");
1427                         comment(tt, e->n, e->seqno);
1428                         fprintf(tt, "\",0,0,0);\n");
1429                 } else
1430                 {       fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
1431                         casenr = 1; /* mhs example */
1432                         j = a;
1433                         goto haveit; /* pakula's example */
1434                 }
1435
1436                 return -1;
1437         }
1438
1439         fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
1440
1441         if (ccache
1442         &&  Pid != claimnr
1443         &&  Pid != eventmapnr
1444         && (Cached = prev_case(e, Pid)))
1445         {       bupcase = Cached->b;
1446                 casenr  = Cached->m;
1447                 fromcache = 1;
1448
1449                 fprintf(tm, "/* STATE %d - line %d %s - [",
1450                         e->seqno, e->n->ln, e->n->fn->name);
1451                 comment(tm, e->n, 0);
1452                 fprintf(tm, "] (%d:%d - %d) same as %d (%d:%d - %d) */\n",
1453                         e->merge_start, e->merge, e->merge_in,
1454                         casenr,
1455                         Cached->e->merge_start, Cached->e->merge, Cached->e->merge_in);
1456
1457                 goto gotit;
1458         }
1459
1460         fprintf(tm, "\tcase %d: /* STATE %d - line %d %s - [",
1461                 uniq++, e->seqno, e->n->ln, e->n->fn->name);
1462         comment(tm, e->n, 0);
1463         nrbups = (e->merge || e->merge_start) ? nrhops(e) : nr_bup(e);
1464         fprintf(tm, "] (%d:%d:%d - %d) */\n\t\t",
1465                 e->merge_start, e->merge, nrbups, e->merge_in);
1466
1467         if (nrbups > MAXMERGE-1)
1468                 fatal("merge requires more than 256 bups", (char *)0);
1469
1470         if (e->n->ntyp != 'r' && Pid != claimnr && Pid != eventmapnr)
1471                 fprintf(tm, "IfNotBlocked\n\t\t");
1472
1473         if (multi_needed != 0 || multi_undo != 0)
1474                 fatal("cannot happen, case_cache", (char *) 0);
1475
1476         if (nrbups > 1)
1477         {       multi_oval = 1;
1478                 multi_needed = nrbups; /* allocated after edge condition */
1479         } else
1480                 multi_oval = 0;
1481
1482         memset(CnT, 0, sizeof(CnT));
1483         YZmax = YZcnt = 0;
1484
1485 /* NEW 4.2.6 */
1486         if (Pid == claimnr)
1487         {
1488                 fprintf(tm, "\n#if defined(VERI) && !defined(NP)\n\t\t");
1489                 fprintf(tm, "{  static int reported%d = 0;\n\t\t", e->seqno);
1490                 /* source state changes in retrans and must be looked up in frm_st0[t->forw] */
1491                 fprintf(tm, "   if (verbose && !reported%d)\n\t\t", e->seqno);
1492                 fprintf(tm, "   {       printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",\n\t\t");
1493                 fprintf(tm, "                   depth, frm_st0[t->forw], src_claim[%d]);\n\t\t", e->seqno);
1494                 fprintf(tm, "           reported%d = 1;\n\t\t", e->seqno);
1495                 fprintf(tm, "           fflush(stdout);\n\t\t");
1496                 fprintf(tm, "}  }\n");
1497                 fprintf(tm, "#endif\n\t\t");
1498         }
1499 /* end */
1500
1501         /* the src xrefs have the numbers in e->seqno builtin */
1502         fprintf(tm, "reached[%d][%d] = 1;\n\t\t", Pid, e->seqno);
1503
1504         doforward(tm, e);
1505
1506         if (e->merge_start)
1507                 target = e->merge_start;
1508         else
1509                 target = e->merge;
1510
1511         if (target)
1512         {       f = e;
1513
1514 more:           if (f->n->ntyp == GOTO)
1515                 {       g = get_lab(f->n, 1);
1516                         if (g->seqno == target)
1517                                 f = g;
1518                         else
1519                                 f = huntele(g, f->status, target);
1520                 } else
1521                         f = f->nxt;
1522
1523
1524                 if (f && f->seqno != target)
1525                 {       if (!f->merge && !f->merge_single)
1526                         {       fprintf(tm, "/* stop at bad hop %d, %d */\n\t\t",
1527                                         f->seqno, target);
1528                                 goto out;
1529                         }
1530                         fprintf(tm, "/* merge: ");
1531                         comment(tm, f->n, 0);
1532                         fprintf(tm,  "(%d, %d, %d) */\n\t\t", f->merge, f->seqno, target);
1533                         fprintf(tm, "reached[%d][%d] = 1;\n\t\t", Pid, f->seqno);
1534                         YZcnt++;
1535                         lab_transfer(e, f);
1536                         mark = f->status&(ATOM|L_ATOM); /* last step wins */
1537                         doforward(tm, f);
1538                         if (f->merge_in == 1) f->merge_mark++;
1539
1540                         goto more;
1541         }       }
1542 out:
1543         fprintf(tm, "_m = %d", getweight(e->n));
1544         if (m_loss && e->n->ntyp == 's') fprintf(tm, "+delta_m; delta_m = 0");
1545         fprintf(tm, "; goto P999; /* %d */\n", YZcnt);
1546
1547         multi_needed = 0;
1548         didcase = 0;
1549
1550         if (target)
1551                 lastfirst(target, e, casenr); /* mergesteps only */
1552
1553         dobackward(e, casenr);                  /* the original step */
1554
1555         fprintf(tb, ";\n\t\t");
1556
1557         if (e->merge || e->merge_start)
1558         {       if (!didcase)
1559                 {       fprintf(tb, "\n\tcase %d: ", casenr);
1560                         fprintf(tb, "/* STATE %d */", e->seqno);
1561                         didcase++;
1562                 } else
1563                         fprintf(tb, ";");
1564         } else
1565                 fprintf(tb, ";");
1566         fprintf(tb, "\n\t\t");
1567
1568         if (multi_undo)
1569         {       fprintf(tb, "ungrab_ints(trpt->bup.ovals, %d);\n\t\t",
1570                         multi_undo);
1571                 multi_undo = 0;
1572         }
1573         if (didcase)
1574         {       fprintf(tb, "goto R999;\n");
1575                 bupcase = casenr;
1576         }
1577
1578         if (!e->merge && !e->merge_start)
1579                 new_case(e, casenr, bupcase, Pid);
1580
1581 gotit:
1582         j = a;
1583         if (e->merge_start)
1584                 j = e->merge_start;
1585         else if (e->merge)
1586                 j = e->merge;
1587 haveit:
1588         fprintf(tt, "%ssettr(%d,%d,%d,%d,%d,\"", fromcache?"/* c */ ":"",
1589                 e->Seqno, mark, j, casenr, bupcase);
1590
1591         return (fromcache)?0:casenr;
1592 }
1593
1594 static void
1595 put_el(Element *e, int Tt0, int Tt1)
1596 {       int a, casenr, Global_ref;
1597         Element *g = ZE;
1598
1599         if (e->n->ntyp == GOTO)
1600         {       g = get_lab(e->n, 1);
1601                 g = huntele(g, e->status, -1);
1602                 cross_dsteps(e->n, g->n);
1603                 a = g->seqno;
1604         } else if (e->nxt)
1605         {       g = huntele(e->nxt, e->status, -1);
1606                 a = g->seqno;
1607         } else
1608                 a = 0;
1609         if (g
1610         &&  (g->status&CHECK2   /* entering remotely ref'd state */
1611         ||   e->status&CHECK2)) /* leaving  remotely ref'd state */
1612                 e->status |= I_GLOB;
1613
1614         /* don't remove dead edges in here, to preserve structure of fsm */
1615         if (e->merge_start || e->merge)
1616                 goto non_generic;
1617
1618         /*** avoid duplicate or redundant cases in pan.m ***/
1619         switch (e->n->ntyp) {
1620         case ELSE:
1621                 casenr = 2; /* standard else */
1622                 putskip(e->seqno);
1623                 goto generic_case;
1624                 /* break; */
1625         case '.':
1626         case GOTO:
1627         case BREAK:
1628                 putskip(e->seqno);
1629                 casenr = 1; /* standard goto */
1630 generic_case:   fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
1631                 fprintf(tt, "settr(%d,%d,%d,%d,0,\"",
1632                         e->Seqno, e->status&ATOM, a, casenr);
1633                 break;
1634 #ifndef PRINTF
1635         case PRINT:
1636                 goto non_generic;
1637         case PRINTM:
1638                 goto non_generic;
1639 #endif
1640         case 'c':
1641                 if (e->n->lft->ntyp == CONST
1642                 &&  e->n->lft->val == 1)        /* skip or true */
1643                 {       casenr = 1;
1644                         putskip(e->seqno);
1645                         goto generic_case;
1646                 }
1647                 goto non_generic;
1648
1649         default:
1650 non_generic:
1651                 casenr = case_cache(e, a);
1652                 if (casenr < 0) return; /* unreachable state */
1653                 break;
1654         }
1655         /* tailend of settr(...); */
1656         Global_ref = (e->status&I_GLOB)?1:has_global(e->n);
1657         comment(tt, e->n, e->seqno);
1658         fprintf(tt, "\", %d, ", Global_ref);
1659         if (Tt0 != 2)
1660         {       fprintf(tt, "%d, %d);", Tt0, Tt1);
1661         } else
1662         {       Tpe(e->n);      /* sets EPT */
1663                 fprintf(tt, "%d, %d);", EPT[0], EPT[1]);
1664         }
1665         if ((e->merge_start && e->merge_start != a)
1666         ||  (e->merge && e->merge != a))
1667         {       fprintf(tt, " /* m: %d -> %d,%d */\n",
1668                         a, e->merge_start, e->merge);
1669                 fprintf(tt, "   reached%d[%d] = 1;",
1670                         Pid, a); /* Sheinman's example */
1671         }
1672         fprintf(tt, "\n");
1673
1674         if (casenr > 2)
1675                 tr_map(casenr, e);
1676         put_escp(e);
1677 }
1678
1679 static void
1680 nested_unless(Element *e, Element *g)
1681 {       struct SeqList *y = e->esc, *z = g->esc;
1682
1683         for ( ; y && z; y = y->nxt, z = z->nxt)
1684                 if (z->this != y->this)
1685                         break;
1686         if (!y && !z)
1687                 return;
1688
1689         if (g->n->ntyp != GOTO
1690         &&  g->n->ntyp != '.'
1691         &&  e->sub->nxt)
1692         {       printf("error: (%s:%d) saw 'unless' on a guard:\n",
1693                         (e->n)?e->n->fn->name:"-",
1694                         (e->n)?e->n->ln:0);
1695                 printf("=====>instead of\n");
1696                 printf("        do (or if)\n");
1697                 printf("        :: ...\n");
1698                 printf("        :: stmnt1 unless stmnt2\n");
1699                 printf("        od (of fi)\n");
1700                 printf("=====>use\n");
1701                 printf("        do (or if)\n");
1702                 printf("        :: ...\n");
1703                 printf("        :: stmnt1\n");
1704                 printf("        od (or fi) unless stmnt2\n");
1705                 printf("=====>or rewrite\n");
1706         }
1707 }
1708
1709 static void
1710 put_seq(Sequence *s, int Tt0, int Tt1)
1711 {       SeqList *h;
1712         Element *e, *g;
1713         int a, deadlink;
1714
1715         if (0) printf("put_seq %d\n", s->frst->seqno);
1716
1717         for (e = s->frst; e; e = e->nxt)
1718         {
1719                 if (0) printf(" step %d\n", e->seqno);
1720                 if (e->status & DONE)
1721                 {
1722                         if (0) printf("         done before\n");
1723                         goto checklast;
1724                 }
1725                 e->status |= DONE;
1726
1727                 if (e->n->ln)
1728                         putsrc(e);
1729
1730                 if (e->n->ntyp == UNLESS)
1731                 {
1732                         if (0) printf("         an unless\n");
1733                         put_seq(e->sub->this, Tt0, Tt1);
1734                 } else if (e->sub)
1735                 {
1736                         if (0) printf("         has sub\n");
1737                         fprintf(tt, "\tT = trans[%d][%d] = ",
1738                                 Pid, e->seqno);
1739                         fprintf(tt, "settr(%d,%d,0,0,0,\"",
1740                                 e->Seqno, e->status&ATOM);
1741                         comment(tt, e->n, e->seqno);
1742                         if (e->status&CHECK2)
1743                                 e->status |= I_GLOB;
1744                         fprintf(tt, "\", %d, %d, %d);",
1745                                 (e->status&I_GLOB)?1:0, Tt0, Tt1);
1746                         blurb(tt, e);
1747                         for (h = e->sub; h; h = h->nxt)
1748                         {       putskip(h->this->frst->seqno);
1749                                 g = huntstart(h->this->frst);
1750                                 if (g->esc)
1751                                         nested_unless(e, g);
1752                                 a = g->seqno;
1753
1754                                 if (g->n->ntyp == 'c'
1755                                 &&  g->n->lft->ntyp == CONST
1756                                 &&  g->n->lft->val == 0         /* 0 or false */
1757                                 && !g->esc)
1758                                 {       fprintf(tt, "#if 0\n\t/* dead link: */\n");
1759                                         deadlink = 1;
1760                                         if (verbose&32)
1761                                         printf("spin: line %3d  %s, Warning: condition is always false\n",
1762                                                 g->n->ln, g->n->fn?g->n->fn->name:"");
1763                                 } else
1764                                         deadlink = 0;
1765                                 if (0) printf("                 settr %d %d\n", a, 0);
1766                                 if (h->nxt)
1767                                         fprintf(tt, "\tT = T->nxt\t= ");
1768                                 else
1769                                         fprintf(tt, "\t    T->nxt\t= ");
1770                                 fprintf(tt, "settr(%d,%d,%d,0,0,\"",
1771                                         e->Seqno, e->status&ATOM, a);
1772                                 comment(tt, e->n, e->seqno);
1773                                 if (g->status&CHECK2)
1774                                         h->this->frst->status |= I_GLOB;
1775                                 fprintf(tt, "\", %d, %d, %d);",
1776                                         (h->this->frst->status&I_GLOB)?1:0,
1777                                         Tt0, Tt1);
1778                                 blurb(tt, e);
1779                                 if (deadlink)
1780                                         fprintf(tt, "#endif\n");
1781                         }
1782                         for (h = e->sub; h; h = h->nxt)
1783                                 put_seq(h->this, Tt0, Tt1);
1784                 } else
1785                 {
1786                         if (0) printf("         [non]atomic %d\n", e->n->ntyp);
1787                         if (e->n->ntyp == ATOMIC
1788                         ||  e->n->ntyp == D_STEP
1789                         ||  e->n->ntyp == NON_ATOMIC)
1790                                 put_sub(e, Tt0, Tt1);
1791                         else
1792                         {
1793                                 if (0) printf("                 put_el %d\n", e->seqno);
1794                                 put_el(e, Tt0, Tt1);
1795                         }
1796                 }
1797 checklast:      if (e == s->last)
1798                         break;
1799         }
1800         if (0) printf("put_seq done\n");
1801 }
1802
1803 static void
1804 patch_atomic(Sequence *s)       /* catch goto's that break the chain */
1805 {       Element *f, *g;
1806         SeqList *h;
1807
1808         for (f = s->frst; f ; f = f->nxt)
1809         {
1810                 if (f->n && f->n->ntyp == GOTO)
1811                 {       g = get_lab(f->n,1);
1812                         cross_dsteps(f->n, g->n);
1813                         if ((f->status & (ATOM|L_ATOM))
1814                         && !(g->status & (ATOM|L_ATOM)))
1815                         {       f->status &= ~ATOM;
1816                                 f->status |= L_ATOM;
1817                         }
1818                         /* bridge atomics */
1819                         if ((f->status & L_ATOM)
1820                         &&  (g->status & (ATOM|L_ATOM)))
1821                         {       f->status &= ~L_ATOM;
1822                                 f->status |= ATOM;
1823                         }
1824                 } else
1825                 for (h = f->sub; h; h = h->nxt)
1826                         patch_atomic(h->this);
1827                 if (f == s->extent)
1828                         break;
1829         }
1830 }
1831
1832 static void
1833 mark_seq(Sequence *s)
1834 {       Element *f;
1835         SeqList *h;
1836
1837         for (f = s->frst; f; f = f->nxt)
1838         {       f->status |= I_GLOB;
1839
1840                 if (f->n->ntyp == ATOMIC
1841                 ||  f->n->ntyp == NON_ATOMIC
1842                 ||  f->n->ntyp == D_STEP)
1843                         mark_seq(f->n->sl->this);
1844
1845                 for (h = f->sub; h; h = h->nxt)
1846                         mark_seq(h->this);
1847                 if (f == s->last)
1848                         return;
1849         }
1850 }
1851
1852 static Element *
1853 find_target(Element *e)
1854 {       Element *f;
1855
1856         if (!e) return e;
1857
1858         if (t_cyc++ > 32)
1859         {       fatal("cycle of goto jumps", (char *) 0);
1860         }
1861         switch (e->n->ntyp) {
1862         case  GOTO:
1863                 f = get_lab(e->n,1);
1864                 cross_dsteps(e->n, f->n);
1865                 f = find_target(f);
1866                 break;
1867         case BREAK:
1868                 if (e->nxt)
1869                 {       f = find_target(huntele(e->nxt, e->status, -1));
1870                         break;  /* 4.3.0 -- was missing */
1871                 }
1872                 /* else fall through */
1873         default:
1874                 f = e;
1875                 break;
1876         }
1877         return f;
1878 }
1879
1880 Element *
1881 target(Element *e)
1882 {
1883         if (!e) return e;
1884         lineno = e->n->ln;
1885         Fname  = e->n->fn;
1886         t_cyc = 0;
1887         return find_target(e);
1888 }
1889
1890 static int
1891 scan_seq(Sequence *s)
1892 {       Element *f, *g;
1893         SeqList *h;
1894
1895         for (f = s->frst; f; f = f->nxt)
1896         {       if ((f->status&CHECK2)
1897                 ||  has_global(f->n))
1898                         return 1;
1899                 if (f->n->ntyp == GOTO) /* may reach other atomic */
1900                 {
1901 #if 0
1902                         /* if jumping from an atomic without globals into
1903                          * one with globals, this does the wrong thing
1904                          * example by Claus Traulsen, 22 June 2007
1905                          */
1906                         g = target(f);
1907                         if (g
1908                         && !(f->status & L_ATOM)
1909                         && !(g->status & (ATOM|L_ATOM)))
1910 #endif
1911                         {       fprintf(tt, "   /* mark-down line %d */\n",
1912                                         f->n->ln);
1913                                 return 1; /* assume worst case */
1914                 }       }
1915                 for (h = f->sub; h; h = h->nxt)
1916                         if (scan_seq(h->this))
1917                                 return 1;
1918                 if (f == s->last)
1919                         break;
1920         }
1921         return 0;
1922 }
1923
1924 static int
1925 glob_args(Lextok *n)
1926 {       int result = 0;
1927         Lextok *v;
1928
1929         for (v = n->rgt; v; v = v->rgt)
1930         {       if (v->lft->ntyp == CONST)
1931                         continue;
1932                 if (v->lft->ntyp == EVAL)
1933                         result += has_global(v->lft->lft);
1934                 else
1935                         result += has_global(v->lft);
1936         }
1937         return result;
1938 }
1939
1940 int
1941 has_global(Lextok *n)
1942 {       Lextok *v; extern int runsafe;
1943
1944         if (!n) return 0;
1945         if (AllGlobal) return 1;        /* global provided clause */
1946
1947         switch (n->ntyp) {
1948         case ATOMIC:
1949         case D_STEP:
1950         case NON_ATOMIC:
1951                 return scan_seq(n->sl->this);
1952
1953         case '.':
1954         case BREAK:
1955         case GOTO:
1956         case CONST:
1957                 return 0;
1958
1959         case   ELSE: return n->val; /* true if combined with chan refs */
1960
1961         case    's': return glob_args(n)!=0 || ((n->sym->xu&(XS|XX)) != XS);
1962         case    'r': return glob_args(n)!=0 || ((n->sym->xu&(XR|XX)) != XR);
1963         case    'R': return glob_args(n)!=0 || (((n->sym->xu)&(XR|XS|XX)) != (XR|XS));
1964         case NEMPTY: return ((n->sym->xu&(XR|XX)) != XR);
1965         case  NFULL: return ((n->sym->xu&(XS|XX)) != XS);
1966         case   FULL: return ((n->sym->xu&(XR|XX)) != XR);
1967         case  EMPTY: return ((n->sym->xu&(XS|XX)) != XS);
1968         case  LEN:   return (((n->sym->xu)&(XR|XS|XX)) != (XR|XS));
1969
1970         case   NAME:
1971                 if (n->sym->context
1972                 || (n->sym->hidden&64)
1973                 ||  strcmp(n->sym->name, "_pid") == 0
1974                 ||  strcmp(n->sym->name, "_") == 0)
1975                         return 0;
1976                 return 1;
1977
1978         case RUN: return 1-runsafe;
1979
1980         case C_CODE: case C_EXPR:
1981                 return glob_inline(n->sym->name);
1982
1983         case ENABLED: case PC_VAL: case NONPROGRESS:
1984         case 'p': case 'q':
1985         case TIMEOUT:
1986                 return 1;
1987
1988         /*      @ was 1 (global) since 2.8.5
1989                 in 3.0 it is considered local and
1990                 conditionally safe, provided:
1991                         II is the youngest process
1992                         and nrprocs < MAXPROCS
1993         */
1994         case '@': return 0;
1995
1996         case '!': case UMIN: case '~': case ASSERT:
1997                 return has_global(n->lft);
1998
1999         case '/': case '*': case '-': case '+':
2000         case '%': case LT:  case GT: case '&': case '^':
2001         case '|': case LE:  case GE:  case NE: case '?':
2002         case EQ:  case OR:  case AND: case LSHIFT:
2003         case RSHIFT: case 'c': case ASGN:
2004                 return has_global(n->lft) || has_global(n->rgt);
2005
2006         case PRINT:
2007                 for (v = n->lft; v; v = v->rgt)
2008                         if (has_global(v->lft)) return 1;
2009                 return 0;
2010         case PRINTM:
2011                 return has_global(n->lft);
2012         }
2013         return 0;
2014 }
2015
2016 static void
2017 Bailout(FILE *fd, char *str)
2018 {
2019         if (!GenCode)
2020                 fprintf(fd, "continue%s", str);
2021         else if (IsGuard)
2022                 fprintf(fd, "%s%s", NextLab[Level], str);
2023         else
2024                 fprintf(fd, "Uerror(\"block in step seq\")%s", str);
2025 }
2026
2027 #define cat0(x)         putstmnt(fd,now->lft,m); fprintf(fd, x); \
2028                         putstmnt(fd,now->rgt,m)
2029 #define cat1(x)         fprintf(fd,"("); cat0(x); fprintf(fd,")")
2030 #define cat2(x,y)       fprintf(fd,x); putstmnt(fd,y,m)
2031 #define cat3(x,y,z)     fprintf(fd,x); putstmnt(fd,y,m); fprintf(fd,z)
2032
2033 void
2034 putstmnt(FILE *fd, Lextok *now, int m)
2035 {       Lextok *v;
2036         int i, j;
2037
2038         if (!now) { fprintf(fd, "0"); return; }
2039         lineno = now->ln;
2040         Fname  = now->fn;
2041
2042         switch (now->ntyp) {
2043         case CONST:     fprintf(fd, "%d", now->val); break;
2044         case '!':       cat3(" !(", now->lft, ")"); break;
2045         case UMIN:      cat3(" -(", now->lft, ")"); break;
2046         case '~':       cat3(" ~(", now->lft, ")"); break;
2047
2048         case '/':       cat1("/");  break;
2049         case '*':       cat1("*");  break;
2050         case '-':       cat1("-");  break;
2051         case '+':       cat1("+");  break;
2052         case '%':       cat1("%%"); break;
2053         case '&':       cat1("&");  break;
2054         case '^':       cat1("^");  break;
2055         case '|':       cat1("|");  break;
2056         case LT:        cat1("<");  break;
2057         case GT:        cat1(">");  break;
2058         case LE:        cat1("<="); break;
2059         case GE:        cat1(">="); break;
2060         case NE:        cat1("!="); break;
2061         case EQ:        cat1("=="); break;
2062         case OR:        cat1("||"); break;
2063         case AND:       cat1("&&"); break;
2064         case LSHIFT:    cat1("<<"); break;
2065         case RSHIFT:    cat1(">>"); break;
2066
2067         case TIMEOUT:
2068                 if (separate == 2)
2069                         fprintf(fd, "((tau)&1)");
2070                 else
2071                         fprintf(fd, "((trpt->tau)&1)");
2072                 if (GenCode)
2073                  printf("spin: line %3d, warning: 'timeout' in d_step sequence\n",
2074                         lineno);
2075                 /* is okay as a guard */
2076                 break;
2077
2078         case RUN:
2079                 if (claimproc
2080                 &&  strcmp(now->sym->name, claimproc) == 0)
2081                         fatal("claim %s, (not runnable)", claimproc);
2082                 if (eventmap
2083                 &&  strcmp(now->sym->name, eventmap) == 0)
2084                         fatal("eventmap %s, (not runnable)", eventmap);
2085
2086                 if (GenCode)
2087                   fatal("'run' in d_step sequence (use atomic)",
2088                         (char *)0);
2089
2090                 fprintf(fd,"addproc(%d", fproc(now->sym->name));
2091                 for (v = now->lft, i = 0; v; v = v->rgt, i++)
2092                 {       cat2(", ", v->lft);
2093                 }
2094                 check_param_count(i, now);
2095
2096                 if (i > Npars)
2097                 {       printf("\t%d parameters used, max %d expected\n", i, Npars);
2098                         fatal("too many parameters in run %s(...)",
2099                         now->sym->name);
2100                 }
2101                 for ( ; i < Npars; i++)
2102                         fprintf(fd, ", 0");
2103                 fprintf(fd, ")");
2104                 break;
2105
2106         case ENABLED:
2107                 cat3("enabled(II, ", now->lft, ")");
2108                 break;
2109
2110         case NONPROGRESS:
2111                 /* o_pm&4=progress, tau&128=claim stutter */
2112                 if (separate == 2)
2113                 fprintf(fd, "(!(o_pm&4) && !(tau&128))");
2114                 else
2115                 fprintf(fd, "(!(trpt->o_pm&4) && !(trpt->tau&128))");
2116                 break;
2117
2118         case PC_VAL:
2119                 cat3("((P0 *) Pptr(", now->lft, "+BASE))->_p");
2120                 break;
2121
2122         case LEN:
2123                 if (!terse && !TestOnly && has_xu)
2124                 {       fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2125                         putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
2126                         putname(fd, "q_R_check(", now->lft, m, "");
2127                         fprintf(fd, ", II)) &&\n\t\t");
2128                         putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
2129                         putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
2130                         fprintf(fd, "\n#endif\n\t\t");
2131                 }
2132                 putname(fd, "q_len(", now->lft, m, ")");
2133                 break;
2134
2135         case FULL:
2136                 if (!terse && !TestOnly && has_xu)
2137                 {       fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2138                         putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
2139                         putname(fd, "q_R_check(", now->lft, m, "");
2140                         fprintf(fd, ", II)) &&\n\t\t");
2141                         putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
2142                         putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
2143                         fprintf(fd, "\n#endif\n\t\t");
2144                 }
2145                 putname(fd, "q_full(", now->lft, m, ")");
2146                 break;
2147
2148         case EMPTY:
2149                 if (!terse && !TestOnly && has_xu)
2150                 {       fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2151                         putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
2152                         putname(fd, "q_R_check(", now->lft, m, "");
2153                         fprintf(fd, ", II)) &&\n\t\t");
2154                         putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
2155                         putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
2156                         fprintf(fd, "\n#endif\n\t\t");
2157                 }
2158                 putname(fd, "(q_len(", now->lft, m, ")==0)");
2159                 break;
2160
2161         case NFULL:
2162                 if (!terse && !TestOnly && has_xu)
2163                 {       fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2164                         putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
2165                         putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
2166                         fprintf(fd, "\n#endif\n\t\t");
2167                 }
2168                 putname(fd, "(!q_full(", now->lft, m, "))");
2169                 break;
2170
2171         case NEMPTY:
2172                 if (!terse && !TestOnly && has_xu)
2173                 {       fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2174                         putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
2175                         putname(fd, "q_R_check(", now->lft, m, ", II)) &&");
2176                         fprintf(fd, "\n#endif\n\t\t");
2177                 }
2178                 putname(fd, "(q_len(", now->lft, m, ")>0)");
2179                 break;
2180
2181         case 's':
2182                 if (Pid == eventmapnr)
2183                 {       fprintf(fd, "if ((ot == EVENT_TRACE && _tp != 's') ");
2184                         putname(fd, "|| _qid+1 != ", now->lft, m, "");
2185                         for (v = now->rgt, i=0; v; v = v->rgt, i++)
2186                         {       if (v->lft->ntyp != CONST
2187                                 &&  v->lft->ntyp != EVAL)
2188                                         continue;
2189                                 fprintf(fd, " \\\n\t\t|| qrecv(");
2190                                 putname(fd, "", now->lft, m, ", ");
2191                                 putname(fd, "q_len(", now->lft, m, ")-1, ");
2192                                 fprintf(fd, "%d, 0) != ", i);
2193                                 if (v->lft->ntyp == CONST)
2194                                         putstmnt(fd, v->lft, m);
2195                                 else /* EVAL */
2196                                         putstmnt(fd, v->lft->lft, m);
2197                         }
2198                         fprintf(fd, ")\n");
2199                         fprintf(fd, "\t\t       continue");
2200                         putname(th, " || (x_y3_ == ", now->lft, m, ")");
2201                         break;
2202                 }
2203                 if (TestOnly)
2204                 {       if (m_loss)
2205                                 fprintf(fd, "1");
2206                         else
2207                                 putname(fd, "!q_full(", now->lft, m, ")");
2208                         break;
2209                 }
2210                 if (has_xu)
2211                 {       fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2212                         putname(fd, "if (q_claim[", now->lft, m, "]&2) ");
2213                         putname(fd, "q_S_check(", now->lft, m, ", II);");
2214                         fprintf(fd, "\n#endif\n\t\t");
2215                 }
2216                 fprintf(fd, "if (q_%s",
2217                         (u_sync > 0 && u_async == 0)?"len":"full");
2218                 putname(fd, "(", now->lft, m, "))\n");
2219
2220                 if (m_loss)
2221                         fprintf(fd, "\t\t{ nlost++; delta_m = 1; } else {");
2222                 else
2223                 {       fprintf(fd, "\t\t\t");
2224                         Bailout(fd, ";");
2225                 }
2226
2227                 if (has_enabled)
2228                         fprintf(fd, "\n\t\tif (TstOnly) return 1;");
2229
2230                 if (u_sync && !u_async && rvopt)
2231                         fprintf(fd, "\n\n\t\tif (no_recvs(II)) continue;\n");
2232
2233                 fprintf(fd, "\n#ifdef HAS_CODE\n");
2234                 fprintf(fd, "\t\tif (readtrail && gui) {\n");
2235                 fprintf(fd, "\t\t\tchar simtmp[32];\n");
2236                 putname(fd, "\t\t\tsprintf(simvals, \"%%d!\", ", now->lft, m, ");\n");
2237                 _isok++;
2238                 for (v = now->rgt, i = 0; v; v = v->rgt, i++)
2239                 {       cat3("\t\tsprintf(simtmp, \"%%d\", ", v->lft, "); strcat(simvals, simtmp);");
2240                         if (v->rgt)
2241                         fprintf(fd, "\t\tstrcat(simvals, \",\");\n");
2242                 }
2243                 _isok--;
2244                 fprintf(fd, "\t\t}\n");
2245                 fprintf(fd, "#endif\n\t\t");
2246
2247                 putname(fd, "\n\t\tqsend(", now->lft, m, "");
2248                 fprintf(fd, ", %d", now->val);
2249                 for (v = now->rgt, i = 0; v; v = v->rgt, i++)
2250                 {       cat2(", ", v->lft);
2251                 }
2252                 if (i > Mpars)
2253                 {       terse++;
2254                         putname(stdout, "channel name: ", now->lft, m, "\n");
2255                         terse--;
2256                         printf("        %d msg parameters sent, %d expected\n", i, Mpars);
2257                         fatal("too many pars in send", "");
2258                 }
2259                 for ( ; i < Mpars; i++)
2260                         fprintf(fd, ", 0");
2261                 fprintf(fd, ")");
2262                 if (u_sync)
2263                 {       fprintf(fd, ";\n\t\t");
2264                         if (u_async)
2265                           putname(fd, "if (q_zero(", now->lft, m, ")) ");
2266                         putname(fd, "{ boq = ", now->lft, m, "");
2267                         if (GenCode)
2268                           fprintf(fd, "; Uerror(\"rv-attempt in d_step\")");
2269                         fprintf(fd, "; }");
2270                 }
2271                 if (m_loss)
2272                         fprintf(fd, ";\n\t\t}\n\t\t"); /* end of m_loss else */
2273                 break;
2274
2275         case 'r':
2276                 if (Pid == eventmapnr)
2277                 {       fprintf(fd, "if ((ot == EVENT_TRACE && _tp != 'r') ");
2278                         putname(fd, "|| _qid+1 != ", now->lft, m, "");
2279                         for (v = now->rgt, i=0; v; v = v->rgt, i++)
2280                         {       if (v->lft->ntyp != CONST
2281                                 &&  v->lft->ntyp != EVAL)
2282                                         continue;
2283                                 fprintf(fd, " \\\n\t\t|| qrecv(");
2284                                 putname(fd, "", now->lft, m, ", ");
2285                                 fprintf(fd, "0, %d, 0) != ", i);
2286                                 if (v->lft->ntyp == CONST)
2287                                         putstmnt(fd, v->lft, m);
2288                                 else /* EVAL */
2289                                         putstmnt(fd, v->lft->lft, m);
2290                         }
2291                         fprintf(fd, ")\n");
2292                         fprintf(fd, "\t\t       continue");
2293
2294                         putname(tc, " || (x_y3_ == ", now->lft, m, ")");
2295
2296                         break;
2297                 }
2298                 if (TestOnly)
2299                 {       fprintf(fd, "((");
2300                         if (u_sync) fprintf(fd, "(boq == -1 && ");
2301
2302                         putname(fd, "q_len(", now->lft, m, ")");
2303
2304                         if (u_sync && now->val <= 1)
2305                         { putname(fd, ") || (boq == ",  now->lft,m," && ");
2306                           putname(fd, "q_zero(", now->lft,m,"))");
2307                         }
2308
2309                         fprintf(fd, ")");
2310                         if (now->val == 0 || now->val == 2)
2311                         {       for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
2312                                 { if (v->lft->ntyp == CONST)
2313                                   { cat3("\n\t\t&& (", v->lft, " == ");
2314                                     putname(fd, "qrecv(", now->lft, m, ", ");
2315                                     fprintf(fd, "0, %d, 0))", i);
2316                                   } else if (v->lft->ntyp == EVAL)
2317                                   { cat3("\n\t\t&& (", v->lft->lft, " == ");
2318                                     putname(fd, "qrecv(", now->lft, m, ", ");
2319                                     fprintf(fd, "0, %d, 0))", i);
2320                                   } else
2321                                   {     j++; continue;
2322                                   }
2323                                 }
2324                         } else
2325                         {       fprintf(fd, "\n\t\t&& Q_has(");
2326                                 putname(fd, "", now->lft, m, "");
2327                                 for (v = now->rgt, i=0; v; v = v->rgt, i++)
2328                                 {       if (v->lft->ntyp == CONST)
2329                                         {       fprintf(fd, ", 1, ");
2330                                                 putstmnt(fd, v->lft, m);
2331                                         } else if (v->lft->ntyp == EVAL)
2332                                         {       fprintf(fd, ", 1, ");
2333                                                 putstmnt(fd, v->lft->lft, m);
2334                                         } else
2335                                         {       fprintf(fd, ", 0, 0");
2336                                 }       }
2337                                 for ( ; i < Mpars; i++)
2338                                         fprintf(fd, ", 0, 0");
2339                                 fprintf(fd, ")");
2340                         }
2341                         fprintf(fd, ")");
2342                         break;
2343                 }
2344                 if (has_xu)
2345                 {       fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2346                         putname(fd, "if (q_claim[", now->lft, m, "]&1) ");
2347                         putname(fd, "q_R_check(", now->lft, m, ", II);");
2348                         fprintf(fd, "\n#endif\n\t\t");
2349                 }
2350                 if (u_sync)
2351                 {       if (now->val >= 2)
2352                         {       if (u_async)
2353                                 { fprintf(fd, "if (");
2354                                   putname(fd, "q_zero(", now->lft,m,"))");
2355                                   fprintf(fd, "\n\t\t{\t");
2356                                 }
2357                                 fprintf(fd, "uerror(\"polling ");
2358                                 fprintf(fd, "rv chan\");\n\t\t");
2359                                 if (u_async)
2360                                   fprintf(fd, " continue;\n\t\t}\n\t\t");
2361                                 fprintf(fd, "IfNotBlocked\n\t\t");
2362                         } else
2363                         {       fprintf(fd, "if (");
2364                                 if (u_async == 0)
2365                                   putname(fd, "boq != ", now->lft,m,") ");
2366                                 else
2367                                 { putname(fd, "q_zero(", now->lft,m,"))");
2368                                   fprintf(fd, "\n\t\t{\tif (boq != ");
2369                                   putname(fd, "",  now->lft,m,") ");
2370                                   Bailout(fd, ";\n\t\t} else\n\t\t");
2371                                   fprintf(fd, "{\tif (boq != -1) ");
2372                                 }
2373                                 Bailout(fd, ";\n\t\t");
2374                                 if (u_async)
2375                                         fprintf(fd, "}\n\t\t");
2376                 }       }
2377                 putname(fd, "if (q_len(", now->lft, m, ") == 0) ");
2378                 Bailout(fd, "");
2379
2380                 for (v = now->rgt, j=0; v; v = v->rgt)
2381                 {       if (v->lft->ntyp != CONST
2382                         &&  v->lft->ntyp != EVAL)
2383                                 j++;    /* count settables */
2384                 }
2385                 fprintf(fd, ";\n\n\t\tXX=1");
2386 /* test */      if (now->val == 0 || now->val == 2)
2387                 {       for (v = now->rgt, i=0; v; v = v->rgt, i++)
2388                         {       if (v->lft->ntyp == CONST)
2389                                 { fprintf(fd, ";\n\t\t");
2390                                   cat3("if (", v->lft, " != ");
2391                                   putname(fd, "qrecv(", now->lft, m, ", ");
2392                                   fprintf(fd, "0, %d, 0)) ", i);
2393                                   Bailout(fd, "");
2394                                 } else if (v->lft->ntyp == EVAL)
2395                                 { fprintf(fd, ";\n\t\t");
2396                                   cat3("if (", v->lft->lft, " != ");
2397                                   putname(fd, "qrecv(", now->lft, m, ", ");
2398                                   fprintf(fd, "0, %d, 0)) ", i);
2399                                   Bailout(fd, "");
2400                         }       }
2401                 } else  /* random receive: val 1 or 3 */
2402                 {       fprintf(fd, ";\n\t\tif (!(XX = Q_has(");
2403                         putname(fd, "", now->lft, m, "");
2404                         for (v = now->rgt, i=0; v; v = v->rgt, i++)
2405                         {       if (v->lft->ntyp == CONST)
2406                                 {       fprintf(fd, ", 1, ");
2407                                         putstmnt(fd, v->lft, m);
2408                                 } else if (v->lft->ntyp == EVAL)
2409                                 {       fprintf(fd, ", 1, ");
2410                                         putstmnt(fd, v->lft->lft, m);
2411                                 } else
2412                                 {       fprintf(fd, ", 0, 0");
2413                         }       }
2414                         for ( ; i < Mpars; i++)
2415                                 fprintf(fd, ", 0, 0");
2416                         fprintf(fd, "))) ");
2417                         Bailout(fd, "");
2418                         fprintf(fd, ";\n\t\t");
2419                         if (multi_oval)
2420                         {       check_needed();
2421                                 fprintf(fd, "(trpt+1)->bup.ovals[%d] = ",
2422                                         multi_oval-1);
2423                                 multi_oval++;
2424                         } else
2425                                 fprintf(fd, "(trpt+1)->bup.oval = ");
2426                         fprintf(fd, "XX");
2427                 }
2428
2429                 if (has_enabled)
2430                         fprintf(fd, ";\n\t\tif (TstOnly) return 1");
2431
2432                 if (j == 0 && now->val >= 2)
2433                 {       fprintf(fd, ";\n\t\t");
2434                         break;  /* poll without side-effect */
2435                 }
2436
2437                 if (!GenCode)
2438                 {       int jj = 0;
2439                         fprintf(fd, ";\n\t\t");
2440                         /* no variables modified */
2441                         if (j == 0 && now->val == 0)
2442                         {       fprintf(fd, "if (q_flds[((Q0 *)qptr(");
2443                                 putname(fd, "", now->lft, m, "-1))->_t]");
2444                                 fprintf(fd, " != %d)\n\t", i);
2445                                 fprintf(fd, "\t\tUerror(\"wrong nr of msg fields in rcv\");\n\t\t");
2446                         }
2447
2448                         for (v = now->rgt; v; v = v->rgt)
2449                                 if ((v->lft->ntyp != CONST
2450                                 &&   v->lft->ntyp != EVAL))
2451                                         jj++;   /* nr of vars needing bup */
2452
2453                         if (jj)
2454                         for (v = now->rgt, i = 0; v; v = v->rgt, i++)
2455                         {       char tempbuf[64];
2456
2457                                 if ((v->lft->ntyp == CONST
2458                                 ||   v->lft->ntyp == EVAL))
2459                                         continue;
2460
2461                                 if (multi_oval)
2462                                 {       check_needed();
2463                                         sprintf(tempbuf, "(trpt+1)->bup.ovals[%d] = ",
2464                                                 multi_oval-1);
2465                                         multi_oval++;
2466                                 } else
2467                                         sprintf(tempbuf, "(trpt+1)->bup.oval = ");
2468
2469                                 if (v->lft->sym && !strcmp(v->lft->sym->name, "_"))
2470                                 {       fprintf(fd, tempbuf);
2471                                         putname(fd, "qrecv(", now->lft, m, "");
2472                                         fprintf(fd, ", XX-1, %d, 0);\n\t\t", i);
2473                                 } else
2474                                 {       _isok++;
2475                                         cat3(tempbuf, v->lft, ";\n\t\t");
2476                                         _isok--;
2477                                 }
2478                         }
2479
2480                         if (jj) /* check for double entries q?x,x */
2481                         {       Lextok *w;
2482
2483                                 for (v = now->rgt; v; v = v->rgt)
2484                                 {       if (v->lft->ntyp != CONST
2485                                         &&  v->lft->ntyp != EVAL
2486                                         &&  v->lft->sym
2487                                         &&  v->lft->sym->type != STRUCT /* not a struct */
2488                                         &&  v->lft->sym->nel == 1       /* not an array */
2489                                         &&  strcmp(v->lft->sym->name, "_") != 0)
2490                                         for (w = v->rgt; w; w = w->rgt)
2491                                                 if (v->lft->sym == w->lft->sym)
2492                                                 {       fatal("cannot use var ('%s') in multiple msg fields",
2493                                                                 v->lft->sym->name);
2494                         }       }               }
2495                 }
2496 /* set */       for (v = now->rgt, i = 0; v; v = v->rgt, i++)
2497                 {       if ((v->lft->ntyp == CONST
2498                         ||   v->lft->ntyp == EVAL) && v->rgt)
2499                                 continue;
2500                         fprintf(fd, ";\n\t\t");
2501
2502                         if (v->lft->ntyp != CONST
2503                         &&  v->lft->ntyp != EVAL
2504                         &&  strcmp(v->lft->sym->name, "_") != 0)
2505                         {       nocast=1;
2506                                 _isok++;
2507                                 putstmnt(fd, v->lft, m);
2508                                 _isok--;
2509                                 nocast=0;
2510                                 fprintf(fd, " = ");
2511                         }
2512                         putname(fd, "qrecv(", now->lft, m, ", ");
2513                         fprintf(fd, "XX-1, %d, ", i);
2514                         fprintf(fd, "%d)", (v->rgt || now->val >= 2)?0:1);
2515
2516                         if (v->lft->ntyp != CONST
2517                         &&  v->lft->ntyp != EVAL
2518                         && strcmp(v->lft->sym->name, "_") != 0
2519                         &&  (v->lft->ntyp != NAME
2520                         ||   v->lft->sym->type != CHAN))
2521                         {       fprintf(fd, ";\n#ifdef VAR_RANGES");
2522                                 fprintf(fd, "\n\t\tlogval(\"");
2523                                 withprocname = terse = nocast = 1;
2524                                 _isok++;
2525                                 putstmnt(fd,v->lft,m);
2526                                 withprocname = terse = nocast = 0;
2527                                 fprintf(fd, "\", ");
2528                                 putstmnt(fd,v->lft,m);
2529                                 _isok--;
2530                                 fprintf(fd, ");\n#endif\n");
2531                                 fprintf(fd, "\t\t");
2532                         }
2533                 }
2534                 fprintf(fd, ";\n\t\t");
2535
2536                 fprintf(fd, "\n#ifdef HAS_CODE\n");
2537                 fprintf(fd, "\t\tif (readtrail && gui) {\n");
2538                 fprintf(fd, "\t\t\tchar simtmp[32];\n");
2539                 putname(fd, "\t\t\tsprintf(simvals, \"%%d?\", ", now->lft, m, ");\n");
2540                 _isok++;
2541                 for (v = now->rgt, i = 0; v; v = v->rgt, i++)
2542                 {       if (v->lft->ntyp != EVAL)
2543                         { cat3("\t\tsprintf(simtmp, \"%%d\", ", v->lft, "); strcat(simvals, simtmp);");
2544                         } else
2545                         { cat3("\t\tsprintf(simtmp, \"%%d\", ", v->lft->lft, "); strcat(simvals, simtmp);");
2546                         }
2547                         if (v->rgt)
2548                         fprintf(fd, "\t\tstrcat(simvals, \",\");\n");
2549                 }
2550                 _isok--;
2551                 fprintf(fd, "\t\t}\n");
2552                 fprintf(fd, "#endif\n\t\t");
2553
2554                 if (u_sync)
2555                 {       putname(fd, "if (q_zero(", now->lft, m, "))");
2556                         fprintf(fd, "\n\t\t{    boq = -1;\n");
2557
2558                         fprintf(fd, "#ifndef NOFAIR\n"); /* NEW 3.0.8 */
2559                         fprintf(fd, "\t\t\tif (fairness\n");
2560                         fprintf(fd, "\t\t\t&& !(trpt->o_pm&32)\n");
2561                         fprintf(fd, "\t\t\t&& (now._a_t&2)\n");
2562                         fprintf(fd, "\t\t\t&&  now._cnt[now._a_t&1] == II+2)\n");
2563                         fprintf(fd, "\t\t\t{    now._cnt[now._a_t&1] -= 1;\n");
2564                         fprintf(fd, "#ifdef VERI\n");
2565                         fprintf(fd, "\t\t\t     if (II == 1)\n");
2566                         fprintf(fd, "\t\t\t             now._cnt[now._a_t&1] = 1;\n");
2567                         fprintf(fd, "#endif\n");
2568                         fprintf(fd, "#ifdef DEBUG\n");
2569                         fprintf(fd, "\t\t\tprintf(\"%%3d: proc %%d fairness \", depth, II);\n");
2570                         fprintf(fd, "\t\t\tprintf(\"Rule 2: --cnt to %%d (%%d)\\n\",\n");
2571                         fprintf(fd, "\t\t\t     now._cnt[now._a_t&1], now._a_t);\n");
2572                         fprintf(fd, "#endif\n");
2573                         fprintf(fd, "\t\t\t     trpt->o_pm |= (32|64);\n");
2574                         fprintf(fd, "\t\t\t}\n");
2575                         fprintf(fd, "#endif\n");
2576
2577                         fprintf(fd, "\n\t\t}");
2578                 }
2579                 break;
2580
2581         case 'R':
2582                 if (!terse && !TestOnly && has_xu)
2583                 {       fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2584                         putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
2585                         fprintf(fd, "q_R_check(");
2586                         putname(fd, "", now->lft, m, ", II)) &&\n\t\t");
2587                         putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
2588                         putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
2589                         fprintf(fd, "\n#endif\n\t\t");
2590                 }
2591                 if (u_sync>0)
2592                         putname(fd, "not_RV(", now->lft, m, ") && \\\n\t\t");
2593
2594                 for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
2595                         if (v->lft->ntyp != CONST
2596                         &&  v->lft->ntyp != EVAL)
2597                         {       j++; continue;
2598                         }
2599                 if (now->val == 0 || i == j)
2600                 {       putname(fd, "(q_len(", now->lft, m, ") > 0");
2601                         for (v = now->rgt, i=0; v; v = v->rgt, i++)
2602                         {       if (v->lft->ntyp != CONST
2603                                 &&  v->lft->ntyp != EVAL)
2604                                         continue;
2605                                 fprintf(fd, " \\\n\t\t&& qrecv(");
2606                                 putname(fd, "", now->lft, m, ", ");
2607                                 fprintf(fd, "0, %d, 0) == ", i);
2608                                 if (v->lft->ntyp == CONST)
2609                                         putstmnt(fd, v->lft, m);
2610                                 else /* EVAL */
2611                                         putstmnt(fd, v->lft->lft, m);
2612                         }
2613                         fprintf(fd, ")");
2614                 } else
2615                 {       putname(fd, "Q_has(", now->lft, m, "");
2616                         for (v = now->rgt, i=0; v; v = v->rgt, i++)
2617                         {       if (v->lft->ntyp == CONST)
2618                                 {       fprintf(fd, ", 1, ");
2619                                         putstmnt(fd, v->lft, m);
2620                                 } else if (v->lft->ntyp == EVAL)
2621                                 {       fprintf(fd, ", 1, ");
2622                                         putstmnt(fd, v->lft->lft, m);
2623                                 } else
2624                                         fprintf(fd, ", 0, 0");
2625                         }
2626                         for ( ; i < Mpars; i++)
2627                                 fprintf(fd, ", 0, 0");
2628                         fprintf(fd, ")");
2629                 }
2630                 break;
2631
2632         case 'c':
2633                 preruse(fd, now->lft);  /* preconditions */
2634                 cat3("if (!(", now->lft, "))\n\t\t\t");
2635                 Bailout(fd, "");
2636                 break;
2637
2638         case  ELSE:
2639                 if (!GenCode)
2640                 {       if (separate == 2)
2641                                 fprintf(fd, "if (o_pm&1)\n\t\t\t");
2642                         else
2643                                 fprintf(fd, "if (trpt->o_pm&1)\n\t\t\t");
2644                         Bailout(fd, "");
2645                 } else
2646                 {       fprintf(fd, "/* else */");
2647                 }
2648                 break;
2649
2650         case '?':
2651                 if (now->lft)
2652                 {       cat3("( (", now->lft, ") ? ");
2653                 }
2654                 if (now->rgt)
2655                 {       cat3("(", now->rgt->lft, ") : ");
2656                         cat3("(", now->rgt->rgt, ") )");
2657                 }
2658                 break;
2659
2660         case ASGN:
2661                 if (has_enabled)
2662                 fprintf(fd, "if (TstOnly) return 1;\n\t\t");
2663                 _isok++;
2664
2665                 if (!GenCode)
2666                 {       if (multi_oval)
2667                         {       char tempbuf[64];
2668                                 check_needed();
2669                                 sprintf(tempbuf, "(trpt+1)->bup.ovals[%d] = ",
2670                                         multi_oval-1);
2671                                 multi_oval++;
2672                                 cat3(tempbuf, now->lft, ";\n\t\t");
2673                         } else
2674                         {       cat3("(trpt+1)->bup.oval = ", now->lft, ";\n\t\t");
2675                 }       }
2676                 nocast = 1; putstmnt(fd,now->lft,m); nocast = 0;
2677                 fprintf(fd," = ");
2678                 _isok--;
2679                 putstmnt(fd,now->rgt,m);
2680
2681                 if (now->sym->type != CHAN
2682                 ||  verbose > 0)
2683                 {       fprintf(fd, ";\n#ifdef VAR_RANGES");
2684                         fprintf(fd, "\n\t\tlogval(\"");
2685                         withprocname = terse = nocast = 1;
2686                         _isok++;
2687                         putstmnt(fd,now->lft,m);
2688                         withprocname = terse = nocast = 0;
2689                         fprintf(fd, "\", ");
2690                         putstmnt(fd,now->lft,m);
2691                         _isok--;
2692                         fprintf(fd, ");\n#endif\n");
2693                         fprintf(fd, "\t\t");
2694                 }
2695                 break;
2696
2697         case PRINT:
2698                 if (has_enabled)
2699                 fprintf(fd, "if (TstOnly) return 1;\n\t\t");
2700 #ifdef PRINTF
2701                 fprintf(fd, "printf(%s", now->sym->name);
2702 #else
2703                 fprintf(fd, "Printf(%s", now->sym->name);
2704 #endif
2705                 for (v = now->lft; v; v = v->rgt)
2706                 {       cat2(", ", v->lft);
2707                 }
2708                 fprintf(fd, ")");
2709                 break;
2710
2711         case PRINTM:
2712                 if (has_enabled)
2713                 fprintf(fd, "if (TstOnly) return 1;\n\t\t");
2714                 fprintf(fd, "printm(");
2715                 if (now->lft && now->lft->ismtyp)
2716                         fprintf(fd, "%d", now->lft->val);
2717                 else
2718                         putstmnt(fd, now->lft, m);
2719                 fprintf(fd, ")");
2720                 break;
2721
2722         case NAME:
2723                 if (!nocast && now->sym && Sym_typ(now) < SHORT)
2724                         putname(fd, "((int)", now, m, ")");
2725                 else
2726                         putname(fd, "", now, m, "");
2727                 break;
2728
2729         case   'p':
2730                 putremote(fd, now, m);
2731                 break;
2732
2733         case   'q':
2734                 if (terse)
2735                         fprintf(fd, "%s", now->sym->name);
2736                 else
2737                         fprintf(fd, "%d", remotelab(now));
2738                 break;
2739
2740         case C_EXPR:
2741                 fprintf(fd, "(");
2742                 plunk_expr(fd, now->sym->name);
2743 #if 1
2744                 fprintf(fd, ")");
2745 #else
2746                 fprintf(fd, ") /* %s */ ", now->sym->name);
2747 #endif
2748                 break;
2749
2750         case C_CODE:
2751                 fprintf(fd, "/* %s */\n\t\t", now->sym->name);
2752                 if (has_enabled)
2753                         fprintf(fd, "if (TstOnly) return 1;\n\t\t");
2754                 if (!GenCode)   /* not in d_step */
2755                 {       fprintf(fd, "sv_save();\n\t\t");
2756                         /* store the old values for reverse moves */
2757                 }
2758                 plunk_inline(fd, now->sym->name, 1);
2759                 if (!GenCode)
2760                 {       fprintf(fd, "\n");      /* state changed, capture it */
2761                         fprintf(fd, "#if defined(C_States) && (HAS_TRACK==1)\n");
2762                         fprintf(fd, "\t\tc_update((uchar *) &(now.c_state[0]));\n");
2763                         fprintf(fd, "#endif\n");
2764                 }
2765                 break;
2766
2767         case ASSERT:
2768                 if (has_enabled)
2769                         fprintf(fd, "if (TstOnly) return 1;\n\t\t");
2770
2771                 cat3("assert(", now->lft, ", ");
2772                 terse = nocast = 1;
2773                 cat3("\"", now->lft, "\", II, tt, t)");
2774                 terse = nocast = 0;
2775                 break;
2776
2777         case '.':
2778         case BREAK:
2779         case GOTO:
2780                 if (Pid == eventmapnr)
2781                         fprintf(fd, "Uerror(\"cannot get here\")");
2782                 putskip(m);
2783                 break;
2784
2785         case '@':
2786                 if (Pid == eventmapnr)
2787                 {       fprintf(fd, "return 0");
2788                         break;
2789                 }
2790
2791                 if (has_enabled)
2792                 {       fprintf(fd, "if (TstOnly)\n\t\t\t");
2793                         fprintf(fd, "return (II+1 == now._nr_pr);\n\t\t");
2794                 }
2795                 fprintf(fd, "if (!delproc(1, II)) ");
2796                 Bailout(fd, "");
2797                 break;
2798
2799         default:
2800                 printf("spin: bad node type %d (.m) - line %d\n",
2801                         now->ntyp, now->ln);
2802                 fflush(tm);
2803                 alldone(1);
2804         }
2805 }
2806
2807 void
2808 putname(FILE *fd, char *pre, Lextok *n, int m, char *suff) /* varref */
2809 {       Symbol *s = n->sym;
2810         lineno = n->ln; Fname = n->fn;
2811
2812         if (!s)
2813                 fatal("no name - putname", (char *) 0);
2814
2815         if (s->context && context && s->type)
2816                 s = findloc(s);         /* it's a local var */
2817
2818         if (!s)
2819         {       fprintf(fd, "%s%s%s", pre, n->sym->name, suff);
2820                 return;
2821         }
2822         if (!s->type)   /* not a local name */
2823                 s = lookup(s->name);    /* must be a global */
2824
2825         if (!s->type)
2826         {       if (strcmp(pre, ".") != 0)
2827                 non_fatal("undeclared variable '%s'", s->name);
2828                 s->type = INT;
2829         }
2830
2831         if (s->type == PROCTYPE)
2832                 fatal("proctype-name '%s' used as array-name", s->name);
2833
2834         fprintf(fd, pre);
2835         if (!terse && !s->owner && evalindex != 1)
2836         {       if (s->context
2837                 ||  strcmp(s->name, "_p") == 0
2838                 ||  strcmp(s->name, "_pid") == 0)
2839                 {       fprintf(fd, "((P%d *)this)->", Pid);
2840                 } else
2841                 {       int x = strcmp(s->name, "_");
2842                         if (!(s->hidden&1) && x != 0)
2843                                 fprintf(fd, "now.");
2844                         if (x == 0 && _isok == 0)
2845                                 fatal("attempt to read value of '_'", 0);
2846         }       }
2847
2848         if (withprocname
2849         &&  s->context
2850         &&  strcmp(pre, "."))
2851                 fprintf(fd, "%s:", s->context->name);
2852
2853         if (evalindex != 1)
2854                 fprintf(fd, "%s", s->name);
2855
2856         if (s->nel != 1)
2857         {       if (no_arrays)
2858                 {
2859                 non_fatal("ref to array element invalid in this context",
2860                         (char *)0);
2861                 printf("\thint: instead of, e.g., x[rs] qu[3], use\n");
2862                 printf("\tchan nm_3 = qu[3]; x[rs] nm_3;\n");
2863                 printf("\tand use nm_3 in sends/recvs instead of qu[3]\n");
2864                 }
2865                 /* an xr or xs reference to an array element
2866                  * becomes an exclusion tag on the array itself -
2867                  * which could result in invalidly labeling
2868                  * operations on other elements of this array to
2869                  * be also safe under the partial order reduction
2870                  * (see procedure has_global())
2871                  */
2872
2873                 if (evalindex == 2)
2874                 {       fprintf(fd, "[%%d]");
2875                 } else if (evalindex == 1)
2876                 {       evalindex = 0;          /* no good if index is indexed array */
2877                         fprintf(fd, ", ");
2878                         putstmnt(fd, n->lft, m);
2879                         evalindex = 1;
2880                 } else
2881                 {       if (terse
2882                         || (n->lft
2883                         &&  n->lft->ntyp == CONST
2884                         &&  n->lft->val < s->nel)
2885                         || (!n->lft && s->nel > 0))
2886                         {       cat3("[", n->lft, "]");
2887                         } else
2888                         {       cat3("[ Index(", n->lft, ", ");
2889                                 fprintf(fd, "%d) ]", s->nel);
2890                         }
2891                 }
2892         }
2893         if (s->type == STRUCT && n->rgt && n->rgt->lft)
2894         {       putname(fd, ".", n->rgt->lft, m, "");
2895         }
2896         fprintf(fd, suff);
2897 }
2898
2899 void
2900 putremote(FILE *fd, Lextok *n, int m)   /* remote reference */
2901 {       int promoted = 0;
2902         int pt;
2903
2904         if (terse)
2905         {       fprintf(fd, "%s", n->lft->sym->name);   /* proctype name */
2906                 if (n->lft->lft)
2907                 {       fprintf(fd, "[");
2908                         putstmnt(fd, n->lft->lft, m);   /* pid */
2909                         fprintf(fd, "]");
2910                 }
2911                 fprintf(fd, ".%s", n->sym->name);
2912         } else
2913         {       if (Sym_typ(n) < SHORT)
2914                 {       promoted = 1;
2915                         fprintf(fd, "((int)");
2916                 }
2917
2918                 pt = fproc(n->lft->sym->name);
2919                 fprintf(fd, "((P%d *)Pptr(", pt);
2920                 if (n->lft->lft)
2921                 {       fprintf(fd, "BASE+");
2922                         putstmnt(fd, n->lft->lft, m);
2923                 } else
2924                         fprintf(fd, "f_pid(%d)", pt);
2925                 fprintf(fd, "))->%s", n->sym->name);
2926         }
2927         if (n->rgt)
2928         {       fprintf(fd, "[");
2929                 putstmnt(fd, n->rgt, m);        /* array var ref */
2930                 fprintf(fd, "]");
2931         }
2932         if (promoted) fprintf(fd, ")");
2933 }
2934
2935 static int
2936 getweight(Lextok *n)
2937 {       /* this piece of code is a remnant of early versions
2938          * of the verifier -- in the current version of Spin
2939          * only non-zero values matter - so this could probably
2940          * simply return 1 in all cases.
2941          */
2942         switch (n->ntyp) {
2943         case 'r':     return 4;
2944         case 's':     return 2;
2945         case TIMEOUT: return 1;
2946         case 'c':     if (has_typ(n->lft, TIMEOUT)) return 1;
2947         }
2948         return 3;
2949 }
2950
2951 int
2952 has_typ(Lextok *n, int m)
2953 {
2954         if (!n) return 0;
2955         if (n->ntyp == m) return 1;
2956         return (has_typ(n->lft, m) || has_typ(n->rgt, m));
2957 }
2958
2959 static int runcount, opcount;
2960
2961 static void
2962 do_count(Lextok *n, int checkop)
2963 {
2964         if (!n) return;
2965
2966         switch (n->ntyp) {
2967         case RUN:
2968                 runcount++;
2969                 break;
2970         default:
2971                 if (checkop) opcount++;
2972                 break;
2973         }
2974         do_count(n->lft, checkop && (n->ntyp != RUN));
2975         do_count(n->rgt, checkop);
2976 }
2977
2978 void
2979 count_runs(Lextok *n)
2980 {
2981         runcount = opcount = 0;
2982         do_count(n, 1);
2983         if (runcount > 1)
2984                 fatal("more than one run operator in expression", "");
2985         if (runcount == 1 && opcount > 1)
2986                 fatal("use of run operator in compound expression", "");
2987 }
2988
2989 void
2990 any_runs(Lextok *n)
2991 {
2992         runcount = opcount = 0;
2993         do_count(n, 0);
2994         if (runcount >= 1)
2995                 fatal("run operator used in invalid context", "");
2996 }