#define Version	"Spin Version 3.4.5 -- 8 March 2000"
#define Source	"models/deadlock.philosophers.prm"

char *TrailFile = Source; /* default */
#define uchar	unsigned char
#define DELTA	500
#ifdef MA
#if MA==1
#undef MA
#define MA	100
#endif
#endif
#ifdef W_XPT
#if W_XPT==1
#undef W_XPT
#define W_XPT 1000000
#endif
#endif
#ifndef NFAIR
#define NFAIR	2	/* must be >= 2 */
#endif
#ifndef HSFSPIN
#define INLINE	1
#endif
#define MERGED	1
#ifdef NP	/* includes np_ demon */
#define HAS_NP	2
#define VERI	2
#define endclaim	3 /* none */
#endif
typedef struct S_F_MAP {
	char *fnm; int from; int upto;
} S_F_MAP;

short nstates1=12;	/* :init: */
#define endstate1	11
short src_ln1 [] = {
	  0,  26,  27,  28,  29,  30,  31,  25, 
	 33,  25,  24,  34,   0, };
S_F_MAP src_file1 [] = {
	{ "-", 0, 0 },
	{ "models/deadlock.philosophers.prm", 1, 11 },
	{ "-", 12, 13 }
};
uchar reached1 [] = {
	  0,   1,   0,   0,   0,   1,   1,   0, 
	  1,   1,   0,   0,   0, };

short nstates0=9;	/* philosopher */
#define endstate0	8
short src_ln0 [] = {
	  0,  12,  13,  15,  15,  11,  18,  11, 
	 18,   0, };
S_F_MAP src_file0 [] = {
	{ "-", 0, 0 },
	{ "models/deadlock.philosophers.prm", 1, 8 },
	{ "-", 9, 10 }
};
uchar reached0 [] = {
	  0,   1,   0,   0,   0,   0,   1,   1, 
	  0,   0, };
#define _T5	12
#define _T2	13
#define SYNC	0
#define ASYNC	1

char *procname[] = {
   "philosopher",
   ":init:",
   ":np_:",
};

typedef struct P1 { /* :init: */
	unsigned _pid : 8;  /* 0..255 */
	unsigned _t   : 3; /* proctype */
	unsigned _p   : 5; /* state    */
	uchar philosophers;
} P1;
#define Air1	(sizeof(P1) - Offsetof(P1, philosophers) - 1*sizeof(uchar))
typedef struct P0 { /* philosopher */
	unsigned _pid : 8;  /* 0..255 */
	unsigned _t   : 3; /* proctype */
	unsigned _p   : 5; /* state    */
	int my_id;
} P0;
#define Air0	(sizeof(P0) - Offsetof(P0, my_id) - 1*sizeof(int))
typedef struct P2 { /* np_ */
	unsigned _pid : 8;  /* 0..255 */
	unsigned _t   : 3; /* proctype */
	unsigned _p   : 5; /* state    */
} P2;
#define Air2	(sizeof(P2) - 2)
#ifdef VERI
#define BASE	1
#else
#define BASE	0
#endif
#ifdef HSFSPIN
typedef struct HSF_Lextok{
  unsigned short ntyp;  /* node type */
  int (*val)(void);     /* value/excutability of condition */
  void *(*var)(void);   /* adress of variable */
  HSF_Lextok *lft,*rgt; /* children in condition tree */
} HSF_Lextok;
HSF_Lextok *Lextok_Wood;
#endif /* HSFSPIN */
typedef struct Trans {
	short atom;	/* if &2 = atomic trans; if &8 local */
	short st;	/* the nextstate */
#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 t_id;	/* transition id, unique within proc */
	int forw;	/* index forward transition */
	int back;	/* index return  transition */
#ifdef HSFSPIN
       HSF_Lextok  *lextok_tree; /* Pointer to root of the lextok tree. */
#endif /* HSFSPIN */
	struct Trans *nxt;
} Trans;

#ifndef HSFSPIN
#define qptr(x)	(((uchar *)&now)+q_offset[x])
#define pptr(x)	(((uchar *)&now)+proc_offset[x])
#else
#define qptr(x)	(((uchar *)now)+q_offset[x])
#define pptr(x)	(((uchar *)now)+proc_offset[x])
#define hsf_qptr(s,x)	(((uchar *)(s))+q_offset[x])
#define hsf_pptr(s,x)	(((uchar *)(s))+proc_offset[x])
#endif /* HSFSPIN */
extern uchar *Pptr(int);
#define q_sz(x)	(((Q0 *)qptr(x))->Qlen)

#ifdef HSFSPIN
#define hsf_q_sz(s,x)	(((Q0 *)hsf_qptr(s,x))->Qlen)

#endif /* HSFSPIN */
#ifndef VECTORSZ
#define VECTORSZ	1024           /* sv   size in bytes */
#endif

#ifdef VERBOSE
#define CHECK
#define DEBUG
#endif
#ifdef SAFETY
#ifndef NOFAIR
#define NOFAIR
#endif
#endif
#ifdef NOREDUCE
#define XUSAFE
#if !defined(SAFETY) && !defined(MA)
#define FULLSTACK
#endif
#else
#ifdef BITSTATE
#ifdef SAFETY
#define CNTRSTACK
#else
#define FULLSTACK
#endif
#else
#define FULLSTACK
#endif
#endif
#ifdef BITSTATE
#define NOCOMP
#if !defined(LC) && defined(SC)
#define LC
#endif
#endif
#ifndef MEMCNT
#ifdef PC
#define MEMCNT	25	/* 32 Mb */
#else
#define MEMCNT	28
#endif
#endif
#if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)
/* accept the above for backward compatibility */
#define COLLAPSE
#endif
#ifdef HC
#define HC2
#endif
#ifdef HC0
#define HC	0
#endif
#ifdef HC1
#define HC	1
#endif
#ifdef HC2
#define HC	2
#endif
#ifdef HC3
#define HC	3
#endif
#ifdef HC4
#define HC	4
#endif
#ifdef COLLAPSE
unsigned long ncomps[256+2];
#endif
#define MAXQ   	255
#define MAXPROC	255
#define WS		sizeof(long)   /* word size in bytes */
typedef struct Stack  {	 /* for queues and processes */
#if VECTORSZ>32000
	int o_delta;
	int o_offset;
	int o_skip;
	int o_delqs;
#else
	short o_delta;
	short o_offset;
	short o_skip;
	short o_delqs;
#endif
	short o_boq;
#ifndef XUSAFE
	char *o_name;
#endif
	char *body;
	struct Stack *nxt;
	struct Stack *lst;
} Stack;

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
	char *body;
	struct Svtack *nxt;
	struct Svtack *lst;
} Svtack;

Trans ***trans;	/* 1 ptr per state per proctype */

#if defined(FULLSTACK)
struct H_el *Lstate;
#endif
int depthfound = -1;	/* loop detection */
int proc_offset[MAXPROC], proc_skip[MAXPROC];
int q_offset[MAXQ], q_skip[MAXQ];
#if VECTORSZ<65536
	unsigned short vsize;
#else
	unsigned long  vsize;	/* vector size in bytes */
#endif
#ifdef SVDUMP
int vprefix=0, svfd;		/* runtime option -pN */
#endif
char *tprefix = "trail";	/* runtime option -tsuffix */
#ifndef HSFSPIN
short boq = -1;		/* blocked_on_queue status */
#endif
#ifndef HSFSPIN
typedef struct State {
#else
typedef struct PackedState {
#endif
	uchar _nr_pr;
	uchar _nr_qs;
	short boq;
	uchar   _a_t;	/* cycle detection */
#ifndef NOFAIR
	uchar   _cnt[NFAIR];	/* counters, weak fairness */
#endif
#ifndef NOVSZ
#if VECTORSZ<65536
	unsigned short _vsz;
#else
	unsigned long  _vsz;
#endif
#endif
#ifdef HAS_LAST
	uchar  _last;	/* pid executed in last step */
#endif
#ifdef EVENT_TRACE
#if nstates_event<256
	uchar _event;
#else
	unsigned short _event;
#endif
#endif
	uchar forks[4];
	uchar sv[VECTORSZ];
#ifndef HSFSPIN
} State
;

#else
        int static equal(PackedState& ps1, PackedState& ps2){
                return (ps1._vsz==ps2._vsz) &&
                       (memcmp((void *)&ps1, (void *)&ps2, ps1._vsz)==0);
                }
        int static hash(PackedState& ps, int max){
                return the_hash_function->hash((unsigned char*)&ps,ps._vsz)%max;
                }
} PackedState
;
#endif /* HSFSPIN */

int _; /* a predefined write-only variable */

#define FORWARD_MOVES	"pan.m"
#define REVERSE_MOVES	"pan.b"
#define LEXTOK_WOOD_VALFUNCS	"pan.v"
#define LEXTOK_WOOD_CONSTRUCTOR	"pan.w"
#define TRANSITIONS	"pan.t"
#define _NP_	2
#ifdef HSFSPIN
short nstates_proc[_NP_]={nstates0,nstates1}; 
#endif /* HSFSPIN */
uchar reached2[3];  /* np_ */
#define nstates2	3 /* np_ */
#define endstate2	2 /* np_ */

