1 /***** tl_spin: tl_main.c *****/
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 #include "tl.h"
13
14 extern FILE *tl_out;
15
16 int newstates = 0; /* debugging only */
17 int tl_errs = 0;
18 int tl_verbose = 0;
19 int tl_terse = 0;
20 int tl_clutter = 0;
21 int state_cnt = 0;
22
23 unsigned long All_Mem = 0;
24 char *claim_name;
25
26 static char *uform;
27 static int hasuform=0, cnt=0;
28
29 extern void cache_stats(void);
30 extern void a_stats(void);
31
32 int
tl_Getchar(void)33 tl_Getchar(void)
34 {
35 if (cnt < hasuform)
36 return uform[cnt++];
37 cnt++;
38 return -1;
39 }
40
41 int
tl_peek(int n)42 tl_peek(int n)
43 {
44 if (cnt+n < hasuform)
45 { return uform[cnt+n];
46 }
47 return -1;
48 }
49
50 void
tl_balanced(void)51 tl_balanced(void)
52 { int i;
53 int k = 0;
54
55 for (i = 0; i < hasuform; i++)
56 { if (uform[i] == '(')
57 { if (i > 0
58 && ((uform[i-1] == '"' && uform[i+1] == '"')
59 || (uform[i-1] == '\'' && uform[i+1] == '\'')))
60 { continue;
61 }
62 k++;
63 } else if (uform[i] == ')')
64 { if (i > 0
65 && ((uform[i-1] == '"' && uform[i+1] == '"')
66 || (uform[i-1] == '\'' && uform[i+1] == '\'')))
67 { continue;
68 }
69 k--;
70 } }
71
72 if (k != 0)
73 { tl_errs++;
74 tl_yyerror("parentheses not balanced");
75 }
76 }
77
78 void
put_uform(void)79 put_uform(void)
80 {
81 fprintf(tl_out, "%s", uform);
82 }
83
84 void
tl_UnGetchar(void)85 tl_UnGetchar(void)
86 {
87 if (cnt > 0) cnt--;
88 }
89
90 static void
tl_stats(void)91 tl_stats(void)
92 { extern int Stack_mx;
93 printf("total memory used: %9ld\n", All_Mem);
94 printf("largest stack sze: %9d\n", Stack_mx);
95 cache_stats();
96 a_stats();
97 }
98
99 int
tl_main(int argc,char * argv[])100 tl_main(int argc, char *argv[])
101 { int i;
102 extern int xspin, s_trail;
103
104 tl_verbose = 0; /* was: tl_verbose = verbose; */
105 if (xspin && s_trail)
106 { tl_clutter = 1;
107 /* generating claims for a replay should
108 be done the same as when generating the
109 pan.c that produced the error-trail */
110 } else
111 { tl_clutter = 1-xspin; /* use -X -f to turn off uncluttering */
112 }
113 newstates = 0;
114 state_cnt = 0;
115 tl_errs = 0;
116 tl_terse = 0;
117 All_Mem = 0;
118 hasuform=0;
119 cnt=0;
120 claim_name = (char *) 0;
121
122 ini_buchi();
123 ini_cache();
124 ini_rewrt();
125 ini_trans();
126
127 while (argc > 1 && argv[1][0] == '-')
128 {
129 switch (argv[1][1]) {
130 case 'd': newstates = 1; /* debugging mode */
131 break;
132 case 'f': argc--; argv++;
133 for (i = 0; argv[1][i]; i++)
134 { if (argv[1][i] == '\t'
135 || argv[1][i] == '\n')
136 argv[1][i] = ' ';
137 }
138 size_t len = strlen(argv[1]);
139 uform = tl_emalloc(len + 1);
140 strcpy(uform, argv[1]);
141 hasuform = (int) len;
142 break;
143 case 'v': tl_verbose++;
144 break;
145 case 'n': tl_terse = 1;
146 break;
147 case 'c': argc--; argv++;
148 claim_name = (char *) emalloc(strlen(argv[1])+1);
149 strcpy(claim_name, argv[1]);
150 break;
151 default : printf("spin -f: saw '-%c'\n", argv[1][1]);
152 goto nogood;
153 }
154 argc--; argv++;
155 }
156 if (hasuform == 0)
157 {
158 nogood: printf("usage:\tspin [-v] [-n] -f formula\n");
159 printf(" -v verbose translation\n");
160 printf(" -n normalize tl formula and exit\n");
161 exit(1);
162 }
163 tl_balanced();
164
165 if (tl_errs == 0)
166 tl_parse();
167
168 if (tl_verbose) tl_stats();
169 return tl_errs;
170 }
171
172 #define Binop(a) \
173 fprintf(tl_out, "("); \
174 dump(n->lft); \
175 fprintf(tl_out, a); \
176 dump(n->rgt); \
177 fprintf(tl_out, ")")
178
179 void
dump(Node * n)180 dump(Node *n)
181 {
182 if (!n) return;
183
184 switch(n->ntyp) {
185 case OR: Binop(" || "); break;
186 case AND: Binop(" && "); break;
187 case U_OPER: Binop(" U "); break;
188 case V_OPER: Binop(" V "); break;
189 #ifdef NXT
190 case NEXT:
191 fprintf(tl_out, "X");
192 fprintf(tl_out, " (");
193 dump(n->lft);
194 fprintf(tl_out, ")");
195 break;
196 #endif
197 case NOT:
198 fprintf(tl_out, "!");
199 fprintf(tl_out, " (");
200 dump(n->lft);
201 fprintf(tl_out, ")");
202 break;
203 case FALSE:
204 fprintf(tl_out, "false");
205 break;
206 case TRUE:
207 fprintf(tl_out, "true");
208 break;
209 case PREDICATE:
210 fprintf(tl_out, "(%s)", n->sym->name);
211 break;
212 case CEXPR:
213 fprintf(tl_out, "c_expr");
214 fprintf(tl_out, " {");
215 dump(n->lft);
216 fprintf(tl_out, "}");
217 break;
218 case -1:
219 fprintf(tl_out, " D ");
220 break;
221 default:
222 printf("Unknown token: ");
223 tl_explain(n->ntyp);
224 break;
225 }
226 }
227
228 void
tl_explain(int n)229 tl_explain(int n)
230 {
231 switch (n) {
232 case ALWAYS: printf("[]"); break;
233 case EVENTUALLY: printf("<>"); break;
234 case IMPLIES: printf("->"); break;
235 case EQUIV: printf("<->"); break;
236 case PREDICATE: printf("predicate"); break;
237 case OR: printf("||"); break;
238 case AND: printf("&&"); break;
239 case NOT: printf("!"); break;
240 case U_OPER: printf("U"); break;
241 case V_OPER: printf("V"); break;
242 #ifdef NXT
243 case NEXT: printf("X"); break;
244 #endif
245 case CEXPR: printf("c_expr"); break;
246 case TRUE: printf("true"); break;
247 case FALSE: printf("false"); break;
248 case ';': printf("end of formula"); break;
249 default: printf("%c", n); break;
250 }
251 }
252
253 static void
tl_non_fatal(char * s1,char * s2)254 tl_non_fatal(char *s1, char *s2)
255 { extern int tl_yychar;
256 int i;
257
258 printf("tl_spin: ");
259 #if 1
260 printf(s1, s2); /* prevent a compiler warning */
261 #else
262 if (s2)
263 printf(s1, s2);
264 else
265 printf(s1);
266 #endif
267 if (tl_yychar != -1 && tl_yychar != 0)
268 { printf(", saw '");
269 tl_explain(tl_yychar);
270 printf("'");
271 }
272 printf("\ntl_spin: %s\n---------", uform);
273 for (i = 0; i < cnt; i++)
274 printf("-");
275 printf("^\n");
276 fflush(stdout);
277 tl_errs++;
278 }
279
280 void
tl_yyerror(char * s1)281 tl_yyerror(char *s1)
282 {
283 Fatal(s1, (char *) 0);
284 }
285
286 void
Fatal(char * s1,char * s2)287 Fatal(char *s1, char *s2)
288 {
289 tl_non_fatal(s1, s2);
290 /* tl_stats(); */
291 exit(1);
292 }
293