123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381 |
- /***** tl_spin: tl_parse.c *****/
- /* Copyright (c) 1995-2000 by Lucent Technologies - Bell Laboratories */
- /* All Rights Reserved. This software is for educational purposes only. */
- /* Permission is given to distribute this code provided that this intro- */
- /* ductory message is not removed and no monies are exchanged. */
- /* No guarantee is expressed or implied by the distribution of this code. */
- /* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */
- /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
- /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
- /* Send bug-reports and/or questions to: gerard@research.bell-labs.com */
- #include "tl.h"
- extern int tl_yylex(void);
- extern int tl_verbose;
- int tl_yychar = 0;
- YYSTYPE tl_yylval;
- static Node *tl_formula(void);
- static Node *tl_factor(void);
- static Node *tl_level(int);
- static int prec[2][4] = {
- { U_OPER, V_OPER, 0, 0 }, /* left associative */
- { OR, AND, IMPLIES, EQUIV, }, /* left associative */
- };
- static Node *
- tl_factor(void)
- { Node *ptr = ZN;
- switch (tl_yychar) {
- case '(':
- ptr = tl_formula();
- if (tl_yychar != ')')
- tl_yyerror("expected ')'");
- tl_yychar = tl_yylex();
- break;
- case NOT:
- ptr = tl_yylval;
- tl_yychar = tl_yylex();
- ptr->lft = tl_factor();
- ptr = push_negation(ptr);
- break;
- case ALWAYS:
- tl_yychar = tl_yylex();
- ptr = tl_factor();
- if (ptr->ntyp == FALSE
- || ptr->ntyp == TRUE)
- break; /* [] false == false */
- if (ptr->ntyp == V_OPER)
- { if (ptr->lft->ntyp == FALSE)
- break; /* [][]p = []p */
- ptr = ptr->rgt; /* [] (p V q) = [] q */
- }
- ptr = tl_nn(V_OPER, False, ptr);
- break;
- #ifdef NXT
- case NEXT:
- tl_yychar = tl_yylex();
- ptr = tl_factor();
- if (ptr->ntyp == TRUE)
- break; /* X true = true */
- ptr = tl_nn(NEXT, ptr, ZN);
- break;
- #endif
- case EVENTUALLY:
- tl_yychar = tl_yylex();
- ptr = tl_factor();
- if (ptr->ntyp == TRUE
- || ptr->ntyp == FALSE)
- break; /* <> true == true */
- if (ptr->ntyp == U_OPER
- && ptr->lft->ntyp == TRUE)
- break; /* <><>p = <>p */
- if (ptr->ntyp == U_OPER)
- { /* <> (p U q) = <> q */
- ptr = ptr->rgt;
- /* fall thru */
- }
- ptr = tl_nn(U_OPER, True, ptr);
- break;
- case PREDICATE:
- ptr = tl_yylval;
- tl_yychar = tl_yylex();
- break;
- case TRUE:
- case FALSE:
- ptr = tl_yylval;
- tl_yychar = tl_yylex();
- break;
- }
- if (!ptr) tl_yyerror("expected predicate");
- #if 0
- printf("factor: ");
- tl_explain(ptr->ntyp);
- printf("\n");
- #endif
- return ptr;
- }
- static Node *
- bin_simpler(Node *ptr)
- { Node *a, *b;
- if (ptr)
- switch (ptr->ntyp) {
- case U_OPER:
- if (ptr->rgt->ntyp == TRUE
- || ptr->rgt->ntyp == FALSE
- || ptr->lft->ntyp == FALSE)
- { ptr = ptr->rgt;
- break;
- }
- if (isequal(ptr->lft, ptr->rgt))
- { /* p U p = p */
- ptr = ptr->rgt;
- break;
- }
- if (ptr->lft->ntyp == U_OPER
- && isequal(ptr->lft->lft, ptr->rgt))
- { /* (p U q) U p = (q U p) */
- ptr->lft = ptr->lft->rgt;
- break;
- }
- if (ptr->rgt->ntyp == U_OPER
- && ptr->rgt->lft->ntyp == TRUE)
- { /* p U (T U q) = (T U q) */
- ptr = ptr->rgt;
- break;
- }
- #ifdef NXT
- /* X p U X q == X (p U q) */
- if (ptr->rgt->ntyp == NEXT
- && ptr->lft->ntyp == NEXT)
- { ptr = tl_nn(NEXT,
- tl_nn(U_OPER,
- ptr->lft->lft,
- ptr->rgt->lft), ZN);
- }
- #endif
- break;
- case V_OPER:
- if (ptr->rgt->ntyp == FALSE
- || ptr->rgt->ntyp == TRUE
- || ptr->lft->ntyp == TRUE)
- { ptr = ptr->rgt;
- break;
- }
- if (isequal(ptr->lft, ptr->rgt))
- { /* p V p = p */
- ptr = ptr->rgt;
- break;
- }
- /* F V (p V q) == F V q */
- if (ptr->lft->ntyp == FALSE
- && ptr->rgt->ntyp == V_OPER)
- { ptr->rgt = ptr->rgt->rgt;
- break;
- }
- /* p V (F V q) == F V q */
- if (ptr->rgt->ntyp == V_OPER
- && ptr->rgt->lft->ntyp == FALSE)
- { ptr->lft = False;
- ptr->rgt = ptr->rgt->rgt;
- break;
- }
- break;
- case IMPLIES:
- if (isequal(ptr->lft, ptr->rgt))
- { ptr = True;
- break;
- }
- ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt);
- ptr = rewrite(ptr);
- break;
- case EQUIV:
- if (isequal(ptr->lft, ptr->rgt))
- { ptr = True;
- break;
- }
- a = rewrite(tl_nn(AND,
- dupnode(ptr->lft),
- dupnode(ptr->rgt)));
- b = rewrite(tl_nn(AND,
- Not(ptr->lft),
- Not(ptr->rgt)));
- ptr = tl_nn(OR, a, b);
- ptr = rewrite(ptr);
- break;
- case AND:
- /* p && (q U p) = p */
- if (ptr->rgt->ntyp == U_OPER
- && isequal(ptr->rgt->rgt, ptr->lft))
- { ptr = ptr->lft;
- break;
- }
- if (ptr->lft->ntyp == U_OPER
- && isequal(ptr->lft->rgt, ptr->rgt))
- { ptr = ptr->rgt;
- break;
- }
- /* p && (q V p) == q V p */
- if (ptr->rgt->ntyp == V_OPER
- && isequal(ptr->rgt->rgt, ptr->lft))
- { ptr = ptr->rgt;
- break;
- }
- if (ptr->lft->ntyp == V_OPER
- && isequal(ptr->lft->rgt, ptr->rgt))
- { ptr = ptr->lft;
- break;
- }
- /* (p U q) && (r U q) = (p && r) U q*/
- if (ptr->rgt->ntyp == U_OPER
- && ptr->lft->ntyp == U_OPER
- && isequal(ptr->rgt->rgt, ptr->lft->rgt))
- { ptr = tl_nn(U_OPER,
- tl_nn(AND, ptr->lft->lft, ptr->rgt->lft),
- ptr->lft->rgt);
- break;
- }
- /* (p V q) && (p V r) = p V (q && r) */
- if (ptr->rgt->ntyp == V_OPER
- && ptr->lft->ntyp == V_OPER
- && isequal(ptr->rgt->lft, ptr->lft->lft))
- { ptr = tl_nn(V_OPER,
- ptr->rgt->lft,
- tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt));
- break;
- }
- #ifdef NXT
- /* X p && X q == X (p && q) */
- if (ptr->rgt->ntyp == NEXT
- && ptr->lft->ntyp == NEXT)
- { ptr = tl_nn(NEXT,
- tl_nn(AND,
- ptr->rgt->lft,
- ptr->lft->lft), ZN);
- break;
- }
- #endif
- if (isequal(ptr->lft, ptr->rgt) /* (p && p) == p */
- || ptr->rgt->ntyp == FALSE /* (p && F) == F */
- || ptr->lft->ntyp == TRUE) /* (T && p) == p */
- { ptr = ptr->rgt;
- break;
- }
- if (ptr->rgt->ntyp == TRUE /* (p && T) == p */
- || ptr->lft->ntyp == FALSE) /* (F && p) == F */
- { ptr = ptr->lft;
- break;
- }
- /* (p V q) && (r U q) == p V q */
- if (ptr->rgt->ntyp == U_OPER
- && ptr->lft->ntyp == V_OPER
- && isequal(ptr->lft->rgt, ptr->rgt->rgt))
- { ptr = ptr->lft;
- break;
- }
- break;
- case OR:
- /* p || (q U p) == q U p */
- if (ptr->rgt->ntyp == U_OPER
- && isequal(ptr->rgt->rgt, ptr->lft))
- { ptr = ptr->rgt;
- break;
- }
- /* p || (q V p) == p */
- if (ptr->rgt->ntyp == V_OPER
- && isequal(ptr->rgt->rgt, ptr->lft))
- { ptr = ptr->lft;
- break;
- }
- /* (p U q) || (p U r) = p U (q || r) */
- if (ptr->rgt->ntyp == U_OPER
- && ptr->lft->ntyp == U_OPER
- && isequal(ptr->rgt->lft, ptr->lft->lft))
- { ptr = tl_nn(U_OPER,
- ptr->rgt->lft,
- tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt));
- break;
- }
- if (isequal(ptr->lft, ptr->rgt) /* (p || p) == p */
- || ptr->rgt->ntyp == FALSE /* (p || F) == p */
- || ptr->lft->ntyp == TRUE) /* (T || p) == T */
- { ptr = ptr->lft;
- break;
- }
- if (ptr->rgt->ntyp == TRUE /* (p || T) == T */
- || ptr->lft->ntyp == FALSE) /* (F || p) == p */
- { ptr = ptr->rgt;
- break;
- }
- /* (p V q) || (r V q) = (p || r) V q */
- if (ptr->rgt->ntyp == V_OPER
- && ptr->lft->ntyp == V_OPER
- && isequal(ptr->lft->rgt, ptr->rgt->rgt))
- { ptr = tl_nn(V_OPER,
- tl_nn(OR, ptr->lft->lft, ptr->rgt->lft),
- ptr->rgt->rgt);
- break;
- }
- /* (p V q) || (r U q) == r U q */
- if (ptr->rgt->ntyp == U_OPER
- && ptr->lft->ntyp == V_OPER
- && isequal(ptr->lft->rgt, ptr->rgt->rgt))
- { ptr = ptr->rgt;
- break;
- }
- break;
- }
- return ptr;
- }
- static Node *
- tl_level(int nr)
- { int i; Node *ptr = ZN;
- if (nr < 0)
- return tl_factor();
- ptr = tl_level(nr-1);
- again:
- for (i = 0; i < 4; i++)
- if (tl_yychar == prec[nr][i])
- { tl_yychar = tl_yylex();
- ptr = tl_nn(prec[nr][i],
- ptr, tl_level(nr-1));
- ptr = bin_simpler(ptr);
- goto again;
- }
- if (!ptr) tl_yyerror("syntax error");
- #if 0
- printf("level %d: ", nr);
- tl_explain(ptr->ntyp);
- printf("\n");
- #endif
- return ptr;
- }
- static Node *
- tl_formula(void)
- { tl_yychar = tl_yylex();
- return tl_level(1); /* 2 precedence levels, 1 and 0 */
- }
- void
- tl_parse(void)
- { Node *n = tl_formula();
- if (tl_verbose)
- { printf("formula: ");
- dump(n);
- printf("\n");
- }
- trans(n);
- }
|