formula: add a missing trivial rewriting in SERE

We should have [*0]|f ≡ f when f is a SERE that already accept the
empty word.  Fixes issue #454.

* spot/tl/formula.cc: Implement the rewriting.
* tests/core/reduccmp.test: Add a test case.
* doc/tl/tl.tex, NEWS: Document it.

NEWS

@@ -32,6 +32,10 @@ New in spot 2.12.0.dev (not yet released)
      following "Efficient Normalization of Linear Temporal Logic" by
      Esparza et al. (J. ACM, 2024).
 
+   - Trivial rewritings (those performed everytime at construction)
+     were missing the rule "[*0]|f ≡ f" when f already accepts the
+     empty word.  (Issue #545.)
+
 New in spot 2.12  (2024-05-16)
 
   Build:

doc/tl/tl.tex

@@ -839,47 +839,47 @@ The following rules are all valid with the two arguments swapped.
 %\samp{$\FUSION$}.)
 
 \begin{align*}
-  \0\AND f &\equiv \0 &
   \0\ANDALT f   &\equiv \0 &
+  \0\AND f &\equiv \0 &
   \0\OR f &\equiv f &
   \0 \FUSION f &\equiv \0 &
-  \0 \CONCAT f &\equiv \0 \\
+  \mathllap{\0 \CONCAT f}&\equiv \0 \\
+  \1\ANDALT b   &\equiv b &
   \1\AND f&\equiv
   \begin{cases}
     1\mathrlap{\text{~if~} \varepsilon\VDash f} \\
     f\mathrlap{\text{~if~} \varepsilon\nVDash f} \\
   \end{cases} &
-  \1\ANDALT b   &\equiv b &
   \1\OR b &\equiv \1 &
-  \1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\
+  \1 \FUSION f & \equiv \mathrlap{f\text{~if~}\varepsilon\nVDash f}\\
-  &&
   \STAR{} \ANDALT f &\equiv f &
+  &&
   \STAR{} \OR f &\equiv \mathrlap{\STAR{}} &
   &&
-  \STAR{} \CONCAT f &\equiv \STAR{}\text{~if~}\varepsilon\VDash f& \\
+  \mathllap{\STAR{} \CONCAT f }&\equiv \STAR{}\text{~if~}\varepsilon\VDash f& \\
-  &&
   \PLUS{} \ANDALT f &\equiv f \text{~if~}\varepsilon\nVDash f&
+  &&
   \PLUS{} \OR f &\equiv \begin{cases}
     \mathrlap{\STAR{}\text{~if~} \varepsilon\VDash f} \\
     \mathrlap{\PLUS{}\text{~if~} \varepsilon\nVDash f} \\
   \end{cases} &
   &&
   && \\
-  \eword\AND f &\equiv f &
   \eword\ANDALT f &\equiv
   \begin{cases}
-    \mathrlap{\eword\text{~if~} \varepsilon\VDash f} \\
+    \!\eword\text{~if~}\varepsilon\VDash{f} \\
-    \0\mathrlap{\phantom{\STAR{}}\text{~if~} \varepsilon\nVDash f} \\
+    \0\!\phantom{\STAR{}}\text{~if~}\varepsilon\nVDash{f} \\
   \end{cases} &
-  &&
+  \mathllap{\eword}\AND f &\equiv f &
+  \eword\OR f &\equiv f \text{~if~} \varepsilon\VDash f&
   \eword \FUSION f &\equiv \0 &
-  \eword \CONCAT f &\equiv f\\
+  \mathllap{\eword \CONCAT f}&\equiv f\\
-  f\AND f &\equiv f&
   f\ANDALT f &\equiv f &
+  f\AND f &\equiv f&
   f\OR f &\equiv f&
   f\FUSION f&\equiv f\FSTAR{2}&
   f\CONCAT f&\equiv f\STAR{2}\\
-  b_1 \AND b_2 &\equiv b_1\ANDALT b_2 &
+  b_1 \AND b_2 &\equiv \mathrlap{b_1\ANDALT b_2}&
   &&
   &&
   b_1:b_2 &\equiv b_1\ANDALT b_2
@@ -890,7 +890,7 @@ f\STAR{\mvar{i}..\mvar{j}}\CONCAT f\STAR{\mvar{k}..\mvar{l}}&\equiv f\STAR{\mvar
 f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f&\equiv f\FSTAR{\mvar{i+1}..\mvar{j+1}} &
 f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f\FSTAR{\mvar{k}..\mvar{l}}&\equiv f\FSTAR{\mvar{i+k}..\mvar{j+l}}\\
 b\STAR{\mvar{i}..\mvar{j}}\FUSION b &\equiv b\STAR{\mvar{\max(i,1)}..\mvar{j}} &
-b\STAR{\mvar{i}..\mvar{j}}\FUSION b\STAR{\mvar{k}..\mvar{l}} &\equiv b\mathrlap{\STAR{\mvar{\max(i,1)+\max(k,1)-1}..\mvar{j+l-1}}}
+b\STAR{\mvar{i}..\mvar{j}}\FUSION b\STAR{\mvar{k}..\mvar{l}} &\equiv b\STAR{\mvar{\max(i,1)+\max(k,1)-1}..\mvar{j+l-1}}
 \end{align*}
 \section{SERE-LTL Binding Operators}
 

spot/tl/formula.cc

@@ -357,7 +357,16 @@ namespace spot
         break;
       case op::OrRat:
         neutral = ff();
-        neutral2 = nullptr;
+        {
+          // If this OrRat contains an operand that accept [*0] but
+          // isn't [*0], then any [+0] can be removed.
+          bool eword_accepted =
+            std::find_if(v.begin(), v.end(),
+                         [](const fnode* f) {
+                           return f->accepts_eword() && !f->is_eword();
+                         }) != v.end();
+          neutral2 = eword_accepted ? eword() : nullptr;
+        }
         abs = one_star();
         abs2 = nullptr;
         weak_abs = one_plus();

tests/core/reduccmp.test

@@ -487,7 +487,8 @@ GF(a && GF(b) && c), G(F(a & c) & Fb)
 {first_match(1:e[*0..3])[*]}[]-> c, c W !e
 {first_match(first_match(a*;e);b)}[]->a, {first_match(a[*];e)}[]-> X(a | !b)
 {first_match(first_match(a*;e):b*)}[]->a, {first_match(a[*];e)}[]-> (a | !b)
-
+# issue 545
+{([*0]|a[*]|b);c}<>->d, {(a[*]|b);c}<>->d
 # issue 558 (was a false alarm, but still good to test)
 {(!b)[*3];b}!, !b & X(!b & X(!b & Xb))
 {(!b)[+];b}!, !b & XFb