Line data Source code
1 : // Author(s): Wieger Wesselink
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/lps/explorer.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_LPS_EXPLORER_H
13 : #define MCRL2_LPS_EXPLORER_H
14 :
15 : #include <random>
16 : #include <thread>
17 : #include <type_traits>
18 : #include "mcrl2/utilities/detail/io.h"
19 : #include "mcrl2/utilities/skip.h"
20 : #include "mcrl2/atermpp/standard_containers/deque.h"
21 : #include "mcrl2/atermpp/standard_containers/vector.h"
22 : #include "mcrl2/atermpp/standard_containers/indexed_set.h"
23 : #include "mcrl2/atermpp/standard_containers/detail/unordered_map_implementation.h"
24 : #include "mcrl2/data/consistency.h"
25 : #include "mcrl2/data/enumerator.h"
26 : #include "mcrl2/data/substitution_utility.h"
27 : #include "mcrl2/lps/detail/instantiate_global_variables.h"
28 : #include "mcrl2/lps/explorer_options.h"
29 : #include "mcrl2/lps/find_representative.h"
30 : #include "mcrl2/lps/one_point_rule_rewrite.h"
31 : #include "mcrl2/lps/order_summand_variables.h"
32 : #include "mcrl2/lps/replace_constants_by_variables.h"
33 : #include "mcrl2/lps/resolve_name_clashes.h"
34 : #include "mcrl2/lps/stochastic_state.h"
35 :
36 : namespace mcrl2::lps {
37 :
38 : enum class caching { none, local, global };
39 :
40 : inline
41 : std::ostream& operator<<(std::ostream& os, caching c)
42 : {
43 : switch(c)
44 : {
45 : case caching::none: os << "none"; break;
46 : case caching::local: os << "local"; break;
47 : case caching::global: os << "global"; break;
48 : default: os.setstate(std::ios_base::failbit);
49 : }
50 : return os;
51 : }
52 :
53 : inline
54 487 : std::vector<data::data_expression> make_data_expression_vector(const data::data_expression_list& v)
55 : {
56 974 : return std::vector<data::data_expression>(v.begin(), v.end());
57 : }
58 :
59 : class todo_set
60 : {
61 : protected:
62 : atermpp::deque<state> todo;
63 :
64 : public:
65 0 : explicit todo_set()
66 0 : {}
67 :
68 174 : explicit todo_set(const state& init)
69 174 : : todo{init}
70 174 : {}
71 :
72 : template<typename ForwardIterator>
73 210 : todo_set(ForwardIterator first, ForwardIterator last)
74 210 : : todo(first, last)
75 210 : {}
76 :
77 384 : virtual ~todo_set() = default;
78 :
79 0 : virtual void choose_element(state& result)
80 : {
81 0 : result = todo.front();
82 0 : todo.pop_front();
83 0 : }
84 :
85 0 : virtual void insert(const state& s)
86 : {
87 0 : todo.push_back(s);
88 0 : }
89 :
90 1354 : virtual void finish_state()
91 1354 : { }
92 :
93 2770 : virtual bool empty() const
94 : {
95 2770 : return todo.empty();
96 : }
97 :
98 1354 : virtual std::size_t size() const
99 : {
100 1354 : return todo.size();
101 : }
102 : };
103 :
104 : class breadth_first_todo_set : public todo_set
105 : {
106 : public:
107 0 : explicit breadth_first_todo_set()
108 0 : : todo_set()
109 0 : {}
110 :
111 93 : explicit breadth_first_todo_set(const state& init)
112 93 : : todo_set(init)
113 93 : {}
114 :
115 : template<typename ForwardIterator>
116 117 : breadth_first_todo_set(ForwardIterator first, ForwardIterator last)
117 117 : : todo_set(first, last)
118 117 : {}
119 :
120 817 : void choose_element(state& result) override
121 : {
122 817 : result = todo.front();
123 817 : todo.pop_front();
124 817 : }
125 :
126 706 : void insert(const state& s) override
127 : {
128 706 : todo.push_back(s);
129 706 : }
130 :
131 0 : atermpp::deque<state>& todo_buffer()
132 : {
133 0 : return todo;
134 : }
135 :
136 : void swap(breadth_first_todo_set& other)
137 : {
138 : todo.swap(other.todo);
139 : }
140 : };
141 :
142 : class depth_first_todo_set : public todo_set
143 : {
144 : public:
145 81 : explicit depth_first_todo_set(const state& init)
146 81 : : todo_set(init)
147 81 : {}
148 :
149 : template<typename ForwardIterator>
150 93 : depth_first_todo_set(ForwardIterator first, ForwardIterator last)
151 93 : : todo_set(first, last)
152 93 : {}
153 :
154 741 : void choose_element(state& result) override
155 : {
156 741 : result = todo.back();
157 741 : todo.pop_back();
158 741 : }
159 :
160 648 : void insert(const state& s) override
161 : {
162 648 : todo.push_back(s);
163 648 : }
164 : };
165 :
166 : class highway_todo_set : public todo_set
167 : {
168 : protected:
169 : std::size_t N;
170 : breadth_first_todo_set new_states;
171 : std::size_t n=0; // This is the number of new_states that are seen, of which at most N are stored in new_states.
172 : std::random_device device;
173 : std::mt19937 generator;
174 :
175 : public:
176 0 : explicit highway_todo_set(const state& init, std::size_t N_)
177 0 : : N(N_),
178 0 : new_states(init),
179 0 : n(1),
180 0 : device(),
181 0 : generator(device())
182 : {
183 0 : }
184 :
185 : template<typename ForwardIterator>
186 0 : highway_todo_set(ForwardIterator first, ForwardIterator last, std::size_t N_)
187 0 : : N(N_),
188 0 : device(),
189 0 : generator(device())
190 : {
191 0 : for(ForwardIterator i=first; i!=last; ++i)
192 : {
193 0 : insert(*i);
194 : }
195 0 : }
196 :
197 0 : void choose_element(state& result) override
198 : {
199 0 : if (todo.empty())
200 : {
201 0 : assert(new_states.size()>0);
202 0 : todo.swap(new_states.todo_buffer());
203 : }
204 0 : result = todo.front();
205 0 : todo.pop_front();
206 0 : }
207 :
208 0 : void insert(const state& s) override
209 : {
210 0 : if (new_states.size() < N-1)
211 : {
212 0 : new_states.insert(s);
213 : }
214 : else
215 : {
216 0 : std::uniform_int_distribution<> distribution(0, n-1);
217 0 : std::size_t k = distribution(generator);
218 0 : if (k < N)
219 : {
220 0 : assert(N==new_states.size());
221 0 : (new_states.todo_buffer())[k] = s;
222 : }
223 : }
224 0 : n++;
225 0 : }
226 :
227 0 : std::size_t size() const override
228 : {
229 0 : return todo.size() + new_states.size();
230 : }
231 :
232 0 : bool empty() const override
233 : {
234 0 : return todo.empty() && new_states.empty();
235 : }
236 :
237 0 : void finish_state() override
238 : {
239 0 : }
240 : };
241 :
242 : template <typename Summand>
243 352 : inline const stochastic_distribution& summand_distribution(const Summand& /* summand */)
244 : {
245 352 : static stochastic_distribution empty_distribution;
246 352 : return empty_distribution;
247 : }
248 :
249 : template <>
250 135 : inline const stochastic_distribution& summand_distribution(const lps::stochastic_action_summand& summand)
251 : {
252 135 : return summand.distribution();
253 : }
254 :
255 : inline
256 172 : const stochastic_distribution& initial_distribution(const lps::specification& /* lpsspec */)
257 : {
258 172 : static stochastic_distribution empty_distribution;
259 172 : return empty_distribution;
260 : }
261 :
262 : inline
263 30 : const stochastic_distribution& initial_distribution(const lps::stochastic_specification& lpsspec)
264 : {
265 30 : return lpsspec.initial_process().distribution();
266 : }
267 :
268 : namespace detail
269 : {
270 : // The functions below are used to support the key type in caches.
271 : //
272 : struct cheap_cache_key
273 : {
274 : data::mutable_indexed_substitution<>& m_sigma;
275 : const std::vector<data::variable>& m_gamma;
276 :
277 0 : cheap_cache_key(data::mutable_indexed_substitution<>& sigma, const std::vector<data::variable>& gamma)
278 0 : : m_sigma(sigma),
279 0 : m_gamma(gamma)
280 0 : {}
281 :
282 : };
283 :
284 : struct cache_equality
285 : {
286 0 : bool operator()(const atermpp::term_appl<data::data_expression>& key1, const atermpp::term_appl<data::data_expression>& key2) const
287 : {
288 0 : return key1==key2;
289 : }
290 :
291 0 : bool operator()(const atermpp::term_appl<data::data_expression>& key1, const cheap_cache_key& key2) const
292 : {
293 0 : std::vector<data::variable>::const_iterator i=key2.m_gamma.begin();
294 0 : for(const data::data_expression& d: key1)
295 : {
296 0 : if (d!=key2.m_sigma(*i))
297 : {
298 0 : return false;
299 : }
300 0 : ++i;
301 : }
302 0 : return true;
303 : }
304 : };
305 :
306 : struct cache_hash
307 : {
308 : std::size_t operator()(const std::pair<const atermpp::term_appl<mcrl2::data::data_expression>,
309 : std::list<atermpp::term_list<mcrl2::data::data_expression>>>& pair) const
310 : {
311 : return operator()(pair.first);
312 : }
313 :
314 0 : std::size_t operator()(const atermpp::term_appl<data::data_expression>& key) const
315 : {
316 0 : std::size_t hash=0;
317 0 : for(const data::data_expression& d: key)
318 : {
319 0 : hash=atermpp::detail::combine(hash,d);
320 : }
321 0 : return hash;
322 : }
323 :
324 0 : std::size_t operator()(const cheap_cache_key& key) const
325 : {
326 0 : std::size_t hash=0;
327 0 : for(const data::variable& v: key.m_gamma)
328 : {
329 0 : hash=atermpp::detail::combine(hash,key.m_sigma(v));
330 : }
331 0 : return hash;
332 : }
333 : };
334 :
335 : } // end namespace detail
336 :
337 :
338 : typedef atermpp::utilities::unordered_map<atermpp::term_appl<data::data_expression>,
339 : atermpp::term_list<data::data_expression_list>,
340 : detail::cache_hash,
341 : detail::cache_equality,
342 : std::allocator< std::pair<atermpp::term_appl<data::data_expression>, atermpp::term_list<data::data_expression_list>> >,
343 : true // Thread_safe.
344 : > summand_cache_map;
345 :
346 :
347 : struct explorer_summand
348 : {
349 : data::variable_list variables;
350 : data::data_expression condition;
351 : lps::multi_action multi_action;
352 : stochastic_distribution distribution;
353 : std::vector<data::data_expression> next_state;
354 : std::size_t index;
355 :
356 : // attributes for caching
357 : caching cache_strategy;
358 : std::vector<data::variable> gamma;
359 : atermpp::function_symbol f_gamma;
360 : mutable summand_cache_map local_cache;
361 :
362 : template <typename ActionSummand>
363 487 : explorer_summand(const ActionSummand& summand, std::size_t summand_index, const data::variable_list& process_parameters, caching cache_strategy_)
364 487 : : variables(summand.summation_variables()),
365 487 : condition(summand.condition()),
366 487 : multi_action(summand.multi_action()),
367 487 : distribution(summand_distribution(summand)),
368 487 : next_state(make_data_expression_vector(summand.next_state(process_parameters))),
369 487 : index(summand_index),
370 487 : cache_strategy(cache_strategy_)
371 : {
372 487 : gamma = free_variables(summand.condition(), process_parameters);
373 487 : if (cache_strategy_ == caching::global)
374 : {
375 0 : gamma.insert(gamma.begin(), data::variable());
376 : }
377 487 : f_gamma = atermpp::function_symbol("@gamma", gamma.size());
378 487 : }
379 :
380 : template <typename T>
381 487 : std::vector<data::variable> free_variables(const T& x, const data::variable_list& v)
382 : {
383 : using utilities::detail::contains;
384 487 : std::set<data::variable> FV = data::find_free_variables(x);
385 487 : std::vector<data::variable> result;
386 3460 : for (const data::variable& vi: v)
387 : {
388 2486 : if (contains(FV, vi))
389 : {
390 711 : result.push_back(vi);
391 : }
392 : }
393 974 : return result;
394 487 : }
395 :
396 0 : void compute_key(atermpp::term_appl<data::data_expression>& key,
397 : data::mutable_indexed_substitution<>& sigma) const
398 : {
399 0 : if (cache_strategy == caching::global)
400 : {
401 0 : bool is_first_element = true;
402 0 : atermpp::make_term_appl(key, f_gamma, gamma.begin(), gamma.end(),
403 0 : [&](data::data_expression& result, const data::variable& x)
404 : {
405 0 : if (is_first_element)
406 : {
407 0 : is_first_element = false;
408 0 : result=condition;
409 0 : return;
410 : }
411 0 : sigma.apply(x, result);
412 0 : return;
413 : }
414 : );
415 : }
416 : else
417 : {
418 0 : atermpp::make_term_appl(key, f_gamma, gamma.begin(), gamma.end(),
419 0 : [&](data::data_expression& result, const data::variable& x)
420 : {
421 0 : sigma.apply(x, result);
422 0 : }
423 : );
424 : }
425 0 : }
426 : };
427 :
428 : inline
429 : std::ostream& operator<<(std::ostream& out, const explorer_summand& summand)
430 : {
431 : return out << lps::stochastic_action_summand(
432 : summand.variables,
433 : summand.condition,
434 : summand.multi_action,
435 : data::make_assignment_list(summand.variables, summand.next_state),
436 : summand.distribution
437 : );
438 : }
439 :
440 : struct abortable
441 : {
442 : virtual void abort() = 0;
443 : };
444 :
445 : template <bool Stochastic, bool Timed, typename Specification>
446 : class explorer: public abortable
447 : {
448 : public:
449 : using state_type = typename std::conditional<Stochastic, stochastic_state, state>::type;
450 : using state_index_type = typename std::conditional<Stochastic, std::list<std::size_t>, std::size_t>::type;
451 : static constexpr bool is_stochastic = Stochastic;
452 : static constexpr bool is_timed = Timed;
453 :
454 : typedef atermpp::indexed_set<state, mcrl2::utilities::detail::GlobalThreadSafe> indexed_set_for_states_type;
455 :
456 :
457 : struct transition
458 : {
459 : lps::multi_action action;
460 : state_type state;
461 :
462 12 : transition(lps::multi_action action_, const state_type& state_)
463 12 : : action(std::move(action_)), state(state_)
464 12 : {}
465 : };
466 :
467 : protected:
468 : using enumerator_element = data::enumerator_list_element_with_substitution<>;
469 : const explorer_options m_options; // must not be a reference.
470 :
471 : // The four data structures that must be separate per thread.
472 : mutable data::mutable_indexed_substitution<> m_global_sigma;
473 : data::rewriter m_global_rewr;
474 : data::enumerator_algorithm<> m_global_enumerator;
475 : data::enumerator_identifier_generator m_global_id_generator;
476 :
477 : Specification m_global_lpsspec;
478 : // Mutexes
479 : std::mutex m_exclusive_state_access;
480 :
481 : std::vector<data::variable> m_process_parameters;
482 : std::size_t m_n; // m_n = m_process_parameters.size()
483 : data::data_expression_list m_initial_state;
484 : lps::stochastic_distribution m_initial_distribution;
485 : bool m_recursive = false;
486 : std::vector<explorer_summand> m_regular_summands;
487 : std::vector<explorer_summand> m_confluent_summands;
488 :
489 : volatile std::atomic<bool> m_must_abort = false;
490 :
491 : // N.B. The keys are stored in term_appl instead of data_expression_list for performance reasons.
492 : summand_cache_map global_cache;
493 :
494 : indexed_set_for_states_type m_discovered;
495 :
496 : // used by make_timed_state, to avoid needless creation of vectors
497 : mutable std::vector<data::data_expression> timed_state;
498 :
499 202 : Specification preprocess(const Specification& lpsspec)
500 : {
501 202 : Specification result = lpsspec;
502 202 : detail::instantiate_global_variables(result);
503 202 : lps::order_summand_variables(result);
504 202 : resolve_summand_variable_name_clashes(result); // N.B. This is a required preprocessing step.
505 202 : if (m_options.one_point_rule_rewrite)
506 : {
507 0 : one_point_rule_rewrite(result);
508 : }
509 202 : if (m_options.replace_constants_by_variables)
510 : {
511 0 : replace_constants_by_variables(result, m_global_rewr, m_global_sigma);
512 : }
513 202 : return result;
514 0 : }
515 :
516 : // Evaluates whether t0 <= t1
517 6 : bool less_equal(const data::data_expression& t0,
518 : const data::data_expression& t1,
519 : data::mutable_indexed_substitution<>& sigma,
520 : data::rewriter& rewr) const
521 : {
522 6 : return rewr(data::less_equal(t0, t1),sigma) == data::sort_bool::true_();
523 : }
524 :
525 : // Find a unique representative in the confluent tau-graph reachable from u0.
526 : template <typename SummandSequence>
527 18 : state find_representative(state& u0,
528 : const SummandSequence& summands,
529 : data::mutable_indexed_substitution<>& sigma,
530 : data::rewriter& rewr,
531 : data::enumerator_algorithm<>& enumerator,
532 : data::enumerator_identifier_generator& id_generator)
533 : {
534 18 : bool recursive_undo = m_recursive;
535 18 : m_recursive = true;
536 18 : data::data_expression_list process_parameter_undo = process_parameter_values(sigma);
537 18 : state result = lps::find_representative(u0,
538 48 : [&](const state& u)
539 24 : { return generate_successors(u, summands, sigma, rewr, enumerator, id_generator); });
540 18 : set_process_parameter_values(process_parameter_undo, sigma);
541 18 : m_recursive = recursive_undo;
542 36 : return result;
543 18 : }
544 :
545 : template <typename DataExpressionSequence>
546 2942 : void compute_state(state& result,
547 : const DataExpressionSequence& v,
548 : data::mutable_indexed_substitution<>& sigma,
549 : data::rewriter& rewr) const
550 : {
551 2942 : lps::make_state(result,
552 : v.begin(),
553 2942 : m_n,
554 14634 : [&](data::data_expression& result, const data::data_expression& x) { return rewr(result, x, sigma); });
555 2942 : }
556 :
557 : template <typename DataExpressionSequence>
558 208 : void compute_stochastic_state(stochastic_state& result,
559 : const stochastic_distribution& distribution,
560 : const DataExpressionSequence& next_state,
561 : data::mutable_indexed_substitution<>& sigma,
562 : data::rewriter& rewr,
563 : data::enumerator_algorithm<>& enumerator) const
564 : {
565 208 : result.clear();
566 208 : if (distribution.is_defined())
567 : {
568 196 : enumerator.enumerate<enumerator_element>(
569 : distribution.variables(),
570 196 : distribution.distribution(),
571 : sigma,
572 1568 : [&](const enumerator_element& p)
573 : {
574 392 : p.add_assignments(distribution.variables(), sigma, rewr);
575 392 : result.probabilities.push_back(p.expression());
576 392 : result.states.emplace_back();
577 392 : compute_state(result.states.back(), next_state, sigma, rewr);
578 392 : return false;
579 : },
580 588 : [](const data::data_expression& x) { return x == data::sort_real::real_zero(); }
581 : );
582 196 : data::remove_assignments(sigma, distribution.variables());
583 196 : if (m_options.check_probabilities)
584 : {
585 0 : check_stochastic_state(result, rewr);
586 : }
587 : }
588 : else
589 : {
590 12 : result.probabilities.push_back(data::sort_real::real_one());
591 12 : result.states.emplace_back();
592 12 : compute_state(result.states.back(),next_state,sigma,rewr);
593 : }
594 208 : }
595 :
596 : /// Rewrite action a, and put it back in place.
597 2548 : lps::multi_action rewrite_action(
598 : const lps::multi_action& a,
599 : data::mutable_indexed_substitution<>& sigma,
600 : data::rewriter& rewr) const
601 : {
602 2548 : const process::action_list& actions = a.actions();
603 2548 : const data::data_expression& time = a.time();
604 : return lps::multi_action(
605 5096 : process::action_list(
606 : actions.begin(),
607 : actions.end(),
608 5000 : [&](process::action& result, const process::action& a)
609 : {
610 2500 : const data::data_expression_list& args = a.arguments();
611 2500 : return process::make_action(result,
612 : a.label(),
613 5000 : data::data_expression_list(args.begin(),
614 : args.end(),
615 4388 : [&](data::data_expression& result,
616 : const data::data_expression& x) -> void
617 4694 : { rewr(result, x, sigma); }));
618 : }
619 : ),
620 5096 : a.has_time() ? rewr(time, sigma) : time
621 5096 : );
622 : }
623 :
624 2554 : void check_enumerator_solution(const data::data_expression& p_expression, // WAS: const enumerator_element& p,
625 : const explorer_summand& summand,
626 : data::mutable_indexed_substitution<>& sigma,
627 : data::rewriter& rewr) const
628 : {
629 2554 : if (p_expression != data::sort_bool::true_())
630 : {
631 0 : std::string printed_condition = data::pp(p_expression);
632 0 : data::remove_assignments(sigma, m_process_parameters);
633 0 : data::remove_assignments(sigma, summand.variables);
634 0 : data::data_expression reduced_condition = rewr(summand.condition, sigma);
635 0 : throw data::enumerator_error("Condition " + data::pp(reduced_condition) +
636 : " does not rewrite to true or false. Culprit: "
637 : + printed_condition.substr(0,300)
638 0 : + (printed_condition.size() > 300 ? "..." : ""));
639 0 : }
640 2554 : }
641 :
642 : // Generates outgoing transitions for a summand, and reports them via the callback function report_transition.
643 : // It is assumed that the substitution sigma contains the assignments corresponding to the current state.
644 : template <typename SummandSequence, typename ReportTransition = utilities::skip>
645 12024 : void generate_transitions(
646 : const explorer_summand& summand,
647 : const SummandSequence& confluent_summands,
648 : data::mutable_indexed_substitution<>& sigma,
649 : data::rewriter& rewr,
650 : data::data_expression& condition, // These three variables are passed on such
651 : state_type& s1, // that they don't have to be declared often.
652 : atermpp::term_appl<data::data_expression>& key, //
653 : data::enumerator_algorithm<>& enumerator,
654 : data::enumerator_identifier_generator& id_generator,
655 : ReportTransition report_transition = ReportTransition()
656 : )
657 : {
658 12024 : bool variables_are_assigned_to_sigma=false;
659 12024 : if (!m_recursive)
660 : {
661 12000 : id_generator.clear();
662 : }
663 12024 : if (summand.cache_strategy == caching::none)
664 : {
665 12024 : rewr(condition, summand.condition, sigma);
666 12024 : if (!data::is_false(condition))
667 : {
668 1342 : if (summand.variables.size()==0)
669 : {
670 : // There is only one solution that is generated as there are no variables.
671 623 : check_enumerator_solution(condition, summand,sigma,rewr);
672 : // state_type s1;
673 : if constexpr (Stochastic)
674 : {
675 165 : compute_stochastic_state(s1, summand.distribution, summand.next_state, sigma, rewr, enumerator);
676 : }
677 : else
678 : {
679 458 : compute_state(s1,summand.next_state,sigma,rewr);
680 458 : if (!confluent_summands.empty())
681 : {
682 0 : s1 = find_representative(s1, confluent_summands, sigma, rewr, enumerator, id_generator);
683 : }
684 : }
685 : // Check whether report transition only needs a state, and no action.
686 : if constexpr (utilities::is_applicable<ReportTransition,state_type,void>::value)
687 : {
688 6 : report_transition(s1);
689 : }
690 : else
691 : {
692 617 : if (m_options.rewrite_actions)
693 : {
694 617 : lps::multi_action a=rewrite_action(summand.multi_action,sigma,rewr);
695 617 : report_transition(a,s1);
696 617 : }
697 : else
698 : {
699 0 : report_transition(summand.multi_action,s1);
700 : }
701 : }
702 : }
703 : else // There are variables to be enumerated.
704 : {
705 719 : enumerator.enumerate<enumerator_element>(
706 719 : summand.variables,
707 : condition,
708 : sigma,
709 17366 : [&](const enumerator_element& p) {
710 1931 : check_enumerator_solution(p.expression(), summand, sigma, rewr);
711 1931 : p.add_assignments(summand.variables, sigma, rewr);
712 1931 : variables_are_assigned_to_sigma=true;
713 1931 : state_type s1;
714 : if constexpr (Stochastic)
715 : {
716 25 : compute_stochastic_state(s1, summand.distribution, summand.next_state, sigma, rewr, enumerator);
717 : }
718 : else
719 : {
720 1906 : compute_state(s1,summand.next_state,sigma,rewr);
721 1906 : if (!confluent_summands.empty())
722 : {
723 12 : s1 = find_representative(s1, confluent_summands, sigma, rewr, enumerator, id_generator);
724 : }
725 : }
726 1931 : if (m_recursive && variables_are_assigned_to_sigma)
727 : {
728 0 : data::remove_assignments(sigma, summand.variables);
729 0 : variables_are_assigned_to_sigma=false;
730 : }
731 : // Check whether report transition only needs a state, and no action.
732 : if constexpr (utilities::is_applicable<ReportTransition,state_type,void>::value)
733 : {
734 0 : report_transition(s1);
735 : }
736 : else
737 : {
738 1931 : if (m_options.rewrite_actions)
739 : {
740 1931 : lps::multi_action a=rewrite_action(summand.multi_action,sigma,rewr);
741 1931 : report_transition(a,s1);
742 1931 : }
743 : else
744 : {
745 0 : report_transition(summand.multi_action,s1);
746 : }
747 : }
748 1931 : return false;
749 1931 : },
750 : data::is_false
751 : );
752 : }
753 : }
754 : }
755 : else
756 : {
757 0 : auto& cache = summand.cache_strategy == caching::global ? global_cache : summand.local_cache;
758 0 : summand_cache_map::iterator q = cache.find(detail::cheap_cache_key(sigma, summand.gamma));
759 0 : if (q == cache.end())
760 : {
761 0 : rewr(condition, summand.condition, sigma);
762 0 : atermpp::term_list<data::data_expression_list> solutions;
763 0 : if (!data::is_false(condition))
764 : {
765 0 : enumerator.enumerate<enumerator_element>(
766 0 : summand.variables,
767 : condition,
768 : sigma,
769 0 : [&](const enumerator_element& p) {
770 0 : check_enumerator_solution(p.expression(), summand, sigma, rewr);
771 0 : solutions.push_front(p.assign_expressions(summand.variables, rewr));
772 0 : return false;
773 : },
774 : data::is_false
775 : );
776 : }
777 0 : summand.compute_key(key, sigma);
778 0 : q = cache.insert({key, solutions}).first;
779 0 : }
780 :
781 0 : for (const data::data_expression_list& e: static_cast<atermpp::term_list<data::data_expression_list>&>(q->second))
782 : {
783 0 : data::add_assignments(sigma, summand.variables, e);
784 0 : variables_are_assigned_to_sigma=true;
785 : if constexpr (Stochastic)
786 : {
787 0 : compute_stochastic_state(s1, summand.distribution, summand.next_state, sigma, rewr, enumerator);
788 : }
789 : else
790 : {
791 0 : compute_state(s1,summand.next_state,sigma,rewr);
792 0 : if (!confluent_summands.empty())
793 : {
794 0 : s1 = find_representative(s1, confluent_summands, sigma, rewr, enumerator, id_generator);
795 : }
796 : }
797 0 : if (m_recursive && variables_are_assigned_to_sigma)
798 : {
799 0 : data::remove_assignments(sigma, summand.variables);
800 0 : variables_are_assigned_to_sigma=false;
801 : }
802 : // If report transition does not require a transition, do not calculate it.
803 : if constexpr (utilities::is_applicable<ReportTransition,state_type,void>::value)
804 : {
805 0 : report_transition(s1);
806 : }
807 : else
808 : {
809 0 : if (m_options.rewrite_actions)
810 : {
811 0 : lps::multi_action a=rewrite_action(summand.multi_action,sigma,rewr);
812 0 : report_transition(a,s1);
813 0 : }
814 : else
815 : {
816 0 : report_transition(summand.multi_action,s1);
817 : }
818 : }
819 : }
820 :
821 : }
822 12024 : if (!m_recursive && variables_are_assigned_to_sigma)
823 : {
824 719 : data::remove_assignments(sigma, summand.variables);
825 : }
826 12024 : }
827 :
828 : template <typename SummandSequence>
829 26 : std::list<transition> out_edges(const state& s,
830 : const SummandSequence& regular_summands,
831 : const SummandSequence& confluent_summands,
832 : data::mutable_indexed_substitution<>& sigma,
833 : data::rewriter& rewr,
834 : data::enumerator_algorithm<>& enumerator,
835 : data::enumerator_identifier_generator& id_generator
836 : )
837 : {
838 26 : data::data_expression condition; // This variable is used often, and it is time consuming to declare it too often.
839 26 : state_type state_; // The same holds for this variable.
840 26 : atermpp::term_appl<data::data_expression> key;
841 26 : std::list<transition> transitions;
842 26 : data::add_assignments(sigma, m_process_parameters, s);
843 70 : for (const explorer_summand& summand: regular_summands)
844 : {
845 44 : generate_transitions(
846 : summand,
847 : confluent_summands,
848 : sigma,
849 : rewr,
850 : condition,
851 : state_,
852 : key,
853 : enumerator,
854 : id_generator,
855 24 : [&](const lps::multi_action& a, const state_type& s1)
856 : {
857 : if constexpr (Timed)
858 : {
859 0 : const data::data_expression& t = s[m_n];
860 0 : if (a.has_time() && less_equal(a.time(), t, sigma, rewr))
861 : {
862 0 : return;
863 : }
864 0 : const data::data_expression& t1 = a.has_time() ? a.time() : t;
865 0 : make_timed_state(state_, s1, t1);
866 0 : transitions.emplace_back(a, state_);
867 : }
868 : else
869 : {
870 12 : transitions.emplace_back(a, s1);
871 : }
872 : }
873 : );
874 : }
875 52 : return transitions;
876 26 : }
877 :
878 : // pre: s0 is in normal form
879 : template <typename SummandSequence>
880 24 : std::vector<state> generate_successors(
881 : const state& s0,
882 : const SummandSequence& summands,
883 : data::mutable_indexed_substitution<>& sigma,
884 : data::rewriter& rewr,
885 : data::enumerator_algorithm<>& enumerator,
886 : data::enumerator_identifier_generator& id_generator,
887 : const SummandSequence& confluent_summands = SummandSequence()
888 : )
889 : {
890 24 : data::data_expression condition;
891 24 : state_type state_;
892 24 : atermpp::term_appl<data::data_expression> key;
893 24 : std::vector<state> result;
894 24 : data::add_assignments(sigma, m_process_parameters, s0);
895 48 : for (const explorer_summand& summand: summands)
896 : {
897 24 : generate_transitions(
898 : summand,
899 : confluent_summands,
900 : sigma,
901 : rewr,
902 : condition,
903 : state_,
904 : key,
905 : enumerator,
906 : id_generator,
907 : // [&](const lps::multi_action& /* a */, const state& s1) OLD. Calculates transitions, that are not used.
908 12 : [&](const state& s1)
909 : {
910 6 : result.push_back(s1);
911 : }
912 : );
913 24 : data::remove_assignments(sigma, summand.variables);
914 : }
915 48 : return result;
916 24 : }
917 :
918 : // Add operations on reals that are needed for the exploration.
919 0 : std::set<data::function_symbol> add_real_operators(std::set<data::function_symbol> s) const
920 : {
921 0 : std::set<data::function_symbol> result = std::move(s);
922 0 : result.insert(data::less_equal(data::sort_real::real_()));
923 0 : result.insert(data::greater_equal(data::sort_real::real_()));
924 0 : result.insert(data::sort_real::plus(data::sort_real::real_(), data::sort_real::real_()));
925 0 : return result;
926 0 : }
927 :
928 174 : std::unique_ptr<todo_set> make_todo_set(const state& init)
929 : {
930 174 : switch (m_options.search_strategy)
931 : {
932 93 : case lps::es_breadth: return std::make_unique<breadth_first_todo_set>(init);
933 81 : case lps::es_depth: return std::make_unique<depth_first_todo_set>(init);
934 0 : case lps::es_highway: return std::make_unique<highway_todo_set>(init, m_options.highway_todo_max);
935 0 : default: throw mcrl2::runtime_error("unsupported search strategy");
936 : }
937 : }
938 :
939 : template <typename ForwardIterator>
940 210 : std::unique_ptr<todo_set> make_todo_set(ForwardIterator first, ForwardIterator last)
941 : {
942 210 : switch (m_options.search_strategy)
943 : {
944 117 : case lps::es_breadth: return std::make_unique<breadth_first_todo_set>(first, last);
945 93 : case lps::es_depth: return std::make_unique<depth_first_todo_set>(first, last);
946 0 : case lps::es_highway: return std::make_unique<highway_todo_set>(first, last, m_options.highway_todo_max);
947 0 : default: throw mcrl2::runtime_error("unsupported search strategy");
948 : }
949 : }
950 :
951 202 : data::rewriter construct_rewriter(const Specification& lpsspec, bool remove_unused_rewrite_rules)
952 : {
953 202 : if (remove_unused_rewrite_rules)
954 : {
955 : return data::rewriter(lpsspec.data(),
956 0 : data::used_data_equation_selector(lpsspec.data(), add_real_operators(lps::find_function_symbols(lpsspec)), lpsspec.global_variables(), false),
957 0 : m_options.rewrite_strategy);
958 : }
959 : else
960 : {
961 202 : return data::rewriter(lpsspec.data(), m_options.rewrite_strategy);
962 : }
963 : }
964 :
965 487 : bool is_confluent_tau(const multi_action& a)
966 : {
967 487 : if (a.actions().empty())
968 : {
969 48 : return m_options.confluence_action == "tau";
970 : }
971 439 : else if (a.actions().size() == 1)
972 : {
973 427 : return std::string(a.actions().front().label().name()) == m_options.confluence_action;
974 : }
975 12 : return false;
976 : }
977 :
978 : public:
979 202 : explorer(const Specification& lpsspec, const explorer_options& options_)
980 202 : : m_options(options_),
981 202 : m_global_rewr(construct_rewriter(lpsspec, m_options.remove_unused_rewrite_rules)),
982 202 : m_global_enumerator(m_global_rewr, lpsspec.data(), m_global_rewr, m_global_id_generator, false),
983 202 : m_global_lpsspec(preprocess(lpsspec)),
984 404 : m_discovered(m_options.number_of_threads)
985 : {
986 202 : const data::variable_list& params = m_global_lpsspec.process().process_parameters();
987 202 : m_process_parameters = std::vector<data::variable>(params.begin(), params.end());
988 202 : m_n = m_process_parameters.size();
989 202 : timed_state.resize(m_n + 1);
990 202 : m_initial_state = m_global_lpsspec.initial_process().expressions();
991 202 : m_initial_distribution = initial_distribution(m_global_lpsspec);
992 :
993 : // Split the summands in regular and confluent summands
994 202 : const auto& lpsspec_summands = m_global_lpsspec.process().action_summands();
995 689 : for (std::size_t i = 0; i < lpsspec_summands.size(); i++)
996 : {
997 487 : const auto& summand = lpsspec_summands[i];
998 487 : auto cache_strategy = m_options.cached ? (m_options.global_cache ? lps::caching::global : lps::caching::local) : lps::caching::none;
999 487 : if (is_confluent_tau(summand.multi_action()))
1000 : {
1001 6 : m_confluent_summands.emplace_back(summand, i, m_global_lpsspec.process().process_parameters(), cache_strategy);
1002 : }
1003 : else
1004 : {
1005 481 : m_regular_summands.emplace_back(summand, i, m_global_lpsspec.process().process_parameters(), cache_strategy);
1006 : }
1007 : }
1008 202 : }
1009 :
1010 202 : ~explorer() = default;
1011 :
1012 : // Get the initial state of the specification.
1013 8 : const data::data_expression_list& initial_state() const
1014 : {
1015 8 : return m_initial_state;
1016 : }
1017 :
1018 : // Make the rewriter available to be used in a class that uses this explorer class.
1019 20 : const data::rewriter& get_rewriter() const
1020 : {
1021 20 : return m_global_rewr;
1022 : }
1023 :
1024 : // Utility function to obtain the outgoing transitions of the current state.
1025 : // Should not be used concurrently.
1026 2 : std::list<transition> out_edges(const state& s)
1027 : {
1028 2 : return out_edges(s, m_regular_summands, m_confluent_summands, m_global_sigma, m_global_rewr, m_global_enumerator, m_global_id_generator);
1029 : }
1030 :
1031 : // Utility function to obtain the outgoing transitions of the current state.
1032 : // Only transitions for the summand with the indicated index are generated.
1033 : // Should not be used concurrently.
1034 24 : std::list<transition> out_edges(const state& s, const std::size_t summand_index)
1035 : {
1036 24 : assert(summand_index<m_regular_summands.size());
1037 : return out_edges(s,
1038 48 : std::vector(1, m_regular_summands[summand_index]),
1039 24 : m_confluent_summands,
1040 72 : m_global_sigma, m_global_rewr, m_global_enumerator, m_global_id_generator);
1041 : }
1042 :
1043 : // Returns the concatenation of s and [t]
1044 18 : void make_timed_state(state& result, const state& s, const data::data_expression& t) const
1045 : {
1046 18 : std::copy(s.begin(), s.end(), timed_state.begin());
1047 18 : timed_state.back() = t;
1048 18 : lps::make_state(result, timed_state.begin(), m_n + 1);
1049 18 : }
1050 :
1051 : state_type make_state(const state& s) const
1052 : {
1053 : if constexpr (Stochastic)
1054 : {
1055 : return stochastic_state(s);
1056 : }
1057 : else
1058 : {
1059 : return s;
1060 : }
1061 : }
1062 :
1063 18 : const state_type& make_state(const stochastic_state& s) const
1064 : {
1065 18 : return s;
1066 : }
1067 :
1068 : template <
1069 : typename StateType,
1070 : typename SummandSequence,
1071 : typename DiscoverState = utilities::skip,
1072 : typename ExamineTransition = utilities::skip,
1073 : typename StartState = utilities::skip,
1074 : typename FinishState = utilities::skip,
1075 : typename DiscoverInitialState = utilities::skip
1076 : >
1077 192 : void generate_state_space_thread(
1078 : std::unique_ptr<todo_set>& todo,
1079 : const std::size_t thread_index,
1080 : std::atomic<std::size_t>& number_of_active_processes,
1081 : std::atomic<std::size_t>& number_of_idle_processes,
1082 : const SummandSequence& regular_summands,
1083 : const SummandSequence& confluent_summands,
1084 : indexed_set_for_states_type& discovered,
1085 : DiscoverState discover_state,
1086 : ExamineTransition examine_transition,
1087 : StartState start_state,
1088 : FinishState finish_state,
1089 : data::rewriter thread_rewr,
1090 : data::mutable_indexed_substitution<> thread_sigma // This is intentionally a copy.
1091 : )
1092 : {
1093 192 : thread_rewr.thread_initialise();
1094 192 : mCRL2log(log::debug) << "Start thread " << thread_index << ".\n";
1095 384 : data::enumerator_identifier_generator thread_id_generator("t_");;
1096 192 : data::data_specification thread_data_specification = m_global_lpsspec.data(); /// XXXX Nodig??
1097 192 : data::enumerator_algorithm<> thread_enumerator(thread_rewr, thread_data_specification, thread_rewr, thread_id_generator, false);
1098 192 : state current_state;
1099 192 : data::data_expression condition; // The condition is used often, and it is effective not to declare it whenever it is used.
1100 192 : state_type state_; // The same holds for state.
1101 192 : std::vector<state> dummy;
1102 192 : std::unique_ptr<todo_set> thread_todo=make_todo_set(dummy.begin(),dummy.end()); // The new states for each process are temporarily stored in this vector for each thread.
1103 192 : atermpp::term_appl<data::data_expression> key;
1104 :
1105 192 : if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.lock();
1106 396 : while (number_of_active_processes>0 || !todo->empty())
1107 : {
1108 204 : assert(m_must_abort || thread_todo->empty());
1109 :
1110 204 : if (!todo->empty())
1111 : {
1112 204 : todo->choose_element(current_state);
1113 204 : thread_todo->insert(current_state);
1114 204 : if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.unlock();
1115 :
1116 1558 : while (!thread_todo->empty() && !m_must_abort.load(std::memory_order_relaxed))
1117 : {
1118 1354 : thread_todo->choose_element(current_state);
1119 1354 : std::size_t s_index = discovered.index(current_state,thread_index);
1120 1354 : start_state(thread_index, current_state, s_index);
1121 1354 : data::add_assignments(thread_sigma, m_process_parameters, current_state);
1122 13310 : for (const explorer_summand& summand: regular_summands)
1123 : {
1124 11956 : generate_transitions(
1125 : summand,
1126 : confluent_summands,
1127 : thread_sigma,
1128 : thread_rewr,
1129 : condition,
1130 : state_,
1131 : key,
1132 : thread_enumerator,
1133 : thread_id_generator,
1134 2650 : [&](const lps::multi_action& a, const state_type& s1)
1135 : {
1136 : if constexpr (Timed)
1137 : {
1138 12 : const data::data_expression& t = current_state[m_n];
1139 12 : if (a.has_time() && less_equal(a.time(), t, thread_sigma, thread_rewr))
1140 : {
1141 0 : return;
1142 : }
1143 : }
1144 : if constexpr (Stochastic)
1145 : {
1146 190 : std::list<std::size_t> s1_index;
1147 190 : const auto& S1 = s1.states;
1148 : // TODO: join duplicate targets
1149 564 : for (const state& s1_: S1)
1150 : {
1151 374 : std::size_t k = discovered.index(s1_,thread_index);
1152 374 : if (k >= discovered.size())
1153 : {
1154 160 : thread_todo->insert(s1_);
1155 160 : k = discovered.insert(s1_, thread_index).first;
1156 160 : discover_state(thread_index, s1_, k);
1157 : }
1158 374 : s1_index.push_back(k);
1159 : }
1160 :
1161 190 : examine_transition(thread_index, m_options.number_of_threads, current_state, s_index, a, s1, s1_index, summand.index);
1162 190 : }
1163 : else
1164 : {
1165 : std::size_t s1_index;
1166 : if constexpr (Timed)
1167 : {
1168 12 : s1_index = discovered.index(s1,thread_index);
1169 12 : if (s1_index >= discovered.size())
1170 : {
1171 12 : const data::data_expression& t = current_state[m_n];
1172 12 : const data::data_expression& t1 = a.has_time() ? a.time() : t;
1173 12 : make_timed_state(state_, s1, t1);
1174 12 : s1_index = discovered.insert(state_, thread_index).first;
1175 12 : discover_state(thread_index, state_, s1_index);
1176 12 : thread_todo->insert(state_);
1177 : }
1178 : }
1179 : else
1180 : {
1181 2334 : std::pair<std::size_t,bool> p = discovered.insert(s1, thread_index);
1182 2334 : s1_index=p.first;
1183 2334 : if (p.second) // Index is newly added.
1184 : {
1185 978 : discover_state(thread_index, s1, s1_index);
1186 978 : thread_todo->insert(s1);
1187 : }
1188 : }
1189 :
1190 2346 : examine_transition(thread_index, m_options.number_of_threads, current_state, s_index, a, s1, s1_index, summand.index);
1191 : }
1192 : }
1193 : );
1194 : }
1195 :
1196 1354 : if (number_of_idle_processes>0 && thread_todo->size()>1)
1197 : {
1198 0 : if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.lock();
1199 :
1200 0 : if (todo->size() < m_options.number_of_threads)
1201 : {
1202 : // move 25% of the states of this thread to the global todo buffer.
1203 0 : for(std::size_t i=0; i<std::min(thread_todo->size()-1,1+(thread_todo->size()/4)); ++i)
1204 : {
1205 0 : thread_todo->choose_element(current_state);
1206 0 : todo->insert(current_state);
1207 : }
1208 : }
1209 :
1210 0 : if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.unlock();
1211 : }
1212 :
1213 1354 : finish_state(thread_index, m_options.number_of_threads, current_state, s_index, thread_todo->size());
1214 1354 : thread_todo->finish_state();
1215 : }
1216 : }
1217 : else
1218 : {
1219 0 : if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.unlock();
1220 : }
1221 : // Check whether all processes are ready. If so the number_of_active_processes becomes 0.
1222 : // Otherwise, this thread becomes active again, and tries to see whether the todo buffer is
1223 : // not empty, to take up more work.
1224 204 : number_of_active_processes--;
1225 204 : number_of_idle_processes++;
1226 204 : if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads > 1) m_exclusive_state_access.lock();
1227 :
1228 204 : assert(thread_todo->empty() || m_must_abort);
1229 204 : if (todo->empty())
1230 : {
1231 192 : if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads > 1) m_exclusive_state_access.unlock();
1232 192 : std::this_thread::sleep_for(std::chrono::milliseconds(100));
1233 192 : if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.lock();
1234 : }
1235 204 : if (number_of_active_processes>0 || !todo->empty())
1236 : {
1237 12 : number_of_active_processes++;
1238 : }
1239 204 : number_of_idle_processes--;
1240 : }
1241 192 : mCRL2log(log::debug) << "Stop thread " << thread_index << ".\n";
1242 192 : if (mcrl2::utilities::detail::GlobalThreadSafe && m_options.number_of_threads>1) m_exclusive_state_access.unlock();
1243 :
1244 192 : } // end generate_state_space_thread.
1245 :
1246 :
1247 :
1248 : // pre: s0 is in normal form
1249 : template <
1250 : typename StateType,
1251 : typename SummandSequence,
1252 : typename DiscoverState = utilities::skip,
1253 : typename ExamineTransition = utilities::skip,
1254 : typename StartState = utilities::skip,
1255 : typename FinishState = utilities::skip,
1256 : typename DiscoverInitialState = utilities::skip
1257 : >
1258 192 : void generate_state_space(
1259 : bool recursive,
1260 : const StateType& s0,
1261 : const SummandSequence& regular_summands,
1262 : const SummandSequence& confluent_summands,
1263 : indexed_set_for_states_type& discovered,
1264 : DiscoverState discover_state = DiscoverState(),
1265 : ExamineTransition examine_transition = ExamineTransition(),
1266 : StartState start_state = StartState(),
1267 : FinishState finish_state = FinishState(),
1268 : DiscoverInitialState discover_initial_state = DiscoverInitialState()
1269 : )
1270 : {
1271 192 : utilities::mcrl2_unused(discover_initial_state); // silence unused parameter warning
1272 :
1273 192 : const std::size_t number_of_threads=m_options.number_of_threads;
1274 192 : assert(number_of_threads>0);
1275 192 : const std::size_t initialisation_thread_index= (number_of_threads==1?0:1);
1276 192 : m_recursive = recursive;
1277 192 : std::unique_ptr<todo_set> todo;
1278 192 : discovered.clear(initialisation_thread_index);
1279 :
1280 : if constexpr (Stochastic)
1281 : {
1282 18 : state_type s0_ = make_state(s0);
1283 18 : const auto& S = s0_.states;
1284 18 : todo = make_todo_set(S.begin(), S.end());
1285 18 : discovered.clear(initialisation_thread_index);
1286 18 : std::list<std::size_t> s0_index;
1287 48 : for (const state& s: S)
1288 : {
1289 : // TODO: join duplicate targets
1290 30 : std::size_t s_index = discovered.index(s, initialisation_thread_index);
1291 30 : if (s_index >= discovered.size())
1292 : {
1293 30 : s_index = discovered.insert(s, initialisation_thread_index).first;
1294 30 : discover_state(initialisation_thread_index, s, s_index);
1295 : }
1296 30 : s0_index.push_back(s_index);
1297 : }
1298 18 : discover_initial_state(s0_, s0_index);
1299 18 : }
1300 : else
1301 : {
1302 174 : todo = make_todo_set(s0);
1303 174 : std::size_t s0_index = discovered.insert(s0, initialisation_thread_index).first;
1304 174 : discover_state(initialisation_thread_index, s0, s0_index);
1305 : }
1306 :
1307 192 : std::atomic<std::size_t> number_of_active_processes=number_of_threads;
1308 192 : std::atomic<std::size_t> number_of_idle_processes=0;
1309 :
1310 192 : if (number_of_threads>1)
1311 : {
1312 0 : std::vector<std::thread> threads;
1313 0 : threads.reserve(number_of_threads);
1314 0 : for(std::size_t i=1; i<=number_of_threads; ++i) // Threads are numbered from 1 to number_of_threads. Thread number 0 is reserved as
1315 : // indicator for a sequential implementation.
1316 : {
1317 0 : threads.emplace_back([&, i](){
1318 : generate_state_space_thread< StateType, SummandSequence,
1319 : DiscoverState, ExamineTransition,
1320 : StartState, FinishState,
1321 : DiscoverInitialState >
1322 0 : (todo,
1323 : i, number_of_active_processes, number_of_idle_processes,
1324 : regular_summands,confluent_summands,discovered, discover_state,
1325 : examine_transition, start_state, finish_state,
1326 0 : m_global_rewr.clone(), m_global_sigma); } ); // It is essential that the rewriter is cloned as
1327 : // one rewriter cannot be used in parallel.
1328 : }
1329 :
1330 0 : for(std::size_t i=1; i<=number_of_threads; ++i)
1331 : {
1332 0 : threads[i-1].join();
1333 : }
1334 0 : }
1335 : else
1336 : {
1337 : // Single threaded variant. Do not start a separate thread.
1338 192 : assert(number_of_threads==1);
1339 192 : const std::size_t single_thread_index=0;
1340 : generate_state_space_thread< StateType, SummandSequence,
1341 : DiscoverState, ExamineTransition,
1342 : StartState, FinishState,
1343 : DiscoverInitialState >
1344 192 : (todo,single_thread_index,number_of_active_processes, number_of_idle_processes,
1345 : regular_summands,confluent_summands,discovered, discover_state,
1346 : examine_transition, start_state, finish_state,
1347 192 : m_global_rewr, m_global_sigma);
1348 : }
1349 :
1350 192 : m_must_abort = false;
1351 192 : }
1352 :
1353 : /// \brief Generates the state space, and reports all discovered states and transitions by means of callback
1354 : /// functions.
1355 : /// \param discover_state Is invoked when a state is encountered for the first time.
1356 : /// \param examine_transition Is invoked on every transition.
1357 : /// \param start_state Is invoked on a state right before its outgoing transitions are being explored.
1358 : /// \param finish_state Is invoked on a state after all of its outgoing transitions have been explored.
1359 : template <
1360 : typename DiscoverState = utilities::skip,
1361 : typename ExamineTransition = utilities::skip,
1362 : typename StartState = utilities::skip,
1363 : typename FinishState = utilities::skip,
1364 : typename DiscoverInitialState = utilities::skip
1365 : >
1366 192 : void generate_state_space(
1367 : bool recursive,
1368 : DiscoverState discover_state = DiscoverState(),
1369 : ExamineTransition examine_transition = ExamineTransition(),
1370 : StartState start_state = StartState(),
1371 : FinishState finish_state = FinishState(),
1372 : DiscoverInitialState discover_initial_state = DiscoverInitialState()
1373 : )
1374 : {
1375 192 : state_type s0;
1376 : if constexpr (Stochastic)
1377 : {
1378 18 : compute_stochastic_state(s0, m_initial_distribution, m_initial_state, m_global_sigma, m_global_rewr, m_global_enumerator);
1379 : }
1380 : else
1381 : {
1382 174 : compute_state(s0,m_initial_state,m_global_sigma, m_global_rewr);
1383 174 : if (!m_confluent_summands.empty())
1384 : {
1385 6 : s0 = find_representative(s0, m_confluent_summands, m_global_sigma, m_global_rewr, m_global_enumerator, m_global_id_generator);
1386 : }
1387 : if constexpr (Timed)
1388 : {
1389 6 : make_timed_state(s0, s0, data::sort_real::real_zero());
1390 : }
1391 : }
1392 192 : generate_state_space(recursive, s0, m_regular_summands, m_confluent_summands, m_discovered, discover_state,
1393 : examine_transition, start_state, finish_state, discover_initial_state);
1394 192 : }
1395 :
1396 : /// \brief Generates outgoing transitions for a given state.
1397 0 : std::vector<std::pair<lps::multi_action, state_type>> generate_transitions(
1398 : const state& d0,
1399 : data::mutable_indexed_substitution<>& sigma,
1400 : data::rewriter& rewr,
1401 : data::enumerator_algorithm<>& enumerator,
1402 : data::enumerator_identifier_generator& id_generator)
1403 : {
1404 0 : data::data_expression_list process_parameter_undo = process_parameter_values(sigma);
1405 0 : std::vector<std::pair<lps::multi_action, state_type>> result;
1406 0 : data::add_assignments(sigma, m_process_parameters, d0);
1407 0 : data::data_expression condition;
1408 0 : atermpp::term_appl<data::data_expression> key;
1409 0 : state_type state;
1410 0 : for (const explorer_summand& summand: m_regular_summands)
1411 : {
1412 0 : generate_transitions(
1413 : summand,
1414 0 : m_confluent_summands,
1415 : sigma,
1416 : rewr,
1417 : condition,
1418 : state,
1419 : key,
1420 : enumerator,
1421 : id_generator,
1422 0 : [&](const lps::multi_action& a, const state_type& d1)
1423 : {
1424 0 : result.emplace_back(lps::multi_action(a.actions(), a.time()), d1);
1425 : }
1426 : );
1427 : }
1428 0 : set_process_parameter_values(process_parameter_undo, sigma);
1429 0 : return result;
1430 0 : }
1431 :
1432 : /// \brief Generates outgoing transitions for a given state, using the global substitution, rewriter, enumerator and id_generator.
1433 : /// \details This function is not suitable to be used in parallel threads, but can only be used for pre or post processing.
1434 0 : std::vector<std::pair<lps::multi_action, state_type>> generate_transitions(
1435 : const state& d0)
1436 : {
1437 0 : assert(m_options.number_of_threads==1); // A global rewriter is invoked, and this can only happen in a single threaded setting.
1438 0 : return generate_transitions(d0, m_global_sigma, m_global_rewr, m_global_enumerator, m_global_id_generator);
1439 : }
1440 :
1441 : /// \brief Generates outgoing transitions for a given state.
1442 : std::vector<std::pair<lps::multi_action, state>> generate_transitions(
1443 : const data::data_expression_list& init,
1444 : data::mutable_indexed_substitution<>& sigma,
1445 : data::rewriter& rewr)
1446 : {
1447 : state d0;
1448 : compute_state(d0,init,sigma,rewr);
1449 : return generate_transitions(d0);
1450 : }
1451 :
1452 : /// \brief Generates outgoing transitions for a given state, reachable via the summand with index i.
1453 : std::vector<std::pair<lps::multi_action, state_type>> generate_transitions(
1454 : const data::data_expression_list& init,
1455 : std::size_t i,
1456 : data::mutable_indexed_substitution<>& sigma,
1457 : data::rewriter& rewr,
1458 : data::data_expression& condition,
1459 : state_type& d0,
1460 : data::enumerator_algorithm<>& enumerator,
1461 : data::enumerator_identifier_generator& id_generator)
1462 : {
1463 : data::data_expression_list process_parameter_undo = process_parameter_values(sigma);
1464 : compute_state(d0,init,sigma,rewr);
1465 : std::vector<std::pair<lps::multi_action, state_type>> result;
1466 : data::add_assignments(sigma, m_process_parameters, d0);
1467 : generate_transitions(
1468 : m_regular_summands[i],
1469 : m_confluent_summands,
1470 : sigma,
1471 : rewr,
1472 : condition,
1473 : d0,
1474 : enumerator,
1475 : id_generator,
1476 : [&](const lps::multi_action& a, const state_type& d1)
1477 : {
1478 : result.emplace_back(lps::multi_action(a), d1);
1479 : }
1480 : );
1481 : data::remove_assignments(sigma, m_regular_summands[i].variables);
1482 : set_process_parameter_values(process_parameter_undo, sigma);
1483 : return result;
1484 : }
1485 :
1486 : // pre: s0 is in normal form
1487 : // N.B. Does not support stochastic specifications!
1488 : template <
1489 : typename SummandSequence,
1490 : typename DiscoverState = utilities::skip,
1491 : typename ExamineTransition = utilities::skip,
1492 : typename TreeEdge = utilities::skip,
1493 : typename BackEdge = utilities::skip,
1494 : typename ForwardOrCrossEdge = utilities::skip,
1495 : typename FinishState = utilities::skip
1496 : >
1497 0 : void generate_state_space_dfs_recursive(
1498 : const state& s0,
1499 : std::unordered_set<state> gray,
1500 : std::unordered_set<state>& discovered,
1501 : const SummandSequence& regular_summands,
1502 : const SummandSequence& confluent_summands,
1503 : DiscoverState discover_state = DiscoverState(),
1504 : ExamineTransition examine_transition = ExamineTransition(),
1505 : TreeEdge tree_edge = TreeEdge(),
1506 : BackEdge back_edge = BackEdge(),
1507 : ForwardOrCrossEdge forward_or_cross_edge = ForwardOrCrossEdge(),
1508 : FinishState finish_state = FinishState()
1509 : )
1510 : {
1511 : using utilities::detail::contains;
1512 :
1513 : // invariants:
1514 : // - s not in discovered => color(s) = white
1515 : // - s in discovered && s in gray => color(s) = gray
1516 : // - s in discovered && s not in gray => color(s) = black
1517 :
1518 0 : gray.insert(s0);
1519 0 : discovered.insert(s0);
1520 0 : discover_state(0, s0);
1521 :
1522 0 : if (m_options.number_of_threads>1)
1523 : {
1524 0 : throw mcrl2::runtime_error("Dfs exploration is not thread safe.");
1525 : }
1526 :
1527 0 : for (const transition& tr: out_edges(s0, regular_summands, confluent_summands, m_global_sigma, m_global_rewr, m_global_enumerator, m_global_id_generator))
1528 : {
1529 0 : if (m_must_abort)
1530 : {
1531 0 : break;
1532 : }
1533 :
1534 0 : const auto&[a, s1] = tr;
1535 0 : const std::size_t number_of_threads = 1;
1536 0 : examine_transition(0, number_of_threads, s0, a, s1); // TODO MAKE THREAD SAFE
1537 :
1538 0 : if (discovered.find(s1) == discovered.end())
1539 : {
1540 0 : tree_edge(s0, a, s1);
1541 : if constexpr (Timed)
1542 : {
1543 0 : const data::data_expression& t = s0[m_n];
1544 0 : const data::data_expression& t1 = a.has_time() ? a.time() : t;
1545 0 : state s1_at_t1;
1546 0 : make_timed_state(s1_at_t1, s1, t1);
1547 0 : discovered.insert(s1_at_t1);
1548 0 : }
1549 : else
1550 : {
1551 0 : discovered.insert(s1);
1552 : }
1553 0 : generate_state_space_dfs_recursive(s1, gray, discovered, regular_summands, confluent_summands, discover_state, examine_transition, tree_edge, back_edge, forward_or_cross_edge, finish_state);
1554 : }
1555 0 : else if (contains(gray, s1))
1556 : {
1557 0 : back_edge(s0, a, s1);
1558 : }
1559 : else
1560 : {
1561 0 : forward_or_cross_edge(s0, a, s1);
1562 : }
1563 : }
1564 0 : gray.erase(s0);
1565 :
1566 0 : finish_state(0, s0); // TODO MAKE THREAD SAFE
1567 0 : }
1568 :
1569 : template <
1570 : typename DiscoverState = utilities::skip,
1571 : typename ExamineTransition = utilities::skip,
1572 : typename TreeEdge = utilities::skip,
1573 : typename BackEdge = utilities::skip,
1574 : typename ForwardOrCrossEdge = utilities::skip,
1575 : typename FinishState = utilities::skip
1576 : >
1577 : void generate_state_space_dfs_recursive(
1578 : bool recursive,
1579 : DiscoverState discover_state = DiscoverState(),
1580 : ExamineTransition examine_transition = ExamineTransition(),
1581 : TreeEdge tree_edge = TreeEdge(),
1582 : BackEdge back_edge = BackEdge(),
1583 : ForwardOrCrossEdge forward_or_cross_edge = ForwardOrCrossEdge(),
1584 : FinishState finish_state = FinishState()
1585 : )
1586 : {
1587 : m_recursive = recursive;
1588 : std::unordered_set<state> gray;
1589 : std::unordered_set<state> discovered;
1590 :
1591 : state s0;
1592 : compute_state(s0, m_initial_state, m_global_sigma, m_global_rewr);
1593 : if (!m_confluent_summands.empty())
1594 : {
1595 : s0 = find_representative(s0, m_confluent_summands, m_global_sigma, m_global_rewr, m_global_enumerator, m_global_id_generator);
1596 : }
1597 : if constexpr (Timed)
1598 : {
1599 : s0 = make_timed_state(s0, data::sort_real::real_zero());
1600 : }
1601 : generate_state_space_dfs_recursive(s0, gray, discovered, m_regular_summands, m_confluent_summands, discover_state, examine_transition, tree_edge, back_edge, forward_or_cross_edge, finish_state);
1602 : m_recursive = false;
1603 : }
1604 :
1605 : // pre: s0 is in normal form
1606 : // N.B. Does not support stochastic specifications!
1607 : template <
1608 : typename SummandSequence,
1609 : typename DiscoverState = utilities::skip,
1610 : typename ExamineTransition = utilities::skip,
1611 : typename TreeEdge = utilities::skip,
1612 : typename BackEdge = utilities::skip,
1613 : typename ForwardOrCrossEdge = utilities::skip,
1614 : typename FinishState = utilities::skip
1615 : >
1616 0 : void generate_state_space_dfs_iterative(
1617 : const state& s0,
1618 : std::unordered_set<state>& discovered,
1619 : const SummandSequence& regular_summands,
1620 : const SummandSequence& confluent_summands,
1621 : DiscoverState discover_state = DiscoverState(),
1622 : ExamineTransition examine_transition = ExamineTransition(),
1623 : TreeEdge tree_edge = TreeEdge(),
1624 : BackEdge back_edge = BackEdge(),
1625 : ForwardOrCrossEdge forward_or_cross_edge = ForwardOrCrossEdge(),
1626 : FinishState finish_state = FinishState()
1627 : )
1628 : {
1629 : using utilities::detail::contains;
1630 :
1631 : // invariants:
1632 : // - s not in discovered => color(s) = white
1633 : // - s in discovered && s in todo => color(s) = gray
1634 : // - s in discovered && s not in todo => color(s) = black
1635 :
1636 0 : std::vector<std::pair<state, std::list<transition>>> todo;
1637 :
1638 0 : if (m_options.number_of_threads>0)
1639 : {
1640 0 : mcrl2::runtime_error("DFS exploration cannot be performend with multiple threads.");
1641 : }
1642 0 : todo.emplace_back(s0, out_edges(s0, regular_summands, confluent_summands, m_global_sigma, m_global_rewr, m_global_enumerator, m_global_id_generator));
1643 0 : discovered.insert(s0);
1644 0 : discover_state(s0);
1645 :
1646 0 : while (!todo.empty() && !m_must_abort)
1647 : {
1648 0 : const state* s = &todo.back().first;
1649 0 : std::list<transition>* E = &todo.back().second;
1650 0 : while (!E->empty())
1651 : {
1652 0 : transition e = E->front();
1653 0 : const auto& a = e.action;
1654 0 : const auto& s1 = e.state;
1655 0 : E->pop_front();
1656 0 : examine_transition(0, 1, *s, a, s1); // TODO: MAKE THREAD SAFE.
1657 :
1658 0 : if (discovered.find(s1) == discovered.end())
1659 : {
1660 0 : tree_edge(*s, a, s1);
1661 : if constexpr (Timed)
1662 : {
1663 0 : const data::data_expression& t = (*s)[m_n];
1664 0 : const data::data_expression& t1 = a.has_time() ? a.time() : t;
1665 0 : state s1_at_t1;
1666 0 : make_timed_state(s1_at_t1, s1, t1);
1667 0 : discovered.insert(s1_at_t1);
1668 0 : discover_state(s1_at_t1);
1669 0 : }
1670 : else
1671 : {
1672 0 : discovered.insert(s1);
1673 0 : discover_state(s1);
1674 : }
1675 0 : todo.emplace_back(s1, out_edges(s1, regular_summands, confluent_summands, m_global_sigma, m_global_rewr, m_global_enumerator, m_global_id_generator));
1676 0 : s = &todo.back().first;
1677 0 : E = &todo.back().second;
1678 : }
1679 : else
1680 : {
1681 0 : if (std::find_if(todo.begin(), todo.end(), [&](const std::pair<state, std::list<transition>>& p) { return s1 == p.first; }) != todo.end())
1682 : {
1683 0 : back_edge(*s, a, s1);
1684 : }
1685 : else
1686 : {
1687 0 : forward_or_cross_edge(*s, a, s1);
1688 : }
1689 : }
1690 : }
1691 0 : todo.pop_back();
1692 0 : finish_state(0, *s); // TODO: Make thread safe
1693 : }
1694 0 : m_must_abort = false;
1695 0 : }
1696 :
1697 : template <
1698 : typename DiscoverState = utilities::skip,
1699 : typename ExamineTransition = utilities::skip,
1700 : typename TreeEdge = utilities::skip,
1701 : typename BackEdge = utilities::skip,
1702 : typename ForwardOrCrossEdge = utilities::skip,
1703 : typename FinishState = utilities::skip
1704 : >
1705 : void generate_state_space_dfs_iterative(
1706 : bool recursive,
1707 : DiscoverState discover_state = DiscoverState(),
1708 : ExamineTransition examine_transition = ExamineTransition(),
1709 : TreeEdge tree_edge = TreeEdge(),
1710 : BackEdge back_edge = BackEdge(),
1711 : ForwardOrCrossEdge forward_or_cross_edge = ForwardOrCrossEdge(),
1712 : FinishState finish_state = FinishState()
1713 : )
1714 : {
1715 : m_recursive = recursive;
1716 : std::unordered_set<state> discovered;
1717 :
1718 : state s0;
1719 : compute_state(s0,m_initial_state,m_global_sigma, m_global_rewr);
1720 : if (!m_confluent_summands.empty())
1721 : {
1722 : s0 = find_representative(s0, m_confluent_summands, m_global_sigma, m_global_rewr, m_global_enumerator, m_global_id_generator);
1723 : }
1724 : if constexpr (Timed)
1725 : {
1726 : s0 = make_timed_state(s0, data::sort_real::real_zero());
1727 : }
1728 : generate_state_space_dfs_iterative(s0, discovered, m_regular_summands, m_confluent_summands, discover_state, examine_transition, tree_edge, back_edge, forward_or_cross_edge, finish_state);
1729 : m_recursive = false;
1730 : }
1731 :
1732 : /// \brief Abort the state space generation
1733 0 : void abort() override
1734 : {
1735 0 : m_must_abort = true;
1736 0 : }
1737 :
1738 : /// \brief Returns a mapping containing all discovered states.
1739 3092 : const indexed_set_for_states_type& state_map() const
1740 : {
1741 3092 : return m_discovered;
1742 : }
1743 :
1744 0 : const std::vector<explorer_summand>& regular_summands() const
1745 : {
1746 0 : return m_regular_summands;
1747 : }
1748 :
1749 0 : const std::vector<explorer_summand>& confluent_summands() const
1750 : {
1751 0 : return m_confluent_summands;
1752 : }
1753 :
1754 : const std::vector<data::variable>& process_parameters() const
1755 : {
1756 : return m_process_parameters;
1757 : }
1758 :
1759 18 : data::data_expression_list process_parameter_values(data::mutable_indexed_substitution<>& sigma) const
1760 : {
1761 72 : return data::data_expression_list{m_process_parameters.begin(), m_process_parameters.end(), [&](const data::variable& x) { return sigma(x); }};
1762 : }
1763 :
1764 : /// \brief Process parameter values for use in a single thread.
1765 0 : data::data_expression_list process_parameter_values() const
1766 : {
1767 0 : assert(m_options.number_of_threads==1); // Using a global sigma is not thread safe.
1768 0 : return process_parameter_values(m_global_sigma);
1769 : }
1770 18 : void set_process_parameter_values(const data::data_expression_list& values, data::mutable_indexed_substitution<>& sigma)
1771 : {
1772 18 : data::add_assignments(sigma, m_process_parameters, values);
1773 18 : }
1774 :
1775 0 : void set_process_parameter_values(const data::data_expression_list& values)
1776 : {
1777 0 : assert(m_options.number_of_threads==1); // Using a global sigma is not thread safe.
1778 0 : set_process_parameter_values(values, m_global_sigma);
1779 0 : }
1780 : };
1781 :
1782 : } // namespace mcrl2::lps
1783 :
1784 : #endif // MCRL2_LPS_EXPLORER_H
|
