From 1b81ecb80ce62781c7c9bccd7968e4470f45e418 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Mar 2024 17:53:23 +0100 Subject: [PATCH] dualize: should not call cleanup_acceptance_here MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Based on a report by Emmanuel Filiot, who was surprized that dualizing Büchi did not always produce co-Büchi. * spot/twaalgos/dualize.cc: Remove the call to cleanup_acceptance_here. * spot/twaalgos/dualize.hh: Improve documentation. * NEWS: Mention the possible backward incompatible change. * tests/core/dualize.test, tests/python/dualize.py, tests/python/pdegen.py: Adjust test cases. * spot/twaalgos/complement.cc (complement): Call cleanup_acceptance_here when dualize() returns a smaller automaton. * THANKS: Add Emmanuel. --- NEWS | 7 ++++++ THANKS | 1 + spot/twaalgos/complement.cc | 15 ++++++++++++- spot/twaalgos/dualize.cc | 4 +--- spot/twaalgos/dualize.hh | 45 +++++++++++++++++++++++++++++-------- tests/core/dualize.test | 9 +++----- tests/python/dualize.py | 7 +++--- tests/python/pdegen.py | 2 ++ 8 files changed, 67 insertions(+), 23 deletions(-) diff --git a/NEWS b/NEWS index 81a5272a7..694d5bf6f 100644 --- a/NEWS +++ b/NEWS @@ -148,6 +148,13 @@ New in spot 2.11.6.dev (not yet released) should raise an exception of return nullptr if it requires more acceptance sets than supported. + - [Potential backward incompatibility] spot::dualize() does not call + cleanup_acceptance() anymore. This change ensures that the dual + of a Büchi automaton will always be a co-Büchi automaton. + Previously cleanup_acceptance(), which remove unused colors from + the acceptance, was sometimes able to simplify co-Büchi to "t", + causing surprizes. + Python: - The spot.automata() and spot.automaton() functions now accept a diff --git a/THANKS b/THANKS index cf923eaec..307d34999 100644 --- a/THANKS +++ b/THANKS @@ -15,6 +15,7 @@ David Dokoupil David Müller Dávid Smolka Edmond Irani Liu +Emmanuel Filiot Ernesto Posse Étienne Renault Fabrice Kordon diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 7e38e519a..00e9cb0ce 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -25,6 +25,7 @@ #include #include #include +#include namespace spot { @@ -510,7 +511,19 @@ namespace spot complement(const const_twa_graph_ptr& aut, const output_aborter* aborter) { if (!aut->is_existential() || is_universal(aut)) - return dualize(aut); + { + twa_graph_ptr res = dualize(aut); + // There are cases with "t" acceptance that get converted to + // Büchi during completion, then dualized to co-Büchi, but the + // acceptance is still not used. To try to clean it up in this + // case. + if (aut->num_sets() == 0 || + // Also dualize removes sink states, but doesn't simplify + // the acceptance condition. + res->num_states() < aut->num_states()) + cleanup_acceptance_here(res); + return res; + } if (is_very_weak_automaton(aut)) // removing alternation may need more acceptance sets than we support. // in this case res==nullptr and we try the other determinization. diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc index 4e2261e12..fc60d78af 100644 --- a/spot/twaalgos/dualize.cc +++ b/spot/twaalgos/dualize.cc @@ -308,7 +308,7 @@ namespace spot } if (is_deterministic(aut_)) { - res = cleanup_acceptance_here(spot::complete(aut_)); + res = spot::complete(aut_); res->set_acceptance(res->num_sets(), res->get_acceptance().complement()); // Complementing the acceptance is likely to break the terminal @@ -368,8 +368,6 @@ namespace spot res->prop_terminal(trival::maybe()); if (!has_sink) res->prop_complete(true); - - cleanup_acceptance_here(res); return res; } }; diff --git a/spot/twaalgos/dualize.hh b/spot/twaalgos/dualize.hh index d84be8173..4d79df66b 100644 --- a/spot/twaalgos/dualize.hh +++ b/spot/twaalgos/dualize.hh @@ -26,23 +26,50 @@ namespace spot /// \ingroup twa_misc /// \brief Complement an automaton by dualizing it. /// - /// Given an automaton \a aut of any type, produces the dual as output. The - /// automaton will be completed if it isn't already. If it is deterministic - /// and complete, complementing the automaton can be done by just - /// complementing the acceptance condition. + /// Given an automaton \a aut of any type, produces the dual as + /// output. Before dualization, the automaton will be completed if + /// it isn't already, but any sink state in the output might then be + /// removed. /// - /// In particular, this implies that an input that use generalized Büchi will - /// be output as generalized co-Büchi. + /// Dualizing the automaton is done by interpreting the outgoing + /// transitions of a state as a Boolean function, and then swapping + /// operators ∧ and ̇∨. This first step does not have to be done on + /// deterministic automata. Additionally, the acceptance condition + /// is dualized by swapping operators ∧ and ̇∨, and swapping Inf and + /// Fin. /// - /// Functions like to_generalized_buchi() or remove_fin() are frequently - /// called on existential automata after dualize() to obtain an easier - /// acceptance condition, but maybe at the cost of losing determinism. + /// For instance, the dual of a generalized Büchi automaton will be + /// a generalized co-Büchi automaton. + /// + /// If the input acceptance condition accepts every infinite path + /// (such as "t" or "Inf(0)|Fin(0)") and the automaton is not + /// complete, then the input automaton will be assumed to have Büchi + /// acceptance in order to complete it, and the output will then + /// have co-Büchi acceptance. + /// + /// Due to a defect in the way transition-based alternating automata + /// are represented in Spot and in the HOA format, existential + /// automata with transition-based acceptance will be converted to + /// use state-based acceptance before dualization. See + /// https://github.com/adl/hoaf/issues/68 for more information. /// /// If the input automaton is deterministic, the output will be deterministic. /// If the input automaton is existential, the output will be universal. /// If the input automaton is universal, the output will be existential. /// Finally, if the input automaton is alternating, the result is alternating. /// More can be found on page 22 (Definition 1.6) of \cite loding.98.msc . + /// + /// Functions like to_generalized_buchi() or remove_fin() are frequently + /// called on existential automata after dualize() to obtain an easier + /// acceptance condition, but maybe at the cost of losing determinism. + /// + /// Up to version 2.11.6, this function used to call + /// cleanup_acceptance_here() to simplify the acceptance condition + /// after dualization. This caused some surprizes, users expected + /// the dual of a Büchi automaton to be a co-Büchi automaton, but + /// cleanup_acceptance_here() sometimes reduced the condition to `t` + /// when all states where accepting. This function is not called + /// anymore since version 2.12. SPOT_API twa_graph_ptr dualize(const const_twa_graph_ptr& aut); } diff --git a/tests/core/dualize.test b/tests/core/dualize.test index c0ba567d4..a1b443d58 100755 --- a/tests/core/dualize.test +++ b/tests/core/dualize.test @@ -49,8 +49,7 @@ HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" -acc-name: all -Acceptance: 0 t +Acceptance: 3 (Fin(0)|Fin(1)) | Inf(2) properties: trans-labels explicit-labels trans-acc complete properties: deterministic --BODY-- @@ -114,8 +113,7 @@ HOA: v1 States: 9 Start: 8 AP: 2 "p0" "p1" -acc-name: co-Buchi -Acceptance: 1 Fin(0) +Acceptance: 2 Fin(0) & Fin(1) properties: trans-labels explicit-labels state-acc univ-branch --BODY-- State: 0 @@ -148,8 +146,7 @@ HOA: v1 States: 9 Start: 8 AP: 2 "p0" "p1" -acc-name: co-Buchi -Acceptance: 1 Fin(0) +Acceptance: 2 Fin(0) & Fin(1) properties: trans-labels explicit-labels state-acc univ-branch Alias: @a 0&!1 Alias: @b !0&!1 diff --git a/tests/python/dualize.py b/tests/python/dualize.py index bfeb20b38..dd06be362 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -191,8 +191,8 @@ tc.assertEqual(h, """HOA: v1 States: 2 Start: 1 AP: 2 "a" "b" -acc-name: all -Acceptance: 0 t +acc-name: co-Buchi +Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 @@ -227,8 +227,7 @@ tc.assertEqual(h, """HOA: v1 States: 2 Start: 1 AP: 2 "a" "b" -acc-name: all -Acceptance: 0 t +Acceptance: 2 Fin(0) & Fin(1) properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py index 1e886f280..4f5796ff9 100644 --- a/tests/python/pdegen.py +++ b/tests/python/pdegen.py @@ -115,6 +115,8 @@ tc.assertEqual(dd.num_states(), 1) tc.assertEqual(str(dd.get_acceptance()), 'Inf(1) & Fin(0)') e = spot.dualize(b) +spot.cleanup_acceptance_here(e) +tc.assertEqual(str(e.get_acceptance()), 'Fin(0)|Fin(1)') de = spot.partial_degeneralize(e, [0, 1]) tc.assertTrue(de.equivalent_to(e)) tc.assertEqual(de.num_states(), 4)