Commit 4d16c076 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 38f0cfd4
Pipeline #8652 passed with stage
in 147 minutes and 57 seconds
...@@ -1549,7 +1549,8 @@ namespace spot ...@@ -1549,7 +1549,8 @@ namespace spot
// concatenation, it means all arguments should be of the // concatenation, it means all arguments should be of the
// form b*, except one that is siSERE (i.e., a sub-formula // form b*, except one that is siSERE (i.e., a sub-formula
// that verify is_syntactic_stutter_invariant() and // 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) if (op_ == op::Concat)
{ {
unsigned sb = 0; // stared Boolean formulas seen unsigned sb = 0; // stared Boolean formulas seen
...@@ -1567,7 +1568,7 @@ namespace spot ...@@ -1567,7 +1568,7 @@ namespace spot
break; break;
} }
} }
is_.syntactic_si = sb == s - 1; is_.syntactic_si = sb >= s - 1;
} }
break; break;
} }
...@@ -1594,7 +1595,7 @@ namespace spot ...@@ -1594,7 +1595,7 @@ namespace spot
if (max_ == unbounded()) if (max_ == unbounded())
{ {
is_.finite = false; is_.finite = false;
is_.syntactic_si = min_ == 1 && children[0]->is_boolean(); is_.syntactic_si = min_ <= 1 && children[0]->is_boolean();
} }
else else
{ {
......
...@@ -135,7 +135,7 @@ Fa M b,&!xLPgopra ...@@ -135,7 +135,7 @@ Fa M b,&!xLPgopra
{p[+]:p[+]},&!xfPsoprla {p[+]:p[+]},&!xfPsoprla
(!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla (!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla
{b[+][:*0..3]},&!fPsopra {b[+][:*0..3]},&!fPsopra
{a->c[*]},fPsopra {a->c[*]},xfPsopra
EOF EOF
run 0 ../kind input run 0 ../kind input
...@@ -130,6 +130,7 @@ b W GFa ...@@ -130,6 +130,7 @@ b W GFa
a U Fb a U Fb
a & (b | c) a & (b | c)
{{!a}[*];a[+]}[]-> b {{!a}[*];a[+]}[]-> b
{a[*];{!a}[*];a[*]}[]-> b
{a[*];{!a}[+];a[*]}[]-> b {a[*];{!a}[+];a[*]}[]-> b
{a[+];{!a}[*];a[*]}[]-> b {a[+];{!a}[*];a[*]}[]-> b
{a[*];{!a}[*];a[+]}[]-> b {a[*];{!a}[*];a[+]}[]-> b
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment