From acead199f55ad03d212a4694ba32e54aa2d78f51 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 26 Jan 2005 17:31:21 +0000 Subject: [PATCH] * src/tgbaalgos/gv04.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/gtec/ce.cc: Do not account for states that are computed but not visited by the BFS&DFS used to construct accepting runs. --- ChangeLog | 7 +++++++ src/tgbaalgos/gtec/ce.cc | 2 +- src/tgbaalgos/gv04.cc | 2 +- src/tgbaalgos/ndfs_result.hxx | 14 +++++++------- 4 files changed, 16 insertions(+), 9 deletions(-) diff --git a/ChangeLog b/ChangeLog index 6df4009c2..81bfc2b2f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2005-01-26 Alexandre Duret-Lutz + + * src/tgbaalgos/gv04.cc, src/tgbaalgos/ndfs_result.hxx, + src/tgbaalgos/gtec/ce.cc: Do not account for states that are + computed but not visited by the BFS&DFS used to construct + accepting runs. + 2005-01-25 Denis Poitrenaud * src/tgbatest/randtgba.cc: Complete performance measurements. diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index f293318f3..99a373ce3 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -180,7 +180,6 @@ namespace spot virtual const state* filter(const state* s) { - r->inc_ars_cycle_states(); numbered_state_heap::state_index_p sip = ecs->h->find(s); // Ignore unknown states. if (!sip.first) @@ -191,6 +190,7 @@ namespace spot // Stay in the final SCC. if (*sip.second < scc_root) return 0; + r->inc_ars_cycle_states(); return sip.first; } diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index cdcad1dbe..2f0e5e4bb 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -339,7 +339,6 @@ namespace spot virtual const state* filter(const state* s) { - r->inc_ars_cycle_states(); // Do not escape the SCC hash_type::const_iterator j = data.h.find(s); if (// This state was never visited so far. @@ -354,6 +353,7 @@ namespace spot delete s; return 0; } + r->inc_ars_cycle_states(); delete s; return j->first; } diff --git a/src/tgbaalgos/ndfs_result.hxx b/src/tgbaalgos/ndfs_result.hxx index 0a0b814dd..9fa0e09a3 100644 --- a/src/tgbaalgos/ndfs_result.hxx +++ b/src/tgbaalgos/ndfs_result.hxx @@ -272,7 +272,6 @@ namespace spot if (!f.it->done()) { const state *s_prime = f.it->current_state(); - inc_ars_cycle_states(); ndfsr_trace << " Visit the successor: " << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); @@ -287,6 +286,7 @@ namespace spot } else if (seen.find(s_prime) == seen.end()) { + inc_ars_cycle_states(); ndfsr_trace << " it is not seen, go down" << std::endl; seen.insert(s_prime); tgba_succ_iterator* i = a_->succ_iter(s_prime); @@ -295,6 +295,7 @@ namespace spot } else if ((acc & covered_acc) != acc) { + inc_ars_cycle_states(); ndfsr_trace << " a propagation is needed, " << "start a search" << std::endl; if (search(s_prime, target, dead)) @@ -398,7 +399,6 @@ namespace spot const state* filter(const state* s) { - ars->inc_ars_cycle_states(); if (!h.has_been_visited(s) || seen.find(s) != seen.end() || dead.find(s) != dead.end()) @@ -406,6 +406,7 @@ namespace spot delete s; return 0; } + ars->inc_ars_cycle_states(); seen.insert(s); return s; } @@ -491,11 +492,6 @@ namespace spot const state* filter(const state* s) { - if (cycle) - ars->inc_ars_cycle_states(); - else - ars->inc_ars_prefix_states(); - ndfsr_trace << "filter: " << a_->format_state(s); if (!h.has_been_visited(s) || seen.find(s) != seen.end()) { @@ -507,6 +503,10 @@ namespace spot return 0; } ndfsr_trace << " OK" << std::endl; + if (cycle) + ars->inc_ars_cycle_states(); + else + ars->inc_ars_prefix_states(); seen.insert(s); return s; }