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 ini_buchi(void); 104 void ini_cache(void); 105 void ini_rewrt(void); 106 void ini_trans(void); 107 void releasenode(int, Node *); 108 void tfree(void *); 109 void tl_explain(int); 110 void tl_UnGetchar(void); 111 void tl_parse(void); 112 void tl_yyerror(char *); 113 void trans(Node *); 114 115 #define ZN (Node *)0 116 #define ZS (Symbol *)0 117 #define Nhash 255 /* must match size in spin.h */ 118 #define True tl_nn(TRUE, ZN, ZN) 119 #define False tl_nn(FALSE, ZN, ZN) 120 #define Not(a) push_negation(tl_nn(NOT, a, ZN)) 121 #define rewrite(n) canonical(right_linked(n)) 122 123 typedef Node *Nodeptr; 124 #define YYSTYPE Nodeptr 125 126 #define Debug(x) { if (tl_verbose) printf(x); } 127 #define Debug2(x,y) { if (tl_verbose) printf(x,y); } 128 #define Dump(x) { if (tl_verbose) dump(x); } 129 #define Explain(x) { if (tl_verbose) tl_explain(x); } 130 131 #define Assert(x, y) { if (!(x)) { tl_explain(y); \ 132 Fatal(": assertion failed\n",(char *)0); } } 133