pangen3.h

这是一个同样来自贝尔实验室的和UNIX有着渊源的操作系统, 其简洁的设计和实现易于我们学习和理解

/***** spin: pangen3.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: [e-mail]            */

static char *Head0[] = {
	"#if defined(BFS) && defined(REACH)",
	"#undef REACH",	/* redundant with bfs */
	"#endif",
	"#ifdef VERI",
		"#define BASE	1",
	"#else",
		"#define BASE	0",
	"#endif",
	"typedef struct Trans {",
	"	short atom;	/* if &2 = atomic trans; if &8 local */",
	"#ifdef HAS_UNLESS",
	"	short escp[HAS_UNLESS];	/* lists the escape states */",
	"	short e_trans;	/* if set, this is an escp-trans */",
	"#endif",
	"	short tpe[2];	/* class of operation (for reduction) */",
	"	short qu[6];	/* for conditional selections: qid's  */",
	"	uchar ty[6];	/* ditto: type's */",
	"#ifdef NIBIS",
	"	short om;	/* completion status of preselects */",
	"#endif",
	"	char *tp;	/* src txt of statement */",
	"	int st;		/* the nextstate */",
	"	int t_id;	/* transition id, unique within proc */",
	"	int forw;	/* index forward transition */",
	"	int back;	/* index return  transition */",
	"	struct Trans *nxt;",
	"} Trans;\n",
	"#define qptr(x)	(((uchar *)&now)+q_offset[x])",
	"#define pptr(x)	(((uchar *)&now)+proc_offset[x])",
/*	"#define Pptr(x)	((proc_offset[x])?pptr(x):noptr)",	*/
	"extern uchar *Pptr(int);",

	"#define q_sz(x)	(((Q0 *)qptr(x))->Qlen)\n",
	"#ifndef VECTORSZ",
	"#define VECTORSZ	1024           /* sv   size in bytes */",
	"#endif\n",
	0,
};

static char *Header[] = {
	"#ifdef VERBOSE",
		"#ifndef CHECK",
		"#define CHECK",
		"#endif",
		"#ifndef DEBUG",
		"#define DEBUG",
		"#endif",
	"#endif",
	"#ifdef SAFETY",
		"#ifndef NOFAIR",
			"#define NOFAIR",
		"#endif",
	"#endif",
	"#ifdef NOREDUCE",
		"#ifndef XUSAFE",
		"#define XUSAFE",
		"#endif",
		"#if !defined(SAFETY) && !defined(MA)",
			"#define FULLSTACK",
		"#endif",
	"#else",
		"#ifdef BITSTATE",
			"#ifdef SAFETY",
				"#define CNTRSTACK",
			"#else",
				"#define FULLSTACK",
			"#endif",
		"#else",
			"#define FULLSTACK",
		"#endif",
	"#endif",
	"#ifdef BITSTATE",
		"#ifndef NOCOMP",
		"#define NOCOMP",
		"#endif",
		"#if !defined(LC) && defined(SC)",
		"#define LC",
		"#endif",
	"#endif",
	"#if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)",
		"/* accept the above for backward compatibility */",
		"#define COLLAPSE",
	"#endif",
	"#ifdef HC",
	"#undef HC",
	"#define HC4",
	"#endif",
	"#ifdef HC0",	/* 32 bits */
	"#define HC	0",
	"#endif",
	"#ifdef HC1",	/* 32+8 bits */
	"#define HC	1",
	"#endif",
	"#ifdef HC2",	/* 32+16 bits */
	"#define HC	2",
	"#endif",
	"#ifdef HC3",	/* 32+24 bits */
	"#define HC	3",
	"#endif",
	"#ifdef HC4",	/* 32+32 bits - combine with -DMA=8 */
	"#define HC	4",
	"#endif",
	"#ifdef COLLAPSE",
	"unsigned long ncomps[256+2];",
	"#endif",

	"#define MAXQ   	255",
	"#define MAXPROC	255",
	"#define WS		sizeof(long)   /* word size in bytes */",
	"typedef struct Stack  {	 /* for queues and processes */",
	"#if VECTORSZ>32000",
	"	int o_delta;",
	"	int o_offset;",
	"	int o_skip;",
	"	int o_delqs;",
	"#else",
	"	short o_delta;",
	"	short o_offset;",
	"	short o_skip;",
	"	short o_delqs;",
	"#endif",
	"	short o_boq;",
	"#ifndef XUSAFE",
	"	char *o_name;",
	"#endif",
	"	char *body;",
	"	struct Stack *nxt;",
	"	struct Stack *lst;",
	"} Stack;\n",
	"typedef struct Svtack { /* for complete state vector */",
	"#if VECTORSZ>32000",
	"	int o_delta;",
	"	int m_delta;",
	"#else",
	"	short o_delta;	 /* current size of frame */",
	"	short m_delta;	 /* maximum size of frame */",
	"#endif",
	"#if SYNC",
	"	short o_boq;",
	"#endif",
	0,
};

