/***** spin: spin.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
 */

typedef struct Symbol {
	char	*name;
	short	type;		/* variable or chan type      */
	int	nel;		/* 1 if scalar, >1 if array   */
	int	*val;		/* runtime value(s), initl 0  */
	struct Node	*ini;	/* initial value, or chan-def */
	struct Symbol	*context; /* 0 if global, or procname */
	struct Symbol	*next;	/* linked list */
} Symbol;

typedef struct Node {
	int	nval;		/* value attribute            */
	short	ntyp;		/* node type                  */
	Symbol	*nsym;		/* new attribute              */
	Symbol	*fname;		/* filename of src            */
	struct SeqList	*seql;	/* list of sequences          */
	struct Node	*lft, *rgt; /* children in parse tree */
} Node;

typedef struct Queue {
	short	qid;		/* runtime q index      */
	short	qlen;		/* nr messages stored   */
	short	nslots, nflds;	/* capacity, flds/slot  */
	short	*fld_width;	/* type of each field   */
	int	*contents;	/* the actual buffer    */
	struct Queue	*nxt;	/* linked list */
} Queue;

typedef struct Element {
	Node	*n;		/* defines the type & contents */
	int	seqno;		/* uniquely identifies this el */
	unsigned char	status;	/* used by analyzer generator  */
	struct SeqList	*sub;	/* subsequences, for compounds */
	struct Element	*nxt;	/* linked list */
} Element;

typedef struct Sequence {
	Element	*frst;
	Element	*last;
} Sequence;

typedef struct SeqList {
	Sequence	*this;	/* one sequence */
	struct SeqList	*nxt;	/* linked list  */
} SeqList;

typedef struct Label {
	Symbol	*s;
	Symbol	*c;
	Element	*e;
	struct Label	*nxt;
} Label;

typedef struct Lbreak {
	Symbol	*l;
	struct Lbreak	*nxt;
} Lbreak;

typedef struct RunList {
	Symbol	*n;		/* name            */
	int	pid;		/* process id      */
	int	maxseq;		/* used by analyzer generator */
	Element	*pc;		/* current stmnt   */
	Symbol	*symtab;	/* local variables */
	struct RunList	*nxt;	/* linked list */
} RunList;

typedef struct ProcList {
	Symbol	*n;		/* name       */
	Node	*p;		/* parameters */
	Sequence *s;		/* body       */
	struct ProcList	*nxt;	/* linked list */
} ProcList;

#define DONE	  1     	/* status bits of elements */
#define ATOM	  2     	/* part of an atomic chain */
#define L_ATOM	  4     	/* last element in a chain */
#define Nhash	255    		/* size of hash table */

#define PREDEF	  5		/* predefined identifier */
#define BIT	  1		/* data types    */
#define BYTE	  8		/* width in bits */
#define SHORT	 16
#define INT	 32
#define	CHAN	 64

#define max(a,b) (((a)<(b)) ? (b) : (a))

/***** Old-Style C - prototype definitions *****/
extern char	*malloc();
extern char	*memcpy();
extern char	*memset();
extern char	*mktemp();
extern char	*strcat();
extern char	*strcpy();
extern long	time();
extern void	exit();
extern int	srand();

extern Element	*d_eval_sub();
extern Element	*colons();
extern Element	*eval_sub();
extern Element	*get_lab();
extern Element	*huntele();
extern Element	*if_seq();
extern Element	*new_el();
extern Element	*walk_sub();
extern Node	*nn();
extern Node	*rem_var();
extern Node	*rem_lab();
extern SeqList	*seqlist();
extern Sequence	*close_seq();
extern Symbol	*break_dest();
extern Symbol	*findloc();
extern Symbol	*has_lab();
extern Symbol	*lookup();
extern char	*emalloc();
extern void	add_el();
extern void	add_seq();
extern void	addsymbol();
extern void	blurb();
extern void	check_proc();
extern void	cnt_mpars();
extern void	do_var();
extern void	doglobal();
extern void	do_init();
extern void	dolocal();
extern void	doq();
extern void	dumpglobals();
extern void	dumplocal();
extern void	dumpskip();
extern void	dumpsrc();
extern void	end_labs();
extern void	explain();
extern void	fatal();
extern void	genaddproc();
extern void	genaddqueue();
extern void	genaddclaim();
extern void	genheader();
extern void	genother();
extern void	gensrc();
extern void	genunio();
extern void	lost_trail();
extern void	main();
extern void	make_atomic();
extern void	match_trail();
extern void	mov_lab();
extern void	naddsymbol();
extern void	ncases();
extern void	ntimes();
extern void	open_seq();
extern void	p_talk();
extern void	patch_atomic();
extern void	pushbreak();
extern void	put_pinit();
extern void	put_ptype();
extern void	putname();
extern void	putnr();
extern void	putremote();
extern void	putproc();
extern void	putprogress();
extern void	putseq();
extern void	putskip();
extern void	putsrc();
extern void	putstmnt();
extern void	ready();
extern void	runnable();
extern void	sched();
extern void	set_lab();
extern void	setmtype();
extern void	setparams();
extern void	settype();
extern void	sr_mesg();
extern void	sr_talk();
extern void	start_claim();
extern void	talk();
extern void	typ2c();
extern void	typex();
extern void	undostmnt();
extern void	walk_atomic();
extern void	whoruns();