mCRL2
Loading...
Searching...
No Matches
liblts_bisim_gj.h
Go to the documentation of this file.
1// Author(s): Jan Friso Groote (with edits by David N. Jansen)
2//
3// Copyright: see the accompanying file COPYING or copy at
4// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
5//
6// Distributed under the Boost Software License, Version 1.0.
7// (See accompanying file LICENSE_1_0.txt or copy at
8// http://www.boost.org/LICENSE_1_0.txt)
9
16
17// TODO:
18// Merge identifying whether there is a splitter and actual splitting (Done. No performance effect).
19// Use BLC lists for the main split.
20// Maintain a co-splitter and a splitter to enable a co-split.
21// Eliminate two pointers in transition_type (done).
22// JFG: Optimise swap.
23
24#ifndef LIBLTS_BISIM_GJ_H
25#define LIBLTS_BISIM_GJ_H
26
27//#include <forward_list>
28#include <deque>
32
33// Decided on 2024-10-07: I won't look into SAVE_BLC_MEMORY any more; we rather
34// would like to know whether the block_label_to_cotransition map can be replaced
35// by adding a pointer to cotransitions in every block.
36
37// If SAVE_BLC_MEMORY is defined, the BLC_indicators type does not include a
38// field end_same_BLC. In principle, one can trade some memory savings against
39// a longer running time. However, we have decided to not pursue this feature,
40// so the code with SAVE_BLC_MEMORY has not been tested and is probably still
41// buggy. Also, it cannot be defined at the same time as CO_SPLITTER_IN_BLC_LIST.
42// #define SAVE_BLC_MEMORY
43
44#ifndef SAVE_BLC_MEMORY
45 // If CO_SPLITTER_IN_BLC_LIST is defined, the co-splitter belonging to a splitter
46 // is found by ordering the BLC_indicators lists in a specific way: the co-splitter
47 // is always placed immediately before the main splitter in the respective list.
48 // (If CO_SPLITTER_IN_BLC_LIST is not defined, one uses a std::unordered_map to
49 // store for every pair <source block, action label> a transition to the respective
50 // co-splitter.)
51 // It seems that defining this constant is advantageous.
52 #define CO_SPLITTER_IN_BLC_LIST
53
54 // It seems that when we define this constant as well, it's a little faster.
55 #define CO_SPLITTER_IN_BLC_LIST_VARIANT
56#endif
57
58// If COUNT_R_U_STATUS_TIMES is defined, simple_splitB() counts how often every
59// step in the coroutines is executed. This helps to find the most efficient
60// arrangement of the checks to determine the step to be executed.
61//#define COUNT_R_U_STATUS_TIMES
62
63// If TRY_EFFICIENT_SWAP is defined, then splitting a block will try to swap more
64// efficiently: states that are already in an acceptable position in m_states_in_blocks
65// will not be moved. This may require some additional reading but fewer changes
66// of pointers.
67// However, a test pointed out that it is about 2% slower. As the code becomes
68// more complex with TRY_EFFICIENT_SWAP, I suggest to not use the option.
69//#define TRY_EFFICIENT_SWAP
70
71#ifndef NDEBUG
72 // If CHECK_COMPLEXITY_GJ is defined, macros are included to check running time
73 // constraints: In every iteration of a loop, some counter of a state or
74 // transition is increased, and no counter is allowed to exceed (log n + 1).
75 // In this way, one can ensure the overall O(m log n) time bound.
76 // (Details: Occasionally, if a loop runs over all states of a block, or over
77 // all transitions of a state, a counter is assigned to the block or state, to
78 // reduce the number of counters slightly.)
79 // This feature only works in debug mode.
80 #define CHECK_COMPLEXITY_GJ
81#endif
82
83#ifdef CHECK_COMPLEXITY_GJ
85 #define mCRL2complexity_gj(unit, call, info_for_debug) mCRL2complexity(unit, call, info_for_debug)
86#else
87 #define mCRL2complexity_gj(unit, call, info_for_debug) do{}while(0)
88#endif
89
90namespace mcrl2
91{
92namespace lts
93{
94namespace detail
95{
96
97template <class LTS_TYPE> class bisim_partitioner_gj;
98
99namespace bisimulation_gj
100{
101
102// Forward declaration.
103struct state_type_gj;
104struct block_type;
105struct transition_type;
107
108typedef std::size_t state_index;
109typedef std::size_t transition_index;
110typedef std::size_t block_index;
111
112
113typedef std::size_t label_index;
114typedef std::size_t constellation_index;
115typedef std::vector<outgoing_transition_type>::iterator outgoing_transitions_it;
116typedef std::vector<outgoing_transition_type>::const_iterator outgoing_transitions_const_it;
117
125
126// The function clear takes care that a container frees memory when it is cleared and it is large.
127template <class CONTAINER>
128void clear(CONTAINER& c)
129{
130 if (c.size()>1000) { c=CONTAINER(); } else { c.clear(); }
131}
132
133// Private linked list that uses less memory.
134
135template <class T>
136struct linked_list_node;
137
138template <class T>
140{
141 typedef std::ptrdiff_t difference_type;
145 typedef std::bidirectional_iterator_tag iterator_category;
146
148
150
152 : m_iterator(t)
153 {}
154
156 {
157 assert(nullptr != m_iterator);
158 *this=m_iterator->next();
159 return *this;
160 }
161
163 {
164 linked_list_iterator temp = *this;
165 operator ++();
166 return temp;
167 }
168
170 {
171 assert(nullptr != m_iterator);
172 *this=m_iterator->prev();
173 return *this;
174 }
175
177 {
178 linked_list_iterator temp = *this;
179 operator --();
180 return temp;
181 }
182
184 {
185 assert(nullptr != m_iterator);
186 return *m_iterator;
187 }
188
190 {
191 assert(nullptr != m_iterator);
192 return m_iterator;
193 }
194
195 bool operator !=(const linked_list_iterator other) const
196 {
197 return m_iterator!=other.m_iterator;
198 }
199
200 bool operator ==(const linked_list_iterator other) const
201 {
202 return m_iterator==other.m_iterator;
203 }
204
205};
206
207template <class T>
208struct linked_list_node: public T
209{
213
214 template <class... Args>
216 : T(std::forward<Args>(args)...),
217 m_next(next),
218 m_prev(prev)
219 {}
220
222 {
223 return m_next;
224 }
225
227 {
228 return m_prev;
229 }
230
232 {
233 return static_cast<T&>(*this);
234 }
235};
236
237template <class T>
239{
240 std::deque<linked_list_node<T> > m_content;
242};
243
244template <class T>
246{
248
251
253 {
254 return m_initial_node;
255 }
256
257 static iterator end()
258 {
259 return nullptr;
260 }
261
262 bool empty() const
263 {
264 return m_initial_node==nullptr;
265 }
266
267#ifndef NDEBUG
268 [[nodiscard]]
269 bool check_linked_list() const
270 {
271 if (empty())
272 {
273 return true;
274 }
276 if (i->prev()!=nullptr)
277 {
278 return false;
279 }
280 while (i->next()!=nullptr)
281 {
282 if (i->next()->prev()!=i)
283 {
284 return false;
285 }
286 i=i->next();
287 assert(i->prev()->next() == i);
288 }
289 return true;
290 }
291#endif
292
293 // Puts a new element before the current element indicated by pos.
294 // It is an error if pos == end().
295 template <class... Args>
296 iterator emplace(iterator pos, Args&&... args)
297 {
298 assert(nullptr != pos);
299 iterator new_position;
300 if (glla().m_free_list==nullptr)
301 {
302 new_position=&glla().m_content.emplace_back(pos, pos->prev(), std::forward<Args>(args)...);
303 }
304 else
305 {
306 // Take an element from the free list.
307 new_position=glla().m_free_list;
308 glla().m_free_list=glla().m_free_list->next();
309 new_position->content()=T(std::forward<Args>(args)...);
310 new_position->next()=pos;
311 new_position->prev()=pos->prev();
312 }
313 if (pos->prev()!=nullptr)
314 {
315 pos->prev()->next()=new_position;
316 }
317 else
318 {
319 m_initial_node=new_position;
320 }
321 pos->prev()=new_position;
322
323 return new_position;
324 }
325
326 // Puts a new element after the current element indicated by pos, unless
327 // pos==end(), in which it is put in front of the list.
328 template <class... Args>
329 iterator emplace_after(iterator pos, Args&&... args)
330 {
331 if (pos==nullptr)
332 {
333 return emplace_front(args...);
334 }
335
336 iterator new_position;
337 if (glla().m_free_list==nullptr)
338 {
339 new_position=&glla().m_content.emplace_back(pos->next(), pos, std::forward<Args>(args)...);
340 }
341 else
342 {
343 // Take an element from the free list.
344 new_position=glla().m_free_list;
345 glla().m_free_list=glla().m_free_list->next();
346 new_position->content()=T(std::forward<Args>(args)...);
347 new_position->next()=pos->next();
348 new_position->prev()=pos;
349 }
350 if (pos->next()!=nullptr)
351 {
352 pos->next()->prev()=new_position;
353 }
354 pos->next()=new_position;
355
356 return new_position;
357 }
358
359 template <class... Args>
360 iterator emplace_front(Args&&... args)
361 {
362 iterator new_position;
363 if (glla().m_free_list==nullptr)
364 {
365 new_position=&glla().m_content.emplace_back(m_initial_node, nullptr, std::forward<Args>(args)...); // Deliver the address to new position.
366 }
367 else
368 {
369 // Take an element from the free list.
370 new_position=glla().m_free_list;
371 glla().m_free_list=glla().m_free_list->next();
372 new_position->content()=T(std::forward<Args>(args)...);
373 new_position->next()=m_initial_node;
374 new_position->prev()=nullptr;
375 }
376 if (m_initial_node!=nullptr)
377 {
378 m_initial_node->prev()=new_position;
379 }
380 m_initial_node=new_position;
381
382 return new_position;
383 }
384
385 //iterator push_front(const T& t)
386 //{
387 // return emplace_front(t);
388 //}
389
390 // The function moves the element pointed at by from_pos (that is in the list
391 // indicated by the 2nd parameter) just after position to_pos (that is in
392 // this list). If to_pos == nullptr, move the element to the beginning of this
393 // list.
394 void splice_to_after(iterator const to_pos, linked_list<T>& other_list, iterator const from_pos)
395 {
396 // remove element from_pos from its original list
397 if (from_pos->next() != nullptr)
398 {
399 assert(from_pos == from_pos->next()->prev());
400 from_pos->next()->prev() = from_pos->prev();
401 }
402 if (from_pos->prev() != nullptr)
403 {
404 assert(from_pos == from_pos->prev()->next());
405 from_pos->prev()->next() = from_pos->next();
406 }
407 else
408 {
409 assert(from_pos == other_list.m_initial_node);
410 other_list.m_initial_node = from_pos->next();
411 }
412 // update the pointers of from_pos and insert from_pos into this list
413 from_pos->prev() = to_pos;
414 if (to_pos != nullptr)
415 {
416 from_pos->next() = to_pos->next();
417 to_pos->next() = from_pos;
418 }
419 else
420 {
421 from_pos->next() = m_initial_node;
422 m_initial_node = from_pos;
423 }
424 if (from_pos->next() != nullptr)
425 {
426 assert(to_pos == from_pos->next()->prev());
427 from_pos->next()->prev() = from_pos;
428 }
429 #ifndef NDEBUG
430 assert(check_linked_list());
431 assert(other_list.check_linked_list());
432 #endif
433 }
434
435 void erase(iterator const pos)
436 {
437 if (pos->next()!=nullptr)
438 {
439 assert(pos == pos->next()->prev());
440 pos->next()->prev()=pos->prev();
441 }
442 if (pos->prev()!=nullptr)
443 {
444 assert(pos == pos->prev()->next());
445 pos->prev()->next()=pos->next();
446 }
447 else
448 {
449 assert(pos == m_initial_node);
450 m_initial_node=pos->next();
451 }
452 pos->next()=glla().m_free_list;
453 glla().m_free_list=pos;
454#ifndef NDEBUG
455 pos->prev()=nullptr;
456#endif
457 }
458};
459
460// The struct below facilitates to walk through a LBC_list starting from an arbitrary transition.
461typedef std::vector<transition_index>::iterator BLC_list_iterator;
462typedef std::vector<transition_index>::const_iterator BLC_list_const_iterator;
463
465{
467 outgoing_transitions_it start_same_saC; // Refers to the last state with the same state, action and constellation,
468 // unless it is the last, which refers to the first state.
469
470 // The default initialiser does not initialize the fields of this struct.
472 {}
473
476 start_same_saC(sssaC)
477 {}
478};
479
480/* struct label_count_sum_triple
481// David suggests to call this a pair, not a triple. The triple is not really used.
482{
483 transition_index label_counter=0;
484 transition_index not_investigated=0;
485
486 // The default initialiser does not initialize the fields of this struct.
487 label_count_sum_triple()
488 {}
489};
490
491struct label_count_sum_triple: label_count_sum_triple
492{
493 transition_index cumulative_label_counter=0;
494
495 // The default initialiser does not initialize the fields of this struct.
496 label_count_sum_triple()
497 {}
498}; */
499
500// a pointer to a state, i.e. a reference to a state
502{
503 state_in_block_pointer(std::vector<state_type_gj>::iterator new_ref_state)
504 : ref_state(new_ref_state)
505 {}
506
508 {}
509
510 std::vector<state_type_gj>::iterator ref_state;
511
512 bool operator==(const state_in_block_pointer& other) const
513 {
514 return ref_state==other.ref_state;
515 }
516
517 bool operator!=(const state_in_block_pointer& other) const
518 {
519 return ref_state!=other.ref_state;
520 }
521};
522
523// a vector with an additional (internal) field to indicate how much work has been
524// done already on it.
526{
527 std::size_t m_todo_indicator=0;
528 std::vector<state_in_block_pointer> m_vec;
529
530 public:
531 //typedef std::vector<state_in_block_pointer>::iterator iterator;
532 typedef std::vector<state_in_block_pointer>::const_iterator const_iterator;
533
535 {
536 assert(!find(s));
537 m_vec.push_back(s);
538 }
539
540 // Move a state from the todo part to the definitive vector.
542 {
543 assert(!todo_is_empty());
544 assert(m_todo_indicator<m_vec.size());
547 return result;
548 }
549
550 std::size_t size() const
551 {
552 return m_vec.size();
553 }
554
555 std::size_t todo_is_empty() const
556 {
557 return m_vec.size()==m_todo_indicator;
558 }
559
560 std::size_t empty() const
561 {
562 return m_vec.empty();
563 }
564
565 bool find(const state_in_block_pointer s) const
566 {
567 return std::find(m_vec.begin(), m_vec.end(), s)!=m_vec.end();
568 }
569
571 {
572 return m_vec.begin();
573 }
574
576 {
577 return m_vec.end();
578 }
579
580 void clear()
581 {
584 }
585
587 {
588 m_todo_indicator=m_vec.size();
589 }
590};
591
592
593
594// Below the four main data structures are listed.
596{
598 std::vector<transition>::iterator start_incoming_transitions;
600 std::vector<state_in_block_pointer>::iterator ref_states_in_blocks;
602 transition_index counter=undefined; // This field is used to store local information while splitting. While set to -1 (undefined)
603 // it is considered to be undefined.
604 // When set to -2 (Rmarked) it is considered to be marked for being in R or R_todo.
605 #ifdef CHECK_COMPLEXITY_GJ
607 template<class LTS_TYPE>
608 std::string debug_id_short(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
609 {
610 assert(&partitioner.m_states.front() <= this);
611 assert(this <= &partitioner.m_states.back());
612 return std::to_string(this - &partitioner.m_states.front());
613 }
614
616 template<class LTS_TYPE>
617 std::string debug_id(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
618 {
619 return "state " + debug_id_short(partitioner);
620 }
621
623 #endif
624};
625
626// The following type gives the start and end indications of the transitions for the same block, label and constellation
627// in the array m_BLC_transitions.
629{
632 #ifndef SAVE_BLC_MEMORY
634 #endif
635
637 : start_same_BLC(start),
639 #ifndef SAVE_BLC_MEMORY
640 , end_same_BLC(end)
641 #endif
642 {}
643
644 #ifdef CHECK_COMPLEXITY_GJ
647 template<class LTS_TYPE>
648 std::string debug_id(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
649 {
650 assert(partitioner.m_BLC_transitions.begin() <= start_same_BLC);
651 BLC_list_const_iterator my_end_same_BLC = partitioner.calculate_end_same_BLC(*this);
652 assert(start_same_BLC <= my_end_same_BLC);
653 if (start_same_BLC == my_end_same_BLC)
654 {
655 return "Empty BLC slice at m_BLC_transitions[" + std::to_string(std::distance(partitioner.m_BLC_transitions.begin(), my_end_same_BLC)) + "]";
656 }
657 assert(my_end_same_BLC <= partitioner.m_BLC_transitions.end());
658 std::string result("BLC slice ");
659 result += partitioner.m_blocks[partitioner.m_states[partitioner.m_aut.get_transitions()[*start_same_BLC].from()].block].debug_id(partitioner);
660 result += " -> ";
661 result += partitioner.m_constellations[partitioner.m_blocks[partitioner.m_states[partitioner.m_aut.get_transitions()[*start_same_BLC].to()].block].constellation].debug_id(partitioner);
662 result += " containing the ";
663 if (std::distance<BLC_list_const_iterator>(start_same_BLC, my_end_same_BLC) > 1)
664 {
665 result += std::to_string(std::distance<BLC_list_const_iterator>(start_same_BLC, my_end_same_BLC));
666 result += " transitions ";
667 }
668 else
669 result += "transition ";
671 if (start_marked_BLC == iter)
672 {
673 result += "| ";
674 }
675 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
676 if (std::distance<BLC_list_const_iterator>(start_same_BLC, my_end_same_BLC) > 4)
677 {
678 ++iter;
679 result += start_marked_BLC == iter ? " | " : ", ";
680 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
681 result += std::next(iter) == start_marked_BLC ? " | ..."
682 : (std::next(iter) < start_marked_BLC && start_marked_BLC <= my_end_same_BLC - 3 ? ", ..|.." : ", ...");
683 iter = my_end_same_BLC - 3;
684 }
685 while (++iter != my_end_same_BLC)
686 {
687 result += start_marked_BLC == iter ? " | " : ", ";
688 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
689 }
690 if (start_marked_BLC == iter)
691 {
692 result += " |";
693 }
694 return result;
695 }
696
698 #endif
699};
700
702{
703 // The position of the transition type corresponds to m_aut.get_transitions().
704 // std::size_t from, label, to are found in m_aut.get_transitions().
706 outgoing_transitions_it ref_outgoing_transitions; // This refers to the position of this transition in m_outgoing_transitions.
707 // During initialisation m_outgoing_transitions contains the indices of this
708 // transition. After initialisation m_outgoing_transitions refers to the corresponding
709 // entry in m_BLC_transitions, of which the field transition contains the index
710 // of this transition.
711
712 #ifdef CHECK_COMPLEXITY_GJ
715 template<class LTS_TYPE>
716 std::string debug_id_short(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
717 {
718 assert(&partitioner.m_transitions.front() <= this);
719 assert(this <= &partitioner.m_transitions.back());
720 const transition& t = partitioner.m_aut.get_transitions()[this - &partitioner.m_transitions.front()];
721 return partitioner.m_states[t.from()].debug_id_short(partitioner) + " -" +
722 pp(partitioner.m_aut.action_label(t.label())) + "-> " +
723 partitioner.m_states[t.to()].debug_id_short(partitioner);
724 }
725
728 template<class LTS_TYPE>
729 std::string debug_id(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
730 {
731 return "transition " + debug_id_short(partitioner);
732 }
733
735#endif
736};
737
739{
742 std::vector<state_in_block_pointer>::iterator start_bottom_states;
743 std::vector<state_in_block_pointer>::iterator start_non_bottom_states;
744 std::vector<state_in_block_pointer>::iterator end_states;
745// David thinks that end_states may perhaps be suppressed.
746// We need the size of a block in two cases: to choose a small block in a constellation,
747// and to decide whether to abort a coroutine early in simple_splitB().
748// In both cases it is enough to get an upper bound on the size of the block,
749// and if a constellation is a contiguous slice in m_states_in_blocks (as I
750// suggested elsewhere), the constellation can provide this upper bound.
752
753 block_type(const std::vector<state_in_block_pointer>::iterator beginning_of_states, constellation_index c)
754 : constellation(c),
756 start_bottom_states(beginning_of_states),
757 start_non_bottom_states(beginning_of_states),
758 end_states(beginning_of_states),
760 {}
761
762 #ifdef CHECK_COMPLEXITY_GJ
764 template<class LTS_TYPE>
765 inline std::string debug_id(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
766 {
767 assert(!partitioner.m_blocks.empty());
768 assert(&partitioner.m_blocks.front() <= this);
769 assert(this <= &partitioner.m_blocks.back());
770 assert(partitioner.m_states_in_blocks.begin() <= start_bottom_states);
773 assert(end_states <= partitioner.m_states_in_blocks.end());
774 return "block [" + std::to_string(std::distance<std::vector<state_in_block_pointer>::const_iterator>(partitioner.m_states_in_blocks.begin(), start_bottom_states)) + "," + std::to_string(std::distance<std::vector<state_in_block_pointer>::const_iterator>(partitioner.m_states_in_blocks.begin(), end_states)) + ")"
775 " (#" + std::to_string(std::distance(&partitioner.m_blocks.front(), this)) + ")";
776 }
777
779 #endif
780};
781
783{
784 std::vector<state_in_block_pointer>::iterator start_const_states;
785 std::vector<state_in_block_pointer>::iterator end_const_states;
786 constellation_type(const std::vector<state_in_block_pointer>::iterator new_start, const std::vector<state_in_block_pointer>::iterator new_end)
787 : start_const_states(new_start),
788 end_const_states(new_end)
789 {}
790
791 #ifndef NDEBUG
793 template<class LTS_TYPE>
794 inline std::string debug_id(const bisim_partitioner_gj<LTS_TYPE>& partitioner) const
795 {
796 assert(&partitioner.m_constellations.front() <= this);
797 assert(this <= &partitioner.m_constellations.back());
798 return "constellation " + std::to_string(this - &partitioner.m_constellations.front());
799 }
800 #endif
801};
802
803} // end namespace bisimulation_gj
804
805
806/*=============================================================================
807= main class =
808=============================================================================*/
809
810
812
815template <class LTS_TYPE>
817{
818 protected:
819
820 typedef std::unordered_set<state_index> set_of_states_type;
821 typedef std::unordered_set<transition_index> set_of_transitions_type;
822 typedef std::vector<constellation_index> set_of_constellations_type;
823
824 #ifndef CO_SPLITTER_IN_BLC_LIST
825 typedef std::unordered_map<std::pair<block_index, label_index>, transition_index> block_label_to_size_t_map;
826 #endif
827
828 #ifndef NDEBUG
829 public: // needed for the debugging functions, e.g. debug_id().
830 #endif
832 LTS_TYPE& m_aut;
833
834 // Generic data structures.
835 std::vector<state_type_gj> m_states;
836 // std::vector<transition_index> m_incoming_transitions;
837 std::vector<outgoing_transition_type> m_outgoing_transitions;
838 // During refining this contains the index in m_BLC_transition, of which
839 // the transition field contains the index of the transition.
840 std::vector<transition_type> m_transitions;
841 std::vector<state_in_block_pointer> m_states_in_blocks;
842 std::vector<block_type> m_blocks;
843 std::vector<constellation_type> m_constellations;
844 // David suggests to allocate blocks and constellations in global_linked_list_administration.
845 // (There is a pool allocator that can be used like this in liblts_bisim_dnj.h.)
846 // Then, one can store pointers to block_type and constellation_type instead of numbers;
847 // the type checking of pointers is more strict than the type checking of integer types,
848 // so it becomes impossible to assign a constellation number to a block or v.v.
849 // Also, it will reduce the complexity of address calculations.
850 std::vector<transition_index> m_BLC_transitions;
851 protected:
852 std::vector<block_index> m_blocks_with_new_bottom_states;
853 // Below are the two vectors that contain the marked and unmarked states, which
854 // are internally split in a part for states to be investigated, and a part for
855 // states that belong definitively to this set.
857 std::vector<state_in_block_pointer> m_U_counter_reset_vector;
858 // The following variable contains all non trivial constellations.
860
861 #ifdef CO_SPLITTER_IN_BLC_LIST
862 std::vector<linked_list<BLC_indicators>::iterator> m_BLC_indicators_to_be_deleted;
863 #endif
864
866 const bool m_branching;
867
874
875 // The function assumes that m_branching is true and tests whether transition t is inert during initialisation under that condition
877 {
878 assert(m_branching);
879 return m_aut.is_tau(m_aut.apply_hidden_label_map(t.label())) && (!m_preserve_divergence || t.from() != t.to());
880 }
881
882 // The function tests whether transition t is inert during initialisation, i.e. when there is only one source/target block.
883 bool is_inert_during_init(const transition& t) const
884 {
886 }
887
888 // The function calculates the label index of transition t, where tau-self-loops get the special index m_aut.num_action_labels() if divergence needs to be preserved
890 {
891 label_index result = m_aut.apply_hidden_label_map(t.label());
892 if (m_preserve_divergence && (assert(m_branching), t.from() == t.to()) && m_aut.is_tau(result))
893 {
894 return m_aut.num_action_labels();
895 }
896 return result;
897 }
898
899 // The function decides whether iterator it points to a transition that is part
900 // of the BLC set ind. (This is non-trivial if SAVE_BLC_MEMORY.)
902 {
903 assert(ind.start_same_BLC <= ind.start_marked_BLC);
904 assert(ind.start_same_BLC <= it);
905 #ifdef SAVE_BLC_MEMORY
906 if (m_BLC_transitions.end() <= it)
907 {
908 return false;
909 }
910 const transition& first_t = m_aut.get_transitions()[*ind.start_same_BLC];
911 const transition& it_t = m_aut.get_transitions()[*it];
912 return m_states[first_t.from()].block == m_states[it_t.from()].block &&
913 label_or_divergence(first_t) == label_or_divergence(it_t) &&
914 m_blocks[m_states[first_t.to()].block].constellation == m_blocks[m_states[it_t.to()].block].constellation;
915 #else
916 assert(ind.start_marked_BLC <= ind.end_same_BLC);
917 return it < ind.end_same_BLC;
918 #endif
919 }
920
921 // This function returns true iff the BLC set ind contains at least one
922 // marked transition.
924 {
925 assert(ind.start_same_BLC <= ind.start_marked_BLC);
926 #ifndef SAVE_BLC_MEMORY
927 assert(ind.start_marked_BLC <= ind.end_same_BLC);
928 #endif
929 return points_into_BLC_set(ind.start_marked_BLC, ind);
930 }
931
932 // This function unmarks all transitions in BLC set ind.
933 // If SAVE_BLC_MEMORY, it is linear in the number of marked transitions, but
934 // that is ok, as transition markings come with the right to visit the
935 // transitions.
937 {
938 assert(ind.start_same_BLC <= ind.start_marked_BLC);
939 #ifdef SAVE_BLC_MEMORY
940 BLC_list_iterator end_same_BLC = ind.start_marked_BLC;
941 for (; assert(ind.start_same_BLC <= end_same_BLC), points_into_BLC_set(end_same_BLC, ind); ++end_same_BLC)
942 {
943 // mCRL2complexity(m_aut.get_transitions()[*ind], add_work(...), *this);
944 // not needed, as we unmark transitions and we are allowed to visit
945 // every marked transition a fixed number of times
946 }
947 ind.start_marked_BLC = end_same_BLC;
948 #else
950 #endif
951 }
952
953 public:
954#ifndef NDEBUG
955 // This suppresses many unused variable warnings.
956
957 // This function calculates the end of the transitions in BLC set ind.
958 // Because it is slow if SAVE_BLC_MEMORY, it is only defined in debug mode
959 // and should only be called in debugging functions.
961 {
962 assert(ind.start_same_BLC <= ind.start_marked_BLC);
963 #ifdef SAVE_BLC_MEMORY
965 for (; assert(ind.start_same_BLC <= it), points_into_BLC_set(it, ind); ++it)
966 {}
967 return it;
968 #else
969 return ind.end_same_BLC;
970 #endif
971 }
972
973 // This function counts the number of marked transitions. Because it is slow
974 // if SAVE_BLC_MEMORY, it is only defined in debug mode and should only be
975 // called in debugging functions.
977 {
978 return std::distance<BLC_list_const_iterator>(ind.start_marked_BLC, calculate_end_same_BLC(ind));
979 }
980
981 protected:
982 void check_transitions(const bool check_temporary_complexity_counters, const bool check_block_to_constellation = true) const
983 {
984 // This routine can only be used after initialisation.
985 for(std::size_t ti=0; ti<m_transitions.size(); ++ti)
986 {
987 const BLC_list_const_iterator btc_ti = m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions;
988 assert(*btc_ti==ti);
989
990 const transition& t=m_aut.get_transitions()[ti];
991 assert(&*m_states[t.to()].start_incoming_transitions <= &t);
992 assert(&t <= &*std::prev(m_aut.get_transitions().end()));
993 if (t.to() + 1 != m_states.size())
994 {
995 assert(&t <= &*std::prev(m_states[t.to() + 1].start_incoming_transitions));
996 }
997
998 assert(m_states[t.from()].start_outgoing_transitions <= m_transitions[ti].ref_outgoing_transitions);
999 if (t.from() + 1 == m_states.size())
1000 assert(m_transitions[ti].ref_outgoing_transitions < m_outgoing_transitions.end());
1001 else
1002 assert(m_transitions[ti].ref_outgoing_transitions < m_states[t.from() + 1].start_outgoing_transitions);
1003
1004 assert(m_transitions[ti].transitions_per_block_to_constellation->start_same_BLC <= btc_ti);
1005 assert(points_into_BLC_set(btc_ti, *m_transitions[ti].transitions_per_block_to_constellation));
1006
1007 if (!check_block_to_constellation)
1008 continue;
1009
1010 const block_index b=m_states[t.from()].block;
1011
1012 const label_index t_label = label_or_divergence(t);
1013 bool found=false;
1014 for(const BLC_indicators& blc: m_blocks[b].block_to_constellation)
1015 {
1016 if (blc.start_same_BLC != blc.start_marked_BLC)
1017 {
1018 assert(blc.start_same_BLC < blc.start_marked_BLC);
1019 assert(blc.start_same_BLC <= std::prev(blc.start_marked_BLC));
1020 assert(points_into_BLC_set(std::prev(blc.start_marked_BLC), blc));
1021 }
1022 #ifndef SAVE_BLC_MEMORY
1023 assert(blc.start_same_BLC < blc.end_same_BLC);
1024 #endif
1025 transition& first_t = m_aut.get_transitions()[*blc.start_same_BLC];
1026 assert(b == m_states[first_t.from()].block);
1027 if (t_label == label_or_divergence(first_t) &&
1028 m_blocks[m_states[first_t.to()].block].constellation == m_blocks[m_states[t.to()].block].constellation)
1029 {
1030// if (found) { std::cerr << "Found multiple BLC sets with transitions (block " << b << " -" << m_aut.action_label(t.label()) << "-> constellation " << m_blocks[m_states[t.to()].block].constellation << ")\n"; }
1031 assert(!found);
1032 assert(blc.start_same_BLC <= btc_ti);
1033 assert(points_into_BLC_set(btc_ti, blc));
1034 assert(&blc == &*m_transitions[ti].transitions_per_block_to_constellation);
1035 found = true;
1036 }
1037 }
1038 assert(found);
1039 if (check_temporary_complexity_counters)
1040 {
1041 #ifdef CHECK_COMPLEXITY_GJ
1042 const block_index targetb = m_states[t.to()].block;
1044 const unsigned max_targetC = check_complexity::log_n - check_complexity::ilog2(number_of_states_in_constellation(m_blocks[targetb].constellation));
1045 const unsigned max_targetB = check_complexity::log_n - check_complexity::ilog2(number_of_states_in_block(targetb));
1046 mCRL2complexity_gj(&m_transitions[ti], no_temporary_work(max_sourceB, max_targetC, max_targetB,
1047 0 == m_states[t.from()].no_of_outgoing_inert_transitions), *this);
1048 #endif
1049 }
1050 }
1051 }
1052
1053 [[nodiscard]]
1054 bool check_data_structures(const std::string& tag, const bool initialisation=false, const bool check_temporary_complexity_counters=true) const
1055 {
1056assert(!initialisation);
1057 mCRL2log(log::debug) << "Check data structures: " << tag << ".\n";
1058 assert(m_states.size()==m_aut.num_states());
1059 assert(m_outgoing_transitions.size()==m_aut.num_transitions());
1060
1061 // Check that the elements in m_states are well formed.
1062 for(std::vector<state_type_gj>::iterator si=const_cast<std::vector<state_type_gj>&>(m_states).begin(); si<m_states.cend(); si++)
1063 {
1064 const state_type_gj& s=*si;
1065
1066 assert(s.counter==undefined);
1067 assert(m_blocks[s.block].start_bottom_states<m_blocks[s.block].start_non_bottom_states);
1068 assert(m_blocks[s.block].start_non_bottom_states<=m_blocks[s.block].end_states);
1069
1070 assert(std::find(m_blocks[s.block].start_bottom_states, m_blocks[s.block].end_states,state_in_block_pointer(si))!=m_blocks[s.block].end_states);
1071
1072 // The construction below is added to enable compilation on Windows.
1073 const outgoing_transitions_const_it end_it1=std::next(si)>=m_states.end() ? m_outgoing_transitions.cend() : std::next(si)->start_outgoing_transitions;
1075 {
1076 const transition& t=m_aut.get_transitions()
1077 [/*initialisation ?it->transition :*/*it->ref_BLC_transitions];
1078// if (t.from() != si) { std::cerr << m_transitions[*it->ref_BLC_transitions].debug_id(*this) << " is an outgoing transition of state " << si << "!\n"; }
1079 assert(m_states.cbegin()+t.from()==si);
1080 assert(!initialisation /*|| m_transitions[it->transition].ref_outgoing_transitions==it*/);
1081 assert(/*initialisation ||*/ m_transitions[*it->ref_BLC_transitions].ref_outgoing_transitions==it);
1082 assert((it->start_same_saC>it && it->start_same_saC<m_outgoing_transitions.end() &&
1083 ((it+1)->start_same_saC==it->start_same_saC || (it+1)->start_same_saC<=it)) ||
1084 (it->start_same_saC<=it && (it+1==m_outgoing_transitions.end() || (it+1)->start_same_saC>it)));
1085// if (it->start_same_saC < it->start_same_saC->start_same_saC) { std::cerr << "Now checking transitions " << m_transitions[*it->start_same_saC->ref_BLC_transitions].debug_id_short(*this) << " ... " << m_transitions[*it->start_same_saC->start_same_saC->ref_BLC_transitions].debug_id_short(*this) << '\n'; }
1086 const label_index t_label = label_or_divergence(t);
1087 // The following for loop is only executed if it is the last transition in the saC-slice.
1088 for(outgoing_transitions_const_it itt=it->start_same_saC; itt<it->start_same_saC->start_same_saC; ++itt)
1089 {
1090 const transition& t1=m_aut.get_transitions()
1091 [/*initialisation?itt->transition:*/*itt->ref_BLC_transitions];
1092// if (t1.from()!=si) { assert(!initialisation); std::cerr << m_transitions[*itt->ref_BLC_transitions].debug_id(*this) << " does not start in state " << si << '\n'; }
1093 assert(m_states.cbegin()+t1.from()==si);
1094 assert(label_or_divergence(t1) == t_label);
1095 assert(m_blocks[m_states[t.to()].block].constellation==m_blocks[m_states[t1.to()].block].constellation);
1096 }
1097 }
1098 assert(s.ref_states_in_blocks->ref_state==si);
1099
1100 // Check that for each state the outgoing transitions satisfy the following invariant.
1101 // First there are inert transitions. Then there are other transitions sorted per label
1102 // and constellation.
1103 std::unordered_set<std::pair<label_index, constellation_index> > constellations_seen;
1104
1105 // The construction below is to enable translation on Windows.
1106 const outgoing_transitions_const_it end_it2=std::next(si)>=m_states.end() ? m_outgoing_transitions.cend() : std::next(si)->start_outgoing_transitions;
1108 {
1109 const transition& t=m_aut.get_transitions()[/*initialisation?it->transition:*/ *it->ref_BLC_transitions];
1111 // Check that if the target constellation, if not new, is equal to the target constellation of the previous outgoing transition.
1112 const constellation_index t_to_constellation = m_blocks[m_states[t.to()].block].constellation;
1113 if (constellations_seen.count(std::pair(label,t_to_constellation))>0)
1114 {
1115 assert(it!=s.start_outgoing_transitions);
1116 const transition& old_t=m_aut.get_transitions()[/*initialisation?std::prev(it)->transition:*/ *std::prev(it)->ref_BLC_transitions];
1117 assert(label_or_divergence(old_t) == label);
1118 assert(t_to_constellation==m_blocks[m_states[old_t.to()].block].constellation);
1119 }
1120 constellations_seen.emplace(label,t_to_constellation);
1121 }
1122 }
1123 // Check that the elements in m_transitions are well formed.
1124 if (!initialisation)
1125 {
1126 check_transitions(check_temporary_complexity_counters);
1127 }
1128 // Check that the elements in m_blocks are well formed.
1129 {
1130 set_of_transitions_type all_transitions;
1131 for(block_index bi=0; bi<m_blocks.size(); ++bi)
1132 {
1133 const block_type& b=m_blocks[bi];
1138
1139 assert(m_states_in_blocks.begin() <= c.start_const_states);
1142 assert(b.start_non_bottom_states <= b.end_states);
1143 assert(b.end_states <= c.end_const_states);
1144 assert(c.end_const_states <= m_states_in_blocks.end());
1145
1146 #ifdef CHECK_COMPLEXITY_GJ
1149 #endif
1150 for(std::vector<state_in_block_pointer>::const_iterator is=b.start_bottom_states;
1151 is!=b.start_non_bottom_states; ++is)
1152 {
1153 assert(is->ref_state->block==bi);
1154 assert(is->ref_state->no_of_outgoing_inert_transitions==0);
1155 if (check_temporary_complexity_counters)
1156 {
1157 mCRL2complexity_gj(is->ref_state, no_temporary_work(max_B, true), *this);
1158 }
1159 }
1160 for(std::vector<state_in_block_pointer>::const_iterator is=b.start_non_bottom_states;
1161 is!=b.end_states; ++is)
1162 {
1163 assert(is->ref_state->block==bi);
1164 assert(is->ref_state->no_of_outgoing_inert_transitions>0);
1165 // Because there cannot be new bottom states among the non-bottom states,
1166 // we can always check the temporary work of non-bottom states:
1167 mCRL2complexity_gj(is->ref_state, no_temporary_work(max_B, false), *this);
1168 }
1169 // Because a block has no temporary or new-bottom-state-related counters,
1170 // we can always check its temporary work:
1171 mCRL2complexity_gj(&b, no_temporary_work(max_C, max_B), *this);
1172
1173 assert(b.block_to_constellation.check_linked_list());
1175 ind!=b.block_to_constellation.end(); ++ind)
1176 {
1177 #ifndef SAVE_BLC_MEMORY
1178 assert(ind->start_same_BLC < ind->end_same_BLC);
1179 #endif
1180 const transition& first_transition=m_aut.get_transitions()[*(ind->start_same_BLC)];
1181 const label_index first_transition_label = label_or_divergence(first_transition);
1182 for(BLC_list_const_iterator i=ind->start_same_BLC; assert(ind->start_same_BLC <= i), points_into_BLC_set(i, *ind); ++i)
1183 {
1184 const transition& t=m_aut.get_transitions()[*i];
1185 assert(m_transitions[*i].transitions_per_block_to_constellation == ind);
1186 all_transitions.emplace(*i);
1187 assert(m_states[t.from()].block==bi);
1188 assert(m_blocks[m_states[t.to()].block].constellation==
1189 m_blocks[m_states[first_transition.to()].block].constellation);
1190 assert(label_or_divergence(t) == first_transition_label);
1191 if (is_inert_during_init(t) && m_blocks[m_states[t.to()].block].constellation==m_blocks[bi].constellation)
1192 {
1193 // The inert transitions should be in the first element of block_to_constellation:
1194 assert(b.block_to_constellation.begin()==ind);
1195 }
1196 }
1197 if (check_temporary_complexity_counters)
1198 {
1199 mCRL2complexity_gj(ind, no_temporary_work(max_C, check_complexity::log_n - check_complexity::ilog2(number_of_states_in_constellation(m_blocks[m_states[first_transition.to()].block].constellation))), *this);
1200 }
1201 }
1202 }
1203 assert(initialisation || all_transitions.size()==m_transitions.size());
1204 // destruct all_transitions here
1205 }
1206
1207 // TODO: Check that the elements in m_constellations are well formed.
1208 {
1209 std::unordered_set<block_index> all_blocks;
1210 for(constellation_index ci=0; ci<m_constellations.size(); ci++)
1211 {
1212 for (std::vector<state_in_block_pointer>::const_iterator constln_it=m_constellations[ci].start_const_states; constln_it<m_constellations[ci].end_const_states; )
1213 {
1214 const block_index bi=constln_it->ref_state->block;
1215 assert(bi<m_blocks.size());
1216 assert(all_blocks.emplace(bi).second); // Block is not already present. Otherwise a block occurs in two constellations.
1217 constln_it = m_blocks[bi].end_states;
1218 }
1219 }
1220 assert(all_blocks.size()==m_blocks.size());
1221 // destruct all_blocks here
1222 }
1223
1224 // Check that the states in m_states_in_blocks refer to with ref_states_in_block to the right position.
1225 // and that a state is correctly designated as a (non-)bottom state.
1226 for(std::vector<state_in_block_pointer>::const_iterator si=m_states_in_blocks.begin(); si!=m_states_in_blocks.end(); ++si)
1227 {
1228 assert(si==si->ref_state->ref_states_in_blocks);
1229 }
1230
1231 // Check that the blocks in m_blocks_with_new_bottom_states are bottom states.
1233 {
1234 assert(m_blocks[bi].contains_new_bottom_states);
1235 }
1236
1237 // Check that the non-trivial constellations are non trivial.
1239 {
1240 // There are at least two blocks in a non-trivial constellation.
1241 const block_index first_bi=m_constellations[ci].start_const_states->ref_state->block;
1242 const block_index last_bi=std::prev(m_constellations[ci].end_const_states)->ref_state->block;
1243 assert(first_bi != last_bi);
1244 }
1245 return true;
1246 }
1247
1272 [[nodiscard]]
1273 bool check_stability(const std::string& tag,
1274 const std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >* calM = nullptr,
1275 const std::pair<BLC_list_iterator, BLC_list_iterator>* calM_elt = nullptr,
1277 const constellation_index old_constellation = null_constellation
1278 #else
1279 const block_label_to_size_t_map* const block_label_to_cotransition = nullptr
1280 #endif
1281 ) const
1282 {
1283 mCRL2log(log::debug) << "Check stability: " << tag << ".\n";
1284 for(block_index bi=0; bi<m_blocks.size(); ++bi)
1285 {
1286 const block_type& b=m_blocks[bi];
1288 ind!=b.block_to_constellation.end(); ++ind)
1289 {
1290 set_of_states_type all_source_bottom_states;
1291
1292 #ifndef SAVE_BLC_MEMORY
1293 assert(ind->start_same_BLC < ind->end_same_BLC);
1294 #endif
1295 const transition& first_t = m_aut.get_transitions()[*ind->start_same_BLC];
1296 const label_index first_t_label = label_or_divergence(first_t);
1297 const bool all_transitions_in_BLC_are_inert = is_inert_during_init(first_t) &&
1298 m_blocks[m_states[first_t.to()].block].constellation == b.constellation;
1299 assert(!all_transitions_in_BLC_are_inert || b.block_to_constellation.begin() == ind);
1300 for(BLC_list_const_iterator i=ind->start_same_BLC; assert(ind->start_same_BLC <= i), points_into_BLC_set(i, *ind); ++i)
1301 {
1302 assert(m_BLC_transitions.begin() <= i);
1303 assert(i < m_BLC_transitions.end());
1304 const transition& t=m_aut.get_transitions()[*i];
1305// if (m_states[t.from()].block != bi) { std::cerr << m_transitions[*ind->start_same_BLC].debug_id(*this) << " should start in block " << bi << '\n'; }
1306 assert(m_states[t.from()].block == bi);
1307 assert(label_or_divergence(t) == first_t_label);
1308 assert(m_blocks[m_states[t.to()].block].constellation == m_blocks[m_states[first_t.to()].block].constellation);
1309 if (is_inert_during_init(t) && m_blocks[m_states[t.to()].block].constellation==b.constellation)
1310 {
1311 assert(all_transitions_in_BLC_are_inert);
1312 }
1313 else
1314 {
1315 // This is a constellation-non-inert transition.
1316 assert(!all_transitions_in_BLC_are_inert);
1317 if (0 == m_states[t.from()].no_of_outgoing_inert_transitions)
1318 {
1319 assert(b.start_bottom_states <= m_states[t.from()].ref_states_in_blocks);
1320 assert(m_states[t.from()].ref_states_in_blocks < b.start_non_bottom_states);
1321 all_source_bottom_states.emplace(t.from());
1322 }
1323 else
1324 {
1325 assert(b.start_non_bottom_states <= m_states[t.from()].ref_states_in_blocks);
1326 assert(m_states[t.from()].ref_states_in_blocks < b.end_states);
1327 }
1328 }
1329 }
1330 assert(all_source_bottom_states.size() <= static_cast<std::size_t>(std::distance(b.start_bottom_states, b.start_non_bottom_states)));
1331 // check that every bottom state has a transition in this BLC entry:
1332 bool eventual_instability_is_ok = true;
1333 bool eventual_marking_is_ok = true;
1334 if (!all_transitions_in_BLC_are_inert &&
1335 all_source_bottom_states.size()!=static_cast<std::size_t>(std::distance(b.start_bottom_states, b.start_non_bottom_states)))
1336 {
1337 // only splitters should be instable.
1338 mCRL2log(log::debug) << "Not all " << std::distance(b.start_bottom_states, b.start_non_bottom_states)
1339 << (m_branching ? " bottom states have a transition in the " : " states have a transition in the ")
1340 << ind->debug_id(*this) << ": transitions found from states";
1341 for (set_of_states_type::iterator asbc_it = all_source_bottom_states.begin() ; asbc_it != all_source_bottom_states.end() ; ++asbc_it) { mCRL2log(log::debug) << ' ' << *asbc_it; }
1342 mCRL2log(log::debug) << '\n';
1343 eventual_instability_is_ok = false;
1344 }
1345 if (has_marked_transitions(*ind))
1346 {
1347 // only splitters should contain marked transitions.
1348 mCRL2log(log::debug) << ind->debug_id(*this) << " contains " << count_marked_transitions(*ind) << " marked transitions.\n";
1349 eventual_marking_is_ok = false;
1350 }
1351 if (m_blocks[bi].contains_new_bottom_states)
1352 {
1353 /* I would like the following to check more closely because in a
1354 block with new bottom states, one should have...
1355 if (!eventual_marking_is_ok)
1356 {
1357 eventual_marking_is_ok = true;
1358 for (BLC_list_const_iterator i=ind->start_marked_BLC; assert(ind->start_same_BLC <= i), points_into_BLC_set(i, *ind); ++i)
1359 {
1360 const state_index from = m_aut.get_transitions()[*i].from();
1361 // assert(m_states[from].block == bi); -- already checked earlier
1362 if (0 != m_states[from].no_of_outgoing_inert_transitions)
1363 {
1364 // the state is a non-bottom state
1365 eventual_marking_is_ok = false;
1366 break;
1367 }
1368 }
1369 if (eventual_marking_is_ok)
1370 {
1371 mCRL2log(log::debug) << " This is ok because all marked transitions begin in new bottom states of block " << bi << ".\n";
1372 eventual_instability_is_ok = true;
1373 }
1374 } */
1375 if (!(eventual_instability_is_ok && eventual_marking_is_ok))
1376 {
1377 mCRL2log(log::debug) << " This is ok because block " << bi << " contains new bottom states.\n";
1378 eventual_instability_is_ok = true;
1379 eventual_marking_is_ok = true;
1380 }
1381 }
1382 if (!(eventual_instability_is_ok && eventual_marking_is_ok) && nullptr != calM && calM->begin() != calM->end())
1383 {
1384 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >::const_iterator calM_iter = calM->begin();
1385 if (nullptr != calM_elt)
1386 {
1387 for(;;)
1388 {
1389 assert(calM->end() != calM_iter);
1390 if (calM_iter->first <= calM_elt->first && calM_elt->second <= calM_iter->second)
1391 {
1392 break;
1393 }
1394 ++calM_iter;
1395 }
1396 if (calM_elt->first <= ind->start_same_BLC && ind->start_same_BLC <= calM_elt->second && !points_into_BLC_set(calM_elt->second, *ind))
1397 {
1398 mCRL2log(log::debug) << " This is ok because the BLC set (block " << bi << " -" << m_aut.action_label(first_t.label()) << "-> constellation " << m_blocks[m_states[first_t.to()].block].constellation << ") is soon going to be a main splitter.\n";
1399 eventual_instability_is_ok = true;
1400 eventual_marking_is_ok = true;
1401 }
1402 else
1403 {
1404 #ifdef CO_SPLITTER_IN_BLC_LIST
1405 if (old_constellation == m_blocks[m_states[first_t.to()].block].constellation)
1406 {
1407 const linked_list<BLC_indicators>::iterator main_splitter = std::next(ind);
1408 if (main_splitter != m_blocks[bi].block_to_constellation.end())
1409 {
1410 assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
1411 const transition& main_t = m_aut.get_transitions()[*main_splitter->start_same_BLC];
1412 assert(m_states[main_t.from()].block == bi);
1413 if (label_or_divergence(first_t) == label_or_divergence(main_t) &&
1414 m_blocks[m_states[main_t.to()].block].constellation == m_constellations.size() - 1)
1415 {
1416// std::cerr << "Corresponding main splitter: " << main_splitter->debug_id(*this) << '\n';
1417 if (calM_elt->first <= main_splitter->start_same_BLC &&
1418 main_splitter->start_same_BLC <= calM_elt->second && !points_into_BLC_set(calM_elt->second, *main_splitter))
1419 {
1420 assert(m_constellations.size() - 1 == m_blocks[m_states[main_t.to()].block].constellation);
1421 mCRL2log(log::debug) << " This is ok because the BLC set (block " << bi << " -" << m_aut.action_label(first_t.label()) << "-> constellation " << old_constellation << ") is soon going to be a co-splitter.\n";
1422 eventual_instability_is_ok = true;
1423 eventual_marking_is_ok = true;
1424 break;
1425 }
1426// else { std::cerr << "Main splitter is not in calM_elt = [" << std::distance(m_BLC_transitions.begin(), calM_elt->first) << ',' << std::distance(m_BLC_transitions.begin(), calM_elt->second) << ")\n" };
1427 }
1428 }
1429 }
1430 #else
1431 if (nullptr != block_label_to_cotransition)
1432 {
1433 for (BLC_list_const_iterator ind_iter = calM_elt->second; ind_iter > calM_elt->first; )
1434 {
1435 #ifndef SAVE_BLC_MEMORY
1436 assert(m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->start_same_BLC < m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->end_same_BLC);
1437 #endif
1438 ind_iter = m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->start_same_BLC;
1439 const transition& t = m_aut.get_transitions()[*ind_iter];
1440 block_label_to_size_t_map::const_iterator co_iter = block_label_to_cotransition->find(std::pair(m_states[t.from()].block, label_or_divergence(t)));
1441 if (block_label_to_cotransition->end() != co_iter && null_transition != co_iter->second && m_transitions[co_iter->second].transitions_per_block_to_constellation == ind)
1442 {
1443 const transition& co_t = m_aut.get_transitions()[co_iter->second];
1444 mCRL2log(log::debug) << " This is ok because the BLC set (block " << bi << " -" << m_aut.action_label(co_t.label()) << "-> constellation " << m_blocks[m_states[co_t.to()].block].constellation << ") is soon going to be a co-splitter.\n";
1445 eventual_instability_is_ok = true;
1446 eventual_marking_is_ok = true;
1447 break;
1448 }
1449 }
1450 }
1451 #endif
1452 }
1453 ++calM_iter;
1454 }
1455 for(; !(eventual_instability_is_ok && eventual_marking_is_ok) && calM->end() != calM_iter; ++calM_iter)
1456 {
1457 if (calM_iter->first <= ind->start_same_BLC && ind->start_same_BLC <= calM_iter->second && !points_into_BLC_set(calM_iter->second, *ind))
1458 {
1459 mCRL2log(log::debug) << " This is ok because the BLC set (block " << bi << " -" << m_aut.action_label(first_t.label()) << "-> constellation " << m_blocks[m_states[first_t.to()].block].constellation << ") is going to be a main splitter later.\n";
1460 eventual_instability_is_ok = true;
1461 eventual_marking_is_ok = true;
1462 }
1463 else
1464 {
1465 #ifdef CO_SPLITTER_IN_BLC_LIST
1466 if (old_constellation == m_blocks[m_states[first_t.to()].block].constellation)
1467 {
1468 const linked_list<BLC_indicators>::iterator main_splitter = std::next(ind);
1469 if (main_splitter != m_blocks[bi].block_to_constellation.end())
1470 {
1471 assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
1472 const transition& main_t = m_aut.get_transitions()[*main_splitter->start_same_BLC];
1473 assert(m_states[main_t.from()].block == bi);
1474 if (label_or_divergence(first_t) == label_or_divergence(main_t) &&
1475 m_blocks[m_states[main_t.to()].block].constellation == m_constellations.size() - 1)
1476 {
1477 if (calM_iter->first <= main_splitter->start_same_BLC &&
1478 main_splitter->start_same_BLC <= calM_iter->second && !points_into_BLC_set(calM_iter->second, *main_splitter))
1479 {
1480 assert(m_constellations.size() - 1 == m_blocks[m_states[main_t.to()].block].constellation);
1481 mCRL2log(log::debug) << " This is ok because the BLC set (block " << bi << " -" << m_aut.action_label(first_t.label()) << "-> constellation " << old_constellation << ") is soon going to be a co-splitter.\n";
1482 eventual_instability_is_ok = true;
1483 eventual_marking_is_ok = true;
1484 break;
1485 }
1486// else { std::cerr << "Main splitter is not in calM_iter = [" << std::distance(m_BLC_transitions.begin(), calM_iter->first) << ',' << std::distance(m_BLC_transitions.begin(), calM_iter->second) << ")\n" };
1487 }
1488 }
1489 }
1490 #else
1491 if (nullptr != block_label_to_cotransition)
1492 {
1493 for (BLC_list_const_iterator ind_iter = calM_iter->second; ind_iter > calM_iter->first; )
1494 {
1495 #ifndef SAVE_BLC_MEMORY
1496 assert(m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->start_same_BLC < m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->end_same_BLC);
1497 #endif
1498 ind_iter = m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->start_same_BLC;
1499 const transition& t = m_aut.get_transitions()[*ind_iter];
1500 block_label_to_size_t_map::const_iterator co_iter = block_label_to_cotransition->find(std::pair(m_states[t.from()].block, label_or_divergence(t)));
1501 if (block_label_to_cotransition->end() != co_iter && null_transition != co_iter->second && m_transitions[co_iter->second].transitions_per_block_to_constellation == ind)
1502 {
1503 const transition& co_t = m_aut.get_transitions()[co_iter->second];
1504 mCRL2log(log::debug) << " This is ok because the BLC set (block " << bi << " -" << m_aut.action_label(co_t.label()) << "-> constellation " << m_blocks[m_states[co_t.to()].block].constellation << ") is going to be a co-splitter later.\n";
1505 eventual_instability_is_ok = true;
1506 eventual_marking_is_ok = true;
1507 break;
1508 }
1509 }
1510 }
1511 #endif
1512 }
1513 }
1514 }
1515 #ifndef CO_SPLITTER_IN_BLC_LIST
1516 if (!(eventual_instability_is_ok && eventual_marking_is_ok) && nullptr != block_label_to_cotransition)
1517 {
1518 block_label_to_size_t_map::const_iterator co_iter = block_label_to_cotransition->find(std::pair(m_states[first_t.from()].block, label_or_divergence(first_t)));
1519 if (block_label_to_cotransition->end() != co_iter && null_transition != co_iter->second && m_transitions[co_iter->second].transitions_per_block_to_constellation == ind)
1520 {
1521 mCRL2log(log::debug) << " (This BLC set is registered as co-splitter but there is no corresponding main splitter.)\n";
1522 }
1523 }
1524 #endif
1525 if (!eventual_marking_is_ok && 1 >= number_of_states_in_block(bi))
1526 {
1527 mCRL2log(log::debug) << " (This is ok because the source block contains only 1 state.)\n";
1528 eventual_marking_is_ok = true;
1529 }
1530 assert(eventual_marking_is_ok);
1531 assert(eventual_instability_is_ok);
1532 }
1533 }
1534 mCRL2log(log::debug) << "Check stability finished: " << tag << ".\n";
1535 return true;
1536 }
1537
1540 , const block_label_to_size_t_map* const block_label_to_cotransition = nullptr
1541 #endif
1542 ) const
1543 {
1544 mCRL2log(log::debug) << "\n BLC_List\n";
1545 for(const BLC_indicators& blc_it: m_blocks[bi].block_to_constellation)
1546 {
1547 mCRL2log(log::debug) << "\n BLC_sublist: " << std::distance<BLC_list_const_iterator>(m_BLC_transitions.begin(),blc_it.start_same_BLC) << " -- "
1548 << std::distance<BLC_list_const_iterator>(m_BLC_transitions.begin(),calculate_end_same_BLC(blc_it)) << "\n";
1549 for(BLC_list_const_iterator i=blc_it.start_same_BLC; assert(blc_it.start_same_BLC <= i), points_into_BLC_set(i, blc_it); ++i)
1550 {
1551 if (i == blc_it.start_marked_BLC)
1552 {
1553 mCRL2log(log::debug) << " (The following transitions are marked.)\n";
1554 }
1555 const transition& t=m_aut.get_transitions()[*i];
1556 mCRL2log(log::debug) << " " << t.from() << " -" << m_aut.action_label(t.label()) << "-> " << t.to();
1557 if (is_inert_during_init(t) && m_states[t.from()].block == m_states[t.to()].block)
1558 {
1559 mCRL2log(log::debug) << " (block-inert)";
1560 }
1561 else if (is_inert_during_init(t) && m_blocks[m_states[t.from()].block].constellation == m_blocks[m_states[t.to()].block].constellation)
1562 {
1563 mCRL2log(log::debug) << " (constellation-inert)";
1564 }
1565 else if (m_preserve_divergence && t.from() == t.to() && m_aut.is_tau(m_aut.apply_hidden_label_map(t.label())))
1566 {
1567 mCRL2log(log::debug) << " (divergent self-loop)";
1568 }
1569 else
1570 {
1571 mCRL2log(log::debug) << " (to constellation " << m_blocks[m_states[t.to()].block].constellation << ')';
1572 }
1573 #ifndef CO_SPLITTER_IN_BLC_LIST
1574 if (nullptr != block_label_to_cotransition)
1575 {
1576 const block_label_to_size_t_map::const_iterator co_tr = block_label_to_cotransition->find(std::pair(bi, label_or_divergence(t)));
1577 if (co_tr != block_label_to_cotransition->end() && co_tr->second == *i)
1578 {
1579 mCRL2log(log::debug) << " (co-splitter transition for <block " << bi << ", label " << m_aut.action_label(t.label()) << ">)";
1580 }
1581 }
1582 #endif
1583 mCRL2log(log::debug) << '\n';
1584 }
1585 }
1586 mCRL2log(log::debug) << " BLC_List end\n";
1587 }
1588
1589
1590 void print_data_structures(const std::string& header,
1592 const block_label_to_size_t_map* const block_label_to_cotransition = nullptr,
1593 #endif
1594 const bool initialisation=false) const
1595 {
1596 assert(!initialisation);
1597 if (!mCRL2logEnabled(log::debug)) return;
1598 mCRL2log(log::debug) << "========= PRINT DATASTRUCTURE: " << header << " =======================================\n";
1599 mCRL2log(log::debug) << "++++++++++++++++++++ States ++++++++++++++++++++++++++++\n";
1600 for(state_index si=0; si<m_states.size(); ++si)
1601 {
1602 mCRL2log(log::debug) << "State " << si <<" (Block: " << m_states[si].block <<"):\n";
1603 mCRL2log(log::debug) << " #Inert outgoing transitions: " << m_states[si].no_of_outgoing_inert_transitions << '\n';
1604
1605 mCRL2log(log::debug) << " Incoming transitions:\n";
1606 std::vector<transition>::const_iterator end=(si+1==m_states.size()?m_aut.get_transitions().end():m_states[si+1].start_incoming_transitions);
1607 for(std::vector<transition>::const_iterator it=m_states[si].start_incoming_transitions; it!=end; ++it)
1608 {
1609 mCRL2log(log::debug) << " " << ptr(*it) << "\n";
1610 }
1611
1612 mCRL2log(log::debug) << " Outgoing transitions:\n";
1613 for(outgoing_transitions_const_it it=m_states[si].start_outgoing_transitions;
1614 it!=m_outgoing_transitions.end() &&
1615 (si+1>=m_states.size() || it!=m_states[si+1].start_outgoing_transitions);
1616 ++it)
1617 {
1618 const transition& t=m_aut.get_transitions()[/*initialisation?it->transition:*/ *it->ref_BLC_transitions];
1619 mCRL2log(log::debug) << " " << t.from() << " -" << m_aut.action_label(t.label()) << "-> " << t.to() << "\n";;
1620 }
1621 mCRL2log(log::debug) << " Ref states in blocks: " << std::distance<std::vector<state_type_gj>::const_iterator>(m_states.cbegin(), m_states[si].ref_states_in_blocks->ref_state) << ". Must be " << si <<".\n";
1622 mCRL2log(log::debug) << "---------------------------------------------------\n";
1623 }
1624 mCRL2log(log::debug) << "++++++++++++++++++++ Transitions ++++++++++++++++++++++++++++\n";
1625 for(state_index ti=0; ti<m_transitions.size(); ++ti)
1626 {
1627 const transition& t=m_aut.get_transitions()[ti];
1628 mCRL2log(log::debug) << "Transition " << ti <<": " << t.from()
1629 << " -" << m_aut.action_label(t.label()) << "-> "
1630 << t.to() << "\n";
1631 }
1632
1633 mCRL2log(log::debug) << "++++++++++++++++++++ Blocks ++++++++++++++++++++++++++++\n";
1634 for(block_index bi=0; bi<m_blocks.size(); ++bi)
1635 {
1636 mCRL2log(log::debug) << " Block " << bi << " (const: " << m_blocks[bi].constellation
1637 << (m_branching ? "):\n Bottom states: " : "):\n States: ");
1638 for(std::vector<state_in_block_pointer>::const_iterator sit=m_blocks[bi].start_bottom_states;
1639 sit!=m_blocks[bi].start_non_bottom_states; ++sit)
1640 {
1641 mCRL2log(log::debug) << std::distance<std::vector<state_type_gj>::const_iterator>(m_states.cbegin(), sit->ref_state) << " ";
1642 }
1643 if (m_branching)
1644 {
1645 mCRL2log(log::debug) << "\n Non-bottom states: ";
1646 for(typename std::vector<state_in_block_pointer>::const_iterator sit=m_blocks[bi].start_non_bottom_states;
1647 sit!=m_blocks[bi].end_states; ++sit)
1648 {
1649 mCRL2log(log::debug) << std::distance<std::vector<state_type_gj>::const_iterator>(m_states.cbegin(), sit->ref_state) << " ";
1650 }
1651 }
1652 else
1653 {
1654 assert(m_blocks[bi].start_non_bottom_states == m_blocks[bi].end_states);
1655 }
1656 if (!initialisation)
1657 {
1660 , block_label_to_cotransition
1661 #endif
1662 );
1663 }
1664 mCRL2log(log::debug) << "\n";
1665 }
1666
1667 mCRL2log(log::debug) << "++++++++++++++++++++ Constellations ++++++++++++++++++++++++++++\n";
1668 for(constellation_index ci=0; ci<m_constellations.size(); ++ci)
1669 {
1670 mCRL2log(log::debug) << " Constellation " << ci << ":\n";
1671 mCRL2log(log::debug) << " Blocks in constellation:";
1672 for (std::vector<state_in_block_pointer>::const_iterator constln_it=m_constellations[ci].start_const_states; constln_it<m_constellations[ci].end_const_states; )
1673 {
1674 const block_index bi=constln_it->ref_state->block;
1675 mCRL2log(log::debug) << " " << bi;
1676 constln_it = m_blocks[bi].end_states;
1677 }
1678 mCRL2log(log::debug) << "\n";
1679 }
1680 mCRL2log(log::debug) << "Non-trivial constellations:";
1682 {
1683 mCRL2log(log::debug) << " " << ci;
1684 }
1685
1686 mCRL2log(log::debug) << "\n++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n";
1687 mCRL2log(log::debug) << "Outgoing transitions:\n";
1688
1690 {
1691 const transition& t=m_aut.get_transitions()[/*initialisation?pi->transition:*/ *pi->ref_BLC_transitions];
1692 mCRL2log(log::debug) << " " << t.from() << " -" << m_aut.action_label(t.label()) << "-> " << t.to();
1693 if (m_outgoing_transitions.begin() <= pi->start_same_saC && pi->start_same_saC < m_outgoing_transitions.end())
1694 {
1695 const transition& t1=m_aut.get_transitions()[/*initialisation?pi->start_same_saC->transition:*/ *pi->start_same_saC->ref_BLC_transitions];
1696 mCRL2log(log::debug) << " \t(same saC: " << t1.from() << " -" << m_aut.action_label(t1.label()) << "-> " << t1.to();
1697 const label_index t_label = label_or_divergence(t);
1698 if (pi->start_same_saC->start_same_saC == pi)
1699 {
1700 // Transition t must be the beginning and/or the end of a saC-slice
1701 if (pi->start_same_saC >= pi && pi > m_outgoing_transitions.begin())
1702 {
1703 // Transition t must be the beginning of a saC-slice
1704 const transition& prev_t = m_aut.get_transitions()[/*initialisation ? std::prev(pi)->transition :*/ *std::prev(pi)->ref_BLC_transitions];
1705 if (prev_t.from() == t.from() &&
1706 label_or_divergence(prev_t) == t_label &&
1707 m_blocks[m_states[prev_t.to()].block].constellation == m_blocks[m_states[t.to()].block].constellation)
1708 {
1709 mCRL2log(log::debug) << " -- error: not the beginning of a saC-slice";
1710 }
1711 }
1712 if (pi->start_same_saC <= pi && std::next(pi) < m_outgoing_transitions.end())
1713 {
1714 // Transition t must be the end of a saC-slice
1715 const transition& next_t = m_aut.get_transitions()[/*initialisation ? std::next(pi)->transition :*/ *std::next(pi)->ref_BLC_transitions];
1716 if (next_t.from() == t.from() &&
1717 label_or_divergence(next_t) == t_label &&
1718 m_blocks[m_states[next_t.to()].block].constellation == m_blocks[m_states[t.to()].block].constellation)
1719 {
1720 mCRL2log(log::debug) << " -- error: not the end of a saC-slice";
1721 }
1722 }
1723 }
1724 else if (pi->start_same_saC > pi ? pi->start_same_saC->start_same_saC > pi : pi->start_same_saC->start_same_saC < pi)
1725 {
1726 mCRL2log(log::debug) << " -- error: not in its own saC-slice";
1727 }
1728 mCRL2log(log::debug) << ')';
1729 }
1730 mCRL2log(log::debug) << '\n';
1731 }
1732
1733 mCRL2log(log::debug) << "++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n";
1734 mCRL2log(log::debug) << "New bottom blocks to be investigated:";
1735
1737 {
1738 mCRL2log(log::debug) << " " << bi;
1739 }
1740
1741 mCRL2log(log::debug) << "\n========= END PRINT DATASTRUCTURE: " << header << " =======================================\n";
1742 }
1743#endif // ifndef NDEBUG
1744
1745 public:
1759 const bool branching = false,
1760 const bool preserve_divergence = false)
1761 : m_aut(aut),
1762 m_states(aut.num_states()),
1763 m_outgoing_transitions(aut.num_transitions()),
1764 m_transitions(aut.num_transitions()),
1765 m_states_in_blocks(aut.num_states()),
1766 m_blocks(1,{m_states_in_blocks.begin(),0}),
1767 m_constellations(1,constellation_type(m_states_in_blocks.begin(), m_states_in_blocks.end())), // Algorithm 1, line 1.2.
1768 m_BLC_transitions(aut.num_transitions()),
1769 m_branching(branching),
1770 m_preserve_divergence(preserve_divergence)
1771 {
1772//log::logger::set_reporting_level(log::debug);
1773
1775 mCRL2log(log::verbose) << "Start initialisation.\n";
1777 mCRL2log(log::verbose) << "After initialisation there are " << m_blocks.size() << " equivalence classes. Start refining. \n";
1779 assert(check_data_structures("READY"));
1780 }
1781
1782
1787 std::size_t num_eq_classes() const
1788 {
1789 return m_blocks.size();
1790 }
1791
1792
1801 {
1802 assert(si<m_states.size());
1803 return m_states[si].block;
1804 }
1805
1806
1820 {
1821 // The transitions are most efficiently directly extracted from the block_to_constellation lists in blocks.
1822 std::vector<transition> T;
1823 for(block_index bi=0; bi<m_blocks.size(); ++bi)
1824 {
1825 const block_type& B=m_blocks[bi];
1826 //mCRL2complexity_gj(&B, add_work(..., 1), *this);
1827 // Because every block is touched exactly once, we do not store a physical counter for this.
1828 for(const BLC_indicators blc_ind: B.block_to_constellation)
1829 {
1830 // mCRL2complexity_gj(&blc_ind, add_work(..., 1), *this);
1831 // Because every BLC set is touched exactly once, we do not store a physical counter for this.
1832 #ifndef SAVE_BLC_MEMORY
1833 assert(blc_ind.start_same_BLC < blc_ind.end_same_BLC);
1834 #endif
1835 const transition& t= m_aut.get_transitions()[*blc_ind.start_same_BLC];
1836 const transition_index new_to=get_eq_class(t.to());
1837 if (!is_inert_during_init(t) || bi!=new_to)
1838 {
1839 T.emplace_back(bi, t.label(), new_to);
1840 }
1841 }
1842 }
1843 m_aut.clear_transitions();
1844 for (const transition& t: T)
1845 {
1846 //mCRL2complexity_gj(..., add_work(..., 1), *this);
1847 // we do not add a counter because every transition has been generated by one of the above iterations.
1848 m_aut.add_transition(t);
1849 }
1850 //
1851 // Merge the states, by setting the state labels of each state to the
1852 // concatenation of the state labels of its equivalence class.
1853
1854 if (m_aut.has_state_info()) /* If there are no state labels this step is not needed */
1855 {
1856 /* Create a vector for the new labels */
1857 std::vector<typename LTS_TYPE::state_label_t> new_labels(num_eq_classes());
1858
1859
1860 for(std::size_t i=0; i<m_aut.num_states(); ++i)
1861 {
1862 //mCRL2complexity_gj(&m_states[i], add_work(..., 1), *this);
1863 // Because every state is touched exactly once, we do not store a physical counter for this.
1864 const state_index new_index(get_eq_class(i));
1865 new_labels[new_index]=new_labels[new_index]+m_aut.state_label(i);
1866 }
1867
1868 m_aut.set_num_states(num_eq_classes());
1869 for (std::size_t i=0; i<num_eq_classes(); ++i)
1870 {
1871 // mCRL2complexity_gj(&m_blocks[i], add_work(check_complexity::finalize_minimized_LTS__set_labels_of_block, 1), *this);
1872 // Because every block is touched exactly once, we do not store a physical counter for this.
1873 m_aut.set_state_label(i, new_labels[i]);
1874 }
1875 }
1876 else
1877 {
1878 m_aut.set_num_states(num_eq_classes());
1879 }
1880
1881 m_aut.set_initial_state(get_eq_class(m_aut.initial_state()));
1882 }
1883
1884
1889 bool in_same_class(state_index const s, state_index const t) const
1890 {
1891 return get_eq_class(s) == get_eq_class(t);
1892 }
1893 protected:
1894
1895 std::string ptr(const transition& t) const
1896 {
1897 return std::to_string(t.from()) + " -" + pp(m_aut.action_label(t.label())) + "-> " + std::to_string(t.to());
1898 }
1899
1900 std::string ptr(const transition_index ti) const
1901 {
1902 const transition& t=m_aut.get_transitions()[ti];
1903 return ptr(t);
1904 }
1905
1906 /*--------------------------- main algorithm ----------------------------*/
1907
1908 /*----------------- splitB -- Algorithm 3 of [GJ 2024] -----------------*/
1909
1911 {
1912 assert(m_blocks[B].start_bottom_states < m_blocks[B].end_states);
1913 return std::distance(m_blocks[B].start_bottom_states, m_blocks[B].end_states);
1914 }
1915
1917 {
1918 assert(m_constellations[C].start_const_states < m_constellations[C].end_const_states);
1919 return std::distance(m_constellations[C].start_const_states, m_constellations[C].end_const_states);
1920 }
1921
1923 typename std::vector<state_in_block_pointer>::iterator pos1,
1924 typename std::vector<state_in_block_pointer>::iterator pos2)
1925 {
1926 assert(m_states_in_blocks.begin() <= pos1);
1927 assert(pos1 < m_states_in_blocks.end());
1928 assert(m_states_in_blocks.begin() <= pos2);
1929 assert(pos2 < m_states_in_blocks.end());
1930 assert(pos1!=pos2);
1931 std::swap(*pos1,*pos2);
1932 pos1->ref_state->ref_states_in_blocks=pos1;
1933 pos2->ref_state->ref_states_in_blocks=pos2;
1934 }
1935
1937 typename std::vector<state_in_block_pointer>::iterator pos1,
1938 typename std::vector<state_in_block_pointer>::iterator pos2)
1939 {
1940 if (pos1!=pos2)
1941 {
1943 }
1944 }
1945
1946 // Move pos1 to pos2, pos2 to pos3 and pos3 to pos1;
1947 // The function requires that pos3 lies in between pos1 and pos2.
1948 // It also requires that pos1 and pos2 are different.
1950 typename std::vector<state_in_block_pointer>::iterator pos1,
1951 typename std::vector<state_in_block_pointer>::iterator pos2,
1952 typename std::vector<state_in_block_pointer>::iterator pos3)
1953 {
1954 assert(m_states_in_blocks.begin()<=pos2);
1955 assert(pos2<pos3); assert(pos3<=pos1);
1956 assert(pos1<m_states_in_blocks.end());
1957 if (pos1==pos3)
1958 {
1959 std::swap(*pos1,*pos2);
1960 }
1961 else
1962 {
1963 const state_in_block_pointer temp=*pos1;
1964 *pos1=*pos3;
1965 *pos3=*pos2;
1966 *pos2=temp;
1967
1968 pos3->ref_state->ref_states_in_blocks=pos3;
1969 }
1970 pos1->ref_state->ref_states_in_blocks=pos1;
1971 pos2->ref_state->ref_states_in_blocks=pos2;
1972 }
1973
1974 // Move pos1 to pos2, pos2 to pos3 and pos3 to pos1;
1975 // The function requires that pos3 lies in between pos1 and pos2.
1977 typename std::vector<state_in_block_pointer>::iterator pos1,
1978 typename std::vector<state_in_block_pointer>::iterator pos2,
1979 typename std::vector<state_in_block_pointer>::iterator pos3)
1980 {
1981 if (pos2==pos3)
1982 {
1984 }
1985 else
1986 {
1988 }
1989/* assert(m_states_in_blocks.begin() <= pos2);
1990 assert(pos2 <= pos3); assert(pos3 <= pos1);
1991 assert(pos1 < m_states_in_blocks.end());
1992 if (pos1 == pos3)
1993 {
1994 if (pos1 == pos2)
1995 {
1996 return;
1997 }
1998 std::swap(*pos1,*pos2);
1999 }
2000 else if (pos2 == pos3)
2001 {
2002 std::swap(*pos1,*pos2);
2003 }
2004 else
2005 {
2006 const state_index temp=*pos1;
2007 *pos1=*pos3;
2008 *pos3=*pos2;
2009 *pos2=temp;
2010
2011 m_states[*pos3].ref_states_in_blocks=pos3;
2012 }
2013 m_states[*pos1].ref_states_in_blocks=pos1;
2014 m_states[*pos2].ref_states_in_blocks=pos2; */
2015 }
2016
2017 // Swap the range [pos1, pos1 + count) with the range [pos2, pos2 + count).
2018 // pos1 must come before pos2.
2019 // (If the ranges overlap, only swap the non-overlapping part.)
2020 // The function requires count > 0 and pos1 < pos2
2021 // (this is sufficient for how it's used below: to swap new bottom states into their proper places;
2022 // also, the work counters assume that [pos2, pos2 + count) is assigned the work.)
2024 typename std::vector<state_in_block_pointer>::iterator pos1,
2025 typename std::vector<state_in_block_pointer>::iterator pos2,
2026 state_index count
2027 #ifdef CHECK_COMPLEXITY_GJ
2028 , const state_index max_B
2029 #endif
2030 )
2031 {
2032 assert(0 < count);
2033 assert(count <= m_states_in_blocks.size());
2034 // if (pos1 > pos2) std::swap(pos1, pos2);
2035 assert(m_states_in_blocks.begin() <= pos1);
2036 assert(pos1 < pos2); // in particular, they are not allowed to be equal
2037 assert(pos2 <= m_states_in_blocks.end() - count);
2038 {
2039 std::make_signed<state_index>::type overlap = std::distance(pos2, pos1 + count);
2040 if (overlap > 0)
2041 {
2042 count -= overlap;
2043 pos2 += overlap;
2044 }
2045 }
2046 state_in_block_pointer temp=*pos1;
2047 while (--count > 0)
2048 {
2050 *pos1 = *pos2;
2051 pos1->ref_state->ref_states_in_blocks=pos1;
2052 ++pos1;
2053 *pos2 = *pos1;
2054 pos2->ref_state->ref_states_in_blocks=pos2;
2055 ++pos2;
2056 }
2057 *pos1 = *pos2;
2058 pos1->ref_state->ref_states_in_blocks=pos1;
2059 *pos2 = temp;
2060 pos2->ref_state->ref_states_in_blocks=pos2;
2061
2062 #ifndef NDEBUG
2063 for (std::vector<state_type_gj>::const_iterator si = m_states.cbegin(); si < m_states.cend(); ++si)
2064 {
2065 assert(si==si->ref_states_in_blocks->ref_state);
2066 }
2067 #endif
2068 }
2069
2070 // marks the transition indicated by out_pos.
2071 // (We use an outgoing_transitions_it because it points to the m_BLC_transitions entry that needs to be updated.)
2073 {
2074 BLC_list_iterator old_pos = out_pos->ref_BLC_transitions;
2075 linked_list<BLC_indicators>::iterator ind = m_transitions[*old_pos].transitions_per_block_to_constellation;
2076 assert(ind->start_same_BLC <= old_pos);
2077 assert(old_pos < m_BLC_transitions.end());
2078 assert(points_into_BLC_set(old_pos, *ind));
2079 if (old_pos < ind->start_marked_BLC)
2080 {
2081 // The transition is not marked
2082 assert(ind->start_same_BLC < ind->start_marked_BLC);
2083 BLC_list_iterator new_pos = std::prev(ind->start_marked_BLC);
2084 assert(ind->start_same_BLC <= new_pos);
2085 assert(new_pos < m_BLC_transitions.end());
2086 assert(points_into_BLC_set(new_pos, *ind));
2087 if (old_pos < new_pos)
2088 {
2089 std::swap(*old_pos, *new_pos);
2090 m_transitions[*old_pos].ref_outgoing_transitions->ref_BLC_transitions = old_pos;
2091 assert(out_pos == m_transitions[*new_pos].ref_outgoing_transitions);
2092 out_pos->ref_BLC_transitions = new_pos;
2093 }
2094 ind->start_marked_BLC--;
2095 }
2096
2097 #ifndef NDEBUG
2098 for (BLC_list_const_iterator it = m_BLC_transitions.cbegin(); it < m_BLC_transitions.cend(); ++it)
2099 {
2100 assert(m_transitions[*it].ref_outgoing_transitions->ref_BLC_transitions == it);
2101 assert(m_transitions[*it].transitions_per_block_to_constellation->start_same_BLC <= it);
2102 assert(points_into_BLC_set(it, *m_transitions[*it].transitions_per_block_to_constellation));
2103 }
2104 #endif
2105 }
2106
2107 // Split the block B by moving the elements in R to the front in m_states, and add a
2108 // new element B_new at the end of m_blocks referring to R. Adapt B.start_bottom_states,
2109 // B.start_non_bottom_states and B.end_states, and do the same for B_new.
2111 const block_index B,
2112 std::vector<state_in_block_pointer>::iterator first_bottom_state_in_R,
2113 std::vector<state_in_block_pointer>::iterator last_bottom_state_in_R,
2114 const todo_state_vector& R
2115 #ifdef TRY_EFFICIENT_SWAP
2116 , const transition_index marking_value
2117 #endif
2118 )
2119 {
2120//std::cerr << "block_index split_block_B_into_R_and_BminR(" << m_blocks[B].debug_id(*this)
2121//<< ",&m_states_in_blocks[" << std::distance(m_states_in_blocks.begin(), first_bottom_state_in_R)
2122//<< "..." << std::distance(m_states_in_blocks.begin(), last_bottom_state_in_R)
2123//<< "),R = {";
2124//for(auto s:R){ std::cerr << ' ' << std::distance(m_states.begin(), s.ref_state); }
2125//std::cerr << " }," << static_cast<std::make_signed<transition_index>::type>(marking_value) << ")\n";
2126//std::cerr << "SPLIT BLOCK " << B << " by removing"; for(auto s = first_bottom_state_in_R; s < last_bottom_state_in_R; ++s){ std::cerr << ' ' << std::distance(m_states.begin(), s->ref_state);} for(auto s:R){ std::cerr << ' ' << std::distance(m_states.begin(), s.ref_state); } std::cerr << '\n';
2127 assert(m_blocks[B].start_bottom_states <= first_bottom_state_in_R);
2128 assert(first_bottom_state_in_R <= last_bottom_state_in_R);
2129 assert(last_bottom_state_in_R <= m_blocks[B].start_non_bottom_states);
2130 // Basic administration. Make a new block and add it to the current constellation.
2131 const block_index B_new=m_blocks.size();
2132 const constellation_index ci = m_blocks[B].constellation;
2133 m_blocks.emplace_back(m_blocks[B].start_bottom_states,ci);
2134 #ifdef CHECK_COMPLEXITY_GJ
2135 m_blocks[B_new].work_counter = m_blocks[B].work_counter;
2136 #endif
2137 if (m_constellations[ci].start_const_states->ref_state->block==std::prev(m_constellations[ci].end_const_states)->ref_state->block) // This constellation is trivial.
2138 {
2139 // This constellation is trivial, as it will be split add it to the non trivial constellations.
2140 assert(std::find(m_non_trivial_constellations.begin(),
2142 ci)==m_non_trivial_constellations.end());
2143 m_non_trivial_constellations.emplace_back(ci);
2144 }
2145
2146 // Carry out the split.
2147 #ifdef CHECK_COMPLEXITY_GJ
2148 // The size of the new block is not yet fixed.
2149 const state_index max_B = check_complexity::log_n - check_complexity::ilog2(std::distance(first_bottom_state_in_R, last_bottom_state_in_R) + R.size());
2150 #endif
2151 if (m_blocks[B].start_bottom_states < first_bottom_state_in_R)
2152 {
2153 multiple_swap_states_in_states_in_block(m_blocks[B].start_bottom_states, first_bottom_state_in_R,
2154 std::distance(first_bottom_state_in_R, last_bottom_state_in_R)
2155 #ifdef CHECK_COMPLEXITY_GJ
2156 , max_B
2157 #endif
2158 );
2159 last_bottom_state_in_R = m_blocks[B].start_bottom_states + std::distance(first_bottom_state_in_R, last_bottom_state_in_R);
2160 first_bottom_state_in_R = m_blocks[B].start_bottom_states;
2161 }
2162
2163 assert(m_blocks[B_new].start_bottom_states==first_bottom_state_in_R);
2164 m_blocks[B_new].start_non_bottom_states=last_bottom_state_in_R;
2165 // Update the block pointers for R-bottom states:
2166 for(std::vector<state_in_block_pointer>::iterator s_it=first_bottom_state_in_R; s_it<last_bottom_state_in_R; ++s_it)
2167 {
2169 max_B), *this);
2170//std::cerr << "MOVE STATE TO NEW BLOCK: " << std::distance(m_states.begin(), s_it->ref_state) << "\n";
2171 assert(B==s_it->ref_state->block);
2172 s_it->ref_state->block=B_new;
2173 assert(s_it->ref_state->ref_states_in_blocks==s_it);
2174 }
2175 // Now the R bottom states are in the correct position, and we don't have to look into them any more.
2176 #ifdef TRY_EFFICIENT_SWAP
2177 // (We could perhaps extend the efficient swap to include the R bottom states,
2178 // but I think that is too complicated for me to think through.)
2179 const std::vector<state_in_block_pointer>::iterator BminR_start_bottom_states=last_bottom_state_in_R+R.size();
2180 const std::vector<state_in_block_pointer>::iterator BminR_start_non_bottom_states=m_blocks[B].start_non_bottom_states+R.size();
2181
2182 if (R.size()>0)
2183 {
2184 std::vector<state_in_block_pointer>::iterator move_next_R_non_bottom_state_to=last_bottom_state_in_R;
2185 std::vector<state_in_block_pointer>::iterator move_next_R_non_bottom_state_to_end=BminR_start_bottom_states;
2186 // Move BminR bottom states out of the way.
2187 std::vector<state_in_block_pointer>::iterator move_next_BminR_bottom_state_to=m_blocks[B].start_non_bottom_states;
2188 if (move_next_BminR_bottom_state_to<move_next_R_non_bottom_state_to_end)
2189 {
2190 // there are many R-non-bottom states, so we will need to move all BminR bottom states.
2191 // (Later, the remaining R-non-bottom states will be placed.)
2192 move_next_R_non_bottom_state_to_end=move_next_BminR_bottom_state_to;
2193 move_next_BminR_bottom_state_to=BminR_start_bottom_states;
2194 }
2195 if (R.size()*2>=static_cast<state_index>(std::distance(m_blocks[B].start_non_bottom_states, m_blocks[B].end_states)))
2196 {
2197 // At least half the non-bottom states go into R.
2198 // It is more economical to disregard R completely and look only at ....counter==marking_value.
2199
2200 // Move BminR bottom states out of the way.
2201 std::vector<state_in_block_pointer>::iterator take_next_R_non_bottom_state_from=BminR_start_non_bottom_states;
2202 #ifdef CHECK_COMPLEXITY_GJ
2203 std::vector<state_in_block_pointer>::const_iterator account_for_skipped_BminR_states=R.begin();
2204 #endif
2205 for (; move_next_R_non_bottom_state_to<move_next_R_non_bottom_state_to_end;
2206 ++move_next_R_non_bottom_state_to, ++move_next_BminR_bottom_state_to)
2207 {
2208 // Now the BminR-bottom state at *move_next_R_non_bottom_state_to should move to *move_next_BminR_bottom_state_to.
2209 // Find some R-non-bottom state that can move to *move_next_R_non_bottom_state_to:
2210 if (marking_value==move_next_BminR_bottom_state_to->ref_state->counter)
2211 {
2212 // There is a R-non-bottom state at *move_next_BminR_bottom_state_to already:
2213 swap_states_in_states_in_block_never_equal(move_next_R_non_bottom_state_to, move_next_BminR_bottom_state_to);
2214 }
2215 else
2216 {
2217 // *move_next_BminR_bottom_state_to now contains a BminR-non-bottom state.
2218 // Find a place where to move it to, namely some R-non-bottom state that needs to be moved.
2219 while (assert(take_next_R_non_bottom_state_from<m_blocks[B].end_states),
2220 marking_value!=take_next_R_non_bottom_state_from->ref_state->counter)
2221 {
2222 #ifdef CHECK_COMPLEXITY_GJ
2223 // assign the work in this loop to some R non-bottom state.
2224 // (This is possible because there are no fewer R non-bottom states than BminR non-bottom states.)
2225 assert(account_for_skipped_BminR_states<R.end());
2226 mCRL2complexity_gj(account_for_skipped_BminR_states->ref_state, add_work(check_complexity::split_block_B_into_R_and_BminR__skip_over_state, max_B), *this);
2227 ++account_for_skipped_BminR_states;
2228 #endif
2229 ++take_next_R_non_bottom_state_from;
2230 }
2231 swap_states_in_states_in_block_23_never_equal(take_next_R_non_bottom_state_from, move_next_R_non_bottom_state_to, move_next_BminR_bottom_state_to);
2232 ++take_next_R_non_bottom_state_from;
2233 }
2234 assert(marking_value==move_next_R_non_bottom_state_to->ref_state->counter);
2235 assert(B==move_next_R_non_bottom_state_to->ref_state->block);
2236 move_next_R_non_bottom_state_to->ref_state->block=B_new;
2237 mCRL2complexity_gj(move_next_R_non_bottom_state_to->ref_state,
2239 *this);
2240 }
2241 for (; move_next_R_non_bottom_state_to<BminR_start_bottom_states; ++move_next_R_non_bottom_state_to)
2242 {
2243 // This loop moves R non-bottom states to places where there were BminR non-bottom states before;
2244 // it is executed if there are more R non-bottom states that BminR bottom states.
2245
2246 // Try to find a R non-bottom state to move to *move_next_R_non_bottom_state_to.
2247 if (marking_value==move_next_R_non_bottom_state_to->ref_state->counter)
2248 {
2249 // There is already a suitable state at this position. Do nothing.
2250 }
2251 else
2252 {
2253 // *move_next_R_non_bottom_state_to now contains a BminR-non-bottom state.
2254 // Find a place where to move it to, namely some R-non-bottom state that needs to be moved.
2255 while (assert(take_next_R_non_bottom_state_from<m_blocks[B].end_states),
2256 marking_value!=take_next_R_non_bottom_state_from->ref_state->counter)
2257 {
2258 #ifdef CHECK_COMPLEXITY_GJ
2259 // assign the work in this loop to some R non-bottom state.
2260 // (This is possible because there are no fewer R non-bottom states than BminR non-bottom states.)
2261 assert(account_for_skipped_BminR_states<R.end());
2262 mCRL2complexity_gj(account_for_skipped_BminR_states->ref_state, add_work(check_complexity::split_block_B_into_R_and_BminR__skip_over_state, max_B), *this);
2263 ++account_for_skipped_BminR_states;
2264 #endif
2265 ++take_next_R_non_bottom_state_from;
2266 }
2267 swap_states_in_states_in_block_never_equal(take_next_R_non_bottom_state_from, move_next_R_non_bottom_state_to);
2268 ++take_next_R_non_bottom_state_from;
2269 assert(marking_value==move_next_R_non_bottom_state_to->ref_state->counter);
2270 }
2271 assert(B==move_next_R_non_bottom_state_to->ref_state->block);
2272 move_next_R_non_bottom_state_to->ref_state->block=B_new;
2273 mCRL2complexity_gj(move_next_R_non_bottom_state_to->ref_state,
2275 *this);
2276 }
2277 }
2278 else
2279 {
2280 // Less than half of the non-bottom states go to R.
2281 // We have to ensure that we assign every move to some R non-bottom state
2282 // (and do not look at too many BminR states).
2283 std::vector<state_in_block_pointer>::const_iterator take_next_R_non_bottom_state_from=R.begin();
2284 for (; move_next_R_non_bottom_state_to<move_next_R_non_bottom_state_to_end;
2285 ++move_next_R_non_bottom_state_to, ++move_next_BminR_bottom_state_to)
2286 {
2287 // Now the BminR-bottom state at *move_next_R_non_bottom_state_to should move to *move_next_BminR_bottom_state_to.
2288 // Find some R-non-bottom state that can move to *move_next_R_non_bottom_state_to:
2289 if (marking_value==move_next_BminR_bottom_state_to->ref_state->counter)
2290 {
2291 // There is a R-non-bottom state at *move_next_BminR_bottom_state_to already:
2292 swap_states_in_states_in_block_never_equal(move_next_R_non_bottom_state_to, move_next_BminR_bottom_state_to);
2293 }
2294 else
2295 {
2296 // *move_next_BminR_bottom_state_to now contains a BminR-non-bottom state.
2297 // Find a place where to move it to, namely some R-non-bottom state that needs to be moved.
2298 while (assert(take_next_R_non_bottom_state_from<R.end()),
2299 take_next_R_non_bottom_state_from->ref_state->ref_states_in_blocks<BminR_start_non_bottom_states)
2300 {
2301 mCRL2complexity_gj(take_next_R_non_bottom_state_from->ref_state, add_work(check_complexity::split_block_B_into_R_and_BminR__skip_over_state, max_B), *this);
2302 assert(marking_value==take_next_R_non_bottom_state_from->ref_state->counter);
2303 assert((take_next_R_non_bottom_state_from->ref_state->ref_states_in_blocks<move_next_R_non_bottom_state_to
2304 ? B_new : B)==take_next_R_non_bottom_state_from->ref_state->block);
2305 ++take_next_R_non_bottom_state_from;
2306 }
2307 swap_states_in_states_in_block_23_never_equal(take_next_R_non_bottom_state_from->ref_state->ref_states_in_blocks, move_next_R_non_bottom_state_to, move_next_BminR_bottom_state_to);
2308 ++take_next_R_non_bottom_state_from;
2309 }
2310 assert(marking_value==move_next_R_non_bottom_state_to->ref_state->counter);
2311 assert(B==move_next_R_non_bottom_state_to->ref_state->block);
2312 move_next_R_non_bottom_state_to->ref_state->block=B_new;
2313 mCRL2complexity_gj(move_next_R_non_bottom_state_to->ref_state,
2315 *this);
2316 }
2317 #ifndef NDEBUG
2318 if (move_next_R_non_bottom_state_to<BminR_start_bottom_states)
2319 {
2320 // There are still some R-non-bottom states that may not be in their correct positions.
2321 assert(move_next_R_non_bottom_state_to==m_blocks[B].start_non_bottom_states);
2322 }
2323 else
2324 {
2325 // All states are in their correct positions.
2326 assert(BminR_start_non_bottom_states==move_next_BminR_bottom_state_to);
2327 }
2328 #endif
2329 for (; move_next_R_non_bottom_state_to<BminR_start_bottom_states; ++move_next_R_non_bottom_state_to)
2330 {
2331 // This loop moves R non-bottom states to places where there were BminR non-bottom states before;
2332 // it is executed if there are more R non-bottom states that BminR bottom states.
2333
2334 // Try to find a R non-bottom state to move to *move_next_R_non_bottom_state_to.
2335 if (marking_value==move_next_R_non_bottom_state_to->ref_state->counter)
2336 {
2337 // There is already a suitable state at this position. Do nothing.
2338 }
2339 else
2340 {
2341 // *move_next_R_non_bottom_state_to now contains a BminR-non-bottom state.
2342 // Find a place where to move it to, namely some R-non-bottom state that needs to be moved.
2343 while (assert(R.begin()<=take_next_R_non_bottom_state_from),
2344 assert(take_next_R_non_bottom_state_from<R.end()),
2345 take_next_R_non_bottom_state_from->ref_state->ref_states_in_blocks<BminR_start_non_bottom_states)
2346 {
2347 // Actually the state at *take_next_R_non_bottom_state_from is already at an acceptable position.
2348 // Leave it there and try the next state.
2349 mCRL2complexity_gj(take_next_R_non_bottom_state_from->ref_state, add_work(check_complexity::split_block_B_into_R_and_BminR__skip_over_state, max_B), *this);
2350 assert(marking_value==take_next_R_non_bottom_state_from->ref_state->counter);
2351 assert((take_next_R_non_bottom_state_from->ref_state->ref_states_in_blocks<move_next_R_non_bottom_state_to
2352 ? B_new : B)==take_next_R_non_bottom_state_from->ref_state->block);
2353 ++take_next_R_non_bottom_state_from;
2354 }
2355 swap_states_in_states_in_block_never_equal(take_next_R_non_bottom_state_from->ref_state->ref_states_in_blocks, move_next_R_non_bottom_state_to);
2356 ++take_next_R_non_bottom_state_from;
2357 assert(marking_value==move_next_R_non_bottom_state_to->ref_state->counter);
2358 }
2359 assert(B==move_next_R_non_bottom_state_to->ref_state->block);
2360 move_next_R_non_bottom_state_to->ref_state->block=B_new;
2361 mCRL2complexity_gj(move_next_R_non_bottom_state_to->ref_state,
2363 *this);
2364 }
2365 }
2366 }
2367 m_blocks[B_new].end_states=BminR_start_bottom_states;
2368 m_blocks[B].start_bottom_states=BminR_start_bottom_states;
2369 m_blocks[B].start_non_bottom_states=BminR_start_non_bottom_states;
2370 assert(static_cast<std::make_signed<state_index>::type>(R.size())==std::distance(m_blocks[B_new].start_non_bottom_states, m_blocks[B_new].end_states));
2371 #else
2372 m_blocks[B_new].end_states=last_bottom_state_in_R;
2373 m_blocks[B].start_bottom_states=last_bottom_state_in_R;
2374
2375 // Move the non-bottom states to their correct positions:
2376 for(state_in_block_pointer s: R)
2377 {
2379 max_B), *this);
2380//std::cerr << "MOVE STATE TO NEW BLOCK: " << s << "\n";
2381 assert(B==s.ref_state->block);
2382 s.ref_state->block=B_new;
2383 typename std::vector<state_in_block_pointer>::iterator pos=s.ref_state->ref_states_in_blocks;
2384 assert(pos>=m_blocks[B].start_non_bottom_states); // the state is a non bottom state.
2385 // pos --> B.start_bottom_states --> B.start_non_bottom_states --> pos.
2386 swap_states_in_states_in_block(pos, m_blocks[B].start_bottom_states, m_blocks[B].start_non_bottom_states);
2387 m_blocks[B].start_non_bottom_states++;
2388 m_blocks[B].start_bottom_states++;
2389 m_blocks[B_new].end_states++;
2390 assert(m_blocks[B].start_bottom_states<=m_blocks[B].start_non_bottom_states);
2391 assert(m_blocks[B_new].start_bottom_states<m_blocks[B_new].end_states);
2392 }
2393 #endif
2394 return B_new;
2395 }
2396
2397 // Move the content if i1 to i2, i2 to i3 and i3 to i1.
2399 {
2400 assert(i3<=i2);
2401 assert(i2<=i1);
2402 if (i1==i3)
2403 {
2404 return;
2405 }
2406 if ((i1==i2)||(i2==i3))
2407 {
2408 std::swap(*i1,*i3);
2409 m_transitions[*i1].ref_outgoing_transitions->ref_BLC_transitions = i1;
2410 m_transitions[*i3].ref_outgoing_transitions->ref_BLC_transitions = i3;
2411 }
2412 else // swap all three elements.
2413 {
2414 transition_index temp = *i1;
2415 *i1=*i2;
2416 *i2=*i3;
2417 *i3=temp;
2418 m_transitions[*i1].ref_outgoing_transitions->ref_BLC_transitions = i1;
2419 m_transitions[*i2].ref_outgoing_transitions->ref_BLC_transitions = i2;
2420 m_transitions[*i3].ref_outgoing_transitions->ref_BLC_transitions = i3;
2421 }
2422 }
2423
2424 // It is assumed that the new block is located precisely before the old_block in m_BLC_transitions.
2425 // This routine can not be used in the initialisation phase. It can only be used during refinement.
2426 // The routine returns true if the last element of old_BLC_block has been removed.
2427 //
2428 // This variant of the swap routine assumes that transition ti is unmarked,
2429 // or at least that it is not relevant if it is marked.
2430 [[nodiscard]]
2432 const transition_index ti,
2435 #ifdef SAVE_BLC_MEMORY
2436 , const constellation_index old_to_constellation
2437 #endif
2438 )
2439 {
2440 assert(new_BLC_block->start_same_BLC <= new_BLC_block->start_marked_BLC);
2441 assert(old_BLC_block->start_same_BLC <= old_BLC_block->start_marked_BLC);
2442 BLC_list_iterator old_position = m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions;
2443 assert(old_BLC_block->start_same_BLC <= old_position);
2444 #ifndef SAVE_BLC_MEMORY
2445 assert(old_position<old_BLC_block->end_same_BLC); // the source block or the target constellation may be wrong, so we cannot use points_into_BLC_set()
2446 assert(new_BLC_block->start_marked_BLC==new_BLC_block->end_same_BLC);
2447 assert(old_BLC_block->start_marked_BLC<=old_BLC_block->end_same_BLC);
2448 #else
2449 // the constellation index of the target block has not yet changed to the new constellation:
2450 assert(old_to_constellation==m_blocks[m_states[m_aut.get_transitions()[ti].to()].block].constellation);
2451 #endif
2452 assert(calculate_end_same_BLC(*new_BLC_block)==old_BLC_block->start_same_BLC);
2453 assert(m_transitions[ti].transitions_per_block_to_constellation == old_BLC_block);
2454 assert(ti == *old_position);
2455
2456 if (old_position>=old_BLC_block->start_marked_BLC)
2457 {
2458 #ifndef NDEBUG
2459 const block_index from_block=m_states[m_aut.get_transitions()[ti].from()].block;
2460 assert(m_blocks[from_block].contains_new_bottom_states || number_of_states_in_block(from_block)<=1);
2461 // It's ok to unmark transitions because they start in blocks with new bottom states,
2462 // or in blocks with only 1 state.
2463 // (However, it may happen that unmarked transitions from other blocks
2464 // are moved, even if there are marked transitions in the same BLC set---
2465 // namely for the co-splitters. So we can only unmark transitions if
2466 // transition ti itself is marked.)
2467 #endif
2468 #ifdef SAVE_BLC_MEMORY
2469 old_BLC_block->start_marked_BLC=std::next(old_position);
2470 #else
2471 old_BLC_block->start_marked_BLC=old_BLC_block->end_same_BLC;
2472 #endif
2473 }
2474 assert(old_BLC_block->start_same_BLC<=old_position);
2475 assert(new_BLC_block->start_marked_BLC==old_BLC_block->start_same_BLC);
2476 if (old_position!=new_BLC_block->start_marked_BLC)
2477 {
2478 std::swap(*old_position,*old_BLC_block->start_same_BLC);
2479 m_transitions[*old_position].ref_outgoing_transitions->ref_BLC_transitions=old_position;
2480 m_transitions[*old_BLC_block->start_same_BLC].ref_outgoing_transitions->ref_BLC_transitions = old_BLC_block->start_same_BLC;
2481 }
2482 else
2483 {
2484 assert(old_position==old_BLC_block->start_same_BLC);
2485 }
2486 #ifndef SAVE_BLC_MEMORY
2487 new_BLC_block->end_same_BLC=
2488 #endif
2489 new_BLC_block->start_marked_BLC=++old_BLC_block->start_same_BLC;
2490 m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
2491// std::cerr << " to new " << new_BLC_block->debug_id(*this) << '\n';
2492 #ifdef SAVE_BLC_MEMORY
2493 if (old_BLC_block->start_same_BLC >= m_BLC_transitions.end())
2494 {
2495 return true;
2496 }
2497 const transition& t=m_aut.get_transitions()[ti];
2498 const transition& old_t = m_aut.get_transitions()[*old_BLC_block->start_same_BLC];
2499 return m_states[old_t.from()].block != m_states[t.from()].block ||
2501 m_blocks[m_states[old_t.to()].block].constellation != old_to_constellation;
2502 #else
2503 return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
2504 #endif
2505 }
2506
2507 // Move the transition t with transition index ti to a new
2508 // LBC list as the target state switches to a new constellation.
2509 // Returns true if a new BLC-entry for non-inert transitions has been created,
2510 // and there are still transitions in the old BLC-entry.
2511 // (Otherwise there is no need to split the block.)
2512 [[nodiscard]]
2514 const block_index index_block_B,
2515 const transition& t,
2516 const transition_index ti)
2517 {
2518 assert(m_states[t.to()].block==index_block_B);
2519 assert(&m_aut.get_transitions()[ti] == &t);
2520 const block_index from_block=m_states[t.from()].block;
2521 assert(m_blocks[from_block].block_to_constellation.check_linked_list());
2522 bool new_block_created = false;
2523 linked_list<BLC_indicators>::iterator this_block_to_constellation=
2524 m_transitions[ti].transitions_per_block_to_constellation;
2525 assert(this_block_to_constellation!=m_blocks[from_block].block_to_constellation.end());
2526 assert(this_block_to_constellation->start_same_BLC <= m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions);
2527 // the transition is never marked:
2528 assert(m_blocks[from_block].contains_new_bottom_states ||
2529 number_of_states_in_block(from_block)<=1 ||
2530 m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions<this_block_to_constellation->start_marked_BLC);
2531 linked_list<BLC_indicators>::iterator next_block_to_constellation;
2532 // if this transition is inert, it is inserted in a block in front. Otherwise, it is inserted after
2533 // the current element in the list.
2534 if (is_inert_during_init(t) && from_block==index_block_B)
2535 {
2536 next_block_to_constellation=m_blocks[from_block].block_to_constellation.begin();
2537 assert(next_block_to_constellation->start_same_BLC<m_BLC_transitions.end());
2538 #ifndef SAVE_BLC_MEMORY
2539 assert(next_block_to_constellation->start_same_BLC<next_block_to_constellation->end_same_BLC);
2540 #endif
2541 assert(m_states[m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].from()].block==index_block_B);
2542 assert(m_aut.is_tau(m_aut.apply_hidden_label_map(m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].label())));
2543 if (next_block_to_constellation==this_block_to_constellation)
2544 {
2545 // Make a new entry in the list block_to_constellation, at the beginning;
2546//std::cerr << "Creating new BLC set for inert " << m_transitions[ti].debug_id(*this) << ": ";
2547
2548 next_block_to_constellation=
2549 m_blocks[from_block].block_to_constellation.
2550 emplace_front(//first_block_to_constellation,
2551 this_block_to_constellation->start_same_BLC,
2552 this_block_to_constellation->start_same_BLC);
2553 #ifdef CHECK_COMPLEXITY_GJ
2554 next_block_to_constellation->work_counter = this_block_to_constellation->work_counter;
2555 #endif
2556 }
2557 else
2558 {
2559//std::cerr << "Extending existing BLC set for inert " << m_transitions[ti].debug_id(*this) << ": ";
2560 assert(m_states[m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].to()].block==index_block_B);
2561 }
2562 }
2563 else
2564 {
2565 // The transition is not constellation-inert.
2566 // The transition will be placed in a BLC set immediately after the BLC set it came from,
2567 // so that main splitters (with transitions to the new constellation)
2568 // come after co-splitters (with transitions to the old constellation).
2569
2570 // This method also ensures that transitions from the old constellation
2571 // to the old constellation will remain at the beginning of their respective BLC set.
2572 next_block_to_constellation=std::next(this_block_to_constellation);
2573 const transition* first_t;
2574 if (next_block_to_constellation==m_blocks[from_block].block_to_constellation.end() ||
2575 (first_t = &m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)],
2576 assert(m_states[first_t->from()].block==from_block),
2577 m_states[first_t->to()].block!=index_block_B) ||
2578 (label_or_divergence(*first_t) != label_or_divergence(t)))
2579 {
2580//std::cerr << "Creating new BLC set for " << m_transitions[ti].debug_id(*this) << ": ";
2581 // Make a new entry in the list next_block_to_constellation, after the current list element.
2582 next_block_to_constellation=
2583 m_blocks[from_block].block_to_constellation.
2584 emplace_after(this_block_to_constellation,
2585 this_block_to_constellation->start_same_BLC,
2586 this_block_to_constellation->start_same_BLC);
2587 #ifdef CHECK_COMPLEXITY_GJ
2588 next_block_to_constellation->work_counter = this_block_to_constellation->work_counter;
2589 #endif
2590 new_block_created = true;
2591 }
2592//else { std::cerr << "Extending existing BLC set for " << m_transitions[ti].debug_id(*this) << ": "; }
2593 }
2594
2596 next_block_to_constellation, this_block_to_constellation
2597 #ifdef SAVE_BLC_MEMORY
2598 , m_blocks[index_block_B].constellation
2599 #endif
2600 ))
2601 {
2602 m_blocks[from_block].block_to_constellation.erase(this_block_to_constellation);
2603 }
2604 #ifndef NDEBUG
2605 check_transitions(false, false);
2606 #endif
2607 return new_block_created;
2608 }
2609
2610 // It is assumed that the new block is located precisely before the old_block in m_BLC_transitions.
2611 // This routine can not be used in the initialisation phase. It can only be used during refinement.
2612 // The routine returns true if the last element of old_BLC_block has been removed.
2613 [[nodiscard]]
2615 const transition_index ti,
2618 #ifdef SAVE_BLC_MEMORY
2619 , const block_index old_from_block,
2620 const constellation_index old_to_constellation
2621 #endif
2622 )
2623 {
2624 assert(new_BLC_block->start_same_BLC <= new_BLC_block->start_marked_BLC);
2625 assert(old_BLC_block->start_same_BLC <= old_BLC_block->start_marked_BLC);
2626 BLC_list_iterator old_position = m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions;
2627 assert(old_BLC_block->start_same_BLC <= old_position);
2628 #ifndef SAVE_BLC_MEMORY
2629 assert(old_position < old_BLC_block->end_same_BLC); // the source block or the target constellation may be wrong, so we cannot use points_into_BLC_set()
2630 assert(new_BLC_block->start_marked_BLC <= new_BLC_block->end_same_BLC);
2631 assert(old_BLC_block->start_marked_BLC <= old_BLC_block->end_same_BLC);
2632 #endif
2633 assert(calculate_end_same_BLC(*new_BLC_block)==old_BLC_block->start_same_BLC);
2634 assert(m_transitions[ti].transitions_per_block_to_constellation == old_BLC_block);
2635 assert(m_blocks.size()-1==m_states[m_aut.get_transitions()[ti].from()].block);
2636 assert(ti == *old_position);
2637 if (old_position < old_BLC_block->start_marked_BLC)
2638 {
2639// std::cerr << "Moving unmarked " << m_transitions[*old_position].debug_id(*this);
2640 assert(old_BLC_block->start_same_BLC <= old_position);
2641 assert(new_BLC_block->start_marked_BLC <= old_BLC_block->start_same_BLC);
2642 swap_three_iterators_and_update_m_transitions(old_position, old_BLC_block->start_same_BLC, new_BLC_block->start_marked_BLC);
2643 new_BLC_block->start_marked_BLC++;
2644 }
2645 else
2646 {
2647// std::cerr << "Moving marked " << m_transitions[*old_position].debug_id(*this);
2648 assert(old_BLC_block->start_marked_BLC <= old_position);
2649 assert(old_BLC_block->start_same_BLC <= old_BLC_block->start_marked_BLC);
2650 swap_three_iterators_and_update_m_transitions(old_position, old_BLC_block->start_marked_BLC, old_BLC_block->start_same_BLC);
2651 old_BLC_block->start_marked_BLC++;
2652 }
2653 m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
2654 #ifndef SAVE_BLC_MEMORY
2655 new_BLC_block->end_same_BLC=
2656 #endif
2657 ++old_BLC_block->start_same_BLC;
2658// std::cerr << " to new " << new_BLC_block->debug_id(*this) << '\n';
2659 #ifdef SAVE_BLC_MEMORY
2660 if (old_BLC_block->start_same_BLC >= m_BLC_transitions.end())
2661 {
2662 return true;
2663 }
2664 const transition& old_t = m_aut.get_transitions()[*old_BLC_block->start_same_BLC];
2665 return (m_states[old_t.from()].block!=old_from_block &&
2666 m_states[old_t.from()].block!=m_blocks.size()-1) ||
2667 label_or_divergence(old_t) != label_or_divergence(m_aut.get_transitions()[ti]) ||
2668 m_blocks[m_states[old_t.to()].block].constellation != old_to_constellation;
2669 #else
2670 return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
2671 #endif
2672 }
2673
2674 // Update the LBC list of a transition, when the from state of the transition moves
2675 // from block old_bi to new_bi.
2677 const block_index old_bi,
2678 const block_index new_bi,
2679 const transition_index ti
2681 , constellation_index old_constellation = null_constellation
2682 // used to maintain the order of BLC sets:
2683 // main splitter BLC sets (target constellation == new constellation) follow immediately
2684 // after co-splitter BLC sets (target constellation == old_constellation) in the BLC sets
2685 #endif
2686 )
2687 {
2688//std::cerr << "update_the_doubly_linked_list_LBC_new_block(old_bi = " << old_bi << ", new_bi = " << new_bi << ", transition_index = " << ti << " = " << m_transitions[ti].debug_id_short(*this) << ")\n";
2689 const transition& t=m_aut.get_transitions()[ti];
2690 assert(m_blocks[old_bi].block_to_constellation.check_linked_list());
2691 assert(m_blocks[new_bi].block_to_constellation.check_linked_list());
2692
2693 assert(m_states[t.from()].block==new_bi);
2694
2695 linked_list<BLC_indicators>::iterator this_block_to_constellation=
2696 m_transitions[ti].transitions_per_block_to_constellation;
2697//std::cerr << "This transition is in " << this_block_to_constellation->debug_id(*this) << '\n';
2698 const label_index a = label_or_divergence(t);
2699 const constellation_index to_constln = m_blocks[m_states[t.to()].block].constellation;
2701 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
2702 if (is_inert_during_init(t) && to_constln==m_blocks[new_bi].constellation)
2703 {
2704 assert(this_block_to_constellation==m_blocks[old_bi].block_to_constellation.begin());
2705 new_BLC_block=m_blocks[new_bi].block_to_constellation.begin();
2706 assert(new_BLC_block!=m_blocks[new_bi].block_to_constellation.end());
2707 #ifndef NDEBUG
2708 if (new_BLC_block->start_same_BLC<new_BLC_block->end_same_BLC)
2709 {
2710 const transition& inert_t=m_aut.get_transitions()[*new_BLC_block->start_same_BLC];
2711 assert(new_bi==m_states[inert_t.from()].block);
2712 assert(a==label_or_divergence(inert_t));
2713 assert(to_constln==m_blocks[m_states[inert_t.to()].block].constellation);
2714 }
2715 #endif
2716 assert(this_block_to_constellation->start_same_BLC==new_BLC_block->end_same_BLC);
2717 }
2718 else
2719 #endif
2720 {
2721 bool co_block_found=false;
2722 if (this_block_to_constellation->start_same_BLC!=m_BLC_transitions.begin())
2723 {
2724 const transition_index co_transition=*(this_block_to_constellation->start_same_BLC-1);
2725 const transition& co_t=m_aut.get_transitions()[co_transition];
2726 if (m_states[co_t.from()].block==new_bi &&
2727 a == label_or_divergence(co_t) &&
2728 to_constln == m_blocks[m_states[co_t.to()].block].constellation)
2729 {
2730 // Move the current transition to the next list indicated by the iterator it.
2731 new_BLC_block=m_transitions[co_transition].transitions_per_block_to_constellation;
2732 co_block_found=true;
2733 }
2734 }
2735 if (!co_block_found)
2736 {
2737 // Make a new entry in the list next_block_to_constellation;
2738
2739 // We first calculate the position where the new BLC set should go to in new_position.
2740 // Default position: at the beginning.
2741 linked_list<BLC_indicators>::iterator new_position=m_blocks[new_bi].block_to_constellation.end();
2742 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
2743 assert(!(is_inert_during_init(t) && to_constln==m_blocks[new_bi].constellation));
2744 #else
2745 if (is_inert_during_init(t) && to_constln==m_blocks[new_bi].constellation)
2746 {
2747 // This BLC slice contains inert transitions and should always be placed at the front.
2748 assert(this_block_to_constellation==m_blocks[old_bi].block_to_constellation.begin());
2749 #ifdef CO_SPLITTER_IN_BLC_LIST
2750 // The inert transitions do not need to preserve their co-splitter position
2751 old_constellation=null_constellation;
2752//std::cerr << "Creating new BLC set for inert transitions\n";
2753 #endif
2754 }
2755 else
2756 #endif
2757 {
2758 // This BLC slice does not contain inert transitions.
2759 #ifdef CO_SPLITTER_IN_BLC_LIST
2760 if (m_blocks[new_bi].block_to_constellation.empty())
2761 {
2762 // This is the first transition that is moved.
2763 #ifdef CO_SPLITTER_INBLC_LIST_VARIANT
2764 assert(!m_branching);
2765 #endif
2766//std::cerr << "This is the first transition that is moved.\n";
2767 }
2768 else
2769 {
2770 assert(false==co_block_found);
2771 if (null_constellation!=old_constellation)
2772 {
2773 // The following comments are all formulated for the case that this_block_to_constellation is a main splitter (except when indicated explicitly).
2774 const constellation_index new_constellation=m_constellations.size()-1;
2775 assert(old_constellation<new_constellation);
2777 if ((old_constellation==to_constln /* i.e. this_block_to_constellation is a co-splitter */ &&
2778 (old_co_splitter = std::next(this_block_to_constellation),
2779//(std::cerr << "Transition is originally in a co-splitter; "),
2780 true)) ||
2781 (new_constellation == to_constln /* i.e. this_block_to_constellation is a main splitter */ &&
2782 (old_co_splitter = std::prev(this_block_to_constellation),
2783//(std::cerr << "Transition is originally in a main splitter; "),
2784 true)))
2785 {
2786 if (m_blocks[old_bi].block_to_constellation.end()!=old_co_splitter)
2787 {
2788//std::cerr << (old_constellation == to_constln ? "Current old main splitter candidate: " : "Current old co-splitter candidate: ") << old_co_splitter->debug_id(*this);
2789 // If the co-splitter belonging to this_block_to_constellation exists,
2790 // then it is old_co_splitter.
2791 // (but if there is no such co-splitter, old_co_splitter could be a different main splitter,
2792 // a different co-splitter without main splitter, or a completely unrelated splitter).
2793
2794 // Try to find out whether there is already a corresponding co-splitter in m_blocks[new_bi].block_to_constellation.
2795 // This co-splitter would be just before old_co_splitter in m_BLC_transitions.
2796 const constellation_index co_to_constln=to_constln^old_constellation^new_constellation;
2797 assert((old_constellation==to_constln && new_constellation==co_to_constln) ||
2798 (new_constellation == to_constln && old_constellation == co_to_constln));
2799 if (m_BLC_transitions.begin()<old_co_splitter->start_same_BLC)
2800 {
2801 // Check the transition in the potential corresponding new co-splitter:
2802 const transition_index temp_transition=*(old_co_splitter->start_same_BLC-1);
2803 const transition& temp_t=m_aut.get_transitions()[temp_transition];
2804 if (new_bi==m_states[temp_t.from()].block &&
2805 a == label_or_divergence(temp_t) &&
2806 co_to_constln == m_blocks[m_states[temp_t.to()].block].constellation)
2807 {
2808 // temp_transition is in the corresponding new co-splitter; place the new BLC set immediately after this co-splitter in the list m_blocks[new_bi].block_to_constellation.
2809 new_position=m_transitions[temp_transition].transitions_per_block_to_constellation;
2810 if (old_constellation==to_constln)
2811 {
2812 // (this_block_to_constellation was a co-splitter:) temp_transition is in the new main splitter; place the new BLC set immediately before this main splitter in the list m_blocks[new_bi].block_to_constellation.
2813 --new_position;
2814//std::cerr << ". This is a real old main splitter.\n";
2815 }
2816//else { std::cerr << ". This is a real old co-splitter.\n"; }
2817 co_block_found=true;
2818 // The new co-splitter was found, and old_co_splitter must have been the old co-splitter.
2819 #ifndef NDEBUG
2820 if (old_co_splitter->start_same_BLC<old_co_splitter->end_same_BLC)
2821 {
2822 const transition& co_t=m_aut.get_transitions()[*old_co_splitter->start_same_BLC];
2823 assert(old_bi==m_states[co_t.from()].block || new_bi==m_states[co_t.from()].block);
2824 assert(a==label_or_divergence(co_t));
2825 assert(co_to_constln==m_blocks[m_states[co_t.to()].block].constellation);
2826 }
2827 #endif
2828 // Now the new main splitter is about to be created.
2829 // In this case it is ok to delete this_block_to_constellation when it becomes empty;
2830 // therefore we set old_constellation in a way that it's going to delete it immediately:
2831 old_constellation=null_constellation;
2832 // We should not use old_constellation for anything else after this point.
2833 }
2834//else { std::cerr << ". The transition just before it in m_BLC_transitions (" << temp_t.from() << " == " << m_transitions[temp_transition].debug_id(*this) << " == " << temp_t.to() << (old_constellation == to_constln ? ") does not belong to the new main splitter.\n" : ") does not belong to the new co-splitter.\n"); }
2835 }
2836//else { std::cerr << (old_constellation == to_constln ? "This candidate is at the beginning of m_BLC_transitions. There is no new main splitter yet.\n" : "This candidate is at the beginning of m_BLC_transitions. There is no new co-splitter yet.\n"); }
2837 }
2838 else
2839 {
2840 // this_block_to_constellation is a main splitter
2841 // but it has no corresponding co-splitter.
2842 // If it becomes empty, one can immediately delete it.
2843 old_constellation=null_constellation;
2844//std::cerr << (old_constellation == to_constln ? "There is no candidate old main splitter.\n" : "There is no candidate old co-splitter.\n");
2845 }
2846 }
2847 else
2848 {
2849 // this_block_to_constellation is neither a main splitter nor a co-splitter.
2850 // If it becomes empty, one can immediately delete it.
2851 old_constellation=null_constellation;
2852 }
2853 }
2854 if (!co_block_found)
2855 {
2856 // place the new BLC set at the beginning unless...
2857 assert(!m_blocks[new_bi].block_to_constellation.empty()); // we already checked that earlier
2858 if (m_branching)
2859 {
2860 const linked_list<BLC_indicators>::iterator perhaps_inert=m_blocks[new_bi].block_to_constellation.begin();
2861 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
2862 // In this case we always inserted a new BLC set for the inert transitions,
2863 // so we can place the BLC set after that one.
2864 new_position=perhaps_inert;
2865 #else
2866 if (perhaps_inert->start_same_BLC<perhaps_inert->end_same_BLC)
2867 {
2868 const transition& p_i_t=m_aut.get_transitions()[*perhaps_inert->start_same_BLC];
2869 assert(new_bi==m_states[p_i_t.from()].block);
2871 m_blocks[new_bi].constellation==m_blocks[m_states[p_i_t.to()].block].constellation)
2872 {
2873 // perhaps_inert does contain constellation-inert transitions, place the new BLC set after that
2874 new_position=perhaps_inert;
2875 }
2876 }
2877 #endif
2878 }
2879 }
2880 }
2881 #else
2882 // Place the new BLC set in the 2nd position
2883 // (This is a safe choice, as there is no requirement on the order of non-inert BLC sets)
2884 new_position=m_blocks[new_bi].block_to_constellation.begin();
2885 #endif
2886 }
2887 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
2888 assert(!m_branching || m_blocks[new_bi].block_to_constellation.end()!=new_position);
2889 #endif
2890 const BLC_list_iterator old_BLC_start=this_block_to_constellation->start_same_BLC;
2891 new_BLC_block=m_blocks[new_bi].block_to_constellation.emplace_after(new_position, old_BLC_start, old_BLC_start);
2892 #ifdef CHECK_COMPLEXITY_GJ
2893 new_BLC_block->work_counter=this_block_to_constellation->work_counter;
2894 #endif
2895 }
2896 }
2897 const bool last_element_removed=swap_in_the_doubly_linked_list_LBC_in_blocks_new_block(ti,
2898 new_BLC_block, this_block_to_constellation
2899 #ifdef SAVE_BLC_MEMORY
2900 , old_bi, to_constln
2901 #endif
2902 );
2903
2904 transition_index remaining_transition=null_transition;
2905 if (last_element_removed)
2906 {
2907 #ifdef CO_SPLITTER_IN_BLC_LIST
2908 if (null_constellation != old_constellation)
2909 {
2910 // Sometimes we could still remove this_block_to_constellation immediately
2911 // (namely if the new main splitter and the new co-splitter already exist,
2912 // or if the old co-splitter does not exist at all).
2913 // A few small such cases are handled above,
2914 // but other cases would require additional, possibly extensive, checks:
2915 // if (co_block_found) {
2916 // copy more or less the code from above that decides
2917 // whether this_block_to_constellation is a main splitter
2918 // that has an old co-splitter but not a new co-splitter or vice versa.
2919 // }
2920 m_BLC_indicators_to_be_deleted.push_back(this_block_to_constellation);
2921 }
2922 else
2923 #endif
2924 {
2925 // Remove this element.
2926 m_blocks[old_bi].block_to_constellation.erase(this_block_to_constellation);
2927 }
2928 }
2929 else
2930 {
2931 remaining_transition= *(this_block_to_constellation->start_same_BLC);
2932 }
2933 #ifndef NDEBUG
2934 check_transitions(false, false);
2935 assert(m_blocks[old_bi].block_to_constellation.check_linked_list());
2936 assert(m_blocks[new_bi].block_to_constellation.check_linked_list());
2937 #endif
2938
2939 return remaining_transition;
2940 }
2941
2942 // Set m_states[s].counter:=undefined for all s in m_R and m_U.
2943 void clear_state_counters(bool restrict_to_R=false)
2944 {
2945 for(const state_in_block_pointer si: m_R)
2946 {
2947 assert(Rmarked == si.ref_state->counter); // this allows us to charge the work in this loop to setting the counter to Rmarked
2948 si.ref_state->counter=undefined;
2949 }
2950 if (restrict_to_R)
2951 {
2952 assert(m_U_counter_reset_vector.empty());
2953 return;
2954 }
2956 {
2957 // this work is charged to adding a value to m_U_counter_reset_vector
2958 assert(undefined!=si.ref_state->counter || m_R.find(si));
2959 assert(Rmarked!=si.ref_state->counter);
2960 si.ref_state->counter=undefined;
2961 }
2963 }
2964
2965 // Calculate the states R in block B that can inertly reach a state with a transition in splitter
2966 // and split B in R and B\R. The complexity is conform the smaller block, either R or B\R.
2967 // The LBC_list and bottom states are not updated.
2968 // Provide the index of subblock R as a result.
2969
2970 // The function assumes that R has already been pre-filled with the
2971 // sources of the marked transitions in the splitter, and therefore a
2972 // split is always needed. Bottom states in R are those in the range
2973 // [m_blocks[B].start_bottom_states, first_unmarked_bottom_state),
2974 // non-bottom states in R are already in m_R. (Unmarked transitions
2975 // in the splitter may need to be checked still, but they can only add
2976 // non-bottom states to R.)
2977
2978 // Occasionally it is necessary to split using only a subset of a splitter.
2979 // Then, splitter_end_unmarked_BLC can be used to indicate that this is the case.
2980 // The function assumes that the *marked* transitions in the splitter have
2981 // already been used to separate the bottom states in block B. This is indicated
2982 // using first_unmarked_bottom_state, an iterator into m_states_in_blocks.
2983
2984 // Return value: the index of subblock R
2987 const std::vector<state_in_block_pointer>::iterator first_unmarked_bottom_state,
2988 // const bool initialisation,
2989 const BLC_list_iterator splitter_end_unmarked_BLC)
2990 {
2991// std::cerr << "simple_splitB(block " << B << ",...)\n";
2992 typedef enum { initializing, state_checking, aborted, aborted_after_initialisation,
2993 incoming_inert_transition_checking, outgoing_action_constellation_check } status_type;
2994 status_type U_status=state_checking;
2995 status_type R_status=initializing;
2996 BLC_list_iterator M_it = splitter->start_same_BLC;
2997 std::vector<transition>::iterator current_U_incoming_transition_iterator;
2998 std::vector<transition>::iterator current_U_incoming_transition_iterator_end;
2999 state_in_block_pointer current_U_outgoing_state;
3000 outgoing_transitions_it current_U_outgoing_transition_iterator;
3001 outgoing_transitions_it current_U_outgoing_transition_iterator_end;
3002 std::vector<transition>::iterator current_R_incoming_transition_iterator;
3003 std::vector<transition>::iterator current_R_incoming_transition_iterator_end;
3004 std::vector<state_in_block_pointer>::iterator current_R_incoming_bottom_state_iterator = m_blocks[B].start_bottom_states;
3005 std::vector<state_in_block_pointer>::iterator current_U_incoming_bottom_state_iterator = first_unmarked_bottom_state;
3006
3007 assert(1 < number_of_states_in_block(B));
3008 assert(!m_blocks[B].contains_new_bottom_states);
3009 assert(m_U.empty());
3010 assert(m_U_counter_reset_vector.empty());
3011 // assert(splitter_end_unmarked_BLC == old value of splitter->start_marked_BLC || splitter_end_unmarked_BLC == splitter->start_same_BLC);
3012 assert(m_BLC_transitions.begin() <= splitter->start_same_BLC);
3013 assert(M_it <= splitter_end_unmarked_BLC);
3014 assert(splitter_end_unmarked_BLC <= splitter->start_marked_BLC);
3015 #ifndef SAVE_BLC_MEMORY
3016 assert(splitter->start_marked_BLC <= splitter->end_same_BLC);
3017 assert(splitter->start_same_BLC < splitter->end_same_BLC);
3018 assert(splitter->end_same_BLC <= m_BLC_transitions.end());
3019 #endif
3020 assert(!has_marked_transitions(*splitter));
3021 assert(m_states[m_aut.get_transitions()[*splitter->start_same_BLC].from()].block == B);
3022 assert(current_R_incoming_bottom_state_iterator <= first_unmarked_bottom_state);
3023 assert(current_R_incoming_bottom_state_iterator < first_unmarked_bottom_state || !m_R.empty() || M_it < splitter_end_unmarked_BLC);
3024 assert(current_U_incoming_bottom_state_iterator < m_blocks[B].start_non_bottom_states);
3025
3026 const std::make_signed<state_index>::type max_R_nonbottom_size=number_of_states_in_block(B)/2-std::distance(m_blocks[B].start_bottom_states, first_unmarked_bottom_state); // can underflow
3027 if (max_R_nonbottom_size < static_cast<std::make_signed<state_index>::type>(m_R.size()))
3028 {
3029 assert(number_of_states_in_block(B)/2<std::distance(m_blocks[B].start_bottom_states, first_unmarked_bottom_state)+m_R.size());
3030 R_status = (M_it == splitter_end_unmarked_BLC) ? aborted_after_initialisation : aborted;
3031 }
3032 else
3033 {
3034 assert(number_of_states_in_block(B)/2>=std::distance(m_blocks[B].start_bottom_states, first_unmarked_bottom_state)+m_R.size());
3035 if (m_blocks[B].start_non_bottom_states==m_blocks[B].end_states)
3036 {
3037 // There are no non-bottom states, hence we do not need to carry out the tau closure.
3038 // Also, there cannot be any new bottom states.
3039 assert(m_blocks[B].start_bottom_states<first_unmarked_bottom_state);
3040 assert(std::distance(m_blocks[B].start_bottom_states, first_unmarked_bottom_state)<=std::distance(first_unmarked_bottom_state, m_blocks[B].start_non_bottom_states));
3041 assert(m_R.empty()); // m_R.clear(); is superfluous
3042 assert(m_U.empty()); // m_U.clear(); is superfluous;
3043 assert(m_U_counter_reset_vector.empty()); // clear_state_counters(); is superfluous
3044 // split_block B into R and B\R.
3045 return split_block_B_into_R_and_BminR(B, m_blocks[B].start_bottom_states, first_unmarked_bottom_state, m_R
3046 #ifdef TRY_EFFICIENT_SWAP
3047 , Rmarked
3048 #endif
3049 );
3050 }
3051 else if (M_it==splitter_end_unmarked_BLC)
3052 {
3053 // There are no more transitions in the splitter whose source states need to be added to R.
3054 //assert(m_blocks[B].start_bottom_states < first_unmarked_bottom_state || !m_R.empty());
3055 R_status=state_checking;
3056 }
3057 }
3058 const std::make_signed<state_index>::type max_U_nonbottom_size=number_of_states_in_block(B)/2-std::distance(first_unmarked_bottom_state, m_blocks[B].start_non_bottom_states); // can underflow
3059 if (max_U_nonbottom_size<0)
3060 {
3061 assert(static_cast<std::make_signed<state_index>::type>(number_of_states_in_block(B)/2)<std::distance(first_unmarked_bottom_state, m_blocks[B].start_non_bottom_states));
3062 assert(aborted != R_status); assert(aborted_after_initialisation != R_status);
3063 U_status=aborted_after_initialisation;
3064 }
3065 else
3066 {
3067 assert(static_cast<std::make_signed<state_index>::type>(number_of_states_in_block(B)/2)>=std::distance(first_unmarked_bottom_state, m_blocks[B].start_non_bottom_states));
3068 if (m_blocks[B].start_non_bottom_states==m_blocks[B].end_states)
3069 {
3070 // There are no non-bottom states, hence we do not need to carry out the tau closure.
3071 // Also, there cannot be any new bottom states.
3072 assert(first_unmarked_bottom_state<m_blocks[B].start_non_bottom_states);
3073 assert(std::distance(first_unmarked_bottom_state, m_blocks[B].start_non_bottom_states)<=std::distance(m_blocks[B].start_bottom_states, first_unmarked_bottom_state));
3074 assert(m_R.empty()); // m_R.clear(); is superfluous
3075 assert(m_U.empty()); // m_U.clear(); is superfluous;
3076 assert(m_U_counter_reset_vector.empty()); // clear_state_counters(); is superfluous
3077 // split_block B into U and B\U.
3078 split_block_B_into_R_and_BminR(B, first_unmarked_bottom_state, m_blocks[B].end_states, m_U
3079 #ifdef TRY_EFFICIENT_SWAP
3080 , 0
3081 #endif
3082 );
3083 return B;
3084 }
3085 }
3086 assert(m_blocks[B].start_non_bottom_states < m_blocks[B].end_states);
3087 #ifndef SAVE_BLC_MEMORY
3088 assert(splitter->start_same_BLC < splitter->end_same_BLC);
3089 #endif
3090 const transition& first_t = m_aut.get_transitions()[*splitter->start_same_BLC];
3091 const label_index a = label_or_divergence(first_t);
3092 const constellation_index C = m_blocks[m_states[first_t.to()].block].constellation;
3093 #ifndef NDEBUG
3094 if (initializing == R_status || aborted == R_status)
3095 {
3096 // For constellation-inert splitters (which only happens for the special split to separate new from old bottom states), one has to mark all transitions in the splitter.
3097 assert(!m_aut.is_tau(a) || m_blocks[B].constellation != C);
3098 }
3099 #endif
3100
3101 // Algorithm 3, line 3.2 left.
3102
3103 // start coroutines. Each co-routine handles one state, and then gives control
3104 // to the other co-routine. The coroutines can be found sequentially below surrounded
3105 // by a while loop.
3106
3107//std::cerr << "simple_splitB() before while\n";
3108 while (true)
3109 {
3110 assert(U_status!=aborted_after_initialisation || (R_status!=aborted && R_status!=aborted_after_initialisation));
3111#ifndef NDEBUG
3112 for(state_in_block_pointer si=state_in_block_pointer(m_states.begin()); si.ref_state<m_states.end(); ++si.ref_state)
3113 {
3114 if (si.ref_state->block!=B || 0==si.ref_state->no_of_outgoing_inert_transitions)
3115 {
3116 assert(undefined==si.ref_state->counter);
3117 assert(!m_R.find(si));
3118 assert(!m_U.find(si));
3119 assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) == m_U_counter_reset_vector.end());
3120 }
3121 else
3122 {
3123 switch(si.ref_state->counter)
3124 {
3125 case undefined: assert(!m_U.find(si)); assert(!m_R.find(si));
3126 assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) == m_U_counter_reset_vector.end());
3127 break;
3128 case Rmarked: assert( m_R.find(si)); assert(!m_U.find(si));
3129 // It can happen that the state has a tau-transition to a U-state, then it will be in the m_U_counter_reset_vector.
3130 break;
3131 case 0: assert(!m_R.find(si)); // It can happen that the state is in U or is not in U
3132 #ifdef TRY_EFFICIENT_SWAP
3133 assert(m_U.find(si) ||
3134 (si==current_U_outgoing_state && outgoing_action_constellation_check==U_status));
3135 #endif
3136 assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) != m_U_counter_reset_vector.end());
3137 break;
3138 default: assert(!m_R.find(si)); assert(!m_U.find(si));
3139 assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) != m_U_counter_reset_vector.end());
3140 break;
3141 }
3142 }
3143 }
3144#endif
3145 // The code for the right co-routine.
3146 #ifdef COUNT_R_U_STATUS_TIMES
3147 m_R_status_counter[R_status]++;
3148 #endif
3149 if (incoming_inert_transition_checking==R_status) // 18178 times (large 1394-fin.lts example: 372431 times)
3150 {
3151 assert(current_R_incoming_transition_iterator<current_R_incoming_transition_iterator_end);
3152 mCRL2complexity_gj(&m_transitions[std::distance(m_aut.get_transitions().begin(), current_R_incoming_transition_iterator)],
3154 assert(m_aut.is_tau(m_aut.apply_hidden_label_map(current_R_incoming_transition_iterator->label())));
3155 assert(m_states[current_R_incoming_transition_iterator->to()].block==B);
3156
3157 const transition& tr=*current_R_incoming_transition_iterator;
3158 if (m_states[tr.from()].block==B && !(m_preserve_divergence && tr.from() == tr.to()))
3159 {
3160 if (m_states[tr.from()].counter!=Rmarked)
3161 {
3162 assert(!m_R.find(m_states.begin() + tr.from()));
3163//std::cerr << "R_todo2 insert: " << tr.from() << "\n";
3164 m_R.add_todo(m_states.begin() + tr.from());
3165 m_states[tr.from()].counter=Rmarked;
3166
3167 // Algorithm 3, line 3.10 and line 3.11, right.
3168 if (m_R.size()>static_cast<state_index>(max_R_nonbottom_size))
3169 {
3170 assert(aborted_after_initialisation!=U_status);
3171 R_status=aborted_after_initialisation;
3172 goto R_handled_and_is_not_state_checking;
3173 }
3174 }
3175 else assert(m_R.find(m_states.begin() + tr.from()));
3176 assert(!m_U.find(m_states.begin() + tr.from()));
3177 }
3178 ++current_R_incoming_transition_iterator;
3179 if (current_R_incoming_transition_iterator!=current_R_incoming_transition_iterator_end &&
3180 m_aut.is_tau(m_aut.apply_hidden_label_map(current_R_incoming_transition_iterator->label())))
3181 {
3182 goto R_handled_and_is_not_state_checking;
3183 }
3184 R_status=state_checking;
3185 }
3186 else if (state_checking==R_status) // 18014 times (large 1394-fin.lts example: 331708 times)
3187 {
3188 const state_in_block_pointer s=(current_R_incoming_bottom_state_iterator<first_unmarked_bottom_state
3189 ? *current_R_incoming_bottom_state_iterator++
3190 : m_R.move_from_todo());
3192//std::cerr << "R insert: " << s << "\n";
3193 assert(s.ref_state->block==B);
3194 if (std::next(s.ref_state)==m_states.end())
3195 {
3196 current_R_incoming_transition_iterator_end=m_aut.get_transitions().end();
3197 }
3198 else
3199 {
3200 current_R_incoming_transition_iterator_end=std::next(s.ref_state)->start_incoming_transitions;
3201 }
3202 current_R_incoming_transition_iterator=s.ref_state->start_incoming_transitions;
3203 if (current_R_incoming_transition_iterator!=current_R_incoming_transition_iterator_end &&
3204 m_aut.is_tau(m_aut.apply_hidden_label_map(current_R_incoming_transition_iterator->label())))
3205 {
3206 R_status=incoming_inert_transition_checking;
3207 goto R_handled_and_is_not_state_checking;
3208 }
3209 }
3210 else if (initializing!=R_status)
3211 {
3212 assert(aborted_after_initialisation==R_status || // 10280 times (large 1394-fin.lts example: 550 times)
3213 aborted==R_status); // 663 times (large 1394-fin.lts example: 584 times)
3214 goto R_handled_and_is_not_state_checking;
3215 }
3216 else // initializing==R_status: 2742 times (large 1394-fin.lts example: 1200 times)
3217 {
3218 // Algorithm 3, line 3.3, right.
3219 assert(M_it<splitter_end_unmarked_BLC);
3220 const state_in_block_pointer si(m_states.begin() + m_aut.get_transitions()[*M_it].from());
3222 assert(si.ref_state->block==B);
3223 assert(!is_inert_during_init(m_aut.get_transitions()[*M_it]) || m_blocks[B].constellation!=m_blocks[m_states[m_aut.get_transitions()[*M_it].to()].block].constellation);
3224 ++M_it;
3225 if (0==si.ref_state->no_of_outgoing_inert_transitions)
3226 {
3227 // The state is a bottom state, it should be in R already
3228 assert(m_blocks[B].start_bottom_states<=si.ref_state->ref_states_in_blocks);
3229 assert(si.ref_state->ref_states_in_blocks<first_unmarked_bottom_state);
3230 assert(!m_R.find(si));
3231 }
3232 else if (si.ref_state->counter!=Rmarked)
3233 {
3234 // The state is a nonbottom state that is not yet in R
3235 assert(m_blocks[B].start_non_bottom_states<=si.ref_state->ref_states_in_blocks);
3236 assert(si.ref_state->ref_states_in_blocks<m_blocks[B].end_states);
3237 assert(!m_R.find(si));
3238 m_R.add_todo(si);
3239 si.ref_state->counter=Rmarked;
3240//std::cerr << "R_todo1 insert: " << si << "\n";
3241 if (m_R.size()>static_cast<state_index>(max_R_nonbottom_size))
3242 {
3243 assert(aborted_after_initialisation!=U_status);
3244 R_status=aborted;
3245 goto R_handled_and_is_not_state_checking;
3246 }
3247 }
3248 else assert(m_R.find(si));
3249 assert(!m_U.find(si));
3250 if (M_it!=splitter_end_unmarked_BLC)
3251 {
3252 goto R_handled_and_is_not_state_checking;
3253 }
3254 assert(m_blocks[B].start_non_bottom_states<m_blocks[B].end_states);
3255 R_status=state_checking;
3256 }
3257 assert(state_checking==R_status);
3258 if (current_R_incoming_bottom_state_iterator==first_unmarked_bottom_state && m_R.todo_is_empty())
3259 {
3260//std::cerr << "R empty: " << "\n";
3261 // split_block B into R and B\R.
3262 assert(0 < std::distance(m_blocks[B].start_bottom_states, first_unmarked_bottom_state) + m_R.size());
3263 assert(std::distance(m_blocks[B].start_bottom_states, first_unmarked_bottom_state) + m_R.size() <= number_of_states_in_block(B)/2);
3264 const block_index block_index_of_R = split_block_B_into_R_and_BminR(B, m_blocks[B].start_bottom_states, first_unmarked_bottom_state, m_R
3265 #ifdef TRY_EFFICIENT_SWAP
3266 , Rmarked
3267 #endif
3268 );
3270 m_R.clear();
3271 m_U.clear();
3272 return block_index_of_R;
3273 }
3274 R_handled_and_is_not_state_checking:
3275 assert(state_checking!=R_status || current_R_incoming_bottom_state_iterator!=first_unmarked_bottom_state || !m_R.todo_is_empty());
3276
3277#ifndef NDEBUG
3278 for(state_in_block_pointer si=state_in_block_pointer(m_states.begin()); si.ref_state<m_states.end(); ++si.ref_state)
3279 {
3280 if (si.ref_state->block!=B || 0==si.ref_state->no_of_outgoing_inert_transitions)
3281 {
3282 assert(undefined==si.ref_state->counter);
3283 assert(!m_R.find(si));
3284 assert(!m_U.find(si));
3285 assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) == m_U_counter_reset_vector.end());
3286 }
3287 else
3288 {
3289 switch(si.ref_state->counter)
3290 {
3291 case undefined: assert(!m_U.find(si)); assert(!m_R.find(si));
3292 assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) == m_U_counter_reset_vector.end());
3293 break;
3294 case Rmarked: assert( m_R.find(si)); assert(!m_U.find(si));
3295 // It can happen that the state has a tau-transition to a U-state, then it will be in the m_U_counter_reset_vector.
3296 break;
3297 case 0: assert(!m_R.find(si)); // It can happen that the state is in U or is not in U
3298 #ifdef TRY_EFFICIENT_SWAP
3299 assert(m_U.find(si) ||
3300 (si==current_U_outgoing_state && outgoing_action_constellation_check==U_status));
3301 #endif
3302 assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) != m_U_counter_reset_vector.end());
3303 break;
3304 default: assert(!m_R.find(si)); assert(!m_U.find(si));
3305 assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), si) != m_U_counter_reset_vector.end());
3306 break;
3307 }
3308 }
3309 }
3310#endif
3311 // The code for the left co-routine.
3312 #ifdef COUNT_R_U_STATUS_TIMES
3313 m_U_status_counter[U_status]++;
3314 #endif
3315 if (incoming_inert_transition_checking==U_status) // 20299 times (large 1394-fin.lts example: 360327 times)
3316 {
3317//std::cerr << "U_incoming_inert_transition_checking\n";
3318 // Algorithm 3, line 3.8, left.
3319 assert(current_U_incoming_transition_iterator<current_U_incoming_transition_iterator_end);
3320 assert(m_aut.is_tau(m_aut.apply_hidden_label_map(current_U_incoming_transition_iterator->label())));
3321 // Check one incoming transition.
3322 // Algorithm 3, line 3.12, left.
3323 mCRL2complexity_gj(&m_transitions[std::distance(m_aut.get_transitions().begin(), current_U_incoming_transition_iterator)], add_work(check_complexity::simple_splitB_U__handle_transition_to_U_state, 1), *this);
3324 current_U_outgoing_state=state_in_block_pointer(m_states.begin()+current_U_incoming_transition_iterator->from());
3325 assert(m_states[current_U_incoming_transition_iterator->to()].block==B);
3326 current_U_incoming_transition_iterator++;
3327//std::cerr << "FROM " << std::distance(m_states.begin(), current_U_outgoing_state.ref_state) << "\n";
3328 if (current_U_outgoing_state.ref_state->block==B && !(m_preserve_divergence && std::prev(current_U_incoming_transition_iterator)->from()==std::prev(current_U_incoming_transition_iterator)->to()))
3329 {
3330 assert(!m_U.find(current_U_outgoing_state));
3331 if (current_U_outgoing_state.ref_state->counter!=Rmarked)
3332 {
3333 if (current_U_outgoing_state.ref_state->counter==undefined) // count(current_U_outgoing_state) is undefined;
3334 {
3335 // Algorithm 3, line 3.13, left.
3336 // Algorithm 3, line 3.15 and 3.18, left.
3337 current_U_outgoing_state.ref_state->counter=current_U_outgoing_state.ref_state->no_of_outgoing_inert_transitions-1;
3338 m_U_counter_reset_vector.push_back(current_U_outgoing_state);
3339 }
3340 else
3341 {
3342 // Algorithm 3, line 3.18, left.
3343 assert(std::find(m_U_counter_reset_vector.begin(), m_U_counter_reset_vector.end(), current_U_outgoing_state) != m_U_counter_reset_vector.end());
3344 assert(current_U_outgoing_state.ref_state->counter>0);
3345 current_U_outgoing_state.ref_state->counter--;
3346 }
3347//std::cerr << "COUNTER " << current_U_outgoing_state.ref_state->counter << "\n";
3348 // Algorithm 3, line 3.19, left.
3349 if (current_U_outgoing_state.ref_state->counter==0)
3350 {
3351 if (initializing==R_status || aborted==R_status)
3352 {
3353 // Start searching for an outgoing transition with action a to constellation C.
3354 current_U_outgoing_transition_iterator=current_U_outgoing_state.ref_state->start_outgoing_transitions;
3355 assert(m_outgoing_transitions.begin()<=current_U_outgoing_transition_iterator);
3356 assert(current_U_outgoing_transition_iterator<m_outgoing_transitions.end());
3357 current_U_outgoing_transition_iterator_end=(std::next(current_U_outgoing_state.ref_state)>=m_states.end() ? m_outgoing_transitions.end() : std::next(current_U_outgoing_state.ref_state)->start_outgoing_transitions);
3358 assert(current_U_outgoing_transition_iterator<current_U_outgoing_transition_iterator_end);
3359 assert(m_states.begin()+m_aut.get_transitions()[*current_U_outgoing_transition_iterator->ref_BLC_transitions].from()==current_U_outgoing_state.ref_state);
3360 U_status=outgoing_action_constellation_check;
3361 goto U_handled_and_is_not_state_checking;
3362 }
3363 // The state can be added to U_todo immediately.
3364 #ifndef NDEBUG
3365 // check that the state has no transition in the splitter
3366 for (outgoing_transitions_it out_it=current_U_outgoing_state.ref_state->start_outgoing_transitions;
3367 out_it<m_outgoing_transitions.end() && (std::next(current_U_outgoing_state.ref_state)>=m_states.end() || out_it<std::next(current_U_outgoing_state.ref_state)->start_outgoing_transitions); ++out_it)
3368 {
3369 assert(m_outgoing_transitions.begin()<=out_it);
3370 assert(out_it<m_outgoing_transitions.end());
3371 assert(m_BLC_transitions.begin()<=out_it->ref_BLC_transitions);
3372 assert(out_it->ref_BLC_transitions<m_BLC_transitions.end());
3373 assert(0<=*out_it->ref_BLC_transitions);
3374 assert(*out_it->ref_BLC_transitions<m_aut.num_transitions());
3375 assert(m_transitions[*out_it->ref_BLC_transitions].ref_outgoing_transitions==out_it);
3376 const transition& t=m_aut.get_transitions()[/*initialisation?current_U_outgoing_transition_iterator->transition:*/ *out_it->ref_BLC_transitions];
3377 assert(m_states.begin()+t.from()==current_U_outgoing_state.ref_state);
3378 if (a==label_or_divergence(t) && C==m_blocks[m_states[t.to()].block].constellation)
3379 {
3380 // The transition is in the splitter, so it must be in the part of the splitter that is disregarded.
3381// std::cerr << "State " << std::distance(m_states.begin(), current_U_outgoing_state.ref_state) << " has a transition in the splitter, namely " << m_transitions[*out_it->ref_BLC_transitions].debug_id_short(*this) << '\n';
3382 assert(out_it->ref_BLC_transitions>=splitter_end_unmarked_BLC);
3383 assert(splitter->start_same_BLC<=out_it->ref_BLC_transitions);
3384 assert(points_into_BLC_set(out_it->ref_BLC_transitions, *splitter));
3385 }
3386 }
3387 #endif
3388 m_U.add_todo(current_U_outgoing_state);
3389 // Algorithm 3, line 3.10 and line 3.11 left.
3390 if (m_U.size()>static_cast<state_index>(max_U_nonbottom_size))
3391 {
3392 assert(aborted!=R_status); assert(aborted_after_initialisation!=R_status);
3393 U_status=aborted_after_initialisation;
3394 goto U_handled_and_is_not_state_checking;
3395 }
3396 }
3397 }
3398 else assert(m_R.find(current_U_outgoing_state));
3399 }
3400 if (current_U_incoming_transition_iterator!=current_U_incoming_transition_iterator_end &&
3401 m_aut.is_tau(m_aut.apply_hidden_label_map(current_U_incoming_transition_iterator->label())))
3402 {
3403 assert(incoming_inert_transition_checking==U_status);
3404 goto U_handled_and_is_not_state_checking;
3405 }
3406 U_status=state_checking;
3407 }
3408 else if (state_checking==U_status) // 18920 times (large 1394-fin.lts example: 340893 times)
3409 {
3410//std::cerr << "U_state_checking\n";
3411
3412 // Algorithm 3, line 3.23 and line 3.24, left.
3413 const state_in_block_pointer s=(current_U_incoming_bottom_state_iterator<m_blocks[B].start_non_bottom_states
3414 ? *current_U_incoming_bottom_state_iterator++
3415 : m_U.move_from_todo());
3416 assert(!m_R.find(s));
3418//std::cerr << "U insert/ U_todo_remove: " << s << "\n";
3419 current_U_incoming_transition_iterator=s.ref_state->start_incoming_transitions;
3420 current_U_incoming_transition_iterator_end=(std::next(s.ref_state)>=m_states.end() ? m_aut.get_transitions().end() : std::next(s.ref_state)->start_incoming_transitions);
3421 if (current_U_incoming_transition_iterator!=current_U_incoming_transition_iterator_end &&
3422 m_aut.is_tau(m_aut.apply_hidden_label_map(current_U_incoming_transition_iterator->label())))
3423 {
3424 U_status=incoming_inert_transition_checking;
3425 goto U_handled_and_is_not_state_checking;
3426 }
3427 }
3428 else if (aborted_after_initialisation==U_status) // 6284 times (large 1394-fin.lts example: 2500 times)
3429 {
3430 goto U_handled_and_is_not_state_checking;
3431 }
3432 else
3433 {
3434 assert(outgoing_action_constellation_check==U_status); // 911 times (large 1394-fin.lts example: 912 times)
3435//std::cerr << "U_outgoing_action_constellation_check\n";
3436 assert(current_U_outgoing_transition_iterator!=current_U_outgoing_transition_iterator_end);
3437 // will only be used if the transitions are not constellation-inert:
3438 assert(!m_aut.is_tau(a) || m_blocks[B].constellation!=C);
3439 // assert(splitter_end_unmarked_BLC == old value of splitter->start_marked_BLC); -- can no longer be checked
3440 #ifdef CHECK_COMPLEXITY_GJ
3441 mCRL2complexity_gj((&m_transitions[/*initialisation?current_U_outgoing_transition_iterator->transition:*/ *current_U_outgoing_transition_iterator->ref_BLC_transitions]), add_work(check_complexity::simple_splitB_U__handle_transition_from_potential_U_state, 1), *this);
3442 // This is one step in the coroutine, so we should assign the work to exactly one transition.
3443 // But to make sure, we also mark the other transitions that we skipped in the optimisation.
3444 for (outgoing_transitions_it out_it=current_U_outgoing_transition_iterator; out_it<current_U_outgoing_transition_iterator->start_same_saC; )
3445 {
3446 ++out_it;
3447 mCRL2complexity_gj(&m_transitions[/*initialisation?out_it->transition:*/ *out_it->ref_BLC_transitions], add_work_notemporary(check_complexity::simple_splitB_U__handle_transition_from_potential_U_state, 1), *this);
3448 }
3449 #endif
3450 const transition& t_local=m_aut.get_transitions()
3451 [/*initialisation
3452 ?current_U_outgoing_transition_iterator->transition
3453 :*/ *current_U_outgoing_transition_iterator->ref_BLC_transitions];
3454 current_U_outgoing_transition_iterator=current_U_outgoing_transition_iterator->start_same_saC; // This is an optimisation.
3455 ++current_U_outgoing_transition_iterator;
3456
3457 assert(m_states.begin()+t_local.from()==current_U_outgoing_state.ref_state);
3458 assert(m_branching);
3459 if (m_blocks[m_states[t_local.to()].block].constellation==C &&
3460 label_or_divergence(t_local) == a)
3461 {
3462 // This state must be blocked.
3463 #ifdef TRY_EFFICIENT_SWAP
3464 if(Rmarked!=current_U_outgoing_state.ref_state->counter)
3465 {
3466 current_U_outgoing_state.ref_state->counter=std::numeric_limits<std::make_signed<transition_index>::type>::max();
3467 assert(0!=current_U_outgoing_state.ref_state->counter);
3468 assert(undefined!=current_U_outgoing_state.ref_state->counter);
3469 assert(Rmarked!=current_U_outgoing_state.ref_state->counter);
3470 }
3471 #endif
3472 }
3473 else if (current_U_outgoing_transition_iterator==current_U_outgoing_transition_iterator_end)
3474 {
3475 assert(!m_U.find(current_U_outgoing_state));
3476//std::cerr << "U_todo4 insert: " << std::distance(m_states.begin(), current_U_outgoing_state.ref_state) << " " << m_U.size() << " " << number_of_states_in_block(B) << "\n";
3477 m_U.add_todo(current_U_outgoing_state);
3478 // Algorithm 3, line 3.10 and line 3.11 left.
3479 if (m_U.size()>static_cast<state_index>(max_U_nonbottom_size))
3480 {
3481 assert(aborted!=R_status); assert(aborted_after_initialisation!=R_status);
3482 U_status=aborted_after_initialisation;
3483 goto U_handled_and_is_not_state_checking;
3484 }
3485 }
3486 else
3487 {
3488 goto U_handled_and_is_not_state_checking;
3489 }
3490
3491 if (current_U_incoming_transition_iterator!=current_U_incoming_transition_iterator_end &&
3492 m_aut.is_tau(m_aut.apply_hidden_label_map(current_U_incoming_transition_iterator->label())))
3493 {
3494 U_status = incoming_inert_transition_checking;
3495 goto U_handled_and_is_not_state_checking;
3496 }
3497 U_status=state_checking;
3498 }
3499 assert(state_checking==U_status);
3500 if (current_U_incoming_bottom_state_iterator==m_blocks[B].start_non_bottom_states && m_U.todo_is_empty())
3501 {
3502 // split_block B into U and B\U.
3503//std::cerr << "U_todo empty:\n";
3504 assert(0 < std::distance(first_unmarked_bottom_state, m_blocks[B].start_non_bottom_states) + m_U.size());
3505 assert(std::distance(first_unmarked_bottom_state, m_blocks[B].start_non_bottom_states) + m_U.size() <= number_of_states_in_block(B)/2);
3506 split_block_B_into_R_and_BminR(B, first_unmarked_bottom_state, m_blocks[B].start_non_bottom_states, m_U
3507 #ifdef TRY_EFFICIENT_SWAP
3508 , 0
3509 #endif
3510 );
3512 m_R.clear();
3513 m_U.clear();
3514 return B;
3515 }
3516 U_handled_and_is_not_state_checking:
3517 assert(state_checking!=U_status || current_U_incoming_bottom_state_iterator!=m_blocks[B].start_non_bottom_states || !m_U.todo_is_empty());
3518 }
3519 assert(0);
3520 }
3521
3522 // Make this transition non-inert.
3523 // The transition must go from one block to another but it cannot be constellation-inert yet.
3525 {
3526//std::cerr << "Transition " << t.from() << " -" << m_aut.action_label(t.label()) << "-> " << t.to() << " becomes non-inert.\n";
3527 assert(is_inert_during_init(t));
3528 assert(m_states[t.to()].block!=m_states[t.from()].block);
3529 assert(m_blocks[m_states[t.to()].block].constellation == m_blocks[m_states[t.from()].block].constellation);
3530 m_states[t.from()].no_of_outgoing_inert_transitions--;
3531 }
3532
3533 void change_non_bottom_state_to_bottom_state(const std::vector<state_type_gj>::iterator si)
3534 {
3535 assert(m_states.begin()<=si);
3536 assert(si<m_states.end());
3537 // Move this former non-bottom state to the bottom states.
3538 // The block of si is not yet inserted into the set of blocks with new bottom states.
3539 block_index bi = si->block;
3540//std::cerr << si->debug_id(*this) << " becomes a new bottom state of " << m_blocks[bi].debug_id(*this) << ".\n";
3541 assert(0 == si->no_of_outgoing_inert_transitions);
3542 assert(!m_blocks[bi].contains_new_bottom_states);
3543 swap_states_in_states_in_block(si->ref_states_in_blocks, m_blocks[bi].start_non_bottom_states);
3544 m_blocks[bi].start_non_bottom_states++;
3545 }
3546
3547 // Split block B in R, being the inert-tau transitive closure of M contains
3548 // states that must be in block, and M\R. M_nonmarked, minus those in unmarked_blocker, are those in the other block.
3549 // The splitting is done in time O(min(|R|,|B\R|). Returns the block index of the R-block.
3551 std::vector<state_in_block_pointer>::iterator first_unmarked_bottom_state,
3552 const BLC_list_iterator splitter_end_unmarked_BLC /* = splitter.start_marked_BLC -- but this default argument is not allowed */,
3554 constellation_index old_constellation = null_constellation,
3555 #else
3556 std::function<void(const block_index, const block_index, const transition_index, const transition_index)>
3557 update_block_label_to_cotransition = [](const block_index, const block_index, const transition_index, const transition_index){},
3558 #endif
3559 // const bool initialisation=false,
3560 //std::function<void(const transition_index, const transition_index, const block_index)> process_transition=
3561 // [](const transition_index, const transition_index, const block_index){},
3562 const bool split_off_new_bottom_states = true)
3563 {
3564//std::cerr << "splitB(splitter = " << splitter->debug_id(*this) << ", first_unmarked_bottom_state = " << first_unmarked_bottom_state->ref_state->debug_id(*this) << ", splitter_end_unmarked_BLC = "
3565//<< (split_off_new_bottom_states && splitter_end_unmarked_BLC == splitter->start_marked_BLC ? "start_marked_BLC" : (splitter_end_unmarked_BLC == splitter->start_same_BLC ? "start_same_BLC" : "?")) << ", ..., split_off_new_bottom_states = " << split_off_new_bottom_states << ")\n";
3566 const block_index B = m_states[m_aut.get_transitions()[*splitter->start_same_BLC].from()].block;
3567//std::cerr << "Marked bottom states:"; for (std::vector<state_in_block_pointer>::iterator it=m_blocks[B].start_bottom_states; it!=first_unmarked_bottom_state; ++it) { std::cerr << ' ' << std::distance(m_states.begin(), it->ref_state); }
3568//std::cerr << "\nUnmarked bottom states:"; for (std::vector<state_in_block_pointer>::iterator it=first_unmarked_bottom_state; it!=m_blocks[B].start_non_bottom_states; ++it) { std::cerr << ' ' << std::distance(m_states.begin(), it->ref_state); } std::cerr << "\nAdditionally, " << m_R.size() << " non-bottom states have been marked.\n";
3569 assert(!has_marked_transitions(*splitter));
3570 if (1 >= number_of_states_in_block(B))
3571 {
3572 mCRL2log(log::debug) << "Trying to split up singleton block " << B << '\n';
3574 return null_block;
3575 }
3576 block_index R_block = simple_splitB(B, splitter, first_unmarked_bottom_state, splitter_end_unmarked_BLC);
3577 const block_index bi = m_blocks.size() - 1;
3578//std::cerr << "Split block of size " << number_of_states_in_block(B) + number_of_states_in_block(bi) << " taking away " << number_of_states_in_block(bi) << " states\n";
3579 assert(bi == R_block || B == R_block);
3581
3582 // Because we visit all states of block bi and almost all their incoming and outgoing transitions,
3583 // we subsume all this bookkeeping in a single block counter:
3585 // Update the LBC_list, and bottom states, and invariant on inert transitions.
3586 const std::vector<state_in_block_pointer>::iterator start_new_bottom_states=m_blocks[R_block].start_non_bottom_states;
3587 linked_list<BLC_indicators>::iterator R_to_U_tau_splitter = m_blocks[R_block].block_to_constellation.end();
3588 bool skip_transitions_in_splitter = false;
3589 assert(m_blocks[bi].block_to_constellation.begin() == m_blocks[bi].block_to_constellation.end());
3590 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
3591 if (m_branching)
3592 {
3593 // insert an empty BLC set into m_blocks[bi].block_to_constellation
3594 // for the inert transitions out of m_blocks[bi],
3595 // to avoid the need to check whether such a BLC set already exists
3596 // in update_the_doubly_linked_list_LBC_new_block().
3597 // This set, if it remains empty, will need to be deleted
3598 // after updating the BLC sets.
3599 // (It may happen that there are actually no inert transitions. Then
3600 // the new list will contain some dummy empty element, which should
3601 // remain empty until it is deleted again later.)
3602 linked_list<BLC_indicators>::iterator perhaps_inert_ind=m_blocks[B].block_to_constellation.begin();
3603 assert(perhaps_inert_ind!=m_blocks[B].block_to_constellation.end());
3604 m_blocks[bi].block_to_constellation.emplace_front(perhaps_inert_ind->start_same_BLC, perhaps_inert_ind->start_same_BLC);
3605 assert(!m_blocks[bi].block_to_constellation.empty());
3606 }
3607 #endif
3608 #ifdef CO_SPLITTER_IN_BLC_LIST
3609 assert(m_BLC_indicators_to_be_deleted.empty());
3610 #endif
3611 if (split_off_new_bottom_states && bi == R_block)
3612 {
3613 // move splitter as a whole from its current list to the new list where it will be part of:
3614 // (This only works if the whole splitter BLC set has moved, i.e. only if split_off_new_bottom_states == true.)
3615 #ifdef CO_SPLITTER_IN_BLC_LIST
3616 if (null_constellation != old_constellation)
3617 {
3618 #ifndef NDEBUG
3619 const constellation_index to_constln = m_blocks[m_states[m_aut.get_transitions()[*splitter->start_same_BLC].to()].block].constellation;
3620 assert(to_constln == old_constellation || to_constln == m_constellations.size() - 1);
3621 #endif
3622 // insert a dummy splitter to help with placing the corresponding main/co splitter correctly:
3624 m_blocks[R_block].block_to_constellation.emplace_after(splitter, splitter->end_same_BLC, splitter->end_same_BLC)
3625 );
3626 }
3627 #endif
3628 m_blocks[R_block].block_to_constellation.splice_to_after(
3630 m_blocks[R_block].block_to_constellation.begin(),
3631 #else
3632 m_blocks[R_block].block_to_constellation.end(),
3633 #endif
3634 m_blocks[B].block_to_constellation, splitter);
3635 skip_transitions_in_splitter = true;
3636 }
3637 // Recall new LBC positions.
3638 for(std::vector<state_in_block_pointer>::iterator ssi=m_blocks[bi].start_bottom_states;
3639 ssi!=m_blocks[bi].end_states;
3640 ++ssi)
3641 {
3642 state_type_gj& s=*ssi->ref_state;
3643 assert(s.ref_states_in_blocks == ssi);
3644 // mCRL2complexity_gj(s, add_work(..., max_bi_counter), *this);
3645 // is subsumed in the above call
3646 assert(s.block == bi);
3647
3648 const outgoing_transitions_it end_it=(std::next(ssi->ref_state)==m_states.end()) ? m_outgoing_transitions.end() : std::next(ssi->ref_state)->start_outgoing_transitions;
3649 // if (!initialisation) // update the BLC_lists.
3650 {
3651 for(outgoing_transitions_it ti=s.start_outgoing_transitions; ti!=end_it; ti++)
3652 {
3653 assert(m_states.begin()+m_aut.get_transitions()[*ti->ref_BLC_transitions].from()==ssi->ref_state);
3654 // mCRL2complexity_gj(&m_transitions[*ti->ref_BLC_transitions], add_work(..., max_bi_counter), *this);
3655 // is subsumed in the above call
3656 transition_index old_remaining_transition;
3657 if (!skip_transitions_in_splitter || m_transitions[*ti->ref_BLC_transitions].transitions_per_block_to_constellation != splitter)
3658 {
3659 old_remaining_transition=update_the_doubly_linked_list_LBC_new_block(B, bi, *ti->ref_BLC_transitions
3661 , old_constellation
3662 #endif
3663 );
3664 }
3665 else
3666 {
3667 // No need to move the splitter transitions individually.
3668 old_remaining_transition = null_transition;
3669 }
3670 //process_transition(*ti->ref_BLC_transitions, old_remaining_transition, B);
3671 #ifdef CO_SPLITTER_IN_BLC_LIST
3672 (void) old_remaining_transition; // avoid unused variable warning
3673 #else
3674 update_block_label_to_cotransition(B, bi, *ti->ref_BLC_transitions, old_remaining_transition);
3675 #endif
3676 }
3677 }
3678
3679 // Situation below is only relevant if the new block contains the R-states:
3680 if (bi == R_block && 0 < s.no_of_outgoing_inert_transitions)
3681 {
3682 assert(ssi >= m_blocks[R_block].start_non_bottom_states);
3683 // si is a non_bottom_state in the smallest block containing M..
3684 bool non_bottom_state_becomes_bottom_state = true;
3685
3686 for(outgoing_transitions_it ti=s.start_outgoing_transitions; ti!=end_it; ti++)
3687 {
3688 // mCRL2complexity_gj(&m_transitions[*ti->ref_BLC_transitions], add_work(..., max_bi_counter), *this);
3689 // is subsumed in the above call
3690 const transition& t=m_aut.get_transitions()[/*initialisation?ti->transition:*/ *ti->ref_BLC_transitions];
3691 assert(m_states.begin()+t.from()==ssi->ref_state);
3693 {
3694 if (m_states[t.to()].block==B)
3695 {
3696 // This is a transition that has become non-inert.
3698 const linked_list<BLC_indicators>::iterator new_splitter = m_transitions[*ti->ref_BLC_transitions].transitions_per_block_to_constellation;
3699 if (R_to_U_tau_splitter == m_blocks[R_block].block_to_constellation.end())
3700 {
3701 #ifndef SAVE_BLC_MEMORY
3702 assert(!has_marked_transitions(*new_splitter));
3703 #endif
3704 }
3705 else
3706 {
3707 assert(R_to_U_tau_splitter == new_splitter);
3708 assert(has_marked_transitions(*new_splitter));
3709 }
3710 R_to_U_tau_splitter = new_splitter;
3711 // immediately mark this transition, in case we get new bottom states:
3713 }
3714 else if (m_states[t.to()].block==R_block)
3715 {
3716 non_bottom_state_becomes_bottom_state=false; // There is an outgoing inert tau. State remains non-bottom.
3717 }
3718 }
3719 }
3720 if (non_bottom_state_becomes_bottom_state)
3721 {
3722 // The state at si has become a bottom_state.
3723 assert(m_blocks[R_block].block_to_constellation.end() != R_to_U_tau_splitter);
3725 }
3726 }
3727
3728 // Investigate the incoming formerly inert tau transitions.
3729 if (bi != R_block && m_blocks[R_block].start_non_bottom_states < m_blocks[R_block].end_states)
3730 {
3731 const std::vector<transition>::iterator it_end = std::next(ssi->ref_state)>=m_states.end() ? m_aut.get_transitions().end() : std::next(ssi->ref_state)->start_incoming_transitions;
3732 for(std::vector<transition>::iterator it=s.start_incoming_transitions;
3733 it!=it_end; it++)
3734 {
3735 const transition& t=*it;
3736 // mCRL2complexity_gj(&m_transitions[std::distance(m_aut.get_transitions().begin(), it)], add_work(..., max_bi_counter), *this);
3737 // is subsumed in the above call
3738 assert(m_states.begin()+t.to()==ssi->ref_state);
3739 if (!m_aut.is_tau(m_aut.apply_hidden_label_map(t.label())))
3740 {
3741 break; // All tau transitions have been investigated.
3742 }
3743
3744 const std::vector<state_type_gj>::iterator from(m_states.begin()+t.from());
3745 if (from->block==R_block && !(m_preserve_divergence && from==ssi->ref_state))
3746 {
3747 // This transition did become non-inert.
3749 const linked_list<BLC_indicators>::iterator new_splitter = m_transitions[std::distance(m_aut.get_transitions().begin(), it)].transitions_per_block_to_constellation;
3750 if (R_to_U_tau_splitter == m_blocks[R_block].block_to_constellation.end())
3751 {
3752 assert(!has_marked_transitions(*new_splitter));
3753 }
3754 else
3755 {
3756 assert(R_to_U_tau_splitter == new_splitter);
3757 assert(has_marked_transitions(*new_splitter));
3758 }
3759 R_to_U_tau_splitter = new_splitter;
3760 // immediately mark this transition, in case we get new bottom states:
3761 mark_BLC_transition(m_transitions[std::distance(m_aut.get_transitions().begin(), it)].ref_outgoing_transitions);
3762
3763 // Check whether from is a new bottom state.
3764 if (from->no_of_outgoing_inert_transitions==0)
3765 {
3766 // This state has no more outgoing inert transitions. It becomes a bottom state.
3768 }
3769 }
3770 }
3771 }
3772 }
3773 assert(m_blocks[R_block].start_bottom_states < m_blocks[R_block].start_non_bottom_states);
3774 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
3775 if (m_branching)
3776 {
3777 // Before the loop we inserted an empty BLC set for the inert transitions
3778 // into m_blocks[bi].block_to_constellation.
3779 // If it is still empty, we have to remove it again.
3780 linked_list<BLC_indicators>::iterator perhaps_inert_ind=m_blocks[bi].block_to_constellation.begin();
3781 if (perhaps_inert_ind->start_same_BLC==perhaps_inert_ind->end_same_BLC)
3782 {
3783 m_blocks[bi].block_to_constellation.erase(perhaps_inert_ind);
3784 }
3785 }
3786 #endif
3787 #ifdef CO_SPLITTER_IN_BLC_LIST
3788 for (std::vector<linked_list<BLC_indicators>::iterator>::iterator it = m_BLC_indicators_to_be_deleted.begin(); it < m_BLC_indicators_to_be_deleted.end(); ++it)
3789 {
3790 m_blocks[B].block_to_constellation.erase(*it);
3791 }
3793 #ifndef NDEBUG
3794 for (const BLC_indicators& B_it : m_blocks[B].block_to_constellation)
3795 {
3796 assert(B_it.start_same_BLC < B_it.end_same_BLC);
3797 }
3798 for (const BLC_indicators& bi_it : m_blocks[bi].block_to_constellation)
3799 {
3800 assert(bi_it.start_same_BLC < bi_it.end_same_BLC);
3801 }
3802 #endif
3803 #endif
3804
3805 #ifdef CHECK_COMPLEXITY_GJ
3807 if (bi == R_block)
3808 {
3809 // account for the work in R
3810 for (typename std::vector<state_in_block_pointer>::iterator s=m_blocks[bi].start_bottom_states;
3811 s!=m_blocks[bi].end_states; ++s)
3812 {
3814 // incoming tau-transitions of s
3815 const std::vector<transition>::iterator in_ti_end = std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end() : std::next(s->ref_state)->start_incoming_transitions;
3816 for (std::vector<transition>::iterator ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
3817 {
3818 if (!m_aut.is_tau(m_aut.apply_hidden_label_map(ti->label()))) break;
3820 }
3821 // outgoing transitions of s
3822 const outgoing_transitions_it out_ti_end=std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end() : std::next(s->ref_state)->start_outgoing_transitions;
3823 for (outgoing_transitions_it ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
3824 {
3826 // We also need to cancel the work on outgoing transitions of U-state candidates that turned out to be new bottom states:
3827 mCRL2complexity_gj(&m_transitions[/*initialisation?ti->transition:*/ *ti->ref_BLC_transitions], cancel_work(check_complexity::simple_splitB_U__handle_transition_from_potential_U_state), *this);
3828 }
3829 }
3830 // ensure not too much work has been done on U
3831 for (std::vector<state_in_block_pointer>::iterator s=m_blocks[B].start_bottom_states;
3832 s!=m_blocks[B].end_states; ++s)
3833 {
3836 // incoming tau-transitions of s
3837 const std::vector<transition>::iterator in_ti_end=std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end() : std::next(s->ref_state)->start_incoming_transitions;
3838 for (std::vector<transition>::iterator ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
3839 {
3840 if (!m_aut.is_tau(m_aut.apply_hidden_label_map(ti->label()))) break;
3841 mCRL2complexity_gj(&m_transitions[std::distance(m_aut.get_transitions().begin(), ti)], cancel_work(check_complexity::simple_splitB_U__handle_transition_to_U_state), *this);
3842 }
3843 // outgoing transitions of s
3844 const outgoing_transitions_it out_ti_end=std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end() : std::next(s->ref_state)->start_outgoing_transitions;
3845 for (outgoing_transitions_it ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
3846 {
3847 mCRL2complexity_gj(&m_transitions[/*initialisation?ti->transition:*/ *ti->ref_BLC_transitions], cancel_work(check_complexity::simple_splitB_U__handle_transition_from_potential_U_state), *this);
3848 }
3849 }
3850 }
3851 else
3852 {
3853 // account for the work in U
3854 for (typename std::vector<state_in_block_pointer>::iterator s=m_blocks[bi].start_bottom_states;
3855 s!=m_blocks[bi].end_states; ++s)
3856 {
3859 // incoming tau-transitions of s
3860 const std::vector<transition>::iterator in_ti_end = std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end() : std::next(s->ref_state)->start_incoming_transitions;
3861 for (std::vector<transition>::iterator ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
3862 {
3863 if (!m_aut.is_tau(m_aut.apply_hidden_label_map(ti->label()))) break;
3865 }
3866 // outgoing transitions of s
3867 const outgoing_transitions_it out_ti_end=std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end() : std::next(s->ref_state)->start_outgoing_transitions;
3868 for (outgoing_transitions_it ti = s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
3869 {
3871 }
3872 }
3873 // ensure not too much work has been done on R
3874 for (typename std::vector<state_in_block_pointer>::iterator s=m_blocks[B].start_bottom_states;
3875 s!=m_blocks[B].end_states; ++s)
3876 {
3878 // incoming tau-transitions of s
3879 const std::vector<transition>::iterator in_ti_end = std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end() : std::next(s->ref_state)->start_incoming_transitions;
3880 for (std::vector<transition>::iterator ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
3881 {
3882 if (!m_aut.is_tau(m_aut.apply_hidden_label_map(ti->label()))) break;
3883 mCRL2complexity_gj(&m_transitions[std::distance(m_aut.get_transitions().begin(), ti)], cancel_work(check_complexity::simple_splitB_R__handle_transition_to_R_state), *this);
3884 }
3885 // outgoing transitions of s
3886 const outgoing_transitions_it out_ti_end=std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end() : std::next(s->ref_state)->start_outgoing_transitions;
3887 for (outgoing_transitions_it ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
3888 {
3889 mCRL2complexity_gj(&m_transitions[/*initialisation?ti->transition:*/ *ti->ref_BLC_transitions], cancel_work(check_complexity::simple_splitB_R__handle_transition_from_R_state), *this);
3890 // We also need to move the work on outgoing transitions of U-state candidates that turned out to be new bottom states:
3892 0==s->ref_state->no_of_outgoing_inert_transitions ? 1 : 0), *this);
3893 }
3894 }
3895 }
3897 #endif // ifdef CHECK_COMPLEXITY_GJ
3898
3899 if (split_off_new_bottom_states && start_new_bottom_states < m_blocks[R_block].start_non_bottom_states)
3900 {
3901 // There are new bottom states, and we have to separate them immediately from the old bottom states.
3902 // This will make sure that the next call of stabilizeB() will not encounter blocks with both old and new bottom states.
3903 assert(m_blocks[R_block].block_to_constellation.end() != R_to_U_tau_splitter);
3904 assert(has_marked_transitions(*R_to_U_tau_splitter));
3905
3906 block_index new_bottom_block;
3907 if (start_new_bottom_states == m_blocks[R_block].start_bottom_states)
3908 {
3909 // all bottom states in this block are new
3910 // unmark_all_transitions(R_to_U_tau_splitter); -- will be done below
3911 new_bottom_block = R_block;
3912 R_block = null_block;
3913 }
3914 else
3915 {
3916 assert(number_of_states_in_block(R_block) > 1);
3917 // Some tau-transitions from R to U may come out of states that are not (yet) new bottom states.
3918 // Therefore we still have to go through the movement of constructing m_R:
3919 const BLC_list_iterator splitter_end_unmarked_BLC = R_to_U_tau_splitter->start_same_BLC;
3920 first_unmarked_bottom_state = not_all_bottom_states_are_touched(R_to_U_tau_splitter
3921 #ifndef NDEBUG
3922 , splitter_end_unmarked_BLC
3923 #endif
3924 );
3925 assert(std::distance(start_new_bottom_states, m_blocks[R_block].start_non_bottom_states) ==
3926 std::distance(m_blocks[R_block].start_bottom_states, first_unmarked_bottom_state));
3927 assert(m_blocks[R_block].start_bottom_states < first_unmarked_bottom_state);
3928 assert(first_unmarked_bottom_state < m_blocks[R_block].start_non_bottom_states);
3929 new_bottom_block = splitB(R_to_U_tau_splitter, first_unmarked_bottom_state,
3930 splitter_end_unmarked_BLC,
3932 old_constellation,
3933 #else
3934 update_block_label_to_cotransition,
3935 #endif
3936 //process_transition,
3937 false);
3938 if (R_block == new_bottom_block)
3939 {
3940 R_block = m_blocks.size() - 1;
3941 }
3942 }
3943 assert(0 <= new_bottom_block); assert(new_bottom_block < m_blocks.size());
3944 assert(!m_blocks[new_bottom_block].contains_new_bottom_states);
3945//std::cerr << "new_bottom_block = " << new_bottom_block << ", R_block = " << static_cast<std::make_signed<block_index>::type>(R_block) << '\n';
3946 m_blocks[new_bottom_block].contains_new_bottom_states = true;
3947 m_blocks_with_new_bottom_states.push_back(new_bottom_block);
3948 }
3949 else if (m_blocks[R_block].block_to_constellation.end() != R_to_U_tau_splitter)
3950 {
3951 // unmark the transitions from R to U.
3952 // We do not need to stabilize the (formerly inert) tau-transitions from R to U,
3953 // because they are still in the same constellation.
3954 unmark_all_transitions(*R_to_U_tau_splitter);
3955 }
3956
3957 return R_block;
3958 }
3959
3960 /* void accumulate_entries_into_not_investigated(std::vector<label_count_sum_triple>& action_counter,
3961 const std::vector<block_index>& todo_stack)
3962 {
3963 transition_index sum=0;
3964 for(block_index index: todo_stack)
3965 {
3966 // The caller has to account for this work.
3967 // Typically, it can be accounted for because todo_stack has been filled
3968 // by actions that are counted.
3969 action_counter[index].not_investigated=sum;
3970 sum=sum+action_counter[index].label_counter;
3971 }
3972 }
3973
3974 void accumulate_entries(std::vector<transition_index>& counter)
3975 {
3976 transition_index sum=0;
3977 for(transition_index& index: counter)
3978 {
3979 transition_index n=index;
3980 index=sum;
3981 sum=sum+n;
3982 }
3983 }
3984
3985 void reset_entries(std::vector<label_count_sum_triple>& action_counter,
3986 std::vector<block_index>& todo_stack)
3987 {
3988 for(block_index index: todo_stack)
3989 {
3990 // To account for this work, we need to ensure that todo_stack has only
3991 // been filled by actions that have been accounted for already.
3992 // it is not necessary to reset the cumulative_label_counter;
3993 action_counter[index].label_counter=0;
3994 }
3995 todo_stack.clear();
3996 } */
3997
3998 transition_index accumulate_entries(std::vector<transition_index>& action_counter,
3999 const std::vector<label_index>& todo_stack) const
4000 {
4001 transition_index sum=0;
4002 for(label_index index: todo_stack)
4003 {
4004 transition_index n=sum;
4005 sum=sum+action_counter[index];
4006 action_counter[index]=n;
4007 }
4008 return sum;
4009 }
4010
4011/* // Group the elements from begin up to end, using a range from [0,number of blocks),
4012 // where each transition pinpointed by the iterator has as value its source block.
4013
4014 void group_in_situ(const std::vector<transition_index>::iterator begin,
4015 const std::vector<transition_index>::iterator end,
4016 std::vector<block_index>& todo_stack,
4017 std::vector<label_count_sum_triple>& value_counter)
4018 {
4019 // Initialise the action counter.
4020 // The work in reset_entries() can be subsumed under mCRL2complexity calls
4021 // that have been issued in earlier executions of group_in_situ().
4022 reset_entries(value_counter, todo_stack);
4023 #ifdef CHECK_COMPLEXITY_GJ
4024 const constellation_index new_constellation = m_constellations.size()-1;
4025 const unsigned max_C = check_complexity::log_n - check_complexity::ilog2(number_of_states_in_constellation(new_constellation));
4026 #endif
4027 for(std::vector<transition_index>::iterator i=begin; i!=end; ++i)
4028 {
4029 const transition& t = m_aut.get_transitions()[*i];
4030 #ifdef CHECK_COMPLEXITY_GJ
4031 assert(m_blocks[m_states[t.to()].block].constellation == new_constellation);
4032 mCRL2complexity_gj(&m_transitions[*i], add_work(check_complexity::group_in_situ__count_transitions_per_block, max_C), *this);
4033 #endif
4034 const block_index n=m_states[t.from()].block;
4035
4036 // mCRL2complexity_gj(..., add_work(..., ...), *this);
4037 if (value_counter[n].label_counter==0)
4038 {
4039 todo_stack.push_back(n);
4040 }
4041 value_counter[n].label_counter++;
4042 }
4043
4044 // The work in accumulate_entries_into_not_investigated() can be subsumed
4045 // under the above call to mCRL2complexity, because an entry in todo_stack
4046 // is only made if there is at least one transition from that block.
4047 accumulate_entries_into_not_investigated(value_counter, todo_stack);
4048
4049 std::vector<block_index>::iterator current_value=todo_stack.begin();
4050 for(std::vector<transition_index>::iterator i=begin; i!=end; )
4051 {
4052 mCRL2complexity_gj(&m_transitions[*i], add_work(check_complexity::group_in_situ__swap_transition, max_C), *this);
4053 block_index n=m_states[m_aut.get_transitions()[*i].from()].block;
4054 if (n==*current_value)
4055 {
4056 value_counter[n].label_counter--;
4057 value_counter[n].not_investigated++;
4058 ++i;
4059 while (assert(current_value!=todo_stack.end()), value_counter[n].label_counter==0)
4060 {
4061 #ifdef CHECK_COMPLEXITY_GJ
4062 // This work needs to be assigned to some transition from block n.
4063 // Just to make sure we assign it to all such transitions:
4064 std::vector<transition_index>::iterator work_i = i;
4065 assert(begin != work_i);
4066 --work_i;
4067 assert(m_states[m_aut.get_transitions()[*work_i].from()].block == n);
4068 do
4069 {
4070 mCRL2complexity_gj(&m_transitions[*work_i], add_work(check_complexity::group_in_situ__skip_to_next_block, max_C), *this);
4071 }
4072 while (begin != work_i && m_states[m_aut.get_transitions()[*--work_i].from()].block == n);
4073 #endif
4074 current_value++;
4075 if (current_value!=todo_stack.end())
4076 {
4077 n = *current_value;
4078 i=begin+value_counter[n].not_investigated; // Jump to the first non investigated action.
4079 }
4080 else
4081 {
4082 assert(i == end);
4083 break; // exit the while and the for loop.
4084 }
4085 }
4086 }
4087 else
4088 {
4089 // Find the first transition with a different label than t.label to swap with.
4090 std::vector<transition_index>::iterator new_position=begin+value_counter[n].not_investigated;
4091 while (m_states[m_aut.get_transitions()[*new_position].from()].block==n)
4092 {
4093 mCRL2complexity_gj(&m_transitions[*new_position], add_work(check_complexity::group_in_situ__swap_transition, max_C), *this);
4094 value_counter[n].not_investigated++;
4095 value_counter[n].label_counter--;
4096 new_position++;
4097 assert(new_position!=end);
4098 }
4099 assert(value_counter[n].label_counter>0);
4100 std::swap(*i, *new_position);
4101 value_counter[n].not_investigated++;
4102 value_counter[n].label_counter--;
4103 }
4104 }
4105 } */
4106
4107//================================================= Create initial partition ========================================================
4109 {
4110 mCRL2log(log::verbose) << "An O(m log n) "
4112 ? "divergence-preserving branching "
4113 : "branching ")
4114 : "")
4115 << "bisimulation partitioner created for " << m_aut.num_states()
4116 << " states and " << m_aut.num_transitions() << " transitions (using the experimental algorithm GJ2024).\n";
4117 // Initialisation.
4118 #ifdef CHECK_COMPLEXITY_GJ
4119 check_complexity::init(2 * m_aut.num_states()); // we need ``2*'' because there is one additional call to splitB during initialisation
4120 #endif
4121
4122 // Initialise m_incoming_(non-)inert-transitions, m_outgoing_transitions, and m_states[si].no_of_outgoing_transitions
4123 //group_transitions_on_label(m_aut.get_transitions(),
4124 // [](const transition& t){ return m_aut.apply_hidden_label_map(t.label()); },
4125 // m_aut.num_action_labels(), m_aut.tau_label_index()); // sort on label. Tau transitions come first.
4126 // group_transitions_on_label(m_aut.get_transitions(),
4127 // [](const transition& t){ return t.from(); },
4128 // m_aut.num_states(), 0); // sort on label. Tau transitions come first.
4129 // group_transitions_on_label_tgt(m_aut.get_transitions(), m_aut.num_action_labels(), m_aut.tau_label_index(), m_aut.num_states()); // sort on label. Tau transitions come first.
4130 // group_transitions_on_tgt(m_aut.get_transitions(), m_aut.num_action_labels(), m_aut.tau_label_index(), m_aut.num_states()); // sort on label. Tau transitions come first.
4131 // sort_transitions(m_aut.get_transitions(), lbl_tgt_src);
4132// David suggests: I think it is enough to sort according to tgt_lbl.
4133// JFG answers: Agreed. But I believe this will cost performance. For 1394-fin-vvlarge this saves 1 second to sort, but
4134// requires five more seconds to carry out the splitting. Apparently, there is benefit to have src together.
4135// This may have been measured on an older version of the code.
4136 sort_transitions(m_aut.get_transitions(), m_aut.hidden_label_set(), tgt_lbl_src); // THIS IS NOW ESSENTIAL.
4137 // sort_transitions(m_aut.get_transitions(), src_lbl_tgt);
4138 // sort_transitions(m_aut.get_transitions(), tgt_lbl);
4139 // sort_transitions(m_aut.get_transitions(), target);
4140
4141 // Count the number of occurring action labels.
4142 assert((unsigned) m_preserve_divergence <= 1);
4143
4144 mCRL2log(log::verbose) << "Start initialisation of the BLC list in the initialisation\n";
4145 {
4146 std::vector<label_index> todo_stack_actions;
4147 std::vector<transition_index> count_transitions_per_action(m_aut.num_action_labels() + (unsigned) m_preserve_divergence, 0);
4148// David suggests: The above allocation may take time up to O(|Act|).
4149// This is a place where the number of actions plays a role.
4150// JFG answers: I think we should accept that the algorithm has a complexity of .... + O(|Act|). Act can be assumed to be smaller
4151// than m, and n can be assumed to be bigger than 1. In that case O(|Act|) will be subsumed.
4152 if (m_branching)
4153 {
4154 todo_stack_actions.push_back(m_aut.tau_label_index()); // ensure that inert transitions come first
4155 count_transitions_per_action[m_aut.tau_label_index()] = 1; // set the number of transitions to a nonzero value so it doesn't trigger todo_stack_actions.push_back(...) in the loop
4156 }
4157 for(transition_index ti=0; ti<m_aut.num_transitions(); ++ti)
4158 {
4159 const transition& t=m_aut.get_transitions()[ti];
4160 // mCRL2complexity_gj(&m_transitions[ti], add_work(..., 1), *this);
4161 // Because every transition is touched exactly once, we do not store a physical counter for this.
4163 transition_index& c=count_transitions_per_action[label];
4164 if (c==0)
4165 {
4166 todo_stack_actions.push_back(label);
4167 }
4168 c++;
4169 }
4170 if (m_branching)
4171 {
4172 assert(m_aut.is_tau(todo_stack_actions.front()));
4173 --count_transitions_per_action[m_aut.tau_label_index()];
4174 }
4175//std::cerr << "COUNT_TRANSITIONS PER ACT1 "; for(auto s: count_transitions_per_action){ std::cerr << s << " "; } std::cerr << "\n";
4176 accumulate_entries(count_transitions_per_action, todo_stack_actions);
4177//std::cerr << "COUNT_TRANSITIONS PER ACT2 "; for(auto s: count_transitions_per_action){ std::cerr << s << " "; } std::cerr << "\n";
4178 for(transition_index ti=0; ti<m_aut.num_transitions(); ++ti)
4179 {
4180 // mCRL2complexity_gj(&m_transitions[ti], add_work(..., 1), *this);
4181 // Because every transition is touched exactly once, we do not store a physical counter for this.
4182 const transition& t=m_aut.get_transitions()[ti];
4184 transition_index& c=count_transitions_per_action[label];
4185 assert(0 <= c); assert(c < m_aut.num_transitions());
4186 m_BLC_transitions[c]=ti;
4187 c++;
4188 }
4189
4190 // create BLC_indicators for every action label:
4191 BLC_list_iterator start_index = m_BLC_transitions.begin();
4192 for(label_index a: todo_stack_actions)
4193 {
4194 // mCRL2complexity_gj(..., add_work(..., 1), *this);
4195 // not needed because the inner loop is always executed (except possibly for 1 iteration)
4196//std::cerr << " Initialising m_BLC_transitions for action " << (m_aut.num_action_labels() == a ? "(tau-self-loops)" : pp(m_aut.action_label(a))) << '\n';
4197 const BLC_list_iterator end_index = m_BLC_transitions.begin() + count_transitions_per_action[a];
4198 assert(end_index <= m_BLC_transitions.end());
4199 if (start_index == end_index)
4200 {
4201 assert(m_branching); assert(m_aut.is_tau(a));
4202 }
4203 else
4204 {
4205 assert(start_index < end_index);
4206 // create a BLC_indicator and insert it into the list...
4207 typename linked_list<BLC_indicators>::iterator current_BLC = m_blocks[0].block_to_constellation.emplace_after(m_blocks[0].block_to_constellation.begin(), start_index, end_index);
4208 if (!is_inert_during_init(m_aut.get_transitions()[*start_index]))
4209 {
4210 current_BLC->start_marked_BLC = start_index; // mark all states in this BLC_indicator for the initial stabilization
4211 }
4212 do
4213 {
4214 // mCRL2complexity_gj(&m_transitions[*start_index], add_work(..., 1), *this);
4215 // Because every transition is touched exactly once, we do not store a physical counter for this.
4216 m_transitions[*start_index].transitions_per_block_to_constellation = current_BLC;
4217 }
4218 while (++start_index < end_index);
4219 }
4220 }
4221 assert(start_index == m_BLC_transitions.end());
4222
4223 // destroy and deallocate todo_stack_actions and count_transitions_per_action here.
4224 }
4225
4226 // Group transitions per outgoing state.
4227 mCRL2log(log::verbose) << "Start setting outgoing transitions\n";
4228 {
4229
4230 std::vector<transition_index> count_outgoing_transitions_per_state(m_aut.num_states(), 0);
4231 for(const transition& t: m_aut.get_transitions())
4232 {
4233 // mCRL2complexity_gj(&m_transitions[std::distance(&*m_aut.get_transitions.begin(), &t)], add_work(..., 1), *this);
4234 // Because every transition is touched exactly once, we do not store a physical counter for this.
4235 count_outgoing_transitions_per_state[t.from()]++;
4236 if (is_inert_during_init(t))
4237 {
4238 m_states[t.from()].no_of_outgoing_inert_transitions++;
4239 }
4240 }
4241
4242 // We now set the outgoing transition per state pointer to the first non-inert transition.
4243 // The counters for outgoing transitions calculated above are reset to 0
4244 // and will later contain the number of transitions already stored.
4245 // Every time an inert transition is stored, the outgoing transition per state pointer is reduced by one.
4246 outgoing_transitions_it current_outgoing_transitions = m_outgoing_transitions.begin();
4247
4248 // place transitions and set the pointers to incoming/outgoing transitions
4249 for (state_index s = 0; s < m_aut.num_states(); ++s)
4250 {
4251 // mCRL2complexity_gj(&m_states[s], add_work(..., 1), *this);
4252 // Because every state is touched exactly once, we do not store a physical counter for this.
4253 m_states[s].start_outgoing_transitions = current_outgoing_transitions + m_states[s].no_of_outgoing_inert_transitions;
4254 current_outgoing_transitions += count_outgoing_transitions_per_state[s];
4255 count_outgoing_transitions_per_state[s] = 0; // meaning of this counter changes to: number of outgoing transitions already stored
4256 }
4257 assert(current_outgoing_transitions == m_outgoing_transitions.end());
4258
4259 mCRL2log(log::verbose) << "Moving incoming and outgoing transitions\n";
4260
4261 for(BLC_list_iterator ti = m_BLC_transitions.begin(); ti < m_BLC_transitions.end(); ++ti)
4262 {
4263 // mCRL2complexity_gj(&m_transitions[*ti], add_work(..., 1), *this);
4264 // Because every transition is touched exactly once, we do not store a physical counter for this.
4265 const transition& t=m_aut.get_transitions()[*ti];
4266 if (is_inert_during_init(t))
4267 {
4268 m_transitions[*ti].ref_outgoing_transitions = --m_states[t.from()].start_outgoing_transitions;
4269 }
4270 else
4271 {
4272 m_transitions[*ti].ref_outgoing_transitions = m_states[t.from()].start_outgoing_transitions + count_outgoing_transitions_per_state[t.from()];
4273 }
4274 m_transitions[*ti].ref_outgoing_transitions->ref_BLC_transitions = ti;
4275 ++count_outgoing_transitions_per_state[t.from()];
4276 }
4277 // destroy and deallocate count_outgoing_transitions_per_state here.
4278 }
4279
4280 state_index current_state=null_state;
4281 assert(current_state + 1 == 0);
4282 // bool tau_transitions_passed=true;
4283 // TODO: This should be combined with another pass through all transitions.
4284 for(std::vector<transition>::iterator it=m_aut.get_transitions().begin(); it!=m_aut.get_transitions().end(); it++)
4285 {
4286 // mCRL2complexity_gj(&m_transitions[std::distance(m_aut.get_transitions().begin(), it)], add_work(..., 1), *this);
4287 // Because every transition is touched exactly once, we do not store a physical counter for this.
4288 const transition& t=*it;
4289 if (t.to()!=current_state)
4290 {
4291 for (state_index i=current_state+1; i<=t.to(); ++i)
4292 {
4293 // ensure that every state is visited at most once:
4295//std::cerr << "SET start_incoming_transitions for state " << i << "\n";
4296 m_states[i].start_incoming_transitions=it;
4297 }
4298 current_state=t.to();
4299 }
4300 }
4301 for (state_index i=current_state+1; i<m_states.size(); ++i)
4302 {
4304//std::cerr << "SET residual start_incoming_transitions for state " << i << "\n";
4305 m_states[i].start_incoming_transitions=m_aut.get_transitions().end();
4306 }
4307
4308 // Set the start_same_saC fields in m_outgoing_transitions.
4310 if (m_outgoing_transitions.begin() < it)
4311 {
4312 --it;
4313 const transition& t = m_aut.get_transitions()[*it->ref_BLC_transitions];
4314 state_index current_state = t.from();
4315 label_index current_label = label_or_divergence(t);
4316 outgoing_transitions_it current_end_same_saC = it;
4317 while (m_outgoing_transitions.begin() < it)
4318 {
4319 --it;
4320 // mCRL2complexity_gj(&m_transitions[*it->ref_BLC_transitions], add_work(..., 1), *this);
4321 // Because every transition is touched exactly once, we do not store a physical counter for this.
4322 const transition& t = m_aut.get_transitions()[*it->ref_BLC_transitions];
4323 const label_index new_label = label_or_divergence(t);
4324 if (current_state == t.from() && current_label == new_label)
4325 {
4326 // We encounter a transition with the same saC. Let it refer to the end.
4327 it->start_same_saC = current_end_same_saC;
4328 }
4329 else
4330 {
4331 // We encounter a transition with a different saC.
4332 current_state = t.from();
4333 current_label = new_label;
4334 current_end_same_saC->start_same_saC = std::next(it);
4335 current_end_same_saC = it;
4336 }
4337 }
4338 current_end_same_saC->start_same_saC = m_outgoing_transitions.begin();
4339 }
4340
4341//std::cerr << "Start filling states_in_blocks\n";
4342 m_states_in_blocks.resize(m_aut.num_states());
4343 typename std::vector<state_in_block_pointer>::iterator lower_i=m_states_in_blocks.begin(), upper_i=m_states_in_blocks.end();
4344 for (std::vector<state_type_gj>::iterator i=m_states.begin(); i<m_states.end(); ++i)
4345 {
4346 // mCRL2complexity_gj(&m_states[i], add_work(..., 1), *this);
4347 // Because every state is touched exactly once, we do not store a physical counter for this.
4348 if (0<i->no_of_outgoing_inert_transitions)
4349 {
4350 --upper_i;
4351 upper_i->ref_state=i;
4352 i->ref_states_in_blocks=upper_i;
4353 }
4354 else
4355 {
4356 lower_i->ref_state=i;
4357 i->ref_states_in_blocks=lower_i;
4358 ++lower_i;
4359 }
4360 }
4361 assert(lower_i == upper_i);
4362 m_blocks[0].start_bottom_states=m_states_in_blocks.begin();
4363 m_blocks[0].start_non_bottom_states = lower_i;
4364 m_blocks[0].end_states=m_states_in_blocks.end();
4365