intersect: statistic provided using an object
* spot/mc/ec.hh, spot/mc/intersect.hh: here.
This commit is contained in:
parent
d430129bb1
commit
94f7c58f44
2 changed files with 21 additions and 13 deletions
|
|
@ -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:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue