[lttv.git] / trunk / verif / Spin / Src5.1.6 / tl.h

/***** 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	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); } }
Commit	Line	Data
0b55f123	1	/*** tl_spin: tl.h ***/
	2
	3	/* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories. */
	4	/* All Rights Reserved. This software is for educational purposes only. */
	5	/* No guarantee whatsoever is expressed or implied by the distribution of */
	6	/* this code. Permission is given to distribute this code provided that */
	7	/* this introductory message is not removed and no monies are exchanged. */
	8	/* Software written by Gerard J. Holzmann. For tool documentation see: */
	9	/* http://spinroot.com/ */
	10	/* Send all bug-reports and/or questions to: bugs@spinroot.com */
	11
	12	/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
	13	/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
	14
	15	#include <stdio.h>
	16	#include <string.h>
	17
	18	typedef struct Symbol {
	19	char *name;
	20	struct Symbol next; / linked list, symbol table */
	21	} Symbol;
	22
	23	typedef struct Node {
	24	short ntyp; /* node type */
	25	struct Symbol *sym;
	26	struct Node lft; / tree */
	27	struct Node rgt; / tree */
	28	struct Node nxt; / if linked list */
	29	} Node;
	30
	31	typedef struct Graph {
	32	Symbol *name;
	33	Symbol *incoming;
	34	Symbol *outgoing;
	35	Symbol *oldstring;
	36	Symbol *nxtstring;
	37	Node *New;
	38	Node *Old;
	39	Node *Other;
	40	Node *Next;
	41	unsigned char isred[64], isgrn[64];
	42	unsigned char redcnt, grncnt;
	43	unsigned char reachable;
	44	struct Graph *nxt;
	45	} Graph;
	46
	47	typedef struct Mapping {
	48	char *from;
	49	Graph *to;
	50	struct Mapping *nxt;
	51	} Mapping;
	52
	53	enum {
	54	ALWAYS=257,
	55	AND, /* 258 */
	56	EQUIV, /* 259 */
	57	EVENTUALLY, /* 260 */
	58	FALSE, /* 261 */
	59	IMPLIES, /* 262 */
	60	NOT, /* 263 */
	61	OR, /* 264 */
	62	PREDICATE, /* 265 */
	63	TRUE, /* 266 */
	64	U_OPER, /* 267 */
65	V_OPER /* 268 */
66	#ifdef NXT
67	, NEXT /* 269 */
68	#endif
69	};
70
71	Node Canonical(Node );
72	Node canonical(Node );
73	Node cached(Node );
74	Node dupnode(Node );
75	Node getnode(Node );
76	Node in_cache(Node );
77	Node push_negation(Node );
78	Node right_linked(Node );
79	Node tl_nn(int, Node , Node *);
80
81	Symbol tl_lookup(char );
82	Symbol getsym(Symbol );
83	Symbol DoDump(Node );
84
85	extern char emalloc(size_t); / in main.c */
86
87	int anywhere(int, Node , Node );
88	int dump_cond(Node , Node , int);
89	int hash(char ); / in sym.c */
90	int isalnum_(int); /* in spinlex.c */
91	int isequal(Node , Node );
92	int tl_Getchar(void);
93
94	void *tl_emalloc(int);
95	void a_stats(void);
96	void addtrans(Graph , char , Node , char );
97	void cache_stats(void);
98	void dump(Node *);
99	void exit(int);
100	void Fatal(char , char );
101	void fatal(char , char );
102	void fsm_print(void);
103	void releasenode(int, Node *);
104	void tfree(void *);
105	void tl_explain(int);
106	void tl_UnGetchar(void);
107	void tl_parse(void);
108	void tl_yyerror(char *);
109	void trans(Node *);
110
111	#define ZN (Node *)0
112	#define ZS (Symbol *)0
113	#define Nhash 255 /* must match size in spin.h */
114	#define True tl_nn(TRUE, ZN, ZN)
115	#define False tl_nn(FALSE, ZN, ZN)
116	#define Not(a) push_negation(tl_nn(NOT, a, ZN))
117	#define rewrite(n) canonical(right_linked(n))
118
119	typedef Node *Nodeptr;
120	#define YYSTYPE Nodeptr
121
122	#define Debug(x) { if (tl_verbose) printf(x); }
123	#define Debug2(x,y) { if (tl_verbose) printf(x,y); }
124	#define Dump(x) { if (tl_verbose) dump(x); }
125	#define Explain(x) { if (tl_verbose) tl_explain(x); }
126
127	#define Assert(x, y) { if (!(x)) { tl_explain(y); \
128	Fatal(": assertion failed\n",(char *)0); } }