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

/* Copyright (c) 1989-2009 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            */

#ifndef SEEN_SPIN_H
#define SEEN_SPIN_H

#include <stdio.h>
#include <string.h>
#include <ctype.h>

enum	    { INIV, PUTV, LOGV };	/* for pangen[14].c */
enum btypes { NONE, N_CLAIM, I_PROC, A_PROC, P_PROC, E_TRACE, N_TRACE };

typedef struct Lextok {
	unsigned short	ntyp;	/* node type */
	short	ismtyp;		/* CONST derived from MTYP */
	int	val;		/* value attribute */
	int	ln;		/* line number */
	int	indstep;	/* part of d_step sequence */
	int	uiid;		/* inline id, if non-zero */
	struct Symbol	*fn;	/* file name */
	struct Symbol	*sym;	/* symbol reference */
        struct Sequence *sq;	/* sequence */
        struct SeqList	*sl;	/* sequence list */
	struct Lextok	*lft, *rgt; /* children in parse tree */
} Lextok;

typedef struct Slicer {
	Lextok	*n;		/* global var, usable as slice criterion */
	short	code;		/* type of use: DEREF_USE or normal USE */
	short	used;		/* set when handled */
	struct Slicer *nxt;	/* linked list */
} Slicer;

typedef struct Access {
	struct Symbol	*who;	/* proctype name of accessor */
	struct Symbol	*what;	/* proctype name of accessed */
	int	cnt, typ;	/* parameter nr and, e.g., 's' or 'r' */
	struct Access	*lnk;	/* linked list */
} Access;

typedef struct Symbol {
	char	*name;
	int	Nid;		/* unique number for the name */
	unsigned short	type;	/* bit,short,.., chan,struct  */
	unsigned char	hidden; /* bit-flags:
				   1=hide, 2=show,
				   4=bit-equiv,   8=byte-equiv,
				  16=formal par, 32=inline par,
				  64=treat as if local; 128=read at least once
				 */
	unsigned char	colnr;	/* for use with xspin during simulation */
	unsigned char	isarray; /* set if decl specifies array bound */
	unsigned char	*bscp;	/* block scope */
	int	nbits;		/* optional width specifier */
	int	nel;		/* 1 if scalar, >1 if array   */
	int	setat;		/* last depth value changed   */
	int	*val;		/* runtime value(s), initl 0  */
	Lextok	**Sval;	/* values for structures */

	int	xu;		/* exclusive r or w by 1 pid  */
	struct Symbol	*xup[2];  /* xr or xs proctype  */
	struct Access	*access;/* e.g., senders and receives of chan */
	Lextok	*ini;	/* initial value, or chan-def */
	Lextok	*Slst;	/* template for structure if struct */
	struct Symbol	*Snm;	/* name of the defining struct */
	struct Symbol	*owner;	/* set for names of subfields in typedefs */
	struct Symbol	*context; /* 0 if global, or procname */
	struct Symbol	*next;	/* linked list */
} Symbol;

typedef struct Ordered {	/* links all names in Symbol table */ 
	struct Symbol	*entry;
	struct Ordered	*next;
} Ordered;

typedef struct Queue {
	short	qid;		/* runtime q index */
	int	qlen;		/* nr messages stored */
	int	nslots, nflds;	/* capacity, flds/slot */
	int	setat;		/* last depth value changed */
	int	*fld_width;	/* type of each field */
	int	*contents;	/* the values stored */
	int	*stepnr;	/* depth when each msg was sent */
	struct Queue	*nxt;	/* linked list */
} Queue;

typedef struct FSM_state {	/* used in pangen5.c - dataflow */
	int from;		/* state number */
	int seen;		/* used for dfs */
	int in;			/* nr of incoming edges */
	int cr;			/* has reachable 1-relevant successor */
	int scratch;
	unsigned long *dom, *mod; /* to mark dominant nodes */
	struct FSM_trans *t;	/* outgoing edges */
	struct FSM_trans *p;	/* incoming edges, predecessors */
	struct FSM_state *nxt;	/* linked list of all states */
} FSM_state;

typedef struct FSM_trans {	/* used in pangen5.c - dataflow */
	int to;
	short	relevant;	/* when sliced */
	short	round;		/* ditto: iteration when marked */
	struct FSM_use *Val[2];	/* 0=reads, 1=writes */
	struct Element *step;
	struct FSM_trans *nxt;
} FSM_trans;

typedef struct FSM_use {	/* used in pangen5.c - dataflow */
	Lextok *n;
	Symbol *var;
	int special;
	struct FSM_use *nxt;
} FSM_use;

typedef struct Element {
	Lextok	*n;		/* defines the type & contents */
	int	Seqno;		/* identifies this el within system */
	int	seqno;		/* identifies this el within a proc */
	int	merge;		/* set by -O if step can be merged */
	int	merge_start;
	int	merge_single;
	short	merge_in;	/* nr of incoming edges */
	short	merge_mark;	/* state was generated in merge sequence */
	unsigned int	status;	/* used by analyzer generator  */
	struct FSM_use	*dead;	/* optional dead variable list */
	struct SeqList	*sub;	/* subsequences, for compounds */
	struct SeqList	*esc;	/* zero or more escape sequences */
	struct Element	*Nxt;	/* linked list - for global lookup */
	struct Element	*nxt;	/* linked list - program structure */
} Element;

