trunk/verif/Spin/Src5.1.6/tl_main.c

   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 }