20#ifndef LIBLTS_BISIM_GJ_H
21#define LIBLTS_BISIM_GJ_H
28#define INIT_WITHOUT_BLC_SETS
30#include "mcrl2/lts/detail/check_complexity.h"
31#include "mcrl2/lts/detail/fixed_vector.h"
32#include "mcrl2/lts/detail/liblts_merge.h"
33#include "mcrl2/lts/detail/liblts_scc.h"
34#include "mcrl2/lts/detail/simple_list.h"
38#define linked_list simple_list
50template <
class LTS_TYPE>
class bisim_partitioner_gj;
52namespace bisimulation_gj
58struct constellation_type;
59struct transition_type;
60struct outgoing_transition_type;
62using state_index = std::size_t;
63using transition_index = std::size_t;
65using label_index = std::size_t;
66using outgoing_transitions_it=fixed_vector<outgoing_transition_type>::iterator;
67using outgoing_transitions_const_it =
68 fixed_vector<outgoing_transition_type>::const_iterator;
70constexpr constellation_type* null_constellation=
nullptr;
71constexpr transition_index null_transition=-1;
72constexpr label_index null_action=-1;
73constexpr state_index null_state=-1;
74constexpr block_type* null_block=
nullptr;
78constexpr transition_index undefined=0;
84 constexpr transition_index marked_range=
85 (std::numeric_limits<transition_index>::max()-2)/3;
87 enum subblocks { ReachAlw=0,
103 static inline constexpr transition_index marked(
enum subblocks subblock)
105 return assert(ReachAlw==subblock || AvoidSml==subblock ||
106 AvoidLrg==subblock || NewBotSt==subblock),
107 marked_range*subblock+1;
111 constexpr transition_index marked_NewBotSt=marked(NewBotSt);
static_assert(marked_NewBotSt<std::numeric_limits<transition_index>::max());
115 constexpr transition_index marked_HitSmall=marked_NewBotSt+1;
118 static inline constexpr bool is_in_marked_range_of
119 (transition_index counter,
enum subblocks subblock)
121 return assert(ReachAlw==subblock || AvoidSml==subblock || AvoidLrg==subblock),
122 counter-marked(subblock)<marked_range;
127template <
class CONTAINER>
128static inline void clear(CONTAINER& c)
130 if (c.size()>1000) { c=CONTAINER(); }
else { c.clear(); }
135using BLC_list_iterator = transition_index*;
136using BLC_list_iterator_or_null = transition_index*;
137using BLC_list_const_iterator =
const transition_index*;
140struct outgoing_transition_type
143 union iterator_or_counter
146 transition_index transitions;
148 BLC_list_iterator BLC_transitions;
150 iterator_or_counter()
154 void convert_to_iterator(BLC_list_iterator other)
156 transitions.~transition_index();
157 new (
static_cast<
void*>(&BLC_transitions)) BLC_list_iterator(other);
160 ~iterator_or_counter() { BLC_transitions.~BLC_list_iterator(); }
170 outgoing_transitions_it start_same_saC;
173 outgoing_transition_type() =
default;
175 outgoing_transition_type(
const outgoing_transitions_it sssaC)
177 start_same_saC(sssaC)
182struct state_in_block_pointer
184 state_in_block_pointer(fixed_vector<state_type_gj>::iterator new_ref_state)
185 : ref_state(new_ref_state)
188 state_in_block_pointer() =
default;
190 fixed_vector<state_type_gj>::iterator ref_state;
192 bool operator==(
const state_in_block_pointer& other)
const
194 return ref_state==other.ref_state;
197 bool operator!=(
const state_in_block_pointer& other)
const
199 return ref_state!=other.ref_state;
205class todo_state_vector
207 std::size_t m_todo_indicator=0;
208 std::vector<state_in_block_pointer> m_vec;
211 using const_iterator = std::vector<state_in_block_pointer>::const_iterator;
213 bool find(
const state_in_block_pointer s)
const
215 return std::find(m_vec.begin(), m_vec.end(), s)!=m_vec.end();
218 void add_todo(
const state_in_block_pointer s)
223 std::size_t todo_is_empty()
const
225 return m_vec.size()==m_todo_indicator;
229 state_in_block_pointer move_from_todo()
230 { assert(!todo_is_empty());
231 state_in_block_pointer result=m_vec[m_todo_indicator];
236 void swap_vec(std::vector<state_in_block_pointer>& other_vec)
238 m_vec.swap(other_vec);
242 std::size_t size()
const
247 std::size_t empty()
const
249 return m_vec.empty();
252 const_iterator begin()
const
254 return m_vec.begin();
257 const_iterator end()
const
262 const state_in_block_pointer* data()
const
267 const state_in_block_pointer* data_end()
const
269 return m_vec.data() + m_vec.size();
272 const state_in_block_pointer& front()
const
274 return m_vec.front();
277 void reserve(std::vector<state_in_block_pointer>::size_type new_cap)
279 m_vec.reserve(new_cap);
282 using iterator = std::vector<state_in_block_pointer>::iterator;
286 return m_vec.begin();
295 void add_todo(iterator begin, iterator end)
297 m_vec.insert(m_vec.end(), begin, end);
303 bisimulation_gj::clear(m_vec);
314 block_type* block=null_block;
316 std::vector<transition>::iterator start_incoming_transitions;
318 outgoing_transitions_it start_outgoing_transitions;
320 state_in_block_pointer* ref_states_in_blocks =
nullptr;
322 transition_index no_of_outgoing_block_inert_transitions=0;
328 transition_index counter=undefined;
331 template<
class LTS_TYPE>
332 std::string debug_id_short(
const bisim_partitioner_gj<LTS_TYPE>& partitioner)
const
334 assert(partitioner.m_states.data()<=
this);
335 assert(
this<partitioner.m_states.data_end());
336 return std::to_string(
this-partitioner.m_states.data());
340 template<
class LTS_TYPE>
341 std::string debug_id(
const bisim_partitioner_gj<LTS_TYPE>& partitioner)
const
343 return "state " + debug_id_short(partitioner);
346 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
347 mutable check_complexity::state_gj_counter_t work_counter;
355 BLC_list_iterator start_same_BLC;
361 BLC_list_iterator_or_null start_marked_BLC;
362 BLC_list_iterator end_same_BLC;
364 BLC_indicators(BLC_list_iterator start, BLC_list_iterator end,
bool is_stable)
365 : start_same_BLC(start),
366 start_marked_BLC(is_stable ?
nullptr : end),
368 { assert(
nullptr!=start_same_BLC); assert(
nullptr!=end_same_BLC);
369 assert(start_same_BLC<=end_same_BLC);
372 bool is_stable()
const
373 { assert(
nullptr!=start_same_BLC); assert(
nullptr!=end_same_BLC);
374 assert(
nullptr==start_marked_BLC || start_same_BLC<=start_marked_BLC);
375 assert(
nullptr==start_marked_BLC || start_marked_BLC<=end_same_BLC);
376 assert(start_same_BLC<=end_same_BLC);
377 return nullptr==start_marked_BLC;
382 bool has_marked_transitions()
const
388 return start_marked_BLC<end_same_BLC;
392 { assert(!is_stable());
393 start_marked_BLC=
nullptr;
397 { assert(is_stable());
398 start_marked_BLC=end_same_BLC;
401 bool operator==(
const BLC_indicators& other)
const
403 return start_same_BLC==other.start_same_BLC &&
404 start_marked_BLC==other.start_marked_BLC &&
405 end_same_BLC==other.end_same_BLC;
408 bool operator!=(
const BLC_indicators& other)
const
410 return !operator==(other);
415 template<
class LTS_TYPE>
416 std::string debug_id(
const bisim_partitioner_gj<LTS_TYPE>& partitioner,
417 const block_type* from_block=
nullptr)
const
419 assert(partitioner.m_BLC_transitions.data()<=start_same_BLC);
420 assert(
nullptr==start_marked_BLC || start_same_BLC<=start_marked_BLC);
421 assert(
nullptr==start_marked_BLC || start_marked_BLC<=end_same_BLC);
422 assert(start_same_BLC<=end_same_BLC);
423 assert(end_same_BLC<=partitioner.m_BLC_transitions.data_end());
424 std::string result(
"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))+
")");
425 if (start_same_BLC==end_same_BLC)
427 return "Empty "+result;
429 result +=
" from "+(
nullptr==from_block ? partitioner.m_states[partitioner.m_aut.get_transitions()[*start_same_BLC].from()].block : from_block)->debug_id(partitioner);
431 result += partitioner.m_states[partitioner.m_aut.get_transitions()[*start_same_BLC].to()].block->c.onstellation->debug_id(partitioner);
432 result +=
" containing the ";
433 if (std::distance(start_same_BLC, end_same_BLC)>1)
435 result+=std::to_string(std::distance(start_same_BLC, end_same_BLC));
436 result +=
" transitions ";
440 result +=
"transition ";
442 BLC_list_const_iterator iter = start_same_BLC;
443 if (start_marked_BLC == iter)
447 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
448 if (std::distance(start_same_BLC, end_same_BLC)>4)
451 result += start_marked_BLC == iter ?
" | " :
", ";
452 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
453 result += std::next(iter) == start_marked_BLC ?
" | ..."
454 : (!is_stable() && start_marked_BLC>std::next(iter) && start_marked_BLC<=end_same_BLC-3 ?
", ..|.." :
", ...");
455 iter = end_same_BLC-3;
457 while (++iter!=end_same_BLC)
459 result += start_marked_BLC == iter ?
" | " :
", ";
460 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
462 if (start_marked_BLC == iter)
469 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
470 mutable check_complexity::BLC_gj_counter_t work_counter;
477struct transition_type
482 transitions_per_block_to_constellation{};
483 outgoing_transitions_it ref_outgoing_transitions;
491 template<
class LTS_TYPE>
492 std::string debug_id_short(
const bisim_partitioner_gj<LTS_TYPE>& partitioner)
const
494 assert(partitioner.m_transitions.data()<=
this);
495 assert(
this<partitioner.m_transitions.data_end());
496 const transition& t=partitioner.m_aut.get_transitions()
497 [
this-partitioner.m_transitions.data()];
498 return partitioner.m_states[t.from()].debug_id_short(partitioner) +
" -" +
499 pp(partitioner.m_aut.action_label(t.label())) +
"-> " +
500 partitioner.m_states[t.to()].debug_id_short(partitioner);
505 template<
class LTS_TYPE>
506 std::string debug_id(
const bisim_partitioner_gj<LTS_TYPE>& partitioner)
const
508 return "transition " + debug_id_short(partitioner);
511 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
512 mutable check_complexity::trans_gj_counter_t work_counter;
530 union constellation_or_first_unmarked_bottom_state
533 constellation_type* onstellation;
536 state_in_block_pointer* first_unmarked_bottom_state;
538 constellation_or_first_unmarked_bottom_state(constellation_type* new_c)
546 state_in_block_pointer* start_bottom_states;
548 union start_non_bottom_states_or_state_in_reduced_LTS
555 state_in_block_pointer* rt_non_bottom_states;
562 state_index te_in_reduced_LTS;
564 start_non_bottom_states_or_state_in_reduced_LTS(state_in_block_pointer* s)
565 : rt_non_bottom_states(s)
570 state_in_block_pointer* end_states;
582 linked_list<BLC_indicators> to_constellation;
static_assert(std::is_trivially_destructible_v<
linked_list<BLC_indicators>>);
596 std::vector<state_in_block_pointer>* R;
611 static bool if_R_is_nullptr_then_to_constellation_is_empty_list()
613 btc_R test_should_be_empty_BLC_list=btc_R(); assert(
nullptr==test_should_be_empty_BLC_list.R);
614 if constexpr (
sizeof(
decltype(test_should_be_empty_BLC_list.R))!=
615 sizeof(
decltype(test_should_be_empty_BLC_list.to_constellation)))
619 if (test_should_be_empty_BLC_list.to_constellation.empty() &&
620 test_should_be_empty_BLC_list.to_constellation==
629 new (&test_should_be_empty_BLC_list)
linked_list<BLC_indicators>();
635 block_type(
const block_type& other)
636 : c(other.c.onstellation),
637 start_bottom_states(other.start_bottom_states),
638 sta(other.sta.rt_non_bottom_states),
639 end_states(other.end_states),
641 contains_new_bottom_states(other.contains_new_bottom_states)
648 bool contains_new_bottom_states =
false;
651 block_type(state_in_block_pointer* start_bottom,
652 state_in_block_pointer* start_non_bottom,
653 state_in_block_pointer* end,
654 constellation_type* new_c)
656 start_bottom_states(start_bottom),
657 sta(start_non_bottom),
663 template<
class LTS_TYPE>
664 std::string debug_id(
const bisim_partitioner_gj<LTS_TYPE>& partitioner)
const
665 { assert(partitioner.m_states_in_blocks.data()<=start_bottom_states);
666 assert(start_bottom_states<=sta.rt_non_bottom_states);
667 assert(sta.rt_non_bottom_states<=end_states);
668 assert(end_states<=partitioner.m_states_in_blocks.data_end());
669 return"block ["+std::to_string
670 (std::distance<
const state_in_block_pointer*>
671 (partitioner.m_states_in_blocks.data(), start_bottom_states))+
","+
673 (std::distance<
const state_in_block_pointer*>
674 (partitioner.m_states_in_blocks.data(), end_states))+
")";
677 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
678 mutable check_complexity::block_gj_counter_t work_counter;
683struct constellation_type
686 state_in_block_pointer* start_const_states;
689 state_in_block_pointer* end_const_states;
691 constellation_type(state_in_block_pointer*
const new_start,
692 state_in_block_pointer*
const new_end)
693 : start_const_states(new_start),
694 end_const_states(new_end)
698 template<
class LTS_TYPE>
699 std::string debug_id(
const bisim_partitioner_gj<LTS_TYPE>& partitioner)
const
700 { assert(partitioner.m_states_in_blocks.data()<=start_const_states);
701 assert(start_const_states<end_const_states);
702 assert(end_const_states<=partitioner.m_states_in_blocks.data_end());
703 return "constellation ["+std::to_string
704 (std::distance<
const state_in_block_pointer*>
705 (partitioner.m_states_in_blocks.data(), start_const_states))+
","+
707 (std::distance<
const state_in_block_pointer*>
708 (partitioner.m_states_in_blocks.data(), end_const_states))+
")";
717
718
721using namespace mcrl2::
lts::
detail::bisimulation_gj;
725template <
class LTS_TYPE>
726class bisim_partitioner_gj
730 using set_of_states_type = std::unordered_set<state_index>;
731 using set_of_transitions_type = std::unordered_set<transition_index>;
740 fixed_vector<state_type_gj> m_states;
747 fixed_vector<outgoing_transition_type> m_outgoing_transitions;
750 fixed_vector<transition_type> m_transitions;
751 fixed_vector<state_in_block_pointer> m_states_in_blocks;
752 state_index no_of_blocks = 1;
753 state_index no_of_constellations = 1;
754 fixed_vector<transition_index> m_BLC_transitions;
756 std::vector<block_type*> m_blocks_with_new_bottom_states;
759 std::vector<constellation_type*> m_non_trivial_constellations;
762 m_BLC_indicators_to_be_deleted;
765 const bool m_branching;
772 const bool m_preserve_divergence;
777 static typename LTS_TYPE::labels_size_type m_aut_apply_hidden_label_map
778 (
typename LTS_TYPE::labels_size_type l)
785 bool is_inert_during_init_if_branching(
const transition& t)
const
786 { assert(m_branching);
787 return m_aut.is_tau(m_aut_apply_hidden_label_map(t.label())) &&
788 (!m_preserve_divergence || t.from() != t.to());
793 bool is_inert_during_init(
const transition& t)
const
795 return m_branching && is_inert_during_init_if_branching(t);
801 label_index label_or_divergence(
const transition& t,
802 const label_index divergent_label=-2
805 label_index result = m_aut_apply_hidden_label_map(t.label()); assert(divergent_label!=result); assert(null_action!=divergent_label);
806 if (m_preserve_divergence && ( assert(m_branching),
807 t.from() == t.to()) &&
808 m_aut.is_tau(result))
810 return divergent_label;
832 void check_transitions(
const bool initialisation,
833 const bool check_temporary_complexity_counters,
834 const bool check_block_to_constellation =
true)
const
836 for(transition_index ti=0; ti<m_transitions.size(); ++ti)
838 const BLC_list_const_iterator btc_ti=
839 m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions;
842 const transition& t=m_aut.get_transitions()[ti];
843 assert(&*m_states[t.to()].start_incoming_transitions<=&t);
844 if (t.to()+1!=m_aut.num_states())
846 assert(&t<=&*std::prev(m_states[t.to()+1].start_incoming_transitions));
850 assert(&t<=&m_aut.get_transitions().back());
853 assert(m_states[t.from()].start_outgoing_transitions<=
854 m_transitions[ti].ref_outgoing_transitions);
855 if (t.from()+1==m_aut.num_states())
857 assert(m_transitions[ti].ref_outgoing_transitions<
858 m_outgoing_transitions.end());
862 assert(m_transitions[ti].ref_outgoing_transitions<
863 m_states[t.from() + 1].start_outgoing_transitions);
866 assert(m_transitions[ti].
867 transitions_per_block_to_constellation->start_same_BLC<=btc_ti);
868 assert(btc_ti<m_transitions[ti].
869 transitions_per_block_to_constellation->end_same_BLC);
871 if (!check_block_to_constellation)
876 block_type*
const b=m_states[t.from()].block;
878 const label_index t_label = label_or_divergence(t);
880 for(
const BLC_indicators& blc: b->block.to_constellation)
882 if (!blc.is_stable())
884 assert(blc.start_same_BLC<=blc.start_marked_BLC);
885 assert(blc.start_marked_BLC<=blc.end_same_BLC);
887 assert(blc.start_same_BLC<blc.end_same_BLC);
888 transition& first_t = m_aut.get_transitions()[*blc.start_same_BLC];
889 assert(b == m_states[first_t.from()].block);
890 if (t_label == label_or_divergence(first_t) &&
891 m_states[first_t.to()].block->c.onstellation ==
892 m_states[t.to()].block->c.onstellation)
894 assert(!found); assert(blc.start_same_BLC <= btc_ti);
895 assert(btc_ti<blc.end_same_BLC);
896 assert(&blc == &*m_transitions[ti].transitions_per_block_to_constellation);
901 if (check_temporary_complexity_counters)
903 block_type*
const targetb = m_states[t.to()].block;
904 const unsigned max_sourceB = check_complexity::log_n-
905 check_complexity::ilog2(number_of_states_in_block(*b));
906 const unsigned max_targetC = check_complexity::log_n-
907 check_complexity::ilog2(number_of_states_in_constellation
908 (*targetb->c.onstellation));
909 const unsigned max_targetB = check_complexity::log_n-
910 check_complexity::ilog2(number_of_states_in_block(*targetb));
912 no_temporary_work(max_sourceB, max_targetC, max_targetB,
914 0==m_states[t.from()].no_of_outgoing_block_inert_transitions),
927 bool check_data_structures(
const std::string& tag,
const bool initialisation=
false,
const bool check_temporary_complexity_counters=
true)
const
929 mCRL2log(log::debug) <<
"Check data structures: " << tag <<
".\n";
930 assert(m_states.size()==m_aut.num_states());
931 assert(m_states_in_blocks.size()==m_aut.num_states());
932 assert(m_transitions.size()==m_aut.num_transitions());
933 assert(m_outgoing_transitions.size()==m_aut.num_transitions());
934 assert(m_BLC_transitions.size()==m_aut.num_transitions());
937 for (fixed_vector<state_type_gj>::iterator si=
938 const_cast<fixed_vector<state_type_gj>&>(m_states).begin();
939 si<m_states.cend(); si++)
941 const state_type_gj& s=*si;
943 assert(s.counter==undefined);
944 assert(s.block->start_bottom_states< s.block->sta.rt_non_bottom_states);
945 assert(s.block->sta.rt_non_bottom_states<=s.block->end_states);
948 assert(std::find(s.block->start_bottom_states,
950 state_in_block_pointer(si))!=s.block->end_states);
952 assert(s.ref_states_in_blocks->ref_state==si);
957 const std::vector<transition>::const_iterator end_it1=
958 std::next(si)>=m_states.end() ? m_aut.get_transitions().end()
959 : std::next(si)->start_incoming_transitions;
960 for (std::vector<transition>::const_iterator
961 it=s.start_incoming_transitions; it!=end_it1; ++it)
963 const transition& t=*it;
964 if (m_aut.is_tau(m_aut_apply_hidden_label_map(t.label())))
981 std::unordered_set<std::pair<label_index,
const constellation_type*> >
986 const outgoing_transitions_const_it end_it2=
987 std::next(si)>=m_states.end() ? m_outgoing_transitions.cend()
988 : std::next(si)->start_outgoing_transitions;
989 for(outgoing_transitions_const_it it=s.start_outgoing_transitions;
992 const transition& t=m_aut.get_transitions()[!initialisation
993 ? *it->ref.BLC_transitions : it->ref.transitions];
994 assert(m_states.cbegin()+t.from()==si);
995 assert(m_transitions[!initialisation ? *it->ref.BLC_transitions
996 : it->ref.transitions].ref_outgoing_transitions==it);
997 assert((it->start_same_saC>it &&
998 it->start_same_saC<m_outgoing_transitions.end() &&
999 ((it+1)->start_same_saC==it->start_same_saC ||
1000 (it+1)->start_same_saC<=it)) ||
1001 (it->start_same_saC<=it &&
1002 (it+1==m_outgoing_transitions.end() ||
1003 (it+1)->start_same_saC>it)));
1004 const label_index t_label = label_or_divergence(t);
1006 for(outgoing_transitions_const_it itt=it->start_same_saC;
1007 itt<it->start_same_saC->start_same_saC; ++itt)
1009 const transition& t1=m_aut.get_transitions()[!initialisation
1010 ? *itt->ref.BLC_transitions : itt->ref.transitions];
1011 assert(m_states.cbegin()+t1.from()==si);
1012 assert(label_or_divergence(t1) == t_label);
1013 assert(m_states[t.to()].block->c.onstellation==
1014 m_states[t1.to()].block->c.onstellation);
1017 const label_index label = label_or_divergence(t);
1020 const constellation_type* t_to_constellation=
1021 m_states[t.to()].block->c.onstellation;
1022 if (constellations_seen.count(std::pair(label,t_to_constellation))>0)
1024 assert(it!=s.start_outgoing_transitions);
1025 const transition& old_t=m_aut.get_transitions()[!initialisation
1026 ? *std::prev(it)->ref.BLC_transitions
1027 : std::prev(it)->ref.transitions];
1028 assert(label_or_divergence(old_t)==label);
1029 assert(t_to_constellation==
1030 m_states[old_t.to()].block->c.onstellation);
1034 if (m_branching && m_aut.is_tau(label))
1042 constellations_seen.emplace(label,t_to_constellation);
1047 if (!initialisation)
1049 check_transitions(initialisation, check_temporary_complexity_counters);
1053 set_of_transitions_type all_transitions;
1054 transition_index actual_no_of_non_constellation_inert_BLC_sets=0;
1055 for (
const state_in_block_pointer* si=m_states_in_blocks.data();
1056 m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
1058 const block_type& b=*si->ref_state->block;
1059 const constellation_type& c=*b.c.onstellation;
1060 assert(m_states_in_blocks.data()<=c.start_const_states);
1061 assert(c.start_const_states<=b.start_bottom_states);
1062 assert(b.start_bottom_states<b.sta.rt_non_bottom_states);
1063 assert(b.sta.rt_non_bottom_states<=b.end_states);
1064 assert(b.end_states<=c.end_const_states);
1065 assert(c.end_const_states<=m_states_in_blocks.data_end());
1067 unsigned char const max_B=check_complexity::log_n-
1068 check_complexity::ilog2(number_of_states_in_block(b));
1069 unsigned char const max_C=check_complexity::log_n-check_complexity::
1070 ilog2(number_of_states_in_constellation(*b.c.onstellation));
1071 for (
const state_in_block_pointer*
1072 is=b.start_bottom_states; is!=b.sta.rt_non_bottom_states; ++is)
1074 assert(is->ref_state->block==&b);
1075 assert(is->ref_state->no_of_outgoing_block_inert_transitions==0);
1076 if (check_temporary_complexity_counters)
1080 !initialisation), *
this);
1083 for (
const state_in_block_pointer*
1084 is=b.sta.rt_non_bottom_states; is!=b.end_states; ++is)
1086 assert(is->ref_state->block==&b);
1087 assert(is->ref_state->no_of_outgoing_block_inert_transitions>0);
1096 if (!initialisation)
1098 assert(b.block.to_constellation.check_linked_list());
1100 ind=b.block.to_constellation.begin();
1101 ind!=b.block.to_constellation.end(); ++ind)
1103 assert(ind->start_same_BLC<ind->end_same_BLC);
1104 const transition& first_transition=
1105 m_aut.get_transitions()[*(ind->start_same_BLC)];
1106 const label_index first_transition_label=
1107 label_or_divergence(first_transition);
1108 if(!is_inert_during_init(first_transition) ||
1109 m_states[first_transition.from()].block->c.onstellation!=
1110 m_states[first_transition.to()].block->c.onstellation)
1112 ++actual_no_of_non_constellation_inert_BLC_sets;
1114 for(BLC_list_const_iterator i=ind->start_same_BLC;
1115 i<ind->end_same_BLC; ++i)
1117 const transition& t=m_aut.get_transitions()[*i];
1118 assert(m_transitions[*i].transitions_per_block_to_constellation==
1120 all_transitions.emplace(*i);
1121 assert(m_states[t.from()].block==&b);
1122 assert(m_states[t.to()].block->c.onstellation==
1123 m_states[first_transition.to()].block->c.onstellation);
1124 assert(label_or_divergence(t)==first_transition_label);
1125 if (is_inert_during_init(t) && b.c.onstellation==
1126 m_states[t.to()].block->c.onstellation)
1130 assert(b.block.to_constellation.begin()==ind);
1133 if (check_temporary_complexity_counters)
1136 check_complexity::log_n-check_complexity::ilog2
1137 (number_of_states_in_constellation(*m_states
1138 [first_transition.to()].block->c.onstellation))), *
this);
1143 if (!initialisation) {
1144 assert(all_transitions.size()==m_transitions.size());
1145 assert(actual_no_of_non_constellation_inert_BLC_sets==
1146 no_of_non_constellation_inert_BLC_sets);
1155 for (
const state_in_block_pointer*
1156 si=m_states_in_blocks.data(); si<m_states_in_blocks.data_end(); ++si)
1158 assert(si==si->ref_state->ref_states_in_blocks);
1162 for(
const block_type* bi: m_blocks_with_new_bottom_states)
1164 assert(bi->contains_new_bottom_states);
1168 for(
const constellation_type* ci: m_non_trivial_constellations)
1171 const block_type*
const first_bi=ci->start_const_states->ref_state->block;
1172 const block_type*
const last_bi=std::prev(ci->end_const_states)->ref_state->block;
1173 assert(first_bi != last_bi);
1205 bool check_stability(
const std::string& tag,
1206 const std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >*
1208 const std::pair<BLC_list_iterator,BLC_list_iterator>* calM_elt=
nullptr,
1209 const constellation_type*
const old_constellation=null_constellation,
1210 const constellation_type*
const new_constellation=null_constellation)
1213 assert((old_constellation==null_constellation &&
1214 new_constellation==null_constellation ) ||
1215 (old_constellation!=null_constellation &&
1216 new_constellation!=null_constellation &&
1217 old_constellation!=new_constellation ));
1218 mCRL2log(log::debug) <<
"Check stability: " << tag <<
".\n";
1219 for (
const state_in_block_pointer* si=m_states_in_blocks.data();
1220 m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
1222 const block_type& b=*si->ref_state->block;
1223 bool previous_stable=
true;
1225 ind=b.block.to_constellation.begin();
1226 ind!=b.block.to_constellation.end(); ++ind)
1228 set_of_states_type all_source_bottom_states;
1230 assert(ind->start_same_BLC<ind->end_same_BLC);
1231 const transition&first_t=m_aut.get_transitions()[*ind->start_same_BLC];
1232 const label_index first_t_label=label_or_divergence(first_t);
1233 const bool all_transitions_in_BLC_are_inert =
1234 is_inert_during_init(first_t) && b.c.onstellation==
1235 m_states[first_t.to()].block->c.onstellation;
1236 assert(!all_transitions_in_BLC_are_inert ||
1237 b.block.to_constellation.begin()==ind);
1238 for (BLC_list_const_iterator i=ind->start_same_BLC;
1239 i<ind->end_same_BLC; ++i)
1241 assert(m_BLC_transitions.data()<=i);
1242 assert(i<m_BLC_transitions.data_end());
1243 const transition& t=m_aut.get_transitions()[*i];
1244 assert(m_states[t.from()].block == &b);
1245 assert(label_or_divergence(t) == first_t_label);
1246 assert(m_states[t.to()].block->c.onstellation==
1247 m_states[first_t.to()].block->c.onstellation);
1248 if (is_inert_during_init(t) && b.c.onstellation==
1249 m_states[t.to()].block->c.onstellation)
1251 assert(all_transitions_in_BLC_are_inert);
1256 assert(!all_transitions_in_BLC_are_inert);
1257 if (0 == m_states[t.from()].no_of_outgoing_block_inert_transitions)
1259 assert(b.start_bottom_states<=
1260 m_states[t.from()].ref_states_in_blocks);
1261 assert(m_states[t.from()].ref_states_in_blocks<
1262 b.sta.rt_non_bottom_states);
1263 all_source_bottom_states.emplace(t.from());
1267 assert(b.sta.rt_non_bottom_states<=
1268 m_states[t.from()].ref_states_in_blocks);
1269 assert(m_states[t.from()].ref_states_in_blocks < b.end_states);
1273 assert(all_source_bottom_states.size()<=
static_cast<std::size_t>
1274 (std::distance(b.start_bottom_states, b.sta.rt_non_bottom_states)));
1276 bool eventual_instability_is_ok =
true;
1277 bool eventual_marking_is_ok =
true;
1278 if (!all_transitions_in_BLC_are_inert &&
1279 all_source_bottom_states.size()!=
static_cast<std::size_t>
1280 (std::distance(b.start_bottom_states, b.sta.rt_non_bottom_states)))
1284 << std::distance(b.start_bottom_states, b.sta.rt_non_bottom_states)
1285 << (m_branching ?
" bottom states have a transition in the "
1286 :
" states have a transition in the ")
1287 << ind->debug_id(*
this) <<
": transitions found from states";
1290 all_source_bottom_state:
1291 all_source_bottom_states)
1295 << all_source_bottom_state;
1298 eventual_instability_is_ok =
false;
1300 if (!ind->is_stable())
1303 mCRL2log(log::debug) << ind->debug_id(*
this) <<
" contains " << std::distance(ind->start_marked_BLC, ind->end_same_BLC) <<
" marked transitions.\n";
1304 eventual_marking_is_ok =
false;
1306 if (b.contains_new_bottom_states)
1308 if (!(eventual_instability_is_ok && eventual_marking_is_ok))
1310 mCRL2log(log::debug) <<
" This is ok because " << b.debug_id(*
this) <<
" contains new bottom states.\n";
1311 eventual_instability_is_ok =
true;
1312 eventual_marking_is_ok =
true;
1315 if (!(eventual_instability_is_ok && eventual_marking_is_ok) &&
nullptr != calM && calM->begin() != calM->end())
1317 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >::const_iterator calM_iter = calM->begin();
1318 if (
nullptr != calM_elt)
1322 assert(calM->end() != calM_iter);
1323 if (calM_iter->first <= calM_elt->first && calM_elt->second <= calM_iter->second)
1329 if (calM_elt->first<=ind->start_same_BLC && ind->end_same_BLC<=calM_elt->second)
1331 mCRL2log(log::debug) <<
" This is ok because the BLC set ("
1332 << b.debug_id(*
this) <<
" -" << m_aut.action_label(first_t.label())
1333 <<
"-> " << m_states[first_t.to()].
1334 block->c.onstellation->debug_id(*
this)
1335 <<
") is soon going to be a main splitter.\n";
1336 eventual_instability_is_ok =
true;
1337 eventual_marking_is_ok =
true;
1341 if (old_constellation==
1342 m_states[first_t.to()].block->c.onstellation)
1344 const linked_list<BLC_indicators>::const_iterator main_splitter=b.block.to_constellation.next(ind);
1345 if (main_splitter!=b.block.to_constellation.end())
1347 assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
1348 const transition& main_t = m_aut.get_transitions()[*main_splitter->start_same_BLC];
1349 assert(m_states[main_t.from()].block == &b);
1350 if(label_or_divergence(first_t)==label_or_divergence(main_t)
1351 && m_states[main_t.to()].block->c.onstellation==
1354 if (calM_elt->first<=main_splitter->start_same_BLC && main_splitter->end_same_BLC<=calM_elt->second)
1356 assert(new_constellation==
1357 m_states[main_t.to()].block->c.onstellation);
1358 mCRL2log(log::debug) <<
" This is ok because the BLC set (" << b.debug_id(*
this) <<
" -" << m_aut.action_label(first_t.label()) <<
"-> " << old_constellation->debug_id(*
this) <<
") is soon going to be a co-splitter.\n";
1359 eventual_instability_is_ok =
true;
1360 eventual_marking_is_ok =
true;
1368 for(; !(eventual_instability_is_ok && eventual_marking_is_ok) && calM->end() != calM_iter; ++calM_iter)
1370 if (calM_iter->first<=ind->start_same_BLC && ind->end_same_BLC<=calM_iter->second)
1372 mCRL2log(log::debug) <<
" This is ok because the BLC set ("
1373 << b.debug_id(*
this) <<
" -" << m_aut.action_label(first_t.label())
1375 << m_states[first_t.to()].block->c.onstellation->debug_id(*
this)
1376 <<
") is going to be a main splitter later.\n";
1377 eventual_instability_is_ok =
true;
1378 eventual_marking_is_ok =
true;
1382 if (old_constellation==
1383 m_states[first_t.to()].block->c.onstellation)
1385 const linked_list<BLC_indicators>::const_iterator main_splitter=b.block.to_constellation.next(ind);
1386 if (main_splitter != b.block.to_constellation.end())
1388 assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
1389 const transition& main_t = m_aut.get_transitions()[*main_splitter->start_same_BLC];
1390 assert(m_states[main_t.from()].block == &b);
1391 if(label_or_divergence(first_t)==label_or_divergence(main_t)
1392 && m_states[main_t.to()].block->c.onstellation==
1395 if (calM_iter->first<=main_splitter->start_same_BLC && main_splitter->end_same_BLC<=calM_iter->second)
1397 assert(new_constellation==
1398 m_states[main_t.to()].block->c.onstellation);
1399 mCRL2log(log::debug) <<
" This is ok because the BLC "
1400 "set (" << b.debug_id(*
this) <<
" -"
1401 << m_aut.action_label(first_t.label())
1402 <<
"-> " << old_constellation->debug_id(*
this)
1403 <<
") is going to be a co-splitter later.\n";
1404 eventual_instability_is_ok =
true;
1405 eventual_marking_is_ok =
true;
1413 if (1>=number_of_states_in_block(b))
1415 if (!eventual_marking_is_ok)
1417 mCRL2log(log::debug) <<
" (This is ok because the source block contains only 1 state.)\n";
1418 eventual_marking_is_ok =
true;
1421 else if (1<no_of_constellations &&
1422 !b.contains_new_bottom_states)
1424 assert(eventual_marking_is_ok); assert(eventual_instability_is_ok);
1425 if (null_constellation==old_constellation && ind->is_stable()) {
1426 assert(previous_stable);
1430 previous_stable=
false;
1435 mCRL2log(log::debug) <<
"Check stability finished: " << tag <<
".\n";
1440 void display_BLC_list(
const block_type*
const bi)
const
1442 mCRL2log(log::debug) <<
"\n BLC_List\n";
1443 for(
const BLC_indicators& blc_it: bi->block.to_constellation)
1445 const transition& first_t=m_aut.get_transitions()[*blc_it.start_same_BLC];
1446 const label_index l=label_or_divergence(first_t, (label_index) -2);
1450 BLC_list_const_iterator>(
1451 m_BLC_transitions.data(),
1452 blc_it.start_same_BLC)
1455 BLC_list_const_iterator>(
1456 m_BLC_transitions.data(),
1457 blc_it.end_same_BLC)
1459 << (std::cmp_equal(-2, l)
1460 ?
"divergent self-loop "
1461 : pp(m_aut.action_label(
1464 <<
"transitions to "
1465 << m_states[first_t.to()]
1466 .block->c.onstellation
1469 for (BLC_list_const_iterator i=blc_it.start_same_BLC; ; ++i)
1471 if (i == blc_it.start_marked_BLC)
1473 mCRL2log(log::debug) <<
" (The BLC set is unstable, and the "
1474 " following transitions are marked.)\n";
1476 if (i>=blc_it.end_same_BLC)
1480 const transition& t=m_aut.get_transitions()[*i];
1481 mCRL2log(log::debug) <<
" " << t.from() <<
" -"
1482 << m_aut.action_label(t.label()) <<
"-> " << t.to();
1483 if (is_inert_during_init(t) &&
1484 m_states[t.from()].block==m_states[t.to()].block)
1486 mCRL2log(log::debug) <<
" (block-inert)";
1488 else if (is_inert_during_init(t) &&
1489 m_states[t.from()].block->c.onstellation==
1490 m_states[t.to()].block->c.onstellation)
1492 mCRL2log(log::debug) <<
" (constellation-inert)";
1497 mCRL2log(log::debug) <<
" BLC_List end\n";
1501 void print_data_structures(
const std::string& header,
1502 const bool initialisation=
false)
const
1504 if (!mCRL2logEnabled(log::debug)) {
return; }
1505 mCRL2log(log::debug) <<
"========= PRINT DATASTRUCTURE: " << header <<
" =======================================\n"
1506 "++++++++++++++++++++ States ++++++++++++++++++++++++++++\n";
1507 for(state_index si=0; si<m_aut.num_states(); ++si)
1509 mCRL2log(log::debug) <<
"State " << si <<
" (" << m_states[si].block->debug_id(*
this) <<
"):\n"
1510 " #Inert outgoing transitions: " << m_states[si].no_of_outgoing_block_inert_transitions <<
"\n"
1512 " Incoming transitions:\n";
1513 std::vector<transition>::const_iterator end=(si+1==m_aut.num_states()?m_aut.get_transitions().end():m_states[si+1].start_incoming_transitions);
1514 for(std::vector<transition>::const_iterator it=m_states[si].start_incoming_transitions; it!=end; ++it)
1516 mCRL2log(log::debug) <<
" " << ptr(*it) <<
"\n";
1519 mCRL2log(log::debug) <<
" Outgoing transitions:\n";
1520 label_index t_label=m_aut.tau_label_index();
1521 const constellation_type* to_constln=null_constellation;
1522 for(outgoing_transitions_const_it it=m_states[si].start_outgoing_transitions;
1523 it!=m_outgoing_transitions.end() &&
1524 (si+1>=m_aut.num_states() || it!=m_states[si+1].start_outgoing_transitions);
1527 const transition& t=m_aut.get_transitions()[!initialisation
1528 ? *it->ref.BLC_transitions : it->ref.transitions];
1529 bool start_same_saC_valid=
1530 m_outgoing_transitions.cbegin()<=it->start_same_saC &&
1531 it->start_same_saC<m_outgoing_transitions.end();
1532 if (start_same_saC_valid &&
1533 it->start_same_saC->start_same_saC==it &&
1534 it->start_same_saC >= it)
1537 const label_index old_t_label=t_label;
1538 t_label=label_or_divergence(t, (label_index) -2);
1539 to_constln=m_states[t.to()].block->c.onstellation;
1543 << (std::cmp_equal(-2,
1551 <<
"transitions to "
1552 << to_constln->debug_id(
1554 << (m_aut.is_tau(t_label)
1563 mCRL2log(log::debug) <<
" " << ptr(t);
1564 if (start_same_saC_valid)
1566 if (label_or_divergence(t, (label_index) -2)!=t_label)
1568 mCRL2log(log::debug) <<
" -- error: different label";
1570 if (!initialisation && m_states[t.to()].block->c.onstellation!=to_constln)
1572 mCRL2log(log::debug) <<
" -- error: different target " << m_states[t.to()].block->c.onstellation->debug_id(*
this);
1574 if (it->start_same_saC->start_same_saC == it)
1577 if (it->start_same_saC >= it && it > m_outgoing_transitions.cbegin())
1580 const transition& prev_t=m_aut.get_transitions()[
1581 !initialisation ? *std::prev(it)->ref.BLC_transitions
1582 : std::prev(it)->ref.transitions];
1583 if (prev_t.from()==t.from() &&
1584 label_or_divergence(prev_t)==t_label &&
1586 m_states[prev_t.to()].block->c.onstellation==
1587 m_states[t.to()].block->c.onstellation))
1589 mCRL2log(log::debug) <<
" -- error: not the beginning of a saC-slice";
1592 if (it->start_same_saC <= it && std::next(it) < m_outgoing_transitions.end())
1595 const transition& next_t=m_aut.get_transitions()[
1596 !initialisation ? *std::next(it)->ref.BLC_transitions
1597 : std::next(it)->ref.transitions];
1598 if (next_t.from()==t.from() &&
1599 label_or_divergence(next_t)==t_label &&
1601 m_states[next_t.to()].block->c.onstellation==
1602 m_states[t.to()].block->c.onstellation))
1604 mCRL2log(log::debug) <<
" -- error: not the end of a saC-slice";
1608 else if (it->start_same_saC > it ? it->start_same_saC->start_same_saC > it : it->start_same_saC->start_same_saC < it)
1610 mCRL2log(log::debug) <<
" -- error: not pointing to its own saC-slice";
1615 mCRL2log(log::debug) <<
" Ref states in blocks: " << std::distance<fixed_vector<state_type_gj>::const_iterator>(m_states.cbegin(), m_states[si].ref_states_in_blocks->ref_state) <<
". Must be " << si <<
".\n";
1616 mCRL2log(log::debug) <<
"---------------------------------------------------\n";
1618 mCRL2log(log::debug) <<
"++++++++++++++++++++ Transitions ++++++++++++++++++++++++++++\n";
1619 for(transition_index ti=0; ti<m_transitions.size(); ++ti)
1621 const transition& t=m_aut.get_transitions()[ti];
1622 mCRL2log(log::debug) <<
"Transition " << ti <<
": " << t.from()
1623 <<
" -" << m_aut.action_label(t.label()) <<
"-> "
1627 mCRL2log(log::debug) <<
"++++++++++++++++++++ Blocks ++++++++++++++++++++++++++++\n";
1628 for (
const state_in_block_pointer* si=m_states_in_blocks.data();
1629 m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
1631 block_type*
const bi=si->ref_state->block;
1632 mCRL2log(log::debug) <<
" Block " << bi;
1633 if (!initialisation) {
1634 mCRL2log(log::debug) <<
" (" << bi->c.onstellation->debug_id(*
this) <<
')';
1636 mCRL2log(log::debug) <<
":\n " << std::distance(bi->start_bottom_states,
1637 bi->sta.rt_non_bottom_states)
1638 << (m_branching ?
" Bottom state" :
" State")
1639 << (1==std::distance(bi->start_bottom_states,
1640 bi->sta.rt_non_bottom_states) ?
": " :
"s: ");
1641 for (
const state_in_block_pointer*
1642 sit=bi->start_bottom_states; sit!=bi->sta.rt_non_bottom_states; ++sit)
1644 mCRL2log(log::debug) << sit->ref_state->debug_id_short(*
this) <<
" ";
1648 mCRL2log(log::debug) <<
"\n " << std::distance
1649 (bi->sta.rt_non_bottom_states, bi->end_states)
1650 <<
" Non-bottom state" << (1==std::distance
1651 (bi->sta.rt_non_bottom_states, bi->end_states)
1653 for (
const state_in_block_pointer*
1654 sit=bi->sta.rt_non_bottom_states; sit!=bi->end_states; ++sit)
1656 mCRL2log(log::debug) << sit->ref_state->debug_id_short(*
this) <<
" ";
1661 assert(bi->sta.rt_non_bottom_states==bi->end_states);
1663 if (!initialisation)
1665 display_BLC_list(bi);
1670 mCRL2log(log::debug) <<
"++++++++++++++++++++ Constellations ++++++++++++++++++++++++++++\n";
1671 for (
const state_in_block_pointer* si=m_states_in_blocks.data();
1672 m_states_in_blocks.data_end()!=si;
1673 si=si->ref_state->block->c.onstellation->end_const_states)
1675 const constellation_type*
const ci=si->ref_state->block->c.onstellation;
1676 mCRL2log(log::debug) <<
" " << ci->debug_id(*
this) <<
":\n";
1677 mCRL2log(log::debug) <<
" Blocks in constellation:";
1678 for (
const state_in_block_pointer*
1679 constln_it=ci->start_const_states;
1680 constln_it<ci->end_const_states; )
1682 const block_type*
const bi=constln_it->ref_state->block;
1683 mCRL2log(log::debug) <<
" " << bi->debug_id(*
this);
1684 constln_it = bi->end_states;
1688 mCRL2log(log::debug) <<
"Non-trivial constellations:";
1689 for (
const constellation_type* ci: m_non_trivial_constellations)
1691 mCRL2log(log::debug) <<
" " << ci->debug_id(*
this);
1695 "\n++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n"
1696 "Outgoing transitions:\n";
1698 for (outgoing_transitions_const_it pi = m_outgoing_transitions.cbegin();
1699 pi < m_outgoing_transitions.cend(); ++pi)
1701 const transition& t=m_aut.get_transitions()[!initialisation
1702 ? *pi->ref.BLC_transitions : pi->ref.transitions];
1703 mCRL2log(log::debug) <<
" " << t.from() <<
" -"
1704 << m_aut.action_label(t.label()) <<
"-> " << t.to();
1705 if (m_outgoing_transitions.cbegin()<=pi->start_same_saC &&
1706 pi->start_same_saC<m_outgoing_transitions.end())
1708 const transition& t1=m_aut.get_transitions()[!initialisation
1709 ? *pi->start_same_saC->ref.BLC_transitions
1710 : pi->start_same_saC->ref.transitions];
1711 mCRL2log(log::debug) <<
" \t(same saC: " << t1.from() <<
" -" << m_aut.action_label(t1.label()) <<
"-> " << t1.to();
1712 const label_index t_label = label_or_divergence(t);
1713 if (pi->start_same_saC->start_same_saC == pi)
1716 if (pi->start_same_saC >= pi && pi > m_outgoing_transitions.cbegin())
1719 const transition& prev_t=m_aut.get_transitions()[
1720 !initialisation ? *std::prev(pi)->ref.BLC_transitions
1721 : std::prev(pi)->ref.transitions];
1722 if (prev_t.from()==t.from() &&
1723 label_or_divergence(prev_t)==t_label &&
1725 m_states[prev_t.to()].block->c.onstellation==
1726 m_states[t.to()].block->c.onstellation))
1728 mCRL2log(log::debug) <<
" -- error: not the beginning of a saC-slice";
1731 if (pi->start_same_saC <= pi && std::next(pi) < m_outgoing_transitions.end())
1734 const transition& next_t=m_aut.get_transitions()[
1735 !initialisation ? *std::next(pi)->ref.BLC_transitions
1736 : std::next(pi)->ref.transitions];
1737 if (next_t.from()==t.from() &&
1738 label_or_divergence(next_t)==t_label &&
1740 m_states[next_t.to()].block->c.onstellation==
1741 m_states[t.to()].block->c.onstellation))
1743 mCRL2log(log::debug) <<
" -- error: not the end of a saC-slice";
1747 else if (pi->start_same_saC > pi ? pi->start_same_saC->start_same_saC > pi : pi->start_same_saC->start_same_saC < pi)
1749 mCRL2log(log::debug) <<
" -- error: not in its own saC-slice";
1755 mCRL2log(log::debug) <<
"++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n"
1756 "New bottom blocks to be investigated:";
1758 for(
const block_type* bi: m_blocks_with_new_bottom_states)
1760 mCRL2log(log::debug) <<
" " << bi->debug_id(*
this) <<
'\n';
1763 mCRL2log(log::debug) <<
"\n========= END PRINT DATASTRUCTURE: " << header <<
" =======================================\n";
1771 std::size_t num_eq_classes()
const
1773 return no_of_blocks;
1784 state_index get_eq_class(
const state_index si)
const
1785 { assert(si<m_states.size());
1786 return m_states[si].block->sta.te_in_reduced_LTS;
1802 void finalize_minimized_LTS()
1809 state_index block_number=0;
1810 for (state_in_block_pointer*
1811 si=m_states_in_blocks.data(); m_states_in_blocks.data_end()!=si;
1812 si=si->ref_state->block->end_states)
1814 block_type*
const bi=si->ref_state->block;
1816 new (&bi->sta.te_in_reduced_LTS) state_index(block_number);
1823 std::remove_reference_t<
decltype(m_aut.get_transitions())> T;
1824 for (state_in_block_pointer*
1825 si=m_states_in_blocks.data(); m_states_in_blocks.data_end()!=si;
1826 si=si->ref_state->block->end_states)
1828 const block_type& B=*si->ref_state->block;
1831 for(
const BLC_indicators blc_ind: B.block.to_constellation)
1835 assert(blc_ind.start_same_BLC<blc_ind.end_same_BLC);
1837 t=m_aut.get_transitions()[*blc_ind.start_same_BLC];
1838 const state_index new_to=get_eq_class(t.to());
1839 if (!is_inert_during_init(t) || B.sta.te_in_reduced_LTS!=new_to)
1841 T.emplace_back(B.sta.te_in_reduced_LTS, t.label(), new_to);
1845 m_aut.get_transitions()=std::move(T);
1851 if (m_aut.has_state_info())
1854 std::remove_reference_t<
decltype(m_aut.state_labels())>
1855 new_labels(num_eq_classes());
1857 for(std::size_t i=0; i<m_aut.num_states(); ++i)
1861 const state_index new_index(get_eq_class(i));
1862 new_labels[new_index]=new_labels[new_index]+m_aut.state_label(i);
1865 m_aut.set_num_states(num_eq_classes(),
false); assert(0==m_aut.num_state_labels());
1866 m_aut.state_labels()=std::move(new_labels);
1870 m_aut.set_num_states(num_eq_classes(),
false);
1873 m_aut.set_initial_state(get_eq_class(m_aut.initial_state()));
1881 bool in_same_class(state_index
const s, state_index
const t)
const
1883 return get_eq_class(s) == get_eq_class(t);
1887 std::string ptr(
const transition& t)
const
1889 return std::to_string(t.from())+
" -"+pp(m_aut.action_label(t.label()))+
1890 "-> "+std::to_string(t.to());
1898 state_index number_of_states_in_block(
const block_type& B)
const
1899 { assert(B.start_bottom_states<B.end_states);
1900 return std::distance(B.start_bottom_states, B.end_states);
1904 state_index number_of_states_in_constellation(
const constellation_type& C)
1906 { assert(C.start_const_states<C.end_const_states);
1907 return std::distance(C.start_const_states, C.end_const_states);
1911 void swap_states_in_states_in_block_never_equal(
1912 state_in_block_pointer* pos1, state_in_block_pointer* pos2)
1913 { assert(m_states_in_blocks.data()<=pos1);
1914 std::swap(*pos1,*pos2); assert(pos1<m_states_in_blocks.data_end());
1915 pos1->ref_state->ref_states_in_blocks=pos1; assert(m_states_in_blocks.data()<=pos2);
1916 pos2->ref_state->ref_states_in_blocks=pos2; assert(pos2<m_states_in_blocks.data_end()); assert(pos1!=pos2);
1920 void swap_states_in_states_in_block(
1921 state_in_block_pointer* pos1, state_in_block_pointer* pos2)
1925 swap_states_in_states_in_block_never_equal(pos1, pos2);
1932 void swap_states_in_states_in_block_23_never_equal(
1933 state_in_block_pointer* pos1,
1934 state_in_block_pointer* pos2,
1935 state_in_block_pointer* pos3)
1936 { assert(m_states_in_blocks.data()<=pos2); assert(pos2<pos3);
1937 assert(pos1<m_states_in_blocks.data_end());
1940 std::swap(*pos1,*pos2);
1943 { assert(pos3<pos1);
1944 const state_in_block_pointer temp=*pos1;
1949 pos3->ref_state->ref_states_in_blocks=pos3;
1951 pos1->ref_state->ref_states_in_blocks=pos1;
1952 pos2->ref_state->ref_states_in_blocks=pos2;
1958 void swap_states_in_states_in_block(
1959 state_in_block_pointer* pos1,
1960 state_in_block_pointer* pos2,
1961 state_in_block_pointer* pos3)
1965 swap_states_in_states_in_block(pos1,pos2);
1969 swap_states_in_states_in_block_23_never_equal(pos1,pos2,pos3);
1980 void multiple_swap_states_in_states_in_block(
1981 state_in_block_pointer* pos1,
1982 state_in_block_pointer* pos2,
1984 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1985 ,
const state_in_block_pointer* assign_work_to,
1986 unsigned char const max_B,
1987 enum check_complexity::counter_type
const ctr=check_complexity::
1988 multiple_swap_states_in_block_swap_state_in_small_block
1991 { assert(count<m_aut.num_states()); assert(m_states_in_blocks.data()<=pos1);
1992 assert(pos1<pos2); assert(pos2<=m_states_in_blocks.data_end()-count);
1994 std::make_signed_t<state_index> overlap =
1995 std::distance(pos2, pos1) +
1996 static_cast<std::make_signed_t<state_index>>(count);
2000 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2004 if (pos2==assign_work_to) {
2005 assign_work_to+=overlap;
2006 }
else { assert(assign_work_to+count<=pos2+overlap ||
2007 pos2+overlap+count<=assign_work_to); }
2011 } assert(0 < count);
2012 state_in_block_pointer temp=*pos1;
2014 {
mCRL2complexity(assign_work_to->ref_state, add_work(ctr, max_B), *
this);
2015 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2019 pos1->ref_state->ref_states_in_blocks=pos1;
2022 pos2->ref_state->ref_states_in_blocks=pos2;
2026 pos1->ref_state->ref_states_in_blocks=pos1;
2028 pos2->ref_state->ref_states_in_blocks=pos2;
2030 for (fixed_vector<state_type_gj>::const_iterator
2031 si=m_states.cbegin(); si<m_states.cend(); ++si)
2033 assert(si==si->ref_states_in_blocks->ref_state);
2041 void mark_BLC_transition(
const outgoing_transitions_it out_pos)
2043 BLC_list_iterator old_pos = out_pos->ref.BLC_transitions;
2045 m_transitions[*old_pos].transitions_per_block_to_constellation; assert(ind->start_same_BLC<=old_pos);
2046 assert(old_pos<m_BLC_transitions.data_end());
2047 assert(old_pos<ind->end_same_BLC); assert(!ind->is_stable());
2048 if (old_pos < ind->start_marked_BLC)
2050 assert(ind->start_same_BLC<ind->start_marked_BLC);
2051 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);
2052 assert(new_pos<m_BLC_transitions.data_end());
2053 if (old_pos < new_pos)
2055 std::swap(*old_pos, *new_pos);
2056 m_transitions[*old_pos].ref_outgoing_transitions->
2057 ref.BLC_transitions = old_pos; assert(out_pos==m_transitions[*new_pos].ref_outgoing_transitions);
2058 out_pos->ref.BLC_transitions = new_pos;
2060 ind->start_marked_BLC--;
2064 for (BLC_list_const_iterator it=m_BLC_transitions.data();
2065 it<m_BLC_transitions.data_end(); ++it)
2067 assert(m_transitions[*it].ref_outgoing_transitions->ref.BLC_transitions==
2069 assert(m_transitions[*it].transitions_per_block_to_constellation->
2070 start_same_BLC<=it);
2072 m_transitions[*it].transitions_per_block_to_constellation->end_same_BLC);
2078 void swap_three_iterators_and_update_m_transitions(
2079 BLC_list_iterator i1,
2080 BLC_list_iterator i2,
2081 BLC_list_iterator i3)
2082 { assert(i3<=i2); assert(i2<=i1);
2087 if ((i1==i2)||(i2==i3))
2090 m_transitions[*i1].ref_outgoing_transitions->ref.BLC_transitions = i1;
2091 m_transitions[*i3].ref_outgoing_transitions->ref.BLC_transitions = i3;
2095 transition_index temp = *i1;
2099 m_transitions[*i1].ref_outgoing_transitions->ref.BLC_transitions = i1;
2100 m_transitions[*i2].ref_outgoing_transitions->ref.BLC_transitions = i2;
2101 m_transitions[*i3].ref_outgoing_transitions->ref.BLC_transitions = i3;
2123 bool swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation(
2124 const transition_index ti,
2125 linked_list<BLC_indicators>::iterator new_BLC_block,
2126 linked_list<BLC_indicators>::iterator old_BLC_block)
2127 { assert(new_BLC_block->is_stable());
2128 BLC_list_iterator old_position=
2129 m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions; assert(old_BLC_block->start_same_BLC <= old_position);
2130 assert(old_position<old_BLC_block->end_same_BLC);
2131 assert(new_BLC_block->end_same_BLC==old_BLC_block->start_same_BLC);
2132 assert(m_transitions[ti].transitions_per_block_to_constellation==old_BLC_block);
2133 assert(ti == *old_position); assert(old_BLC_block->is_stable());
2134 if (old_position!=old_BLC_block->start_same_BLC)
2136 std::swap(*old_position,*old_BLC_block->start_same_BLC);
2137 m_transitions[*old_position].ref_outgoing_transitions->
2138 ref.BLC_transitions = old_position;
2139 m_transitions[*old_BLC_block->start_same_BLC].
2140 ref_outgoing_transitions->ref.BLC_transitions =
2141 old_BLC_block->start_same_BLC;
2143 new_BLC_block->end_same_BLC=++old_BLC_block->start_same_BLC;
2144 m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
2145 return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
2167 bool update_the_doubly_linked_list_LBC_new_constellation(
2168 block_type*
const index_block_B,
2169 const transition& t,
2170 const transition_index ti)
2171 { assert(m_states[t.to()].block==index_block_B);
2172 block_type*
const from_block=m_states[t.from()].block; assert(&m_aut.get_transitions()[ti] == &t);
2173 bool new_block_created =
false; assert(from_block->block.to_constellation.check_linked_list());
2174 linked_list<BLC_indicators>::iterator this_block_to_constellation=
2175 m_transitions[ti].transitions_per_block_to_constellation; assert(this_block_to_constellation->is_stable());
2178 for (
linked_list<BLC_indicators>::const_iterator i=from_block->block.to_constellation.begin();
2179 i!=this_block_to_constellation; ++i)
2181 assert(i!=from_block->block.to_constellation.end());
2184 assert(this_block_to_constellation!=from_block->block.to_constellation.end());
2185 assert(this_block_to_constellation->start_same_BLC <= m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions);
2186 linked_list<BLC_indicators>::iterator next_block_to_constellation;
2189 if (is_inert_during_init(t) && from_block==index_block_B)
2191 next_block_to_constellation=from_block->block.to_constellation.begin(); assert(next_block_to_constellation->start_same_BLC <
2192 next_block_to_constellation->end_same_BLC);
2193 assert(m_states[m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].from()].block==index_block_B);
2194 assert(m_aut.is_tau(m_aut_apply_hidden_label_map(m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].label())));
2195 if (next_block_to_constellation==this_block_to_constellation)
2200 next_block_to_constellation=from_block->block.to_constellation.
2202 this_block_to_constellation->start_same_BLC,
2203 this_block_to_constellation->start_same_BLC,
true);
2204 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2205 next_block_to_constellation->work_counter = this_block_to_constellation->work_counter;
2208 assert(m_states[m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].to()].block==index_block_B);
2222 next_block_to_constellation=from_block->
2223 block.to_constellation.next(this_block_to_constellation);
2224 const transition* first_t;
2225 if (next_block_to_constellation==
2226 from_block->block.to_constellation.end() ||
2227 (first_t=&m_aut.get_transitions()
2228 [*(next_block_to_constellation->start_same_BLC)], assert(m_states[first_t->from()].block==from_block),
2229 m_states[first_t->to()].block!=index_block_B) ||
2230 label_or_divergence(*first_t)!=label_or_divergence(t))
2233 new_block_created =
true;
2234 next_block_to_constellation=from_block->block.to_constellation.
2235 emplace_after(this_block_to_constellation,
2236 this_block_to_constellation->start_same_BLC,
2237 this_block_to_constellation->start_same_BLC,
true);
2238 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2239 next_block_to_constellation->work_counter=
2240 this_block_to_constellation->work_counter;
2242 ++no_of_non_constellation_inert_BLC_sets;
2246 if (swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation(ti,
2247 next_block_to_constellation, this_block_to_constellation))
2249 from_block->block.to_constellation.erase(this_block_to_constellation);
2250 if (!is_inert_during_init(t) ||
2251 from_block->c.onstellation!=index_block_B->c.onstellation)
2258 --no_of_non_constellation_inert_BLC_sets;
2262 check_transitions(
false,
false,
false);
2264 return new_block_created;
2279 bool swap_in_the_doubly_linked_list_LBC_in_blocks_new_block(
2280 const transition_index ti,
2281 linked_list<BLC_indicators>::iterator new_BLC_block,
2282 linked_list<BLC_indicators>::iterator old_BLC_block)
2283 { assert(new_BLC_block->end_same_BLC==old_BLC_block->start_same_BLC);
2284 BLC_list_iterator old_position =
2285 m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions; assert(old_BLC_block->start_same_BLC<=old_position);
2286 assert(old_position<old_BLC_block->end_same_BLC); assert(ti==*old_position);
2287 assert(m_transitions[ti].transitions_per_block_to_constellation==
2290 if (old_BLC_block->is_stable())
2291 { assert(new_BLC_block->is_stable());
2292 if (old_position!=old_BLC_block->start_same_BLC)
2294 std::swap(*old_position, *old_BLC_block->start_same_BLC);
2295 m_transitions[*old_position].ref_outgoing_transitions->
2296 ref.BLC_transitions=old_position;
2297 m_transitions[*old_BLC_block->start_same_BLC].
2298 ref_outgoing_transitions->ref.BLC_transitions=
2299 old_BLC_block->start_same_BLC;
2303 { assert(!new_BLC_block->is_stable());
2304 assert(new_BLC_block->start_same_BLC<=new_BLC_block->start_marked_BLC);
2305 assert(new_BLC_block->start_marked_BLC<=new_BLC_block->end_same_BLC);
2306 if (old_position<old_BLC_block->start_marked_BLC)
2307 { assert(old_BLC_block->start_marked_BLC<=old_BLC_block->end_same_BLC);
2308 swap_three_iterators_and_update_m_transitions(old_position,
2309 old_BLC_block->start_same_BLC, new_BLC_block->start_marked_BLC);
2310 ++new_BLC_block->start_marked_BLC;
2313 { assert(old_BLC_block->start_same_BLC<=old_BLC_block->start_marked_BLC);
2314 swap_three_iterators_and_update_m_transitions(old_position,
2315 old_BLC_block->start_marked_BLC, old_BLC_block->start_same_BLC);
2316 ++old_BLC_block->start_marked_BLC;
2319 m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
2320 new_BLC_block->end_same_BLC=++old_BLC_block->start_same_BLC;
2321 return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
2343 void update_the_doubly_linked_list_LBC_new_block(
2344 block_type*
const old_bi,
2345 block_type*
const new_bi,
2346 const transition_index ti,
2347 constellation_type* old_constellation,
2348 constellation_type*
const new_constellation
2353 { assert(old_bi->block.to_constellation.check_linked_list());
2354 const transition& t=m_aut.get_transitions()[ti]; assert(new_bi->block.to_constellation.check_linked_list());
2355 assert(m_states[t.from()].block==new_bi);
2356 linked_list<BLC_indicators>::iterator this_block_to_constellation=
2357 m_transitions[ti].transitions_per_block_to_constellation;
2360 for (
linked_list<BLC_indicators>::const_iterator i=old_bi->block.to_constellation.begin();
2361 i!=this_block_to_constellation; ++i)
2363 assert(i!=old_bi->block.to_constellation.end());
2366 const label_index a=label_or_divergence(t);
2367 constellation_type*
const to_constln=
2368 m_states[t.to()].block->c.onstellation;
2369 linked_list<BLC_indicators>::iterator new_BLC_block;
2370 const bool t_is_inert=is_inert_during_init(t);
2371 if (t_is_inert && to_constln==new_bi->c.onstellation)
2373 assert(this_block_to_constellation==old_bi->block.to_constellation.begin());
2375 assert(!new_bi->block.to_constellation.empty());
2376 new_BLC_block=new_bi->block.to_constellation.begin(); assert(this_block_to_constellation->start_same_BLC==new_BLC_block->end_same_BLC);
2378 if (new_BLC_block->start_same_BLC<new_BLC_block->end_same_BLC) {
2379 const transition& inert_t=m_aut.get_transitions()[*new_BLC_block->start_same_BLC];
2380 assert(new_bi==m_states[inert_t.from()].block);
2381 assert(a==label_or_divergence(inert_t));
2382 assert(to_constln==m_states[inert_t.to()].block->c.onstellation);
2388 transition_index perhaps_new_BLC_block_transition;
2389 const transition* perhaps_new_BLC_t;
2390 if (this_block_to_constellation->start_same_BLC!=
2391 m_BLC_transitions.data() &&
2392 (perhaps_new_BLC_block_transition=
2393 *std::prev(this_block_to_constellation->start_same_BLC),
2395 &m_aut.get_transitions()[perhaps_new_BLC_block_transition],
2396 m_states[perhaps_new_BLC_t->from()].block==new_bi) &&
2397 a==label_or_divergence(*perhaps_new_BLC_t) &&
2398 to_constln==m_states
2399 [perhaps_new_BLC_t->to()].block->c.onstellation)
2403 new_BLC_block=m_transitions[perhaps_new_BLC_block_transition].
2404 transitions_per_block_to_constellation;
2406 if (this_block_to_constellation->is_stable()) { assert(new_BLC_block->is_stable()); }
2407 else { assert(!new_BLC_block->is_stable()); }
2417 linked_list<BLC_indicators>::iterator new_position=
2418 new_bi->block.to_constellation.end(); assert(!is_inert_during_init(t)||to_constln!=new_bi->c.onstellation);
2419 if (new_bi->block.to_constellation.empty())
2420 { assert(!m_branching);
2421 assert(new_bi->block.to_constellation.end()==new_position);
2426 new_position=new_bi->block.to_constellation.before_end(); assert(new_bi->block.to_constellation.end()!=new_position);
2428 if (null_constellation!=old_constellation)
2431 ((to_constln==new_constellation &&
2432 new_bi->c.onstellation==old_constellation) ||
2437 (to_constln==old_constellation &&
2438 new_bi->c.onstellation==new_constellation)))
2445 old_constellation=null_constellation;
2448 { assert(old_constellation!=new_constellation);
2452 linked_list<BLC_indicators>::const_iterator old_co_splitter{};
2453 constellation_type* co_to_constln;
2454 if ((old_constellation==to_constln &&
2456 (old_co_splitter=old_bi->block.to_constellation.
2457 next(this_block_to_constellation),
2458 co_to_constln=new_constellation,
true)) ||
2459 (new_constellation==to_constln &&
2461 (old_co_splitter=old_bi->block.to_constellation.
2462 prev(this_block_to_constellation),
2463 co_to_constln=old_constellation,
true)))
2465 if (old_bi->block.to_constellation.end()!=old_co_splitter)
2478 if (new_bi->block.to_constellation.end()!=new_position &&
2479 m_BLC_transitions.data()<old_co_splitter->start_same_BLC)
2486 const transition_index perhaps_new_co_spl_transition=
2487 *std::prev(old_co_splitter->start_same_BLC);
2488 const transition& perhaps_new_co_spl_t=
2489 m_aut.get_transitions()[perhaps_new_co_spl_transition];
2490 if(new_bi==m_states[perhaps_new_co_spl_t.from()].block &&
2491 a==label_or_divergence(perhaps_new_co_spl_t) &&
2492 co_to_constln==m_states
2493 [perhaps_new_co_spl_t.to()].block->c.onstellation)
2499 new_position=m_transitions
2500 [perhaps_new_co_spl_transition].
2501 transitions_per_block_to_constellation;
2502 if (old_constellation==to_constln)
2509 new_position=new_bi->block.to_constellation.
2513 if (old_co_splitter->start_same_BLC<old_co_splitter->end_same_BLC)
2515 const transition& co_t=m_aut.get_transitions()
2516 [*old_co_splitter->start_same_BLC];
2517 assert(old_bi==m_states[co_t.from()].block ||
2518 new_bi==m_states[co_t.from()].block);
2519 assert(a==label_or_divergence(co_t));
2520 assert(co_to_constln==m_states[co_t.to()].block->c.onstellation);
2523 old_constellation=null_constellation;
2534 old_constellation=null_constellation;
2542 old_constellation=null_constellation;
2546 else if (this_block_to_constellation->is_stable())
2550 new_position=m_branching ? new_bi->block.to_constellation.begin()
2551 : new_bi->block.to_constellation.end();
2552 } assert(!m_branching || new_bi->block.to_constellation.end()!=new_position);
2553 BLC_list_iterator old_BLC_start=
2554 this_block_to_constellation->start_same_BLC;
2555 new_BLC_block=new_bi->block.to_constellation.emplace_after
2556 (new_position, old_BLC_start, old_BLC_start,
2557 this_block_to_constellation->is_stable());
2558 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2559 new_BLC_block->work_counter=this_block_to_constellation->work_counter;
2561 ++no_of_non_constellation_inert_BLC_sets;
2564 const bool last_element_removed=
2565 swap_in_the_doubly_linked_list_LBC_in_blocks_new_block(ti,
2566 new_BLC_block, this_block_to_constellation);
2568 if (last_element_removed)
2570 if (null_constellation != old_constellation)
2583 m_BLC_indicators_to_be_deleted.push_back
2584 (this_block_to_constellation);
2589 old_bi->block.to_constellation.erase(this_block_to_constellation);
2591 if (!t_is_inert || to_constln!=new_bi->c.onstellation)
2593 --no_of_non_constellation_inert_BLC_sets;
2595 } assert(old_bi->block.to_constellation.check_linked_list());
2597 assert(new_bi->block.to_constellation.check_linked_list());
2598 check_transitions(no_of_constellations<=1,
false,
false);
2608 void clear_state_counters(
2609 std::vector<state_in_block_pointer>::const_iterator begin,
2610 std::vector<state_in_block_pointer>::const_iterator
const end,
2611 block_type*
const block)
2615 { assert(block==begin->ref_state->block);
2616 begin->ref_state->counter=undefined;
2624 void change_non_bottom_state_to_bottom_state(
2625 const fixed_vector<state_type_gj>::iterator si)
2626 { assert(m_states.begin()<=si);
2627 block_type* bi = si->block; assert(si<m_states.end());
2628 swap_states_in_states_in_block(si->ref_states_in_blocks,
2629 bi->sta.rt_non_bottom_states); assert(0 == si->no_of_outgoing_block_inert_transitions);
2630 bi->sta.rt_non_bottom_states++; assert(!bi->contains_new_bottom_states);
2631 ++no_of_new_bottom_states;
2635 void make_stable_and_move_to_start_of_BLC(block_type*
const from_block,
2636 const linked_list<BLC_indicators>::iterator splitter)
2637 { assert(from_block->block.to_constellation.end()!=splitter);
2638 splitter->make_stable(); assert(splitter->start_same_BLC<splitter->end_same_BLC);
2640 const transition& t=m_aut.get_transitions()[*splitter->start_same_BLC];
2641 assert(from_block==m_states[t.from()].block);
2643 linked_list<BLC_indicators>& btc=from_block->block.to_constellation; assert(!btc.empty());
2644 if (splitter!=btc.begin())
2646 linked_list<BLC_indicators>::iterator move_splitter_after=btc.end();
2649 const transition& perhaps_inert_t=
2650 m_aut.get_transitions()[*btc.begin()->start_same_BLC];
2651 if (is_inert_during_init_if_branching(perhaps_inert_t) &&
2652 m_states[perhaps_inert_t.to()].block->c.onstellation==
2653 from_block->c.onstellation)
2655 move_splitter_after=btc.begin();
2658 btc.splice_to_after(move_splitter_after, btc, splitter);
2666 void move_nonbottom_states_to(
const todo_state_vector& R,
2667 state_in_block_pointer* to_pos
2668 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2669 , state_index new_block_bottom_size
2673 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2674 unsigned char const max_B=check_complexity::log_n-
2675 check_complexity::ilog2(new_block_bottom_size+R.size());
2677 for (
const state_in_block_pointer& st: R)
2679 split_block_B_into_R_and_BminR_carry_out_split, max_B), *
this);
2680 swap_states_in_states_in_block(to_pos++,
2681 st.ref_state->ref_states_in_blocks);
2693 block_type* update_BLC_sets_new_block(block_type*
const old_bi,
2694 block_type*
const new_bi,
2695 constellation_type*
const old_constellation,
2696 constellation_type*
const new_constellation)
2700 assert(!old_bi->block.to_constellation.empty());
2703 BLC_list_iterator start_inert_BLC=
2704 old_bi->block.to_constellation.begin()->start_same_BLC;
2705 linked_list<BLC_indicators>::iterator new_inert_BLC_set=
2706 new_bi->block.to_constellation.emplace_front(start_inert_BLC,
2707 start_inert_BLC,
true);
2708 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2709 assert(start_inert_BLC<old_bi->block.to_constellation.begin()->end_same_BLC);
2710 const transition& perhaps_inert_t=m_aut.get_transitions()[*start_inert_BLC];
2711 assert(m_states[perhaps_inert_t.from()].block==old_bi ||
2712 m_states[perhaps_inert_t.from()].block==new_bi);
2713 if (is_inert_during_init(perhaps_inert_t) &&
2714 m_states[perhaps_inert_t.to()].block->c.onstellation==
2715 old_bi->c.onstellation)
2719 new_inert_BLC_set->work_counter=
2720 old_bi->block.to_constellation.begin()->work_counter;
2723 (
void) new_inert_BLC_set;
2727 const state_in_block_pointer*
const it_end=new_bi->end_states;
2728 for (state_in_block_pointer*
2729 it=new_bi->start_bottom_states; it_end!=it; ++it)
2730 { assert(new_bi==it->ref_state->block);
2731 outgoing_transitions_const_it
const out_it_end=
2732 std::next(it->ref_state)==m_states.end()
2733 ? m_outgoing_transitions.end()
2734 : std::next(it->ref_state)->start_outgoing_transitions;
2735 for (outgoing_transitions_it out_it=it->ref_state->
2736 start_outgoing_transitions; out_it_end!=out_it; ++out_it)
2738 update_the_doubly_linked_list_LBC_new_block(old_bi, new_bi,
2739 *out_it->ref.BLC_transitions, old_constellation, new_constellation);
2744 { assert(!new_bi->block.to_constellation.empty());
2751 inert_ind=new_bi->block.to_constellation.begin();
2752 if (inert_ind->start_same_BLC==inert_ind->end_same_BLC)
2753 { assert(inert_ind->is_stable());
2754 new_bi->block.to_constellation.erase(inert_ind);
2758 for (std::vector<
linked_list<BLC_indicators>::iterator>::iterator
2759 it=m_BLC_indicators_to_be_deleted.begin();
2760 it<m_BLC_indicators_to_be_deleted.end(); ++it)
2761 { assert((*it)->start_same_BLC==(*it)->end_same_BLC);
2763 old_bi->block.to_constellation.erase(*it);
2765 clear(m_BLC_indicators_to_be_deleted);
2781 template<
bool initialisation =
false>
2782 block_type* create_new_block(
2783 state_in_block_pointer* start_bottom_states,
2784 state_in_block_pointer*
const start_non_bottom_states,
2785 state_in_block_pointer*
const end_states,
2786 block_type*
const old_block_index,
2787 constellation_type*
const old_constellation,
2788 constellation_type*
const new_constellation)
2791 constellation_type*
const constellation=old_block_index->c.onstellation; assert(constellation->start_const_states<=start_bottom_states);
2792 assert(start_bottom_states<end_states);
2793 block_type*
const new_block_index=
2795 simple_list<BLC_indicators>::get_pool().
2796 template construct<block_type>
2800 (start_bottom_states,
2801 start_non_bottom_states, end_states, constellation); assert(end_states<=constellation->end_const_states);
2804 new_block_index->work_counter=old_block_index->work_counter;
2806 for(; start_bottom_states<start_non_bottom_states; ++start_bottom_states)
2808 start_bottom_states->ref_state->no_of_outgoing_block_inert_transitions);
2809 assert(old_block_index==start_bottom_states->ref_state->block);
2810 start_bottom_states->ref_state->block=new_block_index; assert(start_bottom_states->ref_state->counter==undefined);
2812 for (; start_bottom_states<end_states; ++start_bottom_states)
2813 { assert(old_block_index==start_bottom_states->ref_state->block);
2814 start_bottom_states->ref_state->block=new_block_index; assert(0!=
2815 start_bottom_states->ref_state->no_of_outgoing_block_inert_transitions);
2816 start_bottom_states->ref_state->counter=undefined;
2819 if constexpr (initialisation)
2821 return new_block_index;
2824 return update_BLC_sets_new_block(old_block_index, new_block_index,
2825 old_constellation, new_constellation);
2829 void check_incoming_tau_transitions_become_noninert(
2830 block_type* NewBotSt_block_index,
2831 state_in_block_pointer* start_bottom,
2832 state_in_block_pointer*
const end_non_bottom)
2834 for (; start_bottom!=end_non_bottom; ++start_bottom)
2836 std::vector<transition>::const_iterator
const in_it_end=
2837 std::next(start_bottom->ref_state)>=m_states.end()
2838 ? m_aut.get_transitions().end()
2839 : std::next(start_bottom->ref_state)->start_incoming_transitions; assert(start_bottom->ref_state->block!=NewBotSt_block_index);
2840 for (std::vector<transition>::iterator
2841 in_it=start_bottom->ref_state->start_incoming_transitions;
2843 m_aut.is_tau(m_aut_apply_hidden_label_map(in_it->label()));
2846 const fixed_vector<state_type_gj>::iterator
2847 from=m_states.begin()+
static_cast<std::ptrdiff_t>(in_it->from()); assert(m_states[in_it->to()].ref_states_in_blocks==start_bottom);
2848 if (NewBotSt_block_index==from->block)
2850 if (0== --from->no_of_outgoing_block_inert_transitions)
2852 change_non_bottom_state_to_bottom_state(from);
2862 next_target_constln_in_same_saC(state_in_block_pointer
const src,
2863 BLC_list_const_iterator
const splitter_it)
const
2864 { assert(m_states.begin()+m_aut.get_transitions()[*splitter_it].from()==
2866 outgoing_transitions_const_it
2867 out_it=m_transitions[*splitter_it].ref_outgoing_transitions;
2868 if (out_it<out_it->start_same_saC)
2870 out_it=out_it->start_same_saC;
2873 outgoing_transitions_const_it
const
2874 out_it_end=std::next(src.ref_state)>=m_states.end()
2875 ? m_outgoing_transitions.end()
2876 : std::next(src.ref_state)->start_outgoing_transitions;
2877 if (out_it<out_it_end)
2879 return m_transitions[*out_it->ref.BLC_transitions].
2880 transitions_per_block_to_constellation;
2964 template <
bool has_small_splitter,
bool has_large_splitter>
2965 block_type* four_way_splitB(block_type*
const bi,
2966 linked_list<BLC_indicators>::iterator
const small_splitter,
2967 linked_list<BLC_indicators>::iterator
const large_splitter,
2968 constellation_type*
const old_constellation,
2969 constellation_type*
const new_constellation)
2971 assert(1<number_of_states_in_block(*bi));
2972 assert(!bi->contains_new_bottom_states);
2979 static std::vector<state_in_block_pointer>potential_non_bottom_states[3]; assert(potential_non_bottom_states[ReachAlw].empty());
2980 assert(potential_non_bottom_states[AvoidSml].empty());
2981 assert(potential_non_bottom_states[AvoidLrg].empty());
2982 static std::vector<state_in_block_pointer>
2983 potential_non_bottom_states_HitSmall; assert(potential_non_bottom_states_HitSmall.empty());
2997 static todo_state_vector non_bottom_states[4];
2999 #define non_bottom_states_NewBotSt non_bottom_states[3
]
3013 state_in_block_pointer* start_bottom_states[4]; assert(non_bottom_states[ReachAlw].empty());
3014 start_bottom_states[ReachAlw]=bi->start_bottom_states; assert(non_bottom_states[AvoidSml].empty());
3015 start_bottom_states[AvoidSml]=bi->start_bottom_states; assert(non_bottom_states[AvoidLrg].empty());
3017 #define bottom_size(coroutine) ( assert
(ReachAlw==(coroutine)||AvoidSml==(coroutine)||AvoidLrg==(coroutine)),
3018 assert
(start_bottom_states[(coroutine)]<=start_bottom_states[(coroutine)+1
]),
3019 static_cast<state_type>
3020 (std::distance(start_bottom_states[(coroutine)],
3021 start_bottom_states[(coroutine)+1
])))
3022 #define bottom_and_non_bottom_size(coroutine) ( assert
(aborted!=status[(coroutine)]),
3023 bottom_size((coroutine))+non_bottom_states[(coroutine)].size())
3030 BLC_list_iterator large_splitter_iter_NewBotSt;
3031 BLC_list_const_iterator large_splitter_iter_end_NewBotSt;
3033 if (has_small_splitter )
3034 { assert(bi->block.to_constellation.end()!=small_splitter);
3036 start_bottom_states[AvoidLrg]=bi->sta.rt_non_bottom_states; assert(small_splitter->is_stable());
3039 main_t=m_aut.get_transitions()[*small_splitter->start_same_BLC];
3040 assert(bi==m_states[main_t.from()].block);
3054 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3055 const unsigned char max_C=check_complexity::log_n-check_complexity::
3056 ilog2(number_of_states_in_constellation(*new_constellation));
3059 if (has_large_splitter )
3060 { assert(bi->block.to_constellation.end()!=large_splitter);
3062 four_way_splitB_handle_transitions_in_main_splitter, max_C), *
this);
3064 const transition& co_t=m_aut.get_transitions()[*large_splitter->start_same_BLC];
3065 assert(bi==m_states[co_t.from()].block);
3066 assert(label_or_divergence(main_t)==label_or_divergence(co_t));
3067 assert(!is_inert_during_init(main_t) ||
3068 (new_constellation!=bi->c.onstellation &&
3069 old_constellation!=bi->c.onstellation));
3071 large_splitter_iter_NewBotSt=large_splitter->start_same_BLC; assert(new_constellation==m_states[main_t.to()].block->c.onstellation);
3072 large_splitter_iter_end_NewBotSt=large_splitter->end_same_BLC; assert(old_constellation==m_states[co_t.to()].block->c.onstellation);
3075 { assert(bi->block.to_constellation.end()==large_splitter);
3076 assert((1==max_C) ^ is_inert_during_init(main_t));
3077 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3078 if (old_constellation==bi->c.onstellation) {
3081 four_way_splitB_handle_transitions_in_main_splitter, max_C), *
this);
3082 assert(new_constellation==m_states[main_t.to()].block->c.onstellation);
3086 refine_partition_until_it_becomes_stable_prepare_cosplit,max_C),*
this);
3087 assert(new_constellation==bi->c.onstellation);
3089 assert(number_of_states_in_block(*bi)==
3090 number_of_states_in_constellation(*new_constellation));
3091 assert(old_constellation==m_states[main_t.to()].block->c.onstellation);
3095 large_splitter_iter_NewBotSt=m_BLC_transitions.data_end();
3096 large_splitter_iter_end_NewBotSt=m_BLC_transitions.data_end();
3102 BLC_list_iterator splitter_it=small_splitter->start_same_BLC; assert(splitter_it!=small_splitter->end_same_BLC);
3105 state_in_block_pointer
const src=m_states.begin()+
3106 m_aut.get_transitions()[*splitter_it].from();
3107 if (0==src.ref_state->no_of_outgoing_block_inert_transitions)
3108 { assert(bi->start_bottom_states<=src.ref_state->ref_states_in_blocks);
3109 assert(src.ref_state->ref_states_in_blocks<bi->sta.rt_non_bottom_states);
3110 if (src.ref_state->ref_states_in_blocks<
3111 start_bottom_states[AvoidSml])
3114 if (has_large_splitter) {
3115 assert(next_target_constln_in_same_saC(src, splitter_it)==large_splitter);
3119 else if (!has_large_splitter )
3121 static_assert(ReachAlw + 1 == AvoidSml);
3122 swap_states_in_states_in_block(start_bottom_states[AvoidSml],
3123 src.ref_state->ref_states_in_blocks);
3124 ++start_bottom_states[AvoidSml];
3126 else if (start_bottom_states[AvoidSml+1]<=
3127 src.ref_state->ref_states_in_blocks)
3130 assert(bi->block.to_constellation.end()!=large_splitter);
3131 outgoing_transitions_const_it
const out_it_end=std::next(src.ref_state)>=
3132 m_states.end() ? m_outgoing_transitions.end()
3133 : std::next(src.ref_state)->start_outgoing_transitions;
3134 for (outgoing_transitions_const_it out_it=src.ref_state->
3135 start_outgoing_transitions; out_it!=out_it_end; ++out_it)
3137 assert(m_transitions[*out_it->ref.BLC_transitions].
3138 transitions_per_block_to_constellation!=large_splitter);
3142 else if (next_target_constln_in_same_saC(src, splitter_it)==
3145 static_assert(ReachAlw + 1 == AvoidSml);
3146 swap_states_in_states_in_block(start_bottom_states[AvoidSml],
3147 src.ref_state->ref_states_in_blocks);
3148 ++start_bottom_states[AvoidSml];
3152 static_assert(AvoidSml + 1 == AvoidLrg);
3153 --start_bottom_states[AvoidSml+1];
3154 swap_states_in_states_in_block(start_bottom_states[AvoidSml+1],
3155 src.ref_state->ref_states_in_blocks);
3160 assert(bi->sta.rt_non_bottom_states<=src.ref_state->ref_states_in_blocks);
3161 assert(src.ref_state->ref_states_in_blocks<bi->end_states);
3162 if (undefined==src.ref_state->counter)
3164 if (!has_large_splitter ||
3165 next_target_constln_in_same_saC(src, splitter_it)==
3169 src.ref_state->counter=marked(ReachAlw)+
3170 src.ref_state->no_of_outgoing_block_inert_transitions; assert(is_in_marked_range_of(src.ref_state->counter, ReachAlw));
3172 potential_non_bottom_states[ReachAlw].push_back(src);
3177 src.ref_state->counter=marked_HitSmall;
3178 potential_non_bottom_states_HitSmall.push_back(src);
3180 outgoing_transitions_const_it
const out_it_end=std::next(src.ref_state)>=
3181 m_states.end() ? m_outgoing_transitions.end()
3182 : std::next(src.ref_state)->start_outgoing_transitions;
3183 for (outgoing_transitions_const_it out_it=src.ref_state->
3184 start_outgoing_transitions; out_it!=out_it_end; ++out_it)
3186 assert(has_small_splitter || has_large_splitter),
3187 assert(m_transitions[*out_it->ref.BLC_transitions].
3188 transitions_per_block_to_constellation!=large_splitter);
3194 else if (marked_HitSmall==src.ref_state->counter) {
3195 assert(bi->block.to_constellation.end()!=large_splitter);
3197 assert(is_in_marked_range_of(src.ref_state->counter, ReachAlw));
3198 if (bi->block.to_constellation.end()!=large_splitter) {
3199 assert(has_small_splitter || has_large_splitter),
3200 assert(next_target_constln_in_same_saC(src,splitter_it)==large_splitter);
3207 while (splitter_it!=small_splitter->end_same_BLC);
3209 else if (has_large_splitter )
3210 { assert(bi->block.to_constellation.end()==small_splitter);
3211 assert(bi->block.to_constellation.end()!=large_splitter);
3212 assert(!large_splitter->is_stable());
3213 assert(null_constellation==old_constellation);
3220 large_splitter_iter_NewBotSt=large_splitter->start_same_BLC;
3221 large_splitter_iter_end_NewBotSt=large_splitter->start_marked_BLC;
3223 for (BLC_list_iterator co_splitter_it=large_splitter->start_marked_BLC;
3224 co_splitter_it!=large_splitter->end_same_BLC; ++co_splitter_it)
3226 state_in_block_pointer
const src=m_states.begin()+
3227 m_aut.get_transitions()[*co_splitter_it].from(); assert(0==src.ref_state->no_of_outgoing_block_inert_transitions);
3228 assert(bi->start_bottom_states<=src.ref_state->ref_states_in_blocks);
3229 assert(src.ref_state->ref_states_in_blocks<bi->sta.rt_non_bottom_states);
3230 if (start_bottom_states[AvoidSml]<=
3231 src.ref_state->ref_states_in_blocks)
3233 swap_states_in_states_in_block(start_bottom_states[AvoidSml],
3234 src.ref_state->ref_states_in_blocks);
3235 ++start_bottom_states[AvoidSml];
3239 start_bottom_states[AvoidLrg]=start_bottom_states[AvoidSml];
3240 make_stable_and_move_to_start_of_BLC(bi, large_splitter);
3243 { assert(bi->block.to_constellation.end()==small_splitter);
3244 assert(bi->block.to_constellation.end()==large_splitter);
3255 start_bottom_states[AvoidSml]=bi->c.first_unmarked_bottom_state;
3256 start_bottom_states[AvoidSml+1]=bi->sta.rt_non_bottom_states; assert(
nullptr!=bi->block.R);
3257 potential_non_bottom_states[ReachAlw].swap(*bi->block.R); assert(null_constellation==old_constellation);
3261 bi->block.R=
nullptr; assert(null_constellation!=new_constellation);
3263 new (&bi->c) block_type::
3264 constellation_or_first_unmarked_bottom_state(new_constellation);
3266 for (
const state_in_block_pointer& st: potential_non_bottom_states[ReachAlw])
3268 assert(0<st.ref_state->no_of_outgoing_block_inert_transitions);
3269 assert(st.ref_state->counter==marked(ReachAlw)+st.ref_state->no_of_outgoing_block_inert_transitions);
3270 assert(is_in_marked_range_of(st.ref_state->counter, ReachAlw));
3273 large_splitter_iter_NewBotSt=m_BLC_transitions.data_end();
3274 large_splitter_iter_end_NewBotSt=m_BLC_transitions.data_end();
3277 assert(bi->start_bottom_states==start_bottom_states[ReachAlw]);
3278 assert(start_bottom_states[ReachAlw]<=start_bottom_states[AvoidSml]);
3279 assert(start_bottom_states[AvoidSml]<=start_bottom_states[AvoidLrg]);
3280 assert(start_bottom_states[AvoidLrg]<=start_bottom_states[AvoidLrg+1]);
3281 assert(start_bottom_states[AvoidLrg+1]==bi->sta.rt_non_bottom_states);
3283 if (bi->sta.rt_non_bottom_states==bi->end_states)
3286 block_type* ReachAlw_block_index=null_block;
3287 constellation_type*
const constellation=bi->c.onstellation;
3288 bool constellation_was_trivial=
3289 constellation->start_const_states->ref_state->block==
3290 std::prev(constellation->end_const_states)->ref_state->block;
3291 bool constellation_becomes_nontrivial=
false;
3293 { assert(bi->start_bottom_states==start_bottom_states[ReachAlw]);
3294 if (!has_small_splitter || 0<
bottom_size(ReachAlw))
3296 bi->start_bottom_states=start_bottom_states[ReachAlw+1];
3297 ReachAlw_block_index=create_new_block
3298 <!has_small_splitter && !has_large_splitter>
3299 (start_bottom_states[ReachAlw],
3300 start_bottom_states[ReachAlw+1],
3301 start_bottom_states[ReachAlw+1], bi,
3302 old_constellation, new_constellation);
3303 constellation_becomes_nontrivial=
true;
3307 assert(bi->start_bottom_states==start_bottom_states[AvoidSml]);
3308 if (has_small_splitter && 0<
bottom_size(AvoidSml))
3310 bi->start_bottom_states=start_bottom_states[AvoidSml+1];
3311 create_new_block<!has_small_splitter && !has_large_splitter>
3312 (start_bottom_states[AvoidSml],
3313 start_bottom_states[AvoidSml+1],
3314 start_bottom_states[AvoidSml+1], bi,
3315 old_constellation, new_constellation);
3316 constellation_becomes_nontrivial=
true;
3320 { assert(bi->end_states==start_bottom_states[AvoidLrg+1]);
3321 bi->sta.rt_non_bottom_states=start_bottom_states[AvoidLrg];
3322 bi->end_states=start_bottom_states[AvoidLrg];
3323 create_new_block<!has_small_splitter && !has_large_splitter>
3324 (start_bottom_states[AvoidLrg],
3325 start_bottom_states[AvoidLrg+1],
3326 start_bottom_states[AvoidLrg+1], bi,
3327 old_constellation, new_constellation);
3328 constellation_becomes_nontrivial=
true;
3333 assert(bi->end_states==start_bottom_states[AvoidLrg+1]);
3334 if (has_large_splitter && 0<
bottom_size(AvoidLrg))
3336 bi->sta.rt_non_bottom_states=start_bottom_states[AvoidLrg];
3337 bi->end_states=start_bottom_states[AvoidLrg];
3338 create_new_block<!has_small_splitter && !has_large_splitter>
3339 (start_bottom_states[AvoidLrg],
3340 start_bottom_states[AvoidLrg+1],
3341 start_bottom_states[AvoidLrg+1], bi,
3342 old_constellation, new_constellation);
3343 constellation_becomes_nontrivial=
true;
3345 if ((has_small_splitter || !has_large_splitter) &&
3347 { assert(bi->start_bottom_states==start_bottom_states[ReachAlw]);
3348 bi->start_bottom_states=start_bottom_states[ReachAlw+1]; assert(0<
bottom_size(ReachAlw));
3349 ReachAlw_block_index=create_new_block
3350 <!has_small_splitter && !has_large_splitter>
3351 (start_bottom_states[ReachAlw],
3352 start_bottom_states[ReachAlw+1],
3353 start_bottom_states[ReachAlw+1], bi,
3354 old_constellation, new_constellation);
3355 constellation_becomes_nontrivial=
true;
3359 ReachAlw_block_index=bi;
3360 if ((has_small_splitter || !has_large_splitter) &&
3362 { assert(bi->end_states==start_bottom_states[AvoidSml+1]);
3363 bi->sta.rt_non_bottom_states=start_bottom_states[AvoidSml];
3364 bi->end_states=start_bottom_states[AvoidSml];
3365 create_new_block<!has_small_splitter && !has_large_splitter>
3366 (start_bottom_states[AvoidSml],
3367 start_bottom_states[AvoidSml+1],
3368 start_bottom_states[AvoidSml+1], bi,
3369 old_constellation, new_constellation);
3370 constellation_becomes_nontrivial=
true;
3375 if (constellation_becomes_nontrivial && constellation_was_trivial)
3376 { assert(std::find(m_non_trivial_constellations.begin(),
3377 m_non_trivial_constellations.end(),
3378 constellation)==m_non_trivial_constellations.end());
3379 m_non_trivial_constellations.emplace_back(constellation);
3382 return ReachAlw_block_index;
3383 } assert(m_branching);
3405 assert(non_bottom_states[ReachAlw].empty());
3406 assert(non_bottom_states[AvoidSml].empty());
3407 assert(non_bottom_states[AvoidLrg].empty());
3410 enum { state_checking,
3411 incoming_inert_transition_checking,
3412 outgoing_constellation_checking,
3413 aborted, finished } status[3], status_NewBotSt;
3414 state_in_block_pointer* current_bottom_state_iter[3];
3419 state_index no_of_unfinished_states_in_block=
3420 number_of_states_in_block(*bi);
3427 #define abort_if_bottom_size_too_large(coroutine)
3428 (( assert
(non_bottom_states[(coroutine)].empty()),
3429 bottom_size((coroutine))>no_of_unfinished_states_in_block/2
) &&
3430 ( assert
(std::numeric_limits<state_index>::max()!=
3431 no_of_unfinished_states_in_block),
3432 no_of_unfinished_states_in_block=
3433 std::numeric_limits<state_index>::max(), assert
(m_aut.num_states()<no_of_unfinished_states_in_block/2
),
3434 status[(coroutine)]=aborted,
3448 #define abort_if_non_bottom_size_too_large_NewBotSt(i)
3449 (non_bottom_states_NewBotSt.size()+(i)>
3450 no_of_unfinished_states_in_block/2
&&
3451 ( assert
(std::numeric_limits<state_index>::max()!=
3452 no_of_unfinished_states_in_block),
3453 no_of_unfinished_states_in_block=
3454 std::numeric_limits<state_index>::max(), assert
(m_aut.num_states()<no_of_unfinished_states_in_block/2
),
3455 status_NewBotSt=aborted,
3470 #define abort_if_size_too_large(coroutine, i)
3471 (bottom_and_non_bottom_size((coroutine))+(i)>
3472 no_of_unfinished_states_in_block/2
&&
3473 ( assert
(std::numeric_limits<state_index>::max()!=
3474 no_of_unfinished_states_in_block),
3475 no_of_unfinished_states_in_block=
3476 std::numeric_limits<state_index>::max(), assert
(m_aut.num_states()<no_of_unfinished_states_in_block/2
),
3477 status[(coroutine)]=aborted,
3478 non_bottom_states[(coroutine)].clear(),
3481 int no_of_finished_searches=0;
3482 int no_of_running_searches=0;
3483 enum subblocks running_searches[3];
3485 if ((!has_small_splitter && has_large_splitter) ||
3488 assert(potential_non_bottom_states[AvoidSml].empty());
3490 if (!has_large_splitter || 0==
bottom_size(AvoidLrg))
3499 clear_state_counters(potential_non_bottom_states[ReachAlw].begin(),
3500 potential_non_bottom_states[ReachAlw].end(), bi);
3501 clear(potential_non_bottom_states[ReachAlw]);
3502 if (has_small_splitter && has_large_splitter)
3504 clear_state_counters(potential_non_bottom_states_HitSmall.begin(),
3505 potential_non_bottom_states_HitSmall.end(), bi);
3506 clear(potential_non_bottom_states_HitSmall);
3507 }
else { assert(potential_non_bottom_states_HitSmall.empty()); }
3511 ++no_of_finished_searches;
3512 status[AvoidSml]=finished;
3516 running_searches[no_of_running_searches]=AvoidSml;
3517 ++no_of_running_searches;
3518 current_bottom_state_iter[AvoidSml]=start_bottom_states[AvoidSml];
3519 status[AvoidSml]=state_checking;
3522 if (!has_large_splitter || 0==
bottom_size(AvoidLrg))
3524 assert(potential_non_bottom_states[AvoidLrg].empty());
3525 ++no_of_finished_searches;
3526 status[AvoidLrg]=finished;
3530 running_searches[no_of_running_searches]=AvoidLrg;
3531 ++no_of_running_searches;
3532 current_bottom_state_iter[AvoidLrg]=start_bottom_states[AvoidLrg];
3533 status[AvoidLrg]=state_checking;
3536 status_NewBotSt=state_checking;
3544 (potential_non_bottom_states[ReachAlw]);
3545 if (!has_large_splitter || finished==status[AvoidLrg])
3546 { assert(finished==status[AvoidLrg]);
3550 if (has_small_splitter && has_large_splitter)
3555 (potential_non_bottom_states_HitSmall.begin(),
3556 potential_non_bottom_states_HitSmall.end());
3557 clear(potential_non_bottom_states_HitSmall);
3562 (potential_non_bottom_states_HitSmall);
3564 }
else { assert(potential_non_bottom_states_HitSmall.empty()); }
3569 st.ref_state->counter=marked_NewBotSt;
3571 ++no_of_finished_searches;
3572 status[ReachAlw]=finished; assert(aborted!=status_NewBotSt);
3577 running_searches[no_of_running_searches]=ReachAlw;
3578 ++no_of_running_searches;
3579 current_bottom_state_iter[ReachAlw]=start_bottom_states[ReachAlw];
3580 status[ReachAlw]=state_checking;
3602 std::vector<transition>::iterator current_source_iter[3];
3603 std::vector<transition>::iterator current_source_iter_NewBotSt;
3604 std::vector<transition>::const_iterator current_source_iter_end[3];
3605 std::vector<transition>::const_iterator current_source_iter_end_NewBotSt;
3607 state_in_block_pointer current_source_AvoidLrg;
3608 outgoing_transitions_const_it current_outgoing_iter_start_AvoidLrg;
3609 outgoing_transitions_const_it current_outgoing_iter_AvoidLrg; assert(large_splitter_iter_NewBotSt<=large_splitter_iter_end_NewBotSt);
3611 { assert(2>=no_of_finished_searches);
3612 state_in_block_pointer* new_start_bottom_states_plus_one[3];
3613 state_in_block_pointer* new_end_bottom_states_plus_one[2];
3614 #define new_start_bottom_states(idx) ( assert
(1
<=(idx)), assert
((idx)<=3
),
3615 new_start_bottom_states_plus_one[(idx)-1
])
3616 #define new_end_bottom_states(idx) ( assert
(1
<=(idx)), assert
((idx)<=2
),
3617 new_end_bottom_states_plus_one[(idx)-1
])
3618 #define new_end_bottom_states_NewBotSt
3619 (new_start_bottom_states_plus_one[2
])
3620 for (
int current_search_index=0; current_search_index<
3621 no_of_running_searches; ++current_search_index)
3623 const enum subblocks
3624 current_search=running_searches[current_search_index]; assert(0<=current_search); assert(current_search<NewBotSt);
3626 if (incoming_inert_transition_checking==status[current_search])
3627 { assert(current_source_iter[current_search]<
3628 current_source_iter_end[current_search]);
3629 mCRL2complexity(&m_transitions[std::distance(m_aut.get_transitions().begin(),
3630 current_source_iter[current_search])], add_work(check_complexity::
3631 simple_splitB_U_handle_transition_to_U_state, 1), *
this);
3632 const transition& tr=*current_source_iter[current_search]++; assert(m_aut.is_tau(m_aut_apply_hidden_label_map(tr.label())));
3633 state_in_block_pointer
const src=m_states.begin()+
static_cast<std::ptrdiff_t>(tr.from()); assert(m_states[tr.to()].block==bi);
3635 if (src.ref_state->block==bi &&
3636 !(m_preserve_divergence && tr.from()==tr.to()))
3637 { assert(!non_bottom_states[ReachAlw].find(src));
3638 assert(!non_bottom_states[AvoidSml].find(src));
3639 assert(!non_bottom_states[AvoidLrg].find(src));
3640 const transition_index current_counter=src.ref_state->counter;
3642 if( ( ( undefined==current_counter
3643 || ( has_small_splitter && has_large_splitter
3644 && marked_HitSmall==current_counter
3645 && AvoidSml!=current_search ) || (assert(marked_HitSmall!=current_counter || AvoidSml==current_search),
false)
3648 src.ref_state->counter=marked(current_search)+
3649 src.ref_state->no_of_outgoing_block_inert_transitions, assert(std::find(potential_non_bottom_states[current_search].begin(),
3650 potential_non_bottom_states[current_search].end(), src)==
3651 potential_non_bottom_states[current_search].end()),
3652 potential_non_bottom_states[current_search].
3655 || is_in_marked_range_of(current_counter, current_search) )
3656 { assert(is_in_marked_range_of(src.ref_state->counter, current_search));
3658 --src.ref_state->counter; assert(is_in_marked_range_of(src.ref_state->counter, current_search));
3660 if (marked(current_search)==src.ref_state->counter)
3661 {
if (!has_large_splitter) {
3662 assert(AvoidLrg!=current_search);
3663 if (!has_small_splitter) { assert(marked_HitSmall!=current_counter); }
3665 if (has_large_splitter &&
3666 AvoidLrg==current_search &&
3667 large_splitter_iter_NewBotSt!=
3668 large_splitter_iter_end_NewBotSt)
3669 { assert(bi->block.to_constellation.end()!=large_splitter);
3676 current_source_AvoidLrg=src;
3677 status[AvoidLrg]=outgoing_constellation_checking;
3678 current_outgoing_iter_start_AvoidLrg=
3679 src.ref_state->start_outgoing_transitions;
3680 current_outgoing_iter_AvoidLrg=
3681 std::next(src.ref_state)>=m_states.end()
3682 ? m_outgoing_transitions.end()
3683 : std::next(src.ref_state)->start_outgoing_transitions; assert(current_outgoing_iter_start_AvoidLrg<current_outgoing_iter_AvoidLrg);
3685 }
else { assert(AvoidLrg!=current_search ||
3686 large_splitter_iter_NewBotSt==large_splitter_iter_end_NewBotSt); }
3688 { assert(running_searches[current_search_index]==current_search);
3689 --no_of_running_searches; assert(current_search_index<=no_of_running_searches);
3690 running_searches[current_search_index]=
3691 running_searches[no_of_running_searches]; assert(std::find(potential_non_bottom_states[current_search].begin(),
3692 potential_non_bottom_states[current_search].end(), src)!=
3693 potential_non_bottom_states[current_search].end());
3694 --current_search_index;
3698 non_bottom_states[current_search].add_todo(src);
3702 else if (marked_NewBotSt!=src.ref_state->counter)
3708 if (aborted!=status_NewBotSt &&
3716 src.ref_state->counter=marked_NewBotSt;
3722 if (current_source_iter[current_search]!=
3723 current_source_iter_end[current_search] &&
3724 m_aut.is_tau(m_aut_apply_hidden_label_map
3725 (current_source_iter[current_search]->label())))
3729 status[current_search]=state_checking;
3731 else if (!has_large_splitter||state_checking==status[current_search])
3732 { assert(state_checking==status[current_search]);
3734 state_in_block_pointer
const tgt=
3735 current_bottom_state_iter[current_search]<
3736 start_bottom_states[current_search+1]
3737 ? *current_bottom_state_iter[current_search]++
3738 : non_bottom_states[current_search].move_from_todo(); assert(!non_bottom_states[current_search^1].find(tgt));
3741 add_work(check_complexity::simple_splitB_U_find_predecessors, 1), *
this);
3742 current_source_iter[current_search]=
3743 tgt.ref_state->start_incoming_transitions; assert(!non_bottom_states[current_search^2].find(tgt));
3744 current_source_iter_end[current_search]=
3745 std::next(tgt.ref_state)>=m_states.end()
3746 ? m_aut.get_transitions().end()
3747 : std::next(tgt.ref_state)->start_incoming_transitions; assert(!non_bottom_states[current_search^3].find(tgt));
3748 if (current_source_iter[current_search]<
3749 current_source_iter_end[current_search] &&
3750 m_aut.is_tau(m_aut_apply_hidden_label_map
3751 (current_source_iter[current_search]->label())))
3753 status[current_search]=incoming_inert_transition_checking;
3758 { assert(AvoidLrg==current_search);
3759 assert(outgoing_constellation_checking==status[AvoidLrg]);
3760 assert(current_outgoing_iter_start_AvoidLrg<current_outgoing_iter_AvoidLrg);
3761 assert(m_outgoing_transitions.end()==current_outgoing_iter_AvoidLrg ||
3762 current_outgoing_iter_start_AvoidLrg<
3763 current_outgoing_iter_AvoidLrg->start_same_saC);
3764 --current_outgoing_iter_AvoidLrg; assert(current_outgoing_iter_AvoidLrg->start_same_saC<=
3765 current_outgoing_iter_AvoidLrg);
3766 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3768 outgoing_transitions_const_it out_it=
3769 current_outgoing_iter_AvoidLrg->start_same_saC;
3770 assert(has_small_splitter || has_large_splitter);
3772 add_work(check_complexity::
3773 simple_splitB_U_handle_transition_from_potential_U_state, 1), *
this);
3775 while (++out_it<=current_outgoing_iter_AvoidLrg) {
3776 assert(has_small_splitter || has_large_splitter);
3778 add_work_notemporary(check_complexity::
3779 simple_splitB_U_handle_transition_from_potential_U_state, 1), *
this);
3783 assert(!non_bottom_states[ReachAlw].find(current_source_AvoidLrg));
3784 assert(!non_bottom_states[AvoidLrg].find(current_source_AvoidLrg));
3785 assert(!non_bottom_states[AvoidSml].find(current_source_AvoidLrg));
3786 assert(marked(AvoidLrg)==current_source_AvoidLrg.ref_state->counter ||
3787 marked_NewBotSt==current_source_AvoidLrg.ref_state->counter);
3788 assert(has_small_splitter || has_large_splitter);
3789 linked_list<BLC_indicators>::const_iterator
const current_splitter=
3791 *current_outgoing_iter_AvoidLrg->ref.BLC_transitions].
3792 transitions_per_block_to_constellation; assert(bi->block.to_constellation.end()!=large_splitter);
3793 if (current_splitter==large_splitter)
3798 if (marked_NewBotSt!=current_source_AvoidLrg.ref_state->counter)
3808 current_source_AvoidLrg.ref_state->counter=marked_NewBotSt;
3813 else if (current_outgoing_iter_AvoidLrg=
3814 current_outgoing_iter_AvoidLrg->start_same_saC,
3815 current_outgoing_iter_start_AvoidLrg==
3816 current_outgoing_iter_AvoidLrg
3829 { assert(marked(AvoidLrg)==current_source_AvoidLrg.ref_state->counter);
3832 { assert(running_searches[current_search_index]==AvoidLrg);
3833 --no_of_running_searches; assert(current_search_index<=no_of_running_searches);
3834 running_searches[current_search_index]=
3835 running_searches[no_of_running_searches]; assert(std::find(potential_non_bottom_states[AvoidLrg].begin(),
3836 potential_non_bottom_states[AvoidLrg].end(), current_source_AvoidLrg)!=
3837 potential_non_bottom_states[AvoidLrg].end());
3838 --current_search_index;
3842 non_bottom_states[AvoidLrg].add_todo(current_source_AvoidLrg);
3851 if (current_source_iter[AvoidLrg]!=
3852 current_source_iter_end[AvoidLrg] &&
3853 m_aut.is_tau(m_aut_apply_hidden_label_map
3854 (current_source_iter[AvoidLrg]->label())))
3856 status[AvoidLrg]=incoming_inert_transition_checking;
3859 status[AvoidLrg]=state_checking;
3862 assert(state_checking==status[current_search]);
3863 assert(NewBotSt!=current_search);
3865 if (current_bottom_state_iter[current_search]==
3866 start_bottom_states[current_search+1] &&
3867 non_bottom_states[current_search].todo_is_empty())
3871 status[current_search]=finished;
3872 ++no_of_finished_searches;
3873 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3880 check_complexity::check_temporary_work();
3882 const unsigned char max_new_B=check_complexity::log_n-
3884 for (
const state_in_block_pointer* s=start_bottom_states[current_search];
3885 (s!=start_bottom_states[current_search+1] ||
3886 (s=non_bottom_states[current_search].data(),
true)) &&
3887 s!=non_bottom_states[current_search].data_end(); ++s)
3890 simple_splitB_U_find_predecessors, check_complexity::
3891 simple_splitB_find_predecessors_of_R_or_U_state, max_new_B), *
this);
3893 const std::vector<transition>::const_iterator in_ti_end=
3894 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
3895 : std::next(s->ref_state)->start_incoming_transitions;
3896 for (std::vector<transition>::const_iterator
3897 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
3899 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
3901 cbegin(), ti)], finalise_work(check_complexity::
3902 simple_splitB_U_handle_transition_to_U_state, check_complexity::
3903 simple_splitB_handle_transition_to_R_or_U_state, max_new_B), *
this);
3905 if (has_large_splitter && AvoidLrg==current_search &&
3906 0!=s->ref_state->no_of_outgoing_block_inert_transitions)
3909 const outgoing_transitions_const_it out_ti_end=
3910 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
3911 : std::next(s->ref_state)->start_outgoing_transitions;
3912 for (outgoing_transitions_const_it
3913 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
3915 assert(has_small_splitter || has_large_splitter);
3917 finalise_work(check_complexity::
3918 simple_splitB_U_handle_transition_from_potential_U_state,
3920 simple_splitB_handle_transition_from_R_or_U_state,
3923 }
else { assert(AvoidLrg!=current_search ||
3924 0==s->ref_state->no_of_outgoing_block_inert_transitions); }
3926 if (has_large_splitter && AvoidLrg==current_search)
3934 for (
const state_in_block_pointer*
3935 s=bi->sta.rt_non_bottom_states; s!=bi->end_states; ++s)
3938 const outgoing_transitions_const_it out_ti_end=
3939 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
3940 : std::next(s->ref_state)->start_outgoing_transitions;
3941 for (outgoing_transitions_const_it
3942 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
3944 assert(has_small_splitter || has_large_splitter);
3945 mCRL2complexity(&m_transitions[*ti->ref.BLC_transitions], finalise_work
3947 simple_splitB_U_handle_transition_from_potential_U_state,
3949 simple_splitB_test_outgoing_transitions_found_new_bottom_state,
3958 }
else { assert(AvoidLrg!=current_search); }
3961 if (3>no_of_finished_searches)
3964 assert(finished!=status_NewBotSt);
3976 +potential_non_bottom_states[current_search].size()
3977 -non_bottom_states[current_search].size());
3979 for (
const state_in_block_pointer& st:
3980 potential_non_bottom_states[current_search])
3984 if (marked_NewBotSt!=st.ref_state->counter)
3985 { assert(is_in_marked_range_of(st.ref_state->counter, current_search));
3986 if (marked(current_search)!=st.ref_state->counter)
3988 assert(!non_bottom_states[ReachAlw].find(st));
3997 st.ref_state->counter=marked_NewBotSt; assert(!non_bottom_states[AvoidSml].find(st));
3998 }
else { assert(non_bottom_states[current_search].find(st)); }
3999 }
else { assert(!non_bottom_states[current_search].find(st)); }
4000 } assert(running_searches[current_search_index]==current_search);
4001 clear(potential_non_bottom_states[current_search]);
4002 --no_of_running_searches; assert(current_search_index<=no_of_running_searches);
4003 running_searches[current_search_index]=
4004 running_searches[no_of_running_searches];
4005 --current_search_index; assert((has_small_splitter && has_large_splitter) ||
4006 potential_non_bottom_states_HitSmall.empty());
4007 if (has_small_splitter && has_large_splitter &&
4008 finished==status[ReachAlw] && finished==status[AvoidLrg] &&
4009 aborted!=status_NewBotSt)
4010 { assert(1>=no_of_running_searches);
4012 assert(finished!=status[AvoidSml]);
4013 assert(finished!=status_NewBotSt);
4014 for (
const state_in_block_pointer& st:
4015 potential_non_bottom_states_HitSmall)
4016 { assert(0<st.ref_state->no_of_outgoing_block_inert_transitions);
4020 assert(!non_bottom_states[AvoidSml].find(st));
4021 if (marked_HitSmall==st.ref_state->counter)
4024 st.ref_state->counter=marked_NewBotSt; assert(!non_bottom_states[AvoidLrg].find(st));
4025 }
else { assert(marked(ReachAlw)==st.ref_state->counter ||
4026 marked(AvoidLrg)==st.ref_state->counter ||
4027 marked_NewBotSt==st.ref_state->counter); }
4029 clear(potential_non_bottom_states_HitSmall);
4030 }
else { assert(finished!=status[ReachAlw] || finished!=status[AvoidLrg] ||
4031 aborted==status_NewBotSt ||
4032 potential_non_bottom_states_HitSmall.empty()); }
4033 if (std::numeric_limits<state_index>::max()!=
4034 no_of_unfinished_states_in_block)
4035 { assert(0<no_of_running_searches); assert(no_of_running_searches<=2);
4036 assert(aborted!=status[ReachAlw]); assert(aborted!=status[AvoidLrg]);
4037 no_of_unfinished_states_in_block-=
4039 assert(finished!=status[running_searches[0]]);
4040 assert(aborted!=status[AvoidSml]); assert(aborted!=status_NewBotSt);
4049 running_searches[0]=running_searches[1];
4050 if (0==current_search_index)
4052 --current_search_index;
4054 --no_of_running_searches;
4056 else if (1<no_of_running_searches && ( assert(aborted!=status[running_searches[1]]),
4057 assert(finished!=status[running_searches[1]]),
4064 --no_of_running_searches; assert(1==no_of_running_searches);
4067 { assert(aborted!=status_NewBotSt);
4075 assert(finished==status[AvoidSml]); assert(finished==status[AvoidLrg]);
4076 assert(finished==status[ReachAlw]);
4080 start_bottom_states[ReachAlw+1]+
4081 non_bottom_states[ReachAlw].size();
4086 non_bottom_states[AvoidSml].size();
4090 non_bottom_states[AvoidLrg].size();
4091 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4095 check_complexity::check_waiting_cycles();
4098 if (has_large_splitter) {
4101 for (
const state_in_block_pointer*
4102 s=bi->start_bottom_states; s!=bi->sta.rt_non_bottom_states; ++s)
4105 const outgoing_transitions_it out_ti_end=
4106 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
4107 : std::next(s->ref_state)->start_outgoing_transitions;
4108 for (outgoing_transitions_it
4109 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4111 assert(has_small_splitter || has_large_splitter);
4113 cancel_work(check_complexity::
4114 simple_splitB_R_handle_transition_from_R_state), *
this);
4118 for (
const state_in_block_pointer*
4119 s=bi->sta.rt_non_bottom_states; s!=bi->end_states; ++s)
4122 (check_complexity::simple_splitB_R_find_predecessors), *
this);
4124 const std::vector<transition>::iterator in_ti_end=
4125 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
4126 : std::next(s->ref_state)->start_incoming_transitions;
4127 for (std::vector<transition>::iterator
4128 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
4130 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
4132 get_transitions().begin(), ti)], cancel_work(check_complexity::
4133 simple_splitB_R_handle_transition_to_R_state), *
this);
4135 if (has_large_splitter) {
4137 const outgoing_transitions_it out_ti_end=
4138 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
4139 : std::next(s->ref_state)->start_outgoing_transitions;
4140 for (outgoing_transitions_it
4141 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4143 assert(has_small_splitter || has_large_splitter);
4145 cancel_work(check_complexity::
4146 simple_splitB_R_handle_transition_from_R_state), *
this);
4151 check_complexity::check_temporary_work();
4158 enum subblocks max_process=AvoidLrg;
4160 if (!has_large_splitter ||
4161 (has_small_splitter &&
4165 max_process=AvoidSml;
4170 max_process=ReachAlw;
4172 status_NewBotSt=finished;
4173 status[max_process]=aborted;
4175 clear(potential_non_bottom_states[current_search]); assert(potential_non_bottom_states[max_process].empty());
4176 non_bottom_states[max_process].swap_vec
4177 (potential_non_bottom_states[max_process]);
4179 for (
const state_in_block_pointer& st: potential_non_bottom_states_HitSmall)
4181 assert(has_small_splitter); assert(has_large_splitter);
4182 assert(marked(ReachAlw) == st.ref_state->counter ||
4183 marked(AvoidLrg) == st.ref_state->counter);
4186 if (has_small_splitter && has_large_splitter)
4188 clear(potential_non_bottom_states_HitSmall);
4190 goto end_for_empty_NewBotSt_subblock;
4193 constellation_type*
const constellation=bi->c.onstellation;
4194 if (constellation->start_const_states->ref_state->block==
4195 std::prev(constellation->end_const_states)->ref_state->block)
4196 { assert(std::find(m_non_trivial_constellations.begin(),
4197 m_non_trivial_constellations.end(),
4198 constellation)==m_non_trivial_constellations.end());
4199 m_non_trivial_constellations.emplace_back(constellation);
4204 block_type*
const NewBotSt_block_index=bi;
4210 clear_state_counters
4211 (potential_non_bottom_states[current_search].begin(),
4212 potential_non_bottom_states[current_search].end(), bi);
4213 clear(potential_non_bottom_states[current_search]); assert(potential_non_bottom_states[ReachAlw].empty());
4214 assert(potential_non_bottom_states[AvoidLrg].empty());
4215 assert(potential_non_bottom_states[AvoidSml].empty());
4221 clear_state_counters
4222 (potential_non_bottom_states_HitSmall.begin(),
4223 potential_non_bottom_states_HitSmall.end(), bi);
4224 clear(potential_non_bottom_states_HitSmall); assert(has_large_splitter ||
4226 static_assert(2==AvoidLrg); assert(finished==status[AvoidLrg]);
4227 if (has_large_splitter &&
4231 move_nonbottom_states_to(non_bottom_states[AvoidLrg],
4233 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4237 if (start_bottom_states[AvoidLrg]!=
4240 multiple_swap_states_in_states_in_block
4241 (start_bottom_states[AvoidLrg],
4243 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4244 , start_bottom_states[AvoidLrg],
4245 check_complexity::log_n-
4250 non_bottom_states[AvoidLrg].clear();
4251 create_new_block<!has_small_splitter && !has_large_splitter>
4255 old_constellation, new_constellation);
4256 check_incoming_tau_transitions_become_noninert
4257 (NewBotSt_block_index,
4263 assert(0==
bottom_size(AvoidLrg));assert(non_bottom_states[AvoidLrg].empty());
4265 static_assert(1==AvoidSml); assert(finished==status[AvoidSml]);
4266 if (!has_large_splitter ||
4267 (has_small_splitter &&
4272 move_nonbottom_states_to(non_bottom_states[AvoidSml],
4274 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4278 if (start_bottom_states[AvoidSml]!=
4281 multiple_swap_states_in_states_in_block
4282 (start_bottom_states[AvoidSml],
4284 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4285 , start_bottom_states[AvoidSml],
4286 check_complexity::log_n-
4291 non_bottom_states[AvoidSml].clear();
4292 create_new_block<!has_small_splitter && !has_large_splitter>
4296 old_constellation, new_constellation);
4297 check_incoming_tau_transitions_become_noninert
4298 (NewBotSt_block_index,
4304 assert(0==
bottom_size(AvoidSml));assert(non_bottom_states[AvoidSml].empty());
4307 static_assert(0==ReachAlw); assert(finished==status[ReachAlw]);
4308 block_type* ReachAlw_block_index=null_block;
4309 if (start_bottom_states[ReachAlw]!=
4312 move_nonbottom_states_to(non_bottom_states[ReachAlw],
4313 start_bottom_states[ReachAlw+1]
4314 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4318 non_bottom_states[ReachAlw].clear();
4319 ReachAlw_block_index=create_new_block
4320 <!has_small_splitter && !has_large_splitter>
4321 (start_bottom_states[ReachAlw],
4322 start_bottom_states[ReachAlw+1],
4324 old_constellation, new_constellation);
4325 check_incoming_tau_transitions_become_noninert
4326 (NewBotSt_block_index,
4327 start_bottom_states[ReachAlw],
4330 assert(0==
bottom_size(ReachAlw));assert(non_bottom_states[ReachAlw].empty());
4332 NewBotSt_block_index->contains_new_bottom_states=
true; assert(NewBotSt_block_index->start_bottom_states<
4333 NewBotSt_block_index->sta.rt_non_bottom_states);
4334 m_blocks_with_new_bottom_states.push_back(NewBotSt_block_index);
4336 return ReachAlw_block_index;
4342 if (incoming_inert_transition_checking==status_NewBotSt)
4343 { assert(current_source_iter_NewBotSt<current_source_iter_end_NewBotSt);
4344 mCRL2complexity(&m_transitions[std::distance(m_aut.get_transitions().begin(),
4345 current_source_iter_NewBotSt)], add_work(check_complexity::
4346 simple_splitB_R_handle_transition_to_R_state, 1), *
this);
4347 const transition& tr=*current_source_iter_NewBotSt++; assert(m_aut.is_tau(m_aut_apply_hidden_label_map(tr.label())));
4348 state_in_block_pointer
const src=m_states.begin()+
static_cast<std::ptrdiff_t>(tr.from()); assert(m_states[tr.to()].block==bi);
4350 if (src.ref_state->block==bi &&
4351 !(m_preserve_divergence && tr.from()==tr.to()))
4354 if (marked_NewBotSt!=src.ref_state->counter)
4356 assert(aborted!=status_NewBotSt);
4366 src.ref_state->counter=marked_NewBotSt;
4370 if (current_source_iter_NewBotSt==current_source_iter_end_NewBotSt ||
4371 !m_aut.is_tau(m_aut_apply_hidden_label_map
4372 (current_source_iter_NewBotSt->label())))
4374 status_NewBotSt=state_checking;
4377 else if (state_checking==status_NewBotSt)
4382 state_in_block_pointer
4385 add_work(check_complexity::simple_splitB_R_find_predecessors, 1), *
this);
4386 current_source_iter_NewBotSt=
4387 tgt.ref_state->start_incoming_transitions;
4388 current_source_iter_end_NewBotSt=
4389 std::next(tgt.ref_state)>=m_states.end()
4390 ? m_aut.get_transitions().end()
4391 : std::next(tgt.ref_state)->start_incoming_transitions;
4392 if(current_source_iter_NewBotSt<current_source_iter_end_NewBotSt &&
4393 m_aut.is_tau(m_aut_apply_hidden_label_map
4394 (current_source_iter_NewBotSt->label())))
4396 status_NewBotSt=incoming_inert_transition_checking;
4401 if (1>=no_of_finished_searches)
4403 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4404 check_complexity::wait();
4411 if (has_large_splitter && finished!=status[AvoidLrg] &&
4412 large_splitter_iter_NewBotSt!=large_splitter_iter_end_NewBotSt)
4413 { assert(finished==status[ReachAlw]); assert(finished==status[AvoidSml]);
4420 t=m_aut.get_transitions()[*large_splitter_iter_NewBotSt];
mCRL2complexity(&m_transitions[*large_splitter_iter_NewBotSt],
4421 add_work(check_complexity::
4422 simple_splitB_R_handle_transition_from_R_state, 1), *
this);
4423 ++large_splitter_iter_NewBotSt;
4424 state_in_block_pointer src=m_states.begin()+t.from(); assert(src.ref_state->block==bi);
4426 if (0==src.ref_state->no_of_outgoing_block_inert_transitions)
4427 { assert(!(start_bottom_states[AvoidLrg]<=src.ref_state->ref_states_in_blocks &&
4428 src.ref_state->ref_states_in_blocks<start_bottom_states[AvoidLrg+1]));
4433 if ((undefined==src.ref_state->counter) ||
4434 is_in_marked_range_of(src.ref_state->counter, AvoidLrg))
4435 { assert(!non_bottom_states[ReachAlw].find(src));
4436 assert(!non_bottom_states[AvoidSml].find(src));
4437 assert(!non_bottom_states[AvoidLrg].find(src));
4440 src.ref_state->counter=marked_NewBotSt;
4442 if (0==no_of_running_searches)
4453 assert(aborted!=status_NewBotSt);
4456 }
else { assert(marked_HitSmall!=src.ref_state->counter); }
4458 if (0!=no_of_running_searches)
4463 while ( assert(0==no_of_running_searches), assert(aborted==status[AvoidLrg]),
4464 large_splitter_iter_NewBotSt!=large_splitter_iter_end_NewBotSt);
4467 { assert(finished==status[AvoidLrg] ||
4468 large_splitter_iter_NewBotSt==large_splitter_iter_end_NewBotSt);
4471 check_complexity::check_waiting_cycles();
4493 status_NewBotSt=finished; ++no_of_finished_searches; assert(3==no_of_finished_searches);
4501 if (!has_large_splitter || finished==status[AvoidLrg])
4502 { assert(finished==status[AvoidLrg]);
4505 non_bottom_states[AvoidLrg].size();
4508 if ((!has_small_splitter && has_large_splitter) ||
4509 finished==status[AvoidSml])
4510 { assert(finished==status[AvoidSml]); assert(finished!=status[ReachAlw]);
4513 non_bottom_states[AvoidSml].size();
4517 non_bottom_states[ReachAlw].clear();
4518 clear_state_counters
4519 (potential_non_bottom_states[ReachAlw].begin(),
4520 potential_non_bottom_states[ReachAlw].end(), bi);
4521 clear(potential_non_bottom_states[ReachAlw]);
4524 if (has_small_splitter && has_large_splitter)
4526 clear_state_counters
4527 (potential_non_bottom_states_HitSmall.begin(),
4528 potential_non_bottom_states_HitSmall.end(), bi);
4529 }
else { assert(potential_non_bottom_states_HitSmall.empty()); }
4532 { assert(finished==status[ReachAlw]);
4534 start_bottom_states[ReachAlw+1]+
4535 non_bottom_states[ReachAlw].size();
4539 non_bottom_states[AvoidSml].clear();
4540 clear_state_counters
4541 (potential_non_bottom_states[AvoidSml].begin(),
4542 potential_non_bottom_states[AvoidSml].end(), bi);
4543 clear(potential_non_bottom_states[AvoidSml]);
4549 { assert(finished==status[ReachAlw]);
4551 start_bottom_states[ReachAlw+1]+
4552 non_bottom_states[ReachAlw].size(); assert(finished==status[AvoidSml]);
4557 non_bottom_states[AvoidSml].size();
4561 non_bottom_states[AvoidLrg].clear();
4562 clear_state_counters
4563 (potential_non_bottom_states[AvoidLrg].begin(),
4564 potential_non_bottom_states[AvoidLrg].end(), bi);
4565 clear(potential_non_bottom_states[AvoidLrg]);
4566 if (has_small_splitter)
4569 clear_state_counters
4570 (potential_non_bottom_states_HitSmall.begin(),
4571 potential_non_bottom_states_HitSmall.end(), bi);
4572 }
else { assert(potential_non_bottom_states_HitSmall.empty()); }
4574 if (has_small_splitter && has_large_splitter)
4576 clear(potential_non_bottom_states_HitSmall);
4577 }
else { assert(potential_non_bottom_states_HitSmall.empty()); }
4578 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4587 state_type max_NcludeCo_size=std::distance(
4589 max_NcludeCo_size=std::max<state_type>(max_NcludeCo_size, std::distance(
4591 max_NcludeCo_size=std::max<state_type>(max_NcludeCo_size, std::distance(
4593 const unsigned char max_NcludeCo_B=
4594 check_complexity::log_n-check_complexity::ilog2(max_NcludeCo_size);
4595 const state_in_block_pointer* s=bi->start_bottom_states;
4598 (check_complexity::simple_splitB_U_find_predecessors), *
this);
4600 const std::vector<transition>::const_iterator in_ti_end=
4601 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
4602 : std::next(s->ref_state)->start_incoming_transitions;
4603 for (std::vector<transition>::const_iterator
4604 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
4606 if(!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
4608 cbegin(), ti)], cancel_work(check_complexity::
4609 simple_splitB_U_handle_transition_to_U_state), *
this);
4611 if (has_large_splitter && finished!=status[AvoidLrg]) {
4613 const outgoing_transitions_const_it out_ti_end=
4614 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
4615 : std::next(s->ref_state)->start_outgoing_transitions;
4616 for (outgoing_transitions_const_it
4617 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4619 assert(has_small_splitter || has_large_splitter);
4621 cancel_work(check_complexity::
4622 simple_splitB_U_handle_transition_from_potential_U_state), *
this);
4626 finalise_work(check_complexity::
4627 simple_splitB_R_handle_transition_from_R_state,
4629 simple_splitB_handle_transition_from_R_or_U_state,
4630 max_NcludeCo_B), *
this);
4632 }
else { assert(finished==status[AvoidLrg]); }
4633 }
while (++s!=bi->end_states);
4646 constellation_type*
const constellation=bi->c.onstellation;
4647 if (constellation->start_const_states->ref_state->block==
4648 std::prev(constellation->end_const_states)->ref_state->block)
4649 { assert(std::find(m_non_trivial_constellations.begin(),
4650 m_non_trivial_constellations.end(),
4651 constellation)==m_non_trivial_constellations.end());
4652 m_non_trivial_constellations.emplace_back(constellation);
4657 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4662 block_type*
const NewBotSt_block_index=
4663 create_new_block<!has_small_splitter && !has_large_splitter>
4667 null_constellation, null_constellation);
4668 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4672 const unsigned char max_new_B=check_complexity::log_n-check_complexity::ilog2
4677 simple_splitB_R_find_predecessors, check_complexity::
4678 simple_splitB_find_predecessors_of_R_or_U_state, max_new_B), *
this);
4680 const std::vector<transition>::iterator in_ti_end=
4681 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
4682 : std::next(s->ref_state)->start_incoming_transitions;
4683 for (std::vector<transition>::iterator
4684 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
4686 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
4688 begin(), ti)], finalise_work(check_complexity::
4689 simple_splitB_R_handle_transition_to_R_state, check_complexity::
4690 simple_splitB_handle_transition_to_R_or_U_state, max_new_B), *
this);
4694 }
while (s!=bi->end_states);
4696 check_complexity::check_temporary_work();
4702 outgoing_transitions_const_it
const out_it_end=
4703 std::next(nst_it->ref_state)>=m_states.end()
4704 ? m_outgoing_transitions.end()
4705 : std::next(nst_it->ref_state)->start_outgoing_transitions;
4706 outgoing_transitions_it out_it=nst_it->ref_state->
4707 start_outgoing_transitions; assert(out_it!=out_it_end);
4708 const transition* tr=&m_aut.get_transitions()
4709 [has_small_splitter || has_large_splitter
4710 ?*out_it->ref.BLC_transitions :out_it->ref.transitions]; assert(0<nst_it->ref_state->no_of_outgoing_block_inert_transitions);
4712 { assert(m_states.begin()+tr->from()==nst_it->ref_state);
4713 assert(m_aut.is_tau(m_aut_apply_hidden_label_map(tr->label())));
4714 if (m_states[tr->to()].block==bi)
4715 { assert(is_inert_during_init(*tr));
4716 assert(bi->start_bottom_states<=m_states[tr->to()].ref_states_in_blocks);
4719 assert(0<nst_it->ref_state->no_of_outgoing_block_inert_transitions);
4720 if (0== --nst_it->ref_state->
4721 no_of_outgoing_block_inert_transitions)
4724 change_non_bottom_state_to_bottom_state
4725 (nst_it->ref_state);
4730 m_states[tr->to()].ref_states_in_blocks ||
4731 m_states[tr->to()].ref_states_in_blocks<start_bottom_states[ReachAlw]);
4735 while (out_it!=out_it_end &&
4736 (tr=&m_aut.get_transitions()
4737 [has_small_splitter || has_large_splitter
4738 ?*out_it->ref.BLC_transitions :out_it->ref.transitions],
4739 m_aut.is_tau(m_aut_apply_hidden_label_map(tr->label()))));
4742 while (nst_it!=bi->end_states); assert(NewBotSt_block_index->start_bottom_states<
4743 NewBotSt_block_index->sta.rt_non_bottom_states);
4744 NewBotSt_block_index->contains_new_bottom_states=
true;
4745 m_blocks_with_new_bottom_states.push_back(NewBotSt_block_index);
4751 check_complexity::check_temporary_work();
4754 constellation_type*
const constellation=bi->c.onstellation;
4755 if (constellation->start_const_states->ref_state->block==
4756 std::prev(constellation->end_const_states)->ref_state->block)
4757 { assert(std::find(m_non_trivial_constellations.begin(),
4758 m_non_trivial_constellations.end(),
4759 constellation)==m_non_trivial_constellations.end());
4760 m_non_trivial_constellations.emplace_back(constellation); assert((start_bottom_states[ReachAlw]!=
new_start_bottom_states(ReachAlw+1))+
4766 } assert(finished!=status[AvoidLrg] ||
static_cast<state_index>(std::distance
4772 if (start_bottom_states[AvoidLrg]!=
4775 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4776 const state_in_block_pointer* acct_iter;
4777 state_index acct_B_size;
4778 if (finished==status[AvoidLrg]) {
4779 acct_iter=start_bottom_states[AvoidLrg];
4784 assert(non_bottom_states[AvoidLrg].empty());
4785 assert(finished==status[ReachAlw]); assert(finished==status[AvoidSml]);
4786 state_type count=std::min<state_type>(
bottom_size(AvoidLrg),
4787 std::distance(start_bottom_states[AvoidLrg],
4789 if (non_bottom_states[AvoidSml].size()>=count) {
4790 acct_iter=non_bottom_states[AvoidSml].data();
4792 }
else if (non_bottom_states[ReachAlw].size()>=count) {
4793 acct_iter=non_bottom_states[ReachAlw].data();
4796 assert(count<=non_bottom_states[AvoidSml].size()+
4797 non_bottom_states[ReachAlw].size());
4800 non_bottom_states[AvoidLrg]=non_bottom_states[AvoidSml];
4801 non_bottom_states[AvoidLrg].add_todo(non_bottom_states[ReachAlw].begin(),
4802 non_bottom_states[ReachAlw].begin()
4803 +
static_cast<std::ptrdiff_t>(count-non_bottom_states[AvoidLrg].size()));
4804 acct_iter=non_bottom_states[AvoidLrg].data();
4810 multiple_swap_states_in_states_in_block
4811 (start_bottom_states[AvoidLrg],
4813 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4814 , acct_iter, check_complexity::log_n-check_complexity::ilog2(acct_B_size),
4815 finished==status[AvoidLrg]
4816 ?check_complexity::multiple_swap_states_in_block_swap_state_in_small_block
4818 multiple_swap_states_in_block_account_for_swap_in_aborted_block
4823 if (finished==status[AvoidLrg])
4824 { assert(potential_non_bottom_states[AvoidLrg].empty());
4825 move_nonbottom_states_to(non_bottom_states[AvoidLrg],
4827 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4831 non_bottom_states[AvoidLrg].clear();
4832 create_new_block<!has_small_splitter && !has_large_splitter>
4836 old_constellation, new_constellation);
4840 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4843 non_bottom_states[AvoidLrg].clear();
4846 bi->sta.rt_non_bottom_states=
new_end_bottom_states(AvoidLrg); assert(bi->start_bottom_states<bi->sta.rt_non_bottom_states);
4852 assert(0==
bottom_size(AvoidLrg));assert(non_bottom_states[AvoidLrg].empty());
4853 assert(finished==status[AvoidLrg]);
4855 assert(finished!=status[AvoidSml] ||
static_cast<state_index>(std::distance
4858 if ((has_small_splitter || !has_large_splitter) &&
4865 if (start_bottom_states[AvoidSml]!=
4868 multiple_swap_states_in_states_in_block
4869 (start_bottom_states[AvoidSml],
4871 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4872 , finished==status[AvoidSml] ? start_bottom_states[AvoidSml]
4873 : non_bottom_states[ReachAlw].data(),
4874 check_complexity::log_n-check_complexity::ilog2
4877 finished==status[AvoidSml]
4878 ?check_complexity::multiple_swap_states_in_block_swap_state_in_small_block
4880 multiple_swap_states_in_block_account_for_swap_in_aborted_block
4884 if (finished==status[AvoidSml])
4885 { assert(potential_non_bottom_states[AvoidSml].empty());
4886 move_nonbottom_states_to(non_bottom_states[AvoidSml],
4888 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4892 non_bottom_states[AvoidSml].clear();
4893 create_new_block<!has_small_splitter && !has_large_splitter>
4897 old_constellation, new_constellation);
4902 bi->sta.rt_non_bottom_states=
new_end_bottom_states(AvoidSml); assert(bi->start_bottom_states<bi->sta.rt_non_bottom_states);
4908 assert(0==
bottom_size(AvoidSml));assert(non_bottom_states[AvoidSml].empty());
4909 assert(finished==status[AvoidSml]);
4911 assert(finished!=status[ReachAlw] ||
static_cast<state_index>(std::distance
4914 block_type* ReachAlw_block_index=null_block;
4915 if (start_bottom_states[ReachAlw]!=
4918 if (finished==status[ReachAlw])
4919 { assert(potential_non_bottom_states[ReachAlw].empty());
4920 move_nonbottom_states_to(non_bottom_states[ReachAlw],
4921 start_bottom_states[ReachAlw+1]
4922 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4926 non_bottom_states[ReachAlw].clear();
4927 ReachAlw_block_index=create_new_block
4928 <!has_small_splitter && !has_large_splitter>
4929 (start_bottom_states[ReachAlw],
4930 start_bottom_states[ReachAlw+1],
4932 old_constellation, new_constellation);
4935 { assert(bi->start_bottom_states==start_bottom_states[ReachAlw]);
4936 bi->sta.rt_non_bottom_states=start_bottom_states[ReachAlw+1]; assert(bi->start_bottom_states<bi->sta.rt_non_bottom_states);
4938 ReachAlw_block_index=bi;
4941 assert(0==
bottom_size(ReachAlw));assert(non_bottom_states[ReachAlw].empty());
4943 return ReachAlw_block_index;
4946 assert(aborted==status_NewBotSt);
4948 #undef new_start_bottom_states
4949 #undef new_end_bottom_states
4950 #undef new_end_bottom_states_NewBotSt
4954 #undef abort_if_bottom_size_too_large
4955 #undef abort_if_non_bottom_size_too_large_NewBotSt
4956 #undef abort_if_size_too_large
4957 #undef bottom_and_non_bottom_size
4961 transition_index accumulate_entries(
4962 std::vector<transition_index>& action_counter,
4963 const std::vector<label_index>& todo_stack)
const
4965 transition_index sum=0;
4966 for(label_index index: todo_stack)
4968 transition_index n=sum;
4969 sum=sum+action_counter[index];
4970 action_counter[index]=n;
4980 void order_BLC_transitions_single_BLC_set(
4981 state_in_block_pointer*
const pos,
4982 BLC_list_iterator start_same_BLC,
4983 BLC_list_iterator end_same_BLC)
4984 { assert(start_same_BLC<end_same_BLC);
4985 block_type*
const bi=pos->ref_state->block; assert(pos==bi->start_bottom_states);
4987 block.to_constellation.emplace_back(start_same_BLC,end_same_BLC,
true);
4988 if (!is_inert_during_init(m_aut.get_transitions()[*start_same_BLC]))
4990 ++no_of_non_constellation_inert_BLC_sets;
4993 { assert(bi==m_states[m_aut.get_transitions()[*start_same_BLC].from()].block);
4994 m_transitions[*start_same_BLC].transitions_per_block_to_constellation=
4995 blc;
mCRL2complexity(&m_transitions[*start_same_BLC], add_work(check_complexity::
4996 order_BLC_transitions_sort_transition, check_complexity::log_n), *
this);
4997 m_transitions[*start_same_BLC].ref_outgoing_transitions->
4998 ref.convert_to_iterator(start_same_BLC);
5000 while (++start_same_BLC<end_same_BLC);
5020 void order_BLC_transitions(BLC_list_iterator start_same_BLC,
5021 BLC_list_iterator end_same_BLC,
5022 state_in_block_pointer* min_block,
5023 state_in_block_pointer* max_block)
5024 { assert(start_same_BLC<end_same_BLC);
5025 assert(min_block->ref_state->block->start_bottom_states==min_block);
5026 assert(max_block->ref_state->block->start_bottom_states==max_block);
5027 if (min_block==max_block)
5029 order_BLC_transitions_single_BLC_set(min_block,
5030 start_same_BLC, end_same_BLC);
5032 }
else { assert(min_block<max_block); }
5033 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5034 const unsigned char max_sort=check_complexity::log_n-
5035 check_complexity::ilog2(max_block-min_block+1);
5037 state_in_block_pointer* pivot=min_block+(max_block-min_block+1)/2;
5038 pivot=pivot->ref_state->block->start_bottom_states;
5039 state_in_block_pointer* min_below_pivot=pivot;
5040 state_in_block_pointer* max_above_pivot=pivot;
5041 #define max_below_pivot min_block
5042 #define min_above_pivot max_block
5047 BLC_list_iterator end_equal_to_pivot=start_same_BLC;
5048 BLC_list_iterator end_smaller_than_pivot=start_same_BLC;
5049 BLC_list_iterator begin_larger_than_pivot=end_same_BLC;
5053 { assert(end_smaller_than_pivot<begin_larger_than_pivot);
5055 {
const state_in_block_pointer* sb;
5056 BLC_list_const_iterator it=start_same_BLC;
5057 assert(it<=end_equal_to_pivot);
5058 for (; it<end_equal_to_pivot; ++it) {
5059 assert(m_states[m_aut.get_transitions()[*it].from()].block->
5060 start_bottom_states==pivot);
5062 assert(it<=end_smaller_than_pivot);
5063 for (; it<end_smaller_than_pivot; ++it) {
5065 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5066 start_bottom_states;
5069 assert(it<begin_larger_than_pivot);
5070 for (it=begin_larger_than_pivot; it<end_same_BLC; ++it) {
5072 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5073 start_bottom_states;
5079 check_complexity::order_BLC_transitions_sort_transition, max_sort), *
this);
5080 state_in_block_pointer*
const source_block=
5081 m_states[m_aut.get_transitions()
5082 [*end_smaller_than_pivot].from()].block->start_bottom_states;
5083 if (source_block==pivot)
5085 std::swap(*end_equal_to_pivot++, *end_smaller_than_pivot);
5087 else if (source_block>pivot)
5093 if (source_block>max_above_pivot)
5095 max_above_pivot=source_block;
5101 if (source_block<min_below_pivot)
5103 min_below_pivot=source_block;
5110 ++end_smaller_than_pivot;
5111 if (end_smaller_than_pivot>=begin_larger_than_pivot)
5113 goto break_two_loops;
5119 { assert(end_smaller_than_pivot<begin_larger_than_pivot);
5121 {
const state_in_block_pointer* sb;
5122 BLC_list_const_iterator it=start_same_BLC;
5123 assert(it<=end_equal_to_pivot);
5124 for (; it<end_equal_to_pivot; ++it) {
5125 assert(m_states[m_aut.get_transitions()[*it].from()].block->
5126 start_bottom_states==pivot);
5128 assert(it<=end_smaller_than_pivot);
5129 for (; it<end_smaller_than_pivot; ++it) {
5131 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5132 start_bottom_states;
5136 sb=m_states[m_aut.get_transitions()[*it].from()].
5137 block->start_bottom_states;
5139 for (it=begin_larger_than_pivot; it<end_same_BLC; ++it) {
5140 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5141 start_bottom_states;
5146 --begin_larger_than_pivot;
5147 if (end_smaller_than_pivot>=begin_larger_than_pivot)
5149 goto break_two_loops;
5151 check_complexity::order_BLC_transitions_sort_transition, max_sort), *
this);
5152 state_in_block_pointer*
const source_block=
5153 m_states[m_aut.get_transitions()
5154 [*begin_larger_than_pivot].from()].block->start_bottom_states;
5155 if (source_block==pivot)
5156 { assert(end_smaller_than_pivot<begin_larger_than_pivot);
5157 transition_index temp=*begin_larger_than_pivot; assert(end_equal_to_pivot<=end_smaller_than_pivot);
5158 *begin_larger_than_pivot=*end_smaller_than_pivot;
5159 *end_smaller_than_pivot=*end_equal_to_pivot;
5160 *end_equal_to_pivot=temp;
5161 ++end_equal_to_pivot;
5162 ++end_smaller_than_pivot;
5163 if (end_smaller_than_pivot>=begin_larger_than_pivot)
5165 goto break_two_loops;
5169 if (source_block<pivot)
5171 if (source_block<min_below_pivot)
5173 min_below_pivot=source_block;
5179 std::swap(*end_smaller_than_pivot, *begin_larger_than_pivot);
5180 ++end_smaller_than_pivot;
5181 if (end_smaller_than_pivot>=begin_larger_than_pivot)
5183 goto break_two_loops;
5191 else if (source_block>max_above_pivot)
5193 max_above_pivot=source_block;
5197 break_two_loops: ; assert(end_smaller_than_pivot==begin_larger_than_pivot);
5199 {
const state_in_block_pointer* sb;
5200 BLC_list_const_iterator it=start_same_BLC;
5201 assert(it<=end_equal_to_pivot);
5202 for (; it<end_equal_to_pivot; ++it) {
5203 assert(m_states[m_aut.get_transitions()[*it].from()].block->
5204 start_bottom_states==pivot);
5206 assert(it<=end_smaller_than_pivot);
5207 for (; it<end_smaller_than_pivot; ++it) {
5209 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5210 start_bottom_states;
5213 assert(it==begin_larger_than_pivot); assert(it<=end_same_BLC);
5214 for (; it<end_same_BLC; ++it) {
5216 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5217 start_bottom_states;
5222 if (start_same_BLC<end_equal_to_pivot)
5224 order_BLC_transitions_single_BLC_set(pivot,
5225 start_same_BLC, end_equal_to_pivot);
5230 if (begin_larger_than_pivot<end_same_BLC)
5233 begin_larger_than_pivot, end_same_BLC);
5235 if (end_equal_to_pivot<begin_larger_than_pivot)
5237 order_BLC_transitions(end_equal_to_pivot, begin_larger_than_pivot,
5244 if (end_equal_to_pivot<begin_larger_than_pivot)
5246 order_BLC_transitions_single_BLC_set(min_below_pivot,
5247 end_equal_to_pivot, begin_larger_than_pivot);
5249 if (begin_larger_than_pivot<end_same_BLC)
5251 order_BLC_transitions(begin_larger_than_pivot, end_same_BLC,
5255 } assert(end_equal_to_pivot<begin_larger_than_pivot);
5257 assert(begin_larger_than_pivot<end_same_BLC);
5259 order_BLC_transitions(end_equal_to_pivot, begin_larger_than_pivot,
5262 order_BLC_transitions(begin_larger_than_pivot, end_same_BLC,
5264 #undef max_below_pivot
5265 #undef min_above_pivot
5273 template <
bool initialization=
false>
5276 if (m_blocks_with_new_bottom_states.empty() ||
5277 (initialization && m_BLC_transitions.empty()))
5283 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> > Qhat;
5284 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5285 std::vector<std::pair<BLC_list_const_iterator, BLC_list_const_iterator> >
5286 initialize_qhat_work_to_assign_later;
5287 std::vector<std::pair<BLC_list_const_iterator, BLC_list_const_iterator> >
5288 stabilize_work_to_assign_later;
5290 assert(!m_blocks_with_new_bottom_states.empty());
5291 for(block_type*
const bi: m_blocks_with_new_bottom_states)
5292 { assert(bi->contains_new_bottom_states);
5293 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5297 const state_in_block_pointer* new_bott_it=bi->start_bottom_states;
5298 assert(new_bott_it < bi->sta.rt_non_bottom_states);
5302 add_work(check_complexity::stabilizeB_prepare_block, 1), *
this);
5304 while (++new_bott_it<bi->sta.rt_non_bottom_states);
5306 bi->contains_new_bottom_states=
false; assert(!bi->block.to_constellation.empty());
5307 if (1>=number_of_states_in_block(*bi))
5313 ind=bi->block.to_constellation.begin(); assert(ind->start_same_BLC<ind->end_same_BLC);
5314 const transition* first_t;
5315 if(!initialization ||
5316 (first_t=&m_aut.get_transitions()[*ind->start_same_BLC], assert(m_states[first_t->from()].block==bi),
5317 is_inert_during_init(*first_t) &&
5318 bi->c.onstellation==m_states[first_t->to()].block->c.onstellation))
5321 if (!initialization) { first_t=&m_aut.get_transitions()[*ind->start_same_BLC]; }
5322 assert(m_states[first_t->from()].block==bi);
5323 assert(is_inert_during_init(*first_t) &&
5324 bi->c.onstellation==m_states[first_t->to()].block->c.onstellation);
5325 assert(ind->is_stable());
5326 if constexpr (initialization)
5328 assert(m_BLC_transitions.data()==ind->start_same_BLC);
5329 assert(bi->block.to_constellation.end()==std::next(ind) ||
5330 ind->end_same_BLC==std::next(ind)->start_same_BLC);
5335 if (initialization && bi->block.to_constellation.end()!=ind)
5337 Qhat.emplace_back(ind->start_same_BLC, m_BLC_transitions.data_end());
5339 for (; bi->block.to_constellation.end()!=ind; ++ind)
5340 { assert(ind->is_stable());
5341 ind->start_marked_BLC=ind->end_same_BLC;
5343 assert(!ind->has_marked_transitions());
5344 assert(ind->start_same_BLC<ind->end_same_BLC);
5345 const transition& first_t = m_aut.get_transitions()[*ind->start_same_BLC];
5346 assert(m_states[first_t.from()].block == bi);
5347 assert(!is_inert_during_init(first_t) ||
5348 bi->c.onstellation!=m_states[first_t.to()].block->c.onstellation);
5350 if constexpr (!initialization)
5353 Qhat.emplace_back(ind->start_same_BLC, ind->end_same_BLC);
5355 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5358 bool work_assigned =
false;
5360 for (BLC_list_const_iterator work_it = ind->start_same_BLC;
5361 work_it<ind->end_same_BLC; ++work_it)
5364 if (0==m_states[m_aut.get_transitions()
5365 [*work_it].from()].no_of_outgoing_block_inert_transitions)
5371 check_complexity::stabilizeB_initialize_Qhat, 1), *
this);
5376 check_complexity::stabilizeB_initialize_Qhat, 1), *
this);
5377 work_assigned =
true;
5387 initialize_qhat_work_to_assign_later.emplace_back(ind->start_same_BLC,
5394 if constexpr (!initialization)
5397 state_in_block_pointer* si=bi->start_bottom_states; assert(si<bi->sta.rt_non_bottom_states);
5400 check_complexity::stabilizeB_distribute_states_over_Phat, 1), *
this);
5401 outgoing_transitions_it end_it=
5402 std::next(si->ref_state)>=m_states.end()
5403 ? m_outgoing_transitions.end()
5404 : std::next(si->ref_state)->start_outgoing_transitions; assert(si->ref_state->block==bi);
5405 for (outgoing_transitions_it ti=
5406 si->ref_state->start_outgoing_transitions; ti<end_it; ++ti)
5409 const transition& t=
5410 m_aut.get_transitions()[*ti->ref.BLC_transitions]; assert(m_states.begin()+t.from()==si->ref_state);
5411 if (!is_inert_during_init(t) ||
5412 bi->c.onstellation!=m_states[t.to()].block->c.onstellation)
5415 mark_BLC_transition(ti);
5417 assert(ti <= ti->start_same_saC);
5418 ti = ti->start_same_saC;
5422 while (si<bi->sta.rt_non_bottom_states);
5426 clear(m_blocks_with_new_bottom_states);
5428 bool small_splitter_used_up=
false;
5429 constellation_type* new_constellation=null_constellation;
5432 if (initialization) { new_constellation=m_states[0].block->c.onstellation; }
5448 { assert(check_data_structures(
"End of stabilizeB()"));
5449 assert(check_stability(
"End of stabilizeB()"));
5452 assert(initialize_qhat_work_to_assign_later.empty());
5453 assert(stabilize_work_to_assign_later.empty());
5458 assert(check_data_structures(
"New bottom state loop",
false,
false));
5459 std::pair<BLC_list_iterator,BLC_list_iterator>& Qhat_elt=Qhat.back(); assert(check_stability(
"New bottom state loop", &Qhat));
5460 assert(Qhat_elt.first<Qhat_elt.second);
5461 const linked_list<BLC_indicators>::iterator splitter=
5462 m_transitions[*std::prev(Qhat_elt.second)].
5463 transitions_per_block_to_constellation; assert(splitter->end_same_BLC==Qhat_elt.second);
5465 Qhat_elt.second=splitter->start_same_BLC; assert(splitter->start_same_BLC<splitter->end_same_BLC);
5466 const transition& first_t=
5467 m_aut.get_transitions()[*splitter->start_same_BLC];
5468 block_type*
const from_block_index=m_states[first_t.from()].block; assert(!from_block_index->contains_new_bottom_states);
5469 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5471 bool work_assigned=
false;
5472 for (BLC_list_const_iterator work_it=splitter->start_same_BLC;
5473 work_it<splitter->end_same_BLC; ++work_it)
5476 if (0==m_states[m_aut.get_transitions()[*work_it].from()].
5477 no_of_outgoing_block_inert_transitions)
5483 check_complexity::stabilizeB_main_loop, 1), *
this);
5488 add_work(check_complexity::stabilizeB_main_loop, 1), *
this);
5499 stabilize_work_to_assign_later.emplace_back(splitter->start_same_BLC,
5500 splitter->end_same_BLC);
5503 if (std::distance(from_block_index->start_bottom_states,
5504 from_block_index->end_states)<=1)
5513 splitter->make_stable();
5516 { assert(!is_inert_during_init(first_t) || from_block_index->c.onstellation!=
5517 m_states[first_t.to()].block->c.onstellation);
5518 if (initialization && !small_splitter_used_up && 1==Qhat.size())
5523 make_stable_and_move_to_start_of_BLC(from_block_index, splitter);
5524 four_way_splitB<
true,
false>(from_block_index, splitter,
5525 from_block_index->block.to_constellation.end(),
5526 null_constellation, new_constellation);
5527 if (Qhat_elt.first==Qhat_elt.second)
5532 small_splitter_used_up=
true;
5537 four_way_splitB<
false,
true>(from_block_index, from_block_index->
5538 block.to_constellation.end(), splitter,
5539 null_constellation, null_constellation);
5541 } assert(Qhat_elt.first<=Qhat_elt.second);
5542 if (Qhat_elt.first==Qhat_elt.second)
5548 while (m_blocks_with_new_bottom_states.empty()); assert(1==m_blocks_with_new_bottom_states.size());
5549 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5553 for (std::vector<std::pair<BLC_list_const_iterator,BLC_list_const_iterator> >
5554 ::iterator qhat_it=initialize_qhat_work_to_assign_later.begin();
5555 qhat_it!=initialize_qhat_work_to_assign_later.end(); )
5557 bool new_bottom_state_with_transition_found=
false;
5558 for (BLC_list_const_iterator work_it=qhat_it->first;
5559 work_it<qhat_it->second; ++work_it)
5561 const state_index t_from=m_aut.get_transitions()[*work_it].from();
5562 if (0==m_states[t_from].no_of_outgoing_block_inert_transitions)
5567 if (new_bottom_state_with_transition_found)
5571 stabilizeB_initialize_Qhat_afterwards, 1), *
this);
5576 stabilizeB_initialize_Qhat_afterwards, 1), *
this);
5577 new_bottom_state_with_transition_found=
true;
5583 if (new_bottom_state_with_transition_found)
5587 *qhat_it=initialize_qhat_work_to_assign_later.back();
5588 if (std::next(qhat_it)==initialize_qhat_work_to_assign_later.end())
5590 initialize_qhat_work_to_assign_later.pop_back();
5595 initialize_qhat_work_to_assign_later.pop_back();
5606 for (std::vector<std::pair<BLC_list_const_iterator,BLC_list_const_iterator> >
5607 ::iterator stabilize_it=stabilize_work_to_assign_later.begin();
5608 stabilize_it!=stabilize_work_to_assign_later.end(); )
5610 bool new_bottom_state_with_transition_found=
false;
5611 for (BLC_list_const_iterator work_it=stabilize_it->first;
5612 work_it<stabilize_it->second; ++work_it)
5614 const state_index t_from=m_aut.get_transitions()[*work_it].from();
5615 if (0==m_states[t_from].no_of_outgoing_block_inert_transitions)
5620 if (new_bottom_state_with_transition_found)
5623 check_complexity::stabilizeB_main_loop_afterwards, 1), *
this);
5628 stabilizeB_main_loop_afterwards, 1), *
this);
5629 new_bottom_state_with_transition_found=
true;
5635 if (new_bottom_state_with_transition_found)
5639 *stabilize_it=stabilize_work_to_assign_later.back();
5640 if (std::next(stabilize_it) == stabilize_work_to_assign_later.end())
5642 stabilize_work_to_assign_later.pop_back();
5647 stabilize_work_to_assign_later.pop_back();
5656 block_type*
const bi=m_blocks_with_new_bottom_states.front(); assert(bi->contains_new_bottom_states);
5657 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5661 const state_in_block_pointer* new_bott_it=bi->start_bottom_states;
5662 assert(new_bott_it < bi->sta.rt_non_bottom_states);
5666 add_work(check_complexity::stabilizeB_prepare_block, 1), *
this);
5668 while (++new_bott_it<bi->sta.rt_non_bottom_states);
5670 bi->contains_new_bottom_states=
false;
5671 clear(m_blocks_with_new_bottom_states);
5672 if (1>=number_of_states_in_block(*bi))
5678 ind=bi->block.to_constellation.begin(); assert(!bi->block.to_constellation.empty());
5679 assert(ind->start_same_BLC<ind->end_same_BLC);
5681 const transition& first_t=m_aut.get_transitions()[*ind->start_same_BLC];
5682 assert(m_states[first_t.from()].block==bi);
5683 assert(is_inert_during_init_if_branching(first_t) &&
5684 bi->c.onstellation==m_states[first_t.to()].block->c.onstellation);
5686 assert(ind->is_stable());
5688 for (; bi->block.to_constellation.end()!=ind; ++ind)
5690 if (!ind->is_stable())
5694 while (++ind!=bi->block.to_constellation.end())
5696 assert(!ind->is_stable());
5699 assert(!ind->has_marked_transitions());
5704 ind->start_marked_BLC=ind->end_same_BLC;
5706 assert(!ind->has_marked_transitions());
5707 assert(ind->start_same_BLC<ind->end_same_BLC);
5708 const transition& first_t = m_aut.get_transitions()[*ind->start_same_BLC];
5709 assert(m_states[first_t.from()].block == bi);
5710 assert(!is_inert_during_init_if_branching(first_t) ||
5711 bi->c.onstellation!=m_states[first_t.to()].block->c.onstellation);
5713 Qhat.emplace_back(ind->start_same_BLC, ind->end_same_BLC);
5714 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5717 bool work_assigned =
false;
5719 for (BLC_list_const_iterator work_it = ind->start_same_BLC;
5720 work_it<ind->end_same_BLC; ++work_it)
5723 if (0==m_states[m_aut.get_transitions()
5724 [*work_it].from()].no_of_outgoing_block_inert_transitions)
5730 check_complexity::stabilizeB_initialize_Qhat, 1), *
this);
5735 check_complexity::stabilizeB_initialize_Qhat, 1), *
this);
5736 work_assigned =
true;
5746 initialize_qhat_work_to_assign_later.emplace_back(ind->start_same_BLC,
5754 state_in_block_pointer* si=bi->start_bottom_states; assert(si<bi->sta.rt_non_bottom_states);
5757 check_complexity::stabilizeB_distribute_states_over_Phat, 1), *
this);
5758 outgoing_transitions_it end_it=
5759 std::next(si->ref_state)>=m_states.end()
5760 ? m_outgoing_transitions.end()
5761 : std::next(si->ref_state)->start_outgoing_transitions; assert(si->ref_state->block==bi);
5762 for (outgoing_transitions_it ti=
5763 si->ref_state->start_outgoing_transitions; ti<end_it; ++ti)
5766 const transition& t=
5767 m_aut.get_transitions()[*ti->ref.BLC_transitions]; assert(m_states.begin()+t.from()==si->ref_state);
5768 if (!is_inert_during_init_if_branching(t) ||
5769 bi->c.onstellation!=m_states[t.to()].block->c.onstellation)
5772 mark_BLC_transition(ti);
5774 assert(ti <= ti->start_same_saC);
5775 ti = ti->start_same_saC;
5779 while (si<bi->sta.rt_non_bottom_states);
5783 void create_initial_partition()
5785 mCRL2log(log::verbose) <<
"An O(m log n) "
5786 << (m_branching ? (m_preserve_divergence
5787 ?
"divergence-preserving branching "
5790 <<
"bisimulation partitioner created for " << m_aut.num_states()
5791 <<
" states and " << m_transitions.size()
5792 <<
" transitions (using the experimental algorithm GJ2025).\n";
5793 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5794 check_complexity::init(2 * m_aut.num_states());
5797 group_transitions_on_tgt_label(m_aut);
5799 assert((
unsigned) m_preserve_divergence <= 1);
5800 constellation_type*
const initial_constellation=
5802 simple_list<BLC_indicators>::get_pool().
5803 template construct<constellation_type>
5805 new constellation_type
5807 (m_states_in_blocks.data(), m_states_in_blocks.data_end()); assert(1==no_of_constellations);
5808 block_type*
const initial_block=
5810 simple_list<BLC_indicators>::get_pool().
5811 template construct<block_type>
5815 (m_states_in_blocks.data(), m_states_in_blocks.data_end(),
5816 m_states_in_blocks.data_end(), initial_constellation); assert(1==no_of_blocks);
5818 #define temporary_BLC_list (initial_block->block.to_constellation)
5824 std::vector<label_index> todo_stack_actions;
5825 std::vector<transition_index> count_transitions_per_action
5826 (m_aut.num_action_labels() + (
unsigned) m_preserve_divergence, 0);
5832 todo_stack_actions.push_back(m_aut.tau_label_index());
5833 count_transitions_per_action[m_aut.tau_label_index()] = 1;
5835 for (transition_index ti=0; ti<m_transitions.size(); ++ti)
5837 const transition& t=m_aut.get_transitions()[ti];
5841 const label_index label=label_or_divergence(t,
5842 m_aut.num_action_labels()); assert(m_aut.apply_hidden_label_map(t.label())==t.label());
5843 transition_index& c=count_transitions_per_action[label];
5846 todo_stack_actions.push_back(label);
5851 { assert(m_aut.is_tau(todo_stack_actions.front()));
5852 --count_transitions_per_action[m_aut.tau_label_index()];
5854 accumulate_entries(count_transitions_per_action, todo_stack_actions);
5855 for (transition_index ti=0; ti<m_transitions.size(); ++ti)
5858 const transition& t=m_aut.get_transitions()[ti];
5859 const label_index label = label_or_divergence(t,
5860 m_aut.num_action_labels());
5861 transition_index& c=count_transitions_per_action[label]; assert(c < m_transitions.size());
5862 m_BLC_transitions[c]=ti;
5867 std::vector<label_index>::const_iterator
5868 a_it=todo_stack_actions.begin();
5869 if (a_it!=todo_stack_actions.end() &&
5870 (0!=count_transitions_per_action[*a_it] || (assert(m_branching), assert(m_aut.is_tau(*a_it)),
5871 ++a_it!=todo_stack_actions.end())) )
5873 BLC_list_iterator start_index=m_BLC_transitions.data();
5876 const label_index a=*a_it;
5877 BLC_list_iterator end_index=
5878 m_BLC_transitions.data()+count_transitions_per_action[a]; assert(end_index<=m_BLC_transitions.data_end());
5880 temporary_BLC_list.emplace_back(start_index, end_index,
true); assert(start_index<end_index);
5881 start_index=end_index;
5883 while (++a_it!=todo_stack_actions.end()); assert(start_index==m_BLC_transitions.data_end());
5892 fixed_vector<transition_index> count_outgoing_transitions_per_state
5893 (m_aut.num_states(), 0);
5894 for(
const transition& t: m_aut.get_transitions())
5897 count_outgoing_transitions_per_state[t.from()]++;
5898 if (is_inert_during_init(t))
5900 m_states[t.from()].no_of_outgoing_block_inert_transitions++;
5910 outgoing_transitions_it current_outgoing_transitions=
5911 m_outgoing_transitions.begin();
5914 for (state_index s=0; s<m_aut.num_states(); ++s)
5916 if (marked_range<=m_states[s].no_of_outgoing_block_inert_transitions)
5918 mCRL2log(log::error) <<
"State " << s <<
" has "
5919 << m_states[s].no_of_outgoing_block_inert_transitions
5920 <<
" outgoing block-inert transitions. However, the "
5921 "four-way-split can handle at most " << (marked_range-1)
5922 <<
" outgoing block-inert transitions per state. "
5926 m_states[s].start_outgoing_transitions=current_outgoing_transitions+
5927 m_states[s].no_of_outgoing_block_inert_transitions;
5928 current_outgoing_transitions+=
5929 static_cast<std::ptrdiff_t>(count_outgoing_transitions_per_state[s]);
5930 count_outgoing_transitions_per_state[s]=0;
5933 } assert(m_outgoing_transitions.end()==current_outgoing_transitions);
5935 for (BLC_list_iterator ti=m_BLC_transitions.data();
5936 ti<m_BLC_transitions.data_end(); ++ti)
5938 const transition& t=m_aut.get_transitions()[*ti];
5939 if (is_inert_during_init(t))
5941 m_transitions[*ti].ref_outgoing_transitions =
5942 --m_states[t.from()].start_outgoing_transitions;
5946 m_transitions[*ti].ref_outgoing_transitions =
5947 m_states[t.from()].start_outgoing_transitions +
5948 count_outgoing_transitions_per_state[t.from()];
5951 m_transitions[*ti].ref_outgoing_transitions->ref.transitions=*ti;
5953 m_transitions[*ti].ref_outgoing_transitions->
5954 ref.BLC_transitions=ti;
5956 ++count_outgoing_transitions_per_state[t.from()];
5961 state_index current_state=null_state; assert(current_state + 1 == 0);
5964 for(std::vector<transition>::iterator it=m_aut.get_transitions().begin();
5965 it!=m_aut.get_transitions().end(); it++)
5968 const transition& t=*it;
5969 if (t.to()!=current_state)
5971 for (state_index i=current_state+1; i<=t.to(); ++i)
5974 create_initial_partition_set_start_incoming_transitions, 1), *
this);
5975 m_states[i].start_incoming_transitions=it;
5977 current_state=t.to();
5980 for (state_index i=current_state+1; i<m_aut.num_states(); ++i)
5982 create_initial_partition_set_start_incoming_transitions, 1), *
this);
5983 m_states[i].start_incoming_transitions=m_aut.get_transitions().end();
5987 outgoing_transitions_it it = m_outgoing_transitions.end();
5988 if (m_outgoing_transitions.begin() < it)
5991 const transition& t=m_aut.get_transitions()[
5995 *it->ref.BLC_transitions
5998 state_index current_state = t.from();
5999 label_index current_label = label_or_divergence(t);
6000 outgoing_transitions_it current_end_same_saC = it;
6001 while (m_outgoing_transitions.begin() < it)
6005 const transition& t=m_aut.get_transitions()[
6009 *it->ref.BLC_transitions
6012 const label_index new_label = label_or_divergence(t);
6013 if (current_state == t.from() && current_label == new_label)
6017 it->start_same_saC = current_end_same_saC;
6022 current_state = t.from();
6023 current_label = new_label;
6024 current_end_same_saC->start_same_saC = std::next(it);
6025 current_end_same_saC = it;
6028 current_end_same_saC->start_same_saC = m_outgoing_transitions.begin();
6029 } assert(m_states_in_blocks.size()==m_aut.num_states());
6030 state_in_block_pointer* lower_i=m_states_in_blocks.data(); assert(initial_block->start_bottom_states==lower_i);
6031 state_in_block_pointer* upper_i=m_states_in_blocks.data_end(); assert(initial_block->end_states==upper_i);
6032 for (fixed_vector<state_type_gj>::iterator i=m_states.begin();
6033 i<m_states.end(); ++i)
6035 if (0<i->no_of_outgoing_block_inert_transitions)
6038 upper_i->ref_state=i;
6039 i->ref_states_in_blocks=upper_i;
6043 lower_i->ref_state=i;
6044 i->ref_states_in_blocks=lower_i;
6047 i->block=initial_block;
6048 } assert(lower_i == upper_i);
6049 initial_block->sta.rt_non_bottom_states = lower_i;
6051 for (linked_list<BLC_indicators>::iterator
6052 blc_it=temporary_BLC_list.begin();
6053 temporary_BLC_list.end()!=blc_it; ++blc_it)
6054 { assert(blc_it->start_same_BLC<blc_it->end_same_BLC);
6055 BLC_list_iterator it=blc_it->start_same_BLC;
6056 if (!is_inert_during_init(m_aut.get_transitions()[*it]))
6058 ++no_of_non_constellation_inert_BLC_sets;
6062 m_transitions[*it].transitions_per_block_to_constellation=blc_it;
6065 while (it!=blc_it->end_same_BLC);
6067 #undef temporary_BLC_list
6069 initial_block->contains_new_bottom_states =
true;
6070 m_blocks_with_new_bottom_states.push_back(initial_block);
6072 assert(check_data_structures(
"After initial reading before splitting in the initialisation",
false,
false));
6075 assert(check_data_structures(
"After initial reading before splitting in the initialisation",
true,
false));
6083 if (!temporary_BLC_list.empty())
6086 temporary_BLC_list.begin(); assert(blc_it->start_same_BLC<blc_it->end_same_BLC);
6087 if (!is_inert_during_init
6088 (m_aut.get_transitions()[*blc_it->start_same_BLC]) ||
6089 ++blc_it!=temporary_BLC_list.end())
6093 std::vector<block_type*> blocks_that_need_refinement;
6094 BLC_list_iterator trans_it=blc_it->start_same_BLC; assert(trans_it<blc_it->end_same_BLC);
6095 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
6096 const label_index a=label_or_divergence(m_aut.get_transitions()[*trans_it]);
6101 const transition& t=m_aut.get_transitions()[*trans_it]; assert(label_or_divergence(t)==a);
6102 const state_in_block_pointer s(m_states.begin()+t.from());
6103 block_type& B=*s.ref_state->block;
6104 if (
nullptr==B.block.R)
6105 { assert(std::find(blocks_that_need_refinement.begin(),
6106 blocks_that_need_refinement.end(), s.ref_state->block)==
6107 blocks_that_need_refinement.end());
6108 if (B.contains_new_bottom_states ||
6109 number_of_states_in_block(B)<=1)
6113 B.block.R=
new std::vector<state_in_block_pointer>();
6114 blocks_that_need_refinement.push_back(s.ref_state->block);
6116 B.c.first_unmarked_bottom_state=B.start_bottom_states;
6117 }
else { assert(std::find(blocks_that_need_refinement.begin(),
6118 blocks_that_need_refinement.end(), s.ref_state->block)!=
6119 blocks_that_need_refinement.end()); }
6120 state_in_block_pointer*
const
6121 pos_s=s.ref_state->ref_states_in_blocks; assert(B.start_bottom_states<=pos_s); assert(pos_s<B.end_states);
6122 if (B.c.first_unmarked_bottom_state<=pos_s)
6124 if (0==s.ref_state->no_of_outgoing_block_inert_transitions)
6125 { assert(pos_s<B.sta.rt_non_bottom_states);
6126 swap_states_in_states_in_block
6127 (B.c.first_unmarked_bottom_state, pos_s); assert(undefined==s.ref_state->counter);
6128 B.c.first_unmarked_bottom_state++;
6132 if (undefined==s.ref_state->counter)
6134 B.block.R->push_back(s);
6135 s.ref_state->counter=marked(ReachAlw)+
6136 s.ref_state->no_of_outgoing_block_inert_transitions; assert(B.sta.rt_non_bottom_states<=pos_s);
6137 }
else { assert(B.sta.rt_non_bottom_states<=pos_s); }
6138 assert(is_in_marked_range_of(s.ref_state->counter, ReachAlw));
6142 while (++trans_it<blc_it->end_same_BLC);
6144 for (block_type*
const bi : blocks_that_need_refinement)
6145 { assert(
nullptr!=bi->block.R);
6146 four_way_splitB<
false,
false>(bi,
6149 null_constellation, initial_constellation);
6159 while (++blc_it!=temporary_BLC_list.end());
6162 if (!block_type::btc_R::
6163 if_R_is_nullptr_then_to_constellation_is_empty_list())
6167 state_in_block_pointer* st_it=m_states_in_blocks.data(); assert(m_states_in_blocks.data_end()!=st_it);
6170 block_type*
const blk_it=st_it->ref_state->block; assert(
nullptr==blk_it->block.R);
6174 new(&blk_it->block.to_constellation)
linked_list<BLC_indicators>();
6175 st_it=blk_it->end_states;
6177 while (m_states_in_blocks.data_end()!=st_it);
6180 state_in_block_pointer*
const
6181 last_block_start=std::prev(m_states_in_blocks.end())->
6182 ref_state->block->start_bottom_states;
6184 while(blc_it=temporary_BLC_list.begin(),temporary_BLC_list.end()!=blc_it)
6186 order_BLC_transitions(blc_it->start_same_BLC, blc_it->end_same_BLC,
6187 m_states_in_blocks.data(), last_block_start);
6190 temporary_BLC_list.erase(blc_it);
6194 assert(check_stability(
"End initialisation"));
6195 assert(check_data_structures(
"End initialisation",
false,
false));
6215 linked_list<BLC_indicators>::iterator find_inert_co_transition_for_block(
6216 block_type*
const index_block_B,
6217 const constellation_type*
const old_constellation,
6218 const constellation_type*
const new_constellation)
const
6221 btc_it=index_block_B->block.to_constellation.begin();
6222 if (btc_it == index_block_B->block.to_constellation.end())
6225 return index_block_B->block.to_constellation.end();
6226 } assert(btc_it->start_same_BLC<btc_it->end_same_BLC);
6227 const transition& btc_t=
6228 m_aut.get_transitions()[*(btc_it->start_same_BLC)];
6229 if (!is_inert_during_init_if_branching(btc_t))
6234 return index_block_B->block.to_constellation.end();
6236 if (m_states[btc_t.to()].block->c.onstellation==old_constellation)
6242 if (m_states[btc_t.to()].block->c.onstellation!=new_constellation)
6246 return index_block_B->block.to_constellation.end();
6250 btc_it=index_block_B->block.to_constellation.next(btc_it);
6251 if (btc_it == index_block_B->block.to_constellation.end())
6254 return index_block_B->block.to_constellation.end();
6255 } assert(btc_it->start_same_BLC<btc_it->end_same_BLC);
6256 const transition& btc2_t=
6257 m_aut.get_transitions()[*(btc_it->start_same_BLC)];
6258 if (!is_inert_during_init_if_branching(btc2_t) ||
6259 old_constellation!=m_states[btc2_t.to()].block->c.onstellation)
6263 return index_block_B->block.to_constellation.end();
6278 block_type* select_and_remove_a_block_in_a_non_trivial_constellation()
6279 { assert(!m_non_trivial_constellations.empty());
6282 constellation_type*
const ci=m_non_trivial_constellations.back();
6283 block_type* index_block_B=ci->start_const_states->ref_state->block;
6284 block_type* second_block_B=
6285 std::prev(ci->end_const_states)->ref_state->block;
6287 if (number_of_states_in_block(*index_block_B)<=
6288 number_of_states_in_block(*second_block_B))
6290 ci->start_const_states=index_block_B->end_states;
6294 ci->end_const_states=second_block_B->start_bottom_states;
6295 index_block_B=second_block_B;
6297 return index_block_B;
6309 state_index no_of_new_bottom_states = 0;
6315 transition_index no_of_non_constellation_inert_BLC_sets = 0;
6317 void refine_partition_until_it_becomes_stable()
6323 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> > calM;
6325 std::clock_t next_print_time = std::clock();
6326 const std::clock_t rounded_start_time = next_print_time-CLOCKS_PER_SEC/2;
6329 assert(check_data_structures(
"MAIN LOOP"));
6330 assert(check_stability(
"MAIN LOOP"));
6331 if (mCRL2logEnabled(log::verbose))
6333 if (std::clock_t now = std::clock(); next_print_time <= now ||
6334 m_non_trivial_constellations.empty())
6344 next_print_time+=((now-next_print_time)/(60*CLOCKS_PER_SEC)
6345 + 1) * (60*CLOCKS_PER_SEC);
6346 now = (now - rounded_start_time) / CLOCKS_PER_SEC;
6353 mCRL2log(log::verbose) << now / 3600 <<
" h ";
6356 mCRL2log(log::verbose) << now / 60 <<
" min ";
6360 <<
" sec passed since starting the main loop.\n";
6362 #define PRINT_SG_PL(counter, sg_string, pl_string)
6363 (counter) << (1
== (counter) ? (sg_string) : (pl_string))
6365 << (m_non_trivial_constellations.empty()
6366 ?
"The reduced LTS contains "
6367 :
"The reduced LTS contains at least ")
6368 <<
PRINT_SG_PL(no_of_blocks,
" state and ",
" states and ")
6369 <<
PRINT_SG_PL(no_of_non_constellation_inert_BLC_sets,
6370 " transition.",
" transitions.");
6371 if (1 < no_of_blocks)
6373 #define PRINT_INT_PERCENTAGE(num,denom)
6374 (((num) * 200
+ (denom)) / (denom) / 2
)
6375 mCRL2log(log::verbose) <<
" Estimated "
6379 #undef PRINT_INT_PERCENTAGE
6387 <<
"\nThe current partition contains ";
6392 " new bottom state and ",
" new bottom states and ");
6393 }
else { assert(0==no_of_new_bottom_states); }
6396 " constellation (of which ",
" constellations (of which ")
6397 <<
PRINT_SG_PL(m_non_trivial_constellations.size(),
6398 " is nontrivial).\n",
" are nontrivial).\n");
6402 if (m_non_trivial_constellations.empty())
6407 block_type* index_block_B=
6408 select_and_remove_a_block_in_a_non_trivial_constellation();
6409 constellation_type*
const old_constellation=
6410 index_block_B->c.onstellation;
6413 if (old_constellation->start_const_states->ref_state->block==
6414 std::prev(old_constellation->end_const_states)->ref_state->block)
6415 { assert(m_non_trivial_constellations.back()==old_constellation);
6417 m_non_trivial_constellations.pop_back();
6419 constellation_type*
const new_constellation=
6421 simple_list<BLC_indicators>::get_pool().
6422 template construct<constellation_type>
6424 new constellation_type
6426 (index_block_B->start_bottom_states,
6427 index_block_B->end_states);
6428 ++no_of_constellations;
6429 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
6431 unsigned char const max_C=check_complexity::log_n-check_complexity::
6432 ilog2(number_of_states_in_constellation(*new_constellation));
6434 refine_partition_until_it_becomes_stable_find_splitter, max_C), *
this);
6440 for (state_in_block_pointer* i=index_block_B->start_bottom_states;
6441 i!=index_block_B->end_states; ++i)
6444 const std::vector<transition>::iterator end_it=
6445 (std::next(i->ref_state)==m_states.end())
6446 ? m_aut.get_transitions().end()
6447 : std::next(i->ref_state)->start_incoming_transitions;
6448 for(std::vector<transition>::iterator
6449 j=i->ref_state->start_incoming_transitions; j!=end_it; ++j)
6451 const transition& t=*j;
6452 const transition_index t_index=
6453 std::distance(m_aut.get_transitions().begin(), j);
6456 const outgoing_transitions_it old_pos=
6457 m_transitions[t_index].ref_outgoing_transitions;
6458 const outgoing_transitions_it end_same_saC=
6459 old_pos->start_same_saC < old_pos
6460 ? old_pos : old_pos->start_same_saC;
6461 const outgoing_transitions_it new_pos=end_same_saC->start_same_saC; assert(m_states[t.from()].start_outgoing_transitions<=new_pos);
6462 assert(new_pos<=old_pos);
6463 if (old_pos != new_pos)
6465 std::swap(old_pos->ref.BLC_transitions,
6466 new_pos->ref.BLC_transitions);
6467 m_transitions[*old_pos->ref.BLC_transitions].
6468 ref_outgoing_transitions=old_pos;
6469 m_transitions[*new_pos->ref.BLC_transitions].
6470 ref_outgoing_transitions=new_pos;
6472 if (new_pos < end_same_saC)
6474 end_same_saC->start_same_saC = std::next(new_pos);
6480 new_pos->start_same_saC = new_pos;
6481 if (m_states[t.from()].start_outgoing_transitions<new_pos)
6484 const transition& prev_t = m_aut.get_transitions()
6485 [*std::prev(new_pos)->ref.BLC_transitions]; assert(prev_t.from() == t.from());
6486 if (m_states[prev_t.to()].block == index_block_B &&
6487 label_or_divergence(prev_t) == label_or_divergence(t))
6490 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);
6491 assert(new_pos->start_same_saC<new_pos);
6492 assert(std::prev(new_pos)==new_pos->start_same_saC->start_same_saC);
6493 new_pos->start_same_saC->start_same_saC = new_pos;
6501 for (state_in_block_pointer* i=index_block_B->start_bottom_states;
6502 i!=index_block_B->end_states; ++i)
6505 const std::vector<transition>::iterator end_it=
6506 (std::next(i->ref_state)==m_states.end())
6507 ? m_aut.get_transitions().end()
6508 : std::next(i->ref_state)->start_incoming_transitions;
6509 for(std::vector<transition>::iterator
6510 j=i->ref_state->start_incoming_transitions; j!=end_it; ++j)
6512 const transition& t=*j;
6513 const transition_index t_index=
6514 std::distance(m_aut.get_transitions().begin(), j); assert(m_states[t.to()].block == index_block_B);
6515 bool source_block_is_singleton=
6516 (1>=number_of_states_in_block(*m_states[t.from()].block));
6519 const outgoing_transitions_it out_pos=
6520 m_transitions[t_index].ref_outgoing_transitions;
6521 const outgoing_transitions_it start_new_saC=
6522 out_pos->start_same_saC;
6523 if (start_new_saC < out_pos)
6526 if (out_pos < start_new_saC->start_same_saC)
6529 out_pos->start_same_saC = start_new_saC->start_same_saC;
6534 if (update_the_doubly_linked_list_LBC_new_constellation
6535 (index_block_B, t, t_index) &&
6536 !source_block_is_singleton &&
6537 (!is_inert_during_init(t) ||
6538 index_block_B!=m_states[t.from()].block))
6542 BLC_list_iterator BLC_pos=m_transitions[t_index].
6543 ref_outgoing_transitions->ref.BLC_transitions; assert(t_index == *BLC_pos);
6545 calM.emplace_back(BLC_pos, BLC_pos);
6550 index_block_B->c.onstellation=new_constellation;
6554 if (calM.begin()!=calM.end())
6556 for (std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >::
6557 iterator calM_elt=calM.begin();; )
6559 linked_list <BLC_indicators>::iterator ind=m_transitions
6560 [*calM_elt->first].transitions_per_block_to_constellation;
mCRL2complexity(ind, add_work(check_complexity::
6561 refine_partition_until_it_becomes_stable_correct_end_of_calM,max_C),*
this);
6562 assert(ind->start_same_BLC==calM_elt->first);
6563 assert(!ind->has_marked_transitions());
6564 const transition& last_t=
6565 m_aut.get_transitions()[*std::prev(ind->end_same_BLC)]; assert(m_states[last_t.to()].block->c.onstellation==new_constellation);
6566 assert(ind->start_same_BLC<ind->end_same_BLC);
6567 const transition* next_t=
nullptr;
6568 if ((is_inert_during_init(last_t) &&
6569 m_states[last_t.from()].block->c.onstellation==
6570 old_constellation && (assert(m_states[last_t.from()].block!=index_block_B),
true)
6572 (ind->end_same_BLC<m_BLC_transitions.data_end() &&
6573 (next_t=&m_aut.get_transitions()[*ind->end_same_BLC],
6574 m_states[last_t.from()].block==
6575 m_states[next_t->from()].block &&
6576 label_or_divergence(last_t)==label_or_divergence(*next_t) &&
6578 m_states[next_t->to()].block->c.onstellation)))
6582 calM_elt->second = ind->end_same_BLC;
6584 if (calM_elt==calM.end())
6594 if (std::prev(calM.end())==calM_elt)
6605 calM_elt->first=calM.back().first;
6616 linked_list<BLC_indicators>::iterator tau_co_splitter=
6617 find_inert_co_transition_for_block(index_block_B,
6618 old_constellation, new_constellation);
6621 if (index_block_B->block.to_constellation.end()!=tau_co_splitter)
6625 ++no_of_non_constellation_inert_BLC_sets;
6626 if (number_of_states_in_block(*index_block_B) > 1)
6627 { assert(tau_co_splitter->is_stable());
6628 four_way_splitB<
true,
false>(index_block_B, tau_co_splitter,
6629 index_block_B->block.to_constellation.end(),
6638 for (std::pair<BLC_list_iterator, BLC_list_iterator> calM_elt: calM)
6642 assert(check_stability(
"Main loop", &calM, &calM_elt, old_constellation, new_constellation));
6643 assert(check_data_structures(
"Main loop",
false,
false));
6644 assert(calM_elt.first < calM_elt.second);
6648 m_transitions[*std::prev(calM_elt.second)].
6649 transitions_per_block_to_constellation;
mCRL2complexity(splitter, add_work(check_complexity::
6650 refine_partition_until_it_becomes_stable_execute_main_split,max_C),*
this);
6651 assert(splitter->end_same_BLC==calM_elt.second); assert(splitter->is_stable());
6652 calM_elt.second = splitter->start_same_BLC; assert(splitter->start_same_BLC<splitter->end_same_BLC);
6654 const transition& first_t=
6655 m_aut.get_transitions()[*splitter->start_same_BLC];
6656 const label_index a=label_or_divergence(first_t); assert(m_states[first_t.to()].block->c.onstellation==new_constellation);
6657 block_type* Bpp=m_states[first_t.from()].block; assert(Bpp->c.onstellation!=new_constellation ||
6658 !is_inert_during_init(first_t));
6659 if (number_of_states_in_block(*Bpp) <= 1)
6663 else if (Bpp->contains_new_bottom_states)
6670 else if (is_inert_during_init(first_t) &&
6671 old_constellation==Bpp->c.onstellation)
6676 four_way_splitB<
true,
false>(Bpp, splitter,
6677 Bpp->block.to_constellation.end(),
6678 old_constellation, new_constellation);
6683 linked_list<BLC_indicators>::iterator co_splitter=
6684 Bpp->block.to_constellation.prev(splitter);
6685 const transition* co_t;
6687 if (Bpp->block.to_constellation.end()!=co_splitter &&
6688 ( assert(co_splitter->is_stable()),
6689 assert(co_splitter->start_same_BLC<co_splitter->end_same_BLC),
6690 co_t=&m_aut.get_transitions()[*co_splitter->start_same_BLC], assert(m_states[co_t->from()].block==Bpp),
6691 a==label_or_divergence(*co_t) &&
6693 m_states[co_t->to()].block->c.onstellation))
6696 four_way_splitB<
true,
true>(Bpp, splitter, co_splitter,
6697 old_constellation, new_constellation);
6702 while (calM_elt.first < calM_elt.second);
6704 assert(check_data_structures(
"Before stabilize",
false,
false));
6705 assert(check_stability(
"Before stabilize"));
6708 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
6709 check_complexity::print_grand_totals();
6715 std::clock_t end_initial_part;
6728 bisim_partitioner_gj(LTS_TYPE& aut,
const bool branching =
false,
6729 const bool preserve_divergence =
false)
6731 m_states(aut.num_states()),
6732 m_outgoing_transitions(aut.num_transitions()),
6733 m_transitions(aut.num_transitions()),
6734 m_states_in_blocks(aut.num_states()),
6736 m_BLC_transitions(aut.num_transitions()),
6737 m_branching(branching),
6738 m_preserve_divergence(preserve_divergence)
6739 { assert(m_branching || !m_preserve_divergence);
6742 aut.rename_hidden_labels_to_tau();
6743 create_initial_partition();
6744 end_initial_part=std::clock();
6745 mCRL2log(log::debug) <<
"After initialisation there are "
6746 << no_of_blocks <<
" equivalence classes. Start refining. \n";
6747 refine_partition_until_it_becomes_stable(); assert(check_data_structures(
"READY"));
6778template <
class LTS_TYPE>
6779void bisimulation_reduce_gj(LTS_TYPE& l,
const bool branching =
false,
6780 const bool preserve_divergence=
false)
6782 if (1 >= l.num_states())
6784 mCRL2log(log::warning) <<
"There is only 1 state in the LTS. It is not "
6785 "guaranteed that branching bisimulation minimisation runs in "
6786 "time O(m log n).\n";
6790 const std::clock_t start_SCC=std::clock();
6793 scc_reduce(l, preserve_divergence);
6798 const std::clock_t start_part=std::clock();
6799 bisim_partitioner_gj<LTS_TYPE> bisim_part(l,branching,preserve_divergence);
6802 const std::clock_t end_part=std::clock();
6803 bisim_part.finalize_minimized_LTS();
6805 if (mCRL2logEnabled(log::debug))
6807 const std::clock_t end_finalizing=std::clock();
6808 const int prec=
static_cast<
int>
6809 (std::log10(CLOCKS_PER_SEC)+0.69897000433602);
6815 runtime[0]=(
double) (end_finalizing - start_SCC)/CLOCKS_PER_SEC;
6816 runtime[1]=(
double) ( start_part-start_SCC)/CLOCKS_PER_SEC;
6817 runtime[2]=(
double) ( bisim_part.end_initial_part-start_part )/CLOCKS_PER_SEC;
6818 runtime[3]=(
double) ( end_part-bisim_part.end_initial_part )/CLOCKS_PER_SEC;
6819 runtime[4]=(
double) (end_finalizing-end_part )/CLOCKS_PER_SEC;
6820 if (runtime[0]>=60.0)
6822 int min[
sizeof(runtime)/
sizeof(runtime[0])];
6823 for (
unsigned i = 0; i <
sizeof(runtime)/
sizeof(runtime[0]); ++i)
6825 min[i] =
static_cast<
int>(runtime[i]) / 60;
6826 runtime[i] -= 60 * min[i];
6830 int h[
sizeof(runtime)/
sizeof(runtime[0])];
6831 for (
unsigned i=0; i <
sizeof(runtime)/
sizeof(runtime[0]); ++i)
6836 int width =
static_cast<
int>(std::log10(h[0])) + 1;
6838 mCRL2log(log::debug) << std::fixed << std::setprecision(prec)
6839 <<
"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"
6840 "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"
6841 "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"
6842 "Time spent on finalizing: " << std::setw(width) << h[4] <<
"h " << std::setw(2) << min[4] <<
"min " << std::setw(prec+3) << runtime[4] <<
"s\n"
6843 "Total CPU time: " << std::setw(width) << h[0] <<
"h " << std::setw(2) << min[0] <<
"min " << std::setw(prec+3) << runtime[0] <<
"s\n"
6844 "BENCHMARK TIME: " <<
static_cast<
double>(end_part-start_part)/CLOCKS_PER_SEC <<
"\n"
6845 << std::defaultfloat;
6849 mCRL2log(log::debug) << std::fixed << std::setprecision(prec)
6850 <<
"Time spent on contracting SCCs: " << std::setw(2) << min[1] <<
"min " << std::setw(prec+3) << runtime[1] <<
"s\n"
6851 "Time spent on initial partition:" << std::setw(2) << min[2] <<
"min " << std::setw(prec+3) << runtime[2] <<
"s\n"
6852 "Time spent on stabilize+refine: " << std::setw(2) << min[3] <<
"min " << std::setw(prec+3) << runtime[3] <<
"s\n"
6853 "Time spent on finalizing: " << std::setw(2) << min[4] <<
"min " << std::setw(prec+3) << runtime[4] <<
"s\n"
6854 "Total CPU time: " << std::setw(2) << min[0] <<
"min " << std::setw(prec+3) << runtime[0] <<
"s\n"
6855 "BENCHMARK TIME: " <<
static_cast<
double>(end_part-start_part)/CLOCKS_PER_SEC <<
"\n"
6856 << std::defaultfloat;
6861 mCRL2log(log::debug) << std::fixed << std::setprecision(prec)
6862 <<
"Time spent on contracting SCCs: " << std::setw(prec+3) << runtime[1] <<
"s\n"
6863 "Time spent on initial partition:" << std::setw(prec+3) << runtime[2] <<
"s\n"
6864 "Time spent on stabilize+refine: " << std::setw(prec+3) << runtime[3] <<
"s\n"
6865 "Time spent on finalizing: " << std::setw(prec+3) << runtime[4] <<
"s\n"
6866 "Total CPU time: " << std::setw(prec+3) << runtime[0] <<
"s\n"
6867 "BENCHMARK TIME: " <<
static_cast<
double>(end_part-start_part)/CLOCKS_PER_SEC <<
"\n"
6868 << std::defaultfloat;
6893template <
class LTS_TYPE>
6894bool destructive_bisimulation_compare_gj(LTS_TYPE& l1, LTS_TYPE& l2,
6895 const bool branching =
false,
const bool preserve_divergence =
false,
6896 const bool generate_counter_examples =
false,
6897 const std::string& =
"",
6900 if (generate_counter_examples)
6902 mCRL2log(log::warning) <<
"The GJ25 branching bisimulation "
6903 "algorithm does not generate counterexamples.\n";
6905 std::size_t init_l2(l2.initial_state() + l1.num_states());
6906 detail::merge(l1, std::move(l2));
6911 detail::scc_partitioner<LTS_TYPE> scc_part(l1);
6912 scc_part.replace_transition_system(preserve_divergence);
6913 init_l2 = scc_part.get_eq_class(init_l2);
6914 }
else { assert(!preserve_divergence); }
6915 assert(1 < l1.num_states());
6916 bisim_partitioner_gj<LTS_TYPE>bisim_part(l1,branching,preserve_divergence);
6918 return bisim_part.in_same_class(l1.initial_state(), init_l2);
6938template <
class LTS_TYPE>
6939inline bool bisimulation_compare_gj(
const LTS_TYPE& l1,
const LTS_TYPE& l2,
6940 const bool branching =
false,
const bool preserve_divergence =
false)
6942 LTS_TYPE l1_copy(l1);
6943 LTS_TYPE l2_copy(l2);
6944 return destructive_bisimulation_compare_gj(l1_copy, l2_copy, branching,
6945 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