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, 176 insertions, 45 deletions

diff --git a/sys/src/cmd/spin/run.c b/sys/src/cmd/spin/run.c
index c336feef2..0df4b5f0a 100644
--- a/sys/src/cmd/spin/run.c
+++ b/sys/src/cmd/spin/run.c
@@ -1,13 +1,10 @@
 /***** spin: run.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 <stdlib.h>
 #include "spin.h"
@@ -16,15 +13,18 @@
 extern RunList	*X, *run;
 extern Symbol	*Fname;
 extern Element	*LastStep;
-extern int	Rvous, lineno, Tval, interactive, MadeChoice;
+extern int	Rvous, lineno, Tval, interactive, MadeChoice, Priority_Sum;
 extern int	TstOnly, verbose, s_trail, xspin, jumpsteps, depth;
-extern int	nproc, nstop, no_print, like_java;
+extern int	analyze, nproc, nstop, no_print, like_java, old_priority_rules;
+extern short	Have_claim;
 
 static long	Seed = 1;
 static int	E_Check = 0, Escape_Check = 0;
 
 static int	eval_sync(Element *);
 static int	pc_enabled(Lextok *n);
+static int	get_priority(Lextok *n);
+static void	set_priority(Lextok *n, Lextok *m);
 extern void	sr_buf(int, int);
 
 void
@@ -42,24 +42,23 @@ Rand(void)
 
 Element *
 rev_escape(SeqList *e)
-{	Element *r;
+{	Element *r = (Element *) 0;
 
-	if (!e)
-		return (Element *) 0;
+	if (e)
+	{	if ((r = rev_escape(e->nxt)) == ZE) /* reversed order */
+		{	r = eval_sub(e->this->frst);
+	}	}
 
-	if ((r = rev_escape(e->nxt)) != ZE) /* reversed order */
-		return r;
-
-	return eval_sub(e->this->frst);		
+	return r;		
 }
 
 Element *
 eval_sub(Element *e)
 {	Element *f, *g;
 	SeqList *z;
-	int i, j, k;
+	int i, j, k, only_pos;
 
-	if (!e->n)
+	if (!e || !e->n)
 		return ZE;
 #ifdef DEBUG
 	printf("\n\teval_sub(%d %s: line %d) ",
@@ -69,8 +68,13 @@ eval_sub(Element *e)
 #endif
 	if (e->n->ntyp == GOTO)
 	{	if (Rvous) return ZE;
-		LastStep = e; f = get_lab(e->n, 1);
+		LastStep = e;
+		f = get_lab(e->n, 1);
+		f = huntele(f, e->status, -1); /* 5.2.3: was missing */
 		cross_dsteps(e->n, f->n);
+#ifdef DEBUG
+		printf("GOTO leads to %d\n", f->seqno);
+#endif
 		return f;
 	}
 	if (e->n->ntyp == UNLESS)
@@ -80,6 +84,7 @@ eval_sub(Element *e)
 	{	Element *has_else = ZE;
 		Element *bas_else = ZE;
 		int nr_else = 0, nr_choices = 0;
+		only_pos = -1;
 
 		if (interactive
 		&& !MadeChoice && !E_Check
@@ -89,8 +94,10 @@ eval_sub(Element *e)
 		{	printf("Select stmnt (");
 			whoruns(0); printf(")\n");
 			if (nproc-nstop > 1)
-			printf("\tchoice 0: other process\n");
-		}
+			{	printf("\tchoice 0: other process\n");
+				nr_choices++;
+				only_pos = 0;
+		}	}
 		for (z = e->sub, j=0; z; z = z->nxt)
 		{	j++;
 			if (interactive
@@ -113,13 +120,21 @@ eval_sub(Element *e)
 				if (!Enabled0(z->this->frst))
 					printf("unexecutable, ");
 				else
-					nr_choices++;
+				{	nr_choices++;
+					only_pos = j;
+				}
 				comment(stdout, z->this->frst->n, 0);
 				printf("\n");
 		}	}
 
 		if (nr_choices == 0 && has_else)
-			printf("\tchoice %d: (else)\n", nr_else);
+		{	printf("\tchoice %d: (else)\n", nr_else);
+			only_pos = nr_else;
+		}
+
+		if (nr_choices <= 1 && only_pos != -1 && !MadeChoice)
+		{	MadeChoice = only_pos;
+		}
 
 		if (interactive && depth >= jumpsteps
 		&& !Escape_Check
@@ -132,8 +147,11 @@ eval_sub(Element *e)
 				else
 					printf("Select [0-%d]: ", j);
 				fflush(stdout);
-				scanf("%s", buf);
-				if (isdigit(buf[0]))
+				if (scanf("%64s", buf) <= 0)
+				{	printf("no input\n");
+					return ZE;
+				}
+				if (isdigit((int)buf[0]))
 					k = atoi(buf);
 				else
 				{	if (buf[0] == 'q')
@@ -155,6 +173,7 @@ eval_sub(Element *e)
 			else
 				k = Rand()%j;	/* nondeterminism */
 		}
+
 		has_else = ZE;
 		bas_else = ZE;
 		for (i = 0, z = e->sub; i < j+k; i++)
@@ -215,7 +234,7 @@ eval_sub(Element *e)
 		} else
 		{	SeqList *x;
 			if (!(e->status & (D_ATOM))
-			&&  e->esc && verbose&32)
+			&&  e->esc && (verbose&32))
 			{	printf("Stmnt [");
 				comment(stdout, e->n, 0);
 				printf("] has escape(s): ");
@@ -234,11 +253,18 @@ eval_sub(Element *e)
 			if (!(e->status & D_ATOM))	/* escapes don't reach inside d_steps */
 			/* 4.2.4: only the guard of a d_step can have an escape */
 #endif
+#if 1
+			if (!s_trail)	/* trail determines selections, new 5.2.5 */
+#endif
 			{	Escape_Check++;
 				if (like_java)
 				{	if ((g = rev_escape(e->esc)) != ZE)
 					{	if (verbose&4)
-							printf("\tEscape taken\n");
+						{	printf("\tEscape taken (-J) ");
+							if (g->n && g->n->fn)
+								printf("%s:%d", g->n->fn->name, g->n->ln);
+							printf("\n");
+						}
 						Escape_Check--;
 						return g;
 					}
@@ -246,18 +272,24 @@ eval_sub(Element *e)
 				{	for (x = e->esc; x; x = x->nxt)
 					{	if ((g = eval_sub(x->this->frst)) != ZE)
 						{	if (verbose&4)
-								printf("\tEscape taken\n");
+							{	printf("\tEscape taken ");
+								if (g->n && g->n->fn)
+									printf("%s:%d", g->n->fn->name, g->n->ln);
+								printf("\n");
+							}
 							Escape_Check--;
 							return g;
 				}	}	}
 				Escape_Check--;
 			}
-		
 			switch (e->n->ntyp) {
+			case ASGN:
+				if (check_track(e->n) == STRUCT) { break; }
+				/* else fall thru */
 			case TIMEOUT: case RUN:
 			case PRINT: case PRINTM:
 			case C_CODE: case C_EXPR:
-			case ASGN: case ASSERT:
+			case ASSERT:
 			case 's': case 'r': case 'c':
 				/* toplevel statements only */
 				LastStep = e;
@@ -308,7 +340,8 @@ assign(Lextok *now)
 		t = Sym_typ(now->rgt);
 		break;
 	}
-	typ_ck(Sym_typ(now->lft), t, "assignment"); 
+	typ_ck(Sym_typ(now->lft), t, "assignment");
+
 	return setval(now->lft, eval(now->rgt));
 }
 
@@ -371,6 +404,10 @@ eval(Lextok *now)
 	case  NEMPTY: return (qlen(now)>0);
 	case ENABLED: if (s_trail) return 1;
 		      return pc_enabled(now->lft);
+
+	case GET_P: return get_priority(now->lft);
+	case SET_P: set_priority(now->lft->lft, now->lft->rgt); return 1;
+
 	case    EVAL: return eval(now->lft);
 	case  PC_VAL: return pc_value(now->lft);
 	case NONPROGRESS: return nonprogress();
@@ -384,15 +421,21 @@ eval(Lextok *now)
 	case   'c': return eval(now->lft);	/* condition    */
 	case PRINT: return TstOnly?1:interprint(stdout, now);
 	case PRINTM: return TstOnly?1:printm(stdout, now);
-	case  ASGN: return assign(now);
-
-	case C_CODE: printf("%s:\t", now->sym->name);
-		     plunk_inline(stdout, now->sym->name, 0);
+	case  ASGN:
+		if (check_track(now) == STRUCT) { return 1; }
+		return assign(now);
+
+	case C_CODE: if (!analyze)
+		     {	printf("%s:\t", now->sym->name);
+		     	plunk_inline(stdout, now->sym->name, 0, 1);
+		     }
 		     return 1; /* uninterpreted */
 
-	case C_EXPR: printf("%s:\t", now->sym->name);
-		     plunk_expr(stdout, now->sym->name);
-		     printf("\n");
+	case C_EXPR: if (!analyze)
+		     {	printf("%s:\t", now->sym->name);
+		     	plunk_expr(stdout, now->sym->name);
+		     	printf("\n");
+		     }
 		     return 1; /* uninterpreted */
 
 	case ASSERT: if (TstOnly || eval(now->lft)) return 1;
@@ -407,6 +450,11 @@ eval(Lextok *now)
 	case   '.': return 1;	/* return label for compound */
 	case   '@': return 0;	/* stop state */
 	case  ELSE: return 1;	/* only hit here in guided trails */
+
+	case ',':	/* reached through option -A with array initializer */
+	case 0:
+		    return 0;	/* not great, but safe */
+
 	default   : printf("spin: bad node type %d (run)\n", now->ntyp);
 		    if (s_trail) printf("spin: trail file doesn't match spec?\n");
 		    fatal("aborting", 0);
@@ -426,7 +474,6 @@ printm(FILE *fd, Lextok *n)
 			j = n->lft->val;
 		else
 			j = eval(n->lft);
-		Buf[0] = '\0';
 		sr_buf(j, 1);
 		dotag(fd, Buf);
 	}
@@ -437,9 +484,9 @@ int
 interprint(FILE *fd, Lextok *n)
 {	Lextok *tmp = n->lft;
 	char c, *s = n->sym->name;
-	int i, j; char lbuf[512];
-	extern char Buf[];
-	char tBuf[4096];
+	int i, j; char lbuf[512]; /* matches value in sr_buf() */
+	extern char Buf[];	/* global, size 4096 */
+	char tBuf[4096];	/* match size of global Buf[] */
 
 	Buf[0] = '\0';
 	if (!no_print)
@@ -490,7 +537,7 @@ append:			 strcat(Buf, lbuf);
 		}
 		dotag(fd, Buf);
 	}
-	if (strlen(Buf) > 4096) fatal("printf string too long", 0);
+	if (strlen(Buf) >= 4096) fatal("printf string too long", 0);
 	return 1;
 }
 
@@ -512,6 +559,7 @@ Enabled1(Lextok *n)
 		verbose = v;
 		return i;
 
+	case SET_P:
 	case C_CODE: case C_EXPR:
 	case PRINT: case PRINTM:
 	case   ASGN: case ASSERT:
@@ -552,6 +600,7 @@ Enabled0(Element *e)
 	case '@':
 		return X->pid == (nproc-nstop-1);
 	case '.':
+	case SET_P:
 		return 1;
 	case GOTO:
 		if (Rvous) return 0;
@@ -594,9 +643,91 @@ pc_enabled(Lextok *n)
 	for (Y = run; Y; Y = Y->nxt)
 		if (--i == pid)
 		{	oX = X; X = Y;
-			result = Enabled0(Y->pc);
+			result = Enabled0(X->pc);
 			X = oX;
 			break;
 		}
 	return result;
 }
