1 /***** tl_spin: tl_main.c *****/
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 */
12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
19 int newstates = 0; /* debugging only */
24 unsigned long All_Mem = 0;
26 static char uform[4096];
27 static int hasuform=0, cnt=0;
29 extern void cache_stats(void);
30 extern void a_stats(void);
46 for (i = 0; i < hasuform; i++)
47 { if (uform[i] == '(')
49 } else if (uform[i] == ')')
54 tl_yyerror("parentheses not balanced");
61 fprintf(tl_out, "%s", uform);
72 { extern int Stack_mx;
73 printf("total memory used: %9ld\n", All_Mem);
74 printf("largest stack sze: %9d\n", Stack_mx);
80 tl_main(int argc, char *argv[])
82 extern int verbose, xspin;
84 tl_clutter = 1-xspin; /* use -X -f to turn off uncluttering */
86 while (argc > 1 && argv[1][0] == '-')
87 { switch (argv[1][1]) {
88 case 'd': newstates = 1; /* debugging mode */
90 case 'f': argc--; argv++;
91 for (i = 0; i < argv[1][i]; i++)
92 { if (argv[1][i] == '\t'
94 || argv[1][i] == '\n')
97 strcpy(uform, argv[1]);
98 hasuform = (int) strlen(uform);
100 case 'v': tl_verbose++;
102 case 'n': tl_terse = 1;
104 default : printf("spin -f: saw '-%c'\n", argv[1][1]);
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");
121 if (tl_verbose) tl_stats();
126 fprintf(tl_out, "("); \
128 fprintf(tl_out, a); \
138 case OR: Binop(" || "); break;
139 case AND: Binop(" && "); break;
140 case U_OPER: Binop(" U "); break;
141 case V_OPER: Binop(" V "); break;
144 fprintf(tl_out, "X");
145 fprintf(tl_out, " (");
147 fprintf(tl_out, ")");
151 fprintf(tl_out, "!");
152 fprintf(tl_out, " (");
154 fprintf(tl_out, ")");
157 fprintf(tl_out, "false");
160 fprintf(tl_out, "true");
163 fprintf(tl_out, "(%s)", n->sym->name);
166 fprintf(tl_out, " D ");
169 printf("Unknown token: ");
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;
190 case NEXT: printf("X"); break;
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;
200 tl_non_fatal(char *s1, char *s2)
201 { extern int tl_yychar;
209 if (tl_yychar != -1 && tl_yychar != 0)
211 tl_explain(tl_yychar);
214 printf("\ntl_spin: %s\n---------", uform);
215 for (i = 0; i < cnt; i++)
225 Fatal(s1, (char *) 0);
229 Fatal(char *s1, char *s2)
231 tl_non_fatal(s1, s2);