diff --git a/spot/mc/ec.hh b/spot/mc/ec.hh index 8bac1f859..080eefabb 100644 --- a/spot/mc/ec.hh +++ b/spot/mc/ec.hh @@ -49,7 +49,7 @@ namespace spot : intersect>(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 roots_; int_unionfind uf_; acc_cond acc_; + unsigned sccs_; + unsigned dfs_; }; } diff --git a/spot/mc/intersect.hh b/spot/mc/intersect.hh index 6221b5788..cfc4f4e99 100644 --- a/spot/mc/intersect.hh +++ b/spot/mc/intersect.hh @@ -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: