alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

autfilt: allow --highlight-word to work on Fin acceptance

Browse source 
Fixes #523.

* bin/autfilt.cc: Remove the restriction.
* tests/core/acc_word.test: Add test case.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2023-01-24 11:35:14 +01:00
parent 5b0143eba6
commit e5150d0314
3 changed files with 19 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -24,6 +24,10 @@ New in spot 2.11.3.dev (not yet released)
multiple initial states (because Spot supports only one), the HOA multiple initial states (because Spot supports only one), the HOA
parser could break state-based acceptance. (Issue #522.) parser could break state-based acceptance. (Issue #522.)
- autfilt --highlight-word refused to work on automata with Fin
acceptance for historical reason, but the cose is perfectly able
to handle this now. (Issue #523.)
- delay_branching_here(), a new optimization of Spot 2.11 had an - delay_branching_here(), a new optimization of Spot 2.11 had an
incorrectly handling of states without successors, causing some incorrectly handling of states without successors, causing some
segfaults. (Issue #524.) segfaults. (Issue #524.)

9
bin/autfilt.cc
View file

@ -1667,13 +1667,8 @@ namespace
if (!opt->hl_words.empty()) if (!opt->hl_words.empty())
for (auto& [word_aut, color]: opt->hl_words) for (auto& [word_aut, color]: opt->hl_words)
{ if (auto run = spot::product(aut, word_aut)->accepting_run())
if (aut->acc().uses_fin_acceptance()) run->project(aut)->highlight(color);
error(2, 0,
"--highlight-word does not yet work with Fin acceptance");
if (auto run = spot::product(aut, word_aut)->accepting_run())
run->project(aut)->highlight(color);
}
timer.stop(); timer.stop();
if (opt->uniq) if (opt->uniq)

20
tests/core/acc_word.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2016, 2017, 2018, 2019 Laboratoire de Recherche et Développement # Copyright (C) 2016-2019, 2023 Laboratoire de Recherche
# de l'Epita (LRDE). # et Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -91,6 +91,15 @@ State: 1
EOF EOF
diff expected out diff expected out
ltl2tgba -G '(GF(a & X!a) -> GF(b & XXb)) & GFc' > aut.hoa
word='!a&!c;cycle{!a&b&!c;!a&c;!a&b&c}'
autfilt -H1.1 aut.hoa --highlight-word="$word" > out.hoa
grep spot.highlight.edges out.hoa >out.edges
cat >expected <<EOF
spot.highlight.edges: 3 1 11 1 12 1
EOF
diff out.edges expected
ltl2tgba 'Fa & Fb' | ltl2tgba 'Fa & Fb' |
autfilt -H1.1 \ autfilt -H1.1 \
--highlight-word='2,!a&!b;cycle{!a&b;a&b}' \ --highlight-word='2,!a&!b;cycle{!a&b;a&b}' \
@ -133,11 +142,8 @@ for w in ',!a&!b;cycle{!a&b;a&b}' '-1,cycle{a}' '1 cycle{a}'; do
done done
# highlight-word does not yet work with Fin acceptance # highlight-word used not to work with Fin acceptance, but it's ok now
ltl2tgba -G -D 'FGa' | autfilt --highlight-word='cycle{a}' 2>stderr && exit 1 ltl2tgba -G -D 'FGa' | autfilt --highlight-word='cycle{a}'
test $? -eq 2
grep 'highlight-word.*Fin' stderr
ltlfilt -f 'GFa' --accept-word 'cycle{!a}' && exit 1 ltlfilt -f 'GFa' --accept-word 'cycle{!a}' && exit 1
ltlfilt -f 'GF!a' --accept-word 'cycle{!a}' ltlfilt -f 'GF!a' --accept-word 'cycle{!a}'