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, 376 insertions, 0 deletions

diff --git a/sys/src/cmd/spin/msc_tcl.c b/sys/src/cmd/spin/msc_tcl.c
new file mode 100644
index 000000000..196b8efe6
--- /dev/null
+++ b/sys/src/cmd/spin/msc_tcl.c
@@ -0,0 +1,376 @@
+/***** spin: msc_tcl.c *****/
+
+/*
+ * 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"
+#include "version.h"
+
+#define MW	500	/* page width */
+#define RH	100	/* right margin */
+#define WW	 80	/* distance between process lines */
+#define HH	 12	/* vertical distance between steps */
+#define LW	  2	/* line width of message arrows */
+
+#define RVC	"darkred"	/* rendezvous arrows */
+#define MPC	"darkblue"	/* asynchronous message passing arrow */
+#define GRC	"lightgrey"	/* grid lines */
+
+static int	MH = 600;	/* anticipated page-length */
+static FILE	*pfd;
+static char	**I;		/* initial procs */
+static int	*D,*R;		/* maps between depth (stepnr) and ldepth (msc-step) */
+static short	*M;		/* x location of each box at index y */
+static short	*T;		/* y index of match for each box at index y */
+static char	**L;		/* text labels */
+static int	ProcLine[256];	/* active processes */
+static int	UsedLine[256];	/* process line has at least one entry */
+static int	ldepth = 1;
+static int	maxx, TotSteps = 2*4096; /* max nr of steps for simulation output */
+static float	Scaler = (float) 1.0;
+
+static int	xscale = 2;
+static int	yscale = 1;
+static int	no_box;
+
+extern int	ntrail, s_trail, pno, depth;
+extern Symbol	*oFname;
+
+extern void	exit(int);
+extern void	putpostlude(void);
+
+static void	putpages(void);
+
+static void
+psline(int x0, int y0, int x1, int y1, char *color)
+{	char *side = "last";
+
+	if (x0 == x1)	/* gridline */
+	{	fprintf(pfd, ".c create line %d %d %d %d -fill %s -tags grid -width 1 \n",
+			xscale*(x0+1)*WW-20, yscale*y0+20,
+			xscale*(x1+1)*WW-20, yscale*y1+20, color);
+		fprintf(pfd, ".c lower grid\n");
+	} else
+	{	int xm = xscale*(x0+1)*WW + (xscale*(x1 - x0)*WW)/2 - 20;	/* mid x */
+
+		if (y1 - y0  <= HH+20)
+		{	y1 = y0+20; /* close enough to horizontal - looks better */
+		}
+ 
+		fprintf(pfd, ".c create line %d %d %d %d -fill %s -tags mesg -width %d\n",
+			xscale*(x0+1)*WW-20, yscale*y0+20+10,
+			xm,                  yscale*y0+20+10, color, LW);
+
+		if (y1 != y0+20)
+		{	fprintf(pfd, ".c create line %d %d %d %d -fill %s -tags mesg -width %d\n",
+				xm, yscale*y0+20+10,
+				xm, yscale*y1+20-10, color, LW);
+		}
+
+		fprintf(pfd, ".c create line %d %d %d %d -fill %s -width %d ",
+			xm,                  yscale*y1+20-10,
+			xscale*(x1+1)*WW-20, yscale*y1+20-10, color, LW);
+
+		if (strcmp(color, RVC) == 0)
+		{	side = "both";
+		}
+		fprintf(pfd, "-arrow %s -arrowshape {5 5 5} -tags mesg\n", side);
+		fprintf(pfd, ".c raise mesg\n");
+	}
+}
+
+static void
+colbox(int ix, int iy, int w, int h_unused, char *color)
+{	int x = ix*WW;
+	int y = iy*HH;
+
+	if (ix < 0 || ix > 255)
+	{	fatal("msc_tcl: unexpected\n", (char *) 0);
+	}
+
+	if (ProcLine[ix] < iy)
+	{	/* if (ProcLine[ix] > 0) */
+		{	psline(ix-1, ProcLine[ix]*HH+HH+4,
+			       ix-1, iy*HH-HH, GRC);
+		}
+		fprintf(pfd, "# ProcLine[%d] from %d to %d (Used %d nobox %d)\n",
+			ix, ProcLine[ix], iy, UsedLine[ix], no_box);
+		ProcLine[ix] = iy;
+	} else
+	{	fprintf(pfd, "# ProcLine[%d] stays at %d (Used %d nobox %d)\n",
+			ix, ProcLine[ix], UsedLine[ix], no_box);
+	}
+
+	if (UsedLine[ix])
+	{	no_box = 2;
+	}
+
+	if (strcmp(color, "black") == 0)
+	{	if (no_box == 0)	/* shadow */
+		{	fprintf(pfd, ".c create rectangle %d %d %d %d -fill black\n",
+				xscale*x-(xscale*4*w/3)-20+4, (yscale*y-10)+20+2,
+				xscale*x+(xscale*4*w/3)-20,   (yscale*y+10)+20+2);
+		}
+	} else
+	{	if (no_box == 0)	/* box with outline */
+		{	fprintf(pfd, ".c create rectangle %d %d %d %d -fill ivory\n",
+				xscale*x-(xscale*4*w/3)-20, (yscale*y-10)+20,
+				xscale*x+(xscale*4*w/3)-20, (yscale*y+10)+20);
+			UsedLine[ix]++;
+		} else			/* no outline */
+		{	fprintf(pfd, ".c create rectangle %d %d %d %d -fill white -width 0\n",
+				xscale*x-(xscale*4*w/3)-20, (yscale*y-10)+20,
+				xscale*x+(xscale*4*w/3)-20, (yscale*y+10)+20);
+	}	}
+	if (no_box > 0)
+	{	no_box--;
+	}
+}
+
+static void
+stepnumber(int i)
+{	int y = (yscale*i*HH) + 20;
+
+	fprintf(pfd, ".c create text %d %d -fill #eef -text \"%d\"\n",
+		-10+(xscale*WW)/2, y, i);
+
+	/* horizontal dashed grid line */
+	fprintf(pfd, ".c create line %d %d %d %d -fill #eef -dash {6 4}\n",
+		-20+WW*xscale, y, (maxx+1)*WW*xscale-20, y);
+}
+
+static void
+spitbox(int ix, int y, char *s)
+{	float bw;	/* box width */
+	char d[256], *t, *z;
+	int a, i, x = ix+1;
+	char *color = "black";
+
+	if (y > 0)
+	{	stepnumber(y);
+	}
+
+	bw = (float)1.8*(float)strlen(s);	/* guess at default font width */
+	colbox(x, y, (int) (bw+1.0), 5, "black");
+	if (s[0] == '~')
+	{	switch (s[1]) {
+		default :
+		case 'R': color = "red";   break;
+		case 'B': color = "blue";  break;
+		case 'G': color = "green"; break;
+		}
+		s += 2;
+	} else if (strchr(s, '!'))
+	{	color = "ivory";
+	} else if (strchr(s, '?'))
+	{	color = "azure";
+	} else
+	{	color = "pink";
+		if (sscanf(s, "%d:%250s", &a, d) == 2
+		&&  a >= 0 && a < TotSteps)
+		{	if (!I[a]  || strlen(I[a]) <= strlen(s))
+			{	I[a] = (char *) emalloc((int) strlen(s)+1);
+			}
+			strcpy(I[a], s);
+	}	}
+
+	colbox(x, y, (int) bw, 4, color);
+
+	z = t = (char *) emalloc(2*strlen(s)+1);
+
+	for (i = 0; i < (int) strlen(s); i++)
+	{	if (s[i] == '\n')
+		{	continue;
+		}
+		if (s[i] == '[' || s[i] == ']')
+		{	*t++ = '\\';
+		}
+		*t++ = s[i];
+	}
+
+	fprintf(pfd, ".c create text %d %d -text \"%s\"\n",
+		xscale*x*WW-20, yscale*y*HH+20, z);
+}
+
+static void
+putpages(void)
+{	int i, lasti=0; float nmh;
+
+	if (maxx*xscale*WW > MW-RH/2)
+	{	Scaler = (float) (MW-RH/2) / (float) (maxx*xscale*WW);
+		nmh = (float) MH; nmh /= Scaler; MH = (int) nmh;
+		fprintf(pfd, "# Scaler %f, MH %d\n", Scaler, MH);
+	}
+	if (ldepth >= TotSteps)
+	{	ldepth = TotSteps-1;
+	}
+
+/* W: (maxx+2)*xscale*WW  */
+/* H: ldepth*HH*yscale+50 */
+	fprintf(pfd, "wm title . \"scenario\"\n");
+	fprintf(pfd, "wm geometry . %dx600+650+100\n", (maxx+2)*xscale*WW);
+
+	fprintf(pfd, "canvas .c -width 800 -height 800 \\\n");
+	fprintf(pfd, "	-scrollregion {0c -1c 30c 100c} \\\n");
+	fprintf(pfd, "	-xscrollcommand \".hscroll set\" \\\n");
+	fprintf(pfd, "	-yscrollcommand \".vscroll set\" \\\n");
+	fprintf(pfd, "	-bg white -relief raised -bd 2\n");
+
+	fprintf(pfd, "scrollbar .vscroll -relief sunken ");
+	fprintf(pfd, " -command \".c yview\"\n");
+	fprintf(pfd, "scrollbar .hscroll -relief sunken -orient horiz ");
+	fprintf(pfd, " -command \".c xview\"\n");
+
+	fprintf(pfd, "pack append . \\\n");
+	fprintf(pfd, "	.vscroll {right filly} \\\n");
+	fprintf(pfd, "	.hscroll {bottom fillx} \\\n");
+	fprintf(pfd, "	.c {top expand fill}\n");
+
+	fprintf(pfd, ".c yview moveto 0\n");
+
+	for (i = TotSteps-1; i >= 0; i--)
+	{	if (I[i])
+		{	spitbox(i, -1, I[i]);
+	}	}
+
+	for (i = 0; i <= ldepth; i++)
+	{	if (!M[i] && !L[i])
+		{	continue;	/* no box */
+		}
+		if (T[i] > 0)		/* arrow */
+		{	if (T[i] == i)	/* rv handshake */
+			{	psline(	M[lasti], lasti*HH,
+					M[i],     i*HH, RVC);
+			} else
+			{	psline(	M[i],     i*HH,
+					M[T[i]],  T[i]*HH, MPC);
+		}	}
+		if (L[i])
+		{	spitbox(M[i], i, L[i]);
+			lasti = i;
+	}	}
+}
+
+static void
+putbox(int x)
+{
+	if (ldepth >= TotSteps)
+	{	fprintf(stderr, "max length of %d steps exceeded - ps file truncated\n",
+			TotSteps);
+		putpostlude();
+	}
+	M[ldepth] = x;
+	if (x > maxx)
+	{	maxx = x;
+		fprintf(pfd, "# maxx %d\n", x);
+	}
+}
+
+/* functions called externally: */
+
+extern int WhatSeed(void);
+
+void
+putpostlude(void)
+{	char cmd[512];
+
+	putpages();
+	fprintf(pfd, ".c lower grid\n");
+	fprintf(pfd, ".c raise mesg\n");
+	fclose(pfd);
+
+	fprintf(stderr, "seed used: -n%d\n", WhatSeed());
+	sprintf(cmd, "wish -f %s.tcl &", oFname?oFname->name:"msc");
+	fprintf(stderr, "%s\n", cmd);
+	(void) unlink("pan.pre");
+	exit (system(cmd));
+}
+
+void
+putprelude(void)
+{	char snap[256]; FILE *fd;
+
+	sprintf(snap, "%s.tcl", oFname?oFname->name:"msc");
+	if (!(pfd = fopen(snap, MFLAGS)))
+	{	fatal("cannot create file '%s'", snap);
+	}
+	if (s_trail)
+	{	if (ntrail)
+		sprintf(snap, "%s%d.trail", oFname?oFname->name:"msc", ntrail);
+		else
+		sprintf(snap, "%s.trail", oFname?oFname->name:"msc");
+		if (!(fd = fopen(snap, "r")))
+		{	snap[strlen(snap)-2] = '\0';
+			if (!(fd = fopen(snap, "r")))
+				fatal("cannot open trail file", (char *) 0);
+		}
+		TotSteps = 1;
+		while (fgets(snap, 256, fd)) TotSteps++;
+		fclose(fd);
+	}
+	TotSteps *= 2;
+	R = (int   *) emalloc(TotSteps * sizeof(int));
+	D = (int   *) emalloc(TotSteps * sizeof(int));
+	M = (short *) emalloc(TotSteps * sizeof(short));
+	T = (short *) emalloc(TotSteps * sizeof(short));
+	L = (char **) emalloc(TotSteps * sizeof(char *));
+	I = (char **) emalloc(TotSteps * sizeof(char *));
+}
+
+void
+putarrow(int from, int to)
+{
+	/* from rv if from == to */
+	/* which means that D[from] == D[to] */
+	/* which means that T[x] == x */
+
+	if (from    < TotSteps
+	&&  to      < TotSteps
+	&&  D[from] < TotSteps)
+	{	T[D[from]] = D[to];
+	}
+}
+
+void
+pstext(int x, char *s)
+{	char *tmp = emalloc((int) strlen(s)+1);
+
+	strcpy(tmp, s);
+	if (depth == 0)
+	{	I[x] = tmp;
+	} else
+	{	if (depth >= TotSteps || ldepth >= TotSteps)
+		{	fprintf(stderr, "spin: error: max nr of %d steps exceeded\n",
+				TotSteps);
+			fatal("use -uN to limit steps", (char *) 0);
+		}
+		putbox(x);
+		D[depth] = ldepth;
+		R[ldepth] = depth;
+		L[ldepth] = tmp;
+		ldepth += 2;
+	}
+}
+
+void
+dotag(FILE *fd, char *s)
+{	extern int columns, notabs; extern RunList *X;
+	int i = (!strncmp(s, "MSC: ", 5))?5:0;
+	int pid = s_trail ? pno : (X?X->pid:0);
+
+	if (columns == 2)
+	{	pstext(pid, &s[i]);
+	} else
+	{	if (!notabs)
+		{	printf("  ");
+			for (i = 0; i <= pid; i++)
+			{	printf("    ");
+		}	}
+		fprintf(fd, "%s", s);
+		fflush(fd);
+	}
+}