Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/lts/state_space_generator.h
10 : /// \brief add your file description here.
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 :
18 : namespace mcrl2::lts
19 : {
20 :
21 : inline
22 : std::ostream& operator<<(std::ostream& out, const lps::state& s)
23 : {
24 : return out << atermpp::pp(s);
25 : }
26 :
27 : inline
28 0 : const lps::state& first_state(const lps::state& s)
29 : {
30 0 : return s;
31 : }
32 :
33 : inline
34 0 : const lps::state& first_state(const lps::stochastic_state& s)
35 : {
36 0 : return s.states.front();
37 : }
38 :
39 : namespace detail
40 : {
41 :
42 : inline
43 0 : bool save_trace(
44 : class trace& tr,
45 : const std::string& filename
46 : )
47 : {
48 : try
49 : {
50 0 : tr.save(filename);
51 0 : mCRL2log(log::info) << " and saved trace to '" << filename << "'";
52 0 : return true;
53 : }
54 0 : catch(...)
55 : {
56 0 : mCRL2log(log::info) << ", but its trace could not be saved to '" << filename << "'";
57 0 : }
58 0 : return false;
59 : }
60 :
61 : inline
62 0 : void save_traces(
63 : class trace& tr,
64 : const std::string& filename1,
65 : class trace& tr2,
66 : const std::string& filename2
67 : )
68 : {
69 : try
70 : {
71 0 : tr.save(filename1);
72 0 : tr2.save(filename2);
73 0 : mCRL2log(log::info) << " and saved traces to '" << filename1 << "' and '" << filename2 << "'";
74 : }
75 0 : catch(...)
76 : {
77 0 : mCRL2log(log::info) << ", but its traces could not be saved to '" << filename1 << "' and '" << filename2 << "'";
78 0 : }
79 0 : }
80 :
81 : // Facility for constructing a trace to a given state.
82 : template <typename Explorer>
83 : class trace_constructor
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.
90 0 : lps::multi_action find_action(const lps::state& s0,
91 : const lps::state& s1)
92 : {
93 : if constexpr (Explorer::is_stochastic)
94 : {
95 0 : for (const std::pair<lps::multi_action, lps::stochastic_state>& t: m_explorer.generate_transitions(s0))
96 : {
97 0 : for (const lps::state& s: t.second.states)
98 : {
99 0 : if (s == s1)
100 : {
101 0 : return t.first;
102 : }
103 : }
104 : }
105 : }
106 : else
107 : {
108 0 : for (const std::pair<lps::multi_action, lps::state>& t: m_explorer.generate_transitions(s0))
109 : {
110 0 : if (t.second == s1)
111 : {
112 0 : return t.first;
113 : }
114 : }
115 : }
116 0 : throw mcrl2::runtime_error("no transition found in find_action");
117 : }
118 :
119 : public:
120 192 : explicit trace_constructor(Explorer& explorer_)
121 192 : : m_explorer(explorer_)
122 192 : {}
123 :
124 : // Constructs a trace ending in s, using the backpointers map.
125 0 : class trace construct_trace(const lps::state& s)
126 : {
127 0 : std::deque<lps::state> states{ s };
128 0 : std::deque<lps::multi_action> actions;
129 0 : while (true)
130 : {
131 0 : const lps::state& s1 = states.front();
132 0 : auto i = m_backpointers.find(s1);
133 0 : if (i == m_backpointers.end())
134 : {
135 0 : break;
136 : }
137 0 : const lps::state& s0 = i->second;
138 0 : states.push_front(s0);
139 0 : actions.push_front(find_action(s0, s1));
140 : }
141 :
142 0 : class trace tr;
143 0 : for (std::size_t i = 0; i < actions.size(); i++)
144 : {
145 0 : tr.set_state(states[i]);
146 0 : tr.add_action(actions[i]);
147 : }
148 0 : tr.set_state(states.back());
149 0 : return tr;
150 0 : }
151 :
152 : // Adds a back pointer for the given edge
153 0 : void add_edge(const lps::state& s0, const lps::state& s1)
154 : {
155 0 : m_backpointers[s1] = s0;
156 0 : }
157 :
158 0 : void clear()
159 : {
160 0 : m_backpointers.clear();
161 0 : }
162 :
163 : // Providing access to the explorer should perhaps be avoided.
164 0 : Explorer& explorer()
165 : {
166 0 : return m_explorer;
167 : }
168 : };
169 :
170 : template <typename Explorer>
171 : class action_detector
172 : {
173 : protected:
174 : const std::set<core::identifier_string>& trace_actions;
175 : const std::set<lps::multi_action>& trace_multiactions;
176 : trace_constructor<Explorer>& m_trace_constructor;
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 441 : bool match_action(const lps::action_summand& summand) const
183 : {
184 : using utilities::detail::contains;
185 1293 : for (const process::action& a: summand.multi_action().actions())
186 : {
187 411 : if (contains(trace_actions, a.label().name()))
188 : {
189 0 : return true;
190 : }
191 : }
192 441 : return false;
193 : }
194 :
195 0 : bool match_summand(std::size_t i) const
196 : {
197 0 : return summand_matches[i];
198 : }
199 :
200 0 : std::string create_filename(const lps::multi_action& a)
201 : {
202 : using utilities::detail::contains;
203 0 : std::string filename = filename_prefix + "_act_" + std::to_string(m_trace_count++);
204 0 : if (utilities::detail::contains(trace_multiactions, a))
205 : {
206 0 : filename += "_" + lps::pp(a);
207 : }
208 0 : for (const process::action& a_i: a.actions())
209 : {
210 0 : if (utilities::detail::contains(trace_actions, a_i.label().name()))
211 : {
212 0 : filename += "_" + core::pp(a_i.label().name());
213 : }
214 : }
215 0 : filename = filename + ".trc";
216 0 : return filename;
217 0 : }
218 :
219 : public:
220 : template <typename Specification>
221 192 : action_detector(
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 192 : : trace_actions(trace_actions_),
230 192 : trace_multiactions(trace_multiactions_),
231 192 : m_trace_constructor(trace_constructor_),
232 192 : filename_prefix(filename_prefix_),
233 192 : m_max_trace_count(max_trace_count)
234 : {
235 : using utilities::detail::contains;
236 192 : const auto& summands = lpsspec.process().action_summands();
237 192 : summand_matches.reserve(summands.size());
238 633 : for (const auto& summand: summands)
239 : {
240 441 : summand_matches.push_back(match_action(summand));
241 : }
242 192 : }
243 :
244 0 : 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 : {
246 : using utilities::detail::contains;
247 0 : if (!match_summand(summand_index))
248 : {
249 0 : return false;
250 : }
251 0 : bool result = false;
252 :
253 0 : mCRL2log(log::info) << "Action '" + lps::pp(a) + "' found (state index: " + std::to_string(s0_index) + ")";
254 0 : if (m_trace_count < m_max_trace_count)
255 : {
256 0 : class trace tr = m_trace_constructor.construct_trace(s0);
257 0 : tr.add_action(a);
258 0 : tr.set_state(s1);
259 0 : std::string filename = create_filename(a);
260 0 : save_trace(tr, filename);
261 0 : result = true;
262 0 : }
263 0 : mCRL2log(log::info) << ".\n";
264 0 : if (m_max_trace_count > 0 && m_trace_count >= m_max_trace_count)
265 : {
266 0 : m_trace_constructor.explorer().abort();
267 : }
268 0 : return result;
269 : }
270 : };
271 :
272 : template <typename Explorer>
273 : class deadlock_detector
274 : {
275 : protected:
276 : trace_constructor<Explorer>& m_trace_constructor;
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:
282 192 : deadlock_detector(
283 : trace_constructor<Explorer>& trace_constructor_,
284 : const std::string& filename_prefix_,
285 : std::size_t max_trace_count
286 : )
287 192 : : m_trace_constructor(trace_constructor_),
288 192 : filename_prefix(filename_prefix_),
289 192 : m_max_trace_count(max_trace_count)
290 192 : {}
291 :
292 0 : void detect_deadlock(const lps::state& s, std::size_t s_index)
293 : {
294 0 : mCRL2log(log::info) << "Deadlock found (state index: " + std::to_string(s_index) + ")";
295 0 : if (m_trace_count < m_max_trace_count)
296 : {
297 0 : class trace tr = m_trace_constructor.construct_trace(s);
298 0 : std::string filename = filename_prefix + "_dlk_" + std::to_string(m_trace_count++) + ".trc";
299 0 : save_trace(tr, filename);
300 0 : }
301 0 : if (m_max_trace_count > 0 && m_trace_count >= m_max_trace_count)
302 : {
303 0 : m_trace_constructor.explorer().abort();
304 : }
305 0 : mCRL2log(log::info) << ".\n";
306 0 : }
307 : };
308 :
309 : template <typename Explorer>
310 : class nondeterminism_detector
311 : {
312 : protected:
313 : trace_constructor<Explorer>& m_trace_constructor;
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:
320 192 : nondeterminism_detector(
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 192 : : m_trace_constructor(trace_constructor_),
327 192 : filename_prefix(filename_prefix_),
328 192 : m_transitions_vec(number_of_threads+1), //Threads are number from 1 to n.
329 192 : m_max_trace_count(max_trace_count)
330 : {
331 192 : assert(number_of_threads>0);
332 192 : }
333 :
334 0 : void start_state(std::size_t thread_index)
335 : {
336 0 : assert(thread_index<m_transitions_vec.size());
337 0 : m_transitions_vec[thread_index].clear();
338 0 : }
339 :
340 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)
341 : {
342 0 : bool result = false;
343 0 : assert(thread_index<m_transitions_vec.size());
344 0 : auto i = m_transitions_vec[thread_index].find(a);
345 0 : if (i == m_transitions_vec[thread_index].end())
346 : {
347 0 : m_transitions_vec[thread_index].insert(std::make_pair(a, s1));
348 : }
349 0 : else if (i->second != s1) // nondeterminism detected
350 : {
351 0 : mCRL2log(log::info) << "Nondeterministic state found (state index: " + std::to_string(s0_index) + ")";
352 0 : if (m_trace_count < m_max_trace_count)
353 : {
354 0 : class trace tr = m_trace_constructor.construct_trace(s0);
355 0 : tr.add_action(a);
356 0 : tr.set_state(s1);
357 0 : std::string filename = filename_prefix + "_nondeterministic_" + std::to_string(m_trace_count++) + ".trc";
358 0 : save_trace(tr, filename);
359 0 : result = true;
360 0 : }
361 0 : mCRL2log(log::info) << ".\n";
362 0 : if (m_max_trace_count > 0 && m_trace_count >= m_max_trace_count)
363 : {
364 0 : m_trace_constructor.explorer().abort();
365 : }
366 : }
367 0 : return result;
368 : }
369 : };
370 :
371 : template <typename Explorer>
372 : class divergence_detector
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;
384 : trace_constructor<Explorer> m_local_trace_constructor;
385 : utilities::unordered_map<lps::state, std::size_t> m_divergent_states;
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:
393 0 : divergence_detector(
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 0 : : explorer(explorer_),
400 0 : filename_prefix(filename_prefix_),
401 0 : m_local_trace_constructor(explorer),
402 0 : m_max_trace_count(max_trace_count)
403 : {
404 : using utilities::detail::contains;
405 :
406 0 : auto is_hidden = [&](const lps::explorer_summand& summand)
407 : {
408 0 : for (const process::action& a: summand.multi_action.actions())
409 : {
410 0 : if (!contains(actions, a.label().name()))
411 : {
412 0 : return false;
413 : }
414 : }
415 0 : return true;
416 : };
417 :
418 0 : for (const lps::explorer_summand& summand: explorer.regular_summands())
419 : {
420 0 : if (is_hidden(summand))
421 : {
422 0 : m_regular_summands.push_back(summand);
423 : }
424 : }
425 :
426 0 : for (const lps::explorer_summand& summand: explorer.confluent_summands())
427 : {
428 0 : if (is_hidden(summand))
429 : {
430 0 : m_confluent_summands.push_back(summand);
431 : }
432 : }
433 0 : }
434 :
435 : // Returns true if a trace was saved.
436 0 : bool detect_divergence(const lps::state& s, std::size_t s_index, trace_constructor<Explorer>& global_trace_constructor, bool dfs_recursive = false)
437 : {
438 : using utilities::detail::contains;
439 :
440 0 : bool result = false;
441 0 : divergence_detector_mutex.lock();
442 0 : m_local_trace_constructor.clear();
443 :
444 0 : auto q = m_divergent_states.find(s);
445 0 : if (q != m_divergent_states.end())
446 : {
447 0 : std::string message = "Divergent state found (state index: " + std::to_string(s_index) +
448 0 : "), reachable from divergent state with index " + std::to_string(q->second);
449 0 : mCRL2log(log::info) << message << ".\n";
450 0 : m_divergent_states.erase(q);
451 0 : divergence_detector_mutex.unlock();
452 0 : return false;
453 0 : }
454 :
455 0 : std::unordered_set<lps::state> discovered;
456 0 : data::data_expression_list process_parameter_undo = explorer.process_parameter_values();
457 :
458 0 : if (dfs_recursive)
459 : {
460 0 : std::unordered_set<lps::state> gray;
461 0 : explorer.generate_state_space_dfs_recursive(
462 : s,
463 : gray,
464 : discovered,
465 0 : m_regular_summands,
466 0 : m_confluent_summands,
467 : utilities::skip(), // discover_state
468 : utilities::skip(), // examine_transition
469 : utilities::skip(), // tree_edge
470 :
471 : // back_edge
472 0 : [&](const lps::state& s0, const lps::multi_action& a, const state_type& s1) {
473 0 : mCRL2log(log::info) << "Divergent state found (state index: " + std::to_string(s_index) + ")";
474 0 : if (m_trace_count < m_max_trace_count)
475 : {
476 0 : class trace tr = global_trace_constructor.construct_trace(s);
477 0 : class trace tr_loop = m_local_trace_constructor.construct_trace(s0);
478 0 : for (const lps::state& u: tr_loop.states())
479 : {
480 0 : m_divergent_states[u] = s_index;
481 : }
482 0 : tr_loop.add_action(a);
483 0 : tr_loop.set_state(first_state(s1));
484 0 : std::string filename = filename_prefix + "_divergence_" + std::to_string(m_trace_count) + ".trc";
485 0 : std::string loop_filename = filename_prefix + "_divergence_loop" + std::to_string(m_trace_count++) + ".trc";
486 0 : save_traces(tr, filename, tr_loop, loop_filename);
487 0 : result = true;
488 0 : }
489 0 : mCRL2log(log::info) << ".\n";
490 : //--- Workaround for Visual Studio 2019 ---//
491 : // explorer.abort();
492 0 : static_cast<lps::abortable&>(explorer).abort();
493 : }
494 : );
495 0 : }
496 : else
497 : {
498 0 : explorer.generate_state_space_dfs_iterative(
499 : s,
500 : discovered,
501 0 : m_regular_summands,
502 0 : m_confluent_summands,
503 : utilities::skip(), // discover_state
504 : utilities::skip(), // examine_transition
505 : utilities::skip(), // tree_edge
506 :
507 : // back_edge
508 0 : [&](const lps::state& s0, const lps::multi_action& a, const state_type& s1) {
509 0 : mCRL2log(log::info) << "Divergent state found (state index: " + std::to_string(s_index) + ")";
510 0 : if (m_trace_count < m_max_trace_count)
511 : {
512 0 : class trace tr = global_trace_constructor.construct_trace(s);
513 0 : class trace tr_loop = m_local_trace_constructor.construct_trace(s0);
514 0 : for (const lps::state& u: tr_loop.states())
515 : {
516 0 : m_divergent_states[u] = s_index;
517 : }
518 0 : tr_loop.add_action(a);
519 0 : tr_loop.set_state(first_state(s1));
520 0 : std::string filename = filename_prefix + "_divergence_" + std::to_string(m_trace_count) + ".trc";
521 0 : std::string loop_filename = filename_prefix + "_divergence_loop" + std::to_string(m_trace_count++) + ".trc";
522 0 : save_traces(tr, filename, tr_loop, loop_filename);
523 0 : result = true;
524 0 : }
525 0 : mCRL2log(log::info) << ".\n";
526 : //--- Workaround for Visual Studio 2019 ---//
527 : // explorer.abort();
528 0 : static_cast<lps::abortable&>(explorer).abort();
529 : }
530 : );
531 : }
532 0 : explorer.set_process_parameter_values(process_parameter_undo);
533 0 : if (m_max_trace_count > 0 && m_trace_count >= m_max_trace_count)
534 : {
535 0 : explorer.abort();
536 : }
537 0 : divergence_detector_mutex.unlock();
538 0 : return result;
539 0 : }
540 : };
541 :
542 : class progress_monitor
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 :
554 : lps::exploration_strategy search_strategy;
555 :
556 : public:
557 192 : explicit progress_monitor(lps::exploration_strategy search_strategy_)
558 192 : : search_strategy(search_strategy_)
559 192 : {}
560 :
561 2536 : void examine_transition()
562 : {
563 2536 : transition_count++;
564 2536 : }
565 :
566 1354 : void finish_state(std::size_t state_count, std::size_t todo_list_size, std::size_t number_of_threads)
567 : {
568 1354 : time_t new_log_time = 0;
569 :
570 : static std::mutex exclusive_print_mutex;
571 1354 : if (search_strategy == lps::es_breadth)
572 : {
573 706 : ++count;
574 706 : if (number_of_threads == 1 && count == level_up)
575 : {
576 292 : exclusive_print_mutex.lock();
577 292 : mCRL2log(log::debug) << "Number of states at level " << level << " is " << state_count - last_state_count << "\n";
578 292 : level++;
579 292 : level_up = count + todo_list_size;
580 292 : last_state_count = state_count;
581 292 : last_transition_count = transition_count;
582 292 : exclusive_print_mutex.unlock();
583 : }
584 :
585 1412 : if (time(&new_log_time) > last_log_time.load(std::memory_order_relaxed))
586 : {
587 284 : exclusive_print_mutex.lock();
588 :
589 284 : last_log_time = new_log_time;
590 284 : std::size_t lvl_states = state_count - last_state_count;
591 284 : std::size_t lvl_transitions = transition_count - last_transition_count;
592 284 : if (number_of_threads>1) // Levels have no meaning with multiple threads.
593 : {
594 0 : mCRL2log(log::status) << std::fixed << std::setprecision(2)
595 0 : << state_count << "st, " << transition_count << "tr"
596 0 : << ", explored " << 100.0 * ((float) count / state_count)
597 0 : << "%.\n";
598 : }
599 : else
600 : {
601 284 : mCRL2log(log::status) << std::fixed << std::setprecision(2)
602 0 : << state_count << "st, " << transition_count << "tr"
603 0 : << ", explored " << 100.0 * ((float) count / state_count)
604 0 : << "%. Last level: " << level << ", " << lvl_states << "st, "
605 0 : << lvl_transitions << "tr.\n";
606 : }
607 284 : exclusive_print_mutex.unlock();
608 : }
609 : }
610 : else
611 : {
612 648 : count++;
613 1296 : if (time(&new_log_time) > last_log_time.load(std::memory_order_relaxed))
614 : {
615 263 : exclusive_print_mutex.lock();
616 263 : last_log_time = new_log_time;
617 263 : mCRL2log(log::status) << "monitor: currently explored "
618 0 : << count << " state" << ((count==1)?"":"s")
619 0 : << " and " << transition_count << " transition" << ((transition_count==1)?".":"s.")
620 0 : << std::endl;
621 263 : exclusive_print_mutex.unlock();
622 : }
623 : }
624 1354 : }
625 :
626 192 : void finish_exploration(std::size_t state_count, std::size_t number_of_threads)
627 : {
628 192 : if (search_strategy == lps::es_breadth)
629 : {
630 105 : mCRL2log(log::verbose) << "Done with state space generation (";
631 105 : if (number_of_threads==1)
632 : {
633 105 : mCRL2log(log::verbose) << level-1 << " level" << ((level==2)?"":"s") << ", ";
634 : }
635 105 : mCRL2log(log::verbose) << state_count << " state" << ((state_count == 1)?"":"s")
636 0 : << " and " << transition_count << " transition" << ((transition_count==1)?"":"s") << ")" << std::endl;
637 : }
638 : else
639 : {
640 87 : mCRL2log(log::verbose) << "Done with state space generation ("
641 0 : << state_count << " state" << ((state_count == 1)?"":"s")
642 0 : << " and " << transition_count << " transition" << ((transition_count==1)?"":"s") << ")" << std::endl;
643 : }
644 192 : }
645 : };
646 :
647 : } // namespace detail
648 :
649 : template <bool Stochastic, bool Timed, typename Specification>
650 : struct state_space_generator
651 : {
652 : using explorer_type = lps::explorer<Stochastic, Timed, Specification>;
653 : using state_type = typename explorer_type::state_type;
654 :
655 : const lps::explorer_options& options;
656 : lps::explorer<Stochastic, Timed, Specification> explorer;
657 : detail::trace_constructor<explorer_type> m_trace_constructor;
658 :
659 : detail::action_detector<explorer_type> m_action_detector;
660 : detail::deadlock_detector<explorer_type> m_deadlock_detector;
661 : detail::nondeterminism_detector<explorer_type> m_nondeterminism_detector;
662 : std::unique_ptr<detail::divergence_detector<explorer_type>> m_divergence_detector;
663 : detail::progress_monitor m_progress_monitor;
664 :
665 192 : state_space_generator(const Specification& lpsspec, const lps::explorer_options& options_)
666 192 : : options(options_),
667 192 : explorer(lpsspec, options_),
668 192 : m_trace_constructor(explorer),
669 192 : m_action_detector(lpsspec, m_trace_constructor, options.trace_actions, options.trace_multiactions, options.trace_prefix, options.max_traces),
670 192 : m_deadlock_detector(m_trace_constructor, options.trace_prefix, options.max_traces),
671 192 : m_nondeterminism_detector(m_trace_constructor, options.trace_prefix, options.number_of_threads, options.max_traces),
672 192 : m_progress_monitor(options.search_strategy)
673 : {
674 192 : if (options.detect_divergence)
675 : {
676 0 : m_divergence_detector =
677 0 : std::unique_ptr<detail::divergence_detector<explorer_type>>(
678 0 : new detail::divergence_detector<explorer_type>(explorer,
679 0 : options.actions_internal_for_divergencies,
680 0 : options.trace_prefix,
681 0 : options.max_traces));
682 : }
683 192 : }
684 :
685 1354 : bool max_states_exceeded(const std::size_t thread_index)
686 : {
687 1354 : return explorer.state_map().size(thread_index) >= options.max_states;
688 : }
689 :
690 : struct aligned_bool
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 192 : bool explore(LTSBuilder& builder)
698 : {
699 192 : std::vector<aligned_bool> has_outgoing_transitions(options.number_of_threads+1); // thread indices start at 1.
700 192 : const lps::state* source = nullptr;
701 :
702 : try
703 : {
704 192 : explorer.generate_state_space(
705 : false,
706 :
707 : // discover_state
708 1354 : [&](const std::size_t thread_index, const lps::state& s, std::size_t s_index)
709 : {
710 1354 : if (options.generate_traces && source)
711 : {
712 0 : m_trace_constructor.add_edge(*source, s);
713 : }
714 1354 : if (options.detect_divergence)
715 : {
716 : // TODO: support divergence checks for stochastic specifications
717 : if constexpr (!Stochastic)
718 : {
719 0 : 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 1354 : if (max_states_exceeded(thread_index))
725 : {
726 : static bool not_reported_yet=true;
727 0 : if (not_reported_yet)
728 : {
729 0 : not_reported_yet=false;
730 0 : 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 0 : static_cast<lps::abortable&>(explorer).abort();
735 : }
736 : },
737 :
738 : // examine_transition
739 20288 : [&](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 190 : builder.add_transition(s0_index, a, s1_index, s1.probabilities, number_of_threads);
746 : }
747 : else
748 : {
749 2346 : builder.add_transition(s0_index, a, s1_index, number_of_threads);
750 : }
751 2536 : assert(thread_index<has_outgoing_transitions.size());
752 2536 : has_outgoing_transitions[thread_index].m_bool = true;
753 2536 : if (options.detect_action)
754 : {
755 0 : m_action_detector.detect_action(s0, s0_index, a, first_state(s1), summand_index);
756 : }
757 2536 : if (options.detect_nondeterminism)
758 : {
759 0 : m_nondeterminism_detector.detect_nondeterminism(s0, s0_index, a, first_state(s1), thread_index);
760 : }
761 2536 : if (!options.suppress_progress_messages)
762 : {
763 2536 : m_progress_monitor.examine_transition();
764 : }
765 : },
766 :
767 : // start_state
768 8124 : [&](const std::size_t thread_index, const lps::state& s, std::size_t /* s_index */)
769 : {
770 1354 : if (options.number_of_threads == 1) {
771 1354 : source = &s;
772 : }
773 :
774 1354 : assert(thread_index<has_outgoing_transitions.size());
775 1354 : has_outgoing_transitions[thread_index].m_bool = false;
776 1354 : if (options.detect_nondeterminism)
777 : {
778 0 : m_nondeterminism_detector.start_state(thread_index);
779 : }
780 : },
781 :
782 : // finish_state
783 6770 : [&](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 1354 : assert(thread_index<has_outgoing_transitions.size());
787 1354 : if (options.detect_deadlock && !has_outgoing_transitions[thread_index].m_bool)
788 : {
789 0 : m_deadlock_detector.detect_deadlock(s, s_index);
790 : }
791 1354 : if (!options.suppress_progress_messages)
792 : {
793 1354 : 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 36 : [&](const lps::stochastic_state& s, const std::list<std::size_t>& s_index)
799 : {
800 : if constexpr (Stochastic)
801 : {
802 18 : builder.set_initial_state(s_index, s.probabilities);
803 : }
804 : }
805 : );
806 192 : m_progress_monitor.finish_exploration(explorer.state_map().size(), options.number_of_threads);
807 192 : builder.finalize(explorer.state_map(), Timed);
808 : }
809 0 : catch (const data::enumerator_error& e)
810 : {
811 0 : mCRL2log(log::error) << "Error while exploring state space: " << e.what() << "\n";
812 0 : if (options.save_error_trace)
813 : {
814 0 : const lps::state& s = *source;
815 0 : class trace tr = m_trace_constructor.construct_trace(s);
816 0 : std::string filename = options.trace_prefix + "_error.trc";
817 0 : detail::save_trace(tr, filename);
818 0 : }
819 0 : mCRL2log(log::info) << ".\n";
820 0 : return false;
821 : }
822 :
823 192 : return true;
824 192 : }
825 : };
826 :
827 : } // namespace mcrl2::lts
828 :
829 : #endif // MCRL2_LTS_STATE_SPACE_GENERATOR_H
|
