123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211 |
- /***** tl_spin: tl_main.c *****/
- /* Copyright (c) 1995-2000 by Lucent Technologies - Bell Laboratories */
- /* All Rights Reserved. This software is for educational purposes only. */
- /* Permission is given to distribute this code provided that this intro- */
- /* ductory message is not removed and no monies are exchanged. */
- /* No guarantee is expressed or implied by the distribution of this code. */
- /* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */
- /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
- /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
- /* Send bug-reports and/or questions to: gerard@research.bell-labs.com */
- #include "tl.h"
- extern FILE *tl_out;
- int newstates = 0; /* debugging only */
- int tl_errs = 0;
- int tl_verbose = 0;
- int tl_terse = 0;
- int tl_clutter = 0;
- unsigned long All_Mem = 0;
- static char uform[4096];
- static int hasuform=0, cnt=0;
- static void tl_stats(void);
- static void non_fatal(char *, char *);
- int
- tl_Getchar(void)
- {
- if (cnt < hasuform)
- return uform[cnt++];
- cnt++;
- return -1;
- }
- void
- put_uform(void)
- {
- fprintf(tl_out, "%s", uform);
- }
- void
- tl_UnGetchar(void)
- {
- if (cnt > 0) cnt--;
- }
- int
- tl_main(int argc, char *argv[])
- { int i;
- extern int verbose, xspin;
- tl_verbose = verbose;
- tl_clutter = 1-xspin; /* use -X -f to turn off uncluttering */
- while (argc > 1 && argv[1][0] == '-')
- { switch (argv[1][1]) {
- case 'd': newstates = 1; /* debugging mode */
- break;
- case 'f': argc--; argv++;
- for (i = 0; i < argv[1][i]; i++)
- { if (argv[1][i] == '\t'
- || argv[1][i] == '\"'
- || argv[1][i] == '\n')
- argv[1][i] = ' ';
- }
- strcpy(uform, argv[1]);
- hasuform = strlen(uform);
- break;
- case 'v': tl_verbose++;
- break;
- case 'n': tl_terse = 1;
- break;
- default : printf("spin -f: saw '-%c'\n", argv[1][1]);
- goto nogood;
- }
- argc--; argv++;
- }
- if (hasuform == 0)
- {
- nogood: printf("usage:\tspin [-v] [-n] -f formula\n");
- printf(" -v verbose translation\n");
- printf(" -n normalize tl formula and exit\n");
- exit(1);
- }
- tl_parse();
- if (tl_verbose) tl_stats();
- return tl_errs;
- }
- static void
- tl_stats(void)
- { extern int Stack_mx;
- printf("total memory used: %9ld\n", All_Mem);
- printf("largest stack sze: %9d\n", Stack_mx);
- cache_stats();
- a_stats();
- }
- #define Binop(a) \
- fprintf(tl_out, "("); \
- dump(n->lft); \
- fprintf(tl_out, a); \
- dump(n->rgt); \
- fprintf(tl_out, ")")
- void
- dump(Node *n)
- {
- if (!n) return;
- switch(n->ntyp) {
- case OR: Binop(" || "); break;
- case AND: Binop(" && "); break;
- case U_OPER: Binop(" U "); break;
- case V_OPER: Binop(" V "); break;
- #ifdef NXT
- case NEXT:
- fprintf(tl_out, "X");
- fprintf(tl_out, " (");
- dump(n->lft);
- fprintf(tl_out, ")");
- break;
- #endif
- case NOT:
- fprintf(tl_out, "!");
- fprintf(tl_out, " (");
- dump(n->lft);
- fprintf(tl_out, ")");
- break;
- case FALSE:
- fprintf(tl_out, "false");
- break;
- case TRUE:
- fprintf(tl_out, "true");
- break;
- case PREDICATE:
- fprintf(tl_out, "(%s)", n->sym->name);
- break;
- case -1:
- fprintf(tl_out, " D ");
- break;
- default:
- printf("Unknown token: ");
- tl_explain(n->ntyp);
- break;
- }
- }
- void
- tl_explain(int n)
- {
- switch (n) {
- case ALWAYS: printf("[]"); break;
- case EVENTUALLY: printf("<>"); break;
- case IMPLIES: printf("->"); break;
- case EQUIV: printf("<->"); break;
- case PREDICATE: printf("predicate"); break;
- case OR: printf("||"); break;
- case AND: printf("&&"); break;
- case NOT: printf("!"); break;
- case U_OPER: printf("U"); break;
- case V_OPER: printf("V"); break;
- #ifdef NXT
- case NEXT: printf("X"); break;
- #endif
- case TRUE: printf("true"); break;
- case FALSE: printf("false"); break;
- case ';': printf("end of formula"); break;
- default: printf("%c", n); break;
- }
- }
- static void
- non_fatal(char *s1, char *s2)
- { extern int tl_yychar;
- int i;
- printf("tl_spin: ");
- if (s2)
- printf(s1, s2);
- else
- printf(s1);
- if (tl_yychar != -1 && tl_yychar != 0)
- { printf(", saw '");
- tl_explain(tl_yychar);
- printf("'");
- }
- printf("\ntl_spin: %s\n---------", uform);
- for (i = 0; i < cnt; i++)
- printf("-");
- printf("^\n");
- fflush(stdout);
- tl_errs++;
- }
- void
- tl_yyerror(char *s1)
- {
- Fatal(s1, (char *) 0);
- }
- void
- Fatal(char *s1, char *s2)
- {
- non_fatal(s1, s2);
- /* tl_stats(); */
- exit(1);
- }
|