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

diff --git a/sys/src/cmd/spin/tl_buchi.c b/sys/src/cmd/spin/tl_buchi.c
index 161661950..c7a9d2bf4 100644
--- a/sys/src/cmd/spin/tl_buchi.c
+++ b/sys/src/cmd/spin/tl_buchi.c
@@ -1,20 +1,18 @@
 /***** tl_spin: tl_buchi.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"
 
 extern int tl_verbose, tl_clutter, Total, Max_Red;
+extern char *claim_name;
 
 FILE	*tl_out;	/* if standalone: = stdout; */
 
@@ -38,6 +36,13 @@ typedef struct State {
 static State *never = (State *) 0;
 static int hitsall;
 
+void
+ini_buchi(void)
+{
+	never = (State *) 0;
+	hitsall = 0;
+}
+
 static int
 sametrans(Transition *s, Transition *t)
 {
@@ -58,6 +63,7 @@ Prune(Node *p)
 #ifdef NXT
 	case NEXT:
 #endif
+	case CEXPR:
 		return p;
 	case OR:
 		p->lft = Prune(p->lft);
@@ -545,10 +551,22 @@ rev_trans(Transition *t) /* print transitions  in reverse order... */
 	rev_trans(t->nxt);
 
 	if (t->redundant && !tl_verbose) return;
-	fprintf(tl_out, "\t:: (");
-	if (dump_cond(t->cond, t->cond, 1))
-		fprintf(tl_out, "1");
-	fprintf(tl_out, ") -> goto %s\n", t->name->name);
+
+	if (strcmp(t->name->name, "accept_all") == 0)	/* 6.2.4 */
+	{	/* not d_step because there may be remote refs */
+		fprintf(tl_out, "\t:: atomic { (");
+		if (dump_cond(t->cond, t->cond, 1))
+			fprintf(tl_out, "1");
+		fprintf(tl_out, ") -> assert(!(");
+		if (dump_cond(t->cond, t->cond, 1))
+			fprintf(tl_out, "1");
+		fprintf(tl_out, ")) }\n");
+	} else
+	{	fprintf(tl_out, "\t:: (");
+		if (dump_cond(t->cond, t->cond, 1))
+			fprintf(tl_out, "1");
+		fprintf(tl_out, ") -> goto %s\n", t->name->name);
+	}
 	tcnt++;
 }
 
@@ -570,11 +588,11 @@ printstate(State *b)
 	&&  Max_Red == 0)
 		fprintf(tl_out, "T0%s:\n", &(b->name->name[6]));
 
-	fprintf(tl_out, "\tif\n");
+	fprintf(tl_out, "\tdo\n");
 	tcnt = 0;
 	rev_trans(b->trans);
 	if (!tcnt) fprintf(tl_out, "\t:: false\n");
-	fprintf(tl_out, "\tfi;\n");
+	fprintf(tl_out, "\tod;\n");
 	Total++;
 }
 
@@ -626,13 +644,13 @@ fsm_print(void)
 	if (tl_clutter) clutter();
 
 	b = findstate("T0_init");
-	if (Max_Red == 0)
+	if (b && (Max_Red == 0))
 		b->accepting = 1;
 
 	mergestates(0); 
 	b = findstate("T0_init");
 
-	fprintf(tl_out, "never {    /* ");
+	fprintf(tl_out, "never %s {    /* ", claim_name?claim_name:"");
 		put_uform();
 	fprintf(tl_out, " */\n");