24#ifndef LIBLTS_BISIM_GJ_H
25#define LIBLTS_BISIM_GJ_H
44#ifndef SAVE_BLC_MEMORY
52 #define CO_SPLITTER_IN_BLC_LIST
55 #define CO_SPLITTER_IN_BLC_LIST_VARIANT
80 #define CHECK_COMPLEXITY_GJ
83#ifdef CHECK_COMPLEXITY_GJ
85 #define mCRL2complexity_gj(unit, call, info_for_debug) mCRL2complexity(unit, call, info_for_debug)
87 #define mCRL2complexity_gj(unit, call, info_for_debug) do{}while(0)
97template <
class LTS_TYPE>
class bisim_partitioner_gj;
99namespace bisimulation_gj
127template <
class CONTAINER>
130 if (c.size()>1000) { c=CONTAINER(); }
else { c.clear(); }
214 template <
class... Args>
216 : T(
std::forward<Args>(args)...),
233 return static_cast<T&
>(*this);
276 if (i->
prev()!=
nullptr)
280 while (i->
next()!=
nullptr)
295 template <
class... Args>
298 assert(
nullptr != pos);
300 if (
glla().m_free_list==
nullptr)
302 new_position=&
glla().m_content.emplace_back(pos, pos->prev(), std::forward<Args>(args)...);
307 new_position=
glla().m_free_list;
308 glla().m_free_list=
glla().m_free_list->next();
309 new_position->
content()=T(std::forward<Args>(args)...);
310 new_position->
next()=pos;
311 new_position->
prev()=pos->prev();
313 if (pos->prev()!=
nullptr)
315 pos->prev()->next()=new_position;
321 pos->prev()=new_position;
328 template <
class... Args>
337 if (
glla().m_free_list==
nullptr)
339 new_position=&
glla().m_content.emplace_back(pos->next(), pos, std::forward<Args>(args)...);
344 new_position=
glla().m_free_list;
345 glla().m_free_list=
glla().m_free_list->next();
346 new_position->
content()=T(std::forward<Args>(args)...);
347 new_position->
next()=pos->next();
348 new_position->
prev()=pos;
350 if (pos->next()!=
nullptr)
352 pos->next()->prev()=new_position;
354 pos->next()=new_position;
359 template <
class... Args>
363 if (
glla().m_free_list==
nullptr)
365 new_position=&
glla().m_content.emplace_back(
m_initial_node,
nullptr, std::forward<Args>(args)...);
370 new_position=
glla().m_free_list;
371 glla().m_free_list=
glla().m_free_list->next();
372 new_position->
content()=T(std::forward<Args>(args)...);
374 new_position->
prev()=
nullptr;
397 if (from_pos->
next() !=
nullptr)
399 assert(from_pos == from_pos->
next()->
prev());
402 if (from_pos->
prev() !=
nullptr)
404 assert(from_pos == from_pos->
prev()->
next());
413 from_pos->
prev() = to_pos;
414 if (to_pos !=
nullptr)
417 to_pos->
next() = from_pos;
424 if (from_pos->
next() !=
nullptr)
426 assert(to_pos == from_pos->
next()->
prev());
427 from_pos->
next()->
prev() = from_pos;
437 if (pos->next()!=
nullptr)
439 assert(pos == pos->next()->prev());
440 pos->next()->prev()=pos->prev();
442 if (pos->prev()!=
nullptr)
444 assert(pos == pos->prev()->next());
445 pos->prev()->next()=pos->next();
452 pos->next()=
glla().m_free_list;
453 glla().m_free_list=pos;
528 std::vector<state_in_block_pointer>
m_vec;
562 return m_vec.empty();
572 return m_vec.begin();
605 #ifdef CHECK_COMPLEXITY_GJ
607 template<
class LTS_TYPE>
610 assert(&partitioner.
m_states.front() <=
this);
611 assert(
this <= &partitioner.
m_states.back());
612 return std::to_string(
this - &partitioner.
m_states.front());
616 template<
class LTS_TYPE>
632 #ifndef SAVE_BLC_MEMORY
639 #ifndef SAVE_BLC_MEMORY
644 #ifdef CHECK_COMPLEXITY_GJ
647 template<
class LTS_TYPE>
655 return "Empty BLC slice at m_BLC_transitions[" + std::to_string(std::distance(partitioner.
m_BLC_transitions.begin(), my_end_same_BLC)) +
"]";
658 std::string result(
"BLC slice ");
662 result +=
" containing the ";
663 if (std::distance<BLC_list_const_iterator>(
start_same_BLC, my_end_same_BLC) > 1)
665 result += std::to_string(std::distance<BLC_list_const_iterator>(
start_same_BLC, my_end_same_BLC));
666 result +=
" transitions ";
669 result +=
"transition ";
675 result += partitioner.
m_transitions[*iter].debug_id_short(partitioner);
676 if (std::distance<BLC_list_const_iterator>(
start_same_BLC, my_end_same_BLC) > 4)
680 result += partitioner.
m_transitions[*iter].debug_id_short(partitioner);
683 iter = my_end_same_BLC - 3;
685 while (++iter != my_end_same_BLC)
688 result += partitioner.
m_transitions[*iter].debug_id_short(partitioner);
712 #ifdef CHECK_COMPLEXITY_GJ
715 template<
class LTS_TYPE>
721 return partitioner.
m_states[t.
from()].debug_id_short(partitioner) +
" -" +
723 partitioner.
m_states[t.
to()].debug_id_short(partitioner);
728 template<
class LTS_TYPE>
762 #ifdef CHECK_COMPLEXITY_GJ
764 template<
class LTS_TYPE>
767 assert(!partitioner.
m_blocks.empty());
768 assert(&partitioner.
m_blocks.front() <=
this);
769 assert(
this <= &partitioner.
m_blocks.back());
775 " (#" + std::to_string(std::distance(&partitioner.
m_blocks.front(),
this)) +
")";
786 constellation_type(
const std::vector<state_in_block_pointer>::iterator new_start,
const std::vector<state_in_block_pointer>::iterator new_end)
793 template<
class LTS_TYPE>
798 return "constellation " + std::to_string(
this - &partitioner.
m_constellations.front());
815template <
class LTS_TYPE>
824 #ifndef CO_SPLITTER_IN_BLC_LIST
825 typedef std::unordered_map<std::pair<block_index, label_index>,
transition_index> block_label_to_size_t_map;
861 #ifdef CO_SPLITTER_IN_BLC_LIST
894 return m_aut.num_action_labels();
905 #ifdef SAVE_BLC_MEMORY
926 #ifndef SAVE_BLC_MEMORY
939 #ifdef SAVE_BLC_MEMORY
963 #ifdef SAVE_BLC_MEMORY
982 void check_transitions(
const bool check_temporary_complexity_counters,
const bool check_block_to_constellation =
true)
const
991 assert(&*
m_states[t.
to()].start_incoming_transitions <= &t);
992 assert(&t <= &*std::prev(
m_aut.get_transitions().end()));
995 assert(&t <= &*std::prev(
m_states[t.
to() + 1].start_incoming_transitions));
1004 assert(
m_transitions[ti].transitions_per_block_to_constellation->start_same_BLC <= btc_ti);
1007 if (!check_block_to_constellation)
1016 if (blc.start_same_BLC != blc.start_marked_BLC)
1018 assert(blc.start_same_BLC < blc.start_marked_BLC);
1019 assert(blc.start_same_BLC <= std::prev(blc.start_marked_BLC));
1022 #ifndef SAVE_BLC_MEMORY
1023 assert(blc.start_same_BLC < blc.end_same_BLC);
1032 assert(blc.start_same_BLC <= btc_ti);
1034 assert(&blc == &*
m_transitions[ti].transitions_per_block_to_constellation);
1039 if (check_temporary_complexity_counters)
1041 #ifdef CHECK_COMPLEXITY_GJ
1047 0 ==
m_states[t.
from()].no_of_outgoing_inert_transitions), *
this);
1054 bool check_data_structures(
const std::string&
tag,
const bool initialisation=
false,
const bool check_temporary_complexity_counters=
true)
const
1056assert(!initialisation);
1062 for(std::vector<state_type_gj>::iterator si=
const_cast<std::vector<state_type_gj>&
>(
m_states).begin(); si<
m_states.cend(); si++)
1077 [*it->ref_BLC_transitions];
1080 assert(!initialisation );
1081 assert(
m_transitions[*it->ref_BLC_transitions].ref_outgoing_transitions==it);
1083 ((it+1)->start_same_saC==it->start_same_saC || (it+1)->start_same_saC<=it)) ||
1091 [*itt->ref_BLC_transitions];
1103 std::unordered_set<std::pair<label_index, constellation_index> > constellations_seen;
1109 const transition& t=
m_aut.get_transitions()[ *it->ref_BLC_transitions];
1113 if (constellations_seen.count(std::pair(
label,t_to_constellation))>0)
1116 const transition& old_t=
m_aut.get_transitions()[ *std::prev(it)->ref_BLC_transitions];
1120 constellations_seen.emplace(
label,t_to_constellation);
1124 if (!initialisation)
1146 #ifdef CHECK_COMPLEXITY_GJ
1153 assert(is->ref_state->block==bi);
1154 assert(is->ref_state->no_of_outgoing_inert_transitions==0);
1155 if (check_temporary_complexity_counters)
1163 assert(is->ref_state->block==bi);
1164 assert(is->ref_state->no_of_outgoing_inert_transitions>0);
1177 #ifndef SAVE_BLC_MEMORY
1178 assert(ind->start_same_BLC < ind->end_same_BLC);
1180 const transition& first_transition=
m_aut.get_transitions()[*(ind->start_same_BLC)];
1185 assert(
m_transitions[*i].transitions_per_block_to_constellation == ind);
1186 all_transitions.emplace(*i);
1197 if (check_temporary_complexity_counters)
1203 assert(initialisation || all_transitions.size()==
m_transitions.size());
1209 std::unordered_set<block_index> all_blocks;
1212 for (std::vector<state_in_block_pointer>::const_iterator constln_it=
m_constellations[ci].start_const_states; constln_it<
m_constellations[ci].end_const_states; )
1214 const block_index bi=constln_it->ref_state->block;
1216 assert(all_blocks.emplace(bi).second);
1217 constln_it =
m_blocks[bi].end_states;
1220 assert(all_blocks.size()==
m_blocks.size());
1228 assert(si==si->ref_state->ref_states_in_blocks);
1234 assert(
m_blocks[bi].contains_new_bottom_states);
1243 assert(first_bi != last_bi);
1274 const std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >* calM =
nullptr,
1275 const std::pair<BLC_list_iterator, BLC_list_iterator>* calM_elt =
nullptr,
1279 const block_label_to_size_t_map*
const block_label_to_cotransition =
nullptr
1292 #ifndef SAVE_BLC_MEMORY
1293 assert(ind->start_same_BLC < ind->end_same_BLC);
1295 const transition& first_t =
m_aut.get_transitions()[*ind->start_same_BLC];
1311 assert(all_transitions_in_BLC_are_inert);
1316 assert(!all_transitions_in_BLC_are_inert);
1317 if (0 ==
m_states[t.
from()].no_of_outgoing_inert_transitions)
1321 all_source_bottom_states.emplace(t.
from());
1332 bool eventual_instability_is_ok =
true;
1333 bool eventual_marking_is_ok =
true;
1334 if (!all_transitions_in_BLC_are_inert &&
1339 << (
m_branching ?
" bottom states have a transition in the " :
" states have a transition in the ")
1340 << ind->debug_id(*
this) <<
": transitions found from states";
1341 for (set_of_states_type::iterator asbc_it = all_source_bottom_states.begin() ; asbc_it != all_source_bottom_states.end() ; ++asbc_it) {
mCRL2log(
log::debug) <<
' ' << *asbc_it; }
1343 eventual_instability_is_ok =
false;
1349 eventual_marking_is_ok =
false;
1351 if (
m_blocks[bi].contains_new_bottom_states)
1375 if (!(eventual_instability_is_ok && eventual_marking_is_ok))
1377 mCRL2log(
log::debug) <<
" This is ok because block " << bi <<
" contains new bottom states.\n";
1378 eventual_instability_is_ok =
true;
1379 eventual_marking_is_ok =
true;
1382 if (!(eventual_instability_is_ok && eventual_marking_is_ok) &&
nullptr != calM && calM->begin() != calM->end())
1384 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >::const_iterator calM_iter = calM->begin();
1385 if (
nullptr != calM_elt)
1389 assert(calM->end() != calM_iter);
1390 if (calM_iter->first <= calM_elt->first && calM_elt->second <= calM_iter->second)
1396 if (calM_elt->first <= ind->start_same_BLC && ind->start_same_BLC <= calM_elt->second && !
points_into_BLC_set(calM_elt->second, *ind))
1398 mCRL2log(
log::debug) <<
" This is ok because the BLC set (block " << bi <<
" -" <<
m_aut.action_label(first_t.
label()) <<
"-> constellation " <<
m_blocks[
m_states[first_t.
to()].block].constellation <<
") is soon going to be a main splitter.\n";
1399 eventual_instability_is_ok =
true;
1400 eventual_marking_is_ok =
true;
1404 #ifdef CO_SPLITTER_IN_BLC_LIST
1408 if (main_splitter !=
m_blocks[bi].block_to_constellation.end())
1410 assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
1411 const transition& main_t =
m_aut.get_transitions()[*main_splitter->start_same_BLC];
1417 if (calM_elt->first <= main_splitter->start_same_BLC &&
1418 main_splitter->start_same_BLC <= calM_elt->second && !
points_into_BLC_set(calM_elt->second, *main_splitter))
1421 mCRL2log(
log::debug) <<
" This is ok because the BLC set (block " << bi <<
" -" <<
m_aut.action_label(first_t.
label()) <<
"-> constellation " << old_constellation <<
") is soon going to be a co-splitter.\n";
1422 eventual_instability_is_ok =
true;
1423 eventual_marking_is_ok =
true;
1431 if (
nullptr != block_label_to_cotransition)
1435 #ifndef SAVE_BLC_MEMORY
1436 assert(
m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->start_same_BLC <
m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->end_same_BLC);
1438 ind_iter =
m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->start_same_BLC;
1441 if (block_label_to_cotransition->end() != co_iter &&
null_transition != co_iter->second &&
m_transitions[co_iter->second].transitions_per_block_to_constellation == ind)
1444 mCRL2log(
log::debug) <<
" This is ok because the BLC set (block " << bi <<
" -" <<
m_aut.action_label(co_t.
label()) <<
"-> constellation " <<
m_blocks[
m_states[co_t.
to()].block].constellation <<
") is soon going to be a co-splitter.\n";
1445 eventual_instability_is_ok =
true;
1446 eventual_marking_is_ok =
true;
1455 for(; !(eventual_instability_is_ok && eventual_marking_is_ok) && calM->end() != calM_iter; ++calM_iter)
1457 if (calM_iter->first <= ind->start_same_BLC && ind->start_same_BLC <= calM_iter->second && !
points_into_BLC_set(calM_iter->second, *ind))
1459 mCRL2log(
log::debug) <<
" This is ok because the BLC set (block " << bi <<
" -" <<
m_aut.action_label(first_t.
label()) <<
"-> constellation " <<
m_blocks[
m_states[first_t.
to()].block].constellation <<
") is going to be a main splitter later.\n";
1460 eventual_instability_is_ok =
true;
1461 eventual_marking_is_ok =
true;
1465 #ifdef CO_SPLITTER_IN_BLC_LIST
1469 if (main_splitter !=
m_blocks[bi].block_to_constellation.end())
1471 assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
1472 const transition& main_t =
m_aut.get_transitions()[*main_splitter->start_same_BLC];
1477 if (calM_iter->first <= main_splitter->start_same_BLC &&
1478 main_splitter->start_same_BLC <= calM_iter->second && !
points_into_BLC_set(calM_iter->second, *main_splitter))
1481 mCRL2log(
log::debug) <<
" This is ok because the BLC set (block " << bi <<
" -" <<
m_aut.action_label(first_t.
label()) <<
"-> constellation " << old_constellation <<
") is soon going to be a co-splitter.\n";
1482 eventual_instability_is_ok =
true;
1483 eventual_marking_is_ok =
true;
1491 if (
nullptr != block_label_to_cotransition)
1495 #ifndef SAVE_BLC_MEMORY
1496 assert(
m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->start_same_BLC <
m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->end_same_BLC);
1498 ind_iter =
m_transitions[*std::prev(ind_iter)].transitions_per_block_to_constellation->start_same_BLC;
1501 if (block_label_to_cotransition->end() != co_iter &&
null_transition != co_iter->second &&
m_transitions[co_iter->second].transitions_per_block_to_constellation == ind)
1504 mCRL2log(
log::debug) <<
" This is ok because the BLC set (block " << bi <<
" -" <<
m_aut.action_label(co_t.
label()) <<
"-> constellation " <<
m_blocks[
m_states[co_t.
to()].block].constellation <<
") is going to be a co-splitter later.\n";
1505 eventual_instability_is_ok =
true;
1506 eventual_marking_is_ok =
true;
1515 #ifndef CO_SPLITTER_IN_BLC_LIST
1516 if (!(eventual_instability_is_ok && eventual_marking_is_ok) &&
nullptr != block_label_to_cotransition)
1518 block_label_to_size_t_map::const_iterator co_iter = block_label_to_cotransition->find(std::pair(
m_states[first_t.
from()].block,
label_or_divergence(first_t)));
1519 if (block_label_to_cotransition->end() != co_iter &&
null_transition != co_iter->second &&
m_transitions[co_iter->second].transitions_per_block_to_constellation == ind)
1521 mCRL2log(
log::debug) <<
" (This BLC set is registered as co-splitter but there is no corresponding main splitter.)\n";
1527 mCRL2log(
log::debug) <<
" (This is ok because the source block contains only 1 state.)\n";
1528 eventual_marking_is_ok =
true;
1530 assert(eventual_marking_is_ok);
1531 assert(eventual_instability_is_ok);
1540 ,
const block_label_to_size_t_map*
const block_label_to_cotransition =
nullptr
1551 if (i == blc_it.start_marked_BLC)
1573 #ifndef CO_SPLITTER_IN_BLC_LIST
1574 if (
nullptr != block_label_to_cotransition)
1576 const block_label_to_size_t_map::const_iterator co_tr = block_label_to_cotransition->find(std::pair(bi,
label_or_divergence(t)));
1577 if (co_tr != block_label_to_cotransition->end() && co_tr->second == *i)
1592 const block_label_to_size_t_map*
const block_label_to_cotransition =
nullptr,
1594 const bool initialisation=
false)
const
1596 assert(!initialisation);
1598 mCRL2log(
log::debug) <<
"========= PRINT DATASTRUCTURE: " << header <<
" =======================================\n";
1599 mCRL2log(
log::debug) <<
"++++++++++++++++++++ States ++++++++++++++++++++++++++++\n";
1606 std::vector<transition>::const_iterator end=(si+1==
m_states.size()?
m_aut.get_transitions().end():
m_states[si+1].start_incoming_transitions);
1607 for(std::vector<transition>::const_iterator it=
m_states[si].start_incoming_transitions; it!=end; ++it)
1618 const transition& t=
m_aut.get_transitions()[ *it->ref_BLC_transitions];
1621 mCRL2log(
log::debug) <<
" Ref states in blocks: " << std::distance<std::vector<state_type_gj>::const_iterator>(
m_states.cbegin(),
m_states[si].ref_states_in_blocks->ref_state) <<
". Must be " << si <<
".\n";
1624 mCRL2log(
log::debug) <<
"++++++++++++++++++++ Transitions ++++++++++++++++++++++++++++\n";
1629 <<
" -" <<
m_aut.action_label(t.
label()) <<
"-> "
1633 mCRL2log(
log::debug) <<
"++++++++++++++++++++ Blocks ++++++++++++++++++++++++++++\n";
1637 << (
m_branching ?
"):\n Bottom states: " :
"):\n States: ");
1638 for(std::vector<state_in_block_pointer>::const_iterator sit=
m_blocks[bi].start_bottom_states;
1639 sit!=
m_blocks[bi].start_non_bottom_states; ++sit)
1646 for(
typename std::vector<state_in_block_pointer>::const_iterator sit=
m_blocks[bi].start_non_bottom_states;
1647 sit!=
m_blocks[bi].end_states; ++sit)
1656 if (!initialisation)
1660 , block_label_to_cotransition
1667 mCRL2log(
log::debug) <<
"++++++++++++++++++++ Constellations ++++++++++++++++++++++++++++\n";
1672 for (std::vector<state_in_block_pointer>::const_iterator constln_it=
m_constellations[ci].start_const_states; constln_it<
m_constellations[ci].end_const_states; )
1674 const block_index bi=constln_it->ref_state->block;
1676 constln_it =
m_blocks[bi].end_states;
1686 mCRL2log(
log::debug) <<
"\n++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n";
1691 const transition& t=
m_aut.get_transitions()[ *pi->ref_BLC_transitions];
1695 const transition& t1=
m_aut.get_transitions()[ *pi->start_same_saC->ref_BLC_transitions];
1698 if (pi->start_same_saC->start_same_saC == pi)
1704 const transition& prev_t =
m_aut.get_transitions()[ *std::prev(pi)->ref_BLC_transitions];
1715 const transition& next_t =
m_aut.get_transitions()[ *std::next(pi)->ref_BLC_transitions];
1724 else if (pi->start_same_saC > pi ? pi->start_same_saC->start_same_saC > pi : pi->start_same_saC->start_same_saC < pi)
1733 mCRL2log(
log::debug) <<
"++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n";
1741 mCRL2log(
log::debug) <<
"\n========= END PRINT DATASTRUCTURE: " << header <<
" =======================================\n";
1759 const bool branching =
false,
1760 const bool preserve_divergence =
false)
1822 std::vector<transition> T;
1832 #ifndef SAVE_BLC_MEMORY
1833 assert(blc_ind.start_same_BLC < blc_ind.end_same_BLC);
1835 const transition& t=
m_aut.get_transitions()[*blc_ind.start_same_BLC];
1839 T.emplace_back(bi, t.
label(), new_to);
1843 m_aut.clear_transitions();
1848 m_aut.add_transition(t);
1854 if (
m_aut.has_state_info())
1857 std::vector<typename LTS_TYPE::state_label_t> new_labels(
num_eq_classes());
1860 for(std::size_t i=0; i<
m_aut.num_states(); ++i)
1865 new_labels[new_index]=new_labels[new_index]+
m_aut.state_label(i);
1873 m_aut.set_state_label(i, new_labels[i]);
1897 return std::to_string(t.
from()) +
" -" +
pp(
m_aut.action_label(t.
label())) +
"-> " + std::to_string(t.
to());
1913 return std::distance(
m_blocks[B].start_bottom_states,
m_blocks[B].end_states);
1923 typename std::vector<state_in_block_pointer>::iterator pos1,
1924 typename std::vector<state_in_block_pointer>::iterator pos2)
1932 pos1->ref_state->ref_states_in_blocks=pos1;
1933 pos2->ref_state->ref_states_in_blocks=pos2;
1937 typename std::vector<state_in_block_pointer>::iterator pos1,
1938 typename std::vector<state_in_block_pointer>::iterator pos2)
1950 typename std::vector<state_in_block_pointer>::iterator pos1,
1951 typename std::vector<state_in_block_pointer>::iterator pos2,
1952 typename std::vector<state_in_block_pointer>::iterator pos3)
1955 assert(pos2<pos3); assert(pos3<=pos1);
1968 pos3->
ref_state->ref_states_in_blocks=pos3;
1970 pos1->ref_state->ref_states_in_blocks=pos1;
1971 pos2->ref_state->ref_states_in_blocks=pos2;
1977 typename std::vector<state_in_block_pointer>::iterator pos1,
1978 typename std::vector<state_in_block_pointer>::iterator pos2,
1979 typename std::vector<state_in_block_pointer>::iterator pos3)
2024 typename std::vector<state_in_block_pointer>::iterator pos1,
2025 typename std::vector<state_in_block_pointer>::iterator pos2,
2036 assert(pos1 < pos2);
2039 std::make_signed<state_index>::type overlap = std::distance(pos2, pos1 + count);
2051 pos1->ref_state->ref_states_in_blocks=pos1;
2054 pos2->ref_state->ref_states_in_blocks=pos2;
2058 pos1->ref_state->ref_states_in_blocks=pos1;
2060 pos2->
ref_state->ref_states_in_blocks=pos2;
2063 for (std::vector<state_type_gj>::const_iterator si =
m_states.cbegin(); si <
m_states.cend(); ++si)
2065 assert(si==si->ref_states_in_blocks->ref_state);
2076 assert(ind->start_same_BLC <= old_pos);
2079 if (old_pos < ind->start_marked_BLC)
2082 assert(ind->start_same_BLC < ind->start_marked_BLC);
2084 assert(ind->start_same_BLC <= new_pos);
2087 if (old_pos < new_pos)
2090 m_transitions[*old_pos].ref_outgoing_transitions->ref_BLC_transitions = old_pos;
2091 assert(out_pos ==
m_transitions[*new_pos].ref_outgoing_transitions);
2092 out_pos->ref_BLC_transitions = new_pos;
2094 ind->start_marked_BLC--;
2100 assert(
m_transitions[*it].ref_outgoing_transitions->ref_BLC_transitions == it);
2101 assert(
m_transitions[*it].transitions_per_block_to_constellation->start_same_BLC <= it);
2112 std::vector<state_in_block_pointer>::iterator first_bottom_state_in_R,
2113 std::vector<state_in_block_pointer>::iterator last_bottom_state_in_R,
2115 #ifdef TRY_EFFICIENT_SWAP
2127 assert(
m_blocks[B].start_bottom_states <= first_bottom_state_in_R);
2128 assert(first_bottom_state_in_R <= last_bottom_state_in_R);
2129 assert(last_bottom_state_in_R <=
m_blocks[B].start_non_bottom_states);
2134 #ifdef CHECK_COMPLEXITY_GJ
2147 #ifdef CHECK_COMPLEXITY_GJ
2151 if (
m_blocks[B].start_bottom_states < first_bottom_state_in_R)
2154 std::distance(first_bottom_state_in_R, last_bottom_state_in_R)
2159 last_bottom_state_in_R =
m_blocks[B].start_bottom_states + std::distance(first_bottom_state_in_R, last_bottom_state_in_R);
2160 first_bottom_state_in_R =
m_blocks[B].start_bottom_states;
2163 assert(
m_blocks[B_new].start_bottom_states==first_bottom_state_in_R);
2164 m_blocks[B_new].start_non_bottom_states=last_bottom_state_in_R;
2166 for(std::vector<state_in_block_pointer>::iterator s_it=first_bottom_state_in_R; s_it<last_bottom_state_in_R; ++s_it)
2171 assert(B==s_it->ref_state->block);
2172 s_it->ref_state->block=B_new;
2173 assert(s_it->ref_state->ref_states_in_blocks==s_it);
2176 #ifdef TRY_EFFICIENT_SWAP
2179 const std::vector<state_in_block_pointer>::iterator BminR_start_bottom_states=last_bottom_state_in_R+R.size();
2180 const std::vector<state_in_block_pointer>::iterator BminR_start_non_bottom_states=
m_blocks[B].start_non_bottom_states+R.size();
2184 std::vector<state_in_block_pointer>::iterator move_next_R_non_bottom_state_to=last_bottom_state_in_R;
2185 std::vector<state_in_block_pointer>::iterator move_next_R_non_bottom_state_to_end=BminR_start_bottom_states;
2187 std::vector<state_in_block_pointer>::iterator move_next_BminR_bottom_state_to=
m_blocks[B].start_non_bottom_states;
2188 if (move_next_BminR_bottom_state_to<move_next_R_non_bottom_state_to_end)
2192 move_next_R_non_bottom_state_to_end=move_next_BminR_bottom_state_to;
2193 move_next_BminR_bottom_state_to=BminR_start_bottom_states;
2201 std::vector<state_in_block_pointer>::iterator take_next_R_non_bottom_state_from=BminR_start_non_bottom_states;
2202 #ifdef CHECK_COMPLEXITY_GJ
2203 std::vector<state_in_block_pointer>::const_iterator account_for_skipped_BminR_states=R.begin();
2205 for (; move_next_R_non_bottom_state_to<move_next_R_non_bottom_state_to_end;
2206 ++move_next_R_non_bottom_state_to, ++move_next_BminR_bottom_state_to)
2210 if (marking_value==move_next_BminR_bottom_state_to->ref_state->counter)
2219 while (assert(take_next_R_non_bottom_state_from<
m_blocks[B].end_states),
2220 marking_value!=take_next_R_non_bottom_state_from->ref_state->counter)
2222 #ifdef CHECK_COMPLEXITY_GJ
2225 assert(account_for_skipped_BminR_states<R.end());
2227 ++account_for_skipped_BminR_states;
2229 ++take_next_R_non_bottom_state_from;
2232 ++take_next_R_non_bottom_state_from;
2234 assert(marking_value==move_next_R_non_bottom_state_to->ref_state->counter);
2235 assert(B==move_next_R_non_bottom_state_to->ref_state->block);
2236 move_next_R_non_bottom_state_to->ref_state->block=B_new;
2241 for (; move_next_R_non_bottom_state_to<BminR_start_bottom_states; ++move_next_R_non_bottom_state_to)
2247 if (marking_value==move_next_R_non_bottom_state_to->ref_state->counter)
2255 while (assert(take_next_R_non_bottom_state_from<
m_blocks[B].end_states),
2256 marking_value!=take_next_R_non_bottom_state_from->ref_state->counter)
2258 #ifdef CHECK_COMPLEXITY_GJ
2261 assert(account_for_skipped_BminR_states<R.end());
2263 ++account_for_skipped_BminR_states;
2265 ++take_next_R_non_bottom_state_from;
2268 ++take_next_R_non_bottom_state_from;
2269 assert(marking_value==move_next_R_non_bottom_state_to->ref_state->counter);
2271 assert(B==move_next_R_non_bottom_state_to->ref_state->block);
2272 move_next_R_non_bottom_state_to->ref_state->block=B_new;
2283 std::vector<state_in_block_pointer>::const_iterator take_next_R_non_bottom_state_from=R.begin();
2284 for (; move_next_R_non_bottom_state_to<move_next_R_non_bottom_state_to_end;
2285 ++move_next_R_non_bottom_state_to, ++move_next_BminR_bottom_state_to)
2289 if (marking_value==move_next_BminR_bottom_state_to->ref_state->counter)
2298 while (assert(take_next_R_non_bottom_state_from<R.end()),
2299 take_next_R_non_bottom_state_from->ref_state->ref_states_in_blocks<BminR_start_non_bottom_states)
2302 assert(marking_value==take_next_R_non_bottom_state_from->ref_state->counter);
2303 assert((take_next_R_non_bottom_state_from->ref_state->ref_states_in_blocks<move_next_R_non_bottom_state_to
2304 ? B_new : B)==take_next_R_non_bottom_state_from->ref_state->block);
2305 ++take_next_R_non_bottom_state_from;
2308 ++take_next_R_non_bottom_state_from;
2310 assert(marking_value==move_next_R_non_bottom_state_to->ref_state->counter);
2311 assert(B==move_next_R_non_bottom_state_to->ref_state->block);
2312 move_next_R_non_bottom_state_to->ref_state->block=B_new;
2318 if (move_next_R_non_bottom_state_to<BminR_start_bottom_states)
2321 assert(move_next_R_non_bottom_state_to==
m_blocks[B].start_non_bottom_states);
2326 assert(BminR_start_non_bottom_states==move_next_BminR_bottom_state_to);
2329 for (; move_next_R_non_bottom_state_to<BminR_start_bottom_states; ++move_next_R_non_bottom_state_to)
2335 if (marking_value==move_next_R_non_bottom_state_to->ref_state->counter)
2343 while (assert(R.begin()<=take_next_R_non_bottom_state_from),
2344 assert(take_next_R_non_bottom_state_from<R.end()),
2345 take_next_R_non_bottom_state_from->ref_state->ref_states_in_blocks<BminR_start_non_bottom_states)
2350 assert(marking_value==take_next_R_non_bottom_state_from->ref_state->counter);
2351 assert((take_next_R_non_bottom_state_from->ref_state->ref_states_in_blocks<move_next_R_non_bottom_state_to
2352 ? B_new : B)==take_next_R_non_bottom_state_from->ref_state->block);
2353 ++take_next_R_non_bottom_state_from;
2356 ++take_next_R_non_bottom_state_from;
2357 assert(marking_value==move_next_R_non_bottom_state_to->ref_state->counter);
2359 assert(B==move_next_R_non_bottom_state_to->ref_state->block);
2360 move_next_R_non_bottom_state_to->ref_state->block=B_new;
2367 m_blocks[B_new].end_states=BminR_start_bottom_states;
2368 m_blocks[B].start_bottom_states=BminR_start_bottom_states;
2369 m_blocks[B].start_non_bottom_states=BminR_start_non_bottom_states;
2370 assert(
static_cast<std::make_signed<state_index>::type
>(R.size())==std::distance(
m_blocks[B_new].start_non_bottom_states,
m_blocks[B_new].end_states));
2372 m_blocks[B_new].end_states=last_bottom_state_in_R;
2373 m_blocks[B].start_bottom_states=last_bottom_state_in_R;
2381 assert(B==s.ref_state->block);
2382 s.ref_state->block=B_new;
2383 typename std::vector<state_in_block_pointer>::iterator pos=s.ref_state->ref_states_in_blocks;
2384 assert(pos>=
m_blocks[B].start_non_bottom_states);
2387 m_blocks[B].start_non_bottom_states++;
2390 assert(
m_blocks[B].start_bottom_states<=
m_blocks[B].start_non_bottom_states);
2406 if ((i1==i2)||(i2==i3))
2409 m_transitions[*i1].ref_outgoing_transitions->ref_BLC_transitions = i1;
2410 m_transitions[*i3].ref_outgoing_transitions->ref_BLC_transitions = i3;
2418 m_transitions[*i1].ref_outgoing_transitions->ref_BLC_transitions = i1;
2419 m_transitions[*i2].ref_outgoing_transitions->ref_BLC_transitions = i2;
2420 m_transitions[*i3].ref_outgoing_transitions->ref_BLC_transitions = i3;
2435 #ifdef SAVE_BLC_MEMORY
2440 assert(new_BLC_block->start_same_BLC <= new_BLC_block->start_marked_BLC);
2441 assert(old_BLC_block->start_same_BLC <= old_BLC_block->start_marked_BLC);
2443 assert(old_BLC_block->start_same_BLC <= old_position);
2444 #ifndef SAVE_BLC_MEMORY
2445 assert(old_position<old_BLC_block->end_same_BLC);
2446 assert(new_BLC_block->start_marked_BLC==new_BLC_block->end_same_BLC);
2447 assert(old_BLC_block->start_marked_BLC<=old_BLC_block->end_same_BLC);
2450 assert(old_to_constellation==
m_blocks[
m_states[
m_aut.get_transitions()[ti].to()].block].constellation);
2453 assert(
m_transitions[ti].transitions_per_block_to_constellation == old_BLC_block);
2454 assert(ti == *old_position);
2456 if (old_position>=old_BLC_block->start_marked_BLC)
2468 #ifdef SAVE_BLC_MEMORY
2469 old_BLC_block->start_marked_BLC=std::next(old_position);
2471 old_BLC_block->start_marked_BLC=old_BLC_block->end_same_BLC;
2474 assert(old_BLC_block->start_same_BLC<=old_position);
2475 assert(new_BLC_block->start_marked_BLC==old_BLC_block->start_same_BLC);
2476 if (old_position!=new_BLC_block->start_marked_BLC)
2478 std::swap(*old_position,*old_BLC_block->start_same_BLC);
2479 m_transitions[*old_position].ref_outgoing_transitions->ref_BLC_transitions=old_position;
2480 m_transitions[*old_BLC_block->start_same_BLC].ref_outgoing_transitions->ref_BLC_transitions = old_BLC_block->start_same_BLC;
2484 assert(old_position==old_BLC_block->start_same_BLC);
2486 #ifndef SAVE_BLC_MEMORY
2487 new_BLC_block->end_same_BLC=
2489 new_BLC_block->start_marked_BLC=++old_BLC_block->start_same_BLC;
2490 m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
2492 #ifdef SAVE_BLC_MEMORY
2498 const transition& old_t =
m_aut.get_transitions()[*old_BLC_block->start_same_BLC];
2503 return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
2518 assert(
m_states[t.
to()].block==index_block_B);
2519 assert(&
m_aut.get_transitions()[ti] == &t);
2521 assert(
m_blocks[from_block].block_to_constellation.check_linked_list());
2522 bool new_block_created =
false;
2525 assert(this_block_to_constellation!=
m_blocks[from_block].block_to_constellation.end());
2526 assert(this_block_to_constellation->start_same_BLC <=
m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions);
2528 assert(
m_blocks[from_block].contains_new_bottom_states ||
2530 m_transitions[ti].ref_outgoing_transitions->ref_BLC_transitions<this_block_to_constellation->start_marked_BLC);
2536 next_block_to_constellation=
m_blocks[from_block].block_to_constellation.begin();
2538 #ifndef SAVE_BLC_MEMORY
2539 assert(next_block_to_constellation->start_same_BLC<next_block_to_constellation->end_same_BLC);
2541 assert(
m_states[
m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].from()].block==index_block_B);
2542 assert(
m_aut.is_tau(
m_aut.apply_hidden_label_map(
m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].label())));
2543 if (next_block_to_constellation==this_block_to_constellation)
2548 next_block_to_constellation=
2549 m_blocks[from_block].block_to_constellation.
2551 this_block_to_constellation->start_same_BLC,
2552 this_block_to_constellation->start_same_BLC);
2553 #ifdef CHECK_COMPLEXITY_GJ
2554 next_block_to_constellation->work_counter = this_block_to_constellation->work_counter;
2560 assert(
m_states[
m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].to()].block==index_block_B);
2572 next_block_to_constellation=std::next(this_block_to_constellation);
2574 if (next_block_to_constellation==
m_blocks[from_block].block_to_constellation.end() ||
2575 (first_t = &
m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)],
2577 m_states[first_t->
to()].block!=index_block_B) ||
2582 next_block_to_constellation=
2583 m_blocks[from_block].block_to_constellation.
2584 emplace_after(this_block_to_constellation,
2585 this_block_to_constellation->start_same_BLC,
2586 this_block_to_constellation->start_same_BLC);
2587 #ifdef CHECK_COMPLEXITY_GJ
2588 next_block_to_constellation->work_counter = this_block_to_constellation->work_counter;
2590 new_block_created =
true;
2596 next_block_to_constellation, this_block_to_constellation
2597 #ifdef SAVE_BLC_MEMORY
2598 ,
m_blocks[index_block_B].constellation
2602 m_blocks[from_block].block_to_constellation.erase(this_block_to_constellation);
2607 return new_block_created;
2618 #ifdef SAVE_BLC_MEMORY
2624 assert(new_BLC_block->start_same_BLC <= new_BLC_block->start_marked_BLC);
2625 assert(old_BLC_block->start_same_BLC <= old_BLC_block->start_marked_BLC);
2627 assert(old_BLC_block->start_same_BLC <= old_position);
2628 #ifndef SAVE_BLC_MEMORY
2629 assert(old_position < old_BLC_block->end_same_BLC);
2630 assert(new_BLC_block->start_marked_BLC <= new_BLC_block->end_same_BLC);
2631 assert(old_BLC_block->start_marked_BLC <= old_BLC_block->end_same_BLC);
2634 assert(
m_transitions[ti].transitions_per_block_to_constellation == old_BLC_block);
2636 assert(ti == *old_position);
2637 if (old_position < old_BLC_block->start_marked_BLC)
2640 assert(old_BLC_block->start_same_BLC <= old_position);
2641 assert(new_BLC_block->start_marked_BLC <= old_BLC_block->start_same_BLC);
2643 new_BLC_block->start_marked_BLC++;
2648 assert(old_BLC_block->start_marked_BLC <= old_position);
2649 assert(old_BLC_block->start_same_BLC <= old_BLC_block->start_marked_BLC);
2651 old_BLC_block->start_marked_BLC++;
2653 m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
2654 #ifndef SAVE_BLC_MEMORY
2655 new_BLC_block->end_same_BLC=
2657 ++old_BLC_block->start_same_BLC;
2659 #ifdef SAVE_BLC_MEMORY
2664 const transition& old_t =
m_aut.get_transitions()[*old_BLC_block->start_same_BLC];
2665 return (
m_states[old_t.
from()].block!=old_from_block &&
2670 return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
2690 assert(
m_blocks[old_bi].block_to_constellation.check_linked_list());
2691 assert(
m_blocks[new_bi].block_to_constellation.check_linked_list());
2701 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
2704 assert(this_block_to_constellation==
m_blocks[old_bi].block_to_constellation.begin());
2705 new_BLC_block=
m_blocks[new_bi].block_to_constellation.begin();
2706 assert(new_BLC_block!=
m_blocks[new_bi].block_to_constellation.end());
2708 if (new_BLC_block->start_same_BLC<new_BLC_block->end_same_BLC)
2710 const transition& inert_t=
m_aut.get_transitions()[*new_BLC_block->start_same_BLC];
2716 assert(this_block_to_constellation->start_same_BLC==new_BLC_block->end_same_BLC);
2721 bool co_block_found=
false;
2724 const transition_index co_transition=*(this_block_to_constellation->start_same_BLC-1);
2731 new_BLC_block=
m_transitions[co_transition].transitions_per_block_to_constellation;
2732 co_block_found=
true;
2735 if (!co_block_found)
2742 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
2748 assert(this_block_to_constellation==
m_blocks[old_bi].block_to_constellation.begin());
2749 #ifdef CO_SPLITTER_IN_BLC_LIST
2759 #ifdef CO_SPLITTER_IN_BLC_LIST
2760 if (
m_blocks[new_bi].block_to_constellation.empty())
2763 #ifdef CO_SPLITTER_INBLC_LIST_VARIANT
2770 assert(
false==co_block_found);
2775 assert(old_constellation<new_constellation);
2777 if ((old_constellation==to_constln &&
2778 (old_co_splitter = std::next(this_block_to_constellation),
2781 (new_constellation == to_constln &&
2782 (old_co_splitter = std::prev(this_block_to_constellation),
2786 if (
m_blocks[old_bi].block_to_constellation.end()!=old_co_splitter)
2797 assert((old_constellation==to_constln && new_constellation==co_to_constln) ||
2798 (new_constellation == to_constln && old_constellation == co_to_constln));
2802 const transition_index temp_transition=*(old_co_splitter->start_same_BLC-1);
2809 new_position=
m_transitions[temp_transition].transitions_per_block_to_constellation;
2810 if (old_constellation==to_constln)
2817 co_block_found=
true;
2820 if (old_co_splitter->start_same_BLC<old_co_splitter->end_same_BLC)
2822 const transition& co_t=
m_aut.get_transitions()[*old_co_splitter->start_same_BLC];
2854 if (!co_block_found)
2857 assert(!
m_blocks[new_bi].block_to_constellation.empty());
2861 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
2864 new_position=perhaps_inert;
2866 if (perhaps_inert->start_same_BLC<perhaps_inert->end_same_BLC)
2868 const transition& p_i_t=
m_aut.get_transitions()[*perhaps_inert->start_same_BLC];
2874 new_position=perhaps_inert;
2884 new_position=
m_blocks[new_bi].block_to_constellation.begin();
2887 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
2890 const BLC_list_iterator old_BLC_start=this_block_to_constellation->start_same_BLC;
2891 new_BLC_block=
m_blocks[new_bi].block_to_constellation.emplace_after(new_position, old_BLC_start, old_BLC_start);
2892 #ifdef CHECK_COMPLEXITY_GJ
2893 new_BLC_block->work_counter=this_block_to_constellation->work_counter;
2898 new_BLC_block, this_block_to_constellation
2899 #ifdef SAVE_BLC_MEMORY
2900 , old_bi, to_constln
2905 if (last_element_removed)
2907 #ifdef CO_SPLITTER_IN_BLC_LIST
2926 m_blocks[old_bi].block_to_constellation.erase(this_block_to_constellation);
2931 remaining_transition= *(this_block_to_constellation->start_same_BLC);
2935 assert(
m_blocks[old_bi].block_to_constellation.check_linked_list());
2936 assert(
m_blocks[new_bi].block_to_constellation.check_linked_list());
2939 return remaining_transition;
2947 assert(
Rmarked == si.ref_state->counter);
2959 assert(
Rmarked!=si.ref_state->counter);
2987 const std::vector<state_in_block_pointer>::iterator first_unmarked_bottom_state,
2992 typedef enum { initializing, state_checking, aborted, aborted_after_initialisation,
2993 incoming_inert_transition_checking, outgoing_action_constellation_check } status_type;
2994 status_type U_status=state_checking;
2995 status_type R_status=initializing;
2997 std::vector<transition>::iterator current_U_incoming_transition_iterator;
2998 std::vector<transition>::iterator current_U_incoming_transition_iterator_end;
3002 std::vector<transition>::iterator current_R_incoming_transition_iterator;
3003 std::vector<transition>::iterator current_R_incoming_transition_iterator_end;
3004 std::vector<state_in_block_pointer>::iterator current_R_incoming_bottom_state_iterator =
m_blocks[B].start_bottom_states;
3005 std::vector<state_in_block_pointer>::iterator current_U_incoming_bottom_state_iterator = first_unmarked_bottom_state;
3008 assert(!
m_blocks[B].contains_new_bottom_states);
3013 assert(M_it <= splitter_end_unmarked_BLC);
3014 assert(splitter_end_unmarked_BLC <= splitter->start_marked_BLC);
3015 #ifndef SAVE_BLC_MEMORY
3016 assert(splitter->start_marked_BLC <= splitter->end_same_BLC);
3017 assert(splitter->start_same_BLC < splitter->end_same_BLC);
3021 assert(
m_states[
m_aut.get_transitions()[*splitter->start_same_BLC].from()].block == B);
3022 assert(current_R_incoming_bottom_state_iterator <= first_unmarked_bottom_state);
3023 assert(current_R_incoming_bottom_state_iterator < first_unmarked_bottom_state || !
m_R.
empty() || M_it < splitter_end_unmarked_BLC);
3024 assert(current_U_incoming_bottom_state_iterator <
m_blocks[B].start_non_bottom_states);
3026 const std::make_signed<state_index>::type max_R_nonbottom_size=
number_of_states_in_block(B)/2-std::distance(
m_blocks[B].start_bottom_states, first_unmarked_bottom_state);
3027 if (max_R_nonbottom_size <
static_cast<std::make_signed<state_index>::type
>(
m_R.
size()))
3030 R_status = (M_it == splitter_end_unmarked_BLC) ? aborted_after_initialisation : aborted;
3039 assert(
m_blocks[B].start_bottom_states<first_unmarked_bottom_state);
3040 assert(std::distance(
m_blocks[B].start_bottom_states, first_unmarked_bottom_state)<=std::distance(first_unmarked_bottom_state,
m_blocks[B].start_non_bottom_states));
3046 #ifdef TRY_EFFICIENT_SWAP
3051 else if (M_it==splitter_end_unmarked_BLC)
3055 R_status=state_checking;
3058 const std::make_signed<state_index>::type max_U_nonbottom_size=
number_of_states_in_block(B)/2-std::distance(first_unmarked_bottom_state,
m_blocks[B].start_non_bottom_states);
3059 if (max_U_nonbottom_size<0)
3061 assert(
static_cast<std::make_signed<state_index>::type
>(
number_of_states_in_block(B)/2)<std::distance(first_unmarked_bottom_state,
m_blocks[B].start_non_bottom_states));
3062 assert(aborted != R_status); assert(aborted_after_initialisation != R_status);
3063 U_status=aborted_after_initialisation;
3067 assert(
static_cast<std::make_signed<state_index>::type
>(
number_of_states_in_block(B)/2)>=std::distance(first_unmarked_bottom_state,
m_blocks[B].start_non_bottom_states));
3072 assert(first_unmarked_bottom_state<
m_blocks[B].start_non_bottom_states);
3073 assert(std::distance(first_unmarked_bottom_state,
m_blocks[B].start_non_bottom_states)<=std::distance(
m_blocks[B].start_bottom_states, first_unmarked_bottom_state));
3079 #ifdef TRY_EFFICIENT_SWAP
3087 #ifndef SAVE_BLC_MEMORY
3088 assert(splitter->start_same_BLC < splitter->end_same_BLC);
3090 const transition& first_t =
m_aut.get_transitions()[*splitter->start_same_BLC];
3094 if (initializing == R_status || aborted == R_status)
3110 assert(U_status!=aborted_after_initialisation || (R_status!=aborted && R_status!=aborted_after_initialisation));
3114 if (si.ref_state->block!=B || 0==si.ref_state->no_of_outgoing_inert_transitions)
3116 assert(
undefined==si.ref_state->counter);
3123 switch(si.ref_state->counter)
3131 case 0: assert(!
m_R.
find(si));
3132 #ifdef TRY_EFFICIENT_SWAP
3134 (si==current_U_outgoing_state && outgoing_action_constellation_check==U_status));
3146 #ifdef COUNT_R_U_STATUS_TIMES
3147 m_R_status_counter[R_status]++;
3149 if (incoming_inert_transition_checking==R_status)
3151 assert(current_R_incoming_transition_iterator<current_R_incoming_transition_iterator_end);
3154 assert(
m_aut.is_tau(
m_aut.apply_hidden_label_map(current_R_incoming_transition_iterator->label())));
3155 assert(
m_states[current_R_incoming_transition_iterator->to()].block==B);
3157 const transition& tr=*current_R_incoming_transition_iterator;
3170 assert(aborted_after_initialisation!=U_status);
3171 R_status=aborted_after_initialisation;
3172 goto R_handled_and_is_not_state_checking;
3178 ++current_R_incoming_transition_iterator;
3179 if (current_R_incoming_transition_iterator!=current_R_incoming_transition_iterator_end &&
3180 m_aut.is_tau(
m_aut.apply_hidden_label_map(current_R_incoming_transition_iterator->label())))
3182 goto R_handled_and_is_not_state_checking;
3184 R_status=state_checking;
3186 else if (state_checking==R_status)
3189 ? *current_R_incoming_bottom_state_iterator++
3196 current_R_incoming_transition_iterator_end=
m_aut.get_transitions().end();
3200 current_R_incoming_transition_iterator_end=std::next(s.
ref_state)->start_incoming_transitions;
3202 current_R_incoming_transition_iterator=s.
ref_state->start_incoming_transitions;
3203 if (current_R_incoming_transition_iterator!=current_R_incoming_transition_iterator_end &&
3204 m_aut.is_tau(
m_aut.apply_hidden_label_map(current_R_incoming_transition_iterator->label())))
3206 R_status=incoming_inert_transition_checking;
3207 goto R_handled_and_is_not_state_checking;
3210 else if (initializing!=R_status)
3212 assert(aborted_after_initialisation==R_status ||
3214 goto R_handled_and_is_not_state_checking;
3219 assert(M_it<splitter_end_unmarked_BLC);
3225 if (0==si.
ref_state->no_of_outgoing_inert_transitions)
3228 assert(
m_blocks[B].start_bottom_states<=si.ref_state->ref_states_in_blocks);
3229 assert(si.
ref_state->ref_states_in_blocks<first_unmarked_bottom_state);
3235 assert(
m_blocks[B].start_non_bottom_states<=si.ref_state->ref_states_in_blocks);
3243 assert(aborted_after_initialisation!=U_status);
3245 goto R_handled_and_is_not_state_checking;
3250 if (M_it!=splitter_end_unmarked_BLC)
3252 goto R_handled_and_is_not_state_checking;
3255 R_status=state_checking;
3257 assert(state_checking==R_status);
3258 if (current_R_incoming_bottom_state_iterator==first_unmarked_bottom_state &&
m_R.
todo_is_empty())
3262 assert(0 < std::distance(
m_blocks[B].start_bottom_states, first_unmarked_bottom_state) +
m_R.
size());
3265 #ifdef TRY_EFFICIENT_SWAP
3272 return block_index_of_R;
3274 R_handled_and_is_not_state_checking:
3275 assert(state_checking!=R_status || current_R_incoming_bottom_state_iterator!=first_unmarked_bottom_state || !
m_R.
todo_is_empty());
3280 if (si.ref_state->block!=B || 0==si.ref_state->no_of_outgoing_inert_transitions)
3282 assert(
undefined==si.ref_state->counter);
3289 switch(si.ref_state->counter)
3297 case 0: assert(!
m_R.
find(si));
3298 #ifdef TRY_EFFICIENT_SWAP
3300 (si==current_U_outgoing_state && outgoing_action_constellation_check==U_status));
3312 #ifdef COUNT_R_U_STATUS_TIMES
3313 m_U_status_counter[U_status]++;
3315 if (incoming_inert_transition_checking==U_status)
3319 assert(current_U_incoming_transition_iterator<current_U_incoming_transition_iterator_end);
3320 assert(
m_aut.is_tau(
m_aut.apply_hidden_label_map(current_U_incoming_transition_iterator->label())));
3325 assert(
m_states[current_U_incoming_transition_iterator->to()].block==B);
3326 current_U_incoming_transition_iterator++;
3328 if (current_U_outgoing_state.
ref_state->block==B && !(
m_preserve_divergence && std::prev(current_U_incoming_transition_iterator)->from()==std::prev(current_U_incoming_transition_iterator)->to()))
3330 assert(!
m_U.
find(current_U_outgoing_state));
3337 current_U_outgoing_state.
ref_state->counter=current_U_outgoing_state.
ref_state->no_of_outgoing_inert_transitions-1;
3344 assert(current_U_outgoing_state.
ref_state->counter>0);
3345 current_U_outgoing_state.
ref_state->counter--;
3349 if (current_U_outgoing_state.
ref_state->counter==0)
3351 if (initializing==R_status || aborted==R_status)
3354 current_U_outgoing_transition_iterator=current_U_outgoing_state.
ref_state->start_outgoing_transitions;
3358 assert(current_U_outgoing_transition_iterator<current_U_outgoing_transition_iterator_end);
3359 assert(
m_states.begin()+
m_aut.get_transitions()[*current_U_outgoing_transition_iterator->ref_BLC_transitions].from()==current_U_outgoing_state.
ref_state);
3360 U_status=outgoing_action_constellation_check;
3361 goto U_handled_and_is_not_state_checking;
3373 assert(0<=*out_it->ref_BLC_transitions);
3374 assert(*out_it->ref_BLC_transitions<
m_aut.num_transitions());
3375 assert(
m_transitions[*out_it->ref_BLC_transitions].ref_outgoing_transitions==out_it);
3376 const transition& t=
m_aut.get_transitions()[ *out_it->ref_BLC_transitions];
3382 assert(out_it->ref_BLC_transitions>=splitter_end_unmarked_BLC);
3383 assert(splitter->start_same_BLC<=out_it->ref_BLC_transitions);
3392 assert(aborted!=R_status); assert(aborted_after_initialisation!=R_status);
3393 U_status=aborted_after_initialisation;
3394 goto U_handled_and_is_not_state_checking;
3398 else assert(
m_R.
find(current_U_outgoing_state));
3400 if (current_U_incoming_transition_iterator!=current_U_incoming_transition_iterator_end &&
3401 m_aut.is_tau(
m_aut.apply_hidden_label_map(current_U_incoming_transition_iterator->label())))
3403 assert(incoming_inert_transition_checking==U_status);
3404 goto U_handled_and_is_not_state_checking;
3406 U_status=state_checking;
3408 else if (state_checking==U_status)
3414 ? *current_U_incoming_bottom_state_iterator++
3419 current_U_incoming_transition_iterator=s.
ref_state->start_incoming_transitions;
3420 current_U_incoming_transition_iterator_end=(std::next(s.
ref_state)>=
m_states.end() ?
m_aut.get_transitions().end() : std::next(s.
ref_state)->start_incoming_transitions);
3421 if (current_U_incoming_transition_iterator!=current_U_incoming_transition_iterator_end &&
3422 m_aut.is_tau(
m_aut.apply_hidden_label_map(current_U_incoming_transition_iterator->label())))
3424 U_status=incoming_inert_transition_checking;
3425 goto U_handled_and_is_not_state_checking;
3428 else if (aborted_after_initialisation==U_status)
3430 goto U_handled_and_is_not_state_checking;
3434 assert(outgoing_action_constellation_check==U_status);
3436 assert(current_U_outgoing_transition_iterator!=current_U_outgoing_transition_iterator_end);
3440 #ifdef CHECK_COMPLEXITY_GJ
3444 for (
outgoing_transitions_it out_it=current_U_outgoing_transition_iterator; out_it<current_U_outgoing_transition_iterator->start_same_saC; )
3453 *current_U_outgoing_transition_iterator->ref_BLC_transitions];
3454 current_U_outgoing_transition_iterator=current_U_outgoing_transition_iterator->start_same_saC;
3455 ++current_U_outgoing_transition_iterator;
3463 #ifdef TRY_EFFICIENT_SWAP
3466 current_U_outgoing_state.
ref_state->counter=std::numeric_limits<std::make_signed<transition_index>::type>
::max();
3467 assert(0!=current_U_outgoing_state.
ref_state->counter);
3473 else if (current_U_outgoing_transition_iterator==current_U_outgoing_transition_iterator_end)
3475 assert(!
m_U.
find(current_U_outgoing_state));
3481 assert(aborted!=R_status); assert(aborted_after_initialisation!=R_status);
3482 U_status=aborted_after_initialisation;
3483 goto U_handled_and_is_not_state_checking;
3488 goto U_handled_and_is_not_state_checking;
3491 if (current_U_incoming_transition_iterator!=current_U_incoming_transition_iterator_end &&
3492 m_aut.is_tau(
m_aut.apply_hidden_label_map(current_U_incoming_transition_iterator->label())))
3494 U_status = incoming_inert_transition_checking;
3495 goto U_handled_and_is_not_state_checking;
3497 U_status=state_checking;
3499 assert(state_checking==U_status);
3504 assert(0 < std::distance(first_unmarked_bottom_state,
m_blocks[B].start_non_bottom_states) +
m_U.
size());
3507 #ifdef TRY_EFFICIENT_SWAP
3516 U_handled_and_is_not_state_checking:
3517 assert(state_checking!=U_status || current_U_incoming_bottom_state_iterator!=
m_blocks[B].start_non_bottom_states || !
m_U.
todo_is_empty());
3541 assert(0 == si->no_of_outgoing_inert_transitions);
3542 assert(!
m_blocks[bi].contains_new_bottom_states);
3544 m_blocks[bi].start_non_bottom_states++;
3551 std::vector<state_in_block_pointer>::iterator first_unmarked_bottom_state,
3562 const bool split_off_new_bottom_states =
true)
3579 assert(bi == R_block || B == R_block);
3586 const std::vector<state_in_block_pointer>::iterator start_new_bottom_states=
m_blocks[R_block].start_non_bottom_states;
3588 bool skip_transitions_in_splitter =
false;
3589 assert(
m_blocks[bi].block_to_constellation.begin() ==
m_blocks[bi].block_to_constellation.end());
3590 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
3603 assert(perhaps_inert_ind!=
m_blocks[B].block_to_constellation.end());
3604 m_blocks[bi].block_to_constellation.emplace_front(perhaps_inert_ind->start_same_BLC, perhaps_inert_ind->start_same_BLC);
3605 assert(!
m_blocks[bi].block_to_constellation.empty());
3608 #ifdef CO_SPLITTER_IN_BLC_LIST
3611 if (split_off_new_bottom_states && bi == R_block)
3615 #ifdef CO_SPLITTER_IN_BLC_LIST
3620 assert(to_constln == old_constellation || to_constln ==
m_constellations.size() - 1);
3624 m_blocks[R_block].block_to_constellation.emplace_after(splitter, splitter->end_same_BLC, splitter->end_same_BLC)
3628 m_blocks[R_block].block_to_constellation.splice_to_after(
3630 m_blocks[R_block].block_to_constellation.begin(),
3632 m_blocks[R_block].block_to_constellation.end(),
3634 m_blocks[B].block_to_constellation, splitter);
3635 skip_transitions_in_splitter =
true;
3638 for(std::vector<state_in_block_pointer>::iterator ssi=
m_blocks[bi].start_bottom_states;
3646 assert(s.
block == bi);
3653 assert(
m_states.begin()+
m_aut.get_transitions()[*ti->ref_BLC_transitions].from()==ssi->ref_state);
3657 if (!skip_transitions_in_splitter ||
m_transitions[*ti->ref_BLC_transitions].transitions_per_block_to_constellation != splitter)
3671 #ifdef CO_SPLITTER_IN_BLC_LIST
3672 (void) old_remaining_transition;
3674 update_block_label_to_cotransition(B, bi, *ti->ref_BLC_transitions, old_remaining_transition);
3682 assert(ssi >=
m_blocks[R_block].start_non_bottom_states);
3684 bool non_bottom_state_becomes_bottom_state =
true;
3690 const transition& t=
m_aut.get_transitions()[ *ti->ref_BLC_transitions];
3699 if (R_to_U_tau_splitter ==
m_blocks[R_block].block_to_constellation.end())
3701 #ifndef SAVE_BLC_MEMORY
3707 assert(R_to_U_tau_splitter == new_splitter);
3710 R_to_U_tau_splitter = new_splitter;
3716 non_bottom_state_becomes_bottom_state=
false;
3720 if (non_bottom_state_becomes_bottom_state)
3723 assert(
m_blocks[R_block].block_to_constellation.end() != R_to_U_tau_splitter);
3729 if (bi != R_block &&
m_blocks[R_block].start_non_bottom_states <
m_blocks[R_block].end_states)
3731 const std::vector<transition>::iterator it_end = std::next(ssi->ref_state)>=
m_states.end() ?
m_aut.get_transitions().end() : std::next(ssi->ref_state)->start_incoming_transitions;
3738 assert(
m_states.begin()+t.
to()==ssi->ref_state);
3744 const std::vector<state_type_gj>::iterator
from(
m_states.begin()+t.
from());
3750 if (R_to_U_tau_splitter ==
m_blocks[R_block].block_to_constellation.end())
3756 assert(R_to_U_tau_splitter == new_splitter);
3759 R_to_U_tau_splitter = new_splitter;
3764 if (
from->no_of_outgoing_inert_transitions==0)
3773 assert(
m_blocks[R_block].start_bottom_states <
m_blocks[R_block].start_non_bottom_states);
3774 #ifdef CO_SPLITTER_IN_BLC_LIST_VARIANT
3781 if (perhaps_inert_ind->start_same_BLC==perhaps_inert_ind->end_same_BLC)
3783 m_blocks[bi].block_to_constellation.erase(perhaps_inert_ind);
3787 #ifdef CO_SPLITTER_IN_BLC_LIST
3790 m_blocks[B].block_to_constellation.erase(*it);
3796 assert(B_it.start_same_BLC < B_it.end_same_BLC);
3800 assert(bi_it.start_same_BLC < bi_it.end_same_BLC);
3805 #ifdef CHECK_COMPLEXITY_GJ
3810 for (
typename std::vector<state_in_block_pointer>::iterator s=
m_blocks[bi].start_bottom_states;
3815 const std::vector<transition>::iterator in_ti_end = std::next(s->ref_state)>=
m_states.end() ?
m_aut.get_transitions().end() : std::next(s->ref_state)->start_incoming_transitions;
3818 if (!
m_aut.is_tau(
m_aut.apply_hidden_label_map(ti->label())))
break;
3831 for (std::vector<state_in_block_pointer>::iterator s=
m_blocks[B].start_bottom_states;
3837 const std::vector<transition>::iterator in_ti_end=std::next(s->ref_state)>=
m_states.end() ?
m_aut.get_transitions().end() : std::next(s->ref_state)->start_incoming_transitions;
3840 if (!
m_aut.is_tau(
m_aut.apply_hidden_label_map(ti->label())))
break;
3854 for (
typename std::vector<state_in_block_pointer>::iterator s=
m_blocks[bi].start_bottom_states;
3860 const std::vector<transition>::iterator in_ti_end = std::next(s->ref_state)>=
m_states.end() ?
m_aut.get_transitions().end() : std::next(s->ref_state)->start_incoming_transitions;
3863 if (!
m_aut.is_tau(
m_aut.apply_hidden_label_map(ti->label())))
break;
3874 for (
typename std::vector<state_in_block_pointer>::iterator s=
m_blocks[B].start_bottom_states;
3879 const std::vector<transition>::iterator in_ti_end = std::next(s->ref_state)>=
m_states.end() ?
m_aut.get_transitions().end() : std::next(s->ref_state)->start_incoming_transitions;
3882 if (!
m_aut.is_tau(
m_aut.apply_hidden_label_map(ti->label())))
break;
3899 if (split_off_new_bottom_states && start_new_bottom_states <
m_blocks[R_block].start_non_bottom_states)
3903 assert(
m_blocks[R_block].block_to_constellation.end() != R_to_U_tau_splitter);
3907 if (start_new_bottom_states ==
m_blocks[R_block].start_bottom_states)
3911 new_bottom_block = R_block;
3919 const BLC_list_iterator splitter_end_unmarked_BLC = R_to_U_tau_splitter->start_same_BLC;
3922 , splitter_end_unmarked_BLC
3925 assert(std::distance(start_new_bottom_states,
m_blocks[R_block].start_non_bottom_states) ==
3926 std::distance(
m_blocks[R_block].start_bottom_states, first_unmarked_bottom_state));
3927 assert(
m_blocks[R_block].start_bottom_states < first_unmarked_bottom_state);
3928 assert(first_unmarked_bottom_state <
m_blocks[R_block].start_non_bottom_states);
3929 new_bottom_block =
splitB(R_to_U_tau_splitter, first_unmarked_bottom_state,
3930 splitter_end_unmarked_BLC,
3934 update_block_label_to_cotransition,
3938 if (R_block == new_bottom_block)
3943 assert(0 <= new_bottom_block); assert(new_bottom_block <
m_blocks.size());
3944 assert(!
m_blocks[new_bottom_block].contains_new_bottom_states);
3946 m_blocks[new_bottom_block].contains_new_bottom_states =
true;
3949 else if (
m_blocks[R_block].block_to_constellation.end() != R_to_U_tau_splitter)
3999 const std::vector<label_index>& todo_stack)
const
4005 sum=sum+action_counter[index];
4006 action_counter[index]=n;
4112 ?
"divergence-preserving branching "
4115 <<
"bisimulation partitioner created for " <<
m_aut.num_states()
4116 <<
" states and " <<
m_aut.num_transitions() <<
" transitions (using the experimental algorithm GJ2024).\n";
4118 #ifdef CHECK_COMPLEXITY_GJ
4146 std::vector<label_index> todo_stack_actions;
4154 todo_stack_actions.push_back(
m_aut.tau_label_index());
4155 count_transitions_per_action[
m_aut.tau_label_index()] = 1;
4166 todo_stack_actions.push_back(
label);
4172 assert(
m_aut.is_tau(todo_stack_actions.front()));
4173 --count_transitions_per_action[
m_aut.tau_label_index()];
4185 assert(0 <= c); assert(c <
m_aut.num_transitions());
4199 if (start_index == end_index)
4205 assert(start_index < end_index);
4210 current_BLC->start_marked_BLC = start_index;
4216 m_transitions[*start_index].transitions_per_block_to_constellation = current_BLC;
4218 while (++start_index < end_index);
4230 std::vector<transition_index> count_outgoing_transitions_per_state(
m_aut.num_states(), 0);
4235 count_outgoing_transitions_per_state[t.
from()]++;
4253 m_states[s].start_outgoing_transitions = current_outgoing_transitions +
m_states[s].no_of_outgoing_inert_transitions;
4254 current_outgoing_transitions += count_outgoing_transitions_per_state[s];
4255 count_outgoing_transitions_per_state[s] = 0;
4272 m_transitions[*ti].ref_outgoing_transitions =
m_states[t.
from()].start_outgoing_transitions + count_outgoing_transitions_per_state[t.
from()];
4274 m_transitions[*ti].ref_outgoing_transitions->ref_BLC_transitions = ti;
4275 ++count_outgoing_transitions_per_state[t.
from()];
4281 assert(current_state + 1 == 0);
4284 for(std::vector<transition>::iterator it=
m_aut.get_transitions().begin(); it!=
m_aut.get_transitions().end(); it++)
4289 if (t.
to()!=current_state)
4296 m_states[i].start_incoming_transitions=it;
4298 current_state=t.
to();
4305 m_states[i].start_incoming_transitions=
m_aut.get_transitions().end();
4313 const transition& t =
m_aut.get_transitions()[*it->ref_BLC_transitions];
4322 const transition& t =
m_aut.get_transitions()[*it->ref_BLC_transitions];
4324 if (current_state == t.
from() && current_label == new_label)
4327 it->start_same_saC = current_end_same_saC;
4332 current_state = t.
from();
4333 current_label = new_label;
4334 current_end_same_saC->start_same_saC = std::next(it);
4335 current_end_same_saC = it;
4344 for (std::vector<state_type_gj>::iterator i=
m_states.begin(); i<
m_states.end(); ++i)
4348 if (0<i->no_of_outgoing_inert_transitions)
4351 upper_i->ref_state=i;
4352 i->ref_states_in_blocks=upper_i;
4356 lower_i->ref_state=i;
4357 i->ref_states_in_blocks=lower_i;
4361 assert(lower_i == upper_i);
4363 m_blocks[0].start_non_bottom_states = lower_i;