diff --git a/NEWS b/NEWS index 414257e60..f40b14548 100644 --- a/NEWS +++ b/NEWS @@ -13,7 +13,7 @@ New in spot 2.3.3.dev (not yet released) - genaut is a binary to produce families of automata defined in the literature (in the same way as we have genltl for LTL formulas). - It currently features only one class of automata. + It currently features only two classes of automata. Library: diff --git a/bin/genaut.cc b/bin/genaut.cc index e4208bb9e..9eff69223 100644 --- a/bin/genaut.cc +++ b/bin/genaut.cc @@ -53,6 +53,9 @@ static const argp_option options[] = { "ks-cobuchi", gen::AUT_KS_COBUCHI, "RANGE", 0, "A co-Büchi automaton with 2N+1 states for which any equivalent " "deterministic co-Büchi automaton has at least 2^N/(2N+1) states.", 0}, + { "l-nba", gen::AUT_L_NBA, "RANGE", 0, + "A Büchi automaton with 3N+1 states whose complementary Streett " + "automaton needs at least n! states.", 0}, RANGE_DOC, /**************************************************/ { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, diff --git a/bin/man/genaut.x b/bin/man/genaut.x index 0035b7faa..5b38075c0 100644 --- a/bin/man/genaut.x +++ b/bin/man/genaut.x @@ -7,7 +7,11 @@ Prefixes used in pattern names refer to the following papers: .TP ks D. Kuperberg, M. Skrzypczak: On Determinisation of Good-for-Games -Automata. Proceddings of ICALP'15. +Automata. Proceedings of ICALP'15. +.TP +l +C. Löding: Optimal Bounds for Transformations of ω-Automata. +Proceedings of FSTTCS'99. [SEE ALSO] .BR autfilt (1), diff --git a/doc/org/genaut.org b/doc/org/genaut.org index a2d8f51a3..9a8430a19 100644 --- a/doc/org/genaut.org +++ b/doc/org/genaut.org @@ -17,6 +17,9 @@ genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' : --ks-cobuchi=RANGE A co-Büchi automaton with 2N+1 states for which : any equivalent deterministic co-Büchi automaton : has at least 2^N/(2N+1) states. +: --l-nba=RANGE A Büchi automaton with 3N+1 states whose +: complementary Streett automaton needs at least n! +: states. By default, the output format is [[file:hoa.org][HOA]], but this can be controlled using diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc index dee729b4d..488ea0595 100644 --- a/spot/gen/automata.cc +++ b/spot/gen/automata.cc @@ -88,6 +88,39 @@ namespace spot aut->prop_state_acc(true); return aut; } + + static twa_graph_ptr + l_nba(unsigned n, bdd_dict_ptr dict) + { + if (n == 0) + throw std::runtime_error("l_nba expects a positive argument"); + + auto aut = make_twa_graph(dict); + + bdd p1 = bdd_ithvar(aut->register_ap("a")); + bdd p2 = bdd_ithvar(aut->register_ap("b")); + bdd a = p1 - p2; + bdd b = p2 - p1; + bdd s = p1 & p2; + bdd all = p1 | p2; + + aut->new_states(3 * n + 1); + aut->set_init_state(1); + aut->set_buchi(); + aut->prop_state_acc(true); + + aut->new_acc_edge(0, n + 1, a); + aut->new_edge(2 * n + 1, 0, b); + for (unsigned s = 1; s <= n; ++s) + { + aut->new_edge(s + n, std::min(s + n + 1, 2 * n), a); + aut->new_edge(s + n, s, b); + aut->new_edge(s, s, all); + aut->new_edge(s, s + 2 * n, a); + aut->new_edge(std::min(s + 2 * n + 1, 3 * n), s + 2 * n, a); + } + return aut; + } } twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict) @@ -105,6 +138,8 @@ namespace spot // Keep this alphabetically-ordered! case AUT_KS_COBUCHI: return ks_cobuchi(n, dict); + case AUT_L_NBA: + return l_nba(n, dict); case AUT_END: break; } @@ -116,6 +151,7 @@ namespace spot static const char* const class_name[] = { "ks-cobuchi", + "l-nba", }; // Make sure we do not forget to update the above table every // time a new pattern is added. diff --git a/spot/gen/automata.hh b/spot/gen/automata.hh index 182906968..d1f96f421 100644 --- a/spot/gen/automata.hh +++ b/spot/gen/automata.hh @@ -31,23 +31,56 @@ namespace spot AUT_BEGIN = 256, /// \brief A family of co-Büchi automata. /// - /// ks_cobuchi(n) is a co-Büchi automaton of size 2n+1 that is - /// good-for-games and that has no equivalent deterministic co-Büchi - /// automaton with less than 2^n / (2n+1) states. - /// For details and other classes, see: - /// - /// @InProceedings{kuperberg2015determinisation, - /// author={Kuperberg, Denis and Skrzypczak, Micha{\l}}, - /// title={On Determinisation of Good-for-Games Automata}, - /// booktitle={International Colloquium on Automata, Languages, and - /// Programming}, - /// pages={299--310}, - /// year={2015}, - /// organization={Springer} - /// } + /// Builds a co-Büchi automaton of size 2n+1 that is + /// good-for-games and that has no equivalent deterministic + /// co-Büchi automaton with less than 2^n / (2n+1) states. /// /// Only defined for n>0 + /// + /** \verbatim + @InProceedings{ kuperberg.15.icalp, + author = {Denis Kuperberg and Micha{\l} Skrzypczak }, + title = {On Determinisation of Good-for-Games Automata}, + booktitle = {Proceedings of the 42nd International Colloquium on + Automata, Languages, and Programming (ICALP'15)}, + pages = {299--310}, + year = {2015}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = 9135, + doi = {10.1007/978-3-662-47666-6_24} + } + \endverbatim */ AUT_KS_COBUCHI = AUT_BEGIN, + /// \brief Hard-to-complement non-deterministic Büchi automata + /// + /// Build a non-deterministic Büchi automaton with 3n+1 states + /// and whose complementary language requires an automaton with + /// at least n! states if Streett acceptance is used. + /// + /// Only defined for n>0. The automaton constructed corresponds + /// to the right part of Fig.1 in the following paper, except + /// that only state q_1 is initial. (The fact that states q_2, + /// q_3, ..., and q_n are not initial as in the paper does not + /// change the recognized language.) + /// + /** \verbatim + @InProceedings{loding.99.fstts, + author = {Christof L{\"o}ding}, + title = {Optimal Bounds for Transformations of + $\omega$-Automata}, + booktitle = {Proceedings of the 19th Conference on Foundations of + Software Technology and Theoretical Computer Science + (FSTTCS'99)}, + year = 1999, + publisher = {Springer}, + pages = {97--109}, + series = {Lecture Notes in Computer Science}, + volume = 1738, + doi = {10.1007/3-540-46691-6_8} + } + \endverbatim */ + AUT_L_NBA, AUT_END }; diff --git a/tests/core/genaut.test b/tests/core/genaut.test index b6c08e714..22d51b078 100644 --- a/tests/core/genaut.test +++ b/tests/core/genaut.test @@ -29,13 +29,18 @@ s/[=[].*/=1/p res=`genaut $opts --stats="--%F=%L"` test "$opts" = "$res" -genaut --ks-cobuchi=..3 --stats=%s,%e,%t,%c,%g >out +genaut --ks-cobuchi=..3 --l-nba=..3 --stats=%s,%e,%t,%c,%g >out cat >expected <err && exit 1 grep positive err +genaut --l-nba=0 2>err && exit 1 +grep positive err diff --git a/tests/python/gen.py b/tests/python/gen.py index 2b74f3ec3..fc7e19067 100644 --- a/tests/python/gen.py +++ b/tests/python/gen.py @@ -31,7 +31,7 @@ assert k2.num_states() == 5 # the type returned by spot.gen.ks_cobuchi() is the correct one. assert 'to_str' in dir(k2) -k3 = gen.aut_pattern(gen.AUT_KS_COBUCHI, 3) +k3 = gen.aut_pattern(gen.AUT_L_NBA, 3) assert k2.get_dict() == k3.get_dict() try: @@ -63,3 +63,7 @@ else: assert 40 == sum(p.size() for p in gen.ltl_patterns((gen.LTL_OR_G, 1, 5), (gen.LTL_GH_Q, 3), gen.LTL_EH_PATTERNS)) + +assert 32 == sum(p.num_states() + for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3), + (gen.AUT_KS_COBUCHI, 5)))