22 #include <spot/misc/common.hh>
23 #include <spot/misc/_config.h>
29 #include <spot/kripke/kripke.hh>
30 #include <spot/mc/mc.hh>
31 #include <spot/mc/lpar13.hh>
32 #include <spot/mc/deadlock.hh>
33 #include <spot/mc/cndfs.hh>
34 #include <spot/mc/bloemen.hh>
35 #include <spot/mc/bloemen_ec.hh>
36 #include <spot/misc/timer.hh>
48 using yes = std::true_type;
49 using no = std::false_type;
52 template<
typename U>
static auto test_mc_algo(
U u)
55 std::is_same<
void, decltype(u->setup())>::value &&
56 std::is_same<
void, decltype(u->run())>::value &&
57 std::is_same<
void, decltype(u->finalize())>::value &&
58 std::is_same<
bool, decltype(u->finisher())>::value &&
59 std::is_same<
unsigned, decltype(u->states())>::value &&
60 std::is_same<
unsigned, decltype(u->transitions())>::value &&
61 std::is_same<
unsigned, decltype(u->walltime())>::value &&
62 std::is_same<std::string, decltype(u->name())>::value &&
63 std::is_same<
int, decltype(u->sccs())>::value &&
64 std::is_same<
mc_rvalue, decltype(u->result())>::value &&
65 std::is_same<std::string, decltype(u->trace())>::value
71 template<
typename>
static no test_mc_algo(...);
77 static constexpr
bool value =
78 std::is_same< decltype(test_mc_algo<T>(
nullptr)), yes>::value;
82 template<
typename algo_name,
typename kripke_ptr,
typename State,
83 typename Iterator,
typename Hash,
typename Equal>
84 static ec_stats instanciate(kripke_ptr sys,
85 spot::twacube_ptr prop =
nullptr,
89 std::atomic<bool> stop(
false);
90 unsigned nbth = sys->get_threads();
92 typename algo_name::shared_map map;
93 std::vector<algo_name*> swarmed(nbth);
96 using struct_name =
typename algo_name::shared_struct;
97 std::vector<struct_name*> ss(nbth);
99 tm.
start(
"Initialisation");
100 for (
unsigned i = 0; i < nbth; ++i)
102 ss[i] = algo_name::make_shared_structure(map, i);
103 swarmed[i] =
new algo_name(*sys, prop, map, ss[i], i, stop);
106 "error: does not match the kripkecube requirements");
109 tm.
stop(
"Initialisation");
113 std::atomic<bool> barrier(
true);
114 std::vector<std::thread> threads(nbth);
115 for (
unsigned i = 0; i < nbth; ++i)
117 threads[i] = std::thread ([&swarmed, &iomutex, i, &barrier]
119 #ifdef SPOT_HAVE_SCHED_GETCPU
121 std::lock_guard<std::mutex> iolock(iomutex);
122 std::cout <<
"Thread #" << i
123 <<
": on CPU " << sched_getcpu() <<
'\n';
133 #ifdef SPOT_PTHREAD_SETAFFINITY_NP
138 int rc = pthread_setaffinity_np(threads[i].native_handle(),
139 sizeof(cpu_set_t), &cpuset);
142 std::lock_guard<std::mutex> iolock(iomutex);
143 std::cerr <<
"Error calling pthread_setaffinity_np: " << rc <<
'\n';
149 barrier.store(
false);
151 for (
auto& t: threads)
157 for (
unsigned i = 0; i < nbth; ++i)
159 result.name.emplace_back(swarmed[i]->name());
160 result.walltime.emplace_back(swarmed[i]->walltime());
161 result.states.emplace_back(swarmed[i]->states());
162 result.transitions.emplace_back(swarmed[i]->transitions());
163 result.sccs.emplace_back(swarmed[i]->sccs());
164 result.value.emplace_back(swarmed[i]->result());
165 result.finisher.emplace_back(swarmed[i]->finisher());
171 for (
unsigned i = 0; i < nbth && go_on; ++i)
177 switch (result.value[i])
182 result.trace = swarmed[i]->trace();
196 for (
unsigned i = 0; i < nbth; ++i)
205 template<
typename kripke_ptr,
typename State,
206 typename Iterator,
typename Hash,
typename Equal>
207 static ec_stats ec_instanciator(
const mc_algorithm algo, kripke_ptr sys,
208 spot::twacube_ptr prop =
nullptr,
214 SPOT_ASSERT(prop !=
nullptr);
215 SPOT_ASSERT(sys->ap().size() == prop->ap().size());
216 for (
unsigned int i = 0; i < sys->ap().size(); ++i)
217 SPOT_ASSERT(sys->ap()[i].compare(prop->ap()[i]) == 0);
223 return instanciate<spot::swarmed_bloemen<State, Iterator, Hash, Equal>,
224 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
228 instanciate<spot::swarmed_bloemen_ec<State, Iterator, Hash, Equal>,
229 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
232 return instanciate<spot::swarmed_cndfs<State, Iterator, Hash, Equal>,
233 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
238 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
243 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
246 return instanciate<spot::lpar13<State, Iterator, Hash, Equal>,
247 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
This class allows to ensure (at compile time) if a given parameter can be compsidered as a modelcheck...
Definition: mc_instanciator.hh:46
This class aims to explore a model to detect wether it contains a deadlock. This deadlock detection p...
Definition: deadlock.hh:47
A map of timer, where each timer has a name.
Definition: timer.hh:229
void stop(const std::string &name)
Stop timer name.
Definition: timer.hh:249
void start(const std::string &name)
Start a timer with name name.
Definition: timer.hh:238
Definition: automata.hh:27
mc_algorithm
The list of parallel model-checking algorithms available.
Definition: mc.hh:34
@ 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:44
@ 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:56