/***** 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: bugs@spinroot.com            *//* (c) 2007: small additions for V5.0 to support multi-core verifications */ 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", 	"#ifdef TRIX",	"	#define qptr(x)	(channels[x]->body)",	"	#define pptr(x)	(processes[x]->body)",	"#else",	"	#define qptr(x)	(((uchar *)&now)+(int)q_offset[x])",	"	#define pptr(x)	(((uchar *)&now)+(int)proc_offset[x])",/*	"	#define Pptr(x)	((proc_offset[x])?pptr(x):noptr)",	*/	"#endif",	"extern uchar *Pptr(int);",	"extern uchar *Qptr(int);", 	"#define q_sz(x)	(((Q0 *)qptr(x))->Qlen)",	"",	"#ifdef TRIX",	"	#ifdef VECTORSZ",	"		#undef VECTORSZ",	/* backward compatibility */	"	#endif",	"	#if WS==4",	"		#define VECTORSZ	2056	/* ((MAXPROC+MAXQ+4)*sizeof(uchar *)) */",	"	#else",	"		#define VECTORSZ	4112	/* the formula causes probs in preprocessing */",	"	#endif",	"#else",	"	#ifndef VECTORSZ",	"		#define VECTORSZ	1024	/* sv size in bytes */",	"	#endif",	"#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",	"		#if defined(SAFETY) && !defined(HASH64)",	"			#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",	"	#if NCORE>1 && !defined(SEP_STATE)",	"		unsigned long *ncomps;	/* in shared memory */",	"	#else",	"		unsigned long ncomps[256+2];",	"	#endif",	"#endif", 	"#define MAXQ   	255",	"#define MAXPROC	255",	"",	"typedef struct _Stack  {	 /* for queues and processes */",	"#if VECTORSZ>32000",	"	int o_delta;",	"	#ifndef TRIX",	"		int o_offset;",	"		int o_skip;",	"	#endif",	"	int o_delqs;",	"#else",	"	short o_delta;",	"	#ifndef TRIX",	"		short o_offset;",	"		short o_skip;",	"	#endif",	"	short o_delqs;",	"#endif",	"	short o_boq;",	"#ifdef TRIX",	"	short parent;",	"	char *b_ptr;",	/* used in delq/q_restor and delproc/p_restor */	"#else",	"	char *body;",	/* full copy of state vector in non-trix mode */	"#endif",	"#ifndef XUSAFE",	"	char *o_name;",	"#endif",	"	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",	"struct H_el *Lstate;",	"int depthfound = -1;	/* loop detection */", 	"#ifndef TRIX",	"	#if VECTORSZ>32000",	"		int proc_offset[MAXPROC];",	"		int q_offset[MAXQ];",	"	#else",	"		short proc_offset[MAXPROC];",	"		short q_offset[MAXQ];",	"	#endif",	"	uchar proc_skip[MAXPROC];",	"	uchar q_skip[MAXQ];",	"#endif", 	"unsigned long  vsize;	/* vector size in bytes */",	"#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", 	"#if defined(BITSTATE) && defined(BCS) && defined(STORE_CTX)",	"	uchar  _ctx;	/* nr of context switches so far */",	"#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\");",	"#ifdef V_TRIX",	"	printf(\"%%4d: add process %%d\\n\", depth, h);",	"#endif",	"	switch (n) {",	"	case 0: j = sizeof(P0); break;",	0,}; static char *Addp1[] = {	"	default: Uerror(\"bad proc - addproc\");",	"	}", 	"#ifdef TRIX",	"	vsize += sizeof(struct H_el *);",	"#else",	"	if (vsize%%WS)",	"		proc_skip[h] = WS-(vsize%%WS);",	"	else",	"		proc_skip[h] = 0;",	"	#ifndef NOCOMP",	"		for (k = vsize + (int) proc_skip[h]; k > vsize; k--)",	"			Mask[k-1] = 1; /* align */",	"	#endif",	"	vsize += (int) proc_skip[h];",	"	proc_offset[h] = vsize;",	"	vsize += j;",	"	#if defined(SVDUMP) && defined(VERBOSE)",	"	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));",	"	#if VECTORSZ>32000",	"		write(svfd, (uchar *) &proc_offset[h], sizeof(int));",	"		write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */",	"	#else",	"		write(svfd, (uchar *) &proc_offset[h], sizeof(short));",	"		write(svfd, (uchar *) &now, vprefix-3*sizeof(int)-sizeof(short)); /* padd */",	"	#endif",	"	}",	"	#endif",	"#endif", 	"	now._nr_pr += 1;",	"#if defined(BCS) && defined(CONSERVATIVE)",	"	if (now._nr_pr >= CONSERVATIVE*8)",	"	{	printf(\"pan: error: too many processes -- recompile with \");",	"		printf(\"-DCONSERVATIVE=%%d\\n\", CONSERVATIVE+1);",	"		pan_exit(1);",	"	}",	"#endif",	"	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);",	"	}",	"#ifndef NOVSZ",	"	now._vsz = vsize;",	"#endif",	"	hmax = max(hmax, vsize);", 	"#ifdef TRIX",	"	#ifndef BFS",	"		if (freebodies)",	"		{	processes[h] = freebodies;",	"			freebodies = freebodies->nxt;",	"		} else",	"		{	processes[h] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));",	"			processes[h]->body = (uchar *) emalloc(Maxbody * sizeof(char));",	"		}",	"		processes[h]->modified = 1;	/* addproc */",	"	#endif",	"	processes[h]->psize = j;",	"	processes[h]->parent_pid = calling_pid;",	"	processes[h]->nxt = (TRIX_v6 *) 0;",	"#else",	"	#ifndef NOCOMP",	"		for (k = 1; k <= Air[n]; k++)",	"			Mask[vsize - k] = 1; /* pad */",	"		Mask[vsize-j] = 1; /* _pid */",	"	#endif",	"	if (vsize >= VECTORSZ)",	"	{	printf(\"pan: error, VECTORSZ too small, recompile pan.c\");",	"		printf(\" with -DVECTORSZ=N with N>%%d\\n\", (int) vsize);",	"		Uerror(\"aborting\");",	"	}",	"#endif", 	"	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 calling_pid, int n, int is_rv)",	"{	int j=0, i = now._nr_qs;",	"#if !defined(NOCOMP) && !defined(TRIX)",	"	int k;",	"#endif",	"	if (i >= MAXQ)",	"		Uerror(\"too many queues\");",	"#ifdef V_TRIX",	"	printf(\"%%4d: add queue %%d\\n\", depth, i);",	"#endif",	"	switch (n) {",	0,}; static char *Addq1[] = {	"	default: Uerror(\"bad queue - addqueue\");",	"	}", 	"#ifdef TRIX",	"	vsize += sizeof(struct H_el *);",	"#else",	"	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 += (int) q_skip[i]; k > vsize; k--)",	"			Mask[k-1] = 1;",	"	#endif",	"	vsize += (int) q_skip[i];",	"	q_offset[i] = vsize;",	"	vsize += j;",	"#endif", 	"	now._nr_qs += 1;",	"#ifndef NOVSZ",	"	now._vsz = vsize;",	"#endif",	"	hmax = max(hmax, vsize);", 	"#ifdef TRIX",	"	#ifndef BFS",	"		if (freebodies)",	"		{	channels[i] = freebodies;",	"			freebodies = freebodies->nxt;",	"		} else",	"		{	channels[i] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));",	"			channels[i]->body = (uchar *) emalloc(Maxbody * sizeof(char));",	"		}",	"		channels[i]->modified = 1;	/* addq */",	"	#endif",	"	channels[i]->psize = j;",	"	channels[i]->parent_pid = calling_pid;",	"	channels[i]->nxt = (TRIX_v6 *) 0;",	"#else",	"	if (vsize >= VECTORSZ)",	"		Uerror(\"VECTORSZ is too small, edit pan.h\");",	"#endif", 	"	if (j > 0)", /* zero if there are no queues */	"	{	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#\");",	"#if defined(TRIX) && !defined(BFS)",	"	#ifndef TRIX_ORIG",	"		(trpt+1)->q_bup = now._ids_[now._nr_pr+into];",	"		#ifdef V_TRIX",	"			printf(\"%%4d: channel %%d s save %%p from %%d\\n\",",	"			depth, into, (trpt+1)->q_bup, now._nr_pr+into);",	"		#endif",	"	#endif",	"	channels[into]->modified = 1;	/* qsend */",	"	#ifdef V_TRIX",	"		printf(\"%%4d: channel %%d modified\\n\", depth, into);",	"	#endif",	"#endif",	"	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--)",

Lines 1–500 of 1184. Load more