mCRL2
Loading...
Searching...
No Matches
liblts_failures_refinement.h
Go to the documentation of this file.
1// Author(s): Jan Friso Groote
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//
10
11// This file contains an implementation of
12// T. Wang, S. Song, J. Sun, Y. Liu, J.S. Dong, X. Wang and S. Li.
13// More Anti-Chain Based Refinement Checking. In proceedings ICFEM 2012, editors T. Aoki and K. Tagushi,
14// Lecture Notes in Computer Science no 7635, pages 364-380, 2012.
15//
16// There are six algorithms. One for trace inclusion, one for failures inclusion and one for failures-divergence inclusion.
17// All algorithms come in a variant with and without internal steps.
18// It is possible to generate a counter transition system in case the inclusion is answered by no.
19
20#ifndef LIBLTS_FAILURES_REFINEMENT_H
21#define LIBLTS_FAILURES_REFINEMENT_H
22
26
27namespace mcrl2
28{
29namespace lts
30{
31namespace detail
32{
33 typedef std::size_t state_type;
34 typedef std::size_t label_type;
35 typedef std::set<state_type> set_of_states;
36 typedef std::multimap <detail::state_type,detail::set_of_states> anti_chain_type;
37 typedef std::set < label_type > action_label_set;
38
39 template < class COUNTER_EXAMPLE_CONSTRUCTOR >
41 {
42 protected:
45 typename COUNTER_EXAMPLE_CONSTRUCTOR::index_type m_counter_example_index;
46
47 public:
49 {}
50
53 const state_type state,
54 const set_of_states& states,
55 const typename COUNTER_EXAMPLE_CONSTRUCTOR::index_type& counter_example_index)
56 : m_state(state),
59 {}
60
63 {
64 return m_state;
65 }
66
68 {
72 }
73
75 const set_of_states& states() const
76 {
77 return m_states;
78 }
79
81 const typename COUNTER_EXAMPLE_CONSTRUCTOR::index_type& counter_example_index() const
82 {
84 }
85 };
86
87 template < class COUNTER_EXAMPLE_CONSTRUCTOR >
88 inline bool antichain_insert(
89 anti_chain_type& anti_chain,
90 const state_states_counter_example_index_triple<COUNTER_EXAMPLE_CONSTRUCTOR>& impl_spec);
91
92 // The class below recalls what the stable states and the states with a divergent
93 // self loop of a transition system are, such that it does not have to be recalculated each time again.
94 template < class LTS_TYPE >
96 {
97 protected:
98 LTS_TYPE& m_l;
99 std::vector<std::vector<state_type> > m_tau_reachable_states;
100 std::vector<std::vector<transition> > m_sorted_transitions;
101 std::vector<bool> m_divergent;
102 std::vector<action_label_set> m_enabled_actions;
103
104 private:
105 void calculate_weak_property_cache(const bool weak_reduction)
106 {
107 scc_partitioner<LTS_TYPE> strongly_connected_component_partitioner(m_l);
108 for(const transition& t: m_l.get_transitions())
109 {
110 assert(t.from()<m_l.num_states());
111 if (m_l.is_tau(m_l.apply_hidden_label_map(t.label())) && weak_reduction)
112 {
113 m_tau_reachable_states[t.from()].push_back(t.to()); // There is an outgoing tau.
114 }
115 m_sorted_transitions[t.from()].push_back(t);
116
117 if (weak_reduction && m_l.is_tau(m_l.apply_hidden_label_map(t.label())) &&
118 strongly_connected_component_partitioner.in_same_class(t.from(),t.to()))
119 {
120 m_divergent[t.from()]=true; // There is a self loop.
121 }
122 m_enabled_actions[t.from()].insert(m_l.apply_hidden_label_map(t.label()));
123 }
124 }
125
126 public:
127
128 lts_cache(/* const */ LTS_TYPE& l, const bool weak_reduction) /* l is not changed, but the use of the scc partitioner requires l to be non const */
129 : m_l(l),
130 m_tau_reachable_states(l.num_states()),
131 m_sorted_transitions(l.num_states()),
132 m_divergent(l.num_states(),false),
133 m_enabled_actions(l.num_states())
134 {
135 calculate_weak_property_cache(weak_reduction);
136 }
137
138 bool stable(const state_type s) const
139 {
140 return m_tau_reachable_states[s].size()==0;
141 }
142
143 const std::vector<state_type>& tau_reachable_states(const state_type s) const
144 {
145 return m_tau_reachable_states[s];
146 }
147
148 const std::vector<transition>& transitions(const state_type s) const
149 {
150 assert(s<m_sorted_transitions.size());
151 return m_sorted_transitions[s];
152 }
153
154 bool diverges(const state_type s) const
155 {
156 return m_divergent[s];
157 }
158
160 {
161 return m_enabled_actions[s];
162 }
163 };
164
165 template < class LTS_TYPE >
166 set_of_states collect_reachable_states_via_taus(
167 const state_type s,
168 const lts_cache<LTS_TYPE>& weak_property_cache,
169 const bool weak_reduction);
170
171 template < class LTS_TYPE >
172 set_of_states collect_reachable_states_via_an_action(
173 const state_type s,
174 const label_type e,
175 const lts_cache<LTS_TYPE>& weak_property_cache,
176 const bool weak_reduction,
177 const LTS_TYPE& l);
178
179 template < class LTS_TYPE >
180 bool refusals_contained_in(
181 const state_type impl,
182 const set_of_states& spec,
183 const lts_cache<LTS_TYPE>& weak_property_cache,
184 label_type& culprit,
185 const LTS_TYPE& l,
186 const bool provide_a_counter_example,
187 const bool structured_output);
188
189} // namespace detail
190
192
193template<typename T>
195{
199 {}
200
202 std::deque<T>& working;
203 std::size_t max_working = 0; // The largest size of working.
204 std::size_t max_antichain = 0; // The largest size of the antichain.
205 std::size_t antichain_misses = 0; // Number of times a pair was inserted into the antichain.
206 std::size_t antichain_inserts = 0; // Number of times antichain_insert was called.
207};
208
210template<typename T>
212{
213 mCRL2log(log::debug) << "working (current: " << stats.working.size() << ", max: " << stats.max_working << ").\n";
214 mCRL2log(log::debug) << "antichain (hits: " << stats.antichain_inserts - stats.antichain_misses
215 << ", misses: " << stats.antichain_misses
216 << ", size: " << stats.antichain.size()
217 << ", max: " << stats.max_antichain << ")\n";
218}
219
225template<typename LTS_TYPE>
226std::pair<std::size_t, bool> reduce(LTS_TYPE& lts,
227 const bool weak_reduction,
228 const bool preserve_divergence,
229 std::size_t l2_init)
230{
232 if (weak_reduction)
233 {
234 // Remove inert tau loops when requested, but preserve divergences for failures and failures-divergence.
236 l2_init = scc_part.get_eq_class(l2_init);
237 scc_part.replace_transition_system(preserve_divergence);
238 }
239
240 detail::bisim_partitioner_dnj<LTS_TYPE> bisim_part(lts, weak_reduction,
241 preserve_divergence);
242 // Assign the reduced LTS, and set init_l2.
243 l2_init = bisim_part.get_eq_class(l2_init);
244 bisim_part.finalize_minimized_LTS();
245
246 return std::make_pair(l2_init, l2_init == lts.initial_state());
247}
248
259template < class LTS_TYPE, class COUNTER_EXAMPLE_CONSTRUCTOR = detail::dummy_counter_example_constructor >
261 LTS_TYPE& l1,
262 LTS_TYPE& l2,
263 const refinement_type refinement,
264 const bool weak_reduction,
265 const lps::exploration_strategy strategy,
266 const bool preprocess = true,
267 COUNTER_EXAMPLE_CONSTRUCTOR generate_counter_example = detail::dummy_counter_example_constructor())
268{
269 assert(strategy == lps::exploration_strategy::es_breadth || strategy == lps::exploration_strategy::es_depth); // Need a valid strategy.
270
271 // For weak-failures and failures-divergence, the existence of tau loops make a difference.
272 // Therefore, we apply bisimulation reduction preserving divergences.
273 // A typical example is a.(b+c) which is not weak-failures included n a.tau*.(b+c). The lhs has failure pairs
274 // <a,{a}>, <a,{}> while the rhs has only failure pairs <a,{}>, as the state after the a is not stable.
275 const bool preserve_divergence = weak_reduction && (refinement != refinement_type::trace);
276
277 if (!generate_counter_example.is_dummy() && preprocess)
278 {
279 // Counter example is requested, apply bisimulation to l2.
280 reduce(l2, weak_reduction, preserve_divergence, l2.initial_state());
281 }
282
283 std::size_t init_l2 = l2.initial_state() + l1.num_states();
285 l2.clear(); // No use for l2 anymore.
286
287 if (generate_counter_example.is_dummy() && preprocess)
288 {
289 // No counter example is requested. We can use bisimulation preprocessing.
290 bool initial_equal = false;
291 std::tie(init_l2, initial_equal) = reduce(l1, weak_reduction, preserve_divergence, init_l2);
292
293 if (initial_equal && weak_reduction)
294 {
295 mCRL2log(log::verbose) << "The two LTSs are";
296 if (preserve_divergence)
297 {
298 mCRL2log(log::verbose) << " divergence-preserving";
299 }
300 mCRL2log(log::verbose) << " branching bisimilar, so there is no need to check the refinement relation.\n";
301 return true;
302 }
303 }
304
305
306 const detail::lts_cache<LTS_TYPE> weak_property_cache(l1,weak_reduction);
307 std::deque<detail::state_states_counter_example_index_triple<COUNTER_EXAMPLE_CONSTRUCTOR>>
308 working( // let working be a stack containg the triple (init1,{s|init2-->s},root_index);
310 l1.initial_state(),
311 detail::collect_reachable_states_via_taus(init_l2,weak_property_cache,weak_reduction),
312 generate_counter_example.root_index() ) });
313 // let antichain := emptyset;
314 detail::anti_chain_type anti_chain;
315 detail::antichain_insert(anti_chain, working.front()); // antichain := antichain united with (impl,spec);
316 // This line occurs at another place in the code than in
317 // the original algorithm, where insertion in the anti-chain
318 // was too late, causing too many impl-spec pairs to be investigated.
320
321 while (!working.empty()) // while working!=empty
322 {
323 detail::state_states_counter_example_index_triple < COUNTER_EXAMPLE_CONSTRUCTOR > impl_spec; // pop (impl,spec) from working;
324 impl_spec.swap(working.front());
325 stats.max_working = std::max(working.size(), stats.max_working);
326 stats.max_antichain = std::max(anti_chain.size(), stats.max_antichain);
327 working.pop_front(); // At this point it could be checked whether impl_spec still exists in anti_chain.
328 // Small scale experiments show that this is a little bit more expensive than doing the explicit check below.
329
330 bool spec_diverges = false;
331 if (refinement == refinement_type::failures_divergence)
332 {
333 // Only compute when the result is required.
334 for (detail::state_type s : impl_spec.states())
335 {
336 if (weak_property_cache.diverges(s))
337 {
338 spec_diverges = true;
339 break;
340 }
341 }
342 }
343
344 // if not diverges(spec) or not CheckDiv (refinement == failures_divergence_preorder)
345 if (!spec_diverges || refinement != refinement_type::failures_divergence)
346 {
347 if (weak_property_cache.diverges(impl_spec.state()) && refinement == refinement_type::failures_divergence) // if impl diverges and CheckDiv
348 {
349 generate_counter_example.save_counter_example(impl_spec.counter_example_index(),l1);
350 report_statistics(stats);
351 return false; // return false;
352 }
353
354 if (refinement == refinement_type::failures || refinement == refinement_type::failures_divergence)
355 {
356 detail::label_type offending_action=std::size_t(-1);
357 // if refusals(impl) not contained in refusals(spec) then
358 if (!detail::refusals_contained_in(impl_spec.state(),
359 impl_spec.states(),
360 weak_property_cache,
361 offending_action,
362 l1,
363 !generate_counter_example.is_dummy(),
364 generate_counter_example.is_structured()))
365 {
366 generate_counter_example.save_counter_example(impl_spec.counter_example_index(), l1);
367 report_statistics(stats);
368 return false; // return false;
369 }
370 }
371
372 for(const transition& t: weak_property_cache.transitions(impl_spec.state()))
373 {
374 const typename COUNTER_EXAMPLE_CONSTRUCTOR::index_type new_counterexample_index=
375 generate_counter_example.add_transition(t.label(),impl_spec.counter_example_index());
376 detail::set_of_states spec_prime;
377 if (l1.is_tau(l1.apply_hidden_label_map(t.label())) && weak_reduction) // if e=tau then
378 {
379 spec_prime=impl_spec.states(); // spec' := spec;
380 }
381 else
382 { // spec' := {s' | exists s in spec. s-e->s'};
383 for(const detail::state_type s: impl_spec.states())
384 {
385 detail::set_of_states reachable_states_from_s_via_e=
386 detail::collect_reachable_states_via_an_action(s,l1.apply_hidden_label_map(t.label()),weak_property_cache,weak_reduction,l1);
387 spec_prime.insert(reachable_states_from_s_via_e.begin(),reachable_states_from_s_via_e.end());
388 }
389 }
390 if (spec_prime.empty()) // if spec'={} then
391 {
392 generate_counter_example.save_counter_example(new_counterexample_index,l1);
393 report_statistics(stats);
394 return false; // return false;
395 }
396 // if (impl',spec') in antichain is not true then
397 ++stats.antichain_inserts;
398 const detail::state_states_counter_example_index_triple < COUNTER_EXAMPLE_CONSTRUCTOR >
399 impl_spec_counterex(t.to(),spec_prime,new_counterexample_index);
400 if (detail::antichain_insert(anti_chain, impl_spec_counterex))
401 {
402 ++stats.antichain_misses;
404 {
405 working.push_back(impl_spec_counterex); // add(impl,spec') at the bottom of the working;
406 }
407 else if (strategy == lps::exploration_strategy::es_depth)
408 {
409 working.push_front(impl_spec_counterex); // push(impl,spec') into working;
410 }
411 }
412 }
413 }
414 }
415
416 report_statistics(stats);
417 return true; // return true;
418}
419
420
421namespace detail
422{
423 /* This function generates the set of states reachable from s within labelled
424 transition system l1 by internal transitions, provided weak_reduction is true.
425 Otherwise it generates a set with only state s in it.
426 */
427 template < class LTS_TYPE >
429 const set_of_states& s,
430 const lts_cache<LTS_TYPE>& weak_property_cache,
431 const bool weak_reduction)
432 {
433 set_of_states result(s);
434 if (!weak_reduction)
435 {
436 return result;
437 }
438 set_of_states visited(s);
439 std::deque<state_type> todo_stack(s.begin(),s.end());
440 while (todo_stack.size()>0)
441 {
442 state_type current_state=todo_stack.front();
443 todo_stack.pop_front();
444 for(const state_type s: weak_property_cache.tau_reachable_states(current_state))
445 {
446 if (visited.insert(s).second) // The element has been inserted.
447 {
448 todo_stack.push_back(s);
449 result.insert(s);
450 }
451 }
452 }
453
454 return result;
455 }
456
457 template < class LTS_TYPE >
459 const state_type s,
460 const lts_cache<LTS_TYPE>& weak_property_cache,
461 const bool weak_reduction)
462 {
463 set_of_states set_with_s({s});
464 return collect_reachable_states_via_taus(set_with_s, weak_property_cache, weak_reduction);
465 }
466
467 template < class LTS_TYPE >
469 const state_type s,
470 const label_type e, // This is already the hidden action.
471 const lts_cache<LTS_TYPE>& weak_property_cache,
472 const bool weak_reduction,
473 const LTS_TYPE& l)
474 {
475 const set_of_states set_before_action_e=collect_reachable_states_via_taus(s,weak_property_cache,weak_reduction);
476 set_of_states states_reachable_via_e;
477 for(const state_type s: set_before_action_e)
478 {
479 for(const transition& t: weak_property_cache.transitions(s))
480 {
481 {
482 if (l.apply_hidden_label_map(t.label())==e)
483 {
484 assert(set_before_action_e.count(t.from())>0);
485 states_reachable_via_e.insert(t.to());
486 }
487 }
488 }
489 }
490 return collect_reachable_states_via_taus(states_reachable_via_e, weak_property_cache, weak_reduction);
491 }
492
493 /* This function implements the insertion of <p,state(), p.states()> in the anti_chain.
494 Concretely, this means that p.states() is inserted among the sets s1,...,sn associated to p.state().
495 It is important that an anti_chain contains for each state a set of states of which
496 no set is a subset of another. The idea is that if such two sets occur, it is enough
497 to keep the smallest.
498 If p.states() is smaller than a set si associated to p.state(), this set is removed.
499 If p.states() is larger than a set si, there is no need to add p.states(), as a better candidate
500 is already there.
501 This function returns true if insertion was succesful, and false otherwise.
502 */
503 template < class COUNTER_EXAMPLE_CONSTRUCTOR >
504 inline bool antichain_insert(
505 anti_chain_type& anti_chain,
507 {
508 // First check whether there is a set in the antichain for impl_spec.state() which is smaller than impl_spec.states().
509 // If so, impl_spec.states() does not have to be inserted in the anti_chain.
510 for(anti_chain_type::const_iterator i=anti_chain.lower_bound(impl_spec.state()); i!=anti_chain.upper_bound(impl_spec.state()); ++i)
511 {
512 const set_of_states s=i->second;
513 // If s is included in impl_spec.states()
514 if (std::includes(impl_spec.states().begin(), impl_spec.states().end(), s.begin(),s.end()))
515 {
516 return false;
517 }
518 }
519
520 // Here impl_spec.states() must be inserted in the antichain. Moreover, all sets in the antichain that
521 // are a superset of impl_spec.states() must be removed.
522 for(anti_chain_type::iterator i=anti_chain.lower_bound(impl_spec.state()); i!=anti_chain.upper_bound(impl_spec.state()); )
523 {
524 const set_of_states s=i->second;
525 // if s is a superset of impl_spec.states()
526 // if (std::includes(impl_spec.states().begin(),impl_spec.states().end(),s.begin(),s.end()))
527 if (std::includes(s.begin(), s.end(), impl_spec.states().begin(),impl_spec.states().end()))
528 {
529 // set s must be removed.
530 i=anti_chain.erase(i);
531 }
532 else
533 {
534 ++i;
535 }
536 }
537 anti_chain.insert(std::pair<detail::state_type,detail::set_of_states>(impl_spec.state(),impl_spec.states()));
538 return true;
539 }
540
541 /* Calculate the states that are stable and reachable through tau-steps */
542 template < class LTS_TYPE >
544 const set_of_states& states,
545 const lts_cache<LTS_TYPE>& weak_property_cache)
546 {
547 static std::map<set_of_states, set_of_states> cache;
548 const std::map<set_of_states, set_of_states>::const_iterator i=cache.find(states);
549 if (i!=cache.end())
550 {
551 return i->second;
552 }
553
554 static set_of_states visited;
555 assert(visited.empty());
556 static std::stack < state_type > todo_stack;
557 assert(todo_stack.empty());
558 set_of_states result;
559
560 for(const state_type s: states)
561 {
562 if (weak_property_cache.stable(s))
563 {
564 // Put the outgoing action labels in a set and put these in the result.
565 result.insert(s);
566 }
567 else
568 {
569 visited.insert(s);
570 todo_stack.push(s);
571 }
572 }
573
574 while (todo_stack.size()>0)
575 {
576 const state_type current_state=todo_stack.top();
577 todo_stack.pop();
578 // Consider the states reachable in one tau step.
579 for(const state_type s: weak_property_cache.tau_reachable_states(current_state))
580 {
581 if (weak_property_cache.stable(s))
582 {
583 // Put the outgoing action labels in a set and put these in the result.
584 result.insert(s);
585 }
586 else
587 {
588 if (visited.insert(s).second) // t.to() is a new state.
589 {
590 todo_stack.push(s);
591 }
592 }
593 }
594 }
595 cache[states]=result;
596 visited.clear();
597 return cache[states];
598 }
599
606 template < class LTS_TYPE >
608 const state_type impl,
609 const set_of_states& spec,
610 const lts_cache<LTS_TYPE>& weak_property_cache,
611 label_type& culprit,
612 const LTS_TYPE& l,
613 const bool provide_a_counter_example,
614 const bool structured_output)
615 {
616 if (!weak_property_cache.stable(impl)) return true; // Checking in case of instability is not necessary, but rather time consuming.
617
618 const action_label_set& impl_action_labels = weak_property_cache.action_labels(impl);
619 bool success = false;
620
621 // Compare the obtained enable set of s' with all those of the specification.
622 for(const state_type s : spec)
623 {
624 // Only stable states in this set should be checked.
625 if (!weak_property_cache.stable(s)) { continue; }
626
627 // Check whether the enabled actions of spec are included in the enabled actions of impl.
628 // This is equivalent to checking that all spec_action_labels are in the impl_enabled_action_set.
629 const action_label_set& spec_action_labels = weak_property_cache.action_labels(s);
630
631 // Warning: std::includes checks whether the second range is included in the first.
632 bool inclusion_success = std::includes(impl_action_labels.begin(), impl_action_labels.end(),
633 spec_action_labels.begin(), spec_action_labels.end());
634 if (inclusion_success)
635 {
636 success = true;
637 break;
638 }
639 else
640 {
641 // Find the offending action.
642 for(const label_type a : spec_action_labels)
643 {
644 if (impl_action_labels.count(a) == 0) // We want to know which action caused the problem.
645 {
646 culprit = a;
647 break;
648 }
649 }
650 }
651 }
652
653 if (!success && provide_a_counter_example)
654 {
655 // Print the acceptance set of the implementation
656 if (impl_action_labels.empty())
657 {
658 if (structured_output)
659 {
660 std::cout << "left-acceptance:\n";
661 }
662 else
663 {
664 mCRL2log(log::verbose) << "The acceptance of the left process is empty.\n";
665 }
666 }
667 else
668 {
669 if (structured_output)
670 {
671 std::cout << "left-acceptance: ";
672 }
673 else
674 {
675 mCRL2log(log::verbose) << "A stable acceptance set of the left process is:\n";
676 }
677 std::string sep = "";
678 for (const label_type a: impl_action_labels)
679 {
680 if (structured_output)
681 {
682 std::cout << sep << l.action_label(a);
683 sep = ";";
684 }
685 else
686 {
687 mCRL2log(log::verbose) << l.action_label(a) << "\n";
688 }
689 }
690 if (structured_output)
691 {
692 std::cout << "\n";
693 }
694 }
695
696 // Print the acceptance sets of the specification.
697 if (spec.empty())
698 {
699 if (structured_output)
700 {
701 std::cout << "right-acceptance-sets: 0\n";
702 }
703 else
704 {
705 mCRL2log(log::verbose) << "The process at the right has no acceptance sets.\n";
706 }
707 }
708 else
709 {
710 set_of_states stable;
711 // Only the stable specification states contributed to this counter example.
712 std::copy_if(spec.begin(), spec.end(), std::inserter(stable,stable.end()), [=](const state_type s){return weak_property_cache.stable(s);});
713
714 if (structured_output)
715 {
716 std::cout << "right-acceptance-sets: " << stable.size () << "\n";
717 }
718 else
719 {
720 mCRL2log(log::verbose) << "Below all corresponding stable acceptance sets of the right process are provided:\n";
721 }
722 for (const state_type s: stable)
723 {
724 const action_label_set& spec_action_labels = weak_property_cache.action_labels(s);
725 if (structured_output)
726 {
727 std::cout << "right-acceptance: ";
728 }
729 else
730 {
731 mCRL2log(log::verbose) << "An acceptance set of the right process is:\n";
732 }
733 std::string sep = "";
734 for (const label_type a: spec_action_labels)
735 {
736 if (structured_output)
737 {
738 std::cout << sep << l.action_label(a);
739 sep = ";";
740 }
741 else
742 {
743 mCRL2log(log::verbose) << l.action_label(a) << "\n";
744 }
745 }
746 if (structured_output)
747 {
748 std::cout << "\n";
749 }
750 }
751 }
752 if (!structured_output)
753 {
754 mCRL2log(log::verbose) << "Finished printing acceptance sets.\n";
755 }
756 // Done printing acceptance sets.
757 }
758
759 return success;
760 }
761
762
763} // namespace detail
764} // namespace lts
765} // namespace mcrl2
766
767#endif // LIBLTS_FAILURES_REFINEMENT_H
Read-only balanced binary tree of terms.
implements the main algorithm for the branching bisimulation quotient
state_type get_eq_class(state_type const s) const
Get the equivalence class of a state.
void finalize_minimized_LTS()
Adapt the LTS after minimisation.
A class that can be used to construct counter examples if no.
bool stable(const state_type s) const
std::vector< std::vector< state_type > > m_tau_reachable_states
std::vector< action_label_set > m_enabled_actions
const std::vector< state_type > & tau_reachable_states(const state_type s) const
const action_label_set & action_labels(const state_type s) const
const std::vector< transition > & transitions(const state_type s) const
std::vector< std::vector< transition > > m_sorted_transitions
void calculate_weak_property_cache(const bool weak_reduction)
bool diverges(const state_type s) const
lts_cache(LTS_TYPE &l, const bool weak_reduction)
This class contains an scc partitioner removing inert tau loops.
Definition liblts_scc.h:128
std::size_t get_eq_class(const std::size_t s) const
Gives the equivalence class number of a state. The equivalence class numbers range from 0 upto (and e...
Definition liblts_scc.h:307
void replace_transition_system(const bool preserve_divergence_loops)
The lts for which this partioner is created is replaced by the lts modulo the calculated partition.
Definition liblts_scc.h:248
bool in_same_class(const std::size_t s, const std::size_t t) const
Returns whether two states are in the same bisimulation equivalence class.
Definition liblts_scc.h:313
const set_of_states & states() const
Get the set of states.
state_states_counter_example_index_triple(const state_type state, const set_of_states &states, const typename COUNTER_EXAMPLE_CONSTRUCTOR::index_type &counter_example_index)
Constructor.
void swap(state_states_counter_example_index_triple &other)
const COUNTER_EXAMPLE_CONSTRUCTOR::index_type & counter_example_index() const
Get the counter example index.
A class that contains a labelled transition system.
Definition lts.h:83
states_size_type initial_state() const
Gets the initial state number of this LTS.
Definition lts.h:326
void clear_state_labels()
Clear the labels of an lts.
Definition lts.h:506
This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate st...
Definition trace.h:52
A class containing triples, source label and target representing transitions.
Definition transition.h:43
O(m log n)-time branching bisimulation algorithm.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
@ verbose
Definition logger.h:35
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
std::multimap< detail::state_type, detail::set_of_states > anti_chain_type
std::size_t state_type
type used to store state (numbers and) counts
bool antichain_insert(anti_chain_type &anti_chain, const state_states_counter_example_index_triple< COUNTER_EXAMPLE_CONSTRUCTOR > &impl_spec)
std::size_t label_type
type used to store label numbers and counts
set_of_states collect_reachable_states_via_taus(const state_type s, const lts_cache< LTS_TYPE > &weak_property_cache, const bool weak_reduction)
const set_of_states & calculate_tau_reachable_states(const set_of_states &states, const lts_cache< LTS_TYPE > &weak_property_cache)
set_of_states collect_reachable_states_via_an_action(const state_type s, const label_type e, const lts_cache< LTS_TYPE > &weak_property_cache, const bool weak_reduction, const LTS_TYPE &l)
std::set< state_type > set_of_states
bool refusals_contained_in(const state_type impl, const set_of_states &spec, const lts_cache< LTS_TYPE > &weak_property_cache, label_type &culprit, const LTS_TYPE &l, const bool provide_a_counter_example, const bool structured_output)
This function checks that the refusals(impl) are contained in the refusals of spec,...
std::set< label_type > action_label_set
void report_statistics(refinement_statistics< T > &stats)
Print a message to debugging containing information about the given statistics.
std::pair< std::size_t, bool > reduce(LTS_TYPE &lts, const bool weak_reduction, const bool preserve_divergence, std::size_t l2_init)
Preprocess the LTS for destructive refinement checking.
bool destructive_refinement_checker(LTS_TYPE &l1, LTS_TYPE &l2, const refinement_type refinement, const bool weak_reduction, const lps::exploration_strategy strategy, const bool preprocess=true, COUNTER_EXAMPLE_CONSTRUCTOR generate_counter_example=detail::dummy_counter_example_constructor())
This function checks using algorithms in the paper mentioned above whether transition system l1 is in...
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
void swap(atermpp::unprotected_aterm &t1, atermpp::unprotected_aterm &t2) noexcept
Swaps two aterms.
Definition aterm.h:384
refinement_statistics(detail::anti_chain_type &antichain, std::deque< T > &working)