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, 218 insertions, 78 deletions

diff --git a/sys/src/cmd/spin/sched.c b/sys/src/cmd/spin/sched.c
index ee5b87403..d32e3f175 100644
--- a/sys/src/cmd/spin/sched.c
+++ b/sys/src/cmd/spin/sched.c
@@ -1,13 +1,10 @@
 /***** spin: sched.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 <stdlib.h>
 #include "spin.h"
@@ -19,19 +16,21 @@ extern Ordered	*all_names;
 extern Symbol	*Fname, *context;
 extern int	lineno, nr_errs, dumptab, xspin, jumpsteps, columns;
 extern int	u_sync, Elcnt, interactive, TstOnly, cutoff;
-extern short	has_enabled;
-extern int	limited_vis;
+extern short	has_enabled, has_priority, has_code, replay;
+extern int	limited_vis, product, nclaims, old_priority_rules;
+extern int	old_scope_rules, scope_seq[128], scope_level, has_stdin;
+
+extern int	pc_highest(Lextok *n);
 
 RunList		*X   = (RunList  *) 0;
 RunList		*run = (RunList  *) 0;
 RunList		*LastX  = (RunList  *) 0; /* previous executing proc */
 ProcList	*rdy = (ProcList *) 0;
 Element		*LastStep = ZE;
-int		nproc=0, nstop=0, Tval=0;
+int		nproc=0, nstop=0, Tval=0, Priority_Sum = 0;
 int		Rvous=0, depth=0, nrRdy=0, MadeChoice;
 short		Have_claim=0, Skip_claim=0;
 
-static int	Priority_Sum = 0;
 static void	setlocals(RunList *);
 static void	setparams(RunList *, ProcList *, Lextok *);
 static void	talk(RunList *);
@@ -42,13 +41,20 @@ runnable(ProcList *p, int weight, int noparams)
 
 	r->n  = p->n;
 	r->tn = p->tn;
+	r->b  = p->b;
 	r->pid = nproc++ - nstop + Skip_claim;
+	r->priority = weight;
+	p->priority = (unsigned char) weight; /* not quite the best place of course */
 
-	if ((verbose&4) || (verbose&32))
-		printf("Starting %s with pid %d\n", p->n->name, r->pid);
-
+	if (!noparams && ((verbose&4) || (verbose&32)))
+	{	printf("Starting %s with pid %d",
+			p->n?p->n->name:"--", r->pid);
+		if (has_priority) printf(" priority %d", r->priority);
+		printf("\n");
+	}
 	if (!p->s)
-		fatal("parsing error, no sequence %s", p->n?p->n->name:"--");
+		fatal("parsing error, no sequence %s",
+			p->n?p->n->name:"--");
 
 	r->pc = huntele(p->s->frst, p->s->frst->status, -1);
 	r->ps = p->s;
@@ -58,14 +64,18 @@ runnable(ProcList *p, int weight, int noparams)
 
 	r->nxt = run;
 	r->prov = p->prov;
-	r->priority = weight;
+	if (weight < 1 || weight > 255)
+	{	fatal("bad process priority, valid range: 1..255", (char *) 0);
+	}
+
 	if (noparams) setlocals(r);
 	Priority_Sum += weight;
+
 	run = r;
 }
 
 ProcList *
-ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov)
+ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov, enum btypes b)
 	/* n=name, p=formals, s=body det=deterministic prov=provided */
 {	ProcList *r = (ProcList *) emalloc(sizeof(ProcList));
 	Lextok *fp, *fpt; int j; extern int Npars;
@@ -73,9 +83,15 @@ ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov)
 	r->n = n;
 	r->p = p;
 	r->s = s;
+	r->b = b;
 	r->prov = prov;
-	r->tn = nrRdy++;
-	r->det = (short) det;
+	r->tn = (short) nrRdy++;
+	n->sc = scope_seq[scope_level];	/* scope_level should be 0 */
+
+	if (det != 0 && det != 1)
+	{	fprintf(stderr, "spin: bad value for det (cannot happen)\n");
+	}
+	r->det = (unsigned char) det;
 	r->nxt = rdy;
 	rdy = r;
 
@@ -128,13 +144,15 @@ announce(char *w)
 			run->pid - Have_claim, run->n->name);
 			pstext(run->pid - Have_claim, Buf);
 		} else
-			printf("proc %d = %s\n",
-			run->pid - Have_claim, run->n->name);
+		{	printf("proc %d = %s\n",
+				run->pid - Have_claim, run->n->name);
+		}
 		return;
 	}
 
 	if (dumptab
 	||  analyze
+	||  product
 	||  s_trail
 	|| !(verbose&4))
 		return;
