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

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

Browse source 
(emptiness_check_instantiator): New class.
* src/misc/optionmap.hh (set (const option_map&)): New method.
* src/tgbatest/randtgba.cc: Create every emptiness check via
emptiness_check_instantiator.
This commit is contained in:
Alexandre Duret-Lutz 2005-02-17 19:14:03 +00:00
parent 435b03c2b2
commit 4e1916ec50
7 changed files with 239 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,5 +1,11 @@
2005-02-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc
(emptiness_check_instantiator): New class.
* src/misc/optionmap.hh (set (const option_map&)): New method.
* src/tgbatest/randtgba.cc: Create every emptiness check via
emptiness_check_instantiator.
* src/tgbaalgos/emptiness.hh,
src/tgbaalgos/emptiness.cc (emptiness_check::safe): New method.
* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,

8
src/misc/optionmap.cc
View file

@ -134,6 +134,14 @@ namespace spot
return old;
}
void
option_map::set(const option_map& o)
{
for (std::map<std::string, int>::const_iterator it = o.options_.begin();
it != o.options_.end(); ++it)
options_[it->first] = it->second;
}
int&
option_map::operator[](const char* option)
{

3
src/misc/optionmap.hh
View file

@ -70,6 +70,9 @@ namespace spot
/// or \a def otherwise.
int set(const char* option, int val, int def = 0);
/// Acquire all the settings of \a o.
void set(const option_map& o);
/// \brief Get a reference to the current value of \a option.
int& operator[](const char* option);

2
src/sanity/style.test
View file

@ -94,7 +94,7 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
grep '! ' $tmp &&
diag 'No space after unary operators (!).'
grep ",[^ \"%']" $tmp &&
grep ",[^ \t\"%']" $tmp &&
diag 'Space after coma.'
grep '[^ ]&&[^ ]' $tmp &&

144
src/tgbaalgos/emptiness.cc
View file

@ -24,9 +24,19 @@
#include "tgba/tgba.hh"
#include "tgba/bddprint.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gv04.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/se05.hh"
#include "tgbaalgos/tau03.hh"
#include "tgbaalgos/tau03opt.hh"
namespace spot
{
// tgba_run
//////////////////////////////////////////////////////////////////////
tgba_run::~tgba_run()
{
for (steps::const_iterator i = prefix.begin(); i != prefix.end(); ++i)
@ -51,6 +61,20 @@ namespace spot
}
}
tgba_run&
tgba_run::operator=(const tgba_run& run)
{
if (&run != this)
{
this->~tgba_run();
new(this) tgba_run(run);
}
return *this;
}
// print_tgba_run
//////////////////////////////////////////////////////////////////////
std::ostream&
print_tgba_run(std::ostream& os,
const tgba* a,
@ -82,17 +106,8 @@ namespace spot
return os;
}
tgba_run&
tgba_run::operator=(const tgba_run& run)
{
if (&run != this)
{
this->~tgba_run();
new(this) tgba_run(run);
}
return *this;
}
// emptiness_check_result
//////////////////////////////////////////////////////////////////////
tgba_run*
emptiness_check_result::accepting_run()
@ -121,6 +136,9 @@ namespace spot
}
// emptiness_check
//////////////////////////////////////////////////////////////////////
emptiness_check::~emptiness_check()
{
}
@ -157,6 +175,110 @@ namespace spot
return os;
}
// emptiness_check_instantiator
//////////////////////////////////////////////////////////////////////
namespace
{
spot::emptiness_check*
couvreur99_cons(const spot::tgba* a, spot::option_map o)
{
return spot::couvreur99(a, o);
}
struct ec_algo
{
const char* name;
spot::emptiness_check* (*construct)(const spot::tgba*,
spot::option_map);
unsigned int min_acc;
unsigned int max_acc;
};
ec_algo ec_algos[] =
{
{ "Cou99", couvreur99_cons, 0, -1U },
{ "CVWY90", spot::magic_search, 0, 1 },
{ "GV04", spot::explicit_gv04_check, 0, 1 },
{ "SE05", spot::se05, 0, 1 },
{ "Tau03", spot::explicit_tau03_search, 1, -1U },
{ "Tau03_opt", spot::explicit_tau03_opt_search, 0, -1U },
};
}
emptiness_check_instantiator::emptiness_check_instantiator(option_map o,
void* i)
: o_(o), info_(i)
{
}
unsigned int
emptiness_check_instantiator::min_acceptance_conditions() const
{
return static_cast<ec_algo*>(info_)->min_acc;
}
unsigned int
emptiness_check_instantiator::max_acceptance_conditions() const
{
return static_cast<ec_algo*>(info_)->max_acc;
}
emptiness_check*
emptiness_check_instantiator::instantiate(const tgba* a) const
{
return static_cast<ec_algo*>(info_)->construct(a, o_);
}
emptiness_check_instantiator*
emptiness_check_instantiator::construct(const char* name, const char** err)
{
// Skip spaces.
while (*name && strchr(" \t\n", *name))
++name;
const char* opt_str = strchr(name, '(');
option_map o;
if (opt_str)
{
const char* opt_start = opt_str + 1;
const char* opt_end = strchr(opt_start, ')');
if (!opt_end)
{
*err = opt_start;
return 0;
}
std::string opt(opt_start, opt_end);
const char* res = o.parse_options(opt.c_str());
if (res)
{
*err = opt.c_str() - res + opt_start;
return 0;
}
}
if (!opt_str)
opt_str = name + strlen(name);
// Ignore spaces before `(' (or trailing spaces).
while (opt_str > name && strchr(" \t\n", *--opt_str))
continue;
std::string n(name, opt_str + 1);
ec_algo* info = ec_algos;
for (unsigned i = 0; i < sizeof(ec_algos)/sizeof(*ec_algos); ++i, ++info)
if (n == info->name)
return new emptiness_check_instantiator(o, info);
*err = name;
return 0;
}
// tgba_run_to_tgba
//////////////////////////////////////////////////////////////////////
namespace
{
std::string format_state(const tgba* a, const state* s, int n)

51
src/tgbaalgos/emptiness.hh
View file

@ -188,6 +188,57 @@ namespace spot
option_map o_; ///< The options
};
// Dynamically create emptiness checks. Given their name and options.
class emptiness_check_instantiator
{
public:
/// \brief Create an emptiness-check instantiator, given the name
/// of an emptiness check.
///
/// \a name should have the form \c "name" or \c "name(options)".
///
/// On error, the function returns 0. If the name of the algorithm
/// was unknown, \c *err will be set to \c name. If some fragment of
/// the options could not be parsed, \c *err will point to that
/// fragment.
static emptiness_check_instantiator* construct(const char* name,
const char** err);
/// Actually instantiate the emptiness check, for \a a.
emptiness_check* instantiate(const tgba* a) const;
/// Accessor to the options.
/// @{
const option_map&
options() const
{
return o_;
}
option_map&
options()
{
return o_;
}
/// @}
/// \brief Minimum number of acceptance conditions supported by
/// the emptiness check.
unsigned int min_acceptance_conditions() const;
/// \brief Maximum number of acceptance conditions supported by
/// the emptiness check.
///
/// \return \c -1U if no upper bound exists.
unsigned int max_acceptance_conditions() const;
private:
emptiness_check_instantiator(option_map o, void* i);
option_map o_;
void *info_;
};
/// @}
/// \addtogroup emptiness_check_algorithms Emptiness-check algorithms

