From 1ebd86de04f48e453b10a4d73b638097526e514f Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Tue, 23 Jan 2018 11:16:34 +0100 Subject: [PATCH] Improve IAR construction spot::iar() was fixed to handle correctly Rabin-like conditions. It also now supports Streett-like conditions. * NEWS, spot/twaalgos/postproc.cc: document it * spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh: implement it * tests/core/rabin2parity.test, tests/python/except.py: test it --- NEWS | 8 ++++- spot/twaalgos/postproc.cc | 8 +++-- spot/twaalgos/rabin2parity.cc | 64 +++++++++++++++++++++++++---------- spot/twaalgos/rabin2parity.hh | 20 ++++++----- tests/core/rabin2parity.test | 34 +++++++++++++++++-- tests/python/except.py | 2 +- 6 files changed, 103 insertions(+), 33 deletions(-) diff --git a/NEWS b/NEWS index 7aa56435e..da6b9f1be 100644 --- a/NEWS +++ b/NEWS @@ -1,11 +1,17 @@ New in spot 2.5.0.dev (not yet released) + Library: + + - iar() and iar_maybe() now also handle Streett-like conditions. + Bugs fixed: - streett_to_generalized_buchi() could produce incorrect result on Streett-like input with acceptance like (Inf(0)|Fin(1))&Fin(1) where some Fin(x) is used both with and without a paired Fin(y). + - iar() and iar_maybe() properly handle Rabin-like conditions. + New in spot 2.5 (2018-01-20) Build: @@ -92,7 +98,7 @@ New in spot 2.5 (2018-01-20) New functions in the library: - spot::iar() and spot::iar_maybe() use index appearance records (IAR) - to translate Rabin-like automata into equivalent parity automaton. + to translate Rabin-like automata into equivalent parity automata. This translation preserves determinism and is especially useful when the input automaton is deterministic. diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 8769d2978..4203e5b57 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -242,10 +242,12 @@ namespace spot || (want_parity && !a->acc().is_parity())) { twa_graph_ptr b = nullptr; - if (want_parity && is_deterministic(a)) + if (want_parity && is_deterministic(a) && + !a->acc().is_generalized_buchi()) b = iar_maybe(a); - // possible only if a was deterministic and Rabin-like and - // we want parity + // possible only if a was deterministic and (Rabin-like or Streett-like) + // and we want parity and a is not a TGBA + // NB: on a TGBA, degeneralization is better than IAR if (b) a = b; else diff --git a/spot/twaalgos/rabin2parity.cc b/spot/twaalgos/rabin2parity.cc index 71d843c94..c41638c63 100644 --- a/spot/twaalgos/rabin2parity.cc +++ b/spot/twaalgos/rabin2parity.cc @@ -21,7 +21,6 @@ #include #include -#include namespace spot { @@ -41,8 +40,27 @@ namespace spot } }; + template class iar_generator { + // helper functions: access fin and inf parts of the pairs + // these functions negate the Streett condition to see it as a Rabin one + const acc_cond::mark_t& + fin(unsigned k) const + { + if (is_rabin) + return pairs_[k].fin; + else + return pairs_[k].inf; + } + acc_cond::mark_t + inf(unsigned k) const + { + if (is_rabin) + return pairs_[k].inf; + else + return pairs_[k].fin; + } public: explicit iar_generator(const const_twa_graph_ptr& a, const std::vector& p) @@ -60,10 +78,14 @@ namespace spot build_iar_scc(scc_.initial()); // resulting automaton has acceptance condition: parity max odd - // with priorities ranging from 0 to 2*(nb Rabin pairs) + // with priorities ranging from 0 to 2*(nb pairs) // /!\ priorities are shifted by -1 compared to the original paper - res_->set_acceptance(2*pairs_.size() + 1, - acc_cond::acc_code::parity(true, true, 2*pairs_.size() + 1)); + if (is_rabin) + res_->set_acceptance(2*pairs_.size() + 1, + acc_cond::acc_code::parity(true, true, 2*pairs_.size() + 1)); + else + res_->set_acceptance(2*pairs_.size() + 1, + acc_cond::acc_code::parity(true, false, 2*pairs_.size() + 1)); // set initial state res_->set_init_state( @@ -117,11 +139,11 @@ namespace spot return; } - // determine the Rabin pairs that appear in the SCC + // determine the pairs that appear in the SCC auto colors = scc_.acc_sets_of(scc_num); std::set scc_pairs; for (unsigned k = 0; k != pairs_.size(); ++k) - if (colors & (pairs_[k].fin | pairs_[k].inf)) + if (inf(k) == 0U || (colors & (pairs_[k].fin | pairs_[k].inf))) scc_pairs.insert(k); perm_t p0; @@ -150,10 +172,9 @@ namespace spot perm_t new_perm = current.perm; // Count pairs whose fin-part is seen on this transition unsigned seen_nb = 0; - std::vector seen; // consider the pairs for this SCC only for (unsigned k : scc_pairs) - if (e.acc & pairs_[k].fin) + if (e.acc & fin(k)) { ++seen_nb; auto it = std::find(new_perm.begin(), @@ -192,7 +213,8 @@ namespace spot for (unsigned k = 0; k != current.perm.size(); ++k) { unsigned pk = current.perm[k]; - if (e.acc & (pairs_[pk].fin | pairs_[pk].inf)) + if (inf(pk) == 0U || + (e.acc & (pairs_[pk].fin | pairs_[pk].inf))) // k increases in the loop, so k > maxint necessarily maxint = k; } @@ -200,7 +222,7 @@ namespace spot acc_cond::mark_t acc = 0U; if (maxint == -1U) acc = {0}; - else if (e.acc & pairs_[current.perm[maxint]].fin) + else if (e.acc & fin(current.perm[maxint])) acc = {2*maxint+2}; else acc = {2*maxint+1}; @@ -271,12 +293,20 @@ namespace spot twa_graph_ptr iar_maybe(const const_twa_graph_ptr& aut) { - std::vector rabin_pairs; - if (!aut->acc().is_rabin_like(rabin_pairs)) - return nullptr; - - iar_generator gen(aut, rabin_pairs); - return gen.run(); + std::vector pairs; + if (!aut->acc().is_rabin_like(pairs)) + if (!aut->acc().is_streett_like(pairs)) + return nullptr; + else + { + iar_generator gen(aut, pairs); + return gen.run(); + } + else + { + iar_generator gen(aut, pairs); + return gen.run(); + } } twa_graph_ptr @@ -284,6 +314,6 @@ namespace spot { if (auto res = iar_maybe(aut)) return res; - throw std::runtime_error("iar() expects Rabin-like input"); + throw std::runtime_error("iar() expects Rabin-like or Streett-like input"); } } diff --git a/spot/twaalgos/rabin2parity.hh b/spot/twaalgos/rabin2parity.hh index 56fd78142..e2e8d6848 100644 --- a/spot/twaalgos/rabin2parity.hh +++ b/spot/twaalgos/rabin2parity.hh @@ -23,30 +23,32 @@ namespace spot { /// \ingroup twa_acc_transform - /// \brief Turn a Rabin-like automaton into a parity automaton based on the - /// index appearence record (IAR) + /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton + /// based on the index appearence record (IAR) /// /// If the input automaton has n states and k pairs, the output automaton has /// at most k!*n states and 2k+1 colors. If the input automaton is /// deterministic, the output automaton is deterministic as well, which is the /// intended use case for this function. If the input automaton is /// non-deterministic, the result is still correct, but way larger than an - /// equivalent Büchi automaton. The output parity automaton has max odd - /// acceptance condition. + /// equivalent Büchi automaton. + /// If the input automaton is Rabin-like (resp. Streett-like), the output + /// automaton has max odd (resp. min even) acceptance condition. /// Details on the algorithm can be found in: /// https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017) /// - /// Throws an std::runtime_error if the input is not Rabin-like. + /// Throws an std::runtime_error if the input is neither Rabin-like nor + /// Street-like. SPOT_API twa_graph_ptr iar(const const_twa_graph_ptr& aut); /// \ingroup twa_acc_transform - /// \brief Turn a Rabin-like automaton into a parity automaton based on the - /// index appearence record (IAR) + /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton + /// based on the index appearence record (IAR) /// - /// Return nullptr if the input automaton is not Rabin-like, and - /// calls spot::iar() otherwise. + /// Returns nullptr if the input automaton is neither Rabin-like nor + /// Streett-like, and calls spot::iar() otherwise. SPOT_API twa_graph_ptr iar_maybe(const const_twa_graph_ptr& aut); diff --git a/tests/core/rabin2parity.test b/tests/core/rabin2parity.test index a5fe2d6ea..09a4854f5 100644 --- a/tests/core/rabin2parity.test +++ b/tests/core/rabin2parity.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et +# Copyright (C) 2017-2018 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -39,9 +39,39 @@ State: 1 [0] 1 {1 } [!0] 1 {0 1 } --END-- +HOA: v1 +States: 1 +Start: 0 +AP: 1 "a" +acc-name: Streett 1 +Acceptance: 2 Fin(0) | Inf(1) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[t] 0 +--END-- +HOA: v1 +States: 3 +Start: 0 +AP: 1 "a" +acc-name: Streett 3 +Acceptance: 6 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)) +properties: trans-labels explicit-labels trans-acc deterministic +--BODY-- +State: 0 +[!0] 0 {1 3} +[0] 1 {} +State: 1 +[0] 2 {2} +State: 2 +[!0] 0 {0 4} +[0] 2 {} +--END-- EOF # random automata -randaut 5 -n100 -u -D --acceptance="Rabin 0..6" +randaut 4 -n100 -u -D --acceptance="Rabin 0..6" +randaut 4 -n100 -u -D --acceptance="Streett 0..6" ) | \ autcross \ "autfilt --parity" \ diff --git a/tests/python/except.py b/tests/python/except.py index 8ed74639e..be8169ba9 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -27,7 +27,7 @@ import spot try: spot.iar(spot.translate('GFa & GFb & GFc')) except RuntimeError as e: - assert 'iar() expects Rabin-like input' in str(e) + assert 'iar() expects Rabin-like or Streett-like input' in str(e) alt = spot.dualize(spot.translate('FGa | FGb'))