diff --git a/spot/mc/bloemen.hh b/spot/mc/bloemen.hh index 615032fbe..d6111d3ef 100644 --- a/spot/mc/bloemen.hh +++ b/spot/mc/bloemen.hh @@ -93,7 +93,7 @@ namespace spot iterable_uf(shared_map& map, unsigned tid): map_(map), tid_(tid), size_(std::thread::hardware_concurrency()), - nb_th_(std::thread::hardware_concurrency()) + nb_th_(std::thread::hardware_concurrency()), inserted_(0) { } @@ -120,6 +120,8 @@ namespace spot // FIXME Should we add a local cache to avoid useless allocations? if (!b) delete v; + else + ++inserted_; uf_element* a_root = find(*it); if (a_root->uf_status_.load() == uf_status::DEAD) @@ -376,16 +378,23 @@ namespace spot } } + unsigned inserted() + { + return inserted_; + } + private: shared_map map_; ///< \brief Map shared by threads copy! unsigned tid_; ///< \brief The Id of the current thread unsigned size_; ///< \brief Maximum number of thread unsigned nb_th_; ///< \brief Current number of threads + unsigned inserted_; ///< \brief The number of insert succes }; /// \brief This object is returned by the algorithm below struct SPOT_API bloemen_stats { + unsigned inserted; ///< \brief Number of states inserted unsigned states; ///< \brief Number of states visited unsigned transitions; ///< \brief Number of transitions visited unsigned sccs; ///< \brief Number of SCCs visited @@ -477,7 +486,7 @@ namespace spot bloemen_stats stats() { - return {states_, transitions_, sccs_, walltime()}; + return {uf_.inserted(), states_, transitions_, sccs_, walltime()}; } private: @@ -487,6 +496,7 @@ namespace spot iterable_uf uf_; ///< Copy! unsigned tid_; unsigned nb_th_; + unsigned inserted_ = 0; ///< \brief Number of states inserted unsigned states_ = 0; ///< \brief Number of states visited unsigned transitions_ = 0; ///< \brief Number of transitions visited unsigned sccs_ = 0; ///< \brief Number of SCC visited diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index a91950361..97ec168a6 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -657,10 +657,12 @@ static int checked_main() unsigned sccs = 0; unsigned st = 0; unsigned tr = 0; + unsigned inserted = 0; for (unsigned i = 0; i < res.first.size(); ++i) { std::cout << "\n---- Thread number : " << i << '\n'; std::cout << res.first[i].states << " unique states visited\n"; + std::cout << res.first[i].inserted << " unique states inserted\n"; std::cout << res.first[i].transitions << " transitions explored\n"; std::cout << res.first[i].sccs << " sccs found\n"; @@ -670,6 +672,7 @@ static int checked_main() sccs += res.first[i].sccs; st += res.first[i].states; tr += res.first[i].transitions; + inserted += res.first[i].inserted; if (mc_options.csv) { @@ -679,6 +682,7 @@ static int checked_main() std::cout << "@th_" << i << ',' << res.first[i].walltime << ',' << res.first[i].states << ',' + << res.first[i].inserted << ',' << res.first[i].transitions << ',' << res.first[i].sccs << std::endl; @@ -690,6 +694,7 @@ static int checked_main() std::cout << "\nSummary :\n"; std::cout << "Find following the csv: " << "model,walltimems,memused," + << "inserted_states," << "cumulated_states,cumulated_transitions," << "cumulated_sccs\n"; @@ -698,6 +703,7 @@ static int checked_main() << ',' << tm.timer("bloemen").walltime() << ',' << memused << ',' + << inserted << ',' << st << ',' << tr << ',' << sccs