89
src/tgbatest/randtgba.cc
View file

@ -53,77 +53,43 @@
#include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/emptiness_stats.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gv04.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/se05.hh"
#include "tgbaalgos/tau03.hh"
#include "tgbaalgos/tau03opt.hh"
#include "tgbaalgos/replayrun.hh"
spot::emptiness_check*
couvreur99_cons(const spot::tgba* a, spot::option_map o)
{
return spot::couvreur99(a, o);
}
struct ec_algo
{
const char* name;
const char* options;
spot::emptiness_check* (*construct)(const spot::tgba*, spot::option_map o);
unsigned int min_acc;
unsigned int max_acc;
spot::emptiness_check_instantiator* inst;
};
ec_algo ec_algos[] =
{
{ "Cou99", "!poprem",
couvreur99_cons, 0, -1U },
{ "Cou99_shy-", "!poprem shy !group",
couvreur99_cons, 0, -1U },
{ "Cou99_shy", "!poprem shy group",
couvreur99_cons, 0, -1U },
{ "Cou99_rem", "poprem",
couvreur99_cons, 0, -1U },
{ "Cou99_rem_shy-", "poprem shy !group",
couvreur99_cons, 0, -1U },
{ "Cou99_rem_shy", "poprem shy group",
couvreur99_cons, 0, -1U },
{ "CVWY90", 0,
spot::magic_search, 0, 1 },
{ "CVWY90_bsh", "bsh=4K",
spot::magic_search, 0, 1 },
{ "GV04", 0,
spot::explicit_gv04_check, 0, 1 },
{ "SE05", 0,
spot::se05, 0, 1 },
{ "SE05_bsh", "bsh=4K",
spot::se05, 0, 1 },
{ "Tau03", 0,
spot::explicit_tau03_search, 1, -1U },
{ "Tau03_opt", 0,
spot::explicit_tau03_opt_search, 0, -1U },
{ "Cou99", "Cou99(!poprem)", 0 },
{ "Cou99_shy-", "Cou99(!poprem shy !group)", 0 },
{ "Cou99_shy", "Cou99(!poprem shy group)", 0 },
{ "Cou99_rem", "Cou99(poprem)", 0 },
{ "Cou99_rem_shy-", "Cou99(poprem shy !group)", 0 },
{ "Cou99_rem_shy", "Cou99(poprem shy group)", 0 },
{ "CVWY90", "CVWY90", 0 },
{ "CVWY90_bsh", "CVWY90(bsh=4K)", 0 },
{ "GV04", "GV04", 0 },
{ "SE05", "SE05", 0 },
{ "SE05_bsh", "SE05(bsh=4K)", 0 },
{ "Tau03", "Tau03", 0 },
{ "Tau03_opt", "Tau03_opt", 0 },
};
spot::option_map options;
spot::emptiness_check*
cons_emptiness_check(int num, const spot::tgba* a,
const spot::tgba* degen, unsigned int n_acc)
{
spot::option_map o = options;
if (ec_algos[num].options)
{
const char* err = o.parse_options(ec_algos[num].options);
assert(!err);
(void)err;
}
if (n_acc < ec_algos[num].min_acc || n_acc > ec_algos[num].max_acc)
spot::emptiness_check_instantiator* inst = ec_algos[num].inst;
if (n_acc < inst->min_acceptance_conditions()
|| n_acc > inst->max_acceptance_conditions())
a = degen;
if (a)
return ec_algos[num].construct(a, o);
return inst->instantiate(a);
return 0;
}
@ -602,6 +568,8 @@ main(int argc, char** argv)
spot::tgba* formula = 0;
spot::tgba* product = 0;
spot::option_map options;
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;
spot::bdd_dict* dict = new spot::bdd_dict();
@ -807,6 +775,23 @@ main(int argc, char** argv)
int init_opt_ec = opt_ec;
spot::ltl::atomic_prop_set* apf = new spot::ltl::atomic_prop_set;
if (opt_ec)
{
for (unsigned i = 0; i < sizeof(ec_algos) / sizeof(*ec_algos); ++i)
{
const char* err;
ec_algos[i].inst =
spot::emptiness_check_instantiator::construct(ec_algos[i].options,
&err);
if (ec_algos[i].inst == 0)
{
std::cerr << "Parse error after `" << err << "'" << std::endl;
exit(1);
}
ec_algos[i].inst->options().set(options);
}
}
do
{
if (opt_F)