From e8527d5ae9639259ef0de89d0816a306b3cccdb5 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 2 Sep 2017 16:35:18 +0200
Subject: [PATCH] Improve simplification of expr[*0..1]

Fixes #108.

* spot/tl/simplify.cc: Implement the reduction.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/reduccmp.test: Test it.
---
 NEWS                     | 4 ++++
 doc/tl/tl.tex            | 5 +++--
 spot/tl/simplify.cc      | 2 ++
 tests/core/reduccmp.test | 1 +
 4 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index ab5cc9a9f..1cc9b294b 100644
--- a/NEWS
+++ b/NEWS
@@ -184,6 +184,10 @@ New in spot 2.3.5.dev (not yet released)
     G(a & XF(b & XFc & Fd) can be simplified to G(a & Fb & Fc & Fd),
     and dually F(a | XG(b | XGc | Gd)) = F(a | Gb | Gc | Gd).
 
+    When working with SERE, the simplification of "expr[*0..1]" was
+    improved.  E.g. {{a[*]|b}[*0..1]} becomes {a[*]|b} instead of
+    {{a[+]|b}[*0..1]}.
+
   - The new function spot::to_weak_alternating() is able to take an
     input automaton with generalized Büchi/co-Büchi acceptance and
     convert it to a weak alternating automaton.
diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 09eea55f8..1831e66ab 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1560,8 +1560,9 @@ presence of \samp{$\AND$} operators, but unfortunately not when the
 
 We extend the above definition to bounded repetitions with:
 \begin{align*}
-  r\STAR{\mvar{i}..\mvar{j}} & \equiv r^\square\STAR{0..\mvar{j}}\quad\text{if}\quad\varepsilon\VDash r\STAR{\mvar{i}..\mvar{j}}\text{~and~}\varepsilon\not\VDash r^\square\\
-  r\STAR{\mvar{i}..\mvar{j}} & \equiv r^\square\STAR{1..\mvar{j}}\quad\text{if}\quad\varepsilon\VDash r\STAR{\mvar{i}..\mvar{j}}\text{~and~}\varepsilon\VDash r^\square
+  r\STAR{\mvar{i}..\mvar{j}} & \equiv r^\square\STAR{0..\mvar{j}}\quad\text{if}\quad\varepsilon\VDash r\STAR{\mvar{i}..\mvar{j}},\,\varepsilon\not\VDash r^\square,\,\text{~and~}j>1\\
+  r\STAR{\mvar{i}..\mvar{j}} & \equiv r^\square\STAR{1..\mvar{j}}\quad\text{if}\quad\varepsilon\VDash r\STAR{\mvar{i}..\mvar{j}},\,\varepsilon\VDash r^\square\,\text{~and~}j>1\\
+  r\STAR{\mvar{i}..\mvar{j}} & \equiv r\phantom{^\square\STAR{1..\mvar{j}}}\quad\text{if}\quad\varepsilon\VDash r\text{~and~}\mvar{j}=1
 \end{align*}
 where $r^\square$ is recursively defined as follows:
 \begin{align*}
diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc
index 4bd4c52a3..783a1a48c 100644
--- a/spot/tl/simplify.cc
+++ b/spot/tl/simplify.cc
@@ -1362,6 +1362,8 @@ namespace spot
               if (!f.accepts_eword())
                 return f;
               formula h = f[0];
+              if (f.max() == 1 && h.accepts_eword())
+                return h;
               auto min = 0;
               if (f.max() == formula::unbounded())
                 {
diff --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test
index 5572fa71e..42e62a3fe 100755
--- a/tests/core/reduccmp.test
+++ b/tests/core/reduccmp.test
@@ -376,6 +376,7 @@ G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf)
 {a:b*:c:d*}[]->e, !a | ((!c | (e W !d)) W !b)
 {a|b*|c|d*}[]->e, (e | !(a | c)) & (e W !b) & (e W !d)
 {{[*0]|a};b;{[*0]|a};c;e[*]}[]->f,{{[*0]|a};b;{[*0]|a}}[]->X((f&X(f W !e))|!c)
+{(a[*]|b)[*0..1];c}, {{b | a[*]};c}
 
 {a&b&c*}<>->!Xb, (a & b & X!b) | (a & b & c & X(c U !b))
 {[*]}<>->b, Fb