sched.c

对软件进行可达性测试的软件

/***** spin: sched.c *****/

/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
/* All Rights Reserved.  This software is for educational purposes only.  */
/* No guarantee whatsoever is expressed or implied by the distribution of */
/* this code.  Permission is given to distribute this code provided that  */
/* this introductory message is not removed and no monies are exchanged.  */
/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
/*             http://spinroot.com/                                       */
/* Send all bug-reports and/or questions to: [e-mail]            */

#include <stdlib.h>
#include "spin.h"
#include "y.tab.h"

extern int	verbose, s_trail, analyze, no_wrapup;
extern char	*claimproc, *eventmap, Buf[];
extern Ordered	*all_names;
extern Symbol	*Fname, *context;
extern int	lineno, nr_errs, dumptab, xspin, jumpsteps, columns;
extern int	u_sync, Elcnt, interactive, TstOnly, cutoff;
extern short	has_enabled;
extern int	limited_vis;

RunList		*X   = (RunList  *) 0;
RunList		*run = (RunList  *) 0;
RunList		*LastX  = (RunList  *) 0; /* previous executing proc */
ProcList	*rdy = (ProcList *) 0;
Element		*LastStep = ZE;
int		nproc=0, nstop=0, Tval=0;
int		Rvous=0, depth=0, nrRdy=0, MadeChoice;
short		Have_claim=0, Skip_claim=0;

static int	Priority_Sum = 0;
static void	setlocals(RunList *);
static void	setparams(RunList *, ProcList *, Lextok *);
static void	talk(RunList *);

void
runnable(ProcList *p, int weight, int noparams)
{	RunList *r = (RunList *) emalloc(sizeof(RunList));

	r->n  = p->n;
	r->tn = p->tn;
	r->pid = nproc++ - nstop + Skip_claim;

	if ((verbose&4) || (verbose&32))
		printf("Starting %s with pid %d\n",
			p->n?p->n->name:"--", r->pid);

	if (!p->s)
		fatal("parsing error, no sequence %s",
			p->n?p->n->name:"--");

	r->pc = huntele(p->s->frst, p->s->frst->status, -1);
	r->ps = p->s;

	if (p->s->last)
		p->s->last->status |= ENDSTATE; /* normal end state */

	r->nxt = run;
	r->prov = p->prov;
	r->priority = weight;
	if (noparams) setlocals(r);
	Priority_Sum += weight;
	run = r;
}

ProcList *
ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov)
	/* n=name, p=formals, s=body det=deterministic prov=provided */
{	ProcList *r = (ProcList *) emalloc(sizeof(ProcList));
	Lextok *fp, *fpt; int j; extern int Npars;

	r->n = n;
	r->p = p;
	r->s = s;
	r->prov = prov;
	r->tn = nrRdy++;
	if (det != 0 && det != 1)
	{	fprintf(stderr, "spin: bad value for det (cannot happen)\n");
	}
	r->det = (short) det;
	r->nxt = rdy;
	rdy = r;

	for (fp  = p, j = 0;  fp;  fp = fp->rgt)
	for (fpt = fp->lft;  fpt; fpt = fpt->rgt)
		j++;	/* count # of parameters */
	Npars = max(Npars, j);

	return rdy;
}

int
find_maxel(Symbol *s)
{	ProcList *p;

	for (p = rdy; p; p = p->nxt)
		if (p->n == s)
			return p->s->maxel++;
	return Elcnt++;
}

static void
formdump(void)
{	ProcList *p;
	Lextok *f, *t;
	int cnt;

	for (p = rdy; p; p = p->nxt)
	{	if (!p->p) continue;
		cnt = -1;
		for (f = p->p; f; f = f->rgt)	/* types */
		for (t = f->lft; t; t = t->rgt)	/* formals */
		{	if (t->ntyp != ',')
				t->sym->Nid = cnt--;	/* overload Nid */
			else
				t->lft->sym->Nid = cnt--;
		}
	}
}

void
announce(char *w)
{
	if (columns)
	{	extern char Buf[];
		extern int firstrow;
		firstrow = 1;
		if (columns == 2)
		{	sprintf(Buf, "%d:%s",
			run->pid - Have_claim, run->n->name);
			pstext(run->pid - Have_claim, Buf);
		} else
			printf("proc %d = %s\n",
			run->pid - Have_claim, run->n->name);
		return;
	}

	if (dumptab
	||  analyze
	||  s_trail
	|| !(verbose&4))
		return;

	if (w)
		printf("  0:	proc  - (%s) ", w);
	else
		whoruns(1);
	printf("creates proc %2d (%s)",
		run->pid - Have_claim,
		run->n->name);
	if (run->priority > 1)
		printf(" priority %d", run->priority);
	printf("\n");
}

#ifndef MAXP
#define MAXP	255	/* matches max nr of processes in verifier */
#endif

