Commit 2db69268 authored by Etienne Renault's avatar Etienne Renault
Browse files

intersect: statistic provided using an object

* spot/mc/ec.hh, spot/mc/intersect.hh: here.
parent e4224dcc
......@@ -49,7 +49,7 @@ namespace spot
: intersect<State, SuccIterator, StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>(sys, twa),
acc_(twa->acc())
acc_(twa->acc()), sccs_(0U)
{
}
......@@ -89,8 +89,10 @@ namespace spot
if (top_dfsnum == roots_.back().dfsnum)
{
roots_.pop_back();
++sccs_;
uf_.markdead(top_dfsnum);
}
dfs_ = this->todo.size() > dfs_ ? this->todo.size() : dfs_;
return true;
}
......@@ -238,14 +240,10 @@ namespace spot
return res;
}
// Refine stats to display
virtual std::string stats() override
virtual istats stats() override
{
return
std::to_string(this->dfs_number) + " unique states visited\n" +
std::to_string(roots_.size()) +
" strongly connected components in search stack\n" +
std::to_string(this->transitions) + " transitions explored\n";
return {this->states(), this->trans(), sccs_,
(unsigned)roots_.size(), dfs_};
}
private:
......@@ -262,5 +260,7 @@ namespace spot
std::vector<root_element> roots_;
int_unionfind uf_;
acc_cond acc_;
unsigned sccs_;
unsigned dfs_;
};
}
......@@ -25,6 +25,17 @@
namespace spot
{
/// \brief Wrapper to accumulate results from intersection
/// and emptiness checks
struct SPOT_API istats
{
unsigned states;
unsigned transitions;
unsigned sccs;
unsigned instack_sccs;
unsigned instack_item;
};
/// \brief This class explores (with a DFS) a product between a
/// system and a twa. This exploration is performed on-the-fly.
/// Since this exploration aims to be a generic we need to define
......@@ -154,12 +165,9 @@ namespace spot
return self().trace();
}
virtual std::string stats()
virtual istats stats()
{
return
std::to_string(dfs_number) + " unique states visited\n" +
std::to_string(transitions) + " transitions explored\n";
return {dfs_number, transitions, 0U, 0U, 0U};
}
protected:
......
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