static char *Header0[] = {
	"	char *body;",
	"	struct Svtack *nxt;",
	"	struct Svtack *lst;",
	"} Svtack;\n",
	"Trans ***trans;	/* 1 ptr per state per proctype */\n",
	"#if defined(FULLSTACK) || defined(BFS)",
	"struct H_el *Lstate;",
	"#endif",
	"int depthfound = -1;	/* loop detection */",
	"int proc_offset[MAXPROC], proc_skip[MAXPROC];",
	"int q_offset[MAXQ], q_skip[MAXQ];",
	"#if VECTORSZ<65536",
	"	unsigned short vsize;",
	"#else",
	"	unsigned long  vsize;	/* vector size in bytes */",
	"#endif",
	"#ifdef SVDUMP",
	"int vprefix=0, svfd;		/* runtime option -pN */",
	"#endif",
	"char *tprefix = \"trail\";	/* runtime option -tsuffix */",
	"short boq = -1;		/* blocked_on_queue status */",
	0,
};

static char *Head1[] = {
	"typedef struct State {",
	"	uchar _nr_pr;",
	"	uchar _nr_qs;",
	"	uchar   _a_t;	/* cycle detection */",
#if 0
	in _a_t: bits 0,4, and 5 =(1|16|32) are set during a 2nd dfs
	bit 1 is used as the A-bit for fairness
	bit 7 (128) is the proviso bit, for reduced 2nd dfs (acceptance)
#endif
	"#ifndef NOFAIR",
	"	uchar   _cnt[NFAIR];	/* counters, weak fairness */",
	"#endif",

	"#ifndef NOVSZ",
#ifdef SOLARIS
		"#if 0",
		/* v3.4
		 * noticed alignment problems with some Solaris
		 * compilers, if widest field isn't wordsized
		 */
#else
		"#if VECTORSZ<65536",
#endif
		"	unsigned short _vsz;",
		"#else",
		"	unsigned long  _vsz;",
		"#endif",
	"#endif",

	"#ifdef HAS_LAST",	/* cannot go before _cnt - see hstore() */
	"	uchar  _last;	/* pid executed in last step */",
	"#endif",
	"#ifdef EVENT_TRACE",
		"#if nstates_event<256",
	"	uchar _event;",
		"#else",
	"	unsigned short _event;",
		"#endif",
	"#endif",
	0,
};

static char *Addp0[] = {
	/* addproc(....parlist... */ ")",
	"{	int j, h = now._nr_pr;",
	"#ifndef NOCOMP",
	"	int k;",
	"#endif",
	"	uchar *o_this = this;\n",
	"#ifndef INLINE",
	"	if (TstOnly) return (h < MAXPROC);",
	"#endif",
	"#ifndef NOBOUNDCHECK",
	"/* redefine Index only within this procedure */",
	"#undef Index",
	"#define Index(x, y)	Boundcheck(x, y, 0, 0, 0)",
	"#endif",
	"	if (h >= MAXPROC)",
	"		Uerror(\"too many processes\");",
	"	switch (n) {",
	"	case 0: j = sizeof(P0); break;",
	0,
};

