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, 85 insertions, 35 deletions

diff --git a/sys/src/cmd/spin/vars.c b/sys/src/cmd/spin/vars.c
index e83d74f57..5c73b09f6 100644
--- a/sys/src/cmd/spin/vars.c
+++ b/sys/src/cmd/spin/vars.c
@@ -1,13 +1,10 @@
 /***** spin: vars.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 "y.tab.h"
@@ -17,7 +14,7 @@ extern RunList	*X, *LastX;
 extern Symbol	*Fname;
 extern char	Buf[];
 extern int	lineno, depth, verbose, xspin, limited_vis;
-extern int	analyze, jumpsteps, nproc, nstop, columns;
+extern int	analyze, jumpsteps, nproc, nstop, columns, old_priority_rules;
 extern short	no_arrays, Have_claim;
 extern void	sr_mesg(FILE *, int, int);
 extern void	sr_buf(int, int);
@@ -42,22 +39,54 @@ getval(Lextok *sn)
 	{	if (!X) return 0;
 		return X->pid - Have_claim;
 	}
+	if (strcmp(s->name, "_priority") == 0)
+	{	if (!X) return 0;
+
+		if (old_priority_rules)
+		{	non_fatal("cannot refer to _priority with -o6", (char *) 0);
+			return 1;
+		}
+		return X->priority;
+	}
+
 	if (strcmp(s->name, "_nr_pr") == 0)
-		return nproc-nstop;	/* new 3.3.10 */
+	{	return nproc-nstop;	/* new 3.3.10 */
+	}
 
 	if (s->context && s->type)
-		return getlocal(sn);
+	{	return getlocal(sn);
+	}
 
 	if (!s->type)	/* not declared locally */
 	{	s = lookup(s->name); /* try global */
 		sn->sym = s;	/* fix it */
 	}
+
 	return getglobal(sn);
 }
 
 int
 setval(Lextok *v, int n)
 {
+	if (strcmp(v->sym->name, "_last") == 0
+	||  strcmp(v->sym->name, "_p") == 0
+	||  strcmp(v->sym->name, "_pid") == 0
+	||  strcmp(v->sym->name, "_nr_qs") == 0
+	||  strcmp(v->sym->name, "_nr_pr") == 0)
+	{	non_fatal("illegal assignment to %s", v->sym->name);
+	}
+	if (strcmp(v->sym->name, "_priority") == 0)
+	{	if (old_priority_rules)
+		{	non_fatal("cannot refer to _priority with -o6", (char *) 0);
+			return 1;
+		}
+		if (!X)
+		{	non_fatal("no context for _priority", (char *) 0);
+			return 1;
+		}
+		X->priority = n;
+	}
+
 	if (v->sym->context && v->sym->type)
 		return setlocal(v, n);
 	if (!v->sym->type)
@@ -90,6 +119,7 @@ int
 checkvar(Symbol *s, int n)
 {	int	i, oln = lineno;	/* calls on eval() change it */
 	Symbol	*ofnm = Fname;
+	Lextok  *z, *y;
 
 	if (!in_bound(s, n))
 		return 0;
@@ -101,15 +131,23 @@ checkvar(Symbol *s, int n)
 	/* not a STRUCT */
 	if (s->val == (int *) 0)	/* uninitialized */
 	{	s->val = (int *) emalloc(s->nel*sizeof(int));
+		z = s->ini;
 		for (i = 0; i < s->nel; i++)
-		{	if (s->type != CHAN)
-			{	rm_selfrefs(s, s->ini);
-				s->val[i] = eval(s->ini);
+		{	if (z && z->ntyp == ',')
+			{	y = z->lft;
+				z = z->rgt;
+			} else
+			{	y = z;
+			}
+			if (s->type != CHAN)
+			{	rm_selfrefs(s, y);
+				s->val[i] = eval(y);
 			} else if (!analyze)
-				s->val[i] = qmake(s);
-	}	}
+			{	s->val[i] = qmake(s);
+	}	}	}
 	lineno = oln;
 	Fname  = ofnm;
+
 	return 1;
 }
 
@@ -118,14 +156,16 @@ getglobal(Lextok *sn)
 {	Symbol *s = sn->sym;
 	int i, n = eval(sn->lft);
 
-	if (s->type == 0 && X && (i = find_lab(s, X->n, 0)))
+	if (s->type == 0 && X && (i = find_lab(s, X->n, 0)))	/* getglobal */
 	{	printf("findlab through getglobal on %s\n", s->name);
 		return i;	/* can this happen? */
 	}
 	if (s->type == STRUCT)
-		return Rval_struct(sn, s, 1); /* 1 = check init */
+	{	return Rval_struct(sn, s, 1); /* 1 = check init */
+	}
 	if (checkvar(s, n))
-		return cast_val(s->type, s->val[n], s->nbits);
+	{	return cast_val(s->type, s->val[n], s->nbits);
+	}
 	return 0;
 }
 
@@ -145,23 +185,26 @@ cast_val(int t, int v, int w)
 	}
 
 	if (v != i+s+ (int) u)
