Commit 56188c70 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlcross: be more verbose about product size

This helps diagnosing #96.

* src/bin/ltlcross.cc (process_formula): Print product sizes if
--verbose.
parent 36a3dc45
...@@ -1286,8 +1286,16 @@ namespace ...@@ -1286,8 +1286,16 @@ namespace
<< pos[i]->num_edges() << " ed.)\n"; << pos[i]->num_edges() << " ed.)\n";
auto p = spot::product(pos[i], statespace); auto p = spot::product(pos[i], statespace);
pos_prod[i] = p; pos_prod[i] = p;
if (verbose)
std::cerr << "info: product has " << p->num_states()
<< " st., " << p->num_edges()
<< " ed.\n";
auto sm = new spot::scc_info(p); auto sm = new spot::scc_info(p);
pos_map[i] = sm; pos_map[i] = sm;
if (verbose)
std::cerr << "info: " << sm->scc_count()
<< " SCCs\n";
// Statistics // Statistics
if (want_stats) if (want_stats)
...@@ -1303,17 +1311,24 @@ namespace ...@@ -1303,17 +1311,24 @@ namespace
for (size_t i = 0; i < m; ++i) for (size_t i = 0; i < m; ++i)
if (neg[i]) if (neg[i])
{ {
if (verbose) if (verbose)
std::cerr << ("info: building product between state-space and" std::cerr << ("info: building product between state-space and"
" N") << i " N") << i
<< " (" << neg[i]->num_states() << " st., " << " (" << neg[i]->num_states() << " st., "
<< neg[i]->num_edges() << " ed.)\n"; << neg[i]->num_edges() << " ed.)\n";
auto p = spot::product(neg[i], statespace); auto p = spot::product(neg[i], statespace);
neg_prod[i] = p; neg_prod[i] = p;
if (verbose)
std::cerr << "info: product has " << p->num_states()
<< " st., " << p->num_edges()
<< " ed.\n";
auto sm = new spot::scc_info(p); auto sm = new spot::scc_info(p);
neg_map[i] = sm; neg_map[i] = sm;
if (verbose)
std::cerr << "info: " << sm->scc_count()
<< " SCCs\n";
// Statistics // Statistics
if (want_stats) if (want_stats)
{ {
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment