* src/tgbaalgos/ndfs_result.hxx (ndfs_result, acss_interface):
Conditionally inherit from acss_statistics. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Define Has_Size in all heaps.
This commit is contained in:
parent
603b49e216
commit
7c07f3149f
6 changed files with 42 additions and 19 deletions
|
|
@ -1,3 +1,10 @@
|
||||||
|
2005-01-07 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||||
|
|
||||||
|
* src/tgbaalgos/ndfs_result.hxx (ndfs_result, acss_interface):
|
||||||
|
Conditionally inherit from acss_statistics.
|
||||||
|
* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc,
|
||||||
|
src/tgbaalgos/tau03opt.cc: Define Has_Size in all heaps.
|
||||||
|
|
||||||
2005-01-06 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr>
|
2005-01-06 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr>
|
||||||
|
|
||||||
* src/ltltest/randltl.cc: Include cassert.
|
* src/ltltest/randltl.cc: Include cassert.
|
||||||
|
|
|
||||||
|
|
@ -387,6 +387,7 @@ namespace spot
|
||||||
return (it != h.end());
|
return (it != h.end());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
enum { Has_Size = 1 };
|
||||||
int size() const
|
int size() const
|
||||||
{
|
{
|
||||||
return h.size();
|
return h.size();
|
||||||
|
|
@ -461,12 +462,7 @@ namespace spot
|
||||||
return color((h[ha%size_] >> ((ha%4)*2)) & 3U) != WHITE;
|
return color((h[ha%size_] >> ((ha%4)*2)) & 3U) != WHITE;
|
||||||
}
|
}
|
||||||
|
|
||||||
int size() const
|
enum { Has_Size = 0 };
|
||||||
{
|
|
||||||
// this method must return the number of state stored in the heap. Due
|
|
||||||
// to potential conflicts this size cannot be computed.
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
private:
|
||||||
size_t size_;
|
size_t size_;
|
||||||
|
|
|
||||||
|
|
@ -61,11 +61,37 @@ namespace spot
|
||||||
|
|
||||||
typedef std::list<stack_item> stack_type;
|
typedef std::list<stack_item> stack_type;
|
||||||
|
|
||||||
|
namespace
|
||||||
|
{
|
||||||
|
// The acss_statistics is available only when the heap has a
|
||||||
|
// size() method (which we indicate using n==1).
|
||||||
|
|
||||||
|
template <typename T, int n>
|
||||||
|
struct acss_interface
|
||||||
|
{
|
||||||
|
};
|
||||||
|
|
||||||
|
template <typename T>
|
||||||
|
struct acss_interface<T, 1>
|
||||||
|
: public acss_statistics
|
||||||
|
{
|
||||||
|
int
|
||||||
|
acss_states() const
|
||||||
|
{
|
||||||
|
// all visited states are in the state space search
|
||||||
|
return dynamic_cast<const T*>(this)->h_.size();
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
template <typename ndfs_search, typename heap>
|
template <typename ndfs_search, typename heap>
|
||||||
class ndfs_result:
|
class ndfs_result:
|
||||||
public emptiness_check_result,
|
public emptiness_check_result,
|
||||||
public ars_statistics,
|
public ars_statistics,
|
||||||
public acss_statistics
|
// Conditionally inherit from acss_statistics.
|
||||||
|
public acss_interface<ndfs_result<ndfs_search, heap>, heap::Has_Size>
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
ndfs_result(const ndfs_search& ms)
|
ndfs_result(const ndfs_search& ms)
|
||||||
|
|
@ -74,12 +100,6 @@ namespace spot
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
int acss_states() const
|
|
||||||
{
|
|
||||||
// all visited states are in the state space search
|
|
||||||
return h_.size();
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual ~ndfs_result()
|
virtual ~ndfs_result()
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
@ -195,6 +215,8 @@ namespace spot
|
||||||
private:
|
private:
|
||||||
const ndfs_search& ms_;
|
const ndfs_search& ms_;
|
||||||
const heap& h_;
|
const heap& h_;
|
||||||
|
template <typename T, int n>
|
||||||
|
friend struct acss_interface;
|
||||||
|
|
||||||
struct transition {
|
struct transition {
|
||||||
const state* source;
|
const state* source;
|
||||||
|
|
|
||||||
|
|
@ -445,6 +445,7 @@ namespace spot
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
enum { Has_Size = 1 };
|
||||||
int size() const
|
int size() const
|
||||||
{
|
{
|
||||||
return h.size() + hc.size();
|
return h.size() + hc.size();
|
||||||
|
|
@ -548,12 +549,7 @@ namespace spot
|
||||||
return color((h[ha%size_] >> ((ha%4)*2)) & 3U) != WHITE;
|
return color((h[ha%size_] >> ((ha%4)*2)) & 3U) != WHITE;
|
||||||
}
|
}
|
||||||
|
|
||||||
int size() const
|
enum { Has_Size = 0 };
|
||||||
{
|
|
||||||
// this method must return the number of state stored in the heap. Due
|
|
||||||
// to potential conflicts this size cannot be computed.
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
private:
|
||||||
size_t size_;
|
size_t size_;
|
||||||
|
|
|
||||||
|
|
@ -361,6 +361,7 @@ namespace spot
|
||||||
return (it != h.end());
|
return (it != h.end());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
enum { Has_Size = 1 };
|
||||||
int size() const
|
int size() const
|
||||||
{
|
{
|
||||||
return h.size();
|
return h.size();
|
||||||
|
|
|
||||||
|
|
@ -481,6 +481,7 @@ namespace spot
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
enum { Has_Size = 1 };
|
||||||
int size() const
|
int size() const
|
||||||
{
|
{
|
||||||
return h.size() + hc.size();
|
return h.size() + hc.size();
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue