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, 68 insertions, 23 deletions

diff --git a/sys/src/cmd/spin/spin.h b/sys/src/cmd/spin/spin.h
index 327ec6871..2ec8d3038 100644
--- a/sys/src/cmd/spin/spin.h
+++ b/sys/src/cmd/spin/spin.h
@@ -1,13 +1,10 @@
 /***** spin: spin.h *****/
 
-/* 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
+ */
 
 #ifndef SEEN_SPIN_H
 #define SEEN_SPIN_H
@@ -15,6 +12,15 @@
 #include <stdio.h>
 #include <string.h>
 #include <ctype.h>
+#if !defined(WIN32) && !defined(WIN64)
+ #include <unistd.h>
+#endif
+#if !defined(PC) && !defined(_PLAN9)
+ #include <memory.h>
+#endif
+
+enum	    { INIV, PUTV, LOGV }; /* used in pangen1.c */
+enum btypes { NONE, N_CLAIM, I_PROC, A_PROC, P_PROC, E_TRACE, N_TRACE };
 
 typedef struct Lextok {
 	unsigned short	ntyp;	/* node type */
@@ -22,6 +28,7 @@ typedef struct Lextok {
 	int	val;		/* value attribute */
 	int	ln;		/* line number */
 	int	indstep;	/* part of d_step sequence */
+	int	uiid;		/* inline id, if non-zero */
 	struct Symbol	*fn;	/* file name */
 	struct Symbol	*sym;	/* symbol reference */
         struct Sequence *sq;	/* sequence */
@@ -54,6 +61,9 @@ typedef struct Symbol {
 				  64=treat as if local; 128=read at least once
 				 */
 	unsigned char	colnr;	/* for use with xspin during simulation */
+	unsigned char	isarray; /* set if decl specifies array bound */
+	unsigned char	*bscp;	/* block scope */
+	int	sc;		/* scope seq no -- set only for proctypes */
 	int	nbits;		/* optional width specifier */
 	int	nel;		/* 1 if scalar, >1 if array   */
 	int	setat;		/* last depth value changed   */
@@ -124,7 +134,7 @@ typedef struct Element {
 	int	merge_single;
 	short	merge_in;	/* nr of incoming edges */
 	short	merge_mark;	/* state was generated in merge sequence */
-	unsigned char	status;	/* used by analyzer generator  */
+	unsigned int	status;	/* used by analyzer generator  */
 	struct FSM_use	*dead;	/* optional dead variable list */
 	struct SeqList	*sub;	/* subsequences, for compounds */
 	struct SeqList	*esc;	/* zero or more escape sequences */
@@ -136,6 +146,7 @@ typedef struct Sequence {
 	Element	*frst;
 	Element	*last;		/* links onto continuations */
 	Element *extent;	/* last element in original */
+	int	minel;		/* minimum Seqno, set and used only in guided.c */
 	int	maxel;		/* 1+largest id in sequence */
 } Sequence;
 
@@ -148,6 +159,7 @@ typedef struct Label {
 	Symbol	*s;
 	Symbol	*c;
 	Element	*e;
+	int	uiid;		/* non-zero if label appears in an inline */
 	int	visible;	/* label referenced in claim (slice relevant) */
 	struct Label	*nxt;
 } Label;
@@ -157,11 +169,17 @@ typedef struct Lbreak {
 	struct Lbreak	*nxt;
 } Lbreak;
 
+typedef struct L_List {
+	Lextok *n;
+	struct L_List	*nxt;
+} L_List;
+
 typedef struct RunList {
 	Symbol	*n;		/* name            */
 	int	tn;		/* ordinal of type */
 	int	pid;		/* process id      */
 	int	priority;	/* for simulations only */
+	enum btypes b;		/* the type of process */
 	Element	*pc;		/* current stmnt   */
 	Sequence *ps;		/* used by analyzer generator */
 	Lextok	*prov;		/* provided clause */
@@ -174,11 +192,19 @@ typedef struct ProcList {
 	Lextok	*p;		/* parameters */
 	Sequence *s;		/* body       */
 	Lextok	*prov;		/* provided clause */
+	enum btypes b;		/* e.g., claim, trace, proc */
 	short	tn;		/* ordinal number */
-	short	det;		/* deterministic */
+	unsigned char	det;	/* deterministic */
+	unsigned char   unsafe;	/* contains global var inits */
+	unsigned char	priority; /* process priority, if any */
 	struct ProcList	*nxt;	/* linked list */
 } ProcList;
 
+typedef struct QH {
+	int	n;
+	struct	QH *nxt;
+} QH;
+
 typedef	Lextok *Lexptr;
 
 #define YYSTYPE	Lexptr
@@ -194,7 +220,8 @@ typedef	Lextok *Lexptr;
 #define DONE2	 16		/* used in putcode and main*/
 #define D_ATOM	 32		/* deterministic atomic    */
 #define ENDSTATE 64		/* normal endstate         */
-#define CHECK2	128
+#define CHECK2	128		/* status bits for remote ref check */
+#define CHECK3	256		/* status bits for atomic jump check */
 
 #define Nhash	255    		/* slots in symbol hash-table */
 
@@ -216,18 +243,24 @@ typedef	Lextok *Lexptr;
 
 #define SOMETHINGBIG	65536
 #define RATHERSMALL	512
+#define MAXSCOPESZ	1024
 
 #ifndef max
-#define max(a,b) (((a)<(b)) ? (b) : (a))
+ #define max(a,b) (((a)<(b)) ? (b) : (a))
 #endif
 
-enum	{ INIV, PUTV, LOGV };	/* for pangen[14].c */
+#ifdef PC
+ #define MFLAGS	"wb"
+#else
+ #define MFLAGS	"w"
+#endif
 
 /***** prototype definitions *****/
 Element	*eval_sub(Element *);
 Element	*get_lab(Lextok *, int);
-Element	*huntele(Element *, int, int);
+Element	*huntele(Element *, unsigned int, int);
 Element	*huntstart(Element *);
+Element *mk_skip(void);
 Element	*target(Element *);
 
 Lextok	*do_unless(Lextok *, Lextok *);
@@ -238,8 +271,9 @@ Lextok	*nn(Lextok *, int, Lextok *, Lextok *);
 Lextok	*rem_lab(Symbol *, Lextok *, Symbol *);
 Lextok	*rem_var(Symbol *, Lextok *, Symbol *, Lextok *);
 Lextok	*tail_add(Lextok *, Lextok *);
+Lextok	*return_statement(Lextok *);
 
-ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *);
+ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *, enum btypes);
 
 SeqList	*seqlist(Sequence *, SeqList *);
 Sequence *close_seq(int);
@@ -250,7 +284,8 @@ Symbol	*has_lab(Element *, int);
 Symbol	*lookup(char *);
 Symbol	*prep_inline(Symbol *, Lextok *);
 
-char	*emalloc(int);
+char	*put_inline(FILE *, char *);
+char	*emalloc(size_t);
 long	Rand(void);
 
 int	any_oper(Lextok *, int);
@@ -258,6 +293,7 @@ int	any_undo(Lextok *);
 int	c_add_sv(FILE *);
 int	cast_val(int, int, int);
 int	checkvar(Symbol *, int);
+int	check_track(Lextok *);
 int	Cnt_flds(Lextok *);
 int	cnt_mpars(Lextok *);
 int	complete_rendez(void);
@@ -274,12 +310,14 @@ int	has_typ(Lextok *, int);
 int	in_bound(Symbol *, int);
 int	interprint(FILE *, Lextok *);
 int	printm(FILE *, Lextok *);
+int	is_inline(void);
 int	ismtype(char *);
 int	isproctype(char *);
 int	isutype(char *);
 int	Lval_struct(Lextok *, Symbol *, int, int);
 int	main(int, char **);
 int	pc_value(Lextok *);
+int	pid_is_claim(int);
 int	proper_enabler(Lextok *);
 int	putcode(FILE *, Sequence *, Element *, int, int, int);
 int	q_is_sync(Lextok *);
@@ -298,7 +336,6 @@ int	Sym_typ(Lextok *);
 int	tl_main(int, char *[]);
 int	Width_set(int *, int, Lextok *);
 int	yyparse(void);
-int	yywrap(void);
 int	yylex(void);
 
 void	AST_track(Lextok *, int);
@@ -309,7 +346,6 @@ void	c_state(Symbol *, Symbol *, Symbol *);
 void	c_add_def(FILE *);
 void	c_add_loc(FILE *, char *);
 void	c_add_locinit(FILE *, int, char *);
-void	c_add_use(FILE *);
 void	c_chandump(FILE *);
 void	c_preview(void);
 void	c_struct(FILE *, char *, Symbol *);
@@ -321,6 +357,7 @@ void	check_param_count(int, Lextok *);
 void	checkrun(Symbol *, int);
 void	comment(FILE *, Lextok *, int);
 void	cross_dsteps(Lextok *, Lextok *);
+void	disambiguate(void);
 void	doq(Symbol *, int, RunList *);
 void	dotag(FILE *, char *);
 void	do_locinits(FILE *);
@@ -344,20 +381,22 @@ void	genunio(void);
 void	ini_struct(Symbol *);
 void	loose_ends(void);
 void	make_atomic(Sequence *, int);
+void	mark_last(void);
 void	match_trail(void);
 void	no_side_effects(char *);
 void	nochan_manip(Lextok *, Lextok *, int);
 void	non_fatal(char *, char *);
-void	ntimes(FILE *, int, int, char *c[]);
+void	ntimes(FILE *, int, int, const char *c[]);
 void	open_seq(int);
 void	p_talk(Element *, int);
-void	pickup_inline(Symbol *, Lextok *);
+void	pickup_inline(Symbol *, Lextok *, Lextok *);
 void	plunk_c_decls(FILE *);
 void	plunk_c_fcts(FILE *);
 void	plunk_expr(FILE *, char *);
-void	plunk_inline(FILE *, char *, int);
+void	plunk_inline(FILE *, char *, int, int);
 void	prehint(Symbol *);
 void	preruse(FILE *, Lextok *);
+void	pretty_print(void);
 void	prune_opts(Lextok *);
 void	pstext(int, char *);
 void	pushbreak(void);
@@ -383,17 +422,23 @@ void	start_claim(int);
 void	struct_name(Lextok *, Symbol *, int, char *);
 void	symdump(void);
 void	symvar(Symbol *);
+void	sync_product(void);
 void	trackchanuse(Lextok *, Lextok *, int);
 void	trackvar(Lextok *, Lextok *);
 void	trackrun(Lextok *);
-void	trapwonly(Lextok *, char *);	/* spin.y and main.c */
+void	trapwonly(Lextok * /* , char * */);	/* spin.y and main.c */
 void	typ2c(Symbol *);
 void	typ_ck(int, int, char *);
 void	undostmnt(Lextok *, int);
 void	unrem_Seq(void);
 void	unskip(int);
-void	varcheck(Element *, Element *);
 void	whoruns(int);
 void	wrapup(int);
 void	yyerror(char *, ...);
+
+extern	int unlink(const char *);
+
+#define TMP_FILE1 "._s_p_i_n_"
+#define TMP_FILE2 "._n_i_p_s_"
+
 #endif