randltl: fix generation without unary operators

* spot/tl/randomltl.hh (has_unary_ops): New method.
* spot/tl/randomltl.cc: Avoid creating subformulas of even size
when we do not have unary operators.
* tests/core/randpsl.test: Test it.
* NEWS: Mention it.

NEWS

@@ -36,6 +36,11 @@ New in spot 2.12.0.dev (not yet released)
      were missing the rule "[*0]|f ≡ f" when f already accepts the
      empty word.  (Issue #545.)
 
+  Bug fixes:
+
+  - Generating random formula without any unary opertors would very
+    often create formulas much smaller than asked.
+
 New in spot 2.12  (2024-05-16)
 
   Build:

spot/tl/randomltl.cc

@@ -92,14 +92,20 @@ namespace spot
     {
       assert(n >= 3);
       --n;
-      int l = rrand(1, n - 1);
+      int l;  // size of left
+      if ((n & 1) | rl->has_unary_ops())
+        l = rrand(1, n - 1);
+      else
+        // if we do not have unary ops, we must split n in two odd sizes
+        l = rrand(0, n/2 - 1)*2 + 1;
+
       // Force the order of generation of operands to be right, then
       // left.  This is historical, because gcc evaluates argument
       // from right to left and we used to make the two calls to
       // generate() inside of the call to instance() before
       // discovering that clang would perform the nested calls from
       // left to right.
-      auto right = rl->generate(n - l);
+      formula right = rl->generate(n - l);
       return formula::binop(Op, rl->generate(l), right);
     }
 
@@ -110,7 +116,25 @@ namespace spot
       assert(n >= 3);
       --n;
       const random_psl* rp = static_cast<const random_psl*>(rl);
-      int l = rrand(1, n - 1);
+      int l;  // size of left
+      bool left_must_be_odd = !rp->rs.has_unary_ops();
+      bool right_must_be_odd = !rl->has_unary_ops();
+      if (n & 1)
+        {
+          if (left_must_be_odd && !right_must_be_odd)
+            l = rrand(0, n/2 - 1) * 2 + 1;
+          else if (!left_must_be_odd && right_must_be_odd)
+            l = rrand(1, n/2) * 2;
+          else
+            l = rrand(1, n - 1);
+        }
+      else
+        {
+          if (left_must_be_odd || right_must_be_odd)
+            l = rrand(0, n/2 - 1) * 2 + 1;
+          else
+            l = rrand(1, n - 1);
+        }
       // See comment in binop_builder.
       auto right = rl->generate(n - l);
       return formula::binop(Op, rp->rs.generate(l), right);
@@ -152,9 +176,13 @@ namespace spot
     {
       assert(n >= 3);
       --n;
-      int l = rrand(1, n - 1);
       // See comment in binop_builder.
-      auto right = rl->generate(n - l);
+      int l;  // size of left
+      if ((n & 1) | rl->has_unary_ops())
+        l = rrand(1, n - 1);
+      else
+        l = rrand(0, n/2 - 1)*2 + 1;
+      formula right = rl->generate(n - l);
       return formula::multop(Op, {rl->generate(l), right});
     }
 

spot/tl/randomltl.hh

@@ -72,6 +72,12 @@ namespace spot
     /// occurrences of the \c F operator.
     const char* parse_options(char* options);
 
+    /// \brief whether we can use unary operators
+    bool has_unary_ops() const
+    {
+      return total_2_ > 0.0;
+    }
+
   protected:
     void update_sums();
 

tests/core/randpsl.test

@@ -36,3 +36,21 @@ test `wc -l < formulas` = 50
 
 
 randltl --psl --sere-priorities=first_match=10 -n 100 2 | grep first_match
+
+# the random generator had trouble generating formulas of the proper size when
+# unary operators were disabled
+P=true=0,false=0,not=0
+randltl --tree-size=19 -B --boolean-prio=$P 1000 -n10 --stats=%a >out
+cat >expected <<EOF
+10
+10
+10
+10
+10
+10
+10
+10
+10
+10
+EOF
+diff expected out