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, 229 insertions, 37 deletions

diff --git a/sys/src/cmd/spin/mesg.c b/sys/src/cmd/spin/mesg.c
index 4b2806b40..74e1fe33a 100644
--- a/sys/src/cmd/spin/mesg.c
+++ b/sys/src/cmd/spin/mesg.c
@@ -1,14 +1,12 @@
 /***** spin: mesg.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"
 #include "y.tab.h"
 
@@ -24,9 +22,10 @@ extern int	lineno, depth, xspin, m_loss, jumpsteps;
 extern int	nproc, nstop;
 extern short	Have_claim;
 
+QH	*qh;
 Queue	*qtab = (Queue *) 0;	/* linked list of queues */
 Queue	*ltab[MAXQ];		/* linear list of queues */
-int	nqs = 0, firstrow = 1;
+int	nqs = 0, firstrow = 1, has_stdin = 0;
 char	Buf[4096];
 
 static Lextok	*n_rem = (Lextok *) 0;
@@ -73,7 +72,7 @@ qmake(Symbol *s)
 		return eval(s->ini);
 
 	q = (Queue *) emalloc(sizeof(Queue));
-	q->qid    = ++nqs;
+	q->qid    = (short) ++nqs;
 	q->nslots = s->ini->val;
 	q->nflds  = cnt_mpars(s->ini->rgt);
 	q->setat  = depth;
@@ -130,7 +129,7 @@ qsend(Lextok *n)
 
 	if (whichq == -1)
 	{	printf("Error: sending to an uninitialized chan\n");
-		whichq = 0;
+		/* whichq = 0; */
 		return 0;
 	}
 	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
@@ -143,6 +142,37 @@ qsend(Lextok *n)
 	return 0;
 }
 
