pangen2.h

对软件进行可达性测试的软件

/***** spin: pangen2.h *****/

/* Copyright (c) 1989-2007 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: [e-mail]            */
/* (c) 2007: small additions for V5.0 to support multi-core verifications */

static char *Nvr1[] = {		/* allow separate compilation */
	"#ifdef VERI",
	"void",
	"check_claim(int st)",
	"{",
	"	if (st == endclaim)",
	"		uerror(\"claim violated!\");",
	"	if (stopstate[VERI][st])",
	"		uerror(\"end state in claim reached\");",
	"}",
	"#endif",
	0,
};

static char *Pre0[] = {
"#ifdef SC",
	"#define _FILE_OFFSET_BITS	64",	/* to allow file sizes greater than 2Gb */
"#endif",
	"#include <stdio.h>",
	"#include <signal.h>",
	"#include <stdlib.h>",
	"#include <stdarg.h>",
	"#include <string.h>",
	"#include <ctype.h>",
	"#include <errno.h>",
	"#if defined(WIN32) || defined(WIN64)",
		"#include <time.h>",
	"#else",
		"#include <unistd.h>",
		"#include <sys/times.h>",
	"#endif",
	"#include <sys/types.h>",	/* defines off_t */
	"#include <sys/stat.h>",
	"#include <fcntl.h>",

	"#define Offsetof(X, Y)	((unsigned long)(&(((X *)0)->Y)))",
	"#ifndef max",
	"#define max(a,b) (((a)<(b)) ? (b) : (a))",
	"#endif",
	"#ifndef PRINTF",
	"int Printf(const char *fmt, ...); /* prototype only */",
	"#endif",
	0,
};

