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

diff --git a/sys/src/cmd/spin/pangen7.c b/sys/src/cmd/spin/pangen7.c
new file mode 100644
index 000000000..37f461fbe
--- /dev/null
+++ b/sys/src/cmd/spin/pangen7.c
@@ -0,0 +1,923 @@
+/***** spin: pangen7.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 <assert.h>
+#include "spin.h"
+#include "y.tab.h"
+#include <assert.h>
+#ifndef PC
+#include <unistd.h>
+#endif
+
+extern ProcList	*rdy;
+extern Element *Al_El;
+extern int nclaims, verbose, Strict;
+extern short has_accept;
+
+typedef struct Succ_List Succ_List;
+typedef struct SQueue SQueue;
+typedef struct OneState OneState;
+typedef struct State_Stack State_Stack;
+typedef struct Guard Guard;
+
+struct Succ_List {
+	SQueue	*s;
+	Succ_List *nxt;
+};
+
+struct OneState {
+	int	*combo;	/* the combination of claim states */
+	Succ_List	*succ;	/* list of ptrs to immediate successor states */
+};
+
+struct SQueue {
+	OneState	state;
+	SQueue	*nxt;
+};
+
+struct State_Stack {
+	int *n;
+	State_Stack *nxt;
+};
+
+struct Guard {
+	Lextok *t;
+	Guard *nxt;
+};
+
+static SQueue	*sq, *sd, *render;	/* states move from sq to sd to render to holding */
+static SQueue	*holding, *lasthold;
+static State_Stack *dsts;
+
+static int nst;		/* max nr of states in claims */
+static int *Ist;	/* initial states */
+static int *Nacc;	/* number of accept states in claim */
+static int *Nst;	/* next states */
+static int **reached;	/* n claims x states */
+static int unfolding;	/* to make sure all accept states are reached */
+static int is_accept;	/* remember if the current state is accepting in any claim */
+static int not_printing; /* set during explore_product */
+
+static Element ****matrix;	/* n x two-dimensional arrays state x state */
+static Element **Selfs;	/* self-loop states at end of claims */
+
+static void get_seq(int, Sequence *);
+static void set_el(int n, Element *e);
+static void gen_product(void);
+static void print_state_nm(char *, int *, char *);
+static SQueue *find_state(int *);
+static SQueue *retrieve_state(int *);
+
+static int
+same_state(int *a, int *b)
+{	int i;
+
+	for (i = 0; i < nclaims; i++)
+	{	if (a[i] != b[i])
+		{	return 0;
+	}	}
+	return 1;
+}
+
+static int
+in_stack(SQueue *s, SQueue *in)
+{	SQueue *q;
+
+	for (q = in; q; q = q->nxt)
+	{	if (same_state(q->state.combo, s->state.combo))
+		{	return 1;
+	}	}
+	return 0;
+}
+
+static void
+to_render(SQueue *s)
+{	SQueue *a, *q, *last; /* find in sd/sq and move to render, if not already there */
+	int n;
+
+	for (n = 0; n < nclaims; n++)
+	{	reached[n][ s->state.combo[n] ] |= 2;
+	}
+
+	for (q = render; q; q = q->nxt)
+	{	if (same_state(q->state.combo, s->state.combo))
+		{	return;
+	}	}
+	for (q = holding; q; q = q->nxt)
+	{	if (same_state(q->state.combo, s->state.combo))
+		{	return;
+	}	}
+
+	a = sd;
+more:
+	for (q = a, last = 0; q; last = q, q = q->nxt)
+	{	if (same_state(q->state.combo, s->state.combo))
+		{	if (!last)
+			{	if (a == sd)
+				{	sd = q->nxt;
+				} else if (a == sq)
+				{	sq = q->nxt;
+				} else
+				{	holding = q->nxt;
+				}
+			} else
+			{	last->nxt = q->nxt;
+			}
+			q->nxt = render;
+			render = q;
+			return;
+	}	}
+	if (verbose)
+	{	print_state_nm("looking for: ", s->state.combo, "\n");
+	}
+	(void) find_state(s->state.combo);	/* creates it in sq */
+	if (a != sq)
+	{	a = sq;
+		goto more;
+	}
+	fatal("cannot happen, to_render", 0);
+}
+
+static void
+wrap_text(char *pre, Lextok *t, char *post)
+{
+	printf(pre, (char *) 0);
+	comment(stdout, t, 0);
+	printf(post, (char *) 0);
+}
+
+static State_Stack *
+push_dsts(int *n)
+{	State_Stack *s;
+	int i;
+
+	for (s = dsts; s; s = s->nxt)
+	{	if (same_state(s->n, n))
+		{	if (verbose&64)
+			{	printf("\n");
+				for (s = dsts; s; s = s->nxt)
+				{	print_state_nm("\t", s->n, "\n");
+				}
+				print_state_nm("\t", n, "\n");
+			}
+			return s;
+	}	}
+
+	s = (State_Stack *) emalloc(sizeof(State_Stack));
+	s->n = (int *) emalloc(nclaims * sizeof(int));
+	for (i = 0; i < nclaims; i++)
+		s->n[i] = n[i];
+	s->nxt = dsts;
+	dsts = s;
+	return 0;
+}
+
+static void
+pop_dsts(void)
+{
+	assert(dsts != NULL);
+	dsts = dsts->nxt;
+}
+
+static void
+complete_transition(Succ_List *sl, Guard *g)
+{	Guard *w;
+	int cnt = 0;
+
+	printf("	:: ");
+	for (w = g; w; w = w->nxt)
+	{	if (w->t->ntyp == CONST
+		&&  w->t->val == 1)
+		{	continue;
+		} else if (w->t->ntyp == 'c'
+		&&  w->t->lft->ntyp == CONST
+		&&  w->t->lft->val == 1)
+		{	continue; /* 'true' */
+		}
+
+		if (cnt > 0)
+		{	printf(" && ");
+		}
+		wrap_text("", w->t, "");
+		cnt++;
+	}
+	if (cnt == 0)
+	{	printf("true");
+	}
+	print_state_nm(" -> goto ", sl->s->state.combo, "");
+
+	if (is_accept > 0)
+	{	printf("_U%d\n", (unfolding+1)%nclaims);
+	} else
+	{	printf("_U%d\n", unfolding);
+	}
+}
+
+static void
+state_body(OneState *s, Guard *guard)
+{	Succ_List *sl;
+	State_Stack *y;
+	Guard *g;
+	int i, once;
+
+	for (sl = s->succ; sl; sl = sl->nxt)
+	{	once = 0;
+
+		for (i = 0; i < nclaims; i++)
+		{	Element *e;
+			e = matrix[i][s->combo[i]][sl->s->state.combo[i]];
+
+			/* if one of the claims has a DO or IF move
+			   then pull its target state forward, once
+			 */
+
+			if (!e
+			|| e->n->ntyp == NON_ATOMIC
+			||  e->n->ntyp == DO
+			||  e->n->ntyp == IF)
+			{	s = &(sl->s->state);
+				y = push_dsts(s->combo);
+				if (!y)
+				{	if (once++ == 0)
+					{	assert(s->succ != NULL);
+						state_body(s, guard);
+					}
+					pop_dsts();
+				} else if (!y->nxt)	/* self-loop transition */
+				{	if (!not_printing) printf(" /* self-loop */\n");
+				} else
+				{	/* non_fatal("loop in state body", 0); ** maybe ok */
+				}
+				continue;
+			} else
+			{	g = (Guard *) emalloc(sizeof(Guard));
+				g->t = e->n;
+				g->nxt = guard;
+				guard = g;
+		}	}
+
+		if (guard && !once)
+		{	if (!not_printing) complete_transition(sl, guard);
+			to_render(sl->s);
+	}	}
+}
+
+static struct X {
+	char *s;	int n;
+} spl[] = {
+	{"end",		3 },
+	{"accept",	6 },
+	{0,		0 },
+};
+
+static int slcnt;
+extern Label *labtab;
+
+static ProcList *
+locate_claim(int n)
+{	ProcList *p;
+	int i;
+
+	for (p = rdy, i = 0; p; p = p->nxt, i++) /* find claim name */
+	{	if (i == n)
+		{	break;
+	}	}
+	assert(p && p->b == N_CLAIM);
+
+	return p;
+}
+
+static void
+elim_lab(Element *e)
+{	Label *l, *lst;
+
+	for (l = labtab, lst = NULL; l; lst = l, l = l->nxt)
+	{	if (l->e == e)
+		{	if (lst)
+			{	lst->nxt = l->nxt;
+			} else
+			{	labtab = l->nxt;
+			}
+			break;
+	}	}
+}
+
+static int
+claim_has_accept(ProcList *p)
+{	Label *l;
+
+	for (l = labtab; l; l = l->nxt)
+	{	if (strcmp(l->c->name, p->n->name) == 0
+		&&  strncmp(l->s->name, "accept", 6) == 0)
+		{	return 1;
+	}	}
+	return 0;
+}
+
+static void
+prune_accept(void)
+{	int n;
+
+	for (n = 0; n < nclaims; n++)
+	{	if ((reached[n][Selfs[n]->seqno] & 2) == 0)
+		{	if (verbose)
+			{	printf("claim %d: selfloop not reachable\n", n);
+			}
+			elim_lab(Selfs[n]);
+			Nacc[n] = claim_has_accept(locate_claim(n));
+	}	}
+}
+
+static void
+mk_accepting(int n, Element *e)
+{	ProcList *p;
+	Label *l;
+	int i;
+
+	assert(!Selfs[n]);
+	Selfs[n] = e;
+
+	l = (Label *) emalloc(sizeof(Label));
+	l->s = (Symbol *) emalloc(sizeof(Symbol));
+	l->s->name = "accept00";
+	l->c = (Symbol *) emalloc(sizeof(Symbol));
+	l->uiid = 0;	/* this is not in an inline */
+
+	for (p = rdy, i = 0; p; p = p->nxt, i++) /* find claim name */
+	{	if (i == n)
+		{	l->c->name = p->n->name;
+			break;
+	}	}
+	assert(p && p->b == N_CLAIM);
+	Nacc[n] = 1;
+	has_accept = 1;
+
+	l->e = e;
+	l->nxt = labtab;
+	labtab = l;
+}
+
+static void
+check_special(int *nrs)
+{	ProcList *p;
+	Label *l;
+	int i, j, nmatches;
+	int any_accepts = 0;
+
+	for (i = 0; i < nclaims; i++)
+	{	any_accepts += Nacc[i];
+	}
+
+	is_accept = 0;
+	for (j = 0; spl[j].n; j++) /* 2 special label prefixes */
+	{	nmatches = 0;
+		for (p = rdy, i = 0; p; p = p->nxt, i++) /* check each claim */
+		{	if (p->b != N_CLAIM)
+			{	continue;
+			}
+			/* claim i in state nrs[i], type p->tn, name p->n->name
+			 * either the state has an accept label, or the claim has none,
+			 * so that all its states should be considered accepting
+			 * --- but only if other claims do have accept states!
+			 */
+			if (Strict == 0 && j == 1 && Nacc[i] == 0 && any_accepts > 0)
+			{	if ((verbose&32) && i == unfolding)
+				{	printf("	/* claim %d pseudo-accept */\n", i);
+				}
+				goto is_accepting;
+			}
+			for (l = labtab; l; l = l->nxt)	/* check its labels */
+			{	if (strcmp(l->c->name, p->n->name) == 0  /* right claim */
+				&&  l->e->seqno == nrs[i]		 /* right state */
+				&&  strncmp(l->s->name, spl[j].s, spl[j].n) == 0)
+				{	if (j == 1)	/* accept state */
+					{	char buf[32];
+is_accepting:					if (strchr(p->n->name, ':'))
+						{	sprintf(buf, "N%d", i);
+						} else
+						{	assert(strlen(p->n->name) < sizeof(buf));
+							strcpy(buf, p->n->name);
+						}
+						if (unfolding == 0 && i == 0)
+						{	if (!not_printing)
+							printf("%s_%s_%d:\n",	/* true accept */
+								spl[j].s, buf, slcnt++);
+						} else if (verbose&32)
+						{	if (!not_printing)
+							printf("%s_%s%d:\n",
+								buf, spl[j].s, slcnt++);
+						}
+						if (i == unfolding)
+						{	is_accept++; /* move to next unfolding */
+						}
+					} else
+					{	nmatches++;
+					}
+					break;
+		}	}	}
+		if (j == 0 && nmatches == nclaims)	/* end-state */
+		{	if (!not_printing)
+			{	printf("%s%d:\n", spl[j].s, slcnt++);
+	}	}	}
+}
+
+static int
+render_state(SQueue *q)
+{
+	if (!q || !q->state.succ)
+	{	if (verbose&64)
+		{	printf("	no exit\n");
+		}
+		return 0;
+	}
+
+	check_special(q->state.combo); /* accept or end-state labels */
+
+	dsts = (State_Stack *) 0;
+	push_dsts(q->state.combo);	/* to detect loops */
+
+	if (!not_printing)
+	{	print_state_nm("", q->state.combo, "");	/* the name */
+		printf("_U%d:\n\tdo\n", unfolding);
+	}
+
+	state_body(&(q->state), (Guard *) 0);
+
+	if (!not_printing)
+	{	printf("\tod;\n");
+	}
+	pop_dsts();
+	return 1;
+}
+
+static void
+explore_product(void)
+{	SQueue *q;
+
+	/* all states are in the sd queue */
+
+	q = retrieve_state(Ist);	/* retrieve from the sd q */
+	q->nxt = render;		/* put in render q */
+	render = q;
+	do {
+		q = render;
+		render = render->nxt;
+		q->nxt = 0;		/* remove from render q */
+
+		if (verbose&64)
+		{	print_state_nm("explore: ", q->state.combo, "\n");
+		}
+
+		not_printing = 1;
+		render_state(q);	/* may add new states */
+		not_printing = 0;
+
+		if (lasthold)
+		{	lasthold->nxt = q;
+			lasthold = q;
+		} else
+		{	holding = lasthold = q;
+		}
+	} while (render);
+	assert(!dsts);
+	
+}
+
+static void
+print_product(void)
+{	SQueue *q;
+	int cnt;
+
+	if (unfolding == 0)
+	{	printf("never Product {\n");	/* name expected by iSpin */
+		q = find_state(Ist);	/* should find it in the holding q */
+		assert(q != NULL);
+		q->nxt = holding;	/* put it at the front */
+		holding = q;
+	}
+	render = holding;
+	holding = lasthold = 0;
+
+	printf("/* ============= U%d ============= */\n", unfolding);
+	cnt = 0;
+	do {
+		q = render;
+		render = render->nxt;
+		q->nxt = 0;
+		if (verbose&64)
+		{	print_state_nm("print: ", q->state.combo, "\n");
+		}
+		cnt += render_state(q);
+
+		if (lasthold)
+		{	lasthold->nxt = q;
+			lasthold = q;
+		} else
+		{	holding = lasthold = q;
+		}
+	} while (render);
+	assert(!dsts);
+
+	if (cnt == 0)
+	{	printf("	0;\n");
+	}
+
+	if (unfolding == nclaims-1)
+	{	printf("}\n");
+	}
+}
+
+static void
+prune_dead(void)
+{	Succ_List *sl, *last;
+	SQueue *q;
+	int cnt;
+
+	do {	cnt = 0;
+		for (q = sd; q; q = q->nxt)
+		{	/* if successor is deadend, remove it
+			 * unless it's a move to the end-state of the claim
+			 */
+			last = (Succ_List *) 0;
+			for (sl = q->state.succ; sl; last = sl, sl = sl->nxt)
+			{	if (!sl->s->state.succ)	/* no successor */
+				{	if (!last)
+					{	q->state.succ = sl->nxt;
+					} else
+					{	last->nxt = sl->nxt;
+					}
+					cnt++;
+		}	}	}
+	} while (cnt > 0);
+}
+
+static void
+print_raw(void)
+{	int i, j, n;
+
+	printf("#if 0\n");
+	for (n = 0; n < nclaims; n++)
+	{	printf("C%d:\n", n);
+		for (i = 0; i < nst; i++)
+		{	if (reached[n][i])
+			for (j = 0; j < nst; j++)
+			{	if (matrix[n][i][j])
+				{	if (reached[n][i] & 2) printf("+");
+					if (i == Ist[n]) printf("*");
+					printf("\t%d", i);
+					wrap_text(" -[", matrix[n][i][j]->n, "]->\t");
+					printf("%d\n", j);
+	}	}	}	}
+	printf("#endif\n\n");
+	fflush(stdout);
+}
+
+void
+sync_product(void)
+{	ProcList *p;
+	Element *e;
+	int n, i;
+
+	if (nclaims <= 1) return;
+
+	(void) unlink("pan.pre");
+
+	Ist  = (int *) emalloc(sizeof(int) * nclaims);
+	Nacc = (int *) emalloc(sizeof(int) * nclaims);
+	Nst  = (int *) emalloc(sizeof(int) * nclaims);
+	reached = (int **) emalloc(sizeof(int *) * nclaims);
+	Selfs   = (Element **) emalloc(sizeof(Element *) * nclaims);
+	matrix  = (Element ****) emalloc(sizeof(Element ***) * nclaims); /* claims */
+
+	for (p = rdy, i = 0; p; p = p->nxt, i++)
+	{	if (p->b == N_CLAIM)
+		{	nst = max(p->s->maxel, nst);
+			Nacc[i] = claim_has_accept(p);
+	}	}
+
+	for (n = 0; n < nclaims; n++)
+	{	reached[n] = (int *) emalloc(sizeof(int) * nst);
+		matrix[n] = (Element ***) emalloc(sizeof(Element **) * nst);	/* rows */
+		for (i = 0; i < nst; i++)					/* cols */
+		{	matrix[n][i] = (Element **) emalloc(sizeof(Element *) * nst);
+	}	}
+
+	for (e = Al_El; e; e = e->Nxt)
+	{	e->status &= ~DONE;
+	}
+
+	for (p = rdy, n=0; p; p = p->nxt, n++)
+	{	if (p->b == N_CLAIM)
+		{	/* fill in matrix[n] */
+			e = p->s->frst;
+			Ist[n] = huntele(e, e->status, -1)->seqno;
+
+			reached[n][Ist[n]] = 1|2;
+			get_seq(n, p->s);
+	}	}
+
+	if (verbose)	/* show only the input automata */
+	{	print_raw();
+	}
+
+	gen_product();	/* create product automaton */
+}
+
+static int
+nxt_trans(int n, int cs, int frst)
+{	int j;
+
+	for (j = frst; j < nst; j++)
+	{	if (reached[n][cs]
+		&&  matrix[n][cs][j])
+		{	return j;
+	}	}
+	return -1;
+}
+
+static void
+print_state_nm(char *p, int *s, char *a)
+{	int i;
+	printf("%sP", p);
+	for (i = 0; i < nclaims; i++)
+	{	printf("_%d", s[i]);
+	}
+	printf("%s", a);
+}
+
+static void
+create_transition(OneState *s, SQueue *it)
+{	int n, from, upto;
+	int *F = s->combo;
+	int *T = it->state.combo;
+	Succ_List *sl;
+	Lextok *t;
+
+	if (verbose&64)
+	{	print_state_nm("", F, " ");
+		print_state_nm("-> ", T, "\t");
+	}
+
+	/* check if any of the claims is blocked */
+	/* which makes the state a dead-end */
+	for (n = 0; n < nclaims; n++)
+	{	from = F[n];
+		upto = T[n];
+		t = matrix[n][from][upto]->n;
+		if (verbose&64)
+		{	wrap_text("", t, " ");
+		}
+		if (t->ntyp == 'c'
+		&&  t->lft->ntyp == CONST)
+		{	if (t->lft->val == 0)	/* i.e., false */
+			{	goto done;
+	}	}	}
+
+	sl = (Succ_List *) emalloc(sizeof(Succ_List));
+	sl->s = it;
+	sl->nxt = s->succ;
+	s->succ = sl;
+done:
+	if (verbose&64)
+	{	printf("\n");
+	}
+}
+
+static SQueue *
+find_state(int *cs)
+{	SQueue *nq, *a = sq;
+	int i;
+
+again:	/* check in nq, sq, and then in the render q */
+	for (nq = a; nq; nq = nq->nxt)
+	{	if (same_state(nq->state.combo, cs))
+		{	return nq;	/* found */
+	}	}
+	if (a == sq && sd)
+	{	a = sd;
+		goto again; /* check the other stack too */
+	} else if (a == sd && render)
+	{	a = render;
+		goto again;
+	}
+
+	nq = (SQueue *) emalloc(sizeof(SQueue));
+	nq->state.combo = (int *) emalloc(nclaims * sizeof(int));
+	for (i = 0; i < nclaims; i++)
+	{	nq->state.combo[i] = cs[i];
+	}
+	nq->nxt = sq;	/* add to sq stack */
+	sq = nq;
+
+	return nq;
+}
+
+static SQueue *
+retrieve_state(int *s)
+{	SQueue *nq, *last = NULL;
+
+	for (nq = sd; nq; last = nq, nq = nq->nxt)
+	{	if (same_state(nq->state.combo, s))
+		{	if (last)
+			{	last->nxt = nq->nxt;
+			} else
+			{	sd = nq->nxt;	/* 6.4.0: was sd = nq */
+			}
+			return nq;	/* found */
+	}	}
+
+	fatal("cannot happen: retrieve_state", 0);
+	return (SQueue *) 0;
+}
+
+static void
+all_successors(int n, OneState *cur)
+{	int i, j = 0;
+
+	if (n >= nclaims)
+	{	create_transition(cur, find_state(Nst));
+	} else
+	{	i = cur->combo[n];
+		for (;;)
+		{	j = nxt_trans(n, i, j);
+			if (j < 0) break;
+			Nst[n] = j;
+			all_successors(n+1, cur);
+			j++;
+	}	}
+}
+
+static void
+gen_product(void)
+{	OneState *cur_st;
+	SQueue *q;
+
+	find_state(Ist);	/* create initial state */
+
+	while (sq)
+	{	if (in_stack(sq, sd))
+		{	sq = sq->nxt;
+			continue;
+		}
+		cur_st = &(sq->state);
+
+		q = sq;
+		sq = sq->nxt;	/* delete from sq stack */
+		q->nxt = sd;	/* and move to done stack */
+		sd = q;
+
+		all_successors(0, cur_st);
+	}
+	/* all states are in the sd queue now */
+	prune_dead();
+	explore_product();	/* check if added accept-self-loops are reachable */
+	prune_accept();
+
+	if (verbose)
+	{	print_raw();
+	}
+
+	/* PM: merge states with identical successor lists */
+
+	/* all outgoing transitions from accept-states
+	   from claim n in copy n connect to states in copy (n+1)%nclaims
+	   only accept states from claim 0 in copy 0 are true accept states
+	   in the product
+
+	   PM: what about claims that have no accept states (e.g., restrictions)
+	*/
+
+	for (unfolding = 0; unfolding < nclaims; unfolding++)
+	{	print_product();
+	}
+}
+
+static void
+t_record(int n, Element *e, Element *g)
+{	int from = e->seqno, upto = g?g->seqno:0;
+
+	assert(from >= 0 && from < nst);
+	assert(upto >= 0 && upto < nst);
+
+	matrix[n][from][upto] = e;
+	reached[n][upto] |= 1;
+}
+
+static void
+get_sub(int n, Element *e)
+{
+	if (e->n->ntyp == D_STEP
+	||  e->n->ntyp == ATOMIC)
+	{	fatal("atomic or d_step in never claim product", 0);
+	} 
+	/* NON_ATOMIC */
+	e->n->sl->this->last->nxt = e->nxt;
+	get_seq(n, e->n->sl->this);
+
+	t_record(n, e, e->n->sl->this->frst);
+
+}
+
+static void
+set_el(int n, Element *e)
+{	Element *g;
+
+	if (e->n->ntyp == '@')	/* change to self-loop */
+	{	e->n->ntyp = CONST;
+		e->n->val = 1;	/* true */
+		e->nxt = e;
+		g = e;
+		mk_accepting(n, e);
+	} else
+
+	if (e->n->ntyp == GOTO)
+	{	g = get_lab(e->n, 1);
+		g = huntele(g, e->status, -1);
+	} else if (e->nxt)
+	{	g = huntele(e->nxt, e->status, -1);
+	} else
+	{	g = NULL;
+	}
+
+	t_record(n, e, g);
+}
+
+static void
+get_seq(int n, Sequence *s)
+{	SeqList *h;
+	Element *e;
+
+	e = huntele(s->frst, s->frst->status, -1);
+	for ( ; e; e = e->nxt)
+	{	if (e->status & DONE)
+		{	goto checklast;
+		}
+		e->status |= DONE;
+
+		if (e->n->ntyp == UNLESS)
+		{	fatal("unless stmnt in never claim product", 0);
+		}
+
+		if (e->sub)	/* IF or DO */
+		{	Lextok *x = NULL;
+			Lextok *y = NULL;
+			Lextok *haselse = NULL;
+
+			for (h = e->sub; h; h = h->nxt)
+			{	Lextok *t = h->this->frst->n;
+				if (t->ntyp == ELSE)
+				{	if (verbose&64) printf("else at line %d\n", t->ln);
+					haselse = t;
+					continue;
+				}
+				if (t->ntyp != 'c')
+				{	fatal("product, 'else' combined with non-condition", 0);
+				}
+
+				if (t->lft->ntyp == CONST	/* true */
+				&&  t->lft->val == 1
+				&&  y == NULL)
+				{	y = nn(ZN, CONST, ZN, ZN);
+					y->val = 0;
+				} else
+				{	if (!x)
+						x = t;
+					else
+						x = nn(ZN, OR, x, t);
+					if (verbose&64)
+					{	wrap_text(" [", x, "]\n");
+			}	}	}
+			if (haselse)
+			{	if (!y)
+				{	y = nn(ZN, '!', x, ZN);
+				}
+				if (verbose&64)
+				{	wrap_text(" [else: ", y, "]\n");
+				}
+				haselse->ntyp = 'c';	/* replace else */
+				haselse->lft = y;
+			}
+
+			for (h = e->sub; h; h = h->nxt)
+			{	t_record(n, e, h->this->frst);
+				get_seq(n, h->this);
+			}
+		} else
+		{	if (e->n->ntyp == ATOMIC
+			||  e->n->ntyp == D_STEP
+			||  e->n->ntyp == NON_ATOMIC)
+			{	get_sub(n, e);
+			} else 
+			{	set_el(n, e);
+			}
+		}
+checklast:	if (e == s->last)
+			break;
+	}
+}