* src/tgbaalgos/colordfs.hh, src/tgbaalgos/minimalce.cc,
src/tgbaalgos/minimalce.hh, src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/tarjan_on_fly.hh, src/tgbatest/ltl2tgba.cc: Rename emptyness_search to emptiness_search.
This commit is contained in:
parent
c30823f7be
commit
a59b9aa7f4
7 changed files with 18 additions and 13 deletions
|
|
@ -1,5 +1,10 @@
|
||||||
2004-09-21 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
2004-09-21 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||||
|
|
||||||
|
* src/tgbaalgos/colordfs.hh, src/tgbaalgos/minimalce.cc,
|
||||||
|
src/tgbaalgos/minimalce.hh, src/tgbaalgos/nesteddfs.hh,
|
||||||
|
src/tgbaalgos/tarjan_on_fly.hh, src/tgbatest/ltl2tgba.cc: Rename
|
||||||
|
emptyness_search to emptiness_search.
|
||||||
|
|
||||||
* src/sanity/style.test: Warn about places where size() is used
|
* src/sanity/style.test: Warn about places where size() is used
|
||||||
instead of empty().
|
instead of empty().
|
||||||
* src/misc/bddalloc.cc (bdd_allocator::extend): Use empty() rather
|
* src/misc/bddalloc.cc (bdd_allocator::extend): Use empty() rather
|
||||||
|
|
|
||||||
|
|
@ -31,7 +31,7 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
class colordfs_search: public emptyness_search
|
class colordfs_search: public emptiness_search
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
/// Initialize the Colordfs Search algorithm on the automaton \a a.
|
/// Initialize the Colordfs Search algorithm on the automaton \a a.
|
||||||
|
|
|
||||||
|
|
@ -191,12 +191,12 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
/////////////////////////////////////////////////////////////////////////////
|
/////////////////////////////////////////////////////////////////////////////
|
||||||
// The base interface for build a emptyness search algorithm
|
// The base interface for build a emptiness search algorithm
|
||||||
emptyness_search::emptyness_search()
|
emptiness_search::emptiness_search()
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
emptyness_search::~emptyness_search()
|
emptiness_search::~emptiness_search()
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -215,7 +215,7 @@ namespace spot
|
||||||
*/
|
*/
|
||||||
|
|
||||||
std::ostream&
|
std::ostream&
|
||||||
emptyness_search::print_stat(std::ostream& os) const
|
emptiness_search::print_stat(std::ostream& os) const
|
||||||
{
|
{
|
||||||
return os;
|
return os;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -77,14 +77,14 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
/////////////////////////////////////////////////////////////////////////////
|
/////////////////////////////////////////////////////////////////////////////
|
||||||
// The base interface for build a emptyness search algorithm
|
// The base interface to build an emptiness check algorithm
|
||||||
class emptyness_search
|
class emptiness_search
|
||||||
{
|
{
|
||||||
protected:
|
protected:
|
||||||
emptyness_search();
|
emptiness_search();
|
||||||
|
|
||||||
public:
|
public:
|
||||||
virtual ~emptyness_search();
|
virtual ~emptiness_search();
|
||||||
virtual ce::counter_example* check() = 0;
|
virtual ce::counter_example* check() = 0;
|
||||||
/// \brief Print Stat.
|
/// \brief Print Stat.
|
||||||
virtual std::ostream& print_stat(std::ostream& os) const;
|
virtual std::ostream& print_stat(std::ostream& os) const;
|
||||||
|
|
@ -93,7 +93,7 @@ namespace spot
|
||||||
/////////////////////////////////////////////////////////////////////////////
|
/////////////////////////////////////////////////////////////////////////////
|
||||||
// Perform a minimal search
|
// Perform a minimal search
|
||||||
|
|
||||||
class minimalce_search: public emptyness_search
|
class minimalce_search: public emptiness_search
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
//minimalce_search(const tgba_tba_proxy *a, bool mode = false);
|
//minimalce_search(const tgba_tba_proxy *a, bool mode = false);
|
||||||
|
|
|
||||||
|
|
@ -41,7 +41,7 @@ namespace spot
|
||||||
};
|
};
|
||||||
*/
|
*/
|
||||||
|
|
||||||
class nesteddfs_search: public emptyness_search
|
class nesteddfs_search: public emptiness_search
|
||||||
{
|
{
|
||||||
|
|
||||||
public:
|
public:
|
||||||
|
|
|
||||||
|
|
@ -33,7 +33,7 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
|
||||||
class tarjan_on_fly: public emptyness_search
|
class tarjan_on_fly: public emptiness_search
|
||||||
{
|
{
|
||||||
|
|
||||||
public:
|
public:
|
||||||
|
|
|
||||||
|
|
@ -180,7 +180,7 @@ main(int argc, char** argv)
|
||||||
NestedDFSSearch, NestedDFSSearchModify, ColorDFSSearch,
|
NestedDFSSearch, NestedDFSSearchModify, ColorDFSSearch,
|
||||||
TarjanOnFly, MinimalSearch, MinimalSearchIterative,
|
TarjanOnFly, MinimalSearch, MinimalSearchIterative,
|
||||||
NestedGeneSearch} echeck = None;
|
NestedGeneSearch} echeck = None;
|
||||||
spot::emptyness_search* es = 0;
|
spot::emptiness_search* es = 0;
|
||||||
spot::search_opt opt_nested_search = spot::magic;
|
spot::search_opt opt_nested_search = spot::magic;
|
||||||
enum { NoneDup, BFS, DFS } dupexp = NoneDup;
|
enum { NoneDup, BFS, DFS } dupexp = NoneDup;
|
||||||
bool magic_many = false;
|
bool magic_many = false;
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue