Line data Source code
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 :
11 : /// \file lts/detail/liblts_bisim_dnj.h
12 : ///
13 : /// \brief O(m log n)-time branching bisimulation algorithm
14 : ///
15 : /// \details This file implements an efficient partition refinement algorithm
16 : /// for labelled transition systems inspired by Groote / Jansen / Keiren / Wijs
17 : /// (2017) and Valmari (2009) to calculate the branching bisimulation classes
18 : /// of a labelled transition system. Different from the 2017 article, it does
19 : /// not translate the LTS to a Kripke structure, but works on the LTS directly.
20 : /// In this way the memory use can be reduced. The algorithm is described in
21 : /// the conference publication
22 : ///
23 : /// David N. Jansen, Jan Friso Groote, Jeroen J.A. Keiren, Anton Wijs:
24 : /// An O(m log n) algorithm for branching bisimilarity on labelled transition
25 : /// systems. In: Armin Biere, David Parker (Eds.): Tools and Algorithms for the
26 : /// Construction and Analysis of Systems: TACAS. (LNCS 12070). Springer: Cham,
27 : /// 2020. pp 3-20. https://doi.org/10.1007/978-3-030-45237-7_1
28 : ///
29 : /// Partition refinement means that the algorithm maintains a partition of the
30 : /// state space of the LTS into ``blocks''. A block contains all states in one
31 : /// or several branching bisimulation equivalence classes. Blocks are being
32 : /// refined until every block contains exactly one branching bisimulation
33 : /// equivalence class.
34 : ///
35 : /// The algorithm divides the non-inert transitions into *action_block-slices.*
36 : /// An action_block-slice contains all transitions with a given action label
37 : /// into one block. One or more action_block-slices are joined into a *bunch.*
38 : /// Bunches register which blocks have already been stabilised:
39 : ///
40 : /// > Invariant: The blocks are stable under the bunches, i. e. if a block
41 : /// > has a transition in a bunch, then every bottom state in this block has
42 : /// > a transition in this bunch.
43 : ///
44 : /// However, if a bunch is non-trivial (i. e., it contains more than one
45 : /// action_block-slice), its slices may split some blocks into finer parts:
46 : /// not all states may have a transition in the same action_block-slice. So, a
47 : /// refinement step consists of moving one small action_block-slice from a
48 : /// non-trivial bunch to a new bunch and then splitting blocks to restore the
49 : /// Invariant. Splitting is always done by finding a small subblock and moving
50 : /// the states in that subblock to a new block. Note that we always handle a
51 : /// small part of some larger unit; that ensures that each state and transition
52 : /// is only touched O(log n) times.
53 : ///
54 : /// After splitting blocks, some inert transitions may have become non-inert.
55 : /// These transitions mostly need to be inserted into their own bunch. Also,
56 : /// some states may have lost all their inert transitions and become new bottom
57 : /// states. These states need to be handled as well to re-establish the
58 : /// Invariant.
59 : ///
60 : /// Overall, we spend time as follows:
61 : /// - Every transition is moved to a new bunch at most
62 : /// log<SUB>2</SUB>(2 * n<SUP>2</SUP>) = 2*log<SUB>2</SUB>(n) + 1 times.
63 : /// Every move leads to O(1) work.
64 : /// - Every state is moved to a new block at most log<SUB>2</SUB>(n) times.
65 : /// Every move leads to work proportional to the number of its incoming and
66 : /// outgoing transitions.
67 : /// - Every state becomes a new bottom state at most once. When this happens,
68 : /// this leads to work proportional to the number of its outgoing
69 : /// transitions.
70 : /// When summing this up over all states and transitions, we get that the
71 : /// algorithm spends time in O(m log n), where m is the number of transitions
72 : /// and n ist the number of states.
73 : ///
74 : /// \author David N. Jansen, Institute of Software, Chinese Academy of
75 : /// Sciences, Beijing, PR China
76 :
77 : // The file is best viewed on a screen or in a window that is 160 characters
78 : // wide. The left 80 columns contain the main text of the program. The right
79 : // 80 columns contain assertions and other code used for debugging.
80 :
81 : #ifndef LIBLTS_BISIM_DNJ_H
82 : #define LIBLTS_BISIM_DNJ_H
83 :
84 : #include "mcrl2/lts/detail/liblts_scc.h"
85 : #include "mcrl2/lts/detail/liblts_merge.h"
86 : #include "mcrl2/lts/detail/coroutine.h"
87 : #include "mcrl2/lts/detail/check_complexity.h"
88 : #include "mcrl2/lts/detail/fixed_vector.h"
89 :
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 :
121 : namespace mcrl2
122 : {
123 : namespace lts
124 : {
125 : namespace detail
126 : {
127 : #ifndef NDEBUG
128 : /// \brief include something in Debug mode
129 : /// \details In a few places, we have to include an additional parameter to
130 : /// a function in Debug mode. While it is in principle possible to use
131 : /// #ifndef NDEBUG ... #endif, that would lead to distributing the code
132 : /// over many code lines. This macro expands to its arguments in Debug
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
138 : /// \brief type used to store label numbers and counts
139 : typedef std::size_t label_type;
140 :
141 : template <class LTS_TYPE> class bisim_partitioner_dnj;
142 :
143 : namespace bisim_dnj
144 : {
145 :
146 : /// \class iterator_or_counter
147 : /// \brief union: either iterator or counter (for initialisation)
148 : /// \details During initialisation, we need some counters to count the number
149 : /// of transitions for each state. To avoid allocating separate memory for
150 : /// these counters, we store their value in the same place where we later
151 : /// store an iterator.
152 : ///
153 : /// We assume that each such variable starts out as a counter and at
154 : /// some point becomes an iterator. That point is marked by calling
155 : /// convert_to_iterator(). The structure may only be destroyed after that
156 : /// call, as the destructor assumes it's an iterator.
157 : template <class Iterator>
158 : union iterator_or_counter
159 : {
160 : /// \brief counter (used during initialisation)
161 : trans_type count;
162 :
163 : /// \brief iterator (used during main part of the algorithm)
164 : Iterator begin;
165 :
166 : /// \brief Construct the object as a counter
167 8238 : iterator_or_counter() { count = 0; }
168 :
169 :
170 : /// \brief Convert the object from counter to iterator
171 8238 : void convert_to_iterator(const Iterator other)
172 : {
173 8238 : new (&begin) Iterator(other);
174 8238 : }
175 :
176 :
177 : /// \brief Destruct the object as an iterator
178 106925 : ~iterator_or_counter() { begin.~Iterator(); }
179 : };
180 :
181 :
182 : class block_bunch_entry;
183 : class 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
200 : /// \class pool
201 : /// \brief a pool allocator class
202 : /// \details This class allocates a large chunk of memory at once and hands
203 : /// out smaller parts. It is supposed to be more efficient than calling
204 : /// new/delete, in particular because it assumes that T is trivially
205 : /// destructible, so it won't call destructors. It allows to store
206 : /// elements of different sizes.
207 : ///
208 : /// Internally, it keeps a (single-linked) list of large chunks of size
209 : /// BLOCKSIZE. Each chunk contains a data area; for all chunks except the
210 : /// first one, this area is completely in use.
211 : ///
212 : /// There is a free list, a (single-linked) list of elements in the chunks
213 : /// that have been freed. However, all elements in the free list have to
214 : /// have the same size as type T.
215 : template <class T, size_t BLOCKSIZE = 1000>
216 : class my_pool
217 : { static_assert(std::is_trivially_destructible<T>::value);
218 : private: static_assert(sizeof(void*) <= sizeof(T));
219 : class pool_block_t
220 : {
221 : public:
222 : char data[BLOCKSIZE - sizeof(pool_block_t*)];
223 : pool_block_t* next_block;
224 :
225 469 : pool_block_t(pool_block_t* const new_next_block)
226 469 : : next_block(new_next_block)
227 469 : { }
228 : }; static_assert(sizeof(T) <= sizeof(pool_block_t::data));
229 :
230 : /// \brief first chunk in list of chunks
231 : /// \details All chunks except the first one are completely in use.
232 : pool_block_t* first_block;
233 :
234 : /// \brief start of part in the first chunk that is already in use
235 : void* begin_used_in_first_block;
236 :
237 : /// \brief first freed element
238 : void* first_free_T;
239 :
240 651 : static void*& deref_void(void* addr)
241 : {
242 651 : return *static_cast<void**>(addr);
243 : }
244 : public:
245 : /// \brief constructor
246 333 : my_pool()
247 333 : : first_block(new pool_block_t(nullptr)),
248 333 : begin_used_in_first_block(
249 333 : &first_block->data[sizeof(first_block->data)]),
250 333 : first_free_T(nullptr)
251 333 : { }
252 :
253 :
254 : /// \brief destructor
255 333 : ~my_pool()
256 : {
257 333 : pool_block_t* block(first_block); assert(nullptr != block);
258 : do
259 : {
260 469 : pool_block_t* next_block = block->next_block;
261 469 : delete block;
262 469 : block = next_block;
263 : }
264 469 : while(nullptr != block);
265 333 : }
266 :
267 :
268 : private:
269 : /// \brief allocate and construct a new element of the same size as the
270 : /// free list
271 : template <class U, class... Args>
272 2833 : U* construct_samesize(Args&&... args)
273 : { static_assert(sizeof(T) == sizeof(U));
274 2833 : void* new_el; assert(nullptr != first_block);
275 2833 : if (first_block->data + sizeof(U) <= begin_used_in_first_block)
276 : {
277 2754 : begin_used_in_first_block =
278 2754 : new_el = static_cast<char*>(begin_used_in_first_block) -
279 : sizeof(U);
280 : }
281 79 : 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 63 : new_el = first_free_T;
286 63 : first_free_T = deref_void(new_el);
287 : }
288 : else
289 : {
290 16 : first_block = new pool_block_t(first_block);
291 16 : begin_used_in_first_block =
292 16 : new_el = &first_block->data[sizeof(first_block->data) -
293 : sizeof(U)];
294 : }
295 2833 : return new(new_el) U(std::forward<Args>(args)...);
296 : }
297 :
298 :
299 : /// \brief allocate and construct a new element of a size that doesn't
300 : /// fit the free list
301 : template <class U, class... Args>
302 3364 : U* construct_othersize(Args&&... args)
303 : { static_assert(sizeof(U) != sizeof(T));
304 3364 : void* new_el; assert(nullptr != first_block);
305 3364 : if (first_block->data + sizeof(U) <= begin_used_in_first_block)
306 : {
307 3244 : begin_used_in_first_block =
308 3244 : 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) <=
317 : begin_used_in_first_block)
318 : {
319 : begin_used_in_first_block = static_cast<char*>
320 : (begin_used_in_first_block) - sizeof(T);
321 : deref_void(begin_used_in_first_block) = first_free_T;
322 : first_free_T = begin_used_in_first_block;
323 : }
324 : }
325 : else if constexpr (sizeof(T) < sizeof(U))
326 : {
327 : // There may be space for one T-element (but not more)
328 63 : if (first_block->data + sizeof(T) <=
329 63 : begin_used_in_first_block)
330 : {
331 7 : begin_used_in_first_block = static_cast<char*>
332 7 : (begin_used_in_first_block) - sizeof(T);
333 7 : deref_void(begin_used_in_first_block) = first_free_T;
334 7 : first_free_T = begin_used_in_first_block;
335 : }
336 120 : } assert(first_block->data + sizeof(T) > begin_used_in_first_block);
337 120 : first_block = new pool_block_t(first_block);
338 120 : begin_used_in_first_block =
339 120 : new_el = &first_block->data[sizeof(first_block->data) -
340 : sizeof(U)];
341 : }
342 3364 : return new(new_el) U(std::forward<Args>(args)...);
343 : }
344 : public:
345 : /// \brief allocate and construct a new element (of any type)
346 : template <class U, class... Args>
347 6197 : U* construct(Args&&... args)
348 : { static_assert(std::is_trivially_destructible<U>::value);
349 : if constexpr (sizeof(U) == sizeof(T))
350 : {
351 2833 : return construct_samesize<U>(std::forward<Args>(args)...);
352 : }
353 : else
354 : { static_assert(sizeof(U) <= sizeof(first_block->data));
355 3364 : return construct_othersize<U>(std::forward<Args>(args)...);
356 : }
357 : }
358 :
359 :
360 : /// \brief destroy and delete some element
361 : /// \details destroy() is only allowed if the destructor of U is
362 : /// trivial. This ensures that in my_pool::~my_pool() we do not have
363 : /// to test whether some element has been freed before we destroy it.
364 : /// Also, the size of U has to be the same size as the size of T, so
365 : /// each entry in the free list has the same size.
366 : template <class U>
367 581 : void destroy(U* const old_el)
368 : { static_assert(sizeof(T) == sizeof(U));
369 581 : 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 1716 : for (const pool_block_t* block(first_block);
374 1135 : assert(nullptr != block),
375 2072 : total_order(old_el, block->data) ||
376 937 : total_order(&block->data[sizeof(block->data)], old_el + 1);
377 554 : block = block->next_block )
378 : { }
379 : #endif
380 581 : deref_void(old_el) = first_free_T;
381 581 : first_free_T = static_cast<void*>(old_el);
382 581 : }
383 : };
384 : #endif
385 :
386 : #ifdef USE_SIMPLE_LIST
387 : /// \class simple_list
388 : /// \brief a simple implementation of lists
389 : /// \details This class simplifies lists: It assumes that list entries are
390 : /// trivially destructible, and it does not store the size of a list.
391 : /// Therefore, the destructor, erase() and splice() can be simplified.
392 : /// Also, the simple_list object itself is trivially destructible if the
393 : /// pool allocator is used; therefore, destroying a block_t object becomes
394 : /// trivial as well.
395 : template <class T>
396 : class simple_list
397 : {
398 : private:
399 : /// \brief empty entry, used for the sentinel
400 : class empty_entry
401 : {
402 : protected:
403 : /// \brief pointer to the next element in the list
404 : empty_entry* next;
405 :
406 : /// \brief pointer to the previous element in the list
407 : empty_entry* prev;
408 :
409 4660 : empty_entry(empty_entry*const new_next, empty_entry*const new_prev)
410 4660 : : next(new_next),
411 4660 : prev(new_prev)
412 4660 : { }
413 :
414 : friend class simple_list;
415 : };
416 :
417 : /// \brief sentinel, i.e. element that provides pointers to the
418 : /// beginning and the end of the list
419 : empty_entry sentinel;
420 :
421 : public:
422 : /// \brief list entry
423 : /// \details If the list is to use the pool allocator, its designated
424 : /// type must be `simple_list::entry` so elements can be erased.
425 : class entry : public empty_entry
426 : {
427 : private:
428 : T data;
429 :
430 : friend class simple_list;
431 : public:
432 : template <class... Args>
433 2833 : entry(empty_entry* const new_next, empty_entry* const new_prev,
434 : Args&&... args)
435 : : empty_entry(new_next, new_prev),
436 2833 : data(std::forward<Args>(args)...)
437 2833 : { }
438 : };
439 :
440 : /// \brief constant iterator class for simple_list
441 : class const_iterator
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:
450 : empty_entry* ptr;
451 :
452 43831 : const_iterator(const empty_entry* const new_ptr)
453 43831 : : ptr(const_cast<empty_entry*>(new_ptr))
454 43831 : { }
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 22489 : const_iterator& operator++() { ptr = ptr->next; return *this; }
462 0 : const_iterator& operator--() { ptr = ptr->prev; return *this; }
463 55620 : const T& operator*() const
464 : {
465 55620 : return static_cast<const entry*>(ptr)->data;
466 : }
467 238632 : const T* operator->() const
468 : {
469 238632 : return &static_cast<const entry*>(ptr)->data;
470 : }
471 37307 : bool operator==(const const_iterator& other) const
472 : {
473 37307 : return ptr == other.ptr;
474 : }
475 37245 : bool operator!=(const const_iterator& other) const
476 : {
477 37245 : return !operator==(other);
478 : }
479 : };
480 :
481 : /// \brief iterator class for simple_list
482 : class iterator : public const_iterator
483 : {
484 : public:
485 : typedef typename const_iterator::iterator_category
486 : iterator_category;
487 : typedef typename const_iterator::value_type value_type;
488 : typedef typename const_iterator::difference_type difference_type;
489 : typedef typename const_iterator::pointer pointer;
490 : typedef typename const_iterator::reference reference;
491 : protected:
492 15631 : 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;
499 303 : iterator& operator++(){const_iterator::operator++(); return *this;}
500 0 : iterator& operator--(){const_iterator::operator--(); return *this;}
501 2258 : T& operator*() const
502 : {
503 2258 : return static_cast<entry*>(const_iterator::ptr)->data;
504 : }
505 143403 : T* operator->() const
506 : {
507 143403 : return &static_cast<entry*>(const_iterator::ptr)->data;
508 : }
509 : };
510 :
511 : /// \brief class that stores either an iterator or a null value
512 : /// \details We cannot use C++14's ``null forward iterators'', as they
513 : /// are not guaranteed to compare unequal to valid iterators. We also
514 : /// need to compare null iterators with non-null ones.
515 : class iterator_or_null : public iterator
516 : {
517 : public:
518 : typedef typename iterator::iterator_category iterator_category;
519 : typedef typename iterator::value_type value_type;
520 : typedef typename iterator::difference_type difference_type;
521 : typedef typename iterator::pointer pointer;
522 : typedef typename iterator::reference reference;
523 3690 : iterator_or_null() : iterator() { }
524 1424 : iterator_or_null(std::nullptr_t) : iterator()
525 : {
526 1424 : const_iterator::ptr = nullptr;
527 1424 : }
528 7138 : iterator_or_null(const iterator& other) : iterator(other) { }
529 127121 : bool is_null() const { return nullptr == const_iterator::ptr; }
530 : T& operator*() const
531 : { assert(!is_null());
532 : return iterator::operator*();
533 : }
534 78396 : T* operator->() const
535 78396 : { assert(!is_null());
536 78396 : return iterator::operator->();
537 : }
538 68812 : bool operator==(const const_iterator& other) const
539 : {
540 68812 : return const_iterator::ptr == other.ptr;
541 : }
542 76 : bool operator!=(const const_iterator& other) const
543 : {
544 76 : return !operator==(other);
545 : }
546 74457 : bool operator==(const T* const other) const
547 74457 : { assert(nullptr != other);
548 : // It is allowed to call this even if is_null(). Therefore, we
549 : // cannot use iterator_or_null::operator->().
550 74457 : return const_iterator::operator->() == other;
551 : }
552 71759 : bool operator!=(const T* const other) const
553 : {
554 71759 : return !operator==(other);
555 : }
556 :
557 1748 : void operator=(std::nullptr_t)
558 : {
559 1748 : const_iterator::ptr = nullptr;
560 1748 : }
561 : };
562 :
563 : /// \brief constructor
564 1827 : simple_list()
565 1827 : : sentinel(&sentinel, &sentinel)
566 : { static_assert(std::is_trivially_destructible<entry>::value);
567 1827 : }
568 :
569 : #ifndef USE_POOL_ALLOCATOR
570 : /// \brief destructor
571 : ~simple_list()
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 :
582 : /// \brief return an iterator to the first element of the list
583 6340 : iterator begin() { return iterator(sentinel.next); }
584 :
585 : /// \brief return an iterator past the last element of the list
586 6458 : iterator end() { return iterator(&sentinel); }
587 :
588 : /// \brief return a constant iterator to the first element of the list
589 13808 : const_iterator cbegin() const { return const_iterator(sentinel.next); }
590 :
591 : /// \brief return a constant iterator past the last element of the list
592 14392 : const_iterator cend() const { return const_iterator(&sentinel); }
593 :
594 : /// \brief return a constant iterator to the first element of the list
595 12987 : const_iterator begin() const { return cbegin(); }
596 :
597 : /// \brief return a constant iterator past the last element of the list
598 12987 : const_iterator end() const { return cend(); }
599 :
600 : /// \brief return a reference to the first element of the list
601 2643 : T& front()
602 2643 : { assert(!empty());
603 2643 : return static_cast<entry*>(sentinel.next)->data;
604 : }
605 :
606 : /// \brief return a reference to the last element of the list
607 : T& back()
608 : { assert(!empty());
609 : return static_cast<entry*>(sentinel.prev)->data;
610 : }
611 :
612 : /// \brief return true iff the list is empty
613 12810 : bool empty() const { return sentinel.next == &sentinel; }
614 :
615 : /// \brief construct a new list entry before pos
616 : template<class... Args>
617 : static iterator emplace(
618 : ONLY_IF_POOL_ALLOCATOR( my_pool<entry>& pool, )
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 :
633 : /// \brief construct a new list entry after pos
634 : template<class... Args>
635 612 : static iterator emplace_after(
636 : ONLY_IF_POOL_ALLOCATOR( my_pool<entry>& pool, )
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 612 : (pos.ptr->next, pos.ptr, std::forward<Args>(args)...));
646 612 : pos.ptr->next->prev = new_entry;
647 612 : pos.ptr->next = new_entry;
648 612 : return iterator(new_entry);
649 : }
650 :
651 : /// \brief construct a new list entry at the beginning
652 : template<class... Args>
653 533 : iterator emplace_front(
654 : ONLY_IF_POOL_ALLOCATOR( my_pool<entry>& pool, )
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 533 : (sentinel.next, &sentinel, std::forward<Args>(args)...));
664 533 : sentinel.next->prev = new_entry;
665 533 : sentinel.next = new_entry;
666 533 : return iterator(new_entry);
667 : }
668 :
669 : /// \brief construct a new list entry at the end
670 : template<class... Args>
671 1688 : iterator emplace_back(
672 : ONLY_IF_POOL_ALLOCATOR( my_pool<entry>& pool, )
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 1688 : (&sentinel, sentinel.prev, std::forward<Args>(args)...));
682 1688 : sentinel.prev->next = new_entry;
683 1688 : sentinel.prev = new_entry;
684 1688 : return iterator(new_entry);
685 : }
686 :
687 : /// \brief move a list entry from one position to another (possibly in
688 : /// a different list)
689 5817 : static void splice(iterator const new_pos, simple_list& /* unused */,
690 : iterator const old_pos)
691 : {
692 5817 : old_pos.ptr->prev->next = old_pos.ptr->next;
693 5817 : old_pos.ptr->next->prev = old_pos.ptr->prev;
694 :
695 5817 : old_pos.ptr->next = new_pos.ptr->prev->next;
696 5817 : old_pos.ptr->prev = new_pos.ptr->prev;
697 :
698 5817 : old_pos.ptr->prev->next = old_pos.ptr;
699 5817 : old_pos.ptr->next->prev = old_pos.ptr;
700 5817 : }
701 :
702 : /// \brief erase an element from a list
703 581 : static void erase(
704 : ONLY_IF_POOL_ALLOCATOR( my_pool<entry>& pool, )
705 : iterator const pos)
706 : {
707 581 : pos.ptr->prev->next = pos.ptr->next;
708 581 : pos.ptr->next->prev = pos.ptr->prev;
709 : #ifdef USE_POOL_ALLOCATOR
710 581 : pool.destroy(static_cast<entry*>(pos.ptr));
711 : #else
712 : delete static_cast<entry*>(pos.ptr);
713 : #endif
714 581 : }
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 :
734 : /// \defgroup part_state
735 : /// \brief data structures for states
736 : /// \details States are stored in a refinable partition data structure. The
737 : /// actual state information will not be moved around, but only entries in
738 : /// a separate permutation array. Entries is this array are grouped per
739 : /// block, so that the states in a block can be described as a slice in the
740 : /// permutation array.
741 : ///@{
742 : class state_info_entry;
743 : class permutation_entry;
744 :
745 : /// \class permutation_t
746 : /// \brief stores a permutation of the states, ordered by block
747 : /// \details This is the central concept of the _refinable partition_: the
748 : /// permutation of the states, such that states belonging to the same block are
749 : /// adjacent.
750 : ///
751 : /// Iterating over the states of a block will
752 : /// therefore be done using the permutation_t array.
753 : typedef bisim_gjkw::fixed_vector<permutation_entry> permutation_t;
754 :
755 : class block_t;
756 : class bunch_t;
757 :
758 : class pred_entry;
759 : class succ_entry;
760 :
761 : class block_bunch_slice_t;
762 : typedef simple_list<block_bunch_slice_t>::iterator block_bunch_slice_iter_t;
763 : typedef simple_list<block_bunch_slice_t>::const_iterator
764 : block_bunch_slice_const_iter_t;
765 : #ifdef USE_SIMPLE_LIST
766 : typedef simple_list<block_bunch_slice_t>::iterator_or_null
767 : block_bunch_slice_iter_or_null_t;
768 : #else
769 : union block_bunch_slice_iter_or_null_t
770 : {
771 : private:
772 : const void* null;
773 : block_bunch_slice_iter_t iter;
774 : public:
775 : /// \brief Construct an uninitialized object
776 : block_bunch_slice_iter_or_null_t()
777 : {
778 : if constexpr (!std::is_trivially_destructible<
779 : block_bunch_slice_iter_t>::value)
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 :
788 : /// \brief Construct an object containing a null pointer
789 : explicit block_bunch_slice_iter_or_null_t(nullptr_t)
790 : {
791 : null = nullptr;
792 : }
793 :
794 :
795 : /// \brief Construct an object containing a valid iterator
796 : explicit block_bunch_slice_iter_or_null_t(
797 : const block_bunch_slice_iter_t& other)
798 : {
799 : new (&iter) block_bunch_slice_iter_t(other); assert(nullptr != null);
800 : }
801 :
802 :
803 : /// \brief Destruct an object (whether it contains a valid iterator or
804 : // not)
805 : ~block_bunch_slice_iter_or_null_t()
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 :
844 : /// \brief Compare the object with another iterator_or_null object
845 : /// \details The operator is templated so that iterator_or_null objects of
846 : /// different types can be compared.
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 :
861 : /// \brief Compare the object with another iterator_or_null object
862 : bool operator!=(const block_bunch_slice_iter_or_null_t& other) const
863 : {
864 : return !operator==(other);
865 : }
866 :
867 :
868 : /// \brief Compare the object with an iterator
869 : /// \details If the object does not contain a valid iterator, it
870 : /// compares unequal with the iterator.
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 :
884 : /// \brief Compare the object with a non-null pointer
885 : /// \details If the object does not contain a valid iterator, it
886 : /// compares unequal with the pointer.
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 :
900 : /// \brief Check whether the object contains a valid iterator
901 : bool is_null() const { return nullptr == null; }
902 : };
903 : #endif
904 :
905 : enum new_block_mode_t { new_block_is_U, new_block_is_R };
906 :
907 :
908 : /// \class state_info_entry
909 : /// \brief stores information about a single state
910 : /// \details This class stores all other information about a state that the
911 : /// partition needs. In particular: the block where the state belongs and the
912 : /// position in the permutation array (i. e. the inverse of the permutation).
913 : class state_info_entry
914 : {
915 : public:
916 : /// \brief iterator to first inert incoming transition
917 : /// \details Non-inert incoming transitions of the state are stored just
918 : /// before the element where this iterator points to.
919 : ///
920 : /// During initialisation, this field also doubles up as a counter for
921 : /// the number of incoming transitions, and as the pointer to the first
922 : /// incoming inert transition that already has been initialised.
923 : iterator_or_counter<pred_entry*> pred_inert;
924 :
925 : /// \brief iterator to first inert outgoing transition
926 : /// \details Non-inert outgoing transitions of the state are stored just
927 : /// before the element where this iterator points to.
928 : ///
929 : /// During initialisation, this field also doubles up as a counter for the
930 : /// number of *inert* outgoing transitions, and as the pointer to the first
931 : /// outgoing inert transition that already has been initialised.
932 : iterator_or_counter<succ_entry*> succ_inert;
933 :
934 : /// \brief block where the state belongs
935 : /// \details During initialisation, this field is used to point at the
936 : /// first unused slot of the (non-inert) bledecessors, ahem, predecessors.
937 : /// Sorry for the mock-chinese ``typo''. So we always assume that it
938 : /// starts as a pred_entry*, at some moment is converted to a block_t*, and
939 : /// then stays that way until it is destroyed.
940 : union bl_t {
941 : pred_entry* ed_noninert_end;
942 : block_t* ock;
943 : } bl;
944 :
945 : /// \brief position of the state in the permutation array
946 : permutation_entry* pos;
947 :
948 : /// \brief number of inert transitions to non-U-states
949 : /// \details Actually, as we cannot easily count how many inert outgoing
950 : /// transitions this state has, we initialize this pointer to
951 : /// succ_inert.begin. Every time we find an outgoing transition to a
952 : /// U-state, we increase this iterator; as soon as it no longer points to
953 : /// an outgoing transition of this state, we have found all inert outgoing
954 : /// transitions. This requires that after the inert outgoing transitions
955 : /// there is a transition that starts in another state, or there is a dummy
956 : /// transition.
957 : ///
958 : /// During initialisation, this field also doubles up as a counter for the
959 : /// number of *non-inert* outgoing transitions, and as the pointer to the
960 : /// first outgoing transition that already has been initialised. Therefore
961 : /// it cannot be a `const succ_entry*`.
962 : iterator_or_counter<succ_entry*> untested_to_U_eqv;
963 : #ifndef NDEBUG
964 : /// \brief print a short state identification for debugging
965 : template<class LTS_TYPE>
966 0 : std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
967 : partitioner) const
968 0 : { assert(&partitioner.part_st.state_info.front() <= this);
969 0 : assert(this <= &partitioner.part_st.state_info.back());
970 0 : return std::to_string(this - &partitioner.part_st.state_info.front());
971 : }
972 :
973 : /// \brief print a state identification for debugging
974 : template<class LTS_TYPE>
975 0 : std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>&
976 : partitioner) const
977 : {
978 0 : return "state " + debug_id_short(partitioner);
979 : }
980 :
981 : mutable bisim_gjkw::check_complexity::state_dnj_counter_t work_counter;
982 : #endif
983 : };
984 :
985 :
986 : /// \brief entry in the permutation array
987 : class permutation_entry {
988 : public:
989 : /// \brief pointer to the state information data structure
990 : state_info_entry* st;
991 :
992 :
993 : /// \brief default constructor (should not be deleted)
994 : permutation_entry() = default;
995 :
996 :
997 : /// \brief move constructor
998 : /// \details The move constructor is called when a temporary object is
999 : /// created; in that case, it is not necessary to set the pos pointer.
1000 5946 : permutation_entry(const permutation_entry&& other) noexcept
1001 5946 : {
1002 5946 : st = other.st;
1003 5946 : }
1004 :
1005 :
1006 : /// \brief move assignment operator
1007 : /// \details The move assignment operator is called when an object is moved
1008 : /// to its final place. Therefore, we have to adapt the pos pointer. Note
1009 : /// that std::swap also uses move assignment, so we automatically get the
1010 : /// correct behaviour there.
1011 11934 : void operator=(const permutation_entry&& other) noexcept
1012 : {
1013 11934 : st = other.st;
1014 11934 : st->pos = this;
1015 11934 : }
1016 : };
1017 :
1018 :
1019 : /// \class block_t
1020 : /// \brief stores information about a block
1021 : /// \details A block corresponds to a slice of the permutation array. As the
1022 : /// number of blocks is initially unknown, we will allocate instances of this
1023 : /// class dynamically.
1024 : ///
1025 : /// The slice in the permutation array containing the states of the block is
1026 : /// subdivided into the following subslices (in this order):
1027 : /// 1. unmarked bottom states
1028 : /// 2. marked bottom states (initially empty)
1029 : /// 3. unmarked non-bottom states
1030 : /// 4. marked non-bottom states (initially empty)
1031 : ///
1032 : /// A state should be marked iff it is a predecessor of the current splitter
1033 : /// (through a strong transition). The marking is later extended to the
1034 : /// R-states; that are the states with a weak transition to the splitter.
1035 : ///
1036 : /// (During the execution of some functions, blocks are subdivided further;
1037 : /// however, as these subdivisions are local to a single function, they are not
1038 : /// stored here.)
1039 : ///
1040 : /// Note that block_t uses the default destructor; therefore, if simple_list is
1041 : /// trivially destructible, so is block_t.
1042 : class block_t
1043 : {
1044 : public:
1045 : /// \brief iterator to the first state of the block
1046 : permutation_entry* begin;
1047 :
1048 : /// \brief iterator to the first marked bottom state of the block
1049 : permutation_entry* marked_bottom_begin;
1050 :
1051 : /// \brief iterator to the first non-bottom state of the block
1052 : permutation_entry* nonbottom_begin;
1053 :
1054 : /// \brief iterator to the first marked non-bottom state of the block
1055 : permutation_entry* marked_nonbottom_begin;
1056 :
1057 : /// \brief iterator past the last state of the block
1058 : permutation_entry* end;
1059 :
1060 : /// \brief list of stable block_bunch-slices with transitions from this
1061 : /// block
1062 : simple_list<block_bunch_slice_t> stable_block_bunch;
1063 :
1064 : /// \brief unique sequence number of this block
1065 : /// \details After the stuttering equivalence algorithm has terminated,
1066 : /// this number is used as a state number in the quotient LTS.
1067 : const state_type seqnr;
1068 :
1069 :
1070 : /// \brief constructor
1071 : /// \details The constructor initialises the block to: all states are
1072 : /// bottom states, no state is marked.
1073 : /// \param new_begin initial iterator to the first state of the block
1074 : /// \param new_end initial iterator past the last state of the block
1075 : /// \param new_seqnr is the sequence number of the new block
1076 1494 : block_t(permutation_entry* const new_begin,
1077 : permutation_entry* const new_end, state_type const new_seqnr)
1078 1494 : : begin(new_begin),
1079 1494 : marked_bottom_begin(new_end),
1080 1494 : nonbottom_begin(new_end),
1081 1494 : marked_nonbottom_begin(new_end),
1082 1494 : end(new_end),
1083 1494 : stable_block_bunch(),
1084 1494 : seqnr(new_seqnr)
1085 1494 : { assert(new_begin < new_end);
1086 1494 : }
1087 :
1088 :
1089 : /// \brief provides the number of states in the block
1090 81943 : state_type size() const
1091 81943 : { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1092 81943 : assert(marked_bottom_begin <= nonbottom_begin);
1093 81943 : assert(nonbottom_begin <= marked_nonbottom_begin);
1094 81943 : return end - begin;
1095 : }
1096 :
1097 :
1098 : /// \brief provides the number of bottom states in the block
1099 313 : state_type bottom_size() const
1100 313 : { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1101 313 : assert(marked_bottom_begin <= nonbottom_begin);
1102 313 : assert(nonbottom_begin <= marked_nonbottom_begin);
1103 313 : return nonbottom_begin - begin;
1104 : }
1105 :
1106 :
1107 : /// \brief provides the number of marked bottom states in the block
1108 14719 : state_type marked_bottom_size() const
1109 14719 : { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1110 14719 : assert(marked_bottom_begin <= nonbottom_begin);
1111 14719 : assert(nonbottom_begin <= marked_nonbottom_begin);
1112 14719 : return nonbottom_begin - marked_bottom_begin;
1113 : }
1114 :
1115 :
1116 : /// \brief provides the number of marked states in the block
1117 13525 : state_type marked_size() const
1118 : {
1119 13525 : return end - marked_nonbottom_begin + marked_bottom_size();
1120 : }
1121 :
1122 :
1123 : /// \brief provides the number of unmarked bottom states in the block
1124 4278 : state_type unmarked_bottom_size() const
1125 4278 : { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1126 4278 : assert(marked_bottom_begin <= nonbottom_begin);
1127 4278 : assert(nonbottom_begin <= marked_nonbottom_begin);
1128 4278 : return marked_bottom_begin - begin;
1129 : }
1130 :
1131 :
1132 : /// \brief provides the number of unmarked nonbottom states in the block
1133 2322 : state_type unmarked_nonbottom_size() const
1134 2322 : { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1135 2322 : assert(marked_bottom_begin <= nonbottom_begin);
1136 2322 : assert(nonbottom_begin <= marked_nonbottom_begin);
1137 2322 : return marked_nonbottom_begin - nonbottom_begin;
1138 : }
1139 :
1140 :
1141 : /// \brief mark a non-bottom state
1142 : /// \details Marking is done by moving the state to the slice of the marked
1143 : /// non-bottom states of the block.
1144 : /// \param s the non-bottom state that has to be marked
1145 : /// \returns true iff the state was not marked before
1146 772 : bool mark_nonbottom(permutation_entry* const s)
1147 772 : { assert(nonbottom_begin <= s); assert(s < end);
1148 : // assert(this == s->st->bl.ock); -- does not hold during initialisation
1149 772 : assert(begin <= marked_bottom_begin);
1150 772 : assert(marked_bottom_begin <= nonbottom_begin);
1151 772 : assert(nonbottom_begin <= marked_nonbottom_begin);
1152 772 : if (marked_nonbottom_begin <= s) { return false; } assert(marked_nonbottom_begin <= end);
1153 690 : std::swap(*s, *--marked_nonbottom_begin); assert(nonbottom_begin <= marked_nonbottom_begin);
1154 690 : return true;
1155 : }
1156 :
1157 :
1158 : /// \brief mark a state
1159 : /// \details Marking is done by moving the state to the slice of the marked
1160 : /// bottom or non-bottom states of the block.
1161 : /// \param s the state that has to be marked
1162 : /// \returns true iff the state was not marked before
1163 4122 : bool mark(permutation_entry* const s)
1164 4122 : { assert(begin <= s);
1165 4122 : if (s < nonbottom_begin) // assert(this == s->st->bl.ock); -- does not hold during initialisation
1166 3901 : { assert(begin <= marked_bottom_begin); assert(marked_nonbottom_begin <= end);
1167 3901 : assert(nonbottom_begin <= marked_nonbottom_begin);
1168 3901 : if (marked_bottom_begin <= s) { return false; } assert(marked_bottom_begin <= nonbottom_begin);
1169 3832 : std::swap(*s, *--marked_bottom_begin); assert(begin <= marked_bottom_begin);
1170 3832 : return true;
1171 : }
1172 221 : return mark_nonbottom(s);
1173 : }
1174 :
1175 :
1176 : /// \brief refine a block
1177 : /// \details This function is called after a refinement function has found
1178 : /// where to split the block into unmarked (U) and marked (R) states.
1179 : /// It creates a new block for the smaller subblock.
1180 : /// \param new_block_mode indicates whether the U- or the R-block
1181 : /// should be the new one. (This parameter is necessary in case
1182 : /// the two halves have exactly the same size.)
1183 : /// \param new_seqnr is the sequence number of the new block
1184 : /// \param new_block (if the pool allocator is used) a pointer to an
1185 : /// uninitialized block, where the new block will be stored.
1186 : /// \returns pointer to the new block
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, )
1189 : ONLY_IF_POOL_ALLOCATOR(
1190 : my_pool<simple_list<block_bunch_slice_t>::entry>& storage, )
1191 : state_type new_seqnr);
1192 : #ifndef NDEBUG
1193 : /// \brief print a block identification for debugging
1194 : template<class LTS_TYPE>
1195 0 : inline std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>&
1196 : partitioner) const
1197 0 : { assert(&partitioner.part_st.permutation.front() <= begin);
1198 0 : assert(begin < end); assert(begin <= marked_bottom_begin);
1199 0 : assert(marked_bottom_begin <= nonbottom_begin);
1200 0 : assert(nonbottom_begin <= marked_nonbottom_begin);
1201 0 : assert(marked_nonbottom_begin <= end);
1202 0 : assert(end <= 1 + &partitioner.part_st.permutation.back());
1203 : return "block [" +
1204 0 : std::to_string(begin - &partitioner.part_st.permutation.front()) +
1205 0 : "," + std::to_string(end-&partitioner.part_st.permutation.front()) +
1206 0 : ") (#" + std::to_string(seqnr) + ")";
1207 : }
1208 :
1209 : mutable bisim_gjkw::check_complexity::block_dnj_counter_t work_counter;
1210 : #endif
1211 : };
1212 :
1213 :
1214 : /// \class part_state_t
1215 : /// \brief refinable partition data structure
1216 : /// \details This class collects all information about a partition of the
1217 : /// states.
1218 : class part_state_t
1219 : {
1220 : public:
1221 : /// \brief permutation array
1222 : /// \details This is the central element of the data structure: In this
1223 : /// array, states that belong to the same block are stored in adjacent
1224 : /// elements.
1225 : permutation_t permutation;
1226 :
1227 : /// \brief array with all other information about states
1228 : bisim_gjkw::fixed_vector<state_info_entry> state_info;
1229 :
1230 : /// \brief total number of blocks with unique sequence number allocated
1231 : /// \details Upon starting the stuttering equivalence algorithm, the number
1232 : /// of blocks must be zero.
1233 : state_type nr_of_blocks;
1234 :
1235 : /// \brief constructor
1236 : /// \details The constructor allocates memory and makes the permutation and
1237 : /// state_info arrays consistent with each other, but does not actually
1238 : /// initialise the partition. Immediately afterwards, the initialisation
1239 : /// will be done in `bisim_partitioner_dnj::create_initial_partition()`.
1240 : /// \param num_states number of states in the LTS
1241 333 : part_state_t(state_type const num_states)
1242 333 : : permutation(num_states),
1243 333 : state_info(num_states),
1244 333 : nr_of_blocks(0)
1245 333 : { assert(0 < num_states);
1246 333 : permutation_entry* perm_iter(&permutation.front()); ONLY_IF_POOL_ALLOCATOR(
1247 : static_assert(std::is_trivially_destructible<block_t>::value); )
1248 333 : state_info_entry* state_iter(&state_info.front()); assert(perm_iter <= &permutation.back());
1249 : do
1250 : {
1251 2318 : state_iter->pos = perm_iter;
1252 2318 : perm_iter->st = state_iter;
1253 : }
1254 2318 : while (++state_iter, ++perm_iter <= &permutation.back()); assert(state_iter == 1 + &state_info.back());
1255 333 : }
1256 :
1257 :
1258 : #ifndef USE_POOL_ALLOCATOR
1259 : /// \brief destructor
1260 : /// \details The destructor also deallocates the blocks, as they are
1261 : /// not directly referenced from anywhere. This is only necessary if
1262 : /// we do not use the pool allocator, as the latter will destroy the
1263 : /// blocks wholesale.
1264 : ~part_state_t()
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 :
1278 : /// \brief calculate the size of the state space
1279 : /// \returns the number of states in the LTS
1280 999 : state_type state_size() const { return permutation.size(); }
1281 :
1282 :
1283 : /// \brief find the block of a state
1284 : /// \param s number of the state
1285 : /// \returns a pointer to the block where state s resides in
1286 1637 : const block_t* block(state_type const s) const
1287 : {
1288 1637 : return state_info[s].bl.ock;
1289 : }
1290 : #ifndef NDEBUG
1291 : private:
1292 : /// \brief print a slice of the partition (typically a block)
1293 : /// \details If the slice indicated by the parameters is not empty, the
1294 : /// message and the states in this slice will be printed.
1295 : /// \param message text printed as a title if the slice is not empty
1296 : /// \param begin_print iterator to the beginning of the slice
1297 : /// \param end_print iterator past the end of the slice
1298 : /// \param partitioner LTS partitioner (used to print more details)
1299 : template<class LTS_TYPE>
1300 0 : 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 0 : { assert(B->begin <= begin_print); assert(end_print <= B->end);
1306 0 : if (end_print == begin_print) return;
1307 :
1308 0 : mCRL2log(log::debug) << '\t' << message
1309 0 : << (1 < end_print - begin_print ? "s:\n" : ":\n");
1310 0 : assert(begin_print < end_print);
1311 : do
1312 : {
1313 0 : mCRL2log(log::debug) << "\t\t"
1314 0 : << begin_print->st->debug_id(partitioner);
1315 0 : if (B != begin_print->st->bl.ock)
1316 : {
1317 0 : mCRL2log(log::debug) << ", inconsistent: points "
1318 0 : "to " << begin_print->st->bl.ock->debug_id(partitioner);
1319 : }
1320 0 : if (begin_print != begin_print->st->pos)
1321 : {
1322 0 : mCRL2log(log::debug)
1323 0 : << ", inconsistent pointer to state_info_entry";
1324 : }
1325 0 : mCRL2log(log::debug) << '\n';
1326 : }
1327 0 : while (++begin_print < end_print);
1328 : }
1329 : public:
1330 : /// \brief print the partition per block
1331 : /// \details The function prints all blocks in order. For each block, it
1332 : /// lists its states, separated into nonbottom and bottom states.
1333 : /// \param partitioner LTS partitioner (used to print more details)
1334 : template<class LTS_TYPE>
1335 2088 : void print_part(const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
1336 : {
1337 2088 : if (!mCRL2logEnabled(log::debug)) return;
1338 0 : const block_t* B(permutation.front().st->bl.ock);
1339 : do
1340 : {
1341 0 : mCRL2log(log::debug)<<B->debug_id(partitioner)<<":\n";
1342 0 : print_block(B, "Bottom state",
1343 0 : B->begin, B->marked_bottom_begin, partitioner);
1344 0 : print_block(B, "Marked bottom state",
1345 0 : B->marked_bottom_begin, B->nonbottom_begin, partitioner);
1346 0 : print_block(B, "Non-bottom state",
1347 0 : B->nonbottom_begin, B->marked_nonbottom_begin, partitioner);
1348 0 : print_block(B, "Marked non-bottom state",
1349 0 : B->marked_nonbottom_begin, B->end, partitioner);
1350 : // go to next block
1351 : }
1352 0 : while(B->end <= &permutation.back() && (B = B->end->st->bl.ock, true));
1353 : }
1354 :
1355 : /// \brief asserts that the partition of states is consistent
1356 : /// \details It also requires that no states are marked.
1357 : /// \param partitioner LTS partitioner (used to print more details)
1358 : template<class LTS_TYPE>
1359 1757 : void assert_consistency(
1360 : const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
1361 : {
1362 1757 : const permutation_entry* perm_iter(&permutation.front());
1363 1757 : state_type true_nr_of_blocks(0);
1364 1757 : assert(perm_iter <= &permutation.back());
1365 : do
1366 : {
1367 11537 : const block_t* const block(perm_iter->st->bl.ock);
1368 : // block is consistent:
1369 11537 : assert(block->begin == perm_iter);
1370 11537 : assert(block->begin < block->marked_bottom_begin);
1371 11537 : assert(block->marked_bottom_begin == block->nonbottom_begin);
1372 11537 : assert(block->nonbottom_begin <= block->marked_nonbottom_begin);
1373 11537 : assert(block->marked_nonbottom_begin == block->end);
1374 11537 : assert(partitioner.branching||block->nonbottom_begin==block->end);
1375 : assert(0 <= block->seqnr);
1376 11537 : assert(block->seqnr < nr_of_blocks);
1377 23074 : unsigned const max_block(bisim_gjkw::check_complexity::log_n -
1378 11537 : bisim_gjkw::check_complexity::ilog2(block->size()));
1379 11537 : mCRL2complexity(block, no_temporary_work(max_block), partitioner);
1380 :
1381 : // states in the block are consistent:
1382 : do
1383 : {
1384 25711 : const state_info_entry* const state(perm_iter->st);
1385 : // assert(&part_tr.pred.front() < state->pred_inert.begin);
1386 25711 : 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 25711 : if (perm_iter < block->nonbottom_begin)
1391 : {
1392 22191 : 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 22191 : 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 3520 : 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 3520 : mCRL2complexity(state, no_temporary_work(max_block, false),
1408 : partitioner);
1409 : }
1410 25711 : assert(block == state->bl.ock);
1411 25711 : assert(perm_iter == state->pos);
1412 : }
1413 25711 : while (++perm_iter < block->end);
1414 11537 : assert(perm_iter == block->end);
1415 11537 : ++true_nr_of_blocks;
1416 : }
1417 11537 : while (perm_iter <= &permutation.back());
1418 1757 : assert(nr_of_blocks == true_nr_of_blocks);
1419 1757 : }
1420 : #endif
1421 : };
1422 :
1423 : ///@} (end of group part_state)
1424 :
1425 :
1426 :
1427 :
1428 : #ifndef NDEBUG
1429 : /* ************************************************************************* */ static struct {
1430 98687 : /* */ 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 98687 : /* ************************************************************************* */ return p1.begin > action_block;
1434 : }
1435 : } const action_label_greater;
1436 : #endif
1437 :
1438 :
1439 : /// \defgroup part_trans
1440 : /// \brief data structures for transitions used during partition refinement
1441 : /// \details These definitions provide a partition for transition data
1442 : /// structure that can be used for the partition refinement algorithm.
1443 : ///
1444 : /// Basically, transitions are stored in four arrays:
1445 : /// - `pred`: transitions grouped by goal state, to allow finding all
1446 : /// predecessors of a goal state.
1447 : /// (At the beginning and the end of the pred array, there are dummy
1448 : /// entries.)
1449 : /// - `succ`: transitions grouped by source state and bunch, to allow finding
1450 : /// all successors of a source state. Given a transition in this array, it
1451 : /// is easy to find all transitions from the same source state in the same
1452 : /// bunch.
1453 : /// (At the beginning and the end of the succ array, there are dummy
1454 : /// entries.)
1455 : /// - `action_block`: a permutation of the transitions such that transitions
1456 : /// in the same bunch are adjacent, and within each bunch transitions with
1457 : /// the same action label and target block.
1458 : /// (Between two action_block-slices with different actions, there is a dummy
1459 : /// entry.)
1460 : /// - `block_bunch`: a permutation of the transitions such that transitions
1461 : /// from the same block in the same bunch are adjacent.
1462 : /// (At the beginning of the block_bunch array, there is a dummy entry.)
1463 : /// Entries in these four arrays are linked with each other with circular
1464 : /// iterators, so that one can find the corresponding entry in another array.
1465 : ///
1466 : /// Within this sort order, inert transitions are always placed after non-inert
1467 : /// transitions.
1468 : ///
1469 : /// state_info_entry and block_t (defined above) contain pointers to the slices
1470 : /// of these arrays. For bunches and block_bunch-slices, we additionally
1471 : /// create _descriptors_ that hold some information about the slice.
1472 :
1473 : ///@{
1474 :
1475 : /// \brief information about a transition sorted per source state
1476 : class succ_entry
1477 : {
1478 : public:
1479 : /// \brief circular iterator to link the four transition arrays
1480 : block_bunch_entry* block_bunch;
1481 :
1482 : /// \brief pointer to delimit the slice of transitions in the same bunch
1483 : /// \details For most transitions, this pointer points to the first
1484 : /// transition that starts in the same state and belongs to the same
1485 : /// bunch. But if this transition is the first such transition, the
1486 : /// pointer points to the last such transition (not one past the last, like
1487 : /// otherwise in C and C++).
1488 : ///
1489 : /// For inert transitions, the value is nullptr.
1490 : succ_entry* begin_or_before_end;
1491 :
1492 :
1493 : /// \brief find the beginning of the out-slice
1494 : succ_entry* out_slice_begin( ONLY_IF_DEBUG( const bisim_gjkw::fixed_vector<succ_entry>& succ )
1495 : );
1496 :
1497 :
1498 : /// \brief find the bunch of the transition
1499 : bunch_t* bunch() const;
1500 : #ifndef NDEBUG
1501 : /// \brief assign work to the transitions in an out-slice (i.e. the
1502 : /// transitions from one state in a specific bunch)
1503 : /// \details This debugging function is called to account for work that
1504 : /// could be assigned to any transition in the out-slice. Just to make
1505 : /// sure, we therefore set the corresponding counter `ctr` for every
1506 : /// transition in the out-slice to `max_value`.
1507 : /// \param partitioner LTS partitioner
1508 : /// \param out_slice_begin pointer to the first transition in the
1509 : /// out-slice
1510 : /// \param ctr type of the counter that work is assigned to
1511 : /// \param max_value new value that the counter should get
1512 : template <class LTS_TYPE>
1513 : static inline void add_work_to_out_slice(
1514 : const bisim_partitioner_dnj<LTS_TYPE>& partitioner,
1515 : const succ_entry* out_slice_begin, enum bisim_gjkw::check_complexity::
1516 : counter_type ctr, unsigned max_value);
1517 : #endif
1518 : };
1519 :
1520 :
1521 : /// \brief information about a transition grouped per (source block, bunch)
1522 : /// pair
1523 : class block_bunch_entry
1524 : {
1525 : public:
1526 : /// \brief circular iterator to link the four transition arrays
1527 : pred_entry* pred;
1528 :
1529 : /// \brief block_bunch-slice of which this transition is part
1530 : /// \details The slice is null iff the transition is inert.
1531 : block_bunch_slice_iter_or_null_t slice;
1532 : };
1533 :
1534 :
1535 : /// \brief information about a transition sorted per target state
1536 : /// \details As I expect the transitions in this array to be moved least often,
1537 : /// I store the information on source and target state in this entry. (It
1538 : /// could be stored in any of the four arrays describing the transition;
1539 : /// through the circular iterators, the information would be available anyway.)
1540 : class pred_entry
1541 : {
1542 : public:
1543 : /// \brief circular iterator to link the four transition arrays
1544 : action_block_entry* action_block;
1545 :
1546 : /// \brief source state of the transition
1547 : state_info_entry* source;
1548 :
1549 : /// \brief target state of the transition
1550 : state_info_entry* target;
1551 : #ifndef NDEBUG
1552 : /// \brief print a short transition identification for debugging
1553 : template <class LTS_TYPE>
1554 0 : std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
1555 : partitioner) const
1556 : {
1557 0 : return "from " + source->debug_id_short(partitioner) +
1558 0 : " to " + target->debug_id_short(partitioner);
1559 : }
1560 :
1561 : /// \brief print a transition identification for debugging
1562 : template <class LTS_TYPE>
1563 0 : 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 0 : label_type const label(std::lower_bound(
1568 : partitioner.action_label.cbegin(), partitioner.action_label.cend(),
1569 0 : action_block, action_label_greater) -
1570 0 : partitioner.action_label.cbegin());
1571 0 : assert(label < partitioner.action_label.size());
1572 0 : assert(partitioner.action_label[label].begin <= action_block);
1573 0 : 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 0 : return pp(partitioner.aut.action_label(label)) + "-transition " +
1577 0 : debug_id_short(partitioner);
1578 : }
1579 :
1580 : mutable bisim_gjkw::check_complexity::trans_dnj_counter_t work_counter;
1581 : #endif
1582 : };
1583 :
1584 :
1585 : /// \brief information about a transition sorted per (action, target block)
1586 : /// pair
1587 : class action_block_entry
1588 : {
1589 : public:
1590 : /// \brief circular iterator to link the four transition arrays
1591 : /// \details This iterator can be nullptr because we need to insert dummy
1592 : /// elements between two action_block-slices during initialisation, to make
1593 : /// it easier for first_move_transition_to_new_action_block() to detect
1594 : /// whether two action_block-slices belong to the same action or not.
1595 : succ_entry* succ;
1596 :
1597 : /// \brief pointer to delimit the slice of transitions in the same (action,
1598 : /// block) pair
1599 : /// \details For most transitions, this pointer points to the first
1600 : /// transition that has the same action and goes to the same block. But if
1601 : /// this transition is the first such transition, the pointer points to the
1602 : /// last such transition (not one past the last, like otherwise in C and
1603 : /// C++).
1604 : ///
1605 : /// For inert transitions and dummy entries, the value is nullptr.
1606 : action_block_entry* begin_or_before_end;
1607 :
1608 :
1609 : /// \brief find the beginning of the action_block-slice
1610 2481 : action_block_entry* action_block_slice_begin( ONLY_IF_DEBUG( const action_block_entry* const action_block_begin,
1611 : const action_block_entry* const action_block_orig_inert_begin )
1612 : )
1613 : {
1614 2481 : action_block_entry* result(begin_or_before_end); assert(nullptr != result);
1615 2481 : if (this < result)
1616 488 : { assert(this == result->begin_or_before_end);
1617 488 : 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 2481 : assert(nullptr != succ); assert(nullptr != result->succ);
1623 2481 : assert(succ->bunch() == result->succ->bunch());
1624 2481 : 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 2481 : return result;
1630 : }
1631 : };
1632 :
1633 :
1634 : class part_trans_t;
1635 :
1636 : /// \brief bunch of transitions
1637 : /// \details Like a slice, at the end of the algorithm there will be a bunch
1638 : /// for every transition in the bisimulation quotient. Therefore, we should
1639 : /// try to minimize the size of a bunch as much as possible.
1640 : class bunch_t
1641 : {
1642 : public:
1643 : /// \brief first transition in the bunch
1644 : action_block_entry* begin;
1645 :
1646 : /// \brief pointer past the last transition in the bunch
1647 : action_block_entry* end;
1648 :
1649 : /// \brief pointer to next non-trivial bunch (in the single-linked list) or
1650 : /// label
1651 : /// \details During refinement, this field stores a pointer to the next
1652 : /// nontrivial bunch. After refinement, it is set to the label.
1653 : union next_nontrivial_and_label_t
1654 : {
1655 : /// \brief pointer to the next non-trivial bunch in the single-linked
1656 : /// list
1657 : /// \details This pointer is == nullptr if the bunch is trivial. The
1658 : /// last entry in the list points to itself so its pointer is still
1659 : /// != nullptr.
1660 : bunch_t* next_nontrivial;
1661 :
1662 : /// \brief action label of the transition
1663 : label_type label;
1664 :
1665 :
1666 : /// \brief constructor
1667 1870 : next_nontrivial_and_label_t()
1668 1870 : {
1669 1870 : next_nontrivial = nullptr;
1670 1870 : }
1671 : } next_nontrivial_and_label;
1672 :
1673 :
1674 : /// \brief constructor
1675 1870 : bunch_t(action_block_entry* const new_begin,
1676 : action_block_entry* const new_end)
1677 1870 : : begin(new_begin),
1678 1870 : end(new_end),
1679 1870 : next_nontrivial_and_label()
1680 1870 : { }
1681 :
1682 :
1683 : /// \brief returns true iff the bunch is trivial
1684 : /// \details If this bunch is the last in the list of non-trivial bunches,
1685 : /// the convention is that the next pointer points to this bunch itself (to
1686 : /// distinguish it from nullptr).
1687 17742 : bool is_trivial() const
1688 : {
1689 17742 : return nullptr == next_nontrivial_and_label.next_nontrivial;
1690 : }
1691 :
1692 :
1693 : /// \brief split off a single action_block-slice from the bunch
1694 : /// \details The function splits the current bunch after its first
1695 : /// action_block-slice or before its last action_block-slice, whichever
1696 : /// is smaller. It creates a new bunch for the split-off slice and
1697 : /// returns a pointer to the new bunch. The caller has to adapt the
1698 : /// block_bunch-slices.
1699 : bunch_t* split_off_small_action_block_slice(part_trans_t& part_tr);
1700 : #ifndef NDEBUG
1701 : /// \brief print a short bunch identification for debugging
1702 : template <class LTS_TYPE>
1703 0 : std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE>&
1704 : partitioner) const
1705 : {
1706 0 : assert(partitioner.part_tr.action_block_begin <= begin);
1707 0 : assert(end <= partitioner.part_tr.action_block_inert_begin);
1708 0 : return "bunch [" + std::to_string(begin -
1709 0 : partitioner.part_tr.action_block_begin) + "," +
1710 0 : std::to_string(end - partitioner.part_tr.action_block_begin) + ")";
1711 : }
1712 :
1713 : /// \brief print a long bunch identification for debugging
1714 : template <class LTS_TYPE>
1715 0 : std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1716 : const
1717 0 : { assert(nullptr != end[-1].succ);
1718 0 : const action_block_entry* iter(begin); assert(iter < end);
1719 0 : assert(nullptr != iter->succ);
1720 0 : assert(iter == iter->succ->block_bunch->pred->action_block);
1721 0 : std::string result(debug_id_short(partitioner));
1722 0 : result += " containing transition";
1723 0 : result += iter < end - 1 ? "s " : " ";
1724 0 : result += iter->succ->block_bunch->pred->debug_id_short(partitioner);
1725 0 : ++iter;
1726 0 : if (end <= iter) return result;
1727 0 : while (nullptr == iter->succ) ++iter;
1728 0 : assert(iter < end);
1729 0 : assert(iter == iter->succ->block_bunch->pred->action_block);
1730 0 : result += ", ";
1731 0 : result += iter->succ->block_bunch->pred->debug_id_short(partitioner);
1732 0 : if (iter < end - 3)
1733 : {
1734 0 : result += ", ...";
1735 0 : iter = end - 3;
1736 : }
1737 0 : while (++iter < end)
1738 : {
1739 0 : if (nullptr != iter->succ)
1740 0 : { assert(iter == iter->succ->block_bunch->pred->action_block);
1741 0 : result += ", ";
1742 0 : result += iter->succ->block_bunch->pred->debug_id_short(
1743 : partitioner);
1744 : }
1745 : }
1746 0 : return result;
1747 0 : }
1748 :
1749 : /// \brief calculates the maximal allowed value for work counters
1750 : /// associated with this bunch
1751 : /// \details Work counters may only be nonzero if this bunch is a
1752 : /// single-action bunch, i. e. all its transitions have the same action
1753 : /// label. Also, only then the size can be calculated as end - begin.
1754 : template <class LTS_TYPE>
1755 34241 : int max_work_counter(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
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 34241 : label_type const label(std::lower_bound(
1761 : partitioner.action_label.cbegin(), partitioner.action_label.cend(),
1762 68482 : begin, action_label_greater) -
1763 34241 : partitioner.action_label.cbegin());
1764 34241 : assert(label < partitioner.action_label.size());
1765 34241 : assert(partitioner.action_label[label].begin <= begin);
1766 34241 : assert(0 == label || begin < partitioner.action_label[label-1].begin);
1767 34241 : if (0 == label || end < partitioner.action_label[label - 1].begin)
1768 : {
1769 29472 : assert(bisim_gjkw::check_complexity::ilog2(end - begin) <=
1770 : bisim_gjkw::check_complexity::log_n);
1771 29472 : return bisim_gjkw::check_complexity::log_n -
1772 29472 : bisim_gjkw::check_complexity::ilog2(end - begin);
1773 : }
1774 4769 : return 0;
1775 : }
1776 :
1777 : mutable bisim_gjkw::check_complexity::bunch_dnj_counter_t work_counter;
1778 : #endif
1779 : };
1780 :
1781 :
1782 : /// \brief Information about a set of transitions with the same source block,
1783 : /// in the same bunch
1784 : /// \details A block_bunch-slices contains the transitions in a single bunch
1785 : /// that start in the same block. In the end, we want each block to be stable
1786 : /// under its block_bunch-slices, i.e. every bottom state has a transition in
1787 : /// every block_bunch-slice of the block. Then, there will be one slice for
1788 : /// each transition in the minimised LTS, so we should try to minimize this
1789 : /// data structure as much as possible.
1790 : ///
1791 : /// Also note that these slices are part of a doubly-linked list. We cannot
1792 : /// change this to a singly-linked list because we occasionally delete an
1793 : /// element from this list. This would be possible with a single-linked list
1794 : /// if we could infer the order of the list somehow, e.g. from the transitions
1795 : /// in a bottom state -- however, this does not work when a block loses all its
1796 : /// bottom states, i.e. when a block splits into a small U and large R but R
1797 : /// does not contain any bottom states.
1798 : class block_bunch_slice_t
1799 : {
1800 : public:
1801 : /// \brief pointer past the end of the transitions in the block_bunch array
1802 : /// \details We do not need a begin pointer because we can always walk
1803 : /// through the transitions in the slice from end to beginning.
1804 : block_bunch_entry* end;
1805 :
1806 : /// bunch to which this slice belongs
1807 : bunch_t* bunch;
1808 :
1809 : /// \brief pointer to the first marked transition in the block_bunch array
1810 : /// \details If this pointer is nullptr, then the block_bunch_slice is
1811 : /// stable.
1812 : block_bunch_entry* marked_begin;
1813 :
1814 :
1815 : /// \brief returns true iff the block_bunch-slice is registered as stable
1816 79494 : bool is_stable() const { return nullptr == marked_begin; }
1817 :
1818 :
1819 : /// \brief register that the block_bunch-slice is stable
1820 3665 : void make_stable()
1821 3665 : { assert(!is_stable()); assert(!empty());
1822 3665 : marked_begin = nullptr;
1823 3665 : }
1824 :
1825 :
1826 : /// \brief register that the block_bunch-slice is not stable
1827 4214 : void make_unstable()
1828 4214 : { assert(is_stable());
1829 4214 : marked_begin = end; assert(!is_stable());
1830 4214 : }
1831 :
1832 :
1833 : /// \brief constructor
1834 2833 : block_bunch_slice_t(block_bunch_entry* const new_end,
1835 : bunch_t* const new_bunch, bool const new_is_stable)
1836 2833 : : end(new_end),
1837 2833 : bunch(new_bunch),
1838 2833 : marked_begin(nullptr)
1839 : {
1840 2833 : if (!new_is_stable) make_unstable();
1841 2833 : }
1842 :
1843 :
1844 : /// \brief returns true iff the block_bunch-slice is empty
1845 : /// \details A block_bunch-slice should only become empty if it is
1846 : /// unstable.
1847 71638 : 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 71638 : return end[-1].slice != this;
1852 : }
1853 :
1854 :
1855 : /// compute the source block of the transitions in this slice
1856 60182 : block_t* source_block() const
1857 60182 : { assert(!empty());
1858 60182 : return end[-1].pred->source->bl.ock;
1859 : }
1860 : #ifndef NDEBUG
1861 : /// \brief print a block_bunch-slice identification for debugging
1862 : template <class LTS_TYPE>
1863 0 : std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
1864 : const
1865 : {
1866 : static struct {
1867 0 : bool operator()(const block_bunch_entry& p1,
1868 : const block_bunch_slice_t* const p2) const
1869 : {
1870 0 : return p1.slice != p2;
1871 : }
1872 : } const block_bunch_not_equal;
1873 :
1874 0 : assert(&partitioner.part_tr.block_bunch.front() < end);
1875 0 : assert(end <= partitioner.part_tr.block_bunch_inert_begin);
1876 0 : std::string const index_string(std::to_string(end -
1877 0 : &partitioner.part_tr.block_bunch.cbegin()[1]));
1878 0 : if (empty())
1879 : { //assert(!is_stable());
1880 : return "empty block_bunch_slice [" + index_string + "," +
1881 0 : index_string + ")";
1882 : }
1883 : const block_bunch_entry* begin(
1884 0 : &partitioner.part_tr.block_bunch.cbegin()[1]);
1885 0 : if (trans_type bunch_size(bunch->end - bunch->begin);
1886 0 : (trans_type) (end - begin) > bunch_size)
1887 : {
1888 0 : begin = end - bunch_size;
1889 : }
1890 0 : begin = std::lower_bound(begin, const_cast<const block_bunch_entry*>
1891 0 : (is_stable() || marked_begin==end ? end-1 : marked_begin),
1892 : this, block_bunch_not_equal);
1893 0 : assert(begin->slice == this);
1894 0 : assert(begin[-1].slice != this);
1895 0 : return (is_stable() ? "stable block_bunch-slice ["
1896 : : "unstable block_bunch_slice [") +
1897 0 : std::to_string(begin-&partitioner.part_tr.block_bunch.cbegin()[1]) +
1898 : "," + index_string + ") containing transitions from " +
1899 : source_block()->debug_id(partitioner) +
1900 0 : " in " + bunch->debug_id_short(partitioner);
1901 0 : }
1902 :
1903 : /// \brief add work to transitions starting in bottom states
1904 : /// \details Sometimes an action is done whose time could be accounted for
1905 : /// by any transition starting in a bottom state of the block.
1906 : /// \param ctr counter type to which work is assigned
1907 : /// \param max_value new value of the counter
1908 : /// \param partitioner LTS partitioner (to print error messages if
1909 : /// necessary)
1910 : template <class LTS_TYPE>
1911 121 : bool add_work_to_bottom_transns(enum bisim_gjkw::check_complexity::
1912 : counter_type const ctr, unsigned const max_value,
1913 : const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
1914 121 : { assert(!empty());
1915 121 : assert(1U == max_value);
1916 121 : const block_t* const block(source_block());
1917 121 : bool result(false);
1918 121 : const block_bunch_entry* block_bunch(end);
1919 121 : assert(partitioner.part_tr.block_bunch.front().slice != this);
1920 121 : assert(block_bunch[-1].slice == this);
1921 : do
1922 : {
1923 383 : --block_bunch;
1924 383 : const state_info_entry* const source(block_bunch->pred->source);
1925 383 : assert(source->bl.ock == block);
1926 383 : 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 227 : mCRL2complexity(block_bunch->pred, add_work(ctr, max_value),
1932 : partitioner);
1933 227 : result = true;
1934 : }
1935 : }
1936 383 : while (block_bunch[-1].slice == this);
1937 121 : return result;
1938 : }
1939 :
1940 : mutable bisim_gjkw::check_complexity::block_bunch_dnj_counter_t
1941 : work_counter;
1942 : #endif
1943 : };
1944 :
1945 :
1946 : /// \brief find the beginning of the out-slice
1947 2141 : inline succ_entry* succ_entry::out_slice_begin( ONLY_IF_DEBUG( const bisim_gjkw::fixed_vector<succ_entry>& succ )
1948 : )
1949 2141 : { assert(nullptr != begin_or_before_end);
1950 2141 : succ_entry* result(begin_or_before_end); assert(result->block_bunch->pred->action_block->succ == result);
1951 2141 : if (this < result)
1952 510 : { assert(nullptr != result->begin_or_before_end);
1953 510 : assert(this == result->begin_or_before_end);
1954 510 : result = this; assert(result->block_bunch->pred->action_block->succ == result);
1955 2141 : } assert(block_bunch->pred->source == result->block_bunch->pred->source);
1956 : // assert(this <= result); //< holds always, based on the if() above
1957 2141 : assert(nullptr != result->begin_or_before_end);
1958 2141 : assert(this <= result->begin_or_before_end);
1959 2141 : assert(block_bunch->slice == result->block_bunch->slice);
1960 2141 : 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 2141 : return result;
1964 : }
1965 :
1966 :
1967 : /// \brief find the bunch of a transition
1968 75638 : inline bunch_t* succ_entry::bunch() const
1969 : {
1970 75638 : return block_bunch->slice->bunch;
1971 : }
1972 : #ifndef NDEBUG
1973 : /// \brief register that work has been done for the out-slice containing
1974 : /// `out_slice_begin`
1975 : /// \details This function should be used if work
1976 : /// \param partitioner the partitioner data structure, used to write
1977 : /// diagnostic messages
1978 : /// \param out_slice_begin the first transition in the out-slice
1979 : /// \param ctr counter type to which work has to be assigned
1980 : /// \param max_value new value of the counter
1981 : template <class LTS_TYPE>
1982 14 : /* 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 14 : const succ_entry* const out_slice_before_end(
1988 : out_slice_begin->begin_or_before_end);
1989 14 : assert(nullptr != out_slice_before_end);
1990 14 : assert(out_slice_begin <= out_slice_before_end);
1991 14 : mCRL2complexity(out_slice_begin->block_bunch->pred,
1992 : add_work(ctr, max_value), partitioner);
1993 15 : while (++out_slice_begin <= out_slice_before_end)
1994 : {
1995 : // treat temporary counters specially
1996 1 : mCRL2complexity(out_slice_begin->block_bunch->pred,
1997 : add_work_notemporary(ctr, max_value), partitioner);
1998 : }
1999 14 : }
2000 : #endif
2001 : class part_trans_t
2002 : {
2003 : public:
2004 : /// \brief array containing all successor entries
2005 : /// \details The first and last entry are dummy entries, pointing to a
2006 : /// transition from nullptr to nullptr, to make it easier to check whether
2007 : /// there is another transition from the current state.
2008 : bisim_gjkw::fixed_vector<succ_entry> succ;
2009 :
2010 : /// \brief array containing all block_bunch entries
2011 : /// \details The first entry is a dummy entry, pointing to a transition not
2012 : /// contained in any slice, to make it easier to check whether there is
2013 : /// another transition in the current block_bunch.
2014 : bisim_gjkw::fixed_vector<block_bunch_entry> block_bunch;
2015 :
2016 : /// \brief array containing all predecessor entries
2017 : /// \details The first and last entry are dummy entries, pointing to a
2018 : /// transition to nullptr, to make it easier to check whether there is
2019 : /// another transition to the current state.
2020 : bisim_gjkw::fixed_vector<pred_entry> pred;
2021 :
2022 : /// \brief array containing all action_block entries
2023 : /// \details During initialisation, the transitions are sorted according to
2024 : /// their label. Between transitions with different labels there is a dummy
2025 : /// entry, to make it easier to check whether there is another transition
2026 : /// in the current action_block slice.
2027 : ///
2028 : /// The array may be empty, in particular if there are no transitions. In
2029 : /// that case, the two pointers (and `action_block_inert_begin` below)
2030 : /// should all be null pointers. Also, front() and back() are undefined;
2031 : /// to avoid trouble with these methods, I decided to just store pointers
2032 : /// to the beginning and the end of the array.
2033 : action_block_entry* const action_block_begin;
2034 : action_block_entry* const action_block_end;
2035 :
2036 : /// \brief pointer to the first inert transition in block_bunch
2037 : block_bunch_entry* block_bunch_inert_begin;
2038 :
2039 : /// \brief pointer to the first inert transition in action_block
2040 : action_block_entry* action_block_inert_begin;
2041 : #ifndef NDEBUG
2042 : /// \brief pointer to the first inert transition in the initial partition
2043 : const action_block_entry* action_block_orig_inert_begin;
2044 : #endif
2045 : /// \brief list of unstable block_bunch-slices
2046 : simple_list<block_bunch_slice_t> splitter_list;
2047 : private:
2048 : /// \brief pointer to first non-trivial bunch
2049 : bunch_t* first_nontrivial;
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<
2055 : simple_list<block_bunch_slice_t>::entry>::value);
2056 : /// \brief pool for allocation of block_bunch-slices
2057 : my_pool<simple_list<block_bunch_slice_t>::entry> storage;
2058 : #endif
2059 :
2060 : /// \brief number of new bottom states found until now.
2061 : state_type nr_of_new_bottom_states;
2062 :
2063 : /// \brief counters to measure progress
2064 : trans_type nr_of_bunches;
2065 : trans_type nr_of_nontrivial_bunches;
2066 : trans_type nr_of_action_block_slices;
2067 : trans_type nr_of_block_bunch_slices;
2068 :
2069 : /// \brief constructor
2070 : /// \details The constructor sets up the dummy transitions at the beginning
2071 : /// and end of the succ, block_bunch and pred arrays. (Dummy transitions
2072 : /// in action_block depend on the number of transitions per action label,
2073 : /// so they cannot be set up without knowing details about how many
2074 : /// transitions have which label.)
2075 : /// \param num_transitions number of transitions of the LTS
2076 : /// \param num_actions number of action labels of the LTS
2077 333 : part_trans_t(trans_type num_transitions,
2078 : trans_type num_actions)
2079 333 : : succ(num_transitions + 2),
2080 333 : block_bunch(num_transitions + 1),
2081 333 : pred(num_transitions + 2),
2082 333 : action_block_begin(
2083 333 : new action_block_entry[num_transitions + num_actions - 1]),
2084 333 : action_block_end(action_block_begin + (num_transitions+num_actions-1)),
2085 333 : block_bunch_inert_begin(1 + &block_bunch.back()),
2086 333 : action_block_inert_begin(action_block_end),
2087 333 : splitter_list(),
2088 333 : first_nontrivial(nullptr),
2089 333 : nr_of_new_bottom_states(0),
2090 333 : nr_of_bunches(0),
2091 333 : nr_of_nontrivial_bunches(0),
2092 333 : nr_of_action_block_slices(0),
2093 333 : nr_of_block_bunch_slices(0)
2094 : {
2095 333 : succ.front().block_bunch = &block_bunch.front();
2096 333 : succ.back() .block_bunch = &block_bunch.front();
2097 333 : block_bunch.front().pred = &pred.front();
2098 333 : block_bunch.front().slice = nullptr;
2099 333 : pred.front().source = nullptr;
2100 333 : pred.front().target = nullptr;
2101 333 : pred.back() .source = nullptr;
2102 333 : pred.back() .target = nullptr;
2103 333 : }
2104 :
2105 :
2106 : /// \brief destructor
2107 333 : ~part_trans_t()
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 333 : delete [] action_block_begin;
2134 : #endif
2135 333 : }
2136 :
2137 :
2138 : /// \brief provide some bunch from the list of non-trivial bunches
2139 : /// \returns pointer to a bunch that is in the list of non-trivial bunches
2140 1757 : bunch_t* get_some_nontrivial()
2141 : {
2142 1757 : return first_nontrivial;
2143 : }
2144 :
2145 :
2146 : /// \brief insert a bunch into the list of nontrivial bunches
2147 : /// \param bunch the bunch that has become non-trivial
2148 470 : void make_nontrivial(bunch_t* const bunch)
2149 470 : { 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);
2152 470 : bunch->next_nontrivial_and_label.next_nontrivial =
2153 470 : 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);
2158 470 : first_nontrivial = bunch; assert(nr_of_nontrivial_bunches < nr_of_bunches);
2159 470 : ++nr_of_nontrivial_bunches; //assert(end[-1].begin_or_before_end <= end);
2160 470 : }
2161 :
2162 :
2163 : /// \brief remove a bunch from the list of nontrivial bunches
2164 : /// \param bunch the bunch that has become trivial
2165 470 : void make_trivial(bunch_t* const bunch)
2166 470 : { assert(!bunch->is_trivial()); assert(first_nontrivial == bunch);
2167 470 : first_nontrivial =
2168 470 : bunch == bunch->next_nontrivial_and_label.next_nontrivial
2169 470 : ? nullptr : bunch->next_nontrivial_and_label.next_nontrivial; assert(bunch->end - 1 == bunch->begin->begin_or_before_end);
2170 470 : bunch->next_nontrivial_and_label.next_nontrivial = nullptr; assert(0 < nr_of_nontrivial_bunches);
2171 470 : --nr_of_nontrivial_bunches; assert(bunch->begin == bunch->end[-1].begin_or_before_end);
2172 470 : }
2173 :
2174 :
2175 : /// \brief transition is moved to a new bunch
2176 : /// \details This (and the next function) have to be called after a
2177 : /// transition has changed its bunch. The member function will adapt the
2178 : /// transition data structure. It assumes that the transition is
2179 : /// non-inert.
2180 : ///
2181 : /// The work has to be done in two steps: We call the first step
2182 : /// first_move_transition_to_new_bunch() for each transition in the new
2183 : /// bunch, and then call second_move_transition_to_new_bunch() again for
2184 : /// all these transitions. The reason is that some data structures need to
2185 : /// be finalised in the second phase.
2186 : ///
2187 : /// The first phase moves all transitions to their correct position in
2188 : /// the out-slices and block_bunch-slices, but it doesn't yet create
2189 : /// a fully correct new out-slice and block_bunch-slice. It adapts
2190 : /// current_out_slice of all states with a transition in the new bunch.
2191 : /// \param action_block_iter_iter transition that has to be changed
2192 : /// \param bunch_T_a_Bprime the new bunch in which the transition
2193 : /// lies
2194 : /// \param first_transition_of_state true iff this is the first transition
2195 : /// of the state, so a new out-slice has
2196 : /// to be allocated.
2197 2141 : void first_move_transition_to_new_bunch(
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 2141 : succ_entry* const old_succ_pos(action_block_iter->succ); assert(nullptr != old_succ_pos);
2206 2141 : assert(old_succ_pos->block_bunch->pred->action_block == action_block_iter);
2207 2141 : succ_entry* const out_slice_begin(old_succ_pos->out_slice_begin( ONLY_IF_DEBUG( succ )
2208 2141 : )); assert(out_slice_begin->block_bunch->pred->action_block->succ ==
2209 : out_slice_begin);
2210 2141 : succ_entry* const new_succ_pos(out_slice_begin->begin_or_before_end); assert(nullptr != new_succ_pos);
2211 2141 : assert(out_slice_begin == new_succ_pos->begin_or_before_end);
2212 2141 : assert(new_succ_pos<old_succ_pos->block_bunch->pred->source->succ_inert.begin);
2213 2141 : /* move the transition to the end of its out-slice */ assert(new_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
2214 2141 : if (old_succ_pos < new_succ_pos)
2215 : {
2216 620 : std::swap(old_succ_pos->block_bunch, new_succ_pos->block_bunch);
2217 620 : 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 620 : action_block_iter->succ = new_succ_pos;
2219 1521 : } 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 2141 : 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 2141 : if (first_transition_of_state)
2233 : {
2234 2072 : new_succ_pos->begin_or_before_end = new_succ_pos;
2235 : }
2236 : else
2237 : {
2238 69 : succ_entry* const out_slice_before_end(
2239 69 : new_succ_pos[1].begin_or_before_end); assert(nullptr != out_slice_before_end);
2240 69 : assert(new_succ_pos < out_slice_before_end);
2241 69 : assert(out_slice_before_end->block_bunch->pred->action_block->succ ==
2242 : out_slice_before_end);
2243 69 : assert(new_succ_pos + 1 == out_slice_before_end->begin_or_before_end);
2244 69 : 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 69 : new_succ_pos->begin_or_before_end = out_slice_before_end; assert(bunch_T_a_Bprime == out_slice_before_end->bunch());
2247 : }
2248 :
2249 2141 : /* - - - - - - - adapt part_tr.block_bunch - - - - - - - */ assert(new_succ_pos == action_block_iter->succ);
2250 :
2251 2141 : block_bunch_entry* const old_block_bunch_pos(
2252 2141 : new_succ_pos->block_bunch); assert(old_block_bunch_pos->pred->action_block == action_block_iter);
2253 2141 : block_t*const source_block = old_block_bunch_pos->pred->source->bl.ock; assert(!old_block_bunch_pos->slice.is_null());
2254 2141 : 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 2141 : old_block_bunch_slice->end - 1); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
2258 2141 : 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 3948 : if (new_block_bunch_pos + 1 >= block_bunch_inert_begin ||
2263 1807 : (new_block_bunch_slice = (block_bunch_slice_iter_t)
2264 1807 : new_block_bunch_pos[1].slice, assert(!new_block_bunch_pos[1].slice.is_null()),
2265 1807 : bunch_T_a_Bprime != new_block_bunch_slice->bunch ||
2266 570 : source_block != new_block_bunch_slice->source_block()))
2267 1573 : { 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 1573 : new_block_bunch_slice = splitter_list.emplace_back(
2276 1573 : ONLY_IF_POOL_ALLOCATOR( storage, )
2277 1573 : 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 1573 : ++nr_of_block_bunch_slices; ONLY_IF_DEBUG( new_block_bunch_slice->work_counter =
2284 : old_block_bunch_slice->work_counter; )
2285 1573 : splitter_list.splice(splitter_list.end(),
2286 1573 : source_block->stable_block_bunch, old_block_bunch_slice);
2287 1573 : old_block_bunch_slice->make_unstable();
2288 2141 : } assert(!new_block_bunch_slice->is_stable());
2289 :
2290 : // move the transition to the end of its block_bunch-slice
2291 2141 : if (old_block_bunch_pos < new_block_bunch_pos)
2292 : {
2293 1318 : std::swap(old_block_bunch_pos->pred, new_block_bunch_pos->pred); assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2294 1318 : old_block_bunch_pos->pred->action_block->succ->block_bunch =
2295 1318 : old_block_bunch_pos; assert(new_succ_pos == new_block_bunch_pos->pred->action_block->succ);
2296 1318 : new_succ_pos->block_bunch = new_block_bunch_pos;
2297 823 : } else assert(new_block_bunch_pos == old_block_bunch_pos);
2298 2141 : assert(new_block_bunch_pos->slice == old_block_bunch_slice);
2299 2141 : new_block_bunch_pos->slice = new_block_bunch_slice;
2300 :
2301 2141 : /* adapt the old block_bunch-slice */ assert(new_block_bunch_pos + 1 == old_block_bunch_slice->marked_begin);
2302 2141 : old_block_bunch_slice->end = new_block_bunch_pos;
2303 2141 : old_block_bunch_slice->marked_begin = new_block_bunch_pos; assert(nullptr != new_block_bunch_pos);
2304 2141 : if (old_block_bunch_slice->empty())
2305 410 : { assert(!old_block_bunch_slice->is_stable());
2306 410 : splitter_list.erase( ONLY_IF_POOL_ALLOCATOR( storage, )
2307 410 : old_block_bunch_slice); assert(!new_block_bunch_slice->is_stable());
2308 410 : --nr_of_block_bunch_slices;
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 410 : source_block->stable_block_bunch.splice(
2315 : source_block->stable_block_bunch.end(),
2316 410 : splitter_list, new_block_bunch_slice);
2317 410 : 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 410 : source_block->marked_nonbottom_begin = source_block->end; assert(source_block->marked_bottom_begin == source_block->begin);
2324 410 : source_block->marked_bottom_begin = source_block->nonbottom_begin;
2325 : }
2326 2141 : }
2327 :
2328 :
2329 : /// \brief transition is moved to a new bunch, phase 2
2330 : /// \details This (and the previous function) have to be called after a
2331 : /// transition has changed its bunch. The member function will adapt the
2332 : /// transition data structure. It assumes that the transition is
2333 : /// non-inert.
2334 : ///
2335 : /// The work has to be done in two steps: We call the first step
2336 : /// first_move_transition_to_new_bunch() for each transition in the new
2337 : /// bunch, and then call second_move_transition_to_new_bunch() again for
2338 : /// all these transitions. The reason is that some data structures need to
2339 : /// be finalised/ in the second phase.
2340 : ///
2341 : /// The second phase finalizes the new out-slices and block_bunch-slices
2342 : /// that were left half-finished by the first phase. It assumes that all
2343 : /// block_bunch-slices are registered as stable.
2344 : /// \param action_block_iter_iter transition that has to be changed
2345 : /// \param large_splitter_bunch the large splitter_bunch that has
2346 : /// been split; the transition has moved
2347 : /// from `large_splitter_bunch` to a new,
2348 : /// small bunch.
2349 : ONLY_IF_DEBUG( template <class LTS_TYPE> )
2350 2141 : void second_move_transition_to_new_bunch(
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 2141 : { 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 2141 : succ_entry* const new_succ_pos(action_block_iter->succ); assert(nullptr != new_succ_pos);
2362 2141 : assert(new_succ_pos->block_bunch->pred->action_block == action_block_iter);
2363 2141 : state_info_entry* const source(
2364 2141 : new_succ_pos->block_bunch->pred->source); assert(source->pos->st == source);
2365 2141 : assert(new_succ_pos < source->succ_inert.begin);
2366 2141 : assert(source == &partitioner.part_st.state_info.front() ||
2367 : source[-1].succ_inert.begin <= new_succ_pos);
2368 2141 : assert(nullptr != new_succ_pos->begin_or_before_end);
2369 2141 : succ_entry* const new_begin_or_before_end(
2370 2141 : new_succ_pos->begin_or_before_end->begin_or_before_end); assert(nullptr != new_begin_or_before_end);
2371 2141 : assert(new_begin_or_before_end->block_bunch->pred->action_block->succ ==
2372 : new_begin_or_before_end);
2373 2141 : if (new_begin_or_before_end < new_succ_pos)
2374 6 : { assert(source == &partitioner.part_st.state_info.front() ||
2375 : source[-1].succ_inert.begin <= new_begin_or_before_end);
2376 6 : new_succ_pos->begin_or_before_end = new_begin_or_before_end;
2377 : }
2378 : else
2379 2135 : { assert(new_begin_or_before_end == new_succ_pos);
2380 : // This is the first or the last transition in the out-slice.
2381 2135 : const succ_entry* const new_before_end(
2382 2135 : new_begin_or_before_end->begin_or_before_end); assert(nullptr != new_before_end);
2383 2135 : if (new_begin_or_before_end <= new_before_end)
2384 2072 : { 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 2072 : /* we prepay for it. */ assert(new_before_end + 1 == source->succ_inert.begin ||
2388 : bunch_T_a_Bprime != new_before_end[1].bunch());
2389 3046 : if (source == new_succ_pos[-1].block_bunch->pred->source &&
2390 974 : new_succ_pos[-1].bunch() == large_splitter_bunch)
2391 : {
2392 : // Mark one transition in the large slice
2393 932 : block_bunch_entry* const old_block_bunch_pos(
2394 932 : new_succ_pos[-1].block_bunch); assert(!old_block_bunch_pos->slice.is_null());
2395 932 : assert(old_block_bunch_pos->pred->action_block->succ == new_succ_pos - 1);
2396 932 : block_bunch_slice_iter_t const large_splitter_slice(
2397 : old_block_bunch_pos->slice);
2398 932 : if (!large_splitter_slice->is_stable())
2399 : {
2400 932 : block_bunch_entry* const new_block_bunch_pos(
2401 932 : large_splitter_slice->marked_begin - 1); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
2402 932 : assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
2403 : new_block_bunch_pos);
2404 932 : if (old_block_bunch_pos < new_block_bunch_pos)
2405 : {
2406 487 : std::swap(old_block_bunch_pos->pred,
2407 487 : new_block_bunch_pos->pred); // assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2408 487 : old_block_bunch_pos->pred->action_block->
2409 487 : succ->block_bunch = old_block_bunch_pos; assert(new_block_bunch_pos->pred->action_block->succ == new_succ_pos - 1);
2410 487 : new_succ_pos[-1].block_bunch = new_block_bunch_pos;
2411 : }
2412 932 : large_splitter_slice->marked_begin=new_block_bunch_pos; assert(nullptr != new_block_bunch_pos);
2413 0 : } else assert(1 >= source->bl.ock->size());
2414 : }
2415 63 : } else assert(source == &partitioner.part_st.state_info.front() ||
2416 : source[-1].succ_inert.begin <= new_before_end);
2417 : }
2418 : #ifndef NDEBUG
2419 2141 : /* - - - - - - - adapt part_tr.block_bunch - - - - - - - */ const block_bunch_entry* new_block_bunch_pos(new_succ_pos->block_bunch);
2420 2141 : assert(new_block_bunch_pos->pred->action_block->succ == new_succ_pos);
2421 2141 : assert(!new_block_bunch_pos->slice.is_null());
2422 2141 : /* Nothing needs to be done. */ block_bunch_slice_const_iter_t const new_block_bunch_slice(
2423 : new_block_bunch_pos->slice);
2424 2141 : assert(new_block_bunch_pos < new_block_bunch_slice->end);
2425 2141 : assert(bunch_T_a_Bprime == new_block_bunch_slice->bunch);
2426 2141 : 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 2141 : do assert(source->bl.ock == new_block_bunch_pos->pred->source->bl.ock);
2432 2141 : while ((--new_block_bunch_pos)->slice == new_block_bunch_slice);
2433 1573 : 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:
2441 : /// \brief Adapt the non-inert transitions in an out-slice to a new block
2442 : /// \details After a block has been split, the outgoing transitions of the
2443 : /// new block need to move to the respective block_bunch-slice of the new
2444 : /// block.
2445 : ///
2446 : /// This function handles all transitions in the out-slice just before
2447 : /// `out_slice_end`, as they all belong to the same block_bunch-slice and
2448 : /// can be moved together. However, transitions in `splitter_T` are
2449 : /// excepted: all transitions in `splitter_T` from all states are
2450 : /// transitions of the R-subblock, so if the latter is the new block, then
2451 : /// `splitter_T` can be moved as a whole instead of per-state. In this
2452 : /// case, the caller should move `splitter_T` to the list of stable
2453 : /// block_bunch-slices of the R-subblock.
2454 : ///
2455 : /// The function returns the beginning of this out-slice (which can become
2456 : /// the next out_slice_end). It is meant to be called from the last
2457 : /// out-slice back to the first because it inserts stable
2458 : /// block_bunch-slices at the beginning of the list for the new block, so
2459 : /// it would normally become ordered according to the bunch.
2460 : /// \param out_slice_end The transition just after the out-slice that is
2461 : /// adapted
2462 : /// \param old_block The block in which the source state of the
2463 : /// out-slice was before it was split (only needed if
2464 : /// we do not use simple lists)
2465 : /// \param splitter_T The splitter that made this block split
2466 : /// \returns the beginning of this out-slice (which can become the next
2467 : /// out_slice_end)
2468 : ONLY_IF_DEBUG( template <class LTS_TYPE> )
2469 1876 : succ_entry* move_out_slice_to_new_block(
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 1876 : { assert(&succ.cbegin()[1] < out_slice_end);
2476 1876 : succ_entry* const out_slice_begin(
2477 1876 : out_slice_end[-1].begin_or_before_end); assert(nullptr != out_slice_begin);
2478 1876 : assert(out_slice_begin < out_slice_end);
2479 1876 : assert(out_slice_begin->block_bunch->pred->action_block->succ ==
2480 : out_slice_begin);
2481 1876 : block_bunch_entry* old_block_bunch_pos(out_slice_end[-1].block_bunch); assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2482 1876 : assert(!old_block_bunch_pos->slice.is_null());
2483 1876 : block_bunch_slice_iter_t const old_block_bunch_slice(
2484 1876 : old_block_bunch_pos->slice); assert(old_block_bunch_pos->pred->action_block->succ->block_bunch ==
2485 : old_block_bunch_pos);
2486 1876 : if (&*splitter_T == &*old_block_bunch_slice) return out_slice_begin;
2487 :
2488 1016 : block_bunch_entry* old_block_bunch_slice_end(
2489 1016 : old_block_bunch_slice->end);
2490 1016 : state_info_entry* const source(old_block_bunch_pos->pred->source); assert(out_slice_end <= source->succ_inert.begin);
2491 1016 : assert(&partitioner.part_st.state_info.front() == source ||
2492 : source[-1].succ_inert.begin < out_slice_end);
2493 1016 : block_t* const new_block(source->bl.ock); assert(source == out_slice_begin->block_bunch->pred->source);
2494 1016 : block_bunch_slice_iter_t new_block_bunch_slice; assert(source->pos->st == source);
2495 2990 : if (old_block_bunch_slice_end >= block_bunch_inert_begin ||
2496 1491 : new_block != old_block_bunch_slice_end->pred->source->bl.ock ||
2497 : (new_block_bunch_slice = (block_bunch_slice_iter_t)
2498 475 : old_block_bunch_slice_end->slice, assert(!old_block_bunch_slice_end->slice.is_null()),
2499 475 : 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 814 : 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 =
2508 404 : new_block->stable_block_bunch.emplace_front(
2509 202 : ONLY_IF_POOL_ALLOCATOR( storage, )
2510 202 : old_block_bunch_slice->end,
2511 404 : old_block_bunch_slice->bunch, true);
2512 : #else
2513 : new_block->stable_block_bunch.emplace_front(
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 612 : new_block_bunch_slice = splitter_list.emplace_after(
2524 612 : ONLY_IF_POOL_ALLOCATOR( storage, )
2525 : old_block_bunch_slice,
2526 612 : old_block_bunch_slice->end,
2527 1224 : 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 814 : ++nr_of_block_bunch_slices; ONLY_IF_DEBUG( new_block_bunch_slice->work_counter =
2536 : old_block_bunch_slice->work_counter; )
2537 : }
2538 1016 : ONLY_IF_DEBUG( unsigned max_counter = bisim_gjkw::check_complexity::log_n -
2539 : bisim_gjkw::check_complexity::ilog2(new_block->size()); )
2540 1016 : /* move all transitions in this out-slice to the new block_bunch */ assert(out_slice_begin < out_slice_end);
2541 : do
2542 1370 : { assert(old_block_bunch_pos == out_slice_end[-1].block_bunch);
2543 1370 : --out_slice_end; assert(old_block_bunch_pos->slice == old_block_bunch_slice);
2544 1370 : assert(source == out_slice_end->block_bunch->pred->source);
2545 1370 : --old_block_bunch_slice_end; // assign work already now because the transition may be moved to several
2546 : // places:
2547 1370 : 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 2511 : if (old_block_bunch_slice->is_stable() || ( assert(!new_block_bunch_slice->is_stable()),
2550 1141 : old_block_bunch_slice->marked_begin >
2551 416 : old_block_bunch_slice_end &&
2552 416 : (/* 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 416 : 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 645 : std::swap(old_block_bunch_pos->pred,
2561 645 : old_block_bunch_slice_end->pred);
2562 : }
2563 : else
2564 : {
2565 : // The old block_bunch-slice is unstable and has marked
2566 : // transitions.
2567 725 : pred_entry* const old_pred = old_block_bunch_pos->pred;
2568 725 : 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 389 : block_bunch_entry* const old_marked_begin =
2575 389 : old_block_bunch_slice->marked_begin - 1; assert(old_block_bunch_pos < old_block_bunch_slice_end);
2576 389 : old_block_bunch_slice->marked_begin = old_marked_begin;
2577 :
2578 389 : old_block_bunch_pos->pred = old_marked_begin->pred;
2579 389 : old_marked_begin->pred = old_block_bunch_slice_end->pred;
2580 389 : old_block_bunch_slice_end->pred = old_pred; assert(nullptr != old_marked_begin->pred->action_block->succ);
2581 :
2582 389 : old_marked_begin->pred->action_block->succ->
2583 389 : 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 336 : block_bunch_entry* const new_marked_begin =
2590 336 : new_block_bunch_slice->marked_begin - 1;
2591 336 : 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 336 : old_block_bunch_pos->pred=old_block_bunch_slice_end->pred; assert(old_block_bunch_slice_end <= new_marked_begin);
2594 336 : old_block_bunch_slice_end->pred = new_marked_begin->pred;
2595 336 : new_marked_begin->pred = old_pred; assert(out_slice_end == new_marked_begin->pred->action_block->succ);
2596 :
2597 336 : out_slice_end->block_bunch = new_marked_begin;
2598 : }
2599 1370 : } assert(nullptr != old_block_bunch_slice_end->pred->action_block->succ);
2600 1370 : old_block_bunch_slice_end->pred->action_block->succ->block_bunch =
2601 1370 : old_block_bunch_slice_end; assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2602 1370 : old_block_bunch_pos->pred->action_block->succ->block_bunch =
2603 : old_block_bunch_pos;
2604 : }
2605 1724 : while (out_slice_begin < out_slice_end &&
2606 354 : (old_block_bunch_pos = out_slice_end[-1].block_bunch, true));
2607 1016 : old_block_bunch_slice->end = old_block_bunch_slice_end;
2608 :
2609 1016 : if (old_block_bunch_slice->empty())
2610 : {
2611 : #ifdef USE_SIMPLE_LIST
2612 171 : simple_list<block_bunch_slice_t>::erase(
2613 171 : ONLY_IF_POOL_ALLOCATOR( storage, )
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
2639 171 : --nr_of_block_bunch_slices;
2640 : }
2641 1016 : return out_slice_begin;
2642 : }
2643 :
2644 :
2645 : /// \brief handle one transition after a block has been split
2646 : /// \details The main task of this method is to move the transition to the
2647 : /// correct place in the action_block slice.
2648 : ///
2649 : /// This function handles phase 1. Because the new action_block-slice
2650 : /// cannot be adapted completely until all transitions into the new block
2651 : /// have been handled through phase 1, the next function handles them again
2652 : /// in phase 2.
2653 : /// \param pred_iter transition that has to be moved
2654 2481 : void first_move_transition_to_new_action_block(pred_entry* const pred_iter)
2655 : {
2656 2481 : action_block_entry* const old_action_block_pos(
2657 2481 : pred_iter->action_block); assert(nullptr != old_action_block_pos->succ);
2658 2481 : assert(old_action_block_pos->succ->block_bunch->pred == pred_iter);
2659 : action_block_entry* const action_block_slice_begin(
2660 2481 : old_action_block_pos->action_block_slice_begin( ONLY_IF_DEBUG( action_block_begin, action_block_orig_inert_begin )
2661 2481 : )); assert(nullptr != action_block_slice_begin->succ);
2662 2481 : assert(action_block_slice_begin->succ->block_bunch->pred->action_block ==
2663 : action_block_slice_begin);
2664 2481 : action_block_entry* const new_action_block_pos(
2665 2481 : action_block_slice_begin->begin_or_before_end); assert(nullptr != new_action_block_pos);
2666 2481 : assert(action_block_slice_begin == new_action_block_pos->begin_or_before_end);
2667 2481 : assert(nullptr != new_action_block_pos->succ);
2668 2481 : 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 2481 : if (old_action_block_pos < new_action_block_pos)
2671 : {
2672 1161 : succ_entry* const temp(new_action_block_pos->succ); assert(nullptr != temp); assert(nullptr != old_action_block_pos->succ);
2673 1161 : new_action_block_pos->succ = old_action_block_pos->succ;
2674 1161 : old_action_block_pos->succ = temp;
2675 1161 : temp->block_bunch->pred->action_block = old_action_block_pos; assert(pred_iter == new_action_block_pos->succ->block_bunch->pred);
2676 1161 : pred_iter->action_block = new_action_block_pos;
2677 :
2678 : // adapt the old action_block-slice immediately
2679 1161 : action_block_slice_begin->begin_or_before_end =
2680 1161 : new_action_block_pos - 1;
2681 : }
2682 : else
2683 1320 : { assert(old_action_block_pos == new_action_block_pos);
2684 1320 : 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 526 : action_block_slice_begin->begin_or_before_end =
2690 526 : new_action_block_pos - 1;
2691 : }
2692 794 : else --nr_of_action_block_slices;
2693 2481 : } assert(nullptr != new_action_block_pos->succ);
2694 2481 : 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 7344 : if (new_action_block_pos + 1 >= action_block_inert_begin ||
2701 2382 : nullptr == new_action_block_pos[1].succ ||
2702 1507 : new_action_block_pos[1].succ->bunch() !=
2703 6171 : new_action_block_pos->succ->bunch() ||
2704 1308 : new_action_block_pos[1].succ->block_bunch->pred->target->bl.ock !=
2705 1308 : pred_iter->target->bl.ock)
2706 : {
2707 : // This is the first transition that moves to this new
2708 : // action_block-slice.
2709 1481 : new_action_block_pos->begin_or_before_end = new_action_block_pos;
2710 1481 : ++nr_of_action_block_slices;
2711 : }
2712 : else
2713 : {
2714 1000 : action_block_entry* const action_block_slice_before_end(
2715 1000 : new_action_block_pos[1].begin_or_before_end); assert(nullptr != action_block_slice_before_end);
2716 1000 : assert(new_action_block_pos < action_block_slice_before_end);
2717 1000 : assert(nullptr != action_block_slice_before_end->succ);
2718 1000 : assert(action_block_slice_before_end->succ->block_bunch->pred->action_block ==
2719 : action_block_slice_before_end);
2720 1000 : assert(new_action_block_pos + 1 ==
2721 : action_block_slice_before_end->begin_or_before_end);
2722 1000 : action_block_slice_before_end->begin_or_before_end =
2723 1000 : new_action_block_pos; assert(action_block_slice_before_end->succ->block_bunch->
2724 : pred->target->bl.ock == pred_iter->target->bl.ock);
2725 1000 : new_action_block_pos->begin_or_before_end =
2726 1000 : action_block_slice_before_end; assert(action_block_slice_before_end < action_block_inert_begin);
2727 : }
2728 2481 : }
2729 :
2730 :
2731 : /// \brief handle one transition after a block has been split, phase 2
2732 : /// \details Because the new action_block-slice cannot be adapted
2733 : /// completely until all transitions into the new block have been handled
2734 : /// through phase 1 see the previous function), this function handles them
2735 : /// again in phase 2.
2736 : /// \param pred_iter transition that has to be moved
2737 2481 : void second_move_transition_to_new_action_block(
2738 : pred_entry* const pred_iter)
2739 : {
2740 2481 : action_block_entry* const new_action_block_pos(
2741 2481 : pred_iter->action_block); assert(nullptr != new_action_block_pos->succ);
2742 2481 : assert(new_action_block_pos->succ->block_bunch->pred == pred_iter);
2743 2481 : action_block_entry* const old_begin_or_before_end(
2744 2481 : new_action_block_pos->begin_or_before_end); assert(nullptr != old_begin_or_before_end);
2745 2481 : assert(nullptr != old_begin_or_before_end->succ);
2746 2481 : assert(old_begin_or_before_end->succ->block_bunch->pred->action_block ==
2747 : old_begin_or_before_end);
2748 4962 : if (action_block_entry* const new_begin_or_before_end(
2749 2481 : old_begin_or_before_end->begin_or_before_end); assert(nullptr != new_begin_or_before_end),
2750 2481 : assert(nullptr != new_begin_or_before_end->succ),
2751 2481 : assert(new_begin_or_before_end->succ->block_bunch->pred->action_block ==
2752 2481 : new_begin_or_before_end),
2753 : new_begin_or_before_end < new_action_block_pos)
2754 399 : { assert(old_begin_or_before_end==new_begin_or_before_end->begin_or_before_end);
2755 399 : new_action_block_pos->begin_or_before_end =
2756 399 : new_begin_or_before_end; assert(new_action_block_pos <= old_begin_or_before_end);
2757 399 : return;
2758 2082 : } else assert(new_begin_or_before_end == new_action_block_pos);
2759 2082 : 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 1481 : bunch_t* const bunch(new_action_block_pos->succ->bunch());
2764 1481 : if (!bunch->is_trivial()) { return; } assert(old_begin_or_before_end + 1 == bunch->end);
2765 361 : if (bunch->begin < new_action_block_pos)
2766 : {
2767 144 : make_nontrivial(bunch);
2768 : }
2769 : }
2770 :
2771 :
2772 : /// \brief adapt data structures for a transition that has become non-inert
2773 : /// \details If the action_block-slice and the block_bunch-slice that
2774 : /// precede the inert transitions in the respective arrays fit, the
2775 : /// transition is added to these arrays instead of creating a new one.
2776 : /// This only works if:
2777 : /// - the action_block-slice has the same target block and the same action
2778 : /// as old_pred_pos
2779 : /// - the block_bunch-slice has the same source block as old_pred_pos
2780 : /// - the bunch must contain the action_block-slice.
2781 : /// If only the last two conditions are fulfilled, we can start a new
2782 : /// action_block-slice in the same bunch. (It would be best for this if
2783 : /// the R-subblock's block_bunch-slice would be the new one, because that
2784 : /// would generally allow to add the new non-inert transitions to the last
2785 : /// splitter.)
2786 : ///
2787 : /// The state is only marked if is becomes a new bottom state. Otherwise,
2788 : /// the marking/unmarking of the state is unchanged.
2789 : /// \param old_pred_pos the transition that needs to be adapted.
2790 : /// \param[in,out] new_noninert_block_bunch_ptr the bunch where new
2791 : /// non-inert transitions have to be stored.
2792 : /// If no such bunch has yet been created, it
2793 : /// is nullptr; in that case, make_noninert()
2794 : /// creates a new bunch.
2795 : /// \returns true iff the state became a new bottom state
2796 264 : 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 264 : state_info_entry* const source(old_pred_pos->source); assert(source->pos->st == source);
2800 264 : 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 264 : action_block_inert_begin++); assert(nullptr != new_action_block_pos->succ);
2804 264 : assert(new_action_block_pos->succ->block_bunch->pred->action_block ==
2805 : new_action_block_pos);
2806 264 : 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 264 : block_bunch_inert_begin++); assert(nullptr != new_block_bunch_pos->pred->action_block->succ);
2809 264 : assert(new_block_bunch_pos->pred->action_block->succ->block_bunch ==
2810 : new_block_bunch_pos);
2811 264 : action_block_entry* const old_action_block_pos(
2812 264 : old_pred_pos->action_block); assert(new_action_block_pos <= old_action_block_pos);
2813 :
2814 264 : succ_entry* const old_succ_pos(old_action_block_pos->succ); assert(nullptr != old_succ_pos);
2815 264 : block_bunch_entry* const old_block_bunch_pos(
2816 264 : old_succ_pos->block_bunch); assert(old_pred_pos == old_block_bunch_pos->pred);
2817 264 : pred_entry* const new_pred_pos(target->pred_inert.begin++); assert(nullptr != new_pred_pos->action_block->succ);
2818 264 : assert(new_pred_pos->action_block->succ->block_bunch->pred == new_pred_pos);
2819 :
2820 264 : /* adapt action_block */ assert(nullptr == new_action_block_pos->begin_or_before_end);
2821 264 : if (new_action_block_pos < old_action_block_pos)
2822 213 : { assert(nullptr == old_action_block_pos->begin_or_before_end);
2823 213 : old_action_block_pos->succ = new_action_block_pos->succ; assert(nullptr != old_action_block_pos->succ);
2824 213 : assert(old_action_block_pos->succ->block_bunch->pred->action_block ==
2825 : new_action_block_pos);
2826 213 : old_action_block_pos->succ->block_bunch->pred->action_block =
2827 : old_action_block_pos;
2828 51 : } else assert(new_action_block_pos == old_action_block_pos);
2829 264 : 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 264 : /* adapt succ */ assert(nullptr == new_succ_pos->begin_or_before_end);
2833 264 : if (new_succ_pos < old_succ_pos)
2834 50 : { assert(nullptr == old_succ_pos->begin_or_before_end);
2835 50 : old_succ_pos->block_bunch = new_succ_pos->block_bunch; assert(old_succ_pos->block_bunch->pred->action_block->succ == new_succ_pos);
2836 50 : old_succ_pos->block_bunch->pred->action_block->succ = old_succ_pos; assert(nullptr != old_succ_pos);
2837 214 : } else assert(new_succ_pos == old_succ_pos);
2838 264 : new_succ_pos->block_bunch = new_block_bunch_pos;
2839 : // new_succ_pos->begin_or_before_end = ...; -- see below
2840 :
2841 264 : /* adapt block_bunch */ assert(new_block_bunch_pos->slice.is_null());
2842 264 : if (new_block_bunch_pos < old_block_bunch_pos)
2843 213 : { assert(old_block_bunch_pos->slice.is_null());
2844 213 : assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2845 213 : 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 213 : assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
2848 213 : old_block_bunch_pos->pred->action_block->succ->block_bunch =
2849 : old_block_bunch_pos;
2850 51 : } else assert(new_block_bunch_pos == old_block_bunch_pos);
2851 264 : new_block_bunch_pos->pred = new_pred_pos;
2852 : // new_block_bunch_pos->slice = ...; -- see below
2853 :
2854 : // adapt pred
2855 264 : 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 47 : std::swap(*old_pred_pos, *new_pred_pos); assert(nullptr != old_pred_pos->action_block->succ);
2860 47 : assert(old_pred_pos->action_block->succ->block_bunch->pred == new_pred_pos);
2861 47 : old_pred_pos->action_block->succ->block_bunch->pred = old_pred_pos;
2862 217 : } else assert(new_pred_pos == old_pred_pos);
2863 264 : new_pred_pos->action_block = new_action_block_pos;
2864 :
2865 264 : /* make the state a bottom state if necessary */ assert(source->bl.ock->nonbottom_begin <= source->pos);
2866 264 : bool became_bottom(false); assert(succ.back().block_bunch->pred->source != source);
2867 264 : if (source != source->succ_inert.begin->block_bunch->pred->source)
2868 : {
2869 159 : block_t* const source_block(source->bl.ock);
2870 : // make the state a marked bottom state
2871 159 : if (source->pos >= source_block->marked_nonbottom_begin)
2872 : {
2873 0 : std::swap(*source->pos,
2874 0 : *source_block->marked_nonbottom_begin++);
2875 159 : } assert(source->pos < source_block->marked_nonbottom_begin);
2876 159 : std::swap(*source->pos, *source_block->nonbottom_begin++);
2877 159 : ++nr_of_new_bottom_states;
2878 159 : became_bottom = true;
2879 : }
2880 :
2881 264 : bunch_t* new_noninert_bunch; assert(nullptr != new_action_block_pos);
2882 264 : 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 149 : 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 149 : new_noninert_bunch->end = action_block_inert_begin;
2895 149 : /* extend the block_bunch-slice */ assert((*new_noninert_block_bunch_ptr)->end == new_block_bunch_pos);
2896 149 : (*new_noninert_block_bunch_ptr)->end = block_bunch_inert_begin;
2897 149 : if (!(*new_noninert_block_bunch_ptr)->is_stable())
2898 55 : { assert((*new_noninert_block_bunch_ptr)->marked_begin == new_block_bunch_pos);
2899 55 : (*new_noninert_block_bunch_ptr)->marked_begin =
2900 55 : block_bunch_inert_begin;
2901 : }
2902 149 : new_block_bunch_pos->slice = *new_noninert_block_bunch_ptr;
2903 :
2904 149 : /* adapt the action_block-slice */ assert(new_noninert_bunch->begin < new_action_block_pos);
2905 149 : if (nullptr != new_action_block_pos[-1].succ &&
2906 138 : target->bl.ock == new_action_block_pos[-1].
2907 138 : succ->block_bunch->pred->target->bl.ock)
2908 : {
2909 : // the action_block-slice is suitable: extend it
2910 107 : action_block_entry* const action_block_slice_begin(
2911 107 : new_action_block_pos[-1].begin_or_before_end); assert(nullptr != action_block_slice_begin);
2912 107 : assert(new_action_block_pos-1==action_block_slice_begin->begin_or_before_end);
2913 107 : assert(nullptr != action_block_slice_begin->succ);
2914 107 : assert(action_block_slice_begin->succ->block_bunch->pred->action_block ==
2915 : action_block_slice_begin);
2916 107 : action_block_slice_begin->begin_or_before_end =
2917 : new_action_block_pos;
2918 107 : new_action_block_pos->begin_or_before_end =
2919 : action_block_slice_begin;
2920 107 : }
2921 : else
2922 : {
2923 : // create a new action_block-slice
2924 42 : new_action_block_pos->begin_or_before_end=new_action_block_pos;
2925 42 : if (new_noninert_bunch->is_trivial())
2926 : { // Only during initialisation, it may happen that we add new non-inert
2927 37 : 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 5 : for (const action_block_entry* iter = action_block_begin;
2936 5 : iter < new_noninert_bunch->begin; ++iter)
2937 : {
2938 0 : assert(nullptr == iter->succ);
2939 0 : assert(nullptr == iter->begin_or_before_end);
2940 : }
2941 : }
2942 : #endif
2943 42 : ++nr_of_action_block_slices;
2944 : }
2945 :
2946 149 : /* adapt the out-slice */ assert(source != succ.front().block_bunch->pred->source);
2947 271 : if (source == new_succ_pos[-1].block_bunch->pred->source &&
2948 122 : new_succ_pos[-1].bunch() == new_noninert_bunch)
2949 : {
2950 : // the out-slice is suitable: extend it.
2951 81 : succ_entry* const out_slice_begin(
2952 81 : new_succ_pos[-1].begin_or_before_end); assert(nullptr != out_slice_begin);
2953 81 : assert(new_succ_pos - 1 == out_slice_begin->begin_or_before_end);
2954 81 : 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 81 : new_succ_pos->begin_or_before_end = out_slice_begin;
2957 81 : return became_bottom;
2958 : }
2959 : }
2960 : else
2961 : {
2962 : // create a new bunch for noninert transitions
2963 115 : new_noninert_bunch =
2964 : #ifdef USE_POOL_ALLOCATOR
2965 : storage.template construct<bunch_t>
2966 : #else
2967 : new bunch_t
2968 : #endif
2969 115 : (new_action_block_pos, action_block_inert_begin);
2970 115 : ++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(
2975 115 : splitter_list.emplace_back(
2976 115 : ONLY_IF_POOL_ALLOCATOR( storage, )
2977 115 : block_bunch_inert_begin, new_noninert_bunch, false));
2978 : #else
2979 : splitter_list.emplace_back(block_bunch_inert_begin,
2980 : new_noninert_bunch, false);
2981 : block_bunch_slice_iter_t new_noninert_block_bunch(
2982 : std::prev(splitter_list.end()));
2983 : #endif
2984 115 : ++nr_of_block_bunch_slices;
2985 115 : new_block_bunch_pos->slice = new_noninert_block_bunch;
2986 115 : *new_noninert_block_bunch_ptr = new_noninert_block_bunch;
2987 :
2988 : // create a new action_block-slice
2989 115 : new_action_block_pos->begin_or_before_end = new_action_block_pos;
2990 115 : ++nr_of_action_block_slices;
2991 183 : } 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 183 : new_succ_pos->begin_or_before_end = new_succ_pos;
2995 183 : return became_bottom;
2996 : }
2997 :
2998 :
2999 : public:
3000 : /// \brief Split all data structures after a new block has been created
3001 : /// \details This function splits the block_bunch- and action_block-slices
3002 : /// to reflect that some transitions now start or end in the new block.
3003 : /// They can no longer be in the same slice as the transitions that start
3004 : /// or end in the old block, respectively. It also marks the transitions
3005 : /// that have become non-inert as such and finds new bottom states.
3006 : ///
3007 : /// Its time complexity is O(1 + |in(new_block)| + |out(new_block)|).
3008 : /// \param new_block the new block
3009 : /// \param old_block the old block (from which new_block was split
3010 : /// off)
3011 : /// \param add_new_noninert_to_splitter indicates to which
3012 : /// block_bunch-slice new non-inert transitions
3013 : /// should be added: if this parameter is `false`,
3014 : /// a new slice is created; if it is `true`,
3015 : /// new non-inert transitions are added to
3016 : /// `splitter_T`. The latter can be done iff
3017 : /// `splitter_T` is the last block_bunch-slice
3018 : /// \param splitter_T the splitter that caused new_block and old_block
3019 : /// to separate from each other
3020 : /// \param new_block_mode indicates whether the new block is U or R
3021 : ONLY_IF_DEBUG( template<class LTS_TYPE> )
3022 1161 : void adapt_transitions_for_new_block(
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 1161 : { 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 1161 : permutation_entry* s_iter(new_block->begin); assert(s_iter < new_block->end);
3032 : do
3033 : {
3034 1986 : state_info_entry* const s(s_iter->st); assert(new_block == s->bl.ock);
3035 1986 : assert(s->pos == s_iter);
3036 : /* - - - - - - adapt part_tr.block_bunch - - - - - - */
3037 1986 : assert(s != succ.front().block_bunch->pred->source);
3038 1986 : for (succ_entry* succ_iter(s->succ_inert.begin);
3039 3862 : s == succ_iter[-1].block_bunch->pred->source; )
3040 : {
3041 1876 : 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 1876 : splitter_T); assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
3046 1876 : 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 1986 : assert(s != pred.front().target);
3052 1986 : for (pred_entry* pred_iter(s->pred_inert.begin);
3053 4467 : s == (--pred_iter)->target; )
3054 2481 : { assert(&pred.front() < pred_iter);
3055 2481 : assert(nullptr != pred_iter->action_block->succ);
3056 2481 : assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
3057 2481 : 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 1986 : while (++s_iter < new_block->end);
3061 :
3062 1161 : if (new_block_is_R == new_block_mode)
3063 568 : { 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 568 : new_block->stable_block_bunch.splice(
3067 : new_block->stable_block_bunch.begin(),
3068 568 : old_block->stable_block_bunch, splitter_T);
3069 593 : } 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 1161 : s_iter = new_block->begin; assert(s_iter < new_block->end);
3075 : do
3076 : {
3077 1986 : state_info_entry* const s(s_iter->st); assert(s->pos == s_iter); assert(s != pred.front().target);
3078 1986 : for (pred_entry* pred_iter(s->pred_inert.begin);
3079 4467 : s == (--pred_iter)->target; )
3080 2481 : { assert(&pred.front() < pred_iter);
3081 2481 : assert(nullptr != pred_iter->action_block->succ);
3082 2481 : assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
3083 2481 : 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 1986 : while (++s_iter < new_block->end);
3087 1161 : assert(0 == new_block->marked_size()); assert(0 == old_block->marked_size());
3088 1161 : /* - - - - - - find new non-inert transitions - - - - - - */ assert(1 + &block_bunch.back() - block_bunch_inert_begin ==
3089 : action_block_end - action_block_inert_begin);
3090 1161 : if (block_bunch_inert_begin <= &block_bunch.back())
3091 : {
3092 313 : block_bunch_slice_iter_or_null_t new_noninert_block_bunch;
3093 313 : if (add_new_noninert_to_splitter)
3094 : {
3095 78 : new_noninert_block_bunch = splitter_T;
3096 : }
3097 : else
3098 : {
3099 235 : new_noninert_block_bunch = nullptr;
3100 : }
3101 313 : if (new_block_is_U == new_block_mode)
3102 133 : { assert(old_block == new_block->end->st->bl.ock);
3103 133 : assert(new_block->end <= &partitioner.part_st.permutation.back());
3104 133 : permutation_entry* target_iter(new_block->begin); assert(target_iter < new_block->end);
3105 : do
3106 : {
3107 243 : state_info_entry* const s(target_iter->st); assert(s->pos == target_iter);
3108 : // check all incoming inert transitions of s, whether they
3109 243 : /* still start in new_block */ assert(s != pred.back().target);
3110 353 : for (pred_entry* pred_iter(s->pred_inert.begin);
3111 353 : s == pred_iter->target; ++pred_iter)
3112 110 : { assert(pred_iter < &pred.back());
3113 110 : assert(nullptr != pred_iter->action_block->succ);
3114 110 : state_info_entry* const t(pred_iter->source); assert(pred_iter->action_block->succ->block_bunch->pred == pred_iter);
3115 110 : assert(t->pos->st == t);
3116 110 : if (new_block != t->bl.ock)
3117 81 : { assert(old_block == t->bl.ock);
3118 81 : if (!make_noninert(pred_iter,
3119 : &new_noninert_block_bunch))
3120 : // make_noninert() may modify *pred_iter
3121 : {
3122 25 : 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 243 : while (++target_iter < new_block->end); assert(0 < old_block->bottom_size());
3129 : }
3130 : else
3131 180 : { assert(new_block_is_R == new_block_mode);
3132 180 : /* We have to be careful because make_noninert may move */ assert(&partitioner.part_st.permutation.front() < new_block->begin);
3133 180 : /* a state either forward (to the marked states) or */ assert(old_block == new_block->begin[-1].st->bl.ock);
3134 180 : /* back (to the bottom states). */ assert(0 < old_block->bottom_size());
3135 180 : for(permutation_entry* source_iter(new_block->nonbottom_begin);
3136 503 : source_iter < new_block->marked_nonbottom_begin; )
3137 : {
3138 323 : state_info_entry* const s(source_iter->st); assert(s->pos == source_iter);
3139 : // check all outgoing inert transitions of s, whether they
3140 323 : /* still end in new_block. */ assert(succ.back().block_bunch->pred->source != s);
3141 323 : succ_entry* succ_iter(s->succ_inert.begin); assert(succ_iter < &succ.back());
3142 323 : bool dont_mark(true); assert(s == succ_iter->block_bunch->pred->source);
3143 : do
3144 435 : { assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
3145 435 : if (new_block !=
3146 435 : succ_iter->block_bunch->pred->target->bl.ock)
3147 183 : { assert(old_block == succ_iter->block_bunch->pred->target->bl.ock);
3148 183 : dont_mark = make_noninert(
3149 183 : 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 435 : while (s == (++succ_iter)->block_bunch->pred->source);
3155 323 : if (dont_mark) ++source_iter;
3156 : else
3157 57 : { assert(s->pos == source_iter);
3158 57 : new_block->mark_nonbottom(source_iter);
3159 323 : } assert(new_block->nonbottom_begin <= source_iter);
3160 : // mCRL2complexity(s, ...) -- overapproximated by the call at the end
3161 : }
3162 : }
3163 848 : } else assert(block_bunch_inert_begin == 1 + &block_bunch.back());
3164 1161 : mCRL2complexity(new_block, add_work(bisim_gjkw::check_complexity::
3165 : adapt_transitions_for_new_block, bisim_gjkw::check_complexity::log_n -
3166 : bisim_gjkw::check_complexity::ilog2(new_block->size())), partitioner);
3167 1161 : }
3168 : #ifndef NDEBUG
3169 : /// \brief print all transitions
3170 : /// \details Transitions are printed organised into bunches.
3171 : template <class LTS_TYPE>
3172 2088 : void print_trans(const bisim_partitioner_dnj<LTS_TYPE>& partitioner) const
3173 : {
3174 2088 : if (!mCRL2logEnabled(log::debug)) return;
3175 : // print all outgoing transitions grouped per successor and out-slice
3176 0 : const succ_entry* succ_iter(&succ.cbegin()[1]);
3177 0 : if (succ_iter >= &succ.back())
3178 : {
3179 0 : mCRL2log(log::debug) << "No transitions.\n";
3180 0 : return;
3181 : }
3182 0 : const state_info_entry* source(succ_iter->block_bunch->pred->source);
3183 0 : mCRL2log(log::debug) << source->debug_id(partitioner)
3184 0 : << ":\n";
3185 0 : block_bunch_slice_iter_or_null_t current_out_bunch(
3186 0 : const_cast<part_trans_t*>(this)->splitter_list.end());
3187 : do
3188 : {
3189 0 : if (source != succ_iter->block_bunch->pred->source)
3190 0 : { assert(source < succ_iter->block_bunch->pred->source);
3191 0 : source = succ_iter->block_bunch->pred->source;
3192 0 : mCRL2log(log::debug)
3193 0 : << source->debug_id(partitioner) << ":\n";
3194 0 : current_out_bunch =
3195 0 : const_cast<part_trans_t*>(this)->splitter_list.end();
3196 : }
3197 0 : if (succ_iter->block_bunch->slice != current_out_bunch)
3198 0 : { assert(!current_out_bunch.is_null());
3199 0 : if (succ_iter->block_bunch->slice.is_null())
3200 0 : { assert(succ_iter == source->succ_inert.begin);
3201 0 : mCRL2log(log::debug)<<"\tInert successors:\n";
3202 0 : current_out_bunch = nullptr;
3203 : }
3204 : else
3205 0 : { assert(succ_iter < source->succ_inert.begin);
3206 0 : assert(!current_out_bunch.is_null());
3207 0 : assert(current_out_bunch == splitter_list.end() ||
3208 : current_out_bunch->bunch != succ_iter->bunch());
3209 0 : mCRL2log(log::debug) << "\tSuccessors in "
3210 0 : <<succ_iter->bunch()->debug_id_short(partitioner)<<":\n";
3211 0 : current_out_bunch = succ_iter->block_bunch->slice;
3212 : }
3213 : }
3214 0 : mCRL2log(log::debug) << "\t\t"
3215 0 : << succ_iter->block_bunch->pred->debug_id(partitioner) << '\n';
3216 : }
3217 0 : while (++succ_iter < &succ.back());
3218 :
3219 : // print all transitions grouped per bunch and action_block-slice
3220 0 : const action_block_entry* action_block_iter(action_block_begin);
3221 0 : do assert(action_block_iter < action_block_end);
3222 0 : while (nullptr == action_block_iter->succ &&
3223 0 : (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 0 : assert(nullptr != action_block_iter->succ);
3230 0 : if (action_block_iter->succ->block_bunch->slice.is_null())
3231 0 : { assert(action_block_iter == action_block_inert_begin);
3232 0 : mCRL2log(log::debug) <<"Inert transition slice [";
3233 0 : action_block_slice_end = bunch_end = action_block_end;
3234 : }
3235 : else
3236 : {
3237 0 : const bunch_t* const bunch(action_block_iter->succ->bunch());
3238 0 : assert(nullptr != bunch);
3239 0 : mCRL2log(log::debug) << bunch->debug_id_short(
3240 0 : partitioner) << ":\n\taction_block-slice [";
3241 0 : assert(bunch->begin == action_block_iter);
3242 0 : bunch_end = bunch->end;
3243 0 : assert(bunch_end <= action_block_inert_begin);
3244 0 : assert(nullptr != action_block_iter->begin_or_before_end);
3245 0 : action_block_slice_end =
3246 0 : action_block_iter->begin_or_before_end + 1;
3247 : }
3248 0 : assert(action_block_slice_end <= bunch_end);
3249 : // for all action_block-slices in bunch
3250 : for (;;)
3251 : {
3252 0 : mCRL2log(log::debug) << (action_block_iter -
3253 0 : action_block_begin) << ","
3254 0 : << (action_block_slice_end - action_block_begin) << "):\n";
3255 : // for all transitions in the action_block-slice
3256 0 : assert(action_block_iter < action_block_slice_end);
3257 : do
3258 : {
3259 0 : assert(nullptr != action_block_iter->succ);
3260 0 : mCRL2log(log::debug) << "\t\t"
3261 0 : << action_block_iter->succ->block_bunch->
3262 0 : pred->debug_id(partitioner) << '\n';
3263 : }
3264 0 : while (++action_block_iter < action_block_slice_end);
3265 : // go to next action_block-slice in the same bunch
3266 0 : while (action_block_iter < bunch_end &&
3267 0 : nullptr == action_block_iter->succ)
3268 : {
3269 0 : assert(nullptr == action_block_iter->begin_or_before_end);
3270 0 : ++action_block_iter;
3271 0 : assert(action_block_iter < bunch_end);
3272 : }
3273 0 : if (action_block_iter >= bunch_end) break;
3274 0 : assert(nullptr != action_block_iter->begin_or_before_end);
3275 0 : action_block_slice_end =
3276 0 : action_block_iter->begin_or_before_end + 1;
3277 0 : mCRL2log(log::debug) << "\taction_block-slice [";
3278 : }
3279 : // go to next bunch
3280 0 : assert(action_block_iter == bunch_end);
3281 0 : while (action_block_iter < action_block_end &&
3282 0 : nullptr == action_block_iter->succ)
3283 : {
3284 0 : assert(nullptr == action_block_iter->begin_or_before_end);
3285 0 : ++action_block_iter;
3286 : }
3287 : }
3288 0 : while (action_block_iter < action_block_end);
3289 : }
3290 : #endif
3291 : };
3292 :
3293 :
3294 : /// \brief refine a block
3295 : /// \details This function is called after a refinement function has found
3296 : /// where to split the block into unmarked (U) and marked (R) states.
3297 : /// It creates a new block for the smaller subblock.
3298 : /// \param new_block_mode indicates whether the U- or the R-block should be
3299 : /// the new one. (This parameter is necessary in case
3300 : /// the two halves have exactly the same size.)
3301 : /// \param storage (only if one uses the pool allocator) reference to
3302 : /// the pool allocator where the new block is placed
3303 : /// \param new_seqnr is the sequence number of the new block
3304 : /// \returns pointer to the new block
3305 : ONLY_IF_DEBUG( template<class LTS_TYPE> )
3306 1161 : inline 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, )
3308 : ONLY_IF_POOL_ALLOCATOR(
3309 : my_pool<simple_list<block_bunch_slice_t>::entry>& storage, )
3310 : state_type const new_seqnr)
3311 1161 : { assert(0 < marked_size()); assert(0 < unmarked_bottom_size());
3312 : // create a new block
3313 : block_t* new_block;
3314 1161 : state_type swapcount(std::min(marked_bottom_size(),
3315 1161 : unmarked_nonbottom_size()));
3316 1161 : if (permutation_entry* const splitpoint(marked_bottom_begin +
3317 1161 : unmarked_nonbottom_size()); assert(begin < splitpoint), assert(splitpoint < end),
3318 1161 : assert(splitpoint->st->pos == splitpoint),
3319 : new_block_is_U == new_block_mode)
3320 593 : { 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 593 : (begin, splitpoint, new_seqnr);
3328 593 : new_block->nonbottom_begin = marked_bottom_begin;
3329 :
3330 : // adapt the old block: it only keeps the R-states
3331 593 : begin = splitpoint;
3332 593 : nonbottom_begin = marked_nonbottom_begin;
3333 : }
3334 : else
3335 568 : { 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 568 : (splitpoint, end, new_seqnr);
3343 568 : 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 568 : end = splitpoint;
3347 568 : nonbottom_begin = marked_bottom_begin;
3348 1161 : } 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 1161 : if (0 < swapcount)
3363 : {
3364 : // vector swap the states:
3365 107 : permutation_entry* pos1(marked_bottom_begin);
3366 107 : permutation_entry* pos2(marked_nonbottom_begin); assert(pos1 < pos2);
3367 107 : permutation_entry const temp(std::move(*pos1));
3368 : for (;;)
3369 : {
3370 128 : --pos2; assert(pos1 < pos2);
3371 128 : *pos1 = std::move(*pos2);
3372 128 : ++pos1;
3373 128 : if (0 >= --swapcount) { break; } assert(pos1 < pos2);
3374 21 : *pos2 = std::move(*pos1); // mCRL2complexity(new_block_is_U == new_block_mode ? pos1[-1] : *pos2, ...)
3375 : } // -- overapproximated by the call at the end
3376 107 : *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 1161 : { const permutation_entry* s_iter(begin); assert(s_iter < end);
3380 6805 : do assert(s_iter->st->pos == s_iter);
3381 6805 : while (++s_iter < end); }
3382 : #endif
3383 : // unmark all states in both blocks
3384 1161 : marked_nonbottom_begin = end;
3385 1161 : marked_bottom_begin = nonbottom_begin;
3386 1161 : new_block->marked_bottom_begin = new_block->nonbottom_begin; assert(new_block->size() <= size());
3387 :
3388 1161 : /* set the block pointer of states in the new block */ assert(new_block->marked_nonbottom_begin == new_block->end);
3389 1161 : permutation_entry* s_iter(new_block->begin); assert(s_iter < new_block->end);
3390 : do
3391 1986 : { assert(s_iter->st->pos == s_iter);
3392 1986 : s_iter->st->bl.ock = new_block; // mCRL2complexity (*s_iter, ...) -- subsumed in the call below
3393 : }
3394 1986 : 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 -
3396 : bisim_gjkw::check_complexity::ilog2(new_block->size())),
3397 : partitioner);
3398 1161 : return new_block;
3399 : }
3400 :
3401 :
3402 : /// \brief split off a single action_block-slice from the bunch
3403 : /// \details The function splits the current bunch after its first
3404 : /// action_block-slice or before its last action_block-slice, whichever is
3405 : /// smaller. It creates a new bunch for the split-off slice and returns a
3406 : /// pointer to the new bunch. The caller has to adapt the block_bunch-slices.
3407 : /// \param part_tr the data structure containing information about the
3408 : /// partition of transitions (needed to find the list of
3409 : /// non-trivial bunches)
3410 : /// \returns pointer to a new bunch containing one small action_block-slice
3411 : /// that was originally in this bunch
3412 1424 : inline bunch_t* bunch_t::split_off_small_action_block_slice(
3413 : part_trans_t& part_tr)
3414 1424 : { assert(begin < end); assert(nullptr != begin->succ);
3415 1424 : assert(nullptr != begin->begin_or_before_end);
3416 1424 : 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 1424 : 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 1424 : /* 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 1424 : /* |T--a-->B'| < 1/2 |T| */ assert(nullptr != last_slice_begin->succ);
3421 1424 : 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 375 : (last_slice_begin, end); assert(nullptr != bunch_T_a_Bprime);
3431 375 : end = last_slice_begin;
3432 481 : while (nullptr == end[-1].succ)
3433 : {
3434 106 : --end; assert(first_slice_end <= end); assert(nullptr == end->begin_or_before_end);
3435 375 : } assert(nullptr != end[-1].begin_or_before_end);
3436 375 : 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 1049 : (begin, first_slice_end); assert(nullptr != bunch_T_a_Bprime);
3448 1049 : begin = first_slice_end;
3449 1653 : while (nullptr == begin->succ)
3450 604 : { assert(nullptr == begin->begin_or_before_end);
3451 604 : ++begin; assert(begin <= last_slice_begin);
3452 1049 : } assert(nullptr != begin->begin_or_before_end);
3453 1049 : if (begin == last_slice_begin) part_tr.make_trivial(this);
3454 1424 : } ONLY_IF_DEBUG( bunch_T_a_Bprime->work_counter = work_counter; )
3455 1424 : ++part_tr.nr_of_bunches;
3456 1424 : return bunch_T_a_Bprime;
3457 : }
3458 : ///@} (end of group part_trans)
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 :
3476 : /// \defgroup part_refine
3477 : /// \brief classes to calculate the stutter equivalence quotient of a LTS
3478 : ///@{
3479 :
3480 :
3481 :
3482 : /*=============================================================================
3483 : = main class =
3484 : =============================================================================*/
3485 :
3486 :
3487 :
3488 :
3489 :
3490 : /// \class bisim_partitioner_dnj
3491 : /// \brief implements the main algorithm for the branching bisimulation
3492 : /// quotient
3493 : template <class LTS_TYPE>
3494 : class bisim_partitioner_dnj
3495 : {
3496 : private:
3497 : /// \brief modes that determine details of how split() should work
3498 : enum refine_mode_t{extend_from_marked_states,
3499 : extend_from_marked_states__add_new_noninert_to_splitter,
3500 : extend_from_splitter };
3501 :
3502 : /// \brief automaton that is being reduced
3503 : LTS_TYPE& aut;
3504 : ONLY_IF_DEBUG( public: )
3505 : /// \brief partition of the state space into blocks
3506 : bisim_dnj::part_state_t part_st;
3507 :
3508 : /// \brief partitions of the transitions (with bunches and
3509 : /// action_block-slices)
3510 : bisim_dnj::part_trans_t part_tr;
3511 : private:
3512 : /// \brief action label slices
3513 : /// \details In part_tr.action_block, no information about the action label
3514 : /// is actually stored with the transitions, to save memory. Entry l of
3515 : /// this array contains a pointer to the first entry in
3516 : /// part_tr.action_block with label l.
3517 : ///
3518 : /// During initialisation, entry l of this array contains a counter to
3519 : /// indicate how many non-inert transitions with action label l have been
3520 : /// found.
3521 : bisim_gjkw::fixed_vector<bisim_dnj::iterator_or_counter<
3522 : bisim_dnj::action_block_entry*> > action_label;
3523 : ONLY_IF_DEBUG( public: )
3524 : /// \brief true iff branching (not strong) bisimulation has been requested
3525 : bool const branching;
3526 : private:
3527 : /// \brief true iff divergence-preserving branching bisimulation has been
3528 : /// requested
3529 : /// \details Note that this field must be false if strong bisimulation has
3530 : /// been requested. There is no such thing as divergence-preserving strong
3531 : /// bisimulation.
3532 : bool const preserve_divergence;
3533 : #ifndef NDEBUG
3534 : friend class bisim_dnj::pred_entry;
3535 : friend class bisim_dnj::bunch_t;
3536 : #endif
3537 : public:
3538 : /// \brief constructor
3539 : /// \details The constructor constructs the data structures and immediately
3540 : /// calculates the partition corresponding with the bisimulation quotient.
3541 : /// It destroys the transitions on the LTS (to save memory) but does not
3542 : /// adapt the LTS to represent the quotient's transitions.
3543 : /// \param new_aut LTS that needs to be reduced
3544 : /// \param new_branching If true branching bisimulation is used,
3545 : /// otherwise strong bisimulation is
3546 : /// applied.
3547 : /// \param new_preserve_divergence If true and branching is true, preserve
3548 : /// tau loops on states.
3549 333 : bisim_partitioner_dnj(LTS_TYPE& new_aut, bool const new_branching = false,
3550 : bool const new_preserve_divergence = false)
3551 333 : : aut(new_aut),
3552 333 : part_st(new_aut.num_states()),
3553 333 : part_tr(new_aut.num_transitions(), new_aut.num_action_labels()),
3554 333 : action_label(new_aut.num_action_labels()),
3555 333 : branching(new_branching),
3556 333 : preserve_divergence(new_preserve_divergence)
3557 333 : { assert(branching || !preserve_divergence);
3558 333 : create_initial_partition(); ONLY_IF_DEBUG( part_tr.action_block_orig_inert_begin =
3559 : part_tr.action_block_inert_begin; )
3560 333 : refine_partition_until_it_becomes_stable();
3561 333 : }
3562 :
3563 :
3564 : /// \brief Calculate the number of equivalence classes
3565 : /// \details The number of equivalence classes (which is valid after the
3566 : /// partition has been constructed) is equal to the number of states in the
3567 : /// bisimulation quotient.
3568 1416 : state_type num_eq_classes() const
3569 : {
3570 1416 : return part_st.nr_of_blocks;
3571 : }
3572 :
3573 :
3574 : /// \brief Get the equivalence class of a state
3575 : /// \details After running the minimisation algorithm, this function
3576 : /// produces the number of the equivalence class of a state. This number
3577 : /// is the same as the number of the state in the minimised LTS to which
3578 : /// the original state is mapped.
3579 : /// \param s state whose equivalence class needs to be found
3580 : /// \returns sequence number of the equivalence class of state s
3581 1605 : state_type get_eq_class(state_type const s) const
3582 : {
3583 1605 : return part_st.block(s)->seqnr;
3584 : }
3585 :
3586 :
3587 : /// \brief Adapt the LTS after minimisation
3588 : /// \details After the efficient branching bisimulation minimisation, the
3589 : /// information about the quotient LTS is only stored in the partition data
3590 : /// structure of the partitioner object. This function exports the
3591 : /// information back to the LTS by adapting its states and transitions: it
3592 : /// updates the number of states and adds those transitions that are
3593 : /// mandated by the partition data structure. If desired, it also creates
3594 : /// a vector containing an arbritrary (example) original state per
3595 : /// equivalence class.
3596 : ///
3597 : /// The main parameter and return value are implicit with this function: a
3598 : /// reference to the LTS was stored in the object by the constructor.
3599 317 : void finalize_minimized_LTS()
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
3606 : const bisim_dnj::permutation_entry*
3607 317 : s_iter(&part_st.permutation.front()); assert(s_iter <= &part_st.permutation.back());
3608 : do
3609 : {
3610 1450 : const bisim_dnj::block_t* const B(s_iter->st->bl.ock);
3611 : // for all block_bunch-slices of the block
3612 5094 : for (const bisim_dnj::block_bunch_slice_t& block_bunch :
3613 : B->stable_block_bunch)
3614 2194 : { assert(block_bunch.is_stable()); assert(!block_bunch.empty());
3615 : const bisim_dnj::pred_entry* const
3616 2194 : pred(block_bunch.end[-1].pred); assert(pred->source->bl.ock == B);
3617 2194 : assert(nullptr != pred->action_block->succ);
3618 2194 : /* add a transition from the source block to the goal block */ assert(pred->action_block->succ->block_bunch->pred == pred);
3619 2194 : /* with the indicated label. */ assert(pred->action_block->succ->block_bunch->slice == &block_bunch);
3620 : label_type const
3621 2194 : label(block_bunch.bunch->next_nontrivial_and_label.label); assert(0 <= label); assert(label < action_label.size());
3622 2194 : aut.add_transition(transition(B->seqnr, label,
3623 2194 : pred->target->bl.ock->seqnr));
3624 : }
3625 1450 : s_iter = B->end;
3626 : }
3627 1450 : 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 317 : 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 */
3636 : bisim_gjkw::fixed_vector<typename LTS_TYPE::state_label_t>
3637 180 : new_labels(num_eq_classes());
3638 :
3639 180 : state_type i(aut.num_states()); assert(0 < i);
3640 : do
3641 : {
3642 1232 : --i;
3643 1232 : const state_type new_index(get_eq_class(i));
3644 1232 : new_labels[new_index]=new_labels[new_index]+aut.state_label(i);
3645 : }
3646 1232 : while (0 < i);
3647 :
3648 180 : aut.set_num_states(num_eq_classes());
3649 180 : i = 0; assert(i < num_eq_classes());
3650 : do
3651 : {
3652 739 : aut.set_state_label(i, new_labels[i]);
3653 : }
3654 739 : while (++i < num_eq_classes());
3655 180 : }
3656 : else
3657 : {
3658 137 : aut.set_num_states(num_eq_classes());
3659 : }
3660 :
3661 317 : aut.set_initial_state(get_eq_class(aut.initial_state()));
3662 317 : }
3663 :
3664 :
3665 : /// \brief Check whether two states are in the same equivalence class.
3666 : /// \param s first state that needs to be compared.
3667 : /// \param t second state that needs to be compared.
3668 : /// \returns true iff the two states are in the same equivalence class.
3669 16 : bool in_same_class(state_type const s, state_type const t) const
3670 : {
3671 16 : return part_st.block(s) == part_st.block(t);
3672 : }
3673 : private:
3674 :
3675 : /*--------------------------- main algorithm ----------------------------*/
3676 :
3677 : /// \brief Create a partition satisfying the main invariant
3678 : /// \details Before the actual bisimulation minimisation can start, this
3679 : /// function needs to be called to create a partition that satisfies the
3680 : /// main invariant of the efficient O(m log n) branching bisimulation
3681 : /// minimisation.
3682 : ///
3683 : /// It puts all non-inert transitions into a single bunch, containing one
3684 : /// action_block-slice for each action label. It creates a single block
3685 : /// (or possibly two, if there are states that never will do any visible
3686 : /// action). As a side effect, it deletes all transitions from the LTS
3687 : /// that is stored with the partitioner; information about the transitions
3688 : /// is kept in data structures that are suitable for the efficient
3689 : /// algorithm.
3690 : ///
3691 : /// For divergence-preserving branching bisimulation, we only need to treat
3692 : /// tau-self-loops as non-inert transitions. In other texts, this is
3693 : /// sometimes described as temporarily renaming the tau-self-loops to
3694 : /// self-loops with a special label. However, as there are no other
3695 : /// non-inert tau transitions, we can simply put them in their own
3696 : /// action_block-slice, separate from the inert tau transitions. (It would
3697 : /// be an error to mix the inert transitions with the self-loops in the
3698 : /// same slice.)
3699 333 : void create_initial_partition()
3700 : {
3701 333 : mCRL2log(log::verbose) << "An O(m log n) "
3702 0 : << (branching ? (preserve_divergence
3703 0 : ? "divergence-preserving branching "
3704 : : "branching ")
3705 : : "")
3706 0 : << "bisimulation partitioner created for " << part_st.state_size()
3707 0 : << " states and " << aut.num_transitions() << " transitions.\n";
3708 :
3709 333 : if (part_st.state_size() > 2 * aut.num_transitions() + 1)
3710 : {
3711 0 : 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
3718 : bisim_dnj::block_t* B(
3719 : #ifdef USE_POOL_ALLOCATOR
3720 : part_tr.storage.template construct<bisim_dnj::block_t>
3721 : #else
3722 : new bisim_dnj::block_t
3723 : #endif
3724 333 : (&part_st.permutation.front(),
3725 333 : 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 333 : assert(action_label.size() == aut.num_action_labels());
3736 : // counter for the total number of inert transitions:
3737 333 : trans_type inert_transitions(0);
3738 3377 : for (const transition& t: aut.get_transitions())
3739 : {
3740 3647 : if (branching&&aut.is_tau(aut.apply_hidden_label_map(t.label()))&& ((
3741 603 : t.from() != t.to()) || (assert(preserve_divergence), false)))
3742 : {
3743 : // The transition is inert.
3744 533 : ++part_st.state_info[t.from()].succ_inert.count;
3745 533 : ++inert_transitions;
3746 :
3747 : // The source state should become non-bottom:
3748 533 : if (part_st.state_info[t.from()].pos < B->nonbottom_begin)
3749 : {
3750 413 : std::swap(*part_st.state_info[t.from()].pos,
3751 413 : *--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 2511 : ++part_st.state_info[t.from()].untested_to_U_eqv.count;
3759 2511 : ++action_label[aut.apply_hidden_label_map(t.label())].count;
3760 : }
3761 3044 : ++part_st.state_info[t.to()].pred_inert.count;
3762 : }
3763 : // Now we update the marked_bottom_begin pointer:
3764 333 : B->marked_bottom_begin = B->nonbottom_begin;
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 333 : bisim_dnj::pred_entry* next_pred_begin(&part_tr.pred.begin()[1]);
3773 333 : bisim_dnj::succ_entry* next_succ_begin(&part_tr.succ.begin()[1]);
3774 333 : bisim_dnj::state_info_entry* state_iter(&part_st.state_info.front()); assert(state_iter <= &part_st.state_info.back());
3775 : do
3776 : {
3777 2318 : state_iter->bl.ed_noninert_end = next_pred_begin;
3778 2318 : next_pred_begin += state_iter->pred_inert.count;
3779 2318 : state_iter->pred_inert.convert_to_iterator(next_pred_begin);
3780 :
3781 : // create slice descriptors in part_tr.succ for each state with
3782 2318 : /* outgoing transitions. */ assert(nullptr != next_succ_begin);
3783 2318 : state_iter->untested_to_U_eqv.convert_to_iterator(
3784 2318 : next_succ_begin + state_iter->untested_to_U_eqv.count);
3785 2318 : if (next_succ_begin < state_iter->untested_to_U_eqv.begin)
3786 1586 : { assert(nullptr != state_iter->untested_to_U_eqv.begin);
3787 1586 : next_succ_begin->begin_or_before_end =
3788 1586 : state_iter->untested_to_U_eqv.begin - 1;
3789 1586 : for (bisim_dnj::succ_entry* const
3790 1586 : out_slice_begin(next_succ_begin);
3791 2511 : ++next_succ_begin < state_iter->untested_to_U_eqv.begin; )
3792 : {
3793 925 : 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 1586 : B->mark(state_iter->pos);
3797 : }
3798 2318 : state_iter->succ_inert.convert_to_iterator(next_succ_begin +
3799 2318 : state_iter->succ_inert.count);
3800 : #ifndef NDEBUG
3801 2851 : while (next_succ_begin < state_iter->succ_inert.begin)
3802 533 : { assert(nullptr == next_succ_begin->begin_or_before_end);
3803 533 : ++next_succ_begin;
3804 : }
3805 : #endif
3806 2318 : next_succ_begin = state_iter->succ_inert.begin; // mCRL2complexity(*state_iter, ...) -- subsumed in the call at the end
3807 : }
3808 2318 : while (++state_iter <= &part_st.state_info.back());
3809 :
3810 : // Line 2.4: Pi_t := { { all non-inert transitions } }
3811 333 : part_tr.action_block_inert_begin =
3812 333 : part_tr.action_block_end - inert_transitions; assert(part_tr.action_block_begin <= part_tr.action_block_inert_begin);
3813 333 : part_tr.block_bunch_inert_begin =
3814 333 : 1 + &part_tr.block_bunch.back() - inert_transitions; assert(1 + &part_tr.block_bunch.front() <= part_tr.block_bunch_inert_begin);
3815 333 : bisim_dnj::bunch_t* bunch(nullptr);
3816 :
3817 333 : if (1 + &part_tr.block_bunch.front() < part_tr.block_bunch_inert_begin)
3818 331 : { assert(part_tr.action_block_begin < part_tr.action_block_inert_begin);
3819 : // create a single bunch containing all non-inert transitions
3820 331 : bunch =
3821 : #ifdef USE_POOL_ALLOCATOR
3822 : part_tr.storage.template construct<bisim_dnj::bunch_t>
3823 : #else
3824 : new bisim_dnj::bunch_t
3825 : #endif
3826 662 : (part_tr.action_block_begin,
3827 331 : part_tr.action_block_inert_begin); assert(nullptr != bunch); assert(part_tr.splitter_list.empty());
3828 331 : ++part_tr.nr_of_bunches; assert(1 == part_tr.nr_of_bunches);
3829 :
3830 : // create a single block_bunch entry for all non-inert transitions
3831 331 : part_tr.splitter_list.emplace_front(
3832 331 : ONLY_IF_POOL_ALLOCATOR( part_tr.storage, )
3833 331 : part_tr.block_bunch_inert_begin, bunch, false); assert(!part_tr.splitter_list.empty());
3834 331 : ++part_tr.nr_of_block_bunch_slices; assert(1 == part_tr.nr_of_block_bunch_slices);
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 333 : /* 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);
3847 : bisim_dnj::action_block_entry*
3848 333 : next_action_label_begin(part_tr.action_block_begin);
3849 333 : trans_type const n_square(part_st.state_size() * part_st.state_size()); ONLY_IF_DEBUG( trans_type max_transitions = n_square; )
3850 333 : label_type label(action_label.size()); assert(0 < label);
3851 : do
3852 : {
3853 1284 : --label;
3854 1284 : if (0 < action_label[label].count)
3855 1026 : { assert(nullptr != bunch);
3856 1026 : if (++part_tr.nr_of_action_block_slices == 2)
3857 : {
3858 : // This is the second action_block-slice, so the bunch is
3859 : // not yet marked as nontrivial but it should be.
3860 289 : part_tr.make_nontrivial(bunch);
3861 : }
3862 1026 : if (n_square < action_label[label].count)
3863 : {
3864 4 : mCRL2log(log::warning) << "There are "
3865 2 : << action_label[label].count << ' '
3866 4 : << pp(aut.action_label(label)) << "-transitions. "
3867 2 : "This is more than n^2 (= " << n_square << "). It is "
3868 : "not guaranteed that branching bisimulation "
3869 2 : "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 1026 : action_label[label].convert_to_iterator(
3875 1026 : next_action_label_begin + action_label[label].count);
3876 1026 : next_action_label_begin->begin_or_before_end =
3877 1026 : action_label[label].begin - 1; assert(nullptr != next_action_label_begin->begin_or_before_end);
3878 : bisim_dnj::action_block_entry* const
3879 1026 : action_block_slice_begin(next_action_label_begin); assert(nullptr != action_block_slice_begin);
3880 2511 : while (++next_action_label_begin < action_label[label].begin)
3881 : {
3882 1485 : 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 258 : action_label[label].convert_to_iterator(
3889 : next_action_label_begin);
3890 258 : if (0 != label && aut.num_transitions() < action_label.size())
3891 : {
3892 8 : mCRL2log(log::warning) << "Action label "
3893 4 : << 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 2235 : while (0 < label && (/* insert a dummy entry */ assert(next_action_label_begin < part_tr.action_block_inert_begin),
3902 951 : next_action_label_begin->succ = nullptr,
3903 951 : next_action_label_begin->begin_or_before_end = nullptr,
3904 333 : ++next_action_label_begin, true)); assert(next_action_label_begin == part_tr.action_block_inert_begin);
3905 :
3906 333 : /* distribute the transitions over the data structures */ ONLY_IF_DEBUG( bisim_gjkw::check_complexity::init(2 * max_transitions); )
3907 :
3908 : bisim_dnj::block_bunch_entry*
3909 333 : next_block_bunch(1 + &part_tr.block_bunch.front());
3910 3377 : for (const transition& t: aut.get_transitions())
3911 : {
3912 : bisim_dnj::state_info_entry* const
3913 3044 : source(&part_st.state_info.front() + t.from());
3914 : bisim_dnj::state_info_entry* const
3915 3044 : 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 3647 : if (branching&&aut.is_tau(aut.apply_hidden_label_map(t.label()))&& ((
3922 603 : 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 533 : succ_pos = --source->succ_inert.begin; assert(nullptr == succ_pos->begin_or_before_end);
3928 533 : block_bunch_pos = 1 + &part_tr.block_bunch.back() -
3929 533 : inert_transitions; assert(block_bunch_pos >= part_tr.block_bunch_inert_begin);
3930 533 : pred_pos = --target->pred_inert.begin; assert(block_bunch_pos->slice.is_null());
3931 533 : action_block_pos = part_tr.action_block_end-inert_transitions; assert(action_block_pos >= part_tr.action_block_inert_begin);
3932 533 : action_block_pos->begin_or_before_end = nullptr;
3933 533 : --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 2511 : succ_pos =
3941 2511 : --part_st.state_info[t.from()].untested_to_U_eqv.begin; assert(nullptr != succ_pos->begin_or_before_end);
3942 2511 : assert(nullptr != succ_pos->begin_or_before_end->begin_or_before_end);
3943 2511 : assert(succ_pos->begin_or_before_end <= succ_pos ||
3944 : succ_pos->begin_or_before_end->begin_or_before_end == succ_pos);
3945 2511 : block_bunch_pos = next_block_bunch++; assert(block_bunch_pos < part_tr.block_bunch_inert_begin);
3946 2511 : pred_pos = target->bl.ed_noninert_end++;
3947 2511 : action_block_pos =
3948 2511 : --action_label[aut.apply_hidden_label_map(t.label())].begin; assert(nullptr != action_block_pos->begin_or_before_end);
3949 2511 : assert(nullptr != action_block_pos->begin_or_before_end->begin_or_before_end);
3950 2511 : 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 2511 : assert(!part_tr.splitter_list.empty());
3954 2511 : block_bunch_pos->slice = part_tr.splitter_list.begin(); assert(action_block_pos < part_tr.action_block_inert_begin);
3955 3044 : } assert(target->bl.ed_noninert_end <= target->pred_inert.begin);
3956 3044 : succ_pos->block_bunch = block_bunch_pos;
3957 3044 : block_bunch_pos->pred = pred_pos;
3958 3044 : pred_pos->action_block = action_block_pos;
3959 3044 : pred_pos->source = source;
3960 3044 : pred_pos->target = target; assert(nullptr != succ_pos);
3961 3044 : action_block_pos->succ = succ_pos; // mCRL2complexity(pred_pos, ...) -- subsumed in the call at the end
3962 333 : } assert(0 == inert_transitions);
3963 333 : /* 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 333 : aut.clear_transitions();
3966 :
3967 333 : state_iter = &part_st.state_info.front(); assert(state_iter <= &part_st.state_info.back());
3968 : do
3969 : {
3970 2318 : state_iter->bl.ock = B;
3971 : }
3972 2318 : while (++state_iter <= &part_st.state_info.back());
3973 :
3974 333 : if (nullptr != bunch)
3975 : {
3976 338 : while (nullptr == bunch->begin->succ)
3977 7 : { assert(nullptr == bunch->begin->begin_or_before_end);
3978 7 : ++bunch->begin; assert(bunch->begin < bunch->end);
3979 331 : } assert(nullptr != bunch->begin->begin_or_before_end);
3980 576 : while (nullptr == bunch->end[-1].succ)
3981 245 : { assert(nullptr == bunch->end[-1].begin_or_before_end);
3982 245 : --bunch->end; assert(bunch->begin < bunch->end);
3983 331 : } assert(nullptr != bunch->end[-1].begin_or_before_end);
3984 :
3985 331 : /* 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 331 : if (0 < B->marked_size())
3993 331 : { ONLY_IF_DEBUG( part_st.print_part(*this);
3994 : part_tr.print_trans(*this); )
3995 : bisim_dnj::block_bunch_slice_iter_t slice =
3996 331 : part_tr.splitter_list.begin();
3997 331 : if (1 < B->size())
3998 : {
3999 318 : B = split(B, /* splitter block_bunch */ slice,
4000 : extend_from_marked_states__add_new_noninert_to_splitter);
4001 : // We can ignore possible new non-inert transitions, as
4002 : // every R-bottom state already has a transition in bunch.
4003 318 : B->marked_nonbottom_begin = B->end;
4004 : }
4005 : else
4006 13 : { assert(B->nonbottom_begin == B->end);
4007 13 : /* 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.
4009 13 : B->stable_block_bunch.splice(B->stable_block_bunch.end(),
4010 13 : part_tr.splitter_list, slice);
4011 13 : slice->make_stable();
4012 331 : } assert(!B->stable_block_bunch.empty()); assert(part_tr.splitter_list.empty());
4013 331 : assert(B->stable_block_bunch.front().end <= part_tr.block_bunch_inert_begin);
4014 331 : assert(1 + &part_tr.block_bunch.front() < B->stable_block_bunch.front().end);
4015 331 : B->marked_bottom_begin = B->nonbottom_begin; assert(!B->stable_block_bunch.front().empty());
4016 : }
4017 2 : } else assert(0 == B->marked_size());
4018 333 : }
4019 : #ifndef NDEBUG
4020 : /// \brief assert that the data structure is consistent and stable
4021 : /// \details The data structure is tested against a large number of
4022 : /// assertions to ensure that everything is consistent, e. g. pointers that
4023 : /// should point to successors of state s actually point to a transition
4024 : /// that starts in s.
4025 : ///
4026 : /// Additionally, it is asserted that the partition is stable. i. e. every
4027 : /// bottom state in every block can reach exactly every bunch in the list
4028 : /// of bunches that should be reachable from it, and every nonbottom state
4029 : /// can reach a subset of them.
4030 1757 : void assert_stability() const
4031 : {
4032 1757 : part_st.assert_consistency(*this);
4033 :
4034 1757 : assert(part_tr.succ.size() == part_tr.block_bunch.size() + 1);
4035 1757 : assert(part_tr.pred.size() == part_tr.block_bunch.size() + 1);
4036 1757 : assert((size_t)(part_tr.action_block_end-part_tr.action_block_begin) ==
4037 : part_tr.block_bunch.size() + action_label.size() - 2);
4038 1757 : if (part_tr.block_bunch.empty()) return;
4039 :
4040 1757 : 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 1757 : trans_type true_nr_of_block_bunch_slices(0);
4047 : // for all blocks
4048 : const bisim_dnj::permutation_entry*
4049 1757 : perm_iter(&part_st.permutation.front());
4050 1757 : assert(perm_iter <= &part_st.permutation.back());
4051 : do
4052 : {
4053 11537 : const bisim_dnj::block_t* const block(perm_iter->st->bl.ock);
4054 23074 : unsigned const max_block(bisim_gjkw::check_complexity::log_n -
4055 11537 : bisim_gjkw::check_complexity::ilog2(block->size()));
4056 : // iterators have no predefined hash, so we store pointers:
4057 : std::unordered_set<const bisim_dnj::block_bunch_slice_t*>
4058 11537 : 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 42482 : for (const bisim_dnj::block_bunch_slice_t& block_bunch :
4066 : block->stable_block_bunch)
4067 : {
4068 19408 : assert(block_bunch.source_block() == block);
4069 19408 : assert(block_bunch.is_stable());
4070 19408 : block_bunch_check_set.insert(&block_bunch);
4071 19408 : mCRL2complexity(&block_bunch, no_temporary_work(
4072 : block_bunch.bunch->max_work_counter(*this)), *this);
4073 19408 : ++true_nr_of_block_bunch_slices;
4074 : }
4075 :
4076 : // for all states in the block
4077 : do
4078 : {
4079 25711 : trans_type block_bunch_count(0);
4080 25711 : const bisim_dnj::state_info_entry* const state(perm_iter->st);
4081 25711 : assert(state!=part_tr.succ.front().block_bunch->pred->source);
4082 : // for all out-slices of the state
4083 25711 : for (const bisim_dnj::succ_entry*
4084 25711 : out_slice_end(state->succ_inert.begin);
4085 57567 : state == out_slice_end[-1].block_bunch->pred->source; )
4086 31856 : { assert(!out_slice_end[-1].block_bunch->slice.is_null());
4087 : bisim_dnj::block_bunch_slice_const_iter_t const
4088 31856 : block_bunch_slice(out_slice_end[-1].block_bunch->slice);
4089 31856 : const bisim_dnj::bunch_t* const bunch(
4090 31856 : block_bunch_slice->bunch);
4091 31856 : assert(block == block_bunch_slice->source_block());
4092 31856 : if (block_bunch_slice->is_stable())
4093 : {
4094 31856 : assert(1 == block_bunch_check_set.count(
4095 : &*block_bunch_slice));
4096 31856 : ++block_bunch_count;
4097 : }
4098 0 : else assert(0); // i. e. all block_bunch-slices should
4099 : // be stable
4100 31856 : const bisim_dnj::succ_entry* const out_slice_begin(
4101 31856 : out_slice_end[-1].begin_or_before_end);
4102 31856 : assert(nullptr != out_slice_begin);
4103 31856 : assert(out_slice_begin < out_slice_end);
4104 31856 : assert(nullptr != out_slice_begin->begin_or_before_end);
4105 31856 : 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 40089 : --out_slice_end;
4112 40089 : assert(bunch->begin <=
4113 : out_slice_end->block_bunch->pred->action_block);
4114 40089 : assert(out_slice_end->block_bunch->pred->
4115 : action_block < bunch->end);
4116 40089 : assert(out_slice_end->block_bunch->slice ==
4117 : block_bunch_slice);
4118 40089 : assert(nullptr != out_slice_end->begin_or_before_end);
4119 80178 : if (out_slice_end->block_bunch + 1 !=
4120 40089 : block_bunch_slice->end)
4121 : {
4122 20681 : assert(out_slice_end->block_bunch + 1 <
4123 : block_bunch_slice->end);
4124 20681 : assert(out_slice_end->block_bunch[1].slice ==
4125 : block_bunch_slice);
4126 : }
4127 40089 : 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 48322 : while (out_slice_begin < out_slice_end &&
4135 8233 : (assert(out_slice_begin ==
4136 : out_slice_end->begin_or_before_end), true));
4137 : }
4138 25711 : if (perm_iter < block->nonbottom_begin)
4139 : {
4140 22191 : assert(block_bunch_check_set.size() == block_bunch_count);
4141 : }
4142 : }
4143 25711 : while (++perm_iter < block->end);
4144 11537 : }
4145 11537 : while (perm_iter <= &part_st.permutation.back());
4146 1757 : assert(part_tr.nr_of_block_bunch_slices ==
4147 : true_nr_of_block_bunch_slices);
4148 1757 : assert(part_tr.action_block_begin <= part_tr.action_block_inert_begin);
4149 1757 : assert(&part_tr.block_bunch.front() < part_tr.block_bunch_inert_begin);
4150 1757 : if (branching)
4151 585 : { assert(part_tr.action_block_inert_begin<=part_tr.action_block_end);
4152 585 : assert(part_tr.block_bunch_inert_begin <=
4153 : 1 + &part_tr.block_bunch.back());
4154 585 : assert(1 + &part_tr.block_bunch.back() -
4155 : part_tr.block_bunch_inert_begin ==
4156 : part_tr.action_block_end - part_tr.action_block_inert_begin);
4157 :
4158 : // for all inert transitions
4159 4479 : for (const bisim_dnj::action_block_entry* action_block(
4160 : part_tr.action_block_inert_begin);
4161 4479 : action_block < part_tr.action_block_end;
4162 : ++action_block)
4163 3894 : { assert(nullptr == action_block->begin_or_before_end);
4164 : const bisim_dnj::succ_entry* const
4165 3894 : succ_iter(action_block->succ);
4166 3894 : assert(nullptr != succ_iter);
4167 3894 : assert(succ_iter->block_bunch->slice.is_null());
4168 : const bisim_dnj::pred_entry* const
4169 3894 : pred_iter(succ_iter->block_bunch->pred);
4170 3894 : assert(action_block == pred_iter->action_block);
4171 3894 : assert(part_tr.block_bunch_inert_begin <=
4172 : succ_iter->block_bunch);
4173 3894 : assert(pred_iter->source != pred_iter->target);
4174 3894 : assert(pred_iter->source->bl.ock == pred_iter->target->bl.ock);
4175 3894 : assert(pred_iter->source->succ_inert.begin <= succ_iter);
4176 3894 : assert(pred_iter->source->succ_inert.begin == succ_iter ||
4177 : succ_iter[-1].block_bunch->pred->source==pred_iter->source);
4178 3894 : assert(pred_iter->target->pred_inert.begin <= pred_iter);
4179 3894 : assert(pred_iter->target->pred_inert.begin == pred_iter ||
4180 : pred_iter[-1].target == pred_iter->target);
4181 7788 : unsigned const max_block(bisim_gjkw::check_complexity::log_n -
4182 3894 : bisim_gjkw::check_complexity::ilog2(
4183 3894 : pred_iter->target->bl.ock->size()));
4184 3894 : mCRL2complexity(pred_iter, no_temporary_work(max_block,
4185 : max_block, false), *this);
4186 : }
4187 : }
4188 : else
4189 : {
4190 1172 : assert(!preserve_divergence);
4191 1172 : assert(part_tr.action_block_inert_begin==part_tr.action_block_end);
4192 1172 : assert(part_tr.block_bunch_inert_begin ==
4193 : 1 + &part_tr.block_bunch.back());
4194 : }
4195 : const bisim_dnj::action_block_entry*
4196 1757 : action_slice_end(part_tr.action_block_inert_begin);
4197 1757 : trans_type true_nr_of_bunches(0);
4198 1757 : trans_type true_nr_of_nontrivial_bunches(0);
4199 1757 : trans_type true_nr_of_action_block_slices(0);
4200 : // for all action labels and bunches
4201 1757 : label_type label(0);
4202 1757 : assert(label < action_label.size());
4203 1757 : const bisim_dnj::bunch_t* previous_bunch(nullptr);
4204 : do
4205 : {
4206 8662 : assert(part_tr.action_block_begin <= action_label[label].begin);
4207 8662 : assert(action_label[label].begin <= action_slice_end);
4208 8662 : assert(action_slice_end <= part_tr.action_block_inert_begin);
4209 : // for all action_block slices
4210 8662 : for (const bisim_dnj::action_block_entry*
4211 8662 : action_block_slice_end(action_slice_end);
4212 28014 : action_label[label].begin < action_block_slice_end; )
4213 : {
4214 : const bisim_dnj::action_block_entry* const
4215 19352 : action_block_slice_begin(
4216 19352 : action_block_slice_end[-1].begin_or_before_end);
4217 19352 : assert(nullptr != action_block_slice_begin);
4218 19352 : assert(action_block_slice_begin < action_block_slice_end);
4219 19352 : assert(action_block_slice_end <= action_slice_end);
4220 19352 : assert(nullptr != action_block_slice_begin->succ);
4221 : const bisim_dnj::block_t* const
4222 19352 : target_block(action_block_slice_begin->
4223 19352 : succ->block_bunch->pred->target->bl.ock);
4224 : const bisim_dnj::bunch_t* const
4225 19352 : bunch(action_block_slice_begin->succ->bunch());
4226 19352 : if (previous_bunch != bunch)
4227 : {
4228 13409 : assert(nullptr == previous_bunch);
4229 13409 : previous_bunch = bunch;
4230 13409 : assert(bunch->end == action_block_slice_end);
4231 13409 : 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 11818 : assert(bunch->is_trivial());
4237 : }
4238 : else
4239 : {
4240 1591 : assert(!bunch->is_trivial());
4241 1591 : ++true_nr_of_nontrivial_bunches;
4242 : }
4243 13409 : mCRL2complexity(bunch, no_temporary_work(
4244 : bunch->max_work_counter(*this)), *this);
4245 13409 : ++true_nr_of_bunches;
4246 : }
4247 19352 : if(bunch->begin == action_block_slice_begin)
4248 : {
4249 13409 : previous_bunch = nullptr;
4250 : }
4251 5943 : else assert(bunch->begin < action_block_slice_begin);
4252 :
4253 19352 : assert(action_block_slice_begin->begin_or_before_end + 1 ==
4254 : action_block_slice_end);
4255 : // for all transitions in the action_block slice
4256 : const bisim_dnj::action_block_entry*
4257 19352 : action_block(action_block_slice_end);
4258 : do
4259 : {
4260 40089 : --action_block;
4261 : const bisim_dnj::succ_entry* const
4262 40089 : succ_iter(action_block->succ);
4263 40089 : assert(nullptr != succ_iter);
4264 : const bisim_dnj::pred_entry* const
4265 40089 : pred_iter(succ_iter->block_bunch->pred);
4266 40089 : assert(action_block == pred_iter->action_block);
4267 40089 : assert(succ_iter->block_bunch <
4268 : part_tr.block_bunch_inert_begin);
4269 40089 : assert(!branching || !aut.is_tau(label) ||
4270 : pred_iter->source->bl.ock!=pred_iter->target->bl.ock ||
4271 : (preserve_divergence &&
4272 : pred_iter->source == pred_iter->target));
4273 40089 : assert(succ_iter < pred_iter->source->succ_inert.begin);
4274 40089 : assert(succ_iter+1==pred_iter->source->succ_inert.begin ||
4275 : succ_iter[1].block_bunch->pred->source ==
4276 : pred_iter->source);
4277 40089 : assert(pred_iter < pred_iter->target->pred_inert.begin);
4278 40089 : assert(pred_iter+1==pred_iter->target->pred_inert.begin ||
4279 : pred_iter[1].target == pred_iter->target);
4280 40089 : assert(target_block == pred_iter->target->bl.ock);
4281 40089 : assert(bunch == succ_iter->bunch());
4282 : }
4283 60826 : 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 20737 : assert(action_block->begin_or_before_end ==
4287 : action_block_slice_begin), true));
4288 19352 : action_block_slice_end = action_block_slice_begin;
4289 19352 : ++true_nr_of_action_block_slices;
4290 : }
4291 8662 : if (action_slice_end < part_tr.action_block_inert_begin)
4292 : {
4293 : // there is a dummy transition between action labels
4294 6905 : assert(nullptr == action_slice_end->succ);
4295 6905 : assert(nullptr == action_slice_end->begin_or_before_end);
4296 : }
4297 : }
4298 15567 : while (++label < action_label.size() &&
4299 6905 : (action_slice_end = action_label[label - 1].begin - 1, true));
4300 1757 : assert(nullptr == previous_bunch);
4301 1757 : assert(part_tr.nr_of_bunches == true_nr_of_bunches);
4302 1757 : assert(part_tr.nr_of_nontrivial_bunches ==
4303 : true_nr_of_nontrivial_bunches);
4304 1757 : assert(part_tr.nr_of_action_block_slices ==
4305 : true_nr_of_action_block_slices);
4306 : }
4307 : #endif
4308 : /// \brief Run (branching) bisimulation minimisation in time O(m log n)
4309 : /// \details This function assumes that the partitioner object stores a LTS
4310 : /// with a partition satisfying the invariant:
4311 : ///
4312 : /// > If a state contains a transition in a bunch, then every bottom state
4313 : /// > in the same block contains a transition in that bunch.
4314 : ///
4315 : /// The function runs the efficient O(m log n) algorithm for branching
4316 : /// bisimulation minimisation on the LTS that has been stored in the
4317 : /// partitioner: As long as there are nontrivial bunches, it selects one,
4318 : /// subdivides it into two bunches and then stabilises the partition for
4319 : /// these bunches. As a result, the partition stored in the partitioner
4320 : /// will become stable.
4321 : ///
4322 : /// Parameters and return value are implicit with this function: the LTS,
4323 : /// the partition and the flags of the bisimulation algorithm are all
4324 : /// stored in the partitioner object.
4325 333 : void refine_partition_until_it_becomes_stable()
4326 : {
4327 : // Line 2.5: for all non-trivial bunches bunch_T in Pi_t do
4328 333 : clock_t next_print_time = clock();
4329 333 : 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 1424 : for (;;)
4333 : { // mCRL2complexity(...) -- this loop will be ascribed to (the transitions in)
4334 : // the new bunch below.
4335 1757 : /*------------------ find a non-trivial bunch -------------------*/ ONLY_IF_DEBUG( part_st.print_part(*this); part_tr.print_trans(*this);
4336 : assert_stability(); )
4337 1757 : /* 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 1757 : bisim_dnj::bunch_t* const bunch_T(part_tr.get_some_nontrivial());
4340 1757 : if (mCRL2logEnabled(log::verbose))
4341 : {
4342 0 : if (clock_t now = clock(); next_print_time <= now ||
4343 : nullptr == bunch_T)
4344 : {
4345 :
4346 : /* - - - - -print progress information- - - - - */
4347 :
4348 : // The formula below should ensure that `next_print_time`
4349 : // increases by a whole number of minutes, so that the
4350 : // progress information is printed every minute (or, if
4351 : // one iteration takes more than one minute, after a whole
4352 : // number of minutes).
4353 0 : next_print_time+=((now-next_print_time)/(60*CLOCKS_PER_SEC)
4354 : + 1) * (60*CLOCKS_PER_SEC);
4355 0 : now = (now - rounded_start_time) / CLOCKS_PER_SEC;
4356 0 : if (0 != now)
4357 : {
4358 0 : if (60 <= now)
4359 : {
4360 0 : if (3600 <= now)
4361 : {
4362 0 : mCRL2log(log::verbose)
4363 0 : << now / 3600 << " h ";
4364 0 : now %= 3600;
4365 : }
4366 0 : mCRL2log(log::verbose)
4367 0 : << now / 60 << " min ";
4368 0 : now %= 60;
4369 : }
4370 0 : mCRL2log(log::verbose) << now
4371 0 : << " sec passed since starting the main loop.\n";
4372 : }
4373 : #define PRINT_SG_PL(counter, sg_string, pl_string) \
4374 : (counter) \
4375 : << (1 == (counter) ? (sg_string) : (pl_string))
4376 0 : mCRL2log(log::verbose)
4377 0 : << (nullptr == bunch_T ? "The reduced LTS contains "
4378 : : "The reduced LTS contains at least ")
4379 0 : << PRINT_SG_PL(part_st.nr_of_blocks,
4380 : " state and ", " states and ")
4381 0 : << PRINT_SG_PL(part_tr.nr_of_block_bunch_slices,
4382 : " transition.", " transitions.");
4383 0 : if (1 < part_tr.nr_of_action_block_slices)
4384 : {
4385 : #define PRINT_INT_PERCENTAGE(num,denom) \
4386 : (((num) * 200 + (denom)) / (denom) / 2)
4387 0 : mCRL2log(log::verbose) << " Estimated "
4388 0 : << PRINT_INT_PERCENTAGE(part_tr.nr_of_bunches - 1,
4389 : part_tr.nr_of_action_block_slices - 1)
4390 0 : << "% done.";
4391 : #undef PRINT_INT_PERCENTAGE
4392 : }
4393 0 : mCRL2log(log::verbose)
4394 : // << " Logarithmic estimate: "
4395 : // << (int)(100.5+std::log((double) part_tr.nr_of_bunches/
4396 : // part_tr.nr_of_action_block_slices)
4397 : // *log_initial_nr_of_action_block_slices)
4398 : // << "% done."
4399 0 : << "\nThe current partition contains ";
4400 0 : if (branching)
4401 : {
4402 0 : mCRL2log(log::verbose)
4403 0 : << PRINT_SG_PL(part_tr.nr_of_new_bottom_states,
4404 : " new bottom state, ", " new bottom states, ");
4405 0 : } else assert(0 == part_tr.nr_of_new_bottom_states);
4406 0 : mCRL2log(log::verbose)
4407 0 : << PRINT_SG_PL(part_tr.nr_of_bunches,
4408 : " bunch (of which ", " bunches (of which ")
4409 0 : << PRINT_SG_PL(part_tr.nr_of_nontrivial_bunches,
4410 : " is nontrivial), and ", " are nontrivial), and ")
4411 0 : << PRINT_SG_PL(part_tr.nr_of_action_block_slices,
4412 : " action-block-slice.\n", " action-block-slices.\n");
4413 : #undef PRINT_SG_PL
4414 : }
4415 : }
4416 1757 : if (nullptr == bunch_T) { break; } ONLY_IF_DEBUG( mCRL2log(log::debug) << "Refining "
4417 : /* Line 2.7: Pi_t := Pi_t \ { bunch_T } union */ << bunch_T->debug_id(*this) << '\n'; )
4418 1424 : /* { bunch_T_a_Bprime, bunch_T \ bunch_T_a_Bprime } */ assert(part_tr.nr_of_bunches < part_tr.nr_of_action_block_slices);
4419 : bisim_dnj::bunch_t* const bunch_T_a_Bprime(
4420 1424 : bunch_T->split_off_small_action_block_slice(part_tr));
4421 : #ifndef NDEBUG
4422 1424 : /*------------ find predecessors of bunch_T_a_Bprime ------------*/ mCRL2log(log::debug) << "Splitting off "
4423 0 : << bunch_T_a_Bprime->debug_id(*this) << '\n';
4424 1424 : /* Line 2.8: for all B in splittableBlocks(bunch_T_a_Bprime) do */ unsigned const max_splitter_counter(
4425 1424 : /* we actually run through the transitions in T--a-->B' */ bunch_T_a_Bprime->max_work_counter(*this));
4426 : #endif
4427 1424 : bisim_dnj::action_block_entry* splitter_iter(
4428 1424 : bunch_T_a_Bprime->begin); assert(splitter_iter < bunch_T_a_Bprime->end);
4429 : do
4430 2141 : { assert(nullptr != splitter_iter->succ);
4431 : bisim_dnj::state_info_entry* const
4432 2141 : source(splitter_iter->succ->block_bunch->pred->source); assert(splitter_iter->succ->block_bunch->pred->action_block == splitter_iter);
4433 : // Line 2.11: Mark all transitions in bunch_T_a_Bprime
4434 : // actually we mark the source state (i.e. register it's in
4435 : // R)
4436 : bool const first_transition_of_state(
4437 2141 : source->bl.ock->mark(source->pos));
4438 : // Line 2.9: Add bunch_T_a_Bprime as primary to the splitter
4439 : // list
4440 : // Line 2.10: Add T_B--> \ bunch_T_a_Bprime as secondary to the
4441 : // splitter list
4442 2141 : part_tr.first_move_transition_to_new_bunch(splitter_iter,
4443 : bunch_T_a_Bprime, first_transition_of_state); // mCRL2complexity(splitter_iter->succ->block_bunch->pred, ...) -- subsumed
4444 : // Line 2.13: end for // in the call below
4445 : }
4446 2141 : while (++splitter_iter < bunch_T_a_Bprime->end);
4447 :
4448 : // We cannot join the loop above with the loop below!
4449 :
4450 : // Line 2.8: for all B in splittableBlocks(T--a-->B') do
4451 1424 : splitter_iter = bunch_T_a_Bprime->begin; assert(splitter_iter < bunch_T_a_Bprime->end);
4452 : do
4453 : {
4454 : // Line 2.12: For every state with both marked outgoing
4455 : // transitions and outgoing transitions in
4456 : // T_B--> \ bunch_T_a_Bprime, mark one such
4457 : // transition
4458 2141 : part_tr.second_move_transition_to_new_bunch(splitter_iter, ONLY_IF_DEBUG( *this, bunch_T_a_Bprime, )
4459 : bunch_T); // mCRL2complexity(splitter_iter->succ->block_bunch->pred, ...) -- subsumed
4460 : // Line 2.13: end for // in the call below
4461 : }
4462 2141 : while (++splitter_iter < bunch_T_a_Bprime->end); mCRL2complexity(bunch_T_a_Bprime, add_work(bisim_gjkw::check_complexity::
4463 : refine_partition_until_stable__find_pred,
4464 : /*----------------- stabilise the partition again ---------------*/ max_splitter_counter), *this);
4465 1424 : ONLY_IF_DEBUG( bisim_dnj::block_bunch_slice_iter_or_null_t
4466 : /* Line 2.14: for all T'_B--> in the splitter list (in order) do */ bbslice_T_a_Bprime_B(nullptr); )
4467 3412 : while (!part_tr.splitter_list.empty())
4468 : {
4469 : bisim_dnj::block_bunch_slice_iter_t splitter_Tprime_B( // We have to call mCRL2complexity here because `splitter_Tprime_B` may be
4470 1988 : part_tr.splitter_list.begin()); // split up later.
4471 1988 : bisim_dnj::block_t* block_B(splitter_Tprime_B->source_block()); assert(!splitter_Tprime_B->is_stable());
4472 1988 : bool const is_primary_splitter = 0 < block_B->marked_size(); assert(!splitter_Tprime_B->empty());
4473 : #ifndef NDEBUG
4474 1988 : bool add_stabilize_to_bottom_transns_succeeded = true;
4475 1988 : if (is_primary_splitter)
4476 : {
4477 1163 : assert(bbslice_T_a_Bprime_B.is_null());
4478 : // assign work to this splitter bunch
4479 1163 : mCRL2complexity(splitter_Tprime_B, add_work(bisim_gjkw::
4480 : check_complexity::refine_partition_until_stable__stabilize,
4481 : max_splitter_counter), *this);
4482 : }
4483 825 : else if (!bbslice_T_a_Bprime_B.is_null())
4484 : {
4485 : // assign work to this the corresponding block_bunch-slice of
4486 : // bunch_T_a_Bprime
4487 808 : mCRL2complexity(bbslice_T_a_Bprime_B,
4488 : add_work(bisim_gjkw::check_complexity::
4489 : refine_partition_until_stable__stabilize_for_large_splitter,
4490 : max_splitter_counter), *this);
4491 : }
4492 : else
4493 : {
4494 : // This must be a refinement to stabilize for new bottom states.
4495 : // assign work to the new bottom states in this block_bunch-slice
4496 : add_stabilize_to_bottom_transns_succeeded = splitter_Tprime_B->
4497 17 : add_work_to_bottom_transns(bisim_gjkw::check_complexity::
4498 : refine_partition_until_stable__stabilize_new_noninert_a_priori,
4499 : 1U, *this);
4500 : }
4501 : #endif
4502 1988 : if (1 < block_B->size())
4503 : {
4504 : bisim_dnj::permutation_entry* const
4505 1199 : block_B_begin(block_B->begin); assert(block_B_begin->st->pos == block_B_begin);
4506 : // Line 2.15: (R, U) := split(B, T'_B-->)
4507 : // Line 2.16: Remove T'_B--> from the splitter list
4508 : // Line 2.17: Pi_s := Pi_s \ { B } union { R, U } \ { {} }
4509 1199 : bisim_dnj::block_t*block_R=split(block_B,splitter_Tprime_B,
4510 : is_primary_splitter ? extend_from_marked_states
4511 : : extend_from_splitter);
4512 1199 : if (block_B_begin < block_R->begin)
4513 : {
4514 : // The refinement was non-trivial.
4515 :
4516 : // Line 2.18: if T'_B--> was a primary splitter then
4517 947 : if (is_primary_splitter)
4518 821 : { assert(splitter_Tprime_B->bunch == bunch_T_a_Bprime);
4519 : // Line 2.19: Remove T_U--> \ T_U--a-->B' from the
4520 : // splitter list
4521 : bisim_dnj::block_t* const
4522 821 : block_U(block_B_begin->st->bl.ock); assert(block_U->end == block_R->begin);
4523 : bisim_dnj::block_bunch_slice_iter_t U_splitter(
4524 821 : part_tr.splitter_list.begin()); assert(0 == block_U->marked_size());
4525 1642 : if (part_tr.splitter_list.end() != U_splitter &&
4526 821 : (U_splitter->source_block() == block_U ||
4527 1030 : (++U_splitter != part_tr.splitter_list.end() &&
4528 209 : U_splitter->source_block() == block_U)))
4529 821 : { assert(!U_splitter->is_stable());
4530 821 : assert(U_splitter->bunch == bunch_T);
4531 821 : block_U->stable_block_bunch.splice(
4532 : block_U->stable_block_bunch.end(),
4533 821 : part_tr.splitter_list, U_splitter);
4534 821 : U_splitter->make_stable();
4535 : }
4536 : #ifndef NDEBUG
4537 : // There should be no block-bunch-slice for the co-splitter that is
4538 : // still unstable.
4539 821 : for (bisim_dnj::block_bunch_slice_const_iter_t
4540 821 : iter(part_tr.splitter_list.cbegin());
4541 1405 : part_tr.splitter_list.cend() != iter; ++iter)
4542 584 : { assert(!iter->is_stable());
4543 584 : assert(iter->source_block() != block_U);
4544 : /* Line 2.20: end if */ }
4545 : #endif
4546 : }
4547 : #ifndef NDEBUG
4548 : else
4549 : {
4550 : // account for work that couldn't be accounted for earlier (because we
4551 : // didn't know yet which state would become a new bottom state)
4552 126 : if (!add_stabilize_to_bottom_transns_succeeded)
4553 7 : { assert(splitter_Tprime_B->add_work_to_bottom_transns(bisim_gjkw::
4554 : check_complexity::
4555 : refine_partition_until_stable__stabilize_new_noninert_a_posteriori,
4556 : 1U, *this));
4557 : }
4558 126 : if (splitter_Tprime_B->work_counter.has_temporary_work())
4559 4 : { assert(splitter_Tprime_B->add_work_to_bottom_transns(bisim_gjkw::
4560 : check_complexity::
4561 : handle_new_noninert_transns__make_unstable_a_posteriori,
4562 : 1U, *this));
4563 4 : splitter_Tprime_B->work_counter.reset_temporary_work();
4564 : /* Line 2.21: if R--tau-->U is not empty (i. e. R */ }
4565 : /* has new non-inert transitions) then */ }
4566 : #endif
4567 947 : if (0 < block_R->marked_size())
4568 115 : { ONLY_IF_DEBUG( const bisim_dnj::block_bunch_entry* const splitter_end =
4569 : /* Line 2.22: Create a new bunch containing */ splitter_Tprime_B->end; )
4570 : // exactly R--tau-->U, add R--tau-->U to
4571 : // the splitter list, and mark all its
4572 : // transitions
4573 : // to
4574 : // Line 2.28: For each bottom state, mark one of
4575 : // its outgoing transitions in every
4576 : // T_N--> where it has one
4577 115 : block_R = handle_new_noninert_transns(
4578 : block_R, splitter_Tprime_B);
4579 : #ifndef NDEBUG
4580 115 : if (splitter_end[-1].pred->source->bl.ock == block_R)
4581 31 : { assert(!splitter_end[-1].slice.is_null());
4582 31 : splitter_Tprime_B =
4583 31 : (bisim_dnj::block_bunch_slice_iter_t) splitter_end[-1].slice;
4584 : }
4585 115 : /* Line 2.29: end if */ assert(nullptr == block_R || splitter_Tprime_B->source_block() == block_R);
4586 : #endif
4587 : }
4588 : }
4589 : #ifndef NDEBUG
4590 : else
4591 252 : { assert(0 == block_R->marked_size());
4592 252 : assert(add_stabilize_to_bottom_transns_succeeded);
4593 : // now splitter must have some transitions that start in bottom states:
4594 252 : if (splitter_Tprime_B->work_counter.has_temporary_work())
4595 0 : { assert(!is_primary_splitter);
4596 0 : assert(splitter_Tprime_B->add_work_to_bottom_transns(bisim_gjkw::
4597 : check_complexity::
4598 : handle_new_noninert_transns__make_unstable_a_posteriori,
4599 : 1U, *this));
4600 0 : splitter_Tprime_B->work_counter.reset_temporary_work();
4601 : }
4602 : }
4603 1199 : block_B = block_R;
4604 : #endif
4605 : }
4606 : else
4607 789 : { assert(block_B->nonbottom_begin == block_B->end);
4608 789 : /* A block with 1 state will not be split. However, we */ assert(block_B->marked_nonbottom_begin == block_B->end);
4609 : // may have to unmark all states.
4610 789 : block_B->marked_bottom_begin = block_B->end;
4611 789 : block_B->stable_block_bunch.splice(
4612 : block_B->stable_block_bunch.end(),
4613 789 : part_tr.splitter_list, splitter_Tprime_B);
4614 789 : splitter_Tprime_B->make_stable(); assert(add_stabilize_to_bottom_transns_succeeded);
4615 : #ifndef NDEBUG
4616 : // now splitter must have some transitions that start in bottom states:
4617 789 : if (splitter_Tprime_B->work_counter.has_temporary_work())
4618 0 : { assert(!is_primary_splitter);
4619 0 : assert(splitter_Tprime_B->add_work_to_bottom_transns(bisim_gjkw::
4620 : check_complexity::
4621 : handle_new_noninert_transns__make_unstable_a_posteriori,
4622 : 1U, *this));
4623 0 : splitter_Tprime_B->work_counter.reset_temporary_work();
4624 : }
4625 : #endif
4626 : }
4627 : #ifndef NDEBUG
4628 1163 : if (is_primary_splitter && !part_tr.splitter_list.empty() &&
4629 3963 : part_tr.splitter_list.front().bunch == bunch_T &&
4630 812 : part_tr.splitter_list.front().source_block() == block_B)
4631 : { // The next block_bunch-slice to be handled is the one in the large
4632 : // splitter corresponding to the current splitter. In that iteration,
4633 : // we will need the current splitter block_bunch-slice.
4634 808 : assert(nullptr != block_B);
4635 808 : assert(splitter_Tprime_B->source_block() == block_B);
4636 808 : assert(splitter_Tprime_B->bunch == bunch_T_a_Bprime);
4637 808 : bbslice_T_a_Bprime_B = splitter_Tprime_B;
4638 : }
4639 1180 : /* Line 2.30: end for */ else bbslice_T_a_Bprime_B = nullptr;
4640 : #endif
4641 : }
4642 : // Line 2.31: end for
4643 333 : } assert(part_tr.nr_of_bunches == part_tr.nr_of_action_block_slices);
4644 333 : assert(0 == part_tr.nr_of_nontrivial_bunches);
4645 :
4646 : // store the labels with the action_block-slices
4647 : // As every action_block-slice is a (trivial) bunch at the same time,
4648 : // we can reuse the field next_nontrivial_and_label.label (instead of
4649 : // next_nontrivial_and_label.next_nontrivial) to store the label.
4650 : const bisim_dnj::action_block_entry*
4651 333 : action_block_iter_end(part_tr.action_block_inert_begin);
4652 333 : label_type label(0); assert(label < action_label.size());
4653 : do
4654 : {
4655 1284 : for (bisim_dnj::action_block_entry*
4656 1284 : action_block_iter(action_label[label].begin);
4657 3154 : action_block_iter < action_block_iter_end;
4658 1870 : action_block_iter = action_block_iter->begin_or_before_end + 1)
4659 1870 : { assert(nullptr != action_block_iter->succ);
4660 1870 : assert(action_block_iter->succ->block_bunch->pred->action_block ==
4661 : action_block_iter);
4662 1870 : assert(action_block_iter->succ->bunch()->is_trivial());
4663 3740 : action_block_iter->succ->bunch()->
4664 1870 : next_nontrivial_and_label.label = label; assert(nullptr != action_block_iter->begin_or_before_end);
4665 1870 : assert(action_block_iter <= action_block_iter->begin_or_before_end);
4666 : }
4667 : }
4668 2235 : while (++label < action_label.size() &&
4669 951 : (action_block_iter_end = action_label[label - 1].begin - 1, true));
4670 333 : }
4671 :
4672 : /*----------------- Split -- Algorithm 3 of [JGKW 2020] -----------------*/
4673 :
4674 : /// \brief Split a block according to a splitter
4675 : /// \details The function splits `block_B` into the R-subblock (states
4676 : /// with a transition in `splitter_T`) and the U-subblock (states without a
4677 : /// transition in `splitter_T`). Depending on `mode`, the states are
4678 : /// primed as follows:
4679 : ///
4680 : /// - If `mode == extend_from_marked_states`, then all states with strong
4681 : /// transition(s) must have been marked already.
4682 : /// - If `mode == extend_from_marked_states__add_new_noninert_to_splitter`,
4683 : /// states are marked as above. The only difference is the handling of
4684 : /// new non-inert transitions.
4685 : /// - If `mode == extend_from_splitter`, then no states must be marked;
4686 : /// the initial states with a transition in `splitter_T` are searched by
4687 : /// `split()` itself. Every bottom state with strong transition(s)
4688 : /// needs to have at least one marked strong transition.
4689 : ///
4690 : /// The function will also adapt all data structures and determine
4691 : /// which transitions have changed from inert to non-inert. States
4692 : /// with a new non-inert transition will be marked upon returning.
4693 : /// Normally, the new non-inert transitions are moved to a new
4694 : /// bunch, which will be specially created. However, if `mode ==
4695 : /// extend_from_marked_states__add_new_noninert_to_splitter`, then the new
4696 : /// non-inert transitions will be added to `splitter_T` (which must hold
4697 : /// transitions that have just become non-inert before this call to
4698 : /// `split()`). If the resulting block contains marked states, the caller
4699 : /// has to call `handle_new_noninert_transns()` to stabilise the block
4700 : /// because the new bunch may make the block unstable.
4701 : /// \param block_B block that needs to be refined
4702 : /// \param splitter_T transition set that makes the block unstable
4703 : /// \param mode indicates how to find states with a transition in
4704 : /// `splitter_T`, as described above
4705 : /// \returns (a pointer to) the R-subblock. It is an error to call the
4706 : /// function with settings that lead to an empty R-subblock. (An empty
4707 : /// U-subblock is ok.)
4708 1550 : bisim_dnj::block_t* split(bisim_dnj::block_t* const block_B,
4709 : const bisim_dnj::block_bunch_slice_iter_t splitter_T,
4710 : enum refine_mode_t mode)
4711 1550 : { assert(block_B == splitter_T->source_block());
4712 : #ifndef NDEBUG
4713 1550 : mCRL2log(log::debug) << "split("
4714 : << block_B->debug_id(*this)
4715 : << ',' << splitter_T->debug_id(*this)
4716 0 : << (extend_from_marked_states__add_new_noninert_to_splitter == mode
4717 : ? ",extend_from_marked_states__add_new_noninert_to_splitter,"
4718 : : (extend_from_marked_states == mode
4719 0 : ? ",extend_from_marked_states,"
4720 : : (extend_from_splitter == mode
4721 0 : ? ",extend_from_splitter)\n"
4722 : : ",UNKNOWN MODE)\n")));
4723 : #endif
4724 1550 : bisim_dnj::block_t* block_R; assert(!splitter_T->is_stable()); assert(1 < block_B->size());
4725 : union R_s_iter_t
4726 : {
4727 : bisim_dnj::block_bunch_entry* splitter_iter;
4728 : bisim_dnj::permutation_entry* block;
4729 : } R_s_iter;
4730 :
4731 1550 : if (extend_from_splitter == mode)
4732 280 : { assert(0 == block_B->marked_size());
4733 : // Line 3.2: R := B--Marked(T)--> ; U := Bottom(B) \ R
4734 280 : R_s_iter.splitter_iter = splitter_T->end; assert(splitter_T->marked_begin <= R_s_iter.splitter_iter);
4735 675 : while (splitter_T->marked_begin < R_s_iter.splitter_iter)
4736 395 : { assert(&part_tr.block_bunch.cbegin()[1] < R_s_iter.splitter_iter);
4737 395 : --R_s_iter.splitter_iter;
4738 : bisim_dnj::state_info_entry* const
4739 395 : s(R_s_iter.splitter_iter->pred->source); assert(s->bl.ock == block_B); assert(s->pos->st == s);
4740 395 : block_B->mark(s->pos);
4741 : // We cannot stop, even if the R-subblock becomes too large,
4742 : // because we need to mark all bottom states that are not in U.
4743 : }
4744 1270 : } else { assert(0 < block_B->marked_size());
4745 1270 : assert(splitter_T->marked_begin == splitter_T->end); }
4746 1550 : block_B->stable_block_bunch.splice(block_B->stable_block_bunch.end(),
4747 1550 : part_tr.splitter_list, splitter_T);
4748 1550 : splitter_T->make_stable();
4749 :
4750 : COROUTINES_SECTION
4751 : // shared variables of both coroutines
4752 : bisim_dnj::permutation_entry*
4753 1550 : untested_to_U_defined_end(block_B->nonbottom_begin);
4754 : bisim_dnj::permutation_entry*
4755 1550 : U_nonbottom_end(untested_to_U_defined_end);
4756 :
4757 : // variable declarations of the U-coroutine
4758 : bisim_dnj::permutation_entry* U_s_iter;
4759 : bisim_dnj::pred_entry* U_t_iter;
4760 : bisim_dnj::state_info_entry* U_t;
4761 : const bisim_dnj::succ_entry* U_u_iter;
4762 :
4763 : // variable declarations of the R-coroutine
4764 : bisim_dnj::pred_entry* R_t_iter;
4765 :
4766 2960 : COROUTINE_LABELS( (SPLIT_R_PREDECESSOR_HANDLED)
4767 : (SPLIT_U_PREDECESSOR_HANDLED)
4768 : (SPLIT_R_STATE_HANDLED)
4769 : (SPLIT_U_STATE_HANDLED)
4770 : (SPLIT_U_TESTING)
4771 : (SPLIT_R_COLLECT_SPLITTER))
4772 :
4773 : /*------------------------ find U-states ------------------------*/
4774 :
4775 : COROUTINE
4776 : // Line 3.21l: if |U| > |B|/2 then
4777 1550 : if(block_B->size() / 2 < block_B->unmarked_bottom_size())
4778 : {
4779 : // Line 3.22l: Abort this coroutine
4780 409 : ABORT_THIS_COROUTINE();
4781 : // Line 3.23l: end if
4782 : }
4783 1141 : if (0 == block_B->unmarked_bottom_size())
4784 : {
4785 : // all bottom states are in R, so there cannot be any
4786 : // U-states. Unmark all states, as there are no
4787 : // transitions that have become non-inert.
4788 389 : block_B->marked_nonbottom_begin = block_B->end;
4789 389 : block_B->marked_bottom_begin = block_B->nonbottom_begin;
4790 389 : block_R = block_B; ONLY_IF_DEBUG( finalise_U_is_smaller(nullptr, block_R, *this); )
4791 389 : TERMINATE_COROUTINE_SUCCESSFULLY();
4792 : }
4793 :
4794 : /* - - - - - - - visit U-states - - - - - - - */
4795 :
4796 752 : if (U_nonbottom_end < block_B->marked_nonbottom_begin)
4797 : {
4798 : // Line 3.5l: for all s in U while |U| < |B|/2 do
4799 259 : U_s_iter = block_B->begin;
4800 971 : COROUTINE_DO_WHILE (SPLIT_U_STATE_HANDLED,
4801 : U_s_iter < U_nonbottom_end)
4802 : {
4803 567 : /* Line 3.6l: for all inert transitions t--tau-->s do*/ assert(part_tr.pred.front().target != U_s_iter->st);
4804 1171 : COROUTINE_FOR(SPLIT_U_PREDECESSOR_HANDLED,
4805 : U_t_iter = U_s_iter->st->pred_inert.begin,
4806 : U_t_iter->target == U_s_iter->st, ++U_t_iter)
4807 : {
4808 482 : U_t = U_t_iter->source; assert(block_B->nonbottom_begin <= U_t->pos);
4809 482 : /* Line 3.7l: if t in R then Skip state t */ assert(U_t->pos < block_B->end);
4810 482 : if (block_B->marked_nonbottom_begin <= U_t->pos)
4811 : {
4812 94 : goto continuation;
4813 : }
4814 : // Line 3.8l: if untested[t] is undefined then
4815 388 : if (untested_to_U_defined_end <= U_t->pos)
4816 : {
4817 : // Line 3.9l: untested[t] :=
4818 : // |{ t--tau-->u | u in B }|
4819 380 : U_t->untested_to_U_eqv.begin =
4820 380 : U_t->succ_inert.begin;
4821 380 : std::swap(*U_t->pos,
4822 : *untested_to_U_defined_end++);
4823 : // Line 3.10l: end if
4824 388 : } assert(U_t != part_tr.succ.back().block_bunch->pred->source);
4825 : // Line 3.11l: untested[t] := untested[t] − 1
4826 388 : ++U_t->untested_to_U_eqv.begin;
4827 : // Line 3.12l: if untested[t]>0 then Skip state t
4828 388 : if (U_t == U_t->untested_to_U_eqv.
4829 388 : begin->block_bunch->pred->source)
4830 : {
4831 37 : goto continuation;
4832 : }
4833 : // Line 3.13l: if not (B--T--> subset R) then
4834 351 : if (extend_from_splitter == mode)
4835 70 : { assert(U_t != part_tr.succ.front().block_bunch->pred->source);
4836 : // Line 3.14l: for all non-inert
4837 : // t --alpha--> u do
4838 70 : U_u_iter = U_t->succ_inert.begin; assert(&part_tr.succ.front() < U_u_iter);
4839 91 : COROUTINE_WHILE(SPLIT_U_TESTING, U_t ==
4840 : U_u_iter[-1].block_bunch->pred->source)
4841 : {
4842 48 : U_u_iter=U_u_iter[-1].begin_or_before_end; assert(nullptr != U_u_iter);
4843 48 : /* Line 3.15l: if t --alpha--> u in T */ assert(U_u_iter->block_bunch->pred->source == U_t);
4844 48 : /* then Skip t */ assert(!U_u_iter->block_bunch->slice.is_null());
4845 : bisim_dnj::block_bunch_slice_const_iter_t
4846 48 : const block_bunch(
4847 48 : U_u_iter->block_bunch->slice);
4848 48 : if (&*block_bunch == &*splitter_T)
4849 : {
4850 34 : goto continuation;
4851 : // i. e. break and then continue
4852 14 : } ONLY_IF_DEBUG( bisim_dnj::succ_entry::add_work_to_out_slice(*this, U_u_iter,
4853 : /* Line 3.16l: end for */ bisim_gjkw::check_complexity::split_U__test_noninert_transitions, 1U); )
4854 : }
4855 : END_COROUTINE_WHILE;
4856 : // Line 3.17l: end if
4857 311 : } assert(U_nonbottom_end <= U_t->pos);
4858 311 : /* Line 3.18l: Add t to U */ assert(U_t->pos < untested_to_U_defined_end);
4859 311 : std::swap(*U_t->pos, *U_nonbottom_end++);
4860 : // Line 3.21l: if |U| > |B|/2 then
4861 311 : if (block_B->size() / 2 <
4862 311 : U_nonbottom_end-block_B->nonbottom_begin +
4863 311 : block_B->unmarked_bottom_size())
4864 : {
4865 : // Line 3.22l: Abort this coroutine
4866 : // As the U-coroutine is now aborted, the
4867 : // untested_to_U values are no longer relevant.
4868 : // The assignment tells the R-coroutine that it
4869 : // doesn't need to make complicated swaps any
4870 : // more to keep untested properly initialized.
4871 50 : untested_to_U_defined_end = U_nonbottom_end;
4872 50 : ABORT_THIS_COROUTINE();
4873 : // Line 3.23l: end if
4874 : }
4875 : // Line 3.19l: end for
4876 426 : continuation: mCRL2complexity(U_t_iter, add_work(bisim_gjkw::
4877 : check_complexity::split_U__handle_transition_to_U_state, 1U), *this);
4878 : }
4879 476 : END_COROUTINE_FOR; mCRL2complexity(U_s_iter->st, add_work(bisim_gjkw::check_complexity::
4880 : /* Line 3.20l: end for */ split_U__find_predecessors_of_U_state, 1U), *this);
4881 476 : ++U_s_iter;
4882 476 : if(block_B->marked_bottom_begin == U_s_iter)
4883 : {
4884 147 : U_s_iter = block_B->nonbottom_begin;
4885 : }
4886 : }
4887 476 : END_COROUTINE_DO_WHILE;
4888 : }
4889 :
4890 : /*- - - - - - - split off U-block - - - - - - -*/
4891 :
4892 : // Line 3.24l: Abort the other coroutine
4893 593 : ABORT_OTHER_COROUTINE();
4894 : // Line 2.17: Pi_s := Pi_s \ { B } union ({ R, U } \ { {} })
4895 : // All non-U states are in R.
4896 593 : block_B->marked_nonbottom_begin = U_nonbottom_end;
4897 593 : block_R = block_B;
4898 : bisim_dnj::block_t* const block_U(
4899 1186 : block_R->split_off_block(bisim_dnj::new_block_is_U, ONLY_IF_DEBUG( *this, )
4900 593 : ONLY_IF_POOL_ALLOCATOR( part_tr.storage, )
4901 593 : part_st.nr_of_blocks++));
4902 : // Line 2.16: Remove Tprime_B--> = Tprime_R--> from the
4903 : // splitter list
4904 593 : /* and the remainder of Line 2.17 */ assert(0 == block_U->marked_size()); assert(0 == block_R->marked_size());
4905 593 : part_tr.adapt_transitions_for_new_block(block_U, block_R, ONLY_IF_DEBUG( *this, )
4906 : extend_from_marked_states__add_new_noninert_to_splitter ==
4907 593 : mode, splitter_T, bisim_dnj::new_block_is_U); ONLY_IF_DEBUG( finalise_U_is_smaller(block_U, block_R, *this); )
4908 593 : END_COROUTINE
4909 :
4910 : /*------------------------ find R-states ------------------------*/
4911 :
4912 668 : COROUTINE
4913 : // Line 3.21r: if |R| > |B|/2 then
4914 668 : if (block_B->size() / 2 < block_B->marked_size())
4915 : {
4916 : // Line 3.22r: Abort this coroutine
4917 6 : ABORT_THIS_COROUTINE();
4918 : // Line 3.23r: end if
4919 : }
4920 :
4921 : /* - - - - - collect states from B--T--> - - - - - */
4922 :
4923 662 : if (extend_from_splitter == mode)
4924 : {
4925 : // Line 3.4r: R := R union B--(T \ Marked(T))-->
4926 76 : if (U_nonbottom_end < block_B->marked_nonbottom_begin)
4927 64 : { assert(part_tr.block_bunch.front().slice != splitter_T);
4928 175 : COROUTINE_WHILE (SPLIT_R_COLLECT_SPLITTER,
4929 : R_s_iter.splitter_iter[-1].slice == splitter_T)
4930 94 : { assert(&part_tr.block_bunch.cbegin()[1] < R_s_iter.splitter_iter);
4931 94 : --R_s_iter.splitter_iter;
4932 94 : bisim_dnj::state_info_entry* const s(
4933 94 : R_s_iter.splitter_iter->pred->source); assert(s->bl.ock == block_B); assert(s->pos->st == s);
4934 94 : if (block_B->nonbottom_begin <= s->pos)
4935 91 : { assert(U_nonbottom_end <= s->pos);
4936 91 : if (s->pos < untested_to_U_defined_end)
4937 : {
4938 : // The non-bottom state has a transition
4939 : // to a visited U-state, so untested is
4940 : // initialised; however, now it is
4941 : // discovered to be in R anyway.
4942 34 : std::swap(*s->pos,
4943 : *--untested_to_U_defined_end);
4944 : }
4945 171 : if (block_B->mark_nonbottom(s->pos) &&
4946 : // Line 3.21r: if |R| > |B|/2 then
4947 80 : block_B->size()/2 < block_B->marked_size())
4948 : {
4949 : // Line 3.22r: Abort this coroutine
4950 3 : ABORT_THIS_COROUTINE();
4951 : // Line 3.23r: end if
4952 : }
4953 3 : } else assert(block_B->marked_bottom_begin <= s->pos);
4954 91 : mCRL2complexity(R_s_iter.splitter_iter->pred, add_work(bisim_gjkw::
4955 : check_complexity::split_R__handle_transition_from_R_state, 1U), *this);
4956 : }
4957 : END_COROUTINE_WHILE;
4958 :
4959 : // Indicate to the U-coroutine that all states in
4960 : // B--T--> are now in R.
4961 : // The shared variable `mode` is used
4962 : // instead of a separate shared variable.
4963 57 : mode = extend_from_marked_states;
4964 : }
4965 : #ifndef NDEBUG
4966 : else
4967 : {
4968 : // assert that all non-marked transitions in `splitter_T` start in
4969 : // marked states
4970 12 : assert(part_tr.block_bunch.front().slice != splitter_T);
4971 14 : while (R_s_iter.splitter_iter[-1].slice == splitter_T)
4972 : {
4973 2 : assert(&part_tr.block_bunch.cbegin()[1] < R_s_iter.splitter_iter);
4974 2 : --R_s_iter.splitter_iter;
4975 : bisim_dnj::state_info_entry* const
4976 2 : s(R_s_iter.splitter_iter->pred->source);
4977 2 : assert(s->bl.ock == block_B); assert(s->pos->st == s);
4978 2 : assert(s->pos < block_B->nonbottom_begin ||
4979 : block_B->marked_nonbottom_begin <= s->pos);
4980 2 : assert(block_B->marked_bottom_begin <= s->pos);
4981 : }
4982 : }
4983 : #endif
4984 : }
4985 :
4986 655 : /* - - - - - - - visit R-states - - - - - - - */ assert(0 != block_B->marked_size());
4987 :
4988 655 : if (U_nonbottom_end < block_B->marked_nonbottom_begin)
4989 : {
4990 : // Line 3.5r: for all s in R while |R| < |B|/2 do
4991 219 : R_s_iter.block = block_B->nonbottom_begin;
4992 219 : if (block_B->marked_bottom_begin == R_s_iter.block)
4993 : {
4994 : // It may happen that all found states are non-bottom
4995 : // states. (In that case, some of these states will
4996 : // become new bottom states.)
4997 57 : R_s_iter.block = block_B->end;
4998 219 : } assert(block_B->marked_nonbottom_begin != R_s_iter.block);
4999 886 : COROUTINE_DO_WHILE(SPLIT_R_STATE_HANDLED,
5000 : block_B->marked_nonbottom_begin != R_s_iter.block)
5001 : {
5002 529 : --R_s_iter.block; assert(part_tr.pred.back().target != R_s_iter.block->st);
5003 : // Line 3.7r: for all inert transitions t--tau-->s do
5004 909 : COROUTINE_FOR (SPLIT_R_PREDECESSOR_HANDLED,
5005 : R_t_iter = R_s_iter.block->st->pred_inert.begin,
5006 : R_t_iter->target == R_s_iter.block->st, ++R_t_iter)
5007 : {
5008 : bisim_dnj::state_info_entry* const
5009 378 : t(R_t_iter->source); assert(U_nonbottom_end <= t->pos);
5010 378 : /* Line 3.18r: Add t to R */ assert(t->pos->st == t); assert(t->pos < block_B->end);
5011 378 : if (t->pos < untested_to_U_defined_end)
5012 : {
5013 : // The state has a transition to a U-state, so
5014 : // untested is initialised; however, now it is
5015 : // discovered to be in R anyway.
5016 20 : std::swap(*t->pos,
5017 : *--untested_to_U_defined_end);
5018 : }
5019 689 : if (block_B->mark_nonbottom(t->pos) &&
5020 : // Line 3.21r: if |R| > |B|/2 then
5021 311 : block_B->size() / 2 < block_B->marked_size())
5022 : {
5023 : // Line 3.22r: Abort this coroutine
5024 79 : ABORT_THIS_COROUTINE();
5025 : // Line 3.23r: end if
5026 299 : } mCRL2complexity(R_t_iter, add_work(bisim_gjkw::
5027 : /* Line 3.19r: end for */ check_complexity::split_R__handle_transition_to_R_state, 1U), *this);
5028 : }
5029 447 : END_COROUTINE_FOR; mCRL2complexity(R_s_iter.block->st, add_work(bisim_gjkw::
5030 : check_complexity::split_R__find_predecessors_of_R_state,
5031 : /* Line 3.20r: end for */ 1U), *this);
5032 447 : if (block_B->marked_bottom_begin == R_s_iter.block &&
5033 105 : R_s_iter.block < block_B->nonbottom_begin)
5034 : {
5035 102 : R_s_iter.block = block_B->end;
5036 : }
5037 : }
5038 447 : END_COROUTINE_DO_WHILE;
5039 : }
5040 :
5041 : /*- - - - - - - split off R-block - - - - - - -*/
5042 :
5043 : // Line 3.24r: Abort the other coroutine
5044 568 : ABORT_OTHER_COROUTINE();
5045 : // Line 2.17: Pi_s := Pi_s \ { B } union ({ R, U } \ { {} })
5046 : // All non-R states are in U.
5047 1136 : block_R = block_B->split_off_block(bisim_dnj::new_block_is_R, ONLY_IF_DEBUG( *this, )
5048 568 : ONLY_IF_POOL_ALLOCATOR( part_tr.storage, )
5049 568 : part_st.nr_of_blocks++);
5050 : // Line 2.16: Remove Tprime_B--> = Tprime_R--> from the
5051 : // splitter list
5052 568 : /* and the remainder of Line 2.17 */ assert(0 == block_B->marked_size()); assert(0 == block_R->marked_size());
5053 568 : part_tr.adapt_transitions_for_new_block(block_R, block_B, ONLY_IF_DEBUG( *this, )
5054 : extend_from_marked_states__add_new_noninert_to_splitter ==
5055 568 : mode, splitter_T, bisim_dnj::new_block_is_R); ONLY_IF_DEBUG( finalise_R_is_smaller(block_B, block_R, *this); )
5056 568 : END_COROUTINE
5057 1550 : END_COROUTINES_SECTION
5058 1550 : return block_R;
5059 : }
5060 :
5061 : /*-- Handle new non-inert transitions -- Lines 2.22-2.28 in [JGKW2020] --*/
5062 :
5063 : /// \brief Handle a block with new non-inert transitions
5064 : /// \details When this function starts, it assumes that the states with a
5065 : /// new non-inert transition in `block_R` are marked. It is an error if it
5066 : /// does not contain any marked states.
5067 : ///
5068 : /// The function separates the states with new non-inert transitions from
5069 : /// those without; as a result, the N-subblock (which contains states
5070 : /// with new non-inert transitions) will contain at least one new bottom
5071 : /// state (and no old bottom states). It then registers almost all
5072 : /// block_bunch-slices of this N-subblock as unstable and marks one
5073 : /// transition per block_bunch-slice and new bottom state. Only the
5074 : /// block_bunch-slice containing the new non-inert transitions and, if
5075 : /// possible, `bbslice_Tprime_R` are not registered as unstable.
5076 : /// \param block_R block containing states with new non-inert
5077 : /// transitions that need to be stabilised
5078 : /// \param bbslice_Tprime_R splitter of the last separation before, i.e.
5079 : /// the splitter that made these transitions
5080 : /// non-inert (`block_R` should already be stable
5081 : /// w.r.t. `bbslice_Tprime_R`).
5082 : /// \returns the block containing the old bottom states (and every state in
5083 : /// `block_R` that cannot reach any new non-inert transition),
5084 : /// i.e. the U-subblock of the separation
5085 115 : bisim_dnj::block_t* handle_new_noninert_transns(
5086 : bisim_dnj::block_t* const block_R,
5087 : bisim_dnj::block_bunch_slice_const_iter_t bbslice_Tprime_R)
5088 115 : { assert(block_R == bbslice_Tprime_R->source_block());
5089 115 : bisim_dnj::block_t* block_Rprime; assert(&part_tr.block_bunch.cbegin()[1] < part_tr.block_bunch_inert_begin);
5090 115 : bisim_dnj::block_t* block_N; assert(!part_tr.block_bunch_inert_begin[-1].slice.is_null());
5091 115 : bisim_dnj::block_bunch_slice_iter_t const bbslice_R_tau_U(
5092 115 : part_tr.block_bunch_inert_begin[-1].slice); assert(bbslice_Tprime_R->is_stable());
5093 115 : /* Line 2.23: (N, R') := split(R, R--tau-->U) */ assert(!bbslice_R_tau_U->is_stable());
5094 115 : /* Line 2.24: Remove R--tau-->U from the splitter list */ assert(block_R == bbslice_R_tau_U->source_block());
5095 115 : /* Line 2.25: Pi_s := Pi_s \ { R } union { N, R' } \ { emptyset } */ assert(0 < block_R->marked_size());
5096 : // Line 2.26: Add N--tau-->R' to the bunch containing R--tau-->U
5097 115 : if (0 < block_R->unmarked_bottom_size())
5098 33 : { assert(part_tr.splitter_list.begin() != part_tr.splitter_list.end());
5099 : #ifndef NDEBUG
5100 33 : bool const next_splitter_is_of_same_block =
5101 45 : part_tr.splitter_list.begin() != bbslice_R_tau_U &&
5102 12 : part_tr.splitter_list.front().source_block() == block_R;
5103 : #endif
5104 33 : block_N = split(block_R, bbslice_R_tau_U,
5105 33 : extend_from_marked_states__add_new_noninert_to_splitter); assert(&part_st.permutation.front() < block_N->begin);
5106 33 : block_Rprime = block_N->begin[-1].st->bl.ock;
5107 : #ifndef NDEBUG
5108 : // If the first element of the splitter list was a block_bunch-slice of
5109 : // block_N, it was split up. The condition below checks whether the
5110 : // N-subblock's (= the block with new bottom states) slice is placed before
5111 : // the R'-subblock's (= the block with old bottom states).
5112 41 : if (next_splitter_is_of_same_block &&
5113 41 : (assert(part_tr.splitter_list.begin() != part_tr.splitter_list.end()),
5114 8 : part_tr.splitter_list.front().source_block()==block_N))
5115 : {
5116 : bisim_dnj::block_bunch_slice_iter_t const bbslice_T_Rprime(
5117 1 : std::next(part_tr.splitter_list.begin()));
5118 2 : if (part_tr.splitter_list.end() != bbslice_T_Rprime &&
5119 1 : bbslice_T_Rprime->source_block() == block_Rprime)
5120 : {
5121 : // The R'-subblock's slice must be the first in the splitter list.
5122 : // This is necessary in Debug-mode to ensure that the cost of
5123 : // refining R' is accounted for correctly.
5124 1 : part_tr.splitter_list.splice(part_tr.splitter_list.begin(),
5125 1 : /* If more new noninert transitions are found, we do not need to */ part_tr.splitter_list, bbslice_T_Rprime);
5126 : /* separate them further, as every bottom state already has a */ }
5127 : /* transition in bbslice_R_tau_U->bunch. */ }
5128 : #endif
5129 33 : if (0 < block_N->marked_bottom_size())
5130 : {
5131 : // Not only new non-inert transitions, but also new bottom
5132 : // states have been found. In that case, we also have to
5133 : // refine w.r.t. the last splitter, as the new bottom states in
5134 : // block_N may be unstable under it. We set the variable
5135 : // `bbslice_Tprime_R` to `bbslice_R_tau_U` so it won't disturb
5136 : // in the test below.
5137 27 : bbslice_Tprime_R = bbslice_R_tau_U;
5138 27 : block_N->marked_bottom_begin = block_N->nonbottom_begin;
5139 : }
5140 6 : else if (bbslice_Tprime_R->source_block() != block_N)
5141 2 : { assert(bbslice_Tprime_R->source_block() == block_Rprime);
5142 : // bbslice_Tprime_R contained transitions from every (old and
5143 : // new) bottom state in the block. It has been split, and now
5144 : // it contains transitions from the block with old bottom
5145 2 : /* states; however, we need the block_bunch-slice with */ assert(!bbslice_Tprime_R->end->slice.is_null());
5146 2 : /* transitions from the block with new bottom states. */ assert(bbslice_Tprime_R->end < part_tr.block_bunch_inert_begin);
5147 2 : bbslice_Tprime_R = (bisim_dnj::block_bunch_slice_const_iter_t)
5148 2 : bbslice_Tprime_R->end->slice; assert(bbslice_Tprime_R->source_block() == block_N);
5149 : }
5150 : }
5151 : else
5152 : {
5153 82 : block_N = block_R;
5154 : // make bbslice_R_tau_U stable
5155 82 : block_N->stable_block_bunch.splice(
5156 : block_N->stable_block_bunch.end(),
5157 82 : part_tr.splitter_list, bbslice_R_tau_U);
5158 82 : bbslice_R_tau_U->make_stable();
5159 82 : block_N->marked_bottom_begin = block_N->nonbottom_begin;
5160 82 : block_Rprime = nullptr;
5161 : }
5162 115 : block_N->marked_nonbottom_begin = block_N->end;
5163 :
5164 115 : if (1 >= block_N->size()) return block_Rprime;
5165 :
5166 : // Line 2.27: Insert all T_N--> as secondary into the splitter list
5167 : // However, the bunch of new noninert transitions and the bunch
5168 : // that was the last splitter do not need to be handled (as long
5169 : // as there are no further new bottom states).
5170 : // We cannot do this in time O(1) because we need to call
5171 : // `make_unstable()` for each block_bunch-slice individually.
5172 45 : for (bisim_dnj::block_bunch_slice_iter_t bbslice_T_N(
5173 45 : block_N->stable_block_bunch.begin());
5174 138 : block_N->stable_block_bunch.end() != bbslice_T_N; )
5175 93 : { assert(bbslice_T_N->is_stable());
5176 : bisim_dnj::block_bunch_slice_iter_t const
5177 93 : next_bbslice_T_N(std::next(bbslice_T_N));
5178 141 : if (&*bbslice_T_N != &*bbslice_Tprime_R &&
5179 48 : &*bbslice_T_N != &*bbslice_R_tau_U)
5180 : {
5181 : // In Debug mode, we have to place the new splitters at the end
5182 : // of the splitter list -- after a refinement with a primary
5183 : // splitter, the corresponding refinement with the large
5184 : // splitter should follow immediately, to ensure that the cost
5185 : // for refining `block_Rprime` is accounted for correctly.
5186 10 : part_tr.splitter_list.splice(part_tr.splitter_list.end(),
5187 10 : block_N->stable_block_bunch, bbslice_T_N);
5188 10 : bbslice_T_N->make_unstable();
5189 : }
5190 : #ifndef NDEBUG
5191 : // Try to assign this work to a transition from a bottom state in
5192 : // bbslice_T_N.
5193 : // If that does not succeed, temporarily assign it to the block_bunch
5194 : // itself. Later, we shall find a bottom state to which this work can be
5195 : // assigned.
5196 93 : assert(!bbslice_T_N->work_counter.has_temporary_work());
5197 93 : if (!bbslice_T_N->add_work_to_bottom_transns(bisim_gjkw::check_complexity::
5198 : handle_new_noninert_transns__make_unstable_a_priori, 1U, *this))
5199 4 : { mCRL2complexity(bbslice_T_N, add_work(bisim_gjkw::check_complexity::
5200 : handle_new_noninert_transns__make_unstable_temp, 1U), *this);
5201 4 : assert(bbslice_T_N->work_counter.has_temporary_work());
5202 4 : assert(!bbslice_T_N->is_stable());
5203 : }
5204 : #endif
5205 93 : bbslice_T_N = next_bbslice_T_N;
5206 : }
5207 :
5208 : // Line 2.28: For each bottom state, mark one of its outgoing
5209 : // transitions in each in every T_N--> where it has one
5210 45 : bisim_dnj::permutation_entry* s_iter(block_N->begin); assert(s_iter < block_N->nonbottom_begin);
5211 : do
5212 : {
5213 75 : bisim_dnj::state_info_entry* const s(s_iter->st); assert(s->pos == s_iter);
5214 : // for all out-slices of s do
5215 75 : for (bisim_dnj::succ_entry* succ_iter(s->succ_inert.begin);
5216 220 : s == succ_iter[-1].block_bunch->pred->source; )
5217 145 : { assert(succ_iter[-1].begin_or_before_end < succ_iter);
5218 145 : succ_iter = succ_iter[-1].begin_or_before_end; assert(nullptr != succ_iter);
5219 145 : /* Mark the first transition in the out-slice in its */ assert(succ_iter->block_bunch->pred->action_block->succ == succ_iter);
5220 145 : /* block_bunch-slice */ assert(s == succ_iter->block_bunch->pred->source);
5221 : bisim_dnj::block_bunch_entry* const
5222 145 : old_block_bunch_pos(succ_iter->block_bunch); assert(!old_block_bunch_pos->slice.is_null());
5223 : bisim_dnj::block_bunch_slice_iter_t const
5224 145 : bbslice_T_N((bisim_dnj::block_bunch_slice_iter_t)
5225 : old_block_bunch_pos->slice);
5226 145 : if (!bbslice_T_N->is_stable())
5227 8 : { assert(&*bbslice_T_N != &*bbslice_Tprime_R && bbslice_T_N != bbslice_R_tau_U);
5228 : bisim_dnj::block_bunch_entry* const
5229 8 : new_block_bunch_pos(bbslice_T_N->marked_begin - 1);
5230 : // It may happen that the transition was already paid
5231 : // for earlier, namely if it once was in bunch_T
5232 8 : if (old_block_bunch_pos <= new_block_bunch_pos)
5233 : {
5234 8 : bbslice_T_N->marked_begin = new_block_bunch_pos; assert(new_block_bunch_pos->slice == bbslice_T_N);
5235 8 : std::swap(old_block_bunch_pos->pred,
5236 8 : new_block_bunch_pos->pred); assert(nullptr != old_block_bunch_pos->pred->action_block->succ);
5237 8 : old_block_bunch_pos->pred->action_block->succ->
5238 8 : block_bunch = old_block_bunch_pos; assert(new_block_bunch_pos->pred->action_block->succ == succ_iter);
5239 8 : succ_iter->block_bunch = new_block_bunch_pos; // add_work(succ_iter->block_bunch->pred, ...) -- subsumed in the call below
5240 : }
5241 137 : } else assert(&*bbslice_T_N==&*bbslice_Tprime_R || bbslice_T_N==bbslice_R_tau_U);
5242 75 : } mCRL2complexity(s, add_work(bisim_gjkw::check_complexity::
5243 : handle_new_noninert_transns, 1U), *this);
5244 : }
5245 75 : while (++s_iter < block_N->nonbottom_begin);
5246 :
5247 45 : return block_Rprime;
5248 : }
5249 : };
5250 :
5251 : ///@} (end of group part_refine)
5252 : #ifndef NDEBUG
5253 : namespace bisim_dnj {
5254 :
5255 : /// \brief moves temporary work counters to normal ones if the U-block is
5256 : /// smaller
5257 : /// \param block_U the smaller subblock containing the U-states (can
5258 : /// be nullptr)
5259 : /// \param block_R the larger subblock containing the R-states
5260 : /// \param partitioner the partitioner data structure, used to write
5261 : /// diagnostic messages
5262 : template <class LTS_TYPE>
5263 982 : static void finalise_U_is_smaller(const block_t* const block_U,
5264 : const block_t* const block_R,
5265 : const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
5266 : {
5267 982 : if (nullptr != block_U)
5268 : {
5269 1186 : unsigned const max_U_block(bisim_gjkw::check_complexity::log_n -
5270 593 : bisim_gjkw::check_complexity::ilog2(block_U->size()));
5271 : // finalise work counters for the U-states and their transitions
5272 593 : const permutation_entry* s_iter(block_U->begin);
5273 593 : assert(s_iter < block_U->end);
5274 : do
5275 : {
5276 933 : const state_info_entry* const s(s_iter->st);
5277 933 : mCRL2complexity(s, finalise_work(bisim_gjkw::check_complexity::
5278 : split_U__find_predecessors_of_U_state,
5279 : bisim_gjkw::check_complexity::
5280 : split__find_predecessors_of_R_or_U_state,
5281 : max_U_block), partitioner);
5282 933 : assert(s != partitioner.part_tr.pred.back().target);
5283 962 : for (const pred_entry* pred_iter(s->pred_inert.begin);
5284 962 : s == pred_iter->target; ++pred_iter)
5285 : {
5286 29 : mCRL2complexity(pred_iter, finalise_work(
5287 : bisim_gjkw::check_complexity::
5288 : split_U__handle_transition_to_U_state,
5289 : bisim_gjkw::check_complexity::
5290 : split__handle_transition_to_R_or_U_state,
5291 : max_U_block), partitioner);
5292 : }
5293 : // Sometimes, inert transitions become transitions from R- to
5294 : // U-states; therefore, we also have to walk through the
5295 : // noninert predecessors of U-states:
5296 933 : assert(s != partitioner.part_tr.pred.front().target);
5297 933 : for (const pred_entry* pred_iter(s->pred_inert.begin);
5298 2140 : s == (--pred_iter)->target; )
5299 : {
5300 1207 : mCRL2complexity(pred_iter, finalise_work(
5301 : bisim_gjkw::check_complexity::
5302 : split_U__handle_transition_to_U_state,
5303 : bisim_gjkw::check_complexity::
5304 : split__handle_transition_to_R_or_U_state,
5305 : max_U_block), partitioner);
5306 : }
5307 933 : assert(s != partitioner.part_tr.succ.front().
5308 : block_bunch->pred->source);
5309 933 : for (const succ_entry* succ_iter(s->succ_inert.begin);
5310 1709 : s == (--succ_iter)->block_bunch->pred->source; )
5311 : {
5312 776 : mCRL2complexity(succ_iter->block_bunch->pred,finalise_work(
5313 : bisim_gjkw::check_complexity::
5314 : split_U__test_noninert_transitions,
5315 : bisim_gjkw::check_complexity::
5316 : split__handle_transition_from_R_or_U_state,
5317 : max_U_block), partitioner);
5318 : }
5319 : }
5320 933 : while (++s_iter < block_U->end);
5321 : }
5322 : // cancel work counters for the R-states and their transitions, and
5323 : // also account for work done in the U-coroutine on R-states
5324 982 : const permutation_entry* s_iter(block_R->begin);
5325 982 : assert(s_iter < block_R->end);
5326 : do
5327 : {
5328 3466 : const state_info_entry* const s(s_iter->st);
5329 3466 : mCRL2complexity(s, cancel_work(bisim_gjkw::check_complexity::
5330 : split_R__find_predecessors_of_R_state), partitioner);
5331 3466 : assert(s != partitioner.part_tr.pred.back().target);
5332 4643 : for (const pred_entry* pred_iter(s->pred_inert.begin);
5333 4643 : s == pred_iter->target; ++pred_iter)
5334 : {
5335 1177 : mCRL2complexity(pred_iter, cancel_work(
5336 : bisim_gjkw::check_complexity::
5337 : split_R__handle_transition_to_R_state), partitioner);
5338 : }
5339 3466 : assert(s !=
5340 : partitioner.part_tr.succ.front().block_bunch->pred->source);
5341 3466 : for (const succ_entry* succ_iter(s->succ_inert.begin);
5342 9108 : s == (--succ_iter)->block_bunch->pred->source; )
5343 : {
5344 5642 : mCRL2complexity(succ_iter->block_bunch->pred, cancel_work(
5345 : bisim_gjkw::check_complexity::
5346 : split_R__handle_transition_from_R_state), partitioner);
5347 : // the following counter measures work done in the
5348 : // U-coroutine that found R-states.
5349 5642 : mCRL2complexity(succ_iter->block_bunch->pred,finalise_work(
5350 : bisim_gjkw::check_complexity::
5351 : split_U__test_noninert_transitions,
5352 : bisim_gjkw::check_complexity::
5353 : split__test_noninert_transitions_found_new_bottom_state,
5354 : 1U), partitioner);
5355 : }
5356 : }
5357 3466 : while (++s_iter < block_R->end);
5358 :
5359 982 : bisim_gjkw::check_complexity::check_temporary_work();
5360 982 : }
5361 :
5362 : /// \brief moves temporary work counters to normal ones if the R-block is
5363 : /// smaller
5364 : /// \param block_U the larger subblock containing the U-states
5365 : /// \param block_R the smaller but non-empty subblock containing the
5366 : /// R-states
5367 : /// \param partitioner the partitioner data structure, used to write
5368 : /// diagnostic messages
5369 : template <class LTS_TYPE>
5370 568 : static void finalise_R_is_smaller(const block_t* const block_U,
5371 : const block_t* const block_R,
5372 : const bisim_partitioner_dnj<LTS_TYPE>& partitioner)
5373 : {
5374 1136 : unsigned const max_R_block(bisim_gjkw::check_complexity::log_n -
5375 568 : bisim_gjkw::check_complexity::ilog2(block_R->size()));
5376 : // cancel work counters for the U-states and their transitions
5377 568 : const permutation_entry* s_iter(block_U->begin);
5378 568 : assert(s_iter < block_U->end);
5379 : do
5380 : {
5381 5419 : const state_info_entry* const s(s_iter->st);
5382 5419 : mCRL2complexity(s, cancel_work(bisim_gjkw::check_complexity::
5383 : split_U__find_predecessors_of_U_state), partitioner);
5384 5419 : assert(s != partitioner.part_tr.pred.back().target);
5385 6219 : for (const pred_entry* pred_iter(s->pred_inert.begin);
5386 6219 : s == pred_iter->target; ++pred_iter)
5387 : {
5388 800 : mCRL2complexity(pred_iter, cancel_work(
5389 : bisim_gjkw::check_complexity::
5390 : split_U__handle_transition_to_U_state), partitioner);
5391 : }
5392 : // Sometimes, inert transitions become transitions from R- to
5393 : // U-states; therefore, we also have to walk through the
5394 : // noninert predecessors of U-states:
5395 5419 : assert(s != partitioner.part_tr.pred.front().target);
5396 5419 : for (const pred_entry* pred_iter(s->pred_inert.begin);
5397 12367 : s == (--pred_iter)->target; )
5398 : {
5399 6948 : mCRL2complexity(pred_iter, cancel_work(
5400 : bisim_gjkw::check_complexity::
5401 : split_U__handle_transition_to_U_state), partitioner);
5402 : }
5403 5419 : assert(s !=
5404 : partitioner.part_tr.succ.front().block_bunch->pred->source);
5405 5419 : for (const succ_entry* succ_iter(s->succ_inert.begin);
5406 13014 : s == (--succ_iter)->block_bunch->pred->source; )
5407 : {
5408 7595 : mCRL2complexity(succ_iter->block_bunch->pred, cancel_work(
5409 : bisim_gjkw::check_complexity::
5410 : split_U__test_noninert_transitions), partitioner);
5411 : }
5412 : }
5413 5419 : while (++s_iter < block_U->end);
5414 : // finalise work counters for the R-states and their transitions
5415 568 : s_iter = block_R->begin;
5416 568 : assert(s_iter < block_R->end);
5417 : do
5418 : {
5419 1053 : const state_info_entry* const s(s_iter->st);
5420 1053 : mCRL2complexity(s, finalise_work(bisim_gjkw::check_complexity::
5421 : split_R__find_predecessors_of_R_state,
5422 : bisim_gjkw::check_complexity::
5423 : split__find_predecessors_of_R_or_U_state,
5424 : max_R_block), partitioner);
5425 1053 : assert(s != partitioner.part_tr.pred.back().target);
5426 1305 : for (const pred_entry* pred_iter(s->pred_inert.begin);
5427 1305 : s == pred_iter->target; ++pred_iter)
5428 : {
5429 252 : mCRL2complexity(pred_iter, finalise_work(
5430 : bisim_gjkw::check_complexity::
5431 : split_R__handle_transition_to_R_state,
5432 : bisim_gjkw::check_complexity::
5433 : split__handle_transition_to_R_or_U_state,
5434 : max_R_block), partitioner);
5435 : }
5436 1053 : assert(s !=
5437 : partitioner.part_tr.succ.front().block_bunch->pred->source);
5438 1053 : for (const succ_entry* succ_iter(s->succ_inert.begin);
5439 2738 : s == (--succ_iter)->block_bunch->pred->source; )
5440 : {
5441 1685 : mCRL2complexity(succ_iter->block_bunch->pred, finalise_work(
5442 : bisim_gjkw::check_complexity::
5443 : split_R__handle_transition_from_R_state,
5444 : bisim_gjkw::check_complexity::
5445 : split__handle_transition_from_R_or_U_state,
5446 : max_R_block), partitioner);
5447 : // the following counter actually is work done in the
5448 : // U-coroutine that found R-states.
5449 1685 : mCRL2complexity(succ_iter->block_bunch->pred, cancel_work(
5450 : bisim_gjkw::check_complexity::
5451 : split_U__test_noninert_transitions), partitioner);
5452 : }
5453 : }
5454 1053 : while (++s_iter < block_R->end);
5455 568 : bisim_gjkw::check_complexity::check_temporary_work();
5456 568 : }
5457 :
5458 : } // end namespace bisim_dnj
5459 : #endif
5460 :
5461 :
5462 :
5463 :
5464 :
5465 : /* ************************************************************************* */
5466 : /* */
5467 : /* I N T E R F A C E */
5468 : /* */
5469 : /* ************************************************************************* */
5470 :
5471 :
5472 :
5473 :
5474 :
5475 : /// \defgroup part_interface
5476 : /// \brief nonmember functions serving as interface with the rest of mCRL2
5477 : /// \details These functions are copied, almost without changes, from
5478 : /// liblts_bisim_gw.h, which was written by Anton Wijs.
5479 : ///@{
5480 :
5481 : /// \brief Reduce transition system l with respect to strong or
5482 : /// (divergence-preserving) branching bisimulation.
5483 : /// \param[in,out] l The transition system that is reduced.
5484 : /// \param branching If true branching bisimulation is
5485 : /// applied, otherwise strong bisimulation.
5486 : /// \param preserve_divergence Indicates whether loops of internal
5487 : /// actions on states must be preserved. If
5488 : /// false these are removed. If true these
5489 : /// are preserved.
5490 : template <class LTS_TYPE>
5491 261 : void bisimulation_reduce_dnj(LTS_TYPE& l, bool const branching = false,
5492 : bool const preserve_divergence = false)
5493 : {
5494 261 : if (1 >= l.num_states())
5495 : {
5496 9 : mCRL2log(log::warning) << "There is only 1 state in the LTS. It is not "
5497 : "guaranteed that branching bisimulation minimisation runs in "
5498 : "time O(m log n).\n";
5499 : }
5500 : // Line 2.1: Find tau-SCCs and contract each of them to a single state
5501 261 : if (branching)
5502 : {
5503 102 : scc_reduce(l, preserve_divergence);
5504 : }
5505 :
5506 : // Now apply the branching bisimulation reduction algorithm. If there
5507 : // are no taus, this will automatically yield strong bisimulation.
5508 261 : bisim_partitioner_dnj<LTS_TYPE> bisim_part(l, branching,
5509 : preserve_divergence);
5510 :
5511 : // Assign the reduced LTS
5512 261 : bisim_part.finalize_minimized_LTS();
5513 261 : }
5514 :
5515 :
5516 : /// \brief Checks whether the two initial states of two LTSs are strong or
5517 : /// (divergence-preserving) branching bisimilar.
5518 : /// \details This routine uses the O(m log n) branching bisimulation algorithm
5519 : /// developed in 2018 by David N. Jansen. It runs in O(m log n) time and uses
5520 : /// O(m) memory, where n is the number of states and m is the number of
5521 : /// transitions.
5522 : ///
5523 : /// The LTSs l1 and l2 are not usable anymore after this call.
5524 : /// \param[in,out] l1 A first transition system.
5525 : /// \param[in,out] l2 A second transistion system.
5526 : /// \param branching If true branching bisimulation is used,
5527 : /// otherwise strong bisimulation is
5528 : /// applied.
5529 : /// \param preserve_divergence If true and branching is true, preserve
5530 : /// tau loops on states.
5531 : /// \param generate_counter_examples (non-functional, only in the
5532 : /// interface for historical reasons)
5533 : /// \returns True iff the initial states of the transition systems l1 and l2
5534 : /// are ((divergence-preserving) branching) bisimilar.
5535 : template <class LTS_TYPE>
5536 16 : bool destructive_bisimulation_compare_dnj(LTS_TYPE& l1, LTS_TYPE& l2,
5537 : bool const branching = false, bool const preserve_divergence = false,
5538 : bool const generate_counter_examples = false,
5539 : const std::string& /*counter_example_file*/ = "", bool /*structured_output*/ = false)
5540 : {
5541 16 : if (generate_counter_examples)
5542 : {
5543 0 : mCRL2log(log::warning) << "The JGKW20 branching bisimulation "
5544 : "algorithm does not generate counterexamples.\n";
5545 : }
5546 16 : std::size_t init_l2(l2.initial_state() + l1.num_states());
5547 16 : detail::merge(l1, std::move(l2));
5548 16 : l2.clear(); // No use for l2 anymore.
5549 :
5550 : // Line 2.1: Find tau-SCCs and contract each of them to a single state
5551 16 : if (branching)
5552 : {
5553 0 : scc_partitioner<LTS_TYPE> scc_part(l1);
5554 0 : scc_part.replace_transition_system(preserve_divergence);
5555 0 : init_l2 = scc_part.get_eq_class(init_l2);
5556 16 : } else assert(!preserve_divergence);
5557 16 : assert(1 < l1.num_states());
5558 16 : bisim_partitioner_dnj<LTS_TYPE> bisim_part(l1, branching,
5559 : preserve_divergence);
5560 :
5561 32 : return bisim_part.in_same_class(l1.initial_state(), init_l2);
5562 16 : }
5563 :
5564 :
5565 : /// \brief Checks whether the two initial states of two LTSs are strong or
5566 : /// (divergence-preserving) branching bisimilar.
5567 : /// \details The LTSs l1 and l2 are first duplicated and subsequently reduced
5568 : /// modulo bisimulation. If memory is a concern, one could consider to use
5569 : /// destructive_bisimulation_compare(). This routine uses the O(m log n)
5570 : /// branching bisimulation algorithm developed in 2018 by David N. Jansen. It
5571 : /// runs in O(m log n) time and uses O(m) memory, where n is the number of
5572 : /// states and m is the number of transitions.
5573 : /// \param l1 A first transition system.
5574 : /// \param l2 A second transistion system.
5575 : /// \param branching If true branching bisimulation is used,
5576 : /// otherwise strong bisimulation is applied.
5577 : /// \param preserve_divergence If true and branching is true, preserve tau
5578 : /// loops on states.
5579 : /// \retval True iff the initial states of the transition systems l1 and l2
5580 : /// are ((divergence-preserving) branching) bisimilar.
5581 : template <class LTS_TYPE>
5582 : inline bool bisimulation_compare_dnj(const LTS_TYPE& l1, const LTS_TYPE& l2,
5583 : bool const branching = false, bool const preserve_divergence = false)
5584 : {
5585 : LTS_TYPE l1_copy(l1);
5586 : LTS_TYPE l2_copy(l2);
5587 : return destructive_bisimulation_compare_dnj(l1_copy, l2_copy, branching,
5588 : preserve_divergence);
5589 : }
5590 :
5591 : ///@} (end of group part_interface)
5592 :
5593 : } // end namespace detail
5594 : } // end namespace lts
5595 : } // end namespace mcrl2
5596 :
5597 : #endif // ifndef LIBLTS_BISIM_DNJ_H
|