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 36 tl_Getchar(void) 37 { 38 if (cnt < hasuform) 39 return uform[cnt++]; 40 cnt++; 41 return -1; 42 } 43 44 int 45 tl_peek(int n) 46 { 47 if (cnt+n < hasuform) 48 { return uform[cnt+n]; 49 } 50 return -1; 51 } 52 53 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 71 put_uform(void) 72 { 73 fprintf(tl_out, "%s", uform); 74 } 75 76 void 77 tl_UnGetchar(void) 78 { 79 if (cnt > 0) cnt--; 80 } 81 82 static 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 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 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 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 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 256 tl_yyerror(char *s1) 257 { 258 Fatal(s1, (char *) 0); 259 } 260 261 void 262 Fatal(char *s1, char *s2) 263 { 264 tl_non_fatal(s1, s2); 265 /* tl_stats(); */ 266 exit(1); 267 } 268