1 /***** tl_spin: tl.h *****/ 2 3 /* 4 * This file is part of the public release of Spin. It is subject to the 5 * terms in the LICENSE file that is included in this source directory. 6 * Tool documentation is available at http://spinroot.com 7 * 8 * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, 9 * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. 10 */ 11 12 #ifndef TLH 13 #define TLH 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 , CEXPR /* 270 */ 70 }; 71 72 Node *Canonical(Node *); 73 Node *canonical(Node *); 74 Node *cached(Node *); 75 Node *dupnode(Node *); 76 Node *getnode(Node *); 77 Node *in_cache(Node *); 78 Node *push_negation(Node *); 79 Node *right_linked(Node *); 80 Node *tl_nn(int, Node *, Node *); 81 82 Symbol *tl_lookup(char *); 83 Symbol *getsym(Symbol *); 84 Symbol *DoDump(Node *); 85 86 extern char *emalloc(size_t); /* in main.c */ 87 88 extern unsigned int hash(const char *); /* in sym.c */ 89 90 int anywhere(int, Node *, Node *); 91 int dump_cond(Node *, Node *, int); 92 int isalnum_(int); /* in spinlex.c */ 93 int isequal(Node *, Node *); 94 int tl_Getchar(void); 95 96 void *tl_emalloc(int); 97 void *tl_erealloc(void*, int, int); 98 void a_stats(void); 99 void addtrans(Graph *, char *, Node *, char *); 100 void cache_stats(void); 101 void dump(Node *); 102 void exit(int); 103 void Fatal(char *, char *); 104 void fatal(char *, char *); 105 void fsm_print(void); 106 void ini_buchi(void); 107 void ini_cache(void); 108 void ini_rewrt(void); 109 void ini_trans(void); 110 void releasenode(int, Node *); 111 void tfree(void *); 112 void tl_explain(int); 113 void tl_UnGetchar(void); 114 void tl_parse(void); 115 void tl_yyerror(char *); 116 void trans(Node *); 117 118 #define ZN (Node *)0 119 #define ZS (Symbol *)0 120 #define Nhash 255 /* must match size in spin.h */ 121 #define True tl_nn(TRUE, ZN, ZN) 122 #define False tl_nn(FALSE, ZN, ZN) 123 #define Not(a) push_negation(tl_nn(NOT, a, ZN)) 124 #define rewrite(n) canonical(right_linked(n)) 125 126 typedef Node *Nodeptr; 127 #define YYSTYPE Nodeptr 128 129 #define Debug(x) { if (tl_verbose) printf(x); } 130 #define Debug2(x,y) { if (tl_verbose) printf(x,y); } 131 #define Dump(x) { if (tl_verbose) dump(x); } 132 #define Explain(x) { if (tl_verbose) tl_explain(x); } 133 134 #define Assert(x, y) { if (!(x)) { tl_explain(y); \ 135 Fatal(": assertion failed\n",(char *)0); } } 136 137 #endif 138