diff --git a/NEWS b/NEWS index af4716521..8963d2412 100644 --- a/NEWS +++ b/NEWS @@ -21,6 +21,9 @@ New in spot 2.7.5.dev (not yet released) consistency-checks (they are unnecessary when all automata could be complemented and statistics were not required). + - genaut learned --m-nba=N to generate Max Michel's NBA familly. + (NBAs with N+1 states whose determinized have at least N! states.) + Library: - Add generic_accepting_run() as a variant of generic_emptiness_check() that diff --git a/bin/genaut.cc b/bin/genaut.cc index d76f25b51..9e8f1939e 100644 --- a/bin/genaut.cc +++ b/bin/genaut.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -59,6 +59,9 @@ static const argp_option options[] = { "l-dsa", gen::AUT_L_DSA, "RANGE", 0, "A deterministic Streett automaton with 4N states with no " "equivalent deterministic Rabin automaton of less than N! states.", 0}, + { "m-nba", gen::AUT_M_NBA, "RANGE", 0, + "An NBA with N+1 states whose determinization 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 5b38075c0..bc98d8ea7 100644 --- a/bin/man/genaut.x +++ b/bin/man/genaut.x @@ -12,6 +12,10 @@ Automata. Proceedings of ICALP'15. l C. Löding: Optimal Bounds for Transformations of ω-Automata. Proceedings of FSTTCS'99. +.TP +m +M. Michel: Complementation is more difficult with automata on +infinite words. CNET, Paris (1988). Unpublished manuscript. [SEE ALSO] .BR autfilt (1), diff --git a/doc/org/genaut.org b/doc/org/genaut.org index a4408704e..fef290134 100644 --- a/doc/org/genaut.org +++ b/doc/org/genaut.org @@ -15,15 +15,19 @@ genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: -: --ks-nca=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-dsa=RANGE A deterministic Streett automaton with 4N states -: with no equivalent deterministic Rabin automaton -: of less than N! states. -: --l-nba=RANGE A Büchi automaton with 3N+1 states whose -: complementary Streett automaton needs at least N! -: states. +#+begin_example + --ks-nca=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-dsa=RANGE A deterministic Streett automaton with 4N states + with no equivalent deterministic Rabin automaton + of less than N! states. + --l-nba=RANGE A Büchi automaton with 3N+1 states whose + complementary Streett automaton needs at least N! + states. + --m-nba=RANGE An NBA with N+1 states whose determinization needs + at least N! states +#+end_example 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 bf1785dd3..00b7a5268 100644 --- a/spot/gen/automata.cc +++ b/spot/gen/automata.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2018 Laboratoire de Recherche et Developpement +// Copyright (C) 2017-2019 Laboratoire de Recherche et Developpement // de l'EPITA (LRDE). // // This file is part of Spot, a model checking library. @@ -32,7 +32,7 @@ namespace spot ks_nca(unsigned n, bdd_dict_ptr dict) { if (n == 0) - throw std::runtime_error("ks_nca expects a positive argument"); + throw std::runtime_error("ks-nca expects a positive argument"); // the alphabet has four letters: // i, s (for sigma), p (for pi), h (for hash) // we encode this four letters alphabet thanks to two AP a and b @@ -99,7 +99,7 @@ namespace spot l_nba(unsigned n, bdd_dict_ptr dict) { if (n == 0) - throw std::runtime_error("l_nba expects a positive argument"); + throw std::runtime_error("l-nba expects a positive argument"); auto aut = make_twa_graph(dict); @@ -138,7 +138,7 @@ namespace spot l_dsa(unsigned n, bdd_dict_ptr dict) { if (n < 1 || n > 16) - throw std::runtime_error("l_dsa expects 1 <= n <= 16"); + throw std::runtime_error("l-dsa expects 1 <= n <= 16"); auto aut = make_twa_graph(dict); @@ -173,6 +173,62 @@ namespace spot } } + static unsigned ulog2(unsigned n) + { + assert(n>0); + --n; +#ifdef __GNUC__ + return 8*sizeof(unsigned) - __builtin_clz(n); +#else + unsigned res = 0; + while (n) + { + ++res; + n >>= 1; + } + return res; +#endif + } + + static twa_graph_ptr + m_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); + aut->set_buchi(); + aut->new_states(n + 1); + aut->set_init_state(0); + + // How many AP to we need to represent n+1 letters + unsigned nap = ulog2(n + 1); + std::vector apvars(nap); + for (unsigned a = 0; a < nap; ++a) + apvars[a] = aut->register_ap("p" + std::to_string(a)); + + bdd all = bdd_ibuildcube(0, nap, apvars.data()); + for (unsigned letter = n; letter > 0; --letter) + { + bdd cond = bdd_ibuildcube(letter, nap, apvars.data()); + aut->new_acc_edge(0, letter, cond); + aut->new_edge(letter, 0, cond); + all |= cond; + } + for (unsigned letter = n; letter > 0; --letter) + aut->new_edge(letter, letter, all); + + aut->prop_state_acc(true); + aut->prop_universal(false); + aut->prop_complete(false); + aut->prop_inherently_weak(false); + aut->prop_stutter_invariant(false); + aut->prop_semi_deterministic(false); + + return aut; + } + twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict) { if (n < 0) @@ -192,6 +248,8 @@ namespace spot return l_nba(n, dict); case AUT_L_DSA: return l_dsa(n, dict); + case AUT_M_NBA: + return m_nba(n, dict); case AUT_END: break; } @@ -205,6 +263,7 @@ namespace spot "ks-nca", "l-nba", "l-dsa", + "m-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 25a8e6918..242620745 100644 --- a/spot/gen/automata.hh +++ b/spot/gen/automata.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Developpement de +// Copyright (C) 2017, 2019 Laboratoire de Recherche et Developpement de // l'EPITA (LRDE). // // This file is part of Spot, a model checking library. @@ -109,6 +109,29 @@ namespace spot } \endverbatim */ AUT_L_DSA, + /// \brief An NBA with (n+1) states whose complement needs ≥n! states + /// + /// This automaton is usually attributed to Max Michel (1988), + /// who described it in some unpublished documents. Other + /// descriptions of this automaton can be found in a number + /// of papers, like: + /** \verbatim + @InBook{thomas.97.chapter, + author = {Wolfgang Thomas}, + title = {Languages, Automata, and Logic}, + booktitle = {Handbook of Formal Languages --- + Volume 3 Beyond Words}, + editor = {Grzegorz Rozenberg and Arto Salomaa}, + chapter = 7, + publisher = {Springer-Verlag}, + year = {1997} + } + \endverbatim */ + /// + /// Our implementation uses $\lceil \log_2(n+1)\rceil$ atomic + /// propositions to encode the $n+1$ letters used in the + /// original alphabet. + AUT_M_NBA, AUT_END }; diff --git a/tests/core/genaut.test b/tests/core/genaut.test index 1ed813c31..064aec795 100644 --- a/tests/core/genaut.test +++ b/tests/core/genaut.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +# Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -29,7 +29,8 @@ s/[=[].*/=1/p res=`genaut $opts --stats="--%F=%L"` test "$opts" = "$res" -genaut --ks-nca=..3 --l-nba=..3 --l-dsa=..3 --stats=%s,%e,%t,%c,%g >out +genaut --ks-nca=..3 --l-nba=..3 --l-dsa=..3 --m-nba=..3 \ + --stats=%s,%e,%t,%c,%g >out cat >expected <expected < XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2' + + +# Test the behavior of our determinization on Max Michel automata. +# Any change to Spot that lowers the output.states is welcome :-) +genaut --m-nba=1..4 | autcross --language-preserved 'autfilt -D' --csv=out.csv +cut -d, -f4,17 out.csv > sizes.csv +cat >expected <