From 97832af321e1081c07a1473e2f0feefece750fbf Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 21 Aug 2024 21:36:54 +0200
Subject: [PATCH] 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                    |  5 ++++-
 spot/tl/randomltl.cc    | 38 +++++++++++++++++++++++++++++++++-----
 spot/tl/randomltl.hh    |  6 ++++++
 tests/core/randpsl.test | 18 ++++++++++++++++++
 4 files changed, 61 insertions(+), 6 deletions(-)

diff --git a/NEWS b/NEWS
index c0ab55c77..47cd487cc 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,9 @@
 New in spot 2.12.0.dev (not yet released)
 
-  Nothing yet.
+  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)
 
diff --git a/spot/tl/randomltl.cc b/spot/tl/randomltl.cc
index 9aa604ee2..e415535b2 100644
--- a/spot/tl/randomltl.cc
+++ b/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});
     }
 
diff --git a/spot/tl/randomltl.hh b/spot/tl/randomltl.hh
index d4c52debf..a7ea3561c 100644
--- a/spot/tl/randomltl.hh
+++ b/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();
 
diff --git a/tests/core/randpsl.test b/tests/core/randpsl.test
index 5e7192894..9d4f825aa 100755
--- a/tests/core/randpsl.test
+++ b/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