#define start2	0 /* np_ */
#define start1	10
#define start0	5
#ifdef HSFSPIN
short start_proc[_NP_]={start0,start1}; /* HSF */
#endif /* HSFSPIN */
#ifdef NP
#define ACCEPT_LAB	1 /* at least 1 in np_ */
#else
#define ACCEPT_LAB	0 /* user-defined accept labels */
#endif
#define PROG_LAB	0 /* progress labels */
uchar *accpstate[3];
uchar *progstate[3];
uchar *reached[3];
uchar *stopstate[3];
uchar *visstate[3];
#ifdef HSFSPIN
uchar *dangstate[3];
#endif /* HSFSPIN */
short q_flds[5];
short q_max[5];
typedef struct Q4 {
	uchar Qlen;	/* q_size */
	uchar _t;	/* q_type */
	struct {
		uchar fld0;
	} contents[1];
} Q4;
typedef struct Q3 {
	uchar Qlen;	/* q_size */
	uchar _t;	/* q_type */
	struct {
		uchar fld0;
	} contents[1];
} Q3;
typedef struct Q2 {
	uchar Qlen;	/* q_size */
	uchar _t;	/* q_type */
	struct {
		uchar fld0;
	} contents[1];
} Q2;
typedef struct Q1 {
	uchar Qlen;	/* q_size */
	uchar _t;	/* q_type */
	struct {
		uchar fld0;
	} contents[1];
} Q1;
typedef struct Q0 {	/* generic q */
	uchar Qlen, _t;
#ifdef HSFSPIN
       struct {
              uchar fld0;
       } contents[1];
#endif
} Q0;

/** function prototypes **/
#ifndef HSFSPIN
char *emalloc(unsigned long);
char *Malloc(unsigned long);
#endif /* HSFSPIN */
int Boundcheck(int, int, int, int, Trans *);
/* int abort(void); */
int addqueue(int, int);
/* int atoi(char *); */
int close(int);
int creat(char *, unsigned short);
int write(int, void *, unsigned);
int delproc(int, int);
int endstate(void);
#ifndef HSFSPIN
int hstore(char *, int, short);
#ifdef MA
int gstore(char *, int, uchar);
#endif
#endif /* HSFSPIN */
int q_cond(short, Trans *);
int q_full(int);
int q_len(int);
int q_zero(int);
#ifdef HSFSPIN
#if SYNC
int not_RV(int from);
#endif
#endif /* HSFSPIN */
int qrecv(int, int, int, int);
#ifndef HSFSPIN
int unsend(int);
#endif /* HSFSPIN */
void *sbrk(int);
void Uerror(char *);
void assert(int, char *, int, int, Trans *);
#ifndef HSFSPIN
void checkcycles(void);
#endif /* HSFSPIN */
void crack(int, int, Trans *, short *);
void d_hash(uchar *, int);
#ifndef HSFSPIN
void delq(int);
void do_reach(void);
#endif /* HSFSPIN */
void exit(int);
void hinit(void);
void imed(Trans *, int, int);
void new_state(void);
#ifndef HSFSPIN
void p_restor(int);
#endif /* HSFSPIN */
void putpeg(int, int);
void putrail(void);
#ifndef HSFSPIN
void q_restor(void);
#endif /* HSFSPIN */
void retrans(int, int, int, short *, uchar *);
void settable(void);
void setq_claim(int, int, char *, int, char *);
#ifndef HSFSPIN
void sv_restor(void);
void sv_save(char *);
#endif /* HSFSPIN */
void tagtable(int, int, int, short *, uchar *);
void uerror(char *);
#ifndef HSFSPIN
void unrecv(int, int, int, int, int);
void usage(FILE *);
void wrap_stats(void);
#endif /* HSFSPIN */
void xrefsrc(int, S_F_MAP *, int, int);
#if defined(FULLSTACK) && defined(BITSTATE)
#ifndef HSFSPIN
int  onstack_now(void);
void onstack_init(void);
void onstack_put(void);
void onstack_zap(void);
#endif /* HSFSPIN */
#endif
#ifndef XUSAFE
int q_S_check(int, int);
int q_R_check(int, int);
uchar q_claim[MAXQ+1];
char *q_name[MAXQ+1];
char *p_name[MAXPROC+1];
#endif
void qsend(int, int, int);
#define Addproc(x)	addproc(x, 0)
#define LOCAL	1
#define Q_FULL_F	2
#define Q_EMPT_F	3
#define Q_EMPT_T	4
#define Q_FULL_T	5
#define TIMEOUT_F	6
#define GLOBAL	7
#define BAD	8
#define ALPHA_F	9
#define NTRANS	14
#ifdef PEG
long peg[NTRANS];
#endif
