| 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 releasenode(int, Node *); |
| 104 | void tfree(void *); |
| 105 | void tl_explain(int); |
| 106 | void tl_UnGetchar(void); |
| 107 | void tl_parse(void); |
| 108 | void tl_yyerror(char *); |
| 109 | void trans(Node *); |
| 110 | |
| 111 | #define ZN (Node *)0 |
| 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)) |
| 118 | |
| 119 | typedef Node *Nodeptr; |
| 120 | #define YYSTYPE Nodeptr |
| 121 | |
| 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); } |
| 126 | |
| 127 | #define Assert(x, y) { if (!(x)) { tl_explain(y); \ |
| 128 | Fatal(": assertion failed\n",(char *)0); } } |