spot 2.11.1.dev
mc_instanciator.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2019-2021 Laboratoire de Recherche et
3// Developpement de l'Epita
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <spot/misc/common.hh>
23#include <spot/misc/_config.h>
24#include <string>
25#include <thread>
26#include <vector>
27#include <utility>
28#include <atomic>
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>
37
38namespace spot
39{
40
44 template <typename T>
45 class SPOT_API is_a_mc_algorithm
46 {
47 private:
48 using yes = std::true_type;
49 using no = std::false_type;
50
51 // Hardly waiting C++ concepts...
52 template<typename U> static auto test_mc_algo(U u)
53 -> decltype(
54 // Check the kripke
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
66
67 // finally return the type "yes"
68 , yes());
69
70 // For all other cases return the type "no"
71 template<typename> static no test_mc_algo(...);
72
73 public:
74
77 static constexpr bool value =
78 std::is_same< decltype(test_mc_algo<T>(nullptr)), yes>::value;
79 };
80
81
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,
86 bool trace = false)
87 {
89 std::atomic<bool> stop(false);
90 unsigned nbth = sys->get_threads();
91
92 typename algo_name::shared_map map;
93 std::vector<algo_name*> swarmed(nbth);
94
95 // The shared structure requires sometime one instance per thread
96 using struct_name = typename algo_name::shared_struct;
97 std::vector<struct_name*> ss(nbth);
98
99 tm.start("Initialisation");
100 for (unsigned i = 0; i < nbth; ++i)
101 {
102 ss[i] = algo_name::make_shared_structure(map, i);
103 swarmed[i] = new algo_name(*sys, prop, map, ss[i], i, stop);
104
105 static_assert(spot::is_a_mc_algorithm<decltype(&*swarmed[i])>::value,
106 "error: does not match the kripkecube requirements");
107
108 }
109 tm.stop("Initialisation");
110
111 // Spawn Threads
112 std::mutex iomutex;
113 std::atomic<bool> barrier(true);
114 std::vector<std::thread> threads(nbth);
115 for (unsigned i = 0; i < nbth; ++i)
116 {
117 threads[i] = std::thread ([&swarmed, &iomutex, i, &barrier]
118 {
119#ifdef SPOT_HAVE_SCHED_GETCPU
120 {
121 std::lock_guard<std::mutex> iolock(iomutex);
122 std::cout << "Thread #" << i
123 << ": on CPU " << sched_getcpu() << '\n';
124 }
125#endif
126
127 // Wait all threads to be instanciated.
128 while (barrier)
129 continue;
130 swarmed[i]->run();
131 });
132
133#ifdef SPOT_PTHREAD_SETAFFINITY_NP
134 // Pin threads to a dedicated core.
135 cpu_set_t cpuset;
136 CPU_ZERO(&cpuset);
137 CPU_SET(i, &cpuset);
138 int rc = pthread_setaffinity_np(threads[i].native_handle(),
139 sizeof(cpu_set_t), &cpuset);
140 if (rc != 0)
141 {
142 std::lock_guard<std::mutex> iolock(iomutex);
143 std::cerr << "Error calling pthread_setaffinity_np: " << rc << '\n';
144 }
145#endif
146 }
147
148 tm.start("Run");
149 barrier.store(false);
150
151 for (auto& t: threads)
152 t.join();
153 tm.stop("Run");
154
155 // Build the result
156 ec_stats result;
157 for (unsigned i = 0; i < nbth; ++i)
158 {
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());
166 }
167
168 if (trace)
169 {
170 bool go_on = true;
171 for (unsigned i = 0; i < nbth && go_on; ++i)
172 {
173 // Enumerate cases where a trace can be extraced
174 // Here we use a switch so that adding new algortihm
175 // with new return status will trigger an error that
176 // should the be fixed here.
177 switch (result.value[i])
178 {
179 // A (partial?) trace has been computed
182 result.trace = swarmed[i]->trace();
183 go_on = false;
184 break;
185
186 // Nothing to do here.
188 case mc_rvalue::EMPTY:
191 break;
192 }
193 }
194 }
195
196 for (unsigned i = 0; i < nbth; ++i)
197 {
198 delete swarmed[i];
199 delete ss[i];
200 }
201
202 return result;
203 }
204
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,
209 bool trace = false)
210 {
211 if (algo == mc_algorithm::BLOEMEN_EC || algo == mc_algorithm::CNDFS ||
213 {
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);
218 }
219
220 switch (algo)
221 {
223 return instanciate<spot::swarmed_bloemen<State, Iterator, Hash, Equal>,
224 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
225
227 return
228 instanciate<spot::swarmed_bloemen_ec<State, Iterator, Hash, Equal>,
229 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
230
232 return instanciate<spot::swarmed_cndfs<State, Iterator, Hash, Equal>,
233 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
234
236 return instanciate
238 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
239
241 return instanciate
243 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
244
246 return instanciate<spot::lpar13<State, Iterator, Hash, Equal>,
247 kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
248 }
249 SPOT_UNREACHABLE();
250 }
251}
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
@ U
until
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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4