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

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