diff --git a/NEWS b/NEWS index a9b99e099..3d275ab71 100644 --- a/NEWS +++ b/NEWS @@ -32,6 +32,11 @@ New in spot 1.99.7a (not yet released) fail to find a deterministic automaton (even if one exists) and return a nondeterministic automaton. + * "autfilt --complement" now also works for non-deterministic + automata but will output a deterministic automaton. + "autfilt --complement --tgba" will likely output a + nondeterministic TGBA. + Library: * Building products with different dictionaries now raise an diff --git a/bin/autfilt.cc b/bin/autfilt.cc index f8c53bb5b..8fde37b84 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -562,17 +562,6 @@ namespace if (opt_complement_acc) aut->set_acceptance(aut->acc().num_sets(), aut->get_acceptance().complement()); - if (opt_complement) - { - if (!spot::is_deterministic(aut)) - { - std::cerr << filename << ':' - << haut->loc << (": --complement currently supports " - "only deterministic automata\n"); - exit(2); - } - aut = spot::dtwa_complement(aut); - } if (opt_rem_fin) aut = remove_fin(aut); if (opt_dnf_acc) @@ -658,6 +647,20 @@ namespace return 0; } + if (opt_complement) + { + if (!spot::is_deterministic(aut)) + { + // let's determinize that automaton + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(level); + aut = p.run(aut); + } + aut = spot::dtwa_complement(aut); + } + aut = post.run(aut, nullptr); if (randomize_st || randomize_tr) diff --git a/tests/core/complement.test b/tests/core/complement.test index 92f56e7c1..2c03e0604 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement de +# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -93,6 +93,25 @@ State: 3 EOF diff out expected - -$ltl2tgba -H 'FGa' | $autfilt --complement 2>out && exit 1 -grep 'deterministic' out +# The complement of a nondeterministic automaton is currently done via +# a determinization. +$ltl2tgba -H 'FGa' | $autfilt --complement >out +cat >expected <