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

   1 /***** tl_spin: tl_parse.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 int      tl_yylex(void);
  18 extern int      tl_verbose, tl_errs;
  19
  20 int     tl_yychar = 0;
  21 YYSTYPE tl_yylval;
  22
  23 static Node     *tl_formula(void);
  24 static Node     *tl_factor(void);
  25 static Node     *tl_level(int);
  26
  27 static int      prec[2][4] = {
  28         { U_OPER,  V_OPER, 0, 0 },      /* left associative */
  29         { OR, AND, IMPLIES, EQUIV, },   /* left associative */
  30 };
  31
  32 static Node *
  33 tl_factor(void)
  34 {       Node *ptr = ZN;
  35
  36         switch (tl_yychar) {
  37         case '(':
  38                 ptr = tl_formula();
  39                 if (tl_yychar != ')')
  40                         tl_yyerror("expected ')'");
  41                 tl_yychar = tl_yylex();
  42                 break;
  43         case NOT:
  44                 ptr = tl_yylval;
  45                 tl_yychar = tl_yylex();
  46                 ptr->lft = tl_factor();
  47                 ptr = push_negation(ptr);
  48                 break;
  49         case ALWAYS:
  50                 tl_yychar = tl_yylex();
  51
  52                 ptr = tl_factor();
  53 #ifndef NO_OPT
  54                 if (ptr->ntyp == FALSE
  55                 ||  ptr->ntyp == TRUE)
  56                         break;  /* [] false == false */
  57
  58                 if (ptr->ntyp == V_OPER)
  59                 {       if (ptr->lft->ntyp == FALSE)
  60                                 break;  /* [][]p = []p */
  61
  62                         ptr = ptr->rgt; /* [] (p V q) = [] q */
  63                 }
  64 #endif
  65                 ptr = tl_nn(V_OPER, False, ptr);
  66                 break;
  67 #ifdef NXT
  68         case NEXT:
  69                 tl_yychar = tl_yylex();
  70                 ptr = tl_factor();
  71                 if (ptr->ntyp == TRUE)
  72                         break;  /* X true = true */
  73                 ptr = tl_nn(NEXT, ptr, ZN);
  74                 break;
  75 #endif
  76         case EVENTUALLY:
  77                 tl_yychar = tl_yylex();
  78
  79                 ptr = tl_factor();
  80 #ifndef NO_OPT
  81                 if (ptr->ntyp == TRUE
  82                 ||  ptr->ntyp == FALSE)
  83                         break;  /* <> true == true */
  84
  85                 if (ptr->ntyp == U_OPER
  86                 &&  ptr->lft->ntyp == TRUE)
  87                         break;  /* <><>p = <>p */
  88
  89                 if (ptr->ntyp == U_OPER)
  90                 {       /* <> (p U q) = <> q */
  91                         ptr = ptr->rgt;
  92                         /* fall thru */
  93                 }
  94 #endif
  95                 ptr = tl_nn(U_OPER, True, ptr);
  96
  97                 break;
  98         case PREDICATE:
  99                 ptr = tl_yylval;
 100                 tl_yychar = tl_yylex();
 101                 break;
 102         case TRUE:
 103         case FALSE:
 104                 ptr = tl_yylval;
 105                 tl_yychar = tl_yylex();
 106                 break;
 107         }
 108         if (!ptr) tl_yyerror("expected predicate");
 109 #if 0
 110         printf("factor: ");
 111         tl_explain(ptr->ntyp);
 112         printf("\n");
 113 #endif
 114         return ptr;
 115 }
 116
 117 static Node *
 118 bin_simpler(Node *ptr)
 119 {       Node *a, *b;
 120
 121         if (ptr)
 122         switch (ptr->ntyp) {
 123         case U_OPER:
 124 #ifndef NO_OPT
 125                 if (ptr->rgt->ntyp == TRUE
 126                 ||  ptr->rgt->ntyp == FALSE
 127                 ||  ptr->lft->ntyp == FALSE)
 128                 {       ptr = ptr->rgt;
 129                         break;
 130                 }
 131                 if (isequal(ptr->lft, ptr->rgt))
 132                 {       /* p U p = p */
 133                         ptr = ptr->rgt;
 134                         break;
 135                 }
 136                 if (ptr->lft->ntyp == U_OPER
 137                 &&  isequal(ptr->lft->lft, ptr->rgt))
 138                 {       /* (p U q) U p = (q U p) */
 139                         ptr->lft = ptr->lft->rgt;
 140                         break;
 141                 }
 142                 if (ptr->rgt->ntyp == U_OPER
 143                 &&  ptr->rgt->lft->ntyp == TRUE)
 144                 {       /* p U (T U q)  = (T U q) */
 145                         ptr = ptr->rgt;
 146                         break;
 147                 }
 148 #ifdef NXT
 149                 /* X p U X q == X (p U q) */
 150                 if (ptr->rgt->ntyp == NEXT
 151                 &&  ptr->lft->ntyp == NEXT)
 152                 {       ptr = tl_nn(NEXT,
 153                                 tl_nn(U_OPER,
 154                                         ptr->lft->lft,
 155                                         ptr->rgt->lft), ZN);
 156                 }
 157 #endif
 158 #endif
 159                 break;
 160         case V_OPER:
 161 #ifndef NO_OPT
 162                 if (ptr->rgt->ntyp == FALSE
 163                 ||  ptr->rgt->ntyp == TRUE
 164                 ||  ptr->lft->ntyp == TRUE)
 165                 {       ptr = ptr->rgt;
 166                         break;
 167                 }
 168                 if (isequal(ptr->lft, ptr->rgt))
 169                 {       /* p V p = p */
 170                         ptr = ptr->rgt;
 171                         break;
 172                 }
 173                 /* F V (p V q) == F V q */
 174                 if (ptr->lft->ntyp == FALSE
 175                 &&  ptr->rgt->ntyp == V_OPER)
 176                 {       ptr->rgt = ptr->rgt->rgt;
 177                         break;
 178                 }
 179                 /* p V (F V q) == F V q */
 180                 if (ptr->rgt->ntyp == V_OPER
 181                 &&  ptr->rgt->lft->ntyp == FALSE)
 182                 {       ptr->lft = False;
 183                         ptr->rgt = ptr->rgt->rgt;
 184                         break;
 185                 }
 186 #endif
 187                 break;
 188         case IMPLIES:
 189 #ifndef NO_OPT
 190                 if (isequal(ptr->lft, ptr->rgt))
 191                 {       ptr = True;
 192                         break;
 193                 }
 194 #endif
 195                 ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt);
 196                 ptr = rewrite(ptr);
 197                 break;
 198         case EQUIV:
 199 #ifndef NO_OPT
 200                 if (isequal(ptr->lft, ptr->rgt))
 201                 {       ptr = True;
 202                         break;
 203                 }
 204 #endif
 205                 a = rewrite(tl_nn(AND,
 206                         dupnode(ptr->lft),
 207                         dupnode(ptr->rgt)));
 208                 b = rewrite(tl_nn(AND,
 209                         Not(ptr->lft),
 210                         Not(ptr->rgt)));
 211                 ptr = tl_nn(OR, a, b);
 212                 ptr = rewrite(ptr);
 213                 break;
 214         case AND:
 215 #ifndef NO_OPT
 216                 /* p && (q U p) = p */
 217                 if (ptr->rgt->ntyp == U_OPER
 218                 &&  isequal(ptr->rgt->rgt, ptr->lft))
 219                 {       ptr = ptr->lft;
 220                         break;
 221                 }
 222                 if (ptr->lft->ntyp == U_OPER
 223                 &&  isequal(ptr->lft->rgt, ptr->rgt))
 224                 {       ptr = ptr->rgt;
 225                         break;
 226                 }
 227
 228                 /* p && (q V p) == q V p */
 229                 if (ptr->rgt->ntyp == V_OPER
 230                 &&  isequal(ptr->rgt->rgt, ptr->lft))
 231                 {       ptr = ptr->rgt;
 232                         break;
 233                 }
 234                 if (ptr->lft->ntyp == V_OPER
 235                 &&  isequal(ptr->lft->rgt, ptr->rgt))
 236                 {       ptr = ptr->lft;
 237                         break;
 238                 }
 239
 240                 /* (p U q) && (r U q) = (p && r) U q*/
 241                 if (ptr->rgt->ntyp == U_OPER
 242                 &&  ptr->lft->ntyp == U_OPER
 243                 &&  isequal(ptr->rgt->rgt, ptr->lft->rgt))
 244                 {       ptr = tl_nn(U_OPER,
 245                                 tl_nn(AND, ptr->lft->lft, ptr->rgt->lft),
 246                                 ptr->lft->rgt);
 247                         break;
 248                 }
 249
 250                 /* (p V q) && (p V r) = p V (q && r) */
 251                 if (ptr->rgt->ntyp == V_OPER
 252                 &&  ptr->lft->ntyp == V_OPER
 253                 &&  isequal(ptr->rgt->lft, ptr->lft->lft))
 254                 {       ptr = tl_nn(V_OPER,
 255                                 ptr->rgt->lft,
 256                                 tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt));
 257                         break;
 258                 }
 259 #ifdef NXT
 260                 /* X p && X q == X (p && q) */
 261                 if (ptr->rgt->ntyp == NEXT
 262                 &&  ptr->lft->ntyp == NEXT)
 263                 {       ptr = tl_nn(NEXT,
 264                                 tl_nn(AND,
 265                                         ptr->rgt->lft,
 266                                         ptr->lft->lft), ZN);
 267                         break;
 268                 }
 269 #endif
 270
 271                 if (isequal(ptr->lft, ptr->rgt) /* (p && p) == p */
 272                 ||  ptr->rgt->ntyp == FALSE     /* (p && F) == F */
 273                 ||  ptr->lft->ntyp == TRUE)     /* (T && p) == p */
 274                 {       ptr = ptr->rgt;
 275                         break;
 276                 }
 277                 if (ptr->rgt->ntyp == TRUE      /* (p && T) == p */
 278                 ||  ptr->lft->ntyp == FALSE)    /* (F && p) == F */
 279                 {       ptr = ptr->lft;
 280                         break;
 281                 }
 282
 283                 /* (p V q) && (r U q) == p V q */
 284                 if (ptr->rgt->ntyp == U_OPER
 285                 &&  ptr->lft->ntyp == V_OPER
 286                 &&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
 287                 {       ptr = ptr->lft;
 288                         break;
 289                 }
 290 #endif
 291                 break;
 292
 293         case OR:
 294 #ifndef NO_OPT
 295                 /* p || (q U p) == q U p */
 296                 if (ptr->rgt->ntyp == U_OPER
 297                 &&  isequal(ptr->rgt->rgt, ptr->lft))
 298                 {       ptr = ptr->rgt;
 299                         break;
 300                 }
 301
 302                 /* p || (q V p) == p */
 303                 if (ptr->rgt->ntyp == V_OPER
 304                 &&  isequal(ptr->rgt->rgt, ptr->lft))
 305                 {       ptr = ptr->lft;
 306                         break;
 307                 }
 308
 309                 /* (p U q) || (p U r) = p U (q || r) */
 310                 if (ptr->rgt->ntyp == U_OPER
 311                 &&  ptr->lft->ntyp == U_OPER
 312                 &&  isequal(ptr->rgt->lft, ptr->lft->lft))
 313                 {       ptr = tl_nn(U_OPER,
 314                                 ptr->rgt->lft,
 315                                 tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt));
 316                         break;
 317                 }
 318
 319                 if (isequal(ptr->lft, ptr->rgt) /* (p || p) == p */
 320                 ||  ptr->rgt->ntyp == FALSE     /* (p || F) == p */
 321                 ||  ptr->lft->ntyp == TRUE)     /* (T || p) == T */
 322                 {       ptr = ptr->lft;
 323                         break;
 324                 }
 325                 if (ptr->rgt->ntyp == TRUE      /* (p || T) == T */
 326                 ||  ptr->lft->ntyp == FALSE)    /* (F || p) == p */
 327                 {       ptr = ptr->rgt;
 328                         break;
 329                 }
 330
 331                 /* (p V q) || (r V q) = (p || r) V q */
 332                 if (ptr->rgt->ntyp == V_OPER
 333                 &&  ptr->lft->ntyp == V_OPER
 334                 &&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
 335                 {       ptr = tl_nn(V_OPER,
 336                                 tl_nn(OR, ptr->lft->lft, ptr->rgt->lft),
 337                                 ptr->rgt->rgt);
 338                         break;
 339                 }
 340
 341                 /* (p V q) || (r U q) == r U q */
 342                 if (ptr->rgt->ntyp == U_OPER
 343                 &&  ptr->lft->ntyp == V_OPER
 344                 &&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
 345                 {       ptr = ptr->rgt;
 346                         break;
 347                 }
 348 #endif
 349                 break;
 350         }
 351         return ptr;
 352 }
 353
 354 static Node *
 355 tl_level(int nr)
 356 {       int i; Node *ptr = ZN;
 357
 358         if (nr < 0)
 359                 return tl_factor();
 360
 361         ptr = tl_level(nr-1);
 362 again:
 363         for (i = 0; i < 4; i++)
 364                 if (tl_yychar == prec[nr][i])
 365                 {       tl_yychar = tl_yylex();
 366                         ptr = tl_nn(prec[nr][i],
 367                                 ptr, tl_level(nr-1));
 368                         ptr = bin_simpler(ptr);
 369                         goto again;
 370                 }
 371         if (!ptr) tl_yyerror("syntax error");
 372 #if 0
 373         printf("level %d:       ", nr);
 374         tl_explain(ptr->ntyp);
 375         printf("\n");
 376 #endif
 377         return ptr;
 378 }
 379
 380 static Node *
 381 tl_formula(void)
 382 {       tl_yychar = tl_yylex();
 383         return tl_level(1);     /* 2 precedence levels, 1 and 0 */
 384 }
 385
 386 void
 387 tl_parse(void)
 388 {       Node *n = tl_formula();
 389         if (tl_verbose)
 390         {       printf("formula: ");
 391                 dump(n);
 392                 printf("\n");
 393         }
 394         if (tl_Getchar() != -1)
 395         {       tl_yyerror("syntax error");
 396                 tl_errs++;
 397                 return;
 398         }
 399         trans(n);
 400 }