/***** spin: pangen3.h *****/

/* Copyright (c) 1991,1995 by AT&T Corporation.  All Rights Reserved.     */
/* This software is for educational purposes only.                        */
/* Permission is given to distribute this code provided that this intro-  */
/* ductory message is not removed and no monies are exchanged.            */
/* No guarantee is expressed or implied by the distribution of this code. */
/* Software written by Gerard J. Holzmann as part of the book:            */
/* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4,     */
/* Prentice Hall, Englewood Cliffs, NJ, 07632.                            */
/* Send bug-reports and/or questions to: gerard@research.att.com          */

char *Header[] = {
	"#ifdef VERI",
		"#define BASE	1",
	"#else",
		"#define BASE	0",
	"#endif",
	"#ifdef VERBOSE",
		"#define CHECK",
		"#define DEBUG",
	"#endif",
	"#ifndef REDUCE",
		"#define XUSAFE",
	"#endif",
	"#ifdef REDUCE",
		"#define PARTIAL",
	"#ifdef BITSTATE",
		"#define CNTRSTACK",
	"#else",
		"#define FULLSTACK",
	"#endif",
	"#endif",
	"#ifdef BITSTATE",
		"#define NOCOMP",
	"#endif",
	"#ifndef MEMCNT",
		"#define MEMCNT	30",
	"#endif",
	"#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)",
	"#define q_sz(x)	(((Q0 *)qptr(x))->Qlen)\n",
	"#define MAXQ   	255",
	"#define MAXPROC	255",
	"#define WS		sizeof(long)   /* word size in bytes */",
	"#ifndef VECTORSZ",
	"#define VECTORSZ	1024           /* sv   size in bytes */",
	"#endif\n",
	"typedef struct Stack  {	 /* for queues and processes */",
	"	short o_delta;",
	"	short o_offset;",
	"	short o_skip;",
	"	short o_delqs;",
	"#ifndef XUSAFE",
	"	char *o_name;",
	"#endif",
	"	char *body;",
	"	struct Stack *nxt;",
	"	struct Stack *lst;",
	"} Stack;\n",
	"typedef struct Svtack { /* for complete state vector */",
	"	short o_delta;	 /* current size of frame */",
	"	short m_delta;	 /* maximum size of frame */",
	"#if SYNC",
	"	short o_boq;",
	"#endif",
	"	char *body;",
	"	struct Svtack *nxt;",
	"	struct Svtack *lst;",
	"} Svtack;\n",
	"typedef struct Trans {",
	"	short atom;	/* if &2 = atomic transition; if &8 local */",
	"	short st;	/* the nextstate */",
	"#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];	/* identifies class of operation (for reduction) */",
	"	uchar qu[6];	/* set for conditional selections: qid's  */",
	"	uchar ty[6];	/* set for conditional selections: type's */",
	"#ifdef NIBIS",
	"	short om;	/* remember completion status of preselects */",
	"#endif",
	"	char *tp;	/* src txt of statement */",
	"	int t_id;	/* transition id, unique within proc */",
	"	int forw;	/* index for forward transition */",
	"	int back;	/* index for return  transition */",
	"	struct Trans *nxt;",
	"} Trans;\n",
	"Trans ***trans;	/* 1 ptr per state per proctype */\n",
	"#if defined(FULLSTACK)",
	"struct H_el *Lstate;",
	"#endif",
	"int depthfound = -1;	/* loop detection */",
	"short proc_offset[MAXPROC], proc_skip[MAXPROC];",
	"short q_offset[MAXQ], q_skip[MAXQ];",
	"short vsize;		/* vector size in bytes */",
	"short boq = -1;	/* blocked_on_queue status */",
	"typedef struct State {",
	"	uchar _nr_pr;",
	"	uchar _nr_qs;",
	"	uchar   _a_t;	/* cycle detection */",
	"	uchar   _cnt[NFAIR];	/* counters, weak fairness */",
	"#ifdef HAS_LAST",	/* cannot go before _cnt - see hstore() */
	"	uchar  _last; /* pid executed in last timestep */",
	"#endif",
	0,
};