+
+int
+pc_highest(Lextok *n)
+{	int i = nproc - nstop;
+	int pid = eval(n);
+	int target = 0, result = 1;
+	RunList *Y, *oX;
+
+	if (X->prov && !eval(X->prov)) return 0; /* can't be highest unless fully enabled */
+
+	for (Y = run; Y; Y = Y->nxt)
+	{	if (--i == pid)
+		{	target = Y->priority;
+			break;
+	}	}
+if (0) printf("highest for pid %d @ priority = %d\n", pid, target);
+
+	oX = X;
+	i = nproc - nstop;
+	for (Y = run; Y; Y = Y->nxt)
+	{	i--;
+if (0) printf("	pid %d @ priority %d\t", Y->pid, Y->priority);
+		if (Y->priority > target)
+		{	X = Y;
+if (0) printf("enabled: %s\n", Enabled0(X->pc)?"yes":"nope");
+if (0) printf("provided: %s\n", eval(X->prov)?"yes":"nope");
+			if (Enabled0(X->pc) && (!X->prov || eval(X->prov)))
+			{	result = 0;
+				break;
+		}	}
+else
+if (0) printf("\n");
+	}
+	X = oX;
+
+	return result;
+}
+
+int
+get_priority(Lextok *n)
+{	int i = nproc - nstop;
+	int pid = eval(n);
+	RunList *Y;
+
+	if (old_priority_rules)
+	{	return 1;
+	}
+
+	for (Y = run; Y; Y = Y->nxt)
+	{	if (--i == pid)
+		{	return Y->priority;
+	}	}
+	return 0;
+}
+
+void
+set_priority(Lextok *n, Lextok *p)
+{	int i = nproc - nstop - Have_claim;
+	int pid = eval(n);
+	RunList *Y;
+
+	if (old_priority_rules)
+	{	return;
+	}
+	for (Y = run; Y; Y = Y->nxt)
+	{	if (--i == pid)
+		{	Priority_Sum -= Y->priority;
+			Y->priority = eval(p);
+			Priority_Sum += Y->priority;
+			if (1)
+			{	printf("%3d: setting priority of proc %d (%s) to %d\n",
+					depth, pid, Y->n->name, Y->priority);
+	}	}	}
+	if (verbose&32)
+	{	printf("\tPid\tName\tPriority\n");
+		for (Y = run; Y; Y = Y->nxt)
+		{	printf("\t%d\t%s\t%d\n",
+				Y->pid,
+				Y->n->name,
+				Y->priority);
+	}	}
+}