+#ifndef PC
+ #include <termios.h>
+ static struct termios initial_settings, new_settings;
+
+ void
+ peek_ch_init(void)
+ {
+	tcgetattr(0,&initial_settings);
+ 
+	new_settings = initial_settings;
+	new_settings.c_lflag &= ~ICANON;
+	new_settings.c_lflag &= ~ECHO;
+	new_settings.c_lflag &= ~ISIG;
+	new_settings.c_cc[VMIN] = 0;
+	new_settings.c_cc[VTIME] = 0;
+ }
+
+ int
+ peek_ch(void)
+ {	int n;
+
+	has_stdin = 1;
+
+	tcsetattr(0, TCSANOW, &new_settings);
+	n = getchar();
+	tcsetattr(0, TCSANOW, &initial_settings);
+
+	return n;
+ }
+#endif
+
 int
 qrecv(Lextok *n, int full)
 {	int whichq = eval(n->lft)-1;
@@ -150,22 +180,37 @@ qrecv(Lextok *n, int full)
 	if (whichq == -1)
 	{	if (n->sym && !strcmp(n->sym->name, "STDIN"))
 		{	Lextok *m;
-
+#ifndef PC
+			static int did_once = 0;
+			if (!did_once) /* 6.2.4 */
+			{	peek_ch_init();
+				did_once = 1;
+			}
+#endif
 			if (TstOnly) return 1;
 
 			for (m = n->rgt; m; m = m->rgt)
 			if (m->lft->ntyp != CONST && m->lft->ntyp != EVAL)
-			{	int c = getchar();
+			{
+#ifdef PC
+				int c = getchar();
+#else
+				int c = peek_ch();	/* 6.2.4, was getchar(); */
+#endif
+				if (c == 27 || c == 3)	/* escape or control-c */
+				{	printf("quit\n");
+					exit(0);
+				} /* else: non-blocking */
+				if (c == EOF) return 0;	/* no char available */
 				(void) setval(m->lft, c);
 			} else
-				fatal("invalid use of STDIN", (char *)0);
-
-			whichq = 0;
+			{	fatal("invalid use of STDIN", (char *)0);
+			}
 			return 1;
 		}
 		printf("Error: receiving from an uninitialized chan %s\n",
 			n->sym?n->sym->name:"");
-		whichq = 0;
+		/* whichq = 0; */
 		return 0;
 	}
 	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
@@ -185,9 +230,11 @@ sa_snd(Queue *q, Lextok *n)	/* sorted asynchronous */
 	for (j = 0, m = n->rgt; m && j < q->nflds; m = m->rgt, j++)
 	{	New = cast_val(q->fld_width[j], eval(m->lft), 0);
 		Old = q->contents[i*q->nflds+j];
-		if (New == Old) continue;
-		if (New >  Old) break;			/* inner loop */
-		if (New <  Old) goto found;
+		if (New == Old)
+			continue;
+		if (New >  Old)
+			break;	/* inner loop */
+		goto found;	/* New < Old */
 	}
 found:
 	for (j = q->qlen-1; j >= i; j--)
@@ -204,7 +251,8 @@ void
 typ_ck(int ft, int at, char *s)
 {
 	if ((verbose&32) && ft != at
-	&& (ft == CHAN || at == CHAN))
+	&& (ft == CHAN || at == CHAN)
+	&& (at != PREDEF || strcmp(s, "recv") != 0))
 	{	char buf[128], tag1[64], tag2[64];
 		(void) sputtype(tag1, ft);
 		(void) sputtype(tag2, at);
@@ -383,7 +431,7 @@ s_snd(Queue *q, Lextok *n)
 	return 1;
 }
 
-void
+static void
 channm(Lextok *n)
 {	char lbuf[512];
 
@@ -394,7 +442,11 @@ channm(Lextok *n)
 	else if (n->sym->type == STRUCT)
 	{	Symbol *r = n->sym;
 		if (r->context)
-			r = findloc(r);
+		{	r = findloc(r);
+			if (!r)
+			{	strcat(Buf, "*?*");
+				return;
+		}	}
 		ini_struct(r);
 		printf("%s", r->name);
 		strcpy(lbuf, "");
@@ -422,7 +474,11 @@ difcolumns(Lextok *n, char *tr, int v, int j, Queue *q)
 	sr_buf(v, q->fld_width[j] == MTYPE);
 	if (j == q->nflds - 1)
 	{	int cnr;
-		if (s_trail) cnr = pno; else cnr = X?X->pid - Have_claim:0;
+		if (s_trail)
+		{	cnr = pno;
+		} else
+		{	cnr = X?X->pid - Have_claim:0;
+		}
 		if (tr[0] == '[') strcat(Buf, "]");
 		pstext(cnr, Buf);
 	}
@@ -458,12 +514,6 @@ docolumns(Lextok *n, char *tr, int v, int j, Queue *q)
 	}
 }
 
-typedef struct QH {
-	int	n;
-	struct	QH *nxt;
-} QH;
-QH *qh;
-
 void
 qhide(int q)
 {	QH *p = (QH *) emalloc(sizeof(QH));
@@ -483,7 +533,7 @@ qishidden(int q)
 
 static void
 sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q)
-{	char s[64];
+{	char s[128];
 
 	if (qishidden(eval(n->lft)))
 		return;
@@ -510,9 +560,20 @@ sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q)
 	}
 
 	if (j == 0)
-	{	whoruns(1);
-		printf("line %3d %s %s",
-			n->ln, n->fn->name, s);
+	{	char snm[128];
+		whoruns(1);
+		{	char *ptr = n->fn->name;
+			char *qtr = snm;
+			while (*ptr != '\0')
+			{	if (*ptr != '\"')
+				{	*qtr++ = *ptr;
+				}
+				ptr++;
+			}
+			*qtr = '\0';
+			printf("%s:%d %s",
+				snm, n->ln, s);
+		}
 	} else
 		printf(",");
 	sr_mesg(stdout, v, q->fld_width[j] == MTYPE);
@@ -554,7 +615,11 @@ void
 sr_mesg(FILE *fd, int v, int j)
 {	Buf[0] ='\0';
 	sr_buf(v, j);
+#if 1
+	fprintf(fd, Buf, (char *) 0); /* prevent compiler warning */
+#else
 	fprintf(fd, Buf);
+#endif
 }
 
 void
@@ -572,10 +637,15 @@ doq(Symbol *s, int n, RunList *r)
 			continue;
 		if (q->nslots == 0)
 			continue; /* rv q always empty */
+#if 0
+		if (q->qlen == 0)	/* new 7/10 -- dont show if queue is empty */
+		{	continue;
+		}
+#endif
 		printf("\t\tqueue %d (", q->qid);
 		if (r)
 		printf("%s(%d):", r->n->name, r->pid - Have_claim);
-		if (s->nel != 1)
+		if (s->nel > 1 || s->isarray)
 		  printf("%s[%d]): ", s->name, n);
 		else
 		  printf("%s): ", s->name);
@@ -609,7 +679,11 @@ nochan_manip(Lextok *p, Lextok *n, int d)
 		}	
 	}
 
-	if (!n || n->ntyp == LEN || n->ntyp == RUN)
+	/* ok on the rhs of an assignment: */
+	if (!n || n->ntyp == LEN || n->ntyp == RUN
+	||  n->ntyp == FULL  || n->ntyp == NFULL
+	||  n->ntyp == EMPTY || n->ntyp == NEMPTY
+	||  n->ntyp == 'R')
 		return;
 
 	if (n->sym && n->sym->type == CHAN)
@@ -627,6 +701,121 @@ nochan_manip(Lextok *p, Lextok *n, int d)
 	nochan_manip(p, n->rgt, 1);
 }
 
