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, 184 insertions, 69 deletions

diff --git a/sys/src/cmd/spin/pangen3.c b/sys/src/cmd/spin/pangen3.c
index 4feb80ab1..d59b455ff 100644
--- a/sys/src/cmd/spin/pangen3.c
+++ b/sys/src/cmd/spin/pangen3.c
@@ -1,22 +1,20 @@
 /***** spin: pangen3.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"
+#include <assert.h>
 
-extern FILE	*th;
-extern int	claimnr, eventmapnr;
+extern FILE	*th, *tc;
+extern int	eventmapnr, old_priority_rules;
 
 typedef struct SRC {
-	short ln, st;	/* linenr, statenr */
+	int ln, st;	/* linenr, statenr */
 	Symbol *fn;	/* filename */
 	struct SRC *nxt;
 } SRC;
@@ -28,16 +26,18 @@ static int	lastfrom;
 static SRC	*frst = (SRC *) 0;
 static SRC	*skip = (SRC *) 0;
 
+extern int	ltl_mode;
+
 extern void	sr_mesg(FILE *, int, int);
 
 static void
 putnr(int n)
 {
 	if (col++ == 8)
-	{	fprintf(th, "\n\t");
+	{	fprintf(tc, "\n\t");	/* was th */
 		col = 1;
 	}
-	fprintf(th, "%3d, ", n);
+	fprintf(tc, "%3d, ", n);	/* was th */
 }
 
 static void
@@ -47,7 +47,7 @@ putfnm(int j, Symbol *s)
 		return;
 
 	if (lastfnm)
-		fprintf(th, "{ %s, %d, %d },\n\t",
+		fprintf(tc, "{ \"%s\", %d, %d },\n\t",	/* was th */
 			lastfnm->name,
 			lastfrom,
 			j-1);
@@ -59,73 +59,118 @@ static void
 putfnm_flush(int j)
 {
 	if (lastfnm)
-		fprintf(th, "{ %s, %d, %d }\n",
+		fprintf(tc, "{ \"%s\", %d, %d }\n",	/* was th */
 			lastfnm->name,
 			lastfrom, j);
 }
 
-void
-putskip(int m)	/* states that need not be reached */
+static SRC *
+newsrc(int m, SRC *n)
 {	SRC *tmp;
-
-	for (tmp = skip; tmp; tmp = tmp->nxt)
-		if (tmp->st == m)
-			return;
 	tmp = (SRC *) emalloc(sizeof(SRC));
-	tmp->st = (short) m;
-	tmp->nxt = skip;
-	skip = tmp;
+	tmp->st  = m;
+	tmp->nxt = n;
+	return tmp;
+}
+
+void
+putskip(int m)	/* states that need not be reached */
+{	SRC *tmp, *lst = (SRC *)0;
+	/* 6.4.0: now an ordered list */
+	for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
+	{	if (tmp->st == m)
+		{	return;
+		}
+		if (tmp->st > m)	/* insert before */
+		{	if (tmp == skip)
+			{	tmp = newsrc(m, skip);
+				skip = tmp;
+			} else
+			{	assert(lst);
+				tmp = newsrc(m, lst->nxt);
+				lst->nxt = tmp;
+			}
+			return;	
+	}	}
+	/* insert at the end */
+	if (lst)
+	{	lst->nxt = newsrc(m, 0);
+	} else	/* empty list */
+	{	skip = newsrc(m, 0);
+	}
 }
 
 void
 unskip(int m)	/* a state that needs to be reached after all */
-{	SRC *tmp, *lst=(SRC *)0;
+{	SRC *tmp, *lst = (SRC *)0;
 
 	for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
-		if (tmp->st == m)
+	{	if (tmp->st == m)
 		{	if (tmp == skip)
 				skip = skip->nxt;
-			else
+			else if (lst)	/* always true, but helps coverity */
 				lst->nxt = tmp->nxt;
 			break;
 		}
+		if (tmp->st > m)
+		{	break;	/* m is not in list */
+	}	}
 }
 
 void
 putsrc(Element *e)	/* match states to source lines */
-{	SRC *tmp;
+{	SRC *tmp, *lst = (SRC *)0;
 	int n, m;
 
 	if (!e || !e->n) return;
 
 	n = e->n->ln;
 	m = e->seqno;
-
-	for (tmp = frst; tmp; tmp = tmp->nxt)
-		if (tmp->st == m)
+	/* 6.4.0: now an ordered list */
+	for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
+	{	if (tmp->st == m)
 		{	if (tmp->ln != n || tmp->fn != e->n->fn)
-			printf("putsrc mismatch %d - %d, file %s\n", n,
+			printf("putsrc mismatch seqno %d, line %d - %d, file %s\n", m, n,
 				tmp->ln, tmp->fn->name);
 			return;
 		}
-	tmp = (SRC *) emalloc(sizeof(SRC));
-	tmp->ln = (short) n;
-	tmp->st = (short) m;
+		if (tmp->st > m) /* insert before */
+		{	if (tmp == frst)
+			{	tmp = newsrc(m, frst);
+				frst = tmp;
+			} else
+			{	assert(lst);
+				tmp = newsrc(m, lst->nxt);
+				lst->nxt = tmp;
+			}
+			tmp->ln = n;
+			tmp->fn = e->n->fn;
+			return;
+	}	}
+	/* insert at the end */
+	tmp = newsrc(m, lst?lst->nxt:0);
+	tmp->ln = n;
 	tmp->fn = e->n->fn;
-	tmp->nxt = frst;
-	frst = tmp;
+	if (lst)
+	{	lst->nxt = tmp;
+	} else
+	{	frst = tmp;
+	}
 }
 
 static void
 dumpskip(int n, int m)
 {	SRC *tmp, *lst;
+	FILE *tz = tc;	/* was th */
 	int j;
 
-	fprintf(th, "uchar reached%d [] = {\n\t", m);
+	fprintf(tz, "uchar reached%d [] = {\n\t", m);
+	tmp = skip;
+	lst = (SRC *) 0;
 	for (j = 0, col = 0; j <= n; j++)
-	{	lst = (SRC *) 0;
-		for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
-			if (tmp->st == j)
+	{	/* find j in the sorted list */
+		for ( ; tmp; lst = tmp, tmp = tmp->nxt)
+		{	if (tmp->st == j)
 			{	putnr(1);
 				if (lst)
 					lst->nxt = tmp->nxt;
@@ -133,12 +178,17 @@ dumpskip(int n, int m)
 					skip = tmp->nxt;
 				break;
 			}
+			if (tmp->st > j)
+			{	putnr(0);
+				break;	/* j is not in the list */
+		}	}
+
 		if (!tmp)
-			putnr(0);
-	}
-	fprintf(th, "};\n");
-	if (m == claimnr)
-		fprintf(th, "#define reached_claim	reached%d\n", m);
+		{	putnr(0);
+	}	}
+	fprintf(tz, "};\n");
+	fprintf(tz, "uchar *loopstate%d;\n", m);
+
 	if (m == eventmapnr)
 		fprintf(th, "#define reached_event	reached%d\n", m);
 
@@ -149,27 +199,34 @@ void
 dumpsrc(int n, int m)
 {	SRC *tmp, *lst;
 	int j;
+	static int did_claim = 0;
+	FILE *tz = tc;	/* was th */
 
-	fprintf(th, "short src_ln%d [] = {\n\t", m);
+	fprintf(tz, "\nshort src_ln%d [] = {\n\t", m);
+	tmp = frst;
 	for (j = 0, col = 0; j <= n; j++)
-	{	lst = (SRC *) 0;
-		for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
-			if (tmp->st == j)
+	{	for ( ; tmp; tmp = tmp->nxt)
+		{	if (tmp->st == j)
 			{	putnr(tmp->ln);
 				break;
 			}
+			if (tmp->st > j)
+			{	putnr(0);
+				break;
+		}	}
 		if (!tmp)
-			putnr(0);
-	}
-	fprintf(th, "};\n");
+		{	putnr(0);
+	}	}
+	fprintf(tz, "};\n");
 
 	lastfnm = (Symbol *) 0;
-	lastdef.name = "\"-\"";
-	fprintf(th, "S_F_MAP src_file%d [] = {\n\t", m);
+	lastdef.name = "-";
+	fprintf(tz, "S_F_MAP src_file%d [] = {\n\t", m);
+	tmp = frst;
+	lst = (SRC *) 0;
 	for (j = 0, col = 0; j <= n; j++)
-	{	lst = (SRC *) 0;
-		for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
-			if (tmp->st == j)
+	{	for ( ; tmp; lst = tmp, tmp = tmp->nxt)
+		{	if (tmp->st == j)
 			{	putfnm(j, tmp->fn);
 				if (lst)
 					lst->nxt = tmp->nxt;
@@ -177,14 +234,20 @@ dumpsrc(int n, int m)
 					frst = tmp->nxt;
 				break;
 			}
+			if (tmp->st > j)
+			{	putfnm(j, &lastdef);
+				break;
+		}	}
 		if (!tmp)
-			putfnm(j, &lastdef);
-	}
+		{	putfnm(j, &lastdef);
+	}	}
 	putfnm_flush(j);
-	fprintf(th, "};\n");
+	fprintf(tz, "};\n");
 
-	if (m == claimnr)
-		fprintf(th, "#define src_claim	src_ln%d\n", m);
+	if (pid_is_claim(m) && !did_claim)
+	{	fprintf(tz, "short *src_claim;\n");
+		did_claim++;
+	}
 	if (m == eventmapnr)
 		fprintf(th, "#define src_event	src_ln%d\n", m);
 
@@ -237,7 +300,27 @@ comwork(FILE *fd, Lextok *now, int m)
 	case GT:	Cat1(">"); break;
 	case LT:	Cat1("<"); break;
 	case NE:	Cat1("!="); break;
-	case EQ:	Cat1("=="); break;
+	case EQ:
+			if (ltl_mode
+			&&  now->lft->ntyp == 'p'
+			&&  now->rgt->ntyp == 'q')	/* remote ref */
+			{	Lextok *p = now->lft->lft;
+
+				fprintf(fd, "(");
+				fprintf(fd, "%s", p->sym->name);
+				if (p->lft)
+				{	fprintf(fd, "[");
+					putstmnt(fd, p->lft, 0); /* pid */
+					fprintf(fd, "]");
+				}
+				fprintf(fd, "@");
+				fprintf(fd, "%s", now->rgt->sym->name);
+				fprintf(fd, ")");
+				break;
+			}
+			Cat1("==");
+			break;
+
 	case OR:	Cat1("||"); break;
 	case AND:	Cat1("&&"); break;
 	case LSHIFT:	Cat1("<<"); break;
@@ -298,6 +381,22 @@ comwork(FILE *fd, Lextok *now, int m)
 	case ENABLED:	Cat3("enabled(", 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, "set_priority(");
+				comwork(fd, now->lft->lft, m);
+				fprintf(fd, ", ");
+				comwork(fd, now->lft->rgt, m);
+				fprintf(fd, ")");
+			}
+			break;
+
 	case EVAL:	Cat3("eval(", now->lft, ")");
 			break;
 
@@ -320,12 +419,14 @@ comwork(FILE *fd, Lextok *now, int m)
 			}
 			break;	
 
-	case ASGN:	comwork(fd,now->lft,m);
+	case ASGN:
+			if (check_track(now) == STRUCT) { break; }
+			comwork(fd,now->lft,m);
 			fprintf(fd," = ");
 			comwork(fd,now->rgt,m);
 			break;
 
-	case PRINT:	{	char c, buf[512];
+	case PRINT:	{	char c, buf[1024];
 				strncpy(buf, now->sym->name, 510);
 				for (i = j = 0; i < 510; i++, j++)
 				{	c = now->sym->name[i];
@@ -349,9 +450,23 @@ comwork(FILE *fd, Lextok *now, int m)
 			comwork(fd, now->lft, m);
 			fprintf(fd, ")");
 			break;
-	case NAME:	putname(fd, "", now, m, "");
+	case NAME:
+			putname(fd, "", now, m, "");
 			break;
-	case   'p':	putremote(fd, now, m);
+
+	case   'p':
+			if (ltl_mode)
+			{	fprintf(fd, "%s", now->lft->sym->name); /* proctype */
+				if (now->lft->lft)
+				{	fprintf(fd, "[");
+					putstmnt(fd, now->lft->lft, 0); /* pid */
+					fprintf(fd, "]");
+				}
+				fprintf(fd, ":");	/* remote varref */
+				fprintf(fd, "%s", now->sym->name);	/* varname */
+				break;
+			}
+			putremote(fd, now, m);
 			break;
 	case   'q':	fprintf(fd, "%s", now->sym->name);
 			break;
@@ -366,7 +481,7 @@ comwork(FILE *fd, Lextok *now, int m)
 	case  ELSE:	fprintf(fd, "else"); break;
 	case   '@':	fprintf(fd, "-end-"); break;
 
-	case D_STEP:	fprintf(fd, "D_STEP"); break;
+	case D_STEP:	fprintf(fd, "D_STEP%d", now->ln); break;
 	case ATOMIC:	fprintf(fd, "ATOMIC"); break;
 	case NON_ATOMIC: fprintf(fd, "sub-sequence"); break;
 	case IF:	fprintf(fd, "IF"); break;