diff --git a/NEWS b/NEWS index 12861d97e..f2de77c6f 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,9 @@ New in spot 2.2.1.dev (Not yet released) automata than the former one. The old version has been kept for compatibility. + * The new version of the Couvreur emptiness check is now the default + one, used by is_empty() and accepting_run(). + Build: * If the system has an installed libltdl library, use it instead of diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index ffcd7e869..abdf5ed01 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -1,7 +1,7 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014, 2015, 2016 Laboratoire de Recherche et -// Developpement de l'EPITA (LRDE). -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2011, 2014-2016 Laboratoire de Recherche et Developpement de +// l'EPITA (LRDE). +// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -22,7 +22,7 @@ #include #include -#include +#include #include #include #include @@ -71,10 +71,7 @@ namespace spot bool twa::is_empty() const { - // FIXME: This should be improved based on properties of the - // automaton. For instance we do not need couvreur99 is we know - // the automaton is weak. - return !couvreur99(remove_fin_maybe(shared_from_this()))->check(); + return !couvreur99_new_check(remove_fin_maybe(shared_from_this())); } twa_run_ptr @@ -84,7 +81,7 @@ namespace spot throw std::runtime_error("twa::accepting_run() does not work with " "Fin acceptance (but twa:is_empty() and " "twa::accepting_run() can)"); - auto res = couvreur99(shared_from_this())->check(); + auto res = couvreur99_new_check(shared_from_this()); if (!res) return nullptr; return res->accepting_run();