/***** tl_spin: tl.h *****/ /* Copyright (c) 1995-2003 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            */ /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, *//* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */ #include <stdio.h>#include <string.h> typedef struct Symbol {	char		*name;	struct Symbol	*next;	/* linked list, symbol table */} Symbol; typedef struct Node {	short		ntyp;	/* node type */	struct Symbol	*sym;	struct Node	*lft;	/* tree */	struct Node	*rgt;	/* tree */	struct Node	*nxt;	/* if linked list */} Node; typedef struct Graph {	Symbol		*name;	Symbol		*incoming;	Symbol		*outgoing;	Symbol		*oldstring;	Symbol		*nxtstring;	Node		*New;	Node		*Old;	Node		*Other;	Node		*Next;	unsigned char	isred[64], isgrn[64];	unsigned char	redcnt, grncnt;	unsigned char	reachable;	struct Graph	*nxt;} Graph; typedef struct Mapping {	char	*from;	Graph	*to;	struct Mapping	*nxt;} Mapping; enum {	ALWAYS=257,	AND,		/* 258 */	EQUIV,		/* 259 */	EVENTUALLY,	/* 260 */	FALSE,		/* 261 */	IMPLIES,	/* 262 */	NOT,		/* 263 */	OR,		/* 264 */	PREDICATE,	/* 265 */	TRUE,		/* 266 */	U_OPER,		/* 267 */	V_OPER		/* 268 */#ifdef NXT	, NEXT		/* 269 */#endif}; Node	*Canonical(Node *);Node	*canonical(Node *);Node	*cached(Node *);Node	*dupnode(Node *);Node	*getnode(Node *);Node	*in_cache(Node *);Node	*push_negation(Node *);Node	*right_linked(Node *);Node	*tl_nn(int, Node *, Node *); Symbol	*tl_lookup(char *);Symbol	*getsym(Symbol *);Symbol	*DoDump(Node *); extern char	*emalloc(size_t);	/* in main.c */ int	anywhere(int, Node *, Node *);int	dump_cond(Node *, Node *, int);int	hash(char *);	/* in sym.c */int	isalnum_(int);	/* in spinlex.c */int	isequal(Node *, Node *);int	tl_Getchar(void); void	*tl_emalloc(int);void	a_stats(void);void	addtrans(Graph *, char *, Node *, char *);void	cache_stats(void);void	dump(Node *);void	exit(int);void	Fatal(char *, char *);void	fatal(char *, char *);void	fsm_print(void);void	ini_buchi(void);void	ini_cache(void);void	ini_rewrt(void);void	ini_trans(void);void	releasenode(int, Node *);void	tfree(void *);void	tl_explain(int);void	tl_UnGetchar(void);void	tl_parse(void);void	tl_yyerror(char *);void	trans(Node *); #define ZN	(Node *)0#define ZS	(Symbol *)0#define Nhash	255    	/* must match size in spin.h */#define True	tl_nn(TRUE,  ZN, ZN)#define False	tl_nn(FALSE, ZN, ZN)#define Not(a)	push_negation(tl_nn(NOT, a, ZN))#define rewrite(n)	canonical(right_linked(n)) typedef Node	*Nodeptr;#define YYSTYPE	 Nodeptr #define Debug(x)	{ if (tl_verbose) printf(x); }#define Debug2(x,y)	{ if (tl_verbose) printf(x,y); }#define Dump(x)		{ if (tl_verbose) dump(x); }#define Explain(x)	{ if (tl_verbose) tl_explain(x); } #define Assert(x, y)	{ if (!(x)) { tl_explain(y); \			  Fatal(": assertion failed\n",(char *)0); } }