| 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 | } |