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
89
90#include <cstddef> // for std::size_t
91
92// My provisional recommendation is to always use simple lists and pool
93// allocators. Using standard allocation and standard lists is 5-15% slower
94// and uses perhaps 0.7% more memory. Using standard allocation and simple
95// lists is 10-20% slower and has no significant effect on memory use. These
96// numbers are based on a small set with not-so-large case studies, none of
97// which includes new bottom states.
98
99#define USE_SIMPLE_LIST
100
101#ifndef USE_SIMPLE_LIST
102 #include <list> // for the list of block_bunch-slices
103 #include <type_traits> // for std::is_trivially_destructible<class>
104#endif
105
106#define USE_POOL_ALLOCATOR
107
108#ifdef USE_POOL_ALLOCATOR
109 #ifndef NDEBUG
110 #include <type_traits> // for std::is_trivially_destructible<class>
111 #endif
112
113 #define ONLY_IF_POOL_ALLOCATOR(...) __VA_ARGS__
114 #ifndef USE_SIMPLE_LIST
115 #error "Using the pool allocator also requires using the simple list"
116 #endif
117#else
118 #define ONLY_IF_POOL_ALLOCATOR(...)
119#endif
120
121namespace mcrl2
122{
123namespace lts
124{
125namespace detail
126{
127 #ifndef NDEBUG
133// state_type and trans_type are defined in check_complexity.h. /// mode and to nothing otherwise.
134 #define ONLY_IF_DEBUG(...) __VA_ARGS__
135 #else
136 #define ONLY_IF_DEBUG(...)
137 #endif
139typedef std::size_t label_type;
140
141template <class LTS_TYPE> class bisim_partitioner_dnj;
142
143namespace bisim_dnj
144{
145
157template <class Iterator>
159{
162
164 Iterator begin;
165
168
169
171 void convert_to_iterator(const Iterator other)
172 {
173 new (&begin) Iterator(other);
174 }
175
176
178 ~iterator_or_counter() { begin.~Iterator(); }
179};
180
181
182class block_bunch_entry;
183class action_block_entry;
184
185
186
187
188
189/* ************************************************************************* */
190/* */
191/* M E M O R Y M A N A G E M E N T */
192/* */
193/* ************************************************************************* */
194
195
196
197
198
199#ifdef USE_POOL_ALLOCATOR
215 template <class T, size_t BLOCKSIZE = 1000>
217 { static_assert(std::is_trivially_destructible<T>::value);
218 private: static_assert(sizeof(void*) <= sizeof(T));
220 {
221 public:
222 char data[BLOCKSIZE - sizeof(pool_block_t*)];
224
225 pool_block_t(pool_block_t* const new_next_block)
226 : next_block(new_next_block)
227 { }
228 }; static_assert(sizeof(T) <= sizeof(pool_block_t::data));
229
233
236
239
240 static void*& deref_void(void* addr)
241 {
242 return *static_cast<void**>(addr);
243 }
244 public:
247 : first_block(new pool_block_t(nullptr)),
249 &first_block->data[sizeof(first_block->data)]),
250 first_free_T(nullptr)
251 { }
252
253
256 {
257 pool_block_t* block(first_block); assert(nullptr != block);
258 do
259 {
260 pool_block_t* next_block = block->next_block;
261 delete block;
262 block = next_block;
263 }
264 while(nullptr != block);
265 }
266
267
268 private:
271 template <class U, class... Args>
272 U* construct_samesize(Args&&... args)
273 { static_assert(sizeof(T) == sizeof(U));
274 void* new_el; assert(nullptr != first_block);
275 if (first_block->data + sizeof(U) <= begin_used_in_first_block)
276 {
278 new_el = static_cast<char*>(begin_used_in_first_block) -
279 sizeof(U);
280 }
281 else if (nullptr != first_free_T)
282 {
283 // free list is tested afterwards because I expect that there
284 // won't be too many elements in the free list.
285 new_el = first_free_T;
286 first_free_T = deref_void(new_el);
287 }
288 else
289 {
292 new_el = &first_block->data[sizeof(first_block->data) -
293 sizeof(U)];
294 }
295 return new(new_el) U(std::forward<Args>(args)...);
296 }
297
298
301 template <class U, class... Args>
302 U* construct_othersize(Args&&... args)
303 { static_assert(sizeof(U) != sizeof(T));
304 void* new_el; assert(nullptr != first_block);
305 if (first_block->data + sizeof(U) <= begin_used_in_first_block)
306 {
308 new_el = static_cast<char*>(begin_used_in_first_block) -
309 sizeof(U);
310 }
311 else
312 {
313 if constexpr (sizeof(T) * 2 < sizeof(U))
314 {
315 // There may be space for several T-elements
316 while (first_block->data + sizeof(T) <=
318 {
319 begin_used_in_first_block = static_cast<char*>
320 (begin_used_in_first_block) - sizeof(T);
323 }
324 }
325 else if constexpr (sizeof(T) < sizeof(U))
326 {
327 // There may be space for one T-element (but not more)
328 if (first_block->data + sizeof(T) <=
330 {
331 begin_used_in_first_block = static_cast<char*>
332 (begin_used_in_first_block) - sizeof(T);
335 }
336 } assert(first_block->data + sizeof(T) > begin_used_in_first_block);
339 new_el = &first_block->data[sizeof(first_block->data) -
340 sizeof(U)];
341 }
342 return new(new_el) U(std::forward<Args>(args)...);
343 }
344 public:
346 template <class U, class... Args>
347 U* construct(Args&&... args)
348 { static_assert(std::is_trivially_destructible<U>::value);
349 if constexpr (sizeof(U) == sizeof(T))
350 {
351 return construct_samesize<U>(std::forward<Args>(args)...);
352 }
353 else
354 { static_assert(sizeof(U) <= sizeof(first_block->data));
355 return construct_othersize<U>(std::forward<Args>(args)...);
356 }
357 }
358
359
366 template <class U>
367 void destroy(U* const old_el)
368 { static_assert(sizeof(T) == sizeof(U));
369 old_el->~U(); static_assert(std::is_trivially_destructible<U>::value);
370 #ifndef NDEBUG
371 // ensure that old_el points to an element in some block
372 static std::less<const void*> const total_order;
373 for (const pool_block_t* block(first_block);
374 assert(nullptr != block),
375 total_order(old_el, block->data) ||
376 total_order(&block->data[sizeof(block->data)], old_el + 1);
377 block = block->next_block )
378 { }
379 #endif
380 deref_void(old_el) = first_free_T;
381 first_free_T = static_cast<void*>(old_el);
382 }
383 };
384#endif
385
386#ifdef USE_SIMPLE_LIST
395 template <class T>
397 {
398 private:
401 {
402 protected:
405
408
409 empty_entry(empty_entry*const new_next, empty_entry*const new_prev)
410 : next(new_next),
411 prev(new_prev)
412 { }
413
414 friend class simple_list;
415 };
416
420
421 public:
425 class entry : public empty_entry
426 {
427 private:
429
430 friend class simple_list;
431 public:
432 template <class... Args>
433 entry(empty_entry* const new_next, empty_entry* const new_prev,
434 Args&&... args)
435 : empty_entry(new_next, new_prev),
436 data(std::forward<Args>(args)...)
437 { }
438 };
439
442 {
443 public:
444 typedef std::bidirectional_iterator_tag iterator_category;
445 typedef T value_type;
446 typedef std::ptrdiff_t difference_type;
447 typedef T* pointer;
448 typedef T& reference;
449 protected:
451
452 const_iterator(const empty_entry* const new_ptr)
453 : ptr(const_cast<empty_entry*>(new_ptr))
454 { }
455
456 friend class simple_list;
457 public:
458 const_iterator() = default;
459 const_iterator(const const_iterator& other) = default;
460 const_iterator& operator=(const const_iterator& other) = default;
461 const_iterator& operator++() { ptr = ptr->next; return *this; }
462 const_iterator& operator--() { ptr = ptr->prev; return *this; }
463 const T& operator*() const
464 {
465 return static_cast<const entry*>(ptr)->data;
466 }
467 const T* operator->() const
468 {
469 return &static_cast<const entry*>(ptr)->data;
470 }
471 bool operator==(const const_iterator& other) const
472 {
473 return ptr == other.ptr;
474 }
475 bool operator!=(const const_iterator& other) const
476 {
477 return !operator==(other);
478 }
479 };
480
483 {
484 public:
485 typedef typename const_iterator::iterator_category
491 protected:
492 iterator(empty_entry*const new_ptr) : const_iterator(new_ptr) { }
493
494 friend class simple_list;
495 public:
496 iterator() = default;
497 iterator(const iterator& other) = default;
498 iterator& operator=(const iterator& other) = default;
501 T& operator*() const
502 {
503 return static_cast<entry*>(const_iterator::ptr)->data;
504 }
505 T* operator->() const
506 {
507 return &static_cast<entry*>(const_iterator::ptr)->data;
508 }
509 };
510
516 {
517 public:
521 typedef typename iterator::pointer pointer;
524 iterator_or_null(std::nullptr_t) : iterator()
525 {
526 const_iterator::ptr = nullptr;
527 }
528 iterator_or_null(const iterator& other) : iterator(other) { }
529 bool is_null() const { return nullptr == const_iterator::ptr; }
530 T& operator*() const
531 { assert(!is_null());
532 return iterator::operator*();
533 }
534 T* operator->() const
535 { assert(!is_null());
536 return iterator::operator->();
537 }
538 bool operator==(const const_iterator& other) const
539 {
540 return const_iterator::ptr == other.ptr;
541 }
542 bool operator!=(const const_iterator& other) const
543 {
544 return !operator==(other);
545 }
546 bool operator==(const T* const other) const
547 { assert(nullptr != other);
548 // It is allowed to call this even if is_null(). Therefore, we
549 // cannot use iterator_or_null::operator->().
550 return const_iterator::operator->() == other;
551 }
552 bool operator!=(const T* const other) const
553 {
554 return !operator==(other);
555 }
556
557 void operator=(std::nullptr_t)
558 {
559 const_iterator::ptr = nullptr;
560 }
561 };
562
566 { static_assert(std::is_trivially_destructible<entry>::value);
567 }
568
569 #ifndef USE_POOL_ALLOCATOR
572 {
573 for (iterator iter = begin(); end() != iter; )
574 {
575 iterator next = std::next(iter);
576 delete static_cast<entry*>(iter.ptr);
577 iter = next;
578 }
579 }
580 #endif
581
584
587
590
593
595 const_iterator begin() const { return cbegin(); }
596
598 const_iterator end() const { return cend(); }
599
601 T& front()
602 { assert(!empty());
603 return static_cast<entry*>(sentinel.next)->data;
604 }
605
607 T& back()
608 { assert(!empty());
609 return static_cast<entry*>(sentinel.prev)->data;
610 }
611
613 bool empty() const { return sentinel.next == &sentinel; }
614
616 template<class... Args>
619 iterator pos, Args&&... args)
620 {
621 entry* const new_entry(
622 #ifdef USE_POOL_ALLOCATOR
623 pool.template construct<entry>
624 #else
625 new entry
626 #endif
627 (pos.ptr, pos.ptr->prev, std::forward<Args>(args)...));
628 pos.ptr->prev->next = new_entry;
629 pos.ptr->prev = new_entry;
630 return iterator(new_entry);
631 }
632
634 template<class... Args>
637 iterator pos, Args&&... args)
638 {
639 entry* const new_entry(
640 #ifdef USE_POOL_ALLOCATOR
641 pool.template construct<entry>
642 #else
643 new entry
644 #endif
645 (pos.ptr->next, pos.ptr, std::forward<Args>(args)...));
646 pos.ptr->next->prev = new_entry;
647 pos.ptr->next = new_entry;
648 return iterator(new_entry);
649 }
650
652 template<class... Args>
655 Args&&... args)
656 {
657 entry* const new_entry(
658 #ifdef USE_POOL_ALLOCATOR
659 pool.template construct<entry>
660 #else
661 new entry
662 #endif
663 (sentinel.next, &sentinel, std::forward<Args>(args)...));
664 sentinel.next->prev = new_entry;
665 sentinel.next = new_entry;
666 return iterator(new_entry);
667 }
668
670 template<class... Args>
673 Args&&... args)
674 {
675 entry* const new_entry(
676 #ifdef USE_POOL_ALLOCATOR
677 pool.template construct<entry>
678 #else
679 new entry
680 #endif
681 (&sentinel, sentinel.prev, std::forward<Args>(args)...));
682 sentinel.prev->next = new_entry;
683 sentinel.prev = new_entry;
684 return iterator(new_entry);
685 }
686
689 static void splice(iterator const new_pos, simple_list& /* unused */,
690 iterator const old_pos)
691 {
692 old_pos.ptr->prev->next = old_pos.ptr->next;
693 old_pos.ptr->next->prev = old_pos.ptr->prev;
694
695 old_pos.ptr->next = new_pos.ptr->prev->next;
696 old_pos.ptr->prev = new_pos.ptr->prev;
697
698 old_pos.ptr->prev->next = old_pos.ptr;
699 old_pos.ptr->next->prev = old_pos.ptr;
700 }
701
703 static void erase(
705 iterator const pos)
706 {
707 pos.ptr->prev->next = pos.ptr->next;
708 pos.ptr->next->prev = pos.ptr->prev;
709 #ifdef USE_POOL_ALLOCATOR
710 pool.destroy(static_cast<entry*>(pos.ptr));
711 #else
712 delete static_cast<entry*>(pos.ptr);
713 #endif
714 }
715 };
716#else
717 #define simple_list std::list
718#endif
719
720
721
722
723
724/* ************************************************************************* */
725/* */
726/* R E F I N A B L E P A R T I T I O N */
727/* */
728/* ************************************************************************* */
729
730
731
732
733
742class state_info_entry;
743class permutation_entry;
744
754
755class block_t;
756class bunch_t;
757
758class pred_entry;
759class succ_entry;
760
765#ifdef USE_SIMPLE_LIST
768#else
770 {
771 private:
772 const void* null;
774 public:
777 {
778 if constexpr (!std::is_trivially_destructible<
780 {
781 // We still have to internally decide whether to construct
782 // the iterator or not so the destructor knows what to do.
783 null = nullptr;
784 }
785 }
786
787
789 explicit block_bunch_slice_iter_or_null_t(nullptr_t)
790 {
791 null = nullptr;
792 }
793
794
797 const block_bunch_slice_iter_t& other)
798 {
799 new (&iter) block_bunch_slice_iter_t(other); assert(nullptr != null);
800 }
801
802
804 // not)
806 {
807 if (!is_null()) iter.~block_bunch_slice_iter_t();
808 }
809
810 block_bunch_slice_t* operator->()
811 { assert(nullptr != null);
812 return iter.operator->();
813 }
814 block_bunch_slice_t& operator*()
815 { assert(nullptr != null);
816 return iter.operator*();
817 }
818
819 void operator=(nullptr_t)
820 {
821 if (!is_null()) iter.~block_bunch_slice_iter_t();
822 null = nullptr;
823 }
824
825
826 explicit operator block_bunch_slice_iter_t() const
827 { assert(nullptr != null);
828 return iter;
829 }
830
831
832 explicit operator block_bunch_slice_const_iter_t() const
833 { assert(nullptr != null);
834 return iter;
835 }
836
837
838 void operator=(const block_bunch_slice_iter_t& other)
839 {
840 if (!is_null()) iter.~block_bunch_slice_iter_t();
841 new (&iter) block_bunch_slice_iter_t(other); assert(nullptr != null);
842 }
843
847 bool operator==(const block_bunch_slice_iter_or_null_t& other) const
848 {
849 if constexpr (sizeof(null) == sizeof(iter))
850 {
851 return &*iter == &*other.iter;
852 }
853 else
854 {
855 return (is_null() && other.is_null()) ||
856 (!is_null() && !other.is_null() && &*iter == &*other.iter);
857 }
858 }
859
860
862 bool operator!=(const block_bunch_slice_iter_or_null_t& other) const
863 {
864 return !operator==(other);
865 }
866
867
871 bool operator==(const block_bunch_slice_const_iter_t other) const
872 { // assert(nullptr != &*other); -- generates a warning
873 return (sizeof(null) == sizeof(iter) || !is_null()) &&
874 &*iter == &*other;
875 }
876
877
878 bool operator!=(const block_bunch_slice_const_iter_t other) const
879 {
880 return !operator==(other);
881 }
882
883
887 bool operator==(const block_bunch_slice_t* const other) const
888 { assert(nullptr != other);
889 return (sizeof(null) == sizeof(iter) || !is_null()) &&
890 &*iter == other;
891 }
892
893
894 bool operator!=(const block_bunch_slice_t* const other) const
895 {
896 return !operator==(other);
897 }
898
899
901 bool is_null() const { return nullptr == null; }
902 };
903#endif
904
906
907
914{
915 public:
924
933
940 union bl_t {
943 } bl;
944
947
963 #ifndef NDEBUG
965 template<class LTS_TYPE>
967 partitioner) const
968 { assert(&partitioner.part_st.state_info.front() <= this);
969 assert(this <= &partitioner.part_st.state_info.back());
970 return std::to_string(this - &partitioner.part_st.state_info.front());
971 }
972
974 template<class LTS_TYPE>
976 partitioner) const
977 {
978 return "state " + debug_id_short(partitioner);
979 }
980
982 #endif
983};
984
985
988 public:
991
992
994 permutation_entry() = default;
995
996
1000 permutation_entry(const permutation_entry&& other) noexcept
1001 {
1002 st = other.st;
1003 }
1004
1005
1011 void operator=(const permutation_entry&& other) noexcept
1012 {
1013 st = other.st;
1014 st->pos = this;
1015 }
1016};
1017
1018
1043{
1044 public:
1047
1050
1053
1056
1059
1063
1068
1069
1076 block_t(permutation_entry* const new_begin,
1077 permutation_entry* const new_end, state_type const new_seqnr)
1078 : begin(new_begin),
1079 marked_bottom_begin(new_end),
1080 nonbottom_begin(new_end),
1081 marked_nonbottom_begin(new_end),
1082 end(new_end),
1084 seqnr(new_seqnr)
1085 { assert(new_begin < new_end);
1086 }
1087
1088
1091 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1094 return end - begin;
1095 }
1096
1097
1100 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1103 return nonbottom_begin - begin;
1104 }
1105
1106
1109 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1113 }
1114
1115
1118 {
1120 }
1121
1122
1125 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1128 return marked_bottom_begin - begin;
1129 }
1130
1131
1134 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1138 }
1139
1140
1147 { assert(nonbottom_begin <= s); assert(s < end);
1148 // assert(this == s->st->bl.ock); -- does not hold during initialisation
1149 assert(begin <= marked_bottom_begin);
1152 if (marked_nonbottom_begin <= s) { return false; } assert(marked_nonbottom_begin <= end);
1154 return true;
1155 }
1156
1157
1164 { assert(begin <= s);
1165 if (s < nonbottom_begin) // assert(this == s->st->bl.ock); -- does not hold during initialisation
1166 { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1168 if (marked_bottom_begin <= s) { return false; } assert(marked_bottom_begin <= nonbottom_begin);
1170 return true;
1171 }
1172 return mark_nonbottom(s);
1173 }
1174
1175
1187 ONLY_IF_DEBUG( template<class LTS_TYPE> )
1188 block_t* split_off_block(enum new_block_mode_t new_block_mode, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
1191 state_type new_seqnr);
1192 #ifndef NDEBUG
1194 template<class LTS_TYPE>
1196 partitioner) const
1197 { assert(&partitioner.part_st.permutation.front() <= begin);
1198 assert(begin < end); assert(begin <= marked_bottom_begin);
1201 assert(marked_nonbottom_begin <= end);
1202 assert(end <= 1 + &partitioner.part_st.permutation.back());
1203 return "block [" +
1204 std::to_string(begin - &partitioner.part_st.permutation.front()) +
1205 "," + std::to_string(end-&partitioner.part_st.permutation.front()) +
1206 ") (#" + std::to_string(seqnr) + ")";
1207 }
1208
1210 #endif
1211};
1212
1213
1219{
1220 public:
1226
1229
1234
1241 part_state_t(state_type const num_states)
1242 : permutation(num_states),
1243 state_info(num_states),
1244 nr_of_blocks(0)
1245 { assert(0 < num_states);
1247 static_assert(std::is_trivially_destructible<block_t>::value); )
1248 state_info_entry* state_iter(&state_info.front()); assert(perm_iter <= &permutation.back());
1249 do
1250 {
1251 state_iter->pos = perm_iter;
1252 perm_iter->st = state_iter;
1253 }
1254 while (++state_iter, ++perm_iter <= &permutation.back()); assert(state_iter == 1 + &state_info.back());
1255 }
1256
1257
1258 #ifndef USE_POOL_ALLOCATOR
1265 { ONLY_IF_DEBUG( state_type deleted_blocks(0); )
1266 permutation_entry* perm_iter(1 + &permutation.back()); assert(&permutation.front() < perm_iter);
1267 do
1268 {
1269 block_t* const B(perm_iter[-1].st->bl.ock); assert(B->end == perm_iter);
1270 perm_iter = B->begin; ONLY_IF_DEBUG( ++deleted_blocks; )
1271 delete B;
1272 }
1273 while (&permutation.front() < perm_iter); assert(deleted_blocks == nr_of_blocks);
1274 }
1275 #endif
1276
1277
1280 state_type state_size() const { return permutation.size(); }
1281
1282
1286 const block_t* block(state_type const s) const
1287 {
1288 return state_info[s].bl.ock;
1289 }
1290 #ifndef NDEBUG
1291 private:
1299 template<class LTS_TYPE>
1300 void print_block(const block_t* const B,
1301 const char* const message,
1302 const permutation_entry* begin_print,
1303 const permutation_entry* const end_print,
1304 const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
1305 { assert(B->begin <= begin_print); assert(end_print <= B->end);
1306 if (end_print == begin_print) return;
1307
1308 mCRL2log(log::debug) << '\t' << message
1309 << (1 < end_print - begin_print ? "s:\n" : ":\n");
1310 assert(begin_print < end_print);
1311 do
1312 {
1313 mCRL2log(log::debug) << "\t\t"
1314 << begin_print->st->debug_id(partitioner);
1315 if (B != begin_print->st->bl.ock)
1316 {
1317 mCRL2log(log::debug) << ", inconsistent: points "
1318 "to " << begin_print->st->bl.ock->debug_id(partitioner);
1319 }
1320 if (begin_print != begin_print->st->pos)
1321 {
1323 << ", inconsistent pointer to state_info_entry";
1324 }
1325 mCRL2log(log::debug) << '\n';
1326 }
1327 while (++begin_print < end_print);
1328 }
1329 public:
1334 template<class LTS_TYPE>
1335 void print_part(const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
1336 {
1337 if (!mCRL2logEnabled(log::debug)) return;
1338 const block_t* B(permutation.front().st->bl.ock);
1339 do
1340 {
1341 mCRL2log(log::debug)<<B->debug_id(partitioner)<<":\n";
1342 print_block(B, "Bottom state",
1343 B->begin, B->marked_bottom_begin, partitioner);
1344 print_block(B, "Marked bottom state",
1345 B->marked_bottom_begin, B->nonbottom_begin, partitioner);
1346 print_block(B, "Non-bottom state",
1347 B->nonbottom_begin, B->marked_nonbottom_begin, partitioner);
1348 print_block(B, "Marked non-bottom state",
1349 B->marked_nonbottom_begin, B->end, partitioner);
1350 // go to next block
1351 }
1352 while(B->end <= &permutation.back() && (B = B->end->st->bl.ock, true));
1353 }
1354
1358 template<class LTS_TYPE>
1360 const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
1361 {
1362 const permutation_entry* perm_iter(&permutation.front());
1363 state_type true_nr_of_blocks(0);
1364 assert(perm_iter <= &permutation.back());
1365 do
1366 {
1367 const block_t* const block(perm_iter->st->bl.ock);
1368 // block is consistent:
1369 assert(block->begin == perm_iter);
1374 assert(partitioner.branching||block->nonbottom_begin==block->end);
1375 assert(0 <= block->seqnr);
1376 assert(block->seqnr < nr_of_blocks);
1377 unsigned const max_block(bisim_gjkw::check_complexity::log_n -
1379 mCRL2complexity(block, no_temporary_work(max_block), partitioner);
1380
1381 // states in the block are consistent:
1382 do
1383 {
1384 const state_info_entry* const state(perm_iter->st);
1385 // assert(&part_tr.pred.front() < state->pred_inert.begin);
1386 assert(&state_info.back() == state ||
1387 state->pred_inert.begin <= state[1].pred_inert.begin);
1388 // assert(state->pred_inert.begin <= &part_tr.pred.back());
1389 // assert(state->succ_inert.begin <= &part_tr.succ.back());
1390 if (perm_iter < block->nonbottom_begin)
1391 {
1392 assert(&state_info.back() == state || state->
1393 succ_inert.begin <= state[1].succ_inert.begin);
1394 // assert(state->succ_inert.begin==&part_tr.succ.back() ||
1395 // state <
1396 // state->succ_inert.begin->block_bunch->pred->source);
1397 mCRL2complexity(state, no_temporary_work(max_block, true),
1398 partitioner);
1399 }
1400 else
1401 {
1402 // assert(state->succ_inert.begin < &part_tr.succ.back());
1403 assert(&state_info.back() == state || state->
1404 succ_inert.begin < state[1].succ_inert.begin);
1405 //assert(state ==
1406 // state->succ_inert.begin->block_bunch->pred->source);
1407 mCRL2complexity(state, no_temporary_work(max_block, false),
1408 partitioner);
1409 }
1410 assert(block == state->bl.ock);
1411 assert(perm_iter == state->pos);
1412 }
1413 while (++perm_iter < block->end);
1414 assert(perm_iter == block->end);
1415 ++true_nr_of_blocks;
1416 }
1417 while (perm_iter <= &permutation.back());
1418 assert(nr_of_blocks == true_nr_of_blocks);
1419 }
1420 #endif
1421};
1422
1424
1425
1426
1427
1428 #ifndef NDEBUG
1429/* ************************************************************************* */ static struct {
1430/* */ bool operator()(const iterator_or_counter<action_block_entry*> p1,
1431/* T R A N S I T I O N S */ const action_block_entry* const action_block) const
1432/* */ {
1433/* ************************************************************************* */ return p1.begin > action_block;
1434 }
1436 #endif
1437
1438
1472
1474
1477{
1478 public:
1481
1491
1492
1495 );
1496
1497
1499 bunch_t* bunch() const;
1500 #ifndef NDEBUG
1512 template <class LTS_TYPE>
1513 static inline void add_work_to_out_slice(
1514 const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
1516 counter_type ctr, unsigned max_value);
1517 #endif
1518};
1519
1520
1524{
1525 public:
1528
1532};
1533
1534
1541{
1542 public:
1545
1548
1551 #ifndef NDEBUG
1553 template <class LTS_TYPE>
1555 partitioner) const
1556 {
1557 return "from " + source->debug_id_short(partitioner) +
1558 " to " + target->debug_id_short(partitioner);
1559 }
1560
1562 template <class LTS_TYPE>
1563 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1564 const
1565 {
1566 // Search for the action label in partitioner.action_label
1567 label_type const label(std::lower_bound(
1568 partitioner.action_label.cbegin(), partitioner.action_label.cend(),
1570 partitioner.action_label.cbegin());
1571 assert(label < partitioner.action_label.size());
1572 assert(partitioner.action_label[label].begin <= action_block);
1573 assert(0==label||action_block<partitioner.action_label[label-1].begin);
1574 // class lts_lts_t uses a function pp() to transform the action label
1575 // to a string.
1576 return pp(partitioner.aut.action_label(label)) + "-transition " +
1577 debug_id_short(partitioner);
1578 }
1579
1581 #endif
1582};
1583
1584
1588{
1589 public:
1596
1607
1608
1611 const action_block_entry* const action_block_orig_inert_begin )
1612 )
1613 {
1614 action_block_entry* result(begin_or_before_end); assert(nullptr != result);
1615 if (this < result)
1616 { assert(this == result->begin_or_before_end);
1617 result = this; // The following assertion does not always hold: the function is called
1618 } // immediately after a block is refined, so it may be the case that the
1619 // transitions are still to be moved to different slices.
1620 // assert(succ->block_bunch->pred->target->bl.ock ==
1621 // result->succ->block_bunch->pred->target->bl.ock);
1622 assert(nullptr != succ); assert(nullptr != result->succ);
1623 assert(succ->bunch() == result->succ->bunch());
1624 assert(result == action_block_begin || nullptr == result[-1].succ ||
1625 action_block_orig_inert_begin <= result ||
1626 result[-1].succ->block_bunch->pred->target->bl.ock !=
1627 result->succ->block_bunch->pred->target->bl.ock);
1628 // assert(this has the same action as result);
1629 return result;
1630 }
1631};
1632
1633
1634class part_trans_t;
1635
1641{
1642 public:
1645
1648
1654 {
1661
1664
1665
1668 {
1669 next_nontrivial = nullptr;
1670 }
1672
1673
1675 bunch_t(action_block_entry* const new_begin,
1676 action_block_entry* const new_end)
1677 : begin(new_begin),
1678 end(new_end),
1680 { }
1681
1682
1687 bool is_trivial() const
1688 {
1690 }
1691
1692
1700 #ifndef NDEBUG
1702 template <class LTS_TYPE>
1704 partitioner) const
1705 {
1706 assert(partitioner.part_tr.action_block_begin <= begin);
1707 assert(end <= partitioner.part_tr.action_block_inert_begin);
1708 return "bunch [" + std::to_string(begin -
1709 partitioner.part_tr.action_block_begin) + "," +
1710 std::to_string(end - partitioner.part_tr.action_block_begin) + ")";
1711 }
1712
1714 template <class LTS_TYPE>
1715 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1716 const
1717 { assert(nullptr != end[-1].succ);
1718 const action_block_entry* iter(begin); assert(iter < end);
1719 assert(nullptr != iter->succ);
1720 assert(iter == iter->succ->block_bunch->pred->action_block);
1721 std::string result(debug_id_short(partitioner));
1722 result += " containing transition";
1723 result += iter < end - 1 ? "s " : " ";
1724 result += iter->succ->block_bunch->pred->debug_id_short(partitioner);
1725 ++iter;
1726 if (end <= iter) return result;
1727 while (nullptr == iter->succ) ++iter;
1728 assert(iter < end);
1729 assert(iter == iter->succ->block_bunch->pred->action_block);
1730 result += ", ";
1731 result += iter->succ->block_bunch->pred->debug_id_short(partitioner);
1732 if (iter < end - 3)
1733 {
1734 result += ", ...";
1735 iter = end - 3;
1736 }
1737 while (++iter < end)
1738 {
1739 if (nullptr != iter->succ)
1740 { assert(iter == iter->succ->block_bunch->pred->action_block);
1741 result += ", ";
1742 result += iter->succ->block_bunch->pred->debug_id_short(
1743 partitioner);
1744 }
1745 }
1746 return result;
1747 }
1748
1754 template <class LTS_TYPE>
1756 const
1757 {
1758 // verify that the bunch only has a single action label.
1759 // Search for the action label in partitioner.action_label
1760 label_type const label(std::lower_bound(
1761 partitioner.action_label.cbegin(), partitioner.action_label.cend(),
1763 partitioner.action_label.cbegin());
1764 assert(label < partitioner.action_label.size());
1765 assert(partitioner.action_label[label].begin <= begin);
1766 assert(0 == label || begin < partitioner.action_label[label-1].begin);
1767 if (0 == label || end < partitioner.action_label[label - 1].begin)
1768 {
1773 }
1774 return 0;
1775 }
1776
1778 #endif
1779};
1780
1781
1799{
1800 public:
1805
1808
1813
1814
1816 bool is_stable() const { return nullptr == marked_begin; }
1817
1818
1821 { assert(!is_stable()); assert(!empty());
1822 marked_begin = nullptr;
1823 }
1824
1825
1828 { assert(is_stable());
1829 marked_begin = end; assert(!is_stable());
1830 }
1831
1832
1835 bunch_t* const new_bunch, bool const new_is_stable)
1836 : end(new_end),
1837 bunch(new_bunch),
1838 marked_begin(nullptr)
1839 {
1840 if (!new_is_stable) make_unstable();
1841 }
1842
1843
1847 bool empty() const
1848 { // assert(std::less(&part_tr.block_bunch.front(), end));
1849 // assert(!std::less(part_tr.block_bunch_inert_begin, end));
1850 // assert(part_tr.block_bunch.front().slice != this);
1851 return end[-1].slice != this;
1852 }
1853
1854
1857 { assert(!empty());
1858 return end[-1].pred->source->bl.ock;
1859 }
1860 #ifndef NDEBUG
1862 template <class LTS_TYPE>
1863 std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1864 const
1865 {
1866 static struct {
1867 bool operator()(const block_bunch_entry& p1,
1868 const block_bunch_slice_t* const p2) const
1869 {
1870 return p1.slice != p2;
1871 }
1872 } const block_bunch_not_equal;
1873
1874 assert(&partitioner.part_tr.block_bunch.front() < end);
1875 assert(end <= partitioner.part_tr.block_bunch_inert_begin);
1876 std::string const index_string(std::to_string(end -
1877 &partitioner.part_tr.block_bunch.cbegin()[1]));
1878 if (empty())
1879 { //assert(!is_stable());
1880 return "empty block_bunch_slice [" + index_string + "," +
1881 index_string + ")";
1882 }
1883 const block_bunch_entry* begin(
1884 &partitioner.part_tr.block_bunch.cbegin()[1]);
1885 if (trans_type bunch_size(bunch->end - bunch->begin);
1886 (trans_type) (end - begin) > bunch_size)
1887 {
1888 begin = end - bunch_size;
1889 }
1890 begin = std::lower_bound(begin, const_cast<const block_bunch_entry*>
1892 this, block_bunch_not_equal);
1893 assert(begin->slice == this);
1894 assert(begin[-1].slice != this);
1895 return (is_stable() ? "stable block_bunch-slice ["
1896 : "unstable block_bunch_slice [") +
1897 std::to_string(begin-&partitioner.part_tr.block_bunch.cbegin()[1]) +
1898 "," + index_string + ") containing transitions from " +
1899 source_block()->debug_id(partitioner) +
1900 " in " + bunch->debug_id_short(partitioner);
1901 }
1902
1910 template <class LTS_TYPE>
1912 counter_type const ctr, unsigned const max_value,
1913 const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
1914 { assert(!empty());
1915 assert(1U == max_value);
1916 const block_t* const block(source_block());
1917 bool result(false);
1918 const block_bunch_entry* block_bunch(end);
1919 assert(partitioner.part_tr.block_bunch.front().slice != this);
1920 assert(block_bunch[-1].slice == this);
1921 do
1922 {
1923 --block_bunch;
1924 const state_info_entry* const source(block_bunch->pred->source);
1925 assert(source->bl.ock == block);
1926 if (source->pos < block->nonbottom_begin /*&&
1927 // the transition starts in a (new) bottom state
1928 block_bunch->pred->work_counter.counters[ctr -
1929 bisim_gjkw::check_complexity::TRANS_dnj_MIN] != max_value*/)
1930 {
1931 mCRL2complexity(block_bunch->pred, add_work(ctr, max_value),
1932 partitioner);
1933 result = true;
1934 }
1935 }
1936 while (block_bunch[-1].slice == this);
1937 return result;
1938 }
1939
1942 #endif
1943};
1944
1945
1948 )
1949{ assert(nullptr != begin_or_before_end);
1950 succ_entry* result(begin_or_before_end); assert(result->block_bunch->pred->action_block->succ == result);
1951 if (this < result)
1952 { assert(nullptr != result->begin_or_before_end);
1953 assert(this == result->begin_or_before_end);
1954 result = this; assert(result->block_bunch->pred->action_block->succ == result);
1955 } assert(block_bunch->pred->source == result->block_bunch->pred->source);
1956 // assert(this <= result); //< holds always, based on the if() above
1957 assert(nullptr != result->begin_or_before_end);
1958 assert(this <= result->begin_or_before_end);
1959 assert(block_bunch->slice == result->block_bunch->slice);
1960 assert(&succ.cbegin()[1] == result ||
1961 result[-1].block_bunch->pred->source < block_bunch->pred->source ||
1962 result[-1].bunch() != block_bunch->slice->bunch);
1963 return result;
1964}
1965
1966
1969{
1970 return block_bunch->slice->bunch;
1971}
1972 #ifndef NDEBUG
1981 template <class LTS_TYPE>
1982 /* static */ inline void succ_entry::add_work_to_out_slice(
1983 const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
1984 const succ_entry* out_slice_begin, enum bisim_gjkw::check_complexity::
1985 counter_type const ctr, unsigned const max_value)
1986 {
1987 const succ_entry* const out_slice_before_end(
1989 assert(nullptr != out_slice_before_end);
1990 assert(out_slice_begin <= out_slice_before_end);
1992 add_work(ctr, max_value), partitioner);
1993 while (++out_slice_begin <= out_slice_before_end)
1994 {
1995 // treat temporary counters specially
1997 add_work_notemporary(ctr, max_value), partitioner);
1998 }
1999 }
2000 #endif
2002{
2003 public:
2009
2015
2021
2035
2038
2041 #ifndef NDEBUG
2044 #endif
2047 private:
2050
2051 public:
2052 #ifdef USE_POOL_ALLOCATOR
2053 static_assert(std::is_trivially_destructible<bunch_t>::value);
2054 static_assert(std::is_trivially_destructible<
2058 #endif
2059
2062
2068
2077 part_trans_t(trans_type num_transitions,
2078 trans_type num_actions)
2079 : succ(num_transitions + 2),
2080 block_bunch(num_transitions + 1),
2081 pred(num_transitions + 2),
2083 new action_block_entry[num_transitions + num_actions - 1]),
2084 action_block_end(action_block_begin + (num_transitions+num_actions-1)),
2087 splitter_list(),
2088 first_nontrivial(nullptr),
2090 nr_of_bunches(0),
2094 {
2095 succ.front().block_bunch = &block_bunch.front();
2096 succ.back() .block_bunch = &block_bunch.front();
2097 block_bunch.front().pred = &pred.front();
2098 block_bunch.front().slice = nullptr;
2099 pred.front().source = nullptr;
2100 pred.front().target = nullptr;
2101 pred.back() .source = nullptr;
2102 pred.back() .target = nullptr;
2103 }
2104
2105
2108 {
2109 #ifndef USE_POOL_ALLOCATOR
2110 // The destructor also deallocates the bunches, as they are not
2111 // directly referenced from anywhere. This is only necessary if we
2112 // do not use the pool allocator, as the latter will destroy the
2113 // bunches wholesale.
2114 action_block_entry* action_block_iter(action_block_begin);
2115 for (;;)
2116 {
2117 do
2118 {
2119 if (action_block_inert_begin <= action_block_iter)
2120 { assert(0 == nr_of_bunches);
2121 delete [] action_block_begin;
2122 return;
2123 }
2124 }
2125 while (nullptr == action_block_iter->succ && ( assert(nullptr == action_block_iter->begin_or_before_end),
2126 ++action_block_iter, true)); assert(nullptr != action_block_iter->begin_or_before_end);
2127 bunch_t* const bunch(action_block_iter->succ->bunch()); assert(bunch->begin == action_block_iter);
2128 action_block_iter = bunch->end;
2129 delete bunch; ONLY_IF_DEBUG( --nr_of_bunches; )
2130 }
2131 /* unreachable */ assert(0);
2132 #else
2133 delete [] action_block_begin;
2134 #endif
2135 }
2136
2137
2141 {
2142 return first_nontrivial;
2143 }
2144
2145
2148 void make_nontrivial(bunch_t* const bunch)
2149 { assert(1 < bunch->end - bunch->begin); assert(bunch->is_trivial());
2150 // The following assertions do not necessarily hold during initialisation:
2151 //assert(bunch->begin <= bunch->begin->begin_or_before_end);
2153 nullptr == first_nontrivial ? bunch : first_nontrivial; //assert(nullptr != bunch->begin->begin_or_before_end);
2154 //assert(nullptr != bunch->end[-1].begin_or_before_end);
2155 //assert(bunch->begin->begin_or_before_end <
2156 // bunch->end[-1].begin_or_before_end);
2157 //assert(nullptr != end[-1].begin_or_before_end);
2159 ++nr_of_nontrivial_bunches; //assert(end[-1].begin_or_before_end <= end);
2160 }
2161
2162
2165 void make_trivial(bunch_t* const bunch)
2166 { assert(!bunch->is_trivial()); assert(first_nontrivial == bunch);
2169 ? nullptr : bunch->next_nontrivial_and_label.next_nontrivial; assert(bunch->end - 1 == bunch->begin->begin_or_before_end);
2171 --nr_of_nontrivial_bunches; assert(bunch->begin == bunch->end[-1].begin_or_before_end);
2172 }
2173
2174
2198 action_block_entry* const action_block_iter,
2199 bunch_t* const bunch_T_a_Bprime,
2200 bool const first_transition_of_state)
2201 {
2202
2203 /* - - - - - - - - adapt part_tr.succ - - - - - - - - */
2204
2205 succ_entry* const old_succ_pos(action_block_iter->succ); assert(nullptr != old_succ_pos);
2206 assert(old_succ_pos->block_bunch->pred->action_block == action_block_iter);
2207 succ_entry* const out_slice_begin(old_succ_pos->out_slice_begin( ONLY_IF_DEBUG( succ )
2208 )); assert(out_slice_begin->block_bunch->pred->action_block->succ ==
2209 out_slice_begin);
2210 succ_entry* const new_succ_pos(out_slice_begin->begin_or_before_end); assert(nullptr != new_succ_pos);
2211 assert(out_slice_begin == new_succ_pos->begin_or_before_end);
2212 assert(new_succ_pos<old_succ_pos->block_bunch->pred->source->succ_inert.begin);
2213 /* move the transition to the end of its out-slice */ assert(new_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
2214 if (old_succ_pos < new_succ_pos)
2215 {
2216 std::swap(old_succ_pos->block_bunch, new_succ_pos->block_bunch);
2217 old_succ_pos->block_bunch->pred->action_block->succ = old_succ_pos; assert(action_block_iter == new_succ_pos->block_bunch->pred->action_block);
2218 action_block_iter->succ = new_succ_pos;
2219 } else assert(old_succ_pos == new_succ_pos);
2220
2221 // adapt the old out-slice immediately
2222 // If the old out-slice becomes empty, then out_slice_begin ==
2223 // new_succ_pos, so the two following assignments will assign the
2224 // same variable. The second assignment is the relevant one.
2225 out_slice_begin->begin_or_before_end = new_succ_pos - 1;
2226
2227 // adapt the new out-slice, as far as is possible now:
2228 // make the begin_or_before_end pointers of the first and last
2229 // transition in the slice correct immediately. The other
2230 // begin_or_before_end pointers need to be corrected after all
2231 // transitions in the new bunch have been positioned correctly.
2232 if (first_transition_of_state)
2233 {
2234 new_succ_pos->begin_or_before_end = new_succ_pos;
2235 }
2236 else
2237 {
2238 succ_entry* const out_slice_before_end(
2239 new_succ_pos[1].begin_or_before_end); assert(nullptr != out_slice_before_end);
2240 assert(new_succ_pos < out_slice_before_end);
2241 assert(out_slice_before_end->block_bunch->pred->action_block->succ ==
2242 out_slice_before_end);
2243 assert(new_succ_pos + 1 == out_slice_before_end->begin_or_before_end);
2244 out_slice_before_end->begin_or_before_end = new_succ_pos; assert(out_slice_before_end <
2245 new_succ_pos->block_bunch->pred->source->succ_inert.begin);
2246 new_succ_pos->begin_or_before_end = out_slice_before_end; assert(bunch_T_a_Bprime == out_slice_before_end->bunch());
2247 }
2248
2249 /* - - - - - - - adapt part_tr.block_bunch - - - - - - - */ assert(new_succ_pos == action_block_iter->succ);
2250
2251 block_bunch_entry* const old_block_bunch_pos(
2252 new_succ_pos->block_bunch); assert(old_block_bunch_pos->pred->action_block == action_block_iter);
2253 block_t*const source_block = old_block_bunch_pos->pred->source->bl.ock; assert(!old_block_bunch_pos->slice.is_null());
2254 block_bunch_slice_iter_t const old_block_bunch_slice(
2255 old_block_bunch_pos->slice);
2256 block_bunch_entry* const new_block_bunch_pos(
2257 old_block_bunch_slice->end - 1); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
2258 assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
2259 new_block_bunch_pos);
2260 // create or adapt the new block_bunch-slice
2261 block_bunch_slice_iter_t new_block_bunch_slice;
2262 if (new_block_bunch_pos + 1 >= block_bunch_inert_begin ||
2263 (new_block_bunch_slice = (block_bunch_slice_iter_t)
2264 new_block_bunch_pos[1].slice, assert(!new_block_bunch_pos[1].slice.is_null()),
2265 bunch_T_a_Bprime != new_block_bunch_slice->bunch ||
2266 source_block != new_block_bunch_slice->source_block()))
2267 { assert(first_transition_of_state);
2268 // This is the first transition in the block_bunch-slice.
2269 // The old block_bunch-slice becomes unstable, and the new
2270 // block_bunch-slice is created unstable.
2271
2272 // Note that the new block_bunch-slice should precede the old one.
2273
2274 #ifdef USE_SIMPLE_LIST
2275 new_block_bunch_slice = splitter_list.emplace_back(
2277 new_block_bunch_pos + 1, bunch_T_a_Bprime, false);
2278 #else
2279 splitter_list.emplace_back(new_block_bunch_pos + 1,
2280 bunch_T_a_Bprime, false);
2281 new_block_bunch_slice = std::prev(splitter_list.end());
2282 #endif
2283 ++nr_of_block_bunch_slices; ONLY_IF_DEBUG( new_block_bunch_slice->work_counter =
2284 old_block_bunch_slice->work_counter; )
2286 source_block->stable_block_bunch, old_block_bunch_slice);
2287 old_block_bunch_slice->make_unstable();
2288 } assert(!new_block_bunch_slice->is_stable());
2289
2290 // move the transition to the end of its block_bunch-slice
2291 if (old_block_bunch_pos < new_block_bunch_pos)
2292 {
2293 std::swap(old_block_bunch_pos->pred, new_block_bunch_pos->pred); assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2294 old_block_bunch_pos->pred->action_block->succ->block_bunch =
2295 old_block_bunch_pos; assert(new_succ_pos == new_block_bunch_pos->pred->action_block->succ);
2296 new_succ_pos->block_bunch = new_block_bunch_pos;
2297 } else assert(new_block_bunch_pos == old_block_bunch_pos);
2298 assert(new_block_bunch_pos->slice == old_block_bunch_slice);
2299 new_block_bunch_pos->slice = new_block_bunch_slice;
2300
2301 /* adapt the old block_bunch-slice */ assert(new_block_bunch_pos + 1 == old_block_bunch_slice->marked_begin);
2302 old_block_bunch_slice->end = new_block_bunch_pos;
2303 old_block_bunch_slice->marked_begin = new_block_bunch_pos; assert(nullptr != new_block_bunch_pos);
2304 if (old_block_bunch_slice->empty())
2305 { assert(!old_block_bunch_slice->is_stable());
2307 old_block_bunch_slice); assert(!new_block_bunch_slice->is_stable());
2309
2310 // Because now every bottom state has a transition in the new
2311 // bunch, and no state has a transition in the old bunch, there
2312 // is no need to refine this block. So we make this
2313 // block_bunch-slice stable again.
2314 source_block->stable_block_bunch.splice(
2315 source_block->stable_block_bunch.end(),
2316 splitter_list, new_block_bunch_slice);
2317 new_block_bunch_slice->make_stable();
2318
2319 // unmark the states
2320 // (This transition must be the last transition from
2321 // source_block in the new bunch, so unmarking the states now
2322 // will not be undone by later markings of other states.)
2323 source_block->marked_nonbottom_begin = source_block->end; assert(source_block->marked_bottom_begin == source_block->begin);
2324 source_block->marked_bottom_begin = source_block->nonbottom_begin;
2325 }
2326 }
2327
2328
2349 ONLY_IF_DEBUG( template <class LTS_TYPE> )
2351 action_block_entry* const action_block_iter, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
2352 bunch_t* const bunch_T_a_Bprime, )
2353 bunch_t* const large_splitter_bunch)
2354 { assert(nullptr != bunch_T_a_Bprime);
2355
2356 /* - - - - - - - - adapt part_tr.succ - - - - - - - - */
2357
2358 // We already moved the transition in part_tr.succ to the correct
2359 // place in first_move_transition_to_new_bunch(); now we have to
2360 // set begin_or_before_end.
2361 succ_entry* const new_succ_pos(action_block_iter->succ); assert(nullptr != new_succ_pos);
2362 assert(new_succ_pos->block_bunch->pred->action_block == action_block_iter);
2363 state_info_entry* const source(
2364 new_succ_pos->block_bunch->pred->source); assert(source->pos->st == source);
2365 assert(new_succ_pos < source->succ_inert.begin);
2366 assert(source == &partitioner.part_st.state_info.front() ||
2367 source[-1].succ_inert.begin <= new_succ_pos);
2368 assert(nullptr != new_succ_pos->begin_or_before_end);
2369 succ_entry* const new_begin_or_before_end(
2370 new_succ_pos->begin_or_before_end->begin_or_before_end); assert(nullptr != new_begin_or_before_end);
2371 assert(new_begin_or_before_end->block_bunch->pred->action_block->succ ==
2372 new_begin_or_before_end);
2373 if (new_begin_or_before_end < new_succ_pos)
2374 { assert(source == &partitioner.part_st.state_info.front() ||
2375 source[-1].succ_inert.begin <= new_begin_or_before_end);
2376 new_succ_pos->begin_or_before_end = new_begin_or_before_end;
2377 }
2378 else
2379 { assert(new_begin_or_before_end == new_succ_pos);
2380 // This is the first or the last transition in the out-slice.
2381 const succ_entry* const new_before_end(
2382 new_begin_or_before_end->begin_or_before_end); assert(nullptr != new_before_end);
2383 if (new_begin_or_before_end <= new_before_end)
2384 { assert(&partitioner.part_tr.succ.cbegin()[1] == new_begin_or_before_end ||
2385 /* This is the first transition in the new out-slice. */ new_begin_or_before_end[-1].block_bunch->pred->source < source ||
2386 /* If there is still a transition in the old out-slice, */ new_begin_or_before_end[-1].bunch() != bunch_T_a_Bprime);
2387 /* we prepay for it. */ assert(new_before_end + 1 == source->succ_inert.begin ||
2388 bunch_T_a_Bprime != new_before_end[1].bunch());
2389 if (source == new_succ_pos[-1].block_bunch->pred->source &&
2390 new_succ_pos[-1].bunch() == large_splitter_bunch)
2391 {
2392 // Mark one transition in the large slice
2393 block_bunch_entry* const old_block_bunch_pos(
2394 new_succ_pos[-1].block_bunch); assert(!old_block_bunch_pos->slice.is_null());
2395 assert(old_block_bunch_pos->pred->action_block->succ == new_succ_pos - 1);
2396 block_bunch_slice_iter_t const large_splitter_slice(
2397 old_block_bunch_pos->slice);
2398 if (!large_splitter_slice->is_stable())
2399 {
2400 block_bunch_entry* const new_block_bunch_pos(
2401 large_splitter_slice->marked_begin - 1); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
2402 assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
2403 new_block_bunch_pos);
2404 if (old_block_bunch_pos < new_block_bunch_pos)
2405 {
2406 std::swap(old_block_bunch_pos->pred,
2407 new_block_bunch_pos->pred); // assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2408 old_block_bunch_pos->pred->action_block->
2409 succ->block_bunch = old_block_bunch_pos; assert(new_block_bunch_pos->pred->action_block->succ == new_succ_pos - 1);
2410 new_succ_pos[-1].block_bunch = new_block_bunch_pos;
2411 }
2412 large_splitter_slice->marked_begin=new_block_bunch_pos; assert(nullptr != new_block_bunch_pos);
2413 } else assert(1 >= source->bl.ock->size());
2414 }
2415 } else assert(source == &partitioner.part_st.state_info.front() ||
2416 source[-1].succ_inert.begin <= new_before_end);
2417 }
2418 #ifndef NDEBUG
2419 /* - - - - - - - adapt part_tr.block_bunch - - - - - - - */ const block_bunch_entry* new_block_bunch_pos(new_succ_pos->block_bunch);
2420 assert(new_block_bunch_pos->pred->action_block->succ == new_succ_pos);
2421 assert(!new_block_bunch_pos->slice.is_null());
2422 /* Nothing needs to be done. */ block_bunch_slice_const_iter_t const new_block_bunch_slice(
2423 new_block_bunch_pos->slice);
2424 assert(new_block_bunch_pos < new_block_bunch_slice->end);
2425 assert(bunch_T_a_Bprime == new_block_bunch_slice->bunch);
2426 if (new_block_bunch_pos + 1 < new_block_bunch_slice->end) return;
2427
2428 // This transition is the last in the block_bunch-slice. If there
2429 // were some task that would need to be done exactly once per
2430 // block_bunch-slice, this would be the moment.
2431 do assert(source->bl.ock == new_block_bunch_pos->pred->source->bl.ock);
2432 while ((--new_block_bunch_pos)->slice == new_block_bunch_slice);
2433 assert(new_block_bunch_pos <= &partitioner.part_tr.block_bunch.front() ||
2434 source->bl.ock != new_block_bunch_pos->pred->source->bl.ock ||
2435 bunch_T_a_Bprime != new_block_bunch_pos->slice->bunch);
2436 #endif
2437 }
2438
2439
2440 private:
2468 ONLY_IF_DEBUG( template <class LTS_TYPE> )
2470 succ_entry* out_slice_end, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
2471 #ifndef USE_SIMPLE_LIST
2472 block_t* const old_block,
2473 #endif
2474 block_bunch_slice_const_iter_t const splitter_T)
2475 { assert(&succ.cbegin()[1] < out_slice_end);
2476 succ_entry* const out_slice_begin(
2477 out_slice_end[-1].begin_or_before_end); assert(nullptr != out_slice_begin);
2478 assert(out_slice_begin < out_slice_end);
2479 assert(out_slice_begin->block_bunch->pred->action_block->succ ==
2480 out_slice_begin);
2481 block_bunch_entry* old_block_bunch_pos(out_slice_end[-1].block_bunch); assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2482 assert(!old_block_bunch_pos->slice.is_null());
2483 block_bunch_slice_iter_t const old_block_bunch_slice(
2484 old_block_bunch_pos->slice); assert(old_block_bunch_pos->pred->action_block->succ->block_bunch ==
2485 old_block_bunch_pos);
2486 if (&*splitter_T == &*old_block_bunch_slice) return out_slice_begin;
2487
2488 block_bunch_entry* old_block_bunch_slice_end(
2489 old_block_bunch_slice->end);
2490 state_info_entry* const source(old_block_bunch_pos->pred->source); assert(out_slice_end <= source->succ_inert.begin);
2491 assert(&partitioner.part_st.state_info.front() == source ||
2492 source[-1].succ_inert.begin < out_slice_end);
2493 block_t* const new_block(source->bl.ock); assert(source == out_slice_begin->block_bunch->pred->source);
2494 block_bunch_slice_iter_t new_block_bunch_slice; assert(source->pos->st == source);
2495 if (old_block_bunch_slice_end >= block_bunch_inert_begin ||
2496 new_block != old_block_bunch_slice_end->pred->source->bl.ock ||
2497 (new_block_bunch_slice = (block_bunch_slice_iter_t)
2498 old_block_bunch_slice_end->slice, assert(!old_block_bunch_slice_end->slice.is_null()),
2499 old_block_bunch_slice->bunch != new_block_bunch_slice->bunch))
2500 {
2501 // the new block_bunch-slice is not suitable; create a new one and
2502 // insert it into the correct list.
2503 if (old_block_bunch_slice->is_stable())
2504 {
2505 // In most cases, but not always, the source is a bottom state.
2506 #ifdef USE_SIMPLE_LIST
2507 new_block_bunch_slice =
2510 old_block_bunch_slice->end,
2511 old_block_bunch_slice->bunch, true);
2512 #else
2514 old_block_bunch_slice->end,
2515 old_block_bunch_slice->bunch, true);
2516 new_block_bunch_slice =
2517 new_block->stable_block_bunch.begin();
2518 #endif
2519 }
2520 else
2521 {
2522 #ifdef USE_SIMPLE_LIST
2523 new_block_bunch_slice = splitter_list.emplace_after(
2525 old_block_bunch_slice,
2526 old_block_bunch_slice->end,
2527 old_block_bunch_slice->bunch, false);
2528 #else
2529 new_block_bunch_slice = splitter_list.emplace(
2530 std::next(old_block_bunch_slice),
2531 old_block_bunch_slice->end,
2532 old_block_bunch_slice->bunch, false);
2533 #endif
2534 }
2535 ++nr_of_block_bunch_slices; ONLY_IF_DEBUG( new_block_bunch_slice->work_counter =
2536 old_block_bunch_slice->work_counter; )
2537 }
2538 ONLY_IF_DEBUG( unsigned max_counter = bisim_gjkw::check_complexity::log_n -
2540 /* move all transitions in this out-slice to the new block_bunch */ assert(out_slice_begin < out_slice_end);
2541 do
2542 { assert(old_block_bunch_pos == out_slice_end[-1].block_bunch);
2543 --out_slice_end; assert(old_block_bunch_pos->slice == old_block_bunch_slice);
2544 assert(source == out_slice_end->block_bunch->pred->source);
2545 --old_block_bunch_slice_end; // assign work already now because the transition may be moved to several
2546 // places:
2547 old_block_bunch_slice_end->slice = new_block_bunch_slice; mCRL2complexity(old_block_bunch_pos->pred, add_work(bisim_gjkw::
2548 check_complexity::move_out_slice_to_new_block, max_counter), partitioner);
2549 if (old_block_bunch_slice->is_stable() || ( assert(!new_block_bunch_slice->is_stable()),
2550 old_block_bunch_slice->marked_begin >
2551 old_block_bunch_slice_end &&
2552 (/* As the old block_bunch-slice has no marked */ assert(nullptr != old_block_bunch_slice_end),
2553 // transitions, it is enough to adapt its marked_begin
2554 // and then do a simple (two-way) swap.
2555 old_block_bunch_slice->marked_begin =
2556 old_block_bunch_slice_end, true)))
2557 {
2558 // The old block_bunch-slice is stable, or it has no
2559 // marked transitions.
2560 std::swap(old_block_bunch_pos->pred,
2561 old_block_bunch_slice_end->pred);
2562 }
2563 else
2564 {
2565 // The old block_bunch-slice is unstable and has marked
2566 // transitions.
2567 pred_entry* const old_pred = old_block_bunch_pos->pred;
2568 if (old_block_bunch_pos < old_block_bunch_slice->marked_begin)
2569 {
2570 // The transition is not marked, but there are other
2571 // marked transitions in the old block_bunch-slice.
2572 // Move the transition to the non-marked part of the
2573 // new block_bunch-slice.
2574 block_bunch_entry* const old_marked_begin =
2575 old_block_bunch_slice->marked_begin - 1; assert(old_block_bunch_pos < old_block_bunch_slice_end);
2576 old_block_bunch_slice->marked_begin = old_marked_begin;
2577
2578 old_block_bunch_pos->pred = old_marked_begin->pred;
2579 old_marked_begin->pred = old_block_bunch_slice_end->pred;
2580 old_block_bunch_slice_end->pred = old_pred; assert(nullptr != old_marked_begin->pred->action_block->succ);
2581
2582 old_marked_begin->pred->action_block->succ->
2583 block_bunch = old_marked_begin;
2584 }
2585 else
2586 {
2587 // The transition is marked. Move to the marked part
2588 // of the new block_bunch-slice.
2589 block_bunch_entry* const new_marked_begin =
2590 new_block_bunch_slice->marked_begin - 1;
2591 new_block_bunch_slice->marked_begin = new_marked_begin; assert(old_block_bunch_pos < new_marked_begin ||
2592 old_block_bunch_pos == old_block_bunch_slice_end);
2593 old_block_bunch_pos->pred=old_block_bunch_slice_end->pred; assert(old_block_bunch_slice_end <= new_marked_begin);
2594 old_block_bunch_slice_end->pred = new_marked_begin->pred;
2595 new_marked_begin->pred = old_pred; assert(out_slice_end == new_marked_begin->pred->action_block->succ);
2596
2597 out_slice_end->block_bunch = new_marked_begin;
2598 }
2599 } assert(nullptr != old_block_bunch_slice_end->pred->action_block->succ);
2600 old_block_bunch_slice_end->pred->action_block->succ->block_bunch =
2601 old_block_bunch_slice_end; assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2602 old_block_bunch_pos->pred->action_block->succ->block_bunch =
2603 old_block_bunch_pos;
2604 }
2605 while (out_slice_begin < out_slice_end &&
2606 (old_block_bunch_pos = out_slice_end[-1].block_bunch, true));
2607 old_block_bunch_slice->end = old_block_bunch_slice_end;
2608
2609 if (old_block_bunch_slice->empty())
2610 {
2611 #ifdef USE_SIMPLE_LIST
2614 old_block_bunch_slice);
2615 #else
2616 if (old_block_bunch_slice->is_stable())
2617 {
2618 // If the new block is R, then the old (U) block loses
2619 // exactly one stable block_bunch-slice, namely the one we
2620 // just stabilised for (`splitter_T`). We could perhaps
2621 // optimize this by moving that slice as a whole to the new
2622 // block -- perhaps later.
2623 //
2624 // If the new block is U, then the old (R) block loses
2625 // no stable block_bunch-slices if it contains any bottom
2626 // state. If it doesn't contain any bottom state, it will
2627 // definitely keep `splitter_T`, but nothing else can be
2628 // guaranteed.
2629 //
2630 // So old_block_bunch_slice may be deleted, in particular
2631 // if the new block is U, but not exclusively.
2632 old_block->stable_block_bunch.erase(old_block_bunch_slice);
2633 }
2634 else
2635 {
2636 splitter_list.erase(old_block_bunch_slice);
2637 }
2638 #endif
2640 }
2641 return out_slice_begin;
2642 }
2643
2644
2655 {
2656 action_block_entry* const old_action_block_pos(
2657 pred_iter->action_block); assert(nullptr != old_action_block_pos->succ);
2658 assert(old_action_block_pos->succ->block_bunch->pred == pred_iter);
2659 action_block_entry* const action_block_slice_begin(
2661 )); assert(nullptr != action_block_slice_begin->succ);
2662 assert(action_block_slice_begin->succ->block_bunch->pred->action_block ==
2663 action_block_slice_begin);
2664 action_block_entry* const new_action_block_pos(
2665 action_block_slice_begin->begin_or_before_end); assert(nullptr != new_action_block_pos);
2666 assert(action_block_slice_begin == new_action_block_pos->begin_or_before_end);
2667 assert(nullptr != new_action_block_pos->succ);
2668 assert(new_action_block_pos->succ->block_bunch->pred->action_block ==
2669 /* move the transition to the end of the action_block-slice */ new_action_block_pos);
2670 if (old_action_block_pos < new_action_block_pos)
2671 {
2672 succ_entry* const temp(new_action_block_pos->succ); assert(nullptr != temp); assert(nullptr != old_action_block_pos->succ);
2673 new_action_block_pos->succ = old_action_block_pos->succ;
2674 old_action_block_pos->succ = temp;
2675 temp->block_bunch->pred->action_block = old_action_block_pos; assert(pred_iter == new_action_block_pos->succ->block_bunch->pred);
2676 pred_iter->action_block = new_action_block_pos;
2677
2678 // adapt the old action_block-slice immediately
2679 action_block_slice_begin->begin_or_before_end =
2680 new_action_block_pos - 1;
2681 }
2682 else
2683 { assert(old_action_block_pos == new_action_block_pos);
2684 if (action_block_slice_begin < new_action_block_pos)
2685 {
2686 // The old action_block-slice is not empty, so we have to adapt
2687 // the pointer at the beginning. (If it is empty, it may
2688 // happen that `new_action_block_pos - 1` is an illegal value.)
2689 action_block_slice_begin->begin_or_before_end =
2690 new_action_block_pos - 1;
2691 }
2693 } assert(nullptr != new_action_block_pos->succ);
2694 assert(pred_iter == new_action_block_pos->succ->block_bunch->pred);
2695 // adapt the new action_block-slice, as far as is possible now
2696 // make the begin_or_before_end pointers of the first and last
2697 // transition in the slice correct immediately. The other
2698 // begin_or_before_end pointers need to be corrected after all
2699 // transitions in the new bunch have been positioned correctly.
2700 if (new_action_block_pos + 1 >= action_block_inert_begin ||
2701 nullptr == new_action_block_pos[1].succ ||
2702 new_action_block_pos[1].succ->bunch() !=
2703 new_action_block_pos->succ->bunch() ||
2704 new_action_block_pos[1].succ->block_bunch->pred->target->bl.ock !=
2705 pred_iter->target->bl.ock)
2706 {
2707 // This is the first transition that moves to this new
2708 // action_block-slice.
2709 new_action_block_pos->begin_or_before_end = new_action_block_pos;
2711 }
2712 else
2713 {
2714 action_block_entry* const action_block_slice_before_end(
2715 new_action_block_pos[1].begin_or_before_end); assert(nullptr != action_block_slice_before_end);
2716 assert(new_action_block_pos < action_block_slice_before_end);
2717 assert(nullptr != action_block_slice_before_end->succ);
2718 assert(action_block_slice_before_end->succ->block_bunch->pred->action_block ==
2719 action_block_slice_before_end);
2720 assert(new_action_block_pos + 1 ==
2721 action_block_slice_before_end->begin_or_before_end);
2722 action_block_slice_before_end->begin_or_before_end =
2723 new_action_block_pos; assert(action_block_slice_before_end->succ->block_bunch->
2724 pred->target->bl.ock == pred_iter->target->bl.ock);
2725 new_action_block_pos->begin_or_before_end =
2726 action_block_slice_before_end; assert(action_block_slice_before_end < action_block_inert_begin);
2727 }
2728 }
2729
2730
2738 pred_entry* const pred_iter)
2739 {
2740 action_block_entry* const new_action_block_pos(
2741 pred_iter->action_block); assert(nullptr != new_action_block_pos->succ);
2742 assert(new_action_block_pos->succ->block_bunch->pred == pred_iter);
2743 action_block_entry* const old_begin_or_before_end(
2744 new_action_block_pos->begin_or_before_end); assert(nullptr != old_begin_or_before_end);
2745 assert(nullptr != old_begin_or_before_end->succ);
2746 assert(old_begin_or_before_end->succ->block_bunch->pred->action_block ==
2747 old_begin_or_before_end);
2748 if (action_block_entry* const new_begin_or_before_end(
2749 old_begin_or_before_end->begin_or_before_end); assert(nullptr != new_begin_or_before_end),
2750 assert(nullptr != new_begin_or_before_end->succ),
2751 assert(new_begin_or_before_end->succ->block_bunch->pred->action_block ==
2752 new_begin_or_before_end),
2753 new_begin_or_before_end < new_action_block_pos)
2754 { assert(old_begin_or_before_end==new_begin_or_before_end->begin_or_before_end);
2755 new_action_block_pos->begin_or_before_end =
2756 new_begin_or_before_end; assert(new_action_block_pos <= old_begin_or_before_end);
2757 return;
2758 } else assert(new_begin_or_before_end == new_action_block_pos);
2759 if (old_begin_or_before_end < new_action_block_pos) return;
2760
2761 // this is the first transition in the new action_block-slice.
2762 // Check whether the bunch it belongs to has become nontrivial.
2763 bunch_t* const bunch(new_action_block_pos->succ->bunch());
2764 if (!bunch->is_trivial()) { return; } assert(old_begin_or_before_end + 1 == bunch->end);
2765 if (bunch->begin < new_action_block_pos)
2766 {
2767 make_nontrivial(bunch);
2768 }
2769 }
2770
2771
2796 bool make_noninert(pred_entry* const old_pred_pos,
2797 block_bunch_slice_iter_or_null_t* const new_noninert_block_bunch_ptr)
2798 {
2799 state_info_entry* const source(old_pred_pos->source); assert(source->pos->st == source);
2800 state_info_entry* const target(old_pred_pos->target); assert(target->pos->st == target);
2801
2802 action_block_entry* const new_action_block_pos(
2803 action_block_inert_begin++); assert(nullptr != new_action_block_pos->succ);
2804 assert(new_action_block_pos->succ->block_bunch->pred->action_block ==
2805 new_action_block_pos);
2806 succ_entry* const new_succ_pos(source->succ_inert.begin++); assert(new_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
2807 block_bunch_entry* const new_block_bunch_pos(
2808 block_bunch_inert_begin++); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
2809 assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
2810 new_block_bunch_pos);
2811 action_block_entry* const old_action_block_pos(
2812 old_pred_pos->action_block); assert(new_action_block_pos <= old_action_block_pos);
2813
2814 succ_entry* const old_succ_pos(old_action_block_pos->succ); assert(nullptr != old_succ_pos);
2815 block_bunch_entry* const old_block_bunch_pos(
2816 old_succ_pos->block_bunch); assert(old_pred_pos == old_block_bunch_pos->pred);
2817 pred_entry* const new_pred_pos(target->pred_inert.begin++); assert(nullptr != new_pred_pos->action_block->succ);
2818 assert(new_pred_pos->action_block->succ->block_bunch->pred == new_pred_pos);
2819
2820 /* adapt action_block */ assert(nullptr == new_action_block_pos->begin_or_before_end);
2821 if (new_action_block_pos < old_action_block_pos)
2822 { assert(nullptr == old_action_block_pos->begin_or_before_end);
2823 old_action_block_pos->succ = new_action_block_pos->succ; assert(nullptr != old_action_block_pos->succ);
2824 assert(old_action_block_pos->succ->block_bunch->pred->action_block ==
2825 new_action_block_pos);
2826 old_action_block_pos->succ->block_bunch->pred->action_block =
2827 old_action_block_pos;
2828 } else assert(new_action_block_pos == old_action_block_pos);
2829 new_action_block_pos->succ = new_succ_pos; assert(nullptr != new_succ_pos);
2830 // new_action_block_pos->begin_or_before_end = ...; -- see below
2831
2832 /* adapt succ */ assert(nullptr == new_succ_pos->begin_or_before_end);
2833 if (new_succ_pos < old_succ_pos)
2834 { assert(nullptr == old_succ_pos->begin_or_before_end);
2835 old_succ_pos->block_bunch = new_succ_pos->block_bunch; assert(old_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
2836 old_succ_pos->block_bunch->pred->action_block->succ = old_succ_pos; assert(nullptr != old_succ_pos);
2837 } else assert(new_succ_pos == old_succ_pos);
2838 new_succ_pos->block_bunch = new_block_bunch_pos;
2839 // new_succ_pos->begin_or_before_end = ...; -- see below
2840
2841 /* adapt block_bunch */ assert(new_block_bunch_pos->slice.is_null());
2842 if (new_block_bunch_pos < old_block_bunch_pos)
2843 { assert(old_block_bunch_pos->slice.is_null());
2844 assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2845 old_block_bunch_pos->pred = new_block_bunch_pos->pred; assert(old_block_bunch_pos->pred->action_block->succ->block_bunch ==
2846 new_block_bunch_pos);
2847 assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2848 old_block_bunch_pos->pred->action_block->succ->block_bunch =
2849 old_block_bunch_pos;
2850 } else assert(new_block_bunch_pos == old_block_bunch_pos);
2851 new_block_bunch_pos->pred = new_pred_pos;
2852 // new_block_bunch_pos->slice = ...; -- see below
2853
2854 // adapt pred
2855 if (new_pred_pos < old_pred_pos)
2856 {
2857 // We need std::swap here to swap the whole content, including
2858 // work counters in case we measure the work.
2859 std::swap(*old_pred_pos, *new_pred_pos); assert(nullptr != old_pred_pos->action_block->succ);
2860 assert(old_pred_pos->action_block->succ->block_bunch->pred == new_pred_pos);
2861 old_pred_pos->action_block->succ->block_bunch->pred = old_pred_pos;
2862 } else assert(new_pred_pos == old_pred_pos);
2863 new_pred_pos->action_block = new_action_block_pos;
2864
2865 /* make the state a bottom state if necessary */ assert(source->bl.ock->nonbottom_begin <= source->pos);
2866 bool became_bottom(false); assert(succ.back().block_bunch->pred->source != source);
2867 if (source != source->succ_inert.begin->block_bunch->pred->source)
2868 {
2869 block_t* const source_block(source->bl.ock);
2870 // make the state a marked bottom state
2871 if (source->pos >= source_block->marked_nonbottom_begin)
2872 {
2873 std::swap(*source->pos,
2874 *source_block->marked_nonbottom_begin++);
2875 } assert(source->pos < source_block->marked_nonbottom_begin);
2876 std::swap(*source->pos, *source_block->nonbottom_begin++);
2878 became_bottom = true;
2879 }
2880
2881 bunch_t* new_noninert_bunch; assert(nullptr != new_action_block_pos);
2882 if (!new_noninert_block_bunch_ptr->is_null())
2883 {
2884 // There is already some new non-inert transition from this block.
2885 // So we can reuse this block_bunch and its bunch.
2886 // (However, it may be the case that the current transition goes to
2887 // another block; in the latter case, we have to create a new
2888 // action_block-slice.)
2889
2890 // extend the bunch
2891 new_noninert_bunch = (*new_noninert_block_bunch_ptr)->bunch; assert(new_action_block_pos == new_noninert_bunch->end ||
2892 (nullptr == new_action_block_pos[-1].succ &&
2893 new_action_block_pos - 1 == new_noninert_bunch->end));
2894 new_noninert_bunch->end = action_block_inert_begin;
2895 /* extend the block_bunch-slice */ assert((*new_noninert_block_bunch_ptr)->end == new_block_bunch_pos);
2896 (*new_noninert_block_bunch_ptr)->end = block_bunch_inert_begin;
2897 if (!(*new_noninert_block_bunch_ptr)->is_stable())
2898 { assert((*new_noninert_block_bunch_ptr)->marked_begin == new_block_bunch_pos);
2899 (*new_noninert_block_bunch_ptr)->marked_begin =
2901 }
2902 new_block_bunch_pos->slice = *new_noninert_block_bunch_ptr;
2903
2904 /* adapt the action_block-slice */ assert(new_noninert_bunch->begin < new_action_block_pos);
2905 if (nullptr != new_action_block_pos[-1].succ &&
2906 target->bl.ock == new_action_block_pos[-1].
2907 succ->block_bunch->pred->target->bl.ock)
2908 {
2909 // the action_block-slice is suitable: extend it
2910 action_block_entry* const action_block_slice_begin(
2911 new_action_block_pos[-1].begin_or_before_end); assert(nullptr != action_block_slice_begin);
2912 assert(new_action_block_pos-1==action_block_slice_begin->begin_or_before_end);
2913 assert(nullptr != action_block_slice_begin->succ);
2914 assert(action_block_slice_begin->succ->block_bunch->pred->action_block ==
2915 action_block_slice_begin);
2916 action_block_slice_begin->begin_or_before_end =
2917 new_action_block_pos;
2918 new_action_block_pos->begin_or_before_end =
2919 action_block_slice_begin;
2920 }
2921 else
2922 {
2923 // create a new action_block-slice
2924 new_action_block_pos->begin_or_before_end=new_action_block_pos;
2925 if (new_noninert_bunch->is_trivial())
2926 { // Only during initialisation, it may happen that we add new non-inert
2927 make_nontrivial(new_noninert_bunch); // transitions to a nontrivial bunch:
2928 }
2929 #ifndef NDEBUG
2930 else
2931 {
2932 // We make sure that new_noninert_bunch is the first bunch in
2933 // action_block (and because it's always the last one, it will be the
2934 // only one, so there is only one bunch, as ).
2935 for (const action_block_entry* iter = action_block_begin;
2936 iter < new_noninert_bunch->begin; ++iter)
2937 {
2938 assert(nullptr == iter->succ);
2939 assert(nullptr == iter->begin_or_before_end);
2940 }
2941 }
2942 #endif
2944 }
2945
2946 /* adapt the out-slice */ assert(source != succ.front().block_bunch->pred->source);
2947 if (source == new_succ_pos[-1].block_bunch->pred->source &&
2948 new_succ_pos[-1].bunch() == new_noninert_bunch)
2949 {
2950 // the out-slice is suitable: extend it.
2951 succ_entry* const out_slice_begin(
2952 new_succ_pos[-1].begin_or_before_end); assert(nullptr != out_slice_begin);
2953 assert(new_succ_pos - 1 == out_slice_begin->begin_or_before_end);
2954 out_slice_begin->begin_or_before_end = new_succ_pos; assert(out_slice_begin->block_bunch->pred->action_block->succ ==
2955 out_slice_begin);
2956 new_succ_pos->begin_or_before_end = out_slice_begin;
2957 return became_bottom;
2958 }
2959 }
2960 else
2961 {
2962 // create a new bunch for noninert transitions
2963 new_noninert_bunch =
2964 #ifdef USE_POOL_ALLOCATOR
2965 storage.template construct<bunch_t>
2966 #else
2967 new bunch_t
2968 #endif
2969 (new_action_block_pos, action_block_inert_begin);
2970 ++nr_of_bunches;
2971
2972 // create a new block_bunch-slice
2973 #ifdef USE_SIMPLE_LIST
2974 block_bunch_slice_iter_t new_noninert_block_bunch(
2977 block_bunch_inert_begin, new_noninert_bunch, false));
2978 #else
2980 new_noninert_bunch, false);
2981 block_bunch_slice_iter_t new_noninert_block_bunch(
2982 std::prev(splitter_list.end()));
2983 #endif
2985 new_block_bunch_pos->slice = new_noninert_block_bunch;
2986 *new_noninert_block_bunch_ptr = new_noninert_block_bunch;
2987
2988 // create a new action_block-slice
2989 new_action_block_pos->begin_or_before_end = new_action_block_pos;
2991 } assert(&succ.cbegin()[1] == new_succ_pos ||
2992 new_succ_pos[-1].block_bunch->pred->source < source ||
2993 /* create a new out-slice */ new_succ_pos[-1].bunch() != new_noninert_bunch);
2994 new_succ_pos->begin_or_before_end = new_succ_pos;
2995 return became_bottom;
2996 }
2997
2998
2999 public:
3021 ONLY_IF_DEBUG( template<class LTS_TYPE> )
3023 block_t* const new_block,
3024 block_t* const old_block, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
3025 bool const add_new_noninert_to_splitter,
3026 const block_bunch_slice_iter_t splitter_T,
3027 enum new_block_mode_t const new_block_mode)
3028 { assert(splitter_T->is_stable());
3029 // We begin with a bottom state so the new block gets a sorted list of
3030 // stable block_bunch-slices.
3031 permutation_entry* s_iter(new_block->begin); assert(s_iter < new_block->end);
3032 do
3033 {
3034 state_info_entry* const s(s_iter->st); assert(new_block == s->bl.ock);
3035 assert(s->pos == s_iter);
3036 /* - - - - - - adapt part_tr.block_bunch - - - - - - */
3037 assert(s != succ.front().block_bunch->pred->source);
3038 for (succ_entry* succ_iter(s->succ_inert.begin);
3039 s == succ_iter[-1].block_bunch->pred->source; )
3040 {
3041 succ_iter = move_out_slice_to_new_block(succ_iter, ONLY_IF_DEBUG( partitioner, )
3042 #ifndef USE_SIMPLE_LIST
3043 old_block,
3044 #endif
3045 splitter_T); assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
3046 assert(s == succ_iter->block_bunch->pred->source);
3047 // add_work_to_out_slice(succ_iter, ...) -- subsumed in the call below
3048 }
3049
3050 /*- - - - - - adapt part_tr.action_block - - - - - -*/
3051 assert(s != pred.front().target);
3052 for (pred_entry* pred_iter(s->pred_inert.begin);
3053 s == (--pred_iter)->target; )
3054 { assert(&pred.front() < pred_iter);
3055 assert(nullptr != pred_iter->action_block->succ);
3056 assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
3057 first_move_transition_to_new_action_block(pred_iter); // mCRL2complexity(pred_iter, ...) -- subsumed in the call below
3058 } // mCRL2complexity(s, ...) -- subsumed in the call at the end
3059 }
3060 while (++s_iter < new_block->end);
3061
3062 if (new_block_is_R == new_block_mode)
3063 { assert(splitter_T->source_block() == new_block);
3064 // The `splitter_T` slice moves completely from the old to the new
3065 // block. We move it as a whole to the new block_bunch list.
3066 new_block->stable_block_bunch.splice(
3067 new_block->stable_block_bunch.begin(),
3068 old_block->stable_block_bunch, splitter_T);
3069 } else assert(splitter_T->source_block() == old_block);
3070
3071 // We cannot join the loop above with the one below because transitions
3072 // in the action_block-slices need to be handled in two phases.
3073
3074 s_iter = new_block->begin; assert(s_iter < new_block->end);
3075 do
3076 {
3077 state_info_entry* const s(s_iter->st); assert(s->pos == s_iter); assert(s != pred.front().target);
3078 for (pred_entry* pred_iter(s->pred_inert.begin);
3079 s == (--pred_iter)->target; )
3080 { assert(&pred.front() < pred_iter);
3081 assert(nullptr != pred_iter->action_block->succ);
3082 assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
3083 second_move_transition_to_new_action_block(pred_iter); // mCRL2complexity(pred_iter, ...) -- subsumed in the call below
3084 } // mCRL2complexity(s, ...) -- subsumed in the call at the end
3085 }
3086 while (++s_iter < new_block->end);
3087 assert(0 == new_block->marked_size()); assert(0 == old_block->marked_size());
3088 /* - - - - - - find new non-inert transitions - - - - - - */ assert(1 + &block_bunch.back() - block_bunch_inert_begin ==
3090 if (block_bunch_inert_begin <= &block_bunch.back())
3091 {
3092 block_bunch_slice_iter_or_null_t new_noninert_block_bunch;
3093 if (add_new_noninert_to_splitter)
3094 {
3095 new_noninert_block_bunch = splitter_T;
3096 }
3097 else
3098 {
3099 new_noninert_block_bunch = nullptr;
3100 }
3101 if (new_block_is_U == new_block_mode)
3102 { assert(old_block == new_block->end->st->bl.ock);
3103 assert(new_block->end <= &partitioner.part_st.permutation.back());
3104 permutation_entry* target_iter(new_block->begin); assert(target_iter < new_block->end);
3105 do
3106 {
3107 state_info_entry* const s(target_iter->st); assert(s->pos == target_iter);
3108 // check all incoming inert transitions of s, whether they
3109 /* still start in new_block */ assert(s != pred.back().target);
3110 for (pred_entry* pred_iter(s->pred_inert.begin);
3111 s == pred_iter->target; ++pred_iter)
3112 { assert(pred_iter < &pred.back());
3113 assert(nullptr != pred_iter->action_block->succ);
3114 state_info_entry* const t(pred_iter->source); assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
3115 assert(t->pos->st == t);
3116 if (new_block != t->bl.ock)
3117 { assert(old_block == t->bl.ock);
3118 if (!make_noninert(pred_iter,
3119 &new_noninert_block_bunch))
3120 // make_noninert() may modify *pred_iter
3121 {
3122 old_block->mark_nonbottom(t->pos);
3123 }
3124 } // mCRL2complexity(old value of *pred_iter, ...) -- overapproximated by the
3125 // call below
3126 } // mCRL2complexity(s, ...) -- subsumed in the call at the end
3127 }
3128 while (++target_iter < new_block->end); assert(0 < old_block->bottom_size());
3129 }
3130 else
3131 { assert(new_block_is_R == new_block_mode);
3132 /* We have to be careful because make_noninert may move */ assert(&partitioner.part_st.permutation.front() < new_block->begin);
3133 /* a state either forward (to the marked states) or */ assert(old_block == new_block->begin[-1].st->bl.ock);
3134 /* back (to the bottom states). */ assert(0 < old_block->bottom_size());
3135 for(permutation_entry* source_iter(new_block->nonbottom_begin);
3136 source_iter < new_block->marked_nonbottom_begin; )
3137 {
3138 state_info_entry* const s(source_iter->st); assert(s->pos == source_iter);
3139 // check all outgoing inert transitions of s, whether they
3140 /* still end in new_block. */ assert(succ.back().block_bunch->pred->source != s);
3141 succ_entry* succ_iter(s->succ_inert.begin); assert(succ_iter < &succ.back());
3142 bool dont_mark(true); assert(s == succ_iter->block_bunch->pred->source);
3143 do
3144 { assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
3145 if (new_block !=
3146 succ_iter->block_bunch->pred->target->bl.ock)
3147 { assert(old_block == succ_iter->block_bunch->pred->target->bl.ock);
3148 dont_mark = make_noninert(
3149 succ_iter->block_bunch->pred,
3150 &new_noninert_block_bunch);
3151 } // mCRL2complexity(succ_iter->block_bunch->pred, ...) -- overapproximated by
3152 // the call below
3153 }
3154 while (s == (++succ_iter)->block_bunch->pred->source);
3155 if (dont_mark) ++source_iter;
3156 else
3157 { assert(s->pos == source_iter);
3158 new_block->mark_nonbottom(source_iter);
3159 } assert(new_block->nonbottom_begin <= source_iter);
3160 // mCRL2complexity(s, ...) -- overapproximated by the call at the end
3161 }
3162 }
3163 } else assert(block_bunch_inert_begin == 1 + &block_bunch.back());
3164 mCRL2complexity(new_block, add_work(bisim_gjkw::check_complexity::
3166 bisim_gjkw::check_complexity::ilog2(new_block->size())), partitioner);
3167 }
3168 #ifndef NDEBUG
3171 template <class LTS_TYPE>
3172 void print_trans(const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
3173 {
3174 if (!mCRL2logEnabled(log::debug)) return;
3175 // print all outgoing transitions grouped per successor and out-slice
3176 const succ_entry* succ_iter(&succ.cbegin()[1]);
3177 if (succ_iter >= &succ.back())
3178 {
3179 mCRL2log(log::debug) << "No transitions.\n";
3180 return;
3181 }
3182 const state_info_entry* source(succ_iter->block_bunch->pred->source);
3183 mCRL2log(log::debug) << source->debug_id(partitioner)
3184 << ":\n";
3185 block_bunch_slice_iter_or_null_t current_out_bunch(
3186 const_cast<part_trans_t*>(this)->splitter_list.end());
3187 do
3188 {
3189 if (source != succ_iter->block_bunch->pred->source)
3190 { assert(source < succ_iter->block_bunch->pred->source);
3191 source = succ_iter->block_bunch->pred->source;
3193 << source->debug_id(partitioner) << ":\n";
3194 current_out_bunch =
3195 const_cast<part_trans_t*>(this)->splitter_list.end();
3196 }
3197 if (succ_iter->block_bunch->slice != current_out_bunch)
3198 { assert(!current_out_bunch.is_null());
3199 if (succ_iter->block_bunch->slice.is_null())
3200 { assert(succ_iter == source->succ_inert.begin);
3201 mCRL2log(log::debug)<<"\tInert successors:\n";
3202 current_out_bunch = nullptr;
3203 }
3204 else
3205 { assert(succ_iter < source->succ_inert.begin);
3206 assert(!current_out_bunch.is_null());
3207 assert(current_out_bunch == splitter_list.end() ||
3208 current_out_bunch->bunch != succ_iter->bunch());
3209 mCRL2log(log::debug) << "\tSuccessors in "
3210 <<succ_iter->bunch()->debug_id_short(partitioner)<<":\n";
3211 current_out_bunch = succ_iter->block_bunch->slice;
3212 }
3213 }
3214 mCRL2log(log::debug) << "\t\t"
3215 << succ_iter->block_bunch->pred->debug_id(partitioner) << '\n';
3216 }
3217 while (++succ_iter < &succ.back());
3218
3219 // print all transitions grouped per bunch and action_block-slice
3220 const action_block_entry* action_block_iter(action_block_begin);
3221 do assert(action_block_iter < action_block_end);
3222 while (nullptr == action_block_iter->succ &&
3223 (assert(nullptr == action_block_iter->begin_or_before_end),
3224 ++action_block_iter, true));
3225 do
3226 {
3227 const action_block_entry* bunch_end;
3228 const action_block_entry* action_block_slice_end;
3229 assert(nullptr != action_block_iter->succ);
3230 if (action_block_iter->succ->block_bunch->slice.is_null())
3231 { assert(action_block_iter == action_block_inert_begin);
3232 mCRL2log(log::debug) <<"Inert transition slice [";
3233 action_block_slice_end = bunch_end = action_block_end;
3234 }
3235 else
3236 {
3237 const bunch_t* const bunch(action_block_iter->succ->bunch());
3238 assert(nullptr != bunch);
3240 partitioner) << ":\n\taction_block-slice [";
3241 assert(bunch->begin == action_block_iter);
3242 bunch_end = bunch->end;
3243 assert(bunch_end <= action_block_inert_begin);
3244 assert(nullptr != action_block_iter->begin_or_before_end);
3245 action_block_slice_end =
3246 action_block_iter->begin_or_before_end + 1;
3247 }
3248 assert(action_block_slice_end <= bunch_end);
3249 // for all action_block-slices in bunch
3250 for (;;)
3251 {
3252 mCRL2log(log::debug) << (action_block_iter -
3253 action_block_begin) << ","
3254 << (action_block_slice_end - action_block_begin) << "):\n";
3255 // for all transitions in the action_block-slice
3256 assert(action_block_iter < action_block_slice_end);
3257 do
3258 {
3259 assert(nullptr != action_block_iter->succ);
3260 mCRL2log(log::debug) << "\t\t"
3261 << action_block_iter->succ->block_bunch->
3262 pred->debug_id(partitioner) << '\n';
3263 }
3264 while (++action_block_iter < action_block_slice_end);
3265 // go to next action_block-slice in the same bunch
3266 while (action_block_iter < bunch_end &&
3267 nullptr == action_block_iter->succ)
3268 {
3269 assert(nullptr == action_block_iter->begin_or_before_end);
3270 ++action_block_iter;
3271 assert(action_block_iter < bunch_end);
3272 }
3273 if (action_block_iter >= bunch_end) break;
3274 assert(nullptr != action_block_iter->begin_or_before_end);
3275 action_block_slice_end =
3276 action_block_iter->begin_or_before_end + 1;
3277 mCRL2log(log::debug) << "\taction_block-slice [";
3278 }
3279 // go to next bunch
3280 assert(action_block_iter == bunch_end);
3281 while (action_block_iter < action_block_end &&
3282 nullptr == action_block_iter->succ)
3283 {
3284 assert(nullptr == action_block_iter->begin_or_before_end);
3285 ++action_block_iter;
3286 }
3287 }
3288 while (action_block_iter < action_block_end);
3289 }
3290 #endif
3291};
3292
3293
3305 ONLY_IF_DEBUG( template<class LTS_TYPE> )
3306inline block_t* block_t::split_off_block(
3307 enum new_block_mode_t const new_block_mode, ONLY_IF_DEBUG( const bisim_partitioner_dnj<LTS_TYPE>& partitioner, )
3309 my_pool<simple_list<block_bunch_slice_t>::entry>& storage, )
3310 state_type const new_seqnr)
3311{ assert(0 < marked_size()); assert(0 < unmarked_bottom_size());
3312 // create a new block
3313 block_t* new_block;
3314 state_type swapcount(std::min(marked_bottom_size(),
3315 unmarked_nonbottom_size()));
3316 if (permutation_entry* const splitpoint(marked_bottom_begin +
3317 unmarked_nonbottom_size()); assert(begin < splitpoint), assert(splitpoint < end),
3318 assert(splitpoint->st->pos == splitpoint),
3319 new_block_is_U == new_block_mode)
3320 { assert((state_type) (splitpoint - begin) <= size()/2);
3321 new_block =
3322 #ifdef USE_POOL_ALLOCATOR
3323 storage.template construct<block_t>
3324 #else
3325 new block_t
3326 #endif
3327 (begin, splitpoint, new_seqnr);
3328 new_block->nonbottom_begin = marked_bottom_begin;
3329
3330 // adapt the old block: it only keeps the R-states
3331 begin = splitpoint;
3332 nonbottom_begin = marked_nonbottom_begin;
3333 }
3334 else
3335 { assert(new_block_is_R == new_block_mode);
3336 new_block =
3337 #ifdef USE_POOL_ALLOCATOR
3338 storage.template construct<block_t>
3339 #else
3340 new block_t
3341 #endif
3342 (splitpoint, end, new_seqnr);
3343 new_block->nonbottom_begin = marked_nonbottom_begin; assert((state_type) (end - splitpoint) <= size()/2);
3344
3345 // adapt the old block: it only keeps the U-states
3346 end = splitpoint;
3347 nonbottom_begin = marked_bottom_begin;
3348 } ONLY_IF_DEBUG( new_block->work_counter = work_counter; )
3349
3350 // swap contents
3351
3352 // The structure of a block is
3353 // | unmarked | marked | unmarked | marked |
3354 // | bottom | bottom | non-bottom | non-bottom |
3355 // We have to swap the marked bottom with the unmarked non-bottom
3356 // states.
3357 //
3358 // It is not necessary to reset the untested_to_U counters; these
3359 // counters are anyway only valid for the states in the respective
3360 // slice.
3361
3362 if (0 < swapcount)
3363 {
3364 // vector swap the states:
3365 permutation_entry* pos1(marked_bottom_begin);
3366 permutation_entry* pos2(marked_nonbottom_begin); assert(pos1 < pos2);
3367 permutation_entry const temp(std::move(*pos1));
3368 for (;;)
3369 {
3370 --pos2; assert(pos1 < pos2);
3371 *pos1 = std::move(*pos2);
3372 ++pos1;
3373 if (0 >= --swapcount) { break; } assert(pos1 < pos2);
3374 *pos2 = std::move(*pos1); // mCRL2complexity(new_block_is_U == new_block_mode ? pos1[-1] : *pos2, ...)
3375 } // -- overapproximated by the call at the end
3376 *pos2 = std::move(temp); // mCRL2complexity(new_block_is_U == new_block_mode ? pos1[-1] : *pos2, ...)
3377 } // -- overapproximated by the call at the end
3378 #ifndef NDEBUG
3379 { const permutation_entry* s_iter(begin); assert(s_iter < end);
3380 do assert(s_iter->st->pos == s_iter);
3381 while (++s_iter < end); }
3382 #endif
3383 // unmark all states in both blocks
3384 marked_nonbottom_begin = end;
3385 marked_bottom_begin = nonbottom_begin;
3386 new_block->marked_bottom_begin = new_block->nonbottom_begin; assert(new_block->size() <= size());
3387
3388 /* set the block pointer of states in the new block */ assert(new_block->marked_nonbottom_begin == new_block->end);
3389 permutation_entry* s_iter(new_block->begin); assert(s_iter < new_block->end);
3390 do
3391 { assert(s_iter->st->pos == s_iter);
3392 s_iter->st->bl.ock = new_block; // mCRL2complexity (*s_iter, ...) -- subsumed in the call below
3393 }
3394 while (++s_iter < new_block->end); mCRL2complexity(new_block, add_work(bisim_gjkw::check_complexity::
3395 split_off_block, bisim_gjkw::check_complexity::log_n -
3397 partitioner);
3398 return new_block;
3399}
3400
3401
3413 part_trans_t& part_tr)
3414{ assert(begin < end); assert(nullptr != begin->succ);
3415 assert(nullptr != begin->begin_or_before_end);
3416 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);
3417 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);
3418 bunch_t* bunch_T_a_Bprime;
3419 /* 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);
3420 /* |T--a-->B'| < 1/2 |T| */ assert(nullptr != last_slice_begin->succ);
3421 if (first_slice_end - begin > end - last_slice_begin)
3422 {
3423 // Line 2.7: Pi_t := Pi_t \ {T} union { T--a-->B', T \ T--a-->B' }
3424 bunch_T_a_Bprime =
3425 #ifdef USE_POOL_ALLOCATOR
3426 part_tr.storage.template construct<bunch_t>
3427 #else
3428 new bunch_t
3429 #endif
3430 (last_slice_begin, end); assert(nullptr != bunch_T_a_Bprime);
3431 end = last_slice_begin;
3432 while (nullptr == end[-1].succ)
3433 {
3434 --end; assert(first_slice_end <= end); assert(nullptr == end->begin_or_before_end);
3435 } assert(nullptr != end[-1].begin_or_before_end);
3436 if (first_slice_end == end) part_tr.make_trivial(this);
3437 }
3438 else
3439 {
3440 // Line 2.7: Pi_t := Pi_t \ {T} union { T--a-->B', T \ T--a-->B' }
3441 bunch_T_a_Bprime =
3442 #ifdef USE_POOL_ALLOCATOR
3443 part_tr.storage.template construct<bunch_t>
3444 #else
3445 new bunch_t
3446 #endif
3447 (begin, first_slice_end); assert(nullptr != bunch_T_a_Bprime);
3448 begin = first_slice_end;
3449 while (nullptr == begin->succ)
3450 { assert(nullptr == begin->begin_or_before_end);
3451 ++begin; assert(begin <= last_slice_begin);
3452 } assert(nullptr != begin->begin_or_before_end);
3453 if (begin == last_slice_begin) part_tr.make_trivial(this);
3454 } ONLY_IF_DEBUG( bunch_T_a_Bprime->work_counter = work_counter; )
3455 ++part_tr.nr_of_bunches;
3456 return bunch_T_a_Bprime;
3457}
3459
3460} // end namespace bisim_dnj
3461
3462
3463
3464
3465
3466/* ************************************************************************* */
3467/* */
3468/* A L G O R I T H M S */
3469/* */
3470/* ************************************************************************* */
3471
3472
3473
3474
3475
3479
3480
3481
3482/*=============================================================================
3483= main class =
3484=============================================================================*/
3485
3486
3487
3488
3489
3493template <class LTS_TYPE>
3495{
3496 private:
3501
3503 LTS_TYPE& aut;
3504 ONLY_IF_DEBUG( public: )
3506 bisim_dnj::part_state_t part_st;
3507
3511 private:
3523 ONLY_IF_DEBUG( public: )
3525 bool const branching;
3526 private:
3533 #ifndef NDEBUG
3536 #endif
3537 public:
3549 bisim_partitioner_dnj(LTS_TYPE& new_aut, bool const new_branching = false,
3550 bool const new_preserve_divergence = false)
3551 : aut(new_aut),
3552 part_st(new_aut.num_states()),
3553 part_tr(new_aut.num_transitions(), new_aut.num_action_labels()),
3554 action_label(new_aut.num_action_labels()),
3555 branching(new_branching),
3556 preserve_divergence(new_preserve_divergence)
3557 { assert(branching || !preserve_divergence);
3561 }
3562
3563
3569 {
3570 return part_st.nr_of_blocks;
3571 }
3572
3573
3582 {
3583 return part_st.block(s)->seqnr;
3584 }
3585
3586
3600 {
3601 // The labels have already been stored in
3602 // next_nontrivial_and_label.label by
3603 // refine_partition_until_it_becomes_stable().
3604
3605 // for all blocks
3607 s_iter(&part_st.permutation.front()); assert(s_iter <= &part_st.permutation.back());
3608 do
3609 {
3610 const bisim_dnj::block_t* const B(s_iter->st->bl.ock);
3611 // for all block_bunch-slices of the block
3612 for (const bisim_dnj::block_bunch_slice_t& block_bunch :
3614 { assert(block_bunch.is_stable()); assert(!block_bunch.empty());
3615 const bisim_dnj::pred_entry* const
3616 pred(block_bunch.end[-1].pred); assert(pred->source->bl.ock == B);
3617 assert(nullptr != pred->action_block->succ);
3618 /* add a transition from the source block to the goal block */ assert(pred->action_block->succ->block_bunch->pred == pred);
3619 /* with the indicated label. */ assert(pred->action_block->succ->block_bunch->slice == &block_bunch);
3620 label_type const
3621 label(block_bunch.bunch->next_nontrivial_and_label.label); assert(0 <= label); assert(label < action_label.size());
3622 aut.add_transition(transition(B->seqnr, label,
3623 pred->target->bl.ock->seqnr));
3624 }
3625 s_iter = B->end;
3626 }
3627 while (s_iter <= &part_st.permutation.back());
3628
3629 // Merge the states, by setting the state labels of each state to the
3630 // concatenation of the state labels of its equivalence class.
3631
3632 if (aut.has_state_info()) /* If there are no state labels
3633 this step can be ignored */
3634 {
3635 /* Create a vector for the new labels */
3637 new_labels(num_eq_classes());
3638
3639 state_type i(aut.num_states()); assert(0 < i);
3640 do
3641 {
3642 --i;
3643 const state_type new_index(get_eq_class(i));
3644 new_labels[new_index]=new_labels[new_index]+aut.state_label(i);
3645 }
3646 while (0 < i);
3647
3648 aut.set_num_states(num_eq_classes());
3649 i = 0; assert(i < num_eq_classes());
3650 do
3651 {
3652 aut.set_state_label(i, new_labels[i]);
3653 }
3654 while (++i < num_eq_classes());
3655 }
3656 else
3657 {
3658 aut.set_num_states(num_eq_classes());
3659 }
3660
3661 aut.set_initial_state(get_eq_class(aut.initial_state()));
3662 }
3663
3664
3669 bool in_same_class(state_type const s, state_type const t) const
3670 {
3671 return part_st.block(s) == part_st.block(t);
3672 }
3673 private:
3674
3675 /*--------------------------- main algorithm ----------------------------*/
3676
3700 {
3701 mCRL2log(log::verbose) << "An O(m log n) "
3703 ? "divergence-preserving branching "
3704 : "branching ")
3705 : "")
3706 << "bisimulation partitioner created for " << part_st.state_size()
3707 << " states and " << aut.num_transitions() << " transitions.\n";
3708
3709 if (part_st.state_size() > 2 * aut.num_transitions() + 1)
3710 {
3711 mCRL2log(log::warning) << "There are several isolated states "
3712 "without incoming or outgoing transition. It is not "
3713 "guaranteed that branching bisimulation minimisation runs in "
3714 "time O(m log n).\n";
3715 }
3716
3717 // create one block for all states
3719 #ifdef USE_POOL_ALLOCATOR
3720 part_tr.storage.template construct<bisim_dnj::block_t>
3721 #else
3723 #endif
3724 (&part_st.permutation.front(),
3725 1 + &part_st.permutation.back(), part_st.nr_of_blocks++));
3726
3727 // Iterate over the transitions to count how to order them in
3728 // part_trans_t
3729
3730 // counters for the non-inert outgoing and incoming transitions per
3731 // state are provided in part_st.state_info. These counters have been
3732 // initialised to zero in the constructor of part_state_t.
3733 // counters for the non-inert transition per label are stored in
3734 // action_label.
3735 assert(action_label.size() == aut.num_action_labels());
3736 // counter for the total number of inert transitions:
3737 trans_type inert_transitions(0);
3738 for (const transition& t: aut.get_transitions())
3739 {
3740 if (branching&&aut.is_tau(aut.apply_hidden_label_map(t.label()))&& ((
3741 t.from() != t.to()) || (assert(preserve_divergence), false)))
3742 {
3743 // The transition is inert.
3744 ++part_st.state_info[t.from()].succ_inert.count;
3745 ++inert_transitions;
3746
3747 // The source state should become non-bottom:
3748 if (part_st.state_info[t.from()].pos < B->nonbottom_begin)
3749 {
3750 std::swap(*part_st.state_info[t.from()].pos,
3751 *--B->nonbottom_begin);
3752 // we do not yet update the marked_bottom_begin pointer
3753 }
3754 }
3755 else
3756 {
3757 // The transition is non-inert. (It may be a self-loop).
3758 ++part_st.state_info[t.from()].untested_to_U_eqv.count;
3759 ++action_label[aut.apply_hidden_label_map(t.label())].count;
3760 }
3761 ++part_st.state_info[t.to()].pred_inert.count;
3762 }
3763 // Now we update the marked_bottom_begin pointer:
3765
3766 // set the pointers to transition slices in the state info entries
3767
3768 // We set them all to the end of the respective slice here. Then, with
3769 // every transition, the pointer will be reduced by one, so that after
3770 // placing all transitions it will point to the beginning of the slice.
3771
3772 bisim_dnj::pred_entry* next_pred_begin(&part_tr.pred.begin()[1]);
3773 bisim_dnj::succ_entry* next_succ_begin(&part_tr.succ.begin()[1]);
3774 bisim_dnj::state_info_entry* state_iter(&part_st.state_info.front()); assert(state_iter <= &part_st.state_info.back());
3775 do
3776 {
3777 state_iter->bl.ed_noninert_end = next_pred_begin;
3778 next_pred_begin += state_iter->pred_inert.count;
3779 state_iter->pred_inert.convert_to_iterator(next_pred_begin);
3780
3781 // create slice descriptors in part_tr.succ for each state with
3782 /* outgoing transitions. */ assert(nullptr != next_succ_begin);
3783 state_iter->untested_to_U_eqv.convert_to_iterator(
3784 next_succ_begin + state_iter->untested_to_U_eqv.count);
3785 if (next_succ_begin < state_iter->untested_to_U_eqv.begin)
3786 { assert(nullptr != state_iter->untested_to_U_eqv.begin);
3787 next_succ_begin->begin_or_before_end =
3788 state_iter->untested_to_U_eqv.begin - 1;
3789 for (bisim_dnj::succ_entry* const
3790 out_slice_begin(next_succ_begin);
3791 ++next_succ_begin < state_iter->untested_to_U_eqv.begin; )
3792 {
3793 next_succ_begin->begin_or_before_end = out_slice_begin; // mCRL2complexity(next_succ_begin->block_bunch->pred, ...) -- subsumed in the
3794 } // call below
3795
3796 B->mark(state_iter->pos);
3797 }
3798 state_iter->succ_inert.convert_to_iterator(next_succ_begin +
3799 state_iter->succ_inert.count);
3800 #ifndef NDEBUG
3801 while (next_succ_begin < state_iter->succ_inert.begin)
3802 { assert(nullptr == next_succ_begin->begin_or_before_end);
3803 ++next_succ_begin;
3804 }
3805 #endif
3806 next_succ_begin = state_iter->succ_inert.begin; // mCRL2complexity(*state_iter, ...) -- subsumed in the call at the end
3807 }
3808 while (++state_iter <= &part_st.state_info.back());
3809
3810 // Line 2.4: Pi_t := { { all non-inert transitions } }
3814 1 + &part_tr.block_bunch.back() - inert_transitions; assert(1 + &part_tr.block_bunch.front() <= part_tr.block_bunch_inert_begin);
3815 bisim_dnj::bunch_t* bunch(nullptr);
3816
3819 // create a single bunch containing all non-inert transitions
3820 bunch =
3821 #ifdef USE_POOL_ALLOCATOR
3822 part_tr.storage.template construct<bisim_dnj::bunch_t>
3823 #else
3825 #endif
3827 part_tr.action_block_inert_begin); assert(nullptr != bunch); assert(part_tr.splitter_list.empty());
3829
3830 // create a single block_bunch entry for all non-inert transitions
3833 part_tr.block_bunch_inert_begin, bunch, false); assert(!part_tr.splitter_list.empty());
3835 }
3836
3837 // create slice descriptors in part_tr.action_block for each label
3838
3839 // The action_block array shall have the tau transitions at the end:
3840 // first the non-inert tau transitions (during initialisation, that are
3841 // only the tau self-loops), then the tau transitions that have become
3842 // non-inert and finally the inert transitions.
3843 // Transitions with other labels are placed from beginning to end.
3844 // Every such transition block except the last one ends with a dummy
3845 /* entry. If there are transition labels without transitions, */ assert((size_t) (part_tr.action_block_end - part_tr.action_block_begin) ==
3846 /* multiple dummy entries will be placed side-by-side. */ aut.num_transitions() + action_label.size() - 1);
3848 next_action_label_begin(part_tr.action_block_begin);
3849 trans_type const n_square(part_st.state_size() * part_st.state_size()); ONLY_IF_DEBUG( trans_type max_transitions = n_square; )
3850 label_type label(action_label.size()); assert(0 < label);
3851 do
3852 {
3853 --label;
3854 if (0 < action_label[label].count)
3855 { assert(nullptr != bunch);
3857 {
3858 // This is the second action_block-slice, so the bunch is
3859 // not yet marked as nontrivial but it should be.
3860 part_tr.make_nontrivial(bunch);
3861 }
3862 if (n_square < action_label[label].count)
3863 {
3864 mCRL2log(log::warning) << "There are "
3865 << action_label[label].count << ' '
3866 << pp(aut.action_label(label)) << "-transitions. "
3867 "This is more than n^2 (= " << n_square << "). It is "
3868 "not guaranteed that branching bisimulation "
3869 "minimisation runs in time O(m log n).\n"; ONLY_IF_DEBUG( if (max_transitions < action_label[label].count)
3870 { max_transitions = action_label[label].count; } )
3871 }
3872 // initialise begin_or_before_end pointers for this
3873 // action_block-slice
3874 action_label[label].convert_to_iterator(
3875 next_action_label_begin + action_label[label].count);
3876 next_action_label_begin->begin_or_before_end =
3877 action_label[label].begin - 1; assert(nullptr != next_action_label_begin->begin_or_before_end);
3879 action_block_slice_begin(next_action_label_begin); assert(nullptr != action_block_slice_begin);
3880 while (++next_action_label_begin < action_label[label].begin)
3881 {
3882 next_action_label_begin->begin_or_before_end =
3883 action_block_slice_begin; // mCRL2complexity(next_action_label_begin->succ->block_bunch->pred, ...) --
3884 } // subsumed in the call at the end
3885 }
3886 else
3887 {
3888 action_label[label].convert_to_iterator(
3889 next_action_label_begin);
3890 if (0 != label && aut.num_transitions() < action_label.size())
3891 {
3892 mCRL2log(log::warning) << "Action label "
3893 << pp(aut.action_label(label)) << " has no "
3894 "transitions, and the number of action labels exceeds "
3895 "the number of transitions. It is not guaranteed that "
3896 "branching bisimulation minimisation runs in time "
3897 "O(m log n).\n";
3898 }
3899 }
3900 }
3901 while (0 < label && (/* insert a dummy entry */ assert(next_action_label_begin < part_tr.action_block_inert_begin),
3902 next_action_label_begin->succ = nullptr,
3903 next_action_label_begin->begin_or_before_end = nullptr,
3904 ++next_action_label_begin, true)); assert(next_action_label_begin == part_tr.action_block_inert_begin);
3905
3906 /* distribute the transitions over the data structures */ ONLY_IF_DEBUG( bisim_gjkw::check_complexity::init(2 * max_transitions); )
3907
3909 next_block_bunch(1 + &part_tr.block_bunch.front());
3910 for (const transition& t: aut.get_transitions())
3911 {
3913 source(&part_st.state_info.front() + t.from());
3915 target(&part_st.state_info.front() + t.to());
3916 bisim_dnj::succ_entry* succ_pos;
3917 bisim_dnj::block_bunch_entry* block_bunch_pos;
3918 bisim_dnj::pred_entry* pred_pos;
3919 bisim_dnj::action_block_entry* action_block_pos;
3920
3921 if (branching&&aut.is_tau(aut.apply_hidden_label_map(t.label()))&& ((
3922 t.from() != t.to()) || (assert(preserve_divergence), false)))
3923 {
3924 // It is a (normal) inert transition: place near the end of the
3925 // respective pred/succ slices, just before the other inert
3926 // transitions.
3927 succ_pos = --source->succ_inert.begin; assert(nullptr == succ_pos->begin_or_before_end);
3928 block_bunch_pos = 1 + &part_tr.block_bunch.back() -
3929 inert_transitions; assert(block_bunch_pos >= part_tr.block_bunch_inert_begin);
3930 pred_pos = --target->pred_inert.begin; assert(block_bunch_pos->slice.is_null());
3931 action_block_pos = part_tr.action_block_end-inert_transitions; assert(action_block_pos >= part_tr.action_block_inert_begin);
3932 action_block_pos->begin_or_before_end = nullptr;
3933 --inert_transitions;
3934 }
3935 else
3936 {
3937 // It is a non-inert transition (possibly a self-loop): place
3938 // at the end of the respective succ slice and at the beginning
3939 // of the respective pred slice.
3940 succ_pos =
3941 --part_st.state_info[t.from()].untested_to_U_eqv.begin; assert(nullptr != succ_pos->begin_or_before_end);
3942 assert(nullptr != succ_pos->begin_or_before_end->begin_or_before_end);
3943 assert(succ_pos->begin_or_before_end <= succ_pos ||
3944 succ_pos->begin_or_before_end->begin_or_before_end == succ_pos);
3945 block_bunch_pos = next_block_bunch++; assert(block_bunch_pos < part_tr.block_bunch_inert_begin);
3946 pred_pos = target->bl.ed_noninert_end++;
3947 action_block_pos =
3948 --action_label[aut.apply_hidden_label_map(t.label())].begin; assert(nullptr != action_block_pos->begin_or_before_end);
3949 assert(nullptr != action_block_pos->begin_or_before_end->begin_or_before_end);
3950 assert(action_block_pos->begin_or_before_end <= action_block_pos ||
3951 action_block_pos->begin_or_before_end->
3952 begin_or_before_end == action_block_pos);
3953 assert(!part_tr.splitter_list.empty());
3954 block_bunch_pos->slice = part_tr.splitter_list.begin(); assert(action_block_pos < part_tr.action_block_inert_begin);
3955 } assert(target->bl.ed_noninert_end <= target->pred_inert.begin);
3956 succ_pos->block_bunch = block_bunch_pos;
3957 block_bunch_pos->pred = pred_pos;
3958 pred_pos->action_block = action_block_pos;
3959 pred_pos->source = source;
3960 pred_pos->target = target; assert(nullptr != succ_pos);
3961 action_block_pos->succ = succ_pos; // mCRL2complexity(pred_pos, ...) -- subsumed in the call at the end
3962 } assert(0 == inert_transitions);
3963 /* delete transitions already -- they are no longer needed. We will */ assert(next_block_bunch == part_tr.block_bunch_inert_begin);
3964 // add new transitions at the end of minimisation.
3965 aut.clear_transitions();
3966
3967 state_iter = &part_st.state_info.front(); assert(state_iter <= &part_st.state_info.back());
3968 do
3969 {
3970 state_iter->bl.ock = B;
3971 }
3972 while (++state_iter <= &part_st.state_info.back());
3973
3974 if (nullptr != bunch)
3975 {
3976 while (nullptr == bunch->begin->succ)
3977 { assert(nullptr == bunch->begin->begin_or_before_end);
3978 ++bunch->begin; assert(bunch->begin < bunch->end);
3979 } assert(nullptr != bunch->begin->begin_or_before_end);
3980 while (nullptr == bunch->end[-1].succ)
3981 { assert(nullptr == bunch->end[-1].begin_or_before_end);
3982 --bunch->end; assert(bunch->begin < bunch->end);
3983 } assert(nullptr != bunch->end[-1].begin_or_before_end);
3984
3985 /* Line 2.2: B_vis := { s in S | there exists a visible */ mCRL2complexity(B, add_work(bisim_gjkw::check_complexity::
3986 /* transition that is reachable */ create_initial_partition, 1U), *this);
3987 // from s }
3988 // B_invis := S \ B_vis
3989 // Line 2.3: Pi_s := { B_vis, B_invis } \ { emptyset }
3990 // At this point, all states with a visible transition are
3991 // marked.
3992 if (0 < B->marked_size())
3994 part_tr.print_trans(*this); )
3997 if (1 < B->size())
3998 {
3999 B = split(B, /* splitter block_bunch */ slice,
4001 // We can ignore possible new non-inert transitions, as
4002 // every R-bottom state already has a transition in bunch.
4004 }
4005 else
4006 { assert(B->nonbottom_begin == B->end);
4007 /* A block with 1 state will not be split. However, we */ assert(B->marked_nonbottom_begin == B->end);
4008 // still have to make the splitter stable.
4010 part_tr.splitter_list, slice);
4011 slice->make_stable();
4012 } assert(!B->stable_block_bunch.empty()); assert(part_tr.splitter_list.empty());
4014 assert(1 + &part_tr.block_bunch.front() < B->stable_block_bunch.front().end);
4016 }
4017 } else assert(0 == B->marked_size());
4018 }
4019 #ifndef NDEBUG
4030 void assert_stability() const
4031 {
4033
4034 assert(part_tr.succ.size() == part_tr.block_bunch.size() + 1);
4035 assert(part_tr.pred.size() == part_tr.block_bunch.size() + 1);
4037 part_tr.block_bunch.size() + action_label.size() - 2);
4038 if (part_tr.block_bunch.empty()) return;
4039
4040 assert(part_tr.splitter_list.empty());
4041 /* for (const block_bunch_slice_t& block_bunch : part_tr.splitter_list)
4042 {
4043 assert(!block_bunch.is_stable());
4044 } */
4045
4046 trans_type true_nr_of_block_bunch_slices(0);
4047 // for all blocks
4049 perm_iter(&part_st.permutation.front());
4050 assert(perm_iter <= &part_st.permutation.back());
4051 do
4052 {
4053 const bisim_dnj::block_t* const block(perm_iter->st->bl.ock);
4054 unsigned const max_block(bisim_gjkw::check_complexity::log_n -
4056 // iterators have no predefined hash, so we store pointers:
4057 std::unordered_set<const bisim_dnj::block_bunch_slice_t*>
4058 block_bunch_check_set;
4059 #ifndef USE_SIMPLE_LIST
4060 block_bunch_check_set.reserve(
4061 block->stable_block_bunch.size());
4062 #endif
4063
4064 // for all stable block_bunch-slices of the block
4065 for (const bisim_dnj::block_bunch_slice_t& block_bunch :
4066 block->stable_block_bunch)
4067 {
4068 assert(block_bunch.source_block() == block);
4069 assert(block_bunch.is_stable());
4070 block_bunch_check_set.insert(&block_bunch);
4071 mCRL2complexity(&block_bunch, no_temporary_work(
4072 block_bunch.bunch->max_work_counter(*this)), *this);
4073 ++true_nr_of_block_bunch_slices;
4074 }
4075
4076 // for all states in the block
4077 do
4078 {
4079 trans_type block_bunch_count(0);
4080 const bisim_dnj::state_info_entry* const state(perm_iter->st);
4081 assert(state!=part_tr.succ.front().block_bunch->pred->source);
4082 // for all out-slices of the state
4083 for (const bisim_dnj::succ_entry*
4084 out_slice_end(state->succ_inert.begin);
4085 state == out_slice_end[-1].block_bunch->pred->source; )
4086 { assert(!out_slice_end[-1].block_bunch->slice.is_null());
4088 block_bunch_slice(out_slice_end[-1].block_bunch->slice);
4089 const bisim_dnj::bunch_t* const bunch(
4090 block_bunch_slice->bunch);
4091 assert(block == block_bunch_slice->source_block());
4092 if (block_bunch_slice->is_stable())
4093 {
4094 assert(1 == block_bunch_check_set.count(
4095 &*block_bunch_slice));
4096 ++block_bunch_count;
4097 }
4098 else assert(0); // i. e. all block_bunch-slices should
4099 // be stable
4100 const bisim_dnj::succ_entry* const out_slice_begin(
4101 out_slice_end[-1].begin_or_before_end);
4102 assert(nullptr != out_slice_begin);
4103 assert(out_slice_begin < out_slice_end);
4104 assert(nullptr != out_slice_begin->begin_or_before_end);
4105 assert(out_slice_begin->begin_or_before_end + 1 ==
4106 out_slice_end);
4107
4108 // for all transitions in the out-slice
4109 do
4110 {
4111 --out_slice_end;
4112 assert(bunch->begin <=
4113 out_slice_end->block_bunch->pred->action_block);
4114 assert(out_slice_end->block_bunch->pred->
4115 action_block < bunch->end);
4116 assert(out_slice_end->block_bunch->slice ==
4117 block_bunch_slice);
4118 assert(nullptr != out_slice_end->begin_or_before_end);
4119 if (out_slice_end->block_bunch + 1 !=
4120 block_bunch_slice->end)
4121 {
4122 assert(out_slice_end->block_bunch + 1 <
4123 block_bunch_slice->end);
4124 assert(out_slice_end->block_bunch[1].slice ==
4125 block_bunch_slice);
4126 }
4127 mCRL2complexity(out_slice_end->block_bunch->pred,
4128 no_temporary_work(max_block, bisim_gjkw::
4129 check_complexity::log_n - bisim_gjkw::
4130 check_complexity::ilog2(out_slice_end->
4131 block_bunch->pred->target->bl.ock->size()),
4132 perm_iter < block->nonbottom_begin),*this);
4133 }
4134 while (out_slice_begin < out_slice_end &&
4135 (assert(out_slice_begin ==
4136 out_slice_end->begin_or_before_end), true));
4137 }
4138 if (perm_iter < block->nonbottom_begin)
4139 {
4140 assert(block_bunch_check_set.size() == block_bunch_count);
4141 }
4142 }
4143 while (++perm_iter < block->end);
4144 }
4145 while (perm_iter <= &part_st.permutation.back());
4147 true_nr_of_block_bunch_slices);
4150 if (branching)
4153 1 + &part_tr.block_bunch.back());
4154 assert(1 + &part_tr.block_bunch.back() -
4157
4158 // for all inert transitions
4159 for (const bisim_dnj::action_block_entry* action_block(
4161 action_block < part_tr.action_block_end;
4162 ++action_block)
4163 { assert(nullptr == action_block->begin_or_before_end);
4164 const bisim_dnj::succ_entry* const
4165 succ_iter(action_block->succ);
4166 assert(nullptr != succ_iter);
4167 assert(succ_iter->block_bunch->slice.is_null());
4168 const bisim_dnj::pred_entry* const
4169 pred_iter(succ_iter->block_bunch->pred);
4170 assert(action_block == pred_iter->action_block);
4172 succ_iter->block_bunch);
4173 assert(pred_iter->source != pred_iter->target);
4174 assert(pred_iter->source->bl.ock == pred_iter->target->bl.ock);
4175 assert(pred_iter->source->succ_inert.begin <= succ_iter);
4176 assert(pred_iter->source->succ_inert.begin == succ_iter ||
4177 succ_iter[-1].block_bunch->pred->source==pred_iter->source);
4178 assert(pred_iter->target->pred_inert.begin <= pred_iter);
4179 assert(pred_iter->target->pred_inert.begin == pred_iter ||
4180 pred_iter[-1].target == pred_iter->target);
4181 unsigned const max_block(bisim_gjkw::check_complexity::log_n -
4183 pred_iter->target->bl.ock->size()));
4184 mCRL2complexity(pred_iter, no_temporary_work(max_block,
4185 max_block, false), *this);
4186 }
4187 }
4188 else
4189 {
4190 assert(!preserve_divergence);
4193 1 + &part_tr.block_bunch.back());
4194 }
4196 action_slice_end(part_tr.action_block_inert_begin);
4197 trans_type true_nr_of_bunches(0);
4198 trans_type true_nr_of_nontrivial_bunches(0);
4199 trans_type true_nr_of_action_block_slices(0);
4200 // for all action labels and bunches
4201 label_type label(0);
4202 assert(label < action_label.size());
4203 const bisim_dnj::bunch_t* previous_bunch(nullptr);
4204 do
4205 {
4206 assert(part_tr.action_block_begin <= action_label[label].begin);
4207 assert(action_label[label].begin <= action_slice_end);
4208 assert(action_slice_end <= part_tr.action_block_inert_begin);
4209 // for all action_block slices
4211 action_block_slice_end(action_slice_end);
4212 action_label[label].begin < action_block_slice_end; )
4213 {
4215 action_block_slice_begin(
4216 action_block_slice_end[-1].begin_or_before_end);
4217 assert(nullptr != action_block_slice_begin);
4218 assert(action_block_slice_begin < action_block_slice_end);
4219 assert(action_block_slice_end <= action_slice_end);
4220 assert(nullptr != action_block_slice_begin->succ);
4221 const bisim_dnj::block_t* const
4222 target_block(action_block_slice_begin->
4223 succ->block_bunch->pred->target->bl.ock);
4224 const bisim_dnj::bunch_t* const
4225 bunch(action_block_slice_begin->succ->bunch());
4226 if (previous_bunch != bunch)
4227 {
4228 assert(nullptr == previous_bunch);
4229 previous_bunch = bunch;
4230 assert(bunch->end == action_block_slice_end);
4231 if (bunch->begin == action_block_slice_begin)
4232 {
4233 // Perhaps this does not always hold; sometimes, an
4234 // action_block slice disappears but the bunch cannot
4235 // be made trivial.
4236 assert(bunch->is_trivial());
4237 }
4238 else
4239 {
4240 assert(!bunch->is_trivial());
4241 ++true_nr_of_nontrivial_bunches;
4242 }
4243 mCRL2complexity(bunch, no_temporary_work(
4244 bunch->max_work_counter(*this)), *this);
4245 ++true_nr_of_bunches;
4246 }
4247 if(bunch->begin == action_block_slice_begin)
4248 {
4249 previous_bunch = nullptr;
4250 }
4251 else assert(bunch->begin < action_block_slice_begin);
4252
4253 assert(action_block_slice_begin->begin_or_before_end + 1 ==
4254 action_block_slice_end);
4255 // for all transitions in the action_block slice
4257 action_block(action_block_slice_end);
4258 do
4259 {
4260 --action_block;
4261 const bisim_dnj::succ_entry* const
4262 succ_iter(action_block->succ);
4263 assert(nullptr != succ_iter);
4264 const bisim_dnj::pred_entry* const
4265 pred_iter(succ_iter->block_bunch->pred);
4266 assert(action_block == pred_iter->action_block);
4267 assert(succ_iter->block_bunch <
4269 assert(!branching || !aut.is_tau(label) ||
4270 pred_iter->source->bl.ock!=pred_iter->target->bl.ock ||
4272 pred_iter->source == pred_iter->target));
4273 assert(succ_iter < pred_iter->source->succ_inert.begin);
4274 assert(succ_iter+1==pred_iter->source->succ_inert.begin ||
4275 succ_iter[1].block_bunch->pred->source ==
4276 pred_iter->source);
4277 assert(pred_iter < pred_iter->target->pred_inert.begin);
4278 assert(pred_iter+1==pred_iter->target->pred_inert.begin ||
4279 pred_iter[1].target == pred_iter->target);
4280 assert(target_block == pred_iter->target->bl.ock);
4281 assert(bunch == succ_iter->bunch());
4282 }
4283 while (action_block_slice_begin < action_block &&
4284 (// some properties only need to be checked for states that
4285 // are not the first one:
4286 assert(action_block->begin_or_before_end ==
4287 action_block_slice_begin), true));
4288 action_block_slice_end = action_block_slice_begin;
4289 ++true_nr_of_action_block_slices;
4290 }
4291 if (action_slice_end < part_tr.action_block_inert_begin)
4292 {
4293 // there is a dummy transition between action labels
4294 assert(nullptr == action_slice_end->succ);
4295 assert(nullptr == action_slice_end->begin_or_before_end);
4296 }
4297 }
4298 while (++label < action_label.size() &&
4299 (action_slice_end = action_label[label - 1].begin - 1, true));
4300 assert(nullptr == previous_bunch);
4301 assert(part_tr.nr_of_bunches == true_nr_of_bunches);
4303 true_nr_of_nontrivial_bunches);
4305 true_nr_of_action_block_slices);
4306 }
4307 #endif
4326 {
4327 // Line 2.5: for all non-trivial bunches bunch_T in Pi_t do
4328 clock_t next_print_time = clock();
4329 const clock_t rounded_start_time = next_print_time - CLOCKS_PER_SEC/2;
4330 // const double log_initial_nr_of_action_block_slices =
4331 // 100 / std::log(part_tr.nr_of_action_block_slices);
4332 for (;;)
4333 { // mCRL2complexity(...) -- this loop will be ascribed to (the transitions in)
4334 // the new bunch below.
4335 /*------------------ find a non-trivial bunch -------------------*/ ONLY_IF_DEBUG( part_st.print_part(*this); part_tr.print_trans(*this);
4336 assert_stability(); )
4337 /* 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 <=
4338 /* |bunch_T_a_Bprime| <= 1/2 |bunch_T| */ part_tr.nr_of_action_block_slices);
4339 bisim_dnj::bunch_t* const bunch_T(