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, 57 insertions, 20 deletions

diff --git a/sys/src/cmd/spin/tl_trans.c b/sys/src/cmd/spin/tl_trans.c
index 72964ca6b..ed5b5878a 100644
--- a/sys/src/cmd/spin/tl_trans.c
+++ b/sys/src/cmd/spin/tl_trans.c
@@ -1,21 +1,18 @@
 /***** tl_spin: tl_trans.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 FILE	*tl_out;
-extern int	tl_errs, tl_verbose, tl_terse, newstates;
+extern int	tl_errs, tl_verbose, tl_terse, newstates, state_cnt;
 
 int	Stack_mx=0, Max_Red=0, Total=0;
 
@@ -23,7 +20,7 @@ static Mapping	*Mapped = (Mapping *) 0;
 static Graph	*Nodes_Set = (Graph *) 0;
 static Graph	*Nodes_Stack = (Graph *) 0;
 
-static char	dumpbuf[2048];
+static char	dumpbuf[4096];
 static int	Red_cnt  = 0;
 static int	Lab_cnt  = 0;
 static int	Base     = 0;
@@ -51,6 +48,24 @@ static void	ng(Symbol *, Symbol *, Node *, Node *, Node *);
 static void	push_stack(Graph *);
 static void	sdump(Node *);
 
+void
+ini_trans(void)
+{
+	Stack_mx = 0;
+	Max_Red = 0;
+	Total = 0;
+
+	Mapped = (Mapping *) 0;
+	Nodes_Set = (Graph *) 0;
+	Nodes_Stack = (Graph *) 0;
+
+	memset(dumpbuf, 0, sizeof(dumpbuf));
+	Red_cnt  = 0;
+	Lab_cnt  = 0;
+	Base     = 0;
+	Stack_sz = 0;
+}
+
 static void
 dump_graph(Graph *g)
 {	Node *n1;
@@ -101,9 +116,8 @@ pop_stack(void)
 
 static char *
 newname(void)
-{	static int cnt = 0;
-	static char buf[32];
-	sprintf(buf, "S%d", cnt++);
+{	static char buf[32];
+	sprintf(buf, "S%d", state_cnt++);
 	return buf;
 }
 
@@ -132,6 +146,8 @@ static void
 mk_grn(Node *n)
 {	Graph *p;
 
+	if (!n) return;
+
 	n = right_linked(n);
 more:
 	for (p = Nodes_Set; p; p = p->nxt)
@@ -152,6 +168,8 @@ static void
 mk_red(Node *n)
 {	Graph *p;
 
+	if (!n) return;
+
 	n = right_linked(n);
 	for (p = Nodes_Set; p; p = p->nxt)
 	{	if (p->outgoing
@@ -240,6 +258,15 @@ dump_cond(Node *pp, Node *r, int first)
 	q = dupnode(pp);
 	q = rewrite(q);
 
+	if (q->ntyp == CEXPR)
+	{	if (!frst) fprintf(tl_out, " && ");
+		fprintf(tl_out, "c_expr { ");
+		dump_cond(q->lft, r, 1);
+		fprintf(tl_out, " } ");
+		frst = 0;
+		return frst;
+	}
+
 	if (q->ntyp == PREDICATE
 	||  q->ntyp == NOT
 #ifndef NXT
@@ -342,7 +369,7 @@ static void
 fsm_trans(Graph *p, int count, char *curnm)
 {	Graph	*r;
 	Symbol	*s;
-	char	prefix[128], nwnm[128];
+	char	prefix[128], nwnm[256];
 
 	if (!p->outgoing)
 		addtrans(p, curnm, False, "accept_all");
@@ -452,9 +479,11 @@ fixinit(Node *orig)
 
 	ng(tl_lookup("init"), ZS, ZN, ZN, ZN);
 	p1 = pop_stack();
-	p1->nxt = Nodes_Set;
-	p1->Other = p1->Old = orig;
-	Nodes_Set = p1;
+	if (p1)
+	{	p1->nxt = Nodes_Set;
+		p1->Other = p1->Old = orig;
+		Nodes_Set = p1;
+	}
 
 	for (g = Nodes_Set; g; g = g->nxt)
 	{	for (q1 = g->incoming; q1; q1 = q2)
@@ -532,6 +561,10 @@ common1:		sdump(n->lft);
 	case NEXT:	strcat(dumpbuf, "X");
 			goto common1;
 #endif
+	case CEXPR:	strcat(dumpbuf, "c_expr {");
+			sdump(n->lft);
+			strcat(dumpbuf, "}");
+			break;
 	case NOT:	strcat(dumpbuf, "!");
 			goto common1;
 	case TRUE:	strcat(dumpbuf, "T");
@@ -718,10 +751,13 @@ out:
 		break;
 	case PREDICATE:
 	case NOT:
+	case CEXPR:
 		if (can_release) releasenode(1, now);
 		push_stack(g);
 		break;
 	case V_OPER:
+		Assert(now->rgt != ZN, now->ntyp);
+		Assert(now->lft != ZN, now->ntyp);
 		Assert(now->rgt->nxt == ZN, now->ntyp);
 		Assert(now->lft->nxt == ZN, now->ntyp);
 		n1 = now->rgt;
@@ -759,6 +795,7 @@ out:
 
 #ifdef NXT
 	case NEXT:
+		Assert(now->lft != ZN, now->ntyp);
 		nx = dupnode(now->lft);
 		nx->nxt = g->Next;
 		g->Next = nx;