diff --git a/NEWS b/NEWS index 83b2f4882..8967620df 100644 --- a/NEWS +++ b/NEWS @@ -140,6 +140,10 @@ New in spot 2.4.1.dev (not yet released) optimization for stutter-invariant automata that may produce slightly smaller automata. + - acc_cond::name(fmt) is a new method that name well-known acceptance + conditions. The fmt parameter specify the format to use for that + name (e.g. to the style used in HOA, or that used by print_dot()). + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 4b31f9ae1..f3eb97417 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1498,6 +1498,164 @@ namespace spot } + /// Return the name of this acceptance condition, in the + /// specified format. + std::string acc_cond::name(const char* fmt) const + { + bool accentuated = false; + bool no_extra_param = false; + bool no_main_param = false; + bool no_parity_param = false; + bool abbreviate = false; + bool like_names = false; + bool other = false; + + if (fmt) + while (*fmt) + switch (char c = *fmt++) + { + case '0': // no param style + no_extra_param = no_main_param = no_parity_param = true; + break; + case 'a': + accentuated = true; + break; + case 'b': + abbreviate = true; + break; + case 'd': // print_dot() style + accentuated = no_extra_param = abbreviate = like_names = true; + break; + case 'g': + no_extra_param = true; + break; + case 'l': + like_names = true; + break; + case 'm': + no_main_param = true; + break; + case 'p': + no_parity_param = true; + break; + case 'o': + other = true; + break; + case 's': + other = no_extra_param = no_main_param = no_parity_param = + like_names = true; + break; + default: + throw std::runtime_error + (std::string("unknown option for acc_cond::name(): ") + c); + } + + std::ostringstream os; + + auto gen = [abbreviate]() + { + return abbreviate ? "gen. " : "generalized-"; + }; + auto sets = [no_main_param, this]() -> std::string + { + return no_main_param ? "" : " " + std::to_string(num_sets()); + }; + + if (is_generalized_buchi()) + { + if (is_all()) + os << "all"; + else if (is_buchi()) + os << (accentuated ? "Büchi" : "Buchi"); + else + os << gen() << (accentuated ? "Büchi" : "Buchi") << sets(); + } + else if (is_generalized_co_buchi()) + { + if (is_none()) + os << "none"; + else if (is_co_buchi()) + os << (accentuated ? "co-Büchi" : "co-Buchi"); + else + os << gen() << (accentuated ? "co-Büchi" : "co-Buchi") << sets(); + } + else + { + int r = is_rabin(); + assert(r != 0); + if (r > 0) + { + os << "Rabin"; + if (!no_main_param) + os << ' ' << r; + } + else + { + r = is_streett(); + assert(r != 0); + if (r > 0) + { + os << "Streett"; + if (!no_main_param) + os << ' ' << r; + } + else + { + std::vector pairs; + if (is_generalized_rabin(pairs)) + { + os << gen() << "Rabin"; + if (!no_main_param) + { + os << ' ' << pairs.size(); + if (!no_extra_param) + for (auto p: pairs) + os << ' ' << p; + } + } + else + { + bool max = false; + bool odd = false; + if (is_parity(max, odd)) + { + os << "parity"; + if (!no_parity_param) + os << (max ? " max" : " min") + << (odd ? " odd" : " even"); + os << sets(); + } + else if (like_names) + { + std::vector r_pairs; + bool r_like = is_rabin_like(r_pairs); + unsigned rsz = r_pairs.size(); + std::vector s_pairs; + bool s_like = is_streett_like(s_pairs); + unsigned ssz = s_pairs.size(); + if (r_like && (!s_like || (rsz <= ssz))) + { + os << "Rabin-like"; + if (!no_main_param) + os << ' ' << rsz; + } + else if (s_like && (!r_like || (ssz < rsz))) + { + os << "Streett-like"; + if (!no_main_param) + os << ' ' << ssz; + } + } + } + } + } + } + std::string res = os.str(); + if (other && res.empty()) + res = "other" + sets(); + return res; + } + namespace { diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index e17f7feae..26fb9a5e4 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -33,6 +33,7 @@ namespace spot { class mark_container; } + class SPOT_API acc_cond { public: @@ -899,7 +900,6 @@ namespace spot std::function set_printer = nullptr) const; - /// \brief Construct an acc_code from a string. /// /// The string can follow the following grammar: @@ -1313,6 +1313,19 @@ namespace spot return {num_sets(), code_.remove(all_sets() - rem, true)}; } + /// \brief Return the name of this acceptance condition, in the + /// specified format. + /// + /// The empty string is returned if no name is known. + /// + /// \a fmt should be a combination of the following letters. (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'. + std::string name(const char* fmt = "alo") const; + protected: mark_t::value_t all_sets_() const { diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 5e1aefee4..cb8efa123 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -455,85 +455,9 @@ namespace spot } } - std::string get_acceptance_for_human() - { - std::ostringstream os; - - if (aut_->acc().is_generalized_buchi()) - { - if (aut_->acc().is_all()) - os << "all"; - else if (aut_->acc().is_buchi()) - os << "Büchi"; - else - os << "gen. Büchi " << aut_->num_sets(); - } - else if (aut_->acc().is_generalized_co_buchi()) - { - if (aut_->acc().is_none()) - os << "none"; - else if (aut_->acc().is_co_buchi()) - os << "co-Büchi"; - else - os << "gen. co-Büchi " << aut_->num_sets(); - } - else - { - int r = aut_->acc().is_rabin(); - assert(r != 0); - if (r > 0) - { - os << "Rabin " << r; - } - else - { - r = aut_->acc().is_streett(); - assert(r != 0); - if (r > 0) - { - os << "Streett " << r; - } - else - { - std::vector pairs; - if (aut_->acc().is_generalized_rabin(pairs)) - { - os << "gen. Rabin " << pairs.size(); - } - else - { - bool max = false; - bool odd = false; - if (aut_->acc().is_parity(max, odd)) - { - os << "parity " - << (max ? "max " : "min ") - << (odd ? "odd " : "even ") - << aut_->num_sets(); - } - else - { - std::vector r_pairs; - bool r_like = aut_->acc().is_rabin_like(r_pairs); - unsigned rsz = r_pairs.size(); - std::vector s_pairs; - bool s_like = aut_->acc().is_streett_like(s_pairs); - unsigned ssz = s_pairs.size(); - if (r_like && (!s_like || (rsz <= ssz))) - os << "Rabin-like " << rsz; - else if (s_like && (!r_like || (ssz < rsz))) - os << "Streett-like " << ssz; - } - } - } - } - } - return os.str(); - } - void print_acceptance_for_human() { - std::string accstr = get_acceptance_for_human(); + std::string accstr = aut_->acc().name("d"); if (accstr.empty()) return; os_ << nl_ << '[' << accstr << ']'; diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb index 1922bcf23..bcff265be 100644 --- a/tests/python/acc_cond.ipynb +++ b/tests/python/acc_cond.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.4" + "version": "3.6.3" }, "name": "" }, @@ -1266,6 +1266,36 @@ ], "prompt_number": 46 }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "If the acceptance condition has some known name, it can be retrieved using the `name()` method. By default the name given is a human-readable string close that used in the HOA format, but with proper accents, and support for name like `Streett-like` or `Rabin-like`. The argument `arg` can specify a different style using the same syntax as in `--format='%[arg]g'` when using the command-line tools." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(acc.name())\n", + "print(acc.name(\"d\")) # <- Style used by print_dot(aut, \"a\")\n", + "print(acc.name(\"0\")) # <- no parameters" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "generalized-B\u00fcchi 4\n", + "gen. B\u00fcchi 4\n", + "generalized-Buchi\n" + ] + } + ], + "prompt_number": 47 + }, { "cell_type": "markdown", "metadata": {}, @@ -1293,7 +1323,7 @@ ] } ], - "prompt_number": 47 + "prompt_number": 48 }, { "cell_type": "markdown", @@ -1314,13 +1344,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 48, + "prompt_number": 49, "text": [ "{0,1,2,3}" ] } ], - "prompt_number": 48 + "prompt_number": 49 }, { "cell_type": "markdown", @@ -1351,7 +1381,7 @@ ] } ], - "prompt_number": 49 + "prompt_number": 50 }, { "cell_type": "markdown", @@ -1381,7 +1411,7 @@ ] } ], - "prompt_number": 50 + "prompt_number": 51 }, { "cell_type": "code", @@ -1403,7 +1433,7 @@ ] } ], - "prompt_number": 51 + "prompt_number": 52 }, { "cell_type": "code", @@ -1425,7 +1455,7 @@ ] } ], - "prompt_number": 52 + "prompt_number": 53 } ], "metadata": {}