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 extern char *emalloc(size_t); /* 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); } }
This page took 0.031207 seconds and 4 git commands to generate.