From 351a8076d07ecae9fb5a6da1153174322ccf5965 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Mar 2010 17:39:42 +0100 Subject: [PATCH] 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. --- ChangeLog | 9 +++++++++ src/ltlparse/ltlparse.yy | 4 ++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index a56f31706..2da3577dd 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2010-03-06 Alexandre Duret-Lutz + + 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 * bench/ltl2tgba/formulae.ltl: Fix three formulae to match the diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 857c720e1..ff4874a7a 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -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). /* Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -93,10 +93,10 @@ using namespace spot::ltl; /* Priorities. */ /* Logical operators. */ +%left OP_IMPLIES OP_EQUIV %left OP_OR %left OP_XOR %left OP_AND -%left OP_IMPLIES OP_EQUIV /* LTL operators. */ %left OP_U OP_R