char *Addp0[] = {
	/* addproc(....parlist... */ ")",
	"{	int k, j, h = now._nr_pr;",
	"	uchar *o_this = this;\n",
	"#ifndef INLINE",
	"	if (TstOnly) return (h < MAXPROC);",
	"#endif",
	"	if (h >= MAXPROC)",
	"		Uerror(\"too many processes\");",
	"	switch (n) {",
	"	case 0: j = sizeof(P0); break;",
	0,
};

char *Addp1[] = {
	"	default: Uerror(\"bad proc - addproc\");",
	"	}",
	"	if (vsize%%WS && (j > WS-(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;",
	"#endif",
	"	vsize += proc_skip[h];",
	"	proc_offset[h] = vsize;",
	"	now._nr_pr += 1;",

	"	if (fairness && (now._nr_pr >= (8*NFAIR)/2))",
	"	{	printf(\"Error: too many processes -- \");",
	"		printf(\"current max is %%d procs (-DNFAIR=%%d)\\n\",",
	"			(8*NFAIR)/2 - 1, NFAIR);",
	"		printf(\"\\trecompile with -DNFAIR=%%d\\n\", NFAIR+1);",
	"		exit(1);",
	"	}",

	"	vsize += j;",
	"#ifndef NOCOMP",
	"	for (k = 1; k <= Air[n]; k++)",
	"		Mask[vsize - k] = 1;",
	"	Mask[vsize-j] = 1; /* _pid */",
	"#endif",
	"	hmax = max(hmax, vsize);",
	"	if (vsize >= VECTORSZ)",
	"		Uerror(\"VECTORSZ is too small, edit pan.h\");",
	"	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,
};

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

char *Addq1[] = {
	"	default: Uerror(\"bad queue - addqueue\");",
	"	}",
	"	if (vsize%%WS && (j > WS-(vsize%%WS)))",
	"		q_skip[i] = WS-(vsize%%WS);",
	"	else",
	"		q_skip[i] = 0;",

	"#ifndef NOCOMP",
	"	k = vsize; if (is_rv) k += j;",
	"	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;",
	"	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,
};

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

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

char *Addq3[] = {
	"	case 0: printf(\"queue %%d was deleted\\n\", from+1);",
	"	}",
	"	Uerror(\"bad queue q-zero\");",
	"}",
	"int",
	"not_RV(int from)",
	"{	if (q_zero(from))",
	"	{	printf(\"==>> a test of the contents of a rendezvous \");",
	"		printf(\"channel must always return 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), sndr proc %%s (%%d)\\n\",",
	"				q_name[x], x-1, p_name[who], who);",
	"			uerror(\"xs chans cannot be used for rendez-vous\");",
	"		}",
	"#endif",
	"	} else",
	"	if (q_sender[x] != who+1)",
	"	{	printf(\"pan: xs assertion violated: access to chan <%%s> (%%d)\\n\",",
	"			q_name[x], x-1);",
	"		printf(\"pan: by %%s (proc %%d) and by %%s (proc %%d)\\n\",",
	"			p_name[q_sender[x]-1], q_sender[x]-1,",
	"			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), recv proc %%s (%%d)\\n\",",
	"				q_name[x], x-1, p_name[who], who);",
	"			uerror(\"xr chans cannot be used for rendez-vous\");",
	"		}",
	"#endif",
	"	} else",
	"	if (q_recver[x] != who+1)",
	"	{	printf(\"pan: xr assertion violated: access to chan %%s (%%d)\\n\",",
	"			q_name[x], x-1);",
	"		printf(\"pan: by %%s (proc %%d) and by %%s (proc %%d)\\n\",",
	"			p_name[q_recver[x]-1], q_recver[x]-1,",
	"			p_name[who], who);",
	"		uerror(\"error, partial order reduction invalid\");",
	"	}",
	"	return 1;",
	"}",
	"#endif",
	"int",
	"q_len(int x)",
	"{	if (!x--)",
	"	uerror(\"ref to uninitialized chan name (len)\");",
	"	return ((Q0 *)qptr(x))->Qlen;",
	"}\n",
	"int",
	"q_full(int from)",
	"{	if (!from--)",
	"	uerror(\"ref to uninitialized chan name (qfull)\");",
	"	switch(((Q0 *)qptr(from))->_t) {",
	0,
};

