Import sources from 2011-03-30 iso image

1 files changed, 2352 insertions, 0 deletions

diff --git a/sys/src/cmd/spin/pangen6.c b/sys/src/cmd/spin/pangen6.c
new file mode 100755
index 000000000..50b587749
--- /dev/null
+++ b/sys/src/cmd/spin/pangen6.c
@@ -0,0 +1,2352 @@
+/***** spin: pangen6.c *****/
+
+/* Copyright (c) 2000-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            */
+
+/* Abstract syntax tree analysis / slicing (spin option -A) */
+/* AST_store stores the fsms's for each proctype            */
+/* AST_track keeps track of variables used in properties    */
+/* AST_slice starts the slicing algorithm                   */
+/*      it first collects more info and then calls          */
+/*      AST_criteria to process the slice criteria          */
+
+#include "spin.h"
+#include "y.tab.h"
+
+extern Ordered	 *all_names;
+extern FSM_use   *use_free;
+extern FSM_state **fsm_tbl;
+extern FSM_state *fsm;
+extern int	 verbose, o_max;
+
+static FSM_trans *cur_t;
+static FSM_trans *expl_par;
+static FSM_trans *expl_var;
+static FSM_trans *explicit;
+
+extern void rel_use(FSM_use *);
+
+#define ulong	unsigned long
+
+typedef struct Pair {
+	FSM_state	*h;
+	int		b;
+	struct Pair	*nxt;
+} Pair;
+
+typedef struct AST {
+	ProcList *p;		/* proctype decl */
+	int	i_st;		/* start state */
+	int	nstates, nwords;
+	int	relevant;
+	Pair	*pairs;		/* entry and exit nodes of proper subgraphs */
+	FSM_state *fsm;		/* proctype body */
+	struct AST *nxt;	/* linked list */
+} AST;
+
+typedef struct RPN {		/* relevant proctype names */
+	Symbol	*rn;
+	struct RPN *nxt;
+} RPN;
+
+typedef struct ALIAS {		/* channel aliasing info */
+	Lextok	*cnm;		/* this chan */
+	int	origin;		/* debugging - origin of the alias */
+	struct ALIAS	*alias;	/* can be an alias for these other chans */
+	struct ALIAS	*nxt;	/* linked list */
+} ALIAS;
+
+typedef struct ChanList {
+	Lextok *s;		/* containing stmnt */
+	Lextok *n;		/* point of reference - could be struct */
+	struct ChanList *nxt;	/* linked list */
+} ChanList;
+
+/* a chan alias can be created in one of three ways:
+	assignement to chan name
+		a = b -- a is now an alias for b
+	passing chan name as parameter in run
+		run x(b) -- proctype x(chan a)
+	passing chan name through channel
+		x!b -- x?a
+ */
+
+#define USE		1
+#define DEF		2
+#define DEREF_DEF	4
+#define DEREF_USE	8
+
+static AST	*ast;
+static ALIAS	*chalcur;
+static ALIAS	*chalias;
+static ChanList	*chanlist;
+static Slicer	*slicer;
+static Slicer	*rel_vars;	/* all relevant variables */
+static int	AST_Changes;
+static int	AST_Round;
+static FSM_state no_state;
+static RPN	*rpn;
+static int	in_recv = 0;
+
+static int	AST_mutual(Lextok *, Lextok *, int);
+static void	AST_dominant(void);
+static void	AST_hidden(void);
+static void	AST_setcur(Lextok *);
+static void	check_slice(Lextok *, int);
+static void	curtail(AST *);
+static void	def_use(Lextok *, int);
+static void	name_AST_track(Lextok *, int);
+static void	show_expl(void);
+
+static int
+AST_isini(Lextok *n)	/* is this an initialized channel */
+{	Symbol *s;
+
+	if (!n || !n->sym) return 0;
+
+	s = n->sym;
+
+	if (s->type == CHAN)
+		return (s->ini->ntyp == CHAN); /* freshly instantiated */
+
+	if (s->type == STRUCT && n->rgt)
+		return AST_isini(n->rgt->lft);
+
+	return 0;
+}
+
+static void
+AST_var(Lextok *n, Symbol *s, int toplevel)
+{
+	if (!s) return;
+
+	if (toplevel)
+	{	if (s->context && s->type)
+			printf(":%s:L:", s->context->name);
+		else
+			printf("G:");
+	}
+	printf("%s", s->name); /* array indices ignored */
+
+	if (s->type == STRUCT && n && n->rgt && n->rgt->lft)
+	{	printf(":");
+		AST_var(n->rgt->lft, n->rgt->lft->sym, 0);
+	}
+}
+
+static void
+name_def_indices(Lextok *n, int code)
+{
+	if (!n || !n->sym) return;
+
+	if (n->sym->nel != 1)
+		def_use(n->lft, code);		/* process the index */
+
+	if (n->sym->type == STRUCT		/* and possible deeper ones */
+	&&  n->rgt)
+		name_def_indices(n->rgt->lft, code);
+}
+
+static void
+name_def_use(Lextok *n, int code)
+{	FSM_use *u;
+
+	if (!n) return;
+
+	if ((code&USE)
+	&&  cur_t->step
+	&&  cur_t->step->n)
+	{	switch (cur_t->step->n->ntyp) {
+		case 'c': /* possible predicate abstraction? */
+			n->sym->colnr |= 2; /* yes */
+			break;
+		default:
+			n->sym->colnr |= 1; /* no  */
+			break;
+		}
+	}
+
+	for (u = cur_t->Val[0]; u; u = u->nxt)
+		if (AST_mutual(n, u->n, 1)
+		&&  u->special == code)
+			return;
+
+	if (use_free)
+	{	u = use_free;
+		use_free = use_free->nxt;
+	} else
+		u = (FSM_use *) emalloc(sizeof(FSM_use));
+	
+	u->n = n;
+	u->special = code;
+	u->nxt = cur_t->Val[0];
+	cur_t->Val[0] = u;
+
+	name_def_indices(n, USE|(code&(~DEF)));	/* not def, but perhaps deref */
+}
+
+static void
+def_use(Lextok *now, int code)
+{	Lextok *v;
+
+	if (now)
+	switch (now->ntyp) {
+	case '!':	
+	case UMIN:	
+	case '~':
+	case 'c':
+	case ENABLED:
+	case ASSERT:
+	case EVAL:
+		def_use(now->lft, USE|code);
+		break;
+
+	case LEN:
+	case FULL:
+	case EMPTY:
+	case NFULL:
+	case NEMPTY:
+		def_use(now->lft, DEREF_USE|USE|code);
+		break;
+
+	case '/':
+	case '*':
+	case '-':
+	case '+':
+	case '%':
+	case '&':
+	case '^':
+	case '|':
+	case LE:
+	case GE:
+	case GT:
+	case LT:
+	case NE:
+	case EQ:
+	case OR:
+	case AND:
+	case LSHIFT:
+	case RSHIFT:
+		def_use(now->lft, USE|code);
+		def_use(now->rgt, USE|code); 
+		break;
+
+	case ASGN:
+		def_use(now->lft, DEF|code);
+		def_use(now->rgt, USE|code);
+		break;
+
+	case TYPE:	/* name in parameter list */
+		name_def_use(now, code);
+		break;
+
+	case NAME:
+		name_def_use(now, code);
+		break;
+
+	case RUN:
+		name_def_use(now, USE);			/* procname - not really needed */
+		for (v = now->lft; v; v = v->rgt)
+			def_use(v->lft, USE);		/* params */
+		break;
+
+	case 's':
+		def_use(now->lft, DEREF_DEF|DEREF_USE|USE|code);
+		for (v = now->rgt; v; v = v->rgt)
+			def_use(v->lft, USE|code);
+		break;
+
+	case 'r':
+		def_use(now->lft, DEREF_DEF|DEREF_USE|USE|code);
+		for (v = now->rgt; v; v = v->rgt)
+		{	if (v->lft->ntyp == EVAL)
+				def_use(v->lft, code);	/* will add USE */
+			else if (v->lft->ntyp != CONST)
+				def_use(v->lft, DEF|code);
+		}
+		break;
+
+	case 'R':
+		def_use(now->lft, DEREF_USE|USE|code);
+		for (v = now->rgt; v; v = v->rgt)
+		{	if (v->lft->ntyp == EVAL)
+				def_use(v->lft, code); /* will add USE */
+		}
+		break;
+
+	case '?':
+		def_use(now->lft, USE|code);
+		if (now->rgt)
+		{	def_use(now->rgt->lft, code);
+			def_use(now->rgt->rgt, code);
+		}
+		break;	
+
+	case PRINT:
+		for (v = now->lft; v; v = v->rgt)
+			def_use(v->lft, USE|code);
+		break;
+
+	case PRINTM:
+		def_use(now->lft, USE);
+		break;
+
+	case CONST:
+	case ELSE:	/* ? */
+	case NONPROGRESS:
+	case PC_VAL:
+	case   'p':
+	case   'q':
+		break;
+
+	case   '.':
+	case  GOTO:
+	case BREAK:
+	case   '@':
+	case D_STEP:
+	case ATOMIC:
+	case NON_ATOMIC:
+	case IF:
+	case DO:
+	case UNLESS:
+	case TIMEOUT:
+	case C_CODE:
+	case C_EXPR:
+	default:
+		break;
+	}
+}
+
+static int
+AST_add_alias(Lextok *n, int nr)
+{	ALIAS *ca;
+	int res;
+
+	for (ca = chalcur->alias; ca; ca = ca->nxt)
+		if (AST_mutual(ca->cnm, n, 1))
+		{	res = (ca->origin&nr);
+			ca->origin |= nr;	/* 1, 2, or 4 - run, asgn, or rcv */
+			return (res == 0);	/* 0 if already there with same origin */
+		}
+
+	ca = (ALIAS *) emalloc(sizeof(ALIAS));
+	ca->cnm = n;
+	ca->origin = nr;
+	ca->nxt = chalcur->alias;
+	chalcur->alias = ca;
+	return 1;
+}
+
+static void
+AST_run_alias(char *pn, char *s, Lextok *t, int parno)
+{	Lextok *v;
+	int cnt;
+
+	if (!t) return;
+
+	if (t->ntyp == RUN)
+	{	if (strcmp(t->sym->name, s) == 0)
+		for (v = t->lft, cnt = 1; v; v = v->rgt, cnt++)
+			if (cnt == parno)
+			{	AST_add_alias(v->lft, 1); /* RUN */
+				break;
+			}
+	} else
+	{	AST_run_alias(pn, s, t->lft, parno);
+		AST_run_alias(pn, s, t->rgt, parno);
+	}
+}
+
+static void
+AST_findrun(char *s, int parno)
+{	FSM_state *f;
+	FSM_trans *t;
+	AST *a;
+
+	for (a = ast; a; a = a->nxt)		/* automata       */
+	for (f = a->fsm; f; f = f->nxt)		/* control states */
+	for (t = f->t; t; t = t->nxt)		/* transitions    */
+	{	if (t->step)
+		AST_run_alias(a->p->n->name, s, t->step->n, parno);
+	}
+}
+
+static void
+AST_par_chans(ProcList *p)	/* find local chan's init'd to chan passed as param */
+{	Ordered	*walk;
+	Symbol	*sp;
+
+	for (walk = all_names; walk; walk = walk->next)
+	{	sp = walk->entry;
+		if (sp
+		&&  sp->context
+		&&  strcmp(sp->context->name, p->n->name) == 0
+		&&  sp->Nid >= 0	/* not itself a param */
+		&&  sp->type == CHAN
+		&&  sp->ini->ntyp == NAME)	/* != CONST and != CHAN */
+		{	Lextok *x = nn(ZN, 0, ZN, ZN);
+			x->sym = sp;
+			AST_setcur(x);
+			AST_add_alias(sp->ini, 2);	/* ASGN */
+	}	}
+}
+
+static void
+AST_para(ProcList *p)
+{	Lextok *f, *t, *c;
+	int cnt = 0;
+
+	AST_par_chans(p);
+
+	for (f = p->p; f; f = f->rgt) 		/* list of types */
+	for (t = f->lft; t; t = t->rgt)
+	{	if (t->ntyp != ',')
+			c = t;
+		else
+			c = t->lft;	/* expanded struct */
+
+		cnt++;
+		if (Sym_typ(c) == CHAN)
+		{	ALIAS *na = (ALIAS *) emalloc(sizeof(ALIAS));
+
+			na->cnm = c;
+			na->nxt = chalias;
+			chalcur = chalias = na;
+#if 0
+			printf("%s -- (par) -- ", p->n->name);
+			AST_var(c, c->sym, 1);
+			printf(" => <<");
+#endif
+			AST_findrun(p->n->name, cnt);
+#if 0
+			printf(">>\n");
+#endif
+		}
+	}
+}
+
+static void
+AST_haschan(Lextok *c)
+{
+	if (!c) return;
+	if (Sym_typ(c) == CHAN)
+	{	AST_add_alias(c, 2);	/* ASGN */
+#if 0
+		printf("<<");
+		AST_var(c, c->sym, 1);
+		printf(">>\n");
+#endif
+	} else
+	{	AST_haschan(c->rgt);
+		AST_haschan(c->lft);
+	}
+}
+
+static int
+AST_nrpar(Lextok *n) /* 's' or 'r' */
+{	Lextok *m;
+	int j = 0;
+
+	for (m = n->rgt; m; m = m->rgt)
+		j++;
+	return j;
+}
+
+static int
+AST_ord(Lextok *n, Lextok *s)
+{	Lextok *m;
+	int j = 0;
+
+	for (m = n->rgt; m; m = m->rgt)
+	{	j++;
+		if (s->sym == m->lft->sym)
+			return j;
+	}
+	return 0;
+}
+
+#if 0
+static void
+AST_ownership(Symbol *s)
+{
+	if (!s) return;
+	printf("%s:", s->name);
+	AST_ownership(s->owner);
+}
+#endif
+
+static int
+AST_mutual(Lextok *a, Lextok *b, int toplevel)
+{	Symbol *as, *bs;
+
+	if (!a && !b) return 1;
+
+	if (!a || !b) return 0;
+
+	as = a->sym;
+	bs = b->sym;
+
+	if (!as || !bs) return 0;
+
+	if (toplevel && as->context != bs->context)
+		return 0;
+
+	if (as->type != bs->type)
+		return 0;
+
+	if (strcmp(as->name, bs->name) != 0)
+		return 0;
+
+	if (as->type == STRUCT && a->rgt && b->rgt)
+		return AST_mutual(a->rgt->lft, b->rgt->lft, 0);
+
+	return 1;
+}
+
+static void
+AST_setcur(Lextok *n)	/* set chalcur */
+{	ALIAS *ca;
+
+	for (ca = chalias; ca; ca = ca->nxt)
+		if (AST_mutual(ca->cnm, n, 1))	/* if same chan */
+		{	chalcur = ca;
+			return;
+		}
+
+	ca = (ALIAS *) emalloc(sizeof(ALIAS));
+	ca->cnm = n;
+	ca->nxt = chalias;
+	chalcur = chalias = ca;
+}
+
+static void
+AST_other(AST *a)	/* check chan params in asgns and recvs */
+{	FSM_state *f;
+	FSM_trans *t;
+	FSM_use *u;
+	ChanList *cl;
+
+	for (f = a->fsm; f; f = f->nxt)		/* control states */
+	for (t = f->t; t; t = t->nxt)		/* transitions    */
+	for (u = t->Val[0]; u; u = u->nxt)	/* def/use info   */
+		if (Sym_typ(u->n) == CHAN
+		&&  (u->special&DEF))		/* def of chan-name  */
+		{	AST_setcur(u->n);
+			switch (t->step->n->ntyp) {
+			case ASGN:
+				AST_haschan(t->step->n->rgt);
+				break;
+			case 'r':
+				/* guess sends where name may originate */
+				for (cl = chanlist; cl; cl = cl->nxt)	/* all sends */
+				{	int a = AST_nrpar(cl->s);
+					int b = AST_nrpar(t->step->n);
+					if (a != b)	/* matching nrs of params */
+						continue;
+
+					a = AST_ord(cl->s, cl->n);
+					b = AST_ord(t->step->n, u->n);
+					if (a != b)	/* same position in parlist */
+						continue;
+
+					AST_add_alias(cl->n, 4); /* RCV assume possible match */
+				}
+				break;
+			default:
+				printf("type = %d\n", t->step->n->ntyp);
+				non_fatal("unexpected chan def type", (char *) 0);
+				break;
+		}	}
+}
+
+static void
+AST_aliases(void)
+{	ALIAS *na, *ca;
+
+	for (na = chalias; na; na = na->nxt)
+	{	printf("\npossible aliases of ");
+		AST_var(na->cnm, na->cnm->sym, 1);
+		printf("\n\t");
+		for (ca = na->alias; ca; ca = ca->nxt)
+		{	if (!ca->cnm->sym)
+				printf("no valid name ");
+			else
+				AST_var(ca->cnm, ca->cnm->sym, 1);
+			printf("<");
+			if (ca->origin & 1) printf("RUN ");
+			if (ca->origin & 2) printf("ASGN ");
+			if (ca->origin & 4) printf("RCV ");
+			printf("[%s]", AST_isini(ca->cnm)?"Initzd":"Name");
+			printf(">");
+			if (ca->nxt) printf(", ");
+		}
+		printf("\n");
+	}
+	printf("\n");
+}
+
+static void
+AST_indirect(FSM_use *uin, FSM_trans *t, char *cause, char *pn)
+{	FSM_use *u;
+
+	/* this is a newly discovered relevant statement */
+	/* all vars it uses to contribute to its DEF are new criteria */
+
+	if (!(t->relevant&1)) AST_Changes++;
+
+	t->round = AST_Round;
+	t->relevant = 1;
+
+	if ((verbose&32) && t->step)
+	{	printf("\tDR %s [[ ", pn);
+		comment(stdout, t->step->n, 0);
+		printf("]]\n\t\tfully relevant %s", cause);
+		if (uin) { printf(" due to "); AST_var(uin->n, uin->n->sym, 1); }
+		printf("\n");
+	}
+	for (u = t->Val[0]; u; u = u->nxt)
+		if (u != uin
+		&& (u->special&(USE|DEREF_USE)))
+		{	if (verbose&32)
+			{	printf("\t\t\tuses(%d): ", u->special);
+				AST_var(u->n, u->n->sym, 1);
+				printf("\n");
+			}
+			name_AST_track(u->n, u->special);	/* add to slice criteria */
+		}
+}
+
+static void
+def_relevant(char *pn, FSM_trans *t, Lextok *n, int ischan)
+{	FSM_use *u;
+	ALIAS *na, *ca;
+	int chanref;
+
+	/* look for all DEF's of n
+	 *	mark those stmnts relevant
+	 *	mark all var USEs in those stmnts as criteria
+	 */
+
+	if (n->ntyp != ELSE)
+	for (u = t->Val[0]; u; u = u->nxt)
+	{	chanref = (Sym_typ(u->n) == CHAN);
+
+		if (ischan != chanref			/* no possible match  */
+		|| !(u->special&(DEF|DEREF_DEF)))	/* not a def */
+			continue;
+
+		if (AST_mutual(u->n, n, 1))
+		{	AST_indirect(u, t, "(exact match)", pn);
+			continue;
+		}
+
+		if (chanref)
+		for (na = chalias; na; na = na->nxt)
+		{	if (!AST_mutual(u->n, na->cnm, 1))
+				continue;
+			for (ca = na->alias; ca; ca = ca->nxt)
+				if (AST_mutual(ca->cnm, n, 1)
+				&&  AST_isini(ca->cnm))	
+				{	AST_indirect(u, t, "(alias match)", pn);
+					break;
+				}
+			if (ca) break;
+	}	}	
+}
+
+static void
+AST_relevant(Lextok *n)
+{	AST *a;
+	FSM_state *f;
+	FSM_trans *t;
+	int ischan;
+
+	/* look for all DEF's of n
+	 *	mark those stmnts relevant
+	 *	mark all var USEs in those stmnts as criteria
+	 */
+
+	if (!n) return;
+	ischan = (Sym_typ(n) == CHAN);
+
+	if (verbose&32)
+	{	printf("<<ast_relevant (ntyp=%d) ", n->ntyp);
+		AST_var(n, n->sym, 1);
+		printf(">>\n");
+	}
+
+	for (t = expl_par; t; t = t->nxt)	/* param assignments */
+	{	if (!(t->relevant&1))
+		def_relevant(":params:", t, n, ischan);
+	}
+
+	for (t = expl_var; t; t = t->nxt)
+	{	if (!(t->relevant&1))		/* var inits */
+		def_relevant(":vars:", t, n, ischan);
+	}
+
+	for (a = ast; a; a = a->nxt)		/* all other stmnts */
+	{	if (strcmp(a->p->n->name, ":never:") != 0
+		&&  strcmp(a->p->n->name, ":trace:") != 0
+		&&  strcmp(a->p->n->name, ":notrace:") != 0)
+		for (f = a->fsm; f; f = f->nxt)
+		for (t = f->t; t; t = t->nxt)
+		{	if (!(t->relevant&1))
+			def_relevant(a->p->n->name, t, n, ischan);
+	}	}
+}
+
+static int
+AST_relpar(char *s)
+{	FSM_trans *t, *T;
+	FSM_use *u;
+
+	for (T = expl_par; T; T = (T == expl_par)?expl_var: (FSM_trans *) 0)
+	for (t = T; t; t = t->nxt)
+	{	if (t->relevant&1)
+		for (u = t->Val[0]; u; u = u->nxt)
+		{	if (u->n->sym->type
+			&&  u->n->sym->context
+			&&  strcmp(u->n->sym->context->name, s) == 0)
+			{
+				if (verbose&32)
+				{	printf("proctype %s relevant, due to symbol ", s);
+					AST_var(u->n, u->n->sym, 1);
+					printf("\n");
+				}
+				return 1;
+	}	}	}
+	return 0;
+}
+
+static void
+AST_dorelevant(void)
+{	AST *a;
+	RPN *r;
+
+	for (r = rpn; r; r = r->nxt)
+	{	for (a = ast; a; a = a->nxt)
+			if (strcmp(a->p->n->name, r->rn->name) == 0)
+			{	a->relevant |= 1;
+				break;
+			}
+		if (!a)
+		fatal("cannot find proctype %s", r->rn->name);
+	}		
+}
+
+static void
+AST_procisrelevant(Symbol *s)
+{	RPN *r;
+	for (r = rpn; r; r = r->nxt)
+		if (strcmp(r->rn->name, s->name) == 0)
+			return;
+	r = (RPN *) emalloc(sizeof(RPN));
+	r->rn = s;
+	r->nxt = rpn;
+	rpn = r;
+}
+
+static int
+AST_proc_isrel(char *s)
+{	AST *a;
+
+	for (a = ast; a; a = a->nxt)
+		if (strcmp(a->p->n->name, s) == 0)
+			return (a->relevant&1);
+	non_fatal("cannot happen, missing proc in ast", (char *) 0);
+	return 0;
+}
+
+static int
+AST_scoutrun(Lextok *t)
+{
+	if (!t) return 0;
+
+	if (t->ntyp == RUN)
+		return AST_proc_isrel(t->sym->name);
+	return (AST_scoutrun(t->lft) || AST_scoutrun(t->rgt));
+}
+
+static void
+AST_tagruns(void)
+{	AST *a;
+	FSM_state *f;
+	FSM_trans *t;
+
+	/* if any stmnt inside a proctype is relevant
+	 * or any parameter passed in a run
+	 * then so are all the run statements on that proctype
+	 */
+
+	for (a = ast; a; a = a->nxt)
+	{	if (strcmp(a->p->n->name, ":never:") == 0
+		||  strcmp(a->p->n->name, ":trace:") == 0
+		||  strcmp(a->p->n->name, ":notrace:") == 0
+		||  strcmp(a->p->n->name, ":init:") == 0)
+		{	a->relevant |= 1;	/* the proctype is relevant */
+			continue;
+		}
+		if (AST_relpar(a->p->n->name))
+			a->relevant |= 1;
+		else
+		{	for (f = a->fsm; f; f = f->nxt)
+			for (t = f->t; t; t = t->nxt)
+				if (t->relevant)
+					goto yes;
+yes:			if (f)
+				a->relevant |= 1;
+		}
+	}
+
+	for (a = ast; a; a = a->nxt)
+	for (f = a->fsm; f; f = f->nxt)
+	for (t = f->t; t; t = t->nxt)
+		if (t->step
+		&&  AST_scoutrun(t->step->n))
+		{	AST_indirect((FSM_use *)0, t, ":run:", a->p->n->name);
+			/* BUT, not all actual params are relevant */
+		}
+}
+
+static void
+AST_report(AST *a, Element *e)	/* ALSO deduce irrelevant vars */
+{
+	if (!(a->relevant&2))
+	{	a->relevant |= 2;
+		printf("spin: redundant in proctype %s (for given property):\n",
+			a->p->n->name);
+	}
+	printf("      line %3d %s (state %d)",
+		e->n?e->n->ln:-1,
+		e->n?e->n->fn->name:"-",
+		e->seqno);
+	printf("	[");
+	comment(stdout, e->n, 0);
+	printf("]\n");
+}
+
+static int
+AST_always(Lextok *n)
+{
+	if (!n) return 0;
+
+	if (n->ntyp == '@'	/* -end */
+	||  n->ntyp == 'p')	/* remote reference */
+		return 1;
+	return AST_always(n->lft) || AST_always(n->rgt);
+}
+
+static void
+AST_edge_dump(AST *a, FSM_state *f)
+{	FSM_trans *t;
+	FSM_use *u;
+
+	for (t = f->t; t; t = t->nxt)	/* edges */
+	{
+		if (t->step && AST_always(t->step->n))
+			t->relevant |= 1;	/* always relevant */
+
+		if (verbose&32)
+		{	switch (t->relevant) {
+			case  0: printf("     "); break;
+			case  1: printf("*%3d ", t->round); break;
+			case  2: printf("+%3d ", t->round); break;
+			case  3: printf("#%3d ", t->round); break;
+			default: printf("? "); break;
+			}
+	
+			printf("%d\t->\t%d\t", f->from, t->to);
+			if (t->step)
+				comment(stdout, t->step->n, 0);
+			else
+				printf("Unless");
+	
+			for (u = t->Val[0]; u; u = u->nxt)
+			{	printf(" <");
+				AST_var(u->n, u->n->sym, 1);
+				printf(":%d>", u->special);
+			}
+			printf("\n");
+		} else
+		{	if (t->relevant)
+				continue;
+
+			if (t->step)
+			switch(t->step->n->ntyp) {
+			case ASGN:
+			case 's':
+			case 'r':
+			case 'c':
+				if (t->step->n->lft->ntyp != CONST)
+					AST_report(a, t->step);
+				break;
+
+			case PRINT:	/* don't report */
+			case PRINTM:
+			case ASSERT:
+			case C_CODE:
+			case C_EXPR:
+			default:
+				break;
+	}	}	}
+}
+
+static void
+AST_dfs(AST *a, int s, int vis)
+{	FSM_state *f;
+	FSM_trans *t;
+
+	f = fsm_tbl[s];
+	if (f->seen) return;
+
+	f->seen = 1;
+	if (vis) AST_edge_dump(a, f);
+
+	for (t = f->t; t; t = t->nxt)
+		AST_dfs(a, t->to, vis);
+}
+
+static void
+AST_dump(AST *a)
+{	FSM_state *f;
+
+	for (f = a->fsm; f; f = f->nxt)
+	{	f->seen = 0;
+		fsm_tbl[f->from] = f;
+	}
+
+	if (verbose&32)
+		printf("AST_START %s from %d\n", a->p->n->name, a->i_st);
+
+	AST_dfs(a, a->i_st, 1);
+}
+
+static void
+AST_sends(AST *a)
+{	FSM_state *f;
+	FSM_trans *t;
+	FSM_use *u;
+	ChanList *cl;
+
+	for (f = a->fsm; f; f = f->nxt)		/* control states */
+	for (t = f->t; t; t = t->nxt)		/* transitions    */
+	{	if (t->step
+		&&  t->step->n
+		&&  t->step->n->ntyp == 's')
+		for (u = t->Val[0]; u; u = u->nxt)
+		{	if (Sym_typ(u->n) == CHAN
+			&&  ((u->special&USE) && !(u->special&DEREF_USE)))
+			{
+#if 0
+				printf("%s -- (%d->%d) -- ",
+					a->p->n->name, f->from, t->to);
+				AST_var(u->n, u->n->sym, 1);
+				printf(" -> chanlist\n");
+#endif
+				cl = (ChanList *) emalloc(sizeof(ChanList));
+				cl->s = t->step->n;
+				cl->n = u->n;
+				cl->nxt = chanlist;
+				chanlist = cl;
+}	}	}	}
+
+static ALIAS *
+AST_alfind(Lextok *n)
+{	ALIAS *na;
+
+	for (na = chalias; na; na = na->nxt)
+		if (AST_mutual(na->cnm, n, 1))
+			return na;
+	return (ALIAS *) 0;
+}
+
+static void
+AST_trans(void)
+{	ALIAS *na, *ca, *da, *ea;
+	int nchanges;
+
+	do {
+		nchanges = 0;
+		for (na = chalias; na; na = na->nxt)
+		{	chalcur = na;
+			for (ca = na->alias; ca; ca = ca->nxt)
+			{	da = AST_alfind(ca->cnm);
+				if (da)
+				for (ea = da->alias; ea; ea = ea->nxt)
+				{	nchanges += AST_add_alias(ea->cnm,
+							ea->origin|ca->origin);
+		}	}	}
+	} while (nchanges > 0);
+
+	chalcur = (ALIAS *) 0;
+}
+
+static void
+AST_def_use(AST *a)
+{	FSM_state *f;
+	FSM_trans *t;
+
+	for (f = a->fsm; f; f = f->nxt)		/* control states */
+	for (t = f->t; t; t = t->nxt)		/* all edges */
+	{	cur_t = t;
+		rel_use(t->Val[0]);		/* redo Val; doesn't cover structs */
+		rel_use(t->Val[1]);
+		t->Val[0] = t->Val[1] = (FSM_use *) 0;
+
+		if (!t->step) continue;
+
+		def_use(t->step->n, 0);		/* def/use info, including structs */
+	}
+	cur_t = (FSM_trans *) 0;
+}
+
+static void
+name_AST_track(Lextok *n, int code)
+{	extern int nr_errs;
+#if 0
+	printf("AST_name: ");
+	AST_var(n, n->sym, 1);
+	printf(" -- %d\n", code);
+#endif
+	if (in_recv && (code&DEF) && (code&USE))
+	{	printf("spin: error: DEF and USE of same var in rcv stmnt: ");
+		AST_var(n, n->sym, 1);
+		printf(" -- %d\n", code);
+		nr_errs++;
+	}
+	check_slice(n, code);
+}
+
+void
+AST_track(Lextok *now, int code)	/* called from main.c */
+{	Lextok *v; extern int export_ast;
+
+	if (!export_ast) return;
+
+	if (now)
+	switch (now->ntyp) {
+	case LEN:
+	case FULL:
+	case EMPTY:
+	case NFULL:
+	case NEMPTY:
+		AST_track(now->lft, DEREF_USE|USE|code);
+		break;
+
+	case '/':
+	case '*':
+	case '-':
+	case '+':
+	case '%':
+	case '&':
+	case '^':
+	case '|':
+	case LE:
+	case GE:
+	case GT:
+	case LT:
+	case NE:
+	case EQ:
+	case OR:
+	case AND:
+	case LSHIFT:
+	case RSHIFT:
+		AST_track(now->rgt, USE|code);
+		/* fall through */
+	case '!':	
+	case UMIN:	
+	case '~':
+	case 'c':
+	case ENABLED:
+	case ASSERT:
+		AST_track(now->lft, USE|code);
+		break;
+
+	case EVAL:
+		AST_track(now->lft, USE|(code&(~DEF)));
+		break;
+
+	case NAME:
+		name_AST_track(now, code);
+		if (now->sym->nel != 1)
+			AST_track(now->lft, USE|code);	/* index */
+		break;
+
+	case 'R':
+		AST_track(now->lft, DEREF_USE|USE|code);
+		for (v = now->rgt; v; v = v->rgt)
+			AST_track(v->lft, code); /* a deeper eval can add USE */
+		break;
+
+	case '?':
+		AST_track(now->lft, USE|code);
+		if (now->rgt)
+		{	AST_track(now->rgt->lft, code);
+			AST_track(now->rgt->rgt, code);
+		}
+		break;
+
+/* added for control deps: */
+	case TYPE:	
+		name_AST_track(now, code);
+		break;
+	case ASGN:
+		AST_track(now->lft, DEF|code);
+		AST_track(now->rgt, USE|code);
+		break;
+	case RUN:
+		name_AST_track(now, USE);
+		for (v = now->lft; v; v = v->rgt)
+			AST_track(v->lft, USE|code);
+		break;
+	case 's':
+		AST_track(now->lft, DEREF_DEF|DEREF_USE|USE|code);
+		for (v = now->rgt; v; v = v->rgt)
+			AST_track(v->lft, USE|code);
+		break;
+	case 'r':
+		AST_track(now->lft, DEREF_DEF|DEREF_USE|USE|code);
+		for (v = now->rgt; v; v = v->rgt)
+		{	in_recv++;
+			AST_track(v->lft, DEF|code);
+			in_recv--;
+		}
+		break;
+	case PRINT:
+		for (v = now->lft; v; v = v->rgt)
+			AST_track(v->lft, USE|code);
+		break;
+	case PRINTM:
+		AST_track(now->lft, USE);
+		break;
+/* end add */
+	case   'p':
+#if 0
+			   'p' -sym-> _p
+			   /
+			 '?' -sym-> a (proctype)
+			 /
+			b (pid expr)
+#endif
+		AST_track(now->lft->lft, USE|code);
+		AST_procisrelevant(now->lft->sym);
+		break;
+
+	case CONST:
+	case ELSE:
+	case NONPROGRESS:
+	case PC_VAL:
+	case   'q':
+		break;
+
+	case   '.':
+	case  GOTO:
+	case BREAK:
+	case   '@':
+	case D_STEP:
+	case ATOMIC:
+	case NON_ATOMIC:
+	case IF:
+	case DO:
+	case UNLESS:
+	case TIMEOUT:
+	case C_CODE:
+	case C_EXPR:
+		break;
+
+	default:
+		printf("AST_track, NOT EXPECTED ntyp: %d\n", now->ntyp);
+		break;
+	}
+}
+
+static int
+AST_dump_rel(void)
+{	Slicer *rv;
+	Ordered *walk;
+	char buf[64];
+	int banner=0;
+
+	if (verbose&32)
+	{	printf("Relevant variables:\n");
+		for (rv = rel_vars; rv; rv = rv->nxt)
+		{	printf("\t");
+			AST_var(rv->n, rv->n->sym, 1);
+			printf("\n");
+		}
+		return 1;
+	}
+	for (rv = rel_vars; rv; rv = rv->nxt)
+		rv->n->sym->setat = 1;	/* mark it */
+
+	for (walk = all_names; walk; walk = walk->next)
+	{	Symbol *s;
+		s = walk->entry;
+		if (!s->setat
+		&&  (s->type != MTYPE || s->ini->ntyp != CONST)
+		&&  s->type != STRUCT	/* report only fields */
+		&&  s->type != PROCTYPE
+		&&  !s->owner
+		&&  sputtype(buf, s->type))
+		{	if (!banner)
+			{	banner = 1;
+				printf("spin: redundant vars (for given property):\n");
+			}
+			printf("\t");
+			symvar(s);
+	}	}
+	return banner;
+}
+
+static void
+AST_suggestions(void)
+{	Symbol *s;
+	Ordered *walk;
+	FSM_state *f;
+	FSM_trans *t;
+	AST *a;
+	int banner=0;
+	int talked=0;
+
+	for (walk = all_names; walk; walk = walk->next)
+	{	s = walk->entry;
+		if (s->colnr == 2	/* only used in conditionals */
+		&&  (s->type == BYTE
+		||   s->type == SHORT
+		||   s->type == INT
+		||   s->type == MTYPE))
+		{	if (!banner)
+			{	banner = 1;
+				printf("spin: consider using predicate");
+				printf(" abstraction to replace:\n");
+			}
+			printf("\t");
+			symvar(s);
+	}	}
+
+	/* look for source and sink processes */
+
+	for (a = ast; a; a = a->nxt)		/* automata       */
+	{	banner = 0;
+		for (f = a->fsm; f; f = f->nxt)	/* control states */
+		for (t = f->t; t; t = t->nxt)	/* transitions    */
+		{	if (t->step)
+			switch (t->step->n->ntyp) {
+			case 's':
+				banner |= 1;
+				break;
+			case 'r':
+				banner |= 2;
+				break;
+			case '.':
+			case D_STEP:
+			case ATOMIC:
+			case NON_ATOMIC:
+			case IF:
+			case DO:
+			case UNLESS:
+			case '@':
+			case GOTO:
+			case BREAK:
+			case PRINT:
+			case PRINTM:
+			case ASSERT:
+			case C_CODE:
+			case C_EXPR:
+				break;
+			default:
+				banner |= 4;
+				goto no_good;
+			}
+		}
+no_good:	if (banner == 1 || banner == 2)
+		{	printf("spin: proctype %s defines a %s process\n",
+				a->p->n->name,
+				banner==1?"source":"sink");
+			talked |= banner;
+		} else if (banner == 3)
+		{	printf("spin: proctype %s mimics a buffer\n",
+				a->p->n->name);
+			talked |= 4;
+		}
+	}
+	if (talked&1)
+	{	printf("\tto reduce complexity, consider merging the code of\n");
+		printf("\teach source process into the code of its target\n");
+	}
+	if (talked&2)
+	{	printf("\tto reduce complexity, consider merging the code of\n");
+		printf("\teach sink process into the code of its source\n");
+	}
+	if (talked&4)
+		printf("\tto reduce complexity, avoid buffer processes\n");
+}
+
+static void
+AST_preserve(void)
+{	Slicer *sc, *nx, *rv;
+
+	for (sc = slicer; sc; sc = nx)
+	{	if (!sc->used)
+			break;	/* done */
+
+		nx = sc->nxt;
+
+		for (rv = rel_vars; rv; rv = rv->nxt)
+			if (AST_mutual(sc->n, rv->n, 1))
+				break;
+
+		if (!rv) /* not already there */
+		{	sc->nxt = rel_vars;
+			rel_vars = sc;
+	}	}
+	slicer = sc;
+}
+
+static void
+check_slice(Lextok *n, int code)
+{	Slicer *sc;
+
+	for (sc = slicer; sc; sc = sc->nxt)
+		if (AST_mutual(sc->n, n, 1)
+		&&  sc->code == code)
+			return;	/* already there */
+
+	sc = (Slicer *) emalloc(sizeof(Slicer));
+	sc->n = n;
+
+	sc->code = code;
+	sc->used = 0;
+	sc->nxt = slicer;
+	slicer = sc;
+}
+
+static void
+AST_data_dep(void)
+{	Slicer *sc;
+
+	/* mark all def-relevant transitions */
+	for (sc = slicer; sc; sc = sc->nxt)
+	{	sc->used = 1;
+		if (verbose&32)
+		{	printf("spin: slice criterion ");
+			AST_var(sc->n, sc->n->sym, 1);
+			printf(" type=%d\n", Sym_typ(sc->n));
+		}
+		AST_relevant(sc->n);
+	}
+	AST_tagruns();	/* mark 'run's relevant if target proctype is relevant */
+}
+
+static int
+AST_blockable(AST *a, int s)
+{	FSM_state *f;
+	FSM_trans *t;
+
+	f = fsm_tbl[s];
+
+	for (t = f->t; t; t = t->nxt)
+	{	if (t->relevant&2)
+			return 1;
+
+		if (t->step && t->step->n)
+		switch (t->step->n->ntyp) {
+		case IF:
+		case DO:
+		case ATOMIC:
+		case NON_ATOMIC:
+		case D_STEP:
+			if (AST_blockable(a, t->to))
+			{	t->round = AST_Round;
+				t->relevant |= 2;
+				return 1;
+			}
+			/* else fall through */
+		default:
+			break;
+		}
+		else if (AST_blockable(a, t->to))	/* Unless */
+		{	t->round = AST_Round;
+			t->relevant |= 2;
+			return 1;
+		}
+	}
+	return 0;
+}
+
+static void
+AST_spread(AST *a, int s)
+{	FSM_state *f;
+	FSM_trans *t;
+
+	f = fsm_tbl[s];
+
+	for (t = f->t; t; t = t->nxt)
+	{	if (t->relevant&2)
+			continue;
+
+		if (t->step && t->step->n)
+			switch (t->step->n->ntyp) {
+			case IF:
+			case DO:
+			case ATOMIC:
+			case NON_ATOMIC:
+			case D_STEP:
+				AST_spread(a, t->to);
+				/* fall thru */
+			default:
+				t->round = AST_Round;
+				t->relevant |= 2;
+				break;
+			}
+		else	/* Unless */
+		{	AST_spread(a, t->to);
+			t->round = AST_Round;
+			t->relevant |= 2;
+		}
+	}
+}
+
+static int
+AST_notrelevant(Lextok *n)
+{	Slicer *s;
+
+	for (s = rel_vars; s; s = s->nxt)
+		if (AST_mutual(s->n, n, 1))
+			return 0;
+	for (s = slicer; s; s = s->nxt)
+		if (AST_mutual(s->n, n, 1))
+			return 0;
+	return 1;
+}
+
+static int
+AST_withchan(Lextok *n)
+{
+	if (!n) return 0;
+	if (Sym_typ(n) == CHAN)
+		return 1;
+	return AST_withchan(n->lft) || AST_withchan(n->rgt);
+}
+
+static int
+AST_suspect(FSM_trans *t)
+{	FSM_use *u;
+	/* check for possible overkill */
+	if (!t || !t->step || !AST_withchan(t->step->n))
+		return 0;
+	for (u = t->Val[0]; u; u = u->nxt)
+		if (AST_notrelevant(u->n))
+			return 1;
+	return 0;
+}
+
+static void
+AST_shouldconsider(AST *a, int s)
+{	FSM_state *f;
+	FSM_trans *t;
+
+	f = fsm_tbl[s];
+	for (t = f->t; t; t = t->nxt)
+	{	if (t->step && t->step->n)
+			switch (t->step->n->ntyp) {
+			case IF:
+			case DO:
+			case ATOMIC:
+			case NON_ATOMIC:
+			case D_STEP:
+				AST_shouldconsider(a, t->to);
+				break;
+			default:
+				AST_track(t->step->n, 0);
+/*
+	AST_track is called here for a blockable stmnt from which
+	a relevant stmnmt was shown to be reachable
+	for a condition this makes all USEs relevant
+	but for a channel operation it only makes the executability
+	relevant -- in those cases, parameters that aren't already
+	relevant may be replaceable with arbitrary tokens
+ */
+				if (AST_suspect(t))
+				{	printf("spin: possibly redundant parameters in: ");
+					comment(stdout, t->step->n, 0);
+					printf("\n");
+				}
+				break;
+			}
+		else	/* an Unless */
+			AST_shouldconsider(a, t->to);
+	}
+}
+
+static int
+FSM_critical(AST *a, int s)
+{	FSM_state *f;
+	FSM_trans *t;
+
+	/* is a 1-relevant stmnt reachable from this state? */
+
+	f = fsm_tbl[s];
+	if (f->seen)
+		goto done;
+	f->seen = 1;
+	f->cr   = 0;
+	for (t = f->t; t; t = t->nxt)
+		if ((t->relevant&1)
+		||  FSM_critical(a, t->to))
+		{	f->cr = 1;
+
+			if (verbose&32)
+			{	printf("\t\t\t\tcritical(%d) ", t->relevant);
+				comment(stdout, t->step->n, 0);
+				printf("\n");
+			}
+			break;
+		}
+#if 0
+	else {
+		if (verbose&32)
+		{ printf("\t\t\t\tnot-crit ");
+		  comment(stdout, t->step->n, 0);
+	 	  printf("\n");
+		}
+	}
+#endif
+done:
+	return f->cr;
+}
+
+static void
+AST_ctrl(AST *a)
+{	FSM_state *f;
+	FSM_trans *t;
+	int hit;
+
+	/* add all blockable transitions
+	 * from which relevant transitions can be reached
+	 */
+	if (verbose&32)
+		printf("CTL -- %s\n", a->p->n->name);
+
+	/* 1 : mark all blockable edges */
+	for (f = a->fsm; f; f = f->nxt)
+	{	if (!(f->scratch&2))		/* not part of irrelevant subgraph */
+		for (t = f->t; t; t = t->nxt)
+		{	if (t->step && t->step->n)
+			switch (t->step->n->ntyp) {
+			case 'r':
+			case 's':
+			case 'c':
+			case ELSE:
+				t->round = AST_Round;
+				t->relevant |= 2;	/* mark for next phases */
+				if (verbose&32)
+				{	printf("\tpremark ");
+					comment(stdout, t->step->n, 0);
+					printf("\n");
+				}
+				break;
+			default:
+				break;
+	}	}	}
+
+	/* 2: keep only 2-marked stmnts from which 1-marked stmnts can be reached */
+	for (f = a->fsm; f; f = f->nxt)
+	{	fsm_tbl[f->from] = f;
+		f->seen = 0;	/* used in dfs from FSM_critical */
+	}
+	for (f = a->fsm; f; f = f->nxt)
+	{	if (!FSM_critical(a, f->from))
+		for (t = f->t; t; t = t->nxt)
+			if (t->relevant&2)
+			{	t->relevant &= ~2;	/* clear mark */
+				if (verbose&32)
+				{	printf("\t\tnomark ");
+					comment(stdout, t->step->n, 0);
+					printf("\n");
+	}		}	}
+
+	/* 3 : lift marks across IF/DO etc. */
+	for (f = a->fsm; f; f = f->nxt)
+	{	hit = 0;
+		for (t = f->t; t; t = t->nxt)
+		{	if (t->step && t->step->n)
+			switch (t->step->n->ntyp) {
+			case IF:
+			case DO:
+			case ATOMIC:
+			case NON_ATOMIC:
+			case D_STEP:
+				if (AST_blockable(a, t->to))
+					hit = 1;
+				break;
+			default:
+				break;
+			}
+			else if (AST_blockable(a, t->to))	/* Unless */
+				hit = 1;
+
+			if (hit) break;
+		}
+		if (hit)	/* at least one outgoing trans can block */
+		for (t = f->t; t; t = t->nxt)
+		{	t->round = AST_Round;
+			t->relevant |= 2;	/* lift */
+			if (verbose&32)
+			{	printf("\t\t\tliftmark ");
+				comment(stdout, t->step->n, 0);
+				printf("\n");
+			}
+			AST_spread(a, t->to);	/* and spread to all guards */
+	}	}
+
+	/* 4: nodes with 2-marked out-edges contribute new slice criteria */
+	for (f = a->fsm; f; f = f->nxt)
+	for (t = f->t; t; t = t->nxt)
+		if (t->relevant&2)
+		{	AST_shouldconsider(a, f->from);
+			break;	/* inner loop */
+		}
+}
+
+static void
+AST_control_dep(void)
+{	AST *a;
+
+	for (a = ast; a; a = a->nxt)
+		if (strcmp(a->p->n->name, ":never:") != 0
+		&&  strcmp(a->p->n->name, ":trace:") != 0
+		&&  strcmp(a->p->n->name, ":notrace:") != 0)
+			AST_ctrl(a);
+}
+
+static void
+AST_prelabel(void)
+{	AST *a;
+	FSM_state *f;
+	FSM_trans *t;
+
+	for (a = ast; a; a = a->nxt)
+	{	if (strcmp(a->p->n->name, ":never:") != 0
+		&&  strcmp(a->p->n->name, ":trace:") != 0
+		&&  strcmp(a->p->n->name, ":notrace:") != 0)
+		for (f = a->fsm; f; f = f->nxt)
+		for (t = f->t; t; t = t->nxt)
+		{	if (t->step
+			&&  t->step->n
+			&&  t->step->n->ntyp == ASSERT
+			)
+			{	t->relevant |= 1;
+	}	}	}
+}
+
+static void
+AST_criteria(void)
+{	/*
+	 * remote labels are handled separately -- by making
+	 * sure they are not pruned away during optimization
+	 */
+	AST_Changes = 1;	/* to get started */
+	for (AST_Round = 1; slicer && AST_Changes; AST_Round++)
+	{	AST_Changes = 0;
+		AST_data_dep();
+		AST_preserve();		/* moves processed vars from slicer to rel_vars */
+		AST_dominant();		/* mark data-irrelevant subgraphs */
+		AST_control_dep();	/* can add data deps, which add control deps */
+
+		if (verbose&32)
+			printf("\n\nROUND %d -- changes %d\n",
+				AST_Round, AST_Changes);
+	}
+}
+
+static void
+AST_alias_analysis(void)		/* aliasing of promela channels */
+{	AST *a;
+
+	for (a = ast; a; a = a->nxt)
+		AST_sends(a);		/* collect chan-names that are send across chans */
+
+	for (a = ast; a; a = a->nxt)
+		AST_para(a->p);		/* aliasing of chans thru proctype parameters */
+
+	for (a = ast; a; a = a->nxt)
+		AST_other(a);		/* chan params in asgns and recvs */
+
+	AST_trans();			/* transitive closure of alias table */
+
+	if (verbose&32)
+		AST_aliases();		/* show channel aliasing info */
+}
+
+void
+AST_slice(void)
+{	AST *a;
+	int spurious = 0;
+
+	if (!slicer)
+	{	non_fatal("no slice criteria (or no claim) specified",
+		(char *) 0);
+		spurious = 1;
+	}
+	AST_dorelevant();		/* mark procs refered to in remote refs */
+
+	for (a = ast; a; a = a->nxt)
+		AST_def_use(a);		/* compute standard def/use information */
+
+	AST_hidden();			/* parameter passing and local var inits */
+
+	AST_alias_analysis();		/* channel alias analysis */
+
+	AST_prelabel();			/* mark all 'assert(...)' stmnts as relevant */
+	AST_criteria();			/* process the slice criteria from
+					 * asserts and from the never claim
+					 */
+	if (!spurious || (verbose&32))
+	{	spurious = 1;
+		for (a = ast; a; a = a->nxt)
+		{	AST_dump(a);		/* marked up result */
+			if (a->relevant&2)	/* it printed something */
+				spurious = 0;
+		}
+		if (!AST_dump_rel()		/* relevant variables */
+		&&  spurious)
+			printf("spin: no redundancies found (for given property)\n");
+	}
+	AST_suggestions();
+
+	if (verbose&32)
+		show_expl();
+}
+
+void
+AST_store(ProcList *p, int start_state)
+{	AST *n_ast;
+
+	if (strcmp(p->n->name, ":never:") != 0
+	&&  strcmp(p->n->name, ":trace:") != 0
+	&&  strcmp(p->n->name, ":notrace:") != 0)
+	{	n_ast = (AST *) emalloc(sizeof(AST));
+		n_ast->p = p;
+		n_ast->i_st = start_state;
+		n_ast->relevant = 0;
+		n_ast->fsm = fsm;
+		n_ast->nxt = ast;
+		ast = n_ast;
+	}
+	fsm = (FSM_state *) 0;	/* hide it from FSM_DEL */
+}
+
+static void
+AST_add_explicit(Lextok *d, Lextok *u)
+{	FSM_trans *e = (FSM_trans *) emalloc(sizeof(FSM_trans));
+
+	e->to = 0;			/* or start_state ? */
+	e->relevant = 0;		/* to be determined */
+	e->step = (Element *) 0;	/* left blank */
+	e->Val[0] = e->Val[1] = (FSM_use *) 0;
+
+	cur_t = e;
+
+	def_use(u, USE);
+	def_use(d, DEF);
+
+	cur_t = (FSM_trans *) 0;
+
+	e->nxt = explicit;
+	explicit = e;
+}
+
+static void
+AST_fp1(char *s, Lextok *t, Lextok *f, int parno)
+{	Lextok *v;
+	int cnt;
+
+	if (!t) return;
+
+	if (t->ntyp == RUN)
+	{	if (strcmp(t->sym->name, s) == 0)
+		for (v = t->lft, cnt = 1; v; v = v->rgt, cnt++)
+			if (cnt == parno)
+			{	AST_add_explicit(f, v->lft);
+				break;
+			}
+	} else
+	{	AST_fp1(s, t->lft, f, parno);
+		AST_fp1(s, t->rgt, f, parno);
+	}
+}
+
+static void
+AST_mk1(char *s, Lextok *c, int parno)
+{	AST *a;
+	FSM_state *f;
+	FSM_trans *t;
+
+	/* concoct an extra FSM_trans *t with the asgn of
+	 * formal par c to matching actual pars made explicit
+	 */
+
+	for (a = ast; a; a = a->nxt)		/* automata       */
+	for (f = a->fsm; f; f = f->nxt)		/* control states */
+	for (t = f->t; t; t = t->nxt)		/* transitions    */
+	{	if (t->step)
+		AST_fp1(s, t->step->n, c, parno);
+	}
+}
+
+static void
+AST_par_init(void)	/* parameter passing -- hidden assignments */
+{	AST *a;
+	Lextok *f, *t, *c;
+	int cnt;
+
+	for (a = ast; a; a = a->nxt)
+	{	if (strcmp(a->p->n->name, ":never:") == 0
+		||  strcmp(a->p->n->name, ":trace:") == 0
+		||  strcmp(a->p->n->name, ":notrace:") == 0
+		||  strcmp(a->p->n->name, ":init:") == 0)
+			continue;			/* have no params */
+
+		cnt = 0;
+		for (f = a->p->p; f; f = f->rgt)	/* types */
+		for (t = f->lft; t; t = t->rgt)		/* formals */
+		{	cnt++;				/* formal par count */
+			c = (t->ntyp != ',')? t : t->lft;	/* the formal parameter */
+			AST_mk1(a->p->n->name, c, cnt);		/* all matching run statements */
+	}	}
+}
+
+static void
+AST_var_init(void)		/* initialized vars (not chans) - hidden assignments */
+{	Ordered	*walk;
+	Lextok *x;
+	Symbol	*sp;
+	AST *a;
+
+	for (walk = all_names; walk; walk = walk->next)	
+	{	sp = walk->entry;
+		if (sp
+		&&  !sp->context		/* globals */
+		&&  sp->type != PROCTYPE
+		&&  sp->ini
+		&& (sp->type != MTYPE || sp->ini->ntyp != CONST) /* not mtype defs */
+		&&  sp->ini->ntyp != CHAN)
+		{	x = nn(ZN, TYPE, ZN, ZN);
+			x->sym = sp;
+			AST_add_explicit(x, sp->ini);
+	}	}
+
+	for (a = ast; a; a = a->nxt)
+	{	if (strcmp(a->p->n->name, ":never:") != 0
+		&&  strcmp(a->p->n->name, ":trace:") != 0
+		&&  strcmp(a->p->n->name, ":notrace:") != 0)	/* claim has no locals */
+		for (walk = all_names; walk; walk = walk->next)	
+		{	sp = walk->entry;
+			if (sp
+			&&  sp->context
+			&&  strcmp(sp->context->name, a->p->n->name) == 0
+			&&  sp->Nid >= 0	/* not a param */
+			&&  sp->type != LABEL
+			&&  sp->ini
+			&&  sp->ini->ntyp != CHAN)
+			{	x = nn(ZN, TYPE, ZN, ZN);
+				x->sym = sp;
+				AST_add_explicit(x, sp->ini);
+	}	}	}
+}
+
+static void
+show_expl(void)
+{	FSM_trans *t, *T;
+	FSM_use *u;
+
+	printf("\nExplicit List:\n");
+	for (T = expl_par; T; T = (T == expl_par)?expl_var: (FSM_trans *) 0)
+	{	for (t = T; t; t = t->nxt)
+		{	if (!t->Val[0]) continue;
+			printf("%s", t->relevant?"*":" ");
+			printf("%3d", t->round);
+			for (u = t->Val[0]; u; u = u->nxt)
+			{	printf("\t<");
+				AST_var(u->n, u->n->sym, 1);
+				printf(":%d>, ", u->special);
+			}
+			printf("\n");
+		}
+		printf("==\n");
+	}
+	printf("End\n");
+}
+
+static void
+AST_hidden(void)			/* reveal all hidden assignments */
+{
+	AST_par_init();
+	expl_par = explicit;
+	explicit = (FSM_trans *) 0;
+
+	AST_var_init();
+	expl_var = explicit;
+	explicit = (FSM_trans *) 0;
+}
+
+#define BPW	(8*sizeof(ulong))			/* bits per word */
+
+static int
+bad_scratch(FSM_state *f, int upto)
+{	FSM_trans *t;
+#if 0
+	1. all internal branch-points have else-s
+	2. all non-branchpoints have non-blocking out-edge
+	3. all internal edges are non-relevant
+	subgraphs like this need NOT contribute control-dependencies
+#endif
+
+	if (!f->seen
+	||  (f->scratch&4))
+		return 0;
+
+	if (f->scratch&8)
+		return 1;
+
+	f->scratch |= 4;
+
+	if (verbose&32) printf("X[%d:%d:%d] ", f->from, upto, f->scratch);
+
+	if (f->scratch&1)
+	{	if (verbose&32)
+			printf("\tbad scratch: %d\n", f->from);
+bad:		f->scratch &= ~4;
+	/*	f->scratch |=  8;	 wrong */
+		return 1;
+	}
+
+	if (f->from != upto)
+	for (t = f->t; t; t = t->nxt)
+		if (bad_scratch(fsm_tbl[t->to], upto))
+			goto bad;
+
+	return 0;
+}
+
+static void
+mark_subgraph(FSM_state *f, int upto)
+{	FSM_trans *t;
+
+	if (f->from == upto
+	||  !f->seen
+	||  (f->scratch&2))
+		return;
+
+	f->scratch |= 2;
+
+	for (t = f->t; t; t = t->nxt)
+		mark_subgraph(fsm_tbl[t->to], upto);
+}
+
+static void
+AST_pair(AST *a, FSM_state *h, int y)
+{	Pair *p;
+
+	for (p = a->pairs; p; p = p->nxt)
+		if (p->h == h
+		&&  p->b == y)
+			return;
+
+	p = (Pair *) emalloc(sizeof(Pair));
+	p->h = h;
+	p->b = y;
+	p->nxt = a->pairs;
+	a->pairs = p;
+}
+
+static void
+AST_checkpairs(AST *a)
+{	Pair *p;
+
+	for (p = a->pairs; p; p = p->nxt)
+	{	if (verbose&32)
+			printf("	inspect pair %d %d\n", p->b, p->h->from);
+		if (!bad_scratch(p->h, p->b))	/* subgraph is clean */
+		{	if (verbose&32)
+				printf("subgraph: %d .. %d\n", p->b, p->h->from);
+			mark_subgraph(p->h, p->b);
+		}
+	}
+}
+
+static void
+subgraph(AST *a, FSM_state *f, int out)
+{	FSM_state *h;
+	int i, j;
+	ulong *g;
+#if 0
+	reverse dominance suggests that this is a possible
+	entry and exit node for a proper subgraph
+#endif
+	h = fsm_tbl[out];
+
+	i = f->from / BPW;
+	j = f->from % BPW;
+	g = h->mod;
+
+	if (verbose&32)
+		printf("possible pair %d %d -- %d\n",
+			f->from, h->from, (g[i]&(1<<j))?1:0);
+	
+	if (g[i]&(1<<j))		/* also a forward dominance pair */
+		AST_pair(a, h, f->from);	/* record this pair */
+}
+
+static void
+act_dom(AST *a)
+{	FSM_state *f;
+	FSM_trans *t;
+	int i, j, cnt;
+
+	for (f = a->fsm; f; f = f->nxt)
+	{	if (!f->seen) continue;
+#if 0
+		f->from is the exit-node of a proper subgraph, with
+		the dominator its entry-node, if:
+		a. this node has more than 1 reachable predecessor
+		b. the dominator has more than 1 reachable successor
+		   (need reachability - in case of reverse dominance)
+		d. the dominator is reachable, and not equal to this node
+#endif
+		for (t = f->p, i = 0; t; t = t->nxt)
+			i += fsm_tbl[t->to]->seen;
+		if (i <= 1) continue;					/* a. */
+
+		for (cnt = 1; cnt < a->nstates; cnt++)	/* 0 is endstate */
+		{	if (cnt == f->from
+			||  !fsm_tbl[cnt]->seen)
+				continue;				/* c. */
+
+			i = cnt / BPW;
+			j = cnt % BPW;
+			if (!(f->dom[i]&(1<<j)))
+				continue;
+
+			for (t = fsm_tbl[cnt]->t, i = 0; t; t = t->nxt)
+				i += fsm_tbl[t->to]->seen;
+			if (i <= 1)
+				continue;				/* b. */
+
+			if (f->mod)			/* final check in 2nd phase */
+				subgraph(a, f, cnt);	/* possible entry-exit pair */
+		}
+	}
+}
+
+static void
+reachability(AST *a)
+{	FSM_state *f;
+
+	for (f = a->fsm; f; f = f->nxt)
+		f->seen = 0;		/* clear */
+	AST_dfs(a, a->i_st, 0);		/* mark 'seen' */
+}
+
+static int
+see_else(FSM_state *f)
+{	FSM_trans *t;
+
+	for (t = f->t; t; t = t->nxt)
+	{	if (t->step
+		&&  t->step->n)
+		switch (t->step->n->ntyp) {
+		case ELSE:
+			return 1;
+		case IF:
+		case DO:
+		case ATOMIC:
+		case NON_ATOMIC:
+		case D_STEP:
+			if (see_else(fsm_tbl[t->to]))
+				return 1;
+		default:
+			break;
+		}
+	}
+	return 0;
+}
+
+static int
+is_guard(FSM_state *f)
+{	FSM_state *g;
+	FSM_trans *t;
+
+	for (t = f->p; t; t = t->nxt)
+	{	g = fsm_tbl[t->to];
+		if (!g->seen)
+			continue;
+
+		if (t->step
+		&&  t->step->n)
+		switch(t->step->n->ntyp) {
+		case IF:
+		case DO:
+			return 1;
+		case ATOMIC:
+		case NON_ATOMIC:
+		case D_STEP:
+			if (is_guard(g))
+				return 1;
+		default:
+			break;
+		}
+	}
+	return 0;
+}
+
+static void
+curtail(AST *a)
+{	FSM_state *f, *g;
+	FSM_trans *t;
+	int i, haselse, isrel, blocking;
+#if 0
+	mark nodes that do not satisfy these requirements:
+	1. all internal branch-points have else-s
+	2. all non-branchpoints have non-blocking out-edge
+	3. all internal edges are non-data-relevant
+#endif
+	if (verbose&32)
+		printf("Curtail %s:\n", a->p->n->name);
+
+	for (f = a->fsm; f; f = f->nxt)
+	{	if (!f->seen
+		||  (f->scratch&(1|2)))
+			continue;
+
+		isrel = haselse = i = blocking = 0;
+
+		for (t = f->t; t; t = t->nxt)
+		{	g = fsm_tbl[t->to];
+
+			isrel |= (t->relevant&1);	/* data relevant */
+			i += g->seen;
+
+			if (t->step
+			&&  t->step->n)
+			{	switch (t->step->n->ntyp) {
+				case IF:
+				case DO:
+					haselse |= see_else(g);
+					break;
+				case 'c':
+				case 's':
+				case 'r':
+					blocking = 1;
+					break;
+		}	}	}
+#if 0
+		if (verbose&32)
+			printf("prescratch %d -- %d %d %d %d -- %d\n",
+				f->from, i, isrel, blocking, haselse, is_guard(f));
+#endif
+		if (isrel			/* 3. */		
+		||  (i == 1 && blocking)	/* 2. */
+		||  (i >  1 && !haselse))	/* 1. */
+		{	if (!is_guard(f))
+			{	f->scratch |= 1;
+				if (verbose&32)
+				printf("scratch %d -- %d %d %d %d\n",
+					f->from, i, isrel, blocking, haselse);
+			}
+		}
+	}
+}
+
+static void
+init_dom(AST *a)
+{	FSM_state *f;
+	int i, j, cnt;
+#if 0
+	(1)  D(s0) = {s0}
+	(2)  for s in S - {s0} do D(s) = S
+#endif
+
+	for (f = a->fsm; f; f = f->nxt)
+	{	if (!f->seen) continue;
+
+		f->dom = (ulong *)
+			emalloc(a->nwords * sizeof(ulong));
+
+		if (f->from == a->i_st)
+		{	i = a->i_st / BPW;
+			j = a->i_st % BPW;
+			f->dom[i] = (1<<j);			/* (1) */
+		} else						/* (2) */
+		{	for (i = 0; i < a->nwords; i++)
+				f->dom[i] = (ulong) ~0;			/* all 1's */
+
+			if (a->nstates % BPW)
+			for (i = (a->nstates % BPW); i < (int) BPW; i++)
+				f->dom[a->nwords-1] &= ~(1<<i);	/* clear tail */
+
+			for (cnt = 0; cnt < a->nstates; cnt++)
+				if (!fsm_tbl[cnt]->seen)
+				{	i = cnt / BPW;
+					j = cnt % BPW;
+					f->dom[i] &= ~(1<<j);
+	}	}		}
+}
+
+static int
+dom_perculate(AST *a, FSM_state *f)
+{	static ulong *ndom = (ulong *) 0;
+	static int on = 0;
+	int i, j, cnt = 0;
+	FSM_state *g;
+	FSM_trans *t;
+
+	if (on < a->nwords)
+	{	on = a->nwords;
+		ndom = (ulong *)
+			emalloc(on * sizeof(ulong));
+	}
+
+	for (i = 0; i < a->nwords; i++)
+		ndom[i] = (ulong) ~0;
+
+	for (t = f->p; t; t = t->nxt)	/* all reachable predecessors */
+	{	g = fsm_tbl[t->to];
+		if (g->seen)
+		for (i = 0; i < a->nwords; i++)
+			ndom[i] &= g->dom[i];	/* (5b) */
+	}
+
+	i = f->from / BPW;
+	j = f->from % BPW;
+	ndom[i] |= (1<<j);			/* (5a) */
+
+	for (i = 0; i < a->nwords; i++)
+		if (f->dom[i] != ndom[i])
+		{	cnt++;
+			f->dom[i] = ndom[i];
+		}
+
+	return cnt;
+}
+
+static void
+dom_forward(AST *a)
+{	FSM_state *f;
+	int cnt;
+
+	init_dom(a);						/* (1,2) */
+	do {
+		cnt = 0;
+		for (f = a->fsm; f; f = f->nxt)
+		{	if (f->seen
+			&&  f->from != a->i_st)			/* (4) */
+				cnt += dom_perculate(a, f);	/* (5) */
+		}
+	} while (cnt);						/* (3) */
+	dom_perculate(a, fsm_tbl[a->i_st]);
+}
+
+static void
+AST_dominant(void)
+{	FSM_state *f;
+	FSM_trans *t;
+	AST *a;
+	int oi;
+#if 0
+	find dominators
+	Aho, Sethi, & Ullman, Compilers - principles, techniques, and tools
+	Addison-Wesley, 1986, p.671.
+
+	(1)  D(s0) = {s0}
+	(2)  for s in S - {s0} do D(s) = S
+
+	(3)  while any D(s) changes do
+	(4)    for s in S - {s0} do
+	(5)	D(s) = {s} union  with intersection of all D(p)
+		where p are the immediate predecessors of s
+
+	the purpose is to find proper subgraphs
+	(one entry node, one exit node)
+#endif
+	if (AST_Round == 1)	/* computed once, reused in every round */
+	for (a = ast; a; a = a->nxt)
+	{	a->nstates = 0;
+		for (f = a->fsm; f; f = f->nxt)
+		{	a->nstates++;				/* count */
+			fsm_tbl[f->from] = f;			/* fast lookup */
+			f->scratch = 0;				/* clear scratch marks */
+		}
+		for (oi = 0; oi < a->nstates; oi++)
+			if (!fsm_tbl[oi])
+				fsm_tbl[oi] = &no_state;
+
+		a->nwords = (a->nstates + BPW - 1) / BPW;	/* round up */
+
+		if (verbose&32)
+		{	printf("%s (%d): ", a->p->n->name, a->i_st);
+			printf("states=%d (max %d), words = %d, bpw %d, overflow %d\n",
+				a->nstates, o_max, a->nwords,
+				(int) BPW, (int) (a->nstates % BPW));
+		}
+
+		reachability(a);
+		dom_forward(a);		/* forward dominance relation */
+
+		curtail(a);		/* mark ineligible edges */
+		for (f = a->fsm; f; f = f->nxt)
+		{	t = f->p;
+			f->p = f->t;
+			f->t = t;	/* invert edges */
+
+			f->mod = f->dom;
+			f->dom = (ulong *) 0;
+		}
+		oi = a->i_st;
+		if (fsm_tbl[0]->seen)	/* end-state reachable - else leave it */
+			a->i_st = 0;	/* becomes initial state */
+	
+		dom_forward(a);		/* reverse dominance -- don't redo reachability! */
+		act_dom(a);		/* mark proper subgraphs, if any */
+		AST_checkpairs(a);	/* selectively place 2 scratch-marks */
+
+		for (f = a->fsm; f; f = f->nxt)
+		{	t = f->p;
+			f->p = f->t;
+			f->t = t;	/* restore */
+		}
+		a->i_st = oi;	/* restore */
+	} else
+		for (a = ast; a; a = a->nxt)
+		{	for (f = a->fsm; f; f = f->nxt)
+			{	fsm_tbl[f->from] = f;
+				f->scratch &= 1; /* preserve 1-marks */
+			}
+			for (oi = 0; oi < a->nstates; oi++)
+				if (!fsm_tbl[oi])
+					fsm_tbl[oi] = &no_state;
+
+			curtail(a);		/* mark ineligible edges */
+
+			for (f = a->fsm; f; f = f->nxt)
+			{	t = f->p;
+				f->p = f->t;
+				f->t = t;	/* invert edges */
+			}
+	
+			AST_checkpairs(a);	/* recompute 2-marks */
+
+			for (f = a->fsm; f; f = f->nxt)
+			{	t = f->p;
+				f->p = f->t;
+				f->t = t;	/* restore */
+		}	}
+}