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