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

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

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2005-01-10 17:22:25 +00:00
parent a4b9b791ef
commit 6a0ab6c081
2 changed files with 31 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2005-01-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbatest/randtgba.cc: Add option -P.
2005-01-10 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr> 2005-01-10 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr>
* src/tgbaalgos/tau03.cc: Typo. * src/tgbaalgos/tau03.cc: Typo.

32
src/tgbatest/randtgba.cc
View file

@ -31,8 +31,10 @@
#include "ltlenv/defaultenv.hh" #include "ltlenv/defaultenv.hh"
#include "ltlast/atomic_prop.hh" #include "ltlast/atomic_prop.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaparse/public.hh"
#include "misc/random.hh" #include "misc/random.hh"
#include "tgba/tgbatba.hh" #include "tgba/tgbatba.hh"
#include "tgba/tgbaproduct.hh"
#include "misc/timer.hh" #include "misc/timer.hh"
#include "tgbaalgos/emptiness.hh" #include "tgbaalgos/emptiness.hh"
@ -132,6 +134,8 @@ syntax(char* prog)
<< std::endl << std::endl
<< " -n N number of nodes of the graph [20]" << std::endl << " -n N number of nodes of the graph [20]" << std::endl
<< " -O ALGO run Only ALGO" << std::endl << " -O ALGO run Only ALGO" << std::endl
<< " -P FILE multiply the random automata with the automaton "
<< "from `FILE'." << std::endl
<< " -r compute and replay acceptance runs (implies -e)" << " -r compute and replay acceptance runs (implies -e)"
<< std::endl << std::endl
<< " -R N repeat each emptiness-check and accepting run " << " -R N repeat each emptiness-check and accepting run "
@ -431,8 +435,12 @@ main(int argc, char** argv)
int exit_code = 0; int exit_code = 0;
spot::tgba_explicit* formula = 0;
spot::tgba* product = 0;
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;
spot::bdd_dict* dict = new spot::bdd_dict();
if (argc <= 1) if (argc <= 1)
syntax(argv[0]); syntax(argv[0]);
@ -504,6 +512,16 @@ main(int argc, char** argv)
exit(1); exit(1);
} }
} }
else if (!strcmp(argv[argn], "-P"))
{
if (argc < argn + 2)
syntax(argv[0]);
spot::tgba_parse_error_list pel;
formula = spot::tgba_parse(argv[++argn], pel, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, argv[argn], pel))
return 2;
formula->merge_transitions();
}
else if (!strcmp(argv[argn], "-r")) else if (!strcmp(argv[argn], "-r"))
{ {
opt_replay = true; opt_replay = true;
@ -544,8 +562,6 @@ main(int argc, char** argv)
} }
} }
spot::bdd_dict* dict = new spot::bdd_dict();
spot::timer_map tm_ec; spot::timer_map tm_ec;
spot::timer_map tm_ar; spot::timer_map tm_ar;
std::set<int> failed_seeds; std::set<int> failed_seeds;
@ -557,8 +573,12 @@ main(int argc, char** argv)
spot::srand(opt_ec_seed); spot::srand(opt_ec_seed);
} }
spot::tgba* a = spot::random_graph(opt_n, opt_d, ap, dict, spot::tgba* a;
opt_n_acc, opt_a, opt_t, &env); spot::tgba* r = a = spot::random_graph(opt_n, opt_d, ap, dict,
opt_n_acc, opt_a, opt_t, &env);
if (formula)
a = product = new spot::tgba_product(formula, a);
if (!opt_ec) if (!opt_ec)
{ {
@ -725,7 +745,9 @@ main(int argc, char** argv)
delete degen; delete degen;
} }
delete a; delete product;
delete r;
delete formula;
if (opt_ec) if (opt_ec)
{ {