diff --git a/ChangeLog b/ChangeLog index a00439cb9..c13167507 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2006-02-15 Alexandre Duret-Lutz + + * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh: + Count the number of removed components. + 2006-02-14 Alexandre Duret-Lutz Soheib Baarir diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 0bac3495b..d4897c4a4 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -32,10 +32,14 @@ namespace spot couvreur99_check::couvreur99_check(const tgba* a, option_map o, const numbered_state_heap_factory* nshf) - : emptiness_check(a, o) + : emptiness_check(a, o), + removed_components(0) { poprem_ = o.get("poprem", 1); ecs_ = new couvreur99_check_status(a, nshf); + stats["removed components"] = + static_cast + (&couvreur99_check::get_removed_components); } couvreur99_check::~couvreur99_check() @@ -43,9 +47,16 @@ namespace spot delete ecs_; } + unsigned + couvreur99_check::get_removed_components() const + { + return removed_components; + } + void couvreur99_check::remove_component(const state* from) { + ++removed_components; // If rem has been updated, removing states is very easy. if (poprem_) { diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 12267567e..7c31e4fb5 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -180,6 +180,9 @@ namespace spot /// Whether to store the state to be removed. bool poprem_; + /// Number of dead SCC removed by the algorithm. + unsigned removed_components; + unsigned get_removed_components() const; }; /// \brief A version of spot::couvreur99_check that tries to visit @@ -231,8 +234,7 @@ namespace spot void clear_todo(); - // Whether successors should be grouped for states in the same - // SCC. + /// Whether successors should be grouped for states in the same SCC. bool group_; // If the "group2" option is set (it implies "group"), we // reprocess the successor states of SCC that have been merged.