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

* src/tgbaalgos/gtec/gtec.cc,

Browse source 
src/tgbaalgos/gtec/gtec.hh (couvreur99_check::print_stats): New.
* src/tgbatest/ltl2tgba.cc: Print emptiness-check statistics.
This commit is contained in:
Alexandre Duret-Lutz 2004-10-29 16:10:47 +00:00
parent 55014e9dcc
commit 32403566f6
4 changed files with 18 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,5 +1,9 @@
2004-10-29 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-10-29 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/gtec/gtec.cc,
src/tgbaalgos/gtec/gtec.hh (couvreur99_check::print_stats): New.
* src/tgbatest/ltl2tgba.cc: Print emptiness-check statistics.
* src/sanity/style.test: Diagnose superfluous constructs such * src/sanity/style.test: Diagnose superfluous constructs such
as `if (x) delete x;'. as `if (x) delete x;'.
* iface/gspn/gspn.cc, iface/gspn/ssp.cc, src/ltlvisit/basicreduce.cc, * iface/gspn/gspn.cc, iface/gspn/ssp.cc, src/ltlvisit/basicreduce.cc,

7
src/tgbaalgos/gtec/gtec.cc
View file

@ -234,6 +234,13 @@ namespace spot
return ecs_; return ecs_;
} }
std::ostream&
couvreur99_check::print_stats(std::ostream& os) const
{
ecs_->print_stats(os);
return os;
}
////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////
couvreur99_check_shy::couvreur99_check_shy(const tgba* a, couvreur99_check_shy::couvreur99_check_shy(const tgba* a,

2
src/tgbaalgos/gtec/gtec.hh
View file

@ -79,6 +79,8 @@ namespace spot
/// Check whether the automaton's language is empty. /// Check whether the automaton's language is empty.
virtual emptiness_check_result* check(); virtual emptiness_check_result* check();
virtual std::ostream& print_stats(std::ostream& os) const;
/// \brief Return the status of the emptiness-check. /// \brief Return the status of the emptiness-check.
/// ///
/// When check() succeed, the status should be passed along /// When check() succeed, the status should be passed along

8
src/tgbatest/ltl2tgba.cc
View file

@ -58,9 +58,10 @@ syntax(char* prog)
<< " -A same as -a, but as a set" << std::endl << " -A same as -a, but as a set" << std::endl
<< " -d turn on traces during parsing" << std::endl << " -d turn on traces during parsing" << std::endl
<< " -D degeneralize the automaton" << std::endl << " -D degeneralize the automaton" << std::endl
<< " -eALGO emptiness-check, expect and compute an accepting run" << " -e[ALGO] emptiness-check, expect and compute an "
<< "accepting run" << std::endl
<< " -E[ALGO] emptiness-check, expect no accepting run"
<< std::endl << std::endl
<< " -EALGO emptiness-check, expect no accepting run" << std::endl
<< " -f use Couvreur's FM algorithm for translation" << " -f use Couvreur's FM algorithm for translation"
<< std::endl << std::endl
<< " -F read the formula from the file" << std::endl << " -F read the formula from the file" << std::endl
@ -113,7 +114,7 @@ syntax(char* prog)
<< "(implies -f)" << std::endl << "(implies -f)" << std::endl
<< std::endl << std::endl
<< "Where ALGO should be one of:" << std::endl << "Where ALGO should be one of:" << std::endl
<< " couvreur99" << std::endl << " couvreur99 (the default)" << std::endl
<< " couvreur99_shy" << std::endl << " couvreur99_shy" << std::endl
<< " magic_search" << std::endl << " magic_search" << std::endl
<< " magic_search_repeated" << std::endl; << " magic_search_repeated" << std::endl;
@ -560,6 +561,7 @@ main(int argc, char** argv)
do do
{ {
spot::emptiness_check_result* res = ec->check(); spot::emptiness_check_result* res = ec->check();
ec->print_stats(std::cout);
if (expect_counter_example != !!res) if (expect_counter_example != !!res)
exit_code = 1; exit_code = 1;