typedef struct Sequence {
	Element	*frst;
	Element	*last;		/* links onto continuations */
	Element *extent;	/* last element in original */
	int	maxel;		/* 1+largest id in sequence */
} Sequence;

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

typedef struct Label {
	Symbol	*s;
	Symbol	*c;
	Element	*e;
	int	uiid;		/* non-zero if label appears in an inline */
	int	visible;	/* label referenced in claim (slice relevant) */
	struct Label	*nxt;
} Label;

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

typedef struct RunList {
	Symbol	*n;		/* name            */
	int	tn;		/* ordinal of type */
	int	pid;		/* process id      */
	int	priority;	/* for simulations only */
	enum btypes b;		/* the type of process */
	Element	*pc;		/* current stmnt   */
	Sequence *ps;		/* used by analyzer generator */
	Lextok	*prov;		/* provided clause */
	Symbol	*symtab;	/* local variables */
	struct RunList	*nxt;	/* linked list */
} RunList;

typedef struct ProcList {
	Symbol	*n;		/* name       */
	Lextok	*p;		/* parameters */
	Sequence *s;		/* body       */
	Lextok	*prov;		/* provided clause */
	enum btypes b;		/* e.g., claim, trace, proc */
	short	tn;		/* ordinal number */
	unsigned char	det;	/* deterministic */
	unsigned char   unsafe;	/* contains global var inits */
	struct ProcList	*nxt;	/* linked list */
} ProcList;

typedef	Lextok *Lexptr;

#define YYSTYPE	Lexptr

#define ZN	(Lextok *)0
#define ZS	(Symbol *)0
#define ZE	(Element *)0

#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 I_GLOB    8		/* inherited global ref    */
#define DONE2	 16		/* used in putcode and main*/
#define D_ATOM	 32		/* deterministic atomic    */
#define ENDSTATE 64		/* normal endstate         */
#define CHECK2	128		/* status bits for remote ref check */
#define CHECK3	256		/* status bits for atomic jump check */

#define Nhash	255    		/* slots in symbol hash-table */

#define XR	  	1	/* non-shared receive-only */
#define XS	  	2	/* non-shared send-only    */
#define XX	  	4	/* overrides XR or XS tag  */

#define CODE_FRAG	2	/* auto-numbered code-fragment */
#define CODE_DECL	4	/* auto-numbered c_decl */
#define PREDEF	  	3	/* predefined name: _p, _last */

#define UNSIGNED  5		/* val defines width in bits */
#define BIT	  1		/* also equal to width in bits */
#define BYTE	  8		/* ditto */
#define SHORT	 16		/* ditto */
#define INT	 32		/* ditto */
#define	CHAN	 64		/* not */
#define STRUCT	128		/* user defined structure name */

#define SOMETHINGBIG	65536
#define RATHERSMALL	512
#define MAXSCOPESZ	1024

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

#ifdef PC
	#define MFLAGS	"wb"
#else
	#define MFLAGS	"w"
#endif

/***** prototype definitions *****/
Element	*eval_sub(Element *);
Element	*get_lab(Lextok *, int);
Element	*huntele(Element *, int, int);
Element	*huntstart(Element *);
Element	*target(Element *);

Lextok	*do_unless(Lextok *, Lextok *);
Lextok	*expand(Lextok *, int);
Lextok	*getuname(Symbol *);
Lextok	*mk_explicit(Lextok *, int, int);
Lextok	*nn(Lextok *, int, Lextok *, Lextok *);
Lextok	*rem_lab(Symbol *, Lextok *, Symbol *);
Lextok	*rem_var(Symbol *, Lextok *, Symbol *, Lextok *);
Lextok	*tail_add(Lextok *, Lextok *);

ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *, enum btypes);

SeqList	*seqlist(Sequence *, SeqList *);
Sequence *close_seq(int);

Symbol	*break_dest(void);
Symbol	*findloc(Symbol *);
Symbol	*has_lab(Element *, int);
Symbol	*lookup(char *);
Symbol	*prep_inline(Symbol *, Lextok *);

char	*emalloc(size_t);
long	Rand(void);

