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, 76 insertions, 19 deletions

diff --git a/sys/src/cmd/spin/tl_main.c b/sys/src/cmd/spin/tl_main.c
index 10ab0e9bd..667834265 100644
--- a/sys/src/cmd/spin/tl_main.c
+++ b/sys/src/cmd/spin/tl_main.c
@@ -1,16 +1,13 @@
 /***** tl_spin: tl_main.c *****/
 
-/* Copyright (c) 1995-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            */
-
-/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
-/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */
+/*
+ * 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
+ *
+ * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
+ * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
+ */
 
 #include "tl.h"
 
@@ -21,7 +18,10 @@ int	tl_errs    = 0;
 int	tl_verbose = 0;
 int	tl_terse   = 0;
 int	tl_clutter = 0;
+int	state_cnt = 0;
+
 unsigned long	All_Mem = 0;
+char	*claim_name;
 
 static char	uform[4096];
 static int	hasuform=0, cnt=0;
@@ -38,6 +38,15 @@ tl_Getchar(void)
 	return -1;
 }
 
+int
+tl_peek(int n)
+{
+	if (cnt+n < hasuform)
+	{	return uform[cnt+n];
+	}
+	return -1;
+}
+
 void
 tl_balanced(void)
 {	int i;
@@ -45,10 +54,21 @@ tl_balanced(void)
 
 	for (i = 0; i < hasuform; i++)
 	{	if (uform[i] == '(')
-		{	k++;
+		{	if (i > 0
+			&& ((uform[i-1] == '"'  && uform[i+1] == '"')
+			||  (uform[i-1] == '\'' && uform[i+1] == '\'')))
+			{	continue;
+			}
+			k++;
 		} else if (uform[i] == ')')
-		{	k--;
+		{	if (i > 0
+			&& ((uform[i-1] == '"'  && uform[i+1] == '"')
+			||  (uform[i-1] == '\'' && uform[i+1] == '\'')))
+			{	continue;
+			}
+			k--;
 	}	}
+
 	if (k != 0)
 	{	tl_errs++;
 		tl_yyerror("parentheses not balanced");
@@ -79,18 +99,40 @@ tl_stats(void)
 int
 tl_main(int argc, char *argv[])
 {	int i;
-	extern int verbose, xspin;
-	tl_verbose = verbose;
-	tl_clutter = 1-xspin;	/* use -X -f to turn off uncluttering */
+	extern int xspin, s_trail;
+
+	tl_verbose = 0; /* was: tl_verbose = verbose; */
+	if (xspin && s_trail)
+	{	tl_clutter = 1;
+		/* generating claims for a replay should
+		   be done the same as when generating the
+		   pan.c that produced the error-trail */
+	} else
+	{	tl_clutter = 1-xspin;	/* use -X -f to turn off uncluttering */
+	}
+	newstates  = 0;
+	state_cnt  = 0;
+	tl_errs    = 0;
+	tl_terse   = 0;
+	All_Mem = 0;
+	memset(uform, 0, sizeof(uform));
+	hasuform=0;
+	cnt=0;
+	claim_name = (char *) 0;
+
+	ini_buchi();
+	ini_cache();
+	ini_rewrt();
+	ini_trans();
 
 	while (argc > 1 && argv[1][0] == '-')
-	{	switch (argv[1][1]) {
+	{
+		switch (argv[1][1]) {
 		case 'd':	newstates = 1;	/* debugging mode */
 				break;
 		case 'f':	argc--; argv++;
-				for (i = 0; i < argv[1][i]; i++)
+				for (i = 0; argv[1][i]; i++)
 				{	if (argv[1][i] == '\t'
-					||  argv[1][i] == '\"'
 					||  argv[1][i] == '\n')
 						argv[1][i] = ' ';
 				}
@@ -101,6 +143,10 @@ tl_main(int argc, char *argv[])
 				break;
 		case 'n':	tl_terse = 1;
 				break;
+		case 'c':	argc--; argv++;
+				claim_name = (char *) emalloc(strlen(argv[1])+1);
+				strcpy(claim_name, argv[1]);
+				break;
 		default :	printf("spin -f: saw '-%c'\n", argv[1][1]);
 				goto nogood;
 		}
@@ -162,6 +208,12 @@ dump(Node *n)
 	case PREDICATE:
 		fprintf(tl_out, "(%s)", n->sym->name);
 		break;
+	case CEXPR:
+		fprintf(tl_out, "c_expr");
+		fprintf(tl_out, " {");
+		dump(n->lft);
+		fprintf(tl_out, "}");
+		break;
 	case -1:
 		fprintf(tl_out, " D ");
 		break;
@@ -189,6 +241,7 @@ tl_explain(int n)
 #ifdef NXT
 	case NEXT:	printf("X"); break;
 #endif
+	case CEXPR:	printf("c_expr"); break;
 	case TRUE:	printf("true"); break;
 	case FALSE:	printf("false"); break;
 	case ';':	printf("end of formula"); break;
@@ -202,10 +255,14 @@ tl_non_fatal(char *s1, char *s2)
 	int i;
 
 	printf("tl_spin: ");
+#if 1
+	printf(s1, s2);	/* prevent a compiler warning */
+#else
 	if (s2)
 		printf(s1, s2);
 	else
 		printf(s1);
+#endif
 	if (tl_yychar != -1 && tl_yychar != 0)
 	{	printf(", saw '");
 		tl_explain(tl_yychar);