mCRL2
Loading...
Searching...
No Matches
liblts_bisim_gjkw.cpp
Go to the documentation of this file.
1// Author(s): David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
2//
3// Copyright: see the accompanying file COPYING or copy at
4// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
5//
6// Distributed under the Boost Software License, Version 1.0.
7// (See accompanying file LICENSE_1_0.txt or copy at
8// http://www.boost.org/LICENSE_1_0.txt)
9
10/// \file liblts_bisim_gjkw.cpp
11///
12/// \brief O(m log n)-time stuttering equivalence algorithm
13///
14/// \details This file implements the efficient partition refinement algorithm
15/// by Groote / Jansen / Keiren / Wijs to calculate the stuttering equivalence
16/// quotient of a Kripke structure. (Labelled transition systems are converted
17/// to Kripke structures before the main algorithm).
18/// The file accompanies the planned publication in the ACM Trans. Comput. Log.
19/// Log. special issue for TACAS 2016, to appear in 2017.
20///
21/// \author David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
22
23#include "mcrl2/lts/detail/liblts_bisim_gjkw.h"
24#include "mcrl2/lts/detail/coroutine.h"
25#include "mcrl2/lts/lts_aut.h"
26#include "mcrl2/lts/lts_fsm.h"
27#include "mcrl2/lts/lts_utilities.h"
28
29
30
31namespace mcrl2::lts::detail
32{
33namespace bisim_gjkw
34{
35
36
37
38
39
40/* ************************************************************************* */
41/* */
42/* R E F I N A B L E P A R T I T I O N */
43/* */
44/* ************************************************************************* */
45
46
47
48
49
50block_t* block_t::refinable_first = nullptr;
51state_type block_t::nr_of_blocks = 0;
52constln_t* constln_t::nontrivial_first = nullptr;
53 #ifndef NDEBUG
54 // These variables are only accessed in debug mode. In release mode,
55 // accessing them would lead to a linker error.
56 state_info_const_ptr state_info_entry::s_i_begin;
57 state_info_const_ptr state_info_entry::s_i_end;
58 permutation_const_iter_t block_t::perm_begin;
59 #endif
60/// \brief refine the block (the blue subblock is smaller)
61/// \details This function is called after a refinement function has found
62/// that the blue subblock is the smaller one. It creates a new block for
63/// the blue states.
64/// \param blue_nonbottom_end iterator past the last blue non-bottom state
65/// \returns pointer to the new (blue) block
66block_t* block_t::split_off_blue(permutation_iter_t const blue_nonbottom_end)
67{ assert(unmarked_nonbottom_end() >= blue_nonbottom_end);
68 assert(unmarked_nonbottom_begin() <= blue_nonbottom_end);
69 assert(0 != unmarked_bottom_size());
70 permutation_iter_t const splitpoint = blue_nonbottom_end +
71 static_cast<permutation_iter_t::difference_type>(unmarked_bottom_size()); assert(splitpoint < end()); assert(begin() < splitpoint);
72 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
73 unsigned const max_counter = check_complexity::log_n -
74 /* It is not necessary to reset the nottoblue counters; these counters */ check_complexity::ilog2((state_type) (splitpoint - begin()));
75 /* are anyway only valid for the maybe-blue states. */ assert((state_type) (splitpoint - begin()) <= size()/2);
76 #endif
77 if (state_type swapcount = std::min(unmarked_bottom_size(),
78 (state_type) (marked_nonbottom_end() - blue_nonbottom_end));
79 0 != swapcount)
80 {
81 // vector swap the states:
82 permutation_iter_t pos1 = blue_nonbottom_end;
83 permutation_iter_t pos2 = unmarked_bottom_end();
84 state_info_ptr const temp = *pos1;
85 for (;;)
86 {
87 --pos2; mCRL2complexity(*pos2, add_work(check_complexity::
88 Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29, max_counter), );
89 *pos1 = *pos2;
90 (*pos1)->pos = pos1;
91 ++pos1;
92 if (0 == --swapcount)
93 {
94 break;
95 }
96 *pos2 = *pos1;
97 (*pos2)-> pos = pos2;
98 }
99 *pos2 = temp;
100 (*pos2)->pos = pos2;
101 }
102
103 // create a new block for the blue states
104 block_t* const NewB = new block_t(constln(), begin(), splitpoint);
105 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
106 NewB->work_counter = work_counter;
107 #endif
108 if (BLOCK_NO_SEQNR != seqnr())
109 {
110 NewB->assign_seqnr();
111 }
112 // NewB->set_begin(begin());
113 NewB->set_bottom_begin(blue_nonbottom_end);
114 NewB->set_marked_nonbottom_begin(blue_nonbottom_end);
115 // NewB->set_marked_bottom_begin(splitpoint);
116 /* NewB->set_end(splitpoint); */ assert(NewB->to_constln.empty());
117 /* NewB->set_inert_begin(?); */ mCRL2complexity(NewB, add_work(check_complexity::
118 /* NewB->set_inert_end(?); */ Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29, max_counter), );
119 for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
120 { // mCRL2complexity(*s_iter, ...) -- optimized to the above call.
121 (*s_iter)->block = NewB;
122 }
123
124 // adapt the old block: it only keeps the red states
125 // set_end(end());
126 set_bottom_begin(marked_bottom_begin());
127 // set_marked_bottom_begin(marked_bottom_begin());
128 set_marked_nonbottom_begin(marked_bottom_begin());
129 set_begin(splitpoint);
130
131 constln()->make_nontrivial();
132
133 return NewB;
134}
135
136block_t* block_t::split_off_red(permutation_iter_t const red_nonbottom_begin)
137{ assert(marked_nonbottom_begin() == red_nonbottom_begin);
138 assert(marked_nonbottom_end() >= red_nonbottom_begin);
139 assert(0 != marked_size());
140 permutation_iter_t const splitpoint = red_nonbottom_begin +
141 unmarked_bottom_size(); assert(begin() < splitpoint); assert(splitpoint < end());
142 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
143 unsigned const max_counter = check_complexity::log_n -
144 /* It is not necessary to reset the nottoblue counters; these counters */ check_complexity::ilog2((state_type) (end() - splitpoint));
145 /* are anyway only valid for the maybe-blue states. */ assert((state_type) (end() - splitpoint) <= size() / 2);
146 #endif
147 if (state_type swapcount = std::min(unmarked_bottom_size(),
148 (state_type) (marked_nonbottom_end() - red_nonbottom_begin));
149 0 != swapcount)
150 {
151 // vector swap the states:
152 permutation_iter_t pos1 = red_nonbottom_begin;
153 permutation_iter_t pos2 = unmarked_bottom_end();
154 state_info_ptr const temp = *pos1;
155 for (;;)
156 { mCRL2complexity(*pos1, add_work(check_complexity::
157 Move_Blue_or_Red_to_a_new_block_NewB_swap_3_29, max_counter), );
158 *pos1 = *--pos2;
159 (*pos1)->pos = pos1;
160 ++pos1;
161 if (0 == --swapcount)
162 {
163 break;
164 }
165 *pos2 = *pos1;
166 (*pos2)->pos = pos2;
167 }
168 *pos2 = temp;
169 (*pos2)->pos = pos2;
170 }
171 // create a new block for the red states
172 block_t* const NewB = new block_t(constln(), splitpoint, end());
173 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
174 NewB->work_counter = work_counter;
175 #endif
176 if (BLOCK_NO_SEQNR != seqnr())
177 {
178 NewB->assign_seqnr();
179 }
180 // NewB->set_end(end());
181 NewB->set_marked_bottom_begin(marked_bottom_begin());
182 NewB->set_bottom_begin(marked_bottom_begin());
183 NewB->set_marked_nonbottom_begin(marked_bottom_begin());
184 /* NewB->set_begin(splitpoint); */ assert(NewB->to_constln.empty());
185 /* NewB->set_inert_begin(?); */ mCRL2complexity(NewB, add_work(check_complexity::
186 /* NewB->set_inert_end(?); */ Move_Blue_or_Red_to_a_new_block_NewB_pointer_3_29, max_counter), );
187 for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
188 { // mCRL2complexity(*s_iter, ...) -- optimized to the above call.
189 (*s_iter)->block = NewB;
190 }
191
192 // adapt the old block: it only keeps the blue states
193 // set_begin(begin());
194 set_marked_nonbottom_begin(red_nonbottom_begin);
195 set_bottom_begin(red_nonbottom_begin);
196 set_marked_bottom_begin(splitpoint);
197 set_end(splitpoint);
198
199 constln()->make_nontrivial();
200
201 return NewB;
202}
203 #ifndef NDEBUG
204 /// \brief print a slice of the partition (typically a block)
205 /// \details If the slice indicated by the parameters is not empty, the
206 /// states in this slice will be printed.
207 /// \param message text printed as a title if the slice is not empty
208 /// \param B block that is being printed (it is checked whether
209 /// states belong to this block)
210 /// \param begin iterator to the beginning of the slice
211 /// \param end iterator past the end of the slice
212 void part_state_t::print_block(const char* const message,
213 const block_t* const B,
214 permutation_const_iter_t begin,
215 permutation_const_iter_t const end) const
216 {
217 if (0 != end - begin)
218 {
219 mCRL2log(log::log_level_t::debug) << "\t\t" << message
220 << (1 < end-begin ? "s:\n" : ":\n");
221 do
222 {
223 mCRL2log(log::log_level_t::debug) << "\t\t\t"
224 << (*begin)->debug_id();
225 if (B != (*begin)->block)
226 {
227 mCRL2log(log::log_level_t::debug) << ", inconsistent: "
228 "points to " << (*begin)->block->debug_id();
229 }
230 if (begin != (*begin)->pos)
231 {
232 mCRL2log(log::log_level_t::debug)
233 << ", inconsistent pointer to state_info_entry";
234 }
235 mCRL2log(log::log_level_t::debug) << '\n';
236 }
237 while (++begin != end);
238 }
239 }
240
241 /// \brief print the partition as a tree (per constellation and block)
242 /// \details The function prints all constellations (in order); for each
243 /// constellation it prints the blocks it consists of; and for each block,
244 /// it lists its states, separated into nonbottom and bottom states.
245 /// \param part_tr partition for the transitions
246 void part_state_t::print_part(const part_trans_t& part_tr) const
247 {
248 assert(permutation.begin() < permutation.end());
249 for (const constln_t* C = permutation.front()->constln(); ; )
250 {
251 mCRL2log(log::log_level_t::debug) << C->debug_id() << ":\n";
252 assert(C->begin() < C->end());
253 for (const block_t* B = (*C->begin())->block; ; )
254 {
255 mCRL2log(log::log_level_t::debug) << "\t" << B->debug_id();
256 if (C != B->constln())
257 {
258 mCRL2log(log::log_level_t::debug) << ", inconsistent: "
259 "points to " << B->constln()->debug_id();
260 }
261 mCRL2log(log::log_level_t::debug) << ":\n";
262 print_block("Non-bottom state", B, B->nonbottom_begin(),
263 B->nonbottom_end());
264 print_block("Bottom state", B, B->bottom_begin(),
265 B->bottom_end());
266 mCRL2log(log::log_level_t::debug) << "\t\tThis block has ";
267 if (B->inert_end() == part_tr.B_to_C_begin())
268 {
269 mCRL2log(log::log_level_t::debug)
270 << "no transitions to its own constellation.\n";
271 assert(B->inert_begin() == B->inert_end());
272 }
273 else
274 {
275 assert(B->inert_end() ==
276 B->inert_end()[-1].B_to_C_slice->end);
277 assert(B->inert_end()[-1].B_to_C_slice->from_block() == B);
278 assert(B->inert_end()[-1].B_to_C_slice->to_constln() == C);
279 mCRL2log(log::log_level_t::debug) << B->inert_end() -
280 B->inert_end()[-1].B_to_C_slice->begin
281 <<" transition(s) to its own constellation,\n\t\tof which "
282 << B->inert_end() - B->inert_begin()
283 << (1 == B->inert_end() - B->inert_begin()
284 ? " is inert.\n" : " are inert.\n");
285 }
286 // go to next block
287 if (C->end()
288 == B->end())
289 {
290 break;
291 }
292 B = (*B->end())->block;
293 }
294 // go to next constellation
295 if (permutation.end()
296 == C->end())
297 {
298 break;
299 }
300 C = (*C->end())->constln();
301 }
302 }
303
304 /// \brief print all transitions
305 /// \details For each state (in order), its outgoing transitions are
306 /// listed, sorted by goal constellation. The function also indicates
307 /// where the current constellation pointer of the state points at.
308 void part_state_t::print_trans() const
309 {
310 fixed_vector<state_info_entry>::const_iterator const state_info_end =
311 state_info.end() - 1;
312 for (fixed_vector<state_info_entry>::const_iterator state_iter =
313 state_info.begin(); state_info_end != state_iter; ++state_iter)
314 {
315 // print transitions out of state
316 succ_const_iter_t succ_constln_iter = state_iter->succ_begin();
317 if (state_iter->succ_end() != succ_constln_iter)
318 {
319 mCRL2log(log::log_level_t::debug) << state_iter->debug_id()
320 << ":\n";
321 assert(state_iter->succ_begin() <=
322 state_iter->inert_succ_begin());
323 assert(state_iter->inert_succ_begin() <=
324 state_iter->inert_succ_end());
325 assert(state_iter->succ_begin()==state_iter->inert_succ_begin()
326 || *state_iter->inert_succ_begin()[-1].target->constln() <=
327 *state_iter->constln());
328 assert(state_iter->succ_begin()==state_iter->inert_succ_begin()
329 || state_iter->inert_succ_begin()[-1].target->block !=
330 state_iter->block);
331 assert(state_iter->inert_succ_begin() ==
332 state_iter->inert_succ_end() ||
333 (state_iter->inert_succ_begin()->target->block ==
334 state_iter->block &&
335 state_iter->inert_succ_end()[-1].target->block ==
336 state_iter->block));
337 assert(state_iter->succ_end() == state_iter->inert_succ_end()||
338 *state_iter->constln() <
339 *state_iter->inert_succ_end()->target->constln());
340 do
341 {
342 // print transitions to a constellation
343 mCRL2log(log::log_level_t::debug) << "\ttransitions to "
344 << succ_constln_iter->target->constln()->debug_id()
345 << ":\n";
346 succ_const_iter_t s_iter = succ_constln_iter;
347 // set succ_constln_iter to the end of the transitions to
348 // this constellation
349 succ_constln_iter=succ_entry::slice_end(succ_constln_iter);
350 for ( ;s_iter != succ_constln_iter ;++s_iter)
351 {
352 mCRL2log(log::log_level_t::debug) << "\t\tto "
353 << s_iter->target->debug_id();
354 if (state_iter->inert_succ_begin() <= s_iter &&
355 s_iter < state_iter->inert_succ_end())
356 {
357 mCRL2log(log::log_level_t::debug) << " (inert)";
358 }
359 if (state_iter->current_constln() == s_iter)
360 {
361 mCRL2log(log::log_level_t::debug)
362 << " <- current_constln";
363 }
364 mCRL2log(log::log_level_t::debug) << '\n';
365 assert(s_iter->B_to_C->pred->succ == s_iter);
366 assert(s_iter->B_to_C->pred->source == &*state_iter);
367 }
368 }
369/* ************************************************************************* */ while (state_iter->succ_end() != succ_constln_iter);
370/* */ if (state_iter->current_constln() == state_iter->succ_end())
371/* T R A N S I T I O N S */ {
372/* */ mCRL2log(log::log_level_t::debug)
373/* ************************************************************************* */ << "\t\t<- current_constln\n";
374 }
375 }
376 }
377 }
378 #endif // ifndef NDEBUG
379/// \brief handle the transitions from the splitter to its own constellation
380/// \details split_inert_to_C splits the B_to_C slice of block SpB to its own
381/// constellation into two slices: one for the inert and one for the non-inert
382/// transitions. It is called with SpB just after a constellation is split, as
383/// the transitions from SpB to itself (= the inert transitions) now go to a
384/// different constellation than the other transitions from SpB to its old
385/// constellation. It does, however, not adapt the other transition arrays to
386/// reflect that noninert and inert transitions from block SpB would go to
387/// different constellations.
388///
389/// Its time complexity is O(1+min{|out_noninert(SpB-->C)|, |inert_out(SpB)|}).
390/// \param SpB pointer to the splitter block
391void part_trans_t::split_inert_to_C(block_t* const SpB)
392{
393 // if there are no inert transitions
394 if (SpB->inert_begin() == SpB->inert_end())
395 {
396 if (SpB->inert_end() != B_to_C.begin())
397 {
398 // There are noninert transitions from SpB to its old
399 // constellation: they all go to SpC.
400 SpB->SetFromRed(SpB->inert_end()[-1].B_to_C_slice);
401 // There are no more transitions from SpB to its own constellation
402 SpB->set_inert_begin(B_to_C.begin());
403 SpB->set_inert_end(B_to_C.begin());
404 }
405 return;
406 }
407 B_to_C_desc_iter_t const slice = SpB->inert_begin()->B_to_C_slice;
408 // if all transitions are inert
409 if (slice->begin == SpB->inert_begin())
410 {
411 return;
412 }
413
414 // now the slice actually has to be split
415 B_to_C_desc_iter_t new_slice;
416 // select the smaller number of swaps to decide which part should be the
417 // new one:
418 if(SpB->inert_begin() - slice->begin < slice->end - SpB->inert_begin())
419 {
420 // fewer noninert transitions
421 SpB->to_constln.emplace_front(slice->begin, SpB->inert_begin());
422 new_slice = SpB->to_constln.begin();
423 /* SpB->SetFromRed(new_slice); */ assert(new_slice->from_block() == SpB);
424 slice->begin = SpB->inert_begin();
425 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
426 new_slice->work_counter = slice->work_counter;
427 // We actually change the pointers in the new slice (i. e. the pointers of
428 // the non-inert transitions) because there are fewer of them; however, we
429 // still have to assign this work to the inert transitions.
430 mCRL2complexity(slice, add_work(check_complexity::
431 Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17,
432 check_complexity::log_n-check_complexity::ilog2(SpB->size())), );
433 #endif
434 }
435 else
436 {
437 // fewer (or equal) inert transitions
438 SpB->to_constln.emplace_back(SpB->inert_begin(), slice->end);
439 new_slice = std::prev(SpB->to_constln.end());
440 slice->end = SpB->inert_begin();
441 SpB->SetFromRed(slice);
442 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
443 new_slice->work_counter = slice->work_counter;
444 mCRL2complexity(new_slice, add_work(check_complexity::
445 Register_that_inert_transitions_from_s_go_to_NewC_B_to_C_2_17,
446 check_complexity::log_n-check_complexity::ilog2(SpB->size())), );
447 #endif
448 }
449 // set the slice pointers of the smaller part to the new slice:
450 for (B_to_C_iter_t iter = new_slice->begin; new_slice->end != iter; ++iter)
451 { // mCRL2complexity(...) -- optimized to the above calls.
452 assert(B_to_C.end() > iter); assert(iter->pred->succ->B_to_C == iter);
453 iter->B_to_C_slice = new_slice;
454 }
455}
456
457
458/// \brief transition target is moved to a new constellation
459/// \details part_trans_t::change_to_C has to be called after a transition
460/// target has changed its constellation. The member function will adapt the
461/// transition data structure. It assumes that the transition is non-inert and
462/// that the new constellation does not (yet) have _inert_ incoming
463/// transitions. It returns the boundary between transitions to SpC and
464/// transitions to NewC in the state's outgoing transition array.
465///
466/// In debug mode, two additional parameters `SpC` (splitter constellation) and
467/// `NewC` (new constellation) are available for assertions.
468/// \param pred_iter transition that has to be changed
469/// \param first_transition_of_state This is the first transition of the
470/// state, so a new constln slice is started.
471/// \param first_transition_of_block This is the first transition of the
472/// block, so a new B_to_C slice has to be
473/// allocated.
474succ_iter_t part_trans_t::change_to_C(pred_iter_t const pred_iter, ONLY_IF_DEBUG( constln_t* const SpC, constln_t* const NewC, )
475 bool const first_transition_of_state, bool const first_transition_of_block)
476{ assert(pred_iter<pred.end()); assert(pred_iter->succ->B_to_C->pred==pred_iter);
477 // adapt the B_to_C array:
478 // always move the transition to the beginning of the slice (this will make
479 // it easier because inert transitions are stored at the end of a slice).
480 B_to_C_iter_t const old_B_to_C_pos = pred_iter->succ->B_to_C;
481 B_to_C_desc_iter_t const old_B_to_C_slice = old_B_to_C_pos->B_to_C_slice;
482 B_to_C_iter_t const new_B_to_C_pos = old_B_to_C_slice->begin; assert(new_B_to_C_pos < B_to_C.end());
483 B_to_C_desc_iter_t new_B_to_C_slice; assert(new_B_to_C_pos->pred->succ->B_to_C == new_B_to_C_pos);
484 if (first_transition_of_block)
485 {
486 // create a new slice in B_to_C for the transitions from RfnB to NewC
487 block_t* const RfnB = pred_iter->source->block;
488 RfnB->to_constln.emplace_back(new_B_to_C_pos, new_B_to_C_pos);
489 new_B_to_C_slice = std::prev(RfnB->to_constln.end());
490 #ifndef NDEBUG
491 new_B_to_C_slice->work_counter = old_B_to_C_slice->work_counter;
492 #endif
493 RfnB->SetFromRed(old_B_to_C_slice);
494 }
495 else
496 {
497 new_B_to_C_slice = new_B_to_C_pos[-1].B_to_C_slice;
498 }
499 ++new_B_to_C_slice->end;
500 ++old_B_to_C_slice->begin; assert(new_B_to_C_slice->end == old_B_to_C_slice->begin);
501 swap_B_to_C(pred_iter->succ, new_B_to_C_pos->pred->succ);
502 new_B_to_C_pos->B_to_C_slice = new_B_to_C_slice;
503 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
504 {
505 // this was the last transition from RfnB to SpC
506 block_t* const RfnB = pred_iter->source->block;
507 if (RfnB->inert_end() == old_B_to_C_slice->begin)
508 { assert(RfnB->inert_begin() == RfnB->inert_end());
509 // this was the last transition from RfnB to its own constellation
510 RfnB->set_inert_begin(B_to_C.begin());
511 RfnB->set_inert_end(B_to_C.begin());
512 } assert(RfnB->to_constln.begin() == old_B_to_C_slice);
513 RfnB->to_constln.erase(old_B_to_C_slice);
514 }
515 // adapt the outgoing transition array:
516 // move the transition to the beginning
517 succ_iter_t const old_out_pos = pred_iter->succ; assert(succ.end() > old_out_pos);
518 assert(old_out_pos->B_to_C->pred->succ == old_out_pos);
519 /* move to beginning */ assert(*NewC < *SpC);
520 succ_iter_t const new_out_pos = old_out_pos->slice_begin();
521 swap_out(pred_iter, new_out_pos->B_to_C->pred);
522 if (succ_iter_t const old_slice_end = succ_entry::slice_end(old_out_pos);
523 old_slice_end > new_out_pos + 1)
524 {
525 // the following assignment might assign an illegal transition if the
526 // old slice becomes empty -- but then it doesn't hurt, because it will
527 // be overwritten below. However, Visual Studio C complains.
528 old_slice_end[-1].set_slice_begin_or_before_end(new_out_pos + 1); assert(old_slice_end - 1 == new_out_pos->slice_begin_or_before_end());
529 } else
530 { assert(old_slice_end - 1 == new_out_pos);
531 assert(old_slice_end-1==old_slice_end[-1].slice_begin_or_before_end());
532 }
533 if (first_transition_of_state)
534 {
535 new_out_pos->set_slice_begin_or_before_end(new_out_pos);
536 }
537 else
538 { assert(pred_iter->source->current_constln() == new_out_pos);
539 new_out_pos->set_slice_begin_or_before_end(
540 new_out_pos[-1].slice_begin_or_before_end());
541 }
542 return new_out_pos + 1;
543}
544
545
546/// \brief Split outgoing transitions of a state in the splitter
547/// \details split_s_inert_out splits the outgoing transitions from `s` to its
548/// own constellation into two: the inert transitions become transitions to
549/// the new constellation of which `s` is now part; the non-inert transitions
550/// remain transitions to `OldC` (the old constellation, only available in debug
551/// mode).
552/// Its time complexity is O(1 + min { |out_notau(s)|, |out_tau(s)| }).
553/// \result true iff the state also has transitions to OldC
554bool part_trans_t::split_s_inert_out(state_info_ptr s ONLY_IF_DEBUG( , constln_t* OldC )
555 )
556{
557 constln_t* NewC = s->constln(); assert(*NewC < *OldC); assert(NewC->sort_key + OldC->size() == OldC->sort_key);
558 assert(OldC->end() == NewC->begin() || NewC->end() == OldC->begin());
559 succ_iter_t split
560 = s->inert_succ_begin();
561 succ_iter_t to_C_end
562 = s->inert_succ_end();
563 assert(
564 s->succ_begin() == to_C_end
565 || to_C_end[-1]
566 .slice_begin_or_before_end()
567 < to_C_end);
568 succ_iter_t to_C_begin
569 = s->succ_begin() == to_C_end
570 ? to_C_end
571 : to_C_end[-1]
572 .slice_begin_or_before_end();
573 //< If s has no transitions to OldC at
574 //all, then to_C_begin may be the
575 // beginning of the constln_slice for
576 // transitions to another constellation.
577 // We will check that later.
578 bool result = to_C_begin < split; assert(to_C_begin <= split); assert(split <= to_C_end);
579 assert(succ.end() == split || split->B_to_C->pred->succ == split);
580 assert(succ.end() == to_C_end || to_C_end->B_to_C->pred->succ == to_C_end);
581 assert(succ.end() == to_C_begin ||
582 to_C_begin->B_to_C->pred->succ == to_C_begin);
583 if (!result)
584 {
585 ;
586 }
587 else if (split < to_C_end)
588 {
589 // s has both inert and non-inert
590 // transitions
591 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
592 /* the out-transitions of s also have to be swapped. */ unsigned const max_counter = check_complexity::log_n -
593 /* Actually only B_to_C and the target need to be swapped, as the */ check_complexity::ilog2(NewC->size());
594 /* constln_slices are (still) identical. */ assert(*NewC < *OldC);
595 #endif
596 trans_type swapcount = std::min(to_C_end - split, split - to_C_begin);
597 split = to_C_end - split + to_C_begin; assert(0 != swapcount);
598
599 succ_iter_t pos1 = to_C_begin;
600 succ_iter_t pos2 = to_C_end;
601 state_info_ptr temp_target = pos1->target;
602 B_to_C_iter_t temp_B_to_C = pos1->B_to_C;
603 for (;;)
604 {
605 --pos2; mCRL2complexity(pos2->B_to_C->pred, add_work(check_complexity::
606 Register_that_inert_transitions_from_s_go_to_NewC_swap_2_17,
607 max_counter), );
608 pos1->target = pos2->target;
609 pos1->B_to_C = pos2->B_to_C;
610 pos1->B_to_C->pred->succ = pos1;
611 ++pos1;
612 if (0 == --swapcount)
613 {
614 break;
615 }
616 pos2->target = pos1->target;
617 pos2->B_to_C = pos1->B_to_C;
618 pos2->B_to_C->pred->succ = pos2;
619 }
620 pos2->target = temp_target;
621 pos2->B_to_C = temp_B_to_C;
622 pos2->B_to_C->pred->succ = pos2;
623
624 s->set_inert_succ_begin_and_end(to_C_begin, split); assert(s->succ_begin() == s->inert_succ_begin() ||
625 *s->inert_succ_begin()[-1].target->constln() < *NewC);
626 assert(s->inert_succ_begin()->target->block == s->block);
627 assert(s->inert_succ_end()[-1].target->block == s->block);
628 assert(s->inert_succ_end() < s->succ_end());
629 /* set the pointer to the slice for the inert transitions. */ assert(OldC == s->inert_succ_end()->target->constln());
630 to_C_end[-1].set_slice_begin_or_before_end(split);
631 split[-1].set_slice_begin_or_before_end(to_C_begin);
632 for (succ_iter_t succ_iter = split - 1; to_C_begin != succ_iter; )
633 {
634 --succ_iter; mCRL2complexity(succ_iter->B_to_C->pred,add_work(check_complexity::
635 Register_that_inert_transitions_from_s_go_to_NewC_succ_2_17,
636 max_counter), );
637 assert(succ.end() > succ_iter);
638 assert(succ_iter->B_to_C->pred->succ == succ_iter);
639 succ_iter->set_slice_begin_or_before_end(split - 1);
640 }
641 }
642 else if (*to_C_begin->target->constln() > *NewC)
643 {
644 // s has (noninert) transitions to OldC, but no (inert)
645 /* transitions to NewC. */ assert(to_C_begin->target->constln() == OldC);
646 s->set_inert_succ_begin_and_end(to_C_begin, to_C_begin); assert(s->succ_begin() == s->inert_succ_begin() ||
647 *s->inert_succ_begin()[-1].target->constln() < *NewC);
648 assert(s->succ_end() > s->inert_succ_end()); assert(to_C_end == split);
649 assert(OldC == s->inert_succ_end()->target->constln());
650 }
651 else
652 {
653 // s actually hasn't got transitions to OldC at all, so `result`
654 // should not be true.
655 result = false;
656 }
657 #ifndef NDEBUG
658 if (succ_iter_t succ_iter = s->succ_begin(); succ_iter != s->succ_end())
659 {
660 do
661 {
662 assert(succ_iter->B_to_C->pred->source == s);
663 }
664 while (++succ_iter != s->succ_end());
665 assert(s->succ_begin() == s->inert_succ_begin() ||
666 *s->inert_succ_begin()[-1].target->constln() < *NewC);
667 assert(s->inert_succ_begin() == s->inert_succ_end() ||
668 (s->inert_succ_begin()->target->block == s->block &&
669 s->inert_succ_end()[-1].target->block == s->block));
670 assert(s->inert_succ_end() == s->succ_end() ||
671 *NewC < *s->inert_succ_end()->target->constln());
672 }
673 #endif // ifndef NDEBUG
674 return result;
675}
676
677
678/// \brief handle B_to_C slices after a new blue block has been created
679/// \details part_trans_t::new_blue_block_created splits the B_to_C-slices to
680/// reflect that some transitions now start in the new block NewB. They can no
681/// longer be in the same slice as the transitions that start in the old block.
682/// Its time complexity is O(1 + |out(NewB)|).
683/// \param RfnB the old block that has been refined (now the red subblock)
684/// \param NewB the new block (the blue subblock)
685void part_trans_t::new_blue_block_created(block_t* const RfnB,
686 block_t* const NewB)
687{ assert(RfnB->constln()==NewB->constln()); assert(NewB->end()==RfnB->begin());
688 NewB->set_inert_begin_and_end(B_to_C.begin(), B_to_C.begin());
689 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
690 unsigned const max_counter = check_complexity::log_n -
691 check_complexity::ilog2(NewB->size());
692 mCRL2complexity(NewB, add_work(check_complexity::
693 /* for all outgoing transitions of NewB */ Move_Blue_or_Red_to_a_new_block_states_3_29, max_counter), );
694 #endif
695 for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
696 { // mCRL2complexity(*s_iter, ...) -- optimized to the above call
697 for (succ_iter_t succ_iter = (*s_iter)->succ_begin();
698 (*s_iter)->succ_end() != succ_iter; ++succ_iter)
699 { mCRL2complexity(succ_iter->B_to_C->pred,add_work(check_complexity::
700 Move_Blue_or_Red_to_a_new_block_succ_3_29, max_counter), );
701 /* Move the transition to a new slice: */ assert(succ.end()>succ_iter); assert(succ_iter->B_to_C->pred->succ==succ_iter);
702 B_to_C_iter_t const old_pos = succ_iter->B_to_C;
703 B_to_C_desc_iter_t const old_B_to_C_slice = old_pos->B_to_C_slice;
704 B_to_C_iter_t const after_new_pos = old_B_to_C_slice->end; assert(B_to_C.end() > old_pos); assert(after_new_pos > old_pos);
705 assert(old_pos->pred->succ->B_to_C == old_pos);
706 assert(B_to_C.end() == after_new_pos ||
707 after_new_pos->pred->succ->B_to_C == after_new_pos);
708 B_to_C_desc_iter_t new_B_to_C_slice;
709 if (B_to_C.end() == after_new_pos ||
710 after_new_pos->pred->source->block != NewB ||
711 after_new_pos->pred->succ->target->constln() !=
712 succ_iter->target->constln())
713 {
714 // create a new B_to_C-slice
715 // this can only happen when the first transition from
716 // *s_iter to a new constellation is handled.
717 if (!old_B_to_C_slice->needs_postprocessing())
718 {
719 // (During primary refinement [Line 2.23]: There is no need
720 // to put the FromRed-slice of the new blue block into
721 // position like in new_red_block_created(), as only the
722 // red subblock will be refined further in Line 2.24.)
723 // During postprocessing:
724 // the old_B_to_C_slice does not need postprocessing, so
725 // its corresponding new slice should be in a similar
726 // position near the beginning of the list of slices.
727 NewB->to_constln.emplace_front(after_new_pos,
728 after_new_pos); // new_B_to_C_slice is not yet fully initialised, therefore
729 new_B_to_C_slice = NewB->to_constln.begin(); // the assertion fails:
730 // assert(new_B_to_C_slice->from_block() == NewB);
731 }
732 else
733 {
734 // During postprocessing:
735 // the old_B_to_C_slice needs postprocessing, so also the
736 // new_B_to_C_slice will need postprocessing.
737 NewB->to_constln.emplace_back(after_new_pos,after_new_pos);
738 new_B_to_C_slice = std::prev(NewB->to_constln.end());
739 }
740 #ifndef NDEBUG
741 new_B_to_C_slice->work_counter = old_B_to_C_slice->work_counter;
742 #endif
743 if (RfnB->inert_end() == after_new_pos)
744 {
745 /* this is the first transition from NewB to its own */ assert(NewB->inert_begin() == B_to_C.begin());
746 /* constellation. Adapt the pointers accordingly. */ assert(NewB->inert_end() == B_to_C.begin());
747 NewB->set_inert_end(after_new_pos);
748 NewB->set_inert_begin(after_new_pos);
749 }
750 }
751 else
752 {
753 // the slice at after_new_pos is already the correct one
754 new_B_to_C_slice = after_new_pos->B_to_C_slice;
755 }
756 --new_B_to_C_slice->begin;
757 --old_B_to_C_slice->end; assert(new_B_to_C_slice->begin == old_B_to_C_slice->end);
758 B_to_C_iter_t new_pos = after_new_pos - 1; assert(B_to_C.end() > new_pos);
759 assert(new_pos->pred->succ->B_to_C == new_pos);
760 if (RfnB->inert_end() == after_new_pos)
761 {
762 // The transition goes from NewB to the constellation of
763 // RfnB and NewB.
764 if (RfnB->inert_begin() <= old_pos)
765 {
766 // The transition is inert and has to be moved over the
767 // non-inert transitions of NewB.
768 NewB->set_inert_begin(NewB->inert_begin() - 1);
769 new_pos = NewB->inert_begin();
770 // old_pos --> new_pos --> new_B_to_C_slice->begin -->
771 // old_pos
772 swap3_B_to_C(succ_iter, new_pos->pred->succ,
773 new_B_to_C_slice->begin->pred->succ);
774 }
775 else
776 {
777 // The transition is non-inert, but it has to be moved
778 // over the inert transitions of RfnB.
779 RfnB->set_inert_begin(RfnB->inert_begin() - 1);
780 // old_pos --> new_pos --> RfnB->inert_begin() -> old_pos
781 swap3_B_to_C(succ_iter, new_pos->pred->succ,
782 RfnB->inert_begin()->pred->succ);
783 }
784 RfnB->set_inert_end(RfnB->inert_end() - 1);
785 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
786 {
787 // This was the last transition from RfnB to its own
788 // constellation.
789 RfnB->set_inert_begin(B_to_C.begin());
790 RfnB->set_inert_end(B_to_C.begin());
791
792 RfnB->to_constln.erase(old_B_to_C_slice);
793 }
794 }
795 else
796 {
797 // The transition goes from NewB to a constellation that
798 // does not contain RfnB or NewB. No special treatment is
799 // required.
800 swap_B_to_C(succ_iter, new_pos->pred->succ);
801 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
802 {
803 RfnB->to_constln.erase(old_B_to_C_slice);
804 }
805 }
806 new_pos->B_to_C_slice = new_B_to_C_slice;
807 }
808 }
809 #ifndef NDEBUG
810 if (RfnB->inert_begin() == RfnB->inert_end() &&
811 RfnB->inert_end() != B_to_C.begin() &&
812 (RfnB->inert_end()[-1].pred->source->block != RfnB ||
813 RfnB->inert_end()[-1].pred->succ->target->constln()
814 != RfnB->constln()))
815 {
816 assert(0 && "The old block has no transitions to its own "
817 "constellation, but its inert_begin and "
818 "inert_end pointers are not set to B_to_C.begin()");
819 }
820 if (RfnB->inert_end() != B_to_C.begin())
821 {
822 assert(RfnB->inert_end()[-1].pred->source->block == RfnB);
823 assert(RfnB->inert_end()[-1].pred->succ->target->constln() ==
824 RfnB->constln());
825 }
826 if (NewB->inert_begin() == NewB->inert_end() &&
827 NewB->inert_end() != B_to_C.begin() &&
828 (NewB->inert_end()[-1].pred->source->block != NewB ||
829 NewB->inert_end()[-1].pred->succ->target->constln()
830 != NewB->constln()))
831 {
832 assert(0 && "The new block has no transitions to its own "
833 "constellation, but its inert_begin and "
834 "inert_end pointers are not set to B_to_C.begin()");
835 }
836 if (NewB->inert_end() != B_to_C.begin())
837 {
838 assert(NewB->inert_end()[-1].pred->source->block == NewB);
839 assert(NewB->inert_end()[-1].pred->succ->target->constln() ==
840 NewB->constln());
841 }
842 #endif
843}
844
845
846/// \brief handle B_to_C slices after a new red block has been created
847/// \details part_trans_t::new_red_block_created splits the B_to_C-slices to
848/// reflect that some transitions now start in the new block NewB. They can no
849/// longer be in the same slice as the transitions that start in the old block.
850/// Its time complexity is O(1 + |out(NewB)|).
851/// \param RfnB the old block that has been refined (now the blue subblock)
852/// \param NewB the new block (the red subblock)
853/// \param postprocessing true iff the refinement happened during
854/// postprocessing. (Otherwise, the refinement should
855/// preserve the information about `FromRed()`).
856void part_trans_t::new_red_block_created(block_t* const RfnB,
857 block_t* const NewB, bool const postprocessing)
858{ assert(RfnB->constln()==NewB->constln()); assert(NewB->begin()==RfnB->end());
859 NewB->set_inert_begin_and_end(B_to_C.begin(), B_to_C.begin());
860 bool old_fromred_invalid = false;
861 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
862 unsigned const max_counter = check_complexity::log_n -
863 check_complexity::ilog2(NewB->size());
864 mCRL2complexity(NewB, add_work(check_complexity::
865 /* for all outgoing transitions of NewB */ Move_Blue_or_Red_to_a_new_block_states_3_29, max_counter), );
866 #endif
867 for(permutation_iter_t s_iter=NewB->begin(); NewB->end()!=s_iter; ++s_iter)
868 { // mCRL2complexity(*s_iter, ...) -- optimized to the above call
869 for (succ_iter_t succ_iter = (*s_iter)->succ_begin();
870 (*s_iter)->succ_end() != succ_iter; ++succ_iter)
871 { mCRL2complexity(succ_iter->B_to_C->pred,add_work(check_complexity::
872 Move_Blue_or_Red_to_a_new_block_succ_3_29, max_counter), );
873 /* Move the transition to a new slice: */ assert(succ.end()>succ_iter); assert(succ_iter->B_to_C->pred->succ==succ_iter);
874 B_to_C_iter_t const old_pos = succ_iter->B_to_C;
875 B_to_C_desc_iter_t const old_B_to_C_slice = old_pos->B_to_C_slice;
876 B_to_C_iter_t new_pos = old_B_to_C_slice->begin; assert(B_to_C.end() > old_pos); assert(old_pos->pred->succ->B_to_C == old_pos);
877 assert(B_to_C.end() > new_pos); assert(new_pos->pred->succ->B_to_C == new_pos);
878 B_to_C_desc_iter_t new_B_to_C_slice; assert(new_pos <= old_pos);
879 if (B_to_C.begin() == new_pos ||
880 new_pos[-1].pred->source->block != NewB ||
881 new_pos[-1].pred->succ->target->constln() !=
882 succ_iter->target->constln())
883 {
884 // create a new B_to_C-slice
885 // this can only happen when the first transition from
886 // *s_iter to a new constellation is handled.
887 if (!postprocessing ? !old_fromred_invalid &&
888 RfnB->to_constln.begin() == old_B_to_C_slice
889 : !old_B_to_C_slice->needs_postprocessing())
890 {
891 // During primary refinement (Line 2.23):
892 // The old B_to_C_slice is in the FromRed-position, i. e.
893 // it contains the transitions to SpC. So the new slice
894 // also contains the transitions to SpC.
895 // During postprocessing:
896 // The old_B_to_C_slice does not need postprocessing, so
897 // its corresponding new slice should be in a similar
898 // position near the beginning of the list of slices.
899 NewB->to_constln.emplace_front(new_pos, new_pos); // new_B_to_C_slice is not yet fully initialised, therefore
900 new_B_to_C_slice = NewB->to_constln.begin(); // the assertion fails:
901 // assert(new_B_to_C_slice->from_block() == NewB);
902 }
903 else
904 {
905 // During primary refinement (Line 2.23):
906 // The old_B_to_C_slice is not in the FromRed-position. The
907 // corresponding slice of NewB should be moved into a
908 // position that does not change a potential FromRed-slice
909 // there.
910 // During postprocessing:
911 // The old_B_to_C_slice needs postprocessing, so also the
912 // new_B_to_C_slice will need postprocessing.
913 NewB->to_constln.emplace_back(new_pos, new_pos);
914 new_B_to_C_slice = std::prev(NewB->to_constln.end());
915 }
916 #ifndef NDEBUG
917 new_B_to_C_slice->work_counter = old_B_to_C_slice->work_counter;
918 #endif
919 if (RfnB->inert_end() == old_B_to_C_slice->end)
920 {
921 /* this is the first transition from NewB to its own */ assert(NewB->inert_begin() == B_to_C.begin());
922 /* constellation. Adapt the pointers accordingly. */ assert(NewB->inert_end() == B_to_C.begin());
923 NewB->set_inert_end(new_pos);
924 NewB->set_inert_begin(new_pos);
925 }
926 }
927 else
928 {
929 // the slice before new_pos is already the correct one
930 new_B_to_C_slice = new_pos[-1].B_to_C_slice;
931 }
932 ++new_B_to_C_slice->end;
933 ++old_B_to_C_slice->begin; assert(new_B_to_C_slice->end == old_B_to_C_slice->begin);
934 if (RfnB->inert_end() == old_B_to_C_slice->end)
935 {
936 // The transition goes from NewB to the constellation of
937 // RfnB and NewB.
938 NewB->set_inert_end(NewB->inert_end() + 1);
939 if (RfnB->inert_begin() <= old_pos)
940 {
941 // The transition is inert and has to be moved over the
942 // non-inert transitions of RfnB.
943 // old_pos --> new_pos --> RfnB->inert_begin() --> old_pos
944 swap3_B_to_C(succ_iter, new_pos->pred->succ,
945 RfnB->inert_begin()->pred->succ);
946 RfnB->set_inert_begin(RfnB->inert_begin() + 1);
947 }
948 else
949 {
950 // The transition is non-inert, but it has to be moved
951 // over the inert transitions of NewB.
952 new_pos = NewB->inert_begin();
953 NewB->set_inert_begin(NewB->inert_begin() + 1);
954 // old_pos --> new_pos --> NewB->inert_end() - 1 -> old_pos
955 swap3_B_to_C(succ_iter, new_pos->pred->succ,
956 NewB->inert_end()[-1].pred->succ);
957 }
958 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
959 {
960 // This was the last transition from RfnB to its own
961 // constellation.
962 RfnB->set_inert_begin(B_to_C.begin());
963 RfnB->set_inert_end(B_to_C.begin());
964
965 if (!old_fromred_invalid &&
966 RfnB->to_constln.begin() == old_B_to_C_slice)
967 {
968 old_fromred_invalid = true;
969 }
970 RfnB->to_constln.erase(old_B_to_C_slice);
971 }
972 }
973 else
974 {
975 // The transition goes from NewB to a constellation that
976 // does not contain RfnB or NewB. No special treatment is
977 // required.
978 swap_B_to_C(succ_iter, new_pos->pred->succ);
979 if (old_B_to_C_slice->begin == old_B_to_C_slice->end)
980 {
981 if (!old_fromred_invalid &&
982 RfnB->to_constln.begin() == old_B_to_C_slice)
983 {
984 old_fromred_invalid = true;
985 }
986 RfnB->to_constln.erase(old_B_to_C_slice);
987 }
988 }
989 new_pos->B_to_C_slice = new_B_to_C_slice;
990 }
991 }
992 #ifndef NDEBUG
993 if (RfnB->inert_begin() == RfnB->inert_end() &&
994 RfnB->inert_end() != B_to_C.begin() &&
995 (RfnB->inert_end()[-1].pred->source->block != RfnB ||
996 RfnB->inert_end()[-1].pred->succ->target->constln()
997 != RfnB->constln()))
998 {
999 assert(0 && "The old block has no transitions to its own "
1000 "constellation, but its inert_begin and "
1001 "inert_end pointers are not set to B_to_C.begin()");
1002 }
1003 if (RfnB->inert_end() != B_to_C.begin())
1004 {
1005 assert(RfnB->inert_end()[-1].pred->source->block == RfnB);
1006 assert(RfnB->inert_end()[-1].pred->succ->target->constln() ==
1007 RfnB->constln());
1008 }
1009 if (NewB->inert_begin() == NewB->inert_end() &&
1010 NewB->inert_end() != B_to_C.begin() &&
1011 (NewB->inert_end()[-1].pred->source->block != NewB ||
1012 NewB->inert_end()[-1].pred->succ->target->constln()
1013 != NewB->constln()))
1014 {
1015 assert(0 && "The new block has no transitions to its own "
1016 "constellation, but its inert_begin and "
1017 "inert_end pointers are not set to B_to_C.begin()");
1018 }
1019 if (NewB->inert_end() != B_to_C.begin())
1020 {
1021 assert(NewB->inert_end()[-1].pred->source->block == NewB);
1022 assert(NewB->inert_end()[-1].pred->succ->target->constln() ==
1023 NewB->constln());
1024 }
1025 #endif
1026}
1027 #ifndef NDEBUG
1028 /// \brief assert that the data structure is consistent and stable
1029 /// \details The data structure is tested against a large number of
1030 /// assertions to ensure that everything is consistent, e. g. pointers that
1031 /// should point to successors of state s actually point to a transition
1032 /// that starts in s.
1033 ///
1034 /// Additionally, it is asserted that the partition is stable. i. e. every
1035 /// bottom state in every block can reach exactly the constellations in the
1036 /// list of constellations that should be reachable from it, and every
1037 /// nonbottom state can reach a subset of them.
1038 void part_trans_t::assert_stability(const part_state_t& part_st) const
1039 {
1040 #ifdef MCRL2_GJKW_PARANOID_CHECK
1041 std::vector<state_info_const_ptr> part_st_predecessors;
1042 #endif
1043 // count the nontrivial constellations (to check later whether every
1044 // nontrivial constellation is reachable from the first nontrivial
1045 // constellation)
1046 state_type nr_of_nontrivial_constellations = 0;
1047 const constln_t* C = constln_t::get_some_nontrivial();
1048 if (nullptr != C)
1049 {
1050 for (;;)
1051 {
1052 ++nr_of_nontrivial_constellations;
1053 if (C->get_nontrivial_next()
1054 == C)
1055 {
1056 break;
1057 }
1058 C = C->get_nontrivial_next();
1059 assert(nullptr != C);
1060 }
1061 }
1062
1063 // for all constellations C do
1064 C = part_st.permutation.front()->constln();
1065 assert(C->begin() == part_st.permutation.begin());
1066 for (;;)
1067 {
1068 // assert some properties of constellation C
1069 assert(C->begin() < C->end());
1070 assert(C->postprocess_begin == C->postprocess_end);
1071 unsigned const max_C = check_complexity::log_n -
1072 check_complexity::ilog2(C->size());
1073 const block_t* B = (*C->begin())->block;
1074 assert(C->begin() == B->begin());
1075 if (C->is_trivial())
1076 {
1077 // a trivial constellation contains exactly one block
1078 assert(B->end() == C->end());
1079 }
1080 else
1081 {
1082 // a nontrivial constellation contains at least two blocks
1083 assert(B->end() < C->end());
1084 --nr_of_nontrivial_constellations;
1085 }
1086 // for all blocks B in C do
1087 for (;;)
1088 {
1089 // assert some properties of block B
1090 assert(B->constln() == C);
1091 assert(B->nonbottom_begin() <= B->nonbottom_end());
1092 assert(B->marked_nonbottom_begin()==B->marked_nonbottom_end());
1093 assert(B->bottom_begin() < B->bottom_end());
1094 assert(B->marked_bottom_begin() == B->marked_bottom_end());
1095 assert(!B->is_refinable());
1096 assert(B->inert_begin() <= B->inert_end());
1097 unsigned const max_B = check_complexity::log_n -
1098 check_complexity::ilog2(B->size());
1099 mCRL2complexity(B, no_temporary_work(max_C, max_B), );
1100 // count inert transitions in block
1101 state_type nr_of_inert_successors =
1102 B->inert_end()-B->inert_begin();
1103 permutation_const_iter_t s_iter;
1104 #ifdef MCRL2_GJKW_PARANOID_CHECK
1105 state_type nr_of_inert_predecessors=nr_of_inert_successors;
1106 // make sure that every non-bottom state can reach some
1107 // bottom state in the block. This is done using
1108 // a simple graph algorithm for reachability. The
1109 // algorithm should mark every source of an inert
1110 // transition exactly once. For this, we misuse the field
1111 // state_info_entry::notblue: It is == STATE_TYPE_MAX if
1112 // and only if the state has been marked.
1113
1114 // Because we run through the bottom states and their
1115 // predecessor transitions anyway, we also verify a few
1116 // other properties, in particular everything we want to
1117 // verify about inert predecessor transitions.
1118
1119 // for all bottom states s in B do
1120 assert(part_st_predecessors.empty());
1121 part_st_predecessors.reserve(B->nonbottom_end() -
1122 B->nonbottom_begin());
1123 s_iter = B->bottom_begin();
1124 do
1125 {
1126 state_info_const_ptr const s = *s_iter;
1127 nr_of_inert_predecessors -=
1128 s->inert_pred_end() - s->inert_pred_begin();
1129 // for all inert predecessors pred of s do
1130 for (pred_const_iter_t pred_iter=s->inert_pred_begin();
1131 pred_iter < s->inert_pred_end(); ++pred_iter)
1132 {
1133 // assert some properties of the predecessor
1134 // transition
1135 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1136 from_block() == B);
1137 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1138 to_constln() == C);
1139 assert(pred_iter->succ->target == s);
1140
1141 state_info_const_ptr const pred=pred_iter->source;
1142 // if pred is not yet marked as predecessor then
1143 if (STATE_TYPE_MAX != pred->notblue)
1144 {
1145 // assert some properties of the predecessor
1146 // state
1147 assert(pred->block == B);
1148 assert(pred->pos < B->nonbottom_end());
1149 // mark pred as predecessor
1150 const_cast<state_type&>(pred->notblue) =
1151 STATE_TYPE_MAX;
1152 // add pred to the list of predecessors
1153 part_st_predecessors.push_back(pred);
1154 // end if
1155 }
1156 // end for
1157 }
1158 // end for
1159 }
1160 while(++s_iter < B->bottom_end());
1161
1162 // Now that we have collected the predecessors of the
1163 // bottom states, we have to extend this set to their
1164 // indirect predecessors.
1165
1166 // for all states s in the list of predecessors do
1167 for (std::vector<state_info_const_ptr>::iterator s_iter =
1168 part_st_predecessors.begin();
1169 s_iter < part_st_predecessors.end(); ++s_iter)
1170 {
1171 state_info_const_ptr const s = *s_iter;
1172 nr_of_inert_predecessors -=
1173 s->inert_pred_end() - s->inert_pred_begin();
1174 // for all inert predecessors pred of s do
1175 for (pred_const_iter_t pred_iter=s->inert_pred_begin();
1176 pred_iter < s->inert_pred_end(); ++pred_iter)
1177 {
1178 // assert some properties of the predecessor
1179 // transition
1180 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1181 from_block() == B);
1182 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1183 to_constln() == C);
1184 assert(pred_iter->succ->target == s);
1185
1186 state_info_const_ptr const pred=pred_iter->source;
1187 // if pred is not yet marked as predecessor then
1188 if (STATE_TYPE_MAX != pred->notblue)
1189 {
1190 // assert some properties of the predecessor
1191 // state
1192 assert(pred->block == B);
1193 assert(pred->pos < B->nonbottom_end());
1194 // mark pred as predecessor
1195 const_cast<state_type&>(pred->notblue) =
1196 STATE_TYPE_MAX;
1197 // add pred to the list of predecessors
1198 part_st_predecessors.push_back(pred);
1199 // end if
1200 }
1201 // end for
1202 }
1203 // end for
1204 }
1205 assert(part_st_predecessors.size() == (std::size_t)
1206 (B->nonbottom_end() - B->nonbottom_begin()));
1207 part_st_predecessors.clear();
1208 assert(0 == nr_of_inert_predecessors);
1209 // now all nonbottom states should have
1210 // s->notblue == STATE_TYPE_MAX.
1211 #endif
1212 // verify to_constln list:
1213 bool to_own_constln = false;
1214 for (B_to_C_desc_const_iter_t iter = B->to_constln.begin();
1215 B->to_constln.end() != iter; ++iter)
1216 {
1217 assert(iter->from_block() == B);
1218 mCRL2complexity(iter, no_temporary_work(
1219 check_complexity::log_n -
1220 check_complexity::ilog2(iter->to_constln()->size())), );
1221 if (iter->to_constln() == C)
1222 {
1223 assert(!to_own_constln);
1224 to_own_constln = true;
1225 assert(iter->begin <= B->inert_begin());
1226 assert(iter->end == B->inert_end());
1227 }
1228 }
1229 if (!to_own_constln)
1230 {
1231 assert(B->nonbottom_begin() == B->nonbottom_end());
1232 assert(B->inert_begin() == B_to_C_begin());
1233 assert(B->inert_end() == B_to_C_begin());
1234 }
1235
1236 // for all states s in B do
1237 s_iter = B->begin();
1238 do
1239 {
1240 state_info_const_ptr const s = *s_iter;
1241 // assert some properties of state s
1242 assert(s->pos == s_iter);
1243 assert(s->block == B);
1244 assert(s->pred_begin() <= s->inert_pred_begin());
1245 assert(s->inert_pred_begin() <= s->inert_pred_end());
1246 assert(s->inert_pred_end() == s->pred_end());
1247 assert(s->succ_begin() <= s->inert_succ_begin());
1248 assert(s->inert_succ_begin() <= s->inert_succ_end());
1249 assert(s->inert_succ_end() <= s->succ_end());
1250 assert(s->succ_begin() == s->current_constln() ||
1251 s->succ_end() == s->current_constln() ||
1252 *s->current_constln()[-1].target->constln() <
1253 *s->current_constln()->target->constln());
1254 mCRL2complexity(s, no_temporary_work(max_B,
1255 s_iter >= B->bottom_begin()), );
1256 // count reachable constellations
1257 state_type nr_of_reachable_constlns = B->to_constln.size();
1258
1259 // for all constln-slices of successors of s do
1260 if (succ_const_iter_t succ_iter = s->succ_begin();
1261 succ_iter < s->succ_end())
1262 {
1263 for (;;)
1264 {
1265 succ_const_iter_t before_end =
1266 succ_iter->slice_begin_or_before_end();
1267 succ_const_iter_t slice_end = before_end + 1;
1268 assert(succ_iter < slice_end);
1269 assert(before_end->slice_begin_or_before_end() ==
1270 succ_iter);
1271 const constln_t* const targetC =
1272 succ_iter->target->constln();
1273 // for all noninert transitions in the
1274 // constln-slice do
1275 if (targetC == C)
1276 {
1277 assert(s->inert_succ_end() == slice_end);
1278 slice_end = s->inert_succ_begin();
1279 }
1280 for (; succ_iter < slice_end; ++succ_iter)
1281 {
1282 // assert some properties of the successor
1283 // transition
1284 assert(succ_iter->target->block != B);
1285 assert(succ_iter->target->constln()==targetC);
1286 if (succ_iter != before_end)
1287 {
1288 assert(succ_iter->
1289 slice_begin_or_before_end()==before_end);
1290 }
1291 assert(succ_iter->B_to_C < B->inert_begin() ||
1292 B->inert_end() <= succ_iter->B_to_C);
1293 assert(succ_iter->B_to_C->B_to_C_slice->
1294 from_block() == B);
1295 assert(succ_iter->B_to_C->B_to_C_slice->
1296 to_constln() == targetC);
1297 assert(succ_iter->B_to_C->pred->succ ==
1298 succ_iter);
1299 assert(succ_iter->B_to_C->pred->source == s);
1300 mCRL2complexity(succ_iter->B_to_C->pred,
1301 no_temporary_work(max_B, check_complexity::
1302 log_n - check_complexity::ilog2(
1303 succ_iter->target->constln()->size()),
1304 check_complexity::log_n - check_complexity::
1305 ilog2(succ_iter->target->block->size()),
1306 s_iter >= B->bottom_begin()), );
1307 // end for
1308 }
1309 // if we have reached the inert transitions then
1310 if (targetC == C)
1311 {
1312 // for all inert transitions in the
1313 // constln-slice do
1314 for (slice_end = s->inert_succ_end();
1315 succ_iter < slice_end; ++succ_iter)
1316 {
1317 // assert some properties of inert
1318 // transitions
1319 assert(succ_iter->target->block == B);
1320 if (succ_iter != before_end)
1321 {
1322 assert(before_end == succ_iter->
1323 slice_begin_or_before_end());
1324 }
1325 assert(B->inert_begin() <=
1326 succ_iter->B_to_C);
1327 assert(succ_iter->B_to_C < B->inert_end());
1328 assert(succ_iter->B_to_C->B_to_C_slice->
1329 from_block() == B);
1330 assert(succ_iter->B_to_C->B_to_C_slice->
1331 to_constln() == targetC);
1332 assert(succ_iter->B_to_C->pred->succ ==
1333 succ_iter);
1334 assert(succ_iter->B_to_C->pred->source==s);
1335 mCRL2complexity(succ_iter->B_to_C->pred,
1336 no_temporary_work(max_B,
1337 max_C, max_B, false), );
1338 // end for
1339 }
1340 // end if
1341 }
1342 else
1343 {
1344 --nr_of_reachable_constlns;
1345 }
1346 // end for
1347 if (s->succ_end()
1348 <= succ_iter)
1349 {
1350 break;
1351 }
1352 assert(0 != nr_of_reachable_constlns);
1353 assert(*targetC < *succ_iter->target->constln());
1354 }
1355 }
1356 // if s is a nonbottom state then
1357 if (s_iter < B->bottom_begin())
1358 {
1359 assert(s->inert_succ_begin() < s->inert_succ_end());
1360 nr_of_inert_successors -=
1361 s->inert_succ_end() - s->inert_succ_begin();
1362 // the following assertion is necessary because s must
1363 // have a transition to its own constellation (namely
1364 // an inert one), but this constln_slice is not
1365 // counted.
1366 assert(0 != nr_of_reachable_constlns);
1367
1368 #ifdef MCRL2_GJKW_PARANOID_CHECK
1369 // assert that s can reach a bottom state
1370 assert(STATE_TYPE_MAX == s->notblue);
1371 const_cast<state_type&>(s->notblue) = 1;
1372 #endif
1373 }
1374 else
1375 {
1376 // (s is a bottom state.)
1377 // assert that not too few constellations are
1378 // reachable.
1379 assert((state_type) to_own_constln ==
1380 nr_of_reachable_constlns);
1381 assert(s->inert_succ_begin() == s->inert_succ_end());
1382 // the following assertions are necessary because it
1383 // could be that the state has no transition to its own
1384 // constellation.
1385 assert(s->succ_begin() == s->inert_succ_begin() ||
1386 *s->inert_succ_begin()[-1].target->constln() <= *C);
1387 assert(s->inert_succ_end() == s->succ_end() ||
1388 *s->inert_succ_end()->target->constln() > *C);
1389 }
1390
1391 // for all noninert predecessors of s do
1392 for (pred_const_iter_t pred_iter=s->noninert_pred_begin();
1393 pred_iter < s->noninert_pred_end(); ++pred_iter)
1394 {
1395 // assert some properties of the predecessor
1396 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1397 from_block() != B);
1398 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1399 to_constln() == C);
1400 assert(pred_iter->succ->target == s);
1401 assert(pred_iter->source->block != B);
1402 // end for
1403 }
1404 #ifndef MCRL2_GJKW_PARANOID_CHECK
1405 // for all inert predecessors of s do
1406 for (pred_const_iter_t pred_iter=s->inert_pred_begin();
1407 pred_iter < s->inert_pred_end(); ++pred_iter)
1408 {
1409 // assert some properties of the predecessor
1410 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1411 from_block() == B);
1412 assert(pred_iter->succ->B_to_C->B_to_C_slice->
1413 to_constln() == C);
1414 assert(pred_iter->succ->target == s);
1415 assert(pred_iter->source->block == B);
1416 assert(pred_iter->source->pos<B->nonbottom_end());
1417 // end for
1418 }
1419 #endif
1420 // end for (all states s in B)
1421 }
1422 while (++s_iter < B->end());
1423 assert(0 == nr_of_inert_successors);
1424 // end for (all blocks B in C)
1425 /* *************************************************************************
1426 */
1427 if (B->end()
1428 == C->end())
1429 {
1430 break;
1431 }
1432/* */ assert(B->end() < C->end());
1433/* A L G O R I T H M S */ assert(B->end() == (*B->end())->block->begin());
1434/* */ B = (*B->end())->block;
1435/* ************************************************************************* */ }
1436 // end for (all constellations C)
1437 if (C->end()
1438 == part_st.permutation
1439 .end())
1440 {
1441 break;
1442 }
1443 assert(C->end() < part_st.permutation.end());
1444 assert(C->end() == (*C->end())->constln()->begin());
1445 C = (*C->end())->constln();
1446/*===========================================================================*/ }
1447/* initialisation helper */ assert(0 == nr_of_nontrivial_constellations);
1448/*===========================================================================*/ return;
1449 }
1450 #endif
1451/// \brief constructor of the helper class
1452template<class LTS_TYPE>
1453bisim_partitioner_gjkw_initialise_helper<LTS_TYPE>::
1454bisim_partitioner_gjkw_initialise_helper(LTS_TYPE& l, bool const branching,
1455 bool const preserve_divergence)
1456 : aut(l),
1457 nr_of_states(l.num_states()),
1458 orig_nr_of_states(l.num_states()),
1459 nr_of_transitions(l.num_transitions()),
1460 noninert_out_per_state(l.num_states(), 0),
1461 inert_out_per_state(l.num_states(), 0),
1462 noninert_in_per_state(l.num_states(), 0),
1463 inert_in_per_state(l.num_states(), 0),
1464 noninert_out_per_block(1, 0),
1465 inert_out_per_block(1, 0),
1466 states_per_block(1, l.num_states())
1467{
1468
1469 mCRL2log(log::log_level_t::verbose) << "O(m log n) "
1470 << (preserve_divergence ? "Divergence preserving b" : "B")
1471 << (branching ? "ranching b" : "")
1472 << "isimulation partitioner created for " << l.num_states()
1473 << " states and " << l.num_transitions()
1474 << " transitions [GJKW 2017]\n";
1475 // Iterate over the transitions and collect new states
1476 for (const transition& t: aut.get_transitions())
1477 {
1478 if (!branching || !aut.is_tau(aut.apply_hidden_label_map(t.label())) ||
1479 (preserve_divergence && t.from() == t.to()))
1480 {
1481 // (possibly) create new state
1482 Key const k(aut.apply_hidden_label_map(t.label()), t.to());
1483 std::pair<typename std::unordered_map<Key, state_type,
1484 KeyHasher>::iterator,bool> extra_state = extra_kripke_states.
1485 insert(std::make_pair(k, nr_of_states));
1486 if (extra_state.second)
1487 {
1488 noninert_in_per_state.push_back(0);
1489 inert_in_per_state.push_back(0);
1490 noninert_out_per_state.push_back(0);
1491 inert_out_per_state.push_back(0);
1492
1493 // (possibly) create new block
1494 std::pair<std::unordered_map<label_type, state_type>::iterator,
1495 bool> const action_block = action_block_map.insert(
1496 std::make_pair(aut.apply_hidden_label_map(t.label()),
1497 states_per_block.size()));
1498 if (action_block.second)
1499 {
1500 noninert_out_per_block.push_back(0);
1501 inert_out_per_block.push_back(0);
1502 states_per_block.push_back(0);
1503 }
1504
1505 ++noninert_in_per_state[t.to()];
1506 ++noninert_out_per_state[nr_of_states];
1507 ++noninert_out_per_block[action_block.first->second];
1508 ++states_per_block[action_block.first->second];
1509 ++nr_of_states;
1510 ++nr_of_transitions;
1511 }
1512 ++noninert_in_per_state[extra_state.first->second];
1513 ++noninert_out_per_state[t.from()];
1514 ++noninert_out_per_block[0];
1515 }
1516 else
1517 {
1518 ++inert_in_per_state[t.to()];
1519 if (1 == ++inert_out_per_state[t.from()])
1520 {
1521 // this is the first inert outgoing transition of t.from()
1522 ++nr_of_nonbottom_states;
1523 }
1524 ++inert_out_per_block[0];
1525 }
1526 }
1527 mCRL2log(log::log_level_t::verbose) << "Number of extra states: "
1528 << extra_kripke_states.size() << "\n";
1529 #ifndef NDEBUG
1530 check_complexity::init(nr_of_states);
1531 #endif
1532}
1533
1534
1535/// \brief initialise the state in part_st and the transitions in part_tr
1536template<class LTS_TYPE>
1537inline void bisim_partitioner_gjkw_initialise_helper<LTS_TYPE>::
1538init_transitions(part_state_t& part_st, part_trans_t& part_tr,
1539 bool const branching, bool const preserve_divergence)
1540{ assert(part_st.state_size() == get_nr_of_states());
1541 assert(part_tr.trans_size() == get_nr_of_transitions());
1542 // initialise blocks and B_to_C slices
1543 permutation_iter_t begin = part_st.permutation.begin();
1544 constln_t* const constln = new constln_t(get_nr_of_states(), begin,
1545 part_st.permutation.end(), part_tr.B_to_C_end());
1546 if (1 < states_per_block.size())
1547 {
1548 constln->make_nontrivial();
1549 }
1550 std::vector<block_t*> blocks(states_per_block.size());
1551 B_to_C_iter_t B_to_C_begin = part_tr.B_to_C.begin();
1552 for (state_type B = 0; B < states_per_block.size(); ++B)
1553 {
1554 permutation_iter_t const end = begin + states_per_block[B];
1555 blocks[B] = new block_t(constln, begin, end);
1556 if (0 == noninert_out_per_block[B] && 0 == inert_out_per_block[B])
1557 {
1558 blocks[B]->set_inert_begin_and_end(part_tr.B_to_C.begin(),
1559 part_tr.B_to_C.begin()); assert(blocks[B]->to_constln.empty());
1560 }
1561 else
1562 {
1563 blocks[B]->set_inert_begin_and_end(B_to_C_begin +
1564 noninert_out_per_block[B],
1565 B_to_C_begin + noninert_out_per_block[B] +
1566 inert_out_per_block[B]);
1567 blocks[B]->to_constln.emplace_back(B_to_C_begin,
1568 blocks[B]->inert_end());
1569 B_to_C_desc_iter_t const slice =
1570 std::prev(blocks[B]->to_constln.end()); assert(B_to_C_begin < slice->end);
1571 for (; slice->end != B_to_C_begin; ++B_to_C_begin)
1572 {
1573 B_to_C_begin->B_to_C_slice = slice;
1574 }
1575 }
1576 begin = end;
1577 } assert(part_st.permutation.end() == begin);
1578 /* only block 0 has a sequence number and non-bottom states: */ assert(part_tr.B_to_C.end() == B_to_C_begin);
1579 blocks[0]->assign_seqnr();
1580 blocks[0]->set_bottom_begin(blocks[0]->begin() + nr_of_nonbottom_states);
1581 blocks[0]->set_marked_nonbottom_begin(blocks[0]->bottom_begin());
1582
1583 // initialise states and succ slices
1584 part_st.state_info.front().set_pred_begin(part_tr.pred.begin());
1585 part_st.state_info.front().set_succ_begin(part_tr.succ.begin());
1586 for (state_type s = 0; get_nr_of_states() != s; ++s)
1587 {
1588 part_st.state_info[s].set_pred_end(part_st.state_info[s].pred_begin() +
1589 noninert_in_per_state[s] + inert_in_per_state[s]);
1590 part_st.state_info[s].set_inert_pred_begin(part_st.state_info[s].
1591 pred_begin() + noninert_in_per_state[s]);
1592 // part_st.state_info[s+1].set_pred_begin(part_st.state_info[s].
1593 // pred_end());
1594
1595 succ_iter_t succ_iter = part_st.state_info[s].succ_begin();
1596 succ_iter_t succ_end = succ_iter +
1597 noninert_out_per_state[s] + inert_out_per_state[s];
1598 part_st.state_info[s].set_succ_end(succ_end);
1599 part_st.state_info[s].set_current_constln(succ_end);
1600 part_st.state_info[s].set_inert_succ_begin_and_end(part_st.
1601 state_info[s].succ_begin() + noninert_out_per_state[s], succ_end);
1602 if (succ_iter < succ_end)
1603 {
1604 --succ_end;
1605 for (; succ_iter < succ_end; ++succ_iter)
1606 {
1607 succ_iter->set_slice_begin_or_before_end(succ_end);
1608 } assert(succ_iter == succ_end);
1609 succ_end->set_slice_begin_or_before_end(
1610 part_st.state_info[s].succ_begin());
1611 }
1612 else
1613 {
1614 assert(succ_end == succ_iter);
1615 }
1616 if (s < aut.num_states())
1617 {
1618 // s is not an extra Kripke state. It is in block 0.
1619 part_st.state_info[s].block = blocks[0];
1620 if (0 != inert_out_per_state[s])
1621 {
1622 /* non-bottom state: */ assert(0 != nr_of_nonbottom_states);
1623 --nr_of_nonbottom_states;
1624 part_st.state_info[s].pos = blocks[0]->begin() +
1625 nr_of_nonbottom_states;
1626 }
1627 else
1628 { // The following assertion is incomplete; only the second
1629 // bottom state: // assertion (after the assignment) makes sure that not too
1630 // many states become part of this slice.
1631 assert(0 != states_per_block[0]);
1632 --states_per_block[0];
1633 part_st.state_info[s].pos = blocks[0]->begin() +
1634 states_per_block[0]; assert(part_st.state_info[s].pos >= blocks[0]->bottom_begin());
1635 }
1636 *part_st.state_info[s].pos = &part_st.state_info[s];
1637 // part_st.state_info[s].notblue = 0;
1638 }
1639 }
1640
1641 // initialise transitions (and finalise extra Kripke states)
1642 for (const transition& t: aut.get_transitions())
1643 {
1644 if (!branching || !aut.is_tau(aut.apply_hidden_label_map(t.label())) ||
1645 (preserve_divergence && t.from() == t.to()))
1646 {
1647 // take transition through an extra intermediary state
1648 Key const k(aut.apply_hidden_label_map(t.label()), t.to());
1649 state_type const extra_state = extra_kripke_states[k];
1650 if (0 != noninert_out_per_state[extra_state])
1651 {
1652 state_type const extra_block =
1653 action_block_map[aut.apply_hidden_label_map(t.label())];
1654 // now initialise extra_state correctly
1655 part_st.state_info[extra_state].block = blocks[extra_block]; assert(0 != states_per_block[extra_block]);
1656 --states_per_block[extra_block];
1657 part_st.state_info[extra_state].pos = blocks[extra_block]->
1658 begin() + states_per_block[extra_block];
1659 *part_st.state_info[extra_state].pos =
1660 &part_st.state_info[extra_state];
1661 // part_st.state_info[extra_state].notblue = 0;
1662
1663 // state extra_state has exactly one outgoing transition,
1664 // namely a noninert transition to to t.to(). It has to be
1665 /* initialised now. */ assert(0 != noninert_in_per_state[t.to()]);
1666 --noninert_in_per_state[t.to()];
1667 pred_iter_t const t_pred =
1668 part_st.state_info[t.to()].noninert_pred_begin() +
1669 noninert_in_per_state[t.to()];
1670 --noninert_out_per_state[extra_state]; assert(0 == noninert_out_per_state[extra_state]);
1671 succ_iter_t const t_succ =
1672 part_st.state_info[extra_state].succ_begin(); assert(0 != noninert_out_per_block[extra_block]);
1673 B_to_C_iter_t const t_B_to_C =
1674 blocks[extra_block]->inert_begin() -
1675 noninert_out_per_block[extra_block]--;
1676 t_pred->source = &part_st.state_info[extra_state];
1677 t_pred->succ = t_succ;
1678 t_succ->target = &part_st.state_info[t.to()];
1679 t_succ->B_to_C = t_B_to_C;
1680 // t_B_to_C->B_to_C_slice = (already initialised);
1681 t_B_to_C->pred = t_pred;
1682 }
1683 /* noninert transition from t.from() to extra_state */ assert(0 != noninert_in_per_state[extra_state]);
1684 --noninert_in_per_state[extra_state];
1685 pred_iter_t const t_pred =
1686 part_st.state_info[extra_state].noninert_pred_begin() +
1687 noninert_in_per_state[extra_state]; assert(0 != noninert_out_per_state[t.from()]);
1688 --noninert_out_per_state[t.from()];
1689 succ_iter_t const t_succ=part_st.state_info[t.from()].succ_begin()+
1690 noninert_out_per_state[t.from()]; assert(0 != noninert_out_per_block[0]);
1691 B_to_C_iter_t const t_B_to_C = blocks[0]->inert_begin() -
1692 noninert_out_per_block[0]--;
1693
1694 t_pred->source = &part_st.state_info[t.from()];
1695 t_pred->succ = t_succ;
1696 t_succ->target = &part_st.state_info[extra_state];
1697 t_succ->B_to_C = t_B_to_C;
1698 // t_B_to_C->B_to_C_slice = (already initialised);
1699 t_B_to_C->pred = t_pred;
1700 }
1701 else
1702 {
1703 /* inert transition from t.from() to t.to() */ assert(0 != inert_in_per_state[t.to()]);
1704 --inert_in_per_state[t.to()];
1705 pred_iter_t const t_pred =
1706 part_st.state_info[t.to()].inert_pred_begin() +
1707 inert_in_per_state[t.to()]; assert(0 != inert_out_per_state[t.from()]);
1708 --inert_out_per_state[t.from()];
1709 succ_iter_t const t_succ =
1710 part_st.state_info[t.from()].inert_succ_begin() +
1711 inert_out_per_state[t.from()]; assert(0 != inert_out_per_block[0]);
1712 --inert_out_per_block[0];
1713 B_to_C_iter_t const t_B_to_C = blocks[0]->inert_begin() +
1714 inert_out_per_block[0];
1715
1716 t_pred->source = &part_st.state_info[t.from()];
1717 t_pred->succ = t_succ;
1718 t_succ->target = &part_st.state_info[t.to()];
1719 t_succ->B_to_C = t_B_to_C;
1720 // t_B_to_C->B_to_C_slice = (already initialised);
1721 t_B_to_C->pred = t_pred;
1722 }
1723 }
1724 noninert_out_per_state.clear(); inert_out_per_state.clear();
1725 noninert_in_per_state.clear(); inert_in_per_state.clear();
1726 noninert_out_per_block.clear(); inert_out_per_block.clear();
1727 states_per_block.clear();
1728
1729 aut.clear_transitions();
1730
1731 mCRL2log(log::log_level_t::verbose) << "Size of the resulting Kripke structure: "
1732 << get_nr_of_states() << " states and "
1733 << get_nr_of_transitions() << " transitions.\n";
1734}
1735
1736/// \brief Replaces the transition relation of the current LTS by the
1737/// transitions of the bisimulation-reduced transition system.
1738/// \details Each transition (s, l, s') is replaced by a transition (t, l, t'),
1739/// where t and t' are the equivalence classes of s and s', respectively. If
1740/// the label l is internal, then the transition is only added if t != t' or
1741/// preserve_divergence == true. This effectively removes all inert
1742/// transitions. Duplicates are removed from the transitions in the new LTS.
1743///
1744/// Note that the number of states nor the initial state are not adapted by
1745/// this method. These must be set separately.
1746///
1747/// The code is very much inspired by liblts_bisim_gw.h, which was written by
1748/// Anton Wijs.
1749///
1750/// \pre The bisimulation equivalence classes have been computed.
1751/// \note In debug mode, an additional parameter `branching` is available to
1752/// indicate that non-internal transitions should be removed.
1753template <class LTS_TYPE>
1754void bisim_partitioner_gjkw_initialise_helper<LTS_TYPE>::
1755 replace_transition_system(const part_state_t& part_st, ONLY_IF_DEBUG( const bool branching, )
1756 const bool preserve_divergence)
1757{
1758 std::unordered_map <state_type, Key> to_lts_map;
1759 // obtain a map from state to <action, state> pair from extra_kripke_states
1760 for (typename std::unordered_map<Key, state_type, KeyHasher>::iterator it =
1761 extra_kripke_states.begin(); it != extra_kripke_states.end(); ++it)
1762 {
1763 to_lts_map.insert(std::make_pair(it->second, it->first));
1764 }
1765 extra_kripke_states.clear();
1766
1767 label_type const tau_label = aut.tau_label_index();
1768 // In the following loop, we visit a bottom state of each block and take
1769 // its transitions. As the partition is (assumed to be) stable, in this
1770 // way we visit each transition of a lumped state exactly once.
1771 for (permutation_const_iter_t s_iter = part_st.permutation.begin();
1772 part_st.permutation.end() != s_iter; ++s_iter)
1773 {
1774 block_t *B = (*s_iter)->block;
1775 // forward to last state of block, i. e. to a bottom state:
1776 s_iter = B->end() - 1; assert(B->bottom_end() > s_iter); assert(B->bottom_begin() <= s_iter);
1777 assert(B->end() == B->constln()->end());
1778 state_type const s_eq = B->seqnr();
1779 if (block_t::BLOCK_NO_SEQNR == s_eq)
1780 {
1781 break;
1782 }
1783
1784 for (succ_const_iter_t succ_iter = (*s_iter)->succ_begin();
1785 (*s_iter)->succ_end() != succ_iter; )
1786 {
1787 if (state_type t_eq = succ_iter->target->block->seqnr();
1788 block_t::BLOCK_NO_SEQNR != t_eq)
1789 { assert(branching);
1790 // We have a transition that originally was inert.
1791 if (s_eq == t_eq)
1792 {
1793 // The transition is still inert.
1794 if (!preserve_divergence)
1795 {
1796 // As we do not preserve divergence, we do not add it.
1797 // Nor will we add other transitions to the same
1798 // constellation.
1799 succ_iter = succ_entry::slice_end(succ_iter);
1800 continue;
1801 }
1802 if (*s_iter != succ_iter->target)
1803 {
1804 // The transition was not a self-loop to start with.
1805 // So we do not add it either.
1806 ++succ_iter;
1807 continue;
1808 }
1809 } assert(std::cmp_not_equal(-1, tau_label));
1810 aut.add_transition(transition(s_eq, tau_label, t_eq));
1811 }
1812 else
1813 {
1814 state_type const tgt_id = succ_iter->target -
1815 &part_st.state_info.front();
1816 // We have a non-inert transition to an intermediary state.
1817 // Look up the label and where the transition from the
1818 // intermediary state goes.
1819 Key const k = to_lts_map.find(tgt_id)->second;
1820 t_eq = part_st.state_info[k.second].block->seqnr(); assert(block_t::BLOCK_NO_SEQNR != t_eq);
1821 aut.add_transition(transition(s_eq, k.first, t_eq)); // The target state could also be found through the pointer
1822 // structure (but we also need the labels, which are not stored
1823 // in the refinable partition):
1824 assert(&part_st.state_info[k.second]==succ_iter->target->succ_begin()->target);
1825 assert(1 == succ_iter->target->succ_end() - succ_iter->target->succ_begin());
1826 }
1827 // Skip over other transitions from the same state to the same
1828 // constellation -- they would be mapped to the same resulting
1829 // transition.
1830 succ_iter = succ_entry::slice_end(succ_iter);
1831 }
1832 }
1833
1834 // Merge the states, by setting the state labels of each state to the concatenation of the state labels of its
1835 // equivalence class.
1836
1837 if (aut.has_state_info()) /* If there are no state labels this step can be ignored */
1838 {
1839 /* Create a vector for the new labels */
1840 std::vector<typename LTS_TYPE::state_label_t> new_labels(block_t::nr_of_blocks);
1841
1842 for(std::size_t i=aut.num_states(); i>0; )
1843 {
1844 --i;
1845 const std::size_t new_index=part_st.block(i)->seqnr(); /* get_eq_class(i) */
1846 new_labels[new_index] = new_labels[new_index] + aut.state_label(i);
1847 }
1848
1849 aut.set_num_states(block_t::nr_of_blocks);
1850 for(std::size_t i=0; i<block_t::nr_of_blocks; ++i)
1851 {
1852 aut.set_state_label(i,new_labels[i]);
1853 }
1854 }
1855 else
1856 {
1857 aut.set_num_states(block_t::nr_of_blocks);
1858 }
1859
1860 aut.set_initial_state(part_st.block(aut.initial_state())->seqnr());
1861}
1862
1863} // end namespace bisim_gjkw
1864
1865
1866
1867/*=============================================================================
1868= dbStutteringEquivalence -- Algorithm 2 in [GJKW 2017] =
1869=============================================================================*/
1870
1871
1872
1873template <class LTS_TYPE>
1874void bisim_partitioner_gjkw<LTS_TYPE>::create_initial_partition_gjkw(
1875 bool const branching, bool const preserve_divergence)
1876{
1877 // 2.2: P := P_0, i. e. the initial, cycle-free partition; C = {S}
1878 // and
1879 // 2.3: Initialise all temporary data
1880 init_helper.init_transitions(part_st, part_tr, branching,
1881 preserve_divergence);
1882}
1883
1884
1885template <class LTS_TYPE>
1886void bisim_partitioner_gjkw<LTS_TYPE>::
1887 refine_partition_until_it_becomes_stable_gjkw()
1888{
1889 #ifndef NDEBUG
1890 if (mCRL2logEnabled(log::log_level_t::debug))
1891 {
1892 part_st.print_part(part_tr);
1893 part_st.print_trans();
1894 }
1895
1896 part_tr.assert_stability(part_st);
1897 #endif
1898 // 2.4: while C contains a nontrivial constellation SpC do
1899 while (nullptr != bisim_gjkw::constln_t::get_some_nontrivial())
1900 { // check_complexity::add_work is called below, after SpB has been found
1901 bisim_gjkw::constln_t* const SpC =
1902 bisim_gjkw::constln_t::get_some_nontrivial();
1903 // 2.5: Choose a small splitter block SpB subset of SpC from P,
1904 // i.e. |SpB| <= 1/2*|SpC|
1905 // and
1906 // 2.6: Create a new constellation NewC and move SpB from SpC to NewC
1907 // and
1908 // 2.7: C := partition C where SpB is removed from SpC and NewC is
1909 // added
1910 bisim_gjkw::block_t* const SpB = SpC->split_off_small_block();
1911 bisim_gjkw::constln_t* const NewC = SpB->constln();
1912 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
1913 unsigned const max_counter = check_complexity::log_n -
1914 /*-------------------- find predecessors of SpB ---------------------*/ check_complexity::ilog2(SpB->size());
1915 #endif
1916 /* 2.8: Mark block SpB as refinable */ mCRL2complexity(SpB, add_work(check_complexity::
1917 /* 2.9: Mark all states of SpB as predecessors */ while_C_contains_a_nontrivial_constellation_2_4, max_counter), );
1918 /* we deviate from the published algorithm: only states with a */ assert(nullptr == bisim_gjkw::block_t::get_some_refinable());
1919 // transition to SpC will be marked. SpB will be split separately.
1920 // 2.17: Register that the transitions from s to inert_out(s) go to
1921 // NewC (instead of SpC)
1922 // (Before we enter the loop, we already adapt the ``B_to_C''
1923 // transition array.)
1924 part_tr.split_inert_to_C(SpB);
1925 // 2.10: for all s in SpB do
1926 /* We have to walk through the states from end to beginning so */ mCRL2complexity(SpB,
1927 /* we can mark state s if necessary. Marking will move s to a */ add_work(check_complexity::for_all_s_in_SpB_2_10, max_counter), );
1928 // position that has already been visited.
1929 for (bisim_gjkw::permutation_iter_t s_iter = SpB->end();
1930 SpB->begin() != s_iter; )
1931 {
1932 --s_iter;
1933 bisim_gjkw::state_info_ptr const s = *s_iter; // mCRL2complexity(s, ...) -- optimized to the above call.
1934 // 2.11: for all s_prime in noninert_in(s) do
1935 for (bisim_gjkw::pred_iter_t pred_iter = s->noninert_pred_begin();
1936 s->noninert_pred_end() != pred_iter; ++pred_iter)
1937 { mCRL2complexity(pred_iter, add_work(
1938 check_complexity::for_all_s_prime_in_pred_s_2_11, max_counter), );
1939 assert(part_tr.pred_end() > pred_iter);
1940 assert(pred_iter->succ->B_to_C->pred == pred_iter);
1941 bisim_gjkw::state_info_ptr const s_prime = pred_iter->source;
1942 // 2.12: Mark the block of s_prime as refinable
1943 bool const first_transition_of_block =
1944 s_prime->block->make_refinable();
1945 // 2.13: Mark s_prime as predecessor of SpB
1946 bool const first_transition_of_state =
1947 s_prime->block->mark(s_prime);
1948 // 2.14: Register that s_prime->s goes to NewC (instead of SpC)
1949 // and
1950 // 2.15: Store whether s' still has some transition to SpC\SpB
1951 s_prime->set_current_constln(part_tr.change_to_C(pred_iter, ONLY_IF_DEBUG( SpC, NewC, )
1952 first_transition_of_state, first_transition_of_block));
1953 // 2.16: end for
1954 }
1955 // 2.17: Register that the transitions from s to inert_out(s) go to
1956 // NewC (instead of SpC)
1957 // (Here, we only adapt the ``succ'' transition array.)
1958 if (part_tr.split_s_inert_out(s ONLY_IF_DEBUG( , SpC )
1959 ))
1960 {
1961 // 2.18: Store whether s still has some transition to SpC\SpB
1962 // we deviate from the explanation of the published
1963 // algorithm: we store this information by marking states
1964 // with transitions to SpC.
1965 SpB->mark(s);
1966 }
1967 // 2.19: end for
1968 }
1969
1970 // second pass through the predecessors to correct the pointers to the
1971 // constln_slices
1972 for (auto s : *SpB)
1973 {
1974 for (bisim_gjkw::pred_iter_t pred_iter = s->noninert_pred_begin();
1975 s->noninert_pred_end() != pred_iter; ++pred_iter)
1976 {
1977 bisim_gjkw::succ_iter_t succ = pred_iter->succ;
1978 bisim_gjkw::succ_iter_t before_end =
1979 pred_iter->source->current_constln() - 1;
1980 if (succ != before_end)
1981 { assert(succ<before_end); assert(succ>=before_end->slice_begin_or_before_end());
1982 assert(succ->slice_begin_or_before_end() ==
1983 before_end->slice_begin_or_before_end());
1984 succ->set_slice_begin_or_before_end(before_end);
1985 }
1986 }
1987 }
1988 #ifndef NDEBUG
1989 // The following tests cannot be executed during the above loops
1990 // because a state s_prime may have multiple transitions to SpB.
1991 for (auto s : *SpB)
1992 {
1993 for (bisim_gjkw::pred_const_iter_t pred_iter=s->noninert_pred_begin();
1994 s->noninert_pred_end() != pred_iter; ++pred_iter)
1995 {
1996 bisim_gjkw::state_info_const_ptr const s_prime = pred_iter->source;
1997 // check consistency of s_prime->current_constln()
1998 assert(s_prime->succ_begin() == s_prime->current_constln() ||
1999 *s_prime->current_constln()[-1].target->constln() <= *SpC);
2000 assert(s_prime->succ_end() == s_prime->current_constln() ||
2001 *SpC <= *s_prime->current_constln()->target->constln());
2002 // s_prime must have a transition to the new constellation
2003 assert(s_prime->succ_begin() < s_prime->current_constln());
2004 assert(s_prime->current_constln()[-1].target->constln() == NewC);
2005 // check consistency of s_prime->inert_succ_begin() and
2006 // s_prime->inert_succ_end()
2007 assert(s_prime->succ_begin() == s_prime->inert_succ_begin() ||
2008 *s_prime->inert_succ_begin()[-1].target->constln() <=
2009 *s_prime->constln());
2010 assert(s_prime->succ_begin() == s_prime->inert_succ_begin() ||
2011 s_prime->inert_succ_begin()[-1].target->block !=
2012 s_prime->block);
2013 assert(s_prime->inert_succ_begin()==s_prime->inert_succ_end()||
2014 (s_prime->inert_succ_begin()->target->block ==
2015 s_prime->block &&
2016 s_prime->inert_succ_end()[-1].target->block ==
2017 s_prime->block));
2018 assert(s_prime->succ_end() == s_prime->inert_succ_end() ||
2019 *s_prime->constln() <
2020 *s_prime->inert_succ_end()->target->constln());
2021 }
2022 // check consistency of s->inert_succ_begin() and
2023 // s->inert_succ_end()
2024 assert(s->succ_begin() == s->inert_succ_begin() ||
2025 *s->inert_succ_begin()[-1].target->constln() < *s->constln());
2026 assert(s->inert_succ_begin() == s->inert_succ_end() ||
2027 /*------------------ stabilise the partition again ------------------*/ (s->inert_succ_begin()->target->block == s->block &&
2028 s->inert_succ_end()[-1].target->block == s->block));
2029 /* deviation from the published algorithm: we first refine the */ assert(s->succ_end() == s->inert_succ_end() ||
2030 /* splitter according to the marking of states (marked states have a */ *s->constln() < *s->inert_succ_end()->target->constln());
2031 /* transition to SpC). */ }
2032 #endif // ifndef NDEBUG
2033 if (0 != SpB->marked_size())
2034 {
2035 if (1 == SpB->size())
2036 {
2037 // if the block only contains a single state, the refinement
2038 // would be trivial anyway (and it cannot find new bottom
2039 // states).
2040 SpB->set_marked_bottom_begin(SpB->bottom_end());
2041 }
2042 else
2043 {
2044 bisim_gjkw::block_t* RedB = refine(SpB, SpC, nullptr, false);
2045 if (0 != RedB->unmarked_bottom_size())
2046 {
2047 postprocess_new_bottom(RedB);
2048 }
2049 else
2050 {
2051 RedB->set_marked_bottom_begin(RedB->bottom_end());
2052 }
2053 }
2054 }
2055
2056 // 2.20: for all refinable blocks RfnB do
2057 while (nullptr != bisim_gjkw::block_t::get_some_refinable())
2058 {
2059 bisim_gjkw::block_t* const RfnB =
2060 bisim_gjkw::block_t::get_some_refinable();
2061 // 2.21: Mark block RfnB as non-refinable
2062 RfnB->make_nonrefinable();
2063 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2064 // The work in this loop has to be assigned to the B_to_C-
2065 // slice that contains the transitions from RfnB to NewC.
2066 // Note that this is not FromRed, so we have to find it in a
2067 // different way. First find a marked state:
2068 bisim_gjkw::permutation_iter_t s_mark_iter = RfnB->marked_bottom_begin();
2069 if (s_mark_iter == RfnB->marked_bottom_end())
2070 {
2071 s_mark_iter = RfnB->marked_nonbottom_begin();
2072 assert(s_mark_iter < RfnB->marked_nonbottom_end());
2073 }
2074 // Now, using the current_constln pointer of s, find a
2075 // transition to NewC.
2076 bisim_gjkw::succ_iter_t to_NewC =
2077 std::prev((*s_mark_iter)->current_constln());
2078 assert((*s_mark_iter)->succ_begin() <= to_NewC);
2079 assert(to_NewC->target->constln() == NewC);
2080 mCRL2complexity(to_NewC->B_to_C->B_to_C_slice, add_work(
2081 check_complexity::for_all_refinable_blocks_RfnB_2_20, max_counter), );
2082 #endif
2083 if (1 == RfnB->size())
2084 {
2085 // if the block only contains a single state, the refinement
2086 // would be trivial anyway (and it cannot find new bottom
2087 // states).
2088 RfnB->set_marked_bottom_begin(RfnB->bottom_end());
2089 continue;
2090 }
2091 // 2.22: <RedB, BlueB> := Refine(RfnB, NewC, {marked states in
2092 // RfnB}, {})
2093 bisim_gjkw::block_t* RedB = refine(RfnB, NewC, nullptr, false);
2094 // 2.23: if RedB contains new bottom states then
2095 if (0 != RedB->unmarked_bottom_size())
2096 {
2097 // 2.24: RedB := PostprocessNewBottom(RedB, BlueB)
2098 RedB = postprocess_new_bottom(RedB);
2099 if (nullptr == RedB)
2100 {
2101 continue;
2102 }
2103 // 2.25: end if
2104 }
2105 // 2.30: Unmark all states of the original RfnB as predecessors
2106 // (first part) This needs to be done to make sure the call to
2107 // Refine in line 2.26 does not regard some states as marked.
2108 else
2109 {
2110 RedB->set_marked_bottom_begin(RedB->bottom_end());
2111 }
2112 assert(0 == RedB->marked_size());
2113 if (1 == RedB->size() || nullptr == RedB->FromRed(SpC))
2114 {
2115 // If the block only contains a single state or has no
2116 // transitions to SpC, the refinement would be trivial anyway
2117 // (and it cannot find new bottom states).
2118 continue;
2119 }
2120
2121 // 2.26: <RedB, BlueB> := Refine(RedB, SpC\SpB, {}, {transitions
2122 // from RedB to SpC\SpB})
2123 RedB = refine(RedB, SpC, RedB->FromRed(SpC), false
2124 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2125 , NewC
2126 #endif
2127 );
2128 // 2.27: if RedB contains new bottom states then
2129 if (0 != RedB->unmarked_bottom_size())
2130 {
2131 // 2.28: PostprocessNewBottom(RedB, BlueB)
2132 postprocess_new_bottom(RedB);
2133 // 2.29: endif
2134 }
2135 // 2.30: Unmark all states of the original RfnB as predecessors
2136 // if postprocess_new_bottom is called, that procedure already
2137 // unmarks the new bottom states.
2138 else
2139 {
2140 RedB->set_marked_bottom_begin(RedB->bottom_end());
2141 } assert(0 == RedB->marked_size());
2142 // 2.31: end for
2143 }
2144 #ifndef NDEBUG
2145 if (mCRL2logEnabled(log::log_level_t::debug))
2146 {
2147 part_st.print_part(part_tr);
2148 part_st.print_trans();
2149 }
2150
2151 /* 2.32: end while */ part_tr.assert_stability(part_st);
2152 #endif
2153 }
2154 // 2.33: return P
2155 // (this happens implicitly, through the bisim_partitioner_gjkw object
2156 // data)
2157 mCRL2log(log::log_level_t::verbose) << "number of blocks in the quotient: "
2158 << bisim_gjkw::block_t::nr_of_blocks << '\n';
2159}
2160 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2161 namespace bisim_gjkw
2162 {
2163/*=============================================================================
2164= Refine -- Algorithm 3 in [GJKW 2017] =
2165=============================================================================*/
2166 /// \brief moves temporary counters to normal ones if the blue block is
2167 /// smaller
2168 /// \details When a refinement has finished and the blue block turns out to
2169 /// be smaller, this function moves the corresponding temporary work to the
2170 /// normal counters and cancels the work on the red state counters.
2171 /// \param BlueB pointer to the blue block
2172 /// \param RedB pointer to the red block
2173 /// \param NewC (only needed if called after the refinement in line 2.26)
2174 /// pointer to the constellation NewC, i. e. the
2175 /// constellation that was used as the basis of marking
2176 /// states. If blue_is_smaller() is called from another
2177 /// place, this parameter should be nullptr.
2178 static void blue_is_smaller(block_t* BlueB, block_t* RedB,
2179 const constln_t* NewC)
2180 {
2181 assert(nullptr != RedB);
2182 if (nullptr != BlueB)
2183 {
2184 assert(BlueB->size() <= RedB->size());
2185 unsigned const max_NewB = nullptr == BlueB ? 0
2186 : check_complexity::log_n-check_complexity::ilog2(BlueB->size());
2187 for (auto s : *BlueB)
2188 {
2189 mCRL2complexity(s, finalise_work(check_complexity::
2190 while_Test_is_not_empty_3_6l_s_is_blue_3_11l,
2191 check_complexity::refine_bottom_state_3_6l,
2192 max_NewB), );
2193 mCRL2complexity(s, finalise_work(check_complexity::
2194 while_Blue_contains_unvisited_states_3_15l,
2195 check_complexity::refine_visited_state_3_15,
2196 max_NewB), );
2197 for (succ_iter_t succ = s->succ_begin(); s->succ_end() != succ;
2198 ++succ)
2199 {
2200 mCRL2complexity(succ->B_to_C->pred,finalise_work(
2201 check_complexity::
2202 if_s_prime_has_transition_to_SpC_3_23l,
2203 check_complexity::
2204 refine_outgoing_transition_3_6_or_23l, max_NewB), );
2205 }
2206 for (pred_iter_t pred = s->pred_begin(); s->pred_end() != pred;
2207 ++pred)
2208 {
2209 mCRL2complexity(pred, finalise_work(check_complexity::
2210 for_all_s_prime_in_pred_s_setminus_Red_3_18l,
2211 check_complexity::refine_incoming_transition_3_18,
2212 max_NewB), );
2213 }
2214 }
2215 }
2216 // cancel work counters for the red states, and also measure the work
2217 // done in the blue coroutine on states that turned out to be red.
2218 unsigned const max_NewC = nullptr == NewC ? 0
2219 : check_complexity::log_n - check_complexity::ilog2(NewC->size());
2220 for (auto s : *RedB)
2221 {
2222 mCRL2complexity(s, cancel_work(check_complexity::
2223 while_Red_contains_unvisited_states_3_15r), );
2224 for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
2225 {
2226 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2227 check_complexity::while_FromRed_is_not_empty_3_6r), );
2228 // the following counter should only be set for transitions to
2229 // the splitter constellation. For others transitions, no
2230 // (temporary) work should have been done.
2231 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2232 check_complexity::
2233 while_Test_is_not_empty_3_6l_s_is_red_3_9l,
2234 check_complexity::
2235 refine_outgoing_transition_to_marked_state_3_6l,
2236 succ->target->constln() == NewC ? max_NewC : 0), );
2237 // the following counter only gets 1 during postprocessing, at
2238 // a time when state s is already stored as bottom state.
2239 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2240 check_complexity::
2241 while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing,
2242 check_complexity::
2243 refine_outgoing_transition_postprocess_new_bottom_3_6l,
2244 1), );
2245 // the following counter only gets 1 before postprocessing, at
2246 // the same time as when it is discovered to be a new bottom
2247 // state
2248 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2249 check_complexity::if_s_prime_has_transition_to_SpC_3_23l,
2250 check_complexity::
2251 refine_outgoing_transition_from_new_bottom_3_23l, 1), );
2252 }
2253 for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
2254 {
2255 mCRL2complexity(pred, cancel_work(check_complexity::
2256 for_all_s_prime_in_pred_s_3_18r), );
2257 }
2258 }
2259 // check the balance between useful and cancelled work:
2260 check_complexity::check_temporary_work();
2261 }
2262
2263 /// \brief moves temporary counters to normal ones if the red block is
2264 /// smaller
2265 /// \details When a refinement has finished and the red block turns out to
2266 /// be smaller, this function moves the corresponding temporary work to the
2267 /// normal counters and cancels the work on the blue state counters.
2268 /// \param BlueB pointer to the blue block
2269 /// \param RedB pointer to the red block
2270 static void red_is_smaller(block_t* BlueB, block_t* RedB)
2271 {
2272 assert(nullptr != BlueB);
2273 assert(nullptr != RedB);
2274 assert(BlueB->size() >= RedB->size());
2275 for (auto s : *BlueB)
2276 {
2277 mCRL2complexity(s, cancel_work(check_complexity::
2278 while_Test_is_not_empty_3_6l_s_is_blue_3_11l), );
2279 mCRL2complexity(s, cancel_work(check_complexity::
2280 while_Blue_contains_unvisited_states_3_15l), );
2281 for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
2282 {
2283 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2284 check_complexity::
2285 if_s_prime_has_transition_to_SpC_3_23l), );
2286 }
2287 for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
2288 {
2289 mCRL2complexity(pred, cancel_work(check_complexity::
2290 for_all_s_prime_in_pred_s_setminus_Red_3_18l), );
2291 }
2292 }
2293 unsigned const max_NewB = check_complexity::log_n -
2294 check_complexity::ilog2(RedB->size());
2295 for (auto s : *RedB)
2296 {
2297 mCRL2complexity(s, finalise_work(check_complexity::
2298 while_Red_contains_unvisited_states_3_15r,
2299 check_complexity::refine_visited_state_3_15, max_NewB), );
2300 for (succ_iter_t succ=s->succ_begin(); s->succ_end()!=succ; ++succ)
2301 {
2302 mCRL2complexity(succ->B_to_C->pred, finalise_work(
2303 check_complexity::while_FromRed_is_not_empty_3_6r,
2304 check_complexity::
2305 refine_outgoing_transition_3_6_or_23l, max_NewB), );
2306 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2307 check_complexity::
2308 while_Test_is_not_empty_3_6l_s_is_red_3_9l), );
2309 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2310 check_complexity::
2311 while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing), );
2312 mCRL2complexity(succ->B_to_C->pred, cancel_work(
2313 check_complexity::
2314 if_s_prime_has_transition_to_SpC_3_23l), );
2315 }
2316 for (pred_iter_t pred=s->pred_begin(); s->pred_end()!=pred; ++pred)
2317 {
2318 mCRL2complexity(pred, finalise_work(check_complexity::
2319 for_all_s_prime_in_pred_s_3_18r,
2320 check_complexity::refine_incoming_transition_3_18,
2321 max_NewB), );
2322 }
2323 }
2324 check_complexity::check_temporary_work();
2325 }
2326
2327 } // end namespace bisim_gjkw
2328 #endif
2329/// \brief refine a block into the part that can reach `SpC` and the part that
2330/// cannot
2331///
2332/// \details At the beginning of a call to `refine()`, the block RfnB is sliced
2333/// into these parts:
2334///
2335/// | unmarked |marked | unmarked |marked|
2336/// | non-bottom |non-bot| bottom |bottom|
2337///
2338/// The procedure will partition the block into two parts, called ``blue'' and
2339/// ``red''. The red part can reach the splitter constellation `SpC`, the blue
2340/// part cannot. Upon calling `refine()`, it is known that all marked states
2341/// are red.
2342///
2343/// If states with a strong transition to `SpC` have not yet been found, the
2344/// parameter `FromRed` indicates all such transitions, so `refine()` can
2345/// easily find their sources. It is required that either some states are
2346/// marked or a non-nullptr `FromRed` is supplied. In the latter case, also
2347/// the _current constellation_ pointer of all unmarked bottom states is set in
2348/// a way that it makes easy to check whether the state has a transition to
2349/// `SpC`. (Some non-bottom states may have their _current constellation_
2350/// pointer set similarly; while this is not required, it still speeds up
2351/// `refine()`.)
2352///
2353/// `refine()` works by starting two coroutines to find states in the parts;
2354/// as soon as the first coroutine finishes, the refinement can be completed.
2355///
2356/// Refine slices these states further as follows:
2357///
2358/// refine_blue() refine_red()
2359/// shared variable local variable local variable
2360/// notblue_initialised_end visited_end visited_begin
2361/// v v v
2362/// | blue |notblue|notblue| red | blue |unknown|not blue| red |
2363/// |non-bot| > 0 |undef'd| non-bottom|bottom|bottom | bottom | bottom |
2364/// ^ ^ ^
2365/// refine_blue() block.unmarked_ block.unmarked_
2366/// local variable nonbottom_end() bottom_end()
2367/// blue_nonbottom_end
2368///
2369/// - *blue non-bottom:* states of which it is known that they are blue
2370/// - *notblue > 0:* states that have an inert transition to some blue state,
2371/// but for some transition it is not yet known whether they go to a red or a
2372/// blue state
2373/// - *notblue undefined:* for no inert transition it is known whether it goes
2374/// to a red or a blue state
2375/// - *red non-bottom:* states of which it is known that they are red
2376/// - *blue bottom:* states of which it is known that they are blue
2377/// - *unknown bottom:* states that have not yet been checked
2378/// - *not blue bottom:* states of which the blue coroutine has found that they
2379/// are red, but the red coroutine has not yet handled them
2380/// - *red bottom:* states of which everybody knows that they are red
2381///
2382/// Note that the slices of red non-bottom and the red bottom states may become
2383/// larger than the marked (non-)bottom states have been at the start of
2384/// `refine()`. Upon termination of one of the two coroutines, states whose
2385/// colour has not yet been determined become known to be of the colour of the
2386/// unfinished coroutine.
2387///
2388/// \param RfnB the block that has to be refined
2389/// \param SpC the splitter constellation
2390/// \param FromRed the set of transitions from `RfnB` to `SpC`
2391/// \param postprocessing true iff `refine()` is called during postprocessing
2392/// new bottom states
2393/// \note In debug mode, an additional parameter `NewC` is available:
2394/// (only used for measuring the time complexity, and only if called from
2395/// line 2.26) the constellation that was used as the basis of marking
2396/// states. If not called from line 2.26, pass `nullptr`.
2397/// \result a pointer to the block that contains the red part of `RfnB`.
2398
2399template <class LTS_TYPE>
2400bisim_gjkw::block_t* bisim_partitioner_gjkw<LTS_TYPE>::refine(
2401 bisim_gjkw::block_t* const RfnB, const bisim_gjkw::constln_t* const SpC,
2402 const bisim_gjkw::B_to_C_descriptor* const FromRed,
2403 bool const postprocessing
2404 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2405 , const bisim_gjkw::constln_t* NewC
2406 #endif
2407 )
2408{
2409 #ifndef NDEBUG
2410 if (nullptr != FromRed)
2411 {
2412 assert(FromRed->from_block() == RfnB);
2413 assert(FromRed->to_constln() == SpC);
2414 assert(nullptr != SpC);
2415 assert(0 == RfnB->marked_size());
2416 }
2417 else
2418 {
2419 assert(0 != RfnB->marked_size());
2420 }
2421 assert(1 < RfnB->size());
2422 #endif
2423 // 3.2: if RfnB subseteq SpC then return RfnB
2424 if (RfnB->constln() == SpC)
2425 {
2426 // Mark all bottom states to indicate there are no new bottom states.
2427 RfnB->set_marked_nonbottom_begin(RfnB->nonbottom_end());
2428 RfnB->set_marked_bottom_begin(RfnB->bottom_begin());
2429 return RfnB;
2430 }
2431 // 3.3: Test := {bottom states}\Red, ...
2432 // 3.4: Spend the same amount of work on either coroutine:
2433 // and
2434 // 3.39: RedB := RfnB or RedB := NewB , respectively
2435 #ifndef NDEBUG
2436 bisim_gjkw::permutation_iter_t const red_end = RfnB->end();
2437 #endif
2438 bisim_gjkw::block_t* RedB;
2439
2440 // NOLINTBEGIN(cppcoreguidelines-avoid-goto,misc-static-assert) -- generated by the coroutine framework macros
2441 COROUTINES_SECTION
2442 // common variables
2443 bisim_gjkw::permutation_iter_t notblue_initialised_end =
2444 RfnB->nonbottom_begin();
2445 bool FromRed_is_empty = nullptr == FromRed;
2446
2447 // variables for the blue coroutine
2448 bisim_gjkw::permutation_iter_t blue_visited_end;
2449 bisim_gjkw::state_info_ptr blue_s;
2450 bisim_gjkw::pred_iter_t blue_pred_iter;
2451 bisim_gjkw::state_info_ptr blue_s_prime;
2452 bisim_gjkw::permutation_iter_t blue_blue_nonbottom_end;
2453 bisim_gjkw::succ_const_iter_t blue_begin;
2454 bisim_gjkw::succ_const_iter_t blue_end;
2455
2456 // variables for the red coroutine
2457 bisim_gjkw::B_to_C_iter_t red_fromred_visited_begin;
2458 bisim_gjkw::permutation_iter_t red_visited_begin;
2459 bisim_gjkw::state_info_ptr red_s;
2460 bisim_gjkw::pred_iter_t red_pred_iter;
2461
2462 // NOLINTNEXTLINE(cppcoreguidelines-avoid-c-arrays,modernize-avoid-c-arrays)
2463 COROUTINE_LABELS( (REFINE_BLUE_PREDECESSOR_HANDLED)
2464 (REFINE_BLUE_TESTING)
2465 (REFINE_BLUE_STATE_HANDLED)
2466 (REFINE_BLUE_COLLECT_BOTTOM)
2467 (REFINE_RED_COLLECT_FROMRED)
2468 (REFINE_RED_PREDECESSOR_HANDLED)
2469 (REFINE_RED_STATE_HANDLED))
2470
2471/*--------------------------- handle blue states ----------------------------*/
2472
2473/// The blue coroutine finds blue states in a block, i. e. states that cannot
2474/// reach the splitter. It is one of the two coroutines that together
2475/// implement the fast refinement of block `RfnB` into states that can reach
2476/// the splitter `SpC` (red states) and those that cannot (blue states).
2477///
2478/// This coroutine assumes that `RfnB` is nontrivial, i. e. contains at least
2479/// two states. `refine()` may be called in two ways: either the initially
2480/// red states are marked, or a set of transitions from `RfnB` to `SpC` is
2481/// given. In the first case, all unmarked bottom states are blue. In the
2482/// second case, however, the first thing this coroutine has to do is to decide
2483/// which bottom states are blue and which ones are not. In that case, it
2484/// assumes that the `current_constln` pointer of bottom states is pointing to
2485/// a place where a transition to `SpC` could be inserted. If there is already
2486/// such a transition just before or after that memory location, the bottom
2487/// state is actually red; otherwise, it is blue.
2488///
2489/// After having found the blue bottom states, the coroutine proceeds to find
2490/// blue non-bottom states by walking through the predecessors of the blue
2491/// states. As soon as can be determined that all inert outgoing transitions
2492/// of a state lead to (other) blue states, this state is also blue -- with one
2493/// exception: if this state has a (non-inert) transition to the splitter. If
2494/// `refine()` was called in the second way, one has to check the outgoing
2495/// non-inert transitions to find out whether such a transition exists.
2496///
2497/// As soon as it becomes clear that the blue subblock will be larger, this
2498/// coroutine is aborted. Otherwise, at the end `RfnB` is actually split into
2499/// its two parts, and the coroutine closes with updating the inert-ness of
2500/// transitions and finding new bottom states. New bottom states will be
2501/// unmarked bottom states. (It may also happen that the blue subblock is
2502/// empty; in that case, `RfnB` is not split.)
2503///
2504/// The coroutine implements the left-hand side of Algorithm 3 in [GJKW 2017].
2505
2506 COROUTINE assert(RfnB->nonbottom_begin() == notblue_initialised_end);
2507 // we have to decide which unmarked bottom states are blue. So we
2508 // walk over all of them and check whether they have a transition
2509 // to SpC or not.
2510 // 3.3: ..., Blue := {}
2511 blue_visited_end = RfnB->unmarked_bottom_begin();
2512 // 3.5l: whenever |Blue| > |RfnB|/2 do Abort this coroutine
2513 // nothing needs to be done now, as |Blue| = 0 here.
2514
2515 /* - - - - - - - collect blue bottom states - - - - - - - */
2516
2517 // 3.6l: while Test is not empty and FromRed is not empty do
2518 // We use the variable blue_visited_end in this loop to
2519 // indicate the boundary between blue states (namely those
2520 // in the interval [RfnB->unmarked_bottom_begin(),
2521 // blue_visited_end) ) and Test states (namely those in
2522 // [blue_visited_end, RfnB->unmarked_bottom_end()) ).
2523 COROUTINE_WHILE (REFINE_BLUE_COLLECT_BOTTOM,
2524 RfnB->unmarked_bottom_end() > blue_visited_end)
2525 {
2526 if (FromRed_is_empty)
2527 {
2528 // 3.14l: Blue := Blue union Test
2529 // done implicitly: we now regard all unmarked
2530 // bottom states as blue, i. e. the whole
2531 // interval [RfnB->unmarked_bottom_begin(),
2532 // RfnB->unmarked_bottom_end()).
2533 // 3.5l: whenever |Blue|>|RfnB|/2 do Abort this coroutine
2534 // In this case, Test may not yet be empty, so here we
2535 // have to check the condition of Line 3.5l.
2536 if (RfnB->unmarked_bottom_size() > RfnB->size() / 2)
2537 {
2538 ABORT_THIS_COROUTINE();
2539 }
2540 break;
2541 }
2542 // 3.7l: Choose s in Test
2543 blue_s = *blue_visited_end;
2544 // 3.8l: if s --> SpC then
2545 if (blue_s->surely_has_transition_to(SpC))
2546 {
2547 // 3.9l: Move s from Test to Red
2548 // The state s is not blue. Move it to the slice of
2549 // non-blue bottom states.
2550 RfnB->set_marked_bottom_begin(
2551 RfnB->marked_bottom_begin() - 1);
2552 bisim_gjkw::swap_permutation(blue_visited_end,
2553 RfnB->marked_bottom_begin());
2554 // 3.5r: whenever |Red|>|RfnB|/2 do Abort the red coroutine
2555 if (RfnB->marked_size() > RfnB->size() / 2)
2556 {
2557 ABORT_OTHER_COROUTINE();
2558 }
2559 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2560 // The state is red. Depending on the context of refinement, the work done
2561 // on this state is attributed to one or another element of the Kripke
2562 // structure.
2563 if (postprocessing)
2564 {
2565 // refine() has been called from line 4.14. During postprocessing, the
2566 // work is ascribed to the transitions from s to SpC.
2567 // Using the current_constln pointer of s, find a transition to SpC.
2568 // The work has to be ascribed to the transitions from s to SpC.
2569 bisim_gjkw::succ_iter_t to_SpC = blue_s->current_constln();
2570 if (to_SpC == blue_s->succ_end() || to_SpC->target->constln() != SpC)
2571 {
2572 assert(blue_s->succ_begin() < to_SpC);
2573 --to_SpC;
2574 assert(to_SpC->target->constln() == SpC);
2575 }
2576 bisim_gjkw::succ_entry::slice_add_work_to_transns(to_SpC,
2577 check_complexity::
2578 while_Test_is_not_empty_3_6l_s_is_red_3_9l_postprocessing, 1);
2579 }
2580 else
2581 {
2582 // refine() has been called from line 2.26, and RfnB is a block with a
2583 // transition to SpB. The state has been marked because of these
2584 // transitions (which are not transitions to SpC!).
2585 // code similar to the case if (postprocessing).
2586 bisim_gjkw::succ_iter_t to_NewC = blue_s->current_constln();
2587 if (to_NewC == blue_s->succ_end() || to_NewC->target->constln() == SpC)
2588 {
2589 assert(blue_s->succ_begin() < to_NewC);
2590 --to_NewC;
2591 assert(to_NewC->target->constln() != SpC);
2592 }
2593 bisim_gjkw::succ_entry::slice_add_work_to_transns(to_NewC,
2594 check_complexity::while_Test_is_not_empty_3_6l_s_is_red_3_9l, 1);
2595 }
2596 #endif
2597 // 3.10l: else
2598 }
2599 else
2600 { assert(blue_s->surely_has_no_transition_to(SpC));
2601 // 3.11l: Move s from Test to Blue
2602 ++blue_visited_end;
2603 // 3.5l: whenever |Blue|>|RfnB|/2 do Abort this coroutine
2604 if ((state_type) (blue_visited_end -
2605 RfnB->unmarked_bottom_begin()) > RfnB->size() / 2)
2606 {
2607 ABORT_THIS_COROUTINE();
2608 } mCRL2complexity(blue_s, add_work(
2609 check_complexity::while_Test_is_not_empty_3_6l_s_is_blue_3_11l, 1), );
2610 // 3.12l: end if
2611 }
2612 // 3.13l: end while
2613 }
2614 END_COROUTINE_WHILE; assert(RfnB->constln() != SpC);
2615
2616 if (0 == RfnB->unmarked_bottom_size())
2617 {
2618 // all bottom states are red, so there cannot be any blue
2619 // states.
2620 RfnB->set_marked_nonbottom_begin(RfnB->marked_nonbottom_end());
2621 // RfnB->set_marked_bottom_begin(RfnB->bottom_begin());
2622 RedB = RfnB;
2623 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2624 blue_is_smaller(nullptr, RedB, NewC);
2625 #endif
2626 TERMINATE_COROUTINE_SUCCESSFULLY();
2627 }
2628
2629 /* - - - - - - - - visit blue states - - - - - - - - */
2630
2631 // 3.15l: while Blue contains unvisited states do
2632 blue_visited_end = RfnB->unmarked_bottom_begin();
2633 blue_blue_nonbottom_end = RfnB->unmarked_nonbottom_begin();
2634 COROUTINE_DO_WHILE (REFINE_BLUE_STATE_HANDLED,
2635 blue_visited_end != blue_blue_nonbottom_end)
2636 {
2637 // 3.16l: Choose an unvisited s in Blue
2638 blue_s = *blue_visited_end; assert(blue_visited_end < blue_blue_nonbottom_end ||
2639 (RfnB->unmarked_bottom_begin() <= blue_visited_end &&
2640 RfnB->unmarked_bottom_end() > blue_visited_end));
2641 assert(RfnB->unmarked_nonbottom_begin() <= blue_blue_nonbottom_end);
2642 assert(blue_blue_nonbottom_end <= notblue_initialised_end);
2643 /* 3.17l: Mark s as visited */ assert(RfnB->unmarked_nonbottom_end() >= notblue_initialised_end);
2644 ++blue_visited_end;
2645 // 3.18l: for all s_prime in inert_in(s) \ Red do
2646 COROUTINE_FOR (REFINE_BLUE_PREDECESSOR_HANDLED,
2647 blue_pred_iter = blue_s->inert_pred_begin(),
2648 blue_s->inert_pred_end()!=blue_pred_iter, ++blue_pred_iter)
2649 {
2650 blue_s_prime = blue_pred_iter->source;
2651 if (blue_s_prime->pos >= RfnB->marked_nonbottom_begin())
2652 { mCRL2complexity(blue_pred_iter, add_work(
2653 check_complexity::for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2654 continue;
2655 }
2656 // 3.19l: if notblue(s_prime) undefined then
2657 if (blue_s_prime->pos >= notblue_initialised_end)
2658 {
2659 // 3.20l: notblue(s_prime) := |inert_out(s_prime)|
2660 blue_s_prime->notblue = blue_s_prime->inert_succ_end()-
2661 blue_s_prime->inert_succ_begin();
2662 bisim_gjkw::swap_permutation(blue_s_prime->pos,
2663 notblue_initialised_end);
2664 ++notblue_initialised_end;
2665 // 3.21l: end if
2666 }
2667 // 3.22l: notblue(s_prime) := notblue(s_prime) - 1
2668 --blue_s_prime->notblue;
2669 // 3.23l: if notblue(s_prime) == 0 && ...
2670 if (0 != blue_s_prime->notblue)
2671 { mCRL2complexity(blue_pred_iter, add_work(
2672 check_complexity::for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2673 continue;
2674 }
2675 // 3.23l: ... && (FromRed == {} ||
2676 // out_noninert(s_prime) intersect SpC == {}) then
2677 if (!FromRed_is_empty)
2678 {
2679 if (blue_s_prime->surely_has_transition_to(SpC))
2680 { mCRL2complexity(blue_pred_iter, add_work(
2681 check_complexity::for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2682 continue;
2683 }
2684 if (!blue_s_prime->surely_has_no_transition_to(SpC))
2685 {
2686 // It is not yet known whether s_prime has a
2687 // transition to SpC or not. Execute the slow test
2688 // now.
2689 COROUTINE_FOR (REFINE_BLUE_TESTING,
2690 (blue_begin = blue_s_prime->succ_begin(),
2691 blue_end = blue_s_prime->succ_end() ),
2692 blue_begin < blue_end, (void) 0)
2693 {
2694 // binary search for transitions from s_prime
2695 // to constellation SpC.
2696 bisim_gjkw::succ_const_iter_t const mid =
2697 blue_begin + (blue_end - blue_begin) / 2;
2698 if (*SpC <= *mid->target->constln())
2699 {
2700 blue_end = mid->slice_begin();
2701 }
2702 if (*mid->target->constln() <= *SpC)
2703 {
2704 blue_begin =
2705 bisim_gjkw::succ_entry::slice_end(mid);
2706 }
2707 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2708 bisim_gjkw::succ_entry::slice_add_work_to_transns(mid,
2709 check_complexity::if_s_prime_has_transition_to_SpC_3_23l, 1);
2710 #endif
2711 }
2712 END_COROUTINE_FOR;
2713 if (blue_begin != blue_end)
2714 { mCRL2complexity(blue_pred_iter, add_work(
2715 check_complexity::for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2716 continue;
2717 }
2718 }
2719 }
2720 // 3.24l: Blue := Blue union {s_prime}
2721 bisim_gjkw::swap_permutation(blue_s_prime->pos,
2722 blue_blue_nonbottom_end);
2723 ++blue_blue_nonbottom_end;
2724 // 3.5l: whenever |Blue|>|RfnB| / 2 do Abort this coroutine
2725 if (blue_blue_nonbottom_end -
2726 RfnB->unmarked_nonbottom_begin() +
2727 RfnB->unmarked_bottom_size() > RfnB->size() / 2)
2728 {
2729 ABORT_THIS_COROUTINE();
2730 }
2731 // 3.25l: end if
2732 // this is implicit in the `continue` statements above.
2733 /* 3.26l: end for */ mCRL2complexity(blue_pred_iter, add_work(
2734 check_complexity::for_all_s_prime_in_pred_s_setminus_Red_3_18l, 1), );
2735 }
2736 END_COROUTINE_FOR;
2737 /* 3.27l: end while */ mCRL2complexity(blue_s, add_work(
2738 check_complexity::while_Blue_contains_unvisited_states_3_15l, 1), );
2739 if (RfnB->unmarked_bottom_end() == blue_visited_end)
2740 {
2741 blue_visited_end = RfnB->unmarked_nonbottom_begin();
2742 }
2743 }
2744 END_COROUTINE_DO_WHILE;
2745
2746 /* - - - - - - - - split off blue block - - - - - - - - */
2747
2748 // 3.28l: Abort the other coroutine
2749 ABORT_OTHER_COROUTINE();
2750 // All non-blue states are red.
2751 // 3.29l: Move Blue to a new block NewB
2752 // and
2753 // 3.30l: Destroy all temporary data
2754 bisim_gjkw::block_t* const NewB =
2755 RfnB->split_off_blue(blue_blue_nonbottom_end);
2756 part_tr.new_blue_block_created(RfnB, NewB);
2757 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2758 unsigned const max_counter = check_complexity::log_n -
2759 check_complexity::ilog2(NewB->size());
2760 mCRL2complexity(NewB,
2761 add_work(check_complexity::for_all_s_in_NewB_3_31, max_counter), );
2762 #endif
2763 // 3.31l: for all s in NewB do
2764 for (bisim_gjkw::permutation_iter_t s_iter = NewB->begin();
2765 NewB->end() != s_iter; ++s_iter)
2766 {
2767 blue_s = *s_iter; // mCRL2complexity(s, ...) -- optimized to the above call.
2768 // 3.32l: for all s_prime in inert_in(s) \ NewB do
2769 for (blue_pred_iter = blue_s->inert_pred_begin();
2770 blue_s->inert_pred_end()!=blue_pred_iter; ++blue_pred_iter)
2771 { mCRL2complexity(blue_pred_iter, add_work(
2772 check_complexity::for_all_s_prime_in_pred_s_3_32l, max_counter), );
2773 assert(part_tr.pred_end() > blue_pred_iter);
2774 assert(blue_pred_iter->succ->B_to_C->pred == blue_pred_iter);
2775 blue_s_prime = blue_pred_iter->source;
2776 if (blue_s_prime->block == NewB) { continue; } assert(blue_s_prime->block == RfnB);
2777 // 3.33l: s_prime --> s is no longer inert
2778 part_tr.make_noninert(blue_pred_iter->succ);
2779 // 3.34l: if |inert_out(s_prime)| == 0 then
2780 if (blue_s_prime->inert_succ_begin() ==
2781 blue_s_prime->inert_succ_end())
2782 {
2783 // 3.35l: s_prime is a new bottom state
2784 RfnB->set_marked_nonbottom_begin(
2785 RfnB->bottom_begin() - 1);
2786 RfnB->set_bottom_begin(RfnB->marked_nonbottom_begin());
2787 swap_permutation(blue_s_prime->pos,
2788 RfnB->bottom_begin()); // assert("blue_s_prime has a transition to SpC");
2789 // 3.36l: end if
2790 }
2791 // 3.37l: end for
2792 }
2793 // 3.38l: end for
2794 }
2795
2796 RedB = RfnB;
2797 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2798 blue_is_smaller(NewB, RedB, NewC);
2799 #endif
2800 END_COROUTINE
2801
2802/*---------------------------- handle red states ----------------------------*/
2803
2804/// The red coroutine finds red states in a block, i. e. states that can reach
2805/// the splitter. It is one of the two coroutines that together implement
2806/// the fast refinement of block `RfnB` into states that can reach the splitter
2807/// (red states) and those that cannot (blue states).
2808///
2809/// This coroutine assumes that `RfnB` is nontrivial, i. e. contains at least
2810/// two states, and that there is at least one red state in `RfnB`. The red
2811/// states can be indicated in one of two ways: either some states of `RfnB`
2812/// are marked, or the parameter `FromRed` indicates the set of transitions
2813/// from `RfnB` to the splitter. Exactly one of the two must be chosen: If
2814/// and only if some states are marked, `FromRed` should be `nullptr`.
2815///
2816/// If `FromRed` is not `nullptr`, the coroutine first finds initially red
2817/// states, i. e. states with a transition to the splitter, and marks them.
2818/// Note that it may happen that some non-bottom states (or even only
2819/// non-bottom states) may be initially red as well. When all initially red
2820/// states are marked, it proceeds to find other red states by walking through
2821/// the inert predecessors of red states. Every such predecessor is also a red
2822/// state.
2823///
2824/// As soon as it becomes clear that the red subblock will be larger, this
2825/// coroutine is aborted. Otherwise, at the end `RfnB` is actually split into
2826/// its two parts, and the coroutine closes with updating the inert-ness of
2827/// transitions and finding new bottom states. New bottom states will be
2828/// unmarked bottom states.
2829///
2830/// The coroutine implements the right-hand side of Algorithm 3 in [GJKW 2017].
2831
2832 COROUTINE
2833 // 3.5r: whenever |Red| > |RfnB|/2 then Abort this coroutine
2834 if (RfnB->marked_size() > RfnB->size() / 2)
2835 {
2836 ABORT_THIS_COROUTINE();
2837 }
2838 // The red block contains at most RfnB->size() -
2839 // RfnB->unmarked_bottom_size() + FromRed->size() states. If that
2840 // is <= RfnB->size() / 2, we could abort the other coroutine
2841 // immediately. We don't do it here because we want to investigate
2842 // the effect of this and similar heuristics more systematically.
2843
2844 /* - - - - - - - collect states from FromRed - - - - - - - */
2845
2846 // 3.6r: while FromRed != {} do
2847 if (nullptr != FromRed)
2848 { assert(FromRed->from_block() == RfnB);
2849 red_fromred_visited_begin = FromRed->end; assert(RfnB->inert_end() <= FromRed->begin ||
2850 (RfnB->inert_begin() >= red_fromred_visited_begin &&
2851 RfnB->inert_end() > red_fromred_visited_begin));
2852 COROUTINE_WHILE (REFINE_RED_COLLECT_FROMRED,
2853 FromRed->begin != red_fromred_visited_begin)
2854 {
2855 // 3.10r (order of lines changed): FromRed := FromRed \ {s --> t}
2856 // We can change the order of lines because the
2857 // coroutine is not interrupted in between.
2858 --red_fromred_visited_begin;
2859 // 3.7r: Choose s --> t in FromRed
2860 bisim_gjkw::state_info_ptr const red_s =
2861 red_fromred_visited_begin->pred->source; assert(RfnB->begin() <= red_s->pos);
2862 /* 3.8r: Test := Test \ {s} */ assert(red_s->pos < RfnB->end());
2863 // and
2864 // 3.9r: Red := Red union {s}
2865 if (red_s->pos < notblue_initialised_end)
2866 {
2867 // The non-bottom state has a transition to a blue
2868 // state, so notblue is initialised; however, now it is
2869 // revealed to be red anyway.
2870 bisim_gjkw::swap_permutation(red_s->pos,
2871 --notblue_initialised_end);
2872 }
2873 if (RfnB->mark(red_s) &&
2874 // 3.5r: whenever |Red| > |RfnB|/2 do Abort this coroutine
2875 RfnB->marked_size() > RfnB->size() / 2)
2876 {
2877 ABORT_THIS_COROUTINE();
2878 }
2879 /* 3.13r: end while */ mCRL2complexity(red_fromred_visited_begin->pred,
2880 add_work(check_complexity::while_FromRed_is_not_empty_3_6r, 1), );
2881 }
2882 END_COROUTINE_WHILE;
2883
2884 // The shared variable FromRed_is_empty is set to true as soon
2885 // as FromRed should be considered empty. (From that moment
2886 // on, no slow tests are needed any more.)
2887 FromRed_is_empty = true;
2888 } assert(FromRed_is_empty); assert(0 != RfnB->marked_size());
2889
2890 /* - - - - - - - - visit red states - - - - - - - - */
2891
2892 red_visited_begin = RfnB->marked_bottom_end();
2893 if (RfnB->marked_bottom_begin() == red_visited_begin)
2894 {
2895 // It may happen that all found states are non-bottom states.
2896 // (In that case, some of these states will become new bottom
2897 // states.)
2898 red_visited_begin = RfnB->marked_nonbottom_end();
2899 }
2900 // 3.15r: while Red contains unvisited states do
2901 COROUTINE_DO_WHILE(REFINE_RED_STATE_HANDLED,
2902 RfnB->marked_nonbottom_begin() != red_visited_begin)
2903 {
2904 // 3.17r (order of lines changed): Mark s as visited
2905 --red_visited_begin; assert(RfnB->marked_bottom_begin() <= red_visited_begin ||
2906 (RfnB->marked_nonbottom_begin() <= red_visited_begin &&
2907 RfnB->marked_nonbottom_end() > red_visited_begin));
2908 // 3.16r: Choose an unvisited s in Red
2909 red_s = *red_visited_begin;
2910 // 3.18r: for all s_prime in inert_in(s) do
2911 COROUTINE_FOR (REFINE_RED_PREDECESSOR_HANDLED,
2912 red_pred_iter = red_s->inert_pred_begin(),
2913 red_s->inert_pred_end() != red_pred_iter, ++red_pred_iter)
2914 {
2915 bisim_gjkw::state_info_ptr const s_prime =
2916 red_pred_iter->source;
2917 // 3.24r: Red := Red union {s_prime}
2918 if (s_prime->pos < notblue_initialised_end)
2919 {
2920 // The state has a transition to a blue state, so
2921 // notblue is initialised; however, now it is revealed
2922 // to be red anyway.
2923 bisim_gjkw::swap_permutation(s_prime->pos,
2924 --notblue_initialised_end);
2925 }
2926 if (RfnB->mark_nonbottom(s_prime) &&
2927 // 3.5r: whenever |Red| > |RfnB|/2 do Abort this coroutine
2928 RfnB->marked_size() > RfnB->size() / 2)
2929 {
2930 ABORT_THIS_COROUTINE();
2931 }
2932 /* 3.26r: end for */ mCRL2complexity(red_pred_iter,
2933 add_work(check_complexity::for_all_s_prime_in_pred_s_3_18r, 1), );
2934 }
2935 END_COROUTINE_FOR;
2936 /* 3.27r: end while */ mCRL2complexity(red_s, add_work(
2937 check_complexity::while_Red_contains_unvisited_states_3_15r, 1), );
2938 if (RfnB->marked_bottom_begin() == red_visited_begin)
2939 {
2940 red_visited_begin = RfnB->marked_nonbottom_end();
2941 }
2942 }
2943 END_COROUTINE_DO_WHILE;
2944
2945 /* - - - - - - - - split off red block - - - - - - - - */
2946
2947 // 3.28r: Abort the other coroutine
2948 ABORT_OTHER_COROUTINE();
2949 // All non-red states are blue.
2950 // 3.29r: Move Red to a new block RedB
2951 // and
2952 // 3.30r: Destroy all temporary data
2953 RedB = RfnB->split_off_red(RfnB->marked_nonbottom_begin());
2954 part_tr.new_red_block_created(RfnB, RedB, postprocessing);
2955 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
2956 unsigned const max_counter = check_complexity::log_n -
2957 check_complexity::ilog2(RedB->size());
2958 mCRL2complexity(RedB,
2959 add_work(check_complexity::for_all_s_in_NewB_3_31, max_counter), );
2960 #endif
2961 // 3.31r: for all non-bottom s in RedB do
2962 // we have to run through the states backwards because
2963 // otherwise, we might miss out some states.
2964 for (bisim_gjkw::permutation_iter_t s_iter = RedB->nonbottom_end();
2965 RedB->nonbottom_begin() != s_iter; )
2966 {
2967 --s_iter;
2968 red_s = *s_iter; // mCRL2complexity(s, ...) -- optimized to the above call.
2969 // 3.32r: for all s_prime in inert_out(s) \ RedB do
2970 for (bisim_gjkw::succ_iter_t
2971 succ_iter = red_s->inert_succ_begin();
2972 red_s->inert_succ_end()!=succ_iter; ++succ_iter)
2973 { mCRL2complexity(succ_iter->B_to_C->pred, add_work(
2974 check_complexity::for_all_s_prime_in_succ_s_3_32r, max_counter), );
2975 assert(part_tr.succ_end() > succ_iter);
2976 assert(succ_iter->B_to_C->pred->succ == succ_iter);
2977 if (bisim_gjkw::state_info_ptr const s_prime =
2978 succ_iter->target;
2979 s_prime->block == RedB)
2980 {
2981 continue;
2982 }
2983 else
2984 {
2985 assert(s_prime->block == RfnB);
2986 }
2987 // 3.33r: s --> s_prime is no longer inert
2988 part_tr.make_noninert(succ_iter);
2989 // 3.34r: end for
2990 }
2991 // 3.35r: if |inert_out(s)| == 0 then
2992 if (red_s->inert_succ_begin() == red_s->inert_succ_end())
2993 {
2994 // 3.36r: s is a new bottom state
2995 RedB->set_marked_nonbottom_begin(RedB->bottom_begin() - 1);
2996 RedB->set_bottom_begin(RedB->marked_nonbottom_begin());
2997 swap_permutation(red_s->pos, RedB->bottom_begin()); // assert("red_s has a transition to SpC");
2998 // 3.37r: end if
2999 }
3000 // 3.38r: end for
3001 } assert(RfnB->end() < red_end);
3002 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3003 red_is_smaller(RfnB, RedB);
3004 #endif
3005 END_COROUTINE
3006 END_COROUTINES_SECTION
3007 // NOLINTEND(cppcoreguidelines-avoid-goto,misc-static-assert)
3008
3009
3010 /* 3.41 P := partition P where NewB is added and the states in NewB are */ assert(RedB->end() == red_end);
3011 // removed from RfnB
3012 // done through adapting the data structures in the coroutines.
3013 // 3.42: return <RedB, BlueB> (with old and new bottom states separated)
3014 // The separation is indicated by marking the old bottom states.
3015 // Only RedB is returned explicitly, as most calls to Refine only use
3016 // RedB.
3017 return RedB;
3018}
3019
3020
3021
3022/*=============================================================================
3023= PostprocessNewBottom -- Algorithm 4 in [GJKW 2017] =
3024=============================================================================*/
3025
3026
3027
3028/// \brief function object to compare two constln_t pointers based on their
3029/// contents
3030/// \details This function object is used to create a sorted set of
3031/// constellations, namely those that are reachable from the block of new
3032/// bottom states in Algorithm 4.
3033class constln_ptr_less
3034{
3035 public:
3036 bool operator() (const bisim_gjkw::constln_t* a,
3037 const bisim_gjkw::constln_t* b) const
3038 {
3039 return *a < *b;
3040 }
3041};
3042
3043using R_map_t = std::set<bisim_gjkw::constln_t*, constln_ptr_less>;
3044
3045/// \brief Split a block with new bottom states as needed
3046/// \details The function splits RedB by checking whether all new bottom
3047/// states can reach the constellations that RedB can reach.
3048///
3049/// When this function starts, it assumes that the old bottom states of RedB
3050/// are marked and the new ones are not. It is an error if RedB does not
3051/// contain any new bottom states.
3052/// The function implements Algorithm 4 of [GJKW 2017]. It first separates the
3053/// old from the new bottom states; then it walks through all constellations
3054/// that can be reached from the new bottom states to separate them into
3055/// smaller, stable subblocks. The return value is the block containing the
3056/// old bottom states, resulting from the first separation.
3057/// \param RedB block containing new bottom states that need to be stabilised
3058/// \returns the block containing the old bottom states (and every state in
3059/// RedB that can reach some old bottom state through inert
3060/// transitions)
3061template <class LTS_TYPE>
3062bisim_gjkw::block_t* bisim_partitioner_gjkw<LTS_TYPE>::postprocess_new_bottom(
3063 bisim_gjkw::block_t* RedB
3064 /* , bisim_gjkw::block_t* BlueB */)
3065{ assert(0 != RedB->unmarked_bottom_size());
3066 assert(RedB->marked_nonbottom_begin() == RedB->marked_nonbottom_end());
3067 /*------- collect constellations reachable from new bottom states -------*/
3068
3069 // 4.3: <ResultB, RfnB> := Refine(RedB, cosplit(RedB, BlueB), {old bottom
3070 // states in RedB}, {})
3071 bisim_gjkw::block_t* ResultB;
3072 bisim_gjkw::block_t* RfnB;
3073 #ifndef NDEBUG
3074 bisim_gjkw::permutation_const_iter_t blue_begin = RedB->begin();
3075 #endif
3076 if (0 != RedB->marked_bottom_size())
3077 {
3078 // postprocessing == false is required here because we need to keep
3079 // ResultB->FromRed().
3080 ResultB = refine(RedB, nullptr, nullptr, false); assert(nullptr != ResultB); assert(0 == ResultB->unmarked_bottom_size());
3081 // 4.26: Destroy all temporary data
3082 // As part of this line, we unmark all states.
3083 ResultB->set_marked_bottom_begin(ResultB->bottom_end()); assert(ResultB->begin() > blue_begin);
3084 RfnB = ResultB->begin()[-1]->block;
3085 }
3086 else
3087 {
3088 RfnB = RedB;
3089 ResultB = nullptr;
3090 } assert(ResultB != RfnB); assert(RfnB->begin() == blue_begin);
3091 // do not refine a trivial block
3092 if (1 == RfnB->size())
3093 { assert(0 == RfnB->marked_size());
3094 return ResultB;
3095 }
3096 // 4.2: Create an empty search tree R of constellations
3097 R_map_t R;
3098Line_4_4:
3099 /* 4.4: for all constellations C not in R reachable from RfnB do */ assert(0 == RfnB->marked_bottom_size());
3100 while (!RfnB->to_constln.front().needs_postprocessing())
3101 {
3102 bisim_gjkw::B_to_C_desc_iter_t const new_slice =
3103 RfnB->to_constln.begin(); // try to assign the work to the transitions from bottom states in RfnB to C.
3104 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3105 if (!new_slice->add_work_to_bottom_transns(check_complexity::
3106 for_all_transitions_from_bottom_states_a_priori_4_4, 1))
3107 {
3108 // It didn't work out -- now assign it temporarily to the
3109 // B_to_C slice itself.
3110 mCRL2complexity(new_slice, add_work(check_complexity::
3111 for_all_constellations_C_not_in_R_from_RfnB_4_4, 1), );
3112 }
3113 #endif
3114 bisim_gjkw::constln_t* const C = new_slice->to_constln();
3115 // 4.5: Add C to R
3116 if (!R.insert(C).second) //< complexity log(n)
3117 { assert(0 && "The constellation already was in R");
3118 }
3119 // 4.6: Register that the transitions from RfnB to C need
3120 /* postprocessing */ assert(C->postprocess_begin == C->postprocess_end);
3121 C->postprocess_begin = new_slice->begin;
3122 C->postprocess_end = new_slice->end; assert(C->postprocess_begin < C->postprocess_end);
3123 // move the set of transitions to the end of the list
3124 RfnB->to_constln.splice(RfnB->to_constln.end(), RfnB->to_constln,
3125 new_slice);
3126 // 4.7: end for
3127 }
3128 // 4.8: for all bottom states s in RfnB do
3129 bisim_gjkw::permutation_iter_t s_iter = RfnB->unmarked_bottom_begin();
3130 do
3131 {
3132 bisim_gjkw::state_info_ptr const s = *s_iter; mCRL2complexity(s,
3133 add_work(check_complexity::for_all_bottom_states_s_in_RfnB_4_8, 1), );
3134 // 4.9: Set the current constellation pointer of s to the first
3135 // constellation it can reach
3136 s->set_current_constln(s->succ_begin());
3137 // 4.10: end for
3138 }
3139 while (RfnB->unmarked_bottom_end() != ++s_iter);
3140
3141 /*--------------- stabilise w. r. t. found constellations ---------------*/
3142
3143 // 4.11: for all constellations SpC in R (in order) do
3144 while (!R.empty())
3145 { // the work has to be assigned to the transitions from (new) bottom
3146 bisim_gjkw::constln_t* const SpC = *R.begin(); // states to constellation SpC. We do that assignment in the inner
3147 // 4.12: for all blocks B with transitions to SpC that need // loop. Ensure that the inner loop is executed:
3148 /* postprocessing do */ assert(SpC->postprocess_begin != SpC->postprocess_end);
3149 do
3150 {
3151 // add_work is called indirectly: after refining, work is assigned
3152 // to every (new) bottom state in the refined block.
3153 bisim_gjkw::B_to_C_iter_t const B_iter = SpC->postprocess_begin; assert(part_tr.B_to_C_end() > B_iter);
3154 bisim_gjkw::block_t* const B = B_iter->pred->source->block; assert(B_iter->pred->succ->B_to_C == B_iter);
3155 bisim_gjkw::B_to_C_desc_iter_t FromRed = B_iter->B_to_C_slice; assert(FromRed->begin == B_iter);
3156 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3157 bool postproc_a_posteriori = !FromRed->
3158 add_work_to_bottom_transns(check_complexity::
3159 for_all_transitions_that_need_postproc_a_priori_4_12, 1);
3160 #endif
3161 // 4.13: Delete the transitions from B to SpC from those that need
3162 // postprocessing
3163 SpC->postprocess_begin = FromRed->end; assert(SpC->postprocess_begin <= SpC->postprocess_end);
3164 assert(!B->to_constln.empty());
3165 if (B->to_constln.begin() != FromRed)
3166 { assert(FromRed->from_block() == B);
3167 B->to_constln.splice(B->to_constln.begin(), B->to_constln,
3168 FromRed);
3169 }
3170 /* do not refine a trivial block */ assert(0 == B->marked_size());
3171 if (1 == B->size())
3172 { assert(!postproc_a_posteriori);
3173 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3174 if (0 != FromRed->work_counter.get_work_counter_4_4())
3175 {
3176 if (!FromRed->add_work_to_bottom_transns(check_complexity::
3177 for_all_transitions_from_bottom_states_a_posteriori_4_4, 1))
3178 { assert(0); }
3179 FromRed->work_counter.reset_work_counter_4_4();
3180 }
3181 #endif
3182 continue;
3183 }
3184 // refine() may destroy FromRed: if the red subblock is smaller,
3185 // the transitions in FromRed are moved to a new B_to_C slice.
3186 // Therefore we select some transition from it, to restore the
3187 // slice afterwards. Any transition should do.
3188 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3189 bisim_gjkw::pred_iter_t FromRed_save = FromRed->begin->pred;
3190 #endif
3191 // 4.14: <RedB, BlueB> := Refine(B, SpC, {}, {transitions to SpC})
3192 RedB = refine(B, SpC, &*FromRed, true);
3193 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3194 FromRed = FromRed_save->succ->B_to_C->B_to_C_slice;
3195 if (postproc_a_posteriori && !FromRed->add_work_to_bottom_transns(
3196 check_complexity::
3197 for_all_transitions_that_need_postproc_a_posteriori_4_12, 1))
3198 {
3199 assert(0 && "no new bottom states to assign work to");
3200 }
3201 // try to move the work that was not yet moved to the
3202 // transitions from (new) bottom states now.
3203 if (0 != FromRed->work_counter.get_work_counter_4_4())
3204 {
3205 if (!FromRed->add_work_to_bottom_transns(check_complexity::
3206 for_all_transitions_from_bottom_states_a_posteriori_4_4, 1))
3207 {
3208 assert(0 && "no new bottom states to assign work to");
3209 }
3210 FromRed->work_counter.reset_work_counter_4_4();
3211 }
3212 #endif
3213 // 4.15: for all old bottom states s in RedB do
3214 for (bisim_gjkw::permutation_iter_t
3215 s_iter = RedB->marked_bottom_begin();
3216 RedB->marked_bottom_end() != s_iter; ++s_iter)
3217 {
3218 bisim_gjkw::state_info_ptr const s = *s_iter;
3219 // 4.16: Advance the current constellation pointer of s to the
3220 // next constellation it can reach
3221 if (s->current_constln() < s->succ_end() &&
3222 s->current_constln()->target->constln() == SpC)
3223 {
3224 #if !defined(NDEBUG) || defined(COUNT_WORK_BALANCE)
3225 bisim_gjkw::succ_entry::slice_add_work_to_transns(s->current_constln(),
3226 check_complexity::for_all_old_bottom_states_s_in_RedB_4_15,1);
3227 #endif
3228 s->set_current_constln(bisim_gjkw::succ_entry::slice_end(
3229 s->current_constln()));
3230 } else
3231 { mCRL2complexity(s, add_work(check_complexity::
3232 for_all_old_bottom_states_s_in_RedB_selfloop_4_15, 1), );
3233 assert(B == RedB /* we should test: BlueB is empty */);
3234 assert(B->constln() == SpC);
3235 }
3236 assert(s->succ_end() == s->current_constln() ||
3237 /* 4.17: end for */ *SpC < *s->current_constln()->target->constln());
3238 }
3239 /* 4.18: if RedB contains new bottom states then */ assert(RedB->marked_nonbottom_begin() == RedB->marked_nonbottom_end());
3240 if (0 != RedB->unmarked_bottom_size())
3241 {
3242 // 4.19: <_, RfnB> := Refine(RedB, cosplit(RedB, BlueB), {old
3243 // bottom states in RedB}, {})
3244 #ifndef NDEBUG
3245 blue_begin = RedB->begin();
3246 #endif
3247 if (0 != RedB->marked_bottom_size())
3248 {
3249 RedB = refine(RedB, nullptr, nullptr, true); assert(nullptr != RedB); assert(0 == RedB->unmarked_bottom_size());
3250 // 4.26: Destroy all temporary data
3251 // As part of this line, we unmark all states.
3252 RedB->set_marked_bottom_begin(RedB->bottom_end()); assert(RedB->begin() > blue_begin);
3253 RfnB = RedB->begin()[-1]->block;
3254 }
3255 else
3256 {
3257 RfnB = RedB;
3258 #ifndef NDEBUG
3259 RedB = nullptr;
3260 #endif
3261 } assert(RedB != RfnB);
3262 assert(RfnB->begin() == blue_begin);
3263 // do not refine a trivial block
3264 if (1 == RfnB->size())
3265 { assert(0 == RfnB->marked_size());
3266 continue;
3267 }
3268 // 4.20: Register that the transitions from RfnB to SpC need
3269 // postprocessing
3270 bisim_gjkw::B_to_C_desc_iter_t new_slice =
3271 SpC->postprocess_begin[-1].B_to_C_slice; assert(new_slice->from_block() == RfnB);
3272 assert(new_slice->to_constln() == SpC);
3273 SpC->postprocess_begin = new_slice->begin; assert(new_slice->end <= SpC->postprocess_end);
3274 // move the set of transitions to the end of the list
3275 RfnB->to_constln.splice(RfnB->to_constln.end(),
3276 RfnB->to_constln, new_slice);
3277 // 4.21: Restart the procedure (but keep R),
3278 // i. e. go to Line 4.4
3279 goto Line_4_4;
3280 // 4.22: end if
3281 }
3282 // 4.26: Destroy all temporary data
3283 // As part of this line, we unmark all states.
3284 RedB->set_marked_bottom_begin(RedB->bottom_end());
3285 // 4.23: end for
3286 }
3287 while (SpC->postprocess_begin != SpC->postprocess_end);
3288 // 4.24: Delete SpC from R
3289 R.erase(R.begin());
3290 // 4.25: end for
3291 }
3292 /* 4.26: Destroy all temporary data */ assert(R.empty());
3293
3294 return ResultB;
3295}
3296
3297
3298
3299/*=============================================================================
3300= explicit instantiation requests =
3301=============================================================================*/
3302
3303
3304
3305namespace bisim_gjkw
3306{
3307
3308template class bisim_partitioner_gjkw_initialise_helper<lts_lts_t>;
3309template class bisim_partitioner_gjkw_initialise_helper<lts_aut_t>;
3310template class bisim_partitioner_gjkw_initialise_helper<lts_fsm_t>;
3311
3312} // end namespace bisim_gjkw
3313
3314template class bisim_partitioner_gjkw<lts_lts_t>;
3315template class bisim_partitioner_gjkw<lts_aut_t>;
3316template class bisim_partitioner_gjkw<lts_fsm_t>;
3317
3318} // end namespace detail
3319// end namespace lts
3320// end namespace mcrl2
mCRL2complexity
#define mCRL2complexity(unit, call, info_for_debug)
Assigns work to a counter and checks for errors.
Definition check_complexity.h:1891
mcrl2::lts::detail::constln_ptr_less
function object to compare two constln_t pointers based on their contents
Definition liblts_bisim_gjkw.cpp:3034
mcrl2::lts::detail::indexed_sorted_vector_for_transitions
Definition lts_utilities.h:455
ABORT_THIS_COROUTINE
#define ABORT_THIS_COROUTINE()
indicates that this coroutine gives up control to the other one
Definition coroutine.h:366
END_COROUTINE
#define END_COROUTINE
Ends the definition of code for a coroutine.
Definition coroutine.h:203
ABORT_OTHER_COROUTINE
#define ABORT_OTHER_COROUTINE()
indicates that the other coroutine should give up control
Definition coroutine.h:381
COROUTINE_FOR
#define COROUTINE_FOR(location, init, condition, update)
a for loop where every iteration incurs one unit of work
Definition coroutine.h:274
COROUTINE_WHILE
#define COROUTINE_WHILE(location, condition)
a while loop where every iteration incurs one unit of work
Definition coroutine.h:230
COROUTINES_SECTION
#define COROUTINES_SECTION
begin a section with two coroutines
Definition coroutine.h:145
COROUTINE_DO_WHILE
#define COROUTINE_DO_WHILE(location, condition)
a do { } while loop where every iteration incurs one unit of work
Definition coroutine.h:317
END_COROUTINES_SECTION
#define END_COROUTINES_SECTION
Close a section containing coroutines.
Definition coroutine.h:211
COROUTINE
#define COROUTINE
Define the code for a coroutine.
Definition coroutine.h:195
END_COROUTINE_WHILE
#define END_COROUTINE_WHILE
ends a loop started with COROUTINE_WHILE
Definition coroutine.h:255
END_COROUTINE_FOR
#define END_COROUTINE_FOR
ends a loop started with COROUTINE_FOR
Definition coroutine.h:300
COROUTINE_LABELS
#define COROUTINE_LABELS(locations)
Declare the interrupt locations for the coroutines.
Definition coroutine.h:164
END_COROUTINE_DO_WHILE
#define END_COROUTINE_DO_WHILE
ends a loop started with COROUTINE_DO_WHILE
Definition coroutine.h:339
TERMINATE_COROUTINE_SUCCESSFULLY
#define TERMINATE_COROUTINE_SUCCESSFULLY()
terminate the pair of coroutines successfully
Definition coroutine.h:351
mCRL2log
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:435
mcrl2::lts::detail::bisim_gjkw
Definition liblts_bisim_gjkw.cpp:34