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 315872a54b
commit a1c02856ac
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

@ -10,6 +10,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 reasons, however the code has been
perfectly able to handle this for a while. (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
incorrect handling of states without successors, causing some incorrect 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}'