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

* src/tgbatest/randtgba.cc: Add option -D.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2004-11-25 12:52:01 +00:00
parent f47f955a34
commit 2143d6c4b6
2 changed files with 32 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

2
ChangeLog
View file

@ -1,5 +1,7 @@
2004-11-25 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-11-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbatest/randtgba.cc: Add option -D.
* src/tgbaalgos/emptiness.hh (emptiness_check, emptiness_check_result): * src/tgbaalgos/emptiness.hh (emptiness_check, emptiness_check_result):
Add the TGBA considered as a protected attribute, and provide an Add the TGBA considered as a protected attribute, and provide an
automaton() accessor. automaton() accessor.

40
src/tgbatest/randtgba.cc
View file

@ -32,6 +32,7 @@
#include "ltlast/atomic_prop.hh" #include "ltlast/atomic_prop.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "misc/random.hh" #include "misc/random.hh"
#include "tgba/tgbatba.hh"
#include "tgbaalgos/emptiness.hh" #include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/emptiness_stats.hh" #include "tgbaalgos/emptiness_stats.hh"
@ -53,6 +54,9 @@ syntax(char* prog)
<< " one is true" << std::endl << " one is true" << std::endl
<< " [0 0.0]" << std::endl << " [0 0.0]" << std::endl
<< " -d F density of the graph [0.2]" << std::endl << " -d F density of the graph [0.2]" << std::endl
<< " -D degeneralize TGBA for emptiness-check algorithms that"
<< " would" << std::endl
<< " otherwise be skipped (implies -e)" << std::endl
<< " -e N compare result of all " << " -e N compare result of all "
<< "emptiness checks on N randomly generated graphs" << std::endl << "emptiness checks on N randomly generated graphs" << std::endl
<< " -g output in dot format" << std::endl << " -g output in dot format" << std::endl
@ -203,7 +207,7 @@ main(int argc, char** argv)
int opt_ec = 0; int opt_ec = 0;
int opt_ec_seed = 0; int opt_ec_seed = 0;
bool opt_replay = false; bool opt_replay = false;
bool opt_degen = false;
int argn = 0; int argn = 0;
int exit_code = 0; int exit_code = 0;
@ -235,6 +239,12 @@ main(int argc, char** argv)
syntax(argv[0]); syntax(argv[0]);
opt_d = to_float(argv[++argn]); opt_d = to_float(argv[++argn]);
} }
else if (!strcmp(argv[argn], "-D"))
{
opt_degen = true;
if (!opt_ec)
opt_ec = 1;
}
else if (!strcmp(argv[argn], "-e")) else if (!strcmp(argv[argn], "-e"))
{ {
if (argc < argn + 2) if (argc < argn + 2)
@ -309,6 +319,10 @@ main(int argc, char** argv)
} }
else else
{ {
spot::tgba* degen = 0;
if (opt_degen && opt_n_acc != 1)
degen = new spot::tgba_tba_proxy(a);
std::vector<spot::emptiness_check*> ec_obj; std::vector<spot::emptiness_check*> ec_obj;
std::vector<std::string> ec_name; std::vector<std::string> ec_name;
std::vector<bool> ec_safe; std::vector<bool> ec_safe;
@ -321,32 +335,36 @@ main(int argc, char** argv)
ec_name.push_back("couvreur99_shy"); ec_name.push_back("couvreur99_shy");
ec_safe.push_back(true); ec_safe.push_back(true);
if (opt_n_acc <= 1) if (opt_n_acc <= 1 || opt_degen)
{ {
ec_obj.push_back(spot::explicit_magic_search(a)); spot::tgba* d = opt_n_acc > 1 ? degen : a;
ec_obj.push_back(spot::explicit_magic_search(d));
ec_name.push_back("explicit_magic_search"); ec_name.push_back("explicit_magic_search");
ec_safe.push_back(true); ec_safe.push_back(true);
ec_obj.push_back(spot::bit_state_hashing_magic_search(a, 4096)); ec_obj.push_back(spot::bit_state_hashing_magic_search(d, 4096));
ec_name.push_back("bit_state_hashing_magic_search"); ec_name.push_back("bit_state_hashing_magic_search");
ec_safe.push_back(false); ec_safe.push_back(false);
ec_obj.push_back(spot::explicit_se05_search(a)); ec_obj.push_back(spot::explicit_se05_search(d));
ec_name.push_back("explicit_se05"); ec_name.push_back("explicit_se05");
ec_safe.push_back(true); ec_safe.push_back(true);
ec_obj.push_back(spot::bit_state_hashing_se05_search(a, 4096)); ec_obj.push_back(spot::bit_state_hashing_se05_search(d, 4096));
ec_name.push_back("bit_state_hashing_se05_search"); ec_name.push_back("bit_state_hashing_se05_search");
ec_safe.push_back(false); ec_safe.push_back(false);
ec_obj.push_back(spot::explicit_gv04_check(a)); ec_obj.push_back(spot::explicit_gv04_check(d));
ec_name.push_back("explicit_gv04"); ec_name.push_back("explicit_gv04");
ec_safe.push_back(true); ec_safe.push_back(true);
} }
if (opt_n_acc >= 1) if (opt_n_acc >= 1 || opt_degen)
{ {
ec_obj.push_back(spot::explicit_tau03_search(a)); spot::tgba* d = opt_n_acc == 0 ? degen : a;
ec_obj.push_back(spot::explicit_tau03_search(d));
ec_name.push_back("explicit_tau03_search"); ec_name.push_back("explicit_tau03_search");
ec_safe.push_back(true); ec_safe.push_back(true);
} }
@ -380,7 +398,7 @@ main(int argc, char** argv)
if (run) if (run)
{ {
std::ostringstream s; std::ostringstream s;
if (!spot::replay_tgba_run(s, a, run)) if (!spot::replay_tgba_run(s, res->automaton(), run))
{ {
std::cout << ", but could not replay it (ERROR!)"; std::cout << ", but could not replay it (ERROR!)";
failed_seeds.insert(opt_ec_seed); failed_seeds.insert(opt_ec_seed);
@ -433,6 +451,8 @@ main(int argc, char** argv)
std::cout << "ERROR: not all algorithms agree" << std::endl; std::cout << "ERROR: not all algorithms agree" << std::endl;
failed_seeds.insert(opt_ec_seed); failed_seeds.insert(opt_ec_seed);
} }
delete degen;
} }
delete a; delete a;