/***** spin: pangen2.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 *Preamble[] = {
	"#include <stdio.h>",
	"#include <signal.h>",
	"#include <string.h>",
	"#define Offsetof(X, Y)	((int)(&(((X *)0)->Y)))",
	"#include \"pan.h\"\n",
	"#define max(a,b) (((a)<(b)) ? (b) : (a))",

	"#ifdef CNTRSTACK",
	"#define onstack_now()	(LL[trpt->j6] && LL[trpt->j7])",
	"#define onstack_put()	 LL[trpt->j6]++; LL[trpt->j7]++",
	"#define onstack_zap()	 LL[trpt->j6]--; LL[trpt->j7]--",
	"#endif",

	"#ifndef NOCOMP",
	"#define V_A	(((now._a_t&1)?2:1) << (now._a_t&2))",
	"int	S_A = 0;",
	"#else",
	"#define V_A	0",
	"#define S_A	0",
	"#endif",

	"#if defined(FULLSTACK) && !defined(BITSTATE)",
	"#define onstack_put()	trpt->ostate = Lstate;",
	"#define onstack_zap()	{ if (trpt->ostate) \\",
	"	trpt->ostate->tagged = (S_A)? (trpt->ostate->tagged&~V_A) :0; }",
	"#endif",

	"struct H_el {",
	"	struct H_el *nxt;",
	"#ifdef FULLSTACK",
	"	unsigned tagged;",
	"#endif",
	"#ifdef CHECK",
	"	unsigned st_id;",
	"#endif",
	"#ifdef REACH",
	"	unsigned D;",
	"#endif",
	"	unsigned state;",
	"} **H_tab, **S_tab;\n",

	"typedef struct Trail {",
	"	short st;	/* current state */",
	"	uchar pr;	/* process id */",
	"	uchar tau;	/* 8 different bit-flags */",
	"	uchar o_pm;	/* a few more bit-flags */",

	"#if 0",
	"	Meaning of bit-flags:",
	"	tau&1   -> timeout enabled",
	"	tau&2   -> request to enable timeout 1 level up (in claim)",
	"	tau&4   -> current transition is a  claim move",
	"	tau&8   -> current transition is an atomic move",
	"	tau&16  -> last move was truncated on stack",
	"	tau&32  -> current transition is a preselected move",
	"	tau&64  -> at least one next state is not on the stack",
	"	tau&128 -> current transition is a stutter move",

	"	o_pm&1	-> the current pid moved -- implements else",
	"	o_pm&2	-> this is an acceptance state",
	"	o_pm&4	-> this is a  progress state",
	"	o_pm&8	-> fairness alg rule 1 undo mark",
	"	o_pm&16	-> fairness alg rule 3 undo mark",
	"	o_pm&32	-> fairness alg rule 2 undo mark",
	"	o_pm&64 -> the current proc applied rule2",
	"	o_pm&128 -> a fairness, dummy move - all procs blocked",
	"#endif",
	"	char  o_n, o_ot, o_m;	/* to save locals */",
	"	short o_tt, o_To;", /* used in new_state()  */
	"#ifdef HAS_UNLESS",
	"	short e_state;	/* if escape trans - state of origin */",
	"#endif",
	"#ifdef FULLSTACK",
	"	struct H_el *ostate;	/* pointer to stored state */",
	"#endif",
	"#ifdef CNTRSTACK",
	"	int	j6, j7;",
	"#endif",
	"	Trans *o_t;",	/* transition fct, next state   */
	"	int oval;",	/* backup value of a variable */
	"} Trail;",
	"Trail	*trail, *trpt;",
	"uchar	*this;",
	"int	maxdepth=10000;",
	"uchar	*SS, *LL;",
	"uchar	HASH_NR = 0;",
	"unsigned int HASH_CONST[] = {",
	"	/* asuming 4 bytes per int */",
	"	0x88888EEF,	0x00400007,",
	"	0x04c11db7,	0x100d4e63,",
	"	0x0fc22f87,	0x3ff0c3ff,",
	"	0x38e84cd7,	0x02b148e9,",
	"	0x98b2e49d,	0xb616d379,",
	"	0xa5247fd9,	0xbae92a15,",
	"	0xb91c8bc5,	0x8e5880f3,",
	"	0xacd7c069,	0xb4c44bb3,",
	"	0x2ead1fb7,	0x8e428171,",
	"	0xdbebd459,	0x828ae611,",
	"	0x6cb25933,	0x86cdd651,",
	"	0x9e8f5f21,	0xd5f8d8e7,",
	"	0x9c4e956f,	0xb5cf2c71,",
	"	0x2e805a6d,	0x33fc3a55,",
	"	0xaf203ed1,	0xe31f5909,",
	"	0x5276db35,	0x0c565ef7,",
	"	0x273d1aa5,	0x8923b1dd,",
	"	0",
	"};",
	"int	mreached=0, done=0, errors=0, Nrun=1;",
	"double	nstates=0, nlinks=0, truncs=0, truncs2=0;",
	"double	nlost=0, nShadow=0, hcmp=0;",
	"long	Fa=0, Fh=0, Zh=0, Zn=0;",
	"long	PUT=0, PROBE=0, ZAPS=0;",
	"long	Ccheck=0, Cholds=0;",
	"int	mask, np_cycles=0, a_cycles=0, upto=1;",
	"int	state_tables=0, fairness=0, no_rck=0;",
	"#ifndef INLINE",
	"int	TstOnly=0;",
	"#endif",
	"#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	A_Root;		/* root of acceptance cycles */",
	"State	now;		/* the full state vector */",

	"#ifndef NOCOMP",
	"State	comp_now;	/* compressed state vector */",
	"State	comp_msk;",
	"uchar	*Mask = (uchar *) &comp_msk;",
	"#endif",

	"Stack	*stack; 	/* for queues, processes */",
	"Svtack	*svtack;	/* for old state vectors */",
	"int	J1, J2, j1, j2, j3, j4;",
	"int	A_depth=0;\n",
	"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(int t_id,int a,int b,int c,int d,char *t,int g,int tpe0,int tpe1)",
	"{	Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n",
	"	tmp->atom  = a&(6|32);	/* only &2, &8, and &32 are looked at */",
	"	if (!g) tmp->atom |= 8;	/* no global references */",
	"	tmp->st    = b;",
	"	tmp->tpe[0] = tpe0;",
	"	tmp->tpe[1] = tpe1;",
	"	tmp->tp    = t;",
	"	tmp->t_id  = t_id;",
	"	tmp->forw  = c;",
	"	tmp->back  = d;",
	"	return tmp;",
	"}\n",
	"Trans *",
	"cpytr(Trans *a)",
	"{	Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n",
	"	int i;",
	"	tmp->atom  = a->atom;",
	"	tmp->st    = a->st;",
	"#ifdef HAS_UNLESS",
	"	tmp->e_trans = a->e_trans;",
	"	for (i = 0; i < HAS_UNLESS; i++)",
	"		tmp->escp[i] = a->escp[i];",
	"#endif",
	"	tmp->tpe[0] = a->tpe[0];",
	"	tmp->tpe[1] = a->tpe[1];",
	"	for (i = 0; i < 6; i++)",
	"	{	tmp->qu[i] = a->qu[i];",
	"		tmp->ty[i] = a->ty[i];",
	"	}",
	"	tmp->tp    = (char *) emalloc(strlen(a->tp)+1);",
	"	strcpy(tmp->tp, a->tp);",
	"	tmp->t_id  = a->t_id;",
	"	tmp->forw  = a->forw;",
	"	tmp->back  = a->back;",
	"	return tmp;",
	"}\n",
	"#ifdef PARTIAL",
	"int",
	"srinc_set(int n)",
	"{	if (n <= 2) return LOCAL;",
	"	if (n <= 2+  DELTA) return Q_FULL_F;	/* 's' or nfull  */",
	"	if (n <= 2+2*DELTA) return Q_EMPT_F;	/* 'r' or nempty */",
	"	if (n <= 2+3*DELTA) return Q_EMPT_T;	/* empty */",
	"	if (n <= 2+4*DELTA) return Q_FULL_T;	/* full  */",
	"	if (n ==   5*DELTA) return GLOBAL;",
	"	if (n ==   6*DELTA) return TIMEOUT_F;",
	"	Uerror(\"cannot happen srinc_class\");",
	"	return BAD;",
	"}",
	"int",
	"srunc(int n, int m)",
	"{	switch(m) {",
	"	case Q_FULL_F: return n-2;",
	"	case Q_EMPT_F: return n-2-DELTA;",
	"	case Q_EMPT_T: return n-2-2*DELTA;",
	"	case Q_FULL_T: return n-2-3*DELTA;",
	"	case TIMEOUT_F: return 255;",
	"	}",
	"	Uerror(\"cannot happen srunc\");",
	"	return 0;",
	"}",
	"#endif",
	"int cnt;\n",
	"void",
	"retrans(int n, int m, int is, short srcln[], uchar reach[])",
	"	/* process n, with m states, is=initial state */",
	"{	Trans *T0, *T1, *T2, *T3;",
	"	int i, j, k, p, h, g, aa;",
	"	if (state_tables >= 3)",
	"	{	printf(\"STEP 0 proctype %%s\\n\", ",
	"			procname[n]);",
	"		for (i = 1; i < m; i++)",
	"		for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
	"			crack(n, i, T0, srcln);",
	"		return;",
	"	}",
	"	do {",
	"		for (i = 1, cnt = 0; i < m; i++)",
	"		{	T2 = trans[n][i];",
	"			T1 = T2?T2->nxt:(Trans *)0;",
	"/* prescan: */		for (T0 = T1; T0; T0 = T0->nxt)",
	"/* choice in choice */	{	if (T0->st",
	"				&&  trans[n][T0->st]->nxt)",
	"					break;",
	"			}",
	"#if 0",
	"		if (T0)",
	"		printf(\"\\tstate %%d / %%d: choice in choice\\n\",",
	"		i, T0->st);",
	"#endif",
	"			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);",

	"	if (state_tables >= 2)",
	"	{	printf(\"STEP 2 proctype %%s\\n\", ",
	"			procname[n]);",
	"		for (i = 1; i < m; i++)",
	"		for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
	"			crack(n, i, T0, srcln);",
	"		return;",
	"	}",
	"	for (i = 1; i < m; i++)",
	"	{	if (trans[n][i] && trans[n][i]->nxt) /* optimize */",
	"		{	T1 = trans[n][i]->nxt;",
	"#if 0",
	"			printf(\"\\t\\tpull %%d (%%d) into %%d\\n\",",
	"			T1->st, T1->forw, i);",
	"#endif",
	"			T0 = cpytr(trans[n][T1->st]);",
	"			trans[n][i] = T0;",
	"			reach[T1->st] = 1;",
	"			imed(T0, T1->st, n);",
	"			for (T1 = T1->nxt; T1; T1 = T1->nxt)",
	"			{",
	"#if 0",
	"			printf(\"\\t\\tpull %%d (%%d) into %%d\\n\",",
	"				T1->st, T1->forw, i);",
	"#endif",
	"				T0->nxt = cpytr(trans[n][T1->st]);",
	"				T0 = T0->nxt;",
	"				reach[T1->st] = 1;",
	"				imed(T0, T1->st, n);",
	"	}	}	}",
	"	if (state_tables > 1)",
	"	{	printf(\"STEP 3 proctype %%s\\n\", ",
	"			procname[n]);",
	"		for (i = 1; i < m; i++)",
	"		for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
	"			crack(n, i, T0, srcln);",
	"		return;",
	"	}",
	"#ifdef HAS_UNLESS",
	"	for (i = 1; i < m; i++)",
	"	{	if (!trans[n][i]) continue;",
	"		/* check for each state i if an",
	"		 * escape to some state p is defined",
	"		 * if so, copy and mark p's transitions",
	"		 * and prepend them to the transition-",
	"		 * list of state i",
	"		 */",
	"		T0 = trans[n][i];",
	"		for (k = HAS_UNLESS-1; k >= 0; k--)",
	"		{	if (p = T0->escp[k])",
	"			for (T1 = trans[n][p]; T1; T1 = T1->nxt)",
	"			{	T2 = cpytr(T1);",
	"				T2->e_trans = p;",
	"				T2->nxt = trans[n][i];",
	"				trans[n][i] = T2;",
	"		}	}",
	"	}",
	"#endif",

	"#ifdef PARTIAL",
	"	for (i = 1; i < m; i++)",
	"	{	/* check if mixing of guards preserves a reduction */",
	"		T1 = trans[n][i];",
	"		if (!T1) continue;",
	"		if (T1->nxt)",
	"		{	k = 0;",
	"			for (T0 = T1; T0; T0 = T0->nxt)",
	"			{	if (!(T0->atom&8))",
	"					goto degrade;",
	"				for (aa = 0; aa < 2; aa++)",
	"				{	if (srinc_set(T0->tpe[aa]) >= GLOBAL)",
	"						goto degrade;",
	"					if (T0->tpe[aa]",
	"					&&  T0->tpe[aa] != T1->tpe[0]) k = 1;",
	"			}	}",
	"			g = 0;",
	"			if (k)	/* non-uniform selection */",
	"			for (T0 = T1; T0; T0 = T0->nxt)",
	"			for (aa = 0; aa < 2; aa++)",
	"			{	j = srinc_set(T0->tpe[aa]);",
	"				if (j != LOCAL)",
	"				{	k = srunc(T0->tpe[aa], j);",
	"					for (h = 0; h < 6; h++)",
	"						if (T1->qu[h] == k",
	"						&&  T1->ty[h] == j)",
	"							break;",
	"					if (h >= 6)",
	"					{	T1->qu[g%%6] = k;",
	"						T1->ty[g%%6] = j;",
	"						g++;",
	"			}	}	}",
	"			if (g > 6)",
	"			{	T1->qu[0] = 0;	/* turn it off */",
	"#if 1",
	"				printf(\"line %%d, too many types\",",
	"						srcln[i]);",
	"				printf(\" (%%d) in selection\\n\", g);",
	"#endif",
	"				goto degrade;",
	"			}",
	"		}",
	"		/* mark all options global if at least 1 is global */",
	"		for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
	"			if (!(T1->atom&8)) break;",
	"		if (T1)",
	"degrade:	for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
	"			T1->atom &= ~8;",

	"		/* allow only mixing of 'r's or 's's one the same queue */",
	"		/* and not mixed with other local operations  */",
	"		T1 = trans[n][i]; j = T1->tpe[0];",

	"		if (T1->qu[0]) continue;",

	"		if (T1->nxt && T1->atom&8)",
	"		{ if (j == 5*DELTA)",
	"		  {",
	"#if 1",
	"			printf(\"warning: line %%d, mixed condition: %%s\\n\",",
	"				srcln[i]);",
	"#endif",
	"			goto degrade;",
	"		  }",
	"		  for (T0 = T1; T0; T0 = T0->nxt)",
	"		  for (aa = 0; aa < 2; aa++)",
	"		  if  (T0->tpe[aa] && T0->tpe[aa] != j)",
	"		  {",
	"#if 1",
	"			printf(\"warning: line %%d: [%%d-%%d] mixed %%stion \",",
	"				srcln[i], T0->tpe[aa], j, ",
	"				(j==5*DELTA)?\"condi\":\"selec\");",
	"			printf(\"(defeats reduction)\\n\");",
	"			printf(\"	'%%s' <-> '%%s'\\n\",",
	"				T1->tp, T0->tp);",
	"#endif",
	"			goto degrade;",
	"		} }",
	"	}",
	"#endif",
	"	if (state_tables)",
	"	{	printf(\"proctype \");",
	"		if (!strcmp(procname[n], \":init:\"))",
	"			printf(\"init\\n\");",
	"		else",
	"			printf(\"%%s\\n\", procname[n]);",
	"		for (i = 1; i < m; i++)",
	"			reach[i] = 1;",
	"		tagtable(n, m, is, srcln, reach);",
	"	}",
	"}\n",
	"void",
	"imed(Trans *T, int v, int n)	/* set intermediate state */",
	"{	progstate[n][T->st] |= progstate[n][v];",
	"	accpstate[n][T->st] |= accpstate[n][v];",
	"	stopstate[n][T->st] |= stopstate[n][v];",
	"}\n",
	"void",
	"tagtable(int n, int m, int is, short srcln[], uchar reach[])",
	"{	Trans *z;\n",
	"	if (is >= m || !trans[n][is]",
	"	||  is <= 0 || reach[is] == 0)",
	"		return;",
	"	reach[is] = 0;",
	"	if (state_tables)",
	"	for (z = trans[n][is]; z; z = z->nxt)",
	"		crack(n, is, z, srcln);",
	"	for (z = trans[n][is]; z; z = z->nxt)",
	"	{	int i, j;",
	"		tagtable(n, m, z->st, srcln, reach);",
	"#ifdef HAS_UNLESS",
	"		for (i = 0; i < HAS_UNLESS; i++)",
	"		{	j = trans[n][is]->escp[i];",
	"			if (!j) break;",
	"			tagtable(n, m, j, srcln, reach);",
	"		}",
	"#endif",
	"	}",
	"}\n",
	"void",
	"crack(int n, int j, Trans *z, short srcln[])",
	"{	int i;\n",
	"	if (!z) return;",
