0b55f123 |
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); } } |