diff --git a/spot/mc/bloemen_ec.hh b/spot/mc/bloemen_ec.hh
new file mode 100644
index 000000000..f3412e4dc
--- /dev/null
+++ b/spot/mc/bloemen_ec.hh
@@ -0,0 +1,655 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et
+// Developpement de l'Epita
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program. If not, see .
+
+#pragma once
+
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+
+namespace spot
+{
+ template
+ class iterable_uf_ec
+ {
+
+ public:
+ enum class uf_status { LIVE, LOCK, DEAD };
+ enum class list_status { BUSY, LOCK, DONE };
+ enum class claim_status { CLAIM_FOUND, CLAIM_NEW, CLAIM_DEAD };
+
+ /// \brief Represents a Union-Find element
+ struct uf_element
+ {
+ /// \brief the kripke state handled by the element
+ State st_kripke;
+ /// \brief the prop state handled by the element
+ unsigned st_prop;
+ /// \brief acceptance conditions of the union
+ acc_cond::mark_t acc;
+ /// \brief mutex for acceptance condition
+ std::mutex acc_mutex_;
+ /// \brief reference to the pointer
+ std::atomic parent;
+ /// The set of worker for a given state
+ std::atomic worker_;
+ /// \brief next element for work stealing
+ std::atomic next_;
+ /// \brief current status for the element
+ std::atomic uf_status_;
+ ///< \brief current status for the list
+ std::atomic list_status_;
+ };
+
+ /// \brief The haser for the previous uf_element.
+ struct uf_element_hasher
+ {
+ uf_element_hasher(const uf_element*)
+ { }
+
+ uf_element_hasher() = default;
+
+ brick::hash::hash128_t
+ hash(const uf_element* lhs) const
+ {
+ StateHash hash;
+ // Not modulo 31 according to brick::hashset specifications.
+ unsigned u = hash(lhs->st_kripke) % (1<<30);
+ u = wang32_hash(lhs->st_prop) ^ u;
+ u = u % (1<<30);
+ return {u, u};
+ }
+
+ bool equal(const uf_element* lhs,
+ const uf_element* rhs) const
+ {
+ StateEqual equal;
+ return (lhs->st_prop == rhs->st_prop)
+ && equal(lhs->st_kripke, rhs->st_kripke);
+ }
+ };
+
+ ///< \brief Shortcut to ease shared map manipulation
+ using shared_map = brick::hashset::FastConcurrent ;
+
+
+ iterable_uf_ec(shared_map& map, unsigned tid):
+ map_(map), tid_(tid), size_(std::thread::hardware_concurrency()),
+ nb_th_(std::thread::hardware_concurrency()), inserted_(0),
+ p_(sizeof(uf_element))
+ {
+ }
+
+ ~iterable_uf_ec() {}
+
+ std::pair
+ make_claim(State kripke, unsigned prop)
+ {
+ unsigned w_id = (1U << tid_);
+
+ // Setup and try to insert the new state in the shared map.
+ uf_element* v = (uf_element*) p_.allocate();
+ new (v) (uf_element); // required, otherwise the mutex is unitialized
+ v->st_kripke = kripke;
+ v->st_prop = prop;
+ v->acc = {};
+ v->parent = v;
+ v->next_ = v;
+ v->worker_ = 0;
+ v->uf_status_ = uf_status::LIVE;
+ v->list_status_ = list_status::BUSY;
+
+ auto it = map_.insert({v});
+ bool b = it.isnew();
+
+ // Insertion failed, delete element
+ // FIXME Should we add a local cache to avoid useless allocations?
+ if (!b)
+ p_.deallocate(v);
+ else
+ ++inserted_;
+
+ uf_element* a_root = find(*it);
+ if (a_root->uf_status_.load() == uf_status::DEAD)
+ return {claim_status::CLAIM_DEAD, *it};
+
+ if ((a_root->worker_.load() & w_id) != 0)
+ return {claim_status::CLAIM_FOUND, *it};
+
+ atomic_fetch_or(&(a_root->worker_), w_id);
+ while (a_root->parent.load() != a_root)
+ {
+ a_root = find(a_root);
+ atomic_fetch_or(&(a_root->worker_), w_id);
+ }
+
+ return {claim_status::CLAIM_NEW, *it};
+ }
+
+ uf_element* find(uf_element* a)
+ {
+ uf_element* parent = a->parent.load();
+ uf_element* x = a;
+ uf_element* y;
+
+ while (x != parent)
+ {
+ y = parent;
+ parent = y->parent.load();
+ if (parent == y)
+ return y;
+ x->parent.store(parent);
+ x = parent;
+ parent = x->parent.load();
+ }
+ return x;
+ }
+
+ bool sameset(uf_element* a, uf_element* b)
+ {
+ while (true)
+ {
+ uf_element* a_root = find(a);
+ uf_element* b_root = find(b);
+ if (a_root == b_root)
+ return true;
+
+ if (a_root->parent.load() == a_root)
+ return false;
+ }
+ }
+
+ bool lock_root(uf_element* a)
+ {
+ uf_status expected = uf_status::LIVE;
+ if (a->uf_status_.load() == expected)
+ {
+ if (std::atomic_compare_exchange_strong
+ (&(a->uf_status_), &expected, uf_status::LOCK))
+ {
+ if (a->parent.load() == a)
+ return true;
+ unlock_root(a);
+ }
+ }
+ return false;
+ }
+
+ inline void unlock_root(uf_element* a)
+ {
+ a->uf_status_.store(uf_status::LIVE);
+ }
+
+ uf_element* lock_list(uf_element* a)
+ {
+ uf_element* a_list = a;
+ while (true)
+ {
+ bool dontcare = false;
+ a_list = pick_from_list(a_list, &dontcare);
+ if (a_list == nullptr)
+ {
+ return nullptr;
+ }
+
+ auto expected = list_status::BUSY;
+ bool b = std::atomic_compare_exchange_strong
+ (&(a_list->list_status_), &expected, list_status::LOCK);
+
+ if (b)
+ return a_list;
+
+ a_list = a_list->next_.load();
+ }
+ }
+
+ void unlock_list(uf_element* a)
+ {
+ a->list_status_.store(list_status::BUSY);
+ }
+
+ acc_cond::mark_t
+ unite(uf_element* a, uf_element* b, acc_cond::mark_t acc)
+ {
+ uf_element* a_root;
+ uf_element* b_root;
+ uf_element* q;
+ uf_element* r;
+
+ while (true)
+ {
+ a_root = find(a);
+ b_root = find(b);
+
+ if (a_root == b_root)
+ {
+ // Update acceptance condition
+ {
+ std::lock_guard rlock(a_root->acc_mutex_);
+ a_root->acc |= acc;
+ acc |= a_root->acc;
+ }
+
+ while (a_root->parent.load() != a_root)
+ {
+ a_root = find(a_root);
+ std::lock_guard rlock(a_root->acc_mutex_);
+ a_root->acc |= acc;
+ acc |= a_root->acc;
+ }
+ return acc;
+ }
+
+ r = std::max(a_root, b_root);
+ q = std::min(a_root, b_root);
+
+ if (!lock_root(q))
+ continue;
+
+ break;
+ }
+
+ uf_element* a_list = lock_list(a);
+ if (a_list == nullptr)
+ {
+ unlock_root(q);
+ return acc;
+ }
+
+ uf_element* b_list = lock_list(b);
+ if (b_list == nullptr)
+ {
+ unlock_list(a_list);
+ unlock_root(q);
+ return acc;
+ }
+
+ SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK);
+ SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK);
+
+ // Swapping
+ uf_element* a_next = a_list->next_.load();
+ uf_element* b_next = b_list->next_.load();
+ SPOT_ASSERT(a_next != nullptr);
+ SPOT_ASSERT(b_next != nullptr);
+
+ a_list->next_.store(b_next);
+ b_list->next_.store(a_next);
+ q->parent.store(r);
+
+ // Update workers
+ unsigned q_worker = q->worker_.load();
+ unsigned r_worker = r->worker_.load();
+ if ((q_worker|r_worker) != r_worker)
+ {
+ atomic_fetch_or(&(r->worker_), q_worker);
+ while (r->parent.load() != r)
+ {
+ r = find(r);
+ atomic_fetch_or(&(r->worker_), q_worker);
+ }
+ }
+
+ // Update acceptance condition
+ {
+ std::lock_guard rlock(r->acc_mutex_);
+ std::lock_guard qlock(q->acc_mutex_);
+ q->acc |= acc;
+ r->acc |= q->acc;
+ acc |= r->acc;
+ }
+
+ while (r->parent.load() != r)
+ {
+ r = find(r);
+ std::lock_guard rlock(r->acc_mutex_);
+ std::lock_guard qlock(q->acc_mutex_);
+ r->acc |= q->acc;
+ acc |= r->acc;
+ }
+
+ unlock_list(a_list);
+ unlock_list(b_list);
+ unlock_root(q);
+ return acc;
+ }
+
+ uf_element* pick_from_list(uf_element* u, bool* sccfound)
+ {
+ uf_element* a = u;
+ while (true)
+ {
+ list_status a_status;
+ while (true)
+ {
+ a_status = a->list_status_.load();
+
+ if (a_status == list_status::BUSY)
+ {
+ return a;
+ }
+
+ if (a_status == list_status::DONE)
+ break;
+ }
+
+ uf_element* b = a->next_.load();
+
+ // ------------------------------ NO LAZY : start
+ // if (b == u)
+ // {
+ // uf_element* a_root = find(a);
+ // uf_status status = a_root->uf_status_.load();
+ // while (status != uf_status::DEAD)
+ // {
+ // if (status == uf_status::LIVE)
+ // *sccfound = std::atomic_compare_exchange_strong
+ // (&(a_root->uf_status_), &status, uf_status::DEAD);
+ // status = a_root->uf_status_.load();
+ // }
+ // return nullptr;
+ // }
+ // a = b;
+ // ------------------------------ NO LAZY : end
+
+ if (a == b)
+ {
+ uf_element* a_root = find(u);
+ uf_status status = a_root->uf_status_.load();
+ while (status != uf_status::DEAD)
+ {
+ if (status == uf_status::LIVE)
+ *sccfound = std::atomic_compare_exchange_strong
+ (&(a_root->uf_status_), &status, uf_status::DEAD);
+ status = a_root->uf_status_.load();
+ }
+ return nullptr;
+ }
+
+ list_status b_status;
+ while (true)
+ {
+ b_status = b->list_status_.load();
+
+ if (b_status == list_status::BUSY)
+ {
+ return b;
+ }
+
+ if (b_status == list_status::DONE)
+ break;
+ }
+
+ SPOT_ASSERT(b_status == list_status::DONE);
+ SPOT_ASSERT(a_status == list_status::DONE);
+
+ uf_element* c = b->next_.load();
+ a->next_.store(c);
+ a = c;
+ }
+ }
+
+ void remove_from_list(uf_element* a)
+ {
+ while (true)
+ {
+ list_status a_status = a->list_status_.load();
+
+ if (a_status == list_status::DONE)
+ break;
+
+ if (a_status == list_status::BUSY)
+ std::atomic_compare_exchange_strong
+ (&(a->list_status_), &a_status, list_status::DONE);
+ }
+ }
+
+ 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
+ fixed_size_pool p_; ///< \brief The allocator
+ };
+
+ /// \brief This object is returned by the algorithm below
+ struct SPOT_API bloemen_ec_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
+ bool is_empty; ///< \brief Is the model empty
+ unsigned walltime; ///< \brief Walltime for this thread in ms
+ };
+
+ /// \brief This class implements the SCC decomposition algorithm of bloemen
+ /// as described in PPOPP'16. It uses a shared union-find augmented to manage
+ /// work stealing between threads.
+ template
+ class swarmed_bloemen_ec
+ {
+ public:
+
+ swarmed_bloemen_ec(kripkecube& sys,
+ twacube_ptr twa,
+ iterable_uf_ec& uf,
+ unsigned tid,
+ std::atomic& stop):
+ sys_(sys), twa_(twa), uf_(uf), tid_(tid),
+ nb_th_(std::thread::hardware_concurrency()),
+ stop_(stop)
+ {
+ SPOT_ASSERT(is_a_kripkecube(sys));
+ }
+
+ using uf = iterable_uf_ec;
+ using uf_element = typename uf::uf_element;
+
+ void run()
+ {
+ tm_.start("DFS thread " + std::to_string(tid_));
+ State init_kripke = sys_.initial(tid_);
+ unsigned init_twa = twa_->get_initial();
+ auto pair = uf_.make_claim(init_kripke, init_twa);
+ todo_.push_back(pair.second);
+ Rp_.push_back(pair.second);
+ ++states_;
+
+ while (!todo_.empty())
+ {
+ bloemen_recursive_start:
+ while (!stop_.load(std::memory_order_relaxed))
+ {
+ bool sccfound = false;
+ uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
+ if (v_prime == nullptr)
+ {
+ // The SCC has been explored!
+ sccs_ += sccfound;
+ break;
+ }
+
+ auto it_kripke = sys_.succ(v_prime->st_kripke, tid_);
+ auto it_prop = twa_->succ(v_prime->st_prop);
+ forward_iterators(it_kripke, it_prop, true);
+ while (!it_kripke->done())
+ {
+ auto w = uf_.make_claim(it_kripke->state(),
+ twa_->trans_storage(it_prop, tid_)
+ .dst);
+ auto trans_acc = twa_->trans_storage(it_prop, tid_).acc_;
+ ++transitions_;
+ if (w.first == uf::claim_status::CLAIM_NEW)
+ {
+ todo_.push_back(w.second);
+ Rp_.push_back(w.second);
+ ++states_;
+ sys_.recycle(it_kripke, tid_);
+ goto bloemen_recursive_start;
+ }
+ else if (w.first == uf::claim_status::CLAIM_FOUND)
+ {
+ acc_cond::mark_t scc_acc = trans_acc;
+
+ // This operation is mandatory to update acceptance marks.
+ // Otherwise, when w.second and todo.back() are
+ // already in the same set, the acceptance condition will
+ // not be added.
+ scc_acc |= uf_.unite(w.second, w.second, scc_acc);
+
+ while (!uf_.sameset(todo_.back(), w.second))
+ {
+ uf_element* r = Rp_.back();
+ Rp_.pop_back();
+ uf_.unite(r, Rp_.back(), scc_acc);
+ }
+
+
+ {
+ auto root = uf_.find(w.second);
+ std::lock_guard lock(w.second->acc_mutex_);
+ scc_acc = w.second->acc;
+ }
+
+ // cycle found in SCC and it contains acceptance condition
+ if (twa_->acc().accepting(scc_acc))
+ {
+ stop_ = true;
+ is_empty_ = false;
+ tm_.stop("DFS thread " + std::to_string(tid_));
+ return;
+ }
+ }
+ forward_iterators(it_kripke, it_prop, false);
+ }
+ uf_.remove_from_list(v_prime);
+ sys_.recycle(it_kripke, tid_);
+ }
+
+ if (todo_.back() == Rp_.back())
+ Rp_.pop_back();
+ todo_.pop_back();
+ }
+ tm_.stop("DFS thread " + std::to_string(tid_));
+ }
+
+ /// \brief Find the first couple of iterator (from the top of the
+ /// todo stack) that intersect. The \a parameter indicates wheter
+ /// the state has just been pushed since the underlying job is
+ /// slightly different.
+ void forward_iterators(SuccIterator* it_kripke,
+ std::shared_ptr it_prop,
+ bool just_pushed)
+ {
+ SPOT_ASSERT(!(it_prop->done() &&
+ it_kripke->done()));
+
+ // Sometimes kripke state may have no successors.
+ if (it_kripke->done())
+ return;
+
+ // The state has just been push and the 2 iterators intersect.
+ // There is no need to move iterators forward.
+ SPOT_ASSERT(!(it_prop->done()));
+ if (just_pushed && twa_->get_cubeset()
+ .intersect(twa_->trans_data(it_prop, tid_).cube_,
+ it_kripke->condition()))
+ return;
+
+ // Otherwise we have to compute the next valid successor (if it exits).
+ // This requires two loops. The most inner one is for the twacube since
+ // its costless
+ if (it_prop->done())
+ it_prop->reset();
+ else
+ it_prop->next();
+
+ while (!it_kripke->done())
+ {
+ while (!it_prop->done())
+ {
+ if (SPOT_UNLIKELY(twa_->get_cubeset()
+ .intersect(twa_->trans_data(it_prop, tid_).cube_,
+ it_kripke->condition())))
+ return;
+ it_prop->next();
+ }
+ it_prop->reset();
+ it_kripke->next();
+ }
+ }
+
+ unsigned walltime()
+ {
+ return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
+ }
+
+ bool is_empty()
+ {
+ return is_empty_;
+ }
+
+ bloemen_ec_stats stats()
+ {
+ return {uf_.inserted(), states_, transitions_, sccs_, is_empty_,
+ walltime()};
+ }
+
+ std::string trace()
+ {
+ return "Not implemented";
+ }
+
+ private:
+ kripkecube& sys_; ///< \brief The system to check
+ twacube_ptr twa_; ///< \brief The formula to check
+ std::vector todo_; ///< \brief The "recursive" stack
+ std::vector Rp_; ///< \brief The DFS stack
+ iterable_uf_ec 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
+ bool is_empty_ = true;
+ spot::timer_map tm_; ///< \brief Time execution
+ std::atomic& stop_;
+ };
+}
diff --git a/spot/mc/mc.hh b/spot/mc/mc.hh
index e9a1fbad0..4140b9ec2 100644
--- a/spot/mc/mc.hh
+++ b/spot/mc/mc.hh
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
+// Copyright (C) 2015, 2016, 2017, 2019 Laboratoire de Recherche et
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
@@ -29,6 +29,7 @@
#include
#include
#include
+#include
#include
#include
@@ -232,4 +233,98 @@ namespace spot
}
return std::make_pair(stats, tm);
}
+
+ /// \brief Perform the SCC computation algorithm of bloemen.16.ppopp
+ /// with emptiness check
+ template
+ static std::tuple,
+ spot::timer_map>
+ bloemen_ec(kripke_ptr sys, spot::twacube_ptr prop, bool compute_ctrx = false)
+ {
+ spot::timer_map tm;
+ using algo_name = spot::swarmed_bloemen_ec;
+ using uf_name = spot::iterable_uf_ec;
+
+ unsigned nbth = sys->get_threads();
+ typename uf_name::shared_map map;
+
+ tm.start("Initialisation");
+ std::vector swarmed(nbth);
+ std::vector ufs(nbth);
+ std::atomic stop(false);
+ for (unsigned i = 0; i < nbth; ++i)
+ {
+ ufs[i] = new uf_name(map, i);
+ swarmed[i] = new algo_name(*sys, prop, *ufs[i], i, stop);
+ }
+ tm.stop("Initialisation");
+
+ std::mutex iomutex;
+ std::atomic barrier(true);
+ std::vector threads(nbth);
+ for (unsigned i = 0; i < nbth; ++i)
+ {
+ threads[i] = std::thread ([&swarmed, &iomutex, i, & barrier]
+ {
+#if defined(unix) || defined(__unix__) || defined(__unix)
+ {
+ std::lock_guard iolock(iomutex);
+ std::cout << "Thread #" << i
+ << ": on CPU " << sched_getcpu() << '\n';
+ }
+#endif
+
+ // Wait all threads to be instanciated.
+ while (barrier)
+ continue;
+ swarmed[i]->run();
+ });
+
+#if defined(unix) || defined(__unix__) || defined(__unix)
+ // Pins threads to a dedicated core.
+ cpu_set_t cpuset;
+ CPU_ZERO(&cpuset);
+ CPU_SET(i, &cpuset);
+ int rc = pthread_setaffinity_np(threads[i].native_handle(),
+ sizeof(cpu_set_t), &cpuset);
+ if (rc != 0)
+ {
+ std::lock_guard iolock(iomutex);
+ std::cerr << "Error calling pthread_setaffinity_np: " << rc << '\n';
+ }
+#endif
+ }
+
+ tm.start("Run");
+ barrier.store(false);
+
+ for (auto& t : threads)
+ t.join();
+ tm.stop("Run");
+
+ std::string trace;
+ std::vector stats;
+ bool is_empty = true;
+ for (unsigned i = 0; i < sys->get_threads(); ++i)
+ {
+ if (!swarmed[i]->is_empty())
+ {
+ is_empty = false;
+ if (compute_ctrx)
+ trace = swarmed[i]->trace();
+ }
+
+ stats.push_back(swarmed[i]->stats());
+ }
+
+ for (unsigned i = 0; i < nbth; ++i)
+ {
+ delete swarmed[i];
+ delete ufs[i];
+ }
+ return std::make_tuple(is_empty, trace, stats, tm);
+ }
}
diff --git a/tests/ltsmin/check.test b/tests/ltsmin/check.test
index bd94c83d6..659799fae 100755
--- a/tests/ltsmin/check.test
+++ b/tests/ltsmin/check.test
@@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
-# Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire de Recherche
+# Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017, 2019 Laboratoire de Recherche
# et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -91,3 +91,5 @@ run 0 ../modelcheck --model beem-peterson.4.dve2C \
--csv --bloemen -p 3 >stdout
test `grep "#" stdout | awk -F',' '{print $7}'` -eq 29115
+run 0 ../modelcheck --model beem-peterson.4.dve2C \
+ --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv --bloemen-ec -p 3 >stdout
diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc
index a96576a29..d283dc3c7 100644
--- a/tests/ltsmin/modelcheck.cc
+++ b/tests/ltsmin/modelcheck.cc
@@ -74,6 +74,7 @@ struct mc_options_
bool csv = false;
bool has_deadlock = false;
bool bloemen = false;
+ bool bloemen_ec = false;
} mc_options;
@@ -86,6 +87,9 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
case CSV:
mc_options.csv = true;
break;
+ case 'B':
+ mc_options.bloemen_ec = true;
+ break;
case 'b':
mc_options.bloemen = true;
break;
@@ -150,6 +154,8 @@ static const argp_option options[] =
{ "model", 'm', "STRING", 0, "use the model stored in file STRING", 0 },
// ------------------------------------------------------------
{ nullptr, 0, nullptr, 0, "Process options:", 2 },
+ { "bloemen-ec", 'B', nullptr, 0,
+ "run the SCC computation of Bloemen et al. (PPOPP'16) with EC", 0},
{ "bloemen", 'b', nullptr, 0,
"run the SCC computation of Bloemen et al. (PPOPP'16)", 0 },
{ "counterexample", 'c', nullptr, 0,
@@ -297,7 +303,8 @@ static int checked_main()
if (mc_options.nb_threads == 1 &&
mc_options.formula != nullptr &&
- mc_options.model != nullptr)
+ mc_options.model != nullptr &&
+ !mc_options.bloemen_ec)
{
product = spot::otf_product(model, prop);
@@ -409,7 +416,8 @@ static int checked_main()
if (mc_options.nb_threads != 1 &&
mc_options.formula != nullptr &&
- mc_options.model != nullptr)
+ mc_options.model != nullptr &&
+ !mc_options.bloemen_ec)
{
unsigned int hc = std::thread::hardware_concurrency();
if (mc_options.nb_threads > hc)
@@ -711,6 +719,126 @@ static int checked_main()
}
}
+ if (mc_options.bloemen_ec
+ && mc_options.model != nullptr && mc_options.formula != nullptr)
+ {
+ unsigned int hc = std::thread::hardware_concurrency();
+ if (mc_options.nb_threads > hc)
+ std::cerr << "Warning: you require " << mc_options.nb_threads
+ << " threads, but your computer only support " << hc
+ << ". This could slow down parallel algorithms.\n";
+
+ tm.start("twa to twacube");
+ auto propcube = spot::twa_to_twacube(prop);
+ tm.stop("twa to twacube");
+
+ tm.start("load kripkecube");
+ spot::ltsmin_kripkecube_ptr modelcube = nullptr;
+ try
+ {
+ modelcube = spot::ltsmin_model::load(mc_options.model)
+ .kripkecube(propcube->get_ap(), deadf, mc_options.compress,
+ mc_options.nb_threads);
+ }
+ catch (const std::runtime_error& e)
+ {
+ std::cerr << e.what() << '\n';
+ }
+ tm.stop("load kripkecube");
+
+ int memused = spot::memusage();
+ tm.start("bloemen emptiness check");
+ auto res = spot::bloemen_ec
+ (modelcube, propcube);
+ tm.stop("bloemen emptiness check");
+ memused = spot::memusage() - memused;
+
+ if (!modelcube)
+ {
+ exit_code = 2;
+ goto safe_exit;
+ }
+
+ // Display statistics
+ unsigned sccs = 0;
+ unsigned st = 0;
+ unsigned tr = 0;
+ unsigned inserted = 0;
+ for (unsigned i = 0; i < std::get<2>(res).size(); ++i)
+ {
+ std::cout << "\n---- Thread number : " << i << '\n';
+ std::cout << std::get<2>(res)[i].states
+ << " unique states visited\n";
+ std::cout << std::get<2>(res)[i].inserted
+ << " unique states inserted\n";
+ std::cout << std::get<2>(res)[i].transitions
+ << " transitions explored\n";
+ std::cout << std::get<2>(res)[i].sccs << " sccs found\n";
+ std::cout << std::get<2>(res)[i].walltime
+ << " milliseconds\n";
+
+ sccs += std::get<2>(res)[i].sccs;
+ st += std::get<2>(res)[i].states;
+ tr += std::get<2>(res)[i].transitions;
+ inserted += std::get<2>(res)[i].inserted;
+
+ if (mc_options.csv)
+ {
+ std::cout << "Find following the csv: "
+ << "thread_id,walltimems,type,"
+ << "states,transitions,sccs\n";
+ std::cout << "@th_" << i << ','
+ << std::get<2>(res)[i].walltime << ','
+ << (std::get<2>(res)[i].is_empty ?
+ "EMPTY," : "NONEMPTY,")
+ << std::get<2>(res)[i].states << ','
+ << std::get<2>(res)[i].inserted << ','
+ << std::get<2>(res)[i].transitions << ','
+ << std::get<2>(res)[i].sccs
+ << std::endl;
+ }
+ }
+
+ if (mc_options.csv)
+ {
+ std::cout << "\nSummary :\n";
+ if (std::get<0>(res))
+ std::cout << "no accepting run found\n";
+ else if (!mc_options.compute_counterexample)
+ {
+ std::cout << "an accepting run exists "
+ << "(use -c to print it)" << std::endl;
+ exit_code = 1;
+ }
+ else
+ std::cout << "an accepting run exists\n"
+ << std::get<1>(res) << '\n';
+
+
+ std::cout << "Find following the csv: "
+ << "model,walltimems,memused,"
+ << "type,inserted_states,"
+ << "cumulated_states,cumulated_transitions,"
+ << "cumulated_sccs\n";
+
+ std::cout << '#'
+ << split_filename(mc_options.model)
+ << ','
+ << tm.timer("bloemen emptiness check").walltime() << ','
+ << memused << ','
+ << (std::get<0>(res) ? "EMPTY," : "NONEMPTY,")
+ << inserted << ','
+ << st << ','
+ << tr << ','
+ << sccs
+ << '\n';
+ }
+ }
+
safe_exit:
if (mc_options.use_timer)
tm.print(std::cout);