diff --git a/NEWS b/NEWS index 7213ce507..444f15a15 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,7 @@ New in spot 1.99.1a (not yet released) - Nothing yet. + * Bugs fixed: + - p[+][:*2] was not detected as belonging to siPSL New in spot 1.99.1 (2015-06-23) diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index 2801dddbb..1026e22f2 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -69,15 +69,11 @@ namespace spot break; case FStar: is.accepting_eword = false; + is.syntactic_si &= !child->is_boolean(); if (max_ == unbounded) - { - is.finite = false; - is.syntactic_si &= !child->is_boolean(); - } - else - { - is.syntactic_si = false; - } + is.finite = false; + if (min_ == 0) + is.syntactic_si = false; break; } } diff --git a/src/tests/kind.test b/src/tests/kind.test index 09a4824cf..b0733bc2d 100755 --- a/src/tests/kind.test +++ b/src/tests/kind.test @@ -130,6 +130,9 @@ Fa M b,&!xLPgopra {a[+];b*;c[+]},&!xfPsopra {a[+] && b || c[+]},&!fPsopra {a[+] && b[+] || c[+]},&!xfPsopra +{p[+]:p[+]},&!xfPsoprla +(!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla +{b[+][:*0..3]},&!fPsopra EOF run 0 ../kind input