static char *Preamble[] = {

	"#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",

	"#if !defined(SAFETY) && !defined(NOCOMP)",
		/*
		 * V_A identifies states in the current statespace
		 * A_V identifies states in the 'other' statespace
		 * S_A remembers how many leading bytes in the sv
		 * are used for these markers + fairness bits
		 */
		"#define V_A	(((now._a_t&1)?2:1) << (now._a_t&2))",
		"#define A_V	(((now._a_t&1)?1:2) << (now._a_t&2))",
		"int	S_A = 0;",
	"#else",
		"#define V_A	0",
		"#define A_V	0",
		"#define S_A	0",
	"#endif",

"#ifdef MA",
	"#undef onstack_now",
	"#undef onstack_put",
	"#undef onstack_zap",
	"#define onstack_put()	;",
	"#define onstack_zap()	gstore((char *) &now, vsize, 4)",
"#else",
	"#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",
"#endif",

	"#ifndef NO_V_PROVISO",
	"#define V_PROVISO",
	"#endif",
	"",
	"struct H_el {",
	"	struct H_el *nxt;",
	"#ifdef FULLSTACK",
	"	unsigned int tagged;",
	"	#if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)",
		"	unsigned int proviso;", /* uses just 1 bit 0/1 */
	"	#endif",
	"#endif",
	"#if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))",
	"	unsigned long st_id;",
	"#endif",
	"#if !defined(SAFETY) || defined(REACH)",
	"	unsigned int D;",
	"#endif",
	"#if NCORE>1",
	"	/* could cost 1 extra word: 4 bytes if 32-bit and 8 bytes if 64-bit */",
	"	#ifdef V_PROVISO",
	"	uchar	cpu_id;		/* id of cpu that created the state */",
	"	#endif",
	"#endif",
	"#ifdef COLLAPSE",
	"	#if VECTORSZ<65536",
	"	unsigned short ln;",	/* length of vector */
	"	#else",
	"	unsigned long ln;",	/* length of vector */
	"	#endif",
	"#endif",
	"	unsigned state;",
	"} **H_tab, **S_Tab;\n",

	"typedef struct Trail {",
	"	int   st;	/* current state */",
	"	uchar pr;	/* process id */",
	"	uchar tau;	/* 8 bit-flags */",
	"	uchar o_pm;	/* 8 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",
	"#ifdef NSUCC",
	"	uchar n_succ;	/* nr of successor states */",
	"#endif",
	"#if defined(FULLSTACK) && defined(MA) && !defined(BFS)",
	"	uchar proviso;",
	"#endif",
	"#ifndef BFS",
	"	uchar  o_n, o_ot;	/* to save locals */",
	"#endif",
	"	uchar  o_m;",
	"#ifdef EVENT_TRACE",
		"#if nstates_event<256",
	"	uchar o_event;",
		"#else",
	"	unsigned short o_event;",
		"#endif",
	"#endif",
	"	int o_tt;",
	"#ifndef BFS",
	"	short o_To;",
		"#ifdef RANDOMIZE",
	"	short oo_i;",
		"#endif",
	"#endif",
	"#if defined(HAS_UNLESS) && !defined(BFS)",
	"	int e_state;	/* if escape trans - state of origin */",
	"#endif",
	"#if (defined(FULLSTACK) && !defined(MA)) || defined(BFS) || (NCORE>1)",
	"	struct H_el *ostate;	/* pointer to stored state */",
	"#endif",
	/* CNTRSTACK when !NOREDUCE && BITSTATE && SAFETY, uses LL[] */
	"#if defined(CNTRSTACK) && !defined(BFS)",
	"	long	j6, j7;",
	"#endif",
	"	Trans *o_t;",	/* transition fct, next state   */
	"#if defined(BUDGET)",
	"	double o_budget;",
	"#endif",
	"#ifdef HAS_SORTED",
	"	short ipt;",	/* insertion slot in q */
	"#endif",
	"	union {",
	"		int oval;",	/* single backup value of variable */
	"		int *ovals;",	/* ptr to multiple values */
	"	} bup;",
	"} Trail;",
	"Trail	*trail, *trpt;",

	"FILE	*efd;",
	"uchar	*this;",
	"long	maxdepth=10000;",
	"long	omaxdepth=10000;",
	"#if NCORE>1",
	"long	z_handoff = -1;",
	"#endif",
	"#ifdef SC",	/* stack cycling */
	"char	*stackfile;",
 	"#endif",
	"uchar	*SS, *LL;",
	"uchar	HASH_NR = 0;",
	"",
	"double memcnt = (double) 0;",
	"double memlim = (double) (1<<30);",
	"",
	"/* for emalloc: */",
	"static char *have;",
	"static long left = 0L;",
	"static double fragment = (double) 0;",
	"static unsigned long grow;",
	"",
	"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",
	"};",
	"#if NCORE>1",
	"extern int core_id;",
	"#endif",
	"long	mreached=0;",
	"int done=0, errors=0, Nrun=1;",
	"int	c_init_done=0;",
	"char	*c_stack_start = (char *) 0;",
	"double	nstates=0, nlinks=0, truncs=0, truncs2=0;",
	"double	nlost=0, nShadow=0, hcmp=0, ngrabs=0;",
	"#if defined(BUDGET)",
	"double budget=0.0;",
	"#endif",
	"int	c_init_run;",
	"#ifdef BFS",
	"double midrv=0, failedrv=0, revrv=0;",
	"#endif",
	"unsigned long	nr_states=0; /* nodes in DFA */",
	"long	Fa=0, Fh=0, Zh=0, Zn=0;",
	"long	PUT=0, PROBE=0, ZAPS=0;",
	"long	Ccheck=0, Cholds=0;",
	"int	a_cycles=0, upto=1, strict=0, verbose = 0, signoff = 0;",
	"#ifdef HAS_CODE",
	"int	gui = 0, coltrace = 0, readtrail = 0, whichtrail = 0, onlyproc = -1, silent = 0;",
	"#endif",
	"int	state_tables=0, fairness=0, no_rck=0, Nr_Trails=0;",
	"char	simvals[128];",
	"#ifndef INLINE",
	"int	TstOnly=0;",
	"#endif",
	"unsigned long mask, nmask;",
	"#ifdef BITSTATE",
	"int	ssize=23;	/* 1 Mb */",
	"#else",
	"int	ssize=19;	/* 512K slots */",
	"#endif",
	"int	hmax=0, svmax=0, smax=0;",
	"int	Maxbody=0, XX;",
	"uchar	*noptr;	/* used by macro Pptr(x) */",
	"#ifdef VAR_RANGES",
	"void logval(char *, int);",
	"void dumpranges(void);",
	"#endif",

	"#ifdef MA",
	"#define INLINE_REV",
	"extern void dfa_init(unsigned short);",
	"extern int  dfa_member(unsigned long);",
	"extern int  dfa_store(uchar *);",
	"unsigned int	maxgs = 0;",
	"#endif",

	"State	comp_now;	/* compressed state vector */",
	"State	comp_msk;",
	"uchar	*Mask = (uchar *) &comp_msk;",
	"#ifdef COLLAPSE",
	"State	comp_tmp;",
	"static char	*scratch = (char *) &comp_tmp;",
	"#endif",

	"Stack	*stack; 	/* for queues, processes */",
	"Svtack	*svtack;	/* for old state vectors */",
	"#ifdef BITSTATE",
	"static unsigned int hfns = 3;	/* new default */",
	"#endif",
	"static unsigned long j1;",
	"static unsigned long K1, K2;",
	"static unsigned long j2, j3, j4;",
	"#ifdef BITSTATE",
#ifndef POWOW
	"static long udmem;",
#endif
	"#endif",
	"static long	A_depth = 0;",
	"long	depth = 0;",	/* not static to support -S2 option, but possible clash with embedded code */
	"#if NCORE>1",
	"long nr_handoffs = 0;",
	"#endif",
	"static uchar	warned = 0, iterative = 0, like_java = 0, every_error = 0;",
	"static uchar	noasserts = 0, noends = 0, bounded = 0;",
	"#if SYNC>0 && ASYNC==0",
	"void set_recvs(void);",
	"int  no_recvs(int);",
	"#endif",
	"#if SYNC",
	"#define IfNotBlocked	if (boq != -1) continue;",
	"#define UnBlock     	boq = -1",
	"#else",
	"#define IfNotBlocked	/* cannot block */",
	"#define UnBlock     	/* don't bother */",
	"#endif\n",
	"#ifdef BITSTATE",
	"int (*bstore)(char *, int);",
	"int bstore_reg(char *, int);",
#ifndef POWOW
	"int bstore_mod(char *, int);",
#endif
	"#endif",
	"void active_procs(void);",
	"void cleanup(void);",
	"void do_the_search(void);",
	"void find_shorter(int);",
	"void iniglobals(void);",
	"void stopped(int);",
	"void wrapup(void);",
	"int *grab_ints(int);",
	"void ungrab_ints(int *, int);",
	0,
};

