* src/ltlvisit/formlength.cc: Rename as ...

* src/ltlvisit/length.cc: ... this.
* src/ltlvisit/length.hh: New file, extracted from ...
* src/ltlvisit/reducform.hh: ... here.
* src/ltlvisit/Makefile.am (ltlvisit_HEADERS): Add length.hh.
(libltlvisit_la_SOURCES): Rename formlength.cc as length.cc.
* src/ltltest/reduc.cc: Include length.hh.

ChangeLog

@@ -1,5 +1,13 @@
 2004-05-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/ltlvisit/formlength.cc: Rename as ...
+	* src/ltlvisit/length.cc: ... this.
+	* src/ltlvisit/length.hh: New file, extracted from ...
+	* src/ltlvisit/reducform.hh: ... here.
+	* src/ltlvisit/Makefile.am (ltlvisit_HEADERS): Add length.hh.
+	(libltlvisit_la_SOURCES): Rename formlength.cc as length.cc.
+	* src/ltltest/reduc.cc: Include length.hh.
+
 	* src/ltlvisit/formlength.cc (length_form_vistor): Rename as ..
 	(length_visitor): ... this.
 	(form_length): Rename as ...

src/ltltest/reduc.cc

@@ -29,6 +29,7 @@
 #include "ltlvisit/destroy.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/reducform.hh"
+#include "ltlvisit/length.hh"
 #include "ltlast/allnodes.hh"
 
 void

src/ltlvisit/Makefile.am

@@ -29,25 +29,26 @@ ltlvisit_HEADERS = \
   destroy.hh \
   dotty.hh \
   dump.hh \
-  tostring.hh \
+  length.hh \
   lunabbrev.hh \
   nenoform.hh \
   postfix.hh \
-  tunabbrev.hh \
+  reducform.hh \
-  reducform.hh
+  tostring.hh \
+  tunabbrev.hh
 
 noinst_LTLIBRARIES = libltlvisit.la
 libltlvisit_la_SOURCES = \
+  basereduc.cc \
   clone.cc \
   destroy.cc \
   dotty.cc \
   dump.cc \
-  tostring.cc \
+  forminf.cc \
+  length.cc \
   lunabbrev.cc \
   nenoform.cc \
   postfix.cc \
-  tunabbrev.cc \
   reducform.cc \
-  basereduc.cc \
+  tostring.cc \
-  forminf.cc \
+  tunabbrev.cc
-  formlength.cc

src/ltlvisit/formlength.cc

@@ -1,95 +0,0 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
-// et Marie Curie.
-//
-// This file is part of Spot, a model checking library.
-//
-// Spot is free software; you can redistribute it and/or modify it
-// under the terms of the GNU General Public License as published by
-// the Free Software Foundation; either version 2 of the License, or
-// (at your option) any later version.
-//
-// Spot is distributed in the hope that it will be useful, but WITHOUT
-// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
-// License for more details.
-//
-// You should have received a copy of the GNU General Public License
-// along with Spot; see the file COPYING.  If not, write to the Free
-// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
-// 02111-1307, USA.
-
-#include "reducform.hh"
-#include "ltlast/allnodes.hh"
-
-namespace spot
-{
-  namespace ltl
-  {
-
-   class length_visitor : public const_visitor
-    {
-    public:
-
-      length_visitor()
-      {
-	result_ = 0;
-      }
-
-      virtual
-      ~length_visitor()
-      {
-      }
-
-      int
-      result() const
-      {
-	return result_;
-      }
-
-      void
-      visit(const atomic_prop*)
-      {
-	result_ = 1;
-      }
-
-      void
-      visit(const constant*)
-      {
-	result_ = 1;
-      }
-
-      void
-      visit(const unop* uo)
-      {
-	result_ = 1 + length(uo->child());
-      }
-
-      void
-      visit(const binop* bo)
-      {
-	result_ = 1 + length(bo->first()) + length(bo->second());
-      }
-
-      void
-      visit(const multop* mo)
-      {
-	unsigned mos = mo->size();
-	for (unsigned i = 0; i < mos; ++i)
-	  result_ += length(mo->nth(i));
-      }
-
-    protected:
-      int result_; // size of the formula
-    };
-
-    int
-    length(const formula* f)
-    {
-      length_visitor v;
-      const_cast<formula*>(f)->accept(v);
-      return v.result();
-    }
-
-  }
-}

src/ltlvisit/length.hh

@@ -0,0 +1,40 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_LTLVISIT_LENGTH_HH
+# define SPOT_LTLVISIT_LENGTH_HH
+
+#include "ltlast/formula.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    /// \brief Compute the length of a formula.
+    ///
+    /// The length of a formula is the number of atomic properties,
+    /// constants, and operators (logical and temporal) occurring in
+    /// the formula.
+    int length(const formula* f);
+  }
+}
+
+#endif // SPOT_LTLVISIT_LENGTH_HH

src/ltlvisit/reducform.hh

@@ -74,9 +74,6 @@ namespace spot
     /// FIXME: Describe what universal formulae are.  Cite paper.
     bool is_universal(const formula* f);
 
-    /// Length of a formula.
-    int length(const formula* f);
-
     /// Type the first node of a formula.
     class node_type_form_visitor : public const_visitor
     {