From 9e7e6d50fbbc28a4e710e33fc3f851b251200a8a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 26 Apr 2019 22:14:19 +0200
Subject: [PATCH] formula: b* is siSERE

Since b[+] and [*0] are siSERE, b* is siSERE as well.
Suggested by Victor Khomenko.

* spot/tl/formula.cc: Implement that for Star and also
in the concatenation rule.
* tests/core/kind.test, tests/core/ltlfilt.test: Adjust.
---
 spot/tl/formula.cc      | 7 ++++---
 tests/core/kind.test    | 2 +-
 tests/core/ltlfilt.test | 1 +
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc
index 36397d2d4..707c62d0f 100644
--- a/spot/tl/formula.cc
+++ b/spot/tl/formula.cc
@@ -1549,7 +1549,8 @@ namespace spot
           // concatenation, it means all arguments should be of the
           // form b*, except one that is siSERE (i.e., a sub-formula
           // that verify is_syntactic_stutter_invariant() and
-          // !is_boolean());
+          // !is_boolean()).   Since b* is siSERE, that means we
+          // want at least s-1 operands of the form b*.
           if (op_ == op::Concat)
             {
               unsigned sb = 0; // stared Boolean formulas seen
@@ -1567,7 +1568,7 @@ namespace spot
                       break;
                     }
                 }
-              is_.syntactic_si = sb == s - 1;
+              is_.syntactic_si = sb >= s - 1;
             }
           break;
         }
@@ -1594,7 +1595,7 @@ namespace spot
               if (max_ == unbounded())
                 {
                   is_.finite = false;
-                  is_.syntactic_si = min_ == 1 && children[0]->is_boolean();
+                  is_.syntactic_si = min_ <= 1 && children[0]->is_boolean();
                 }
               else
                 {
diff --git a/tests/core/kind.test b/tests/core/kind.test
index a7b859d97..e07fd02b9 100755
--- a/tests/core/kind.test
+++ b/tests/core/kind.test
@@ -135,7 +135,7 @@ Fa  M b,&!xLPgopra
 {p[+]:p[+]},&!xfPsoprla
 (!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla
 {b[+][:*0..3]},&!fPsopra
-{a->c[*]},fPsopra
+{a->c[*]},xfPsopra
 EOF
 
 run 0 ../kind input
diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test
index 998b5ab1a..5c10a1b0e 100755
--- a/tests/core/ltlfilt.test
+++ b/tests/core/ltlfilt.test
@@ -130,6 +130,7 @@ b W GFa
 a U Fb
 a & (b | c)
 {{!a}[*];a[+]}[]-> b
+{a[*];{!a}[*];a[*]}[]-> b
 {a[*];{!a}[+];a[*]}[]-> b
 {a[+];{!a}[*];a[*]}[]-> b
 {a[*];{!a}[*];a[+]}[]-> b
-- 
GitLab