Subversion Repositories planix.SVN

/***** 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); } }