alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

mc: bloemen count unique states

Browse source 
* spot/mc/bloemen.hh, tests/ltsmin/modelcheck.cc: here.
This commit is contained in:
Etienne Renault 2017-11-21 13:39:12 +01:00
parent 80746e4332
commit 63a4b4085a
2 changed files with 18 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

14
spot/mc/bloemen.hh
View file

@ -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<State, StateHash, StateEqual> 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

6
tests/ltsmin/modelcheck.cc
View file

@ -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