From 919fc298ff4eca61eb6c975cc954be5d59b690b6 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 22 Jan 2010 11:00:49 +0100
Subject: [PATCH] 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.
---
 ChangeLog              |  8 ++++++++
 src/ltlvisit/length.cc | 14 ++++++++++++++
 2 files changed, 22 insertions(+)

diff --git a/ChangeLog b/ChangeLog
index 9fca66224..86bffe0ed 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -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>
 
 	Please the style checks...
diff --git a/src/ltlvisit/length.cc b/src/ltlvisit/length.cc
index 5adb276a4..ba214b37e 100644
--- a/src/ltlvisit/length.cc
+++ b/src/ltlvisit/length.cc
@@ -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),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -21,6 +23,7 @@
 
 #include "length.hh"
 #include "ltlvisit/postfix.hh"
+#include "ltlast/multop.hh"
 
 namespace spot
 {
@@ -42,6 +45,17 @@ namespace spot
 	  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
 	doit_default(formula*)
 	{