0b55f123 |
1 | /***** tl_spin: tl_main.c *****/ |
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 "tl.h" |
16 | |
17 | extern FILE *tl_out; |
18 | |
19 | int newstates = 0; /* debugging only */ |
20 | int tl_errs = 0; |
21 | int tl_verbose = 0; |
22 | int tl_terse = 0; |
23 | int tl_clutter = 0; |
24 | unsigned long All_Mem = 0; |
25 | |
26 | static char uform[4096]; |
27 | static int hasuform=0, cnt=0; |
28 | |
29 | extern void cache_stats(void); |
30 | extern void a_stats(void); |
31 | |
32 | int |
33 | tl_Getchar(void) |
34 | { |
35 | if (cnt < hasuform) |
36 | return uform[cnt++]; |
37 | cnt++; |
38 | return -1; |
39 | } |
40 | |
41 | void |
42 | tl_balanced(void) |
43 | { int i; |
44 | int k = 0; |
45 | |
46 | for (i = 0; i < hasuform; i++) |
47 | { if (uform[i] == '(') |
48 | { k++; |
49 | } else if (uform[i] == ')') |
50 | { k--; |
51 | } } |
52 | if (k != 0) |
53 | { tl_errs++; |
54 | tl_yyerror("parentheses not balanced"); |
55 | } |
56 | } |
57 | |
58 | void |
59 | put_uform(void) |
60 | { |
61 | fprintf(tl_out, "%s", uform); |
62 | } |
63 | |
64 | void |
65 | tl_UnGetchar(void) |
66 | { |
67 | if (cnt > 0) cnt--; |
68 | } |
69 | |
70 | static void |
71 | tl_stats(void) |
72 | { extern int Stack_mx; |
73 | printf("total memory used: %9ld\n", All_Mem); |
74 | printf("largest stack sze: %9d\n", Stack_mx); |
75 | cache_stats(); |
76 | a_stats(); |
77 | } |
78 | |
79 | int |
80 | tl_main(int argc, char *argv[]) |
81 | { int i; |
82 | extern int verbose, xspin; |
83 | tl_verbose = verbose; |
84 | tl_clutter = 1-xspin; /* use -X -f to turn off uncluttering */ |
85 | |
86 | while (argc > 1 && argv[1][0] == '-') |
87 | { switch (argv[1][1]) { |
88 | case 'd': newstates = 1; /* debugging mode */ |
89 | break; |
90 | case 'f': argc--; argv++; |
91 | for (i = 0; i < argv[1][i]; i++) |
92 | { if (argv[1][i] == '\t' |
93 | || argv[1][i] == '\"' |
94 | || argv[1][i] == '\n') |
95 | argv[1][i] = ' '; |
96 | } |
97 | strcpy(uform, argv[1]); |
98 | hasuform = (int) strlen(uform); |
99 | break; |
100 | case 'v': tl_verbose++; |
101 | break; |
102 | case 'n': tl_terse = 1; |
103 | break; |
104 | default : printf("spin -f: saw '-%c'\n", argv[1][1]); |
105 | goto nogood; |
106 | } |
107 | argc--; argv++; |
108 | } |
109 | if (hasuform == 0) |
110 | { |
111 | nogood: printf("usage:\tspin [-v] [-n] -f formula\n"); |
112 | printf(" -v verbose translation\n"); |
113 | printf(" -n normalize tl formula and exit\n"); |
114 | exit(1); |
115 | } |
116 | tl_balanced(); |
117 | |
118 | if (tl_errs == 0) |
119 | tl_parse(); |
120 | |
121 | if (tl_verbose) tl_stats(); |
122 | return tl_errs; |
123 | } |
124 | |
125 | #define Binop(a) \ |
126 | fprintf(tl_out, "("); \ |
127 | dump(n->lft); \ |
128 | fprintf(tl_out, a); \ |
129 | dump(n->rgt); \ |
130 | fprintf(tl_out, ")") |
131 | |
132 | void |
133 | dump(Node *n) |
134 | { |
135 | if (!n) return; |
136 | |
137 | switch(n->ntyp) { |
138 | case OR: Binop(" || "); break; |
139 | case AND: Binop(" && "); break; |
140 | case U_OPER: Binop(" U "); break; |
141 | case V_OPER: Binop(" V "); break; |
142 | #ifdef NXT |
143 | case NEXT: |
144 | fprintf(tl_out, "X"); |
145 | fprintf(tl_out, " ("); |
146 | dump(n->lft); |
147 | fprintf(tl_out, ")"); |
148 | break; |
149 | #endif |
150 | case NOT: |
151 | fprintf(tl_out, "!"); |
152 | fprintf(tl_out, " ("); |
153 | dump(n->lft); |
154 | fprintf(tl_out, ")"); |
155 | break; |
156 | case FALSE: |
157 | fprintf(tl_out, "false"); |
158 | break; |
159 | case TRUE: |
160 | fprintf(tl_out, "true"); |
161 | break; |
162 | case PREDICATE: |
163 | fprintf(tl_out, "(%s)", n->sym->name); |
164 | break; |
165 | case -1: |
166 | fprintf(tl_out, " D "); |
167 | break; |
168 | default: |
169 | printf("Unknown token: "); |
170 | tl_explain(n->ntyp); |
171 | break; |
172 | } |
173 | } |
174 | |
175 | void |
176 | tl_explain(int n) |
177 | { |
178 | switch (n) { |
179 | case ALWAYS: printf("[]"); break; |
180 | case EVENTUALLY: printf("<>"); break; |
181 | case IMPLIES: printf("->"); break; |
182 | case EQUIV: printf("<->"); break; |
183 | case PREDICATE: printf("predicate"); break; |
184 | case OR: printf("||"); break; |
185 | case AND: printf("&&"); break; |
186 | case NOT: printf("!"); break; |
187 | case U_OPER: printf("U"); break; |
188 | case V_OPER: printf("V"); break; |
189 | #ifdef NXT |
190 | case NEXT: printf("X"); break; |
191 | #endif |
192 | case TRUE: printf("true"); break; |
193 | case FALSE: printf("false"); break; |
194 | case ';': printf("end of formula"); break; |
195 | default: printf("%c", n); break; |
196 | } |
197 | } |
198 | |
199 | static void |
200 | tl_non_fatal(char *s1, char *s2) |
201 | { extern int tl_yychar; |
202 | int i; |
203 | |
204 | printf("tl_spin: "); |
205 | if (s2) |
206 | printf(s1, s2); |
207 | else |
208 | printf(s1); |
209 | if (tl_yychar != -1 && tl_yychar != 0) |
210 | { printf(", saw '"); |
211 | tl_explain(tl_yychar); |
212 | printf("'"); |
213 | } |
214 | printf("\ntl_spin: %s\n---------", uform); |
215 | for (i = 0; i < cnt; i++) |
216 | printf("-"); |
217 | printf("^\n"); |
218 | fflush(stdout); |
219 | tl_errs++; |
220 | } |
221 | |
222 | void |
223 | tl_yyerror(char *s1) |
224 | { |
225 | Fatal(s1, (char *) 0); |
226 | } |
227 | |
228 | void |
229 | Fatal(char *s1, char *s2) |
230 | { |
231 | tl_non_fatal(s1, s2); |
232 | /* tl_stats(); */ |
233 | exit(1); |
234 | } |