-	{	char buf[32]; sprintf(buf, "%d->%d (%d)", v, i+s+u, t);
+	{	char buf[64]; sprintf(buf, "%d->%d (%d)", v, i+s+(int)u, t);
 		non_fatal("value (%s) truncated in assignment", buf);
 	}
-	return (int)(i+s+u);
+	return (int)(i+s+(int)u);
 }
 
 static int
 setglobal(Lextok *v, int m)
 {
 	if (v->sym->type == STRUCT)
-		(void) Lval_struct(v, v->sym, 1, m);
-	else
+	{	(void) Lval_struct(v, v->sym, 1, m);
+	} else
 	{	int n = eval(v->lft);
 		if (checkvar(v->sym, n))
-		{	v->sym->val[n] = cast_val(v->sym->type, m, v->sym->nbits);
-			v->sym->setat = depth;
-	}	}
+		{	int oval = v->sym->val[n];
+			int nval = cast_val(v->sym->type, m, v->sym->nbits);
+			v->sym->val[n] = nval;
+			if (oval != nval)
+			{	v->sym->setat = depth;
+	}	}	}
 	return 1;
 }
 
@@ -215,7 +258,12 @@ dumpglobals(void)
 			continue;
 
 		if (sp->type == STRUCT)
-		{	dump_struct(sp, sp->name, 0);
+		{	if ((verbose&4) && !(verbose&64)
+			&&  (sp->setat < depth
+			&&   jumpsteps != depth))
+			{	continue;
+			}
+			dump_struct(sp, sp->name, 0);
 			continue;
 		}
 		for (j = 0; j < sp->nel; j++)
@@ -227,13 +275,15 @@ dumpglobals(void)
 			if ((verbose&4) && !(verbose&64)
 			&&  (sp->setat < depth
 			&&   jumpsteps != depth))
-				continue;
+			{	continue;
+			}
+
 			dummy->sym = sp;
 			dummy->lft->val = j;
 			/* in case of cast_val warnings, do this first: */
 			prefetch = getglobal(dummy);
 			printf("\t\t%s", sp->name);
-			if (sp->nel > 1) printf("[%d]", j);
+			if (sp->nel > 1 || sp->isarray) printf("[%d]", j);
 			printf(" = ");
 			sr_mesg(stdout, prefetch,
 				sp->type == MTYPE);
@@ -249,7 +299,7 @@ dumpglobals(void)
 				}
 				sr_buf(prefetch, sp->type == MTYPE);
 				if (sp->colnr == 0)
-				{	sp->colnr = maxcolnr;
+				{	sp->colnr = (unsigned char) maxcolnr;
 					maxcolnr = 1+(maxcolnr%10);
 				}
 				colpos = nproc+sp->colnr-1;
@@ -266,7 +316,7 @@ dumpglobals(void)
 					depth, colpos);
 				printf("(state 0)\t[printf('MSC: globvar\\\\n')]\n");
 				printf("\t\t%s", sp->name);
-				if (sp->nel > 1) printf("[%d]", j);
+				if (sp->nel > 1 || sp->isarray) printf("[%d]", j);
 				printf(" = %s\n", Buf);
 	}	}	}
 }
@@ -303,8 +353,8 @@ dumplocal(RunList *r)
 			dummy->lft->val = i;
 
 			printf("\t\t%s(%d):%s",
-				r->n->name, r->pid, z->name);
-			if (z->nel > 1) printf("[%d]", i);
+				r->n->name, r->pid - Have_claim, z->name);
+			if (z->nel > 1 || z->isarray) printf("[%d]", i);
 			printf(" = ");
 			sr_mesg(stdout, getval(dummy), z->type == MTYPE);
 			printf("\n");
@@ -321,7 +371,7 @@ dumplocal(RunList *r)
 				}
 				sr_buf(getval(dummy), z->type==MTYPE);
 				if (z->colnr == 0)
-				{	z->colnr = maxcolnr;
+				{	z->colnr = (unsigned char) maxcolnr;
 					maxcolnr = 1+(maxcolnr%10);
 				}
 				colpos = nproc+z->colnr-1;
@@ -341,7 +391,7 @@ dumplocal(RunList *r)
 				printf("(state 0)\t[printf('MSC: locvar\\\\n')]\n");
 				printf("\t\t%s(%d):%s",
 					r->n->name, r->pid, z->name);
-				if (z->nel > 1) printf("[%d]", i);
+				if (z->nel > 1 || z->isarray) printf("[%d]", i);
 				printf(" = %s\n", Buf);
 	}	}	}
 }