alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Tweak precedence of "->" and <->.

Browse source 
* src/ltlparse/ltlparse.yy: Change the precedence of "->" and
"<->" so that "a & b -> c" is interpreted as "(a & b) -> c"
instead of "a & (b -> c)".  The new interpretation is more
intuitive, and matches that of LBTT.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-06 17:39:42 +01:00
parent cc66aff634
commit 351a8076d0
2 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2010-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Tweak precedence of "->" and <->.
* src/ltlparse/ltlparse.yy: Change the precedence of "->" and
"<->" so that "a & b -> c" is interpreted as "(a & b) -> c"
instead of "a & (b -> c)". The new interpretation is more
intuitive, and matches that of LBTT.
2010-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* bench/ltl2tgba/formulae.ltl: Fix three formulae to match the * bench/ltl2tgba/formulae.ltl: Fix three formulae to match the

4
src/ltlparse/ltlparse.yy
View file

@ -1,4 +1,4 @@
/* Copyright (C) 2009 Laboratoire de Recherche et Développement /* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
** de l'Epita (LRDE). ** de l'Epita (LRDE).
/* Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de /* Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -93,10 +93,10 @@ using namespace spot::ltl;
/* Priorities. */ /* Priorities. */
/* Logical operators. */ /* Logical operators. */
%left OP_IMPLIES OP_EQUIV
%left OP_OR %left OP_OR
%left OP_XOR %left OP_XOR
%left OP_AND %left OP_AND
%left OP_IMPLIES OP_EQUIV
/* LTL operators. */ /* LTL operators. */
%left OP_U OP_R %left OP_U OP_R