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 <iomanip> // for std::fixed, std::setprecision(), std::setw()
85#include <ctime> // for std::clock_t, std::clock()
86#include "mcrl2/lts/detail/liblts_scc.h"
87#include "mcrl2/lts/detail/liblts_merge.h"
88#include "mcrl2/lts/detail/coroutine.h"
89#include "mcrl2/lts/detail/check_complexity.h"
90#include "mcrl2/lts/detail/fixed_vector.h"
91#include "mcrl2/lts/detail/simple_list.h"
92
93#include <cstddef> // for std::size_t
94
95namespace mcrl2
96{
97namespace lts
98{
99namespace detail
100{
101 #ifndef NDEBUG
107// state_type and trans_type are defined in check_complexity.h. /// mode and to nothing otherwise.
108 #define ONLY_IF_DEBUG(...) __VA_ARGS__
109 #else
110 #define ONLY_IF_DEBUG(...)
111 #endif
115typedef std::size_t label_type;
116
117template <class LTS_TYPE> class bisim_partitioner_dnj;
118
119namespace bisim_dnj
120{
121
133template <class Iterator>
134union iterator_or_counter
135{
137 trans_type count;
138
140 Iterator begin;
141
143 iterator_or_counter() { count = 0; }
144
145
147 void convert_to_iterator(const Iterator other)
148 {
149 new (&begin) Iterator(other);
150 }
151
152
154 ~iterator_or_counter() { begin.~Iterator(); }
155};
156
157
158class block_bunch_entry;
159class action_block_entry;
160
161
162
163
164
165/* ************************************************************************* */
166/* */
167/* R E F I N A B L E P A R T I T I O N */
168/* */
169/* ************************************************************************* */
170
171
172
173
174
183class state_info_entry;
184class permutation_entry;
185
194typedef fixed_vector<permutation_entry> permutation_t;
195
196class block_t;
197class bunch_t;
198
199class pred_entry;
200class succ_entry;
201
202class block_bunch_slice_t;
203typedef simple_list<block_bunch_slice_t>::iterator block_bunch_slice_iter_t;
204typedef simple_list<block_bunch_slice_t>::const_iterator
205 block_bunch_slice_const_iter_t;
206typedef iterator_or_null_t<block_bunch_slice_t>
207 block_bunch_slice_iter_or_null_t;
208
209enum new_block_mode_t { new_block_is_U, new_block_is_R };
210
211
217class state_info_entry
218{
219 public:
227 iterator_or_counter<pred_entry*> pred_inert;
228
236 iterator_or_counter<succ_entry*> succ_inert;
237
244 union bl_t {
245 pred_entry* ed_noninert_end;
246 block_t* ock;
247 } bl;
248
250 permutation_entry* pos;
251
266 iterator_or_counter<succ_entry*> untested_to_U_eqv;
267 #ifndef NDEBUG
269 template<class LTS_TYPE>
270 std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
271 partitioner) const
272 { assert(partitioner.part_st.state_info.data() <= this);
273 assert(this < partitioner.part_st.state_info.data_end());
274 return std::to_string(this - partitioner.part_st.state_info.data());
275 }
276
278 template<class LTS_TYPE>
279 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>&
280 partitioner) const
281 {
282 return "state " + debug_id_short(partitioner);
283 }
284 #endif
285 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
286 mutable check_complexity::state_dnj_counter_t work_counter;
287 #endif
288};
289
290
292class permutation_entry {
293 public:
295 state_info_entry* st;
296
297
299 permutation_entry() = default;
300
301
305 permutation_entry(const permutation_entry&& other) noexcept
306 {
307 st = other.st;
308 }
309
310
316 void operator=(const permutation_entry&& other) noexcept
317 {
318 st = other.st;
319 st->pos = this;
320 }
321};
322
323
347class block_t
348{
349 public:
351 permutation_entry* begin;
352
354 permutation_entry* marked_bottom_begin;
355
357 permutation_entry* nonbottom_begin;
358
360 permutation_entry* marked_nonbottom_begin;
361
363 permutation_entry* end;
364
367 simple_list<block_bunch_slice_t> stable_block_bunch;
368
372 const state_type seqnr;
373
374
381 block_t(permutation_entry* const new_begin,
382 permutation_entry* const new_end, state_type const new_seqnr)
383 : begin(new_begin),
384 marked_bottom_begin(new_end),
385 nonbottom_begin(new_end),
386 marked_nonbottom_begin(new_end),
387 end(new_end),
388 stable_block_bunch(),
389 seqnr(new_seqnr)
390 { assert(new_begin < new_end);
391 }
392
393
395 state_type size() const
396 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
397 assert(marked_bottom_begin <= nonbottom_begin);
398 assert(nonbottom_begin <= marked_nonbottom_begin);
399 return end - begin;
400 }
401
402
404 state_type bottom_size() const
405 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
406 assert(marked_bottom_begin <= nonbottom_begin);
407 assert(nonbottom_begin <= marked_nonbottom_begin);
408 return nonbottom_begin - begin;
409 }
410
411
413 state_type marked_bottom_size() const
414 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
415 assert(marked_bottom_begin <= nonbottom_begin);
416 assert(nonbottom_begin <= marked_nonbottom_begin);
417 return nonbottom_begin - marked_bottom_begin;
418 }
419
420
422 state_type marked_size() const
423 {
424 return end - marked_nonbottom_begin + marked_bottom_size();
425 }
426
427
429 state_type unmarked_bottom_size() const
430 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
431 assert(marked_bottom_begin <= nonbottom_begin);
432 assert(nonbottom_begin <= marked_nonbottom_begin);
433 return marked_bottom_begin - begin;
434 }
435
436
438 state_type unmarked_nonbottom_size() const
439 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
440 assert(marked_bottom_begin <= nonbottom_begin);
441 assert(nonbottom_begin <= marked_nonbottom_begin);
442 return marked_nonbottom_begin - nonbottom_begin;
443 }
444
445
451 bool mark_nonbottom(permutation_entry* const s)
452 { assert(nonbottom_begin <= s); assert(s < end);
453 // assert(this == s->st->bl.ock); -- does not hold during initialisation
454 assert(begin <= marked_bottom_begin);
455 assert(marked_bottom_begin <= nonbottom_begin);
456 assert(nonbottom_begin <= marked_nonbottom_begin);
457 if (marked_nonbottom_begin <= s) { return false; } assert(marked_nonbottom_begin <= end);
458 std::swap(*s, *--marked_nonbottom_begin); assert(nonbottom_begin <= marked_nonbottom_begin);
459 return true;
460 }
461
462
468 bool mark(permutation_entry* const s)
469 { assert(begin <= s);
470 if (s < nonbottom_begin) // assert(this == s->st->bl.ock); -- does not hold during initialisation
471 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
472 assert(nonbottom_begin <= marked_nonbottom_begin);
473 if (marked_bottom_begin <= s) { return false; } assert(marked_bottom_begin <= nonbottom_begin);
474 std::swap(*s, *--marked_bottom_begin); assert(begin <= marked_bottom_begin);
475 return true;
476 }
477 return mark_nonbottom(s);
478 }
479
480
492 ONLY_IF_DEBUG( template<class LTS_TYPE> )
493 block_t* split_off_block(enum new_block_mode_t new_block_mode, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
494 state_type new_seqnr);
495 #ifndef NDEBUG
497 template<class LTS_TYPE>
498 inline std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>&
499 partitioner) const
500 { assert(partitioner.part_st.permutation.data() <= begin);
501 assert(begin < end); assert(begin <= marked_bottom_begin);
502 assert(marked_bottom_begin <= nonbottom_begin);
503 assert(nonbottom_begin <= marked_nonbottom_begin);
504 assert(marked_nonbottom_begin <= end);
505 assert(end <= partitioner.part_st.permutation.data_end());
506 return "block [" +
507 std::to_string(begin - partitioner.part_st.permutation.data()) +
508 "," + std::to_string(end - partitioner.part_st.permutation.data()) +
509 ") (#" + std::to_string(seqnr) + ")";
510 }
511 #endif
512 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
513 mutable check_complexity::block_dnj_counter_t work_counter;
514 #endif
515};
516
517
522class part_state_t
523{
524 public:
529 permutation_t permutation;
530
532 fixed_vector<state_info_entry> state_info;
533
537 state_type nr_of_blocks;
538
545 part_state_t(state_type const num_states)
546 : permutation(num_states),
547 state_info(num_states),
548 nr_of_blocks(0)
549 { assert(0 < num_states);
550 permutation_entry* perm_iter(permutation.data());
551 #ifdef USE_POOL_ALLOCATOR
552 static_assert(std::is_trivially_destructible<block_t>::value);
553 #endif
554 state_info_entry* state_iter(state_info.data()); assert(perm_iter < permutation.data_end());
555 do
556 {
557 state_iter->pos = perm_iter;
558 perm_iter->st = state_iter;
559 }
560 while (++state_iter, ++perm_iter < permutation.data_end()); assert(state_iter == state_info.data_end());
561 }
562
563
564 #ifndef USE_POOL_ALLOCATOR
570 ~part_state_t()
571 { ONLY_IF_DEBUG( state_type deleted_blocks(0); )
572 permutation_entry* perm_iter(permutation.data_end()); assert(permutation.data() < perm_iter);
573 do
574 {
575 block_t* const B(perm_iter[-1].st->bl.ock); assert(B->end == perm_iter);
576 perm_iter = B->begin; ONLY_IF_DEBUG( ++deleted_blocks; )
577 delete B;
578 }
579 while (permutation.data() < perm_iter); assert(deleted_blocks == nr_of_blocks);
580 }
581 #endif
582
583
586 state_type state_size() const { return permutation.size(); }
587
588
592 const block_t* block(state_type const s) const
593 {
594 return state_info[s].bl.ock;
595 }
596 #ifndef NDEBUG
597 private:
605 template<class LTS_TYPE>
606 void print_block(const block_t* const B,
607 const char* const message,
608 const permutation_entry* begin_print,
609 const permutation_entry* const end_print,
610 const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
611 { assert(B->begin <= begin_print); assert(end_print <= B->end);
612 if (end_print == begin_print) return;
613
614 mCRL2log(log::debug) << '\t' << message
615 << (1 < end_print - begin_print ? "s:\n" : ":\n");
616 assert(begin_print < end_print);
617 do
618 {
619 mCRL2log(log::debug) << "\t\t"
620 << begin_print->st->debug_id(partitioner);
621 if (B != begin_print->st->bl.ock)
622 {
623 mCRL2log(log::debug) << ", inconsistent: points "
624 "to " << begin_print->st->bl.ock->debug_id(partitioner);
625 }
626 if (begin_print != begin_print->st->pos)
627 {
628 mCRL2log(log::debug)
629 << ", inconsistent pointer to state_info_entry";
630 }
631 mCRL2log(log::debug) << '\n';
632 }
633 while (++begin_print < end_print);
634 }
635 public:
640 template<class LTS_TYPE>
641 void print_part(const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
642 {
643 if (!mCRL2logEnabled(log::debug)) return;
644 const block_t* B(permutation.front().st->bl.ock);
645 do
646 {
647 mCRL2log(log::debug)<<B->debug_id(partitioner)<<":\n";
648 print_block(B, "Bottom state",
649 B->begin, B->marked_bottom_begin, partitioner);
650 print_block(B, "Marked bottom state",
651 B->marked_bottom_begin, B->nonbottom_begin, partitioner);
652 print_block(B, "Non-bottom state",
653 B->nonbottom_begin, B->marked_nonbottom_begin, partitioner);
654 print_block(B, "Marked non-bottom state",
655 B->marked_nonbottom_begin, B->end, partitioner);
656 // go to next block
657 }
658 while(B->end<permutation.data_end() && (B = B->end->st->bl.ock, true));
659 }
660
664 template<class LTS_TYPE>
665 void assert_consistency(
666 const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
667 {
668 const permutation_entry* perm_iter(permutation.data());
669 state_type true_nr_of_blocks(0);
670 assert(perm_iter < permutation.data_end());
671 do
672 {
673 const block_t* const block(perm_iter->st->bl.ock);
674 // block is consistent:
675 assert(block->begin == perm_iter);
676 assert(block->begin < block->marked_bottom_begin);
677 assert(block->marked_bottom_begin == block->nonbottom_begin);
678 assert(block->nonbottom_begin <= block->marked_nonbottom_begin);
679 assert(block->marked_nonbottom_begin == block->end);
680 assert(partitioner.branching||block->nonbottom_begin==block->end);
681 assert(0 <= block->seqnr);
682 assert(block->seqnr < nr_of_blocks);
683 unsigned const max_block(check_complexity::log_n -
684 check_complexity::ilog2(block->size()));
685 mCRL2complexity(block, no_temporary_work(max_block), partitioner);
686
687 // states in the block are consistent:
688 do
689 {
690 const state_info_entry* const state(perm_iter->st);
691 // assert(part_tr.pred.data() < state->pred_inert.begin);
692 assert(&state_info.back() == state ||
693 state->pred_inert.begin <= state[1].pred_inert.begin);
694 // assert(state->pred_inert.begin < part_tr.pred.data_end());
695 // assert(state->succ_inert.begin < part_tr.succ.data_end());
696 if (perm_iter < block->nonbottom_begin)
697 {
698 assert(&state_info.back() == state || state->
699 succ_inert.begin <= state[1].succ_inert.begin);
700 // assert(state->succ_inert.begin==&part_tr.succ.back() ||
701 // state <
702 // state->succ_inert.begin->block_bunch->pred->source);
703 mCRL2complexity(state, no_temporary_work(max_block, true),
704 partitioner);
705 }
706 else
707 {
708 // assert(state->succ_inert.begin < &part_tr.succ.back());
709 assert(&state_info.back() == state || state->
710 succ_inert.begin < state[1].succ_inert.begin);
711 //assert(state ==
712 // state->succ_inert.begin->block_bunch->pred->source);
713 mCRL2complexity(state, no_temporary_work(max_block, false),
714 partitioner);
715 }
716 assert(block == state->bl.ock);
717 assert(perm_iter == state->pos);
718 }
719 while (++perm_iter < block->end);
720 assert(perm_iter == block->end);
721 ++true_nr_of_blocks;
722 }
723 while (perm_iter < permutation.data_end());
724 assert(nr_of_blocks == true_nr_of_blocks);
725 }
726 #endif
727};
728
730
731
732
733
734 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
735/* ************************************************************************* */ static struct {
736/* */ bool operator()(const iterator_or_counter<action_block_entry*> p1,
737/* T R A N S I T I O N S */ const action_block_entry* const action_block) const
738/* */ {
739/* ************************************************************************* */ return p1.begin > action_block;
740 }
741 } const action_label_greater;
742 #endif
743
744
778
780
782class succ_entry
783{
784 public:
786 block_bunch_entry* block_bunch;
787
796 succ_entry* begin_or_before_end;
797
798
800 succ_entry* out_slice_begin( ONLY_IF_DEBUG( const fixed_vector<succ_entry>& succ )
801 );
802
803
805 bunch_t* bunch() const;
806 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
818 template <class LTS_TYPE>
819 static inline void add_work_to_out_slice(
820 const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
821 const succ_entry* out_slice_begin,
822 enum check_complexity::counter_type ctr, unsigned max_value);
823 #endif
824};
825
826
829class block_bunch_entry
830{
831 public:
833 pred_entry* pred;
834
837 block_bunch_slice_iter_or_null_t slice;
838};
839
840
846class pred_entry
847{
848 public:
850 action_block_entry* action_block;
851
853 state_info_entry* source;
854
856 state_info_entry* target;
857 #ifndef NDEBUG
859 template <class LTS_TYPE>
860 std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
861 partitioner) const
862 {
863 return "from " + source->debug_id_short(partitioner) +
864 " to " + target->debug_id_short(partitioner);
865 }
866
868 template <class LTS_TYPE>
869 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
870 const
871 {
872 // Search for the action label in partitioner.action_label
873 label_type const label(std::lower_bound(
874 partitioner.action_label.cbegin(), partitioner.action_label.cend(),
875 action_block, action_label_greater) -
876 partitioner.action_label.cbegin());
877 assert(label < partitioner.action_label.size());
878 assert(partitioner.action_label[label].begin <= action_block);
879 assert(0==label||action_block<partitioner.action_label[label-1].begin);
880 // class lts_lts_t uses a function pp() to transform the action label
881 // to a string.
882 return pp(partitioner.aut.action_label(label)) + "-transition " +
883 debug_id_short(partitioner);
884 }
885 #endif
886 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
887 mutable check_complexity::trans_dnj_counter_t work_counter;
888 #endif
889};
890
891
894class action_block_entry
895{
896 public:
902 succ_entry* succ;
903
913 action_block_entry* begin_or_before_end;
914
915
917 action_block_entry* action_block_slice_begin( ONLY_IF_DEBUG( const action_block_entry* const action_block_begin,
918 const action_block_entry* const action_block_orig_inert_begin )
919 )
920 {
921 action_block_entry* result(begin_or_before_end); assert(nullptr != result);
922 if (this < result)
923 { assert(this == result->begin_or_before_end);
924 result = this; // The following assertion does not always hold: the function is called
925 } // immediately after a block is refined, so it may be the case that the
926 // transitions are still to be moved to different slices.
927 // assert(succ->block_bunch->pred->target->bl.ock ==
928 // result->succ->block_bunch->pred->target->bl.ock);
929 assert(nullptr != succ); assert(nullptr != result->succ);
930 assert(succ->bunch() == result->succ->bunch());
931 assert(result == action_block_begin || nullptr == result[-1].succ ||
932 action_block_orig_inert_begin <= result ||
933 result[-1].succ->block_bunch->pred->target->bl.ock !=
934 result->succ->block_bunch->pred->target->bl.ock);
935 // assert(this has the same action as result);
936 return result;
937 }
938};
939
940
941class part_trans_t;
942
947class bunch_t
948{
949 public:
951 action_block_entry* begin;
952
954 action_block_entry* end;
955
960 union next_nontrivial_and_label_t
961 {
967 bunch_t* next_nontrivial;
968
970 label_type label;
971
972
974 next_nontrivial_and_label_t()
975 {
976 next_nontrivial = nullptr;
977 }
978 } next_nontrivial_and_label;
979
980
982 bunch_t(action_block_entry* const new_begin,
983 action_block_entry* const new_end)
984 : begin(new_begin),
985 end(new_end),
986 next_nontrivial_and_label()
987 { }
988
989
994 bool is_trivial() const
995 {
996 return nullptr == next_nontrivial_and_label.next_nontrivial;
997 }
998
999
1006 bunch_t* split_off_small_action_block_slice(part_trans_t& part_tr);
1007 #ifndef NDEBUG
1009 template <class LTS_TYPE>
1010 std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
1011 partitioner) const
1012 {
1013 assert(partitioner.part_tr.action_block.data() <= begin);
1014 assert(end <= partitioner.part_tr.action_block_inert_begin);
1015 return "bunch [" + std::to_string(begin -
1016 partitioner.part_tr.action_block.data()) + "," +
1017 std::to_string(end - partitioner.part_tr.action_block.data()) + ")";
1018 }
1019
1021 template <class LTS_TYPE>
1022 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1023 const
1024 { assert(nullptr != end[-1].succ);
1025 const action_block_entry* iter(begin); assert(iter < end);
1026 assert(nullptr != iter->succ);
1027 assert(iter == iter->succ->block_bunch->pred->action_block);
1028 std::string result(debug_id_short(partitioner));
1029 result += " containing transition";
1030 result += iter < end - 1 ? "s " : " ";
1031 result += iter->succ->block_bunch->pred->debug_id_short(partitioner);
1032 ++iter;
1033 if (end <= iter) return result;
1034 while (nullptr == iter->succ) ++iter;
1035 assert(iter < end);
1036 assert(iter == iter->succ->block_bunch->pred->action_block);
1037 result += ", ";
1038 result += iter->succ->block_bunch->pred->debug_id_short(partitioner);
1039 if (iter < end - 3)
1040 {
1041 result += ", ...";
1042 iter = end - 3;
1043 }
1044 while (++iter < end)
1045 {
1046 if (nullptr != iter->succ)
1047 { assert(iter == iter->succ->block_bunch->pred->action_block);
1048 result += ", ";
1049 result += iter->succ->block_bunch->pred->debug_id_short(
1050 partitioner);
1051 }
1052 }
1053 return result;
1054 }
1055 #endif
1056 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1062 template <class LTS_TYPE>
1063 int max_work_counter(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1064 const
1065 {
1066 // verify that the bunch only has a single action label.
1067 // Search for the action label in partitioner.action_label
1068 label_type const label(std::lower_bound(
1069 partitioner.action_label.cbegin(), partitioner.action_label.cend(),
1070 begin, action_label_greater) -
1071 partitioner.action_label.cbegin());
1072 assert(label < partitioner.action_label.size());
1073 assert(partitioner.action_label[label].begin <= begin);
1074 assert(0 == label || begin < partitioner.action_label[label-1].begin);
1075 if (0 == label || end < partitioner.action_label[label - 1].begin)
1076 {
1077 assert(check_complexity::ilog2(end - begin) <=
1078 check_complexity::log_n);
1079 return check_complexity::log_n-check_complexity::ilog2(end-begin);
1080 }
1081 return 0;
1082 }
1083
1084 mutable check_complexity::bunch_dnj_counter_t work_counter;
1085 #endif
1086};
1087
1088
1105class block_bunch_slice_t
1106{
1107 public:
1111 block_bunch_entry* end;
1112
1114 bunch_t* bunch;
1115
1119 block_bunch_entry* marked_begin;
1120
1121
1123 bool is_stable() const { return nullptr == marked_begin; }
1124
1125
1127 void make_stable()
1128 { assert(!is_stable()); assert(!empty());
1129 marked_begin = nullptr;
1130 }
1131
1132
1134 void make_unstable()
1135 { assert(is_stable());
1136 marked_begin = end; assert(!is_stable());
1137 }
1138
1139
1141 block_bunch_slice_t(block_bunch_entry* const new_end,
1142 bunch_t* const new_bunch, bool const new_is_stable)
1143 : end(new_end),
1144 bunch(new_bunch),
1145 marked_begin(nullptr)
1146 {
1147 if (!new_is_stable) make_unstable();
1148 }
1149
1150
1154 bool empty() const
1155 { // assert(std::less(part_tr.block_bunch.data(), end));
1156 // assert(!std::less(part_tr.block_bunch_inert_begin, end));
1157 // assert(part_tr.block_bunch.front().slice != this);
1158 return end[-1].slice != this;
1159 }
1160
1161
1163 block_t* source_block() const
1164 { assert(!empty());
1165 return end[-1].pred->source->bl.ock;
1166 }
1167 #ifndef NDEBUG
1169 template <class LTS_TYPE>
1170 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1171 const
1172 {
1173 static struct {
1174 bool operator()(const block_bunch_entry& p1,
1175 const block_bunch_slice_t* const p2) const
1176 {
1177 return p1.slice != p2;
1178 }
1179 } const block_bunch_not_equal;
1180
1181 assert(partitioner.part_tr.block_bunch.data() < end);
1182 assert(end <= partitioner.part_tr.block_bunch_inert_begin);
1183 std::string const index_string(std::to_string(end -
1184 &partitioner.part_tr.block_bunch.cbegin()[1]));
1185 if (empty())
1186 { //assert(!is_stable());
1187 return "empty block_bunch_slice [" + index_string + "," +
1188 index_string + ")";
1189 }
1190 const block_bunch_entry* begin(
1191 &partitioner.part_tr.block_bunch.cbegin()[1]);
1192 if (trans_type bunch_size(bunch->end - bunch->begin);
1193 (trans_type) (end - begin) > bunch_size)
1194 {
1195 begin = end - bunch_size;
1196 }
1197 begin = std::lower_bound(begin, const_cast<const block_bunch_entry*>
1198 (is_stable() || marked_begin==end ? end-1 : marked_begin),
1199 this, block_bunch_not_equal);
1200 assert(begin->slice == this);
1201 assert(begin[-1].slice != this);
1202 return (is_stable() ? "stable block_bunch-slice ["
1203 : "unstable block_bunch_slice [") +
1204 std::to_string(begin-&partitioner.part_tr.block_bunch.cbegin()[1]) +
1205 "," + index_string + ") containing transitions from " +
1206 source_block()->debug_id(partitioner) +
1207 " in " + bunch->debug_id_short(partitioner);
1208 }
1209 #endif
1210 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1218 template <class LTS_TYPE>
1219 bool add_work_to_bottom_transns(enum check_complexity::
1220 counter_type const ctr, unsigned const max_value,
1221 const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
1222 { assert(!empty());
1223 assert(1U == max_value);
1224 const block_t* const block(source_block());
1225 bool result(false);
1226 const block_bunch_entry* block_bunch(end);
1227 assert(partitioner.part_tr.block_bunch.front().slice != this);
1228 assert(block_bunch[-1].slice == this);
1229 do
1230 {
1231 --block_bunch;
1232 const state_info_entry* const source(block_bunch->pred->source);
1233 assert(source->bl.ock == block);
1234 if (source->pos < block->nonbottom_begin /*&&
1235 // the transition starts in a (new) bottom state
1236 block_bunch->pred->work_counter.counters[ctr -
1237 check_complexity::TRANS_dnj_MIN] != max_value*/)
1238 {
1239 mCRL2complexity(block_bunch->pred, add_work(ctr, max_value),
1240 partitioner);
1241 (void) partitioner; // avoid unused variable warning
1242 result = true;
1243 }
1244 }
1245 while (block_bunch[-1].slice == this);
1246 return result;
1247 }
1248
1249 mutable check_complexity::block_bunch_dnj_counter_t work_counter;
1250 #endif
1251};
1252
1253
1255inline succ_entry* succ_entry::out_slice_begin( ONLY_IF_DEBUG( const fixed_vector<succ_entry>& succ )
1256 )
1257{ assert(nullptr != begin_or_before_end);
1258 succ_entry* result(begin_or_before_end); assert(result->block_bunch->pred->action_block->succ == result);
1259 if (this < result)
1260 { assert(nullptr != result->begin_or_before_end);
1261 assert(this == result->begin_or_before_end);
1262 result = this; assert(result->block_bunch->pred->action_block->succ == result);
1263 } assert(block_bunch->pred->source == result->block_bunch->pred->source);
1264 // assert(this <= result); //< holds always, based on the if() above
1265 assert(nullptr != result->begin_or_before_end);
1266 assert(this <= result->begin_or_before_end);
1267 assert(block_bunch->slice == result->block_bunch->slice);
1268 assert(&succ.cbegin()[1] == result ||
1269 result[-1].block_bunch->pred->source < block_bunch->pred->source ||
1270 result[-1].bunch() != block_bunch->slice->bunch);
1271 return result;
1272}
1273
1274
1276inline bunch_t* succ_entry::bunch() const
1277{
1278 return block_bunch->slice->bunch;
1279}
1280 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1289 template <class LTS_TYPE>
1290 /* static */ inline void succ_entry::add_work_to_out_slice(
1291 const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
1292 const succ_entry* out_slice_begin,
1293 enum check_complexity::counter_type const ctr,unsigned const max_value)
1294 {
1295 const succ_entry* const out_slice_before_end(
1296 out_slice_begin->begin_or_before_end);
1297 assert(nullptr != out_slice_before_end);
1298 assert(out_slice_begin <= out_slice_before_end);
1299 mCRL2complexity(out_slice_begin->block_bunch->pred,
1300 add_work(ctr, max_value), partitioner);
1301 #ifndef NDEBUG
1302 while (++out_slice_begin <= out_slice_before_end)
1303 {
1304 // treat temporary counters specially
1305 mCRL2complexity(out_slice_begin->block_bunch->pred,
1306 add_work_notemporary(ctr, max_value), partitioner);
1307 }
1308 #else
1309 (void) partitioner; (void) out_slice_before_end;
1310 // avoid unused variable warning
1311 #endif
1312 }
1313 #endif
1314class part_trans_t
1315{
1316 public:
1321 fixed_vector<succ_entry> succ;
1322
1327 fixed_vector<block_bunch_entry> block_bunch;
1328
1333 fixed_vector<pred_entry> pred;
1334
1342 fixed_vector<action_block_entry> action_block;
1343
1345 block_bunch_entry* block_bunch_inert_begin;
1346
1348 action_block_entry* action_block_inert_begin;
1349 #ifndef NDEBUG
1351 const action_block_entry* action_block_orig_inert_begin;
1352 #endif
1354 simple_list<block_bunch_slice_t> splitter_list;
1355 private:
1357 bunch_t* first_nontrivial;
1358
1359 public:
1360 #ifdef USE_POOL_ALLOCATOR
1361 static_assert(std::is_trivially_destructible<bunch_t>::value);
1362 #endif
1363
1365 state_type nr_of_new_bottom_states;
1366
1368 trans_type nr_of_bunches;
1369 trans_type nr_of_nontrivial_bunches;
1370 trans_type nr_of_action_block_slices;
1371 trans_type nr_of_block_bunch_slices;
1372
1381 part_trans_t(trans_type num_transitions,
1382 trans_type num_actions)
1383 : succ(num_transitions + 2),
1384 block_bunch(num_transitions + 1),
1385 pred(num_transitions + 2),
1386 action_block(num_transitions + num_actions < 1
1387 ? 0 : num_transitions + num_actions - 1),
1388 block_bunch_inert_begin(block_bunch.data_end()),
1389 action_block_inert_begin(action_block.data_end()),
1390 splitter_list(),
1391 first_nontrivial(nullptr),
1392 nr_of_new_bottom_states(0),
1393 nr_of_bunches(0),
1394 nr_of_nontrivial_bunches(0),
1395 nr_of_action_block_slices(0),
1396 nr_of_block_bunch_slices(0)
1397 {
1398 succ.front().block_bunch = block_bunch.data();
1399 succ.back() .block_bunch = block_bunch.data();
1400 block_bunch.front().pred = pred.data();
1401 block_bunch.front().slice = nullptr;
1402 pred.front().source = nullptr;
1403 pred.front().target = nullptr;
1404 pred.back() .source = nullptr;
1405 pred.back() .target = nullptr;
1406 }
1407
1408
1410 ~part_trans_t()
1411 {
1412 #ifndef USE_POOL_ALLOCATOR
1413 // The destructor also deallocates the bunches, as they are not
1414 // directly referenced from anywhere. This is only necessary if we
1415 // do not use the pool allocator, as the latter will destroy the
1416 // bunches wholesale.
1417 action_block_entry* action_block_iter(action_block.data());
1418 for (;;)
1419 {
1420 do
1421 {
1422 if (action_block_inert_begin <= action_block_iter)
1423 { assert(0 == nr_of_bunches);
1424 return;
1425 }
1426 }
1427 while (nullptr == action_block_iter->succ && ( assert(nullptr == action_block_iter->begin_or_before_end),
1428 ++action_block_iter, true)); assert(nullptr != action_block_iter->begin_or_before_end);
1429 bunch_t* const bunch(action_block_iter->succ->bunch()); assert(bunch->begin == action_block_iter);
1430 action_block_iter = bunch->end;
1431 delete bunch; ONLY_IF_DEBUG( --nr_of_bunches; )
1432 }
1433 /* unreachable */ assert(0);
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 new_block_bunch_pos + 1, bunch_T_a_Bprime, false);
1577 #else
1578 splitter_list.emplace_back(new_block_bunch_pos + 1,
1579 bunch_T_a_Bprime, false);
1580 new_block_bunch_slice = std::prev(splitter_list.end());
1581 #endif
1582 ++nr_of_block_bunch_slices;
1583 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1584 new_block_bunch_slice->work_counter = old_block_bunch_slice->work_counter;
1585 #endif
1586 splitter_list.splice(splitter_list.end(),
1587 source_block->stable_block_bunch, old_block_bunch_slice);
1588 old_block_bunch_slice->make_unstable();
1589 } assert(!new_block_bunch_slice->is_stable());
1590
1591 // move the transition to the end of its block_bunch-slice
1592 if (old_block_bunch_pos < new_block_bunch_pos)
1593 {
1594 std::swap(old_block_bunch_pos->pred, new_block_bunch_pos->pred); assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
1595 old_block_bunch_pos->pred->action_block->succ->block_bunch =
1596 old_block_bunch_pos; assert(new_succ_pos == new_block_bunch_pos->pred->action_block->succ);
1597 new_succ_pos->block_bunch = new_block_bunch_pos;
1598 } else assert(new_block_bunch_pos == old_block_bunch_pos);
1599 assert(new_block_bunch_pos->slice == old_block_bunch_slice);
1600 new_block_bunch_pos->slice = new_block_bunch_slice;
1601
1602 /* adapt the old block_bunch-slice */ assert(new_block_bunch_pos + 1 == old_block_bunch_slice->marked_begin);
1603 old_block_bunch_slice->end = new_block_bunch_pos;
1604 old_block_bunch_slice->marked_begin = new_block_bunch_pos; assert(nullptr != new_block_bunch_pos);
1605 if (old_block_bunch_slice->empty())
1606 { assert(!old_block_bunch_slice->is_stable());
1607 splitter_list.erase(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.data() ||
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.data() ||
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.data() ||
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.data() ||
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 block_t* const old_block,
1772 block_bunch_slice_const_iter_t const splitter_T)
1773 { assert(&succ.cbegin()[1] < out_slice_end);
1774 succ_entry* const out_slice_begin(
1775 out_slice_end[-1].begin_or_before_end); assert(nullptr != out_slice_begin);
1776 assert(out_slice_begin < out_slice_end);
1777 assert(out_slice_begin->block_bunch->pred->action_block->succ ==
1778 out_slice_begin);
1779 block_bunch_entry* old_block_bunch_pos(out_slice_end[-1].block_bunch); assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
1780 assert(!old_block_bunch_pos->slice.is_null());
1781 block_bunch_slice_iter_t const old_block_bunch_slice(
1782 old_block_bunch_pos->slice); assert(old_block_bunch_pos->pred->action_block->succ->block_bunch ==
1783 old_block_bunch_pos);
1784 if (&*splitter_T == &*old_block_bunch_slice) return out_slice_begin;
1785
1786 block_bunch_entry* old_block_bunch_slice_end(
1787 old_block_bunch_slice->end);
1788 state_info_entry* const source(old_block_bunch_pos->pred->source); assert(out_slice_end <= source->succ_inert.begin);
1789 assert(partitioner.part_st.state_info.data() == source ||
1790 source[-1].succ_inert.begin < out_slice_end);
1791 block_t* const new_block(source->bl.ock); assert(source == out_slice_begin->block_bunch->pred->source);
1792 block_bunch_slice_iter_t new_block_bunch_slice; assert(source->pos->st == source);
1793 if (old_block_bunch_slice_end >= block_bunch_inert_begin ||
1794 new_block != old_block_bunch_slice_end->pred->source->bl.ock ||
1795 (new_block_bunch_slice = (block_bunch_slice_iter_t)
1796 old_block_bunch_slice_end->slice, assert(!old_block_bunch_slice_end->slice.is_null()),
1797 old_block_bunch_slice->bunch != new_block_bunch_slice->bunch))
1798 {
1799 // the new block_bunch-slice is not suitable; create a new one and
1800 // insert it into the correct list.
1801 if (old_block_bunch_slice->is_stable())
1802 {
1803 // In most cases, but not always, the source is a bottom state.
1804 #ifdef USE_SIMPLE_LIST
1805 new_block_bunch_slice =
1806 new_block->stable_block_bunch.emplace_front(
1807 old_block_bunch_slice->end,
1808 old_block_bunch_slice->bunch, true);
1809 #else
1810 new_block->stable_block_bunch.emplace_front(
1811 old_block_bunch_slice->end,
1812 old_block_bunch_slice->bunch, true);
1813 new_block_bunch_slice =
1814 new_block->stable_block_bunch.begin();
1815 #endif
1816 }
1817 else
1818 {
1819 #ifdef USE_SIMPLE_LIST
1820 new_block_bunch_slice = splitter_list.emplace_after(
1821 old_block_bunch_slice,
1822 old_block_bunch_slice->end,
1823 old_block_bunch_slice->bunch, false);
1824 #else
1825 new_block_bunch_slice = splitter_list.emplace(
1826 std::next(old_block_bunch_slice),
1827 old_block_bunch_slice->end,
1828 old_block_bunch_slice->bunch, false);
1829 #endif
1830 }
1831 ++nr_of_block_bunch_slices;
1832 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1833 new_block_bunch_slice->work_counter = old_block_bunch_slice->work_counter;
1834 #endif
1835 }
1836 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1837 unsigned max_counter = check_complexity::log_n -
1838 check_complexity::ilog2(new_block->size());
1839 #endif
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 if (old_block_bunch_slice->is_stable())
1912 {
1913 // If the new block is R, then the old (U) block loses
1914 // exactly one stable block_bunch-slice, namely the one we
1915 // just stabilised for (`splitter_T`). We could perhaps
1916 // optimize this by moving that slice as a whole to the new
1917 // block -- perhaps later.
1918 //
1919 // If the new block is U, then the old (R) block loses
1920 // no stable block_bunch-slices if it contains any bottom
1921 // state. If it doesn't contain any bottom state, it will
1922 // definitely keep `splitter_T`, but nothing else can be
1923 // guaranteed.
1924 //
1925 // So old_block_bunch_slice may be deleted, in particular
1926 // if the new block is U, but not exclusively.
1927 old_block->stable_block_bunch.erase(old_block_bunch_slice);
1928 }
1929 else
1930 {
1931 splitter_list.erase(old_block_bunch_slice);
1932 }
1933 --nr_of_block_bunch_slices;
1934 }
1935 return out_slice_begin;
1936 }
1937
1938
1948 void first_move_transition_to_new_action_block(pred_entry* const pred_iter)
1949 {
1950 action_block_entry* const old_action_block_pos(
1951 pred_iter->action_block); assert(nullptr != old_action_block_pos->succ);
1952 assert(old_action_block_pos->succ->block_bunch->pred == pred_iter);
1953 action_block_entry* const action_block_slice_begin(
1954 old_action_block_pos->action_block_slice_begin( ONLY_IF_DEBUG( action_block.data(), action_block_orig_inert_begin )
1955 )); assert(nullptr != action_block_slice_begin->succ);
1956 assert(action_block_slice_begin->succ->block_bunch->pred->action_block ==
1957 action_block_slice_begin);
1958 action_block_entry* const new_action_block_pos(
1959 action_block_slice_begin->begin_or_before_end); assert(nullptr != new_action_block_pos);
1960 assert(action_block_slice_begin == new_action_block_pos->begin_or_before_end);
1961 assert(nullptr != new_action_block_pos->succ);
1962 assert(new_action_block_pos->succ->block_bunch->pred->action_block ==
1963 /* move the transition to the end of the action_block-slice */ new_action_block_pos);
1964 if (old_action_block_pos < new_action_block_pos)
1965 {
1966 succ_entry* const temp(new_action_block_pos->succ); assert(nullptr != temp); assert(nullptr != old_action_block_pos->succ);
1967 new_action_block_pos->succ = old_action_block_pos->succ;
1968 old_action_block_pos->succ = temp;
1969 temp->block_bunch->pred->action_block = old_action_block_pos; assert(pred_iter == new_action_block_pos->succ->block_bunch->pred);
1970 pred_iter->action_block = new_action_block_pos;
1971
1972 // adapt the old action_block-slice immediately
1973 action_block_slice_begin->begin_or_before_end =
1974 new_action_block_pos - 1;
1975 }
1976 else
1977 { assert(old_action_block_pos == new_action_block_pos);
1978 if (action_block_slice_begin < new_action_block_pos)
1979 {
1980 // The old action_block-slice is not empty, so we have to adapt
1981 // the pointer at the beginning. (If it is empty, it may
1982 // happen that `new_action_block_pos - 1` is an illegal value.)
1983 action_block_slice_begin->begin_or_before_end =
1984 new_action_block_pos - 1;
1985 }
1986 else --nr_of_action_block_slices;
1987 } assert(nullptr != new_action_block_pos->succ);
1988 assert(pred_iter == new_action_block_pos->succ->block_bunch->pred);
1989 // adapt the new action_block-slice, as far as is possible now
1990 // make the begin_or_before_end pointers of the first and last
1991 // transition in the slice correct immediately. The other
1992 // begin_or_before_end pointers need to be corrected after all
1993 // transitions in the new bunch have been positioned correctly.
1994 if (new_action_block_pos + 1 >= action_block_inert_begin ||
1995 nullptr == new_action_block_pos[1].succ ||
1996 new_action_block_pos[1].succ->bunch() !=
1997 new_action_block_pos->succ->bunch() ||
1998 new_action_block_pos[1].succ->block_bunch->pred->target->bl.ock !=
1999 pred_iter->target->bl.ock)
2000 {
2001 // This is the first transition that moves to this new
2002 // action_block-slice.
2003 new_action_block_pos->begin_or_before_end = new_action_block_pos;
2004 ++nr_of_action_block_slices;
2005 }
2006 else
2007 {
2008 action_block_entry* const action_block_slice_before_end(
2009 new_action_block_pos[1].begin_or_before_end); assert(nullptr != action_block_slice_before_end);
2010 assert(new_action_block_pos < action_block_slice_before_end);
2011 assert(nullptr != action_block_slice_before_end->succ);
2012 assert(action_block_slice_before_end->succ->block_bunch->pred->action_block ==
2013 action_block_slice_before_end);
2014 assert(new_action_block_pos + 1 ==
2015 action_block_slice_before_end->begin_or_before_end);
2016 action_block_slice_before_end->begin_or_before_end =
2017 new_action_block_pos; assert(action_block_slice_before_end->succ->block_bunch->
2018 pred->target->bl.ock == pred_iter->target->bl.ock);
2019 new_action_block_pos->begin_or_before_end =
2020 action_block_slice_before_end; assert(action_block_slice_before_end < action_block_inert_begin);
2021 }
2022 }
2023
2024
2031 void second_move_transition_to_new_action_block(
2032 pred_entry* const pred_iter)
2033 {
2034 action_block_entry* const new_action_block_pos(
2035 pred_iter->action_block); assert(nullptr != new_action_block_pos->succ);
2036 assert(new_action_block_pos->succ->block_bunch->pred == pred_iter);
2037 action_block_entry* const old_begin_or_before_end(
2038 new_action_block_pos->begin_or_before_end); assert(nullptr != old_begin_or_before_end);
2039 assert(nullptr != old_begin_or_before_end->succ);
2040 assert(old_begin_or_before_end->succ->block_bunch->pred->action_block ==
2041 old_begin_or_before_end);
2042 if (action_block_entry* const new_begin_or_before_end(
2043 old_begin_or_before_end->begin_or_before_end); assert(nullptr != new_begin_or_before_end),
2044 assert(nullptr != new_begin_or_before_end->succ),
2045 assert(new_begin_or_before_end->succ->block_bunch->pred->action_block ==
2046 new_begin_or_before_end),
2047 new_begin_or_before_end < new_action_block_pos)
2048 { assert(old_begin_or_before_end==new_begin_or_before_end->begin_or_before_end);
2049 new_action_block_pos->begin_or_before_end =
2050 new_begin_or_before_end; assert(new_action_block_pos <= old_begin_or_before_end);
2051 return;
2052 } else assert(new_begin_or_before_end == new_action_block_pos);
2053 if (old_begin_or_before_end < new_action_block_pos) return;
2054
2055 // this is the first transition in the new action_block-slice.
2056 // Check whether the bunch it belongs to has become nontrivial.
2057 bunch_t* const bunch(new_action_block_pos->succ->bunch());
2058 if (!bunch->is_trivial()) { return; } assert(old_begin_or_before_end + 1 == bunch->end);
2059 if (bunch->begin < new_action_block_pos)
2060 {
2061 make_nontrivial(bunch);
2062 }
2063 }
2064
2065
2090 bool make_noninert(pred_entry* const old_pred_pos,
2091 block_bunch_slice_iter_or_null_t* const new_noninert_block_bunch_ptr)
2092 {
2093 state_info_entry* const source(old_pred_pos->source); assert(source->pos->st == source);
2094 state_info_entry* const target(old_pred_pos->target); assert(target->pos->st == target);
2095
2096 action_block_entry* const new_action_block_pos(
2097 action_block_inert_begin++); assert(nullptr != new_action_block_pos->succ);
2098 assert(new_action_block_pos->succ->block_bunch->pred->action_block ==
2099 new_action_block_pos);
2100 succ_entry* const new_succ_pos(source->succ_inert.begin++); assert(new_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
2101 block_bunch_entry* const new_block_bunch_pos(
2102 block_bunch_inert_begin++); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
2103 assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
2104 new_block_bunch_pos);
2105 action_block_entry* const old_action_block_pos(
2106 old_pred_pos->action_block); assert(new_action_block_pos <= old_action_block_pos);
2107
2108 succ_entry* const old_succ_pos(old_action_block_pos->succ); assert(nullptr != old_succ_pos);
2109 block_bunch_entry* const old_block_bunch_pos(
2110 old_succ_pos->block_bunch); assert(old_pred_pos == old_block_bunch_pos->pred);
2111 pred_entry* const new_pred_pos(target->pred_inert.begin++); assert(nullptr != new_pred_pos->action_block->succ);
2112 assert(new_pred_pos->action_block->succ->block_bunch->pred == new_pred_pos);
2113
2114 /* adapt action_block */ assert(nullptr == new_action_block_pos->begin_or_before_end);
2115 if (new_action_block_pos < old_action_block_pos)
2116 { assert(nullptr == old_action_block_pos->begin_or_before_end);
2117 old_action_block_pos->succ = new_action_block_pos->succ; assert(nullptr != old_action_block_pos->succ);
2118 assert(old_action_block_pos->succ->block_bunch->pred->action_block ==
2119 new_action_block_pos);
2120 old_action_block_pos->succ->block_bunch->pred->action_block =
2121 old_action_block_pos;
2122 } else assert(new_action_block_pos == old_action_block_pos);
2123 new_action_block_pos->succ = new_succ_pos; assert(nullptr != new_succ_pos);
2124 // new_action_block_pos->begin_or_before_end = ...; -- see below
2125
2126 /* adapt succ */ assert(nullptr == new_succ_pos->begin_or_before_end);
2127 if (new_succ_pos < old_succ_pos)
2128 { assert(nullptr == old_succ_pos->begin_or_before_end);
2129 old_succ_pos->block_bunch = new_succ_pos->block_bunch; assert(old_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
2130 old_succ_pos->block_bunch->pred->action_block->succ = old_succ_pos; assert(nullptr != old_succ_pos);
2131 } else assert(new_succ_pos == old_succ_pos);
2132 new_succ_pos->block_bunch = new_block_bunch_pos;
2133 // new_succ_pos->begin_or_before_end = ...; -- see below
2134
2135 /* adapt block_bunch */ assert(new_block_bunch_pos->slice.is_null());
2136 if (new_block_bunch_pos < old_block_bunch_pos)
2137 { assert(old_block_bunch_pos->slice.is_null());
2138 assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2139 old_block_bunch_pos->pred = new_block_bunch_pos->pred; assert(old_block_bunch_pos->pred->action_block->succ->block_bunch ==
2140 new_block_bunch_pos);
2141 assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2142 old_block_bunch_pos->pred->action_block->succ->block_bunch =
2143 old_block_bunch_pos;
2144 } else assert(new_block_bunch_pos == old_block_bunch_pos);
2145 new_block_bunch_pos->pred = new_pred_pos;
2146 // new_block_bunch_pos->slice = ...; -- see below
2147
2148 // adapt pred
2149 if (new_pred_pos < old_pred_pos)
2150 {
2151 // We need std::swap here to swap the whole content, including
2152 // work counters in case we measure the work.
2153 std::swap(*old_pred_pos, *new_pred_pos); assert(nullptr != old_pred_pos->action_block->succ);
2154 assert(old_pred_pos->action_block->succ->block_bunch->pred == new_pred_pos);
2155 old_pred_pos->action_block->succ->block_bunch->pred = old_pred_pos;
2156 } else assert(new_pred_pos == old_pred_pos);
2157 new_pred_pos->action_block = new_action_block_pos;
2158
2159 /* make the state a bottom state if necessary */ assert(source->bl.ock->nonbottom_begin <= source->pos);
2160 bool became_bottom(false); assert(succ.back().block_bunch->pred->source != source);
2161 if (source != source->succ_inert.begin->block_bunch->pred->source)
2162 {
2163 block_t* const source_block(source->bl.ock);
2164 // make the state a marked bottom state
2165 if (source->pos >= source_block->marked_nonbottom_begin)
2166 {
2167 std::swap(*source->pos,
2168 *source_block->marked_nonbottom_begin++);
2169 } assert(source->pos < source_block->marked_nonbottom_begin);
2170 std::swap(*source->pos, *source_block->nonbottom_begin++);
2171 ++nr_of_new_bottom_states;
2172 became_bottom = true;
2173 }
2174
2175 bunch_t* new_noninert_bunch; assert(nullptr != new_action_block_pos);
2176 if (!new_noninert_block_bunch_ptr->is_null())
2177 {
2178 // There is already some new non-inert transition from this block.
2179 // So we can reuse this block_bunch and its bunch.
2180 // (However, it may be the case that the current transition goes to
2181 // another block; in the latter case, we have to create a new
2182 // action_block-slice.)
2183
2184 // extend the bunch
2185 new_noninert_bunch = (*new_noninert_block_bunch_ptr)->bunch; assert(new_action_block_pos >= new_noninert_bunch->end);
2186 ONLY_IF_DEBUG(
2187 for (const action_block_entry*temp_action_block_pos=new_action_block_pos ;
2188 temp_action_block_pos > new_noninert_bunch->end ; )
2189 {
2190 assert(nullptr == (--temp_action_block_pos)->succ);
2191 }
2192 )
2193 new_noninert_bunch->end = action_block_inert_begin;
2194 /* extend the block_bunch-slice */ assert((*new_noninert_block_bunch_ptr)->end == new_block_bunch_pos);
2195 (*new_noninert_block_bunch_ptr)->end = block_bunch_inert_begin;
2196 if (!(*new_noninert_block_bunch_ptr)->is_stable())
2197 { assert((*new_noninert_block_bunch_ptr)->marked_begin == new_block_bunch_pos);
2198 (*new_noninert_block_bunch_ptr)->marked_begin =
2199 block_bunch_inert_begin;
2200 }
2201 new_block_bunch_pos->slice = *new_noninert_block_bunch_ptr;
2202
2203 /* adapt the action_block-slice */ assert(new_noninert_bunch->begin < new_action_block_pos);
2204 if (nullptr != new_action_block_pos[-1].succ &&
2205 target->bl.ock == new_action_block_pos[-1].
2206 succ->block_bunch->pred->target->bl.ock)
2207 {
2208 // the action_block-slice is suitable: extend it
2209 action_block_entry* const action_block_slice_begin(
2210 new_action_block_pos[-1].begin_or_before_end); assert(nullptr != action_block_slice_begin);
2211 assert(new_action_block_pos-1==action_block_slice_begin->begin_or_before_end);
2212 assert(nullptr != action_block_slice_begin->succ);
2213 assert(action_block_slice_begin->succ->block_bunch->pred->action_block ==
2214 action_block_slice_begin);
2215 action_block_slice_begin->begin_or_before_end =
2216 new_action_block_pos;
2217 new_action_block_pos->begin_or_before_end =
2218 action_block_slice_begin;
2219 }
2220 else
2221 {
2222 // create a new action_block-slice
2223 new_action_block_pos->begin_or_before_end=new_action_block_pos;
2224 if (new_noninert_bunch->is_trivial())
2225 { // Only during initialisation, it may happen that we add new non-inert
2226 make_nontrivial(new_noninert_bunch); // transitions to a nontrivial bunch:
2227 }
2228 #ifndef NDEBUG
2229 else
2230 {
2231 // We make sure that new_noninert_bunch is the first bunch in
2232 // action_block (and because it's always the last one, it will be the
2233 // only one, so there is only one bunch, as ).
2234 for (const action_block_entry* iter = action_block.data();
2235 iter < new_noninert_bunch->begin; ++iter)
2236 {
2237 assert(nullptr == iter->succ);
2238 assert(nullptr == iter->begin_or_before_end);
2239 }
2240 }
2241 #endif
2242 ++nr_of_action_block_slices;
2243 }
2244
2245 /* adapt the out-slice */ assert(source != succ.front().block_bunch->pred->source);
2246 if (source == new_succ_pos[-1].block_bunch->pred->source &&
2247 new_succ_pos[-1].bunch() == new_noninert_bunch)
2248 {
2249 // the out-slice is suitable: extend it.
2250 succ_entry* const out_slice_begin(
2251 new_succ_pos[-1].begin_or_before_end); assert(nullptr != out_slice_begin);
2252 assert(new_succ_pos - 1 == out_slice_begin->begin_or_before_end);
2253 out_slice_begin->begin_or_before_end = new_succ_pos; assert(out_slice_begin->block_bunch->pred->action_block->succ ==
2254 out_slice_begin);
2255 new_succ_pos->begin_or_before_end = out_slice_begin;
2256 return became_bottom;
2257 }
2258 }
2259 else
2260 {
2261 // create a new bunch for noninert transitions
2262 new_noninert_bunch =
2263 #ifdef USE_POOL_ALLOCATOR
2264 simple_list<block_bunch_slice_t>::get_pool().
2265 template construct<bunch_t>
2266 #else
2267 new bunch_t
2268 #endif
2269 (new_action_block_pos, action_block_inert_begin);
2270 ++nr_of_bunches;
2271
2272 // create a new block_bunch-slice
2273 #ifdef USE_SIMPLE_LIST
2274 block_bunch_slice_iter_t new_noninert_block_bunch(
2275 splitter_list.emplace_back(
2276 block_bunch_inert_begin, new_noninert_bunch, false));
2277 #else
2278 splitter_list.emplace_back(block_bunch_inert_begin,
2279 new_noninert_bunch, false);
2280 block_bunch_slice_iter_t new_noninert_block_bunch(
2281 std::prev(splitter_list.end()));
2282 #endif
2283 ++nr_of_block_bunch_slices;
2284 new_block_bunch_pos->slice = new_noninert_block_bunch;
2285 *new_noninert_block_bunch_ptr = new_noninert_block_bunch;
2286
2287 // create a new action_block-slice
2288 new_action_block_pos->begin_or_before_end = new_action_block_pos;
2289 ++nr_of_action_block_slices;
2290 } assert(&succ.cbegin()[1] == new_succ_pos ||
2291 new_succ_pos[-1].block_bunch->pred->source < source ||
2292 /* create a new out-slice */ new_succ_pos[-1].bunch() != new_noninert_bunch);
2293 new_succ_pos->begin_or_before_end = new_succ_pos;
2294 return became_bottom;
2295 }
2296
2297
2298 public:
2320 ONLY_IF_DEBUG( template<class LTS_TYPE> )
2321 void adapt_transitions_for_new_block(
2322 block_t* const new_block,
2323 block_t* const old_block, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
2324 bool const add_new_noninert_to_splitter,
2325 const block_bunch_slice_iter_t splitter_T,
2326 enum new_block_mode_t const new_block_mode)
2327 { assert(splitter_T->is_stable());
2328 // We begin with a bottom state so the new block gets a sorted list of
2329 // stable block_bunch-slices.
2330 permutation_entry* s_iter(new_block->begin); assert(s_iter < new_block->end);
2331 do
2332 {
2333 state_info_entry* const s(s_iter->st); assert(new_block == s->bl.ock);
2334 assert(s->pos == s_iter);
2335 /* - - - - - - adapt part_tr.block_bunch - - - - - - */
2336 assert(s != succ.front().block_bunch->pred->source);
2337 for (succ_entry* succ_iter(s->succ_inert.begin);
2338 s == succ_iter[-1].block_bunch->pred->source; )
2339 {
2340 succ_iter = move_out_slice_to_new_block(succ_iter, ONLY_IF_DEBUG( partitioner, )
2341 old_block, splitter_T); assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
2342 assert(s == succ_iter->block_bunch->pred->source);
2343 // add_work_to_out_slice(succ_iter, ...) -- subsumed in the call below
2344 }
2345
2346 /*- - - - - - adapt part_tr.action_block - - - - - -*/
2347 assert(s != pred.front().target);
2348 for (pred_entry* pred_iter(s->pred_inert.begin);
2349 s == (--pred_iter)->target; )
2350 { assert(pred.data() < pred_iter);
2351 assert(nullptr != pred_iter->action_block->succ);
2352 assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
2353 first_move_transition_to_new_action_block(pred_iter); // mCRL2complexity(pred_iter, ...) -- subsumed in the call below
2354 } // mCRL2complexity(s, ...) -- subsumed in the call at the end
2355 }
2356 while (++s_iter < new_block->end);
2357
2358 if (new_block_is_R == new_block_mode)
2359 { assert(splitter_T->source_block() == new_block);
2360 // The `splitter_T` slice moves completely from the old to the new
2361 // block. We move it as a whole to the new block_bunch list.
2362 new_block->stable_block_bunch.splice(
2363 new_block->stable_block_bunch.begin(),
2364 old_block->stable_block_bunch, splitter_T);
2365 } else assert(splitter_T->source_block() == old_block);
2366
2367 // We cannot join the loop above with the one below because transitions
2368 // in the action_block-slices need to be handled in two phases.
2369
2370 s_iter = new_block->begin; assert(s_iter < new_block->end);
2371 do
2372 {
2373 state_info_entry* const s(s_iter->st); assert(s->pos == s_iter); assert(s != pred.front().target);
2374 for (pred_entry* pred_iter(s->pred_inert.begin);
2375 s == (--pred_iter)->target; )
2376 { assert(pred.data() < pred_iter);
2377 assert(nullptr != pred_iter->action_block->succ);
2378 assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
2379 second_move_transition_to_new_action_block(pred_iter); // mCRL2complexity(pred_iter, ...) -- subsumed in the call below
2380 } // mCRL2complexity(s, ...) -- subsumed in the call at the end
2381 }
2382 while (++s_iter < new_block->end);
2383 assert(0 == new_block->marked_size()); assert(0 == old_block->marked_size());
2384 /* - - - - - - find new non-inert transitions - - - - - - */ assert(block_bunch.data_end() - block_bunch_inert_begin ==
2385 action_block.data_end() - action_block_inert_begin);
2386 if (block_bunch_inert_begin < block_bunch.data_end())
2387 {
2388 block_bunch_slice_iter_or_null_t new_noninert_block_bunch;
2389 if (add_new_noninert_to_splitter)
2390 {
2391 new_noninert_block_bunch = splitter_T;
2392 }
2393 else
2394 {
2395 new_noninert_block_bunch = nullptr;
2396 }
2397 if (new_block_is_U == new_block_mode)
2398 { assert(old_block == new_block->end->st->bl.ock);
2399 assert(new_block->end < partitioner.part_st.permutation.data_end());
2400 permutation_entry* target_iter(new_block->begin); assert(target_iter < new_block->end);
2401 do
2402 {
2403 state_info_entry* const s(target_iter->st); assert(s->pos == target_iter);
2404 // check all incoming inert transitions of s, whether they
2405 /* still start in new_block */ assert(s != pred.back().target);
2406 for (pred_entry* pred_iter(s->pred_inert.begin);
2407 s == pred_iter->target; ++pred_iter)
2408 { assert(pred_iter < &pred.back());
2409 assert(nullptr != pred_iter->action_block->succ);
2410 state_info_entry* const t(pred_iter->source); assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
2411 assert(t->pos->st == t);
2412 if (new_block != t->bl.ock)
2413 { assert(old_block == t->bl.ock);
2414 if (!make_noninert(pred_iter,
2415 &new_noninert_block_bunch))
2416 // make_noninert() may modify *pred_iter
2417 {
2418 old_block->mark_nonbottom(t->pos);
2419 }
2420 } // mCRL2complexity(old value of *pred_iter, ...) -- overapproximated by the
2421 // call below
2422 } // mCRL2complexity(s, ...) -- subsumed in the call at the end
2423 }
2424 while (++target_iter < new_block->end); assert(0 < old_block->bottom_size());
2425 }
2426 else
2427 { assert(new_block_is_R == new_block_mode);
2428 /* We have to be careful because make_noninert may move */ assert(partitioner.part_st.permutation.data() < new_block->begin);
2429 /* a state either forward (to the marked states) or */ assert(old_block == new_block->begin[-1].st->bl.ock);
2430 /* back (to the bottom states). */ assert(0 < old_block->bottom_size());
2431 for(permutation_entry* source_iter(new_block->nonbottom_begin);
2432 source_iter < new_block->marked_nonbottom_begin; )
2433 {
2434 state_info_entry* const s(source_iter->st); assert(s->pos == source_iter);
2435 // check all outgoing inert transitions of s, whether they
2436 /* still end in new_block. */ assert(succ.back().block_bunch->pred->source != s);
2437 succ_entry* succ_iter(s->succ_inert.begin); assert(succ_iter < &succ.back());
2438 bool dont_mark(true); assert(s == succ_iter->block_bunch->pred->source);
2439 do
2440 { assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
2441 if (new_block !=
2442 succ_iter->block_bunch->pred->target->bl.ock)
2443 { assert(old_block == succ_iter->block_bunch->pred->target->bl.ock);
2444 dont_mark = make_noninert(
2445 succ_iter->block_bunch->pred,
2446 &new_noninert_block_bunch);
2447 } // mCRL2complexity(succ_iter->block_bunch->pred, ...) -- overapproximated by
2448 // the call below
2449 }
2450 while (s == (++succ_iter)->block_bunch->pred->source);
2451 if (dont_mark) ++source_iter;
2452 else
2453 { assert(s->pos == source_iter);
2454 new_block->mark_nonbottom(source_iter);
2455 } assert(new_block->nonbottom_begin <= source_iter);
2456 // mCRL2complexity(s, ...) -- overapproximated by the call at the end
2457 }
2458 }
2459 } else assert(block_bunch_inert_begin == block_bunch.data_end());
2460 mCRL2complexity(new_block, add_work(check_complexity::
2461 adapt_transitions_for_new_block, check_complexity::log_n -
2462 check_complexity::ilog2(new_block->size())), partitioner);
2463 }
2464 #ifndef NDEBUG
2467 template <class LTS_TYPE>
2468 void print_trans(const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
2469 {
2470 if (!mCRL2logEnabled(log::debug)) return;
2471 // print all outgoing transitions grouped per successor and out-slice
2472 const succ_entry* succ_iter(&succ.cbegin()[1]);
2473 if (succ_iter >= &succ.back())
2474 {
2475 mCRL2log(log::debug) << "No transitions.\n";
2476 return;
2477 }
2478 const state_info_entry* source(succ_iter->block_bunch->pred->source);
2479 mCRL2log(log::debug) << source->debug_id(partitioner) << ":\n";
2480 if (succ_iter->block_bunch->slice.is_null())
2481 {
2482 mCRL2log(log::debug) << "\tInert successors:\n";
2483 }
2484 block_bunch_slice_iter_or_null_t current_out_bunch(nullptr);
2485 do
2486 {
2487 bool always_print=false;
2488 if (source != succ_iter->block_bunch->pred->source)
2489 { assert(source < succ_iter->block_bunch->pred->source);
2490 source = succ_iter->block_bunch->pred->source;
2491 mCRL2log(log::debug)
2492 << source->debug_id(partitioner) << ":\n";
2493 always_print=true;
2494 }
2495 if (always_print ||
2496 succ_iter->block_bunch->slice != current_out_bunch)
2497 { //assert(!current_out_bunch.is_null());
2498 if (succ_iter->block_bunch->slice.is_null())
2499 { assert(succ_iter == source->succ_inert.begin);
2500 mCRL2log(log::debug)<<"\tInert successors:\n";
2501 current_out_bunch = nullptr;
2502 }
2503 else
2504 { assert(succ_iter < source->succ_inert.begin);
2505 //assert(!current_out_bunch.is_null());
2506 //assert(current_out_bunch == splitter_list.end() ||
2507 // current_out_bunch->bunch != succ_iter->bunch());
2508 mCRL2log(log::debug) << "\tSuccessors in "
2509 <<succ_iter->bunch()->debug_id_short(partitioner)<<":\n";
2510 current_out_bunch = succ_iter->block_bunch->slice;
2511 }
2512 }
2513 mCRL2log(log::debug) << "\t\t"
2514 << succ_iter->block_bunch->pred->debug_id(partitioner) << '\n';
2515 }
2516 while (++succ_iter < &succ.back());
2517
2518 // print all transitions grouped per bunch and action_block-slice
2519 const action_block_entry* action_block_iter(action_block.data());
2520 do assert(action_block_iter < action_block.data_end());
2521 while (nullptr == action_block_iter->succ &&
2522 (assert(nullptr == action_block_iter->begin_or_before_end),
2523 ++action_block_iter, true));
2524 do
2525 {
2526 const action_block_entry* bunch_end;
2527 const action_block_entry* action_block_slice_end;
2528 assert(nullptr != action_block_iter->succ);
2529 if (action_block_iter->succ->block_bunch->slice.is_null())
2530 { assert(action_block_iter == action_block_inert_begin);
2531 mCRL2log(log::debug) <<"Inert transition slice [";
2532 action_block_slice_end = bunch_end = action_block.data_end();
2533 }
2534 else
2535 {
2536 const bunch_t* const bunch(action_block_iter->succ->bunch());
2537 assert(nullptr != bunch);
2538 mCRL2log(log::debug) << bunch->debug_id_short(
2539 partitioner) << ":\n\taction_block-slice [";
2540 assert(bunch->begin == action_block_iter);
2541 bunch_end = bunch->end;
2542 assert(bunch_end <= action_block_inert_begin);
2543 assert(nullptr != action_block_iter->begin_or_before_end);
2544 action_block_slice_end =
2545 action_block_iter->begin_or_before_end + 1;
2546 }
2547 assert(action_block_slice_end <= bunch_end);
2548 // for all action_block-slices in bunch
2549 for (;;)
2550 {
2551 mCRL2log(log::debug) << (action_block_iter -
2552 action_block.data()) << ","
2553 << (action_block_slice_end - action_block.data()) << "):\n";
2554 // for all transitions in the action_block-slice
2555 assert(action_block_iter < action_block_slice_end);
2556 do
2557 {
2558 assert(nullptr != action_block_iter->succ);
2559 mCRL2log(log::debug) << "\t\t"
2560 << action_block_iter->succ->block_bunch->
2561 pred->debug_id(partitioner) << '\n';
2562 }
2563 while (++action_block_iter < action_block_slice_end);
2564 // go to next action_block-slice in the same bunch
2565 while (action_block_iter < bunch_end &&
2566 nullptr == action_block_iter->succ)
2567 {
2568 assert(nullptr == action_block_iter->begin_or_before_end);
2569 ++action_block_iter;
2570 assert(action_block_iter < bunch_end);
2571 }
2572 if (action_block_iter >= bunch_end) break;
2573 assert(nullptr != action_block_iter->begin_or_before_end);
2574 action_block_slice_end =
2575 action_block_iter->begin_or_before_end + 1;
2576 mCRL2log(log::debug) << "\taction_block-slice [";
2577 }
2578 // go to next bunch
2579 assert(action_block_iter == bunch_end);
2580 while (action_block_iter < action_block.data_end() &&
2581 nullptr == action_block_iter->succ)
2582 {
2583 assert(nullptr == action_block_iter->begin_or_before_end);
2584 ++action_block_iter;
2585 }
2586 }
2587 while (action_block_iter < action_block.data_end());
2588 }
2589 #endif
2590};
2591
2592
2602 ONLY_IF_DEBUG( template<class LTS_TYPE> )
2603inline block_t* block_t::split_off_block(
2604 enum new_block_mode_t const new_block_mode, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
2605 state_type const new_seqnr)
2606{ assert(0 < marked_size()); assert(0 < unmarked_bottom_size());
2607 // create a new block
2608 block_t* new_block;
2609 state_type swapcount(std::min(marked_bottom_size(),
2610 unmarked_nonbottom_size()));
2611 if (permutation_entry* const splitpoint(marked_bottom_begin +
2612 unmarked_nonbottom_size()); assert(begin < splitpoint), assert(splitpoint < end),
2613 assert(splitpoint->st->pos == splitpoint),
2614 new_block_is_U == new_block_mode)
2615 { assert((state_type) (splitpoint - begin) <= size()/2);
2616 new_block =
2617 #ifdef USE_POOL_ALLOCATOR
2618 simple_list<block_bunch_slice_t>::get_pool().
2619 template construct<block_t>
2620 #else
2621 new block_t
2622 #endif
2623 (begin, splitpoint, new_seqnr);
2624 new_block->nonbottom_begin = marked_bottom_begin;
2625
2626 // adapt the old block: it only keeps the R-states
2627 begin = splitpoint;
2628 nonbottom_begin = marked_nonbottom_begin;
2629 }
2630 else
2631 { assert(new_block_is_R == new_block_mode);
2632 new_block =
2633 #ifdef USE_POOL_ALLOCATOR
2634 simple_list<block_bunch_slice_t>::get_pool().
2635 template construct<block_t>
2636 #else
2637 new block_t
2638 #endif
2639 (splitpoint, end, new_seqnr);
2640 new_block->nonbottom_begin = marked_nonbottom_begin; assert((state_type) (end - splitpoint) <= size()/2);
2641
2642 // adapt the old block: it only keeps the U-states
2643 end = splitpoint;
2644 nonbottom_begin = marked_bottom_begin;
2645 }
2646 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2647 /* swap contents */ new_block->work_counter = work_counter;
2648 #endif
2649 // The structure of a block is
2650 // | unmarked | marked | unmarked | marked |
2651 // | bottom | bottom | non-bottom | non-bottom |
2652 // We have to swap the marked bottom with the unmarked non-bottom
2653 // states.
2654 //
2655 // It is not necessary to reset the untested_to_U counters; these
2656 // counters are anyway only valid for the states in the respective
2657 // slice.
2658
2659 if (0 < swapcount)
2660 {
2661 // vector swap the states:
2662 permutation_entry* pos1(marked_bottom_begin);
2663 permutation_entry* pos2(marked_nonbottom_begin); assert(pos1 < pos2);
2664 permutation_entry const temp(std::move(*pos1));
2665 for (;;)
2666 {
2667 --pos2; assert(pos1 < pos2);
2668 *pos1 = std::move(*pos2);
2669 ++pos1;
2670 if (0 >= --swapcount) { break; } assert(pos1 < pos2);
2671 *pos2 = std::move(*pos1); // mCRL2complexity(new_block_is_U == new_block_mode ? pos1[-1] : *pos2, ...)
2672 } // -- overapproximated by the call at the end
2673 *pos2 = std::move(temp); // mCRL2complexity(new_block_is_U == new_block_mode ? pos1[-1] : *pos2, ...)
2674 } // -- overapproximated by the call at the end
2675 #ifndef NDEBUG
2676 { const permutation_entry* s_iter(begin); assert(s_iter < end);
2677 do assert(s_iter->st->pos == s_iter);
2678 while (++s_iter < end); }
2679 #endif
2680 // unmark all states in both blocks
2681 marked_nonbottom_begin = end;
2682 marked_bottom_begin = nonbottom_begin;
2683 new_block->marked_bottom_begin = new_block->nonbottom_begin; assert(new_block->size() <= size());
2684
2685 /* set the block pointer of states in the new block */ assert(new_block->marked_nonbottom_begin == new_block->end);
2686 permutation_entry* s_iter(new_block->begin); assert(s_iter < new_block->end);
2687 do
2688 { assert(s_iter->st->pos == s_iter);
2689 s_iter->st->bl.ock = new_block; // mCRL2complexity (*s_iter, ...) -- subsumed in the call below
2690 }
2691 while (++s_iter < new_block->end); mCRL2complexity(new_block, add_work(check_complexity::split_off_block,
2692 check_complexity::log_n - check_complexity::ilog2(new_block->size())),
2693 partitioner);
2694 return new_block;
2695}
2696
2697
2708inline bunch_t* bunch_t::split_off_small_action_block_slice(
2709 part_trans_t& part_tr)
2710{ assert(begin < end); assert(nullptr != begin->succ);
2711 assert(nullptr != begin->begin_or_before_end);
2712 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);
2713 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);
2714 bunch_t* bunch_T_a_Bprime;
2715 /* 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);
2716 /* |T--a-->B'| < 1/2 |T| */ assert(nullptr != last_slice_begin->succ);
2717 if (first_slice_end - begin > end - last_slice_begin)
2718 {
2719 // Line 2.7: Pi_t := Pi_t \ {T} union { T--a-->B', T \ T--a-->B' }
2720 bunch_T_a_Bprime =
2721 #ifdef USE_POOL_ALLOCATOR
2722 simple_list<block_bunch_slice_t>::get_pool().
2723 template construct<bunch_t>
2724 #else
2725 new bunch_t
2726 #endif
2727 (last_slice_begin, end); assert(nullptr != bunch_T_a_Bprime);
2728 end = last_slice_begin;
2729 while (nullptr == end[-1].succ)
2730 {
2731 --end; assert(first_slice_end <= end); assert(nullptr == end->begin_or_before_end);
2732 } assert(nullptr != end[-1].begin_or_before_end);
2733 if (first_slice_end == end) part_tr.make_trivial(this);
2734 }
2735 else
2736 {
2737 // Line 2.7: Pi_t := Pi_t \ {T} union { T--a-->B', T \ T--a-->B' }
2738 bunch_T_a_Bprime =
2739 #ifdef USE_POOL_ALLOCATOR
2740 simple_list<block_bunch_slice_t>::get_pool().
2741 template construct<bunch_t>
2742 #else
2743 new bunch_t
2744 #endif
2745 (begin, first_slice_end); assert(nullptr != bunch_T_a_Bprime);
2746 begin = first_slice_end;
2747 while (nullptr == begin->succ)
2748 { assert(nullptr == begin->begin_or_before_end);
2749 ++begin; assert(begin <= last_slice_begin);
2750 } assert(nullptr != begin->begin_or_before_end);
2751 if (begin == last_slice_begin) part_tr.make_trivial(this);
2752 }
2753 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2754 bunch_T_a_Bprime->work_counter = work_counter;
2755 #endif
2756 ++part_tr.nr_of_bunches;
2757 return bunch_T_a_Bprime;
2758}
2760
2761} // end namespace bisim_dnj
2762
2763
2764
2765
2766
2767/* ************************************************************************* */
2768/* */
2769/* A L G O R I T H M S */
2770/* */
2771/* ************************************************************************* */
2772
2773
2774
2775
2776
2780
2781
2782
2783/*=============================================================================
2784= main class =
2785=============================================================================*/
2786
2787
2788
2789
2790
2794template <class LTS_TYPE>
2795class bisim_partitioner_dnj
2796{
2797 private:
2799 enum refine_mode_t{extend_from_marked_states,
2800 extend_from_marked_states__add_new_noninert_to_splitter,
2801 extend_from_splitter };
2802
2804 LTS_TYPE& aut;
2805 ONLY_IF_DEBUG( public: )
2807 bisim_dnj::part_state_t part_st;
2808
2811 bisim_dnj::part_trans_t part_tr;
2812 private:
2822 fixed_vector<bisim_dnj::iterator_or_counter<
2823 bisim_dnj::action_block_entry*> > action_label;
2824 ONLY_IF_DEBUG( public: )
2826 bool const branching;
2827 private:
2833 bool const preserve_divergence;
2834 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2835 friend class bisim_dnj::pred_entry;
2836 friend class bisim_dnj::bunch_t;
2837 #endif
2838 public:
2840 std::clock_t end_initial_part;
2841
2853 bisim_partitioner_dnj(LTS_TYPE& new_aut, bool const new_branching = false,
2854 bool const new_preserve_divergence = false)
2855 : aut(new_aut),
2856 part_st(new_aut.num_states()),
2857 part_tr(new_aut.num_transitions(), new_aut.num_action_labels()),
2858 action_label(new_aut.num_action_labels()),
2859 branching(new_branching),
2860 preserve_divergence(new_preserve_divergence)
2861 { assert(branching || !preserve_divergence);
2862
2863 mCRL2log(log::verbose) << "Start initialisation.\n";
2864 create_initial_partition(); ONLY_IF_DEBUG( part_tr.action_block_orig_inert_begin =
2865 part_tr.action_block_inert_begin; )
2866 end_initial_part = std::clock();
2867 mCRL2log(log::verbose) << "Start refining\n";
2868 refine_partition_until_it_becomes_stable();
2869 }
2870
2871
2876 state_type num_eq_classes() const
2877 {
2878 return part_st.nr_of_blocks;
2879 }
2880
2881
2889 state_type get_eq_class(state_type const s) const
2890 {
2891 return part_st.block(s)->seqnr;
2892 }
2893
2894
2907 void finalize_minimized_LTS()
2908 {
2909 // The labels have already been stored in
2910 // next_nontrivial_and_label.label by
2911 // refine_partition_until_it_becomes_stable().
2912
2913 // for all blocks
2914 const bisim_dnj::permutation_entry* s_iter(part_st.permutation.data()); assert(s_iter < part_st.permutation.data_end());
2915 do
2916 {
2917 const bisim_dnj::block_t* const B(s_iter->st->bl.ock);
2918 // for all block_bunch-slices of the block
2919 for (const bisim_dnj::block_bunch_slice_t& block_bunch :
2920 B->stable_block_bunch)
2921 { assert(block_bunch.is_stable()); assert(!block_bunch.empty());
2922 const bisim_dnj::pred_entry* const
2923 pred(block_bunch.end[-1].pred); assert(pred->source->bl.ock == B);
2924 assert(nullptr != pred->action_block->succ);
2925 /* add a transition from the source block to the goal block */ assert(pred->action_block->succ->block_bunch->pred == pred);
2926 /* with the indicated label. */ assert(pred->action_block->succ->block_bunch->slice == &block_bunch);
2927 label_type const
2928 label(block_bunch.bunch->next_nontrivial_and_label.label); assert(0 <= label); assert(label < action_label.size());
2929 aut.add_transition(transition(B->seqnr, label,
2930 pred->target->bl.ock->seqnr));
2931 }
2932 s_iter = B->end;
2933 }
2934 while (s_iter < part_st.permutation.data_end());
2935
2936 // Merge the states, by setting the state labels of each state to the
2937 // concatenation of the state labels of its equivalence class.
2938
2939 if (aut.has_state_info()) /* If there are no state labels
2940 this step can be ignored */
2941 {
2942 /* Create a vector for the new labels */
2943 typename std::remove_reference<decltype(aut.state_labels())>::type
2944 new_labels(num_eq_classes());
2945
2946 state_type i(0); assert(i < aut.num_states());
2947 do
2948 {
2949 const state_type new_index(get_eq_class(i));
2950 new_labels[new_index]=new_labels[new_index]+aut.state_label(i);
2951 }
2952 while (++i < aut.num_states());
2953
2954 aut.set_num_states(num_eq_classes(), false); assert(0 == aut.num_state_labels());
2955 //m_aut.clear_state_labels();
2956 new_labels.swap(aut.state_labels());
2957 }
2958 else
2959 {
2960 aut.set_num_states(num_eq_classes(), false);
2961 }
2962
2963 aut.set_initial_state(get_eq_class(aut.initial_state()));
2964 }
2965
2966
2971 bool in_same_class(state_type const s, state_type const t) const
2972 {
2973 return part_st.block(s) == part_st.block(t);
2974 }
2975 private:
2976
2977 /*--------------------------- main algorithm ----------------------------*/
2978
3001 void create_initial_partition()
3002 {
3003 mCRL2log(log::verbose) << "An O(m log n) "
3004 << (branching ? (preserve_divergence
3005 ? "divergence-preserving branching "
3006 : "branching ")
3007 : "")
3008 << "bisimulation partitioner created for " << part_st.state_size()
3009 << " states and " << aut.num_transitions() << " transitions.\n";
3010
3011 if (part_st.state_size() > 2 * aut.num_transitions() + 1)
3012 {
3013 mCRL2log(log::warning) << "There are several isolated states "
3014 "without incoming or outgoing transition. It is not "
3015 "guaranteed that branching bisimulation minimisation runs in "
3016 "time O(m log n).\n";
3017 }
3018
3019 sort_transitions(aut.get_transitions(), tgt_lbl_src);
3020 mCRL2log(log::verbose) << "Carried out sorting\n";
3021 // create one block for all states
3022 bisim_dnj::block_t* B(
3023 #ifdef USE_POOL_ALLOCATOR
3024 simple_list<bisim_dnj::block_bunch_slice_t>::get_pool().
3025 template construct<bisim_dnj::block_t>
3026 #else
3027 new bisim_dnj::block_t
3028 #endif
3029 (part_st.permutation.data(),
3030 part_st.permutation.data_end(), part_st.nr_of_blocks++));
3031
3032 // Iterate over the transitions to count how to order them in
3033 // part_trans_t
3034
3035 // counters for the non-inert outgoing and incoming transitions per
3036 // state are provided in part_st.state_info. These counters have been
3037 // initialised to zero in the constructor of part_state_t.
3038 // counters for the non-inert transition per label are stored in
3039 // action_label.
3040 assert(action_label.size() == aut.num_action_labels());
3041 // counter for the total number of inert transitions:
3042 trans_type inert_transitions(0);
3043 for (const transition& t: aut.get_transitions())
3044 {
3045 if (branching&&aut.is_tau(aut.apply_hidden_label_map(t.label()))&& ((
3046 t.from() != t.to()) || (assert(preserve_divergence), false)))
3047 {
3048 // The transition is inert.
3049 ++part_st.state_info[t.from()].succ_inert.count;
3050 ++inert_transitions;
3051
3052 // The source state should become non-bottom:
3053 if (part_st.state_info[t.from()].pos < B->nonbottom_begin)
3054 {
3055 std::swap(*part_st.state_info[t.from()].pos,
3056 *--B->nonbottom_begin);
3057 // we do not yet update the marked_bottom_begin pointer
3058 }
3059 }
3060 else
3061 {
3062 // The transition is non-inert. (It may be a self-loop).
3063 ++part_st.state_info[t.from()].untested_to_U_eqv.count;
3064 ++action_label[aut.apply_hidden_label_map(t.label())].count;
3065 }
3066 ++part_st.state_info[t.to()].pred_inert.count;
3067 }
3068 // Now we update the marked_bottom_begin pointer:
3069 B->marked_bottom_begin = B->nonbottom_begin;
3070
3071 // set the pointers to transition slices in the state info entries
3072
3073 // We set them all to the end of the respective slice here. Then, with
3074 // every transition, the pointer will be reduced by one, so that after
3075 // placing all transitions it will point to the beginning of the slice.
3076
3077 bisim_dnj::pred_entry* next_pred_begin(&part_tr.pred.begin()[1]);
3078 bisim_dnj::succ_entry* next_succ_begin(&part_tr.succ.begin()[1]);
3079 bisim_dnj::state_info_entry* state_iter(part_st.state_info.data()); assert(state_iter < part_st.state_info.data_end());
3080 do
3081 {
3082 state_iter->bl.ed_noninert_end = next_pred_begin;
3083 next_pred_begin += state_iter->pred_inert.count;
3084 state_iter->pred_inert.convert_to_iterator(next_pred_begin);
3085
3086 // create slice descriptors in part_tr.succ for each state with
3087 /* outgoing transitions. */ assert(nullptr != next_succ_begin);
3088 state_iter->untested_to_U_eqv.convert_to_iterator(
3089 next_succ_begin + state_iter->untested_to_U_eqv.count);
3090 if (next_succ_begin < state_iter->untested_to_U_eqv.begin)
3091 { assert(nullptr != state_iter->untested_to_U_eqv.begin);
3092 next_succ_begin->begin_or_before_end =
3093 state_iter->untested_to_U_eqv.begin - 1;
3094 for (bisim_dnj::succ_entry* const
3095 out_slice_begin(next_succ_begin);
3096 ++next_succ_begin < state_iter->untested_to_U_eqv.begin; )
3097 {
3098 next_succ_begin->begin_or_before_end = out_slice_begin; // mCRL2complexity(next_succ_begin->block_bunch->pred, ...) -- subsumed in the
3099 } // call below
3100
3101 B->mark(state_iter->pos);
3102 }
3103 state_iter->succ_inert.convert_to_iterator(next_succ_begin +
3104 state_iter->succ_inert.count);
3105 #ifndef NDEBUG
3106 while (next_succ_begin < state_iter->succ_inert.begin)
3107 { assert(nullptr == next_succ_begin->begin_or_before_end);
3108 ++next_succ_begin;
3109 }
3110 #endif
3111 next_succ_begin = state_iter->succ_inert.begin; // mCRL2complexity(*state_iter, ...) -- subsumed in the call at the end
3112 }
3113 while (++state_iter < part_st.state_info.data_end());
3114
3115 // Line 2.4: Pi_t := { { all non-inert transitions } }
3116 part_tr.action_block_inert_begin =
3117 part_tr.action_block.data_end() - inert_transitions; assert(part_tr.action_block.data() <= part_tr.action_block_inert_begin);
3118 part_tr.block_bunch_inert_begin =
3119 part_tr.block_bunch.data_end() - inert_transitions; assert(part_tr.block_bunch.data() < part_tr.block_bunch_inert_begin);
3120 bisim_dnj::bunch_t* bunch(nullptr);
3121
3122 if (1 + part_tr.block_bunch.data() < part_tr.block_bunch_inert_begin)
3123 { assert(part_tr.action_block.data() < part_tr.action_block_inert_begin);
3124 // create a single bunch containing all non-inert transitions
3125 bunch =
3126 #ifdef USE_POOL_ALLOCATOR
3127 simple_list<bisim_dnj::block_bunch_slice_t>::get_pool().
3128 template construct<bisim_dnj::bunch_t>
3129 #else
3130 new bisim_dnj::bunch_t
3131 #endif
3132 (part_tr.action_block.data(),
3133 part_tr.action_block_inert_begin); assert(nullptr != bunch); assert(part_tr.splitter_list.empty());
3134 ++part_tr.nr_of_bunches; assert(1 == part_tr.nr_of_bunches);
3135
3136 // create a single block_bunch entry for all non-inert transitions
3137 part_tr.splitter_list.emplace_front(
3138 part_tr.block_bunch_inert_begin, bunch, false); assert(!part_tr.splitter_list.empty());
3139 ++part_tr.nr_of_block_bunch_slices; assert(1 == part_tr.nr_of_block_bunch_slices);
3140 }
3141
3142 // create slice descriptors in part_tr.action_block for each label
3143
3144 // The action_block array shall have the tau transitions at the end:
3145 // first the non-inert tau transitions (during initialisation, that are
3146 // only the tau self-loops), then the tau transitions that have become
3147 // non-inert and finally the inert transitions.
3148 // Transitions with other labels are placed from beginning to end.
3149 // Every such transition block except the last one ends with a dummy
3150 /* entry. If there are transition labels without transitions, */ assert(part_tr.action_block.size() ==
3151 /* multiple dummy entries will be placed side-by-side. */ aut.num_transitions() + action_label.size() - 1);
3152 bisim_dnj::action_block_entry*
3153 next_action_label_begin(part_tr.action_block.data());
3154 trans_type const n_square(part_st.state_size() * part_st.state_size());
3155 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3156 trans_type max_transitions = n_square;
3157 #endif
3158 label_type label(action_label.size()); assert(0 < label);
3159 do
3160 {
3161 --label;
3162 if (0 < action_label[label].count)
3163 { assert(nullptr != bunch);
3164 if (++part_tr.nr_of_action_block_slices == 2)
3165 {
3166 // This is the second action_block-slice, so the bunch is
3167 // not yet marked as nontrivial but it should be.
3168 part_tr.make_nontrivial(bunch);
3169 }
3170 if (n_square < action_label[label].count)
3171 {
3172 mCRL2log(log::warning) << "There are "
3173 << action_label[label].count << ' '
3174 << pp(aut.action_label(label)) << "-transitions. "
3175 "This is more than n^2 (= " << n_square << "). It is "
3176 "not guaranteed that branching bisimulation "
3177 "minimisation runs in time O(m log n).\n";
3178 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3179 if (max_transitions < action_label[label].count)
3180 { max_transitions = action_label[label].count; }
3181 #endif
3182 }
3183 // initialise begin_or_before_end pointers for this
3184 // action_block-slice
3185 action_label[label].convert_to_iterator(
3186 next_action_label_begin + action_label[label].count);
3187 next_action_label_begin->begin_or_before_end =
3188 action_label[label].begin - 1; assert(nullptr != next_action_label_begin->begin_or_before_end);
3189 bisim_dnj::action_block_entry* const
3190 action_block_slice_begin(next_action_label_begin); assert(nullptr != action_block_slice_begin);
3191 while (++next_action_label_begin < action_label[label].begin)
3192 {
3193 next_action_label_begin->begin_or_before_end =
3194 action_block_slice_begin; // mCRL2complexity(next_action_label_begin->succ->block_bunch->pred, ...) --
3195 } // subsumed in the call at the end
3196 }
3197 else
3198 {
3199 action_label[label].convert_to_iterator(
3200 next_action_label_begin);
3201 if (0 != label && aut.num_transitions() < action_label.size())
3202 {
3203 mCRL2log(log::warning) << "Action label "
3204 << pp(aut.action_label(label)) << " has no "
3205 "transitions, and the number of action labels exceeds "
3206 "the number of transitions. It is not guaranteed that "
3207 "branching bisimulation minimisation runs in time "
3208 "O(m log n).\n";
3209 }
3210 }
3211 }
3212 while (0 < label && (/* insert a dummy entry */ assert(next_action_label_begin < part_tr.action_block_inert_begin),
3213 next_action_label_begin->succ = nullptr,
3214 next_action_label_begin->begin_or_before_end = nullptr,
3215 ++next_action_label_begin, true)); assert(next_action_label_begin == part_tr.action_block_inert_begin);
3216 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3217 /* distribute the transitions over the data structures */ check_complexity::init(2 * max_transitions);
3218 #endif
3219 bisim_dnj::block_bunch_entry*
3220 next_block_bunch(1 + part_tr.block_bunch.data());
3221 for (const transition& t: aut.get_transitions())
3222 {
3223 bisim_dnj::state_info_entry* const
3224 source(part_st.state_info.data() + t.from());
3225 bisim_dnj::state_info_entry* const
3226 target(part_st.state_info.data() + t.to());
3227 bisim_dnj::succ_entry* succ_pos;
3228 bisim_dnj::block_bunch_entry* block_bunch_pos;
3229 bisim_dnj::pred_entry* pred_pos;
3230 bisim_dnj::action_block_entry* action_block_pos;
3231
3232 if (branching&&aut.is_tau(aut.apply_hidden_label_map(t.label()))&& ((
3233 t.from() != t.to()) || (assert(preserve_divergence), false)))
3234 {
3235 // It is a (normal) inert transition: place near the end of the
3236 // respective pred/succ slices, just before the other inert
3237 // transitions.
3238 succ_pos = --source->succ_inert.begin; assert(nullptr == succ_pos->begin_or_before_end);
3239 block_bunch_pos = part_tr.block_bunch.data_end() -
3240 inert_transitions; assert(block_bunch_pos >= part_tr.block_bunch_inert_begin);
3241 pred_pos = --target->pred_inert.begin; assert(block_bunch_pos->slice.is_null());
3242 action_block_pos = part_tr.action_block.data_end() -
3243 inert_transitions; assert(action_block_pos >= part_tr.action_block_inert_begin);
3244 action_block_pos->begin_or_before_end = nullptr;
3245 --inert_transitions;
3246 }
3247 else
3248 {
3249 // It is a non-inert transition (possibly a self-loop): place
3250 // at the end of the respective succ slice and at the beginning
3251 // of the respective pred slice.
3252 succ_pos =
3253 --part_st.state_info[t.from()].untested_to_U_eqv.begin; assert(nullptr != succ_pos->begin_or_before_end);
3254 assert(nullptr != succ_pos->begin_or_before_end->begin_or_before_end);
3255 assert(succ_pos->begin_or_before_end <= succ_pos ||
3256 succ_pos->begin_or_before_end->begin_or_before_end == succ_pos);
3257 block_bunch_pos = next_block_bunch++; assert(block_bunch_pos < part_tr.block_bunch_inert_begin);
3258 pred_pos = target->bl.ed_noninert_end++;
3259 action_block_pos =
3260 --action_label[aut.apply_hidden_label_map(t.label())].begin; assert(nullptr != action_block_pos->begin_or_before_end);
3261 assert(nullptr != action_block_pos->begin_or_before_end->begin_or_before_end);
3262 assert(action_block_pos->begin_or_before_end <= action_block_pos ||
3263 action_block_pos->begin_or_before_end->
3264 begin_or_before_end == action_block_pos);
3265 assert(!part_tr.splitter_list.empty());
3266 block_bunch_pos->slice = part_tr.splitter_list.begin(); assert(action_block_pos < part_tr.action_block_inert_begin);
3267 } assert(target->bl.ed_noninert_end <= target->pred_inert.begin);
3268 succ_pos->block_bunch = block_bunch_pos;
3269 block_bunch_pos->pred = pred_pos;
3270 pred_pos->action_block = action_block_pos;
3271 pred_pos->source = source;
3272 pred_pos->target = target; assert(nullptr != succ_pos);
3273 action_block_pos->succ = succ_pos; // mCRL2complexity(pred_pos, ...) -- subsumed in the call at the end
3274 } assert(0 == inert_transitions);
3275 /* delete transitions already -- they are no longer needed. We will */ assert(next_block_bunch == part_tr.block_bunch_inert_begin);
3276 // add new transitions at the end of minimisation.
3277 aut.clear_transitions();
3278
3279 state_iter = part_st.state_info.data(); assert(state_iter < part_st.state_info.data_end());
3280 do
3281 {
3282 state_iter->bl.ock = B;
3283 }
3284 while (++state_iter < part_st.state_info.data_end());
3285
3286 if (nullptr != bunch)
3287 {
3288 while (nullptr == bunch->begin->succ)
3289 { assert(nullptr == bunch->begin->begin_or_before_end);
3290 ++bunch->begin; assert(bunch->begin < bunch->end);
3291 } assert(nullptr != bunch->begin->begin_or_before_end);
3292 while (nullptr == bunch->end[-1].succ)
3293 { assert(nullptr == bunch->end[-1].begin_or_before_end);
3294 --bunch->end; assert(bunch->begin < bunch->end);
3295 } assert(nullptr != bunch->end[-1].begin_or_before_end);
3296
3297 /* Line 2.2: B_vis := { s in S | there exists a visible */ mCRL2complexity(B, add_work(check_complexity::
3298 /* transition that is reachable */ create_initial_partition, 1U), *this);
3299 // from s }
3300 // B_invis := S \ B_vis
3301 // Line 2.3: Pi_s := { B_vis, B_invis } \ { emptyset }
3302 // At this point, all states with a visible transition are
3303 // marked.
3304 if (0 < B->marked_size())
3305 { ONLY_IF_DEBUG( part_st.print_part(*this);
3306 part_tr.print_trans(*this); )
3307 bisim_dnj::block_bunch_slice_iter_t slice =
3308 part_tr.splitter_list.begin();
3309 if (1 < B->size())
3310 {
3311 B = split(B, /* splitter block_bunch */ slice,
3312 extend_from_marked_states__add_new_noninert_to_splitter);
3313 // We can ignore possible new non-inert transitions, as
3314 // every R-bottom state already has a transition in bunch.
3315 B->marked_nonbottom_begin = B->end;
3316 }
3317 else
3318 { assert(B->nonbottom_begin == B->end);
3319 /* A block with 1 state will not be split. However, we */ assert(B->marked_nonbottom_begin == B->end);
3320 // still have to make the splitter stable.
3321 B->stable_block_bunch.splice(B->stable_block_bunch.end(),
3322 part_tr.splitter_list, slice);
3323 slice->make_stable();
3324 } assert(!B->stable_block_bunch.empty()); assert(part_tr.splitter_list.empty());
3325 assert(B->stable_block_bunch.front().end <= part_tr.block_bunch_inert_begin);
3326 assert(1 + part_tr.block_bunch.data() < B->stable_block_bunch.front().end);
3327 B->marked_bottom_begin = B->nonbottom_begin; assert(!B->stable_block_bunch.front().empty());
3328 }
3329 } else assert(0 == B->marked_size());
3330 }
3331 #ifndef NDEBUG
3342 void assert_stability() const
3343 {
3344 part_st.assert_consistency(*this);
3345
3346 assert(part_tr.succ.size() == part_tr.block_bunch.size() + 1);
3347 assert(part_tr.pred.size() == part_tr.block_bunch.size() + 1);
3348 assert(part_tr.action_block.size() ==
3349 part_tr.block_bunch.size() + action_label.size() - 2);
3350 if (part_tr.block_bunch.empty()) return;
3351
3352 assert(part_tr.splitter_list.empty());
3353 /* for (const block_bunch_slice_t& block_bunch : part_tr.splitter_list)
3354 {
3355 assert(!block_bunch.is_stable());
3356 } */
3357
3358 trans_type true_nr_of_block_bunch_slices(0);
3359 // for all blocks
3360 const bisim_dnj::permutation_entry*
3361 perm_iter(part_st.permutation.data());
3362 assert(perm_iter < part_st.permutation.data_end());
3363 do
3364 {
3365 const bisim_dnj::block_t* const block(perm_iter->st->bl.ock);
3366 unsigned const max_block(check_complexity::log_n -
3367 check_complexity::ilog2(block->size()));
3368 // iterators have no predefined hash, so we store pointers:
3369 std::unordered_set<const bisim_dnj::block_bunch_slice_t*>
3370 block_bunch_check_set;
3371 #ifndef USE_SIMPLE_LIST
3372 block_bunch_check_set.reserve(
3373 block->stable_block_bunch.size());
3374 #endif
3375
3376 // for all stable block_bunch-slices of the block
3377 for (const bisim_dnj::block_bunch_slice_t& block_bunch :
3378 block->stable_block_bunch)
3379 {
3380 assert(block_bunch.source_block() == block);
3381 assert(block_bunch.is_stable());
3382 block_bunch_check_set.insert(&block_bunch);
3383 mCRL2complexity(&block_bunch, no_temporary_work(
3384 block_bunch.bunch->max_work_counter(*this)), *this);
3385 ++true_nr_of_block_bunch_slices;
3386 }
3387
3388 // for all states in the block
3389 do
3390 {
3391 trans_type block_bunch_count(0);
3392 const bisim_dnj::state_info_entry* const state(perm_iter->st);
3393 assert(state!=part_tr.succ.front().block_bunch->pred->source);
3394 // for all out-slices of the state
3395 for (const bisim_dnj::succ_entry*
3396 out_slice_end(state->succ_inert.begin);
3397 state == out_slice_end[-1].block_bunch->pred->source; )
3398 { assert(!out_slice_end[-1].block_bunch->slice.is_null());
3399 bisim_dnj::block_bunch_slice_const_iter_t const
3400 block_bunch_slice(out_slice_end[-1].block_bunch->slice);
3401 const bisim_dnj::bunch_t* const bunch(
3402 block_bunch_slice->bunch);
3403 assert(block == block_bunch_slice->source_block());
3404 if (block_bunch_slice->is_stable())
3405 {
3406 assert(1 == block_bunch_check_set.count(
3407 &*block_bunch_slice));
3408 ++block_bunch_count;
3409 }
3410 else assert(0); // i. e. all block_bunch-slices should
3411 // be stable
3412 const bisim_dnj::succ_entry* const out_slice_begin(
3413 out_slice_end[-1].begin_or_before_end);
3414 assert(nullptr != out_slice_begin);
3415 assert(out_slice_begin < out_slice_end);
3416 assert(nullptr != out_slice_begin->begin_or_before_end);
3417 assert(out_slice_begin->begin_or_before_end + 1 ==
3418 out_slice_end);
3419
3420 // for all transitions in the out-slice
3421 do
3422 {
3423 --out_slice_end;
3424 assert(bunch->begin <=
3425 out_slice_end->block_bunch->pred->action_block);
3426 assert(out_slice_end->block_bunch->pred->
3427 action_block < bunch->end);
3428 assert(out_slice_end->block_bunch->slice ==
3429 block_bunch_slice);
3430 assert(nullptr != out_slice_end->begin_or_before_end);
3431 if (out_slice_end->block_bunch + 1 !=
3432 block_bunch_slice->end)
3433 {
3434 assert(out_slice_end->block_bunch + 1 <
3435 block_bunch_slice->end);
3436 assert(out_slice_end->block_bunch[1].slice ==
3437 block_bunch_slice);
3438 }
3439 mCRL2complexity(out_slice_end->block_bunch->pred,
3440 no_temporary_work(max_block,
3441 check_complexity::log_n -
3442 check_complexity::ilog2(out_slice_end->
3443 block_bunch->pred->target->bl.ock->size()),
3444 perm_iter < block->nonbottom_begin),*this);
3445 }
3446 while (out_slice_begin < out_slice_end &&
3447 (assert(out_slice_begin ==
3448 out_slice_end->begin_or_before_end), true));
3449 }
3450 if (perm_iter < block->nonbottom_begin)
3451 {
3452 assert(block_bunch_check_set.size() == block_bunch_count);
3453 }
3454 }
3455 while (++perm_iter < block->end);
3456 }
3457 while (perm_iter < part_st.permutation.data_end());
3458 assert(part_tr.nr_of_block_bunch_slices ==
3459 true_nr_of_block_bunch_slices);
3460 assert(part_tr.action_block.data()<=part_tr.action_block_inert_begin);
3461 assert(part_tr.block_bunch.data() < part_tr.block_bunch_inert_begin);
3462 if (branching)
3463 { assert(part_tr.action_block_inert_begin <=
3464 part_tr.action_block.data_end());
3465 assert(part_tr.block_bunch_inert_begin <=
3466 part_tr.block_bunch.data_end());
3467 assert(part_tr.block_bunch.data_end() -
3468 part_tr.block_bunch_inert_begin ==
3469 part_tr.action_block.data_end()-part_tr.action_block_inert_begin);
3470
3471 // for all inert transitions
3472 for (const bisim_dnj::action_block_entry* action_block(
3473 part_tr.action_block_inert_begin);
3474 action_block < part_tr.action_block.data_end();
3475 ++action_block)
3476 { assert(nullptr == action_block->begin_or_before_end);
3477 const bisim_dnj::succ_entry* const
3478 succ_iter(action_block->succ);
3479 assert(nullptr != succ_iter);
3480 assert(succ_iter->block_bunch->slice.is_null());
3481 const bisim_dnj::pred_entry* const
3482 pred_iter(succ_iter->block_bunch->pred);
3483 assert(action_block == pred_iter->action_block);
3484 assert(part_tr.block_bunch_inert_begin <=
3485 succ_iter->block_bunch);
3486 assert(pred_iter->source != pred_iter->target);
3487 assert(pred_iter->source->bl.ock == pred_iter->target->bl.ock);
3488 assert(pred_iter->source->succ_inert.begin <= succ_iter);
3489 assert(pred_iter->source->succ_inert.begin == succ_iter ||
3490 succ_iter[-1].block_bunch->pred->source==pred_iter->source);
3491 assert(pred_iter->target->pred_inert.begin <= pred_iter);
3492 assert(pred_iter->target->pred_inert.begin == pred_iter ||
3493 pred_iter[-1].target == pred_iter->target);
3494 unsigned const max_block(check_complexity::log_n -
3495 check_complexity::ilog2(pred_iter->target->bl.ock->size()));
3496 mCRL2complexity(pred_iter, no_temporary_work(max_block,
3497 max_block, false), *this);
3498 }
3499 }
3500 else
3501 {
3502 assert(!preserve_divergence);
3503 assert(part_tr.action_block_inert_begin ==
3504 part_tr.action_block.data_end());
3505 assert(part_tr.block_bunch_inert_begin ==
3506 part_tr.block_bunch.data_end());
3507 }
3508 const bisim_dnj::action_block_entry*
3509 action_slice_end(part_tr.action_block_inert_begin);
3510 trans_type true_nr_of_bunches(0);
3511 trans_type true_nr_of_nontrivial_bunches(0);
3512 trans_type true_nr_of_action_block_slices(0);
3513 // for all action labels and bunches
3514 label_type label(0);
3515 assert(label < action_label.size());
3516 const bisim_dnj::bunch_t* previous_bunch(nullptr);
3517 do
3518 {
3519 assert(part_tr.action_block.data() <= action_label[label].begin);
3520 assert(action_label[label].begin <= action_slice_end);
3521 assert(action_slice_end <= part_tr.action_block_inert_begin);
3522 // for all action_block slices
3523 for (const bisim_dnj::action_block_entry*
3524 action_block_slice_end(action_slice_end);
3525 action_label[label].begin < action_block_slice_end; )
3526 {
3527 const bisim_dnj::action_block_entry* const
3528 action_block_slice_begin(
3529 action_block_slice_end[-1].begin_or_before_end);
3530 assert(nullptr != action_block_slice_begin);
3531 assert(action_block_slice_begin < action_block_slice_end);
3532 assert(action_block_slice_end <= action_slice_end);
3533 assert(nullptr != action_block_slice_begin->succ);
3534 const bisim_dnj::block_t* const
3535 target_block(action_block_slice_begin->
3536 succ->block_bunch->pred->target->bl.ock);
3537 const bisim_dnj::bunch_t* const
3538 bunch(action_block_slice_begin->succ->bunch());
3539 if (previous_bunch != bunch)
3540 {
3541 assert(nullptr == previous_bunch);
3542 previous_bunch = bunch;
3543 assert(bunch->end == action_block_slice_end);
3544 if (bunch->begin == action_block_slice_begin)
3545 {
3546 // Perhaps this does not always hold; sometimes, an
3547 // action_block slice disappears but the bunch cannot
3548 // be made trivial.
3549 assert(bunch->is_trivial());
3550 }
3551 else
3552 {
3553 assert(!bunch->is_trivial());
3554 ++true_nr_of_nontrivial_bunches;
3555 }
3556 mCRL2complexity(bunch, no_temporary_work(
3557 bunch->max_work_counter(*this)), *this);
3558 ++true_nr_of_bunches;
3559 }
3560 if(bunch->begin == action_block_slice_begin)
3561 {
3562 previous_bunch = nullptr;
3563 }
3564 else assert(bunch->begin < action_block_slice_begin);
3565
3566 assert(action_block_slice_begin->begin_or_before_end + 1 ==
3567 action_block_slice_end);
3568 // for all transitions in the action_block slice
3569 const bisim_dnj::action_block_entry*
3570 action_block(action_block_slice_end);
3571 do
3572 {
3573 --action_block;
3574 const bisim_dnj::succ_entry* const
3575 succ_iter(action_block->succ);
3576 assert(nullptr != succ_iter);
3577 const bisim_dnj::pred_entry* const
3578 pred_iter(succ_iter->block_bunch->pred);
3579 assert(action_block == pred_iter->action_block);
3580 assert(succ_iter->block_bunch <
3581 part_tr.block_bunch_inert_begin);
3582 assert(!branching || !aut.is_tau(label) ||
3583 pred_iter->source->bl.ock!=pred_iter->target->bl.ock ||
3584 (preserve_divergence &&
3585 pred_iter->source == pred_iter->target));
3586 assert(succ_iter < pred_iter->source->succ_inert.begin);
3587 assert(succ_iter+1==pred_iter->source->succ_inert.begin ||
3588 succ_iter[1].block_bunch->pred->source ==
3589 pred_iter->source);
3590 assert(pred_iter < pred_iter->target->pred_inert.begin);
3591 assert(pred_iter+1==pred_iter->target->pred_inert.begin ||
3592 pred_iter[1].target == pred_iter->target);
3593 assert(target_block == pred_iter->target->bl.ock);
3594 assert(bunch == succ_iter->bunch());
3595 }
3596 while (action_block_slice_begin < action_block &&
3597 (// some properties only need to be checked for states that
3598 // are not the first one:
3599 assert(action_block->begin_or_before_end ==
3600 action_block_slice_begin), true));
3601 action_block_slice_end = action_block_slice_begin;
3602 ++true_nr_of_action_block_slices;
3603 }
3604 if (action_slice_end < part_tr.action_block_inert_begin)
3605 {
3606 // there is a dummy transition between action labels
3607 assert(nullptr == action_slice_end->succ);
3608 assert(nullptr == action_slice_end->begin_or_before_end);
3609 }
3610 }
3611 while (++label < action_label.size() &&
3612 (action_slice_end = action_label[label - 1].begin - 1, true));
3613 assert(nullptr == previous_bunch);
3614 assert(part_tr.nr_of_bunches == true_nr_of_bunches);
3615 assert(part_tr.nr_of_nontrivial_bunches ==
3616 true_nr_of_nontrivial_bunches);
3617 assert(part_tr.nr_of_action_block_slices ==
3618 true_nr_of_action_block_slices);
3619 }
3620 #endif
3638 void refine_partition_until_it_becomes_stable()
3639 {
3640 // Line 2.5: for all non-trivial bunches bunch_T in Pi_t do
3641 std::clock_t next_print_time = std::clock();
3642 const std::clock_t rounded_start_time=next_print_time-CLOCKS_PER_SEC/2;
3643 // const double log_initial_nr_of_action_block_slices =
3644 // 100 / std::log(part_tr.nr_of_action_block_slices);
3645 for (;;)
3646 { // mCRL2complexity(...) -- this loop will be ascribed to (the transitions in)
3647 // the new bunch below.
3648 /*------------------ find a non-trivial bunch -------------------*/ ONLY_IF_DEBUG( part_st.print_part(*this); part_tr.print_trans(*this);
3649 assert_stability(); )
3650 /* 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 <=
3651 /* |bunch_T_a_Bprime| <= 1/2 |bunch_T| */ part_tr.nr_of_action_block_slices);
3652 bisim_dnj::bunch_t* const bunch_T(part_tr.get_some_nontrivial());
3653 if (mCRL2logEnabled(log::verbose))
3654 {
3655 if (std::clock_t now = std::clock(); next_print_time <= now ||
3656 nullptr == bunch_T)
3657 {
3658
3659 /* - - - - -print progress information- - - - - */
3660
3661 // The formula below should ensure that `next_print_time`
3662 // increases by a whole number of minutes, so that the
3663 // progress information is printed every minute (or, if
3664 // one iteration takes more than one minute, after a whole
3665 // number of minutes).
3666 next_print_time+=((now-next_print_time)/(60*CLOCKS_PER_SEC)
3667 + 1) * (60*CLOCKS_PER_SEC);
3668 now = (now - rounded_start_time) / CLOCKS_PER_SEC;
3669 if (0 != now)
3670 {
3671 if (60 <= now)
3672 {
3673 if (3600 <= now)
3674 {
3675 mCRL2log(log::verbose)
3676 << now / 3600 << " h ";
3677 now %= 3600;
3678 }
3679 mCRL2log(log::verbose)
3680 << now / 60 << " min ";
3681 now %= 60;
3682 }
3683 mCRL2log(log::verbose) << now
3684 << " sec passed since starting the main loop.\n";
3685 }
3686 #define PRINT_SG_PL(counter, sg_string, pl_string) \
3687 (counter) \
3688 << (1 == (counter) ? (sg_string) : (pl_string))
3689 mCRL2log(log::verbose)
3690 << (nullptr == bunch_T ? "The reduced LTS contains "
3691 : "The reduced LTS contains at least ")
3692 << PRINT_SG_PL(part_st.nr_of_blocks,
3693 " state and ", " states and ")
3694 << PRINT_SG_PL(part_tr.nr_of_block_bunch_slices,
3695 " transition.", " transitions.");
3696 if (1 < part_tr.nr_of_action_block_slices)
3697 {
3698 #define PRINT_INT_PERCENTAGE(num,denom) \
3699 (((num) * 200 + (denom)) / (denom) / 2)
3700 mCRL2log(log::verbose) << " Estimated "
3701 << PRINT_INT_PERCENTAGE(part_tr.nr_of_bunches - 1,
3702 part_tr.nr_of_action_block_slices - 1)
3703 << "% done.";
3704 #undef PRINT_INT_PERCENTAGE
3705 }
3706 mCRL2log(log::verbose)
3707 // << " Logarithmic estimate: "
3708 // << (int)(100.5+std::log((double) part_tr.nr_of_bunches/
3709 // part_tr.nr_of_action_block_slices)
3710 // *log_initial_nr_of_action_block_slices)
3711 // << "% done."
3712 << "\nThe current partition contains ";
3713 if (branching)
3714 {
3715 mCRL2log(log::verbose)
3716 << PRINT_SG_PL(part_tr.nr_of_new_bottom_states,
3717 " new bottom state, ", " new bottom states, ");
3718 } else assert(0 == part_tr.nr_of_new_bottom_states);
3719 mCRL2log(log::verbose)
3720 << PRINT_SG_PL(part_tr.nr_of_bunches,
3721 " bunch (of which ", " bunches (of which ")
3722 << PRINT_SG_PL(part_tr.nr_of_nontrivial_bunches,
3723 " is nontrivial), and ", " are nontrivial), and ")
3724 << PRINT_SG_PL(part_tr.nr_of_action_block_slices,
3725 " action-block-slice.\n", " action-block-slices.\n");
3726 #undef PRINT_SG_PL
3727 }
3728 }
3729 if (nullptr == bunch_T) { break; } ONLY_IF_DEBUG( mCRL2log(log::debug) << "Refining "
3730 /* Line 2.7: Pi_t := Pi_t \ { bunch_T } union */ << bunch_T->debug_id(*this) << '\n'; )
3731 /* { bunch_T_a_Bprime, bunch_T \ bunch_T_a_Bprime } */ assert(part_tr.nr_of_bunches < part_tr.nr_of_action_block_slices);
3732 bisim_dnj::bunch_t* const bunch_T_a_Bprime(
3733 bunch_T->split_off_small_action_block_slice(part_tr));
3734 ONLY_IF_DEBUG( mCRL2log(log::debug) << "Splitting off "
3735 /*------------ find predecessors of bunch_T_a_Bprime ------------*/ << bunch_T_a_Bprime->debug_id(*this) << '\n'; )
3736 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3737 /* Line 2.8: for all B in splittableBlocks(bunch_T_a_Bprime) do */ unsigned const max_splitter_counter(
3738 /* we actually run through the transitions in T--a-->B' */ bunch_T_a_Bprime->max_work_counter(*this));
3739 #endif
3740 bisim_dnj::action_block_entry* splitter_iter(
3741 bunch_T_a_Bprime->begin); assert(splitter_iter < bunch_T_a_Bprime->end);
3742 do
3743 { assert(nullptr != splitter_iter->succ);
3744 bisim_dnj::state_info_entry* const
3745 source(splitter_iter->succ->block_bunch->pred->source); assert(splitter_iter->succ->block_bunch->pred->action_block == splitter_iter);
3746 // Line 2.11: Mark all transitions in bunch_T_a_Bprime
3747 // actually we mark the source state (i.e. register it's in
3748 // R)
3749 bool const first_transition_of_state(
3750 source->bl.ock->mark(source->pos));
3751 // Line 2.9: Add bunch_T_a_Bprime as primary to the splitter
3752 // list
3753 // Line 2.10: Add T_B--> \ bunch_T_a_Bprime as secondary to the
3754 // splitter list
3755 part_tr.first_move_transition_to_new_bunch(splitter_iter,
3756 bunch_T_a_Bprime, first_transition_of_state); // mCRL2complexity(splitter_iter->succ->block_bunch->pred, ...) -- subsumed
3757 // Line 2.13: end for // in the call below
3758 }
3759 while (++splitter_iter < bunch_T_a_Bprime->end);
3760
3761 // We cannot join the loop above with the loop below!
3762
3763 // Line 2.8: for all B in splittableBlocks(T--a-->B') do
3764 splitter_iter = bunch_T_a_Bprime->begin; assert(splitter_iter < bunch_T_a_Bprime->end);
3765 do
3766 {
3767 // Line 2.12: For every state with both marked outgoing
3768 // transitions and outgoing transitions in
3769 // T_B--> \ bunch_T_a_Bprime, mark one such
3770 // transition
3771 part_tr.second_move_transition_to_new_bunch(splitter_iter, ONLY_IF_DEBUG( *this, bunch_T_a_Bprime, )
3772 bunch_T); // mCRL2complexity(splitter_iter->succ->block_bunch->pred, ...) -- subsumed
3773 // Line 2.13: end for // in the call below
3774 }
3775 while (++splitter_iter < bunch_T_a_Bprime->end); mCRL2complexity(bunch_T_a_Bprime,
3776 add_work(check_complexity::refine_partition_until_stable__find_pred,
3777 /*----------------- stabilise the partition again ---------------*/ max_splitter_counter), *this);
3778 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3779 /* Line 2.14: for all T'_B--> in the splitter list (in order) do */ bisim_dnj::block_bunch_slice_iter_or_null_t bbslice_T_a_Bprime_B(nullptr);
3780 #endif
3781 while (!part_tr.splitter_list.empty())
3782 {
3783 bisim_dnj::block_bunch_slice_iter_t splitter_Tprime_B( // We have to call mCRL2complexity here because `splitter_Tprime_B` may be
3784 part_tr.splitter_list.begin()); // split up later.
3785 bisim_dnj::block_t* block_B(splitter_Tprime_B->source_block()); assert(!splitter_Tprime_B->is_stable());
3786 bool const is_primary_splitter = 0 < block_B->marked_size(); assert(!splitter_Tprime_B->empty());
3787 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3788 bool add_stabilize_to_bottom_transns_succeeded = true;
3789 if (is_primary_splitter)
3790 {
3791 assert(bbslice_T_a_Bprime_B.is_null());
3792 // assign work to this splitter bunch
3793 mCRL2complexity(splitter_Tprime_B, add_work(
3794 check_complexity::refine_partition_until_stable__stabilize,
3795 max_splitter_counter), *this);
3796 }
3797 else if (!bbslice_T_a_Bprime_B.is_null())
3798 {
3799 // assign work to this the corresponding block_bunch-slice of
3800 // bunch_T_a_Bprime
3801 mCRL2complexity(bbslice_T_a_Bprime_B,
3802 add_work(check_complexity::
3803 refine_partition_until_stable__stabilize_for_large_splitter,
3804 max_splitter_counter), *this);
3805 }
3806 else
3807 {
3808 // This must be a refinement to stabilize for new bottom states.
3809 // assign work to the new bottom states in this block_bunch-slice
3810 add_stabilize_to_bottom_transns_succeeded = splitter_Tprime_B->
3811 add_work_to_bottom_transns(check_complexity::
3812 refine_partition_until_stable__stabilize_new_noninert_a_priori,
3813 1U, *this);
3814 }
3815 #endif
3816 if (1 < block_B->size())
3817 {
3818 bisim_dnj::permutation_entry* const
3819 block_B_begin(block_B->begin); assert(block_B_begin->st->pos == block_B_begin);
3820 // Line 2.15: (R, U) := split(B, T'_B-->)
3821 // Line 2.16: Remove T'_B--> from the splitter list
3822 // Line 2.17: Pi_s := Pi_s \ { B } union { R, U } \ { {} }
3823 bisim_dnj::block_t*block_R=split(block_B,splitter_Tprime_B,
3824 is_primary_splitter ? extend_from_marked_states
3825 : extend_from_splitter);
3826 if (block_B_begin < block_R->begin)
3827 {
3828 // The refinement was non-trivial.
3829
3830 // Line 2.18: if T'_B--> was a primary splitter then
3831 if (is_primary_splitter)
3832 { assert(splitter_Tprime_B->bunch == bunch_T_a_Bprime);
3833 // Line 2.19: Remove T_U--> \ T_U--a-->B' from the
3834 // splitter list
3835 bisim_dnj::block_t* const
3836 block_U(block_B_begin->st->bl.ock); assert(block_U->end == block_R->begin);
3837 bisim_dnj::block_bunch_slice_iter_t U_splitter(
3838 part_tr.splitter_list.begin()); assert(0 == block_U->marked_size());
3839 if (part_tr.splitter_list.end() != U_splitter &&
3840 (U_splitter->source_block() == block_U ||
3841 (++U_splitter != part_tr.splitter_list.end() &&
3842 U_splitter->source_block() == block_U)))
3843 { assert(!U_splitter->is_stable());
3844 assert(U_splitter->bunch == bunch_T);
3845 block_U->stable_block_bunch.splice(
3846 block_U->stable_block_bunch.end(),
3847 part_tr.splitter_list, U_splitter);
3848 U_splitter->make_stable();
3849 }
3850 #ifndef NDEBUG
3851 // There should be no block-bunch-slice for the co-splitter that is
3852 // still unstable.
3853 for (bisim_dnj::block_bunch_slice_const_iter_t
3854 iter(part_tr.splitter_list.cbegin());
3855 part_tr.splitter_list.cend() != iter; ++iter)
3856 { assert(!iter->is_stable());
3857 assert(iter->source_block() != block_U);
3858 /* Line 2.20: end if */ }
3859 #endif
3860 }
3861 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3862 else
3863 {
3864 // account for work that couldn't be accounted for earlier (because we
3865 // didn't know yet which state would become a new bottom state)
3866 if (!add_stabilize_to_bottom_transns_succeeded)
3867 { assert(splitter_Tprime_B->add_work_to_bottom_transns(
3868 check_complexity::
3869 refine_partition_until_stable__stabilize_new_noninert_a_posteriori,
3870 1U, *this));
3871 }
3872 if (splitter_Tprime_B->work_counter.has_temporary_work())
3873 { assert(splitter_Tprime_B->add_work_to_bottom_transns(
3874 check_complexity::
3875 handle_new_noninert_transns__make_unstable_a_posteriori,
3876 1U, *this));
3877 splitter_Tprime_B->work_counter.reset_temporary_work();
3878 /* Line 2.21: if R--tau-->U is not empty (i. e. R */ }
3879 /* has new non-inert transitions) then */ }
3880 #endif
3881 if (0 < block_R->marked_size())
3882 { ONLY_IF_DEBUG( const bisim_dnj::block_bunch_entry* const splitter_end =
3883 /* Line 2.22: Create a new bunch containing */ splitter_Tprime_B->end; )
3884 // exactly R--tau-->U, add R--tau-->U to
3885 // the splitter list, and mark all its
3886 // transitions
3887 // to
3888 // Line 2.28: For each bottom state, mark one of
3889 // its outgoing transitions in every
3890 // T_N--> where it has one
3891 block_R = handle_new_noninert_transns(
3892 block_R, splitter_Tprime_B);
3893 #ifndef NDEBUG
3894 if (splitter_end[-1].pred->source->bl.ock == block_R)
3895 { assert(!splitter_end[-1].slice.is_null());
3896 splitter_Tprime_B =
3897 (bisim_dnj::block_bunch_slice_iter_t) splitter_end[-1].slice;
3898 }
3899 /* Line 2.29: end if */ assert(nullptr == block_R || splitter_Tprime_B->source_block() == block_R);
3900 #endif
3901 }
3902 }
3903 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3904 else
3905 { assert(0 == block_R->marked_size());
3906 assert(add_stabilize_to_bottom_transns_succeeded);
3907 // now splitter must have some transitions that start in bottom states:
3908 if (splitter_Tprime_B->work_counter.has_temporary_work())
3909 { assert(!is_primary_splitter);
3910 if (!splitter_Tprime_B->add_work_to_bottom_transns(check_complexity
3911 ::handle_new_noninert_transns__make_unstable_a_posteriori,
3912 1U, *this))
3913 { assert(0); }
3914 splitter_Tprime_B->work_counter.reset_temporary_work();
3915 }
3916 }
3917 block_B = block_R;
3918 #endif
3919 }
3920 else
3921 { assert(block_B->nonbottom_begin == block_B->end);
3922 /* A block with 1 state will not be split. However, we */ assert(block_B->marked_nonbottom_begin == block_B->end);
3923 // may have to unmark all states.
3924 block_B->marked_bottom_begin = block_B->end;
3925 block_B->stable_block_bunch.splice(
3926 block_B->stable_block_bunch.end(),
3927 part_tr.splitter_list, splitter_Tprime_B);
3928 splitter_Tprime_B->make_stable(); assert(add_stabilize_to_bottom_transns_succeeded);
3929 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3930 // now splitter must have some transitions that start in bottom states:
3931 if (splitter_Tprime_B->work_counter.has_temporary_work())
3932 { assert(!is_primary_splitter);
3933 if (!splitter_Tprime_B->add_work_to_bottom_transns(check_complexity::
3934 handle_new_noninert_transns__make_unstable_a_posteriori,
3935 1U, *this))
3936 { assert(0); }
3937 splitter_Tprime_B->work_counter.reset_temporary_work();
3938 }
3939 #endif
3940 }
3941 #ifndef NDEBUG
3942 if (is_primary_splitter && !part_tr.splitter_list.empty() &&
3943 part_tr.splitter_list.front().bunch == bunch_T &&
3944 part_tr.splitter_list.front().source_block() == block_B)
3945 { // The next block_bunch-slice to be handled is the one in the large
3946 // splitter corresponding to the current splitter. In that iteration,
3947 // we will need the current splitter block_bunch-slice.
3948 assert(nullptr != block_B);
3949 assert(splitter_Tprime_B->source_block() == block_B);
3950 assert(splitter_Tprime_B->bunch == bunch_T_a_Bprime);
3951 bbslice_T_a_Bprime_B = splitter_Tprime_B;
3952 }
3953 /* Line 2.30: end for */ else bbslice_T_a_Bprime_B = nullptr;
3954 #endif
3955 }
3956 // Line 2.31: end for
3957 } assert(part_tr.nr_of_bunches == part_tr.nr_of_action_block_slices);
3958 assert(0 == part_tr.nr_of_nontrivial_bunches);
3959
3960 // store the labels with the action_block-slices
3961 // As every action_block-slice is a (trivial) bunch at the same time,
3962 // we can reuse the field next_nontrivial_and_label.label (instead of
3963 // next_nontrivial_and_label.next_nontrivial) to store the label.
3964 const bisim_dnj::action_block_entry*
3965 action_block_iter_end(part_tr.action_block_inert_begin);
3966 label_type label(0); assert(label < action_label.size());
3967 do
3968 {
3969 for (bisim_dnj::action_block_entry*
3970 action_block_iter(action_label[label].begin);
3971 action_block_iter < action_block_iter_end;
3972 action_block_iter = action_block_iter->begin_or_before_end + 1)
3973 { assert(nullptr != action_block_iter->succ);
3974 assert(action_block_iter->succ->block_bunch->pred->action_block ==
3975 action_block_iter);
3976 assert(action_block_iter->succ->bunch()->is_trivial());
3977 action_block_iter->succ->bunch()->
3978 next_nontrivial_and_label.label = label; assert(nullptr != action_block_iter->begin_or_before_end);
3979 assert(action_block_iter <= action_block_iter->begin_or_before_end);
3980 }
3981 }
3982 while (++label < action_label.size() &&
3983 (action_block_iter_end = action_label[label - 1].begin - 1, true));
3984 }
3985
3986 /*----------------- Split -- Algorithm 3 of [JGKW 2020] -----------------*/
3987
4022 bisim_dnj::block_t* split(bisim_dnj::block_t* const block_B,
4023 const bisim_dnj::block_bunch_slice_iter_t splitter_T,
4024 enum refine_mode_t mode)
4025 { assert(block_B == splitter_T->source_block());
4026 #ifndef NDEBUG
4027 mCRL2log(log::debug) << "split("
4028 << block_B->debug_id(*this)
4029 << ',' << splitter_T->debug_id(*this)
4030 << (extend_from_marked_states__add_new_noninert_to_splitter == mode
4031 ? ",extend_from_marked_states__add_new_noninert_to_splitter)\n"
4032 : (extend_from_marked_states == mode
4033 ? ",extend_from_marked_states)\n"
4034 : (extend_from_splitter == mode
4035 ? ",extend_from_splitter)\n"
4036 : ",UNKNOWN MODE)\n")));
4037 #endif
4038 bisim_dnj::block_t* block_R=nullptr; assert(!splitter_T->is_stable()); assert(1 < block_B->size());
4039 union R_s_iter_t
4040 {
4041 bisim_dnj::block_bunch_entry* splitter_iter;
4042 bisim_dnj::permutation_entry* block;
4043 } R_s_iter;
4044
4045 if (extend_from_splitter == mode)
4046 { assert(0 == block_B->marked_size());
4047 // Line 3.2: R := B--Marked(T)--> ; U := Bottom(B) \ R
4048 R_s_iter.splitter_iter = splitter_T->end; assert(splitter_T->marked_begin <= R_s_iter.splitter_iter);
4049 while (splitter_T->marked_begin < R_s_iter.splitter_iter)
4050 { assert(&part_tr.block_bunch.cbegin()[1] < R_s_iter.splitter_iter);
4051 --R_s_iter.splitter_iter;
4052 bisim_dnj::state_info_entry* const
4053 s(R_s_iter.splitter_iter->pred->source); assert(s->bl.ock == block_B); assert(s->pos->st == s);
4054 block_B->mark(s->pos);
4055 // We cannot stop, even if the R-subblock becomes too large,
4056 // because we need to mark all bottom states that are not in U.
4057 }
4058 } else { assert(0 < block_B->marked_size());
4059 assert(splitter_T->marked_begin == splitter_T->end); }
4060 block_B->stable_block_bunch.splice(block_B->stable_block_bunch.end(),
4061 part_tr.splitter_list, splitter_T);
4062 splitter_T->make_stable();
4063
4064 COROUTINES_SECTION
4065 // shared variables of both coroutines
4066 bisim_dnj::permutation_entry*
4067 untested_to_U_defined_end(block_B->nonbottom_begin);
4068 bisim_dnj::permutation_entry*
4069 U_nonbottom_end(untested_to_U_defined_end);
4070
4071 // variable declarations of the U-coroutine
4072 bisim_dnj::permutation_entry* U_s_iter;
4073 bisim_dnj::pred_entry* U_t_iter;
4074 bisim_dnj::state_info_entry* U_t;
4075 const bisim_dnj::succ_entry* U_u_iter;
4076
4077 // variable declarations of the R-coroutine
4078 bisim_dnj::pred_entry* R_t_iter;
4079
4080 COROUTINE_LABELS( (SPLIT_R_PREDECESSOR_HANDLED)
4081 (SPLIT_U_PREDECESSOR_HANDLED)
4082 (SPLIT_R_STATE_HANDLED)
4083 (SPLIT_U_STATE_HANDLED)
4084 (SPLIT_U_TESTING)
4085 (SPLIT_R_COLLECT_SPLITTER))
4086
4087 /*------------------------ find U-states ------------------------*/
4088
4089 COROUTINE
4090 // Line 3.21l: if |U| > |B|/2 then
4091 if(block_B->size() / 2 < block_B->unmarked_bottom_size())
4092 {
4093 // Line 3.22l: Abort this coroutine
4094 ABORT_THIS_COROUTINE();
4095 // Line 3.23l: end if
4096 }
4097 if (0 == block_B->unmarked_bottom_size())
4098 {
4099 // all bottom states are in R, so there cannot be any
4100 // U-states. Unmark all states, as there are no
4101 // transitions that have become non-inert.
4102 block_B->marked_nonbottom_begin = block_B->end;
4103 block_B->marked_bottom_begin = block_B->nonbottom_begin;
4104 block_R = block_B;
4105 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4106 finalise_U_is_smaller(nullptr, block_R, *this);
4107 #endif
4108 TERMINATE_COROUTINE_SUCCESSFULLY();
4109 }
4110
4111 /* - - - - - - - visit U-states - - - - - - - */
4112
4113 if (U_nonbottom_end < block_B->marked_nonbottom_begin)
4114 {
4115 // Line 3.5l: for all s in U while |U| < |B|/2 do
4116 U_s_iter = block_B->begin;
4117 COROUTINE_DO_WHILE (SPLIT_U_STATE_HANDLED,
4118 U_s_iter < U_nonbottom_end)
4119 {
4120 /* Line 3.6l: for all inert transitions t--tau-->s do*/ assert(part_tr.pred.front().target != U_s_iter->st);
4121 COROUTINE_FOR(SPLIT_U_PREDECESSOR_HANDLED,
4122 U_t_iter = U_s_iter->st->pred_inert.begin,
4123 U_t_iter->target == U_s_iter->st, ++U_t_iter)
4124 {
4125 U_t = U_t_iter->source; assert(block_B->nonbottom_begin <= U_t->pos);
4126 /* Line 3.7l: if t in R then Skip state t */ assert(U_t->pos < block_B->end);
4127 if (block_B->marked_nonbottom_begin <= U_t->pos)
4128 {
4129 goto continuation;
4130 }
4131 // Line 3.8l: if untested[t] is undefined then
4132 if (untested_to_U_defined_end <= U_t->pos)
4133 {
4134 // Line 3.9l: untested[t] :=
4135 // |{ t--tau-->u | u in B }|
4136 U_t->untested_to_U_eqv.begin =
4137 U_t->succ_inert.begin;
4138 std::swap(*U_t->pos,
4139 *untested_to_U_defined_end++);
4140 // Line 3.10l: end if
4141 } assert(U_t != part_tr.succ.back().block_bunch->pred->source);
4142 // Line 3.11l: untested[t] := untested[t] − 1
4143 ++U_t->untested_to_U_eqv.begin;
4144 // Line 3.12l: if untested[t]>0 then Skip state t
4145 if (U_t == U_t->untested_to_U_eqv.
4146 begin->block_bunch->pred->source)
4147 {
4148 goto continuation;
4149 }
4150 // Line 3.13l: if not (B--T--> subset R) then
4151 if (extend_from_splitter == mode)
4152 { assert(U_t != part_tr.succ.front().block_bunch->pred->source);
4153 // Line 3.14l: for all non-inert
4154 // t --alpha--> u do
4155 U_u_iter = U_t->succ_inert.begin; assert(part_tr.succ.data() < U_u_iter);
4156 COROUTINE_WHILE(SPLIT_U_TESTING, U_t ==
4157 U_u_iter[-1].block_bunch->pred->source)
4158 {
4159 U_u_iter=U_u_iter[-1].begin_or_before_end; assert(nullptr != U_u_iter);
4160 /* Line 3.15l: if t --alpha--> u in T */ assert(U_u_iter->block_bunch->pred->source == U_t);
4161 /* then Skip t */ assert(!U_u_iter->block_bunch->slice.is_null());
4162 bisim_dnj::block_bunch_slice_const_iter_t
4163 const block_bunch(
4164 U_u_iter->block_bunch->slice);
4165 if (&*block_bunch == &*splitter_T)
4166 {
4167 goto continuation;
4168 // i. e. break and then continue
4169 }
4170 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4171 bisim_dnj::succ_entry::add_work_to_out_slice(*this, U_u_iter,
4172 /* Line 3.16l: end for */ check_complexity::split_U__test_noninert_transitions, 1U);
4173 #endif
4174 }
4175 END_COROUTINE_WHILE;
4176 // Line 3.17l: end if
4177 } assert(U_nonbottom_end <= U_t->pos);
4178 /* Line 3.18l: Add t to U */ assert(U_t->pos < untested_to_U_defined_end);
4179 std::swap(*U_t->pos, *U_nonbottom_end++);
4180 // Line 3.21l: if |U| > |B|/2 then
4181 if (block_B->size() / 2 <
4182 U_nonbottom_end-block_B->nonbottom_begin +
4183 block_B->unmarked_bottom_size())
4184 {
4185 // Line 3.22l: Abort this coroutine
4186 // As the U-coroutine is now aborted, the
4187 // untested_to_U values are no longer relevant.
4188 // The assignment tells the R-coroutine that it
4189 // doesn't need to make complicated swaps any
4190 // more to keep untested properly initialized.
4191 untested_to_U_defined_end = U_nonbottom_end;
4192 ABORT_THIS_COROUTINE();
4193 // Line 3.23l: end if
4194 }
4195 // Line 3.19l: end for
4196 continuation: mCRL2complexity(U_t_iter, add_work(
4197 check_complexity::split_U__handle_transition_to_U_state, 1U), *this);
4198 }
4199 END_COROUTINE_FOR; mCRL2complexity(U_s_iter->st, add_work(
4200 /* Line 3.20l: end for */ check_complexity::split_U__find_predecessors_of_U_state, 1U), *this);
4201 ++U_s_iter;
4202 if(block_B->marked_bottom_begin == U_s_iter)
4203 {
4204 U_s_iter = block_B->nonbottom_begin;
4205 }
4206 }
4207 END_COROUTINE_DO_WHILE;
4208 }
4209
4210 /*- - - - - - - split off U-block - - - - - - -*/
4211
4212 // Line 3.24l: Abort the other coroutine
4213 ABORT_OTHER_COROUTINE();
4214 // Line 2.17: Pi_s := Pi_s \ { B } union ({ R, U } \ { {} })
4215 // All non-U states are in R.
4216 block_B->marked_nonbottom_begin = U_nonbottom_end;
4217 block_R = block_B;
4218 bisim_dnj::block_t* const block_U(
4219 block_R->split_off_block(bisim_dnj::new_block_is_U, ONLY_IF_DEBUG( *this, )
4220 part_st.nr_of_blocks++));
4221 // Line 2.16: Remove Tprime_B--> = Tprime_R--> from the
4222 // splitter list
4223 /* and the remainder of Line 2.17 */ assert(0 == block_U->marked_size()); assert(0 == block_R->marked_size());
4224 part_tr.adapt_transitions_for_new_block(block_U, block_R, ONLY_IF_DEBUG( *this, )
4225 extend_from_marked_states__add_new_noninert_to_splitter ==
4226 mode, splitter_T, bisim_dnj::new_block_is_U);
4227 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4228 finalise_U_is_smaller(block_U, block_R, *this);
4229 #endif
4230 END_COROUTINE
4231
4232 /*------------------------ find R-states ------------------------*/
4233
4234 COROUTINE
4235 // Line 3.21r: if |R| > |B|/2 then
4236 if (block_B->size() / 2 < block_B->marked_size())
4237 {
4238 // Line 3.22r: Abort this coroutine
4239 ABORT_THIS_COROUTINE();
4240 // Line 3.23r: end if
4241 }
4242
4243 /* - - - - - collect states from B--T--> - - - - - */
4244
4245 if (extend_from_splitter == mode)
4246 {
4247 // Line 3.4r: R := R union B--(T \ Marked(T))-->
4248 if (U_nonbottom_end < block_B->marked_nonbottom_begin)
4249 { assert(part_tr.block_bunch.front().slice != splitter_T);
4250 COROUTINE_WHILE (SPLIT_R_COLLECT_SPLITTER,
4251 R_s_iter.splitter_iter[-1].slice == splitter_T)
4252 { assert(&part_tr.block_bunch.cbegin()[1] < R_s_iter.splitter_iter);
4253 --R_s_iter.splitter_iter;
4254 bisim_dnj::state_info_entry* const s(
4255 R_s_iter.splitter_iter->pred->source); assert(s->bl.ock == block_B); assert(s->pos->st == s);
4256 if (block_B->nonbottom_begin <= s->pos)
4257 { assert(U_nonbottom_end <= s->pos);
4258 if (s->pos < untested_to_U_defined_end)
4259 {
4260 // The non-bottom state has a transition
4261 // to a visited U-state, so untested is
4262 // initialised; however, now it is
4263 // discovered to be in R anyway.
4264 std::swap(*s->pos,
4265 *--untested_to_U_defined_end);
4266 }
4267 if (block_B->mark_nonbottom(s->pos) &&
4268 // Line 3.21r: if |R| > |B|/2 then
4269 block_B->size()/2 < block_B->marked_size())
4270 {
4271 // Line 3.22r: Abort this coroutine
4272 ABORT_THIS_COROUTINE();
4273 // Line 3.23r: end if
4274 }
4275 } else assert(block_B->marked_bottom_begin <= s->pos);
4276 mCRL2complexity(R_s_iter.splitter_iter->pred, add_work(
4277 check_complexity::split_R__handle_transition_from_R_state, 1U), *this);
4278 }
4279 END_COROUTINE_WHILE;
4280
4281 // Indicate to the U-coroutine that all states in
4282 // B--T--> are now in R.
4283 // The shared variable `mode` is used
4284 // instead of a separate shared variable.
4285 mode = extend_from_marked_states;
4286 }
4287 #ifndef NDEBUG
4288 else
4289 {
4290 // assert that all non-marked transitions in `splitter_T` start in
4291 // marked states
4292 assert(part_tr.block_bunch.front().slice != splitter_T);
4293 while (R_s_iter.splitter_iter[-1].slice == splitter_T)
4294 {
4295 assert(&part_tr.block_bunch.cbegin()[1] < R_s_iter.splitter_iter);
4296 --R_s_iter.splitter_iter;
4297 bisim_dnj::state_info_entry* const
4298 s(R_s_iter.splitter_iter->pred->source);
4299 assert(s->bl.ock == block_B); assert(s->pos->st == s);
4300 assert(s->pos < block_B->nonbottom_begin ||
4301 block_B->marked_nonbottom_begin <= s->pos);
4302 assert(block_B->marked_bottom_begin <= s->pos);
4303 }
4304 }
4305 #endif
4306 }
4307
4308 /* - - - - - - - visit R-states - - - - - - - */ assert(0 != block_B->marked_size());
4309
4310 if (U_nonbottom_end < block_B->marked_nonbottom_begin)
4311 {
4312 // Line 3.5r: for all s in R while |R| < |B|/2 do
4313 R_s_iter.block = block_B->nonbottom_begin;
4314 if (block_B->marked_bottom_begin == R_s_iter.block)
4315 {
4316 // It may happen that all found states are non-bottom
4317 // states. (In that case, some of these states will
4318 // become new bottom states.)
4319 R_s_iter.block = block_B->end;
4320 } assert(block_B->marked_nonbottom_begin != R_s_iter.block);
4321 COROUTINE_DO_WHILE(SPLIT_R_STATE_HANDLED,
4322 block_B->marked_nonbottom_begin != R_s_iter.block)
4323 {
4324 --R_s_iter.block; assert(part_tr.pred.back().target != R_s_iter.block->st);
4325 // Line 3.7r: for all inert transitions t--tau-->s do
4326 COROUTINE_FOR (SPLIT_R_PREDECESSOR_HANDLED,
4327 R_t_iter = R_s_iter.block->st->pred_inert.begin,
4328 R_t_iter->target == R_s_iter.block->st, ++R_t_iter)
4329 {
4330 bisim_dnj::state_info_entry* const
4331 t(R_t_iter->source); assert(U_nonbottom_end <= t->pos);
4332 /* Line 3.18r: Add t to R */ assert(t->pos->st == t); assert(t->pos < block_B->end);
4333 if (t->pos < untested_to_U_defined_end)
4334 {
4335 // The state has a transition to a U-state, so
4336 // untested is initialised; however, now it is
4337 // discovered to be in R anyway.
4338 std::swap(*t->pos,
4339 *--untested_to_U_defined_end);
4340 }
4341 if (block_B->mark_nonbottom(t->pos) &&
4342 // Line 3.21r: if |R| > |B|/2 then
4343 block_B->size() / 2 < block_B->marked_size())
4344 {
4345 // Line 3.22r: Abort this coroutine
4346 ABORT_THIS_COROUTINE();
4347 // Line 3.23r: end if
4348 } mCRL2complexity(R_t_iter, add_work(
4349 /* Line 3.19r: end for */ check_complexity::split_R__handle_transition_to_R_state, 1U), *this);
4350 }
4351 END_COROUTINE_FOR; mCRL2complexity(R_s_iter.block->st, add_work(
4352 check_complexity::split_R__find_predecessors_of_R_state,
4353 /* Line 3.20r: end for */ 1U), *this);
4354 if (block_B->marked_bottom_begin == R_s_iter.block &&
4355 R_s_iter.block < block_B->nonbottom_begin)
4356 {
4357 R_s_iter.block = block_B->end;
4358 }
4359 }
4360 END_COROUTINE_DO_WHILE;
4361 }
4362
4363 /*- - - - - - - split off R-block - - - - - - -*/
4364
4365 // Line 3.24r: Abort the other coroutine
4366 ABORT_OTHER_COROUTINE();
4367 // Line 2.17: Pi_s := Pi_s \ { B } union ({ R, U } \ { {} })
4368 // All non-R states are in U.
4369 block_R = block_B->split_off_block(bisim_dnj::new_block_is_R, ONLY_IF_DEBUG( *this, )
4370 part_st.nr_of_blocks++);
4371 // Line 2.16: Remove Tprime_B--> = Tprime_R--> from the
4372 // splitter list
4373 /* and the remainder of Line 2.17 */ assert(0 == block_B->marked_size()); assert(0 == block_R->marked_size());
4374 part_tr.adapt_transitions_for_new_block(block_R, block_B, ONLY_IF_DEBUG( *this, )
4375 extend_from_marked_states__add_new_noninert_to_splitter ==
4376 mode, splitter_T, bisim_dnj::new_block_is_R);
4377 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4378 finalise_R_is_smaller(block_B, block_R, *this);
4379 #endif
4380 END_COROUTINE
4381 END_COROUTINES_SECTION
4382 return block_R;
4383 }
4384
4385 /*-- Handle new non-inert transitions -- Lines 2.22-2.28 in [JGKW2020] --*/
4386
4409 bisim_dnj::block_t* handle_new_noninert_transns(
4410 bisim_dnj::block_t* const block_R,
4411 bisim_dnj::block_bunch_slice_const_iter_t bbslice_Tprime_R)
4412 { assert(block_R == bbslice_Tprime_R->source_block());
4413 bisim_dnj::block_t* block_Rprime; assert(&part_tr.block_bunch.cbegin()[1] < part_tr.block_bunch_inert_begin);
4414 bisim_dnj::block_t* block_N; assert(!part_tr.block_bunch_inert_begin[-1].slice.is_null());
4415 bisim_dnj::block_bunch_slice_iter_t const bbslice_R_tau_U(
4416 part_tr.block_bunch_inert_begin[-1].slice); assert(bbslice_Tprime_R->is_stable());
4417 /* Line 2.23: (N, R') := split(R, R--tau-->U) */ assert(!bbslice_R_tau_U->is_stable());
4418 /* Line 2.24: Remove R--tau-->U from the splitter list */ assert(block_R == bbslice_R_tau_U->source_block());
4419 /* Line 2.25: Pi_s := Pi_s \ { R } union { N, R' } \ { emptyset } */ assert(0 < block_R->marked_size());
4420 // Line 2.26: Add N--tau-->R' to the bunch containing R--tau-->U
4421 if (0 < block_R->unmarked_bottom_size())
4422 { assert(part_tr.splitter_list.begin() != part_tr.splitter_list.end());
4423 #ifndef NDEBUG
4424 bool const next_splitter_is_of_same_block =
4425 part_tr.splitter_list.begin() != bbslice_R_tau_U &&
4426 part_tr.splitter_list.front().source_block() == block_R;
4427 #endif
4428 block_N = split(block_R, bbslice_R_tau_U,
4429 extend_from_marked_states__add_new_noninert_to_splitter); assert(part_st.permutation.data() < block_N->begin);
4430 block_Rprime = block_N->begin[-1].st->bl.ock;
4431 #ifndef NDEBUG
4432 // If the first element of the splitter list was a block_bunch-slice of
4433 // block_N, it was split up. The condition below checks whether the
4434 // N-subblock's (= the block with new bottom states) slice is placed before
4435 // the R'-subblock's (= the block with old bottom states).
4436 if (next_splitter_is_of_same_block &&
4437 (assert(part_tr.splitter_list.begin() != part_tr.splitter_list.end()),
4438 part_tr.splitter_list.front().source_block()==block_N))
4439 {
4440 bisim_dnj::block_bunch_slice_iter_t const bbslice_T_Rprime(
4441 std::next(part_tr.splitter_list.begin()));
4442 if (part_tr.splitter_list.end() != bbslice_T_Rprime &&
4443 bbslice_T_Rprime->source_block() == block_Rprime)
4444 {
4445 // The R'-subblock's slice must be the first in the splitter list.
4446 // This is necessary in Debug-mode to ensure that the cost of
4447 // refining R' is accounted for correctly.
4448 part_tr.splitter_list.splice(part_tr.splitter_list.begin(),
4449 /* If more new noninert transitions are found, we do not need to */ part_tr.splitter_list, bbslice_T_Rprime);
4450 /* separate them further, as every bottom state already has a */ }
4451 /* transition in bbslice_R_tau_U->bunch. */ }
4452 #endif
4453 if (0 < block_N->marked_bottom_size())
4454 {
4455 // Not only new non-inert transitions, but also new bottom
4456 // states have been found. In that case, we also have to
4457 // refine w.r.t. the last splitter, as the new bottom states in
4458 // block_N may be unstable under it. We set the variable
4459 // `bbslice_Tprime_R` to `bbslice_R_tau_U` so it won't disturb
4460 // in the test below.
4461 bbslice_Tprime_R = bbslice_R_tau_U;
4462 block_N->marked_bottom_begin = block_N->nonbottom_begin;
4463 }
4464 else if (bbslice_Tprime_R->source_block() != block_N)
4465 { assert(bbslice_Tprime_R->source_block() == block_Rprime);
4466 // bbslice_Tprime_R contained transitions from every (old and
4467 // new) bottom state in the block. It has been split, and now
4468 // it contains transitions from the block with old bottom
4469 /* states; however, we need the block_bunch-slice with */ assert(!bbslice_Tprime_R->end->slice.is_null());
4470 /* transitions from the block with new bottom states. */ assert(bbslice_Tprime_R->end < part_tr.block_bunch_inert_begin);
4471 bbslice_Tprime_R = (bisim_dnj::block_bunch_slice_const_iter_t)
4472 bbslice_Tprime_R->end->slice; assert(bbslice_Tprime_R->source_block() == block_N);
4473 }
4474 }
4475 else
4476 {
4477 block_N = block_R;
4478 // make bbslice_R_tau_U stable
4479 block_N->stable_block_bunch.splice(
4480 block_N->stable_block_bunch.end(),
4481 part_tr.splitter_list, bbslice_R_tau_U);
4482 bbslice_R_tau_U->make_stable();
4483 block_N->marked_bottom_begin = block_N->nonbottom_begin;
4484 block_Rprime = nullptr;
4485 }
4486 block_N->marked_nonbottom_begin = block_N->end;
4487
4488 if (1 >= block_N->size()) return block_Rprime;
4489
4490 // Line 2.27: Insert all T_N--> as secondary into the splitter list
4491 // However, the bunch of new noninert transitions and the bunch
4492 // that was the last splitter do not need to be handled (as long
4493 // as there are no further new bottom states).
4494 // We cannot do this in time O(1) because we need to call
4495 // `make_unstable()` for each block_bunch-slice individually.
4496 for (bisim_dnj::block_bunch_slice_iter_t bbslice_T_N(
4497 block_N->stable_block_bunch.begin());
4498 block_N->stable_block_bunch.end() != bbslice_T_N; )
4499 { assert(bbslice_T_N->is_stable());
4500 bisim_dnj::block_bunch_slice_iter_t const
4501 next_bbslice_T_N(std::next(bbslice_T_N));
4502 if (&*bbslice_T_N != &*bbslice_Tprime_R &&
4503 &*bbslice_T_N != &*bbslice_R_tau_U)
4504 {
4505 // In Debug mode, we have to place the new splitters at the end
4506 // of the splitter list -- after a refinement with a primary
4507 // splitter, the corresponding refinement with the large
4508 // splitter should follow immediately, to ensure that the cost
4509 // for refining `block_Rprime` is accounted for correctly.
4510 part_tr.splitter_list.splice(part_tr.splitter_list.end(),
4511 block_N->stable_block_bunch, bbslice_T_N);
4512 bbslice_T_N->make_unstable();
4513 }
4514 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4515 // Try to assign this work to a transition from a bottom state in
4516 // bbslice_T_N.
4517 // If that does not succeed, temporarily assign it to the block_bunch
4518 // itself. Later, we shall find a bottom state to which this work can be
4519 // assigned.
4520 assert(!bbslice_T_N->work_counter.has_temporary_work());
4521 if (!bbslice_T_N->add_work_to_bottom_transns(check_complexity::
4522 handle_new_noninert_transns__make_unstable_a_priori, 1U, *this))
4523 { mCRL2complexity(bbslice_T_N, add_work(check_complexity::
4524 handle_new_noninert_transns__make_unstable_temp, 1U), *this);
4525 assert(bbslice_T_N->work_counter.has_temporary_work());
4526 assert(!bbslice_T_N->is_stable());
4527 }
4528 #endif
4529 bbslice_T_N = next_bbslice_T_N;
4530 }
4531
4532 // Line 2.28: For each bottom state, mark one of its outgoing
4533 // transitions in each in every T_N--> where it has one
4534 bisim_dnj::permutation_entry* s_iter(block_N->begin); assert(s_iter < block_N->nonbottom_begin);
4535 do
4536 {
4537 bisim_dnj::state_info_entry* const s(s_iter->st); assert(s->pos == s_iter);
4538 // for all out-slices of s do
4539 for (bisim_dnj::succ_entry* succ_iter(s->succ_inert.begin);
4540 s == succ_iter[-1].block_bunch->pred->source; )
4541 { assert(succ_iter[-1].begin_or_before_end < succ_iter);
4542 succ_iter = succ_iter[-1].begin_or_before_end; assert(nullptr != succ_iter);
4543 /* Mark the first transition in the out-slice in its */ assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
4544 /* block_bunch-slice */ assert(s == succ_iter->block_bunch->pred->source);
4545 bisim_dnj::block_bunch_entry* const
4546 old_block_bunch_pos(succ_iter->block_bunch); assert(!old_block_bunch_pos->slice.is_null());
4547 bisim_dnj::block_bunch_slice_iter_t const
4548 bbslice_T_N((bisim_dnj::block_bunch_slice_iter_t)
4549 old_block_bunch_pos->slice);
4550 if (!bbslice_T_N->is_stable())
4551 { assert(&*bbslice_T_N != &*bbslice_Tprime_R && bbslice_T_N != bbslice_R_tau_U);
4552 bisim_dnj::block_bunch_entry* const
4553 new_block_bunch_pos(bbslice_T_N->marked_begin - 1);
4554 // It may happen that the transition was already paid
4555 // for earlier, namely if it once was in bunch_T
4556 if (old_block_bunch_pos <= new_block_bunch_pos)
4557 {
4558 bbslice_T_N->marked_begin = new_block_bunch_pos; assert(new_block_bunch_pos->slice == bbslice_T_N);
4559 std::swap(old_block_bunch_pos->pred,
4560 new_block_bunch_pos->pred); assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
4561 old_block_bunch_pos->pred->action_block->succ->
4562 block_bunch = old_block_bunch_pos; assert(new_block_bunch_pos->pred->action_block->succ == succ_iter);
4563 succ_iter->block_bunch = new_block_bunch_pos; // add_work(succ_iter->block_bunch->pred, ...) -- subsumed in the call below
4564 }
4565 } else assert(&*bbslice_T_N==&*bbslice_Tprime_R || bbslice_T_N==bbslice_R_tau_U);
4566 } mCRL2complexity(s, add_work(
4567 check_complexity::handle_new_noninert_transns, 1U), *this);
4568 }
4569 while (++s_iter < block_N->nonbottom_begin);
4570
4571 return block_Rprime;
4572 }
4573};
4574
4576 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4577 namespace bisim_dnj {
4578
4586 template <class LTS_TYPE>
4587 static void finalise_U_is_smaller(const block_t* const block_U,
4588 const block_t* const block_R,
4589 const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
4590 {
4591 if (nullptr != block_U)
4592 {
4593 unsigned const max_U_block(check_complexity::log_n -
4594 check_complexity::ilog2(block_U->size()));
4595 // finalise work counters for the U-states and their transitions
4596 const permutation_entry* s_iter(block_U->begin);
4597 assert(s_iter < block_U->end);
4598 do
4599 {
4600 const state_info_entry* const s(s_iter->st);
4601 mCRL2complexity(s, finalise_work(
4602 check_complexity::split_U__find_predecessors_of_U_state,
4603 check_complexity::split__find_predecessors_of_R_or_U_state,
4604 max_U_block), partitioner);
4605 assert(s != partitioner.part_tr.pred.back().target);
4606 for (const pred_entry* pred_iter(s->pred_inert.begin);
4607 s == pred_iter->target; ++pred_iter)
4608 {
4609 mCRL2complexity(pred_iter, finalise_work(check_complexity::
4610 split_U__handle_transition_to_U_state,
4611 check_complexity::
4612 split__handle_transition_to_R_or_U_state,
4613 max_U_block), partitioner);
4614 }
4615 // Sometimes, inert transitions become transitions from R- to
4616 // U-states; therefore, we also have to walk through the
4617 // noninert predecessors of U-states:
4618 assert(s != partitioner.part_tr.pred.front().target);
4619 for (const pred_entry* pred_iter(s->pred_inert.begin);
4620 s == (--pred_iter)->target; )
4621 {
4622 mCRL2complexity(pred_iter, finalise_work(check_complexity::
4623 split_U__handle_transition_to_U_state,
4624 check_complexity::
4625 split__handle_transition_to_R_or_U_state,
4626 max_U_block), partitioner);
4627 }
4628 assert(s != partitioner.part_tr.succ.front().
4629 block_bunch->pred->source);
4630 for (const succ_entry* succ_iter(s->succ_inert.begin);
4631 s == (--succ_iter)->block_bunch->pred->source; )
4632 {
4633 mCRL2complexity(succ_iter->block_bunch->pred,finalise_work(
4634 check_complexity::
4635 split_U__test_noninert_transitions,
4636 check_complexity::
4637 split__handle_transition_from_R_or_U_state,
4638 max_U_block), partitioner);
4639 }
4640 }
4641 while (++s_iter < block_U->end);
4642 }
4643 // cancel work counters for the R-states and their transitions, and
4644 // also account for work done in the U-coroutine on R-states
4645 const permutation_entry* s_iter(block_R->begin);
4646 assert(s_iter < block_R->end);
4647 do
4648 {
4649 const state_info_entry* const s(s_iter->st);
4650 mCRL2complexity(s, cancel_work(check_complexity::
4651 split_R__find_predecessors_of_R_state), partitioner);
4652 assert(s != partitioner.part_tr.pred.back().target);
4653 for (const pred_entry* pred_iter(s->pred_inert.begin);
4654 s == pred_iter->target; ++pred_iter)
4655 {
4656 mCRL2complexity(pred_iter, cancel_work(check_complexity::
4657 split_R__handle_transition_to_R_state), partitioner);
4658 }
4659 assert(s !=
4660 partitioner.part_tr.succ.front().block_bunch->pred->source);
4661 for (const succ_entry* succ_iter(s->succ_inert.begin);
4662 s == (--succ_iter)->block_bunch->pred->source; )
4663 {
4664 mCRL2complexity(succ_iter->block_bunch->pred, cancel_work(
4665 check_complexity::
4666 split_R__handle_transition_from_R_state), partitioner);
4667 // the following counter measures work done in the
4668 // U-coroutine that found R-states.
4669 mCRL2complexity(succ_iter->block_bunch->pred,finalise_work(
4670 check_complexity::
4671 split_U__test_noninert_transitions,
4672 check_complexity::
4673 split__test_noninert_transitions_found_new_bottom_state,
4674 1U), partitioner);
4675 }
4676 }
4677 while (++s_iter < block_R->end);
4678
4679 check_complexity::check_temporary_work();
4680 (void) partitioner; // avoid unused variable warning
4681 }
4682
4690 template <class LTS_TYPE>
4691 static void finalise_R_is_smaller(const block_t* const block_U,
4692 const block_t* const block_R,
4693 const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
4694 {
4695 unsigned const max_R_block(check_complexity::log_n -
4696 check_complexity::ilog2(block_R->size()));
4697 // cancel work counters for the U-states and their transitions
4698 const permutation_entry* s_iter(block_U->begin);
4699 assert(s_iter < block_U->end);
4700 do
4701 {
4702 const state_info_entry* const s(s_iter->st);
4703 mCRL2complexity(s, cancel_work(check_complexity::
4704 split_U__find_predecessors_of_U_state), partitioner);
4705 assert(s != partitioner.part_tr.pred.back().target);
4706 for (const pred_entry* pred_iter(s->pred_inert.begin);
4707 s == pred_iter->target; ++pred_iter)
4708 {
4709 mCRL2complexity(pred_iter, cancel_work(check_complexity::
4710 split_U__handle_transition_to_U_state), partitioner);
4711 }
4712 // Sometimes, inert transitions become transitions from R- to
4713 // U-states; therefore, we also have to walk through the
4714 // noninert predecessors of U-states:
4715 assert(s != partitioner.part_tr.pred.front().target);
4716 for (const pred_entry* pred_iter(s->pred_inert.begin);
4717 s == (--pred_iter)->target; )
4718 {
4719 mCRL2complexity(pred_iter, cancel_work(check_complexity::
4720 split_U__handle_transition_to_U_state), partitioner);
4721 }
4722 assert(s !=
4723 partitioner.part_tr.succ.front().block_bunch->pred->source);
4724 for (const succ_entry* succ_iter(s->succ_inert.begin);
4725 s == (--succ_iter)->block_bunch->pred->source; )
4726 {
4727 mCRL2complexity(succ_iter->block_bunch->pred, cancel_work(
4728 check_complexity::
4729 split_U__test_noninert_transitions), partitioner);
4730 }
4731 }
4732 while (++s_iter < block_U->end);
4733 // finalise work counters for the R-states and their transitions
4734 s_iter = block_R->begin;
4735 assert(s_iter < block_R->end);
4736 do
4737 {
4738 const state_info_entry* const s(s_iter->st);
4739 mCRL2complexity(s, finalise_work(
4740 check_complexity::split_R__find_predecessors_of_R_state,
4741 check_complexity::split__find_predecessors_of_R_or_U_state,
4742 max_R_block), partitioner);
4743 assert(s != partitioner.part_tr.pred.back().target);
4744 for (const pred_entry* pred_iter(s->pred_inert.begin);
4745 s == pred_iter->target; ++pred_iter)
4746 {
4747 mCRL2complexity(pred_iter, finalise_work(
4748 check_complexity::split_R__handle_transition_to_R_state,
4749 check_complexity::split__handle_transition_to_R_or_U_state,
4750 max_R_block), partitioner);
4751 }
4752 assert(s !=
4753 partitioner.part_tr.succ.front().block_bunch->pred->source);
4754 for (const succ_entry* succ_iter(s->succ_inert.begin);
4755 s == (--succ_iter)->block_bunch->pred->source; )
4756 {
4757 mCRL2complexity(succ_iter->block_bunch->pred, finalise_work(
4758 check_complexity::
4759 split_R__handle_transition_from_R_state,
4760 check_complexity::
4761 split__handle_transition_from_R_or_U_state,
4762 max_R_block), partitioner);
4763 // the following counter actually is work done in the
4764 // U-coroutine that found R-states.
4765 mCRL2complexity(succ_iter->block_bunch->pred, cancel_work(
4766 check_complexity::
4767 split_U__test_noninert_transitions), partitioner);
4768 }
4769 }
4770 while (++s_iter < block_R->end);
4771 check_complexity::check_temporary_work();
4772 (void) partitioner; // avoid unused variable warning
4773 }
4774
4775 } // end namespace bisim_dnj
4776 #endif
4777
4778
4779
4780
4781
4782/* ************************************************************************* */
4783/* */
4784/* I N T E R F A C E */
4785/* */
4786/* ************************************************************************* */
4787
4788
4789
4790
4791
4797
4807template <class LTS_TYPE>
4808void bisimulation_reduce_dnj(LTS_TYPE& l, bool const branching = false,
4809 bool const preserve_divergence = false)
4810{
4811 if (1 >= l.num_states())
4812 {
4813 // LTSs with 1 state also need to be reduced because some users call
4814 // bisimulation minimisation just to remove duplicated transitions.
4815 mCRL2log(log::warning) << "There is only 1 state in the LTS. It is "
4816 "not guaranteed that branching bisimulation minimisation runs "
4817 "in time O(m log n).\n";
4818 }
4819 // Line 2.1: Find tau-SCCs and contract each of them to a single state
4820 const std::clock_t start_SCC=std::clock();
4821 mCRL2log(log::verbose) << "Start SCC\n";
4822 if (branching)
4823 {
4824 scc_reduce(l, preserve_divergence);
4825 // If only 1 state remains after this contraction, we are already
4826 // finished because scc_reduce() also removes duplicated transitions.
4827 if (1 >= l.num_states()) return;
4828 }
4829 // Now apply the branching bisimulation reduction algorithm. If there
4830 // are no taus, this will automatically yield strong bisimulation.
4831 const std::clock_t start_part=std::clock();
4832 mCRL2log(log::verbose) << "Start Partitioning\n";
4833 bisim_partitioner_dnj<LTS_TYPE> bisim_part(l, branching,
4834 preserve_divergence);
4835
4836 // Assign the reduced LTS
4837 const std::clock_t end_part=std::clock();
4838 mCRL2log(log::verbose) << "Start finalizing\n";
4839 bisim_part.finalize_minimized_LTS();
4840
4841 if (mCRL2logEnabled(log::verbose))
4842 {
4843 const std::clock_t end_finalizing=std::clock();
4844 const int prec=std::lrint(std::log10(CLOCKS_PER_SEC)+0.19897000433602);
4845 // For example, if CLOCKS_PER_SEC>= 20: >=2 digits
4846 // If CLOCKS_PER_SEC>= 200: >=3 digits
4847 // If CLOCKS_PER_SEC>=2000000: >=7 digits
4848
4849 double runtime[5];
4850 runtime[0]=(double) (end_finalizing - start_SCC)/CLOCKS_PER_SEC; // total time
4851 runtime[1]=(double) ( start_part-start_SCC)/CLOCKS_PER_SEC;
4852 runtime[2]=(double) ( bisim_part.end_initial_part-start_part )/CLOCKS_PER_SEC;
4853 runtime[3]=(double) ( end_part-bisim_part.end_initial_part )/CLOCKS_PER_SEC;
4854 runtime[4]=(double) (end_finalizing-end_part )/CLOCKS_PER_SEC;
4855 if (runtime[0]>=60.0)
4856 {
4857 int min[sizeof(runtime)/sizeof(runtime[0])];
4858 for (unsigned i = 0; i < sizeof(runtime)/sizeof(runtime[0]); ++i)
4859 {
4860 min[i] = trunc(runtime[i] / 60.0);
4861 runtime[i] -= 60 * min[i];
4862 }
4863 if (min[0]>=60)
4864 {
4865 int h[sizeof(runtime)/sizeof(runtime[0])];
4866 for (unsigned i=0; i < sizeof(runtime)/sizeof(runtime[0]); ++i)
4867 {
4868 h[i] = min[i] / 60;
4869 min[i] %= 60;
4870 }
4871 int width = trunc(log10(h[0])) + 1;
4872
4873 mCRL2log(log::verbose) << std::fixed << std::setprecision(prec)
4874 << "Time spent on contracting SCCs: " << std::setw(width) << h[1] << "h " << std::setw(2) << min[1] << "min " << std::setw(prec+3) << runtime[1] << "s\n"
4875 "Time spent on initial partition:" << std::setw(width) << h[2] << "h " << std::setw(2) << min[2] << "min " << std::setw(prec+3) << runtime[2] << "s\n"
4876 "Time spent on refining: " << std::setw(width) << h[3] << "h " << std::setw(2) << min[3] << "min " << std::setw(prec+3) << runtime[3] << "s\n"
4877 "Time spent on finalizing: " << std::setw(width) << h[4] << "h " << std::setw(2) << min[4] << "min " << std::setw(prec+3) << runtime[4] << "s\n"
4878 "Total CPU time: " << std::setw(width) << h[0] << "h " << std::setw(2) << min[0] << "min " << std::setw(prec+3) << runtime[0] << "s\n"
4879 << std::defaultfloat;
4880 }
4881 else
4882 {
4883 mCRL2log(log::verbose) << std::fixed << std::setprecision(prec)
4884 << "Time spent on contracting SCCs: " << std::setw(2) << min[1] << "min " << std::setw(prec+3) << runtime[1] << "s\n"
4885 "Time spent on initial partition:" << std::setw(2) << min[2] << "min " << std::setw(prec+3) << runtime[2] << "s\n"
4886 "Time spent on refining: " << std::setw(2) << min[3] << "min " << std::setw(prec+3) << runtime[3] << "s\n"
4887 "Time spent on finalizing: " << std::setw(2) << min[4] << "min " << std::setw(prec+3) << runtime[4] << "s\n"
4888 "Total CPU time: " << std::setw(2) << min[0] << "min " << std::setw(prec+3) << runtime[0] << "s\n"
4889 << std::defaultfloat;
4890 }
4891 }
4892 else
4893 {
4894 mCRL2log(log::verbose) << std::fixed << std::setprecision(prec)
4895 << "Time spent on contracting SCCs: " << std::setw(prec+3) << runtime[1] << "s\n"
4896 "Time spent on initial partition:" << std::setw(prec+3) << runtime[2] << "s\n"
4897 "Time spent on refining: " << std::setw(prec+3) << runtime[3] << "s\n"
4898 "Time spent on finalizing: " << std::setw(prec+3) << runtime[4] << "s\n"
4899 "Total CPU time: " << std::setw(prec+3) << runtime[0] << "s\n"
4900 << std::defaultfloat;
4901 }
4902 }
4903}
4904
4905
4925template <class LTS_TYPE>
4926bool destructive_bisimulation_compare_dnj(LTS_TYPE& l1, LTS_TYPE& l2,
4927 bool const branching = false, bool const preserve_divergence = false,
4928 bool const generate_counter_examples = false,
4929 const std::string& /*counter_example_file*/ = "",
4930 bool /*structured_output*/ = false)
4931{
4932 if (generate_counter_examples)
4933 {
4934 mCRL2log(log::warning) << "The JGKW20 branching bisimulation "
4935 "algorithm does not generate counterexamples.\n";
4936 }
4937 std::size_t init_l2(l2.initial_state() + l1.num_states());
4938 detail::merge(l1, std::move(l2));
4939 l2.clear(); // No use for l2 anymore.
4940
4941 // Line 2.1: Find tau-SCCs and contract each of them to a single state
4942 if (branching)
4943 {
4944 scc_partitioner<LTS_TYPE> scc_part(l1);
4945 scc_part.replace_transition_system(preserve_divergence);
4946 init_l2 = scc_part.get_eq_class(init_l2);
4947 } else assert(!preserve_divergence);
4948 assert(1 < l1.num_states());
4949 bisim_partitioner_dnj<LTS_TYPE> bisim_part(l1, branching,
4950 preserve_divergence);
4951
4952 return bisim_part.in_same_class(l1.initial_state(), init_l2);
4953}
4954
4955
4972template <class LTS_TYPE>
4973inline bool bisimulation_compare_dnj(const LTS_TYPE& l1, const LTS_TYPE& l2,
4974 bool const branching = false, bool const preserve_divergence = false)
4975{
4976 LTS_TYPE l1_copy(l1);
4977 LTS_TYPE l2_copy(l2);
4978 return destructive_bisimulation_compare_dnj(l1_copy, l2_copy, branching,
4979 preserve_divergence);
4980}
4981
4983
4984} // end namespace detail
4985} // end namespace lts
4986} // end namespace mcrl2
4987
4988#endif // ifndef LIBLTS_BISIM_DNJ_H
check_complexity.h
helper class for time complexity checks during test runs
mCRL2complexity
#define mCRL2complexity(unit, call, info_for_debug)
Assigns work to a counter and checks for errors.
Definition check_complexity.h:1941
atermpp::term_balanced_tree
Read-only balanced binary tree of terms.
Definition aterm_balanced_tree.h:40
atermpp::term_balanced_tree::begin
iterator begin() const
Returns an iterator pointing to the beginning of the term_balanced_tree.
Definition aterm_balanced_tree.h:402
mcrl2::lts::detail::bisim_dnj::action_block_entry
information about a transition sorted per (action, target block) pair
Definition liblts_bisim_dnj.h:895
mcrl2::lts::detail::bisim_dnj::action_block_entry::begin_or_before_end
action_block_entry * begin_or_before_end
pointer to delimit the slice of transitions in the same (action, block) pair
Definition liblts_bisim_dnj.h:913
mcrl2::lts::detail::bisim_dnj::action_block_entry::succ
succ_entry * succ
circular iterator to link the four transition arrays
Definition liblts_bisim_dnj.h:902
mcrl2::lts::detail::bisim_dnj::action_block_entry::action_block_slice_begin
action_block_entry * action_block_slice_begin(ONLY_IF_DEBUG(const action_block_entry *const action_block_begin, const action_block_entry *const action_block_orig_inert_begin))
find the beginning of the action_block-slice
Definition liblts_bisim_dnj.h:917
mcrl2::lts::detail::bisim_dnj::block_bunch_entry
information about a transition grouped per (source block, bunch) pair
Definition liblts_bisim_dnj.h:830
mcrl2::lts::detail::bisim_dnj::block_bunch_entry::slice
block_bunch_slice_iter_or_null_t slice
block_bunch-slice of which this transition is part
Definition liblts_bisim_dnj.h:837
mcrl2::lts::detail::bisim_dnj::block_bunch_entry::pred
pred_entry * pred
circular iterator to link the four transition arrays
Definition liblts_bisim_dnj.h:833
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t
Information about a set of transitions with the same source block, in the same bunch.
Definition liblts_bisim_dnj.h:1106
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::make_unstable
void make_unstable()
register that the block_bunch-slice is not stable
Definition liblts_bisim_dnj.h:1134
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::is_stable
bool is_stable() const
returns true iff the block_bunch-slice is registered as stable
Definition liblts_bisim_dnj.h:1123
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::empty
bool empty() const
returns true iff the block_bunch-slice is empty
Definition liblts_bisim_dnj.h:1154
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::work_counter
check_complexity::block_bunch_dnj_counter_t work_counter
Definition liblts_bisim_dnj.h:1249
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::add_work_to_bottom_transns
bool add_work_to_bottom_transns(enum check_complexity::counter_type const ctr, unsigned const max_value, const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
add work to transitions starting in bottom states
Definition liblts_bisim_dnj.h:1219
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::block_bunch_slice_t
block_bunch_slice_t(block_bunch_entry *const new_end, bunch_t *const new_bunch, bool const new_is_stable)
constructor
Definition liblts_bisim_dnj.h:1141
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::bunch
bunch_t * bunch
bunch to which this slice belongs
Definition liblts_bisim_dnj.h:1114
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::debug_id
std::string debug_id(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print a block_bunch-slice identification for debugging
Definition liblts_bisim_dnj.h:1170
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::end
block_bunch_entry * end
pointer past the end of the transitions in the block_bunch array
Definition liblts_bisim_dnj.h:1111
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::make_stable
void make_stable()
register that the block_bunch-slice is stable
Definition liblts_bisim_dnj.h:1127
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::marked_begin
block_bunch_entry * marked_begin
pointer to the first marked transition in the block_bunch array
Definition liblts_bisim_dnj.h:1119
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::source_block
block_t * source_block() const
compute the source block of the transitions in this slice
Definition liblts_bisim_dnj.h:1163
mcrl2::lts::detail::bisim_dnj::block_t
stores information about a block
Definition liblts_bisim_dnj.h:348
mcrl2::lts::detail::bisim_dnj::block_t::debug_id
std::string debug_id(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print a block identification for debugging
Definition liblts_bisim_dnj.h:498
mcrl2::lts::detail::bisim_dnj::block_t::size
state_type size() const
provides the number of states in the block
Definition liblts_bisim_dnj.h:395
mcrl2::lts::detail::bisim_dnj::block_t::nonbottom_begin
permutation_entry * nonbottom_begin
iterator to the first non-bottom state of the block
Definition liblts_bisim_dnj.h:357
mcrl2::lts::detail::bisim_dnj::block_t::begin
permutation_entry * begin
iterator to the first state of the block
Definition liblts_bisim_dnj.h:351
mcrl2::lts::detail::bisim_dnj::block_t::mark_nonbottom
bool mark_nonbottom(permutation_entry *const s)
mark a non-bottom state
Definition liblts_bisim_dnj.h:451
mcrl2::lts::detail::bisim_dnj::block_t::work_counter
check_complexity::block_dnj_counter_t work_counter
Definition liblts_bisim_dnj.h:513
mcrl2::lts::detail::bisim_dnj::block_t::marked_bottom_begin
permutation_entry * marked_bottom_begin
iterator to the first marked bottom state of the block
Definition liblts_bisim_dnj.h:354
mcrl2::lts::detail::bisim_dnj::block_t::marked_size
state_type marked_size() const
provides the number of marked states in the block
Definition liblts_bisim_dnj.h:422
mcrl2::lts::detail::bisim_dnj::block_t::marked_bottom_size
state_type marked_bottom_size() const
provides the number of marked bottom states in the block
Definition liblts_bisim_dnj.h:413
mcrl2::lts::detail::bisim_dnj::block_t::end
permutation_entry * end
iterator past the last state of the block
Definition liblts_bisim_dnj.h:363
mcrl2::lts::detail::bisim_dnj::block_t::stable_block_bunch
simple_list< block_bunch_slice_t > stable_block_bunch
list of stable block_bunch-slices with transitions from this block
Definition liblts_bisim_dnj.h:367
mcrl2::lts::detail::bisim_dnj::block_t::unmarked_bottom_size
state_type unmarked_bottom_size() const
provides the number of unmarked bottom states in the block
Definition liblts_bisim_dnj.h:429
mcrl2::lts::detail::bisim_dnj::block_t::bottom_size
state_type bottom_size() const
provides the number of bottom states in the block
Definition liblts_bisim_dnj.h:404
mcrl2::lts::detail::bisim_dnj::block_t::mark
bool mark(permutation_entry *const s)
mark a state
Definition liblts_bisim_dnj.h:468
mcrl2::lts::detail::bisim_dnj::block_t::seqnr
const state_type seqnr
unique sequence number of this block
Definition liblts_bisim_dnj.h:372
mcrl2::lts::detail::bisim_dnj::block_t::marked_nonbottom_begin
permutation_entry * marked_nonbottom_begin
iterator to the first marked non-bottom state of the block
Definition liblts_bisim_dnj.h:360
mcrl2::lts::detail::bisim_dnj::block_t::block_t
block_t(permutation_entry *const new_begin, permutation_entry *const new_end, state_type const new_seqnr)
constructor
Definition liblts_bisim_dnj.h:381
mcrl2::lts::detail::bisim_dnj::block_t::unmarked_nonbottom_size
state_type unmarked_nonbottom_size() const
provides the number of unmarked nonbottom states in the block
Definition liblts_bisim_dnj.h:438
mcrl2::lts::detail::bisim_dnj::bunch_t
bunch of transitions
Definition liblts_bisim_dnj.h:948
mcrl2::lts::detail::bisim_dnj::bunch_t::end
action_block_entry * end
pointer past the last transition in the bunch
Definition liblts_bisim_dnj.h:954
mcrl2::lts::detail::bisim_dnj::bunch_t::debug_id
std::string debug_id(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print a long bunch identification for debugging
Definition liblts_bisim_dnj.h:1022
mcrl2::lts::detail::bisim_dnj::bunch_t::debug_id_short
std::string debug_id_short(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print a short bunch identification for debugging
Definition liblts_bisim_dnj.h:1010
mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label
union mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t next_nontrivial_and_label
mcrl2::lts::detail::bisim_dnj::bunch_t::begin
action_block_entry * begin
first transition in the bunch
Definition liblts_bisim_dnj.h:951
mcrl2::lts::detail::bisim_dnj::bunch_t::max_work_counter
int max_work_counter(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
calculates the maximal allowed value for work counters associated with this bunch
Definition liblts_bisim_dnj.h:1063
mcrl2::lts::detail::bisim_dnj::bunch_t::work_counter
check_complexity::bunch_dnj_counter_t work_counter
Definition liblts_bisim_dnj.h:1084
mcrl2::lts::detail::bisim_dnj::bunch_t::is_trivial
bool is_trivial() const
returns true iff the bunch is trivial
Definition liblts_bisim_dnj.h:994
mcrl2::lts::detail::bisim_dnj::bunch_t::bunch_t
bunch_t(action_block_entry *const new_begin, action_block_entry *const new_end)
constructor
Definition liblts_bisim_dnj.h:982
mcrl2::lts::detail::bisim_dnj::part_state_t
refinable partition data structure
Definition liblts_bisim_dnj.h:523
mcrl2::lts::detail::bisim_dnj::part_state_t::assert_consistency
void assert_consistency(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
asserts that the partition of states is consistent
Definition liblts_bisim_dnj.h:665
mcrl2::lts::detail::bisim_dnj::part_state_t::state_info
fixed_vector< state_info_entry > state_info
array with all other information about states
Definition liblts_bisim_dnj.h:532
mcrl2::lts::detail::bisim_dnj::part_state_t::~part_state_t
~part_state_t()
destructor
Definition liblts_bisim_dnj.h:570
mcrl2::lts::detail::bisim_dnj::part_state_t::nr_of_blocks
state_type nr_of_blocks
total number of blocks with unique sequence number allocated
Definition liblts_bisim_dnj.h:537
mcrl2::lts::detail::bisim_dnj::part_state_t::print_block
void print_block(const block_t *const B, const char *const message, const permutation_entry *begin_print, const permutation_entry *const end_print, const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print a slice of the partition (typically a block)
Definition liblts_bisim_dnj.h:606
mcrl2::lts::detail::bisim_dnj::part_state_t::permutation
permutation_t permutation
permutation array
Definition liblts_bisim_dnj.h:529
mcrl2::lts::detail::bisim_dnj::part_state_t::block
const block_t * block(state_type const s) const
find the block of a state
Definition liblts_bisim_dnj.h:592
mcrl2::lts::detail::bisim_dnj::part_state_t::part_state_t
part_state_t(state_type const num_states)
constructor
Definition liblts_bisim_dnj.h:545
mcrl2::lts::detail::bisim_dnj::part_state_t::state_size
state_type state_size() const
calculate the size of the state space
Definition liblts_bisim_dnj.h:586
mcrl2::lts::detail::bisim_dnj::part_state_t::print_part
void print_part(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print the partition per block
Definition liblts_bisim_dnj.h:641
mcrl2::lts::detail::bisim_dnj::part_trans_t
Definition liblts_bisim_dnj.h:1315
mcrl2::lts::detail::bisim_dnj::part_trans_t::pred
fixed_vector< pred_entry > pred
array containing all predecessor entries
Definition liblts_bisim_dnj.h:1333
mcrl2::lts::detail::bisim_dnj::part_trans_t::nr_of_new_bottom_states
state_type nr_of_new_bottom_states
number of new bottom states found until now.
Definition liblts_bisim_dnj.h:1365
mcrl2::lts::detail::bisim_dnj::part_trans_t::action_block_inert_begin
action_block_entry * action_block_inert_begin
pointer to the first inert transition in action_block
Definition liblts_bisim_dnj.h:1348
mcrl2::lts::detail::bisim_dnj::part_trans_t::nr_of_nontrivial_bunches
trans_type nr_of_nontrivial_bunches
Definition liblts_bisim_dnj.h:1369
mcrl2::lts::detail::bisim_dnj::part_trans_t::block_bunch
fixed_vector< block_bunch_entry > block_bunch
array containing all block_bunch entries
Definition liblts_bisim_dnj.h:1327
mcrl2::lts::detail::bisim_dnj::part_trans_t::block_bunch_inert_begin
block_bunch_entry * block_bunch_inert_begin
pointer to the first inert transition in block_bunch
Definition liblts_bisim_dnj.h:1345
mcrl2::lts::detail::bisim_dnj::part_trans_t::~part_trans_t
~part_trans_t()
destructor
Definition liblts_bisim_dnj.h:1410
mcrl2::lts::detail::bisim_dnj::part_trans_t::action_block_orig_inert_begin
const action_block_entry * action_block_orig_inert_begin
pointer to the first inert transition in the initial partition
Definition liblts_bisim_dnj.h:1351
mcrl2::lts::detail::bisim_dnj::part_trans_t::second_move_transition_to_new_action_block
void second_move_transition_to_new_action_block(pred_entry *const pred_iter)
handle one transition after a block has been split, phase 2
Definition liblts_bisim_dnj.h:2031
mcrl2::lts::detail::bisim_dnj::part_trans_t::succ
fixed_vector< succ_entry > succ
array containing all successor entries
Definition liblts_bisim_dnj.h:1321
mcrl2::lts::detail::bisim_dnj::part_trans_t::move_out_slice_to_new_block
succ_entry * move_out_slice_to_new_block(succ_entry *out_slice_end, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) block_t *const old_block, block_bunch_slice_const_iter_t const splitter_T)
Adapt the non-inert transitions in an out-slice to a new block.
Definition liblts_bisim_dnj.h:1769
mcrl2::lts::detail::bisim_dnj::part_trans_t::make_noninert
bool make_noninert(pred_entry *const old_pred_pos, block_bunch_slice_iter_or_null_t *const new_noninert_block_bunch_ptr)
adapt data structures for a transition that has become non-inert
Definition liblts_bisim_dnj.h:2090
mcrl2::lts::detail::bisim_dnj::part_trans_t::part_trans_t
part_trans_t(trans_type num_transitions, trans_type num_actions)
constructor
Definition liblts_bisim_dnj.h:1381
mcrl2::lts::detail::bisim_dnj::part_trans_t::print_trans
void print_trans(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print all transitions
Definition liblts_bisim_dnj.h:2468
mcrl2::lts::detail::bisim_dnj::part_trans_t::splitter_list
simple_list< block_bunch_slice_t > splitter_list
list of unstable block_bunch-slices
Definition liblts_bisim_dnj.h:1354
mcrl2::lts::detail::bisim_dnj::part_trans_t::nr_of_block_bunch_slices
trans_type nr_of_block_bunch_slices
Definition liblts_bisim_dnj.h:1371
mcrl2::lts::detail::bisim_dnj::part_trans_t::first_move_transition_to_new_bunch
void first_move_transition_to_new_bunch(action_block_entry *const action_block_iter, bunch_t *const bunch_T_a_Bprime, bool const first_transition_of_state)
transition is moved to a new bunch
Definition liblts_bisim_dnj.h:1497
mcrl2::lts::detail::bisim_dnj::part_trans_t::nr_of_action_block_slices
trans_type nr_of_action_block_slices
Definition liblts_bisim_dnj.h:1370
mcrl2::lts::detail::bisim_dnj::part_trans_t::make_nontrivial
void make_nontrivial(bunch_t *const bunch)
insert a bunch into the list of nontrivial bunches
Definition liblts_bisim_dnj.h:1448
mcrl2::lts::detail::bisim_dnj::part_trans_t::action_block
fixed_vector< action_block_entry > action_block
array containing all action_block entries
Definition liblts_bisim_dnj.h:1342
mcrl2::lts::detail::bisim_dnj::part_trans_t::adapt_transitions_for_new_block
void adapt_transitions_for_new_block(block_t *const new_block, block_t *const old_block, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) bool const add_new_noninert_to_splitter, const block_bunch_slice_iter_t splitter_T, enum new_block_mode_t const new_block_mode)
Split all data structures after a new block has been created.
Definition liblts_bisim_dnj.h:2321
mcrl2::lts::detail::bisim_dnj::part_trans_t::get_some_nontrivial
bunch_t * get_some_nontrivial()
provide some bunch from the list of non-trivial bunches
Definition liblts_bisim_dnj.h:1440
mcrl2::lts::detail::bisim_dnj::part_trans_t::first_move_transition_to_new_action_block
void first_move_transition_to_new_action_block(pred_entry *const pred_iter)
handle one transition after a block has been split
Definition liblts_bisim_dnj.h:1948
mcrl2::lts::detail::bisim_dnj::part_trans_t::nr_of_bunches
trans_type nr_of_bunches
counters to measure progress
Definition liblts_bisim_dnj.h:1368
mcrl2::lts::detail::bisim_dnj::part_trans_t::make_trivial
void make_trivial(bunch_t *const bunch)
remove a bunch from the list of nontrivial bunches
Definition liblts_bisim_dnj.h:1465
mcrl2::lts::detail::bisim_dnj::part_trans_t::second_move_transition_to_new_bunch
void second_move_transition_to_new_bunch(action_block_entry *const action_block_iter, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner, bunch_t *const bunch_T_a_Bprime,) bunch_t *const large_splitter_bunch)
transition is moved to a new bunch, phase 2
Definition liblts_bisim_dnj.h:1650
mcrl2::lts::detail::bisim_dnj::part_trans_t::first_nontrivial
bunch_t * first_nontrivial
pointer to first non-trivial bunch
Definition liblts_bisim_dnj.h:1357
mcrl2::lts::detail::bisim_dnj::permutation_entry
entry in the permutation array
Definition liblts_bisim_dnj.h:292
mcrl2::lts::detail::bisim_dnj::permutation_entry::permutation_entry
permutation_entry(const permutation_entry &&other) noexcept
move constructor
Definition liblts_bisim_dnj.h:305
mcrl2::lts::detail::bisim_dnj::permutation_entry::permutation_entry
permutation_entry()=default
default constructor (should not be deleted)
mcrl2::lts::detail::bisim_dnj::permutation_entry::operator=
void operator=(const permutation_entry &&other) noexcept
move assignment operator
Definition liblts_bisim_dnj.h:316
mcrl2::lts::detail::bisim_dnj::permutation_entry::st
state_info_entry * st
pointer to the state information data structure
Definition liblts_bisim_dnj.h:295
mcrl2::lts::detail::bisim_dnj::pred_entry
information about a transition sorted per target state
Definition liblts_bisim_dnj.h:847
mcrl2::lts::detail::bisim_dnj::pred_entry::target
state_info_entry * target
target state of the transition
Definition liblts_bisim_dnj.h:856
mcrl2::lts::detail::bisim_dnj::pred_entry::action_block
action_block_entry * action_block
circular iterator to link the four transition arrays
Definition liblts_bisim_dnj.h:850
mcrl2::lts::detail::bisim_dnj::pred_entry::debug_id_short
std::string debug_id_short(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print a short transition identification for debugging
Definition liblts_bisim_dnj.h:860
mcrl2::lts::detail::bisim_dnj::pred_entry::source
state_info_entry * source
source state of the transition
Definition liblts_bisim_dnj.h:853
mcrl2::lts::detail::bisim_dnj::pred_entry::debug_id
std::string debug_id(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print a transition identification for debugging
Definition liblts_bisim_dnj.h:869
mcrl2::lts::detail::bisim_dnj::pred_entry::work_counter
check_complexity::trans_dnj_counter_t work_counter
Definition liblts_bisim_dnj.h:887
mcrl2::lts::detail::bisim_dnj::state_info_entry
stores information about a single state
Definition liblts_bisim_dnj.h:218
mcrl2::lts::detail::bisim_dnj::state_info_entry::pos
permutation_entry * pos
position of the state in the permutation array
Definition liblts_bisim_dnj.h:250
mcrl2::lts::detail::bisim_dnj::state_info_entry::pred_inert
iterator_or_counter< pred_entry * > pred_inert
iterator to first inert incoming transition
Definition liblts_bisim_dnj.h:227
mcrl2::lts::detail::bisim_dnj::state_info_entry::bl
union mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t bl
mcrl2::lts::detail::bisim_dnj::state_info_entry::work_counter
check_complexity::state_dnj_counter_t work_counter
Definition liblts_bisim_dnj.h:286
mcrl2::lts::detail::bisim_dnj::state_info_entry::debug_id_short
std::string debug_id_short(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print a short state identification for debugging
Definition liblts_bisim_dnj.h:270
mcrl2::lts::detail::bisim_dnj::state_info_entry::untested_to_U_eqv
iterator_or_counter< succ_entry * > untested_to_U_eqv
number of inert transitions to non-U-states
Definition liblts_bisim_dnj.h:266
mcrl2::lts::detail::bisim_dnj::state_info_entry::succ_inert
iterator_or_counter< succ_entry * > succ_inert
iterator to first inert outgoing transition
Definition liblts_bisim_dnj.h:236
mcrl2::lts::detail::bisim_dnj::state_info_entry::debug_id
std::string debug_id(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
print a state identification for debugging
Definition liblts_bisim_dnj.h:279
mcrl2::lts::detail::bisim_dnj::succ_entry
information about a transition sorted per source state
Definition liblts_bisim_dnj.h:783
mcrl2::lts::detail::bisim_dnj::succ_entry::begin_or_before_end
succ_entry * begin_or_before_end
pointer to delimit the slice of transitions in the same bunch
Definition liblts_bisim_dnj.h:796
mcrl2::lts::detail::bisim_dnj::succ_entry::block_bunch
block_bunch_entry * block_bunch
circular iterator to link the four transition arrays
Definition liblts_bisim_dnj.h:786
mcrl2::lts::detail::bisim_partitioner_dnj
implements the main algorithm for the branching bisimulation quotient
Definition liblts_bisim_dnj.h:2796
mcrl2::lts::detail::bisim_partitioner_dnj::refine_partition_until_it_becomes_stable
void refine_partition_until_it_becomes_stable()
Run (branching) bisimulation minimisation in time O(m log n)
Definition liblts_bisim_dnj.h:3638
mcrl2::lts::detail::bisim_partitioner_dnj::num_eq_classes
state_type num_eq_classes() const
Calculate the number of equivalence classes.
Definition liblts_bisim_dnj.h:2876
mcrl2::lts::detail::bisim_partitioner_dnj::create_initial_partition
void create_initial_partition()
Create a partition satisfying the main invariant.
Definition liblts_bisim_dnj.h:3001
mcrl2::lts::detail::bisim_partitioner_dnj::in_same_class
bool in_same_class(state_type const s, state_type const t) const
Check whether two states are in the same equivalence class.
Definition liblts_bisim_dnj.h:2971
mcrl2::lts::detail::bisim_partitioner_dnj::handle_new_noninert_transns
bisim_dnj::block_t * handle_new_noninert_transns(bisim_dnj::block_t *const block_R, bisim_dnj::block_bunch_slice_const_iter_t bbslice_Tprime_R)
Handle a block with new non-inert transitions.
Definition liblts_bisim_dnj.h:4409
mcrl2::lts::detail::bisim_partitioner_dnj::assert_stability
void assert_stability() const
assert that the data structure is consistent and stable
Definition liblts_bisim_dnj.h:3342
mcrl2::lts::detail::bisim_partitioner_dnj::part_tr
bisim_dnj::part_trans_t part_tr
partitions of the transitions (with bunches and action_block-slices)
Definition liblts_bisim_dnj.h:2811
mcrl2::lts::detail::bisim_partitioner_dnj::aut
LTS_TYPE & aut
automaton that is being reduced
Definition liblts_bisim_dnj.h:2804
mcrl2::lts::detail::bisim_partitioner_dnj::get_eq_class
state_type get_eq_class(state_type const s) const
Get the equivalence class of a state.
Definition liblts_bisim_dnj.h:2889
mcrl2::lts::detail::bisim_partitioner_dnj::split
bisim_dnj::block_t * split(bisim_dnj::block_t *const block_B, const bisim_dnj::block_bunch_slice_iter_t splitter_T, enum refine_mode_t mode)
Split a block according to a splitter.
Definition liblts_bisim_dnj.h:4022
mcrl2::lts::detail::bisim_partitioner_dnj::finalize_minimized_LTS
void finalize_minimized_LTS()
Adapt the LTS after minimisation.
Definition liblts_bisim_dnj.h:2907
mcrl2::lts::detail::bisim_partitioner_dnj::end_initial_part
std::clock_t end_initial_part
time measurement after the end of create_initial_partition()
Definition liblts_bisim_dnj.h:2840
mcrl2::lts::detail::bisim_partitioner_dnj::bisim_partitioner_dnj
bisim_partitioner_dnj(LTS_TYPE &new_aut, bool const new_branching=false, bool const new_preserve_divergence=false)
constructor
Definition liblts_bisim_dnj.h:2853
mcrl2::lts::detail::bisim_partitioner_dnj::branching
bool const branching
true iff branching (not strong) bisimulation has been requested
Definition liblts_bisim_dnj.h:2826
mcrl2::lts::detail::bisim_partitioner_dnj::refine_mode_t
refine_mode_t
modes that determine details of how split() should work
Definition liblts_bisim_dnj.h:2799
mcrl2::lts::detail::bisim_partitioner_dnj::extend_from_marked_states
@ extend_from_marked_states
Definition liblts_bisim_dnj.h:2799
mcrl2::lts::detail::bisim_partitioner_dnj::extend_from_marked_states__add_new_noninert_to_splitter
@ extend_from_marked_states__add_new_noninert_to_splitter
Definition liblts_bisim_dnj.h:2800
mcrl2::lts::detail::bisim_partitioner_dnj::part_st
bisim_dnj::part_state_t part_st
partition of the state space into blocks
Definition liblts_bisim_dnj.h:2807
mcrl2::lts::detail::bisim_partitioner_dnj::preserve_divergence
bool const preserve_divergence
true iff divergence-preserving branching bisimulation has been requested
Definition liblts_bisim_dnj.h:2833
mcrl2::lts::detail::bisim_partitioner_dnj::action_label
fixed_vector< bisim_dnj::iterator_or_counter< bisim_dnj::action_block_entry * > > action_label
action label slices
Definition liblts_bisim_dnj.h:2823
mcrl2::lts::detail::check_complexity::block_bunch_dnj_counter_t
Definition check_complexity.h:1318
mcrl2::lts::detail::check_complexity::block_dnj_counter_t
Definition check_complexity.h:1177
mcrl2::lts::detail::check_complexity::bunch_dnj_counter_t
Definition check_complexity.h:1280
mcrl2::lts::detail::check_complexity::state_dnj_counter_t
Definition check_complexity.h:1229
mcrl2::lts::detail::check_complexity::trans_dnj_counter_t
Definition check_complexity.h:1387
mcrl2::lts::detail::check_complexity
class for time complexity checks
Definition check_complexity.h:138
mcrl2::lts::detail::check_complexity::ilog2
static int ilog2(state_type size)
calculate the base-2 logarithm, rounded down
Definition check_complexity.h:479
mcrl2::lts::detail::check_complexity::log_n
static unsigned char log_n
value of floor(log2(n)) for easy access
Definition check_complexity.h:474
mcrl2::lts::detail::check_complexity::counter_type
counter_type
Type for complexity budget counters.
Definition check_complexity.h:150
mcrl2::lts::detail::check_complexity::split_off_block
@ split_off_block
Definition check_complexity.h:300
mcrl2::lts::detail::check_complexity::move_out_slice_to_new_block
@ move_out_slice_to_new_block
Definition check_complexity.h:345
mcrl2::lts::detail::fixed_vector
Definition fixed_vector.h:41
mcrl2::lts::detail::fixed_vector::data_end
T * data_end()
Definition fixed_vector.h:60
mcrl2::lts::detail::scc_partitioner
This class contains an scc partitioner removing inert tau loops.
Definition liblts_scc.h:128
mcrl2::lts::detail::scc_partitioner::get_eq_class
std::size_t get_eq_class(const std::size_t s) const
Gives the equivalence class number of a state. The equivalence class numbers range from 0 upto (and e...
Definition liblts_scc.h:339
mcrl2::lts::detail::scc_partitioner::replace_transition_system
void replace_transition_system(const bool preserve_divergence_loops)
The lts for which this partioner is created is replaced by the lts modulo the calculated partition.
Definition liblts_scc.h:248
mcrl2::lts::detail::simple_list::const_iterator
constant iterator class for simple_list
Definition simple_list.h:341
mcrl2::lts::detail::simple_list::iterator
iterator class for simple_list
Definition simple_list.h:390
mcrl2::lts::detail::simple_list
a simple implementation of lists
Definition simple_list.h:296
mcrl2::lts::detail::simple_list::get_pool
static my_pool< entry > & get_pool()
Definition simple_list.h:331
mcrl2::lts::transition
A class containing triples, source label and target representing transitions.
Definition transition.h:48
coroutine.h
helper macros for coroutines
ABORT_THIS_COROUTINE
#define ABORT_THIS_COROUTINE()
indicates that this coroutine gives up control to the other one
Definition coroutine.h:363
END_COROUTINE
#define END_COROUTINE
Ends the definition of code for a coroutine.
Definition coroutine.h:200
ABORT_OTHER_COROUTINE
#define ABORT_OTHER_COROUTINE()
indicates that the other coroutine should give up control
Definition coroutine.h:378
COROUTINE_FOR
#define COROUTINE_FOR(location, init, condition, update)
a for loop where every iteration incurs one unit of work
Definition coroutine.h:271
COROUTINE_WHILE
#define COROUTINE_WHILE(location, condition)
a while loop where every iteration incurs one unit of work
Definition coroutine.h:227
COROUTINES_SECTION
#define COROUTINES_SECTION
begin a section with two coroutines
Definition coroutine.h:142
COROUTINE_DO_WHILE
#define COROUTINE_DO_WHILE(location, condition)
a do { } while loop where every iteration incurs one unit of work
Definition coroutine.h:314
END_COROUTINES_SECTION
#define END_COROUTINES_SECTION
Close a section containing coroutines.
Definition coroutine.h:208
COROUTINE
#define COROUTINE
Define the code for a coroutine.
Definition coroutine.h:192
END_COROUTINE_WHILE
#define END_COROUTINE_WHILE
ends a loop started with COROUTINE_WHILE
Definition coroutine.h:252
END_COROUTINE_FOR
#define END_COROUTINE_FOR
ends a loop started with COROUTINE_FOR
Definition coroutine.h:297
COROUTINE_LABELS
#define COROUTINE_LABELS(locations)
Declare the interrupt locations for the coroutines.
Definition coroutine.h:161
END_COROUTINE_DO_WHILE
#define END_COROUTINE_DO_WHILE
ends a loop started with COROUTINE_DO_WHILE
Definition coroutine.h:336
TERMINATE_COROUTINE_SUCCESSFULLY
#define TERMINATE_COROUTINE_SUCCESSFULLY()
terminate the pair of coroutines successfully
Definition coroutine.h:348
fixed_vector.h
a vector class that cannot be moved while it is not empty
mcrl2::lts::detail::bisimulation_compare_dnj
bool bisimulation_compare_dnj(const LTS_TYPE &l1, const LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false)
Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bis...
Definition liblts_bisim_dnj.h:4973
mcrl2::lts::detail::destructive_bisimulation_compare_dnj
bool destructive_bisimulation_compare_dnj(LTS_TYPE &l1, LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false, bool const generate_counter_examples=false, const std::string &="", bool=false)
Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bis...
Definition liblts_bisim_dnj.h:4926
mcrl2::lts::detail::bisimulation_reduce_dnj
void bisimulation_reduce_dnj(LTS_TYPE &l, bool const branching=false, bool const preserve_divergence=false)
Reduce transition system l with respect to strong or (divergence-preserving) branching bisimulation.
Definition liblts_bisim_dnj.h:4808
mcrl2::lts::detail::bisim_dnj::permutation_t
fixed_vector< permutation_entry > permutation_t
Definition liblts_bisim_dnj.h:194
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_iter_or_null_t
iterator_or_null_t< block_bunch_slice_t > block_bunch_slice_iter_or_null_t
Definition liblts_bisim_dnj.h:207
mcrl2::lts::detail::bisim_dnj::new_block_mode_t
new_block_mode_t
Definition liblts_bisim_dnj.h:209
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_iter_t
simple_list< block_bunch_slice_t >::iterator block_bunch_slice_iter_t
Definition liblts_bisim_dnj.h:203
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_const_iter_t
simple_list< block_bunch_slice_t >::const_iterator block_bunch_slice_const_iter_t
Definition liblts_bisim_dnj.h:205
mcrl2::lts::detail::bisim_dnj::new_block_is_U
@ new_block_is_U
Definition liblts_bisim_dnj.h:209
mcrl2::lts::detail::bisim_dnj::new_block_is_R
@ new_block_is_R
Definition liblts_bisim_dnj.h:209
mcrl2::lts::detail::bisim_dnj::bunch_t::split_off_small_action_block_slice
bunch_t * split_off_small_action_block_slice(part_trans_t &part_tr)
split off a single action_block-slice from the bunch
Definition liblts_bisim_dnj.h:2708
mcrl2::lts::detail::bisim_dnj::succ_entry::out_slice_begin
succ_entry * out_slice_begin(ONLY_IF_DEBUG(const fixed_vector< succ_entry > &succ))
find the beginning of the out-slice
Definition liblts_bisim_dnj.h:1255
mcrl2::lts::detail::bisim_dnj::block_t::split_off_block
block_t * split_off_block(enum new_block_mode_t new_block_mode, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) state_type new_seqnr)
refine a block
Definition liblts_bisim_dnj.h:2603
mcrl2::lts::detail::bisim_dnj::succ_entry::add_work_to_out_slice
static void add_work_to_out_slice(const bisim_partitioner_dnj< LTS_TYPE > &partitioner, const succ_entry *out_slice_begin, enum check_complexity::counter_type ctr, unsigned max_value)
assign work to the transitions in an out-slice (i.e. the transitions from one state in a specific bun...
Definition liblts_bisim_dnj.h:1290
mcrl2::lts::detail::bisim_dnj::succ_entry::bunch
bunch_t * bunch() const
find the bunch of the transition
Definition liblts_bisim_dnj.h:1276
PRINT_SG_PL
#define PRINT_SG_PL(counter, sg_string, pl_string)
ONLY_IF_DEBUG
#define ONLY_IF_DEBUG(...)
include something in Debug mode
Definition liblts_bisim_dnj.h:108
PRINT_INT_PERCENTAGE
#define PRINT_INT_PERCENTAGE(num, denom)
liblts_merge.h
liblts_scc.h
mCRL2log
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
atermpp::pp
std::string pp(const atermpp::aterm &t)
Transform an aterm to an ascii string.
Definition aterm.h:440
mcrl2::data::detail::pp
std::string pp(const detail::lhs_t &lhs)
Definition linear_inequalities.h:507
mcrl2::data::min
data_expression min(const data_expression &e1, const data_expression &e2, const rewriter &)
Definition linear_inequalities.h:953
mcrl2::log::warning
@ warning
Definition logger.h:34
mcrl2::log::verbose
@ verbose
Definition logger.h:37
mcrl2::lps::state
atermpp::term_balanced_tree< data::data_expression > state
Definition state.h:24
mcrl2::lts::detail::bisim_dnj::action_label_greater
static struct mcrl2::lts::detail::bisim_dnj::@1 action_label_greater
mcrl2::lts::detail::bisim_dnj::finalise_U_is_smaller
static void finalise_U_is_smaller(const block_t *const block_U, const block_t *const block_R, const bisim_partitioner_dnj< LTS_TYPE > &partitioner)
moves temporary work counters to normal ones if the U-block is smaller
Definition liblts_bisim_dnj.h:4587
mcrl2::lts::detail::bisim_dnj::finalise_R_is_smaller
static void finalise_R_is_smaller(const block_t *const block_U, const block_t *const block_R, const bisim_partitioner_dnj< LTS_TYPE > &partitioner)
moves temporary work counters to normal ones if the R-block is smaller
Definition liblts_bisim_dnj.h:4691
mcrl2::lts::detail::state_type
std::size_t state_type
type used to store state (numbers and) counts
Definition check_complexity.h:112
mcrl2::lts::detail::iterator_or_null_t
typename simple_list< El >::iterator_or_null iterator_or_null_t
Definition simple_list.h:962
mcrl2::lts::detail::label_type
std::size_t label_type
type used to store label numbers and counts
Definition liblts_bisim_dnj.h:115
mcrl2::lts::detail::trans_type
std::size_t trans_type
type used to store transition (numbers and) counts
Definition check_complexity.h:122
mcrl2::lts::sort_transitions
void sort_transitions(std::vector< transition > &transitions, const std::set< transition::size_type > &hidden_label_set, transition_sort_style ts=src_lbl_tgt)
Sorts the transitions using a sort style.
Definition lts_utilities.h:36
mcrl2::lts::label
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
Definition lts_utilities.h:690
mcrl2::lts::scc_reduce
void scc_reduce(LTS_TYPE &l, const bool preserve_divergence_loops=false)
Definition liblts_scc.h:394
mcrl2
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
std::swap
void swap(atermpp::unprotected_aterm_core &t1, atermpp::unprotected_aterm_core &t2) noexcept
Swaps two aterms.
Definition aterm.h:462
simple_list.h
Simple list implementation (with pool allocator)
USE_POOL_ALLOCATOR
#define USE_POOL_ALLOCATOR
Definition simple_list.h:66
mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t
pointer to next non-trivial bunch (in the single-linked list) or label
Definition liblts_bisim_dnj.h:961
mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t::label
label_type label
action label of the transition
Definition liblts_bisim_dnj.h:970
mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t::next_nontrivial_and_label_t
next_nontrivial_and_label_t()
constructor
Definition liblts_bisim_dnj.h:974
mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t::next_nontrivial
bunch_t * next_nontrivial
pointer to the next non-trivial bunch in the single-linked list
Definition liblts_bisim_dnj.h:967
mcrl2::lts::detail::bisim_dnj::iterator_or_counter
union: either iterator or counter (for initialisation)
Definition liblts_bisim_dnj.h:135
mcrl2::lts::detail::bisim_dnj::iterator_or_counter::iterator_or_counter
iterator_or_counter()
Construct the object as a counter.
Definition liblts_bisim_dnj.h:143
mcrl2::lts::detail::bisim_dnj::iterator_or_counter::count
trans_type count
counter (used during initialisation)
Definition liblts_bisim_dnj.h:137
mcrl2::lts::detail::bisim_dnj::iterator_or_counter::begin
Iterator begin
iterator (used during main part of the algorithm)
Definition liblts_bisim_dnj.h:140
mcrl2::lts::detail::bisim_dnj::iterator_or_counter::~iterator_or_counter
~iterator_or_counter()
Destruct the object as an iterator.
Definition liblts_bisim_dnj.h:154
mcrl2::lts::detail::bisim_dnj::iterator_or_counter::convert_to_iterator
void convert_to_iterator(const Iterator other)
Convert the object from counter to iterator.
Definition liblts_bisim_dnj.h:147
mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t
block where the state belongs
Definition liblts_bisim_dnj.h:244
mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t::ock
block_t * ock
Definition liblts_bisim_dnj.h:246
mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t::ed_noninert_end
pred_entry * ed_noninert_end
Definition liblts_bisim_dnj.h:245