From bb47e31b1e1298ccc45e84c741de5b2b8d39d9fa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 15 Feb 2006 13:41:37 +0000 Subject: [PATCH] * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh: Count the number of removed components. --- ChangeLog | 5 +++++ src/tgbaalgos/gtec/gtec.cc | 13 ++++++++++++- src/tgbaalgos/gtec/gtec.hh | 6 ++++-- 3 files changed, 21 insertions(+), 3 deletions(-) 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.