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 unsigned long All_Mem = 0; 25 26 static char uform[4096]; 27 static int hasuform=0, cnt=0; 28 29 extern void cache_stats(void); 30 extern void a_stats(void); 31 32 int 33 tl_Getchar(void) 34 { 35 if (cnt < hasuform) 36 return uform[cnt++]; 37 cnt++; 38 return -1; 39 } 40 41 void 42 put_uform(void) 43 { 44 fprintf(tl_out, "%s", uform); 45 } 46 47 void 48 tl_UnGetchar(void) 49 { 50 if (cnt > 0) cnt--; 51 } 52 53 static void 54 tl_stats(void) 55 { extern int Stack_mx; 56 printf("total memory used: %9ld\n", All_Mem); 57 printf("largest stack sze: %9d\n", Stack_mx); 58 cache_stats(); 59 a_stats(); 60 } 61 62 int 63 tl_main(int argc, char *argv[]) 64 { int i; 65 extern int verbose, xspin; 66 tl_verbose = verbose; 67 tl_clutter = 1-xspin; /* use -X -f to turn off uncluttering */ 68 69 while (argc > 1 && argv[1][0] == '-') 70 { switch (argv[1][1]) { 71 case 'd': newstates = 1; /* debugging mode */ 72 break; 73 case 'f': argc--; argv++; 74 for (i = 0; i < argv[1][i]; i++) 75 { if (argv[1][i] == '\t' 76 || argv[1][i] == '\"' 77 || argv[1][i] == '\n') 78 argv[1][i] = ' '; 79 } 80 strcpy(uform, argv[1]); 81 hasuform = (int) strlen(uform); 82 break; 83 case 'v': tl_verbose++; 84 break; 85 case 'n': tl_terse = 1; 86 break; 87 default : printf("spin -f: saw '-%c'\n", argv[1][1]); 88 goto nogood; 89 } 90 argc--; argv++; 91 } 92 if (hasuform == 0) 93 { 94 nogood: printf("usage:\tspin [-v] [-n] -f formula\n"); 95 printf(" -v verbose translation\n"); 96 printf(" -n normalize tl formula and exit\n"); 97 exit(1); 98 } 99 tl_parse(); 100 if (tl_verbose) tl_stats(); 101 return tl_errs; 102 } 103 104 #define Binop(a) \ 105 fprintf(tl_out, "("); \ 106 dump(n->lft); \ 107 fprintf(tl_out, a); \ 108 dump(n->rgt); \ 109 fprintf(tl_out, ")") 110 111 void 112 dump(Node *n) 113 { 114 if (!n) return; 115 116 switch(n->ntyp) { 117 case OR: Binop(" || "); break; 118 case AND: Binop(" && "); break; 119 case U_OPER: Binop(" U "); break; 120 case V_OPER: Binop(" V "); break; 121 #ifdef NXT 122 case NEXT: 123 fprintf(tl_out, "X"); 124 fprintf(tl_out, " ("); 125 dump(n->lft); 126 fprintf(tl_out, ")"); 127 break; 128 #endif 129 case NOT: 130 fprintf(tl_out, "!"); 131 fprintf(tl_out, " ("); 132 dump(n->lft); 133 fprintf(tl_out, ")"); 134 break; 135 case FALSE: 136 fprintf(tl_out, "false"); 137 break; 138 case TRUE: 139 fprintf(tl_out, "true"); 140 break; 141 case PREDICATE: 142 fprintf(tl_out, "(%s)", n->sym->name); 143 break; 144 case -1: 145 fprintf(tl_out, " D "); 146 break; 147 default: 148 printf("Unknown token: "); 149 tl_explain(n->ntyp); 150 break; 151 } 152 } 153 154 void 155 tl_explain(int n) 156 { 157 switch (n) { 158 case ALWAYS: printf("[]"); break; 159 case EVENTUALLY: printf("<>"); break; 160 case IMPLIES: printf("->"); break; 161 case EQUIV: printf("<->"); break; 162 case PREDICATE: printf("predicate"); break; 163 case OR: printf("||"); break; 164 case AND: printf("&&"); break; 165 case NOT: printf("!"); break; 166 case U_OPER: printf("U"); break; 167 case V_OPER: printf("V"); break; 168 #ifdef NXT 169 case NEXT: printf("X"); break; 170 #endif 171 case TRUE: printf("true"); break; 172 case FALSE: printf("false"); break; 173 case ';': printf("end of formula"); break; 174 default: printf("%c", n); break; 175 } 176 } 177 178 static void 179 tl_non_fatal(char *s1, char *s2) 180 { extern int tl_yychar; 181 int i; 182 183 printf("tl_spin: "); 184 if (s2) 185 printf(s1, s2); 186 else 187 printf(s1); 188 if (tl_yychar != -1 && tl_yychar != 0) 189 { printf(", saw '"); 190 tl_explain(tl_yychar); 191 printf("'"); 192 } 193 printf("\ntl_spin: %s\n---------", uform); 194 for (i = 0; i < cnt; i++) 195 printf("-"); 196 printf("^\n"); 197 fflush(stdout); 198 tl_errs++; 199 } 200 201 void 202 tl_yyerror(char *s1) 203 { 204 Fatal(s1, (char *) 0); 205 } 206 207 void 208 Fatal(char *s1, char *s2) 209 { 210 tl_non_fatal(s1, s2); 211 /* tl_stats(); */ 212 exit(1); 213 } 214