diff --git a/NEWS b/NEWS index 3e4431873..ff80769f1 100644 --- a/NEWS +++ b/NEWS @@ -79,6 +79,12 @@ New in spot 2.8.5.dev (not yet released) should be on each transition; propagate_marks_here() actually modifies the automaton. + - rabin_to_buchi_if_realizable() is a new variant of + rabin_to_buchi_maybe() that converts a Rabin-like automaton into a + Büchi automaton only if the resulting Büchi automaton can keep the + same transition structure (where the ..._maybe() variant would + modify the Rabin automaton if needed). + Bugs fixed: - degeneralize_tba() was incorrectly not honnoring the "skip_level" diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 54d72e4c0..5bfe0d0a0 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -791,6 +791,37 @@ namespace spot return true; } + twa_graph_ptr + rabin_to_buchi_if_realizable(const const_twa_graph_ptr& aut) + { + std::vector pairs; + if (!aut->acc().is_rabin_like(pairs)) + return nullptr; + + auto aut_pairs = rs_pairs_view(pairs); + auto code = aut->get_acceptance(); + if (code.is_t()) + return nullptr; + + scc_info si(aut, scc_info_options::TRACK_STATES); + std::vector final(aut->edge_vector().size(), false); + std::vector keep(aut->edge_vector().size(), true); + + for (unsigned scc = 0; scc < si.scc_count(); ++scc) + if (!is_scc_tba_type(aut, si, scc, keep, aut_pairs, final)) + return nullptr; + + auto res = make_twa_graph(aut, twa::prop_set::all()); + auto m = res->set_buchi(); + + auto& ev = res->edge_vector(); + unsigned edgecount = ev.size(); + for (unsigned eidx = 1; eidx < edgecount; ++eidx) + ev[eidx].acc = final[eidx] ? m : acc_cond::mark_t{}; + + return res; + } + twa_graph_ptr rabin_to_buchi_maybe(const const_twa_graph_ptr& aut) { diff --git a/spot/twaalgos/remfin.hh b/spot/twaalgos/remfin.hh index 5f234efdb..5b71e5f29 100644 --- a/spot/twaalgos/remfin.hh +++ b/spot/twaalgos/remfin.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et +// Copyright (C) 2015, 2017, 2018, 2020 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -24,15 +24,37 @@ namespace spot { /// \ingroup twa_acc_transform - /// \brief Check if \aut is Büchi-realizable. This is inspired - /// from rabin_to_buchi_maybe()'s algorithm. The main difference is that - /// here, no automaton is built. + /// \brief Check if \a aut is Rablin-like and Büchi-realizable. + /// + /// This is inspired from rabin_to_buchi_maybe()'s algorithm. The + /// main difference is that here, no automaton is built. + /// + /// If the input is non-deterministic, this algorithm may fail + /// to detect Büchi-realizability (false-negative). SPOT_API bool rabin_is_buchi_realizable(const const_twa_graph_ptr& aut); /// \ingroup twa_acc_transform - /// \brief Convert a Rabin automaton to Büchi automaton, preserving - /// determinism when possible. + /// \brief Convert a Rabin-like automaton into a Büchi automaton only + /// when it can be done without changing the automaton structure. + /// + /// If \a aut is a Rabin-like automaton that is not Büchi-realizable, + /// this returns a Büchi automaton equivalent to \a aut that use + /// exactly the same transition structure (the order of edges is + /// even preserved). In particular, determinism is preserved. + /// + /// If \a aut is not a Rabin-like automaton or is not + /// Büchi-realizable, return `nullptr`. + /// + /// If the input is non-deterministic, this algorithm may fail + /// to detect Büchi-realizability (false-negative). + SPOT_API twa_graph_ptr + rabin_to_buchi_if_realizable(const const_twa_graph_ptr& aut); + + /// \ingroup twa_acc_transform + /// + /// \brief Convert a Rabin-like automaton into a Büchi automaton, + /// preserving determinism when possible. /// /// Return nullptr if the input is not a Rabin (or Rabin-like) /// automaton. @@ -43,7 +65,8 @@ namespace spot /// /// Unless you know what you are doing, you are probably better off /// calling remove_fin() instead, as this will call more specialized - /// algorithms (e.g., for weak automata) when appropriate. + /// algorithms (e.g., for weak automata) when appropriate, and will + /// deal with more than just Rabin-like automata. SPOT_API twa_graph_ptr rabin_to_buchi_maybe(const const_twa_graph_ptr& aut); diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py index a7c09a5d7..e96a4a5fc 100644 --- a/tests/python/tra2tba.py +++ b/tests/python/tra2tba.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement +# Copyright (C) 2016-2018, 2020 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -482,10 +482,31 @@ State: 1 [0] 1 {0} --END--""" - res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) +# Different order for rabin_to_buchi_if_realizable() due to merge_edges() not +# being called. This is on purpose: the edge order should match exactly the +# original automaton. +exp2 = """HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p2" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 1 +[!0] 0 {0} +State: 1 +[0] 1 {0} +[!0] 0 {0} +--END--""" +res = spot.rabin_to_buchi_if_realizable(aut) +assert(res.to_str('hoa') == exp2) + # Test 12. aut = spot.automaton(""" HOA: v1 @@ -574,6 +595,32 @@ State: 1 res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) +# rabin_to_buchi_if_realizable() does not call merge_edges() on purpose: the +# edge order should match exactly the original automaton. +exp2 = """HOA: v1 +States: 2 +Start: 0 +AP: 2 "p3" "p2" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[0&1] 1 +[0&!1] 0 {0} +[!0&1] 1 +[!0&!1] 0 {0} +State: 1 +[0&1] 1 {0} +[0&!1] 0 {0} +[!0&1] 1 {0} +[!0&!1] 0 {0} +--END--""" + +res = spot.rabin_to_buchi_if_realizable(aut) +assert(res.to_str('hoa') == exp2) + # Test 14. aut = spot.automaton(""" HOA: v1 @@ -608,3 +655,4 @@ State: 1 res = spot.remove_fin(aut) assert(res.to_str('hoa') == exp) +assert spot.rabin_to_buchi_if_realizable(aut) is None