spin: Update to most recent version. (thanks Ori_B)

from Ori_B:

There were a small number of changes needed from the tarball
on spinroot.org:

  - The mkfile needed to be updated
  - Memory.h needed to not be included
  - It needed to invoke /bin/cpp instead of gcc -E
  - It depended on `yychar`, which our yacc doesn't
    provide.

I'm still figuring out how to use spin, but it seems to do
the right thing when testing a few of the examples:

	% cd $home/src/Spin/Examples/
	% spin -a peterson.pml
	% pcc pan.c -D_POSIX_SOURCE
	% ./6.out

	(Spin Version 6.4.7 -- 19 August 2017)
		+ Partial Order Reduction

	Full statespace search for:
		never claim         	- (none specified)
		assertion violations	+
		acceptance   cycles 	- (not selected)
		invalid end states	+

	State-vector 32 byte, depth reached 24, errors: 0
	40 states, stored
	27 states, matched
	67 transitions (= stored+matched)
		0 atomic steps
	hash conflicts:         0 (resolved)

	Stats on memory usage (in Megabytes):
	0.002	equivalent memory usage for states (stored*(State-vector + overhead))
	0.292	actual memory usage for states
	128.000	memory used for hash table (-w24)
	0.534	memory used for DFS stack (-m10000)
	128.730	total actual memory usage


	unreached in proctype user
		/tmp/Spin/Examples/peterson.pml:20, state 10, "-end-"
		(1 of 10 states)

	pan: elapsed time 1.25 seconds
	pan: rate        32 states/second

1 files changed, 752 insertions, 320 deletions

diff --git a/sys/src/cmd/spin/pangen2.c b/sys/src/cmd/spin/pangen2.c
index 05ad9fa1f..828ded881 100644
--- a/sys/src/cmd/spin/pangen2.c
+++ b/sys/src/cmd/spin/pangen2.c
@@ -1,13 +1,10 @@
 /***** spin: pangen2.c *****/
 
-/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
-/* All Rights Reserved.  This software is for educational purposes only.  */
-/* No guarantee whatsoever is expressed or implied by the distribution of */
-/* this code.  Permission is given to distribute this code provided that  */
-/* this introductory message is not removed and no monies are exchanged.  */
-/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
-/*             http://spinroot.com/                                       */
-/* Send all bug-reports and/or questions to: bugs@spinroot.com            */
+/*
+ * This file is part of the public release of Spin. It is subject to the
+ * terms in the LICENSE file that is included in this source directory.
+ * Tool documentation is available at http://spinroot.com
+ */
 
 #include "spin.h"
 #include "version.h"
@@ -15,33 +12,40 @@
 #include "pangen2.h"
 #include "pangen4.h"
 #include "pangen5.h"
+#include "pangen7.h"
 
 #define DELTA	500	/* sets an upperbound on nr of chan names */
 
 #define blurb(fd, e)	{ fprintf(fd, "\n"); if (!merger) fprintf(fd, "\t\t/* %s:%d */\n", \
 				e->n->fn->name, e->n->ln); }
-#define tr_map(m, e)	{ if (!merger) fprintf(tt, "\t\ttr_2_src(%d, %s, %d);\n", \
+#define tr_map(m, e)	{ if (!merger) fprintf(tt, "\t\ttr_2_src(%d, \"%s\", %d);\n", \
 				m, e->n->fn->name, e->n->ln); }
 
 extern ProcList	*rdy;
 extern RunList	*run;
+extern Lextok	*runstmnts;
 extern Symbol	*Fname, *oFname, *context;
 extern char	*claimproc, *eventmap;
-extern int	lineno, verbose, Npars, Mpars;
+extern int	lineno, verbose, Npars, Mpars, nclaims;
 extern int	m_loss, has_remote, has_remvar, merger, rvopt, separate;
-extern int	Ntimeouts, Etimeouts, deadvar;
-extern int	u_sync, u_async, nrRdy;
+extern int	Ntimeouts, Etimeouts, deadvar, old_scope_rules, old_priority_rules;
+extern int	u_sync, u_async, nrRdy, Unique;
 extern int	GenCode, IsGuard, Level, TestOnly;
+extern int	globmin, globmax, ltl_mode, dont_simplify;
+
 extern short	has_stack;
-extern char	*NextLab[];
+extern char	*NextLab[64];	/* must match value in dstep.c:18 */
 
-FILE	*tc, *th, *tt, *tm, *tb;
+int	 	 buzzed;
+FILE		*tc, *th, *tt, *tb;
+static FILE	*tm;
 
-int	OkBreak = -1;
+int	OkBreak = -1, has_hidden = 0; /* has_hidden set in sym.c and structs.c */
 short	nocast=0;	/* to turn off casts in lvalues */
 short	terse=0;	/* terse printing of varnames */
 short	no_arrays=0;
 short	has_last=0;	/* spec refers to _last */
+short	has_priority=0;	/* spec refers to _priority */
 short	has_badelse=0;	/* spec contains else combined with chan refs */
 short	has_enabled=0;	/* spec contains enabled() */
 short	has_pcvalue=0;	/* spec contains pc_value() */
@@ -52,9 +56,7 @@ short	has_xu=0;	/* spec contains xr or xs assertions */
 short	has_unless=0;	/* spec contains unless statements */
 short	has_provided=0;	/* spec contains PROVIDED clauses on procs */
 short	has_code=0;	/* spec contains c_code, c_expr, c_state */
-short	_isok=0;	/* checks usage of predefined variable _ */
-short	evalindex=0;	/* evaluate index of var names */
-short	withprocname=0;	/* prefix local varnames with procname */
+short	has_ltl=0;	/* has inline ltl formulae */
 int	mst=0;		/* max nr of state/process */
 int	claimnr = -1;	/* claim process, if any */
 int	eventmapnr = -1; /* event trace, if any */
@@ -74,6 +76,9 @@ static int	TPE[2], EPT[2];
 static int	uniq=1;
 static int	multi_needed, multi_undo;
 static short	AllGlobal=0;	/* set if process has provided clause */
+static short	withprocname=0;	/* prefix local varnames with procname */
+static short	_isok=0;	/* checks usage of predefined variable _ */
+static short	evalindex=0;	/* evaluate index of var names */
 
 int	has_global(Lextok *);
 static int	getweight(Lextok *);
@@ -86,6 +91,29 @@ static void	putproc(ProcList *);
 static void	Tpe(Lextok *);
 extern void	spit_recvs(FILE *, FILE*);
 
+static L_List *keep_track;
+
+void
+keep_track_off(Lextok *n)
+{	L_List *p;
+
+	p = (L_List *) emalloc(sizeof(L_List));
+	p->n = n;
+	p->nxt = keep_track;
+	keep_track = p;
+}
+
+int
+check_track(Lextok *n)
+{	L_List *p;
+
+	for (p = keep_track; p; p = p->nxt)
+	{	if (p->n == n)
+		{	return n->sym?n->sym->type:0;
+	}	}
+	return 0;
+}
+
 static int
 fproc(char *s)
 {	ProcList *p;
@@ -98,12 +126,33 @@ fproc(char *s)
 	return -1;
 }
 
+int
+pid_is_claim(int p)	/* Pid (p->tn) to type (p->b) */
+{	ProcList *r;
+
+	for (r = rdy; r; r = r->nxt)
+	{	if (r->tn == p) return (r->b == N_CLAIM);
+	}
+	printf("spin: error, cannot find pid %d\n", p);
+	return 0;
+}
+
 static void
 reverse_procs(RunList *q)
 {
 	if (!q) return;
 	reverse_procs(q->nxt);
-	fprintf(tc, "	Addproc(%d);\n", q->tn);
+	fprintf(tc, "		Addproc(%d, %d);\n",
+		q->tn, q->priority < 1 ? 1 : q->priority);
+}
+
+static void
+forward_procs(RunList *q)
+{
+	if (!q) return;
+	fprintf(tc, "		Addproc(%d, %d);\n",
+		q->tn, q->priority < 1 ? 1 : q->priority);
+	forward_procs(q->nxt);
 }
 
 static void
