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

Fix the computation of the length of multops.

Browse source 
* src/ltlvisit/length.cc (visit(multop*)): New function. "a & b &
c" has length 5, not 4, even though it is stored as And(a,b,c).
This caused reduc.test to fail on some formulae.
This commit is contained in:
Alexandre Duret-Lutz 2010-01-22 11:00:49 +01:00
parent e733f951be
commit 919fc298ff
2 changed files with 22 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2010-01-22 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix the computation of the length of multops.
* src/ltlvisit/length.cc (visit(multop*)): New function. "a & b &
c" has length 5, not 4, even though it is stored as And(a,b,c).
This caused reduc.test to fail on some formulae.
2010-01-21 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-01-21 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Please the style checks... Please the style checks...

14
src/ltlvisit/length.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2010 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
@ -21,6 +23,7 @@
#include "length.hh" #include "length.hh"
#include "ltlvisit/postfix.hh" #include "ltlvisit/postfix.hh"
#include "ltlast/multop.hh"
namespace spot namespace spot
{ {
@ -42,6 +45,17 @@ namespace spot
return result_; return result_;
} }
virtual void
visit(multop* mo)
{
unsigned s = mo->size();
for (unsigned i = 0; i < s; ++i)
mo->nth(i)->accept(*this);
// "a & b & c" should count for 5, even though it is
// stored as And(a,b,c).
mo += s - 1;
}
virtual void virtual void
doit_default(formula*) doit_default(formula*)
{ {