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

* src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_stats):

Browse source 
New function.
* src/tgbaalgos/emptinesscheck.hh (emptiness_check::print_stats):
Likewise.
* iface/gspn/ltlgspn.cc (main) <Couvreur>: Call print_stats().
* iface/gspn/ltleesrg.cc (main): Likewise.
This commit is contained in:
Alexandre Duret-Lutz 2004-01-09 10:56:56 +00:00
parent 4732d165db
commit 7a54e04800
5 changed files with 35 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,5 +1,12 @@
2004-01-09 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-01-09 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_stats):
New function.
* src/tgbaalgos/emptinesscheck.hh (emptiness_check::print_stats):
Likewise.
* iface/gspn/ltlgspn.cc (main) <Couvreur>: Call print_stats().
* iface/gspn/ltleesrg.cc (main): Likewise.
* iface/gspn/ltlgspn.cc: Add option -P. * iface/gspn/ltlgspn.cc: Add option -P.
2004-01-08 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-01-08 Alexandre Duret-Lutz <adl@src.lip6.fr>

5
iface/gspn/ltleesrg.cc
View file

@ -75,12 +75,15 @@ main(int argc, char **argv)
{ {
ec.counter_example(); ec.counter_example();
ec.print_result(std::cout, &a); ec.print_result(std::cout, &a);
exit(1);
} }
else else
{ {
std::cout << "empty" << std::endl; std::cout << "empty" << std::endl;
} }
std::cout << std::endl;
ec.print_stats(std::cout);
if (!res)
exit(1);
} }
delete prod; delete prod;

5
iface/gspn/ltlgspn.cc
View file

@ -146,12 +146,15 @@ main(int argc, char **argv)
{ {
std::cout << "non empty" << std::endl; std::cout << "non empty" << std::endl;
} }
exit(1);
} }
else else
{ {
std::cout << "empty" << std::endl; std::cout << "empty" << std::endl;
} }
std::cout << std::endl;
ec.print_stats(std::cout);
if (!res)
exit(1);
} }
break; break;
case Magic: case Magic:

13
src/tgbaalgos/emptinesscheck.cc
View file

@ -633,4 +633,17 @@ namespace spot
// forming a cycle. // forming a cycle.
complete_cycle(scc, start, suffix.back()); complete_cycle(scc, start, suffix.back());
} }
void
emptiness_check::print_stats(std::ostream& os) const
{
os << h.size() << " unique states visited" << std::endl;
os << suffix.size() << " states in suffix" << std::endl;
os << period.size() << " states in period" << std::endl;
os << root.size()
<< " strongly connected components in search stack"
<< std::endl;
}
} }

8
src/tgbaalgos/emptinesscheck.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -68,9 +68,15 @@ namespace spot
/// Compute a counter example if tgba_emptiness_check() returned false. /// Compute a counter example if tgba_emptiness_check() returned false.
void counter_example(); void counter_example();
/// \brief Display the example computed by counter_example().
///
/// \param restrict optional automaton to project the example on.
std::ostream& print_result(std::ostream& os, std::ostream& print_result(std::ostream& os,
const tgba* restrict = 0) const; const tgba* restrict = 0) const;
/// Output statistics about this object.
void print_stats(std::ostream& os) const;
private: private:
struct connected_component struct connected_component