mCRL2
Loading...
Searching...
No Matches
liblts_bisim_dnj.h
Go to the documentation of this file.
1// Author(s): David N. Jansen, Institute of Software, Chinese Academy of
2// Sciences, Beijing, PR China
3//
4// Copyright: see the accompanying file COPYING or copy at
5// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
6//
7// Distributed under the Boost Software License, Version 1.0.
8// (See accompanying file LICENSE_1_0.txt or copy at
9// http://www.boost.org/LICENSE_1_0.txt)
10
76
77// The file is best viewed on a screen or in a window that is 160 characters
78// wide. The left 80 columns contain the main text of the program. The right
79// 80 columns contain assertions and other code used for debugging.
80
81#ifndef LIBLTS_BISIM_DNJ_H
82#define LIBLTS_BISIM_DNJ_H
83
84#include "mcrl2/lts/detail/liblts_scc.h"
85#include "mcrl2/lts/detail/liblts_merge.h"
86#include "mcrl2/lts/detail/coroutine.h"
87#include "mcrl2/lts/detail/check_complexity.h"
88#include "mcrl2/lts/detail/fixed_vector.h"
89#include "mcrl2/lts/detail/simple_list.h"
90
91#include <cstddef> // for std::size_t
92
93namespace mcrl2
94{
95namespace lts
96{
97namespace detail
98{
99 #ifndef NDEBUG
105// state_type and trans_type are defined in check_complexity.h. /// mode and to nothing otherwise.
106 #define ONLY_IF_DEBUG(...) __VA_ARGS__
107 #else
108 #define ONLY_IF_DEBUG(...)
109 #endif
113typedef std::size_t label_type;
114
115template <class LTS_TYPE> class bisim_partitioner_dnj;
116
117namespace bisim_dnj
118{
119
131template <class Iterator>
132union iterator_or_counter
133{
135 trans_type count;
136
138 Iterator begin;
139
141 iterator_or_counter() { count = 0; }
142
143
145 void convert_to_iterator(const Iterator other)
146 {
147 new (&begin) Iterator(other);
148 }
149
150
152 ~iterator_or_counter() { begin.~Iterator(); }
153};
154
155
156class block_bunch_entry;
157class action_block_entry;
158
159
160
161
162
163/* ************************************************************************* */
164/* */
165/* R E F I N A B L E P A R T I T I O N */
166/* */
167/* ************************************************************************* */
168
169
170
171
172
181class state_info_entry;
182class permutation_entry;
183
192typedef fixed_vector<permutation_entry> permutation_t;
193
194class block_t;
195class bunch_t;
196
197class pred_entry;
198class succ_entry;
199
200class block_bunch_slice_t;
201typedef simple_list<block_bunch_slice_t>::iterator block_bunch_slice_iter_t;
202typedef simple_list<block_bunch_slice_t>::const_iterator
203 block_bunch_slice_const_iter_t;
204typedef iterator_or_null_t<block_bunch_slice_t>
205 block_bunch_slice_iter_or_null_t;
206
207enum new_block_mode_t { new_block_is_U, new_block_is_R };
208
209
215class state_info_entry
216{
217 public:
225 iterator_or_counter<pred_entry*> pred_inert;
226
234 iterator_or_counter<succ_entry*> succ_inert;
235
242 union bl_t {
243 pred_entry* ed_noninert_end;
244 block_t* ock;
245 } bl;
246
248 permutation_entry* pos;
249
264 iterator_or_counter<succ_entry*> untested_to_U_eqv;
265 #ifndef NDEBUG
267 template<class LTS_TYPE>
268 std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
269 partitioner) const
270 { assert(&partitioner.part_st.state_info.front() <= this);
271 assert(this <= &partitioner.part_st.state_info.back());
272 return std::to_string(this - &partitioner.part_st.state_info.front());
273 }
274
276 template<class LTS_TYPE>
277 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>&
278 partitioner) const
279 {
280 return "state " + debug_id_short(partitioner);
281 }
282
283 mutable check_complexity::state_dnj_counter_t work_counter;
284 #endif
285};
286
287
289class permutation_entry {
290 public:
292 state_info_entry* st;
293
294
296 permutation_entry() = default;
297
298
302 permutation_entry(const permutation_entry&& other) noexcept
303 {
304 st = other.st;
305 }
306
307
313 void operator=(const permutation_entry&& other) noexcept
314 {
315 st = other.st;
316 st->pos = this;
317 }
318};
319
320
344class block_t
345{
346 public:
348 permutation_entry* begin;
349
351 permutation_entry* marked_bottom_begin;
352
354 permutation_entry* nonbottom_begin;
355
357 permutation_entry* marked_nonbottom_begin;
358
360 permutation_entry* end;
361
364 simple_list<block_bunch_slice_t> stable_block_bunch;
365
369 const state_type seqnr;
370
371
378 block_t(permutation_entry* const new_begin,
379 permutation_entry* const new_end, state_type const new_seqnr)
380 : begin(new_begin),
381 marked_bottom_begin(new_end),
382 nonbottom_begin(new_end),
383 marked_nonbottom_begin(new_end),
384 end(new_end),
385 stable_block_bunch(),
386 seqnr(new_seqnr)
387 { assert(new_begin < new_end);
388 }
389
390
392 state_type size() const
393 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
394 assert(marked_bottom_begin <= nonbottom_begin);
395 assert(nonbottom_begin <= marked_nonbottom_begin);
396 return end - begin;
397 }
398
399
401 state_type bottom_size() const
402 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
403 assert(marked_bottom_begin <= nonbottom_begin);
404 assert(nonbottom_begin <= marked_nonbottom_begin);
405 return nonbottom_begin - begin;
406 }
407
408
410 state_type marked_bottom_size() const
411 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
412 assert(marked_bottom_begin <= nonbottom_begin);
413 assert(nonbottom_begin <= marked_nonbottom_begin);
414 return nonbottom_begin - marked_bottom_begin;
415 }
416
417
419 state_type marked_size() const
420 {
421 return end - marked_nonbottom_begin + marked_bottom_size();
422 }
423
424
426 state_type unmarked_bottom_size() const
427 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
428 assert(marked_bottom_begin <= nonbottom_begin);
429 assert(nonbottom_begin <= marked_nonbottom_begin);
430 return marked_bottom_begin - begin;
431 }
432
433
435 state_type unmarked_nonbottom_size() const
436 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
437 assert(marked_bottom_begin <= nonbottom_begin);
438 assert(nonbottom_begin <= marked_nonbottom_begin);
439 return marked_nonbottom_begin - nonbottom_begin;
440 }
441
442
448 bool mark_nonbottom(permutation_entry* const s)
449 { assert(nonbottom_begin <= s); assert(s < end);
450 // assert(this == s->st->bl.ock); -- does not hold during initialisation
451 assert(begin <= marked_bottom_begin);
452 assert(marked_bottom_begin <= nonbottom_begin);
453 assert(nonbottom_begin <= marked_nonbottom_begin);
454 if (marked_nonbottom_begin <= s) { return false; } assert(marked_nonbottom_begin <= end);
455 std::swap(*s, *--marked_nonbottom_begin); assert(nonbottom_begin <= marked_nonbottom_begin);
456 return true;
457 }
458
459
465 bool mark(permutation_entry* const s)
466 { assert(begin <= s);
467 if (s < nonbottom_begin) // assert(this == s->st->bl.ock); -- does not hold during initialisation
468 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
469 assert(nonbottom_begin <= marked_nonbottom_begin);
470 if (marked_bottom_begin <= s) { return false; } assert(marked_bottom_begin <= nonbottom_begin);
471 std::swap(*s, *--marked_bottom_begin); assert(begin <= marked_bottom_begin);
472 return true;
473 }
474 return mark_nonbottom(s);
475 }
476
477
489 ONLY_IF_DEBUG( template<class LTS_TYPE> )
490 block_t* split_off_block(enum new_block_mode_t new_block_mode, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
491 ONLY_IF_POOL_ALLOCATOR(
492 my_pool<simple_list<block_bunch_slice_t>::entry>& storage, )
493 state_type new_seqnr);
494 #ifndef NDEBUG
496 template<class LTS_TYPE>
497 inline std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>&
498 partitioner) const
499 { assert(&partitioner.part_st.permutation.front() <= begin);
500 assert(begin < end); assert(begin <= marked_bottom_begin);
501 assert(marked_bottom_begin <= nonbottom_begin);
502 assert(nonbottom_begin <= marked_nonbottom_begin);
503 assert(marked_nonbottom_begin <= end);
504 assert(end <= 1 + &partitioner.part_st.permutation.back());
505 return "block [" +
506 std::to_string(begin - &partitioner.part_st.permutation.front()) +
507 "," + std::to_string(end-&partitioner.part_st.permutation.front()) +
508 ") (#" + std::to_string(seqnr) + ")";
509 }
510
511 mutable check_complexity::block_dnj_counter_t work_counter;
512 #endif
513};
514
515
520class part_state_t
521{
522 public:
527 permutation_t permutation;
528
530 fixed_vector<state_info_entry> state_info;
531
535 state_type nr_of_blocks;
536
543 part_state_t(state_type const num_states)
544 : permutation(num_states),
545 state_info(num_states),
546 nr_of_blocks(0)
547 { assert(0 < num_states);
548 permutation_entry* perm_iter(&permutation.front()); ONLY_IF_POOL_ALLOCATOR(
549 static_assert(std::is_trivially_destructible<block_t>::value); )
550 state_info_entry* state_iter(&state_info.front()); assert(perm_iter <= &permutation.back());
551 do
552 {
553 state_iter->pos = perm_iter;
554 perm_iter->st = state_iter;
555 }
556 while (++state_iter, ++perm_iter <= &permutation.back()); assert(state_iter == 1 + &state_info.back());
557 }
558
559
560 #ifndef USE_POOL_ALLOCATOR
566 ~part_state_t()
567 { ONLY_IF_DEBUG( state_type deleted_blocks(0); )
568 permutation_entry* perm_iter(1 + &permutation.back()); assert(&permutation.front() < perm_iter);
569 do
570 {
571 block_t* const B(perm_iter[-1].st->bl.ock); assert(B->end == perm_iter);
572 perm_iter = B->begin; ONLY_IF_DEBUG( ++deleted_blocks; )
573 delete B;
574 }
575 while (&permutation.front() < perm_iter); assert(deleted_blocks == nr_of_blocks);
576 }
577 #endif
578
579
582 state_type state_size() const { return permutation.size(); }
583
584
588 const block_t* block(state_type const s) const
589 {
590 return state_info[s].bl.ock;
591 }
592 #ifndef NDEBUG
593 private:
601 template<class LTS_TYPE>
602 void print_block(const block_t* const B,
603 const char* const message,
604 const permutation_entry* begin_print,
605 const permutation_entry* const end_print,
606 const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
607 { assert(B->begin <= begin_print); assert(end_print <= B->end);
608 if (end_print == begin_print) return;
609
610 mCRL2log(log::debug) << '\t' << message
611 << (1 < end_print - begin_print ? "s:\n" : ":\n");
612 assert(begin_print < end_print);
613 do
614 {
615 mCRL2log(log::debug) << "\t\t"
616 << begin_print->st->debug_id(partitioner);
617 if (B != begin_print->st->bl.ock)
618 {
619 mCRL2log(log::debug) << ", inconsistent: points "
620 "to " << begin_print->st->bl.ock->debug_id(partitioner);
621 }
622 if (begin_print != begin_print->st->pos)
623 {
624 mCRL2log(log::debug)
625 << ", inconsistent pointer to state_info_entry";
626 }
627 mCRL2log(log::debug) << '\n';
628 }
629 while (++begin_print < end_print);
630 }
631 public:
636 template<class LTS_TYPE>
637 void print_part(const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
638 {
639 if (!mCRL2logEnabled(log::debug)) return;
640 const block_t* B(permutation.front().st->bl.ock);
641 do
642 {
643 mCRL2log(log::debug)<<B->debug_id(partitioner)<<":\n";
644 print_block(B, "Bottom state",
645 B->begin, B->marked_bottom_begin, partitioner);
646 print_block(B, "Marked bottom state",
647 B->marked_bottom_begin, B->nonbottom_begin, partitioner);
648 print_block(B, "Non-bottom state",
649 B->nonbottom_begin, B->marked_nonbottom_begin, partitioner);
650 print_block(B, "Marked non-bottom state",
651 B->marked_nonbottom_begin, B->end, partitioner);
652 // go to next block
653 }
654 while(B->end <= &permutation.back() && (B = B->end->st->bl.ock, true));
655 }
656
660 template<class LTS_TYPE>
661 void assert_consistency(
662 const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
663 {
664 const permutation_entry* perm_iter(&permutation.front());
665 state_type true_nr_of_blocks(0);
666 assert(perm_iter <= &permutation.back());
667 do
668 {
669 const block_t* const block(perm_iter->st->bl.ock);
670 // block is consistent:
671 assert(block->begin == perm_iter);
672 assert(block->begin < block->marked_bottom_begin);
673 assert(block->marked_bottom_begin == block->nonbottom_begin);
674 assert(block->nonbottom_begin <= block->marked_nonbottom_begin);
675 assert(block->marked_nonbottom_begin == block->end);
676 assert(partitioner.branching||block->nonbottom_begin==block->end);
677 assert(0 <= block->seqnr);
678 assert(block->seqnr < nr_of_blocks);
679 unsigned const max_block(check_complexity::log_n -
680 check_complexity::ilog2(block->size()));
681 mCRL2complexity(block, no_temporary_work(max_block), partitioner);
682
683 // states in the block are consistent:
684 do
685 {
686 const state_info_entry* const state(perm_iter->st);
687 // assert(&part_tr.pred.front() < state->pred_inert.begin);
688 assert(&state_info.back() == state ||
689 state->pred_inert.begin <= state[1].pred_inert.begin);
690 // assert(state->pred_inert.begin <= &part_tr.pred.back());
691 // assert(state->succ_inert.begin <= &part_tr.succ.back());
692 if (perm_iter < block->nonbottom_begin)
693 {
694 assert(&state_info.back() == state || state->
695 succ_inert.begin <= state[1].succ_inert.begin);
696 // assert(state->succ_inert.begin==&part_tr.succ.back() ||
697 // state <
698 // state->succ_inert.begin->block_bunch->pred->source);
699 mCRL2complexity(state, no_temporary_work(max_block, true),
700 partitioner);
701 }
702 else
703 {
704 // assert(state->succ_inert.begin < &part_tr.succ.back());
705 assert(&state_info.back() == state || state->
706 succ_inert.begin < state[1].succ_inert.begin);
707 //assert(state ==
708 // state->succ_inert.begin->block_bunch->pred->source);
709 mCRL2complexity(state, no_temporary_work(max_block, false),
710 partitioner);
711 }
712 assert(block == state->bl.ock);
713 assert(perm_iter == state->pos);
714 }
715 while (++perm_iter < block->end);
716 assert(perm_iter == block->end);
717 ++true_nr_of_blocks;
718 }
719 while (perm_iter <= &permutation.back());
720 assert(nr_of_blocks == true_nr_of_blocks);
721 }
722 #endif
723};
724
726
727
728
729
730 #ifndef NDEBUG
731/* ************************************************************************* */ static struct {
732/* */ bool operator()(const iterator_or_counter<action_block_entry*> p1,
733/* T R A N S I T I O N S */ const action_block_entry* const action_block) const
734/* */ {
735/* ************************************************************************* */ return p1.begin > action_block;
736 }
737 } const action_label_greater;
738 #endif
739
740
774
776
778class succ_entry
779{
780 public:
782 block_bunch_entry* block_bunch;
783
792 succ_entry* begin_or_before_end;
793
794
796 succ_entry* out_slice_begin( ONLY_IF_DEBUG( const fixed_vector<succ_entry>& succ )
797 );
798
799
801 bunch_t* bunch() const;
802 #ifndef NDEBUG
814 template <class LTS_TYPE>
815 static inline void add_work_to_out_slice(
816 const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
817 const succ_entry* out_slice_begin,
818 enum check_complexity::counter_type ctr, unsigned max_value);
819 #endif
820};
821
822
825class block_bunch_entry
826{
827 public:
829 pred_entry* pred;
830
833 block_bunch_slice_iter_or_null_t slice;
834};
835
836
842class pred_entry
843{
844 public:
846 action_block_entry* action_block;
847
849 state_info_entry* source;
850
852 state_info_entry* target;
853 #ifndef NDEBUG
855 template <class LTS_TYPE>
856 std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
857 partitioner) const
858 {
859 return "from " + source->debug_id_short(partitioner) +
860 " to " + target->debug_id_short(partitioner);
861 }
862
864 template <class LTS_TYPE>
865 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
866 const
867 {
868 // Search for the action label in partitioner.action_label
869 label_type const label(std::lower_bound(
870 partitioner.action_label.cbegin(), partitioner.action_label.cend(),
871 action_block, action_label_greater) -
872 partitioner.action_label.cbegin());
873 assert(label < partitioner.action_label.size());
874 assert(partitioner.action_label[label].begin <= action_block);
875 assert(0==label||action_block<partitioner.action_label[label-1].begin);
876 // class lts_lts_t uses a function pp() to transform the action label
877 // to a string.
878 return pp(partitioner.aut.action_label(label)) + "-transition " +
879 debug_id_short(partitioner);
880 }
881
882 mutable check_complexity::trans_dnj_counter_t work_counter;
883 #endif
884};
885
886
889class action_block_entry
890{
891 public:
897 succ_entry* succ;
898
908 action_block_entry* begin_or_before_end;
909
910
912 action_block_entry* action_block_slice_begin( ONLY_IF_DEBUG( const action_block_entry* const action_block_begin,
913 const action_block_entry* const action_block_orig_inert_begin )
914 )
915 {
916 action_block_entry* result(begin_or_before_end); assert(nullptr != result);
917 if (this < result)
918 { assert(this == result->begin_or_before_end);
919 result = this; // The following assertion does not always hold: the function is called
920 } // immediately after a block is refined, so it may be the case that the
921 // transitions are still to be moved to different slices.
922 // assert(succ->block_bunch->pred->target->bl.ock ==
923 // result->succ->block_bunch->pred->target->bl.ock);
924 assert(nullptr != succ); assert(nullptr != result->succ);
925 assert(succ->bunch() == result->succ->bunch());
926 assert(result == action_block_begin || nullptr == result[-1].succ ||
927 action_block_orig_inert_begin <= result ||
928 result[-1].succ->block_bunch->pred->target->bl.ock !=
929 result->succ->block_bunch->pred->target->bl.ock);
930 // assert(this has the same action as result);
931 return result;
932 }
933};
934
935
936class part_trans_t;
937
942class bunch_t
943{
944 public:
946 action_block_entry* begin;
947
949 action_block_entry* end;
950
955 union next_nontrivial_and_label_t
956 {
962 bunch_t* next_nontrivial;
963
965 label_type label;
966
967
969 next_nontrivial_and_label_t()
970 {
971 next_nontrivial = nullptr;
972 }
973 } next_nontrivial_and_label;
974
975
977 bunch_t(action_block_entry* const new_begin,
978 action_block_entry* const new_end)
979 : begin(new_begin),
980 end(new_end),
981 next_nontrivial_and_label()
982 { }
983
984
989 bool is_trivial() const
990 {
991 return nullptr == next_nontrivial_and_label.next_nontrivial;
992 }
993
994
1001 bunch_t* split_off_small_action_block_slice(part_trans_t& part_tr);
1002 #ifndef NDEBUG
1004 template <class LTS_TYPE>
1005 std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
1006 partitioner) const
1007 {
1008 assert(partitioner.part_tr.action_block_begin <= begin);
1009 assert(end <= partitioner.part_tr.action_block_inert_begin);
1010 return "bunch [" + std::to_string(begin -
1011 partitioner.part_tr.action_block_begin) + "," +
1012 std::to_string(end - partitioner.part_tr.action_block_begin) + ")";
1013 }
1014
1016 template <class LTS_TYPE>
1017 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1018 const
1019 { assert(nullptr != end[-1].succ);
1020 const action_block_entry* iter(begin); assert(iter < end);
1021 assert(nullptr != iter->succ);
1022 assert(iter == iter->succ->block_bunch->pred->action_block);
1023 std::string result(debug_id_short(partitioner));
1024 result += " containing transition";
1025 result += iter < end - 1 ? "s " : " ";
1026 result += iter->succ->block_bunch->pred->debug_id_short(partitioner);
1027 ++iter;
1028 if (end <= iter) return result;
1029 while (nullptr == iter->succ) ++iter;
1030 assert(iter < end);
1031 assert(iter == iter->succ->block_bunch->pred->action_block);
1032 result += ", ";
1033 result += iter->succ->block_bunch->pred->debug_id_short(partitioner);
1034 if (iter < end - 3)
1035 {
1036 result += ", ...";
1037 iter = end - 3;
1038 }
1039 while (++iter < end)
1040 {
1041 if (nullptr != iter->succ)
1042 { assert(iter == iter->succ->block_bunch->pred->action_block);
1043 result += ", ";
1044 result += iter->succ->block_bunch->pred->debug_id_short(
1045 partitioner);
1046 }
1047 }
1048 return result;
1049 }
1050
1056 template <class LTS_TYPE>
1057 int max_work_counter(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1058 const
1059 {
1060 // verify that the bunch only has a single action label.
1061 // Search for the action label in partitioner.action_label
1062 label_type const label(std::lower_bound(
1063 partitioner.action_label.cbegin(), partitioner.action_label.cend(),
1064 begin, action_label_greater) -
1065 partitioner.action_label.cbegin());
1066 assert(label < partitioner.action_label.size());
1067 assert(partitioner.action_label[label].begin <= begin);
1068 assert(0 == label || begin < partitioner.action_label[label-1].begin);
1069 if (0 == label || end < partitioner.action_label[label - 1].begin)
1070 {
1071 assert(check_complexity::ilog2(end - begin) <=
1072 check_complexity::log_n);
1073 return check_complexity::log_n-check_complexity::ilog2(end-begin);
1074 }
1075 return 0;
1076 }
1077
1078 mutable check_complexity::bunch_dnj_counter_t work_counter;
1079 #endif
1080};
1081
1082
1099class block_bunch_slice_t
1100{
1101 public:
1105 block_bunch_entry* end;
1106
1108 bunch_t* bunch;
1109
1113 block_bunch_entry* marked_begin;
1114
1115
1117 bool is_stable() const { return nullptr == marked_begin; }
1118
1119
1121 void make_stable()
1122 { assert(!is_stable()); assert(!empty());
1123 marked_begin = nullptr;
1124 }
1125
1126
1128 void make_unstable()
1129 { assert(is_stable());
1130 marked_begin = end; assert(!is_stable());
1131 }
1132
1133
1135 block_bunch_slice_t(block_bunch_entry* const new_end,
1136 bunch_t* const new_bunch, bool const new_is_stable)
1137 : end(new_end),
1138 bunch(new_bunch),
1139 marked_begin(nullptr)
1140 {
1141 if (!new_is_stable) make_unstable();
1142 }
1143
1144
1148 bool empty() const
1149 { // assert(std::less(&part_tr.block_bunch.front(), end));
1150 // assert(!std::less(part_tr.block_bunch_inert_begin, end));
1151 // assert(part_tr.block_bunch.front().slice != this);
1152 return end[-1].slice != this;
1153 }
1154
1155
1157 block_t* source_block() const
1158 { assert(!empty());
1159 return end[-1].pred->source->bl.ock;
1160 }
1161 #ifndef NDEBUG
1163 template <class LTS_TYPE>
1164 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1165 const
1166 {
1167 static struct {
1168 bool operator()(const block_bunch_entry& p1,
1169 const block_bunch_slice_t* const p2) const
1170 {
1171 return p1.slice != p2;
1172 }
1173 } const block_bunch_not_equal;
1174
1175 assert(&partitioner.part_tr.block_bunch.front() < end);
1176 assert(end <= partitioner.part_tr.block_bunch_inert_begin);
1177 std::string const index_string(std::to_string(end -
1178 &partitioner.part_tr.block_bunch.cbegin()[1]));
1179 if (empty())
1180 { //assert(!is_stable());
1181 return "empty block_bunch_slice [" + index_string + "," +
1182 index_string + ")";
1183 }
1184 const block_bunch_entry* begin(
1185 &partitioner.part_tr.block_bunch.cbegin()[1]);
1186 if (trans_type bunch_size(bunch->end - bunch->begin);
1187 (trans_type) (end - begin) > bunch_size)
1188 {
1189 begin = end - bunch_size;
1190 }
1191 begin = std::lower_bound(begin, const_cast<const block_bunch_entry*>
1192 (is_stable() || marked_begin==end ? end-1 : marked_begin),
1193 this, block_bunch_not_equal);
1194 assert(begin->slice == this);
1195 assert(begin[-1].slice != this);
1196 return (is_stable() ? "stable block_bunch-slice ["
1197 : "unstable block_bunch_slice [") +
1198 std::to_string(begin-&partitioner.part_tr.block_bunch.cbegin()[1]) +
1199 "," + index_string + ") containing transitions from " +
1200 source_block()->debug_id(partitioner) +
1201 " in " + bunch->debug_id_short(partitioner);
1202 }
1203
1211 template <class LTS_TYPE>
1212 bool add_work_to_bottom_transns(enum check_complexity::
1213 counter_type const ctr, unsigned const max_value,
1214 const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
1215 { assert(!empty());
1216 assert(1U == max_value);
1217 const block_t* const block(source_block());
1218 bool result(false);
1219 const block_bunch_entry* block_bunch(end);
1220 assert(partitioner.part_tr.block_bunch.front().slice != this);
1221 assert(block_bunch[-1].slice == this);
1222 do
1223 {
1224 --block_bunch;
1225 const state_info_entry* const source(block_bunch->pred->source);
1226 assert(source->bl.ock == block);
1227 if (source->pos < block->nonbottom_begin /*&&
1228 // the transition starts in a (new) bottom state
1229 block_bunch->pred->work_counter.counters[ctr -
1230 check_complexity::TRANS_dnj_MIN] != max_value*/)
1231 {
1232 mCRL2complexity(block_bunch->pred, add_work(ctr, max_value),
1233 partitioner);
1234 result = true;
1235 }
1236 }
1237 while (block_bunch[-1].slice == this);
1238 return result;
1239 }
1240
1241 mutable check_complexity::block_bunch_dnj_counter_t work_counter;
1242 #endif
1243};
1244
1245
1247inline succ_entry* succ_entry::out_slice_begin( ONLY_IF_DEBUG( const fixed_vector<succ_entry>& succ )
1248 )
1249{ assert(nullptr != begin_or_before_end);
1250 succ_entry* result(begin_or_before_end); assert(result->block_bunch->pred->action_block->succ == result);
1251 if (this < result)
1252 { assert(nullptr != result->begin_or_before_end);
1253 assert(this == result->begin_or_before_end);
1254 result = this; assert(result->block_bunch->pred->action_block->succ == result);
1255 } assert(block_bunch->pred->source == result->block_bunch->pred->source);
1256 // assert(this <= result); //< holds always, based on the if() above
1257 assert(nullptr != result->begin_or_before_end);
1258 assert(this <= result->begin_or_before_end);
1259 assert(block_bunch->slice == result->block_bunch->slice);
1260 assert(&succ.cbegin()[1] == result ||
1261 result[-1].block_bunch->pred->source < block_bunch->pred->source ||
1262 result[-1].bunch() != block_bunch->slice->bunch);
1263 return result;
1264}
1265
1266
1268inline bunch_t* succ_entry::bunch() const
1269{
1270 return block_bunch->slice->bunch;
1271}
1272 #ifndef NDEBUG
1281 template <class LTS_TYPE>
1282 /* static */ inline void succ_entry::add_work_to_out_slice(
1283 const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
1284 const succ_entry* out_slice_begin,
1285 enum check_complexity::counter_type const ctr,unsigned const max_value)
1286 {
1287 const succ_entry* const out_slice_before_end(
1288 out_slice_begin->begin_or_before_end);
1289 assert(nullptr != out_slice_before_end);
1290 assert(out_slice_begin <= out_slice_before_end);
1291 mCRL2complexity(out_slice_begin->block_bunch->pred,
1292 add_work(ctr, max_value), partitioner);
1293 while (++out_slice_begin <= out_slice_before_end)
1294 {
1295 // treat temporary counters specially
1296 mCRL2complexity(out_slice_begin->block_bunch->pred,
1297 add_work_notemporary(ctr, max_value), partitioner);
1298 }
1299 }
1300 #endif
1301class part_trans_t
1302{
1303 public:
1308 fixed_vector<succ_entry> succ;
1309
1314 fixed_vector<block_bunch_entry> block_bunch;
1315
1320 fixed_vector<pred_entry> pred;
1321
1333 action_block_entry* const action_block_begin;
1334 action_block_entry* const action_block_end;
1335
1337 block_bunch_entry* block_bunch_inert_begin;
1338
1340 action_block_entry* action_block_inert_begin;
1341 #ifndef NDEBUG
1343 const action_block_entry* action_block_orig_inert_begin;
1344 #endif
1346 simple_list<block_bunch_slice_t> splitter_list;
1347 private:
1349 bunch_t* first_nontrivial;
1350
1351 public:
1352 #ifdef USE_POOL_ALLOCATOR
1353 static_assert(std::is_trivially_destructible<bunch_t>::value);
1354 static_assert(std::is_trivially_destructible<
1355 simple_list<block_bunch_slice_t>::entry>::value);
1357 my_pool<simple_list<block_bunch_slice_t>::entry> storage;
1358 #endif
1359
1361 state_type nr_of_new_bottom_states;
1362
1364 trans_type nr_of_bunches;
1365 trans_type nr_of_nontrivial_bunches;
1366 trans_type nr_of_action_block_slices;
1367 trans_type nr_of_block_bunch_slices;
1368
1377 part_trans_t(trans_type num_transitions,
1378 trans_type num_actions)
1379 : succ(num_transitions + 2),
1380 block_bunch(num_transitions + 1),
1381 pred(num_transitions + 2),
1382 action_block_begin(
1383 new action_block_entry[num_transitions + num_actions - 1]),
1384 action_block_end(action_block_begin + (num_transitions+num_actions-1)),
1385 block_bunch_inert_begin(1 + &block_bunch.back()),
1386 action_block_inert_begin(action_block_end),
1387 splitter_list(),
1388 first_nontrivial(nullptr),
1389 nr_of_new_bottom_states(0),
1390 nr_of_bunches(0),
1391 nr_of_nontrivial_bunches(0),
1392 nr_of_action_block_slices(0),
1393 nr_of_block_bunch_slices(0)
1394 {
1395 succ.front().block_bunch = &block_bunch.front();
1396 succ.back() .block_bunch = &block_bunch.front();
1397 block_bunch.front().pred = &pred.front();
1398 block_bunch.front().slice = nullptr;
1399 pred.front().source = nullptr;
1400 pred.front().target = nullptr;
1401 pred.back() .source = nullptr;
1402 pred.back() .target = nullptr;
1403 }
1404
1405
1407 ~part_trans_t()
1408 {
1409 #ifndef USE_POOL_ALLOCATOR
1410 // The destructor also deallocates the bunches, as they are not
1411 // directly referenced from anywhere. This is only necessary if we
1412 // do not use the pool allocator, as the latter will destroy the
1413 // bunches wholesale.
1414 action_block_entry* action_block_iter(action_block_begin);
1415 for (;;)
1416 {
1417 do
1418 {
1419 if (action_block_inert_begin <= action_block_iter)
1420 { assert(0 == nr_of_bunches);
1421 delete [] action_block_begin;
1422 return;
1423 }
1424 }
1425 while (nullptr == action_block_iter->succ && ( assert(nullptr == action_block_iter->begin_or_before_end),
1426 ++action_block_iter, true)); assert(nullptr != action_block_iter->begin_or_before_end);
1427 bunch_t* const bunch(action_block_iter->succ->bunch()); assert(bunch->begin == action_block_iter);
1428 action_block_iter = bunch->end;
1429 delete bunch; ONLY_IF_DEBUG( --nr_of_bunches; )
1430 }
1431 /* unreachable */ assert(0);
1432 #else
1433 delete [] action_block_begin;
1434 #endif
1435 }
1436
1437
1440 bunch_t* get_some_nontrivial()
1441 {
1442 return first_nontrivial;
1443 }
1444
1445
1448 void make_nontrivial(bunch_t* const bunch)
1449 { assert(1 < bunch->end - bunch->begin); assert(bunch->is_trivial());
1450 // The following assertions do not necessarily hold during initialisation:
1451 //assert(bunch->begin <= bunch->begin->begin_or_before_end);
1452 bunch->next_nontrivial_and_label.next_nontrivial =
1453 nullptr == first_nontrivial ? bunch : first_nontrivial; //assert(nullptr != bunch->begin->begin_or_before_end);
1454 //assert(nullptr != bunch->end[-1].begin_or_before_end);
1455 //assert(bunch->begin->begin_or_before_end <
1456 // bunch->end[-1].begin_or_before_end);
1457 //assert(nullptr != end[-1].begin_or_before_end);
1458 first_nontrivial = bunch; assert(nr_of_nontrivial_bunches < nr_of_bunches);
1459 ++nr_of_nontrivial_bunches; //assert(end[-1].begin_or_before_end <= end);
1460 }
1461
1462
1465 void make_trivial(bunch_t* const bunch)
1466 { assert(!bunch->is_trivial()); assert(first_nontrivial == bunch);
1467 first_nontrivial =
1468 bunch == bunch->next_nontrivial_and_label.next_nontrivial
1469 ? nullptr : bunch->next_nontrivial_and_label.next_nontrivial; assert(bunch->end - 1 == bunch->begin->begin_or_before_end);
1470 bunch->next_nontrivial_and_label.next_nontrivial = nullptr; assert(0 < nr_of_nontrivial_bunches);
1471 --nr_of_nontrivial_bunches; assert(bunch->begin == bunch->end[-1].begin_or_before_end);
1472 }
1473
1474
1497 void first_move_transition_to_new_bunch(
1498 action_block_entry* const action_block_iter,
1499 bunch_t* const bunch_T_a_Bprime,
1500 bool const first_transition_of_state)
1501 {
1502
1503 /* - - - - - - - - adapt part_tr.succ - - - - - - - - */
1504
1505 succ_entry* const old_succ_pos(action_block_iter->succ); assert(nullptr != old_succ_pos);
1506 assert(old_succ_pos->block_bunch->pred->action_block == action_block_iter);
1507 succ_entry* const out_slice_begin(old_succ_pos->out_slice_begin( ONLY_IF_DEBUG( succ )
1508 )); assert(out_slice_begin->block_bunch->pred->action_block->succ ==
1509 out_slice_begin);
1510 succ_entry* const new_succ_pos(out_slice_begin->begin_or_before_end); assert(nullptr != new_succ_pos);
1511 assert(out_slice_begin == new_succ_pos->begin_or_before_end);
1512 assert(new_succ_pos<old_succ_pos->block_bunch->pred->source->succ_inert.begin);
1513 /* move the transition to the end of its out-slice */ assert(new_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
1514 if (old_succ_pos < new_succ_pos)
1515 {
1516 std::swap(old_succ_pos->block_bunch, new_succ_pos->block_bunch);
1517 old_succ_pos->block_bunch->pred->action_block->succ = old_succ_pos; assert(action_block_iter == new_succ_pos->block_bunch->pred->action_block);
1518 action_block_iter->succ = new_succ_pos;
1519 } else assert(old_succ_pos == new_succ_pos);
1520
1521 // adapt the old out-slice immediately
1522 // If the old out-slice becomes empty, then out_slice_begin ==
1523 // new_succ_pos, so the two following assignments will assign the
1524 // same variable. The second assignment is the relevant one.
1525 out_slice_begin->begin_or_before_end = new_succ_pos - 1;
1526
1527 // adapt the new out-slice, as far as is possible now:
1528 // make the begin_or_before_end pointers of the first and last
1529 // transition in the slice correct immediately. The other
1530 // begin_or_before_end pointers need to be corrected after all
1531 // transitions in the new bunch have been positioned correctly.
1532 if (first_transition_of_state)
1533 {
1534 new_succ_pos->begin_or_before_end = new_succ_pos;
1535 }
1536 else
1537 {
1538 succ_entry* const out_slice_before_end(
1539 new_succ_pos[1].begin_or_before_end); assert(nullptr != out_slice_before_end);
1540 assert(new_succ_pos < out_slice_before_end);
1541 assert(out_slice_before_end->block_bunch->pred->action_block->succ ==
1542 out_slice_before_end);
1543 assert(new_succ_pos + 1 == out_slice_before_end->begin_or_before_end);
1544 out_slice_before_end->begin_or_before_end = new_succ_pos; assert(out_slice_before_end <
1545 new_succ_pos->block_bunch->pred->source->succ_inert.begin);
1546 new_succ_pos->begin_or_before_end = out_slice_before_end; assert(bunch_T_a_Bprime == out_slice_before_end->bunch());
1547 }
1548
1549 /* - - - - - - - adapt part_tr.block_bunch - - - - - - - */ assert(new_succ_pos == action_block_iter->succ);
1550
1551 block_bunch_entry* const old_block_bunch_pos(
1552 new_succ_pos->block_bunch); assert(old_block_bunch_pos->pred->action_block == action_block_iter);
1553 block_t*const source_block = old_block_bunch_pos->pred->source->bl.ock; assert(!old_block_bunch_pos->slice.is_null());
1554 block_bunch_slice_iter_t const old_block_bunch_slice(
1555 old_block_bunch_pos->slice);
1556 block_bunch_entry* const new_block_bunch_pos(
1557 old_block_bunch_slice->end - 1); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
1558 assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
1559 new_block_bunch_pos);
1560 // create or adapt the new block_bunch-slice
1561 block_bunch_slice_iter_t new_block_bunch_slice;
1562 if (new_block_bunch_pos + 1 >= block_bunch_inert_begin ||
1563 (new_block_bunch_slice = (block_bunch_slice_iter_t)
1564 new_block_bunch_pos[1].slice, assert(!new_block_bunch_pos[1].slice.is_null()),
1565 bunch_T_a_Bprime != new_block_bunch_slice->bunch ||
1566 source_block != new_block_bunch_slice->source_block()))
1567 { assert(first_transition_of_state);
1568 // This is the first transition in the block_bunch-slice.
1569 // The old block_bunch-slice becomes unstable, and the new
1570 // block_bunch-slice is created unstable.
1571
1572 // Note that the new block_bunch-slice should precede the old one.
1573
1574 #ifdef USE_SIMPLE_LIST
1575 new_block_bunch_slice = splitter_list.emplace_back(
1576 ONLY_IF_POOL_ALLOCATOR( storage, )
1577 new_block_bunch_pos + 1, bunch_T_a_Bprime, false);
1578 #else
1579 splitter_list.emplace_back(new_block_bunch_pos + 1,
1580 bunch_T_a_Bprime, false);
1581 new_block_bunch_slice = std::prev(splitter_list.end());
1582 #endif
1583 ++nr_of_block_bunch_slices; ONLY_IF_DEBUG( new_block_bunch_slice->work_counter =
1584 old_block_bunch_slice->work_counter; )
1585 splitter_list.splice(splitter_list.end(),
1586 source_block->stable_block_bunch, old_block_bunch_slice);
1587 old_block_bunch_slice->make_unstable();
1588 } assert(!new_block_bunch_slice->is_stable());
1589
1590 // move the transition to the end of its block_bunch-slice
1591 if (old_block_bunch_pos < new_block_bunch_pos)
1592 {
1593 std::swap(old_block_bunch_pos->pred, new_block_bunch_pos->pred); assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
1594 old_block_bunch_pos->pred->action_block->succ->block_bunch =
1595 old_block_bunch_pos; assert(new_succ_pos == new_block_bunch_pos->pred->action_block->succ);
1596 new_succ_pos->block_bunch = new_block_bunch_pos;
1597 } else assert(new_block_bunch_pos == old_block_bunch_pos);
1598 assert(new_block_bunch_pos->slice == old_block_bunch_slice);
1599 new_block_bunch_pos->slice = new_block_bunch_slice;
1600
1601 /* adapt the old block_bunch-slice */ assert(new_block_bunch_pos + 1 == old_block_bunch_slice->marked_begin);
1602 old_block_bunch_slice->end = new_block_bunch_pos;
1603 old_block_bunch_slice->marked_begin = new_block_bunch_pos; assert(nullptr != new_block_bunch_pos);
1604 if (old_block_bunch_slice->empty())
1605 { assert(!old_block_bunch_slice->is_stable());
1606 splitter_list.erase( ONLY_IF_POOL_ALLOCATOR( storage, )
1607 old_block_bunch_slice); assert(!new_block_bunch_slice->is_stable());
1608 --nr_of_block_bunch_slices;
1609
1610 // Because now every bottom state has a transition in the new
1611 // bunch, and no state has a transition in the old bunch, there
1612 // is no need to refine this block. So we make this
1613 // block_bunch-slice stable again.
1614 source_block->stable_block_bunch.splice(
1615 source_block->stable_block_bunch.end(),
1616 splitter_list, new_block_bunch_slice);
1617 new_block_bunch_slice->make_stable();
1618
1619 // unmark the states
1620 // (This transition must be the last transition from
1621 // source_block in the new bunch, so unmarking the states now
1622 // will not be undone by later markings of other states.)
1623 source_block->marked_nonbottom_begin = source_block->end; assert(source_block->marked_bottom_begin == source_block->begin);
1624 source_block->marked_bottom_begin = source_block->nonbottom_begin;
1625 }
1626 }
1627
1628
1649 ONLY_IF_DEBUG( template <class LTS_TYPE> )
1650 void second_move_transition_to_new_bunch(
1651 action_block_entry* const action_block_iter, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
1652 bunch_t* const bunch_T_a_Bprime, )
1653 bunch_t* const large_splitter_bunch)
1654 { assert(nullptr != bunch_T_a_Bprime);
1655
1656 /* - - - - - - - - adapt part_tr.succ - - - - - - - - */
1657
1658 // We already moved the transition in part_tr.succ to the correct
1659 // place in first_move_transition_to_new_bunch(); now we have to
1660 // set begin_or_before_end.
1661 succ_entry* const new_succ_pos(action_block_iter->succ); assert(nullptr != new_succ_pos);
1662 assert(new_succ_pos->block_bunch->pred->action_block == action_block_iter);
1663 state_info_entry* const source(
1664 new_succ_pos->block_bunch->pred->source); assert(source->pos->st == source);
1665 assert(new_succ_pos < source->succ_inert.begin);
1666 assert(source == &partitioner.part_st.state_info.front() ||
1667 source[-1].succ_inert.begin <= new_succ_pos);
1668 assert(nullptr != new_succ_pos->begin_or_before_end);
1669 succ_entry* const new_begin_or_before_end(
1670 new_succ_pos->begin_or_before_end->begin_or_before_end); assert(nullptr != new_begin_or_before_end);
1671 assert(new_begin_or_before_end->block_bunch->pred->action_block->succ ==
1672 new_begin_or_before_end);
1673 if (new_begin_or_before_end < new_succ_pos)
1674 { assert(source == &partitioner.part_st.state_info.front() ||
1675 source[-1].succ_inert.begin <= new_begin_or_before_end);
1676 new_succ_pos->begin_or_before_end = new_begin_or_before_end;
1677 }
1678 else
1679 { assert(new_begin_or_before_end == new_succ_pos);
1680 // This is the first or the last transition in the out-slice.
1681 const succ_entry* const new_before_end(
1682 new_begin_or_before_end->begin_or_before_end); assert(nullptr != new_before_end);
1683 if (new_begin_or_before_end <= new_before_end)
1684 { assert(&partitioner.part_tr.succ.cbegin()[1] == new_begin_or_before_end ||
1685 /* This is the first transition in the new out-slice. */ new_begin_or_before_end[-1].block_bunch->pred->source < source ||
1686 /* If there is still a transition in the old out-slice, */ new_begin_or_before_end[-1].bunch() != bunch_T_a_Bprime);
1687 /* we prepay for it. */ assert(new_before_end + 1 == source->succ_inert.begin ||
1688 bunch_T_a_Bprime != new_before_end[1].bunch());
1689 if (source == new_succ_pos[-1].block_bunch->pred->source &&
1690 new_succ_pos[-1].bunch() == large_splitter_bunch)
1691 {
1692 // Mark one transition in the large slice
1693 block_bunch_entry* const old_block_bunch_pos(
1694 new_succ_pos[-1].block_bunch); assert(!old_block_bunch_pos->slice.is_null());
1695 assert(old_block_bunch_pos->pred->action_block->succ == new_succ_pos - 1);
1696 block_bunch_slice_iter_t const large_splitter_slice(
1697 old_block_bunch_pos->slice);
1698 if (!large_splitter_slice->is_stable())
1699 {
1700 block_bunch_entry* const new_block_bunch_pos(
1701 large_splitter_slice->marked_begin - 1); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
1702 assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
1703 new_block_bunch_pos);
1704 if (old_block_bunch_pos < new_block_bunch_pos)
1705 {
1706 std::swap(old_block_bunch_pos->pred,
1707 new_block_bunch_pos->pred); // assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
1708 old_block_bunch_pos->pred->action_block->
1709 succ->block_bunch = old_block_bunch_pos; assert(new_block_bunch_pos->pred->action_block->succ == new_succ_pos - 1);
1710 new_succ_pos[-1].block_bunch = new_block_bunch_pos;
1711 }
1712 large_splitter_slice->marked_begin=new_block_bunch_pos; assert(nullptr != new_block_bunch_pos);
1713 } else assert(1 >= source->bl.ock->size());
1714 }
1715 } else assert(source == &partitioner.part_st.state_info.front() ||
1716 source[-1].succ_inert.begin <= new_before_end);
1717 }
1718 #ifndef NDEBUG
1719 /* - - - - - - - adapt part_tr.block_bunch - - - - - - - */ const block_bunch_entry* new_block_bunch_pos(new_succ_pos->block_bunch);
1720 assert(new_block_bunch_pos->pred->action_block->succ == new_succ_pos);
1721 assert(!new_block_bunch_pos->slice.is_null());
1722 /* Nothing needs to be done. */ block_bunch_slice_const_iter_t const new_block_bunch_slice(
1723 new_block_bunch_pos->slice);
1724 assert(new_block_bunch_pos < new_block_bunch_slice->end);
1725 assert(bunch_T_a_Bprime == new_block_bunch_slice->bunch);
1726 if (new_block_bunch_pos + 1 < new_block_bunch_slice->end) return;
1727
1728 // This transition is the last in the block_bunch-slice. If there
1729 // were some task that would need to be done exactly once per
1730 // block_bunch-slice, this would be the moment.
1731 do assert(source->bl.ock == new_block_bunch_pos->pred->source->bl.ock);
1732 while ((--new_block_bunch_pos)->slice == new_block_bunch_slice);
1733 assert(new_block_bunch_pos <= &partitioner.part_tr.block_bunch.front() ||
1734 source->bl.ock != new_block_bunch_pos->pred->source->bl.ock ||
1735 bunch_T_a_Bprime != new_block_bunch_pos->slice->bunch);
1736 #endif
1737 }
1738
1739
1740 private:
1768 ONLY_IF_DEBUG( template <class LTS_TYPE> )
1769 succ_entry* move_out_slice_to_new_block(
1770 succ_entry* out_slice_end, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
1771 #ifndef USE_SIMPLE_LIST
1772 block_t* const old_block,
1773 #endif
1774 block_bunch_slice_const_iter_t const splitter_T)
1775 { assert(&succ.cbegin()[1] < out_slice_end);
1776 succ_entry* const out_slice_begin(
1777 out_slice_end[-1].begin_or_before_end); assert(nullptr != out_slice_begin);
1778 assert(out_slice_begin < out_slice_end);
1779 assert(out_slice_begin->block_bunch->pred->action_block->succ ==
1780 out_slice_begin);
1781 block_bunch_entry* old_block_bunch_pos(out_slice_end[-1].block_bunch); assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
1782 assert(!old_block_bunch_pos->slice.is_null());
1783 block_bunch_slice_iter_t const old_block_bunch_slice(
1784 old_block_bunch_pos->slice); assert(old_block_bunch_pos->pred->action_block->succ->block_bunch ==
1785 old_block_bunch_pos);
1786 if (&*splitter_T == &*old_block_bunch_slice) return out_slice_begin;
1787
1788 block_bunch_entry* old_block_bunch_slice_end(
1789 old_block_bunch_slice->end);
1790 state_info_entry* const source(old_block_bunch_pos->pred->source); assert(out_slice_end <= source->succ_inert.begin);
1791 assert(&partitioner.part_st.state_info.front() == source ||
1792 source[-1].succ_inert.begin < out_slice_end);
1793 block_t* const new_block(source->bl.ock); assert(source == out_slice_begin->block_bunch->pred->source);
1794 block_bunch_slice_iter_t new_block_bunch_slice; assert(source->pos->st == source);
1795 if (old_block_bunch_slice_end >= block_bunch_inert_begin ||
1796 new_block != old_block_bunch_slice_end->pred->source->bl.ock ||
1797 (new_block_bunch_slice = (block_bunch_slice_iter_t)
1798 old_block_bunch_slice_end->slice, assert(!old_block_bunch_slice_end->slice.is_null()),
1799 old_block_bunch_slice->bunch != new_block_bunch_slice->bunch))
1800 {
1801 // the new block_bunch-slice is not suitable; create a new one and
1802 // insert it into the correct list.
1803 if (old_block_bunch_slice->is_stable())
1804 {
1805 // In most cases, but not always, the source is a bottom state.
1806 #ifdef USE_SIMPLE_LIST
1807 new_block_bunch_slice =
1808 new_block->stable_block_bunch.emplace_front(
1809 ONLY_IF_POOL_ALLOCATOR( storage, )
1810 old_block_bunch_slice->end,
1811 old_block_bunch_slice->bunch, true);
1812 #else
1813 new_block->stable_block_bunch.emplace_front(
1814 old_block_bunch_slice->end,
1815 old_block_bunch_slice->bunch, true);
1816 new_block_bunch_slice =
1817 new_block->stable_block_bunch.begin();
1818 #endif
1819 }
1820 else
1821 {
1822 #ifdef USE_SIMPLE_LIST
1823 new_block_bunch_slice = splitter_list.emplace_after(
1824 ONLY_IF_POOL_ALLOCATOR( storage, )
1825 old_block_bunch_slice,
1826 old_block_bunch_slice->end,
1827 old_block_bunch_slice->bunch, false);
1828 #else
1829 new_block_bunch_slice = splitter_list.emplace(
1830 std::next(old_block_bunch_slice),
1831 old_block_bunch_slice->end,
1832 old_block_bunch_slice->bunch, false);
1833 #endif
1834 }
1835 ++nr_of_block_bunch_slices; ONLY_IF_DEBUG( new_block_bunch_slice->work_counter =
1836 old_block_bunch_slice->work_counter; )
1837 }
1838 ONLY_IF_DEBUG( unsigned max_counter = check_complexity::log_n -
1839 check_complexity::ilog2(new_block->size()); )
1840 /* move all transitions in this out-slice to the new block_bunch */ assert(out_slice_begin < out_slice_end);
1841 do
1842 { assert(old_block_bunch_pos == out_slice_end[-1].block_bunch);
1843 --out_slice_end; assert(old_block_bunch_pos->slice == old_block_bunch_slice);
1844 assert(source == out_slice_end->block_bunch->pred->source);
1845 --old_block_bunch_slice_end; // assign work already now because the transition may be moved to several
1846 // places:
1847 old_block_bunch_slice_end->slice = new_block_bunch_slice; mCRL2complexity(old_block_bunch_pos->pred, add_work(
1848 check_complexity::move_out_slice_to_new_block, max_counter), partitioner);
1849 if (old_block_bunch_slice->is_stable() || ( assert(!new_block_bunch_slice->is_stable()),
1850 old_block_bunch_slice->marked_begin >
1851 old_block_bunch_slice_end &&
1852 (/* As the old block_bunch-slice has no marked */ assert(nullptr != old_block_bunch_slice_end),
1853 // transitions, it is enough to adapt its marked_begin
1854 // and then do a simple (two-way) swap.
1855 old_block_bunch_slice->marked_begin =
1856 old_block_bunch_slice_end, true)))
1857 {
1858 // The old block_bunch-slice is stable, or it has no
1859 // marked transitions.
1860 std::swap(old_block_bunch_pos->pred,
1861 old_block_bunch_slice_end->pred);
1862 }
1863 else
1864 {
1865 // The old block_bunch-slice is unstable and has marked
1866 // transitions.
1867 pred_entry* const old_pred = old_block_bunch_pos->pred;
1868 if (old_block_bunch_pos < old_block_bunch_slice->marked_begin)
1869 {
1870 // The transition is not marked, but there are other
1871 // marked transitions in the old block_bunch-slice.
1872 // Move the transition to the non-marked part of the
1873 // new block_bunch-slice.
1874 block_bunch_entry* const old_marked_begin =
1875 old_block_bunch_slice->marked_begin - 1; assert(old_block_bunch_pos < old_block_bunch_slice_end);
1876 old_block_bunch_slice->marked_begin = old_marked_begin;
1877
1878 old_block_bunch_pos->pred = old_marked_begin->pred;
1879 old_marked_begin->pred = old_block_bunch_slice_end->pred;
1880 old_block_bunch_slice_end->pred = old_pred; assert(nullptr != old_marked_begin->pred->action_block->succ);
1881
1882 old_marked_begin->pred->action_block->succ->
1883 block_bunch = old_marked_begin;
1884 }
1885 else
1886 {
1887 // The transition is marked. Move to the marked part
1888 // of the new block_bunch-slice.
1889 block_bunch_entry* const new_marked_begin =
1890 new_block_bunch_slice->marked_begin - 1;
1891 new_block_bunch_slice->marked_begin = new_marked_begin; assert(old_block_bunch_pos < new_marked_begin ||
1892 old_block_bunch_pos == old_block_bunch_slice_end);
1893 old_block_bunch_pos->pred=old_block_bunch_slice_end->pred; assert(old_block_bunch_slice_end <= new_marked_begin);
1894 old_block_bunch_slice_end->pred = new_marked_begin->pred;
1895 new_marked_begin->pred = old_pred; assert(out_slice_end == new_marked_begin->pred->action_block->succ);
1896
1897 out_slice_end->block_bunch = new_marked_begin;
1898 }
1899 } assert(nullptr != old_block_bunch_slice_end->pred->action_block->succ);
1900 old_block_bunch_slice_end->pred->action_block->succ->block_bunch =
1901 old_block_bunch_slice_end; assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
1902 old_block_bunch_pos->pred->action_block->succ->block_bunch =
1903 old_block_bunch_pos;
1904 }
1905 while (out_slice_begin < out_slice_end &&
1906 (old_block_bunch_pos = out_slice_end[-1].block_bunch, true));
1907 old_block_bunch_slice->end = old_block_bunch_slice_end;
1908
1909 if (old_block_bunch_slice->empty())
1910 {
1911 #ifdef USE_SIMPLE_LIST
1912 simple_list<block_bunch_slice_t>::erase(
1913 ONLY_IF_POOL_ALLOCATOR( storage, )
1914 old_block_bunch_slice);
1915 #else
1916 if (old_block_bunch_slice->is_stable())
1917 {
1918 // If the new block is R, then the old (U) block loses
1919 // exactly one stable block_bunch-slice, namely the one we
1920 // just stabilised for (`splitter_T`). We could perhaps
1921 // optimize this by moving that slice as a whole to the new
1922 // block -- perhaps later.
1923 //
1924 // If the new block is U, then the old (R) block loses
1925 // no stable block_bunch-slices if it contains any bottom
1926 // state. If it doesn't contain any bottom state, it will
1927 // definitely keep `splitter_T`, but nothing else can be
1928 // guaranteed.
1929 //
1930 // So old_block_bunch_slice may be deleted, in particular
1931 // if the new block is U, but not exclusively.
1932 old_block->stable_block_bunch.erase(old_block_bunch_slice);
1933 }
1934 else
1935 {
1936 splitter_list.erase(old_block_bunch_slice);
1937 }
1938 #endif
1939 --nr_of_block_bunch_slices;
1940 }
1941 return out_slice_begin;
1942 }
1943
1944
1954 void first_move_transition_to_new_action_block(pred_entry* const pred_iter)
1955 {
1956 action_block_entry* const old_action_block_pos(
1957 pred_iter->action_block); assert(nullptr != old_action_block_pos->succ);
1958 assert(old_action_block_pos->succ->block_bunch->pred == pred_iter);
1959 action_block_entry* const action_block_slice_begin(
1960 old_action_block_pos->action_block_slice_begin( ONLY_IF_DEBUG( action_block_begin, action_block_orig_inert_begin )
1961 )); assert(nullptr != action_block_slice_begin->succ);
1962 assert(action_block_slice_begin->succ->block_bunch->pred->action_block ==
1963 action_block_slice_begin);
1964 action_block_entry* const new_action_block_pos(
1965 action_block_slice_begin->begin_or_before_end); assert(nullptr != new_action_block_pos);
1966 assert(action_block_slice_begin == new_action_block_pos->begin_or_before_end);
1967 assert(nullptr != new_action_block_pos->succ);
1968 assert(new_action_block_pos->succ->block_bunch->pred->action_block ==
1969 /* move the transition to the end of the action_block-slice */ new_action_block_pos);
1970 if (old_action_block_pos < new_action_block_pos)
1971 {
1972 succ_entry* const temp(new_action_block_pos->succ); assert(nullptr != temp); assert(nullptr != old_action_block_pos->succ);
1973 new_action_block_pos->succ = old_action_block_pos->succ;
1974 old_action_block_pos->succ = temp;
1975 temp->block_bunch->pred->action_block = old_action_block_pos; assert(pred_iter == new_action_block_pos->succ->block_bunch->pred);
1976 pred_iter->action_block = new_action_block_pos;
1977
1978 // adapt the old action_block-slice immediately
1979 action_block_slice_begin->begin_or_before_end =
1980 new_action_block_pos - 1;
1981 }
1982 else
1983 { assert(old_action_block_pos == new_action_block_pos);
1984 if (action_block_slice_begin < new_action_block_pos)
1985 {
1986 // The old action_block-slice is not empty, so we have to adapt
1987 // the pointer at the beginning. (If it is empty, it may
1988 // happen that `new_action_block_pos - 1` is an illegal value.)
1989 action_block_slice_begin->begin_or_before_end =
1990 new_action_block_pos - 1;
1991 }
1992 else --nr_of_action_block_slices;
1993 } assert(nullptr != new_action_block_pos->succ);
1994 assert(pred_iter == new_action_block_pos->succ->block_bunch->pred);
1995 // adapt the new action_block-slice, as far as is possible now
1996 // make the begin_or_before_end pointers of the first and last
1997 // transition in the slice correct immediately. The other
1998 // begin_or_before_end pointers need to be corrected after all
1999 // transitions in the new bunch have been positioned correctly.
2000 if (new_action_block_pos + 1 >= action_block_inert_begin ||
2001 nullptr == new_action_block_pos[1].succ ||
2002 new_action_block_pos[1].succ->bunch() !=
2003 new_action_block_pos->succ->bunch() ||
2004 new_action_block_pos[1].succ->block_bunch->pred->target->bl.ock !=
2005 pred_iter->target->bl.ock)
2006 {
2007 // This is the first transition that moves to this new
2008 // action_block-slice.
2009 new_action_block_pos->begin_or_before_end = new_action_block_pos;
2010 ++nr_of_action_block_slices;
2011 }
2012 else
2013 {
2014 action_block_entry* const action_block_slice_before_end(
2015 new_action_block_pos[1].begin_or_before_end); assert(nullptr != action_block_slice_before_end);
2016 assert(new_action_block_pos < action_block_slice_before_end);
2017 assert(nullptr != action_block_slice_before_end->succ);
2018 assert(action_block_slice_before_end->succ->block_bunch->pred->action_block ==
2019 action_block_slice_before_end);
2020 assert(new_action_block_pos + 1 ==
2021 action_block_slice_before_end->begin_or_before_end);
2022 action_block_slice_before_end->begin_or_before_end =
2023 new_action_block_pos; assert(action_block_slice_before_end->succ->block_bunch->
2024 pred->target->bl.ock == pred_iter->target->bl.ock);
2025 new_action_block_pos->begin_or_before_end =
2026 action_block_slice_before_end; assert(action_block_slice_before_end < action_block_inert_begin);
2027 }
2028 }
2029
2030
2037 void second_move_transition_to_new_action_block(
2038 pred_entry* const pred_iter)
2039 {
2040 action_block_entry* const new_action_block_pos(
2041 pred_iter->action_block); assert(nullptr != new_action_block_pos->succ);
2042 assert(new_action_block_pos->succ->block_bunch->pred == pred_iter);
2043 action_block_entry* const old_begin_or_before_end(
2044 new_action_block_pos->begin_or_before_end); assert(nullptr != old_begin_or_before_end);
2045 assert(nullptr != old_begin_or_before_end->succ);
2046 assert(old_begin_or_before_end->succ->block_bunch->pred->action_block ==
2047 old_begin_or_before_end);
2048 if (action_block_entry* const new_begin_or_before_end(
2049 old_begin_or_before_end->begin_or_before_end); assert(nullptr != new_begin_or_before_end),
2050 assert(nullptr != new_begin_or_before_end->succ),
2051 assert(new_begin_or_before_end->succ->block_bunch->pred->action_block ==
2052 new_begin_or_before_end),
2053 new_begin_or_before_end < new_action_block_pos)
2054 { assert(old_begin_or_before_end==new_begin_or_before_end->begin_or_before_end);
2055 new_action_block_pos->begin_or_before_end =
2056 new_begin_or_before_end; assert(new_action_block_pos <= old_begin_or_before_end);
2057 return;
2058 } else assert(new_begin_or_before_end == new_action_block_pos);
2059 if (old_begin_or_before_end < new_action_block_pos) return;
2060
2061 // this is the first transition in the new action_block-slice.
2062 // Check whether the bunch it belongs to has become nontrivial.
2063 bunch_t* const bunch(new_action_block_pos->succ->bunch());
2064 if (!bunch->is_trivial()) { return; } assert(old_begin_or_before_end + 1 == bunch->end);
2065 if (bunch->begin < new_action_block_pos)
2066 {
2067 make_nontrivial(bunch);
2068 }
2069 }
2070
2071
2096 bool make_noninert(pred_entry* const old_pred_pos,
2097 block_bunch_slice_iter_or_null_t* const new_noninert_block_bunch_ptr)
2098 {
2099 state_info_entry* const source(old_pred_pos->source); assert(source->pos->st == source);
2100 state_info_entry* const target(old_pred_pos->target); assert(target->pos->st == target);
2101
2102 action_block_entry* const new_action_block_pos(
2103 action_block_inert_begin++); assert(nullptr != new_action_block_pos->succ);
2104 assert(new_action_block_pos->succ->block_bunch->pred->action_block ==
2105 new_action_block_pos);
2106 succ_entry* const new_succ_pos(source->succ_inert.begin++); assert(new_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
2107 block_bunch_entry* const new_block_bunch_pos(
2108 block_bunch_inert_begin++); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
2109 assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
2110 new_block_bunch_pos);
2111 action_block_entry* const old_action_block_pos(
2112 old_pred_pos->action_block); assert(new_action_block_pos <= old_action_block_pos);
2113
2114 succ_entry* const old_succ_pos(old_action_block_pos->succ); assert(nullptr != old_succ_pos);
2115 block_bunch_entry* const old_block_bunch_pos(
2116 old_succ_pos->block_bunch); assert(old_pred_pos == old_block_bunch_pos->pred);
2117 pred_entry* const new_pred_pos(target->pred_inert.begin++); assert(nullptr != new_pred_pos->action_block->succ);
2118 assert(new_pred_pos->action_block->succ->block_bunch->pred == new_pred_pos);
2119
2120 /* adapt action_block */ assert(nullptr == new_action_block_pos->begin_or_before_end);
2121 if (new_action_block_pos < old_action_block_pos)
2122 { assert(nullptr == old_action_block_pos->begin_or_before_end);
2123 old_action_block_pos->succ = new_action_block_pos->succ; assert(nullptr != old_action_block_pos->succ);
2124 assert(old_action_block_pos->succ->block_bunch->pred->action_block ==
2125 new_action_block_pos);
2126 old_action_block_pos->succ->block_bunch->pred->action_block =
2127 old_action_block_pos;
2128 } else assert(new_action_block_pos == old_action_block_pos);
2129 new_action_block_pos->succ = new_succ_pos; assert(nullptr != new_succ_pos);
2130 // new_action_block_pos->begin_or_before_end = ...; -- see below
2131
2132 /* adapt succ */ assert(nullptr == new_succ_pos->begin_or_before_end);
2133 if (new_succ_pos < old_succ_pos)
2134 { assert(nullptr == old_succ_pos->begin_or_before_end);
2135 old_succ_pos->block_bunch = new_succ_pos->block_bunch; assert(old_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
2136 old_succ_pos->block_bunch->pred->action_block->succ = old_succ_pos; assert(nullptr != old_succ_pos);
2137 } else assert(new_succ_pos == old_succ_pos);
2138 new_succ_pos->block_bunch = new_block_bunch_pos;
2139 // new_succ_pos->begin_or_before_end = ...; -- see below
2140
2141 /* adapt block_bunch */ assert(new_block_bunch_pos->slice.is_null());
2142 if (new_block_bunch_pos < old_block_bunch_pos)
2143 { assert(old_block_bunch_pos->slice.is_null());
2144 assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2145 old_block_bunch_pos->pred = new_block_bunch_pos->pred; assert(old_block_bunch_pos->pred->action_block->succ->block_bunch ==
2146 new_block_bunch_pos);
2147 assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2148 old_block_bunch_pos->pred->action_block->succ->block_bunch =
2149 old_block_bunch_pos;
2150 } else assert(new_block_bunch_pos == old_block_bunch_pos);
2151 new_block_bunch_pos->pred = new_pred_pos;
2152 // new_block_bunch_pos->slice = ...; -- see below
2153
2154 // adapt pred
2155 if (new_pred_pos < old_pred_pos)
2156 {
2157 // We need std::swap here to swap the whole content, including
2158 // work counters in case we measure the work.
2159 std::swap(*old_pred_pos, *new_pred_pos); assert(nullptr != old_pred_pos->action_block->succ);
2160 assert(old_pred_pos->action_block->succ->block_bunch->pred == new_pred_pos);
2161 old_pred_pos->action_block->succ->block_bunch->pred = old_pred_pos;
2162 } else assert(new_pred_pos == old_pred_pos);
2163 new_pred_pos->action_block = new_action_block_pos;
2164
2165 /* make the state a bottom state if necessary */ assert(source->bl.ock->nonbottom_begin <= source->pos);
2166 bool became_bottom(false); assert(succ.back().block_bunch->pred->source != source);
2167 if (source != source->succ_inert.begin->block_bunch->pred->source)
2168 {
2169 block_t* const source_block(source->bl.ock);
2170 // make the state a marked bottom state
2171 if (source->pos >= source_block->marked_nonbottom_begin)
2172 {
2173 std::swap(*source->pos,
2174 *source_block->marked_nonbottom_begin++);
2175 } assert(source->pos < source_block->marked_nonbottom_begin);
2176 std::swap(*source->pos, *source_block->nonbottom_begin++);
2177 ++nr_of_new_bottom_states;
2178 became_bottom = true;
2179 }
2180
2181 bunch_t* new_noninert_bunch; assert(nullptr != new_action_block_pos);
2182 if (!new_noninert_block_bunch_ptr->is_null())
2183 {
2184 // There is already some new non-inert transition from this block.
2185 // So we can reuse this block_bunch and its bunch.
2186 // (However, it may be the case that the current transition goes to
2187 // another block; in the latter case, we have to create a new
2188 // action_block-slice.)
2189
2190 // extend the bunch
2191 new_noninert_bunch = (*new_noninert_block_bunch_ptr)->bunch; assert(new_action_block_pos >= new_noninert_bunch->end);
2192 ONLY_IF_DEBUG(
2193 for (const action_block_entry*temp_action_block_pos=new_action_block_pos ;
2194 temp_action_block_pos > new_noninert_bunch->end ; )
2195 {
2196 assert(nullptr == (--temp_action_block_pos)->succ);
2197 }
2198 )
2199 new_noninert_bunch->end = action_block_inert_begin;
2200 /* extend the block_bunch-slice */ assert((*new_noninert_block_bunch_ptr)->end == new_block_bunch_pos);
2201 (*new_noninert_block_bunch_ptr)->end = block_bunch_inert_begin;
2202 if (!(*new_noninert_block_bunch_ptr)->is_stable())
2203 { assert((*new_noninert_block_bunch_ptr)->marked_begin == new_block_bunch_pos);
2204 (*new_noninert_block_bunch_ptr)->marked_begin =
2205 block_bunch_inert_begin;
2206 }
2207 new_block_bunch_pos->slice = *new_noninert_block_bunch_ptr;
2208
2209 /* adapt the action_block-slice */ assert(new_noninert_bunch->begin < new_action_block_pos);
2210 if (nullptr != new_action_block_pos[-1].succ &&
2211 target->bl.ock == new_action_block_pos[-1].
2212 succ->block_bunch->pred->target->bl.ock)
2213 {
2214 // the action_block-slice is suitable: extend it
2215 action_block_entry* const action_block_slice_begin(
2216 new_action_block_pos[-1].begin_or_before_end); assert(nullptr != action_block_slice_begin);
2217 assert(new_action_block_pos-1==action_block_slice_begin->begin_or_before_end);
2218 assert(nullptr != action_block_slice_begin->succ);
2219 assert(action_block_slice_begin->succ->block_bunch->pred->action_block ==
2220 action_block_slice_begin);
2221 action_block_slice_begin->begin_or_before_end =
2222 new_action_block_pos;
2223 new_action_block_pos->begin_or_before_end =
2224 action_block_slice_begin;
2225 }
2226 else
2227 {
2228 // create a new action_block-slice
2229 new_action_block_pos->begin_or_before_end=new_action_block_pos;
2230 if (new_noninert_bunch->is_trivial())
2231 { // Only during initialisation, it may happen that we add new non-inert
2232 make_nontrivial(new_noninert_bunch); // transitions to a nontrivial bunch:
2233 }
2234 #ifndef NDEBUG
2235 else
2236 {
2237 // We make sure that new_noninert_bunch is the first bunch in
2238 // action_block (and because it's always the last one, it will be the
2239 // only one, so there is only one bunch, as ).
2240 for (const action_block_entry* iter = action_block_begin;
2241 iter < new_noninert_bunch->begin; ++iter)
2242 {
2243 assert(nullptr == iter->succ);
2244 assert(nullptr == iter->begin_or_before_end);
2245 }
2246 }
2247 #endif
2248 ++nr_of_action_block_slices;
2249 }
2250
2251 /* adapt the out-slice */ assert(source != succ.front().block_bunch->pred->source);
2252 if (source == new_succ_pos[-1].block_bunch->pred->source &&
2253 new_succ_pos[-1].bunch() == new_noninert_bunch)
2254 {
2255 // the out-slice is suitable: extend it.
2256 succ_entry* const out_slice_begin(
2257 new_succ_pos[-1].begin_or_before_end); assert(nullptr != out_slice_begin);
2258 assert(new_succ_pos - 1 == out_slice_begin->begin_or_before_end);
2259 out_slice_begin->begin_or_before_end = new_succ_pos; assert(out_slice_begin->block_bunch->pred->action_block->succ ==
2260 out_slice_begin);
2261 new_succ_pos->begin_or_before_end = out_slice_begin;
2262 return became_bottom;
2263 }
2264 }
2265 else
2266 {
2267 // create a new bunch for noninert transitions
2268 new_noninert_bunch =
2269 #ifdef USE_POOL_ALLOCATOR
2270 storage.template construct<bunch_t>
2271 #else
2272 new bunch_t
2273 #endif
2274 (new_action_block_pos, action_block_inert_begin);
2275 ++nr_of_bunches;
2276
2277 // create a new block_bunch-slice
2278 #ifdef USE_SIMPLE_LIST
2279 block_bunch_slice_iter_t new_noninert_block_bunch(
2280 splitter_list.emplace_back(
2281 ONLY_IF_POOL_ALLOCATOR( storage, )
2282 block_bunch_inert_begin, new_noninert_bunch, false));
2283 #else
2284 splitter_list.emplace_back(block_bunch_inert_begin,
2285 new_noninert_bunch, false);
2286 block_bunch_slice_iter_t new_noninert_block_bunch(
2287 std::prev(splitter_list.end()));
2288 #endif
2289 ++nr_of_block_bunch_slices;
2290 new_block_bunch_pos->slice = new_noninert_block_bunch;
2291 *new_noninert_block_bunch_ptr = new_noninert_block_bunch;
2292
2293 // create a new action_block-slice
2294 new_action_block_pos->begin_or_before_end = new_action_block_pos;
2295 ++nr_of_action_block_slices;
2296 } assert(&succ.cbegin()[1] == new_succ_pos ||
2297 new_succ_pos[-1].block_bunch->pred->source < source ||
2298 /* create a new out-slice */ new_succ_pos[-1].bunch() != new_noninert_bunch);
2299 new_succ_pos->begin_or_before_end = new_succ_pos;
2300 return became_bottom;
2301 }
2302
2303
2304 public:
2326 ONLY_IF_DEBUG( template<class LTS_TYPE> )
2327 void adapt_transitions_for_new_block(
2328 block_t* const new_block,
2329 block_t* const old_block, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
2330 bool const add_new_noninert_to_splitter,
2331 const block_bunch_slice_iter_t splitter_T,
2332 enum new_block_mode_t const new_block_mode)
2333 { assert(splitter_T->is_stable());
2334 // We begin with a bottom state so the new block gets a sorted list of
2335 // stable block_bunch-slices.
2336 permutation_entry* s_iter(new_block->begin); assert(s_iter < new_block->end);
2337 do
2338 {
2339 state_info_entry* const s(s_iter->st); assert(new_block == s->bl.ock);
2340 assert(s->pos == s_iter);
2341 /* - - - - - - adapt part_tr.block_bunch - - - - - - */
2342 assert(s != succ.front().block_bunch->pred->source);
2343 for (succ_entry* succ_iter(s->succ_inert.begin);
2344 s == succ_iter[-1].block_bunch->pred->source; )
2345 {
2346 succ_iter = move_out_slice_to_new_block(succ_iter, ONLY_IF_DEBUG( partitioner, )
2347 #ifndef USE_SIMPLE_LIST
2348 old_block,
2349 #endif
2350 splitter_T); assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
2351 assert(s == succ_iter->block_bunch->pred->source);
2352 // add_work_to_out_slice(succ_iter, ...) -- subsumed in the call below
2353 }
2354
2355 /*- - - - - - adapt part_tr.action_block - - - - - -*/
2356 assert(s != pred.front().target);
2357 for (pred_entry* pred_iter(s->pred_inert.begin);
2358 s == (--pred_iter)->target; )
2359 { assert(&pred.front() < pred_iter);
2360 assert(nullptr != pred_iter->action_block->succ);
2361 assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
2362 first_move_transition_to_new_action_block(pred_iter); // mCRL2complexity(pred_iter, ...) -- subsumed in the call below
2363 } // mCRL2complexity(s, ...) -- subsumed in the call at the end
2364 }
2365 while (++s_iter < new_block->end);
2366
2367 if (new_block_is_R == new_block_mode)
2368 { assert(splitter_T->source_block() == new_block);
2369 // The `splitter_T` slice moves completely from the old to the new
2370 // block. We move it as a whole to the new block_bunch list.
2371 new_block->stable_block_bunch.splice(
2372 new_block->stable_block_bunch.begin(),
2373 old_block->stable_block_bunch, splitter_T);
2374 } else assert(splitter_T->source_block() == old_block);
2375
2376 // We cannot join the loop above with the one below because transitions
2377 // in the action_block-slices need to be handled in two phases.
2378
2379 s_iter = new_block->begin; assert(s_iter < new_block->end);
2380 do
2381 {
2382 state_info_entry* const s(s_iter->st); assert(s->pos == s_iter); assert(s != pred.front().target);
2383 for (pred_entry* pred_iter(s->pred_inert.begin);
2384 s == (--pred_iter)->target; )
2385 { assert(&pred.front() < pred_iter);
2386 assert(nullptr != pred_iter->action_block->succ);
2387 assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
2388 second_move_transition_to_new_action_block(pred_iter); // mCRL2complexity(pred_iter, ...) -- subsumed in the call below
2389 } // mCRL2complexity(s, ...) -- subsumed in the call at the end
2390 }
2391 while (++s_iter < new_block->end);
2392 assert(0 == new_block->marked_size()); assert(0 == old_block->marked_size());
2393 /* - - - - - - find new non-inert transitions - - - - - - */ assert(1 + &block_bunch.back() - block_bunch_inert_begin ==
2394 action_block_end - action_block_inert_begin);
2395 if (block_bunch_inert_begin <= &block_bunch.back())
2396 {
2397 block_bunch_slice_iter_or_null_t new_noninert_block_bunch;
2398 if (add_new_noninert_to_splitter)
2399 {
2400 new_noninert_block_bunch = splitter_T;
2401 }
2402 else
2403 {
2404 new_noninert_block_bunch = nullptr;
2405 }
2406 if (new_block_is_U == new_block_mode)
2407 { assert(old_block == new_block->end->st->bl.ock);
2408 assert(new_block->end <= &partitioner.part_st.permutation.back());
2409 permutation_entry* target_iter(new_block->begin); assert(target_iter < new_block->end);
2410 do
2411 {
2412 state_info_entry* const s(target_iter->st); assert(s->pos == target_iter);
2413 // check all incoming inert transitions of s, whether they
2414 /* still start in new_block */ assert(s != pred.back().target);
2415 for (pred_entry* pred_iter(s->pred_inert.begin);
2416 s == pred_iter->target; ++pred_iter)
2417 { assert(pred_iter < &pred.back());
2418 assert(nullptr != pred_iter->action_block->succ);
2419 state_info_entry* const t(pred_iter->source); assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
2420 assert(t->pos->st == t);
2421 if (new_block != t->bl.ock)
2422 { assert(old_block == t->bl.ock);
2423 if (!make_noninert(pred_iter,
2424 &new_noninert_block_bunch))
2425 // make_noninert() may modify *pred_iter
2426 {
2427 old_block->mark_nonbottom(t->pos);
2428 }
2429 } // mCRL2complexity(old value of *pred_iter, ...) -- overapproximated by the
2430 // call below
2431 } // mCRL2complexity(s, ...) -- subsumed in the call at the end
2432 }
2433 while (++target_iter < new_block->end); assert(0 < old_block->bottom_size());
2434 }
2435 else
2436 { assert(new_block_is_R == new_block_mode);
2437 /* We have to be careful because make_noninert may move */ assert(&partitioner.part_st.permutation.front() < new_block->begin);
2438 /* a state either forward (to the marked states) or */ assert(old_block == new_block->begin[-1].st->bl.ock);
2439 /* back (to the bottom states). */ assert(0 < old_block->bottom_size());
2440 for(permutation_entry* source_iter(new_block->nonbottom_begin);
2441 source_iter < new_block->marked_nonbottom_begin; )
2442 {
2443 state_info_entry* const s(source_iter->st); assert(s->pos == source_iter);
2444 // check all outgoing inert transitions of s, whether they
2445 /* still end in new_block. */ assert(succ.back().block_bunch->pred->source != s);
2446 succ_entry* succ_iter(s->succ_inert.begin); assert(succ_iter < &succ.back());
2447 bool dont_mark(true); assert(s == succ_iter->block_bunch->pred->source);
2448 do
2449 { assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
2450 if (new_block !=
2451 succ_iter->block_bunch->pred->target->bl.ock)
2452 { assert(old_block == succ_iter->block_bunch->pred->target->bl.ock);
2453 dont_mark = make_noninert(
2454 succ_iter->block_bunch->pred,
2455 &new_noninert_block_bunch);
2456 } // mCRL2complexity(succ_iter->block_bunch->pred, ...) -- overapproximated by
2457 // the call below
2458 }
2459 while (s == (++succ_iter)->block_bunch->pred->source);
2460 if (dont_mark) ++source_iter;
2461 else
2462 { assert(s->pos == source_iter);
2463 new_block->mark_nonbottom(source_iter);
2464 } assert(new_block->nonbottom_begin <= source_iter);
2465 // mCRL2complexity(s, ...) -- overapproximated by the call at the end
2466 }
2467 }
2468 } else assert(block_bunch_inert_begin == 1 + &block_bunch.back());
2469 mCRL2complexity(new_block, add_work(check_complexity::
2470 adapt_transitions_for_new_block, check_complexity::log_n -
2471 check_complexity::ilog2(new_block->size())), partitioner);
2472 }
2473 #ifndef NDEBUG
2476 template <class LTS_TYPE>
2477 void print_trans(const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
2478 {
2479 if (!mCRL2logEnabled(log::debug)) return;
2480 // print all outgoing transitions grouped per successor and out-slice
2481 const succ_entry* succ_iter(&succ.cbegin()[1]);
2482 if (succ_iter >= &succ.back())
2483 {
2484 mCRL2log(log::debug) << "No transitions.\n";
2485 return;
2486 }
2487 const state_info_entry* source(succ_iter->block_bunch->pred->source);
2488 mCRL2log(log::debug) << source->debug_id(partitioner) << ":\n";
2489 block_bunch_slice_iter_or_null_t current_out_bunch(
2490 const_cast<part_trans_t*>(this)->splitter_list.end());
2491 do
2492 {
2493 if (source != succ_iter->block_bunch->pred->source)
2494 { assert(source < succ_iter->block_bunch->pred->source);
2495 source = succ_iter->block_bunch->pred->source;
2496 mCRL2log(log::debug)
2497 << source->debug_id(partitioner) << ":\n";
2498 current_out_bunch =
2499 const_cast<part_trans_t*>(this)->splitter_list.end();
2500 }
2501 if (succ_iter->block_bunch->slice != current_out_bunch)
2502 { assert(!current_out_bunch.is_null());
2503 if (succ_iter->block_bunch->slice.is_null())
2504 { assert(succ_iter == source->succ_inert.begin);
2505 mCRL2log(log::debug)<<"\tInert successors:\n";
2506 current_out_bunch = nullptr;
2507 }
2508 else
2509 { assert(succ_iter < source->succ_inert.begin);
2510 assert(!current_out_bunch.is_null());
2511 assert(current_out_bunch == splitter_list.end() ||
2512 current_out_bunch->bunch != succ_iter->bunch());
2513 mCRL2log(log::debug) << "\tSuccessors in "
2514 <<succ_iter->bunch()->debug_id_short(partitioner)<<":\n";
2515 current_out_bunch = succ_iter->block_bunch->slice;
2516 }
2517 }
2518 mCRL2log(log::debug) << "\t\t"
2519 << succ_iter->block_bunch->pred->debug_id(partitioner) << '\n';
2520 }
2521 while (++succ_iter < &succ.back());
2522
2523 // print all transitions grouped per bunch and action_block-slice
2524 const action_block_entry* action_block_iter(action_block_begin);
2525 do assert(action_block_iter < action_block_end);
2526 while (nullptr == action_block_iter->succ &&
2527 (assert(nullptr == action_block_iter->begin_or_before_end),
2528 ++action_block_iter, true));
2529 do
2530 {
2531 const action_block_entry* bunch_end;
2532 const action_block_entry* action_block_slice_end;
2533 assert(nullptr != action_block_iter->succ);
2534 if (action_block_iter->succ->block_bunch->slice.is_null())
2535 { assert(action_block_iter == action_block_inert_begin);
2536 mCRL2log(log::debug) <<"Inert transition slice [";
2537 action_block_slice_end = bunch_end = action_block_end;
2538 }
2539 else
2540 {
2541 const bunch_t* const bunch(action_block_iter->succ->bunch());
2542 assert(nullptr != bunch);
2543 mCRL2log(log::debug) << bunch->debug_id_short(
2544 partitioner) << ":\n\taction_block-slice [";
2545 assert(bunch->begin == action_block_iter);
2546 bunch_end = bunch->end;
2547 assert(bunch_end <= action_block_inert_begin);
2548 assert(nullptr != action_block_iter->begin_or_before_end);
2549 action_block_slice_end =
2550 action_block_iter->begin_or_before_end + 1;
2551 }
2552 assert(action_block_slice_end <= bunch_end);
2553 // for all action_block-slices in bunch
2554 for (;;)
2555 {
2556 mCRL2log(log::debug) << (action_block_iter -
2557 action_block_begin) << ","
2558 << (action_block_slice_end - action_block_begin) << "):\n";
2559 // for all transitions in the action_block-slice
2560 assert(action_block_iter < action_block_slice_end);
2561 do
2562 {
2563 assert(nullptr != action_block_iter->succ);
2564 mCRL2log(log::debug) << "\t\t"
2565 << action_block_iter->succ->block_bunch->
2566 pred->debug_id(partitioner) << '\n';
2567 }
2568 while (++action_block_iter < action_block_slice_end);
2569 // go to next action_block-slice in the same bunch
2570 while (action_block_iter < bunch_end &&
2571 nullptr == action_block_iter->succ)
2572 {
2573 assert(nullptr == action_block_iter->begin_or_before_end);
2574 ++action_block_iter;
2575 assert(action_block_iter < bunch_end);
2576 }
2577 if (action_block_iter >= bunch_end) break;
2578 assert(nullptr != action_block_iter->begin_or_before_end);
2579 action_block_slice_end =
2580 action_block_iter->begin_or_before_end + 1;
2581 mCRL2log(log::debug) << "\taction_block-slice [";
2582 }
2583 // go to next bunch
2584 assert(action_block_iter == bunch_end);
2585 while (action_block_iter < action_block_end &&
2586 nullptr == action_block_iter->succ)
2587 {
2588 assert(nullptr == action_block_iter->begin_or_before_end);
2589 ++action_block_iter;
2590 }
2591 }
2592 while (action_block_iter < action_block_end);
2593 }
2594 #endif
2595};
2596
2597
2609 ONLY_IF_DEBUG( template<class LTS_TYPE> )
2610inline block_t* block_t::split_off_block(
2611 enum new_block_mode_t const new_block_mode, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
2612 ONLY_IF_POOL_ALLOCATOR(
2613 my_pool<simple_list<block_bunch_slice_t>::entry>& storage, )
2614 state_type const new_seqnr)
2615{ assert(0 < marked_size()); assert(0 < unmarked_bottom_size());
2616 // create a new block
2617 block_t* new_block;
2618 state_type swapcount(std::min(marked_bottom_size(),
2619 unmarked_nonbottom_size()));
2620 if (permutation_entry* const splitpoint(marked_bottom_begin +
2621 unmarked_nonbottom_size()); assert(begin < splitpoint), assert(splitpoint < end),
2622 assert(splitpoint->st->pos == splitpoint),
2623 new_block_is_U == new_block_mode)
2624 { assert((state_type) (splitpoint - begin) <= size()/2);
2625 new_block =
2626 #ifdef USE_POOL_ALLOCATOR
2627 storage.template construct<block_t>
2628 #else
2629 new block_t
2630 #endif
2631 (begin, splitpoint, new_seqnr);
2632 new_block->nonbottom_begin = marked_bottom_begin;
2633
2634 // adapt the old block: it only keeps the R-states
2635 begin = splitpoint;
2636 nonbottom_begin = marked_nonbottom_begin;
2637 }
2638 else
2639 { assert(new_block_is_R == new_block_mode);
2640 new_block =
2641 #ifdef USE_POOL_ALLOCATOR
2642 storage.template construct<block_t>
2643 #else
2644 new block_t
2645 #endif
2646 (splitpoint, end, new_seqnr);
2647 new_block->nonbottom_begin = marked_nonbottom_begin; assert((state_type) (end - splitpoint) <= size()/2);
2648
2649 // adapt the old block: it only keeps the U-states
2650 end = splitpoint;
2651 nonbottom_begin = marked_bottom_begin;
2652 } ONLY_IF_DEBUG( new_block->work_counter = work_counter; )
2653
2654 // swap contents
2655
2656 // The structure of a block is
2657 // | unmarked | marked | unmarked | marked |
2658 // | bottom | bottom | non-bottom | non-bottom |
2659 // We have to swap the marked bottom with the unmarked non-bottom
2660 // states.
2661 //
2662 // It is not necessary to reset the untested_to_U counters; these
2663 // counters are anyway only valid for the states in the respective
2664 // slice.
2665
2666 if (0 < swapcount)
2667 {
2668 // vector swap the states:
2669 permutation_entry* pos1(marked_bottom_begin);
2670 permutation_entry* pos2(marked_nonbottom_begin); assert(pos1 < pos2);
2671 permutation_entry const temp(std::move(*pos1));
2672 for (;;)
2673 {
2674 --pos2; assert(pos1 < pos2);
2675 *pos1 = std::move(*pos2);
2676 ++pos1;
2677 if (0 >= --swapcount) { break; } assert(pos1 < pos2);
2678 *pos2 = std::move(*pos1); // mCRL2complexity(new_block_is_U == new_block_mode ? pos1[-1] : *pos2, ...)
2679 } // -- overapproximated by the call at the end
2680 *pos2 = std::move(temp); // mCRL2complexity(new_block_is_U == new_block_mode ? pos1[-1] : *pos2, ...)
2681 } // -- overapproximated by the call at the end
2682 #ifndef NDEBUG
2683 { const permutation_entry* s_iter(begin); assert(s_iter < end);
2684 do assert(s_iter->st->pos == s_iter);
2685 while (++s_iter < end); }
2686 #endif
2687 // unmark all states in both blocks
2688 marked_nonbottom_begin = end;
2689 marked_bottom_begin = nonbottom_begin;
2690 new_block->marked_bottom_begin = new_block->nonbottom_begin; assert(new_block->size() <= size());
2691
2692 /* set the block pointer of states in the new block */ assert(new_block->marked_nonbottom_begin == new_block->end);
2693 permutation_entry* s_iter(new_block->begin); assert(s_iter < new_block->end);
2694 do
2695 { assert(s_iter->st->pos == s_iter);
2696 s_iter->st->bl.ock = new_block; // mCRL2complexity (*s_iter, ...) -- subsumed in the call below
2697 }
2698 while (++s_iter < new_block->end); mCRL2complexity(new_block, add_work(check_complexity::split_off_block,
2699 check_complexity::log_n - check_complexity::ilog2(new_block->size())),
2700 partitioner);
2701 return new_block;
2702}
2703
2704
2715inline bunch_t* bunch_t::split_off_small_action_block_slice(
2716 part_trans_t& part_tr)
2717{ assert(begin < end); assert(nullptr != begin->succ);
2718 assert(nullptr != begin->begin_or_before_end);
2719 action_block_entry* const first_slice_end(begin->begin_or_before_end + 1); assert(nullptr != end[-1].succ); assert(nullptr!=end[-1].begin_or_before_end);
2720 action_block_entry* const last_slice_begin(end[-1].begin_or_before_end); assert(begin < first_slice_end); assert(first_slice_end <= last_slice_begin);
2721 bunch_t* bunch_T_a_Bprime;
2722 /* Line 2.6: Select some a in Act and B' in Pi_s such that */ assert(last_slice_begin < end); assert(nullptr != first_slice_end[-1].succ);
2723 /* |T--a-->B'| < 1/2 |T| */ assert(nullptr != last_slice_begin->succ);
2724 if (first_slice_end - begin > end - last_slice_begin)
2725 {
2726 // Line 2.7: Pi_t := Pi_t \ {T} union { T--a-->B', T \ T--a-->B' }
2727 bunch_T_a_Bprime =
2728 #ifdef USE_POOL_ALLOCATOR
2729 part_tr.storage.template construct<bunch_t>
2730 #else
2731 new bunch_t
2732 #endif
2733 (last_slice_begin, end); assert(nullptr != bunch_T_a_Bprime);
2734 end = last_slice_begin;
2735 while (nullptr == end[-1].succ)
2736 {
2737 --end; assert(first_slice_end <= end); assert(nullptr == end->begin_or_before_end);
2738 } assert(nullptr != end[-1].begin_or_before_end);
2739 if (first_slice_end == end) part_tr.make_trivial(this);
2740 }
2741 else
2742 {
2743 // Line 2.7: Pi_t := Pi_t \ {T} union { T--a-->B', T \ T--a-->B' }
2744 bunch_T_a_Bprime =
2745 #ifdef USE_POOL_ALLOCATOR
2746 part_tr.storage.template construct<bunch_t>
2747 #else
2748 new bunch_t
2749 #endif
2750 (begin, first_slice_end); assert(nullptr != bunch_T_a_Bprime);
2751 begin = first_slice_end;
2752 while (nullptr == begin->succ)
2753 { assert(nullptr == begin->begin_or_before_end);
2754 ++begin; assert(begin <= last_slice_begin);
2755 } assert(nullptr != begin->begin_or_before_end);
2756 if (begin == last_slice_begin) part_tr.make_trivial(this);
2757 } ONLY_IF_DEBUG( bunch_T_a_Bprime->work_counter = work_counter; )
2758 ++part_tr.nr_of_bunches;
2759 return bunch_T_a_Bprime;
2760}
2762
2763} // end namespace bisim_dnj
2764
2765
2766
2767
2768
2769/* ************************************************************************* */
2770/* */
2771/* A L G O R I T H M S */
2772/* */
2773/* ************************************************************************* */
2774
2775
2776
2777
2778
2782
2783
2784
2785/*=============================================================================
2786= main class =
2787=============================================================================*/
2788
2789
2790
2791
2792
2796template <class LTS_TYPE>
2797class bisim_partitioner_dnj
2798{
2799 private:
2801 enum refine_mode_t{extend_from_marked_states,
2802 extend_from_marked_states__add_new_noninert_to_splitter,
2803 extend_from_splitter };
2804
2806 LTS_TYPE& aut;
2807 ONLY_IF_DEBUG( public: )
2809 bisim_dnj::part_state_t part_st;
2810
2813 bisim_dnj::part_trans_t part_tr;
2814 private:
2824 fixed_vector<bisim_dnj::iterator_or_counter<
2825 bisim_dnj::action_block_entry*> > action_label;
2826 ONLY_IF_DEBUG( public: )
2828 bool const branching;
2829 private:
2835 bool const preserve_divergence;
2836 #ifndef NDEBUG
2837 friend class bisim_dnj::pred_entry;
2838 friend class bisim_dnj::bunch_t;
2839 #endif
2840 public:
2852 bisim_partitioner_dnj(LTS_TYPE& new_aut, bool const new_branching = false,
2853 bool const new_preserve_divergence = false)
2854 : aut(new_aut),
2855 part_st(new_aut.num_states()),
2856 part_tr(new_aut.num_transitions(), new_aut.num_action_labels()),
2857 action_label(new_aut.num_action_labels()),
2858 branching(new_branching),
2859 preserve_divergence(new_preserve_divergence)
2860 { assert(branching || !preserve_divergence);
2861
2862mCRL2log(log::verbose) << "Start initialisation.\n";
2863 create_initial_partition(); ONLY_IF_DEBUG( part_tr.action_block_orig_inert_begin =
2864 part_tr.action_block_inert_begin; )
2865mCRL2log(log::verbose) << "Start refining\n";
2866 refine_partition_until_it_becomes_stable();
2867 }
2868
2869
2874 state_type num_eq_classes() const
2875 {
2876 return part_st.nr_of_blocks;
2877 }
2878
2879
2887 state_type get_eq_class(state_type const s) const
2888 {
2889 return part_st.block(s)->seqnr;
2890 }
2891
2892
2905 void finalize_minimized_LTS()
2906 {
2907 // The labels have already been stored in
2908 // next_nontrivial_and_label.label by
2909 // refine_partition_until_it_becomes_stable().
2910
2911 // for all blocks
2912 const bisim_dnj::permutation_entry*
2913 s_iter(&part_st.permutation.front()); assert(s_iter <= &part_st.permutation.back());
2914 do
2915 {
2916 const bisim_dnj::block_t* const B(s_iter->st->bl.ock);
2917 // for all block_bunch-slices of the block
2918 for (const bisim_dnj::block_bunch_slice_t& block_bunch :
2919 B->stable_block_bunch)
2920 { assert(block_bunch.is_stable()); assert(!block_bunch.empty());
2921 const bisim_dnj::pred_entry* const
2922 pred(block_bunch.end[-1].pred); assert(pred->source->bl.ock == B);
2923 assert(nullptr != pred->action_block->succ);
2924 /* add a transition from the source block to the goal block */ assert(pred->action_block->succ->block_bunch->pred == pred);
2925 /* with the indicated label. */ assert(pred->action_block->succ->block_bunch->slice == &block_bunch);
2926 label_type const
2927 label(block_bunch.bunch->next_nontrivial_and_label.label); assert(0 <= label); assert(label < action_label.size());
2928 aut.add_transition(transition(B->seqnr, label,
2929 pred->target->bl.ock->seqnr));
2930 }
2931 s_iter = B->end;
2932 }
2933 while (s_iter <= &part_st.permutation.back());
2934
2935 // Merge the states, by setting the state labels of each state to the
2936 // concatenation of the state labels of its equivalence class.
2937
2938 if (aut.has_state_info()) /* If there are no state labels
2939 this step can be ignored */
2940 {
2941 /* Create a vector for the new labels */
2942 typename std::remove_reference<decltype(aut.state_labels())>::type
2943 new_labels(num_eq_classes());
2944
2945 state_type i(0); assert(i < aut.num_states());
2946 do
2947 {
2948 const state_type new_index(get_eq_class(i));
2949 new_labels[new_index]=new_labels[new_index]+aut.state_label(i);
2950 }
2951 while (++i < aut.num_states());
2952
2953 aut.set_num_states(num_eq_classes(), false); assert(0 == aut.num_state_labels());
2954 //m_aut.clear_state_labels();
2955 new_labels.swap(aut.state_labels());
2956 }
2957 else
2958 {
2959 aut.set_num_states(num_eq_classes(), false);
2960 }
2961
2962 aut.set_initial_state(get_eq_class(aut.initial_state()));
2963 }
2964
2965
2970 bool in_same_class(state_type const s, state_type const t) const
2971 {
2972 return part_st.block(s) == part_st.block(t);
2973 }
2974 private:
2975
2976 /*--------------------------- main algorithm ----------------------------*/
2977
3000 void create_initial_partition()
3001 {
3002 mCRL2log(log::verbose) << "An O(m log n) "
3003 << (branching ? (preserve_divergence
3004 ? "divergence-preserving branching "
3005 : "branching ")
3006 : "")
3007 << "bisimulation partitioner created for " << part_st.state_size()
3008 << " states and " << aut.num_transitions() << " transitions.\n";
3009
3010 if (part_st.state_size() > 2 * aut.num_transitions() + 1)
3011 {
3012 mCRL2log(log::warning) << "There are several isolated states "
3013 "without incoming or outgoing transition. It is not "
3014 "guaranteed that branching bisimulation minimisation runs in "
3015 "time O(m log n).\n";
3016 }
3017
3018sort_transitions(aut.get_transitions(), tgt_lbl_src);
3019mCRL2log(log::verbose) << "Carried out sorting\n";
3020 // create one block for all states
3021 bisim_dnj::block_t* B(
3022 #ifdef USE_POOL_ALLOCATOR
3023 part_tr.storage.template construct<bisim_dnj::block_t>
3024 #else
3025 new bisim_dnj::block_t
3026 #endif
3027 (&part_st.permutation.front(),
3028 1 + &part_st.permutation.back(), part_st.nr_of_blocks++));
3029
3030 // Iterate over the transitions to count how to order them in
3031 // part_trans_t
3032
3033 // counters for the non-inert outgoing and incoming transitions per
3034 // state are provided in part_st.state_info. These counters have been
3035 // initialised to zero in the constructor of part_state_t.
3036 // counters for the non-inert transition per label are stored in
3037 // action_label.
3038 assert(action_label.size() == aut.num_action_labels());
3039 // counter for the total number of inert transitions:
3040 trans_type inert_transitions(0);
3041 for (const transition& t: aut.get_transitions())
3042 {
3043 if (branching&&aut.is_tau(aut.apply_hidden_label_map(t.label()))&& ((
3044 t.from() != t.to()) || (assert(preserve_divergence), false)))
3045 {
3046 // The transition is inert.
3047 ++part_st.state_info[t.from()].succ_inert.count;
3048 ++inert_transitions;
3049
3050 // The source state should become non-bottom:
3051 if (part_st.state_info[t.from()].pos < B->nonbottom_begin)
3052 {
3053 std::swap(*part_st.state_info[t.from()].pos,
3054 *--B->nonbottom_begin);
3055 // we do not yet update the marked_bottom_begin pointer
3056 }
3057 }
3058 else
3059 {
3060 // The transition is non-inert. (It may be a self-loop).
3061 ++part_st.state_info[t.from()].untested_to_U_eqv.count;
3062 ++action_label[aut.apply_hidden_label_map(t.label())].count;
3063 }
3064 ++part_st.state_info[t.to()].pred_inert.count;
3065 }
3066 // Now we update the marked_bottom_begin pointer:
3067 B->marked_bottom_begin = B->nonbottom_begin;
3068
3069 // set the pointers to transition slices in the state info entries
3070
3071 // We set them all to the end of the respective slice here. Then, with
3072 // every transition, the pointer will be reduced by one, so that after
3073 // placing all transitions it will point to the beginning of the slice.
3074
3075 bisim_dnj::pred_entry* next_pred_begin(&part_tr.pred.begin()[1]);
3076 bisim_dnj::succ_entry* next_succ_begin(&part_tr.succ.begin()[1]);
3077 bisim_dnj::state_info_entry* state_iter(&part_st.state_info.front()); assert(state_iter <= &part_st.state_info.back());
3078 do
3079 {
3080 state_iter->bl.ed_noninert_end = next_pred_begin;
3081 next_pred_begin += state_iter->pred_inert.count;
3082 state_iter->pred_inert.convert_to_iterator(next_pred_begin);
3083
3084 // create slice descriptors in part_tr.succ for each state with
3085 /* outgoing transitions. */ assert(nullptr != next_succ_begin);
3086 state_iter->untested_to_U_eqv.convert_to_iterator(
3087 next_succ_begin + state_iter->untested_to_U_eqv.count);
3088 if (next_succ_begin < state_iter->untested_to_U_eqv.begin)
3089 { assert(nullptr != state_iter->untested_to_U_eqv.begin);
3090 next_succ_begin->begin_or_before_end =
3091 state_iter->untested_to_U_eqv.begin - 1;
3092 for (bisim_dnj::succ_entry* const
3093 out_slice_begin(next_succ_begin);
3094 ++next_succ_begin < state_iter->untested_to_U_eqv.begin; )
3095 {
3096 next_succ_begin->begin_or_before_end = out_slice_begin; // mCRL2complexity(next_succ_begin->block_bunch->pred, ...) -- subsumed in the
3097 } // call below
3098
3099 B->mark(state_iter->pos);
3100 }
3101 state_iter->succ_inert.convert_to_iterator(next_succ_begin +
3102 state_iter->succ_inert.count);
3103 #ifndef NDEBUG
3104 while (next_succ_begin < state_iter->succ_inert.begin)
3105 { assert(nullptr == next_succ_begin->begin_or_before_end);
3106 ++next_succ_begin;
3107 }
3108 #endif
3109 next_succ_begin = state_iter->succ_inert.begin; // mCRL2complexity(*state_iter, ...) -- subsumed in the call at the end
3110 }
3111 while (++state_iter <= &part_st.state_info.back());
3112
3113 // Line 2.4: Pi_t := { { all non-inert transitions } }
3114 part_tr.action_block_inert_begin =
3115 part_tr.action_block_end - inert_transitions; assert(part_tr.action_block_begin <= part_tr.action_block_inert_begin);
3116 part_tr.block_bunch_inert_begin =
3117 1 + &part_tr.block_bunch.back() - inert_transitions; assert(1 + &part_tr.block_bunch.front() <= part_tr.block_bunch_inert_begin);
3118 bisim_dnj::bunch_t* bunch(nullptr);
3119
3120 if (1 + &part_tr.block_bunch.front() < part_tr.block_bunch_inert_begin)
3121 { assert(part_tr.action_block_begin < part_tr.action_block_inert_begin);
3122 // create a single bunch containing all non-inert transitions
3123 bunch =
3124 #ifdef USE_POOL_ALLOCATOR
3125 part_tr.storage.template construct<bisim_dnj::bunch_t>
3126 #else
3127 new bisim_dnj::bunch_t
3128 #endif
3129 (part_tr.action_block_begin,
3130 part_tr.action_block_inert_begin); assert(nullptr != bunch); assert(part_tr.splitter_list.empty());
3131 ++part_tr.nr_of_bunches; assert(1 == part_tr.nr_of_bunches);
3132
3133 // create a single block_bunch entry for all non-inert transitions
3134 part_tr.splitter_list.emplace_front(
3135 ONLY_IF_POOL_ALLOCATOR( part_tr.storage, )
3136 part_tr.block_bunch_inert_begin, bunch, false); assert(!part_tr.splitter_list.empty());
3137 ++part_tr.nr_of_block_bunch_slices; assert(1 == part_tr.nr_of_block_bunch_slices);
3138 }
3139
3140 // create slice descriptors in part_tr.action_block for each label
3141
3142 // The action_block array shall have the tau transitions at the end:
3143 // first the non-inert tau transitions (during initialisation, that are
3144 // only the tau self-loops), then the tau transitions that have become
3145 // non-inert and finally the inert transitions.
3146 // Transitions with other labels are placed from beginning to end.
3147 // Every such transition block except the last one ends with a dummy
3148 /* entry. If there are transition labels without transitions, */ assert((size_t) (part_tr.action_block_end - part_tr.action_block_begin) ==
3149 /* multiple dummy entries will be placed side-by-side. */ aut.num_transitions() + action_label.size() - 1);
3150 bisim_dnj::action_block_entry*
3151 next_action_label_begin(part_tr.action_block_begin);
3152 trans_type const n_square(part_st.state_size() * part_st.state_size()); ONLY_IF_DEBUG( trans_type max_transitions = n_square; )
3153 label_type label(action_label.size()); assert(0 < label);
3154 do
3155 {
3156 --label;
3157 if (0 < action_label[label].count)
3158 { assert(nullptr != bunch);
3159 if (++part_tr.nr_of_action_block_slices == 2)
3160 {
3161 // This is the second action_block-slice, so the bunch is
3162 // not yet marked as nontrivial but it should be.
3163 part_tr.make_nontrivial(bunch);
3164 }
3165 if (n_square < action_label[label].count)
3166 {
3167 mCRL2log(log::warning) << "There are "
3168 << action_label[label].count << ' '
3169 << pp(aut.action_label(label)) << "-transitions. "
3170 "This is more than n^2 (= " << n_square << "). It is "
3171 "not guaranteed that branching bisimulation "
3172 "minimisation runs in time O(m log n).\n"; ONLY_IF_DEBUG( if (max_transitions < action_label[label].count)
3173 { max_transitions = action_label[label].count; } )
3174 }
3175 // initialise begin_or_before_end pointers for this
3176 // action_block-slice
3177 action_label[label].convert_to_iterator(
3178 next_action_label_begin + action_label[label].count);
3179 next_action_label_begin->begin_or_before_end =
3180 action_label[label].begin - 1; assert(nullptr != next_action_label_begin->begin_or_before_end);
3181 bisim_dnj::action_block_entry* const
3182 action_block_slice_begin(next_action_label_begin); assert(nullptr != action_block_slice_begin);
3183 while (++next_action_label_begin < action_label[label].begin)
3184 {
3185 next_action_label_begin->begin_or_before_end =
3186 action_block_slice_begin; // mCRL2complexity(next_action_label_begin->succ->block_bunch->pred, ...) --
3187 } // subsumed in the call at the end
3188 }
3189 else
3190 {
3191 action_label[label].convert_to_iterator(
3192 next_action_label_begin);
3193 if (0 != label && aut.num_transitions() < action_label.size())
3194 {
3195 mCRL2log(log::verbose) << "Action label "
3196 << pp(aut.action_label(label)) << " has no "
3197 "transitions, and the number of action labels exceeds "
3198 "the number of transitions. It is not guaranteed that "
3199 "branching bisimulation minimisation runs in time "
3200 "O(m log n).\n";
3201 }
3202 }
3203 }
3204 while (0 < label && (/* insert a dummy entry */ assert(next_action_label_begin < part_tr.action_block_inert_begin),
3205 next_action_label_begin->succ = nullptr,
3206 next_action_label_begin->begin_or_before_end = nullptr,
3207 ++next_action_label_begin, true)); assert(next_action_label_begin == part_tr.action_block_inert_begin);
3208
3209 /* distribute the transitions over the data structures */ ONLY_IF_DEBUG( check_complexity::init(2 * max_transitions); )
3210
3211 bisim_dnj::block_bunch_entry*
3212 next_block_bunch(1 + &part_tr.block_bunch.front());
3213 for (const transition& t: aut.get_transitions())
3214 {
3215 bisim_dnj::state_info_entry* const
3216 source(&part_st.state_info.front() + t.from());
3217 bisim_dnj::state_info_entry* const
3218 target(&part_st.state_info.front() + t.to());
3219 bisim_dnj::succ_entry* succ_pos;
3220 bisim_dnj::block_bunch_entry* block_bunch_pos;
3221 bisim_dnj::pred_entry* pred_pos;
3222 bisim_dnj::action_block_entry* action_block_pos;
3223
3224 if (branching&&aut.is_tau(aut.apply_hidden_label_map(t.label()))&& ((
3225 t.from() != t.to()) || (assert(preserve_divergence), false)))
3226 {
3227 // It is a (normal) inert transition: place near the end of the
3228 // respective pred/succ slices, just before the other inert
3229 // transitions.
3230 succ_pos = --source->succ_inert.begin; assert(nullptr == succ_pos->begin_or_before_end);
3231 block_bunch_pos = 1 + &part_tr.block_bunch.back() -
3232 inert_transitions; assert(block_bunch_pos >= part_tr.block_bunch_inert_begin);
3233 pred_pos = --target->pred_inert.begin; assert(block_bunch_pos->slice.is_null());
3234 action_block_pos = part_tr.action_block_end-inert_transitions; assert(action_block_pos >= part_tr.action_block_inert_begin);
3235 action_block_pos->begin_or_before_end = nullptr;
3236 --inert_transitions;
3237 }
3238 else
3239 {
3240 // It is a non-inert transition (possibly a self-loop): place
3241 // at the end of the respective succ slice and at the beginning
3242 // of the respective pred slice.
3243 succ_pos =
3244 --part_st.state_info[t.from()].untested_to_U_eqv.begin; assert(nullptr != succ_pos->begin_or_before_end);
3245 assert(nullptr != succ_pos->begin_or_before_end->begin_or_before_end);
3246 assert(succ_pos->begin_or_before_end <= succ_pos ||
3247 succ_pos->begin_or_before_end->begin_or_before_end == succ_pos);
3248 block_bunch_pos = next_block_bunch++; assert(block_bunch_pos < part_tr.block_bunch_inert_begin);
3249 pred_pos = target->bl.ed_noninert_end++;
3250 action_block_pos =
3251 --action_label[aut.apply_hidden_label_map(t.label())].begin; assert(nullptr != action_block_pos->begin_or_before_end);
3252 assert(nullptr != action_block_pos->begin_or_before_end->begin_or_before_end);
3253 assert(action_block_pos->begin_or_before_end <= action_block_pos ||
3254 action_block_pos->begin_or_before_end->
3255 begin_or_before_end == action_block_pos);
3256 assert(!part_tr.splitter_list.empty());
3257 block_bunch_pos->slice = part_tr.splitter_list.begin(); assert(action_block_pos < part_tr.action_block_inert_begin);
3258 } assert(target->bl.ed_noninert_end <= target->pred_inert.begin);
3259 succ_pos->block_bunch = block_bunch_pos;
3260 block_bunch_pos->pred = pred_pos;
3261 pred_pos->action_block = action_block_pos;
3262 pred_pos->source = source;
3263 pred_pos->target = target; assert(nullptr != succ_pos);
3264 action_block_pos->succ = succ_pos; // mCRL2complexity(pred_pos, ...) -- subsumed in the call at the end
3265 } assert(0 == inert_transitions);
3266 /* delete transitions already -- they are no longer needed. We will */ assert(next_block_bunch == part_tr.block_bunch_inert_begin);
3267 // add new transitions at the end of minimisation.
3268 aut.clear_transitions();
3269
3270 state_iter = &part_st.state_info.front(); assert(state_iter <= &part_st.state_info.back());
3271 do
3272 {
3273 state_iter->bl.ock = B;
3274 }
3275 while (++state_iter <= &part_st.state_info.back());
3276
3277 if (nullptr != bunch)
3278 {
3279 while (nullptr == bunch->begin->succ)
3280 { assert(nullptr == bunch->begin->begin_or_before_end);
3281 ++bunch->begin; assert(bunch->begin < bunch->end);
3282 } assert(nullptr != bunch->begin->begin_or_before_end);
3283 while (nullptr == bunch->end[-1].succ)
3284 { assert(nullptr == bunch->end[-1].begin_or_before_end);
3285 --bunch->end; assert(bunch->begin < bunch->end);
3286 } assert(nullptr != bunch->end[-1].begin_or_before_end);
3287
3288 /* Line 2.2: B_vis := { s in S | there exists a visible */ mCRL2complexity(B, add_work(check_complexity::
3289 /* transition that is reachable */ create_initial_partition, 1U), *this);
3290 // from s }
3291 // B_invis := S \ B_vis
3292 // Line 2.3: Pi_s := { B_vis, B_invis } \ { emptyset }
3293 // At this point, all states with a visible transition are
3294 // marked.
3295 if (0 < B->marked_size())
3296 { ONLY_IF_DEBUG( part_st.print_part(*this);
3297 part_tr.print_trans(*this); )
3298 bisim_dnj::block_bunch_slice_iter_t slice =
3299 part_tr.splitter_list.begin();
3300 if (1 < B->size())
3301 {
3302 B = split(B, /* splitter block_bunch */ slice,
3303 extend_from_marked_states__add_new_noninert_to_splitter);
3304 // We can ignore possible new non-inert transitions, as
3305 // every R-bottom state already has a transition in bunch.
3306 B->marked_nonbottom_begin = B->end;
3307 }
3308 else
3309 { assert(B->nonbottom_begin == B->end);
3310 /* A block with 1 state will not be split. However, we */ assert(B->marked_nonbottom_begin == B->end);
3311 // still have to make the splitter stable.
3312 B->stable_block_bunch.splice(B->stable_block_bunch.end(),
3313 part_tr.splitter_list, slice);
3314 slice->make_stable();
3315 } assert(!B->stable_block_bunch.empty()); assert(part_tr.splitter_list.empty());
3316 assert(B->stable_block_bunch.front().end <= part_tr.block_bunch_inert_begin);
3317 assert(1 + &part_tr.block_bunch.front() < B->stable_block_bunch.front().end);
3318 B->marked_bottom_begin = B->nonbottom_begin; assert(!B->stable_block_bunch.front().empty());
3319 }
3320 } else assert(0 == B->marked_size());
3321 }
3322 #ifndef NDEBUG
3333 void assert_stability() const
3334 {
3335 part_st.assert_consistency(*this);
3336
3337 assert(part_tr.succ.size() == part_tr.block_bunch.size() + 1);
3338 assert(part_tr.pred.size() == part_tr.block_bunch.size() + 1);
3339 assert((size_t)(part_tr.action_block_end-part_tr.action_block_begin) ==
3340 part_tr.block_bunch.size() + action_label.size() - 2);
3341 if (part_tr.block_bunch.empty()) return;
3342
3343 assert(part_tr.splitter_list.empty());
3344 /* for (const block_bunch_slice_t& block_bunch : part_tr.splitter_list)
3345 {
3346 assert(!block_bunch.is_stable());
3347 } */
3348
3349 trans_type true_nr_of_block_bunch_slices(0);
3350 // for all blocks
3351 const bisim_dnj::permutation_entry*
3352 perm_iter(&part_st.permutation.front());
3353 assert(perm_iter <= &part_st.permutation.back());
3354 do
3355 {
3356 const bisim_dnj::block_t* const block(perm_iter->st->bl.ock);
3357 unsigned const max_block(check_complexity::log_n -
3358 check_complexity::ilog2(block->size()));
3359 // iterators have no predefined hash, so we store pointers:
3360 std::unordered_set<const bisim_dnj::block_bunch_slice_t*>
3361 block_bunch_check_set;
3362 #ifndef USE_SIMPLE_LIST
3363 block_bunch_check_set.reserve(
3364 block->stable_block_bunch.size());
3365 #endif
3366
3367 // for all stable block_bunch-slices of the block
3368 for (const bisim_dnj::block_bunch_slice_t& block_bunch :
3369 block->stable_block_bunch)
3370 {
3371 assert(block_bunch.source_block() == block);
3372 assert(block_bunch.is_stable());
3373 block_bunch_check_set.insert(&block_bunch);
3374 mCRL2complexity(&block_bunch, no_temporary_work(
3375 block_bunch.bunch->max_work_counter(*this)), *this);
3376 ++true_nr_of_block_bunch_slices;
3377 }
3378
3379 // for all states in the block
3380 do
3381 {
3382 trans_type block_bunch_count(0);
3383 const bisim_dnj::state_info_entry* const state(perm_iter->st);
3384 assert(state!=part_tr.succ.front().block_bunch->pred->source);
3385 // for all out-slices of the state
3386 for (const bisim_dnj::succ_entry*
3387 out_slice_end(state->succ_inert.begin);
3388 state == out_slice_end[-1].block_bunch->pred->source; )
3389 { assert(!out_slice_end[-1].block_bunch->slice.is_null());
3390 bisim_dnj::block_bunch_slice_const_iter_t const
3391 block_bunch_slice(out_slice_end[-1].block_bunch->slice);
3392 const bisim_dnj::bunch_t* const bunch(
3393 block_bunch_slice->bunch);
3394 assert(block == block_bunch_slice->source_block());
3395 if (block_bunch_slice->is_stable())
3396 {
3397 assert(1 == block_bunch_check_set.count(
3398 &*block_bunch_slice));
3399 ++block_bunch_count;
3400 }
3401 else assert(0); // i. e. all block_bunch-slices should
3402 // be stable
3403 const bisim_dnj::succ_entry* const out_slice_begin(
3404 out_slice_end[-1].begin_or_before_end);
3405 assert(nullptr != out_slice_begin);
3406 assert(out_slice_begin < out_slice_end);
3407 assert(nullptr != out_slice_begin->begin_or_before_end);
3408 assert(out_slice_begin->begin_or_before_end + 1 ==
3409 out_slice_end);
3410
3411 // for all transitions in the out-slice
3412 do
3413 {
3414 --out_slice_end;
3415 assert(bunch->begin <=
3416 out_slice_end->block_bunch->pred->action_block);
3417 assert(out_slice_end->block_bunch->pred->
3418 action_block < bunch->end);
3419 assert(out_slice_end->block_bunch->slice ==
3420 block_bunch_slice);
3421 assert(nullptr != out_slice_end->begin_or_before_end);
3422 if (out_slice_end->block_bunch + 1 !=
3423 block_bunch_slice->end)
3424 {
3425 assert(out_slice_end->block_bunch + 1 <
3426 block_bunch_slice->end);
3427 assert(out_slice_end->block_bunch[1].slice ==
3428 block_bunch_slice);
3429 }
3430 mCRL2complexity(out_slice_end->block_bunch->pred,
3431 no_temporary_work(max_block,
3432 check_complexity::log_n -
3433 check_complexity::ilog2(out_slice_end->
3434 block_bunch->pred->target->bl.ock->size()),
3435 perm_iter < block->nonbottom_begin),*this);
3436 }
3437 while (out_slice_begin < out_slice_end &&
3438 (assert(out_slice_begin ==
3439 out_slice_end->begin_or_before_end), true));
3440 }
3441 if (perm_iter < block->nonbottom_begin)
3442 {
3443 assert(block_bunch_check_set.size() == block_bunch_count);
3444 }
3445 }
3446 while (++perm_iter < block->end);
3447 }
3448 while (perm_iter <= &part_st.permutation.back());
3449 assert(part_tr.nr_of_block_bunch_slices ==
3450 true_nr_of_block_bunch_slices);
3451 assert(part_tr.action_block_begin <= part_tr.action_block_inert_begin);
3452 assert(&part_tr.block_bunch.front() < part_tr.block_bunch_inert_begin);
3453 if (branching)
3454 { assert(part_tr.action_block_inert_begin<=part_tr.action_block_end);
3455 assert(part_tr.block_bunch_inert_begin <=
3456 1 + &part_tr.block_bunch.back());
3457 assert(1 + &part_tr.block_bunch.back() -
3458 part_tr.block_bunch_inert_begin ==
3459 part_tr.action_block_end - part_tr.action_block_inert_begin);
3460
3461 // for all inert transitions
3462 for (const bisim_dnj::action_block_entry* action_block(
3463 part_tr.action_block_inert_begin);
3464 action_block < part_tr.action_block_end;
3465 ++action_block)
3466 { assert(nullptr == action_block->begin_or_before_end);
3467 const bisim_dnj::succ_entry* const
3468 succ_iter(action_block->succ);
3469 assert(nullptr != succ_iter);
3470 assert(succ_iter->block_bunch->slice.is_null());
3471 const bisim_dnj::pred_entry* const
3472 pred_iter(succ_iter->block_bunch->pred);
3473 assert(action_block == pred_iter->action_block);
3474 assert(part_tr.block_bunch_inert_begin <=
3475 succ_iter->block_bunch);
3476 assert(pred_iter->source != pred_iter->target);
3477 assert(pred_iter->source->bl.ock == pred_iter->target->bl.ock);
3478 assert(pred_iter->source->succ_inert.begin <= succ_iter);
3479 assert(pred_iter->source->succ_inert.begin == succ_iter ||
3480 succ_iter[-1].block_bunch->pred->source==pred_iter->source);
3481 assert(pred_iter->target->pred_inert.begin <= pred_iter);
3482 assert(pred_iter->target->pred_inert.begin == pred_iter ||
3483 pred_iter[-1].target == pred_iter->target);
3484 unsigned const max_block(check_complexity::log_n -
3485 check_complexity::ilog2(pred_iter->target->bl.ock->size()));
3486 mCRL2complexity(pred_iter, no_temporary_work(max_block,
3487 max_block, false), *this);
3488 }
3489 }
3490 else
3491 {
3492 assert(!preserve_divergence);
3493 assert(part_tr.action_block_inert_begin==part_tr.action_block_end);
3494 assert(part_tr.block_bunch_inert_begin ==
3495 1 + &part_tr.block_bunch.back());
3496 }
3497 const bisim_dnj::action_block_entry*
3498 action_slice_end(part_tr.action_block_inert_begin);
3499 trans_type true_nr_of_bunches(0);
3500 trans_type true_nr_of_nontrivial_bunches(0);
3501 trans_type true_nr_of_action_block_slices(0);
3502 // for all action labels and bunches
3503 label_type label(0);
3504 assert(label < action_label.size());
3505 const bisim_dnj::bunch_t* previous_bunch(nullptr);
3506 do
3507 {
3508 assert(part_tr.action_block_begin <= action_label[label].begin);
3509 assert(action_label[label].begin <= action_slice_end);
3510 assert(action_slice_end <= part_tr.action_block_inert_begin);
3511 // for all action_block slices
3512 for (const bisim_dnj::action_block_entry*
3513 action_block_slice_end(action_slice_end);
3514 action_label[label].begin < action_block_slice_end; )
3515 {
3516 const bisim_dnj::action_block_entry* const
3517 action_block_slice_begin(
3518 action_block_slice_end[-1].begin_or_before_end);
3519 assert(nullptr != action_block_slice_begin);
3520 assert(action_block_slice_begin < action_block_slice_end);
3521 assert(action_block_slice_end <= action_slice_end);
3522 assert(nullptr != action_block_slice_begin->succ);
3523 const bisim_dnj::block_t* const
3524 target_block(action_block_slice_begin->
3525 succ->block_bunch->pred->target->bl.ock);
3526 const bisim_dnj::bunch_t* const
3527 bunch(action_block_slice_begin->succ->bunch());
3528 if (previous_bunch != bunch)
3529 {
3530 assert(nullptr == previous_bunch);
3531 previous_bunch = bunch;
3532 assert(bunch->end == action_block_slice_end);
3533 if (bunch->begin == action_block_slice_begin)
3534 {
3535 // Perhaps this does not always hold; sometimes, an
3536 // action_block slice disappears but the bunch cannot
3537 // be made trivial.
3538 assert(bunch->is_trivial());
3539 }
3540 else
3541 {
3542 assert(!bunch->is_trivial());
3543 ++true_nr_of_nontrivial_bunches;
3544 }
3545 mCRL2complexity(bunch, no_temporary_work(
3546 bunch->max_work_counter(*this)), *this);
3547 ++true_nr_of_bunches;
3548 }
3549 if(bunch->begin == action_block_slice_begin)
3550 {
3551 previous_bunch = nullptr;
3552 }
3553 else assert(bunch->begin < action_block_slice_begin);
3554
3555 assert(action_block_slice_begin->begin_or_before_end + 1 ==
3556 action_block_slice_end);
3557 // for all transitions in the action_block slice
3558 const bisim_dnj::action_block_entry*
3559 action_block(action_block_slice_end);
3560 do
3561 {
3562 --action_block;
3563 const bisim_dnj::succ_entry* const
3564 succ_iter(action_block->succ);
3565 assert(nullptr != succ_iter);
3566 const bisim_dnj::pred_entry* const
3567 pred_iter(succ_iter->block_bunch->pred);
3568 assert(action_block == pred_iter->action_block);
3569 assert(succ_iter->block_bunch <
3570 part_tr.block_bunch_inert_begin);
3571 assert(!branching || !aut.is_tau(label) ||
3572 pred_iter->source->bl.ock!=pred_iter->target->bl.ock ||
3573 (preserve_divergence &&
3574 pred_iter->source == pred_iter->target));
3575 assert(succ_iter < pred_iter->source->succ_inert.begin);
3576 assert(succ_iter+1==pred_iter->source->succ_inert.begin ||
3577 succ_iter[1].block_bunch->pred->source ==
3578 pred_iter->source);
3579 assert(pred_iter < pred_iter->target->pred_inert.begin);
3580 assert(pred_iter+1==pred_iter->target->pred_inert.begin ||
3581 pred_iter[1].target == pred_iter->target);
3582 assert(target_block == pred_iter->target->bl.ock);
3583 assert(bunch == succ_iter->bunch());
3584 }
3585 while (action_block_slice_begin < action_block &&
3586 (// some properties only need to be checked for states that
3587 // are not the first one:
3588 assert(action_block->begin_or_before_end ==
3589 action_block_slice_begin), true));
3590 action_block_slice_end = action_block_slice_begin;
3591 ++true_nr_of_action_block_slices;
3592 }
3593 if (action_slice_end < part_tr.action_block_inert_begin)
3594 {
3595 // there is a dummy transition between action labels
3596 assert(nullptr == action_slice_end->succ);
3597 assert(nullptr == action_slice_end->begin_or_before_end);
3598 }
3599 }
3600 while (++label < action_label.size() &&
3601 (action_slice_end = action_label[label - 1].begin - 1, true));
3602 assert(nullptr == previous_bunch);
3603 assert(part_tr.nr_of_bunches == true_nr_of_bunches);
3604 assert(part_tr.nr_of_nontrivial_bunches ==
3605 true_nr_of_nontrivial_bunches);
3606 assert(part_tr.nr_of_action_block_slices ==
3607 true_nr_of_action_block_slices);
3608 }
3609 #endif
3627 void refine_partition_until_it_becomes_stable()
3628 {
3629 // Line 2.5: for all non-trivial bunches bunch_T in Pi_t do
3630 clock_t next_print_time = clock();
3631 const clock_t rounded_start_time = next_print_time - CLOCKS_PER_SEC/2;
3632 // const double log_initial_nr_of_action_block_slices =
3633 // 100 / std::log(part_tr.nr_of_action_block_slices);
3634 for (;;)
3635 { // mCRL2complexity(...) -- this loop will be ascribed to (the transitions in)
3636 // the new bunch below.
3637 /*------------------ find a non-trivial bunch -------------------*/ ONLY_IF_DEBUG( part_st.print_part(*this); part_tr.print_trans(*this);
3638 assert_stability(); )
3639 /* Line 2.6: Select some a in Act and B' in Pi_s such that */ assert(part_tr.nr_of_bunches + part_tr.nr_of_nontrivial_bunches <=
3640 /* |bunch_T_a_Bprime| <= 1/2 |bunch_T| */ part_tr.nr_of_action_block_slices);
3641 bisim_dnj::bunch_t* const bunch_T(part_tr.get_some_nontrivial());
3642 if (mCRL2logEnabled(log::verbose))
3643 {
3644 if (clock_t now = clock(); next_print_time <= now ||
3645 nullptr == bunch_T)
3646 {
3647
3648 /* - - - - -print progress information- - - - - */
3649
3650 // The formula below should ensure that `next_print_time`
3651 // increases by a whole number of minutes, so that the
3652 // progress information is printed every minute (or, if
3653 // one iteration takes more than one minute, after a whole
3654 // number of minutes).
3655 next_print_time+=((now-next_print_time)/(60*CLOCKS_PER_SEC)
3656 + 1) * (60*CLOCKS_PER_SEC);
3657 now = (now - rounded_start_time) / CLOCKS_PER_SEC;
3658 if (0 != now)
3659 {
3660 if (60 <= now)
3661 {
3662 if (3600 <= now)
3663 {
3664 mCRL2log(log::verbose)
3665 << now / 3600 << " h ";
3666 now %= 3600;
3667 }
3668 mCRL2log(log::verbose)
3669 << now / 60 << " min ";
3670 now %= 60;
3671 }
3672 mCRL2log(log::verbose) << now
3673 << " sec passed since starting the main loop.\n";
3674 }
3675 #define PRINT_SG_PL(counter, sg_string, pl_string) \
3676 (counter) \
3677 << (1 == (counter) ? (sg_string) : (pl_string))
3678 mCRL2log(log::verbose)
3679 << (nullptr == bunch_T ? "The reduced LTS contains "
3680 : "The reduced LTS contains at least ")
3681 << PRINT_SG_PL(part_st.nr_of_blocks,
3682 " state and ", " states and ")
3683 << PRINT_SG_PL(part_tr.nr_of_block_bunch_slices,
3684 " transition.", " transitions.");
3685 if (1 < part_tr.nr_of_action_block_slices)
3686 {
3687 #define PRINT_INT_PERCENTAGE(num,denom) \
3688 (((num) * 200 + (denom)) / (denom) / 2)
3689 mCRL2log(log::verbose) << " Estimated "
3690 << PRINT_INT_PERCENTAGE(part_tr.nr_of_bunches - 1,
3691 part_tr.nr_of_action_block_slices - 1)
3692 << "% done.";
3693 #undef PRINT_INT_PERCENTAGE
3694 }
3695 mCRL2log(log::verbose)
3696 // << " Logarithmic estimate: "
3697 // << (int)(100.5+std::log((double) part_tr.nr_of_bunches/
3698 // part_tr.nr_of_action_block_slices)
3699 // *log_initial_nr_of_action_block_slices)
3700 // << "% done."
3701 << "\nThe current partition contains ";
3702 if (branching)
3703 {
3704 mCRL2log(log::verbose)
3705 << PRINT_SG_PL(part_tr.nr_of_new_bottom_states,
3706 " new bottom state, ", " new bottom states, ");
3707 } else assert(0 == part_tr.nr_of_new_bottom_states);
3708 mCRL2log(log::verbose)
3709 << PRINT_SG_PL(part_tr.nr_of_bunches,
3710 " bunch (of which ", " bunches (of which ")
3711 << PRINT_SG_PL(part_tr.nr_of_nontrivial_bunches,
3712 " is nontrivial), and ", " are nontrivial), and ")
3713 << PRINT_SG_PL(part_tr.nr_of_action_block_slices,
3714 " action-block-slice.\n", " action-block-slices.\n");
3715 #undef PRINT_SG_PL
3716 }
3717 }
3718 if (nullptr == bunch_T) { break; } ONLY_IF_DEBUG( mCRL2log(log::debug) << "Refining "
3719 /* Line 2.7: Pi_t := Pi_t \ { bunch_T } union */ << bunch_T->debug_id(*this) << '\n'; )
3720 /* { bunch_T_a_Bprime, bunch_T \ bunch_T_a_Bprime } */ assert(part_tr.nr_of_bunches < part_tr.nr_of_action_block_slices);
3721 bisim_dnj::bunch_t* const bunch_T_a_Bprime(
3722 bunch_T->split_off_small_action_block_slice(part_tr));
3723 #ifndef NDEBUG
3724 /*------------ find predecessors of bunch_T_a_Bprime ------------*/ mCRL2log(log::debug) << "Splitting off "
3725 << bunch_T_a_Bprime->debug_id(*this) << '\n';
3726 /* Line 2.8: for all B in splittableBlocks(bunch_T_a_Bprime) do */ unsigned const max_splitter_counter(
3727 /* we actually run through the transitions in T--a-->B' */ bunch_T_a_Bprime->max_work_counter(*this));
3728 #endif
3729 bisim_dnj::action_block_entry* splitter_iter(
3730 bunch_T_a_Bprime->begin); assert(splitter_iter < bunch_T_a_Bprime->end);
3731 do
3732 { assert(nullptr != splitter_iter->succ);
3733 bisim_dnj::state_info_entry* const
3734 source(splitter_iter->succ->block_bunch->pred->source); assert(splitter_iter->succ->block_bunch->pred->action_block == splitter_iter);
3735 // Line 2.11: Mark all transitions in bunch_T_a_Bprime
3736 // actually we mark the source state (i.e. register it's in
3737 // R)
3738 bool const first_transition_of_state(
3739 source->bl.ock->mark(source->pos));
3740 // Line 2.9: Add bunch_T_a_Bprime as primary to the splitter
3741 // list
3742 // Line 2.10: Add T_B--> \ bunch_T_a_Bprime as secondary to the
3743 // splitter list
3744 part_tr.first_move_transition_to_new_bunch(splitter_iter,
3745 bunch_T_a_Bprime, first_transition_of_state); // mCRL2complexity(splitter_iter->succ->block_bunch->pred, ...) -- subsumed
3746 // Line 2.13: end for // in the call below
3747 }
3748 while (++splitter_iter < bunch_T_a_Bprime->end);
3749
3750 // We cannot join the loop above with the loop below!
3751
3752 // Line 2.8: for all B in splittableBlocks(T--a-->B') do
3753 splitter_iter = bunch_T_a_Bprime->begin; assert(splitter_iter < bunch_T_a_Bprime->end);
3754 do
3755 {
3756 // Line 2.12: For every state with both marked outgoing
3757 // transitions and outgoing transitions in
3758 // T_B--> \ bunch_T_a_Bprime, mark one such
3759 // transition
3760 part_tr.second_move_transition_to_new_bunch(splitter_iter, ONLY_IF_DEBUG( *this, bunch_T_a_Bprime, )
3761 bunch_T); // mCRL2complexity(splitter_iter->succ->block_bunch->pred, ...) -- subsumed
3762 // Line 2.13: end for // in the call below
3763 }
3764 while (++splitter_iter < bunch_T_a_Bprime->end); mCRL2complexity(bunch_T_a_Bprime,
3765 add_work(check_complexity::refine_partition_until_stable__find_pred,
3766 /*----------------- stabilise the partition again ---------------*/ max_splitter_counter), *this);
3767 ONLY_IF_DEBUG( bisim_dnj::block_bunch_slice_iter_or_null_t
3768 /* Line 2.14: for all T'_B--> in the splitter list (in order) do */ bbslice_T_a_Bprime_B(nullptr); )
3769 while (!part_tr.splitter_list.empty())
3770 {
3771 bisim_dnj::block_bunch_slice_iter_t splitter_Tprime_B( // We have to call mCRL2complexity here because `splitter_Tprime_B` may be
3772 part_tr.splitter_list.begin()); // split up later.
3773 bisim_dnj::block_t* block_B(splitter_Tprime_B->source_block()); assert(!splitter_Tprime_B->is_stable());
3774 bool const is_primary_splitter = 0 < block_B->marked_size(); assert(!splitter_Tprime_B->empty());
3775 #ifndef NDEBUG
3776 bool add_stabilize_to_bottom_transns_succeeded = true;
3777 if (is_primary_splitter)
3778 {
3779 assert(bbslice_T_a_Bprime_B.is_null());
3780 // assign work to this splitter bunch
3781 mCRL2complexity(splitter_Tprime_B, add_work(
3782 check_complexity::refine_partition_until_stable__stabilize,
3783 max_splitter_counter), *this);
3784 }
3785 else if (!bbslice_T_a_Bprime_B.is_null())
3786 {
3787 // assign work to this the corresponding block_bunch-slice of
3788 // bunch_T_a_Bprime
3789 mCRL2complexity(bbslice_T_a_Bprime_B,
3790 add_work(check_complexity::
3791 refine_partition_until_stable__stabilize_for_large_splitter,
3792 max_splitter_counter), *this);
3793 }
3794 else
3795 {
3796 // This must be a refinement to stabilize for new bottom states.
3797 // assign work to the new bottom states in this block_bunch-slice
3798 add_stabilize_to_bottom_transns_succeeded = splitter_Tprime_B->
3799 add_work_to_bottom_transns(check_complexity::
3800 refine_partition_until_stable__stabilize_new_noninert_a_priori,
3801 1U, *this);
3802 }
3803 #endif
3804 if (1 < block_B->size())
3805 {
3806 bisim_dnj::permutation_entry* const
3807 block_B_begin(block_B->begin); assert(block_B_begin->st->pos == block_B_begin);
3808 // Line 2.15: (R, U) := split(B, T'_B-->)
3809 // Line 2.16: Remove T'_B--> from the splitter list
3810 // Line 2.17: Pi_s := Pi_s \ { B } union { R, U } \ { {} }
3811 bisim_dnj::block_t*block_R=split(block_B,splitter_Tprime_B,
3812 is_primary_splitter ? extend_from_marked_states
3813 : extend_from_splitter);
3814 if (block_B_begin < block_R->begin)
3815 {
3816 // The refinement was non-trivial.
3817
3818 // Line 2.18: if T'_B--> was a primary splitter then
3819 if (is_primary_splitter)
3820 { assert(splitter_Tprime_B->bunch == bunch_T_a_Bprime);
3821 // Line 2.19: Remove T_U--> \ T_U--a-->B' from the
3822 // splitter list
3823 bisim_dnj::block_t* const
3824 block_U(block_B_begin->st->bl.ock); assert(block_U->end == block_R->begin);
3825 bisim_dnj::block_bunch_slice_iter_t U_splitter(
3826 part_tr.splitter_list.begin()); assert(0 == block_U->marked_size());
3827 if (part_tr.splitter_list.end() != U_splitter &&
3828 (U_splitter->source_block() == block_U ||
3829 (++U_splitter != part_tr.splitter_list.end() &&
3830 U_splitter->source_block() == block_U)))
3831 { assert(!U_splitter->is_stable());
3832 assert(U_splitter->bunch == bunch_T);
3833 block_U->stable_block_bunch.splice(
3834 block_U->stable_block_bunch.end(),
3835 part_tr.splitter_list, U_splitter);
3836 U_splitter->make_stable();
3837 }
3838 #ifndef NDEBUG
3839 // There should be no block-bunch-slice for the co-splitter that is
3840 // still unstable.
3841 for (bisim_dnj::block_bunch_slice_const_iter_t
3842 iter(part_tr.splitter_list.cbegin());
3843 part_tr.splitter_list.cend() != iter; ++iter)
3844 { assert(!iter->is_stable());
3845 assert(iter->source_block() != block_U);
3846 /* Line 2.20: end if */ }
3847 #endif
3848 }
3849 #ifndef NDEBUG
3850 else
3851 {
3852 // account for work that couldn't be accounted for earlier (because we
3853 // didn't know yet which state would become a new bottom state)
3854 if (!add_stabilize_to_bottom_transns_succeeded)
3855 { assert(splitter_Tprime_B->add_work_to_bottom_transns(
3856 check_complexity::
3857 refine_partition_until_stable__stabilize_new_noninert_a_posteriori,
3858 1U, *this));
3859 }
3860 if (splitter_Tprime_B->work_counter.has_temporary_work())
3861 { assert(splitter_Tprime_B->add_work_to_bottom_transns(
3862 check_complexity::
3863 handle_new_noninert_transns__make_unstable_a_posteriori,
3864 1U, *this));
3865 splitter_Tprime_B->work_counter.reset_temporary_work();
3866 /* Line 2.21: if R--tau-->U is not empty (i. e. R */ }
3867 /* has new non-inert transitions) then */ }
3868 #endif
3869 if (0 < block_R->marked_size())
3870 { ONLY_IF_DEBUG( const bisim_dnj::block_bunch_entry* const splitter_end =
3871 /* Line 2.22: Create a new bunch containing */ splitter_Tprime_B->end; )
3872 // exactly R--tau-->U, add R--tau-->U to
3873 // the splitter list, and mark all its
3874 // transitions
3875 // to
3876 // Line 2.28: For each bottom state, mark one of
3877 // its outgoing transitions in every
3878 // T_N--> where it has one
3879 block_R = handle_new_noninert_transns(
3880 block_R, splitter_Tprime_B);
3881 #ifndef NDEBUG
3882 if (splitter_end[-1].pred->source->bl.ock == block_R)
3883 { assert(!splitter_end[-1].slice.is_null());
3884 splitter_Tprime_B =
3885 (bisim_dnj::block_bunch_slice_iter_t) splitter_end[-1].slice;
3886 }
3887 /* Line 2.29: end if */ assert(nullptr == block_R || splitter_Tprime_B->source_block() == block_R);
3888 #endif
3889 }
3890 }
3891 #ifndef NDEBUG
3892 else
3893 { assert(0 == block_R->marked_size());
3894 assert(add_stabilize_to_bottom_transns_succeeded);
3895 // now splitter must have some transitions that start in bottom states:
3896 if (splitter_Tprime_B->work_counter.has_temporary_work())
3897 { assert(!is_primary_splitter);
3898 assert(splitter_Tprime_B->add_work_to_bottom_transns(
3899 check_complexity::
3900 handle_new_noninert_transns__make_unstable_a_posteriori,
3901 1U, *this));
3902 splitter_Tprime_B->work_counter.reset_temporary_work();
3903 }
3904 }
3905 block_B = block_R;
3906 #endif
3907 }
3908 else
3909 { assert(block_B->nonbottom_begin == block_B->end);
3910 /* A block with 1 state will not be split. However, we */ assert(block_B->marked_nonbottom_begin == block_B->end);
3911 // may have to unmark all states.
3912 block_B->marked_bottom_begin = block_B->end;
3913 block_B->stable_block_bunch.splice(
3914 block_B->stable_block_bunch.end(),
3915 part_tr.splitter_list, splitter_Tprime_B);
3916 splitter_Tprime_B->make_stable(); assert(add_stabilize_to_bottom_transns_succeeded);
3917 #ifndef NDEBUG
3918 // now splitter must have some transitions that start in bottom states:
3919 if (splitter_Tprime_B->work_counter.has_temporary_work())
3920 { assert(!is_primary_splitter);
3921 assert(splitter_Tprime_B->add_work_to_bottom_transns(
3922 check_complexity::
3923 handle_new_noninert_transns__make_unstable_a_posteriori,
3924 1U, *this));
3925 splitter_Tprime_B->work_counter.reset_temporary_work();
3926 }
3927 #endif
3928 }
3929 #ifndef NDEBUG
3930 if (is_primary_splitter && !part_tr.splitter_list.empty() &&
3931 part_tr.splitter_list.front().bunch == bunch_T &&
3932 part_tr.splitter_list.front().source_block() == block_B)
3933 { // The next block_bunch-slice to be handled is the one in the large
3934 // splitter corresponding to the current splitter. In that iteration,
3935 // we will need the current splitter block_bunch-slice.
3936 assert(nullptr != block_B);
3937 assert(splitter_Tprime_B->source_block() == block_B);
3938 assert(splitter_Tprime_B->bunch == bunch_T_a_Bprime);
3939 bbslice_T_a_Bprime_B = splitter_Tprime_B;
3940 }
3941 /* Line 2.30: end for */ else bbslice_T_a_Bprime_B = nullptr;
3942 #endif
3943 }
3944 // Line 2.31: end for
3945 } assert(part_tr.nr_of_bunches == part_tr.nr_of_action_block_slices);
3946 assert(0 == part_tr.nr_of_nontrivial_bunches);
3947
3948 // store the labels with the action_block-slices
3949 // As every action_block-slice is a (trivial) bunch at the same time,
3950 // we can reuse the field next_nontrivial_and_label.label (instead of
3951 // next_nontrivial_and_label.next_nontrivial) to store the label.
3952 const bisim_dnj::action_block_entry*
3953 action_block_iter_end(part_tr.action_block_inert_begin);
3954 label_type label(0); assert(label < action_label.size());
3955 do
3956 {
3957 for (bisim_dnj::action_block_entry*
3958 action_block_iter(action_label[label].begin);
3959 action_block_iter < action_block_iter_end;
3960 action_block_iter = action_block_iter->begin_or_before_end + 1)
3961 { assert(nullptr != action_block_iter->succ);
3962 assert(action_block_iter->succ->block_bunch->pred->action_block ==
3963 action_block_iter);
3964 assert(action_block_iter->succ->bunch()->is_trivial());
3965 action_block_iter->succ->bunch()->
3966 next_nontrivial_and_label.label = label; assert(nullptr != action_block_iter->begin_or_before_end);
3967 assert(action_block_iter <= action_block_iter->begin_or_before_end);
3968 }
3969 }
3970 while (++label < action_label.size() &&
3971 (action_block_iter_end = action_label[label - 1].begin - 1, true));
3972 }
3973
3974 /*----------------- Split -- Algorithm 3 of [JGKW 2020] -----------------*/
3975
4010 bisim_dnj::block_t* split(bisim_dnj::block_t* const block_B,
4011 const bisim_dnj::block_bunch_slice_iter_t splitter_T,
4012 enum refine_mode_t mode)
4013 { assert(block_B == splitter_T->source_block());
4014 #ifndef NDEBUG
4015 mCRL2log(log::debug) << "split("
4016 << block_B->debug_id(*this)
4017 << ',' << splitter_T->debug_id(*this)
4018 << (extend_from_marked_states__add_new_noninert_to_splitter == mode
4019 ? ",extend_from_marked_states__add_new_noninert_to_splitter)\n"
4020 : (extend_from_marked_states == mode
4021 ? ",extend_from_marked_states)\n"
4022 : (extend_from_splitter == mode
4023 ? ",extend_from_splitter)\n"
4024 : ",UNKNOWN MODE)\n")));
4025 #endif
4026 bisim_dnj::block_t* block_R=nullptr; assert(!splitter_T->is_stable()); assert(1 < block_B->size());
4027 union R_s_iter_t
4028 {
4029 bisim_dnj::block_bunch_entry* splitter_iter;
4030 bisim_dnj::permutation_entry* block;
4031 } R_s_iter;
4032
4033 if (extend_from_splitter == mode)
4034 { assert(0 == block_B->marked_size());
4035 // Line 3.2: R := B--Marked(T)--> ; U := Bottom(B) \ R
4036 R_s_iter.splitter_iter = splitter_T->end; assert(splitter_T->marked_begin <= R_s_iter.splitter_iter);
4037 while (splitter_T->marked_begin < R_s_iter.splitter_iter)
4038 { assert(&part_tr.block_bunch.cbegin()[1] < R_s_iter.splitter_iter);
4039 --R_s_iter.splitter_iter;
4040 bisim_dnj::state_info_entry* const
4041 s(R_s_iter.splitter_iter->pred->source); assert(s->bl.ock == block_B); assert(s->pos->st == s);
4042 block_B->mark(s->pos);
4043 // We cannot stop, even if the R-subblock becomes too large,
4044 // because we need to mark all bottom states that are not in U.
4045 }
4046 } else { assert(0 < block_B->marked_size());
4047 assert(splitter_T->marked_begin == splitter_T->end); }
4048 block_B->stable_block_bunch.splice(block_B->stable_block_bunch.end(),
4049 part_tr.splitter_list, splitter_T);
4050 splitter_T->make_stable();
4051
4052 COROUTINES_SECTION
4053 // shared variables of both coroutines
4054 bisim_dnj::permutation_entry*
4055 untested_to_U_defined_end(block_B->nonbottom_begin);
4056 bisim_dnj::permutation_entry*
4057 U_nonbottom_end(untested_to_U_defined_end);
4058
4059 // variable declarations of the U-coroutine
4060 bisim_dnj::permutation_entry* U_s_iter;
4061 bisim_dnj::pred_entry* U_t_iter;
4062 bisim_dnj::state_info_entry* U_t;
4063 const bisim_dnj::succ_entry* U_u_iter;
4064
4065 // variable declarations of the R-coroutine
4066 bisim_dnj::pred_entry* R_t_iter;
4067
4068 COROUTINE_LABELS( (SPLIT_R_PREDECESSOR_HANDLED)
4069 (SPLIT_U_PREDECESSOR_HANDLED)
4070 (SPLIT_R_STATE_HANDLED)
4071 (SPLIT_U_STATE_HANDLED)
4072 (SPLIT_U_TESTING)
4073 (SPLIT_R_COLLECT_SPLITTER))
4074
4075 /*------------------------ find U-states ------------------------*/
4076
4077 COROUTINE
4078 // Line 3.21l: if |U| > |B|/2 then
4079 if(block_B->size() / 2 < block_B->unmarked_bottom_size())
4080 {
4081 // Line 3.22l: Abort this coroutine
4082 ABORT_THIS_COROUTINE();
4083 // Line 3.23l: end if
4084 }
4085 if (0 == block_B->unmarked_bottom_size())
4086 {
4087 // all bottom states are in R, so there cannot be any
4088 // U-states. Unmark all states, as there are no
4089 // transitions that have become non-inert.
4090 block_B->marked_nonbottom_begin = block_B->end;
4091 block_B->marked_bottom_begin = block_B->nonbottom_begin;
4092 block_R = block_B; ONLY_IF_DEBUG( finalise_U_is_smaller(nullptr, block_R, *this); )
4093 TERMINATE_COROUTINE_SUCCESSFULLY();
4094 }
4095
4096 /* - - - - - - - visit U-states - - - - - - - */
4097
4098 if (U_nonbottom_end < block_B->marked_nonbottom_begin)
4099 {
4100 // Line 3.5l: for all s in U while |U| < |B|/2 do
4101 U_s_iter = block_B->begin;
4102 COROUTINE_DO_WHILE (SPLIT_U_STATE_HANDLED,
4103 U_s_iter < U_nonbottom_end)
4104 {
4105 /* Line 3.6l: for all inert transitions t--tau-->s do*/ assert(part_tr.pred.front().target != U_s_iter->st);
4106 COROUTINE_FOR(SPLIT_U_PREDECESSOR_HANDLED,
4107 U_t_iter = U_s_iter->st->pred_inert.begin,
4108 U_t_iter->target == U_s_iter->st, ++U_t_iter)
4109 {
4110 U_t = U_t_iter->source; assert(block_B->nonbottom_begin <= U_t->pos);
4111 /* Line 3.7l: if t in R then Skip state t */ assert(U_t->pos < block_B->end);
4112 if (block_B->marked_nonbottom_begin <= U_t->pos)
4113 {
4114 goto continuation;
4115 }
4116 // Line 3.8l: if untested[t] is undefined then
4117 if (untested_to_U_defined_end <= U_t->pos)
4118 {
4119 // Line 3.9l: untested[t] :=
4120 // |{ t--tau-->u | u in B }|
4121 U_t->untested_to_U_eqv.begin =
4122 U_t->succ_inert.begin;
4123 std::swap(*U_t->pos,
4124 *untested_to_U_defined_end++);
4125 // Line 3.10l: end if
4126 } assert(U_t != part_tr.succ.back().block_bunch->pred->source);
4127 // Line 3.11l: untested[t] := untested[t] − 1
4128 ++U_t->untested_to_U_eqv.begin;
4129 // Line 3.12l: if untested[t]>0 then Skip state t
4130 if (U_t == U_t->untested_to_U_eqv.
4131 begin->block_bunch->pred->source)
4132 {
4133 goto continuation;
4134 }
4135 // Line 3.13l: if not (B--T--> subset R) then
4136 if (extend_from_splitter == mode)
4137 { assert(U_t != part_tr.succ.front().block_bunch->pred->source);
4138 // Line 3.14l: for all non-inert
4139 // t --alpha--> u do
4140 U_u_iter = U_t->succ_inert.begin; assert(&part_tr.succ.front() < U_u_iter);
4141 COROUTINE_WHILE(SPLIT_U_TESTING, U_t ==
4142 U_u_iter[-1].block_bunch->pred->source)
4143 {
4144 U_u_iter=U_u_iter[-1].begin_or_before_end; assert(nullptr != U_u_iter);
4145 /* Line 3.15l: if t --alpha--> u in T */ assert(U_u_iter->block_bunch->pred->source == U_t);
4146 /* then Skip t */ assert(!U_u_iter->block_bunch->slice.is_null());
4147 bisim_dnj::block_bunch_slice_const_iter_t
4148 const block_bunch(
4149 U_u_iter->block_bunch->slice);
4150 if (&*block_bunch == &*splitter_T)
4151 {
4152 goto continuation;
4153 // i. e. break and then continue
4154 } ONLY_IF_DEBUG( bisim_dnj::succ_entry::add_work_to_out_slice(*this, U_u_iter,
4155 /* Line 3.16l: end for */ check_complexity::split_U__test_noninert_transitions, 1U); )
4156 }
4157 END_COROUTINE_WHILE;
4158 // Line 3.17l: end if
4159 } assert(U_nonbottom_end <= U_t->pos);
4160 /* Line 3.18l: Add t to U */ assert(U_t->pos < untested_to_U_defined_end);
4161 std::swap(*U_t->pos, *U_nonbottom_end++);
4162 // Line 3.21l: if |U| > |B|/2 then
4163 if (block_B->size() / 2 <
4164 U_nonbottom_end-block_B->nonbottom_begin +
4165 block_B->unmarked_bottom_size())
4166 {
4167 // Line 3.22l: Abort this coroutine
4168 // As the U-coroutine is now aborted, the
4169 // untested_to_U values are no longer relevant.
4170 // The assignment tells the R-coroutine that it
4171 // doesn't need to make complicated swaps any
4172 // more to keep untested properly initialized.
4173 untested_to_U_defined_end = U_nonbottom_end;
4174 ABORT_THIS_COROUTINE();
4175 // Line 3.23l: end if
4176 }
4177 // Line 3.19l: end for
4178 continuation: mCRL2complexity(U_t_iter, add_work(
4179 check_complexity::split_U__handle_transition_to_U_state, 1U), *this);
4180 }
4181 END_COROUTINE_FOR; mCRL2complexity(U_s_iter->st, add_work(
4182 /* Line 3.20l: end for */ check_complexity::split_U__find_predecessors_of_U_state, 1U), *this);
4183 ++U_s_iter;
4184 if(block_B->marked_bottom_begin == U_s_iter)
4185 {
4186 U_s_iter = block_B->nonbottom_begin;
4187 }
4188 }
4189 END_COROUTINE_DO_WHILE;
4190 }
4191
4192 /*- - - - - - - split off U-block - - - - - - -*/
4193
4194 // Line 3.24l: Abort the other coroutine
4195 ABORT_OTHER_COROUTINE();
4196 // Line 2.17: Pi_s := Pi_s \ { B } union ({ R, U } \ { {} })
4197 // All non-U states are in R.
4198 block_B->marked_nonbottom_begin = U_nonbottom_end;
4199 block_R = block_B;
4200 bisim_dnj::block_t* const block_U(
4201 block_R->split_off_block(bisim_dnj::new_block_is_U, ONLY_IF_DEBUG( *this, )
4202 ONLY_IF_POOL_ALLOCATOR( part_tr.storage, )
4203 part_st.nr_of_blocks++));
4204 // Line 2.16: Remove Tprime_B--> = Tprime_R--> from the
4205 // splitter list
4206 /* and the remainder of Line 2.17 */ assert(0 == block_U->marked_size()); assert(0 == block_R->marked_size());
4207 part_tr.adapt_transitions_for_new_block(block_U, block_R, ONLY_IF_DEBUG( *this, )
4208 extend_from_marked_states__add_new_noninert_to_splitter ==
4209 mode, splitter_T, bisim_dnj::new_block_is_U); ONLY_IF_DEBUG( finalise_U_is_smaller(block_U, block_R, *this); )
4210 END_COROUTINE
4211
4212 /*------------------------ find R-states ------------------------*/
4213
4214 COROUTINE
4215 // Line 3.21r: if |R| > |B|/2 then
4216 if (block_B->size() / 2 < block_B->marked_size())
4217 {
4218 // Line 3.22r: Abort this coroutine
4219 ABORT_THIS_COROUTINE();
4220 // Line 3.23r: end if
4221 }
4222
4223 /* - - - - - collect states from B--T--> - - - - - */
4224
4225 if (extend_from_splitter == mode)
4226 {
4227 // Line 3.4r: R := R union B--(T \ Marked(T))-->
4228 if (U_nonbottom_end < block_B->marked_nonbottom_begin)
4229 { assert(part_tr.block_bunch.front().slice != splitter_T);
4230 COROUTINE_WHILE (SPLIT_R_COLLECT_SPLITTER,
4231 R_s_iter.splitter_iter[-1].slice == splitter_T)
4232 { assert(&part_tr.block_bunch.cbegin()[1] < R_s_iter.splitter_iter);
4233 --R_s_iter.splitter_iter;
4234 bisim_dnj::state_info_entry* const s(
4235 R_s_iter.splitter_iter->pred->source); assert(s->bl.ock == block_B); assert(s->pos->st == s);
4236 if (block_B->nonbottom_begin <= s->pos)
4237 { assert(U_nonbottom_end <= s->pos);
4238 if (s->pos < untested_to_U_defined_end)
4239 {
4240 // The non-bottom state has a transition
4241 // to a visited U-state, so untested is
4242 // initialised; however, now it is
4243 // discovered to be in R anyway.
4244 std::swap(*s->pos,
4245 *--untested_to_U_defined_end);
4246 }
4247 if (block_B->mark_nonbottom(s->pos) &&
4248 // Line 3.21r: if |R| > |B|/2 then
4249 block_B->size()/2 < block_B->marked_size())
4250 {
4251 // Line 3.22r: Abort this coroutine
4252 ABORT_THIS_COROUTINE();
4253 // Line 3.23r: end if
4254 }
4255 } else assert(block_B->marked_bottom_begin <= s->pos);
4256 mCRL2complexity(R_s_iter.splitter_iter->pred, add_work(
4257 check_complexity::split_R__handle_transition_from_R_state, 1U), *this);
4258 }
4259 END_COROUTINE_WHILE;
4260
4261 // Indicate to the U-coroutine that all states in
4262 // B--T--> are now in R.
4263 // The shared variable `mode` is used
4264 // instead of a separate shared variable.
4265 mode = extend_from_marked_states;
4266 }
4267 #ifndef NDEBUG
4268 else
4269 {
4270 // assert that all non-marked transitions in `splitter_T` start in
4271 // marked states
4272 assert(part_tr.block_bunch.front().slice != splitter_T);
4273 while (R_s_iter.splitter_iter[-1].slice == splitter_T)
4274 {
4275 assert(&part_tr.block_bunch.cbegin()[1] < R_s_iter.splitter_iter);
4276 --R_s_iter.splitter_iter;
4277 bisim_dnj::state_info_entry* const
4278 s(R_s_iter.splitter_iter->pred->source);
4279 assert(s->bl.ock == block_B); assert(s->pos->st == s);
4280 assert(s->pos < block_B->nonbottom_begin ||
4281 block_B->marked_nonbottom_begin <= s->pos);
4282 assert(block_B->marked_bottom_begin <= s->pos);
4283 }
4284 }
4285 #endif
4286 }
4287
4288 /* - - - - - - - visit R-states - - - - - - - */ assert(0 != block_B->marked_size());
4289
4290 if (U_nonbottom_end < block_B->marked_nonbottom_begin)
4291 {
4292 // Line 3.5r: for all s in R while |R| < |B|/2 do
4293 R_s_iter.block = block_B->nonbottom_begin;
4294 if (block_B->marked_bottom_begin == R_s_iter.block)
4295 {
4296 // It may happen that all found states are non-bottom
4297 // states. (In that case, some of these states will
4298 // become new bottom states.)
4299 R_s_iter.block = block_B->end;
4300 } assert(block_B->marked_nonbottom_begin != R_s_iter.block);
4301 COROUTINE_DO_WHILE(SPLIT_R_STATE_HANDLED,
4302 block_B->marked_nonbottom_begin != R_s_iter.block)
4303 {
4304 --R_s_iter.block; assert(part_tr.pred.back().target != R_s_iter.block->st);
4