diff --git a/NEWS b/NEWS index 5246909ea..d27c76f98 100644 --- a/NEWS +++ b/NEWS @@ -219,6 +219,10 @@ New in spot 2.11.6.dev (not yet released) fail to color some transiant edges when the "acd" option was activated. + - The formula printer incorrectly replaced a SERE like "(!a)[*3];a" + by "a[->]". The latter should only replace "(!a)[*];a". + (Issue #559.) + New in spot 2.11.6 (2023-08-01) Bug fixes: diff --git a/spot/tl/print.cc b/spot/tl/print.cc index 044f83d94..ef998ba86 100644 --- a/spot/tl/print.cc +++ b/spot/tl/print.cc @@ -348,6 +348,8 @@ namespace spot static formula strip_star_not(formula f) { + if (!f.is_Kleene_star()) + return nullptr; return f.get_child_of({op::Star, op::Not}); } diff --git a/tests/core/sugar.test b/tests/core/sugar.test index 386793595..344a403df 100755 --- a/tests/core/sugar.test +++ b/tests/core/sugar.test @@ -59,6 +59,10 @@ F[]a|G[]b|X[]c {##[1..2] b*}|->e {a ##[+] b}|->e {##[*] b}|->e +{(!a)[*];a;b}! +{(!a)[+];a;b}! +{(!a)[*3];a;b}! +{((!a)[*];a)[*2..3];b}! EOF ltlfilt -F ok.in > ok.out @@ -99,6 +103,10 @@ FGa | Gb | XGc {[*1..2];b[*]}[]-> e {a;[*];b}[]-> e {[*];b}[]-> e +{a[->];b}! +{{!a}[+];a;b}! +{{!a}[*3];a;b}! +{a[->2..3];b}! EOF diff ok.out expect