Commit c1d0cab3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc,

src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc: Provide wrapper
functions that read the hash-map size from a "bsh" option.
* src/tgbatest/randtgba.cc: Simplify.
parent fed4b6f0
2005-02-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc,
src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc: Provide wrapper
functions that read the hash-map size from a "bsh" option.
* src/tgbatest/randtgba.cc: Simplify.
* src/misc/optionmap.hh, src/misc/optionmap.cc
(option_map::parse_options): Rewrite. Do not modify the input
string, allow !foo as a shorthand for foo=0, and support K and
......
......@@ -46,14 +46,14 @@ namespace spot
/// \brief Emptiness checker on spot::tgba automata having at most one
/// accepting condition (i.e. a TBA).
template <typename heap>
class magic_search : public emptiness_check, public ec_statistics
class magic_search_ : public emptiness_check, public ec_statistics
{
public:
/// \brief Initialize the Magic Search algorithm on the automaton \a a
///
/// \pre The automaton \a a must have at most one accepting
/// condition (i.e. it is a TBA).
magic_search(const tgba *a, size_t size, option_map o = option_map())
magic_search_(const tgba *a, size_t size, option_map o = option_map())
: emptiness_check(a, o),
h(size),
all_cond(a->all_acceptance_conditions())
......@@ -61,7 +61,7 @@ namespace spot
assert(a->number_of_acceptance_conditions() <= 1);
}
virtual ~magic_search()
virtual ~magic_search_()
{
// Release all iterators on the stacks.
while (!st_blue.empty())
......@@ -318,7 +318,7 @@ namespace spot
public acss_statistics
{
public:
result_from_stack(magic_search& ms)
result_from_stack(magic_search_& ms)
: emptiness_check_result(ms.automaton()), ms_(ms)
{
}
......@@ -366,7 +366,7 @@ namespace spot
return 0;
}
private:
magic_search& ms_;
magic_search_& ms_;
};
# define FROM_STACK "ar:from_stack"
......@@ -374,13 +374,13 @@ namespace spot
class magic_search_result: public emptiness_check_result
{
public:
magic_search_result(magic_search& m, option_map o = option_map())
magic_search_result(magic_search_& m, option_map o = option_map())
: emptiness_check_result(m.automaton(), o), ms(m)
{
if (options()[FROM_STACK])
computer = new result_from_stack(ms);
else
computer = new ndfs_result<magic_search<heap>, heap>(ms);
computer = new ndfs_result<magic_search_<heap>, heap>(ms);
}
virtual void options_updated(const option_map& old)
......@@ -388,7 +388,7 @@ namespace spot
if (old[FROM_STACK] && !options()[FROM_STACK])
{
delete computer;
computer = new ndfs_result<magic_search<heap>, heap>(ms);
computer = new ndfs_result<magic_search_<heap>, heap>(ms);
}
else if (!old[FROM_STACK] && options()[FROM_STACK])
{
......@@ -414,7 +414,7 @@ namespace spot
private:
emptiness_check_result* computer;
magic_search& ms;
magic_search_& ms;
};
};
......@@ -575,13 +575,22 @@ namespace spot
emptiness_check* explicit_magic_search(const tgba *a, option_map o)
{
return new magic_search<explicit_magic_search_heap>(a, 0, o);
return new magic_search_<explicit_magic_search_heap>(a, 0, o);
}
emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size,
option_map o)
{
return new magic_search<bsh_magic_search_heap>(a, size, o);
return new magic_search_<bsh_magic_search_heap>(a, size, o);
}
emptiness_check*
magic_search(const tgba *a, option_map o)
{
size_t size = o.get("bsh");
if (size)
return bit_state_hashing_magic_search(a, size, o);
return explicit_magic_search(a, o);
}
}
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
......@@ -82,7 +82,7 @@ namespace spot
/// (which deals with accepting states) presented in
///
/// \verbatim
/// Article{ courcoubertis.92.fmsd,
/// Article{ courcoubetis.92.fmsd,
/// author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre
/// Wolper and Mihalis Yannakakis},
/// title = {Memory-Efficient Algorithm for the Verification of
......@@ -94,6 +94,8 @@ namespace spot
/// }
/// \endverbatim
///
/// \fixme The name is misleading. Magic-search is the algorithm
/// from \c godefroid.93.pstv, not \c courcoubetis.92.fmsd.
emptiness_check* explicit_magic_search(const tgba *a,
option_map o = option_map());
......@@ -127,6 +129,14 @@ namespace spot
emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size,
option_map o = option_map());
/// \brief Wrapper for the two magic_search implementations.
///
/// This wrapper calls explicit_magic_search_search() or
/// bit_state_hashing_magic_search() according to the \c "bsh" option
/// in the \c option_map. If \c "bsh" is set and non null, its value
/// is used as the size of the hash map.
emptiness_check* magic_search(const tgba *a, option_map o = option_map());
/// @}
}
......
......@@ -675,4 +675,13 @@ namespace spot
return new se05_search<bsh_se05_search_heap>(a, size, o);
}
emptiness_check*
se05(const tgba *a, option_map o)
{
size_t size = o.get("bsh");
if (size)
return bit_state_hashing_se05_search(a, size, o);
return explicit_se05_search(a, o);
}
}
......@@ -133,6 +133,15 @@ namespace spot
emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size,
option_map o = option_map());
/// \brief Wrapper for the two se05 implementations.
///
/// This wrapper calls explicit_se05_search() or
/// bit_state_hashing_se05_search() according to the \c "bsh" option
/// in the \c option_map. If \c "bsh" is set and non null, its value
/// is used as the size of the hash map.
emptiness_check* se05(const tgba *a, option_map o);
/// @}
}
......
......@@ -68,30 +68,6 @@ couvreur99_cons(const spot::tgba* a, spot::option_map o)
return spot::couvreur99(a, o);
}
spot::emptiness_check*
ms_cons(const spot::tgba* a, spot::option_map o)
{
return spot::explicit_magic_search(a, o);
}
spot::emptiness_check*
se05_cons(const spot::tgba* a, spot::option_map o)
{
return spot::explicit_se05_search(a, o);
}
spot::emptiness_check*
bsh_ms_cons(const spot::tgba* a, spot::option_map o)
{
return spot::bit_state_hashing_magic_search(a, 4096, o);
}
spot::emptiness_check*
bsh_se05_cons(const spot::tgba* a, spot::option_map o)
{
return spot::bit_state_hashing_se05_search(a, 4096, o);
}
struct ec_algo
{
const char* name;
......@@ -117,15 +93,15 @@ ec_algo ec_algos[] =
{ "Cou99_rem_shy", "poprem shy group",
couvreur99_cons, 0, -1U, true },
{ "CVWY90", 0,
ms_cons, 0, 1, true },
{ "CVWY90_bsh", 0,
bsh_ms_cons, 0, 1, false },
spot::magic_search, 0, 1, true },
{ "CVWY90_bsh", "bsh=4K",
spot::magic_search, 0, 1, false },
{ "GV04", 0,
spot::explicit_gv04_check, 0, 1, true },
{ "SE05", 0,
se05_cons, 0, 1, true },
{ "SE05_bsh", 0,
bsh_se05_cons, 0, 1, false },
spot::se05, 0, 1, true },
{ "SE05_bsh", "bsh=4K",
spot::se05, 0, 1, false },
{ "Tau03", 0,
spot::explicit_tau03_search, 1, -1U, true },
{ "Tau03_opt", 0,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment