...
 
Commits (22)
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2013, 2014, 2016, 2017, 2019 Laboratoire
// Copyright (C) 2009, 2010, 2013, 2014, 2016, 2017, 2019, 2020 Laboratoire
// de Recherche et Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
......@@ -58,7 +58,7 @@ namespace spot
void recycle(SuccIterator*, unsigned tid);
/// \brief This method allow to deallocate a given state.
const std::vector<std::string> get_ap();
const std::vector<std::string> ap();
};
#ifndef SWIG
......@@ -68,7 +68,7 @@ namespace spot
/// a given parameter is of type kripkecube. It also check
/// if the iterator has the good interface.
template <typename T, typename State, typename SuccIter>
class is_a_kripkecube_ptr
class SPOT_API is_a_kripkecube_ptr
{
private:
using yes = std::true_type;
......@@ -84,7 +84,7 @@ namespace spot
std::is_same<SuccIter*, decltype(u->succ(State(), 0))>::value &&
std::is_same<void, decltype(u->recycle(nullptr, 0))>::value &&
std::is_same<const std::vector<std::string>,
decltype(u->get_ap())>::value &&
decltype(u->ap())>::value &&
std::is_same<void, decltype(u->recycle(nullptr, 0))>::value &&
// Check the SuccIterator
......@@ -94,8 +94,7 @@ namespace spot
std::is_same<spot::cube, decltype(v->condition())>::value
// finally return the type "yes"
, yes()
);
, yes());
// For all other cases return the type "no"
template<typename, typename> static no test_kripke(...);
......
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement de
// l'Epita (LRDE)
// Copyright (C) 2017, 2018, 2019, 2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
......@@ -221,7 +221,7 @@ namespace spot
void recycle(cspins_iterator* it, unsigned tid);
/// \brief List the atomic propositions used by *this* kripke
const std::vector<std::string> get_ap();
const std::vector<std::string> ap();
/// \brief The number of thread used by *this* kripke
unsigned get_threads();
......
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
// Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement de
// l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
......@@ -302,7 +302,7 @@ namespace spot
}
const std::vector<std::string>
kripkecube<cspins_state, cspins_iterator>::get_ap()
kripkecube<cspins_state, cspins_iterator>::ap()
{
return aps_;
}
......
## -*- coding: utf-8 -*-
## Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement de
## l'Epita (LRDE).
## Copyright (C) 2015, 2016, 2017, 2019, 2020 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
##
......@@ -21,8 +21,8 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc
mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\
mc.hh deadlock.hh bloemen.hh cndfs.hh
mc_HEADERS = intersect.hh lpar13.hh unionfind.hh utils.hh mc.hh\
mc_instanciator.hh deadlock.hh bloemen.hh bloemen_ec.hh cndfs.hh
noinst_LTLIBRARIES = libmc.la
......
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et
// Copyright (C) 2015, 2016, 2017, 2018, 2019, 2020 Laboratoire de Recherche et
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
......@@ -21,15 +21,18 @@
#include <atomic>
#include <chrono>
#include <spot/bricks/brick-hashset>
#include <stdlib.h>
#include <thread>
#include <vector>
#include <utility>
#include <spot/misc/common.hh>
#include <spot/bricks/brick-hashset>
#include <spot/kripke/kripke.hh>
#include <spot/misc/common.hh>
#include <spot/misc/fixpool.hh>
#include <spot/misc/timer.hh>
#include <spot/twacube/twacube.hh>
#include <spot/twacube/fwd.hh>
#include <spot/mc/mc.hh>
namespace spot
{
......@@ -405,16 +408,6 @@ namespace spot
fixed_size_pool<pool_type::Unsafe> p_; ///< \brief The allocator
};
/// \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
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.
......@@ -426,24 +419,36 @@ namespace spot
swarmed_bloemen() = delete;
public:
swarmed_bloemen(kripkecube<State, SuccIterator>& sys,
iterable_uf<State, StateHash, StateEqual>& uf,
unsigned tid):
sys_(sys), uf_(uf), tid_(tid),
nb_th_(std::thread::hardware_concurrency())
using uf = iterable_uf<State, StateHash, StateEqual>;
using uf_element = typename uf::uf_element;
using shared_struct = uf;
using shared_map = typename uf::shared_map;
static shared_struct* make_shared_structure(shared_map m, unsigned i)
{
return new uf(m, i);
}
swarmed_bloemen(kripkecube<State, SuccIterator>& sys,
twacube_ptr, /* useless here */
shared_map& map, /* useless here */
iterable_uf<State, StateHash, StateEqual>* uf,
unsigned tid,
std::atomic<bool>& stop):
sys_(sys), uf_(*uf), tid_(tid),
nb_th_(std::thread::hardware_concurrency()),
stop_(stop)
{
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value,
"error: does not match the kripkecube requirements");
}
using uf = iterable_uf<State, StateHash, StateEqual>;
using uf_element = typename uf::uf_element;
void run()
{
tm_.start("DFS thread " + std::to_string(tid_));
setup();
State init = sys_.initial(tid_);
auto pair = uf_.make_claim(init);
todo_.push_back(pair.second);
......@@ -453,7 +458,7 @@ namespace spot
while (!todo_.empty())
{
bloemen_recursive_start:
while (true)
while (!stop_.load(std::memory_order_relaxed))
{
bool sccfound = false;
uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
......@@ -496,17 +501,63 @@ namespace spot
Rp_.pop_back();
todo_.pop_back();
}
finalize();
}
void setup()
{
tm_.start("DFS thread " + std::to_string(tid_));
}
void finalize()
{
bool tst_val = false;
bool new_val = true;
bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
if (exchanged)
finisher_ = true;
tm_.stop("DFS thread " + std::to_string(tid_));
}
bool finisher()
{
return finisher_;
}
unsigned states()
{
return states_;
}
unsigned transitions()
{
return transitions_;
}
unsigned walltime()
{
return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
}
bloemen_stats stats()
std::string name()
{
return "bloemen_scc";
}
int sccs()
{
return sccs_;
}
mc_rvalue result()
{
return mc_rvalue::SUCCESS;
}
std::string trace()
{
return {uf_.inserted(), states_, transitions_, sccs_, walltime()};
// Returning a trace has no sense in this algorithm
return "";
}
private:
......@@ -521,5 +572,7 @@ namespace spot
unsigned transitions_ = 0; ///< \brief Number of transitions visited
unsigned sccs_ = 0; ///< \brief Number of SCC visited
spot::timer_map tm_; ///< \brief Time execution
std::atomic<bool>& stop_;
bool finisher_ = false;
};
}
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et
// Copyright (C) 2015, 2016, 2017, 2018, 2019, 2020 Laboratoire de Recherche et
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
......@@ -31,6 +31,9 @@
#include <spot/misc/fixpool.hh>
#include <spot/misc/timer.hh>
#include <spot/twacube/twacube.hh>
#include <spot/twacube/fwd.hh>
#include <spot/mc/intersect.hh>
#include <spot/mc/mc.hh>
namespace spot
{
......@@ -100,7 +103,6 @@ namespace spot
using shared_map = brick::hashset::FastConcurrent <uf_element*,
uf_element_hasher>;
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),
......@@ -446,17 +448,6 @@ namespace spot
fixed_size_pool<pool_type::Unsafe> 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.
......@@ -466,12 +457,24 @@ namespace spot
{
public:
using uf = iterable_uf_ec<State, StateHash, StateEqual>;
using uf_element = typename uf::uf_element;
using shared_struct = uf;
using shared_map = typename uf::shared_map;
static shared_struct* make_shared_structure(shared_map m, unsigned i)
{
return new uf(m, i);
}
swarmed_bloemen_ec(kripkecube<State, SuccIterator>& sys,
twacube_ptr twa,
iterable_uf_ec<State, StateHash, StateEqual>& uf,
shared_map& map, /* useless here */
iterable_uf_ec<State, StateHash, StateEqual>* uf,
unsigned tid,
std::atomic<bool>& stop):
sys_(sys), twa_(twa), uf_(uf), tid_(tid),
sys_(sys), twa_(twa), uf_(*uf), tid_(tid),
nb_th_(std::thread::hardware_concurrency()),
stop_(stop)
{
......@@ -480,12 +483,9 @@ namespace spot
"error: does not match the kripkecube requirements");
}
using uf = iterable_uf_ec<State, StateHash, StateEqual>;
using uf_element = typename uf::uf_element;
void run()
{
tm_.start("DFS thread " + std::to_string(tid_));
setup();
State init_kripke = sys_.initial(tid_);
unsigned init_twa = twa_->get_initial();
auto pair = uf_.make_claim(init_kripke, init_twa);
......@@ -509,7 +509,7 @@ namespace spot
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);
forward_iterators(sys_, twa_, it_kripke, it_prop, true, tid_);
while (!it_kripke->done())
{
auto w = uf_.make_claim(it_kripke->state(),
......@@ -558,7 +558,8 @@ namespace spot
return;
}
}
forward_iterators(it_kripke, it_prop, false);
forward_iterators(sys_, twa_, it_kripke, it_prop,
false, tid_);
}
uf_.remove_from_list(v_prime);
sys_.recycle(it_kripke, tid_);
......@@ -568,53 +569,37 @@ namespace spot
Rp_.pop_back();
todo_.pop_back();
}
finalize();
}
void setup()
{
tm_.start("DFS thread " + std::to_string(tid_));
}
void finalize()
{
bool tst_val = false;
bool new_val = true;
bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
if (exchanged)
finisher_ = true;
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<trans_index> it_prop,
bool just_pushed)
bool finisher()
{
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();
return finisher_;
}
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 states()
{
return states_;
}
unsigned transitions()
{
return transitions_;
}
unsigned walltime()
......@@ -622,15 +607,19 @@ namespace spot
return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
}
bool is_empty()
std::string name()
{
return "bloemen_ec";
}
int sccs()
{
return is_empty_;
return sccs_;
}
bloemen_ec_stats stats()
mc_rvalue result()
{
return {uf_.inserted(), states_, transitions_, sccs_, is_empty_,
walltime()};
return is_empty_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY;
}
std::string trace()
......@@ -653,5 +642,6 @@ namespace spot
bool is_empty_ = true;
spot::timer_map tm_; ///< \brief Time execution
std::atomic<bool>& stop_;
bool finisher_ = false;
};
}
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et
// Copyright (C) 2015, 2016, 2017, 2018, 2019, 2020 Laboratoire de Recherche et
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
......@@ -29,22 +29,13 @@
#include <spot/misc/fixpool.hh>
#include <spot/misc/timer.hh>
#include <spot/twacube/twacube.hh>
#include <spot/mc/mc.hh>
namespace spot
{
/// \brief This object is returned by the algorithm below
struct SPOT_API cndfs_stats
{
unsigned states; ///< \brief Number of states visited
unsigned transitions; ///< \brief Number of transitions visited
unsigned instack_dfs; ///< \brief Maximum DFS stack
bool is_empty; ///< \brief Is the model empty
unsigned walltime; ///< \brief Walltime for this thread in ms
};
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
class swarmed_cndfs
class SPOT_API swarmed_cndfs
{
struct local_colors
{
......@@ -95,7 +86,7 @@ namespace spot
}
};
struct todo__element
struct todo_element
{
product_state st;
SuccIterator* it_kripke;
......@@ -108,9 +99,16 @@ namespace spot
///< \brief Shortcut to ease shared map manipulation
using shared_map = brick::hashset::FastConcurrent <product_state,
state_hasher>;
using shared_struct = shared_map;
static shared_struct* make_shared_structure(shared_map m, unsigned i)
{
return nullptr; // Useless here.
}
swarmed_cndfs(kripkecube<State, SuccIterator>& sys, twacube_ptr twa,
shared_map& map, unsigned tid, std::atomic<bool>& stop):
shared_map& map, shared_struct* /* useless here*/,
unsigned tid, std::atomic<bool>& stop):
sys_(sys), twa_(twa), tid_(tid), map_(map),
nb_th_(std::thread::hardware_concurrency()),
p_colors_(sizeof(cndfs_colors) +
......@@ -120,6 +118,7 @@ namespace spot
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value,
"error: does not match the kripkecube requirements");
SPOT_ASSERT(nb_th_ > tid);
}
virtual ~swarmed_cndfs()
......@@ -136,6 +135,13 @@ namespace spot
}
}
void run()
{
setup();
blue_dfs();
finalize();
}
void setup()
{
tm_.start("DFS thread " + std::to_string(tid_));
......@@ -180,17 +186,6 @@ namespace spot
return {true, *it};
}
bool pop_blue()
{
// Track maximum dfs size
dfs_ = todo_blue_.size() > dfs_ ? todo_blue_.size() : dfs_;
todo_blue_.back().st.colors->l[tid_].cyan = false;
sys_.recycle(todo_blue_.back().it_kripke, tid_);
todo_blue_.pop_back();
return true;
}
std::pair<bool, product_state>
push_red(product_state s, bool ignore_cyan)
{
......@@ -216,6 +211,17 @@ namespace spot
return {true, *it};
}
bool pop_blue()
{
// Track maximum dfs size
dfs_ = todo_blue_.size() > dfs_ ? todo_blue_.size() : dfs_;
todo_blue_.back().st.colors->l[tid_].cyan = false;
sys_.recycle(todo_blue_.back().it_kripke, tid_);
todo_blue_.pop_back();
return true;
}
bool pop_red()
{
// Track maximum dfs size
......@@ -230,9 +236,19 @@ namespace spot
void finalize()
{
bool tst_val = false;
bool new_val = true;
bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
if (exchanged)
finisher_ = true;
tm_.stop("DFS thread " + std::to_string(tid_));
}
bool finisher()
{
return finisher_;
}
unsigned states()
{
return states_;
......@@ -243,13 +259,73 @@ namespace spot
return transitions_;
}
void run()
unsigned walltime()
{
setup();
blue_dfs();
finalize();
return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
}
std::string name()
{
return "cndfs";
}
int sccs()
{
return -1;
}
mc_rvalue result()
{
return is_empty_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY;
}
std::string trace()
{
SPOT_ASSERT(!is_empty_);
StateEqual equal;
auto state_equal = [equal](product_state a, product_state b)
{
return a.st_prop == b.st_prop
&& equal(a.st_kripke, b.st_kripke);
};
std::string res = "Prefix:\n";
auto it = todo_blue_.begin();
while (it != todo_blue_.end())
{
if (state_equal(((*it)).st, cycle_start_))
break;
res += " " + std::to_string(((*it)).st.st_prop)
+ "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
++it;
}
res += "Cycle:\n";
while (it != todo_blue_.end())
{
res += " " + std::to_string(((*it)).st.st_prop)
+ "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
++it;
}
if (!todo_red_.empty())
{
it = todo_red_.begin() + 1; // skip first element, also in blue
while (it != todo_red_.end())
{
res += " " + std::to_string(((*it)).st.st_prop)
+ "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
++it;
}
}
res += " " + std::to_string(cycle_start_.st_prop)
+ "*" + sys_.to_string(cycle_start_.st_kripke) + "\n";
return res;
}
private:
void blue_dfs()
{
product_state initial = {sys_.initial(tid_),
......@@ -262,7 +338,8 @@ namespace spot
if (todo_blue_.back().it_prop->done())
return;
forward_iterators(todo_blue_, true);
forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
todo_blue_.back().it_prop, true, tid_);
while (!todo_blue_.empty() && !stop_.load(std::memory_order_relaxed))
{
......@@ -278,11 +355,13 @@ namespace spot
};
bool acc = (bool) twa_->trans_storage(current.it_prop, tid_).acc_;
forward_iterators(todo_blue_, false);
forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
todo_blue_.back().it_prop, false, tid_);
auto tmp = push_blue(s, acc);
if (tmp.first)
forward_iterators(todo_blue_, true);
forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
todo_blue_.back().it_prop, true, tid_);
else if (acc)
{
// The state cyan and we can reach it throught an
......@@ -324,14 +403,14 @@ namespace spot
void post_red_dfs()
{
for (product_state& s : Rp_acc_)
for (product_state& s: Rp_acc_)
{
while (s.colors->red.load() && !stop_.load())
{
// await
}
}
for (product_state& s : Rp_)
for (product_state& s: Rp_)
{
s.colors->red.store(true);
s.colors->l[tid_].is_in_Rp = false; // empty Rp
......@@ -349,7 +428,8 @@ namespace spot
if (!init_push.first)
return;
forward_iterators(todo_red_, true);
forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
todo_red_.back().it_prop, true, tid_);
while (!todo_red_.empty() && !stop_.load(std::memory_order_relaxed))
{
......@@ -364,12 +444,14 @@ namespace spot
nullptr
};
bool acc = (bool) twa_->trans_storage(current.it_prop, tid_).acc_;
forward_iterators(todo_red_, false);
forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
todo_red_.back().it_prop, false, tid_);
auto res = push_red(s, false);
if (res.first) // could push properly
{
forward_iterators(todo_red_, true);
forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
todo_red_.back().it_prop, true, tid_);
SPOT_ASSERT(res.second.colors->blue);
......@@ -419,130 +501,23 @@ namespace spot
}
}
std::string trace()
{
SPOT_ASSERT(!is_empty());
StateEqual equal;
auto state_equal = [equal](product_state a, product_state b)
{
return a.st_prop == b.st_prop
&& equal(a.st_kripke, b.st_kripke);
};
std::string res = "Prefix:\n";
auto it = todo_blue_.begin();
while (it != todo_blue_.end())
{
if (state_equal(((*it)).st, cycle_start_))
break;
res += " " + std::to_string(((*it)).st.st_prop)
+ "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
++it;
}
res += "Cycle:\n";
while (it != todo_blue_.end())
{
res += " " + std::to_string(((*it)).st.st_prop)
+ "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
++it;
}
if (!todo_red_.empty())
{
it = todo_red_.begin() + 1; // skip first element, also in blue
while (it != todo_red_.end())
{
res += " " + std::to_string(((*it)).st.st_prop)
+ "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
++it;
}
}
res += " " + std::to_string(cycle_start_.st_prop)
+ "*" + sys_.to_string(cycle_start_.st_kripke) + "\n";
return res;
}
bool is_empty()
{
return is_empty_;
}
unsigned walltime()
{
return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
}
cndfs_stats stats()
{
return {states(), transitions(), dfs_, is_empty(), walltime()};
}
protected:
void forward_iterators(std::vector<todo__element>& todo, bool just_pushed)
{
SPOT_ASSERT(!todo.empty());
auto top = todo.back();
SPOT_ASSERT(!(top.it_prop->done() &&
top.it_kripke->done()));
// Sometimes kripke state may have no successors.
if (top.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(!(top.it_prop->done()));
if (just_pushed && twa_->get_cubeset()
.intersect(twa_->trans_data(top.it_prop, tid_).cube_,
top.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 (top.it_prop->done())
top.it_prop->reset();
else
top.it_prop->next();
while (!top.it_kripke->done())
{
while (!top.it_prop->done())
{
if (twa_->get_cubeset()
.intersect(twa_->trans_data(top.it_prop, tid_).cube_,
top.it_kripke->condition()))
return;
top.it_prop->next();
}
top.it_prop->reset();
top.it_kripke->next();
}
}
private:
kripkecube<State, SuccIterator>& sys_;
twacube_ptr twa_;
std::vector<todo__element> todo_blue_;
std::vector<todo__element> todo_red_;
unsigned transitions_ = 0; ///< \brief Number of transitions
unsigned tid_; ///< \brief Thread's current ID
kripkecube<State, SuccIterator>& sys_; ///< \brief The system to check
twacube_ptr twa_; ///< \brief The propertu to check
std::vector<todo_element> todo_blue_; ///< \brief Blue Stack
std::vector<todo_element> todo_red_; ///< \ brief Red Stack
unsigned transitions_ = 0; ///< \brief Number of transitions
unsigned tid_; ///< \brief Thread's current ID
shared_map map_; ///< \brief Map shared by threads
spot::timer_map tm_; ///< \brief Time execution
unsigned states_ = 0; ///< \brief Number of states
unsigned dfs_ = 0; ///< \brief Maximum DFS stack size
/// \brief Maximum number of threads that can be handled by this algorithm
unsigned nb_th_ = 0;
fixed_size_pool<pool_type::Unsafe> p_colors_;
bool is_empty_ = true; ///< \brief Accepting cycle detected?
unsigned nb_th_ = 0; /// \brief Maximum number of threads
fixed_size_pool<pool_type::Unsafe> p_colors_; /// \brief Memory pool
bool is_empty_ = true; ///< \brief Accepting cycle detected?
std::atomic<bool>& stop_; ///< \brief Stop-the-world boolean
std::vector<product_state> Rp_;
std::vector<product_state> Rp_acc_;
product_state cycle_start_;
std::vector<product_state> Rp_; ///< \brief Rp stack
std::vector<product_state> Rp_acc_; ///< \brief Rp acc stack
product_state cycle_start_; ///< \brief Begining of a cycle
bool finisher_ = false;
};
}
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et
// Copyright (C) 2015, 2016, 2017, 2018, 2019, 2020 Laboratoire de Recherche et
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
......@@ -29,25 +29,21 @@
#include <spot/kripke/kripke.hh>
#include <spot/misc/fixpool.hh>
#include <spot/misc/timer.hh>
#include <spot/twacube/twacube.hh>
#include <spot/twacube/fwd.hh>
#include <spot/mc/mc.hh>
namespace spot
{
/// \brief This object is returned by the algorithm below
struct SPOT_API deadlock_stats
{
unsigned states; ///< \brief Number of states visited
unsigned transitions; ///< \brief Number of transitions visited
unsigned instack_dfs; ///< \brief Maximum DFS stack
bool has_deadlock; ///< \brief Does the model contains a deadlock
unsigned walltime; ///< \brief Walltime for this thread in ms
};
/// \brief This class aims to explore a model to detect wether it
/// contains a deadlock. This deadlock detection performs a DFS traversal
/// sharing information shared among multiple threads.
/// If Deadlock equals std::true_type performs dealock algorithm,
/// otherwise perform a simple reachability.
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
class swarmed_deadlock
typename StateHash, typename StateEqual,
typename Deadlock>
class SPOT_API swarmed_deadlock
{
/// \brief Describes the status of a state
enum st_status
......@@ -89,14 +85,26 @@ namespace spot
}
};
static constexpr bool compute_deadlock =
std::is_same<std::true_type, Deadlock>::value;
public:
///< \brief Shortcut to ease shared map manipulation
using shared_map = brick::hashset::FastConcurrent <deadlock_pair*,
pair_hasher>;
using shared_struct = shared_map;
static shared_struct* make_shared_structure(shared_map, unsigned)
{
return nullptr; // Useless
}
swarmed_deadlock(kripkecube<State, SuccIterator>& sys,
shared_map& map, unsigned tid, std::atomic<bool>& stop):
twacube_ptr, /* useless here */
shared_map& map, shared_struct* /* useless here */,
unsigned tid,
std::atomic<bool>& stop):
sys_(sys), tid_(tid), map_(map),
nb_th_(std::thread::hardware_concurrency()),
p_(sizeof(int)*std::thread::hardware_concurrency()),
......@@ -106,6 +114,7 @@ namespace spot
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value,
"error: does not match the kripkecube requirements");
SPOT_ASSERT(nb_th_ > tid);
}
virtual ~swarmed_deadlock()
......@@ -117,6 +126,46 @@ namespace spot
}
}
void run()
{
setup();
State initial = sys_.initial(tid_);
if (SPOT_LIKELY(push(initial)))
{
todo_.push_back({initial, sys_.succ(initial, tid_), transitions_});
}
while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
{
if (todo_.back().it->done())
{
if (SPOT_LIKELY(pop()))
{
deadlock_ = todo_.back().current_tr == transitions_;
if (compute_deadlock && deadlock_)
break;
sys_.recycle(todo_.back().it, tid_);
todo_.pop_back();
}
}
else
{
++transitions_;
State dst = todo_.back().it->state();
if (SPOT_LIKELY(push(dst)))
{
todo_.back().it->next();
todo_.push_back({dst, sys_.succ(dst, tid_), transitions_});
}
else
{
todo_.back().it->next();
}
}
}
finalize();
}
void setup()
{
tm_.start("DFS thread " + std::to_string(tid_));
......@@ -173,10 +222,19 @@ namespace spot
void finalize()
{
stop_ = true;
bool tst_val = false;
bool new_val = true;
bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
if (exchanged)
finisher_ = true;
tm_.stop("DFS thread " + std::to_string(tid_));
}
bool finisher()
{
return finisher_;
}
unsigned states()
{
return states_;
......@@ -187,72 +245,49 @@ namespace spot
return transitions_;
}
void run()
unsigned walltime()
{
setup();
State initial = sys_.initial(tid_);
if (SPOT_LIKELY(push(initial)))
{
todo_.push_back({initial, sys_.succ(initial, tid_), transitions_});
}
while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
{
if (todo_.back().it->done())
{
if (SPOT_LIKELY(pop()))
{
deadlock_ = todo_.back().current_tr == transitions_;
if (deadlock_)
break;
sys_.recycle(todo_.back().it, tid_);
todo_.pop_back();
}
}
else
{
++transitions_;
State dst = todo_.back().it->state();
return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
}
if (SPOT_LIKELY(push(dst)))
{
todo_.back().it->next();
todo_.push_back({dst, sys_.succ(dst, tid_), transitions_});
}
else
{
todo_.back().it->next();
}
}
}
finalize();
std::string name()
{
if (compute_deadlock)
return "deadlock";
return "reachability";
}
bool has_deadlock()
int sccs()
{
return deadlock_;
return -1;
}
unsigned walltime()
mc_rvalue result()
{
return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
if (compute_deadlock)
return deadlock_ ? mc_rvalue::DEADLOCK : mc_rvalue::NO_DEADLOCK;
return mc_rvalue::SUCCESS;
}
deadlock_stats stats()
std::string trace()
{
return {states(), transitions(), dfs_, has_deadlock(), walltime()};
std::string result;
for (auto& e: todo_)
result += sys_.to_string(e.s, tid_);
return result;
}
private:
struct todo__element
struct todo_element
{
State s;
SuccIterator* it;
unsigned current_tr;
};
kripkecube<State, SuccIterator>& sys_; ///< \brief The system to check
std::vector<todo__element> todo_; ///< \brief The DFS stack
unsigned transitions_ = 0; ///< \brief Number of transitions
unsigned tid_; ///< \brief Thread's current ID
std::vector<todo_element> todo_; ///< \brief The DFS stack
unsigned transitions_ = 0; ///< \brief Number of transitions
unsigned tid_; ///< \brief Thread's current ID
shared_map map_; ///< \brief Map shared by threads
spot::timer_map tm_; ///< \brief Time execution
unsigned states_ = 0; ///< \brief Number of states
......@@ -266,5 +301,6 @@ namespace spot
/// \brief Stack that grows according to the todo stack. It avoid multiple
/// concurent access to the shared map.
std::vector<int*> refs_;
bool finisher_ = false;
};
}
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2018, 2019 Laboratoire de Recherche et
// Copyright (C) 2015, 2016, 2018, 2019, 2020 Laboratoire de Recherche et
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
......@@ -25,251 +25,54 @@
namespace spot
{
/// \brief Wrapper to accumulate results from intersection
/// and emptiness checks
struct SPOT_API istats
/// \brief Find the first couple of iterator (from a given pair of
/// interators) that intersect. This method can be used in any
/// DFS/BFS-like exploration algorithm. The \a parameter indicates
/// wheter the state has just been visited since the underlying job
/// is slightly different.
template<typename SuccIterator, typename State>
static void forward_iterators(kripkecube<State, SuccIterator>& sys,
twacube_ptr twa,
SuccIterator* it_kripke,
std::shared_ptr<trans_index> it_prop,
bool just_visited,
unsigned tid)
{
unsigned states;
unsigned transitions;
unsigned sccs;
unsigned instack_sccs;
unsigned instack_item;
bool is_empty;
};
/// \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
/// hooks to the various emptiness checks.
/// Actually, we use "mixins templates" in order to efficiently
/// call emptiness check procedure. This means that we add
/// a template \a EmptinessCheck that will be called though
/// four functions:
/// - setup: called before any operation
/// - push: called for every new state
/// - pop: called every time a state leave the DFS stack
/// - update: called for every closing edge
/// - trace: must return a counterexample (if exists)
///
/// The other template parameters allows to consider any kind
/// of state (and so any kind of kripke structures).
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual,
typename EmptinessCheck>
class SPOT_API intersect
{
public:
intersect(const intersect<State, SuccIterator, StateHash,
StateEqual, EmptinessCheck>& i) = default;
intersect(kripkecube<State, SuccIterator>& sys,
twacube_ptr twa, unsigned tid, bool& stop):
sys_(sys), twa_(twa), tid_(tid), stop_(stop)
{
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value,
"error: does not match the kripkecube requirements");
map.reserve(2000000);
todo.reserve(100000);
}
~intersect()
{
map.clear();
}
/// \brief In order to implement "mixin paradigm", we
/// must be abble to access the acual definition of
/// the emptiness check that, in turn, has to access
/// local variables.
EmptinessCheck& self()
{
return static_cast<EmptinessCheck&>(*this);
}
/// \brief The main function that will perform the
/// product on-the-fly and call the emptiness check
/// when necessary.
bool run()
{
self().setup();
product_state initial = {sys_.initial(tid_), twa_->get_initial()};
if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, {})))
{
todo.push_back({initial, sys_.succ(initial.st_kripke, tid_),
twa_->succ(initial.st_prop)});
// Not going further! It's a product with a single state.
if (todo.back().it_prop->done())
return false;
forward_iterators(true);
map[initial] = ++dfs_number;
}
while (!todo.empty() && !stop_)
{
// Check the kripke is enough since it's the outer loop. More
// details in forward_iterators.
if (todo.back().it_kripke->done())
{
bool is_init = todo.size() == 1;
auto newtop = is_init? todo.back().st: todo[todo.size() -2].st;
if (SPOT_LIKELY(self().pop_state(todo.back().st,
map[todo.back().st],
is_init,
newtop,
map[newtop])))
{
sys_.recycle(todo.back().it_kripke, tid_);
// FIXME a local storage for twacube iterator?
todo.pop_back();
if (SPOT_UNLIKELY(self().counterexample_found()))
return true;
}
}
else
{
++transitions;
product_state dst = {
todo.back().it_kripke->state(),
twa_->trans_storage(todo.back().it_prop, tid_).dst
};
auto acc = twa_->trans_data(todo.back().it_prop, tid_).acc_;
forward_iterators(false);
auto it = map.find(dst);
if (it == map.end())
{
if (SPOT_LIKELY(self().push_state(dst, dfs_number+1, acc)))
{
map[dst] = ++dfs_number;
todo.push_back({dst, sys_.succ(dst.st_kripke, tid_),
twa_->succ(dst.st_prop)});
forward_iterators(true);
}
}
else if (SPOT_UNLIKELY(self().update(todo.back().st,
dfs_number,
dst, map[dst], acc)))
return true;
}
}
return false;
}
unsigned int states()
{
return dfs_number;
}
unsigned int trans()
{
return transitions;
}
std::string counterexample()
{
return self().trace();
}
virtual istats stats()
{
return {dfs_number, transitions, 0U, 0U, 0U, false};
}
protected:
/// \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(bool just_pushed)
{
SPOT_ASSERT(!todo.empty());
SPOT_ASSERT(!(todo.back().it_prop->done() &&
todo.back().it_kripke->done()));
// Sometimes kripke state may have no successors.
if (todo.back().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(!(todo.back().it_prop->done()));
if (just_pushed && twa_->get_cubeset()
.intersect(twa_->trans_data(todo.back().it_prop, tid_).cube_,
todo.back().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 (todo.back().it_prop->done())
todo.back().it_prop->reset();
else
todo.back().it_prop->next();
while (!todo.back().it_kripke->done())
{
while (!todo.back().it_prop->done())
{
if (SPOT_UNLIKELY(twa_->get_cubeset()
.intersect(twa_->trans_data(todo.back().it_prop, tid_).cube_,
todo.back().it_kripke->condition())))
return;
todo.back().it_prop->next();
}
todo.back().it_prop->reset();
todo.back().it_kripke->next();
}
}
public:
struct product_state
{
State st_kripke;
unsigned st_prop;
};
struct product_state_equal
{
bool
operator()(const product_state lhs,
const product_state rhs) const
{
StateEqual equal;
return (lhs.st_prop == rhs.st_prop) &&
equal(lhs.st_kripke, rhs.st_kripke);
}
};
struct product_state_hash
{
size_t
operator()(const product_state that) const noexcept
(void) sys; // System is useless, but the API is clearer
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 visited and the 2 iterators intersect.
// There is no need to move iterators forward.
SPOT_ASSERT(!(it_prop->done()));
if (just_visited && 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())
{
// FIXME! wang32_hash(that.st_prop) could have
// been pre-calculated!
StateHash hasher;
return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
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();
}
};
struct todo_element
{
product_state st;
SuccIterator* it_kripke;
std::shared_ptr<trans_index> it_prop;
};
kripkecube<State, SuccIterator>& sys_;
twacube_ptr twa_;
std::vector<todo_element> todo;
typedef std::unordered_map<const product_state, int,
product_state_hash,
product_state_equal> visited_map;
visited_map map;
unsigned int dfs_number = 0;
unsigned int transitions = 0;
unsigned tid_;
bool& stop_; // Do not need to be atomic.
};
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et
// Copyright (C) 2015, 2016, 2018, 2019, 2020 Laboratoire de Recherche et
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
......@@ -22,6 +22,10 @@
#include <spot/twa/acc.hh>
#include <spot/mc/unionfind.hh>
#include <spot/mc/intersect.hh>
#include <spot/mc/mc.hh>
#include <spot/misc/timer.hh>
#include <spot/twacube/twacube.hh>
#include <spot/twacube/fwd.hh>
namespace spot
{
......@@ -32,50 +36,148 @@ namespace spot
/// the Gabow's one.
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
class ec_renault13lpar : public intersect<State, SuccIterator,
StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>
class SPOT_API lpar13
{
// Ease the manipulation
using typename intersect<State, SuccIterator, StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash,
StateEqual>>::product_state;
struct product_state
{
State st_kripke;
unsigned st_prop;
};
struct product_state_equal
{
bool
operator()(const product_state lhs,
const product_state rhs) const
{
StateEqual equal;
return (lhs.st_prop == rhs.st_prop) &&
equal(lhs.st_kripke, rhs.st_kripke);
}