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 tl_balanced(void) 43 { int i; 44 int k = 0; 45 46 for (i = 0; i < hasuform; i++) 47 { if (uform[i] == '(') 48 { k++; 49 } else if (uform[i] == ')') 50 { k--; 51 } } 52 if (k != 0) 53 { tl_errs++; 54 tl_yyerror("parentheses not balanced"); 55 } 56 } 57 58 void 59 put_uform(void) 60 { 61 fprintf(tl_out, "%s", uform); 62 } 63 64 void 65 tl_UnGetchar(void) 66 { 67 if (cnt > 0) cnt--; 68 } 69 70 static void 71 tl_stats(void) 72 { extern int Stack_mx; 73 printf("total memory used: %9ld\n", All_Mem); 74 printf("largest stack sze: %9d\n", Stack_mx); 75 cache_stats(); 76 a_stats(); 77 } 78 79 int 80 tl_main(int argc, char *argv[]) 81 { int i; 82 extern int verbose, xspin; 83 tl_verbose = verbose; 84 tl_clutter = 1-xspin; /* use -X -f to turn off uncluttering */ 85 86 while (argc > 1 && argv[1][0] == '-') 87 { switch (argv[1][1]) { 88 case 'd': newstates = 1; /* debugging mode */ 89 break; 90 case 'f': argc--; argv++; 91 for (i = 0; i < argv[1][i]; i++) 92 { if (argv[1][i] == '\t' 93 || argv[1][i] == '\"' 94 || argv[1][i] == '\n') 95 argv[1][i] = ' '; 96 } 97 strcpy(uform, argv[1]); 98 hasuform = (int) strlen(uform); 99 break; 100 case 'v': tl_verbose++; 101 break; 102 case 'n': tl_terse = 1; 103 break; 104 default : printf("spin -f: saw '-%c'\n", argv[1][1]); 105 goto nogood; 106 } 107 argc--; argv++; 108 } 109 if (hasuform == 0) 110 { 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"); 114 exit(1); 115 } 116 tl_balanced(); 117 118 if (tl_errs == 0) 119 tl_parse(); 120 121 if (tl_verbose) tl_stats(); 122 return tl_errs; 123 } 124 125 #define Binop(a) \ 126 fprintf(tl_out, "("); \ 127 dump(n->lft); \ 128 fprintf(tl_out, a); \ 129 dump(n->rgt); \ 130 fprintf(tl_out, ")") 131 132 void 133 dump(Node *n) 134 { 135 if (!n) return; 136 137 switch(n->ntyp) { 138 case OR: Binop(" || "); break; 139 case AND: Binop(" && "); break; 140 case U_OPER: Binop(" U "); break; 141 case V_OPER: Binop(" V "); break; 142 #ifdef NXT 143 case NEXT: 144 fprintf(tl_out, "X"); 145 fprintf(tl_out, " ("); 146 dump(n->lft); 147 fprintf(tl_out, ")"); 148 break; 149 #endif 150 case NOT: 151 fprintf(tl_out, "!"); 152 fprintf(tl_out, " ("); 153 dump(n->lft); 154 fprintf(tl_out, ")"); 155 break; 156 case FALSE: 157 fprintf(tl_out, "false"); 158 break; 159 case TRUE: 160 fprintf(tl_out, "true"); 161 break; 162 case PREDICATE: 163 fprintf(tl_out, "(%s)", n->sym->name); 164 break; 165 case -1: 166 fprintf(tl_out, " D "); 167 break; 168 default: 169 printf("Unknown token: "); 170 tl_explain(n->ntyp); 171 break; 172 } 173 } 174 175 void 176 tl_explain(int n) 177 { 178 switch (n) { 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; 189 #ifdef NXT 190 case NEXT: printf("X"); break; 191 #endif 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; 196 } 197 } 198 199 static void 200 tl_non_fatal(char *s1, char *s2) 201 { extern int tl_yychar; 202 int i; 203 204 printf("tl_spin: "); 205 if (s2) 206 printf(s1, s2); 207 else 208 printf(s1); 209 if (tl_yychar != -1 && tl_yychar != 0) 210 { printf(", saw '"); 211 tl_explain(tl_yychar); 212 printf("'"); 213 } 214 printf("\ntl_spin: %s\n---------", uform); 215 for (i = 0; i < cnt; i++) 216 printf("-"); 217 printf("^\n"); 218 fflush(stdout); 219 tl_errs++; 220 } 221 222 void 223 tl_yyerror(char *s1) 224 { 225 Fatal(s1, (char *) 0); 226 } 227 228 void 229 Fatal(char *s1, char *s2) 230 { 231 tl_non_fatal(s1, s2); 232 /* tl_stats(); */ 233 exit(1); 234 } 235