Commit ac86b0e4 authored by Etienne Renault's avatar Etienne Renault
Browse files

mc: bloemen count unique states

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