Line data Source code
1 : // Author(s): Wieger Wesselink 2017-2019
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/pbes/pbesinst_lazy_algorithm.h
10 : /// \brief A lazy algorithm for instantiating a PBES, ported from bes_deprecated.h.
11 :
12 : #include <thread>
13 : #include <mutex>
14 :
15 : #include "mcrl2/atermpp/standard_containers/deque.h"
16 : #include "mcrl2/atermpp/standard_containers/indexed_set.h"
17 : #include "mcrl2/data/substitution_utility.h"
18 : #include "mcrl2/pbes/detail/bes_equation_limit.h"
19 : #include "mcrl2/pbes/detail/instantiate_global_variables.h"
20 : #include "mcrl2/pbes/pbes_equation_index.h"
21 : #include "mcrl2/pbes/pbessolve_options.h"
22 : #include "mcrl2/pbes/remove_equations.h"
23 : #include "mcrl2/pbes/replace_constants_by_variables.h"
24 : #include "mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h"
25 : #include "mcrl2/pbes/rewriters/one_point_rule_rewriter.h"
26 : #include "mcrl2/pbes/rewriters/simplify_quantifiers_rewriter.h"
27 : #include "mcrl2/pbes/transformation_strategy.h"
28 : #include "mcrl2/pbes/transformations.h"
29 :
30 : #ifndef MCRL2_PBES_PBESINST_LAZY_H
31 : #define MCRL2_PBES_PBESINST_LAZY_H
32 :
33 : namespace mcrl2
34 : {
35 :
36 : namespace pbes_system
37 : {
38 :
39 : // This todo set maintains elements that were removed by the reset procedure.
40 : class pbesinst_lazy_todo
41 : {
42 : protected:
43 : std::unordered_set<propositional_variable_instantiation> irrelevant;
44 : atermpp::deque<propositional_variable_instantiation> todo;
45 :
46 : // checks some invariants on the internal state
47 : bool check_invariants() const
48 : {
49 : using utilities::detail::contains;
50 : for (const auto& X: irrelevant)
51 : {
52 : if (contains(todo, X))
53 : {
54 : return false;
55 : }
56 : }
57 : std::unordered_set<propositional_variable_instantiation> tmp(todo.begin(), todo.end());
58 : return tmp.size() == todo.size();
59 : }
60 :
61 : public:
62 3549 : const propositional_variable_instantiation& front() const
63 : {
64 3549 : return todo.front();
65 : }
66 :
67 0 : const propositional_variable_instantiation& back() const
68 : {
69 0 : return todo.back();
70 : }
71 :
72 : bool empty() const
73 : {
74 : return todo.empty() && irrelevant.empty();
75 : }
76 :
77 : std::size_t size() const
78 : {
79 : return todo.size();
80 : }
81 :
82 3682 : const atermpp::deque<propositional_variable_instantiation>& elements() const
83 : {
84 3682 : return todo;
85 : }
86 :
87 : const std::unordered_set<propositional_variable_instantiation>& irrelevant_elements() const
88 : {
89 : return irrelevant;
90 : }
91 :
92 : std::unordered_set<propositional_variable_instantiation>& irrelevant_elements()
93 : {
94 : return irrelevant;
95 : }
96 :
97 3549 : void pop_front()
98 : {
99 3549 : todo.pop_front();
100 3549 : }
101 :
102 0 : void pop_back()
103 : {
104 0 : todo.pop_back();
105 0 : }
106 :
107 133 : void insert(const propositional_variable_instantiation& x)
108 : {
109 133 : irrelevant.erase(x);
110 133 : todo.push_back(x);
111 133 : }
112 :
113 : template <typename FwdIter, bool ThreadSafe>
114 3549 : void insert(FwdIter first,
115 : FwdIter last,
116 : const atermpp::indexed_set<propositional_variable_instantiation, ThreadSafe>& discovered,
117 : const std::size_t thread_index)
118 : {
119 : using utilities::detail::contains;
120 :
121 9140 : for (FwdIter i = first; i != last; ++i)
122 : {
123 5591 : auto j = irrelevant.find(*i);
124 5591 : if (j != irrelevant.end())
125 : {
126 0 : todo.push_back(*j);
127 0 : irrelevant.erase(j);
128 : }
129 5591 : else if (!contains(discovered, *i, thread_index))
130 : {
131 3416 : todo.push_back(*i);
132 : }
133 : }
134 3549 : }
135 :
136 : void set_todo(atermpp::deque<propositional_variable_instantiation>& new_todo)
137 : {
138 : using utilities::detail::contains;
139 : std::size_t size_before = todo.size() + irrelevant.size();
140 : std::unordered_set<propositional_variable_instantiation> new_irrelevant;
141 : for (const propositional_variable_instantiation& x: todo)
142 : {
143 : if (!contains(new_todo, x))
144 : {
145 : new_irrelevant.insert(x);
146 : }
147 : }
148 : for (const propositional_variable_instantiation& x: irrelevant)
149 : {
150 : if (!contains(new_todo, x))
151 : {
152 : new_irrelevant.insert(x);
153 : }
154 : }
155 : std::swap(todo, new_todo);
156 : std::swap(irrelevant, new_irrelevant);
157 :
158 : std::size_t size_after = todo.size() + irrelevant.size();
159 : if (size_before != size_after)
160 : {
161 : throw mcrl2::runtime_error("sizes do not match in pbesinst_lazy_todo::set_todo");
162 : }
163 : assert(check_invariants());
164 : }
165 : };
166 :
167 : inline
168 : std::ostream& operator<<(std::ostream& out, const pbesinst_lazy_todo& todo)
169 : {
170 : return out << "todo = " << core::detail::print_list(todo.elements()) << " irrelevant = " << core::detail::print_list(todo.irrelevant_elements()) << std::endl;
171 : }
172 :
173 : /// \brief A PBES instantiation algorithm that uses a lazy strategy
174 : class pbesinst_lazy_algorithm
175 : {
176 : protected:
177 : /// \brief Algorithm options.
178 : const pbessolve_options& m_options;
179 :
180 : /// \brief Data rewriter.
181 : data::rewriter datar;
182 :
183 : /// \brief A PBES.
184 : pbes m_pbes;
185 :
186 : /// \brief A lookup map for PBES equations.
187 : pbes_equation_index m_equation_index;
188 :
189 : /// \brief The propositional variable instantiations that need to be handled.
190 : pbesinst_lazy_todo todo;
191 :
192 : /// \brief The propositional variable instantiations that have been discovered (not necessarily handled).
193 : atermpp::indexed_set<propositional_variable_instantiation, true> discovered;
194 :
195 : /// \brief The initial value (after rewriting).
196 : propositional_variable_instantiation init;
197 :
198 : // \brief The number of iterations
199 : std::size_t m_iteration_count = 0;
200 :
201 : // The data structures that must be separate per thread.
202 : /// \brief The rewriter.
203 : enumerate_quantifiers_rewriter m_global_R;
204 :
205 : // Mutexes
206 : utilities::mutex m_todo_access;
207 :
208 : volatile bool m_must_abort = false;
209 :
210 : // \brief Returns a status message about the progress
211 0 : virtual std::string status_message(std::size_t equation_count)
212 : {
213 0 : if (equation_count > 0 && equation_count % 1000 == 0)
214 : {
215 0 : std::ostringstream out;
216 0 : out << "Generated " << equation_count << " BES equations" << std::endl;
217 0 : return out.str();
218 0 : }
219 0 : return "";
220 : }
221 :
222 : // instantiates global variables
223 : // simplifies the pbes
224 133 : pbes preprocess(const pbes& x) const
225 : {
226 133 : pbes p = x;
227 133 : pbes_system::detail::instantiate_global_variables(p);
228 : pbes_system::one_point_rule_rewriter one_point_rule_rewriter;
229 133 : pbes_system::simplify_quantifiers_data_rewriter<mcrl2::data::rewriter> simplify_rewriter(datar);
230 606 : for (pbes_equation& eqn: p.equations())
231 : {
232 473 : eqn.formula() = order_quantified_variables(one_point_rule_rewriter(simplify_rewriter(eqn.formula())), p.data());
233 : }
234 266 : return p;
235 0 : }
236 :
237 0 : static void rewrite_true_false(pbes_expression& result,
238 : const fixpoint_symbol& symbol,
239 : const propositional_variable_instantiation& X,
240 : const pbes_expression& psi
241 : )
242 : {
243 0 : bool changed = false;
244 0 : replace_propositional_variables(
245 : result,
246 : psi,
247 0 : [&](const propositional_variable_instantiation& Y) -> pbes_expression
248 : {
249 0 : if (Y == X)
250 : {
251 0 : changed = true;
252 0 : if (symbol.is_mu())
253 : {
254 0 : return false_();
255 : }
256 : else
257 : {
258 0 : return true_();
259 : }
260 : }
261 0 : return Y;
262 : }
263 : );
264 0 : if (changed)
265 : {
266 : simplify_rewriter simplify;
267 0 : const pbes_expression result1=result;
268 0 : simplify(result, result1);
269 0 : }
270 0 : }
271 :
272 133 : data::rewriter construct_rewriter(const pbes& pbesspec)
273 : {
274 133 : if (m_options.remove_unused_rewrite_rules)
275 : {
276 : return data::rewriter(pbesspec.data(),
277 0 : data::used_data_equation_selector(pbesspec.data(), pbes_system::find_function_symbols(pbesspec), pbesspec.global_variables()),
278 0 : m_options.rewrite_strategy);
279 : }
280 : else
281 : {
282 133 : return data::rewriter(pbesspec.data(), m_options.rewrite_strategy);
283 : }
284 : }
285 :
286 : public:
287 :
288 : /// \brief Constructor.
289 : /// \param p The pbes used in the exploration algorithm.
290 : /// \param rewrite_strategy A strategy for the data rewriter.
291 : /// \param search_strategy The search strategy used to explore the pbes, typically depth or breadth first.
292 : /// \param optimization An indication of the optimisation level.
293 133 : explicit pbesinst_lazy_algorithm(
294 : const pbessolve_options& options,
295 : const pbes& p
296 : )
297 133 : : m_options(options),
298 133 : datar(construct_rewriter(p)),
299 133 : m_pbes(preprocess(p)),
300 133 : m_equation_index(p),
301 133 : discovered(m_options.number_of_threads),
302 399 : m_global_R(datar, p.data())
303 133 : { }
304 :
305 133 : virtual ~pbesinst_lazy_algorithm() = default;
306 :
307 : /// \brief Reports BES equations that are produced by the algorithm.
308 : /// This function is called for every BES equation X = psi with rank k that is produced. By default it does nothing.
309 0 : virtual void on_report_equation(const std::size_t /* thread_index */,
310 : const propositional_variable_instantiation& /* X */,
311 : const pbes_expression& /* psi */, std::size_t /* k */
312 : )
313 0 : { }
314 :
315 : /// \brief This function is called when new elements are added to discovered.
316 3549 : virtual void on_discovered_elements(const std::set<propositional_variable_instantiation>& /* elements */)
317 3549 : { }
318 :
319 : /// \brief This function is called right after the while loop is finished.
320 133 : virtual void on_end_while_loop()
321 133 : { }
322 :
323 3549 : void next_todo(propositional_variable_instantiation& result)
324 : {
325 3549 : if (m_options.exploration_strategy == breadth_first)
326 : {
327 3549 : result = todo.front();
328 3549 : todo.pop_front();
329 : }
330 : else
331 : {
332 0 : result = todo.back();
333 0 : todo.pop_back();
334 : }
335 3549 : }
336 :
337 : const fixpoint_symbol& symbol(std::size_t i) const
338 : {
339 : return m_pbes.equations()[i].symbol();
340 : }
341 :
342 : // rewrite the right hand side of the equation X = psi
343 3549 : virtual void rewrite_psi(const std::size_t /* thread_index */,
344 : pbes_expression& result,
345 : const fixpoint_symbol& symbol,
346 : const propositional_variable_instantiation& X,
347 : const pbes_expression& psi
348 : )
349 : {
350 3549 : if (m_options.optimization >= 1)
351 : {
352 0 : rewrite_true_false(result, symbol, X, psi);
353 : }
354 : else
355 : {
356 3549 : result = psi;
357 : }
358 3549 : }
359 :
360 3549 : virtual bool solution_found(const propositional_variable_instantiation& /* init */) const
361 : {
362 3549 : return false;
363 : }
364 :
365 133 : virtual void run_thread(const std::size_t thread_index,
366 : pbesinst_lazy_todo& todo,
367 : std::atomic<std::size_t>& number_of_active_processes,
368 : data::mutable_indexed_substitution<> sigma,
369 : enumerate_quantifiers_rewriter R
370 : )
371 : {
372 : using utilities::detail::contains;
373 :
374 133 : if (m_options.number_of_threads > 1) mCRL2log(log::debug) << "Start thread " << thread_index << ".\n";
375 133 : R.thread_initialise();
376 :
377 133 : propositional_variable_instantiation X_e;
378 133 : pbes_expression psi_e;
379 :
380 266 : while (number_of_active_processes > 0)
381 : {
382 133 : m_todo_access.lock();
383 3682 : while (!todo.elements().empty() && !m_must_abort)
384 : {
385 3549 : ++m_iteration_count;
386 3549 : mCRL2log(log::status) << status_message(m_iteration_count);
387 3549 : detail::check_bes_equation_limit(m_iteration_count);
388 :
389 3549 : next_todo(X_e);
390 3549 : m_todo_access.unlock();
391 :
392 3549 : std::size_t index = m_equation_index.index(X_e.name());
393 3549 : const pbes_equation& eqn = m_pbes.equations()[index];
394 3549 : const auto& phi = eqn.formula();
395 3549 : data::add_assignments(sigma, eqn.variable().parameters(), X_e.parameters());
396 3549 : R(psi_e, phi, sigma);
397 3549 : R.clear_identifier_generator();
398 3549 : data::remove_assignments(sigma, eqn.variable().parameters());
399 :
400 : // optional step
401 3549 : m_todo_access.lock();
402 3549 : rewrite_psi(thread_index, psi_e, eqn.symbol(), X_e, psi_e);
403 3549 : m_todo_access.unlock();
404 :
405 3549 : std::set<propositional_variable_instantiation> occ = find_propositional_variable_instantiations(psi_e);
406 :
407 : // report the generated equation
408 3549 : std::size_t k = m_equation_index.rank(X_e.name());
409 3549 : m_todo_access.lock();
410 3549 : mCRL2log(log::debug) << "generated equation " << X_e << " = " << psi_e
411 0 : << " with rank " << k << std::endl;
412 3549 : on_report_equation(thread_index, X_e, psi_e, k);
413 3549 : todo.insert(occ.begin(), occ.end(), discovered, thread_index);
414 9140 : for (auto i = occ.begin(); i != occ.end(); ++i)
415 : {
416 5591 : discovered.insert(*i, thread_index);
417 : }
418 3549 : on_discovered_elements(occ);
419 :
420 3549 : if (solution_found(init))
421 : {
422 0 : break;
423 : }
424 3549 : }
425 133 : m_todo_access.unlock();
426 :
427 : // Check whether all processes are ready. If so the
428 : // number_of_active_processes becomes 0. Otherwise, this thread becomes
429 : // active again, and tries to see whether the todo buffer is not empty,
430 : // to take up more work.
431 133 : number_of_active_processes--;
432 133 : std::this_thread::sleep_for(std::chrono::milliseconds(100));
433 133 : if (number_of_active_processes > 0)
434 : {
435 0 : number_of_active_processes++;
436 : }
437 : }
438 :
439 133 : if (m_options.number_of_threads>1) mCRL2log(log::debug) << "Stop thread " << thread_index << ".\n";
440 133 : }
441 :
442 : /// \brief Runs the algorithm. The result is obtained by calling the function \p get_result.
443 133 : virtual void run()
444 : {
445 133 : m_iteration_count = 0;
446 :
447 133 : const std::size_t number_of_threads = m_options.number_of_threads;
448 133 : const std::size_t initialisation_thread_index = (number_of_threads==1?0:1);
449 133 : std::atomic<std::size_t> number_of_active_processes = number_of_threads;
450 133 : std::vector<std::thread> threads;
451 :
452 133 : data::mutable_indexed_substitution<> sigma;
453 133 : if (m_options.replace_constants_by_variables)
454 : {
455 0 : pbes_system::replace_constants_by_variables(m_pbes, datar, sigma);
456 : }
457 :
458 133 : init = atermpp::down_cast<propositional_variable_instantiation>(m_global_R(m_pbes.initial_state(), sigma));
459 133 : todo.insert(init);
460 133 : discovered.insert(init, initialisation_thread_index);
461 :
462 133 : if (number_of_threads>1)
463 : {
464 0 : threads.reserve(number_of_threads);
465 0 : for (std::size_t i = 1; i <= number_of_threads; ++i)
466 : {
467 0 : std::thread tr([&, i](){
468 0 : run_thread(i,
469 0 : todo,
470 0 : number_of_active_processes,
471 0 : sigma.clone(),
472 0 : m_global_R.clone()
473 : );
474 0 : });
475 0 : threads.push_back(std::move(tr));
476 0 : }
477 :
478 0 : for (std::size_t i = 1; i <= number_of_threads; ++i)
479 : {
480 0 : threads[i-1].join();
481 : }
482 : }
483 : else
484 : {
485 : // There is only one thread. Run the process in the main thread, without cloning sigma or the rewriter.
486 133 : const std::size_t single_thread_index=0;
487 266 : run_thread(single_thread_index,
488 133 : todo,
489 : number_of_active_processes,
490 : sigma,
491 133 : m_global_R
492 : );
493 : }
494 133 : on_end_while_loop();
495 133 : }
496 :
497 : const pbes_equation_index& equation_index() const
498 : {
499 : return m_equation_index;
500 : }
501 :
502 : enumerate_quantifiers_rewriter& rewriter()
503 : {
504 : return m_global_R;
505 : }
506 : };
507 :
508 : } // namespace pbes_system
509 :
510 : } // namespace mcrl2
511 :
512 : #endif // MCRL2_PBES_PBESINST_LAZY_H
|