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