static char *Addp1[] = {
	"	default: Uerror(\"bad proc - addproc\");",
	"	}",
	"	if (vsize%%WS)",
	"		proc_skip[h] = WS-(vsize%%WS);",
	"	else",
	"		proc_skip[h] = 0;",
	"#ifndef NOCOMP",
	"	for (k = vsize + proc_skip[h]; k > vsize; k--)",
	"		Mask[k-1] = 1; /* align */",
	"#endif",
	"	vsize += proc_skip[h];",
	"	proc_offset[h] = vsize;",
	"#ifdef SVDUMP",
	"	if (vprefix > 0)",
	"	{	int dummy = 0;",
	"		write(svfd, (uchar *) &dummy, sizeof(int)); /* mark */",
	"		write(svfd, (uchar *) &h, sizeof(int));",
	"		write(svfd, (uchar *) &n, sizeof(int));",
	"		write(svfd, (uchar *) &proc_offset[h], sizeof(int));",
	"		write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */",
	"	}",
	"#endif",
	"	now._nr_pr += 1;",
	"	if (fairness && ((int) now._nr_pr + 1 >= (8*NFAIR)/2))",
	"	{	printf(\"pan: error: too many processes -- current\");",
	"		printf(\" max is %%d procs (-DNFAIR=%%d)\\n\",",
	"			(8*NFAIR)/2 - 2, NFAIR);",
	"		printf(\"\\trecompile with -DNFAIR=%%d\\n\",",
	"			NFAIR+1);",
	"		pan_exit(1);",
	"	}",

	"	vsize += j;",
	"#ifndef NOVSZ",
	"	now._vsz = vsize;",
	"#endif",
	"#ifndef NOCOMP",
	"	for (k = 1; k <= Air[n]; k++)",
	"		Mask[vsize - k] = 1; /* pad */",
	"	Mask[vsize-j] = 1; /* _pid */",
	"#endif",
	"	hmax = max(hmax, vsize);",
	"	if (vsize >= VECTORSZ)",
	"	{	printf(\"pan: error, VECTORSZ too small, recompile pan.c\");",
	"		printf(\" with -DVECTORSZ=N with N>%%d\\n\", vsize);",
	"		Uerror(\"aborting\");",
	"	}",
	"	memset((char *)pptr(h), 0, j);",
	"	this = pptr(h);",
	"	if (BASE > 0 && h > 0)",
	"		((P0 *)this)->_pid = h-BASE;",
	"	else",
	"		((P0 *)this)->_pid = h;",
	"	switch (n) {",
	0,
};

static char *Addq0[] = {
	"int",
	"addqueue(int n, int is_rv)",
	"{	int j=0, i = now._nr_qs;",
	"#ifndef NOCOMP",
	"	int k;",
	"#endif",
	"	if (i >= MAXQ)",
	"		Uerror(\"too many queues\");",
	"	switch (n) {",
	0,
};

static char *Addq1[] = {
	"	default: Uerror(\"bad queue - addqueue\");",
	"	}",
	"	if (vsize%%WS)",
	"		q_skip[i] = WS-(vsize%%WS);",
	"	else",
	"		q_skip[i] = 0;",
	"#ifndef NOCOMP",
	"	k = vsize;",
	"#ifndef BFS",
	"	if (is_rv) k += j;",
	"#endif",
	"	for (k += q_skip[i]; k > vsize; k--)",
	"		Mask[k-1] = 1;",
	"#endif",
	"	vsize += q_skip[i];",
	"	q_offset[i] = vsize;",
	"	now._nr_qs += 1;",
	"	vsize += j;",
	"#ifndef NOVSZ",
	"	now._vsz = vsize;",
	"#endif",
	"	hmax = max(hmax, vsize);",
	"	if (vsize >= VECTORSZ)",
	"		Uerror(\"VECTORSZ is too small, edit pan.h\");",
	"	memset((char *)qptr(i), 0, j);",
	"	((Q0 *)qptr(i))->_t = n;",
	"	return i+1;",
	"}\n",
	0,
};

static char *Addq11[] = {
	"{	int j; uchar *z;\n",
	"#ifdef HAS_SORTED",
	"	int k;",
	"#endif",
	"	if (!into--)",
	"	uerror(\"ref to uninitialized chan name (sending)\");",
	"	if (into >= (int) now._nr_qs || into < 0)",
	"		Uerror(\"qsend bad queue#\");",
	"	z = qptr(into);",
	"	j = ((Q0 *)qptr(into))->Qlen;",
	"	switch (((Q0 *)qptr(into))->_t) {",
	0,
};

