/***** spin: spin.h *****/ /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. *//* This software is for educational purposes only. *//* Permission is given to distribute this code provided that this intro- *//* ductory message is not removed and no monies are exchanged. *//* No guarantee is expressed or implied by the distribution of this code. *//* Software 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 and/or questions to: gerard@research.att.com */ #include <stdio.h>#include <string.h>#define Version "Spin Version 2.2.2 -- 24 February 1995" 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 */ struct Symbol *fn; /* file name */ struct Symbol *sym; /* fields 1,4-7 used as union */ struct Sequence *sq; /* sequence */ struct SeqList *sl; /* sequence list */ struct Lextok *lft, *rgt; /* children in parse tree */} Lextok; typedef struct Symbol { char *name; int Nid; /* unique number for the name */ short type; /* bit,short,.., chan,struct */ short hidden; /* 1 if outside statevector */ int nel; /* 1 if scalar, >1 if array */ int setat; /* last depth value changed */ int *val; /* runtime value(s), initl 0 */ struct Lextok **Sval; /* values for structures */ int xu; /* exclusive r or w by 1 pid */ struct Symbol *xup[2]; /* xr or xs proctype */ struct Lextok *ini; /* initial value, or chan-def */ struct 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 Queue { short qid; /* runtime q index */ short qlen; /* nr messages stored */ short nslots, nflds; /* capacity, flds/slot */ int setat; /* last depth value changed */ int *fld_width; /* type of each field */ int *contents; /* the actual buffer */ struct Queue *nxt; /* linked list */} Queue; typedef struct Element { Lextok *n; /* defines the type & contents */ int Seqno; /* identifies this el within system */ int seqno; /* identifies this el within a proc */ unsigned char status; /* used by analyzer generator */ 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 the sequence */} 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 tn; /* ordinal of type */ int pid; /* process id */ Element *pc; /* current stmnt */ Sequence *ps; /* used by analyzer generator */ Symbol *symtab; /* local variables */ struct RunList *nxt; /* linked list */} RunList; typedef struct ProcList { Symbol *n; /* name */ Lextok *p; /* parameters */ Sequence *s; /* body */ int tn; /* ordinal number */ 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 CHECK1 64#define CHECK2 128 #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 PREDEF 3 /* predefined names: _p, _last */#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 max(a,b) (((a)<(b)) ? (b) : (a)) /***** ANSI C - prototype definitions *****/Element *colons(Lextok *);Element *eval_sub(Element *);Element *get_lab(Lextok *, int);Element *huntele(Element *, int);Element *huntstart(Element *);Element *if_seq(Lextok *);Element *new_el(Lextok *);Element *target(Element *);Element *unless_seq(Lextok *); Lextok *cpnn(Lextok *, int, int, int);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 *tail_add(Lextok *, Lextok *); ProcList *ready(Symbol *, Lextok *, Sequence *); SeqList *seqlist(Sequence *, SeqList *);Sequence *close_seq(int); Symbol *break_dest(void);Symbol *findloc(Symbol *);Symbol *has_lab(Element *);Symbol *lookup(char *); char *emalloc(int);long time(long *); int a_rcv(Queue *, Lextok *, int);int a_snd(Queue *, Lextok *);int any_oper(Lextok *, int);int any_undo(Lextok *);int atoi(char *);int blog(int);int cast_val(int, int);int check_name(char *);int checkvar(Symbol *, int);int Cnt_flds(Lextok *);int cnt_mpars(Lextok *);int complete_rendez(void);int dolocal(int, int, char *);int enable(Symbol *, Lextok *);int Enabled0(Element *);int Enabled1(Lextok *);int eval(Lextok *);int eval_sync(Element *);int fill_struct(Symbol *, int, int, char *, Symbol **);int find_lab(Symbol *, Symbol *);int find_maxel(Symbol *);int fproc(char *);int getglobal(Lextok *);int getlocal(Lextok *);int getval(Lextok *);int getweight(Lextok *);int has_global(Lextok *);int has_typ(Lextok *, int);int hash(char *);int interprint(Lextok *);int ismtype(char *);int isproctype(char *);int isutype(char *);int Lval_struct(Lextok *, Symbol *, int, int);int newer(char *, char *);int pc_value(Lextok *);int putcode(FILE *, Sequence *, Element *, int);int puttype(int);int q_is_sync(Lextok *);int qlen(Lextok *);int qfull(Lextok *);int qmake(Symbol *);int qrecv(Lextok *, int);int qsend(Lextok *);int Rval_struct(Lextok *, Symbol *, int);int remotelab(Lextok *);int remotevar(Lextok *);int sa_snd(Queue *, Lextok *);int s_snd(Queue *, Lextok *);int scan_seq(Sequence *);int setglobal(Lextok *, int);int setlocal(Lextok *, int);int setval(Lextok *, int);int sputtype(char *, int);int Sym_typ(Lextok *);int symbolic(FILE *, Lextok *);int Width_set(int *, int, Lextok *);int yyparse(void);int yywrap(void);int yylex(void);long Rand(void); void add_el(Element *, Sequence *);void add_seq(Lextok *);void addsymbol(RunList *, Symbol *);void attach_escape(Sequence *, Sequence *);void check_proc(Lextok *, int);void comment(FILE *, Lextok *, int);void comwork(FILE *, Lextok *, int);void cross_dsteps(Lextok *, Lextok *);void do_init(Symbol *);void do_var(int, char *, Symbol *);void doglobal(int);void dohidden(void);void doq(Symbol *, int, RunList *);void dump_struct(Symbol *, char *, RunList *);void dumpclaims(FILE *, int, char *);void dumpglobals(void);void dumplabels(void);void dumplocal(RunList *);void dumpskip(int, int);void dumpsrc(int, int);void end_labs(Symbol *, int);void exit(int);void explain(int);void fatal(char *, char *);void full_name(FILE *, Lextok *, Symbol *, int);void fix_dest(Symbol *, Symbol *);void genaddproc(void);void genaddqueue(void);void genconditionals(void);void genheader(void);void genother(void);void gensrc(void);void genunio(void);void ini_struct(Symbol *);void lost_trail(void);void main(int, char **);void make_atomic(Sequence *, int);void mark_seq(Sequence *);void match_trail(void);void mov_lab(Symbol *, Element *, Element *);void ncases(FILE *, int, int, int, char **);void non_fatal(char *, char *);void ntimes(FILE *, int, int, char *c[]);void open_seq(int);void p_talk(Element *, int);void patch_atomic(Sequence *);void pushbreak(void);void put_pinit(Element *, Symbol *, Lextok *, int);void put_ptype(char *, int, int, int);void put_seq(Sequence *, int, int);void putCode(FILE *, Element *, Element *, Element *, int);void putname(FILE *, char *, Lextok *, int, char *);void putnr(int);void putproc(Symbol *, Sequence *, int, int, int);void putremote(FILE *, Lextok *, int);void putskip(int);void putsrc(int, int);void putstmnt(FILE *, Lextok *, int);void putunames(FILE *);void rem_Seq(void);void runnable(ProcList *);void sched(void);void set_lab(Symbol *, Element *);void setmtype(Lextok *);void setparams(RunList *, ProcList *, Lextok *);void setpname(Lextok *);void setptype(Lextok *, int, Lextok *); /* predefined types */void setuname(Lextok *); /* userdefined types */void setutype(Lextok *, Symbol *, Lextok *);void setxus(Lextok *, int);void sr_mesg(int, int);void sr_talk(Lextok *, int, char *, char *, int, Queue *);void Srand(unsigned);void start_claim(int);void symdump(void);void formdump(void);void struct_name(Lextok *, Symbol *, int);void symvar(Symbol *);void talk(RunList *);void typ_ck(int, int, char *);void typ2c(Symbol *);void undostmnt(Lextok *, int);void unrem_Seq(void);void unskip(int);void varcheck(Element *, Element *);void walk_atomic(Element *, Element *, int);void whichproc(int);void whoruns(int);void wrapup(int);void yyerror(char *, ...);
/***** spin: spin.h *****/
/* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */
/* This software is for educational purposes only. */
/* Permission is given to distribute this code provided that this intro- */
/* ductory message is not removed and no monies are exchanged. */
/* No guarantee is expressed or implied by the distribution of this code. */
/* Software 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 and/or questions to: gerard@research.att.com */
#include <stdio.h>
#include <string.h>
#define Version "Spin Version 2.2.2 -- 24 February 1995"
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 */
struct Symbol *fn; /* file name */
struct Symbol *sym; /* fields 1,4-7 used as union */
struct Sequence *sq; /* sequence */
struct SeqList *sl; /* sequence list */
struct Lextok *lft, *rgt; /* children in parse tree */
} Lextok;
typedef struct Symbol {
char *name;
int Nid; /* unique number for the name */
short type; /* bit,short,.., chan,struct */
short hidden; /* 1 if outside statevector */
int nel; /* 1 if scalar, >1 if array */
int setat; /* last depth value changed */
int *val; /* runtime value(s), initl 0 */
struct Lextok **Sval; /* values for structures */
int xu; /* exclusive r or w by 1 pid */
struct Symbol *xup[2]; /* xr or xs proctype */
struct Lextok *ini; /* initial value, or chan-def */
struct 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 Queue {
short qid; /* runtime q index */
short qlen; /* nr messages stored */
short nslots, nflds; /* capacity, flds/slot */
int setat; /* last depth value changed */
int *fld_width; /* type of each field */
int *contents; /* the actual buffer */
struct Queue *nxt; /* linked list */
} Queue;
typedef struct Element {
Lextok *n; /* defines the type & contents */
int Seqno; /* identifies this el within system */
int seqno; /* identifies this el within a proc */
unsigned char status; /* used by analyzer generator */
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 the sequence */
} 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 tn; /* ordinal of type */
int pid; /* process id */
Element *pc; /* current stmnt */
Sequence *ps; /* used by analyzer generator */
Symbol *symtab; /* local variables */
struct RunList *nxt; /* linked list */
} RunList;
typedef struct ProcList {
Symbol *n; /* name */
Lextok *p; /* parameters */
Sequence *s; /* body */
int tn; /* ordinal number */
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 CHECK1 64
#define CHECK2 128
#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 PREDEF 3 /* predefined names: _p, _last */
#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 max(a,b) (((a)<(b)) ? (b) : (a))
/***** ANSI C - prototype definitions *****/
Element *colons(Lextok *);
Element *eval_sub(Element *);
Element *get_lab(Lextok *, int);
Element *huntele(Element *, int);
Element *huntstart(Element *);
Element *if_seq(Lextok *);
Element *new_el(Lextok *);
Element *target(Element *);
Element *unless_seq(Lextok *);
Lextok *cpnn(Lextok *, int, int, int);
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 *tail_add(Lextok *, Lextok *);
ProcList *ready(Symbol *, Lextok *, Sequence *);
SeqList *seqlist(Sequence *, SeqList *);
Sequence *close_seq(int);
Symbol *break_dest(void);
Symbol *findloc(Symbol *);
Symbol *has_lab(Element *);
Symbol *lookup(char *);
char *emalloc(int);
long time(long *);
int a_rcv(Queue *, Lextok *, int);
int a_snd(Queue *, Lextok *);
int any_oper(Lextok *, int);
int any_undo(Lextok *);
int atoi(char *);
int blog(int);
int cast_val(int, int);
int check_name(char *);
int checkvar(Symbol *, int);
int Cnt_flds(Lextok *);
int cnt_mpars(Lextok *);
int complete_rendez(void);
int dolocal(int, int, char *);
int enable(Symbol *, Lextok *);
int Enabled0(Element *);
int Enabled1(Lextok *);
int eval(Lextok *);
int eval_sync(Element *);
int fill_struct(Symbol *, int, int, char *, Symbol **);
int find_lab(Symbol *, Symbol *);
int find_maxel(Symbol *);
int fproc(char *);
int getglobal(Lextok *);
int getlocal(Lextok *);
int getval(Lextok *);
int getweight(Lextok *);
int has_global(Lextok *);
int has_typ(Lextok *, int);
int hash(char *);
int interprint(Lextok *);
int ismtype(char *);
int isproctype(char *);
int isutype(char *);
int Lval_struct(Lextok *, Symbol *, int, int);
int newer(char *, char *);
int pc_value(Lextok *);
int putcode(FILE *, Sequence *, Element *, int);
int puttype(int);
int q_is_sync(Lextok *);
int qlen(Lextok *);
int qfull(Lextok *);
int qmake(Symbol *);
int qrecv(Lextok *, int);
int qsend(Lextok *);
int Rval_struct(Lextok *, Symbol *, int);
int remotelab(Lextok *);
int remotevar(Lextok *);
int sa_snd(Queue *, Lextok *);
int s_snd(Queue *, Lextok *);
int scan_seq(Sequence *);
int setglobal(Lextok *, int);
int setlocal(Lextok *, int);
int setval(Lextok *, int);
int sputtype(char *, int);
int Sym_typ(Lextok *);
int symbolic(FILE *, Lextok *);
int Width_set(int *, int, Lextok *);
int yyparse(void);
int yywrap(void);
int yylex(void);
long Rand(void);
void add_el(Element *, Sequence *);
void add_seq(Lextok *);
void addsymbol(RunList *, Symbol *);
void attach_escape(Sequence *, Sequence *);
void check_proc(Lextok *, int);
void comment(FILE *, Lextok *, int);
void comwork(FILE *, Lextok *, int);
void cross_dsteps(Lextok *, Lextok *);
void do_init(Symbol *);
void do_var(int, char *, Symbol *);
void doglobal(int);
void dohidden(void);
void doq(Symbol *, int, RunList *);
void dump_struct(Symbol *, char *, RunList *);
void dumpclaims(FILE *, int, char *);
void dumpglobals(void);
void dumplabels(void);
void dumplocal(RunList *);
void dumpskip(int, int);
void dumpsrc(int, int);
void end_labs(Symbol *, int);
void exit(int);
void explain(int);
void fatal(char *, char *);
void full_name(FILE *, Lextok *, Symbol *, int);
void fix_dest(Symbol *, Symbol *);
void genaddproc(void);
void genaddqueue(void);
void genconditionals(void);
void genheader(void);
void genother(void);
void gensrc(void);
void genunio(void);
void ini_struct(Symbol *);
void lost_trail(void);
void main(int, char **);
void make_atomic(Sequence *, int);
void mark_seq(Sequence *);
void match_trail(void);
void mov_lab(Symbol *, Element *, Element *);
void ncases(FILE *, int, int, int, char **);
void non_fatal(char *, char *);
void ntimes(FILE *, int, int, char *c[]);
void open_seq(int);
void p_talk(Element *, int);
void patch_atomic(Sequence *);
void pushbreak(void);
void put_pinit(Element *, Symbol *, Lextok *, int);
void put_ptype(char *, int, int, int);
void put_seq(Sequence *, int, int);
void putCode(FILE *, Element *, Element *, Element *, int);
void putname(FILE *, char *, Lextok *, int, char *);
void putnr(int);
void putproc(Symbol *, Sequence *, int, int, int);
void putremote(FILE *, Lextok *, int);
void putskip(int);
void putsrc(int, int);
void putstmnt(FILE *, Lextok *, int);
void putunames(FILE *);
void rem_Seq(void);
void runnable(ProcList *);
void sched(void);
void set_lab(Symbol *, Element *);
void setmtype(Lextok *);
void setparams(RunList *, ProcList *, Lextok *);
void setpname(Lextok *);
void setptype(Lextok *, int, Lextok *); /* predefined types */
void setuname(Lextok *); /* userdefined types */
void setutype(Lextok *, Symbol *, Lextok *);
void setxus(Lextok *, int);
void sr_mesg(int, int);
void sr_talk(Lextok *, int, char *, char *, int, Queue *);
void Srand(unsigned);
void start_claim(int);
void symdump(void);
void formdump(void);
void struct_name(Lextok *, Symbol *, int);
void symvar(Symbol *);
void talk(RunList *);
void typ_ck(int, int, char *);
void typ2c(Symbol *);
void undostmnt(Lextok *, int);
void unrem_Seq(void);
void unskip(int);
void varcheck(Element *, Element *);
void walk_atomic(Element *, Element *, int);
void whichproc(int);
void whoruns(int);
void wrapup(int);
void yyerror(char *, ...);