21#include <spot/misc/common.hh>
22#include <spot/misc/_config.h>
28#include <spot/kripke/kripke.hh>
29#include <spot/mc/mc.hh>
30#include <spot/mc/lpar13.hh>
31#include <spot/mc/deadlock.hh>
32#include <spot/mc/cndfs.hh>
33#include <spot/mc/bloemen.hh>
34#include <spot/mc/bloemen_ec.hh>
35#include <spot/misc/timer.hh>
47 using yes = std::true_type;
48 using no = std::false_type;
51 template<
typename U>
static auto test_mc_algo(
U u)
54 std::is_same<void,
decltype(u->setup())>::value &&
55 std::is_same<
void,
decltype(u->run())>::value &&
56 std::is_same<
void,
decltype(u->finalize())>::value &&
57 std::is_same<
bool,
decltype(u->finisher())>::value &&
58 std::is_same<
unsigned,
decltype(u->states())>::value &&
59 std::is_same<
unsigned,
decltype(u->transitions())>::value &&
60 std::is_same<
unsigned,
decltype(u->walltime())>::value &&
61 std::is_same<std::string,
decltype(u->name())>::value &&
62 std::is_same<
int,
decltype(u->sccs())>::value &&
63 std::is_same<
mc_rvalue,
decltype(u->result())>::value &&
64 std::is_same<std::string,
decltype(u->trace())>::value
70 template<
typename>
static no test_mc_algo(...);
76 static constexpr bool value =
77 std::is_same< decltype(test_mc_algo<T>(
nullptr)), yes>::value;
81 template<
typename algo_name,
typename kripke_ptr,
typename State,
82 typename Iterator,
typename Hash,
typename Equal>
83 static ec_stats instanciate(kripke_ptr sys,
84 spot::twacube_ptr prop =
nullptr,
88 std::atomic<bool> stop(
false);
89 unsigned nbth = sys->get_threads();
91 typename algo_name::shared_map map;
92 std::vector<algo_name*> swarmed(nbth);
95 using struct_name =
typename algo_name::shared_struct;
96 std::vector<struct_name*> ss(nbth);
98 tm.
start(
"Initialisation");
99 for (
unsigned i = 0; i < nbth; ++i)
101 ss[i] = algo_name::make_shared_structure(map, i);
102 swarmed[i] =
new algo_name(*sys, prop, map, ss[i], i, stop);
105 "error: does not match the kripkecube requirements");
108 tm.
stop(
"Initialisation");
112 std::atomic<bool> barrier(
true);
113 std::vector<std::thread> threads(nbth);
114 for (
unsigned i = 0; i < nbth; ++i)
116 threads[i] = std::thread ([&swarmed, &iomutex, i, &barrier]
118#ifdef SPOT_HAVE_SCHED_GETCPU
120 std::lock_guard<std::mutex> iolock(iomutex);
121 std::cout <<
"Thread #" << i
122 <<
": on CPU " << sched_getcpu() <<
'\n';
132#ifdef SPOT_PTHREAD_SETAFFINITY_NP
137 int rc = pthread_setaffinity_np(threads[i].native_handle(),
138 sizeof(cpu_set_t), &cpuset);
141 std::lock_guard<std::mutex> iolock(iomutex);
142 std::cerr <<
"Error calling pthread_setaffinity_np: " << rc <<
'\n';
148 barrier.store(
false);
150 for (
auto& t: threads)
156 for (
unsigned i = 0; i < nbth; ++i)
158 result.name.emplace_back(swarmed[i]->name());
159 result.walltime.emplace_back(swarmed[i]->walltime());
160 result.states.emplace_back(swarmed[i]->states());
161 result.transitions.emplace_back(swarmed[i]->transitions());
162 result.sccs.emplace_back(swarmed[i]->sccs());
163 result.value.emplace_back(swarmed[i]->result());
164 result.finisher.emplace_back(swarmed[i]->finisher());
170 for (
unsigned i = 0; i < nbth && go_on; ++i)
176 switch (result.value[i])
181 result.trace = swarmed[i]->trace();
195 for (
unsigned i = 0; i < nbth; ++i)
204 template<
typename kripke_ptr,
typename State,
205 typename Iterator,
typename Hash,
typename Equal>
206 static ec_stats ec_instanciator(
const mc_algorithm algo, kripke_ptr sys,
207 spot::twacube_ptr prop =
nullptr,
213 SPOT_ASSERT(prop !=
nullptr);
214 SPOT_ASSERT(sys->ap().size() == prop->ap().size());
215 for (
unsigned int i = 0; i < sys->ap().size(); ++i)
216 SPOT_ASSERT(sys->ap()[i].compare(prop->ap()[i]) == 0);
222 return instanciate<spot::swarmed_bloemen<State, Iterator, Hash, Equal>,
223 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
227 instanciate<spot::swarmed_bloemen_ec<State, Iterator, Hash, Equal>,
228 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
231 return instanciate<spot::swarmed_cndfs<State, Iterator, Hash, Equal>,
232 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
237 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
242 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
245 return instanciate<spot::lpar13<State, Iterator, Hash, Equal>,
246 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
This class allows to ensure (at compile time) if a given parameter can be considered as a modelchecki...
Definition: mc_instanciator.hh:45
This class aims to explore a model to detect wether it contains a deadlock. This deadlock detection p...
Definition: deadlock.hh:46
A map of timer, where each timer has a name.
Definition: timer.hh:225
void stop(const std::string &name)
Stop timer name.
Definition: timer.hh:245
void start(const std::string &name)
Start a timer with name name.
Definition: timer.hh:234
Definition: automata.hh:26
mc_algorithm
The list of parallel model-checking algorithms available.
Definition: mc.hh:33
@ CNDFS
Evangelista.12.atva emptiness check.
@ REACHABILITY
Only perform a reachability algorithm.
@ SWARMING
Holzmann.11.ieee applied to renault.13.lpar.
@ DEADLOCK
Check wether there is a deadlock.
@ BLOEMEN_SCC
Bloemen.16.ppopp SCC computation.
@ BLOEMEN_EC
Bloemen.16.hvc emptiness check.
mc_rvalue
Definition: mc.hh:43
@ NOT_EMPTY
The product is not empty.
@ NO_DEADLOCK
No deadlock has been found.
@ FAILURE
The Algorithm finished abnormally.
@ DEADLOCK
A deadlock has been found.
@ EMPTY
The product is empty.
@ SUCCESS
The Algorithm finished normally.
This structure contains, for each thread, the collected information during the traversal.
Definition: mc.hh:55