sys/src/cmd/spin/tl_main.c

   1 /***** tl_spin: tl_main.c *****/
   2
   3 /*
   4  * This file is part of the public release of Spin. It is subject to the
   5  * terms in the LICENSE file that is included in this source directory.
   6  * Tool documentation is available at http://spinroot.com
   7  *
   8  * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
   9  * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
  10  */
  11
  12 #include "tl.h"
  13
  14 extern FILE     *tl_out;
  15
  16 int     newstates  = 0; /* debugging only */
  17 int     tl_errs    = 0;
  18 int     tl_verbose = 0;
  19 int     tl_terse   = 0;
  20 int     tl_clutter = 0;
  21 int     state_cnt = 0;
  22
  23 unsigned long   All_Mem = 0;
  24 char    *claim_name;
  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 int
  42 tl_peek(int n)
  43 {
  44         if (cnt+n < hasuform)
  45         {       return uform[cnt+n];
  46         }
  47         return -1;
  48 }
  49
  50 void
  51 tl_balanced(void)
  52 {       int i;
  53         int k = 0;
  54
  55         for (i = 0; i < hasuform; i++)
  56         {       if (uform[i] == '(')
  57                 {       if (i > 0
  58                         && ((uform[i-1] == '"'  && uform[i+1] == '"')
  59                         ||  (uform[i-1] == '\'' && uform[i+1] == '\'')))
  60                         {       continue;
  61                         }
  62                         k++;
  63                 } else if (uform[i] == ')')
  64                 {       if (i > 0
  65                         && ((uform[i-1] == '"'  && uform[i+1] == '"')
  66                         ||  (uform[i-1] == '\'' && uform[i+1] == '\'')))
  67                         {       continue;
  68                         }
  69                         k--;
  70         }       }
  71
  72         if (k != 0)
  73         {       tl_errs++;
  74                 tl_yyerror("parentheses not balanced");
  75         }
  76 }
  77
  78 void
  79 put_uform(void)
  80 {
  81         fprintf(tl_out, "%s", uform);
  82 }
  83
  84 void
  85 tl_UnGetchar(void)
  86 {
  87         if (cnt > 0) cnt--;
  88 }
  89
  90 static void
  91 tl_stats(void)
  92 {       extern int Stack_mx;
  93         printf("total memory used: %9ld\n", All_Mem);
  94         printf("largest stack sze: %9d\n", Stack_mx);
  95         cache_stats();
  96         a_stats();
  97 }
  98
  99 int
 100 tl_main(int argc, char *argv[])
 101 {       int i;
 102         extern int xspin, s_trail;
 103
 104         tl_verbose = 0; /* was: tl_verbose = verbose; */
 105         if (xspin && s_trail)
 106         {       tl_clutter = 1;
 107                 /* generating claims for a replay should
 108                    be done the same as when generating the
 109                    pan.c that produced the error-trail */
 110         } else
 111         {       tl_clutter = 1-xspin;   /* use -X -f to turn off uncluttering */
 112         }
 113         newstates  = 0;
 114         state_cnt  = 0;
 115         tl_errs    = 0;
 116         tl_terse   = 0;
 117         All_Mem = 0;
 118         memset(uform, 0, sizeof(uform));
 119         hasuform=0;
 120         cnt=0;
 121         claim_name = (char *) 0;
 122
 123         ini_buchi();
 124         ini_cache();
 125         ini_rewrt();
 126         ini_trans();
 127
 128         while (argc > 1 && argv[1][0] == '-')
 129         {
 130                 switch (argv[1][1]) {
 131                 case 'd':       newstates = 1;  /* debugging mode */
 132                                 break;
 133                 case 'f':       argc--; argv++;
 134                                 for (i = 0; argv[1][i]; i++)
 135                                 {       if (argv[1][i] == '\t'
 136                                         ||  argv[1][i] == '\n')
 137                                                 argv[1][i] = ' ';
 138                                 }
 139                                 strcpy(uform, argv[1]);
 140                                 hasuform = (int) strlen(uform);
 141                                 break;
 142                 case 'v':       tl_verbose++;
 143                                 break;
 144                 case 'n':       tl_terse = 1;
 145                                 break;
 146                 case 'c':       argc--; argv++;
 147                                 claim_name = (char *) emalloc(strlen(argv[1])+1);
 148                                 strcpy(claim_name, argv[1]);
 149                                 break;
 150                 default :       printf("spin -f: saw '-%c'\n", argv[1][1]);
 151                                 goto nogood;
 152                 }
 153                 argc--; argv++;
 154         }
 155         if (hasuform == 0)
 156         {
 157 nogood:         printf("usage:\tspin [-v] [-n] -f formula\n");
 158                 printf("        -v verbose translation\n");
 159                 printf("        -n normalize tl formula and exit\n");
 160                 exit(1);
 161         }
 162         tl_balanced();
 163
 164         if (tl_errs == 0)
 165                 tl_parse();
 166
 167         if (tl_verbose) tl_stats();
 168         return tl_errs;
 169 }
 170
 171 #define Binop(a)                \
 172                 fprintf(tl_out, "(");   \
 173                 dump(n->lft);           \
 174                 fprintf(tl_out, a);     \
 175                 dump(n->rgt);           \
 176                 fprintf(tl_out, ")")
 177
 178 void
 179 dump(Node *n)
 180 {
 181         if (!n) return;
 182
 183         switch(n->ntyp) {
 184         case OR:        Binop(" || "); break;
 185         case AND:       Binop(" && "); break;
 186         case U_OPER:    Binop(" U ");  break;
 187         case V_OPER:    Binop(" V ");  break;
 188 #ifdef NXT
 189         case NEXT:
 190                 fprintf(tl_out, "X");
 191                 fprintf(tl_out, " (");
 192                 dump(n->lft);
 193                 fprintf(tl_out, ")");
 194                 break;
 195 #endif
 196         case NOT:
 197                 fprintf(tl_out, "!");
 198                 fprintf(tl_out, " (");
 199                 dump(n->lft);
 200                 fprintf(tl_out, ")");
 201                 break;
 202         case FALSE:
 203                 fprintf(tl_out, "false");
 204                 break;
 205         case TRUE:
 206                 fprintf(tl_out, "true");
 207                 break;
 208         case PREDICATE:
 209                 fprintf(tl_out, "(%s)", n->sym->name);
 210                 break;
 211         case CEXPR:
 212                 fprintf(tl_out, "c_expr");
 213                 fprintf(tl_out, " {");
 214                 dump(n->lft);
 215                 fprintf(tl_out, "}");
 216                 break;
 217         case -1:
 218                 fprintf(tl_out, " D ");
 219                 break;
 220         default:
 221                 printf("Unknown token: ");
 222                 tl_explain(n->ntyp);
 223                 break;
 224         }
 225 }
 226
 227 void
 228 tl_explain(int n)
 229 {
 230         switch (n) {
 231         case ALWAYS:    printf("[]"); break;
 232         case EVENTUALLY: printf("<>"); break;
 233         case IMPLIES:   printf("->"); break;
 234         case EQUIV:     printf("<->"); break;
 235         case PREDICATE: printf("predicate"); break;
 236         case OR:        printf("||"); break;
 237         case AND:       printf("&&"); break;
 238         case NOT:       printf("!"); break;
 239         case U_OPER:    printf("U"); break;
 240         case V_OPER:    printf("V"); break;
 241 #ifdef NXT
 242         case NEXT:      printf("X"); break;
 243 #endif
 244         case CEXPR:     printf("c_expr"); break;
 245         case TRUE:      printf("true"); break;
 246         case FALSE:     printf("false"); break;
 247         case ';':       printf("end of formula"); break;
 248         default:        printf("%c", n); break;
 249         }
 250 }
 251
 252 static void
 253 tl_non_fatal(char *s1, char *s2)
 254 {       extern int tl_yychar;
 255         int i;
 256
 257         printf("tl_spin: ");
 258 #if 1
 259         printf(s1, s2); /* prevent a compiler warning */
 260 #else
 261         if (s2)
 262                 printf(s1, s2);
 263         else
 264                 printf(s1);
 265 #endif
 266         if (tl_yychar != -1 && tl_yychar != 0)
 267         {       printf(", saw '");
 268                 tl_explain(tl_yychar);
 269                 printf("'");
 270         }
 271         printf("\ntl_spin: %s\n---------", uform);
 272         for (i = 0; i < cnt; i++)
 273                 printf("-");
 274         printf("^\n");
 275         fflush(stdout);
 276         tl_errs++;
 277 }
 278
 279 void
 280 tl_yyerror(char *s1)
 281 {
 282         Fatal(s1, (char *) 0);
 283 }
 284
 285 void
 286 Fatal(char *s1, char *s2)
 287 {
 288         tl_non_fatal(s1, s2);
 289         /* tl_stats(); */
 290         exit(1);
 291 }