1 /***** tl_spin: tl.h *****/
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 */
12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
18 typedef struct Symbol {
20 struct Symbol *next; /* linked list, symbol table */
24 short ntyp; /* node type */
26 struct Node *lft; /* tree */
27 struct Node *rgt; /* tree */
28 struct Node *nxt; /* if linked list */
31 typedef struct Graph {
41 unsigned char isred[64], isgrn[64];
42 unsigned char redcnt, grncnt;
43 unsigned char reachable;
47 typedef struct Mapping {
71 Node *Canonical(Node *);
72 Node *canonical(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 *);
81 Symbol *tl_lookup(char *);
82 Symbol *getsym(Symbol *);
83 Symbol *DoDump(Node *);
85 char *emalloc(int); /* in main.c */
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 *);
94 void *tl_emalloc(int);
96 void addtrans(Graph *, char *, Node *, char *);
97 void cache_stats(void);
100 void Fatal(char *, char *);
101 void fatal(char *, char *);
102 void fsm_print(void);
103 void releasenode(int, Node *);
105 void tl_explain(int);
106 void tl_UnGetchar(void);
108 void tl_yyerror(char *);
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))
119 typedef Node *Nodeptr;
120 #define YYSTYPE Nodeptr
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); }
127 #define Assert(x, y) { if (!(x)) { tl_explain(y); \
128 Fatal(": assertion failed\n",(char *)0); } }