int
enable(Lextok *m)
{	ProcList *p;
	Symbol *s = m->sym;	/* proctype name */
	Lextok *n = m->lft;	/* actual parameters */

	if (m->val < 1) m->val = 1;	/* minimum priority */
	for (p = rdy; p; p = p->nxt)
		if (strcmp(s->name, p->n->name) == 0)
		{	if (nproc-nstop >= MAXP)
			{	printf("spin: too many processes (%d max)\n", MAXP);
				break;
			}
			runnable(p, m->val, 0);
			announce((char *) 0);
			setparams(run, p, n);
			setlocals(run); /* after setparams */
			return run->pid - Have_claim + Skip_claim; /* effective simu pid */
		}
	return 0; /* process not found */
}

void
check_param_count(int i, Lextok *m)
{	ProcList *p;
	Symbol *s = m->sym;	/* proctype name */
	Lextok *f, *t;		/* formal pars */
	int cnt = 0;

	for (p = rdy; p; p = p->nxt)
	{	if (strcmp(s->name, p->n->name) == 0)
		{	if (m->lft)	/* actual param list */
			{	lineno = m->lft->ln;
				Fname  = m->lft->fn;
			}
			for (f = p->p;   f; f = f->rgt) /* one type at a time */
			for (t = f->lft; t; t = t->rgt)	/* count formal params */
			{	cnt++;
			}
			if (i != cnt)
			{	printf("spin: saw %d parameters, expected %d\n", i, cnt);
				non_fatal("wrong number of parameters", "");
			}
			break;
	}	}
}

void
start_claim(int n)
{	ProcList *p;
	RunList  *r, *q = (RunList *) 0;

	for (p = rdy; p; p = p->nxt)
		if (p->tn == n
		&&  strcmp(p->n->name, ":never:") == 0)
		{	runnable(p, 1, 1);
			goto found;
		}
	printf("spin: couldn't find claim (ignored)\n");
	Skip_claim = 1;
	goto done;
found:
	/* move claim to far end of runlist, and reassign it pid 0 */
	if (columns == 2)
	{	depth = 0;
		pstext(0, "0::never:");
		for (r = run; r; r = r->nxt)
		{	if (!strcmp(r->n->name, ":never:"))
				continue;
			sprintf(Buf, "%d:%s",
				r->pid+1, r->n->name);
			pstext(r->pid+1, Buf);
	}	}

	if (run->pid == 0) return; /* it is the first process started */

	q = run; run = run->nxt;
	q->pid = 0; q->nxt = (RunList *) 0;	/* remove */
done:
	Have_claim = 1;
	for (r = run; r; r = r->nxt)
	{	r->pid = r->pid+Have_claim;	/* adjust */
		if (!r->nxt)
		{	r->nxt = q;
			break;
	}	}
}

int
f_pid(char *n)
{	RunList *r;
	int rval = -1;

	for (r = run; r; r = r->nxt)
		if (strcmp(n, r->n->name) == 0)
		{	if (rval >= 0)
			{	printf("spin: remote ref to proctype %s, ", n);
				printf("has more than one match: %d and %d\n",
					rval, r->pid);
			} else
				rval = r->pid;
		}
	return rval;
}

void
wrapup(int fini)
{
	limited_vis = 0;
	if (columns)
	{	extern void putpostlude(void);
		if (columns == 2) putpostlude();
		if (!no_wrapup)
		printf("-------------\nfinal state:\n-------------\n");
	}
	if (no_wrapup)
		goto short_cut;
	if (nproc != nstop)
	{	int ov = verbose;
		printf("#processes: %d\n", nproc-nstop - Have_claim + Skip_claim);
		verbose &= ~4;
		dumpglobals();
		verbose = ov;
		verbose &= ~1;	/* no more globals */
		verbose |= 32;	/* add process states */
		for (X = run; X; X = X->nxt)
			talk(X);
		verbose = ov;	/* restore */
	}
	printf("%d process%s created\n",
		nproc - Have_claim + Skip_claim,
		(xspin || nproc!=1)?"es":"");
short_cut:
	if (xspin) alldone(0);	/* avoid an abort from xspin */
	if (fini)  alldone(1);
}

static char is_blocked[256];

static int
p_blocked(int p)
{	int i, j;

	is_blocked[p%256] = 1;
	for (i = j = 0; i < nproc - nstop; i++)
		j += is_blocked[i];
	if (j >= nproc - nstop)
	{	memset(is_blocked, 0, 256);
		return 1;
	}
	return 0;
}

static Element *
silent_moves(Element *e)
{	Element *f;

	if (e->n)
	switch (e->n->ntyp) {
	case GOTO:
		if (Rvous) break;
		f = get_lab(e->n, 1);
		cross_dsteps(e->n, f->n);
		return f; /* guard against goto cycles */
	case UNLESS:
		return silent_moves(e->sub->this->frst);
	case NON_ATOMIC:
	case ATOMIC:
	case D_STEP:
		e->n->sl->this->last->nxt = e->nxt;
		return silent_moves(e->n->sl->this->frst);
	case '.':
		return silent_moves(e->nxt);
	}
	return e;
}

