51#ifndef LIBLTS_BISIM_GJ_LAZY_BLC_H
52#define LIBLTS_BISIM_GJ_LAZY_BLC_H
60#include "mcrl2/lts/detail/check_complexity.h"
61#include "mcrl2/lts/detail/fixed_vector.h"
62#include "mcrl2/lts/detail/liblts_merge.h"
63#include "mcrl2/lts/detail/liblts_scc.h"
64#include "mcrl2/lts/detail/simple_list.h"
66#include <forward_list>
68#include <unordered_set>
71#include "mcrl2/lts/detail/liblts_bisim_gj.h"
82template <
class LTS_TYPE>
class bisim_partitioner_gj_lazy_BLC;
84namespace bisimulation_gj_lazy_BLC
88struct state_type_gj_lb;
90struct BLC_source_type;
91struct block_that_needs_refinement_type;
92struct constellation_type_lb;
93struct transition_type_lb;
94struct outgoing_transition_type_lb;
96using outgoing_transitions_it_lb = fixed_vector<outgoing_transition_type_lb>::iterator;
97using outgoing_transitions_const_it_lb = fixed_vector<outgoing_transition_type_lb>::const_iterator;
99constexpr constellation_type_lb* null_constellation_lb=
nullptr;
100constexpr block_type_lb* null_block_lb=
nullptr;
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
175struct outgoing_transition_type_lb
178 BLC_list_iterator ref_BLC_transitions;
184 outgoing_transitions_it_lb start_same_saC;
187 outgoing_transition_type_lb() =
default;
189 outgoing_transition_type_lb(
const outgoing_transitions_it_lb sssaC)
190 : start_same_saC(sssaC)
195struct state_in_block_pointer_lb
197 state_in_block_pointer_lb(fixed_vector<state_type_gj_lb>::iterator new_ref_state)
198 : ref_state(new_ref_state)
201 state_in_block_pointer_lb() =
default;
203 fixed_vector<state_type_gj_lb>::iterator ref_state;
205 bool operator==(
const state_in_block_pointer_lb other)
const
207 return ref_state==other.ref_state;
210 bool operator!=(
const state_in_block_pointer_lb other)
const
212 return ref_state!=other.ref_state;
218class todo_state_vector_lb
220 std::size_t m_todo_indicator=0;
221 std::vector<state_in_block_pointer_lb> m_vec;
224 using const_iterator =
225 std::vector<state_in_block_pointer_lb>::const_iterator;
227 bool find(
const state_in_block_pointer_lb s)
const
229 return std::find(m_vec.begin(), m_vec.end(), s)!=m_vec.end();
232 void add_todo(
const state_in_block_pointer_lb s)
237 std::size_t todo_is_empty()
const
239 return m_vec.size()<=m_todo_indicator;
243 state_in_block_pointer_lb move_from_todo()
244 { assert(!todo_is_empty());
245 state_in_block_pointer_lb result=m_vec[m_todo_indicator];
250 void swap_vec(std::vector<state_in_block_pointer_lb>& other_vec)
251 { assert(empty()); assert(0==m_todo_indicator);
252 m_vec = std::move(other_vec);
256 std::size_t size()
const
261 std::size_t empty()
const
263 return m_vec.empty();
266 const_iterator begin()
const
268 return m_vec.begin();
271 const_iterator end()
const
276 const state_in_block_pointer_lb* data()
const
281 const state_in_block_pointer_lb* data_end()
const
283 return m_vec.data() + m_vec.size();
286 const state_in_block_pointer_lb& front()
const
288 return m_vec.front();
291 void reserve(std::vector<state_in_block_pointer_lb>::size_type new_cap)
293 m_vec.reserve(new_cap);
296 using iterator = std::vector<state_in_block_pointer_lb>::iterator;
300 return m_vec.begin();
309 void add_todo(iterator begin, iterator end)
311 m_vec.insert(m_vec.end(), begin, end);
317 bisimulation_gj::clear(m_vec);
325struct state_type_gj_lb
328 block_type_lb* block = null_block_lb;
330 std::vector<transition>::iterator start_incoming_transitions;
332 outgoing_transitions_it_lb start_outgoing_transitions;
334 state_in_block_pointer_lb* ref_states_in_blocks =
nullptr;
336 transition_index no_of_outgoing_block_inert_transitions=0;
342 transition_index counter=undefined;
345 template<
class LTS_TYPE>
346 std::string debug_id_short(
const bisim_partitioner_gj_lazy_BLC<LTS_TYPE>& partitioner)
const
348 assert(partitioner.m_states.data()<=
this);
349 assert(
this<partitioner.m_states.data_end());
350 return std::to_string(
this-partitioner.m_states.data());
354 template<
class LTS_TYPE>
355 std::string debug_id(
const bisim_partitioner_gj_lazy_BLC<LTS_TYPE>& partitioner)
const
357 return "state " + debug_id_short(partitioner);
360 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
361 mutable check_complexity::state_gj_counter_t work_counter;
368struct BLC_indicators_lb
371 BLC_list_iterator start_same_BLC;
379 BLC_list_iterator_or_null start_marked_BLC;
382 BLC_list_iterator end_same_BLC;
398 bool starts_in_small_subblock =
true;
400 BLC_indicators_lb(BLC_list_iterator start, BLC_list_iterator end,
402 : start_same_BLC(start),
403 start_marked_BLC(is_stable ?
nullptr : end),
405 { assert(
nullptr!=start_same_BLC); assert(
nullptr!=end_same_BLC);
406 assert(start_same_BLC<=end_same_BLC);
409 bool is_stable()
const
410 { assert(
nullptr!=start_same_BLC); assert(
nullptr!=end_same_BLC);
411 assert(
nullptr==start_marked_BLC || start_same_BLC<=start_marked_BLC);
412 assert(
nullptr==start_marked_BLC || start_marked_BLC<=end_same_BLC);
413 assert(start_same_BLC<=end_same_BLC);
414 return nullptr==start_marked_BLC;
419 bool has_marked_transitions()
const
425 return start_marked_BLC<end_same_BLC;
429 { assert(!is_stable());
430 start_marked_BLC=
nullptr;
434 { assert(is_stable());
435 start_marked_BLC=end_same_BLC;
438 bool operator==(
const BLC_indicators_lb& other)
const
440 return start_same_BLC==other.start_same_BLC &&
441 start_marked_BLC==other.start_marked_BLC &&
442 end_same_BLC==other.end_same_BLC;
445 bool operator!=(
const BLC_indicators_lb& other)
const
447 return !operator==(other);
452 template<
class LTS_TYPE>
453 std::string debug_id(
const bisim_partitioner_gj_lazy_BLC<LTS_TYPE>& partitioner)
const
455 assert(partitioner.m_BLC_transitions.data()<=start_same_BLC);
456 assert(
nullptr==start_marked_BLC || start_same_BLC<=start_marked_BLC);
457 assert(
nullptr==start_marked_BLC || start_marked_BLC<=end_same_BLC);
458 assert(start_same_BLC<=end_same_BLC);
459 assert(end_same_BLC<=partitioner.m_BLC_transitions.data_end());
460 std::string result(
"super-BLC set ["+std::to_string(std::distance<BLC_list_const_iterator>(&*partitioner.m_BLC_transitions.begin(), start_same_BLC))+
","+std::to_string(std::distance<BLC_list_const_iterator>(&*partitioner.m_BLC_transitions.begin(), end_same_BLC))+
")");
461 if (start_same_BLC==end_same_BLC)
463 return "Empty "+result;
466 result += partitioner.m_states[partitioner.m_aut.get_transitions()[*start_same_BLC].from()].block->block_BLC_source->debug_id(partitioner);
468 result += partitioner.m_states[partitioner.m_aut.get_transitions()[*start_same_BLC].to()].block->constellation->debug_id(partitioner);
469 result +=
" containing the ";
470 if (std::distance(start_same_BLC, end_same_BLC)>1)
472 result+=std::to_string(std::distance(start_same_BLC, end_same_BLC));
473 result +=
" transitions ";
477 result +=
"transition ";
479 BLC_list_const_iterator iter = start_same_BLC;
480 if (start_marked_BLC == iter)
484 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
485 if (std::distance(start_same_BLC, end_same_BLC)>4)
488 result += start_marked_BLC == iter ?
" | " :
", ";
489 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
490 result += std::next(iter) == start_marked_BLC ?
" | ..."
491 : (!is_stable() && start_marked_BLC>std::next(iter) && start_marked_BLC<=end_same_BLC-3 ?
", ..|.." :
", ...");
492 iter = end_same_BLC-3;
494 while (++iter!=end_same_BLC)
496 result += start_marked_BLC == iter ?
" | " :
", ";
497 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
499 if (start_marked_BLC == iter)
506 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
507 mutable check_complexity::BLC_gj_counter_t work_counter;
516struct transition_type_lb
519 simple_list<BLC_indicators_lb>::iterator
520 transitions_per_block_to_constellation;
523 outgoing_transitions_it_lb ref_outgoing_transitions;
527 template<
class LTS_TYPE> std::string debug_id_short
528 (
const bisim_partitioner_gj_lazy_BLC<LTS_TYPE>& partitioner)
const
530 assert(partitioner.m_transitions.data()<=
this);
531 assert(
this<partitioner.m_transitions.data_end());
532 const transition& t=partitioner.m_aut.get_transitions()
533 [
this-partitioner.m_transitions.data()];
534 return partitioner.m_states[t.from()].debug_id_short(partitioner) +
" -" +
535 pp(partitioner.m_aut.action_label(t.label())) +
"-> " +
536 partitioner.m_states[t.to()].debug_id_short(partitioner);
541 template<
class LTS_TYPE> std::string debug_id
542 (
const bisim_partitioner_gj_lazy_BLC<LTS_TYPE>& partitioner)
const
544 return "transition " + debug_id_short(partitioner);
547 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
548 mutable check_complexity::trans_gj_counter_t work_counter;
567 constellation_type_lb* constellation;
572 state_in_block_pointer_lb* start_bottom_states;
574 union start_non_bottom_states_or_state_in_reduced_LTS
581 state_in_block_pointer_lb* rt_non_bottom_states;
588 state_index te_in_reduced_LTS;
590 start_non_bottom_states_or_state_in_reduced_LTS
591 (state_in_block_pointer_lb* s)
592 : rt_non_bottom_states(s)
597 state_in_block_pointer_lb* end_states;
602 BLC_source_type* block_BLC_source;
610 state_index refinement_info = null_state;
613 block_type_lb(
const block_type_lb& other)
614 : constellation(other.constellation),
615 start_bottom_states(other.start_bottom_states),
616 sta(other.sta.rt_non_bottom_states),
617 end_states(other.end_states),
618 block_BLC_source(other.block_BLC_source),
619 refinement_info(other.refinement_info),
620 contains_new_bottom_states(other.contains_new_bottom_states),
621 small_subblock_counter(other.small_subblock_counter)
628 char contains_new_bottom_states =
false;
634 char small_subblock_counter;
637 block_type_lb(state_in_block_pointer_lb* start_bottom,
638 state_in_block_pointer_lb* start_non_bottom,
639 state_in_block_pointer_lb* end,
640 constellation_type_lb& new_c,
641 BLC_source_type& new_bbs,
642 char new_small_subblock_counter)
643 : constellation(&new_c),
644 start_bottom_states(start_bottom),
645 sta(start_non_bottom),
647 block_BLC_source(&new_bbs),
648 small_subblock_counter(new_small_subblock_counter)
649 { assert(start_bottom<=start_non_bottom); assert(start_non_bottom<=end);
653 template<
class LTS_TYPE> std::string debug_id_short
654 (
const bisim_partitioner_gj_lazy_BLC<LTS_TYPE>& partitioner)
const
655 { assert(partitioner.m_states_in_blocks.data()<=start_bottom_states);
656 assert(start_bottom_states<=sta.rt_non_bottom_states);
657 assert(sta.rt_non_bottom_states<=end_states);
658 assert(end_states<=partitioner.m_states_in_blocks.data_end());
659 return "["+std::to_string(std::distance<
const state_in_block_pointer_lb*>
660 (partitioner.m_states_in_blocks.data(), start_bottom_states))+
","+
661 std::to_string(std::distance<
const state_in_block_pointer_lb*>
662 (partitioner.m_states_in_blocks.data(), end_states))+
")";
666 template<
class LTS_TYPE> std::string debug_id
667 (
const bisim_partitioner_gj_lazy_BLC<LTS_TYPE>& partitioner)
const
669 static const char block_name[6][7] = {
"BLOCK ",
"BLOCk ",
"BLOck ",
"BLock ",
"Block ",
"block " };
670 return block_name[small_subblock_counter>5 ? 5 : small_subblock_counter] + debug_id_short(partitioner);
673 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
674 mutable check_complexity::block_gj_counter_t work_counter;
679struct BLC_source_type
682 state_in_block_pointer_lb* start_BLC_source;
685 state_in_block_pointer_lb* end_BLC_source;
688 simple_list<BLC_indicators_lb> block_to_constellation;
689 static_assert(std::is_trivially_destructible_v<simple_list<BLC_indicators_lb>>);
690 BLC_source_type(state_in_block_pointer_lb* new_start,
691 state_in_block_pointer_lb* new_end)
692 : start_BLC_source(new_start),
693 end_BLC_source(new_end),
694 block_to_constellation()
695 { assert(new_start <= new_end);
699 template<
class LTS_TYPE> std::string debug_id
700 (
const bisim_partitioner_gj_lazy_BLC<LTS_TYPE>& partitioner)
const
701 { assert(partitioner.m_states_in_blocks.data()<=start_BLC_source);
702 assert(start_BLC_source<end_BLC_source);
703 assert(end_BLC_source<=partitioner.m_states_in_blocks.data_end());
704 std::string result(
"BLC source [");
705 result += std::to_string(std::distance<
const state_in_block_pointer_lb*>
706 (partitioner.m_states_in_blocks.data(), start_BLC_source));
708 result += std::to_string(std::distance<
const state_in_block_pointer_lb*>
709 (partitioner.m_states_in_blocks.data(), end_BLC_source));
711 if (start_BLC_source->ref_state->block !=
712 std::prev(end_BLC_source)->ref_state->block)
714 result +=
" containing";
715 const state_in_block_pointer_lb* it = start_BLC_source;
718 result += it->ref_state->block->debug_id(partitioner);
719 it = it->ref_state->block->end_states;
720 }
while (it < end_BLC_source);
732struct block_that_needs_refinement_type
748 std::array<state_in_block_pointer_lb*, 4> start_bottom_states;
753 std::array<std::vector<state_in_block_pointer_lb>, 3> potential_non_bottom_states;
754 std::vector<state_in_block_pointer_lb> potential_non_bottom_states_HitSmall;
762 BLC_indicators_lb* large_splitter;
764 #ifdef MORE_STATISTICS
768 fixed_vector<state_type_gj_lb>::iterator transition_count_sample_state;
776 block_that_needs_refinement_type(block_type_lb& B, BLC_indicators_lb* a_large_splitter =
nullptr)
777 : start_bottom_states{B.start_bottom_states, B.start_bottom_states, B.sta.rt_non_bottom_states, B.sta.rt_non_bottom_states},
778 potential_non_bottom_states(),
779 potential_non_bottom_states_HitSmall(),
780 large_splitter(a_large_splitter)
781#ifdef MORE_STATISTICS
783 transition_count_sample_state(B.start_bottom_states->ref_state)
788 state_index bottom_size(
enum subblocks coroutine)
789 { assert(ReachAlw==coroutine ||
790 AvoidSml==coroutine ||
791 AvoidLrg==coroutine);
792 assert(start_bottom_states[(coroutine)]<=start_bottom_states[(coroutine)+1]);
793 return std::distance(start_bottom_states[coroutine],
794 start_bottom_states[coroutine+1]);
797 template<
class LTS_TYPE>
798 std::string debug_id(
const bisim_partitioner_gj_lazy_BLC<LTS_TYPE>& partitioner)
const
800 std::string result(
"refinement info for ");
801 result += start_bottom_states[0]->ref_state->block->debug_id(partitioner);
803 const state_in_block_pointer_lb* bott_it = start_bottom_states[0];
804 assert(bott_it <= start_bottom_states[1]);
805 if (bott_it < start_bottom_states[1]) {
806 result +=
" ReachAlw = { ";
808 result += bott_it->ref_state->debug_id_short(partitioner); result +=
" ";
809 }
while (++bott_it < start_bottom_states[1]);
812 assert(bott_it <= start_bottom_states[2]);
813 if (bott_it < start_bottom_states[2]) {
814 result +=
" AvoidSml = { ";
816 result += bott_it->ref_state->debug_id_short(partitioner); result +=
" ";
817 }
while (++bott_it < start_bottom_states[2]);
820 assert(bott_it <= start_bottom_states[3]);
821 if (bott_it < start_bottom_states[3]) {
822 result +=
" AvoidLrg = { ";
824 result += bott_it->ref_state->debug_id_short(partitioner); result +=
" ";
825 }
while (++bott_it < start_bottom_states[3]);
828 if (!potential_non_bottom_states[0].empty()) {
829 result +=
" pot-ReachAlw = { ";
830 std::vector<state_in_block_pointer_lb>::const_iterator it = potential_non_bottom_states[0].begin();
832 result += it->ref_state->debug_id_short(partitioner); result +=
" ";
833 }
while (++it != potential_non_bottom_states[0].end());
836 if (!potential_non_bottom_states[1].empty()) {
837 result +=
" pot-AvoidSml = { ";
838 std::vector<state_in_block_pointer_lb>::const_iterator it = potential_non_bottom_states[1].begin();
840 result += it->ref_state->debug_id_short(partitioner); result +=
" ";
841 }
while (++it != potential_non_bottom_states[1].end());
844 if (!potential_non_bottom_states[2].empty()) {
845 result +=
" pot-AvoidLrg = { ";
846 std::vector<state_in_block_pointer_lb>::const_iterator it = potential_non_bottom_states[2].begin();
848 result += it->ref_state->debug_id_short(partitioner); result +=
" ";
849 }
while (++it != potential_non_bottom_states[2].end());
852 if (!potential_non_bottom_states_HitSmall.empty()) {
853 result +=
" HitSmall = { ";
854 std::vector<state_in_block_pointer_lb>::const_iterator it = potential_non_bottom_states_HitSmall.begin();
856 result += it->ref_state->debug_id_short(partitioner); result +=
" ";
857 }
while (++it != potential_non_bottom_states_HitSmall.end());
860 result +=
" LargeSp = ";
861 if (
nullptr == large_splitter) { result +=
"nullptr"; }
862 else { result += large_splitter->debug_id(partitioner); }
869struct constellation_type_lb
872 state_in_block_pointer_lb* start_const_states;
875 state_in_block_pointer_lb* end_const_states;
877 constellation_type_lb(state_in_block_pointer_lb*
const new_start,
878 state_in_block_pointer_lb*
const new_end)
879 : start_const_states(new_start),
880 end_const_states(new_end)
884 template<
class LTS_TYPE>
885 std::string debug_id(
const bisim_partitioner_gj_lazy_BLC<LTS_TYPE>& partitioner)
const
886 { assert(partitioner.m_states_in_blocks.data()<=start_const_states);
887 assert(start_const_states<end_const_states);
888 assert(end_const_states<=partitioner.m_states_in_blocks.data_end());
889 return "constellation ["+std::to_string
890 (std::distance<
const state_in_block_pointer_lb*>
891 (partitioner.m_states_in_blocks.data(), start_const_states))+
","+
893 (std::distance<
const state_in_block_pointer_lb*>
894 (partitioner.m_states_in_blocks.data(), end_const_states))+
")";
903
904
907using namespace mcrl2::
lts::
detail::bisimulation_gj_lazy_BLC;
911template <
class LTS_TYPE>
912class bisim_partitioner_gj_lazy_BLC
916 using set_of_states_type = std::unordered_set<state_index>;
917 using set_of_transitions_type = std::unordered_set<transition_index>;
926 fixed_vector<state_type_gj_lb> m_states;
933 fixed_vector<outgoing_transition_type_lb> m_outgoing_transitions;
938 fixed_vector<transition_type_lb> m_transitions;
941 fixed_vector<state_in_block_pointer_lb> m_states_in_blocks;
944 state_index no_of_blocks = 1;
947 state_index no_of_constellations = 1;
950 fixed_vector<transition_index> m_BLC_transitions;
953 std::vector<block_type_lb*> m_blocks_with_new_bottom_states;
954 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
955 block_type_lb* m_singleton_block_with_new_bottom_states_for_debug =
959 std::vector<constellation_type_lb*> m_non_trivial_constellations;
967 std::vector<std::pair<BLC_source_type&, simple_list<BLC_indicators_lb>::iterator> >
968 m_BLC_indicators_to_be_deleted;
971 const bool m_branching;
978 const bool m_preserve_divergence;
983 static typename LTS_TYPE::labels_size_type m_aut_apply_hidden_label_map
984 (
typename LTS_TYPE::labels_size_type l)
991 bool is_inert_during_init_if_branching(
const transition& t)
const
992 { assert(m_branching);
993 return m_aut.is_tau(m_aut_apply_hidden_label_map(t.label())) &&
994 (!m_preserve_divergence || t.from() != t.to());
999 bool is_inert_during_init(
const transition& t)
const
1001 return m_branching && is_inert_during_init_if_branching(t);
1007 label_index label_or_divergence(
const transition& t,
1008 const label_index divergent_label=-2
1011 label_index result = m_aut_apply_hidden_label_map(t.label()); assert(divergent_label!=result); assert(null_action!=divergent_label);
1012 if (m_preserve_divergence && ( assert(m_branching),
1013 t.from() == t.to()) &&
1014 m_aut.is_tau(result))
1016 return divergent_label;
1038 void check_transitions(
const bool initialisation,
1039 const bool check_temporary_complexity_counters,
1040 const bool check_block_to_constellation =
true)
const
1042 for(transition_index ti=0; ti<m_transitions.size(); ++ti)
1044 const BLC_list_const_iterator btc_ti=
1045 m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions;
1046 assert(*btc_ti==ti);
1048 const transition& t=m_aut.get_transitions()[ti];
1049 assert(&*m_states[t.to()].start_incoming_transitions<=&t);
1050 if (t.to()+1!=m_aut.num_states())
1052 assert(&t<=&*std::prev(m_states[t.to()+1].start_incoming_transitions));
1056 assert(&t<=&m_aut.get_transitions().back());
1059 assert(m_states[t.from()].start_outgoing_transitions<=
1060 m_transitions[ti].ref_outgoing_transitions);
1061 if (t.from()+1==m_aut.num_states())
1063 assert(m_transitions[ti].ref_outgoing_transitions<
1064 m_outgoing_transitions.end());
1068 assert(m_transitions[ti].ref_outgoing_transitions<
1069 m_states[t.from() + 1].start_outgoing_transitions);
1072 assert(m_transitions[ti].
1073 transitions_per_block_to_constellation->start_same_BLC<=btc_ti);
1074 assert(btc_ti<m_transitions[ti].
1075 transitions_per_block_to_constellation->end_same_BLC);
1077 if (!check_block_to_constellation)
1082 const bisimulation_gj_lazy_BLC::block_type_lb& b=*m_states[t.from()].block;
1083 const BLC_source_type& blc_src=*b.block_BLC_source;
1085 const label_index t_label = label_or_divergence(t);
1087 for(
const BLC_indicators_lb& blc: blc_src.block_to_constellation)
1089 if (!blc.is_stable())
1091 assert(blc.start_same_BLC<=blc.start_marked_BLC);
1092 assert(blc.start_marked_BLC<=blc.end_same_BLC);
1094 assert(blc.start_same_BLC<blc.end_same_BLC);
1095 transition& first_t = m_aut.get_transitions()[*blc.start_same_BLC];
1096 assert(&blc_src == m_states[first_t.from()].block->block_BLC_source);
1097 if (t_label == label_or_divergence(first_t) &&
1098 m_states[first_t.to()].block->constellation ==
1099 m_states[t.to()].block->constellation)
1101 assert(!found); assert(blc.start_same_BLC <= btc_ti);
1102 assert(btc_ti<blc.end_same_BLC);
1103 assert(&blc == &*m_transitions[ti].transitions_per_block_to_constellation);
1108 if (check_temporary_complexity_counters)
1110 block_type_lb& targetb = *m_states[t.to()].block;
1111 const unsigned max_sourceB = check_complexity::log_n-
1112 check_complexity::ilog2(number_of_states_in_block(b));
1113 const unsigned max_targetC = check_complexity::log_n-
1114 check_complexity::ilog2(number_of_states_in_constellation
1115 (*targetb.constellation));
1116 const unsigned max_targetB = check_complexity::log_n-
1117 check_complexity::ilog2(number_of_states_in_block(targetb));
1119 no_temporary_work(max_sourceB, max_targetC, max_targetB,
1121 0==m_states[t.from()].no_of_outgoing_block_inert_transitions),
1134 bool check_data_structures(
const std::string& tag,
const bool check_temporary_complexity_counters=
true)
const
1136 mCRL2log(log::debug) <<
"Check data structures: " << tag <<
".\n";
1137 assert(m_states.size()==m_aut.num_states());
1138 assert(m_states_in_blocks.size()==m_aut.num_states());
1139 assert(m_transitions.size()==m_aut.num_transitions());
1140 assert(m_outgoing_transitions.size()==m_aut.num_transitions());
1141 assert(m_BLC_transitions.size()==m_aut.num_transitions());
1144 for (fixed_vector<state_type_gj_lb>::iterator si=
1145 const_cast<fixed_vector<state_type_gj_lb>&>(m_states).begin();
1146 si<m_states.cend(); si++)
1148 const state_type_gj_lb& s=*si;
1150 assert(s.counter==undefined);
1153 assert(std::find(s.block->start_bottom_states, s.block->end_states,
1154 state_in_block_pointer_lb(si))!=s.block->end_states);
1156 assert(s.ref_states_in_blocks->ref_state==si);
1160 bool maybe_tau=
true;
1161 const std::vector<transition>::const_iterator end_it1=
1162 std::next(si)>=m_states.end() ? m_aut.get_transitions().end()
1163 : std::next(si)->start_incoming_transitions;
1164 for (std::vector<transition>::const_iterator
1165 it=s.start_incoming_transitions; it!=end_it1; ++it)
1167 const transition& t=*it;
1168 if (m_aut.is_tau(m_aut_apply_hidden_label_map(t.label())))
1185 std::unordered_set<std::pair<label_index,
const constellation_type_lb*> >
1186 constellations_seen;
1190 const outgoing_transitions_const_it_lb end_it2=
1191 std::next(si)>=m_states.end() ? m_outgoing_transitions.cend()
1192 : std::next(si)->start_outgoing_transitions;
1193 for(outgoing_transitions_const_it_lb it=s.start_outgoing_transitions;
1196 const transition& t=m_aut.get_transitions()[*it->ref_BLC_transitions];
1197 assert(m_states.cbegin()+t.from()==si);
1198 assert(m_transitions[*it->ref_BLC_transitions].
1199 ref_outgoing_transitions==it);
1200 if (it->start_same_saC>it) {
1201 assert(it->start_same_saC<m_outgoing_transitions.end());
1202 assert((it+1)->start_same_saC==it->start_same_saC ||
1203 (it+1)->start_same_saC<=it);
1205 assert(it+1==m_outgoing_transitions.end() ||
1206 (it+1)->start_same_saC>it);
1208 const label_index t_label = label_or_divergence(t);
1210 for(outgoing_transitions_const_it_lb itt=it->start_same_saC;
1211 itt<it->start_same_saC->start_same_saC; ++itt)
1213 const transition& t1=
1214 m_aut.get_transitions()[*itt->ref_BLC_transitions];
1215 assert(m_states.cbegin()+t1.from()==si);
1216 assert(label_or_divergence(t1) == t_label);
1217 assert(m_states[t.to()].block->constellation==
1218 m_states[t1.to()].block->constellation);
1221 const label_index label = label_or_divergence(t);
1224 const constellation_type_lb& t_to_constellation=
1225 *m_states[t.to()].block->constellation;
1226 if (constellations_seen.count(std::pair(label, &t_to_constellation))>0)
1228 assert(it!=s.start_outgoing_transitions);
1229 const transition& old_t=m_aut.get_transitions()
1230 [*std::prev(it)->ref_BLC_transitions];
1231 assert(label_or_divergence(old_t)==label);
1232 assert(&t_to_constellation==
1233 m_states[old_t.to()].block->constellation);
1237 if (m_branching && m_aut.is_tau(label))
1245 constellations_seen.emplace(label, &t_to_constellation);
1250 check_transitions(
false, check_temporary_complexity_counters);
1254 set_of_transitions_type all_transitions;
1255 #ifdef MORE_STATISTICS
1256 transition_index actual_no_of_non_block_inert_sample_transitions=0;
1258 for (
const state_in_block_pointer_lb* si=m_states_in_blocks.data();
1259 m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
1261 const block_type_lb& b=*si->ref_state->block;
1262 const constellation_type_lb& c=*b.constellation;
1263 assert(m_states_in_blocks.data()<=c.start_const_states);
1264 assert(c.start_const_states<=b.start_bottom_states);
1265 assert(b.start_bottom_states<b.sta.rt_non_bottom_states);
1266 assert(b.sta.rt_non_bottom_states<=b.end_states);
1267 assert(b.end_states<=c.end_const_states);
1268 assert(c.end_const_states<=m_states_in_blocks.data_end());
1269 assert(b.block_BLC_source->start_BLC_source<=b.start_bottom_states);
1270 assert(b.end_states<=b.block_BLC_source->end_BLC_source);
1271 if (null_state != b.refinement_info) {
1272 assert(b.refinement_info < blocks_that_need_refinement.size());
1273 assert(blocks_that_need_refinement[b.refinement_info].
1274 start_bottom_states[0] == b.start_bottom_states);
1275 assert(blocks_that_need_refinement[b.refinement_info].
1276 start_bottom_states[3] == b.sta.rt_non_bottom_states);
1278 #ifdef MORE_STATISTICS
1279 fixed_vector<state_type_gj_lb>::iterator sample_state =
1280 null_state == b.refinement_info
1281 ? b.start_bottom_states->ref_state
1282 : blocks_that_need_refinement[b.refinement_info].
1283 transition_count_sample_state;
1284 assert(0 == sample_state->no_of_outgoing_block_inert_transitions);
1285 outgoing_transitions_const_it_lb
const out_it_end =
1286 std::next(sample_state)==m_states.end()
1287 ? m_outgoing_transitions.end()
1288 : std::next(sample_state)->start_outgoing_transitions;
1289 for (outgoing_transitions_const_it_lb out_it =
1290 sample_state->start_outgoing_transitions; out_it < out_it_end;
1291 assert(out_it <= out_it->start_same_saC),
1292 out_it = std::next(out_it->start_same_saC))
1293 { ++actual_no_of_non_block_inert_sample_transitions; }
1295 unsigned char const max_B=check_complexity::log_n-
1296 check_complexity::ilog2(number_of_states_in_block(b));
1297 unsigned char const max_C=check_complexity::log_n-check_complexity::
1298 ilog2(number_of_states_in_constellation(*b.constellation));
1299 for (
const state_in_block_pointer_lb*
1300 is=b.start_bottom_states; is!=b.sta.rt_non_bottom_states; ++is)
1302 assert(is->ref_state->block==&b);
1303 assert(is->ref_state->no_of_outgoing_block_inert_transitions==0);
1304 if (check_temporary_complexity_counters)
1309 for (
const state_in_block_pointer_lb*
1310 is=b.sta.rt_non_bottom_states; is!=b.end_states; ++is)
1312 assert(is->ref_state->block==&b);
1313 assert(is->ref_state->no_of_outgoing_block_inert_transitions>0);
1322 const BLC_source_type& blc_src = *b.block_BLC_source;
1323 if (blc_src.start_BLC_source == b.start_bottom_states)
1325 assert(blc_src.block_to_constellation.check_linked_list());
1326 for (simple_list<BLC_indicators_lb>::const_iterator
1327 ind=blc_src.block_to_constellation.begin();
1328 ind!=blc_src.block_to_constellation.end(); ++ind)
1330 assert(ind->start_same_BLC<ind->end_same_BLC);
1331 const transition& first_transition=
1332 m_aut.get_transitions()[*(ind->start_same_BLC)];
1333 const label_index first_transition_label=
1334 label_or_divergence(first_transition);
1335 for(BLC_list_const_iterator i=ind->start_same_BLC;
1336 i<ind->end_same_BLC; ++i)
1338 const transition& t=m_aut.get_transitions()[*i];
1339 assert(m_transitions[*i].transitions_per_block_to_constellation==
1341 all_transitions.emplace(*i);
1342 assert(m_states[t.from()].block->block_BLC_source==&blc_src);
1343 assert(m_states[t.to()].block->constellation==
1344 m_states[first_transition.to()].block->constellation);
1345 assert(label_or_divergence(t)==first_transition_label);
1355 if (check_temporary_complexity_counters)
1358 check_complexity::log_n-check_complexity::ilog2
1359 (number_of_states_in_constellation(*m_states
1360 [first_transition.to()].block->constellation))), *
this);
1365 assert(all_transitions.size()==m_transitions.size());
1366 #ifdef MORE_STATISTICS
1367 assert(actual_no_of_non_block_inert_sample_transitions==
1368 no_of_non_block_inert_sample_transitions);
1374 const state_in_block_pointer_lb* ci=m_states_in_blocks.data();
1375 assert(m_states_in_blocks.data_end()!=ci);
1378 const constellation_type_lb& c=*ci->ref_state->block->constellation;
1379 assert(c.start_const_states==ci);
1380 const state_in_block_pointer_lb* bi=ci;
1381 ci=c.end_const_states;
1385 const block_type_lb& b=*bi->ref_state->block;
1386 assert(b.start_bottom_states==bi);
1387 assert(b.constellation==&c);
1392 while (ci<m_states_in_blocks.data_end());
1395 const state_in_block_pointer_lb* bsi=m_states_in_blocks.data();
1396 assert(m_states_in_blocks.data_end()!=bsi);
1399 const BLC_source_type& bs=*bsi->ref_state->block->block_BLC_source;
1400 assert(bs.start_BLC_source==bsi);
1402 const state_in_block_pointer_lb* bi=bsi;
1403 bsi=bs.end_BLC_source;
1407 const block_type_lb& b=*bi->ref_state->block;
1408 assert(b.start_bottom_states==bi);
1409 assert(b.block_BLC_source==&bs);
1414 while (bsi<m_states_in_blocks.data_end());
1418 for (
const state_in_block_pointer_lb*
1419 si=m_states_in_blocks.data(); si<m_states_in_blocks.data_end(); ++si)
1421 assert(si==si->ref_state->ref_states_in_blocks);
1425 for(
const block_type_lb* bi: m_blocks_with_new_bottom_states)
1427 assert(bi->contains_new_bottom_states);
1428 assert(1 < number_of_states_in_block(*bi));
1432 for(
const constellation_type_lb* ci: m_non_trivial_constellations)
1435 const block_type_lb& first_bi=*ci->start_const_states->ref_state->block;
1436 const block_type_lb& last_bi=*std::prev(ci->end_const_states)->ref_state->block;
1437 assert(&first_bi != &last_bi);
1469 bool check_stability(
const std::string& tag,
1470 const std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >*
1472 const std::pair<BLC_list_iterator,BLC_list_iterator>* calM_elt=
nullptr,
1473 const constellation_type_lb*
const old_constellation=null_constellation_lb,
1474 const constellation_type_lb*
const new_constellation=null_constellation_lb)
1477 assert((old_constellation==null_constellation_lb &&
1478 new_constellation==null_constellation_lb ) ||
1479 (old_constellation!=null_constellation_lb &&
1480 new_constellation!=null_constellation_lb &&
1481 old_constellation!=new_constellation ));
1482 mCRL2log(log::debug) <<
"Check stability: " << tag <<
".\n";
1484 for (
const state_in_block_pointer_lb* blc_src_it=m_states_in_blocks.data();
1485 m_states_in_blocks.data_end()!=blc_src_it;
1486 blc_src_it=blc_src_it->ref_state->block->block_BLC_source->end_BLC_source)
1488 const BLC_source_type& blc_src=*blc_src_it->ref_state->block->block_BLC_source;
1490 bool previous_stable=
true;
1491 for(simple_list<BLC_indicators_lb>::const_iterator
1492 ind=blc_src.block_to_constellation.begin();
1493 ind!=blc_src.block_to_constellation.end(); ++ind)
1496 assert(m_BLC_transitions.data()<=ind->start_same_BLC);
1497 assert(ind->start_same_BLC<ind->end_same_BLC);
1498 if (!ind->is_stable())
1500 assert(ind->start_same_BLC<=ind->start_marked_BLC);
1501 assert(ind->start_marked_BLC<=ind->end_same_BLC);
1502 previous_stable =
false;
1505 { assert(previous_stable); }
1506 assert(ind->end_same_BLC<=m_BLC_transitions.data_end());
1509 const transition&first_t=m_aut.get_transitions()[*ind->start_same_BLC];
1510 const label_index first_t_label=label_or_divergence(first_t);
1511 const constellation_type_lb&
1512 to_constln=*m_states[first_t.to()].block->constellation;
1513 for (BLC_list_const_iterator i=ind->start_same_BLC;
1514 i<ind->end_same_BLC; ++i)
1516 const transition& t=m_aut.get_transitions()[*i];
1517 assert(&blc_src == m_states[t.from()].block->block_BLC_source);
1518 assert(label_or_divergence(t) == first_t_label);
1519 assert(&to_constln == m_states[t.to()].block->constellation);
1522 bool eventual_instability_is_ok =
true;
1523 bool all_blocks_are_singletons =
true;
1524 for (
const state_in_block_pointer_lb* blk_it = blc_src_it;
1525 blk_it != blc_src.end_BLC_source;
1526 blk_it = blk_it->ref_state->block->end_states)
1528 const block_type_lb& b = *blk_it->ref_state->block;
1529 if (1<std::distance(b.start_bottom_states, b.end_states))
1530 { all_blocks_are_singletons =
false; }
1531 if (!is_inert_during_init(first_t) || b.constellation != &to_constln)
1535 set_of_states_type all_source_bottom_states;
1536 bool has_transitions =
false;
1537 for (BLC_list_const_iterator i=ind->start_same_BLC;
1538 i<ind->end_same_BLC; ++i)
1540 const transition& t = m_aut.get_transitions()[*i];
1541 const state_type_gj_lb& src = m_states[t.from()];
1542 if (&b != src.block)
1546 has_transitions =
true;
1547 if (src.ref_states_in_blocks < b.sta.rt_non_bottom_states) {
1548 assert(b.start_bottom_states <= src.ref_states_in_blocks);
1549 assert(0 == src.no_of_outgoing_block_inert_transitions);
1550 all_source_bottom_states.emplace(t.from());
1552 assert(src.ref_states_in_blocks <= b.end_states);
1553 assert(0 != src.no_of_outgoing_block_inert_transitions);
1556 assert(all_source_bottom_states.size() <=
static_cast<std::size_t>
1557 (std::distance(b.start_bottom_states,
1558 b.sta.rt_non_bottom_states)));
1559 if (all_source_bottom_states.size() !=
static_cast<std::size_t>
1560 (std::distance(b.start_bottom_states,
1561 b.sta.rt_non_bottom_states)) &&
1566 << std::distance(b.start_bottom_states,
1567 b.sta.rt_non_bottom_states)
1568 << (m_branching ?
" bottom states in "
1570 << b.debug_id(*
this) <<
" have a transition in the "
1571 << ind->debug_id(*
this) <<
": transitions found from states";
1572 for (
const state_index asbc : all_source_bottom_states)
1573 {
mCRL2log(log::debug) <<
' ' << asbc; }
1575 if (b.contains_new_bottom_states)
1577 mCRL2log(log::debug) <<
" This is ok because "
1578 << b.debug_id(*
this) <<
" contains new bottom states.\n";
1581 { eventual_instability_is_ok =
false; }
1586 bool eventual_marking_is_ok =
true;
1587 if (!ind->is_stable())
1590 mCRL2log(log::debug) << ind->debug_id(*
this) <<
" contains "
1591 << std::distance(ind->start_marked_BLC, ind->end_same_BLC)
1592 <<
" marked transitions.\n";
1593 eventual_marking_is_ok =
false;
1595 if (!(eventual_instability_is_ok && eventual_marking_is_ok) &&
nullptr != calM && calM->begin() != calM->end())
1597 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >::const_iterator calM_iter = calM->begin();
1598 if (
nullptr != calM_elt)
1602 assert(calM->end() != calM_iter);
1603 if (calM_iter->first <= calM_elt->first && calM_elt->second <= calM_iter->second)
1609 if (calM_elt->first<=ind->start_same_BLC && ind->end_same_BLC<=calM_elt->second)
1611 mCRL2log(log::debug) <<
" This is ok because the super-BLC set ("
1612 << blc_src.debug_id(*
this) <<
" -" << m_aut.action_label(first_t.label())
1613 <<
"-> " << to_constln.debug_id(*
this)
1614 <<
") is soon going to be a main splitter.\n";
1615 eventual_instability_is_ok =
true;
1616 eventual_marking_is_ok =
true;
1620 if (old_constellation==&to_constln)
1622 const simple_list<BLC_indicators_lb>::const_iterator main_splitter=blc_src.block_to_constellation.next(ind);
1623 if (main_splitter!=blc_src.block_to_constellation.end())
1625 assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
1626 const transition& main_t = m_aut.get_transitions()[*main_splitter->start_same_BLC];
1627 assert(m_states[main_t.from()].block->block_BLC_source == &blc_src);
1628 if (first_t_label==label_or_divergence(main_t) &&
1629 m_states[main_t.to()].block->constellation==
1632 if (calM_elt->first<=main_splitter->start_same_BLC && main_splitter->end_same_BLC<=calM_elt->second)
1634 mCRL2log(log::debug) <<
" This is ok because the BLC set (" << blc_src.debug_id(*
this) <<
" -" << m_aut.action_label(first_t.label()) <<
"-> " << old_constellation->debug_id(*
this) <<
") is soon going to be a co-splitter.\n";
1635 eventual_instability_is_ok =
true;
1636 eventual_marking_is_ok =
true;
1644 for(; !(eventual_instability_is_ok && eventual_marking_is_ok) && calM->end() != calM_iter; ++calM_iter)
1646 if (calM_iter->first<=ind->start_same_BLC && ind->end_same_BLC<=calM_iter->second)
1648 mCRL2log(log::debug) <<
" This is ok because the BLC set ("
1649 << blc_src.debug_id(*
this) <<
" -" << m_aut.action_label(first_t.label())
1650 <<
"-> " << to_constln.debug_id(*
this)
1651 <<
") is going to be a main splitter later.\n";
1652 eventual_instability_is_ok =
true;
1653 eventual_marking_is_ok =
true;
1657 if (old_constellation == &to_constln)
1659 const simple_list<BLC_indicators_lb>::const_iterator main_splitter=blc_src.block_to_constellation.next(ind);
1660 if (main_splitter != blc_src.block_to_constellation.end())
1662 assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
1663 const transition& main_t = m_aut.get_transitions()[*main_splitter->start_same_BLC];
1664 assert(m_states[main_t.from()].block->block_BLC_source == &blc_src);
1665 if(first_t_label == label_or_divergence(main_t) &&
1666 m_states[main_t.to()].block->constellation==
1669 if (calM_iter->first<=main_splitter->start_same_BLC && main_splitter->end_same_BLC<=calM_iter->second)
1671 assert(new_constellation==
1672 m_states[main_t.to()].block->constellation);
1673 mCRL2log(log::debug) <<
" This is ok because the BLC "
1674 "set (" << blc_src.debug_id(*
this) <<
" -"
1675 << m_aut.action_label(first_t.label())
1676 <<
"-> " << old_constellation->debug_id(*
this)
1677 <<
") is going to be a co-splitter later.\n";
1678 eventual_instability_is_ok =
true;
1679 eventual_marking_is_ok =
true;
1687 if (all_blocks_are_singletons)
1689 if (!eventual_marking_is_ok)
1691 mCRL2log(log::debug) <<
" (This is ok because every source block contains only 1 state.)\n";
1692 eventual_marking_is_ok =
true;
1695 assert(eventual_instability_is_ok);
1696 assert(eventual_marking_is_ok);
1699 mCRL2log(log::debug) <<
"Check stability finished: " << tag <<
".\n";
1704 void display_BLC_list(
const BLC_source_type& blc_src)
const
1706 mCRL2log(log::debug) <<
"\n BLC_List\n";
1707 for(
const BLC_indicators_lb& blc_it: blc_src.block_to_constellation)
1709 const transition&first_t=m_aut.get_transitions()[*blc_it.start_same_BLC];
1710 const label_index l=label_or_divergence(first_t, (label_index) -2);
1714 BLC_list_const_iterator>(
1715 m_BLC_transitions.data(),
1716 blc_it.start_same_BLC)
1719 BLC_list_const_iterator>(
1720 m_BLC_transitions.data(),
1721 blc_it.end_same_BLC)
1723 << (std::cmp_equal(-2, l)
1724 ?
"divergent self-loop "
1725 : pp(m_aut.action_label(
1728 <<
"transitions to "
1729 << m_states[first_t.to()]
1730 .block->constellation
1733 for (BLC_list_const_iterator i=blc_it.start_same_BLC; ; ++i)
1735 if (i == blc_it.start_marked_BLC)
1737 mCRL2log(log::debug) <<
" (The BLC set is unstable, and the "
1738 " following transitions are marked.)\n";
1740 if (i>=blc_it.end_same_BLC)
1744 const transition& t=m_aut.get_transitions()[*i];
1745 mCRL2log(log::debug) <<
" " << t.from() <<
" -"
1746 << m_aut.action_label(t.label()) <<
"-> " << t.to();
1747 if (is_inert_during_init(t) &&
1748 m_states[t.from()].block==m_states[t.to()].block)
1750 mCRL2log(log::debug) <<
" (block-inert)";
1752 else if (is_inert_during_init(t) &&
1753 m_states[t.from()].block->constellation==
1754 m_states[t.to()].block->constellation)
1756 mCRL2log(log::debug) <<
" (constellation-inert)";
1761 mCRL2log(log::debug) <<
" BLC_List end\n";
1765 void print_data_structures(
const std::string& header)
const
1767 if (!mCRL2logEnabled(log::debug)) {
return; }
1768 mCRL2log(log::debug) <<
"========= PRINT DATASTRUCTURE: " << header <<
" =======================================\n"
1769 "++++++++++++++++++++ States ++++++++++++++++++++++++++++\n";
1770 for(state_index si=0; si<m_aut.num_states(); ++si)
1772 mCRL2log(log::debug) <<
"State " << si <<
" (" << m_states[si].block->debug_id(*
this) <<
"):\n"
1773 " #Inert outgoing transitions: " << m_states[si].no_of_outgoing_block_inert_transitions <<
"\n"
1775 " Incoming transitions:\n";
1776 std::vector<transition>::const_iterator end=(si+1==m_aut.num_states()?m_aut.get_transitions().end():m_states[si+1].start_incoming_transitions);
1777 for(std::vector<transition>::const_iterator it=m_states[si].start_incoming_transitions; it!=end; ++it)
1779 mCRL2log(log::debug) <<
" " << ptr(*it) <<
"\n";
1782 mCRL2log(log::debug) <<
" Outgoing transitions:\n";
1783 label_index t_label=m_aut.tau_label_index();
1784 const constellation_type_lb* to_constln=null_constellation_lb;
1785 for(outgoing_transitions_const_it_lb it=m_states[si].start_outgoing_transitions;
1786 it!=m_outgoing_transitions.end() &&
1787 (si+1>=m_aut.num_states() || it!=m_states[si+1].start_outgoing_transitions);
1790 const transition& t=m_aut.get_transitions()[*it->ref_BLC_transitions];
1791 bool start_same_saC_valid=
1792 m_outgoing_transitions.cbegin()<=it->start_same_saC &&
1793 it->start_same_saC<m_outgoing_transitions.end();
1794 if (start_same_saC_valid &&
1795 it->start_same_saC->start_same_saC==it &&
1796 it->start_same_saC >= it)
1799 const label_index old_t_label=t_label;
1800 t_label=label_or_divergence(t, (label_index) -2);
1801 to_constln=m_states[t.to()].block->constellation;
1805 << (std::cmp_equal(-2,
1813 <<
"transitions to "
1814 << to_constln->debug_id(
1816 << (m_aut.is_tau(t_label)
1825 mCRL2log(log::debug) <<
" " << ptr(t);
1826 if (start_same_saC_valid)
1828 if (label_or_divergence(t, (label_index) -2)!=t_label)
1830 mCRL2log(log::debug) <<
" -- error: different label";
1832 if (m_states[t.to()].block->constellation!=to_constln)
1834 mCRL2log(log::debug) <<
" -- error: different target " << m_states[t.to()].block->constellation->debug_id(*
this);
1836 if (it->start_same_saC->start_same_saC == it)
1839 if (it->start_same_saC >= it && it > m_outgoing_transitions.cbegin())
1842 const transition& prev_t=m_aut.get_transitions()
1843 [*std::prev(it)->ref_BLC_transitions];
1844 if (prev_t.from()==t.from() &&
1845 label_or_divergence(prev_t)==t_label &&
1846 m_states[prev_t.to()].block->constellation==
1847 m_states[t.to()].block->constellation)
1849 mCRL2log(log::debug) <<
" -- error: not the beginning of a saC-slice";
1852 if (it->start_same_saC <= it &&
1853 std::next(it) < m_outgoing_transitions.end())
1856 const transition& next_t=m_aut.get_transitions()
1857 [*std::next(it)->ref_BLC_transitions];
1858 if (next_t.from()==t.from() &&
1859 label_or_divergence(next_t)==t_label &&
1860 m_states[next_t.to()].block->constellation==
1861 m_states[t.to()].block->constellation)
1863 mCRL2log(log::debug) <<
" -- error: not the end of a saC-slice";
1867 else if (it->start_same_saC > it ? it->start_same_saC->start_same_saC > it : it->start_same_saC->start_same_saC < it)
1869 mCRL2log(log::debug) <<
" -- error: not pointing to its own saC-slice";
1874 mCRL2log(log::debug) <<
" Ref states in blocks: " << std::distance<fixed_vector<state_type_gj_lb>::const_iterator>(m_states.cbegin(), m_states[si].ref_states_in_blocks->ref_state) <<
". Must be " << si <<
".\n";
1875 mCRL2log(log::debug) <<
"---------------------------------------------------\n";
1877 mCRL2log(log::debug) <<
"++++++++++++++++++++ Transitions ++++++++++++++++++++++++++++\n";
1878 for(transition_index ti=0; ti<m_transitions.size(); ++ti)
1880 const transition& t=m_aut.get_transitions()[ti];
1881 mCRL2log(log::debug) <<
"Transition " << ti <<
": " << t.from()
1882 <<
" -" << m_aut.action_label(t.label()) <<
"-> "
1886 mCRL2log(log::debug) <<
"++++++++++++++++++++ Blocks ++++++++++++++++++++++++++++\n";
1887 for (
const state_in_block_pointer_lb* si=m_states_in_blocks.data();
1888 m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
1890 block_type_lb& bi=*si->ref_state->block;
1891 mCRL2log(log::debug) <<
" " << bi.debug_id(*
this)
1892 <<
" (" << bi.constellation->debug_id(*
this) <<
')'
1893 <<
":\n " << std::distance(bi.start_bottom_states,
1894 bi.sta.rt_non_bottom_states)
1895 << (m_branching ?
" Bottom state" :
" State")
1896 << (1==std::distance(bi.start_bottom_states,
1897 bi.sta.rt_non_bottom_states) ?
": " :
"s: ");
1898 for (
const state_in_block_pointer_lb*
1899 sit=bi.start_bottom_states; sit!=bi.sta.rt_non_bottom_states; ++sit)
1901 mCRL2log(log::debug) << sit->ref_state->debug_id_short(*
this) <<
" ";
1905 mCRL2log(log::debug) <<
"\n " << std::distance
1906 (bi.sta.rt_non_bottom_states, bi.end_states)
1907 <<
" Non-bottom state" << (1==std::distance
1908 (bi.sta.rt_non_bottom_states, bi.end_states)
1910 for (
const state_in_block_pointer_lb*
1911 sit=bi.sta.rt_non_bottom_states; sit!=bi.end_states; ++sit)
1913 mCRL2log(log::debug) << sit->ref_state->debug_id_short(*
this) <<
" ";
1918 assert(bi.sta.rt_non_bottom_states==bi.end_states);
1923 mCRL2log(log::debug) <<
"++++++++++++++++++++ Constellations ++++++++++++++++++++++++++++\n";
1924 for (
const state_in_block_pointer_lb* si=m_states_in_blocks.data();
1925 m_states_in_blocks.data_end()!=si;
1926 si=si->ref_state->block->constellation->end_const_states)
1928 const constellation_type_lb& ci=*si->ref_state->block->constellation;
1929 mCRL2log(log::debug) <<
" " << ci.debug_id(*
this) <<
":\n";
1930 mCRL2log(log::debug) <<
" Blocks in constellation:";
1931 for (
const state_in_block_pointer_lb*
1932 constln_it=ci.start_const_states;
1933 constln_it<ci.end_const_states; )
1935 const block_type_lb& bi=*constln_it->ref_state->block;
1936 mCRL2log(log::debug) <<
" " << bi.debug_id(*
this);
1937 constln_it = bi.end_states;
1941 mCRL2log(log::debug) <<
"Non-trivial constellations:";
1942 for (
const constellation_type_lb* ci: m_non_trivial_constellations)
1944 mCRL2log(log::debug) <<
" " << ci->debug_id(*
this);
1946 mCRL2log(log::debug) <<
"\n++++++++++++++++++++ BLC sources ++++++++++++++++++++++++++++\n";
1947 for (
const state_in_block_pointer_lb* si=m_states_in_blocks.data();
1948 m_states_in_blocks.data_end()!=si;
1949 si=si->ref_state->block->block_BLC_source->end_BLC_source)
1951 const BLC_source_type& blc_src=*si->ref_state->block->block_BLC_source;
1952 mCRL2log(log::debug) <<
" " << blc_src.debug_id(*
this) <<
'\n';
1953 display_BLC_list(blc_src);
1957 "\n++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n"
1958 "Outgoing transitions:\n";
1960 for (outgoing_transitions_const_it_lb pi = m_outgoing_transitions.cbegin();
1961 pi < m_outgoing_transitions.cend(); ++pi)
1963 const transition& t=m_aut.get_transitions()[*pi->ref_BLC_transitions];
1964 mCRL2log(log::debug) <<
" " << t.from() <<
" -"
1965 << m_aut.action_label(t.label()) <<
"-> " << t.to();
1966 if (m_outgoing_transitions.cbegin()<=pi->start_same_saC &&
1967 pi->start_same_saC<m_outgoing_transitions.end())
1969 const transition& t1=m_aut.get_transitions()
1970 [*pi->start_same_saC->ref_BLC_transitions];
1971 mCRL2log(log::debug) <<
" \t(same saC: " << t1.from() <<
" -" << m_aut.action_label(t1.label()) <<
"-> " << t1.to();
1972 const label_index t_label = label_or_divergence(t);
1973 if (pi->start_same_saC->start_same_saC == pi)
1976 if (pi->start_same_saC >= pi && pi > m_outgoing_transitions.cbegin())
1979 const transition& prev_t=m_aut.get_transitions()
1980 [*std::prev(pi)->ref_BLC_transitions];
1981 if (prev_t.from()==t.from() &&
1982 label_or_divergence(prev_t)==t_label &&
1983 m_states[prev_t.to()].block->constellation==
1984 m_states[t.to()].block->constellation)
1986 mCRL2log(log::debug) <<
" -- error: not the beginning of a saC-slice";
1989 if (pi->start_same_saC <= pi && std::next(pi) < m_outgoing_transitions.end())
1992 const transition& next_t=m_aut.get_transitions()
1993 [*std::next(pi)->ref_BLC_transitions];
1994 if (next_t.from()==t.from() &&
1995 label_or_divergence(next_t)==t_label &&
1996 m_states[next_t.to()].block->constellation==
1997 m_states[t.to()].block->constellation)
1999 mCRL2log(log::debug) <<
" -- error: not the end of a saC-slice";
2003 else if (pi->start_same_saC > pi ? pi->start_same_saC->start_same_saC > pi : pi->start_same_saC->start_same_saC < pi)
2005 mCRL2log(log::debug) <<
" -- error: not in its own saC-slice";
2011 mCRL2log(log::debug) <<
"++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n"
2012 "New bottom blocks to be investigated:";
2014 for(
const block_type_lb* bi: m_blocks_with_new_bottom_states)
2016 mCRL2log(log::debug) <<
" " << bi->debug_id(*
this) <<
'\n';
2019 mCRL2log(log::debug) <<
"\n========= END PRINT DATASTRUCTURE: " << header <<
" =======================================\n";
2027 std::size_t num_eq_classes()
const
2029 return no_of_blocks;
2040 state_index get_eq_class(
const state_index si)
const
2041 { assert(si<m_states.size());
2042 return m_states[si].block->sta.te_in_reduced_LTS;
2056 void finalize_minimized_LTS()
2063 state_index block_number=0;
2064 for (state_in_block_pointer_lb*
2065 si=m_states_in_blocks.data(); m_states_in_blocks.data_end()!=si;
2066 si=si->ref_state->block->end_states)
2068 block_type_lb& bi=*si->ref_state->block;
2070 new (&bi.sta.te_in_reduced_LTS) state_index(block_number);
2081 std::remove_reference_t<
decltype(m_aut.get_transitions())> T;
2082 const state_in_block_pointer_lb* blk_it = m_states_in_blocks.data(); assert(blk_it < m_states_in_blocks.data_end());
2085 const block_type_lb &blk = *blk_it->ref_state->block; assert(blk.start_bottom_states == blk_it);
2086 const fixed_vector<state_type_gj_lb>::const_iterator si =
2087 blk_it->ref_state; assert(0==si->no_of_outgoing_block_inert_transitions);
2088 const state_index new_from =
2089 get_eq_class(std::distance(m_states.cbegin(), si));
2090 assert(blk.constellation->start_const_states == blk_it);
2092 outgoing_transitions_const_it_lb out_it =
2093 si->start_outgoing_transitions; assert(blk_it < blk.end_states);
2094 outgoing_transitions_const_it_lb
const out_it_end =
2095 std::next(si)==m_states.end()
2096 ? m_outgoing_transitions.end()
2097 : std::next(si)->start_outgoing_transitions;
2098 while (out_it < out_it_end)
2100 const transition& tr =
2101 m_aut.get_transitions()[*out_it->ref_BLC_transitions]; assert(std::distance(m_states.cbegin(), si) == tr.from());
2102 T.emplace_back(new_from, tr.label(), get_eq_class(tr.to())); assert(out_it <= out_it->start_same_saC);
2103 out_it = std::next(out_it->start_same_saC);
2105 blk_it = blk.end_states; assert(blk_it == blk.constellation->end_const_states);
2107 while (blk_it < m_states_in_blocks.data_end()); assert(blk_it == m_states_in_blocks.data_end());
2108 m_aut.get_transitions()=std::move(T);
2114 if (m_aut.has_state_info())
2117 std::remove_reference_t<
decltype(m_aut.state_labels())>
2118 new_labels(num_eq_classes());
2120 for(std::size_t i=0; i<m_aut.num_states(); ++i)
2124 const state_index new_index(get_eq_class(i));
2125 new_labels[new_index]=new_labels[new_index]+m_aut.state_label(i);
2128 m_aut.set_num_states(num_eq_classes(),
false); assert(0==m_aut.num_state_labels());
2129 m_aut.state_labels()=std::move(new_labels);
2133 m_aut.set_num_states(num_eq_classes(),
false);
2136 m_aut.set_initial_state(get_eq_class(m_aut.initial_state()));
2144 bool in_same_class(state_index
const s, state_index
const t)
const
2146 return get_eq_class(s) == get_eq_class(t);
2150 std::string ptr(
const transition& t)
const
2152 return std::to_string(t.from())+
" -"+pp(m_aut.action_label(t.label()))+
2153 "-> "+std::to_string(t.to());
2161 state_index number_of_states_in_block(
const block_type_lb& B)
const
2162 { assert(B.start_bottom_states<B.end_states);
2163 return std::distance(B.start_bottom_states, B.end_states);
2167 state_index number_of_states_in_constellation(
const constellation_type_lb& C)
const
2168 { assert(C.start_const_states<C.end_const_states);
2169 return std::distance(C.start_const_states, C.end_const_states);
2173 void swap_states_in_states_in_block_never_equal(
2174 state_in_block_pointer_lb* pos1, state_in_block_pointer_lb* pos2)
2175 { assert(m_states_in_blocks.data()<=pos1);
2176 std::swap(*pos1,*pos2); assert(pos1<m_states_in_blocks.data_end());
2177 pos1->ref_state->ref_states_in_blocks=pos1; assert(m_states_in_blocks.data()<=pos2);
2178 pos2->ref_state->ref_states_in_blocks=pos2; assert(pos2<m_states_in_blocks.data_end()); assert(pos1!=pos2);
2182 void swap_states_in_states_in_block(
2183 state_in_block_pointer_lb* pos1, state_in_block_pointer_lb* pos2)
2187 swap_states_in_states_in_block_never_equal(pos1, pos2);
2198 void multiple_swap_states_in_states_in_block(
2199 state_in_block_pointer_lb* pos1,
2200 state_in_block_pointer_lb* pos2,
2202 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2203 ,
const state_in_block_pointer_lb* assign_work_to,
2204 unsigned char const max_B,
2205 enum check_complexity::counter_type
const ctr=check_complexity::
2206 multiple_swap_states_in_block_swap_state_in_small_block
2209 { assert(count<m_aut.num_states()); assert(m_states_in_blocks.data()<=pos1);
2210 assert(pos1<pos2); assert(pos2<=m_states_in_blocks.data_end()-count);
2212 std::make_signed_t<state_index> overlap=std::distance(pos2,pos1)+
static_cast<std::make_signed_t<state_index>>(count);
2216 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2220 if (pos2==assign_work_to) {
2221 assign_work_to+=overlap;
2222 }
else { assert(assign_work_to+count<=pos2+overlap ||
2223 pos2+overlap+count<=assign_work_to); }
2227 } assert(0 < count);
2228 state_in_block_pointer_lb temp=*pos1;
2230 {
mCRL2complexity(assign_work_to->ref_state, add_work(ctr, max_B), *
this);
2231 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2235 pos1->ref_state->ref_states_in_blocks=pos1;
2238 pos2->ref_state->ref_states_in_blocks=pos2;
2242 pos1->ref_state->ref_states_in_blocks=pos1;
2244 pos2->ref_state->ref_states_in_blocks=pos2;
2246 for (fixed_vector<state_type_gj_lb>::const_iterator
2247 si=m_states.cbegin(); si<m_states.cend(); ++si)
2249 assert(si==si->ref_states_in_blocks->ref_state);
2257 void mark_BLC_transition(
const outgoing_transitions_it_lb out_pos)
2259 BLC_list_iterator old_pos = out_pos->ref_BLC_transitions;
2260 BLC_indicators_lb& ind =
2261 *m_transitions[*old_pos].transitions_per_block_to_constellation; assert(ind.start_same_BLC<=old_pos);
2262 assert(old_pos<m_BLC_transitions.data_end());
2263 assert(old_pos<ind.end_same_BLC); assert(!ind.is_stable());
2264 if (old_pos < ind.start_marked_BLC)
2266 assert(ind.start_same_BLC<ind.start_marked_BLC);
2267 BLC_list_iterator new_pos = std::prev(ind.start_marked_BLC); assert(ind.start_same_BLC<=new_pos); assert(new_pos<ind.end_same_BLC);
2268 assert(new_pos<m_BLC_transitions.data_end());
2269 if (old_pos < new_pos)
2271 std::swap(*old_pos, *new_pos);
2272 m_transitions[*old_pos].ref_outgoing_transitions->
2273 ref_BLC_transitions = old_pos; assert(out_pos==m_transitions[*new_pos].ref_outgoing_transitions);
2274 out_pos->ref_BLC_transitions = new_pos;
2276 ind.start_marked_BLC = new_pos;
2280 for (BLC_list_const_iterator it=m_BLC_transitions.data();
2281 it<m_BLC_transitions.data_end(); ++it)
2283 assert(m_transitions[*it].ref_outgoing_transitions->ref_BLC_transitions==
2285 assert(m_transitions[*it].transitions_per_block_to_constellation->
2286 start_same_BLC<=it);
2288 m_transitions[*it].transitions_per_block_to_constellation->end_same_BLC);
2294 void swap_three_iterators_and_update_m_transitions(
2295 BLC_list_iterator i1,
2296 BLC_list_iterator i2,
2297 BLC_list_iterator i3)
2298 { assert(i3<=i2); assert(i2<=i1);
2303 if ((i1==i2)||(i2==i3))
2306 m_transitions[*i1].ref_outgoing_transitions->ref_BLC_transitions = i1;
2307 m_transitions[*i3].ref_outgoing_transitions->ref_BLC_transitions = i3;
2311 transition_index temp = *i1;
2315 m_transitions[*i1].ref_outgoing_transitions->ref_BLC_transitions = i1;
2316 m_transitions[*i2].ref_outgoing_transitions->ref_BLC_transitions = i2;
2317 m_transitions[*i3].ref_outgoing_transitions->ref_BLC_transitions = i3;
2337 bool swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation(
2338 const transition_index ti,
2339 simple_list<BLC_indicators_lb>::iterator new_BLC_block,
2340 simple_list<BLC_indicators_lb>::iterator old_BLC_block)
2341 { assert(new_BLC_block->is_stable());
2346 BLC_list_iterator old_position=
2347 m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions; assert(old_BLC_block->start_same_BLC <= old_position);
2348 assert(old_position<old_BLC_block->end_same_BLC);
2349 assert(new_BLC_block->end_same_BLC==old_BLC_block->start_same_BLC);
2350 assert(m_transitions[ti].transitions_per_block_to_constellation==old_BLC_block);
2351 assert(ti == *old_position); assert(old_BLC_block->is_stable());
2352 if (old_position!=old_BLC_block->start_same_BLC)
2354 std::swap(*old_position,*old_BLC_block->start_same_BLC);
2355 m_transitions[*old_position].ref_outgoing_transitions->
2356 ref_BLC_transitions = old_position;
2357 m_transitions[*old_BLC_block->start_same_BLC].
2358 ref_outgoing_transitions->ref_BLC_transitions =
2359 old_BLC_block->start_same_BLC;
2361 new_BLC_block->end_same_BLC=++old_BLC_block->start_same_BLC;
2362 m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
2363 return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
2382 bool update_the_doubly_linked_list_LBC_new_constellation(
2383 block_type_lb& index_block_B,
2384 const transition& t,
2385 const transition_index ti)
2386 { assert(m_states[t.to()].block==&index_block_B);
2389 block_type_lb& from_block=*m_states[t.from()].block; assert(&m_aut.get_transitions()[ti] == &t);
2390 BLC_source_type& blc_src=*from_block.block_BLC_source;
2391 bool new_block_created =
false; assert(blc_src.block_to_constellation.check_linked_list());
2392 simple_list<BLC_indicators_lb>::iterator this_block_to_constellation=
2393 m_transitions[ti].transitions_per_block_to_constellation; assert(this_block_to_constellation->is_stable());
2396 for (simple_list<BLC_indicators_lb>::const_iterator
2397 i=blc_src.block_to_constellation.begin();
2398 i!=this_block_to_constellation; ++i)
2400 assert(i!=blc_src.block_to_constellation.end());
2402 assert(this_block_to_constellation!=blc_src.block_to_constellation.end());
2403 assert(this_block_to_constellation->start_same_BLC <= m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions);
2405 simple_list<BLC_indicators_lb>::iterator next_block_to_constellation=
2406 blc_src.block_to_constellation.next(this_block_to_constellation);
2407 const transition* first_t;
2408 if (next_block_to_constellation==blc_src.block_to_constellation.end() ||
2409 (first_t=&m_aut.get_transitions()
2410 [*(next_block_to_constellation->start_same_BLC)], assert(m_states[first_t->from()].block->block_BLC_source==&blc_src),
2411 m_states[first_t->to()].block!=&index_block_B) ||
2412 label_or_divergence(*first_t)!=label_or_divergence(t))
2416 new_block_created =
true;
2417 next_block_to_constellation=blc_src.
2418 block_to_constellation.emplace_after(this_block_to_constellation,
2419 this_block_to_constellation->start_same_BLC,
2420 this_block_to_constellation->start_same_BLC,
true);
2421 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2422 next_block_to_constellation->work_counter=
2423 this_block_to_constellation->work_counter;
2427 if (swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation(ti,
2428 next_block_to_constellation, this_block_to_constellation))
2430 blc_src.block_to_constellation.erase(this_block_to_constellation);
2434 return new_block_created;
2452 bool swap_in_the_doubly_linked_list_LBC_in_blocks_new_block(
2453 const transition_index ti,
2454 simple_list<BLC_indicators_lb>::iterator new_BLC_block,
2455 simple_list<BLC_indicators_lb>::iterator old_BLC_block,
2456 const bool mark_all_transitions_in_instable_BLC_sets =
false)
2457 { assert(new_BLC_block->end_same_BLC==old_BLC_block->start_same_BLC);
2458 assert(new_BLC_block->start_same_BLC<=new_BLC_block->end_same_BLC);
2459 BLC_list_iterator old_position =
2460 m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions; assert(old_BLC_block->start_same_BLC<=old_position);
2461 assert(old_position<old_BLC_block->end_same_BLC); assert(ti==*old_position);
2462 assert(m_transitions[ti].transitions_per_block_to_constellation==
2464 if (old_BLC_block->is_stable() ||
2465 (mark_all_transitions_in_instable_BLC_sets && ( assert(new_BLC_block->start_same_BLC==new_BLC_block->start_marked_BLC),
2466 old_position<old_BLC_block->start_marked_BLC)))
2471 if (old_position!=old_BLC_block->start_same_BLC)
2473 std::swap(*old_position, *old_BLC_block->start_same_BLC);
2474 m_transitions[*old_position].ref_outgoing_transitions->
2475 ref_BLC_transitions=old_position;
2476 m_transitions[*old_BLC_block->start_same_BLC].
2477 ref_outgoing_transitions->ref_BLC_transitions=
2478 old_BLC_block->start_same_BLC;
2482 { assert(!old_BLC_block->is_stable()); assert(!new_BLC_block->is_stable());
2483 if (!mark_all_transitions_in_instable_BLC_sets &&
2484 old_position<old_BLC_block->start_marked_BLC)
2485 { assert(old_BLC_block->start_marked_BLC<=old_BLC_block->end_same_BLC);
2487 swap_three_iterators_and_update_m_transitions(old_position,
2488 old_BLC_block->start_same_BLC, new_BLC_block->start_marked_BLC);
2489 ++new_BLC_block->start_marked_BLC;
2492 { assert(old_BLC_block->start_same_BLC<=old_BLC_block->start_marked_BLC);
2494 swap_three_iterators_and_update_m_transitions(old_position,
2495 old_BLC_block->start_marked_BLC, old_BLC_block->start_same_BLC);
2496 ++old_BLC_block->start_marked_BLC;
2499 m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
2500 new_BLC_block->end_same_BLC=++old_BLC_block->start_same_BLC;
2501 return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
2504 #define SPLIT_LEFT -1
2505 #define SPLIT_RIGHT 1
2506 #define SPLIT_SMALLER 0
2512 void update_small_subblock_counters(state_in_block_pointer_lb* start_blocks,
2513 state_in_block_pointer_lb* splitpoint,
2514 state_in_block_pointer_lb* end_blocks,
2516 { assert(m_states_in_blocks.data()<=start_blocks);
2517 assert(start_blocks<splitpoint); assert(splitpoint<end_blocks);
2518 assert(end_blocks<=m_states_in_blocks.data_end());
2519 assert(
SPLIT_LEFT != split_type || std::distance(start_blocks, splitpoint) <=
2520 std::distance(splitpoint, end_blocks));
2521 assert(
SPLIT_RIGHT!= split_type || std::distance(start_blocks, splitpoint) >=
2522 std::distance(splitpoint, end_blocks));
2527 unsigned char log_old_size = check_complexity::ilog2
2528 (std::distance(start_blocks, end_blocks));
2529 unsigned char left_increment = log_old_size - check_complexity::ilog2
2530 (std::distance(start_blocks, splitpoint));
2531 if (left_increment > 0)
2541 block_type_lb& blk = *start_blocks->ref_state->block; assert(start_blocks == blk.start_bottom_states);
2542 blk.small_subblock_counter =
static_cast<
char>(blk.small_subblock_counter + left_increment);
2543 start_blocks = blk.end_states;
2545 while (start_blocks < splitpoint); assert(start_blocks == splitpoint);
2547 unsigned char right_increment = log_old_size - check_complexity::ilog2
2548 (std::distance(splitpoint, end_blocks)); assert(0<left_increment || 0<right_increment);
2549 if (right_increment > 0)
2553 block_type_lb& blk = *splitpoint->ref_state->block; assert(splitpoint == blk.start_bottom_states);
2554 blk.small_subblock_counter =
static_cast<
char>(blk.small_subblock_counter + right_increment);
2555 splitpoint = blk.end_states;
2557 while (splitpoint < end_blocks); assert(splitpoint == end_blocks);
2565 void update_all_small_subblock_counters
2566 (state_in_block_pointer_lb* start_block,
2567 state_in_block_pointer_lb* end_block)
2568 { assert(m_states_in_blocks.data()<=start_block); assert(start_block<end_block);
2569 assert(end_block<=m_states_in_blocks.data_end());
2570 unsigned char log_old_size = check_complexity::ilog2
2571 (std::distance(start_block, end_block));
2573 bool all_increments_are_nonzero =
true;
2577 block_type_lb& blk = *start_block->ref_state->block; assert(start_block == blk.start_bottom_states);
2578 unsigned char increment = log_old_size - check_complexity::ilog2
2579 (std::distance(start_block, blk.end_states));
2580 blk.small_subblock_counter =
static_cast<
char>(blk.small_subblock_counter + increment);
2583 { assert(all_increments_are_nonzero); all_increments_are_nonzero=
false; }
2585 start_block = blk.end_states;
2587 while (start_block < end_block); assert(start_block == end_block);
2591 state_index no_of_BLC_source_sets = 1;
2617 void make_BLC_simple_split_off_part(BLC_source_type& BLC_source,
2618 state_in_block_pointer_lb*
const splitpoint,
2619 const bool mark_all_transitions_in_instable_BLC_sets,
2620 constellation_type_lb* old_constellation,
2621 constellation_type_lb*
const new_constellation,
2623 { assert(BLC_source.start_BLC_source < splitpoint);
2624 state_in_block_pointer_lb* it = splitpoint; assert(splitpoint < BLC_source.end_BLC_source);
2625 state_in_block_pointer_lb* end_it = splitpoint; assert((null_constellation_lb==old_constellation)==
2626 (null_constellation_lb==new_constellation));
2627 update_small_subblock_counters(BLC_source.start_BLC_source, splitpoint,
2628 BLC_source.end_BLC_source, split_type);
2629 if (0 > split_type ||
2631 std::distance(BLC_source.start_BLC_source, splitpoint) <
2632 std::distance(splitpoint, BLC_source.end_BLC_source)))
2635 it = BLC_source.start_BLC_source;
2636 BLC_source.start_BLC_source = end_it;
2641 end_it = BLC_source.end_BLC_source;
2642 BLC_source.end_BLC_source = it;
2643 } assert(it < end_it);
2644 BLC_source_type*
const new_BLC_source=
2646 simple_list<BLC_indicators_lb>::get_pool().
2647 template construct<BLC_source_type>
2651 (it, end_it); assert(std::distance(it, end_it) <=
2652 std::distance(BLC_source.start_BLC_source,BLC_source.end_BLC_source));
2655 block_type_lb& current_block = *it->ref_state->block; assert(&BLC_source == current_block.block_BLC_source);
2656 const BLC_indicators_lb*
const old_large_splitter =
2657 null_state == current_block.refinement_info
2659 : ( assert(current_block.refinement_info < blocks_that_need_refinement.size()),
2660 blocks_that_need_refinement
2661 [current_block.refinement_info].large_splitter);
2662 current_block.block_BLC_source = new_BLC_source;
2663 state_in_block_pointer_lb*
const blk_end_it=current_block.end_states; assert(it < blk_end_it); assert(blk_end_it <= end_it);
2672 outgoing_transitions_it_lb out_it =
2673 it->ref_state->start_outgoing_transitions;
2674 outgoing_transitions_const_it_lb
const
2675 out_it_end=std::next(it->ref_state)==m_states.end()
2676 ? m_outgoing_transitions.end()
2677 : std::next(it->ref_state)->start_outgoing_transitions;
2678 for (; out_it < out_it_end; ++out_it)
2681 BLC_list_iterator old_position = out_it->ref_BLC_transitions;
2682 simple_list<BLC_indicators_lb>::iterator
2683 old_BLC_set = m_transitions[*old_position].
2684 transitions_per_block_to_constellation; assert(old_BLC_set->start_same_BLC<=old_position);
2685 assert(old_position<old_BLC_set->end_same_BLC);
2686 BLC_list_iterator new_position = old_BLC_set->start_same_BLC;
2687 simple_list<BLC_indicators_lb>::iterator new_BLC_set;
2688 const transition& tr = m_aut.get_transitions()[*old_position];
2689 const label_index a = label_or_divergence(tr);
2690 const transition* prev_tr;
2691 bool empty_old_BLC_set_can_be_deleted_immediately =
2692 null_constellation_lb == old_constellation;
2693 if (new_position == m_BLC_transitions.data() ||
2694 (prev_tr = &m_aut.get_transitions()[*std::prev(new_position)],
2695 m_states[prev_tr->from()].ref_states_in_blocks <
2696 new_BLC_source->start_BLC_source) ||
2697 m_states[prev_tr->from()].ref_states_in_blocks >=
2698 new_BLC_source->end_BLC_source ||
2699 m_states[tr.to()].block->constellation !=
2700 m_states[prev_tr->to()].block->constellation ||
2701 a != label_or_divergence(*prev_tr))
2707 if (old_BLC_set->is_stable())
2712 const constellation_type_lb* to_constln;
2713 simple_list<BLC_indicators_lb>::const_iterator old_co_splitter;
2714 constellation_type_lb* co_to_constln=null_constellation_lb;
2715 transition_index perhaps_new_co_spl_transition;
2716 const transition* perhaps_new_co_spl_t;
2717 if (null_constellation_lb != old_constellation &&
2721 (to_constln = m_states[tr.to()].block->constellation, assert(null_constellation_lb != new_constellation),
2722 (to_constln == old_constellation &&
2725 BLC_source.block_to_constellation.next(old_BLC_set),
2727 co_to_constln = new_constellation,
true)) ||
2728 (to_constln == new_constellation &&
2731 BLC_source.block_to_constellation.prev(old_BLC_set),
2733 co_to_constln = old_constellation,
true)) ||
2738 empty_old_BLC_set_can_be_deleted_immediately =
true,
2740 BLC_source.block_to_constellation.end()!=old_co_splitter &&
2748 m_BLC_transitions.data()<old_co_splitter->start_same_BLC &&
2752 (perhaps_new_co_spl_transition =
2753 *std::prev(old_co_splitter->start_same_BLC),
2754 perhaps_new_co_spl_t =
2755 &m_aut.get_transitions()[perhaps_new_co_spl_transition],
2757 m_states[perhaps_new_co_spl_t->from()].block->
2758 block_BLC_source == new_BLC_source) &&
2759 a == label_or_divergence(*perhaps_new_co_spl_t) &&
2760 co_to_constln == m_states
2761 [perhaps_new_co_spl_t->to()].block->constellation)
2765 if (old_constellation==to_constln)
2767 assert(new_constellation==co_to_constln);
2772 new_BLC_set = new_BLC_source->block_to_constellation.
2773 emplace(m_transitions[perhaps_new_co_spl_transition].
2774 transitions_per_block_to_constellation,
2775 new_position, new_position,
true);
2781 assert(old_constellation==co_to_constln);
2786 new_BLC_set = new_BLC_source->block_to_constellation.
2788 (m_transitions[perhaps_new_co_spl_transition].
2789 transitions_per_block_to_constellation,
2790 new_position, new_position,
true);
2792 empty_old_BLC_set_can_be_deleted_immediately =
true;
2804 new_BLC_set = new_BLC_source->block_to_constellation.
2805 emplace_front(new_position, new_position,
true);
2809 { assert(null_constellation_lb == old_constellation);
2810 assert(null_constellation_lb == new_constellation);
2811 new_BLC_set = new_BLC_source->block_to_constellation.
2812 emplace_back(new_position, new_position,
false);
2815 new_BLC_set->work_counter = old_BLC_set->work_counter;
2817 if (null_state != current_block.refinement_info && ( assert(current_block.refinement_info < blocks_that_need_refinement.size()),
2818 &*old_BLC_set == blocks_that_need_refinement
2819 [current_block.refinement_info].large_splitter))
2821 blocks_that_need_refinement[current_block.refinement_info].
2822 large_splitter = &*new_BLC_set;
2828 new_BLC_set = m_transitions[*std::prev(new_position)].
2829 transitions_per_block_to_constellation;
2833 bool last_element_removed =
2834 swap_in_the_doubly_linked_list_LBC_in_blocks_new_block
2835 (*old_position, new_BLC_set, old_BLC_set,
2836 mark_all_transitions_in_instable_BLC_sets);
2841 if (last_element_removed)
2843 if (!empty_old_BLC_set_can_be_deleted_immediately ||
2844 (null_constellation_lb != old_constellation &&
2845 !old_BLC_set->is_stable()))
2870 m_BLC_indicators_to_be_deleted.emplace_back(BLC_source,
2875 assert(old_BLC_set->start_same_BLC==old_BLC_set->end_same_BLC);
2876 BLC_source.block_to_constellation.erase(old_BLC_set);
2882 }
else { assert(old_BLC_set->start_same_BLC<old_BLC_set->end_same_BLC); }
2886 while (it < blk_end_it);
2887 if (
nullptr != old_large_splitter)
2888 { assert(current_block.refinement_info < blocks_that_need_refinement.size());
2889 if(old_large_splitter == blocks_that_need_refinement
2890 [current_block.refinement_info].large_splitter)
2893 for (BLC_list_const_iterator it = old_large_splitter->start_same_BLC;
2894 it != old_large_splitter->end_same_BLC; ++it)
2896 assert(m_states[m_aut.get_transitions()[*it].from()].block!=¤t_block);
2899 blocks_that_need_refinement[current_block.refinement_info].
2900 large_splitter =
nullptr;
2904 simple_list<BLC_indicators_lb>::const_iterator
2905 BLC_it = new_BLC_source->block_to_constellation.begin();
2907 assert(new_BLC_source->block_to_constellation.end() != BLC_it);
2908 }
while(&*BLC_it++!=blocks_that_need_refinement[current_block.refinement_info].large_splitter);
2913 while (it < end_it);
2914 ++no_of_BLC_source_sets;
2942 void make_BLC_simple(block_type_lb& block_index,
2943 const bool mark_all_transitions_in_instable_BLC_sets =
false,
2944 constellation_type_lb*
const old_constellation = null_constellation_lb,
2945 constellation_type_lb*
const new_constellation = null_constellation_lb)
2949 BLC_source_type& BLC_source = *block_index.block_BLC_source; assert(BLC_source.start_BLC_source <= block_index.start_bottom_states);
2950 assert(block_index.end_states <= BLC_source.end_BLC_source);
2951 assert(m_branching);
2952 if (state_index first_part_size = std::distance
2953 (BLC_source.start_BLC_source, block_index.start_bottom_states);
2954 0 == first_part_size)
2956 if (block_index.end_states == BLC_source.end_BLC_source)
2961 make_BLC_simple_split_off_part(BLC_source, block_index.end_states,
2962 mark_all_transitions_in_instable_BLC_sets,
2963 old_constellation, new_constellation);
2964 }
else if (state_index last_part_size = std::distance
2965 (block_index.end_states, BLC_source.end_BLC_source);
2966 0 == last_part_size)
2968 make_BLC_simple_split_off_part(BLC_source,
2969 block_index.start_bottom_states,
2970 mark_all_transitions_in_instable_BLC_sets,
2971 old_constellation, new_constellation);
2973 state_in_block_pointer_lb* splitpoint = block_index.end_states;
2975 if (first_part_size < last_part_size)
2978 make_BLC_simple_split_off_part(BLC_source,
2979 block_index.start_bottom_states,
2980 mark_all_transitions_in_instable_BLC_sets,
2981 old_constellation, new_constellation,
SPLIT_LEFT);
2986 make_BLC_simple_split_off_part(BLC_source,
2987 block_index.end_states,
2988 mark_all_transitions_in_instable_BLC_sets,
2989 old_constellation, new_constellation,
SPLIT_RIGHT);
2990 splitpoint = block_index.start_bottom_states;
2992 make_BLC_simple_split_off_part(BLC_source, splitpoint,
2993 mark_all_transitions_in_instable_BLC_sets,
2994 old_constellation, new_constellation);
3003 void clear_state_counters
3004 (std::vector<state_in_block_pointer_lb>::const_iterator begin,
3005 std::vector<state_in_block_pointer_lb>::const_iterator
const end,
3006 block_type_lb& block)
3010 { assert(&block==begin->ref_state->block);
3011 begin->ref_state->counter=undefined;
3019 void change_non_bottom_state_to_bottom_state
3020 (
const fixed_vector<state_type_gj_lb>::iterator si)
3021 { assert(m_states.begin()<=si);
3022 block_type_lb& bi = *si->block; assert(si<m_states.end());
3023 swap_states_in_states_in_block(si->ref_states_in_blocks,
3024 bi.sta.rt_non_bottom_states); assert(0 == si->no_of_outgoing_block_inert_transitions);
3025 bi.sta.rt_non_bottom_states++; assert(!bi.contains_new_bottom_states);
3026 ++no_of_new_bottom_states;
3030 void make_stable_and_move_to_start_of_BLC
3031 (BLC_source_type& from_blc_src,
3032 const simple_list<BLC_indicators_lb>::iterator splitter)
3033 { assert(from_blc_src.block_to_constellation.end()!=splitter);
3034 splitter->make_stable(); assert(splitter->start_same_BLC<splitter->end_same_BLC);
3036 const transition& t=m_aut.get_transitions()[*splitter->start_same_BLC];
3037 assert(&from_blc_src==m_states[t.from()].block->block_BLC_source);
3039 simple_list<BLC_indicators_lb>& btc=from_blc_src.block_to_constellation; assert(!btc.empty());
3040 if (splitter!=btc.begin())
3042 btc.splice(btc.begin(), btc, splitter);
3050 void move_nonbottom_states_to(
const todo_state_vector_lb& R,
3051 state_in_block_pointer_lb* to_pos
3052 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3053 , state_index new_block_bottom_size
3057 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3058 unsigned char const max_B=check_complexity::log_n-
3059 check_complexity::ilog2(new_block_bottom_size+R.size());
3061 for (state_in_block_pointer_lb st: R)
3063 split_block_B_into_R_and_BminR_carry_out_split, max_B), *
this);
3064 swap_states_in_states_in_block(to_pos++,
3065 st.ref_state->ref_states_in_blocks);
3075 block_type_lb* create_new_block(
3076 state_in_block_pointer_lb* start_bottom_states,
3077 state_in_block_pointer_lb*
const start_non_bottom_states,
3078 state_in_block_pointer_lb*
const end_states,
3079 block_type_lb& old_block_index)
3082 constellation_type_lb& constellation=*old_block_index.constellation; assert(constellation.start_const_states<=start_bottom_states);
3083 assert(old_block_index.block_BLC_source->start_BLC_source<=start_bottom_states);
3084 assert(start_bottom_states<end_states);
3085 block_type_lb& new_block_index = *
3087 simple_list<BLC_indicators_lb>::get_pool().
3088 template construct<block_type_lb>
3092 (start_bottom_states, start_non_bottom_states, end_states,
3093 constellation, *old_block_index.block_BLC_source,
3094 old_block_index.small_subblock_counter); assert(end_states<=constellation.end_const_states);
3095 ++no_of_blocks; assert(end_states<=old_block_index.block_BLC_source->end_BLC_source);
3097 new_block_index.work_counter=old_block_index.work_counter;
3099 for(; start_bottom_states<start_non_bottom_states; ++start_bottom_states)
3101 start_bottom_states->ref_state->no_of_outgoing_block_inert_transitions);
3102 assert(&old_block_index==start_bottom_states->ref_state->block);
3103 start_bottom_states->ref_state->block=&new_block_index; assert(start_bottom_states->ref_state->counter==undefined);
3105 for (; start_bottom_states<end_states; ++start_bottom_states)
3106 { assert(&old_block_index==start_bottom_states->ref_state->block);
3107 start_bottom_states->ref_state->block=&new_block_index; assert(0!=
3108 start_bottom_states->ref_state->no_of_outgoing_block_inert_transitions);
3109 start_bottom_states->ref_state->counter=undefined;
3112 return &new_block_index;
3116 void check_incoming_tau_transitions_become_noninert(
3117 block_type_lb& NewBotSt_block,
3118 state_in_block_pointer_lb* start_bottom,
3119 state_in_block_pointer_lb*
const end_non_bottom)
3121 for (; start_bottom!=end_non_bottom; ++start_bottom)
3123 std::vector<transition>::const_iterator
const in_it_end=
3124 std::next(start_bottom->ref_state)>=m_states.end()
3125 ? m_aut.get_transitions().end()
3126 : std::next(start_bottom->ref_state)->start_incoming_transitions; assert(&NewBotSt_block != start_bottom->ref_state->block);
3127 for (std::vector<transition>::iterator
3128 in_it=start_bottom->ref_state->start_incoming_transitions;
3130 m_aut.is_tau(m_aut_apply_hidden_label_map(in_it->label()));
3133 const fixed_vector<state_type_gj_lb>::iterator
3134 from=m_states.begin()+
static_cast<std::ptrdiff_t>(in_it->from()); assert(m_states[in_it->to()].ref_states_in_blocks==start_bottom);
3135 if (&NewBotSt_block == from->block)
3137 if (0== --from->no_of_outgoing_block_inert_transitions)
3139 change_non_bottom_state_to_bottom_state(from);
3146 #ifdef MORE_STATISTICS
3154 void update_sample_counter_for_new_block(block_type_lb& new_block,
3155 block_type_lb& old_block)
3157 assert(null_state == new_block.refinement_info);
3158 fixed_vector<state_type_gj_lb>::iterator additional_sample_state =
3159 new_block.start_bottom_states->ref_state; assert(old_block.refinement_info < blocks_that_need_refinement.size());
3160 if (&new_block == blocks_that_need_refinement
3161 [old_block.refinement_info].transition_count_sample_state->block)
3165 swap_states_in_states_in_block(new_block.start_bottom_states,
3166 blocks_that_need_refinement[old_block.refinement_info].
3167 transition_count_sample_state->ref_states_in_blocks);
3168 additional_sample_state = old_block.start_bottom_states->ref_state; assert(&old_block == additional_sample_state->block);
3169 blocks_that_need_refinement[old_block.refinement_info].
3170 transition_count_sample_state = additional_sample_state;
3173 assert(0==additional_sample_state->no_of_outgoing_block_inert_transitions);
3174 outgoing_transitions_const_it_lb
const out_it_end =
3175 std::next(additional_sample_state)>=m_states.end()
3176 ? m_outgoing_transitions.end()
3177 : std::next(additional_sample_state)->start_outgoing_transitions; assert(old_block.constellation==additional_sample_state->block->constellation);
3178 for (outgoing_transitions_it_lb out_it = additional_sample_state->
3179 start_outgoing_transitions; out_it < out_it_end; assert(out_it <= out_it->start_same_saC),
3180 out_it = std::next(out_it->start_same_saC))
3182 ++no_of_non_block_inert_sample_transitions;
3189 BLC_indicators_lb* next_target_constln_in_same_saC(
3190 state_in_block_pointer_lb
const src,
3191 BLC_list_const_iterator
const splitter_it)
const
3192 { assert(m_states.begin()+m_aut.get_transitions()[*splitter_it].from()==
3194 outgoing_transitions_const_it_lb
3195 out_it=m_transitions[*splitter_it].ref_outgoing_transitions;
3196 if (out_it<out_it->start_same_saC)
3198 out_it=out_it->start_same_saC;
3201 outgoing_transitions_const_it_lb
const
3202 out_it_end=std::next(src.ref_state)>=m_states.end()
3203 ? m_outgoing_transitions.end()
3204 : std::next(src.ref_state)->start_outgoing_transitions;
3205 if (out_it<out_it_end)
3207 return &*m_transitions[*out_it->ref_BLC_transitions].
3208 transitions_per_block_to_constellation;
3216 #ifdef MORE_STATISTICS
3217 transition_index number_of_large_splitters_searched_in_small_subblocks=0;
3218 transition_index number_of_large_splitters_searched_in_large_subblocks=0;
3266 block_type_lb* four_way_splitB(block_that_needs_refinement_type& bri,
3267 constellation_type_lb*
const old_constellation = null_constellation_lb,
3268 constellation_type_lb*
const new_constellation = null_constellation_lb)
3270 block_type_lb& bi=*bri.start_bottom_states[0]->ref_state->block; assert(1<number_of_states_in_block(bi));
3271 assert(!bi.contains_new_bottom_states);
3284 static todo_state_vector_lb non_bottom_states[4]; assert(null_block_lb == m_singleton_block_with_new_bottom_states_for_debug);
3286 #define non_bottom_states_NewBotSt non_bottom_states[3
]
3293 #define bottom_and_non_bottom_size(coroutine) ( assert
(aborted!=status[(coroutine)]),
3294 bri.bottom_size((coroutine))+non_bottom_states[(coroutine)].size())
3301 BLC_list_iterator large_splitter_iter_NewBotSt;
3302 BLC_list_iterator large_splitter_iter_end_NewBotSt;
3303 bool large_splitter_is_known_to_be_a_strict_BLC_set =
false;
3305 if (
nullptr != bri.large_splitter )
3308 const simple_list<BLC_indicators_lb>& btc =
3309 bi.block_BLC_source->block_to_constellation;
3310 for (simple_list<BLC_indicators_lb>::const_iterator it = btc.begin();
3311 bri.large_splitter != &*it; ++it)
3312 { assert(btc.end() != it); }
3316 large_splitter_iter_NewBotSt = bri.large_splitter->start_same_BLC;
3317 large_splitter_iter_end_NewBotSt = bri.large_splitter->is_stable()
3318 ? bri.large_splitter->end_same_BLC
3319 : ( assert(null_constellation_lb == old_constellation),
3320 assert(null_constellation_lb == new_constellation),
3321 bri.large_splitter->start_marked_BLC);
3333 large_splitter_iter_NewBotSt = m_BLC_transitions.data_end();
3334 large_splitter_iter_end_NewBotSt = m_BLC_transitions.data_end();
3335 large_splitter_is_known_to_be_a_strict_BLC_set =
true;
3338 assert(bi.start_bottom_states==bri.start_bottom_states[ReachAlw]);
3339 assert(bri.start_bottom_states[ReachAlw]<=bri.start_bottom_states[AvoidSml]);
3340 assert(bri.start_bottom_states[AvoidSml]<=bri.start_bottom_states[AvoidLrg]);
3341 assert(bri.start_bottom_states[AvoidLrg]<=bri.start_bottom_states[AvoidLrg+1]);
3342 assert(bri.start_bottom_states[AvoidLrg+1]==bi.sta.rt_non_bottom_states);
3344 if (bi.sta.rt_non_bottom_states==bi.end_states)
3347 block_type_lb* ReachAlw_block_index = null_block_lb;
3348 constellation_type_lb& constellation=*bi.constellation;
3349 const bool constellation_was_trivial=
3350 constellation.start_const_states->ref_state->block==
3351 std::prev(constellation.end_const_states)->ref_state->block;
3352 bool constellation_becomes_nontrivial=
false;
3354 if (bri.bottom_size(ReachAlw) < bri.bottom_size(AvoidLrg))
3355 { assert(bi.start_bottom_states==bri.start_bottom_states[ReachAlw]);
3356 if (0 < bri.bottom_size(ReachAlw))
3358 bi.start_bottom_states = bri.start_bottom_states[ReachAlw+1];
3359 ReachAlw_block_index=create_new_block
3360 (bri.start_bottom_states[ReachAlw],
3361 bri.start_bottom_states[ReachAlw+1],
3362 bri.start_bottom_states[ReachAlw+1], bi);
3363 #ifdef MORE_STATISTICS
3364 update_sample_counter_for_new_block(*ReachAlw_block_index, bi);
3366 constellation_becomes_nontrivial=
true;
3368 if (bri.bottom_size(AvoidSml) < bri.bottom_size(AvoidLrg))
3369 { assert(bi.start_bottom_states==bri.start_bottom_states[AvoidSml]);
3370 if (0 < bri.bottom_size(AvoidSml))
3372 bi.start_bottom_states = bri.start_bottom_states[AvoidSml+1];
3373 block_type_lb& AvoidSml_block = *create_new_block
3374 (bri.start_bottom_states[AvoidSml],
3375 bri.start_bottom_states[AvoidSml+1],
3376 bri.start_bottom_states[AvoidSml+1], bi);
3377 #ifdef MORE_STATISTICS
3378 update_sample_counter_for_new_block(AvoidSml_block, bi);
3380 (
void) AvoidSml_block;
3382 constellation_becomes_nontrivial=
true;
3385 else if (0 < bri.bottom_size(AvoidLrg))
3386 { assert(bi.end_states==bri.start_bottom_states[AvoidLrg+1]);
3387 bi.sta.rt_non_bottom_states = bri.start_bottom_states[AvoidLrg];
3388 bi.end_states = bri.start_bottom_states[AvoidLrg];
3389 block_type_lb& AvoidLrg_block = *create_new_block
3390 (bri.start_bottom_states[AvoidLrg],
3391 bri.start_bottom_states[AvoidLrg+1],
3392 bri.start_bottom_states[AvoidLrg+1], bi);
3393 #ifdef MORE_STATISTICS
3394 update_sample_counter_for_new_block(AvoidLrg_block, bi);
3396 (
void) AvoidLrg_block;
3398 constellation_becomes_nontrivial=
true;
3402 { assert(bi.end_states==bri.start_bottom_states[AvoidLrg+1]);
3403 if (0 < bri.bottom_size(AvoidLrg))
3405 bi.sta.rt_non_bottom_states = bri.start_bottom_states[AvoidLrg];
3406 bi.end_states = bri.start_bottom_states[AvoidLrg];
3407 block_type_lb& AvoidLrg_block = *create_new_block
3408 (bri.start_bottom_states[AvoidLrg],
3409 bri.start_bottom_states[AvoidLrg+1],
3410 bri.start_bottom_states[AvoidLrg+1], bi);
3411 #ifdef MORE_STATISTICS
3412 update_sample_counter_for_new_block(AvoidLrg_block, bi);
3414 (
void) AvoidLrg_block;
3416 constellation_becomes_nontrivial=
true;
3418 if (bri.bottom_size(ReachAlw) < bri.bottom_size(AvoidSml))
3419 { assert(bi.start_bottom_states==bri.start_bottom_states[ReachAlw]);
3420 bi.start_bottom_states = bri.start_bottom_states[ReachAlw+1]; assert(0<bri.bottom_size(ReachAlw));
3421 ReachAlw_block_index=create_new_block
3422 (bri.start_bottom_states[ReachAlw],
3423 bri.start_bottom_states[ReachAlw+1],
3424 bri.start_bottom_states[ReachAlw+1], bi);
3425 #ifdef MORE_STATISTICS
3426 update_sample_counter_for_new_block(*ReachAlw_block_index, bi);
3428 constellation_becomes_nontrivial=
true;
3432 ReachAlw_block_index = &bi;
3433 if (0 < bri.bottom_size(AvoidSml))
3434 { assert(bi.end_states==bri.start_bottom_states[AvoidSml+1]);
3435 bi.sta.rt_non_bottom_states = bri.start_bottom_states[AvoidSml];
3436 bi.end_states = bri.start_bottom_states[AvoidSml];
3437 block_type_lb& AvoidSml_block = *create_new_block
3438 (bri.start_bottom_states[AvoidSml],
3439 bri.start_bottom_states[AvoidSml+1],
3440 bri.start_bottom_states[AvoidSml+1], bi);
3441 #ifdef MORE_STATISTICS
3442 update_sample_counter_for_new_block(AvoidSml_block, bi);
3444 (
void) AvoidSml_block;
3446 constellation_becomes_nontrivial=
true;
3451 if (constellation_becomes_nontrivial && constellation_was_trivial)
3452 { assert(std::find(m_non_trivial_constellations.begin(),
3453 m_non_trivial_constellations.end(),
3454 &constellation)==m_non_trivial_constellations.end());
3455 m_non_trivial_constellations.emplace_back(&constellation);
3458 #ifdef MORE_STATISTICS
3459 swap_states_in_states_in_block(bi.start_bottom_states,
3460 bri.transition_count_sample_state->ref_states_in_blocks); assert(&bi==bri.transition_count_sample_state->block);
3461 assert(0==bri.transition_count_sample_state->
3462 no_of_outgoing_block_inert_transitions);
3464 update_all_small_subblock_counters(bri.start_bottom_states[ReachAlw],
3465 bri.start_bottom_states[AvoidLrg+1]);
3466 return ReachAlw_block_index;
3467 } assert(m_branching);
3489 assert(non_bottom_states[ReachAlw].empty());
3490 assert(non_bottom_states[AvoidSml].empty());
3491 assert(non_bottom_states[AvoidLrg].empty());
3494 enum { state_checking,
3495 incoming_inert_transition_checking,
3496 outgoing_constellation_checking,
3497 aborted, finished } status[3], status_NewBotSt;
3498 state_in_block_pointer_lb* current_bottom_state_iter[3];
3499 #define DEBUG_coroutine_name(coroutine) ((coroutine)<=AvoidSml
3500 ? ((coroutine) < AvoidSml ? "ReachAlw" : "AvoidSml")
3501 : ((coroutine)== AvoidLrg ? "AvoidLrg" : "NewBotSt"))
3503 state_index no_of_unfinished_states_in_block=
3504 number_of_states_in_block(bi);
3512 #define abort_if_bottom_size_too_large(coroutine)
3513 (( assert
(non_bottom_states[(coroutine)].empty()),
3514 bri.bottom_size((coroutine))>no_of_unfinished_states_in_block/2
) &&
3515 ( assert
(std::numeric_limits<state_index>::max()!=
3516 no_of_unfinished_states_in_block),
3517 no_of_unfinished_states_in_block=
3518 std::numeric_limits<state_index>::max(), assert
(m_aut.num_states()<no_of_unfinished_states_in_block/2
),
3519 status[(coroutine)]=aborted,
3534 #define abort_if_non_bottom_size_too_large_NewBotSt(i)
3535 (( assert
(aborted!=status_NewBotSt),
3536 non_bottom_states_NewBotSt.size()+(i)>
3537 no_of_unfinished_states_in_block/2
) &&
3538 ( assert
(std::numeric_limits<state_index>::max()!=
3539 no_of_unfinished_states_in_block),
3540 no_of_unfinished_states_in_block=
3541 std::numeric_limits<state_index>::max(), assert
(m_aut.num_states()<no_of_unfinished_states_in_block/2
),
3542 status_NewBotSt=aborted,
3558 #define abort_if_size_too_large(coroutine, i)
3559 (bottom_and_non_bottom_size((coroutine))+(i)>
3560 no_of_unfinished_states_in_block/2
&&
3561 ( assert
(std::numeric_limits<state_index>::max()!=
3562 no_of_unfinished_states_in_block),
3563 no_of_unfinished_states_in_block=
3564 std::numeric_limits<state_index>::max(), assert
(m_aut.num_states()<no_of_unfinished_states_in_block/2
),
3565 status[(coroutine)]=aborted,
3566 non_bottom_states[(coroutine)].clear(),
3569 int no_of_finished_searches=0;
3570 int no_of_running_searches=0;
3571 enum subblocks running_searches[3];
3573 if (0==bri.bottom_size(AvoidSml))
3574 { assert(0==bri.bottom_size(AvoidSml));
3576 assert(bri.potential_non_bottom_states[AvoidSml].empty());
3578 if (0==bri.bottom_size(AvoidLrg))
3588 clear_state_counters
3589 (bri.potential_non_bottom_states[ReachAlw].begin(),
3590 bri.potential_non_bottom_states[ReachAlw].end(), bi);
3591 clear(bri.potential_non_bottom_states[ReachAlw]);
3592 clear_state_counters
3593 (bri.potential_non_bottom_states_HitSmall.begin(),
3594 bri.potential_non_bottom_states_HitSmall.end(), bi);
3595 clear(bri.potential_non_bottom_states_HitSmall);
3597 #ifdef MORE_STATISTICS
3600 swap_states_in_states_in_block(bi.start_bottom_states,
3601 bri.transition_count_sample_state->ref_states_in_blocks); assert(&bi==bri.transition_count_sample_state->block);
3602 assert(0==bri.transition_count_sample_state->
3603 no_of_outgoing_block_inert_transitions);
3607 ++no_of_finished_searches;
3608 status[AvoidSml]=finished;
3612 running_searches[no_of_running_searches] = AvoidSml;
3613 ++no_of_running_searches;
3614 current_bottom_state_iter[AvoidSml]=bri.start_bottom_states[AvoidSml];
3615 status[AvoidSml]=state_checking;
3618 if (0 == bri.bottom_size(AvoidLrg))
3621 assert(bri.potential_non_bottom_states[AvoidLrg].empty());
3622 ++no_of_finished_searches;
3623 status[AvoidLrg]=finished;
3627 running_searches[no_of_running_searches] = AvoidLrg;
3628 ++no_of_running_searches;
3629 current_bottom_state_iter[AvoidLrg]=bri.start_bottom_states[AvoidLrg];
3630 status[AvoidLrg]=state_checking;
3633 status_NewBotSt=state_checking;
3634 if (0==bri.bottom_size(ReachAlw))
3642 (bri.potential_non_bottom_states[ReachAlw]);
3643 if (finished == status[AvoidLrg])
3651 (bri.potential_non_bottom_states_HitSmall.begin(),
3652 bri.potential_non_bottom_states_HitSmall.end());
3653 clear(bri.potential_non_bottom_states_HitSmall);
3658 (bri.potential_non_bottom_states_HitSmall);
3664 st.ref_state->counter=marked_NewBotSt;
3666 ++no_of_finished_searches;
3667 status[ReachAlw]=finished;
3672 running_searches[no_of_running_searches] = ReachAlw;
3673 ++no_of_running_searches;
3674 current_bottom_state_iter[ReachAlw]=bri.start_bottom_states[ReachAlw];
3675 status[ReachAlw]=state_checking;
3697 std::vector<transition>::iterator current_source_iter[3];
3698 std::vector<transition>::iterator current_source_iter_NewBotSt;
3699 std::vector<transition>::const_iterator current_source_iter_end[3];
3700 std::vector<transition>::const_iterator current_source_iter_end_NewBotSt;
3702 state_in_block_pointer_lb current_source_AvoidLrg;
3703 outgoing_transitions_const_it_lb
3704 current_outgoing_iter_start_AvoidLrg, current_outgoing_iter_AvoidLrg; assert(large_splitter_iter_NewBotSt<=large_splitter_iter_end_NewBotSt);
3706 { assert(2>=no_of_finished_searches);
3707 for (
int current_search_index=0; current_search_index<
3708 no_of_running_searches; ++current_search_index)
3710 const enum subblocks
3711 current_search=running_searches[current_search_index]; assert(0<=current_search); assert(current_search<NewBotSt);
3713 if (incoming_inert_transition_checking==status[current_search])
3714 { assert(current_source_iter[current_search]<
3715 current_source_iter_end[current_search]);
3716 mCRL2complexity(&m_transitions[std::distance(m_aut.get_transitions().begin(),
3717 current_source_iter[current_search])], add_work(check_complexity::
3718 simple_splitB_U_handle_transition_to_U_state, 1), *
this);
3719 const transition& tr=*current_source_iter[current_search]++; assert(m_aut.is_tau(m_aut_apply_hidden_label_map(tr.label())));
3720 state_in_block_pointer_lb
const src = m_states.begin() +
static_cast<std::ptrdiff_t>(tr.from()); assert(m_states[tr.to()].block==&bi);
3722 if (src.ref_state->block==&bi &&
3723 !(m_preserve_divergence && tr.from()==tr.to()))
3724 { assert(!non_bottom_states[ReachAlw].find(src));
3725 assert(!non_bottom_states[AvoidSml].find(src));
3726 assert(!non_bottom_states[AvoidLrg].find(src));
3727 const transition_index current_counter=src.ref_state->counter;
3729 if( ( ( undefined==current_counter
3730 || ( marked_HitSmall==current_counter
3731 && AvoidSml!=current_search ) || (assert(marked_HitSmall!=current_counter || AvoidSml==current_search),
false)
3734 src.ref_state->counter=marked(current_search)+
3735 src.ref_state->no_of_outgoing_block_inert_transitions, assert(std::find(bri.potential_non_bottom_states[current_search].begin(),
3736 bri.potential_non_bottom_states[current_search].end(), src)==
3737 bri.potential_non_bottom_states[current_search].end()),
3738 bri.potential_non_bottom_states[current_search].
3741 || is_in_marked_range_of(current_counter, current_search) )
3742 { assert(is_in_marked_range_of(src.ref_state->counter, current_search));
3744 --src.ref_state->counter; assert(is_in_marked_range_of(src.ref_state->counter, current_search));
3746 if (marked(current_search)==src.ref_state->counter)
3750 if (AvoidLrg==current_search &&
3751 large_splitter_iter_NewBotSt!=
3752 large_splitter_iter_end_NewBotSt)
3753 { assert(
nullptr != bri.large_splitter);
3759 src.ref_state->counter = marked(AvoidLrg)+marked_range-1;
3760 current_source_AvoidLrg=src;
3761 status[AvoidLrg] = outgoing_constellation_checking;
3762 current_outgoing_iter_start_AvoidLrg=
3763 src.ref_state->start_outgoing_transitions;
3764 current_outgoing_iter_AvoidLrg=
3765 std::next(src.ref_state)>=m_states.end()
3766 ? m_outgoing_transitions.end()
3767 : std::next(src.ref_state)->start_outgoing_transitions; assert(current_outgoing_iter_start_AvoidLrg<current_outgoing_iter_AvoidLrg);
3772 { assert(running_searches[current_search_index]==current_search);
3773 --no_of_running_searches; assert(current_search_index<=no_of_running_searches);
3774 running_searches[current_search_index]=
3775 running_searches[no_of_running_searches]; assert(std::find(bri.potential_non_bottom_states[current_search].begin(),
3776 bri.potential_non_bottom_states[current_search].end(), src)!=
3777 bri.potential_non_bottom_states[current_search].end());
3778 --current_search_index;
3782 non_bottom_states[current_search].add_todo(src);
3786 else if (marked_NewBotSt != src.ref_state->counter)
3792 if (aborted!=status_NewBotSt &&
3800 src.ref_state->counter = marked_NewBotSt;
3806 if (current_source_iter[current_search]!=
3807 current_source_iter_end[current_search] &&
3808 m_aut.is_tau(m_aut_apply_hidden_label_map
3809 (current_source_iter[current_search]->label())))
3813 status[current_search]=state_checking;
3815 else if (state_checking == status[current_search])
3818 state_in_block_pointer_lb
const tgt=
3819 current_bottom_state_iter[current_search]<
3820 bri.start_bottom_states[current_search+1]
3821 ? *current_bottom_state_iter[current_search]++
3822 : non_bottom_states[current_search].move_from_todo(); assert(!non_bottom_states[current_search^1].find(tgt));
3824 add_work(check_complexity::simple_splitB_U_find_predecessors, 1), *
this);
3825 current_source_iter[current_search]=
3826 tgt.ref_state->start_incoming_transitions; assert(!non_bottom_states[current_search^2].find(tgt));
3827 current_source_iter_end[current_search]=
3828 std::next(tgt.ref_state)>=m_states.end()
3829 ? m_aut.get_transitions().end()
3830 : std::next(tgt.ref_state)->start_incoming_transitions; assert(!non_bottom_states[current_search^3].find(tgt));
3831 if (current_source_iter[current_search]<
3832 current_source_iter_end[current_search] &&
3833 m_aut.is_tau(m_aut_apply_hidden_label_map
3834 (current_source_iter[current_search]->label())))
3836 status[current_search]=incoming_inert_transition_checking;
3841 { assert(AvoidLrg==current_search);
3842 assert(outgoing_constellation_checking==status[AvoidLrg]);
3843 assert(current_outgoing_iter_start_AvoidLrg<current_outgoing_iter_AvoidLrg);
3844 assert(m_outgoing_transitions.end()==current_outgoing_iter_AvoidLrg ||
3845 current_outgoing_iter_start_AvoidLrg<
3846 current_outgoing_iter_AvoidLrg->start_same_saC);
3847 --current_outgoing_iter_AvoidLrg; assert(current_outgoing_iter_AvoidLrg->start_same_saC<=
3848 current_outgoing_iter_AvoidLrg);
3849 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3851 outgoing_transitions_const_it_lb out_it=
3852 current_outgoing_iter_AvoidLrg->start_same_saC;
3854 add_work(check_complexity::
3855 simple_splitB_U_handle_transition_from_potential_U_state, 1), *
this);
3857 while (++out_it<=current_outgoing_iter_AvoidLrg) {
3859 add_work_notemporary(check_complexity::
3860 simple_splitB_U_handle_transition_from_potential_U_state, 1), *
this);
3864 assert(!non_bottom_states[ReachAlw].find(current_source_AvoidLrg));
3865 assert(!non_bottom_states[AvoidLrg].find(current_source_AvoidLrg));
3866 assert(!non_bottom_states[AvoidSml].find(current_source_AvoidLrg));
3867 assert(marked(AvoidLrg)+marked_range-1 ==
3868 current_source_AvoidLrg.ref_state->counter ||
3869 marked_NewBotSt==current_source_AvoidLrg.ref_state->counter);
3870 simple_list<BLC_indicators_lb>::const_iterator
const
3871 current_splitter=m_transitions[
3872 *current_outgoing_iter_AvoidLrg->ref_BLC_transitions].
3873 transitions_per_block_to_constellation; assert(
nullptr != bri.large_splitter);
3874 if (current_splitter==bri.large_splitter)
3879 if (marked_NewBotSt!=current_source_AvoidLrg.ref_state->counter)
3884 if (aborted!=status_NewBotSt &&
3886 { assert(aborted!=status_NewBotSt);
3892 current_source_AvoidLrg.ref_state->counter = marked_NewBotSt;
3897 else if (current_outgoing_iter_AvoidLrg=
3898 current_outgoing_iter_AvoidLrg->start_same_saC,
3899 current_outgoing_iter_start_AvoidLrg==
3900 current_outgoing_iter_AvoidLrg
3913 { assert(marked(AvoidLrg)+marked_range-1 ==
3914 current_source_AvoidLrg.ref_state->counter);
3917 { assert(running_searches[current_search_index]==AvoidLrg);
3918 --no_of_running_searches; assert(current_search_index<=no_of_running_searches);
3919 running_searches[current_search_index]=
3920 running_searches[no_of_running_searches]; assert(std::find(bri.potential_non_bottom_states[AvoidLrg].begin(),
3921 bri.potential_non_bottom_states[AvoidLrg].end(), current_source_AvoidLrg)!=
3922 bri.potential_non_bottom_states[AvoidLrg].end());
3923 --current_search_index;
3927 current_source_AvoidLrg.ref_state->counter = marked(AvoidLrg);
3928 non_bottom_states[AvoidLrg].add_todo(current_source_AvoidLrg);
3937 if (current_source_iter[AvoidLrg]!=
3938 current_source_iter_end[AvoidLrg] &&
3939 m_aut.is_tau(m_aut_apply_hidden_label_map(current_source_iter
3940 [AvoidLrg]->label())))
3942 status[AvoidLrg] = incoming_inert_transition_checking;
3945 status[AvoidLrg]=state_checking;
3948 assert(state_checking==status[current_search]);
3949 assert(NewBotSt!=current_search);
3951 if (current_bottom_state_iter[current_search]==
3952 bri.start_bottom_states[current_search+1] &&
3953 non_bottom_states[current_search].todo_is_empty())
3957 status[current_search]=finished;
3958 ++no_of_finished_searches;
3959 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3966 check_complexity::check_temporary_work();
3968 const unsigned char max_new_B=check_complexity::log_n-
3970 for (
const state_in_block_pointer_lb* s=bri.start_bottom_states[current_search];
3971 (s!=bri.start_bottom_states[current_search+1] ||
3972 (s=non_bottom_states[current_search].data(),
true)) &&
3973 s!=non_bottom_states[current_search].data_end(); ++s)
3976 simple_splitB_U_find_predecessors, check_complexity::
3977 simple_splitB_find_predecessors_of_R_or_U_state, max_new_B), *
this);
3979 const std::vector<transition>::const_iterator in_ti_end=
3980 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
3981 : std::next(s->ref_state)->start_incoming_transitions;
3982 for (std::vector<transition>::const_iterator
3983 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
3985 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
3987 cbegin(), ti)], finalise_work(check_complexity::
3988 simple_splitB_U_handle_transition_to_U_state, check_complexity::
3989 simple_splitB_handle_transition_to_R_or_U_state, max_new_B), *
this);
3991 if (AvoidLrg==current_search &&
3992 0!=s->ref_state->no_of_outgoing_block_inert_transitions)
3995 const outgoing_transitions_const_it_lb out_ti_end=
3996 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
3997 : std::next(s->ref_state)->start_outgoing_transitions;
3998 for (outgoing_transitions_const_it_lb
3999 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4002 finalise_work(check_complexity::
4003 simple_splitB_U_handle_transition_from_potential_U_state,
4005 simple_splitB_handle_transition_from_R_or_U_state,
4010 if (AvoidLrg==current_search)
4018 for (
const state_in_block_pointer_lb*
4019 s=bi.sta.rt_non_bottom_states; s!=bi.end_states; ++s)
4022 const outgoing_transitions_const_it_lb out_ti_end=
4023 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
4024 : std::next(s->ref_state)->start_outgoing_transitions;
4025 for (outgoing_transitions_const_it_lb
4026 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4028 mCRL2complexity(&m_transitions[*ti->ref_BLC_transitions], finalise_work
4030 simple_splitB_U_handle_transition_from_potential_U_state,
4032 simple_splitB_test_outgoing_transitions_found_new_bottom_state,
4044 if (3>no_of_finished_searches)
4047 assert(finished!=status_NewBotSt);
4059 +bri.potential_non_bottom_states[current_search].size()
4060 -non_bottom_states[current_search].size());
4062 for (state_in_block_pointer_lb st:
4063 bri.potential_non_bottom_states[current_search])
4067 if (marked_NewBotSt != st.ref_state->counter)
4068 { assert(is_in_marked_range_of(st.ref_state->counter, current_search));
4069 if (marked(current_search)!=st.ref_state->counter)
4071 assert(!non_bottom_states[ReachAlw].find(st));
4080 st.ref_state->counter = marked_NewBotSt; assert(!non_bottom_states[AvoidSml].find(st));
4081 }
else { assert(non_bottom_states[current_search].find(st)); }
4082 }
else { assert(!non_bottom_states[current_search].find(st)); }
4083 } assert(running_searches[current_search_index]==current_search);
4084 clear(bri.potential_non_bottom_states[current_search]);
4085 --no_of_running_searches; assert(current_search_index<=no_of_running_searches);
4086 running_searches[current_search_index]=
4087 running_searches[no_of_running_searches];
4088 --current_search_index;
4090 if (finished==status[ReachAlw] &&
4091 finished==status[AvoidLrg] &&
4092 aborted!=status_NewBotSt)
4093 { assert(1>=no_of_running_searches);
4095 assert(finished!=status[AvoidSml]);
4096 assert(finished!=status_NewBotSt);
4097 for (state_in_block_pointer_lb st:
4098 bri.potential_non_bottom_states_HitSmall)
4099 { assert(0<st.ref_state->no_of_outgoing_block_inert_transitions);
4103 assert(!non_bottom_states[AvoidSml].find(st));
4104 if (marked_HitSmall == st.ref_state->counter)
4107 st.ref_state->counter = marked_NewBotSt; assert(!non_bottom_states[AvoidLrg].find(st));
4108 }
else { assert(marked(ReachAlw)==st.ref_state->counter ||
4109 marked(AvoidLrg)==st.ref_state->counter ||
4110 marked_NewBotSt==st.ref_state->counter); }
4112 clear(bri.potential_non_bottom_states_HitSmall);
4114 if (std::numeric_limits<state_index>::max()!=
4115 no_of_unfinished_states_in_block)
4116 { assert(0<no_of_running_searches); assert(no_of_running_searches<=2);
4117 assert(aborted!=status[ReachAlw]); assert(aborted!=status[AvoidLrg]);
4118 no_of_unfinished_states_in_block-=
4120 assert(finished!=status[running_searches[0]]);
4121 assert(aborted!=status[AvoidSml]); assert(aborted!=status_NewBotSt);
4130 running_searches[0]=running_searches[1];
4131 if (0==current_search_index)
4133 --current_search_index;
4135 --no_of_running_searches;
4137 else if (1<no_of_running_searches && ( assert(aborted!=status[running_searches[1]]),
4138 assert(finished!=status[running_searches[1]]),
4145 --no_of_running_searches; assert(1==no_of_running_searches);
4156 assert(finished==status[AvoidSml]); assert(finished==status[AvoidLrg]);
4157 assert(finished==status[ReachAlw]);
4159 state_in_block_pointer_lb* new_start_bottom_states_plus_one[3];
4160 state_in_block_pointer_lb* new_end_bottom_states_plus_one[2];
4161 #define new_start_bottom_states(idx) (assert
(1
<=(idx)), assert
((idx)<=3
), new_start_bottom_states_plus_one[(idx)-1
])
4162 #define new_end_bottom_states(idx) (assert
(1
<=(idx)), assert
((idx)<=2
), new_end_bottom_states_plus_one[(idx)-1
])
4163 #define new_end_bottom_states_NewBotSt (new_start_bottom_states_plus_one[2
])
4166 bri.start_bottom_states[ReachAlw+1] +
4167 non_bottom_states[ReachAlw].size();
4172 non_bottom_states[AvoidSml].size();
4176 non_bottom_states[AvoidLrg].size();
4177 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4181 check_complexity::check_waiting_cycles();
4184 if (
nullptr != bri.large_splitter) {
4187 for (
const state_in_block_pointer_lb*
4188 s=bi.start_bottom_states; s!=bi.sta.rt_non_bottom_states; ++s)
4191 const outgoing_transitions_it_lb out_ti_end=
4192 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
4193 : std::next(s->ref_state)->start_outgoing_transitions;
4194 for (outgoing_transitions_it_lb
4195 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4198 cancel_work(check_complexity::
4199 simple_splitB_R_handle_transition_from_R_state), *
this);
4203 for (
const state_in_block_pointer_lb*
4204 s=bi.sta.rt_non_bottom_states; s!=bi.end_states; ++s)
4207 (check_complexity::simple_splitB_R_find_predecessors), *
this);
4209 const std::vector<transition>::iterator in_ti_end=
4210 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
4211 : std::next(s->ref_state)->start_incoming_transitions;
4212 for (std::vector<transition>::iterator
4213 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
4215 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
4217 get_transitions().begin(), ti)], cancel_work(check_complexity::
4218 simple_splitB_R_handle_transition_to_R_state), *
this);
4220 if (
nullptr != bri.large_splitter) {
4222 const outgoing_transitions_it_lb out_ti_end=
4223 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
4224 : std::next(s->ref_state)->start_outgoing_transitions;
4225 for (outgoing_transitions_it_lb
4226 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4229 cancel_work(check_complexity::
4230 simple_splitB_R_handle_transition_from_R_state), *
this);
4235 check_complexity::check_temporary_work();
4240 constellation_type_lb& constellation=*bi.constellation;
4241 if (constellation.start_const_states->ref_state->block==
4242 std::prev(constellation.end_const_states)->ref_state->block)
4243 { assert(std::find(m_non_trivial_constellations.begin(),
4244 m_non_trivial_constellations.end(),
4245 &constellation)==m_non_trivial_constellations.end());
4246 m_non_trivial_constellations.emplace_back(&constellation);
4251 block_type_lb& NewBotSt_block = bi;
4257 clear_state_counters
4258 (bri.potential_non_bottom_states[current_search].begin(),
4259 bri.potential_non_bottom_states[current_search].end(), bi);
4260 clear(bri.potential_non_bottom_states[current_search]); assert(bri.potential_non_bottom_states[ReachAlw].empty());
4261 assert(bri.potential_non_bottom_states[AvoidLrg].empty());
4262 assert(bri.potential_non_bottom_states[AvoidSml].empty());
4268 clear_state_counters
4269 (bri.potential_non_bottom_states_HitSmall.begin(),
4270 bri.potential_non_bottom_states_HitSmall.end(), bi);
4271 clear(bri.potential_non_bottom_states_HitSmall);
4272 static_assert(2==AvoidLrg); assert(finished==status[AvoidLrg]);
4273 block_type_lb* AvoidLrg_block_index = null_block_lb;
4277 move_nonbottom_states_to(
4278 non_bottom_states[AvoidLrg],
4280 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4281 , bri.bottom_size(AvoidLrg)
4284 if (bri.start_bottom_states[AvoidLrg]!=
4287 multiple_swap_states_in_states_in_block
4288 (bri.start_bottom_states[AvoidLrg],
4290 bri.bottom_size(AvoidLrg)
4291 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4292 , bri.start_bottom_states[AvoidLrg],
4293 check_complexity::log_n-
4298 non_bottom_states[AvoidLrg].clear();
4299 AvoidLrg_block_index = create_new_block
4303 check_incoming_tau_transitions_become_noninert
4308 assert(0==bri.bottom_size(AvoidLrg));
4309 assert(non_bottom_states[AvoidLrg].empty());
4311 static_assert(1==AvoidSml); assert(finished==status[AvoidSml]);
4312 block_type_lb* AvoidSml_block_index = null_block_lb;
4315 { assert(0<bri.bottom_size(AvoidSml));
4316 move_nonbottom_states_to(
4317 non_bottom_states[AvoidSml],
4319 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4320 , bri.bottom_size(AvoidSml)
4323 if (bri.start_bottom_states[AvoidSml]!=
4326 multiple_swap_states_in_states_in_block
4327 (bri.start_bottom_states[AvoidSml],
4329 bri.bottom_size(AvoidSml)
4330 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4331 , bri.start_bottom_states[AvoidSml],
4332 check_complexity::log_n-
4337 non_bottom_states[AvoidSml].clear();
4338 AvoidSml_block_index = create_new_block
4342 check_incoming_tau_transitions_become_noninert
4347 assert(0==bri.bottom_size(AvoidSml));
4348 assert(non_bottom_states[AvoidSml].empty());
4350 static_assert(0==ReachAlw); assert(finished==status[ReachAlw]);
4351 block_type_lb* ReachAlw_block_index = null_block_lb;
4352 if (bri.start_bottom_states[ReachAlw]!=
4354 { assert(0<bri.bottom_size(ReachAlw));
4355 move_nonbottom_states_to(non_bottom_states[ReachAlw],
4356 bri.start_bottom_states[ReachAlw+1]
4357 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4358 , bri.bottom_size(ReachAlw)
4361 non_bottom_states[ReachAlw].clear();
4362 ReachAlw_block_index=create_new_block
4363 (bri.start_bottom_states[ReachAlw],
4364 bri.start_bottom_states[ReachAlw+1],
4366 check_incoming_tau_transitions_become_noninert
4368 bri.start_bottom_states[ReachAlw],
4371 assert(0==bri.bottom_size(ReachAlw));
4372 assert(non_bottom_states[ReachAlw].empty());
4374 #ifdef MORE_STATISTICS
4375 if (null_block_lb != AvoidLrg_block_index)
4377 update_sample_counter_for_new_block(*AvoidLrg_block_index, bi);
4379 if (null_block_lb != AvoidSml_block_index)
4381 update_sample_counter_for_new_block(*AvoidSml_block_index, bi);
4383 if (null_block_lb != ReachAlw_block_index)
4385 update_sample_counter_for_new_block(*ReachAlw_block_index, bi);
4386 } assert(&bi==bri.transition_count_sample_state->block);
4387 swap_states_in_states_in_block(bi.start_bottom_states,
4388 bri.transition_count_sample_state->ref_states_in_blocks); assert(0==bri.transition_count_sample_state->
4389 no_of_outgoing_block_inert_transitions);
4391 (
void) AvoidLrg_block_index;
4392 (
void) AvoidSml_block_index;
4394 assert(NewBotSt_block.start_bottom_states<
4395 NewBotSt_block.sta.rt_non_bottom_states);
4396 if (1 < number_of_states_in_block(NewBotSt_block))
4398 NewBotSt_block.contains_new_bottom_states =
true;
4399 m_blocks_with_new_bottom_states.push_back(&NewBotSt_block);
4401 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4402 assert(null_block_lb==m_singleton_block_with_new_bottom_states_for_debug);
4403 m_singleton_block_with_new_bottom_states_for_debug = &NewBotSt_block;
4407 update_all_small_subblock_counters
4408 (bri.start_bottom_states[ReachAlw], bi.end_states);
4409 return ReachAlw_block_index;
4410 #undef new_start_bottom_states
4411 #undef new_end_bottom_states
4412 #undef new_end_bottom_states_NewBotSt
4418 if (incoming_inert_transition_checking==status_NewBotSt)
4419 { assert(current_source_iter_NewBotSt<current_source_iter_end_NewBotSt);
4420 mCRL2complexity(&m_transitions[std::distance(m_aut.get_transitions().begin(),
4421 current_source_iter_NewBotSt)], add_work(check_complexity::
4422 simple_splitB_R_handle_transition_to_R_state, 1), *
this);
4423 const transition& tr=*current_source_iter_NewBotSt++; assert(m_aut.is_tau(m_aut_apply_hidden_label_map(tr.label())));
4424 state_in_block_pointer_lb
const src=m_states.begin()+
static_cast<std::ptrdiff_t>(tr.from()); assert(m_states[tr.to()].block==&bi);
4426 if (src.ref_state->block==&bi &&
4427 !(m_preserve_divergence && tr.from()==tr.to()))
4430 if (marked_NewBotSt != src.ref_state->counter)
4442 src.ref_state->counter = marked_NewBotSt;
4446 if (current_source_iter_NewBotSt==current_source_iter_end_NewBotSt ||
4447 !m_aut.is_tau(m_aut_apply_hidden_label_map
4448 (current_source_iter_NewBotSt->label())))
4450 status_NewBotSt=state_checking;
4453 else if (state_checking==status_NewBotSt)
4458 state_in_block_pointer_lb
4461 add_work(check_complexity::simple_splitB_R_find_predecessors, 1), *
this);
4462 current_source_iter_NewBotSt=
4463 tgt.ref_state->start_incoming_transitions;
4464 current_source_iter_end_NewBotSt=
4465 std::next(tgt.ref_state)>=m_states.end()
4466 ? m_aut.get_transitions().end()
4467 : std::next(tgt.ref_state)->start_incoming_transitions;
4468 if(current_source_iter_NewBotSt<current_source_iter_end_NewBotSt &&
4469 m_aut.is_tau(m_aut_apply_hidden_label_map
4470 (current_source_iter_NewBotSt->label())))
4472 status_NewBotSt=incoming_inert_transition_checking;
4477 if (1>=no_of_finished_searches)
4479 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4480 check_complexity::wait();
4488 if (finished != status[AvoidLrg] &&
4489 large_splitter_iter_NewBotSt!=large_splitter_iter_end_NewBotSt &&
4490 !large_splitter_is_known_to_be_a_strict_BLC_set)
4491 { assert(large_splitter_iter_NewBotSt==bri.large_splitter->start_same_BLC);
4492 assert(large_splitter_iter_end_NewBotSt== (bri.large_splitter->is_stable()
4493 ? bri.large_splitter->end_same_BLC : bri.large_splitter->start_marked_BLC));
4494 if(&bi!=bi.block_BLC_source->start_BLC_source->ref_state->block ||
4495 &bi!=bi.block_BLC_source->end_BLC_source[-1].ref_state->block)
4500 if (0<bi.small_subblock_counter)
4502 #ifdef MORE_STATISTICS
4503 ++number_of_large_splitters_searched_in_small_subblocks;
4505 --bi.small_subblock_counter;
4507 const transition& large_tr =
4508 m_aut.get_transitions()[*large_splitter_iter_NewBotSt];
4509 const label_index large_a = label_or_divergence(large_tr);
4510 const constellation_type_lb*
const large_to_constln =
4511 m_states[large_tr.to()].block->constellation;
4513 state_in_block_pointer_lb*sta_it=bi.sta.rt_non_bottom_states; assert(sta_it < bi.end_states);
4516 if (sta_it->ref_state->counter % marked_range !=
4517 marked((
enum subblocks) 0))
4518 { assert(marked(ReachAlw)!=sta_it->ref_state->counter);
4519 assert(marked(AvoidSml)!=sta_it->ref_state->counter);
4520 assert(marked(AvoidLrg)!=sta_it->ref_state->counter);
4521 assert(marked_NewBotSt !=sta_it->ref_state->counter);
4522 outgoing_transitions_const_it_lb
const out_it_end =
4523 std::next(sta_it->ref_state)>=m_states.end()
4524 ? m_outgoing_transitions.end()
4525 : std::next(sta_it->ref_state)->
4526 start_outgoing_transitions;
4527 outgoing_transitions_it_lb out_it=
4528 sta_it->ref_state->start_outgoing_transitions; assert(out_it < out_it_end);
4532 const transition& tr=m_aut.get_transitions()[*out_it->ref_BLC_transitions];
4534 if (large_splitter_iter_NewBotSt <=
4535 out_it->ref_BLC_transitions &&
4536 out_it->ref_BLC_transitions <
4537 large_splitter_iter_end_NewBotSt)
4539 assert(large_a == label_or_divergence(tr));
4540 assert(large_to_constln == m_states[tr.to()].block->constellation);
4546 sta_it->ref_state->counter = marked_NewBotSt;
4549 }
else { assert(large_a != label_or_divergence(tr) ||
4550 large_to_constln != m_states[tr.to()].block->constellation); }
4551 assert(out_it <= out_it->start_same_saC);
4552 out_it = std::next(out_it->start_same_saC);
4554 while (out_it < out_it_end);
4555 }
else { assert(marked(ReachAlw)==sta_it->ref_state->counter ||
4556 marked(AvoidSml)==sta_it->ref_state->counter ||
4557 marked(AvoidLrg)==sta_it->ref_state->counter ||
4558 marked_NewBotSt ==sta_it->ref_state->counter); }
4561 while (sta_it < bi.end_states);
4562 large_splitter_iter_NewBotSt=large_splitter_iter_end_NewBotSt;
4572 state_in_block_pointer_lb
4575 add_work(check_complexity::simple_splitB_R_find_predecessors, 1), *
this);
4576 current_source_iter_NewBotSt=
4577 tgt.ref_state->start_incoming_transitions;
4578 current_source_iter_end_NewBotSt=
4579 std::next(tgt.ref_state)>=m_states.end()
4580 ? m_aut.get_transitions().end()
4581 : std::next(tgt.ref_state)->start_incoming_transitions;
4582 if (current_source_iter_NewBotSt <
4583 current_source_iter_end_NewBotSt &&
4584 m_aut.is_tau(m_aut_apply_hidden_label_map
4585 (current_source_iter_NewBotSt->label())))
4587 status_NewBotSt=incoming_inert_transition_checking;
4594 { assert(null_constellation_lb != old_constellation);
4595 assert(null_constellation_lb != new_constellation);
4596 #ifdef MORE_STATISTICS
4597 ++number_of_large_splitters_searched_in_large_subblocks;
4599 make_BLC_simple(bi,
false,old_constellation,new_constellation);
4600 if (
nullptr == bri.large_splitter)
4604 large_splitter_iter_NewBotSt = m_BLC_transitions.data_end();
4605 large_splitter_iter_end_NewBotSt =
4606 m_BLC_transitions.data_end();
4610 large_splitter_iter_NewBotSt =
4611 bri.large_splitter->start_same_BLC;
4612 large_splitter_iter_end_NewBotSt =
4613 bri.large_splitter->is_stable()
4614 ? bri.large_splitter->end_same_BLC
4615 : bri.large_splitter->start_marked_BLC;
4619 large_splitter_is_known_to_be_a_strict_BLC_set =
true;
4621 if (finished != status[AvoidLrg] &&
4622 large_splitter_iter_NewBotSt!=large_splitter_iter_end_NewBotSt)
4623 { assert(finished==status[ReachAlw]); assert(finished==status[AvoidSml]);
4631 t=m_aut.get_transitions()[*large_splitter_iter_NewBotSt];
mCRL2complexity(&m_transitions[*large_splitter_iter_NewBotSt],
4632 add_work(check_complexity::
4633 simple_splitB_R_handle_transition_from_R_state, 1), *
this);
4634 ++large_splitter_iter_NewBotSt;
4635 state_in_block_pointer_lb src = m_states.begin() + t.from(); assert(src.ref_state->block==&bi);
4637 if (0==src.ref_state->no_of_outgoing_block_inert_transitions)
4638 { assert(!(bri.start_bottom_states[AvoidLrg]<=src.ref_state->ref_states_in_blocks &&
4639 src.ref_state->ref_states_in_blocks<bri.start_bottom_states[AvoidLrg+1]));
4644 if (undefined==src.ref_state->counter ||
4645 is_in_marked_range_of(src.ref_state->counter, AvoidLrg))
4646 { assert(!non_bottom_states[ReachAlw].find(src));
4647 assert(!non_bottom_states[AvoidSml].find(src));
4648 assert(!non_bottom_states[AvoidLrg].find(src));
4651 src.ref_state->counter = marked_NewBotSt;
4653 if (0==no_of_running_searches)
4667 }
else { assert(marked_HitSmall!=src.ref_state->counter); }
4669 if (0!=no_of_running_searches)
4674 while ( assert(0==no_of_running_searches), assert(aborted==status[AvoidLrg]),
4675 large_splitter_iter_NewBotSt!=large_splitter_iter_end_NewBotSt);
4680 check_complexity::check_waiting_cycles();
4702 status_NewBotSt=finished; ++no_of_finished_searches; assert(3==no_of_finished_searches);
4707 state_in_block_pointer_lb* new_start_bottom_states_plus_one[3];
4708 state_in_block_pointer_lb* new_end_bottom_states_plus_one[2];
4709 #define new_start_bottom_states(idx) (assert
(1
<=(idx)), assert
((idx)<=3
), new_start_bottom_states_plus_one[(idx)-1
])
4710 #define new_end_bottom_states(idx) (assert
(1
<=(idx)), assert
((idx)<=2
), new_end_bottom_states_plus_one[(idx)-1
])
4711 #define new_end_bottom_states_NewBotSt (new_start_bottom_states_plus_one[2
])
4716 if (finished == status[AvoidLrg])
4720 non_bottom_states[AvoidLrg].size();
4723 if (finished==status[AvoidSml])
4724 { assert(finished==status[AvoidSml]); assert(finished!=status[ReachAlw]);
4727 non_bottom_states[AvoidSml].size();
4731 non_bottom_states[ReachAlw].clear();
4732 clear_state_counters
4733 (bri.potential_non_bottom_states[ReachAlw].begin(),
4734 bri.potential_non_bottom_states[ReachAlw].end(), bi);
4735 clear(bri.potential_non_bottom_states[ReachAlw]);
4738 if (
nullptr != bri.large_splitter)
4740 clear_state_counters
4741 (bri.potential_non_bottom_states_HitSmall.begin(),
4742 bri.potential_non_bottom_states_HitSmall.end(), bi);
4743 }
else { assert(bri.potential_non_bottom_states_HitSmall.empty()); }
4746 { assert(finished==status[ReachAlw]);
4748 bri.start_bottom_states[ReachAlw+1]+
4749 non_bottom_states[ReachAlw].size();
4753 non_bottom_states[AvoidSml].clear();
4754 clear_state_counters
4755 (bri.potential_non_bottom_states[AvoidSml].begin(),
4756 bri.potential_non_bottom_states[AvoidSml].end(), bi);
4757 clear(bri.potential_non_bottom_states[AvoidSml]);
4763 { assert(finished==status[ReachAlw]);
4765 bri.start_bottom_states[ReachAlw+1]+
4766 non_bottom_states[ReachAlw].size(); assert(finished==status[AvoidSml]);
4771 non_bottom_states[AvoidSml].size();
4775 non_bottom_states[AvoidLrg].clear();
4776 clear_state_counters
4777 (bri.potential_non_bottom_states[AvoidLrg].begin(),
4778 bri.potential_non_bottom_states[AvoidLrg].end(), bi);
4779 clear(bri.potential_non_bottom_states[AvoidLrg]);
4781 clear_state_counters
4782 (bri.potential_non_bottom_states_HitSmall.begin(),
4783 bri.potential_non_bottom_states_HitSmall.end(), bi);
4785 clear(bri.potential_non_bottom_states_HitSmall);
4786 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4795 state_index max_NcludeCo_size=std::distance
4797 max_NcludeCo_size=std::max<state_index>(max_NcludeCo_size, std::distance(
4799 max_NcludeCo_size=std::max<state_index>(max_NcludeCo_size, std::distance(
4801 const unsigned char max_NcludeCo_B = 0==max_NcludeCo_size ? 0
4802 : check_complexity::log_n-check_complexity::ilog2(max_NcludeCo_size);
4803 const state_in_block_pointer_lb* s=bi.start_bottom_states;
4806 (check_complexity::simple_splitB_U_find_predecessors), *
this);
4808 const std::vector<transition>::const_iterator in_ti_end=
4809 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
4810 : std::next(s->ref_state)->start_incoming_transitions;
4811 for (std::vector<transition>::const_iterator
4812 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
4814 if(!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
4816 cbegin(), ti)], cancel_work(check_complexity::
4817 simple_splitB_U_handle_transition_to_U_state), *
this);
4819 if (finished!=status[AvoidLrg]) {
4821 const outgoing_transitions_const_it_lb out_ti_end=
4822 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
4823 : std::next(s->ref_state)->start_outgoing_transitions;
4824 for (outgoing_transitions_const_it_lb
4825 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4828 cancel_work(check_complexity::
4829 simple_splitB_U_handle_transition_from_potential_U_state), *
this);
4833 finalise_work(check_complexity::
4834 simple_splitB_R_handle_transition_from_R_state,
4836 simple_splitB_handle_transition_from_R_or_U_state,
4837 max_NcludeCo_B), *
this);
4840 }
while (++s!=bi.end_states);
4854 constellation_type_lb& constellation=*bi.constellation;
4855 if (constellation.start_const_states->ref_state->block==
4856 std::prev(constellation.end_const_states)->ref_state->block)
4857 { assert(std::find(m_non_trivial_constellations.begin(),
4858 m_non_trivial_constellations.end(),
4859 &constellation)==m_non_trivial_constellations.end());
4860 m_non_trivial_constellations.emplace_back(&constellation);
4865 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4870 block_type_lb& NewBotSt_block=
4874 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4879 const unsigned char max_new_B=check_complexity::log_n-check_complexity::ilog2
4884 simple_splitB_R_find_predecessors, check_complexity::
4885 simple_splitB_find_predecessors_of_R_or_U_state, max_new_B), *
this);
4887 const std::vector<transition>::iterator in_ti_end=
4888 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
4889 : std::next(s->ref_state)->start_incoming_transitions;
4890 for (std::vector<transition>::iterator
4891 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
4893 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
4895 begin(), ti)], finalise_work(check_complexity::
4896 simple_splitB_R_handle_transition_to_R_state, check_complexity::
4897 simple_splitB_handle_transition_to_R_or_U_state, max_new_B), *
this);
4901 }
while (s!=bi.end_states);
4903 check_complexity::check_temporary_work();
4906 assert(nst_it!=bi.end_states);
4909 outgoing_transitions_const_it_lb
const
4910 out_it_end = std::next(nst_it->ref_state)>=m_states.end()
4911 ? m_outgoing_transitions.end()
4912 : std::next(nst_it->ref_state)->start_outgoing_transitions;
4913 outgoing_transitions_it_lb out_it=
4914 nst_it->ref_state->start_outgoing_transitions; assert(out_it!=out_it_end);
4915 const transition* tr=&m_aut.get_transitions()
4916 [*out_it->ref_BLC_transitions]; assert(0<nst_it->ref_state->no_of_outgoing_block_inert_transitions);
4918 { assert(m_states.begin()+tr->from()==nst_it->ref_state);
4919 assert(m_aut.is_tau(m_aut_apply_hidden_label_map(tr->label())));
4920 if (m_states[tr->to()].block==&bi)
4921 { assert(is_inert_during_init(*tr));
4922 assert(bi.start_bottom_states<=m_states[tr->to()].ref_states_in_blocks);
4925 assert(0<nst_it->ref_state->no_of_outgoing_block_inert_transitions);
4926 if (0== --nst_it->ref_state->
4927 no_of_outgoing_block_inert_transitions)
4930 change_non_bottom_state_to_bottom_state
4931 (nst_it->ref_state);
4936 m_states[tr->to()].ref_states_in_blocks ||
4937 m_states[tr->to()].ref_states_in_blocks<bri.start_bottom_states[ReachAlw]);
4941 while (out_it!=out_it_end &&
4942 (tr=&m_aut.get_transitions()[*out_it->ref_BLC_transitions],
4943 m_aut.is_tau(m_aut_apply_hidden_label_map(tr->label()))));
4946 while (nst_it!=bi.end_states); assert(NewBotSt_block.start_bottom_states<
4947 NewBotSt_block.sta.rt_non_bottom_states);
4948 if (1 < number_of_states_in_block(NewBotSt_block))
4950 NewBotSt_block.contains_new_bottom_states=
true;
4951 m_blocks_with_new_bottom_states.push_back(&NewBotSt_block);
4953 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4954 assert(null_block_lb==m_singleton_block_with_new_bottom_states_for_debug);
4955 m_singleton_block_with_new_bottom_states_for_debug = &NewBotSt_block;
4958 #ifdef MORE_STATISTICS
4959 update_sample_counter_for_new_block(NewBotSt_block, bi);
4966 check_complexity::check_temporary_work();
4968 assert(bri.start_bottom_states[AvoidSml]<bri.start_bottom_states[AvoidLrg+1]);
4969 if (bri.start_bottom_states[ReachAlw] ==
4970 bri.start_bottom_states[ReachAlw+1] &&
4971 (bri.start_bottom_states[AvoidSml] ==
4972 bri.start_bottom_states[AvoidSml+1] ||
4973 bri.start_bottom_states[AvoidLrg] ==
4974 bri.start_bottom_states[AvoidLrg+1]))
4987 if (constellation.start_const_states->ref_state->block==
4988 std::prev(constellation.end_const_states)->ref_state->block)
4989 { assert(std::find(m_non_trivial_constellations.begin(),
4990 m_non_trivial_constellations.end(),
4991 &constellation)==m_non_trivial_constellations.end());
4992 m_non_trivial_constellations.emplace_back(&constellation); assert((bri.start_bottom_states[ReachAlw]!=
new_start_bottom_states(ReachAlw+1))+
4999 } assert(finished!=status[AvoidLrg] ||
static_cast<state_index>(std::distance
5004 { assert(0!=bri.bottom_size(AvoidLrg));
5005 if (bri.start_bottom_states[AvoidLrg]!=
5008 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5009 const state_in_block_pointer_lb* acct_iter;
5010 state_index acct_B_size;
5011 if (finished==status[AvoidLrg]) {
5012 acct_iter=bri.start_bottom_states[AvoidLrg];
5017 assert(non_bottom_states[AvoidLrg].empty());
5018 assert(finished==status[ReachAlw]); assert(finished==status[AvoidSml]);
5019 state_index count=std::min<state_index>(bri.bottom_size(AvoidLrg),
5020 std::distance(bri.start_bottom_states[AvoidLrg],
5022 if (non_bottom_states[AvoidSml].size()>=count) {
5023 acct_iter=non_bottom_states[AvoidSml].data();
5025 }
else if (non_bottom_states[ReachAlw].size()>=count) {
5026 acct_iter=non_bottom_states[ReachAlw].data();
5029 assert(count<=non_bottom_states[AvoidSml].size()+
5030 non_bottom_states[ReachAlw].size());
5033 non_bottom_states[AvoidLrg]=non_bottom_states[AvoidSml];
5034 non_bottom_states[AvoidLrg].add_todo(non_bottom_states[ReachAlw].begin(),
5035 non_bottom_states[ReachAlw].begin()
5036 +
static_cast<std::ptrdiff_t>(count-non_bottom_states[AvoidLrg].size()));
5037 acct_iter=non_bottom_states[AvoidLrg].data();
5041 } assert(0<acct_B_size);
5043 multiple_swap_states_in_states_in_block
5044 (bri.start_bottom_states[AvoidLrg],
5046 bri.bottom_size(AvoidLrg)
5047 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5048 , acct_iter, check_complexity::log_n-check_complexity::ilog2(acct_B_size),
5049 finished==status[AvoidLrg]
5050 ?check_complexity::multiple_swap_states_in_block_swap_state_in_small_block
5052 multiple_swap_states_in_block_account_for_swap_in_aborted_block
5057 if (finished==status[AvoidLrg])
5058 { assert(bri.potential_non_bottom_states[AvoidLrg].empty());
5059 move_nonbottom_states_to(non_bottom_states[AvoidLrg],
5061 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5062 , bri.bottom_size(AvoidLrg)
5065 non_bottom_states[AvoidLrg].clear();
5066 block_type_lb& AvoidLrg_block = *create_new_block
5070 #ifdef MORE_STATISTICS
5071 update_sample_counter_for_new_block(AvoidLrg_block, bi);
5073 (
void) AvoidLrg_block;
5078 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5081 non_bottom_states[AvoidLrg].clear();
5084 bi.sta.rt_non_bottom_states =
new_end_bottom_states(AvoidLrg); assert(bi.start_bottom_states<bi.sta.rt_non_bottom_states);
5090 assert(0==bri.bottom_size(AvoidLrg));assert(non_bottom_states[AvoidLrg].empty());
5091 assert(finished==status[AvoidLrg]);
5093 assert(finished!=status[AvoidSml] ||
static_cast<state_index>(std::distance
5098 { assert(0!=bri.bottom_size(AvoidSml));
5102 if (bri.start_bottom_states[AvoidSml]!=
5105 multiple_swap_states_in_states_in_block
5106 (bri.start_bottom_states[AvoidSml],
5108 bri.bottom_size(AvoidSml)
5109 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5110 , finished==status[AvoidSml] ? bri.start_bottom_states[AvoidSml]
5111 : non_bottom_states[ReachAlw].data(),
5112 check_complexity::log_n-check_complexity::ilog2
5115 finished==status[AvoidSml]
5116 ?check_complexity::multiple_swap_states_in_block_swap_state_in_small_block
5118 multiple_swap_states_in_block_account_for_swap_in_aborted_block
5122 if (finished==status[AvoidSml])
5123 { assert(bri.potential_non_bottom_states[AvoidSml].empty());
5124 move_nonbottom_states_to(non_bottom_states[AvoidSml],
5126 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5127 , bri.bottom_size(AvoidSml)
5130 non_bottom_states[AvoidSml].clear();
5131 block_type_lb& AvoidSml_block = *create_new_block
5135 #ifdef MORE_STATISTICS
5136 update_sample_counter_for_new_block(AvoidSml_block, bi);
5138 (
void) AvoidSml_block;
5144 bi.sta.rt_non_bottom_states =
new_end_bottom_states(AvoidSml); assert(bi.start_bottom_states<bi.sta.rt_non_bottom_states);
5150 assert(0==bri.bottom_size(AvoidSml));
5151 assert(non_bottom_states[AvoidSml].empty());
5152 assert(finished==status[AvoidSml]);
5154 assert(finished!=status[ReachAlw] ||
static_cast<state_index>(std::distance
5157 block_type_lb* ReachAlw_block_index = null_block_lb;
5158 if (bri.start_bottom_states[ReachAlw]!=
5160 { assert(0<bri.bottom_size(ReachAlw));
5161 if (finished==status[ReachAlw])
5162 { assert(bri.potential_non_bottom_states[ReachAlw].empty());
5163 move_nonbottom_states_to(non_bottom_states[ReachAlw],
5164 bri.start_bottom_states[ReachAlw+1]
5165 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5166 , bri.bottom_size(ReachAlw)
5169 non_bottom_states[ReachAlw].clear();
5170 ReachAlw_block_index=create_new_block
5171 (bri.start_bottom_states[ReachAlw],
5172 bri.start_bottom_states[ReachAlw+1],
5174 #ifdef MORE_STATISTICS
5175 update_sample_counter_for_new_block(*ReachAlw_block_index,
5180 { assert(bi.start_bottom_states==bri.start_bottom_states[ReachAlw]);
5181 bi.sta.rt_non_bottom_states =
5182 bri.start_bottom_states[ReachAlw+1]; assert(bi.start_bottom_states<bi.sta.rt_non_bottom_states);
5184 ReachAlw_block_index=&bi;
5187 assert(0==bri.bottom_size(ReachAlw));assert(non_bottom_states[ReachAlw].empty());
5189 #ifdef MORE_STATISTICS
5190 swap_states_in_states_in_block(bi.start_bottom_states,
5191 bri.transition_count_sample_state->ref_states_in_blocks); assert(&bi==bri.transition_count_sample_state->block);
5192 assert(0==bri.transition_count_sample_state->
5193 no_of_outgoing_block_inert_transitions);
5196 update_all_small_subblock_counters
5197 (bri.start_bottom_states[ReachAlw], nst_it);
5198 return ReachAlw_block_index;
5199 #undef new_start_bottom_states
5200 #undef new_end_bottom_states
5201 #undef new_end_bottom_states_NewBotSt
5204 assert(aborted==status_NewBotSt);
5208 #undef abort_if_bottom_size_too_large
5209 #undef abort_if_non_bottom_size_too_large_NewBotSt
5210 #undef abort_if_size_too_large
5211 #undef bottom_and_non_bottom_size
5212 #undef non_bottom_states_NewBotSt
5222 transition_index accumulate_entries(
5223 std::vector<transition_index>& action_counter,
5224 const std::vector<label_index>& todo_stack)
const
5226 transition_index sum=0;
5227 for(label_index index: todo_stack)
5229 transition_index n=sum;
5230 sum=sum+action_counter[index];
5231 action_counter[index]=n;
5241 #ifdef MORE_STATISTICS
5242 state_index number_of_small_bottom_block_refinements = 0;
5243 state_index number_of_large_bottom_block_refinements = 0;
5264 if (m_blocks_with_new_bottom_states.empty())
5267 } assert(m_branching);
5270 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> > Qhat;
5271 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5272 std::vector<std::pair<BLC_list_const_iterator, BLC_list_const_iterator> >
5273 initialize_qhat_work_to_assign_later;
5274 std::vector<std::pair<BLC_list_const_iterator, BLC_list_const_iterator> >
5275 stabilize_work_to_assign_later;
5280 assert(!m_blocks_with_new_bottom_states.empty());
5281 for(block_type_lb*
const bi: m_blocks_with_new_bottom_states)
5282 { assert(bi->contains_new_bottom_states);
5283 assert(1 < number_of_states_in_block(*bi));
5284 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5288 const state_in_block_pointer_lb* new_bott_it=bi->start_bottom_states;
5289 assert(new_bott_it < bi->sta.rt_non_bottom_states);
5293 add_work(check_complexity::stabilizeB_prepare_block, 1), *
this);
5295 while (++new_bott_it<bi->sta.rt_non_bottom_states);
5297 assert(!bi->block_BLC_source->block_to_constellation.empty());
5298 if (0==bi->small_subblock_counter &&
5299 bi->sta.rt_non_bottom_states < bi->end_states)
5314 make_BLC_simple(*bi);
5320 for(block_type_lb*
const bi: m_blocks_with_new_bottom_states)
5321 { assert(bi->contains_new_bottom_states);
5324 bi->contains_new_bottom_states=
false; assert(!bi->block_BLC_source->block_to_constellation.empty());
5325 simple_list<BLC_indicators_lb>& btc =
5326 bi->block_BLC_source->block_to_constellation; assert(1 < number_of_states_in_block(*bi));
5328 if (0==bi->small_subblock_counter &&
5329 bi->sta.rt_non_bottom_states < bi->end_states)
5330 { assert(bi->block_BLC_source->start_BLC_source==bi->start_bottom_states);
5331 assert(bi->block_BLC_source->end_BLC_source==bi->end_states);
5332 typename simple_list<BLC_indicators_lb>::iterator ind=btc.begin(); assert(btc.end() != ind); assert(ind->start_same_BLC<ind->end_same_BLC);
5333 const transition& tr=m_aut.get_transitions()[*ind->start_same_BLC]; assert(m_states[tr.from()].block == bi);
5334 if (m_states[tr.to()].block->constellation == bi->constellation &&
5335 is_inert_during_init_if_branching(tr) &&
5336 (ind = btc.next(ind),
5344 { assert(btc.end() != ind);
5345 while (ind->is_stable())
5346 { assert(ind->start_same_BLC<ind->end_same_BLC);
5347 ind->starts_in_small_subblock =
false;
5348 ind->make_unstable();
5350 Qhat.emplace_back(ind->start_same_BLC, ind->end_same_BLC);
5351 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5354 bool work_assigned =
false;
5356 for (BLC_list_const_iterator work_it = ind->start_same_BLC;
5357 work_it < ind->end_same_BLC; ++work_it)
5360 const transition& tr = m_aut.get_transitions()[*work_it];
5361 assert(!is_inert_during_init(tr) ||
5362 m_states[tr.to()].block->constellation != bi->constellation);
5363 assert(m_states[tr.from()].block == bi);
5364 if (0==m_states[tr.from()].no_of_outgoing_block_inert_transitions)
5367 if (work_assigned) {
5369 check_complexity::stabilizeB_initialize_Qhat, 1), *
this);
5374 check_complexity::stabilizeB_initialize_Qhat, 1), *
this);
5375 work_assigned =
true;
5381 if (!work_assigned) {
5384 initialize_qhat_work_to_assign_later.emplace_back(ind->start_same_BLC,
5388 ind = btc.next(ind);
5389 if (btc.end() == ind)
5392 } assert(ind->start_same_BLC < ind->end_same_BLC);
5393 const transition& tr = m_aut.get_transitions()
5394 [*ind->start_same_BLC]; assert(m_states[tr.from()].block == bi);
5395 if(m_states[tr.to()].block->constellation==bi->constellation &&
5396 is_inert_during_init_if_branching(tr))
5398 assert(btc.begin() != ind);
5401 const simple_list<BLC_indicators_lb>::iterator
5402 next_ind = btc.next(ind);
5404 btc.splice(btc.begin(), btc, ind);
5408 if (btc.end() == ind)
5415 for (; btc.end() != ind; ++ind) {
5416 const transition& tr = m_aut.get_transitions()[*ind->start_same_BLC];
5417 assert(m_states[tr.from()].block == bi); assert(!ind->is_stable());
5418 assert(m_states[tr.to()].block->constellation != bi->constellation ||
5419 !is_inert_during_init(tr));
5424 state_in_block_pointer_lb* si=bi->start_bottom_states; assert(si<bi->sta.rt_non_bottom_states);
5427 check_complexity::stabilizeB_distribute_states_over_Phat, 1), *
this);
5428 outgoing_transitions_it_lb end_it=
5429 std::next(si->ref_state)>=m_states.end()
5430 ? m_outgoing_transitions.end()
5431 : std::next(si->ref_state)->start_outgoing_transitions; assert(si->ref_state->block==bi);
5432 for(outgoing_transitions_it_lb ti=
5433 si->ref_state->start_outgoing_transitions; ti<end_it; ++ti)
5436 const transition& t=
5437 m_aut.get_transitions()[*ti->ref_BLC_transitions]; assert(m_states.begin()+t.from()==si->ref_state);
5438 if(bi->constellation!=m_states[t.to()].block->constellation||
5439 !is_inert_during_init_if_branching(t))
5442 mark_BLC_transition(ti);
5443 }
else { assert(m_transitions[*ti->ref_BLC_transitions].
5444 transitions_per_block_to_constellation->is_stable()); }
5445 assert(ti <= ti->start_same_saC);
5446 ti = ti->start_same_saC;
5450 while (si<bi->sta.rt_non_bottom_states);
5455 if (bi->sta.rt_non_bottom_states < bi->end_states)
5459 --bi->small_subblock_counter;
5461 if (bi->start_bottom_states ==
5462 bi->block_BLC_source->start_BLC_source &&
5463 bi->end_states == bi->block_BLC_source->end_BLC_source)
5472 typename simple_list<BLC_indicators_lb>::iterator
5473 ind = btc.begin(); assert(btc.end() != ind);
5476 if (!ind->is_stable())
5480 const transition& tr = m_aut.get_transitions()[*ind->start_same_BLC];
5481 assert(m_states[tr.from()].block == bi); assert(!ind->is_stable());
5482 assert(m_states[tr.to()].block->constellation!=bi->constellation ||
5483 !is_inert_during_init(tr));
5485 assert(ind->starts_in_small_subblock);
5486 }
while(++ind != btc.end());
5490 const transition& tr = m_aut.get_transitions()
5491 [*ind->start_same_BLC]; assert(m_states[tr.from()].block == bi);
5492 const simple_list<BLC_indicators_lb>::iterator
5493 next_ind = btc.next(ind);
5494 if(m_states[tr.to()].block->constellation==bi->constellation &&
5495 is_inert_during_init_if_branching(tr))
5496 { assert(ind->is_stable());
5500 if (btc.begin() != ind)
5503 btc.splice(btc.begin(), btc, ind);
5513 ind->starts_in_small_subblock =
true;
5514 ind->start_marked_BLC = ind->start_same_BLC;
5516 Qhat.emplace_back(ind->start_same_BLC, ind->end_same_BLC);
5520 while (btc.end() != ind);
5530 state_in_block_pointer_lb* it = bi->start_bottom_states; assert(it < bi->end_states);
5534 outgoing_transitions_it_lb out_it =
5535 it->ref_state->start_outgoing_transitions;
5536 outgoing_transitions_const_it_lb
const
5537 out_it_end=std::next(it->ref_state)==m_states.end()
5538 ? m_outgoing_transitions.end()
5539 : std::next(it->ref_state)->start_outgoing_transitions; assert(out_it < out_it_end);
5542 BLC_list_iterator old_pos=out_it->ref_BLC_transitions;
5543 const transition& tr = m_aut.get_transitions()[*old_pos];
5544 if (m_states[tr.to()].block->constellation !=
5545 bi->constellation ||
5546 !is_inert_during_init_if_branching(tr))
5550 simple_list<BLC_indicators_lb>::iterator ind=m_transitions
5551 [*old_pos].transitions_per_block_to_constellation;
5552 if (ind->is_stable())
5554 ind->make_unstable();
5555 ind->starts_in_small_subblock =
true;
5557 btc.splice(btc.end(), btc, ind);
5559 Qhat.emplace_back(ind->start_same_BLC,ind->end_same_BLC);
5560 } assert(ind->starts_in_small_subblock);
5561 mark_BLC_transition(out_it);
5563 assert(out_it <= out_it->start_same_saC);
5565 out_it = std::next(out_it->start_same_saC);
5567 while (out_it < out_it_end);
5570 while (it < bi->end_states);
5576 clear(m_blocks_with_new_bottom_states);
5581 { assert(m_blocks_with_new_bottom_states.empty());
5583 { assert(check_data_structures(
"End of stabilizeB()"));
5584 assert(check_stability(
"End of stabilizeB()"));
5587 assert(initialize_qhat_work_to_assign_later.empty());
5588 assert(stabilize_work_to_assign_later.empty());
5592 print_data_structures(
"New bottom state loop");
5594 assert(check_data_structures(
"New bottom state loop",
false));
5595 std::pair<BLC_list_iterator,BLC_list_iterator>& Qhat_elt=Qhat.back(); assert(check_stability(
"New bottom state loop", &Qhat));
5596 assert(Qhat_elt.first<Qhat_elt.second);
5597 const simple_list<BLC_indicators_lb>::iterator
5598 splitter = m_transitions[*std::prev(Qhat_elt.second)].
5599 transitions_per_block_to_constellation; assert(splitter->end_same_BLC==Qhat_elt.second);
5602 Qhat_elt.second=splitter->start_same_BLC; assert(splitter->start_same_BLC<splitter->end_same_BLC);
5603 const transition& first_t=
5604 m_aut.get_transitions()[*splitter->start_same_BLC]; assert(!splitter->is_stable());
5605 block_type_lb& from_block_index=*m_states[first_t.from()].block; assert(!from_block_index.contains_new_bottom_states);
5606 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5609 BLC_list_const_iterator work_it=splitter->start_marked_BLC;
5610 if (work_it==splitter->end_same_BLC && splitter->starts_in_small_subblock) {
5615 mCRL2log(log::warning) <<
"Cannot find a way to prove the timing bound on "
5616 << splitter->debug_id(*
this) <<
'\n';
5618 bool work_assigned=
false;
5619 for(; work_it!=splitter->end_same_BLC; ++work_it) {
5621 if (0==m_states[m_aut.get_transitions()[*work_it].from()].
5622 no_of_outgoing_block_inert_transitions)
5625 if (work_assigned) {
5627 check_complexity::stabilizeB_main_loop, 1), *
this);
5632 add_work(check_complexity::stabilizeB_main_loop, 1), *
this);
5639 if (!work_assigned) {
5642 stabilize_work_to_assign_later.emplace_back(splitter->start_same_BLC,
5643 splitter->end_same_BLC);
5647 BLC_source_type& BLC_source=*from_block_index.block_BLC_source;
5649 bool is_inert = is_inert_during_init(first_t);
5650 constellation_type_lb& to_constellation =
5651 *m_states[first_t.to()].block->constellation;
5657 for(BLC_list_iterator splitter_it = splitter->start_marked_BLC;
5658 splitter_it != splitter->end_same_BLC; ++splitter_it)
5660 const transition& t=m_aut.get_transitions()[*splitter_it]; assert(is_inert == is_inert_during_init(t));
5661 state_in_block_pointer_lb
const src = m_states.begin()+t.from(); assert(m_states[t.to()].block->constellation == &to_constellation);
5662 assert(BLC_source.start_BLC_source <= src.ref_state->ref_states_in_blocks);
5663 assert(src.ref_state->ref_states_in_blocks < BLC_source.end_BLC_source);
5664 block_type_lb& bi = *src.ref_state->block; assert(!is_inert || bi.constellation != &to_constellation);
5665 assert(!bi.contains_new_bottom_states);
5666 if (1 < number_of_states_in_block(bi))
5668 if (null_state == bi.refinement_info)
5672 bi.refinement_info = blocks_that_need_refinement.size();
5673 blocks_that_need_refinement.emplace_back(bi,
5674 splitter->starts_in_small_subblock ?
nullptr : &*splitter)
5676 .start_bottom_states[AvoidSml+1] = bi.start_bottom_states; assert(bi.refinement_info < blocks_that_need_refinement.size());
5678 block_that_needs_refinement_type& bri =
5679 blocks_that_need_refinement[bi.refinement_info]; assert(bri.start_bottom_states[AvoidSml] == bri.start_bottom_states[AvoidLrg]);
5680 if (0 == src.ref_state->no_of_outgoing_block_inert_transitions)
5681 { assert(bi.start_bottom_states<=src.ref_state->ref_states_in_blocks);
5682 assert(src.ref_state->ref_states_in_blocks<bi.sta.rt_non_bottom_states);
5683 if (src.ref_state->ref_states_in_blocks <
5684 bri.start_bottom_states[AvoidSml])
5690 static_assert(ReachAlw + 1 == AvoidSml);
5691 swap_states_in_states_in_block
5692 (bri.start_bottom_states[AvoidSml],
5693 src.ref_state->ref_states_in_blocks);
5694 bri.start_bottom_states[AvoidLrg] =
5695 ++bri.start_bottom_states[AvoidSml];
5699 { assert(splitter->starts_in_small_subblock);
5700 assert(
nullptr == bri.large_splitter);
5701 assert(bi.sta.rt_non_bottom_states<=src.ref_state->ref_states_in_blocks);
5702 assert(src.ref_state->ref_states_in_blocks<bi.end_states);
5703 if (undefined == src.ref_state->counter)
5706 src.ref_state->counter = marked(ReachAlw) +
5707 src.ref_state->no_of_outgoing_block_inert_transitions; assert(is_in_marked_range_of(src.ref_state->counter, ReachAlw));
5709 bri.potential_non_bottom_states[ReachAlw].push_back(src);
5711 assert(is_in_marked_range_of(src.ref_state->counter, ReachAlw));
5712 assert(std::find(bri.potential_non_bottom_states[ReachAlw].begin(),
5713 bri.potential_non_bottom_states[ReachAlw].end(), src)!=
5714 bri.potential_non_bottom_states[ReachAlw].end());
5717 }
else { assert(null_state == bi.refinement_info); }
5719 if (splitter->starts_in_small_subblock)
5721 make_stable_and_move_to_start_of_BLC(BLC_source, splitter);
5724 { assert(BLC_source.start_BLC_source == from_block_index.start_bottom_states);
5725 assert(BLC_source.end_BLC_source == from_block_index.end_states);
5729 if (blocks_that_need_refinement.empty())
5730 { assert(!from_block_index.contains_new_bottom_states);
5731 assert(number_of_states_in_block(from_block_index) > 1);
5732 assert(null_state == from_block_index.refinement_info);
5733 assert(!is_inert || from_block_index.constellation != &to_constellation);
5734 from_block_index.refinement_info = 0;
5736 blocks_that_need_refinement.emplace_back(from_block_index,
5738 .start_bottom_states[AvoidSml+1] =
5739 from_block_index.start_bottom_states; assert(from_block_index.refinement_info < blocks_that_need_refinement.size());
5740 } assert(std::next(blocks_that_need_refinement.begin()) ==
5741 blocks_that_need_refinement.end());
5745 while(!blocks_that_need_refinement.empty())
5747 block_that_needs_refinement_type& bri=
5748 blocks_that_need_refinement.back();
5749 block_type_lb& bi=*bri.start_bottom_states[0]->ref_state->block; assert(!bi.contains_new_bottom_states);
5750 bool bi_was_small_subblock = (
nullptr == bri.large_splitter); assert(&bri==&blocks_that_need_refinement[bi.refinement_info]);
5751 #ifdef MORE_STATISTICS
5752 if (bi_was_small_subblock)
5754 ++number_of_small_bottom_block_refinements;
5758 ++number_of_large_bottom_block_refinements;
5761 assert(1<number_of_states_in_block(bi));
5762 four_way_splitB(bri); assert(bi.refinement_info<blocks_that_need_refinement.size());
5763 assert(bi_was_small_subblock ==
5764 (
nullptr==blocks_that_need_refinement[bi.refinement_info].large_splitter));
5765 #ifdef MORE_STATISTICS
5766 assert(bi.start_bottom_states==blocks_that_need_refinement
5767 [bi.refinement_info].transition_count_sample_state->ref_states_in_blocks);
5769 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5770 if (null_block_lb != m_singleton_block_with_new_bottom_states_for_debug) {
5771 const state_index new_bottom_state_index = std::distance(m_states.begin(),
5772 m_singleton_block_with_new_bottom_states_for_debug->
5773 start_bottom_states->ref_state);
5777 for (std::vector<std::pair<BLC_list_const_iterator,BLC_list_const_iterator>
5778 >::iterator qhat_it=initialize_qhat_work_to_assign_later.begin();
5779 qhat_it!=initialize_qhat_work_to_assign_later.end(); )
5781 bool new_bottom_state_with_transition_found=
false;
5782 for (BLC_list_const_iterator work_it=qhat_it->first;
5783 work_it<qhat_it->second; ++work_it)
5785 if (new_bottom_state_index==m_aut.get_transitions()[*work_it].from()) {
5789 if (new_bottom_state_with_transition_found) {
5792 stabilizeB_initialize_Qhat_afterwards, 1), *
this);
5797 stabilizeB_initialize_Qhat_afterwards, 1), *
this);
5798 new_bottom_state_with_transition_found=
true;
5804 if (new_bottom_state_with_transition_found) {
5807 if (std::next(qhat_it)==initialize_qhat_work_to_assign_later.end()) {
5808 initialize_qhat_work_to_assign_later.pop_back();
5811 *qhat_it=initialize_qhat_work_to_assign_later.back();
5812 initialize_qhat_work_to_assign_later.pop_back();
5820 for (std::vector<std::pair<BLC_list_const_iterator,BLC_list_const_iterator>
5821 >::iterator stabilize_it=stabilize_work_to_assign_later.begin();
5822 stabilize_it!=stabilize_work_to_assign_later.end(); )
5824 bool new_bottom_state_with_transition_found=
false;
5825 for (BLC_list_const_iterator work_it=stabilize_it->first;
5826 work_it<stabilize_it->second; ++work_it)
5828 if (new_bottom_state_index==m_aut.get_transitions()[*work_it].from()) {
5832 if (new_bottom_state_with_transition_found) {
5834 check_complexity::stabilizeB_main_loop_afterwards, 1), *
this);
5839 stabilizeB_main_loop_afterwards, 1), *
this);
5840 new_bottom_state_with_transition_found=
true;
5846 if (new_bottom_state_with_transition_found) {
5849 if (std::next(stabilize_it) == stabilize_work_to_assign_later.end()) {
5850 stabilize_work_to_assign_later.pop_back();
5853 *stabilize_it=stabilize_work_to_assign_later.back();
5854 stabilize_work_to_assign_later.pop_back();
5860 m_singleton_block_with_new_bottom_states_for_debug = null_block_lb;
5863 blocks_that_need_refinement.pop_back(); assert(blocks_that_need_refinement.size()==bi.refinement_info);
5864 bi.refinement_info = null_state;
5865 assert(&BLC_source==bi.block_BLC_source);
5866 if (!bi_was_small_subblock)
5867 { assert(blocks_that_need_refinement.empty());
5868 make_stable_and_move_to_start_of_BLC(BLC_source, splitter); assert(&bi==&from_block_index);
5869 assert(!BLC_source.block_to_constellation.empty());
5870 if(BLC_source.block_to_constellation.before_end()->is_stable())
5876 else if (0 < bi.small_subblock_counter ||
5877 bi.sta.rt_non_bottom_states == bi.end_states ||
5886 make_BLC_simple(bi,
true), assert(!BLC_source.block_to_constellation.empty()),
5891 0 < bi.small_subblock_counter &&
5892 !BLC_source.block_to_constellation.before_end()->
5901 simple_list<BLC_indicators_lb>::iterator btc_it =
5902 BLC_source.block_to_constellation.before_end(); assert(!btc_it->is_stable());
5905 btc_it->start_marked_BLC = btc_it->start_same_BLC;
5906 btc_it->starts_in_small_subblock =
true; assert(btc_it != BLC_source.block_to_constellation.begin());
5909 while (!btc_it->is_stable());
5915 state_in_block_pointer_lb* blc_src_it =
5916 BLC_source.start_BLC_source; assert(blc_src_it < BLC_source.end_BLC_source);
5919 block_type_lb& current_blk=*blc_src_it->ref_state->block;
5920 if (!current_blk.contains_new_bottom_states &&
5921 current_blk.sta.rt_non_bottom_states <
5922 current_blk.end_states)
5923 { assert(0<current_blk.small_subblock_counter);
5924 --current_blk.small_subblock_counter;
5925 } assert(!current_blk.contains_new_bottom_states ||
5926 std::find(m_blocks_with_new_bottom_states.begin(),
5927 m_blocks_with_new_bottom_states.end(), ¤t_blk)!=
5928 m_blocks_with_new_bottom_states.end());
5929 blc_src_it = current_blk.end_states; assert(blc_src_it <= BLC_source.end_BLC_source);
5931 while (blc_src_it < BLC_source.end_BLC_source);
5937 }
else { assert(splitter->is_stable()); }
5938 } assert(Qhat_elt.first<=Qhat_elt.second);
5939 if (Qhat_elt.first==Qhat_elt.second)
5945 while (m_blocks_with_new_bottom_states.empty());
5946 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5950 for (std::vector<std::pair<BLC_list_const_iterator,BLC_list_const_iterator> >
5951 ::iterator qhat_it=initialize_qhat_work_to_assign_later.begin();
5952 qhat_it!=initialize_qhat_work_to_assign_later.end(); )
5954 bool new_bottom_state_with_transition_found=
false;
5955 for (BLC_list_const_iterator work_it=qhat_it->first;
5956 work_it<qhat_it->second; ++work_it)
5958 const state_index t_from=m_aut.get_transitions()[*work_it].from();
5959 if (0==m_states[t_from].no_of_outgoing_block_inert_transitions &&
5960 m_states[t_from].block->contains_new_bottom_states)
5965 if (new_bottom_state_with_transition_found) {
5968 stabilizeB_initialize_Qhat_afterwards, 1), *
this);
5973 stabilizeB_initialize_Qhat_afterwards, 1), *
this);
5974 new_bottom_state_with_transition_found=
true;
5980 if (new_bottom_state_with_transition_found) {
5983 if (std::next(qhat_it)==initialize_qhat_work_to_assign_later.end()) {
5984 initialize_qhat_work_to_assign_later.pop_back();
5987 *qhat_it=initialize_qhat_work_to_assign_later.back();
5988 initialize_qhat_work_to_assign_later.pop_back();
5996 for (std::vector<std::pair<BLC_list_const_iterator,BLC_list_const_iterator> >
5997 ::iterator stabilize_it=stabilize_work_to_assign_later.begin();
5998 stabilize_it!=stabilize_work_to_assign_later.end(); )
6000 bool new_bottom_state_with_transition_found=
false;
6001 for (BLC_list_const_iterator work_it=stabilize_it->first;
6002 work_it<stabilize_it->second; ++work_it)
6004 const state_index t_from=m_aut.get_transitions()[*work_it].from();
6005 if (0==m_states[t_from].no_of_outgoing_block_inert_transitions &&
6006 m_states[t_from].block->contains_new_bottom_states)
6011 if (new_bottom_state_with_transition_found) {
6013 check_complexity::stabilizeB_main_loop_afterwards, 1), *
this);
6018 stabilizeB_main_loop_afterwards, 1), *
this);
6019 new_bottom_state_with_transition_found=
true;
6025 if (new_bottom_state_with_transition_found) {
6028 if (std::next(stabilize_it) == stabilize_work_to_assign_later.end()) {
6029 stabilize_work_to_assign_later.pop_back();
6032 *stabilize_it=stabilize_work_to_assign_later.back();
6033 stabilize_work_to_assign_later.pop_back();
6051 std::vector<block_that_needs_refinement_type> blocks_that_need_refinement;
6079 void refine_super_BLC(BLC_indicators_lb& small_splitter,
6080 BLC_indicators_lb*
const large_splitter =
nullptr)
6093 const transition& first_t =
6094 m_aut.get_transitions()[*small_splitter.start_same_BLC];
6095 constellation_type_lb*
const new_constellation =
6096 m_states[first_t.to()].block->constellation;
6097 constellation_type_lb*
const old_constellation =
6098 nullptr==large_splitter ?
nullptr :
6099 m_states[m_aut.get_transitions()[*large_splitter->start_same_BLC].to()].
6100 block->constellation;
6101 const bool is_inert = is_inert_during_init(first_t);
6107 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
6116 const unsigned char max_C=check_complexity::log_n-check_complexity::
6117 ilog2(number_of_states_in_constellation(*new_constellation));
6121 four_way_splitB_handle_transitions_in_main_splitter, max_C), *
this);
6123 BLC_list_iterator splitter_it = small_splitter.start_same_BLC; assert(splitter_it != small_splitter.end_same_BLC);
6126 const transition& t=m_aut.get_transitions()[*splitter_it];
6127 state_in_block_pointer_lb
const src = m_states.begin() + t.from(); assert(is_inert == is_inert_during_init(t));
6130 block_type_lb& bi = *src.ref_state->block;
6131 if (!bi.contains_new_bottom_states &&
6132 1 < number_of_states_in_block(bi) &&
6133 (!is_inert || bi.constellation != new_constellation))
6135 if (null_state == bi.refinement_info)
6138 bi.refinement_info = blocks_that_need_refinement.size();
6139 blocks_that_need_refinement.emplace_back(bi,
6140 is_inert && old_constellation == bi.constellation
6141 ?
nullptr : large_splitter); assert(bi.refinement_info < blocks_that_need_refinement.size());
6143 block_that_needs_refinement_type& bri =
6144 blocks_that_need_refinement[bi.refinement_info]; assert(bri.start_bottom_states[ReachAlw] == bi.start_bottom_states);
6145 if (0==src.ref_state->no_of_outgoing_block_inert_transitions)
6146 { assert(bi.start_bottom_states<=src.ref_state->ref_states_in_blocks);
6147 assert(src.ref_state->ref_states_in_blocks<bi.sta.rt_non_bottom_states);
6148 if (src.ref_state->ref_states_in_blocks <
6149 bri.start_bottom_states[AvoidSml])
6152 if (
nullptr != large_splitter &&
6153 !(is_inert && old_constellation == bi.constellation)) {
6154 assert(next_target_constln_in_same_saC(src, splitter_it)==large_splitter);
6158 else if (
nullptr == large_splitter ||
6159 (is_inert && old_constellation == bi.constellation))
6161 static_assert(ReachAlw + 1 == AvoidSml);
6162 swap_states_in_states_in_block(bri.start_bottom_states[AvoidSml],
6163 src.ref_state->ref_states_in_blocks);
6164 ++bri.start_bottom_states[AvoidSml];
6166 else if (bri.start_bottom_states[AvoidSml+1] <=
6167 src.ref_state->ref_states_in_blocks)
6170 assert(
nullptr!=large_splitter);
6171 outgoing_transitions_const_it_lb
const out_it_end=
6172 std::next(src.ref_state)>=m_states.end() ? m_outgoing_transitions.end()
6173 : std::next(src.ref_state)->start_outgoing_transitions;
6174 for (outgoing_transitions_const_it_lb out_it=
6175 src.ref_state->start_outgoing_transitions; out_it!=out_it_end; ++out_it)
6177 assert(m_transitions[*out_it->ref_BLC_transitions].
6178 transitions_per_block_to_constellation!=large_splitter);
6182 else if (next_target_constln_in_same_saC(src, splitter_it)==
6185 static_assert(ReachAlw + 1 == AvoidSml);
6186 swap_states_in_states_in_block(bri.start_bottom_states[AvoidSml],
6187 src.ref_state->ref_states_in_blocks);
6188 ++bri.start_bottom_states[AvoidSml];
6192 static_assert(AvoidSml + 1 == AvoidLrg);
6193 --bri.start_bottom_states[AvoidSml+1];
6194 swap_states_in_states_in_block
6195 (bri.start_bottom_states[AvoidSml+1],
6196 src.ref_state->ref_states_in_blocks);
6201 assert(bi.sta.rt_non_bottom_states<=src.ref_state->ref_states_in_blocks);
6202 assert(src.ref_state->ref_states_in_blocks<bi.end_states);
6203 if (undefined == src.ref_state->counter)
6205 if (
nullptr==large_splitter ||
6206 (is_inert && old_constellation == bi.constellation) ||
6207 next_target_constln_in_same_saC(src, splitter_it)==
6211 src.ref_state->counter = marked(ReachAlw) +
6212 src.ref_state->no_of_outgoing_block_inert_transitions; assert(is_in_marked_range_of(src.ref_state->counter, ReachAlw));
6214 bri.potential_non_bottom_states[ReachAlw].push_back(src);
6219 src.ref_state->counter = marked_HitSmall;
6220 bri.potential_non_bottom_states_HitSmall.push_back(src);
6222 outgoing_transitions_const_it_lb
const out_it_end=std::next(src.ref_state)>=
6223 m_states.end() ? m_outgoing_transitions.end()
6224 : std::next(src.ref_state)->start_outgoing_transitions;
6225 for (outgoing_transitions_const_it_lb out_it=src.ref_state->
6226 start_outgoing_transitions; out_it!=out_it_end; ++out_it)
6228 assert(m_transitions[*out_it->ref_BLC_transitions].
6229 transitions_per_block_to_constellation!=large_splitter);
6235 else if (marked_HitSmall==src.ref_state->counter) {
6236 assert(
nullptr != bri.large_splitter);
6238 assert(is_in_marked_range_of(src.ref_state->counter, ReachAlw));
6239 if (
nullptr != bri.large_splitter) {
6240 assert(next_target_constln_in_same_saC(src,splitter_it)==bri.large_splitter);
6245 }
else { assert(null_state == bi.refinement_info); }
6248 while (splitter_it!=small_splitter.end_same_BLC);
6250 assert(m_BLC_indicators_to_be_deleted.empty());
6251 while(!blocks_that_need_refinement.empty())
6253 block_that_needs_refinement_type&
6254 bri=blocks_that_need_refinement.back();
6256 block_type_lb& bi = *bri.start_bottom_states[0]->ref_state->block; assert(!bi.contains_new_bottom_states);
6257 assert(&bri==&blocks_that_need_refinement[bi.refinement_info]);
6258 assert(1<number_of_states_in_block(bi));
6259 four_way_splitB(bri, old_constellation, new_constellation); assert(bi.refinement_info<blocks_that_need_refinement.size());
6260 #ifdef MORE_STATISTICS
6261 assert(bi.start_bottom_states==blocks_that_need_refinement
6262 [bi.refinement_info].transition_count_sample_state->ref_states_in_blocks);
6264 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
6265 m_singleton_block_with_new_bottom_states_for_debug = null_block_lb;
6267 blocks_that_need_refinement.pop_back(); assert(blocks_that_need_refinement.size()==bi.refinement_info);
6268 bi.refinement_info = null_state;
6271 for (std::vector<std::pair<BLC_source_type&, simple_list<BLC_indicators_lb>::iterator> >::iterator
6272 it=m_BLC_indicators_to_be_deleted.begin();
6273 it<m_BLC_indicators_to_be_deleted.end(); ++it)
6274 { assert(it->second->start_same_BLC==it->second->end_same_BLC);
6276 it->first.block_to_constellation.erase(it->second);
6278 clear(m_BLC_indicators_to_be_deleted);
6291 void create_initial_partition()
6293 mCRL2log(log::verbose) <<
"An O(m log n) "
6294 << (m_branching ? (m_preserve_divergence
6295 ?
"divergence-preserving branching "
6298 <<
"bisimulation partitioner created for " << m_aut.num_states()
6299 <<
" states and " << m_transitions.size()
6300 <<
" transitions (using the experimental algorithm with lazy BLC sets).\n";
6301 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
6302 check_complexity::init(2 * m_aut.num_states());
6305 group_transitions_on_tgt_label(m_aut);
6307 assert((
unsigned) m_preserve_divergence <= 1);
6308 constellation_type_lb& initial_constellation = *
6310 simple_list<BLC_indicators_lb>::get_pool().
6311 template construct<constellation_type_lb>
6313 new constellation_type_lb
6315 (m_states_in_blocks.data(), m_states_in_blocks.data_end()); assert(1==no_of_constellations);
6316 BLC_source_type& initial_BLC_source = *
6318 simple_list<BLC_indicators_lb>::get_pool().
6319 template construct<BLC_source_type>
6323 (m_states_in_blocks.data(), m_states_in_blocks.data_end());
6324 block_type_lb& initial_block = *
6326 simple_list<BLC_indicators_lb>::get_pool().
6327 template construct<block_type_lb>
6331 (m_states_in_blocks.data(), m_states_in_blocks.data_end(),
6332 m_states_in_blocks.data_end(), initial_constellation,
6333 initial_BLC_source, check_complexity::ilog2(m_aut.num_states())); assert(1==no_of_blocks);
6339 std::vector<label_index> todo_stack_actions;
6340 std::vector<transition_index> count_transitions_per_action
6341 (m_aut.num_action_labels() + (
unsigned) m_preserve_divergence, 0);
6342 for (
const transition& t : m_aut.get_transitions())
6345 const label_index label=label_or_divergence(t,
6346 m_aut.num_action_labels()); assert(m_aut.apply_hidden_label_map(t.label())==t.label());
6347 transition_index& c=count_transitions_per_action[label];
6350 todo_stack_actions.push_back(label);
6357 accumulate_entries(count_transitions_per_action, todo_stack_actions);
6358 for (transition_index ti=0; ti<m_transitions.size(); ++ti)
6360 const transition& t=m_aut.get_transitions()[ti];
6361 const label_index label = label_or_divergence(t,
6362 m_aut.num_action_labels());
6363 transition_index& c=count_transitions_per_action[label]; assert(c < m_transitions.size());
6364 m_BLC_transitions[c]=ti;
6369 std::vector<label_index>::const_iterator
6370 a_it=todo_stack_actions.begin();
6371 BLC_list_iterator start_index=m_BLC_transitions.data();
6372 while (todo_stack_actions.end() != a_it)
6374 const label_index a = *a_it;
6375 BLC_list_iterator end_index =
6376 m_BLC_transitions.data()+count_transitions_per_action[a]; assert(end_index<=m_BLC_transitions.data_end());
6378 initial_BLC_source.block_to_constellation.emplace_back
6379 (start_index, end_index,
true); assert(start_index<end_index);
6380 start_index = end_index;
6382 } assert(start_index==m_BLC_transitions.data_end());
6390 fixed_vector<transition_index> count_outgoing_transitions_per_state
6391 (m_aut.num_states(), 0);
6392 for(
const transition& t: m_aut.get_transitions())
6395 count_outgoing_transitions_per_state[t.from()]++;
6396 if (is_inert_during_init(t))
6398 m_states[t.from()].no_of_outgoing_block_inert_transitions++;
6408 outgoing_transitions_it_lb
6409 current_outgoing_transitions = m_outgoing_transitions.begin();
6412 for (state_index s=0; s<m_aut.num_states(); ++s)
6414 if (marked_range<=m_states[s].no_of_outgoing_block_inert_transitions)
6416 mCRL2log(log::error) <<
"State " << s <<
" has "
6417 << m_states[s].no_of_outgoing_block_inert_transitions
6418 <<
" outgoing block-inert transitions. However, the "
6419 "four-way-split can handle at most "
6421 <<
" outgoing block-inert transitions per state. "
6425 m_states[s].start_outgoing_transitions=current_outgoing_transitions+
6426 m_states[s].no_of_outgoing_block_inert_transitions;
6427 current_outgoing_transitions+=
6428 static_cast<std::ptrdiff_t>(count_outgoing_transitions_per_state[s]);
6429 count_outgoing_transitions_per_state[s]=0;
6432 } assert(m_outgoing_transitions.end()==current_outgoing_transitions);
6434 for (BLC_list_iterator ti=m_BLC_transitions.data();
6435 ti<m_BLC_transitions.data_end(); ++ti)
6437 const transition& t=m_aut.get_transitions()[*ti];
6438 if (is_inert_during_init(t))
6440 m_transitions[*ti].ref_outgoing_transitions =
6441 --m_states[t.from()].start_outgoing_transitions;
6445 m_transitions[*ti].ref_outgoing_transitions =
6446 m_states[t.from()].start_outgoing_transitions +
6447 count_outgoing_transitions_per_state[t.from()];
6449 m_transitions[*ti].ref_outgoing_transitions->ref_BLC_transitions=ti;
6450 ++count_outgoing_transitions_per_state[t.from()];
6455 state_index current_state=null_state; assert(current_state + 1 == 0);
6457 for(std::vector<transition>::iterator it=m_aut.get_transitions().begin();
6458 it!=m_aut.get_transitions().end(); it++)
6462 if (it->to() != current_state)
6464 state_index i = current_state;
6465 current_state = it->to();
6469 create_initial_partition_set_start_incoming_transitions, 1), *
this);
6470 m_states[i].start_incoming_transitions=it;
6472 while (i != current_state);
6475 while (++current_state < m_aut.num_states())
6476 {
mCRL2complexity(&m_states[current_state], add_work(check_complexity::
6477 create_initial_partition_set_start_incoming_transitions, 1), *
this);
6478 m_states[current_state].start_incoming_transitions =
6479 m_aut.get_transitions().end();
6483 outgoing_transitions_it_lb it = m_outgoing_transitions.end();
6484 if (m_outgoing_transitions.begin() < it)
6487 const transition& t=m_aut.get_transitions()[*it->ref_BLC_transitions];
6488 state_index current_state = t.from();
6489 label_index current_label = label_or_divergence(t);
6490 outgoing_transitions_it_lb current_end_same_saC = it;
6491 while (m_outgoing_transitions.begin() < it)
6494 const transition&t=m_aut.get_transitions()[*it->ref_BLC_transitions];
6495 const label_index new_label = label_or_divergence(t);
6496 if (current_state == t.from() && current_label == new_label)
6500 it->start_same_saC = current_end_same_saC;
6505 current_state = t.from();
6506 current_label = new_label;
6507 current_end_same_saC->start_same_saC = std::next(it);
6508 current_end_same_saC = it;
6511 current_end_same_saC->start_same_saC = m_outgoing_transitions.begin();
6512 } assert(m_states_in_blocks.size()==m_aut.num_states());
6513 state_in_block_pointer_lb* lower_i = m_states_in_blocks.data(); assert(initial_block.start_bottom_states==lower_i);
6514 state_in_block_pointer_lb* upper_i = m_states_in_blocks.data_end(); assert(initial_block.end_states==upper_i);
6515 for (fixed_vector<state_type_gj_lb>::iterator
6516 i = m_states.begin(); i < m_states.end(); ++i)
6518 if (0<i->no_of_outgoing_block_inert_transitions)
6521 upper_i->ref_state=i;
6522 i->ref_states_in_blocks=upper_i;
6526 lower_i->ref_state=i;
6527 i->ref_states_in_blocks=lower_i;
6530 i->block=&initial_block;
6531 } assert(lower_i == upper_i);
6532 initial_block.sta.rt_non_bottom_states = lower_i;
6534 #ifdef MORE_STATISTICS
6536 fixed_vector<state_type_gj_lb>::iterator sample_state =
6537 m_states_in_blocks.begin()->ref_state; assert(0==no_of_non_block_inert_sample_transitions);
6538 outgoing_transitions_const_it_lb
const out_it_end =
6539 std::next(sample_state) >= m_states.end()
6540 ? m_outgoing_transitions.end()
6541 : std::next(sample_state)->start_outgoing_transitions; assert(0==sample_state->no_of_outgoing_block_inert_transitions);
6542 for (outgoing_transitions_it_lb out_it =
6543 sample_state->start_outgoing_transitions; out_it < out_it_end; assert(out_it <= out_it->start_same_saC),
6544 out_it = std::next(out_it->start_same_saC))
6548 const transition& tr = m_aut.get_transitions()[*out_it->ref_BLC_transitions];
6549 assert(sample_state == m_states.begin() + tr.from());
6551 ++no_of_non_block_inert_sample_transitions;
6555 for (simple_list<BLC_indicators_lb>::iterator
6556 blc_it=initial_BLC_source.block_to_constellation.begin();
6557 initial_BLC_source.block_to_constellation.end()!=blc_it; ++blc_it)
6558 { assert(blc_it->start_same_BLC<blc_it->end_same_BLC);
6559 BLC_list_iterator it=blc_it->start_same_BLC;
6562 m_transitions[*it].transitions_per_block_to_constellation=blc_it;
6565 while (it!=blc_it->end_same_BLC);
6568 for (simple_list<BLC_indicators_lb>::iterator
6569 blc_it=initial_BLC_source.block_to_constellation.begin();
6570 initial_BLC_source.block_to_constellation.end()!=blc_it; ++blc_it)
6571 { assert(blc_it->start_same_BLC<blc_it->end_same_BLC);
6572 if (!is_inert_during_init(m_aut.get_transitions()
6573 [*blc_it->start_same_BLC]))
6576 refine_super_BLC(*blc_it);
6578 } assert(1==no_of_BLC_source_sets);
6579 assert(check_data_structures(
"After initial reading before splitting in the initialisation",
false));
6581 print_data_structures(
"End initialisation");
6583 assert(check_stability(
"End initialisation"));
6584 assert(check_data_structures(
"End initialisation",
false));
6598 block_type_lb* select_and_remove_a_block_in_a_non_trivial_constellation()
6599 { assert(!m_non_trivial_constellations.empty());
6602 constellation_type_lb& ci=*m_non_trivial_constellations.back();
6603 block_type_lb& index_block_B=*ci.start_const_states->ref_state->block;
6604 block_type_lb& second_block_B=
6605 *std::prev(ci.end_const_states)->ref_state->block;
6607 if (number_of_states_in_block(index_block_B)<=
6608 number_of_states_in_block(second_block_B))
6610 ci.start_const_states=index_block_B.end_states;
6611 update_small_subblock_counters(index_block_B.start_bottom_states,
6612 index_block_B.end_states, ci.end_const_states,
SPLIT_LEFT);
6613 return &index_block_B;
6617 ci.end_const_states=second_block_B.start_bottom_states;
6618 update_small_subblock_counters(ci.start_const_states,
6619 second_block_B.start_bottom_states,
6621 return &second_block_B;
6634 state_index no_of_new_bottom_states = 0;
6636 #ifdef MORE_STATISTICS
6641 transition_index no_of_non_block_inert_sample_transitions = 0;
6657 void refine_partition_until_it_becomes_stable()
6663 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> > calM;
6665 std::clock_t next_print_time = std::clock();
6666 const std::clock_t rounded_start_time = next_print_time-CLOCKS_PER_SEC/2;
6670 print_data_structures(
"MAIN LOOP");
6672 assert(check_data_structures(
"MAIN LOOP"));
6673 assert(check_stability(
"MAIN LOOP"));
6674 if (mCRL2logEnabled(log::verbose))
6676 if (std::clock_t now = std::clock(); next_print_time <= now ||
6677 m_non_trivial_constellations.empty())
6682 #ifndef MORE_STATISTICS
6688 next_print_time+=((now-next_print_time)/(60*CLOCKS_PER_SEC)
6689 + 1) * (60*CLOCKS_PER_SEC);
6692 next_print_time+=((now-next_print_time)/(10*CLOCKS_PER_SEC)
6693 + 1) * (10*CLOCKS_PER_SEC);
6695 now = (now - rounded_start_time) / CLOCKS_PER_SEC;
6702 mCRL2log(log::verbose) << now / 3600 <<
" h ";
6705 mCRL2log(log::verbose) << now / 60 <<
" min ";
6709 <<
" sec passed since starting the main loop.\n";
6711 #define PRINT_SG_PL(counter, sg_string, pl_string)
6712 (counter) << (1
== (counter) ? (sg_string) : (pl_string))
6714 << (m_non_trivial_constellations.empty()
6715 ?
"The reduced LTS contains "
6716 :
"The reduced LTS contains at least ")
6717 #ifndef MORE_STATISTICS
6718 <<
PRINT_SG_PL(no_of_blocks,
" state.",
" states.");
6720 << PRINT_SG_PL(no_of_blocks,
" state and ",
" states and ")
6721 << PRINT_SG_PL(no_of_non_block_inert_sample_transitions,
6722 " transition.",
" transitions.");
6724 if (1 < no_of_blocks)
6726 #define PRINT_INT_PERCENTAGE(num,denom)
6727 (((num) * 200
+ (denom)) / (denom) / 2
)
6728 mCRL2log(log::verbose) <<
" Estimated "
6732 #undef PRINT_INT_PERCENTAGE
6735 <<
"\nThe current partition contains ";
6740 " new bottom state, ",
" new bottom states, ");
6741 }
else { assert(0==no_of_new_bottom_states); }
6744 " constellation (of which ",
" constellations (of which ")
6745 <<
PRINT_SG_PL(m_non_trivial_constellations.size(),
6746 " is nontrivial), and ",
" are nontrivial), and ")
6748 " super-BLC source set.\n",
" super-BLC source sets.\n");
6749 #ifdef MORE_STATISTICS
6756 mCRL2log(log::verbose)
6757 <<
"The large splitter has been visited "
6758 "by the NewBotSt coroutine in "
6760 (number_of_large_splitters_searched_in_small_subblocks,
6761 " small sub-block and ",
" small sub-blocks and ")
6763 (number_of_large_splitters_searched_in_large_subblocks,
6764 " large sub-block. There have been ",
6765 " large sub-blocks. There have been ")
6766 << PRINT_SG_PL(number_of_small_bottom_block_refinements,
6768 <<
" to refine a small new bottom state block and "
6769 << PRINT_SG_PL(number_of_large_bottom_block_refinements,
6771 <<
" to refine a large new bottom state block.\n";
6777 if (m_non_trivial_constellations.empty())
6782 block_type_lb& index_block_B=
6783 *select_and_remove_a_block_in_a_non_trivial_constellation();
6784 constellation_type_lb& old_constellation=*index_block_B.constellation;
6787 if (old_constellation.start_const_states->ref_state->block==
6788 std::prev(old_constellation.end_const_states)->ref_state->block)
6789 { assert(m_non_trivial_constellations.back()==&old_constellation);
6791 m_non_trivial_constellations.pop_back();
6793 constellation_type_lb& new_constellation = *
6795 simple_list<BLC_indicators_lb>::get_pool().
6796 template construct<constellation_type_lb>
6798 new constellation_type_lb
6800 (index_block_B.start_bottom_states,
6801 index_block_B.end_states);
6802 ++no_of_constellations;
6806 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
6808 unsigned char const max_C=check_complexity::log_n-check_complexity::
6809 ilog2(number_of_states_in_constellation(new_constellation));
6811 refine_partition_until_it_becomes_stable_find_splitter, max_C), *
this);
6827 for (state_in_block_pointer_lb* i=index_block_B.start_bottom_states;
6828 i!=index_block_B.end_states; ++i)
6831 const std::vector<transition>::iterator end_it=
6832 (std::next(i->ref_state)==m_states.end())
6833 ? m_aut.get_transitions().end()
6834 : std::next(i->ref_state)->start_incoming_transitions;
6835 for(std::vector<transition>::iterator
6836 j=i->ref_state->start_incoming_transitions; j!=end_it; ++j)
6838 const transition& t=*j; assert(m_states[t.to()].ref_states_in_blocks == i);
6839 const transition_index t_index=
6840 std::distance(m_aut.get_transitions().begin(), j);
6843 const outgoing_transitions_it_lb old_pos=
6844 m_transitions[t_index].ref_outgoing_transitions;
6845 const outgoing_transitions_it_lb
6846 end_same_saC = old_pos->start_same_saC<old_pos
6847 ? old_pos : old_pos->start_same_saC;
6848 const outgoing_transitions_it_lb
6849 new_pos=end_same_saC->start_same_saC; assert(m_states[t.from()].start_outgoing_transitions<=new_pos);
6850 if (old_pos != new_pos)
6851 { assert(new_pos<old_pos);
6852 std::swap(old_pos->ref_BLC_transitions,
6853 new_pos->ref_BLC_transitions);
6854 m_transitions[*old_pos->ref_BLC_transitions].
6855 ref_outgoing_transitions=old_pos;
6856 m_transitions[*new_pos->ref_BLC_transitions].
6857 ref_outgoing_transitions=new_pos;
6858 } assert(new_pos<=end_same_saC);
6859 end_same_saC->start_same_saC = std::next(new_pos);
6864 const transition* prev_t;
6865 if (m_states[t.from()].start_outgoing_transitions < new_pos &&
6867 (prev_t = &m_aut.get_transitions()
6868 [*std::prev(new_pos)->ref_BLC_transitions], assert(prev_t->from() == t.from()),
6869 m_states[prev_t->to()].block == &index_block_B) &&
6870 label_or_divergence(*prev_t) == label_or_divergence(t))
6873 new_pos->start_same_saC = std::prev(new_pos)->start_same_saC; assert(m_states[t.from()].start_outgoing_transitions<=new_pos->start_same_saC);
6874 assert(new_pos->start_same_saC<new_pos);
6875 assert(std::prev(new_pos)==new_pos->start_same_saC->start_same_saC);
6876 new_pos->start_same_saC->start_same_saC = new_pos;
6881 new_pos->start_same_saC = new_pos;
6882 #ifdef MORE_STATISTICS
6883 if (m_states[t.from()].block->start_bottom_states ==
6884 m_states[t.from()].ref_states_in_blocks)
6886 assert(!is_inert_during_init(t) || &index_block_B != m_states[t.from()].block);
6888 ++no_of_non_block_inert_sample_transitions;
6892 #ifdef MORE_STATISTICS
6893 if (end_same_saC == new_pos)
6896 if (m_states[t.from()].block->start_bottom_states ==
6897 m_states[t.from()].ref_states_in_blocks)
6899 assert(!is_inert_during_init(t) || &index_block_B != m_states[t.from()].block);
6901 --no_of_non_block_inert_sample_transitions;
6910 for (state_in_block_pointer_lb* i=index_block_B.start_bottom_states;
6911 i!=index_block_B.end_states; ++i)
6914 const std::vector<transition>::iterator end_it=
6915 (std::next(i->ref_state)==m_states.end())
6916 ? m_aut.get_transitions().end()
6917 : std::next(i->ref_state)->start_incoming_transitions;
6918 for(std::vector<transition>::iterator
6919 j=i->ref_state->start_incoming_transitions; j!=end_it; ++j)
6921 const transition& t=*j;
6922 const transition_index t_index=
6923 std::distance(m_aut.get_transitions().begin(), j); assert(m_states[t.to()].block == &index_block_B);
6928 const outgoing_transitions_it_lb out_pos=
6929 m_transitions[t_index].ref_outgoing_transitions;
6930 const outgoing_transitions_it_lb start_new_saC=
6931 out_pos->start_same_saC;
6932 if (start_new_saC < out_pos)
6935 if (out_pos < start_new_saC->start_same_saC)
6940 out_pos->start_same_saC = start_new_saC->start_same_saC;
6947 if (update_the_doubly_linked_list_LBC_new_constellation
6948 (index_block_B, t, t_index))
6955 BLC_list_iterator BLC_pos=m_transitions[t_index].
6956 ref_outgoing_transitions->ref_BLC_transitions; assert(t_index == *BLC_pos);
6958 calM.emplace_back(BLC_pos, BLC_pos);
6963 index_block_B.constellation=&new_constellation;
6969 for (std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >::
6970 iterator calM_elt=calM.begin();; )
6972 simple_list <BLC_indicators_lb>::iterator
6973 ind=m_transitions[*calM_elt->first].
6974 transitions_per_block_to_constellation;
mCRL2complexity(ind, add_work(check_complexity::
6975 refine_partition_until_it_becomes_stable_correct_end_of_calM,max_C),*
this);
6976 assert(ind->start_same_BLC==calM_elt->first);
6977 assert(!ind->has_marked_transitions());
6978 const transition& last_t=
6979 m_aut.get_transitions()[*std::prev(ind->end_same_BLC)]; assert(m_states[last_t.to()].block->constellation==&new_constellation);
6980 assert(ind->start_same_BLC<ind->end_same_BLC);
6981 const transition* next_t=
nullptr;
6982 if (is_inert_during_init(last_t) ||
6983 (ind->end_same_BLC<m_BLC_transitions.data_end() &&
6984 (next_t=&m_aut.get_transitions()[*ind->end_same_BLC],
6985 m_states[last_t.from()].block->block_BLC_source==
6986 m_states[next_t->from()].block->block_BLC_source &&
6987 label_or_divergence(last_t)==label_or_divergence(*next_t) &&
6988 &old_constellation==
6989 m_states[next_t->to()].block->constellation)))
6993 calM_elt->second = ind->end_same_BLC;
6995 if (calM_elt==calM.end())
7005 if (std::next(calM_elt)==calM.end())
7016 calM_elt->first=calM.back().first;
7026 if (m_branching && 1 < number_of_states_in_block(index_block_B))
7027 { assert(null_state == index_block_B.refinement_info);
7028 index_block_B.refinement_info = blocks_that_need_refinement.size();
7029 block_that_needs_refinement_type& co_refinement_info =
7030 blocks_that_need_refinement.emplace_back(index_block_B);
7031 state_in_block_pointer_lb* sta_it=index_block_B.start_bottom_states; assert(sta_it < index_block_B.sta.rt_non_bottom_states);
7035 const outgoing_transitions_it_lb out_it_end =
7036 std::next(sta_it->ref_state)==m_states.end()
7037 ? m_outgoing_transitions.end()
7038 : std::next(sta_it->ref_state)->start_outgoing_transitions; assert(undefined==sta_it->ref_state->counter);
7039 for (outgoing_transitions_it_lb out_it = sta_it->ref_state->
7040 start_outgoing_transitions; out_it<out_it_end; assert(out_it <= out_it->start_same_saC),
7041 out_it = std::next(out_it->start_same_saC))
7043 const transition& tr=m_aut.get_transitions()
7044 [*out_it->ref_BLC_transitions]; assert(&m_states[tr.from()]==&*sta_it->ref_state);
7046 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(tr.label())))
7049 while(++out_it<out_it_end){ assert(!m_aut.is_tau(m_aut_apply_hidden_label_map
7050 (m_aut.get_transitions()[*out_it->ref_BLC_transitions].label()))); }
7054 if (!m_preserve_divergence || tr.from() != tr.to())
7055 { assert(is_inert_during_init(tr));
7056 if (m_states[tr.to()].block->constellation==&old_constellation)
7057 { assert(sta_it == sta_it->ref_state->ref_states_in_blocks);
7058 assert(sta_it >= co_refinement_info.start_bottom_states[ReachAlw+1]);
7059 static_assert(ReachAlw + 1 == AvoidSml);
7060 swap_states_in_states_in_block
7061 (co_refinement_info.start_bottom_states[ReachAlw+1],
7063 ++co_refinement_info.start_bottom_states[ReachAlw+1];
7066 }
else { assert(!is_inert_during_init(tr)); }
7070 while (sta_it < index_block_B.sta.rt_non_bottom_states);
7071 for (; sta_it < index_block_B.end_states; ++sta_it)
7073 const outgoing_transitions_it_lb out_it_end =
7074 std::next(sta_it->ref_state)==m_states.end()
7075 ? m_outgoing_transitions.end()
7076 : std::next(sta_it->ref_state)->start_outgoing_transitions; assert(undefined==sta_it->ref_state->counter);
7077 for (outgoing_transitions_it_lb out_it = sta_it->ref_state->
7078 start_outgoing_transitions; out_it<out_it_end; assert(out_it <= out_it->start_same_saC),
7079 out_it = std::next(out_it->start_same_saC))
7081 const transition& tr=m_aut.get_transitions()
7082 [*out_it->ref_BLC_transitions]; assert(&m_states[tr.from()]==&*sta_it->ref_state);
7084 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(tr.label())))
7087 while(++out_it<out_it_end){ assert(!m_aut.is_tau(m_aut_apply_hidden_label_map
7088 (m_aut.get_transitions()[*out_it->ref_BLC_transitions].label()))); }
7092 if (!m_preserve_divergence || tr.from() != tr.to())
7093 { assert(is_inert_during_init(tr));
7094 if (m_states[tr.to()].block->constellation==&old_constellation)
7098 sta_it->ref_state->counter = marked(ReachAlw)+
7099 sta_it->ref_state->no_of_outgoing_block_inert_transitions; assert(is_in_marked_range_of(sta_it->ref_state->counter, ReachAlw));
7100 co_refinement_info.potential_non_bottom_states[ReachAlw].
7104 }
else { assert(!is_inert_during_init(tr)); }
7110 if (0!=co_refinement_info.bottom_size(AvoidSml))
7112 if (0!=co_refinement_info.bottom_size(ReachAlw) ||
7113 !co_refinement_info.
7114 potential_non_bottom_states[ReachAlw].empty())
7120 four_way_splitB(co_refinement_info,
7121 &old_constellation, &new_constellation);
7122 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
7123 m_singleton_block_with_new_bottom_states_for_debug = null_block_lb;
7129 clear_state_counters(co_refinement_info.
7130 potential_non_bottom_states[ReachAlw].begin(),
7131 co_refinement_info.potential_non_bottom_states[ReachAlw].end(),
7133 } assert(&co_refinement_info ==
7134 &blocks_that_need_refinement[index_block_B.refinement_info]);
7135 #ifdef MORE_STATISTICS
7136 assert(index_block_B.start_bottom_states==
7137 co_refinement_info.transition_count_sample_state->ref_states_in_blocks);
7139 blocks_that_need_refinement.pop_back(); assert(blocks_that_need_refinement.size()==index_block_B.refinement_info);
7140 index_block_B.refinement_info = null_state;
7143 for (std::pair<BLC_list_iterator, BLC_list_iterator> calM_elt: calM)
7147 print_data_structures(
"Main loop");
7149 assert(check_stability(
"Main loop", &calM, &calM_elt, &old_constellation, &new_constellation));
7150 assert(check_data_structures(
"Main loop",
false));
7151 assert(calM_elt.first < calM_elt.second);
7154 simple_list<BLC_indicators_lb>::iterator
7155 small_splitter=m_transitions[*std::prev(calM_elt.second)].
7156 transitions_per_block_to_constellation;
mCRL2complexity(small_splitter, add_work(check_complexity::
7157 refine_partition_until_it_becomes_stable_execute_main_split,max_C),*
this);
7158 assert(small_splitter->end_same_BLC==calM_elt.second);
7159 assert(small_splitter->is_stable());
7160 calM_elt.second = small_splitter->start_same_BLC; assert(small_splitter->start_same_BLC<small_splitter->end_same_BLC);
7162 const transition& first_t=
7163 m_aut.get_transitions()[*small_splitter->start_same_BLC]; assert(m_states[first_t.to()].block->constellation==&new_constellation);
7164 const BLC_source_type& block_BLC_source =
7165 *m_states[first_t.from()].block->block_BLC_source;
7170 simple_list<BLC_indicators_lb>::iterator
const large_splitter =
7171 block_BLC_source.block_to_constellation.prev(small_splitter);
7172 const transition* large_t;
7173 if(block_BLC_source.block_to_constellation.end()==large_splitter ||
7174 large_splitter->start_same_BLC==large_splitter->end_same_BLC ||
7176 &m_aut.get_transitions()[*large_splitter->start_same_BLC], assert(m_states[large_t->from()].block->block_BLC_source==&block_BLC_source),
7177 m_states[large_t->to()].block->constellation !=
7178 &old_constellation) ||
7179 label_or_divergence(first_t) != label_or_divergence(*large_t))
7182 if (is_inert_during_init(first_t) &&
7183 block_BLC_source.start_BLC_source <
7184 old_constellation.end_const_states &&
7185 old_constellation.start_const_states <
7186 block_BLC_source.end_BLC_source)
7191 refine_super_BLC(*small_splitter,
nullptr);
7196 refine_super_BLC(*small_splitter, &*large_splitter);
7199 while (calM_elt.first < calM_elt.second);
7202 print_data_structures(
"Before stabilize");
7204 assert(check_data_structures(
"Before stabilize",
false));
7205 assert(check_stability(
"Before stabilize"));
7208 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
7209 check_complexity::print_grand_totals();
7215 std::clock_t end_initial_part;
7228 bisim_partitioner_gj_lazy_BLC(LTS_TYPE& aut,
const bool branching =
false,
const bool preserve_divergence =
false)
7230 m_states(aut.num_states()),
7231 m_outgoing_transitions(aut.num_transitions()),
7232 m_transitions(aut.num_transitions()),
7233 m_states_in_blocks(aut.num_states()),
7235 m_BLC_transitions(aut.num_transitions()),
7236 m_branching(branching),
7237 m_preserve_divergence(preserve_divergence)
7238 { assert(m_branching || !m_preserve_divergence);
7241 aut.rename_hidden_labels_to_tau();
7242 create_initial_partition();
7243 end_initial_part=std::clock();
7244 mCRL2log(log::debug) <<
"After initialisation there are "
7245 << no_of_blocks <<
" equivalence classes. Start refining. \n";
7246 refine_partition_until_it_becomes_stable(); assert(check_data_structures(
"READY"));
7277template <
class LTS_TYPE>
7278void bisimulation_reduce_gj_lazy_BLC(LTS_TYPE& l,
const bool branching =
false,
7279 const bool preserve_divergence =
false)
7281 if (1 >= l.num_states())
7283 mCRL2log(log::warning) <<
"There is only 1 state in the LTS. It is not "
7284 "guaranteed that branching bisimulation minimisation runs in "
7285 "time O(m log n).\n";
7289 const std::clock_t start_SCC=std::clock();
7292 scc_reduce(l, preserve_divergence);
7297 const std::clock_t start_part=std::clock();
7298 bisim_partitioner_gj_lazy_BLC<LTS_TYPE> bisim_part(l,
7299 branching, preserve_divergence);
7302 const std::clock_t end_part=std::clock();
7303 bisim_part.finalize_minimized_LTS();
7305 if (mCRL2logEnabled(log::debug))
7307 const std::clock_t end_finalizing=std::clock();
7308 const int prec=
static_cast<
int>
7309 (std::log10(CLOCKS_PER_SEC)+0.69897000433602);
7315 runtime[0]=(
double) (end_finalizing - start_SCC)/CLOCKS_PER_SEC;
7316 runtime[1]=(
double) ( start_part-start_SCC)/CLOCKS_PER_SEC;
7317 runtime[2]=(
double) ( bisim_part.end_initial_part-start_part )/CLOCKS_PER_SEC;
7318 runtime[3]=(
double) ( end_part-bisim_part.end_initial_part )/CLOCKS_PER_SEC;
7319 runtime[4]=(
double) (end_finalizing-end_part )/CLOCKS_PER_SEC;
7320 if (runtime[0]>=60.0)
7322 int min[
sizeof(runtime)/
sizeof(runtime[0])];
7323 for (
unsigned i = 0; i <
sizeof(runtime)/
sizeof(runtime[0]); ++i)
7325 min[i] =
static_cast<
int>(runtime[i]) / 60;
7326 runtime[i] -= 60 * min[i];
7330 int h[
sizeof(runtime)/
sizeof(runtime[0])];
7331 for (
unsigned i=0; i <
sizeof(runtime)/
sizeof(runtime[0]); ++i)
7336 int width =
static_cast<
int>(std::log10(h[0])) + 1;
7338 mCRL2log(log::debug) << std::fixed << std::setprecision(prec)
7339 <<
"Time spent on contracting SCCs: " << std::setw(width) << h[1] <<
"h " << std::setw(2) << min[1] <<
"min " << std::setw(prec+3) << runtime[1] <<
"s\n"
7340 "Time spent on initial partition:" << std::setw(width) << h[2] <<
"h " << std::setw(2) << min[2] <<
"min " << std::setw(prec+3) << runtime[2] <<
"s\n"
7341 "Time spent on stabilize+refine: " << std::setw(width) << h[3] <<
"h " << std::setw(2) << min[3] <<
"min " << std::setw(prec+3) << runtime[3] <<
"s\n"
7342 "Time spent on finalizing: " << std::setw(width) << h[4] <<
"h " << std::setw(2) << min[4] <<
"min " << std::setw(prec+3) << runtime[4] <<
"s\n"
7343 "Total CPU time: " << std::setw(width) << h[0] <<
"h " << std::setw(2) << min[0] <<
"min " << std::setw(prec+3) << runtime[0] <<
"s\n"
7344 "BENCHMARK TIME: " <<
static_cast<
double>(end_part-start_part)/CLOCKS_PER_SEC <<
"\n"
7345 << std::defaultfloat;
7349 mCRL2log(log::debug) << std::fixed << std::setprecision(prec)
7350 <<
"Time spent on contracting SCCs: " << std::setw(2) << min[1] <<
"min " << std::setw(prec+3) << runtime[1] <<
"s\n"
7351 "Time spent on initial partition:" << std::setw(2) << min[2] <<
"min " << std::setw(prec+3) << runtime[2] <<
"s\n"
7352 "Time spent on stabilize+refine: " << std::setw(2) << min[3] <<
"min " << std::setw(prec+3) << runtime[3] <<
"s\n"
7353 "Time spent on finalizing: " << std::setw(2) << min[4] <<
"min " << std::setw(prec+3) << runtime[4] <<
"s\n"
7354 "Total CPU time: " << std::setw(2) << min[0] <<
"min " << std::setw(prec+3) << runtime[0] <<
"s\n"
7355 "BENCHMARK TIME: " <<
static_cast<
double>(end_part-start_part)/CLOCKS_PER_SEC <<
"\n"
7356 << std::defaultfloat;
7361 mCRL2log(log::debug) << std::fixed << std::setprecision(prec)
7362 <<
"Time spent on contracting SCCs: " << std::setw(prec+3) << runtime[1] <<
"s\n"
7363 "Time spent on initial partition:" << std::setw(prec+3) << runtime[2] <<
"s\n"
7364 "Time spent on stabilize+refine: " << std::setw(prec+3) << runtime[3] <<
"s\n"
7365 "Time spent on finalizing: " << std::setw(prec+3) << runtime[4] <<
"s\n"
7366 "Total CPU time: " << std::setw(prec+3) << runtime[0] <<
"s\n"
7367 "BENCHMARK TIME: " <<
static_cast<
double>(end_part-start_part)/CLOCKS_PER_SEC <<
"\n"
7368 << std::defaultfloat;
7394template <
class LTS_TYPE>
7395bool destructive_bisimulation_compare_gj_lazy_BLC(LTS_TYPE& l1, LTS_TYPE& l2,
7396 const bool branching =
false,
const bool preserve_divergence =
false,
7397 const bool generate_counter_examples =
false,
7398 const std::string& =
"",
7401 if (generate_counter_examples)
7403 mCRL2log(log::warning) <<
"The GJ25 branching bisimulation "
7404 "algorithm does not generate counterexamples.\n";
7406 std::size_t init_l2(l2.initial_state() + l1.num_states());
7407 detail::merge(l1, std::move(l2));
7412 detail::scc_partitioner<LTS_TYPE> scc_part(l1);
7413 scc_part.replace_transition_system(preserve_divergence);
7414 init_l2 = scc_part.get_eq_class(init_l2);
7415 }
else { assert(!preserve_divergence); }
7416 assert(1 < l1.num_states());
7417 bisim_partitioner_gj_lazy_BLC<LTS_TYPE> bisim_part(l1,
7418 branching, preserve_divergence);
7420 return bisim_part.in_same_class(l1.initial_state(), init_l2);
7441template <
class LTS_TYPE>
7442inline bool bisimulation_compare_gj_lazy_BLC(
const LTS_TYPE& l1,
7444 const bool branching =
false,
7445 const bool preserve_divergence =
false)
7447 LTS_TYPE l1_copy(l1);
7448 LTS_TYPE l2_copy(l2);
7449 return destructive_bisimulation_compare_gj_lazy_BLC(l1_copy, l2_copy,
7450 branching, preserve_divergence);
#define mCRL2complexity(unit, call, info_for_debug)
Assigns work to a counter and checks for errors.
aterm & operator=(const aterm &other) noexcept=default
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
std::size_t m_top_of_stack
static constexpr std::size_t maximal_size_of_stack
std::array< unprotected_aterm_core, maximal_size_of_stack > m_stack
void initialise(const term_balanced_tree< Term > &tree)
const Term & dereference() const
Dereference operator.
iterator(const iterator &other)
bool equal(const iterator &other) const
Equality operator.
iterator(const term_balanced_tree< Term > &tree)
void increment()
Increments the iterator.
bool is_node() const
Returns true iff the tree is a node with a left and right subtree.
static void make_tree_helper(aterm &result, ForwardTraversalIterator &p, const std::size_t size, Transformer transformer)
term_balanced_tree & operator=(const term_balanced_tree &) noexcept=default
Assignment operator.
size_type size() const
Returns the size of the term_balanced_tree.
term_balanced_tree(term_balanced_tree &&) noexcept=default
Move constructor.
bool empty() const
Returns true if tree is empty.
static const aterm & empty_tree()
static void make_tree(aterm &result, ForwardTraversalIterator &p, const std::size_t size, Transformer transformer)
term_balanced_tree(ForwardTraversalIterator first, const std::size_t size)
Creates an term_balanced_tree with a copy of a range.
static const function_symbol & tree_single_node_function()
const aterm & left_branch() const
Get the left branch of the tree.
term_balanced_tree(const term_balanced_tree &) noexcept=default
Copy constructor.
term_balanced_tree(ForwardTraversalIterator first, const std::size_t size, Transformer transformer)
Creates an term_balanced_tree with a copy of a range, where a transformer is applied to each term bef...
static const function_symbol & tree_node_function()
const Term & operator[](std::size_t position) const
Element indexing operator.
iterator begin() const
Returns an iterator pointing to the beginning of the term_balanced_tree.
iterator end() const
Returns an iterator pointing to the end of the term_balanced_tree.
term_balanced_tree()
Default constructor. Creates an empty tree.
const aterm & right_branch() const
Get the left branch of the tree.
term_balanced_tree & operator=(term_balanced_tree &&) noexcept=default
Move assign operator.
term_balanced_tree(const aterm &tree)
Construction from aterm.
const Term & element_at(std::size_t position, std::size_t size) const
Get an element at the indicated position.
static const function_symbol & tree_empty_function()
friend void make_term_balanced_tree(term_balanced_tree< Term1 > &result, ForwardTraversalIterator p, std::size_t size, Transformer transformer)
term_balanced_tree(detail::_term_appl *t)
A unordered_map class in which aterms can be stored.
data_expression & operator=(data_expression &&) noexcept=default
sort_expression sort() const
Returns the sort of the data expression.
data_expression(const data_expression &) noexcept=default
Move semantics.
data_expression(data_expression &&) noexcept=default
Rewriter that operates on data expressions.
data_expression operator()(const data_expression &d) const
Rewrites a data expression.
void add_sort(const basic_sort &s)
Adds a sort to this specification.
\brief An untyped parameter
Action rename specification.
\brief A timed multi-action
multi_action(const multi_action &) noexcept=default
Move semantics.
const process::action_list & actions() const
multi_action(const process::action_list &actions=process::action_list(), data::data_expression time=data::undefined_real())
Constructor. Actions are sorted to establish the sorted-storage invariant.
This class contains labels for probabilistic transistions, consisting of a numerator and a denumerato...
static const data::rewriter & m_rewriter()
static probabilistic_data_expression one()
Constant one.
probabilistic_data_expression operator+(const probabilistic_data_expression &other) const
Standard addition operator. Note that the expression is not evaluated. For this the rewriter has to b...
probabilistic_data_expression(const data::data_expression &d)
Construct a probabilistic_data_expression from a data_expression, which must be of sort real.
bool operator==(const probabilistic_data_expression &other) const
probabilistic_data_expression(std::size_t enumerator, std::size_t denominator)
bool operator!=(const probabilistic_data_expression &other) const
bool operator>=(const probabilistic_data_expression &other) const
bool operator<(const probabilistic_data_expression &other) const
bool operator<=(const probabilistic_data_expression &other) const
bool operator>(const probabilistic_data_expression &other) const
probabilistic_data_expression(const std::string &enumerator, const std::string &denominator)
probabilistic_data_expression operator-(const probabilistic_data_expression &other) const
Standard subtraction operator.
static data::data_specification data_specification_with_real()
probabilistic_data_expression()
static probabilistic_data_expression zero()
Constant zero.
Linear process specification.
STATE & state()
Get the state in a state probability pair.
PROBABILITY m_probability
state_probability_pair(state_probability_pair &&p)=default
state_probability_pair & operator=(state_probability_pair &&p)=default
state_probability_pair(const state_probability_pair &p)=default
Copy constructor;.
state_probability_pair & operator=(const state_probability_pair &p)=default
Standard assignment.
const PROBABILITY & probability() const
get the probability from a state proability pair.
const STATE & state() const
Get the state from a state probability pair.
PROBABILITY & probability()
Set the probability in a state probability pair.
state_probability_pair(const STATE &state, const PROBABILITY &probability)
constructor.
bool operator==(const state_probability_pair &other) const
Standard equality operator.
Linear process specification.
A class containing the values for action labels for the .lts format.
action_label_lts & operator=(const action_label_lts &)=default
Copy assignment.
void hide_actions(const std::vector< std::string > &tau_actions)
Hide the actions with labels in tau_actions.
action_label_lts(const action_label_lts &)=default
Copy constructor.
static const action_label_lts & tau_action()
action_label_lts(const mcrl2::lps::multi_action &a)
Constructor.
action_label_lts()=default
Default constructor.
void set_truths(formula &f)
Compute and set the truth values of a formula f.
block_index_type target(observation_t obs)
state_type max_state_index
level_type gca_level(const block_index_type B1, const block_index_type B2)
Auxiliarry function that computes the level of the greatest common ancestor. In other words a lvl i s...
std::vector< block > blocks
std::vector< state_type > block_index_of_a_state
label_type label(observation_t obs)
bisim_partitioner_minimal_depth(LTS_TYPE &l, const std::size_t init_l2)
Creates a bisimulation partitioner for an LTS.
std::set< block_index_type > partition
mcrl2::state_formulas::state_formula dist_formula_mindepth(const std::size_t s, const std::size_t t)
Creates a state formula that distinguishes state s from state t.
formula distinguish(const block_index_type b1, const block_index_type b2)
Creates a formula that distinguishes a block b1 from the block b2.
std::vector< block_index_type > BL
~bisim_partitioner_minimal_depth()=default
Destroys this partitioner.
std::vector< bool > block_flags
std::vector< block_index_type > to_be_processed
regular_formulas::regular_formula create_regular_formula(const mcrl2::lps::multi_action &a) const
create_regular_formula Creates a regular formula that represents action a
bool in_same_class(const std::size_t s, const std::size_t t)
block_index_type lift_block(const block_index_type B1, level_type goal)
mcrl2::state_formulas::state_formula conjunction(std::vector< formula > &conjunctions)
conjunction Creates a conjunction of state formulas
std::vector< bool > state_flags
mcrl2::state_formulas::state_formula convert_formula(formula &f)
void split_BL(level_type lvl)
Performs the splits based on the blocks in Bsplit and the flags set in state_flags.
bool refine_partition(level_type lvl)
std::vector< bool > block_flags
state_type max_state_index
mcrl2::state_formulas::state_formula conjunction(std::set< mcrl2::state_formulas::state_formula > terms) const
conjunction Creates a conjunction of state formulas
regular_formulas::regular_formula create_regular_formula(const mcrl2::lts::action_label_string &a) const
create_regular_formula Creates a regular formula that represents action a
regular_formulas::regular_formula create_regular_formula(const mcrl2::lps::multi_action &a) const
create_regular_formula Creates a regular formula that represents action a
std::vector< bool > block_is_in_to_be_processed
std::vector< bool > state_flags
std::map< block_index_type, block_index_type > right_child
std::vector< block_index_type > BL
bool in_same_class(const std::size_t s, const std::size_t t) const
Returns whether two states are in the same bisimulation equivalence class.
mcrl2::state_formulas::state_formula until_formula(const mcrl2::state_formulas::state_formula &phi1, const label_type &a, const mcrl2::state_formulas::state_formula &phi2)
until_formula Creates a state formula that corresponds to the until operator phi1phi2 from HMLU
std::size_t get_eq_class(const std::size_t s) const
Gives the bisimulation equivalence class number of a state.
bisim_partitioner(LTS_TYPE &l, const bool branching=false, const bool preserve_divergence=false, const bool generate_counter_examples=false)
Creates a bisimulation partitioner for an LTS.
~bisim_partitioner()=default
Destroys this partitioner.
std::map< block_index_type, label_type > split_by_action
std::size_t num_eq_classes() const
Gives the number of bisimulation equivalence classes of the LTS.
mcrl2::state_formulas::state_formula counter_formula(std::size_t s, std::size_t t)
Creates a state formula that distinguishes state s from state t.
void order_recursively_on_tau_reachability(const state_type s, std::map< state_type, std::vector< state_type > > &inert_transition_map, std::vector< non_bottom_state > &new_non_bottom_states, std::set< state_type > &visited)
std::vector< block_index_type > to_be_processed
std::map< block_index_type, block_index_type > split_by_block
void refine_partion_with_respect_to_divergences()
void replace_transition_system(const bool branching, const bool preserve_divergences)
Replaces the transition relation of the current lts by the transitions of the bisimulation reduced tr...
std::vector< block > blocks
void order_on_tau_reachability(std::vector< non_bottom_state > &non_bottom_states)
void split_the_blocks_in_BL(bool &partition_is_unstable, const label_type splitter_label, const block_index_type splitter_block)
void refine_partition_until_it_becomes_stable(const bool branching, const bool preserve_divergence)
void create_initial_partition(const bool branching, const bool preserve_divergences)
std::vector< state_type > block_index_of_a_state
mcrl2::state_formulas::state_formula counter_formula_aux(const block_index_type B1, const block_index_type B2)
void check_internal_consistency_of_the_partitioning_data_structure(const bool branching, const bool preserve_divergence) const
outgoing_transitions_per_state_action_t outgoing_transitions
function object to compare two constln_t pointers based on their contents
A class that can be used to store counterexample trees and.
lts_type type()
Provides the type of this lts, in casu lts_aut.
bool operator==(const lts_aut_base &) const
Standard equality function.
void swap(lts_aut_base &) noexcept
Standard swap function.
void swap(lts_dot_base &) noexcept
The standard swap function.
lts_type type() const
The lts_type of state_label_dot. In this case lts_dot.
void clear()
Clear the transitions system.
const std::vector< std::string > & state_element_values(std::size_t idx) const
Provides the vector of strings that correspond to the values of the number at position idx in a vecto...
std::size_t add_state_element_value(std::size_t idx, const std::string &s)
Adds a string to the state element values for the idx-th position in a state vector....
void swap(lts_fsm_base &other) noexcept
Standard swap function.
bool operator==(const lts_fsm_base &other) const
lts_type type() const
The lts_type of this labelled transition system. In this case lts_fsm.
std::string state_element_value(std::size_t parameter_index, std::size_t element_index) const
Returns the element_index'th element for the parameter with index parameter_index.
std::string state_label_to_string(const state_label_fsm &l) const
Pretty print a state value of this FSM.
a base class for lts_lts_t and probabilistic_lts_t.
static lts_type type()
Yields the type of this lts, in this case lts_lts.
void set_process_parameters(const data::variable_list ¶ms)
Set the state parameters for this LTS.
lts_lts_base()=default
Default constructor.
bool operator==(const lts_lts_base &other) const
Standard equality function;.
process::action_label_list m_action_decls
void set_action_label_declarations(const process::action_label_list &decls)
Set the action label information for this LTS.
const data::variable & process_parameter(std::size_t i) const
Returns the i-th parameter of the state vectors stored in this LTS.
data::data_specification m_data_spec
const data::variable_list & process_parameters() const
Return the process parameters stored in this LTS.
void set_data(const data::data_specification &spec)
Set the mCRL2 data specification of this LTS.
void swap(lts_lts_base &l) noexcept
const process::action_label_list & action_label_declarations() const
Return action label declarations stored in this LTS.
data::variable_list m_parameters
A simple labelled transition format with only strings as action labels.
void load(const std::string &filename)
Load the labelled transition system from a file.
void load(std::istream &is)
Load the labelled transition system from an input stream.
void save(const std::string &filename) const
Save the labelled transition system to file.
A class to contain labelled transition systems in graphviz format.
void save(const std::string &filename) const
Save the labelled transition system to a file.
void save(std::ostream &os) const
Save the labelled transition system to a stream.
The class lts_fsm_t contains labelled transition systems in .fsm format.
void load(const std::string &filename)
Save the labelled transition system to file.
void save(const std::string &filename) const
Save the labelled transition system to file.
This class contains labelled transition systems in .lts format.
lts_lts_t()=default
Creates an object containing no information.
void save(const std::string &filename) const
Save the labelled transition system to file.
void load(const std::string &filename)
Load the labelled transition system from file.
A simple labelled transition format with only strings as action labels.
void load(const std::string &filename)
Load the labelled transition system from a file.
void load(std::istream &is)
Load the labelled transition system from an input stream.
void save(const std::string &filename) const
Save the labelled transition system to file.
A class to contain labelled transition systems in graphviz format.
void save(std::ostream &os) const
Save the labelled transition system to a stream.
void save(const std::string &filename) const
Save the labelled transition system to a file.
The class lts_fsm_t contains labelled transition systems in .fsm format.
This class contains probabilistic labelled transition systems in .lts format.
probabilistic_lts_lts_t()=default
Creates an object containing no information.
void load(const std::string &filename)
Load the labelled transition system from file.
void save(const std::string &filename) const
Save the labelled transition system to file.
A class that contains a labelled transition system.
probabilistic_lts(probabilistic_lts &&other)=default
Standard move constructor.
void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T &state)
Sets the probabilistic initial state number of this LTS.
probabilistic_lts()=default
Creates an empty LTS.
const PROBABILISTIC_STATE_T & initial_probabilistic_state() const
Gets the initial state number of this LTS.
bool operator==(const probabilistic_lts &other) const
Standard equality operator.
labels_size_type num_probabilistic_states() const
Gets the number of probabilistic states of this LTS.
static constexpr bool is_probabilistic_lts
An indicator that this is a probabilistic lts.
void clear_probabilistic_states()
Clear the probabilistic states in this probabilistic transitions system.
states_size_type add_and_reset_probabilistic_state(PROBABILISTIC_STATE_T &s)
Adds a probabilistic state to this LTS and resets the state to empty.
void clear()
Clear the transitions system.
probabilistic_lts & operator=(probabilistic_lts &&other)=default
Standard assignment move operator.
void swap(probabilistic_lts &other) noexcept
Swap this lts with the supplied supplied LTS.
probabilistic_lts & operator=(const probabilistic_lts &other)=default
Standard assignment operator.
std::vector< PROBABILISTIC_STATE_T > m_probabilistic_states
probabilistic_lts(const probabilistic_lts &other)=default
Standard copy constructor.
states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T &s)
Adds a probabilistic state to this LTS.
states_size_type initial_state() const
PROBABILISTIC_STATE_T m_init_probabilistic_state
A class that contains a probabilistic state.
void set(const STATE &s)
Set this probabilistic state to a single state with probability one.
const_iterator begin() const
Gets an iterator over pairs of state and probability. This can only be used when the state is stored ...
void construct_internal_vector_representation()
Guarantee that this probabilistic state is internally stored as a vector, such that begin/end,...
probabilistic_state & operator=(const probabilistic_state &other)
Copy assignment constructor.
const_reverse_iterator rbegin() const
Gets a reverse iterator over pairs of state and probability. This can only be used when the state is ...
std::size_t size() const
Gets the number of probabilistic states in the vector representation of this state....
bool operator!=(const probabilistic_state &other) const
Standard equality operator.
iterator begin()
Gets an iterator over pairs of state and probability. This can only be used if the state is internall...
probabilistic_state & operator=(probabilistic_state &&other)=default
Move assignment operator.
STATE get() const
Get a probabilistic state if is is simple, i.e., consists of a single state.
void swap(probabilistic_state &other) noexcept
Swap this probabilistic state.
iterator end()
Gets the end iterator over pairs of state and probability.
reverse_iterator rbegin()
Gets a reverse iterator over pairs of state and probability. This can only be used if the state is in...
std::vector< state_probability_pair > m_probabilistic_state
const_iterator end() const
Gets the end iterator over pairs of state and probability.
reverse_iterator rend()
Gets the reverse end iterator over pairs of state and probability.
bool operator==(const probabilistic_state &other) const
Standard equality operator.
void clear()
Makes the probabilistic state empty.
probabilistic_state(probabilistic_state &&other)=default
Move constructor.
probabilistic_state(const STATE_PROBABILITY_PAIR_ITERATOR begin, const STATE_PROBABILITY_PAIR_ITERATOR end)
Creates a probabilistic state on the basis of state_probability_pairs.
STATE maximal_state() const
Provides the maximal state index in a probabilistic state.
probabilistic_state(const probabilistic_state &other)
Copy constructor.
void shrink_to_fit()
If a probabilistic state is ready, shrinking it to minimal size might be useful to reduce its memory ...
probabilistic_state()
Default constructor.
probabilistic_state(const STATE &s)
Constructor of a probabilistic state from a non probabilistic state.
void add(const STATE &s, const PROBABILITY &p)
Add a state with a probability to the probabilistic state.
const_reverse_iterator rend() const
Gets the reverse end iterator over pairs of state and probability.
Class for computing the signature for strong bisimulation.
Class for computing the signature for branching bisimulation.
Class for computing the signature for divergence preserving branching bisimulation.
Signature based reductions for labelled transition systems.
This class contains labels for states in dot format.
void set_name(const std::string &s)
This method sets the name of the state label to the string s.
std::string name() const
This method returns the string in the name field of a state label.
std::string label() const
This method returns the label in the name field of a state label.
void set_label(const std::string &s)
This method sets the label field of the state label to the string s.
state_label_dot(const std::string &state_name, const std::string &state_label)
A constructor setting the name and label of this state label to the indicated values.
std::string m_state_label
bool operator==(const state_label_dot &l) const
Standard comparison operator, comparing both the string in the name field, as well as the one in the ...
bool operator!=(const state_label_dot &l) const
Standard inequality operator. Just the negation of equality.
state_label_dot()=default
The default constructor.
This class contains state labels for the fsm format.
state_label_fsm()=default
Default constructor. The label becomes an empty vector.
state_label_fsm(const state_label_fsm &)=default
Copy constructor.
state_label_fsm & operator=(const state_label_fsm &)=default
Copy assignment.
static state_label_fsm number_to_label(const std::size_t n)
Create a state label consisting of a number as the only list element.
state_label_fsm(const std::vector< std::size_t > &v)
Default constructor. The label is set to the vector v.
state_label_fsm operator+(const state_label_fsm &l) const
An operator to concatenate two state labels. Fsm labels cannot be concatenated. Therefore,...
This class contains state labels for an labelled transition system in .lts format.
state_label_lts(const state_label_lts &)=default
Copy constructor.
state_label_lts operator+(const state_label_lts &l) const
An operator to concatenate two state labels.
state_label_lts(const super &l)
Construct a state label out of list of balanced trees of data expressions, representing a state label...
state_label_lts()=default
Default constructor.
state_label_lts(const lps::state &l)
Construct a state label out of a balanced tree of data expressions, representing a state label.
state_label_lts & operator=(const state_label_lts &)=default
Copy assignment.
static state_label_lts number_to_label(const std::size_t n)
Create a state label consisting of a number as the only list element.
state_label_lts(const CONTAINER &l)
Construct a single state label out of the elements in a container.
Process specification consisting of a data specification, action labels, a sequence of process equati...
\brief An untyped multi action or data application
#define PRINT_SG_PL(counter, sg_string, pl_string)
#define ONLY_IF_DEBUG(...)
include something in Debug mode
#define PRINT_INT_PERCENTAGE(num, denom)
#define INIT_WITHOUT_BLC_SETS
#define abort_if_non_bottom_size_too_large_NewBotSt(i)
#define bottom_size(coroutine)
#define new_start_bottom_states(idx)
#define new_end_bottom_states(idx)
#define abort_if_size_too_large(coroutine, i)
#define non_bottom_states_NewBotSt
#define new_end_bottom_states_NewBotSt
#define abort_if_bottom_size_too_large(coroutine)
#define bottom_and_non_bottom_size(coroutine)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
global_function_symbol g_tree_node("@node@", 2)
global_function_symbol g_empty("@empty@", 0)
aterm g_empty_tree(g_empty)
global_function_symbol g_single_tree_node("@single_node@", 1)
std::string pp(const term_balanced_tree< Term > t)
bool is_aterm_balanced_tree(const aterm &t)
void make_term_balanced_tree(term_balanced_tree< Term > &result, ForwardTraversalIterator p, std::size_t size, Transformer transformer)
static data_specification const & default_specification()
Namespace for system defined sort bool_.
const function_symbol & false_()
Constructor for function symbol false.
const function_symbol & true_()
Constructor for function symbol true.
Namespace for system defined sort int_.
application cint(const data_expression &arg0)
Application of function symbol @cInt.
const basic_sort & int_()
Constructor for sort expression Int.
Namespace for system defined sort nat.
const basic_sort & nat()
Constructor for sort expression Nat.
application cnat(const data_expression &arg0)
Application of function symbol @cNat.
Namespace for system defined sort pos.
const basic_sort & pos()
Constructor for sort expression Pos.
Namespace for system defined sort real_.
data_expression & real_one()
application creal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @cReal.
data_expression & real_zero()
const basic_sort & real_()
Constructor for sort expression Real.
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
application minus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
application less(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <.
bool is_untyped_data_parameter(const atermpp::aterm &x)
application equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ==.
std::pair< std::set< data::variable >, std::set< data::variable > > read_write_parameters(const lps::action_summand &summand, const std::set< data::variable > &process_parameters)
Computes the read and written process parameters for the given summand.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
multi_action complete_multi_action(process::untyped_multi_action &x, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
void remove_common_divisor(std::size_t &enumerator, std::size_t &denominator)
void complete_action_rename_specification(action_rename_specification &x, const lps::stochastic_specification &spec)
process::untyped_multi_action parse_multi_action_new(const std::string &text)
multi_action complete_multi_action(process::untyped_multi_action &x, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
std::size_t greatest_common_divisor(std::size_t x, std::size_t y)
action_rename_specification parse_action_rename_specification_new(const std::string &text)
The main namespace for the LPS library.
specification parse_linear_process_specification(const std::string &text)
Parses a linear process specification from a string.
void complete_data_specification(stochastic_specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
multi_action parse_multi_action(const std::string &text, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
Parses a multi_action from a string.
void parse_lps(std::istream &, Specification &)
process::action parse_action(const std::string &text, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
Parses an action from a string.
void complete_data_specification(specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
std::string pp(const probabilistic_data_expression &l)
multi_action parse_multi_action(std::stringstream &in, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
Parses a multi_action from an input stream.
action_rename_specification parse_action_rename_specification(std::istream &in, const lps::stochastic_specification &spec)
Parses a process specification from an input stream.
std::ostream & operator<<(std::ostream &out, const probabilistic_data_expression &x)
Pretty print to an outstream.
multi_action parse_multi_action(std::stringstream &in, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
Parses a multi_action from an input stream.
action_rename_specification parse_action_rename_specification(const std::string &spec_string, const lps::stochastic_specification &spec)
Parses an action rename specification. Parses an action rename specification. If the action rename sp...
void parse_lps< specification >(std::istream &from, specification &result)
void make_state(state &result, ForwardTraversalIterator p, const std::size_t size)
void parse_lps< stochastic_specification >(std::istream &from, stochastic_specification &result)
Parses a stochastic linear process specification from an input stream.
std::string pp(const lps::state &x)
multi_action parse_multi_action(const std::string &text, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
Parses a multi_action from a string.
void parse_lps(const std::string &text, Specification &result)
specification parse_linear_process_specification(std::istream &spec_stream)
Parses a linear process specification from an input stream.
void make_state(state &result, ForwardTraversalIterator p, const std::size_t size, Transformer transformer)
bool bisimulation_compare(const LTS_TYPE &l1, const LTS_TYPE &l2, bool branching=false, bool preserve_divergences=false, bool generate_counter_examples=false, const std::string &counter_example_file="", bool structured_output=false)
Checks whether the two initial states of two lts's are strong or branching bisimilar.
lts_type guess_format(std::string const &s, const bool be_verbose)
Determines the LTS format from a filename by its extension.
static const std::array< std::string, 5 > extension_strings
std::string supported_lts_formats_text(lts_type default_format, const std::set< lts_type > &supported)
Gives a textual list describing supported LTS formats.
std::string supported_lts_formats_text(const std::set< lts_type > &supported)
Gives a textual list describing supported LTS formats.
bool destructive_bisimulation_compare_minimal_depth(LTS_TYPE &l1, LTS_TYPE &l2, const std::string &counter_example_file)
std::string string_for_type(const lts_type type)
Gives a string representation of an LTS format.
void unmark_explicit_divergence_transitions(LTS_TYPE &l, const std::size_t divergent_transition_label)
std::string mime_type_for_type(const lts_type type)
Gives the MIME type associated with an LTS format.
void get_trans(const outgoing_transitions_per_state_t &begin, tree_set_store &tss, std::ptrdiff_t d, std::vector< transition > &d_trans, LTS_TYPE &aut)
lts_type parse_format(std::string const &s)
Determines the LTS format from a format specification string.
static const std::array< std::string, 5 > type_strings
std::string extension_for_type(const lts_type type)
Gives the filename extension associated with an LTS format.
LABEL_TYPE make_divergence_label(const std::string &s)
const std::set< lts_type > & supported_lts_formats()
Gives the set of all supported LTS formats.
std::string lts_extensions_as_string(const std::set< lts_type > &supported)
Gives a list of extensions for supported LTS formats.
std::string lts_extensions_as_string(const std::string &sep, const std::set< lts_type > &supported)
Gives a list of extensions for supported LTS formats.
std::size_t mark_explicit_divergence_transitions(LTS_TYPE &l)
bool destructive_bisimulation_compare(LTS_TYPE &l1, LTS_TYPE &l2, bool branching=false, bool preserve_divergences=false, bool generate_counter_examples=false, const std::string &counter_example_file="", bool structured_output=false)
Checks whether the two initial states of two lts's are strong or branching bisimilar.
void bisimulation_reduce(LTS_TYPE &l, bool branching=false, bool preserve_divergences=false)
Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
bool lts_named_cmp(const std::array< std::string, Size > &N, T a, T b)
static const std::array< std::string, 5 > type_desc_strings
static const std::array< std::string, 5 > mime_type_strings
static const std::set< lts_type > & initialise_supported_lts_formats()
std::string pp(const state_label_dot &l)
Pretty print function for a state_label_dot. Only prints the label field.
std::string pp(const state_label_lts &label)
Pretty print a state value of this LTS.
bool is_deterministic(const LTS_TYPE &l)
Checks whether this LTS is deterministic.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(const std::vector< transition > &trans)
Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
action_label_lts parse_lts_action(const std::string &multi_action_string, const data::data_specification &data_spec, lps::multi_action_type_checker &typechecker)
Parse a string into an action label.
void group_transitions_on_label(std::vector< transition > &transitions, std::function< std::size_t(const transition &)> get_label, const std::size_t number_of_labels, const std::size_t tau_label_index)
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
std::string pp(const state_label_fsm &label)
Pretty print an fsm state label.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(const std::vector< transition > &trans)
Provide the transitions as a multimap accessible per from state and label.
void sort_transitions(std::vector< transition > &transitions, const std::set< transition::size_type > &hidden_label_set, transition_sort_style ts=src_lbl_tgt)
Sorts the transitions using a sort style.
void determinise(LTS_TYPE &l)
Determinises this LTS.
std::string pp(const probabilistic_state< STATE, PROBABILITY > &l)
std::ostream & operator<<(std::ostream &out, const probabilistic_state< STATE, PROBABILITY > &l)
Pretty print to an outstream.
void reduce(LTS_TYPE &l, lts_equivalence eq)
Applies a reduction algorithm to this LTS.
bool compare(const LTS_TYPE &l1, const LTS_TYPE &l2, lts_equivalence eq, bool generate_counter_examples=false, const std::string &counter_example_file="", bool structured_output=false)
Checks whether this LTS is equivalent to another LTS.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(const std::vector< transition > &trans, const std::set< transition::size_type > &hide_label_set)
Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
bool destructive_compare(LTS_TYPE &l1, LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file=std::string(), const bool structured_output=false)
Checks whether this LTS is equivalent to another LTS.
std::string pp(const action_label_lts &l)
Print the action label to string.
bool destructive_compare(LTS_TYPE &l1, LTS_TYPE &l2, lts_preorder pre, bool generate_counter_example, const std::string &counter_example_file="", bool structured_output=false, lps::exploration_strategy strategy=lps::es_breadth, bool preprocess=true)
Checks whether this LTS is smaller than another LTS according to a preorder.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(const std::vector< transition > &trans, const std::set< transition::size_type > &hide_label_set)
Provide the transitions as a multimap accessible per from state and label.
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
Merge the second lts into the first lts.
bool reachability_check(lts< SL, AL, BASE > &l, bool remove_unreachable=false)
Checks whether all states in this LTS are reachable from the initial state and remove unreachable sta...
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator &i)
From state of an iterator exploring transitions per outgoing state and action.
void group_transitions_on_label(const std::vector< transition >::iterator begin, const std::vector< transition >::iterator end, std::function< std::size_t(const transition &)> get_label, std::vector< std::pair< std::size_t, std::size_t > > &count_sum_transitions_per_action, const std::size_t tau_label_index=0, std::vector< std::size_t > &todo_stack=bogus_todo_stack)
bool reachability_check(probabilistic_lts< SL, AL, PROBABILISTIC_STATE, BASE > &l, bool remove_unreachable=false)
Checks whether all states in a probabilistic LTS are reachable from the initial state and remove unre...
bool compare(const LTS_TYPE &l1, const LTS_TYPE &l2, lts_preorder pre, bool generate_counter_example, const std::string &counter_example_file="", bool structured_output=false, lps::exploration_strategy strategy=lps::es_breadth, bool preprocess=true)
Checks whether this LTS is smaller than another LTS according to a preorder.
The main namespace for the Process library.
bool is_linear(const process_specification &p, bool verbose=false)
Returns true if the process specification is linear.
bool is_untyped_multi_action(const atermpp::aterm &x)
void swap(atermpp::term_balanced_tree< T > &t1, atermpp::term_balanced_tree< T > &t2) noexcept
Swaps two balanced trees.
#define USE_POOL_ALLOCATOR
static const atermpp::aterm StateMay
static const atermpp::aterm StateOr
static const atermpp::aterm UntypedRegFrm
static const atermpp::aterm StateFrm
static const atermpp::aterm StateYaled
static const atermpp::aterm RegAlt
static const atermpp::aterm ActNot
static const atermpp::aterm ActImp
static const atermpp::aterm ActTrue
static const atermpp::aterm StateInfimum
static const atermpp::aterm StateAnd
static const atermpp::aterm StateExists
static const atermpp::aterm RegTrans
static const atermpp::aterm ActOr
static const atermpp::aterm StateConstantMultiplyAlt
static const atermpp::aterm ActFrm
static const atermpp::aterm ActForall
static const atermpp::aterm StateYaledTimed
static const atermpp::aterm ActFalse
static const atermpp::aterm StateFalse
static const atermpp::aterm RegFrm
static const atermpp::aterm StateDelay
static const atermpp::aterm StatePlus
static const atermpp::aterm StateMinus
static const atermpp::aterm StateNu
static const atermpp::aterm ActAnd
static const atermpp::aterm StateDelayTimed
static const atermpp::aterm StateSupremum
static const atermpp::aterm StateSum
static const atermpp::aterm ActAt
static const atermpp::aterm ActExists
static const atermpp::aterm StateMu
static const atermpp::aterm RegTransOrNil
static const atermpp::aterm StateVar
static const atermpp::aterm StateImp
static const atermpp::aterm RegSeq
static const atermpp::aterm StateTrue
static const atermpp::aterm StateForall
static const atermpp::aterm StateMust
static const atermpp::aterm StateNot
static const atermpp::aterm ActMultAct
static const atermpp::aterm StateConstantMultiply
std::vector< state_type > bottom_states
block_index_type parent_block_index
block_index_type block_index
void swap(block &b) noexcept
std::vector< transition > non_inert_transitions
std::vector< non_bottom_state > non_bottom_states
std::vector< state_type > inert_transitions
non_bottom_state(const state_type s, const std::vector< state_type > &it)
non_bottom_state(const state_type s)
std::vector< state_type > states
void swap(block &b) noexcept
block_index_type block_index
std::vector< transition > transitions
block_index_type parent_block_index
Converts a process expression into linear process format. Use the convert member functions for this.
lps::specification convert(const process_specification &p)
Converts a process_specification into a specification. Throws non_linear_process if a non-linear sub-...
Converts a process expression into linear process format. Use the convert member functions for this.
lps::stochastic_specification convert(const process_specification &p)
Converts a process_specification into a stochastic_specification. Throws non_linear_process if a non-...
std::size_t operator()(const atermpp::term_balanced_tree< T > &t) const
std::size_t operator()(const mcrl2::lps::probabilistic_data_expression &p) const
std::size_t operator()(const mcrl2::lps::state_probability_pair< STATE, PROBABILITY > &p) const
std::size_t operator()(const mcrl2::lts::action_label_lts &as) const
std::size_t operator()(const mcrl2::lts::probabilistic_state< STATE, PROBABILITY > &p) const