char *Addq4[] = {
	"	case 0: printf(\"queue %%d was deleted\\n\", from+1);",
	"	}",
	"	Uerror(\"bad queue - q_full\");",
	"	return 0;",
	"}\n",
	"int",
	"qrecv(int from, int slot, int fld, int done)",
	"{	uchar *z;",
	"	int j, k, r=0;\n",
	"	if (!from--)",
	"	uerror(\"ref to uninitialized chan name (receiving)\");",
	"	if (from >= now._nr_qs || from < 0)",
	"		Uerror(\"qrecv bad queue#\");",
	"	z = qptr(from);",
	"	switch (((Q0 *)qptr(from))->_t) {",
	0,
};

char *Addq5[] = {
	"	case 0: printf(\"queue %%d was deleted\\n\", from+1);",
	"	default: Uerror(\"bad queue - qrecv\");",
	"	}",
	"	return r;",
	"}\n",
	0,
};

char *Code0[] = {
	"void",
	"run(void)",
	"{	void active_procs(void);",
	"	int i;",
	"	memset((char *)&now, 0, sizeof(State));",
	"	vsize = sizeof(State) - VECTORSZ;",
	"	settable();",
	0,
};

char *R0[] = {
	"	Maxbody = max(Maxbody, sizeof(P%d));",
	"	reached[%d] = reached%d;",
	"	accpstate[%d] = (uchar *) emalloc(nstates%d);",
	"	progstate[%d] = (uchar *) emalloc(nstates%d);",
	"	stopstate[%d] = (uchar *) emalloc(nstates%d);",
	"	stopstate[%d][endstate%d] = 1;",
	0,
};

char *R1[] = {
	"	reached[%d] = (uchar *) emalloc(4*sizeof(uchar));",
	"	stopstate[%d] = (uchar *) emalloc(4*sizeof(uchar));",
	"	progstate[%d] = stopstate[%d];",
	"	accpstate[%d] = stopstate[%d];",
	0,
};

char *R0a[] = {
	"	retrans(%d, nstates%d, start%d, src_ln%d, reached%d);",
	0,
};
char *R0b[] = {
	"	if (state_tables)",
	"	{	printf(\"\\nTransition Type: \");",
	"		printf(\"A=atomic; D=d_step; L=local; G=global\\n\");",
	"		printf(\"Source-State Labels: \");",
	"		printf(\"p=progress; e=end; a=accept;\\n\");",
	"		exit(0);",
	"	}",
	0,
};

char *Code1[] = {
	"#define ACCEPT_LAB	%d /* accept labels */",
	0,
};

char *Code3[] = {
	"#define PROG_LAB	%d /* progress labels */",
	0,
};

