From 974a4238f63c3554a9f3dc97b3c6d2e46ec6b623 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 23 Nov 2017 11:29:52 +0100
Subject: [PATCH] introduce formula::is_leaf()

Fixes #307.

* spot/tl/formula.hh: Here.
* tests/python/ltlparse.py: Test it.
* NEWS: Mention it.
---
 NEWS                     |  3 +++
 spot/tl/formula.hh       | 15 +++++++++++++++
 tests/python/ltlparse.py | 12 ++++++++++--
 3 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index fc4fd6f40..f89546641 100644
--- a/NEWS
+++ b/NEWS
@@ -187,6 +187,9 @@ New in spot 2.4.2.dev (not yet released)
       Fin(i) & Fin(j) = f          Inf(i) | Inf(j) = t
       Fin(i) & Inf(i) = f          Fin(i) | Inf(i) = t
 
+  - The new spot::formula::is_leaf() method can be used to detect
+    formulas without children (atomic propositions, or constants).
+
   Deprecation notices:
 
   (These functions still work but compilers emit warnings.)
diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh
index ac6368255..e596dec96 100644
--- a/spot/tl/formula.hh
+++ b/spot/tl/formula.hh
@@ -231,6 +231,12 @@ namespace spot
         return size_;
       }
 
+      /// \see formula::is_leaf
+      bool is_leaf() const
+      {
+        return size_ == 0;
+      }
+
       /// \see formula::id
       size_t id() const
       {
@@ -1277,6 +1283,15 @@ namespace spot
       return ptr_->size();
     }
 
+    /// \brief Whether the formula is a leaf.
+    ///
+    /// Leaves are formulas without children.  They are either
+    /// constants (true, false, empty word) or atomic propositions.
+    bool is_leaf() const
+    {
+      return ptr_->is_leaf();
+    }
+
     /// \brief Return the id of a formula.
     ///
     /// Can be used as a hash number.
diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py
index 50fc095c4..a4585134a 100755
--- a/tests/python/ltlparse.py
+++ b/tests/python/ltlparse.py
@@ -25,9 +25,13 @@ import spot
 
 e = spot.default_environment.instance()
 
-l = ['GFa', 'a U (((b)) xor c)', '!(FFx <=> Fx)', 'a \\/ a \\/ b \\/ a \\/ a']
+l = [('GFa', False),
+     ('a U (((b)) xor c)', False),
+     ('!(FFx <=> Fx)', True),
+     ('a \\/ a \\/ b \\/ a \\/ a', False)]
 
-for str1 in l:
+
+for str1, isl in l:
     pf = spot.parse_infix_psl(str1, e, False)
     if pf.format_errors(spot.get_cout()):
         sys.exit(1)
@@ -37,8 +41,12 @@ for str1 in l:
     pf = spot.parse_infix_psl(str2, e)
     if pf.format_errors(spot.get_cout()):
         sys.exit(1)
+    assert isl == pf.f.is_leaf()
     del pf
 
+assert spot.formula('a').is_leaf();
+assert spot.formula('0').is_leaf();
+
 for str1 in ['a * b', 'a xor b', 'a <-> b']:
     pf = spot.parse_infix_boolean(str1, e, False)
     if pf.format_errors(spot.get_cout()):