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, 136 insertions, 24 deletions

diff --git a/sys/src/cmd/spin/guided.c b/sys/src/cmd/spin/guided.c
index 0bc4dcbc7..d58e33420 100644
--- a/sys/src/cmd/spin/guided.c
+++ b/sys/src/cmd/spin/guided.c
@@ -1,17 +1,15 @@
 /***** spin: guided.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 <sys/types.h>
 #include <sys/stat.h>
+#include <limits.h>
 #include "y.tab.h"
 
 extern RunList	*run, *X;
@@ -19,8 +17,9 @@ extern Element	*Al_El;
 extern Symbol	*Fname, *oFname;
 extern int	verbose, lineno, xspin, jumpsteps, depth, merger, cutoff;
 extern int	nproc, nstop, Tval, ntrail, columns;
-extern short	Have_claim, Skip_claim;
+extern short	Have_claim, Skip_claim, has_code;
 extern void ana_src(int, int);
+extern char	**trailfilename;
 
 int	TstOnly = 0, pno;
 
@@ -73,12 +72,70 @@ not_claim(void)
 	return (!Have_claim || !X || X->pid != 0);
 }
 
+int globmin = INT_MAX;
+int globmax = 0;
+
+int
+find_min(Sequence *s)
+{	SeqList *l;
+	Element *e;
+
+	if (s->minel < 0)
+	{	s->minel = INT_MAX;
+		for (e = s->frst; e; e = e->nxt)
+		{	if (e->status & 512)
+			{	continue;
+			}
+			e->status |= 512;
+
+			if (e->n->ntyp == ATOMIC
+			||  e->n->ntyp == NON_ATOMIC
+			||  e->n->ntyp == D_STEP)
+			{	int n = find_min(e->n->sl->this);
+				if (n < s->minel)
+				{	s->minel = n;
+				}
+			} else if (e->Seqno < s->minel)
+			{	s->minel = e->Seqno;
+			}
+			for (l = e->sub; l; l = l->nxt)
+			{	int n = find_min(l->this);
+				if (n < s->minel)
+				{	s->minel = n;
+		}	}	}
+	}
+	if (s->minel < globmin)
+	{	globmin = s->minel;
+	}
+	return s->minel;
+}
+
+int
+find_max(Sequence *s)
+{
+	if (s->last->Seqno > globmax)
+	{	globmax = s->last->Seqno;
+	}
+	return s->last->Seqno;
+}
+
 void
 match_trail(void)
 {	int i, a, nst;
 	Element *dothis;
 	char snap[512], *q;
 
+	if (has_code)
+	{	printf("spin: important:\n");
+		printf("  =======================================warning====\n");
+		printf("  this model contains embedded c code statements\n");
+		printf("  these statements will not be executed when the trail\n");
+		printf("  is replayed in this way -- they are just printed,\n");
+		printf("  which will likely lead to inaccurate variable values.\n");
+		printf("  for an accurate replay use: ./pan -r\n");
+		printf("  =======================================warning====\n\n");
+	}
+
 	/*
 	 * if source model name is leader.pml
 	 * look for the trail file under these names:
@@ -88,10 +145,18 @@ match_trail(void)
 	 *	leader.tra
 	 */
 
-	if (ntrail)
-		sprintf(snap, "%s%d.trail", oFname->name, ntrail);
-	else
-		sprintf(snap, "%s.trail", oFname->name);
+	if (trailfilename)
+	{	if (strlen(*trailfilename) < sizeof(snap))
+		{	strcpy(snap, (const char *) *trailfilename);
+		} else
+		{	fatal("filename %s too long", *trailfilename);
+		}
+	} else
+	{	if (ntrail)
+			sprintf(snap, "%s%d.trail", oFname->name, ntrail);
+		else
+			sprintf(snap, "%s.trail", oFname->name);
+	}
 
 	if ((fd = fopen(snap, "r")) == NULL)
 	{	snap[strlen(snap)-2] = '\0';	/* .tra */
@@ -118,9 +183,9 @@ match_trail(void)
 	}	}
 okay:		
 	if (xspin == 0 && newer(oFname->name, snap))
-	printf("spin: warning, \"%s\" is newer than %s\n",
-		oFname->name, snap);
-
+	{	printf("spin: warning, \"%s\" is newer than %s\n",
+			oFname->name, snap);
+	}
 	Tval = 1;
 
 	/*
@@ -132,10 +197,23 @@ okay:
 	hookup();
 
 	while (fscanf(fd, "%d:%d:%d\n", &depth, &pno, &nst) == 3)
-	{	if (depth == -2) { start_claim(pno); continue; }
-		if (depth == -4) { merger = 1; ana_src(0, 1); continue; }
-		if (depth == -1)
+	{	if (depth == -2)
 		{	if (verbose)
+			{	printf("starting claim %d\n", pno);
+			}
+			start_claim(pno);
+			continue;
+		}
+		if (depth == -4)
+		{	if (verbose)
+			{	printf("using statement merging\n");
+			}
+			merger = 1;
+			ana_src(0, 1);
+			continue;
+		}
+		if (depth == -1)
+		{	if (1 || verbose)
 			{	if (columns == 2)
 				dotag(stdout, " CYCLE>\n");
 				else
@@ -188,16 +266,50 @@ okay:
 				pno - Have_claim, i, nst, dothis->n->ntyp);
 			lost_trail();
 		}
+
+		if (0 && !xspin && (verbose&32))
+		{	printf("step %d i=%d pno %d stmnt %d\n", depth, i, pno, nst);
+		}
+
 		for (X = run; X; X = X->nxt)
 		{	if (--i == pno)
 				break;
 		}
+
 		if (!X)
-		{	printf("%3d: no process %d ", depth, pno - Have_claim);
-			printf("(state %d)\n", nst);
-			lost_trail();
+		{	if (verbose&32)
+			{	printf("%3d: no process %d (stmnt %d)\n", depth, pno - Have_claim, nst);
+				printf(" max %d (%d - %d + %d) claim %d ",
+					nproc - nstop + Skip_claim,
+					nproc, nstop, Skip_claim, Have_claim);
+				printf("active processes:\n");
+				for (X = run; X; X = X->nxt)
+				{	printf("\tpid %d\tproctype %s\n", X->pid, X->n->name);
+				}
+				printf("\n");
+				continue;	
+			} else
+			{	printf("%3d:\tproc  %d (?) ", depth, pno);
+				lost_trail();
+			}
+		} else
+		{	int min_seq = find_min(X->ps);
+			int max_seq = find_max(X->ps);
+
+
+			if (nst < min_seq || nst > max_seq)
+			{	printf("%3d: error: invalid statement", depth);
+				if (verbose&32)
+				{	printf(": pid %d:%d (%s:%d:%d) stmnt %d (valid range %d .. %d)",
+					pno, X->pid, X->n->name, X->tn, X->b, nst, min_seq, max_seq);
+				}
+				printf("\n");
+				continue;
+				/* lost_trail(); */
+			}
+			X->pc  = dothis;
 		}
-		X->pc  = dothis;
+
 		lineno = dothis->n->ln;
 		Fname  = dothis->n->fn;
 
@@ -271,7 +383,7 @@ keepgoing:		if (dothis->merge_start)
 		}	}
 
 		if (Have_claim && X && X->pid == 0
-		&&  dothis && dothis->n
+		&&  dothis->n
 		&&  lastclaim != dothis->n->ln)
 		{	lastclaim = dothis->n->ln;
 			if (columns == 2)