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, 259 insertions, 11 deletions

diff --git a/sys/src/cmd/spin/reprosrc.c b/sys/src/cmd/spin/reprosrc.c
index 0d4ba6be7..d418eaf59 100644
--- a/sys/src/cmd/spin/reprosrc.c
+++ b/sys/src/cmd/spin/reprosrc.c
@@ -1,22 +1,21 @@
 /***** spin: reprosrc.c *****/
 
-/* Copyright (c) 2002-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 <stdio.h>
+#include <assert.h>
 #include "spin.h"
 #include "y.tab.h"
 
 static int indent = 1;
 
+extern YYSTYPE yylval;
 extern ProcList	*rdy;
-void repro_seq(Sequence *);
+static void repro_seq(Sequence *);
 
 void
 doindent(void)
@@ -48,7 +47,7 @@ repro_sub(Element *e)
 	printf(" };\n");
 }
 
-void
+static void
 repro_seq(Sequence *s)
 {	Element *e;
 	Symbol *v;
@@ -96,7 +95,7 @@ repro_seq(Sequence *s)
 				doindent();
 				if (e->n->ntyp == C_CODE)
 				{	printf("c_code ");
-					plunk_inline(stdout, e->n->sym->name, 1);
+					plunk_inline(stdout, e->n->sym->name, 1, 1);
 				} else if (e->n->ntyp == 'c'
 				       &&  e->n->lft->ntyp == C_EXPR)
 				{	printf("c_expr { ");
@@ -134,3 +133,252 @@ repro_src(void)
 {
 	repro_proc(rdy);
 }
+
+static int in_decl;
+static int in_c_decl;
+static int in_c_code;
+
+void
+blip(int n, char *b)
+{	char mtxt[1024];
+
+	strcpy(mtxt, "");
+
+	switch (n) {
+	default:	if (n > 0 && n < 256)
+				sprintf(mtxt, "%c", n);
+			else
+				sprintf(mtxt, "<%d?>", n);
+
+			break;
+	case '(':	strcpy(mtxt, "("); in_decl++; break;
+	case ')':	strcpy(mtxt, ")"); in_decl--; break;
+	case '{':	strcpy(mtxt, "{"); break;
+	case '}':	strcpy(mtxt, "}"); break;
+	case '\t':	sprintf(mtxt, "\\t"); break;
+	case '\f':	sprintf(mtxt, "\\f"); break;
+	case '\n':	sprintf(mtxt, "\\n"); break;
+	case '\r':	sprintf(mtxt, "\\r"); break;
+	case 'c':	sprintf(mtxt, "condition"); break;
+	case 's':	sprintf(mtxt, "send"); break;
+	case 'r':	sprintf(mtxt, "recv"); break;
+	case 'R':	sprintf(mtxt, "recv poll"); break;
+	case '@':	sprintf(mtxt, "@"); break;
+	case '?':	sprintf(mtxt, "(x->y:z)"); break;
+	case NEXT:	sprintf(mtxt, "X"); break;
+	case ALWAYS:	sprintf(mtxt, "[]"); break;
+	case EVENTUALLY: sprintf(mtxt, "<>"); break;
+	case IMPLIES:	sprintf(mtxt, "->"); break;
+	case EQUIV:	sprintf(mtxt, "<->"); break;
+	case UNTIL:	sprintf(mtxt, "U"); break;
+	case WEAK_UNTIL: sprintf(mtxt, "W"); break;
+	case IN: sprintf(mtxt, "in"); break;
+	case ACTIVE:	sprintf(mtxt, "active"); break;
+	case AND:	sprintf(mtxt, "&&"); break;
+	case ARROW:	sprintf(mtxt, "->"); break;
+	case ASGN:	sprintf(mtxt, "="); break;
+	case ASSERT:	sprintf(mtxt, "assert"); break;
+	case ATOMIC:	sprintf(mtxt, "atomic"); break;
+	case BREAK:	sprintf(mtxt, "break"); break;
+	case C_CODE:	sprintf(mtxt, "c_code"); in_c_code++; break;
+	case C_DECL:	sprintf(mtxt, "c_decl"); in_c_decl++; break;
+	case C_EXPR:	sprintf(mtxt, "c_expr"); break;
+	case C_STATE:	sprintf(mtxt, "c_state"); break;
+	case C_TRACK:	sprintf(mtxt, "c_track"); break;
+	case CLAIM:	sprintf(mtxt, "never"); break;
+	case CONST:	sprintf(mtxt, "%d", yylval->val); break;
+	case DECR:	sprintf(mtxt, "--"); break;
+	case D_STEP:	sprintf(mtxt, "d_step"); break;
+	case D_PROCTYPE: sprintf(mtxt, "d_proctype"); break;
+	case DO:	sprintf(mtxt, "do"); break;
+	case DOT:	sprintf(mtxt, "."); break;
+	case ELSE:	sprintf(mtxt, "else"); break;
+	case EMPTY:	sprintf(mtxt, "empty"); break;
+	case ENABLED:	sprintf(mtxt, "enabled"); break;
+	case EQ:	sprintf(mtxt, "=="); break;
+	case EVAL:	sprintf(mtxt, "eval"); break;
+	case FI:	sprintf(mtxt, "fi"); break;
+	case FULL:	sprintf(mtxt, "full"); break;
+	case GE:	sprintf(mtxt, ">="); break;
+	case GET_P:	sprintf(mtxt, "get_priority"); break;
+	case GOTO:	sprintf(mtxt, "goto"); break;
+	case GT:	sprintf(mtxt, ">"); break;
+	case HIDDEN:	sprintf(mtxt, "hidden"); break;
+	case IF:	sprintf(mtxt, "if"); break;
+	case INCR:	sprintf(mtxt, "++"); break;
+
+	case INLINE:	sprintf(mtxt, "inline"); break;
+	case INIT:	sprintf(mtxt, "init"); break;
+	case ISLOCAL:	sprintf(mtxt, "local"); break;
+
+	case LABEL:	sprintf(mtxt, "<label-name>"); break;
+
+	case LE:	sprintf(mtxt, "<="); break;
+	case LEN:	sprintf(mtxt, "len"); break;
+	case LSHIFT:	sprintf(mtxt, "<<"); break;
+	case LT:	sprintf(mtxt, "<"); break;
+	case LTL:	sprintf(mtxt, "ltl"); break;
+
+	case NAME:	sprintf(mtxt, "%s", yylval->sym->name); break;
+
+	case XU:	switch (yylval->val) {
+			case XR:	sprintf(mtxt, "xr"); break;
+			case XS:	sprintf(mtxt, "xs"); break;
+			default:	sprintf(mtxt, "<?>"); break;
+			}
+			break;
+
+	case TYPE:	switch (yylval->val) {
+			case BIT:	sprintf(mtxt, "bit"); break;
+			case BYTE:	sprintf(mtxt, "byte"); break;
+			case CHAN:	sprintf(mtxt, "chan"); in_decl++; break;
+			case INT:	sprintf(mtxt, "int"); break;
+			case MTYPE:	sprintf(mtxt, "mtype"); break;
+			case SHORT:	sprintf(mtxt, "short"); break;
+			case UNSIGNED:	sprintf(mtxt, "unsigned"); break;
+			default:	sprintf(mtxt, "<unknown type>"); break;
+			}
+			break;
+
+	case NE:	sprintf(mtxt, "!="); break;
+	case NEG:	sprintf(mtxt, "!"); break;
+	case NEMPTY:	sprintf(mtxt, "nempty"); break;
+	case NFULL:	sprintf(mtxt, "nfull"); break;
+
+	case NON_ATOMIC: sprintf(mtxt, "<sub-sequence>"); break;
+
+	case NONPROGRESS: sprintf(mtxt, "np_"); break;
+	case OD:	sprintf(mtxt, "od"); break;
+	case OF:	sprintf(mtxt, "of"); break;
+	case OR:	sprintf(mtxt, "||"); break;
+	case O_SND:	sprintf(mtxt, "!!"); break;
+	case PC_VAL:	sprintf(mtxt, "pc_value"); break;
+	case PRINT:	sprintf(mtxt, "printf"); break;
+	case PRINTM:	sprintf(mtxt, "printm"); break;
+	case PRIORITY:	sprintf(mtxt, "priority"); break;
+	case PROCTYPE:	sprintf(mtxt, "proctype"); break;
+	case PROVIDED:	sprintf(mtxt, "provided"); break;
+	case RCV:	sprintf(mtxt, "?"); break;
+	case R_RCV:	sprintf(mtxt, "??"); break;
+	case RSHIFT:	sprintf(mtxt, ">>"); break;
+	case RUN:	sprintf(mtxt, "run"); break;
+	case SEP:	sprintf(mtxt, "::"); break;
+	case SEMI:	sprintf(mtxt, ";"); break;
+	case SET_P:	sprintf(mtxt, "set_priority"); break;
+	case SHOW:	sprintf(mtxt, "show"); break;
+	case SND:	sprintf(mtxt, "!"); break;
+
+	case INAME:
+	case UNAME:
+	case PNAME:
+	case STRING:	sprintf(mtxt, "%s", yylval->sym->name); break;
+
+	case TRACE:	sprintf(mtxt, "trace"); break;
+	case TIMEOUT:	sprintf(mtxt, "timeout"); break;
+	case TYPEDEF:	sprintf(mtxt, "typedef"); break;
+	case UMIN:	sprintf(mtxt, "-"); break;
+	case UNLESS:	sprintf(mtxt, "unless"); break;
+	}
+	strcat(b, mtxt);
+}
+
+void
+purge(char *b)
+{
+	if (strlen(b) == 0) return;
+
+	if (b[strlen(b)-1] != ':')	/* label? */
+	{	if (b[0] == ':' && b[1] == ':')
+		{	indent--;
+			doindent();
+			indent++;
+		} else
+		{	doindent();
+		}
+	}
+	printf("%s\n", b);
+	strcpy(b, "");
+
+	in_decl = 0;
+	in_c_code = 0;
+	in_c_decl = 0;
+}
+
+int pp_mode;
+extern int lex(void);
+
+void
+pretty_print(void)
+{	int c, lastc = 0;
+	char buf[1024];
+
+	pp_mode = 1;
+	indent = 0;
+	strcpy(buf, "");
+	while ((c = lex()) != EOF)
+	{
+		if ((lastc == IF || lastc == DO) && c != SEP)
+		{	indent--;	/* c_code if */
+		}
+		if (c == C_DECL  || c == C_STATE
+		||  c == C_TRACK || c == SEP
+		||  c == DO      || c == IF
+		|| (c == TYPE && !in_decl))
+		{	purge(buf); /* start on new line */
+		}
+
+		if (c == '{'
+		&& lastc != OF && lastc != IN
+		&& lastc != ATOMIC && lastc != D_STEP
+		&& lastc != C_CODE && lastc != C_DECL && lastc != C_EXPR)
+		{	purge(buf);
+		}
+
+		if (c == PREPROC)
+		{	int oi = indent;
+			purge(buf);
+			assert(strlen(yylval->sym->name) < sizeof(buf));
+			strcpy(buf, yylval->sym->name);
+			indent = 0;
+			purge(buf);
+			indent = oi;
+			continue;
+		}
+
+		if (c != ':' && c != SEMI
+		&&  c != ',' && c != '('
+		&&  c != '#' && lastc != '#'
+		&&  c != ARROW && lastc != ARROW
+		&&  c != '.' && lastc != '.'
+		&&  c != '!' && lastc != '!'
+		&&  c != SND && lastc != SND
+		&&  c != RCV && lastc != RCV
+		&&  c != O_SND && lastc != O_SND
+		&&  c != R_RCV && lastc != R_RCV
+		&&  (c != ']' || lastc != '[')
+		&&  (c != '>' || lastc != '<')
+		&&  (c != GT || lastc != LT)
+		&&  c != '@' && lastc != '@'
+		&&  c != DO && c != OD && c != IF && c != FI
+		&&  c != SEP && strlen(buf) > 0)
+			strcat(buf, " ");
+
+		if (c == '}' || c == OD || c == FI)
+		{	purge(buf);
+			indent--;
+		}
+		blip(c, buf);
+
+		if (c == '{' || c == DO || c == IF)
+		{	purge(buf);
+			indent++;
+		}
+
+		if (c == '}' || c == BREAK || c == SEMI
+		|| (c == ':' && lastc == NAME))
+		{	purge(buf);
+		}
+		lastc = c;
+	}
+	purge(buf);
+}