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

/* Copyright (c) 1991 by AT&T Bell Telephone Laboratories, Inc.
 * All Rights Reserved. This software is for educational purposes only.
 * No part of this source code may be reproduced in any form
 * without explicit written permission from the copyright owner.
 * This software was 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 to: gerard@research.att.com
 */

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 *R0a[] = {
	"	retrans(%d, nstates%d);",
	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 *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[] = {
	"	case %d: /* progress checker */",
	"		((P%d *)pptr(h))->_t = %d;",
	"		((P%d *)pptr(h))->_p = 1;",
	"		now._p_t = 0;",
	"		break;",
	"	}",
	"#ifdef VERI",
	"	if (h == 0 && !addproc(VERI))",
	"		return 0;",
	"#endif",
	"	if (h == 0 && loops && !addproc(%d))",
	"		return 0;",
	"#ifdef VERI",
	"	return (h>0)?h-loops-1:0;",
	"#else",
	"	return (h>0)?h-loops:0;",
	"#endif",
	"}\n",
	0,
};
char *R8[] = {
	"	case %d: j = sizeof(Q%d); break;",
	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[] = {
	"unsend(into)",
	"{	int m=0, j; uchar *z;",
	"	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;",
	"}",
	"",
	"unrecv(from, slot, fld, fldvar, strt)",
	"{	int j;",
	"	uchar *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,
};