From 4d16c0760fe609361cd8bf0b8fb0f295a7a9f1d8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz 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