mCRL2
Loading...
Searching...
No Matches
liblts_bisim_gj.h
Go to the documentation of this file.
1// Author(s): Jan Friso Groote
2//
3// Copyright: see the accompanying file COPYING or copy at
4// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
5//
6// Distributed under the Boost Software License, Version 1.0.
7// (See accompanying file LICENSE_1_0.txt or copy at
8// http://www.boost.org/LICENSE_1_0.txt)
9
17
18#ifndef LIBLTS_BISIM_GJ_H
19#define LIBLTS_BISIM_GJ_H
20
21#include <forward_list>
22#include <deque>
25// #include "mcrl2/lts/detail/check_complexity.h"
26// #include "mcrl2/lts/detail/fixed_vector.h"
27
28
29namespace mcrl2
30{
31namespace lts
32{
33namespace detail
34{
35namespace bisimulation_gj
36{
37
38// Forward declaration.
39struct block_type;
40struct transition_type;
41
42typedef std::size_t state_index;
43typedef std::size_t action_index;
44typedef std::size_t transition_index;
45typedef std::size_t block_index;
46typedef std::size_t constellation_index;
47
49
50// Below the four main data structures are listed.
52{
54 std::vector<transition_index>::iterator start_incoming_transitions;
55 std::vector<transition_index>::iterator start_outgoing_inert_transitions;
56 std::vector<transition_index>::iterator start_outgoing_non_inert_transitions;
57 std::vector<state_index>::iterator ref_states_in_blocks;
58};
59
61{
62 // The position of the transition type corresponds to m_aut.get_transitions().
63 // std::size_t from, label, to are found in m_aut.transitions.
64 std::forward_list<transition_index > :: const_iterator transitions_per_block_to_constellation;
67 std::vector<std::size_t>::iterator trans_count;
68};
69
71{
73 std::vector<state_index>::iterator start_bottom_states;
74 std::vector<state_index>::iterator start_non_bottom_states;
75 std::forward_list< transition_index > block_to_constellation;
76
77 block_type(const std::vector<state_index>::iterator beginning_of_states, constellation_index c)
78 : constellation(c),
79 start_bottom_states(beginning_of_states),
80 start_non_bottom_states(beginning_of_states)
81 {}
82};
83
85{
88
90 : start_block(start),
91 end_block(end)
92 {}
93};
94
95// The struct below facilitates to walk through a L_B_C_list starting from an arbitrary transition.
97{
98 bool walk_backwards=true;
101 const std::vector<transition_type>& m_transitions;
102
103 L_B_C_list_iterator(const transition_index ti, const std::vector<transition_type>& transitions)
104 : m_start_transition(ti),
106 m_transitions(transitions)
107 {}
108
110 {
111 if (walk_backwards)
112 {
115 {
116 walk_backwards=false;
118 }
119 }
120 else
121 {
123 }
124 }
125
127 {
129 }
130
131 // Equality is implemented minimally for the purpose of this algorithm,
132 // essentially only intended to compare the iterator to its end, i.e., null_transition.
133 bool operator ==(const L_B_C_list_iterator& it) const
134 {
136 }
137};
138
139/* struct L_B_C_list_walker
140{
141 typedef L_B_C_list_iterator iterator;
142
143 const transition_index start_transition;
144 std::vector<transition_type>& m_transitions;
145
146
147 L_B_C_list_walker(const transition_index ti, const std::vector<transition_type>& transitions)
148 : start_transtition(ti),
149 m_transitions.
150 {}
151} */
152
153} // end namespace bisimulation_gj
154
155
156/*=============================================================================
157= main class =
158=============================================================================*/
159
160
162
163
164
168template <class LTS_TYPE>
170{
171 protected:
172 typedef typename LTS_TYPE::labels_size_type label_index;
173 typedef typename LTS_TYPE::states_size_type state_index;
174 typedef std::unordered_set<state_index> set_of_states_type;
175 typedef std::unordered_set<constellation_index> set_of_constellations_type;
176 typedef std::unordered_map<label_index, set_of_states_type > states_per_action_label_type;
177 typedef std::unordered_map<block_index, set_of_states_type > states_per_block_type;
178 typedef std::unordered_map<std::pair<state_index, label_index>, std::size_t> state_label_to_size_t_map;
179 typedef std::unordered_map<label_index, std::size_t> label_to_size_t_map;
180
182 {
183 static const set_of_states_type s=set_of_states_type();
184 return s;
185 }
186
188 LTS_TYPE& m_aut;
189
190 // Generic data structures.
191 std::vector<state_type_gj> m_states;
192 std::vector<std::reference_wrapper<transition_type>> m_incoming_transitions;
193 std::vector<std::reference_wrapper<transition_type>> m_outgoing_transitions;
194 std::vector<transition_type> m_transitions;
195 std::deque<std::size_t> m_state_to_constellation_count;
196 std::vector<state_index> m_states_in_blocks;
197 std::vector<block_type> m_blocks;
198 std::vector<constellation_type> m_constellations;
200
202 const bool m_branching;
203
210
213
214 std::size_t number_of_states_in_block(const block_index B) const
215 {
216 if (m_blocks.size()==B+1) // This is the last block.
217 {
218 return m_states_in_blocks.size()-m_blocks[B].start_bottom_states;
219 }
220 return m_blocks[B+1].start_bottom_states-m_blocks[B].start_bottom_states;
221 }
222
223 public:
236 bisim_partitioner_gj(LTS_TYPE& aut,
237 const bool branching = false,
238 const bool preserve_divergence = false)
239 : m_aut(aut),
240 m_states(aut.num_states()),
241 m_transitions(aut.num_transitions()),
242 m_blocks(1,{m_states_in_blocks.begin(),0}),
243 m_constellations(1,constellation_type(0,1)), // Algorithm 1, line 1.2.
244 m_branching(branching),
245 m_preserve_divergence(preserve_divergence)
246 {
250 }
251
252
258 {
259 return m_blocks.size();
260 }
261
262
271 {
272 assert(s<m_blocks.size());
273 return m_states[s].block;
274 }
275
276
290 {
291 std::unordered_set<transition> T;
292 for(const transition& t: m_aut.get_transitions())
293 {
294 T.insert(transition(get_eq_class(t.from()), t.label(), t.to()));
295 }
296 for (const transition t: T)
297 {
298 m_aut.add_transition(t);
299 }
300
301 // Merge the states, by setting the state labels of each state to the
302 // concatenation of the state labels of its equivalence class.
303
304 if (m_aut.has_state_info()) /* If there are no state labels this step is not needed */
305 {
306 /* Create a vector for the new labels */
307 std::vector<typename LTS_TYPE::state_label_t> new_labels(num_eq_classes());
308
309
310 for(std::size_t i=0; i<m_aut.num_states(); ++i)
311 {
312 const state_type_gj new_index(get_eq_class(i));
313 new_labels[new_index]=new_labels[new_index]+m_aut.state_label(i);
314 }
315
316 m_aut.set_num_states(num_eq_classes());
317 for (std::size_t i=0; i<num_eq_classes(); ++i)
318 {
319 m_aut.set_state_label(i, new_labels[i]);
320 }
321 }
322 else
323 {
324 m_aut.set_num_states(num_eq_classes());
325 }
326
327 m_aut.set_initial_state(get_eq_class(m_aut.initial_state()));
328 }
329
330
335 bool in_same_class(state_index const s, state_index const t) const
336 {
337 return get_eq_class(s) == get_eq_class(t);
338 }
339 protected:
340
341 /*--------------------------- main algorithm ----------------------------*/
342
343
344 // Traverse the states in block co_bi to determine which of the states in
345 // block bi did become new bottom states.
347 const block_index /* bi */,
348 const block_index /* co_bi */)
349 {
350 assert(0);
351 // XXX TODO.
352 }
353
354 // Traverse the states in block bi and determine which did become bottom states.
356 const block_index bi)
357
358 {
359 for(typename std::vector<state_index>::iterator si=m_blocks[bi].start_non_bottom_states;
360 si!=m_states_in_blocks.end() &&
361 (bi+1==m_blocks.size() || si!=m_blocks[bi+1].start_bottom_states);
362 ++si)
363 {
364 const state_type_gj& s= m_states[si];
365 bool no_inert_transition_seen=true;
366 for(std::vector<transition_index>::iterator ti=s.start_incoming_transitions;
367 m_aut.is_tau(m_aut.get_transitions()[ti].label()) &&
368 ti!=m_incoming_transitions.end() &&
369 ti!=(si+1)->get().start_incoming_transitions;
370 ti++)
371 {
372 if (m_states[m_aut.get_transitions()[ti].from()].block==m_states[m_aut.get_transitions()[ti].to()].block)
373 {
374 // This transition is inert.
375 no_inert_transition_seen=false;
376 ti++;
377 }
378 else
379 {
380 // This transition is non-inert
381 }
382 }
383 if (no_inert_transition_seen)
384 {
385 m_P[bi].insert(*si);
386 }
387 }
388 }
389
390 // Move transitions that became non-inert to their proper place in
391 // m_incoming_transitions
392 // m_outgoing_transitions
393 // m_states_in_blocks
394 // Moreover, record the states that became bottom states in m_P;
396 {
397 // Calculate the newly obtained bottom states and put them in m_P.
398 // We walk through all non-bottom states of blocks.
399 for(block_index bi=0; bi<m_blocks.size(); ++bi)
400 {
402 }
403 }
404
405 /*----------------- SplitB -- Algorithm 3 of [GJ 2024] -----------------*/
406
408 {
411 m_blocks[m_states_in_blocks[pos3]].ref_states_in_block=pos3;
413 m_blocks[m_states_in_blocks[pos2]].ref_states_in_block=pos2;
414 m_states_in_blocks[pos1]=temp;
415 m_blocks[m_states_in_blocks[pos1]].ref_states_in_block=pos1;
416 }
417
418 block_index split_block_B_into_R_and_BminR(const block_index B, const std::unordered_set<state_index>& R)
419 {
420 m_blocks.emplace_back(m_blocks[B].bottom_states,m_blocks[B].constellation);
421 m_non_trivial_constellations.insert(m_blocks[B].constellation);
422 const block_index new_block_index=m_blocks.size()-1;
423 for(state_index s: R)
424 {
425 m_states[s].block=new_block_index;
426 std::size_t pos=m_states[s].ref_states_in_block;
427 if (pos>=m_blocks[B].non_bottom_states) // the state is a non bottom state.
428 {
429 swap_states_in_states_in_block(pos,m_blocks[B].bottom_states,m_blocks[B].non_bottom_states);
430 }
431 else // the state is a non bottom state
432 {
433 swap_states_in_states_in_block(pos,m_blocks[new_block_index].bottom_states,m_blocks[B].non_bottom_states);
434 }
435 m_blocks[B].bottom_states++;
436 m_blocks[B].non_bottom_states++;
437 }
438 return new_block_index;
439 }
440
442 const transition& t,
443 const transition_index ti,
444 std::forward_list<transition_index > :: iterator position)
445 {
446 std::forward_list<transition_index > :: iterator this_block_to_constellation=
447 m_transitions[ti].transitions_per_block_to_constellation;
448 transition_index& current_transition_index= *position;
449 // Check whether this is an inert transition.
450 if (m_aut.is_tau(t.label()) &&
451 m_states[t.from()].block==m_states[t.to()].block)
452 {
453 // insert before current transition.
454 m_transitions[ti].next_L_B_C_element=current_transition_index;
455 m_transitions[ti].previous_L_B_C_element=m_transitions[ti].previous_L_B_C_element;;
456 if (m_transitions[current_transition_index].previous_L_B_C_element!=null_transition)
457 {
458 m_transitions[m_transitions[current_transition_index].previous_L_B_C_element].next_L_B_C_element=ti;
459 }
460 m_transitions[current_transition_index].previous_L_B_C_element=ti;
461 }
462 else
463 {
464 // insert after current transition.
465 m_transitions[ti].previous_L_B_C_element=current_transition_index;
466 m_transitions[ti].next_L_B_C_element=m_transitions[ti].previous_L_B_C_element;;
467 if (m_transitions[current_transition_index].next_L_B_C_element!=null_transition)
468 {
469 m_transitions[m_transitions[current_transition_index].next_L_B_C_element].previous_L_B_C_element=ti;
470 }
471 m_transitions[current_transition_index].next_L_B_C_element=ti;
472 }
473 }
474
475 // Move the transition t with transition index ti to an new
476 // L_B_C list if its source state is in block B and the target state switches to a new constellation.
477
479 const block_index index_block_B,
480 const transition& t,
481 const transition_index ti)
482 {
483 if (m_states[t.from()].block==index_block_B)
484 {
485 std::forward_list<transition_index > :: iterator this_block_to_constellation=
486 m_transitions[ti].transitions_per_block_to_constellation;
487 std::forward_list<transition_index > :: iterator next_block_to_constellation=
488 ++std::forward_list<transition_index > :: iterator(this_block_to_constellation);
489 if (next_block_to_constellation==m_blocks[m_states[t.from()].block].end() ||
490 *next_block_to_constellation==null_transition ||
491 m_blocks[m_aut.get_transitions()[*next_block_to_constellation].to()]!=index_block_B ||
492 m_aut.get_transitions()[*next_block_to_constellation].label()!=t.label())
493 {
494 // Make a new entry in the list next_block_to_constellation;
495 next_block_to_constellation=
496 m_blocks[m_states[m_transitions[ti].from()].block].block_to_constellation.
497 insert_after(this_block_to_constellation, ti);
498 }
499 // Move the current transition to the next list.
500 // First check whether this_block_to_constellation contains exactly transition ti.
501 // It must be replaced by a later or earlier element from the L_B_C_list.
502 bool last_element_removed=remove_from_the_doubly_linked_list_L_B_C_in_blocks(ti);
503 insert_in_the_doubly_linked_list_L_B_C_in_blocks(t, ti, next_block_to_constellation);
504
505 if (last_element_removed)
506 {
507 // move the L_B_C_list in next_block_to_constellation to block_to_constellation
508 // and remove the next element.
509 *this_block_to_constellation = *next_block_to_constellation;
510 m_blocks[m_states[m_transitions[ti].from()].block].this_block_to_constellation.
511 erase_after(this_block_to_constellation);
512 }
513 }
514 }
515
516 // Update the L_B_C list of a transition, when the from state of the transition moves
517 // from block old_bi to new_bi.
519 const block_index old_bi,
520 const block_index new_bi,
521 const transition& t,
522 const transition_index ti,
523 std::unordered_set< std::pair <action_index, constellation_index>,
524 std::forward_list< transition_index >::iterator>& new_LBC_list_entries)
525 {
526 assert(m_states[t.from()].block==old_bi);
527
528 std::forward_list<transition_index > :: iterator this_block_to_constellation=
529 m_transitions[ti].transitions_per_block_to_constellation;
530 std::forward_list<transition_index > :: iterator next_block_to_constellation=
531 ++std::forward_list<transition_index > :: iterator(this_block_to_constellation);
532 std::unordered_set< std::pair <action_index, constellation_index>,
533 std::forward_list< transition_index >::iterator>::iterator it=
534 new_LBC_list_entries.find(std::pair(t.label(), m_blocks[m_states[t.from()].block].constellation));
535 bool last_element_removed=remove_from_the_doubly_linked_list_L_B_C_in_blocks(ti);
536 if (it==new_LBC_list_entries.end())
537 {
538 // Make a new entry in the list next_block_to_constellation;
539 m_blocks[new_bi].next_block_to_constellation.push_front(ti);
540 new_LBC_list_entries[std::pair(t.label(), m_blocks[m_states[t.from()].block].constellation)]=
541 m_blocks[new_bi].block_to_constellations.begin();
545 }
546 else
547 {
548 // Move the current transition to the next list indicated by the iterator it.
550 }
551
552 if (last_element_removed)
553 {
554 // move the L_B_C_list in next_block_to_constellation to block_to_constellation
555 // and remove the next element.
556 *this_block_to_constellation = *next_block_to_constellation;
557 m_blocks[m_states[m_transitions[ti].from()].block].this_block_to_constellation.
558 erase_after(this_block_to_constellation);
559 }
560 }
561
562 // Calculate the states R in block B that can inertly reach M and split
563 // B in R and B\R. The complexity is conform the smallest block of R and B\R.
564 // The L_B_C_list, trans_count and bottom states are not updated.
565 // Provide the index of the newly created block as a result. This block is the smallest of R and B\R.
566 // Return in M_in_bi whether the new block bi is the one containing M.
567 template <class MARKED_STATE_ITERATOR,
568 class UNMARKED_STATE_ITERATOR>
570 const MARKED_STATE_ITERATOR M_begin,
571 const MARKED_STATE_ITERATOR M_end,
572 const std::function<bool(state_index)>& marked_blocker,
573 const UNMARKED_STATE_ITERATOR M_co_begin,
574 const UNMARKED_STATE_ITERATOR M_co_end,
575 const std::function<bool(state_index)>& unmarked_blocker,
576 bool& M_in_bi)
577 {
578 const std::size_t B_size=number_of_states_in_block(B);
579 std::unordered_set<state_index> U, U_todo;
580 std::unordered_set<state_index> R, R_todo;
581 typedef enum { initializing, state_checking, aborted } status_type;
582 status_type U_status=initializing;
583 status_type R_status=initializing;
584 MARKED_STATE_ITERATOR M_it=M_begin;
585 UNMARKED_STATE_ITERATOR M_co_it=M_co_begin;
586 const state_index bottom_state_walker_end=m_blocks[B].start_bottom_states;
587
588 // Algorithm 3, line 3.2 left.
589 std::unordered_map<state_index, size_t> count;
590
591
592 // start coroutines. Each co-routine handles one state, and then gives control
593 // to the other co-routine. The coroutines can be found sequentially below surrounded
594 // by a while loop.
595
596 while (true)
597 {
598 // The code for the left co-routine.
599 switch (U_status)
600 {
601 case initializing:
602 {
603 // Algorithm 3, line 3.3 left.
604 if (M_co_it==M_co_end)
605 {
606 U_status=state_checking;
607 }
608 else
609 {
610 const state_index si=state_in_blocks(*M_co_it);
611 if (!unmarked_blocker(si))
612 {
613 U_todo.insert(si);
614 }
615 }
616 break;
617 }
618 case state_checking:
619 {
620 // Algorithm 3, line 3.22 and line 3.23.
621 if (U_todo.empty())
622 {
623 assert(!U.empty());
624 // split_block B into U and B\U.
625 block_index block_index_of_U=split_block_B_into_R_and_BminR(B, U);
626 M_in_bi = false;
627 return block_index_of_U;
628 }
629 else
630 {
631 const state_index s=U_todo.extract(U_todo.begin());
632 U.insert(s);
633 count(s)=0;
634 // Algorithm 3, line 3.8.
635 for(transition_index t=m_states[s].start_outgoing_inert_transitions;
636 t<m_states[s].start_non_inert_outgoing_transitions;
637 t++)
638 {
639 // Algorithm 3, line 3.11.
640 state_index from=m_aut.get_transitions()[t];
641 if (count.find(from)==count.end()) // count(from) is undefined;
642 {
643 // Algorithm 3, line 3.12.
644 if (unmarked_blocker(from)>0)
645 {
646 // Algorithm 3, line 3.13.
647 count[from]=std::numeric_limits<std::size_t>::max;
648 }
649 else
650 {
651 // Algorithm 3, line 3.14 and 3.17.
652 count[from]=m_states[from].start_non_inert_outgoing_transitions-
653 m_states[from].start_outgoing_inert_transitions-1;
654 }
655 }
656 else
657 {
658 // Algorithm 3, line 3.17.
659 count[from]=m_states[from]--;
660 }
661 // Algorithm 3, line 3.18.
662 if (count[from]==0)
663 {
664 if (U.count(from)==U.end())
665 {
666 U_todo.insert(from);
667 }
668 }
669 }
670 }
671 // Algorithm 3, line 3.9 and line 3.10 left.
672 if (2*(U.size()+U_todo.size())>B_size)
673 {
674 U_status=aborted;
675 }
676 }
677 default: break;
678 }
679 // The code for the right co-routine.
680 switch (R_status)
681 {
682 case initializing:
683 {
684 // Algorithm 3, line 3.3 right.
685 if (M_it==M_end)
686 {
687 R_status=state_checking;
688 }
689 else
690 {
691 const state_index si=state_in_blocks(*M_it);
692 if (!marked_blocker(si))
693 {
694 R_todo.insert(si);
695 }
696 }
697 break;
698 }
699 case state_checking:
700 {
701 if (R_todo.empty())
702 {
703 // split_block B into R and B\R.
704 block_index block_index_of_R=split_block_B_into_R_and_BminR(B, R);
705 M_in_bi=true;
706 return block_index_of_R;
707 }
708 else
709 {
710 const state_index s=R_todo.extract(R_todo.begin());
711 R.insert(s);
712 for(transition_index t=m_states[s].incoming_transitions;
713 m_aut.is_tau(m_aut.get_transitions()[t].label()) &&
714 m_states[m_aut.get_transitions()[t].from()].block==m_states[m_aut.get_transitions()[t].to()].block;
715 t++)
716 {
717 const transition& tr=m_aut.get_transitions()[t];
718 if (R.count(tr.from())==0)
719 {
720 R.todo.insert(tr.from());
721 }
722 }
723 // Algorithm 3, line 3.9 and line 3.10 Right.
724 if (2*(R.size()+R_todo.size())>B_size)
725 {
726 R_status=aborted;
727 }
728 }
729 }
730 default: break;
731 }
732 }
733 }
734
735 // Split block B in R, being the inert-tau transitive closure of M minus those in marked_blocker contains
736 // states that must be in block, and M\R. M_nonmarked, minus those in unmarked_blocker, are those in the other block.
737 // The splitting is done in time O(min(|R|,|B\R|). Return the block index of the smallest
738 // block, which is newly created. Indicate in M_in_new_block whether this new block contains M.
739 template <class MARKED_STATE_ITERATOR,
740 class UNMARKED_STATE_ITERATOR>
742 const MARKED_STATE_ITERATOR M_begin,
743 const MARKED_STATE_ITERATOR M_end,
744 const std::function<bool(state_index)>& marked_blocker,
745 const UNMARKED_STATE_ITERATOR M_co_begin,
746 const UNMARKED_STATE_ITERATOR M_co_end,
747 const std::function<bool(state_index)>& unmarked_blocker,
748 bool& M_in_new_block)
749 {
750 assert(M_begin!=M_end && M_co_begin!=M_co_end);
751 block_index bi=simple_splitB(B, M_begin, M_end, marked_blocker, M_co_begin, M_co_end, unmarked_blocker, M_in_new_block);
752
753
754 // Update the L_B_C_list, and bottom states, and invariant on inert transitions.
755 for(typename std::vector<state_index>::iterator si=m_blocks[bi].start_bottom_states;
756 si!=m_states_in_blocks.end() &&
757 (bi+1==m_blocks.size() || si!=m_blocks[bi+1].start_bottom_states);
758 ++si)
759 {
760 state_type_gj& s= m_states[si];
761 s.block=bi;
762
763 bool no_inert_transition_seen=true;
764
765 // Adapt the L_B_C_list.
766 std::unordered_set< std::pair <action_index, constellation_index>,
767 std::forward_list< transition_index >::iterator> new_LBC_list_entries;
768 for(std::vector<transition_index>::iterator ti=s.start_outgoing_inert_transitions;
770 )
771 {
772 // Situation below is only relevant if not M_in_new_block;
773 if (!M_in_new_block)
774 {
775 const transition& t=m_aut.get_transitions()[*ti];
776 assert(m_aut.is_tau(t.label()));
777 if (m_states[t.from()].block()!=m_states[t.to()].block())
778 {
779 // This is a transition that has become non-inert.
780 // Swap this transition to the non-inert transitions.
783 *ti=temp;
785 // Do not increment ti as it refers to a new transition.
786 }
787 else
788 {
789 update_the_doubly_linked_list_L_B_C_new_block(B, bi, *ti, m_transitions[*ti], new_LBC_list_entries);
790 no_inert_transition_seen=false;
791 ti++;
792 }
793 }
794 }
795
796 for(std::vector<transition_index>::iterator ti=s.start_outgoing_non_inert_transitions;
797 m_aut.is_tau(m_aut.get_transitions()[ti].label()) &&
798 ti!=m_outgoing_transitions.end() &&
799 ti!=(si+1)->get().start_outgoing_transitions;
800 ti++)
801 {
802 update_the_doubly_linked_list_L_B_C_new_block(B, bi, *ti, m_transitions[*ti], new_LBC_list_entries);
803 }
804
805 if (no_inert_transition_seen)
806 {
807 // The state at si has become a bottom_state.
808 m_P.insert(*si);
809 // Move this former non bottom state to the bottom states.
810 state_index temp=*si;
811 *si=*(m_blocks[bi].start_non_bottom_states);
812 *(m_blocks[bi].start_non_bottom_states)=temp;
813 m_blocks[bi].start_non_bottom_states++;
814 }
815
816 // Investigate the incoming tau transitions.
817 if (M_in_new_block)
818 {
819 std::vector<std::vector<transition_index>::iterator> transitions_that_became_non_inert;
820 std::vector<transition_index>::iterator last_former_inert_transition;
821 for(std::vector<transition_index>::iterator ti=s.start_incoming_transitions;
822 m_aut.is_tau(m_aut.get_transitions()[ti].label()) &&
823 ti!=m_incoming_transitions.end() &&
824 ti!=(si+1)->get().start_incoming_transitions;
825 ti++)
826 {
827 if (m_states[m_aut.get_transitions()[*ti].from()].block==
828 m_states[m_aut.get_transitions()[*ti].to()].block)
829 {
830 last_former_inert_transition=ti;
831 }
832 if (m_states[m_aut.get_transitions()[*ti].from()].block==B &&
833 m_states[m_aut.get_transitions()[*ti].to()].block==bi)
834 {
835 last_former_inert_transition=ti;
836 // This transition did become non-inert.
837 transitions_that_became_non_inert.push_back(ti);
838 // Check whether from is a new bottom state.
839 state_index from=m_aut.get_transitions()[*ti].from();
840 transition& from_trans= m_aut.transitions(*m_states[from].outgoing_transitions);
841 assert(from_trans.from()==from);
842 if (m_states[from].block!=m_states[from_trans.to()].block ||
843 !m_aut.is_tau(from_trans.label()))
844 {
845 // This transition is not inert. The state from is a new bottom state.
846 m_P.insert(from);
847 // Move this former non bottom state to the bottom states.
848 typename std::vector<state_index>::iterator position_in_states_in_blocks=m_states[from].ref_states_in_blocks;
849 state_index temp=*position_in_states_in_blocks;
850 block_index temp_bi=m_states[from].block;
851 *position_in_states_in_blocks=*(m_blocks[temp_bi].start_non_bottom_states);
852 *(m_blocks[temp_bi].start_non_bottom_states)=temp;
853 m_blocks[temp_bi].start_non_bottom_states++;
854 }
855 }
856 }
857 // Move the non_inert_transitions to the end.
858 while(!transitions_that_became_non_inert.empty())
859 {
860 std::vector<transition_index>::iterator tti=transitions_that_became_non_inert.back();
861 transitions_that_became_non_inert.pop_back();
862 transition_index temp= *tti;
863 *tti=*last_former_inert_transition;
864 *last_former_inert_transition=temp;
865 }
866 }
867 }
868
869 return bi;
870 }
871
872
874 {
875 mCRL2log(log::verbose) << "An O(m log n) "
877 ? "divergence-preserving branching "
878 : "branching ")
879 : "")
880 << "bisimulation partitioner created for " << m_aut.num_states()
881 << " states and " << m_aut.num_transitions() << " transitions.\n";
882 // Initialisation.
883
884 // Initialise m_incoming_transitions and m_transitions.trans_count and m_transitions.transitions_per_block_to_constellation.
885 typedef std::unordered_multimap<typename std::pair<typename LTS_TYPE::states_size_type, typename LTS_TYPE::labels_size_type>,
886 transition&> temporary_store_type;
887 temporary_store_type temporary_store;
888 for(const transition& t: m_aut.get_transitions())
889 {
890 temporary_store[std::pair(t.from(),t.label())]=t;
891 }
892 state_index current_from_state=-1;
893 label_index current_label=-1;
894 m_incoming_transitions.reserve(m_aut.num_transitions());
895 for(auto [_,t]: temporary_store)
896 {
897 m_incoming_transitions.emplace(t);
898 if (t.from()!=current_from_state || t.label()!=current_label)
899 {
900 m_state_to_constellation_count.emplace_back(1);
901 m_blocks[0].block_to_constellation.push_front(t);
902 current_label=t.label();
903 }
904 else
905 {
906 assert(m_state_to_constellation_count.size()>0);
908 m_blocks[0].block_to_constellation.front().push_front(t);
909 }
910 if (t.from()!=current_from_state)
911 {
912 m_states[t.from()].start_incoming_transitions=m_incoming_transitions.end()-1;
913 current_from_state=t.from();
914 }
915 std::size_t transition_index=std::distance(t,m_aut.get_transitions().begin());
917 m_transitions[transition_index].transitions_per_block_to_constellation=m_blocks[0].block_to_constellation.front().begin();
918 }
919 temporary_store.clear();
920
921 // Initialise m_outgoing_transitions and
922 // initialise m_states_in_blocks, together with start_bottom_states start_non_bottom_states in m_blocks.
923 std::vector<bool> state_has_outgoing_tau(m_aut.num_states(),false);
924 for(const transition& t: m_aut.get_transitions())
925 {
926 temporary_store[std::pair(t.to(),t.label())]=t;
927 if (m_aut.is_tau(t))
928 {
929 state_has_outgoing_tau[t.from()]=true;
930 }
931 }
932 m_outgoing_transitions.reserve(m_aut.num_transitions());
933 typename LTS_TYPE::states_sizes_type current_to_state=-1;
934 for(auto [_,t]: temporary_store)
935 {
936 m_outgoing_transitions.emplace(t);
937 if (t.to()!=current_to_state)
938 {
939 m_states[t.to()].start_outgoing_inert_transitions=m_outgoing_transitions.end()-1;
940 current_to_state=t.to();
941 }
942 }
943 temporary_store=temporary_store_type(); // release memory.
944
945 m_states_in_blocks.reserve(m_aut.num_states());
946 std::size_t i=0;
947 for(bool b: state_has_outgoing_tau)
948 {
949 if (b)
950 {
951 m_states_in_blocks.emplace_back(i);
952 }
953 i++;
954 }
955 m_blocks[0].start_bottom_states=0;
956 m_blocks[0].start_non_bottom_states=i;
957 i=0;
958 for(bool b: state_has_outgoing_tau)
959 {
960 if (!b)
961 {
962 m_states_in_blocks.emplace_back(i);
963 }
964 i++;
965 }
966
967 // The data structures are now initialized.
968 // The following implements line 1.3 of Algorithm 1.
969 states_per_action_label_type states_per_action_label;
970 for(const transition& t: m_aut.get_transitions())
971 {
972 states_per_action_label[t.label()]=states_per_action_label[t.label()].insert(t.from());
973 }
974
975 for(const set_of_states_type& stateset: states_per_action_label)
976 {
977 for(const set_of_states_type& M: stateset)
978 {
980 for(const state_index s: M)
981 {
982 Bprime[m_states[s].block].insert(s);
983 }
984
985 for(auto [block_index, split_states]: Bprime)
986 {
987 // Check whether the block B, indexed by block_index, can be split.
988 // This means that the bottom states of B are not all in the split_states.
991 {
992 if (!split_states.contains(i))
993 {
994 simpleSplitB(block_index, split_states);
995 i=B.start_non_bottom_states; // This means break the loop.
996 }
997 }
998 }
999 }
1000 }
1001
1002 std::unordered_map<block_index, set_of_states_type> P;
1004 }
1005
1006 // Update the doubly linked list L_B->C in blocks.
1007 // First removing and adding a single element are implemented.
1008 //
1009 // If there is more than one element it is removed.
1010 // In that case false is returned. Otherwise, the result is true,
1011 // and the element is actually not removed.
1013 {
1014 if (m_transitions[ti].previous_L_B_C_element==null_transition &&
1015 m_transitions[ti].previous_L_B_C_element==null_transition)
1016 {
1017 // This is the only element in the list. Leave it alone.
1018 return true;
1019 }
1020 else
1021 {
1022 // There is more than one element.
1023 if (m_transitions[ti].previous_L_B_C_element!=null_transition)
1024 {
1025 m_transitions[m_transitions[ti].previous_L_B_C_element].next_L_B_C_element=
1026 m_transitions[ti].next_L_B_C_element;
1027 }
1028 if (m_transitions[ti].next_L_B_C_element!=null_transition)
1029 {
1030 m_transitions[m_transitions[ti].next_L_B_C_element].previous_L_B_C_element=
1031 m_transitions[ti].previous_L_B_C_element;
1032 }
1033 return false;
1034 }
1035 }
1036
1037
1038 // Algorithm 4. Stabilize the current partition with respect to the current constellation
1039 // given that the states in m_P did become new bottom states.
1040
1042 {
1043 // Algorithm 4, line 4.3.
1044 std::unordered_map<block_index, set_of_states_type> Phat;
1045 for(const state_index si: m_P)
1046 {
1047 Phat[m_states[si].block].insert(si);
1048 }
1049 m_P.clear();
1050
1051 // Algorithm 4, line 4.4.
1052 while (!Phat.empty())
1053 {
1054 // Algorithm 4, line 4.5.
1055 const block_index bi=Phat.front().first;
1056 const set_of_states_type& V=Phat.front().second;
1057 Phat.erase(bi);
1058
1059 // Algorithm 4, line 4.6.
1060 // Collect all new bottom states and group them per action-constellation pair.
1061 std::unordered_map<std::pair<action_index, constellation_index>, state_index> grouped_transitions;
1062 for(const state_index si: V)
1063 {
1064 for(transition_index ti=m_states[si].outgoing_transitions;
1065 ti!=m_outgoing_transitions.size() &&
1066 (si+1>=m_states.size() || ti!=m_states[si+1].outgoing_transitions);
1067 ++ti)
1068 {
1069 transition& t=m_aut.get_transitions()[ti];
1070 grouped_transitions[std::pair(t.label(), m_blocks[m_states[t.to()].block()].constellation())]=t.from();
1071 }
1072 }
1073
1074 // Algorithm 4, line 4.7, and implicitly 4.8.
1075 for(std::forward_list< transition_index >::iterator Q=m_blocks[bi].block_to_constellation.begin();
1076 Q!=m_blocks[bi].block_to_constellation.end(); ++Q)
1077 {
1078 // Algorithm 4, line 4.9.
1080 transition& t=m_aut.get_transitions()[*Q];
1081 set_of_states_type& aux=grouped_transitions[std::pair(t.label(), m_blocks[m_states[t.to()].block()].constellation())];
1082 W.erase(aux.begin(),aux.end());
1083 // Algorithm 4, line 4.10.
1084 if (!W.empty())
1085 {
1086 // Algorithm 4, line 4.11, and implicitly 4.12.
1087 bool V_in_bi=false;
1088 block_index bi_new=splitB(bi,
1089 m_blocks[bi].start_bottom_states,
1090 m_blocks[bi].start_non_bottom_states,
1091 [&W](const state_index si){ return W.count(si)!=0; },
1092 W.begin(),
1093 W.end(),
1094 [](const state_index ){ return false; },
1095 V_in_bi);
1096 // Algorithm 4, line 4.13.
1097 if (V_in_bi)
1098 {
1099 // The new bottom states V are in block bi, and block bi is the largest block of bi and bi_new.
1101 }
1102 else
1103 {
1104 // The new bottom states V are in block bi_new, and block bi is the largest block of bi and bi_new.
1106 }
1107
1108 }
1109 }
1110
1111 // Algorithm 4, line 4.17.
1112 for(const state_index si: m_P)
1113 {
1114 Phat[m_states[si].block].insert(si);
1115 }
1116 m_P.clear();
1117
1118 }
1119 }
1120
1122 {
1123 // This represents the while loop in Algorithm 1 from line 1.6 to 1.25.
1124
1125 // Algorithm 1, line 1.6.
1126 while (!m_non_trivial_constellations.empty())
1127 {
1128 const set_of_constellations_type::const_iterator i=m_non_trivial_constellations.begin();
1129 constellation_index ci= *i;
1131
1132 // Algorithm 1, line 1.7.
1133 std::size_t index_block_B=m_constellations[ci].start_block;
1134 if (number_of_states_in_block(index_block_B)<number_of_states_in_block(index_block_B+1))
1135 {
1136 m_states_in_blocks[index_block_B].swap(m_states_in_blocks[index_block_B+1]);
1137 }
1138
1139 // Algorithm 1, line 1.8.
1140 m_constellations[ci].start_block=index_block_B+1;
1141 if (m_constellations[ci].start_block!=m_constellations[ci].end_block) // Constellation is not trivial.
1142 {
1144 }
1145 m_constellations.emplace_back(index_block_B, index_block_B);
1146 // Here the variables block_to_constellation and the doubly linked list L_B->C in blocks must be still be updated.
1147 // Moreover, the variable m_state_to_constellation_count in transitions requires updating.
1148 // This happens below.
1149
1150 // Algorithm 1, line 1.9.
1152 state_label_to_size_t_map newly_created_state_to_constellation_count_entry;
1153 label_to_size_t_map label_to_transition;
1154 state_label_to_size_t_map outgoing_transitions_count_per_label_state;
1155
1156
1157 // Walk through all states in block B
1158 for(typename std::vector<state_index>::iterator i=m_states_in_blocks[index_block_B].start_bottom_states;
1159 i!=m_states_in_blocks.end() &&
1160 (index_block_B+1>m_blocks.size() || i!=m_states_in_blocks[index_block_B+1].start_bottom_states);
1161 ++i)
1162 {
1163 // and visit the incoming transitions.
1164 for(std::vector<transition_index>::iterator j=i->get().start_incoming_transitions;
1165 j!=m_incoming_transitions.end() &&
1166 (i+1!=m_states_in_blocks.end() || j!=(i+1)->get().start_incoming_transitions);
1167 ++j)
1168 {
1169 const transition& t=m_aut.transitions[*j];
1170 // Add the source state grouped per label in calM, provided the transition is non inert.
1171 if (!m_aut.is_tau(t.label()) || m_states[t.from()].m_block!=m_states[t.to()].m_block)
1172 {
1173 calM[t.label()].insert(t.from());
1174 }
1175 // Update outgoing_transitions_count_per_label_state;
1176 typename state_label_to_size_t_map::iterator it=outgoing_transitions_count_per_label_state.find(std::pair(t.label(),t.from()));
1177 if (it==outgoing_transitions_count_per_label_state.end())
1178 {
1179 outgoing_transitions_count_per_label_state[std::pair(t.label(),t.from())](*m_transitions[*j].trans_count)-1;
1180 }
1181 else
1182 {
1183 *it--;
1184 }
1185 // Update m_state_to_constellation_count.
1186 if (m_states[t.to()].block==index_block_B)
1187 {
1188 const std::size_t new_position=m_state_to_constellation_count.size();
1189 const std::size_t found_position=
1190 newly_created_state_to_constellation_count_entry.try_emplace(
1191 std::pair(t.from(),t.label()),
1192 new_position)->second;
1193 if (new_position==found_position)
1194 {
1195 m_state_to_constellation_count.push_back(1);
1196 (m_transitions[*j].trans_count)--;
1197 m_transitions[*j].trans_count=m_state_to_constellation_count.end()-1;
1198 }
1199 }
1200 // Update the label_to_transition map.
1201 if (label_to_transition.find(std::pair(t.from(), t.label()))==label_to_transition.end())
1202 {
1203 // Not found. Add a transition from the L_B_C_list to label_to_transition
1204 // that goes to C\B, or the null_transition if no such transition exists, which prevents searching
1205 // the list again.
1206 // First look backwards.
1207 L_B_C_list_iterator transition_walker(*j, m_transitions);
1208
1209 bool found=false;
1210
1211 while (!found && i*transition_walker!=null_transition)
1212 {
1213 transition& tw=m_aut.get_transitions()[transition_walker];
1214 if (m_states[tw.to()].block==ci)
1215 {
1216 found=true;
1217 }
1218 else
1219 {
1220 ++transition_walker;
1221 }
1222 }
1223 label_to_transition[t.label()]=transition_walker;
1224 }
1225 // Update the doubly linked list L_B->C in blocks as the constellation is split in B and C\B.
1227 }
1228 }
1229
1230 // Algorithm 1, line 1.10.
1231 for(const auto& [a, M]: calM)
1232 {
1233 // Algorithm 1, line 1.11.
1234 states_per_block_type Mleft_map;
1235 for(const state_index si: M)
1236 {
1237 Mleft_map[m_states[si].block].insert(si);
1238 }
1239 for(const auto& [bi, Mleft]: Mleft_map)
1240 {
1241 assert(!Mleft.empty());
1242 // Check whether the bottom states of bi are not all included in Mleft.
1243 bool bottom_states_all_included=true;
1244 for(typename std::vector<state_index>::iterator state_it=m_blocks[bi].start_bottom_states;
1245 state_it!=m_blocks[bi].start_non_bottom_states;
1246 state_it++)
1247 {
1248 if (Mleft.count(*state_it)==0)
1249 {
1250 bottom_states_all_included=false;
1251 break; // leave the for loop.
1252 }
1253 }
1254 if (!bottom_states_all_included)
1255 {
1256 // Algorithm 1, line 1.12.
1257 bool M_in_bi1=true;
1258 block_index bi1=splitB(bi, Mleft.begin(),
1259 Mleft.end(),
1260 [](const state_index ){ return false; },
1261 m_blocks[bi].start_bottom_states,
1262 m_blocks[bi].start_non_bottom_states,
1263 [&](const state_index si){ return Mleft.count(si)>0; },
1264 M_in_bi1);
1265 // Algorithm 1, line 1.13.
1266 block_index Bpp=(M_in_bi1, bi1, bi);
1267 // Algorithm 1, line 1.14 is implicitly done in the call of splitB above.
1268 // Algorithm 1, line 1.15.
1269 bool size_U_larger_than_zero=false;
1270 bool size_U_smaller_than_Bpp_bottom=false;
1271 for(state_index si=m_states[Bpp].bottom_states;
1272 !(size_U_larger_than_zero && size_U_smaller_than_Bpp_bottom) &&
1273 si!=m_states[Bpp].non_bottom_states;
1274 ++si)
1275 {
1276 if (outgoing_transitions_count_per_label_state[std::pair(a,si)]>0)
1277 {
1278 size_U_larger_than_zero=true;
1279 }
1280 else
1281 {
1282 size_U_larger_than_zero=true;
1283 }
1284 }
1285 // Algorithm 1, line 1.16.
1286 if (size_U_larger_than_zero && size_U_smaller_than_Bpp_bottom)
1287 {
1288 // Algorithm 1, line 1.17.
1289 transition_index co_t=label_to_transition[a];
1290
1291 bool dummy=false;
1294 [](const state_index ){ return false; },
1295 m_states[Bpp].bottom_states,
1296 m_states[Bpp].non_bottom_states,
1297 [&](const state_index si){ outgoing_transitions_count_per_label_state.count(std::pair(a,si))>0; },
1298 dummy);
1299 // Algorithm 1, line 1.18 and 1.19. P is updated implicitly when splitting Bpp.
1300
1301 }
1302
1303 }
1304 }
1305 }
1306 stabilizeB();
1307 }
1308 }
1309
1310};
1311
1312
1313
1314
1315/* ************************************************************************* */
1316/* */
1317/* I N T E R F A C E */
1318/* */
1319/* ************************************************************************* */
1320
1321
1322
1323
1324
1329
1330
1340template <class LTS_TYPE>
1341void bisimulation_reduce_gj(LTS_TYPE& l, const bool branching = false,
1342 const bool preserve_divergence = false)
1343{
1344 if (1 >= l.num_states())
1345 {
1346 mCRL2log(log::warning) << "There is only 1 state in the LTS. It is not "
1347 "guaranteed that branching bisimulation minimisation runs in "
1348 "time O(m log n).\n";
1349 }
1350 // Line 2.1: Find tau-SCCs and contract each of them to a single state
1351 if (branching)
1352 {
1353 scc_reduce(l, preserve_divergence);
1354 }
1355
1356 // Now apply the branching bisimulation reduction algorithm. If there
1357 // are no taus, this will automatically yield strong bisimulation.
1358 bisim_partitioner_gj<LTS_TYPE> bisim_part(l, branching,
1359 preserve_divergence);
1360
1361 // Assign the reduced LTS
1362 bisim_part.finalize_minimized_LTS();
1363}
1364
1365
1385template <class LTS_TYPE>
1386bool destructive_bisimulation_compare_gj(LTS_TYPE& l1, LTS_TYPE& l2,
1387 const bool branching = false, const bool preserve_divergence = false,
1388 const bool generate_counter_examples = false,
1389 const std::string& /*counter_example_file*/ = "", bool /*structured_output*/ = false)
1390{
1391 if (generate_counter_examples)
1392 {
1393 mCRL2log(log::warning) << "The JGKW20 branching bisimulation "
1394 "algorithm does not generate counterexamples.\n";
1395 }
1396 std::size_t init_l2(l2.initial_state() + l1.num_states());
1397 detail::merge(l1, std::move(l2));
1398 l2.clear(); // No use for l2 anymore.
1399
1400 // Line 2.1: Find tau-SCCs and contract each of them to a single state
1401 if (branching)
1402 {
1404 scc_part.replace_transition_system(preserve_divergence);
1405 init_l2 = scc_part.get_eq_class(init_l2);
1406 } else assert(!preserve_divergence);
1407 assert(1 < l1.num_states());
1408 bisim_partitioner_gj<LTS_TYPE> bisim_part(l1, branching,
1409 preserve_divergence);
1410
1411 return bisim_part.in_same_class(l1.initial_state(), init_l2);
1412}
1413
1414
1431template <class LTS_TYPE>
1432inline bool bisimulation_compare_gj(const LTS_TYPE& l1, const LTS_TYPE& l2,
1433 const bool branching = false, const bool preserve_divergence = false)
1434{
1435 LTS_TYPE l1_copy(l1);
1436 LTS_TYPE l2_copy(l2);
1437 return destructive_bisimulation_compare_gj(l1_copy, l2_copy, branching,
1438 preserve_divergence);
1439}
1440
1441
1442} // end namespace detail
1443} // end namespace lts
1444} // end namespace mcrl2
1445
1446#endif // ifndef LIBLTS_BISIM_GJ_H
const_iterator end() const
implements the main algorithm for the branching bisimulation quotient
void finalize_minimized_LTS()
Adapt the LTS after minimisation.
LTS_TYPE & m_aut
automaton that is being reduced
std::size_t number_of_states_in_block(const block_index B) const
std::unordered_set< state_index > set_of_states_type
std::vector< constellation_type > m_constellations
void check_transitions_that_became_non_inert_in_a_block_by_co_block(const block_index, const block_index)
void check_transitions_that_became_non_inert_in_a_block(const block_index bi)
std::deque< std::size_t > m_state_to_constellation_count
void insert_in_the_doubly_linked_list_L_B_C_in_blocks(const transition &t, const transition_index ti, std::forward_list< transition_index > ::iterator position)
block_index splitB(const block_index B, const MARKED_STATE_ITERATOR M_begin, const MARKED_STATE_ITERATOR M_end, const std::function< bool(state_index)> &marked_blocker, const UNMARKED_STATE_ITERATOR M_co_begin, const UNMARKED_STATE_ITERATOR M_co_end, const std::function< bool(state_index)> &unmarked_blocker, bool &M_in_new_block)
std::vector< transition_type > m_transitions
std::unordered_map< label_index, set_of_states_type > states_per_action_label_type
state_type_gj num_eq_classes() const
Calculate the number of equivalence classes.
void swap_states_in_states_in_block(block_index pos1, block_index pos2, block_index pos3)
void update_the_doubly_linked_list_L_B_C_new_block(const block_index old_bi, const block_index new_bi, const transition &t, const transition_index ti, std::unordered_set< std::pair< action_index, constellation_index >, std::forward_list< transition_index >::iterator > &new_LBC_list_entries)
set_of_constellations_type m_non_trivial_constellations
The following variable contains all non trivial constellations.
std::vector< std::reference_wrapper< transition_type > > m_outgoing_transitions
std::vector< std::reference_wrapper< transition_type > > m_incoming_transitions
std::vector< state_type_gj > m_states
state_type_gj get_eq_class(const state_type_gj s) const
Get the equivalence class of a state.
bool remove_from_the_doubly_linked_list_L_B_C_in_blocks(const transition_index ti)
block_index simple_splitB(const block_index B, const MARKED_STATE_ITERATOR M_begin, const MARKED_STATE_ITERATOR M_end, const std::function< bool(state_index)> &marked_blocker, const UNMARKED_STATE_ITERATOR M_co_begin, const UNMARKED_STATE_ITERATOR M_co_end, const std::function< bool(state_index)> &unmarked_blocker, bool &M_in_bi)
void update_the_doubly_linked_list_L_B_C_same_block(const block_index index_block_B, const transition &t, const transition_index ti)
block_index split_block_B_into_R_and_BminR(const block_index B, const std::unordered_set< state_index > &R)
const bool m_branching
true iff branching (not strong) bisimulation has been requested
std::unordered_map< std::pair< state_index, label_index >, std::size_t > state_label_to_size_t_map
std::unordered_map< label_index, std::size_t > label_to_size_t_map
const bool m_preserve_divergence
true iff divergence-preserving branching bisimulation has been requested
std::unordered_set< constellation_index > set_of_constellations_type
std::vector< state_index > m_states_in_blocks
std::unordered_map< block_index, set_of_states_type > states_per_block_type
bisim_partitioner_gj(LTS_TYPE &aut, const bool branching=false, const bool preserve_divergence=false)
constructor
bool in_same_class(state_index const s, state_index const t) const
Check whether two states are in the same equivalence class.
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
A class containing triples, source label and target representing transitions.
Definition transition.h:43
size_type from() const
The source of the transition.
Definition transition.h:77
size_type label() const
The label of the transition.
Definition transition.h:83
size_type to() const
The target of the transition.
Definition transition.h:90
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
@ warning
Definition logger.h:32
@ verbose
Definition logger.h:35
constexpr transition_index null_transition
bool bisimulation_compare_gj(const LTS_TYPE &l1, const LTS_TYPE &l2, const bool branching=false, const bool preserve_divergence=false)
Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bis...
bool destructive_bisimulation_compare_gj(LTS_TYPE &l1, LTS_TYPE &l2, const bool branching=false, const bool preserve_divergence=false, const bool generate_counter_examples=false, const std::string &="", bool=false)
Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bis...
void bisimulation_reduce_gj(LTS_TYPE &l, const bool branching=false, const bool preserve_divergence=false)
Reduce transition system l with respect to strong or (divergence-preserving) branching bisimulation.
std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator &i)
From state of an iterator exploring transitions per outgoing state and action.
void scc_reduce(LTS_TYPE &l, const bool preserve_divergence_loops=false)
Definition liblts_scc.h:362
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
bool operator==(const L_B_C_list_iterator &it) const
const std::vector< transition_type > & m_transitions
L_B_C_list_iterator(const transition_index ti, const std::vector< transition_type > &transitions)
std::forward_list< transition_index > block_to_constellation
block_type(const std::vector< state_index >::iterator beginning_of_states, constellation_index c)
std::vector< state_index >::iterator start_non_bottom_states
std::vector< state_index >::iterator start_bottom_states
constellation_type(const block_index start, const block_index end)
std::vector< state_index >::iterator ref_states_in_blocks
std::vector< transition_index >::iterator start_outgoing_inert_transitions
std::vector< transition_index >::iterator start_outgoing_non_inert_transitions
std::vector< transition_index >::iterator start_incoming_transitions
std::forward_list< transition_index >::const_iterator transitions_per_block_to_constellation
std::vector< std::size_t >::iterator trans_count