static 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|32) have meaning */",
	"	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",
	"#ifndef NOREDUCE",
	"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;",
	"	if (n ==   7*DELTA) return ALPHA_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 ALPHA_F:",
	"	case TIMEOUT_F: return 257; /* non-zero, and > MAXQ */",
	"	}",
	"	Uerror(\"cannot happen srunc\");",
	"	return 0;",
	"}",
	"#endif",
	"int cnt;",
	"#ifdef HAS_UNLESS",
	"int",
	"isthere(Trans *a, int b)", /* is b already in a's list? */
	"{	Trans *t;",
	"	for (t = a; t; t = t->nxt)",
	"		if (t->t_id == b)",
	"			return 1;",
	"	return 0;",
	"}",
	"#endif",
	"#ifndef NOREDUCE",
	"int",
	"mark_safety(Trans *t) /* for conditional safety */",
	"{	int g = 0, i, j, k;",
	"",
	"	if (!t) return 0;",
	"	if (t->qu[0])",
	"		return (t->qu[1])?2:1;	/* marked */",
	"",
	"	for (i = 0; i < 2; i++)",
	"	{	j = srinc_set(t->tpe[i]);",
	"		if (j >= GLOBAL && j != ALPHA_F)",
	"			return -1;",
	"		if (j != LOCAL)",
	"		{	k = srunc(t->tpe[i], j);",
	"			if (g == 0",
	"			||  t->qu[0] != k",
	"			||  t->ty[0] != j)",
	"			{	t->qu[g] = k;",
	"				t->ty[g] = j;",
	"				g++;",
	"	}	}	}",
	"	return g;",
	"}",
	"#endif",
	"void",
	"retrans(int n, int m, int is, short srcln[], uchar reach[], uchar lstate[])",
	"	/* process n, with m states, is=initial state */",
	"{	Trans *T0, *T1, *T2, *T3;",
	"	int i, k;",
	"#ifndef NOREDUCE",
	"	int g, h, j, aa;",
	"#endif",