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