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