char *R2[] = {
	"uchar *accpstate[%d];",
	"uchar *progstate[%d];",
	"uchar *reached[%d];",
	"uchar *stopstate[%d];",
	0,
};
char *R3[] = {
	"	Maxbody = max(Maxbody, sizeof(Q%d));",
	0,
};
char *R4[] = {
	"	r_ck(reached%d, nstates%d, %d, src_ln%d);",
	0,
};
char *R5[] = {
	"	case %d: j = sizeof(P%d); break;",
	0,
};
char *R6[] = {
	"	}",
	"	this = o_this;",
	"	return h-BASE;",
	"}\n",
	0,
};
char *R9[] = {
	"typedef struct Q%d {",
	"	uchar Qlen;	/* q_size */",
	"	uchar _t;	/* q_type */",
	"	struct {",
	0,
};
char *R10[] = {
	"typedef struct Q0 {\t/* generic q */",
	"	uchar Qlen, _t;",
	"} Q0;",
	0,
};
char *R12[] = {
	"\t\tcase %d: r = ((Q%d *)z)->contents[slot].fld%d; break;",
	0,
};
char *R13[] = {
	"int ",
	"unsend(int into)",
	"{	int m=0, j, k; uchar *z;\n",
	"	if (!into--) uerror(\"ref to uninitialized chan (unsend)\");",
	"	z = qptr(into);",
	"	j = ((Q0 *)z)->Qlen;",
	"	((Q0 *)z)->Qlen = --j;",
	"	switch (((Q0 *)qptr(into))->_t) {",
	0,
};
char *R14[] = {
	"	default: Uerror(\"bad queue - unsend\");",
	"	}",
	"	return m;",
	"}\n",
	"void",
	"unrecv(int from, int slot, int fld, int fldvar, int strt)",
	"{	int j; uchar *z;\n",
	"	if (!from--) uerror(\"ref to uninitialized chan (unrecv)\");",
	"	z = qptr(from);",
	"	j = ((Q0 *)z)->Qlen;",
	"	if (strt) ((Q0 *)z)->Qlen = j+1;",
	"	switch (((Q0 *)qptr(from))->_t) {",
	0,
};
char *R15[] = {
	"	default: Uerror(\"bad queue - qrecv\");",
	"	}",
	"}",
	0,
};
char *Proto[] = {
	"",
	"/** function prototypes **/",
	"char *emalloc(unsigned);",
	"char *malloc(unsigned);",
	"/* char *strcpy(char *, const char *); */",
	"int Boundcheck(int, int, int, int, Trans *);",
	"int abort(void);\n",
	"int addqueue(int, int);",
	"int atoi(char *);",
	"int close(int);",
	"int creat(char *, unsigned short);",
	"int delproc(int, int);",
	"int endstate(void);",
	"int hstore(char *, short, short);",
	"/* int memcmp(const void *, void *, const unsigned); */",
	"/* void *memcpy(void *, const void *, unsigned); */",
	"/* void *memset(void *,    int, unsigned); */",
	"int q_cond(Trans *);",
	"int q_full(int);",
	"int q_len(int);",
	"int q_zero(int);",
	"#ifndef XUSAFE",
	"int q_S_check(int, int);",
	"int q_R_check(int, int);",
	"#endif",
	"int qrecv(int, int, int, int);",
	"/* int strcmp(const char *, const char *); */",
	"/* int strlen(const char *); */",
	"int unsend(int);",
	"int write(int, void *, unsigned);",
	"void *sbrk(int);",
	"void Uerror(char *);",
	"void assert(int, char *, int, int, Trans *);",
	"void checkcycles(void);",
	"void crack(int, int, Trans *, short *);",
	"void db_hash(uchar *, int);",
	"void sbf_hash(uchar *, int);",
	"void sbb_hash(uchar *, int);",
	"void (*d_hash)(uchar *, int);",
	"void delq(int);",
	"void do_reach(void);",
	"void exit(int);",
	"void hinit(void);",
	"void imed(Trans *, int, int);",
	"void new_state(void);",
	"void p_restor(int);",
	"void putpeg(int, int);",
	"void putrail(void);",
	"void q_restor(void);",
	"void retrans(int, int, int, short *, uchar *);",
	"void settable(void);",
	"void setq_claim(int, int, char *, int, char *);",
	"void sv_restor(int);",
	"void sv_save(char *);",
	"void tagtable(int, int, int, short *, uchar *);",
	"void uerror(char *);",
	"void unrecv(int, int, int, int, int);",
	"void usage(FILE *);",
	"void wrap_stats(void);",
	"void xrefsrc(int, int, int);",
	"#if defined(FULLSTACK) && defined(BITSTATE)",
	"int  onstack_now(void);",
	"void onstack_init(void);",
	"void onstack_put(void);",
	"void onstack_zap(void);",
	"#endif",
	"#ifndef XUSAFE",
	"uchar q_claim[MAXQ+1];",
	"char *q_name[MAXQ+1];",
	"char *p_name[MAXPROC+1];",
	"#endif",
	0,
};