From f2616069be4b6dbefda33ad8e409f0fe320fd86b Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Sat, 17 Jun 2017 21:31:43 +0200 Subject: [PATCH] twaalgos/cobuchi: Add dnf_to_nca() method * NEWS: Update. * spot/twaalgos/cobuchi.hh: Declare dnf_to_nca(). * spot/twaalgos/cobuchi.cc: Implement it. * tests/core/dca.test: Add tests. --- NEWS | 15 +-- spot/twaalgos/cobuchi.cc | 42 ++++++- spot/twaalgos/cobuchi.hh | 32 ++++- tests/core/dca.test | 266 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 343 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index 9d5f3ee47..8b45690cb 100644 --- a/NEWS +++ b/NEWS @@ -23,18 +23,19 @@ New in spot 2.4.0.dev (not yet released) specified SCC. It must only be called on automata with a Streett-like acceptance condition. - - The new function nsa_to_nca() is able to convert when possible an - automaton with a Streett-like acceptance to an equivalent - automaton with a co-Büchi acceptance. Actually the resulting - automaton will always recognize at least the same language. It can - recognize more if the original language can not be expressed with - a co-Büchi acceptance condition. - - The new function dnf_to_streett() is able to convert any automaton with an acceptance condition in Disjunctive Normal Form to a Streett-like automaton. This is used by the new option '--streett-like' of autfilt. + - The new functions nsa_to_nca() and nra_to_nca() are able to convert + when possible respectively an automaton with a Streett-like + acceptance or a Rabin-like acceptance to an equivalent automaton + with a co-Büchi acceptance. Actually the resulting automaton will + always recognize at least the same language. It can recognize more + if the original language can not be expressed with a co-Büchi + acceptance condition. + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index e416f6b3a..fee28c488 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -28,6 +28,13 @@ #include #include +#define DEBUG 0 +#if DEBUG +#define debug std::cerr +#else +#define debug while (0) std::cout +#endif + namespace spot { namespace @@ -249,14 +256,45 @@ namespace spot } + twa_graph_ptr + dnf_to_nca(const const_twa_graph_ptr& ref, + bool named_states, + vect_nca_info* nca_info) + { + const acc_cond::acc_code& code = ref->get_acceptance(); + if (!code.is_dnf()) + throw std::runtime_error("dnf_to_nca() only works with DNF acceptance " + "condition"); + + auto streett_aut = spot::dnf_to_streett(ref, true); + + std::vector pairs; + if (!streett_aut->acc().is_streett_like(pairs)) + throw std::runtime_error("dnf_to_nca() could not convert the original " + "automaton into an intermediate Streett-like automaton"); + + nsa_to_nca_converter nca_converter(streett_aut, + ref, + pairs, + named_states, + true, + ref->num_states()); + return nca_converter.run(nca_info); + } + + twa_graph_ptr to_dca(const const_twa_graph_ptr& aut, bool named_states) { + const acc_cond::acc_code& code = aut->get_acceptance(); + std::vector pairs; if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity()) return nsa_to_nca(aut, named_states); + else if (code.is_dnf()) + return dnf_to_nca(aut, named_states); else - throw std::runtime_error("to_dca() only works with Streett-like or Parity" - " acceptance condition"); + throw std::runtime_error("to_dca() only works with Streett-like, Parity " + "or any acceptance condition in DNF"); } } diff --git a/spot/twaalgos/cobuchi.hh b/spot/twaalgos/cobuchi.hh index 861f63544..4906781a0 100644 --- a/spot/twaalgos/cobuchi.hh +++ b/spot/twaalgos/cobuchi.hh @@ -26,9 +26,10 @@ namespace spot { - /// A vector of nca_st_info is given as argument to nsa_to_nca(). Each - /// nca_st_info has information about a state that must be seen infinitely - /// often. For a state 's' visited infinitely often by a run, the information + /// A vector of nca_st_info is given as argument to nsa_to_nca() or + /// dnf_to_nca(). Each nca_st_info has information about a state that must be + /// seen infinitely often. + /// For a state 's' visited infinitely often by a run, the information /// provided is: /// - the clause number satisfied by the run (from left to right) /// - the state number of 's' @@ -81,6 +82,31 @@ namespace spot bool named_states = false, vect_nca_info* nca_info = nullptr); + /// \brief Converts an aut. with acceptance in DNF to a nondet. co-Büchi aut. + /// + /// This function converts the Rabin-like automaton into a Strett-like + /// automaton and then calls nsa_to_nca() on it. It is described in section + /// 3.2 of: + /** \verbatim + @Article{boker.2009.lcs, + author = {Udi Boker and Orna Kupferman}, + title = {Co-Büching Them All}, + booktitle = {Foundations of Software Science and Computational + Structures - 14th International Conference, FOSSACS 2011} + year = {2011}, + pages = {184--198}, + url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}} + } + \endverbatim */ + /// + /// \a aut The automaton to convert. + /// \a named_states name each state for easier debugging. + /// \a nca_info retrieve information about state visited infinitely often. + SPOT_API twa_graph_ptr + dnf_to_nca(const const_twa_graph_ptr& aut, + bool named_states = false, + vect_nca_info* nca_info = nullptr); + /// \brief Converts any ω-automata to det. co-buchi (when possible) /// /// The resulting automaton will always recognize at least the same language. diff --git a/tests/core/dca.test b/tests/core/dca.test index 64641c8e7..ece9bf11f 100644 --- a/tests/core/dca.test +++ b/tests/core/dca.test @@ -197,3 +197,269 @@ do autfilt input.hoa --included-in=res.hoa done done + +cat formulas | ltlcross \ + --timeout=60 \ + '{1} ltl2tgba %f | autfilt --gra >%T' \ + '{2} case `ltlfilt -f %f --format=%\[w]h` in *P*) ltl2tgba -B %f | autfilt\ + --gra | autfilt --dca ;; *) ltl2tgba -B %f;; esac >%O' + +cat > bigtest.hoa << EOF +HOA: v1 +States: 29 +Start: 7 +AP: 3 "a" "b" "c" +Acceptance: 5 Fin(0) & (Inf(1) | Fin(2)) & (Inf(3) | Fin(4)) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 {3} +[0&!1&!2] 0 +[0&1&!2] 1 +[0&!1&2] 4 +[!0&1&2] 13 +[!0&!1&2] 15 +[!0&1&!2] 20 +[!0&!1&!2] 21 +[0&1&2] 22 +State: 1 {3} +[0&!1&!2] 0 +[0&1&!2] 1 +[!0&2] 13 +[!0&1&!2] 20 +[!0&!1&!2] 21 +[0&2] 22 +State: 2 {3} +[0&!1&2] 2 +[0&!1&!2] 3 +[0&1&!2] 12 +[!0&1] 13 +[0&1&2] 14 +[!0&!1] 15 +State: 3 {3} +[0&!1&2] 2 +[0&!1&!2] 3 +[0&1&!2] 12 +[!0&1&2] 13 +[0&1&2] 14 +[!0&!1&2] 15 +[!0&!1&!2] 16 +[!0&1&!2] 20 +State: 4 {3} +[0&!1&!2] 3 +[0&!1&2] 4 +[0&1&!2] 12 +[!0&1] 13 +[!0&!1] 15 +[0&1&2] 22 +State: 5 {3} +[0&!1&2] 5 +[0&1&!2] 12 +[!0&1] 13 +[0&1&2] 14 +[!0&!1] 15 +[0&!1&!2] 17 +State: 6 {3} +[0&!1&2] 5 +[0&!1&!2] 6 +[!0&1&2] 13 +[0&1&2] 14 +[!0&!1&2] 15 +[0&1&!2] 18 +[!0&1&!2] 20 +[!0&!1&!2] 28 +State: 7 {1 3} +[!0 | 2] 13 +[0&1&!2] 18 +[0&!1&!2] 19 +State: 8 {1 3} +[0&1&!2] 1 +[0&!1&2] 8 +[0&!1&!2] 9 +[!0&1] 13 +[0&1&2] 22 +[!0&!1] 23 +State: 9 {1 3} +[0&1&!2] 1 +[0&!1&2] 8 +[0&!1&!2] 9 +[!0&1&2] 13 +[!0&1&!2] 20 +[0&1&2] 22 +[!0&!1&2] 23 +[!0&!1&!2] 24 +State: 10 {1 3} +[0&1&!2] 10 +[0&!1&!2] 11 +[!0&2] 13 +[0&2] 22 +[!0&1&!2] 25 +[!0&!1&!2] 26 +State: 11 {1 3} +[0&!1&2] 8 +[0&1&!2] 10 +[0&!1&!2] 11 +[!0&1&2] 13 +[0&1&2] 22 +[!0&!1&2] 23 +[!0&1&!2] 25 +[!0&!1&!2] 26 +State: 12 {0 1 3} +[0&!1&!2] 0 +[0&1&!2] 1 +[!0&2] 13 +[!0&1&!2] 20 +[!0&!1&!2] 21 +[0&2] 22 +State: 13 {0 1 3} +[0&1&!2] 10 +[0&!1&!2] 11 +[!0 | 2] 13 +State: 14 {0 1 3} +[!0] 13 +[0&1&!2] 18 +[0&!1&!2] 19 +[0&2] 22 +State: 15 {0 1 3} +[0&!1&!2] 6 +[!0&1 | 1&2] 13 +[0&1&!2] 18 +[!0&!1 | !1&2] 23 +State: 16 {0 1 3} +[0&!1&!2] 6 +[1&2] 13 +[0&1&!2] 18 +[!0&1&!2] 20 +[!1&2] 23 +[!0&!1&!2] 24 +State: 17 {0 1 3} +[0&1&!2] 1 +[0&!1&2] 8 +[0&!1&!2] 9 +[!0&1&2] 13 +[!0&1&!2] 20 +[0&1&2] 22 +[!0&!1&2] 23 +[!0&!1&!2] 24 +State: 18 {0 1 3} +[0&1&!2] 10 +[0&!1&!2] 11 +[!0&2] 13 +[0&2] 22 +[!0&1&!2] 25 +[!0&!1&!2] 26 +State: 19 {0 1 3} +[0&!1&2] 8 +[0&1&!2] 10 +[0&!1&!2] 11 +[!0&1&2] 13 +[0&1&2] 22 +[!0&!1&2] 23 +[!0&1&!2] 25 +[!0&!1&!2] 26 +State: 20 {0 1 3} +[2] 13 +[0&1&!2] 18 +[0&!1&!2] 19 +[!0&1&!2] 25 +[!0&!1&!2] 26 +State: 21 {0 1 3} +[1&2] 13 +[0&1&!2] 18 +[0&!1&!2] 19 +[!1&2] 23 +[!0&1&!2] 25 +[!0&!1&!2] 26 +State: 22 {2 3} +[!0] 13 +[0&1&!2] 18 +[0&!1&!2] 19 +[0&2] 22 +State: 23 {2 3} +[0&!1&!2] 6 +[!0&1 | 1&2] 13 +[0&1&!2] 18 +[!0&!1 | !1&2] 23 +State: 24 {2 3} +[0&!1&!2] 6 +[1&2] 13 +[0&1&!2] 18 +[!0&1&!2] 20 +[!1&2] 23 +[!0&!1&!2] 24 +State: 25 {2 3} +[2] 13 +[0&1&!2] 18 +[0&!1&!2] 19 +[!0&1&!2] 25 +[!0&!1&!2] 26 +State: 26 {2 3} +[1&2] 13 +[0&1&!2] 18 +[0&!1&!2] 19 +[!1&2] 23 +[!0&1&!2] 25 +[!0&!1&!2] 26 +State: 27 {2 3} +[0&!1&2] 5 +[0&!1&!2] 6 +[!0&1&2] 13 +[0&1&2] 14 +[!0&!1&2] 15 +[0&1&!2] 18 +[!0&1&!2] 20 +[!0&!1&!2] 28 +State: 28 {4} +[1&2] 13 +[!1&2] 15 +[0&1&!2] 18 +[!0&1&!2] 20 +[0&!1&!2] 27 +[!0&!1&!2] 28 +--END-- +EOF +autfilt bigtest.hoa --dca > res.hoa +autfilt bigtest.hoa --equivalent-to='res.hoa' + +cat >empty.hoa< res.hoa +autfilt empty.hoa --equivalent-to='res.hoa' + +cat >empty.hoa< res.hoa +autfilt empty.hoa --equivalent-to='res.hoa' + +cat >empty.hoa< res.hoa +autfilt empty.hoa --equivalent-to='res.hoa'