17#ifndef LIBLTS_BISIM_GJ_H
18#define LIBLTS_BISIM_GJ_H
25#define INIT_WITHOUT_BLC_SETS
29#include "mcrl2/lts/detail/liblts_scc.h"
30#include "mcrl2/lts/detail/liblts_merge.h"
31#include "mcrl2/lts/detail/check_complexity.h"
32#include "mcrl2/lts/detail/fixed_vector.h"
33#include "mcrl2/lts/detail/simple_list.h"
34#define linked_list simple_list
43template <
class LTS_TYPE>
class bisim_partitioner_gj;
121template <
class CONTAINER>
122static inline void clear(CONTAINER& c)
124 if (c.size()>1000) { c=CONTAINER(); }
else { c.clear(); }
187 return ref_state==other.ref_state;
192 return ref_state!=other.ref_state;
208 return std::find(m_vec.begin(), m_vec.end(), s)!=m_vec.end();
218 return m_vec.size()==m_todo_indicator;
229 void swap_vec(std::vector<state_in_block_pointer>& other_vec)
231 m_vec.swap(other_vec);
242 return m_vec.empty();
247 return m_vec.begin();
262 return m_vec.data() + m_vec.size();
267 return m_vec.front();
275 void reserve(std::vector<state_in_block_pointer>::size_type new_cap)
277 m_vec.reserve(new_cap);
284 return m_vec.begin();
295 m_vec.insert(m_vec.end(), begin, end);
301 bisimulation_gj::clear(m_vec);
329 template<
class LTS_TYPE>
332 assert(partitioner.m_states.data()<=
this);
333 assert(
this<partitioner.m_states.data_end());
334 return std::to_string(
this-partitioner.m_states.data());
338 template<
class LTS_TYPE>
339 std::string
debug_id(
const bisim_partitioner_gj<LTS_TYPE>& partitioner)
const
341 return "state " + debug_id_short(partitioner);
344 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
413 template<
class LTS_TYPE>
414 std::string
debug_id(
const bisim_partitioner_gj<LTS_TYPE>& partitioner,
421 assert(
end_same_BLC<=partitioner.m_BLC_transitions.data_end());
422 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 return "Empty "+result;
427 result +=
" from "+(
nullptr==from_block ? partitioner.m_states[partitioner.m_aut.get_transitions()[*start_same_BLC].from()].block : from_block)->debug_id(partitioner);
429 result += partitioner.m_states[partitioner.m_aut.get_transitions()[*start_same_BLC].to()].block->c.onstellation->debug_id(partitioner);
430 result +=
" containing the ";
433 result+=std::to_string(std::distance(start_same_BLC, end_same_BLC));
434 result +=
" transitions ";
438 result +=
"transition ";
445 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
449 result += start_marked_BLC == iter ?
" | " :
", ";
450 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
451 result += std::next(iter) == start_marked_BLC ?
" | ..."
452 : (!is_stable() && start_marked_BLC>std::next(iter) && start_marked_BLC<=end_same_BLC-3 ?
", ..|.." :
", ...");
457 result += start_marked_BLC == iter ?
" | " :
", ";
458 result += partitioner.m_transitions[*iter].debug_id_short(partitioner);
467 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
488 template<
class LTS_TYPE>
491 assert(partitioner.m_transitions.data()<=
this);
492 assert(
this<partitioner.m_transitions.data_end());
493 const transition& t=partitioner.m_aut.get_transitions()
494 [
this-partitioner.m_transitions.data()];
495 return partitioner.m_states[t
.from()].debug_id_short(partitioner) +
" -" +
496 pp(partitioner.m_aut.action_label(t
.label())) +
"-> " +
497 partitioner.m_states[t
.to()].debug_id_short(partitioner);
502 template<
class LTS_TYPE>
503 std::string
debug_id(
const bisim_partitioner_gj<LTS_TYPE>& partitioner)
const
505 return "transition " + debug_id_short(partitioner);
508 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
611 btc_R test_should_be_empty_BLC_list=
btc_R(); assert(
nullptr==test_should_be_empty_BLC_list.R);
612 if constexpr (
sizeof(test_should_be_empty_BLC_list.R)!=
613 sizeof(test_should_be_empty_BLC_list.to_constellation))
617 if (test_should_be_empty_BLC_list.to_constellation.empty() &&
618 test_should_be_empty_BLC_list.to_constellation==
627 new (&test_should_be_empty_BLC_list)
linked_list<BLC_indicators>();
655 sta
(start_non_bottom
),
659 { assert(start_bottom<=start_non_bottom); assert(start_non_bottom<=end);
663 template<
class LTS_TYPE>
664 std::string
debug_id(
const bisim_partitioner_gj<LTS_TYPE>& partitioner)
const
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)
698 template<
class LTS_TYPE>
699 std::string
debug_id(
const bisim_partitioner_gj<LTS_TYPE>& partitioner)
const
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
725template <
class LTS_TYPE>
726class bisim_partitioner_gj
778 (
typename LTS_TYPE::labels_size_type l)
808 m_aut.is_tau(result))
810 return divergent_label;
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)
874 block_type*
const b=m_states[t.from()].block;
876 const label_index t_label = label_or_divergence(t);
878 for(
const BLC_indicators& blc: b->block.to_constellation)
880 if (!blc.is_stable())
882 assert(blc.start_same_BLC<=blc.start_marked_BLC);
883 assert(blc.start_marked_BLC<=blc.end_same_BLC);
885 assert(blc.start_same_BLC<blc.end_same_BLC);
886 transition& first_t = m_aut.get_transitions()[*blc.start_same_BLC];
887 assert(b == m_states[first_t.from()].block);
888 if (t_label == label_or_divergence(first_t) &&
889 m_states[first_t.to()].block->c.onstellation ==
890 m_states[t.to()].block->c.onstellation)
892 assert(!found); assert(blc.start_same_BLC <= btc_ti);
893 assert(btc_ti<blc.end_same_BLC);
894 assert(&blc == &*m_transitions[ti].transitions_per_block_to_constellation);
899 if (check_temporary_complexity_counters)
901 block_type*
const targetb = m_states[t.to()].block;
902 const unsigned max_sourceB = check_complexity::log_n-
903 check_complexity::ilog2(number_of_states_in_block(*b));
904 const unsigned max_targetC = check_complexity::log_n-
905 check_complexity::ilog2(number_of_states_in_constellation
906 (*targetb->c.onstellation));
907 const unsigned max_targetB = check_complexity::log_n-
908 check_complexity::ilog2(number_of_states_in_block(*targetb));
910 no_temporary_work(max_sourceB, max_targetC, max_targetB,
912 0==m_states[t.from()].no_of_outgoing_block_inert_transitions),
925 bool check_data_structures(
const std::string& tag,
const bool initialisation=
false,
const bool check_temporary_complexity_counters=
true)
const
928 assert(m_states.size()==m_aut.num_states());
929 assert(m_states_in_blocks.size()==m_aut.num_states());
930 assert(m_transitions.size()==m_aut.num_transitions());
931 assert(m_outgoing_transitions.size()==m_aut.num_transitions());
932 assert(m_BLC_transitions.size()==m_aut.num_transitions());
935 for (fixed_vector<state_type_gj>::iterator si=
936 const_cast<fixed_vector<state_type_gj>&>(m_states).begin();
937 si<m_states.cend(); si++)
939 const state_type_gj& s=*si;
941 assert(s.counter==undefined);
942 assert(s.block->start_bottom_states< s.block->sta.rt_non_bottom_states);
943 assert(s.block->sta.rt_non_bottom_states<=s.block->end_states);
946 assert(std::find(s.block->start_bottom_states,
948 state_in_block_pointer(si))!=s.block->end_states);
950 assert(s.ref_states_in_blocks->ref_state==si);
955 const std::vector<transition>::const_iterator end_it1=
956 std::next(si)>=m_states.end() ? m_aut.get_transitions().end()
957 : std::next(si)->start_incoming_transitions;
958 for (std::vector<transition>::const_iterator
959 it=s.start_incoming_transitions; it!=end_it1; ++it)
961 const transition& t=*it;
962 if (m_aut.is_tau(m_aut_apply_hidden_label_map(t.label())))
979 std::unordered_set<std::pair<label_index,
const constellation_type*> >
984 const outgoing_transitions_const_it end_it2=
985 std::next(si)>=m_states.end() ? m_outgoing_transitions.cend()
986 : std::next(si)->start_outgoing_transitions;
987 for(outgoing_transitions_const_it it=s.start_outgoing_transitions;
990 const transition& t=m_aut.get_transitions()[!initialisation
991 ? *it->ref.BLC_transitions : it->ref.transitions];
992 assert(m_states.cbegin()+t.from()==si);
993 assert(m_transitions[!initialisation ? *it->ref.BLC_transitions
994 : it->ref.transitions].ref_outgoing_transitions==it);
995 assert((it->start_same_saC>it &&
996 it->start_same_saC<m_outgoing_transitions.end() &&
997 ((it+1)->start_same_saC==it->start_same_saC ||
998 (it+1)->start_same_saC<=it)) ||
999 (it->start_same_saC<=it &&
1000 (it+1==m_outgoing_transitions.end() ||
1001 (it+1)->start_same_saC>it)));
1002 const label_index t_label = label_or_divergence(t);
1004 for(outgoing_transitions_const_it itt=it->start_same_saC;
1005 itt<it->start_same_saC->start_same_saC; ++itt)
1007 const transition& t1=m_aut.get_transitions()[!initialisation
1008 ? *itt->ref.BLC_transitions : itt->ref.transitions];
1009 assert(m_states.cbegin()+t1.from()==si);
1010 assert(label_or_divergence(t1) == t_label);
1011 assert(m_states[t.to()].block->c.onstellation==
1012 m_states[t1.to()].block->c.onstellation);
1015 const label_index label = label_or_divergence(t);
1018 const constellation_type* t_to_constellation=
1019 m_states[t.to()].block->c.onstellation;
1020 if (constellations_seen.count(std::pair(label,t_to_constellation))>0)
1022 assert(it!=s.start_outgoing_transitions);
1023 const transition& old_t=m_aut.get_transitions()[!initialisation
1024 ? *std::prev(it)->ref.BLC_transitions
1025 : std::prev(it)->ref.transitions];
1026 assert(label_or_divergence(old_t)==label);
1027 assert(t_to_constellation==
1028 m_states[old_t.to()].block->c.onstellation);
1032 if (m_branching && m_aut.is_tau(label))
1040 constellations_seen.emplace(label,t_to_constellation);
1045 if (!initialisation)
1053 for (
const state_in_block_pointer* si=m_states_in_blocks.data();
1054 m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
1056 const block_type& b=*si->ref_state->block;
1057 const constellation_type& c=*b.c.onstellation;
1058 assert(m_states_in_blocks.data()<=c.start_const_states);
1059 assert(c.start_const_states<=b.start_bottom_states);
1060 assert(b.start_bottom_states<b.sta.rt_non_bottom_states);
1061 assert(b.sta.rt_non_bottom_states<=b.end_states);
1062 assert(b.end_states<=c.end_const_states);
1063 assert(c.end_const_states<=m_states_in_blocks.data_end());
1065 unsigned char const max_B=check_complexity::log_n-
1066 check_complexity::ilog2(number_of_states_in_block(b));
1067 unsigned char const max_C=check_complexity::log_n-check_complexity::
1068 ilog2(number_of_states_in_constellation(*b.c.onstellation));
1069 for (
const state_in_block_pointer*
1070 is=b.start_bottom_states; is!=b.sta.rt_non_bottom_states; ++is)
1072 assert(is->ref_state->block==&b);
1073 assert(is->ref_state->no_of_outgoing_block_inert_transitions==0);
1074 if (check_temporary_complexity_counters)
1078 !initialisation), *
this);
1081 for (
const state_in_block_pointer*
1082 is=b.sta.rt_non_bottom_states; is!=b.end_states; ++is)
1084 assert(is->ref_state->block==&b);
1085 assert(is->ref_state->no_of_outgoing_block_inert_transitions>0);
1094 if (!initialisation)
1096 assert(b.block.to_constellation.check_linked_list());
1098 ind=b.block.to_constellation.begin();
1099 ind!=b.block.to_constellation.end(); ++ind)
1101 assert(ind->start_same_BLC<ind->end_same_BLC);
1102 const transition& first_transition=
1103 m_aut.get_transitions()[*(ind->start_same_BLC)];
1104 const label_index first_transition_label=
1105 label_or_divergence(first_transition);
1106 if(!is_inert_during_init(first_transition) ||
1107 m_states[first_transition.from()].block->c.onstellation!=
1108 m_states[first_transition.to()].block->c.onstellation)
1110 ++actual_no_of_non_constellation_inert_BLC_sets;
1112 for(BLC_list_const_iterator i=ind->start_same_BLC;
1113 i<ind->end_same_BLC; ++i)
1115 const transition& t=m_aut.get_transitions()[*i];
1116 assert(m_transitions[*i].transitions_per_block_to_constellation==
1118 all_transitions.emplace(*i);
1119 assert(m_states[t.from()].block==&b);
1120 assert(m_states[t.to()].block->c.onstellation==
1121 m_states[first_transition.to()].block->c.onstellation);
1122 assert(label_or_divergence(t)==first_transition_label);
1123 if (is_inert_during_init(t) && b.c.onstellation==
1124 m_states[t.to()].block->c.onstellation)
1128 assert(b.block.to_constellation.begin()==ind);
1131 if (check_temporary_complexity_counters)
1134 check_complexity::log_n-check_complexity::ilog2
1135 (number_of_states_in_constellation(*m_states
1136 [first_transition.to()].block->c.onstellation))), *
this);
1141 if (!initialisation) {
1142 assert(all_transitions.size()==m_transitions.size());
1143 assert(actual_no_of_non_constellation_inert_BLC_sets==
1153 for (
const state_in_block_pointer*
1154 si=m_states_in_blocks.data(); si<m_states_in_blocks.data_end(); ++si)
1156 assert(si==si->ref_state->ref_states_in_blocks);
1160 for(
const block_type* bi: m_blocks_with_new_bottom_states)
1162 assert(bi->contains_new_bottom_states);
1166 for(
const constellation_type* ci: m_non_trivial_constellations)
1169 const block_type*
const first_bi=ci->start_const_states->ref_state->block;
1170 const block_type*
const last_bi=std::prev(ci->end_const_states)->ref_state->block;
1171 assert(first_bi != last_bi);
1204 const std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >*
1215 old_constellation!=new_constellation ));
1217 for (
const state_in_block_pointer* si=m_states_in_blocks.data();
1218 m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
1220 const block_type& b=*si->ref_state->block;
1221 bool previous_stable=
true;
1223 ind=b.block.to_constellation.begin();
1224 ind!=b.block.to_constellation.end(); ++ind)
1226 set_of_states_type all_source_bottom_states;
1228 assert(ind->start_same_BLC<ind->end_same_BLC);
1229 const transition&first_t=m_aut.get_transitions()[*ind->start_same_BLC];
1230 const label_index first_t_label=label_or_divergence(first_t);
1231 const bool all_transitions_in_BLC_are_inert =
1232 is_inert_during_init(first_t) && b.c.onstellation==
1233 m_states[first_t.to()].block->c.onstellation;
1234 assert(!all_transitions_in_BLC_are_inert ||
1235 b.block.to_constellation.begin()==ind);
1236 for (BLC_list_const_iterator i=ind->start_same_BLC;
1237 i<ind->end_same_BLC; ++i)
1239 assert(m_BLC_transitions.data()<=i);
1240 assert(i<m_BLC_transitions.data_end());
1241 const transition& t=m_aut.get_transitions()[*i];
1242 assert(m_states[t.from()].block == &b);
1243 assert(label_or_divergence(t) == first_t_label);
1244 assert(m_states[t.to()].block->c.onstellation==
1245 m_states[first_t.to()].block->c.onstellation);
1246 if (is_inert_during_init(t) && b.c.onstellation==
1247 m_states[t.to()].block->c.onstellation)
1249 assert(all_transitions_in_BLC_are_inert);
1254 assert(!all_transitions_in_BLC_are_inert);
1255 if (0 == m_states[t.from()].no_of_outgoing_block_inert_transitions)
1257 assert(b.start_bottom_states<=
1258 m_states[t.from()].ref_states_in_blocks);
1259 assert(m_states[t.from()].ref_states_in_blocks<
1260 b.sta.rt_non_bottom_states);
1261 all_source_bottom_states.emplace(t.from());
1265 assert(b.sta.rt_non_bottom_states<=
1266 m_states[t.from()].ref_states_in_blocks);
1267 assert(m_states[t.from()].ref_states_in_blocks < b.end_states);
1271 assert(all_source_bottom_states.size()<=
static_cast<std::size_t>
1272 (std::distance(b.start_bottom_states, b.sta.rt_non_bottom_states)));
1274 bool eventual_instability_is_ok =
true;
1275 bool eventual_marking_is_ok =
true;
1276 if (!all_transitions_in_BLC_are_inert &&
1277 all_source_bottom_states.size()!=
static_cast<std::size_t>
1278 (std::distance(b.start_bottom_states, b.sta.rt_non_bottom_states)))
1282 << std::distance(b.start_bottom_states, b.sta.rt_non_bottom_states)
1283 << (m_branching ?
" bottom states have a transition in the "
1284 :
" states have a transition in the ")
1285 << ind->debug_id(*
this) <<
": transitions found from states";
1286 for (set_of_states_type::iterator
1287 asbc_it=all_source_bottom_states.begin();
1288 asbc_it!=all_source_bottom_states.end() ; ++asbc_it)
1289 {
mCRL2log(log::debug) <<
' ' << *asbc_it; }
1291 eventual_instability_is_ok =
false;
1293 if (!ind->is_stable())
1296 mCRL2log(log::debug) << ind->debug_id(*
this) <<
" contains " << std::distance(ind->start_marked_BLC, ind->end_same_BLC) <<
" marked transitions.\n";
1297 eventual_marking_is_ok =
false;
1299 if (b.contains_new_bottom_states)
1301 if (!(eventual_instability_is_ok && eventual_marking_is_ok))
1303 mCRL2log(log::debug) <<
" This is ok because " << b.debug_id(*
this) <<
" contains new bottom states.\n";
1304 eventual_instability_is_ok =
true;
1305 eventual_marking_is_ok =
true;
1308 if (!(eventual_instability_is_ok && eventual_marking_is_ok) &&
nullptr != calM && calM->begin() != calM->end())
1310 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >::const_iterator calM_iter = calM->begin();
1311 if (
nullptr != calM_elt)
1315 assert(calM->end() != calM_iter);
1316 if (calM_iter->first <= calM_elt->first && calM_elt->second <= calM_iter->second)
1322 if (calM_elt->first<=ind->start_same_BLC && ind->end_same_BLC<=calM_elt->second)
1324 mCRL2log(log::debug) <<
" This is ok because the BLC set ("
1325 << b.debug_id(*
this) <<
" -" << m_aut.action_label(first_t.label())
1326 <<
"-> " << m_states[first_t.to()].
1327 block->c.onstellation->debug_id(*
this)
1328 <<
") is soon going to be a main splitter.\n";
1329 eventual_instability_is_ok =
true;
1330 eventual_marking_is_ok =
true;
1334 if (old_constellation==
1335 m_states[first_t.to()].block->c.onstellation)
1337 const linked_list<BLC_indicators>::const_iterator main_splitter=b.block.to_constellation.next(ind);
1338 if (main_splitter!=b.block.to_constellation.end())
1340 assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
1341 const transition& main_t = m_aut.get_transitions()[*main_splitter->start_same_BLC];
1342 assert(m_states[main_t.from()].block == &b);
1343 if(label_or_divergence(first_t)==label_or_divergence(main_t)
1344 && m_states[main_t.to()].block->c.onstellation==
1347 if (calM_elt->first<=main_splitter->start_same_BLC && main_splitter->end_same_BLC<=calM_elt->second)
1349 assert(new_constellation==
1350 m_states[main_t.to()].block->c.onstellation);
1351 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";
1352 eventual_instability_is_ok =
true;
1353 eventual_marking_is_ok =
true;
1361 for(; !(eventual_instability_is_ok && eventual_marking_is_ok) && calM->end() != calM_iter; ++calM_iter)
1363 if (calM_iter->first<=ind->start_same_BLC && ind->end_same_BLC<=calM_iter->second)
1365 mCRL2log(log::debug) <<
" This is ok because the BLC set ("
1366 << b.debug_id(*
this) <<
" -" << m_aut.action_label(first_t.label())
1368 << m_states[first_t.to()].block->c.onstellation->debug_id(*
this)
1369 <<
") is going to be a main splitter later.\n";
1370 eventual_instability_is_ok =
true;
1371 eventual_marking_is_ok =
true;
1375 if (old_constellation==
1376 m_states[first_t.to()].block->c.onstellation)
1378 const linked_list<BLC_indicators>::const_iterator main_splitter=b.block.to_constellation.next(ind);
1379 if (main_splitter != b.block.to_constellation.end())
1381 assert(main_splitter->start_same_BLC < main_splitter->end_same_BLC);
1382 const transition& main_t = m_aut.get_transitions()[*main_splitter->start_same_BLC];
1383 assert(m_states[main_t.from()].block == &b);
1384 if(label_or_divergence(first_t)==label_or_divergence(main_t)
1385 && m_states[main_t.to()].block->c.onstellation==
1388 if (calM_iter->first<=main_splitter->start_same_BLC && main_splitter->end_same_BLC<=calM_iter->second)
1390 assert(new_constellation==
1391 m_states[main_t.to()].block->c.onstellation);
1392 mCRL2log(log::debug) <<
" This is ok because the BLC "
1393 "set (" << b.debug_id(*
this) <<
" -"
1394 << m_aut.action_label(first_t.label())
1395 <<
"-> " << old_constellation->debug_id(*
this)
1396 <<
") is going to be a co-splitter later.\n";
1397 eventual_instability_is_ok =
true;
1398 eventual_marking_is_ok =
true;
1406 if (1>=number_of_states_in_block(b))
1408 if (!eventual_marking_is_ok)
1410 mCRL2log(log::debug) <<
" (This is ok because the source block contains only 1 state.)\n";
1411 eventual_marking_is_ok =
true;
1414 else if (1<no_of_constellations &&
1415 !b.contains_new_bottom_states)
1417 assert(eventual_marking_is_ok); assert(eventual_instability_is_ok);
1418 if (null_constellation==old_constellation && ind->is_stable()) {
1419 assert(previous_stable);
1423 previous_stable=
false;
1436 for(
const BLC_indicators& blc_it: bi->block.to_constellation)
1438 const transition& first_t=m_aut.get_transitions()[*blc_it.start_same_BLC];
1439 const label_index l=label_or_divergence(first_t, (label_index) -2);
1440 mCRL2log(log::debug) <<
"\n BLC set "
1441 << std::distance<BLC_list_const_iterator>(m_BLC_transitions.data(),
1442 blc_it.start_same_BLC) <<
" -- "
1443 << std::distance<BLC_list_const_iterator>(m_BLC_transitions.data(),
1444 blc_it.end_same_BLC)
1445 <<
" of " << ((label_index)-2==l ?
"divergent self-loop "
1446 : pp(m_aut.action_label(l))+
"-")
1447 <<
"transitions to " << m_states[first_t.to()].block->c.onstellation->debug_id(*
this) <<
":\n";
1448 for (BLC_list_const_iterator i=blc_it.start_same_BLC; ; ++i)
1450 if (i == blc_it.start_marked_BLC)
1452 mCRL2log(log::debug) <<
" (The BLC set is unstable, and the "
1453 " following transitions are marked.)\n";
1455 if (i>=blc_it.end_same_BLC)
1459 const transition& t=m_aut.get_transitions()[*i];
1460 mCRL2log(log::debug) <<
" " << t.from() <<
" -"
1461 << m_aut.action_label(t.label()) <<
"-> " << t.to();
1462 if (is_inert_during_init(t) &&
1463 m_states[t.from()].block==m_states[t.to()].block)
1465 mCRL2log(log::debug) <<
" (block-inert)";
1467 else if (is_inert_during_init(t) &&
1468 m_states[t.from()].block->c.onstellation==
1469 m_states[t.to()].block->c.onstellation)
1471 mCRL2log(log::debug) <<
" (constellation-inert)";
1481 const bool initialisation=
false)
const
1484 mCRL2log(log::debug) <<
"========= PRINT DATASTRUCTURE: " << header <<
" =======================================\n"
1485 "++++++++++++++++++++ States ++++++++++++++++++++++++++++\n";
1488 mCRL2log(log::debug) <<
"State " << si <<
" (" << m_states[si].block->debug_id(*
this) <<
"):\n"
1489 " #Inert outgoing transitions: " << m_states[si].no_of_outgoing_block_inert_transitions <<
"\n"
1491 " Incoming transitions:\n";
1492 std::vector<transition>::const_iterator end=(si+1==m_aut.num_states()?m_aut.get_transitions().end():m_states[si+1].start_incoming_transitions);
1493 for(std::vector<transition>::const_iterator it=m_states[si].start_incoming_transitions; it!=end; ++it)
1495 mCRL2log(log::debug) <<
" " << ptr(*it) <<
"\n";
1501 for(outgoing_transitions_const_it it=m_states[si].start_outgoing_transitions;
1502 it!=m_outgoing_transitions.end() &&
1503 (si+1>=m_aut.num_states() || it!=m_states[si+1].start_outgoing_transitions);
1506 const transition& t=m_aut.get_transitions()[!initialisation
1507 ? *it->ref.BLC_transitions : it->ref.transitions];
1508 bool start_same_saC_valid=
1509 m_outgoing_transitions.cbegin()<=it->start_same_saC &&
1510 it->start_same_saC<m_outgoing_transitions.end();
1511 if (start_same_saC_valid &&
1512 it->start_same_saC->start_same_saC==it &&
1513 it->start_same_saC >= it)
1516 const label_index old_t_label=t_label;
1517 t_label=label_or_divergence(t, (label_index) -2);
1518 to_constln=m_states[t.to()].block->c.onstellation;
1519 mCRL2log(log::debug) <<
" - - - - saC slice of "
1520 << ((label_index) -2==t_label ?
"divergent self-loop "
1521 : pp(m_aut.action_label(t_label))+
"-")
1522 <<
"transitions to " << to_constln->debug_id(*
this)
1523 << (m_aut.is_tau(t_label) && !m_aut.is_tau(old_t_label)
1524 ?
" -- error: tau-transitions should come first\n"
1527 mCRL2log(log::debug) <<
" " << ptr(t);
1528 if (start_same_saC_valid)
1530 if (label_or_divergence(t, (label_index) -2)!=t_label)
1532 mCRL2log(log::debug) <<
" -- error: different label";
1534 if (!initialisation && m_states[t.to()].block->c.onstellation!=to_constln)
1536 mCRL2log(log::debug) <<
" -- error: different target " << m_states[t.to()].block->c.onstellation->debug_id(*
this);
1538 if (it->start_same_saC->start_same_saC == it)
1541 if (it->start_same_saC >= it && it > m_outgoing_transitions.cbegin())
1544 const transition& prev_t=m_aut.get_transitions()[
1545 !initialisation ? *std::prev(it)->ref.BLC_transitions
1546 : std::prev(it)->ref.transitions];
1547 if (prev_t.from()==t.from() &&
1548 label_or_divergence(prev_t)==t_label &&
1550 m_states[prev_t.to()].block->c.onstellation==
1551 m_states[t.to()].block->c.onstellation))
1553 mCRL2log(log::debug) <<
" -- error: not the beginning of a saC-slice";
1556 if (it->start_same_saC <= it && std::next(it) < m_outgoing_transitions.end())
1559 const transition& next_t=m_aut.get_transitions()[
1560 !initialisation ? *std::next(it)->ref.BLC_transitions
1561 : std::next(it)->ref.transitions];
1562 if (next_t.from()==t.from() &&
1563 label_or_divergence(next_t)==t_label &&
1565 m_states[next_t.to()].block->c.onstellation==
1566 m_states[t.to()].block->c.onstellation))
1568 mCRL2log(log::debug) <<
" -- error: not the end of a saC-slice";
1572 else if (it->start_same_saC > it ? it->start_same_saC->start_same_saC > it : it->start_same_saC->start_same_saC < it)
1574 mCRL2log(log::debug) <<
" -- error: not pointing to its own saC-slice";
1579 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";
1582 mCRL2log(log::debug) <<
"++++++++++++++++++++ Transitions ++++++++++++++++++++++++++++\n";
1583 for(transition_index ti=0; ti<m_transitions.size(); ++ti)
1585 const transition& t=m_aut.get_transitions()[ti];
1586 mCRL2log(log::debug) <<
"Transition " << ti <<
": " << t.from()
1587 <<
" -" << m_aut.action_label(t.label()) <<
"-> "
1592 for (
const state_in_block_pointer* si=m_states_in_blocks.data();
1593 m_states_in_blocks.data_end()!=si; si=si->ref_state->block->end_states)
1595 block_type*
const bi=si->ref_state->block;
1596 mCRL2log(log::debug) <<
" Block " << bi;
1597 if (!initialisation) {
1598 mCRL2log(log::debug) <<
" (" << bi->c.onstellation->debug_id(*
this) <<
')';
1600 mCRL2log(log::debug) <<
":\n " << std::distance(bi->start_bottom_states,
1601 bi->sta.rt_non_bottom_states)
1602 << (m_branching ?
" Bottom state" :
" State")
1603 << (1==std::distance(bi->start_bottom_states,
1604 bi->sta.rt_non_bottom_states) ?
": " :
"s: ");
1605 for (
const state_in_block_pointer*
1606 sit=bi->start_bottom_states; sit!=bi->sta.rt_non_bottom_states; ++sit)
1608 mCRL2log(log::debug) << sit->ref_state->debug_id_short(*
this) <<
" ";
1612 mCRL2log(log::debug) <<
"\n " << std::distance
1613 (bi->sta.rt_non_bottom_states, bi->end_states)
1614 <<
" Non-bottom state" << (1==std::distance
1615 (bi->sta.rt_non_bottom_states, bi->end_states)
1617 for (
const state_in_block_pointer*
1618 sit=bi->sta.rt_non_bottom_states; sit!=bi->end_states; ++sit)
1620 mCRL2log(log::debug) << sit->ref_state->debug_id_short(*
this) <<
" ";
1625 assert(bi->sta.rt_non_bottom_states==bi->end_states);
1627 if (!initialisation)
1629 display_BLC_list(bi);
1634 mCRL2log(log::debug) <<
"++++++++++++++++++++ Constellations ++++++++++++++++++++++++++++\n";
1635 for (
const state_in_block_pointer* si=m_states_in_blocks.data();
1636 m_states_in_blocks.data_end()!=si;
1637 si=si->ref_state->block->c.onstellation->end_const_states)
1639 const constellation_type*
const ci=si->ref_state->block->c.onstellation;
1640 mCRL2log(log::debug) <<
" " << ci->debug_id(*
this) <<
":\n";
1641 mCRL2log(log::debug) <<
" Blocks in constellation:";
1642 for (
const state_in_block_pointer*
1643 constln_it=ci->start_const_states;
1644 constln_it<ci->end_const_states; )
1646 const block_type*
const bi=constln_it->ref_state->block;
1647 mCRL2log(log::debug) <<
" " << bi->debug_id(*
this);
1648 constln_it = bi->end_states;
1653 for (
const constellation_type* ci: m_non_trivial_constellations)
1655 mCRL2log(log::debug) <<
" " << ci->debug_id(*
this);
1659 "\n++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n"
1660 "Outgoing transitions:\n";
1662 for (outgoing_transitions_const_it pi = m_outgoing_transitions.cbegin();
1663 pi < m_outgoing_transitions.cend(); ++pi)
1665 const transition& t=m_aut.get_transitions()[!initialisation
1666 ? *pi->ref.BLC_transitions : pi->ref.transitions];
1667 mCRL2log(log::debug) <<
" " << t.from() <<
" -"
1668 << m_aut.action_label(t.label()) <<
"-> " << t.to();
1669 if (m_outgoing_transitions.cbegin()<=pi->start_same_saC &&
1670 pi->start_same_saC<m_outgoing_transitions.end())
1672 const transition& t1=m_aut.get_transitions()[!initialisation
1673 ? *pi->start_same_saC->ref.BLC_transitions
1674 : pi->start_same_saC->ref.transitions];
1675 mCRL2log(log::debug) <<
" \t(same saC: " << t1.from() <<
" -" << m_aut.action_label(t1.label()) <<
"-> " << t1.to();
1676 const label_index t_label = label_or_divergence(t);
1677 if (pi->start_same_saC->start_same_saC == pi)
1680 if (pi->start_same_saC >= pi && pi > m_outgoing_transitions.cbegin())
1683 const transition& prev_t=m_aut.get_transitions()[
1684 !initialisation ? *std::prev(pi)->ref.BLC_transitions
1685 : std::prev(pi)->ref.transitions];
1686 if (prev_t.from()==t.from() &&
1687 label_or_divergence(prev_t)==t_label &&
1689 m_states[prev_t.to()].block->c.onstellation==
1690 m_states[t.to()].block->c.onstellation))
1692 mCRL2log(log::debug) <<
" -- error: not the beginning of a saC-slice";
1695 if (pi->start_same_saC <= pi && std::next(pi) < m_outgoing_transitions.end())
1698 const transition& next_t=m_aut.get_transitions()[
1699 !initialisation ? *std::next(pi)->ref.BLC_transitions
1700 : std::next(pi)->ref.transitions];
1701 if (next_t.from()==t.from() &&
1702 label_or_divergence(next_t)==t_label &&
1704 m_states[next_t.to()].block->c.onstellation==
1705 m_states[t.to()].block->c.onstellation))
1707 mCRL2log(log::debug) <<
" -- error: not the end of a saC-slice";
1711 else if (pi->start_same_saC > pi ? pi->start_same_saC->start_same_saC > pi : pi->start_same_saC->start_same_saC < pi)
1713 mCRL2log(log::debug) <<
" -- error: not in its own saC-slice";
1719 mCRL2log(log::debug) <<
"++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++\n"
1720 "New bottom blocks to be investigated:";
1722 for(
const block_type* bi: m_blocks_with_new_bottom_states)
1724 mCRL2log(log::debug) <<
" " << bi->debug_id(*
this) <<
'\n';
1727 mCRL2log(log::debug) <<
"\n========= END PRINT DATASTRUCTURE: " << header <<
" =======================================\n";
1749 { assert(si<m_states.size());
1750 return m_states[si].block->sta.te_in_reduced_LTS;
1774 for (state_in_block_pointer*
1775 si=m_states_in_blocks.data(); m_states_in_blocks.data_end()!=si;
1776 si=si->ref_state->block->end_states)
1778 block_type*
const bi=si->ref_state->block;
1780 new (&bi->sta.te_in_reduced_LTS) state_index(block_number);
1787 typename std::remove_reference<
decltype(
m_aut.get_transitions())>::type
1789 for (state_in_block_pointer*
1790 si=m_states_in_blocks.data(); m_states_in_blocks.data_end()!=si;
1791 si=si->ref_state->block->end_states)
1793 const block_type& B=*si->ref_state->block;
1796 for(
const BLC_indicators blc_ind: B.block.to_constellation)
1800 assert(blc_ind.start_same_BLC<blc_ind.end_same_BLC);
1802 t=m_aut.get_transitions()[*blc_ind.start_same_BLC];
1803 const state_index new_to=get_eq_class(t.to());
1804 if (!is_inert_during_init(t) || B.sta.te_in_reduced_LTS!=new_to)
1806 T.emplace_back(B.sta.te_in_reduced_LTS, t.label(), new_to);
1810 m_aut.get_transitions()=
std::move(T);
1816 if (
m_aut.has_state_info())
1819 typename std::remove_reference<
decltype(
m_aut.state_labels())>::type
1822 for(
std::size_t i=0; i<
m_aut.num_states(); ++i)
1827 new_labels[new_index]=new_labels[new_index]+
m_aut.state_label(i);
1832 m_aut.state_labels()=
std::move(new_labels);
1855 return std::to_string(t.from())+
" -"+pp(m_aut.action_label(t.label()))+
1856 "-> "+std::to_string(t.to());
1879 { assert(m_states_in_blocks.data()<=pos1);
1880 std::swap(*pos1,*pos2); assert(pos1<m_states_in_blocks.data_end());
1881 pos1->ref_state->ref_states_in_blocks=pos1; assert(m_states_in_blocks.data()<=pos2);
1882 pos2->ref_state->ref_states_in_blocks=pos2; assert(pos2<m_states_in_blocks.data_end()); assert(pos1!=pos2);
1902 { assert(m_states_in_blocks.data()<=pos2); assert(pos2<pos3);
1903 assert(pos1<m_states_in_blocks.data_end());
1906 std::swap(*pos1,*pos2);
1909 { assert(pos3<pos1);
1915 pos3->ref_state->ref_states_in_blocks=pos3;
1917 pos1->ref_state->ref_states_in_blocks=pos1;
1918 pos2->ref_state->ref_states_in_blocks=pos2;
1931 swap_states_in_states_in_block(pos1,pos2);
1950 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1952 unsigned char const max_B,
1957 { assert(count<
m_aut.num_states()); assert(m_states_in_blocks.data()<=pos1);
1958 assert(pos1<pos2); assert(pos2<=m_states_in_blocks.data_end()-count);
1960 std::make_signed<state_index>::type
1961 overlap=std::distance(pos2, pos1)+count;
1965 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1969 if (pos2==assign_work_to) {
1970 assign_work_to+=overlap;
1971 }
else { assert(assign_work_to+count<=pos2+overlap ||
1972 pos2+overlap+count<=assign_work_to); }
1976 } assert(0 < count);
1979 {
mCRL2complexity(assign_work_to->ref_state, add_work(ctr, max_B), *
this);
1980 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1984 pos1->ref_state->ref_states_in_blocks=pos1;
1987 pos2->ref_state->ref_states_in_blocks=pos2;
1991 pos1->ref_state->ref_states_in_blocks=pos1;
1993 pos2->ref_state->ref_states_in_blocks=pos2;
1995 for (fixed_vector<state_type_gj>::const_iterator
1996 si=m_states.cbegin(); si<m_states.cend(); ++si)
1998 assert(si==si->ref_states_in_blocks->ref_state);
2010 m_transitions[*old_pos].transitions_per_block_to_constellation; assert(ind->start_same_BLC<=old_pos);
2011 assert(old_pos<m_BLC_transitions.data_end());
2012 assert(old_pos<ind->end_same_BLC); assert(!ind->is_stable());
2013 if (old_pos < ind->start_marked_BLC)
2015 assert(ind->start_same_BLC<ind->start_marked_BLC);
2016 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);
2017 assert(new_pos<m_BLC_transitions.data_end());
2018 if (old_pos < new_pos)
2020 std::swap(*old_pos, *new_pos);
2021 m_transitions[*old_pos].ref_outgoing_transitions->
2022 ref.BLC_transitions = old_pos; assert(out_pos==m_transitions[*new_pos].ref_outgoing_transitions);
2023 out_pos->ref.BLC_transitions = new_pos;
2025 ind->start_marked_BLC--;
2029 for (BLC_list_const_iterator it=m_BLC_transitions.data();
2030 it<m_BLC_transitions.data_end(); ++it)
2032 assert(m_transitions[*it].ref_outgoing_transitions->ref.BLC_transitions==
2034 assert(m_transitions[*it].transitions_per_block_to_constellation->
2035 start_same_BLC<=it);
2037 m_transitions[*it].transitions_per_block_to_constellation->end_same_BLC);
2047 { assert(i3<=i2); assert(i2<=i1);
2052 if ((i1==i2)||(i2==i3))
2055 m_transitions[*i1].ref_outgoing_transitions->ref.BLC_transitions = i1;
2056 m_transitions[*i3].ref_outgoing_transitions->ref.BLC_transitions = i3;
2064 m_transitions[*i1].ref_outgoing_transitions->ref.BLC_transitions = i1;
2065 m_transitions[*i2].ref_outgoing_transitions->ref.BLC_transitions = i2;
2066 m_transitions[*i3].ref_outgoing_transitions->ref.BLC_transitions = i3;
2090 linked_list<BLC_indicators>::iterator new_BLC_block,
2091 linked_list<BLC_indicators>::iterator old_BLC_block)
2092 { assert(new_BLC_block->is_stable());
2094 m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions; assert(old_BLC_block->start_same_BLC <= old_position);
2095 assert(old_position<old_BLC_block->end_same_BLC);
2096 assert(new_BLC_block->end_same_BLC==old_BLC_block->start_same_BLC);
2097 assert(m_transitions[ti].transitions_per_block_to_constellation==old_BLC_block);
2098 assert(ti == *old_position); assert(old_BLC_block->is_stable());
2099 if (old_position!=old_BLC_block->start_same_BLC)
2101 std::swap(*old_position,*old_BLC_block->start_same_BLC);
2102 m_transitions[*old_position].ref_outgoing_transitions->
2103 ref.BLC_transitions = old_position;
2104 m_transitions[*old_BLC_block->start_same_BLC].
2105 ref_outgoing_transitions->ref.BLC_transitions =
2106 old_BLC_block->start_same_BLC;
2108 new_BLC_block->end_same_BLC=++old_BLC_block->start_same_BLC;
2109 m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
2110 return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
2136 { assert(m_states[t.to()].block==index_block_B);
2137 block_type*
const from_block=m_states[t.from()].block; assert(&
m_aut.get_transitions()[ti] == &t);
2138 bool new_block_created =
false; assert(from_block->block.to_constellation.check_linked_list());
2139 linked_list<BLC_indicators>::iterator this_block_to_constellation=
2140 m_transitions[ti].transitions_per_block_to_constellation; assert(this_block_to_constellation->is_stable());
2143 for (
linked_list<BLC_indicators>::const_iterator i=from_block->block.to_constellation.begin();
2144 i!=this_block_to_constellation; ++i)
2146 assert(i!=from_block->block.to_constellation.end());
2149 assert(this_block_to_constellation!=from_block->block.to_constellation.end());
2150 assert(this_block_to_constellation->start_same_BLC <= m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions);
2151 linked_list<BLC_indicators>::iterator next_block_to_constellation;
2156 next_block_to_constellation=from_block->block.to_constellation.begin(); assert(next_block_to_constellation->start_same_BLC <
2157 next_block_to_constellation->end_same_BLC);
2158 assert(m_states[m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].from()].block==index_block_B);
2159 assert(m_aut.is_tau(m_aut_apply_hidden_label_map(m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].label())));
2160 if (next_block_to_constellation==this_block_to_constellation)
2165 next_block_to_constellation=from_block->block.to_constellation.
2167 this_block_to_constellation->start_same_BLC,
2168 this_block_to_constellation->start_same_BLC,
true);
2169 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2170 next_block_to_constellation->work_counter = this_block_to_constellation->work_counter;
2173 assert(m_states[m_aut.get_transitions()[*(next_block_to_constellation->start_same_BLC)].to()].block==index_block_B);
2187 next_block_to_constellation=from_block->
2188 block.to_constellation.next(this_block_to_constellation);
2190 if (next_block_to_constellation==
2191 from_block->block.to_constellation.end() ||
2192 (first_t=&m_aut.get_transitions()
2193 [*(next_block_to_constellation->start_same_BLC)], assert(m_states[first_t->from()].block==from_block),
2194 m_states[first_t->to()].block!=index_block_B) ||
2195 label_or_divergence(*first_t)!=label_or_divergence(t))
2198 new_block_created =
true;
2199 next_block_to_constellation=from_block->block.to_constellation.
2200 emplace_after(this_block_to_constellation,
2201 this_block_to_constellation->start_same_BLC,
2202 this_block_to_constellation->start_same_BLC,
true);
2203 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2204 next_block_to_constellation->work_counter=
2205 this_block_to_constellation->work_counter;
2211 if (swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation(ti,
2212 next_block_to_constellation, this_block_to_constellation))
2214 from_block->block.to_constellation.erase(this_block_to_constellation);
2229 return new_block_created;
2246 linked_list<BLC_indicators>::iterator new_BLC_block,
2247 linked_list<BLC_indicators>::iterator old_BLC_block)
2248 { assert(new_BLC_block->end_same_BLC==old_BLC_block->start_same_BLC);
2250 m_transitions[ti].ref_outgoing_transitions->ref.BLC_transitions; assert(old_BLC_block->start_same_BLC<=old_position);
2251 assert(old_position<old_BLC_block->end_same_BLC); assert(ti==*old_position);
2252 assert(m_transitions[ti].transitions_per_block_to_constellation==
2255 if (old_BLC_block->is_stable())
2256 { assert(new_BLC_block->is_stable());
2257 if (old_position!=old_BLC_block->start_same_BLC)
2259 std::swap(*old_position, *old_BLC_block->start_same_BLC);
2260 m_transitions[*old_position].ref_outgoing_transitions->
2261 ref.BLC_transitions=old_position;
2262 m_transitions[*old_BLC_block->start_same_BLC].
2263 ref_outgoing_transitions->ref.BLC_transitions=
2264 old_BLC_block->start_same_BLC;
2268 { assert(!new_BLC_block->is_stable());
2269 assert(new_BLC_block->start_same_BLC<=new_BLC_block->start_marked_BLC);
2270 assert(new_BLC_block->start_marked_BLC<=new_BLC_block->end_same_BLC);
2271 if (old_position<old_BLC_block->start_marked_BLC)
2272 { assert(old_BLC_block->start_marked_BLC<=old_BLC_block->end_same_BLC);
2273 swap_three_iterators_and_update_m_transitions(old_position,
2274 old_BLC_block->start_same_BLC, new_BLC_block->start_marked_BLC);
2275 ++new_BLC_block->start_marked_BLC;
2278 { assert(old_BLC_block->start_same_BLC<=old_BLC_block->start_marked_BLC);
2279 swap_three_iterators_and_update_m_transitions(old_position,
2280 old_BLC_block->start_marked_BLC, old_BLC_block->start_same_BLC);
2281 ++old_BLC_block->start_marked_BLC;
2284 m_transitions[ti].transitions_per_block_to_constellation=new_BLC_block;
2285 new_BLC_block->end_same_BLC=++old_BLC_block->start_same_BLC;
2286 return old_BLC_block->start_same_BLC==old_BLC_block->end_same_BLC;
2318 { assert(old_bi->block.to_constellation.check_linked_list());
2319 const transition& t=
m_aut.get_transitions()[ti]; assert(new_bi->block.to_constellation.check_linked_list());
2320 assert(m_states[t.from()].block==new_bi);
2321 linked_list<BLC_indicators>::iterator this_block_to_constellation=
2322 m_transitions[ti].transitions_per_block_to_constellation;
2325 for (
linked_list<BLC_indicators>::const_iterator i=old_bi->block.to_constellation.begin();
2326 i!=this_block_to_constellation; ++i)
2328 assert(i!=old_bi->block.to_constellation.end());
2333 m_states[t.to()].block->c.onstellation;
2334 linked_list<BLC_indicators>::iterator new_BLC_block;
2338 assert(this_block_to_constellation==old_bi->block.to_constellation.begin());
2340 assert(!new_bi->block.to_constellation.empty());
2341 new_BLC_block=new_bi->block.to_constellation.begin(); assert(this_block_to_constellation->start_same_BLC==new_BLC_block->end_same_BLC);
2343 if (new_BLC_block->start_same_BLC<new_BLC_block->end_same_BLC) {
2344 const transition& inert_t=m_aut.get_transitions()[*new_BLC_block->start_same_BLC];
2345 assert(new_bi==m_states[inert_t.from()].block);
2347 assert(to_constln==m_states[inert_t.to()].block->c.onstellation);
2355 if (this_block_to_constellation->start_same_BLC!=
2356 m_BLC_transitions.data() &&
2357 (perhaps_new_BLC_block_transition=
2358 *std::prev(this_block_to_constellation->start_same_BLC),
2360 &m_aut.get_transitions()[perhaps_new_BLC_block_transition],
2361 m_states[perhaps_new_BLC_t->from()].block==new_bi) &&
2362 a==label_or_divergence(*perhaps_new_BLC_t) &&
2363 to_constln==m_states
2364 [perhaps_new_BLC_t->to()].block->c.onstellation)
2368 new_BLC_block=m_transitions[perhaps_new_BLC_block_transition].
2369 transitions_per_block_to_constellation;
2371 if (this_block_to_constellation->is_stable()) { assert(new_BLC_block->is_stable()); }
2372 else { assert(!new_BLC_block->is_stable()); }
2382 linked_list<BLC_indicators>::iterator new_position=
2384 if (new_bi->block.to_constellation.empty())
2386 assert(new_bi->block.to_constellation.end()==new_position);
2391 new_position=new_bi->block.to_constellation.before_end(); assert(new_bi->block.to_constellation.end()!=new_position);
2396 ((to_constln==new_constellation &&
2402 (to_constln==old_constellation &&
2413 { assert(old_constellation!=new_constellation);
2417 linked_list<BLC_indicators>::const_iterator old_co_splitter;
2419 if ((old_constellation==to_constln &&
2421 (old_co_splitter=old_bi->block.to_constellation.
2422 next(this_block_to_constellation),
2423 co_to_constln=new_constellation,
true)) ||
2424 (new_constellation==to_constln &&
2426 (old_co_splitter=old_bi->block.to_constellation.
2427 prev(this_block_to_constellation),
2428 co_to_constln=old_constellation,
true)))
2430 if (old_bi->block.to_constellation.end()!=old_co_splitter)
2443 if (new_bi->block.to_constellation.end()!=new_position &&
2444 m_BLC_transitions.data()<old_co_splitter->start_same_BLC)
2452 *std::prev(old_co_splitter->start_same_BLC);
2454 m_aut.get_transitions()[perhaps_new_co_spl_transition];
2455 if(new_bi==m_states[perhaps_new_co_spl_t.from()].block &&
2456 a==label_or_divergence(perhaps_new_co_spl_t) &&
2457 co_to_constln==m_states
2458 [perhaps_new_co_spl_t.to()].block->c.onstellation)
2464 new_position=m_transitions
2465 [perhaps_new_co_spl_transition].
2466 transitions_per_block_to_constellation;
2467 if (old_constellation==to_constln)
2474 new_position=new_bi->block.to_constellation.
2478 if (old_co_splitter->start_same_BLC<old_co_splitter->end_same_BLC)
2480 const transition& co_t=m_aut.get_transitions()
2481 [*old_co_splitter->start_same_BLC];
2482 assert(old_bi==m_states[co_t.from()].block ||
2483 new_bi==m_states[co_t.from()].block);
2485 assert(co_to_constln==m_states[co_t.to()].block->c.onstellation);
2511 else if (this_block_to_constellation->is_stable())
2515 new_position=m_branching ? new_bi->block.to_constellation.begin()
2516 : new_bi->block.to_constellation.end();
2517 } assert(!m_branching || new_bi->block.to_constellation.end()!=new_position);
2518 const BLC_list_iterator old_BLC_start=this_block_to_constellation->start_same_BLC;
2519 new_BLC_block=new_bi->block.to_constellation.emplace_after
2520 (new_position, old_BLC_start, old_BLC_start,
2521 this_block_to_constellation->is_stable());
2522 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2523 new_BLC_block->work_counter=this_block_to_constellation->work_counter;
2528 const bool last_element_removed=
2529 swap_in_the_doubly_linked_list_LBC_in_blocks_new_block(ti,
2530 new_BLC_block, this_block_to_constellation);
2532 if (last_element_removed)
2547 m_BLC_indicators_to_be_deleted.push_back
2548 (this_block_to_constellation);
2553 old_bi->block.to_constellation.erase(this_block_to_constellation);
2559 } assert(old_bi->block.to_constellation.check_linked_list());
2561 assert(new_bi->block.to_constellation.check_linked_list());
2573 std::vector<state_in_block_pointer>::const_iterator begin,
2574 std::vector<state_in_block_pointer>::const_iterator
const end,
2579 { assert(block==begin->ref_state->block);
2580 begin->ref_state->counter=undefined;
2589 const fixed_vector<state_type_gj>::iterator si)
2590 { assert(m_states.begin()<=si);
2591 block_type* bi = si->block; assert(si<m_states.end());
2592 swap_states_in_states_in_block(si->ref_states_in_blocks,
2593 bi->sta.rt_non_bottom_states); assert(0 == si->no_of_outgoing_block_inert_transitions);
2600 const linked_list<BLC_indicators>::iterator splitter)
2601 { assert(from_block->block.to_constellation.end()!=splitter);
2602 splitter->make_stable(); assert(splitter->start_same_BLC<splitter->end_same_BLC);
2604 const transition& t=m_aut.get_transitions()[*splitter->start_same_BLC];
2605 assert(from_block==m_states[t.from()].block);
2608 if (splitter!=btc.begin())
2610 linked_list<BLC_indicators>::iterator move_splitter_after=btc.end();
2614 m_aut.get_transitions()[*btc.begin()->start_same_BLC];
2615 if (is_inert_during_init_if_branching(perhaps_inert_t) &&
2616 m_states[perhaps_inert_t.to()].block->c.onstellation==
2617 from_block->c.onstellation)
2619 move_splitter_after=btc.begin();
2622 btc.splice_to_after(move_splitter_after, btc, splitter);
2632 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2637 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2641 for (state_in_block_pointer st: R)
2643 split_block_B_into_R_and_BminR__carry_out_split, max_B), *
this);
2644 swap_states_in_states_in_block(to_pos++,
2645 st.ref_state->ref_states_in_blocks);
2664 assert(!old_bi->block.to_constellation.empty());
2668 old_bi->block.to_constellation.begin()->start_same_BLC;
2669 linked_list<BLC_indicators>::iterator new_inert_BLC_set=
2670 new_bi->block.to_constellation.emplace_front(start_inert_BLC,
2671 start_inert_BLC,
true);
2672 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2673 assert(start_inert_BLC<old_bi->block.to_constellation.begin()->end_same_BLC);
2674 const transition& perhaps_inert_t=
m_aut.get_transitions()[*start_inert_BLC];
2675 assert(m_states[perhaps_inert_t.from()].block==old_bi ||
2676 m_states[perhaps_inert_t.from()].block==new_bi);
2677 if (is_inert_during_init(perhaps_inert_t) &&
2678 m_states[perhaps_inert_t.to()].block->c.onstellation==
2679 old_bi->c.onstellation)
2683 new_inert_BLC_set->work_counter=
2684 old_bi->block.to_constellation.begin()->work_counter;
2687 (
void) new_inert_BLC_set;
2694 { assert(new_bi==it->ref_state->block);
2696 std::next(it->ref_state)==m_states.end()
2697 ? m_outgoing_transitions.end()
2698 : std::next(it->ref_state)->start_outgoing_transitions;
2700 start_outgoing_transitions; out_it_end!=out_it; ++out_it)
2703 *out_it->ref.BLC_transitions
, old_constellation
, new_constellation
);
2708 { assert(!new_bi->block.to_constellation.empty());
2715 inert_ind=new_bi->block.to_constellation.begin();
2716 if (inert_ind->start_same_BLC==inert_ind->end_same_BLC)
2717 { assert(inert_ind->is_stable());
2718 new_bi->block.to_constellation.erase(inert_ind);
2722 for (std::vector<
linked_list<BLC_indicators>::iterator>::iterator
2723 it=m_BLC_indicators_to_be_deleted.begin();
2724 it<m_BLC_indicators_to_be_deleted.end(); ++it)
2725 { assert((*it)->start_same_BLC==(*it)->end_same_BLC);
2727 old_bi->block.to_constellation.erase(*it);
2729 clear(m_BLC_indicators_to_be_deleted);
2745 template<
bool initialisation =
false>
2756 assert(start_bottom_states<end_states);
2759 simple_list<BLC_indicators>::get_pool().
2760 template construct<block_type>
2764 (start_bottom_states,
2765 start_non_bottom_states, end_states, constellation); assert(end_states<=constellation
->end_const_states);
2770 for(; start_bottom_states<start_non_bottom_states; ++start_bottom_states)
2772 start_bottom_states->ref_state->no_of_outgoing_block_inert_transitions);
2773 assert(old_block_index==start_bottom_states->ref_state->block);
2774 start_bottom_states->ref_state->block=new_block_index; assert(start_bottom_states->ref_state->counter==
undefined);
2776 for (; start_bottom_states<end_states; ++start_bottom_states)
2777 { assert(old_block_index==start_bottom_states->ref_state->block);
2778 start_bottom_states->ref_state->block=new_block_index; assert(0!=
2779 start_bottom_states->ref_state->no_of_outgoing_block_inert_transitions);
2780 start_bottom_states->ref_state->counter=
undefined;
2783 if constexpr (initialisation)
2785 return new_block_index;
2789 old_constellation
, new_constellation
);
2798 for (; start_bottom!=end_non_bottom; ++start_bottom)
2800 std::vector<transition>::const_iterator
const in_it_end=
2801 std::next(start_bottom->ref_state)>=m_states.end()
2802 ? m_aut.get_transitions().end()
2803 : std::next(start_bottom->ref_state)->start_incoming_transitions; assert(start_bottom->ref_state->block!=NewBotSt_block_index);
2804 for (std::vector<transition>::iterator
2805 in_it=start_bottom->ref_state->start_incoming_transitions;
2807 m_aut.is_tau(m_aut_apply_hidden_label_map(in_it->label()));
2810 const fixed_vector<state_type_gj>::iterator
2811 from=m_states.begin()+in_it->from(); assert(m_states[in_it->to()].ref_states_in_blocks==start_bottom);
2812 if (NewBotSt_block_index==from->block)
2815 if (0== --from->no_of_outgoing_block_inert_transitions)
2817 change_non_bottom_state_to_bottom_state(from);
2829 { assert(m_states.begin()+m_aut.get_transitions()[*splitter_it].from()==
2832 out_it=m_transitions[*splitter_it].ref_outgoing_transitions;
2833 if (out_it<out_it->start_same_saC)
2835 out_it=out_it->start_same_saC;
2839 out_it_end=std::next(src.ref_state)>=m_states.end()
2840 ? m_outgoing_transitions.end()
2841 : std::next(src.ref_state)->start_outgoing_transitions;
2842 if (out_it<out_it_end)
2844 return m_transitions[*out_it->ref.BLC_transitions].
2845 transitions_per_block_to_constellation;
2929 template <
bool has_small_splitter,
bool has_large_splitter>
2931 linked_list<BLC_indicators>::iterator
const small_splitter,
2932 linked_list<BLC_indicators>::iterator
const large_splitter,
2944 static std::vector<state_in_block_pointer>potential_non_bottom_states[3]; assert(potential_non_bottom_states[ReachAlw].empty());
2945 assert(potential_non_bottom_states[AvoidSml].empty());
2946 assert(potential_non_bottom_states[AvoidLrg].empty());
2947 static std::vector<state_in_block_pointer>
2948 potential_non_bottom_states_HitSmall; assert(potential_non_bottom_states_HitSmall.empty());
2964 #define non_bottom_states_NewBotSt non_bottom_states[3
]
2982 #define bottom_size(coroutine) ( assert
(ReachAlw==(coroutine)||AvoidSml==(coroutine)||AvoidLrg==(coroutine)),
2983 assert
(start_bottom_states[(coroutine)]<=start_bottom_states[(coroutine)+1
]),
2984 static_cast<state_type>
2985 (std::distance(start_bottom_states[(coroutine)],
2986 start_bottom_states[(coroutine)+1
])))
2987 #define bottom_and_non_bottom_size(coroutine) ( assert
(aborted!=status[(coroutine)]),
2988 bottom_size((coroutine))+non_bottom_states[(coroutine)].size())
2998 if (has_small_splitter )
2999 { assert(bi->block.to_constellation.end()!=small_splitter);
3004 main_t=m_aut.get_transitions()[*small_splitter->start_same_BLC];
3005 assert(bi==m_states[main_t.from()].block);
3019 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3024 if (has_large_splitter )
3025 { assert(bi->block.to_constellation.end()!=large_splitter);
3027 four_way_splitB__handle_transitions_in_main_splitter, max_C), *
this);
3029 const transition& co_t=m_aut.get_transitions()[*large_splitter->start_same_BLC];
3030 assert(bi==m_states[co_t.from()].block);
3036 large_splitter_iter_NewBotSt=large_splitter->start_same_BLC; assert(new_constellation==m_states[main_t.to()].block->c.onstellation);
3037 large_splitter_iter_end_NewBotSt=large_splitter->end_same_BLC; assert(old_constellation==m_states[co_t.to()].block->c.onstellation);
3040 { assert(bi->block.to_constellation.end()==large_splitter);
3042 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3046 four_way_splitB__handle_transitions_in_main_splitter, max_C), *
this);
3047 assert(new_constellation==m_states[main_t.to()].block->c.onstellation);
3051 refine_partition_until_it_becomes_stable__prepare_cosplit,max_C),*
this);
3056 assert(old_constellation==m_states[main_t.to()].block->c.onstellation);
3060 large_splitter_iter_NewBotSt=m_BLC_transitions.data_end();
3061 large_splitter_iter_end_NewBotSt=m_BLC_transitions.data_end();
3067 BLC_list_iterator splitter_it=small_splitter->start_same_BLC; assert(splitter_it!=small_splitter->end_same_BLC);
3070 state_in_block_pointer
const src=m_states.begin()+
3071 m_aut.get_transitions()[*splitter_it].from();
3072 if (0==src.ref_state->no_of_outgoing_block_inert_transitions)
3073 { assert(bi->start_bottom_states<=src.ref_state->ref_states_in_blocks);
3074 assert(src.ref_state->ref_states_in_blocks<bi->sta.rt_non_bottom_states);
3075 if (src.ref_state->ref_states_in_blocks<
3076 start_bottom_states[AvoidSml])
3079 if (has_large_splitter) {
3080 assert(next_target_constln_in_same_saC(src, splitter_it)==large_splitter);
3084 else if (!has_large_splitter )
3086 assert(ReachAlw+1==AvoidSml);
3087 swap_states_in_states_in_block(start_bottom_states[AvoidSml],
3088 src.ref_state->ref_states_in_blocks);
3089 ++start_bottom_states[AvoidSml];
3091 else if (start_bottom_states[AvoidSml+1]<=
3092 src.ref_state->ref_states_in_blocks)
3095 assert(bi->block.to_constellation.end()!=large_splitter);
3096 outgoing_transitions_const_it
const out_it_end=std::next(src.ref_state)>=
3097 m_states.end() ? m_outgoing_transitions.end()
3098 : std::next(src.ref_state)->start_outgoing_transitions;
3099 for (outgoing_transitions_const_it out_it=src.ref_state->
3100 start_outgoing_transitions; out_it!=out_it_end; ++out_it)
3102 assert(m_transitions[*out_it->ref.BLC_transitions].
3103 transitions_per_block_to_constellation!=large_splitter);
3107 else if (next_target_constln_in_same_saC(src, splitter_it)==
3110 assert(ReachAlw+1==AvoidSml);
3111 swap_states_in_states_in_block(start_bottom_states[AvoidSml],
3112 src.ref_state->ref_states_in_blocks);
3113 ++start_bottom_states[AvoidSml];
3117 assert(AvoidSml+1==AvoidLrg);
3118 --start_bottom_states[AvoidSml+1];
3119 swap_states_in_states_in_block(start_bottom_states[AvoidSml+1],
3120 src.ref_state->ref_states_in_blocks);
3125 assert(bi->sta.rt_non_bottom_states<=src.ref_state->ref_states_in_blocks);
3126 assert(src.ref_state->ref_states_in_blocks<bi->end_states);
3127 if (undefined==src.ref_state->counter)
3129 if (!has_large_splitter ||
3130 next_target_constln_in_same_saC(src, splitter_it)==
3134 src.ref_state->counter=marked(ReachAlw)+
3135 src.ref_state->no_of_outgoing_block_inert_transitions; assert(is_in_marked_range_of(src.ref_state->counter, ReachAlw));
3137 potential_non_bottom_states[ReachAlw].push_back(src);
3142 src.ref_state->counter=marked_HitSmall;
3143 potential_non_bottom_states_HitSmall.push_back(src);
3145 outgoing_transitions_const_it
const out_it_end=std::next(src.ref_state)>=
3146 m_states.end() ? m_outgoing_transitions.end()
3147 : std::next(src.ref_state)->start_outgoing_transitions;
3148 for (outgoing_transitions_const_it out_it=src.ref_state->
3149 start_outgoing_transitions; out_it!=out_it_end; ++out_it)
3151 assert(has_small_splitter || has_large_splitter),
3152 assert(m_transitions[*out_it->ref.BLC_transitions].
3153 transitions_per_block_to_constellation!=large_splitter);
3159 else if (marked_HitSmall==src.ref_state->counter) {
3160 assert(bi->block.to_constellation.end()!=large_splitter);
3162 assert(is_in_marked_range_of(src.ref_state->counter, ReachAlw));
3163 if (bi->block.to_constellation.end()!=large_splitter) {
3164 assert(has_small_splitter || has_large_splitter),
3165 assert(next_target_constln_in_same_saC(src,splitter_it)==large_splitter);
3172 while (splitter_it!=small_splitter->end_same_BLC);
3174 else if (has_large_splitter )
3175 { assert(bi->block.to_constellation.end()==small_splitter);
3176 assert(bi->block.to_constellation.end()!=large_splitter);
3177 assert(!large_splitter->is_stable());
3185 large_splitter_iter_NewBotSt=large_splitter->start_same_BLC;
3186 large_splitter_iter_end_NewBotSt=large_splitter->start_marked_BLC;
3188 for (BLC_list_iterator co_splitter_it=large_splitter->start_marked_BLC;
3189 co_splitter_it!=large_splitter->end_same_BLC; ++co_splitter_it)
3191 state_in_block_pointer
const src=m_states.begin()+
3192 m_aut.get_transitions()[*co_splitter_it].from(); assert(0==src.ref_state->no_of_outgoing_block_inert_transitions);
3193 assert(bi->start_bottom_states<=src.ref_state->ref_states_in_blocks);
3194 assert(src.ref_state->ref_states_in_blocks<bi->sta.rt_non_bottom_states);
3195 if (start_bottom_states[AvoidSml]<=
3196 src.ref_state->ref_states_in_blocks)
3198 swap_states_in_states_in_block(start_bottom_states[AvoidSml],
3199 src.ref_state->ref_states_in_blocks);
3200 ++start_bottom_states[AvoidSml];
3205 make_stable_and_move_to_start_of_BLC(bi, large_splitter);
3208 { assert(bi->block.to_constellation.end()==small_splitter);
3209 assert(bi->block.to_constellation.end()==large_splitter);
3222 potential_non_bottom_states[ReachAlw].swap(*bi->block.R); assert(
null_constellation==old_constellation);
3231 for (state_in_block_pointer st: potential_non_bottom_states[ReachAlw]) {
3232 assert(0<st.ref_state->no_of_outgoing_block_inert_transitions);
3233 assert(st.ref_state->counter==marked(ReachAlw)+
3234 st.ref_state->no_of_outgoing_block_inert_transitions);
3235 assert(is_in_marked_range_of(st.ref_state->counter, ReachAlw));
3238 large_splitter_iter_NewBotSt=m_BLC_transitions.data_end();
3239 large_splitter_iter_end_NewBotSt=m_BLC_transitions.data_end();
3253 bool constellation_was_trivial=
3256 bool constellation_becomes_nontrivial=
false;
3262 ReachAlw_block_index=create_new_block
3263 <!has_small_splitter && !has_large_splitter>
3266 start_bottom_states[
ReachAlw+1], bi,
3267 old_constellation, new_constellation);
3268 constellation_becomes_nontrivial=
true;
3276 create_new_block<!has_small_splitter && !has_large_splitter>
3279 start_bottom_states[
AvoidSml+1], bi,
3280 old_constellation, new_constellation);
3281 constellation_becomes_nontrivial=
true;
3288 create_new_block<!has_small_splitter && !has_large_splitter>
3291 start_bottom_states[
AvoidLrg+1], bi,
3292 old_constellation, new_constellation);
3293 constellation_becomes_nontrivial=
true;
3303 create_new_block<!has_small_splitter && !has_large_splitter>
3306 start_bottom_states[
AvoidLrg+1], bi,
3307 old_constellation, new_constellation);
3308 constellation_becomes_nontrivial=
true;
3310 if ((has_small_splitter || !has_large_splitter) &&
3314 ReachAlw_block_index=create_new_block
3315 <!has_small_splitter && !has_large_splitter>
3318 start_bottom_states[
ReachAlw+1], bi,
3319 old_constellation, new_constellation);
3320 constellation_becomes_nontrivial=
true;
3324 ReachAlw_block_index=bi;
3325 if ((has_small_splitter || !has_large_splitter) &&
3330 create_new_block<!has_small_splitter && !has_large_splitter>
3333 start_bottom_states[
AvoidSml+1], bi,
3334 old_constellation, new_constellation);
3335 constellation_becomes_nontrivial=
true;
3340 if (constellation_becomes_nontrivial && constellation_was_trivial)
3341 { assert(std::find(m_non_trivial_constellations.begin(),
3342 m_non_trivial_constellations.end(),
3343 constellation)==m_non_trivial_constellations.end());
3344 m_non_trivial_constellations.emplace_back(constellation);
3347 return ReachAlw_block_index;
3375 enum { state_checking,
3376 incoming_inert_transition_checking,
3377 outgoing_constellation_checking,
3378 aborted, finished } status[3], status_NewBotSt;
3392 #define abort_if_bottom_size_too_large(coroutine)
3393 (( assert
(non_bottom_states[(coroutine)].empty()),
3394 bottom_size((coroutine))>no_of_unfinished_states_in_block/2
) &&
3395 ( assert
(std::numeric_limits<state_index>::max()!=
3396 no_of_unfinished_states_in_block),
3397 no_of_unfinished_states_in_block=
3398 std::numeric_limits<state_index>::max(), assert
(m_aut.num_states()<no_of_unfinished_states_in_block/2
),
3399 status[(coroutine)]=aborted,
3413 #define abort_if_non_bottom_size_too_large_NewBotSt(i)
3414 (( assert
(aborted!=status_NewBotSt),
3416 no_of_unfinished_states_in_block/2
) &&
3417 ( assert
(std::numeric_limits<state_index>::max()!=
3418 no_of_unfinished_states_in_block),
3419 no_of_unfinished_states_in_block=
3420 std::numeric_limits<state_index>::max(), assert
(m_aut.num_states()<no_of_unfinished_states_in_block/2
),
3421 status_NewBotSt=aborted,
3436 #define abort_if_size_too_large(coroutine, i)
3437 (bottom_and_non_bottom_size((coroutine))+(i)>
3438 no_of_unfinished_states_in_block/2
&&
3439 ( assert
(std::numeric_limits<state_index>::max()!=
3440 no_of_unfinished_states_in_block),
3441 no_of_unfinished_states_in_block=
3442 std::numeric_limits<state_index>::max(), assert
(m_aut.num_states()<no_of_unfinished_states_in_block/2
),
3443 status[(coroutine)]=aborted,
3444 non_bottom_states[(coroutine)].clear(),
3447 int no_of_finished_searches=0;
3448 int no_of_running_searches=0;
3451 if ((!has_small_splitter && has_large_splitter) ||
3454 assert(potential_non_bottom_states[AvoidSml].empty());
3465 clear_state_counters(potential_non_bottom_states[ReachAlw].begin(),
3466 potential_non_bottom_states[ReachAlw].end(), bi);
3467 clear(potential_non_bottom_states[ReachAlw]);
3468 if (has_small_splitter && has_large_splitter)
3470 clear_state_counters(potential_non_bottom_states_HitSmall.begin(),
3471 potential_non_bottom_states_HitSmall.end(), bi);
3472 clear(potential_non_bottom_states_HitSmall);
3473 }
else { assert(potential_non_bottom_states_HitSmall.empty()); }
3477 ++no_of_finished_searches;
3482 running_searches[no_of_running_searches]=
AvoidSml;
3483 ++no_of_running_searches;
3490 assert(potential_non_bottom_states[AvoidLrg].empty());
3491 ++no_of_finished_searches;
3496 running_searches[no_of_running_searches]=
AvoidLrg;
3497 ++no_of_running_searches;
3502 status_NewBotSt=state_checking;
3510 (potential_non_bottom_states[ReachAlw]);
3511 if (!has_large_splitter || finished==status[
AvoidLrg])
3512 { assert(finished==status[
AvoidLrg]);
3516 if (has_small_splitter && has_large_splitter)
3521 (potential_non_bottom_states_HitSmall.begin(),
3522 potential_non_bottom_states_HitSmall.end());
3523 clear(potential_non_bottom_states_HitSmall);
3528 (potential_non_bottom_states_HitSmall);
3530 }
else { assert(potential_non_bottom_states_HitSmall.empty()); }
3535 st.ref_state->counter=marked_NewBotSt;
3537 ++no_of_finished_searches;
3543 running_searches[no_of_running_searches]=
ReachAlw;
3544 ++no_of_running_searches;
3568 std::vector<transition>::iterator current_source_iter[3],
3569 current_source_iter_NewBotSt;
3570 std::vector<transition>::const_iterator current_source_iter_end[3],
3571 current_source_iter_end_NewBotSt;
3577 { assert(2>=no_of_finished_searches);
3580 #define new_start_bottom_states(idx) (assert
(1
<=(idx)), assert
((idx)<=3
), new_start_bottom_states_plus_one[(idx)-1
])
3581 #define new_end_bottom_states(idx) (assert
(1
<=(idx)), assert
((idx)<=2
), new_end_bottom_states_plus_one[(idx)-1
])
3582 #define new_end_bottom_states_NewBotSt (new_start_bottom_states_plus_one[2
])
3583 for (
int current_search_index=0; current_search_index<
3584 no_of_running_searches; ++current_search_index)
3587 current_search=running_searches[current_search_index]; assert(0<=current_search); assert(current_search<
NewBotSt);
3589 if (incoming_inert_transition_checking==status[current_search])
3590 { assert(current_source_iter[current_search]<
3591 current_source_iter_end[current_search]);
3592 mCRL2complexity(&m_transitions[std::distance(m_aut.get_transitions().begin(),
3593 current_source_iter[current_search])], add_work(check_complexity::
3594 simple_splitB_U__handle_transition_to_U_state, 1), *
this);
3598 if (src.ref_state->block==bi &&
3605 if( ( ( undefined==current_counter
3606 || ( has_small_splitter && has_large_splitter
3607 && marked_HitSmall==current_counter
3608 && AvoidSml!=current_search ) || (assert(marked_HitSmall!=current_counter || AvoidSml==current_search),
false)
3611 src.ref_state->counter=marked(current_search)+
3612 src.ref_state->no_of_outgoing_block_inert_transitions, assert(std::find(potential_non_bottom_states[current_search].begin(),
3613 potential_non_bottom_states[current_search].end(), src)==
3614 potential_non_bottom_states[current_search].end()),
3615 potential_non_bottom_states[current_search].
3618 || is_in_marked_range_of(current_counter, current_search) )
3619 { assert(is_in_marked_range_of(src.ref_state->counter, current_search));
3621 --src.ref_state->counter; assert(is_in_marked_range_of(src.ref_state->counter, current_search));
3623 if (
marked(current_search
)==src.ref_state->counter)
3624 {
if (!has_large_splitter) {
3626 if (!has_small_splitter) { assert(
marked_HitSmall!=current_counter); }
3628 if (has_large_splitter &&
3630 large_splitter_iter_NewBotSt!=
3631 large_splitter_iter_end_NewBotSt)
3632 { assert(bi->block.to_constellation.end()!=large_splitter);
3639 current_source_AvoidLrg=src;
3640 status[
AvoidLrg]=outgoing_constellation_checking;
3641 current_outgoing_iter_start_AvoidLrg=
3642 src.ref_state->start_outgoing_transitions;
3643 current_outgoing_iter_AvoidLrg=
3644 std::next(src.ref_state)>=m_states.end()
3645 ? m_outgoing_transitions.end()
3646 : std::next(src.ref_state)->start_outgoing_transitions; assert(current_outgoing_iter_start_AvoidLrg<current_outgoing_iter_AvoidLrg);
3648 }
else { assert(
AvoidLrg!=current_search ||
3649 large_splitter_iter_NewBotSt==large_splitter_iter_end_NewBotSt); }
3651 { assert(running_searches[current_search_index]==current_search);
3652 --no_of_running_searches; assert(current_search_index<=no_of_running_searches);
3653 running_searches[current_search_index]=
3654 running_searches[no_of_running_searches]; assert(std::find(potential_non_bottom_states[current_search].begin(),
3655 potential_non_bottom_states[current_search].end(), src)!=
3656 potential_non_bottom_states[current_search].end());
3657 --current_search_index;
3671 if (aborted!=status_NewBotSt &&
3685 if (current_source_iter[current_search]!=
3686 current_source_iter_end[current_search] &&
3687 m_aut.is_tau(m_aut_apply_hidden_label_map
3688 (current_source_iter[current_search]->label())))
3692 status[current_search]=state_checking;
3694 else if (!has_large_splitter||state_checking==status[current_search])
3695 { assert(state_checking==status[current_search]);
3698 current_bottom_state_iter[current_search]<
3699 start_bottom_states[current_search+1]
3700 ? *current_bottom_state_iter[current_search]++
3705 current_source_iter[current_search]=
3706 tgt.ref_state->start_incoming_transitions; assert(!non_bottom_states[current_search^2]
.find(tgt
));
3707 current_source_iter_end[current_search]=
3708 std::next(tgt.ref_state)>=m_states.end()
3709 ? m_aut.get_transitions().end()
3710 : std::next(tgt.ref_state)->start_incoming_transitions; assert(!non_bottom_states[current_search^3]
.find(tgt
));
3711 if (current_source_iter[current_search]<
3712 current_source_iter_end[current_search] &&
3713 m_aut.is_tau(m_aut_apply_hidden_label_map
3714 (current_source_iter[current_search]->label())))
3716 status[current_search]=incoming_inert_transition_checking;
3721 { assert(
AvoidLrg==current_search);
3722 assert(outgoing_constellation_checking==status[
AvoidLrg]);
3723 assert(current_outgoing_iter_start_AvoidLrg<current_outgoing_iter_AvoidLrg);
3724 assert(m_outgoing_transitions.end()==current_outgoing_iter_AvoidLrg ||
3725 current_outgoing_iter_start_AvoidLrg<
3726 current_outgoing_iter_AvoidLrg->start_same_saC);
3727 --current_outgoing_iter_AvoidLrg; assert(current_outgoing_iter_AvoidLrg->start_same_saC<=
3728 current_outgoing_iter_AvoidLrg);
3729 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3732 current_outgoing_iter_AvoidLrg->start_same_saC;
3733 assert(has_small_splitter || has_large_splitter);
3735 add_work(check_complexity::
3736 simple_splitB_U__handle_transition_from_potential_U_state, 1), *
this);
3738 while (++out_it<=current_outgoing_iter_AvoidLrg) {
3739 assert(has_small_splitter || has_large_splitter);
3741 add_work_notemporary(check_complexity::
3742 simple_splitB_U__handle_transition_from_potential_U_state, 1), *
this);
3751 assert(has_small_splitter || has_large_splitter);
3752 linked_list<BLC_indicators>::const_iterator
const current_splitter=
3754 *current_outgoing_iter_AvoidLrg->ref.BLC_transitions].
3755 transitions_per_block_to_constellation; assert(bi->block.to_constellation.end()!=large_splitter);
3756 if (current_splitter==large_splitter)
3766 if (aborted!=status_NewBotSt &&
3768 { assert(aborted!=status_NewBotSt);
3779 else if (current_outgoing_iter_AvoidLrg=
3780 current_outgoing_iter_AvoidLrg->start_same_saC,
3781 current_outgoing_iter_start_AvoidLrg==
3782 current_outgoing_iter_AvoidLrg
3798 { assert(running_searches[current_search_index]==
AvoidLrg);
3799 --no_of_running_searches; assert(current_search_index<=no_of_running_searches);
3800 running_searches[current_search_index]=
3801 running_searches[no_of_running_searches]; assert(std::find(potential_non_bottom_states[AvoidLrg].begin(),
3802 potential_non_bottom_states[AvoidLrg].end(), current_source_AvoidLrg)!=
3803 potential_non_bottom_states[AvoidLrg].end());
3804 --current_search_index;
3817 if (current_source_iter[AvoidLrg]!=
3818 current_source_iter_end[AvoidLrg] &&
3819 m_aut.is_tau(m_aut_apply_hidden_label_map
3820 (current_source_iter[AvoidLrg]->label())))
3822 status[
AvoidLrg]=incoming_inert_transition_checking;
3828 assert(state_checking==status[current_search]);
3831 if (current_bottom_state_iter[current_search]==
3832 start_bottom_states[current_search+1] &&
3837 status[current_search]=finished;
3838 ++no_of_finished_searches;
3839 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3851 (s!=start_bottom_states[current_search+1] ||
3852 (s=non_bottom_states[current_search]
.data(),
true)) &&
3853 s!=non_bottom_states[current_search]
.data_end(); ++s)
3859 const std::vector<transition>::const_iterator in_ti_end=
3860 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
3861 : std::next(s->ref_state)->start_incoming_transitions;
3862 for (std::vector<transition>::const_iterator
3863 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
3865 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
3867 cbegin(), ti)], finalise_work(check_complexity::
3868 simple_splitB_U__handle_transition_to_U_state, check_complexity::
3869 simple_splitB__handle_transition_to_R_or_U_state, max_new_B), *
this);
3871 if (has_large_splitter &&
AvoidLrg==current_search &&
3872 0!=s->ref_state->no_of_outgoing_block_inert_transitions)
3876 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
3877 : std::next(s->ref_state)->start_outgoing_transitions;
3879 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
3881 assert(has_small_splitter || has_large_splitter);
3883 finalise_work(check_complexity::
3884 simple_splitB_U__handle_transition_from_potential_U_state,
3886 simple_splitB__handle_transition_from_R_or_U_state,
3889 }
else { assert(
AvoidLrg!=current_search ||
3890 0==s->ref_state->no_of_outgoing_block_inert_transitions); }
3892 if (has_large_splitter &&
AvoidLrg==current_search)
3905 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
3906 : std::next(s->ref_state)->start_outgoing_transitions;
3908 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
3910 assert(has_small_splitter || has_large_splitter);
3911 mCRL2complexity(&m_transitions[*ti->ref.BLC_transitions], finalise_work
3913 simple_splitB_U__handle_transition_from_potential_U_state,
3915 simple_splitB__test_outgoing_transitions_found_new_bottom_state,
3924 }
else { assert(
AvoidLrg!=current_search); }
3927 if (3>no_of_finished_searches)
3930 assert(finished!=status_NewBotSt);
3942 +potential_non_bottom_states[current_search].size()
3943 -non_bottom_states[current_search].size());
3945 for (state_in_block_pointer st:
3946 potential_non_bottom_states[current_search])
3950 if (marked_NewBotSt!=st.ref_state->counter)
3951 { assert(is_in_marked_range_of(st.ref_state->counter, current_search));
3952 if (marked(current_search)!=st.ref_state->counter)
3954 assert(!non_bottom_states[ReachAlw].find(st));
3963 st.ref_state->counter=marked_NewBotSt; assert(!non_bottom_states[AvoidSml].find(st));
3964 }
else { assert(non_bottom_states[current_search].find(st)); }
3965 }
else { assert(!non_bottom_states[current_search].find(st)); }
3966 } assert(running_searches[current_search_index]==current_search);
3967 clear(potential_non_bottom_states[current_search]);
3968 --no_of_running_searches; assert(current_search_index<=no_of_running_searches);
3969 running_searches[current_search_index]=
3970 running_searches[no_of_running_searches];
3971 --current_search_index; assert((has_small_splitter && has_large_splitter) ||
3972 potential_non_bottom_states_HitSmall.empty());
3973 if (has_small_splitter && has_large_splitter &&
3975 aborted!=status_NewBotSt)
3976 { assert(1>=no_of_running_searches);
3978 assert(finished!=status[
AvoidSml]);
3979 assert(finished!=status_NewBotSt);
3980 for (state_in_block_pointer st:
3981 potential_non_bottom_states_HitSmall)
3982 { assert(0<st.ref_state->no_of_outgoing_block_inert_transitions);
3986 assert(!non_bottom_states[AvoidSml].find(st));
3987 if (marked_HitSmall==st.ref_state->counter)
3990 st.ref_state->counter=marked_NewBotSt; assert(!non_bottom_states[AvoidLrg].find(st));
3991 }
else { assert(marked(ReachAlw)==st.ref_state->counter ||
3992 marked(AvoidLrg)==st.ref_state->counter ||
3993 marked_NewBotSt==st.ref_state->counter); }
3995 clear(potential_non_bottom_states_HitSmall);
3996 }
else { assert(finished!=status[ReachAlw] || finished!=status[AvoidLrg] ||
3997 aborted==status_NewBotSt ||
3998 potential_non_bottom_states_HitSmall.empty()); }
4000 no_of_unfinished_states_in_block)
4001 { assert(0<no_of_running_searches); assert(no_of_running_searches<=2);
4003 no_of_unfinished_states_in_block-=
4005 assert(finished!=status[running_searches[0]]);
4006 assert(aborted!=status[
AvoidSml]); assert(aborted!=status_NewBotSt);
4015 running_searches[0]=running_searches[1];
4017 if (0==current_search_index)
4019 --current_search_index;
4021 --no_of_running_searches;
4023 else if (1<no_of_running_searches && ( assert(aborted!=status[running_searches[1]]),
4024 assert(finished!=status[running_searches[1]]),
4031 --no_of_running_searches; assert(1==no_of_running_searches);
4043 assert(finished==status[
ReachAlw]);
4058 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4065 if (has_large_splitter) {
4073 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
4074 : std::next(s->ref_state)->start_outgoing_transitions;
4076 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4078 assert(has_small_splitter || has_large_splitter);
4080 cancel_work(check_complexity::
4081 simple_splitB_R__handle_transition_from_R_state), *
this);
4091 const std::vector<transition>::iterator in_ti_end=
4092 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
4093 : std::next(s->ref_state)->start_incoming_transitions;
4094 for (std::vector<transition>::iterator
4095 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
4097 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
4099 get_transitions().begin(), ti)], cancel_work(check_complexity::
4100 simple_splitB_R__handle_transition_to_R_state), *
this);
4102 if (has_large_splitter) {
4105 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
4106 : std::next(s->ref_state)->start_outgoing_transitions;
4108 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4110 assert(has_small_splitter || has_large_splitter);
4112 cancel_work(check_complexity::
4113 simple_splitB_R__handle_transition_from_R_state), *
this);
4127 if (!has_large_splitter ||
4128 (has_small_splitter &&
4139 status_NewBotSt=finished;
4140 status[max_process]=aborted;
4142 clear(potential_non_bottom_states[current_search]); assert(potential_non_bottom_states[max_process].empty());
4143 non_bottom_states[max_process].swap_vec
4144 (potential_non_bottom_states[max_process]);
4146 for (state_in_block_pointer st: potential_non_bottom_states_HitSmall) {
4147 assert(has_small_splitter); assert(has_large_splitter);
4148 assert(marked(ReachAlw)==st.ref_state->counter ||
4149 marked(AvoidLrg)==st.ref_state->counter);
4152 if (has_small_splitter && has_large_splitter)
4154 clear(potential_non_bottom_states_HitSmall);
4156 goto end_for_empty_NewBotSt_subblock;
4162 { assert(std::find(m_non_trivial_constellations.begin(),
4163 m_non_trivial_constellations.end(),
4164 constellation)==m_non_trivial_constellations.end());
4165 m_non_trivial_constellations.emplace_back(constellation);
4176 clear_state_counters
4177 (potential_non_bottom_states[current_search].begin(),
4178 potential_non_bottom_states[current_search].end(), bi);
4179 clear(potential_non_bottom_states[current_search]); assert(potential_non_bottom_states[ReachAlw].empty());
4180 assert(potential_non_bottom_states[AvoidLrg].empty());
4181 assert(potential_non_bottom_states[AvoidSml].empty());
4187 clear_state_counters
4188 (potential_non_bottom_states_HitSmall.begin(),
4189 potential_non_bottom_states_HitSmall.end(), bi);
4190 clear(potential_non_bottom_states_HitSmall); assert(has_large_splitter ||
4193 if (has_large_splitter &&
4199 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4203 if (start_bottom_states[
AvoidLrg]!=
4209 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4217 create_new_block<!has_small_splitter && !has_large_splitter>
4221 old_constellation, new_constellation);
4223 (NewBotSt_block_index
,
4232 if (!has_large_splitter ||
4233 (has_small_splitter &&
4240 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4244 if (start_bottom_states[
AvoidSml]!=
4250 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4258 create_new_block<!has_small_splitter && !has_large_splitter>
4262 old_constellation, new_constellation);
4264 (NewBotSt_block_index
,
4275 if (start_bottom_states[
ReachAlw]!=
4280 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4285 ReachAlw_block_index=create_new_block
4286 <!has_small_splitter && !has_large_splitter>
4290 old_constellation, new_constellation);
4292 (NewBotSt_block_index
,
4300 m_blocks_with_new_bottom_states.push_back(NewBotSt_block_index);
4302 return ReachAlw_block_index;
4308 if (incoming_inert_transition_checking==status_NewBotSt)
4309 { assert(current_source_iter_NewBotSt<current_source_iter_end_NewBotSt);
4310 mCRL2complexity(&m_transitions[std::distance(m_aut.get_transitions().begin(),
4311 current_source_iter_NewBotSt)], add_work(check_complexity::
4312 simple_splitB_R__handle_transition_to_R_state, 1), *
this);
4316 if (src.ref_state->block==bi &&
4336 if (current_source_iter_NewBotSt==current_source_iter_end_NewBotSt ||
4337 !m_aut.is_tau(m_aut_apply_hidden_label_map
4338 (current_source_iter_NewBotSt->label())))
4340 status_NewBotSt=state_checking;
4343 else if (state_checking==status_NewBotSt)
4352 current_source_iter_NewBotSt=
4353 tgt.ref_state->start_incoming_transitions;
4354 current_source_iter_end_NewBotSt=
4355 std::next(tgt.ref_state)>=m_states.end()
4356 ? m_aut.get_transitions().end()
4357 : std::next(tgt.ref_state)->start_incoming_transitions;
4358 if(current_source_iter_NewBotSt<current_source_iter_end_NewBotSt &&
4359 m_aut.is_tau(m_aut_apply_hidden_label_map
4360 (current_source_iter_NewBotSt->label())))
4362 status_NewBotSt=incoming_inert_transition_checking;
4367 if (1>=no_of_finished_searches)
4369 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4377 if (has_large_splitter && finished!=status[
AvoidLrg] &&
4378 large_splitter_iter_NewBotSt!=large_splitter_iter_end_NewBotSt)
4386 t=
m_aut.get_transitions()[*large_splitter_iter_NewBotSt];
mCRL2complexity(&m_transitions[*large_splitter_iter_NewBotSt],
4387 add_work(check_complexity::
4388 simple_splitB_R__handle_transition_from_R_state, 1), *
this);
4389 ++large_splitter_iter_NewBotSt;
4392 if (0==src.ref_state->no_of_outgoing_block_inert_transitions)
4393 { assert(!(start_bottom_states[
AvoidLrg]<=src.ref_state->ref_states_in_blocks &&
4394 src.ref_state->ref_states_in_blocks<start_bottom_states[
AvoidLrg+1]));
4399 if ((
undefined==src.ref_state->counter) ||
4400 is_in_marked_range_of(src.ref_state->counter,
AvoidLrg))
4408 if (0==no_of_running_searches)
4424 if (0!=no_of_running_searches)
4429 while ( assert(0==no_of_running_searches), assert(aborted==status[
AvoidLrg]),
4430 large_splitter_iter_NewBotSt!=large_splitter_iter_end_NewBotSt);
4433 { assert(finished==status[
AvoidLrg] ||
4434 large_splitter_iter_NewBotSt==large_splitter_iter_end_NewBotSt);
4459 status_NewBotSt=finished; assert(3==++no_of_finished_searches);
4467 if (!has_large_splitter || finished==status[
AvoidLrg])
4468 { assert(finished==status[
AvoidLrg]);
4474 if ((!has_small_splitter && has_large_splitter) ||
4484 clear_state_counters
4485 (potential_non_bottom_states[ReachAlw].begin(),
4486 potential_non_bottom_states[ReachAlw].end(), bi);
4487 clear(potential_non_bottom_states[ReachAlw]);
4490 if (has_small_splitter && has_large_splitter)
4492 clear_state_counters
4493 (potential_non_bottom_states_HitSmall.begin(),
4494 potential_non_bottom_states_HitSmall.end(), bi);
4495 }
else { assert(potential_non_bottom_states_HitSmall.empty()); }
4498 { assert(finished==status[
ReachAlw]);
4506 clear_state_counters
4507 (potential_non_bottom_states[AvoidSml].begin(),
4508 potential_non_bottom_states[AvoidSml].end(), bi);
4509 clear(potential_non_bottom_states[AvoidSml]);
4515 { assert(finished==status[
ReachAlw]);
4528 clear_state_counters
4529 (potential_non_bottom_states[AvoidLrg].begin(),
4530 potential_non_bottom_states[AvoidLrg].end(), bi);
4531 clear(potential_non_bottom_states[AvoidLrg]);
4532 if (has_small_splitter)
4535 clear_state_counters
4536 (potential_non_bottom_states_HitSmall.begin(),
4537 potential_non_bottom_states_HitSmall.end(), bi);
4538 }
else { assert(potential_non_bottom_states_HitSmall.empty()); }
4540 if (has_small_splitter && has_large_splitter)
4542 clear(potential_non_bottom_states_HitSmall);
4543 }
else { assert(potential_non_bottom_states_HitSmall.empty()); }
4544 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4559 const unsigned char max_NcludeCo_B=
4566 const std::vector<transition>::const_iterator in_ti_end=
4567 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
4568 : std::next(s->ref_state)->start_incoming_transitions;
4569 for (std::vector<transition>::const_iterator
4570 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
4572 if(!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
4574 cbegin(), ti)], cancel_work(check_complexity::
4575 simple_splitB_U__handle_transition_to_U_state), *
this);
4577 if (has_large_splitter && finished!=status[
AvoidLrg]) {
4580 std::next(s->ref_state)>=m_states.end() ? m_outgoing_transitions.end()
4581 : std::next(s->ref_state)->start_outgoing_transitions;
4583 ti=s->ref_state->start_outgoing_transitions; ti!=out_ti_end; ++ti)
4585 assert(has_small_splitter || has_large_splitter);
4587 cancel_work(check_complexity::
4588 simple_splitB_U__handle_transition_from_potential_U_state), *
this);
4592 finalise_work(check_complexity::
4593 simple_splitB_R__handle_transition_from_R_state,
4595 simple_splitB__handle_transition_from_R_or_U_state,
4596 max_NcludeCo_B), *
this);
4598 }
else { assert(finished==status[
AvoidLrg]); }
4615 { assert(std::find(m_non_trivial_constellations.begin(),
4616 m_non_trivial_constellations.end(),
4617 constellation)==m_non_trivial_constellations.end());
4618 m_non_trivial_constellations.emplace_back(constellation);
4623 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4629 create_new_block<!has_small_splitter && !has_large_splitter>
4634 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4646 const std::vector<transition>::iterator in_ti_end=
4647 std::next(s->ref_state)>=m_states.end() ? m_aut.get_transitions().end()
4648 : std::next(s->ref_state)->start_incoming_transitions;
4649 for (std::vector<transition>::iterator
4650 ti=s->ref_state->start_incoming_transitions; ti!=in_ti_end; ++ti)
4652 if (!m_aut.is_tau(m_aut_apply_hidden_label_map(ti->label()))) {
break; }
4654 begin(), ti)], finalise_work(check_complexity::
4655 simple_splitB_R__handle_transition_to_R_state, check_complexity::
4656 simple_splitB__handle_transition_to_R_or_U_state, max_new_B), *
this);
4669 std::next(nst_it->ref_state)>=m_states.end()
4670 ? m_outgoing_transitions.end()
4671 : std::next(nst_it->ref_state)->start_outgoing_transitions;
4673 start_outgoing_transitions; assert(out_it!=out_it_end);
4675 [has_small_splitter || has_large_splitter
4676 ?*out_it->ref.BLC_transitions :out_it->ref.transitions]; assert(0<nst_it->ref_state->no_of_outgoing_block_inert_transitions);
4678 { assert(m_states.begin()+tr->from()==nst_it->ref_state);
4680 if (m_states[tr->to()].block==bi)
4682 assert(bi->start_bottom_states<=m_states[tr->to()].ref_states_in_blocks);
4685 assert(0<nst_it->ref_state->no_of_outgoing_block_inert_transitions);
4686 if (0== --nst_it->ref_state->
4687 no_of_outgoing_block_inert_transitions)
4690 change_non_bottom_state_to_bottom_state
4691 (nst_it->ref_state);
4696 m_states[tr->to()].ref_states_in_blocks ||
4697 m_states[tr->to()].ref_states_in_blocks<start_bottom_states[ReachAlw]);
4701 while (out_it!=out_it_end &&
4702 (tr=&
m_aut.get_transitions()
4703 [has_small_splitter || has_large_splitter
4704 ?*out_it->ref.BLC_transitions :out_it->ref.transitions],
4711 m_blocks_with_new_bottom_states.push_back(NewBotSt_block_index);
4723 { assert(std::find(m_non_trivial_constellations.begin(),
4724 m_non_trivial_constellations.end(),
4725 constellation)==m_non_trivial_constellations.end());
4738 if (start_bottom_states[
AvoidLrg]!=
4741 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4745 acct_iter=start_bottom_states[
AvoidLrg];
4779 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4790 { assert(potential_non_bottom_states[AvoidLrg].empty());
4793 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4798 create_new_block<!has_small_splitter && !has_large_splitter>
4802 old_constellation, new_constellation);
4806 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4819 assert(finished==status[
AvoidLrg]);
4824 if ((has_small_splitter || !has_large_splitter) &&
4831 if (start_bottom_states[
AvoidSml]!=
4837 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4851 { assert(potential_non_bottom_states[AvoidSml].empty());
4854 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4859 create_new_block<!has_small_splitter && !has_large_splitter>
4863 old_constellation, new_constellation);
4875 assert(finished==status[
AvoidSml]);
4881 if (start_bottom_states[
ReachAlw]!=
4885 { assert(potential_non_bottom_states[ReachAlw].empty());
4888 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
4893 ReachAlw_block_index=create_new_block
4894 <!has_small_splitter && !has_large_splitter>
4898 old_constellation, new_constellation);
4904 ReachAlw_block_index=bi;
4909 return ReachAlw_block_index;
4912 assert(aborted==status_NewBotSt);
4917 #undef abort_if_bottom_size_too_large
4918 #undef abort_if_non_bottom_size_too_large_NewBotSt
4919 #undef abort_if_size_too_large
4920 #undef bottom_and_non_bottom_size
4925 std::vector<transition_index>& action_counter,
4926 const std::vector<label_index>& todo_stack)
const
4929 for(label_index index: todo_stack)
4931 transition_index n=sum;
4932 sum=sum+action_counter[index];
4933 action_counter[index]=n;
4947 { assert(start_same_BLC<end_same_BLC);
4950 block.to_constellation.emplace_back(start_same_BLC,end_same_BLC,
true);
4956 { assert(bi==m_states[m_aut.get_transitions()[*start_same_BLC].from()].block);
4957 m_transitions[*start_same_BLC].transitions_per_block_to_constellation=
4958 blc;
mCRL2complexity(&m_transitions[*start_same_BLC], add_work(check_complexity::
4959 order_BLC_transitions__sort_transition, check_complexity::log_n), *
this);
4960 m_transitions[*start_same_BLC].ref_outgoing_transitions->
4961 ref.convert_to_iterator(start_same_BLC);
4963 while (++start_same_BLC<end_same_BLC);
4987 { assert(start_same_BLC<end_same_BLC);
4988 assert(min_block->ref_state->block->start_bottom_states==min_block);
4989 assert(max_block->ref_state->block->start_bottom_states==max_block);
4990 if (min_block==max_block)
4993 start_same_BLC
, end_same_BLC
);
4995 }
else { assert(min_block<max_block); }
4996 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5001 pivot=pivot->ref_state->block->start_bottom_states;
5004 #define max_below_pivot min_block
5005 #define min_above_pivot max_block
5016 { assert(end_smaller_than_pivot<begin_larger_than_pivot);
5020 assert(it<=end_equal_to_pivot);
5021 for (; it<end_equal_to_pivot; ++it) {
5022 assert(m_states[m_aut.get_transitions()[*it].from()].block->
5023 start_bottom_states==pivot);
5025 assert(it<=end_smaller_than_pivot);
5026 for (; it<end_smaller_than_pivot; ++it) {
5028 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5029 start_bottom_states;
5032 assert(it<begin_larger_than_pivot);
5033 for (it=begin_larger_than_pivot; it<end_same_BLC; ++it) {
5035 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5036 start_bottom_states;
5042 check_complexity::order_BLC_transitions__sort_transition, max_sort), *
this);
5044 m_states[m_aut.get_transitions()
5045 [*end_smaller_than_pivot].from()].block->start_bottom_states;
5046 if (source_block==pivot)
5048 std::swap(*end_equal_to_pivot++, *end_smaller_than_pivot);
5050 else if (source_block>pivot)
5056 if (source_block>max_above_pivot)
5058 max_above_pivot=source_block;
5064 if (source_block<min_below_pivot)
5066 min_below_pivot=source_block;
5073 ++end_smaller_than_pivot;
5074 if (end_smaller_than_pivot>=begin_larger_than_pivot)
5076 goto break_two_loops;
5082 { assert(end_smaller_than_pivot<begin_larger_than_pivot);
5086 assert(it<=end_equal_to_pivot);
5087 for (; it<end_equal_to_pivot; ++it) {
5088 assert(m_states[m_aut.get_transitions()[*it].from()].block->
5089 start_bottom_states==pivot);
5091 assert(it<=end_smaller_than_pivot);
5092 for (; it<end_smaller_than_pivot; ++it) {
5094 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5095 start_bottom_states;
5099 sb=m_states[m_aut.get_transitions()[*it].from()].
5100 block->start_bottom_states;
5102 for (it=begin_larger_than_pivot; it<end_same_BLC; ++it) {
5103 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5104 start_bottom_states;
5109 --begin_larger_than_pivot;
5110 if (end_smaller_than_pivot>=begin_larger_than_pivot)
5112 goto break_two_loops;
5114 check_complexity::order_BLC_transitions__sort_transition, max_sort), *
this);
5116 m_states[m_aut.get_transitions()
5117 [*begin_larger_than_pivot].from()].block->start_bottom_states;
5118 if (source_block==pivot)
5119 { assert(end_smaller_than_pivot<begin_larger_than_pivot);
5120 transition_index temp=*begin_larger_than_pivot; assert(end_equal_to_pivot<=end_smaller_than_pivot);
5121 *begin_larger_than_pivot=*end_smaller_than_pivot;
5122 *end_smaller_than_pivot=*end_equal_to_pivot;
5123 *end_equal_to_pivot=temp;
5124 ++end_equal_to_pivot;
5125 ++end_smaller_than_pivot;
5126 if (end_smaller_than_pivot>=begin_larger_than_pivot)
5128 goto break_two_loops;
5132 if (source_block<pivot)
5134 if (source_block<min_below_pivot)
5136 min_below_pivot=source_block;
5142 std::swap(*end_smaller_than_pivot, *begin_larger_than_pivot);
5143 ++end_smaller_than_pivot;
5144 if (end_smaller_than_pivot>=begin_larger_than_pivot)
5146 goto break_two_loops;
5154 else if (source_block>max_above_pivot)
5156 max_above_pivot=source_block;
5160 break_two_loops: ; assert(end_smaller_than_pivot==begin_larger_than_pivot);
5164 assert(it<=end_equal_to_pivot);
5165 for (; it<end_equal_to_pivot; ++it) {
5166 assert(m_states[m_aut.get_transitions()[*it].from()].block->
5167 start_bottom_states==pivot);
5169 assert(it<=end_smaller_than_pivot);
5170 for (; it<end_smaller_than_pivot; ++it) {
5172 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5173 start_bottom_states;
5176 assert(it==begin_larger_than_pivot); assert(it<=end_same_BLC);
5177 for (; it<end_same_BLC; ++it) {
5179 sb=m_states[m_aut.get_transitions()[*it].from()].block->
5180 start_bottom_states;
5185 if (start_same_BLC<end_equal_to_pivot)
5188 start_same_BLC
, end_equal_to_pivot
);
5193 if (begin_larger_than_pivot<end_same_BLC)
5196 begin_larger_than_pivot
, end_same_BLC
);
5198 if (end_equal_to_pivot<begin_larger_than_pivot)
5207 if (end_equal_to_pivot<begin_larger_than_pivot)
5210 end_equal_to_pivot
, begin_larger_than_pivot
);
5212 if (begin_larger_than_pivot<end_same_BLC)
5218 } assert(end_equal_to_pivot<begin_larger_than_pivot);
5220 assert(begin_larger_than_pivot<end_same_BLC);
5227 #undef max_below_pivot
5228 #undef min_above_pivot
5236 template <
bool initialization=
false>
5239 if (m_blocks_with_new_bottom_states.empty() ||
5240 (initialization && m_BLC_transitions.empty()))
5246 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> > Qhat;
5247 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5248 std::vector<std::pair<BLC_list_const_iterator, BLC_list_const_iterator> >
5249 initialize_qhat_work_to_assign_later;
5250 std::vector<std::pair<BLC_list_const_iterator, BLC_list_const_iterator> >
5251 stabilize_work_to_assign_later;
5253 assert(!m_blocks_with_new_bottom_states.empty());
5254 for(block_type*
const bi: m_blocks_with_new_bottom_states)
5255 { assert(bi->contains_new_bottom_states);
5256 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5260 const state_in_block_pointer* new_bott_it=bi->start_bottom_states;
5261 assert(new_bott_it < bi->sta.rt_non_bottom_states);
5265 add_work(check_complexity::stabilizeB__prepare_block, 1), *
this);
5267 while (++new_bott_it<bi->sta.rt_non_bottom_states);
5269 bi->contains_new_bottom_states=
false; assert(!bi->block.to_constellation.empty());
5270 if (1>=number_of_states_in_block(*bi))
5276 ind=bi->block.to_constellation.begin(); assert(ind->start_same_BLC<ind->end_same_BLC);
5277 const transition* first_t;
5278 if(!initialization ||
5279 (first_t=&m_aut.get_transitions()[*ind->start_same_BLC], assert(m_states[first_t->from()].block==bi),
5280 is_inert_during_init(*first_t) &&
5281 bi->c.onstellation==m_states[first_t->to()].block->c.onstellation))
5284 if (!initialization) { first_t=&m_aut.get_transitions()[*ind->start_same_BLC]; }
5285 assert(m_states[first_t->from()].block==bi);
5286 assert(is_inert_during_init(*first_t) &&
5287 bi->c.onstellation==m_states[first_t->to()].block->c.onstellation);
5288 assert(ind->is_stable());
5289 if constexpr (initialization)
5291 assert(m_BLC_transitions.data()==ind->start_same_BLC);
5292 assert(bi->block.to_constellation.end()==std::next(ind) ||
5293 ind->end_same_BLC==std::next(ind)->start_same_BLC);
5298 if (initialization && bi->block.to_constellation.end()!=ind)
5300 Qhat.emplace_back(ind->start_same_BLC, m_BLC_transitions.data_end());
5302 for (; bi->block.to_constellation.end()!=ind; ++ind)
5303 { assert(ind->is_stable());
5304 ind->start_marked_BLC=ind->end_same_BLC;
5306 assert(!ind->has_marked_transitions());
5307 assert(ind->start_same_BLC<ind->end_same_BLC);
5308 const transition& first_t = m_aut.get_transitions()[*ind->start_same_BLC];
5309 assert(m_states[first_t.from()].block == bi);
5310 assert(!is_inert_during_init(first_t) ||
5311 bi->c.onstellation!=m_states[first_t.to()].block->c.onstellation);
5313 if constexpr (!initialization)
5316 Qhat.emplace_back(ind->start_same_BLC, ind->end_same_BLC);
5318 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5321 bool work_assigned =
false;
5323 for (BLC_list_const_iterator work_it = ind->start_same_BLC;
5324 work_it<ind->end_same_BLC; ++work_it)
5327 if (0==m_states[m_aut.get_transitions()
5328 [*work_it].from()].no_of_outgoing_block_inert_transitions)
5334 check_complexity::stabilizeB__initialize_Qhat, 1), *
this);
5339 check_complexity::stabilizeB__initialize_Qhat, 1), *
this);
5340 work_assigned =
true;
5350 initialize_qhat_work_to_assign_later.emplace_back(ind->start_same_BLC,
5357 if constexpr (!initialization)
5360 state_in_block_pointer* si=bi->start_bottom_states; assert(si<bi->sta.rt_non_bottom_states);
5363 check_complexity::stabilizeB__distribute_states_over_Phat, 1), *
this);
5364 outgoing_transitions_it end_it=
5365 std::next(si->ref_state)>=m_states.end()
5366 ? m_outgoing_transitions.end()
5367 : std::next(si->ref_state)->start_outgoing_transitions; assert(si->ref_state->block==bi);
5368 for (outgoing_transitions_it ti=
5369 si->ref_state->start_outgoing_transitions; ti<end_it; ++ti)
5372 const transition& t=
5373 m_aut.get_transitions()[*ti->ref.BLC_transitions]; assert(m_states.begin()+t.from()==si->ref_state);
5374 if (!is_inert_during_init(t) ||
5375 bi->c.onstellation!=m_states[t.to()].block->c.onstellation)
5378 mark_BLC_transition(ti);
5380 assert(ti <= ti->start_same_saC);
5381 ti = ti->start_same_saC;
5385 while (si<bi->sta.rt_non_bottom_states);
5389 clear(m_blocks_with_new_bottom_states);
5391 bool small_splitter_used_up=
false;
5395 if (initialization) { new_constellation=m_states[0].block->c.onstellation; }
5411 { assert(check_data_structures(
"End of stabilizeB()"));
5412 assert(check_stability(
"End of stabilizeB()"));
5415 assert(initialize_qhat_work_to_assign_later.empty());
5416 assert(stabilize_work_to_assign_later.empty());
5421 assert(check_data_structures(
"New bottom state loop",
false,
false));
5422 std::pair<BLC_list_iterator,BLC_list_iterator>& Qhat_elt=Qhat.back(); assert(check_stability(
"New bottom state loop", &Qhat));
5423 assert(Qhat_elt.first<Qhat_elt.second);
5424 const linked_list<BLC_indicators>::iterator splitter=
5425 m_transitions[*std::prev(Qhat_elt.second)].
5426 transitions_per_block_to_constellation; assert(splitter->end_same_BLC==Qhat_elt.second);
5428 Qhat_elt.second=splitter->start_same_BLC; assert(splitter->start_same_BLC<splitter->end_same_BLC);
5429 const transition& first_t=
5430 m_aut.get_transitions()[*splitter->start_same_BLC];
5431 block_type*
const from_block_index=m_states[first_t.from()].block; assert(!from_block_index->contains_new_bottom_states);
5432 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5434 bool work_assigned=
false;
5435 for (BLC_list_const_iterator work_it=splitter->start_same_BLC;
5436 work_it<splitter->end_same_BLC; ++work_it)
5439 if (0==m_states[m_aut.get_transitions()[*work_it].from()].
5440 no_of_outgoing_block_inert_transitions)
5446 check_complexity::stabilizeB__main_loop, 1), *
this);
5451 add_work(check_complexity::stabilizeB__main_loop, 1), *
this);
5462 stabilize_work_to_assign_later.emplace_back(splitter->start_same_BLC,
5463 splitter->end_same_BLC);
5466 if (std::distance(from_block_index->start_bottom_states,
5467 from_block_index->end_states)<=1)
5476 splitter->make_stable();
5479 { assert(!is_inert_during_init(first_t) || from_block_index->c.onstellation!=
5480 m_states[first_t.to()].block->c.onstellation);
5481 if (initialization && !small_splitter_used_up && 1==Qhat.size())
5486 make_stable_and_move_to_start_of_BLC(from_block_index, splitter);
5487 four_way_splitB<
true,
false>(from_block_index, splitter,
5488 from_block_index->block.to_constellation.end(),
5489 null_constellation, new_constellation);
5490 if (Qhat_elt.first==Qhat_elt.second)
5495 small_splitter_used_up=
true;
5500 four_way_splitB<
false,
true>(from_block_index, from_block_index->
5501 block.to_constellation.end(), splitter,
5502 null_constellation, null_constellation);
5504 } assert(Qhat_elt.first<=Qhat_elt.second);
5505 if (Qhat_elt.first==Qhat_elt.second)
5511 while (m_blocks_with_new_bottom_states.empty()); assert(1==m_blocks_with_new_bottom_states.size());
5512 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5516 for (std::vector<std::pair<BLC_list_const_iterator,BLC_list_const_iterator> >
5517 ::iterator qhat_it=initialize_qhat_work_to_assign_later.begin();
5518 qhat_it!=initialize_qhat_work_to_assign_later.end(); )
5520 bool new_bottom_state_with_transition_found=
false;
5521 for (BLC_list_const_iterator work_it=qhat_it->first;
5522 work_it<qhat_it->second; ++work_it)
5524 const state_index t_from=m_aut.get_transitions()[*work_it].from();
5525 if (0==m_states[t_from].no_of_outgoing_block_inert_transitions)
5530 if (new_bottom_state_with_transition_found)
5534 stabilizeB__initialize_Qhat_afterwards, 1), *
this);
5539 stabilizeB__initialize_Qhat_afterwards, 1), *
this);
5540 new_bottom_state_with_transition_found=
true;
5546 if (new_bottom_state_with_transition_found)
5550 *qhat_it=initialize_qhat_work_to_assign_later.back();
5551 if (std::next(qhat_it)==initialize_qhat_work_to_assign_later.end())
5553 initialize_qhat_work_to_assign_later.pop_back();
5558 initialize_qhat_work_to_assign_later.pop_back();
5569 for (std::vector<std::pair<BLC_list_const_iterator,BLC_list_const_iterator> >
5570 ::iterator stabilize_it=stabilize_work_to_assign_later.begin();
5571 stabilize_it!=stabilize_work_to_assign_later.end(); )
5573 bool new_bottom_state_with_transition_found=
false;
5574 for (BLC_list_const_iterator work_it=stabilize_it->first;
5575 work_it<stabilize_it->second; ++work_it)
5577 const state_index t_from=m_aut.get_transitions()[*work_it].from();
5578 if (0==m_states[t_from].no_of_outgoing_block_inert_transitions)
5583 if (new_bottom_state_with_transition_found)
5586 check_complexity::stabilizeB__main_loop_afterwards, 1), *
this);
5591 stabilizeB__main_loop_afterwards, 1), *
this);
5592 new_bottom_state_with_transition_found=
true;
5598 if (new_bottom_state_with_transition_found)
5602 *stabilize_it=stabilize_work_to_assign_later.back();
5603 if (std::next(stabilize_it) == stabilize_work_to_assign_later.end())
5605 stabilize_work_to_assign_later.pop_back();
5610 stabilize_work_to_assign_later.pop_back();
5620 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5634 clear(m_blocks_with_new_bottom_states);
5641 ind=bi->block.to_constellation.begin(); assert(!bi->block.to_constellation.empty());
5642 assert(ind->start_same_BLC<ind->end_same_BLC);
5644 const transition& first_t=m_aut.get_transitions()[*ind->start_same_BLC];
5645 assert(m_states[first_t.from()].block==bi);
5646 assert(is_inert_during_init_if_branching(first_t) &&
5647 bi->c.onstellation==m_states[first_t.to()].block->c.onstellation);
5649 assert(ind->is_stable());
5651 for (; bi->block.to_constellation.end()!=ind; ++ind)
5653 if (!ind->is_stable())
5657 while (++ind!=bi->block.to_constellation.end())
5659 assert(!ind->is_stable());
5662 assert(!ind->has_marked_transitions());
5667 ind->start_marked_BLC=ind->end_same_BLC;
5669 assert(!ind->has_marked_transitions());
5670 assert(ind->start_same_BLC<ind->end_same_BLC);
5671 const transition& first_t = m_aut.get_transitions()[*ind->start_same_BLC];
5672 assert(m_states[first_t.from()].block == bi);
5673 assert(!is_inert_during_init_if_branching(first_t) ||
5674 bi->c.onstellation!=m_states[first_t.to()].block->c.onstellation);
5676 Qhat.emplace_back(ind->start_same_BLC, ind->end_same_BLC);
5677 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5680 bool work_assigned =
false;
5682 for (BLC_list_const_iterator work_it = ind->start_same_BLC;
5683 work_it<ind->end_same_BLC; ++work_it)
5686 if (0==m_states[m_aut.get_transitions()
5687 [*work_it].from()].no_of_outgoing_block_inert_transitions)
5693 check_complexity::stabilizeB__initialize_Qhat, 1), *
this);
5698 check_complexity::stabilizeB__initialize_Qhat, 1), *
this);
5699 work_assigned =
true;
5709 initialize_qhat_work_to_assign_later.emplace_back(ind->start_same_BLC,
5722 std::next(si->ref_state)>=m_states.end()
5723 ? m_outgoing_transitions.end()
5724 : std::next(si->ref_state)->start_outgoing_transitions; assert(si->ref_state->block==bi);
5726 si->ref_state->start_outgoing_transitions; ti<end_it; ++ti)
5730 m_aut.get_transitions()[*ti->ref.BLC_transitions]; assert(m_states.begin()+t.from()==si->ref_state);
5731 if (!is_inert_during_init_if_branching(t) ||
5732 bi->c.onstellation!=m_states[t.to()].block->c.onstellation)
5737 assert(ti <= ti->start_same_saC);
5738 ti = ti->start_same_saC;
5748 mCRL2log(log::verbose) <<
"An O(m log n) "
5749 << (m_branching ? (m_preserve_divergence
5750 ?
"divergence-preserving branching "
5753 <<
"bisimulation partitioner created for " << m_aut.num_states()
5754 <<
" states and " << m_transitions.size()
5755 <<
" transitions (using the experimental algorithm GJ2025).\n";
5756 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
5760 group_transitions_on_tgt_label(
m_aut);
5764 "initialisation, after sorting.\n";
5767 simple_list<BLC_indicators>::get_pool().
5768 template construct<constellation_type>
5770 new constellation_type
5775 simple_list<BLC_indicators>::get_pool().
5776 template construct<block_type>
5780 (m_states_in_blocks.data(), m_states_in_blocks.data_end(),
5781 m_states_in_blocks.data_end(), initial_constellation); assert(1==
no_of_blocks);
5783 #define temporary_BLC_list (initial_block->block.to_constellation)
5789 std::vector<label_index> todo_stack_actions;
5790 std::vector<transition_index> count_transitions_per_action
5791 (m_aut.num_action_labels() + (
unsigned) m_preserve_divergence, 0);
5797 todo_stack_actions.push_back(m_aut.tau_label_index());
5798 count_transitions_per_action[m_aut.tau_label_index()] = 1;
5800 for (transition_index ti=0; ti<m_transitions.size(); ++ti)
5802 const transition& t=m_aut.get_transitions()[ti];
5804 const label_index label=label_or_divergence(t,
5805 m_aut.num_action_labels()); assert(m_aut.apply_hidden_label_map(t.label())==t.label());
5806 transition_index& c=count_transitions_per_action[label];
5809 todo_stack_actions.push_back(label);
5814 { assert(m_aut.is_tau(todo_stack_actions.front()));
5815 --count_transitions_per_action[m_aut.tau_label_index()];
5817 accumulate_entries(count_transitions_per_action, todo_stack_actions);
5818 for (transition_index ti=0; ti<m_transitions.size(); ++ti)
5821 const transition& t=m_aut.get_transitions()[ti];
5822 const label_index label = label_or_divergence(t,
5823 m_aut.num_action_labels());
5824 transition_index& c=count_transitions_per_action[label]; assert(0 <= c); assert(c < m_transitions.size());
5825 m_BLC_transitions[c]=ti;
5830 std::vector<label_index>::const_iterator
5831 a_it=todo_stack_actions.begin();
5832 if (a_it!=todo_stack_actions.end() &&
5833 (0!=count_transitions_per_action[*a_it] || (assert(m_branching), assert(m_aut.is_tau(*a_it)),
5834 ++a_it!=todo_stack_actions.end())) )
5839 const label_index a=*a_it;
5840 const BLC_list_iterator end_index=
5841 m_BLC_transitions.data()+count_transitions_per_action[a]; assert(end_index<=m_BLC_transitions.data_end());
5843 temporary_BLC_list.emplace_back(start_index, end_index,
true); assert(start_index<end_index);
5844 start_index=end_index;
5846 while (++a_it!=todo_stack_actions.end()); assert(start_index==m_BLC_transitions.data_end());
5856 (m_aut.num_states(), 0);
5860 count_outgoing_transitions_per_state[t.from()]++;
5863 m_states[t.from()].no_of_outgoing_block_inert_transitions++;
5874 m_outgoing_transitions.begin();
5879 if (marked_range<=m_states[s].no_of_outgoing_block_inert_transitions)
5881 mCRL2log(log::error) <<
"State " << s <<
" has "
5882 << m_states[s].no_of_outgoing_block_inert_transitions
5883 <<
" outgoing block-inert transitions. However, the "
5884 "four-way-split can handle at most " << (marked_range-1)
5885 <<
" outgoing block-inert transitions per state. "
5889 m_states[s].start_outgoing_transitions=current_outgoing_transitions+
5890 m_states[s].no_of_outgoing_block_inert_transitions;
5891 current_outgoing_transitions+=
5892 count_outgoing_transitions_per_state[s];
5893 count_outgoing_transitions_per_state[s]=0;
5896 } assert(m_outgoing_transitions.end()==current_outgoing_transitions);
5900 for (BLC_list_iterator ti=m_BLC_transitions.data();
5901 ti<m_BLC_transitions.data_end(); ++ti)
5903 const transition& t=m_aut.get_transitions()[*ti];
5904 if (is_inert_during_init(t))
5906 m_transitions[*ti].ref_outgoing_transitions =
5907 --m_states[t.from()].start_outgoing_transitions;
5911 m_transitions[*ti].ref_outgoing_transitions =
5912 m_states[t.from()].start_outgoing_transitions +
5913 count_outgoing_transitions_per_state[t.from()];
5916 m_transitions[*ti].ref_outgoing_transitions->ref.transitions=*ti;
5918 m_transitions[*ti].ref_outgoing_transitions->ref.BLC_transitions=ti;
5920 ++count_outgoing_transitions_per_state[t.from()];
5928 for(std::vector<transition>::iterator it=m_aut.get_transitions().begin();
5929 it!=m_aut.get_transitions().end(); it++)
5932 const transition& t=*it;
5933 if (t.to()!=current_state)
5935 for (state_index i=current_state+1; i<=t.to(); ++i)
5938 create_initial_partition__set_start_incoming_transitions, 1), *
this);
5939 m_states[i].start_incoming_transitions=it;
5941 current_state=t.to();
5946 create_initial_partition__set_start_incoming_transitions, 1), *
this);
5947 m_states[i].start_incoming_transitions=m_aut.get_transitions().end();
5952 if (m_outgoing_transitions.begin() < it)
5959 *it->ref.BLC_transitions
5965 while (m_outgoing_transitions.begin() < it)
5969 const transition& t=m_aut.get_transitions()[
5973 *it->ref.BLC_transitions
5976 const label_index new_label = label_or_divergence(t);
5977 if (current_state == t.from() && current_label == new_label)
5981 it->start_same_saC = current_end_same_saC;
5986 current_state = t.from();
5987 current_label = new_label;
5988 current_end_same_saC->start_same_saC = std::next(it);
5989 current_end_same_saC = it;
5992 current_end_same_saC->start_same_saC = m_outgoing_transitions.begin();
5993 } assert(m_states_in_blocks.size()==m_aut.num_states());
5996 for (fixed_vector<state_type_gj>::iterator i=m_states.begin();
5997 i<m_states.end(); ++i)
5999 if (0<i->no_of_outgoing_block_inert_transitions)
6002 upper_i->ref_state=i;
6003 i->ref_states_in_blocks=upper_i;
6007 lower_i->ref_state=i;
6008 i->ref_states_in_blocks=lower_i;
6011 i->block=initial_block;
6012 } assert(lower_i == upper_i);
6015 mCRL2log(log::verbose) <<
"Start refining in the initialisation WITH BLC sets\n";
6016 for (linked_list<BLC_indicators>::iterator
6017 blc_it=temporary_BLC_list.begin();
6018 temporary_BLC_list.end()!=blc_it; ++blc_it)
6019 { assert(blc_it->start_same_BLC<blc_it->end_same_BLC);
6020 BLC_list_iterator it=blc_it->start_same_BLC;
6021 if (!is_inert_during_init(m_aut.get_transitions()[*it]))
6023 ++no_of_non_constellation_inert_BLC_sets;
6027 m_transitions[*it].transitions_per_block_to_constellation=blc_it;
6030 while (it!=blc_it->end_same_BLC);
6032 #undef temporary_BLC_list
6034 initial_block->contains_new_bottom_states =
true;
6035 m_blocks_with_new_bottom_states.push_back(initial_block);
6037 assert(check_data_structures(
"After initial reading before splitting in the initialisation",
false,
false));
6048 if (!temporary_BLC_list.empty())
6051 temporary_BLC_list.begin(); assert(blc_it->start_same_BLC<blc_it->end_same_BLC);
6052 if (!is_inert_during_init
6053 (m_aut.get_transitions()[*blc_it->start_same_BLC]) ||
6054 ++blc_it!=temporary_BLC_list.end())
6058 std::vector<block_type*> blocks_that_need_refinement;
6059 BLC_list_iterator trans_it=blc_it->start_same_BLC; assert(trans_it<blc_it->end_same_BLC);
6060 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
6061 const label_index a=label_or_divergence(m_aut.get_transitions()[*trans_it]);
6066 const transition& t=m_aut.get_transitions()[*trans_it]; assert(label_or_divergence(t)==a);
6067 const state_in_block_pointer s(m_states.begin()+t.from());
6068 block_type& B=*s.ref_state->block;
6069 if (
nullptr==B.block.R)
6070 { assert(std::find(blocks_that_need_refinement.begin(),
6071 blocks_that_need_refinement.end(), s.ref_state->block)==
6072 blocks_that_need_refinement.end());
6073 if (B.contains_new_bottom_states ||
6074 number_of_states_in_block(B)<=1)
6078 B.block.R=
new std::vector<state_in_block_pointer>();
6079 blocks_that_need_refinement.push_back(s.ref_state->block);
6081 B.c.first_unmarked_bottom_state=B.start_bottom_states;
6082 }
else { assert(std::find(blocks_that_need_refinement.begin(),
6083 blocks_that_need_refinement.end(), s.ref_state->block)!=
6084 blocks_that_need_refinement.end()); }
6085 state_in_block_pointer*
const
6086 pos_s=s.ref_state->ref_states_in_blocks; assert(B.start_bottom_states<=pos_s); assert(pos_s<B.end_states);
6087 if (B.c.first_unmarked_bottom_state<=pos_s)
6089 if (0==s.ref_state->no_of_outgoing_block_inert_transitions)
6090 { assert(pos_s<B.sta.rt_non_bottom_states);
6091 swap_states_in_states_in_block
6092 (B.c.first_unmarked_bottom_state, pos_s); assert(undefined==s.ref_state->counter);
6093 B.c.first_unmarked_bottom_state++;
6097 if (undefined==s.ref_state->counter)
6099 B.block.R->push_back(s);
6100 s.ref_state->counter=marked(ReachAlw)+
6101 s.ref_state->no_of_outgoing_block_inert_transitions; assert(B.sta.rt_non_bottom_states<=pos_s);
6102 }
else { assert(B.sta.rt_non_bottom_states<=pos_s); }
6103 assert(is_in_marked_range_of(s.ref_state->counter, ReachAlw));
6107 while (++trans_it<blc_it->end_same_BLC);
6109 for (block_type*
const bi : blocks_that_need_refinement)
6110 { assert(
nullptr!=bi->block.R);
6111 four_way_splitB<
false,
false>(bi,
6114 null_constellation, initial_constellation);
6124 while (++blc_it!=temporary_BLC_list.end());
6135 block_type*
const blk_it=st_it->ref_state->block; assert(
nullptr==blk_it->block.R);
6139 new(&blk_it->block.to_constellation)
linked_list<BLC_indicators>();
6140 st_it=blk_it->end_states;
6142 while (m_states_in_blocks.data_end()!=st_it);
6146 last_block_start=std::prev(m_states_in_blocks.end())->
6147 ref_state->block->start_bottom_states;
6149 while(blc_it=temporary_BLC_list.begin(),temporary_BLC_list.end()!=blc_it)
6151 order_BLC_transitions(blc_it->start_same_BLC, blc_it->end_same_BLC,
6152 m_states_in_blocks.data(), last_block_start);
6155 temporary_BLC_list.erase(blc_it);
6159 assert(check_stability(
"End initialisation"));
6186 btc_it=index_block_B->block.to_constellation.begin();
6187 if (btc_it == index_block_B->block.to_constellation.end())
6190 return index_block_B->block.to_constellation.end();
6191 } assert(btc_it->start_same_BLC<btc_it->end_same_BLC);
6193 m_aut.get_transitions()[*(btc_it->start_same_BLC)];
6199 return index_block_B->block.to_constellation.end();
6201 if (m_states[btc_t.to()].block->c.onstellation==old_constellation)
6207 if (m_states[btc_t.to()].block->c.onstellation!=new_constellation)
6211 return index_block_B->block.to_constellation.end();
6215 btc_it=index_block_B->block.to_constellation.next(btc_it);
6216 if (btc_it == index_block_B->block.to_constellation.end())
6219 return index_block_B->block.to_constellation.end();
6220 } assert(btc_it->start_same_BLC<btc_it->end_same_BLC);
6222 m_aut.get_transitions()[*(btc_it->start_same_BLC)];
6223 if (!is_inert_during_init_if_branching(btc2_t) ||
6224 old_constellation!=m_states[btc2_t.to()].block->c.onstellation)
6228 return index_block_B->block.to_constellation.end();
6244 { assert(!m_non_trivial_constellations.empty());
6260 index_block_B=second_block_B;
6262 return index_block_B;
6288 std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> > calM;
6290 clock_t next_print_time = clock();
6291 const clock_t rounded_start_time = next_print_time - CLOCKS_PER_SEC/2;
6295 assert(check_stability(
"MAIN LOOP"));
6298 if (
std::clock_t now =
std::clock(); next_print_time <= now ||
6299 m_non_trivial_constellations.empty())
6309 next_print_time+=((now-next_print_time)/(60*CLOCKS_PER_SEC)
6310 + 1) * (60*CLOCKS_PER_SEC);
6311 now = (now - rounded_start_time) / CLOCKS_PER_SEC;
6325 <<
" sec passed since starting the main loop.\n";
6327 #define PRINT_SG_PL(counter, sg_string, pl_string)
6328 (counter) << (1
== (counter) ? (sg_string) : (pl_string))
6330 << (m_non_trivial_constellations.empty()
6331 ?
"The reduced LTS contains "
6332 :
"The reduced LTS contains at least ")
6333 <<
PRINT_SG_PL(no_of_blocks,
" state and ",
" states and ")
6334 <<
PRINT_SG_PL(no_of_non_constellation_inert_BLC_sets,
6335 " transition.",
" transitions.");
6338 #define PRINT_INT_PERCENTAGE(num,denom)
6339 (((num) * 200
+ (denom)) / (denom) / 2
)
6344 #undef PRINT_INT_PERCENTAGE
6352 <<
"\nThe current partition contains ";
6357 " new bottom state and ",
" new bottom states and ");
6361 " constellation (of which ",
" constellations (of which ")
6362 <<
PRINT_SG_PL(m_non_trivial_constellations.size(),
6363 " is nontrivial).\n",
" are nontrivial).\n");
6367 if (m_non_trivial_constellations.empty())
6380 { assert(m_non_trivial_constellations.back()==old_constellation);
6382 m_non_trivial_constellations.pop_back();
6386 simple_list<BLC_indicators>::get_pool().
6387 template construct<constellation_type>
6389 new constellation_type
6391 (index_block_B->start_bottom_states,
6392 index_block_B->end_states);
6394 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
6409 const std::vector<transition>::iterator end_it=
6410 (std::next(i->ref_state)==m_states.end())
6411 ? m_aut.get_transitions().end()
6412 : std::next(i->ref_state)->start_incoming_transitions;
6413 for(std::vector<transition>::iterator
6414 j=i->ref_state->start_incoming_transitions; j!=end_it; ++j)
6416 const transition& t=*j;
6417 const transition_index t_index=
6418 std::distance(m_aut.get_transitions().begin(), j);
6421 const outgoing_transitions_it old_pos=
6422 m_transitions[t_index].ref_outgoing_transitions;
6423 const outgoing_transitions_it end_same_saC=
6424 old_pos->start_same_saC < old_pos
6425 ? old_pos : old_pos->start_same_saC;
6426 const outgoing_transitions_it new_pos=end_same_saC->start_same_saC; assert(m_states[t.from()].start_outgoing_transitions<=new_pos);
6427 assert(new_pos<=old_pos);
6428 if (old_pos != new_pos)
6430 std::swap(old_pos->ref.BLC_transitions,
6431 new_pos->ref.BLC_transitions);
6432 m_transitions[*old_pos->ref.BLC_transitions].
6433 ref_outgoing_transitions=old_pos;
6434 m_transitions[*new_pos->ref.BLC_transitions].
6435 ref_outgoing_transitions=new_pos;
6437 if (new_pos < end_same_saC)
6439 end_same_saC->start_same_saC = std::next(new_pos);
6445 new_pos->start_same_saC = new_pos;
6446 if (m_states[t.from()].start_outgoing_transitions<new_pos)
6449 const transition& prev_t = m_aut.get_transitions()
6450 [*std::prev(new_pos)->ref.BLC_transitions]; assert(prev_t.from() == t.from());
6451 if (m_states[prev_t.to()].block == index_block_B &&
6452 label_or_divergence(prev_t) == label_or_divergence(t))
6455 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);
6456 assert(new_pos->start_same_saC<new_pos);
6457 assert(std::prev(new_pos)==new_pos->start_same_saC->start_same_saC);
6458 new_pos->start_same_saC->start_same_saC = new_pos;
6470 const std::vector<transition>::iterator end_it=
6471 (std::next(i->ref_state)==m_states.end())
6472 ? m_aut.get_transitions().end()
6473 : std::next(i->ref_state)->start_incoming_transitions;
6474 for(std::vector<transition>::iterator
6475 j=i->ref_state->start_incoming_transitions; j!=end_it; ++j)
6477 const transition& t=*j;
6478 const transition_index t_index=
6479 std::distance(m_aut.get_transitions().begin(), j); assert(m_states[t.to()].block == index_block_B);
6480 bool source_block_is_singleton=
6481 (1>=number_of_states_in_block(*m_states[t.from()].block));
6484 const outgoing_transitions_it out_pos=
6485 m_transitions[t_index].ref_outgoing_transitions;
6486 const outgoing_transitions_it start_new_saC=
6487 out_pos->start_same_saC;
6488 if (start_new_saC < out_pos)
6491 if (out_pos < start_new_saC->start_same_saC)
6494 out_pos->start_same_saC = start_new_saC->start_same_saC;
6499 if (update_the_doubly_linked_list_LBC_new_constellation(index_block_B, t, t_index) &&
6500 !source_block_is_singleton &&
6501 (!is_inert_during_init(t) || index_block_B!=m_states[t.from()].block))
6505 BLC_list_iterator BLC_pos=m_transitions[t_index].
6506 ref_outgoing_transitions->ref.BLC_transitions; assert(t_index == *BLC_pos);
6508 calM.emplace_back(BLC_pos, BLC_pos);
6517 if (calM.begin()!=calM.end())
6519 for (std::vector<std::pair<BLC_list_iterator, BLC_list_iterator> >::
6520 iterator calM_elt=calM.begin();; )
6522 linked_list <BLC_indicators>::iterator ind=m_transitions
6523 [*calM_elt->first].transitions_per_block_to_constellation;
mCRL2complexity(ind, add_work(check_complexity::
6524 refine_partition_until_it_becomes_stable__correct_end_of_calM,max_C),*
this);
6525 assert(ind->start_same_BLC==calM_elt->first);
6526 assert(!ind->has_marked_transitions());
6528 m_aut.get_transitions()[*std::prev(ind->end_same_BLC)]; assert(m_states[last_t.to()].block->c.onstellation==new_constellation);
6529 assert(ind->start_same_BLC<ind->end_same_BLC);
6531 if ((is_inert_during_init(last_t) &&
6532 m_states[last_t.from()].block->c.onstellation==
6533 old_constellation && (assert(m_states[last_t.from()].block!=index_block_B),
true)
6535 (ind->end_same_BLC<m_BLC_transitions.data_end() &&
6536 (next_t=&m_aut.get_transitions()[*ind->end_same_BLC],
6537 m_states[last_t.from()].block==
6538 m_states[next_t->from()].block &&
6539 label_or_divergence(last_t)==label_or_divergence(*next_t) &&
6541 m_states[next_t->to()].block->c.onstellation)))
6545 calM_elt->second = ind->end_same_BLC;
6547 if (calM_elt==calM.end())
6557 if (std::prev(calM.end())==calM_elt)
6568 calM_elt->first=calM.back().first;
6579 linked_list<BLC_indicators>::iterator tau_co_splitter=
6580 find_inert_co_transition_for_block(index_block_B,
6581 old_constellation, new_constellation);
6584 if (index_block_B->block.to_constellation.end()!=tau_co_splitter)
6590 { assert(tau_co_splitter->is_stable());
6591 four_way_splitB<
true,
false>(index_block_B, tau_co_splitter,
6592 index_block_B->block.to_constellation.end(),
6601 for (std::pair<BLC_list_iterator, BLC_list_iterator> calM_elt: calM)
6605 assert(check_stability(
"Main loop", &calM, &calM_elt, old_constellation, new_constellation));
6606 assert(check_data_structures(
"Main loop",
false,
false));
6607 assert(calM_elt.first < calM_elt.second);
6611 m_transitions[*std::prev(calM_elt.second)].
6612 transitions_per_block_to_constellation;
mCRL2complexity(splitter, add_work(check_complexity::
6613 refine_partition_until_it_becomes_stable__execute_main_split,max_C),*
this);
6614 assert(splitter->end_same_BLC==calM_elt.second); assert(splitter->is_stable());
6615 calM_elt.second = splitter->start_same_BLC; assert(splitter->start_same_BLC<splitter->end_same_BLC);
6617 const transition& first_t=
6618 m_aut.get_transitions()[*splitter->start_same_BLC];
6619 const label_index a=label_or_divergence(first_t); assert(m_states[first_t.to()].block->c.onstellation==new_constellation);
6620 block_type* Bpp=m_states[first_t.from()].block; assert(Bpp->c.onstellation!=new_constellation ||
6621 !is_inert_during_init(first_t));
6622 if (number_of_states_in_block(*Bpp) <= 1)
6626 else if (Bpp->contains_new_bottom_states)
6633 else if (is_inert_during_init(first_t) &&
6634 old_constellation==Bpp->c.onstellation)
6639 four_way_splitB<
true,
false>(Bpp, splitter,
6640 Bpp->block.to_constellation.end(),
6641 old_constellation, new_constellation);
6646 linked_list<BLC_indicators>::iterator co_splitter=
6647 Bpp->block.to_constellation.prev(splitter);
6648 const transition* co_t;
6650 if (Bpp->block.to_constellation.end()!=co_splitter &&
6651 ( assert(co_splitter->is_stable()),
6652 assert(co_splitter->start_same_BLC<co_splitter->end_same_BLC),
6653 co_t=&m_aut.get_transitions()[*co_splitter->start_same_BLC], assert(m_states[co_t->from()].block==Bpp),
6654 a==label_or_divergence(*co_t) &&
6656 m_states[co_t->to()].block->c.onstellation))
6659 four_way_splitB<
true,
true>(Bpp, splitter, co_splitter,
6660 old_constellation, new_constellation);
6665 while (calM_elt.first < calM_elt.second);
6668 assert(check_stability(
"Before stabilize"));
6671 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
6692 const bool branching =
false,
6693 const bool preserve_divergence =
false)
6712 <<
no_of_blocks <<
" equivalence classes. Start refining. \n";
6744template <
class LTS_TYPE>
6746 const bool preserve_divergence =
false)
6748 if (1 >= l.num_states())
6751 "guaranteed that branching bisimulation minimisation runs in "
6752 "time O(m log n).\n";
6756 const std::clock_t start_SCC=
std::clock();
6760 scc_reduce(l, preserve_divergence);
6765 const std::clock_t start_part=
std::clock();
6767 bisim_partitioner_gj<LTS_TYPE> bisim_part(l,branching,preserve_divergence);
6770 const std::clock_t end_part=
std::clock();
6772 bisim_part.finalize_minimized_LTS();
6776 const std::clock_t end_finalizing=
std::clock();
6777 const int prec=
static_cast<
int>
6778 (
std::log10(CLOCKS_PER_SEC)+0.69897000433602);
6784 runtime[0]=(
double) (end_finalizing - start_SCC)/CLOCKS_PER_SEC;
6785 runtime[1]=(
double) ( start_part-start_SCC)/CLOCKS_PER_SEC;
6786 runtime[2]=(
double) ( bisim_part.end_initial_part-start_part )/CLOCKS_PER_SEC;
6787 runtime[3]=(
double) ( end_part-bisim_part.end_initial_part )/CLOCKS_PER_SEC;
6788 runtime[4]=(
double) (end_finalizing-end_part )/CLOCKS_PER_SEC;
6789 if (runtime[0]>=60.0)
6791 int min[
sizeof(runtime)/
sizeof(runtime[0])];
6792 for (
unsigned i = 0; i <
sizeof(runtime)/
sizeof(runtime[0]); ++i)
6794 min[i] =
static_cast<
int>(runtime[i]) / 60;
6795 runtime[i] -= 60 * min[i];
6799 int h[
sizeof(runtime)/
sizeof(runtime[0])];
6800 for (
unsigned i=0; i <
sizeof(runtime)/
sizeof(runtime[0]); ++i)
6805 int width =
static_cast<
int>(
std::log10(h[0])) + 1;
6808 <<
"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"
6809 "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"
6810 "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"
6811 "Time spent on finalizing: " <<
std::setw(width) << h[4] <<
"h " <<
std::setw(2) << min[4] <<
"min " <<
std::setw(prec+3) << runtime[4] <<
"s\n"
6812 "Total CPU time: " <<
std::setw(width) << h[0] <<
"h " <<
std::setw(2) << min[0] <<
"min " <<
std::setw(prec+3) << runtime[0] <<
"s\n"
6813 "BENCHMARK TIME: " <<
static_cast<
double>(end_part-start_part)/CLOCKS_PER_SEC <<
"\n"
6814 <<
std::defaultfloat;
6819 <<
"Time spent on contracting SCCs: " <<
std::setw(2) << min[1] <<
"min " <<
std::setw(prec+3) << runtime[1] <<
"s\n"
6820 "Time spent on initial partition:" <<
std::setw(2) << min[2] <<
"min " <<
std::setw(prec+3) << runtime[2] <<
"s\n"
6821 "Time spent on stabilize+refine: " <<
std::setw(2) << min[3] <<
"min " <<
std::setw(prec+3) << runtime[3] <<
"s\n"
6822 "Time spent on finalizing: " <<
std::setw(2) << min[4] <<
"min " <<
std::setw(prec+3) << runtime[4] <<
"s\n"
6823 "Total CPU time: " <<
std::setw(2) << min[0] <<
"min " <<
std::setw(prec+3) << runtime[0] <<
"s\n"
6824 "BENCHMARK TIME: " <<
static_cast<
double>(end_part-start_part)/CLOCKS_PER_SEC <<
"\n"
6825 <<
std::defaultfloat;
6831 <<
"Time spent on contracting SCCs: " <<
std::setw(prec+3) << runtime[1] <<
"s\n"
6832 "Time spent on initial partition:" <<
std::setw(prec+3) << runtime[2] <<
"s\n"
6833 "Time spent on stabilize+refine: " <<
std::setw(prec+3) << runtime[3] <<
"s\n"
6834 "Time spent on finalizing: " <<
std::setw(prec+3) << runtime[4] <<
"s\n"
6835 "Total CPU time: " <<
std::setw(prec+3) << runtime[0] <<
"s\n"
6836 "BENCHMARK TIME: " <<
static_cast<
double>(end_part-start_part)/CLOCKS_PER_SEC <<
"\n"
6837 <<
std::defaultfloat;
6862template <
class LTS_TYPE>
6864 const bool branching =
false,
const bool preserve_divergence =
false,
6865 const bool generate_counter_examples =
false,
6866 const std::string& =
"",
6869 if (generate_counter_examples)
6872 "algorithm does not generate counterexamples.\n";
6874 std::size_t init_l2(l2.initial_state() + l1.num_states());
6881 scc_part.replace_transition_system(preserve_divergence);
6882 init_l2 = scc_part.get_eq_class(init_l2);
6883 }
else { assert(!preserve_divergence); }
6884 assert(1 < l1.num_states());
6885 bisim_partitioner_gj<LTS_TYPE>bisim_part(l1,branching,preserve_divergence);
6887 return bisim_part.in_same_class(l1.initial_state(), init_l2);
6907template <
class LTS_TYPE>
6909 const bool branching =
false,
const bool preserve_divergence =
false)
6911 LTS_TYPE l1_copy(l1);
6912 LTS_TYPE l2_copy(l2);
6913 return destructive_bisimulation_compare_gj(l1_copy, l2_copy, branching,
6914 preserve_divergence);
#define mCRL2complexity(unit, call, info_for_debug)
Assigns work to a counter and checks for errors.
const aterm & operator[](const size_type i) const
Returns the i-th argument.
aterm & operator=(const aterm &other) noexcept=default
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
const function_symbol & function() const noexcept
bool operator!=(const function_symbol &f) const
Inequality test.
bool operator==(const function_symbol &f) const
Equality test.
std::size_t m_top_of_stack
unprotected_aterm_core m_stack[maximal_size_of_stack]
static constexpr std::size_t maximal_size_of_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.
friend void make_term_balanced_tree(term_balanced_tree< Term1 > &result, ForwardTraversalIterator p, const std::size_t size, Transformer transformer)
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.
Term & reference
Reference to T.
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.
std::size_t size_type
An unsigned integral type.
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 * pointer
Pointer to T.
Term value_type
The type of object, T stored in the term_balanced_tree.
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.
const Term const_reference
Const reference to T.
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()
term_balanced_tree(detail::_term_appl *t)
ptrdiff_t difference_type
A signed integral type.
An unprotected term does not change the reference count of the shared term when it is copied or moved...
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
bool defined() const
Returns true if this term is not equal to the term assigned by the default constructor of aterms,...
const detail::_aterm * m_term
bool operator!=(const unprotected_aterm_core &t) const
Inequality operator on two unprotected aterms.
const function_symbol & function() const
Yields the function symbol in an aterm.
data_expression & operator=(const data_expression &) noexcept=default
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
Class for logging messages.
static void set_reporting_level(const log_level_t level)
Set reporting level.
logger(const log_level_t l)
Default constructor.
Read-only singly linked list of action rename rules.
\brief A timed multi-action
multi_action(const multi_action &) noexcept=default
Move semantics.
const process::action_list & actions() const
const data::data_expression & time() const
multi_action(multi_action &&) noexcept=default
multi_action(const process::action_list &actions=process::action_list(), data::data_expression time=data::undefined_real())
Constructor.
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 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.
static mcrl2::lps::multi_action sort_multiactions(const mcrl2::lps::multi_action &a)
A function to sort a multi action to guarantee that multi-actions are compared properly.
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()
Default constructor.
action_label_lts(const mcrl2::lps::multi_action &a)
Constructor.
This class contains strings to be used as values for action labels in lts's.
static std::string sort_multiactions(const std::string &s)
Sort multiactions in a string.
void hide_actions(const std::vector< std::string > &string_vector)
action_label_string & operator=(const action_label_string &)=default
Copy assignment.
static const action_label_string & tau_action()
action_label_string(const std::string &s)
bool operator<(const action_label_string &l) const
action_label_string(const action_label_string &)=default
Copy constructor.
stores information about a block
stores information about a constellation
refinable partition data structure
stores information about a single state
bool surely_has_no_transition_to(const constln_t *const SpC) const
quick check to find out whether the state has no transition to SpC
bool surely_has_transition_to(const constln_t *const SpC) const
quick check to find out whether the state has a transition to SpC
state_index number_of_states_in_block(const block_type &B) const
return the number of states in block B
void finalize_minimized_LTS()
Adapt the LTS after minimisation.
label_index label_or_divergence(const transition &t, const label_index divergent_label=-2) const
void swap_states_in_states_in_block(state_in_block_pointer *pos1, state_in_block_pointer *pos2)
swap the contents of pos1 and pos2 if they are different
LTS_TYPE & m_aut
automaton that is being reduced
block_type * select_and_remove_a_block_in_a_non_trivial_constellation()
Select a block that is not the largest block in a non-trivial constellation.
std::string ptr(const transition &t) const
std::unordered_set< state_index > set_of_states_type
std::vector< block_type * > m_blocks_with_new_bottom_states
std::unordered_set< transition_index > set_of_transitions_type
std::vector< constellation_type * > m_non_trivial_constellations
The following variable contains all non-trivial constellations.
void swap_states_in_states_in_block(state_in_block_pointer *pos1, state_in_block_pointer *pos2, state_in_block_pointer *pos3)
Move the contents of pos1 to pos2, those of pos2 to pos3 and those of pos3 to pos1
void multiple_swap_states_in_states_in_block(state_in_block_pointer *pos1, state_in_block_pointer *pos2, state_index count, const state_in_block_pointer *assign_work_to, unsigned char const max_B, enum check_complexity::counter_type const ctr=check_complexity::multiple_swap_states_in_block__swap_state_in_small_block)
Swap the range [pos1, pos1 + count) with the range [pos2, pos2 + count)
bool is_inert_during_init(const transition &t) const
state_index no_of_constellations
state_index no_of_new_bottom_states
number of new bottom states found after constructing the initial partition
linked_list< BLC_indicators >::const_iterator next_target_constln_in_same_saC(state_in_block_pointer const src, BLC_list_const_iterator const splitter_it) const
find the next constellation after splitter_it's in the same_saC slice of the outgoing transitions
bool is_inert_during_init_if_branching(const transition &t) const
std::vector< linked_list< BLC_indicators >::iterator > m_BLC_indicators_to_be_deleted
void mark_BLC_transition(const outgoing_transitions_it out_pos)
marks the transition indicated by out_pos.
void check_incoming_tau_transitions_become_noninert(block_type *NewBotSt_block_index, state_in_block_pointer *start_bottom, state_in_block_pointer *const end_non_bottom)
makes incoming transitions from block NewBotSt_block_index non-block-inert
std::clock_t end_initial_part
time measurement after creating the initial partition (but before the first call to stabilizeB())
void move_nonbottom_states_to(const todo_state_vector &R, state_in_block_pointer *to_pos, state_index new_block_bottom_size)
Move states in a set to a specific position in m_states_in_block
linked_list< BLC_indicators >::iterator find_inert_co_transition_for_block(block_type *const index_block_B, const constellation_type *const old_constellation, const constellation_type *const new_constellation) const
find a splitter for the tau-transitions from the new constellation to the old constellation
state_index get_eq_class(const state_index si) const
Get the equivalence class of a state.
void swap_states_in_states_in_block_never_equal(state_in_block_pointer *pos1, state_in_block_pointer *pos2)
swap the contents of pos1 and pos2, assuming they are different
bool swap_in_the_doubly_linked_list_LBC_in_blocks_new_block(const transition_index ti, linked_list< BLC_indicators >::iterator new_BLC_block, linked_list< BLC_indicators >::iterator old_BLC_block)
Swap transition ti from BLC set old_BLC_block to BLC set new_BLC_block
std::size_t num_eq_classes() const
Calculate the number of equivalence classes.
bool check_data_structures(const std::string &tag, const bool initialisation=false, const bool check_temporary_complexity_counters=true) const
Checks whether data structures are consistent.
fixed_vector< transition_type > m_transitions
void refine_partition_until_it_becomes_stable()
void order_BLC_transitions_single_BLC_set(state_in_block_pointer *const pos, BLC_list_iterator start_same_BLC, const BLC_list_iterator end_same_BLC)
create one BLC set for the block starting at pos
void create_initial_partition()
const bool m_branching
true iff branching (not strong) bisimulation has been requested
void display_BLC_list(const block_type *const bi) const
Prints the list of BLC sets as debug output.
void clear_state_counters(std::vector< state_in_block_pointer >::const_iterator begin, std::vector< state_in_block_pointer >::const_iterator const end, block_type *const block)
reset a range of state counters to undefined
state_index number_of_states_in_constellation(const constellation_type &C) const
return the number of states in constellation C
void swap_three_iterators_and_update_m_transitions(const BLC_list_iterator i1, const BLC_list_iterator i2, const BLC_list_iterator i3)
Move the content of i1 to i2, i2 to i3 and i3 to i1.
block_type * create_new_block(state_in_block_pointer *start_bottom_states, state_in_block_pointer *const start_non_bottom_states, state_in_block_pointer *const end_states, block_type *const old_block_index, constellation_type *const old_constellation, constellation_type *const new_constellation)
create a new block and adapt the BLC sets, and reset state counters
void order_BLC_transitions(const BLC_list_iterator start_same_BLC, const BLC_list_iterator end_same_BLC, state_in_block_pointer *min_block, state_in_block_pointer *max_block)
order m_BLC_transition entries according to source block
void check_transitions(const bool initialisation, const bool check_temporary_complexity_counters, const bool check_block_to_constellation=true) const
Checks whether the transition data structure is correct.
const bool m_preserve_divergence
true iff divergence-preserving branching bisimulation has been requested
fixed_vector< outgoing_transition_type > m_outgoing_transitions
transitions ordered per source state
void make_stable_and_move_to_start_of_BLC(block_type *const from_block, const linked_list< BLC_indicators >::iterator splitter)
Makes splitter stable and moves it to the beginning of the list.
void update_the_doubly_linked_list_LBC_new_block(block_type *const old_bi, block_type *const new_bi, const transition_index ti, constellation_type *old_constellation, constellation_type *const new_constellation)
Update the BLC list of transition ti, which now starts in block new_bi
fixed_vector< state_type_gj > m_states
information about states
fixed_vector< transition_index > m_BLC_transitions
static LTS_TYPE::labels_size_type m_aut_apply_hidden_label_map(typename LTS_TYPE::labels_size_type l)
void change_non_bottom_state_to_bottom_state(const fixed_vector< state_type_gj >::iterator si)
Moves the former non-bottom state si to the bottom states.
bool swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation(const transition_index ti, linked_list< BLC_indicators >::iterator new_BLC_block, linked_list< BLC_indicators >::iterator old_BLC_block)
Swap transition ti from BLC set old_BLC_block to BLC set new_BLC_block
block_type * four_way_splitB(block_type *const bi, linked_list< BLC_indicators >::iterator const small_splitter, linked_list< BLC_indicators >::iterator const large_splitter, constellation_type *const old_constellation, constellation_type *const new_constellation)
split a block (using main and co-splitter) into up to four subblocks
void swap_states_in_states_in_block_23_never_equal(state_in_block_pointer *pos1, state_in_block_pointer *pos2, state_in_block_pointer *pos3)
Move the contents of pos1 to pos2, those of pos2 to pos3 and those of pos3 to pos1
transition_index accumulate_entries(std::vector< transition_index > &action_counter, const std::vector< label_index > &todo_stack) const
fixed_vector< state_in_block_pointer > m_states_in_blocks
transition_index no_of_non_constellation_inert_BLC_sets
number of non-inert BLC sets in the partition
block_type * update_BLC_sets_new_block(block_type *const old_bi, block_type *const new_bi, constellation_type *const old_constellation, constellation_type *const new_constellation)
Update all BLC sets after a new block has been created.
bool update_the_doubly_linked_list_LBC_new_constellation(block_type *const index_block_B, const transition &t, const transition_index ti)
Move transition t with transition index ti to a new BLC set.
void print_data_structures(const std::string &header, const bool initialisation=false) const
Prints the partition refinement data structure as debug output.
bisim_partitioner_gj(LTS_TYPE &aut, const bool branching=false, const bool preserve_divergence=false)
constructor
bool in_same_class(state_index const s, state_index const t) const
Check whether two states are in the same equivalence class.
bool check_stability(const std::string &tag, const std::vector< std::pair< BLC_list_iterator, BLC_list_iterator > > *calM=nullptr, const std::pair< BLC_list_iterator, BLC_list_iterator > *calM_elt=nullptr, const constellation_type *const old_constellation=null_constellation, const constellation_type *const new_constellation=null_constellation) const
Checks the main invariant of the partition refinement algorithm.
implements the main algorithm for the stutter equivalence quotient
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
std::pair< label_type, block_index_type > observation_t
std::size_t block_index_type
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
std::set< observation_t > derivatives_t
label_type label(observation_t obs)
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
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::map< std::pair< block_index_type, block_index_type >, level_type > greatest_common_ancestor
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)
std::size_t formula_index_type
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
std::size_t block_index_type
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, std::set< block_index_type > > r_tauP
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.
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 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
std::map< block_index_type, std::set< block_index_type > > r_alpha
mcrl2::state_formulas::state_formula counter_formula_aux(const block_index_type B1, const block_index_type B2)
mcrl2::state_formulas::state_formula counter_formula(const std::size_t s, const std::size_t t)
Creates a state formula that distinguishes state s from state t.
void refine_partion_with_respect_to_divergences(void)
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
void add_todo(iterator begin, iterator end)
std::size_t m_todo_indicator
const state_in_block_pointer * data() const
void swap_vec(std::vector< state_in_block_pointer > &other_vec)
std::vector< state_in_block_pointer > m_vec
std::vector< state_in_block_pointer >::iterator iterator
const_iterator begin() const
std::size_t empty() const
const_iterator end() const
void reserve(std::vector< state_in_block_pointer >::size_type new_cap)
const state_in_block_pointer * data_end() const
const state_in_block_pointer & front() const
void add_todo(const state_in_block_pointer s)
bool find(const state_in_block_pointer s) const
std::size_t todo_is_empty() const
std::vector< state_in_block_pointer >::const_iterator const_iterator
state_in_block_pointer move_from_todo()
counters for a B_to_C slice
class for time complexity checks
static int ilog2(state_type size)
calculate the base-2 logarithm, rounded down
static void wait(trans_type units=1)
do some work that cannot be assigned directly
static void check_waiting_cycles()
static unsigned char log_n
value of floor(log2(n)) for easy access
counter_type
Type for complexity budget counters.
@ stabilizeB__distribute_states_over_Phat
@ multiple_swap_states_in_block__swap_state_in_small_block
@ multiple_swap_states_in_block__account_for_swap_in_aborted_block
@ stabilizeB__prepare_block
@ refine_partition_until_it_becomes_stable__find_splitter
@ simple_splitB__find_predecessors_of_R_or_U_state
@ simple_splitB_R__find_predecessors
@ simple_splitB_U__find_predecessors
static void check_temporary_work()
check that not too much superfluous work has been done
static void print_grand_totals()
print grand total of work in the coroutines (to measure overhead)
static void init(state_type n)
starts counting for a new refinement run
compare_transitions_lts(const std::set< std::size_t > &hide_action_set)
bool operator()(const transition &t1, const transition &t2)
const std::set< std::size_t > & m_hide_action_set
const std::set< std::size_t > & m_hide_action_set
bool operator()(const transition &t1, const transition &t2)
compare_transitions_slt(const std::set< std::size_t > &hide_action_set)
bool operator()(const transition &t1, const transition &t2)
compare_transitions_target()
bool operator()(const transition &t1, const transition &t2)
compare_transitions_tl(const std::set< std::size_t > &hide_action_set)
const std::set< std::size_t > & m_hide_action_set
const std::set< std::size_t > & m_hide_action_set
compare_transitions_tls(const std::set< std::size_t > &hide_action_set)
bool operator()(const transition &t1, const transition &t2)
compare_transitions_tsl(const std::set< std::size_t > &hide_action_set)
const std::set< std::size_t > & m_hide_action_set
bool operator()(const transition &t1, const transition &t2)
A class that can be used to store counterexample trees and.
const T * data_end() const
const T * data_cend() const
size_t upperbound(const state_type s) const
indexed_sorted_vector_for_tau_transitions(const LTS_TYPE &aut, bool outgoing)
std::vector< size_t > m_indices
size_t lowerbound(const state_type s) const
const std::vector< state_type > & get_transitions() const
std::vector< state_type > m_states_with_outgoing_or_incoming_tau_transition
size_t upperbound(const state_type s) const
std::vector< CONTENT > m_states_with_outgoing_or_incoming_transition
size_t lowerbound(const state_type s) const
std::vector< size_t > m_indices
std::pair< label_type, state_type > label_state_pair
indexed_sorted_vector_for_transitions(const std::vector< transition > &transitions, state_type num_states, bool outgoing)
const std::vector< CONTENT > & get_transitions() const
void swap(lts_aut_base &)
Standard swap function.
lts_type type()
Provides the type of this lts, in casu lts_aut.
bool operator==(const lts_aut_base &) const
Standard equality function.
lts_type type() const
The lts_type of state_label_dot. In this case lts_dot.
void swap(lts_dot_base &)
The standard swap function.
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....
bool operator==(const lts_fsm_base &other) const
void clear_process_parameters()
Clear the state parameters for this LTS.
std::vector< std::vector< std::string > > m_state_element_values
state_element_values contain the values that can occur at the i-th position of a state label
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::pair< std::string, std::string > process_parameter(std::size_t i) const
Returns the i-th parameter of the state vectors stored in this LTS.
std::vector< std::pair< std::string, std::string > > m_parameters
m_parameters contain the parameters corresponding to the consecutive elements of a state vector....
std::vector< std::pair< std::string, std::string > > process_parameters() const
Return the parameters of the state vectors stored in this LTS.
void add_process_parameter(const std::string &name, const std::string &sort)
Set the state parameters for this LTS.
std::string state_label_to_string(const state_label_fsm &l) const
Pretty print a state value of this FSM.
void swap(lts_fsm_base &other)
Standard swap function.
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.
bool operator==(const lts_lts_base &other) const
Standard equality function;.
process::action_label_list m_action_decls
void swap(lts_lts_base &l)
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.
lts_lts_base()
Default constructor.
const process::action_label_list & action_label_declarations() const
Return action label declarations stored in this LTS.
data::variable_list m_parameters
This class contains an scc partitioner removing inert tau loops.
std::size_t get_eq_class(const std::size_t s) const
Gives the equivalence class number of a state. The equivalence class numbers range from 0 upto (and e...
void dfs_numbering(const state_type t, const indexed_sorted_vector_for_tau_transitions< LTS_TYPE > &src_tgt, std::vector< bool > &visited)
std::size_t num_eq_classes() const
Gives the number of bisimulation equivalence classes of the LTS.
state_type equivalence_class_index
void group_components(const state_type t, const state_type equivalence_class_index, const indexed_sorted_vector_for_tau_transitions< LTS_TYPE > &src_tgt_src, std::vector< bool > &visited)
scc_partitioner(LTS_TYPE &l)
Creates an scc partitioner for an LTS.
void replace_transition_system(const bool preserve_divergence_loops)
The lts for which this partioner is created is replaced by the lts modulo the calculated partition.
~scc_partitioner()=default
Destroys this partitioner.
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.
std::vector< state_type > block_index_of_a_state
std::vector< state_type > dfsn2state
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.
void swap(lts_default_base &)
Standard swap function.
lts_type type()
Provides the type of this lts, in casu lts_none.
bool operator==(const lts_default_base &) const
Standard equality function.
A class to contain labelled transition systems in graphviz format.
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.
lts< state_label_fsm, action_label_string, detail::lts_fsm_base > super
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()
Creates an object containing no information.
A class that contains a labelled transition system.
states_size_type num_state_labels() const
Gets the number of state labels of this LTS.
labels_size_type num_action_labels() const
Gets the number of action labels of this LTS.
states_size_type m_init_state
void add_transition(const transition &t)
Add a transition to the lts.
void set_num_action_labels(const labels_size_type n)
Sets the number of action labels of this LTS.
bool has_action_info() const
Checks whether this LTS has labels associated with its actions, which are numbers.
bool is_tau(labels_size_type action) const
Checks whether an action is a tau action.
std::set< labels_size_type > & hidden_label_set()
Returns the hidden label set that tells for each label what its corresponding hidden label is.
states_size_type num_states() const
Gets the number of states of this LTS.
void set_hidden_label_set(const std::set< labels_size_type > &m)
Sets the hidden label map that tells for each label what its corresponding hidden label is.
void clear_transitions(const std::size_t n=0)
Clear the transitions of an lts.
void set_num_transitions(const std::size_t n)
Sets the number of transitions of this LTS and tries to shrink the datastructure.
void clear_actions()
Clear the action labels of an lts.
void set_num_states(const states_size_type n, const bool has_state_labels=true)
Sets the number of states of this LTS.
void store_action_label_to_be_renamed(const ACTION_LABEL_T &a, const labels_size_type i, std::map< labels_size_type, labels_size_type > &action_rename_map)
void add_state_number_as_state_information()
Label each state with its state number.
static constexpr bool is_probabilistic_lts
An indicator that this is not a probabilistic lts.
bool is_probabilistic(const states_size_type state) const
Gets the label of a state.
ACTION_LABEL_T action_label_t
The type of action labels.
const std::set< labels_size_type > & hidden_label_set() const
Returns the hidden label set that tells for each label what its corresponding hidden label is.
std::vector< transition > m_transitions
std::vector< STATE_LABEL_T > & state_labels()
Provides the state labels of an LTS.
ACTION_LABEL_T action_label(const labels_size_type action) const
Gets the label of an action.
const labels_size_type tau_label_index() const
Provide the index of the label that represents tau.
const std::vector< ACTION_LABEL_T > & action_labels() const
The action labels in this lts.
bool has_state_info() const
Checks whether this LTS has state values associated with its states.
lts(const lts &l)
Creates a copy of the supplied LTS.
void set_initial_state(const states_size_type state)
Sets the initial state number of this LTS.
void set_action_label(const labels_size_type action, const ACTION_LABEL_T &label)
Sets the label of an action.
void rename_labels(const std::map< labels_size_type, labels_size_type > &action_rename_map)
std::set< labels_size_type > m_hidden_label_set
std::vector< STATE_LABEL_T >::size_type states_size_type
The sort that contains the indices of states.
void apply_hidden_actions(const std::vector< std::string > &tau_actions)
Rename actions in the lts by hiding the actions in the vector tau_actions.
labels_size_type apply_hidden_label_map(const labels_size_type action) const
If the action label is registered hidden, it returns tau, otherwise the original label.
std::vector< transition > & get_transitions()
Gets a reference to the vector of transitions of the current lts.
std::vector< ACTION_LABEL_T >::size_type labels_size_type
The sort that represents the indices of labels.
lts & operator=(const lts &l)
Standard assignment operator.
const std::vector< STATE_LABEL_T > & state_labels() const
Provides the state labels of an LTS.
std::vector< STATE_LABEL_T > m_state_labels
STATE_LABEL_T state_label(const states_size_type state) const
Gets the label of a state.
states_size_type add_state(const STATE_LABEL_T &label=STATE_LABEL_T())
Adds a state to this LTS.
STATE_LABEL_T state_label_t
The type of state labels.
void clear()
Clear the transitions system.
lts()
Creates an empty LTS.
bool operator==(const lts &other) const
Standard equality operator.
states_size_type m_nstates
const std::vector< transition > & get_transitions() const
Gets a const reference to the vector of transitions of the current lts.
LTS_BASE base_t
The type of the used lts base.
std::vector< transition >::size_type transitions_size_type
The sort that contains indices of transitions.
states_size_type initial_state() const
Gets the initial state number of this LTS.
void clear_state_labels()
Clear the labels of an lts.
void swap(lts &l)
Swap this lts with the supplied supplied LTS.
void record_hidden_actions(const std::vector< std::string > &tau_actions)
Records all actions with a string that occurs in tau_actions internally.
std::vector< ACTION_LABEL_T > m_action_labels
transitions_size_type num_transitions() const
Gets the number of transitions of this LTS.
void set_state_label(const states_size_type state, const STATE_LABEL_T &label)
Sets the label of a state.
labels_size_type add_action(const ACTION_LABEL_T &label)
Adds an action with a label to this LTS.
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.
The class lts_fsm_t contains labelled transition systems in .fsm format.
probabilistic_lts< state_label_fsm, action_label_string, probabilistic_state_t, detail::lts_fsm_base > super
void save(const std::string &filename) const
Save the labelled transition system to file.
void load(const std::string &filename)
Save the labelled transition system to file.
This class contains probabilistic labelled transition systems in .lts format.
probabilistic_lts_lts_t()
Creates an object containing no information.
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.
const PROBABILISTIC_STATE_T & initial_probabilistic_state() const
Gets the initial state number of this LTS.
super::transitions_size_type transitions_size_type
bool operator==(const probabilistic_lts &other) const
Standard equality operator.
void swap(probabilistic_lts &other)
Swap this lts with the supplied supplied LTS.
super::states_size_type states_size_type
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.
lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > super
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 set_initial_state(const states_size_type s)
void clear()
Clear the transitions system.
probabilistic_lts & operator=(probabilistic_lts &&other)=default
Standard assignment move operator.
PROBABILISTIC_STATE_T probabilistic_state_t
The type of probabilistic labels.
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.
super::state_label_t state_label_t
states_size_type initial_state() const
PROBABILISTIC_STATE_T m_init_probabilistic_state
super::labels_size_type labels_size_type
super::action_label_t action_label_t
const PROBABILISTIC_STATE_T & probabilistic_state(const states_size_type index) const
Gets the probabilistic label of an index.
probabilistic_lts()
Creates an empty LTS.
void set_probabilistic_state(const states_size_type index, const PROBABILISTIC_STATE_T &s)
Sets the probabilistic label corresponding to some index.
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...
std::vector< state_probability_pair >::const_iterator const_iterator
STATE get() const
Get a probabilistic state if is is simple, i.e., consists of a single state.
iterator end()
Gets the end iterator over pairs of state and probability.
PROBABILITY probability_t
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.
std::vector< state_probability_pair >::iterator iterator
void swap(probabilistic_state &other)
Swap this probabilistic state.
reverse_iterator rend()
Gets the reverse end iterator over pairs of state and probability.
std::vector< state_probability_pair >::const_reverse_iterator const_reverse_iterator
bool operator==(const probabilistic_state &other) const
Standard equality operator.
void clear()
Makes the probabilistic state empty.
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.
std::vector< state_probability_pair >::reverse_iterator reverse_iterator
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.
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.
state_label_dot()
The default constructor.
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.
Contains empty state values, used for lts's without state valued.
bool operator==(const state_label_empty &) const
static state_label_empty number_to_label(const std::size_t)
Create a state label consisting of a number as the only list element. For empty state labels this doe...
bool operator!=(const state_label_empty &other) const
state_label_empty operator+(const state_label_empty &) const
An operator to concatenate two state labels.
This class contains state labels for the fsm format.
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()
Default constructor. The label becomes an empty vector.
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()
Default constructor.
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...
atermpp::term_list< lps::state > super
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.
A class containing triples, source label and target representing transitions.
void set_label(const size_type label)
Set the label of the transition.
transition & operator=(const transition &t)=default
Assignment.
void set_to(const size_type to)
Set the target of the transition.
bool operator<(const transition &t) const
Standard lexicographic ordering on transitions.
transition(const std::size_t f, const std::size_t l, const std::size_t t)
Constructor (there is no default constructor).
size_type from() const
The source of the transition.
transition & operator=(transition &&t)=default
Move assignment.
bool operator!=(const transition &t) const
Standard inequality on transitions.
size_type label() const
The label of the transition.
size_type to() const
The target of the transition.
void set_from(const size_type from)
Set the source of the transition.
transition(transition &&t)=default
Move constructor.
transition(const transition &t)=default
Copy constructor.
std::size_t size_type
The type of the elements in a transition.
bool operator==(const transition &t) const
Standard equality on transitions.
action_label(const core::identifier_string &name, const data::sort_expression_list &sorts)
\brief Constructor Z12.
action(const action_label &label, const data::data_expression_list &arguments)
\brief Constructor Z14.
Process specification consisting of a data specification, action labels, a sequence of process equati...
\brief An untyped multi action or data application
Standard exception class for reporting runtime errors.
void div_mod(const big_natural_number &other, big_natural_number &result, big_natural_number &remainder, big_natural_number &calculation_buffer_divisor) const
bool is_number(std::size_t n) const
Returns whether this number equals a number of std::size_t.
big_natural_number(const std::size_t n)
big_natural_number operator*(const big_natural_number &other) const
operator std::size_t() const
Transforms this number to a std::size_t, provided it is sufficiently small. If not an mcrl2::runtime_...
bool operator>=(const big_natural_number &other) const
void is_well_defined() const
std::size_t operator[](const std::size_t n) const
Give the n-th digit where the most significant digit is positioned last.
void add(const big_natural_number &other)
std::vector< std::size_t > m_number
big_natural_number operator+(const big_natural_number &other) const
bool operator==(const big_natural_number &other) const
std::size_t divide_by(std::size_t n)
big_natural_number operator%(const big_natural_number &other) const
std::size_t size() const
Give the number of digits in this big number.
big_natural_number operator-(const big_natural_number &other) const
friend void swap(big_natural_number &x, big_natural_number &y)
Standard overload of swap.
void remove_significant_digits_that_are_zero()
bool operator<=(const big_natural_number &other) const
big_natural_number operator/(const big_natural_number &other) const
void clear()
Sets the number to zero.
bool operator!=(const big_natural_number &other) const
bool is_zero() const
Returns whether this number equals zero.
void multiply(const big_natural_number &other, big_natural_number &result, big_natural_number &calculation_buffer_for_multiplicand) const
void push_back(const std::size_t n)
bool operator<(const big_natural_number &other) const
void subtract(const big_natural_number &other)
bool operator>(const big_natural_number &other) const
void multiply_by(std::size_t n, std::size_t carry)
This class contains labels for probabilistic transistions, consisting of a numerator and a denominato...
probabilistic_arbitrary_precision_fraction operator*(const probabilistic_arbitrary_precision_fraction &other) const
probabilistic_arbitrary_precision_fraction()
static void greatest_common_divisor_destructive(utilities::big_natural_number &x, utilities::big_natural_number &y, utilities::big_natural_number &buffer_divide, utilities::big_natural_number &buffer_remainder, utilities::big_natural_number &buffer)
static utilities::big_natural_number & buffer2()
bool operator>=(const probabilistic_arbitrary_precision_fraction &other) const
static void remove_common_factors(utilities::big_natural_number &enumerator, utilities::big_natural_number &denominator)
bool operator!=(const probabilistic_arbitrary_precision_fraction &other) const
const utilities::big_natural_number & denominator() const
probabilistic_arbitrary_precision_fraction operator+(const probabilistic_arbitrary_precision_fraction &other) const
bool operator<(const probabilistic_arbitrary_precision_fraction &other) const
bool operator>(const probabilistic_arbitrary_precision_fraction &other) const
static probabilistic_arbitrary_precision_fraction & one()
Constant one.
static utilities::big_natural_number greatest_common_divisor(utilities::big_natural_number x, utilities::big_natural_number y)
static utilities::big_natural_number & buffer3()
static utilities::big_natural_number & buffer1()
probabilistic_arbitrary_precision_fraction operator-(const probabilistic_arbitrary_precision_fraction &other) const
utilities::big_natural_number m_denominator
const utilities::big_natural_number & enumerator() const
static probabilistic_arbitrary_precision_fraction & zero()
Constant zero.
probabilistic_arbitrary_precision_fraction operator/(const probabilistic_arbitrary_precision_fraction &other) const
bool operator<=(const probabilistic_arbitrary_precision_fraction &other) const
probabilistic_arbitrary_precision_fraction(const utilities::big_natural_number &enumerator, const utilities::big_natural_number &denominator)
utilities::big_natural_number m_enumerator
bool operator==(const probabilistic_arbitrary_precision_fraction &other) const
bool bisimulation_compare_gjkw(const LTS_TYPE &l1, const LTS_TYPE &l2, bool branching=false, bool preserve_divergence=false)
Checks whether the two initial states of two LTSs are strong or branching bisimilar.
void bisimulation_reduce_gjkw(LTS_TYPE &l, bool branching=false, bool preserve_divergence=false)
Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
bool destructive_bisimulation_compare_gjkw(LTS_TYPE &l1, LTS_TYPE &l2, bool branching=false, bool preserve_divergence=false, bool generate_counter_examples=false)
Checks whether the two initial states of two LTSs are strong or branching bisimilar.
bool destructive_bisimulation_compare_gjkw(LTS_TYPE &l1, LTS_TYPE &l2, bool branching, bool preserve_divergence, bool generate_counter_examples, const std::string &, bool)
std::string debug_id() const
print a B_to_C slice identification for debugging
std::string debug_id() const
print a constellation identification for debugging
fixed_vector< B_to_C_entry > B_to_C
part_trans_t(trans_type m)
permutation_t permutation
permutation array
std::string debug_id() const
print a block identification for debugging
bisim_partitioner_gjkw(LTS_TYPE &l, bool branching=false, bool preserve_divergence=false)
check_complexity::trans_counter_t work_counter
succ_iter_t change_to_C(pred_iter_t pred_iter, ONLY_IF_DEBUG(constln_t *SpC, constln_t *NewC,) bool first_transition_of_state, bool first_transition_of_block)
transition target is moved to a new constellation
block_t * refinable_next
next block in the list of refinable blocks
static permutation_const_iter_t permutation_begin()
provide an iterator to the beginning of the permutation array
permutation_iter_t unmarked_bottom_end()
permutation_const_iter_t end() const
iterator past the last state in the block
void split_inert_to_C(block_t *B)
handle the transitions from the splitter to its own constellation
void set_inert_begin(B_to_C_iter_t new_inert_begin)
void replace_transition_system(bool branching, bool preserve_divergence)
void assert_stability(const part_state_t &part_st) const
assert that the data structure is consistent and stable
succ_const_iter_t slice_begin() const
bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE > init_helper
const constln_t * to_constln() const
compute the goal constellation of the transitions in this slice
succ_iter_t slice_begin_or_before_end()
static state_type nr_of_blocks
total number of blocks with unique sequence number allocated
state_type unmarked_bottom_size() const
provides the number of unmarked bottom states in the block
void replace_transition_system(const part_state_t &part_st, ONLY_IF_DEBUG(bool branching,) bool preserve_divergence)
Replaces the transition relation of the current LTS by the transitions of the bisimulation-reduced tr...
bool split_s_inert_out(state_info_ptr s ONLY_IF_DEBUG(, constln_t *OldC))
Split outgoing transitions of a state in the splitter.
pred_iter_t inert_pred_end()
void set_marked_bottom_begin(permutation_iter_t new_marked_bottom_begin)
void SetFromRed(B_to_C_desc_iter_t new_fromred)
set FromRed to an existing element in to_constln
void make_nontrivial()
makes a constellation non-trivial (i. e. inserts it into the respective list)
permutation_const_iter_t nonbottom_begin() const
iterator to the first non-bottom state in the block
B_to_C_const_iter_t B_to_C_begin() const
pred_const_iter_t inert_pred_end() const
iterator one past the last inert incoming transition
permutation_iter_t marked_bottom_begin()
friend class bisim_partitioner_gjkw_initialise_helper
const block_t * from_block() const
compute the source block of the transitions in this slice
bisim_gjkw::block_t * refine(bisim_gjkw::block_t *RfnB, const bisim_gjkw::constln_t *SpC, const bisim_gjkw::B_to_C_descriptor *FromRed, bool postprocessing, const bisim_gjkw::constln_t *NewC=nullptr)
refine a block into the part that can reach SpC and the part that cannot
block_t * split_off_small_block()
split off a single block from the constellation
bisim_gjkw::block_t * postprocess_new_bottom(bisim_gjkw::block_t *RedB)
Split a block with new bottom states as needed.
void set_succ_begin(succ_iter_t new_out_begin)
B_to_C_iter_t postprocess_begin
iterator to the first transition into this constellation that needs postprocessing
bool add_work_to_bottom_transns(enum check_complexity::counter_type ctr, unsigned max_value)
B_to_C_iter_t B_to_C_end()
bool operator>(const constln_t &other) const
const constln_t * constln() const
get constellation where the state belongs
permutation_const_iter_t begin() const
iterator to the first state in the block
pred_iter_t noninert_pred_begin()
void make_trivial()
makes a constellation trivial (i. e. removes it from the respective list)
succ_iter_t slice_begin()
void swap_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2)
succ_iter_t state_inert_out_end
iterator past the last inert outgoing transition
B_to_C_descriptor(B_to_C_iter_t begin_, B_to_C_iter_t end_)
bool surely_has_no_transition_to(const constln_t *SpC) const
std::size_t operator()(const Key &k) const
bool needs_postprocessing() const
returns true iff the slice is marked for postprocessing
void set_begin(permutation_iter_t new_begin)
permutation_const_iter_t marked_nonbottom_begin() const
iterator to the first marked non-bottom state in the block
permutation_iter_t pos
position of the state in the permutation array
state_type get_eq_class(state_type s) const
static constln_t * nontrivial_first
first constellation in the list of non-trivial constellations
permutation_iter_t unmarked_bottom_begin()
bool operator>=(const constln_t &other) const
std::unordered_map< label_type, state_type > action_block_map
void set_pred_begin(pred_iter_t new_in_begin)
succ_iter_t current_constln()
trans_type nr_of_transitions
permutation_const_iter_t end() const
constant iterator past the last state in the constellation
permutation_iter_t marked_nonbottom_end()
permutation_const_iter_t unmarked_bottom_begin() const
iterator to the first unmarked bottom state in the block
bisim_gjkw::part_trans_t part_tr
void set_succ_end(succ_iter_t new_out_end)
std::vector< state_type > inert_out_per_state
fixed_vector< pred_entry > pred
void set_inert_begin_and_end(B_to_C_iter_t new_inert_begin, B_to_C_iter_t new_inert_end)
B_to_C_const_iter_t inert_begin() const
iterator to the first inert transition of the block
permutation_iter_t unmarked_nonbottom_end()
void make_nonrefinable()
makes a block non-refinable (i. e. removes it from the respective list)
B_to_C_desc_iter_t B_to_C_slice
permutation_const_iter_t marked_bottom_begin() const
iterator to the first marked bottom state in the block
pred_const_iter_t noninert_pred_begin() const
iterator to first non-inert incoming transition
pred_iter_t noninert_pred_end()
bool mark_nonbottom(state_info_ptr s)
mark a non-bottom state
permutation_const_iter_t bottom_begin() const
iterator to the first bottom state in the block
std::string debug_id_short() const
print a short state identification for debugging
permutation_iter_t int_marked_bottom_begin
iterator to the first marked bottom state of the block
void swap_out(pred_iter_t const pos1, pred_iter_t const pos2)
state_type size() const
provides the number of states in the block
void init_transitions(part_state_t &part_st, part_trans_t &part_tr, bool branching, bool preserve_divergence)
initialise the state in part_st and the transitions in part_tr
bool operator==(const Key &other) const
permutation_iter_t int_begin
iterator to the first state in the constellation
succ_iter_t int_current_constln
iterator to first outgoing transition to the constellation of interest
block_t * split_off_blue(permutation_iter_t blue_nonbottom_end)
refine the block (the blue subblock is smaller)
part_state_t(state_type n)
constructor
permutation_iter_t int_bottom_begin
iterator to the first bottom state of the block
permutation_const_iter_t marked_bottom_end() const
iterator past the last marked bottom state in the block
std::vector< state_type > inert_out_per_block
void set_slice_begin_or_before_end(succ_iter_t new_value)
state_type notblue
number of inert transitions to non-blue states
permutation_const_iter_t marked_nonbottom_end() const
iterator one past the last marked non-bottom state in the block
static state_type num_eq_classes()
check_complexity::state_counter_t work_counter
const state_type sort_key
sort key to order constellation-related information
state_type marked_bottom_size() const
provides the number of marked bottom states in the block
std::vector< state_type > states_per_block
bool is_trivial() const
returns true iff the constellation is trivial
state_type nr_of_nonbottom_states
permutation_iter_t int_marked_nonbottom_begin
iterator to the first marked non-bottom state of the block
void make_noninert(succ_iter_t const succ_iter)
permutation_iter_t int_end
iterator past the last state of the block
pred_iter_t inert_pred_begin()
B_to_C_desc_list to_constln
list of B_to_C with transitions from this block
state_type get_nr_of_states() const
provides the number of states in the Kripke structure
static block_t * get_some_refinable()
provides an arbitrary refinable block
static succ_iter_t slice_end(succ_iter_t this_)
block_t * block
block where the state belongs
void create_initial_partition_gjkw(bool branching, bool preserve_divergence)
const constln_t * get_nontrivial_next() const
provides the next non-trivial constellation
void set_constln(constln_t *new_constln)
B_to_C_iter_t inert_begin()
succ_iter_t inert_succ_begin()
void set_marked_nonbottom_begin(permutation_iter_t new_marked_nonbottom_begin)
permutation_iter_t begin()
static permutation_const_iter_t perm_begin
bool operator<(const constln_t &other) const
compares two constellations for ordering them
bool make_refinable()
makes a block refinable (i. e. inserts it into the respective list)
fixed_vector< state_info_entry > state_info
array with all other information about states
state_type state_size() const
provide size of state space
state_type size() const
returns number of states in the constellation
B_to_C_const_iter_t inert_end() const
iterator past the last inert transition of the block
permutation_iter_t unmarked_nonbottom_begin()
const constln_t * constln() const
constellation where the block belongs to
permutation_iter_t bottom_end()
constln_t * int_constln
constellation to which the block belongs
permutation_const_iter_t bottom_end() const
iterator past the last bottom state in the block
static block_t * refinable_first
first block in the list of refinable blocks
static void slice_add_work_to_transns(succ_const_iter_t this_, enum check_complexity::counter_type ctr, unsigned max_value)
void swap_in(B_to_C_iter_t const pos1, B_to_C_iter_t const pos2)
state_type int_seqnr
unique sequence number of this block
succ_const_iter_t succ_begin() const
iterator to first outgoing transition
bool operator<=(const constln_t &other) const
succ_const_iter_t current_constln() const
void new_red_block_created(block_t *OldB, block_t *NewB, bool postprocessing)
handle B_to_C slices after a new red block has been created
void set_end(permutation_iter_t new_end)
void print_trans() const
print all transitions
std::vector< state_type > inert_in_per_state
bool is_refinable() const
checks whether the block is refinable
block_t * split_off_red(permutation_iter_t red_nonbottom_begin)
refine the block (the red subblock is smaller)
succ_iter_t int_slice_begin_or_before_end
points to the last or the first transition to the same constellation
succ_iter_t inert_succ_end()
succ_const_iter_t inert_succ_begin() const
iterator to first inert outgoing transition
permutation_const_iter_t begin() const
constant iterator to the first state in the constellation
bisim_gjkw::part_state_t part_st
pred_iter_t state_in_begin
iterator to first incoming transition
const state_type orig_nr_of_states
permutation_iter_t int_begin
iterator to the first state of the block
pred_iter_t state_inert_in_begin
iterator to first inert incoming transition
void assign_seqnr()
assigns a unique sequence number
std::unordered_map< Key, state_type, KeyHasher > extra_kripke_states
B_to_C_iter_t inert_end()
void new_blue_block_created(block_t *OldB, block_t *NewB)
handle B_to_C slices after a new blue block has been created
~bisim_partitioner_gjkw()
permutation_iter_t marked_bottom_end()
permutation_iter_t begin()
iterator to the first state in the constellation
static state_info_const_ptr s_i_begin
pointer at the first entry in the state_info array
check_complexity::B_to_C_counter_t work_counter
static constln_t * get_some_nontrivial()
provides an arbitrary non-trivial constellation
permutation_const_iter_t unmarked_bottom_end() const
iterator past the last unmarked bottom state in the block
bool operator<(const block_t &other) const
compares two blocks for ordering them
void set_bottom_begin(permutation_iter_t new_bottom_begin)
void set_nonbottom_end(permutation_iter_t new_nonbottom_end)
std::string debug_id() const
print a state identification for debugging
void set_inert_pred_begin(pred_iter_t new_inert_in_begin)
void clear()
deallocates constellations and blocks
constln_t(state_type sort_key_, permutation_iter_t begin_, permutation_iter_t end_, B_to_C_iter_t postprocess_none)
constructor
void set_inert_succ_begin_and_end(succ_iter_t new_inert_out_begin, succ_iter_t new_inert_out_end)
void swap3_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2, succ_iter_t const pos3)
block_t(constln_t *const constln_, permutation_iter_t const begin_, permutation_iter_t const end_)
constructor
const block_t * block(state_type s) const
find block of a state
succ_const_iter_t inert_succ_end() const
iterator past the last inert outgoing transition
permutation_iter_t end()
iterator past the last state in the constellation
succ_const_iter_t slice_begin_or_before_end() const
check_complexity::block_counter_t work_counter
std::vector< state_type > noninert_in_per_state
bisim_partitioner_gjkw_initialise_helper(LTS_TYPE &l, bool branching, bool preserve_divergence)
constructor of the helper class
succ_iter_t state_out_begin
iterator to first outgoing transition
pred_const_iter_t inert_pred_begin() const
iterator to first inert incoming transition
std::string debug_id() const
print a transition identification for debugging
Key(const label_type &f, const state_type &s)
B_to_C_iter_t int_inert_begin
iterator to the first inert transition of the block
void set_unmarked_bottom_end(permutation_iter_t new_unmarked_bottom_end)
pred_const_iter_t noninert_pred_end() const
iterator past the last non-inert incoming transition
void set_inert_end(B_to_C_iter_t new_inert_end)
~part_state_t()
destructor
pred_const_iter_t pred_end() const
iterator past the last incoming transition
constln_t * nontrivial_next
next constellation in the list of non-trivial constellations
bool in_same_class(state_type s, state_type t) const
B_to_C_iter_t int_inert_end
iterator past the last inert transition of the block
fixed_vector< succ_entry > succ
permutation_iter_t nonbottom_end()
static state_info_const_ptr s_i_end
pointer past the last actual entry in the state_info array
void set_pred_end(pred_iter_t new_in_end)
permutation_iter_t bottom_begin()
permutation_const_iter_t unmarked_nonbottom_begin() const
iterator to the first unmarked non-bottom state in the block
void set_end(permutation_iter_t new_end)
set the iterator past the last state in the constellation
permutation_const_iter_t nonbottom_end() const
iterator past the last non-bottom state in the block
succ_const_iter_t succ_end() const
iterator past the last outgoing transition
void set_unmarked_nonbottom_end(permutation_iter_t new_unmarked_nonbottom_end)
void clear()
clear allocated memory
permutation_iter_t nonbottom_begin()
B_to_C_descriptor * FromRed(const constln_t *SpC)
read FromRed
std::string debug_id_short() const
print a short transition identification for debugging
std::vector< state_type > noninert_out_per_block
permutation_const_iter_t unmarked_nonbottom_end() const
iterator past the last unmarked non-bottom state in the block
succ_const_iter_t succ_end() const
void print_block(const char *message, const block_t *B, permutation_const_iter_t begin, permutation_const_iter_t end) const
print a slice of the partition (typically a block)
state_type marked_size() const
provides the number of marked states in the block
permutation_iter_t marked_nonbottom_begin()
pred_const_iter_t pred_end() const
std::vector< state_type > noninert_out_per_state
trans_type trans_size() const
B_to_C_iter_t postprocess_end
iterator past the last transition into this constellation that needs postprocessing
void refine_partition_until_it_becomes_stable_gjkw()
trans_type get_nr_of_transitions() const
provides the number of transitions in the Kripke structure
void print_part(const part_trans_t &part_tr) const
print the partition as a tree (per constellation and block)
permutation_iter_t int_end
iterator past the last state in the constellation
void set_current_constln(succ_iter_t const new_current_constln)
void set_inert_succ_begin(succ_iter_t const new_inert_out_begin)
bool mark(state_info_ptr s)
mark a state
succ_iter_t state_inert_out_begin
iterator to first inert outgoing transition
pred_const_iter_t pred_begin() const
iterator to first incoming transition
bool surely_has_transition_to(const constln_t *SpC) const
void set_begin(permutation_iter_t new_begin)
set the iterator to the first state in the constellation
#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.
#define BRANCH_BIS_EXPERIMENT_JFG
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)
The main namespace for the aterm++ library.
term_balanced_tree< aterm > aterm_balanced_tree
A term_balanced_tree with elements of type aterm.
void make_term_balanced_tree(term_balanced_tree< Term > &result, ForwardTraversalIterator p, const std::size_t size, Transformer transformer)
bool is_aterm_balanced_tree(const aterm &t)
const atermpp::function_symbol & function_symbol_StateImp()
const atermpp::function_symbol & function_symbol_StateMinus()
const atermpp::function_symbol & function_symbol_ActForall()
const atermpp::function_symbol & function_symbol_StateForall()
const atermpp::function_symbol & function_symbol_StateYaledTimed()
const atermpp::function_symbol & function_symbol_RegSeq()
const atermpp::function_symbol & function_symbol_StateNu()
const atermpp::function_symbol & function_symbol_StateConstantMultiplyAlt()
const atermpp::function_symbol & function_symbol_StateExists()
const atermpp::function_symbol & function_symbol_StateVar()
const atermpp::function_symbol & function_symbol_ActMultAct()
const atermpp::function_symbol & function_symbol_StateNot()
const atermpp::function_symbol & function_symbol_ActImp()
const atermpp::function_symbol & function_symbol_StateSum()
const atermpp::function_symbol & function_symbol_ActAt()
const atermpp::function_symbol & function_symbol_StateMu()
const atermpp::function_symbol & function_symbol_RegTransOrNil()
const atermpp::function_symbol & function_symbol_StateMay()
const atermpp::function_symbol & function_symbol_StatePlus()
const atermpp::function_symbol & function_symbol_RegTrans()
const atermpp::function_symbol & function_symbol_RegAlt()
const atermpp::function_symbol & function_symbol_ActAnd()
const atermpp::function_symbol & function_symbol_StateDelayTimed()
const atermpp::function_symbol & function_symbol_StateConstantMultiply()
const atermpp::function_symbol & function_symbol_StateOr()
const atermpp::function_symbol & function_symbol_ActOr()
const atermpp::function_symbol & function_symbol_StateAnd()
const atermpp::function_symbol & function_symbol_StateInfimum()
const atermpp::function_symbol & function_symbol_ActNot()
const atermpp::function_symbol & function_symbol_ActExists()
const atermpp::function_symbol & function_symbol_UntypedRegFrm()
const atermpp::function_symbol & function_symbol_StateSupremum()
const atermpp::function_symbol & function_symbol_StateMust()
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
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.
data_expression nat(const std::string &n)
Constructs expression of type Nat from a string.
Namespace for system defined sort pos.
const function_symbol & c1()
Constructor for function symbol @c1.
data_expression pos(const std::string &n)
Constructs expression of type Pos from a string.
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 -.
Namespace for all data library functionality.
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 <.
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
bool is_untyped_data_parameter(const atermpp::aterm &x)
atermpp::term_list< variable > variable_list
\brief list of variables
atermpp::term_list< assignment > assignment_list
\brief list of assignments
application equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ==.
bool mCRL2logEnabled(const log_level_t level)
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)
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)
The main namespace for the LPS library.
void complete_data_specification(stochastic_specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
void parse_lps(std::istream &, Specification &)
void complete_data_specification(specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
atermpp::term_balanced_tree< data::data_expression > state
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.
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.
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)
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)
const state_info_entry * state_info_const_ptr
fixed_vector< pred_entry >::iterator pred_iter_t
fixed_vector< succ_entry >::const_iterator succ_const_iter_t
permutation_t::iterator permutation_iter_t
fixed_vector< pred_entry >::const_iterator pred_const_iter_t
state_info_entry * state_info_ptr
fixed_vector< state_info_ptr > permutation_t
permutation_t::const_iterator permutation_const_iter_t
std::list< B_to_C_descriptor > B_to_C_desc_list
B_to_C_desc_list::const_iterator B_to_C_desc_const_iter_t
B_to_C_desc_list::iterator B_to_C_desc_iter_t
fixed_vector< B_to_C_entry >::iterator B_to_C_iter_t
fixed_vector< succ_entry >::iterator succ_iter_t
fixed_vector< B_to_C_entry >::const_iterator B_to_C_const_iter_t
static void swap_permutation(permutation_iter_t s1, permutation_iter_t s2)
swap two permutations
constexpr constellation_type * null_constellation
constexpr transition_index undefined
default counter value if the counter field of a state is not in use currently
fixed_vector< outgoing_transition_type >::const_iterator outgoing_transitions_const_it
transition_index * BLC_list_iterator_or_null
fixed_vector< outgoing_transition_type >::iterator outgoing_transitions_it
transition_index * BLC_list_iterator
std::size_t transition_index
constexpr transition_index marked_NewBotSt
counter value to indicate that a state is in the NewBotSt subset
constexpr label_index null_action
const transition_index * BLC_list_const_iterator
constexpr transition_index marked_range
the number of counter values that can be used for one subblock
static void clear(CONTAINER &c)
constexpr block_type * null_block
static constexpr bool is_in_marked_range_of(transition_index counter, enum subblocks subblock)
checks whether a counter value is a marking for a given subblock
constexpr transition_index null_transition
constexpr transition_index marked_HitSmall
constexpr state_index null_state
static constexpr transition_index marked(enum subblocks subblock)
base marking value for a subblock
A base class for the lts_dot labelled transition system.
bool bisimulation_compare(const LTS_TYPE &l1, const LTS_TYPE &l2, const bool branching=false, const bool preserve_divergences=false, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false)
Checks whether the two initial states of two lts's are strong or branching bisimilar.
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
std::string supported_lts_formats_text(lts_type default_format, const std::set< lts_type > &supported)
Gives a textual list describing supported LTS formats.
static std::string mime_type_strings[]
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::size_t state_type
type used to store state (numbers and) counts
void bisimulation_reduce(LTS_TYPE &l, const bool branching=false, const bool preserve_divergences=false)
Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
std::string extension_for_type(const lts_type type)
Gives the filename extension associated with an LTS format.
void unmark_explicit_divergence_transitions(LTS_TYPE &l, const std::size_t divergent_transition_label)
bool bisimulation_compare_gj(const LTS_TYPE &l1, const LTS_TYPE &l2, const bool branching=false, const bool preserve_divergence=false)
Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bis...
std::string string_for_type(const lts_type type)
Gives a string representation of an LTS format.
lts_type parse_format(std::string const &s)
Determines the LTS format from a format specification string.
bool destructive_bisimulation_compare(LTS_TYPE &l1, LTS_TYPE &l2, const bool branching=false, const bool preserve_divergences=false, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false)
Checks whether the two initial states of two lts's are strong or branching bisimilar.
static std::string type_desc_strings[]
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.
bool destructive_bisimulation_compare_gj(LTS_TYPE &l1, LTS_TYPE &l2, const bool branching=false, const bool preserve_divergence=false, const bool generate_counter_examples=false, const std::string &="", bool=false)
Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bis...
std::size_t label_type
type used to store label numbers and counts
std::size_t trans_type
type used to store transition (numbers and) counts
std::string lts_extensions_as_string(const std::set< lts_type > &supported)
Gives a list of extensions for supported LTS formats.
static const std::string type_strings[]
bool lts_named_cmp(const std::string N[], T a, T b)
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)
lts_type guess_format(std::string const &s, const bool be_verbose)
Determines the LTS format from a filename by its extension.
void bisimulation_reduce_gj(LTS_TYPE &l, const bool branching=false, const bool preserve_divergence=false)
nonmember functions serving as interface with the rest of mCRL2
static const std::string extension_strings[]
void get_trans(const outgoing_transitions_per_state_t &begin, tree_set_store &tss, std::size_t d, std::vector< transition > &d_trans, LTS_TYPE &aut)
std::size_t apply_hidden_labels(const std::size_t n, const std::set< std::size_t > &hidden_action_set)
std::string mime_type_for_type(const lts_type type)
Gives the MIME type associated with an LTS format.
static const std::set< lts_type > & initialise_supported_lts_formats()
std::size_t label(const outgoing_transitions_per_state_action_t::const_iterator &i)
Label of an iterator exploring transitions per outgoing state and action.
std::string pp(const state_label_dot &l)
Pretty print function for a state_label_dot. Only prints the label field.
lts_equivalence
LTS equivalence relations.
@ lts_eq_branching_bisim_sigref
@ lts_eq_divergence_preserving_weak_bisim
@ lts_eq_branching_bisim_gjkw
@ lts_red_determinisation
@ lts_eq_branching_bisim_gv
@ lts_eq_divergence_preserving_branching_bisim_sigref
@ lts_eq_divergence_preserving_branching_bisim
@ lts_eq_branching_bisim_gj
@ lts_eq_divergence_preserving_branching_bisim_gjkw
@ lts_eq_divergence_preserving_branching_bisim_gv
@ lts_eq_divergence_preserving_branching_bisim_gj
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.
lts_type
The enumerated type lts_type contains an index for every type type of labelled transition system that...
bool destructive_compare(LTS_TYPE &l1, LTS_TYPE &l2, const lts_preorder pre, const bool generate_counter_example, const std::string &counter_example_file="", const bool structured_output=false, const lps::exploration_strategy strategy=lps::es_breadth, const bool preprocess=true)
Checks whether this LTS is smaller than another LTS according to a preorder.
transition_sort_style
Transition sort styles.
std::multimap< std::pair< transition::size_type, transition::size_type >, transition::size_type > outgoing_transitions_per_state_action_t
Type for exploring transitions per state and action.
std::string pp(const state_label_empty &)
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.
lts_preorder
LTS preorder relations.
@ lts_pre_failures_divergence_refinement
@ lts_pre_trace_anti_chain
@ lts_pre_failures_refinement
@ lts_pre_weak_failures_refinement
@ lts_pre_weak_trace_anti_chain
@ lts_pre_impossible_futures
void group_transitions_on_label_tgt(std::vector< transition > &transitions, const std::size_t number_of_labels, const std::size_t tau_label_index, const std::size_t number_of_states)
static std::vector< std::size_t > bogus_todo_stack
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.
std::size_t to(const outgoing_transitions_per_state_action_t::const_iterator &i)
To state of an iterator exploring transitions per outgoing state and action.
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 sort_transitions(std::vector< transition > &transitions, transition_sort_style ts=src_lbl_tgt)
Sorts the transitions using a sort style.
void determinise(LTS_TYPE &l)
Determinises this LTS.
void group_transitions_on_tgt_label(std::vector< transition > &transitions, const std::size_t number_of_labels, const std::size_t tau_label_index, const std::size_t number_of_states)
std::string pp(const probabilistic_state< STATE, PROBABILITY > &l)
void reduce(LTS_TYPE &l, lts_equivalence eq)
Applies a reduction algorithm to this LTS.
detail::indexed_sorted_vector_for_transitions< outgoing_pair_t > outgoing_transitions_per_state_t
void group_transitions_on_tgt_label(LTS_TYPE &aut)
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 ptr(const transition t)
Sorts the transitions on labels. Action with the tau label are put first.
std::string pp(const action_label_lts &l)
Print the action label to string.
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 scc_reduce(LTS_TYPE &l, const bool preserve_divergence_loops=false)
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)
static const std::size_t const_tau_label_index
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...
std::pair< transition::size_type, transition::size_type > outgoing_pair_t
Type for exploring transitions per state.
bool compare(const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_preorder pre, const bool generate_counter_example, const std::string &counter_example_file="", const bool structured_output=false, const lps::exploration_strategy strategy=lps::es_breadth, const bool preprocess=true)
Checks whether this LTS is smaller than another LTS according to a preorder.
std::string pp(const action_label_string &l)
bool compare(const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false)
Checks whether this LTS is equivalent to another LTS.
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.
atermpp::term_list< action_label > action_label_list
\brief list of action_labels
std::vector< action > action_vector
\brief vector of actions
atermpp::term_list< action > action_list
\brief list of actions
bool is_untyped_multi_action(const atermpp::aterm &x)
process_specification parse_process_specification(std::istream &in)
Parses a process specification from an input stream.
void remove_common_divisor(std::size_t &p, std::size_t &q)
std::size_t hash_combine(const std::size_t h1, const std::size_t h2)
std::size_t multiply_single_number(const std::size_t n1, const std::size_t n2, std::size_t &multiplication_carry)
std::size_t divide_single_number(const std::size_t p, const std::size_t q, std::size_t &remainder)
std::size_t add_single_number(const std::size_t n1, const std::size_t n2, std::size_t &carry)
std::size_t greatest_common_divisor(std::size_t p, std::size_t q)
std::size_t subtract_single_number(const std::size_t n1, const std::size_t n2, std::size_t &carry)
std::string pp(const probabilistic_arbitrary_precision_fraction &l)
std::string pp(const big_natural_number &l)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
void swap(atermpp::term_balanced_tree< T > &t1, atermpp::term_balanced_tree< T > &t2)
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
static const atermpp::function_symbol UntypedRegFrm
static const atermpp::function_symbol StateMu
static const atermpp::function_symbol ActMultAct
static const atermpp::function_symbol RegSeq
static const atermpp::function_symbol StateConstantMultiply
static const atermpp::function_symbol ActNot
static const atermpp::function_symbol StateSum
static const atermpp::function_symbol ActAnd
static const atermpp::function_symbol StateConstantMultiplyAlt
static const atermpp::function_symbol StateForall
static const atermpp::function_symbol StateOr
static const atermpp::function_symbol ActFalse
static const atermpp::function_symbol RegTransOrNil
static const atermpp::function_symbol StateYaledTimed
static const atermpp::function_symbol StateExists
static const atermpp::function_symbol ActExists
static const atermpp::function_symbol StateVar
static const atermpp::function_symbol StateTrue
static const atermpp::function_symbol StateFalse
static const atermpp::function_symbol StateImp
static const atermpp::function_symbol RegAlt
static const atermpp::function_symbol RegTrans
static const atermpp::function_symbol StateMinus
static const atermpp::function_symbol StateNot
static const atermpp::function_symbol StateInfimum
static const atermpp::function_symbol StateDelay
static const atermpp::function_symbol StateYaled
static const atermpp::function_symbol ActAt
static const atermpp::function_symbol StateMay
static const atermpp::function_symbol StateDelayTimed
static const atermpp::function_symbol ActImp
static const atermpp::function_symbol ActTrue
static const atermpp::function_symbol ActForall
static const atermpp::function_symbol StatePlus
static const atermpp::function_symbol StateMust
static const atermpp::function_symbol StateNu
static const atermpp::function_symbol StateAnd
static const atermpp::function_symbol ActOr
static const atermpp::function_symbol StateSupremum
std::vector< state_type > bottom_states
block_index_type parent_block_index
block_index_type block_index
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
block_index_type block_index
std::vector< transition > transitions
std::set< std::pair< label_type, block_index_type > > outgoing_observations
block_index_type parent_block_index
bool operator!=(const BLC_indicators &other) const
BLC_list_iterator_or_null start_marked_BLC
bool has_marked_transitions() const
BLC_list_iterator end_same_BLC
std::string debug_id(const bisim_partitioner_gj< LTS_TYPE > &partitioner, const block_type *from_block=nullptr) const
print a B_to_C slice identification for debugging
BLC_indicators(BLC_list_iterator start, BLC_list_iterator end, bool is_stable)
bool operator==(const BLC_indicators &other) const
check_complexity::BLC_gj_counter_t work_counter
BLC_list_iterator start_same_BLC
std::string debug_id(const bisim_partitioner_gj< LTS_TYPE > &partitioner) const
print a block identification for debugging
state_in_block_pointer * end_states
pointer past the last state in the block
block_type(state_in_block_pointer *start_bottom, state_in_block_pointer *start_non_bottom, state_in_block_pointer *end, constellation_type *new_c)
constructor
check_complexity::block_gj_counter_t work_counter
state_in_block_pointer * start_bottom_states
bool contains_new_bottom_states
a boolean that is true iff the block contains new bottom states
block_type(const block_type &other)
copy constructor. Required by MSCV.
information about a constellation
constellation_type(state_in_block_pointer *const new_start, state_in_block_pointer *const new_end)
state_in_block_pointer * end_const_states
points past the last state in m_states_in_blocks
std::string debug_id(const bisim_partitioner_gj< LTS_TYPE > &partitioner) const
print a constellation identification for debugging
state_in_block_pointer * start_const_states
points to the first state in m_states_in_blocks
information about a transition stored in m_outgoing_transitions
outgoing_transitions_it start_same_saC
outgoing_transition_type(const outgoing_transitions_it sssaC)
outgoing_transition_type()
a pointer to a state, i.e. a reference to a state
fixed_vector< state_type_gj >::iterator ref_state
bool operator!=(const state_in_block_pointer &other) const
bool operator==(const state_in_block_pointer &other) const
state_in_block_pointer(fixed_vector< state_type_gj >::iterator new_ref_state)
information about a state
transition_index no_of_outgoing_block_inert_transitions
number of outgoing block-inert transitions
std::vector< transition >::iterator start_incoming_transitions
first incoming transition
check_complexity::state_gj_counter_t work_counter
state_in_block_pointer * ref_states_in_blocks
pointer to the corresponding entry in m_states_in_blocks
std::string debug_id(const bisim_partitioner_gj< LTS_TYPE > &partitioner) const
print a state identification for debugging
std::string debug_id_short(const bisim_partitioner_gj< LTS_TYPE > &partitioner) const
print a short state identification for debugging
block_type * block
block of the state
outgoing_transitions_it start_outgoing_transitions
first outgoing transition
outgoing_transitions_it ref_outgoing_transitions
check_complexity::trans_gj_counter_t work_counter
std::string debug_id(const bisim_partitioner_gj< LTS_TYPE > &partitioner) const
print a transition identification for debugging
linked_list< BLC_indicators >::iterator transitions_per_block_to_constellation
std::string debug_id_short(const bisim_partitioner_gj< LTS_TYPE > &partitioner) const
print a short transition identification for debugging
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::aterm &t) const
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const
std::size_t operator()(const atermpp::term_balanced_tree< T > &t) const
std::size_t operator()(const mcrl2::lps::multi_action &ma) 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::action_label_string &as) const
std::size_t operator()(const mcrl2::lts::probabilistic_state< STATE, PROBABILITY > &p) const
std::size_t operator()(const mcrl2::lts::transition &t) const
std::size_t operator()(const mcrl2::utilities::big_natural_number &n) const
std::size_t operator()(const mcrl2::utilities::probabilistic_arbitrary_precision_fraction &p) const
linked_list< BLC_indicators > to_constellation
list of descriptors of all BLC sets that contain transitions starting in the block
std::vector< state_in_block_pointer > * R
used during initialisation for a pointer to a vector of marked states
static bool if_R_is_nullptr_then_to_constellation_is_empty_list()
indicates whether the default values of the union members agree
constellation_type * onstellation
constellation that the block is in
constellation_or_first_unmarked_bottom_state(constellation_type *new_c)
state_in_block_pointer * first_unmarked_bottom_state
used during initialisation for the first unmarked bottom state
state_index te_in_reduced_LTS
used during finalizing for the state index in the reduced LTS
state_in_block_pointer * rt_non_bottom_states
start_non_bottom_states_or_state_in_reduced_LTS(state_in_block_pointer *s)
pointer to the corresponding entry in m_BLC_transitions
BLC_list_iterator BLC_transitions
pointer to the corresponding entry in m_BLC_transitions (used during main part of the algorithm)
transition_index transitions
transition index (used during initialisation)
~iterator_or_counter()
Destruct the object as an iterator.
iterator_or_counter()
Construct the object as a transition index.
void convert_to_iterator(const BLC_list_iterator other)
Convert the object from counter to iterator.