diff --git a/NEWS b/NEWS index 1bf5d76e4..64409d0de 100644 --- a/NEWS +++ b/NEWS @@ -39,6 +39,10 @@ New in spot 2.7.2.dev (not yet released) helpful to display automata as "graphs", e.g., when illustrating algorithms that do not care about labels. + - A new complement() function that return automata with unspecified + acceptance condition. The output can be alternating only if the + input was alternating. + Bugs fixed: - When processing CSV files with MSDOS-style \r\n line endings, diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 6b8f658ca..042e66746 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -49,6 +49,7 @@ #include #include #include +#include #include #include #include @@ -318,7 +319,7 @@ static const argp_option options[] = { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0, "remove unused acceptance sets from the automaton", 0 }, { "complement", OPT_COMPLEMENT, nullptr, 0, - "complement each automaton (currently via determinization)", 0 }, + "complement each automaton (different strategies are used)", 0 }, { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0, "complement the acceptance condition (without touching the automaton)", 0 }, @@ -1500,7 +1501,7 @@ namespace if (opt_complement) { - aut = spot::dualize(ensure_deterministic(aut)); + aut = spot::complement(aut); aut->merge_edges(); } diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index 4a8d23c4f..3ca0a9e67 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -28,8 +28,7 @@ #include #include #include -#include -#include +#include #include #include #include @@ -172,20 +171,13 @@ namespace spot namespace { static const_twa_graph_ptr - ensure_deterministic(const const_twa_ptr& aut_in) + ensure_graph(const const_twa_ptr& aut_in) { const_twa_graph_ptr aut = std::dynamic_pointer_cast(aut_in); - if (!aut) - aut = make_twa_graph(aut_in, twa::prop_set::all()); - - if (is_deterministic(aut)) + if (aut) return aut; - postprocessor p; - p.set_type(postprocessor::Generic); - p.set_pref(postprocessor::Deterministic); - p.set_level(postprocessor::Low); - return p.run(std::const_pointer_cast(aut)); + return make_twa_graph(aut_in, twa::prop_set::all()); } } twa_run_ptr @@ -199,9 +191,9 @@ namespace spot if (auto aa = std::dynamic_pointer_cast(a)) if (is_deterministic(aa)) std::swap(a, b); - if (auto run = a->intersecting_run(dualize(ensure_deterministic(b)))) + if (auto run = a->intersecting_run(complement(ensure_graph(b)))) return run; - return b->intersecting_run(dualize(ensure_deterministic(a))); + return b->intersecting_run(complement(ensure_graph(a))); } twa_word_ptr @@ -215,9 +207,9 @@ namespace spot if (auto aa = std::dynamic_pointer_cast(a)) if (is_deterministic(aa)) std::swap(a, b); - if (auto word = a->intersecting_word(dualize(ensure_deterministic(b)))) + if (auto word = a->intersecting_word(complement(ensure_graph(b)))) return word; - return b->intersecting_word(dualize(ensure_deterministic(a))); + return b->intersecting_word(complement(ensure_graph(a))); } void diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index c61b422c7..947501250 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2015, 2017-2018 Laboratoire de Recherche et +// Copyright (C) 2013-2015, 2017-2019 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -23,6 +23,9 @@ #include #include #include +#include +#include +#include #include namespace spot @@ -506,4 +509,19 @@ namespace spot auto ncsb = ncsb_complementation(aut, show_names); return ncsb.run(); } + + twa_graph_ptr + complement(const const_twa_graph_ptr& aut) + { + if (!aut->is_existential() || is_universal(aut)) + return dualize(aut); + if (is_very_weak_automaton(aut)) + return remove_alternation(dualize(aut)); + // Determinize + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(spot::postprocessor::Low); + return dualize(p.run(std::const_pointer_cast(aut))); + } } diff --git a/spot/twaalgos/complement.hh b/spot/twaalgos/complement.hh index 55f7da10c..fef481df7 100644 --- a/spot/twaalgos/complement.hh +++ b/spot/twaalgos/complement.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2015, 2017 Laboratoire de Recherche et +// Copyright (C) 2013-2015, 2017, 2019 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -52,4 +52,26 @@ namespace spot /// S. Schewe, J. Strejček, and MH. Tsai (TACAS'16). SPOT_API twa_graph_ptr complement_semidet(const const_twa_graph_ptr& aut, bool show_names = false); + + + /// \brief Complement a TωA + /// + /// This employs different complementation strategies depending + /// on the type of the automaton. + /// + /// If the input is alternating, the output may be alternating and + /// is simply the result of calling dualize(). + /// + /// If the input is not alternating, the output will not be + /// alternating, but could have any acceptance condition. + /// - deterministic inputs are passed to dualize() + /// - very weak automata are also dualized, and then + /// passed to remove_alternation() to obtain a TGBA + /// - any other type of input is determized before + /// complementation. + /// + /// complement_semidet() is not yet used. + SPOT_API twa_graph_ptr + complement(const const_twa_graph_ptr& aut); + } diff --git a/spot/twaalgos/contains.cc b/spot/twaalgos/contains.cc index a94b3ac40..6c76249d5 100644 --- a/spot/twaalgos/contains.cc +++ b/spot/twaalgos/contains.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2018 Laboratoire de Recherche et Développement de +// Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de // l'Epita. // // This file is part of Spot, a model checking library. @@ -19,27 +19,14 @@ #include "config.h" #include -#include +#include #include #include -#include namespace spot { namespace { - static spot::const_twa_graph_ptr - ensure_deterministic(const spot::const_twa_graph_ptr& aut) - { - if (spot::is_deterministic(aut)) - return aut; - spot::postprocessor p; - p.set_type(spot::postprocessor::Generic); - p.set_pref(spot::postprocessor::Deterministic); - p.set_level(spot::postprocessor::Low); - return p.run(std::const_pointer_cast(aut)); - } - static spot::const_twa_graph_ptr translate(formula f, const bdd_dict_ptr& dict) { @@ -49,25 +36,22 @@ namespace spot bool contains(const_twa_graph_ptr left, const_twa_graph_ptr right) { - return !right->intersects(dualize(ensure_deterministic(left))); + return !complement(left)->intersects(right); } bool contains(const_twa_graph_ptr left, formula right) { - auto right_aut = translate(right, left->get_dict()); - return !right_aut->intersects(dualize(ensure_deterministic(left))); + return contains(left, translate(right, left->get_dict())); } bool contains(formula left, const_twa_graph_ptr right) { - return !right->intersects(translate(formula::Not(left), right->get_dict())); + return !translate(formula::Not(left), right->get_dict())->intersects(right); } bool contains(formula left, formula right) { - auto dict = make_bdd_dict(); - auto right_aut = translate(right, dict); - return !right_aut->intersects(translate(formula::Not(left), dict)); + return contains(left, translate(right, make_bdd_dict())); } bool are_equivalent(const_twa_graph_ptr left, const_twa_graph_ptr right) diff --git a/spot/twaalgos/powerset.cc b/spot/twaalgos/powerset.cc index d152a7111..b80d69253 100644 --- a/spot/twaalgos/powerset.cc +++ b/spot/twaalgos/powerset.cc @@ -463,12 +463,9 @@ namespace spot neg_aut = scc_filter(neg_aut, true); } - if (product(det, neg_aut)->is_empty()) - // Complement the DBA. - if (product(aut, remove_fin(dualize(det)))->is_empty()) - // Finally, we are now sure that it was safe - // to determinize the automaton. - return det; + if (!det->intersects(neg_aut) && !aut->intersects(dualize(det))) + // Determinization was safe. + return det; return aut; } diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 6f4e20574..0a58294c3 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement de +// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -28,9 +28,8 @@ #include #include #include -#include +#include #include -#include #include #include #include @@ -602,16 +601,7 @@ namespace spot bool own_nf = false; if (!aut_nf) { - twa_graph_ptr tmp = aut_f; - if (!is_deterministic(aut_f)) - { - spot::postprocessor p; - p.set_type(spot::postprocessor::Generic); - p.set_pref(spot::postprocessor::Deterministic); - p.set_level(spot::postprocessor::Low); - tmp = p.run(aut_f); - } - aut_nf = dualize(std::move(tmp)); + aut_nf = complement(aut_f); own_nf = true; } bool res = do_si_check(aut_f, own_f, @@ -709,13 +699,7 @@ namespace spot return res; if (neg == nullptr) - { - spot::postprocessor p; - p.set_type(spot::postprocessor::Generic); - p.set_pref(spot::postprocessor::Deterministic); - p.set_level(spot::postprocessor::Low); - neg = dualize(p.run(std::const_pointer_cast(pos))); - } + neg = complement(pos); auto product_states = [](const const_twa_graph_ptr& a) { @@ -782,13 +766,7 @@ namespace spot return res; if (neg == nullptr) - { - spot::postprocessor p; - p.set_type(spot::postprocessor::Generic); - p.set_pref(spot::postprocessor::Deterministic); - p.set_level(spot::postprocessor::Low); - neg = dualize(p.run(std::const_pointer_cast(pos))); - } + neg = complement(pos); auto product_states = [](const const_twa_graph_ptr& a) { diff --git a/tests/core/complement.test b/tests/core/complement.test index 7d466f483..555336d3c 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2018 Laboratoire de Recherche et Développement de +# Copyright (C) 2015-2019 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -105,17 +105,17 @@ HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" -acc-name: parity min even 2 -Acceptance: 2 Inf(0) | Fin(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[!0 | !1] 0 -[0&1] 1 {1} +[!0 | !1] 0 {0} +[0&1] 1 State: 1 [!0 | !1] 0 {0} -[0&1] 1 {1} +[0&1] 1 --END-- EOF diff out expected @@ -128,17 +128,17 @@ HOA: v1 States: 2 Start: 0 AP: 1 "a" -acc-name: parity min even 2 -Acceptance: 2 Inf(0) | Fin(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[!0] 0 -[0] 1 {1} +[!0] 0 {0} +[0] 1 State: 1 [!0] 0 {0} -[0] 1 {1} +[0] 1 --END-- EOF diff out expected