diff --git a/NEWS b/NEWS index 8967620df..1663d6ccc 100644 --- a/NEWS +++ b/NEWS @@ -49,6 +49,17 @@ New in spot 2.4.1.dev (not yet released) implication-based simplification rules of ltl2tgba. See the spot-x man-page for details. + - The --format=%g option of tools that output automata used to + print the acceptance condition as a *formula* in the HOA format. + This %g can now take optional arguments to print the acceptance + *name* in different formats. For instance + + ... | autfilt -o '%[s]g.hoa' + + will separate a stream of automata into different files named + by their acceptance name (Buchi, co-Buchi, Streett, etc.) or + "other" if no name is known for the acceptance condition. + Library: - Rename three methods of spot::scc_info. New names are clearer. The diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index c175da88b..4cc2b771a 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -159,6 +159,21 @@ const struct argp aoutput_argp = { options, parse_opt_aoutput, nullptr, nullptr, char F_doc[32] = "name of the input file"; char L_doc[32] = "location in the input file"; +#define doc_g \ + "acceptance condition (in HOA syntax); add brackets to print " \ + "an acceptance name instead and LETTERS to tweak the format: " \ + "(0) no parameters, " \ + "(a) accentuated, " \ + "(b) abbreviated, " \ + "(d) style used in dot output, " \ + "(g) no generalized parameter, " \ + "(l) recognize Street-like and Rabin-like, " \ + "(m) no main parameter, " \ + "(p) no parity parameter, " \ + "(o) name unknown acceptance as 'other', " \ + "(s) shorthand for 'lo0'." + + static const argp_option io_options[] = { /**************************************************/ @@ -180,8 +195,8 @@ static const argp_option io_options[] = "number of reachable transitions", 0 }, { "%A, %a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, - { "%G, %g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "acceptance condition (in HOA syntax)", 0 }, + { "%G, %g, %[LETTERS]G, %[LETTERS]g", 0, nullptr, + OPTION_DOC | OPTION_NO_USAGE, doc_g, 0 }, { "%C, %c, %[LETTERS]C, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs; you may filter the SCCs to count " @@ -241,8 +256,8 @@ static const argp_option o_options[] = "number of reachable transitions", 0 }, { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, - { "%g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "acceptance condition (in HOA syntax)", 0 }, + { "%g, %[LETTERS]g", 0, nullptr, + OPTION_DOC | OPTION_NO_USAGE, doc_g, 0 }, { "%c, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs; you may filter the SCCs to count " "using the following LETTERS, possibly concatenated: (a) accepting, " @@ -464,13 +479,9 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, if (has('P')) haut_complete_ = is_complete(haut->aut); - if (has('G')) - { - std::ostringstream os; - os << haut->aut->get_acceptance(); - haut_gen_acc_ = os.str(); - } + haut_gen_acc_ = haut->aut->acc(); + if (has('W')) { if (auto word = haut->aut->accepting_word()) diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index bde94d0cd..98724b61b 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -156,7 +156,7 @@ private: spot::printable_value aut_name_; spot::printable_value aut_word_; spot::printable_value haut_word_; - spot::printable_value haut_gen_acc_; + spot::printable_acc_cond haut_gen_acc_; spot::printable_value haut_states_; spot::printable_value haut_edges_; spot::printable_value haut_trans_; diff --git a/doc/org/randaut.org b/doc/org/randaut.org index 2ef48d1dc..99639c4af 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -163,7 +163,6 @@ $txt #+RESULTS: [[file:randaut3.png]] - * Acceptance condition The generation of the acceptance sets abn is controlled with the following four parameters: @@ -471,6 +470,30 @@ The output format can be controlled using [[file:oaut.org][the common output opt like =--hoaf=, =--dot==, =--lbtt=, and =--spin=. Note that =--spin= automatically implies =--ba=. +Automata are send to standard output by default, by you can use =-o= +to give a filename, or even a pattern for filenames. For instance the +following generates 20 automatas, but store them in different files +according to the acceptance condition. The format =%g= represent the +formula for the acceptance condition and would not make a nice +filename, but =%[s]g= is a short name for that acceptance condition +(its is replaced by "other" if Spot does not know better). + +#+BEGIN_SRC sh :results verbatim :exports both +randaut -n20 -Q10 -A 'random 3' 2 -o 'randaut-%[s]g.hoa' +wc -l randaut-*.hoa +#+END_SRC + +#+RESULTS: +: 222 randaut-Rabin-like.hoa +: 380 randaut-Streett-like.hoa +: 100 randaut-generalized-Buchi.hoa +: 249 randaut-other.hoa +: 951 total + +#+BEGIN_SRC sh :results silent :exports results +rm -f rautaut-*.hoa +#+END_SRC + * Generating a stream of automata Use option =-n= to specify a number of automata to build. A negative diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index a68912ad2..cfcdd51c5 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -331,6 +331,31 @@ namespace spot os << count; } + void printable_acc_cond::print(std::ostream& os, const char* pos) const + { + if (*pos != '[') + { + os << val_.get_acceptance(); + return; + } + const char* beg = pos; + ++pos; + const char* end = strchr(pos, ']'); + try + { + os << val_.name(std::string(pos, end).c_str()); + } + catch (const std::runtime_error& e) + { + std::ostringstream tmp; + tmp << "while processing %" + << std::string(beg, end + 2) << ", "; + tmp << e.what(); + throw std::runtime_error(tmp.str()); + + } + } + stat_printer::stat_printer(std::ostream& os, const char* format) : format_(format) @@ -397,11 +422,7 @@ namespace spot } if (has('g')) - { - std::ostringstream os; - os << aut->get_acceptance(); - gen_acc_ = os.str(); - } + gen_acc_ = aut->acc(); auto& os = format(format_); // Make sure we do not hold a pointer to the automaton or the diff --git a/spot/twaalgos/stats.hh b/spot/twaalgos/stats.hh index be67c66fc..6f8655134 100644 --- a/spot/twaalgos/stats.hh +++ b/spot/twaalgos/stats.hh @@ -70,6 +70,20 @@ namespace spot print(std::ostream& os, const char*) const override; }; + class SPOT_API printable_acc_cond final: public spot::printable + { + acc_cond val_; + public: + printable_acc_cond& + operator=(const acc_cond& new_val) + { + val_ = new_val; + return *this; + } + + void print(std::ostream& os, const char* pos) const override; + }; + class SPOT_API printable_scc_info final: public spot::printable { @@ -117,7 +131,7 @@ namespace spot printable_value nondetstates_; printable_value deterministic_; printable_value complete_; - printable_value gen_acc_; + printable_acc_cond gen_acc_; }; /// @} diff --git a/tests/core/acc2.test b/tests/core/acc2.test index 8f808f1c7..2d885749e 100755 --- a/tests/core/acc2.test +++ b/tests/core/acc2.test @@ -25,10 +25,22 @@ set -e ltl2tgba -H 'GFa & GFb' > in grep 'Acceptance:' in > expected +grep 'acc-name:' in > expected-b ltl2tgba -H 'GFa & GFb' --stats='Acceptance: %a %g' > out1 +ltl2tgba -H 'GFa & GFb' --stats='acc-name: %[]g' > out1b autfilt -H in --format='Acceptance: %A %G' > out2 +autfilt -H in --format='acc-name: %[]G' > out2b diff out1 expected diff out2 expected +diff out1b expected-b +diff out2b expected-b + +autfilt -H in --format='%[d]G, %[0lo]g, %[0abdglmpos]g' > out3 +echo 'gen. Büchi 2, generalized-Buchi, gen. Büchi' >exp3 +diff out3 exp3 + +autfilt -H in --format='%[bug]g' 2>err && exit 1 +grep '%\[bug\]g.*: u' err cat >header <