...
 
Commits (22)
// -*- coding: utf-8 -*- // -*- 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 // de Recherche et Developpement de l'Epita
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -58,7 +58,7 @@ namespace spot ...@@ -58,7 +58,7 @@ namespace spot
void recycle(SuccIterator*, unsigned tid); void recycle(SuccIterator*, unsigned tid);
/// \brief This method allow to deallocate a given state. /// \brief This method allow to deallocate a given state.
const std::vector<std::string> get_ap(); const std::vector<std::string> ap();
}; };
#ifndef SWIG #ifndef SWIG
...@@ -68,7 +68,7 @@ namespace spot ...@@ -68,7 +68,7 @@ namespace spot
/// a given parameter is of type kripkecube. It also check /// a given parameter is of type kripkecube. It also check
/// if the iterator has the good interface. /// if the iterator has the good interface.
template <typename T, typename State, typename SuccIter> template <typename T, typename State, typename SuccIter>
class is_a_kripkecube_ptr class SPOT_API is_a_kripkecube_ptr
{ {
private: private:
using yes = std::true_type; using yes = std::true_type;
...@@ -84,7 +84,7 @@ namespace spot ...@@ -84,7 +84,7 @@ namespace spot
std::is_same<SuccIter*, decltype(u->succ(State(), 0))>::value && std::is_same<SuccIter*, decltype(u->succ(State(), 0))>::value &&
std::is_same<void, decltype(u->recycle(nullptr, 0))>::value && std::is_same<void, decltype(u->recycle(nullptr, 0))>::value &&
std::is_same<const std::vector<std::string>, 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 && std::is_same<void, decltype(u->recycle(nullptr, 0))>::value &&
// Check the SuccIterator // Check the SuccIterator
...@@ -94,8 +94,7 @@ namespace spot ...@@ -94,8 +94,7 @@ namespace spot
std::is_same<spot::cube, decltype(v->condition())>::value std::is_same<spot::cube, decltype(v->condition())>::value
// finally return the type "yes" // finally return the type "yes"
, yes() , yes());
);
// For all other cases return the type "no" // For all other cases return the type "no"
template<typename, typename> static no test_kripke(...); template<typename, typename> static no test_kripke(...);
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement de // Copyright (C) 2017, 2018, 2019, 2020 Laboratoire de Recherche et
// l'Epita (LRDE) // Développement de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -221,7 +221,7 @@ namespace spot ...@@ -221,7 +221,7 @@ namespace spot
void recycle(cspins_iterator* it, unsigned tid); void recycle(cspins_iterator* it, unsigned tid);
/// \brief List the atomic propositions used by *this* kripke /// \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 /// \brief The number of thread used by *this* kripke
unsigned get_threads(); unsigned get_threads();
......
// -*- coding: utf-8 -*- // -*- 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) // l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -302,7 +302,7 @@ namespace spot ...@@ -302,7 +302,7 @@ namespace spot
} }
const std::vector<std::string> const std::vector<std::string>
kripkecube<cspins_state, cspins_iterator>::get_ap() kripkecube<cspins_state, cspins_iterator>::ap()
{ {
return aps_; return aps_;
} }
......
## -*- coding: utf-8 -*- ## -*- coding: utf-8 -*-
## Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement de ## Copyright (C) 2015, 2016, 2017, 2019, 2020 Laboratoire de Recherche et
## l'Epita (LRDE). ## Développement de l'Epita (LRDE).
## ##
## This file is part of Spot, a model checking library. ## This file is part of Spot, a model checking library.
## ##
...@@ -21,8 +21,8 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) ...@@ -21,8 +21,8 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc mcdir = $(pkgincludedir)/mc
mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\ mc_HEADERS = intersect.hh lpar13.hh unionfind.hh utils.hh mc.hh\
mc.hh deadlock.hh bloemen.hh cndfs.hh mc_instanciator.hh deadlock.hh bloemen.hh bloemen_ec.hh cndfs.hh
noinst_LTLIBRARIES = libmc.la noinst_LTLIBRARIES = libmc.la
......
// -*- coding: utf-8 -*- // -*- 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 // Developpement de l'Epita
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -21,15 +21,18 @@ ...@@ -21,15 +21,18 @@
#include <atomic> #include <atomic>
#include <chrono> #include <chrono>
#include <spot/bricks/brick-hashset>
#include <stdlib.h> #include <stdlib.h>
#include <thread> #include <thread>
#include <vector> #include <vector>
#include <utility> #include <utility>
#include <spot/misc/common.hh> #include <spot/bricks/brick-hashset>
#include <spot/kripke/kripke.hh> #include <spot/kripke/kripke.hh>
#include <spot/misc/common.hh>
#include <spot/misc/fixpool.hh> #include <spot/misc/fixpool.hh>
#include <spot/misc/timer.hh> #include <spot/misc/timer.hh>
#include <spot/twacube/twacube.hh>
#include <spot/twacube/fwd.hh>
#include <spot/mc/mc.hh>
namespace spot namespace spot
{ {
...@@ -405,16 +408,6 @@ namespace spot ...@@ -405,16 +408,6 @@ namespace spot
fixed_size_pool<pool_type::Unsafe> p_; ///< \brief The allocator 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 /// \brief This class implements the SCC decomposition algorithm of bloemen
/// as described in PPOPP'16. It uses a shared union-find augmented to manage /// as described in PPOPP'16. It uses a shared union-find augmented to manage
/// work stealing between threads. /// work stealing between threads.
...@@ -426,24 +419,36 @@ namespace spot ...@@ -426,24 +419,36 @@ namespace spot
swarmed_bloemen() = delete; swarmed_bloemen() = delete;
public: public:
swarmed_bloemen(kripkecube<State, SuccIterator>& sys,
iterable_uf<State, StateHash, StateEqual>& uf, using uf = iterable_uf<State, StateHash, StateEqual>;
unsigned tid): using uf_element = typename uf::uf_element;
sys_(sys), uf_(uf), tid_(tid),
nb_th_(std::thread::hardware_concurrency()) 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), static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value, State, SuccIterator>::value,
"error: does not match the kripkecube requirements"); "error: does not match the kripkecube requirements");
} }
using uf = iterable_uf<State, StateHash, StateEqual>;
using uf_element = typename uf::uf_element;
void run() void run()
{ {
tm_.start("DFS thread " + std::to_string(tid_)); setup();
State init = sys_.initial(tid_); State init = sys_.initial(tid_);
auto pair = uf_.make_claim(init); auto pair = uf_.make_claim(init);
todo_.push_back(pair.second); todo_.push_back(pair.second);
...@@ -453,7 +458,7 @@ namespace spot ...@@ -453,7 +458,7 @@ namespace spot
while (!todo_.empty()) while (!todo_.empty())
{ {
bloemen_recursive_start: bloemen_recursive_start:
while (true) while (!stop_.load(std::memory_order_relaxed))
{ {
bool sccfound = false; bool sccfound = false;
uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound); uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
...@@ -496,17 +501,63 @@ namespace spot ...@@ -496,17 +501,63 @@ namespace spot
Rp_.pop_back(); Rp_.pop_back();
todo_.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_)); tm_.stop("DFS thread " + std::to_string(tid_));
} }
bool finisher()
{
return finisher_;
}
unsigned states()
{
return states_;
}
unsigned transitions()
{
return transitions_;
}
unsigned walltime() unsigned walltime()
{ {
return tm_.timer("DFS thread " + std::to_string(tid_)).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: private:
...@@ -521,5 +572,7 @@ namespace spot ...@@ -521,5 +572,7 @@ namespace spot
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
spot::timer_map tm_; ///< \brief Time execution spot::timer_map tm_; ///< \brief Time execution
std::atomic<bool>& stop_;
bool finisher_ = false;
}; };
} }
// -*- coding: utf-8 -*- // -*- 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 // Developpement de l'Epita
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -31,6 +31,9 @@ ...@@ -31,6 +31,9 @@
#include <spot/misc/fixpool.hh> #include <spot/misc/fixpool.hh>
#include <spot/misc/timer.hh> #include <spot/misc/timer.hh>
#include <spot/twacube/twacube.hh> #include <spot/twacube/twacube.hh>
#include <spot/twacube/fwd.hh>
#include <spot/mc/intersect.hh>
#include <spot/mc/mc.hh>
namespace spot namespace spot
{ {
...@@ -100,7 +103,6 @@ namespace spot ...@@ -100,7 +103,6 @@ namespace spot
using shared_map = brick::hashset::FastConcurrent <uf_element*, using shared_map = brick::hashset::FastConcurrent <uf_element*,
uf_element_hasher>; uf_element_hasher>;
iterable_uf_ec(shared_map& map, unsigned tid): iterable_uf_ec(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()), inserted_(0), nb_th_(std::thread::hardware_concurrency()), inserted_(0),
...@@ -446,17 +448,6 @@ namespace spot ...@@ -446,17 +448,6 @@ namespace spot
fixed_size_pool<pool_type::Unsafe> p_; ///< \brief The allocator 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 /// \brief This class implements the SCC decomposition algorithm of bloemen
/// as described in PPOPP'16. It uses a shared union-find augmented to manage /// as described in PPOPP'16. It uses a shared union-find augmented to manage
/// work stealing between threads. /// work stealing between threads.
...@@ -466,12 +457,24 @@ namespace spot ...@@ -466,12 +457,24 @@ namespace spot
{ {
public: 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, swarmed_bloemen_ec(kripkecube<State, SuccIterator>& sys,
twacube_ptr twa, twacube_ptr twa,
iterable_uf_ec<State, StateHash, StateEqual>& uf, shared_map& map, /* useless here */
iterable_uf_ec<State, StateHash, StateEqual>* uf,
unsigned tid, unsigned tid,
std::atomic<bool>& stop): 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()), nb_th_(std::thread::hardware_concurrency()),
stop_(stop) stop_(stop)
{ {
...@@ -480,12 +483,9 @@ namespace spot ...@@ -480,12 +483,9 @@ namespace spot
"error: does not match the kripkecube requirements"); "error: does not match the kripkecube requirements");
} }
using uf = iterable_uf_ec<State, StateHash, StateEqual>;
using uf_element = typename uf::uf_element;
void run() void run()
{ {
tm_.start("DFS thread " + std::to_string(tid_)); setup();
State init_kripke = sys_.initial(tid_); State init_kripke = sys_.initial(tid_);
unsigned init_twa = twa_->get_initial(); unsigned init_twa = twa_->get_initial();
auto pair = uf_.make_claim(init_kripke, init_twa); auto pair = uf_.make_claim(init_kripke, init_twa);
...@@ -509,7 +509,7 @@ namespace spot ...@@ -509,7 +509,7 @@ namespace spot
auto it_kripke = sys_.succ(v_prime->st_kripke, tid_); auto it_kripke = sys_.succ(v_prime->st_kripke, tid_);
auto it_prop = twa_->succ(v_prime->st_prop); 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()) while (!it_kripke->done())
{ {
auto w = uf_.make_claim(it_kripke->state(), auto w = uf_.make_claim(it_kripke->state(),
...@@ -558,7 +558,8 @@ namespace spot ...@@ -558,7 +558,8 @@ namespace spot
return; return;
} }
} }
forward_iterators(it_kripke, it_prop, false); forward_iterators(sys_, twa_, it_kripke, it_prop,
false, tid_);
} }
uf_.remove_from_list(v_prime); uf_.remove_from_list(v_prime);
sys_.recycle(it_kripke, tid_); sys_.recycle(it_kripke, tid_);
...@@ -568,53 +569,37 @@ namespace spot ...@@ -568,53 +569,37 @@ namespace spot
Rp_.pop_back(); Rp_.pop_back();
todo_.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_)); tm_.stop("DFS thread " + std::to_string(tid_));
} }
/// \brief Find the first couple of iterator (from the top of the bool finisher()
/// 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)
{ {
SPOT_ASSERT(!(it_prop->done() && return finisher_;
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()) unsigned states()
{ {
while (!it_prop->done()) return states_;
{ }
if (SPOT_UNLIKELY(twa_->get_cubeset()
.intersect(twa_->trans_data(it_prop, tid_).cube_, unsigned transitions()
it_kripke->condition()))) {
return; return transitions_;
it_prop->next();
}
it_prop->reset();
it_kripke->next();
}
} }
unsigned walltime() unsigned walltime()
...@@ -622,15 +607,19 @@ namespace spot ...@@ -622,15 +607,19 @@ namespace spot
return tm_.timer("DFS thread " + std::to_string(tid_)).walltime(); 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_, return is_empty_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY;
walltime()};
} }
std::string trace() std::string trace()
...@@ -653,5 +642,6 @@ namespace spot ...@@ -653,5 +642,6 @@ namespace spot
bool is_empty_ = true; bool is_empty_ = true;
spot::timer_map tm_; ///< \brief Time execution spot::timer_map tm_; ///< \brief Time execution
std::atomic<bool>& stop_; std::atomic<bool>& stop_;
bool finisher_ = false;
}; };
} }
This diff is collapsed.
// -*- coding: utf-8 -*- // -*- 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 // Developpement de l'Epita
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -29,25 +29,21 @@ ...@@ -29,25 +29,21 @@
#include <spot/kripke/kripke.hh> #include <spot/kripke/kripke.hh>
#include <spot/misc/fixpool.hh> #include <spot/misc/fixpool.hh>
#include <spot/misc/timer.hh> #include <spot/misc/timer.hh>
#include <spot/twacube/twacube.hh>
#include <spot/twacube/fwd.hh>
#include <spot/mc/mc.hh>
namespace spot 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 /// \brief This class aims to explore a model to detect wether it
/// contains a deadlock. This deadlock detection performs a DFS traversal /// contains a deadlock. This deadlock detection performs a DFS traversal
/// sharing information shared among multiple threads. /// 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, template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual> typename StateHash, typename StateEqual,
class swarmed_deadlock typename Deadlock>
class SPOT_API swarmed_deadlock
{ {
/// \brief Describes the status of a state /// \brief Describes the status of a state
enum st_status enum st_status
...@@ -89,14 +85,26 @@ namespace spot ...@@ -89,14 +85,26 @@ namespace spot
} }
}; };
static constexpr bool compute_deadlock =
std::is_same<std::true_type, Deadlock>::value;
public: public:
///< \brief Shortcut to ease shared map manipulation ///< \brief Shortcut to ease shared map manipulation
using shared_map = brick::hashset::FastConcurrent <deadlock_pair*, using shared_map = brick::hashset::FastConcurrent <deadlock_pair*,
pair_hasher>; 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, 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), sys_(sys), tid_(tid), map_(map),
nb_th_(std::thread::hardware_concurrency()), nb_th_(std::thread::hardware_concurrency()),
p_(sizeof(int)*std::thread::hardware_concurrency()), p_(sizeof(int)*std::thread::hardware_concurrency()),
...@@ -106,6 +114,7 @@ namespace spot ...@@ -106,6 +114,7 @@ namespace spot
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys), static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value, State, SuccIterator>::value,
"error: does not match the kripkecube requirements"); "error: does not match the kripkecube requirements");
SPOT_ASSERT(nb_th_ > tid);
} }
virtual ~swarmed_deadlock() virtual ~swarmed_deadlock()
...@@ -117,6 +126,46 @@ namespace spot ...@@ -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() void setup()
{ {
tm_.start("DFS thread " + std::to_string(tid_)); tm_.start("DFS thread " + std::to_string(tid_));
...@@ -173,10 +222,19 @@ namespace spot ...@@ -173,10 +222,19 @@ namespace spot
void finalize() 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_)); tm_.stop("DFS thread " + std::to_string(tid_));
} }
bool finisher()
{
return finisher_;
}
unsigned states() unsigned states()
{ {
return states_; return states_;
...@@ -187,72 +245,49 @@ namespace spot ...@@ -187,72 +245,49 @@ namespace spot
return transitions_; return transitions_;
} }
void run() unsigned walltime()
{ {
setup(); return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
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();
if (SPOT_LIKELY(push(dst))) std::string name()
{ {
todo_.back().it->next(); if (compute_deadlock)
todo_.push_back({dst, sys_.succ(dst, tid_), transitions_}); return "deadlock";
} return "reachability";
else
{
todo_.back().it->next();
}
}
}
finalize();
} }
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: private:
struct todo__element struct todo_element
{ {
State s; State s;
SuccIterator* it; SuccIterator* it;
unsigned current_tr; unsigned current_tr;
}; };
kripkecube<State, SuccIterator>& sys_; ///< \brief The system to check kripkecube<State, SuccIterator>& sys_; ///< \brief The system to check
std::vector<todo__element> todo_; ///< \brief The DFS stack std::vector<todo_element> todo_; ///< \brief The DFS stack
unsigned transitions_ = 0; ///< \brief Number of transitions unsigned transitions_ = 0; ///< \brief Number of transitions
unsigned tid_; ///< \brief Thread's current ID unsigned tid_; ///< \brief Thread's current ID
shared_map map_; ///< \brief Map shared by threads shared_map map_; ///< \brief Map shared by threads
spot::timer_map tm_; ///< \brief Time execution spot::timer_map tm_; ///< \brief Time execution
unsigned states_ = 0; ///< \brief Number of states unsigned states_ = 0; ///< \brief Number of states
...@@ -266,5 +301,6 @@ namespace spot ...@@ -266,5 +301,6 @@ namespace spot
/// \brief Stack that grows according to the todo stack. It avoid multiple /// \brief Stack that grows according to the todo stack. It avoid multiple
/// concurent access to the shared map. /// concurent access to the shared map.
std::vector<int*> refs_; std::vector<int*> refs_;
bool finisher_ = false;
}; };
} }
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
// -*- coding: utf-8 -*-
// Copyright (C) 2019, 2020 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <string>
#include <thread>
#include <vector>
#include <utility>
#include <spot/kripke/kripke.hh>
#include <spot/mc/mc.hh>
#include <spot/mc/lpar13.hh>
#include <spot/mc/deadlock.hh>
#include <spot/mc/cndfs.hh>
#include <spot/mc/bloemen.hh>
#include <spot/mc/bloemen_ec.hh>
#include <spot/misc/common.hh>
#include <spot/misc/timer.hh>
namespace spot
{
/// \brief This class allows to ensure (at compile time) if
/// a given parameter can be compsidered as a modelchecking algorithm
/// (i.e., usable by instanciate)
template <typename T>
class SPOT_API is_a_mc_algorithm
{
private:
using yes = std::true_type;
using no = std::false_type;
// Hardly waiting C++ concepts...
template<typename U> static auto test_mc_algo(U u)
-> decltype(
// Check the kripke
std::is_same<void, decltype(u->setup())>::value &&
std::is_same<void, decltype(u->run())>::value &&
std::is_same<void, decltype(u->finalize())>::value &&
std::is_same<bool, decltype(u->finisher())>::value &&
std::is_same<unsigned, decltype(u->states())>::value &&
std::is_same<unsigned, decltype(u->transitions())>::value &&
std::is_same<unsigned, decltype(u->walltime())>::value &&
std::is_same<std::string, decltype(u->name())>::value &&
std::is_same<int, decltype(u->sccs())>::value &&
std::is_same<mc_rvalue, decltype(u->result())>::value &&
std::is_same<std::string, decltype(u->trace())>::value
// finally return the type "yes"
, yes());
// For all other cases return the type "no"
template<typename> static no test_mc_algo(...);
public:
/// \brief Checking this value will ensure, at compile time, that the
/// Kripke specialisation respects the required interface.
static constexpr bool value =
std::is_same< decltype(test_mc_algo<T>(nullptr)), yes>::value;
};
template<typename algo_name, typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal>
static SPOT_API ec_stats instanciate(kripke_ptr sys,
spot::twacube_ptr prop = nullptr,
bool trace = false)
{
// FIXME ensure that algo_name contains all methods
spot::timer_map tm;
std::atomic<bool> stop(false);
unsigned nbth = sys->get_threads();
typename algo_name::shared_map map;
std::vector<algo_name*> swarmed(nbth);
// The shared structure requires sometime one instance per thread
using struct_name = typename algo_name::shared_struct;
std::vector<struct_name*> ss(nbth);
tm.start("Initialisation");
for (unsigned i = 0; i < nbth; ++i)
{
ss[i] = algo_name::make_shared_structure(map, i);
swarmed[i] = new algo_name(*sys, prop, map, ss[i], i, stop);
static_assert(spot::is_a_mc_algorithm<decltype(&*swarmed[i])>::value,
"error: does not match the kripkecube requirements");
}
tm.stop("Initialisation");
// Spawn Threads
std::mutex iomutex;
std::atomic<bool> barrier(true);
std::vector<std::thread> 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<std::mutex> 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<std::mutex> 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");
// Build the result
ec_stats result;
for (unsigned i = 0; i < nbth; ++i)
{
result.name.emplace_back(swarmed[i]->name());
result.walltime.emplace_back(swarmed[i]->walltime());
result.states.emplace_back(swarmed[i]->states());
result.transitions.emplace_back(swarmed[i]->transitions());
result.sccs.emplace_back(swarmed[i]->sccs());
result.value.emplace_back(swarmed[i]->result());
result.finisher.emplace_back(swarmed[i]->finisher());
}
if (trace)
{
bool go_on = true;
for (unsigned i = 0; i < nbth && go_on; ++i)
{
// Enumerate cases where a trace can be extraced
// Here we use a switch so that adding new algortihm
// with new return status will trigger an error that
// should the be fixed here.
switch (result.value[i])
{
// A (partial?) trace has been computed
case mc_rvalue::DEADLOCK:
case mc_rvalue::NOT_EMPTY:
result.trace = swarmed[i]->trace();
go_on = false;
break;
// Nothing to do here.
case mc_rvalue::NO_DEADLOCK:
case mc_rvalue::EMPTY:
case mc_rvalue::SUCCESS:
case mc_rvalue::FAILURE:
break;
}
}
}
for (unsigned i = 0; i < nbth; ++i)
{
delete swarmed[i];
delete ss[i];
}
return result;
}
template<typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal>
static ec_stats ec_instanciator(const mc_algorithm algo, kripke_ptr sys,
spot::twacube_ptr prop = nullptr,
bool trace = false)
{
if (algo == mc_algorithm::BLOEMEN_EC || algo == mc_algorithm::CNDFS ||
algo == mc_algorithm::SWARMING)
{
SPOT_ASSERT(prop != nullptr);
SPOT_ASSERT(sys->ap().size() == prop->ap().size());
for (unsigned int i = 0; i < sys->ap().size(); ++i)
SPOT_ASSERT(sys->ap()[i].compare(prop->ap()[i]) == 0);
}
switch (algo)
{
case mc_algorithm::BLOEMEN_SCC:
return instanciate<spot::swarmed_bloemen<State, Iterator, Hash, Equal>,
kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
case mc_algorithm::BLOEMEN_EC:
return
instanciate<spot::swarmed_bloemen_ec<State, Iterator, Hash, Equal>,
kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
case mc_algorithm::CNDFS:
return instanciate<spot::swarmed_cndfs<State, Iterator, Hash, Equal>,
kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
case mc_algorithm::DEADLOCK:
return instanciate
<spot::swarmed_deadlock<State, Iterator, Hash, Equal, std::true_type>,
kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
case mc_algorithm::REACHABILITY:
return instanciate
<spot::swarmed_deadlock<State, Iterator, Hash, Equal, std::false_type>,
kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
case mc_algorithm::SWARMING:
return instanciate<spot::lpar13<State, Iterator, Hash, Equal>,
kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
}
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <spot/kripke/kripke.hh>
namespace spot
{
/// \brief This template class provide a sequential reachability
/// of a kripkecube. The algorithm uses a single DFS since it
/// is the most efficient in a sequential setting
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual,
typename Visitor>
class SPOT_API seq_reach_kripke
{
public:
seq_reach_kripke(kripkecube<State, SuccIterator>& sys, unsigned tid):
sys_(sys), tid_(tid)
{
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value,
"error: does not match the kripkecube requirements");
visited.reserve(2000000);
todo.reserve(100000);
}
~seq_reach_kripke()
{
// States will be destroyed by the system, so just clear map
visited.clear();
}
Visitor& self()
{
return static_cast<Visitor&>(*this);
}
void run()
{
self().setup();
State initial = sys_.initial(tid_);
if (SPOT_LIKELY(self().push(initial, dfs_number)))
{
todo.push_back({initial, sys_.succ(initial, tid_)});
visited[initial] = ++dfs_number;
}
while (!todo.empty())
{
if (todo.back().it->done())
{
if (SPOT_LIKELY(self().pop(todo.back().s)))
{
sys_.recycle(todo.back().it, tid_);
todo.pop_back();
}
}
else
{
++transitions;
State dst = todo.back().it->state();
auto it = visited.insert({dst, dfs_number+1});
if (it.second)
{
++dfs_number;
if (SPOT_LIKELY(self().push(dst, dfs_number)))
{
todo.back().it->next();
todo.push_back({dst, sys_.succ(dst, tid_)});
}
}
else
{
self().edge(visited[todo.back().s], visited[dst]);
todo.back().it->next();
}
}
}
self().finalize();
}
unsigned int states()
{
return dfs_number;
}
unsigned int trans()
{
return transitions;
}
protected:
struct todo_element
{
State s;
SuccIterator* it;
};
kripkecube<State, SuccIterator>& sys_;
std::vector<todo_element> todo;
// FIXME: The system already handle a set of visited states so
// this map is redundant: an we avoid this new map?
typedef std::unordered_map<const State, int,
StateHash, StateEqual> visited_map;
visited_map visited;
unsigned int dfs_number = 0;
unsigned int transitions = 0;
unsigned int tid_;
};
}
This diff is collapsed.
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Developpement de // Copyright (C) 2015, 2016, 2018, 2020 Laboratoire de Recherche et
// l'EPITA (LRDE). // Developpement de l'EPITA (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -66,7 +66,7 @@ namespace spot ...@@ -66,7 +66,7 @@ namespace spot
return acc_; return acc_;
} }
std::vector<std::string> twacube::get_ap() const std::vector<std::string> twacube::ap() const
{ {
return aps_; return aps_;
} }
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche // Copyright (C) 2015, 2016, 2020 Laboratoire de Recherche
// et Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -139,7 +139,7 @@ namespace spot ...@@ -139,7 +139,7 @@ namespace spot
acc_cond& acc(); acc_cond& acc();
/// \brief Returns the names of the atomic properties. /// \brief Returns the names of the atomic properties.
std::vector<std::string> get_ap() const; std::vector<std::string> ap() const;
/// \brief This method creates a new state. /// \brief This method creates a new state.
unsigned new_state(); unsigned new_state();
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Developpement de // Copyright (C) 2015, 2016, 2018, 2020 Laboratoire de Recherche et
// l'Epita (LRDE). // Developpement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -19,6 +19,7 @@ ...@@ -19,6 +19,7 @@
#include "config.h" #include "config.h"
#include <spot/twacube_algos/convert.hh> #include <spot/twacube_algos/convert.hh>
#include <spot/twaalgos/contains.hh>
#include <assert.h> #include <assert.h>
namespace spot namespace spot
...@@ -62,6 +63,9 @@ namespace spot ...@@ -62,6 +63,9 @@ namespace spot
spot::twacube_ptr twa_to_twacube(const spot::const_twa_graph_ptr aut) spot::twacube_ptr twa_to_twacube(const spot::const_twa_graph_ptr aut)
{ {
if (aut == nullptr)
return nullptr;
// Compute the necessary binder and extract atomic propositions // Compute the necessary binder and extract atomic propositions
std::unordered_map<int, int> ap_binder; std::unordered_map<int, int> ap_binder;
std::vector<std::string>* aps = extract_aps(aut, ap_binder); std::vector<std::string>* aps = extract_aps(aut, ap_binder);
...@@ -94,23 +98,17 @@ namespace spot ...@@ -94,23 +98,17 @@ namespace spot
// Special case for bddfalse // Special case for bddfalse
if (cond == bddfalse) if (cond == bddfalse)
continue;
// Split the bdd into multiple transitions
while (cond != bddfalse)
{ {
spot::cube cube = tg->get_cubeset().alloc(); bdd one = bdd_satone(cond);
for (unsigned int i = 0; i < cs.size(); ++i) cond -= one;
cs.set_false_var(cube, i); // FIXME ! use fill! spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
tg->create_transition(st_binder[n], cube, tg->create_transition(st_binder[n], cube, t.acc,
t.acc, st_binder[t.dst]); st_binder[t.dst]);
} }
else
// Split the bdd into multiple transitions
while (cond != bddfalse)
{
bdd one = bdd_satone(cond);
cond -= one;
spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
tg->create_transition(st_binder[n], cube, t.acc,
st_binder[t.dst]);
}
} }
// Must be contiguous to support swarming. // Must be contiguous to support swarming.
assert(tg->succ_contiguous()); assert(tg->succ_contiguous());
...@@ -151,7 +149,7 @@ namespace spot ...@@ -151,7 +149,7 @@ namespace spot
// Grep bdd id for each atomic propositions // Grep bdd id for each atomic propositions
std::vector<int> bdds_ref; std::vector<int> bdds_ref;
for (auto& ap : twacube->get_ap()) for (auto& ap : twacube->ap())
bdds_ref.push_back(res->register_ap(ap)); bdds_ref.push_back(res->register_ap(ap));
// Build all resulting states // Build all resulting states
...@@ -184,4 +182,76 @@ namespace spot ...@@ -184,4 +182,76 @@ namespace spot
return res; return res;
} }
// FIXME this code is very close to twacube_to_twa, can we merge both?
bool are_equivalent(const spot::twacube_ptr twacube,
const spot::const_twa_graph_ptr twa)
{
// Compute the necessary binder and extract atomic propositions
std::unordered_map<int, int> ap_binder;
std::vector<std::string>* aps_twa = extract_aps(twa, ap_binder);
std::vector<std::string> aps_twacube = twacube->ap();
// Comparator to compare two strings in case insensitive manner
std::function< bool (const std::string&, const std::string&) >
comparator = [](const std::string& lhs, const std::string& rhs){
return lhs.compare(rhs) == 0;
};
// Error. Not working on the same set of aps.
if (aps_twa->size() != aps_twacube.size() ||
!std::equal(aps_twa->begin(), aps_twa->end(),
aps_twacube.begin(), comparator))
throw std::runtime_error("are_equivalent: not working on the same "
"atomic propositions");
// Grab necessary variables
auto& theg = twacube->get_graph();
spot::cubeset cs = twacube->get_cubeset();
auto d = twa->get_dict();
auto res = make_twa_graph(d);
// Fix the acceptance of the resulting automaton
res->acc() = twacube->acc();
// Grep bdd id for each atomic propositions
std::vector<int> bdds_ref;
for (unsigned i = 0; i < aps_twacube.size(); ++i)
{
bdds_ref.push_back(ap_binder[i]);
}
// Build all resulting states
for (unsigned int i = 0; i < theg.num_states(); ++i)
{
unsigned st = res->new_state();
(void) st;
assert(st == i);
}
// Build all resulting conditions.
for (unsigned int i = 1; i <= theg.num_edges(); ++i)
{
bdd cond = bddtrue;
for (unsigned j = 0; j < cs.size(); ++j)
{
if (cs.is_true_var(theg.edge_data(i).cube_, j))
cond &= bdd_ithvar(bdds_ref[j]);
else if (cs.is_false_var(theg.edge_data(i).cube_, j))
cond &= bdd_nithvar(bdds_ref[j]);
// otherwise it 's a free variable do nothing
}
res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst,
cond, theg.edge_data(i).acc_);
}
// Fix the initial state
res->set_init_state(twacube->get_initial());
bool result = are_equivalent(res, twa);
delete aps_twa;
return result;
}
} }
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Developpement de // Copyright (C) 2015, 2016, 2020 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE). // l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -53,4 +53,8 @@ namespace spot ...@@ -53,4 +53,8 @@ namespace spot
/// \brief Convert a twacube into a twa /// \brief Convert a twacube into a twa
SPOT_API spot::twa_graph_ptr SPOT_API spot::twa_graph_ptr
twacube_to_twa(spot::twacube_ptr twacube); twacube_to_twa(spot::twacube_ptr twacube);
/// \brief Check wether a twacube and a twa are equivalent
SPOT_API bool are_equivalent(const spot::twacube_ptr twacube,
const spot::const_twa_graph_ptr twa);
} }
## -*- coding: utf-8 -*- ## -*- coding: utf-8 -*-
## Copyright (C) 2009-2019 Laboratoire de Recherche et Développement ## Copyright (C) 2009-2020 Laboratoire de Recherche et Développement
## de l'Epita (LRDE). ## de l'Epita (LRDE).
## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 ## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
...@@ -452,6 +452,7 @@ EXTRA_DIST = \ ...@@ -452,6 +452,7 @@ EXTRA_DIST = \
if USE_LTSMIN if USE_LTSMIN
check_PROGRAMS += ltsmin/modelcheck check_PROGRAMS += ltsmin/modelcheck
check_PROGRAMS += ltsmin/testconvert
ltsmin_modelcheck_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \ ltsmin_modelcheck_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
$(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib $(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib
ltsmin_modelcheck_CXXFLAGS = $(CXXFLAGS) -pthread ltsmin_modelcheck_CXXFLAGS = $(CXXFLAGS) -pthread
...@@ -462,19 +463,31 @@ ltsmin_modelcheck_LDADD = \ ...@@ -462,19 +463,31 @@ ltsmin_modelcheck_LDADD = \
$(top_builddir)/spot/libspot.la \ $(top_builddir)/spot/libspot.la \
$(top_builddir)/spot/ltsmin/libspotltsmin.la $(top_builddir)/spot/ltsmin/libspotltsmin.la
ltsmin_testconvert_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
$(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib
ltsmin_testconvert_CXXFLAGS = $(CXXFLAGS) -pthread
ltsmin_testconvert_SOURCES = ltsmin/testconvert.cc
ltsmin_testconvert_LDADD = \
$(top_builddir)/bin/libcommon.a \
$(top_builddir)/lib/libgnu.la \
$(top_builddir)/spot/libspot.la \
$(top_builddir)/spot/ltsmin/libspotltsmin.la
check_SCRIPTS += ltsmin/defs check_SCRIPTS += ltsmin/defs
ltsmin/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in ltsmin/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in
$(top_builddir)/config.status --file ltsmin/defs:core/defs.in $(top_builddir)/config.status --file ltsmin/defs:core/defs.in
TESTS_ltsmin = \ TESTS_ltsmin = \
ltsmin/check.test \ ltsmin/check.test \
ltsmin/check2.test \ ltsmin/check2.test \
ltsmin/check3.test \ ltsmin/check3.test \
ltsmin/finite.test \ ltsmin/finite.test \
ltsmin/finite2.test \ ltsmin/finite2.test \
ltsmin/finite3.test \ ltsmin/finite3.test \
ltsmin/kripke.test ltsmin/kripke.test \
ltsmin/testconvert.test
EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/beem-peterson.4.gal \ EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/beem-peterson.4.gal \
ltsmin/elevator2.1.pm ltsmin/finite.dve ltsmin/finite.pm ltsmin/finite.gal ltsmin/elevator2.1.pm ltsmin/finite.dve ltsmin/finite.pm ltsmin/finite.gal
......
<
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Développement // Copyright (C) 2015, 2016, 2018, 2020 Laboratoire de Recherche et
// de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -49,10 +49,12 @@ int main() ...@@ -49,10 +49,12 @@ int main()
// Test translation // Test translation
auto aut = twa_to_twacube(tg); auto aut = twa_to_twacube(tg);
assert(spot::are_equivalent(aut, tg));
spot::print_dot(std::cout, tg, "A"); spot::print_dot(std::cout, tg, "A");
std::cout << "-----------\n" << *aut << "-----------\n"; std::cout << "-----------\n" << *aut << "-----------\n";
const std::vector<std::string>& aps = aut->get_ap(); const std::vector<std::string>& aps = aut->ap();
unsigned int seed = 17; unsigned int seed = 17;
for (auto it = aut->succ(2); !it->done(); it->next()) for (auto it = aut->succ(2); !it->done(); it->next())
{ {