From 5d9e7d1f93057f101c15ff1c92069e56c62d0b54 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 23 Jun 2015 19:27:30 +0200 Subject: [PATCH] ltl: fix detection of some siPSL formulas * src/ltlast/bunop.cc: Fix detection of f[:*2] as siPSL if f is siPSL * src/tests/kind.test: Test it. * NEWS: Mention it. --- NEWS | 3 ++- src/ltlast/bunop.cc | 12 ++++-------- src/tests/kind.test | 3 +++ 3 files changed, 9 insertions(+), 9 deletions(-) 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