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

* src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh:

Browse source 
Count the number of removed components.
This commit is contained in:
Alexandre Duret-Lutz 2006-02-15 13:41:37 +00:00
parent 857f0ac54e
commit bb47e31b1e
3 changed files with 21 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2006-02-15 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh:
Count the number of removed components.
2006-02-14 Alexandre Duret-Lutz <adl@src.lip6.fr> 2006-02-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
Soheib Baarir <Souheib.Baarir@lip6.fr> Soheib Baarir <Souheib.Baarir@lip6.fr>

13
src/tgbaalgos/gtec/gtec.cc
View file

@ -32,10 +32,14 @@ namespace spot
couvreur99_check::couvreur99_check(const tgba* a, couvreur99_check::couvreur99_check(const tgba* a,
option_map o, option_map o,
const numbered_state_heap_factory* nshf) const numbered_state_heap_factory* nshf)
: emptiness_check(a, o) : emptiness_check(a, o),
removed_components(0)
{ {
poprem_ = o.get("poprem", 1); poprem_ = o.get("poprem", 1);
ecs_ = new couvreur99_check_status(a, nshf); ecs_ = new couvreur99_check_status(a, nshf);
stats["removed components"] =
static_cast<spot::unsigned_statistics::unsigned_fun>
(&couvreur99_check::get_removed_components);
} }
couvreur99_check::~couvreur99_check() couvreur99_check::~couvreur99_check()
@ -43,9 +47,16 @@ namespace spot
delete ecs_; delete ecs_;
} }
unsigned
couvreur99_check::get_removed_components() const
{
return removed_components;
}
void void
couvreur99_check::remove_component(const state* from) couvreur99_check::remove_component(const state* from)
{ {
++removed_components;
// If rem has been updated, removing states is very easy. // If rem has been updated, removing states is very easy.
if (poprem_) if (poprem_)
{ {

6
src/tgbaalgos/gtec/gtec.hh
View file

@ -180,6 +180,9 @@ namespace spot
/// Whether to store the state to be removed. /// Whether to store the state to be removed.
bool poprem_; 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 /// \brief A version of spot::couvreur99_check that tries to visit
@ -231,8 +234,7 @@ namespace spot
void clear_todo(); void clear_todo();
// Whether successors should be grouped for states in the same /// Whether successors should be grouped for states in the same SCC.
// SCC.
bool group_; bool group_;
// If the "group2" option is set (it implies "group"), we // If the "group2" option is set (it implies "group"), we
// reprocess the successor states of SCC that have been merged. // reprocess the successor states of SCC that have been merged.