alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Default emptiness check is the new version of Couvreur.

Browse source 
* spot/twa/twa.cc: is_empty() and accepting_run() now call the new
version of the Couvreur algorithm.
This commit is contained in:
Maximilien Colange 2016-11-25 13:42:47 +01:00
parent 1a08eca840
commit 114f7f1200
2 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -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 automata than the former one. The old version has been kept for
compatibility. compatibility.
* The new version of the Couvreur emptiness check is now the default
one, used by is_empty() and accepting_run().
Build: Build:
* If the system has an installed libltdl library, use it instead of * If the system has an installed libltdl library, use it instead of

15
spot/twa/twa.cc
View file

@ -1,7 +1,7 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2014, 2015, 2016 Laboratoire de Recherche et // Copyright (C) 2011, 2014-2016 Laboratoire de Recherche et Developpement de
// Developpement de l'EPITA (LRDE). // l'EPITA (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -22,7 +22,7 @@
#include <spot/twa/twa.hh> #include <spot/twa/twa.hh>
#include <spot/twa/twagraph.hh> #include <spot/twa/twagraph.hh>
#include <spot/twaalgos/gtec/gtec.hh> #include <spot/twaalgos/couvreurnew.hh>
#include <spot/twaalgos/word.hh> #include <spot/twaalgos/word.hh>
#include <spot/twaalgos/remfin.hh> #include <spot/twaalgos/remfin.hh>
#include <spot/twa/twaproduct.hh> #include <spot/twa/twaproduct.hh>
@ -71,10 +71,7 @@ namespace spot
bool bool
twa::is_empty() const twa::is_empty() const
{ {
// FIXME: This should be improved based on properties of the return !couvreur99_new_check(remove_fin_maybe(shared_from_this()));
// automaton. For instance we do not need couvreur99 is we know
// the automaton is weak.
return !couvreur99(remove_fin_maybe(shared_from_this()))->check();
} }
twa_run_ptr twa_run_ptr
@ -84,7 +81,7 @@ namespace spot
throw std::runtime_error("twa::accepting_run() does not work with " throw std::runtime_error("twa::accepting_run() does not work with "
"Fin acceptance (but twa:is_empty() and " "Fin acceptance (but twa:is_empty() and "
"twa::accepting_run() can)"); "twa::accepting_run() can)");
auto res = couvreur99(shared_from_this())->check(); auto res = couvreur99_new_check(shared_from_this());
if (!res) if (!res)
return nullptr; return nullptr;
return res->accepting_run(); return res->accepting_run();