+++ /dev/null
-/***** tl_spin: tl_parse.c *****/
-
-/* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories. */
-/* All Rights Reserved. This software is for educational purposes only. */
-/* No guarantee whatsoever is expressed or implied by the distribution of */
-/* this code. Permission is given to distribute this code provided that */
-/* this introductory message is not removed and no monies are exchanged. */
-/* Software written by Gerard J. Holzmann. For tool documentation see: */
-/* http://spinroot.com/ */
-/* Send all bug-reports and/or questions to: bugs@spinroot.com */
-
-/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
-/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
-
-#include "tl.h"
-
-extern int tl_yylex(void);
-extern int tl_verbose, tl_errs;
-
-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();
-#ifndef NO_OPT
- 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 */
- }
-#endif
- 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();
-#ifndef NO_OPT
- 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 */
- }
-#endif
- 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:
-#ifndef NO_OPT
- 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
-#endif
- break;
- case V_OPER:
-#ifndef NO_OPT
- 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;
- }
-#endif
- break;
- case IMPLIES:
-#ifndef NO_OPT
- if (isequal(ptr->lft, ptr->rgt))
- { ptr = True;
- break;
- }
-#endif
- ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt);
- ptr = rewrite(ptr);
- break;
- case EQUIV:
-#ifndef NO_OPT
- if (isequal(ptr->lft, ptr->rgt))
- { ptr = True;
- break;
- }
-#endif
- 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:
-#ifndef NO_OPT
- /* 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;
- }
-#endif
- break;
-
- case OR:
-#ifndef NO_OPT
- /* 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;
- }
-#endif
- 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");
- }
- if (tl_Getchar() != -1)
- { tl_yyerror("syntax error");
- tl_errs++;
- return;
- }
- trans(n);
-}
projects / lttv.git / blobdiff