+typedef struct BaseName {
+	char *str;
+	int cnt;
+	struct BaseName *nxt;
+} BaseName;
+
+static BaseName *bsn;
+
+void
+newbasename(char *s)
+{	BaseName *b;
+
+/*	printf("+++++++++%s\n", s);	*/
+	for (b = bsn; b; b = b->nxt)
+		if (strcmp(b->str, s) == 0)
+		{	b->cnt++;
+			return;
+		}
+	b = (BaseName *) emalloc(sizeof(BaseName));
+	b->str = emalloc(strlen(s)+1);
+	b->cnt = 1;
+	strcpy(b->str, s);
+	b->nxt = bsn;
+	bsn = b;
+}
+
+void
+delbasename(char *s)
+{	BaseName *b, *prv = (BaseName *) 0;
+
+	for (b = bsn; b; prv = b, b = b->nxt)
+	{	if (strcmp(b->str, s) == 0)
+		{	b->cnt--;
+			if (b->cnt == 0)
+			{	if (prv)
+				{	prv->nxt = b->nxt;
+				} else
+				{	bsn = b->nxt;
+			}	}
+/*	printf("---------%s\n", s);	*/
+			break;
+	}	}
+}
+
+void
+checkindex(char *s, char *t)
+{	BaseName *b;
+
+/*	printf("xxx Check %s (%s)\n", s, t);	*/
+	for (b = bsn; b; b = b->nxt)
+	{
+/*		printf("	%s\n", b->str);	*/
+		if (strcmp(b->str, s) == 0)
+		{	non_fatal("do not index an array with itself (%s)", t);
+			break;
+	}	}
+}
+
+void
+scan_tree(Lextok *t, char *mn, char *mx)
+{	char sv[512];
+	char tmp[32];
+	int oln = lineno;
+
+	if (!t) return;
+
+	lineno = t->ln;
+
+	if (t->ntyp == NAME)
+	{	strcat(mn, t->sym->name);
+		strcat(mx, t->sym->name);
+		if (t->lft)		/* array index */
+		{	strcat(mn, "[]");
+			newbasename(mn);
+				strcpy(sv, mn);		/* save */
+				strcpy(mn, "");		/* clear */
+				strcat(mx, "[");
+				scan_tree(t->lft, mn, mx);	/* index */
+				strcat(mx, "]");
+				checkindex(mn, mx);	/* match against basenames */
+				strcpy(mn, sv);		/* restore */
+			delbasename(mn);
+		}
+		if (t->rgt)	/* structure element */
+		{	scan_tree(t->rgt, mn, mx);
+		}
+	} else if (t->ntyp == CONST)
+	{	strcat(mn, "1"); /* really: t->val */
+		sprintf(tmp, "%d", t->val);
+		strcat(mx, tmp);
+	} else if (t->ntyp == '.')
+	{	strcat(mn, ".");
+		strcat(mx, ".");
+		scan_tree(t->lft, mn, mx);
+	} else
+	{	strcat(mn, "??");
+		strcat(mx, "??");
+	}
+	lineno = oln;
+}
+
+void
+no_nested_array_refs(Lextok *n)	/* a [ a[1] ] with a[1] = 1, causes trouble in pan.b */
+{	char mn[512];
+	char mx[512];
+
+/*	printf("==================================ZAP\n");	*/
+	bsn = (BaseName *) 0;	/* start new list */
+	strcpy(mn, "");
+	strcpy(mx, "");
+
+	scan_tree(n, mn, mx);
+/*	printf("==> %s\n", mn);	*/
+}
+
 void
 no_internals(Lextok *n)
 {	char *sp;
@@ -638,7 +827,10 @@ no_internals(Lextok *n)
 	sp = n->sym->name;
 
 	if ((strlen(sp) == strlen("_nr_pr") && strcmp(sp, "_nr_pr") == 0)
+	||  (strlen(sp) == strlen("_pid") && strcmp(sp, "_pid") == 0)
 	||  (strlen(sp) == strlen("_p") && strcmp(sp, "_p") == 0))
-	{	fatal("attempt to assign value to system variable %s", sp);
+	{	fatal("invalid assignment to %s", sp);
 	}
+
+	no_nested_array_refs(n);
 }