* src/tgbaalgos/emptiness.hh,
src/tgbaalgos/emptiness.cc (emptiness_check::safe): New method. * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc: Implement it. * src/tgbatest/randtgba.cc: Simplify.
This commit is contained in:
Alexandre Duret-Lutz
parent
c1d0cab3af
commit
435b03c2b2
6 changed files with 115 additions and 69 deletions
|
|
@ -1,5 +1,11 @@
|
|||
2005-02-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
* src/tgbaalgos/emptiness.hh,
|
||||
src/tgbaalgos/emptiness.cc (emptiness_check::safe): New method.
|
||||
* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
|
||||
src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc: Implement it.
|
||||
* src/tgbatest/randtgba.cc: Simplify.
|
||||
|
||||
* 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.
|
||||
|
|
|
|||
|
|
@ -51,9 +51,10 @@ namespace spot
|
|||
}
|
||||
}
|
||||
|
||||
std::ostream& print_tgba_run(std::ostream& os,
|
||||
const tgba* a,
|
||||
const tgba_run* run)
|
||||
std::ostream&
|
||||
print_tgba_run(std::ostream& os,
|
||||
const tgba* a,
|
||||
const tgba_run* run)
|
||||
{
|
||||
bdd_dict* d = a->get_dict();
|
||||
os << "Prefix:" << std::endl;
|
||||
|
|
@ -105,6 +106,21 @@ namespace spot
|
|||
return dynamic_cast<const unsigned_statistics*>(this);
|
||||
}
|
||||
|
||||
const char*
|
||||
emptiness_check_result::parse_options(char* options)
|
||||
{
|
||||
option_map old(o_);
|
||||
const char* s = o_.parse_options(options);
|
||||
options_updated(old);
|
||||
return s;
|
||||
}
|
||||
|
||||
void
|
||||
emptiness_check_result::options_updated(const option_map&)
|
||||
{
|
||||
}
|
||||
|
||||
|
||||
emptiness_check::~emptiness_check()
|
||||
{
|
||||
}
|
||||
|
|
@ -115,6 +131,26 @@ namespace spot
|
|||
return dynamic_cast<const unsigned_statistics*>(this);
|
||||
}
|
||||
|
||||
const char*
|
||||
emptiness_check::parse_options(char* options)
|
||||
{
|
||||
option_map old(o_);
|
||||
const char* s = o_.parse_options(options);
|
||||
options_updated(old);
|
||||
return s;
|
||||
}
|
||||
|
||||
void
|
||||
emptiness_check::options_updated(const option_map&)
|
||||
{
|
||||
}
|
||||
|
||||
bool
|
||||
emptiness_check::safe() const
|
||||
{
|
||||
return true;
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
emptiness_check::print_stats(std::ostream& os) const
|
||||
{
|
||||
|
|
@ -131,7 +167,8 @@ namespace spot
|
|||
}
|
||||
}
|
||||
|
||||
tgba* tgba_run_to_tgba(const tgba* a, const tgba_run* run)
|
||||
tgba*
|
||||
tgba_run_to_tgba(const tgba* a, const tgba_run* run)
|
||||
{
|
||||
tgba_explicit* res = new tgba_explicit(a->get_dict());
|
||||
res->copy_acceptance_conditions_of(a);
|
||||
|
|
|
|||
|
|
@ -114,29 +114,18 @@ namespace spot
|
|||
return o_;
|
||||
}
|
||||
|
||||
/// Modify the options parametrizing how the accepting run is computed.
|
||||
const char*
|
||||
parse_options(char* options)
|
||||
{
|
||||
option_map old(o_);
|
||||
const char* s = o_.parse_options(options);
|
||||
options_updated(old);
|
||||
return s;
|
||||
}
|
||||
/// Modify the algorithm options.
|
||||
const char* parse_options(char* options);
|
||||
|
||||
/// Return statistics, if available.
|
||||
virtual const unsigned_statistics* statistics() const;
|
||||
|
||||
protected:
|
||||
/// React when options are modified.
|
||||
virtual void
|
||||
options_updated(const option_map& old)
|
||||
{
|
||||
(void)old;
|
||||
}
|
||||
/// Notify option updates.
|
||||
virtual void options_updated(const option_map& old);
|
||||
|
||||
const tgba* a_; ///< The automaton.
|
||||
option_map o_; ///< The options
|
||||
option_map o_; ///< The options.
|
||||
};
|
||||
|
||||
/// Common interface to emptiness check algorithms.
|
||||
|
|
@ -163,19 +152,15 @@ namespace spot
|
|||
return o_;
|
||||
}
|
||||
|
||||
/// Modify the options parametrizing how the accepting run is realized.
|
||||
const char*
|
||||
parse_options(char* options)
|
||||
{
|
||||
option_map old(o_);
|
||||
const char* s = o_.parse_options(options);
|
||||
options_updated(old);
|
||||
return s;
|
||||
}
|
||||
/// Modify the algorithm options.
|
||||
const char* parse_options(char* options);
|
||||
|
||||
/// Return false iff accepting_run() can return 0 for non-empty automata.
|
||||
virtual bool safe() const;
|
||||
|
||||
/// \brief Check whether the automaton contain an accepting run.
|
||||
///
|
||||
/// Return 0 if the automaton accept no run. Return an instance
|
||||
/// Return 0 if the automaton accepts no run. Return an instance
|
||||
/// of emptiness_check_result otherwise. This instance might
|
||||
/// allow to obtain one sample acceptance run. The result has to
|
||||
/// be destroyed before the emptiness_check instance that
|
||||
|
|
@ -183,6 +168,10 @@ namespace spot
|
|||
///
|
||||
/// Some emptiness_check algorithms may allow check() to be called
|
||||
/// several time, but generally you should not assume that.
|
||||
///
|
||||
/// Some emptiness_check algorithms, especially those using bit state
|
||||
/// hashing may return 0 even if the automaton is not empty.
|
||||
/// \see safe()
|
||||
virtual emptiness_check_result* check() = 0;
|
||||
|
||||
/// Return statistics, if available.
|
||||
|
|
@ -191,11 +180,8 @@ namespace spot
|
|||
/// Print statistics, if any.
|
||||
virtual std::ostream& print_stats(std::ostream& os) const;
|
||||
|
||||
/// React when options are modified.
|
||||
virtual void options_updated(const option_map& old)
|
||||
{
|
||||
(void)old;
|
||||
}
|
||||
/// Notify option updates.
|
||||
virtual void options_updated(const option_map& old);
|
||||
|
||||
protected:
|
||||
const tgba* a_; ///< The automaton.
|
||||
|
|
|
|||
|
|
@ -125,20 +125,25 @@ namespace spot
|
|||
return os;
|
||||
}
|
||||
|
||||
virtual bool safe() const
|
||||
{
|
||||
return heap::Safe;
|
||||
}
|
||||
|
||||
const heap& get_heap() const
|
||||
{
|
||||
return h;
|
||||
}
|
||||
{
|
||||
return h;
|
||||
}
|
||||
|
||||
const stack_type& get_st_blue() const
|
||||
{
|
||||
return st_blue;
|
||||
}
|
||||
{
|
||||
return st_blue;
|
||||
}
|
||||
|
||||
const stack_type& get_st_red() const
|
||||
{
|
||||
return st_red;
|
||||
}
|
||||
{
|
||||
return st_red;
|
||||
}
|
||||
private:
|
||||
|
||||
void push(stack_type& st, const state* s,
|
||||
|
|
@ -421,6 +426,8 @@ namespace spot
|
|||
class explicit_magic_search_heap
|
||||
{
|
||||
public:
|
||||
enum { Safe = 1 };
|
||||
|
||||
class color_ref
|
||||
{
|
||||
public:
|
||||
|
|
@ -505,6 +512,8 @@ namespace spot
|
|||
class bsh_magic_search_heap
|
||||
{
|
||||
public:
|
||||
enum { Safe = 0 };
|
||||
|
||||
class color_ref
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -125,24 +125,29 @@ namespace spot
|
|||
return os;
|
||||
}
|
||||
|
||||
virtual bool safe() const
|
||||
{
|
||||
return heap::Safe;
|
||||
}
|
||||
|
||||
const heap& get_heap() const
|
||||
{
|
||||
return h;
|
||||
}
|
||||
{
|
||||
return h;
|
||||
}
|
||||
|
||||
const stack_type& get_st_blue() const
|
||||
{
|
||||
return st_blue;
|
||||
}
|
||||
{
|
||||
return st_blue;
|
||||
}
|
||||
|
||||
const stack_type& get_st_red() const
|
||||
{
|
||||
return st_red;
|
||||
}
|
||||
{
|
||||
return st_red;
|
||||
}
|
||||
private:
|
||||
|
||||
void push(stack_type& st, const state* s,
|
||||
const bdd& label, const bdd& acc)
|
||||
const bdd& label, const bdd& acc)
|
||||
{
|
||||
inc_depth();
|
||||
tgba_succ_iterator* i = a_->succ_iter(s);
|
||||
|
|
@ -436,6 +441,8 @@ namespace spot
|
|||
typedef Sgi::hash_map<const state*, color,
|
||||
state_ptr_hash, state_ptr_equal> hash_type;
|
||||
public:
|
||||
enum { Safe = 1 };
|
||||
|
||||
class color_ref
|
||||
{
|
||||
public:
|
||||
|
|
@ -568,6 +575,8 @@ namespace spot
|
|||
typedef Sgi::hash_set<const state*,
|
||||
state_ptr_hash, state_ptr_equal> hcyan_type;
|
||||
public:
|
||||
enum { Safe = 0 };
|
||||
|
||||
class color_ref
|
||||
{
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -75,37 +75,36 @@ struct ec_algo
|
|||
spot::emptiness_check* (*construct)(const spot::tgba*, spot::option_map o);
|
||||
unsigned int min_acc;
|
||||
unsigned int max_acc;
|
||||
bool safe;
|
||||
};
|
||||
|
||||
ec_algo ec_algos[] =
|
||||
{
|
||||
{ "Cou99", "!poprem",
|
||||
couvreur99_cons, 0, -1U, true },
|
||||
couvreur99_cons, 0, -1U },
|
||||
{ "Cou99_shy-", "!poprem shy !group",
|
||||
couvreur99_cons, 0, -1U, true },
|
||||
couvreur99_cons, 0, -1U },
|
||||
{ "Cou99_shy", "!poprem shy group",
|
||||
couvreur99_cons, 0, -1U, true },
|
||||
couvreur99_cons, 0, -1U },
|
||||
{ "Cou99_rem", "poprem",
|
||||
couvreur99_cons, 0, -1U, true },
|
||||
couvreur99_cons, 0, -1U },
|
||||
{ "Cou99_rem_shy-", "poprem shy !group",
|
||||
couvreur99_cons, 0, -1U, true },
|
||||
couvreur99_cons, 0, -1U },
|
||||
{ "Cou99_rem_shy", "poprem shy group",
|
||||
couvreur99_cons, 0, -1U, true },
|
||||
couvreur99_cons, 0, -1U },
|
||||
{ "CVWY90", 0,
|
||||
spot::magic_search, 0, 1, true },
|
||||
spot::magic_search, 0, 1 },
|
||||
{ "CVWY90_bsh", "bsh=4K",
|
||||
spot::magic_search, 0, 1, false },
|
||||
spot::magic_search, 0, 1 },
|
||||
{ "GV04", 0,
|
||||
spot::explicit_gv04_check, 0, 1, true },
|
||||
spot::explicit_gv04_check, 0, 1 },
|
||||
{ "SE05", 0,
|
||||
spot::se05, 0, 1, true },
|
||||
spot::se05, 0, 1 },
|
||||
{ "SE05_bsh", "bsh=4K",
|
||||
spot::se05, 0, 1, false },
|
||||
spot::se05, 0, 1 },
|
||||
{ "Tau03", 0,
|
||||
spot::explicit_tau03_search, 1, -1U, true },
|
||||
spot::explicit_tau03_search, 1, -1U },
|
||||
{ "Tau03_opt", 0,
|
||||
spot::explicit_tau03_opt_search, 0, -1U, true },
|
||||
spot::explicit_tau03_opt_search, 0, -1U },
|
||||
};
|
||||
|
||||
spot::option_map options;
|
||||
|
|
@ -1038,7 +1037,7 @@ main(int argc, char** argv)
|
|||
}
|
||||
else
|
||||
{
|
||||
if (ec_algos[i].safe)
|
||||
if (ec->safe())
|
||||
{
|
||||
if (!opt_paper)
|
||||
std::cout << "empty language" << std::endl;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue