ltlsynt: fix usage for --dot's argument

* bin/ltlsynt.cc (dispatch_print_hoa): Pass the right argument to
print_dot.
* tests/core/ltlsynt.test: Test it.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2024-09-02 17:26:42 +02:00
parent 514209e80f
commit 1a36ea6ce4
3 changed files with 8 additions and 2 deletions

2
NEWS
View file

@ -10,6 +10,8 @@ New in spot 2.12.0.dev (not yet released)
confused by games with "parity min" acceptance using transition
with several colors (a rather uncommon situation).
- "ltlsynt ... --print-game --dot=ARGS" was ignoring ARGS.
New in spot 2.12 (2024-05-16)
Build:

View file

@ -322,7 +322,7 @@ namespace
rs->patch_game(game);
if (opt_dot)
spot::print_dot(std::cout, game, opt_print_hoa_args);
spot::print_dot(std::cout, game, opt_dot_arg);
else if (opt_print_pg)
spot::print_pg(std::cout, game);
else

View file

@ -1085,7 +1085,11 @@ diff outx exp
# Test --dot and --hide-status
ltlsynt -f 'i <-> Fo' --ins=i --aiger --dot | grep arrowhead=dot
ltlsynt -f 'i <-> Fo' --ins=i --print-game-hoa --dot | grep 'shape="diamond"'
ltlsynt -f 'i <-> Fo' --ins=i --print-game-hoa --dot > out
grep 'shape="diamond"' out
grep 'Inf(0)' out
ltlsynt -f 'i <-> Fo' --ins=i --print-game-hoa --dot=bar > out
grep 'label=<Inf(<font' out
ltlsynt -f 'i <-> Fo' --ins=i --dot --hide-status > res
cat >exp <<EOF
digraph "" {