@@ -111,13 +160,14 @@ tm_predef_np(void)
 {
 	fprintf(th, "#define _T5	%d\n", uniq++);
 	fprintf(th, "#define _T2	%d\n", uniq++);
+
 	fprintf(tm, "\tcase  _T5:\t/* np_ */\n");
 
 	if (separate == 2)
-	fprintf(tm, "\t\tif (!((!(o_pm&4) && !(tau&128))))\n");
-	else
-	fprintf(tm, "\t\tif (!((!(trpt->o_pm&4) && !(trpt->tau&128))))\n");
-
+	{	fprintf(tm, "\t\tif (!((!(o_pm&4) && !(tau&128))))\n");
+	} else
+	{	fprintf(tm, "\t\tif (!((!(trpt->o_pm&4) && !(trpt->tau&128))))\n");
+	}
 	fprintf(tm, "\t\t\tcontinue;\n");
 	fprintf(tm, "\t\t/* else fall through */\n");
 	fprintf(tm, "\tcase  _T2:\t/* true */\n");
@@ -151,51 +201,120 @@ static struct {
 void
 gensrc(void)
 {	ProcList *p;
+	int i;
+
+	disambiguate();		/* avoid name-clashes between scopes */
 
-	if (!(tc = fopen(Cfile[0].nm[separate], "w"))		/* main routines */
-	||  !(th = fopen(Cfile[1].nm[separate], "w"))		/* header file   */
-	||  !(tt = fopen(Cfile[2].nm[separate], "w"))		/* transition matrix */
-	||  !(tm = fopen(Cfile[3].nm[separate], "w"))		/* forward  moves */
-	||  !(tb = fopen(Cfile[4].nm[separate], "w")))	/* backward moves */
+	if (!(tc = fopen(Cfile[0].nm[separate], MFLAGS))		/* main routines */
+	||  !(th = fopen(Cfile[1].nm[separate], MFLAGS))		/* header file   */
+	||  !(tt = fopen(Cfile[2].nm[separate], MFLAGS))		/* transition matrix */
+	||  !(tm = fopen(Cfile[3].nm[separate], MFLAGS))		/* forward  moves */
+	||  !(tb = fopen(Cfile[4].nm[separate], MFLAGS)))	/* backward moves */
 	{	printf("spin: cannot create pan.[chtmfb]\n");
 		alldone(1);
 	}
 
-	fprintf(th, "#define Version	\"%s\"\n", Version);
-	fprintf(th, "#define Source	\"%s\"\n\n", oFname->name);
-	if (separate != 2)
-	fprintf(th, "char *TrailFile = Source; /* default */\n");
+	fprintf(th, "#ifndef PAN_H\n");
+	fprintf(th, "#define PAN_H\n\n");
+
+	fprintf(th, "#define SpinVersion	\"%s\"\n", SpinVersion);
+	fprintf(th, "#define PanSource	\"");
+	for (i = 0; oFname->name[i] != '\0'; i++)
+	{	char c = oFname->name[i];
+		if (c == '\\' || c == ' ') /* Windows path */
+		{	fprintf(th, "\\");
+		}
+		fprintf(th, "%c", c);
+	}
+	fprintf(th, "\"\n\n");
+
+	fprintf(th, "#define G_long	%d\n", (int) sizeof(long));
+	fprintf(th, "#define G_int	%d\n\n", (int) sizeof(int));
+	fprintf(th, "#define ulong	unsigned long\n");
+	fprintf(th, "#define ushort	unsigned short\n");
+
+	fprintf(th, "#ifdef WIN64\n");
+	fprintf(th, "	#define ONE_L	(1L)\n");
+	fprintf(th, "/*	#define long	long long */\n");
+	fprintf(th, "#else\n");
+	fprintf(th, "	#define ONE_L	(1L)\n");
+	fprintf(th, "#endif\n\n");
+
+	fprintf(th, "#ifdef BFS_PAR\n");
+	fprintf(th, "	#define NRUNS	%d\n", (runstmnts)?1:0);
+	fprintf(th, "	#ifndef BFS\n");
+	fprintf(th, "		#define BFS\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "	#ifndef PUTPID\n");
+	fprintf(th, "		#define PUTPID\n");
+	fprintf(th, "	#endif\n\n");
+	fprintf(th, "	#if !defined(USE_TDH) && !defined(NO_TDH)\n");
+	fprintf(th, "		#define USE_TDH\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "	#if defined(USE_TDH) && !defined(NO_HC)\n");
+	fprintf(th, "		#define HC /* default for USE_TDH */\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "	#ifndef BFS_MAXPROCS\n");
+	fprintf(th, "		#define BFS_MAXPROCS	64	/* max nr of cores to use */\n");
+	fprintf(th, "	#endif\n");
+
+	fprintf(th, "	#define BFS_GLOB	0	/* global lock */\n");
+	fprintf(th, "	#define BFS_ORD		1	/* used with -DCOLLAPSE */\n");
+	fprintf(th, "	#define BFS_MEM		2	/* malloc from shared heap */\n");
+	fprintf(th, "	#define BFS_PRINT	3	/* protect printfs */\n");
+	fprintf(th, "	#define BFS_STATE	4	/* hashtable */\n\n");
+	fprintf(th, "	#define BFS_INQ 	2	/* state is in q */\n\n");
+
+	fprintf(th, "	#ifdef BFS_FIFO\n");	/* queue access */
+	fprintf(th, "	  #define BFS_ID(a,b)	(BFS_STATE + (int) ((a)*BFS_MAXPROCS+(b)))\n");
+	fprintf(th, "	  #define BFS_MAXLOCKS	(BFS_STATE + (BFS_MAXPROCS*BFS_MAXPROCS))\n");
+	fprintf(th, "	#else\n");		/* h_store access (not needed for o_store) */
+	fprintf(th, "	  #ifndef BFS_W\n");
+	fprintf(th, "		#define BFS_W	10\n");	/* 1<<BFS_W locks */
+	fprintf(th, "	  #endif\n");
+	fprintf(th, "	  #define BFS_MASK	((1<<BFS_W) - 1)\n");
+	fprintf(th, "	  #define BFS_ID	(BFS_STATE + (int) (j1_spin & (BFS_MASK)))\n");
+	fprintf(th, "	  #define BFS_MAXLOCKS	(BFS_STATE + (1<<BFS_W))\n"); /* 4+1024 */
+	fprintf(th, "	#endif\n");
+
+	fprintf(th, "	#undef NCORE\n");
+	fprintf(th, "	extern int Cores, who_am_i;\n");
+	fprintf(th, "	#ifndef SAFETY\n");
+	fprintf(th, "	  #if !defined(BFS_STAGGER) && !defined(BFS_DISK)\n");
+	fprintf(th, "		#define BFS_STAGGER	64 /* randomizer, was 16 */\n");
+	fprintf(th, "	  #endif\n");
+	fprintf(th, "	  #ifndef L_BOUND\n");
+	fprintf(th, "		#define L_BOUND 	10 /* default */\n");
+	fprintf(th, "	  #endif\n");
+	fprintf(th, "	  extern int L_bound;\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "	#if defined(BFS_DISK) && defined(BFS_STAGGER)\n");
+	fprintf(th, "		#error BFS_DISK and BFS_STAGGER are not compatible\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "#endif\n\n");
 
 	fprintf(th, "#if defined(BFS)\n");
-	fprintf(th, "#ifndef SAFETY\n");
-	fprintf(th, "#define SAFETY\n");
-	fprintf(th, "#endif\n");
-	fprintf(th, "#ifndef XUSAFE\n");
-	fprintf(th, "#define XUSAFE\n");
-	fprintf(th, "#endif\n");
+	fprintf(th, "	#ifndef SAFETY\n");
+	fprintf(th, "		#define SAFETY\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "	#ifndef XUSAFE\n");
+	fprintf(th, "		#define XUSAFE\n");
+	fprintf(th, "	#endif\n");
 	fprintf(th, "#endif\n");
 
 	fprintf(th, "#ifndef uchar\n");
-	fprintf(th, "#define uchar	unsigned char\n");
+	fprintf(th, "	#define uchar	unsigned char\n");
 	fprintf(th, "#endif\n");
 	fprintf(th, "#ifndef uint\n");
-	fprintf(th, "#define uint	unsigned int\n");
+	fprintf(th, "	#define uint	unsigned int\n");
 	fprintf(th, "#endif\n");
 
-	if (sizeof(void *) > 4)	/* 64 bit machine */
-	{	fprintf(th, "#ifndef HASH32\n");
-		fprintf(th, "#define HASH64\n");
-		fprintf(th, "#endif\n");
-	}
-#if 0
-	if (sizeof(long)==sizeof(int))
-		fprintf(th, "#define long	int\n");
-#endif
 	if (separate == 1 && !claimproc)
 	{	Symbol *n = (Symbol *) emalloc(sizeof(Symbol));
 		Sequence *s = (Sequence *) emalloc(sizeof(Sequence));
+		s->minel = -1;
 		claimproc = n->name = "_:never_template:_";
-		ready(n, ZN, s, 0, ZN);
+		ready(n, ZN, s, 0, ZN, N_CLAIM);
 	}
 	if (separate == 2)
 	{	if (has_remote)
@@ -207,20 +326,29 @@ gensrc(void)
 		fprintf(th, "#endif\n");
 		if (has_last)
 		fprintf(th, "#define HAS_LAST	%d\n", has_last);
+		if (has_priority && !old_priority_rules)
+		fprintf(th, "#define HAS_PRIORITY	%d\n", has_priority);
 		goto doless;
 	}
 
 	fprintf(th, "#define DELTA	%d\n", DELTA);
 	fprintf(th, "#ifdef MA\n");
-	fprintf(th, "#if MA==1\n"); /* user typed -DMA without size */
-	fprintf(th, "#undef MA\n#define MA	100\n");
-	fprintf(th, "#endif\n#endif\n");
+	fprintf(th, "	#if NCORE>1 && !defined(SEP_STATE)\n");
+	fprintf(th, "		#define SEP_STATE\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "	#if MA==1\n"); /* user typed -DMA without size */
+	fprintf(th, "		#undef MA\n");
+	fprintf(th, "		#define MA	100\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "#endif\n");
 	fprintf(th, "#ifdef W_XPT\n");
-	fprintf(th, "#if W_XPT==1\n"); /* user typed -DW_XPT without size */
-	fprintf(th, "#undef W_XPT\n#define W_XPT 1000000\n");
-	fprintf(th, "#endif\n#endif\n");
+	fprintf(th, "	#if W_XPT==1\n"); /* user typed -DW_XPT without size */
+	fprintf(th, "		#undef W_XPT\n");
+	fprintf(th, "		#define W_XPT 1000000\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "#endif\n");
 	fprintf(th, "#ifndef NFAIR\n");
-	fprintf(th, "#define NFAIR	2	/* must be >= 2 */\n");
+	fprintf(th, "	#define NFAIR	2	/* must be >= 2 */\n");
 	fprintf(th, "#endif\n");
 	if (Ntimeouts)
 	fprintf(th, "#define NTIM	%d\n", Ntimeouts);
@@ -230,18 +358,33 @@ gensrc(void)
 	fprintf(th, "#define REM_VARS	1\n");
 	if (has_remote)
 	fprintf(th, "#define REM_REFS	%d\n", has_remote); /* not yet used */
+	if (has_hidden)
+	{	fprintf(th, "#define HAS_HIDDEN	%d\n", has_hidden);
+		fprintf(th, "#if defined(BFS_PAR) || defined(BFS)\n");
+		fprintf(th, "	#error cannot use BFS on models with variables declared hidden\n");
+		fprintf(th, "#endif\n");
+	}
 	if (has_last)
 	fprintf(th, "#define HAS_LAST	%d\n", has_last);
+	if (has_priority && !old_priority_rules)
+	fprintf(th, "#define HAS_PRIORITY	%d\n", has_priority);
 	if (has_sorted)
 	fprintf(th, "#define HAS_SORTED	%d\n", has_sorted);
 	if (m_loss)
 	fprintf(th, "#define M_LOSS\n");
 	if (has_random)
 	fprintf(th, "#define HAS_RANDOM	%d\n", has_random);
-	fprintf(th, "#define HAS_CODE\n");	/* doesn't seem to cause measurable overhead */
+	if (has_ltl)
+	fprintf(th, "#define HAS_LTL	1\n");
+	fprintf(th, "#define HAS_CODE	1\n");	/* could also be set to has_code */
+		/* always defining it doesn't seem to cause measurable overhead though */
+		/* and allows for pan -r etc to work for non-embedded code as well */
+	fprintf(th, "#if defined(RANDSTORE) && !defined(RANDSTOR)\n");
+	fprintf(th, "	#define RANDSTOR	RANDSTORE\n"); /* xspin uses RANDSTORE... */
+	fprintf(th, "#endif\n");
 	if (has_stack)
-	fprintf(th, "#define HAS_STACK\n");
-	if (has_enabled)
+	fprintf(th, "#define HAS_STACK	%d\n", has_stack);
+	if (has_enabled || (has_priority && !old_priority_rules))
 	fprintf(th, "#define HAS_ENABLED	1\n");
 	if (has_unless)
 	fprintf(th, "#define HAS_UNLESS	%d\n", has_unless);
@@ -252,11 +395,12 @@ gensrc(void)
 	if (has_badelse)
 	fprintf(th, "#define HAS_BADELSE	%d\n", has_badelse);
 	if (has_enabled
+	|| (has_priority && !old_priority_rules)
 	||  has_pcvalue
 	||  has_badelse
 	||  has_last)
 	{	fprintf(th, "#ifndef NOREDUCE\n");
-		fprintf(th, "#define NOREDUCE	1\n");
+		fprintf(th, "	#define NOREDUCE	1\n");
 		fprintf(th, "#endif\n");
 	}
 	if (has_np)
@@ -265,33 +409,46 @@ gensrc(void)
 	fprintf(th, "#define MERGED	1\n");
 
 doless:
-	fprintf(th, "#ifdef NP	/* includes np_ demon */\n");
+	fprintf(th, "#if !defined(HAS_LAST) && defined(BCS)\n");
+	fprintf(th, "	#define HAS_LAST	1 /* use it, but */\n");
+	fprintf(th, "	#ifndef STORE_LAST\n"); /* unless the user insists */
+	fprintf(th, "		#define NO_LAST	1 /* dont store it */\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "#endif\n");
+
+	fprintf(th, "#if defined(BCS) && defined(BITSTATE)\n");
+	fprintf(th, "	#ifndef NO_CTX\n");
+	fprintf(th, "		#define STORE_CTX	1\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "#endif\n");
+
+	fprintf(th, "#ifdef NP\n");
 	if (!has_np)
-	fprintf(th, "#define HAS_NP	2\n");
-	fprintf(th, "#define VERI	%d\n",	nrRdy);
-	fprintf(th, "#define endclaim	3 /* none */\n");
+	fprintf(th, "	#define HAS_NP	2\n");
+	fprintf(th, "	#define VERI	%d	/* np_ */\n",	nrRdy);
 	fprintf(th, "#endif\n");
 	if (claimproc)
-	{	claimnr = fproc(claimproc);
-		/* NP overrides claimproc */
-		fprintf(th, "#if !defined(NOCLAIM) && !defined NP\n");
-		fprintf(th, "#define VERI	%d\n",	claimnr);
-		fprintf(th, "#define endclaim	endstate%d\n",	claimnr);
+	{	claimnr = fproc(claimproc);	/* the default claim */
+		fprintf(th, "#ifndef NOCLAIM\n");
+		fprintf(th, "	#define NCLAIMS	%d\n", nclaims);
+		fprintf(th, "	#ifndef NP\n");
+		fprintf(th, "		#define VERI	%d\n", claimnr);
+		fprintf(th, "	#endif\n");
 		fprintf(th, "#endif\n");
 	}
 	if (eventmap)
 	{	eventmapnr = fproc(eventmap);
 		fprintf(th, "#define EVENT_TRACE	%d\n",	eventmapnr);
-		fprintf(th, "#define endevent	endstate%d\n",	eventmapnr);
+		fprintf(th, "#define endevent	_endstate%d\n",	eventmapnr);
 		if (eventmap[2] == 'o')	/* ":notrace:" */
 		fprintf(th, "#define NEGATED_TRACE	1\n");
 	}
 
-	fprintf(th, "typedef struct S_F_MAP {\n");
-	fprintf(th, "	char *fnm; int from; int upto;\n");
+	fprintf(th, "\ntypedef struct S_F_MAP {\n");
+	fprintf(th, "	char *fnm;\n\tint from;\n\tint upto;\n");
 	fprintf(th, "} S_F_MAP;\n");
 
-	fprintf(tc, "/*** Generated by %s ***/\n", Version);
+	fprintf(tc, "/*** Generated by %s ***/\n", SpinVersion);
 	fprintf(tc, "/*** From source: %s ***/\n\n", oFname->name);
 
 	ntimes(tc, 0, 1, Pre0);
@@ -304,19 +461,36 @@ doless:
 	case 2:	fprintf(tc, "#include \"pan_t.h\"\n"); break;
 	}
 
+	if (separate != 2)
+	{	fprintf(tc, "char *TrailFile = PanSource; /* default */\n");
+		fprintf(tc, "char *trailfilename;\n");
+	}
+
+	fprintf(tc, "#ifdef LOOPSTATE\n");
+	fprintf(tc, "double cnt_loops;\n");
+	fprintf(tc, "#endif\n");
+
 	fprintf(tc, "State	A_Root;	/* seed-state for cycles */\n");
 	fprintf(tc, "State	now;	/* the full state-vector */\n");
+	fprintf(tc, "#if NQS > 0\n");
+	fprintf(tc, "short q_flds[NQS+1];\n");
+	fprintf(tc, "short q_max[NQS+1];\n");
+	fprintf(tc, "#endif\n");
+
 	plunk_c_fcts(tc);	/* State can be used in fcts */
 
 	if (separate != 2)
-		ntimes(tc, 0, 1, Preamble);
-	else
-		fprintf(tc, "extern int verbose; extern long depth;\n");
+	{	ntimes(tc, 0, 1, Preamble);
+		ntimes(tc, 0, 1, Separate); /* things that moved out of pan.h */
+	} else
+	{	fprintf(tc, "extern int verbose;\n");
+		fprintf(tc, "extern long depth, depthfound;\n");
+	}
 
 	fprintf(tc, "#ifndef NOBOUNDCHECK\n");
-	fprintf(tc, "#define Index(x, y)\tBoundcheck(x, y, II, tt, t)\n");
+	fprintf(tc, "	#define Index(x, y)\tBoundcheck(x, y, II, tt, t)\n");
 	fprintf(tc, "#else\n");
-	fprintf(tc, "#define Index(x, y)\tx\n");
+	fprintf(tc, "	#define Index(x, y)\tx\n");
 	fprintf(tc, "#endif\n");
 
 	c_preview();	/* sets hastrack */
@@ -335,7 +509,7 @@ doless:
 		fprintf(tt, "}\n\n");
 		fprintf(tt, "void\nputpeg(int n, int m)\n");
 		fprintf(tt, "{	printf(\"%%5d\ttrans %%4d \", m, n);\n");
-		fprintf(tt, "	printf(\"file %%s line %%3d\\n\",\n");
+		fprintf(tt, "	printf(\"%%s:%%d\\n\",\n");
 		fprintf(tt, "		T_SRC[n].fl, T_SRC[n].ln);\n");
 		fprintf(tt, "}\n");
 		if (!merger)
@@ -359,13 +533,18 @@ doless:
 		}
 
 		fprintf(tm, "#define rand	pan_rand\n");
+		fprintf(tm, "#define pthread_equal(a,b)	((a)==(b))\n");
 		fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n");
-		fprintf(tm, "	printf(\"Pr: %%d Tr: %%d\\n\", II, t->forw);\n");
+		fprintf(tm, "	#ifdef BFS_PAR\n");
+		fprintf(tm, "		bfs_printf(\"Pr: %%d Tr: %%d\\n\", II, t->forw);\n");
+		fprintf(tm, "	#else\n");
+		fprintf(tm, "		cpu_printf(\"Pr: %%d Tr: %%d\\n\", II, t->forw);\n");
+		fprintf(tm, "	#endif\n");
 		fprintf(tm, "#endif\n");
 		fprintf(tm, "	switch (t->forw) {\n");
 	} else
 	{	fprintf(tt, "#ifndef PEG\n");
-		fprintf(tt, "#define tr_2_src(m,f,l)\n");
+		fprintf(tt, "	#define tr_2_src(m,f,l)\n");
 		fprintf(tt, "#endif\n");
 		fprintf(tt, "void\nset_claim(void)\n{\tTrans *T;\n");
 		fprintf(tt, "\textern Trans ***trans;\n");
@@ -373,8 +552,9 @@ doless:
 		fprintf(tt, " char *, int, int, int);\n\n");
 
 		fprintf(tm, "#define rand	pan_rand\n");
+		fprintf(tm, "#define pthread_equal(a,b)	((a)==(b))\n");
 		fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n");
-		fprintf(tm, "	printf(\"Pr: %%d Tr: %%d\\n\", II, forw);\n");
+		fprintf(tm, "	cpu_printf(\"Pr: %%d Tr: %%d\\n\", II, forw);\n");
 		fprintf(tm, "#endif\n");
 		fprintf(tm, "	switch (forw) {\n");
 	}
@@ -404,24 +584,47 @@ doless:
 	fprintf(tb, "	case  0: goto R999; /* nothing to undo */\n");
 
 	for (p = rdy; p; p = p->nxt)
-		putproc(p);
-
+	{	putproc(p);
+	}
 
 	if (separate != 2)
-	{	fprintf(th, "struct {\n");
-		fprintf(th, "	int tp; short *src;\n");
-		fprintf(th, "} src_all[] = {\n");
+	{	fprintf(th, "\n");
+		for (p = rdy; p; p = p->nxt)
+			fprintf(th, "extern short src_ln%d[];\n", p->tn);
+		for (p = rdy; p; p = p->nxt)
+			fprintf(th, "extern S_F_MAP src_file%d[];\n", p->tn);
+		fprintf(th, "\n");
+
+		fprintf(tc, "uchar reached%d[3];  /* np_ */\n", nrRdy);	
+		fprintf(tc, "uchar *loopstate%d;  /* np_ */\n", nrRdy);
+
+		fprintf(tc, "struct {\n");
+		fprintf(tc, "	int tp; short *src;\n");
+		fprintf(tc, "} src_all[] = {\n");
 		for (p = rdy; p; p = p->nxt)
-			fprintf(th, "	{ %d, &src_ln%d[0] },\n",
+			fprintf(tc, "	{ %d, &src_ln%d[0] },\n",
 				p->tn, p->tn);
-		fprintf(th, "	{ 0, (short *) 0 }\n");
-		fprintf(th, "};\n");
-		fprintf(th, "short *frm_st0;\n");	/* records src states for transitions in never claim */
+		fprintf(tc, "	{ 0, (short *) 0 }\n");
+		fprintf(tc, "};\n");
+
+		fprintf(tc, "S_F_MAP *flref[] = {\n");	/* 5.3.0 */
+		for (p = rdy; p; p = p->nxt)
+		{	fprintf(tc, "	src_file%d%c\n", p->tn, p->nxt?',':' ');
+		}
+		fprintf(tc, "};\n\n");
 	} else
-	{	fprintf(th, "extern short *frm_st0;\n");
+	{	fprintf(tc, "extern uchar reached%d[3];  /* np_ */\n", nrRdy);	
 	}
 
-	gencodetable(th);
+	gencodetable(tc);	/* was th */
+
+	if (Unique < (1 << (8*sizeof(unsigned char)) ))	/* was uniq before */
+	{	fprintf(th, "#define T_ID	unsigned char\n");
+	} else if (Unique < (1 << (8*sizeof(unsigned short)) ))
+	{	fprintf(th, "#define T_ID	unsigned short\n");
+	} else
+	{	fprintf(th, "#define T_ID	unsigned int\n");
+	}
 
 	if (separate != 1)
 	{	tm_predef_np();
@@ -438,13 +641,13 @@ doless:
 		genheader();
 		if (separate == 1)
 		{	fprintf(th, "#define FORWARD_MOVES\t\"pan_s.m\"\n");
-			fprintf(th, "#define REVERSE_MOVES\t\"pan_s.b\"\n");
+			fprintf(th, "#define BACKWARD_MOVES\t\"pan_s.b\"\n");
 			fprintf(th, "#define SEPARATE\n");
 			fprintf(th, "#define TRANSITIONS\t\"pan_s.t\"\n");
 			fprintf(th, "extern void ini_claim(int, int);\n");
 		} else
 		{	fprintf(th, "#define FORWARD_MOVES\t\"pan.m\"\n");
-			fprintf(th, "#define REVERSE_MOVES\t\"pan.b\"\n");
+			fprintf(th, "#define BACKWARD_MOVES\t\"pan.b\"\n");
 			fprintf(th, "#define TRANSITIONS\t\"pan.t\"\n");
 		}
 		genaddproc();
@@ -456,33 +659,37 @@ doless:
 		if (!run) fatal("no runable process", (char *)0);
 		fprintf(tc, "void\n");
 		fprintf(tc, "active_procs(void)\n{\n");
+
+		fprintf(tc, "	if (reversing == 0) {\n");
 			reverse_procs(run);
+		fprintf(tc, "	} else {\n");
+			forward_procs(run);
+		fprintf(tc, "	}\n");
+
 		fprintf(tc, "}\n");
 		ntimes(tc, 0, 1, Dfa);
 		ntimes(tc, 0, 1, Xpt);
 
 		fprintf(th, "#define NTRANS	%d\n", uniq);
-		fprintf(th, "#ifdef PEG\n");
-		fprintf(th, "long peg[NTRANS];\n");
-		fprintf(th, "#endif\n");
-
 		if (u_sync && !u_async)
-			spit_recvs(th, tc);
+		{	spit_recvs(th, tc);
+		}
 	} else
 	{	genheader();
 		fprintf(th, "#define FORWARD_MOVES\t\"pan_t.m\"\n");
-		fprintf(th, "#define REVERSE_MOVES\t\"pan_t.b\"\n");
+		fprintf(th, "#define BACKWARD_MOVES\t\"pan_t.b\"\n");
 		fprintf(th, "#define TRANSITIONS\t\"pan_t.t\"\n");
 		fprintf(tc, "extern int Maxbody;\n");
 		fprintf(tc, "#if VECTORSZ>32000\n");
-		fprintf(tc, "extern int proc_offset[];\n");
+		fprintf(tc, "	extern int *proc_offset;\n");
 		fprintf(tc, "#else\n");
-		fprintf(tc, "extern short proc_offset[];\n");
+		fprintf(tc, "	extern short *proc_offset;\n");
 		fprintf(tc, "#endif\n");
-		fprintf(tc, "extern uchar proc_skip[];\n");
+		fprintf(tc, "extern uchar *proc_skip;\n");
 		fprintf(tc, "extern uchar *reached[];\n");
 		fprintf(tc, "extern uchar *accpstate[];\n");
 		fprintf(tc, "extern uchar *progstate[];\n");
+		fprintf(tc, "extern uchar *loopstate[];\n");
 		fprintf(tc, "extern uchar *stopstate[];\n");
 		fprintf(tc, "extern uchar *visstate[];\n\n");
 		fprintf(tc, "extern short *mapstate[];\n");
@@ -491,7 +698,7 @@ doless:
 		fprintf(tc, "\textern State now;\n");
 		fprintf(tc, "\textern void set_claim(void);\n\n");
 		fprintf(tc, "#ifdef PROV\n");
-		fprintf(tc, "#include PROV\n");
+		fprintf(tc, "	#include PROV\n");
 		fprintf(tc, "#endif\n");
 		fprintf(tc, "\tset_claim();\n");
 		genother();
@@ -509,13 +716,42 @@ doless:
 		fprintf(tc, "int\nrev_claim(int backw)\n{ return 0; }\n");
 		fprintf(tc, "#include TRANSITIONS\n");
 	}
-	if (separate != 1)
-		ntimes(tc, 0, 1, Nvr1);
 
 	if (separate != 2)
 	{	c_wrapper(tc);
 		c_chandump(tc);
 	}
+
+	fprintf(th, "#if defined(BFS_PAR) || NCORE>1\n");
+	fprintf(th, "	void e_critical(int);\n");
+	fprintf(th, "	void x_critical(int);\n");
+	fprintf(th, "	#ifdef BFS_PAR\n");
+	fprintf(th, "		void bfs_main(int, int);\n");
+	fprintf(th, "		void bfs_report_mem(void);\n");
+	fprintf(th, "	#endif\n");
+	fprintf(th, "#endif\n");
+
+	fprintf(th, "\n\n/* end of PAN_H */\n#endif\n");
+	fclose(th);
+	fclose(tt);
+	fclose(tm);
+	fclose(tb);
+
+	if (!(th = fopen("pan.p", MFLAGS)))
+	{	printf("spin: cannot create pan.p for -DBFS_PAR\n");
+		return; 	/* we're done anyway */
+	}
+
+	ntimes(th, 0, 1, pan_par);	/* BFS_PAR */
+	fclose(th);
+
+	fprintf(tc, "\nTrans *t_id_lkup[%d];\n\n", globmax+1); 
+
+	if (separate != 2)
+	{	fprintf(tc, "\n#ifdef BFS_PAR\n\t#include \"pan.p\"\n#endif\n");
+	}
+	fprintf(tc, "\n/* end of pan.c */\n");
+	fclose(tc);
 }
 
 static int
@@ -537,13 +773,13 @@ dolen(Symbol *s, char *pre, int pid, int ai, int qln)
 	fprintf(tc, "%s(", pre);
 	if (!(s->hidden&1))
 	{	if (s->context)
-			fprintf(tc, "((P%d *)this)->", pid);
+			fprintf(tc, "(int) ( ((P%d *)this)->", pid);
 		else
-			fprintf(tc, "now.");
+			fprintf(tc, "(int) ( now.");
 	}
 	fprintf(tc, "%s", s->name);
-	if (qln > 1) fprintf(tc, "[%d]", ai);
-	fprintf(tc, ")");
+	if (qln > 1 || s->isarray) fprintf(tc, "[%d]", ai);
+	fprintf(tc, ") )");
 }
 
 struct AA {	char TT[9];	char CC[8]; };
@@ -712,47 +948,60 @@ genconditionals(void)
 	fprintf(tc, "}\n");
 }
 
+extern int find_min(Sequence *);
+extern int find_max(Sequence *);
+
 static void
 putproc(ProcList *p)
 {	Pid = p->tn;
 	Det = p->det;
 
-	if (Pid == claimnr
+	if (pid_is_claim(Pid)
 	&&  separate == 1)
 	{	fprintf(th, "extern uchar reached%d[];\n", Pid);
 #if 0
-		fprintf(th, "extern short nstates%d;\n", Pid);
+		fprintf(th, "extern short _nstates%d;\n", Pid);
 #else
-		fprintf(th, "\n#define nstates%d	%d\t/* %s */\n",
+		fprintf(th, "\n#define _nstates%d	%d\t/* %s */\n",
 			Pid, p->s->maxel, p->n->name);
 #endif
 		fprintf(th, "extern short src_ln%d[];\n", Pid);
+		fprintf(th, "extern uchar *loopstate%d;\n", Pid);
 		fprintf(th, "extern S_F_MAP src_file%d[];\n", Pid);
-		fprintf(th, "#define endstate%d	%d\n",
+		fprintf(th, "#define _endstate%d	%d\n",
 			Pid, p->s->last?p->s->last->seqno:0);
-		fprintf(th, "#define src_claim	src_ln%d\n", claimnr);
-
 		return;
 	}
-	if (Pid != claimnr
+	if (!pid_is_claim(Pid)
 	&&  separate == 2)
 	{	fprintf(th, "extern short src_ln%d[];\n", Pid);
+		fprintf(th, "extern uchar *loopstate%d;\n", Pid);
 		return;
 	}
 
 	AllGlobal = (p->prov)?1:0;	/* process has provided clause */
 
-	fprintf(th, "\n#define nstates%d	%d\t/* %s */\n",
+	fprintf(th, "\n#define _nstates%d	%d\t/* %s */\n",
 		Pid, p->s->maxel, p->n->name);
-	if (Pid == claimnr)
-	fprintf(th, "#define nstates_claim	nstates%d\n", Pid);
+/* new */
+	fprintf(th, "#define minseq%d	%d\n", Pid, find_min(p->s));
+	fprintf(th, "#define maxseq%d	%d\n", Pid, find_max(p->s));
+
+/* end */
+
 	if (Pid == eventmapnr)
-	fprintf(th, "#define nstates_event	nstates%d\n", Pid);
+	fprintf(th, "#define nstates_event	_nstates%d\n", Pid);
+
+	fprintf(th, "#define _endstate%d	%d\n", Pid, p->s->last?p->s->last->seqno:0);
 
-	fprintf(th, "#define endstate%d	%d\n",
-		Pid, p->s->last->seqno);
-	fprintf(tm, "\n		 /* PROC %s */\n", p->n->name);
-	fprintf(tb, "\n		 /* PROC %s */\n", p->n->name);
+	if (p->b == N_CLAIM || p->b == E_TRACE || p->b == N_TRACE)
+	{	fprintf(tm, "\n		 /* CLAIM %s */\n", p->n->name);
+		fprintf(tb, "\n		 /* CLAIM %s */\n", p->n->name);
+	}
+	else
+	{	fprintf(tm, "\n		 /* PROC %s */\n", p->n->name);
+		fprintf(tb, "\n		 /* PROC %s */\n", p->n->name);
+	}
 	fprintf(tt, "\n	/* proctype %d: %s */\n", Pid, p->n->name);
 	fprintf(tt, "\n	trans[%d] = (Trans **)", Pid);
 	fprintf(tt, " emalloc(%d*sizeof(Trans *));\n\n", p->s->maxel);
@@ -761,7 +1010,6 @@ putproc(ProcList *p)
 	{	fprintf(th, "\n#define in_s_scope(x_y3_)	0");
 		fprintf(tc, "\n#define in_r_scope(x_y3_)	0");
 	}
-
 	put_seq(p->s, 2, 0);
 	if (Pid == eventmapnr)
 	{	fprintf(th, "\n\n");
@@ -947,10 +1195,10 @@ put_sub(Element *e, int Tt0, int Tt1)
 	if (e->n->ntyp == D_STEP)
 	{	int inherit = (e->status&(ATOM|L_ATOM));
 		fprintf(tm, "\tcase %d: ", uniq++);
-		fprintf(tm, "/* STATE %d - line %d %s - [",
-			e->seqno, e->n->ln, e->n->fn->name);
+		fprintf(tm, "// STATE %d - %s:%d - [",
+			e->seqno, e->n->fn->name, e->n->ln);
 		comment(tm, e->n, 0);
-		fprintf(tm, "] */\n\t\t");
+		fprintf(tm, "]\n\t\t");
 
 		if (s->last->n->ntyp == BREAK)
 			OkBreak = target(huntele(s->last->nxt,
@@ -971,7 +1219,7 @@ put_sub(Element *e, int Tt0, int Tt1)
 		}
 	
 		fprintf(tb, "\tcase %d: ", uniq-1);
-		fprintf(tb, "/* STATE %d */\n", e->seqno);
+		fprintf(tb, "// STATE %d\n", e->seqno);
 		fprintf(tb, "\t\tsv_restor();\n");
 		fprintf(tb, "\t\tgoto R999;\n");
 		if (e->nxt)
@@ -1024,7 +1272,7 @@ typedef struct CaseCache {
 	struct CaseCache *nxt;
 } CaseCache;
 
-CaseCache *casing[6];
+static CaseCache *casing[6];
 
 static int
 identical(Lextok *p, Lextok *q)
@@ -1076,6 +1324,9 @@ advance(Element *e, int stopat)
 	if (stopat)
 	while (f && f->seqno != stopat)
 	{	f = findnext(f);
+		if (!f)
+		{	break;
+		}
 		switch (f->n->ntyp) {
 		case GOTO:
 		case '.':
@@ -1084,8 +1335,7 @@ advance(Element *e, int stopat)
 			break;
 		default:
 			return f;
-		}
-	}
+	}	}
 	return (Element *) 0;
 }
 
@@ -1107,18 +1357,16 @@ equiv_merges(Element *a, Element *b)
 	if (!stopat_a && !stopat_b)
 		return 1;
 
-	for (;;)
-	{
-		f = advance(a, stopat_a);
-		g = advance(b, stopat_b);
-		if (!f && !g)
-			return 1;
-		if (f && g)
-			return identical(f->n, g->n);
-		else
-			return 0;
-	}
-	return 1;
+	f = advance(a, stopat_a);
+	g = advance(b, stopat_b);
+
+	if (!f && !g)
+		return 1;
+
+	if (f && g)
+		return identical(f->n, g->n);
+
+	return 0;
 }
 
 static CaseCache *
@@ -1174,6 +1422,7 @@ nr_bup(Element *e)
 
 	switch (e->n->ntyp) {
 	case ASGN:
+		if (check_track(e->n) == STRUCT) { break; }
 		nr++;
 		break;
 	case  'r':
@@ -1234,10 +1483,10 @@ nrhops(Element *e)
 		}
 
 		if (f && !f->merge && !f->merge_single && f->seqno != stopat)
-		{	fprintf(tm, "\n\t\tbad hop %s:%d -- at %d, <",
+		{	fprintf(tm, "\n\t\t// bad hop %s:%d -- at %d, <",
 				f->n->fn->name,f->n->ln, f->seqno);
 			comment(tm, f->n, 0);
-			fprintf(tm, "> looking for %d -- merge %d:%d:%d\n\t\t",
+			fprintf(tm, "> looking for %d -- merge %d:%d:%d ",
 				stopat, f->merge, f->merge_start, f->merge_single);
 		 	break;
 		}
@@ -1258,18 +1507,20 @@ check_needed(void)
 }
 
 static void
-doforward(FILE *tm, Element *e)
+doforward(FILE *tm_fd, Element *e)
 {	FSM_use *u;
 
-	putstmnt(tm, e->n, e->seqno);
+	putstmnt(tm_fd, e->n, e->seqno);
 
 	if (e->n->ntyp != ELSE && Det)
-	{	fprintf(tm, ";\n\t\tif (trpt->o_pm&1)\n\t\t");
-		fprintf(tm, "\tuerror(\"non-determinism in D_proctype\")");
+	{	fprintf(tm_fd, ";\n\t\tif (trpt->o_pm&1)\n\t\t");
+		fprintf(tm_fd, "\tuerror(\"non-determinism in D_proctype\")");
 	}
 	if (deadvar && !has_code)
 	for (u = e->dead; u; u = u->nxt)
-	{	fprintf(tm, ";\n\t\t/* dead %d: %s */  ",
+	{	fprintf(tm_fd, ";\n\t\t");
+		fprintf(tm_fd, "if (TstOnly) return 1; /* TT */\n");
+		fprintf(tm_fd, "\t\t/* dead %d: %s */  ",
 			u->special, u->var->name);
 
 		switch (u->special) {
@@ -1281,10 +1532,10 @@ doforward(FILE *tm, Element *e)
 			}
 			if (e->n->ntyp != 'r')
 			{	XZ.sym = u->var;
-				fprintf(tm, "\n#ifdef HAS_CODE\n");
-				fprintf(tm, "\t\tif (!readtrail)\n");
-				fprintf(tm, "#endif\n\t\t\t");
-				putname(tm, "", &XZ, 0, " = 0");
+				fprintf(tm_fd, "\n#ifdef HAS_CODE\n");
+				fprintf(tm_fd, "\t\tif (!readtrail)\n");
+				fprintf(tm_fd, "#endif\n\t\t\t");
+				putname(tm_fd, "", &XZ, 0, " = 0");
 				break;
 			} /* else fall through */
 		case 1:		/* dead after read -- add asgn of rval -- needs bup */
@@ -1292,20 +1543,20 @@ doforward(FILE *tm, Element *e)
 			CnT[YZcnt]++;		/* this step added bups */
 			if (multi_oval)
 			{	check_needed();
-				fprintf(tm, "(trpt+1)->bup.ovals[%d] = ",
+				fprintf(tm_fd, "(trpt+1)->bup.ovals[%d] = ",
 					multi_oval-1);
 				multi_oval++;
 			} else
-				fprintf(tm, "(trpt+1)->bup.oval = ");
-			putname(tm, "", &YZ[YZmax], 0, ";\n");
-			fprintf(tm, "#ifdef HAS_CODE\n");
-			fprintf(tm, "\t\tif (!readtrail)\n");
-			fprintf(tm, "#endif\n\t\t\t");
-			putname(tm, "", &YZ[YZmax], 0, " = 0");
+				fprintf(tm_fd, "(trpt+1)->bup.oval = ");
+			putname(tm_fd, "", &YZ[YZmax], 0, ";\n");
+			fprintf(tm_fd, "#ifdef HAS_CODE\n");
+			fprintf(tm_fd, "\t\tif (!readtrail)\n");
+			fprintf(tm_fd, "#endif\n\t\t\t");
+			putname(tm_fd, "", &YZ[YZmax], 0, " = 0");
 			YZmax++;
 			break;
 	}	}
-	fprintf(tm, ";\n\t\t");
+	fprintf(tm_fd, ";\n\t\t");
 }
 
 static int
@@ -1318,7 +1569,7 @@ dobackward(Element *e, int casenr)
 
 	if (!didcase)
 	{	fprintf(tb, "\n\tcase %d: ", casenr);
-		fprintf(tb, "/* STATE %d */\n\t\t", e->seqno);
+		fprintf(tb, "// STATE %d\n\t\t", e->seqno);
 		didcase++;
 	}
 
@@ -1412,7 +1663,7 @@ case_cache(Element *e, int a)
 {	int bupcase = 0, casenr = uniq, fromcache = 0;
 	CaseCache *Cached = (CaseCache *) 0;
 	Element *f, *g;
-	int j, nrbups, mark, target;
+	int j, nrbups, mark, ntarget;
 	extern int ccache;
 
 	mark = (e->status&ATOM); /* could lose atomicity in a merge chain */
@@ -1439,17 +1690,17 @@ case_cache(Element *e, int a)
 	fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
 
 	if (ccache
-	&&  Pid != claimnr
+	&&  !pid_is_claim(Pid)
 	&&  Pid != eventmapnr
 	&& (Cached = prev_case(e, Pid)))
 	{	bupcase = Cached->b;
 		casenr  = Cached->m;
 		fromcache = 1;
 
-		fprintf(tm, "/* STATE %d - line %d %s - [",
-			e->seqno, e->n->ln, e->n->fn->name);
+		fprintf(tm, "// STATE %d - %s:%d - [",
+			e->seqno, e->n->fn->name, e->n->ln);
 		comment(tm, e->n, 0);
-		fprintf(tm, "] (%d:%d - %d) same as %d (%d:%d - %d) */\n",
+		fprintf(tm, "] (%d:%d - %d) same as %d (%d:%d - %d)\n",
 			e->merge_start, e->merge, e->merge_in,
 			casenr,
 			Cached->e->merge_start, Cached->e->merge, Cached->e->merge_in);
@@ -1457,17 +1708,17 @@ case_cache(Element *e, int a)
 		goto gotit;
 	}
 
-	fprintf(tm, "\tcase %d: /* STATE %d - line %d %s - [",
-		uniq++, e->seqno, e->n->ln, e->n->fn->name);
+	fprintf(tm, "\tcase %d: // STATE %d - %s:%d - [",
+		uniq++, e->seqno, e->n->fn->name, e->n->ln);
 	comment(tm, e->n, 0);
 	nrbups = (e->merge || e->merge_start) ? nrhops(e) : nr_bup(e);
-	fprintf(tm, "] (%d:%d:%d - %d) */\n\t\t",
+	fprintf(tm, "] (%d:%d:%d - %d)\n\t\t",
 		e->merge_start, e->merge, nrbups, e->merge_in);
 
 	if (nrbups > MAXMERGE-1)
 		fatal("merge requires more than 256 bups", (char *)0);
 
-	if (e->n->ntyp != 'r' && Pid != claimnr && Pid != eventmapnr)
+	if (e->n->ntyp != 'r' && !pid_is_claim(Pid) && Pid != eventmapnr)
 		fprintf(tm, "IfNotBlocked\n\t\t");
 
 	if (multi_needed != 0 || multi_undo != 0)
@@ -1482,18 +1733,29 @@ case_cache(Element *e, int a)
 	memset(CnT, 0, sizeof(CnT));
 	YZmax = YZcnt = 0;
 
-/* NEW 4.2.6 */
-	if (Pid == claimnr)
-	{
-		fprintf(tm, "\n#if defined(VERI) && !defined(NP)\n\t\t");
-		fprintf(tm, "{	static int reported%d = 0;\n\t\t", e->seqno);
-		/* source state changes in retrans and must be looked up in frm_st0[t->forw] */
-		fprintf(tm, "	if (verbose && !reported%d)\n\t\t", e->seqno);
-		fprintf(tm, "	{	printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",\n\t\t");
-		fprintf(tm, "			depth, frm_st0[t->forw], src_claim[%d]);\n\t\t", e->seqno);
-		fprintf(tm, "		reported%d = 1;\n\t\t", e->seqno);
-		fprintf(tm, "		fflush(stdout);\n\t\t");
-		fprintf(tm, "}	}\n");
+/* new 4.2.6, revised 6.0.0 */
+	if (pid_is_claim(Pid))
+	{	fprintf(tm, "\n#if defined(VERI) && !defined(NP)\n");
+		fprintf(tm, "#if NCLAIMS>1\n\t\t");
+		 fprintf(tm, "{	static int reported%d = 0;\n\t\t", e->seqno);
+		 fprintf(tm, "	if (verbose && !reported%d)\n\t\t", e->seqno);
+		 fprintf(tm, "	{	int nn = (int) ((Pclaim *)pptr(0))->_n;\n\t\t");
+		 fprintf(tm, "		printf(\"depth %%ld: Claim %%s (%%d), state %%d (line %%d)\\n\",\n\t\t");
+		 fprintf(tm, "			depth, procname[spin_c_typ[nn]], nn, ");
+		 fprintf(tm, "(int) ((Pclaim *)pptr(0))->_p, src_claim[ (int) ((Pclaim *)pptr(0))->_p ]);\n\t\t");
+		 fprintf(tm, "		reported%d = 1;\n\t\t", e->seqno);
+		 fprintf(tm, "		fflush(stdout);\n\t\t");
+		 fprintf(tm, "}	}\n");
+		fprintf(tm, "#else\n\t\t");
+		 fprintf(tm, "{	static int reported%d = 0;\n\t\t", e->seqno);
+		 fprintf(tm, "	if (verbose && !reported%d)\n\t\t", e->seqno);
+		 fprintf(tm, "	{	printf(\"depth %%d: Claim, state %%d (line %%d)\\n\",\n\t\t");
+		 fprintf(tm, "			(int) depth, (int) ((Pclaim *)pptr(0))->_p, ");
+		 fprintf(tm, "src_claim[ (int) ((Pclaim *)pptr(0))->_p ]);\n\t\t");
+		 fprintf(tm, "		reported%d = 1;\n\t\t", e->seqno);
+		 fprintf(tm, "		fflush(stdout);\n\t\t");
+		 fprintf(tm, "}	}\n");
+		fprintf(tm, "#endif\n");
 		fprintf(tm, "#endif\n\t\t");
 	}
 /* end */
@@ -1504,32 +1766,32 @@ case_cache(Element *e, int a)
 	doforward(tm, e);
 
 	if (e->merge_start)
-		target = e->merge_start;
+		ntarget = e->merge_start;
 	else
-		target = e->merge;
+		ntarget = e->merge;
 
-	if (target)
+	if (ntarget)
 	{	f = e;
 
 more:		if (f->n->ntyp == GOTO)
 		{	g = get_lab(f->n, 1);
-			if (g->seqno == target)
+			if (g->seqno == ntarget)
 				f = g;
 			else
-				f = huntele(g, f->status, target);
+				f = huntele(g, f->status, ntarget);
 		} else
 			f = f->nxt;
 
 
-		if (f && f->seqno != target)
+		if (f && f->seqno != ntarget)
 		{	if (!f->merge && !f->merge_single)
 			{	fprintf(tm, "/* stop at bad hop %d, %d */\n\t\t",
-					f->seqno, target);
+					f->seqno, ntarget);
 				goto out;
 			}
 			fprintf(tm, "/* merge: ");
 			comment(tm, f->n, 0);
-			fprintf(tm,  "(%d, %d, %d) */\n\t\t", f->merge, f->seqno, target);
+			fprintf(tm,  "(%d, %d, %d) */\n\t\t", f->merge, f->seqno, ntarget);
 			fprintf(tm, "reached[%d][%d] = 1;\n\t\t", Pid, f->seqno);
 			YZcnt++;
 			lab_transfer(e, f);
@@ -1547,8 +1809,8 @@ out:
 	multi_needed = 0;
 	didcase = 0;
 
-	if (target)
-		lastfirst(target, e, casenr); /* mergesteps only */
+	if (ntarget)
+		lastfirst(ntarget, e, casenr); /* mergesteps only */
 
 	dobackward(e, casenr);			/* the original step */
 
@@ -1557,7 +1819,7 @@ out:
 	if (e->merge || e->merge_start)
 	{	if (!didcase)
 		{	fprintf(tb, "\n\tcase %d: ", casenr);
-			fprintf(tb, "/* STATE %d */", e->seqno);
+			fprintf(tb, "// STATE %d", e->seqno);
 			didcase++;
 		} else
 			fprintf(tb, ";");
@@ -1607,8 +1869,8 @@ put_el(Element *e, int Tt0, int Tt1)
 	} else
 		a = 0;
 	if (g
-	&&  (g->status&CHECK2	/* entering remotely ref'd state */
-	||   e->status&CHECK2))	/* leaving  remotely ref'd state */
+	&&  ((g->status&CHECK2)		/* entering remotely ref'd state */
+	||   (e->status&CHECK2)))	/* leaving  remotely ref'd state */
 		e->status |= I_GLOB;
 
 	/* don't remove dead edges in here, to preserve structure of fsm */
@@ -1758,8 +2020,8 @@ put_seq(Sequence *s, int Tt0, int Tt1)
 				{	fprintf(tt, "#if 0\n\t/* dead link: */\n");
 					deadlink = 1;
 					if (verbose&32)
-					printf("spin: line %3d  %s, Warning: condition is always false\n",
-						g->n->ln, g->n->fn?g->n->fn->name:"");
+					printf("spin: %s:%d, warning, condition is always false\n",
+						g->n->fn?g->n->fn->name:"", g->n->ln);
 				} else
 					deadlink = 0;
 				if (0) printf("			settr %d %d\n", a, 0);
@@ -1867,7 +2129,7 @@ find_target(Element *e)
 	case BREAK:
 		if (e->nxt)
 		{	f = find_target(huntele(e->nxt, e->status, -1));
-			break;	/* 4.3.0 -- was missing */
+			break;	/* new 5.0 -- was missing */
 		}
 		/* else fall through */
 	default:
@@ -1888,6 +2150,26 @@ target(Element *e)
 }
 
 static int
+seq_has_el(Sequence *s, Element *g)		/* new to version 5.0 */
+{	Element *f;
+	SeqList *h;
+
+	for (f = s->frst; f; f = f->nxt)	/* g in same atomic? */
+	{	if (f == g)
+		{	return 1;
+		}
+		if (f->status & CHECK3)
+		{	continue;
+		}
+		f->status |= CHECK3; /* protect against cycles */
+		for (h = f->sub; h; h = h->nxt)
+		{	if (h->this && seq_has_el(h->this, g))
+			{	return 1;
+	}	}	}
+	return 0;
+}
+
+static int
 scan_seq(Sequence *s)
 {	Element *f, *g;
 	SeqList *h;
@@ -1896,20 +2178,22 @@ scan_seq(Sequence *s)
 	{	if ((f->status&CHECK2)
 		||  has_global(f->n))
 			return 1;
-		if (f->n->ntyp == GOTO)	/* may reach other atomic */
-		{
-#if 0
-			/* if jumping from an atomic without globals into
-			 * one with globals, this does the wrong thing
+		if  (f->n->ntyp == GOTO	/* may exit or reach other atomic */
+		&& !(f->status & D_ATOM))	/* cannot jump from d_step */
+		{	/* consider jump from an atomic without globals into
+			 * an atomic with globals
 			 * example by Claus Traulsen, 22 June 2007
 			 */
 			g = target(f);
+#if 1
+			if (g && !seq_has_el(s, g)) /* not internal to this atomic/dstep */
+
+#else
 			if (g
 			&& !(f->status & L_ATOM)
 			&& !(g->status & (ATOM|L_ATOM)))
 #endif
-			{	fprintf(tt, "	/* mark-down line %d */\n",
-					f->n->ln);
+			{	fprintf(tt, "\t/* mark-down line %d status %d = %d */\n", f->n->ln, f->status, (f->status & D_ATOM));
 				return 1; /* assume worst case */
 		}	}
 		for (h = f->sub; h; h = h->nxt)
@@ -1937,9 +2221,26 @@ glob_args(Lextok *n)
 	return result;
 }
 
+static int
+proc_is_safe(const Lextok *n)
+{	ProcList *p;
+	/* not safe unless no local var inits are used */
+	/* note that a local variable init could refer to a global */
+
+	for (p = rdy; p; p = p->nxt)
+	{	if (strcmp(n->sym->name, p->n->name) == 0)
+		{	/* printf("proc %s safety: %d\n", p->n->name, p->unsafe); */
+			return (p->unsafe != 0);
+	}	}
+/*	non_fatal("bad call to proc_is_safe", (char *) 0);	*/
+	/* cannot happen */
+	return 0;
+}
+
 int
 has_global(Lextok *n)
-{	Lextok *v; extern int runsafe;
+{	Lextok *v;
+	static Symbol *n_seen = (Symbol *) 0;
 
 	if (!n) return 0;
 	if (AllGlobal) return 1;	/* global provided clause */
@@ -1968,6 +2269,14 @@ has_global(Lextok *n)
 	case  LEN:   return (((n->sym->xu)&(XR|XS|XX)) != (XR|XS));
 
 	case   NAME:
+		if (strcmp(n->sym->name, "_priority") == 0)
+		{	if (old_priority_rules)
+			{	if (n_seen != n->sym)
+					fatal("cannot refer to _priority with -o6", (char *) 0);
+				n_seen = n->sym;
+			}
+			return 0;
+		}
 		if (n->sym->context
 		|| (n->sym->hidden&64)
 		||  strcmp(n->sym->name, "_pid") == 0
@@ -1975,14 +2284,15 @@ has_global(Lextok *n)
 			return 0;
 		return 1;
 
-	case RUN: return 1-runsafe;
+	case RUN:
+		return proc_is_safe(n);
 
 	case C_CODE: case C_EXPR:
 		return glob_inline(n->sym->name);
 
 	case ENABLED: case PC_VAL: case NONPROGRESS:
-	case 'p': case 'q':
-	case TIMEOUT:
+	case 'p':    case 'q':
+	case TIMEOUT: case SET_P:  case GET_P:
 		return 1;
 
 	/* 	@ was 1 (global) since 2.8.5
@@ -2017,11 +2327,12 @@ static void
 Bailout(FILE *fd, char *str)
 {
 	if (!GenCode)
-		fprintf(fd, "continue%s", str);
-	else if (IsGuard)
-		fprintf(fd, "%s%s", NextLab[Level], str);
-	else
-		fprintf(fd, "Uerror(\"block in step seq\")%s", str);
+	{	fprintf(fd, "continue%s", str);
+	} else if (IsGuard)
+	{	fprintf(fd, "%s%s", NextLab[Level], str);
+	} else
+	{	fprintf(fd, "Uerror(\"block in d_step seq\")%s", str);
+	}
 }
 
 #define cat0(x)   	putstmnt(fd,now->lft,m); fprintf(fd, x); \
@@ -2029,6 +2340,7 @@ Bailout(FILE *fd, char *str)
 #define cat1(x)		fprintf(fd,"("); cat0(x); fprintf(fd,")")
 #define cat2(x,y)  	fprintf(fd,x); putstmnt(fd,y,m)
 #define cat3(x,y,z)	fprintf(fd,x); putstmnt(fd,y,m); fprintf(fd,z)
+#define cat30(x,y,z)	fprintf(fd,x,0); putstmnt(fd,y,m); fprintf(fd,z)
 
 void
 putstmnt(FILE *fd, Lextok *now, int m)
@@ -2070,12 +2382,14 @@ putstmnt(FILE *fd, Lextok *now, int m)
 		else
 			fprintf(fd, "((trpt->tau)&1)");
 		if (GenCode)
-		 printf("spin: line %3d, warning: 'timeout' in d_step sequence\n",
-			lineno);
+		 printf("spin: %s:%d, warning, 'timeout' in d_step sequence\n",
+			Fname->name, lineno);
 		/* is okay as a guard */
 		break;
 
 	case RUN:
+		if (now->sym == NULL)
+			fatal("internal error pangen2.c", (char *) 0);
 		if (claimproc
 		&&  strcmp(now->sym->name, claimproc) == 0)
 			fatal("claim %s, (not runnable)", claimproc);
@@ -2084,29 +2398,57 @@ putstmnt(FILE *fd, Lextok *now, int m)
 			fatal("eventmap %s, (not runnable)", eventmap);
 
 		if (GenCode)
-		  fatal("'run' in d_step sequence (use atomic)",
-			(char *)0);
+			fatal("'run' in d_step sequence (use atomic)", (char *)0);
 
-		fprintf(fd,"addproc(%d", fproc(now->sym->name));
+		fprintf(fd,"addproc(II, %d, %d",
+			(now->val > 0 && !old_priority_rules) ? now->val : 1,
+			fproc(now->sym->name));
 		for (v = now->lft, i = 0; v; v = v->rgt, i++)
 		{	cat2(", ", v->lft);
 		}
 		check_param_count(i, now);
 
 		if (i > Npars)
-		{	printf("\t%d parameters used, max %d expected\n", i, Npars);
-			fatal("too many parameters in run %s(...)",
-			now->sym->name);
+		{	/* printf("\t%d parameters used, max %d expected\n", i, Npars); */
+			fatal("too many parameters in run %s(...)", now->sym->name);
 		}
 		for ( ; i < Npars; i++)
 			fprintf(fd, ", 0");
 		fprintf(fd, ")");
+#if 0
+		/* process now->sym->name has run priority now->val */
+		if (now->val > 0 && now->val < 256 && !old_priority_rules)
+		{	fprintf(fd, " && (((P0 *)pptr(now._nr_pr - 1))->_priority = %d)", now->val);
+		}
+#endif
+		if (now->val < 0 || now->val > 255)	/* 0 itself is allowed */
+		{	fatal("bad process in run %s, valid range: 1..255", now->sym->name);
+		}
 		break;
 
 	case ENABLED:
 		cat3("enabled(II, ", now->lft, ")");
 		break;
 
+	case GET_P:
+		if (old_priority_rules)
+		{	fprintf(fd, "1");
+		} else
+		{	cat3("get_priority(", now->lft, ")");
+		}
+		break;
+
+	case SET_P:
+		if (!old_priority_rules)
+		{	fprintf(fd, "if (TstOnly) return 1; /* T30 */\n\t\t");
+			fprintf(fd, "set_priority(");
+			putstmnt(fd, now->lft->lft, m);
+			fprintf(fd, ", ");
+			putstmnt(fd, now->lft->rgt, m);
+			fprintf(fd, ")");
+		}
+		break;
+
 	case NONPROGRESS:
 		/* o_pm&4=progress, tau&128=claim stutter */
 		if (separate == 2)
@@ -2180,7 +2522,7 @@ putstmnt(FILE *fd, Lextok *now, int m)
 
 	case 's':
 		if (Pid == eventmapnr)
-		{	fprintf(fd, "if ((ot == EVENT_TRACE && _tp != 's') ");
+		{	fprintf(fd, "if ((II == -EVENT_TRACE && _tp != 's') ");
 			putname(fd, "|| _qid+1 != ", now->lft, m, "");
 			for (v = now->rgt, i=0; v; v = v->rgt, i++)
 			{	if (v->lft->ntyp != CONST
@@ -2208,31 +2550,37 @@ putstmnt(FILE *fd, Lextok *now, int m)
 			break;
 		}
 		if (has_xu)
-		{	fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
-			putname(fd, "if (q_claim[", now->lft, m, "]&2) ");
-			putname(fd, "q_S_check(", now->lft, m, ", II);");
-			fprintf(fd, "\n#endif\n\t\t");
+		{	fprintf(fd, "\n#if !defined(XUSAFE) && !defined(NOREDUCE)\n\t\t");
+			putname(fd, "if (q_claim[", now->lft, m, "]&2)\n\t\t");
+			putname(fd, "{	q_S_check(", now->lft, m, ", II);\n\t\t");
+			fprintf(fd, "}\n");
+			if (has_sorted && now->val == 1)
+			{	putname(fd, "\t\tif (q_claim[", now->lft, m, "]&1)\n\t\t"); /* &1 iso &2 */
+				fprintf(fd, "{	uerror(\"sorted send on xr channel violates po reduction\");\n\t\t");
+				fprintf(fd, "}\n");
+			}
+			fprintf(fd, "#endif\n\t\t");
 		}
 		fprintf(fd, "if (q_%s",
 			(u_sync > 0 && u_async == 0)?"len":"full");
 		putname(fd, "(", now->lft, m, "))\n");
 
 		if (m_loss)
-			fprintf(fd, "\t\t{ nlost++; delta_m = 1; } else {");
-		else
+		{	fprintf(fd, "\t\t{ nlost++; delta_m = 1; } else {");
+		} else
 		{	fprintf(fd, "\t\t\t");
 			Bailout(fd, ";");
 		}
 
-		if (has_enabled)
-			fprintf(fd, "\n\t\tif (TstOnly) return 1;");
+		if (has_enabled || has_priority)
+			fprintf(fd, "\n\t\tif (TstOnly) return 1; /* T1 */");
 
 		if (u_sync && !u_async && rvopt)
 			fprintf(fd, "\n\n\t\tif (no_recvs(II)) continue;\n");
 
 		fprintf(fd, "\n#ifdef HAS_CODE\n");
 		fprintf(fd, "\t\tif (readtrail && gui) {\n");
-		fprintf(fd, "\t\t\tchar simtmp[32];\n");
+		fprintf(fd, "\t\t\tchar simtmp[64];\n");
 		putname(fd, "\t\t\tsprintf(simvals, \"%%d!\", ", now->lft, m, ");\n");
 		_isok++;
 		for (v = now->rgt, i = 0; v; v = v->rgt, i++)
@@ -2256,9 +2604,9 @@ putstmnt(FILE *fd, Lextok *now, int m)
 			printf("	%d msg parameters sent, %d expected\n", i, Mpars);
 			fatal("too many pars in send", "");
 		}
-		for ( ; i < Mpars; i++)
+		for (j = i; i < Mpars; i++)
 			fprintf(fd, ", 0");
-		fprintf(fd, ")");
+		fprintf(fd, ", %d)", j);
 		if (u_sync)
 		{	fprintf(fd, ";\n\t\t");
 			if (u_async)
@@ -2274,7 +2622,7 @@ putstmnt(FILE *fd, Lextok *now, int m)
 
 	case 'r':
 		if (Pid == eventmapnr)
-		{	fprintf(fd, "if ((ot == EVENT_TRACE && _tp != 'r') ");
+		{	fprintf(fd, "if ((II == -EVENT_TRACE && _tp != 'r') ");
 			putname(fd, "|| _qid+1 != ", now->lft, m, "");
 			for (v = now->rgt, i=0; v; v = v->rgt, i++)
 			{	if (v->lft->ntyp != CONST
@@ -2342,10 +2690,13 @@ putstmnt(FILE *fd, Lextok *now, int m)
 			break;
 		}
 		if (has_xu)
-		{	fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
-			putname(fd, "if (q_claim[", now->lft, m, "]&1) ");
-			putname(fd, "q_R_check(", now->lft, m, ", II);");
-			fprintf(fd, "\n#endif\n\t\t");
+		{	fprintf(fd, "\n#if !defined(XUSAFE) && !defined(NOREDUCE)\n\t\t");
+			putname(fd, "if (q_claim[", now->lft, m, "]&1)\n\t\t");
+			putname(fd, "{	q_R_check(", now->lft, m, ", II);\n\t\t");
+			if (has_random && now->val != 0)
+			fprintf(fd, "	uerror(\"rand receive on xr channel violates po reduction\");\n\t\t");
+			fprintf(fd, "}\n");
+			fprintf(fd, "#endif\n\t\t");
 		}
 		if (u_sync)
 		{	if (now->val >= 2)
@@ -2398,6 +2749,8 @@ putstmnt(FILE *fd, Lextok *now, int m)
 				  fprintf(fd, "0, %d, 0)) ", i);
 				  Bailout(fd, "");
 			}	}
+			if (has_enabled || has_priority)
+				fprintf(fd, ";\n\t\tif (TstOnly) return 1 /* T2 */");
 		} else	/* random receive: val 1 or 3 */
 		{	fprintf(fd, ";\n\t\tif (!(XX = Q_has(");
 			putname(fd, "", now->lft, m, "");
@@ -2415,19 +2768,21 @@ putstmnt(FILE *fd, Lextok *now, int m)
 				fprintf(fd, ", 0, 0");
 			fprintf(fd, "))) ");
 			Bailout(fd, "");
-			fprintf(fd, ";\n\t\t");
-			if (multi_oval)
-			{	check_needed();
-				fprintf(fd, "(trpt+1)->bup.ovals[%d] = ",
-					multi_oval-1);
-				multi_oval++;
-			} else
-				fprintf(fd, "(trpt+1)->bup.oval = ");
-			fprintf(fd, "XX");
-		}
 
-		if (has_enabled)
-			fprintf(fd, ";\n\t\tif (TstOnly) return 1");
+			if (has_enabled || has_priority)
+				fprintf(fd, ";\n\t\tif (TstOnly) return 1 /* T2 */");
+			if (!GenCode) {
+				fprintf(fd, ";\n\t\t");
+				if (multi_oval)
+				{	check_needed();
+					fprintf(fd, "(trpt+1)->bup.ovals[%d] = ",
+						multi_oval-1);
+					multi_oval++;
+				} else
+				{	fprintf(fd, "(trpt+1)->bup.oval = ");
+				}
+				fprintf(fd, "XX");
+		}	}
 
 		if (j == 0 && now->val >= 2)
 		{	fprintf(fd, ";\n\t\t");
@@ -2439,16 +2794,20 @@ putstmnt(FILE *fd, Lextok *now, int m)
 			fprintf(fd, ";\n\t\t");
 			/* no variables modified */
 			if (j == 0 && now->val == 0)
-			{	fprintf(fd, "if (q_flds[((Q0 *)qptr(");
+			{	fprintf(fd, "\n#ifndef BFS_PAR\n\t\t");
+				/* q_flds values are not shared among cores */
+				fprintf(fd, "if (q_flds[((Q0 *)qptr(");
 				putname(fd, "", now->lft, m, "-1))->_t]");
-				fprintf(fd, " != %d)\n\t", i);
-				fprintf(fd, "\t\tUerror(\"wrong nr of msg fields in rcv\");\n\t\t");
+				fprintf(fd, " != %d)\n\t\t\t", i);
+				fprintf(fd, "Uerror(\"wrong nr of msg fields in rcv\");\n");
+				fprintf(fd, "#endif\n\t\t");
 			}
 
 			for (v = now->rgt; v; v = v->rgt)
-				if ((v->lft->ntyp != CONST
+			{	if ((v->lft->ntyp != CONST
 				&&   v->lft->ntyp != EVAL))
-					jj++;	/* nr of vars needing bup */
+				{	jj++;	/* nr of vars needing bup */
+			}	}
 
 			if (jj)
 			for (v = now->rgt, i = 0; v; v = v->rgt, i++)
@@ -2467,12 +2826,12 @@ putstmnt(FILE *fd, Lextok *now, int m)
 					sprintf(tempbuf, "(trpt+1)->bup.oval = ");
 
 				if (v->lft->sym && !strcmp(v->lft->sym->name, "_"))
-				{	fprintf(fd, tempbuf);
+				{	fprintf(fd, tempbuf, (char *) 0);
 					putname(fd, "qrecv(", now->lft, m, "");
 					fprintf(fd, ", XX-1, %d, 0);\n\t\t", i);
 				} else
 				{	_isok++;
-					cat3(tempbuf, v->lft, ";\n\t\t");
+					cat30(tempbuf, v->lft, ";\n\t\t");
 					_isok--;
 				}
 			}
@@ -2485,7 +2844,7 @@ putstmnt(FILE *fd, Lextok *now, int m)
 					&&  v->lft->ntyp != EVAL
 					&&  v->lft->sym
 					&&  v->lft->sym->type != STRUCT	/* not a struct */
-					&&  v->lft->sym->nel == 1	/* not an array */
+					&&  (v->lft->sym->nel == 1 && v->lft->sym->isarray == 0) /* not array */
 					&&  strcmp(v->lft->sym->name, "_") != 0)
 					for (w = v->rgt; w; w = w->rgt)
 						if (v->lft->sym == w->lft->sym)
@@ -2501,6 +2860,7 @@ putstmnt(FILE *fd, Lextok *now, int m)
 
 			if (v->lft->ntyp != CONST
 			&&  v->lft->ntyp != EVAL
+			&&  v->lft->sym != NULL
 			&&  strcmp(v->lft->sym->name, "_") != 0)
 			{	nocast=1;
 				_isok++;
@@ -2515,6 +2875,7 @@ putstmnt(FILE *fd, Lextok *now, int m)
 
 			if (v->lft->ntyp != CONST
 			&&  v->lft->ntyp != EVAL
+			&&  v->lft->sym != NULL
 			&& strcmp(v->lft->sym->name, "_") != 0
 			&&  (v->lft->ntyp != NAME
 			||   v->lft->sym->type != CHAN))
@@ -2658,8 +3019,10 @@ putstmnt(FILE *fd, Lextok *now, int m)
 		break;
 
 	case ASGN:
-		if (has_enabled)
-		fprintf(fd, "if (TstOnly) return 1;\n\t\t");
+		if (check_track(now) == STRUCT) { break; }
+
+		if (has_enabled || has_priority)
+		fprintf(fd, "if (TstOnly) return 1; /* T3 */\n\t\t");
 		_isok++;
 
 		if (!GenCode)
@@ -2669,14 +3032,27 @@ putstmnt(FILE *fd, Lextok *now, int m)
 				sprintf(tempbuf, "(trpt+1)->bup.ovals[%d] = ",
 					multi_oval-1);
 				multi_oval++;
-				cat3(tempbuf, now->lft, ";\n\t\t");
+				cat30(tempbuf, now->lft, ";\n\t\t");
 			} else
 			{	cat3("(trpt+1)->bup.oval = ", now->lft, ";\n\t\t");
 		}	}
+		if (now->lft->sym
+		&&  now->lft->sym->type == PREDEF
+		&&  strcmp(now->lft->sym->name, "_") != 0
+		&&  strcmp(now->lft->sym->name, "_priority") != 0)
+		{	fatal("invalid assignment to %s", now->lft->sym->name);
+		}
+
 		nocast = 1; putstmnt(fd,now->lft,m); nocast = 0;
 		fprintf(fd," = ");
 		_isok--;
-		putstmnt(fd,now->rgt,m);
+		if (now->lft->sym->isarray
+		&&  now->rgt->ntyp == ',')	/* array initializer */
+		{	putstmnt(fd, now->rgt->lft, m);
+			non_fatal("cannot use an array list initializer here", (char *) 0);
+		} else
+		{	putstmnt(fd, now->rgt, m);
+		}
 
 		if (now->sym->type != CHAN
 		||  verbose > 0)
@@ -2695,8 +3071,8 @@ putstmnt(FILE *fd, Lextok *now, int m)
 		break;
 
 	case PRINT:
-		if (has_enabled)
-		fprintf(fd, "if (TstOnly) return 1;\n\t\t");
+		if (has_enabled || has_priority)
+			fprintf(fd, "if (TstOnly) return 1; /* T4 */\n\t\t");
 #ifdef PRINTF
 		fprintf(fd, "printf(%s", now->sym->name);
 #else
@@ -2709,8 +3085,8 @@ putstmnt(FILE *fd, Lextok *now, int m)
 		break;
 
 	case PRINTM:
-		if (has_enabled)
-		fprintf(fd, "if (TstOnly) return 1;\n\t\t");
+		if (has_enabled || has_priority)
+			fprintf(fd, "if (TstOnly) return 1; /* T5 */\n\t\t");
 		fprintf(fd, "printm(");
 		if (now->lft && now->lft->ismtyp)
 			fprintf(fd, "%d", now->lft->val);
@@ -2732,7 +3108,7 @@ putstmnt(FILE *fd, Lextok *now, int m)
 
 	case   'q':
 		if (terse)
-			fprintf(fd, "%s", now->sym->name);
+			fprintf(fd, "%s", now->sym?now->sym->name:"?");
 		else
 			fprintf(fd, "%d", remotelab(now));
 		break;
@@ -2748,14 +3124,16 @@ putstmnt(FILE *fd, Lextok *now, int m)
 		break;
 
 	case C_CODE:
-		fprintf(fd, "/* %s */\n\t\t", now->sym->name);
-		if (has_enabled)
-			fprintf(fd, "if (TstOnly) return 1;\n\t\t");
-		if (!GenCode)	/* not in d_step */
-		{	fprintf(fd, "sv_save();\n\t\t");
-			/* store the old values for reverse moves */
-		}
-		plunk_inline(fd, now->sym->name, 1);
+		if (now->sym)
+			fprintf(fd, "/* %s */\n\t\t", now->sym->name);
+		if (has_enabled || has_priority)
+			fprintf(fd, "if (TstOnly) return 1; /* T6 */\n\t\t");
+
+		if (now->sym)
+			plunk_inline(fd, now->sym->name, 1, GenCode);
+		else
+			fatal("internal error pangen2.c", (char *) 0);
+
 		if (!GenCode)
 		{	fprintf(fd, "\n");	/* state changed, capture it */
 			fprintf(fd, "#if defined(C_States) && (HAS_TRACK==1)\n");
@@ -2765,10 +3143,10 @@ putstmnt(FILE *fd, Lextok *now, int m)
 		break;
 
 	case ASSERT:
-		if (has_enabled)
-			fprintf(fd, "if (TstOnly) return 1;\n\t\t");
+		if (has_enabled || has_priority)
+			fprintf(fd, "if (TstOnly) return 1; /* T7 */\n\t\t");
 
-		cat3("assert(", now->lft, ", ");
+		cat3("spin_assert(", now->lft, ", ");
 		terse = nocast = 1;
 		cat3("\"", now->lft, "\", II, tt, t)");
 		terse = nocast = 0;
@@ -2788,7 +3166,7 @@ putstmnt(FILE *fd, Lextok *now, int m)
 			break;
 		}
 
-		if (has_enabled)
+		if (has_enabled || has_priority)
 		{	fprintf(fd, "if (TstOnly)\n\t\t\t");
 			fprintf(fd, "return (II+1 == now._nr_pr);\n\t\t");
 		}
@@ -2797,16 +3175,30 @@ putstmnt(FILE *fd, Lextok *now, int m)
 		break;
 
 	default:
-		printf("spin: bad node type %d (.m) - line %d\n",
-			now->ntyp, now->ln);
-		fflush(tm);
+		printf("spin: error, %s:%d, bad node type %d (.m)\n",
+			now->fn->name, now->ln, now->ntyp);
+		fflush(fd);
 		alldone(1);
 	}
 }
 
+char *
+simplify_name(char *s)
+{	char *t = s;
+
+	if (!old_scope_rules)
+	{	while (*t == '_' || isdigit((int)*t))
+		{	t++;
+	}	}
+
+	return t;
+}
+
 void
 putname(FILE *fd, char *pre, Lextok *n, int m, char *suff) /* varref */
 {	Symbol *s = n->sym;
+	char *ptr;
+
 	lineno = n->ln; Fname = n->fn;
 
 	if (!s)
@@ -2819,48 +3211,67 @@ putname(FILE *fd, char *pre, Lextok *n, int m, char *suff) /* varref */
 	{	fprintf(fd, "%s%s%s", pre, n->sym->name, suff);
 		return;
 	}
+
 	if (!s->type)	/* not a local name */
 		s = lookup(s->name);	/* must be a global */
 
 	if (!s->type)
 	{	if (strcmp(pre, ".") != 0)
-		non_fatal("undeclared variable '%s'", s->name);
+			fatal("undeclared variable '%s'", s->name);
 		s->type = INT;
 	}
 
 	if (s->type == PROCTYPE)
 		fatal("proctype-name '%s' used as array-name", s->name);
 
-	fprintf(fd, pre);
+	fprintf(fd, pre, 0);
 	if (!terse && !s->owner && evalindex != 1)
-	{	if (s->context
-		||  strcmp(s->name, "_p") == 0
-		||  strcmp(s->name, "_pid") == 0)
-		{	fprintf(fd, "((P%d *)this)->", Pid);
+	{	if (old_priority_rules
+		&&  strcmp(s->name, "_priority") == 0)
+		{	fprintf(fd, "1");	
+			goto shortcut;
 		} else
-		{	int x = strcmp(s->name, "_");
-			if (!(s->hidden&1) && x != 0)
-				fprintf(fd, "now.");
-			if (x == 0 && _isok == 0)
-				fatal("attempt to read value of '_'", 0);
-	}	}
-
-	if (withprocname
-	&&  s->context
-	&&  strcmp(pre, "."))
-		fprintf(fd, "%s:", s->context->name);
+		{	if (s->context
+			||  strcmp(s->name, "_p") == 0
+			||  strcmp(s->name, "_pid") == 0
+			||  strcmp(s->name, "_priority") == 0)
+			{	fprintf(fd, "((P%d *)this)->", Pid);
+			} else
+			{	int x = strcmp(s->name, "_");
+				if (!(s->hidden&1) && x != 0)
+					fprintf(fd, "now.");
+				if (x == 0 && _isok == 0)
+					fatal("attempt to read value of '_'", 0);
+	}	}	}
+
+	if (terse && buzzed == 1)
+	{	fprintf(fd, "B_state.%s", (s->context)?"local[B_pid].":"");
+	}
+
+	ptr = s->name;
+
+	if (!dont_simplify	/* new 6.4.3 */
+	&&  s->type != PREDEF)	/* new 6.0.2 */
+	{	if (withprocname
+		&&  s->context
+		&&  strcmp(pre, "."))
+		{	fprintf(fd, "%s:", s->context->name);
+			ptr = simplify_name(ptr);
+		} else
+		{	if (terse)
+			{	ptr = simplify_name(ptr);
+	}	}	}
 
 	if (evalindex != 1)
-		fprintf(fd, "%s", s->name);
+		fprintf(fd, "%s", ptr);
 
-	if (s->nel != 1)
+	if (s->nel > 1 || s->isarray == 1)
 	{	if (no_arrays)
-		{
-		non_fatal("ref to array element invalid in this context",
-			(char *)0);
-		printf("\thint: instead of, e.g., x[rs] qu[3], use\n");
-		printf("\tchan nm_3 = qu[3]; x[rs] nm_3;\n");
-		printf("\tand use nm_3 in sends/recvs instead of qu[3]\n");
+		{	non_fatal("ref to array element invalid in this context",
+				(char *)0);
+			printf("\thint: instead of, e.g., x[rs] qu[3], use\n");
+			printf("\tchan nm_3 = qu[3]; x[rs] nm_3;\n");
+			printf("\tand use nm_3 in sends/recvs instead of qu[3]\n");
 		}
 		/* an xr or xs reference to an array element
 		 * becomes an exclusion tag on the array itself -
@@ -2885,15 +3296,32 @@ putname(FILE *fd, char *pre, Lextok *n, int m, char *suff) /* varref */
 			|| (!n->lft && s->nel > 0))
 			{	cat3("[", n->lft, "]");
 			} else
-			{	cat3("[ Index(", n->lft, ", ");
+			{	/* attempt to catch arrays that are indexed with an array element in the same array
+				 * this causes trouble in the verifier in the backtracking
+				 * e.g., restoring a[?] in the assignment: a [a[1]] = x where a[1] == 1
+				 * but it is hard when the array is inside a structure, so the names dont match
+				 */
+#if 0
+				if (n->lft->ntyp == NAME)
+				{	printf("%4d: Basename %s	index %s\n",
+						n->lft->ln, s->name, n->lft->sym->name);
+				}
+#endif
+				cat3("[ Index(", n->lft, ", ");
 				fprintf(fd, "%d) ]", s->nel);
-			}
-		}
-	}
+		}	}
+	} else
+	{	if (n->lft	/* effectively a scalar, but with an index */
+		&& (n->lft->ntyp != CONST
+		||  n->lft->val != 0))
+		{	fatal("ref to scalar '%s' using array index", (char *) ptr);
+	}	}
+
 	if (s->type == STRUCT && n->rgt && n->rgt->lft)
 	{	putname(fd, ".", n->rgt->lft, m, "");
 	}
-	fprintf(fd, suff);
+shortcut:
+	fprintf(fd, suff, 0);
 }
 
 void
@@ -2908,7 +3336,11 @@ putremote(FILE *fd, Lextok *n, int m)	/* remote reference */
 			putstmnt(fd, n->lft->lft, m);	/* pid */
 			fprintf(fd, "]");
 		}
-		fprintf(fd, ".%s", n->sym->name);
+		if (ltl_mode)
+		{	fprintf(fd, ":%s", n->sym->name);
+		} else
+		{	fprintf(fd, ".%s", n->sym->name);
+		}
 	} else
 	{	if (Sym_typ(n) < SHORT)
 		{	promoted = 1;