/***** spin: pangen2.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 *Preamble[] = {
	"#include	<stdio.h>",
	"#include	<signal.h>",
	"#include	\"pan.h\"\n",
	"#define max(a,b) (((a)<(b)) ? (b) : (a))",
	"typedef struct Trail {",
	"	short pr;	/* process id    */",
	"	short st;	/* current state */",
	"	char  o_n, o_ot, o_m, tau;", /* to save locals */
	"	short o_tt, o_To;", /* used in new_state()  */
	"#if CONNECT>0",
	"#ifndef BITSTATE",
	"	struct H_el *parent;",
	"#endif",
	"#endif",
	"	Trans *o_t;",	/* transition fct, next state   */
	"	int oval;",	/* backup value of a variable */
	"} Trail;",
	"Trail *trail, *trpt;",
	"uchar *this;\n",
	"int maxdepth=10000;",
	"uchar *SS, *LL;",
	"char *emalloc(), *malloc(), *memset();",
	"int mreached=0, done=0, nstates=0;",
	"int nlinks=0, truncs=0, errors=0;",
	"int mask, hcmp=0, loops=0, upto=1;",
	"#ifdef BITSTATE",
	"int ssize=22;",
	"#else",
	"int ssize=18;",
	"#endif",
	"int hmax=0, svmax=0, smax=0;",
	"int Maxbody=0;",
	"uchar *noptr;	/* used by macro Pptr(x) */",
	"State	now;		/* the full state vector */",
	"Stack	*stack; 	/* for queues, processes */",
	"Svtack	*svtack;	/* for old state vectors */",
	"int J1, J2, j1, j2, j3, j4;",
	"int depth=0;\n",
	"#if SYNC",
	"#define IfNotBlocked	if (boq != -1) continue;",
	"#define UnBlock     	boq = -1",
	"#else",
	"#define IfNotBlocked	/* cannot block */",
	"#define UnBlock     	/* don't bother */",
	"#endif\n",
	0,
};

char *Tail[] = {
	"Trans *",
	"settr(a, b, c, d)",
	"{	Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n",
	"	tmp->atom = a&6;",
	"	tmp->st = b;",
	"	tmp->forw = c;",
	"	tmp->back = d;",
	"	return tmp;",
	"}\n",
	"Trans *",
	"cpytr(a)",
	"	Trans *a;",
	"{	Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n",
	"	tmp->atom = a->atom;",
	"	tmp->st = a->st;",
	"	tmp->ist = a->ist;",
	"	tmp->forw = a->forw;",
	"	tmp->back = a->back;",
	"	return tmp;",
	"}\n",
	"int cnt;",
	"retrans(n, m)	/* proc n, m states */",
	"{	Trans *T0, *T1, *T2, *T3;",
	"	int i, j=0;",
	"	do {	j++;",
	"		for (i = 1, cnt = 0; i < m; i++)",
	"		{	T1 = trans[n][i]->nxt;",
	"			T2 = trans[n][i];",
	"/* prescan: */		for (T0 = T1; T0; T0 = T0->nxt)",
	"/* choice inside choice */	if (trans[n][T0->st]->nxt)",
	"					break;",
	"			if (T0)",
	"			for (T0 = T1; T0; T0 = T0->nxt)",
	"			{	T3 = trans[n][T0->st];",
	"				if (!T3->nxt)",
	"				{	T2->nxt = cpytr(T0);",
	"					T2 = T2->nxt;",
	"					imed(T2, T0->st, n);",
	"					continue;",
	"				}",
	"				do {	T3 = T3->nxt;",
	"					T2->nxt = cpytr(T3);",
	"					T2 = T2->nxt;",
	"					imed(T2, T0->st, n);",
	"				} while (T3->nxt);",
	"				cnt++;",
	"			}",
	"		}",
	"	} while (cnt);",
	"	for (i = 1; i < m; i++)",
	"	if (trans[n][i]->nxt)	/* optimize the list a bit */",
	"	{	T1 = trans[n][i]->nxt;",
	"		T0 = trans[n][i] = cpytr(trans[n][T1->st]);",
	"		imed(T0, T1->st, n);",
	"		for (T1 = T1->nxt; T1; T1 = T1->nxt)",
	"		{	T0->nxt = cpytr(trans[n][T1->st]);",
	"			T0 = T0->nxt;",
	"			imed(T0, T1->st, n);",
	"	}	}",
	"}",
	"imed(T, v, n)	/* set intermediate state */",
	"	Trans *T;",
	"{	static uchar warned=0;",
	"	if (T->ist && !warned)",
	"	{	warned=1;",
	"		printf(\"warning: %%s has \", procname[n]);",
	"		printf(\"ambiguous flow ctl structures, \");",
	"		printf(\"revise model\\n\");",
	"	}",
	"	progstate[n][T->st] |= progstate[n][v];",
	"	accpstate[n][T->st] |= accpstate[n][v];",
	"	stopstate[n][T->st] |= stopstate[n][v];",
	"	T->ist = v;",
	"}",
	0,
};