diff --git a/bin/autfilt.cc b/bin/autfilt.cc index e5b4e5451..cff6829c6 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -304,8 +304,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 support only deterministic " - "automata)", 0 }, + "complement each automaton (currently via determinization)", 0 }, { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0, "complement the acceptance condition (without touching the automaton)", 0 }, @@ -1423,7 +1422,10 @@ namespace } if (opt_complement) - aut = spot::dualize(ensure_deterministic(aut)); + { + aut = spot::dualize(ensure_deterministic(aut)); + aut->merge_edges(); + } if (opt_dualize) aut = spot::dualize(aut); diff --git a/tests/core/complement.test b/tests/core/complement.test index 3ca643564..7d466f483 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2015-2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -50,7 +50,7 @@ EOF diff out expected -ltl2tgba -H 'GFa & GFb' Xa Fa | autfilt --complement -H >out +ltl2tgba -H 'GFa & GFb' Xa Fa 'FGa & FGb' | autfilt --complement -H >out cat >expected <