From 7e228e86ee0b7b6e41d9c738e7bfcc1a571ac795 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Mar 2024 14:41:42 +0100 Subject: [PATCH] hoa: add option 'b' to build an alias-based basis for all labels Related to issue #563. * spot/twaalgos/hoa.hh (create_alias_basis): New function. * spot/twaalgos/hoa.cc (create_alias_basis): New function. (print_hoa): Add support for option 'b' and create_alias_basis in this case. * bin/common_aoutput.cc, NEWS: Document -Hb. * tests/core/readsave.test, tests/python/aliases.py: Add test cases. --- NEWS | 7 ++++++ bin/common_aoutput.cc | 1 + spot/twaalgos/hoa.cc | 46 ++++++++++++++++++++++++++++++++++++++-- spot/twaalgos/hoa.hh | 20 +++++++++++++++-- tests/core/readsave.test | 22 ++++++++++++------- tests/python/aliases.py | 45 +++++++++++++++++++++++++++++++++++++++ 6 files changed, 129 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index 111c3acb1..1af53cda2 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,13 @@ New in spot 2.11.6.dev (not yet released) autfilt input.hoa -o output-%l.hoa + - For tools that produce automata, using -Hb or --hoa=b will produce + an HOA file in which aliases are used to form a basis for the + whole set of labels. Those aliases are only used when more than + one atomic proposition is used (otherwise, the atomic proposition + and its negation is already a basis). This can help reducing the + size of large HOA files. + - ltlfilt has a new option --relabel-overlapping-bool=abc|pnn that will replace boolean subformulas by fresh atomic propositions even if those subformulas share atomic propositions. diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index ad221812e..f5ba8d625 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -132,6 +132,7 @@ static const argp_option options[] = { "hoaf", 'H', "1.1|i|k|l|m|s|t|v", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format (default). Add letters to select " "(1.1) version 1.1 of the format, " + "(b) create an alias basis if >=2 AP are used, " "(i) use implicit labels for complete deterministic automata, " "(s) prefer state-based acceptance when possible [default], " "(t) force transition-based acceptance, " diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 644d8f166..9839955f7 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -20,6 +20,7 @@ #include #include #include +#include #include #include #include @@ -30,6 +31,7 @@ #include #include #include +#include using namespace std::string_literals; @@ -70,7 +72,8 @@ namespace spot if (bdd_is_cube(a)) alias_cubes_.emplace_back(a, i); bdd neg = !a; - aliases_map_[neg.id()] = i; + // do not overwrite an existing alias with a negation + aliases_map_.emplace(neg.id(), i); if (bdd_is_cube(neg)) alias_cubes_.emplace_back(neg, i); } @@ -464,6 +467,7 @@ namespace spot bool verbose = false; bool state_labels = false; bool v1_1 = false; + bool alias_basis = false; if (opt) while (*opt) @@ -486,6 +490,9 @@ namespace spot v1_1 = false; } break; + case 'b': + alias_basis = true; + break; case 'i': implicit_labels = true; break; @@ -520,6 +527,27 @@ namespace spot throw std::runtime_error("print_hoa(): automaton is declared not weak, " "but the acceptance makes this impossible"); + // If we were asked to create an alias basis, make sure we save + // existing aliases, so we can restore it before we exit this + // function. + std::vector> old_aliases; + if (aut->ap().size() <= 1) + alias_basis = false; + if (alias_basis) + { + if (auto* aliases = get_aliases(aut)) + old_aliases = *aliases; + create_alias_basis(std::const_pointer_cast(aut)); + } + // restore the old aliases using a unique_ptr-based scope guard, + // because there are too many ways to exit this function. + auto restore_aliases = [&old_aliases, alias_basis, aut](void*) { + if (alias_basis) + set_aliases(std::const_pointer_cast(aut), old_aliases); + }; + std::unique_ptr + restore_aliases_guard((void*)1, restore_aliases); + metadata md(aut, implicit_labels, state_labels); if (acceptance == Hoa_Acceptance_States && !md.has_state_acc) @@ -1013,7 +1041,8 @@ namespace spot } void - set_aliases(twa_ptr g, std::vector> aliases) + set_aliases(twa_ptr g, + const std::vector>& aliases) { if (aliases.empty()) { @@ -1027,4 +1056,17 @@ namespace spot } } + void + create_alias_basis(const twa_graph_ptr& aut) + { + edge_separator es; + es.add_to_basis(aut); + std::vector> aliases; + unsigned n = 0; + for (bdd b: es.basis()) + aliases.emplace_back(std::to_string(n++), b); + std::reverse(aliases.begin(), aliases.end()); + set_aliases(aut, aliases); + } + } diff --git a/spot/twaalgos/hoa.hh b/spot/twaalgos/hoa.hh index 70e2c98c6..9a53f41c9 100644 --- a/spot/twaalgos/hoa.hh +++ b/spot/twaalgos/hoa.hh @@ -35,7 +35,8 @@ namespace spot /// \param os The output stream to print on. /// \param g The automaton to output. /// \param opt a set of characters each corresponding to a possible - /// option: (i) implicit labels for complete and + /// option: (b) create an alias basis if more >=2 AP + /// are used, (i) implicit labels for complete and /// deterministic automata, (k) state labels when possible, /// (s) state-based acceptance when possible, (t) /// transition-based acceptance, (m) mixed acceptance, (l) @@ -62,7 +63,8 @@ namespace spot /// /// Pass an empty vector to remove existing aliases. SPOT_API void - set_aliases(twa_ptr g, std::vector> aliases); + set_aliases(twa_ptr g, + const std::vector>& aliases); /// \ingroup twa_io /// \brief Help printing BDDs as text, using aliases. @@ -164,4 +166,18 @@ namespace spot } }; + /// \ingroup twa_io + /// \brief Create an alias basis + /// + /// This use spot::edge_separator to build a set of alias that can + /// be used as a basis for all labels of the automaton. + /// + /// Such a basis can be used to shorten the size of an output file + /// when printing in HOA format (actually, calling print_hoa() with + /// option 'b' will call this function). Such a basis may also be + /// useful to help visualize an automaton (using spot::print_dot's + /// `@` option) when its labels are too large. + SPOT_API void + create_alias_basis(const twa_graph_ptr& aut); + } diff --git a/tests/core/readsave.test b/tests/core/readsave.test index a8c301f70..b5c2f9b08 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -685,7 +685,7 @@ EOF diff output2 expect2 -SPOT_DEFAULT_FORMAT=hoa=k autfilt expect2 >output2b +SPOT_DEFAULT_FORMAT=hoa=kb autfilt expect2 >output2b cat >expect2b <output3 -autfilt -H --remove-dead input >>output3 +autfilt -Hb --remove-dead input >>output3 cat >expect3 <