static char *Addq2[] = {
	"	case 0: printf(\"queue %%d was deleted\\n\", into+1);",
	"	default: Uerror(\"bad queue - qsend\");",
	"	}",
	"#ifdef EVENT_TRACE",
	"	if (in_s_scope(into+1))",
	"		require('s', into);",
	"#endif",
	"}",
	"#endif\n",
	"#if SYNC",
	"int",
	"q_zero(int from)",
	"{	if (!from--)",
	"	{	uerror(\"ref to uninitialized chan name (q_zero)\");",
	"		return 0;",
	"	}",
	"	switch(((Q0 *)qptr(from))->_t) {",
	0,
};

static char *Addq3[] = {
	"	case 0: printf(\"queue %%d was deleted\\n\", from+1);",
	"	}",
	"	Uerror(\"bad queue q-zero\");",
	"	return -1;",
	"}",
	"int",
	"not_RV(int from)",
	"{	if (q_zero(from))",
	"	{	printf(\"==>> a test of the contents of a rv \");",
	"		printf(\"channel always returns FALSE\\n\");",
	"		uerror(\"error to poll rendezvous channel\");",
	"	}",
	"	return 1;",
	"}",
	"#endif",
	"#ifndef XUSAFE",
	"void",
	"setq_claim(int x, int m, char *s, int y, char *p)",
	"{	if (x == 0)",
	"	uerror(\"x[rs] claim on uninitialized channel\");",
	"	if (x < 0 || x > MAXQ)",
	"		Uerror(\"cannot happen setq_claim\");",
	"	q_claim[x] |= m;",
	"	p_name[y] = p;",
	"	q_name[x] = s;",
	"	if (m&2) q_S_check(x, y);",
	"	if (m&1) q_R_check(x, y);",
	"}",
	"short q_sender[MAXQ+1];",
	"int",
	"q_S_check(int x, int who)",
	"{	if (!q_sender[x])",
	"	{	q_sender[x] = who+1;",
	"#if SYNC",
	"		if (q_zero(x))",
	"		{	printf(\"chan %%s (%%d), \",",
	"				q_name[x], x-1);",
	"			printf(\"sndr proc %%s (%%d)\\n\",",
	"				p_name[who], who);",
	"			uerror(\"xs chans cannot be used for rv\");",
	"		}",
	"#endif",
	"	} else",
	"	if (q_sender[x] != who+1)",
	"	{	printf(\"pan: xs assertion violated: \");",
	"		printf(\"access to chan <%%s> (%%d)\\npan: by \",",
	"			q_name[x], x-1);",
	"		if (q_sender[x] > 0 && p_name[q_sender[x]-1])",
	"			printf(\"%%s (proc %%d) and by \",",
	"			p_name[q_sender[x]-1], q_sender[x]-1);",
	"		printf(\"%%s (proc %%d)\\n\",",
	"			p_name[who], who);",
	"		uerror(\"error, partial order reduction invalid\");",
	"	}",
	"	return 1;",
	"}",
	"short q_recver[MAXQ+1];",
	"int",
	"q_R_check(int x, int who)",
	"{	if (!q_recver[x])",
	"	{	q_recver[x] = who+1;",
	"#if SYNC",
	"		if (q_zero(x))",
	"		{	printf(\"chan %%s (%%d), \",",
	"				q_name[x], x-1);",
	"			printf(\"recv proc %%s (%%d)\\n\",",
	"				p_name[who], who);",
	"			uerror(\"xr chans cannot be used for rv\");",
	"		}",
	"#endif",
	"	} else",
	"	if (q_recver[x] != who+1)",
	"	{	printf(\"pan: xr assertion violated: \");",
	"		printf(\"access to chan %%s (%%d)\\npan: \",",
	"			q_name[x], x-1);",
	"		if (q_recver[x] > 0 && p_name[q_recver[x]-1])",
	"			printf(\"by %%s (proc %%d) and \",",
	"			p_name[q_recver[x]-1], q_recver[x]-1);",
	"		printf(\"by %%s (proc %%d)\\n\",",
	"			p_name[who], who);",
	"		uerror(\"error, partial order reduction invalid\");",