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
);
This page took 0.033123 seconds and 4 git commands to generate.