#if 0
	"	printf(\"\tstate %%3d --[%%3d]-->\",",
	"		j, z->forw);",
#else
	"	printf(\"\tstate %%3d -(tr %%3d)-> state %%3d  \",",
	"		j, z->forw, z->st);",
	"	printf(\"[id %%3d tp %%3d\", z->t_id, z->tpe[0]);",
	"	if (z->tpe[1]) printf(\",%%d\", z->tpe[1]);",
	"#ifdef HAS_UNLESS",
	"	if (z->e_trans)",
	"		printf(\" org %%3d\", z->e_trans);",
	"	else if (state_tables >= 2)",
	"	for (i = 0; i < HAS_UNLESS; i++)",
	"	{	if (!z->escp[i]) break;",
	"		printf(\" esc %%d\", z->escp[i]);",
	"	}",
	"#endif",
	"	printf(\"]\");",
#endif
	"	printf(\" [%%s%%s%%s%%s%%s] line %%d => \",",
	"		z->atom&6?\"A\":z->atom&32?\"D\":\"-\",",
	"		accpstate[n][j]?\"a\" :\"-\",",
	"		stopstate[n][j]?\"e\" : \"-\",",
	"		progstate[n][j]?\"p\" : \"-\",",
	"		z->atom & 8 ?\"L\":\"G\",",
	"		srcln[j]);",
	"	for (i = 0; z->tp[i]; i++)",
	"		if (z->tp[i] == \'\\n\')",
	"			printf(\"\\\\n\");",
	"		else",
	"			putchar(z->tp[i]);",
	"#if 0",
	"	printf(\"\\n\");",
	"#else",
	"	if (z->qu[0])",
	"	{	printf(\"\\t[\");",
	"		for (i = 0; i < 6; i++)",
	"		if (z->qu[i]) printf(\"(%%d,%%d)\", z->qu[i], z->ty[i]);",
	"		printf(\"]\");",
	"	}",
	"	printf(\"\\n\");",
	"#endif",
	"	fflush(stdout);",
	"}",
	0,
};