Add a new length_boolone() function to fix an assert in randpsl.

* src/ltlvisit/length.hh (length_boolone): New function.
* src/ltlvisit/length.cc (length_boolone): Implement it using...
(length_boolone_visitor): ... this new visitor.
* src/ltltest/randltl.cc: Use length_boolone() to check the result
of the random generator, and ignore any formula larger (in
length()) than opt_f.  This fix a bug where the random formula
generator would sometime produce formula larger than requested,
because of the trivial rewriting of {f}[]->e as e|!f.
* src/ltltest/length.cc: Add option -b to call length_boolone().
* src/ltltest/length.test: Test length_boolone().

src/ltltest/length.cc

@@ -21,6 +21,7 @@
 #include <iostream>
 #include <cassert>
 #include <cstdlib>
+#include <cstring>
 #include "ltlparse/public.hh"
 #include "ltlvisit/length.hh"
 #include "ltlast/allnodes.hh"
@@ -35,15 +36,25 @@ syntax(char *prog)
 int
 main(int argc, char **argv)
 {
-  if (argc != 2)
+  if (argc < 2 || argc > 3)
     syntax(argv[0]);
 
+  bool boolone = false;
+  if (!strcmp(argv[1], "-b"))
+    {
+      boolone = true;
+      ++argv;
+    }
+
   spot::ltl::parse_error_list p1;
   spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
 
   if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
     return 2;
 
+  if (boolone)
+    std::cout << spot::ltl::length_boolone(f1) << std::endl;
+  else
     std::cout << spot::ltl::length(f1) << std::endl;
 
   f1->destroy();

src/ltltest/length.test

@@ -24,6 +24,15 @@
 
 set -e
 
-test `run 0 ../length 'a U Xc'` = 4
-test `run 0 ../length 'a&b&c'` = 5
-test `run 0 ../length 'a|b|c'` = 5
+len()
+{
+  test `run 0 ../length "$1"` = $2
+  test `run 0 ../length -b "$1"` = $3
+}
+
+len 'a U Xc'      4 4
+len 'a&b&c'       5 1
+len 'a|b|c'       5 1
+len '!a|b|!c'     7 1
+len '!(!a|b|!c)'  8 1
+len '!X(!a|b|!c)' 9 3

src/ltltest/randltl.cc

@@ -321,7 +321,16 @@ main(int argc, char** argv)
 		    }
 		  else
 		    {
-		      assert(spot::ltl::length(f) <= opt_f);
+		      assert(spot::ltl::length_boolone(f) <= opt_f);
+
+		      // We might have a formula bigger than opt_f
+		      // because {e}[]->f of length 3 gets trivially reduced
+		      // to f|!e of length 4.
+		      if (spot::ltl::length(f) > opt_f)
+			{
+			  f->destroy();
+			  continue;
+			}
 		    }
 		  break;
 		}

src/ltlvisit/length.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2010 Laboratoire de Recherche et Développement de
+// Copyright (C) 2010, 2012 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
@@ -24,6 +24,7 @@
 #include "length.hh"
 #include "ltlvisit/postfix.hh"
 #include "ltlast/multop.hh"
+#include "ltlast/unop.hh"
 
 namespace spot
 {
@@ -65,6 +66,38 @@ namespace spot
       protected:
 	int result_; // size of the formula
       };
+
+      class length_boolone_visitor: public length_visitor
+      {
+
+	virtual void
+	visit(unop* uo)
+	{
+	  ++result_;
+	  // Boolean formula have length one.
+	  if (!uo->is_boolean())
+	    uo->child()->accept(*this);
+	}
+
+	virtual void
+	visit(multop* mo)
+	{
+	  // Boolean formula have length one.
+	  if (mo->is_boolean())
+	    {
+	      ++result_;
+	      return;
+	    }
+
+	  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).
+	  result_ += s - 1;
+	}
+
+      };
     }
 
     int
@@ -75,5 +108,13 @@ namespace spot
       return v.result();
     }
 
+    int
+    length_boolone(const formula* f)
+    {
+      length_boolone_visitor v;
+      const_cast<formula*>(f)->accept(v);
+      return v.result();
+    }
+
   }
 }

src/ltlvisit/length.hh

@@ -33,13 +33,23 @@ namespace spot
     /// \brief Compute the length of a formula.
     /// \ingroup ltl_misc
     ///
-    /// The length of a formula is the number of atomic properties,
+    /// The length of a formula is the number of atomic propositions,
     /// constants, and operators (logical and temporal) occurring in
     /// the formula.  spot::ltl::multop instances with n arguments
-    /// count only n-1; for instance <code>a | b | c</code>
-    /// has length 5, even if there is only as single <code>|</code> node
+    /// count for n-1; for instance <code>a | b | c</code> has length
+    /// 5, even if there is only as single <code>|</code> node
     /// internally.
+    ///
+    /// If squash_boolean is set, all Boolean formulae are assumed
+    /// to have length one.
     int length(const formula* f);
+
+    /// \brief Compute the length of a formula, squashing Boolean formulae
+    /// \ingroup ltl_misc
+    ///
+    /// This is similar to spot::ltl::length(), except all Boolean
+    /// formulae are assumed to have length one.
+    int length_boolone(const formula* f);
   }
 }