@@ -161,9 +179,11 @@ enable(Lextok *m)
 	Symbol *s = m->sym;	/* proctype name */
 	Lextok *n = m->lft;	/* actual parameters */
 
-	if (m->val < 1) m->val = 1;	/* minimum priority */
+	if (m->val < 1)
+	{	m->val = 1;	/* minimum priority */
+	}
 	for (p = rdy; p; p = p->nxt)
-		if (strcmp(s->name, p->n->name) == 0)
+	{	if (strcmp(s->name, p->n->name) == 0)
 		{	if (nproc-nstop >= MAXP)
 			{	printf("spin: too many processes (%d max)\n", MAXP);
 				break;
@@ -173,7 +193,7 @@ enable(Lextok *m)
 			setparams(run, p, n);
 			setlocals(run); /* after setparams */
 			return run->pid - Have_claim + Skip_claim; /* effective simu pid */
-		}
+	}	}
 	return 0; /* process not found */
 }
 
@@ -208,26 +228,29 @@ start_claim(int n)
 	RunList  *r, *q = (RunList *) 0;
 
 	for (p = rdy; p; p = p->nxt)
-		if (p->tn == n
-		&&  strcmp(p->n->name, ":never:") == 0)
+		if (p->tn == n && p->b == N_CLAIM)
 		{	runnable(p, 1, 1);
 			goto found;
 		}
-	printf("spin: couldn't find claim (ignored)\n");
+	printf("spin: couldn't find claim %d (ignored)\n", n);
+	if (verbose&32)
+	for (p = rdy; p; p = p->nxt)
+		printf("\t%d = %s\n", p->tn, p->n->name);
+
 	Skip_claim = 1;
 	goto done;
 found:
 	/* move claim to far end of runlist, and reassign it pid 0 */
 	if (columns == 2)
-	{	depth = 0;
-		pstext(0, "0::never:");
+	{	extern char Buf[];
+		depth = 0;
+		sprintf(Buf, "%d:%s", 0, p->n->name);
+		pstext(0, Buf);
 		for (r = run; r; r = r->nxt)
-		{	if (!strcmp(r->n->name, ":never:"))
-				continue;
-			sprintf(Buf, "%d:%s",
-				r->pid+1, r->n->name);
-			pstext(r->pid+1, Buf);
-	}	}
+		{	if (r->b != N_CLAIM)
+			{	sprintf(Buf, "%d:%s", r->pid+1, r->n->name);
+				pstext(r->pid+1, Buf);
+	}	}	}
 
 	if (run->pid == 0) return; /* it is the first process started */
 
@@ -288,7 +311,7 @@ wrapup(int fini)
 		nproc - Have_claim + Skip_claim,
 		(xspin || nproc!=1)?"es":"");
 short_cut:
-	if (xspin) alldone(0);	/* avoid an abort from xspin */
+	if (s_trail || xspin) alldone(0);	/* avoid an abort from xspin */
 	if (fini)  alldone(1);
 }
 
@@ -332,6 +355,24 @@ silent_moves(Element *e)
 	return e;
 }
 
+static int
+x_can_run(void)	/* the currently selected process in X can run */
+{
+	if (X->prov && !eval(X->prov))
+	{
+if (0) printf("pid %d cannot run: not provided\n", X->pid);
+		return 0;
+	}
+	if (has_priority && !old_priority_rules)
+	{	Lextok *n = nn(ZN, CONST, ZN, ZN);
+		n->val = X->pid;
+if (0) printf("pid %d %s run (priority)\n", X->pid, pc_highest(n)?"can":"cannot");
+		return pc_highest(n);
+	}
+if (0) printf("pid %d can run\n", X->pid);
+	return 1;
+}
+
 static RunList *
 pickproc(RunList *Y)
 {	SeqList *z; Element *has_else;
@@ -343,7 +384,25 @@ pickproc(RunList *Y)
 		return NULL;
 	}
 	if (!interactive || depth < jumpsteps)