static RunList *
pickproc(RunList *Y)
{	SeqList *z; Element *has_else;
	short Choices[256];
	int j, k, nr_else = 0;

	if (nproc <= nstop+1)
	{	X = run;
		return NULL;
	}
	if (!interactive || depth < jumpsteps)
	{	/* was: j = (int) Rand()%(nproc-nstop); */
		if (Priority_Sum < nproc-nstop)
			fatal("cannot happen - weights", (char *)0);
		j = (int) Rand()%Priority_Sum;

		while (j - X->priority >= 0)
		{	j -= X->priority;
			Y = X;
			X = X->nxt;
			if (!X) { Y = NULL; X = run; }
		}
	} else
	{	int only_choice = -1;
		int no_choice = 0, proc_no_ch, proc_k;

		Tval = 0;	/* new 4.2.6 */
try_again:	printf("Select a statement\n");
try_more:	for (X = run, k = 1; X; X = X->nxt)
		{	if (X->pid > 255) break;

			Choices[X->pid] = (short) k;

			if (!X->pc
			||  (X->prov && !eval(X->prov)))
			{	if (X == run)
					Choices[X->pid] = 0;
				continue;
			}
			X->pc = silent_moves(X->pc);
			if (!X->pc->sub && X->pc->n)
			{	int unex;
				unex = !Enabled0(X->pc);
				if (unex)
					no_choice++;
				else
					only_choice = k;
				if (!xspin && unex && !(verbose&32))
				{	k++;
					continue;
				}
				printf("\tchoice %d: ", k++);
				p_talk(X->pc, 0);
				if (unex)
					printf(" unexecutable,");
				printf(" [");
				comment(stdout, X->pc->n, 0);
				if (X->pc->esc) printf(" + Escape");
				printf("]\n");
			} else {
			has_else = ZE;
			proc_no_ch = no_choice;
			proc_k = k;
			for (z = X->pc->sub, j=0; z; z = z->nxt)
			{	Element *y = silent_moves(z->this->frst);
				int unex;
				if (!y) continue;

				if (y->n->ntyp == ELSE)
				{	has_else = (Rvous)?ZE:y;
					nr_else = k++;
					continue;
				}

				unex = !Enabled0(y);
				if (unex)
					no_choice++;
				else
					only_choice = k;
				if (!xspin && unex && !(verbose&32))
				{	k++;
					continue;
				}
				printf("\tchoice %d: ", k++);
				p_talk(X->pc, 0);
				if (unex)
					printf(" unexecutable,");
				printf(" [");
				comment(stdout, y->n, 0);
				printf("]\n");
			}
			if (has_else)
			{	if (no_choice-proc_no_ch >= (k-proc_k)-1)
				{	only_choice = nr_else;
					printf("\tchoice %d: ", nr_else);
					p_talk(X->pc, 0);
					printf(" [else]\n");
				} else
				{	no_choice++;
					printf("\tchoice %d: ", nr_else);
					p_talk(X->pc, 0);
					printf(" unexecutable, [else]\n");
			}	}
		}	}
		X = run;
		if (k - no_choice < 2 && Tval == 0)
		{	Tval = 1;
			no_choice = 0; only_choice = -1;
			goto try_more;
		}
		if (xspin)
			printf("Make Selection %d\n\n", k-1);
		else
		{	if (k - no_choice < 2)
			{	printf("no executable choices\n");
				alldone(0);
			}
			printf("Select [1-%d]: ", k-1);
		}
		if (!xspin && k - no_choice == 2)
		{	printf("%d\n", only_choice);
			j = only_choice;
		} else
		{	char buf[256];
			fflush(stdout);
			scanf("%64s", buf);
			j = -1;
			if (isdigit(buf[0]))
				j = atoi(buf);
			else
			{	if (buf[0] == 'q')
					alldone(0);
			}
			if (j < 1 || j >= k)
			{	printf("\tchoice is outside range\n");
				goto try_again;
		}	}
		MadeChoice = 0;
		Y = NULL;
		for (X = run; X; Y = X, X = X->nxt)
		{	if (!X->nxt
			||   X->nxt->pid > 255
			||   j < Choices[X->nxt->pid])
			{
				MadeChoice = 1+j-Choices[X->pid];
				break;
		}	}
	}
	return Y;
}

void
sched(void)
{	Element *e;
	RunList *Y = NULL;	/* previous process in run queue */
	RunList *oX;
	int go, notbeyond = 0;
#ifdef PC
	int bufmax = 100;
#endif
	if (dumptab)
	{	formdump();
		symdump();
		dumplabels();
		return;
	}

	if (has_enabled && u_sync > 0)
	{	printf("spin: error, cannot use 'enabled()' in ");
		printf("models with synchronous channels.\n");
		nr_errs++;
	}
	if (analyze)
	{	gensrc();
		return;
	} else if (s_trail)
	{	match_trail();
		return;
	}
	if (claimproc)