tl: fix detection of goto
Fixes #559. * spot/tl/print.cc (strip_star_not): Only match a full star. * tests/core/sugar.test: Add test case.
This commit is contained in:
parent
94ab42612a
commit
db168f97e6
3 changed files with 14 additions and 0 deletions
4
NEWS
4
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
|
fail to color some transiant edges when the "acd" option was
|
||||||
activated.
|
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)
|
New in spot 2.11.6 (2023-08-01)
|
||||||
|
|
||||||
Bug fixes:
|
Bug fixes:
|
||||||
|
|
|
||||||
|
|
@ -348,6 +348,8 @@ namespace spot
|
||||||
static formula
|
static formula
|
||||||
strip_star_not(formula f)
|
strip_star_not(formula f)
|
||||||
{
|
{
|
||||||
|
if (!f.is_Kleene_star())
|
||||||
|
return nullptr;
|
||||||
return f.get_child_of({op::Star, op::Not});
|
return f.get_child_of({op::Star, op::Not});
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -59,6 +59,10 @@ F[]a|G[]b|X[]c
|
||||||
{##[1..2] b*}|->e
|
{##[1..2] b*}|->e
|
||||||
{a ##[+] b}|->e
|
{a ##[+] b}|->e
|
||||||
{##[*] b}|->e
|
{##[*] b}|->e
|
||||||
|
{(!a)[*];a;b}!
|
||||||
|
{(!a)[+];a;b}!
|
||||||
|
{(!a)[*3];a;b}!
|
||||||
|
{((!a)[*];a)[*2..3];b}!
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
ltlfilt -F ok.in > ok.out
|
ltlfilt -F ok.in > ok.out
|
||||||
|
|
@ -99,6 +103,10 @@ FGa | Gb | XGc
|
||||||
{[*1..2];b[*]}[]-> e
|
{[*1..2];b[*]}[]-> e
|
||||||
{a;[*];b}[]-> e
|
{a;[*];b}[]-> e
|
||||||
{[*];b}[]-> e
|
{[*];b}[]-> e
|
||||||
|
{a[->];b}!
|
||||||
|
{{!a}[+];a;b}!
|
||||||
|
{{!a}[*3];a;b}!
|
||||||
|
{a[->2..3];b}!
|
||||||
EOF
|
EOF
|
||||||
diff ok.out expect
|
diff ok.out expect
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue