1 /***** tl_spin: tl_main.c *****/ 2 3 /* Copyright (c) 1995-2000 by Lucent Technologies - Bell Laboratories */ 4 /* All Rights Reserved. This software is for educational purposes only. */ 5 /* Permission is given to distribute this code provided that this intro- */ 6 /* ductory message is not removed and no monies are exchanged. */ 7 /* No guarantee is expressed or implied by the distribution of this code. */ 8 /* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */ 9 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */ 10 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */ 11 /* Send bug-reports and/or questions to: gerard@research.bell-labs.com */ 12 13 #include "tl.h" 14 15 extern FILE *tl_out; 16 17 int newstates = 0; /* debugging only */ 18 int tl_errs = 0; 19 int tl_verbose = 0; 20 int tl_terse = 0; 21 int tl_clutter = 0; 22 unsigned long All_Mem = 0; 23 24 static char uform[4096]; 25 static int hasuform=0, cnt=0; 26 27 static void tl_stats(void); 28 static void non_fatal(char *, char *); 29 30 int 31 tl_Getchar(void) 32 { 33 if (cnt < hasuform) 34 return uform[cnt++]; 35 cnt++; 36 return -1; 37 } 38 39 void 40 put_uform(void) 41 { 42 fprintf(tl_out, "%s", uform); 43 } 44 45 void 46 tl_UnGetchar(void) 47 { 48 if (cnt > 0) cnt--; 49 } 50 51 int 52 tl_main(int argc, char *argv[]) 53 { int i; 54 extern int verbose, xspin; 55 tl_verbose = verbose; 56 tl_clutter = 1-xspin; /* use -X -f to turn off uncluttering */ 57 58 while (argc > 1 && argv[1][0] == '-') 59 { switch (argv[1][1]) { 60 case 'd': newstates = 1; /* debugging mode */ 61 break; 62 case 'f': argc--; argv++; 63 for (i = 0; i < argv[1][i]; i++) 64 { if (argv[1][i] == '\t' 65 || argv[1][i] == '\"' 66 || argv[1][i] == '\n') 67 argv[1][i] = ' '; 68 } 69 strcpy(uform, argv[1]); 70 hasuform = strlen(uform); 71 break; 72 case 'v': tl_verbose++; 73 break; 74 case 'n': tl_terse = 1; 75 break; 76 default : printf("spin -f: saw '-%c'\n", argv[1][1]); 77 goto nogood; 78 } 79 argc--; argv++; 80 } 81 if (hasuform == 0) 82 { 83 nogood: printf("usage:\tspin [-v] [-n] -f formula\n"); 84 printf(" -v verbose translation\n"); 85 printf(" -n normalize tl formula and exit\n"); 86 exit(1); 87 } 88 tl_parse(); 89 if (tl_verbose) tl_stats(); 90 return tl_errs; 91 } 92 93 static void 94 tl_stats(void) 95 { extern int Stack_mx; 96 printf("total memory used: %9ld\n", All_Mem); 97 printf("largest stack sze: %9d\n", Stack_mx); 98 cache_stats(); 99 a_stats(); 100 } 101 102 #define Binop(a) \ 103 fprintf(tl_out, "("); \ 104 dump(n->lft); \ 105 fprintf(tl_out, a); \ 106 dump(n->rgt); \ 107 fprintf(tl_out, ")") 108 109 void 110 dump(Node *n) 111 { 112 if (!n) return; 113 114 switch(n->ntyp) { 115 case OR: Binop(" || "); break; 116 case AND: Binop(" && "); break; 117 case U_OPER: Binop(" U "); break; 118 case V_OPER: Binop(" V "); break; 119 #ifdef NXT 120 case NEXT: 121 fprintf(tl_out, "X"); 122 fprintf(tl_out, " ("); 123 dump(n->lft); 124 fprintf(tl_out, ")"); 125 break; 126 #endif 127 case NOT: 128 fprintf(tl_out, "!"); 129 fprintf(tl_out, " ("); 130 dump(n->lft); 131 fprintf(tl_out, ")"); 132 break; 133 case FALSE: 134 fprintf(tl_out, "false"); 135 break; 136 case TRUE: 137 fprintf(tl_out, "true"); 138 break; 139 case PREDICATE: 140 fprintf(tl_out, "(%s)", n->sym->name); 141 break; 142 case -1: 143 fprintf(tl_out, " D "); 144 break; 145 default: 146 printf("Unknown token: "); 147 tl_explain(n->ntyp); 148 break; 149 } 150 } 151 152 void 153 tl_explain(int n) 154 { 155 switch (n) { 156 case ALWAYS: printf("[]"); break; 157 case EVENTUALLY: printf("<>"); break; 158 case IMPLIES: printf("->"); break; 159 case EQUIV: printf("<->"); break; 160 case PREDICATE: printf("predicate"); break; 161 case OR: printf("||"); break; 162 case AND: printf("&&"); break; 163 case NOT: printf("!"); break; 164 case U_OPER: printf("U"); break; 165 case V_OPER: printf("V"); break; 166 #ifdef NXT 167 case NEXT: printf("X"); break; 168 #endif 169 case TRUE: printf("true"); break; 170 case FALSE: printf("false"); break; 171 case ';': printf("end of formula"); break; 172 default: printf("%c", n); break; 173 } 174 } 175 176 static void 177 non_fatal(char *s1, char *s2) 178 { extern int tl_yychar; 179 int i; 180 181 printf("tl_spin: "); 182 if (s2) 183 printf(s1, s2); 184 else 185 printf(s1); 186 if (tl_yychar != -1 && tl_yychar != 0) 187 { printf(", saw '"); 188 tl_explain(tl_yychar); 189 printf("'"); 190 } 191 printf("\ntl_spin: %s\n---------", uform); 192 for (i = 0; i < cnt; i++) 193 printf("-"); 194 printf("^\n"); 195 fflush(stdout); 196 tl_errs++; 197 } 198 199 void 200 tl_yyerror(char *s1) 201 { 202 Fatal(s1, (char *) 0); 203 } 204 205 void 206 Fatal(char *s1, char *s2) 207 { 208 non_fatal(s1, s2); 209 /* tl_stats(); */ 210 exit(1); 211 } 212