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

Add -rD option to ltl2tgba, to display some caching statistics.

Browse source 
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh (print_stats):
New function.
* src/tgbatest/ltl2tgba.cc: Call it.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-19 21:03:56 +02:00
parent babc024097
commit a80a5137fd
3 changed files with 44 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ltlvisit/simplify.cc
View file

@ -121,6 +121,16 @@ namespace spot
opt.containment_checks |= opt.containment_checks_stronger; opt.containment_checks |= opt.containment_checks_stronger;
} }
void
print_stats(std::ostream& os) const
{
os << "simplified formulae: " << simplified_.size() << " entries\n"
<< "negative normal form: " << nenoform_.size() << " entries\n"
<< "syntactic implications: " << syntimpl_.size() << " entries\n"
<< "boolean to bdd: " << as_bdd_.size() << " entries\n"
<< "star normal form: " << snf_cache_.size() << " entries\n";
}
// Convert a Boolean formula into a BDD for easier comparison. // Convert a Boolean formula into a BDD for easier comparison.
bdd bdd
as_bdd(const formula* f) as_bdd(const formula* f)
@ -4249,5 +4259,12 @@ namespace spot
return cache_->dict; return cache_->dict;
} }
void
ltl_simplifier::print_stats(std::ostream& os) const
{
cache_->print_stats(os);
}
} }
} }

4
src/ltlvisit/simplify.hh
View file

@ -24,6 +24,7 @@
#include "ltlast/formula.hh" #include "ltlast/formula.hh"
#include "bdd.h" #include "bdd.h"
#include "tgba/bdddict.hh" #include "tgba/bdddict.hh"
#include <iosfwd>
namespace spot namespace spot
{ {
@ -136,6 +137,9 @@ namespace spot
/// Cached version of spot::ltl::star_normal_form(). /// Cached version of spot::ltl::star_normal_form().
const formula* star_normal_form(const formula* f); const formula* star_normal_form(const formula* f);
/// Dump statistics about the caches.
void print_stats(std::ostream& os) const;
private: private:
ltl_simplifier_cache* cache_; ltl_simplifier_cache* cache_;
// Copy disallowed. // Copy disallowed.

23
src/tgbatest/ltl2tgba.cc
View file

@ -177,6 +177,7 @@ syntax(char* prog)
<< " -r6 reduce formula using tau03+" << std::endl << " -r6 reduce formula using tau03+" << std::endl
<< " -r7 reduce formula using tau03+ and -r4" << std::endl << " -r7 reduce formula using tau03+ and -r4" << std::endl
<< " -rd display the reduced formula" << std::endl << " -rd display the reduced formula" << std::endl
<< " -rD dump statistics about the simplifier cache" << std::endl
<< " -rL disable basic rewritings producing larger formulas" << " -rL disable basic rewritings producing larger formulas"
<< std::endl << std::endl << std::endl << std::endl
@ -305,6 +306,7 @@ main(int argc, char** argv)
bool simpltl = false; bool simpltl = false;
spot::ltl::ltl_simplifier_options redopt(false, false, false, false, spot::ltl::ltl_simplifier_options redopt(false, false, false, false,
false, false, false); false, false, false);
bool simpcache_stats = false;
bool scc_filter_all = false; bool scc_filter_all = false;
bool symbolic_scc_pruning = false; bool symbolic_scc_pruning = false;
bool display_reduced_form = false; bool display_reduced_form = false;
@ -619,6 +621,10 @@ main(int argc, char** argv)
{ {
display_reduced_form = true; display_reduced_form = true;
} }
else if (!strcmp(argv[formula_index], "-rD"))
{
simpcache_stats = true;
}
else if (!strcmp(argv[formula_index], "-RDS")) else if (!strcmp(argv[formula_index], "-RDS"))
{ {
reduction_dir_sim = true; reduction_dir_sim = true;
@ -879,6 +885,23 @@ main(int argc, char** argv)
tm.stop("translating formula"); tm.stop("translating formula");
to_free = a; to_free = a;
if (simp && simpcache_stats)
{
simp->print_stats(std::cerr);
bddStat s;
bdd_stats(&s);
std::cerr << "BDD produced: " << s.produced
<< "\n nodenum: " << s.nodenum
<< "\n maxnodenum: " << s.maxnodenum
<< "\n freenodes: " << s.freenodes
<< "\n minfreenodes: " << s.minfreenodes
<< "\n varnum: " << s.varnum
<< "\n cachesize: " << s.cachesize
<< "\n gbcnum: " << s.gbcnum
<< std::endl;
bdd_fprintstat(stderr);
dict->dump(std::cerr);
}
delete simp; delete simp;
} }