mCRL2
Loading...
Searching...
No Matches
state_space_generator.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_LTS_STATE_SPACE_GENERATOR_H
13#define MCRL2_LTS_STATE_SPACE_GENERATOR_H
14
15#include "mcrl2/lps/explorer.h"
16#include "mcrl2/lts/trace.h"
17
18namespace mcrl2::lts
19{
20
21inline
22std::ostream& operator<<(std::ostream& out, const lps::state& s)
23{
24 return out << atermpp::pp(s);
25}
26
27inline
29{
30 return s;
31}
32
33inline
35{
36 return s.states.front();
37}
38
39namespace detail
40{
41
42inline
44 class trace& tr,
45 const std::string& filename
46)
47{
48 try
49 {
50 tr.save(filename);
51 mCRL2log(log::info) << " and saved trace to '" << filename << "'";
52 return true;
53 }
54 catch(...)
55 {
56 mCRL2log(log::info) << ", but its trace could not be saved to '" << filename << "'";
57 }
58 return false;
59}
60
61inline
63 class trace& tr,
64 const std::string& filename1,
65 class trace& tr2,
66 const std::string& filename2
67)
68{
69 try
70 {
71 tr.save(filename1);
72 tr2.save(filename2);
73 mCRL2log(log::info) << " and saved traces to '" << filename1 << "' and '" << filename2 << "'";
74 }
75 catch(...)
76 {
77 mCRL2log(log::info) << ", but its traces could not be saved to '" << filename1 << "' and '" << filename2 << "'";
78 }
79}
80
81// Facility for constructing a trace to a given state.
82template <typename Explorer>
84{
85 protected:
86 Explorer& m_explorer;
87 std::map<lps::state, lps::state> m_backpointers;
88
89 // Finds a transition s0 --a--> s1, and returns a.
91 const lps::state& s1)
92 {
93 if constexpr (Explorer::is_stochastic)
94 {
95 for (const std::pair<lps::multi_action, lps::stochastic_state>& t: m_explorer.generate_transitions(s0))
96 {
97 for (const lps::state& s: t.second.states)
98 {
99 if (s == s1)
100 {
101 return t.first;
102 }
103 }
104 }
105 }
106 else
107 {
108 for (const std::pair<lps::multi_action, lps::state>& t: m_explorer.generate_transitions(s0))
109 {
110 if (t.second == s1)
111 {
112 return t.first;
113 }
114 }
115 }
116 throw mcrl2::runtime_error("no transition found in find_action");
117 }
118
119 public:
120 explicit trace_constructor(Explorer& explorer_)
121 : m_explorer(explorer_)
122 {}
123
124 // Constructs a trace ending in s, using the backpointers map.
125 class trace construct_trace(const lps::state& s)
126 {
127 std::deque<lps::state> states{ s };
128 std::deque<lps::multi_action> actions;
129 while (true)
130 {
131 const lps::state& s1 = states.front();
132 auto i = m_backpointers.find(s1);
133 if (i == m_backpointers.end())
134 {
135 break;
136 }
137 const lps::state& s0 = i->second;
138 states.push_front(s0);
139 actions.push_front(find_action(s0, s1));
140 }
141
142 class trace tr;
143 for (std::size_t i = 0; i < actions.size(); i++)
144 {
145 tr.set_state(states[i]);
146 tr.add_action(actions[i]);
147 }
148 tr.set_state(states.back());
149 return tr;
150 }
151
152 // Adds a back pointer for the given edge
153 void add_edge(const lps::state& s0, const lps::state& s1)
154 {
155 m_backpointers[s1] = s0;
156 }
157
158 void clear()
159 {
160 m_backpointers.clear();
161 }
162
163 // Providing access to the explorer should perhaps be avoided.
164 Explorer& explorer()
165 {
166 return m_explorer;
167 }
168};
169
170template <typename Explorer>
172{
173 protected:
174 const std::set<core::identifier_string>& trace_actions;
175 const std::set<lps::multi_action>& trace_multiactions;
177 const std::string& filename_prefix;
178 std::vector<bool> summand_matches;
179 std::size_t m_trace_count = 0;
180 std::size_t m_max_trace_count;
181
182 bool match_action(const lps::action_summand& summand) const
183 {
185 for (const process::action& a: summand.multi_action().actions())
186 {
187 if (contains(trace_actions, a.label().name()))
188 {
189 return true;
190 }
191 }
192 return false;
193 }
194
195 bool match_summand(std::size_t i) const
196 {
197 return summand_matches[i];
198 }
199
200 std::string create_filename(const lps::multi_action& a)
201 {
203 std::string filename = filename_prefix + "_act_" + std::to_string(m_trace_count++);
205 {
206 filename += "_" + lps::pp(a);
207 }
208 for (const process::action& a_i: a.actions())
209 {
210 if (utilities::detail::contains(trace_actions, a_i.label().name()))
211 {
212 filename += "_" + core::pp(a_i.label().name());
213 }
214 }
215 filename = filename + ".trc";
216 return filename;
217 }
218
219 public:
220 template <typename Specification>
222 const Specification& lpsspec,
223 trace_constructor<Explorer>& trace_constructor_,
224 const std::set<core::identifier_string>& trace_actions_,
225 const std::set<lps::multi_action>& trace_multiactions_,
226 const std::string& filename_prefix_,
227 std::size_t max_trace_count
228 )
229 : trace_actions(trace_actions_),
230 trace_multiactions(trace_multiactions_),
231 m_trace_constructor(trace_constructor_),
232 filename_prefix(filename_prefix_),
233 m_max_trace_count(max_trace_count)
234 {
236 const auto& summands = lpsspec.process().action_summands();
237 summand_matches.reserve(summands.size());
238 for (const auto& summand: summands)
239 {
240 summand_matches.push_back(match_action(summand));
241 }
242 }
243
244 bool detect_action(const lps::state& s0, std::size_t s0_index, const lps::multi_action& a, const lps::state& s1, std::size_t summand_index)
245 {
247 if (!match_summand(summand_index))
248 {
249 return false;
250 }
251 bool result = false;
252
253 mCRL2log(log::info) << "Action '" + lps::pp(a) + "' found (state index: " + std::to_string(s0_index) + ")";
255 {
256 class trace tr = m_trace_constructor.construct_trace(s0);
257 tr.add_action(a);
258 tr.set_state(s1);
259 std::string filename = create_filename(a);
260 save_trace(tr, filename);
261 result = true;
262 }
263 mCRL2log(log::info) << ".\n";
265 {
266 m_trace_constructor.explorer().abort();
267 }
268 return result;
269 }
270};
271
272template <typename Explorer>
274{
275 protected:
277 const std::string& filename_prefix;
278 std::size_t m_trace_count = 0;
279 std::size_t m_max_trace_count;
280
281 public:
283 trace_constructor<Explorer>& trace_constructor_,
284 const std::string& filename_prefix_,
285 std::size_t max_trace_count
286 )
287 : m_trace_constructor(trace_constructor_),
288 filename_prefix(filename_prefix_),
289 m_max_trace_count(max_trace_count)
290 {}
291
292 void detect_deadlock(const lps::state& s, std::size_t s_index)
293 {
294 mCRL2log(log::info) << "Deadlock found (state index: " + std::to_string(s_index) + ")";
296 {
297 class trace tr = m_trace_constructor.construct_trace(s);
298 std::string filename = filename_prefix + "_dlk_" + std::to_string(m_trace_count++) + ".trc";
299 save_trace(tr, filename);
300 }
302 {
303 m_trace_constructor.explorer().abort();
304 }
305 mCRL2log(log::info) << ".\n";
306 }
307};
308
309template <typename Explorer>
311{
312 protected:
314 const std::string& filename_prefix;
315 std::vector<std::map<lps::multi_action, lps::state> > m_transitions_vec;
316 std::size_t m_trace_count = 0;
317 std::size_t m_max_trace_count;
318
319 public:
321 trace_constructor<Explorer>& trace_constructor_,
322 const std::string& filename_prefix_,
323 const std::size_t number_of_threads,
324 std::size_t max_trace_count = 0
325 )
326 : m_trace_constructor(trace_constructor_),
327 filename_prefix(filename_prefix_),
328 m_transitions_vec(number_of_threads+1), //Threads are number from 1 to n.
329 m_max_trace_count(max_trace_count)
330 {
331 assert(number_of_threads>0);
332 }
333
334 void start_state(std::size_t thread_index)
335 {
336 assert(thread_index<m_transitions_vec.size());
337 m_transitions_vec[thread_index].clear();
338 }
339
340 bool detect_nondeterminism(const lps::state& s0, std::size_t s0_index, const lps::multi_action& a, const lps::state& s1, std::size_t thread_index)
341 {
342 bool result = false;
343 assert(thread_index<m_transitions_vec.size());
344 auto i = m_transitions_vec[thread_index].find(a);
345 if (i == m_transitions_vec[thread_index].end())
346 {
347 m_transitions_vec[thread_index].insert(std::make_pair(a, s1));
348 }
349 else if (i->second != s1) // nondeterminism detected
350 {
351 mCRL2log(log::info) << "Nondeterministic state found (state index: " + std::to_string(s0_index) + ")";
353 {
354 class trace tr = m_trace_constructor.construct_trace(s0);
355 tr.add_action(a);
356 tr.set_state(s1);
357 std::string filename = filename_prefix + "_nondeterministic_" + std::to_string(m_trace_count++) + ".trc";
358 save_trace(tr, filename);
359 result = true;
360 }
361 mCRL2log(log::info) << ".\n";
363 {
364 m_trace_constructor.explorer().abort();
365 }
366 }
367 return result;
368 }
369};
370
371template <typename Explorer>
373{
374 public:
375 using state_type = typename Explorer::state_type;
376 using state_index_type = typename Explorer::state_index_type;
377
378 // data type for storing the last discovered states
379 using last_discovered_type = typename std::conditional<Explorer::is_stochastic, std::forward_list<lps::state>, lps::state>::type;
380
381 protected:
382 Explorer& explorer;
383 const std::string& filename_prefix;
386 std::vector<lps::explorer_summand> m_regular_summands;
387 std::vector<lps::explorer_summand> m_confluent_summands;
388 std::size_t m_trace_count = 0;
389 std::size_t m_max_trace_count;
390 std::mutex divergence_detector_mutex; // As it stands the divergence detector is sequential.
391
392 public:
394 Explorer& explorer_,
395 const std::set<core::identifier_string>& actions,
396 const std::string& filename_prefix_,
397 std::size_t max_trace_count
398 )
399 : explorer(explorer_),
400 filename_prefix(filename_prefix_),
402 m_max_trace_count(max_trace_count)
403 {
405
406 auto is_hidden = [&](const lps::explorer_summand& summand)
407 {
408 for (const process::action& a: summand.multi_action.actions())
409 {
410 if (!contains(actions, a.label().name()))
411 {
412 return false;
413 }
414 }
415 return true;
416 };
417
418 for (const lps::explorer_summand& summand: explorer.regular_summands())
419 {
420 if (is_hidden(summand))
421 {
422 m_regular_summands.push_back(summand);
423 }
424 }
425
427 {
428 if (is_hidden(summand))
429 {
430 m_confluent_summands.push_back(summand);
431 }
432 }
433 }
434
435 // Returns true if a trace was saved.
436 bool detect_divergence(const lps::state& s, std::size_t s_index, trace_constructor<Explorer>& global_trace_constructor, bool dfs_recursive = false)
437 {
439
440 bool result = false;
443
444 auto q = m_divergent_states.find(s);
445 if (q != m_divergent_states.end())
446 {
447 std::string message = "Divergent state found (state index: " + std::to_string(s_index) +
448 "), reachable from divergent state with index " + std::to_string(q->second);
449 mCRL2log(log::info) << message << ".\n";
450 m_divergent_states.erase(q);
452 return false;
453 }
454
455 std::unordered_set<lps::state> discovered;
457
458 if (dfs_recursive)
459 {
460 std::unordered_set<lps::state> gray;
462 s,
463 gray,
464 discovered,
467 utilities::skip(), // discover_state
468 utilities::skip(), // examine_transition
469 utilities::skip(), // tree_edge
470
471 // back_edge
472 [&](const lps::state& s0, const lps::multi_action& a, const state_type& s1) {
473 mCRL2log(log::info) << "Divergent state found (state index: " + std::to_string(s_index) + ")";
475 {
476 class trace tr = global_trace_constructor.construct_trace(s);
477 class trace tr_loop = m_local_trace_constructor.construct_trace(s0);
478 for (const lps::state& u: tr_loop.states())
479 {
480 m_divergent_states[u] = s_index;
481 }
482 tr_loop.add_action(a);
483 tr_loop.set_state(first_state(s1));
484 std::string filename = filename_prefix + "_divergence_" + std::to_string(m_trace_count) + ".trc";
485 std::string loop_filename = filename_prefix + "_divergence_loop" + std::to_string(m_trace_count++) + ".trc";
486 save_traces(tr, filename, tr_loop, loop_filename);
487 result = true;
488 }
489 mCRL2log(log::info) << ".\n";
490 //--- Workaround for Visual Studio 2019 ---//
491 // explorer.abort();
492 static_cast<lps::abortable&>(explorer).abort();
493 }
494 );
495 }
496 else
497 {
499 s,
500 discovered,
503 utilities::skip(), // discover_state
504 utilities::skip(), // examine_transition
505 utilities::skip(), // tree_edge
506
507 // back_edge
508 [&](const lps::state& s0, const lps::multi_action& a, const state_type& s1) {
509 mCRL2log(log::info) << "Divergent state found (state index: " + std::to_string(s_index) + ")";
511 {
512 class trace tr = global_trace_constructor.construct_trace(s);
513 class trace tr_loop = m_local_trace_constructor.construct_trace(s0);
514 for (const lps::state& u: tr_loop.states())
515 {
516 m_divergent_states[u] = s_index;
517 }
518 tr_loop.add_action(a);
519 tr_loop.set_state(first_state(s1));
520 std::string filename = filename_prefix + "_divergence_" + std::to_string(m_trace_count) + ".trc";
521 std::string loop_filename = filename_prefix + "_divergence_loop" + std::to_string(m_trace_count++) + ".trc";
522 save_traces(tr, filename, tr_loop, loop_filename);
523 result = true;
524 }
525 mCRL2log(log::info) << ".\n";
526 //--- Workaround for Visual Studio 2019 ---//
527 // explorer.abort();
528 static_cast<lps::abortable&>(explorer).abort();
529 }
530 );
531 }
532 explorer.set_process_parameter_values(process_parameter_undo);
534 {
535 explorer.abort();
536 }
538 return result;
539 }
540};
541
543{
544 protected:
545 std::size_t level = 1; // the current exploration level
546 std::size_t level_up = 1; // when count reaches level_up, the level is increased
547 std::atomic<std::size_t> count = 0;
548 std::atomic<std::size_t> transition_count = 0;
549
550 std::size_t last_state_count = 0;
551 std::size_t last_transition_count = 0;
552 std::atomic<time_t> last_log_time = time(nullptr) - 1;
553
555
556 public:
558 : search_strategy(search_strategy_)
559 {}
560
562 {
564 }
565
566 void finish_state(std::size_t state_count, std::size_t todo_list_size, std::size_t number_of_threads)
567 {
568 time_t new_log_time = 0;
569
570 static std::mutex exclusive_print_mutex;
572 {
573 ++count;
574 if (number_of_threads == 1 && count == level_up)
575 {
576 exclusive_print_mutex.lock();
577 mCRL2log(log::debug) << "Number of states at level " << level << " is " << state_count - last_state_count << "\n";
578 level++;
579 level_up = count + todo_list_size;
580 last_state_count = state_count;
582 exclusive_print_mutex.unlock();
583 }
584
585 if (time(&new_log_time) > last_log_time.load(std::memory_order_relaxed))
586 {
587 exclusive_print_mutex.lock();
588
589 last_log_time = new_log_time;
590 std::size_t lvl_states = state_count - last_state_count;
591 std::size_t lvl_transitions = transition_count - last_transition_count;
592 if (number_of_threads>1) // Levels have no meaning with multiple threads.
593 {
594 mCRL2log(log::status) << std::fixed << std::setprecision(2)
595 << state_count << "st, " << transition_count << "tr"
596 << ", explored " << 100.0 * ((float) count / state_count)
597 << "%.\n";
598 }
599 else
600 {
601 mCRL2log(log::status) << std::fixed << std::setprecision(2)
602 << state_count << "st, " << transition_count << "tr"
603 << ", explored " << 100.0 * ((float) count / state_count)
604 << "%. Last level: " << level << ", " << lvl_states << "st, "
605 << lvl_transitions << "tr.\n";
606 }
607 exclusive_print_mutex.unlock();
608 }
609 }
610 else
611 {
612 count++;
613 if (time(&new_log_time) > last_log_time.load(std::memory_order_relaxed))
614 {
615 exclusive_print_mutex.lock();
616 last_log_time = new_log_time;
617 mCRL2log(log::status) << "monitor: currently explored "
618 << count << " state" << ((count==1)?"":"s")
619 << " and " << transition_count << " transition" << ((transition_count==1)?".":"s.")
620 << std::endl;
621 exclusive_print_mutex.unlock();
622 }
623 }
624 }
625
626 void finish_exploration(std::size_t state_count, std::size_t number_of_threads)
627 {
629 {
630 mCRL2log(log::verbose) << "Done with state space generation (";
631 if (number_of_threads==1)
632 {
633 mCRL2log(log::verbose) << level-1 << " level" << ((level==2)?"":"s") << ", ";
634 }
635 mCRL2log(log::verbose) << state_count << " state" << ((state_count == 1)?"":"s")
636 << " and " << transition_count << " transition" << ((transition_count==1)?"":"s") << ")" << std::endl;
637 }
638 else
639 {
640 mCRL2log(log::verbose) << "Done with state space generation ("
641 << state_count << " state" << ((state_count == 1)?"":"s")
642 << " and " << transition_count << " transition" << ((transition_count==1)?"":"s") << ")" << std::endl;
643 }
644 }
645};
646
647} // namespace detail
648
649template <bool Stochastic, bool Timed, typename Specification>
651{
654
658
662 std::unique_ptr<detail::divergence_detector<explorer_type>> m_divergence_detector;
664
665 state_space_generator(const Specification& lpsspec, const lps::explorer_options& options_)
666 : options(options_),
667 explorer(lpsspec, options_),
669 m_action_detector(lpsspec, m_trace_constructor, options.trace_actions, options.trace_multiactions, options.trace_prefix, options.max_traces),
670 m_deadlock_detector(m_trace_constructor, options.trace_prefix, options.max_traces),
671 m_nondeterminism_detector(m_trace_constructor, options.trace_prefix, options.number_of_threads, options.max_traces),
672 m_progress_monitor(options.search_strategy)
673 {
675 {
677 std::unique_ptr<detail::divergence_detector<explorer_type>>(
682 }
683 }
684
685 bool max_states_exceeded(const std::size_t thread_index)
686 {
687 return explorer.state_map().size(thread_index) >= options.max_states;
688 }
689
691 {
692 alignas(64) size_t m_bool;
693 };
694
695 // Explore the specification passed via the constructor, and put the results in builder.
696 template <typename LTSBuilder>
697 bool explore(LTSBuilder& builder)
698 {
699 std::vector<aligned_bool> has_outgoing_transitions(options.number_of_threads+1); // thread indices start at 1.
700 const lps::state* source = nullptr;
701
702 try
703 {
705 false,
706
707 // discover_state
708 [&](const std::size_t thread_index, const lps::state& s, std::size_t s_index)
709 {
710 if (options.generate_traces && source)
711 {
712 m_trace_constructor.add_edge(*source, s);
713 }
715 {
716 // TODO: support divergence checks for stochastic specifications
717 if constexpr (!Stochastic)
718 {
719 m_divergence_detector->detect_divergence(s, s_index, m_trace_constructor, options.dfs_recursive);
720 }
721 }
722 // if (explorer.state_map().size() >= options.max_states)
723 //--- Workaround for Visual Studio 2019 ---//
724 if (max_states_exceeded(thread_index))
725 {
726 static bool not_reported_yet=true;
727 if (not_reported_yet)
728 {
729 not_reported_yet=false;
730 mCRL2log(log::verbose) << "Explored the maximum number (" << options.max_states << ") of states, terminating." << std::endl;
731 }
732 //--- Workaround for Visual Studio 2019 ---//
733 // explorer.abort();
734 static_cast<lps::abortable&>(explorer).abort();
735 }
736 },
737
738 // examine_transition
739 [&](const std::size_t thread_index, const std::size_t number_of_threads,
740 const lps::state& s0, std::size_t s0_index, const lps::multi_action& a,
741 const auto& s1, const auto& s1_index, std::size_t summand_index)
742 {
743 if constexpr (Stochastic)
744 {
745 builder.add_transition(s0_index, a, s1_index, s1.probabilities, number_of_threads);
746 }
747 else
748 {
749 builder.add_transition(s0_index, a, s1_index, number_of_threads);
750 }
751 assert(thread_index<has_outgoing_transitions.size());
752 has_outgoing_transitions[thread_index].m_bool = true;
754 {
755 m_action_detector.detect_action(s0, s0_index, a, first_state(s1), summand_index);
756 }
758 {
759 m_nondeterminism_detector.detect_nondeterminism(s0, s0_index, a, first_state(s1), thread_index);
760 }
762 {
764 }
765 },
766
767 // start_state
768 [&](const std::size_t thread_index, const lps::state& s, std::size_t /* s_index */)
769 {
770 if (options.number_of_threads == 1) {
771 source = &s;
772 }
773
774 assert(thread_index<has_outgoing_transitions.size());
775 has_outgoing_transitions[thread_index].m_bool = false;
777 {
778 m_nondeterminism_detector.start_state(thread_index);
779 }
780 },
781
782 // finish_state
783 [&](const std::size_t thread_index, const std::size_t number_of_threads,
784 const lps::state& s, std::size_t s_index, std::size_t todo_list_size)
785 {
786 assert(thread_index<has_outgoing_transitions.size());
787 if (options.detect_deadlock && !has_outgoing_transitions[thread_index].m_bool)
788 {
789 m_deadlock_detector.detect_deadlock(s, s_index);
790 }
792 {
793 m_progress_monitor.finish_state(explorer.state_map().size(thread_index), todo_list_size, number_of_threads);
794 }
795 },
796
797 // discover_initial_state
798 [&](const lps::stochastic_state& s, const std::list<std::size_t>& s_index)
799 {
800 if constexpr (Stochastic)
801 {
802 builder.set_initial_state(s_index, s.probabilities);
803 }
804 }
805 );
807 builder.finalize(explorer.state_map(), Timed);
808 }
809 catch (const data::enumerator_error& e)
810 {
811 mCRL2log(log::error) << "Error while exploring state space: " << e.what() << "\n";
813 {
814 const lps::state& s = *source;
815 class trace tr = m_trace_constructor.construct_trace(s);
816 std::string filename = options.trace_prefix + "_error.trc";
817 detail::save_trace(tr, filename);
818 }
819 mCRL2log(log::info) << ".\n";
820 return false;
821 }
822
823 return true;
824 }
825};
826
827} // namespace mcrl2::lts
828
829#endif // MCRL2_LTS_STATE_SPACE_GENERATOR_H
Read-only balanced binary tree of terms.
A unordered_map class in which aterms can be stored.
LPS summand containing a multi-action.
const lps::multi_action & multi_action() const
Returns the multi-action of this summand.
void abort() override
Abort the state space generation.
Definition explorer.h:1742
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
const indexed_set_for_states_type & state_map() const
Returns a mapping containing all discovered states.
Definition explorer.h:1748
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 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
data::data_expression_list process_parameter_values(data::mutable_indexed_substitution<> &sigma) const
Definition explorer.h:1768
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
const std::vector< explorer_summand > & regular_summands() const
Definition explorer.h:1753
typename std::conditional< Stochastic, stochastic_state, state >::type state_type
Definition explorer.h:450
\brief A timed multi-action
const process::action_list & actions() const
action_detector(const Specification &lpsspec, trace_constructor< Explorer > &trace_constructor_, const std::set< core::identifier_string > &trace_actions_, const std::set< lps::multi_action > &trace_multiactions_, const std::string &filename_prefix_, std::size_t max_trace_count)
trace_constructor< Explorer > & m_trace_constructor
bool detect_action(const lps::state &s0, std::size_t s0_index, const lps::multi_action &a, const lps::state &s1, std::size_t summand_index)
bool match_action(const lps::action_summand &summand) const
const std::set< core::identifier_string > & trace_actions
std::string create_filename(const lps::multi_action &a)
const std::set< lps::multi_action > & trace_multiactions
deadlock_detector(trace_constructor< Explorer > &trace_constructor_, const std::string &filename_prefix_, std::size_t max_trace_count)
void detect_deadlock(const lps::state &s, std::size_t s_index)
trace_constructor< Explorer > & m_trace_constructor
std::vector< lps::explorer_summand > m_confluent_summands
typename Explorer::state_index_type state_index_type
utilities::unordered_map< lps::state, std::size_t > m_divergent_states
bool detect_divergence(const lps::state &s, std::size_t s_index, trace_constructor< Explorer > &global_trace_constructor, bool dfs_recursive=false)
std::vector< lps::explorer_summand > m_regular_summands
trace_constructor< Explorer > m_local_trace_constructor
typename std::conditional< Explorer::is_stochastic, std::forward_list< lps::state >, lps::state >::type last_discovered_type
divergence_detector(Explorer &explorer_, const std::set< core::identifier_string > &actions, const std::string &filename_prefix_, std::size_t max_trace_count)
trace_constructor< Explorer > & m_trace_constructor
std::vector< std::map< lps::multi_action, lps::state > > m_transitions_vec
nondeterminism_detector(trace_constructor< Explorer > &trace_constructor_, const std::string &filename_prefix_, const std::size_t number_of_threads, std::size_t max_trace_count=0)
bool detect_nondeterminism(const lps::state &s0, std::size_t s0_index, const lps::multi_action &a, const lps::state &s1, std::size_t thread_index)
progress_monitor(lps::exploration_strategy search_strategy_)
std::atomic< std::size_t > transition_count
void finish_exploration(std::size_t state_count, std::size_t number_of_threads)
void finish_state(std::size_t state_count, std::size_t todo_list_size, std::size_t number_of_threads)
lps::multi_action find_action(const lps::state &s0, const lps::state &s1)
class trace construct_trace(const lps::state &s)
std::map< lps::state, lps::state > m_backpointers
void add_edge(const lps::state &s0, const lps::state &s1)
This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate st...
Definition trace.h:52
const std::vector< lps::state > & states() const
Definition trace.h:426
void set_state(const lps::state &s)
Set the state at the current position.
Definition trace.h:332
void save(const std::string &filename, trace_format tf=tfMcrl2) const
Output the trace into a file with the indicated name.
Definition trace.h:401
void add_action(const mcrl2::lps::multi_action &action)
Add an action to the current trace.
Definition trace.h:319
Standard exception class for reporting runtime errors.
Definition exception.h:27
size_type size(std::size_t thread_index=0) const
The number of elements in the indexed set.
add your file description here.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
std::string pp(const atermpp::aterm &t)
Transform an aterm to an ascii string.
Definition aterm.h:362
std::string pp(const identifier_string &x)
Definition core.cpp:26
std::ostream & operator<<(std::ostream &out, const abstraction &x)
Definition abstraction.h:94
@ verbose
Definition logger.h:35
std::string pp(const action_summand &x)
Definition lps.cpp:26
void save_traces(class trace &tr, const std::string &filename1, class trace &tr2, const std::string &filename2)
bool save_trace(class trace &tr, const std::string &filename)
The main LTS namespace.
const lps::state & first_state(const lps::state &s)
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
Enumerator exception.
Definition enumerator.h:216
std::set< core::identifier_string > actions_internal_for_divergencies
std::vector< state > states
state_space_generator(const Specification &lpsspec, const lps::explorer_options &options_)
std::unique_ptr< detail::divergence_detector< explorer_type > > m_divergence_detector
const lps::explorer_options & options
bool max_states_exceeded(const std::size_t thread_index)
detail::action_detector< explorer_type > m_action_detector
detail::progress_monitor m_progress_monitor
typename explorer_type::state_type state_type
detail::trace_constructor< explorer_type > m_trace_constructor
detail::nondeterminism_detector< explorer_type > m_nondeterminism_detector
lps::explorer< Stochastic, Timed, Specification > explorer
detail::deadlock_detector< explorer_type > m_deadlock_detector
The skip operation with a variable number of arguments.
Definition skip.h:21
This class allows to flexibly manipulate traces.