-	{	/* was: j = (int) Rand()%(nproc-nstop); */
+	{	if (has_priority && !old_priority_rules)	/* new 6.3.2 */
+		{	j = Rand()%(nproc-nstop);
+			for (X = run; X; X = X->nxt)
+			{	if (j-- <= 0)
+					break;
+			}
+			if (X == NULL)
+			{	fatal("unexpected, pickproc", (char *)0);
+			}
+			j = nproc - nstop;
+			while (j-- > 0)
+			{	if (x_can_run())
+				{	Y = X;
+					break;
+				}
+				X = (X->nxt)?X->nxt:run;
+			}
+			return Y;
+		}
 		if (Priority_Sum < nproc-nstop)
 			fatal("cannot happen - weights", (char *)0);
 		j = (int) Rand()%Priority_Sum;
@@ -354,6 +413,7 @@ pickproc(RunList *Y)
 			X = X->nxt;
 			if (!X) { Y = NULL; X = run; }
 		}
+
 	} else
 	{	int only_choice = -1;
 		int no_choice = 0, proc_no_ch, proc_k;
@@ -365,8 +425,7 @@ try_more:	for (X = run, k = 1; X; X = X->nxt)
 
 			Choices[X->pid] = (short) k;
 
-			if (!X->pc
-			||  (X->prov && !eval(X->prov)))
+			if (!X->pc || !x_can_run())
 			{	if (X == run)
 					Choices[X->pid] = 0;
 				continue;
@@ -457,9 +516,12 @@ try_more:	for (X = run, k = 1; X; X = X->nxt)
 		} else
 		{	char buf[256];
 			fflush(stdout);
-			scanf("%s", buf);
+			if (scanf("%64s", buf) == 0)
+			{	printf("\tno input\n");
+				goto try_again;
+			}
 			j = -1;
-			if (isdigit(buf[0]))
+			if (isdigit((int) buf[0]))
 				j = atoi(buf);
 			else
 			{	if (buf[0] == 'q')
@@ -484,6 +546,26 @@ try_more:	for (X = run, k = 1; X; X = X->nxt)
 }
 
 void
+multi_claims(void)
+{	ProcList *p, *q = NULL;
+
+	if (nclaims > 1)
+	{	printf("  the model contains %d never claims:", nclaims);
+		for (p = rdy; p; p = p->nxt)
+		{	if (p->b == N_CLAIM)
+			{	printf("%s%s", q?", ":" ", p->n->name);
+				q = p;
+		}	}
+		printf("\n");
+		printf("  only one claim is used in a verification run\n");
+		printf("  choose which one with ./pan -a -N name (defaults to -N %s)\n",
+			q?q->n->name:"--");
+		printf("  or use e.g.: spin -search -ltl %s %s\n",
+			q?q->n->name:"--", Fname?Fname->name:"filename");
+	}
+}
+
+void
 sched(void)
 {	Element *e;
 	RunList *Y = NULL;	/* previous process in run queue */
@@ -498,19 +580,33 @@ sched(void)
 		dumplabels();
 		return;
 	}
+	if (has_code && !analyze)
+	{	printf("spin: warning: c_code fragments remain uninterpreted\n");
+		printf("      in random simulations with spin; use ./pan -r instead\n");
+	}
 
 	if (has_enabled && u_sync > 0)
 	{	printf("spin: error, cannot use 'enabled()' in ");
 		printf("models with synchronous channels.\n");
 		nr_errs++;
 	}
-	if (analyze)
+	if (product)
+	{	sync_product();
+		alldone(0);
+	}
+	if (analyze && (!replay || has_code))
 	{	gensrc();
+		multi_claims();
 		return;
-	} else if (s_trail)
+	}
+	if (replay && !has_code)
+	{	return;
+	}
+	if (s_trail)
 	{	match_trail();
 		return;
 	}
+
 	if (claimproc)
 	printf("warning: never claim not used in random simulation\n");
 	if (eventmap)
@@ -543,9 +639,9 @@ sched(void)
 		depth++; LastStep = ZE;
 		oX = X;	/* a rendezvous could change it */
 		go = 1;
-		if (X && X->prov && X->pc
+		if (X->pc
 		&& !(X->pc->status & D_ATOM)
-		&& !eval(X->prov))
+		&& !x_can_run())
 		{	if (!xspin && ((verbose&32) || (verbose&4)))
 			{	p_talk(X->pc, 1);
 				printf("\t<<Not Enabled>>\n");
@@ -557,9 +653,10 @@ sched(void)
 			&& ((verbose&32) || (verbose&4)))
 			{	if (X == oX)
 				if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */
-				{	p_talk(X->pc, 1);
+				{	if (!LastStep) LastStep = X->pc;
+					/* A. Tanaka, changed order */
+					p_talk(LastStep, 1);
 					printf("	[");
-					if (!LastStep) LastStep = X->pc;
 					comment(stdout, LastStep->n, 0);
 					printf("]\n");
 				}
@@ -570,7 +667,8 @@ sched(void)
 				if (xspin)
 					printf("\n");
 			}
-			if (oX != X)
+			if (oX != X
+			||  (X->pc->status & (ATOM|D_ATOM)))		/* new 5.0 */
 			{	e = silent_moves(e);
 				notbeyond = 0;
 			}
@@ -587,10 +685,12 @@ sched(void)
 			}
 		} else
 		{	depth--;
-			if (oX->pc->status & D_ATOM)
-			 non_fatal("stmnt in d_step blocks", (char *)0);
-
-			if (X->pc->n->ntyp == '@'
+			if (oX->pc && (oX->pc->status & D_ATOM))
+			{	non_fatal("stmnt in d_step blocks", (char *)0);
+			}
+			if (X->pc
+			&&  X->pc->n
+			&&  X->pc->n->ntyp == '@'
 			&&  X->pid == (nproc-nstop-1))
 			{	if (X != run && Y != NULL)
 					Y->nxt = X->nxt;
@@ -610,14 +710,19 @@ sched(void)
 				X = (X->nxt) ? X->nxt : run;
 			} else
 			{	if (p_blocked(X->pid))
-				{	if (Tval) break;
-					Tval = 1;
-					if (depth >= jumpsteps)
+				{	if (Tval && !has_stdin)
+					{	break;
+					}
+					if (!Tval && depth >= jumpsteps)
 					{	oX = X;
 						X = (RunList *) 0; /* to suppress indent */
 						dotag(stdout, "timeout\n");
 						X = oX;
+						Tval = 1;
 		}	}	}	}
+
+		if (!run || !X) break;	/* new 5.0 */
+
 		Y = pickproc(X);
 		notbeyond = 0;
 	}
@@ -662,7 +767,7 @@ complete_rendez(void)
 				printf("	[");
 				comment(stdout, s_was->n, 0);
 				printf("]\n");
-				tmp = orun; orun = X; X = tmp;
+				tmp = orun; /* orun = X; */ X = tmp;
 				if (!LastStep) LastStep = X->pc;
 				p_talk(LastStep, 1);
 				printf("	[");
@@ -692,25 +797,33 @@ addsymbol(RunList *r, Symbol  *s)
 	int i;
 
 	for (t = r->symtab; t; t = t->next)
-		if (strcmp(t->name, s->name) == 0)
+		if (strcmp(t->name, s->name) == 0
+		&& (old_scope_rules
+		 || strcmp((const char *)t->bscp, (const char *)s->bscp) == 0))
 			return;		/* it's already there */
 
 	t = (Symbol *) emalloc(sizeof(Symbol));
 	t->name = s->name;
 	t->type = s->type;
 	t->hidden = s->hidden;
+	t->isarray = s->isarray;
 	t->nbits  = s->nbits;
 	t->nel  = s->nel;
 	t->ini  = s->ini;
 	t->setat = depth;
 	t->context = r->n;
+
+	t->bscp  = (unsigned char *) emalloc(strlen((const char *)s->bscp)+1);
+	strcpy((char *)t->bscp, (const char *)s->bscp);
+
 	if (s->type != STRUCT)
 	{	if (s->val)	/* if already initialized, copy info */
 		{	t->val = (int *) emalloc(s->nel*sizeof(int));
 			for (i = 0; i < s->nel; i++)
 				t->val[i] = s->val[i];
 		} else
-			(void) checkvar(t, 0);	/* initialize it */
+		{	(void) checkvar(t, 0);	/* initialize it */
+		}
 	} else
 	{	if (s->Sval)
 			fatal("saw preinitialized struct %s", s->name);
@@ -759,7 +872,7 @@ oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p)
 
 	if (!a)
 		fatal("missing actual parameters: '%s'", p->n->name);
-	if (t->sym->nel != 1)
+	if (t->sym->nel > 1 || t->sym->isarray)
 		fatal("array in parameter list, %s", t->sym->name);
 	k = eval(a->lft);
 
@@ -768,7 +881,7 @@ oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p)
 	ft = Sym_typ(t);
 
 	if (at != ft && (at == CHAN || ft == CHAN))
-	{	char buf[128], tag1[64], tag2[64];
+	{	char buf[256], tag1[64], tag2[64];
 		(void) sputtype(tag1, ft);
 		(void) sputtype(tag2, at);
 		sprintf(buf, "type-clash in params of %s(..), (%s<-> %s)",
@@ -809,8 +922,11 @@ findloc(Symbol *s)
 		return ZS;
 	}
 	for (r = X->symtab; r; r = r->next)
-		if (strcmp(r->name, s->name) == 0)
-			break;
+	{	if (strcmp(r->name, s->name) == 0
+		&& (old_scope_rules
+		 || strcmp((const char *)r->bscp, (const char *)s->bscp) == 0))
+		{	break;
+	}	}
 	if (!r)
 	{	addsymbol(X, s);
 		r = X->symtab;
@@ -878,7 +994,11 @@ whoruns(int lnr)
 		printf(" -");
 	else
 		printf("%2d", X->pid - Have_claim);
-	printf(" (%s) ", X->n->name);
+	if (old_priority_rules)
+	{	printf(" (%s) ", X->n->name);
+	} else
+	{	printf(" (%s:%d) ", X->n->name, X->priority);
+	}
 }
 
 static void
@@ -895,6 +1015,7 @@ talk(RunList *r)
 void
 p_talk(Element *e, int lnr)
 {	static int lastnever = -1;
+	static char nbuf[128];
 	int newnever = -1;
 
 	if (e && e->n)
@@ -918,9 +1039,22 @@ p_talk(Element *e, int lnr)
 
 	whoruns(lnr);
 	if (e)
-	{	printf("line %3d %s (state %d)",
+	{	if (e->n)
+		{	char *ptr = e->n->fn->name;
+			char *qtr = nbuf;
+			while (*ptr != '\0')
+			{	if (*ptr != '"')
+				{	*qtr++ = *ptr;
+				}
+				ptr++;
+			}
+			*qtr = '\0';
+		} else
+		{	strcpy(nbuf, "-");
+		}
+		printf("%s:%d (state %d)",
+			nbuf,
 			e->n?e->n->ln:-1,
-			e->n?e->n->fn->name:"-",
 			e->seqno);
 		if (!xspin
 		&&  ((e->status&ENDSTATE) || has_lab(e, 2)))	/* 2=end */
@@ -943,8 +1077,9 @@ remotelab(Lextok *n)
 	{	fatal("remote ref to label '%s' inside d_step",
 			n->sym->name);
 	}
-	if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0)
-		fatal("unknown labelname: %s", n->sym->name);
+	if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0)	/* remotelab */
+	{	fatal("unknown labelname: %s", n->sym->name);
+	}
 	return i;
 }
 
@@ -970,7 +1105,8 @@ remotevar(Lextok *n)
 	}	}
 
 	if (prno < 0)
-		return 0;	/* non-existing process */
+	{	return 0;	/* non-existing process */
+	}
 #if 0
 	i = nproc - nstop;
 	for (Y = run; Y; Y = Y->nxt)
@@ -978,7 +1114,7 @@ remotevar(Lextok *n)
 		printf("	%s: i=%d, prno=%d, ->pid=%d\n", Y->n->name, i, prno, Y->pid);
 	}
 #endif
-	i = nproc - nstop;
+	i = nproc - nstop + Skip_claim;	/* 6.0: added Skip_claim */
 	for (Y = run; Y; Y = Y->nxt)
 	if (--i == prno)
 	{	if (strcmp(Y->n->name, n->lft->sym->name) != 0)
@@ -988,12 +1124,13 @@ remotevar(Lextok *n)
 		}
 		if (strcmp(n->sym->name, "_p") == 0)
 		{	if (Y->pc)
-				return Y->pc->seqno;
+			{	return Y->pc->seqno;
+			}
 			/* harmless, can only happen with -t */
 			return 0;
 		}
-#if 1
-		/* new 4.0 allow remote variables */
+
+		/* check remote variables */
 		oX = X;
 		X = Y;
 
@@ -1001,17 +1138,20 @@ remotevar(Lextok *n)
 		n->lft = n->rgt;
 
 		os = n->sym;
-		n->sym = findloc(n->sym);
-
+		if (!n->sym->context)
+		{	n->sym->context = Y->n;
+		}
+		{ int rs = old_scope_rules;
+		  old_scope_rules = 1; /* 6.4.0 */
+		  n->sym = findloc(n->sym);
+		  old_scope_rules = rs;
+		}
 		i = getval(n);
 
 		n->sym = os;
 		n->lft = onl;
 		X = oX;
 		return i;
-#else
-		break;
-#endif
 	}
 	printf("remote ref: %s[%d] ", n->lft->sym->name, prno-added);
 	non_fatal("%s not found", n->sym->name);