diff --git a/NEWS b/NEWS index 1cbd800e1..23739d738 100644 --- a/NEWS +++ b/NEWS @@ -82,6 +82,9 @@ New in spot 2.10.6.dev (not yet released) averted in the parser by delaying the construction of such n-ary nodes until all children are known. + - complement() used to always turn tautological acceptance conditions + into Büchi. It now only does that if the automaton is modified. + New in spot 2.10.6 (2022-05-18) Bugs fixed: diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc index 20be2ea06..803b3f440 100644 --- a/spot/twaalgos/complete.cc +++ b/spot/twaalgos/complete.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2018, 2022 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -29,6 +29,8 @@ namespace spot return; unsigned n = aut->num_states(); + bool need_acc_fix = false; + // UM is a pair (bool, mark). If the Boolean is false, the // acceptance is always satisfiable. Otherwise, MARK is an // example of unsatisfiable mark. @@ -36,10 +38,11 @@ namespace spot if (!um.first) { // We cannot safely complete an automaton if its - // acceptance is always satisfiable. - auto acc = aut->set_buchi(); - for (auto& t: aut->edge_vector()) - t.acc = acc; + // acceptance is always satisfiable, so we will + // have to fix the acceptance automaton. However + // postpone that until we are sure that the + // automaton really need to be completed. + need_acc_fix = true; } else { @@ -129,6 +132,8 @@ namespace spot // acceptance sets as the last outgoing edge of the // state. acc = t.acc; + // If a state already has a edge to a sink, remember it + // so we can add the missing conditions to it. if (t.dst == sink) edge_to_sink = aut->edge_number(t); } @@ -136,6 +141,15 @@ namespace spot // edge to some sink state. if (missingcond != bddfalse) { + if (need_acc_fix) + { + auto a = aut->set_buchi(); + for (auto& t: aut->edge_vector()) + t.acc = a; + if (aut->num_edges()) + acc = a; + need_acc_fix = false; + } // If we haven't found any sink, simply add one. if (sink == -1U) { diff --git a/spot/twaalgos/complete.hh b/spot/twaalgos/complete.hh index 87703dcc2..3525904be 100644 --- a/spot/twaalgos/complete.hh +++ b/spot/twaalgos/complete.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2017 Laboratoire de Recherche et +// Copyright (C) 2013-2015, 2017, 2022 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -25,12 +25,13 @@ namespace spot { /// \brief Complete a twa_graph in place. /// - /// If the TωA has an acceptance condition that is a tautology, - /// it will be changed into a Büchi automaton. + /// If the TωA is incomplete and has an acceptance condition that is + /// a tautology, it will be changed into a Büchi automaton. SPOT_API void complete_here(twa_graph_ptr aut); /// \brief Clone a twa and complete it. /// - /// If the twa has no acceptance set, one will be added. + /// If the TωA is incomplete and has an acceptance condition that is + /// a tautology, it will be changed into a Büchi automaton. SPOT_API twa_graph_ptr complete(const const_twa_ptr& aut); }