int	any_oper(Lextok *, int);
int	any_undo(Lextok *);
int	c_add_sv(FILE *);
int	cast_val(int, int, int);
int	checkvar(Symbol *, int);
int	Cnt_flds(Lextok *);
int	cnt_mpars(Lextok *);
int	complete_rendez(void);
int	enable(Lextok *);
int	Enabled0(Element *);
int	eval(Lextok *);
int	find_lab(Symbol *, Symbol *, int);
int	find_maxel(Symbol *);
int	full_name(FILE *, Lextok *, Symbol *, int);
int	getlocal(Lextok *);
int	getval(Lextok *);
int	glob_inline(char *);
int	has_typ(Lextok *, int);
int	in_bound(Symbol *, int);
int	interprint(FILE *, Lextok *);
int	printm(FILE *, Lextok *);
int	is_inline(void);
int	ismtype(char *);
int	isproctype(char *);
int	isutype(char *);
int	Lval_struct(Lextok *, Symbol *, int, int);
int	main(int, char **);
int	pc_value(Lextok *);
int	pid_is_claim(int);
int	proper_enabler(Lextok *);
int	putcode(FILE *, Sequence *, Element *, int, int, int);
int	q_is_sync(Lextok *);
int	qlen(Lextok *);
int	qfull(Lextok *);
int	qmake(Symbol *);
int	qrecv(Lextok *, int);
int	qsend(Lextok *);
int	remotelab(Lextok *);
int	remotevar(Lextok *);
int	Rval_struct(Lextok *, Symbol *, int);
int	setlocal(Lextok *, int);
int	setval(Lextok *, int);
int	sputtype(char *, int);
int	Sym_typ(Lextok *);
int	tl_main(int, char *[]);
int	Width_set(int *, int, Lextok *);
int	yyparse(void);
int	yywrap(void);
int	yylex(void);

void	AST_track(Lextok *, int);
void	add_seq(Lextok *);
void	alldone(int);
void	announce(char *);
void	c_state(Symbol *, Symbol *, Symbol *);
void	c_add_def(FILE *);
void	c_add_loc(FILE *, char *);
void	c_add_locinit(FILE *, int, char *);
void	c_add_use(FILE *);
void	c_chandump(FILE *);
void	c_preview(void);
void	c_struct(FILE *, char *, Symbol *);
void	c_track(Symbol *, Symbol *, Symbol *);
void	c_var(FILE *, char *, Symbol *);
void	c_wrapper(FILE *);
void	chanaccess(void);
void	check_param_count(int, Lextok *);
void	checkrun(Symbol *, int);
void	comment(FILE *, Lextok *, int);
void	cross_dsteps(Lextok *, Lextok *);
void	disambiguate(void);
void	doq(Symbol *, int, RunList *);
void	dotag(FILE *, char *);
void	do_locinits(FILE *);
void	do_var(FILE *, int, char *, Symbol *, char *, char *, char *);
void	dump_struct(Symbol *, char *, RunList *);
void	dumpclaims(FILE *, int, char *);
void	dumpglobals(void);
void	dumplabels(void);
void	dumplocal(RunList *);
void	dumpsrc(int, int);
void	fatal(char *, char *);
void	fix_dest(Symbol *, Symbol *);
void	genaddproc(void);
void	genaddqueue(void);
void	gencodetable(FILE *);
void	genheader(void);
void	genother(void);
void	gensrc(void);
void	gensvmap(void);
void	genunio(void);
void	ini_struct(Symbol *);
void	loose_ends(void);
void	make_atomic(Sequence *, int);
void	match_trail(void);
void	no_side_effects(char *);
void	nochan_manip(Lextok *, Lextok *, int);
void	non_fatal(char *, char *);
void	ntimes(FILE *, int, int, char *c[]);
void	open_seq(int);
void	p_talk(Element *, int);
void	pickup_inline(Symbol *, Lextok *);
void	plunk_c_decls(FILE *);
void	plunk_c_fcts(FILE *);
void	plunk_expr(FILE *, char *);
void	plunk_inline(FILE *, char *, int, int);
void	prehint(Symbol *);
void	preruse(FILE *, Lextok *);
void	prune_opts(Lextok *);
void	pstext(int, char *);
void	pushbreak(void);
void	putname(FILE *, char *, Lextok *, int, char *);
void	putremote(FILE *, Lextok *, int);
void	putskip(int);
void	putsrc(Element *);
void	putstmnt(FILE *, Lextok *, int);
void	putunames(FILE *);
void	rem_Seq(void);
void	runnable(ProcList *, int, int);
void	sched(void);
void	setaccess(Symbol *, Symbol *, int, int);
void	set_lab(Symbol *, Element *);
void	setmtype(Lextok *);
void	setpname(Lextok *);
void	setptype(Lextok *, int, Lextok *);
void	setuname(Lextok *);
void	setutype(Lextok *, Symbol *, Lextok *);
void	setxus(Lextok *, int);
void	show_lab(void);
void	Srand(unsigned);
void	start_claim(int);
void	struct_name(Lextok *, Symbol *, int, char *);
void	symdump(void);
void	symvar(Symbol *);
void	sync_product(void);
void	trackchanuse(Lextok *, Lextok *, int);
void	trackvar(Lextok *, Lextok *);
void	trackrun(Lextok *);
void	trapwonly(Lextok * /* , char * */);	/* spin.y and main.c */
void	typ2c(Symbol *);
void	typ_ck(int, int, char *);
void	undostmnt(Lextok *, int);
void	unrem_Seq(void);
void	unskip(int);
void	varcheck(Element *, Element *);
void	whoruns(int);
void	wrapup(int);
void	yyerror(char *, ...);
#endif